mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.exact_iff_kernel_ι_comp_cokernel_π_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [S.HasHomology] [inst_3 : CategoryTheory.Limits.HasKernel S.g]
  [inst_4 : CategoryTheory.Limits.HasCokernel S.f],
  S.Exact ↔
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι S.g) (CategoryTheory.Limits.cokernel.π S.f) = 0
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.constantCoeff_C : ∀ {R : Type u_1} [inst : Semiring R] (a : R), PowerSeries.constantCoeff (PowerSeries.C a) = a
-- Mathlib.Order.Filter.Prod
Filter.principal_coprod_principal : ∀ {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β),
  (Filter.principal s).coprod (Filter.principal t) = Filter.principal (sᶜ ×ˢ tᶜ)ᶜ
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.YonedaCollection.mk_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)}
  {F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} {X : C}
  (s : CategoryTheory.yoneda.obj X ⟶ A) (x : F.obj (Opposite.op (CategoryTheory.CostructuredArrow.mk s))),
  (CategoryTheory.OverPresheafAux.YonedaCollection.mk s x).snd =
    (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.eqToHom ⋯))) x
-- Mathlib.Data.NNReal.Defs
/-- **Alias** of the reverse direction of `NNReal.coe_lt_coe`. -/
_private.Mathlib.Data.NNReal.Defs.0.NNReal.Bound.coe_lt_coe_of_lt : ∀ {r₁ r₂ : NNReal}, r₁ < r₂ → ↑r₁ < ↑r₂
-- Mathlib.Data.EReal.Basic
EReal.coe_natCast : ∀ {n : ℕ}, ↑↑n = ↑n
-- Mathlib.Order.Filter.Prod
Filter.Tendsto.coprod_of_prod_top_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α × β → γ} {la : Filter α} {lb : Filter β} {lc : Filter γ},
  (∀ s ∈ lb, Filter.Tendsto f (la ×ˢ Filter.principal sᶜ) lc) →
    Filter.Tendsto f (⊤ ×ˢ lb) lc → Filter.Tendsto f (la.coprod lb) lc
-- Lean.DocString.Formatter
_private.Lean.DocString.Formatter.0.Lean.Doc.Parser.atomString : Lean.Syntax → String
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.iSup_eq_lsub : ∀ {ι : Type u_3} (f : ι → Ordinal.{max u_4 u_3}), iSup (Order.succ ∘ f) = Ordinal.lsub f
-- Init.Data.Bool
Bool.decide_coe : ∀ (b : Bool) [inst : Decidable (b = true)], decide (b = true) = b
-- Mathlib.RingTheory.Finiteness.Basic
Submodule.FG.stabilizes_of_iSup_eq : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {M' : Submodule R M}, M'.FG → ∀ (N : ℕ →o Submodule R M), iSup ⇑N = M' → ∃ n, M' = N n
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.map_iSup : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [inst_2 : FunLike F M N]
  [mc : MonoidHomClass F M N] {ι : Sort u_5} (f : F) (s : ι → Submonoid M),
  Submonoid.map f (iSup s) = ⨆ i, Submonoid.map f (s i)
-- Mathlib.Data.List.Sort
/-- **Alias** of the reverse direction of `List.sortedLT_iff_getElem_lt_getElem_of_lt`. -/
List.sortedLT_of_getElem_lt_getElem_of_lt : ∀ {α : Type u_1} {l : List α} [inst : Preorder α],
  (∀ ⦃i j : ℕ⦄ ⦃hi : i < l.length⦄ ⦃hj : j < l.length⦄, i < j → l[i] < l[j]) → l.SortedLT
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.incl_range : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (K : LieSubalgebra R L),
  K.incl.range = K
-- Mathlib.Data.Seq.Computation
Computation.think_empty : ∀ {α : Type u}, Computation.empty α = (Computation.empty α).think
-- Mathlib.Analysis.Normed.Algebra.MatrixExponential
Matrix.exp_conj' : ∀ {m : Type u_1} {𝔸 : Type u_5} [inst : Fintype m] [inst_1 : DecidableEq m] [inst_2 : NormedCommRing 𝔸]
  [NormedAlgebra ℚ 𝔸] [CompleteSpace 𝔸] (U A : Matrix m m 𝔸),
  IsUnit U → NormedSpace.exp (U⁻¹ * A * U) = U⁻¹ * NormedSpace.exp A * U
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instSMulCommClass : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] {K : Type u_5} [inst_1 : SMul γ β]
  [inst_2 : SMul K β] [SMulCommClass K γ β], SMulCommClass K γ (MeasureTheory.SimpleFunc α β)
