mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.DedekindDomain.Different
FractionalIdeal.dual.eq_1 : ∀ (A : Type u_1) (K : Type u_2) {L : Type u} {B : Type u_3} [inst : CommRing A] [inst_1 : Field K] [inst_2 : CommRing B]
  [inst_3 : Field L] [inst_4 : Algebra A K] [inst_5 : Algebra B L] [inst_6 : Algebra A B] [inst_7 : Algebra K L]
  [inst_8 : Algebra A L] [inst_9 : IsScalarTower A K L] [inst_10 : IsScalarTower A B L] [inst_11 : IsFractionRing A K]
  [inst_12 : IsIntegrallyClosed A] [inst_13 : FiniteDimensional K L] [inst_14 : IsIntegralClosure B A L]
  [inst_15 : Algebra.IsSeparable K L] [inst_16 : IsDomain A] [inst_17 : IsFractionRing B L] [inst_18 : Nontrivial B]
  [inst_19 : NoZeroDivisors B] (I : FractionalIdeal (nonZeroDivisors B) L),
  FractionalIdeal.dual A K I = if hI : I = 0 then 0 else ⟨Submodule.traceDual A K ↑I, ⋯⟩
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.mk.inj : ∀ {α : Type u_6} {inst : NonUnitalNonAssocSemiring α} {toAddMonoidHom : α →+ α}
  {map_mul_left' : ∀ (a b : α), (↑toAddMonoidHom).toFun (a * b) = a * (↑toAddMonoidHom).toFun b}
  {map_mul_right' : ∀ (a b : α), (↑toAddMonoidHom).toFun (a * b) = (↑toAddMonoidHom).toFun a * b}
  {toAddMonoidHom_1 : α →+ α}
  {map_mul_left'_1 : ∀ (a b : α), (↑toAddMonoidHom_1).toFun (a * b) = a * (↑toAddMonoidHom_1).toFun b}
  {map_mul_right'_1 : ∀ (a b : α), (↑toAddMonoidHom_1).toFun (a * b) = (↑toAddMonoidHom_1).toFun a * b},
  { toAddMonoidHom := toAddMonoidHom, map_mul_left' := map_mul_left', map_mul_right' := map_mul_right' } =
      { toAddMonoidHom := toAddMonoidHom_1, map_mul_left' := map_mul_left'_1, map_mul_right' := map_mul_right'_1 } →
    toAddMonoidHom = toAddMonoidHom_1
-- Mathlib.Topology.Bornology.Absorbs
Set.Finite.absorbs_sInter : ∀ {G₀ : Type u_1} {α : Type u_2} [inst : GroupWithZero G₀] [inst_1 : Bornology G₀] [inst_2 : MulAction G₀ α] {t : Set α}
  {S : Set (Set α)}, S.Finite → (Absorbs G₀ (⋂₀ S) t ↔ ∀ s ∈ S, Absorbs G₀ s t)
-- Mathlib.CategoryTheory.MorphismProperty.WeakFactorizationSystem
CategoryTheory.MorphismProperty.IsWeakFactorizationSystem.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W₁ W₂ : CategoryTheory.MorphismProperty C},
  W₁.rlp = W₂ →
    W₂.llp = W₁ →
      autoParam (W₁.HasFactorization W₂)
          CategoryTheory.MorphismProperty.IsWeakFactorizationSystem.hasFactorization._autoParam →
        W₁.IsWeakFactorizationSystem W₂
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.coe_mul : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Mul β]
  [inst_3 : ContinuousMul β] (f g : C(α, β)), ⇑(f * g) = ⇑f * ⇑g
-- Init.Data.List.Basic
/-- Returns a list of the numbers from `0` to `n` exclusive, in increasing order.

`O(n)`.

Examples:
* `range 5 = [0, 1, 2, 3, 4]`
* `range 0 = []`
* `range 2 = [0, 1]`
 -/
List.range : ℕ → List ℕ
-- Mathlib.Algebra.Algebra.Basic
instFaithfulSMulNatOfCharZero : ∀ (R : Type u_1) [inst : CommSemiring R] [CharZero R], FaithfulSMul ℕ R
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHintClientCapabilities.resolveSupport? : Lean.Lsp.InlayHintClientCapabilities → Option Lean.Lsp.ResolveSupport
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.endsWith_dropEndWhile : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [String.Slice.Pattern.Model.StrictPatternModel pat] [inst_2 : String.Slice.Pattern.BackwardPattern pat]
  [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat] {s : String}, (s.dropEndWhile pat).endsWith pat = false
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
/-- If `F : J ⥤ K ⥤ C` is a functor into a functor category which has a limit,
then the evaluation of that limit at `k` is the limit of the evaluations of `F.obj j` at `k`.
 -/
CategoryTheory.Limits.limitObjIsoLimitCompEvaluation : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type u₁} →
      [inst_1 : CategoryTheory.Category.{v₁, u₁} J] →
        {K : Type u₂} →
          [inst_2 : CategoryTheory.Category.{v₂, u₂} K] →
            [inst_3 : CategoryTheory.Limits.HasLimitsOfShape J C] →
              (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) →
                (k : K) →
                  (CategoryTheory.Limits.limit F).obj k ≅
                    CategoryTheory.Limits.limit (F.comp ((CategoryTheory.evaluation K C).obj k))
-- Init.Data.String.ToSlice
/-- Typeclass for types that have a conversion function to `String.Slice`. This typeclass is used to
make some `String`/`String.Slice` functions polymorphic. As such, for now it is not intended that
there instances of this beyond `ToSlice String` and `ToSlice String.Slice`.

To convert arbitrary data into a string representation, see `ToString` and `Repr`.
 -/
String.ToSlice : Type u → Type u
-- Mathlib.Order.LiminfLimsup
Filter.inf_limsup : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteDistribLattice α] {f : Filter β} {u : β → α} (a : α),
  a ⊓ Filter.limsup u f = Filter.limsup (fun x => a ⊓ u x) f
