mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.ConfigEval.Types
Lean.Elab.ConfigEval.EvalConfigItem.mk.injEq : ∀ {α : Type} (set set_1 : α → Lean.Elab.ConfigEval.ConfigItem → Lean.Elab.TermElabM α),
  ({ set := set } = { set := set_1 }) = (set = set_1)
-- Mathlib.Data.ENat.BigOperators
ENat.lt_top_of_sum_ne_top : ∀ {α : Type u_1} {s : Finset α} {f : α → ℕ∞}, ∑ x ∈ s, f x ≠ ⊤ → ∀ {a : α}, a ∈ s → f a < ⊤
-- Mathlib.Combinatorics.Graph.Simple
Graph.Simple.anti : ∀ {α : Type u_1} {β : Type u_2} {G H : Graph α β} [G.Simple], H ≤ G → H.Simple
-- Mathlib.Algebra.Quandle
UnitalShelf.act_self_act_eq : ∀ {S : Type u_1} [inst : UnitalShelf S] (x y : S), Shelf.act x (Shelf.act x y) = Shelf.act x y
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
IsDedekindDomain.HeightOneSpectrum.instCoeIdeal : {R : Type u_1} → [inst : CommRing R] → Coe (IsDedekindDomain.HeightOneSpectrum R) (Ideal R)
-- Mathlib.Combinatorics.Additive.Corner.Roth
IsCornerFree.eq_1 : ∀ {G : Type u_1} [inst : AddCommMonoid G] (A : Set (G × G)),
  IsCornerFree A = ∀ ⦃x₁ y₁ x₂ y₂ : G⦄, IsCorner A x₁ y₁ x₂ y₂ → x₁ = x₂
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
/-- Construct a bundled `SemiNormedGrp₁` from the underlying type and typeclass.  -/
SemiNormedGrp₁.of : (carrier : Type u) → [str : SeminormedAddCommGroup carrier] → SemiNormedGrp₁
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.mk_mul_mk : ∀ {R : Type u_1} {a b : R} [inst : Mul R] [inst_1 : Add R] (x1 y1 x2 y2 : R),
  { re := x1, im := y1 } * { re := x2, im := y2 } =
    { re := x1 * x2 + a * y1 * y2, im := x1 * y2 + y1 * x2 + b * y1 * y2 }
-- Mathlib.Combinatorics.Enumerative.Composition
CompositionAsSet.card_boundaries_pos : ∀ {n : ℕ} (c : CompositionAsSet n), 0 < c.boundaries.card
-- Init.Data.Int.DivMod.Lemmas
Int.sub_mul_bmod_self_right : ∀ (a b : ℤ) (c : ℕ), (a - b * ↑c).bmod c = a.bmod c
-- Lean.Elab.Util
Lean.Elab.evalSyntaxConstant : Lean.Environment → Lean.Options → Lean.Name → ExceptT String Id Lean.Syntax
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.roots_C_mul : ∀ {R : Type u} {a : R} [inst : CommRing R] [inst_1 : IsDomain R] (p : Polynomial R),
  a ≠ 0 → (Polynomial.C a * p).roots = p.roots
