mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get?_insertManyIfNewUnit_list : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => Unit) [EquivBEq α]
  [LawfulHashable α],
  (↑m).WF →
    ∀ {l : List α} {k : α},
      Std.DHashMap.Internal.Raw₀.Const.get? (↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m l)) k =
        if m.contains k = true ∨ l.contains k = true then some () else none
-- Mathlib.Data.FP.Basic
FP.RMode.noConfusionType : Sort v✝ → FP.RMode → FP.RMode → Sort v✝
-- Mathlib.Algebra.Ring.BooleanRing
instNegBool_mathlib : Neg Bool
-- Mathlib.CategoryTheory.Filtered.Basic
CategoryTheory.IsCofiltered.of_hasFiniteLimits : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteLimits C],
  CategoryTheory.IsCofiltered C
-- Batteries.Data.Fin.Fold
Fin.dfoldl_succ : ∀ {n : ℕ} {α : Fin (n + 1 + 1) → Type u_1} (f : (i : Fin (n + 1)) → α i.castSucc → α i.succ) (x : α 0),
  Fin.dfoldl (n + 1) α f x = Fin.dfoldl n (α ∘ Fin.succ) (fun x1 x2 => f x1.succ x2) (f 0 x)
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.prodProdProdComm_symm : ∀ (R : Type u_8) (M₁ : Type u_9) (M₂ : Type u_10) (M₃ : Type u_11) (M₄ : Type u_12) [inst : Semiring R]
  [inst_1 : AddCommMonoid M₁] [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : AddCommMonoid M₄]
  [inst_5 : Module R M₁] [inst_6 : Module R M₂] [inst_7 : Module R M₃] [inst_8 : Module R M₄]
  [inst_9 : TopologicalSpace M₁] [inst_10 : TopologicalSpace M₂] [inst_11 : TopologicalSpace M₃]
  [inst_12 : TopologicalSpace M₄],
  (ContinuousLinearEquiv.prodProdProdComm R M₁ M₂ M₃ M₄).symm = ContinuousLinearEquiv.prodProdProdComm R M₁ M₃ M₂ M₄
-- Mathlib.RingTheory.MvPolynomial.Ideal
MonomialOrder.span_leadingTerm_insert_zero : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] {m : MonomialOrder σ} (B : Set (MvPolynomial σ R)),
  Ideal.span (m.leadingTerm '' insert 0 B) = Ideal.span (m.leadingTerm '' B)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.nil_append : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), SimpleGraph.Walk.nil.append p = p
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.val_neg : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : NegMemClass σ A]
  {𝒜 : ι → σ} {x : Submonoid A} (y : HomogeneousLocalization 𝒜 x), (-y).val = -y.val
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.size_alter_eq_add_one : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {f : Option β → Option β}, k ∉ t → (f t[k]?).isSome = true → (t.alter k f).size = t.size + 1
-- Lean.Namespace
/-- Return `true` if `n` is the name of a namespace in `env`.  -/
Lean.Environment.isNamespace : Lean.Environment → Lean.Name → Bool
-- Mathlib.Tactic.Linter.TextBased
/-- Parse all style exceptions for a line of input.
Return an array of all exceptions which could be parsed: invalid input is ignored.  -/
_private.Mathlib.Tactic.Linter.TextBased.0.Mathlib.Linter.TextBased.parseStyleExceptions : Array String → Array Mathlib.Linter.TextBased.ErrorContext✝
-- Mathlib.Topology.PartialHomeomorph.Defs
Homeomorph.toPartialHomeomorphOfImageEq_symm_apply : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : X ≃ₜ Y) (s : Set X)
  (t : Set Y) (h : ⇑e '' s = t), ↑(e.toPartialHomeomorphOfImageEq s t h).symm = ⇑e.symm
