mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Subsemigroup.Basic
/-- An induction principle for closure membership. If `p` holds for all elements of `s`, and
is preserved under multiplication, then `p` holds for all elements of the closure of `s`.  -/
Subsemigroup.closure_induction : ∀ {M : Type u_1} [inst : Mul M] {s : Set M} {p : (x : M) → x ∈ Subsemigroup.closure s → Prop},
  (∀ (x : M) (h : x ∈ s), p x ⋯) →
    (∀ (x y : M) (hx : x ∈ Subsemigroup.closure s) (hy : y ∈ Subsemigroup.closure s), p x hx → p y hy → p (x * y) ⋯) →
      ∀ {x : M} (hx : x ∈ Subsemigroup.closure s), p x hx
-- Init.Data.Fin.Lemmas
Fin.val_lt_last : ∀ {n : ℕ} {i : Fin (n + 1)}, i ≠ Fin.last n → ↑i < n
-- Mathlib.Topology.Algebra.InfiniteSum.Group
Summable.hasFiniteSupport_of_discreteTopology : ∀ {α : Type u_5} [inst : AddCommGroup α] [inst_1 : TopologicalSpace α] [DiscreteTopology α] {β : Type u_6} (f : β → α),
  Summable f → Function.HasFiniteSupport f
-- Mathlib.Analysis.Real.Sqrt
Real.sqrt_sq : ∀ {x : ℝ}, 0 ≤ x → √(x ^ 2) = x
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.hom_ext_iff : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆}
  [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} {θ θ' : ψ ⟶ ψ'},
  θ = θ' ↔ θ.left = θ'.left ∧ θ.right = θ'.right ∧ θ.base = θ'.base
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.LocalInvariantProp.liftProp_id : ∀ {H : Type u_1} {M : Type u_2} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M]
  {G : StructureGroupoid H} {Q : (H → H) → Set H → H → Prop},
  G.LocalInvariantProp G Q → (∀ (y : H), Q id Set.univ y) → ChartedSpace.LiftProp Q id
-- Mathlib.AlgebraicTopology.SimplicialComplex.Basic
AbstractSimplicialComplex.top_toPreAbstractSimplicialComplex : ∀ {ι : Type u_1}, ⊤.toPreAbstractSimplicialComplex = ⊤
-- Init.Data.Iterators.Basic
/-- A variant of `IterStep` that bundles the step together with a proof that it is "plausible".
The plausibility predicate will later be chosen to assert that a state is a plausible successor
of another state. Having this proof bundled up with the step is important for termination proofs.

See `IterM.Step` and `Iter.Step` for the concrete choice of the plausibility predicate.
 -/
Std.PlausibleIterStep : {α : Type u} → {β : Type w} → (Std.IterStep α β → Prop) → Type (max 0 u w)
-- Init.Data.String.FindPos
/-- Returns the previous valid position before the given position, or `none` if the position is
the start position.  -/
String.Pos.prev? : {s : String} → s.Pos → Option s.Pos
-- Mathlib.NumberTheory.Real.GoldenRatio
/-- The golden ratio is irrational.  -/
Real.goldenRatio_irrational : Irrational Real.goldenRatio
-- Mathlib.Algebra.Order.WithTop.Untop0
WithTop.untop₀_zero : ∀ {α : Type u_1} [inst : Zero α], WithTop.untop₀ 0 = 0
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.hom_inv_id_tensor'_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {V W X Y Z : C}
  (f : V ⟶ W) [inst_2 : CategoryTheory.IsIso f] (g : X ⟶ Y) (h : Y ⟶ Z) {Z_1 : C}
  (h_1 : CategoryTheory.MonoidalCategoryStruct.tensorObj V Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.inv f) h)
        h_1) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id V) g)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id V) h) h_1)