-- Mathlib.Algebra.GroupWithZero.Action.Defs
/-- Compose a `SMulWithZero` with a `ZeroHom`, with action `f r' • m`  -/
SMulWithZero.compHom : {M₀ : Type u_2} →
  {M₀' : Type u_3} →
    (A : Type u_7) →
      [inst : Zero M₀] →
        [inst_1 : Zero A] → [SMulWithZero M₀ A] → [inst_3 : Zero M₀'] → ZeroHom M₀' M₀ → SMulWithZero M₀' A
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.liesOver_conjugate_embedding_of_mem_ramifiedPlacesOver : ∀ {K : Type u_4} {L : Type u_5} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  {v : NumberField.InfinitePlace K} {w : NumberField.InfinitePlace L},
  w ∈ NumberField.InfinitePlace.ramifiedPlacesOver L v →
    NumberField.ComplexEmbedding.LiesOver (NumberField.ComplexEmbedding.conjugate w.embedding) v.embedding
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
Subgroup.instEncodableSubtypeMulOppositeMemOp.eq_1 : ∀ {G : Type u_2} [inst : Group G] (H : Subgroup G) [inst_1 : Encodable ↥H],
  H.instEncodableSubtypeMulOppositeMemOp = Encodable.ofEquiv (↥H) H.equivOp.symm
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
CategoryTheory.StrictPseudofunctor.comp_obj : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C] {D : Type u₃}
  [inst_2 : CategoryTheory.Bicategory D] (F : CategoryTheory.StrictPseudofunctor B C)
  (G : CategoryTheory.StrictPseudofunctor C D) (X : B), (F.comp G).obj X = G.obj (F.obj X)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.ofZeros_H : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) (hg : S.g = 0),
  (CategoryTheory.ShortComplex.LeftHomologyData.ofZeros S hf hg).H = S.X₂
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.of_mul_left_left : ∀ {R : Type u} [inst : CommSemiring R] {x y z : R}, IsCoprime (x * y) z → IsCoprime x z
-- Mathlib.RingTheory.Lasker
Submodule.IsMinimalPrimaryDecomposition.comap_localized₀_eq_ite : ∀ {R : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Submodule R M}
  (s₀ : Finset ↑N.associatedPrimes),
  IsLowerSet ↑s₀ →
    ∀ (q : Submodule R M),
      q.IsPrimary →
        ∀ (p : ↑N.associatedPrimes),
          (q.colon Set.univ).radical = ↑p →
            Submodule.comap (LocalizedModule.mkLinearMap (⨅ q ∈ s₀, (↑q).primeCompl) M)
                (Submodule.localized₀ (⨅ q ∈ s₀, (↑q).primeCompl)
                  (LocalizedModule.mkLinearMap (⨅ q ∈ s₀, (↑q).primeCompl) M) q) =
              if p ∈ s₀ then q else ⊤
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw.size_eq_length : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β},
  Std.DHashMap.Internal.Raw.WFImp m → m.size = (Std.DHashMap.Internal.toListModel m.buckets).length
-- Mathlib.Data.Finmap
Finmap.keys_singleton : ∀ {α : Type u} {β : α → Type v} (a : α) (b : β a), (Finmap.singleton a b).keys = {a}
-- Std.Data.TreeMap.Basic
Std.TreeMap.mk.injEq : ∀ {α : Type u} {β : Type v} {cmp : autoParam (α → α → Ordering) Std.TreeMap._auto_1}
  (inner inner_1 : Std.DTreeMap α (fun x => β) cmp), ({ inner := inner } = { inner := inner_1 }) = (inner = inner_1)
-- Mathlib.RepresentationTheory.Intertwining
Representation.TensorProduct.comm_symm : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : CommSemiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  (ρ : Representation A G V) (σ : Representation A G W),
  (Representation.TensorProduct.comm σ ρ).symm = Representation.TensorProduct.comm ρ σ
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
CategoryTheory.Functor.leftKanExtensionIsoFiberwiseColimit_hom_app : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D) {H : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} H] (F : CategoryTheory.Functor C H)
  [inst_3 : L.HasPointwiseLeftKanExtension F] [inst_4 : L.HasLeftKanExtension F] (X : D),
  (L.leftKanExtensionIsoFiberwiseColimit F).hom.app X =
    CategoryTheory.CategoryStruct.comp (L.leftKanExtensionObjIsoColimit F X).hom
      (CategoryTheory.Limits.HasColimit.isoOfNatIso
          (CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.CostructuredArrow.ιCompGrothendieckProj L X) F)).inv
