mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Fubini
/-- The cone `coneOfHasLimitCurryCompLim` is in fact a limit cone.
 -/
CategoryTheory.Limits.isLimitConeOfHasLimitCurryCompLim : {J : Type u_1} →
  {K : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} K] →
        {C : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
            (G : CategoryTheory.Functor (J × K) C) →
              [inst_3 : CategoryTheory.Limits.HasLimitsOfShape K C] →
                [inst_4 :
                    CategoryTheory.Limits.HasLimit
                      ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.lim)] →
                  CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.coneOfHasLimitCurryCompLim G)
-- Mathlib.Topology.Algebra.Module.LinearPMap
LinearPMap.IsClosed.eq_1 : ∀ {R : Type u_1} {E : Type u_2} {F : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup E] [inst_2 : AddCommGroup F]
  [inst_3 : Module R E] [inst_4 : Module R F] [inst_5 : TopologicalSpace E] [inst_6 : TopologicalSpace F]
  (f : E →ₗ.[R] F), f.IsClosed = IsClosed ↑f.graph
-- Mathlib.Algebra.Lie.Classical
/-- The symplectic Lie algebra: skew-adjoint matrices with respect to the canonical skew-symmetric
bilinear form.  -/
LieAlgebra.Symplectic.sp : (l : Type u_4) →
  (R : Type u₂) →
    [inst : DecidableEq l] → [inst_1 : CommRing R] → [inst_2 : Fintype l] → LieSubalgebra R (Matrix (l ⊕ l) (l ⊕ l) R)
-- Mathlib.RingTheory.PolynomialLaw.Basic
PolynomialLaw.one_tmul_ground_apply' : ∀ {R : Type u} [inst : CommSemiring R] {M : Type u_1} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_2}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (f : M →ₚₗ[R] N) {S : Type u} [inst_5 : CommSemiring S]
  [inst_6 : Algebra R S] (x : M), 1 ⊗ₜ[R] f.ground x = f.toFun' S (1 ⊗ₜ[R] x)
-- Mathlib.RingTheory.WittVector.FrobeniusFractionField
/-- This is the `n+1`st coefficient of our solution, projected from `root_exists`.  -/
WittVector.RecursionMain.succNthVal : (p : ℕ) →
  [hp : Fact (Nat.Prime p)] →
    {k : Type u_1} →
      [inst : Field k] →
        [CharP k p] →
          [IsAlgClosed k] → (n : ℕ) → (a₁ a₂ : WittVector p k) → (Fin (n + 1) → k) → a₁.coeff 0 ≠ 0 → a₂.coeff 0 ≠ 0 → k
-- Mathlib.Probability.StrongLaw
ProbabilityTheory.integral_truncation_eq_intervalIntegral : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
  MeasureTheory.AEStronglyMeasurable f μ →
    ∀ {A : ℝ},
      0 ≤ A → ∫ (x : α), ProbabilityTheory.truncation f A x ∂μ = ∫ (y : ℝ) in -A..A, y ∂MeasureTheory.Measure.map f μ
