mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Triangulated.Triangulated
CategoryTheory.Triangulated.Octahedron.mem : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃}
  {comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ ⟶ Z₁₂}
  {w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  {h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂}
  {h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  {h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  (self : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃),
  CategoryTheory.Pretriangulated.Triangle.mk self.m₁ self.m₃
      (CategoryTheory.CategoryStruct.comp w₂₃ ((CategoryTheory.shiftFunctor C 1).map v₁₂)) ∈
    CategoryTheory.Pretriangulated.distinguishedTriangles
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgHom.fst_apply : ∀ (R : Type u_1) (A : Type u_2) (B : Type u_3) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Star A] [inst_4 : Semiring B] [inst_5 : Algebra R B] [inst_6 : Star B] (self : A × B),
  (StarAlgHom.fst R A B) self = self.1
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.congr_trans : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] (v : Valuation R Γ₀)
  {S : Type u_3} [inst_2 : Ring S] {Λ₀ : Type u_4} [inst_3 : LinearOrderedCommGroupWithZero Λ₀] (w : Valuation S Λ₀)
  {T : Type u_5} [inst_4 : Ring T] (u : Valuation T Γ₀) (f : R ≃+* S) (g : S ≃+* T),
  WithVal.congr v u (f.trans g) = (WithVal.congr v w f).trans (WithVal.congr w u g)
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.addSubgroup_eq_bot : ∀ (M : Type u_1) [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M],
  ArchimedeanClass.addSubgroup ⊤ = ⊥
-- Lean.Meta.Tactic.Grind.Theorems
_private.Lean.Meta.Tactic.Grind.Theorems.0.Lean.Meta.Grind.Theorems.mk : {α : Type} →
  Lean.PHashMap Lean.Name (List α) →
    Lean.PHashSet Lean.Meta.Grind.Origin →
      Lean.PHashSet Lean.Meta.Grind.Origin → Lean.PHashMap Lean.Meta.Grind.Origin (List α) → Lean.Meta.Grind.Theorems α
-- Mathlib.RingTheory.PowerSeries.WellKnown
PowerSeries.invOneSubPow.eq_2 : ∀ (S : Type u_1) [inst : CommRing S] (d : ℕ),
  PowerSeries.invOneSubPow S d.succ =
    { val := PowerSeries.mk fun n => ↑((d + n).choose d), inv := (1 - PowerSeries.X) ^ (d + 1), val_inv := ⋯,
      inv_val := ⋯ }
-- Mathlib.Algebra.GradedMonoid
/-- The `CommMonoid` structure derived from `GCommMonoid A`.  -/
GradedMonoid.GradeZero.commMonoid : {ι : Type u_1} → (A : ι → Type u_2) → [inst : AddCommMonoid ι] → [GradedMonoid.GCommMonoid A] → CommMonoid (A 0)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
/-- The polar coordinate open partial homeomorphism of `ℝ^r₁ × (ℝ × ℝ)^r₂` defined as the identity on
the first component and mapping `(rᵢ cos θᵢ, rᵢ sin θᵢ)ᵢ` to `(rᵢ, θᵢ)ᵢ` on the second component.
 -/
NumberField.mixedEmbedding.polarCoordReal : (K : Type u_1) →
  [inst : Field K] →
    [NumberField K] →
      OpenPartialHomeomorph (NumberField.mixedEmbedding.realMixedSpace K) (NumberField.mixedEmbedding.realMixedSpace K)
-- Mathlib.Topology.Homeomorph.Lemmas
Homeomorph.toEquiv_piCongr : ∀ {ι₁ : Type u_7} {ι₂ : Type u_8} {Y₁ : ι₁ → Type u_9} {Y₂ : ι₂ → Type u_10}
  [inst : (i₁ : ι₁) → TopologicalSpace (Y₁ i₁)] [inst_1 : (i₂ : ι₂) → TopologicalSpace (Y₂ i₂)] (e : ι₁ ≃ ι₂)
  (F : (i₁ : ι₁) → Y₁ i₁ ≃ₜ Y₂ (e i₁)),
  (Homeomorph.piCongr e F).toEquiv = (Equiv.piCongrRight fun i => (F i).toEquiv).trans (Equiv.piCongrLeft Y₂ e)
-- Init.GrindInstances.ToInt
Lean.Grind.instMulBitVecUint : ∀ {v : ℕ}, Lean.Grind.ToInt.Mul (BitVec v) (Lean.Grind.IntInterval.uint v)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey!_insert_le_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k : α} {v : β k}, (cmp (t.insert k v).minKey! k).isLE = true
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.instIsCentralScalar : ∀ {M : Type u_2} {α : Type u_5} [inst : NonUnitalNonAssocSemiring α] [inst_1 : Monoid M] [inst_2 : DistribMulAction M α]
  [inst_3 : SMulCommClass M α α] [inst_4 : IsScalarTower M α α] [inst_5 : DistribMulAction Mᵐᵒᵖ α]
  [inst_6 : IsCentralScalar M α], IsCentralScalar M (CentroidHom α)
