mathlib-initiative/mathlib-types huggingface dataset:
-- Aesop.RuleSet.Member
Aesop.BaseRuleSetMember.safeForwardRule.sizeOf_spec : ∀ (r₁ : Aesop.ForwardRule) (r₂ : Aesop.SafeRule),
  sizeOf (Aesop.BaseRuleSetMember.safeForwardRule r₁ r₂) = 1 + sizeOf r₁ + sizeOf r₂
-- Std.Time.Duration
Std.Time.instOfNatDuration : {n : ℕ} → OfNat Std.Time.Duration n
-- Mathlib.Data.Subtype
Subtype.restrict_apply : ∀ {α : Sort u_5} {β : α → Type u_4} (f : (x : α) → β x) (p : α → Prop) (x : Subtype p), Subtype.restrict p f x = f ↑x
-- Std.Sync.Notify
Std.Notify.State.mk.injEq : ∀ (consumers consumers_1 : Std.Queue (Std.Notify.Consumer Unit)),
  ({ consumers := consumers } = { consumers := consumers_1 }) = (consumers = consumers_1)
-- Std.Data.HashSet.Lemmas
Std.HashSet.mem_toArray : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [LawfulBEq α] {k : α}, k ∈ m.toArray ↔ k ∈ m
-- Mathlib.CategoryTheory.Sites.Point.Map
/-- Relation between the fiber functors on presheaves for the points `Φ.map F K`
and `Φ`.  -/
CategoryTheory.GrothendieckTopology.Point.presheafFiberMapObjIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} D] →
        {J : CategoryTheory.GrothendieckTopology C} →
          (Φ : J.Point) →
            (F : CategoryTheory.Functor C D) →
              (K : CategoryTheory.GrothendieckTopology D) →
                [inst_2 : F.IsCocontinuous J K] →
                  [inst_3 : CategoryTheory.LocallySmall.{w, v', u'} D] →
                    {A : Type u''} →
                      [inst_4 : CategoryTheory.Category.{v'', u''} A] →
                        [inst_5 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] →
                          (P : CategoryTheory.Functor Dᵒᵖ A) →
                            (Φ.map F K).presheafFiber.obj P ≅ Φ.presheafFiber.obj (F.op.comp P)
-- Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
CliffordAlgebra.involuteEquiv_symm_apply : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (a : CliffordAlgebra Q), CliffordAlgebra.involuteEquiv.symm a = CliffordAlgebra.involute a
-- Mathlib.MeasureTheory.Measure.Haar.Extension
/-- If `φ : A →+ B` and `ψ : B →+ C` define a short exact sequence of additive
topological groups, then we can define a Haar measure on `B` induced by the Haar measures on `A`
and `C`.  -/
TopologicalAddGroup.IsSES.inducedMeasure : {A : Type u_1} →
  {B : Type u_2} →
    {C : Type u_3} →
      [inst : AddGroup A] →
        [inst_1 : AddGroup B] →
          [inst_2 : AddGroup C] →
            [inst_3 : TopologicalSpace A] →
              [inst_4 : TopologicalSpace B] →
                [inst_5 : TopologicalSpace C] →
                  {φ : A →+ B} →
                    {ψ : B →+ C} →
                      TopologicalAddGroup.IsSES φ ψ →
                        [IsTopologicalAddGroup A] →
                          [IsTopologicalAddGroup B] →
                            [inst_8 : MeasurableSpace A] →
                              [BorelSpace A] →
                                (μA : MeasureTheory.Measure A) →
                                  [hμA : μA.IsAddHaarMeasure] →
                                    [IsTopologicalAddGroup C] →
                                      [LocallyCompactSpace B] →
                                        [inst : MeasurableSpace C] →
                                          [BorelSpace C] →
                                            (μC : MeasureTheory.Measure C) →
                                              [hμC : μC.IsAddHaarMeasure] →
                                                [T2Space B] →
                                                  [inst : MeasurableSpace B] → [BorelSpace B] → MeasureTheory.Measure B
