mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.App
/-- Instructs the elaborator to elaborate applications of the given declaration without an expected
type. This may prevent the elaborator from incorrectly inferring implicit arguments.
 -/
Lean.Elab.Term.elabWithoutExpectedTypeAttr : Lean.TagAttribute
-- Mathlib.CategoryTheory.Adjunction.Reflective
/-- A functor is *reflective*, or *a reflective inclusion*, if it is fully faithful and right adjoint.
 -/
CategoryTheory.Reflective : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor D C → Type (max (max (max u₁ u₂) v₁) v₂)
-- Mathlib.Data.Finset.PImage
Finset.coe_pimage : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {f : α →. β} [inst_1 : (x : α) → Decidable (f x).Dom]
  {s : Finset α}, ↑(Finset.pimage f s) = f.image ↑s
-- Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Real.tendsto_rightDeriv_mul_log_atTop : Filter.Tendsto (fun x => derivWithin (fun x => x * Real.log x) (Set.Ioi x) x) Filter.atTop Filter.atTop
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.singletonMulHom_apply : ∀ {α : Type u_2} [inst : Mul α] (a : α), Set.singletonMulHom a = {a}
-- Init.Data.Array.Nat
Array.prod_reverse_nat : ∀ (xs : Array ℕ), xs.reverse.prod = xs.prod
-- Mathlib.RingTheory.Nullstellensatz
MvPolynomial.zeroLocus_span : ∀ {k : Type u_1} {K : Type u_2} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] {σ : Type u_3}
  (S : Set (MvPolynomial σ k)), MvPolynomial.zeroLocus K (Ideal.span S) = {x | ∀ p ∈ S, (MvPolynomial.aeval x) p = 0}
-- Lean.Message
Lean.Kernel.Exception.toMessageData : Lean.Kernel.Exception → Lean.Options → Lean.MessageData
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_alter! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF →
    ∀ {k k' fallback : α} {f : Option (β k) → Option (β k)},
      (Std.DTreeMap.Internal.Impl.alter! k f t).getKeyD k' fallback =
        if compare k k' = Ordering.eq then if (f (t.get? k)).isSome = true then k else fallback
        else t.getKeyD k' fallback
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
/-- If `f` is integrable, then for any `c > 0` the set `{x | f x > c}` has finite
measure.  -/
MeasureTheory.Integrable.measure_gt_lt_top : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {f : α → β} [inst_1 : Lattice β] [HasSolidNorm β] [AddLeftMono β],
  MeasureTheory.Integrable f μ → ∀ {ε : β}, 0 < ε → μ {a | ε < f a} < ⊤
-- Lean.Data.Lsp.Basic
Lean.Lsp.instFromJsonPartialResultParams : Lean.FromJson Lean.Lsp.PartialResultParams
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
/-- Eta-expanded form of `iteratedDeriv_mul` -/
iteratedDeriv_fun_mul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : ℕ} {x : 𝕜} {𝔸 : Type u_5} [inst_1 : NormedRing 𝔸]
  [inst_2 : NormedAlgebra 𝕜 𝔸] {f g : 𝕜 → 𝔸},
  ContDiffAt 𝕜 (↑n) f x →
    ContDiffAt 𝕜 (↑n) g x →
      iteratedDeriv n (fun i => f i * g i) x =
        ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * iteratedDeriv i f x * iteratedDeriv (n - i) g x
-- Mathlib.Topology.Constructions.SumProd
isOpen_sum_iff : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set (X ⊕ Y)},
  IsOpen s ↔ IsOpen (Sum.inl ⁻¹' s) ∧ IsOpen (Sum.inr ⁻¹' s)
