mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.sum_empty : ∀ {ι : Type u_1} {M : Type u_3} {f : ι → M} [inst : AddCommMonoid M], ∑ x ∈ ∅, f x = 0
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.size_toArray : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α], m.WF → (Std.DHashMap.Raw.Const.toArray m).size = m.size
-- Mathlib.AlgebraicGeometry.Cover.Open
AlgebraicGeometry.Scheme.AffineOpenCover.instIsOpenImmersionF : ∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.AffineOpenCover) (j : 𝒰.I₀), AlgebraicGeometry.IsOpenImmersion (𝒰.f j)
-- Init.Data.Queue
Std.Queue.mk.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (eList dList : List α),
  sizeOf { eList := eList, dList := dList } = 1 + sizeOf eList + sizeOf dList
-- Lean.Meta.HaveTelescope
/-- Configuration for specifying how unused let-declarations are eliminated.  -/
Lean.Meta.ZetaUnusedMode : Type
-- Mathlib.Topology.Category.TopCat.Limits.Pullbacks
TopCat.pullback_fst_image_snd_preimage : ∀ {X Y Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z) (U : Set ↑Y),
  ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.fst f g)) ''
      ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.snd f g)) ⁻¹' U =
    ⇑(CategoryTheory.ConcreteCategory.hom f) ⁻¹' ⇑(CategoryTheory.ConcreteCategory.hom g) '' U
-- Mathlib.CategoryTheory.Elements
/-- The initial object in the category of elements for a representable functor. In `isInitial` it is
shown that this is initial.
 -/
CategoryTheory.Functor.Elements.initial : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → (A : C) → (CategoryTheory.yoneda.obj A).Elements
-- Mathlib.Algebra.Exact.Basic
LinearMap.exact_iff : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {P : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P}, Function.Exact ⇑f ⇑g ↔ g.ker = f.range
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.toArrowArrowFunctor_obj_right_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C),
  (CategoryTheory.Square.toArrowArrowFunctor.obj sq).right.left = sq.X₂
-- Mathlib.AlgebraicGeometry.Sites.Proetale
AlgebraicGeometry.Scheme.ProEt.instIsContinuousOverForgetTopologyOverProetaleTopology : ∀ (S : AlgebraicGeometry.Scheme),
  (AlgebraicGeometry.Scheme.ProEt.forget S).IsContinuous (AlgebraicGeometry.Scheme.ProEt.topology S)
    (AlgebraicGeometry.Scheme.proetaleTopology.over S)
-- Mathlib.Logic.Function.Basic
Function.Involutive.surjective : ∀ {α : Sort u} {f : α → α}, Function.Involutive f → Function.Surjective f
-- Mathlib.Topology.Connected.PathConnected
ZerothHomotopy.isQuotientMap_mk : ∀ {X : Type u_1} [inst : TopologicalSpace X], Topology.IsQuotientMap ZerothHomotopy.mk
-- Mathlib.Algebra.DualQuaternion
Quaternion.re_fst_dualNumberEquiv : ∀ {R : Type u_1} [inst : CommRing R] (q : Quaternion (DualNumber R)),
  (TrivSqZeroExt.fst (Quaternion.dualNumberEquiv q)).re = TrivSqZeroExt.fst q.re
-- Mathlib.Combinatorics.SimpleGraph.Prod
SimpleGraph.Iso.boxProdSumDistrib_symm_apply : ∀ {V : Type u_4} {W₁ : Type u_8} {W₂ : Type u_9} (G : SimpleGraph V) (H₁ : SimpleGraph W₁) (H₂ : SimpleGraph W₂)
  (a : V × W₁ ⊕ V × W₂),
  (RelIso.symm (SimpleGraph.Iso.boxProdSumDistrib G H₁ H₂)) a =
    ((Equiv.sumProdDistrib W₁ W₂ V).symm (Sum.map Prod.swap Prod.swap a)).swap
