mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.mem_alter!_of_not_compare_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF →
    ∀ {k k' : α} {f : Option (β k) → Option (β k)},
      ¬compare k k' = Ordering.eq → (k' ∈ Std.DTreeMap.Internal.Impl.alter! k f t ↔ k' ∈ t)
-- Mathlib.FieldTheory.IsAlgClosed.Basic
IsAlgClosed.card_roots_map_eq_natDegree_from_simpleRing : ∀ {A : Type u_1} {B : Type u_2} [inst : Ring A] [IsSimpleRing A] [inst_2 : Field B] [IsAlgClosed B] (f : A →+* B)
  (p : Polynomial A), (Polynomial.map f p).roots.card = p.natDegree
-- Mathlib.LinearAlgebra.LinearIndependent.Basic
LinearIndepOn.comp_of_image : ∀ {ι : Type u'} {ι' : Type u_1} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] {s : Set ι'} {f : ι' → ι},
  LinearIndepOn R v (f '' s) → Set.InjOn f s → LinearIndepOn R (v ∘ f) s
-- Mathlib.Topology.Algebra.InfiniteSum.Group
Summable.sub : ∀ {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [inst : AddCommGroup α] [inst_1 : TopologicalSpace α]
  [IsTopologicalAddGroup α] {f g : β → α}, Summable f L → Summable g L → Summable (fun b => f b - g b) L
-- Lean.Attributes
Lean.Attribute.Builtin.getIdent? : Lean.Syntax → Lean.AttrM (Option Lean.Syntax)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getD_insertIfNew! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF →
    ∀ {k a : α} {fallback : β a} {v : β k},
      (Std.DTreeMap.Internal.Impl.insertIfNew! k v t).getD a fallback =
        if h : compare k a = Ordering.eq ∧ k ∉ t then cast ⋯ v else t.getD a fallback
-- Mathlib.Analysis.Normed.Field.Basic
nnnorm_zpow : ∀ {α : Type u_2} [inst : NormedDivisionRing α] (a : α) (n : ℤ), ‖a ^ n‖₊ = ‖a‖₊ ^ n
-- Mathlib.Algebra.Polynomial.Smeval
Polynomial.smeval_mul : ∀ (R : Type u_1) [inst : Semiring R] (p q : Polynomial R) {S : Type u_2} [inst_1 : NonAssocSemiring S]
  [inst_2 : Module R S] [inst_3 : Pow S ℕ] (x : S) [NatPowAssoc S] [IsScalarTower R S S] [SMulCommClass R S S],
  (p * q).smeval x = p.smeval x * q.smeval x
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.minD_le_of_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α},
  t.contains k = true → ∀ {fallback : α}, (cmp (t.minD fallback) k).isLE = true
-- Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
MeasureTheory.lpNorm_smul_measure_of_ne_top : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E],
  p ≠ ⊤ → ∀ {f : α → E} (c : NNReal), MeasureTheory.lpNorm f p (c • μ) = c ^ p.toReal⁻¹ • MeasureTheory.lpNorm f p μ
-- Mathlib.Combinatorics.SimpleGraph.Ends.Properties
/-- The `componentCompl`s chosen by an end are all infinite.  -/
SimpleGraph.end_componentCompl_infinite : ∀ {V : Type} (G : SimpleGraph V) (e : ↑G.end) (K : (Finset V)ᵒᵖ), (SimpleGraph.ComponentCompl.supp (↑e K)).Infinite
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.opow_le_of_isSuccLimit : ∀ {a b c : Ordinal.{u_1}}, a ≠ 0 → Order.IsSuccLimit b → (a ^ b ≤ c ↔ ∀ b' < b, a ^ b' ≤ c)
-- Mathlib.Algebra.Group.Fin.Tuple
Matrix.smul_empty : ∀ {α : Type u_1} {M : Type u_2} [inst : SMul M α] (x : M) (v : Fin 0 → α), x • v = ![]
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.map_sub : ∀ {R : Type u} [inst : Ring R] {p q : Polynomial R} {S : Type u_1} [inst_1 : Ring S] (f : R →+* S),
  Polynomial.map f (p - q) = Polynomial.map f p - Polynomial.map f q