-- Mathlib.Algebra.Ring.Int.Parity
/-- **Alias** of the reverse direction of `Int.natAbs_odd`. -/
Odd.natAbs : ∀ {n : ℤ}, Odd n → Odd n.natAbs
-- Mathlib.MeasureTheory.Measure.EverywherePos
MeasureTheory.Measure.IsEverywherePos.smul_measure : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α},
  μ.IsEverywherePos s → ∀ {c : ENNReal}, c ≠ 0 → (c • μ).IsEverywherePos s
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.RightResolution.Hom.comm : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂}
  {R R' : Φ.RightResolution X₂} (self : R.Hom R'), CategoryTheory.CategoryStruct.comp R.w (Φ.functor.map self.f) = R'.w
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.liftAux.eq_1 : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] {E : Type u_9} [inst_3 : AddCommMonoid E] [inst_4 : Module R E]
  (φ : MultilinearMap R s E), PiTensorProduct.liftAux φ = PiTensorProduct.liftAddHom (fun p => p.1 • φ p.2) ⋯ ⋯ ⋯ ⋯ ⋯
-- Mathlib.Analysis.Calculus.FDeriv.Congr
DifferentiableWithinAt.congr_of_eventuallyEq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f f₁ : E → F} {x : E} {s : Set E},
  DifferentiableWithinAt 𝕜 f s x → f₁ =ᶠ[nhdsWithin x s] f → f₁ x = f x → DifferentiableWithinAt 𝕜 f₁ s x
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.unitIso_hom_inv_id_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D) (X : C),
  CategoryTheory.CategoryStruct.comp (e.unit.app X) (e.unitInv.app X) = CategoryTheory.CategoryStruct.id X
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.ι_descQ_eq_zero_of_boundary : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData) {A : C} (k : S.X₂ ⟶ A) (x : S.X₃ ⟶ A)
  (hx : k = CategoryTheory.CategoryStruct.comp S.g x), CategoryTheory.CategoryStruct.comp h.ι (h.descQ k ⋯) = 0
-- Init.Tactics
/-- The common arguments of `dsimp?` and `dsimp?!`.  -/
Lean.Parser.Tactic.dsimpTraceArgsRest : Lean.ParserDescr
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.prod.instIsFiniteMeasureOnCompacts : ∀ {α : Type u_4} {β : Type u_5} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure β)
  [MeasureTheory.IsFiniteMeasureOnCompacts μ] [MeasureTheory.IsFiniteMeasureOnCompacts ν],
  MeasureTheory.IsFiniteMeasureOnCompacts (μ.prod ν)
-- Lean.Declaration
Lean.QuotKind.noConfusionType : Sort v✝ → Lean.QuotKind → Lean.QuotKind → Sort v✝
-- Batteries.Data.List.Basic
List.zipWithLeft'TR.go.eq_def : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → Option β → γ) (a : List α) (a_1 : List β) (a_2 : Array γ),
  List.zipWithLeft'TR.go f a a_1 a_2 =
    match a, a_1, a_2 with
    | [], bs, acc => (acc.toList, bs)
    | as, [], acc => ((List.foldl (fun acc a => acc.push (f a none)) acc as).toList, [])
    | a :: as, b :: bs, acc => List.zipWithLeft'TR.go f as bs (acc.push (f a (some b)))
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- `MonoidAlgebra.coeff` as an equiv.  -/
MonoidAlgebra.coeffEquiv : {R : Type u_1} → {M : Type u_4} → [inst : Semiring R] → MonoidAlgebra R M ≃ (M →₀ R)
-- Init.Data.String.Basic
String.Pos.Raw.prev.eq_1 : ∀ (x : String) (x_1 : String.Pos.Raw), String.Pos.Raw.prev x x_1 = String.Pos.Raw.utf8PrevAux x.toList 0 x_1
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.bot_ext : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (x y : ↥⊥), x = y
-- Mathlib.RingTheory.PowerSeries.Evaluation
PowerSeries.hasSum_aeval : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] {a : S} [inst_2 : UniformSpace R]
  [inst_3 : UniformSpace S] [inst_4 : IsUniformAddGroup R] [inst_5 : IsTopologicalSemiring R]
  [inst_6 : IsUniformAddGroup S] [inst_7 : T2Space S] [inst_8 : CompleteSpace S] [inst_9 : IsTopologicalRing S]
  [inst_10 : IsLinearTopology S S] [inst_11 : Algebra R S] [inst_12 : ContinuousSMul R S] (ha : PowerSeries.HasEval a)
  (f : PowerSeries R), HasSum (fun d => (PowerSeries.coeff d) f • a ^ d) ((PowerSeries.aeval ha) f)