-- Mathlib.Analysis.Calculus.FDeriv.Prod
fderivWithin_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {s : Set E} {ι : Type u_6} {F' : ι → Type u_7}
  [inst_3 : (i : ι) → NormedAddCommGroup (F' i)] [inst_4 : (i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i},
  DifferentiableWithinAt 𝕜 Φ s x →
    UniqueDiffWithinAt 𝕜 s x →
      ∀ (i : ι), fderivWithin 𝕜 (fun x => Φ x i) s x = ContinuousLinearMap.proj i ∘SL fderivWithin 𝕜 Φ s x
-- Init.Data.Int.DivMod.Basic
/-- Integer modulo using the T-rounding convention.

In [the T-rounding convention][t-rounding] (division with truncation), all rounding is towards zero.
Division by 0 is defined to be 0 and `Int.tmod a 0 = a`.

In this convention, `Int.tmod a b + b * (Int.tdiv a b) = a`. Additionally,
`Int.natAbs (Int.tmod a b) = Int.natAbs a % Int.natAbs b`, and when `b` does not divide `a`,
`Int.tmod a b` has the same sign as `a`.

[t-rounding]: https://dl.acm.org/doi/pdf/10.1145/128861.128862

This function is overridden by the compiler with an efficient implementation. This definition is the
logical model.

Examples:
* `(7 : Int).tmod (0 : Int) = 7`
* `(0 : Int).tmod (7 : Int) = 0`
* `(12 : Int).tmod (6 : Int) = 0`
* `(12 : Int).tmod (-6 : Int) = 0`
* `(-12 : Int).tmod (6 : Int) = 0`
* `(-12 : Int).tmod (-6 : Int) = 0`
* `(12 : Int).tmod (7 : Int) = 5`
* `(12 : Int).tmod (-7 : Int) = 5`
* `(-12 : Int).tmod (7 : Int) = -5`
* `(-12 : Int).tmod (-7 : Int) = -5`
 -/
Int.tmod : ℤ → ℤ → ℤ
-- Std.Data.Internal.List.Associative
Std.Internal.List.isEmpty_filter_not_contains_map_fst_iff : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l₁ →
    ((List.filter (fun p => !(List.map Sigma.fst l₂).contains p.fst) l₁).isEmpty = true ↔
      ∀ (k : α), Std.Internal.List.containsKey k l₁ = true → Std.Internal.List.containsKey k l₂ = true)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.forget_obj : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor J C) (t : CategoryTheory.Limits.Cone F),
  (CategoryTheory.Limits.Cone.forget F).obj t = t.pt
-- Mathlib.Algebra.Lie.Basic
LieEquiv.coe_injective : ∀ {R : Type u} {L₁ : Type v} {L₂ : Type w} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieRing L₂]
  [inst_3 : LieAlgebra R L₁] [inst_4 : LieAlgebra R L₂], Function.Injective DFunLike.coe
-- Mathlib.Order.RelClasses
Set.Bounded.eq_1 : ∀ {α : Type u} (r : α → α → Prop) (s : Set α), Set.Bounded r s = ∃ a, ∀ b ∈ s, r b a
-- Mathlib.Topology.MetricSpace.IsometricSMul
IsIsometricSMul.opposite_of_comm : ∀ (M : Type u) (X : Type w) [inst : PseudoEMetricSpace X] [inst_1 : SMul M X] [inst_2 : SMul Mᵐᵒᵖ X]
  [IsCentralScalar M X] [IsIsometricSMul M X], IsIsometricSMul Mᵐᵒᵖ X
-- Mathlib.Data.Finset.Lattice.Basic
Finset.mem_union_right : ∀ {α : Type u_1} [inst : DecidableEq α] {t : Finset α} {a : α} (s : Finset α), a ∈ t → a ∈ s ∪ t
-- Mathlib.LinearAlgebra.DFinsupp
/-- **Alias** of `iSupIndep_iff_finsetSum_eq_imp_eq`. -/
iSupIndep_iff_finset_sum_eq_imp_eq : ∀ {ι : Type u_1} {R : Type u_3} {N : Type u_6} [inst : Ring R] [inst_1 : AddCommGroup N] [inst_2 : Module R N]
  (p : ι → Submodule R N),
  iSupIndep p ↔
    ∀ (s : Finset ι) (v w : ι → N), (∀ i ∈ s, v i ∈ p i ∧ w i ∈ p i) → ∑ i ∈ s, v i = ∑ i ∈ s, w i → ∀ i ∈ s, v i = w i
-- Lean.Util.LeanOptions
Lean.instReprLeanOptions : Repr Lean.LeanOptions
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardSliceSearcher.exists_matchesAt_iff_eq_append : ∀ {pat s : String.Slice}, (∃ pos, String.Slice.Pattern.Model.MatchesAt pat pos) ↔ ∃ t₁ t₂, s.copy = t₁ ++ pat.copy ++ t₂
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.subst_zero_eq_C_constantCoeff : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] {τ : Type u_4} {S : Type u_5} [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {f : MvPowerSeries σ R},
  MvPowerSeries.subst 0 f = (MvPowerSeries.map (algebraMap R S)) (MvPowerSeries.C (MvPowerSeries.constantCoeff f))
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.ObjectProperty.isCoseparating_bot_of_isThin : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [Quiver.IsThin C], ⊥.IsCoseparating
-- Mathlib.LinearAlgebra.Reflection
Module.reflection.congr_simp : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {x x_1 : M}
  (e_x : x = x_1) {f f_1 : Module.Dual R M} (e_f : f = f_1) (h : f x = 2), Module.reflection h = Module.reflection ⋯
-- Mathlib.Combinatorics.Enumerative.Pentagonal.Basic
pentagonal_def : ∀ (k : ℤ), pentagonal k = (k * (3 * k - 1) / 2).toNat
-- Mathlib.Data.DFinsupp.BigOperators
AddEquiv.map_dfinsuppSumAddHom : ∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] {R : Type u_1} {S : Type u_2} [inst_1 : AddCommMonoid R]
  [inst_2 : AddCommMonoid S] [inst_3 : (i : ι) → AddZeroClass (β i)] (h : R ≃+ S) (f : Π₀ (i : ι), β i)
  (g : (i : ι) → β i →+ R), h ((DFinsupp.sumAddHom g) f) = (DFinsupp.sumAddHom fun i => h.toAddMonoidHom.comp (g i)) f
