mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Kernel.Composition.KernelLemmas
ProbabilityTheory.Kernel.comp_eq_snd_compProd : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {mX : MeasurableSpace X} {mY : MeasurableSpace Y}
  {mZ : MeasurableSpace Z} (η : ProbabilityTheory.Kernel Y Z) [ProbabilityTheory.IsSFiniteKernel η]
  (κ : ProbabilityTheory.Kernel X Y) [ProbabilityTheory.IsSFiniteKernel κ],
  η.comp κ = (κ.compProd (ProbabilityTheory.Kernel.prodMkLeft X η)).snd
-- Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne
SimplexCategory.toMk₁_apply_eq_zero_iff : ∀ {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)),
  (CategoryTheory.ConcreteCategory.hom (SimplexCategory.toMk₁ i)) j = 0 ↔ j.castSucc < i
-- Mathlib.NumberTheory.NumberField.Units.Basic
Rat.RingOfIntegers.isUnit_iff : ∀ {x : NumberField.RingOfIntegers ℚ}, IsUnit x ↔ ↑x = 1 ∨ ↑x = -1
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.intCoe : {R : Type u_1} → [inst : AddGroupWithOne R] → Coe (ArithmeticFunction ℤ) (ArithmeticFunction R)
-- Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
/-- `pinGroup Q` is defined as the infimum of `lipschitzGroup Q` and `unitary (CliffordAlgebra Q)`.
See `mem_iff`.  -/
pinGroup : {R : Type u_1} →
  [inst : CommRing R] →
    {M : Type u_2} →
      [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → (Q : QuadraticForm R M) → Submonoid (CliffordAlgebra Q)
-- Mathlib.Data.Sum.Interval
Sum.Icc_inr_inr : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : LocallyFiniteOrder β] (b₁ b₂ : β),
  Finset.Icc (Sum.inr b₁) (Sum.inr b₂) = Finset.map Function.Embedding.inr (Finset.Icc b₁ b₂)
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.shiftFunctorComm_inv_app_of_add_eq_zero_assoc : ∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddCommMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (m n : A) (hmn : m + n = 0) (X : C) {Z : C}
  (h : (CategoryTheory.shiftFunctor C n).obj ((CategoryTheory.shiftFunctor C m).obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorComm C m n).inv.app X) h =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId C n m ⋯).hom.app X)
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId C m n hmn).inv.app X) h)
-- Mathlib.Topology.Compactness.Lindelof
/-- In a non-Lindelöf space, `Set.univ` is not a Lindelöf set.  -/
NonLindelofSpace.nonLindelof_univ : ∀ {X : Type u_2} {inst : TopologicalSpace X} [self : NonLindelofSpace X], ¬IsLindelof Set.univ
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.lift_snd_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {X Y : C},
  CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y)
      (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y) =
    (β_ X Y).hom
-- Plausible.Arbitrary
Plausible.UInt64.Arbitrary : Plausible.Arbitrary UInt64
-- Mathlib.Algebra.Order.Group.Pointwise.Bounds
isGLB_neg : ∀ {G : Type u_2} [inst : AddGroup G] [inst_1 : Preorder G] [AddLeftMono G] [AddRightMono G] {s : Set G} {a : G},
  IsGLB (-s) a ↔ IsLUB s (-a)
