mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.Birational.Birational
AlgebraicGeometry.Scheme.instIsRationalOverOverAffineSpaceInferInstanceOverClass : ∀ (S : AlgebraicGeometry.Scheme) (n : Type u),
  AlgebraicGeometry.Scheme.IsRationalOver (AlgebraicGeometry.AffineSpace n S ↘ S)
-- Init.Data.SInt.Lemmas
Int16.ofNat_mod : ∀ {a b : ℕ}, a < 2 ^ 15 → b < 2 ^ 15 → Int16.ofNat (a % b) = Int16.ofNat a % Int16.ofNat b
-- Mathlib.Data.Rel.Cover
SetRel.IsCover.union : ∀ {X : Type u_1} {U : SetRel X X} {s t N₁ N₂ : Set X}, U.IsCover s N₁ → U.IsCover t N₂ → U.IsCover (s ∪ t) (N₁ ∪ N₂)
-- Batteries.Classes.Order
Std.instTransCmpFlipOrdering_batteries : ∀ {α : Type u_1} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp], Std.TransCmp (flip cmp)
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
/-- **Alias** of the forward direction of `upperHemicontinuousWithinAt_iff_forall_isOpen`. -/
UpperHemicontinuousWithinAt.forall_isOpen : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f : α → Set β} {s : Set α} {x : α}
  [inst_1 : TopologicalSpace β],
  UpperHemicontinuousWithinAt f s x → ∀ (u : Set β), IsOpen u → f x ⊆ u → ∀ᶠ (x' : α) in nhdsWithin x s, f x' ⊆ u
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.submoduleMap_apply_coe : ∀ {R : Type u_11} {M : Type u_14} {M₁ : Type u_15} [inst : Ring R] [inst_1 : SeminormedAddCommGroup M]
  [inst_2 : SeminormedAddCommGroup M₁] [inst_3 : Module R M] [inst_4 : Module R M₁] (p : Submodule R M)
  (e : M →ₗᵢ[R] M₁) (c : ↥p), ↑((LinearIsometry.submoduleMap p e) c) = e ↑c
-- Init.Data.SInt.Lemmas
Int32.add_eq_left : ∀ {a b : Int32}, a + b = a ↔ b = 0
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.iSupLift_mk : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : NonUnitalNonAssocSemiring B] [inst_4 : Module R B] [inst_5 : IsScalarTower R A A]
  [inst_6 : SMulCommClass R A A] {ι : Sort u_1} [inst_7 : Nonempty ι] {K : ι → NonUnitalSubalgebra R A}
  {dir : Directed (fun x1 x2 => x1 ≤ x2) K} {f : (i : ι) → ↥(K i) →ₙₐ[R] B}
  {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (NonUnitalSubalgebra.inclusion h)} {T : NonUnitalSubalgebra R A}
  {hT : T = iSup K} {i : ι} (x : ↥(K i)) (hx : ↑x ∈ T),
  (NonUnitalSubalgebra.iSupLift K dir f hf T hT) ⟨↑x, hx⟩ = (f i) x
-- Lean.Parser.Module.Syntax
Lean.Parser.Module.header.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.ENode.isCongrRoot : Lean.Meta.Grind.ENode → Bool
-- Std.Http.Data.Body.Empty
Std.Http.Body.instCoeAsyncResponseEmptyContextAsyncAny : Coe (Std.Async.Async (Std.Http.Response Std.Http.Body.Empty))
  (Std.Async.ContextAsync (Std.Http.Response Std.Http.Body.Any))
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Continuous.measurable2 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_5} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α]
  [OpensMeasurableSpace α] [inst_3 : TopologicalSpace β] [inst_4 : MeasurableSpace β] [OpensMeasurableSpace β]
  [inst_6 : TopologicalSpace γ] [inst_7 : MeasurableSpace γ] [BorelSpace γ] [inst_9 : MeasurableSpace δ]
  [SecondCountableTopologyEither α β] {f : δ → α} {g : δ → β} {c : α → β → γ},
  (Continuous fun p => c p.1 p.2) → Measurable f → Measurable g → Measurable fun a => c (f a) (g a)