-- Mathlib.Algebra.Azumaya.Basic
IsAzumaya.of_AlgEquiv : ∀ (R : Type u_1) (A : Type u_2) (B : Type u_3) [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Ring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (e : A ≃ₐ[R] B) [IsAzumaya R A], IsAzumaya R B
-- Lean.Meta.IndPredBelow
_private.Lean.Meta.IndPredBelow.0.Lean.Meta.IndPredBelow.toImplicit.eq_def : ∀ (e : Lean.Expr),
  Lean.Meta.IndPredBelow.toImplicit✝ e =
    match e with
    | Lean.Expr.forallE binderName t (b@h:(Lean.Expr.forallE binderName_1 binderType body binderInfo)) binderInfo_1 =>
      e.updateForall! Lean.BinderInfo.implicit t (Lean.Meta.IndPredBelow.toImplicit✝ b)
    | e => e
-- Mathlib.Algebra.Star.Subalgebra
/-- Galois insertion between `adjoin` and `coe`.  -/
StarAlgebra.gi : {R : Type u_2} →
  {A : Type u_3} →
    [inst : CommSemiring R] →
      [inst_1 : StarRing R] →
        [inst_2 : Semiring A] →
          [inst_3 : Algebra R A] →
            [inst_4 : StarRing A] → [inst_5 : StarModule R A] → GaloisInsertion (StarAlgebra.adjoin R) SetLike.coe
-- Init.Data.UInt.Lemmas
USize.toFin_ofNatClamp_of_le : ∀ {n : ℕ}, USize.size ≤ n → (USize.ofNatClamp n).toFin = ⟨USize.size - 1, USize.toFin_ofNatClamp_of_le._proof_1⟩
-- Aesop.EMap
Aesop.instInhabitedEMap.default : {α : Type u_1} → Aesop.EMap α
-- Mathlib.Combinatorics.Enumerative.DoubleCounting
Finset.bipartiteBelow_swap : ∀ {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (t : Finset β) (a : α) [inst : DecidablePred (r a)],
  Finset.bipartiteBelow (Function.swap r) t a = Finset.bipartiteAbove r t a
-- Mathlib.Data.Fin.SuccPredOrder
Fin.orderPred_succ : ∀ {n : ℕ} (i : Fin n), Order.pred i.succ = i.castSucc
-- Mathlib.Data.ZMod.IntUnitsPower
ofMul_uzpow : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : Module R (Additive ℤˣ)] (u : ℤˣ) (r : R),
  Additive.ofMul (u ^ r) = r • Additive.ofMul u
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.HomClass.mk : ∀ {L : outParam FirstOrder.Language} {F : Type u_3} {M : outParam (Type u_4)} {N : outParam (Type u_5)}
  [inst : FunLike F M N] [inst_1 : L.Structure M] [inst_2 : L.Structure N],
  (∀ (φ : F) {n : ℕ} (f : L.Functions n) (x : Fin n → M),
      φ (FirstOrder.Language.Structure.funMap f x) = FirstOrder.Language.Structure.funMap f (⇑φ ∘ x)) →
    (∀ (φ : F) {n : ℕ} (r : L.Relations n) (x : Fin n → M),
        FirstOrder.Language.Structure.RelMap r x → FirstOrder.Language.Structure.RelMap r (⇑φ ∘ x)) →
      L.HomClass F M N
-- Mathlib.Topology.Sheaves.Flasque
CategoryTheory.CategoryStruct.toQuiver.hcongr_2 : ∀ (obj obj' : Type u),
  obj = obj' →
    ∀ (self : CategoryTheory.CategoryStruct.{v, u} obj) (self' : CategoryTheory.CategoryStruct.{v, u} obj'),
      self ≍ self' → self.toQuiver ≍ self'.toQuiver
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.coeff_X_mul' : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : DecidableEq σ] (m : σ →₀ ℕ) (s : σ)
  (p : MvPolynomial σ R),
  MvPolynomial.coeff m (MvPolynomial.X s * p) = if s ∈ m.support then MvPolynomial.coeff (m - fun₀ | s => 1) p else 0
-- Mathlib.Tactic.ClickSuggestions.TryPremises
_private.Mathlib.Tactic.ClickSuggestions.TryPremises.0.Mathlib.Tactic.ClickSuggestions.Candidates.appAt.injEq : ∀ (arr arr_1 : Array Mathlib.Tactic.ClickSuggestions.ApplyAtLemma),
  (Mathlib.Tactic.ClickSuggestions.Candidates.appAt✝ arr = Mathlib.Tactic.ClickSuggestions.Candidates.appAt✝ arr_1) =
    (arr = arr_1)
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.strictMap_iSup : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (F : CategoryTheory.Functor C D) {ι : Type u_3} (P : ι → CategoryTheory.MorphismProperty C),
  (⨆ i, P i).strictMap F = ⨆ i, (P i).strictMap F
-- Mathlib.Data.Nat.ModEq
Nat.ModEq.rfl : ∀ {n a : ℕ}, a ≡ a [MOD n]
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
_private.Mathlib.Analysis.InnerProductSpace.Orthogonal.0.ClosedSubmodule.«term⟪_,_⟫» : Lean.ParserDescr
-- Mathlib.Computability.Reduce
stdRefl_manyOneReducible : ∀ {α : Type u_1} [inst : Primcodable α], Std.Refl ManyOneReducible
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.foldrM_eq_foldrM_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {δ : Type w} {m : Type w → Type w'} {β : Type v}
  {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp] [inst_1 : Monad m] [inst_2 : LawfulMonad m]
  {f : α → β → δ → m δ} {init : δ},
  Std.ExtDTreeMap.foldrM f init t = List.foldrM (fun a b => f a.1 a.2 b) init (Std.ExtDTreeMap.Const.toList t)
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
AlgEquiv.subalgebraMap_symm_apply_coe : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (e : A ≃ₐ[R] B) (S : Subalgebra R A)
  (y : ↑(⇑↑e.toRingEquiv.toAddEquiv '' ↑S.toAddSubmonoid)), ↑((e.subalgebraMap S).symm y) = e.symm ↑y
-- Mathlib.Topology.Order.LeftRightNhds
/-- A set is a neighborhood of `a` within `(a, +∞)` if and only if it contains an interval `(a, u]`
with `a < u`.  -/
mem_nhdsGT_iff_exists_Ioc_subset : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [NoMaxOrder α]
  [DenselyOrdered α] {a : α} {s : Set α}, s ∈ nhdsWithin a (Set.Ioi a) ↔ ∃ u ∈ Set.Ioi a, Set.Ioc a u ⊆ s
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.abs_toReal_eq_pi_div_two_iff : ∀ {θ : Real.Angle}, |θ.toReal| = Real.pi / 2 ↔ θ = ↑(Real.pi / 2) ∨ θ = ↑(-Real.pi / 2)
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
_private.Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic.0.CategoryTheory.WithInitial.opEquiv.match_3.eq_2 : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{u_2, u_1} C]
  (motive : (x y : (CategoryTheory.WithInitial C)ᵒᵖ) → (Opposite.unop y ⟶ Opposite.unop x) → (x ⟶ y) → Sort u_3) (a : C)
  (x :
    Opposite.unop (Opposite.op CategoryTheory.WithInitial.star) ⟶
      Opposite.unop (Opposite.op (CategoryTheory.WithInitial.of a)))
  (x_1 : Opposite.op (CategoryTheory.WithInitial.of a) ⟶ Opposite.op CategoryTheory.WithInitial.star)
  (h_1 :
    (x y : C) →
      (f :
          Opposite.unop (Opposite.op (CategoryTheory.WithInitial.of y)) ⟶
            Opposite.unop (Opposite.op (CategoryTheory.WithInitial.of x))) →
        (x_2 : Opposite.op (CategoryTheory.WithInitial.of x) ⟶ Opposite.op (CategoryTheory.WithInitial.of y)) →
          motive (Opposite.op (CategoryTheory.WithInitial.of x)) (Opposite.op (CategoryTheory.WithInitial.of y)) f x_2)
  (h_2 :
    (a : C) →
      (x :
          Opposite.unop (Opposite.op CategoryTheory.WithInitial.star) ⟶
            Opposite.unop (Opposite.op (CategoryTheory.WithInitial.of a))) →
        (x_2 : Opposite.op (CategoryTheory.WithInitial.of a) ⟶ Opposite.op CategoryTheory.WithInitial.star) →
          motive (Opposite.op (CategoryTheory.WithInitial.of a)) (Opposite.op CategoryTheory.WithInitial.star) x x_2)
  (h_3 :
    (x :
        Opposite.unop (Opposite.op CategoryTheory.WithInitial.star) ⟶
          Opposite.unop (Opposite.op CategoryTheory.WithInitial.star)) →
      (x_2 : Opposite.op CategoryTheory.WithInitial.star ⟶ Opposite.op CategoryTheory.WithInitial.star) →
        motive (Opposite.op CategoryTheory.WithInitial.star) (Opposite.op CategoryTheory.WithInitial.star) x x_2),
  (match Opposite.op (CategoryTheory.WithInitial.of a), Opposite.op CategoryTheory.WithInitial.star, x, x_1 with
    | Opposite.op (CategoryTheory.WithInitial.of x), Opposite.op (CategoryTheory.WithInitial.of y), f, x_2 =>
      h_1 x y f x_2
    | Opposite.op (CategoryTheory.WithInitial.of a), Opposite.op CategoryTheory.WithInitial.star, x, x_2 => h_2 a x x_2
    | Opposite.op CategoryTheory.WithInitial.star, Opposite.op CategoryTheory.WithInitial.star, x, x_2 => h_3 x x_2) =
    h_2 a x x_1
-- Mathlib.Data.Set.Basic
Set.union_isComm : ∀ {α : Type u}, Std.Commutative fun x1 x2 => x1 ∪ x2
-- Mathlib.Analysis.Complex.Trigonometric
Real.tanh_zero : Real.tanh 0 = 0
-- Lean.Meta.Tactic.Cases
/-- Applies `cases` (recursively) to any hypothesis of the form `h : p ∧ q`.
 -/
Lean.MVarId.casesAnd : Lean.MVarId → Lean.MetaM Lean.MVarId
-- Mathlib.Order.Monotone.Monovary
antivaryOn_id_iff : ∀ {ι : Type u_1} {α : Type u_3} [inst : Preorder α] {f : ι → α} {s : Set ι} [inst_1 : PartialOrder ι],
  AntivaryOn f id s ↔ AntitoneOn f s
-- Mathlib.Algebra.Group.Idempotent
IsIdempotentElem.coe_one : ∀ {M : Type u_1} [inst : MulOneClass M], ↑1 = 1
-- Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
NumberField.Units.finrank_modTorsion : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  Module.finrank ℤ (Additive ((NumberField.RingOfIntegers K)ˣ ⧸ NumberField.Units.torsion K)) = NumberField.Units.rank K
-- Init.Data.Float.Float
/-- Computes the floor of a floating-point number, which is the largest integer that's no larger
than the given number.

This function does not reduce in the kernel. It is implemented in compiled code by the C function
`floor`.

Examples:
 * `Float.floor 1.5 = 1`
 * `Float.floor (-1.5) = (-2)`
 -/
Float.floor : Float → Float
-- Mathlib.Analysis.Normed.Group.Uniform
/-- **Alias** of the reverse direction of `antilipschitzWith_inv_iff`. -/
AntilipschitzWith.inv : ∀ {α : Type u_4} {E : Type u_5} [inst : SeminormedCommGroup E] [inst_1 : PseudoEMetricSpace α] {K : NNReal} {f : α → E},
  AntilipschitzWith K f → AntilipschitzWith K f⁻¹
-- Lean.Meta.Basic
Lean.Meta.SynthInstanceCacheKey : Type
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.instAddCommMonoid.eq_1 : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R],
  MonoidAlgebra.instAddCommMonoid = { toAddMonoid := MonoidAlgebra.instAddMonoid, add_comm := ⋯ }
-- Init.Data.SInt.Lemmas
Int8.toBitVec_minValue : Int8.minValue.toBitVec = BitVec.intMin 8
-- Mathlib.Algebra.Order.Field.Basic
LinearOrderedSemiField.toDenselyOrdered : ∀ {α : Type u_2} [inst : Semifield α] [inst_1 : PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α],
  DenselyOrdered α
-- Lean.Language.Lean.Types
Lean.Language.Lean.CommandResultSnapshot.mk : Lean.Language.Snapshot → Lean.Elab.Command.State → Lean.Language.Lean.CommandResultSnapshot
-- Mathlib.Order.SuccPred.Limit
/-- Recursion principle on a well-founded partial `SuccOrder`.  -/
SuccOrder.prelimitRecOn : {α : Type u_1} →
  (b : α) →
    {motive : α → Sort u_2} →
      [inst : PartialOrder α] →
        [inst_1 : SuccOrder α] →
          [WellFoundedLT α] →
            ((a : α) → ¬IsMax a → motive a → motive (Order.succ a)) →
              ((a : α) → Order.IsSuccPrelimit a → ((b : α) → b < a → motive b) → motive a) → motive b
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.SimpleFunc.setToL1S_smul_left' : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (T T' : Set α → E →L[ℝ] F) (c : ℝ),
  (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T' s = c • T s) →
    ∀ (f : ↥(α →₁ₛ[μ] E)), MeasureTheory.L1.SimpleFunc.setToL1S T' f = c • MeasureTheory.L1.SimpleFunc.setToL1S T f
-- Std.Sync.Broadcast
Std.Broadcast.instDecidableEqError : DecidableEq Std.Broadcast.Error
-- Mathlib.Algebra.Opposites
/-- The element of `MulOpposite α` that represents `x : α`.  -/
MulOpposite.op : {α : Type u_1} → α → αᵐᵒᵖ
-- Lean.Language.Lean.Types
/-- Parser input context supplied by the driver, stored here for incremental parsing.  -/
Lean.Language.Lean.HeaderParsedSnapshot.ictx : Lean.Language.Lean.HeaderParsedSnapshot → Lean.Parser.InputContext
-- Init.Data.String.Lemmas.Basic
String.copy_toByteArray_sliceTo : ∀ {s : String} {pos : s.Pos}, (s.sliceTo pos).copy.toByteArray = s.toByteArray.extract 0 pos.offset.byteIdx
-- Mathlib.Data.Set.Image
sigma_mk_preimage_image_eq_self : ∀ {α : Type u_1} {β : α → Type u_2} {i : α} {s : Set (β i)}, Sigma.mk i ⁻¹' Sigma.mk i '' s = s
-- Mathlib.RingTheory.HahnSeries.HEval
HahnSeries.SummableFamily.powerSeriesFamily_hsum_zero : ∀ {Γ : Type u_1} {R : Type u_3} {V : Type u_4} [inst : AddCommMonoid Γ] [inst_1 : LinearOrder Γ]
  [inst_2 : IsOrderedCancelAddMonoid Γ] [inst_3 : CommRing R] [inst_4 : CommRing V] [inst_5 : Algebra R V]
  (f : PowerSeries R), (HahnSeries.SummableFamily.powerSeriesFamily 0 f).hsum = PowerSeries.constantCoeff f • 1
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get!_filter_of_getKey?_eq_some : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited β] {f : α → β → Bool} {k k' : α},
  m.getKey? k = some k' →
    Std.ExtDHashMap.Const.get! (Std.ExtDHashMap.filter f m) k =
      (Option.filter (fun x => f k' x) (Std.ExtDHashMap.Const.get? m k)).get!
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
_private.Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing.0.AlgebraicGeometry.PresheafedSpace.GlueData.«termπ₁_,_,_» : Lean.ParserDescr
-- Lean.Meta.HaveTelescope
/-- Simplify and eliminate unused `let`-declarations in a single pass.  -/
Lean.Meta.ZetaUnusedMode.singlePass : Lean.Meta.ZetaUnusedMode
-- Mathlib.NumberTheory.Ostrowski
/-- If `f n > 1` for some `n` then `f n > 1` for all `n ≥ 2`  -/
Rat.AbsoluteValue.one_lt_of_not_bounded : ∀ {f : AbsoluteValue ℚ ℝ}, (¬∀ (n : ℕ), f ↑n ≤ 1) → ∀ {n₀ : ℕ}, 1 < n₀ → 1 < f ↑n₀
-- Lean.Elab.App
/-- Elaborate function application arguments.  -/
Lean.Elab.Term.ElabAppArgs.main : Lean.Elab.Term.ElabAppArgs.M Lean.Expr
-- Batteries.Data.Array.Basic
/-- Returns the first maximal element among `d` and elements of the array.
If `start` and `stop` are given, only the subarray `xs[start...stop]` is
considered (in addition to `d`).
 -/
Array.rangeMaxWith : {α : Type u_1} → [ord : Ord α] → (xs : Array α) → α → optParam ℕ 0 → optParam ℕ xs.size → α
-- Mathlib.LinearAlgebra.Matrix.Cartan
CartanMatrix.E₆_transpose : CartanMatrix.E₆.transpose = CartanMatrix.E₆
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
HasSum.summable : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {L : SummationFilter β}
  {f : β → α} {a : α}, HasSum f a L → Summable f L
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.mk_fin : ∀ (n : ℕ), Cardinal.mk (Fin n) = ↑n
-- Mathlib.Analysis.Distribution.TemperedDistribution
TemperedDistribution.smulLeftCLM_neg : ∀ {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : AddCommGroup F]
  [inst_3 : Module ℂ F] [inst_4 : TopologicalSpace F] [inst_5 : IsTopologicalAddGroup F]
  [inst_6 : ContinuousConstSMul ℂ F] {g : E → ℂ},
  Function.HasTemperateGrowth g → TemperedDistribution.smulLeftCLM F (-g) = -TemperedDistribution.smulLeftCLM F g