mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.DirectSum.TensorProduct
/-- The linear equivalence `(⨁ i₁, M₁ i₁) ⊗ (⨁ i₂, M₂ i₂) ≃ (⨁ i₁, ⨁ i₂, M₁ i₁ ⊗ M₂ i₂)`, i.e.
"tensor product distributes over direct sum".  -/
TensorProduct.directSum : (R : Type u) →
  [inst : CommSemiring R] →
    (S : Type u_1) →
      [inst_1 : Semiring S] →
        [inst_2 : Algebra R S] →
          {ι₁ : Type v₁} →
            {ι₂ : Type v₂} →
              [DecidableEq ι₁] →
                [DecidableEq ι₂] →
                  (M₁ : ι₁ → Type w₁) →
                    (M₂ : ι₂ → Type w₂) →
                      [inst_5 : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)] →
                        [inst_6 : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)] →
                          [inst_7 : (i₁ : ι₁) → Module R (M₁ i₁)] →
                            [inst_8 : (i₂ : ι₂) → Module R (M₂ i₂)] →
                              [inst_9 : (i₁ : ι₁) → Module S (M₁ i₁)] →
                                [inst_10 : ∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)] →
                                  TensorProduct R (DirectSum ι₁ fun i₁ => M₁ i₁) (DirectSum ι₂ fun i₂ => M₂ i₂) ≃ₗ[S]
                                    DirectSum (ι₁ × ι₂) fun i => TensorProduct R (M₁ i.1) (M₂ i.2)
-- Mathlib.SetTheory.Ordinal.Basic
Cardinal.omega0_le_ord : ∀ {a : Cardinal.{u_1}}, Ordinal.omega0 ≤ a.ord ↔ Cardinal.aleph0 ≤ a
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitDisc.one_add_coe_ne_zero : ∀ (z : Complex.UnitDisc), 1 + ↑z ≠ 0
-- Std.Data.String.ToInt
String.Slice.toInt?_eq_none_iff : ∀ {s : String.Slice}, s.toInt? = none ↔ s.isInt = false
-- Plausible.Sampleable
Plausible.Array.sampleableExt : {α : Type u_1} → [Plausible.SampleableExt α] → Plausible.SampleableExt (Array α)
-- Mathlib.Algebra.Order.Group.Abs
mabs_div_mabs_le_mabs_div : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] (a b : G), |a|ₘ / |b|ₘ ≤ |a / b|ₘ
-- Mathlib.CategoryTheory.Functor.OfSequence
CategoryTheory.Functor.OfSequence.congr_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (i j : ℕ)
  (h : i = j),
  f i =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
      (CategoryTheory.CategoryStruct.comp (f j) (CategoryTheory.eqToHom ⋯))
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.IsBasis.closure_inter_isBasis_closure : ∀ {α : Type u_2} {M : Matroid α} {X I : Set α},
  M.IsBasis (X ∩ I) X → M.Indep I → M.IsBasis (M.closure X ∩ I) (M.closure X)
-- Mathlib.CategoryTheory.Comma.Basic
/-- `Comma.preLeft` is a particular case of `Comma.map`,
but with better definitional properties.  -/
CategoryTheory.Comma.preLeftIso : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    {B : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
        {T : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} T] →
            {C : Type u₄} →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} C] →
                (F : CategoryTheory.Functor C A) →
                  (L : CategoryTheory.Functor A T) →
                    (R : CategoryTheory.Functor B T) →
                      CategoryTheory.Comma.preLeft F L R ≅
                        CategoryTheory.Comma.map (F.comp L).rightUnitor.inv
                          (CategoryTheory.CategoryStruct.comp R.rightUnitor.hom R.leftUnitor.inv)
-- Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
HasFDerivAt.continuousAlternatingMapCompContinuousLinearMap : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {H : Type u_6}
  [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]
  [inst_7 : NormedAddCommGroup H] [inst_8 : NormedSpace 𝕜 H] {f : E → G [⋀^ι]→L[𝕜] H} {f' : E →L[𝕜] G [⋀^ι]→L[𝕜] H}
  {g : E → F →L[𝕜] G} {g' : E →L[𝕜] F →L[𝕜] G} {x : E} [inst_9 : Fintype ι] [inst_10 : DecidableEq ι],
  HasFDerivAt f f' x →
    HasFDerivAt g g' x →
      HasFDerivAt (fun x => (f x).compContinuousLinearMap (g x))
        (ContinuousAlternatingMap.compContinuousLinearMapCLM (g x) ∘SL f' +
          (f x).fderivCompContinuousLinearMap (g x) ∘SL g')
        x
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.refl_inverse : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C],
  CategoryTheory.Equivalence.refl.inverse = CategoryTheory.Functor.id C
-- Mathlib.Analysis.ODE.Gronwall
/-- If `f` and `g` are two exact solutions of the same ODE, then the distance between them
can't grow faster than exponentially. This is a simple corollary of Grönwall's inequality, and some
people call this Grönwall's inequality too.

This version assumes all inequalities to be true in some time-dependent set `s t`,
and assumes that the solutions never leave this set.  -/
dist_le_of_trajectories_ODE_of_mem : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {v : ℝ → E → E} {s : ℝ → Set E} {K : NNReal}
  {f g : ℝ → E} {a b δ : ℝ},
  (∀ t ∈ Set.Ico a b, LipschitzOnWith K (v t) (s t)) →
    ContinuousOn f (Set.Icc a b) →
      (∀ t ∈ Set.Ico a b, HasDerivWithinAt f (v t (f t)) (Set.Ici t) t) →
        (∀ t ∈ Set.Ico a b, f t ∈ s t) →
          ContinuousOn g (Set.Icc a b) →
            (∀ t ∈ Set.Ico a b, HasDerivWithinAt g (v t (g t)) (Set.Ici t) t) →
              (∀ t ∈ Set.Ico a b, g t ∈ s t) →
                dist (f a) (g a) ≤ δ → ∀ t ∈ Set.Icc a b, dist (f t) (g t) ≤ δ * Real.exp (↑K * (t - a))
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.imageOneHom.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : One α] [inst_1 : DecidableEq β] [inst_2 : One β]
  [inst_3 : FunLike F α β] [inst_4 : OneHomClass F α β] (f : F),
  Finset.imageOneHom f = { toFun := Finset.image ⇑f, map_one' := ⋯ }
-- Mathlib.AlgebraicTopology.RelativeCellComplex.Basic
HomotopicalAlgebra.RelativeCellComplex.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w'} [inst_1 : LinearOrder J] [inst_2 : OrderBot J]
  [inst_3 : SuccOrder J] [inst_4 : WellFoundedLT J] {α : J → Type t} {A B : (j : J) → α j → C}
  {basicCell : (j : J) → (i : α j) → A j i ⟶ B j i} {X Y : C} {f : X ⟶ Y}
  (toTransfiniteCompositionOfShape : CategoryTheory.TransfiniteCompositionOfShape J f)
  (attachCells :
    (j : J) →
      ¬IsMax j →
        HomotopicalAlgebra.AttachCells (basicCell j) (toTransfiniteCompositionOfShape.F.map (CategoryTheory.homOfLE ⋯)))
  (toTransfiniteCompositionOfShape_1 : CategoryTheory.TransfiniteCompositionOfShape J f)
  (attachCells_1 :
    (j : J) →
      ¬IsMax j →
        HomotopicalAlgebra.AttachCells (basicCell j)
          (toTransfiniteCompositionOfShape_1.F.map (CategoryTheory.homOfLE ⋯))),
  ({ toTransfiniteCompositionOfShape := toTransfiniteCompositionOfShape, attachCells := attachCells } =
      { toTransfiniteCompositionOfShape := toTransfiniteCompositionOfShape_1, attachCells := attachCells_1 }) =
    (toTransfiniteCompositionOfShape = toTransfiniteCompositionOfShape_1 ∧ attachCells ≍ attachCells_1)
-- Lean.Elab.PreDefinition.Basic
_private.Lean.Elab.PreDefinition.Basic.0.Lean.Elab.reportTheoremDiag : Lean.TheoremVal → Lean.Elab.TermElabM Unit
-- Init.Data.Int.Order
Int.lt_trans : ∀ {a b c : ℤ}, a < b → b < c → a < c
-- Mathlib.Data.Set.Lattice
Set.union_distrib_iInter₂_left : ∀ {α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_8} (s : Set α) (t : (i : ι) → κ i → Set α),
  s ∪ ⋂ i, ⋂ j, t i j = ⋂ i, ⋂ j, s ∪ t i j
-- Mathlib.LinearAlgebra.Prod
LinearMap.kerComplementEquivRange_apply_coe : ∀ {R : Type u_3} {M : Type u_4} {M₂ : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂] (f : M →ₗ[R] M₂) {C : Submodule R M} (h : IsCompl C f.ker) (x : ↥C),
  ↑((f.kerComplementEquivRange h) x) = f ↑x
-- Mathlib.Algebra.Order.Floor.Ring
Int.fract_eq_zero_iff : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] {a : R},
  Int.fract a = 0 ↔ a ∈ Set.range Int.cast
-- Init.Data.Range.Polymorphic.PRange
/-- This type class ensures that the intersection according to `Rco.HasRcoIntersection`
of two ranges contains exactly those elements that are contained in both ranges.
 -/
Std.Rco.LawfulRcoIntersection : (α : Type w) → [LT α] → [LE α] → [Std.Rco.HasRcoIntersection α] → Prop
-- Mathlib.Combinatorics.Digraph.Orientation
/-- Orientation-forgetting map from `Digraph` to `SimpleGraph` that gives an unoriented edge if
either orientation is present.
 -/
Digraph.toSimpleGraphInclusive : {V : Type u_1} → Digraph V → SimpleGraph V
-- Mathlib.Analysis.Normed.Algebra.MatrixExponential
Matrix.exp_add_of_commute : ∀ {m : Type u_1} {𝔸 : Type u_5} [inst : Fintype m] [inst_1 : DecidableEq m] [inst_2 : NormedRing 𝔸] [NormedAlgebra ℚ 𝔸]
  [CompleteSpace 𝔸] (A B : Matrix m m 𝔸), Commute A B → NormedSpace.exp (A + B) = NormedSpace.exp A * NormedSpace.exp B
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.StructureSheaf.algebraMap_germ_assoc : ∀ {R : Type u} [inst : CommRing R] (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R))
  (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) (hxU : x ∈ U) {Z : CommRingCat}
  (h : (AlgebraicGeometry.structurePresheafInCommRingCat R).stalk x ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CommRingCat.ofHom (algebraMap R ((AlgebraicGeometry.structureSheafInType R R).obj.obj (Opposite.op U))))
      (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.structurePresheafInCommRingCat R).germ U x hxU) h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.StructureSheaf.toStalk R x) h