-- Mathlib.Control.Bitraversable.Instances
/-- The bitraverse function for `α × β`.  -/
Prod.bitraverse : {F : Type u → Type u} →
  [Applicative F] →
    {α : Type u_1} → {α' : Type u} → {β : Type u_2} → {β' : Type u} → (α → F α') → (β → F β') → α × β → F (α' × β')
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.isSome_minKey?_of_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  t.contains k = true → t.minKey?.isSome = true
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.ToForwardSearcher.DefaultForwardSearcher.mk : {ρ : Type} →
  {pat : ρ} → {s : String.Slice} → s.Pos → String.Slice.Pattern.ToForwardSearcher.DefaultForwardSearcher pat s
-- Mathlib.Data.List.SplitLengths
List.splitLengths_cons : ∀ {α : Type u_1} (l : List α) (sz : List ℕ) (n : ℕ),
  (n :: sz).splitLengths l = List.take n l :: sz.splitLengths (List.drop n l)
-- Init.Data.UInt.Lemmas
USize.mod_self : ∀ {a : USize}, a % a = 0
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.Heap.length.eq_2 : ∀ {α : Type u_1} (rank : ℕ) (val : α) (c : Batteries.BinomialHeap.Imp.HeapNode α)
  (s : Batteries.BinomialHeap.Imp.Heap α), (Batteries.BinomialHeap.Imp.Heap.cons rank val c s).length = s.length + 1
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.map_eq_bot_iff : ∀ {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : AddCommGroup V₂]
  [inst_5 : Module k V₂] [inst_6 : AddTorsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) {s : AffineSubspace k P₁},
  AffineSubspace.map f s = ⊥ ↔ s = ⊥
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.pellZd_add : ∀ {a : ℕ} (a1 : 1 < a) (m n : ℕ), Pell.pellZd a1 (m + n) = Pell.pellZd a1 m * Pell.pellZd a1 n
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.coeffs_mul_X : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (p : MvPolynomial σ R) (n : σ),
  (p * MvPolynomial.X n).coeffs = p.coeffs
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.setLIntegral_mono_ae' : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f g : α → ENNReal},
  MeasurableSet s → (∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ g x) → ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.inl_opIso_inv_assoc : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (P Q : C) [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct P Q] {Z : Cᵒᵖ} (h : Opposite.op (P ⊞ Q) ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.opIso P Q).inv h) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst.op h
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.tendsto_atTop_principal : ∀ {α : Type u_3} {β : Type u_4} [Nonempty α] [inst : Preorder α] [IsDirectedOrder α] {f : α → β} {s : Set β},
  Filter.Tendsto f Filter.atTop (Filter.principal s) ↔ ∃ N, ∀ (n : α), N ≤ n → f n ∈ s
-- Mathlib.RingTheory.PiTensorProduct
PiTensorProduct.mul_assoc : ∀ {ι : Type u_1} {R : Type u_3} {A : ι → Type u_4} [inst : CommSemiring R] [inst_1 : (i : ι) → NonUnitalSemiring (A i)]
  [inst_2 : (i : ι) → Module R (A i)] [inst_3 : ∀ (i : ι), SMulCommClass R (A i) (A i)]
  [inst_4 : ∀ (i : ι), IsScalarTower R (A i) (A i)] (x y z : PiTensorProduct R fun i => A i),
  (PiTensorProduct.mul ((PiTensorProduct.mul x) y)) z = (PiTensorProduct.mul x) ((PiTensorProduct.mul y) z)
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
/-- If `f : M → N` is a submultiplicative function, `f (x * y) ≤ f x * f y`, `f 1 = 1`, and `g i`,
`i ∈ s`, is a finite family of elements of `M`, then `f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)`.  -/
Finset.le_prod_of_submultiplicative : ∀ {ι : Type u_1} {M : Type u_4} {N : Type u_5} [inst : CommMonoid M] [inst_1 : CommMonoid N] [inst_2 : Preorder N]
  [IsOrderedMonoid N] (f : M → N),
  f 1 ≤ 1 → (∀ (x y : M), f (x * y) ≤ f x * f y) → ∀ (s : Finset ι) (g : ι → M), f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.addX_self : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} (P : Fin 3 → R), W'.addX P P = 0
