mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.map₂.eq_1 : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] {t : ι → Type u_11} {t' : ι → Type u_12} [inst_3 : (i : ι) → AddCommMonoid (t i)]
  [inst_4 : (i : ι) → Module R (t i)] [inst_5 : (i : ι) → AddCommMonoid (t' i)] [inst_6 : (i : ι) → Module R (t' i)]
  (f : (i : ι) → s i →ₗ[R] t i →ₗ[R] t' i),
  PiTensorProduct.map₂ f =
    PiTensorProduct.lift (PiTensorProduct.piTensorHomMap.compMultilinearMap ((PiTensorProduct.tprod R).compLinearMap f))
-- Mathlib.Analysis.Calculus.FDeriv.Mul
hasStrictFDerivAt_list_prod_finRange' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {𝔸 : Type u_6} [inst_1 : NormedRing 𝔸] [inst_2 : NormedAlgebra 𝕜 𝔸]
  {n : ℕ} {x : Fin n → 𝔸},
  HasStrictFDerivAt (fun x => (List.map x (List.finRange n)).prod)
    (∑ i,
      (List.map x (List.take (↑i) (List.finRange n))).prod •
        MulOpposite.op (List.map x (List.drop (↑i).succ (List.finRange n))).prod • ContinuousLinearMap.proj i)
    x
-- Mathlib.Algebra.Group.InjSurj
/-- A type endowed with `0`, `+`, unary `-`, and binary `-` is a
`SubNegMonoid` if it admits a surjective map that preserves `0`, `+`, unary `-`, and binary `-` to
a `SubNegMonoid`.  -/
Function.Surjective.subNegMonoid : {M₁ : Type u_1} →
  {M₂ : Type u_2} →
    [inst : Add M₂] →
      [inst_1 : Zero M₂] →
        [inst_2 : SMul ℕ M₂] →
          [inst_3 : Neg M₂] →
            [inst_4 : Sub M₂] →
              [inst_5 : SMul ℤ M₂] →
                [inst_6 : SubNegMonoid M₁] →
                  (f : M₁ → M₂) →
                    Function.Surjective f →
                      f 0 = 0 →
                        (∀ (x y : M₁), f (x + y) = f x + f y) →
                          (∀ (x : M₁), f (-x) = -f x) →
                            (∀ (x y : M₁), f (x - y) = f x - f y) →
                              (∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) →
                                (∀ (x : M₁) (n : ℤ), f (n • x) = n • f x) → SubNegMonoid M₂
-- Mathlib.Algebra.Category.Grp.Basic
CommGrpCat.Hom.Simps.hom.eq_1 : ∀ (X Y : CommGrpCat) (f : X.Hom Y), CommGrpCat.Hom.Simps.hom X Y f = f.hom
-- Mathlib.Analysis.Normed.MulAction
edist_smul₀ : ∀ {α : Type u_1} {β : Type u_2} [inst : SeminormedRing α] [inst_1 : SeminormedAddCommGroup β] [inst_2 : Module α β]
  [NormSMulClass α β] (s : α) (x y : β), edist (s • x) (s • y) = ‖s‖₊ • edist x y
-- Mathlib.Data.Nat.BitIndices
/-- Together with `Nat.sum_map_bitIndices_two_pow`, this implies a bijection between `ℕ` and `Finset ℕ`.
See `Finset.equivBitIndices` for this bijection.
 -/
Nat.bitIndices_sum_map_two_pow : ∀ {L : List ℕ}, L.SortedLT → (List.map (fun i => 2 ^ i) L).sum.bitIndices = L
-- Mathlib.Order.SupClosed
finsetSup'_mem_supClosure : ∀ {α : Type u_3} [inst : SemilatticeSup α] {s : Set α} {ι : Type u_5} {t : Finset ι} (ht : t.Nonempty) {f : ι → α},
  (∀ i ∈ t, f i ∈ s) → t.sup' ht f ∈ supClosure s
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.coeff_eq_zero : ∀ {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {x : PolynomialModule R M}, x.coeff = 0 ↔ x = 0
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.zeroLocus_empty_iff_eq_top : ∀ {R : Type u} [inst : CommSemiring R] {I : Ideal R}, PrimeSpectrum.zeroLocus ↑I = ∅ ↔ I = ⊤
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceInverse_obj_right_as : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T)
  (G : CategoryTheory.Functor D T) (c : C) (Y : CategoryTheory.Comma ((CategoryTheory.Over.forget c).comp F) G),
  ((CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceInverse F G c).obj Y).right.as = PUnit.unit
-- Mathlib.Tactic.Linarith.Datatypes
Mathlib.Tactic.Linarith.PreprocessorBase.mk.sizeOf_spec : ∀ (name : autoParam Lean.Name Mathlib.Tactic.Linarith.PreprocessorBase.name._autoParam) (description : String),
  sizeOf { name := name, description := description } = 1 + sizeOf name + sizeOf description
-- Mathlib.CategoryTheory.Sites.Point.Category
/-- The natural transformation on fibers of presheaves that is induced
by a morphism of points of a site.  -/
CategoryTheory.GrothendieckTopology.Point.Hom.presheafFiber : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {A : Type u'} →
        [inst_1 : CategoryTheory.Category.{v', u'} A] →
          [inst_2 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] →
            {Φ₁ Φ₂ : J.Point} → (Φ₁ ⟶ Φ₂) → (Φ₂.presheafFiber ⟶ Φ₁.presheafFiber)
-- Mathlib.MeasureTheory.OuterMeasure.Basic
/-- **Alias** of the reverse direction of `MeasureTheory.measure_iUnion_null_iff`. -/
MeasureTheory.measure_iUnion_null : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F}
  {ι : Sort u_4} [Countable ι] {s : ι → Set α}, (∀ (i : ι), μ (s i) = 0) → μ (⋃ i, s i) = 0
-- Mathlib.Algebra.Homology.Factorizations.CM5b
/-- Given a cochain complex `K`, this is a cochain complex `I K` with
zero differentials which in degree `n` consists of the injective
object `Injective.under (K.X n)`.  -/
CochainComplex.cm5b.I : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] → [CategoryTheory.EnoughInjectives C] → CochainComplex C ℤ → CochainComplex C ℤ
-- Mathlib.Analysis.InnerProductSpace.LinearPMap
/-- Restricting `A` to a dense submodule and taking the `LinearPMap.adjoint` is the same
as taking the `ContinuousLinearMap.adjoint` interpreted as a `LinearPMap`.  -/
ContinuousLinearMap.toPMap_adjoint_eq_adjoint_toPMap_of_dense : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : CompleteSpace E] [inst_6 : CompleteSpace F] (A : E →L[𝕜] F) {p : Submodule 𝕜 E},
  Dense ↑p → ((↑A).toPMap p).adjoint = (↑(ContinuousLinearMap.adjoint A)).toPMap ⊤