-- Mathlib.Algebra.Group.Basic
one_add_zsmul : ∀ {G : Type u_3} [inst : AddGroup G] (a : G) (n : ℤ), (1 + n) • a = a + n • a
-- Mathlib.Analysis.SpecialFunctions.Log.Deriv
/-- For `0 ≤ x < 1`, the partial sums of the series expansion of $\frac{1}{2} * \log(\frac{1+x}{1-x})$
at `0` form a lower bound for it. This shows that the absolute value in `sum_range_sub_log_div_le`
can be dropped, and gives explicit lower bounds for logarithms.
 -/
Real.sum_range_le_log_div : ∀ {x : ℝ},
  0 ≤ x → x < 1 → ∀ (n : ℕ), ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (2 * ↑i + 1) ≤ 1 / 2 * Real.log ((1 + x) / (1 - x))
-- Mathlib.Algebra.Order.Interval.Basic
Interval.commMonoid.eq_1 : ∀ {α : Type u_2} [inst : CommMonoid α] [inst_1 : Preorder α] [inst_2 : IsOrderedMonoid α],
  Interval.commMonoid =
    { toMul := Interval.mulOneClass.toMul, mul_assoc := ⋯, toOne := Interval.mulOneClass.toOne, one_mul := ⋯,
      mul_one := ⋯, npow := npowRecAuto, npow_zero := ⋯, npow_succ := ⋯, mul_comm := ⋯ }