-- Mathlib.LinearAlgebra.Projectivization.Basic
Projectivization.mk'_eq_mk : ∀ (K : Type u_1) {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  (v : { v // v ≠ 0 }), Projectivization.mk' K v = Projectivization.mk K ↑v ⋯
-- Mathlib.NumberTheory.Dioph
_private.Mathlib.NumberTheory.Dioph.0.Poly.sumsq.match_1.eq_2 : ∀ {α : Type u_1} (motive : List (Poly α) → Sort u_2) (p : Poly α) (ps : List (Poly α)) (h_1 : Unit → motive [])
  (h_2 : (p : Poly α) → (ps : List (Poly α)) → motive (p :: ps)),
  (match p :: ps with
    | [] => h_1 ()
    | p :: ps => h_2 p ps) =
    h_2 p ps
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
sub_le_self_iff : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [AddLeftMono α] (a : α) {b : α}, a - b ≤ a ↔ 0 ≤ b
-- Mathlib.AlgebraicGeometry.ColimitsOver
AlgebraicGeometry.Scheme.Cover.ColimitGluingData.pullbackGluedIso_inv_snd_assoc : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [inst : P.IsStableUnderBaseChange]
  [inst_1 : P.IsMultiplicative] {S : AlgebraicGeometry.Scheme} {J : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} J] {D : CategoryTheory.Functor J (P.Over ⊤ S)} {𝒰 : S.OpenCover}
  [inst_3 : CategoryTheory.Category.{v_2, u_2} 𝒰.I₀] [inst_4 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰]
  (d : AlgebraicGeometry.Scheme.Cover.ColimitGluingData D 𝒰)
  [inst_5 :
    ∀ {i j : 𝒰.I₀} (hij : i ⟶ j),
      CategoryTheory.Limits.PreservesColimitsOfShape J
        (CategoryTheory.MorphismProperty.Over.pullback P ⊤ (AlgebraicGeometry.Scheme.Cover.trans 𝒰 hij))]
  [inst_6 : Quiver.IsThin 𝒰.I₀] [inst_7 : Small.{u, u_2} 𝒰.I₀] [inst_8 : AlgebraicGeometry.IsZariskiLocalAtTarget P]
  (i : 𝒰.I₀) {Z : AlgebraicGeometry.Scheme} (h : 𝒰.X i ⟶ Z),
  CategoryTheory.CategoryStruct.comp (d.pullbackGluedIso i).inv.left
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd d.glued.hom (𝒰.f i)) h) =
    CategoryTheory.CategoryStruct.comp (d.cocone i).pt.hom h
-- Mathlib.Order.Hom.Basic
OrderIso.instEquivLike : {α : Type u_2} → {β : Type u_3} → [inst : LE α] → [inst_1 : LE β] → EquivLike (α ≃o β) α β
-- Mathlib.Algebra.Category.Ring.Constructions
CommRingCat.coproductCocone_inr : ∀ (A B : CommRingCat), (A.coproductCocone B).inr = CommRingCat.ofHom Algebra.TensorProduct.includeRight.toRingHom
-- Mathlib.Analysis.SpecialFunctions.Exp
Real.image_exp_uIcc : ∀ (a b : ℝ), Real.exp '' Set.uIcc a b = Set.uIcc (Real.exp a) (Real.exp b)
-- Mathlib.Algebra.Category.AlgCat.Monoidal
AlgCat.hom_whiskerLeft : ∀ {R : Type u} [inst : CommRing R] (L : AlgCat R) {M N : AlgCat R} (f : M ⟶ N),
  AlgCat.Hom.hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft L f) =
    Algebra.TensorProduct.map (AlgHom.id R ↑L) (AlgCat.Hom.hom f)