-- Mathlib.Data.LawfulXor.Basic
instAssociativeXor_mathlib : ∀ {α : Type u_1} [inst : XorOp α] [inst_1 : Zero α] [LawfulXor α], Std.Associative XorOp.xor
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey!_diff_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₁ → (t₁ \ t₂).getKey! k = default
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Internal.USquash.inflate.inj : ∀ {α : Type v} {x : Std.Internal.Small α} {x_1 y : Std.Internal.USquash α}, x_1.inflate = y.inflate → x_1 = y
-- Mathlib.Algebra.GroupWithZero.Basic
/-- In a monoid with zero, zero equals one if and only if all elements of that semiring
are equal.  -/
subsingleton_iff_zero_eq_one : ∀ {M₀ : Type u_1} [inst : MulZeroOneClass M₀], 0 = 1 ↔ Subsingleton M₀
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupSeminorm.apply_one : ∀ {E : Type u_3} [inst : AddGroup E] [inst_1 : DecidableEq E] (x : E), 1 x = if x = 0 then 0 else 1
-- Lean.Data.PrefixTree
Lean.instEmptyCollectionPrefixTree : {α : Type u_1} → {β : Type u_2} → {p : α → α → Ordering} → EmptyCollection (Lean.PrefixTree α β p)
-- Mathlib.Logic.Equiv.Option
/-- **Alias** of `Equiv.removeNoneAux_none`. -/
Equiv.removeNone_aux_none : ∀ {α : Type u_1} {β : Type u_2} (e : Option α ≃ Option β) {x : α}, e (some x) = none → some (e.removeNoneAux x) = e none
-- Init.Data.SInt.Lemmas
Int32.toISize_ofNat : ∀ {n : ℕ}, n ≤ 2147483647 → (OfNat.ofNat n).toISize = OfNat.ofNat n
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNormEssSup_le_of_ae_nnnorm_bound : ∀ {α : Type u_1} {F : Type u_5} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup F]
  {f : α → F} {C : NNReal}, (∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ C) → MeasureTheory.eLpNormEssSup f μ ≤ ↑C