-- Mathlib.Topology.Homotopy.HomotopyGroup
/-- Composition with `Cube.insertAt` as a continuous map.  -/
GenLoop.cCompInsert : {N : Type u_1} →
  {X : Type u_2} →
    [inst : TopologicalSpace X] →
      [DecidableEq N] → (i : N) → C(C(N → ↑unitInterval, X), C(↑unitInterval × ({ j // j ≠ i } → ↑unitInterval), X))
-- Mathlib.CategoryTheory.Sites.Sheaf
CategoryTheory.Sheaf.Hom.epi_of_presheaf_epi : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u₂)
  [inst_1 : CategoryTheory.Category.{v₂, u₂} A] {F G : CategoryTheory.Sheaf J A} (f : F ⟶ G)
  [h : CategoryTheory.Epi f.hom], CategoryTheory.Epi f
-- Mathlib.Data.List.Sort
List.insertionSort_cons_of_forall_rel : ∀ {α : Type u_1} (r : α → α → Prop) [inst : DecidableRel r] {a : α} {l : List α},
  (∀ b ∈ l, r a b) → List.insertionSort r (a :: l) = a :: List.insertionSort r l
-- Init.Data.List.OfFn
_private.Init.Data.List.OfFn.0.List.ofFnM.eq_1 : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} {n : ℕ} [inst : Monad m] (f : Fin n → m α),
  List.ofFnM f = List.reverse <$> Fin.foldlM n (fun xs i => (fun x => x :: xs) <$> f i) []
-- Mathlib.Topology.Algebra.Module.UniformConvergence
/-- Let `E` be a TVS, `𝔖 : Set (Set α)` and `H` a submodule of `α →ᵤ[𝔖] E`. If the image of any
`S ∈ 𝔖` by any `u ∈ H` is bounded (in the sense of `Bornology.IsVonNBounded`), then `H`,
equipped with the topology of `𝔖`-convergence, is a TVS.

For convenience, we don't literally ask for `H : Submodule (α →ᵤ[𝔖] E)`. Instead, we prove the
result for any vector space `H` equipped with a linear inducing to `α →ᵤ[𝔖] E`, which is often
easier to use. We also state the `Submodule` version as
`UniformOnFun.continuousSMul_submodule_of_image_bounded`.  -/
UniformOnFun.continuousSMul_induced_of_image_bounded : ∀ (𝕜 : Type u_1) (α : Type u_2) (E : Type u_3) (H : Type u_4) {hom : Type u_5} [inst : NormedField 𝕜]
  [inst_1 : AddCommGroup H] [inst_2 : Module 𝕜 H] [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E]
  [inst_5 : TopologicalSpace H] [inst_6 : UniformSpace E] [IsUniformAddGroup E] [ContinuousSMul 𝕜 E] {𝔖 : Set (Set α)}
  [inst_9 : FunLike hom H (α → E)] [LinearMapClass hom 𝕜 H (α → E)] (φ : hom),
  Topology.IsInducing (⇑(UniformOnFun.ofFun 𝔖) ∘ ⇑φ) →
    (∀ (u : H), ∀ s ∈ 𝔖, Bornology.IsVonNBounded 𝕜 (φ u '' s)) → ContinuousSMul 𝕜 H
-- Mathlib.Logic.Embedding.Set
Function.Embedding.sumSet_preimage_inr : ∀ {α : Type u_1} {s t r : Set α} (h : Disjoint s t),
  Subtype.val '' Sum.inr ⁻¹' ⇑(Function.Embedding.sumSet h) ⁻¹' r = r ∩ t
-- Mathlib.Algebra.Algebra.Hom
AlgHom.funLike : {R : Type u} →
  {A : Type v} →
    {B : Type w} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Semiring B] → [inst_3 : Algebra R A] → [inst_4 : Algebra R B] → FunLike (A →ₐ[R] B) A B
-- Mathlib.LinearAlgebra.Eigenspace.Matrix
Matrix.maxGenEigenspace_toLin'_diagonal_eq_eigenspace : ∀ {R : Type u_1} {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing R] (d : n → R) {μ : R}
  [IsDomain R],
  Module.End.maxGenEigenspace (Matrix.toLin' (Matrix.diagonal d)) μ =
    Module.End.eigenspace (Matrix.toLin' (Matrix.diagonal d)) μ
-- Mathlib.Order.UpperLower.Prod
LowerSet.sup_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (s₁ s₂ : LowerSet α) (t : LowerSet β),
  (s₁ ⊔ s₂) ×ˢ t = s₁ ×ˢ t ⊔ s₂ ×ˢ t
-- Mathlib.GroupTheory.DoubleCoset
DoubleCoset.rel_bot_eq_right_group_rel : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), ⇑(DoubleCoset.setoid ↑H ↑⊥) = ⇑(QuotientGroup.rightRel H)
-- Std.Sat.AIG.Basic
Std.Sat.AIG.Ref.gate : {α : Type} → [inst : Hashable α] → [inst_1 : DecidableEq α] → {aig : Std.Sat.AIG α} → aig.Ref → ℕ
-- Mathlib.Order.Restriction
Preorder.restrictLe_apply : ∀ {α : Type u_1} [inst : Preorder α] {π : α → Type u_2} (a : α) (f : (a : α) → π a) (i : ↑(Set.Iic a)),
  Preorder.restrictLe a f i = f ↑i
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.grothendieckTypeToCat_functor_obj_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C (Type w))
  (X : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)),
  ((CategoryTheory.Grothendieck.grothendieckTypeToCat G).functor.obj X).snd = X.fiber.as
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
Collinear.eq_1 : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (s : Set P), Collinear k s = (Module.rank k ↥(vectorSpan k s) ≤ 1)
-- Mathlib.Analysis.Convex.Contractible
RealTopologicalVectorSpace.contractibleSpace : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [ContinuousAdd E]
  [ContinuousSMul ℝ E], ContractibleSpace E