-- Init.Data.SInt.Lemmas
Int32.toISize_lt : ∀ {a b : Int32}, a.toISize < b.toISize ↔ a < b
-- Mathlib.Data.List.Sort
OrderEmbedding.sortedLT_listMap : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (e : α ↪o β) {l : List α},
  (List.map (⇑e) l).SortedLT ↔ l.SortedLT
-- Mathlib.Topology.MetricSpace.Algebra
/-- If a scalar is central, then its right action is bounded when its left action is.  -/
IsBoundedSMul.op : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] [inst_2 : Zero α]
  [inst_3 : Zero β] [inst_4 : SMul α β] [IsBoundedSMul α β] [inst_6 : SMul αᵐᵒᵖ β] [IsCentralScalar α β],
  IsBoundedSMul αᵐᵒᵖ β
-- Mathlib.Order.KrullDimension
Order.coheight_toDual : ∀ {α : Type u_1} [inst : Preorder α] (x : α), Order.coheight (OrderDual.toDual x) = Order.height x
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
SzemerediRegularity.chunk.congr_simp : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {P P_1 : Finpartition Finset.univ} (e_P : P = P_1)
  (hP : P.IsEquipartition) (G G_1 : SimpleGraph α),
  G = G_1 →
    ∀ {inst_2 : DecidableRel G.Adj} [inst_3 : DecidableRel G_1.Adj] (ε ε_1 : ℝ),
      ε = ε_1 →
        ∀ {U : Finset α} (hU : U ∈ P.parts), SzemerediRegularity.chunk hP G ε hU = SzemerediRegularity.chunk ⋯ G_1 ε_1 ⋯
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- The action of a monoid object on itself.  -/
CategoryTheory.ModObj.regular : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (M : C) → [inst_2 : CategoryTheory.MonObj M] → CategoryTheory.ModObj M M
-- Mathlib.RingTheory.WittVector.IsPoly
WittVector.IsPoly₂.ext : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)]
  {f g : ⦃R : Type u⦄ → [CommRing R] → WittVector p R → WittVector p R → WittVector p R},
  WittVector.IsPoly₂ p f →
    WittVector.IsPoly₂ p g →
      (∀ (R : Type u) [_Rcr : CommRing R] (x y : WittVector p R) (n : ℕ),
          (WittVector.ghostComponent n) (f x y) = (WittVector.ghostComponent n) (g x y)) →
        ∀ (R : Type u) [_Rcr : CommRing R] (x y : WittVector p R), f x y = g x y
-- Std.Data.ExtTreeMap.Basic
/-- Tries to retrieve the smallest key in the tree map, panicking if the map is empty.
 -/
Std.ExtTreeMap.minKey! : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → [Inhabited α] → Std.ExtTreeMap α β cmp → α
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
Subgroup.unop_top : ∀ {G : Type u_2} [inst : Group G], ⊤.unop = ⊤
-- Mathlib.Condensed.Light.Sequence
_private.Mathlib.Condensed.Light.Sequence.0.InternalProjectivityProof.y_surjective : ∀ {S : Type u_1} {T : Type u_2} {X : Type u_3} (π : T → S × OnePoint X),
  Function.Surjective π → Function.Surjective (InternalProjectivityProof.y✝ π)
-- Init.Data.String.PosRaw
String.Pos.Raw.zero_add_char_eq : ∀ (c : Char), 0 + c = { byteIdx := c.utf8Size }
-- Std.Time.Date.Unit.Day
Std.Time.Day.instToStringOffset : ToString Std.Time.Day.Offset
-- Lean.Compiler.Options
Lean.Compiler.compiler.ignoreBorrowAnnotation : Lean.Option Bool
-- Mathlib.Algebra.Algebra.Operations
Submodule.equivOpposite_symm_apply : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (p : (Submodule R A)ᵐᵒᵖ),
  Submodule.equivOpposite.symm p = Submodule.comap (↑(MulOpposite.opLinearEquiv R).symm) (MulOpposite.unop p)