-- Mathlib.Analysis.Polynomial.MahlerMeasure
Polynomial.logMahlerMeasure.eq_1 : ∀ (p : Polynomial ℂ), p.logMahlerMeasure = Real.circleAverage (fun x => Real.log ‖Polynomial.eval x p‖) 0 1
-- Mathlib.NumberTheory.ModularForms.Petersson
UpperHalfPlane.IsZeroAtImInfty.petersson_isZeroAtImInfty_left : ∀ {F : Type u_1} {F' : Type u_2} [inst : FunLike F UpperHalfPlane ℂ] [inst_1 : FunLike F' UpperHalfPlane ℂ] (k : ℤ)
  (Γ : Subgroup (GL (Fin 2) ℝ)) [Fact (IsCusp OnePoint.infty Γ)] [Γ.HasDetPlusMinusOne] [DiscreteTopology ↥Γ]
  [ModularFormClass F Γ k] [ModularFormClass F' Γ k] {f : F},
  UpperHalfPlane.IsZeroAtImInfty ⇑f → ∀ (f' : F'), UpperHalfPlane.IsZeroAtImInfty (UpperHalfPlane.petersson k ⇑f ⇑f')
-- Mathlib.Data.Vector.Basic
List.Vector.instLawfulTraversableFlipNat : ∀ {n : ℕ}, LawfulTraversable (flip List.Vector n)
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.Approx.Agree.continu : ∀ {F : PFunctor.{uA, uB}} (x : PFunctor.Approx.CofixA F 0) (y : PFunctor.Approx.CofixA F 1), PFunctor.Approx.Agree x y
-- Init.Data.String.Lemmas.Order
String.Pos.slice_le_iff : ∀ {s : String} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {p : (s.slice p₀ p₁ h).Pos} {q : s.Pos} {h₀ : p₀ ≤ q} {h₁ : q ≤ p₁},
  q.slice p₀ p₁ h₀ h₁ ≤ p ↔ q ≤ String.Pos.ofSlice p
-- Mathlib.Algebra.MvPolynomial.Expand
MvPolynomial.coeff_expand_zero : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] (p : ℕ),
  p ≠ 0 → ∀ (φ : MvPolynomial σ R), MvPolynomial.coeff 0 ((MvPolynomial.expand p) φ) = MvPolynomial.coeff 0 φ
-- Mathlib.RingTheory.Adjoin.Polynomial.Basic
Algebra.adjoin_singleton_eq_range_aeval : ∀ (R : Type u) {A : Type z} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (x : A),
  R[x] = (Polynomial.aeval x).range
-- Init.SimpLemmas
Eq.mpr_prop : ∀ {p q : Prop}, p = q → q → p
-- Mathlib.Order.Birkhoff
UpperSet.infIrred_iff_of_finite : ∀ {α : Type u_1} [inst : PartialOrder α] {s : UpperSet α} [Finite α], InfIrred s ↔ ∃ a, UpperSet.Ici a = s
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic
/-- The group cohomology of a `k`-linear `G`-representation `A`, as the cohomology of its complex
of inhomogeneous cochains.  -/
groupCohomology : {k G : Type u} → [inst : CommRing k] → [inst_1 : Group G] → Rep.{u, u, u} k G → ℕ → ModuleCat k
-- Mathlib.Algebra.Lie.Nilpotent
/-- Given a Lie module `M` over a Lie algebra `L` together with an ideal `I` of `L`, this is the
lower central series of `M` as an `I`-module. The advantage of using this definition instead of
`LieModule.lowerCentralSeries R I M` is that its terms are Lie submodules of `M` as an
`L`-module, rather than just as an `I`-module.

See also `LieIdeal.coe_lcs_eq`.  -/
LieIdeal.lcs : {R : Type u_1} →
  {L : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : LieRing L] →
        [inst_2 : LieAlgebra R L] →
          LieIdeal R L →
            (M : Type u_3) →
              [inst_3 : AddCommGroup M] → [inst_4 : Module R M] → [inst_5 : LieRingModule L M] → ℕ → LieSubmodule R L M
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
/-- The canonical linear map `M →ₗ[R] ExteriorAlgebra R M`.
 -/
ExteriorAlgebra.ι : (R : Type u1) →
  [inst : CommRing R] → {M : Type u2} → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → M →ₗ[R] ExteriorAlgebra R M
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.mul_subset_range : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Mul α] [inst_1 : Mul β] [inst_2 : FunLike F α β]
  [MulHomClass F α β] (m : F) {s t : Set β}, s ⊆ Set.range ⇑m → t ⊆ Set.range ⇑m → s * t ⊆ Set.range ⇑m
-- Mathlib.GroupTheory.Submonoid.Inverses
/-- `S.leftNeg` is the additive submonoid containing all the left additive inverses of `S`.  -/
AddSubmonoid.leftNeg : {M : Type u_1} → [inst : AddMonoid M] → AddSubmonoid M → AddSubmonoid M
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.Hom.mk.inj : ∀ {B : Type u} {inst : CategoryTheory.Bicategory B} {a b : B} {l : a ⟶ b} {r : b ⟶ a}
  {adj : CategoryTheory.Bicategory.Adjunction l r} {l_1 : a ⟶ b} {r_1 : b ⟶ a}
  {adj_1 : CategoryTheory.Bicategory.Adjunction l_1 r_1},
  { l := l, r := r, adj := adj } = { l := l_1, r := r_1, adj := adj_1 } → l = l_1 ∧ r = r_1 ∧ adj ≍ adj_1
