mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
/-- If `e : C ≌ D`, then the pushforwards along `e.functor` and `e.inverse` forms an equivalence.  -/
SheafOfModules.pushforwardPushforwardEquivalence : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : CategoryTheory.GrothendieckTopology C} →
          {K : CategoryTheory.GrothendieckTopology D} →
            (eqv : C ≌ D) →
              {S : CategoryTheory.Sheaf J RingCat} →
                {R : CategoryTheory.Sheaf K RingCat} →
                  [inst_2 : eqv.functor.IsContinuous J K] →
                    [inst_3 : eqv.inverse.IsContinuous K J] →
                      (φ : S ⟶ (eqv.functor.sheafPushforwardContinuous RingCat J K).obj R) →
                        (ψ : R ⟶ (eqv.inverse.sheafPushforwardContinuous RingCat K J).obj S) →
                          CategoryTheory.Functor.whiskerRight (CategoryTheory.NatTrans.op eqv.counit) R.obj =
                              CategoryTheory.CategoryStruct.comp ψ.hom (eqv.inverse.op.whiskerLeft φ.hom) →
                            CategoryTheory.CategoryStruct.comp φ.hom
                                  (CategoryTheory.CategoryStruct.comp (eqv.functor.op.whiskerLeft ψ.hom)
                                    (CategoryTheory.Functor.whiskerRight (CategoryTheory.NatTrans.op eqv.unit) S.obj)) =
                                CategoryTheory.CategoryStruct.id S.obj →
                              (SheafOfModules R ≌ SheafOfModules S)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof : Type
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenModifier.defaultLibrary : Lean.Lsp.SemanticTokenModifier
-- Mathlib.Combinatorics.Additive.ETransform
/-- The **Dyson e-transform**. Turns `(s, t)` into `(s ∪ e • t, t ∩ e⁻¹ • s)`. This reduces the
product of the two sets.  -/
Finset.mulDysonETransform : {α : Type u_1} → [DecidableEq α] → [CommGroup α] → α → Finset α × Finset α → Finset α × Finset α
-- Mathlib.Algebra.Order.BigOperators.Group.Multiset
Multiset.sum_le_sum_of_rel_le : ∀ {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : Preorder α] {s t : Multiset α} [AddLeftMono α],
  Multiset.Rel (fun x1 x2 => x1 ≤ x2) s t → s.sum ≤ t.sum
-- Mathlib.RingTheory.GradedAlgebra.TensorProduct
GradedAlgebra.instRingSubtypeTensorProductMemSubmoduleBaseChangeOfNat : {ι : Type u_1} →
  {R : Type u_2} →
    {A : Type u_3} →
      {S : Type u_4} →
        [inst : CommSemiring R] →
          [inst_1 : CommRing S] →
            [inst_2 : Algebra R S] →
              [inst_3 : DecidableEq ι] →
                [inst_4 : AddMonoid ι] →
                  [inst_5 : Semiring A] →
                    [inst_6 : Algebra R A] →
                      (𝒜 : ι → Submodule R A) → [GradedAlgebra 𝒜] → Ring ↥(Submodule.baseChange S (𝒜 0))
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.image_ofSnowflaking_eball : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [inst : PseudoEMetricSpace X] (x : Metric.Snowflaking X α hα₀ hα₁)
  (d : ENNReal),
  ⇑Metric.Snowflaking.ofSnowflaking '' Metric.eball x d = Metric.eball (Metric.Snowflaking.ofSnowflaking x) (d ^ α⁻¹)
