mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjId_inv_app_fst_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (X : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B)
  (X_1 : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) (X_2 : X),
  ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjId X F G).inv.app X_1).fst.app X_2 =
    CategoryTheory.CategoryStruct.id (X_1.fst.obj X_2)
-- Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
CategoryTheory.ObjectProperty.le_strictLimitsClosureIter : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) {α : Type t}
  (J : α → Type u') [inst_1 : (a : α) → CategoryTheory.Category.{v', u'} (J a)] {β : Type w'} [inst_2 : LinearOrder β]
  [OrderBot β] [inst_4 : SuccOrder β] [inst_5 : WellFoundedLT β] (b : β), P ≤ P.strictLimitsClosureIter J b
-- Mathlib.Algebra.Group.Opposite
MulOpposite.commute_unop : ∀ {α : Type u_1} [inst : Mul α] {x y : αᵐᵒᵖ}, Commute (MulOpposite.unop x) (MulOpposite.unop y) ↔ Commute x y
-- Mathlib.CategoryTheory.Limits.Constructions.EpiMono
/-- If `F` reflects pullbacks, then it reflects monomorphisms.  -/
CategoryTheory.reflects_mono_of_reflectsLimit : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y : C} (f : X ⟶ Y)
  [CategoryTheory.Limits.ReflectsLimit (CategoryTheory.Limits.cospan f f) F] [CategoryTheory.Mono (F.map f)],
  CategoryTheory.Mono f
-- Aesop.Forward.State
/-- A monad for operations that add hyps or matches to a cluster state. The
monad's state is an array of complete matches discovered while adding
hyps/matches.  -/
Aesop.ClusterState.AddM : Type → Type
-- Mathlib.Algebra.Group.Submonoid.Defs
Submonoid.instUniqueOfSubsingleton : {M : Type u_1} → [inst : MulOneClass M] → [Subsingleton M] → Unique (Submonoid M)
-- Mathlib.Algebra.Group.InjSurj
/-- A type endowed with `1`, `*`, `⁻¹`, and `/` is a commutative group, if it admits a surjective
map that preserves `1`, `*`, `⁻¹`, and `/` from a commutative group. See note
[reducible non-instances].  -/
Function.Surjective.commGroup : {M₁ : Type u_1} →
  {M₂ : Type u_2} →
    [inst : Mul M₂] →
      [inst_1 : One M₂] →
        [inst_2 : Pow M₂ ℕ] →
          [inst_3 : Inv M₂] →
            [inst_4 : Div M₂] →
              [inst_5 : Pow M₂ ℤ] →
                [inst_6 : CommGroup M₁] →
                  (f : M₁ → M₂) →
                    Function.Surjective f →
                      f 1 = 1 →
                        (∀ (x y : M₁), f (x * y) = f x * f y) →
                          (∀ (x : M₁), f x⁻¹ = (f x)⁻¹) →
                            (∀ (x y : M₁), f (x / y) = f x / f y) →
                              (∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) →
                                (∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n) → CommGroup M₂
-- Mathlib.Order.Filter.Pointwise
Filter.Tendsto.add_add : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddZeroClass α] [inst_1 : AddZeroClass β]
  [inst_2 : FunLike F α β] [AddHomClass F α β] (m : F) {f₁ g₁ : Filter α} {f₂ g₂ : Filter β},
  Filter.Tendsto (⇑m) f₁ f₂ → Filter.Tendsto (⇑m) g₁ g₂ → Filter.Tendsto (⇑m) (f₁ + g₁) (f₂ + g₂)
