mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.closure_loops : ∀ {α : Type u_1} (M : Matroid α), M.closure M.loops = M.loops
-- Lean.DocString.Types
Lean.Doc.Block.dl.inj : ∀ {i : Type u} {b : Type v} {items items_1 : Array (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b))},
  Lean.Doc.Block.dl items = Lean.Doc.Block.dl items_1 → items = items_1
-- Mathlib.Algebra.Ring.Periodic
Function.Periodic.sub_nsmul_eq : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c x : α} [inst : AddGroup α],
  Function.Periodic f c → ∀ (n : ℕ), f (x - n • c) = f x
-- Mathlib.Analysis.Fourier.AddCircle
fourierCoeff_toLp : ∀ {T : ℝ} [hT : Fact (0 < T)] (f : C(AddCircle T, ℂ)) (n : ℤ),
  fourierCoeff (↑↑((ContinuousMap.toLp 2 AddCircle.haarAddCircle ℂ) f)) n = fourierCoeff (⇑f) n
-- Mathlib.Data.Int.Interval
Int.card_fintype_Ioo_of_lt : ∀ (a b : ℤ), a < b → ↑(Fintype.card ↑(Set.Ioo a b)) = b - a - 1
-- Mathlib.Analysis.Convex.Combination
convexHull_pi : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} [Finite ι] [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜]
  [IsStrictOrderedRing 𝕜] [inst_3 : (i : ι) → AddCommGroup (E i)] [inst_4 : (i : ι) → Module 𝕜 (E i)] (s : Set ι)
  (t : (i : ι) → Set (E i)), (convexHull 𝕜) (s.pi t) = s.pi fun i => (convexHull 𝕜) (t i)