-- Std.Http.Protocol.H1.Reader
Std.Http.Protocol.H1.Reader.instReprState.repr : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Reader.State dir → ℕ → Std.Format
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.coe_inj : ∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂]
  {f g : NormedAddGroupHom V₁ V₂}, ⇑f = ⇑g → f = g
-- Mathlib.Algebra.GCDMonoid.Multiset
Multiset.gcd_dedup : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] [inst_2 : DecidableEq α]
  (s : Multiset α), s.dedup.gcd = s.gcd
-- Mathlib.Algebra.Group.Basic
neg_add' : ∀ {α : Type u_1} [inst : SubtractionCommMonoid α] (a b : α), -(a + b) = -a - b
-- Batteries.Tactic.PrintPrefix
_private.Batteries.Tactic.PrintPrefix.0.Batteries.Tactic.elabPrintPrefixConfig.evalConfigItem : Lean.Elab.ConfigEval.EvalConfigItem Batteries.Tactic.PrintPrefixConfig
-- Mathlib.Logic.Embedding.Basic
Equiv.toEmbedding_apply : ∀ {α : Sort u} {β : Sort v} (f : α ≃ β) (a : α), f.toEmbedding a = f a
-- Lean.Meta.Diagnostics
Lean.Meta.DiagSummary.mk.inj : ∀ {data : Array Lean.MessageData} {max : ℕ} {data_1 : Array Lean.MessageData} {max_1 : ℕ},
  { data := data, max := max } = { data := data_1, max := max_1 } → data = data_1 ∧ max = max_1
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
/-- Pushforwards along equal morphisms are isomorphic.  -/
AlgebraicGeometry.Scheme.Modules.pushforwardCongr : {X Y : AlgebraicGeometry.Scheme} →
  {f g : X ⟶ Y} →
    f = g → (AlgebraicGeometry.Scheme.Modules.pushforward f ≅ AlgebraicGeometry.Scheme.Modules.pushforward g)
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.isCentralVAdd : ∀ {S : Type u'} {R : Type u} {M : Type v} [inst : AddMonoid R] [inst_1 : AddAction R M] [inst_2 : VAdd S R]
  [inst_3 : VAdd S M] [inst_4 : VAddAssocClass S R M] (p : SubAddAction R M) [inst_5 : VAdd Sᵃᵒᵖ R]
  [inst_6 : VAdd Sᵃᵒᵖ M] [inst_7 : VAddAssocClass Sᵃᵒᵖ R M] [IsCentralVAdd S M], IsCentralVAdd S ↥p
-- Mathlib.Logic.Equiv.Basic
Function.Injective.swap_comp : ∀ {α : Sort u_1} {β : Sort u_4} [inst : DecidableEq α] [inst_1 : DecidableEq β] {f : α → β},
  Function.Injective f → ∀ (x y : α), ⇑(Equiv.swap (f x) (f y)) ∘ f = f ∘ ⇑(Equiv.swap x y)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.llcomp_apply : ∀ (R : Type u_1) (U : Type u_2) (V : Type u_3) (W : Type u_4) [inst : CommSemiring R] [inst_1 : AddCommMonoid U]
  [inst_2 : Module R U] [inst_3 : TopologicalSpace U] [inst_4 : AddCommMonoid V] [inst_5 : Module R V]
  [inst_6 : TopologicalSpace V] [inst_7 : ContinuousAdd V] [inst_8 : ContinuousConstSMul R V] [inst_9 : AddCommMonoid W]
  [inst_10 : Module R W] [inst_11 : TopologicalSpace W] [inst_12 : ContinuousAdd W] [inst_13 : ContinuousConstSMul R W]
  (l : U →L[R] V), (ContinuousLinearMap.llcomp R U V W) l = ContinuousLinearMap.lcomp W l
-- Mathlib.Order.Lattice
inf_le_of_right_le : ∀ {α : Type u} [inst : SemilatticeInf α] {a b c : α}, b ≤ c → a ⊓ b ≤ c
-- Mathlib.Data.ZMod.Basic
ZMod.instInv : (n : ℕ) → Inv (ZMod n)
-- Mathlib.Topology.PartitionOfUnity
/-- A `BumpCovering ι X s` is an indexed family of functions `f i`, `i : ι`, such that

* the supports of `f i` form a locally finite family of sets, i.e., for every point `x : X` there
  exists a neighborhood `U ∋ x` such that all but finitely many functions `f i` are zero on `U`;
* for all `i`, `x` we have `0 ≤ f i x ≤ 1`;
* each point `x ∈ s` belongs to the interior of `{x | f i x = 1}` for some `i`.

One of the main use cases for a `BumpCovering` is to define a `PartitionOfUnity`, see
`BumpCovering.toPartitionOfUnity`, but some proofs can directly use a `BumpCovering` instead of
a `PartitionOfUnity`.

If `X` is a normal paracompact space, then `BumpCovering.exists_isSubordinate` guarantees that for
every open covering `U : Set (Set X)` of `s` there exists a `BumpCovering` of `s` that is
subordinate to `U`.
 -/
BumpCovering : Type u_1 → (X : Type u_2) → [TopologicalSpace X] → optParam (Set X) Set.univ → Type (max u_1 u_2)
-- Mathlib.Probability.Independence.Integration
/-- The product of two independent and integrable random variables is integrable.  -/
ProbabilityTheory.IndepFun.integrable_mul : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {E : Type u_5} [inst : TopologicalSpace E]
  [inst_1 : ContinuousENorm E] [inst_2 : Mul E] [ContinuousMul E] [ENormSMulClass E E] [inst_5 : MeasurableSpace E]
  [OpensMeasurableSpace E] {X Y : Ω → E},
  ProbabilityTheory.IndepFun X Y μ →
    MeasureTheory.Integrable X μ → MeasureTheory.Integrable Y μ → MeasureTheory.Integrable (X * Y) μ
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.isNonloop_of_notMem_closure : ∀ {α : Type u_1} {M : Matroid α} {e : α} {X : Set α},
  e ∉ M.closure X → autoParam (e ∈ M.E) Matroid.isNonloop_of_notMem_closure._auto_1 → M.IsNonloop e
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.Option.dmap.match_1.splitter : {α : Type u_1} →
  {β : Type u_3} →
    (motive : (x : Option α) → ((a : α) → x = some a → β) → Sort u_2) →
      (x : Option α) →
        (x_1 : (a : α) → x = some a → β) →
          ((x : (a : α) → none = some a → β) → motive none x) →
            ((a : α) → (f : (a_1 : α) → some a = some a_1 → β) → motive (some a) f) → motive x x_1
-- Aesop.RuleTac.Forward
Aesop.RuleTac.forwardExpr : Lean.Expr → Aesop.UnorderedArraySet Aesop.PremiseIndex → Bool → Aesop.RuleTac
-- Std.Data.DHashMap.Basic
/-- Tries to retrieve the mapping for the given key, returning `fallback` if no such mapping is present.

Uses the `LawfulBEq` instance to cast the retrieved value to the correct type.
 -/
Std.DHashMap.getD : {α : Type u} →
  {β : α → Type v} → {x : BEq α} → {x_1 : Hashable α} → [LawfulBEq α] → Std.DHashMap α β → (a : α) → β a → β a
-- Mathlib.NumberTheory.FactorisationProperties
/-- Any natural number power of a prime is deficient  -/
Nat.Prime.deficient_pow : ∀ {n m : ℕ}, Nat.Prime n → (n ^ m).Deficient
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.toAlgEquiv_injective : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A]
  [inst_6 : Algebra R B], Function.Injective ContinuousAlgEquiv.toAlgEquiv
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
BoxIntegral.TaggedPrepartition.IsPartition.biUnionPrepartition : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {π : BoxIntegral.TaggedPrepartition I},
  π.IsPartition →
    ∀ {πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J},
      (∀ J ∈ π, (πi J).IsPartition) → (π.biUnionPrepartition πi).IsPartition
