mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Kleene
IdemCommSemiring.toSemilatticeSup : {α : Type u_5} → [self : IdemCommSemiring α] → SemilatticeSup α
-- Mathlib.NumberTheory.LSeries.Nonvanishing
_private.Mathlib.NumberTheory.LSeries.Nonvanishing.0.DirichletCharacter.BadChar.mk.sizeOf_spec : ∀ {N : ℕ} [inst : NeZero N] (χ : DirichletCharacter ℂ N) (χ_ne : χ ≠ 1) (χ_sq : χ ^ 2 = 1)
  (hχ : DirichletCharacter.LFunction χ 1 = 0),
  sizeOf { χ := χ, χ_ne := χ_ne, χ_sq := χ_sq, hχ := hχ } = 1 + sizeOf χ + sizeOf χ_sq + sizeOf hχ
-- Lean.Data.AssocList
Lean.instInhabitedAssocList.default : {α : Type u} → {β : Type v} → Lean.AssocList α β
-- Mathlib.Algebra.Lie.IdealOperations
LieSubmodule.mono_lie : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] {N N' : LieSubmodule R L M} [inst_5 : LieAlgebra R L]
  {I J : LieIdeal R L}, I ≤ J → N ≤ N' → ⁅I, N⁆ ≤ ⁅J, N'⁆
-- Mathlib.Topology.Compactness.Lindelof
Filter.coclosedLindelof.eq_1 : ∀ (X : Type u_2) [inst : TopologicalSpace X],
  Filter.coclosedLindelof X = ⨅ s, ⨅ (_ : IsClosed s), ⨅ (_ : IsLindelof s), Filter.principal sᶜ
-- Mathlib.LinearAlgebra.Determinant
LinearMap.det_toLin' : ∀ {R : Type u_1} [inst : CommRing R] {ι : Type u_4} [inst_1 : DecidableEq ι] [inst_2 : Fintype ι] (f : Matrix ι ι R),
  LinearMap.det (Matrix.toLin' f) = f.det
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.ext_iff : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {h h' : X ≃ₜ Y},
  h = h' ↔ ∀ (x : X), h x = h' x
-- Init.Data.List.Basic
/-- Creates a list that contains `n` copies of `a`.

* `List.replicate 5 "five" = ["five", "five", "five", "five", "five"]`
* `List.replicate 0 "zero" = []`
* `List.replicate 2 ' ' = [' ', ' ']`
 -/
List.replicate : {α : Type u} → ℕ → α → List α
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.cosimplicialSimplicialEquiv_functor_obj_obj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (F : (CategoryTheory.Functor SimplexCategory C)ᵒᵖ)
  (X : SimplexCategoryᵒᵖ),
  ((CategoryTheory.cosimplicialSimplicialEquiv C).functor.obj F).obj X =
    Opposite.op ((Opposite.unop F).obj (Opposite.unop X))
-- Mathlib.Order.UpperLower.Basic
IsLowerSet.total : ∀ {α : Type u_1} [inst : LinearOrder α] {s t : Set α}, IsLowerSet s → IsLowerSet t → s ⊆ t ∨ t ⊆ s
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyData.ofIso_right_Q : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (e : S₁ ≅ S₂) (h : S₁.HomologyData),
  (CategoryTheory.ShortComplex.HomologyData.ofIso e h).right.Q = h.right.Q
-- Mathlib.Algebra.Group.UniqueProds.Basic
/-- Let `G` be a Type with multiplication, let `A B : Finset G` be finite subsets and
let `a0 b0 : G` be two elements.  `UniqueMul A B a0 b0` asserts `a0 * b0` can be written in at
most one way as a product of an element of `A` and an element of `B`.  -/
UniqueMul : {G : Type u_1} → [Mul G] → Finset G → Finset G → G → G → Prop
-- Mathlib.Order.BooleanAlgebra.Defs
PUnit.instBooleanAlgebra : BooleanAlgebra PUnit.{u_2 + 1}
-- Mathlib.RingTheory.RingHom.QuasiFinite
RingHom.QuasiFinite.of_comp : ∀ {T : Type u_3} [inst : CommRing T] {R : Type u_4} {S : Type u_5} [inst_1 : CommRing R] [inst_2 : CommRing S]
  {f : S →+* T} {g : R →+* S}, (f.comp g).QuasiFinite → f.QuasiFinite
-- Mathlib.Algebra.Group.Pi.Lemmas
Pi.mulSingle_comp_equiv : ∀ {α : Type u_2} {m : Type u_5} {n : Type u_6} [inst : DecidableEq n] [inst_1 : DecidableEq m] [inst_2 : One α]
  (σ : n ≃ m) (i : m) (x : α), Pi.mulSingle i x ∘ ⇑σ = Pi.mulSingle (σ.symm i) x
-- Mathlib.Analysis.Normed.Lp.WithLp
/-- `WithLp.ofLp` and `WithLp.toLp` as an equivalence.  -/
WithLp.equiv : (p : ENNReal) → (V : Type u_4) → WithLp p V ≃ V
-- Init.Data.Option.Lemmas
Option.pbind_join : ∀ {α : Type u_1} {β : Type u_2} {o : Option (Option α)} {f : (a : α) → o.join = some a → Option β},
  o.join.pbind f = o.pbind fun o' ho' => o'.pbind fun a ha => f a ⋯
-- Mathlib.Data.Nat.Totient
Nat.totient_two_mul_of_even : ∀ {n : ℕ}, Even n → (2 * n).totient = 2 * n.totient
-- Mathlib.Order.Antisymmetrization
/-- `Antisymmetrization` and `orderDual` commute.  -/
OrderIso.dualAntisymmetrization : (α : Type u_1) →
  [inst : Preorder α] → (Antisymmetrization α fun x1 x2 => x1 ≤ x2)ᵒᵈ ≃o Antisymmetrization αᵒᵈ fun x1 x2 => x1 ≤ x2
-- Mathlib.CategoryTheory.Galois.Topology
CategoryTheory.PreGaloisCategory.obj_discreteTopology : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) (X : C),
  DiscreteTopology (F.obj X).obj
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.getD_eq_of_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  {k fallback : α}, t.contains k = true → t.getD k fallback = k
-- Init.Classical
Classical.exists_true_of_nonempty : ∀ {α : Sort u}, Nonempty α → ∃ x, True
-- Mathlib.CategoryTheory.Groupoid
CategoryTheory.Groupoid.mk : {obj : Type u} →
  [toCategory : CategoryTheory.Category.{v, u} obj] →
    (inv : {X Y : obj} → (X ⟶ Y) → (Y ⟶ X)) →
      autoParam
          (∀ {X Y : obj} (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (inv f) f = CategoryTheory.CategoryStruct.id Y)
          CategoryTheory.Groupoid.inv_comp._autoParam →
        autoParam
            (∀ {X Y : obj} (f : X ⟶ Y),
              CategoryTheory.CategoryStruct.comp f (inv f) = CategoryTheory.CategoryStruct.id X)
            CategoryTheory.Groupoid.comp_inv._autoParam →
          CategoryTheory.Groupoid obj
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.monotone : ∀ {α : Type u_3} {E : α → Type u_4} [inst : (i : α) → NormedAddCommGroup (E i)] {p q : ENNReal}, q ≤ p → lp E q ≤ lp E p
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.monomial_zero_eq_C : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R], ⇑(MvPowerSeries.monomial 0) = ⇑MvPowerSeries.C
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp₁.hom_mkHom : ∀ {M N : Type u} [inst : SeminormedAddCommGroup M] [inst_1 : SeminormedAddCommGroup N] (f : NormedAddGroupHom M N)
  (hf : f.NormNoninc), ↑(SemiNormedGrp₁.Hom.hom (SemiNormedGrp₁.mkHom f hf)) = f
-- Mathlib.NumberTheory.ArithmeticFunction.Moebius
ArithmeticFunction.moebius_sq_eq_one_of_squarefree : ∀ {l : ℕ}, Squarefree l → ArithmeticFunction.moebius l ^ 2 = 1
-- Mathlib.Topology.Order.OrderClosed
eventually_lt_nhds : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIciTopology α] {a b : α},
  a < b → ∀ᶠ (x : α) in nhds a, x < b
-- Mathlib.Algebra.Order.ToIntervalMod
toIocMod_sub_self_eq_mul : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R), toIocMod hp a b - b = -↑(toIocDiv hp a b) * p
-- Mathlib.CategoryTheory.GuitartExact.Basic
CategoryTheory.TwoSquare.costructuredArrowRightwards_obj : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃}
  {R : CategoryTheory.Functor C₂ C₄} {B : CategoryTheory.Functor C₃ C₄} (w : CategoryTheory.TwoSquare T L R B) (X₃ : C₃)
  (X : CategoryTheory.CostructuredArrow L X₃),
  (w.costructuredArrowRightwards X₃).obj X =
    (CategoryTheory.CostructuredArrow.pre T R (B.obj X₃)).obj
      ((CategoryTheory.Comma.mapLeft (CategoryTheory.Functor.fromPUnit (B.obj X₃)) w).obj
        (CategoryTheory.CostructuredArrow.mk (B.map X.hom)))
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.tendsto_coe_nhds_top : ∀ {α : Type u_1} {f : α → NNReal} {l : Filter α},
  Filter.Tendsto (fun x => ↑(f x)) l (nhds ⊤) ↔ Filter.Tendsto f l Filter.atTop
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
/-- The transpose of a matrix in `SL(n, R)`  -/
Matrix.SpecialLinearGroup.«term_ᵀ» : Lean.TrailingParserDescr
-- Mathlib.Data.Finset.Image
Finset.filter_attach' : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α) (p : ↥s → Prop) [inst_1 : DecidablePred p],
  Finset.filter p s.attach =
    Finset.map { toFun := Subtype.map id ⋯, inj' := ⋯ } {x ∈ s | ∃ (h : x ∈ s), p ⟨x, h⟩}.attach
-- Init.Data.Rat.Lemmas
Rat.floor_def : ∀ (a : ℚ), a.floor = a.num / ↑a.den
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.one_sub_X_sq_mul_derivative_derivative_T_eq_poly_in_T : ∀ {R : Type u_1} [inst : CommRing R] (n : ℤ),
  (1 - Polynomial.X ^ 2) * (⇑Polynomial.derivative)^[2] (Polynomial.Chebyshev.T R n) =
    Polynomial.X * Polynomial.derivative (Polynomial.Chebyshev.T R n) - ↑n ^ 2 * Polynomial.Chebyshev.T R n
-- Mathlib.Logic.Relation
/-- **Alias** of `Relation.TransGen.stdSymm`. -/
Relation.TransGen.symmetric : ∀ {α : Type u_1} {r : α → α → Prop} [Std.Symm r], Std.Symm (Relation.TransGen r)
-- Init.Data.Repr
instReprRaw : Repr String.Pos.Raw
-- Mathlib.RingTheory.FreeRing
FreeRing.hom_ext : ∀ {α : Type u} {R : Type v} [inst : Ring R] ⦃f g : FreeRing α →+* R⦄,
  (∀ (x : α), f (FreeRing.of x) = g (FreeRing.of x)) → f = g
-- Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
SSet.σ_mem_degenerate : ∀ (X : SSet) {n : ℕ} (i : Fin (n + 1)) (x : X.obj (Opposite.op { len := n })),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.σ X i)) x ∈ X.degenerate (n + 1)
-- Mathlib.Analysis.Calculus.ContDiff.Comp
/-- The composition of `C^n` functions on domains is `C^n`.  -/
ContDiffOn.comp_inter : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {n : WithTop ℕ∞} {s : Set E} {t : Set F} {g : F → G}
  {f : E → F}, ContDiffOn 𝕜 n g t → ContDiffOn 𝕜 n f s → ContDiffOn 𝕜 n (g ∘ f) (s ∩ f ⁻¹' t)
-- Std.Do.SPred.SPred
Std.Do.SPred.pure_nil : ∀ {P : Prop}, ⌜P⌝ = { down := P }
-- Mathlib.Data.FunLike.Group
/-- A `FunLike` type that satisfies `(f * g) x = f x * g x` has right cancellative multiplication if
`β` has right cancellative multiplication.  -/
FunLike.isRightCancelMul : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Mul F] [inst_2 : Mul β]
  [IsRightCancelMul β] [IsMulApply F α β], IsRightCancelMul F
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
MeasureTheory.MemLp.condExp : ∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_2} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : α → E} {p : ENNReal},
  1 ≤ p → MeasureTheory.MemLp f p μ → MeasureTheory.MemLp μ[f | m] p μ