-- Mathlib.LinearAlgebra.Vandermonde
Matrix.projVandermonde_map : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} {R' : Type u_3} [inst_1 : CommRing R'] (φ : R →+* R') (v w : Fin n → R),
  (Matrix.projVandermonde (fun i => φ (v i)) fun i => φ (w i)) = φ.mapMatrix (Matrix.projVandermonde v w)
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.isoOfEqMk_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B A : C} (X : CategoryTheory.Subobject B) (f : A ⟶ B)
  [inst_1 : CategoryTheory.Mono f] (h : X = CategoryTheory.Subobject.mk f),
  (X.isoOfEqMk f h).inv = CategoryTheory.Subobject.ofMkLE f X ⋯
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.coe_mk : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (g : β → α) (s : Set α) (t : Set β) (ml : ∀ ⦃x : α⦄, x ∈ s → f x ∈ t)
  (mr : ∀ ⦃x : β⦄, x ∈ t → g x ∈ s) (il : ∀ ⦃x : α⦄, x ∈ s → g (f x) = x) (ir : ∀ ⦃x : β⦄, x ∈ t → f (g x) = x),
  ↑{ toFun := f, invFun := g, source := s, target := t, map_source' := ml, map_target' := mr, left_inv' := il,
        right_inv' := ir } =
    f
-- Mathlib.MeasureTheory.Measure.Sub
MeasureTheory.Measure.restrict_sub_eq_restrict_sub_restrict : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {s : Set α},
  MeasurableSet s → (μ - ν).restrict s = μ.restrict s - ν.restrict s
-- Mathlib.Data.Finset.NoncommProd
Finset.noncommProd_singleton : ∀ {α : Type u_3} {β : Type u_4} [inst : Monoid β] (a : α) (f : α → β), {a}.noncommProd f ⋯ = f a
-- Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
CategoryTheory.SimplicialObject.σ_δ₀Iter_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.SimplicialObject C) (i : ℕ) {n m : ℕ}
  (j : Fin (m + 1)) (hi : autoParam (n + (i + 1) = m + 1) CategoryTheory.SimplicialObject.σ_δ₀Iter._auto_1),
  autoParam (↑j ≤ i) CategoryTheory.SimplicialObject.σ_δ₀Iter._auto_3 →
    ∀ {Z : C} (h : X.obj (Opposite.op { len := n }) ⟶ Z),
      CategoryTheory.CategoryStruct.comp (X.σ j) (CategoryTheory.CategoryStruct.comp (X.δ₀Iter (i + 1) hi) h) =
        CategoryTheory.CategoryStruct.comp (X.δ₀Iter i ⋯) h
-- Mathlib.Data.List.Defs
_private.Mathlib.Data.List.Defs.0.List.headI.match_1.splitter : {α : Type u_1} →
  (motive : List α → Sort u_2) →
    (x : List α) → (Unit → motive []) → ((a : α) → (tail : List α) → motive (a :: tail)) → motive x
-- Mathlib.ModelTheory.Equivalence
FirstOrder.Language.Theory.ModelsBoundedFormula.eq_1 : ∀ {L : FirstOrder.Language} (T : L.Theory) {α : Type w} {n : ℕ} (φ : L.BoundedFormula α n),
  T ⊨ᵇ φ = ∀ (M : T.ModelType) (v : α → ↑M) (xs : Fin n → ↑M), φ.Realize v xs
-- Lean.Data.JsonRpc
Lean.IO.FS.Stream.writeNotification : {α : Type u_1} → [Lean.ToJson α] → IO.FS.Stream → Lean.JsonRpc.Notification α → IO Unit
-- Lean.Environment
Lean.Environment.getModuleIdxFor? : Lean.Environment → Lean.Name → Option Lean.ModuleIdx
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (X : C) [grp : CategoryTheory.GrpObj X] (X_1 : C) (grp_1 : CategoryTheory.GrpObj X_1),
  ({ X := X, grp := grp } = { X := X_1, grp := grp_1 }) = (X = X_1 ∧ grp ≍ grp_1)