-- Mathlib.Algebra.Group.Fin.Basic
Fin.rev_sub : ∀ {n : ℕ} (a b : Fin n), (a - b).rev = a.rev + b
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_eq_zero : ∀ {ι : Type u_1} {M : Type u_4} {s : Finset ι} [inst : AddCommMonoid M] {f : ι → M},
  (∀ x ∈ s, f x = 0) → ∑ x ∈ s, f x = 0
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound
Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.reduce_fold_fn.match_1.congr_eq_1 : ∀ (motive : Std.Tactic.BVDecide.LRAT.Internal.Assignment → Sort u_1) (x : Std.Tactic.BVDecide.LRAT.Internal.Assignment)
  (h_1 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos)
  (h_2 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg)
  (h_3 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.both)
  (h_4 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned),
  x = Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos →
    (match x with
      | Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos => h_1 ()
      | Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg => h_2 ()
      | Std.Tactic.BVDecide.LRAT.Internal.Assignment.both => h_3 ()
      | Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned => h_4 ()) ≍
      h_1 ()
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.Closeds.isClopen_singleton_bot : ∀ {α : Type u_1} [inst : UniformSpace α], IsClopen {⊥}
-- Mathlib.Data.Nat.Hyperoperation
hyperoperation_ge_four_zero : ∀ (n k : ℕ), hyperoperation (n + 4) 0 k = if Even k then 1 else 0
-- Lean.Elab.MutualInductive
Lean.Elab.Command.ElabHeaderResult.toPreElabHeaderResult : Lean.Elab.Command.ElabHeaderResult → Lean.Elab.Command.PreElabHeaderResult
-- Init.Data.Ord.Array
_private.Init.Data.Ord.Array.0.Array.compareLex.match_1.splitter : (motive : Ordering → Sort u_1) →
  (x : Ordering) → (Unit → motive Ordering.lt) → (Unit → motive Ordering.eq) → (Unit → motive Ordering.gt) → motive x
-- Mathlib.Order.Interval.Finset.Floor
Nat.cast_mem_Iic_iff : ∀ {α : Type u_1} [inst : Semiring α] [inst_1 : LinearOrder α] [inst_2 : FloorSemiring α] {b : α} {n : ℕ},
  0 ≤ b → (↑n ∈ Set.Iic b ↔ n ∈ Finset.Iic ⌊b⌋₊)
-- Lean.Parser.Term
Lean.Parser.Term.isIdent : Lean.Syntax → Bool
-- Mathlib.Order.Closure
LowerAdjoint.idempotent : ∀ {α : Type u_1} {β : Type u_4} [inst : PartialOrder α] [inst_1 : Preorder β] {u : β → α} (l : LowerAdjoint u) (x : α),
  u (l.toFun (u (l.toFun x))) = u (l.toFun x)
-- Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
isOpen.dynEntourage : ∀ {X : Type u_1} {U : SetRel X X} [inst : TopologicalSpace X] {T : X → X},
  Continuous T → IsOpen U → ∀ (n : ℕ), IsOpen (Dynamics.dynEntourage T U n)
-- Mathlib.Control.Monad.Cont
ContT.monadLift_bind : ∀ {r : Type u} {m : Type u → Type v} [inst : Monad m] [LawfulMonad m] {α β : Type u} (x : m α) (f : α → m β),
  monadLift (x >>= f) = monadLift x >>= monadLift ∘ f