-- Mathlib.CategoryTheory.Subobject.FactorThru
CategoryTheory.Subobject.factorThru_eq_zero : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} {P : CategoryTheory.Subobject Y} {f : X ⟶ Y} {h : P.Factors f}, P.factorThru f h = 0 ↔ f = 0
-- Mathlib.GroupTheory.PGroup
IsPGroup.to_inf_left : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] {H K : Subgroup G}, IsPGroup p ↥H → IsPGroup p ↥(H ⊓ K)
-- Mathlib.Order.Interval.Finset.Basic
Set.infinite_iff_exists_lt : ∀ {α : Type u_2} [inst : LinearOrder α] [LocallyFiniteOrderTop α] {s : Set α} [Nonempty α],
  s.Infinite ↔ ∀ (a : α), ∃ b ∈ s, b < a
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Ring
/-- The yoneda embedding of `CommRingObjCat C` into presheaves of commutative rings.  -/
CategoryTheory.yonedaCommRing : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        CategoryTheory.Functor (CategoryTheory.CommRingObjCat C) (CategoryTheory.Functor Cᵒᵖ CommRingCat)
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.w₁₃_τ₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C), CategoryTheory.CategoryStruct.comp S.v₁₂.τ₂ S.v₂₃.τ₂ = 0
-- Lean.Meta.Sym.Arith.Poly
Lean.Grind.CommRing.Mon.toExpr : Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Expr
-- Mathlib.FieldTheory.Extension
/-- The lifted RingHom, expressed as an AlgHom.  -/
IntermediateField.Lifts.emb : {F : Type u_1} →
  {E : Type u_2} →
    {K : Type u_3} →
      [inst : Field F] →
        [inst_1 : Field E] →
          [inst_2 : Field K] →
            [inst_3 : Algebra F E] →
              [inst_4 : Algebra F K] → (self : IntermediateField.Lifts F E K) → ↥self.carrier →ₐ[F] K
-- Mathlib.Algebra.GradedMonoid
GradedMonoid.instSMulCommClass : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} {A : ι → Type u_2} [inst : (i : ι) → SMul α (A i)]
  [inst_1 : (i : ι) → SMul β (A i)] [∀ (i : ι), SMulCommClass α β (A i)], SMulCommClass α β (GradedMonoid A)
-- Mathlib.Data.Set.Lattice
Set.iUnion_eq_range_sigma : ∀ {α : Type u_1} {β : Type u_2} (s : α → Set β), ⋃ i, s i = Set.range fun a => ↑a.snd
-- Batteries.Data.Vector.Lemmas
Vector.isSome_finIdxOf? : ∀ {α : Type u_1} {n : ℕ} [inst : BEq α] [PartialEquivBEq α] {v : Vector α n} {a : α},
  (v.finIdxOf? a).isSome = v.contains a