-- Mathlib.Lean.Meta.RefinedDiscrTree.Lookup
/-- Monad for working with a `RefinedDiscrTree`.  -/
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Lookup.0.Lean.Meta.RefinedDiscrTree.TreeM : Type → Type → Type
-- Mathlib.LinearAlgebra.BilinearForm.Basic
LinearMap.BilinForm.congr_fun : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {B D : LinearMap.BilinForm R M}, B = D → ∀ (x y : M), (B x) y = (D x) y
-- Mathlib.Algebra.MvPolynomial.Division
MvPolynomial.eq_modMonomial_single_iff : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] {i : σ} {p r : MvPolynomial σ R},
  MvPolynomial.X i ∣ p - r → ((r = p.modMonomial fun₀ | i => 1) ↔ ∀ n ∈ r.support, n i = 0)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.Cell.mk.inj : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} {inst : LinearOrder ι} {f : P.RankFunction ι} {i : ι}
  {s : ↑P.II} {rank_s : f.rank s = i} {s_1 : ↑P.II} {rank_s_1 : f.rank s_1 = i},
  { s := s, rank_s := rank_s } = { s := s_1, rank_s := rank_s_1 } → s = s_1
-- Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
CliffordAlgebra.changeForm_ι_mul_ι : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q Q' : QuadraticForm R M} {B : LinearMap.BilinForm R M} (h : LinearMap.BilinMap.toQuadraticMap B = Q' - Q)
  (m₁ m₂ : M),
  (CliffordAlgebra.changeForm h) ((CliffordAlgebra.ι Q) m₁ * (CliffordAlgebra.ι Q) m₂) =
    (CliffordAlgebra.ι Q') m₁ * (CliffordAlgebra.ι Q') m₂ - (algebraMap R (CliffordAlgebra Q')) ((B m₁) m₂)
-- Std.Data.DHashMap.Internal.Defs
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.contains : {α : Type u} → {β : α → Type v} → [BEq α] → [Hashable α] → Std.DHashMap.Internal.Raw₀ α β → α → Bool
-- Mathlib.MeasureTheory.OuterMeasure.AE
MeasureTheory.ae_eq_rfl : ∀ {α : Type u_1} {β : Type u_2} {F : Type u_3} [inst : FunLike F (Set α) ENNReal]
  [inst_1 : MeasureTheory.OuterMeasureClass F α] {μ : F} {f : α → β}, f =ᵐ[μ] f
-- Mathlib.Topology.Algebra.Group.Torsor
/-- A topological torsor over a topological group is a torsor where `•` and `/ₛ` are continuous.  -/
IsTopologicalTorsor : {V : Type u_1} → [inst : Group V] → [TopologicalSpace V] → (P : Type u_2) → [Torsor V P] → [TopologicalSpace P] → Prop
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.mk.inj : ∀ {𝕜 : Type u_7} {α : Type u_8} {inst : Zero 𝕜} {inst_1 : LE α} {toFun : α → α → 𝕜}
  {eq_zero_of_not_le' : ∀ ⦃a b : α⦄, ¬a ≤ b → toFun a b = 0} {toFun_1 : α → α → 𝕜}
  {eq_zero_of_not_le'_1 : ∀ ⦃a b : α⦄, ¬a ≤ b → toFun_1 a b = 0},
  { toFun := toFun, eq_zero_of_not_le' := eq_zero_of_not_le' } =
      { toFun := toFun_1, eq_zero_of_not_le' := eq_zero_of_not_le'_1 } →
    toFun = toFun_1
-- Mathlib.Algebra.GroupWithZero.Action.End
/-- Each non-zero element of a `GroupWithZero` defines an additive monoid isomorphism of an
`AddMonoid` on which it acts distributively.
This is a stronger version of `DistribSMul.toAddMonoidHom`.  -/
DistribMulAction.toAddEquiv₀ : {α : Type u_6} →
  (β : Type u_7) → [inst : GroupWithZero α] → [inst_1 : AddMonoid β] → [DistribMulAction α β] → (x : α) → x ≠ 0 → β ≃+ β
-- Lean.Elab.DeprecatedArg
Lean.Elab.DeprecatedArgEntry.mk : Lean.Name → Lean.Name → Option Lean.Name → Option String → Option String → Lean.Elab.DeprecatedArgEntry
-- Mathlib.Order.Category.FinBddDistLat
FinBddDistLat.dualEquiv_functor : FinBddDistLat.dualEquiv.functor = FinBddDistLat.dual
-- Mathlib.Tactic.FunProp.FunctionData
/-- main function  -/
Mathlib.Meta.FunProp.FunctionData.fn : Mathlib.Meta.FunProp.FunctionData → Lean.Expr
-- Mathlib.Algebra.Star.StarRingHom
NonUnitalStarRingHom.instZero : {A : Type u_1} →
  {B : Type u_2} →
    [inst : NonUnitalNonAssocSemiring A] →
      [inst_1 : StarAddMonoid A] →
        [inst_2 : NonUnitalNonAssocSemiring B] → [inst_3 : StarAddMonoid B] → Zero (A →⋆ₙ+* B)
-- Mathlib.Data.List.DropRight
/-- Take elements from the tail end of a list that satisfy `p : α → Bool`.
Implemented naively via `List.reverse`  -/
List.rtakeWhile : {α : Type u_1} → (α → Bool) → List α → List α
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
/-- `X₁ ⨿[Z₁] (X₂ ⨿[Z₂] X₃)` is the pushout `(X₁ ⨿[Z₁] X₂) ⨿[Z₂] X₃`.  -/
CategoryTheory.Limits.pushoutAssocSymmIsPushout : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X₁ X₂ X₃ Z₁ Z₂ : C} →
      (g₁ : Z₁ ⟶ X₁) →
        (g₂ : Z₁ ⟶ X₂) →
          (g₃ : Z₂ ⟶ X₂) →
            (g₄ : Z₂ ⟶ X₃) →
              [inst_1 : CategoryTheory.Limits.HasPushout g₁ g₂] →
                [inst_2 : CategoryTheory.Limits.HasPushout g₃ g₄] →
                  [inst_3 :
                      CategoryTheory.Limits.HasPushout g₁
                        (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄))] →
                    CategoryTheory.Limits.IsColimit
                      (CategoryTheory.Limits.PushoutCocone.mk
                        (CategoryTheory.Limits.pushout.desc
                          (CategoryTheory.Limits.pushout.inl g₁
                            (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄)))
                          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl g₃ g₄)
                            (CategoryTheory.Limits.pushout.inr g₁
                              (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄))))
                          ⋯)
                        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr g₃ g₄)
                          (CategoryTheory.Limits.pushout.inr g₁
                            (CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.pushout.inl g₃ g₄))))
                        ⋯)