-- Mathlib.Order.Monotone.Monovary
monovary_id_iff : ∀ {ι : Type u_1} {α : Type u_3} [inst : Preorder α] {f : ι → α} [inst_1 : PartialOrder ι], Monovary f id ↔ Monotone f
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.powC.induct_unfolding : ∀ (p : Lean.Grind.CommRing.Poly) (c : ℕ) (motive : ℕ → Lean.Grind.CommRing.Poly → Prop),
  motive 0 (Lean.Grind.CommRing.Poly.num 1) →
    motive 1 p →
      (∀ (k : ℕ), (k = 0 → False) → motive k (p.powC k c) → motive k.succ (p.mulC (p.powC k c) c)) →
        ∀ (k : ℕ), motive k (p.powC k c)
-- Batteries.Data.Vector.Lemmas
Vector.tail_eq_of_ne_zero : ∀ {n : ℕ} {α : Type u_1} [inst : NeZero n] {v : Vector α n}, v.tail = v.eraseIdx 0 ⋯
-- Mathlib.RingTheory.Ideal.Quotient.Defs
Ideal.Quotient.factor.congr_simp : ∀ {R : Type u} [inst : Ring R] {S T : Ideal R} [inst_1 : S.IsTwoSided] [inst_2 : T.IsTwoSided] (H : S ≤ T),
  Ideal.Quotient.factor H = Ideal.Quotient.factor H