-- Mathlib.Order.Hom.Basic
/-- `Prod.swap` as an `OrderIso`.  -/
OrderIso.prodComm : {α : Type u_2} → {β : Type u_3} → [inst : LE α] → [inst_1 : LE β] → α × β ≃o β × α
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
/-- Technical lemma ensuring that the preimage under an extended chart of a neighborhood of a point
in the source is a neighborhood of the preimage, within a set.  -/
OpenPartialHomeomorph.extend_preimage_mem_nhdsWithin : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  (f : OpenPartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} {s t : Set M} {x : M},
  x ∈ f.source →
    t ∈ nhdsWithin x s →
      ↑(f.extend I).symm ⁻¹' t ∈ nhdsWithin (↑(f.extend I) x) (↑(f.extend I).symm ⁻¹' s ∩ Set.range ↑I)
-- Mathlib.Algebra.Order.Floor.Div
floorDiv_one : ∀ {α : Type u_2} {β : Type u_3} [inst : Semiring α] [inst_1 : PartialOrder α] [inst_2 : AddCommMonoid β]
  [inst_3 : PartialOrder β] [inst_4 : MulActionWithZero α β] [inst_5 : FloorDiv α β] [IsOrderedRing α] [Nontrivial α]
  (b : β), b ⌊/⌋ 1 = b
-- Batteries.Recycling.RBTree.Lemmas
/-- The value `x` returned by `upperBound?` is greater or equal to the `cut`.  -/
RBTree.RBNode.upperBound?_ge : ∀ {α : Type u_1} {cut : α → Ordering} {x : α} {t : RBTree.RBNode α},
  RBTree.RBNode.upperBound? cut t = some x → cut x ≠ Ordering.gt
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.map_sub : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup E₂] [inst_4 : Module R E]
  [inst_5 : Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) (x y : E), f (x - y) = f x - f y
-- Mathlib.RingTheory.TwoSidedIdeal.Operations
TwoSidedIdeal.rightModule : {R : Type u_1} → [inst : Ring R] → (I : TwoSidedIdeal R) → Module Rᵐᵒᵖ ↥I
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.sInf_toSubalgebra : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E]
  (S : Set (IntermediateField F E)), (sInf S).toSubalgebra = sInf (IntermediateField.toSubalgebra '' S)
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.zero_ne_one_of_charC_cert.eq_1 : ∀ (c : ℕ) (p : Lean.Grind.Linarith.Poly),
  Lean.Grind.Linarith.zero_ne_one_of_charC_cert c p =
    (decide (↑c > 1) && p == Lean.Grind.Linarith.Poly.add 1 0 Lean.Grind.Linarith.Poly.nil)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cochain.shift_units_smul : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {R : Type u_1}
  [inst_2 : Ring R] [inst_3 : CategoryTheory.Linear R C] {K L : CochainComplex C ℤ} {n : ℤ}
  (γ : CochainComplex.HomComplex.Cochain K L n) (a : ℤ) (x : Rˣ), (x • γ).shift a = x • γ.shift a
-- Init.Data.List.Nat.TakeDrop
List.take_take : ∀ {α : Type u_1} {i j : ℕ} {l : List α}, List.take i (List.take j l) = List.take (min i j) l
-- Mathlib.Analysis.Calculus.FDeriv.CompCLM
DifferentiableWithinAt.clm_comp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {x : E} {s : Set E} {H : Type u_5}
  [inst_7 : NormedAddCommGroup H] [inst_8 : NormedSpace 𝕜 H] {c : E → G →L[𝕜] H} {d : E → F →L[𝕜] G},
  DifferentiableWithinAt 𝕜 c s x → DifferentiableWithinAt 𝕜 d s x → DifferentiableWithinAt 𝕜 (fun y => c y ∘SL d y) s x