-- Init.Prelude
instHashableString : Hashable String
-- Lean.Elab.Command.Scope
Lean.Elab.Command.instInhabitedScope.default : Lean.Elab.Command.Scope
-- Mathlib.Probability.Independence.Integrable
/-- If a nonzero function is integrable and is independent of another function, then
the space is a probability space.  -/
MeasureTheory.Integrable.isProbabilityMeasure_of_indepFun : ∀ {Ω : Type u_1} {E : Type u_2} {F : Type u_3} [inst : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  [inst_1 : NormedAddCommGroup E] [inst_2 : MeasurableSpace E] [OpensMeasurableSpace E] [inst_4 : MeasurableSpace F]
  (f : Ω → E) (g : Ω → F),
  MeasureTheory.Integrable f μ →
    (¬∀ᵐ (ω : Ω) ∂μ, f ω = 0) → ProbabilityTheory.IndepFun f g μ → MeasureTheory.IsProbabilityMeasure μ
-- Mathlib.Data.List.Chain
/-- If an `r`-decreasing chain `l` is empty or its head is accessible by `r`, then
`l` is accessible by the lexicographic order `List.Lex r`.  -/
Acc.list_chain' : ∀ {α : Type u_1} {r : α → α → Prop} {l : List.chains r}, (∀ a ∈ (↑l).head?, Acc r a) → Acc (List.lex_chains r) l
-- Mathlib.SetTheory.Cardinal.Cofinality.Club
IsClub.iInter_of_countable : ∀ {α : Type v} [inst : LinearOrder α] [WellFoundedLT α] {ι : Sort u_1} {f : ι → Set α} [Countable ι],
  Order.cof α ≠ Cardinal.aleph0 → (∀ (i : ι), IsClub (f i)) → IsClub (⋂ i, f i)
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Parser.indexing_modeHyp_ : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- Two maps to the domain of `f`  -/
CategoryTheory.RegularEpi.right : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} → {f : X ⟶ Y} → (self : CategoryTheory.RegularEpi f) → self.W ⟶ X
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.isLoop_iff : ∀ {α : Type u_1} {M : Matroid α} {e : α}, M.IsLoop e ↔ e ∈ M.loops
-- Mathlib.SetTheory.ZFC.Class
/-- **There is no universal set.**
This is stated as `univ ∉ univ`, meaning that `univ` (the class of all sets) is proper (does not
belong to the class of all sets).  -/
Class.univ_notMem_univ : Class.univ ∉ Class.univ
-- Init.Grind.AC
Lean.Grind.AC.instReprSeq.repr : Lean.Grind.AC.Seq → ℕ → Std.Format
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
CategoryTheory.leftAdjointMate_comp_evaluation : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
  [inst_2 : CategoryTheory.HasLeftDual X] [inst_3 : CategoryTheory.HasLeftDual Y] (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (ᘁf)) (ε_ (ᘁX) X) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f ᘁY) (ε_ (ᘁY) Y)
-- Mathlib.GroupTheory.Commutator.Basic
Commute.commutator_eq : ∀ {G : Type u_1} [inst : Group G] {g₁ g₂ : G}, Commute g₁ g₂ → ⁅g₁, g₂⁆ = 1
-- Mathlib.RingTheory.TwoSidedIdeal.Basic
TwoSidedIdeal.mem_op_iff : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] {I : TwoSidedIdeal R} {x : Rᵐᵒᵖ}, x ∈ I.op ↔ MulOpposite.unop x ∈ I
-- Lean.Meta.Tactic.FunIndInfo
Lean.Meta.getFunInductName : Lean.Name → optParam Bool false → Lean.Name
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
/-- The equivalence relation on right fractions for a morphism property `W`.  -/
CategoryTheory.MorphismProperty.RightFractionRel : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W : CategoryTheory.MorphismProperty C} → {X Y : C} → W.RightFraction X Y → W.RightFraction X Y → Prop
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.kernel.lift.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.HasKernel f] {W : C} (k k_1 : W ⟶ X) (e_k : k = k_1)
  (h : CategoryTheory.CategoryStruct.comp k f = 0),
  CategoryTheory.Limits.kernel.lift f k h = CategoryTheory.Limits.kernel.lift f k_1 ⋯