-- Mathlib.Order.GaloisConnection.Defs
/-- Make a `GaloisCoinsertion` between `α` and `β` from a `GaloisInsertion` between `αᵒᵈ`
and `βᵒᵈ`.  -/
GaloisInsertion.ofDual : {α : Type u} →
  {β : Type v} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] →
        {u : αᵒᵈ → βᵒᵈ} →
          {l : βᵒᵈ → αᵒᵈ} →
            GaloisInsertion l u →
              GaloisCoinsertion (⇑OrderDual.ofDual ∘ u ∘ ⇑OrderDual.toDual) (⇑OrderDual.ofDual ∘ l ∘ ⇑OrderDual.toDual)
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.toSnowflaking_comp_ofSnowflaking : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1},
  ⇑Metric.Snowflaking.toSnowflaking ∘ ⇑Metric.Snowflaking.ofSnowflaking = id
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.ofFn.go.eq_2 : ∀ {α : Type u} {n : ℕ} (f : Fin n → α) (acc : Array α) (x_2 : 0 ≤ n), Array.ofFn.go✝ f acc 0 x_2 = acc
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
integral_cos_pow_three : ∀ {a b : ℝ}, ∫ (x : ℝ) in a..b, Real.cos x ^ 3 = Real.sin b - Real.sin a - (Real.sin b ^ 3 - Real.sin a ^ 3) / 3
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
/-- The preimage in `X` of a basic open in `Spec Γ(X)` (as an open set).  -/
AlgebraicGeometry.LocallyRingedSpace.toΓSpecMapBasicOpen : (X : AlgebraicGeometry.LocallyRingedSpace) →
  ↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X)) → TopologicalSpace.Opens ↑X.toTopCat