-- Lean.Elab.MutualInductive
/-- Inferred resulting universe  -/
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.ResultingUniverseResult.u : Lean.Elab.Command.ResultingUniverseResult✝ → Lean.Level
-- Mathlib.Analysis.InnerProductSpace.Reproducing
RKHS.ext : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {X : Type u_2} {V : Type u_3} [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] {H : Type u_4} [inst_3 : NormedAddCommGroup H] [inst_4 : InnerProductSpace 𝕜 H]
  [inst_5 : RKHS 𝕜 H X V] {f g : H}, (∀ (x : X), f x = g x) → f = g
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- Continuous linear maps between modules. We only put the type classes that are necessary for the
definition, although in applications `M` and `M₂` will be topological modules over the topological
ring `R`.  -/
ContinuousLinearMap : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : Semiring S] →
        (R →+* S) →
          (M : Type u_3) →
            [TopologicalSpace M] →
              [inst_3 : AddCommMonoid M] →
                (M₂ : Type u_4) →
                  [TopologicalSpace M₂] →
                    [inst_5 : AddCommMonoid M₂] → [Module R M] → [Module S M₂] → Type (max u_3 u_4)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
SheafOfModules.instIsLeftAdjointOverOverRingCatPushforwardIdSheafOver : ∀ {C : Type u'} [inst : CategoryTheory.Category.{v', u'} C] [CategoryTheory.Limits.HasBinaryProducts C]
  {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} (x : C),
  (SheafOfModules.pushforward (CategoryTheory.CategoryStruct.id (R.over x))).IsLeftAdjoint
-- Mathlib.Logic.Relation
Relation.ReflGen.mono : ∀ {α : Type u_1} {r p : α → α → Prop}, r ≤ p → Relation.ReflGen r ≤ Relation.ReflGen p
-- Mathlib.Algebra.Group.Subgroup.Ker
AddSubgroup.map_injective : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {f : G →+ N},
  Function.Injective ⇑f → Function.Injective (AddSubgroup.map f)
-- Mathlib.Algebra.Group.Subgroup.Pointwise
AddSubgroup.closure_nsmul_le : ∀ {G : Type u_2} [inst : AddGroup G] {s : Set G} {n : ℕ}, AddSubgroup.closure (n • s) ≤ AddSubgroup.closure s
-- Mathlib.Data.List.Defs
_private.Mathlib.Data.List.Defs.0.List.map₂Left'.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : List α → List β → Sort u_3) →
      (x : List α) →
        (x_1 : List β) →
          ((bs : List β) → motive [] bs) →
            ((a : α) → (as : List α) → motive (a :: as) []) →
              ((a : α) → (as : List α) → (b : β) → (bs : List β) → motive (a :: as) (b :: bs)) → motive x x_1
-- Mathlib.Algebra.Group.End
MonoidHom.toHomPerm_apply_symm_apply : ∀ {α : Type u_4} {G : Type u_7} [inst : Group G] (f : G →* Function.End α) (x : G),
  ⇑(Equiv.symm (f.toHomPerm x)) = ↑(f.toHomUnits x)⁻¹
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.pow.inj : ∀ {a : Lean.Grind.CommRing.Expr} {k : ℕ} {a_1 : Lean.Grind.CommRing.Expr} {k_1 : ℕ},
  a.pow k = a_1.pow k_1 → a = a_1 ∧ k = k_1
-- Lean.Meta.WHNF
/-- Add auxiliary annotation to indicate the `match`-expression `e` must be reduced when performing smart unfolding.  -/
Lean.Meta.markSmartUnfoldingMatch : Lean.Expr → Lean.Expr
-- Init.Data.AC
Lean.Data.AC.instBEqExpr : BEq Lean.Data.AC.Expr
-- Mathlib.RingTheory.RingHom.Integral
/-- `S` is an integral `R`-algebra if there exists a set `{ r }` that
spans `R` such that each `Sᵣ` is an integral `Rᵣ`-algebra.  -/
RingHom.isIntegral_ofLocalizationSpan : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] x => x.IsIntegral
-- Mathlib.Data.Rat.Floor
Rat.den_intFract : ∀ (x : ℚ), (Int.fract x).den = x.den
-- Mathlib.CategoryTheory.Triangulated.Generators
/-- An object property `P` is called a strong triangulated generator, if every object
can be reached from objects in `P` by shifts, binary products, retracts and at most `n`
extensions, for some fixed `n`.  -/
CategoryTheory.ObjectProperty.IsStrongTriangulatedGenerator : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.HasShift C ℤ] →
        [inst_3 : CategoryTheory.Preadditive C] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [CategoryTheory.Pretriangulated C] → CategoryTheory.ObjectProperty C → Prop
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.MonadHom.app_μ_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T₁ T₂ : CategoryTheory.Monad C}
  (self : CategoryTheory.MonadHom T₁ T₂) (X : C) {Z : C} (h : T₂.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (T₁.μ.app X) (CategoryTheory.CategoryStruct.comp (self.app X) h) =
    CategoryTheory.CategoryStruct.comp (T₁.map (self.app X))
      (CategoryTheory.CategoryStruct.comp (self.app (T₂.obj X)) (CategoryTheory.CategoryStruct.comp (T₂.μ.app X) h))
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
SimpleGraph.isBipartiteWith_bipartiteDoubleCover : ∀ {V : Type u_1} {G : SimpleGraph V},
  G.bipartiteDoubleCover.IsBipartiteWith {v | v.isLeft = true} {w | w.isRight = true}
-- Mathlib.Algebra.Order.Group.End
OrderHom.instIsOneApplyEqSelf : ∀ {α : Type u_1} [inst : Preorder α], IsOneApplyEqSelf (α →o α) α
-- Mathlib.CategoryTheory.Quotient.Linear
CategoryTheory.Quotient.linear_functor : ∀ (R : Type u_1) {C : Type u_2} [inst : Semiring R] [inst_1 : CategoryTheory.Category.{v_1, u_2} C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear R C] (r : HomRel C)
  [inst_4 : CategoryTheory.Congruence r] (hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂))
  [inst_5 : CategoryTheory.Preadditive (CategoryTheory.Quotient r)]
  [inst_6 : (CategoryTheory.Quotient.functor r).Additive],
  CategoryTheory.Functor.Linear R (CategoryTheory.Quotient.functor r)