-- Init.Data.UInt.Lemmas
UInt16.sub_eq_add_mul : ∀ (a b : UInt16), a - b = a + 65535 * b
-- Std.Data.TreeSet.Raw.WF
Std.TreeSet.Raw.WF.emptyc : ∀ {α : Type u} {cmp : α → α → Ordering}, ∅.WF
-- Mathlib.LinearAlgebra.Matrix.Trace
Matrix.trace_blockDiagonal : ∀ {n : Type u_3} {p : Type u_4} {R : Type u_6} [inst : Fintype n] [inst_1 : Fintype p] [inst_2 : AddCommMonoid R]
  [inst_3 : DecidableEq p] (M : p → Matrix n n R), (Matrix.blockDiagonal M).trace = ∑ i, (M i).trace
-- Mathlib.Analysis.LocallyConvex.HahnBanach
/-- A finite-dimensional submodule of a polynormable space over a field satisfying
`IsRCLikeNormedField` is `Submodule.ClosedComplemented`.  -/
Submodule.ClosedComplemented.of_finiteDimensional : ∀ {𝕜 : Type u_1} [inst : NormedField 𝕜] [IsRCLikeNormedField 𝕜] {F : Type u_3} [inst_2 : AddCommGroup F]
  [inst_3 : TopologicalSpace F] [IsTopologicalAddGroup F] [inst_5 : Module 𝕜 F] [ContinuousSMul 𝕜 F] [T2Space F]
  [PolynormableSpace 𝕜 F] (S : Submodule 𝕜 F) [FiniteDimensional 𝕜 ↥S], S.ClosedComplemented
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.measurePreserving_div_right : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [MeasurableMul G] (μ : MeasureTheory.Measure G)
  [μ.IsMulRightInvariant] (g : G), MeasureTheory.MeasurePreserving (fun x => x / g) μ μ
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Rxc.Iterator.step.eq_1 : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LE α] [inst_2 : DecidableLE α] (it : Std.Iter α),
  Std.Rxc.Iterator.step it =
    match it.internalState.next with
    | none => Std.IterStep.done
    | some next =>
      if next ≤ it.internalState.upperBound then
        Std.IterStep.yield
          { internalState := { next := Std.PRange.succ? next, upperBound := it.internalState.upperBound } } next
      else Std.IterStep.done