-- Mathlib.Algebra.Lie.Basic
/-- A Lie ring bracket is additive in its first component.  -/
LieRing.add_lie : ∀ {L : Type v} [self : LieRing L] (x y z : L), ⁅x + y, z⁆ = ⁅x, z⁆ + ⁅y, z⁆
-- Mathlib.Algebra.Star.Basic
Pi.star_mulSingle : ∀ {ι : Type u_1} {R : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → MulOneClass (R i)]
  [inst_2 : (i : ι) → StarMul (R i)] (i : ι) (r : R i), star (Pi.mulSingle i r) = Pi.mulSingle i (star r)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
/-- `Finset α` is an `AddCommSemigroup` under pointwise operations if `α` is.  -/
Finset.addCommSemigroup : {α : Type u_2} → [DecidableEq α] → [AddCommSemigroup α] → AddCommSemigroup (Finset α)
-- Std.Data.DTreeMap.Basic
Std.DTreeMap.instInter : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Inter (Std.DTreeMap α β cmp)
-- Mathlib.Order.Hom.Set
OrderIso.setCongr_apply : ∀ {α : Type u_1} [inst : Preorder α] (s t : Set α) (h : s = t) (a : { a // (fun x => x ∈ s) a }),
  (OrderIso.setCongr s t h) a = ⟨↑a, ⋯⟩
-- Mathlib.Tactic.ClickSuggestions.GRewrite
Mathlib.Tactic.ClickSuggestions.GrwKey.mk.injEq : ∀ (numGoals nameLength replacementSize : ℕ) (name : String) (replacement : Lean.Meta.AbstractMVarsResult)
  (numGoals_1 nameLength_1 replacementSize_1 : ℕ) (name_1 : String) (replacement_1 : Lean.Meta.AbstractMVarsResult),
  ({ numGoals := numGoals, nameLength := nameLength, replacementSize := replacementSize, name := name,
        replacement := replacement } =
      { numGoals := numGoals_1, nameLength := nameLength_1, replacementSize := replacementSize_1, name := name_1,
        replacement := replacement_1 }) =
    (numGoals = numGoals_1 ∧
      nameLength = nameLength_1 ∧ replacementSize = replacementSize_1 ∧ name = name_1 ∧ replacement = replacement_1)
-- Mathlib.Topology.Algebra.Algebra
instIsTopologicalSemiringSubtypeMemSubalgebra : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u} [inst_1 : TopologicalSpace A] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [IsTopologicalSemiring A] (s : Subalgebra R A), IsTopologicalSemiring ↥s
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_castSucc_Iio : ∀ {n : ℕ} (i : Fin n), Finset.image Fin.castSucc (Finset.Iio i) = Finset.Iio i.castSucc
-- Mathlib.Order.Heyting.Basic
/-- **Alias** of `hnot_le_comm`. -/
hnot_le_iff_hnot_le : ∀ {α : Type u_2} [inst : CoheytingAlgebra α] {a b : α}, ￢b ≤ a ↔ ￢a ≤ b
-- Mathlib.Data.Set.Lattice.Image
Set.image2_sUnion_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (S : Set (Set α)) (t : Set β),
  Set.image2 f (⋃₀ S) t = ⋃ s ∈ S, Set.image2 f s t
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multiequalizer.lift.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  (I : CategoryTheory.Limits.MulticospanIndex J C) [inst_1 : CategoryTheory.Limits.HasMultiequalizer I] (W : C)
  (k k_1 : (a : J.L) → W ⟶ I.left a) (e_k : k = k_1)
  (h :
    ∀ (b : J.R),
      CategoryTheory.CategoryStruct.comp (k (J.fst b)) (I.fst b) =
        CategoryTheory.CategoryStruct.comp (k (J.snd b)) (I.snd b)),
  CategoryTheory.Limits.Multiequalizer.lift I W k h = CategoryTheory.Limits.Multiequalizer.lift I W k_1 ⋯
-- Init.Data.SInt.Lemmas
Int8.toInt32_ofInt : ∀ {n : ℤ}, Int8.minValue.toInt ≤ n → n ≤ Int8.maxValue.toInt → (Int8.ofInt n).toInt32 = Int32.ofInt n
-- Mathlib.Data.Set.Card
Set.Finite.encard_eq_coe_toFinset_card : ∀ {α : Type u_1} {s : Set α} (h : s.Finite), s.encard = ↑h.toFinset.card
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.aeval_zero : ∀ {R : Type u} {A : Type z} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (x : A),
  (Polynomial.aeval x) 0 = 0
-- Mathlib.CategoryTheory.CodiscreteCategory
CategoryTheory.Codiscrete.mk_as : ∀ {α : Type u} (X : CategoryTheory.Codiscrete α), { as := X.as } = X
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.IsIndepSet.eq_1 : ∀ {α : Type u_1} (G : SimpleGraph α) (s : Set α), G.IsIndepSet s = s.Pairwise fun v w => ¬G.Adj v w
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateDelImp : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.Compiler.LCNF.Code pu → Lean.FVarId → Lean.Compiler.LCNF.Code pu → Lean.Compiler.LCNF.Code pu
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.exists_genWeightSpace_zero_le_ker_of_isNoetherian : ∀ (R : Type u_2) {L : Type u_3} (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] [IsNoetherian R M] (x : L),
  ∃ k, ↑(LieModule.genWeightSpace M 0) ≤ LinearMap.ker ((LieModule.toEnd R L M) x ^ k)
-- Mathlib.Lean.Thunk
/-- The sum of two thunks.  -/
Thunk.add : {α : Type u} → [Add α] → Thunk α → Thunk α → Thunk α
-- Mathlib.Combinatorics.SimpleGraph.CycleGraph
SimpleGraph.cycleGraph_degree_two_le : ∀ {n : ℕ} {v : Fin (n + 2)}, (SimpleGraph.cycleGraph (n + 2)).degree v = {v - 1, v + 1}.card
-- Mathlib.Analysis.SpecificLimits.Normed
/-- The **alternating series test** for monotone sequences.  -/
Monotone.tendsto_alternating_series_of_tendsto_zero : ∀ {f : ℕ → ℝ},
  Monotone f →
    Filter.Tendsto f Filter.atTop (nhds 0) →
      ∃ l, Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, (-1) ^ i * f i) Filter.atTop (nhds l)
-- Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_eq_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : ChainComplex C ℕ) {Δ Δ' : SimplexCategory} (i : Δ' ⟶ Δ) [inst_2 : CategoryTheory.Mono i],
  Δ ≠ Δ' → ¬AlgebraicTopology.DoldKan.Isδ₀ i → AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K i = 0
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Equiv.get_eq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β}
  [inst_2 : LawfulBEq α] {k : α} (h₁ : m₁.WF) (h₂ : m₂.WF) (hk : k ∈ m₁) (h : m₁.Equiv m₂), m₁.get k hk = m₂.get k ⋯
-- Mathlib.LinearAlgebra.DFinsupp
/-- Two `R`-linear maps from `Π₀ i, M i` which agree on each `single i x` agree everywhere.  -/
DFinsupp.lhom_ext : ∀ {ι : Type u_1} {R : Type u_3} {M : ι → Type u_5} {N : Type u_6} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M i)] [inst_2 : (i : ι) → Module R (M i)] [inst_3 : AddCommMonoid N]
  [inst_4 : Module R N] [inst_5 : DecidableEq ι] ⦃φ ψ : (Π₀ (i : ι), M i) →ₗ[R] N⦄,
  (∀ (i : ι) (x : M i), (φ fun₀ | i => x) = ψ fun₀ | i => x) → φ = ψ
-- Mathlib.Order.Hom.Lattice
SupHom.coe_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Max α] [inst_1 : Max β] [inst_2 : Max γ] (f : SupHom β γ)
  (g : SupHom α β), ⇑(f.comp g) = ⇑f ∘ ⇑g
-- Mathlib.Analysis.Complex.Cardinality
/-- The cardinality of the complex numbers, as a type.  -/
Cardinal.mk_complex : Cardinal.mk ℂ = Cardinal.continuum
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.lineMap_apply_module : ∀ {k : Type u_1} {V1 : Type u_2} [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : Module k V1] (p₀ p₁ : V1) (c : k),
  (AffineMap.lineMap p₀ p₁) c = (1 - c) • p₀ + c • p₁
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.lift.congr_simp : ∀ {R : Type u_1} [inst : CommSemiring R] {M M_1 : Submonoid R} (e_M : M = M_1) {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] {P : Type u_3} [inst_3 : CommSemiring P] [inst_4 : IsLocalization M S] {g g_1 : R →+* P}
  (e_g : g = g_1) (hg : ∀ (y : ↥M), IsUnit (g ↑y)), IsLocalization.lift hg = IsLocalization.lift ⋯