-- Mathlib.Data.Finsupp.Single
Finsupp.mem_support_single : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] (a a' : α) (b : M), a ∈ (fun₀ | a' => b).support ↔ a = a' ∧ b ≠ 0
-- Mathlib.Order.Filter.Map
Filter.generate_image_preimage_le_comap : ∀ {α : Type u_1} {β : Type u_2} (U : Set (Set α)) (f : β → α),
  Filter.generate ((fun x => f ⁻¹' x) '' U) ≤ Filter.comap f (Filter.generate U)
-- Mathlib.Algebra.Algebra.Defs
algebraMap.coeHTCT : (R : Type u_1) → (A : Type u_2) → [inst : CommSemiring R] → [inst_1 : Semiring A] → [Algebra R A] → CoeHTCT R A
-- Mathlib.Topology.Instances.EReal.Lemmas
EReal.tendsto_coe_nhds_bot_iff : ∀ {α : Type u_1} {f : α → ℝ} {l : Filter α},
  Filter.Tendsto (fun x => ↑(f x)) l (nhds ⊥) ↔ Filter.Tendsto f l Filter.atBot
-- Mathlib.Combinatorics.Enumerative.Composition
_private.Mathlib.Combinatorics.Enumerative.Composition.0.Composition.recOnSingleAppend.match_1.splitter : (motive : (blocks : List ℕ) → (∀ {i : ℕ}, i ∈ blocks → 0 < i) → Sort u_1) →
  (blocks : List ℕ) →
    (blocks_pos : ∀ {i : ℕ}, i ∈ blocks → 0 < i) →
      ((blocks_pos : ∀ {i : ℕ}, i ∈ [] → 0 < i) → motive [] blocks_pos) →
        ((tail : List ℕ) → (blocks_pos : ∀ {i : ℕ}, i ∈ 0 :: tail → 0 < i) → motive (0 :: tail) blocks_pos) →
          ((k : ℕ) →
              (l : List ℕ) → (blocks_pos : ∀ {i : ℕ}, i ∈ (k + 1) :: l → 0 < i) → motive (k.succ :: l) blocks_pos) →
            motive blocks blocks_pos
-- Lean.Server.References
/-- Yields the definition location of `ident`.  -/
Lean.Server.References.definitionOf? : Lean.Server.References → Lean.Lsp.RefIdent → Option Lean.Server.References.DocumentRefInfo
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.Precylinder.unop_P : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Cᵒᵖ} (P : HomotopicalAlgebra.Precylinder A),
  P.unop.P = Opposite.unop P.I
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PullbackObjObj.ofIsInitial_fst : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  (G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)) {X₁ Y₁ : C₁} (f₁ : X₁ ⟶ Y₁) {X₃ Y₃ : C₃}
  (f₃ : X₃ ⟶ Y₃)
  [inst_3 : CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) (G.flip.obj X₃)]
  [inst_4 : CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) (G.flip.obj Y₃)]
  (h : CategoryTheory.Limits.IsInitial X₁),
  (CategoryTheory.Functor.PullbackObjObj.ofIsInitial G f₁ f₃ h).fst =
    (CategoryTheory.Limits.IsTerminal.isTerminalObj (G.flip.obj X₃) (Opposite.op X₁)
          (CategoryTheory.Limits.IsInitial.op C₁ h)).from
      ((G.obj (Opposite.op Y₁)).obj Y₃)
-- Mathlib.RingTheory.KrullDimension.PID
IsPrincipalIdealRing.krullDimLE_one : ∀ (R : Type u_1) [inst : CommRing R] [IsPrincipalIdealRing R], Ring.KrullDimLE 1 R
-- Mathlib.CategoryTheory.Join.Pseudofunctor
_private.Mathlib.CategoryTheory.Join.Pseudofunctor.0.CategoryTheory.Join.id.match_1.splitter : {C : Type u_3} →
  [inst : CategoryTheory.Category.{u_1, u_3} C] →
    {D : Type u_4} →
      [inst_1 : CategoryTheory.Category.{u_2, u_4} D] →
        (motive : CategoryTheory.Join C D → Sort u_5) →
          (x : CategoryTheory.Join C D) →
            ((x : C) → motive (CategoryTheory.Join.left x)) →
              ((x : D) → motive (CategoryTheory.Join.right x)) → motive x
-- Mathlib.Topology.Algebra.Monoid
Pi.separatelyContinuousAdd : ∀ {ι : Type u_1} {C : ι → Type u_6} [inst : (i : ι) → TopologicalSpace (C i)] [inst_1 : (i : ι) → Add (C i)]
  [∀ (i : ι), SeparatelyContinuousAdd (C i)], SeparatelyContinuousAdd ((i : ι) → C i)
-- Mathlib.Topology.Order.LawsonTopology
Topology.lawsonClosed_of_scottClosed : ∀ {α : Type u_1} [inst : Preorder α] (s : Set α),
  IsClosed (⇑Topology.WithScott.ofScott ⁻¹' s) → IsClosed (⇑Topology.WithLawson.ofLawson ⁻¹' s)