-- Init.Data.String.Termination
String.Pos.inner_down : ∀ {s : String} {p : s.Pos}, p.down.inner = p
-- Mathlib.Algebra.Ring.Subring.Basic
AddSubgroup.int_mul_mem : ∀ {R : Type u} [inst : NonAssocRing R] {G : AddSubgroup R} (k : ℤ) {g : R}, g ∈ G → ↑k * g ∈ G
-- Mathlib.NumberTheory.FLT.Basic
fermatLastTheoremFor_zero : FermatLastTheoremFor 0
-- Mathlib.CategoryTheory.Category.Quiv
CategoryTheory.Quiv.inv_obj_hom_obj_of_iso : ∀ {V W : CategoryTheory.Quiv} (e : V ≅ W) (X : ↑V), e.inv.obj (e.hom.obj X) = X
-- Mathlib.Analysis.Calculus.ContDiff.Comp
/-- A special case of `ContDiffWithinAt.fderivWithin'` where we require that `x₀ ∈ s` and there
are unique derivatives everywhere within `t`.  -/
ContDiffWithinAt.fderivWithin : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {s : Set E} {x₀ : E} {m n : WithTop ℕ∞} {f : E → F → G}
  {g : E → F} {t : Set F},
  ContDiffWithinAt 𝕜 n (Function.uncurry f) (s ×ˢ t) (x₀, g x₀) →
    ContDiffWithinAt 𝕜 m g s x₀ →
      UniqueDiffOn 𝕜 t →
        m + 1 ≤ n → x₀ ∈ s → s ⊆ g ⁻¹' t → ContDiffWithinAt 𝕜 m (fun x => fderivWithin 𝕜 (f x) t (g x)) s x₀
-- Mathlib.CategoryTheory.Comma.Over.Pullback
CategoryTheory.Under.forgetMapInitial_inv_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C) {I : C} (hI : CategoryTheory.Limits.IsInitial I)
  (X_1 : CategoryTheory.Under X),
  (CategoryTheory.Under.forgetMapInitial X hI).inv.app X_1 = CategoryTheory.CategoryStruct.id X_1.right
-- Mathlib.RingTheory.Algebraic.Basic
transcendental_ringHom_iff_of_comp_eq : ∀ {R : Type u} {S : Type u_1} {A : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Ring A]
  [inst_3 : Algebra R A] {B : Type u_2} [inst_4 : Ring B] [inst_5 : Algebra S B] {FRS : Type u_3} {FAB : Type u_4}
  [inst_6 : EquivLike FRS R S] [inst_7 : RingEquivClass FRS R S] [inst_8 : FunLike FAB A B]
  [inst_9 : RingHomClass FAB A B] (f : FRS) (g : FAB),
  Function.Injective ⇑g →
    (algebraMap S B).comp ↑f = (↑g).comp (algebraMap R A) → ∀ {a : A}, Transcendental S (g a) ↔ Transcendental R a
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get?_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {a k : α} {v : β k},
  (t.insert k v).get? a = if h : cmp k a = Ordering.eq then some (cast ⋯ v) else t.get? a
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.contains_of_contains_erase : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {k a : α}, (m.erase k).contains a = true → m.contains a = true
-- Mathlib.Order.Heyting.Regular
Heyting.Regular.coe_sup : ∀ {α : Type u_1} [inst : HeytingAlgebra α] (a b : Heyting.Regular α), ↑(a ⊔ b) = (↑a ⊔ ↑b)ᶜᶜ
-- Aesop.Search.Expansion.Basic
Aesop.runRuleTac : Aesop.RuleTac →
  Aesop.RuleName → Lean.Meta.SavedState → Aesop.RuleTacInput → Aesop.BaseM (Except Lean.Exception Aesop.RuleTacOutput)
-- Mathlib.CategoryTheory.Category.Quiv
/-- Compatible equivalences of types and hom-types induce an isomorphism of quivers.  -/
CategoryTheory.Quiv.isoOfEquiv : {V W : Type u} →
  [inst : Quiver V] →
    [inst_1 : Quiver W] →
      (e : V ≃ W) → ((X Y : V) → (X ⟶ Y) ≃ (e X ⟶ e Y)) → (CategoryTheory.Quiv.of V ≅ CategoryTheory.Quiv.of W)
-- Lean.Meta.Tactic.Grind.Arith.Linear.StructId
_private.Lean.Meta.Tactic.Grind.Arith.Linear.StructId.0.Lean.Meta.Grind.Arith.Linear.ensureToFieldDefEq : Lean.Expr → Lean.Expr → Lean.Name → Lean.Level → Lean.Expr → Lean.Meta.Grind.GoalM Unit
-- Mathlib.Algebra.Module.Lattice
Submodule.IsLattice.span_eq_top : ∀ {R : Type u_1} {inst : CommRing R} {A : outParam (Type u_2)} {inst_1 : CommRing A} {inst_2 : Algebra R A}
  {V : Type u_3} {inst_3 : AddCommMonoid V} {inst_4 : Module R V} {inst_5 : Module A V}
  {inst_6 inst_7 : IsScalarTower R A V} {M : Submodule R V} [self : Submodule.IsLattice A M], Submodule.span A ↑M = ⊤