-- Mathlib.Geometry.Manifold.Diffeomorph
/-- Infinitely differentiable diffeomorphism between `E` and `E'`.  -/
Manifold.«term_≃ₘ[_]_» : Lean.TrailingParserDescr
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get!_inter_of_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [inst_2 : Inhabited α] [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∈ m₂ → (m₁ ∩ m₂).get! k = m₁.get! k
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.ExSum.brecOn.go : {u : Lean.Level} →
  {α : Q(Type u)} →
    {BaseType : Q(«$α») → Type} →
      {sα : Q(CommSemiring «$α»)} →
        {motive_1 : (e : Q(«$α»)) → Mathlib.Tactic.Ring.Common.ExBase BaseType sα e → Sort u} →
          {motive_2 : (e : Q(«$α»)) → Mathlib.Tactic.Ring.Common.ExProd BaseType sα e → Sort u} →
            {motive_3 : (e : Q(«$α»)) → Mathlib.Tactic.Ring.Common.ExSum BaseType sα e → Sort u} →
              {e : Q(«$α»)} →
                (t : Mathlib.Tactic.Ring.Common.ExSum BaseType sα e) →
                  ((e : Q(«$α»)) → (t : Mathlib.Tactic.Ring.Common.ExBase BaseType sα e) → t.below → motive_1 e t) →
                    ((e : Q(«$α»)) → (t : Mathlib.Tactic.Ring.Common.ExProd BaseType sα e) → t.below → motive_2 e t) →
                      ((e : Q(«$α»)) → (t : Mathlib.Tactic.Ring.Common.ExSum BaseType sα e) → t.below → motive_3 e t) →
                        motive_3 e t ×' t.below
-- Mathlib.Combinatorics.Hypergraph.Basic
Hypergraph.mem_completeOn : ∀ {α : Type u_1} {e f : Set α}, e ∈ (Hypergraph.completeOn f).edgeSet ↔ e ⊆ f
-- Init.Data.Vector.Lemmas
Vector.getElem_pop : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ} (h : i < n - 1), xs.pop[i] = xs[i]
-- Mathlib.Topology.Algebra.Group.Matrix
/-- The special linear group over a topological ring is a topological group.  -/
Matrix.SpecialLinearGroup.topologicalGroup : ∀ {n : Type u_1} {R : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R]
  [inst_3 : TopologicalSpace R] [IsTopologicalRing R], IsTopologicalGroup (Matrix.SpecialLinearGroup n R)