-- Mathlib.Order.ConditionallyCompletePartialOrder.Basic
OrderDual.instConditionallyCompletePartialOrderSupOfConditionallyCompletePartialOrderInf : {α : Type u_1} → [ConditionallyCompletePartialOrderInf α] → ConditionallyCompletePartialOrderSup αᵒᵈ
-- Mathlib.Data.Num.ZNum
Num.ofZNum'_toNat : ∀ (n : ZNum), castNum <$> Num.ofZNum' n = (↑n).toNat?
-- Mathlib.Analysis.Distribution.DerivNotation
/-- `∂^{m} f` is the iterated line derivative of `f`, where `m` is a finite number of (different)
directions.  -/
LineDeriv.iteratedLineDerivOp : {V : Type u_11} → {E : Type u_12} → [LineDeriv V E E] → {n : ℕ} → (Fin n → V) → E → E
-- Mathlib.Logic.Function.Basic
Function.LeftInverse.eq_rec_on_eq : ∀ {α : Sort u_1} {β : Sort u_2} {γ : β → Sort v} {f : α → β} {g : β → α} (h : Function.LeftInverse g f)
  (C : (a : α) → γ (f a)) (a : α), Eq.recOn ⋯ (C (g (f a))) = C a
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.inverseImage_sSup : ∀ {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) (P : Set (CategoryTheory.MorphismProperty D)),
  (sSup P).inverseImage F = ⨆ P' ∈ P, P'.inverseImage F
-- Std.Time.DateTime
/-- Checks if the `DateTime` is in a leap year.
 -/
Std.Time.DateTime.inLeapYear : Std.Time.DateTime → Bool
-- Mathlib.NumberTheory.Height.Basic
/-- The logarithmic height of `x * y` is at most the sum of the logarithmic heights
of `x` and `y`.  -/
Height.logHeight₁_mul_le : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] (x y : K),
  Height.logHeight₁ (x * y) ≤ Height.logHeight₁ x + Height.logHeight₁ y
-- Mathlib.Topology.GDelta.Basic
/-- A set is called **nowhere dense** iff its closure has empty interior.  -/
IsNowhereDense : {X : Type u_1} → [TopologicalSpace X] → Set X → Prop
-- Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction
CategoryTheory.ParametrizedAdjunction.inr_arrowHomEquiv_symm_apply_left_assoc : ∀ {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₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)}
  {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} (adj₂ : F ⊣₂ G) {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁}
  {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂} {X₃ Y₃ : C₃} {f₃ : X₃ ⟶ Y₃} (sq₁₂ : F.PushoutObjObj f₁ f₂) (sq₁₃ : G.PullbackObjObj f₁ f₃)
  (β : CategoryTheory.Arrow.mk f₂ ⟶ CategoryTheory.Arrow.mk sq₁₃.π) {Z : C₃}
  (h : (CategoryTheory.Arrow.mk f₃).left ⟶ Z),
  CategoryTheory.CategoryStruct.comp sq₁₂.inr
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left ((adj₂.arrowHomEquiv sq₁₂ sq₁₃).symm β)) h) =
    CategoryTheory.CategoryStruct.comp
      (adj₂.homEquiv.symm (CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.right β) sq₁₃.fst)) h
-- Mathlib.Analysis.Complex.Norm
/-- The real part of a complex Cauchy sequence, as a real Cauchy sequence.  -/
Complex.cauSeqRe : (CauSeq ℂ fun x => ‖x‖) → CauSeq ℝ abs
-- Mathlib.Topology.Bornology.Basic
Bornology.isCobounded_def : ∀ {α : Type u_2} {x : Bornology α} {s : Set α}, Bornology.IsCobounded s ↔ s ∈ Bornology.cobounded α
-- Lean.Data.Json.Basic
Lean.JsonNumber.instDecidableLt : (a b : Lean.JsonNumber) → Decidable (a < b)