-- Mathlib.FieldTheory.Finite.GaloisField
instInhabitedGaloisField : (p : ℕ) → [inst : Fact (Nat.Prime p)] → (n : ℕ) → Inhabited (GaloisField p n)
-- Mathlib.CategoryTheory.Monoidal.FunctorCategory
CategoryTheory.instMonoidalFunctorObjWhiskeringRight : {C : Type u_1} →
  {D : Type u_2} →
    {E : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} E] →
            [inst_3 : CategoryTheory.MonoidalCategory D] →
              [inst_4 : CategoryTheory.MonoidalCategory E] →
                (L : CategoryTheory.Functor D E) →
                  [L.Monoidal] → ((CategoryTheory.Functor.whiskeringRight C D E).obj L).Monoidal
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.TransvectionStruct.toSpecialLinearGroup_def : ∀ {ι : Type u_1} {F : Type u_2} [inst : DecidableEq ι] [inst_1 : Fintype ι] [inst_2 : CommRing F]
  (t : Matrix.TransvectionStruct ι F), t.toSpecialLinearGroup = Matrix.SpecialLinearGroup.transvection ⋯ t.c
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F : Cᵒᵖ ⥤ Dᵒᵖ` creates colimits, then `F.unop : C ⥤ D` creates limits.  -/
CategoryTheory.Limits.createsLimitsUnop : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) → [CategoryTheory.CreatesColimits F] → CategoryTheory.CreatesLimits F.unop
-- Mathlib.CategoryTheory.Adjunction.Reflective
CategoryTheory.instIsRightAdjointCoreflector : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (j : CategoryTheory.Functor C D) [inst_2 : CategoryTheory.Coreflective j],
  (CategoryTheory.coreflector j).IsRightAdjoint
-- Init.Prelude
/-- The modulo operator, which computes the remainder when dividing one natural number by another.
Usually accessed via the `%` operator. When the divisor is `0`, the result is the dividend rather
than an error.

`Nat.mod` is a wrapper around `Nat.modCore` that special-cases two situations, giving better
definitional reductions:
 * `Nat.mod 0 m` should reduce to `m`, for all terms `m : Nat`.
 * `Nat.mod n (m + n + 1)` should reduce to `n` for concrete `Nat` literals `n`.

These reductions help `Fin n` literals work well, because the `OfNat` instance for `Fin` uses
`Nat.mod`. In particular, `(0 : Fin (n + 1)).val` should reduce definitionally to `0`. `Nat.modCore`
can handle all numbers, but its definitional reductions are not as convenient.

This function is overridden at runtime with an efficient implementation. This definition is the
logical model.

Examples:
 * `7 % 2 = 1`
 * `9 % 3 = 0`
 * `5 % 7 = 5`
 * `5 % 0 = 5`
 * `show ∀ (n : Nat), 0 % n = 0 from fun _ => rfl`
 * `show ∀ (m : Nat), 5 % (m + 6) = 5 from fun _ => rfl`
 -/
Nat.mod : ℕ → ℕ → ℕ
-- Mathlib.Tactic.Polynomial.Core
/-- Infer the base ring of `Polynomial`-like types that are registered using the `polynomial`
environment extensions. Includes e.g. `Polynomial` and `MvPolynomial`.  -/
Mathlib.Tactic.Polynomial.inferBase : Lean.Expr → Lean.MetaM Lean.Expr
-- Lean.Parser.Extension
Lean.Parser.mkParserAttributeImpl : Lean.Name → Lean.Name → autoParam Lean.Name Lean.Parser.mkParserAttributeImpl._auto_1 → Lean.AttributeImpl
-- Std.Data.DHashMap.Internal.Raw
Std.DHashMap.Internal.Raw.Const.beq_eq : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : BEq β]
  {m₁ m₂ : Std.DHashMap.Raw α fun x => β} (h₁ : m₁.WF) (h₂ : m₂.WF),
  Std.DHashMap.Raw.Const.beq m₁ m₂ = Std.DHashMap.Internal.Raw₀.Const.beq ⟨m₁, ⋯⟩ ⟨m₂, ⋯⟩
-- Lean.Meta.Tactic.Grind.Beta
/-- Applies beta-reduction for lambdas in `f`s equivalence class.
We use this function while internalizing new applications.
 -/
Lean.Meta.Grind.propagateBetaForNewApp : Lean.Expr → Lean.Meta.Grind.GoalM Unit
-- Mathlib.CategoryTheory.Category.Pairwise
_private.Mathlib.CategoryTheory.Category.Pairwise.0.CategoryTheory.Pairwise.diagramMap.match_1.eq_1 : ∀ {ι : Type u_1} (motive : (x x_1 : CategoryTheory.Pairwise ι) → (x ⟶ x_1) → Sort u_2) (i : ι)
  (h_1 :
    (i : ι) →
      motive (CategoryTheory.Pairwise.single i) (CategoryTheory.Pairwise.single i)
        (CategoryTheory.Pairwise.Hom.id_single i))
  (h_2 :
    (i j : ι) →
      motive (CategoryTheory.Pairwise.pair i j) (CategoryTheory.Pairwise.pair i j)
        (CategoryTheory.Pairwise.Hom.id_pair i j))
  (h_3 :
    (i j : ι) →
      motive (CategoryTheory.Pairwise.pair i j) (CategoryTheory.Pairwise.single i)
        (CategoryTheory.Pairwise.Hom.left i j))
  (h_4 :
    (i j : ι) →
      motive (CategoryTheory.Pairwise.pair i j) (CategoryTheory.Pairwise.single j)
        (CategoryTheory.Pairwise.Hom.right i j)),
  (match CategoryTheory.Pairwise.single i, CategoryTheory.Pairwise.single i,
      CategoryTheory.Pairwise.Hom.id_single i with
    | .(CategoryTheory.Pairwise.single i), .(CategoryTheory.Pairwise.single i),
      CategoryTheory.Pairwise.Hom.id_single i => h_1 i
    | .(CategoryTheory.Pairwise.pair i j), .(CategoryTheory.Pairwise.pair i j),
      CategoryTheory.Pairwise.Hom.id_pair i j => h_2 i j
    | .(CategoryTheory.Pairwise.pair i j), .(CategoryTheory.Pairwise.single i), CategoryTheory.Pairwise.Hom.left i j =>
      h_3 i j
    | .(CategoryTheory.Pairwise.pair i j), .(CategoryTheory.Pairwise.single j), CategoryTheory.Pairwise.Hom.right i j =>
      h_4 i j) =
    h_1 i
-- Mathlib.Analysis.Normed.Group.Hom
/-- If a bounded group homomorphism map is constructed from a group homomorphism via the constructor
`NormedAddGroupHom.ofLipschitz`, then its norm is bounded by the bound given to the constructor.  -/
NormedAddGroupHom.ofLipschitz_norm_le : ∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂] (f : V₁ →+ V₂)
  {K : NNReal} (h : LipschitzWith K ⇑f), ‖NormedAddGroupHom.ofLipschitz f h‖ ≤ ↑K
-- Std.Data.DTreeMap.AdditionalOperations
/-- Given a proof that such a mapping exists, retrieves the key-value pair with the smallest key that is
greater than or equal to the given key.
 -/
Std.DTreeMap.getEntryGE : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      [Std.TransCmp cmp] → (t : Std.DTreeMap α β cmp) → (k : α) → (∃ a ∈ t, (cmp a k).isGE = true) → (a : α) × β a
-- Mathlib.Algebra.Group.Action.Pi
Pi.vadd' : {ι : Type u_1} →
  {α : ι → Type u_4} → {β : ι → Type u_5} → [(i : ι) → VAdd (α i) (β i)] → VAdd ((i : ι) → α i) ((i : ι) → β i)
-- Mathlib.RingTheory.PowerSeries.Trunc
PowerSeries.monomial_eq_C_mul_X_pow : ∀ {R : Type u_1} [inst : Semiring R] (r : R) (n : ℕ), (PowerSeries.monomial n) r = PowerSeries.C r * PowerSeries.X ^ n
-- Lean.Data.LOption
Lean.instBEqLOption : {α : Type u_1} → [BEq α] → BEq (Lean.LOption α)
-- Mathlib.Analysis.RCLike.TangentCone
UniqueDiffWithinAt.of_real : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [h𝕜 : IsRCLikeNormedField 𝕜] {E : Type u_2}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedSpace ℝ E] {s : Set E} {x : E},
  UniqueDiffWithinAt ℝ s x → UniqueDiffWithinAt 𝕜 s x
-- Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells
/-- The inclusion of a cell.  -/
HomotopicalAlgebra.AttachCells.cell : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {α : Type t} →
      {A B : α → C} →
        {g : (a : α) → A a ⟶ B a} →
          {X₁ X₂ : C} → {f : X₁ ⟶ X₂} → (c : HomotopicalAlgebra.AttachCells g f) → (i : c.ι) → B (c.π i) ⟶ X₂
-- Mathlib.RingTheory.DividedPowers.RatAlgebra
/-- The family of functions `ℕ → A → A` given by `x^n/n!`.  -/
DividedPowers.OfInvertibleFactorial.dpow : {A : Type u_1} → [inst : CommSemiring A] → (I : Ideal A) → [DecidablePred fun x => x ∈ I] → ℕ → A → A
-- Init.Data.List.MinMax
List.min?_replicate_of_pos : ∀ {α : Type u_1} [inst : Min α] [Std.MinEqOr α] {n : ℕ} {a : α}, 0 < n → (List.replicate n a).min? = some a
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.testAgainstNN_zero : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω),
  μ.testAgainstNN 0 = 0
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.Hom.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M₁ M₂ : PresheafOfModules R} [inst_1 : SizeOf C] (app : (X : Cᵒᵖ) → M₁.obj X ⟶ M₂.obj X)
  (naturality :
    autoParam
      (∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
        CategoryTheory.CategoryStruct.comp (M₁.map f)
            ((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (app Y)) =
          CategoryTheory.CategoryStruct.comp (app X) (M₂.map f))
      PresheafOfModules.Hom.naturality._autoParam),
  sizeOf { app := app, naturality := naturality } = 1
-- Mathlib.Algebra.Homology.ComplexShape
ComplexShape.subsingleton_next : ∀ {ι : Type u_1} (c : ComplexShape ι) (i : ι), Subsingleton { j // c.Rel i j }
-- Mathlib.Data.Finsupp.Order
Finsupp.single_nonpos : ∀ {ι : Type u_1} {α : Type u_3} [inst : Zero α] [inst_1 : Preorder α] {i : ι} {a : α}, (fun₀ | i => a) ≤ 0 ↔ a ≤ 0
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.limNthHom.congr_simp : ∀ {R : Type u_1} [inst : NonAssocSemiring R] {p : ℕ} {f f_1 : (k : ℕ) → R →+* ZMod (p ^ k)} (e_f : f = f_1)
  [hp_prime : Fact (Nat.Prime p)]
  (f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1) (r r_1 : R),
  r = r_1 → PadicInt.limNthHom f_compat r = PadicInt.limNthHom ⋯ r_1
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.Matroidᵣ.ext : ∀ {α : Type u_2} {x y : Matroid.Matroidᵣ α}, x.toMatroid = y.toMatroid → x = y
-- Mathlib.Data.Int.Init
Int.leInductionDown.eq_1 : ∀ {m : ℤ} {motive : (n : ℤ) → n ≤ m → Sort u_1} (base : motive m ⋯)
  (pred : (n : ℤ) → (hnm : n ≤ m) → motive n hnm → motive (n - 1) ⋯) (n : ℤ),
  Int.leInductionDown base pred n =
    Int.inductionOn' (motive := fun x => (hnm : x ≤ m) → motive x hnm) n m (fun x => base) (fun x x_1 x_2 x_3 => ⋯.elim)
      fun k hle ih x => pred k hle (ih hle)
-- Init.Data.Nat.Internal.SOM
_private.Init.Data.Nat.Internal.SOM.0.Nat.Internal.SOM.Poly.mul.eq_1 : ∀ (p₁ p₂ : Nat.Internal.SOM.Poly), p₁.mul p₂ = Nat.Internal.SOM.Poly.mul.go✝ p₂ p₁ []
-- Mathlib.Topology.Algebra.InfiniteSum.Ring
Summable.tsum_pow_mul_one_sub : ∀ {α : Type u_3} [inst : Ring α] [inst_1 : TopologicalSpace α] [IsTopologicalRing α] [T2Space α] {x : α},
  (Summable fun x_1 => x ^ x_1) → (∑' (i : ℕ), x ^ i) * (1 - x) = 1
-- Aesop.Frontend.Tactic
_private.Aesop.Frontend.Tactic.0.Aesop.Frontend.TacticConfig.parse.addClause : Lean.MVarId →
  Bool →
    Lean.TSyntax `Aesop.tactic_clause → StateRefT' IO.RealWorld Aesop.Frontend.TacticConfig Lean.Elab.TermElabM Unit