-- Mathlib.Order.Filter.Basic
Filter.eventually_iff_exists_mem : ∀ {α : Type u} {p : α → Prop} {f : Filter α}, (∀ᶠ (x : α) in f, p x) ↔ ∃ v ∈ f, ∀ y ∈ v, p y
-- Mathlib.Order.Minimal
minimal_mem_Icc : ∀ {α : Type u_2} {x : α} [inst : PartialOrder α] {a b : α}, a ≤ b → (Minimal (fun x => x ∈ Set.Icc a b) x ↔ x = a)
-- Mathlib.Data.PFunctor.Multivariate.Basic
MvPFunctor.instLawfulMvFunctorObj : ∀ {n : ℕ} (P : MvPFunctor.{u} n), LawfulMvFunctor ↑P
-- Mathlib.Algebra.Order.Archimedean.Real.Basic
/-- As `sSup s = 0` when `s` is an empty set of reals, it suffices to show that all elements of `s`
are nonpositive to show that `sSup s ≤ 0`.  -/
Real.sSup_nonpos : ∀ {s : Set ℝ}, (∀ x ∈ s, x ≤ 0) → sSup s ≤ 0
-- Mathlib.Data.Set.Sigma
Set.fst_image_sigma_subset : ∀ {ι : Type u_1} {α : ι → Type u_3} (s : Set ι) (t : (i : ι) → Set (α i)), Sigma.fst '' s.sigma t ⊆ s
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.norm_eq_of_norm_sub_lt_right : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {z1 z2 : ℚ_[p]}, ‖z1 - z2‖ < ‖z2‖ → ‖z1‖ = ‖z2‖
-- Mathlib.GroupTheory.Coprod.Basic
AddEquiv.coprodComm.eq_1 : ∀ (M : Type u_1) (N : Type u_2) [inst : AddZeroClass M] [inst_1 : AddZeroClass N],
  AddEquiv.coprodComm M N = (AddMonoid.Coprod.swap M N).toAddEquiv (AddMonoid.Coprod.swap N M) ⋯ ⋯
-- Lean.Meta.Tactic.Induction
Lean.Meta.instInhabitedInductionSubgoal : Inhabited Lean.Meta.InductionSubgoal
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.ofSimplex_ι : ∀ {X : SSet} (x : X.obj (Opposite.op { len := 0 })), (SSet.Subcomplex.ofSimplex x).ι = SSet.const x
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
CategoryTheory.CardinalDirectedPoset.instHasTerminalElemCarrierObjPartOrdEmbIsCardinalFilteredWithTopValSetPropSetWithTop : ∀ {κ : Cardinal.{u}} [inst : Fact κ.IsRegular] (J : CategoryTheory.CardinalDirectedPoset κ) (κ' : Cardinal.{u})
  [inst_1 : Fact κ'.IsRegular] (S : Subtype (J.PropSetWithTop κ')), CategoryTheory.Limits.HasTerminal ↑↑S
-- Std.Sat.AIG.Basic
Std.Sat.AIG.Decl.gate.inj : ∀ {α : Type} {l r l_1 r_1 : Std.Sat.AIG.Fanin},
  Std.Sat.AIG.Decl.gate l r = Std.Sat.AIG.Decl.gate l_1 r_1 → l = l_1 ∧ r = r_1
-- Mathlib.CategoryTheory.Limits.WeakLimits.Basic
CategoryTheory.Limits.weakLimit.isWeakLimit_lift : ∀ {J : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} J] {C : Type u_3}
  [inst_1 : CategoryTheory.Category.{v_3, u_3} C] {F : CategoryTheory.Functor J C}
  [inst_2 : CategoryTheory.Limits.HasWeakLimit F] (c : CategoryTheory.Limits.Cone F),
  (CategoryTheory.Limits.weakLimit.isWeakLimit F).lift c = CategoryTheory.Limits.weakLimit.lift F c