-- Mathlib.SetTheory.ZFC.Class
/-- Unlike the other set constructors, the `iota` definite descriptor
is a set for any set input, but not constructively so, so there is no
associated `Class → Set` function.  -/
Class.iota_ex : ∀ (A : Class.{u}), A.iota ∈ Class.univ
-- Mathlib.Algebra.Star.Subsemiring
/-- The center of magma `A` is the set of elements that commute and associate
with everything in `A`, here realized as a `SubStarSemigroup`.  -/
SubStarSemigroup.center : (A : Type u_1) → [inst : Mul A] → [inst_1 : StarMul A] → SubStarSemigroup A
-- Lean.Meta.MethodSpecs
Lean.MethodSpecsAttrData : Type
-- Mathlib.Analysis.InnerProductSpace.TwoDim
Orientation.kahler_mul : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o : Orientation ℝ E (Fin 2)) (a x y : E), (o.kahler x) a * (o.kahler a) y = ↑‖a‖ ^ 2 * (o.kahler x) y
-- Mathlib.Topology.Connected.PathConnected
IsPathConnected.eq_1 : ∀ {X : Type u_1} [inst : TopologicalSpace X] (F : Set X), IsPathConnected F = ∃ x ∈ F, ∀ ⦃y : X⦄, y ∈ F → JoinedIn F x y
-- Batteries.Data.Array.Scan
Array.scanrM_eq_scanrM_toList : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {init : β} [inst : Monad m] [LawfulMonad m] {f : α → β → m β}
  {as : Array α}, Array.scanrM f init as = List.toArray <$> List.scanrM f init as.toList
