mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.Augmented.w_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.CosimplicialObject.Augmented C}
  {η : X ⟶ Y} {n : SimplexCategory},
  CategoryTheory.CategoryStruct.comp η.left (Y.hom.app n) =
    CategoryTheory.CategoryStruct.comp (X.hom.app n) (η.right.app n)
-- Init.Data.String.Slice
_private.Init.Data.String.Slice.0.String.Slice.RevSplitIterator.toOption.eq_2 : ∀ {ρ : Type} {ρ_1 : ρ} {σ : String.Slice → Type} [inst : String.Slice.Pattern.ToBackwardSearcher ρ_1 σ]
  {s : String.Slice}, String.Slice.RevSplitIterator.toOption✝ String.Slice.RevSplitIterator.atEnd = none
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
CategoryTheory.Subobject.Classifier.hom_comp_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (𝒞₁ 𝒞₂ 𝒞₃ : CategoryTheory.Subobject.Classifier C) {Z : C}
  (h : 𝒞₃.Ω ⟶ Z),
  CategoryTheory.CategoryStruct.comp (𝒞₁.hom 𝒞₂) (CategoryTheory.CategoryStruct.comp (𝒞₂.hom 𝒞₃) h) =
    CategoryTheory.CategoryStruct.comp (𝒞₁.hom 𝒞₃) h
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.add_overlap_pf : ∀ {R : Type u_1} [inst : CommSemiring R] {a b c : R} (x : R) (e : ℕ), a + b = c → x ^ e * a + x ^ e * b = x ^ e * c
-- Std.Tactic.BVDecide.LRAT.Actions
Std.Tactic.BVDecide.LRAT.Action.del.injEq : ∀ {β : Type u} {α : Type v} (ids ids_1 : Array ℕ),
  (Std.Tactic.BVDecide.LRAT.Action.del ids = Std.Tactic.BVDecide.LRAT.Action.del ids_1) = (ids = ids_1)
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.mem_support_swap_mul_imp_mem_support_ne : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {f : Equiv.Perm α} {x y : α},
  y ∈ (Equiv.swap x (f x) * f).support → y ∈ f.support ∧ y ≠ x
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
nnnorm_cfcₙ_nnreal_lt_iff : ∀ {A : Type u_1} [inst : NonUnitalNormedRing A] [inst_1 : StarRing A] [inst_2 : NormedSpace ℝ A]
  [inst_3 : IsScalarTower ℝ A A] [inst_4 : SMulCommClass ℝ A A] [inst_5 : PartialOrder A] [inst_6 : StarOrderedRing A]
  [inst_7 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_8 : NonnegSpectrumClass ℝ A]
  (f : NNReal → NNReal) (a : A) (c : NNReal),
  autoParam (ContinuousOn f (quasispectrum NNReal a)) nnnorm_cfcₙ_nnreal_lt_iff._auto_1 →
    autoParam (f 0 = 0) nnnorm_cfcₙ_nnreal_lt_iff._auto_3 →
      autoParam (0 ≤ a) nnnorm_cfcₙ_nnreal_lt_iff._auto_5 → (‖cfcₙ f a‖₊ < c ↔ ∀ x ∈ quasispectrum NNReal a, f x < c)
-- Mathlib.NumberTheory.LSeries.Nonvanishing
_private.Mathlib.NumberTheory.LSeries.Nonvanishing.0.DirichletCharacter.BadChar.mk : {N : ℕ} →
  [inst : NeZero N] →
    (χ : DirichletCharacter ℂ N) →
      χ ≠ 1 → χ ^ 2 = 1 → DirichletCharacter.LFunction χ 1 = 0 → DirichletCharacter.BadChar✝ N