-- Mathlib.Algebra.Module.Lattice
Submodule.IsLattice.of_le_of_isLattice_of_fg : ∀ {R : Type u_1} [inst : CommRing R] (A : Type u_2) [inst_1 : CommRing A] [inst_2 : Algebra R A] {V : Type u_3}
  [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : Module A V] [inst_6 : IsScalarTower R A V]
  {M N : Submodule R V}, M ≤ N → ∀ [Submodule.IsLattice A M], N.FG → Submodule.IsLattice A N
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.associated_apply : ∀ (S : Type u_1) {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] [inst_5 : CommSemiring S] [inst_6 : Algebra S R]
  [inst_7 : Module S N] [inst_8 : IsScalarTower S R N] [inst_9 : Invertible 2] (Q : QuadraticMap R M N) (x y : M),
  (((QuadraticMap.associatedHom S) Q) x) y = ⅟2 • (Q (x + y) - Q x - Q y)
-- Mathlib.Computability.Partrec
Nat.rfindOpt_dom : ∀ {α : Type u_1} {f : ℕ → Option α}, (Nat.rfindOpt f).Dom ↔ ∃ n a, a ∈ f n
-- Mathlib.CategoryTheory.Monoidal.Cartesian.ShrinkYoneda
CategoryTheory.instSmallCarrierObjOppositeMonCatMonFunctorYonedaMon : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] (M : CategoryTheory.Mon C) (X : Cᵒᵖ),
  Small.{w, v} ↑((CategoryTheory.yonedaMon.obj M).obj X)
-- Mathlib.Data.List.Nodup
/-- **Alias** of the reverse direction of `List.nodup_attach`. -/
List.Nodup.attach : ∀ {α : Type u} {l : List α}, l.Nodup → l.attach.Nodup
-- Mathlib.Data.Nat.Pairing
iSup_unpair : ∀ {α : Type u_1} [inst : CompleteLattice α] (f : ℕ → ℕ → α), ⨆ n, f (Nat.unpair n).1 (Nat.unpair n).2 = ⨆ i, ⨆ j, f i j
-- Mathlib.RingTheory.Polynomial.Pochhammer
_private.Mathlib.RingTheory.Polynomial.Pochhammer.0.ascPochhammer.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Lean.DocString.Syntax
Lean.Doc.Syntax.inline.quot : Lean.ParserDescr
-- Mathlib.Order.Partition.Finpartition
/-- The `sup` of a sup-bot-preserving map `f` over the parts of a `Finpartition` equals `f a`.  -/
Finpartition.sup_parts_apply : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] {a : α} (P : Finpartition a) {β : Type u_2} {f : α → β}
  [inst_2 : SemilatticeSup β] [inst_3 : OrderBot β],
  (∀ (x y : α), f (x ⊔ y) = f x ⊔ f y) → f ⊥ = ⊥ → P.parts.sup f = f a
-- Mathlib.Algebra.Group.Pi.Lemmas
Sigma.curry_single : ∀ {α : Type u_5} {β : α → Type u_6} {γ : (a : α) → β a → Type u_7} [inst : DecidableEq α]
  [inst_1 : (a : α) → DecidableEq (β a)] [inst_2 : (a : α) → (b : β a) → Zero (γ a b)] (i : (a : α) × β a)
  (x : γ i.fst i.snd), Sigma.curry (Pi.single i x) = Pi.single i.fst (Pi.single i.snd x)
-- Mathlib.MeasureTheory.OuterMeasure.BorelCantelli
MeasureTheory.liminf_ae_eq_of_forall_ae_eq : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [inst_1 : MeasureTheory.OuterMeasureClass F α]
  {μ : F} (s : ℕ → Set α) {t : Set α}, (∀ (n : ℕ), s n =ᵐ[μ] t) → Filter.liminf s Filter.atTop =ᵐ[μ] t