-- Init.Data.UInt.Lemmas
USize.ofFin_div : ∀ (a b : Fin USize.size), USize.ofFin (a / b) = USize.ofFin a / USize.ofFin b
-- Mathlib.Algebra.Group.UniqueProds.Basic
TwoUniqueProds.instMulOpposite : ∀ {G : Type u} [inst : Mul G] [h : TwoUniqueProds G], TwoUniqueProds Gᵐᵒᵖ
-- Mathlib.Algebra.FreeMonoid.Count
/-- `List.countP` lifted to free additive monoids  -/
FreeAddMonoid.countP' : {α : Type u_1} → (p : α → Prop) → [DecidablePred p] → FreeAddMonoid α → ℕ
-- Mathlib.Algebra.BigOperators.Fin
Fin.sum_Ioo_castAdd : ∀ {M : Type u_2} [inst : AddCommMonoid M] {n : ℕ} (m : ℕ) (f : Fin (n + m) → M) (a b : Fin n),
  ∑ i ∈ Finset.Ioo (Fin.castAdd m a) (Fin.castAdd m b), f i = ∑ i ∈ Finset.Ioo a b, f (Fin.castAdd m i)
-- Mathlib.Data.ULift
PLift.up_inj : ∀ {α : Sort u} {x y : α}, { down := x } = { down := y } ↔ x = y
-- Batteries.Data.String.Lemmas
String.rawEndPos_asString : ∀ (cs : List Char), (String.ofList cs).rawEndPos = { byteIdx := String.utf8Len cs }
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
CovariantDerivative.mk.inj : ∀ {𝕜 : 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} {F : Type u_5} {inst_6 : NormedAddCommGroup F}
  {inst_7 : NormedSpace 𝕜 F} {V : M → Type u_6} {inst_8 : TopologicalSpace (Bundle.TotalSpace F V)}
  {inst_9 : (x : M) → AddCommGroup (V x)} {inst_10 : (x : M) → Module 𝕜 (V x)}
  {inst_11 : (x : M) → TopologicalSpace (V x)} {inst_12 : ∀ (x : M), IsTopologicalAddGroup (V x)}
  {inst_13 : ∀ (x : M), ContinuousSMul 𝕜 (V x)} {inst_14 : FiberBundle F V}
  {toFun : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x}
  {isCovariantDerivativeOnUniv : IsCovariantDerivativeOn F toFun}
  {toFun_1 : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x}
  {isCovariantDerivativeOnUniv_1 : IsCovariantDerivativeOn F toFun_1},
  { toFun := toFun, isCovariantDerivativeOnUniv := isCovariantDerivativeOnUniv } =
      { toFun := toFun_1, isCovariantDerivativeOnUniv := isCovariantDerivativeOnUniv_1 } →
    toFun = toFun_1