-- Mathlib.Algebra.BigOperators.ModEq
Nat.ModEq.listProd_one : ∀ {n : ℕ} {l : List ℕ}, (∀ x ∈ l, x ≡ 1 [MOD n]) → l.prod ≡ 1 [MOD n]
-- Mathlib.LinearAlgebra.Projectivization.Independence
/-- A family of points in projective space is independent if and only if the family of
submodules which the points determine is independent in the lattice-theoretic sense.  -/
Projectivization.independent_iff_iSupIndep : ∀ {ι : Type u_1} {K : Type u_2} {V : Type u_3} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {f : ι → Projectivization K V}, Projectivization.Independent f ↔ iSupIndep fun i => (f i).submodule
-- Init.Prelude
eq_true_of_ne_false : ∀ {b : Bool}, ¬b = false → b = true
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.nnnorm_def' : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A] (a : DoubleCentralizer 𝕜 A),
  ‖a‖₊ = ‖DoubleCentralizer.toProdMulOppositeHom a‖₊
-- Lean.Meta.Tactic.Grind.Inv
_private.Lean.Meta.Tactic.Grind.Inv.0.Lean.Meta.Grind.checkChild : Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM Bool
-- Mathlib.RingTheory.TensorProduct.MvPolynomial
MvPolynomial.rTensorAlgEquiv.eq_1 : ∀ {R : Type u} {N : Type v} [inst : CommSemiring R] {σ : Type u_1} {S : Type u_3} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : CommSemiring N] [inst_4 : Algebra R N],
  MvPolynomial.rTensorAlgEquiv = AddMonoidAlgebra.rTensorEquivAlgEquiv R S S N