-- Mathlib.Order.SuccPred.Basic
Order.Ioc_subset_Ioo_succ_right_of_not_isMax : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] {a b : α}, ¬IsMax b → Set.Ioc a b ⊆ Set.Ioo a (Order.succ b)
-- Mathlib.RingTheory.TensorProduct.Basic
Algebra.TensorProduct.instOneTensorProduct : {R : Type uR} →
  {A : Type uA} →
    {B : Type uB} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoidWithOne A] →
          [inst_2 : Module R A] → [inst_3 : AddCommMonoidWithOne B] → [inst_4 : Module R B] → One (TensorProduct R A B)
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- The `bound` tactic can't handle `m ≠ 0` goals yet, so we express as `0 < m`  -/
Bound.le_self_pow_of_pos : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : Preorder M₀] {a : M₀} {n : ℕ} [ZeroLEOneClass M₀]
  [PosMulMono M₀], 1 ≤ a → 0 < n → a ≤ a ^ n
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.instStarRing : {d : ℤ} → StarRing (ℤ√d)
-- Mathlib.Algebra.DirectSum.Ring
DirectSum.GSemiring.mk : {ι : Type u_1} →
  {A : ι → Type u_2} →
    [inst : AddMonoid ι] →
      [inst_1 : (i : ι) → AddCommMonoid (A i)] →
        [toGNonUnitalNonAssocSemiring : DirectSum.GNonUnitalNonAssocSemiring A] →
          [toGOne : GradedMonoid.GOne A] →
            (∀ (a : GradedMonoid A), 1 * a = a) →
              (∀ (a : GradedMonoid A), a * 1 = a) →
                (∀ (a b c : GradedMonoid A), a * b * c = a * (b * c)) →
                  (gnpow : (n : ℕ) → {i : ι} → A i → A (n • i)) →
                    autoParam (∀ (a : GradedMonoid A), GradedMonoid.mk (0 • a.fst) (gnpow 0 a.snd) = 1)
                        GradedMonoid.GMonoid.gnpow_zero'._autoParam →
                      autoParam
                          (∀ (n : ℕ) (a : GradedMonoid A),
                            GradedMonoid.mk (n.succ • a.fst) (gnpow n.succ a.snd) = ⟨n • a.fst, gnpow n a.snd⟩ * a)
                          GradedMonoid.GMonoid.gnpow_succ'._autoParam →
                        (natCast : ℕ → A 0) →
                          natCast 0 = 0 →
                            (∀ (n : ℕ), natCast (n + 1) = natCast n + GradedMonoid.GOne.one) → DirectSum.GSemiring A
-- Mathlib.SetTheory.Ordinal.Veblen
/-- The epsilon function enumerates the fixed points of `ω ^ ⬝`.
This is an abbreviation for `veblen 1`. 

Conventions for notations in identifiers:

 * The recommended spelling of `ε_ ` in identifiers is `epsilon`. -/
Ordinal.epsilon : Ordinal.{u_1} → Ordinal.{u_1}
-- Mathlib.Analysis.SpecialFunctions.Gamma.Deriv
Complex.not_continuousAt_Gamma_zero : ¬ContinuousAt Complex.Gamma 0
-- Mathlib.Topology.MetricSpace.Isometry
Isometry.preimage_eball : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β},
  Isometry f → ∀ (x : α) (r : ENNReal), f ⁻¹' Metric.eball (f x) r = Metric.eball x r
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
ModularGroup.coe.eq_1 : ∀ (g : Matrix.SpecialLinearGroup (Fin 2) ℤ),
  ModularGroup.coe g = Matrix.SpecialLinearGroup.toGLPos ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) g)