-- Mathlib.LinearAlgebra.Matrix.Rank
Matrix.lift_cRank_reindex : ∀ {m : Type um} {m₀ : Type um₀} {n₀ : Type un₀} {R : Type uR} {n : Type un} [inst : Semiring R] (A : Matrix m n R)
  (em : m ≃ m₀) (en : n ≃ n₀),
  Cardinal.lift.{um, max uR um₀} ((Matrix.reindex em en) A).cRank = Cardinal.lift.{um₀, max uR um} A.cRank
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- Transport a binary bicone via isomorphisms.  -/
CategoryTheory.Limits.BinaryBicone.ofIso : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {P P' Q Q' : C} →
        CategoryTheory.Limits.BinaryBicone P Q → (P ≅ P') → (Q ≅ Q') → CategoryTheory.Limits.BinaryBicone P' Q'
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.cos_antiperiodic : Function.Antiperiodic Real.Angle.cos ↑Real.pi
-- Mathlib.LinearAlgebra.Basis.Basic
/-- `Basis.singleton ι R` is the basis sending the unique element of `ι` to `1 : R`.  -/
Module.Basis.singleton : (ι : Type u_7) → (R : Type u_8) → [Unique ι] → [inst : Semiring R] → Module.Basis ι R R
-- Mathlib.Algebra.Homology.SpectralSequence.Basic
CategoryTheory.SpectralSequence.mk.inj : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{u_3, u_1} C} {inst_1 : CategoryTheory.Abelian C} {κ : Type u_2}
  {c : ℤ → ComplexShape κ} {r₀ : ℤ}
  {page : (r : ℤ) → autoParam (r₀ ≤ r) CategoryTheory.SpectralSequence._auto_1 → HomologicalComplex C (c r)}
  {iso :
    (r r' : ℤ) →
      (pq : κ) →
        (hrr' : autoParam (r + 1 = r') CategoryTheory.SpectralSequence._auto_3) →
          (hr : autoParam (r₀ ≤ r) CategoryTheory.SpectralSequence._auto_5) → (page r ⋯).homology pq ≅ (page r' ⋯).X pq}
  {page_1 : (r : ℤ) → autoParam (r₀ ≤ r) CategoryTheory.SpectralSequence._auto_1 → HomologicalComplex C (c r)}
  {iso_1 :
    (r r' : ℤ) →
      (pq : κ) →
        (hrr' : autoParam (r + 1 = r') CategoryTheory.SpectralSequence._auto_3) →
          (hr : autoParam (r₀ ≤ r) CategoryTheory.SpectralSequence._auto_5) →
            (page_1 r ⋯).homology pq ≅ (page_1 r' ⋯).X pq},
  { page := page, iso := iso } = { page := page_1, iso := iso_1 } → page = page_1 ∧ iso ≍ iso_1
-- Mathlib.Algebra.Group.Subsemigroup.Defs
/-- An `AddSubsemigroup` of an `AddSemigroup` inherits an `AddSemigroup` structure.  -/
AddMemClass.toAddSemigroup : {M : Type u_4} →
  [inst : AddSemigroup M] → {A : Type u_5} → [inst_1 : SetLike A M] → [AddMemClass A M] → (S : A) → AddSemigroup ↥S
-- Mathlib.Algebra.Group.Units.Basic
AddUnits.neg_add_eq_zero : ∀ {α : Type u} [inst : AddMonoid α] {u : AddUnits α} {a : α}, ↑(-u) + a = 0 ↔ ↑u = a
-- Mathlib.Topology.NhdsWithin
map_nhdsSet_induced_eq : ∀ {α : Type u_5} {β : Type u_6} {t : TopologicalSpace β} {f : α → β} (s : Set α),
  Filter.map f (nhdsSet s) = nhdsSetWithin (f '' s) (Set.range f)
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
CategoryTheory.AB5OfSize.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasFilteredColimitsOfSize.{w, w', v, u} C],
  (∀ (J : Type w') [inst_2 : CategoryTheory.Category.{w, w'} J] [inst_3 : CategoryTheory.IsFiltered J],
      CategoryTheory.HasExactColimitsOfShape J C) →
    CategoryTheory.AB5OfSize.{w, w', v, u} C
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.mk.sizeOf_spec : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : SMul R M] [inst_4 : SizeOf R] [inst_5 : SizeOf M] (carrier : Set M)
  (smul_mem' : ∀ ⦃c : R⦄, 0 < c → ∀ ⦃x : M⦄, x ∈ carrier → c • x ∈ carrier)
  (add_mem' : ∀ ⦃x : M⦄, x ∈ carrier → ∀ ⦃y : M⦄, y ∈ carrier → x + y ∈ carrier),
  sizeOf { carrier := carrier, smul_mem' := smul_mem', add_mem' := add_mem' } = 1
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.instInhabited : {α : Type u_1} → [inst : LE α] → Inhabited (UpperSet α)
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.tensorObj_X : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (A B : CategoryTheory.Comon C),
  (CategoryTheory.MonoidalCategoryStruct.tensorObj A B).X = CategoryTheory.MonoidalCategoryStruct.tensorObj A.X B.X
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.isColimitCoconeUnopOfCone_desc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ) {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsLimit c)
  (s : CategoryTheory.Limits.Cocone F.unop),
  (CategoryTheory.Limits.isColimitCoconeUnopOfCone F hc).desc s =
    (hc.lift (CategoryTheory.Limits.coneOfCoconeUnop s)).unop
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.maxEntry?.eq_3 : ∀ {α : Type u} {β : Type v} (size : ℕ) (k : α) (v : β) (l : Std.DTreeMap.Internal.Impl α fun x => β) (size_1 : ℕ)
  (k_1 : α) (v_1 : β) (l_1 r : Std.DTreeMap.Internal.Impl α fun x => β),
  Std.DTreeMap.Internal.Impl.Const.maxEntry?
      (Std.DTreeMap.Internal.Impl.inner size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)) =
    Std.DTreeMap.Internal.Impl.Const.maxEntry? (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
QuasispectrumRestricts.map_zero : ∀ {R : Type u_3} {S : Type u_4} {A : Type u_5} [inst : Semifield R] [inst_1 : Field S] [inst_2 : NonUnitalRing A]
  [inst_3 : Module R A] [inst_4 : Module S A] [inst_5 : Algebra R S] {a : A} {f : S → R},
  QuasispectrumRestricts a f → f 0 = 0
-- Lean.PrettyPrinter.Delaborator.Options
Lean.getPPUnicodeFun : Lean.Options → Bool
-- Mathlib.CategoryTheory.Discrete.SumsProducts
CategoryTheory.Discrete.sumEquiv_inverse_map : ∀ {J : Type u_1} {K : Type u_2} {X Y : CategoryTheory.Discrete J ⊕ CategoryTheory.Discrete K} (f : X ⟶ Y),
  CategoryTheory.Discrete.sumEquiv.inverse.map f =
    CategoryTheory.Sum.homInduction
      (fun x x_1 f => (CategoryTheory.Discrete.functor fun t => { as := Sum.inl t }).map f)
      (fun x x_1 g => (CategoryTheory.Discrete.functor fun t => { as := Sum.inr t }).map g) f
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
AffineSubspace.ext : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {p q : AffineSubspace k P}, (∀ (x : P), x ∈ p ↔ x ∈ q) → p = q
-- Mathlib.GroupTheory.Subgroup.Centralizer
Subgroup.centralizer_eq_top_iff_subset : ∀ {G : Type u_1} [inst : Group G] {s : Set G}, Subgroup.centralizer s = ⊤ ↔ s ⊆ ↑(Subgroup.center G)
-- Mathlib.Algebra.Group.Subgroup.Basic
MonoidHom.liftOfRightInverse_comp_apply : ∀ {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [inst : Group G₁] [inst_1 : Group G₂] [inst_2 : Group G₃]
  (f : G₁ →* G₂) (f_inv : G₂ → G₁) (hf : Function.RightInverse f_inv ⇑f) (g : { g // f.ker ≤ g.ker }) (x : G₁),
  ((f.liftOfRightInverse f_inv hf) g) (f x) = ↑g x
-- Mathlib.Algebra.Homology.Single
HomologicalComplex.single.congr_simp : ∀ (V : Type u) [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  [inst_2 : CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [inst_3 : DecidableEq ι] (c : ComplexShape ι)
  (j j_1 : ι), j = j_1 → HomologicalComplex.single V c j = HomologicalComplex.single V c j_1
-- Mathlib.Data.Sym.Sym2
Sym2.eq_swap : ∀ {α : Type u_1} {a b : α}, s(a, b) = s(b, a)
-- Mathlib.Logic.Function.Basic
Function.LeftInverse.surjective : ∀ {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α}, Function.LeftInverse f g → Function.Surjective f
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Equiv.diff_congr : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ m₃ m₄ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → m₃.WF → m₄.WF → m₁.Equiv m₃ → m₂.Equiv m₄ → (m₁ \ m₂).Equiv (m₃ \ m₄)
-- Mathlib.LinearAlgebra.Matrix.Hermitian
/-- **Alias** of the forward direction of `Matrix.isHermitian_iff_isSelfAdjoint`. -/
Matrix.IsHermitian.isSelfAdjoint : ∀ {α : Type u_1} {n : Type u_4} [inst : Star α] {A : Matrix n n α}, A.IsHermitian → IsSelfAdjoint A
-- Mathlib.Order.Category.BddOrd
_private.Mathlib.Order.Category.BddOrd.0.BddOrd.Hom.mk : {X Y : BddOrd} → BoundedOrderHom ↑X.toPartOrd ↑Y.toPartOrd → X.Hom Y
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBasis'.insert_not_indep : ∀ {α : Type u_1} {M : Matroid α} {I X : Set α} {e : α}, M.IsBasis' I X → e ∈ X \ I → ¬M.Indep (insert e I)
-- Std.Http.Data.URI.Encoding
Std.Http.URI.instReprEncodedQueryString : {r : UInt8 → Bool} → Repr (Std.Http.URI.EncodedQueryString r)
-- Mathlib.Algebra.Module.SpanRank
Submodule.lift_spanRank_map_eq_of_injective : ∀ {R : Type u_1} {S : Type u_2} {M : Type u} [inst : Semiring R] [inst_1 : Semiring S] {σ : R →+* S}
  [inst_2 : AddCommMonoid M] [inst_3 : Module R M] {L : Type v} [inst_4 : AddCommMonoid L] [inst_5 : Module S L]
  [inst_6 : RingHomSurjective σ] (f : M →ₛₗ[σ] L),
  Function.Injective ⇑f →
    ∀ (p : Submodule R M), Cardinal.lift.{u, v} (Submodule.map f p).spanRank = Cardinal.lift.{v, u} p.spanRank
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.Turing.TM1.stepAux.match_1.splitter : {Γ : Type u_1} →
  {Λ : Type u_2} →
    {σ : Type u_3} →
      [inst : Inhabited Γ] →
        (motive : Turing.TM1.Stmt Γ Λ σ → σ → Turing.Tape Γ → Sort u_4) →
          (x : Turing.TM1.Stmt Γ Λ σ) →
            (x_1 : σ) →
              (x_2 : Turing.Tape Γ) →
                ((d : Turing.Dir) →
                    (q : Turing.TM1.Stmt Γ Λ σ) →
                      (v : σ) → (T : Turing.Tape Γ) → motive (Turing.TM1.Stmt.move d q) v T) →
                  ((a : Γ → σ → Γ) →
                      (q : Turing.TM1.Stmt Γ Λ σ) →
                        (v : σ) → (T : Turing.Tape Γ) → motive (Turing.TM1.Stmt.write a q) v T) →
                    ((s : Γ → σ → σ) →
                        (q : Turing.TM1.Stmt Γ Λ σ) →
                          (v : σ) → (T : Turing.Tape Γ) → motive (Turing.TM1.Stmt.load s q) v T) →
                      ((p : Γ → σ → Bool) →
                          (q₁ q₂ : Turing.TM1.Stmt Γ Λ σ) →
                            (v : σ) → (T : Turing.Tape Γ) → motive (Turing.TM1.Stmt.branch p q₁ q₂) v T) →
                        ((l : Γ → σ → Λ) → (v : σ) → (T : Turing.Tape Γ) → motive (Turing.TM1.Stmt.goto l) v T) →
                          ((v : σ) → (T : Turing.Tape Γ) → motive Turing.TM1.Stmt.halt v T) → motive x x_1 x_2
-- Mathlib.Analysis.Normed.Algebra.Spectrum
_private.Mathlib.Analysis.Normed.Algebra.Spectrum.0.spectrum.termρ_1 : Lean.ParserDescr
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.lift_f_snd_v_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ}
  (α : CochainComplex.HomComplex.Cocycle K F 1) (β : CochainComplex.HomComplex.Cochain K G 0)
  (eq : CochainComplex.HomComplex.δ 0 1 β + (↑α).comp (CochainComplex.HomComplex.Cochain.ofHom φ) ⋯ = 0) (p q : ℤ)
  (hpq : p + 0 = q) {Z : C} (h : G.X q ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.lift φ α β eq).f p)
      (CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.snd φ).v p q hpq) h) =
    CategoryTheory.CategoryStruct.comp (β.v p q hpq) h
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
/-- An infinite cyclic group is isomorphic to `Multiplicative ℤ`.  -/
intCyclicMulEquiv : {G : Type u_2} → [Infinite G] → [inst : Group G] → [IsCyclic G] → Multiplicative ℤ ≃* G
-- Mathlib.Data.PNat.Prime
PNat.dvd_lcm_right : ∀ (n m : ℕ+), m ∣ n.lcm m
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
/-- The additive equivalence `Cochain K L n ≃+ Cochain K L⟦a⟧ n'` when `n' + a = n`.  -/
CochainComplex.HomComplex.Cochain.rightShiftAddEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (K L : CochainComplex C ℤ) →
        (n a n' : ℤ) →
          n' + a = n →
            CochainComplex.HomComplex.Cochain K L n ≃+
              CochainComplex.HomComplex.Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'
-- Mathlib.Algebra.GroupWithZero.Defs
CancelCommMonoidWithZero.mk : {M₀ : Type u_2} → (toCommMonoidWithZero : CommMonoidWithZero M₀) → IsLeftCancelMulZero M₀ → CancelCommMonoidWithZero M₀
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.inv_hom_h₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreOneHypercover S} (e : E ≅ F)
  (i : F.I₀), CategoryTheory.CategoryStruct.comp (e.inv.h₀ i) (e.hom.h₀ (e.inv.s₀ i)) = CategoryTheory.eqToHom ⋯
-- Mathlib.LinearAlgebra.Basis.Defs
/-- `b.reindexRange` is a basis indexed by `range b`, the basis vectors themselves.  -/
Module.Basis.reindexRange : {ι : Type u_10} →
  {R : Type u_11} →
    {M : Type u_12} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] → (b : Module.Basis ι R M) → Module.Basis (↑(Set.range ⇑b)) R M
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapMk_mk : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (f p : Polynomial R),
  (AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapMk I f)
      ((Ideal.Quotient.mk (Ideal.map (AdjoinRoot.mk f) (Ideal.map Polynomial.C I))) ((AdjoinRoot.mk f) p)) =
    (DoubleQuot.quotQuotMk (Ideal.map Polynomial.C I) (Ideal.span {f})) p
-- Lean.DocString.Parser
/-- Parses as `ifVerso` if module docs should use Verso syntax, or as `ifNotVerso` otherwise.
Checks `doc.verso.module` if explicitly set, otherwise falls back to `doc.verso`.
 -/
Lean.Doc.Parser.ifVersoModuleDocs : Lean.Parser.Parser → Lean.Parser.Parser → Lean.Parser.Parser
-- Mathlib.Topology.Bases
TopologicalSpace.IsSeparable.mono : ∀ {α : Type u} [t : TopologicalSpace α] {s u : Set α},
  TopologicalSpace.IsSeparable s → u ⊆ s → TopologicalSpace.IsSeparable u
-- Mathlib.Order.Atoms
SetLike.covBy_iff : ∀ {A : Type u_4} {B : Type u_5} [inst : PartialOrder A] [inst_1 : SetLike A B] [IsConcreteLE A B] {K L : A},
  K ⋖ L ↔ K < L ∧ ∀ (H : A) (g : B), K ≤ H → H ≤ L → g ∉ K → g ∈ H → H = L
-- Mathlib.Algebra.Ring.Divisibility.Lemmas
Commute.add_pow_dvd_pow_of_pow_eq_zero_right : ∀ {R : Type u_1} {x y : R} {n m p : ℕ} [inst : Ring R], n + m ≤ p + 1 → Commute x y → x ^ n = 0 → (x + y) ^ m ∣ y ^ p
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- The cokernel of `biprod.inl : X ⟶ X ⊞ Y` is `Y`.  -/
CategoryTheory.Limits.cokernelBiprodInlIso : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] →
          CategoryTheory.Limits.cokernel CategoryTheory.Limits.biprod.inl ≅ Y
-- Mathlib.Tactic.FunProp.FunctionData
Mathlib.Meta.FunProp.DecompositionResult.comp.sizeOf_spec : ∀ (f g : Lean.Expr), sizeOf (Mathlib.Meta.FunProp.DecompositionResult.comp f g) = 1 + sizeOf f + sizeOf g
-- Lean.Elab.MutualInductive
/-- Runs `k` with the resulting type as the ref or, if that's not available, with the view's ref.  -/
Lean.Elab.Command.InductiveView.withTypeRef : {m : Type → Type} → {α : Type} → [Monad m] → [Lean.MonadRef m] → Lean.Elab.Command.InductiveView → m α → m α
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_one : ∀ (x : NNReal), x ^ 1 = x
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- If `C` has limits of shape `J` and `G` preserves them, then if `G` reflects isomorphisms then it
reflects limits of shape `J`.
 -/
CategoryTheory.Limits.reflectsLimitsOfShape_of_reflectsIsomorphisms : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] {G : CategoryTheory.Functor C D} [G.ReflectsIsomorphisms]
  [CategoryTheory.Limits.HasLimitsOfShape J C] [CategoryTheory.Limits.PreservesLimitsOfShape J G],
  CategoryTheory.Limits.ReflectsLimitsOfShape J G
-- Init.Omega.IntList
/-- The gcd of the absolute values of the entries of an `IntList`.  -/
Lean.Omega.IntList.gcd : Lean.Omega.IntList → ℕ
-- Mathlib.Topology.Sequences
Topology.IsInducing.frechetUrysohnSpace : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [FrechetUrysohnSpace Y]
  {f : X → Y}, Topology.IsInducing f → FrechetUrysohnSpace X
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.pseudofunctor_mapId : ∀ (C : CategoryTheory.Cat),
  CategoryTheory.WithInitial.pseudofunctor.mapId C = CategoryTheory.Cat.Hom.isoMk (CategoryTheory.WithInitial.mapId ↑C)
-- Init.Data.Nat.Coprime
Nat.Coprime.pow_right : ∀ {k m : ℕ} (n : ℕ), k.Coprime m → k.Coprime (m ^ n)
-- Init.Data.String.PosRaw
String.instLERaw : LE String.Pos.Raw
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.IsReal.isUnramified : ∀ (k : Type u_1) [inst : Field k] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra k K]
  {w : NumberField.InfinitePlace K}, w.IsReal → NumberField.InfinitePlace.IsUnramified k w
-- Init.Data.UInt.Bitwise
UInt16.toUInt8_and : ∀ (a b : UInt16), (a &&& b).toUInt8 = a.toUInt8 &&& b.toUInt8
-- Mathlib.CategoryTheory.Localization.HomEquiv
CategoryTheory.LocalizerMorphism.id_homMap : ∀ {C₁ : Type u_2} {D₁ : Type u_5} [inst : CategoryTheory.Category.{v_2, u_2} C₁]
  [inst_1 : CategoryTheory.Category.{v_5, u_5} D₁] {W₁ : CategoryTheory.MorphismProperty C₁}
  (L₁ : CategoryTheory.Functor C₁ D₁) [inst_2 : L₁.IsLocalization W₁] {X Y : C₁} (f : L₁.obj X ⟶ L₁.obj Y),
  (CategoryTheory.LocalizerMorphism.id W₁).homMap L₁ L₁ f = f
-- Mathlib.ModelTheory.Definability
/-- A family of functions is definable when each coordinate is definable.  -/
Set.DefinableMap : {M : Type u_1} →
  (L : FirstOrder.Language) → [L.Structure M] → {α : Type u_2} → {β : Type u_3} → Set M → ((α → M) → β → M) → Prop
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.darts_take : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (n : ℕ), (p.take n).darts = List.take n p.darts
-- Mathlib.Algebra.CharP.Lemmas
add_pow_prime_eq : ∀ {R : Type u_1} [inst : CommSemiring R] {p : ℕ},
  Nat.Prime p →
    ∀ (x y : R),
      (x + y) ^ p = x ^ p + y ^ p + ↑p * x * y * ∑ k ∈ Finset.Ioo 0 p, x ^ (k - 1) * y ^ (p - k - 1) * ↑(p.choose k / p)
-- Mathlib.Geometry.Euclidean.SignedDist
signedDist_anticomm : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (v : V) (p q : P), -((signedDist v) p) q = ((signedDist v) q) p
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
/-- Reinterpret a linear map as an affine map.  -/
LinearMap.toAffineMap : {k : Type u_1} →
  {V₁ : Type u_2} →
    {V₂ : Type u_3} →
      [inst : Ring k] →
        [inst_1 : AddCommGroup V₁] →
          [inst_2 : Module k V₁] → [inst_3 : AddCommGroup V₂] → [inst_4 : Module k V₂] → (V₁ →ₗ[k] V₂) → V₁ →ᵃ[k] V₂
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.mem_alter_of_compare_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k k' : α} {f : Option β → Option β}, cmp k k' = Ordering.eq → (k' ∈ t.alter k f ↔ (f t[k]?).isSome = true)
-- Mathlib.Logic.Function.Basic
Function.Injective.eq_1 : ∀ {α : Sort u_1} {β : Sort u_2} (f : α → β), Function.Injective f = ∀ ⦃a₁ a₂ : α⦄, f a₁ = f a₂ → a₁ = a₂
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
/-- The sets of a filter basis for the neighborhood filter of 0.  -/
SeminormFamily.basisSets : {R : Type u_1} →
  {E : Type u_6} →
    {ι : Type u_9} →
      [inst : SeminormedRing R] → [inst_1 : AddCommGroup E] → [inst_2 : Module R E] → SeminormFamily R E ι → Set (Set E)
-- Mathlib.Topology.MetricSpace.MetricSeparated
/-- **Alias** of the reverse direction of `Metric.AreSeparated.finset_iUnion_right_iff`. -/
Metric.AreSeparated.finset_iUnion_right : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {ι : Type u_3} {I : Finset ι} {s : Set X} {t : ι → Set X},
  (∀ i ∈ I, Metric.AreSeparated s (t i)) → Metric.AreSeparated s (⋃ i ∈ I, t i)
-- Mathlib.Analysis.SpecialFunctions.Stirling
/-- The limit `a` of the sequence `stirlingSeq` satisfies `0 < a`  -/
Stirling.stirlingSeq_has_pos_limit_a : ∃ a, 0 < a ∧ Filter.Tendsto Stirling.stirlingSeq Filter.atTop (nhds a)
-- Lean.Linter.MissingDocs
Lean.Linter.MissingDocs.checkRegisterOption : Lean.Linter.MissingDocs.SimpleHandler