-- Mathlib.Topology.PartitionOfUnity
/-- the functions sum up to one on `s`  -/
PartitionOfUnity.sum_eq_one' : ∀ {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {s : optParam (Set X) Set.univ}
  (self : PartitionOfUnity ι X s), ∀ x ∈ s, ∑ᶠ (i : ι), (self.toFun i) x = 1
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
mfderiv_comp_mfderivWithin_of_eq : ∀ {𝕜 : 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'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {E'' : Type u_8}
  [inst_11 : NormedAddCommGroup E''] [inst_12 : NormedSpace 𝕜 E''] {H'' : Type u_9} [inst_13 : TopologicalSpace H'']
  {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [inst_14 : TopologicalSpace M''] [inst_15 : ChartedSpace H'' M'']
  {f : M → M'} {s : Set M} {g : M' → M''} {x : M} {y : M'},
  MDiffAt g y → MDiffAt[s] f x → UniqueMDiffAt[s] x → f x = y → mfderiv[s] (g ∘ f) x = mfderiv% g y ∘SL mfderiv[s] f x
-- Mathlib.Analysis.Complex.Polynomial.Basic
/-- An irreducible real polynomial has degree at most two.  -/
Irreducible.degree_le_two : ∀ {p : Polynomial ℝ}, Irreducible p → p.degree ≤ 2
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.all_eq_not_any_not : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_2 : Monad m]
  [LawfulMonad m] [inst_4 : Std.IteratorLoop α m m] [Std.LawfulIteratorLoop α m m] {it : Std.IterM m β} {p : β → Bool},
  Std.IterM.all p it = (fun x => { down := !x.down }) <$> Std.IterM.any (fun x => !p x) it
-- Mathlib.Algebra.Homology.SpectralObject.Homology
CategoryTheory.Abelian.SpectralObject.instEpiGDCokernelSequence : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.Category.{v_2, u_2} ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {i₀ i₁ i₂ i₃ i₄ i₅ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅) (f₃₄ : i₂ ⟶ i₄)
  (h₃₄ : CategoryTheory.CategoryStruct.comp f₃ f₄ = f₃₄) (n₀ n₁ n₂ n₃ : ℤ) (x : n₀ + 1 = n₁) (x_1 : n₁ + 1 = n₂)
  (x_2 : n₂ + 1 = n₃), CategoryTheory.Epi (X.dCokernelSequence f₁ f₂ f₃ f₄ f₅ f₃₄ h₃₄ n₀ n₁ n₂ n₃ x x_1 x_2).g
-- Std.Data.Iterators.Combinators.Monadic.TakeWhile
Std.Iterators.Types.TakeWhile.mk.sizeOf_spec : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} {P : β → Std.Iterators.PostconditionT m (ULift.{w, 0} Bool)}
  [inst : SizeOf α] [inst_1 : (a : Type w) → SizeOf (m a)] [inst_2 : SizeOf β] (inner : Std.IterM m β),
  sizeOf { inner := inner } = 1 + sizeOf inner
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.isometry_toFun : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (self : α ≃ᵢ β),
  Isometry self.toFun
-- Lean.ReducibilityAttrs
Lean.ReducibilityStatus.implicitReducible.sizeOf_spec : sizeOf Lean.ReducibilityStatus.implicitReducible = 1
-- Mathlib.Topology.Algebra.Group.Matrix
Matrix.SpecialLinearGroup.isEmbedding_mapGL : ∀ {n : Type u_1} {R : Type u_2} {S : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R]
  [inst_3 : TopologicalSpace R] [inst_4 : CommRing S] [inst_5 : TopologicalSpace S] [inst_6 : Algebra R S]
  [IsTopologicalRing S],
  Topology.IsEmbedding ⇑(algebraMap R S) → Topology.IsEmbedding ⇑(Matrix.SpecialLinearGroup.mapGL S)
-- Lean.Meta.Sym.Arith.Types
/-- Arith type classification state, stored as a `SymExtension`.  -/
Lean.Meta.Sym.Arith.State : Type
-- Init.Data.BitVec.Lemmas
BitVec.toInt_neg_of_not_negOverflow : ∀ {w : ℕ} {x : BitVec w}, ¬x.negOverflow = true → (-x).toInt = -x.toInt
-- Lean.Data.Lsp.Ipc
Lean.Lsp.Ipc.expandOutgoingCallHierarchy : ℕ → Lean.Lsp.DocumentUri → Lean.Lsp.Position → Lean.Lsp.Ipc.IpcM (Array Lean.Lsp.Ipc.CallHierarchy × ℕ)
-- Mathlib.Algebra.Group.Subsemigroup.Defs
AddSubsemigroup.coe_bot : ∀ {M : Type u_1} [inst : Add M], ↑⊥ = ∅
-- Mathlib.Algebra.Group.Basic
ne_iff_ne_of_mul_eq_mul : ∀ {α : Type u_1} [inst : CancelCommMonoid α] {a b c d : α}, a * b = c * d → (a ≠ c ↔ b ≠ d)
-- Mathlib.Data.Int.Init
Int.leInductionDown_base : ∀ {m : ℤ} {motive : (n : ℤ) → n ≤ m → Sort u_1} (base : motive m ⋯)
  (pred : (n : ℤ) → (hnm : n ≤ m) → motive n hnm → motive (n - 1) ⋯), Int.leInductionDown base pred m ⋯ = base
-- Mathlib.FieldTheory.Galois.IsGaloisGroup
IsGaloisGroup.fixedPoints_top : ∀ (G : Type u_1) (K : Type u_3) (L : Type u_4) [inst : Group G] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra K L] [inst_4 : MulSemiringAction G L] [hGKL : IsGaloisGroup G K L],
  FixedPoints.intermediateField ↥⊤ = ⊥
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.stalk_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Y)
  [H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] [inst_1 : CategoryTheory.Limits.HasColimits C] (x : ↑↑X),
  CategoryTheory.IsIso (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap f x)