-- Mathlib.LinearAlgebra.Matrix.Reindex
Matrix.reindexLinearEquiv_mul : ∀ {m : Type u_2} {n : Type u_3} {o : Type u_4} {m' : Type u_6} {n' : Type u_7} {o' : Type u_8} (R : Type u_11)
  (A : Type u_12) [inst : Semiring R] [inst_1 : Semiring A] [inst_2 : Module R A] [inst_3 : Fintype n]
  [inst_4 : Fintype n'] (eₘ : m ≃ m') (eₙ : n ≃ n') (eₒ : o ≃ o') (M : Matrix m n A) (N : Matrix n o A),
  (Matrix.reindexLinearEquiv R A eₘ eₙ) M * (Matrix.reindexLinearEquiv R A eₙ eₒ) N =
    (Matrix.reindexLinearEquiv R A eₘ eₒ) (M * N)
-- Mathlib.Topology.Algebra.Module.Alternating.Topology
ContinuousAlternatingMap.instTopologicalSpace : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      {ι : Type u_4} →
        [inst : NormedField 𝕜] →
          [inst_1 : AddCommGroup E] →
            [inst_2 : Module 𝕜 E] →
              [inst_3 : TopologicalSpace E] →
                [inst_4 : AddCommGroup F] →
                  [inst_5 : Module 𝕜 F] →
                    [inst_6 : TopologicalSpace F] → [IsTopologicalAddGroup F] → TopologicalSpace (E [⋀^ι]→L[𝕜] F)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α Unit} [EquivBEq α] [LawfulHashable α],
  m.WF →
    ∀ {l : List α} {k k' fallback : α},
      (k == k') = true →
        k ∉ m →
          List.Pairwise (fun a b => (a == b) = false) l → k ∈ l → (m.insertManyIfNewUnit l).getKeyD k' fallback = k
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.IsPosSemidef.add : ∀ {R : Type u_1} {M : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {I₁ : R →+* R}
  [inst_3 : Preorder R] [AddLeftMono R] {B C : M →ₛₗ[I₁] M →ₗ[R] R},
  B.IsPosSemidef → C.IsPosSemidef → (B + C).IsPosSemidef
-- LeanSearchClient.LoogleSyntax
LeanSearchClient.unicode_turnstile : Lean.Parser.Parser
-- Mathlib.Data.Set.Image
Disjoint.of_preimage : ∀ {α : Type u_1} {β : Type u_2} {f : α → β},
  Function.Surjective f → ∀ {s t : Set β}, Disjoint (f ⁻¹' s) (f ⁻¹' t) → Disjoint s t
-- Mathlib.Algebra.Category.Ring.Adjunctions
CommRingCat.coyonedaUnique_inv_app_hom_apply : ∀ {n : Type v} [inst : Unique n] (X : CommRingCat) (a : ↑X) (a_1 : Opposite.unop (Opposite.op n)),
  (CommRingCat.Hom.hom (CommRingCat.coyonedaUnique.inv.app X)) a a_1 = a
-- Init.Data.Int.DivMod.Bootstrap
Int.emod_eq_zero_of_dvd : ∀ {a b : ℤ}, a ∣ b → b % a = 0
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
/-- The underlying modification of lax transformations.  -/
CategoryTheory.Oplax.LaxTrans.Hom.as : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.OplaxFunctor B C} →
          {η θ : F ⟶ G} → CategoryTheory.Oplax.LaxTrans.Hom η θ → CategoryTheory.Oplax.LaxTrans.Modification η θ
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.TableEntry.mk.injEq : ∀ (waiters : Array Lean.Meta.SynthInstance.Waiter) (answers : Array Lean.Meta.SynthInstance.Answer)
  (waiters_1 : Array Lean.Meta.SynthInstance.Waiter) (answers_1 : Array Lean.Meta.SynthInstance.Answer),
  ({ waiters := waiters, answers := answers } = { waiters := waiters_1, answers := answers_1 }) =
    (waiters = waiters_1 ∧ answers = answers_1)
-- Mathlib.CategoryTheory.Limits.FintypeCat
CategoryTheory.Limits.FintypeCat.inclusion_preservesFiniteColimits : CategoryTheory.Limits.PreservesFiniteColimits FintypeCat.incl
-- Mathlib.Data.Nat.Digits.Defs
_private.Mathlib.Data.Nat.Digits.Defs.0.Nat.digitsAux0.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.coe_of : ∀ (R : Type u) [inst : Semiring R] (X : Type v) [inst_1 : Semiring X] [inst_2 : Module R X], ↑(SemimoduleCat.of R X) = X
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem!_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited β], t.WF → ∀ {k a : α} {v : β}, (t.insert k v)[a]! = if cmp k a = Ordering.eq then v else t[a]!
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.integrableOn_iff_comap_subtypeVal : ∀ {α : Type u_1} {ε : Type u_3} {mα : MeasurableSpace α} {f : α → ε} {s : Set α} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε],
  MeasurableSet s →
    (MeasureTheory.IntegrableOn f s μ ↔
      MeasureTheory.Integrable (f ∘ Subtype.val) (MeasureTheory.Measure.comap Subtype.val μ))
-- Mathlib.Algebra.Lie.Weights.IsSimple
LieIdeal.mem_rootSet : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : LieRing L] [inst_2 : LieAlgebra K L]
  [inst_3 : FiniteDimensional K L] {H : LieSubalgebra K L} [inst_4 : H.IsCartanSubalgebra] {I : LieIdeal K L}
  {α : ↥LieSubalgebra.root}, α ∈ I.rootSet ↔ LieAlgebra.rootSpace H ⇑↑α ≤ LieSubmodule.restr I H
-- Mathlib.Algebra.Torsor.Basic
/-- Subtracting the point `p` is an injective function.  -/
vsub_left_injective : ∀ {G : Type u_1} {P : Type u_2} [inst : AddGroup G] [T : AddTorsor G P] (p : P), Function.Injective fun x => x -ᵥ p
-- Mathlib.Analysis.Matrix.Order
/-- **Alias** of the forward direction of `Matrix.isStrictlyPositive_iff_posDef`. -/
Matrix.IsStrictlyPositive.posDef : ∀ {𝕜 : Type u_1} {n : Type u_2} [inst : RCLike 𝕜] [inst_1 : Fintype n] [inst_2 : DecidableEq n] {x : Matrix n n 𝕜},
  IsStrictlyPositive x → x.PosDef