-- Mathlib.Tactic.Linarith.Lemmas
Mathlib.Tactic.Linarith.le_of_eq_of_le : ∀ {α : Type u} [inst : Semiring α] [inst_1 : PartialOrder α] {a b : α}, a = 0 → b ≤ 0 → a + b ≤ 0
-- Mathlib.RingTheory.Extension.Cotangent.Basic
/-- The first homology of the (naive) cotangent complex of `S` over `R`,
induced by a given presentation `0 → I → P → R → 0`,
defined as the kernel of `I/I² → S ⊗[P] Ω[P⁄R]`.
 -/
Algebra.Extension.H1Cotangent : {R : Type u} →
  {S : Type v} → [inst : CommRing R] → [inst_1 : CommRing S] → [inst_2 : Algebra R S] → Algebra.Extension R S → Type w
-- Mathlib.CategoryTheory.Functor.FunctorHom
CategoryTheory.Functor.homObjFunctor_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (F G : CategoryTheory.Functor C D) {A A' : (CategoryTheory.Functor C (Type w))ᵒᵖ} (f : A ⟶ A'),
  (F.homObjFunctor G).map f =
    TypeCat.ofHom fun x =>
      { app := fun X a => x.app X ((CategoryTheory.ConcreteCategory.hom (f.unop.app X)) a), naturality := ⋯ }
-- Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris
CategoryTheory.GrothendieckTopology.MayerVietorisSquare.fromBiprod.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : CategoryTheory.HasWeakSheafify J (Type v)] [inst_2 : CategoryTheory.HasSheafify J AddCommGrpCat]
  [inst_3 : CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)] (S : J.MayerVietorisSquare)
  (F : CategoryTheory.Sheaf J AddCommGrpCat) (n : ℕ),
  S.fromBiprod F n =
    CategoryTheory.Limits.biprod.desc ((F.cohomologyPresheaf n).map S.f₁₂.op) (-(F.cohomologyPresheaf n).map S.f₁₃.op)