-- Mathlib.Order.Interval.Set.Basic
Set.eq_left_or_mem_Ioo_of_mem_Ico : ∀ {α : Type u_1} [inst : PartialOrder α] {a b x : α}, x ∈ Set.Ico a b → x = a ∨ x ∈ Set.Ioo a b
-- Lean.Level
Lean.instInhabitedLevelMVarId.default : Lean.LevelMVarId
-- Mathlib.Algebra.Category.CommBialgCat
instIsCommMonObjOppositeCommAlgCatOpOfOfIsCocomm : ∀ {R : Type u} [inst : CommRing R] {A : Type u} [inst_1 : CommRing A] [inst_2 : Bialgebra R A] [Coalgebra.IsCocomm R A],
  CategoryTheory.IsCommMonObj (Opposite.op (CommAlgCat.of R A))
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRoot.lift_algebraMap_apply : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRoot S f) {T : Type u_1} [inst_3 : CommRing T] {x : T} [inst_4 : Algebra R T]
  (hx' : (Polynomial.aeval x) f = 0) (z : S), (h.lift (algebraMap R T) x hx') z = (h.liftHom x hx') z
-- Mathlib.Algebra.Ring.GeomSum
one_sub_dvd_one_sub_pow : ∀ {R : Type u_1} [inst : Ring R] (x : R) (n : ℕ), 1 - x ∣ 1 - x ^ n
-- Mathlib.Order.Filter.SmallSets
Filter.bind_smallSets_gc : ∀ {α : Type u_1}, GaloisConnection (fun L => L.bind Filter.principal) Filter.smallSets
-- Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension
/-- **Alias** of `ModuleCat.projectiveDimension_eq_of_linearEquiv`. -/
CategoryTheory.projectiveDimension_eq_of_linearEquiv : ∀ {R : Type u} [inst : Ring R] [Small.{v, u} R] [Small.{v', u} R] {M : ModuleCat R} {N : ModuleCat R} (e : ↑M ≃ₗ[R] ↑N),
  CategoryTheory.projectiveDimension M = CategoryTheory.projectiveDimension N
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.coe_mapCoeffs : ∀ {ι : Type u_10} {R : Type u_11} {M : Type u_12} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (b : Module.Basis ι R M) {R' : Type u_13} [inst_3 : Semiring R'] [inst_4 : Module R' M] (f : R ≃+* R')
  (h : ∀ (c : R) (x : M), f c • x = c • x), ⇑(b.mapCoeffs f h) = ⇑b
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.rTensor_add : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [inst : CommSemiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : AddCommMonoid U] [inst_5 : Module A V]
  [inst_6 : Module A W] [inst_7 : Module A U] {ρ : Representation A G V} {σ : Representation A G W}
  {τ : Representation A G U} (f₁ f₂ : σ.IntertwiningMap τ),
  Representation.IntertwiningMap.rTensor ρ (f₁ + f₂) =
    Representation.IntertwiningMap.rTensor ρ f₁ + Representation.IntertwiningMap.rTensor ρ f₂
-- Mathlib.RingTheory.Polynomial.Wronskian
/-- For coprime polynomials `a` and `b`, their Wronskian is zero
if and only if their derivatives are zeros.
 -/
IsCoprime.wronskian_eq_zero_iff : ∀ {R : Type u_1} [inst : CommRing R] [NoZeroDivisors R] {a b : Polynomial R},
  IsCoprime a b → (a.wronskian b = 0 ↔ Polynomial.derivative a = 0 ∧ Polynomial.derivative b = 0)
-- Mathlib.Analysis.Normed.Group.Defs
SeminormedCommGroup.toSeminormedGroup : {E : Type u_5} → [SeminormedCommGroup E] → SeminormedGroup E
-- Mathlib.CategoryTheory.IsConnected
CategoryTheory.isConnected_of_nonempty_and_subsingleton : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] [Nonempty J] [Subsingleton J], CategoryTheory.IsConnected J
-- Mathlib.NumberTheory.Cyclotomic.Basic
/-- If `(⊥ : SubAlgebra A B) = ⊤`, then `IsCyclotomicExtension {0} A B`.  -/
IsCyclotomicExtension.singleton_zero_of_bot_eq_top : ∀ {A : Type u} {B : Type v} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B],
  ⊥ = ⊤ → IsCyclotomicExtension {0} A B
-- Lean.Server.GoTo
Lean.Server.locationLinksFromImport : Lean.Elab.CommandInfo → Lean.Server.GoToM (Array Lean.Lsp.LeanLocationLink)
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.DiagramOfCocones.mk : {J : Type u_1} →
  {K : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} K] →
        {C : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
            {F : CategoryTheory.Functor J (CategoryTheory.Functor K C)} →
              (obj : (j : J) → CategoryTheory.Limits.Cocone (F.obj j)) →
                (map :
                    {j j' : J} →
                      (f : j ⟶ j') → obj j ⟶ (CategoryTheory.Limits.Cocone.precompose (F.map f)).obj (obj j')) →
                  autoParam
                      (∀ (j : J),
                        (map (CategoryTheory.CategoryStruct.id j)).hom = CategoryTheory.CategoryStruct.id (obj j).pt)
                      CategoryTheory.Limits.DiagramOfCocones.id._autoParam →
                    autoParam
                        (∀ {j₁ j₂ j₃ : J} (f : j₁ ⟶ j₂) (g : j₂ ⟶ j₃),
                          (map (CategoryTheory.CategoryStruct.comp f g)).hom =
                            CategoryTheory.CategoryStruct.comp (map f).hom (map g).hom)
                        CategoryTheory.Limits.DiagramOfCocones.comp._autoParam →
                      CategoryTheory.Limits.DiagramOfCocones F
-- Lean.Elab.Tactic.Config
Lean.Elab.Tactic.ConfigItemView.value : Lean.Elab.Tactic.ConfigItemView → Lean.Term
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.NeWord.replaceHead.eq_def : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] (x x_1 : ι) (x_2 : M x) (x_3 : x_2 ≠ 1)
  (x_4 : Monoid.CoprodI.NeWord M x x_1),
  Monoid.CoprodI.NeWord.replaceHead x_2 x_3 x_4 =
    match x, x_1, x_2, x_3, x_4 with
    | x, .(x), x_5, h, Monoid.CoprodI.NeWord.singleton x_6 a => Monoid.CoprodI.NeWord.singleton x_5 h
    | x, x_5, x_6, h, w₁.append hne w₂ => (Monoid.CoprodI.NeWord.replaceHead x_6 h w₁).append hne w₂
-- Mathlib.Algebra.Homology.HomologicalComplex
/-- A constructor for chain maps between `α`-indexed chain complexes built using `ChainComplex.of`,
from a dependently typed collection of morphisms.
 -/
ChainComplex.ofHom : {V : Type u} →
  [inst : CategoryTheory.Category.{v, u} V] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
      {α : Type u_2} →
        [inst_2 : AddRightCancelSemigroup α] →
          [inst_3 : One α] →
            {X Y : ChainComplex V α} →
              (f : (i : α) → X.X i ⟶ Y.X i) →
                (∀ (i : α),
                    CategoryTheory.CategoryStruct.comp (f (i + 1)) (Y.d (i + 1) i) =
                      CategoryTheory.CategoryStruct.comp (X.d (i + 1) i) (f i)) →
                  (X ⟶ Y)
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Subsemigroup.le_op_iff : ∀ {M : Type u_2} [inst : Mul M] {S₁ : Subsemigroup Mᵐᵒᵖ} {S₂ : Subsemigroup M}, S₁ ≤ S₂.op ↔ S₁.unop ≤ S₂
-- Aesop.RuleSet.Member
Aesop.BaseRuleSetMember.normRule : Aesop.NormRule → Aesop.BaseRuleSetMember
-- Batteries.Data.String.Lemmas
String.Legacy.Iterator.ValidFor.of_eq : ∀ {l r : List Char} (it : String.Legacy.Iterator),
  it.s.toList = l.reverseAux r → it.i.byteIdx = String.utf8Len l → String.Legacy.Iterator.ValidFor l r it
-- Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
/-- The limit of `(1 + t/x) ^ x` as `x → ∞` is `exp t` for `t : ℂ`.  -/
Complex.tendsto_one_add_div_cpow_exp : ∀ (t : ℂ), Filter.Tendsto (fun x => (1 + t / ↑x) ^ ↑x) Filter.atTop (nhds (Complex.exp t))
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
Finsupp.linearCombination_comp : ∀ {α : Type u_1} {M : Type u_2} (R : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {α' : Type u_7} {v : α → M} (f : α' → α),
  Finsupp.linearCombination R (v ∘ f) = Finsupp.linearCombination R v ∘ₗ Finsupp.lmapDomain R R f
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- Expand `⟪x + y, x + y⟫`  -/
inner_add_add_self : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x y : E), inner 𝕜 (x + y) (x + y) = inner 𝕜 x x + inner 𝕜 x y + inner 𝕜 y x + inner 𝕜 y y
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.mk_sigma_congr_lift : ∀ {ι : Type v} {ι' : Type v'} {f : ι → Type w} {g : ι' → Type w'} (e : ι ≃ ι'),
  (∀ (i : ι), Cardinal.lift.{w', w} (Cardinal.mk (f i)) = Cardinal.lift.{w, w'} (Cardinal.mk (g (e i)))) →
    Cardinal.lift.{max v' w', max w v} (Cardinal.mk ((i : ι) × f i)) =
      Cardinal.lift.{max v w, max w' v'} (Cardinal.mk ((i : ι') × g i))
-- Mathlib.RepresentationTheory.Coinvariants
Rep.coinvariantsShortComplex_f : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{w, u, v} k G) (S : Subgroup G)
  [inst_2 : S.Normal],
  (A.coinvariantsShortComplex S).f =
    Rep.ofHom
      { toLinearMap := (Representation.Coinvariants.ker (MonoidHom.comp A.ρ S.subtype)).subtype, isIntertwining' := ⋯ }
-- Std.Data.HashMap.Lemmas
Std.HashMap.size_modify : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α}
  {f : β → β}, (m.modify k f).size = m.size
-- Mathlib.Order.SupClosed
InfClosed.supClosure : ∀ {α : Type u_3} [inst : DistribLattice α] {s : Set α}, InfClosed s → InfClosed (supClosure s)
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
/-- A choice of witnesses of non-uniformity among the parts of a finpartition.  -/
Finpartition.nonuniformWitnesses : {α : Type u_1} →
  {𝕜 : Type u_2} →
    [inst : Field 𝕜] →
      [inst_1 : LinearOrder 𝕜] →
        [IsStrictOrderedRing 𝕜] →
          [inst : DecidableEq α] →
            {A : Finset α} →
              Finpartition A → (G : SimpleGraph α) → [DecidableRel G.Adj] → 𝕜 → Finset α → Finset (Finset α)
-- Init.Core
Subtype.instDecidableEq : {α : Sort u} → {p : α → Prop} → [DecidableEq α] → DecidableEq { x // p x }
-- Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
/-- If `A` is a family of enough low-degree polynomials over a finite field,
there is a pair of elements in `A` (with different indices but not necessarily
distinct), such that the difference of their remainders is close together.  -/
Polynomial.exists_approx_polynomial : ∀ {Fq : Type u_1} [inst : Fintype Fq] [inst_1 : Field Fq] {b : Polynomial Fq},
  b ≠ 0 →
    ∀ {ε : ℝ},
      0 < ε →
        ∀ (A : Fin (Fintype.card Fq ^ ⌈-Real.log ε / Real.log ↑(Fintype.card Fq)⌉₊).succ → Polynomial Fq),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ↑(Polynomial.cardPowDegree (A i₁ % b - A i₀ % b)) < Polynomial.cardPowDegree b • ε
-- Mathlib.Analysis.Normed.Ring.Lemmas
Filter.Tendsto.zero_mul_isBoundedUnder_le : ∀ {α : Type u_1} {ι : Type u_3} [inst : NonUnitalSeminormedRing α] {f g : ι → α} {l : Filter ι},
  Filter.Tendsto f l (nhds 0) →
    Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l ((fun x => ‖x‖) ∘ g) → Filter.Tendsto (fun x => f x * g x) l (nhds 0)
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the forward direction of `monovaryOn_inv_left₀`. -/
MonovaryOn.of_inv_left₀ : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : LinearOrder β] {s : Set ι} {f : ι → α} {g : ι → β},
  (∀ i ∈ s, 0 < f i) → MonovaryOn f⁻¹ g s → AntivaryOn f g s
-- Mathlib.Analysis.Calculus.Deriv.Comp
HasDerivAt.comp_hasFDerivWithinAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type w} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {𝕜' : Type u_1} [inst_3 : NontriviallyNormedField 𝕜'] [inst_4 : NormedAlgebra 𝕜 𝕜']
  {h₂ : 𝕜' → 𝕜'} {h₂' : 𝕜'} {f : E → 𝕜'} {f' : E →L[𝕜] 𝕜'} {s : Set E} (x : E),
  HasDerivAt h₂ h₂' (f x) → HasFDerivWithinAt f f' s x → HasFDerivWithinAt (h₂ ∘ f) (h₂' • f') s x
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.sup_eq_closure : ∀ {G : Type u_1} [inst : AddGroup G] (H H' : AddSubgroup G), H ⊔ H' = AddSubgroup.closure (↑H ∪ ↑H')
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapRightIso_functor_obj_right : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (L : CategoryTheory.Functor A T) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {R₁ R₂ : CategoryTheory.Functor B T} [inst_5 : P.RespectsIso] [inst_6 : Q.RespectsIso] [inst_7 : W.RespectsIso]
  (e : R₁ ≅ R₂) (X : CategoryTheory.MorphismProperty.Comma L R₁ P Q W),
  ((CategoryTheory.MorphismProperty.Comma.mapRightIso L e).functor.obj X).right = X.right
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKeyLE?.go.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (best : Option α) (size : ℕ) (k' : α) (v : β k')
  (l r : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.getKeyLE?.go k best (Std.DTreeMap.Internal.Impl.inner size k' v l r) =
    match compare k k' with
    | Ordering.lt => Std.DTreeMap.Internal.Impl.getKeyLE?.go k best l
    | Ordering.eq => some k'
    | Ordering.gt => Std.DTreeMap.Internal.Impl.getKeyLE?.go k (some k') r
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
CategoryTheory.Pseudofunctor.Grothendieck.mk.injEq : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} (base : 𝒮)
  (fiber : ↑(F.obj { as := base })) (base_1 : 𝒮) (fiber_1 : ↑(F.obj { as := base_1 })),
  ({ base := base, fiber := fiber } = { base := base_1, fiber := fiber_1 }) = (base = base_1 ∧ fiber ≍ fiber_1)
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.map_bot : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {K : Type u_3}
  [inst_3 : Field K] [inst_4 : Algebra F K] (f : E →ₐ[F] K), IntermediateField.map f ⊥ = ⊥
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.mapGm_apply : ∀ {β : Type u_2} [inst : MeasurableSpace β] {M : Type u_3} [inst_1 : AddCommMonoid M] [inst_2 : TopologicalSpace M]
  [inst_3 : ContinuousAdd M] {α : Type u_4} [inst_4 : MeasurableSpace α] (f : α → β)
  (v : MeasureTheory.VectorMeasure α M), (MeasureTheory.VectorMeasure.mapGm f) v = v.map f
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.iterate_pos_le_iff : ∀ (f : CircleDeg1Lift) {x : ℝ} {m : ℤ} {n : ℕ}, 0 < n → ((⇑f)^[n] x ≤ x + ↑n * ↑m ↔ f x ≤ x + ↑m)
-- Init.Data.Float.Model.Unpacked.Operations.ToNat
/-- Converts an `UnpackedFloat` to a `UInt8`, truncating after the decimal point, sending `NaN` to
`0` and clamping out-of-range values and infinities.
 -/
Float.Model.UnpackedFloat.toUInt8 : Float.Model.UnpackedFloat → UInt8
-- Init.Ext
/-- Registers an extensionality theorem.

* When `@[ext]` is applied to a theorem, the theorem is registered for the `ext` tactic, and it generates an "`ext_iff`" theorem.
The name of the theorem is from adding the suffix `_iff` to the theorem name.

* When `@[ext]` is applied to a structure, it generates an `.ext` theorem and applies the `@[ext]` attribute to it.
The result is an `.ext` and an `.ext_iff` theorem with the `.ext` theorem registered for the `ext` tactic.

* An optional natural number argument, e.g. `@[ext 9000]`, specifies a priority for the `ext` lemma.
Higher-priority lemmas are chosen first, and the default is `1000`.

* The flag `@[ext (iff := false)]` disables generating an `ext_iff` theorem.

* The flag `@[ext (flat := false)]` causes generated structure extensionality theorems to show inherited fields based on their representation,
rather than flattening the parents' fields into the lemma's equality hypotheses.
 -/
Lean.Parser.Attr.ext : Lean.ParserDescr
-- Mathlib.GroupTheory.Torsion
AddCommGroup.mem_torsion : ∀ {G : Type u_1} [inst : AddCommGroup G] (g : G), g ∈ AddCommGroup.torsion G ↔ IsOfFinAddOrder g
-- Lean.Parser.Basic
_private.Lean.Parser.Basic.0.Lean.Parser.decimalNumberFn.parseScientific : String.Pos.Raw → Bool → Lean.Parser.ParserContext → Lean.Parser.ParserState → Lean.Parser.ParserState
-- Mathlib.Topology.Maps.Strict.Group
/-- The product (in the sense of `MonoidHom.prodMap`) of group homomorphisms is strict if and only
if both homomorphisms are strict.  -/
MonoidHom.isStrictMap_prodMap_iff : ∀ {G : Type u_1} {H : Type u_2} {G' : Type u_3} {H' : Type u_4} [inst : Group G'] [inst_1 : Group H'] [inst_2 : Group G]
  [inst_3 : Group H] {f : G →* H} {g : G' →* H'} [inst_4 : TopologicalSpace G] [inst_5 : TopologicalSpace H]
  [IsTopologicalGroup G] [inst_7 : TopologicalSpace G'] [IsTopologicalGroup G'] [inst_9 : TopologicalSpace H'],
  Topology.IsStrictMap ⇑(f.prodMap g) ↔ Topology.IsStrictMap ⇑f ∧ Topology.IsStrictMap ⇑g
-- Mathlib.Analysis.Normed.Group.Defs
SeminormedAddGroup.ofAddDist.eq_1 : ∀ {E : Type u_5} [inst : Norm E] [inst_1 : AddGroup E] [inst_2 : PseudoMetricSpace E] (h₁ : ∀ (x : E), ‖x‖ = dist 0 x)
  (h₂ : ∀ (x y z : E), dist x y ≤ dist (z + x) (z + y)),
  SeminormedAddGroup.ofAddDist h₁ h₂ =
    { toNorm := inst, toAddGroup := inst_1, toPseudoMetricSpace := inst_2, dist_eq := ⋯ }
-- Mathlib.Topology.Homotopy.Product
ContinuousMap.Homotopy.prod_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {A : Type u_3}
  [inst_2 : TopologicalSpace A] {f₀ f₁ : C(A, α)} {g₀ g₁ : C(A, β)} (F : f₀.Homotopy f₁) (G : g₀.Homotopy g₁)
  (t : ↑unitInterval × A), (F.prod G) t = (F t, G t)
-- Mathlib.Order.WithBot
_private.Mathlib.Order.WithBot.0.WithBot.decidableLE.match_1.eq_2 : ∀ {α : Type u_1} (motive : WithBot α → WithBot α → Sort u_2) (a : α) (h_1 : (x : WithBot α) → motive none x)
  (h_2 : (a : α) → motive (some a) none) (h_3 : (a b : α) → motive (some a) (some b)),
  (match some a, none with
    | none, x => h_1 x
    | some a, none => h_2 a
    | some a, some b => h_3 a b) =
    h_2 a
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.interior_eq_empty : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] [inst_4 : PartialOrder k] (s : Affine.Simplex k P 0), s.interior = ∅