-- Lean.Widget.UserWidget
Lean.Widget.GetWidgetSourceParams.mk.injEq : ∀ (hash : UInt64) (pos : Lean.Lsp.Position) (hash_1 : UInt64) (pos_1 : Lean.Lsp.Position),
  ({ hash := hash, pos := pos } = { hash := hash_1, pos := pos_1 }) = (hash = hash_1 ∧ pos = pos_1)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.yonedaAddMon_map_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {X Y : CategoryTheory.AddMon C} (ψ : X ⟶ Y) (x : Cᵒᵖ),
  (CategoryTheory.yonedaAddMon.map ψ).app x =
    AddMonCat.ofHom (CategoryTheory.IsAddMonHom.addMonoidHom ψ.hom (Opposite.unop x))
-- Mathlib.RepresentationTheory.FiniteIndex
Rep.coindResAdjunction_counit_app : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Group G] {S : Subgroup G}
  [inst_2 : DecidableRel ⇑(QuotientGroup.rightRel S)] [inst_3 : S.FiniteIndex] (B : Rep.{max w u v, u, v} k G),
  (Rep.coindResAdjunction k S).counit.app B =
    CategoryTheory.CategoryStruct.comp (Rep.res S.subtype B).indCoindIso.inv
      ((Rep.indResAdjunction k S.subtype).counit.app B)
-- Mathlib.Topology.Order.IntermediateValue
IsPreconnected.intermediate_value_Ioc : ∀ {X : Type u} {α : Type v} [inst : TopologicalSpace X] [inst_1 : LinearOrder α] [inst_2 : TopologicalSpace α]
  [OrderClosedTopology α] {s : Set X},
  IsPreconnected s →
    ∀ {a : X} {l : Filter X},
      a ∈ s →
        ∀ [l.NeBot],
          l ≤ Filter.principal s →
            ∀ {f : X → α}, ContinuousOn f s → ∀ {v : α}, Filter.Tendsto f l (nhds v) → Set.Ioc v (f a) ⊆ f '' s
-- Mathlib.Algebra.Homology.Embedding.Connect
CochainComplex.ConnectData.d_sub_one_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} (h : CochainComplex.ConnectData K L), h.d (-1) 0 = h.d₀
-- Mathlib.Topology.Algebra.Group.Basic
Filter.map_divLeft_nhdsNE : ∀ {G : Type w} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] {c a : G},
  Filter.map (fun x => c / x) (nhdsWithin a {a}ᶜ) = nhdsWithin (c / a) {c / a}ᶜ
