mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Module.TransferInstance
/-- Transfer `Module` across an `Equiv`  -/
Equiv.module : (R : Type u_1) →
  {α : Type u_2} →
    {β : Type u_3} → [inst : Semiring R] → (e : α ≃ β) → [inst_1 : AddCommMonoid β] → [Module R β] → Module R α
-- Mathlib.Data.Real.ConjExponents
ENNReal.HolderConjugate.toNNReal_iff : ∀ {p q : ENNReal}, 1 < p.toNNReal → (p.toNNReal.HolderConjugate q.toNNReal ↔ p.HolderConjugate q)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.mk : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S : CategoryTheory.ShortComplex C} →
        (K H : C) →
          (i : K ⟶ S.X₂) →
            (π : K ⟶ H) →
              (wi : CategoryTheory.CategoryStruct.comp i S.g = 0) →
                (hi : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι i wi)) →
                  (wπ :
                      CategoryTheory.CategoryStruct.comp (hi.lift (CategoryTheory.Limits.KernelFork.ofι S.f ⋯)) π = 0) →
                    CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ π wπ) → S.LeftHomologyData
-- Mathlib.Analysis.InnerProductSpace.Reproducing
/-- The "reproducing" property of the kernel functions, left version.  -/
RKHS.kerFun_inner : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {X : Type u_2} {V : Type u_3} [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] {H : Type u_4} [inst_3 : NormedAddCommGroup H] [inst_4 : InnerProductSpace 𝕜 H]
  [inst_5 : RKHS 𝕜 H X V] [inst_6 : CompleteSpace H] [inst_7 : CompleteSpace V] (x : X) (v : V) (f : H),
  inner 𝕜 ((RKHS.kerFun H x) v) f = inner 𝕜 v (f x)
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.kernelIsIsoComp_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y Z : C}
  (f : X ⟶ Y) (g : Y ⟶ Z) [inst_2 : CategoryTheory.IsIso f] [inst_3 : CategoryTheory.Limits.HasKernel g],
  (CategoryTheory.Limits.kernelIsIsoComp f g).hom =
    CategoryTheory.Limits.kernel.lift g
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι (CategoryTheory.CategoryStruct.comp f g)) f) ⋯
-- Mathlib.Algebra.Group.Submonoid.Units
AddSubgroup.addUnit_of_mem_ofAddUnits.eq_1 : ∀ {M : Type u_1} [inst : AddMonoid M] (S : AddSubgroup (AddUnits M)) {x : M} (h : x ∈ S.ofAddUnits),
  S.addUnit_of_mem_ofAddUnits h = (Classical.choose h).copy x ⋯ ↑(-Classical.choose h) ⋯
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.equiv_inv_hom_apply_pt : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor J C) (c : (X : Cᵒᵖ) × ((CategoryTheory.Functor.const J).obj (Opposite.unop X) ⟶ F)),
  ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Cone.equiv F).inv) c).pt = Opposite.unop c.fst
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.sheafPushforwardContinuous.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F F_1 : CategoryTheory.Functor C D) (e_F : F = F_1) (A : Type u) [inst_2 : CategoryTheory.Category.{t, u} A]
  (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [inst_3 : F.IsContinuous J K],
  F.sheafPushforwardContinuous A J K = F_1.sheafPushforwardContinuous A J K
-- Mathlib.Data.Finset.Max
Finset.max_le : ∀ {α : Type u_2} [inst : LinearOrder α] {M : WithBot α} {s : Finset α}, (∀ a ∈ s, ↑a ≤ M) → s.max ≤ M
-- Mathlib.Analysis.InnerProductSpace.PiL2
DirectSum.IsInternal.collectedOrthonormalBasis_mem : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] {A : ι → Submodule 𝕜 E} [inst_4 : DecidableEq ι]
  (h : DirectSum.IsInternal A) {α : ι → Type u_7} [inst_5 : (i : ι) → Fintype (α i)]
  (hV : OrthogonalFamily 𝕜 (fun i => ↥(A i)) fun i => (A i).subtypeₗᵢ) (v : (i : ι) → OrthonormalBasis (α i) 𝕜 ↥(A i))
  (a : (i : ι) × α i), (DirectSum.IsInternal.collectedOrthonormalBasis hV h v) a ∈ A a.fst
