mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKey?_le_maxKey?_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k} {km kmi : α}, t.maxKey? = some km → (t.insertIfNew k v).maxKey?.get ⋯ = kmi → (cmp km kmi).isLE = true
-- Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
AlgebraicGeometry.Scheme.IdealSheafData.comap_bot : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y), ⊥.comap f = ⊥
-- Mathlib.CategoryTheory.Abelian.Basic
/-- In an abelian category, a mono is the kernel of its cokernel. More precisely:
If `f` is a monomorphism and `s` is some colimit cokernel cocone on `f`, then `f` is a kernel
of `cofork.π s`.  -/
CategoryTheory.Abelian.monoIsKernelOfCokernel : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {X Y : C} →
        {f : X ⟶ Y} →
          [CategoryTheory.Mono f] →
            (s : CategoryTheory.Limits.Cofork f 0) →
              CategoryTheory.Limits.IsColimit s →
                CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι f ⋯)
-- Lean.Elab.Declaration
Lean.Elab.Command.expandMutualPreamble : Lean.Macro
-- Mathlib.Data.Finsupp.Defs
Finsupp.default_eq_zero : ∀ {α : Type u_1} {M : Type u_4} [inst : Zero M], default = 0
-- Mathlib.Algebra.Group.InjSurj
/-- A type endowed with `0`, `+`, unary `-`, and binary `-` is a
`SubNegMonoid` if it admits an injective map that preserves `0`, `+`, unary `-`, and binary `-` to
a `SubNegMonoid`. This version takes custom `nsmul` and `zsmul` as `[SMul ℕ M₁]` and `[SMul ℤ M₁]`
arguments.  -/
Function.Injective.subNegMonoid : {M₁ : Type u_1} →
  {M₂ : Type u_2} →
    [inst : Add M₁] →
      [inst_1 : Zero M₁] →
        [inst_2 : SMul ℕ M₁] →
          [inst_3 : Neg M₁] →
            [inst_4 : Sub M₁] →
              [inst_5 : SMul ℤ M₁] →
                [inst_6 : SubNegMonoid M₂] →
                  (f : M₁ → M₂) →
                    Function.Injective f →
                      f 0 = 0 →
                        (∀ (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 (n • x) = n • f x) →
                                (∀ (x : M₁) (n : ℤ), f (n • x) = n • f x) → SubNegMonoid M₁
-- Mathlib.Algebra.CubicDiscriminant
_private.Mathlib.Algebra.CubicDiscriminant.0.Cubic.coeffs : ∀ {R : Type u_1} {P : Cubic R} [inst : Semiring R],
  (∀ n > 3, P.toPoly.coeff n = 0) ∧
    P.toPoly.coeff 3 = P.a ∧ P.toPoly.coeff 2 = P.b ∧ P.toPoly.coeff 1 = P.c ∧ P.toPoly.coeff 0 = P.d
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.DiseqCnstr.mk : Lean.Grind.Linarith.Poly → Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof → Lean.Meta.Grind.Arith.Linear.DiseqCnstr
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.mulSingle_one : ∀ {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [inst : (i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i)
  [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → One (G i)] [inst_3 : ∀ (i : ι), OneMemClass (S i) (G i)] (i : ι),
  RestrictedProduct.mulSingle A i 1 = 1
-- Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
MeasureTheory.left_measure_le_of_levyProkhorovEDist_lt : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : PseudoEMetricSpace Ω] {μ ν : MeasureTheory.Measure Ω}
  {c : ENNReal},
  MeasureTheory.levyProkhorovEDist μ ν < c → ∀ {B : Set Ω}, MeasurableSet B → μ B ≤ ν (Metric.thickening c.toReal B) + c
-- Mathlib.Order.Closure
ClosureOperator.mk.inj : ∀ {α : Type u_1} {inst : Preorder α} {toOrderHom : α →o α} {le_closure' : ∀ (x : α), x ≤ toOrderHom.toFun x}
  {idempotent' : ∀ (x : α), toOrderHom.toFun (toOrderHom.toFun x) = toOrderHom.toFun x} {IsClosed : α → Prop}
  {isClosed_iff : autoParam (∀ {x : α}, IsClosed x ↔ toOrderHom.toFun x = x) ClosureOperator.isClosed_iff._autoParam}
  {toOrderHom_1 : α →o α} {le_closure'_1 : ∀ (x : α), x ≤ toOrderHom_1.toFun x}
  {idempotent'_1 : ∀ (x : α), toOrderHom_1.toFun (toOrderHom_1.toFun x) = toOrderHom_1.toFun x} {IsClosed_1 : α → Prop}
  {isClosed_iff_1 :
    autoParam (∀ {x : α}, IsClosed_1 x ↔ toOrderHom_1.toFun x = x) ClosureOperator.isClosed_iff._autoParam},
  { toOrderHom := toOrderHom, le_closure' := le_closure', idempotent' := idempotent', IsClosed := IsClosed,
        isClosed_iff := isClosed_iff } =
      { toOrderHom := toOrderHom_1, le_closure' := le_closure'_1, idempotent' := idempotent'_1, IsClosed := IsClosed_1,
        isClosed_iff := isClosed_iff_1 } →
    toOrderHom = toOrderHom_1 ∧ IsClosed = IsClosed_1
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
MeasureTheory.condExp_zero : ∀ {α : Type u_1} {E : Type u_3} {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E], μ[0 | m] = 0
-- Init.Control.Lawful.MonadAttach.Instances
_private.Init.Control.Lawful.MonadAttach.Instances.0.instLawfulMonadAttachExceptTOfLawfulMonad.match_2.eq_1 : ∀ {ε α : Type (max u_1 u_2)} {P : α → Prop} (motive : Except ε (Subtype P) → Sort u_3) (a : Subtype P)
  (h_1 : (a : Subtype P) → motive (Except.ok a)) (h_2 : (e : ε) → motive (Except.error e)),
  (match Except.ok a with
    | Except.ok a => h_1 a
    | Except.error e => h_2 e) =
    h_1 a
-- Mathlib.Analysis.Distribution.TestFunction
/-- Notation for the space of "test functions", i.e. bundled smooth (infinitely differentiable) maps
with compact support.  -/
Distributions.«term𝓓(_,_)» : Lean.ParserDescr
-- Mathlib.Topology.LocallyFinsupp
/-- Simplifier lemma: `single x 0` is zero.
 -/
Function.locallyFinsuppWithin.single_zero : ∀ {X : Type u_1} [inst : TopologicalSpace X] {Y : Type u_2} [inst_1 : DecidableEq X] [inst_2 : Zero Y] {x : X},
  Function.locallyFinsuppWithin.single x 0 = 0
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
SemiNormedGrp.explicitCokernelIso_hom_π : ∀ {X Y : SemiNormedGrp} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (SemiNormedGrp.explicitCokernelπ f) (SemiNormedGrp.explicitCokernelIso f).hom =
    CategoryTheory.Limits.cokernel.π f
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.separatingRight_iff_linear_flip_nontrivial : ∀ {R : Type u_1} {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_5} {M₁ : Type u_6} {M₂ : Type u_7} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : CommSemiring R₁] [inst_4 : AddCommMonoid M₁]
  [inst_5 : Module R₁ M₁] [inst_6 : CommSemiring R₂] [inst_7 : AddCommMonoid M₂] [inst_8 : Module R₂ M₂] {I₁ : R₁ →+* R}
  {I₂ : R₂ →+* R} {B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M}, B.SeparatingRight ↔ ∀ (y : M₂), B.flip y = 0 → y = 0
-- Mathlib.Analysis.Seminorm
Seminorm.restrictScalars_ball : ∀ (𝕜 : Type u_3) {E : Type u_7} {𝕜' : Type u_12} [inst : NormedField 𝕜] [inst_1 : SeminormedRing 𝕜']
  [inst_2 : SMul 𝕜 𝕜'] [inst_3 : NormSMulClass 𝕜 𝕜'] [inst_4 : NormOneClass 𝕜'] [inst_5 : AddCommGroup E]
  [inst_6 : Module 𝕜' E] [inst_7 : SMul 𝕜 E] [inst_8 : IsScalarTower 𝕜 𝕜' E] (p : Seminorm 𝕜' E),
  (Seminorm.restrictScalars 𝕜 p).ball = p.ball
-- Mathlib.RingTheory.Localization.Away.Basic
IsLocalization.Away.isUnit_of_dvd : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (x : R)
  [IsLocalization.Away x S] {r : R}, r ∣ x → IsUnit ((algebraMap R S) r)
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
CategoryTheory.IsRegularEpi.regularEpi : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {X Y : C} {f : X ⟶ Y}
  [self : CategoryTheory.IsRegularEpi f], Nonempty (CategoryTheory.RegularEpi f)
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.sSup_toSubmodule : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (S : Set (LieSubmodule R L M)),
  ↑(sSup S) = sSup {x | ∃ s ∈ S, ↑s = x}
-- Mathlib.Data.Rat.BigOperators
Rat.cast_list_prod : ∀ {α : Type u_2} [inst : DivisionRing α] [CharZero α] (s : List ℚ), ↑s.prod = (List.map Rat.cast s).prod
-- Mathlib.NumberTheory.Divisors
Nat.swap_mem_divisorsAntidiagonalList : ∀ {n : ℕ} {a : ℕ × ℕ}, a.swap ∈ n.divisorsAntidiagonalList ↔ a ∈ n.divisorsAntidiagonalList
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PullbackObjObj.π_fst_assoc : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₃ Y₃ : C₃}
  {f₃ : X₃ ⟶ Y₃} (self : G.PullbackObjObj f₁ f₃) {Z : C₂} (h : (G.obj (Opposite.op X₁)).obj X₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.π (CategoryTheory.CategoryStruct.comp self.fst h) =
    CategoryTheory.CategoryStruct.comp ((G.map f₁.op).app X₃) h
-- Mathlib.Geometry.Euclidean.Sphere.OrthRadius
EuclideanGeometry.Sphere.orthogonalProjection_orthRadius_center : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (s : EuclideanGeometry.Sphere P) (p : P),
  ↑((EuclideanGeometry.orthogonalProjection (s.orthRadius p)) s.center) = p
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.lift_type_lt : ∀ {α : Type u} {β : Type v} {r : α → α → Prop} {s : β → β → Prop} [inst : IsWellOrder α r] [inst_1 : IsWellOrder β s],
  Ordinal.lift.{max v w, u} (Ordinal.type r) < Ordinal.lift.{max u w, v} (Ordinal.type s) ↔ Nonempty (PrincipalSeg r s)
-- Mathlib.Algebra.Order.BigOperators.Expect
Finset.expect_eq_zero_iff_of_nonpos : ∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α]
  [inst_3 : Module ℚ≥0 α] {s : Finset ι} {f : ι → α},
  (∀ i ∈ s, f i ≤ 0) → ((s.expect fun i => f i) = 0 ↔ ∀ i ∈ s, f i = 0)
-- Mathlib.Analysis.Asymptotics.LinearGrowth
LinearGrowth.linearGrowthSup_eventually_monotone : ∀ {u v : ℕ → EReal}, u ≤ᶠ[Filter.atTop] v → LinearGrowth.linearGrowthSup u ≤ LinearGrowth.linearGrowthSup v
-- Mathlib.Topology.UrysohnsLemma
/-- Urysohn's lemma: if `s` and `t` are two disjoint sets in a regular locally compact topological
space `X`, with `s` compact and `t` closed, then there exists a continuous compactly supported
function `f : X → ℝ` such that

* `f` equals one on `s`;
* `f` equals zero on `t`;
* `0 ≤ f x ≤ 1` for all `x`.

Moreover, if `s` is Gδ, one can ensure that `f ⁻¹ {1}` is exactly `s`.
 -/
exists_continuous_one_zero_of_isCompact_of_isGδ : ∀ {X : Type u_1} [inst : TopologicalSpace X] [RegularSpace X] [LocallyCompactSpace X] {s t : Set X},
  IsCompact s →
    IsGδ s →
      IsClosed t →
        Disjoint s t → ∃ f, s = ⇑f ⁻¹' {1} ∧ Set.EqOn (⇑f) 0 t ∧ HasCompactSupport ⇑f ∧ ∀ (x : X), f x ∈ Set.Icc 0 1
-- Mathlib.Algebra.Group.Conj
isAddConj_iff_eq : ∀ {α : Type u_1} [inst : AddCommMonoid α] {a b : α}, IsAddConj a b ↔ a = b
-- Init.Tactics
/-- In tactic mode, `if t then tac1 else tac2` is alternative syntax for:
```
by_cases t
· tac1
· tac2
```
It performs case distinction on `h† : t` or `h† : ¬t`, where `h†` is an anonymous hypothesis, and
`tac1` and `tac2` are the subproofs. (It doesn't actually use nondependent `if`, since this wouldn't
add anything to the context and hence would be useless for proving theorems. To actually insert an
`ite` application use `refine if t then ?_ else ?_`.)

The assumptions in each subgoal can be named. `if h : t then tac1 else tac2` can be used as
alternative syntax for:
```
by_cases h : t
· tac1
· tac2
```
It performs case distinction on `h : t` or `h : ¬t`.

You can use `?_` or `_` for either subproof to delay the goal to after the tactic, but
if a tactic sequence is provided for `tac1` or `tac2` then it will require the goal to be closed
by the end of the block.
 -/
Lean.Parser.Tactic.tacIfThenElse : Lean.ParserDescr
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
/-- A trail doesn't go through a vertex that is not 2-edge-reachable from its 2-edge-reachable
endpoints.  -/
SimpleGraph.Walk.IsTrail.not_mem_edges_of_not_isEdgeReachable_two : ∀ {V : Type u_1} {G : SimpleGraph V} {u v x : V} {w : G.Walk u v},
  w.IsTrail → G.IsEdgeReachable 2 u v → ¬G.IsEdgeReachable 2 u x → x ∉ w.support
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey_eq_minKey! : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  [inst_4 : Inhabited α] {l : List ((a : α) × β a)} {he : l.isEmpty = false},
  Std.Internal.List.minKey l he = Std.Internal.List.minKey! l
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurableSet_mem : ∀ {α : Type u_1} (a : α), MeasurableSet {s | a ∈ s}
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instSMulCommClass : ∀ {M : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] [inst_1 : SMul M X] [inst_2 : ContinuousConstSMul M X]
  {N : Type u_3} [inst_3 : SMul N X] [inst_4 : ContinuousConstSMul N X] [SMulCommClass M N X],
  SMulCommClass M N (SeparationQuotient X)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Complex.continuousOn_tan : ContinuousOn Complex.tan {x | Complex.cos x ≠ 0}
-- Mathlib.Algebra.Category.Ring.Basic
_private.Mathlib.Algebra.Category.Ring.Basic.0.SemiRingCat.Hom.mk.inj : ∀ {R S : SemiRingCat} {hom' hom'_1 : ↑R →+* ↑S}, { hom' := hom' } = { hom' := hom'_1 } → hom' = hom'_1
-- Mathlib.Order.LiminfLimsup
/-- If `Filter.limsup u atTop ≤ x`, then for all `ε > 0`, there exists a positive natural
number `n` such that `u n < x + ε`.  -/
Filter.exists_lt_of_limsup_le : ∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : AddZeroClass α] [AddLeftStrictMono α] {x ε : α}
  {u : ℕ → α}, Filter.IsBoundedUnder LE.le Filter.atTop u → Filter.limsup u Filter.atTop ≤ x → 0 < ε → ∃ n, u ↑n < x + ε
-- Std.Data.ExtTreeSet.Basic
/-- Removes all elements from the tree set for which the given function returns `false`.  -/
Std.ExtTreeSet.filter : {α : Type u} → {cmp : α → α → Ordering} → (α → Bool) → Std.ExtTreeSet α cmp → Std.ExtTreeSet α cmp
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsLongestMatch.eq : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {pos pos' : s.Pos},
  String.Slice.Pattern.Model.IsLongestMatch pat pos → String.Slice.Pattern.Model.IsLongestMatch pat pos' → pos = pos'
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.L₂'_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C), S.L₂'.f = S.δ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.size_alter_eq_self_of_not_mem : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] (h : t.WF)
  {k : α} {f : Option β → Option β},
  k ∉ t →
    (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).isNone = true →
      (Std.DTreeMap.Internal.Impl.Const.alter k f t ⋯).impl.size = t.size
-- Init.Data.List.Lemmas
List.eraseDupsBy_nil : ∀ {α : Type u_1} {r : α → α → Bool}, List.eraseDupsBy r [] = []
-- Mathlib.LinearAlgebra.TensorAlgebra.Basic
TensorAlgebra.range_lift : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {A : Type u_3}
  [inst_3 : Semiring A] [inst_4 : Algebra R A] (f : M →ₗ[R] A),
  ((TensorAlgebra.lift R) f).range = Algebra.adjoin R (Set.range ⇑f)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.toReal_pi : (↑Real.pi).toReal = Real.pi
-- Mathlib.Order.Category.BddDistLat
BddDistLat.ofHom_hom : ∀ {X Y : BddDistLat} (f : X ⟶ Y), BddDistLat.ofHom (BddDistLat.Hom.hom f) = f
-- Aesop.Search.Expansion
Aesop.RuleResult.proved.inj : ∀ {newRapps newRapps_1 : Array Aesop.RappRef},
  Aesop.RuleResult.proved newRapps = Aesop.RuleResult.proved newRapps_1 → newRapps = newRapps_1
-- Mathlib.Algebra.Module.Equiv.Basic
/-- If a linear map has an inverse, it is a linear equivalence.  -/
LinearEquiv.ofLinear : {R : Type u_1} →
  {R₂ : Type u_2} →
    {M : Type u_5} →
      {M₂ : Type u_7} →
        [inst : Semiring R] →
          [inst_1 : Semiring R₂] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommMonoid M₂] →
                {module_M : Module R M} →
                  {module_M₂ : Module R₂ M₂} →
                    {σ₁₂ : R →+* R₂} →
                      {σ₂₁ : R₂ →+* R} →
                        {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} →
                          {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} →
                            (f : M →ₛₗ[σ₁₂] M₂) →
                              (g : M₂ →ₛₗ[σ₂₁] M) → f ∘ₛₗ g = LinearMap.id → g ∘ₛₗ f = LinearMap.id → M ≃ₛₗ[σ₁₂] M₂
-- Mathlib.CategoryTheory.Localization.Construction
/-- The lifting of a functor `C ⥤ D` inverting `W` as a functor `W.Localization ⥤ D`  -/
CategoryTheory.Localization.Construction.lift : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    {W : CategoryTheory.MorphismProperty C} →
      {D : Type uD} →
        [inst_1 : CategoryTheory.Category.{uD', uD} D] →
          (G : CategoryTheory.Functor C D) → W.IsInvertedBy G → CategoryTheory.Functor W.Localization D
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.hom_ext_iff : ∀ {X : AlgebraicGeometry.Scheme} {M N : X.Modules} {f g : M ⟶ N},
  f = g ↔ ∀ (U : X.Opens), AlgebraicGeometry.Scheme.Modules.Hom.app f U = AlgebraicGeometry.Scheme.Modules.Hom.app g U
-- Lean.Elab.Term.TermElabM
/-- Elaborate `stx` and ensure result is a type.  -/
Lean.Elab.Term.elabType : Lean.Syntax → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.Algebra.Symmetrized
SymAlg.addCommGroup : {α : Type u_1} → [AddCommGroup α] → AddCommGroup αˢʸᵐ
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Spec_obj : ∀ (R : CommRingCatᵒᵖ), AlgebraicGeometry.Scheme.Spec.obj R = AlgebraicGeometry.Spec (Opposite.unop R)
-- Mathlib.GroupTheory.DivisibleHull
DivisibleHull.coe_add : ∀ {M : Type u_1} [inst : AddCommMonoid M] {m1 m2 : M}, ↑(m1 + m2) = ↑m1 + ↑m2
-- Mathlib.GroupTheory.Coxeter.Basic
_private.Mathlib.GroupTheory.Coxeter.Basic.0.CoxeterSystem.groupLift.eq_1 : ∀ {B : Type u_1} {W : Type u_3} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {G : Type u_5}
  [inst_1 : Group G] {f : B → G} (hf : M.IsLiftable f),
  CoxeterSystem.groupLift✝ cs hf = (PresentedGroup.toGroup ⋯).comp cs.mulEquiv.toMonoidHom
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
MeasureTheory.sigmaFinite_of_locallyFinite : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace α]
  [SecondCountableTopology α] [MeasureTheory.IsLocallyFiniteMeasure μ], MeasureTheory.SigmaFinite μ
-- Mathlib.Data.Finset.Powerset
/-- For `s` a finset, `s.ssubsets` is the finset comprising strict subsets of `s`.  -/
Finset.ssubsets : {α : Type u_1} → [DecidableEq α] → Finset α → Finset (Finset α)
-- Mathlib.LinearAlgebra.Basis.Defs
/-- If `R` and `R'` are isomorphic rings that act identically on a module `M`,
then a basis for `M` as `R`-module is also a basis for `M` as `R'`-module.

See also `Basis.algebraMapCoeffs` for the case where `f` is equal to `algebraMap`.
 -/
Module.Basis.mapCoeffs : {ι : Type u_10} →
  {R : Type u_11} →
    {M : Type u_12} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            Module.Basis ι R M →
              {R' : Type u_13} →
                [inst_3 : Semiring R'] →
                  [inst_4 : Module R' M] → (f : R ≃+* R') → (∀ (c : R) (x : M), f c • x = c • x) → Module.Basis ι R' M
-- Lean.Linter.MissingDocs
Lean.Linter.getLinterMissingDocs : Lean.Linter.LinterOptions → Bool
-- Mathlib.Algebra.MonoidAlgebra.Degree
AddMonoidAlgebra.coeff_eq_zero_of_not_le_supDegree : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_5} [inst : Semiring R] [inst_1 : SemilatticeSup B] [inst_2 : OrderBot B]
  {D : A → B} {p : AddMonoidAlgebra R A} {a : A}, ¬D a ≤ AddMonoidAlgebra.supDegree D p → p.coeff a = 0
-- Mathlib.Tactic.CategoryTheory.Coherence.PureCoherence
/-- The normalized 1-morphism.  -/
Mathlib.Tactic.BicategoryLike.Normalize.Result.normalizedHom : Mathlib.Tactic.BicategoryLike.Normalize.Result → Mathlib.Tactic.BicategoryLike.NormalizedHom
-- Mathlib.Algebra.Lie.Subalgebra
/-- `lieSpan` forms a Galois insertion with the coercion from `LieSubalgebra` to `Set`.  -/
LieSubalgebra.gi : (R : Type u) →
  (L : Type v) →
    [inst : CommRing R] →
      [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → GaloisInsertion (LieSubalgebra.lieSpan R L) SetLike.coe
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.card_support_eq_zero : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {f : Equiv.Perm α}, f.support.card = 0 ↔ f = 1
-- Init.Grind.AC
Lean.Grind.AC.Context.mk.injEq : ∀ {α : Sort u} (vars : Lean.RArray (PLift α)) (op : α → α → α) (vars_1 : Lean.RArray (PLift α)) (op_1 : α → α → α),
  ({ vars := vars, op := op } = { vars := vars_1, op := op_1 }) = (vars = vars_1 ∧ op = op_1)
-- Mathlib.Algebra.GroupWithZero.WithZero
/-- Any group with zero is isomorphic to adjoining `0` to the units of itself.  -/
WithZero.withZeroUnitsEquiv : {G : Type u_4} → [inst : GroupWithZero G] → [DecidablePred fun a => a = 0] → WithZero Gˣ ≃* G
-- Mathlib.Order.Filter.Cofinite
Filter.Tendsto.exists_within_forall_le : ∀ {α : Type u_4} {β : Type u_5} [inst : LinearOrder β] {s : Set α},
  s.Nonempty → ∀ {f : α → β}, Filter.Tendsto f Filter.cofinite Filter.atTop → ∃ a₀ ∈ s, ∀ a ∈ s, f a₀ ≤ f a
-- Mathlib.Topology.GDelta.Basic
/-- A nowhere dense set `s` is contained in a closed nowhere dense set (namely, its closure).  -/
IsNowhereDense.subset_of_closed_isNowhereDense : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsNowhereDense s → ∃ t, s ⊆ t ∧ IsNowhereDense t ∧ IsClosed t
-- Mathlib.Combinatorics.Matroid.IndepAxioms
IndepMatroid.mk : {α : Type u_2} →
  (E : Set α) →
    (Indep : Set α → Prop) →
      Indep ∅ →
        (∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I) →
          (∀ ⦃I B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)) →
            (∀ X ⊆ E, Matroid.ExistsMaximalSubsetProperty Indep X) → (∀ (I : Set α), Indep I → I ⊆ E) → IndepMatroid α
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Hom.resLE_preimage : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {U : Y.Opens} {V : X.Opens}
  (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) (O : (↑U).Opens),
  (TopologicalSpace.Opens.map (AlgebraicGeometry.Scheme.Hom.resLE f U V e).base).obj O =
    (TopologicalSpace.Opens.map V.ι.base).obj
      ((TopologicalSpace.Opens.map f.base).obj ((AlgebraicGeometry.Scheme.Hom.opensFunctor U.ι).obj O))
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast!_eq_default : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l : List ((a : α) × β a)} {a : α}
  [inst_2 : Inhabited (β a)], Std.Internal.List.containsKey a l = false → Std.Internal.List.getValueCast! a l = default
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.FiniteElement.val_zero : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K], ↑0 = 0
-- Lean.Elab.Command
Lean.Elab.Command.elabCommand : Lean.Syntax → Lean.Elab.Command.CommandElabM Unit
-- Mathlib.Algebra.Module.SpanRank
Submodule.spanRank_bot : ∀ {R : Type u_1} [inst : Semiring R], Submodule.spanRank ⊥ = 0
-- Mathlib.LinearAlgebra.QuadraticForm.Isometry
QuadraticMap.Isometry.mk.injEq : ∀ {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} {N : Type u_7} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid N] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} (toLinearMap : M₁ →ₗ[R] M₂)
  (map_app' : ∀ (m : M₁), Q₂ (toLinearMap.toFun m) = Q₁ m) (toLinearMap_1 : M₁ →ₗ[R] M₂)
  (map_app'_1 : ∀ (m : M₁), Q₂ (toLinearMap_1.toFun m) = Q₁ m),
  ({ toLinearMap := toLinearMap, map_app' := map_app' } = { toLinearMap := toLinearMap_1, map_app' := map_app'_1 }) =
    (toLinearMap = toLinearMap_1)