-- Mathlib.Algebra.Prime.Lemmas
/-- **Alias** of `not_irreducible_of_not_isUnit_of_dvdNotUnit`. -/
not_irreducible_of_not_unit_dvdNotUnit : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] {p q : M}, ¬IsUnit p → DvdNotUnit p q → ¬Irreducible q
-- Mathlib.CategoryTheory.PathCategory.Basic
CategoryTheory.Paths.lift_nil : ∀ {V : Type u₁} [inst : Quiver V] {C : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} C] (φ : V ⥤q C) (X : V),
  (CategoryTheory.Paths.lift φ).map Quiver.Path.nil = CategoryTheory.CategoryStruct.id (φ.obj X)
-- Mathlib.RingTheory.Smooth.Basic
Algebra.FormallySmooth.instLocalization : ∀ {R : Type u_4} {A : Type u_5} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [Algebra.FormallySmooth R A] (M : Submonoid A), Algebra.FormallySmooth R (Localization M)
-- Mathlib.RepresentationTheory.Homological.TateCohomology.Basic
_private.Mathlib.RepresentationTheory.Homological.TateCohomology.Basic.0.CochainComplex.ConnectData.X.match_1.splitter : (motive : ℤ → Sort u_1) → (x : ℤ) → ((n : ℕ) → motive (Int.ofNat n)) → ((n : ℕ) → motive (Int.negSucc n)) → motive x
-- Mathlib.RingTheory.Etale.Basic
Algebra.Etale.instAway : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] (s : A)
  [Algebra.Etale R A], Algebra.Etale R (Localization.Away s)
-- Lean.Widget.UserWidget
Lean.Widget.instToModuleModule : Lean.Widget.ToModule Lean.Widget.Module
-- Mathlib.RepresentationTheory.Intertwining
/-- An intertwining map between two representations `ρ` and `σ` of the same monoid `G` is a map
between underlying modules which commutes with the `G`-actions.  -/
Representation.IntertwiningMap : {A : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        [inst : Semiring A] →
          [inst_1 : Monoid G] →
            [inst_2 : AddCommMonoid V] →
              [inst_3 : AddCommMonoid W] →
                [inst_4 : Module A V] →
                  [inst_5 : Module A W] → Representation A G V → Representation A G W → Type (max u_3 u_4)
-- Mathlib.MeasureTheory.Measure.Typeclasses.NullSingletonClass
Set.Countable.ae_notMem : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {s : Set α},
  s.Countable → ∀ (μ : MeasureTheory.Measure α) [MeasureTheory.NullSingletonClass μ], ∀ᵐ (x : α) ∂μ, x ∉ s
-- Std.Data.String.ToNat
String.Slice.isNat_comp_copy : String.isNat ∘ String.Slice.copy = String.Slice.isNat
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.Substring.Raw.toString.eq_1 : ∀ (s : String) (b e : String.Pos.Raw), { str := s, startPos := b, stopPos := e }.toString = String.Pos.Raw.extract s b e
-- Mathlib.Algebra.ContinuedFractions.Computation.Translations
GenContFract.of_terminatedAt_iff_intFractPair_seq1_terminatedAt : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : FloorRing K] {v : K} {n : ℕ},
  (GenContFract.of v).TerminatedAt n ↔ (GenContFract.IntFractPair.seq1 v).2.TerminatedAt n
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.coe_smul : ∀ {S : Type u_1} {R : Type u_3} {c₁ c₂ c₃ : R} [inst : Zero R] [inst_1 : SMulZeroClass S R] (s : S) (r : R),
  ↑(s • r) = s • ↑r