-- Mathlib.Analysis.Meromorphic.Order
/-- The order of a function `f` equals the order of `-f`.  -/
meromorphicOrderAt_fun_neg : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : 𝕜} {f : 𝕜 → E}, meromorphicOrderAt f x = meromorphicOrderAt (fun z => -f z) x
-- Init.Data.SInt.Lemmas
ISize.toInt64_ofIntLE : ∀ {n : ℤ} (h₁ : ISize.minValue.toInt ≤ n) (h₂ : n ≤ ISize.maxValue.toInt),
  (ISize.ofIntLE n h₁ h₂).toInt64 = Int64.ofIntLE n ⋯ ⋯
-- Mathlib.Analysis.Convex.Strong
StrongConvexOn.eq_1 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (s : Set E) (m : ℝ),
  StrongConvexOn s m = UniformConvexOn s fun r => m / 2 * r ^ 2
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Descent
Module.FaithfullyFlat.injective_of_tensorProduct : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {T : Type u_3}
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [Module.FaithfullyFlat R S],
  Function.Injective ⇑(algebraMap S (TensorProduct R S T)) → Function.Injective ⇑(algebraMap R T)
-- Mathlib.Analysis.Calculus.Deriv.Polynomial
Polynomial.hasFDerivWithinAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {s : Set 𝕜} (p : Polynomial 𝕜) (x : 𝕜),
  HasFDerivWithinAt (fun x => Polynomial.eval x p)
    (ContinuousLinearMap.smulRight 1 (Polynomial.eval x (Polynomial.derivative p))) s x
-- Mathlib.Topology.Algebra.StarSubalgebra
/-- The closure of a star subalgebra in a topological star algebra as a star subalgebra.  -/
StarSubalgebra.topologicalClosure : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : StarRing R] →
        [inst_2 : TopologicalSpace A] →
          [inst_3 : Semiring A] →
            [inst_4 : Algebra R A] →
              [inst_5 : StarRing A] →
                [inst_6 : StarModule R A] →
                  [IsSemitopologicalSemiring A] → [ContinuousStar A] → StarSubalgebra R A → StarSubalgebra R A
-- Mathlib.Data.Nat.Prime.Basic
Nat.Prime.not_prime_pow' : ∀ {x n : ℕ}, n ≠ 1 → ¬Nat.Prime (x ^ n)
-- Mathlib.Logic.Relation
Relation.reflTransGen_le_of_le : ∀ {α : Type u_1} {r r' : α → α → Prop} [Std.Refl r] [IsTrans α r], r' ≤ r → Relation.ReflTransGen r' ≤ r
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.NeWord.replaceHead.eq_1 : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] (x : ι) (x_1 : M x) (x_2 : x_1 ≠ 1) (x_7 : M x)
  (a : x_7 ≠ 1),
  Monoid.CoprodI.NeWord.replaceHead x_1 x_2 (Monoid.CoprodI.NeWord.singleton x_7 a) =
    Monoid.CoprodI.NeWord.singleton x_1 x_2
-- Mathlib.Data.List.Cycle
List.prev_getElem : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α),
  l.Nodup → ∀ (i : ℕ) (hi : i < l.length), l.prev l[i] ⋯ = l[(i + (l.length - 1)) % l.length]
-- Mathlib.RingTheory.FormalGroup.Basic
FormalGroup.Xzero.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (F : FormalGroup R),
  F.Xzero = MvPowerSeries.subst ![PowerSeries.X, 0] F.toPowerSeries
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.strictAnti_rpow_of_base_lt_one : ∀ {b : ℝ}, 0 < b → b < 1 → StrictAnti fun x => b ^ x
-- Mathlib.CategoryTheory.Retract
CategoryTheory.Retract.retract : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (self : CategoryTheory.Retract X Y),
  CategoryTheory.CategoryStruct.comp self.i self.r = CategoryTheory.CategoryStruct.id X