-- Mathlib.Data.Set.Restrict
Set.injOn_iff_injective : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β}, Set.InjOn f s ↔ Function.Injective (s.domRestrict f)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopLayer.go.eq_def : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {outWidth : ℕ} {aig : Std.Sat.AIG α} {w len : ℕ} (iterNum : ℕ)
  (oldLayer : aig.RefVec (len * w)) (newLayer : aig.RefVec (iterNum * w)) (hold : 2 * (iterNum - 1) < len)
  (hout : outWidth = (len + 1) / 2 * w),
  Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopLayer.go iterNum oldLayer newLayer hold hout =
    if hlen : 0 < len - iterNum * 2 then
      let res :=
        Std.Tactic.BVDecide.BVExpr.bitblast.blastExtract aig
          { w := len * w, vec := oldLayer, start := 2 * iterNum * w };
      let aig_1 := res.aig;
      let op1 := res.vec;
      have this := ⋯;
      let oldLayer_1 := oldLayer.cast this;
      have newLayer_1 := newLayer.cast this;
      let res :=
        Std.Tactic.BVDecide.BVExpr.bitblast.blastExtract aig_1
          { w := len * w, vec := oldLayer_1, start := (2 * iterNum + 1) * w };
      let aig_2 := res.aig;
      let op2 := res.vec;
      have this_1 := ⋯;
      have oldLayer_2 := oldLayer_1.cast this_1;
      have newLayer_2 := newLayer_1.cast this_1;
      let op1 := op1.cast this_1;
      let res := Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd aig_2 { lhs := op1, rhs := op2 };
      let aig_3 := res.aig;
      have add := res.vec;
      have this_2 := ⋯;
      have oldLayer_3 := oldLayer_2.cast this_2;
      have newLayer_3 := newLayer_2.cast this_2;
      let res :=
        Std.Tactic.BVDecide.BVExpr.bitblast.blastAppend aig_3
          { lw := w, rw := iterNum * w, lhs := add, rhs := newLayer_3, h := ⋯ };
      have aig_4 := res.aig;
      have newLayer_4 := res.vec;
      have this_3 := ⋯;
      have oldLayer_4 := oldLayer_3.cast this_3;
      Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopLayer.go (iterNum + 1) oldLayer_4 newLayer_4 ⋯ hout
    else
      have hcast := ⋯;
      { aig := aig, vec := hcast ▸ newLayer }
-- Mathlib.Data.NNReal.Defs
NNReal.not_toReal_neg : ∀ {r : NNReal}, ¬↑r < 0
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.eq_spanSingleton_mul : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  [inst_3 : IsLocalization S P] {x : P} {I J : FractionalIdeal S P},
  I = FractionalIdeal.spanSingleton S x * J ↔ (∀ zI ∈ I, ∃ zJ ∈ J, x * zJ = zI) ∧ ∀ z ∈ J, x * z ∈ I
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- The inverse of the left unitor as a term of `normalExpr`.  -/
Mathlib.Tactic.BicategoryLike.NormalExpr.leftUnitorInvM : {m : Type → Type} →
  [Monad m] →
    [Mathlib.Tactic.BicategoryLike.MonadMor₂Iso m] →
      [Mathlib.Tactic.BicategoryLike.MonadNormalExpr m] →
        Mathlib.Tactic.BicategoryLike.Mor₁ → m Mathlib.Tactic.BicategoryLike.NormalExpr
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.length_surjective : ∀ {α : Type u_1} [Nonempty α], Function.Surjective FreeAddMonoid.length
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.Grp.Hom.hom_hom_div : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {G H : CategoryTheory.Grp C} [inst_3 : CategoryTheory.IsCommMonObj H.X]
  (f g : G ⟶ H), (f / g).hom.hom = f.hom.hom / g.hom.hom
-- Lean.DocString.Markdown
Lean.Doc.MarkdownInline.mk : {i : Type u} →
  ((Lean.Doc.Inline i → Lean.Doc.MarkdownM (Array String)) →
      i → Array (Lean.Doc.Inline i) → Lean.Doc.MarkdownM (Array String)) →
    Lean.Doc.MarkdownInline i