-- Mathlib.Lean.Meta.RefinedDiscrTree.Initialize
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Initialize.0.Lean.Meta.RefinedDiscrTree.getChildNgen : Lean.CoreM Lean.NameGenerator
-- Mathlib.Topology.UniformSpace.Defs
UniformSpace.isCover_iff_subset_iUnion_ball : ∀ {β : Type ub} {U : SetRel β β} [U.IsSymm] {s N : Set β}, U.IsCover s N ↔ s ⊆ ⋃ y ∈ N, UniformSpace.ball y U
-- Mathlib.MeasureTheory.Group.FundamentalDomain
/-- A measure `μ` on `α ⧸ G` satisfying `QuotientMeasureEqMeasurePreimage` and having finite
covolume is a finite measure.  -/
MeasureTheory.QuotientMeasureEqMeasurePreimage.isFiniteMeasure_quotient : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α]
  {ν : MeasureTheory.Measure α} [MeasureTheory.SMulInvariantMeasure G α ν] [Countable G] [MeasurableConstSMul G α]
  (μ : MeasureTheory.Measure (Quotient (MulAction.orbitRel G α))) [MeasureTheory.QuotientMeasureEqMeasurePreimage ν μ]
  [hasFun : MeasureTheory.HasFundamentalDomain G α ν],
  MeasureTheory.covolume G α ν ≠ ⊤ → MeasureTheory.IsFiniteMeasure μ
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
IsLocalDiffeomorphAt.isInteriorPoint_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {N : Type u_7} [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H' N] {n : WithTop ℕ∞},
  n ≠ 0 → ∀ {f : M → N} {x : M}, IsLocalDiffeomorphAt I I' n f x → (I.IsInteriorPoint x ↔ I'.IsInteriorPoint (f x))
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
IsDedekindDomain.HeightOneSpectrum.comap.congr_simp : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_4} [inst_1 : CommRing S] (f f_1 : R →+* S) (e_f : f = f_1)
  (hf : Function.Surjective ⇑f) (v v_1 : IsDedekindDomain.HeightOneSpectrum S),
  v = v_1 → IsDedekindDomain.HeightOneSpectrum.comap f hf v = IsDedekindDomain.HeightOneSpectrum.comap f_1 ⋯ v_1
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Matrix.isAdjMatrix_compl : ∀ {α : Type u_1} {V : Type u_2} [inst : DecidableEq α] [inst_1 : DecidableEq V] (A : Matrix V V α) [inst_2 : Zero α]
  [inst_3 : One α], A.IsSymm → A.compl.IsAdjMatrix