-- Init.Data.SInt.Lemmas
ISize.toInt32_add : ∀ (a b : ISize), (a + b).toInt32 = a.toInt32 + b.toInt32
-- Mathlib.NumberTheory.RamificationInertia.Ramification
/-- **Alias** of `Ideal.le_pow_ramificationIdx'`. -/
Ideal.le_pow_ramificationIdx : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] {p : Ideal R}
  {P : Ideal S}, Ideal.map (algebraMap R S) p ≤ P ^ p.ramificationIdx' P
-- Mathlib.Data.ZMod.ValMinAbs
ZMod.injective_valMinAbs : ∀ {n : ℕ}, Function.Injective ZMod.valMinAbs
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.smul_finset_subset_smul : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : SMul α β] {t : Finset β} {a : α} {s : Finset α},
  a ∈ s → a • t ⊆ s • t
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.sPolynomial_leadingTerm_mul : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommRing R] [NoZeroDivisors R]
  (p₁ p₂ q₁ q₂ : MvPolynomial σ R),
  m.sPolynomial (m.leadingTerm p₁ * q₁) (m.leadingTerm p₂ * q₂) =
    (MvPolynomial.monomial ((m.degree p₁ + m.degree q₁) ⊔ (m.degree p₂ + m.degree q₂) - m.degree q₁ ⊔ m.degree q₂))
        (m.leadingCoeff p₁ * m.leadingCoeff p₂) *
      m.sPolynomial q₁ q₂
-- Mathlib.RingTheory.DividedPowers.DPMorphism
DividedPowers.DPMorphism.fromGens_coe : ∀ {A : Type u_3} {B : Type u_4} [inst : CommSemiring A] [inst_1 : CommSemiring B] {I : Ideal A} {J : Ideal B}
  (hI : DividedPowers I) (hJ : DividedPowers J) {f : A →+* B} {S : Set A} (hS : I = Ideal.span S)
  (hf : Ideal.map f I ≤ J) (h : ∀ {n : ℕ}, ∀ x ∈ S, f (hI.dpow n x) = hJ.dpow n (f x)),
  (DividedPowers.DPMorphism.fromGens hI hJ hS hf ⋯).toRingHom = f
-- Mathlib.Order.LiminfLimsup
Filter.limsup_eq_iInf_iSup_of_nat : ∀ {α : Type u_1} [inst : CompleteLattice α] {u : ℕ → α}, Filter.limsup u Filter.atTop = ⨅ n, ⨆ i, ⨆ (_ : i ≥ n), u i
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rco.mem_toList_iff_mem : ∀ {α : Type u} {r : Std.Rco α} [inst : LE α] [inst_1 : LT α] [inst_2 : DecidableLT α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLT α] [Std.PRange.LawfulUpwardEnumerableLE α] [inst_7 : Std.Rxo.IsAlwaysFinite α]
  {a : α}, a ∈ r.toList ↔ a ∈ r
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SignatureHelp.mk.injEq : ∀ (signatures : Array Lean.Lsp.SignatureInformation) (activeSignature? activeParameter? : Option ℕ)
  (signatures_1 : Array Lean.Lsp.SignatureInformation) (activeSignature?_1 activeParameter?_1 : Option ℕ),
  ({ signatures := signatures, activeSignature? := activeSignature?, activeParameter? := activeParameter? } =
      { signatures := signatures_1, activeSignature? := activeSignature?_1, activeParameter? := activeParameter?_1 }) =
    (signatures = signatures_1 ∧ activeSignature? = activeSignature?_1 ∧ activeParameter? = activeParameter?_1)