-- Mathlib.Probability.IdentDistrib
ProbabilityTheory.IdentDistrib.ae_mem_snd : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {f : α → γ} {g : β → γ},
  ProbabilityTheory.IdentDistrib f g μ ν →
    ∀ {t : Set γ}, MeasurableSet t → (∀ᵐ (x : α) ∂μ, f x ∈ t) → ∀ᵐ (x : β) ∂ν, g x ∈ t
-- Mathlib.Analysis.Calculus.Deriv.Polynomial
Polynomial.differentiableAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} (p : Polynomial 𝕜),
  DifferentiableAt 𝕜 (fun x => Polynomial.eval x p) x
-- Lean.ToExpr
Lean.instToExprInt : Lean.ToExpr ℤ
-- Mathlib.Topology.UniformSpace.Cauchy
cauchySeq_iff' : ∀ {α : Type u} [uniformSpace : UniformSpace α] {u : ℕ → α},
  CauchySeq u ↔ ∀ V ∈ uniformity α, ∀ᶠ (k : ℕ × ℕ) in Filter.atTop, k ∈ Prod.map u u ⁻¹' V
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
/-- The `i`-th degeneracy map from `⦋n+1⦌` to `⦋n⦌`  -/
SimplexCategory.σ : {n : ℕ} → Fin (n + 1) → ({ len := n + 1 } ⟶ { len := n })
-- Mathlib.Topology.Order.Category.FrameAdjunction
/-- The unit of the adjunction between locales and topological spaces, which associates with
a point `x` of the space `X` a point of the locale of opens of `X`.  -/
Locale.localePointOfSpacePoint : (X : Type u_1) → [inst : TopologicalSpace X] → X → Locale.PT (TopologicalSpace.Opens X)
-- Mathlib.Algebra.Group.Subgroup.Lattice
/-- `closure` forms a Galois insertion with the coercion to set.  -/
AddSubgroup.gi : (G : Type u_1) → [inst : AddGroup G] → GaloisInsertion AddSubgroup.closure SetLike.coe
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.SelectM.State.mk.inj : ∀ {suggestions : Array Lean.Meta.Tactic.TryThis.Suggestion} {thms : Array Lean.Meta.Grind.EMatchTheorem}
  {suggestions_1 : Array Lean.Meta.Tactic.TryThis.Suggestion} {thms_1 : Array Lean.Meta.Grind.EMatchTheorem},
  { suggestions := suggestions, thms := thms } = { suggestions := suggestions_1, thms := thms_1 } →
    suggestions = suggestions_1 ∧ thms = thms_1
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
AugmentedSimplexCategory.tensorHom_id : ∀ {x₁ x₂ : AugmentedSimplexCategory} (y : AugmentedSimplexCategory) (f : x₁ ⟶ x₂),
  CategoryTheory.MonoidalCategoryStruct.tensorHom f (CategoryTheory.CategoryStruct.id y) =
    CategoryTheory.MonoidalCategoryStruct.whiskerRight f y
-- Mathlib.Data.Finset.Basic
Finset.erase_injOn' : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α), Set.InjOn (fun s => s.erase a) {s | a ∈ s}
-- Init.Internal.Order.Basic
Lean.Order.inf_le : ∀ {α : Sort u} [inst : Lean.Order.CompleteLattice α] {c : α → Prop} {y : α},
  c y → Lean.Order.PartialOrder.rel (Lean.Order.inf c) y