-- Mathlib.Algebra.Torsor.Basic
Prod.mk_vsub_mk : ∀ {G : Type u_1} {G' : Type u_2} {P : Type u_3} {P' : Type u_4} [inst : AddGroup G] [inst_1 : AddGroup G']
  [inst_2 : AddTorsor G P] [inst_3 : AddTorsor G' P'] (p₁ p₂ : P) (p₁' p₂' : P'),
  (p₁, p₁') -ᵥ (p₂, p₂') = (p₁ -ᵥ p₂, p₁' -ᵥ p₂')
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
AbsoluteValue.mk.inj : ∀ {R : Type u_5} {S : Type u_6} {inst : Semiring R} {inst_1 : Semiring S} {inst_2 : PartialOrder S} {toMulHom : R →ₙ* S}
  {nonneg' : ∀ (x : R), 0 ≤ toMulHom.toFun x} {eq_zero' : ∀ (x : R), toMulHom.toFun x = 0 ↔ x = 0}
  {add_le' : ∀ (x y : R), toMulHom.toFun (x + y) ≤ toMulHom.toFun x + toMulHom.toFun y} {toMulHom_1 : R →ₙ* S}
  {nonneg'_1 : ∀ (x : R), 0 ≤ toMulHom_1.toFun x} {eq_zero'_1 : ∀ (x : R), toMulHom_1.toFun x = 0 ↔ x = 0}
  {add_le'_1 : ∀ (x y : R), toMulHom_1.toFun (x + y) ≤ toMulHom_1.toFun x + toMulHom_1.toFun y},
  { toMulHom := toMulHom, nonneg' := nonneg', eq_zero' := eq_zero', add_le' := add_le' } =
      { toMulHom := toMulHom_1, nonneg' := nonneg'_1, eq_zero' := eq_zero'_1, add_le' := add_le'_1 } →
    toMulHom = toMulHom_1
-- Mathlib.LinearAlgebra.Complex.Module
/-- `ℝ`-algebra morphism version of the canonical embedding of `ℝ` in `ℂ`.  -/
Complex.ofRealAm : ℝ →ₐ[ℝ] ℂ
-- Mathlib.GroupTheory.HNNExtension
/-- The relation we quotient the coproduct by to form an `HNNExtension`.  -/
HNNExtension.con : (G : Type u_1) → [inst : Group G] → (A B : Subgroup G) → ↥A ≃* ↥B → Con (Monoid.Coprod G (Multiplicative ℤ))
-- Init.Data.String.Basic
String.Slice.Pos.nextFast : {s : String.Slice} → (pos : s.Pos) → pos ≠ s.endPos → s.Pos
-- Mathlib.Data.TypeVec
/-- arrow in the category of `0-length` vectors  -/
TypeVec.nilFun : {α : TypeVec.{u_1} 0} → {β : TypeVec.{u_2} 0} → α.Arrow β
-- Mathlib.GroupTheory.GroupAction.ConjAct
ConjAct.normal_of_characteristic_of_normal : ∀ {G : Type u_3} [inst : Group G] {H : Subgroup G} [hH : H.Normal] {K : Subgroup ↥H} [h : K.Characteristic],
  (Subgroup.map H.subtype K).Normal
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
/-- Given `i : Fin (n + 1)`, this is the isomorphism from `Δ[0]` to the face
of `Δ[n]` corresponding to `{i}`.  -/
SSet.stdSimplex.faceSingletonIso : {n : ℕ} → (i : Fin (n + 1)) → SSet.stdSimplex.obj { len := 0 } ≅ (SSet.stdSimplex.face {i}).toSSet
-- Lean.Server.Completion.CompletionCollectors
Lean.Server.Completion.optionCompletion : Lean.Lsp.DocumentUri →
  Lean.Lsp.Position →
    ℕ → Lean.Elab.ContextInfo → Lean.Syntax → Lean.Lsp.ClientCapabilities → IO (Array Lean.Lsp.ResolvableCompletionItem)
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
/-- Promote a `NormedAddGroupHom` to a morphism in `SemiNormedGrp₁`.  -/
SemiNormedGrp₁.mkHom : {M N : Type u} →
  [inst : SeminormedAddCommGroup M] →
    [inst_1 : SeminormedAddCommGroup N] →
      (f : NormedAddGroupHom M N) → f.NormNoninc → ({ carrier := M, str := inst } ⟶ { carrier := N, str := inst_1 })
-- Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Module.rankAtStalk_eq_of_equiv : ∀ {R : Type uR} {M : Type uM} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_1}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (e : M ≃ₗ[R] N), Module.rankAtStalk M = Module.rankAtStalk N
-- Mathlib.Algebra.Order.Archimedean.Class
FiniteMulArchimedeanClass.mk_le_mk : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {a : M} (ha : a ≠ 1) {b : M}
  (hb : b ≠ 1),
  FiniteMulArchimedeanClass.mk a ha ≤ FiniteMulArchimedeanClass.mk b hb ↔
    MulArchimedeanClass.mk a ≤ MulArchimedeanClass.mk b
-- Mathlib.CategoryTheory.FiberedCategory.HomLift
CategoryTheory.IsHomLift.id : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₂} 𝒳] [inst_1 : CategoryTheory.Category.{v₂, u₁} 𝒮]
  {p : CategoryTheory.Functor 𝒳 𝒮} {R : 𝒮} {a : 𝒳},
  p.obj a = R → p.IsHomLift (CategoryTheory.CategoryStruct.id R) (CategoryTheory.CategoryStruct.id a)
-- Mathlib.Data.Finite.Defs
/-- **Alias** of the reverse direction of `Set.not_infinite`. -/
Set.Finite.not_infinite : ∀ {α : Type u} {s : Set α}, s.Finite → ¬s.Infinite
-- Mathlib.Order.SetDissipate
Set.antitone_dissipate : ∀ {α : Type u_1} {β : Type u_2} {s : α → Set β} [inst : Preorder α], Antitone (Set.dissipate s)
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.evalCheckMeta : Lean.Environment → Lean.Name → Except String Unit
-- Mathlib.RingTheory.Perfectoid.BDeRham
_private.Mathlib.RingTheory.Perfectoid.BDeRham.0.«term𝔹_dR(_)» : Lean.ParserDescr
-- Init.Data.UInt.Lemmas
UInt16.toUInt16_toUInt64 : ∀ (n : UInt16), n.toUInt64.toUInt16 = n
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
/-- `Πʳ i, [R i, A i]` is `RestrictedProduct R A cofinite`.  -/
RestrictedProduct.«termΠʳ_,[_,_]» : Lean.ParserDescr
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr.0.Std.Tactic.BVDecide.BVExpr.bitblast.goCache.match_3.eq_1 : ∀ {w : ℕ} (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) (motive : Option (aig.RefVec w) → Sort u_1) (vec : aig.RefVec w)
  (h_1 : (vec : aig.RefVec w) → motive (some vec)) (h_2 : Unit → motive none),
  (match some vec with
    | some vec => h_1 vec
    | none => h_2 ()) =
    h_1 vec
-- Mathlib.GroupTheory.GroupAction.Quotient
AddAction.orbitProdStabilizerEquivAddGroup.eq_1 : ∀ (G : Type u) {X : Type v} [inst : AddGroup G] [inst_1 : AddAction G X] (b : X),
  AddAction.orbitProdStabilizerEquivAddGroup G b =
    ((AddAction.orbitEquivQuotientStabilizer G b).prodCongr (Equiv.refl ↥(AddAction.stabilizer G b))).trans
      AddSubgroup.addGroupEquivQuotientProdAddSubgroup.symm
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.exists_cube_associated : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S : FermatLastTheoremForThreeGen.Solution✝ hζ)
  [inst_1 : NumberField K] [inst_2 : IsCyclotomicExtension {3} ℚ K],
  (∃ X, Associated (X ^ 3) (FermatLastTheoremForThreeGen.Solution.x✝ S)) ∧
    (∃ Y, Associated (Y ^ 3) (FermatLastTheoremForThreeGen.Solution.y✝ S)) ∧
      ∃ Z, Associated (Z ^ 3) (FermatLastTheoremForThreeGen.Solution.z✝ S)
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.isSheaf : ∀ {X : AlgebraicGeometry.Scheme} (M : X.Modules), M.presheaf.IsSheaf
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balanceₘ.match_1.congr_eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (l : Std.DTreeMap.Internal.Impl α β)
  (motive : (r : Std.DTreeMap.Internal.Impl α β) → r.size > Std.DTreeMap.Internal.delta * l.size → Sort u_3)
  (r : Std.DTreeMap.Internal.Impl α β) (h : r.size > Std.DTreeMap.Internal.delta * l.size)
  (h_1 :
    (h : Std.DTreeMap.Internal.Impl.leaf.size > Std.DTreeMap.Internal.delta * l.size) →
      motive Std.DTreeMap.Internal.Impl.leaf h)
  (h_2 :
    (size : ℕ) →
      (rk : α) →
        (rv : β rk) →
          (rl rr : Std.DTreeMap.Internal.Impl α β) →
            (h : (Std.DTreeMap.Internal.Impl.inner size rk rv rl rr).size > Std.DTreeMap.Internal.delta * l.size) →
              motive (Std.DTreeMap.Internal.Impl.inner size rk rv rl rr) h)
  (size : ℕ) (rk : α) (rv : β rk) (rl rr : Std.DTreeMap.Internal.Impl α β)
  (h_3 : (Std.DTreeMap.Internal.Impl.inner size rk rv rl rr).size > Std.DTreeMap.Internal.delta * l.size),
  r = Std.DTreeMap.Internal.Impl.inner size rk rv rl rr →
    h ≍ h_3 →
      (match r, h with
        | Std.DTreeMap.Internal.Impl.leaf, h => h_1 h
        | Std.DTreeMap.Internal.Impl.inner size rk rv rl rr, h => h_2 size rk rv rl rr h) ≍
        h_2 size rk rv rl rr h_3
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.valuesArray_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.valuesArray = t₂.valuesArray
-- Mathlib.Data.Set.Function
Set.injOn_singleton : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (a : α), Set.InjOn f {a}
-- Mathlib.Topology.Category.Stonean.Basic
/-- A morphism in `Stonean` is an epi iff it is surjective.
 -/