-- Mathlib.Data.List.Defs
/-- `iterate f a n` is `[a, f a, ..., f^[n - 1] a]`.  -/
List.iterate : {α : Type u_1} → (α → α) → α → ℕ → List α
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- **Alias** of `CategoryTheory.SubobjectRepresentableBy.hasTerminal`. -/
CategoryTheory.Classifier.SubobjectRepresentableBy.hasTerminal : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {Ω : C}
  (h : CategoryTheory.SubobjectRepresentableBy Ω), CategoryTheory.Limits.HasTerminal C
-- Mathlib.Topology.Category.TopCat.Monoidal
TopCat.I.ext : ∀ {x y : ↑TopCat.I}, TopCat.I.homeomorph x = TopCat.I.homeomorph y → x = y
-- Mathlib.Topology.Compactness.Compact
Filter.cocompact_le_coclosedCompact : ∀ {X : Type u} [inst : TopologicalSpace X], Filter.cocompact X ≤ Filter.coclosedCompact X
-- Mathlib.Combinatorics.Schnirelmann
_private.Mathlib.Combinatorics.Schnirelmann.0.add_eq_univ_of_one_le_schirelmannDensity_add_schnirelmannDensity.match_1_1.eq_1 : ∀ (motive : ℕ ⊕ ℕ → Sort u_1) (x : ℕ) (h_1 : (x : ℕ) → motive (Sum.inl x)) (h_2 : (y : ℕ) → motive (Sum.inr y)),
  (match Sum.inl x with
    | Sum.inl x => h_1 x
    | Sum.inr y => h_2 y) =
    h_1 x
-- Init.Data.Nat.Div.Basic
Nat.mul_add_mod_self_left : ∀ (a b c : ℕ), (a * b + c) % a = c % a
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
coe_nnreal_ennreal_nndist : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x y : α), ↑(nndist x y) = edist x y
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.instAddCommGroupCoeOfAddSubgroupClass.eq_1 : ∀ {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)]
  {B : (i : ι) → S i} [inst_1 : (i : ι) → AddCommGroup (R i)] [inst_2 : ∀ (i : ι), AddSubgroupClass (S i) (R i)],
  RestrictedProduct.instAddCommGroupCoeOfAddSubgroupClass R = Function.Injective.addCommGroup DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm'_norm_rpow : ∀ {α : Type u_1} {F : Type u_5} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup F]
  (f : α → F) (p q : ℝ),
  0 < q → MeasureTheory.eLpNorm' (fun x => ‖f x‖ ^ q) p μ = MeasureTheory.eLpNorm' f (p * q) μ ^ q
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.instIsScalarTowerSubtypeMemOfNatLocalization : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι] {𝒜 : ι → σ}
  [inst_5 : GradedRing 𝒜] {x : Submonoid A}, IsScalarTower (↥(𝒜 0)) (HomogeneousLocalization 𝒜 x) (Localization x)
-- Mathlib.AlgebraicTopology.SimplexCategory.Defs
/-- The simplex category:
* for each `n : ℕ`, there is an object `⦋n⦌`;
* morphisms `⦋n⦌ ⟶ ⦋m⦌` are monotone functions `Fin (n+1) → Fin (m+1)`
 -/
SimplexCategory : Type
-- Mathlib.FieldTheory.KummerExtension
_private.Mathlib.FieldTheory.KummerExtension.0.X_pow_sub_C_eq_prod' : ∀ {K : Type u} [inst : Field K] {n : ℕ} {ζ : K},
  IsPrimitiveRoot ζ n →
    ∀ {α a : K},
      0 < n →
        α ^ n = a → Polynomial.X ^ n - Polynomial.C a = ∏ i ∈ Finset.range n, (Polynomial.X - Polynomial.C (ζ ^ i * α))