-- Mathlib.NumberTheory.LSeries.Injectivity
LSeries_eq_zero_of_abscissaOfAbsConv_eq_top : ∀ {f : ℕ → ℂ}, LSeries.abscissaOfAbsConv f = ⊤ → LSeries f = 0
-- Mathlib.Computability.DFA
DFA.inter_step : ∀ {α : Type u} {σ1 σ2 : Type v} (M1 : DFA α σ1) (M2 : DFA α σ2) (s : σ1 × σ2) (a : α),
  (M1.inter M2).step s a = (M1.step s.1 a, M2.step s.2 a)
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.CommMon.instHasInitial : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C], CategoryTheory.Limits.HasInitial (CategoryTheory.CommMon C)
-- Mathlib.Order.Hom.Bounded
TopHom.instPartialOrder.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Top α] [inst_1 : PartialOrder β] [inst_2 : Top β],
  TopHom.instPartialOrder = PartialOrder.lift DFunLike.coe ⋯
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
AddCircle.homeomorphCircle'_apply_mk : ∀ (x : ℝ), AddCircle.homeomorphCircle' ↑x = Circle.exp x
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- The sign of the angle between two linear combinations of two vectors is the sign of the
determinant of the factors in those combinations multiplied by the sign of the angle between the
two vectors.  -/
Orientation.oangle_sign_smul_add_smul_smul_add_smul : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x y : V) (r₁ r₂ r₃ r₄ : ℝ),
  (o.oangle (r₁ • x + r₂ • y) (r₃ • x + r₄ • y)).sign = SignType.sign (r₁ * r₄ - r₂ * r₃) * (o.oangle x y).sign
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.smul_right_def : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] (v : Valuation R Γ₀)
  {S : Type u_3} [inst_2 : SMul S R] (s : S) (x : WithVal v), s • x = WithVal.toVal v (s • x.ofVal)
-- Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
DerivedCategory.HomologySequence.epi_homologyMap_mor₂_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
    ∀ (n₀ n₁ : ℤ) (h : autoParam (n₀ + 1 = n₁) DerivedCategory.HomologySequence.epi_homologyMap_mor₂_iff._auto_1),
      CategoryTheory.Epi ((DerivedCategory.homologyFunctor C n₀).map T.mor₂) ↔
        DerivedCategory.HomologySequence.δ T n₀ n₁ h = 0
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
/-- Auxiliary definition for `normalize`.  -/
CategoryTheory.FreeMonoidalCategory.normalizeObj' : {C : Type u} →
  CategoryTheory.FreeMonoidalCategory C →
    CategoryTheory.Functor ((CategoryTheory.Discrete ∘ CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject) C)
      ((CategoryTheory.Discrete ∘ CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject) C)
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.size_singleL : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (l : Std.DTreeMap.Internal.Impl α β) (rk : α) (rv : β rk)
  (rl rr : Std.DTreeMap.Internal.Impl α β),
  (Std.DTreeMap.Internal.Impl.singleL k v l rk rv rl rr).size =
    (Std.DTreeMap.Internal.Impl.bin k v l (Std.DTreeMap.Internal.Impl.bin rk rv rl rr)).size
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Monad.Algebra.instCategoryStruct : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {T : CategoryTheory.Monad C} → CategoryTheory.CategoryStruct.{v₁, max u₁ v₁} T.Algebra
-- Mathlib.Algebra.Order.Hom.MonoidWithZero
OrderMonoidWithZeroHom.mk.injEq : ∀ {α : Type u_6} {β : Type u_7} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : MulZeroOneClass α]
  [inst_3 : MulZeroOneClass β] (toMonoidWithZeroHom : α →*₀ β) (monotone' : Monotone (↑toMonoidWithZeroHom).toFun)
  (toMonoidWithZeroHom_1 : α →*₀ β) (monotone'_1 : Monotone (↑toMonoidWithZeroHom_1).toFun),
  ({ toMonoidWithZeroHom := toMonoidWithZeroHom, monotone' := monotone' } =
      { toMonoidWithZeroHom := toMonoidWithZeroHom_1, monotone' := monotone'_1 }) =
    (toMonoidWithZeroHom = toMonoidWithZeroHom_1)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getKeyD_modify_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [Inhabited α] {k fallback : α} {f : β → β},
  (Std.ExtDHashMap.Const.modify m k f).getKeyD k fallback = if k ∈ m then k else fallback
-- Lean.Declaration
Lean.ReducibilityHints.getHeightEx : Lean.ReducibilityHints → UInt32
-- Mathlib.Topology.UniformSpace.UniformEmbedding
isUniformEmbedding_iff_isUniformInducing : ∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] [T0Space α] {f : α → β},
  IsUniformEmbedding f ↔ IsUniformInducing f
-- Mathlib.Probability.Kernel.Composition.CompProd
ProbabilityTheory.Kernel.fst_compProd : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel (α × β) γ)
  [ProbabilityTheory.IsSFiniteKernel κ] [ProbabilityTheory.IsMarkovKernel η], (κ.compProd η).fst = κ