-- Init.Data.UInt.Lemmas
UInt8.toUInt16_inj : ∀ {a b : UInt8}, a.toUInt16 = b.toUInt16 ↔ a = b
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.lt_rootMultiplicity_iff_isRoot_iterate_derivative_of_mem_nonZeroDivisors : ∀ {R : Type u} [inst : CommRing R] {p : Polynomial R} {t : R} {n : ℕ},
  p ≠ 0 →
    ↑n.factorial ∈ nonZeroDivisors R →
      (n < Polynomial.rootMultiplicity t p ↔ ∀ m ≤ n, ((⇑Polynomial.derivative)^[m] p).IsRoot t)
-- Mathlib.Analysis.SpecialFunctions.Exponential
/-- The exponential in a Banach algebra `𝔸` over a normed field `𝕂` has Fréchet derivative
`1 : 𝔸 →L[𝕂] 𝔸` at zero, as long as it converges on a neighborhood of zero.  -/
hasFDerivAt_exp_zero_of_radius_pos : ∀ {𝕂 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕂] [inst_1 : NormedRing 𝔸] [CharZero 𝕂]
  [inst_3 : NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸],
  0 < (NormedSpace.expSeries 𝕂 𝔸).radius → HasFDerivAt NormedSpace.exp 1 0
-- Mathlib.Analysis.Normed.Group.Basic
preimage_mul_ball : ∀ {E : Type u_5} [inst : SeminormedCommGroup E] (a b : E) (r : ℝ),
  (fun x => b * x) ⁻¹' Metric.ball a r = Metric.ball (a / b) r
-- Mathlib.Algebra.Category.Ring.Basic
CommSemiRingCat.hom_ofHom : ∀ {R S : Type u} [inst : CommSemiring R] [inst_1 : CommSemiring S] (f : R →+* S),
  CommSemiRingCat.Hom.hom (CommSemiRingCat.ofHom f) = f
-- Mathlib.AlgebraicTopology.DoldKan.Normalized
AlgebraicTopology.DoldKan.PInfty_comp_PInftyToNormalizedMooreComplex : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] [inst_1 : CategoryTheory.Abelian A]
  (X : CategoryTheory.SimplicialObject A),
  CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.PInfty
      (AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex X) =
    AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex X
-- Mathlib.Analysis.Calculus.FDeriv.Const
differentiable_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] (c : F), Differentiable 𝕜 fun x => c
-- Mathlib.Algebra.Lie.Abelian
LieAlgebra.isLieAbelian_iff_center_eq_top : ∀ (R : Type u) (L : Type v) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L],
  IsLieAbelian L ↔ LieAlgebra.center R L = ⊤
-- Init.Control.State
/-- Sequences two actions. Typically used via the `>>=` operator.
 -/
StateT.bind : {σ : Type u} → {m : Type u → Type v} → [Monad m] → {α β : Type u} → StateT σ m α → (α → StateT σ m β) → StateT σ m β
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Cat
CategoryTheory.Bicategory.Adj.left_triangle_components : ∀ {C₁ C₂ : CategoryTheory.Bicategory.Adj CategoryTheory.Cat} (α : C₁ ⟶ C₂) (X : ↑C₁.obj),
  CategoryTheory.CategoryStruct.comp (α.l.toFunctor.map (α.adj.unit.toNatTrans.app X))
      (α.adj.counit.toNatTrans.app (α.l.toFunctor.obj X)) =
    CategoryTheory.CategoryStruct.id (α.l.toFunctor.obj X)
-- Mathlib.Topology.Algebra.Support
HasCompactSupport.list_sum : ∀ {α : Type u_9} {β : Type u_10} [inst : TopologicalSpace α] [inst_1 : AddMonoid β] {l : List (α → β)},
  (∀ f ∈ l, HasCompactSupport f) → HasCompactSupport l.sum
