semorrison

[init]
def Array.mapMUnsafe.map._at.Simps.applyProjectionRules._spec_1 (x_1 : usize) (x_2 : usize) (x_3 : obj) : obj :=
  let x_4 : u8 := USize.decLt x_2 x_1;
  case x_4 : obj of
  Bool.false →
    ret x_3
  Bool.true →
    let x_5 : obj := Array.uget ◾ x_3 x_2 ◾;
    let x_6 : obj := 0;

semorrison

  * `mapIdx` / `mapIdxM`
  * `findIdx` / `findIdx?`
  * `indexOf`
  * `List.Subset`
  * `List.bagInter`
  * `List.diff`
  * `List.tail`
  * `List.next?`
  * `after`
  * `insertNth` / `removeNth` / `modifyNth` / `modifyNthTail` / `modifyHead` / `modifyLast`

semorrison

info: [Meta.synthInstance] 💥 AddMonoidHomClass (AddGroupSeminorm ℂ) ℂ ℝ
  [Meta.synthInstance] new goal AddMonoidHomClass (AddGroupSeminorm ℂ) ℂ ℝ
    [Meta.synthInstance.instances] #[AddEquivClass.instAddMonoidHomClass, @SemilinearMapClass.instAddMonoidHomClass, @NonUnitalRingHomClass.toAddMonoidHomClass, @RingHomClass.toAddMonoidHomClass, @DistribMulActionSemiHomClass.toAddMonoidHomClass, @CentroidHomClass.toAddMonoidHomClass, @ContinuousAddMonoidHomClass.toAddMonoidHomClass]
  [Meta.synthInstance] ✅ apply @ContinuousAddMonoidHomClass.toAddMonoidHomClass to AddMonoidHomClass
        (AddGroupSeminorm ℂ) ℂ ℝ
    [Meta.synthInstance.tryResolve] ✅ AddMonoidHomClass (AddGroupSeminorm ℂ) ℂ
          ℝ ≟ AddMonoidHomClass (AddGroupSeminorm ℂ) ℂ ℝ
    [Meta.synthInstance] new goal TopologicalSpace ℂ
      [Meta.synthInstance.instances] #[WithIdeal.instTopologicalSpace, @UniformSpace.toTopologicalSpace, @UpgradedStandardBorel.toTopologicalSpace, Scott.topologicalSpace, @AlexandrovDiscreteSpace.toTopologicalSpace]
 

semorrison

info: [Meta.synthInstance] ❌ AddMonoidHomClass (AddGroupSeminorm ℂ) ℂ ℝ
  [Meta.synthInstance] new goal AddMonoidHomClass (AddGroupSeminorm ℂ) ℂ ℝ
    [Meta.synthInstance.instances] #[AddEquivClass.instAddMonoidHomClass, @SemilinearMapClass.instAddMonoidHomClass, @NonUnitalRingHomClass.toAddMonoidHomClass, @RingHomClass.toAddMonoidHomClass, @DistribMulActionSemiHomClass.toAddMonoidHomClass, @CentroidHomClass.toAddMonoidHomClass, @ContinuousAddMonoidHomClass.toAddMonoidHomClass]
  [Meta.synthInstance] ✅ apply @ContinuousAddMonoidHomClass.toAddMonoidHomClass to AddMonoidHomClass
        (AddGroupSeminorm ℂ) ℂ ℝ
    [Meta.synthInstance.tryResolve] ✅ AddMonoidHomClass (AddGroupSeminorm ℂ) ℂ
          ℝ ≟ AddMonoidHomClass (AddGroupSeminorm ℂ) ℂ ℝ
    [Meta.synthInstance] new goal TopologicalSpace ℂ
      [Meta.synthInstance.instances] #[WithIdeal.instTopologicalSpace, @UniformSpace.toTopologicalSpace, @UpgradedStandardBorel.toTopologicalSpace, Scott.topologicalSpace, @AlexandrovDiscreteSpace.toTopologicalSpace]
 

semorrison

import Mathlib

/--
error: failed to synthesize
  AddMonoidHomClass (AddGroupSeminorm ℂ) ℂ ℝ
(deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit)
-/
#guard_msgs in
#synth AddMonoidHomClass (AddGroupSeminorm ℂ) ℂ ℝ

semorrison

theorem _root_.Nat.mod_eq_sub_div_mul {a b : Nat} : a % b = a - (a / b) * b := by
  rw [eq_comm, Nat.sub_eq_iff_eq_add (Nat.div_mul_le_self _ _), Nat.mul_comm, Nat.mod_add_div]

theorem _root_.Nat.mod_eq_sub_mul_div {a b : Nat} : a % b = a - b * (a / b) := by
  rw [Nat.mod_eq_sub_div_mul, Nat.mul_comm]

theorem _root_.BitVec.extractLsb_flatten (hi lo : Nat) {w  : Nat} (vs : List (BitVec w))
    (w₁ : lo ≤ hi) (w₂ : hi < w * vs.length) (h : hi / w = lo / w) :
    extractLsb hi lo (BitVec.flatten vs) =

semorrison

intervalIntegral.integral_comp_smul_deriv''
Filter.lift_lift'_same_le_lift'
PartialHomeomorph.extend_left_inv'
Submodule.disjoint_span_singleton'
ContinuousOn.comp'
Computation.map_think'
List.LT'
ULift.mulDistribMulAction'
set_integral_withDensity_eq_set_integral_smul₀'
Bimod.TensorBimod.right_assoc'

semorrison

[class_instances]  class-instance resolution trace
[class_instances] (0) ?x_0 : @mono C _inst_1 X Y f := @category_theory.initial_mono ?x_1 ?x_2 ?x_3 ?x_4 ?x_5 ?x_6
failed is_def_eq
[class_instances] (0) ?x_0 : @mono C _inst_1 X Y f := @category_theory.image_to_kernel_map_mono ?x_7 ?x_8 ?x_9 ?x_10 ?x_11 ?x_12 ?x_13 ?x_14 ?x_15 ?x_16 ?x_17
failed is_def_eq
[class_instances] (0) ?x_0 : @mono C _inst_1 X Y f := @AddCommGroup.category_theory.mono ?x_18 ?x_19 ?x_20
failed is_def_eq
[class_instances] (0) ?x_0 : @mono C _inst_1 X Y f := @abelian.mono_pushout_of_mono_g ?x_21 ?x_22 ?x_23 ?x_24 ?x_25 ?x_26 ?x_27 ?x_28 ?x_29 ?x_30
failed is_def_eq
[class_instances] (0) ?x_0 : @mono C _inst_1 X Y f := @abelian.mono_pushout_of_mono_f ?x_31 ?x_32 ?x_33 ?x_34 ?x_35 ?x_36 ?x_37 ?x_38 ?x_39 ?x_40

semorrison

1393c1393
< add_equiv.map_sum: algebra/big_operators.lean
---
> add_equiv.map_sum: algebra/big_operators/basic.lean
1831c1831
< add_monoid_hom.map_sum: algebra/big_operators.lean
---
> add_monoid_hom.map_sum: algebra/big_operators/basic.lean
14853c14853
< directed.finset_le: algebra/big_operators.lean

semorrison

import category_theory.follow_your_nose

universes u₁ v₁

open category_theory
open opposite

namespace terse

variables (C : Type u₁) [𝒞 : category.{v₁+1} C]