-- Mathlib.Data.Fin.VecNotation
Matrix.cons_val_fin_one : ∀ {α : Type u} (x : α) (u : Fin 0 → α) (i : Fin 1), Matrix.vecCons x u i = x
-- Mathlib.Order.Concept
Concept.extent_sSup : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (S : Set (Concept α β r)),
  (sSup S).extent = lowerPolar r (⋂ i ∈ S, i.intent)
-- Mathlib.Algebra.Lie.Engel
/-- A Lie algebra `L` is said to be Engelian if a sufficient condition for any `L`-Lie module `M` to
be nilpotent is that the image of the map `L → End(M)` consists of nilpotent elements.

Engel's theorem `LieAlgebra.isEngelian_of_isNoetherian` states that any Noetherian Lie algebra is
Engelian.  -/
LieAlgebra.IsEngelian : (R : Type u₁) → (L : Type u₂) → [inst : CommRing R] → [inst_1 : LieRing L] → [LieAlgebra R L] → Prop
-- Mathlib.Analysis.Normed.Ring.Basic
/-- A seminormed commutative ring is a non-unital seminormed commutative ring.  -/
SeminormedCommRing.toNonUnitalSeminormedCommRing : {α : Type u_2} → [β : SeminormedCommRing α] → NonUnitalSeminormedCommRing α
-- Mathlib.Algebra.Group.Basic
mul_pow_sub_one : ∀ {M : Type u_4} [inst : Monoid M] {n : ℕ}, n ≠ 0 → ∀ (a : M), a * a ^ (n - 1) = a ^ n
-- Mathlib.Analysis.Normed.Group.Uniform
LipschitzOnWith.norm_neg_add_le_of_le : ∀ {E : Type u_2} {F : Type u_3} [inst : SeminormedAddGroup E] [inst_1 : SeminormedAddGroup F] {s : Set E} {a b : E}
  {r : ℝ} {f : E → F} {C : NNReal}, LipschitzOnWith C f s → a ∈ s → b ∈ s → ‖-a + b‖ ≤ r → ‖-f a + f b‖ ≤ ↑C * r
-- Mathlib.Data.Finset.Option
Finset.eraseNone_union : ∀ {α : Type u_1} [inst : DecidableEq (Option α)] [inst_1 : DecidableEq α] (s t : Finset (Option α)),
  Finset.eraseNone (s ∪ t) = Finset.eraseNone s ∪ Finset.eraseNone t
-- Aesop.Script.SScript
Aesop.Script.SScript.focusAndSolve.injEq : ∀ (goalPos : ℕ) (here tail : Aesop.Script.SScript) (goalPos_1 : ℕ) (here_1 tail_1 : Aesop.Script.SScript),
  (Aesop.Script.SScript.focusAndSolve goalPos here tail = Aesop.Script.SScript.focusAndSolve goalPos_1 here_1 tail_1) =
    (goalPos = goalPos_1 ∧ here = here_1 ∧ tail = tail_1)