-- Mathlib.RingTheory.Grassmannian
Module.Grassmannian.mk : {R : Type u} →
  [inst : CommRing R] →
    {M : Type v} →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          {k : ℕ} →
            (toSubmodule : Submodule R M) →
              Module.Finite R (M ⧸ toSubmodule) →
                Module.Projective R (M ⧸ toSubmodule) →
                  (∀ (p : PrimeSpectrum R), Module.rankAtStalk (M ⧸ toSubmodule) p = k) → Module.Grassmannian R M k
-- Init.Data.Int.Linear
Int.Internal.Linear.eq_dvd_subst_cert.eq_1 : ∀ (x : Int.Internal.Linear.Var) (p₁ : Int.Internal.Linear.Poly) (d₂ : ℤ) (p₂ : Int.Internal.Linear.Poly) (d₃ : ℤ)
  (p₃ : Int.Internal.Linear.Poly),
  Int.Internal.Linear.eq_dvd_subst_cert x p₁ d₂ p₂ d₃ p₃ =
    (d₃.beq' (Int.Internal.Linear.abs (p₁.coeff_k x * d₂))).and'
      (p₃.beq'
        (Int.Internal.Linear.Poly.combine_mul_k (p₁.coeff_k x) (-p₂.coeff_k x)
          (Int.Internal.Linear.Poly.insert (-p₂.coeff_k x) x p₂)
          (Int.Internal.Linear.Poly.insert (-p₁.coeff_k x) x p₁)))
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.Hom.comm₂₃_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {S₁ S₂ : CategoryTheory.ShortComplex.SnakeInput C} (self : S₁.Hom S₂) {Z : CategoryTheory.ShortComplex C}
  (h : S₂.L₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.f₂ (CategoryTheory.CategoryStruct.comp S₂.v₂₃ h) =
    CategoryTheory.CategoryStruct.comp S₁.v₂₃ (CategoryTheory.CategoryStruct.comp self.f₃ h)
-- Lean.Meta.Basic
Lean.Meta.ProjReductionKind.yesWithDelta.sizeOf_spec : sizeOf Lean.Meta.ProjReductionKind.yesWithDelta = 1
-- Init.Data.Nat.Dvd
Nat.dvd_mul_right : ∀ (a b : ℕ), a ∣ a * b
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.mk.injEq : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_4} {V₂ : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : Module k V₁] [inst_4 : Module k V₂]
  [inst_5 : AddTorsor V₁ P₁] [inst_6 : AddTorsor V₂ P₂] (toEquiv : P₁ ≃ P₂) (linear : V₁ ≃ₗ[k] V₂)
  (map_vadd' : ∀ (p : P₁) (v : V₁), toEquiv (v +ᵥ p) = linear v +ᵥ toEquiv p) (toEquiv_1 : P₁ ≃ P₂)
  (linear_1 : V₁ ≃ₗ[k] V₂) (map_vadd'_1 : ∀ (p : P₁) (v : V₁), toEquiv_1 (v +ᵥ p) = linear_1 v +ᵥ toEquiv_1 p),
  ({ toEquiv := toEquiv, linear := linear, map_vadd' := map_vadd' } =
      { toEquiv := toEquiv_1, linear := linear_1, map_vadd' := map_vadd'_1 }) =
    (toEquiv = toEquiv_1 ∧ linear = linear_1)
-- Mathlib.Combinatorics.SimpleGraph.Matching
SimpleGraph.Subgraph.isMatching_iff_forall_degree : ∀ {V : Type u_1} {G : SimpleGraph V} {M : G.Subgraph} [inst : (v : V) → Fintype ↑(M.neighborSet v)],
  M.IsMatching ↔ ∀ v ∈ M.verts, M.degree v = 1
-- Mathlib.Algebra.Homology.CommSq
CategoryTheory.CommSq.shortComplex_X₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {X₁ X₂ X₃ X₄ : C}
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X₂ X₃] {f : X₁ ⟶ X₂} {g : X₁ ⟶ X₃} {inl : X₂ ⟶ X₄} {inr : X₃ ⟶ X₄}
  (sq : CategoryTheory.CommSq f g inl inr), sq.shortComplex.X₃ = X₄
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.instAddAction : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Ring R] →
      [inst_1 : Ring S] →
        {σ : R →+* S} →
          {E : Type u_4} →
            [inst_2 : AddCommGroup E] →
              [inst_3 : Module R E] →
                {F : Type u_5} →
                  [inst_4 : AddCommGroup F] → [inst_5 : Module S F] → AddAction (E →ₛₗ[σ] F) (E →ₛₗ.[σ] F)
-- Mathlib.Analysis.Normed.Group.Constructions
ULift.norm_def : ∀ {E : Type u_2} [inst : Norm E] (x : ULift.{u_5, u_2} E), ‖x‖ = ‖x.down‖
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.BoundedFormula.realize_rel₂ : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {l : ℕ} {v : α → M} {xs : Fin l → M}
  {R : L.Relations 2} {t₁ t₂ : L.Term (α ⊕ Fin l)},
  (R.boundedFormula₂ t₁ t₂).Realize v xs ↔
    FirstOrder.Language.Structure.RelMap R
      ![FirstOrder.Language.Term.realize (Sum.elim v xs) t₁, FirstOrder.Language.Term.realize (Sum.elim v xs) t₂]
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.mem_map : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [inst_2 : FunLike F M N]
  [mc : MonoidHomClass F M N] {f : F} {S : Submonoid M} {y : N}, y ∈ Submonoid.map f S ↔ ∃ x ∈ S, f x = y
-- Mathlib.Algebra.Ring.Submonoid.Pointwise
AddSubmonoid.mul_iSup : ∀ {R : Type u_2} [inst : NonUnitalNonAssocSemiring R] {ι : Sort u_4} (T : AddSubmonoid R) (S : ι → AddSubmonoid R),
  T * ⨆ i, S i = ⨆ i, T * S i
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.two_le_iff_one_lt : ∀ {c : Cardinal.{u_1}}, 2 ≤ c ↔ 1 < c
-- Mathlib.CategoryTheory.Monoidal.Hopf_
CategoryTheory.HopfObj.antipode_left_assoc : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  {inst_2 : CategoryTheory.BraidedCategory C} (X : C) [self : CategoryTheory.HopfObj X] {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.HopfObj.antipode X)
        (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul h)) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.counit
      (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one h)