-- Mathlib.FieldTheory.RatFunc.AsPolynomial
RatFunc.algebraMap_comp_C : ∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K],
  (algebraMap (Polynomial K) (RatFunc K)).comp Polynomial.C = RatFunc.C
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.tan_add_int_mul_pi : ∀ (x : ℝ) (n : ℤ), Real.tan (x + ↑n * Real.pi) = Real.tan x
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
/-- This is slightly different from `Measurable.piecewise`. It can be used to show
`Measurable (ite (x=0) 0 1)` by
`exact Measurable.ite (measurableSet_singleton 0) measurable_const measurable_const`,
but replacing `Measurable.ite` by `Measurable.piecewise` in that example proof does not work.  -/
Measurable.ite : ∀ {α : Type u_1} {β : Type u_2} {f g : α → β} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {p : α → Prop}
  {x : DecidablePred p},
  MeasurableSet {a | p a} → Measurable f → Measurable g → Measurable fun x_1 => if p x_1 then f x_1 else g x_1
-- Mathlib.Analysis.Normed.Module.Alternating.Curry
ContinuousAlternatingMap.norm_curryLeft : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : ℕ}
  (f : E [⋀^Fin (n + 1)]→L[𝕜] F), ‖f.curryLeft‖ = ‖f‖
-- Init.Data.BitVec.Lemmas
BitVec.zero_udiv : ∀ {w : ℕ} {x : BitVec w}, 0#w / x = 0#w
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.homMk_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M₁ M₂ : PresheafOfModules R} (φ : M₁.presheaf ⟶ M₂.presheaf)
  (hφ :
    ∀ (X : Cᵒᵖ) (r : ↑(R.obj X)) (m : ↑(M₁.obj X)),
      (CategoryTheory.ConcreteCategory.hom (φ.app X)) (r • m) = r • (CategoryTheory.ConcreteCategory.hom (φ.app X)) m)
  (X : Cᵒᵖ),
  (PresheafOfModules.homMk φ hφ).app X =
    ModuleCat.ofHom { toFun := ⇑(CategoryTheory.ConcreteCategory.hom (φ.app X)), map_add' := ⋯, map_smul' := ⋯ }
-- Mathlib.CategoryTheory.Adjunction.Basic
/-- The notation `F ⊣ G` stands for `Adjunction F G` representing that `F` is left adjoint to `G`  -/
CategoryTheory.«term_⊣_» : Lean.TrailingParserDescr
-- Mathlib.Topology.Compactness.Bases
eq_sUnion_finset_of_isTopologicalBasis_of_isCompact_open : ∀ {X : Type u_1} [inst : TopologicalSpace X] (b : Set (Set X)),
  TopologicalSpace.IsTopologicalBasis b → ∀ (U : Set X), IsCompact U → IsOpen U → ∃ s, U = ⋃₀ (Subtype.val '' ↑s)
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.CWComplex.skeletonLT_zero_eq_empty : ∀ {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [inst : T2Space X] [inst_1 : Topology.CWComplex C],
  ↑(Topology.RelCWComplex.skeletonLT C 0) = ∅
-- Mathlib.Data.EReal.Operations
EReal.neg_lt_zero : ∀ {a : EReal}, -a < 0 ↔ 0 < a
-- Mathlib.RingTheory.Fintype
card_units_lt : ∀ (M₀ : Type u_1) [inst : MonoidWithZero M₀] [Nontrivial M₀] [inst_2 : Fintype M₀], Fintype.card M₀ˣ < Fintype.card M₀
-- Mathlib.Order.Notation
/-- Set / lattice complement  -/
Compl : Type u_1 → Type u_1
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.imp_keq : ∀ {α : Type u_1} [inst : Lean.Grind.CommRing α] (ctx : Lean.Grind.CommRing.Context α) [Lean.Grind.NoNatZeroDivisors α]
  (k : ℤ) (lhs rhs : Lean.Grind.CommRing.Expr) (p₁ p₂ : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Stepwise.imp_keq_cert lhs rhs k p₁ p₂ = true →
    ↑k * Lean.Grind.CommRing.Poly.denote ctx p₁ = Lean.Grind.CommRing.Poly.denote ctx p₂ →
      Lean.Grind.CommRing.Expr.denote ctx lhs = Lean.Grind.CommRing.Expr.denote ctx rhs
-- Mathlib.RingTheory.PowerSeries.WellKnown
PowerSeries.one_sub_pow_mul_invOneSubPow_val_add_eq_invOneSubPow_val : ∀ (S : Type u_1) [inst : CommRing S] (d e : ℕ),
  (1 - PowerSeries.X) ^ e * ↑(PowerSeries.invOneSubPow S (d + e)) = ↑(PowerSeries.invOneSubPow S d)
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Implementation
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.numClausesInFormula : {n : ℕ} → Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n → ℕ
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.coe_one : ∀ {α : Type u_1} {l : Filter α} {M : Type u_5} [inst : One M], ↑1 = 1
-- Mathlib.GroupTheory.Perm.Fin
Equiv.Perm.decomposeFin_symm_of_one : ∀ {n : ℕ} (p : Fin (n + 1)), Equiv.Perm.decomposeFin.symm (p, 1) = Equiv.swap 0 p
-- Mathlib.AlgebraicTopology.CechNerve
CategoryTheory.SimplicialObject.cechNerve_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 :
    ∀ (n : ℕ) (f : CategoryTheory.Arrow C),
      CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom]
  {X Y : CategoryTheory.Arrow C} (F : X ⟶ Y),
  CategoryTheory.SimplicialObject.cechNerve.map F = CategoryTheory.Arrow.mapCechNerve F
-- Mathlib.Combinatorics.SetFamily.FourFunctions
/-- An inequality of Daykin. Interestingly, any lattice in which this inequality holds is
distributive.  -/
Finset.le_card_infs_mul_card_sups : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : DecidableEq α] (s t : Finset α),
  s.card * t.card ≤ (s ⊼ t).card * (s ⊻ t).card
-- Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes
Mathlib.Tactic.Monoidal.instContextContext : Mathlib.Tactic.BicategoryLike.Context Mathlib.Tactic.Monoidal.Context
-- Mathlib.Order.Cover
wcovBy_eq_reflGen_covBy : ∀ {α : Type u_1} [inst : PartialOrder α], (fun x1 x2 => x1 ⩿ x2) = Relation.ReflGen fun x1 x2 => x1 ⋖ x2
-- Mathlib.Order.CompletePartialOrder
Directed.iSup_le : ∀ {ι : Sort u_1} {α : Type u_2} [inst : CompletePartialOrder α] {f : ι → α} {a : α},
  Directed (fun x1 x2 => x1 ≤ x2) f → (∀ (i : ι), f i ≤ a) → ⨆ i, f i ≤ a
-- Mathlib.Data.Set.Function
Set.injOn_empty : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), Set.InjOn f ∅
-- Mathlib.NumberTheory.SumPrimeReciprocals
/-- `Multipliable` over `Nat.Primes` iff over `ℕ` extending `f` by `1`.  -/
Nat.Primes.multipliable_iff_multipliable_ite : ∀ {M : Type u_1} [inst : CommMonoid M] [inst_1 : TopologicalSpace M] (f : ℕ → M),
  (Multipliable fun p => f ↑p) ↔ Multipliable fun n => if Nat.Prime n then f n else 1
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingHom.id_comp : ∀ {α : Type u_2} {β : Type u_3} [inst : NonAssocSemiring α] [inst_1 : Preorder α] [inst_2 : NonAssocSemiring β]
  [inst_3 : Preorder β] (f : α →+*o β), (OrderRingHom.id β).comp f = f
-- Init.Data.List.BasicAux
List.get.eq_2 : ∀ {α : Type u} (head : α) (as : List α) (i : ℕ) (h : i.succ < (head :: as).length),
  (head :: as).get ⟨i.succ, h⟩ = as.get ⟨i, ⋯⟩
-- Lean.Parser.Basic
/-- Consume whitespace and comments  -/
Lean.Parser.whitespace : Lean.Parser.ParserFn
-- Lean.Parser.Module.Syntax
Lean.Parser.Module.all.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.HasSeparator.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C],
  (∃ G, CategoryTheory.IsSeparator G) → CategoryTheory.HasSeparator C
-- Mathlib.Data.Set.Semiring
Set.up_image : ∀ {α : Type u_1} {β : Type u_2} [inst : MulOneClass α] [inst_1 : MulOneClass β] (f : α →* β) (s : Set α),
  Set.up (⇑f '' s) = (SetSemiring.imageHom f) (Set.up s)