-- Mathlib.Analysis.InnerProductSpace.PiL2
EuclideanSpace.real_norm_sq_eq : ∀ {n : Type u_7} [inst : Fintype n] (x : EuclideanSpace ℝ n), ‖x‖ ^ 2 = ∑ i, x.ofLp i ^ 2
-- Mathlib.Algebra.Group.AddChar
AddChar.zsmul_apply : ∀ {A : Type u_1} {M : Type u_2} [inst : AddCommGroup A] [inst_1 : DivisionCommMonoid M] (n : ℤ) (ψ : AddChar A M)
  (a : A), (n • ψ) a = ψ a ^ n
-- Mathlib.Order.Filter.Prod
Filter.prod_inj : ∀ {α : Type u_1} {β : Type u_2} {f₁ f₂ : Filter α} {g₁ g₂ : Filter β} [f₁.NeBot] [g₁.NeBot],
  f₁ ×ˢ g₁ = f₂ ×ˢ g₂ ↔ f₁ = f₂ ∧ g₁ = g₂
-- Mathlib.CategoryTheory.Category.ReflQuiv
CategoryTheory.Cat.FreeRefl.quotientFunctor_map_nil : ∀ {V : Type u_1} [inst : CategoryTheory.ReflQuiver V] (x : CategoryTheory.Paths V),
  (CategoryTheory.Cat.FreeRefl.quotientFunctor V).map Quiver.Path.nil =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.Cat.FreeRefl.quotientFunctor V).obj x)
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
/-- A non-unital subsemiring of a `NonUnitalNonAssocSemiring` inherits a
`NonUnitalNonAssocSemiring` structure  -/
NonUnitalSubsemiringClass.toNonUnitalNonAssocSemiring : {R : Type u} →
  {S : Type v} →
    [inst : NonUnitalNonAssocSemiring R] →
      [inst_1 : SetLike S R] → [NonUnitalSubsemiringClass S R] → (s : S) → NonUnitalNonAssocSemiring ↥s
-- Mathlib.Topology.Constructions
Finset.continuous_restrict₂_apply : ∀ {X : Type u} {Z : Type u_1} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Z] {s t : Finset X} (hst : s ⊆ t)
  {f : ↥t → Z}, Continuous f → Continuous (Finset.restrict₂ hst f)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Images
CategoryTheory.PreservesImage.hom_comp_map_image_ι_assoc : ∀ {A : Type u₁} {B : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Limits.HasEqualizers A] [inst_3 : CategoryTheory.Limits.HasImages A]
  [inst_4 : CategoryTheory.StrongEpiCategory B] [inst_5 : CategoryTheory.Limits.HasImages B]
  (L : CategoryTheory.Functor A B)
  [inst_6 :
    ∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) L]
  [inst_7 :
    ∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) L]
  {X Y : A} (f : X ⟶ Y) {Z : B} (h : L.obj Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.PreservesImage.iso L f).hom
      (CategoryTheory.CategoryStruct.comp (L.map (CategoryTheory.Limits.image.ι f)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι (L.map f)) h
-- Mathlib.Control.Monad.Cont
instMonadContWriterTOfMonadOfMonoid : {m : Type u → Type v} → (ω : Type u) → [Monad m] → [Monoid ω] → [MonadCont m] → MonadCont (WriterT ω m)
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.CommMon.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] [inst_3 : SizeOf C] (X : C) [mon : CategoryTheory.MonObj X]
  [comm : CategoryTheory.IsCommMonObj X],
  sizeOf { X := X, mon := mon, comm := comm } = 1 + sizeOf X + sizeOf mon + sizeOf comm
-- Mathlib.Tactic.Determinant.Bird.Meta
Mathlib.Tactic.Determinant.ReifiedBirdDet.mk : {u : Lean.Level} →
  {α : Q(Type u)} →
    (rα : Q(CommRing «$α»)) → Mathlib.Tactic.Determinant.Ctx rα → Mathlib.Tactic.Determinant.ReifiedBirdDet