-- Lean.Environment
Lean.persistentEnvExtensionsRef : IO.Ref (Array (Lean.PersistentEnvExtension Lean.EnvExtensionEntry Lean.EnvExtensionEntry Lean.EnvExtensionState))
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.domDomCongrLinearEquiv'_apply : ∀ (R : Type uR) (S : Type uS) {ι : Type uι} (M₁ : ι → Type v₁) (M₂ : Type v₂) [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : (i : ι) → Module R (M₁ i)] [inst_3 : AddCommMonoid M₂]
  [inst_4 : Module R M₂] [inst_5 : Semiring S] [inst_6 : Module S M₂] [inst_7 : SMulCommClass R S M₂] {ι' : Type u_1}
  (σ : ι ≃ ι') (f : MultilinearMap R M₁ M₂),
  (MultilinearMap.domDomCongrLinearEquiv' R S M₁ M₂ σ) f =
    { toFun := ⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm, map_update_add' := ⋯, map_update_smul' := ⋯ }
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.leftRightHomologyComparison'_eq_descH : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h₁ : S.LeftHomologyData) (h₂ : S.RightHomologyData),
  CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁ h₂ =
    h₁.descH (h₂.liftH (CategoryTheory.CategoryStruct.comp h₁.i h₂.p) ⋯) ⋯
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instAddCommMonoid.eq_1 : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : AddCommMonoid Y],
  LocallyConstant.instAddCommMonoid = Function.Injective.addCommMonoid DFunLike.coe ⋯ ⋯ ⋯ ⋯
-- Init.Data.Float.Model.Format.Basic
/-- A floating point format is specified by two pieces of information: the number
of bits in the mantissa, and the number of bits in the exponent.
 -/
Float.Model.Format : Type
-- Mathlib.Algebra.Order.Module.Defs
Pi.instSMulPosMono : ∀ {α : Type u_1} {ι : Type u_3} {β : ι → Type u_4} [inst : Preorder α] [inst_1 : (i : ι) → Preorder (β i)]
  [inst_2 : (i : ι) → SMul α (β i)] [inst_3 : (i : ι) → Zero (β i)] [∀ (i : ι), SMulPosMono α (β i)],
  SMulPosMono α ((i : ι) → β i)
-- Mathlib.Analysis.MeanInequalities
/-- **Young's inequality** equality condition, `ℝ≥0∞` version with real conjugate exponents.  -/
ENNReal.young_inequality_eq_iff : ∀ (a b : ENNReal) {p q : ℝ},
  p.HolderConjugate q →
    (a * b = a ^ p / ENNReal.ofReal p + b ^ q / ENNReal.ofReal q ↔ a = ⊤ ∧ b ≠ 0 ∨ a ≠ 0 ∧ b = ⊤ ∨ a ^ p = b ^ q)
-- Mathlib.CategoryTheory.Adjunction.Additive
CategoryTheory.Adjunction.homAddEquiv_zero : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Preadditive D] {F : CategoryTheory.Functor C D}
  {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [F.Additive] (X : C) (Y : D), (adj.homEquiv X Y) 0 = 0
-- Mathlib.Algebra.Homology.SpectralObject.Basic
CategoryTheory.Abelian.SpectralObject.sc₃_g : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_4, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg) (n₀ n₁ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.sc₃._auto_1),
  (X.sc₃ f g fg h n₀ n₁ hn₁).g = X.δ f g n₀ n₁ hn₁
-- Mathlib.Probability.Kernel.Disintegration.Basic
ProbabilityTheory.Kernel.condKernelCountable_apply : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mΩ : MeasurableSpace Ω} [inst : Countable α] (κCond : α → ProbabilityTheory.Kernel β Ω)
  (h_atom : ∀ (x y : α), x ∈ measurableAtom y → κCond x = κCond y) (p : α × β),
  (ProbabilityTheory.Kernel.condKernelCountable κCond h_atom) p = (κCond p.1) p.2