-- Mathlib.Topology.Algebra.Monoid
Pi.continuousMul : ∀ {ι : Type u_1} {C : ι → Type u_6} [inst : (i : ι) → TopologicalSpace (C i)] [inst_1 : (i : ι) → Mul (C i)]
  [∀ (i : ι), ContinuousMul (C i)], ContinuousMul ((i : ι) → C i)
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.ResolveSimpIdResult.simproc : Lean.Name → Lean.Elab.Tactic.ResolveSimpIdResult
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.takeWhileTR.go.match_1.splitter : {α : Type u_1} →
  (motive : List α → Array α → Sort u_2) →
    (x : List α) →
      (x_1 : Array α) →
        ((x : Array α) → motive [] x) →
          ((a : α) → (as : List α) → (acc : Array α) → motive (a :: as) acc) → motive x x_1
-- Mathlib.Algebra.Category.Grp.Basic
AddGrpCat.instZeroHom : (G H : AddGrpCat) → Zero (G ⟶ H)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
/-- Use `getVert_eq_support_getElem` to rewrite in the reverse direction.  -/
SimpleGraph.Walk.support_getElem_eq_getVert : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {n : ℕ} (p : G.Walk u v) (h : n < p.support.length),
  p.support[n] = p.getVert n
-- Mathlib.FieldTheory.RatFunc.Luroth
_private.Mathlib.FieldTheory.RatFunc.Luroth.0.RatFunc.Luroth.b_ne_zero : ∀ {K : Type u_1} [inst : Field K] {E : IntermediateField K (RatFunc K)}, RatFunc.Luroth.b✝ E ≠ 0
-- Mathlib.CategoryTheory.Equivalence.Symmetry
CategoryTheory.Equivalence.symmEquivInverse_obj_counitIso_hom : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] (D : Type u_2)
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (X : (D ≌ C)ᵒᵖ),
  ((CategoryTheory.Equivalence.symmEquivInverse C D).obj X).counitIso.hom = (Opposite.unop X).unitIso.inv