-- Init.Data.Vector.Lemmas
Vector.mk_zip_mk : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {as : Array α} {bs : Array β} (h : as.size = n) (h' : bs.size = n),
  (Vector.mk as h).zip (Vector.mk bs h') = Vector.mk (as.zip bs) ⋯
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.MapBijective
CategoryTheory.Functor.mapExt_bijective_of_preservesInjectiveObjects : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] [inst_3 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.Additive] [inst_5 : CategoryTheory.Limits.PreservesFiniteLimits F]
  [inst_6 : CategoryTheory.Limits.PreservesFiniteColimits F] [F.Full] [F.Faithful] [inst_9 : CategoryTheory.HasExt C]
  [inst_10 : CategoryTheory.HasExt D] [CategoryTheory.EnoughInjectives C] [F.PreservesInjectiveObjects] (X Y : C)
  (n : ℕ), Function.Bijective ⇑(F.mapExtAddHom X Y n)
-- Init.Data.UInt.Lemmas
USize.ofNat_mul : ∀ (a b : ℕ), USize.ofNat (a * b) = USize.ofNat a * USize.ofNat b
-- Mathlib.Topology.Gluing
TopCat.GlueData.ι_injective : ∀ (D : TopCat.GlueData) (i : D.J), Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (D.ι i))
-- Mathlib.LinearAlgebra.TensorProduct.Basic
TensorProduct.curry_apply : ∀ {R : Type u_1} {R₂ : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7}
  {N : Type u_8} {P₂ : Type u_17} [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : AddCommMonoid P₂]
  [inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : Module R₂ P₂] (f : TensorProduct R M N →ₛₗ[σ₁₂] P₂) (m : M)
  (n : N), ((TensorProduct.curry f) m) n = f (m ⊗ₜ[R] n)
-- Mathlib.Control.Bifunctor
LawfulBifunctor.bimap_comp_bimap : ∀ {F : Type u₀ → Type u₁ → Type u₂} {inst : Bifunctor F} [self : LawfulBifunctor F] {α₀ α₁ α₂ : Type u₀}
  {β₀ β₁ β₂ : Type u₁} (f : α₀ → α₁) (f' : α₁ → α₂) (g : β₀ → β₁) (g' : β₁ → β₂),
  bimap f' g' ∘ bimap f g = bimap (f' ∘ f) (g' ∘ g)
-- Mathlib.Data.List.Zip
List.zip_swap : ∀ {α : Type u} {β : Type u_1} (l₁ : List α) (l₂ : List β), List.map Prod.swap (l₁.zip l₂) = l₂.zip l₁
-- Mathlib.Computability.StateTransition
StateTransition.Reaches₁.to₀ : ∀ {σ : Type u_1} {f : σ → Option σ} {a b : σ}, StateTransition.Reaches₁ f a b → StateTransition.Reaches₀ f a b
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.realizeValue.unsafe_impl_4 : {α : Type u_1} → [inst : BEq α] → [inst_1 : Hashable α] → NonScalar → Lean.PHashMap α (Task Dynamic)
-- Mathlib.Combinatorics.Quiver.ConnectedComponent
Quiver.stronglyConnectedComponent_singleton_iff : ∀ {V : Type u_2} [inst : Quiver V] (v : V),
  (∀ (w : V), Quiver.StronglyConnectedComponent.mk w = Quiver.StronglyConnectedComponent.mk v → w = v) ↔
    ∀ (w : V), w ≠ v → ¬(Nonempty (Quiver.Path v w) ∧ Nonempty (Quiver.Path w v))
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
/-- To show a category is an `InitialMonoClass` it suffices to show every morphism out of the
initial object is a monomorphism.  -/
CategoryTheory.Limits.InitialMonoClass.of_initial : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasInitial C],
  (∀ (X : C), CategoryTheory.Mono (CategoryTheory.Limits.initial.to X)) → CategoryTheory.Limits.InitialMonoClass C
-- Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
CategoryTheory.MonoidalCategory.IsPushout.whiskerLeft_inl_isoPushout_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {Z X Y P : C}
  {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (hP : CategoryTheory.IsPushout f g inl inr)
  [inst_2 : CategoryTheory.Limits.HasPushout f g] {Q Z_1 : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Q (CategoryTheory.Limits.pushout f g) ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q inl)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q hP.isoPushout.hom) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q (CategoryTheory.Limits.pushout.inl f g)) h