-- Mathlib.Order.Max
nonempty_gt : ∀ {α : Type u_1} [inst : LT α] [NoMaxOrder α] (a : α), Nonempty { x // a < x }
-- Aesop.Tracing
Aesop.TraceOption.tree : Aesop.TraceOption
-- Mathlib.Analysis.LocallyConvex.WeakSpace
toWeakSpace_closedConvexHull_eq : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] [inst_3 : Module ℝ E]
  [IsScalarTower ℝ 𝕜 E] [inst_5 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E]
  [LocallyConvexSpace ℝ E] {s : Set E},
  ⇑(toWeakSpace 𝕜 E) '' (closedConvexHull 𝕜) s = (closedConvexHull 𝕜) (⇑(toWeakSpace 𝕜 E) '' s)
-- Mathlib.Topology.Order.LeftRightNhds
/-- The set of points in a set which are isolated on the right in this set is countable when the
space is second-countable.  -/
countable_setOfPred_isolated_right_within : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [SecondCountableTopology α]
  {s : Set α}, {x | x ∈ s ∧ nhdsWithin x (s ∩ Set.Ioi x) = ⊥}.Countable
-- Mathlib.Topology.Connected.LocallyPathConnected
/-- In a locally path-connected space, connected components and path-connected components align  -/
connectedComponentsEquivZerothHomotopy : {X : Type u_1} → [inst : TopologicalSpace X] → [LocallyPathConnectedSpace X] → ConnectedComponents X ≃ ZerothHomotopy X
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBMap.find?_some_mem_toList : ∀ {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} {x : α} {v : β} {t : RBTree.RBMap α β cmp},
  t.find? x = some v → ∃ y, (y, v) ∈ t.toList ∧ cmp x y = Ordering.eq
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
/-- The isomorphism in the category of profinite group between a profinite group and
the projective limit of its quotients by open normal subgroups  -/
ProfiniteGrp.isoLimittoFiniteQuotientFunctor : (P : ProfiniteGrp.{u}) → P ≅ ProfiniteGrp.limit P.diagram
-- Init.Data.Fin.Lemmas
cast.congr_simp : ∀ {α β : Sort u} (h : α = β) (a a_1 : α), a = a_1 → cast h a = cast h a_1
-- Mathlib.Combinatorics.SimpleGraph.Girth
SimpleGraph.girth_eq_zero : ∀ {α : Type u_1} {G : SimpleGraph α}, G.girth = 0 ↔ G.IsAcyclic
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.IsCycle.cycleOf : ∀ {α : Type u_2} {f : Equiv.Perm α} {x : α} [inst : DecidableRel f.SameCycle] [inst_1 : DecidableEq α],
  f.IsCycle → f.cycleOf x = if f x = x then 1 else f
-- Mathlib.AlgebraicGeometry.Morphisms.Flat
AlgebraicGeometry.pushoutSection.congr_simp : ∀ {X Y S T : AlgebraicGeometry.Scheme} {f : T ⟶ S} {g g_1 : Y ⟶ X} (e_g : g = g_1) {iX : X ⟶ S} {iY iY_1 : Y ⟶ T}
  (e_iY : iY = iY_1) (H : CategoryTheory.IsPullback g iY iX f) {US : S.Opens} {UT : T.Opens} {UX : X.Opens}
  (hUST : UT ≤ (TopologicalSpace.Opens.map f.base).obj US) (hUSX : UX ≤ (TopologicalSpace.Opens.map iX.base).obj US)
  {UY : Y.Opens} (hUY : UY = (TopologicalSpace.Opens.map g.base).obj UX ⊓ (TopologicalSpace.Opens.map iY.base).obj UT),
  AlgebraicGeometry.pushoutSection H hUST hUSX hUY = AlgebraicGeometry.pushoutSection ⋯ hUST hUSX ⋯