-- Mathlib.CategoryTheory.Limits.Types.Images
/-- the inclusion of `Image f` into the target  -/
CategoryTheory.Limits.Types.Image.ι : {α β : Type u} → (f : α ⟶ β) → CategoryTheory.Limits.Types.Image f ⟶ β
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
WeierstrassCurve.natDegree_Ψ₂Sq_le : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R), W.Ψ₂Sq.natDegree ≤ 3
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
/-- The map taking the product of two fundamental groupoids to the fundamental groupoid of the product
of the two topological spaces. This is in fact an isomorphism (see `prodIso`).
 -/
FundamentalGroupoidFunctor.prodToProdTop : (A : TopCat) →
  (B : TopCat) →
    CategoryTheory.Functor
      (↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj A) ×
        ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj B))
      ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj (TopCat.of (↑A × ↑B)))
-- Mathlib.Analysis.SpecialFunctions.Complex.Log
Complex.log_mul_ofReal : ∀ (r : ℝ), 0 < r → ∀ (x : ℂ), x ≠ 0 → Complex.log (x * ↑r) = ↑(Real.log r) + Complex.log x
-- Mathlib.CategoryTheory.GuitartExact.Quotient
CategoryTheory.TwoSquare.GuitartExact.quotient_of_nonempty_leftHomotopy : ∀ {C₀ : Type u_1} {C : Type u_2} {H₀ : Type u_3} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C₀]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.Category.{v_3, u_3} H₀]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} H] {T : CategoryTheory.Functor C₀ H₀} {L : CategoryTheory.Functor C₀ C}
  {R : CategoryTheory.Functor H₀ H} {B : CategoryTheory.Functor C H} [T.EssSurj] [T.Full] [B.Full]
  (e : T.comp R ≅ L.comp B),
  (∀ ⦃X₀ : C₀⦄ ⦃Y : C⦄ (f₀ f₁ : L.obj X₀ ⟶ Y),
      B.map f₀ = B.map f₁ → ∃ P, T.map P.i₀ = T.map P.i₁ ∧ Nonempty ((P.map L).LeftHomotopy f₀ f₁)) →
    CategoryTheory.TwoSquare.GuitartExact e.hom
-- Lean.Elab.Do.Basic
Lean.Elab.Do.observingPostpone : {α : Type} → Lean.Elab.Do.DoElabM α → Lean.Elab.Do.DoElabM (Option α)
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.HasImageMaps.has_image_map : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.Limits.HasImages C}
  [self : CategoryTheory.Limits.HasImageMaps C] {f g : CategoryTheory.Arrow C} (st : f ⟶ g),
  CategoryTheory.Limits.HasImageMap st