-- Std.Async.System
Std.Async.System.instInhabitedUserId.default : Std.Async.System.UserId
-- Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells
/-- `cofan₂` is colimit  -/
HomotopicalAlgebra.AttachCells.isColimit₂ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {α : Type t} →
      {A B : α → C} →
        {g : (a : α) → A a ⟶ B a} →
          {X₁ X₂ : C} →
            {f : X₁ ⟶ X₂} → (self : HomotopicalAlgebra.AttachCells g f) → CategoryTheory.Limits.IsColimit self.cofan₂
-- Mathlib.Data.Set.FiniteExhaustion
Set.FiniteExhaustion.mono : ∀ {α : Type u_1} {s : Set α} (K : s.FiniteExhaustion) {m n : ℕ}, m ≤ n → K m ⊆ K n
-- Mathlib.Order.CompletePartialOrder
CompletePartialOrder.mk : {α : Type u_4} →
  [toPartialOrder : PartialOrder α] →
    [toSupSet : SupSet α] →
      [toOrderBot : OrderBot α] →
        (∀ (d : Set α), DirectedOn (fun x1 x2 => x1 ≤ x2) d → IsLUB d (sSup d)) → CompletePartialOrder α
-- Mathlib.Order.WithBot
WithBot.eq_of_forall_le_coe_iff : ∀ {α : Type u_1} [inst : PartialOrder α] {x y : WithBot α} [NoBotOrder α], (∀ (a : α), x ≤ ↑a ↔ y ≤ ↑a) → x = y
-- Mathlib.Algebra.GroupWithZero.WithZero
/-- `Mᵐ⁰` is notation for `WithZero (Multiplicative M)`.

This naturally shows up as the codomain of valuations in valuation theory.  -/
WithZero.«term_ᵐ⁰» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Lie.CartanExists
LieAlgebra.engel_isBot_of_isMin.lieCharpoly_map_eval : ∀ {R : Type u_2} {L : Type u_3} (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : Module.Finite R L] [inst_8 : Module.Free R L] [inst_9 : Module.Finite R M] [inst_10 : Module.Free R M]
  (x y : L) (r : R),
  Polynomial.map (Polynomial.evalRingHom r) (LieAlgebra.engel_isBot_of_isMin.lieCharpoly✝ R M x y) =
    LinearMap.charpoly ((LieModule.toEnd R L M) (r • y + x))
-- Mathlib.Algebra.DirectSum.Basic
/-- If two additive homomorphisms from `⨁ i, β i` are equal on each `of β i y`,
then they are equal.

See note [partially-applied ext lemmas].  -/
DirectSum.addHom_ext' : ∀ {ι : Type v} {β : ι → Type w} [inst : (i : ι) → AddCommMonoid (β i)] [inst_1 : DecidableEq ι] {γ : Type u_1}
  [inst_2 : AddZeroClass γ] ⦃f g : (DirectSum ι fun i => β i) →+ γ⦄,
  (∀ (i : ι), f.comp (DirectSum.of β i) = g.comp (DirectSum.of β i)) → f = g
-- Mathlib.Data.Set.Restrict
/-- **Alias** of `Set.domRestrict_eq_iff`. -/
Set.restrict_eq_iff : ∀ {α : Type u_1} {π : α → Type u_6} {f : (a : α) → π a} {s : Set α} {g : (a : ↑s) → π ↑a},
  s.domRestrict f = g ↔ ∀ (a : α) (ha : a ∈ s), f a = g ⟨a, ha⟩
-- Mathlib.RingTheory.ZariskisMainTheorem
Subalgebra.val.eq_1 : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (S : Subalgebra R A),
  S.val = { toFun := Subtype.val, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }
-- Mathlib.Topology.ContinuousMap.Basic
ContinuousMap.instInhabited : (α : Type u_1) →
  {β : Type u_2} → [inst : TopologicalSpace α] → [inst_1 : TopologicalSpace β] → [Inhabited β] → Inhabited C(α, β)
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
/-- The distinguished triangle `(t.truncLT n).obj A ⟶ A ⟶ (t.truncGE n).obj A ⟶ ...`
as a functor `C ⥤ Triangle C` when `t` is a `t`-structure on a pretriangulated
category `C` and `n : ℤ`.  -/
CategoryTheory.Triangulated.TStructure.triangleLTGE : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              CategoryTheory.Triangulated.TStructure C →
                ℤ → CategoryTheory.Functor C (CategoryTheory.Pretriangulated.Triangle C)
-- Mathlib.Logic.Denumerable
_private.Mathlib.Logic.Denumerable.0.Nat.Subtype.toFunAux_eq : ∀ {s : Set ℕ} [inst : DecidablePred fun x => x ∈ s] (x : ↑s),
  Nat.Subtype.toFunAux✝ x = {y ∈ Finset.range ↑x | y ∈ s}.card
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryGT.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] (k k_1 : α) (e_k : k = k_1)
  (t t_1 : Std.DTreeMap.Internal.Impl α β) (e_t : t = t_1) (ho : t.Ordered) (he : ∃ a ∈ t, compare a k = Ordering.gt),
  Std.DTreeMap.Internal.Impl.getEntryGT k t ho he = Std.DTreeMap.Internal.Impl.getEntryGT k_1 t_1 ⋯ ⋯
-- Init.System.IO
/-- The process's exit code.  -/
IO.Process.Output.exitCode : IO.Process.Output → UInt32
-- Mathlib.Analysis.Normed.Module.ContinuousInverse
ContinuousLinearMap.HasLeftInverse.comp : ∀ {R : Type u_1} [inst : Semiring R] {E : Type u_2} {F : Type u_4} {G : Type u_6} [inst_1 : TopologicalSpace E]
  [inst_2 : AddCommMonoid E] [inst_3 : Module R E] [inst_4 : TopologicalSpace F] [inst_5 : AddCommMonoid F]
  [inst_6 : Module R F] {f : E →L[R] F} [inst_7 : TopologicalSpace G] [inst_8 : AddCommMonoid G] [inst_9 : Module R G]
  {g : F →L[R] G}, g.HasLeftInverse → f.HasLeftInverse → (g ∘SL f).HasLeftInverse
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.subst1 : ℤ →
  Lean.Meta.Grind.Arith.Linear.EqCnstr →
    Lean.Meta.Grind.Arith.Linear.DiseqCnstr → Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof
-- Mathlib.Topology.Algebra.Module.Equiv
/-- Create a `ContinuousLinearEquiv` from two `ContinuousLinearMap`s that are
inverse of each other, in the `ContinuousLinearMap.comp` sense. See also `equivOfInverse`.
*ToDo*: Improve the naiming to make it match `LinearMap.ofLinear`  -/
ContinuousLinearEquiv.equivOfInverse' : {R₁ : Type u_1} →
  {R₂ : Type u_2} →
    [inst : Semiring R₁] →
      [inst_1 : Semiring R₂] →
        {σ₁₂ : R₁ →+* R₂} →
          {σ₂₁ : R₂ →+* R₁} →
            [inst_2 : RingHomInvPair σ₁₂ σ₂₁] →
              [inst_3 : RingHomInvPair σ₂₁ σ₁₂] →
                {M₁ : Type u_4} →
                  [inst_4 : TopologicalSpace M₁] →
                    [inst_5 : AddCommMonoid M₁] →
                      {M₂ : Type u_5} →
                        [inst_6 : TopologicalSpace M₂] →
                          [inst_7 : AddCommMonoid M₂] →
                            [inst_8 : Module R₁ M₁] →
                              [inst_9 : Module R₂ M₂] →
                                (f₁ : M₁ →SL[σ₁₂] M₂) →
                                  (f₂ : M₂ →SL[σ₂₁] M₁) →
                                    f₁ ∘SL f₂ = ContinuousLinearMap.id R₂ M₂ →
                                      f₂ ∘SL f₁ = ContinuousLinearMap.id R₁ M₁ → M₁ ≃SL[σ₁₂] M₂