-- Mathlib.Algebra.Polynomial.Degree.SmallDegree
Polynomial.natDegree_quadratic_le : ∀ {R : Type u} {a b c : R} [inst : Semiring R],
  (Polynomial.C a * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c).natDegree ≤ 2
-- Mathlib.Geometry.Manifold.VectorBundle.Tangent
tangentBundle_model_space_coe_chartAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_4} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H}
  (p : TangentBundle I H), ↑(chartAt (ModelProd H E) p) = ⇑(Bundle.TotalSpace.toProd H E)
-- Init.System.FilePath
_private.Init.System.FilePath.0.System.FilePath.normalize.normalizeDriveLetter : System.FilePath → System.FilePath
-- Mathlib.CategoryTheory.Abelian.LeftDerived
CategoryTheory.Functor.leftDerivedZeroIsoSelf_inv_hom_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.HasProjectiveResolutions C]
  [inst_4 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [inst_5 : F.Additive]
  [inst_6 : CategoryTheory.Limits.PreservesFiniteColimits F],
  CategoryTheory.CategoryStruct.comp F.leftDerivedZeroIsoSelf.inv F.fromLeftDerivedZero =
    CategoryTheory.CategoryStruct.id F
-- Mathlib.CategoryTheory.Generator.Basic
/-- Given `P : ObjectProperty C` and `X : C`, this is the coproduct of
all the morphisms `Y ⟶ X` such that `P Y` holds.  -/
CategoryTheory.ObjectProperty.coproductFrom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (P : CategoryTheory.ObjectProperty C) →
      (X : C) → [inst_1 : CategoryTheory.Limits.HasCoproduct (P.coproductFromFamily X)] → ∐ P.coproductFromFamily X ⟶ X
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomAddAct.toEquiv_mkHomeomorph : ∀ {M : Type u_1} [inst : TopologicalSpace M], DomAddAct.mkHomeomorph.toEquiv = DomAddAct.mk
-- Mathlib.Tactic.Ring.Basic
Mathlib.Tactic.Ring.natCast_zero : ∀ {R : Type u_1} [inst : CommSemiring R], ↑0 = 0
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
FormalMultilinearSeries.removeZero_of_pos : ∀ {𝕜 : Type u} {E : Type v} {F : Type w} [inst : Semiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [inst_4 : ContinuousAdd E] [inst_5 : ContinuousConstSMul 𝕜 E] [inst_6 : AddCommMonoid F]
  [inst_7 : Module 𝕜 F] [inst_8 : TopologicalSpace F] [inst_9 : ContinuousAdd F] [inst_10 : ContinuousConstSMul 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ}, 0 < n → p.removeZero n = p n
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
mul_nonneg_iff_of_pos_left : ∀ {R : Type u} [inst : Semiring R] [inst_1 : LinearOrder R] {b c : R} [PosMulStrictMono R], 0 < c → (0 ≤ c * b ↔ 0 ≤ b)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
WeierstrassCurve.Affine.evalEval_negPolynomial : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} (x y : R),
  Polynomial.evalEval x y W'.negPolynomial = W'.negY x y
-- Init.Omega.LinearCombo
/-- Constant term.  -/
Lean.Omega.LinearCombo.const : Lean.Omega.LinearCombo → ℤ
-- Mathlib.Algebra.Order.Interval.Set.SuccPred
Set.Icc_sub_one_right_eq_Ico_of_not_isMin : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : Sub α] [PredSubOrder α] {b : α},
  ¬IsMin b → ∀ (a : α), Set.Icc a (b - 1) = Set.Ico a b
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
/-- Auxiliary function to constructing a linear map `(⨂[R] i, s i) → E` given a
`MultilinearMap R s E` with the property that its composition with the canonical
`MultilinearMap R s (⨂[R] i, s i)` is the given multilinear map.  -/
PiTensorProduct.liftAux : {ι : Type u_1} →
  {R : Type u_4} →
    [inst : CommSemiring R] →
      {s : ι → Type u_7} →
        [inst_1 : (i : ι) → AddCommMonoid (s i)] →
          [inst_2 : (i : ι) → Module R (s i)] →
            {E : Type u_9} →
              [inst_3 : AddCommMonoid E] →
                [inst_4 : Module R E] → MultilinearMap R s E → (PiTensorProduct R fun i => s i) →+ E
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.π_comp_leftHomologyIso_inv_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData) [inst_2 : S.HasLeftHomology] {Z : C}
  (h_1 : S.leftHomology ⟶ Z),
  CategoryTheory.CategoryStruct.comp h.π (CategoryTheory.CategoryStruct.comp h.leftHomologyIso.inv h_1) =
    CategoryTheory.CategoryStruct.comp h.cyclesIso.inv (CategoryTheory.CategoryStruct.comp S.leftHomologyπ h_1)