-- Mathlib.Data.Holor
Holor.CPRankMax1.below : {α : Type} →
  [inst : Mul α] →
    {motive : {ds : List ℕ} → (a : Holor α ds) → a.CPRankMax1 → Prop} →
      {ds : List ℕ} → {a : Holor α ds} → a.CPRankMax1 → Prop
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.MemLp.toLp.congr_simp : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] (f f_1 : α → E) (e_f : f = f_1) (h_mem_ℒp : MeasureTheory.MemLp f p μ),
  MeasureTheory.MemLp.toLp f h_mem_ℒp = MeasureTheory.MemLp.toLp f_1 ⋯
-- Mathlib.RingTheory.HahnSeries.Lex
HahnSeries.leadingCoeff_nonneg_iff : ∀ {Γ : Type u_1} {R : Type u_2} [inst : LinearOrder Γ] [inst_1 : Zero R] [inst_2 : LinearOrder R]
  {x : Lex (HahnSeries Γ R)}, 0 ≤ (ofLex x).leadingCoeff ↔ 0 ≤ x
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get!_erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t.WF →
    ∀ {k a : α} [inst_1 : Inhabited (β a)], (t.erase k).get! a = if cmp k a = Ordering.eq then default else t.get! a
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonCompletionItemTag : Lean.ToJson Lean.Lsp.CompletionItemTag
-- Lean.Meta.Sym.AlphaShareCommon
Lean.Meta.Sym.AlphaShareCommon.Context.mk : Lean.Environment → Bool → Bool → Lean.Meta.Sym.AlphaShareCommon.Context
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.pullbackCone_fst_φ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : CategoryTheory.Limits.FormalCoproduct C} (f : X ⟶ Z)
  (g : Y ⟶ Z)
  (pb :
    (i : Function.Pullback f.f g.f) →
      CategoryTheory.Limits.PullbackCone (CategoryTheory.CategoryStruct.comp (f.φ (↑i).1) (CategoryTheory.eqToHom ⋯))
        (g.φ (↑i).2))
  (i : (CategoryTheory.Limits.FormalCoproduct.pullbackCone f g pb).pt.I),
  (CategoryTheory.Limits.FormalCoproduct.pullbackCone f g pb).fst.φ i = (pb i).fst
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.single_boxes : ∀ {ι : Type u_1} (I J : BoxIntegral.Box ι) (h : J ≤ I), (BoxIntegral.Prepartition.single I J h).boxes = {J}
-- Mathlib.Topology.Connected.LocallyPathConnected
/-- **Alias** of `LocallyPathConnectedSpace.of_bases`. -/
LocPathConnectedSpace.of_bases : ∀ {X : Type u_1} [inst : TopologicalSpace X] {ι : Type u_3} {p : X → ι → Prop} {s : X → ι → Set X},
  (∀ (x : X), (nhds x).HasBasis (p x) (s x)) →
    (∀ (x : X) (i : ι), p x i → IsPathConnected (s x i)) → LocallyPathConnectedSpace X
-- Mathlib.Algebra.Algebra.Hom
AlgHom.toLinearMap_id : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
  (AlgHom.id R A).toLinearMap = LinearMap.id
-- Mathlib.LinearAlgebra.Dimension.RankNullity
Submodule.exists_of_finrank_lt : ∀ {R : Type u_1} {M : Type u} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [HasRankNullity.{u, u_1} R] [StrongRankCondition R] [Module.Finite R M] (N : Submodule R M),
  Module.finrank R ↥N < Module.finrank R M → ∃ m, ∀ (r : R), r ≠ 0 → r • m ∉ N
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.T_zero : ∀ (R : Type u_1) [inst : CommRing R], Polynomial.Chebyshev.T R 0 = 1
-- Init.Data.String.Substring
Substring.Raw.Internal.getImpl : Substring.Raw → String.Pos.Raw → Char
-- Mathlib.Algebra.Module.Submodule.Map
/-- A linear map between two modules restricts to a linear map from any submodule p of the
domain onto the image of that submodule.