-- Mathlib.Order.Hom.CompleteLattice
FrameHom.ext : ∀ {α : Type u_2} {β : Type u_3} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] {f g : FrameHom α β},
  (∀ (a : α), f a = g a) → f = g
-- Mathlib.Order.WithBot
WithBot.toDual_bot : ∀ {α : Type u_1}, WithBot.toDual ⊥ = ⊤
-- Mathlib.Algebra.Order.UpperLower
LowerSet.commSemigroup.eq_1 : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : Preorder α] [inst_2 : IsOrderedMonoid α],
  LowerSet.commSemigroup = Function.Injective.commSemigroup SetLike.coe ⋯ ⋯
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
/-- Orthogonal submodules are disjoint.  -/
Submodule.IsOrtho.disjoint : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {U V : Submodule 𝕜 E}, U ⟂ V → Disjoint U V
-- Mathlib.LinearAlgebra.Ray
/-- The action via `LinearEquiv.apply_distribMulAction` corresponds to `Module.Ray.map`.  -/
Module.Ray.linearEquiv_smul_eq_map : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] (e : M ≃ₗ[R] M) (v : Module.Ray R M), e • v = (Module.Ray.map e) v
-- Init.NotationExtra
Lean.«command__Unif_hint____Where_|_-⊢__» : Lean.ParserDescr
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- See also `pow_left_strictMono₀` and `Nat.pow_left_strictMono`.  -/
pow_left_strictMonoOn₀ : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : PartialOrder M₀] {n : ℕ} [PosMulStrictMono M₀] [MulPosMono M₀],
  n ≠ 0 → StrictMonoOn (fun x => x ^ n) {a | 0 ≤ a}
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.coe_toAddMonoidHom : ∀ {α : Type u_5} [inst : NonUnitalNonAssocSemiring α] (f : CentroidHom α), ⇑↑f = ⇑f
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
/-- Typecheck a `ContinuousAddMonoidHom` as a morphism in `ProfiniteAddGrp`.  -/
ProfiniteAddGrp.ofHom : {X Y : Type u} →
  [inst : AddGroup X] →
    [inst_1 : TopologicalSpace X] →
      [inst_2 : IsTopologicalAddGroup X] →
        [inst_3 : CompactSpace X] →
          [inst_4 : TotallyDisconnectedSpace X] →
            [inst_5 : AddGroup Y] →
              [inst_6 : TopologicalSpace Y] →
                [inst_7 : IsTopologicalAddGroup Y] →
                  [inst_8 : CompactSpace Y] →
                    [inst_9 : TotallyDisconnectedSpace Y] → (X →ₜ+ Y) → (ProfiniteAddGrp.of X ⟶ ProfiniteAddGrp.of Y)
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.locallyIntegrableOn_const : ∀ {X : Type u_1} {E : Type u_6} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure X} {s : Set X} [MeasureTheory.IsLocallyFiniteMeasure μ] (c : E),
  MeasureTheory.LocallyIntegrableOn (fun x => c) s μ