-- Init.Data.List.MinMaxIdx
_private.Init.Data.List.MinMaxIdx.0.List.minIdxOn?.eq_2 : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] (f : α → β) (y : α) (ys : List α),
  List.minIdxOn? f (y :: ys) = some (List.minIdxOn f (y :: ys) ⋯)
-- Init.Data.UInt.Lemmas
UInt16.toNat_mul : ∀ (a b : UInt16), (a * b).toNat = a.toNat * b.toNat % 2 ^ 16
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
_private.Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances.0.termσₙ : Lean.ParserDescr
-- Mathlib.RingTheory.Localization.NumDen
IsFractionRing.num_den_unique : ∀ (A : Type u_1) [inst : CommRing A] [inst_1 : IsDomain A] [inst_2 : UniqueFactorizationMonoid A] {K : Type u_2}
  [inst_3 : Field K] [inst_4 : Algebra A K] [inst_5 : IsFractionRing A K] (x : K) (n : A) (d : ↥(nonZeroDivisors A)),
  IsRelPrime n ↑d →
    IsLocalization.mk' K n d = x → Associated (IsFractionRing.num A x) n ∧ Associated ↑(IsFractionRing.den A x) ↑d
-- Mathlib.Algebra.Group.Subgroup.Ker
/-- **Alias** of `AddMonoidHom.ker_domRestrict`. -/
AddMonoidHom.ker_restrict : ∀ {G : Type u_1} [inst : AddGroup G] (K : AddSubgroup G) {M : Type u_7} [inst_1 : AddZeroClass M] (f : G →+ M),
  (f.domRestrict K).ker = f.ker.addSubgroupOf K