This is the linear version of `AddMonoidHom.addSubmonoidMap` and `AddMonoidHom.addSubgroupMap`.

TODO: Consider making this an `abbrev`, dropping its API, and renaming to something like
`restrictSubmodule`.  -/
LinearMap.submoduleMap : {R : Type u_1} →
  {R₂ : Type u_3} →
    {M : Type u_5} →
      {M₂ : Type u_7} →
        [inst : Semiring R] →
          [inst_1 : Semiring R₂] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommMonoid M₂] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R₂ M₂] →
                    {σ₁₂ : R →+* R₂} →
                      [inst_6 : RingHomSurjective σ₁₂] →
                        (f : M →ₛₗ[σ₁₂] M₂) → (p : Submodule R M) → ↥p →ₛₗ[σ₁₂] ↥(Submodule.map f p)
-- Mathlib.Topology.Order.Category.AlexDisc
alexDiscEquivPreord_counitIso : alexDiscEquivPreord.counitIso =
  CategoryTheory.NatIso.ofComponents (fun X => Preord.Iso.mk (id (orderIsoSpecializationWithUpperSetTopology ↑X).symm))
    @alexDiscEquivPreord._proof_4
-- Mathlib.Algebra.MonoidAlgebra.Module
/-- If the image of an element `m : M` in `R[M]` belongs to the submodule generated by the
closure of some `s : Set M` then `m ∈ closure s`.  -/
MonoidAlgebra.mem_closure_of_mem_span_closure : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : MulOneClass M] {s : Set M} {m : M} [Nontrivial R],
  (MonoidAlgebra.of R M) m ∈ Submodule.span R ↑(Submonoid.closure (⇑(MonoidAlgebra.of R M) '' s)) →
    m ∈ Submonoid.closure s
-- Lean.Meta.RecursorInfo
Lean.Meta.RecursorInfo.motivePos : Lean.Meta.RecursorInfo → ℕ
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.testAgainstNN_const : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω)
  (c : NNReal), μ.testAgainstNN (BoundedContinuousFunction.const Ω c) = c * μ.mass
-- Mathlib.RingTheory.LocalRing.MaximalIdeal.Square
IsLocalRing.maximalIdeal_sq_lt : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsLocalRing R] [IsNoetherianRing R],
  0 < ringKrullDim R → IsLocalRing.maximalIdeal R ^ 2 < IsLocalRing.maximalIdeal R
-- Std.Data.DTreeMap.Raw.Basic
/-- Tries to retrieve the smallest key that is greater than the given key,
returning `none` if no such key exists.
 -/
Std.DTreeMap.Raw.getKeyGT? : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap.Raw α β cmp → α → Option α
-- Mathlib.CategoryTheory.Presentable.ColimitPresentation
/-- Morphisms in the `Total` category.  -/
CategoryTheory.Limits.ColimitPresentation.Total.Hom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type u_1} →
      {I : J → Type u_2} →
        [inst_1 : CategoryTheory.Category.{v_1, u_1} J] →
          [inst_2 : (j : J) → CategoryTheory.Category.{u_3, u_2} (I j)] →
            {D : CategoryTheory.Functor J C} →
              {P : (j : J) → CategoryTheory.Limits.ColimitPresentation (I j) (D.obj j)} →
                CategoryTheory.Limits.ColimitPresentation.Total P →
                  CategoryTheory.Limits.ColimitPresentation.Total P → Type (max v v_1)
-- Mathlib.GroupTheory.OrderOfElement
IsOfFinOrder.mem_powers_iff_mem_range_orderOf : ∀ {G : Type u_1} [inst : Monoid G] {x y : G} [inst_1 : DecidableEq G],
  IsOfFinOrder x → (y ∈ Submonoid.powers x ↔ y ∈ Finset.image (fun x_1 => x ^ x_1) (Finset.range (orderOf x)))