-- Mathlib.Data.List.Iterate
_private.Mathlib.Data.List.Iterate.0.Nat.iterate.match_1.eq_2 : ∀ {α : Sort u_2} (motive : ℕ → α → Sort u_1) (k : ℕ) (a : α) (h_1 : (a : α) → motive 0 a)
  (h_2 : (k : ℕ) → (a : α) → motive k.succ a),
  (match k.succ, a with
    | 0, a => h_1 a
    | k.succ, a => h_2 k a) =
    h_2 k a
-- Mathlib.Analysis.Calculus.Deriv.Pow
deriv_fun_pow' : ∀ {𝕜 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing 𝔸] [inst_2 : NormedAlgebra 𝕜 𝔸]
  {f : 𝕜 → 𝔸} {x : 𝕜},
  DifferentiableAt 𝕜 f x →
    ∀ (n : ℕ), deriv (fun x => f x ^ n) x = ∑ i ∈ Finset.range n, f x ^ (n.pred - i) * deriv f x * f x ^ i
-- Aesop.Script.TacticState
Aesop.Script.TacticState.visibleGoals : Aesop.Script.TacticState → Array Aesop.GoalWithMVars
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Decl.toSignature : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Decl pu → Lean.Compiler.LCNF.Signature pu
-- Std.Data.HashMap.Basic
/-- Computes the difference of the given hash maps.

This function always iterates through the smaller map, so the expected runtime is
`O(min(m₁.size, m₂.size))`.
 -/
Std.HashMap.diff : {α : Type u} →
  {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → Std.HashMap α β → Std.HashMap α β → Std.HashMap α β
-- Mathlib.Analysis.Calculus.Deriv.ZPow
iter_deriv_inv : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (k : ℕ) (x : 𝕜),
  deriv^[k] Inv.inv x = (-1) ^ k * ↑k.factorial * x ^ (-1 - ↑k)
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.augment_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) (X₀ : C)
  (f : X.obj (Opposite.op { len := 0 }) ⟶ X₀)
  (w :
    ∀ (i : SimplexCategory) (g₁ g₂ : { len := 0 } ⟶ i),
      CategoryTheory.CategoryStruct.comp (X.map g₁.op) f = CategoryTheory.CategoryStruct.comp (X.map g₂.op) f),
  (X.augment X₀ f w).right = X₀
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.UnsatProof.diseq.sizeOf_spec : ∀ (c : Lean.Meta.Grind.Arith.Linear.DiseqCnstr), sizeOf (Lean.Meta.Grind.Arith.Linear.UnsatProof.diseq c) = 1 + sizeOf c
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.instEpiGCokernelSequenceOpcyclesE : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃)
  (f₁₂ : i₀ ⟶ i₂) (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁)
  (hn₂ : n₁ + 1 = n₂), CategoryTheory.Epi (X.cokernelSequenceOpcyclesE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).g