-- Mathlib.LinearAlgebra.Matrix.Unique
Matrix.uniqueAlgEquiv_symm_apply : ∀ {m : Type u_1} {A : Type u_3} {R : Type u_4} [inst : Unique m] [inst_1 : Semiring A] [inst_2 : CommSemiring R]
  [inst_3 : Algebra R A] (a : A), Matrix.uniqueAlgEquiv.symm a = Matrix.of fun x x_1 => a
-- Mathlib.Order.WithBot
WithTop.le_toDual_iff : ∀ {α : Type u_1} [inst : LE α] {x : WithTop α} {y : WithBot αᵒᵈ}, y ≤ WithTop.toDual x ↔ x ≤ WithBot.ofDual y
-- Mathlib.Algebra.Quaternion
Quaternion.normSq_coe : ∀ {R : Type u_3} [inst : CommRing R] (x : R), Quaternion.normSq ↑x = x ^ 2
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
/-- Extending the ordered partitions of `Fin n` bijects with the ordered partitions
of `Fin (n+1)`.  -/
OrderedFinpartition.extendEquiv : (n : ℕ) → (c : OrderedFinpartition n) × Option (Fin c.length) ≃ OrderedFinpartition (n + 1)
-- Mathlib.LinearAlgebra.TensorProduct.Decomposition
DirectSum.toBaseChange_bijective : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {S : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (ℳ : ι → Submodule R M) [inst_3 : DecidableEq ι] [DirectSum.Decomposition ℳ]
  [inst_5 : CommSemiring S] [inst_6 : Algebra R S] (i : ι), Function.Bijective ⇑(Submodule.toBaseChange S (ℳ i))
-- Mathlib.Algebra.Category.AlgCat.Basic
AlgCat.instAlgebraObjForgetAlgHomCarrier : (R : Type u) → [inst : CommRing R] → {S : AlgCat R} → Algebra R ((CategoryTheory.forget (AlgCat R)).obj S)
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.gamma_succ_eq_nfp : ∀ (o : Ordinal.{u_1}), (Order.succ o).gamma = Ordinal.nfp (fun x => Ordinal.veblen x 0) (Order.succ o.gamma)
-- Mathlib.Analysis.Convex.DoublyStochasticMatrix
/-- Each row sum of a doubly stochastic matrix is 1.  -/
sum_row_of_mem_doublyStochastic : ∀ {R : Type u_1} {n : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R]
  [inst_3 : PartialOrder R] [inst_4 : IsOrderedRing R] {M : Matrix n n R},
  M ∈ doublyStochastic R n → ∀ (i : n), ∑ j, M i j = 1
-- Mathlib.RingTheory.Etale.Field
/-- `A` is étale over a field `K` if and only if
`A` is a finite product of finite separable field extensions.
 -/
Algebra.Etale.iff_exists_algEquiv_prod : ∀ (K : Type u_1) (A : Type u) [inst : Field K] [inst_1 : CommRing A] [inst_2 : Algebra K A],
  Algebra.Etale K A ↔
    ∃ I, ∃ (_ : Finite I), ∃ Ai x x_1 x_2, ∀ (i : I), Module.Finite K (Ai i) ∧ Algebra.IsSeparable K (Ai i)
-- Std.Data.HashMap.Lemmas
Std.HashMap.size_unitOfList_le : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α},
  (Std.HashMap.unitOfList l).size ≤ l.length
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.ι_colimitIsoOfIsLeftKanExtension_hom_assoc : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  (α : F ⟶ L.comp F') [inst_3 : F'.IsLeftKanExtension α] [inst_4 : CategoryTheory.Limits.HasColimit F]
  [inst_5 : CategoryTheory.Limits.HasColimit F'] (i : C) {Z : H} (h : CategoryTheory.Limits.colimit F ⟶ Z),
  CategoryTheory.CategoryStruct.comp (α.app i)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F' (L.obj i))
        (CategoryTheory.CategoryStruct.comp (F'.colimitIsoOfIsLeftKanExtension α).hom h)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F i) h
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.instIsScalarTowerSubtypeMemValuationSubringValuationSubringAtPrime : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type u_2} [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R),
  IsScalarTower R (↥(IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime K v)) K
-- Mathlib.Combinatorics.Additive.FreimanHom
/-- Characterisation of `2`-Freiman isomorphisms.  -/
isAddFreimanIso_two : ∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : AddCommMonoid β] {A : Set α} {B : Set β} {f : α → β},
  IsAddFreimanIso 2 A B f ↔ Set.BijOn f A B ∧ ∀ a ∈ A, ∀ b ∈ A, ∀ c ∈ A, ∀ d ∈ A, f a + f b = f c + f d ↔ a + b = c + d
-- Mathlib.LinearAlgebra.TensorProduct.Tower
/-- `baseChange` as a linear map.

When `M = N`, this is true more strongly as `Module.End.baseChangeHom`.  -/
LinearMap.baseChangeHom : (R : Type u_1) →
  (A : Type u_2) →
    (M : Type u_4) →
      (N : Type u_5) →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : Algebra R A] →
              [inst_3 : AddCommMonoid M] →
                [inst_4 : AddCommMonoid N] →
                  [inst_5 : Module R M] →
                    [inst_6 : Module R N] → (M →ₗ[R] N) →ₗ[R] TensorProduct R A M →ₗ[A] TensorProduct R A N