-- Mathlib.Algebra.Algebra.RestrictScalars
RestrictScalars.smul_def : ∀ (R : Type u_1) (S : Type u_2) (M : Type u_3) [inst : AddCommMonoid M] [inst_1 : CommSemiring R] [inst_2 : Semiring S]
  [inst_3 : Algebra R S] [inst_4 : Module S M] (c : R) (x : RestrictScalars R S M),
  c • x = (RestrictScalars.addEquiv R S M).symm ((algebraMap R S) c • (RestrictScalars.addEquiv R S M) x)
-- Mathlib.Data.NNReal.Defs
NNReal.coe_iInf : ∀ {ι : Sort u_2} (s : ι → NNReal), ↑(⨅ i, s i) = ⨅ i, ↑(s i)
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
AEMeasurable.of_discrete : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [inst : MeasurableSpace β] {f : α → β}
  {μ : MeasureTheory.Measure α} [DiscreteMeasurableSpace α], AEMeasurable f μ
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- Swapping the first and third points in an oriented angle negates the sign of that angle.  -/
EuclideanGeometry.oangle_swap₁₃_sign : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  (p₁ p₂ p₃ : P), -(EuclideanGeometry.oangle p₁ p₂ p₃).sign = (EuclideanGeometry.oangle p₃ p₂ p₁).sign
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
/-- Cached `getDecLevel type`  -/
Lean.Meta.Grind.Arith.CommRing.Ring.u : Lean.Meta.Grind.Arith.CommRing.Ring → Lean.Level
-- Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess
_private.Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess.0.Finset.monotone_orderEmbOfFinWithBot : ∀ {T : Type u_1} [inst : LinearOrder T] (I : Finset T) [inst_1 : OrderBot T], Monotone (Finset.orderEmbOfFinWithBot✝ I)
-- Mathlib.Order.Partition.Basic
Partition.IsRepFun.mapsTo : ∀ {α : Type u_1} {s u : Set α} {P : Partition u} {f : α → α}, P.IsRepFun f → u ⊆ s → Set.MapsTo f s s
-- Mathlib.Algebra.Lie.Weights.RootSystem
LieAlgebra.IsKilling.reflectRoot.congr_simp : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : CharZero K] [inst_2 : LieRing L] [inst_3 : LieAlgebra K L]
  [inst_4 : LieAlgebra.IsKilling K L] [inst_5 : FiniteDimensional K L] {H : LieSubalgebra K L}
  [inst_6 : H.IsCartanSubalgebra] [inst_7 : LieModule.IsTriangularizable K (↥H) L] (α α_1 : LieModule.Weight K (↥H) L),
  α = α_1 →
    ∀ (β β_1 : LieModule.Weight K (↥H) L),
      β = β_1 → LieAlgebra.IsKilling.reflectRoot α β = LieAlgebra.IsKilling.reflectRoot α_1 β_1
-- Mathlib.Analysis.Normed.Module.Dual
/-- If `x'` is a `StrongDual 𝕜 E` element such that the norms `‖x' z‖` are bounded for `z ∈ s`, then
a small scalar multiple of `x'` is in `polar 𝕜 s`.  -/
NormedSpace.smul_mem_polar : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E} {x' : StrongDual 𝕜 E} {c : 𝕜},
  (∀ z ∈ s, ‖x' z‖ ≤ ‖c‖) → c⁻¹ • x' ∈ StrongDual.polar 𝕜 s