-- Mathlib.Order.Filter.Ultrafilter.Defs
Ultrafilter.eq_of_le : ∀ {α : Type u} {f g : Ultrafilter α}, ↑f ≤ ↑g → f = g
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop.0.Std.IterM.DefaultConsumers.forIn'.match_1.eq_1 : ∀ {β : Type u_3} (γ : Type u_1) (PlausibleForInStep : β → γ → ForInStep γ → Prop) (acc : γ) (out : β)
  (motive : Subtype (PlausibleForInStep out acc) → Sort u_2) (c : γ)
  (h' : PlausibleForInStep out acc (ForInStep.yield c))
  (h_1 : (c : γ) → (h' : PlausibleForInStep out acc (ForInStep.yield c)) → motive ⟨ForInStep.yield c, h'⟩)
  (h_2 : (c : γ) → (h : PlausibleForInStep out acc (ForInStep.done c)) → motive ⟨ForInStep.done c, h⟩),
  (match ⟨ForInStep.yield c, h'⟩ with
    | ⟨ForInStep.yield c, h'⟩ => h_1 c h'
    | ⟨ForInStep.done c, h⟩ => h_2 c h) =
    h_1 c h'
-- Std.Time.Time.Unit.Hour
Std.Time.Hour.instInhabitedOrdinal : Inhabited Std.Time.Hour.Ordinal
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.injective_pointReflection_left_of_injective_two_nsmul : ∀ (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁],
  (Function.Injective fun x => 2 • x) → ∀ (y : P₁), Function.Injective fun x => (AffineEquiv.pointReflection k x) y
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isSome_minKey?_of_isSome_minKey?_erase! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {k : α}, (Std.DTreeMap.Internal.Impl.erase! k t).minKey?.isSome = true → t.minKey?.isSome = true
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Multiset.sum_map_sum : ∀ {ι : Type u_1} {M : Type u_4} {α : Type u_5} [inst : AddCommMonoid M] {m : Multiset ι} {s : Finset α} {f : ι → α → M},
  (Multiset.map (fun i => ∑ a ∈ s, f i a) m).sum = ∑ a ∈ s, (Multiset.map (fun i => f i a) m).sum
-- Init.Meta.Defs
/-- Syntax that represents a tactic.
 -/
Lean.Syntax.Tactic : Type
-- Mathlib.Algebra.Group.Subgroup.Ker
Subgroup.map_le_map_iff' : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {f : G →* N} {H K : Subgroup G},
  Subgroup.map f H ≤ Subgroup.map f K ↔ H ⊔ f.ker ≤ K ⊔ f.ker
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.sum_single_add_single : ∀ {ι : Type u_2} {A : Type u_4} {B : Type u_5} [inst : AddCommMonoid A] [inst_1 : AddCommMonoid B] (f₁ f₂ : ι)
  (g₁ g₂ : A) (F : ι → A → B),
  f₁ ≠ f₂ → (∀ (f : ι), F f 0 = 0) → ((fun₀ | f₁ => g₁) + fun₀ | f₂ => g₂).sum F = F f₁ g₁ + F f₂ g₂
-- Mathlib.Order.Filter.Lift
Filter.le_lift' : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {h : Set α → Set β} {g : Filter β}, g ≤ f.lift' h ↔ ∀ s ∈ f, h s ∈ g
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.distinct_keys_toList : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → List.Pairwise (fun a b => (a.1 == b.1) = false) m.toList
-- Mathlib.Topology.Algebra.Nonarchimedean.TotallyDisconnected
NonarchimedeanAddGroup.exists_openAddSubgroup_separating : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [NonarchimedeanAddGroup G] [T2Space G] {a b : G},
  a ≠ b → ∃ V, Disjoint (a +ᵥ ↑V) (b +ᵥ ↑V)
-- Mathlib.AlgebraicGeometry.Sites.QuasiCompact
AlgebraicGeometry.Scheme.presieve₀_mem_qcPrecoverage_iff : ∀ {S : AlgebraicGeometry.Scheme} {E : CategoryTheory.PreZeroHypercover S},
  E.presieve₀ ∈ AlgebraicGeometry.Scheme.qcPrecoverage.coverings S ↔ AlgebraicGeometry.QuasiCompactCover E
-- Mathlib.CategoryTheory.Abelian.Projective.Resolution
CategoryTheory.ProjectiveResolution.instProjectiveXNatOfComplex : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.EnoughProjectives C] (Z : C) (n : ℕ),
  CategoryTheory.Projective ((CategoryTheory.ProjectiveResolution.ofComplex Z).X n)
-- Mathlib.RingTheory.DividedPowers.Basic
DividedPowers.dpow_mul_right : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} {a b : A} (hI : DividedPowers I) {n : ℕ},
  a ∈ I → hI.dpow n (a * b) = hI.dpow n a * b ^ n