-- Mathlib.AlgebraicGeometry.Geometrically.Basic
AlgebraicGeometry.geometrically_iff_of_commRing_of_isClosedUnderIsomorphisms : ∀ {X : AlgebraicGeometry.Scheme} {P : CategoryTheory.ObjectProperty AlgebraicGeometry.Scheme} {R : Type u}
  [inst : CommRing R] {f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of R)} [P.IsClosedUnderIsomorphisms],
  AlgebraicGeometry.geometrically P f ↔
    ∀ (K : Type u) [inst_2 : Field K] [inst_3 : Algebra R K],
      P (CategoryTheory.Limits.pullback f (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R K))))
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.CommGrp.forget_obj : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X : CategoryTheory.CommGrp C),
  (CategoryTheory.CommGrp.forget C).obj X = X.X
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Hom.resLE_appLE : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {U : Y.Opens} {V : X.Opens}
  (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) (O : (↑U).Opens) (W : (↑V).Opens)
  (e' : W ≤ (TopologicalSpace.Opens.map (AlgebraicGeometry.Scheme.Hom.resLE f U V e).base).obj O),
  AlgebraicGeometry.Scheme.Hom.appLE (AlgebraicGeometry.Scheme.Hom.resLE f U V e) O W e' =
    AlgebraicGeometry.Scheme.Hom.appLE f ((AlgebraicGeometry.Scheme.Hom.opensFunctor U.ι).obj O)
      ((AlgebraicGeometry.Scheme.Hom.opensFunctor V.ι).obj W) ⋯
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.pushforward_monotone : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X),
  Monotone (CategoryTheory.Sieve.pushforward f)
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal.mk.congr_simp : ∀ {J : Type w} [inst : CategoryTheory.SmallCategory J] {κ : Cardinal.{w}}
  (toDiagram : CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram J κ) (top : J)
  (isTerminal isTerminal_1 : toDiagram.IsTerminal top),
  isTerminal = isTerminal_1 →
    ∀ (uniq_terminal : ∀ (j : J) (hj : toDiagram.IsTerminal j), j = top),
      { toDiagram := toDiagram, top := top, isTerminal := isTerminal, uniq_terminal := uniq_terminal } =
        { toDiagram := toDiagram, top := top, isTerminal := isTerminal_1, uniq_terminal := uniq_terminal }
-- Mathlib.GroupTheory.Exponent
Group.exponent_dvd_iff_forall_zpow_eq_one : ∀ {G : Type u} [inst : Group G] {n : ℤ}, ↑(Monoid.exponent G) ∣ n ↔ ∀ (g : G), g ^ n = 1
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- An `affineCombination` with sum of weights 1 is in the
`affineSpan` of an indexed family, if the underlying ring is
nontrivial.  -/
affineCombination_mem_affineSpan : ∀ {ι : Type u_1} {k : Type u_2} {V : Type u_3} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V]
  [inst_2 : Module k V] [inst_3 : AddTorsor V P] [Nontrivial k] {s : Finset ι} {w : ι → k},
  ∑ i ∈ s, w i = 1 → ∀ (p : ι → P), (Finset.affineCombination k s p) w ∈ affineSpan k (Set.range p)
-- Mathlib.Analysis.Convex.Gauge
le_gauge_of_subset_closedBall : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {s : Set E} {r : ℝ} {x : E},
  Absorbent ℝ s → 0 ≤ r → s ⊆ Metric.closedBall 0 r → ‖x‖ / r ≤ gauge s x
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
CochainComplex.mappingCocone.liftCochain.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (φ : K ⟶ L) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ}
  {n m : ℤ} (α α_1 : CochainComplex.HomComplex.Cochain M K n),
  α = α_1 →
    ∀ (β β_1 : CochainComplex.HomComplex.Cochain M L m),
      β = β_1 →
        ∀ (h : m + 1 = n) (T : CochainComplex.HomComplex.Triplet n),
          CochainComplex.mappingCocone.liftCochain φ α β h T = CochainComplex.mappingCocone.liftCochain φ α_1 β_1 h T
-- Mathlib.Combinatorics.Enumerative.Partition.GenFun
_private.Mathlib.Combinatorics.Enumerative.Partition.GenFun.0.Nat.Partition.aux_dvd_of_coeff_ne_zero : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : TopologicalSpace R] [T2Space R] {f : ℕ → ℕ → R} {d : ℕ}
  {s : Finset ℕ},
  0 ∉ s →
    ∀ {g : ℕ →₀ ℕ},
      g ∈ s.finsuppAntidiag d →
        (∀ i ∈ s, (PowerSeries.coeff (g i)) (1 + ∑' (j : ℕ), f i (j + 1) • PowerSeries.X ^ (i * (j + 1))) ≠ 0) →
          ∀ (x : ℕ), x ∣ g x
-- Mathlib.ModelTheory.Algebra.Field.Basic
FirstOrder.Field.FieldAxiom.mulAssoc : FirstOrder.Field.FieldAxiom