-- Mathlib.Data.Finset.Sups
Finset.powerset_sups_powerset_self : ∀ {α : Type u_2} [inst : DecidableEq α] (s : Finset α), s.powerset ⊻ s.powerset = s.powerset
-- Mathlib.Order.BooleanAlgebra.Set
Set.sdiff_singleton_ssubset : ∀ {α : Type u_1} {s : Set α} {a : α}, s \ {a} ⊂ s ↔ a ∈ s
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.head_some_of_get?_some : ∀ {α : Type u} {s : Stream'.WSeq α} {a : α} {n : ℕ}, some a ∈ s.get? n → ∃ a', some a' ∈ s.head
-- Aesop.Util.Basic
Aesop.instMonadParentDeclReaderT_aesop : {m : Type → Type} → {ρ : Type} → [Lean.Elab.MonadParentDecl m] → Lean.Elab.MonadParentDecl (ReaderT ρ m)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKey?_bind_getKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t.maxKey?.bind t.getKey? = t.maxKey?
-- Mathlib.Order.Category.CompleteLat
completeLat_dual_comp_forget_to_bddLat : CompleteLat.dual.comp (CategoryTheory.forget₂ CompleteLat BddLat) =
  (CategoryTheory.forget₂ CompleteLat BddLat).comp BddLat.dual
-- Mathlib.RingTheory.Ideal.Norm.RelNorm
/-- See `Ideal.relNorm_eq_pow_of_isMaximal` for a statement that does not require the extension to
be Galois.
 -/
Ideal.relNorm_eq_pow_of_isPrime_isGalois : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] {S : Type u_3} [inst_2 : CommRing S] [inst_3 : IsDomain S]
  [inst_4 : IsIntegrallyClosed R] [inst_5 : IsIntegrallyClosed S] [inst_6 : Algebra R S] [inst_7 : Module.Finite R S]
  [inst_8 : Module.IsTorsionFree R S] [inst_9 : IsDedekindDomain R] [inst_10 : IsDedekindDomain S] (P : Ideal S)
  (p : Ideal R) [hPp : P.LiesOver p] [p.IsMaximal] [P.IsPrime] [IsGalois (FractionRing R) (FractionRing S)],
  (Ideal.relNorm R) P = p ^ P.inertiaDeg R
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
Finpartition.IsEquipartition.sum_nonUniforms_lt' : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : DecidableEq α] {A : Finset α} {P : Finpartition A} {G : SimpleGraph α} [inst_4 : DecidableRel G.Adj]
  {ε : 𝕜},
  A.Nonempty →
    0 < ε →
      P.IsEquipartition →
        P.IsUniform G ε → ∑ i ∈ P.nonUniforms G ε, ↑i.1.card * ↑i.2.card < ε * (↑A.card + ↑P.parts.card) ^ 2
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.le_minKey : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    ∀ {k : α} {he : t.isEmpty = false}, (compare k (t.minKey he)).isLE = true ↔ ∀ k' ∈ t, (compare k k').isLE = true
-- Mathlib.Algebra.Squarefree.Basic
Squarefree.isRadical : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] [DecompositionMonoid R] {x : R}, Squarefree x → IsRadical x
-- Lean.Data.Lsp.BasicAux
Lean.Lsp.instBEqRange.beq : Lean.Lsp.Range → Lean.Lsp.Range → Bool
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.map_C : ∀ {Γ : Type u_1} {R : Type u_3} {S : Type u_4} [inst : AddCommMonoid Γ] [inst_1 : PartialOrder Γ]
  [inst_2 : IsOrderedCancelAddMonoid Γ] [inst_3 : NonAssocSemiring R] [inst_4 : NonAssocSemiring S] (a : R)
  (f : R →+* S), (HahnSeries.C a).map f = HahnSeries.C (f a)