-- Std.Http.Data.Headers.Basic
Std.Http.Header.Connection.inst : Std.Http.Header Std.Http.Header.Connection
-- Mathlib.Algebra.Group.Commute.Defs
/-- If both `a` and `b` commute with `c`, then their product commutes with `c`.  -/
Commute.mul_left : ∀ {S : Type u_3} [inst : Semigroup S] {a b c : S}, Commute a c → Commute b c → Commute (a * b) c
-- Mathlib.LinearAlgebra.Transvection.Generation
/-- Auxiliary lemma for the second non-exceptional case in Dieudonné's theorem:
with the notation of the proof of
`mem_transvections_pow_mul_dilatransvections_of_fixedReduce_ne_smul_id`,
the reductions of `auxTransvection hf * e` and `auxTransvection hg * e`
cannot both be homotheties.  -/
_private.Mathlib.LinearAlgebra.Transvection.Generation.0.LinearEquiv.not_forall_fixedReduce_eq_smul : ∀ {K : Type u_1} [inst : DivisionRing K] {V : Type u_2} [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [Module.Finite K V] {e : V ≃ₗ[K] V} {f g : Module.Dual K V} {v : V} {a b : K},
  LinearIndependent K ![(↑e).fixedSubmodule.mkQ v, e.fixedReduce ((↑e).fixedSubmodule.mkQ v)] →
    ∀ {hf : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ LinearMap.ker f},
      f v = 1 →
        ∀ {hg : (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ≤ LinearMap.ker (f + g)},
          (f + g) v = 1 →
            g ≠ 0 →
              (↑e).fixedSubmodule ⊔ K ∙ (e v - v) ⊔ K ∙ v < ⊤ →
                (∀ (x : V ⧸ (↑(LinearEquiv.auxTransvection✝ hf * e)).fixedSubmodule),
                    (LinearEquiv.auxTransvection✝ hf * e).fixedReduce x = a • x) →
                  (∀ (x : V ⧸ (↑(LinearEquiv.auxTransvection✝ hg * e)).fixedSubmodule),
                      (LinearEquiv.auxTransvection✝ hg * e).fixedReduce x = b • x) →
                    False
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous
CategoryTheory.Functor.instIsWellOrderContinuousNat : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor ℕ C), F.IsWellOrderContinuous
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.Attach
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.Attach.0.Std.Iterators.Types.Attach.Monadic.modifyStep.match_1.splitter : {α : Type u_1} →
  {m : Type u_1 → Type u_2} →
    {β : Type u_1} →
      [inst : Std.Iterator α m β] →
        {P : β → Prop} →
          (it : Std.IterM m { out // P out }) →
            (motive : it.internalState.inner.Step → Sort u_3) →
              (step : it.internalState.inner.Step) →
                ((it' : Std.IterM m β) →
                    (out : β) →
                      (h : it.internalState.inner.IsPlausibleStep (Std.IterStep.yield it' out)) →
                        motive ⟨Std.IterStep.yield it' out, h⟩) →
                  ((it' : Std.IterM m β) →
                      (h : it.internalState.inner.IsPlausibleStep (Std.IterStep.skip it')) →
                        motive ⟨Std.IterStep.skip it', h⟩) →
                    ((property : it.internalState.inner.IsPlausibleStep Std.IterStep.done) →
                        motive ⟨Std.IterStep.done, property⟩) →
                      motive step
-- Mathlib.Algebra.Group.End
Equiv.Perm.ofSubtype_apply_of_not_mem : ∀ {α : Type u_4} {p : α → Prop} [inst : DecidablePred p] {a : α} (f : Equiv.Perm (Subtype p)),
  ¬p a → (Equiv.Perm.ofSubtype f) a = a
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Relations.realize_total : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {r : L.Relations 2},
  M ⊨ r.total ↔ Std.Total fun x y => FirstOrder.Language.Structure.RelMap r ![x, y]
-- Mathlib.CategoryTheory.EquivalenceRelation
/-- A symmetric relation is a jointly monic pair of parallel morphisms `p₁, p₂ : R ⟶ X` together
with a morphism `s : R ⟶ R` which interchanges `p₁` and `p₂`.  -/
CategoryTheory.SymmetricRelation : {C : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} C] → {R X : C} → (R ⟶ X) → (R ⟶ X) → Type v_1
-- Mathlib.Order.Interval.Set.UnorderedInterval
/-- `uIoo a b` is the set of elements lying between `a` and `b`, with `a` and `b` not included.
Note that we define it more generally in a lattice as `Set.Ioo (a ⊓ b) (a ⊔ b)`. In a product type,
`uIoo` corresponds to the bounding box of the two elements.  -/
Set.uIoo : {α : Type u_1} → [LinearOrder α] → α → α → Set α
-- Mathlib.Algebra.Group.Defs
neg_add_cancel_comm : ∀ {G : Type u_1} [inst : AddCommGroup G] (a b : G), -a + b + a = b
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
/-- **Alias** of `ContMDiff.curry_left`.

---

Curried `C^n` functions are `C^n` in the first coordinate.  -/
ContMDiff.along_fst : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {F : Type u_8}
  [inst_11 : NormedAddCommGroup F] [inst_12 : NormedSpace 𝕜 F] {G : Type u_9} [inst_13 : TopologicalSpace G]
  {J : ModelWithCorners 𝕜 F G} {N : Type u_10} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  {n : WithTop ℕ∞} {f : M → M' → N},
  ContMDiff (I.prod I') J n (Function.uncurry f) → ∀ {y : M'}, ContMDiff I J n fun x => f x y
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem?_eq_some_iff_exists_compare_eq_eq_and_mem_toList : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β}, t[k]? = some v ↔ ∃ k', cmp k k' = Ordering.eq ∧ (k', v) ∈ t.toList
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
IntervalIntegrable.trans_iterate : ∀ {ε : Type u_3} [inst : TopologicalSpace ε] [inst_1 : ENormedAddMonoid ε] {f : ℝ → ε} {μ : MeasureTheory.Measure ℝ}
  [TopologicalSpace.PseudoMetrizableSpace ε] {a : ℕ → ℝ} {n : ℕ},
  (∀ k < n, IntervalIntegrable f μ (a k) (a (k + 1))) → IntervalIntegrable f μ (a 0) (a n)
-- Mathlib.Logic.Basic
/-- Any predicate `p` is decidable classically.  -/
Classical.decPred : {α : Sort u_1} → (p : α → Prop) → DecidablePred p
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_inv_rpow_eq_iff : ∀ {x : NNReal} {y : ℝ}, (x ^ y⁻¹) ^ y = x ↔ y ≠ 0 ∨ x = 1
-- Init.Data.String.Lemmas.Pattern.Basic
Std.IterM.toIter.eq_1 : ∀ {α β : Type w} (it : Std.IterM Id β), it.toIter = { internalState := it.internalState }
-- Mathlib.Algebra.Algebra.Hom
AlgHom.comp_toRingHom : ∀ {R : Type u} {A : Type v} {B : Type w} {C : Type u₁} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Semiring C] [inst_4 : Algebra R A] [inst_5 : Algebra R B] [inst_6 : Algebra R C]
  (φ₁ : B →ₐ[R] C) (φ₂ : A →ₐ[R] B), ↑(φ₁.comp φ₂) = (↑φ₁).comp ↑φ₂
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.empty_zpow : ∀ {α : Type u_2} [inst : DivisionMonoid α] {n : ℤ}, n ≠ 0 → ∅ ^ n = ∅
-- Init.Prelude
/-- Converts an `Array α` into a `List α` that contains the same elements in the same order.

At runtime, this is implemented by `Array.toListImpl` and is `O(n)` in the length of the
array.
 -/
Array.toList : {α : Type u} → Array α → List α
-- Mathlib.Topology.LocallyFinsupp
/-- Assign a function with locally finite support within `U` to a function in the subgroup.
 -/
Function.locallyFinsuppWithin.mk_of_mem_addSubmonoid : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    {U : Set X} →
      {Y : Type u_2} →
        [inst_1 : AddMonoid Y] →
          (f : X → Y) → f ∈ Function.locallyFinsuppWithin.addSubmonoid U → Function.locallyFinsuppWithin U Y
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey_le_minKey_erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {he : t.erase k ≠ ∅}, (cmp (t.minKey ⋯) ((t.erase k).minKey he)).isLE = true
-- Mathlib.Tactic.Contrapose
Mathlib.Tactic.Contrapose.contrapose_iff₁ : ∀ {p q : Prop}, (¬p ↔ ¬q) → (p ↔ q)
-- Mathlib.RingTheory.Artinian.Module
IsArtinianRing.isPrime_iff_isMaximal : ∀ {R : Type u_1} [inst : CommRing R] [IsArtinianRing R] (p : Ideal R), p.IsPrime ↔ p.IsMaximal
-- Mathlib.AlgebraicGeometry.ValuativeCriterion
/-- [Stacks Tag 01KE](https://stacks.math.columbia.edu/tag/01KE) -/
AlgebraicGeometry.ValuativeCriterion.Existence.specializingMap : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y), AlgebraicGeometry.ValuativeCriterion.Existence f → SpecializingMap ⇑f
-- Mathlib.LinearAlgebra.Determinant
LinearMap.associated_det_of_eq_comp : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] (e : M ≃ₗ[R] M)
  (f f' : M →ₗ[R] M), (∀ (x : M), f x = f' (e x)) → Associated (LinearMap.det f) (LinearMap.det f')
-- Mathlib.Algebra.Notation.Support
Function.mulSupport_const : ∀ {ι : Type u_1} {M : Type u_3} [inst : One M] {c : M}, c ≠ 1 → (Function.mulSupport fun x => c) = Set.univ
-- Mathlib.CategoryTheory.Bicategory.Basic
/-- Middle component of the associator as a natural isomorphism.  -/
CategoryTheory.Bicategory.associatorNatIsoMiddle : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c d : B} →
      (f : a ⟶ b) →
        (h : c ⟶ d) →
          ((CategoryTheory.Bicategory.precomposing a b c).obj f).comp
              ((CategoryTheory.Bicategory.postcomposing a c d).obj h) ≅
            ((CategoryTheory.Bicategory.postcomposing b c d).obj h).comp
              ((CategoryTheory.Bicategory.precomposing a b d).obj f)