-- Lean.Meta.Basic
Lean.Meta.resetSynthInstanceCache : Lean.MetaM Unit
-- Mathlib.Order.RelClasses
/-- Set notation form of `lt_irrefl` -/
ssubset_irrefl : ∀ {α : Type u_1} [UsesSetNotationForOrder α] [inst : Preorder α] (a : α), ¬a ⊂ a
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
/-- The `i`th opcycles functor `HomologicalComplex C c ⥤ C`.  -/
HomologicalComplex.opcyclesFunctor : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {ι : Type u_2} →
        (c : ComplexShape ι) →
          ι → [CategoryTheory.CategoryWithHomology C] → CategoryTheory.Functor (HomologicalComplex C c) C
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getKey_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List (α × β)} {k : α} (contains_eq_false : (List.map Prod.fst l).contains k = false)
  {h : k ∈ Std.ExtDHashMap.Const.insertMany m l}, (Std.ExtDHashMap.Const.insertMany m l).getKey k h = m.getKey k ⋯
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- The natural isomorphism `(homologyFunctor C).op ≅ opFunctor C ⋙ homologyFunctor Cᵒᵖ`
which relates the homology in `C` and in `Cᵒᵖ`.  -/
CategoryTheory.ShortComplex.homologyFunctorOpNatIso : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      [inst_2 : CategoryTheory.CategoryWithHomology C] →
        (CategoryTheory.ShortComplex.homologyFunctor C).op ≅
          (CategoryTheory.ShortComplex.opFunctor C).comp (CategoryTheory.ShortComplex.homologyFunctor Cᵒᵖ)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.isSome_get?_eq_contains : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α],
  m.WF → ∀ {a : α}, (m.get? a).isSome = m.contains a
-- Mathlib.CategoryTheory.Monoidal.Internal.Module
ModuleCat.MonModuleEquivalenceAlgebra.algebraMap : ∀ {R : Type u} [inst : CommRing R] (A : ModuleCat R) [inst_1 : CategoryTheory.MonObj A] (r : R),
  (algebraMap R ↑A) r = (CategoryTheory.ConcreteCategory.hom CategoryTheory.MonObj.one) r