-- Mathlib.Topology.VectorBundle.Hom
Bundle.ContinuousLinearMap.memTrivializationAtlas : ∀ {𝕜₁ : Type u_1} [inst : NontriviallyNormedField 𝕜₁] {𝕜₂ : Type u_2} [inst_1 : NontriviallyNormedField 𝕜₂]
  (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} {F₁ : Type u_4} [inst_2 : NormedAddCommGroup F₁] [inst_3 : NormedSpace 𝕜₁ F₁]
  {E₁ : B → Type u_5} [inst_4 : (x : B) → AddCommGroup (E₁ x)] [inst_5 : (x : B) → Module 𝕜₁ (E₁ x)]
  [inst_6 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_6} [inst_7 : NormedAddCommGroup F₂]
  [inst_8 : NormedSpace 𝕜₂ F₂] {E₂ : B → Type u_7} [inst_9 : (x : B) → AddCommGroup (E₂ x)]
  [inst_10 : (x : B) → Module 𝕜₂ (E₂ x)] [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [inst_12 : TopologicalSpace B] (e₁ : Bundle.Trivialization F₁ Bundle.TotalSpace.proj)
  (e₂ : Bundle.Trivialization F₂ Bundle.TotalSpace.proj) [inst_13 : (x : B) → TopologicalSpace (E₁ x)]
  [inst_14 : FiberBundle F₁ E₁] [inst_15 : VectorBundle 𝕜₁ F₁ E₁] [inst_16 : (x : B) → TopologicalSpace (E₂ x)]
  [inst_17 : FiberBundle F₂ E₂] [inst_18 : VectorBundle 𝕜₂ F₂ E₂] [inst_19 : ∀ (x : B), IsTopologicalAddGroup (E₂ x)]
  [inst_20 : ∀ (x : B), ContinuousSMul 𝕜₂ (E₂ x)] [inst_21 : RingHomIsometric σ] [he₁ : MemTrivializationAtlas e₁]
  [he₂ : MemTrivializationAtlas e₂], MemTrivializationAtlas (Bundle.Trivialization.continuousLinearMap σ e₁ e₂)
-- Init.Data.String.Slice
String.Slice.SplitInclusiveIterator.instIteratorId : {ρ : Type} →
  {σ : String.Slice → Type} →
    [(s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)] →
      {pat : ρ} →
        [inst : String.Slice.Pattern.ToForwardSearcher pat σ] →
          {s : String.Slice} → Std.Iterator (String.Slice.SplitInclusiveIterator pat s) Id String.Slice
-- Mathlib.Data.Finset.Lattice.Fold
Multiset.mem_sup : ∀ {α : Type u_7} {β : Type u_8} [inst : DecidableEq β] {s : Finset α} {f : α → Multiset β} {x : β},
  x ∈ s.sup f ↔ ∃ v ∈ s, x ∈ f v
-- Mathlib.MeasureTheory.Group.FoelnerFilter
/-- The limit along an ultrafilter of the density of a set with respect to a sequence in `X`.  -/
IsAddFoelner.mean : {X : Type u_2} →
  [inst : MeasurableSpace X] → MeasureTheory.Measure X → {ι : Type u_3} → Ultrafilter ι → (ι → Set X) → Set X → ENNReal
-- Mathlib.GroupTheory.OrderOfElement
/-- See `Subgroup.closure_toSubmonoid_of_isOfFinOrder` for a version with weaker assumptions.  -/
Subgroup.closure_toSubmonoid_of_finite : ∀ {G : Type u_1} [inst : Group G] [Finite G] {s : Set G}, (Subgroup.closure s).toSubmonoid = Submonoid.closure s
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.coeffEquiv.eq_1 : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R],
  MonoidAlgebra.coeffEquiv =
    { toFun := MonoidAlgebra.coeff, invFun := MonoidAlgebra.ofCoeff, left_inv := ⋯, right_inv := ⋯ }