-- Init.Data.Array.Monadic
Array.flatMapM_unattach : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {P : α → Prop}
  {xs : Array (Subtype P)} {f : α → m (Array β)},
  Array.flatMapM f xs.unattach =
    Array.flatMapM
      (fun x =>
        match x with
        | ⟨x, h⟩ => binderNameHint x f (binderNameHint h () (f (wfParam x))))
      xs
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.IsSwap.mul_mem_closure_three_cycles : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {σ τ : Equiv.Perm α},
  σ.IsSwap → τ.IsSwap → σ * τ ∈ Subgroup.closure {σ | σ.IsThreeCycle}
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
MeasureTheory.Measure.tendsto_addHaar_inter_smul_one_of_density_one_aux : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (s : Set E),
  MeasurableSet s →
    ∀ (x : E),
      Filter.Tendsto (fun r => μ (s ∩ Metric.closedBall x r) / μ (Metric.closedBall x r)) (nhdsWithin 0 (Set.Ioi 0))
          (nhds 1) →
        ∀ (t : Set E),
          MeasurableSet t →
            μ t ≠ 0 →
              μ t ≠ ⊤ →
                Filter.Tendsto (fun r => μ (s ∩ ({x} + r • t)) / μ ({x} + r • t)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 1)
-- Mathlib.Data.Fin.Fin2
/-- Converts a natural into a `Fin2` if it is in range  -/
Fin2.optOfNat : {n : ℕ} → ℕ → Option (Fin2 n)
-- Init.Data.List.Lemmas
List.contains_iff_exists_mem_beq : ∀ {α : Type u_1} [inst : BEq α] {l : List α} {a : α}, l.contains a = true ↔ ∃ a' ∈ l, (a == a') = true
-- Mathlib.Order.Hom.CompleteLattice
/-- Reinterpret a `FrameHom` as a `LatticeHom`.  -/
FrameHom.toLatticeHom : {α : Type u_2} →
  {β : Type u_3} → [inst : CompleteLattice α] → [inst_1 : CompleteLattice β] → FrameHom α β → LatticeHom α β
-- Mathlib.Algebra.Group.Hom.Defs
OneHom.inverse_apply : ∀ {M : Type u_4} {N : Type u_5} [inst : One M] [inst_1 : One N] (f : OneHom M N) (g : N → M)
  (h₁ : Function.LeftInverse g ⇑f) (a : N), (f.inverse g h₁) a = g a
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalRightAction.monoidalOppositeRightAction_actionRight_mop : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (c : C) {d d' : D} (f : d ⟶ d'),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f { unmop := c } =
    CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c f
-- Mathlib.Tactic.Simproc.FinsetInterval
_private.Mathlib.Tactic.Simproc.FinsetInterval.0.Mathlib.Tactic.Simp.Int.Ioc_eq_of_Icc_succ_eq : ∀ {m n : ℤ} {s : Finset ℤ}, Finset.Icc (m + 1) n = s → Finset.Ioc m n = s
-- Mathlib.Data.Set.Constructions
/-- This is a hybrid of `Set.biUnion_empty` and `Finset.biUnion_empty` (the index set on the LHS is
the empty finset, but `s` is a family of sets, not finsets).  -/
Set.biUnion_empty_finset : ∀ {ι : Type u_2} {X : Type u_3} {s : ι → Set X}, ⋃ i ∈ ∅, s i = ∅
-- Init.Grind.Norm
Lean.Grind.forall_and : ∀ {α : Sort u_1} {p q : α → Prop}, (∀ (x : α), p x ∧ q x) = ((∀ (x : α), p x) ∧ ∀ (x : α), q x)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.addX_of_Z_ne_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} [inst_1 : DecidableEq F] {P Q : Fin 3 → F},
  W.Equation P →
    W.Equation Q →
      P 2 ≠ 0 →
        Q 2 ≠ 0 →
          P 0 * Q 2 ^ 2 ≠ Q 0 * P 2 ^ 2 →
            W.addX P Q / WeierstrassCurve.Jacobian.addZ P Q ^ 2 =
              W.toAffine.addX (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2)
                (W.toAffine.slope (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) (Q 1 / Q 2 ^ 3))
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.coe_sSup : ∀ {α : Type u_1} [inst : LE α] (S : Set (LowerSet α)), ↑(sSup S) = ⋃ s ∈ S, ↑s
-- Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Real.concaveOn_negMulLog : ConcaveOn ℝ (Set.Ici 0) Real.negMulLog
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instInvolutiveInv.eq_1 : ∀ {α : Type u_1} [inst : InvolutiveInv α], Colex.instInvolutiveInv = { toInv := Colex.instInv, inv_inv := ⋯ }
-- Mathlib.Data.Fintype.Pi
Fintype.filter_piFinset_of_notMem : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {δ : α → Type u_4} [inst_2 : (a : α) → DecidableEq (δ a)]
  (t : (a : α) → Finset (δ a)) (a : α), ∀ x ∉ t a, {f ∈ Fintype.piFinset t | f a = x} = ∅