-- Mathlib.Topology.Category.CompHausLike.Basic
CompHausLike.ofHom_comp : ∀ (P : TopCat → Prop) {X : Type u} [inst : TopologicalSpace X] [inst_1 : CompactSpace X] [inst_2 : T2Space X]
  [inst_3 : CompHausLike.HasProp P X] {Y : Type u} [inst_4 : TopologicalSpace Y] [inst_5 : CompactSpace Y]
  [inst_6 : T2Space Y] [inst_7 : CompHausLike.HasProp P Y] {Z : Type u} [inst_8 : TopologicalSpace Z]
  [inst_9 : CompactSpace Z] [inst_10 : T2Space Z] [inst_11 : CompHausLike.HasProp P Z] (f : C(X, Y)) (g : C(Y, Z)),
  CompHausLike.ofHom P (g.comp f) = CategoryTheory.CategoryStruct.comp (CompHausLike.ofHom P f) (CompHausLike.ofHom P g)
-- Mathlib.Topology.Closure
isClosed_of_closure_subset : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, closure s ⊆ s → IsClosed s
-- Mathlib.Algebra.Group.Subsemigroup.Basic
/-- Additive subsemigroup closure of a set is monotone in its
argument: if `s ⊆ t`, then `closure s ≤ closure t`  -/
AddSubsemigroup.closure_mono : ∀ {M : Type u_1} [inst : Add M] ⦃s t : Set M⦄, s ⊆ t → AddSubsemigroup.closure s ≤ AddSubsemigroup.closure t
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.equivOfUnique_apply : ∀ (p : ENNReal) (𝕜 : Type u_1) {ι : Type u_2} (β : ι → Type u_4) [inst : Semiring 𝕜]
  [inst_1 : (i : ι) → AddCommGroup (β i)] [inst_2 : (i : ι) → Module 𝕜 (β i)]
  [inst_3 : (i : ι) → TopologicalSpace (β i)] [inst_4 : Unique ι] (x : PiLp p β),
  (PiLp.equivOfUnique p 𝕜 β) x = x.ofLp default
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
/-- The underlying function.