-- Mathlib.Analysis.Complex.LocallyUniformLimit
/-- If the terms in the sum `∑' (i : ι), F i` are uniformly bounded on `U` by a
summable function, then the sum of `deriv F i` at a point in `U` is the derivative of the
sum.  -/
Complex.hasSum_deriv_of_summable_norm : ∀ {E : Type u_1} {ι : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {U : Set ℂ} {z : ℂ}
  {F : ι → ℂ → E} [CompleteSpace E] {u : ι → ℝ},
  Summable u →
    (∀ (i : ι), DifferentiableOn ℂ (F i) U) →
      IsOpen U →
        (∀ (i : ι), ∀ w ∈ U, ‖F i w‖ ≤ u i) →
          z ∈ U → HasSum (fun i => deriv (F i) z) (deriv (fun w => ∑' (i : ι), F i w) z)
-- Mathlib.LinearAlgebra.Finsupp.Span
Submodule.exists_finset_of_mem_iSup : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Type u_4}
  (p : ι → Submodule R M) {m : M}, m ∈ ⨆ i, p i → ∃ s, m ∈ ⨆ i ∈ s, p i
-- Mathlib.Topology.ContinuousMap.Ideals
ContinuousMap.mem_setOfIdeal : ∀ {X : Type u_1} {R : Type u_2} [inst : TopologicalSpace X] [inst_1 : Semiring R] [inst_2 : TopologicalSpace R]
  [inst_3 : IsTopologicalSemiring R] {I : Ideal C(X, R)} {x : X}, x ∈ ContinuousMap.setOfIdeal I ↔ ∃ f ∈ I, f x ≠ 0
-- Mathlib.Order.Bounds.Basic
/-- If `s` has a least element, then it is bounded below.  -/
IsLeast.bddBelow : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} {a : α}, IsLeast s a → BddBelow s
-- Mathlib.GroupTheory.MonoidLocalization.Finite
/-- The Grothendieck group of a finitely generated monoid is finitely generated.  -/
Algebra.GrothendieckGroup.instFG : ∀ {M : Type u_1} [inst : CommMonoid M] [Monoid.FG M], Monoid.FG (Algebra.GrothendieckGroup M)
-- Lean.Parser.Syntax
Lean.Parser.Command.prefix.formatter : Lean.PrettyPrinter.Formatter
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.minKey?_modify_eq_minKey? : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {k : α} {f : β → β}, (Std.DTreeMap.Const.modify t k f).minKey? = t.minKey?
-- Mathlib.Analysis.InnerProductSpace.l2Space
/-- A Hilbert space admits a Hilbert basis extending a given orthonormal subset.  -/
Orthonormal.exists_hilbertBasis_extension : ∀ {𝕜 : Type u_2} [inst : RCLike 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [CompleteSpace E] {s : Set E}, Orthonormal 𝕜 Subtype.val → ∃ w b, s ⊆ w ∧ ⇑b = Subtype.val
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get?_inter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β}
  [inst_2 : LawfulBEq α], m₁.WF → m₂.WF → ∀ {k : α}, (m₁ ∩ m₂).get? k = if k ∈ m₂ then m₁.get? k else none
-- Mathlib.Order.Heyting.Basic
snd_himp : ∀ {α : Type u_2} {β : Type u_3} [inst : HImp α] [inst_1 : HImp β] (a b : α × β), (a ⇨ b).2 = a.2 ⇨ b.2
-- Mathlib.GroupTheory.Congruence.Hom
AddCon.mkAddHom_apply : ∀ {M : Type u_1} [inst : Add M] (c : AddCon M) (a : M), c.mkAddHom a = ↑a
-- Init.Data.Int.Linear
Int.Internal.Linear.of_var_eq_mul_cert : Int.Internal.Linear.Var → ℤ → Int.Internal.Linear.Var → Int.Internal.Linear.Poly → Bool
-- Mathlib.Condensed.Light.TopCatAdjunction
/-- The adjunction `lightCondSetToTopCat ⊣ topCatToLightCondSet` restricted to sequential
spaces.
 -/
LightCondSet.sequentialAdjunction : LightCondSet.lightCondSetToSequential ⊣ LightCondSet.sequentialToLightCondSet
-- Init.Data.UInt.Lemmas
UInt8.neg_mul : ∀ (a b : UInt8), -a * b = -(a * b)
-- Mathlib.Analysis.SpecialFunctions.Sigmoid
unitInterval.tendsto_sigmoid_atBot : Filter.Tendsto unitInterval.sigmoid Filter.atBot (nhds 0)
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.Iter.length_eq_match_step.match_1.eq_3 : ∀ {α β : Type u_1} (motive : Std.IterStep (Std.Iter β) β → Sort u_2)
  (h_1 : (it' : Std.Iter β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.Iter β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.done with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_3 ()
-- Mathlib.Tactic.Simps.Basic
Simps.ParsedProjectionData.mk.injEq : ∀ (strName : Lean.Name) (strStx : Lean.Syntax) (newName : Lean.Name) (newStx : Lean.Syntax) (isDefault isPrefix : Bool)
  (expr? : Option Lean.Expr) (projNrs : Array ℕ) (isCustom : Bool) (strName_1 : Lean.Name) (strStx_1 : Lean.Syntax)
  (newName_1 : Lean.Name) (newStx_1 : Lean.Syntax) (isDefault_1 isPrefix_1 : Bool) (expr?_1 : Option Lean.Expr)
  (projNrs_1 : Array ℕ) (isCustom_1 : Bool),
  ({ strName := strName, strStx := strStx, newName := newName, newStx := newStx, isDefault := isDefault,
        isPrefix := isPrefix, expr? := expr?, projNrs := projNrs, isCustom := isCustom } =
      { strName := strName_1, strStx := strStx_1, newName := newName_1, newStx := newStx_1, isDefault := isDefault_1,
        isPrefix := isPrefix_1, expr? := expr?_1, projNrs := projNrs_1, isCustom := isCustom_1 }) =
    (strName = strName_1 ∧
      strStx = strStx_1 ∧
        newName = newName_1 ∧
          newStx = newStx_1 ∧
            isDefault = isDefault_1 ∧
              isPrefix = isPrefix_1 ∧ expr? = expr?_1 ∧ projNrs = projNrs_1 ∧ isCustom = isCustom_1)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
WeierstrassCurve.Affine.negY.eq_1 : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Affine R) (x y : R), W'.negY x y = -y - W'.a₁ * x - W'.a₃
-- Init.Data.String.Lemmas.Splits
String.Slice.Pos.Splits.nextn : ∀ {s : String.Slice} {t₁ t₂ : String} {p : s.Pos},
  p.Splits t₁ t₂ →
    ∀ (n : ℕ), (p.nextn n).Splits (t₁ ++ String.ofList (List.take n t₂.toList)) (String.ofList (List.drop n t₂.toList))
-- Lean.MetavarContext
Lean.instInhabitedLevelMetavarDecl.default : Lean.LevelMetavarDecl
-- Mathlib.CategoryTheory.FiberedCategory.Grothendieck
CategoryTheory.Functor.Fiber.inducedFunctor.congr_simp : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  {p : CategoryTheory.Functor 𝒳 𝒮} {S : 𝒮} {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F F_1 : CategoryTheory.Functor C 𝒳} (e_F : F = F_1) (hF : F.comp p = (CategoryTheory.Functor.const C).obj S),
  CategoryTheory.Functor.Fiber.inducedFunctor hF = CategoryTheory.Functor.Fiber.inducedFunctor ⋯
-- Mathlib.Analysis.Complex.Order
Complex.neg_iff : ∀ {z : ℂ}, z < 0 ↔ z.re < 0 ∧ z.im = 0
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get_union_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} (not_mem : k ∉ t₁) {h' : k ∈ t₁ ∪ t₂}, (t₁ ∪ t₂).get k h' = t₂.get k ⋯
-- Mathlib.GroupTheory.OrderOfElement
IsOfFinAddOrder.nsmul : ∀ {G : Type u_1} [inst : AddMonoid G] {a : G} {n : ℕ}, IsOfFinAddOrder a → IsOfFinAddOrder (n • a)
-- Mathlib.Logic.Basic
eq_iff_eq_cancel_left : ∀ {α : Sort u_1} {b c : α}, (∀ {a : α}, a = b ↔ a = c) ↔ b = c
-- Init.Data.Array.Attach
_private.Init.Data.Array.Attach.0.Array.pmapImpl.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {P : α → Prop} (f : (a : α) → P a → β) (xs : Array α) (H : ∀ a ∈ xs, P a),
  Array.pmapImpl f xs H =
    Array.map
      (fun x =>
        match x with
        | ⟨x, h'⟩ => f x h')
      (xs.attachWith P H)
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
/-- The universal property of the free groupoid.  -/
CategoryTheory.FreeGroupoid.strictUniversalPropertyFixedTarget : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {G : Type u₁} →
      [inst_1 : CategoryTheory.Groupoid G] →
        CategoryTheory.Localization.StrictUniversalPropertyFixedTarget (CategoryTheory.FreeGroupoid.of C) ⊤ G
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.HasRightHomology.hasKernel : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [S.HasRightHomology] [inst_3 : CategoryTheory.Limits.HasCokernel S.f],
  CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.desc S.f S.g ⋯)
-- Init.Data.UInt.Lemmas
UInt8.ofNatLT_add : ∀ {a b : ℕ} (hab : a + b < 2 ^ 8), UInt8.ofNatLT (a + b) hab = UInt8.ofNatLT a ⋯ + UInt8.ofNatLT b ⋯
-- Mathlib.Algebra.IsPrimePow
IsPrimePow.ne_zero : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] [IsReduced R] {n : R}, IsPrimePow n → n ≠ 0
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey?_congr : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k k' : α},
  cmp k k' = Ordering.eq → t.getKey? k = t.getKey? k'
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.Answer.mk : Lean.Meta.AbstractMVarsResult → Lean.Expr → ℕ → Lean.Meta.SynthInstance.Answer
-- Aesop.Search.Expansion.Norm
Aesop.NormSeqResult.changed.injEq : ∀ (goal : Lean.MVarId) (script : Array (Aesop.DisplayRuleName × Option (Array Aesop.Script.LazyStep)))
  (goal_1 : Lean.MVarId) (script_1 : Array (Aesop.DisplayRuleName × Option (Array Aesop.Script.LazyStep))),
  (Aesop.NormSeqResult.changed goal script = Aesop.NormSeqResult.changed goal_1 script_1) =
    (goal = goal_1 ∧ script = script_1)