-- Mathlib.GroupTheory.ArchimedeanDensely
LinearOrderedCommGroupWithZero.wellFoundedOn_setOfPred_le_lt_iff_nonempty_discrete_of_ne_zero : ∀ {G₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero G₀] [Nontrivial G₀ˣ] {g : G₀},
  g ≠ 0 → (({x | g ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2) ↔ Nonempty (G₀ ≃*o WithZero (Multiplicative ℤ)))
-- Mathlib.Data.Num.Lemmas
PosNum.to_nat_to_int : ∀ (n : PosNum), ↑↑n = ↑n
-- Mathlib.RingTheory.SimpleModule.Isotypic
Submodule.IsFullyInvariant.of_mem_isotypicComponents : ∀ {R : Type u_2} {M : Type u} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {m : Submodule R M},
  m ∈ isotypicComponents R M → m.IsFullyInvariant
-- Init.Data.Dyadic.Basic
/-- `roundUp x prec` is the least dyadic number with precision at most `prec` which is greater than or equal to `x`.  -/
Dyadic.roundUp : Dyadic → ℤ → Dyadic
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
/-- Given a cell `c` of rank `j` for a rank function `f` for a proper
pairing of a subcomplex of a simplicial set, this is the induced
morphism `c.horn ⟶ f.filtration j`.  -/
SSet.Subcomplex.Pairing.RankFunction.Cell.mapHorn : {X : SSet} →
  {A : X.Subcomplex} →
    {P : A.Pairing} →
      {ι : Type v} →
        [inst : LinearOrder ι] →
          (f : P.RankFunction ι) →
            [inst_1 : P.IsProper] → {j : ι} → (c : f.Cell j) → c.horn.toSSet ⟶ (f.filtration j).toSSet
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
/-- The additive map which sends a cohomology class to the corresponding morphism
in the homotopy category.  -/
CochainComplex.HomComplex.CohomologyClass.toHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {K L : CochainComplex C ℤ} →
        {n : ℤ} →
          CochainComplex.HomComplex.CohomologyClass K L n →+
            ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K ⟶
              (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj
                ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj L))