-- Mathlib.Analysis.Normed.Group.Constructions
/-- Finite product of normed groups, using the sup norm.  -/
Pi.normedGroup : {ι : Type u_1} → {G : ι → Type u_4} → [Fintype ι] → [(i : ι) → NormedGroup (G i)] → NormedGroup ((i : ι) → G i)
-- Mathlib.Order.Hom.WithTopBot
LatticeHom.withBotWithTop_id : ∀ {α : Type u_1} [inst : Lattice α], (LatticeHom.id α).withBotWithTop = BoundedLatticeHom.id (WithBot (WithTop α))
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap.0.Std.IterM.step_flattenAfter.match_1.splitter : {α α₂ β : Type u_1} →
  {m : Type u_1 → Type u_2} →
    [inst : Std.Iterator α m (Std.IterM m β)] →
      {it₁ : Std.IterM m (Std.IterM m β)} →
        (motive : it₁.Step → Sort u_3) →
          (x : it₁.Step) →
            ((it₁' : Std.IterM m (Std.IterM m β)) →
                (it₂' : Std.IterM m β) →
                  (h : it₁.IsPlausibleStep (Std.IterStep.yield it₁' it₂')) → motive ⟨Std.IterStep.yield it₁' it₂', h⟩) →
              ((it₁' : Std.IterM m (Std.IterM m β)) →
                  (h : it₁.IsPlausibleStep (Std.IterStep.skip it₁')) → motive ⟨Std.IterStep.skip it₁', h⟩) →
                ((h : it₁.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩) → motive x
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.smul_apply : ∀ {𝕜 : Type u_2} {𝕝 : Type u_3} {α : Type u_5} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α]
  [inst_2 : AddCommMonoid 𝕜] [inst_3 : AddCommMonoid 𝕝] [inst_4 : SMul 𝕜 𝕝] (f : IncidenceAlgebra 𝕜 α)
  (g : IncidenceAlgebra 𝕝 α) (a b : α), (f • g) a b = ∑ x ∈ Finset.Icc a b, f a x • g x b
-- Mathlib.InformationTheory.KullbackLeibler.KLFun
/-- `klFun` is convex on $(0,∞)$.
This is an often useful consequence of `convexOn_klFun`, which states convexity on $[0, ∞)$.  -/
InformationTheory.convexOn_Ioi_klFun : ConvexOn ℝ (Set.Ioi 0) InformationTheory.klFun
-- Init.Data.List.MinMax
List.get_min? : ∀ {α : Type u_1} [inst : Min α] {l : List α} {h : l.min?.isSome = true}, l.min?.get h = l.min ⋯
-- Mathlib.Algebra.Group.Semiconj.Basic
/-- **Alias** of the reverse direction of `SemiconjBy.inv_inv_symm_iff`. -/
SemiconjBy.inv_inv_symm : ∀ {G : Type u_1} [inst : DivisionMonoid G] {a x y : G}, SemiconjBy a y x → SemiconjBy a⁻¹ x⁻¹ y⁻¹
-- Mathlib.Topology.Convenient.HomSpace
Topology.ContinuousMapGeneratedBy.postcomp_apply : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type v} [inst_1 : TopologicalSpace Y]
  {Z : Type v'} [inst_2 : TopologicalSpace Z] {T : Type v''} [inst_3 : TopologicalSpace T]
  [inst_4 : ∀ (i : ι), LocallyCompactSpace (X i)] [inst_5 : ∀ (i j : ι), Topology.IsGeneratedBy X (X i × X j)]
  (p : Topology.ContinuousMapGeneratedBy X Z T) (g : Topology.ContinuousMapGeneratedBy X Y Z), p.postcomp g = p.comp g
-- Mathlib.CategoryTheory.Limits.Types.Pushouts
/-- The cocone `cocone f g` is colimit.  -/
CategoryTheory.Limits.Types.Pushout.isColimitCocone : {S X₁ X₂ : Type u} →
  (f : S ⟶ X₁) → (g : S ⟶ X₂) → CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Types.Pushout.cocone f g)
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.mop_associator : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y Z : C),
  (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).mop =
    (CategoryTheory.MonoidalCategoryStruct.associator { unmop := Z } { unmop := Y } { unmop := X }).symm
-- Mathlib.Topology.Instances.Matrix
instIsTopologicalAddGroupMatrix : ∀ {m : Type u_4} {n : Type u_5} {R : Type u_8} [inst : TopologicalSpace R] [inst_1 : AddGroup R]
  [IsTopologicalAddGroup R], IsTopologicalAddGroup (Matrix m n R)
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.parseIdentifier : Std.Internal.Parsec.String.Parser String
-- Mathlib.Data.DFinsupp.BigOperators
map_dfinsuppProd : ∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] {R : Type u_1} {S : Type u_2} {H : Type u_3}
  [inst_1 : (i : ι) → Zero (β i)] [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] [inst_3 : CommMonoid R]
  [inst_4 : CommMonoid S] [inst_5 : FunLike H R S] [MonoidHomClass H R S] (h : H) (f : Π₀ (i : ι), β i)
  (g : (i : ι) → β i → R), h (f.prod g) = f.prod fun a b => h (g a b)
-- Mathlib.Topology.Maps.Basic
Topology.IsEmbedding.of_comp_iff : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [inst : TopologicalSpace X]
  [inst_1 : TopologicalSpace Y] [inst_2 : TopologicalSpace Z],
  Topology.IsEmbedding g → (Topology.IsEmbedding (g ∘ f) ↔ Topology.IsEmbedding f)
-- Mathlib.Tactic.NormNum.DivMod
Mathlib.Meta.NormNum.isNat_neg_of_isNegNat : ∀ {a : ℤ} {b : ℕ}, Mathlib.Meta.NormNum.IsInt a (Int.negOfNat b) → Mathlib.Meta.NormNum.IsNat (-a) b
-- Mathlib.Order.CompleteLattice.Defs
OrderDual.instCompleteLinearOrder : {α : Type u_1} → [CompleteLinearOrder α] → CompleteLinearOrder αᵒᵈ
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.SimpleFunc.tendsto_approxOn_range_L1_enorm : ∀ {β : Type u_2} {E : Type u_4} [inst : MeasurableSpace β] [inst_1 : MeasurableSpace E] [inst_2 : NormedAddCommGroup E]
  [inst_3 : OpensMeasurableSpace E] {f : β → E} {μ : MeasureTheory.Measure β}
  [inst_4 : TopologicalSpace.SeparableSpace ↑(Set.range f ∪ {0})] (fmeas : Measurable f),
  MeasureTheory.Integrable f μ →
    Filter.Tendsto
      (fun n => ∫⁻ (x : β), ‖(MeasureTheory.SimpleFunc.approxOn f fmeas (Set.range f ∪ {0}) 0 ⋯ n) x - f x‖ₑ ∂μ)
      Filter.atTop (nhds 0)
-- Mathlib.CategoryTheory.Bicategory.Span.Basic
/-- the right map  -/
CategoryTheory.Span.r : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {Wₗ Wᵣ : CategoryTheory.MorphismProperty C} → {c c' : C} → (self : CategoryTheory.Span Wₗ Wᵣ c c') → self.apex ⟶ c'
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.sum_eq_nsmul_single : ∀ {M : Type u_4} [inst : AddMonoid M] {l : List M} [inst_1 : DecidableEq M] (a : M),
  (∀ (a' : M), a' ≠ a → a' ∈ l → a' = 0) → l.sum = List.count a l • a
-- Mathlib.InformationTheory.KullbackLeibler.DataProcessing
InformationTheory.toReal_klDiv_trim_of_ac : ∀ {𝓧 : Type u_1} {m m𝓧 : MeasurableSpace 𝓧} {μ ν : MeasureTheory.Measure 𝓧} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν] (hm : m ≤ m𝓧),
  μ.AbsolutelyContinuous ν →
    (InformationTheory.klDiv (μ.trim hm) (ν.trim hm)).toReal =
      ∫ (x : 𝓧), InformationTheory.klFun (ν[fun x => (μ.rnDeriv ν x).toReal | m] x) ∂ν
-- Mathlib.Order.Basic
Order.Preimage.eq_1 : ∀ {α : Type u_2} {β : Type u_3} (f : α → β) (s : β → β → Prop) (x y : α), (f ⁻¹'o s) x y = s (f x) (f y)
-- Mathlib.Order.Closure
OrderIso.equivClosureOperator_symm_apply : ∀ {α : Type u_4} {β : Type u_5} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β) (c : ClosureOperator β),
  e.equivClosureOperator.symm c = c.conjBy e.symm
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.BinaryFan.swap_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (s : CategoryTheory.Limits.BinaryFan X Y),
  s.swap.snd = s.fst
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.moduleCategory : (R : Type u) → [inst : Semiring R] → CategoryTheory.Category.{v, max (v + 1) u} (SemimoduleCat R)
-- Mathlib.NumberTheory.ArithmeticFunction.Zeta
ArithmeticFunction.zeta_apply : ∀ {x : ℕ}, ArithmeticFunction.zeta x = if x = 0 then 0 else 1
-- Mathlib.Topology.Order.LawsonTopology
Topology.IsLawson.mk : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α], inst_1 = Topology.lawson α → Topology.IsLawson α