Do NOT use directly. Use the coercion instead.  -/
SchwartzMap.toFun : {E : Type u_5} →
  {F : Type u_6} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        [inst_2 : NormedAddCommGroup F] → [inst_3 : NormedSpace ℝ F] → SchwartzMap E F → E → F
-- Mathlib.Analysis.Normed.Group.InfiniteSum
cauchySeq_finset_of_summable_norm : ∀ {ι : Type u_1} {E : Type u_3} [inst : SeminormedAddCommGroup E] {f : ι → E},
  (Summable fun a => ‖f a‖) → CauchySeq fun s => ∑ a ∈ s, f a
-- Mathlib.GroupTheory.Subgroup.Centralizer
AddSubgroup.mem_centralizer_iff_addCommutator_eq_zero' : ∀ {G : Type u_1} [inst : AddGroup G] {g : G} {s : Set G}, g ∈ AddSubgroup.centralizer s ↔ ∀ h ∈ s, ⁅g, h⁆ = 0
-- Mathlib.Topology.LocallyConstant.Basic
LocallyConstant.congr_fun : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {f g : LocallyConstant X Y}, f = g → ∀ (x : X), f x = g x
-- Mathlib.CategoryTheory.Adjunction.PartialAdjoint
CategoryTheory.Functor.partialLeftAdjoint_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor D C) {X Y : F.PartialLeftAdjointSource} (f : X ⟶ Y),
  F.partialLeftAdjoint.map f = F.partialLeftAdjointMap f
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.liftAddHom_singleAddHom : ∀ {α : Type u_1} {M : Type u_8} [inst : AddCommMonoid M],
  Finsupp.liftAddHom Finsupp.singleAddHom = AddMonoidHom.id (α →₀ M)