-- Mathlib.Algebra.Group.Action.Equidecomp
Equidecomp.restr_refl_symm : ∀ {X : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : MulAction G X] (A : Set X),
  ((Equidecomp.refl X G).restr A).symm = (Equidecomp.refl X G).restr A
-- Mathlib.Data.Finset.Sum
Finset.toLeft_subset_toLeft : ∀ {α : Type u_1} {β : Type u_2} {u v : Finset (α ⊕ β)}, u ⊆ v → u.toLeft ⊆ v.toLeft
-- Init.Data.Nat.Div.Basic
Nat.sub_mod_add_mod_cancel : ∀ (a b : ℕ) [NeZero a], a - b % a + b % a = a
-- Init.Data.UInt.Lemmas
UInt16.le_of_lt : ∀ {a b : UInt16}, a < b → a ≤ b
-- Mathlib.Topology.Order.MonotoneContinuity
/-- If `f` is a monotone function on a neighborhood of `a` and the image of this neighborhood under
`f` meets every interval `(b, f a)`, `b < f a`, and every interval `(f a, b)`, `b > f a`, then `f`
is continuous at `a`.  -/
continuousAt_of_monotoneOn_of_exists_between : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : LinearOrder β] [inst_4 : TopologicalSpace β] [OrderTopology β] {f : α → β} {s : Set α} {a : α},
  MonotoneOn f s →
    s ∈ nhds a →
      (∀ b < f a, ∃ c ∈ s, f c ∈ Set.Ioo b (f a)) → (∀ b > f a, ∃ c ∈ s, f c ∈ Set.Ioo (f a) b) → ContinuousAt f a
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupNorm.mk.sizeOf_spec : ∀ {G : Type u_6} [inst : Group G] [inst_1 : SizeOf G] (toGroupSeminorm : GroupSeminorm G)
  (eq_one_of_map_eq_zero' : ∀ (x : G), toGroupSeminorm.toFun x = 0 → x = 1),
  sizeOf { toGroupSeminorm := toGroupSeminorm, eq_one_of_map_eq_zero' := eq_one_of_map_eq_zero' } =
    1 + sizeOf toGroupSeminorm
-- Mathlib.Analysis.Normed.Lp.lpSpace
/-- `ℓ⁰(ι, E)` is the space of finitely supported functions `ι → E`. In general, this should not
be used outside of the context of `ℓ^p(ι, E)` spaces, and one should instead prefer `Finsupp`
in other situations.  -/
lp.«termℓ⁰(_,_)» : Lean.ParserDescr
-- Init.Prelude
instLEUInt8 : LE UInt8
-- Mathlib.MeasureTheory.Measure.Hausdorff
MeasureTheory.Measure.le_hausdorffMeasure : ∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X] (d : ℝ)
  (μ : MeasureTheory.Measure X) (ε : ENNReal),
  0 < ε → (∀ (s : Set X), Metric.ediam s ≤ ε → μ s ≤ Metric.ediam s ^ d) → μ ≤ MeasureTheory.Measure.hausdorffMeasure d
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
/-- If a family of vectors spans `M`, then the family of its `n`-fold exterior products spans
`⋀[R]^n M`. Here we work in the exterior algebra.  -/
exteriorPower.ιMulti_family_span_fixedDegree_of_span : ∀ (R : Type u) [inst : CommRing R] {n : ℕ} {M : Type u_1} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {I : Type u_4}
  [inst_3 : LinearOrder I] {v : I → M},
  Submodule.span R (Set.range v) = ⊤ → Submodule.span R (Set.range (ExteriorAlgebra.ιMulti_family R n v)) = ⋀[R]^n M
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.fixedIndicesToParams.go.eq_def : ∀ (masks : List (Array Bool)) (mask : Array Bool) (i : ℕ) (type : Lean.Expr) (typesToCheck : List Lean.Expr),
  Lean.Elab.Command.fixedIndicesToParams.go✝ masks mask i type typesToCheck =
    if i < mask.size then
      if (!masks.all fun mask => decide (i < mask.size) && mask[i]!) = true then pure i
      else
        if (!type.isForall) = true then pure i
        else
          have paramType := type.bindingDomain!;
          do
          let __do_lift ← List.allM (fun type => Lean.Elab.Command.isDomainDefEq✝ type paramType) typesToCheck
          if (!__do_lift) = true then
              have cls := `Elab.inductive;
              do
              let __do_lift ← Lean.isTracingEnabledFor cls
              have __do_jp : Unit → Lean.MetaM ℕ := fun __r => pure i
              if __do_lift = true then do
                  let __r ←
                    Lean.addTrace cls
                        (Lean.toMessageData "domain not def eq: " ++ Lean.toMessageData i ++ Lean.toMessageData ", " ++
                              Lean.toMessageData type ++
                            Lean.toMessageData " =?= " ++
                          Lean.toMessageData paramType)
                  __do_jp __r
                else __do_jp ()
            else
              Lean.Meta.withLocalDeclD `a paramType fun paramNew => do
                let typesToCheck ←
                  List.mapM (fun type => Lean.Meta.whnfD (type.bindingBody!.instantiate1 paramNew)) typesToCheck
                Lean.Elab.Command.fixedIndicesToParams.go✝ masks mask (i + 1) (type.bindingBody!.instantiate1 paramNew)
                    typesToCheck
    else pure i
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.vadd_sInter_subset : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] (s : Set α) (T : Set (Set β)), s +ᵥ ⋂₀ T ⊆ ⋂ t ∈ T, s +ᵥ t
-- Std.Data.HashSet.Lemmas
Std.HashSet.get!_ofList_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] [inst : Inhabited α] {l : List α} {k : α},
  l.contains k = false → (Std.HashSet.ofList l).get! k = default
-- Lean.Data.PersistentHashSet
Lean.PersistentHashSet.instForInOfMonad : {α : Type u_1} →
  {m : Type u_2 → Type u_3} → {x : BEq α} → {x_1 : Hashable α} → [Monad m] → ForIn m (Lean.PersistentHashSet α) α
-- Mathlib.GroupTheory.GroupAction.Hom
/-- The proposition that the function preserves addition  -/
DistribMulActionHom.map_add' : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} {A : Type u_10}
  [inst_2 : AddMonoid A] [inst_3 : DistribMulAction M A] {B : Type u_11} [inst_4 : AddMonoid B]
  [inst_5 : DistribMulAction N B] (self : A →ₑ+[φ] B) (x y : A), self.toFun (x + y) = self.toFun x + self.toFun y
-- Std.Time.Format
Std.Time.DateTime.instToString : ToString Std.Time.DateTime
-- Lean.Elab.Tactic.Try
/-- Check if a config contains `+suggestions` or `+locals`  -/
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.configHasSuggestionsOrLocals : Lean.TSyntax `Lean.Parser.Tactic.optConfig → Bool