-- Init.Data.Vector.Lemmas
Vector.size_zero_iff_forall_not_mem : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n}, n = 0 ↔ ∀ (a : α), a ∉ xs
-- Mathlib.Data.Seq.Basic
Stream'.Seq.map_id : ∀ {α : Type u} (s : Stream'.Seq α), Stream'.Seq.map id s = s
-- Mathlib.Order.Monotone.Union
/-- If `f` is antitone both on `(-∞, a]` and `[a, ∞)`, then it is antitone on the whole line.  -/
AntitoneOn.Iic_union_Ici : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : Preorder β] {a : α} {f : α → β},
  AntitoneOn f (Set.Iic a) → AntitoneOn f (Set.Ici a) → Antitone f
-- Mathlib.LinearAlgebra.Matrix.IsDiag
Matrix.isDiag_smul_one : ∀ {α : Type u_1} (n : Type u_6) [inst : MulZeroOneClass α] [inst_1 : DecidableEq n] (k : α), (k • 1).IsDiag
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
/-- Given `F : Set.Iic j ⥤ C`, `i : J` such that `hi : i ≤ j`, this is the
cocone consisting of all maps `F.obj ⟨k, hk⟩ ⟶ F.obj ⟨i, hi⟩` for `k : J` such that `k < i`.  -/
CategoryTheory.SmallObject.coconeOfLE : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : PartialOrder J] →
        {j : J} →
          (F : CategoryTheory.Functor (↑(Set.Iic j)) C) →
            {i : J} → (hi : i ≤ j) → CategoryTheory.Limits.Cocone (CategoryTheory.SmallObject.restrictionLT F hi)
-- Mathlib.Algebra.MvPolynomial.Supported
/-- The isomorphism between the subalgebra of polynomials supported by `s` and
`MvPolynomial s R`.  -/
MvPolynomial.supportedEquivMvPolynomial : {σ : Type u_1} →
  {R : Type u} → [inst : CommSemiring R] → (s : Set σ) → ↥(MvPolynomial.supported R s) ≃ₐ[R] MvPolynomial (↑s) R
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey_eq_get_minKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {he : t ≠ ∅}, t.minKey he = t.minKey?.get ⋯
-- Mathlib.RingTheory.PowerSeries.Trunc
PowerSeries.trunc_zero' : ∀ {R : Type u_1} [inst : Semiring R] {f : PowerSeries R}, (PowerSeries.trunc 0) f = 0
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
/-- Action of `GL (Fin 2) ℝ` on the upper half-plane, with `GL(2, ℝ)⁺` acting by Moebius
transformations in the usual way, extended to all of `GL (Fin 2) ℝ` using complex conjugation.  -/
UpperHalfPlane.glAction : MulAction (GL (Fin 2) ℝ) UpperHalfPlane
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
/-- An `AffineMap k P1 P2` (notation: `P1 →ᵃ[k] P2`) is a map from `P1` to `P2` that
induces a corresponding linear map from `V1` to `V2`.  -/
AffineMap : (k : Type u_1) →
  {V1 : Type u_2} →
    (P1 : Type u_3) →
      {V2 : Type u_4} →
        (P2 : Type u_5) →
          [inst : Ring k] →
            [inst_1 : AddCommGroup V1] →
              [Module k V1] →
                [AddTorsor V1 P1] →
                  [inst_4 : AddCommGroup V2] →
                    [Module k V2] → [AddTorsor V2 P2] → Type (max (max (max u_2 u_3) u_4) u_5)
-- Mathlib.Topology.Partial
continuousWithinAt_iff_ptendsto_res : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y) {x : X}
  {s : Set X}, ContinuousWithinAt f s x ↔ Filter.PTendsto (PFun.res f s) (nhds x) (nhds (f x))
-- Init.Data.Function
/-- Transforms a two-parameter function into an equivalent function from pairs.

Examples:
* `Function.uncurry List.drop (1, ["a", "b", "c"]) = ["b", "c"]`
* `[("orange", 2), ("android", 3) ].map (Function.uncurry String.take) = ["or", "and"]`
 -/
Function.uncurry : {α : Type u_1} → {β : Type u_2} → {φ : Sort u_3} → (α → β → φ) → α × β → φ