-- Std.Time.Zoned.ZoneRules
Std.Time.TimeZone.instInhabitedUTLocal : Inhabited Std.Time.TimeZone.UTLocal
-- Aesop.Tree.Data
Aesop.instInhabitedNormalizationState : Inhabited Aesop.NormalizationState
-- Mathlib.Data.Set.Prod
Set.univ_pi_ite : ∀ {ι : Type u_1} {α : ι → Type u_2} (s : Set ι) [inst : DecidablePred fun x => x ∈ s] (t : (i : ι) → Set (α i)),
  (Set.univ.pi fun i => if i ∈ s then t i else Set.univ) = s.pi t
-- Mathlib.RingTheory.FiniteType
RingHom.FiniteType.comp : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : CommRing C]
  {g : B →+* C} {f : A →+* B}, g.FiniteType → f.FiniteType → (g.comp f).FiniteType
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
CategoryTheory.Functor.additive_of_iso : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive D] {F : CategoryTheory.Functor C D} [F.Additive] {G : CategoryTheory.Functor C D}
  (e : F ≅ G), G.Additive
-- Mathlib.Data.Nat.Totient
Nat.totient_dvd_of_dvd : ∀ {a b : ℕ}, a ∣ b → a.totient ∣ b.totient
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
/-- note: the version for `ℝ≥0`, `Unitization.nnreal_cfcₙ_eq_cfc_inr`, can be found in
`Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean`  -/
Unitization.real_cfcₙ_eq_cfc_inr : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] (a : A) (f : ℝ → ℝ),
  autoParam (f 0 = 0) Unitization.real_cfcₙ_eq_cfc_inr._auto_1 → ↑(cfcₙ f a) = cfc f ↑a
-- Aesop.Options.Internal
Aesop.Options'.mk : Aesop.Options → Bool → Option ℕ → Aesop.Options'