-- Init.Data.FloatArray.Basic
FloatArray.ext : ∀ {x y : FloatArray}, x.data = y.data → x = y
-- Mathlib.CategoryTheory.ObjectProperty.Basic
CategoryTheory.ObjectProperty.ofObj_apply : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] {ι : Type u'} (X : ι → C) (i : ι),
  CategoryTheory.ObjectProperty.ofObj X (X i)
-- Mathlib.Algebra.Homology.Embedding.Basic
/-- The obvious embedding from `up ℕ` to `up ℤ`.  -/
ComplexShape.embeddingUpNat : (ComplexShape.up ℕ).Embedding (ComplexShape.up ℤ)
-- Mathlib.NumberTheory.FLT.Three
/-- We have that `S.Solution'_descent.multiplicity < S.multiplicity`.  -/
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.Solution'_descent_multiplicity_lt : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S : FermatLastTheoremForThreeGen.Solution✝ hζ)
  [inst_1 : NumberField K] [inst_2 : IsCyclotomicExtension {3} ℚ K],
  FermatLastTheoremForThreeGen.Solution'.multiplicity✝ (FermatLastTheoremForThreeGen.Solution.Solution'_descent✝ S) <
    FermatLastTheoremForThreeGen.Solution.multiplicity✝ S
-- Mathlib.SetTheory.Ordinal.Principal
Ordinal.isPrincipal_zero : ∀ {op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}}, Ordinal.IsPrincipal op 0
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
/-- A vector added to the first point lies in the affine span of two points if and only if it is
a multiple of their difference.  -/
vadd_left_mem_affineSpan_pair : ∀ {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₁ p₂ : P} {v : V}, v +ᵥ p₁ ∈ line[k, p₁, p₂] ↔ ∃ r, r • (p₂ -ᵥ p₁) = v
-- Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions
/-- Bound for the operator norm of `ContinuousMap.toLp`.  -/
ContinuousMap.toLp_norm_le : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} (μ : MeasureTheory.Measure α)
  [inst : TopologicalSpace α] [inst_1 : BorelSpace α] [inst_2 : NormedAddCommGroup E]
  [inst_3 : SecondCountableTopologyEither α E] [inst_4 : CompactSpace α] [inst_5 : MeasureTheory.IsFiniteMeasure μ]
  [inst_6 : Fact (1 ≤ p)] {𝕜 : Type u_4} [inst_7 : NontriviallyNormedField 𝕜] [inst_8 : NormedSpace 𝕜 E],
  ‖ContinuousMap.toLp p μ 𝕜‖ ≤ ↑(MeasureTheory.measureUnivNNReal μ) ^ p.toReal⁻¹
-- Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
SchwartzMap.fourierInv_coe : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {V : Type u_3} [inst_2 : NormedAddCommGroup V]
  [inst_3 : InnerProductSpace ℝ V] [inst_4 : FiniteDimensional ℝ V] [inst_5 : MeasurableSpace V] [inst_6 : BorelSpace V]
  (f : SchwartzMap V E), ⇑(FourierTransformInv.fourierInv f) = FourierTransformInv.fourierInv ⇑f
-- Mathlib.Data.List.Lattice
List.inter_cons_of_mem : ∀ {α : Type u_1} {l₂ : List α} {a : α} [inst : DecidableEq α] (l₁ : List α), a ∈ l₂ → (a :: l₁) ∩ l₂ = a :: l₁ ∩ l₂
-- Mathlib.Topology.Algebra.Group.CompactOpen
ContinuousAddMonoidHom.instIsTopologicalAddGroup : ∀ {A : Type u_2} {E : Type u_6} [inst : AddMonoid A] [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace E] [inst_4 : IsTopologicalAddGroup E], IsTopologicalAddGroup (A →ₜ+ E)
-- Mathlib.GroupTheory.Congruence.Hom
Con.mapOfSurjective.eq_1 : ∀ {M : Type u_1} {N : Type u_2} {F : Type u_4} [inst : Mul M] [inst_1 : Mul N] [inst_2 : FunLike F M N]
  [inst_3 : MulHomClass F M N] {c : Con M} (f : F) (h : Con.ker f ≤ c) (hf : Function.Surjective ⇑f),
  Con.mapOfSurjective f h hf = { toSetoid := c.mapOfSurjective (⇑f) h hf, mul' := ⋯ }
-- Lean.Elab.Command
Lean.Elab.Command.runLinters : Lean.Syntax → Lean.Elab.Command.CommandElabM Unit
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBicone.ofIso_fst : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P P' Q Q' : C} (b : CategoryTheory.Limits.BinaryBicone P Q) (eP : P ≅ P') (eQ : Q ≅ Q'),
  (b.ofIso eP eQ).fst = CategoryTheory.CategoryStruct.comp b.fst eP.hom