-- Init.Data.Option.Lemmas
Option.filter_guard : ∀ {α : Type u_1} {p q : α → Bool} {x : α}, Option.filter q (Option.guard p x) = Option.guard (fun y => p y && q y) x
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basis
Set.powersetCard.ofCard.congr_simp : ∀ {α : Type u_1} {n : ℕ} {s s_1 : Finset α} (e_s : s = s_1) (s_card : s.card = n),
  Set.powersetCard.ofCard s_card = Set.powersetCard.ofCard ⋯
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages
CategoryTheory.Limits.cokernel.mapIso.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasCokernel f] {X' Y' : C} (f' : X' ⟶ Y')
  [inst_3 : CategoryTheory.Limits.HasCokernel f'] (p p_1 : X ≅ X') (e_p : p = p_1) (q q_1 : Y ≅ Y') (e_q : q = q_1)
  (w : CategoryTheory.CategoryStruct.comp f q.hom = CategoryTheory.CategoryStruct.comp p.hom f'),
  CategoryTheory.Limits.cokernel.mapIso f f' p q w = CategoryTheory.Limits.cokernel.mapIso f f' p_1 q_1 ⋯
-- Mathlib.Analysis.Normed.Module.Bases
/-- The action of the projection on a vector.  -/
SchauderBasis.proj_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {X : Type u_2} [inst_1 : NormedAddCommGroup X]
  [inst_2 : NormedSpace 𝕜 X] (b : SchauderBasis 𝕜 X) (n : ℕ) (x : X),
  (b.proj n) x = ∑ i ∈ Finset.range n, (b.coord i) x • ↑b i
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.toPoly.eq_9 : ∀ (k : ℕ) (n : ℤ),
  ((Lean.Grind.CommRing.Expr.num n).pow k).toPoly =
    bif k == 0 then Lean.Grind.CommRing.Poly.num 1 else Lean.Grind.CommRing.Poly.num (n ^ k)
-- Mathlib.Order.Filter.AtTopBot.Archimedean
Filter.Eventually.ratCast_atTop : ∀ {R : Type u_2} [inst : Field R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [Archimedean R] {p : R → Prop},
  (∀ᶠ (x : R) in Filter.atTop, p x) → ∀ᶠ (n : ℚ) in Filter.atTop, p ↑n
-- Mathlib.CategoryTheory.MorphismProperty.Descent
CategoryTheory.MorphismProperty.faithful_overPullback_of_isomorphisms_descendAlong : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.MorphismProperty C}
  [(CategoryTheory.MorphismProperty.isomorphisms C).DescendsAlong P] [P.IsStableUnderBaseChange]
  [inst_3 : CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.Limits.HasEqualizers C] {S T : C} {f : T ⟶ S},
  P f → (CategoryTheory.Over.pullback f).Faithful
-- Mathlib.RingTheory.UniqueFactorizationDomain.Defs
/-- Well-foundedness of the strict version of ∣, which is equivalent to the descending chain
condition on divisibility and to the ascending chain condition on
principal ideals in an integral domain.
 -/
WfDvdMonoid : (α : Type u_2) → [CommMonoidWithZero α] → Prop
-- Mathlib.RingTheory.Nullstellensatz
/-- Main statement of the Nullstellensatz  -/
MvPolynomial.vanishingIdeal_zeroLocus_eq_radical : ∀ {k : Type u_1} {K : Type u_2} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] {σ : Type u_3}
  [IsAlgClosed K] [Finite σ] (I : Ideal (MvPolynomial σ k)),
  MvPolynomial.vanishingIdeal k (MvPolynomial.zeroLocus K I) = I.radical
-- Std.Async.Basic
Std.Async.EAsync.forIn : {ε β : Type} →
  β →
    (Unit → β → Std.Async.EAsync ε (ForInStep β)) → optParam Task.Priority Task.Priority.default → Std.Async.EAsync ε β
-- Lean.EnvExtension
Lean.SimplePersistentEnvExtensionDescr.mk.inj : ∀ {α σ : Type} {name : autoParam Lean.Name Lean.SimplePersistentEnvExtensionDescr.name._autoParam}
  {addEntryFn : σ → α → σ} {addImportedFn : Array (Array α) → σ} {toArrayFn : List α → Array α}
  {exportEntriesFnEx? : Option (Lean.Environment → σ → List α → Lean.OLeanEntries (Array α))}
  {asyncMode : Lean.EnvExtension.AsyncMode} {replay? : Option (List α → σ → σ → List α × σ)}
  {name_1 : autoParam Lean.Name Lean.SimplePersistentEnvExtensionDescr.name._autoParam} {addEntryFn_1 : σ → α → σ}
  {addImportedFn_1 : Array (Array α) → σ} {toArrayFn_1 : List α → Array α}
  {exportEntriesFnEx?_1 : Option (Lean.Environment → σ → List α → Lean.OLeanEntries (Array α))}
  {asyncMode_1 : Lean.EnvExtension.AsyncMode} {replay?_1 : Option (List α → σ → σ → List α × σ)},
  { name := name, addEntryFn := addEntryFn, addImportedFn := addImportedFn, toArrayFn := toArrayFn,
        exportEntriesFnEx? := exportEntriesFnEx?, asyncMode := asyncMode, replay? := replay? } =
      { name := name_1, addEntryFn := addEntryFn_1, addImportedFn := addImportedFn_1, toArrayFn := toArrayFn_1,
        exportEntriesFnEx? := exportEntriesFnEx?_1, asyncMode := asyncMode_1, replay? := replay?_1 } →
    name = name_1 ∧
      addEntryFn = addEntryFn_1 ∧
        addImportedFn = addImportedFn_1 ∧
          toArrayFn = toArrayFn_1 ∧
            exportEntriesFnEx? = exportEntriesFnEx?_1 ∧ asyncMode = asyncMode_1 ∧ replay? = replay?_1
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.basis_one : ∀ (L : PeriodPair), L.basis 1 = L.ω₂
-- Mathlib.AlgebraicGeometry.Sites.Pretopology
AlgebraicGeometry.Scheme.pretopology_monotone : ∀ {P Q : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [inst : P.IsMultiplicative]
  [inst_1 : P.IsStableUnderBaseChange] [inst_2 : Q.IsMultiplicative] [inst_3 : Q.IsStableUnderBaseChange],
  P ≤ Q → AlgebraicGeometry.Scheme.pretopology P ≤ AlgebraicGeometry.Scheme.pretopology Q
-- Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Module.rank_le_one_iff_top_isPrincipal : ∀ {K : Type u} {V : Type v} [inst : Ring K] [StrongRankCondition K] [inst_2 : AddCommGroup V] [inst_3 : Module K V]
  [Module.Free K V], Module.rank K V ≤ 1 ↔ ⊤.IsPrincipal
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.homIso.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cocone F} (h : CategoryTheory.Limits.IsColimit t) (W : C),
  h.homIso W = (Equiv.ulift.trans h.homEquiv).toIso