-- Mathlib.ModelTheory.Order
FirstOrder.Language.noBotOrder_of_dlo : ∀ (L : FirstOrder.Language) (M : Type w') [inst : L.IsOrdered] [inst_1 : L.Structure M] [inst_2 : LE M]
  [L.OrderedStructure M] [M ⊨ L.dlo], NoBotOrder M
-- Mathlib.Algebra.Lie.Extension
LieAlgebra.Extension.mk.inj : ∀ {R : Type u_1} {N : Type u_2} {M : Type u_4} {inst : CommRing R} {inst_1 : LieRing N} {inst_2 : LieAlgebra R N}
  {inst_3 : LieRing M} {inst_4 : LieAlgebra R M} {L : Type u_5} {instLieRing : LieRing L}
  {instLieAlgebra : LieAlgebra R L} {incl : N →ₗ⁅R⁆ L} {proj : L →ₗ⁅R⁆ M}
  {IsExtension : LieAlgebra.IsExtension incl proj} {L_1 : Type u_5} {instLieRing_1 : LieRing L_1}
  {instLieAlgebra_1 : LieAlgebra R L_1} {incl_1 : N →ₗ⁅R⁆ L_1} {proj_1 : L_1 →ₗ⁅R⁆ M}
  {IsExtension_1 : LieAlgebra.IsExtension incl_1 proj_1},
  { L := L, instLieRing := instLieRing, instLieAlgebra := instLieAlgebra, incl := incl, proj := proj,
        IsExtension := IsExtension } =
      { L := L_1, instLieRing := instLieRing_1, instLieAlgebra := instLieAlgebra_1, incl := incl_1, proj := proj_1,
        IsExtension := IsExtension_1 } →
    L = L_1 ∧ instLieRing ≍ instLieRing_1 ∧ instLieAlgebra ≍ instLieAlgebra_1 ∧ incl ≍ incl_1 ∧ proj ≍ proj_1
-- Mathlib.RingTheory.Binomial
Ring.choose_zero_right' : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : Pow R ℕ] [inst_2 : BinomialRing R] (r : R),
  Ring.choose r 0 = (r + 1) ^ 0
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.MethodsRef.toMethodsImpl : Lean.Meta.Simp.MethodsRef → Lean.Meta.Simp.Methods
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.Final.zigzag_of_eqvGen_colimitTypeRel : ∀ {C : Type v} [inst : CategoryTheory.Category.{v, v} C] {D : Type u₁} [inst_1 : CategoryTheory.Category.{v, u₁} D]
  {F : CategoryTheory.Functor C D} {d : D} {f₁ f₂ : (X : C) × (d ⟶ F.obj X)},
  Relation.EqvGen (F.comp (CategoryTheory.coyoneda.obj (Opposite.op d))).ColimitTypeRel f₁ f₂ →
    CategoryTheory.Zigzag (CategoryTheory.StructuredArrow.mk f₁.snd) (CategoryTheory.StructuredArrow.mk f₂.snd)
-- Mathlib.Algebra.Order.Module.HahnEmbedding
HahnEmbedding.Seed.coeff_baseEmbedding : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] {R : Type u_3} [inst_9 : AddCommGroup R]
  [inst_10 : LinearOrder R] [inst_11 : Module K R] (seed : HahnEmbedding.Seed K M R) {x : ↥seed.baseEmbedding.domain}
  {f : Π₀ (c : FiniteArchimedeanClass M), ↥(seed.stratum c)},
  (↑x = f.sum fun c => ⇑(seed.stratum c).subtype) →
    ∀ (c : FiniteArchimedeanClass M), (ofLex (↑seed.baseEmbedding x)).coeff c = (seed.coeff c) (f c)
-- Mathlib.Data.Sym.Sym2
Sym2.filter_image_mk_isDiag : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α),
  {x ∈ Finset.image (Function.uncurry Sym2.mk) (s ×ˢ s) | x.IsDiag} = Finset.image (Function.uncurry Sym2.mk) s.diag