-- Mathlib.Algebra.MvPolynomial.Equiv
/-- The `MvPolynomial.degreeOf` of a particular variable in a multivariate polynomial
is equal to the `Polynomial.natDegree` of the single-variable polynomial
obtained by treating the multivariable polynomial as a single variable polynomial
over multivariable polynomials in the remaining variables
 -/
MvPolynomial.degreeOf_eq_natDegree : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : DecidableEq σ] (a : σ) (p : MvPolynomial σ R),
  MvPolynomial.degreeOf a p =
    ((MvPolynomial.optionEquivLeft R { b // b ≠ a })
        ((MvPolynomial.rename ⇑(Equiv.optionSubtypeNe a).symm) p)).natDegree
-- Mathlib.Data.TypeVec
TypeVec.dropFun_of_subtype : ∀ {n : ℕ} {α : TypeVec.{u_1} (n + 1)} (p : α.Arrow (TypeVec.repeat (n + 1) Prop)),
  TypeVec.dropFun (TypeVec.ofSubtype p) = TypeVec.ofSubtype (TypeVec.dropFun p)
-- Lean.Parser.Basic
_private.Lean.Parser.Basic.0.Lean.Parser.finishCommentBlock.eoi : Bool → Lean.Parser.ParserState → Lean.Parser.ParserState
-- Mathlib.GroupTheory.Index
Subgroup.index_map_eq : ∀ {G : Type u_1} {G' : Type u_2} [inst : Group G] [inst_1 : Group G'] (H : Subgroup G) {f : G →* G'},
  Function.Surjective ⇑f → f.ker ≤ H → (Subgroup.map f H).index = H.index
-- Std.Data.HashSet.Lemmas
Std.HashSet.beq_iff_equiv : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [LawfulBEq α], (m₁ == m₂) = true ↔ m₁.Equiv m₂
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.ElabSimpArgResult.addSimproc.sizeOf_spec : ∀ («simproc» : Lean.Name) (post : Bool),
  sizeOf (Lean.Elab.Tactic.ElabSimpArgResult.addSimproc «simproc» post) = 1 + sizeOf «simproc» + sizeOf post
-- Mathlib.Topology.UniformSpace.Equicontinuity
EquicontinuousOn.mono : ∀ {ι : Type u_1} {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] {F : ι → X → α}
  {S T : Set X}, EquicontinuousOn F T → S ⊆ T → EquicontinuousOn F S
-- Mathlib.NumberTheory.ModularForms.LevelOne.Basic
ModularFormClass.levelOne_neg_weight_eq_zero : ∀ {F : Type u_1} [inst : FunLike F UpperHalfPlane ℂ] {k : ℤ}
  [ModularFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k], k < 0 → ∀ (f : F), ⇑f = 0
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.le_inf : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {A : C}
  (h f g : CategoryTheory.Subobject A), h ≤ f → h ≤ g → h ≤ (CategoryTheory.Subobject.inf.obj f).obj g
-- Mathlib.Topology.MetricSpace.GromovHausdorff
/-- A metric space representative of any abstract point in `GHSpace`  -/
GromovHausdorff.GHSpace.Rep : GromovHausdorff.GHSpace → Type
-- Lean.Elab.Calc
/-- A proof of `term`  -/
Lean.Elab.Term.CalcStepView.proof : Lean.Elab.Term.CalcStepView → Lean.Term
-- Batteries.Data.Array.Scan
Array.scanrM.loop.congr_simp : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] (f f_1 : α → β → m β),
  f = f_1 →
    ∀ (init init_1 : β),
      init = init_1 →
        ∀ (as as_1 : Array α) (e_as : as = as_1) (start start_1 : ℕ) (e_start : start = start_1) (stop stop_1 : ℕ),
          stop = stop_1 →
            ∀ (h_start : start ≤ as.size) (acc acc_1 : Array β),
              acc = acc_1 →
                Array.scanrM.loop f init as start stop h_start acc =
                  Array.scanrM.loop f_1 init_1 as_1 start_1 stop_1 ⋯ acc_1
-- Mathlib.Topology.MetricSpace.IsometricSMul
edist_add_right : ∀ {M : Type u} [inst : Add M] [inst_1 : PseudoEMetricSpace M] [IsIsometricVAdd Mᵃᵒᵖ M] (a b c : M),
  edist (a + c) (b + c) = edist a b
-- Mathlib.Algebra.Order.Field.Power
Odd.zpow_pos_iff : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a : α} {n : ℤ},
  Odd n → (0 < a ^ n ↔ 0 < a)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem?_toArray_roc_eq_some_iff : ∀ {k m n i : ℕ}, (m<...=n).toArray[i]? = some k ↔ i < n - m ∧ m + 1 + i = k
-- Mathlib.Combinatorics.Enumerative.Partition.GenFun
_private.Mathlib.Combinatorics.Enumerative.Partition.GenFun.0.Nat.Partition.aux_prod_coeff_eq_zero_of_notMem_range : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : TopologicalSpace R] [T2Space R] (f : ℕ → ℕ → R) {d : ℕ}
  {s : Finset ℕ},
  0 ∉ s →
    ∀ {g : ℕ →₀ ℕ},
      g ∈ s.finsuppAntidiag d →
        g ∉ Set.range Nat.Partition.toFinsuppAntidiag →
          ∏ i ∈ s, (PowerSeries.coeff (g i)) (1 + ∑' (j : ℕ), f i (j + 1) • PowerSeries.X ^ (i * (j + 1))) = 0
-- Mathlib.Order.Filter.Ultrafilter.Basic
Ultrafilter.finite_biUnion_mem_iff : ∀ {α : Type u} {β : Type v} {f : Ultrafilter α} {is : Set β} {s : β → Set α},
  is.Finite → (⋃ i ∈ is, s i ∈ f ↔ ∃ i ∈ is, s i ∈ f)
-- Lean.Data.JsonRpc
Lean.JsonRpc.MessageDirection.serverToClient.sizeOf_spec : sizeOf Lean.JsonRpc.MessageDirection.serverToClient = 1
-- Mathlib.Combinatorics.Matroid.Rank.Finite
Matroid.IsRkFinite.inter_ground : ∀ {α : Type u_1} {M : Matroid α} {X : Set α}, M.IsRkFinite X → M.IsRkFinite (X ∩ M.E)
-- Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
/-- The isomorphism `F.obj i ≅ F.obj j` induced by `φ : i ⟶ j`,
when `h : F.IsEventuallyConstantFrom i₀` and there exists a map `i₀ ⟶ i`.  -/
CategoryTheory.Functor.IsEventuallyConstantFrom.isoMap : {J : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C] →
        {F : CategoryTheory.Functor J C} →
          {i₀ : J} → F.IsEventuallyConstantFrom i₀ → {i j : J} → (i ⟶ j) → Nonempty (i₀ ⟶ i) → (F.obj i ≅ F.obj j)
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
/-- obvious triangles `X ⟶ X ⟶ 0 ⟶ X⟦1⟧` are distinguished  -/
CategoryTheory.Pretriangulated.contractible_distinguished : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.Limits.HasZeroObject C}
  {inst_2 : CategoryTheory.HasShift C ℤ} {inst_3 : CategoryTheory.Preadditive C}
  {inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive} [self : CategoryTheory.Pretriangulated C] (X : C),
  CategoryTheory.Pretriangulated.contractibleTriangle X ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
-- Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
/-- Legendre's doubling formula for the Gamma function, for positive real arguments. Note that
we shall later prove this for all `s` as `Real.Gamma_mul_Gamma_add_half` (superseding this result)
but this result is needed as an intermediate step.  -/
Real.Gamma_mul_Gamma_add_half_of_pos : ∀ {s : ℝ}, 0 < s → Real.Gamma s * Real.Gamma (s + 1 / 2) = Real.Gamma (2 * s) * 2 ^ (1 - 2 * s) * √Real.pi