-- Mathlib.SetTheory.Ordinal.FixedPointApproximants
/-- The approximation at the index of the successor of the domain's cardinality is a fixed point  -/
OrdinalApprox.lfpApprox_ord_mem_fixedPoint : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) {x : α},
  x ≤ f x → OrdinalApprox.lfpApprox f x (Order.succ (Cardinal.mk α)).ord ∈ Function.fixedPoints ⇑f
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.homothety_injective : ∀ {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [inst : CommRing k] [inst_1 : AddCommGroup V1]
  [inst_2 : AddTorsor V1 P1] [inst_3 : Module k V1] [Module.IsTorsionFree k V1] [IsCancelMulZero k] (c : P1) {r : k},
  r ≠ 0 → Function.Injective ⇑(AffineMap.homothety c r)
-- Mathlib.Algebra.Polynomial.Homogenize
Polynomial.homogenize_map : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] (f : R →+* S) (p : Polynomial R)
  (n : ℕ), (Polynomial.map f p).homogenize n = (MvPolynomial.map f) (p.homogenize n)
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
antitone_mul_right : ∀ {R : Type u} [inst : Semiring R] [inst_1 : Preorder R] [ExistsAddOfLE R] [MulPosMono R] [AddRightMono R]
  [AddRightReflectLE R] {a : R}, a ≤ 0 → Antitone fun x => x * a
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- **Alias** of `Topology.RelCWComplex.pairwiseDisjoint`. -/
Topology.CWComplex.pairwiseDisjoint : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D],
  Set.univ.PairwiseDisjoint fun ni => Topology.RelCWComplex.openCell ni.fst ni.snd
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.ball_subset_ball' : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x y : α} {ε₁ ε₂ : ℝ},
  ε₁ + dist x y ≤ ε₂ → Metric.ball x ε₁ ⊆ Metric.ball y ε₂
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.ι_colimitOfIsReflexivePairIsoCoequalizer_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B : C} {f g : A ⟶ B}
  [inst_1 : CategoryTheory.IsReflexivePair f g] [h : CategoryTheory.Limits.HasCoequalizer f g],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.ofIsReflexivePair f g)
        CategoryTheory.Limits.WalkingReflexivePair.zero)
      CategoryTheory.Limits.colimitOfIsReflexivePairIsoCoequalizer.hom =
    CategoryTheory.Limits.coequalizer.π f g
-- Init.SizeOf
/-- Every type `α` has a low priority default `SizeOf` instance that just returns `0`
for every element of `α`.
 -/
instSizeOfDefault : (α : Sort u) → SizeOf α
-- Mathlib.Order.Category.LinOrd
_private.Mathlib.Order.Category.LinOrd.0.LinOrd.Hom.mk.injEq : ∀ {X Y : LinOrd} (hom' hom'_1 : ↑X →o ↑Y), ({ hom' := hom' } = { hom' := hom'_1 }) = (hom' = hom'_1)
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.toLin'_to_linearMap : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R]
  (A : Matrix.SpecialLinearGroup n R), ↑(Matrix.SpecialLinearGroup.toLin' A) = Matrix.toLin' ↑A
-- Std.Time.Format.Modifier
Std.Time.Modifier.c.injEq : ∀ (presentation presentation_1 : Std.Time.Number ⊕ Std.Time.Text),
  (Std.Time.Modifier.c presentation = Std.Time.Modifier.c presentation_1) = (presentation = presentation_1)
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalSubalgebra.starClosure_le_iff : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : StarModule R A] [inst_6 : IsScalarTower R A A]
  [inst_7 : SMulCommClass R A A] {S₁ : NonUnitalSubalgebra R A} {S₂ : NonUnitalStarSubalgebra R A},
  S₁.starClosure ≤ S₂ ↔ S₁ ≤ S₂.toNonUnitalSubalgebra
-- Mathlib.LinearAlgebra.TensorProduct.Tower
LinearMap.baseChangeHom_apply : ∀ (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] (f : M →ₗ[R] N), (LinearMap.baseChangeHom R A M N) f = LinearMap.baseChange A f