-- Mathlib.Data.List.AList
AList.insert_singleton_eq : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {b b' : β a},
  AList.insert a b (AList.singleton a b') = AList.singleton a b
-- Mathlib.LinearAlgebra.RootSystem.CartanMatrix
RootPairing.Base.cartanMatrix_apply_eq_zero_iff_pairing : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} (b : P.Base)
  [inst_5 : P.IsCrystallographic] [CharZero R] {i j : ↥b.support}, b.cartanMatrix i j = 0 ↔ P.pairing ↑i ↑j = 0
-- Mathlib.Control.Traversable.Basic
ApplicativeTransformation.instCoeFunForallForall : (F : Type u → Type v) →
  [inst : Applicative F] →
    (G : Type u → Type w) →
      [inst_1 : Applicative G] → CoeFun (ApplicativeTransformation F G) fun x => {α : Type u} → F α → G α
-- Mathlib.Order.Concept
Concept.isUpperSet_intent_le : ∀ {α : Type u_6} [inst : Preorder α] (c : Concept α α fun x1 x2 => x1 ≤ x2), IsUpperSet c.intent
-- Mathlib.Data.Nat.Factorization.PrimePow
Nat.Primes.prodNatEquiv_apply : ∀ (p : Nat.Primes) (k : ℕ), Nat.Primes.prodNatEquiv (p, k) = ⟨↑p ^ (k + 1), ⋯⟩
-- Mathlib.FieldTheory.Finite.Basic
FiniteField.X_pow_card_sub_X_natDegree_eq : ∀ (K' : Type u_3) [inst : Field K'] {p : ℕ}, 1 < p → (Polynomial.X ^ p - Polynomial.X).natDegree = p
-- Init.MetaTypes
/-- Which structure types should eta be used with?  -/
Lean.Meta.EtaStructMode : Type
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.instModuleOfSMulCommClassRealOfContinuousConstSMul : {E : Type u_3} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℝ E] →
      {Ω : TopologicalSpace.Opens E} →
        {F : Type u_4} →
          [inst_2 : NormedAddCommGroup F] →
            [inst_3 : NormedSpace ℝ F] →
              {n : ℕ∞} →
                {R : Type u_6} →
                  [inst_4 : Semiring R] →
                    [inst_5 : Module R F] →
                      [SMulCommClass ℝ R F] → [ContinuousConstSMul R F] → Module R (TestFunction Ω F n)
-- Mathlib.LinearAlgebra.Basis.VectorSpace
/-- For a module over a division ring, the span of a nonzero element is an atom of the
lattice of submodules.  -/
nonzero_span_atom : ∀ {K : Type u_3} {V : Type u_4} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] (v : V),
  v ≠ 0 → IsAtom (K ∙ v)
-- Mathlib.Probability.Kernel.CondDistrib
ProbabilityTheory.aestronglyMeasurable_integral_condDistrib : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] [inst_3 : NormedAddCommGroup F] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_4 : MeasureTheory.IsFiniteMeasure μ] {X : α → β} {Y : α → Ω} {mβ : MeasurableSpace β} {f : β × Ω → F}
  [inst_5 : NormedSpace ℝ F],
  AEMeasurable X μ →
    AEMeasurable Y μ →
      MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ) →
        MeasureTheory.AEStronglyMeasurable (fun a => ∫ (y : Ω), f (X a, y) ∂(ProbabilityTheory.condDistrib Y X μ) (X a))
          μ
-- Mathlib.CategoryTheory.Abelian.Basic
/-- There is a canonical isomorphism between the abelian coimage and the categorical image of a
morphism.  -/
CategoryTheory.Abelian.coimageIsoImage' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {X Y : C} → (f : X ⟶ Y) → CategoryTheory.Abelian.coimage f ≅ CategoryTheory.Limits.image f
-- Mathlib.Algebra.MonoidAlgebra.Module
MonoidAlgebra.symm_mapDomainLinearEquiv : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : Module R S] (e : M ≃ N),
  (MonoidAlgebra.mapDomainLinearEquiv R S e).symm = MonoidAlgebra.mapDomainLinearEquiv R S e.symm
-- Mathlib.LinearAlgebra.Prod
LinearMap.coe_prod : ∀ {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module R M₂]
  [inst_6 : Module R M₃] (f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃), ⇑(f.prod g) = Function.prod ⇑f ⇑g
-- Mathlib.Algebra.Group.TypeTags.Basic
instDecidableEqAdditive : {α : Type u} → [h : DecidableEq α] → DecidableEq (Additive α)
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.Lp.simpleFunc.stronglyMeasurable : ∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {p : ENNReal}
  {μ : MeasureTheory.Measure α} (f : ↥(MeasureTheory.Lp.simpleFunc E p μ)),
  MeasureTheory.StronglyMeasurable ⇑(MeasureTheory.Lp.simpleFunc.toSimpleFunc f)
-- Mathlib.Data.Fin.SuccPred
Fin.castSucc_lt_or_lt_succ : ∀ {n : ℕ} (p : Fin (n + 1)) (i : Fin n), i.castSucc < p ∨ p < i.succ