-- Lean.Syntax
Lean.Syntax.unescapeAntiquot : Lean.Syntax → Lean.Syntax
-- Lean.Attributes
_private.Lean.Attributes.0.Lean.addAttrEntry : Lean.AttributeExtensionState → Lean.AttributeExtensionOLeanEntry × Lean.AttributeImpl → Lean.AttributeExtensionState
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
/-- A pointwise right Kan extension of `F` along `L` applied to an object `Y` is isomorphic to
`limit (StructuredArrow.proj Y L ⋙ F)`.  -/
CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtensionAt.isoLimit : {C : Type u_1} →
  {D : Type u_2} →
    {H : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} H] →
            {L : CategoryTheory.Functor C D} →
              {F : CategoryTheory.Functor C H} →
                {E : L.RightExtension F} →
                  {Y : D} →
                    E.IsPointwiseRightKanExtensionAt Y →
                      [inst_3 : CategoryTheory.Limits.HasLimit ((CategoryTheory.StructuredArrow.proj Y L).comp F)] →
                        (CategoryTheory.CostructuredArrow.left E).obj Y ≅
                          CategoryTheory.Limits.limit ((CategoryTheory.StructuredArrow.proj Y L).comp F)
-- Mathlib.Analysis.Calculus.Deriv.Comp
HasDerivWithinAt.scomp : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (x : 𝕜) {s : Set 𝕜} {𝕜' : Type u_1} [inst_3 : NontriviallyNormedField 𝕜']
  [inst_4 : NormedAlgebra 𝕜 𝕜'] [inst_5 : NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {t' : Set 𝕜'} {h : 𝕜 → 𝕜'} {h' : 𝕜'}
  {g₁ : 𝕜' → F} {g₁' : F},
  HasDerivWithinAt g₁ g₁' t' (h x) →
    HasDerivWithinAt h h' s x → Set.MapsTo h s t' → HasDerivWithinAt (g₁ ∘ h) (h' • g₁') s x
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get_inter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} {h_mem : k ∈ t₁ ∩ t₂}, (t₁ ∩ t₂).get k h_mem = t₁.get k ⋯
-- Mathlib.GroupTheory.GroupAction.Hom
MulSemiringActionHom.coe_fn_coe : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} {R : Type u_10} [inst_2 : Semiring R]
  [inst_3 : MulSemiringAction M R] {S : Type u_12} [inst_4 : Semiring S] [inst_5 : MulSemiringAction N S]
  (f : R →ₑ+*[φ] S), ⇑↑f = ⇑f
-- Batteries.Recycling.RBTree.Basic
/-- `O(log n)`. Find the value corresponding to key `k`.  -/
RBTree.RBMap.find? : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → RBTree.RBMap α β cmp → α → Option β
-- Init.Data.SInt.Lemmas
ISize.lt_or_le : ∀ (a b : ISize), a < b ∨ b ≤ a
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
/-- **Alias** of `AlgebraicGeometry.Scheme.Hom.finite_preimage_singleton`. -/
AlgebraicGeometry.IsFinite.finite_preimage_singleton : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.LocallyQuasiFinite f]
  [AlgebraicGeometry.QuasiCompact f] (y : ↥Y), (⇑f ⁻¹' {y}).Finite
-- Mathlib.Algebra.MonoidAlgebra.ToDirectSum
DirectSum.toAddMonoidAlgebra_pow : ∀ {ι : Type u_1} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : AddMonoid ι] [inst_2 : Semiring M]
  [inst_3 : (m : M) → Decidable (m ≠ 0)] (f : DirectSum ι fun x => M) (n : ℕ),
  (f ^ n).toAddMonoidAlgebra = f.toAddMonoidAlgebra ^ n