-- Mathlib.CategoryTheory.Comma.Basic
/-- If `F` is an equivalence, then so is `preLeft F L R`.  -/
CategoryTheory.Comma.isEquivalence_preLeft : ∀ {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) [F.IsEquivalence], (CategoryTheory.Comma.preLeft F L R).IsEquivalence
-- Mathlib.CategoryTheory.LiftingProperties.Basic
/-- `HasLiftingProperty i p` means that `i` has the left lifting
property with respect to `p`, or equivalently that `p` has
the right lifting property with respect to `i`.  -/
CategoryTheory.HasLiftingProperty : {C : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} C] → {A B X Y : C} → (A ⟶ B) → (X ⟶ Y) → Prop
-- Mathlib.CategoryTheory.Monoidal.Subcategory
/-- The braided structure on a full subcategory inherited by the braided structure on `C`.
 -/
CategoryTheory.ObjectProperty.fullBraidedSubcategory : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (P : CategoryTheory.ObjectProperty C) →
        [inst_2 : P.IsMonoidal] → [CategoryTheory.BraidedCategory C] → CategoryTheory.BraidedCategory P.FullSubcategory
-- Mathlib.Order.Category.OmegaCompletePartialOrder
ωCPO.instInhabited : Inhabited ωCPO
-- Init.Data.UInt.BasicAux
/-- Converts a natural number to `USize`, returning the largest representable value if the number is too
large.

Returns `USize.size - 1`, which is  `2^64 - 1` or `2^32 - 1` depending on the platform, for natural
numbers greater than or equal to `USize.size`.
 -/
USize.ofNatClamp : ℕ → USize
-- Mathlib.Topology.Defs.Filter
/-- The quotient of a topological space by its `inseparableSetoid`. Also called the Kolmogorov
quotient. This quotient is guaranteed to be a T₀ space.  -/
SeparationQuotient : (X : Type u_1) → [TopologicalSpace X] → Type u_1
-- Lean.Compiler.InitAttr
Lean.hasInitAttr : Lean.Environment → Lean.Name → Bool
-- Mathlib.Order.Heyting.Basic
sdiff_le_sdiff : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b c d : α}, d ≤ c → b ≤ a → d \ a ≤ c \ b
-- Mathlib.Algebra.Homology.LeftResolution.Basic
/-- Given `ι : C ⥤ A`, `Λ : LeftResolution ι`, this is a
functor `A ⥤ ChainComplex C ℕ` which sends `X : A` to a resolution consisting
of objects in `C`.  -/
CategoryTheory.Abelian.LeftResolution.chainComplexFunctor : {A : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_2} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_1} A] →
        {ι : CategoryTheory.Functor C A} →
          CategoryTheory.Abelian.LeftResolution ι →
            [ι.Full] →
              [ι.Faithful] →
                [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C] →
                  [CategoryTheory.Abelian A] → CategoryTheory.Functor A (ChainComplex C ℕ)
-- Mathlib.Algebra.Group.Shrink
equivShrink_add : ∀ {α : Type u_2} [inst : Small.{v, u_2} α] [inst_1 : Add α] (x y : α),
  (equivShrink α) (x + y) = (equivShrink α) x + (equivShrink α) y
-- Mathlib.Algebra.Homology.Homotopy
Homotopy.nullHomotopicMap'_f_of_not_rel_right : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} {k₁ k₀ : ι} (r₁₀ : c.Rel k₁ k₀),
  (∀ (l : ι), ¬c.Rel l k₁) →
    ∀ (h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)),
      (Homotopy.nullHomotopicMap' h).f k₁ = CategoryTheory.CategoryStruct.comp (C.d k₁ k₀) (h k₀ k₁ r₁₀)
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.trPosNum.eq_1 : Turing.PartrecToTM2.trPosNum PosNum.one = [Turing.PartrecToTM2.Γ'.bit1]
-- Mathlib.RingTheory.HopkinsLevitzki
IsSemiprimaryRing.isNoetherian_iff_finite_of_jacobson_fg : ∀ {R : Type u_2} {M : Type u} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsSemiprimaryRing R],
  (Ring.jacobson R).FG → (IsNoetherian R M ↔ Module.Finite R M)