-- Mathlib.Topology.Instances.EReal.Lemmas
EReal.isEmbedding_coe : Topology.IsEmbedding Real.toEReal
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point.0.WeierstrassCurve.Affine.Point.add.match_1.eq_1 : ∀ {F : Type u_1} [inst : Field F] {W : WeierstrassCurve.Affine F} (motive : W.Point → W.Point → Sort u_2) (P : W.Point)
  (h_1 : (P : W.Point) → motive WeierstrassCurve.Affine.Point.zero P)
  (h_2 : (P : W.Point) → motive P WeierstrassCurve.Affine.Point.zero)
  (h_3 :
    (x₁ y₁ : F) →
      (h₁ : W.Nonsingular x₁ y₁) →
        (x₂ y₂ : F) →
          (h₂ : W.Nonsingular x₂ y₂) →
            motive (WeierstrassCurve.Affine.Point.some x₁ y₁ h₁) (WeierstrassCurve.Affine.Point.some x₂ y₂ h₂)),
  (match WeierstrassCurve.Affine.Point.zero, P with
    | WeierstrassCurve.Affine.Point.zero, P => h_1 P
    | P, WeierstrassCurve.Affine.Point.zero => h_2 P
    | WeierstrassCurve.Affine.Point.some x₁ y₁ h₁, WeierstrassCurve.Affine.Point.some x₂ y₂ h₂ =>
      h_3 x₁ y₁ h₁ x₂ y₂ h₂) =
    h_1 P