-- Init.Data.Int.Linear
Int.Internal.Linear.diseq_eq_subst_cert.eq_1 : ∀ (x : Int.Internal.Linear.Var) (p₁ p₂ p₃ : Int.Internal.Linear.Poly),
  Int.Internal.Linear.diseq_eq_subst_cert x p₁ p₂ p₃ =
    (!(p₁.coeff x).beq' 0).and' (p₃.beq' (Int.Internal.Linear.Poly.combine_mul_k (p₂.coeff x) (-p₁.coeff x) p₁ p₂))
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
CategoryTheory.Functor.lan.eq_1 : ∀ {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] (L : CategoryTheory.Functor C D) {H : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} H]
  [inst_3 : ∀ (F : CategoryTheory.Functor C H), L.HasLeftKanExtension F],
  L.lan =
    { obj := fun F => L.leftKanExtension F,
      map := fun {F₁ F₂} φ =>
        (L.leftKanExtension F₁).descOfIsLeftKanExtension (L.leftKanExtensionUnit F₁) (L.leftKanExtension F₂)
          (CategoryTheory.CategoryStruct.comp φ (L.leftKanExtensionUnit F₂)),
      map_id := ⋯, map_comp := ⋯ }
-- Mathlib.AlgebraicGeometry.PullbackCarrier
AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr_inv : ∀ {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} {x y : AlgebraicGeometry.Scheme.Pullback.Triplet f g}
  (e : x = y),
  (AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr e).inv =
    (AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr ⋯).hom
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.Stream.toList_cons : ∀ {α : Type u_1} {x : α} {r : RBTree.RBNode α} {s : RBTree.RBNode.Stream α},
  (RBTree.RBNode.Stream.cons x r s).toList = x :: r.toList ++ s.toList
-- Mathlib.Analysis.CStarAlgebra.Module.Constructions
WithCStarModule.instNormProd : {A : Type u_1} →
  [inst : NonUnitalCStarAlgebra A] →
    [inst_1 : PartialOrder A] →
      {E : Type u_2} →
        {F : Type u_3} →
          [inst_2 : NormedAddCommGroup E] →
            [inst_3 : Module ℂ E] →
              [inst_4 : SMul A E] →
                [inst_5 : NormedAddCommGroup F] →
                  [inst_6 : Module ℂ F] →
                    [inst_7 : SMul A F] → [CStarModule A E] → [CStarModule A F] → Norm (WithCStarModule A (E × F))
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
cbiSup_eq_of_not_forall : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLinearOrder α] {p : ι → Prop} {f : Subtype p → α},
  (¬∀ (i : ι), p i) → ⨆ i, ⨆ (h : p i), f ⟨i, h⟩ = max (iSup f) (sSup ∅)
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Iter.forIn'_eq_match_step.match_3.eq_3 : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] {it : Std.Iter β} (motive : it.Step → Sort u_2)
  (property : it.IsPlausibleStep Std.IterStep.done)
  (h_1 :
    (it' : Std.Iter β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.Iter β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (property : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩),
  (match ⟨Std.IterStep.done, property⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, property⟩ => h_3 property) =
    h_3 property
-- Mathlib.Tactic.Linarith.Datatypes
Mathlib.Tactic.Linarith.Comp.mk.sizeOf_spec : ∀ (str : Mathlib.Ineq) (coeffs : Mathlib.Tactic.Linarith.Linexp),
  sizeOf { str := str, coeffs := coeffs } = 1 + sizeOf str + sizeOf coeffs
-- Mathlib.Analysis.Normed.Module.MStructure
IsLprojection.Subtype.sdiff : {X : Type u_1} →
  [inst : NormedAddCommGroup X] →
    {M : Type u_2} → [inst_1 : Ring M] → [inst_2 : Module M X] → [FaithfulSMul M X] → SDiff { P // IsLprojection X P }
-- Batteries.Data.Array.Scan
Array.idRun_scanrM : ∀ {α : Type u_1} {β : Type u_2} {init : β} {f : α → β → Id β} {as : Array α},
  (Array.scanrM f init as).run = Array.scanr (fun x1 x2 => (f x1 x2).run) init as
-- Mathlib.Algebra.Lie.SerreConstruction
/-- The Lie algebra of type Bₙ, isomorphic to so(2n+1).  -/
CartanMatrix.bₙ : (R : Type u_1) → [CommRing R] → ℕ → Type u_1
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get?_union : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  {k : α}, Std.DTreeMap.Const.get? (t₁ ∪ t₂) k = (Std.DTreeMap.Const.get? t₂ k).or (Std.DTreeMap.Const.get? t₁ k)
-- Mathlib.SetTheory.Descriptive.Tree
Descriptive.Tree.mem_pullSub_short : ∀ {A : Type u_1} {T : ↥(Descriptive.tree A)} {x y : List A},
  y.length ≤ x.length → (y ∈ Descriptive.Tree.pullSub T x ↔ y <+: x ∧ [] ∈ T)
-- Mathlib.RingTheory.DedekindDomain.Ideal.Basic
FractionRing.algEquiv.congr_simp : ∀ (A : Type u_4) [inst : CommRing A] (K : Type u_6) [inst_1 : CommRing K] [inst_2 : Algebra A K]
  [inst_3 : IsFractionRing A K], FractionRing.algEquiv A K = FractionRing.algEquiv A K
-- Mathlib.Data.Sym.Sym2
/-- A two-argument version of `Sym2.lift`.  -/
Sym2.lift₂ : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} →
      { f // ∀ (a₁ a₂ : α) (b₁ b₂ : β), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁ } ≃
        (Sym2 α → Sym2 β → γ)
-- Std.Tactic.BVDecide.LRAT.Internal.LRATCheckerSound
Std.Tactic.BVDecide.LRAT.Internal.WellFormedAction.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : Std.Tactic.BVDecide.LRAT.Internal.Clause α β] (id : ℕ) (c : β)
  (p : Std.Sat.Literal α) (rupHints : Array ℕ) (ratHints : Array (ℕ × Array ℕ)),
  Std.Tactic.BVDecide.LRAT.Internal.WellFormedAction (Std.Tactic.BVDecide.LRAT.Action.addRat id c p rupHints ratHints) =
    Std.Tactic.BVDecide.LRAT.Internal.Limplies α p c
-- Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
CategoryTheory.Functor.preservesFiniteColimits_iff_forall_exact_map_and_epi : ∀ {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.Abelian C]
  [inst_3 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [inst_4 : F.Additive],
  CategoryTheory.Limits.PreservesFiniteColimits F ↔
    ∀ (S : CategoryTheory.ShortComplex C), S.ShortExact → (S.map F).Exact ∧ CategoryTheory.Epi (F.map S.g)
-- Mathlib.Topology.Algebra.InfiniteSum.Order
summable_abs_iff : ∀ {ι : Type u_1} {α : Type u_3} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α]
  [inst_3 : UniformSpace α] [IsUniformAddGroup α] [CompleteSpace α] {f : ι → α}, (Summable fun x => |f x|) ↔ Summable f
-- Mathlib.Topology.Algebra.InfiniteSum.Group
/-- Product divergence test: if `f` is unconditionally multipliable, then `f x` tends to one along
`cofinite`.  -/
Multipliable.tendsto_cofinite_one : ∀ {α : Type u_1} {G : Type u_4} [inst : TopologicalSpace G] [inst_1 : CommGroup G] [IsTopologicalGroup G] {f : α → G},
  Multipliable f → Filter.Tendsto f Filter.cofinite (nhds 1)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Right.nsmul_neg_iff : ∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : LinearOrder M] [AddRightStrictMono M] {n : ℕ} {x : M},
  0 < n → (n • x < 0 ↔ x < 0)
-- Mathlib.Order.Types.Defs
OrderType.type_toType : ∀ (o : OrderType.{u_1}), OrderType.type o.ToType = o
-- Aesop.Search.SearchM
Aesop.setTree : {Q : Type} → [inst : Aesop.Queue Q] → Aesop.Tree → Aesop.SearchM Q Unit
-- Init.Data.Range.Polymorphic.UInt
UInt16.succMany?_ofBitVec : ∀ {k : ℕ} {x : BitVec 16}, Std.PRange.succMany? k { toBitVec := x } = UInt16.ofBitVec <$> Std.PRange.succMany? k x
-- Init.Data.Array.OfFn
_private.Init.Data.Array.OfFn.0.Array.ofFn.go.eq_def : ∀ {α : Type u} {n : ℕ} (f : Fin n → α) (acc : Array α) (i : ℕ) (a : i ≤ n),
  Array.ofFn.go✝ f acc i a =
    match i, a with
    | i.succ, h =>
      have w := ⋯;
      Array.ofFn.go✝ f (acc.push (f ⟨n - i - 1, w⟩)) i ⋯
    | 0, x => acc
-- Lean.Meta.DecLevel
_private.Lean.Meta.DecLevel.0.Lean.Meta.decAux? : Lean.Level → ReaderT Lean.Meta.DecLevelContext Lean.MetaM (Option Lean.Level)
-- Mathlib.Data.List.Pairwise
List.Pairwise.rel_get_of_le : ∀ {α : Type u_1} {R : α → α → Prop} [Std.Refl R] {l : List α},
  List.Pairwise R l → ∀ {a b : Fin l.length}, a ≤ b → R (l.get a) (l.get b)
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.isSeparator_iff_epi : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (G : C)
  [inst_1 : ∀ (A : C), CategoryTheory.Limits.HasCoproduct fun x => G],
  CategoryTheory.IsSeparator G ↔ ∀ (A : C), CategoryTheory.Epi (CategoryTheory.Limits.Sigma.desc fun f => f)
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ico_filter_le_of_left_le : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {a b c : α}
  [inst_2 : DecidablePred fun x => c ≤ x], a ≤ c → {x ∈ Finset.Ico a b | c ≤ x} = Finset.Ico c b
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getKey!_ofList_of_contains_eq_false : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] [inst_4 : Inhabited α]
  {l : List (α × β)} {k : α},
  (List.map Prod.fst l).contains k = false → (Std.DHashMap.Raw.Const.ofList l).getKey! k = default