Stonean.epi_iff_surjective : ∀ {X Y : Stonean} (f : X ⟶ Y), CategoryTheory.Epi f ↔ Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContinuousLinearMap.bilinearRestrictScalars.congr_simp : ∀ (𝕜 : Type u_1) {E : Type u_4} {F : Type u_6} {G : Type u_8} {𝕜' : Type u_11} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NontriviallyNormedField 𝕜'] [inst_2 : NormedAlgebra 𝕜 𝕜'] [inst_3 : SeminormedAddCommGroup E]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜' E] [inst_6 : IsScalarTower 𝕜 𝕜' E]
  [inst_7 : SeminormedAddCommGroup F] [inst_8 : NormedSpace 𝕜 F] [inst_9 : NormedSpace 𝕜' F]
  [inst_10 : IsScalarTower 𝕜 𝕜' F] [inst_11 : SeminormedAddCommGroup G] [inst_12 : NormedSpace 𝕜 G]
  [inst_13 : NormedSpace 𝕜' G] [inst_14 : IsScalarTower 𝕜 𝕜' G] (B B_1 : E →L[𝕜'] F →L[𝕜'] G),
  B = B_1 → ContinuousLinearMap.bilinearRestrictScalars 𝕜 B = ContinuousLinearMap.bilinearRestrictScalars 𝕜 B_1
-- Lean.Parser.Term
Lean.Parser.Term.dynamicQuot.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
CategoryTheory.GradedObject.BifunctorComp₁₂IndexData.mk.injEq : ∀ {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃ → J} (I₁₂ : Type u_11)
  (p : I₁ × I₂ → I₁₂) (q : I₁₂ × I₃ → J) (hpq : ∀ (i : I₁ × I₂ × I₃), q (p (i.1, i.2.1), i.2.2) = r i)
  (I₁₂_1 : Type u_11) (p_1 : I₁ × I₂ → I₁₂_1) (q_1 : I₁₂_1 × I₃ → J)
  (hpq_1 : ∀ (i : I₁ × I₂ × I₃), q_1 (p_1 (i.1, i.2.1), i.2.2) = r i),
  ({ I₁₂ := I₁₂, p := p, q := q, hpq := hpq } = { I₁₂ := I₁₂_1, p := p_1, q := q_1, hpq := hpq_1 }) =
    (I₁₂ = I₁₂_1 ∧ p ≍ p_1 ∧ q ≍ q_1)
-- Mathlib.Logic.Function.Iterate
Function.Injective.iterate : ∀ {α : Type u} {f : α → α}, Function.Injective f → ∀ (n : ℕ), Function.Injective f^[n]
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.mk_mul_mk : ∀ {M : Type u_1} [inst : CommMonoid M] {x y : M}, Associates.mk x * Associates.mk y = Associates.mk (x * y)
-- Init.Control.State
StateT.tryFinally : {m : Type u → Type v} → {σ : Type u} → [MonadFinally m] → [Monad m] → MonadFinally (StateT σ m)
-- Mathlib.CategoryTheory.MorphismProperty.Representable
/-- Given a representable morphism `f : X ⟶ Y`, then for any `g : F.obj a ⟶ Y`, `hf.snd g`
denotes the morphism in `C` giving rise to the following diagram
```
hf.pullback g --F.map (hf.snd g)--> F.obj a
    |                                 |
   fst                                g
    |                                 |
    v                                 v
    X -------------- f -------------> Y
```  -/
CategoryTheory.Functor.relativelyRepresentable.snd : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {X Y : D} → {f : X ⟶ Y} → (hf : F.relativelyRepresentable f) → {a : C} → (g : F.obj a ⟶ Y) → hf.pullback g ⟶ a
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.le_support_iff_le_vanishingIdeal : ∀ {X : AlgebraicGeometry.Scheme} {I : X.IdealSheafData} {Z : TopologicalSpace.Closeds ↥X},
  Z ≤ I.support ↔ I ≤ AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal Z
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
ProfiniteAddGrp.toFiniteQuotientFunctor.eq_1 : ∀ (P : ProfiniteAddGrp.{u_1}),
  P.toFiniteQuotientFunctor =
    { obj := fun H => FiniteAddGrp.of (↑P.toProfinite.toTop ⧸ ↑H.toOpenAddSubgroup),
      map := fun {X Y} fHK =>
        FiniteAddGrp.ofHom
          (QuotientAddGroup.map (↑X.toOpenAddSubgroup) (↑Y.toOpenAddSubgroup) (AddMonoidHom.id ↑P.toProfinite.toTop) ⋯),
      map_id := ⋯, map_comp := ⋯ }
-- Mathlib.Order.Hom.Lattice
LatticeHom.coe_comp_sup_hom : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : Lattice γ]
  (f : LatticeHom β γ) (g : LatticeHom α β),
  { toFun := ⇑(f.comp g), map_sup' := ⋯ } = { toFun := ⇑f, map_sup' := ⋯ }.comp { toFun := ⇑g, map_sup' := ⋯ }
-- Mathlib.Order.Atoms
/-- **Alias** of the reverse direction of `bot_covBy_iff`. -/
IsAtom.bot_covBy : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : OrderBot α] {a : α}, IsAtom a → ⊥ ⋖ a
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.Functor.Monoidal.μ_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  {E : Type u₃} [inst_4 : CategoryTheory.Category.{v₃, u₃} E] [inst_5 : CategoryTheory.CartesianMonoidalCategory E]
  (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [inst_6 : F.Monoidal] [inst_7 : G.Monoidal]
  [inst_8 : (F.comp G).Monoidal] (X Y : C),
  CategoryTheory.Functor.LaxMonoidal.μ (F.comp G) X Y =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ G (F.obj X) (F.obj Y))
      (G.map (CategoryTheory.Functor.LaxMonoidal.μ F X Y))
-- Mathlib.RingTheory.Polynomial.Basic
Ideal.mem_leadingCoeffNth_zero : ∀ {R : Type u} [inst : CommSemiring R] (I : Ideal (Polynomial R)) (x : R), x ∈ I.leadingCoeffNth 0 ↔ Polynomial.C x ∈ I
-- Std.Http.Data.Body.Full
Std.Http.Body.instCoeFullAny : Coe Std.Http.Body.Full Std.Http.Body.Any
-- Init.Data.List.Sublist
List.IsSuffix.trans : ∀ {α : Type u_1} {l₁ l₂ l₃ : List α}, l₁ <:+ l₂ → l₂ <:+ l₃ → l₁ <:+ l₃
-- Init.Data.Nat.Lemmas
Nat.div_mul_div_le : ∀ (a b c d : ℕ), a / b * (c / d) ≤ a * c / (b * d)
-- Mathlib.Analysis.Normed.Ring.Units
NormedRing.inverse_one_sub_nth_order' : ∀ {R : Type u_1} [inst : NormedRing R] [HasSummableGeomSeries R] (n : ℕ) {t : R},
  ‖t‖ < 1 → Ring.inverse (1 - t) = ∑ i ∈ Finset.range n, t ^ i + t ^ n * Ring.inverse (1 - t)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get?_eq_none : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {a : α}, a ∉ t → t.get? a = none
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.Pre.of.injEq : ∀ {R : Type u_1} {X : Type u_2} (a a_1 : X), (FreeAlgebra.Pre.of a = FreeAlgebra.Pre.of a_1) = (a = a_1)
-- Mathlib.Data.Finset.Defs
/-- `Finset α` is the type of finite sets of elements of `α`. It is implemented
as a multiset (a list up to permutation) which has no duplicate elements.  -/
Finset : Type u_4 → Type u_4
-- Mathlib.Algebra.Group.Invertible.Defs
invOf_mul : ∀ {α : Type u} [inst : Monoid α] (a b : α) [inst_1 : Invertible a] [inst_2 : Invertible b]
  [inst_3 : Invertible (a * b)], ⅟(a * b) = ⅟b * ⅟a
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.SimpTheorems.eraseCore : Lean.Meta.SimpTheorems → Lean.Meta.Origin → Lean.Meta.SimpTheorems
-- Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
/-- When 3 is a unit, `Y² + Y = X³` is an elliptic curve.
It is of j-invariant 0 (see `WeierstrassCurve.ofJ0_j`).  -/
WeierstrassCurve.instIsEllipticOfJ0OfFactIsUnitOfNat : ∀ (R : Type u_1) [inst : CommRing R] [hu : Fact (IsUnit 3)], (WeierstrassCurve.ofJ0 R).IsElliptic
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_castAdd_uIoc_castAdd : ∀ {n : ℕ} (m : ℕ) (i j : Fin n), Fin.castAdd m ⁻¹' Set.uIoc (Fin.castAdd m i) (Fin.castAdd m j) = Set.uIoc i j
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.comapDomainAddMonoidHom_apply : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] (f : M → N) (hf : Function.Injective f)
  (x : AddMonoidAlgebra R N), (AddMonoidAlgebra.comapDomainAddMonoidHom f hf) x = AddMonoidAlgebra.comapDomain f hf x
-- Lean.Language.Basic
/-- Adds unexpected exceptions from header processing to the message log as a last resort; standard
errors should already have been caught earlier.  -/
Lean.Language.withHeaderExceptions : {α : Type} → (Lean.Language.Snapshot → α) → Lean.Language.ProcessingT IO α → Lean.Language.ProcessingM α
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
MeasureTheory.condExpL1.congr_simp : ∀ {α : Type u_1} {F' : Type u_3} [inst : NormedAddCommGroup F'] [inst_1 : NormedSpace ℝ F'] {m m0 : MeasurableSpace α}
  (hm : m ≤ m0) (μ : MeasureTheory.Measure α) [inst_2 : MeasureTheory.SigmaFinite (μ.trim hm)] (f f_1 : α → F'),
  f = f_1 → MeasureTheory.condExpL1 hm μ f = MeasureTheory.condExpL1 hm μ f_1
-- Mathlib.Topology.Sheaves.Skyscraper
StalkSkyscraperPresheafAdjunctionAuxs.toSkyscraperPresheaf_app : ∀ {X : TopCat} (p₀ : ↑X) [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v}
  [inst_1 : CategoryTheory.Category.{u, v} C] [inst_2 : CategoryTheory.Limits.HasTerminal C]
  [inst_3 : CategoryTheory.Limits.HasColimits C] {𝓕 : TopCat.Presheaf C X} {c : C} (f : 𝓕.stalk p₀ ⟶ c)
  (U : (TopologicalSpace.Opens ↑X)ᵒᵖ),
  (StalkSkyscraperPresheafAdjunctionAuxs.toSkyscraperPresheaf p₀ f).app U =
    if h : p₀ ∈ Opposite.unop U then
      CategoryTheory.CategoryStruct.comp (𝓕.germ (Opposite.unop U) p₀ h)
        (CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom ⋯))
    else (⋯ ▸ CategoryTheory.Limits.terminalIsTerminal).from (𝓕.obj U)
-- Mathlib.Algebra.Polynomial.OfFn
Polynomial.ofFn_comp_toFn_eq_id_of_natDegree_lt : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : DecidableEq R] {n : ℕ} {p : Polynomial R},
  p.natDegree < n → (Polynomial.ofFn n) ((Polynomial.toFn n) p) = p
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.setRed.match_1.eq_2 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → Sort u_2)
  (h_1 :
    (c : RBTree.RBColor) →
      (a : RBTree.RBNode α) → (v : α) → (b : RBTree.RBNode α) → motive (RBTree.RBNode.node c a v b))
  (h_2 : Unit → motive RBTree.RBNode.nil),
  (match RBTree.RBNode.nil with
    | RBTree.RBNode.node c a v b => h_1 c a v b
    | RBTree.RBNode.nil => h_2 ()) =
    h_2 ()
-- Mathlib.Data.ENNReal.Basic
ENNReal.instLinearOrderedAddCommMonoidWithTop : LinearOrderedAddCommMonoidWithTop ENNReal
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
SSet.S.IsUniquelyCodimOneFace.cast : ∀ {X : SSet} {x y : X.S} (hxy : x.IsUniquelyCodimOneFace y) {d : ℕ} (hd : x.dim = d),
  (x.cast hd).IsUniquelyCodimOneFace (y.cast ⋯)
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
integral_cos_mul_complex : ∀ {z : ℂ},
  z ≠ 0 → ∀ (a b : ℝ), ∫ (x : ℝ) in a..b, Complex.cos (z * ↑x) = Complex.sin (z * ↑b) / z - Complex.sin (z * ↑a) / z