-- Mathlib.Topology.Compactification.OnePoint.Basic
/-- If `X` is an infinite type with discrete topology (e.g., `ℕ`), then the identity map from
`CofiniteTopology (OnePoint X)` to `OnePoint X` is not continuous.  -/
OnePoint.not_continuous_cofiniteTopology_of_symm : ∀ {X : Type u_1} [inst : TopologicalSpace X] [Infinite X] [DiscreteTopology X], ¬Continuous ⇑CofiniteTopology.of.symm
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.toReal_add_of_sign_eq_neg_sign : ∀ {θ ψ : Real.Angle}, θ ≠ ↑Real.pi ∨ ψ ≠ ↑Real.pi → θ.sign = -ψ.sign → (θ + ψ).toReal = θ.toReal + ψ.toReal
-- Mathlib.Topology.Order.AtTopBotIxx
comap_coe_Ioi_nhdsGT : ∀ {X : Type u_1} [inst : LinearOrder X] [inst_1 : TopologicalSpace X] [OrderTopology X] (a : X),
  autoParam (Order.IsPredPrelimit a) comap_coe_Ioi_nhdsGT._auto_1 →
    Filter.comap Subtype.val (nhdsWithin a (Set.Ioi a)) = Filter.atBot
-- Mathlib.Order.IsNormal
Order.isNormal_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : α → β},
  Order.IsNormal f ↔ StrictMono f ∧ ∀ (o : α), Order.IsSuccLimit o → ∀ (a : β), (∀ b < o, f b ≤ a) → f o ≤ a
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.pow.sizeOf_spec : ∀ (ka : ℤ) (ca? : Option Lean.Meta.Grind.Arith.Cutsat.EqCnstr) (kb : ℕ)
  (cb? : Option Lean.Meta.Grind.Arith.Cutsat.EqCnstr),
  sizeOf (Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.pow ka ca? kb cb?) =
    1 + sizeOf ka + sizeOf ca? + sizeOf kb + sizeOf cb?
-- Lean.Meta.Sym.LitValues
Lean.Meta.Sym.FinValue.mk.sizeOf_spec : ∀ (n : ℕ) (val : Fin n), sizeOf { n := n, val := val } = 1 + sizeOf n + sizeOf val
-- Mathlib.Topology.MetricSpace.Basic
/-- Build new pseudometric space from an old one where the distance is provably (but typically
non-definitionally) equal to some given distance. We also provide convenience versions for
PseudoEMetric, Emetric and Metric spaces.  -/
PseudoMetricSpace.replaceDist : {X : Type u_2} → (m : PseudoMetricSpace X) → (d : X → X → ℝ) → d = dist → PseudoMetricSpace X
-- Mathlib.Algebra.Ring.Hom.Defs
RingHom.coe_monoidHom_id : ∀ {α : Type u_2} {x : NonAssocSemiring α}, ↑(RingHom.id α) = MonoidHom.id α
-- Mathlib.Util.Superscript
Mathlib.Tactic.Superscript.instInhabitedMapping.default : Mathlib.Tactic.Superscript.Mapping
-- Mathlib.Data.Set.Function
Set.SurjOn.extendDomain : ∀ {α : Type u_1} {β : Type u_2} {p : β → Prop} [inst : DecidablePred p] {f : α ≃ Subtype p} {g : Equiv.Perm α}
  {s t : Set α}, Set.SurjOn (⇑g) s t → Set.SurjOn (⇑(g.extendDomain f)) (Subtype.val ∘ ⇑f '' s) (Subtype.val ∘ ⇑f '' t)
-- Mathlib.Topology.MetricSpace.Cauchy
Metric.exists_subseq_bounded_of_cauchySeq : ∀ {α : Type u} [inst : PseudoMetricSpace α] (u : ℕ → α),
  CauchySeq u →
    ∀ (b : ℕ → ℝ), (∀ (n : ℕ), 0 < b n) → ∃ f, StrictMono f ∧ ∀ (n m : ℕ), m ≥ f n → dist (u m) (u (f n)) < b n
-- Mathlib.GroupTheory.Torsion
/-- A torsion additive monoid is isomorphic to its torsion additive submonoid.  -/
IsAddTorsion.torsionAddEquiv : {G : Type u_1} → [inst : AddCommMonoid G] → IsAddTorsion G → ↥(AddCommMonoid.addTorsion G) ≃+ G