mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.baseChange_ψ₂ : ∀ {R : Type r} {S : Type s} [inst : CommRing R] [inst_1 : CommRing S] (W : WeierstrassCurve R) [inst_2 : Algebra R S]
  {A : Type u} [inst_3 : CommRing A] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [IsScalarTower R S A] {B : Type v}
  [inst_7 : CommRing B] [inst_8 : Algebra R B] [inst_9 : Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B),
  (W.baseChange B).ψ₂ = Polynomial.map (Polynomial.mapRingHom ↑f) (W.baseChange A).ψ₂
-- Mathlib.Combinatorics.Derangements.Basic
/-- The set of permutations that fix either `a` or nothing is equivalent to the sum of:
- derangements on `α`
- derangements on `α` minus `a`.  -/
derangements.atMostOneFixedPointEquivSum_derangements : {α : Type u_1} →
  [DecidableEq α] → (a : α) → { f // Function.fixedPoints ⇑f ⊆ {a} } ≃ ↑(derangements ↑{a}ᶜ) ⊕ ↑(derangements α)
-- Mathlib.Topology.MetricSpace.Gluing
_private.Mathlib.Topology.MetricSpace.Gluing.0.Metric.Sum.mem_uniformity : ∀ {X : Type u} {Y : Type v} [inst : MetricSpace X] [inst_1 : MetricSpace Y] (s : Set ((X ⊕ Y) × (X ⊕ Y))),
  s ∈ uniformity (X ⊕ Y) ↔ ∃ ε > 0, ∀ (a b : X ⊕ Y), Metric.Sum.dist a b < ε → (a, b) ∈ s
-- Mathlib.RingTheory.Valuation.Basic
Valuation.instNontrivialSubtypeUnitsMemSubmonoidValueMonoidOfClassOfIsNontrivial : ∀ {R : Type u_3} [inst : Ring R] {Γ₀ : Type u_7} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] {v : Valuation R Γ₀}
  [hv : v.IsNontrivial], Nontrivial ↥(MonoidWithZeroHom.ofClass v).valueMonoid
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
instIsDiscreteValuationRingSubtypeMemSubringIntegerWithZeroMultiplicativeIntValuation : ∀ (A : Type u_1) [inst : CommRing A] [inst_1 : IsDedekindDomain A] (K : Type u_2) [inst_2 : Field K]
  [inst_3 : Algebra A K] [inst_4 : IsFractionRing A K] (v : IsDedekindDomain.HeightOneSpectrum A),
  IsDiscreteValuationRing ↥(IsDedekindDomain.HeightOneSpectrum.valuation K v).integer
-- Mathlib.Order.Filter.Basic
Filter.Eventually.lt_top_of_ne : ∀ {α : Type u} {β : Type v} [inst : PartialOrder β] [inst_1 : OrderTop β] {l : Filter α} {f : α → β},
  (∀ᶠ (x : α) in l, f x ≠ ⊤) → ∀ᶠ (x : α) in l, f x < ⊤
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
SSet.horn₂₂.sq : (SSet.stdSimplex.face {2}).BicartSq (SSet.stdSimplex.face {0, 2}) (SSet.stdSimplex.face {1, 2}) (SSet.horn 2 2)
-- Mathlib.MeasureTheory.Measure.Typeclasses.NullSingletonClass
MeasureTheory.Ioo_ae_eq_Ioc : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NullSingletonClass μ]
  [inst : PartialOrder α] {a b : α}, Set.Ioo a b =ᵐ[μ] Set.Ioc a b
-- Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
_private.Mathlib.LinearAlgebra.CliffordAlgebra.Contraction.0.CliffordAlgebra.«term_⌋_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Group.Basic
/-- If `x ^ n = 1`, then `x ^ m` is the same as `x ^ (m % n)`  -/
pow_eq_pow_mod : ∀ {M : Type u_4} [inst : Monoid M] {a : M} {n : ℕ} (m : ℕ), a ^ n = 1 → a ^ m = a ^ (m % n)
-- Mathlib.Order.Minimal
/-- **Alias** of `setOfPred_maximal_subset`. -/
setOf_maximal_subset : ∀ {α : Type u_2} [inst : Preorder α] (s : Set α), {x | Maximal (fun x => x ∈ s) x} ⊆ s
-- Mathlib.Analysis.Complex.Norm
Complex.nndist_conj_self : ∀ (z : ℂ), nndist ((starRingEnd ℂ) z) z = 2 * Real.nnabs z.im
-- Mathlib.Data.NNReal.Defs
NNReal.exists : ∀ {p : NNReal → Prop}, (∃ x, p x) ↔ ∃ x, ∃ (hx : 0 ≤ x), p (NNReal.mk x hx)
-- Mathlib.Topology.Constructions.SumProd
Topology.IsOpenEmbedding.inr : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y], Topology.IsOpenEmbedding Sum.inr
-- Mathlib.Topology.Sheaves.Sheaf
/-- The sheaf condition has several different equivalent formulations.
The official definition chosen here is in terms of Grothendieck topologies so that the results on
sites could be applied here easily, and this condition does not require additional constraints on
the value category.
The equivalent formulations of the sheaf condition on `presheaf C X` are as follows :

1. `TopCat.Presheaf.IsSheaf`: (the official definition)
  It is a sheaf with respect to the Grothendieck topology on `opens X`, which is to say:
  For each open cover `{ Uᵢ }` of `U`, and a family of compatible functions `A ⟶ F(Uᵢ)` for an
  `A : X`, there exists a unique gluing `A ⟶ F(U)` compatible with the restriction.

2. `TopCat.Presheaf.IsSheafEqualizerProducts`: (requires `C` to have all products)
  For each open cover `{ Uᵢ }` of `U`, `F(U) ⟶ ∏ᶜ F(Uᵢ)` is the equalizer of the two morphisms
  `∏ᶜ F(Uᵢ) ⟶ ∏ᶜ F(Uᵢ ∩ Uⱼ)`.
  See `TopCat.Presheaf.isSheaf_iff_isSheafEqualizerProducts`.

3. `TopCat.Presheaf.IsSheafOpensLeCover`:
  For each open cover `{ Uᵢ }` of `U`, `F(U)` is the limit of the diagram consisting of arrows
  `F(V₁) ⟶ F(V₂)` for every pair of open sets `V₁ ⊇ V₂` that are contained in some `Uᵢ`.
  See `TopCat.Presheaf.isSheaf_iff_isSheafOpensLeCover`.

4. `TopCat.Presheaf.IsSheafPairwiseIntersections`:
  For each open cover `{ Uᵢ }` of `U`, `F(U)` is the limit of the diagram consisting of arrows
  from `F(Uᵢ)` and `F(Uⱼ)` to `F(Uᵢ ∩ Uⱼ)` for each pair `(i, j)`.
  See `TopCat.Presheaf.isSheaf_iff_isSheafPairwiseIntersections`.

The following requires `C` to be concrete and complete, and `forget C` to reflect isomorphisms and
preserve limits. This applies to most "algebraic" categories, e.g. groups, abelian groups and rings.

5. `TopCat.Presheaf.IsSheafUniqueGluing`:
  (requires `C` to be concrete and complete; `forget C` to reflect isomorphisms and preserve limits)
  For each open cover `{ Uᵢ }` of `U`, and a compatible family of elements `x : F(Uᵢ)`, there exists
  a unique gluing `x : F(U)` that restricts to the given elements.
  See `TopCat.Presheaf.isSheaf_iff_isSheafUniqueGluing`.

6. The underlying sheaf of types is a sheaf.
  See `TopCat.Presheaf.isSheaf_iff_isSheaf_comp` and
  `CategoryTheory.Presheaf.isSheaf_iff_isSheaf_forget`.
 -/
TopCat.Presheaf.IsSheaf : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X : TopCat} → TopCat.Presheaf C X → Prop
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
exists_nsmul_ne_zero_of_isAddCyclic : ∀ {G : Type u_2} [inst : AddGroup G] [G_addCyclic : IsAddCyclic G] {k : ℕ}, k ≠ 0 → k < Nat.card G → ∃ a, k • a ≠ 0
-- Mathlib.Algebra.MonoidAlgebra.Ideal
/-- If `x` belongs to the ideal generated by generators in `s`, then every element of the support of
`x` factors additively through an element of `s`.
 -/
AddMonoidAlgebra.mem_ideal_span_of'_image : ∀ {k : Type u_1} {A : Type u_2} [inst : AddMonoid A] [inst_1 : Semiring k] {s : Set A} {x : AddMonoidAlgebra k A},
  x ∈ Ideal.span (AddMonoidAlgebra.of' k A '' s) ↔ ∀ m ∈ x.coeff.support, ∃ m' ∈ s, ∃ d, m = d + m'
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.Ioo_subset_Icc : ∀ {ι : Type u_1} (I : BoxIntegral.Box ι), BoxIntegral.Box.Ioo I ⊆ BoxIntegral.Box.Icc I
-- Lean.Elab.DefView
Lean.Elab.HeaderProcessedSnapshot.mk : Lean.Language.Snapshot →
  Lean.Elab.DefViewElabHeaderData →
    Lean.Elab.Term.SavedState →
      Option Lean.Syntax →
        Option (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) →
          Lean.Syntax →
            Lean.Language.SnapshotTask (Option Lean.Elab.BodyProcessedSnapshot) →
              Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree) → Lean.Elab.HeaderProcessedSnapshot
-- Lean.Compiler.IR.Basic
Lean.IR.instInhabitedParam.default : Lean.IR.Param
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.prod_bot_sup_bot_prod : ∀ {N : Type u_2} [inst : AddZeroClass N] {M : Type u_5} [inst_1 : AddZeroClass M] (s : AddSubmonoid M)
  (t : AddSubmonoid N), s.prod ⊥ ⊔ ⊥.prod t = s.prod t
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
/-- **Alias** of `MeasurableEquiv.setOfPred`.

---

`Set.ofPred` as a `MeasurableEquiv`.  -/
MeasurableEquiv.setOf : {α : Type u_8} → (α → Prop) ≃ᵐ Set α
-- Init.Dynamic
_private.Init.Dynamic.0.TypeName.mk' : {α : Type u} → (TypeNameData α).type → TypeName α
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.coe_sUnion : ∀ (x : ZFSet.{u}), ↑x.sUnion = ⋃₀ (SetLike.coe '' ↑x)
-- Mathlib.Order.Lattice
Prod.instMax_mathlib : (α : Type u) → (β : Type v) → [Max α] → [Max β] → Max (α × β)
-- Mathlib.Util.Notation3
/-- Matches raw `Nat` literals.  -/
Mathlib.Notation3.natLitMatcher : ℕ → Mathlib.Notation3.Matcher
-- Mathlib.Analysis.Complex.Positivity
/-- An entire function whose iterated derivatives at `c` are all nonnegative real has nonnegative
real values on `c + ℝ≥0`.  -/
Differentiable.nonneg_of_iteratedDeriv_nonneg : ∀ {f : ℂ → ℂ}, Differentiable ℂ f → ∀ {c : ℂ}, (∀ (n : ℕ), 0 ≤ iteratedDeriv n f c) → ∀ ⦃z : ℂ⦄, c ≤ z → 0 ≤ f z
-- Std.Do.SPred.SVal
_private.Std.Do.SPred.SVal.0.Std.Do.SVal.uncurry.match_1.splitter : (head : Type u_1) →
  (tail : List (Type u_1)) →
    (motive : Std.Do.SVal.StateTuple (head :: tail) → Sort u_2) →
      (x : Std.Do.SVal.StateTuple (head :: tail)) →
        ((s : head) → (t : Std.Do.SVal.StateTuple tail) → motive (s, t)) → motive x
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField
AlgebraicGeometry.LocallyRingedSpace.residueFieldMap_id : ∀ {X : AlgebraicGeometry.LocallyRingedSpace} (x : ↑X.toTopCat),
  AlgebraicGeometry.LocallyRingedSpace.residueFieldMap (CategoryTheory.CategoryStruct.id X) x =
    CategoryTheory.CategoryStruct.id (X.residueField x)
-- Mathlib.Algebra.CubicDiscriminant
Cubic.degree_of_b_eq_zero' : ∀ {R : Type u_1} {c d : R} [inst : Semiring R], { a := 0, b := 0, c := c, d := d }.toPoly.degree ≤ 1
-- Mathlib.Order.Filter.IsBounded
Filter.bddBelow_range_of_tendsto_atTop_atTop : ∀ {α : Type u_1} [inst : Preorder α] [Nonempty α] [IsCodirectedOrder α] {u : ℕ → α},
  Filter.Tendsto u Filter.atTop Filter.atTop → BddBelow (Set.range u)
-- Init.Control.Lawful.Instances
StateT.seqLeft_eq : ∀ {m : Type u_1 → Type u_2} {σ α β : Type u_1} [inst : Monad m] [LawfulMonad m] (x : StateT σ m α) (y : StateT σ m β),
  x <* y = Function.const β <$> x <*> y
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_Y : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {X : C}
  (S : J.Cover X) (x x_1 : S.Arrow) (r : x.Relation x_1), S.preOneHypercover.Y r = r.Z
-- Mathlib.Topology.Order.LocalExtr
IsLocalMax.sup : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SemilatticeSup β] {f g : α → β} {a : α},
  IsLocalMax f a → IsLocalMax g a → IsLocalMax (fun x => f x ⊔ g x) a
-- Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
InnerProductSpace.gramSchmidtOrthonormalBasis_apply_of_orthogonal : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_3} [inst_3 : LinearOrder ι] [inst_4 : LocallyFiniteOrderBot ι] [inst_5 : WellFoundedLT ι]
  [inst_6 : Fintype ι] [inst_7 : FiniteDimensional 𝕜 E] (h : Module.finrank 𝕜 E = Fintype.card ι) {f : ι → E},
  (Pairwise fun i j => inner 𝕜 (f i) (f j) = 0) →
    ∀ {i : ι}, f i ≠ 0 → (InnerProductSpace.gramSchmidtOrthonormalBasis h f) i = (↑‖f i‖)⁻¹ • f i
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
Polynomial.resultant_zero_left_deg : ∀ {R : Type u_1} [inst : CommRing R] (f g : Polynomial R) (m : ℕ), f.resultant g 0 m = f.coeff 0 ^ m
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnModule.single_zero_smul_eq_smul : ∀ {Γ' : Type u_2} {R : Type u_3} {V : Type u_5} [inst : PartialOrder Γ'] [inst_1 : AddCommMonoid V] (Γ : Type u_6)
  [inst_2 : AddCommMonoid Γ] [inst_3 : PartialOrder Γ] [inst_4 : AddAction Γ Γ'] [inst_5 : IsOrderedCancelVAdd Γ Γ']
  [inst_6 : MulZeroClass R] [inst_7 : SMulWithZero R V] {r : R} {x : HahnModule Γ' R V},
  (HahnSeries.single 0) r • x = r • x
-- Init.Coe
CoeSort.mk : {α : Sort u} → {β : outParam (Sort v)} → (α → β) → CoeSort α β
-- Mathlib.Order.Category.FinBoolAlg
/-- `OrderDual` as a functor.  -/
FinBoolAlg.dual : CategoryTheory.Functor FinBoolAlg FinBoolAlg
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.erase_empty : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {k : α},
  (Std.DTreeMap.Internal.Impl.erase k Std.DTreeMap.Internal.Impl.empty ⋯).impl = Std.DTreeMap.Internal.Impl.empty
-- Mathlib.CategoryTheory.Abelian.Preradical.Colon
CategoryTheory.Abelian.Preradical.toColon_hom_left_app_colonπ_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (Φ Ψ : CategoryTheory.Abelian.Preradical C) (X : C),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Over.Hom.left (Φ.toColon Ψ).hom).app X) ((Φ.colonπ Ψ).app X) = 0
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Expr.intMul.sizeOf_spec : ∀ (k : ℤ) (a : Lean.Grind.Linarith.Expr), sizeOf (Lean.Grind.Linarith.Expr.intMul k a) = 1 + sizeOf k + sizeOf a
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.instNeg.eq_1 : ∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace γ]
  [inst_2 : AddGroup γ] [inst_3 : IsTopologicalAddGroup γ],
  MeasureTheory.AEEqFun.instNeg = { neg := MeasureTheory.AEEqFun.comp Neg.neg ⋯ }
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.synth : Lean.Meta.SynthInstance.SynthM (Option Lean.Meta.AbstractMVarsResult)
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.sum_le_one_iff : ∀ {α : Type u_2} {s : Finset α} {f : α → ℕ},
  ∑ x ∈ s, f x ≤ 1 ↔ ∀ (x y : α), x ∈ s → y ∈ s → f x ≠ 0 → f y ≠ 0 → x = y ∧ f x = 1
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.StrongHomClass.realize_boundedFormula : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N] {α : Type u'}
  {n : ℕ} {F : Type u_4} [inst_2 : EquivLike F M N] [L.StrongHomClass F M N] (g : F) (φ : L.BoundedFormula α n)
  {v : α → M} {xs : Fin n → M}, φ.Realize (⇑g ∘ v) (⇑g ∘ xs) ↔ φ.Realize v xs
-- Qq.ForLean.ReduceEval
Lean.Meta.instReduceEvalUSize_qq : Lean.Meta.ReduceEval USize
-- Mathlib.CategoryTheory.Preadditive.Comma
CategoryTheory.CommaMorphism.instNegHomComma : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    [inst_1 : CategoryTheory.Preadditive A] →
      {B : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} B] →
          [inst_3 : CategoryTheory.Preadditive B] →
            {T : Type u₃} →
              [inst_4 : CategoryTheory.Category.{v₃, u₃} T] →
                [inst_5 : CategoryTheory.Preadditive T] →
                  (L : CategoryTheory.Functor A T) →
                    [L.Additive] →
                      (R : CategoryTheory.Functor B T) → [R.Additive] → {u v : CategoryTheory.Comma L R} → Neg (u ⟶ v)
-- Mathlib.CategoryTheory.Sites.Hypercover.Saturate
CategoryTheory.PreZeroHypercover.isLimit_saturate_type_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {S : C} (E : CategoryTheory.PreZeroHypercover S)
  (F : CategoryTheory.Functor Cᵒᵖ (Type u_3)),
  Nonempty (CategoryTheory.Limits.IsLimit (E.saturate.multifork F)) ↔ CategoryTheory.Presieve.IsSheafFor F E.presieve₀
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.instSimpAndPureTrue : ∀ (σs : List (Type u_1)) (P : Std.Do.SPred σs), Std.Do.SPred.Tactic.SimpAnd P ⌜True⌝ P
-- Mathlib.Algebra.Order.GroupWithZero.OrderIso
OrderIso.mulRight₀_symm : ∀ {G₀ : Type u_1} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [inst_2 : MulPosReflectLT G₀] (a : G₀)
  (ha : 0 < a), (OrderIso.mulRight₀ a ha).symm = OrderIso.mulRight₀ a⁻¹ ⋯
-- Mathlib.Data.Set.Finite.Basic
Set.finite_univ : ∀ {α : Type u} [Finite α], Set.univ.Finite
-- Std.Data.ExtDTreeMap.Lemmas
_private.Std.Data.ExtDTreeMap.Lemmas.0.Std.ExtDTreeMap.Const.insertManyIfNewUnit_list_mk : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {t : Std.DTreeMap α (fun x => Unit) cmp} {l : List α},
  Std.ExtDTreeMap.Const.insertManyIfNewUnit (Std.ExtDTreeMap.mk t) l =
    Std.ExtDTreeMap.mk (Std.DTreeMap.Const.insertManyIfNewUnit t l)
-- Mathlib.AlgebraicTopology.SimplicialSet.PiZero
/-- A simplicial set is econnected when it has exactly one connected component.  -/
SSet.IsConnected : SSet → Prop
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Splitting.mk : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {S : CategoryTheory.ShortComplex C} →
        (r : S.X₂ ⟶ S.X₁) →
          (s : S.X₃ ⟶ S.X₂) →
            autoParam (CategoryTheory.CategoryStruct.comp S.f r = CategoryTheory.CategoryStruct.id S.X₁)
                CategoryTheory.ShortComplex.Splitting.f_r._autoParam →
              autoParam (CategoryTheory.CategoryStruct.comp s S.g = CategoryTheory.CategoryStruct.id S.X₃)
                  CategoryTheory.ShortComplex.Splitting.s_g._autoParam →
                autoParam
                    (CategoryTheory.CategoryStruct.comp r S.f + CategoryTheory.CategoryStruct.comp S.g s =
                      CategoryTheory.CategoryStruct.id S.X₂)
                    CategoryTheory.ShortComplex.Splitting.id._autoParam →
                  S.Splitting
-- Mathlib.Analysis.Real.Cardinality
/-- **Non-Denumerability of the Continuum**: The reals are not countable.  -/
Cardinal.instUncountableReal : Uncountable ℝ
-- Mathlib.GroupTheory.Coxeter.Basic
CoxeterSystem.simple.eq_1 : ∀ {B : Type u_1} {W : Type u_3} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B),
  cs.simple i = cs.mulEquiv.symm (PresentedGroup.of i)
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.instFunLikeReal : FunLike CircleDeg1Lift ℝ ℝ
-- Mathlib.CategoryTheory.RepresentedBy
CategoryTheory.Functor.isRepresentedBy_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type w)) {X : C}
  (x : F.obj (Opposite.op X)),
  F.IsRepresentedBy x ↔ ∀ {Y : C}, Function.Bijective fun f => (CategoryTheory.ConcreteCategory.hom (F.map f.op)) x
-- Init.Grind.Ring.CommSemiringAdapter
_private.Init.Grind.Ring.CommSemiringAdapter.0.Lean.Grind.CommRing.Expr.toPolyS.match_4.eq_6 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (n : ℕ) (h_1 : (n : ℤ) → motive (Lean.Grind.CommRing.Expr.num n))
  (h_2 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_3 : (a b : Lean.Grind.CommRing.Expr) → motive (a.add b))
  (h_4 : (a b : Lean.Grind.CommRing.Expr) → motive (a.mul b))
  (h_5 : (a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k))
  (h_6 : (n : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast n))
  (h_7 : (a b : Lean.Grind.CommRing.Expr) → motive (a.sub b)) (h_8 : (a : Lean.Grind.CommRing.Expr) → motive a.neg)
  (h_9 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k)),
  (match Lean.Grind.CommRing.Expr.natCast n with
    | Lean.Grind.CommRing.Expr.num n => h_1 n
    | Lean.Grind.CommRing.Expr.var x => h_2 x
    | a.add b => h_3 a b
    | a.mul b => h_4 a b
    | a.pow k => h_5 a k
    | Lean.Grind.CommRing.Expr.natCast n => h_6 n
    | a.sub b => h_7 a b
    | a.neg => h_8 a
    | Lean.Grind.CommRing.Expr.intCast k => h_9 k) =
    h_6 n
-- Mathlib.Probability.Kernel.Category.Stoch
instDeterministicStochOfSFinKerHomWideSubcategoryStochHom : ∀ {X Y : Stoch} (κ : X ⟶ Y) [CategoryTheory.Deterministic κ.hom], CategoryTheory.Deterministic κ
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
IsFreeGroup.lift.eq_1 : ∀ {G : Type u_1} [inst : Group G] [inst_1 : IsFreeGroup G] {H : Type u_2} [inst_2 : Group H],
  IsFreeGroup.lift = (IsFreeGroup.basis G).lift
-- Mathlib.Order.CountableSupClosed
isLUB_countableSupClosure : ∀ {α : Type u_2} {s : Set α} {a : α} [inst : Preorder α], IsLUB (countableSupClosure s) a ↔ IsLUB s a
-- Std.Time.Zoned.Database.Windows
Std.Time.Database.WindowsDb.noConfusionType : Sort v✝ → Std.Time.Database.WindowsDb → Std.Time.Database.WindowsDb → Sort v✝
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.pairingCore.Type₁.mk.congr_simp : ∀ {m : ℕ} {k : Fin (m + 1)} {n : ℕ} (x x_1 : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N)
  (e_x : x = x_1) (d : ℕ) (hd : x.dim = d + 1) (index index_1 : Fin (d + 1)) (e_index : index = index_1)
  (isIndex : SSet.prodStdSimplex.pairingCore.IsIndex x hd index.succ),
  { x := x, d := d, hd := hd, index := index, isIndex := isIndex } =
    { x := x_1, d := d, hd := ⋯, index := index_1, isIndex := ⋯ }
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Cont'.cons₂.inj : ∀ {a a_1 : Turing.PartrecToTM2.Cont'}, a.cons₂ = a_1.cons₂ → a = a_1
-- Mathlib.ModelTheory.Algebra.Ring.Basic
/-- The constant `0` in the `Language.ring.Structure` is the same as the constant given by the
`Zero` instance  -/
FirstOrder.Ring.CompatibleRing.funMap_zero : ∀ {R : Type u_2} {inst : Add R} {inst_1 : Mul R} {inst_2 : Neg R} {inst_3 : One R} {inst_4 : Zero R}
  [self : FirstOrder.Ring.CompatibleRing R] (x : Fin 0 → R),
  FirstOrder.Language.Structure.funMap FirstOrder.Ring.zeroFunc x = 0
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.cylinder.map_ι₀_eq_map_ι₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} (K : HomologicalComplex C c) [inst_2 : DecidableRel c.Rel]
  [inst_3 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [inst_4 : K.HasCylinder],
  (∀ (j : ι), ∃ i, c.Rel i j) →
    ∀ {D : Type u_3} [inst_5 : CategoryTheory.Category.{v_2, u_3} D]
      (H : CategoryTheory.Functor (HomologicalComplex C c) D),
      (HomologicalComplex.homotopyEquivalences C c).IsInvertedBy H →
        H.map (HomologicalComplex.cylinder.ι₀ K) = H.map (HomologicalComplex.cylinder.ι₁ K)
-- Mathlib.GroupTheory.Perm.Centralizer
/-- Unapplied variant of `Equiv.Perm.mem_range_toPermHom_iff`  -/
Equiv.Perm.OnCycleFactors.mem_range_toPermHom_iff' : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {g : Equiv.Perm α} {τ : Equiv.Perm ↥g.cycleFactorsFinset},
  τ ∈ (Equiv.Perm.OnCycleFactors.toPermHom g).range ↔ (fun c => (↑c).support.card) ∘ ⇑τ = fun c => (↑c).support.card
-- Mathlib.Algebra.Group.Pi.Units
Pi.instSubsingletonUnits : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] [∀ (i : ι), Subsingleton (M i)ˣ],
  Subsingleton ((i : ι) → M i)ˣ
-- Mathlib.CategoryTheory.Subobject.FactorThru
CategoryTheory.Subobject.le_of_factors : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Y : C} {P Q : CategoryTheory.Subobject Y},
  Q.Factors P.arrow → P ≤ Q
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.IsThreeCycle.inv : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {f : Equiv.Perm α}, f.IsThreeCycle → f⁻¹.IsThreeCycle
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.integrable_mul_const_iff : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {𝕜 : Type u_8} [inst : NormedRing 𝕜] {c : 𝕜},
  IsUnit c → ∀ (f : α → 𝕜), MeasureTheory.Integrable (fun x => f x * c) μ ↔ MeasureTheory.Integrable f μ
-- Init.Data.SInt.Lemmas
Int32.ofInt_iSizeToInt : ∀ (x : ISize), Int32.ofInt x.toInt = x.toInt32
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.core.sizeOf_spec : ∀ (e : Lean.Expr), sizeOf (Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.core e) = 1 + sizeOf e
-- Mathlib.RingTheory.Binomial
Ring.multichoose_neg_succ : ∀ (n : ℕ), Ring.multichoose (-↑n) (n + 1) = 0
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
HomotopicalAlgebra.BifibrantObject.HoCat.homEquivLeft.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {X Y : C}
  [inst_2 : HomotopicalAlgebra.IsCofibrant X] [inst_3 : HomotopicalAlgebra.IsCofibrant Y]
  [inst_4 : HomotopicalAlgebra.IsFibrant X] [inst_5 : HomotopicalAlgebra.IsFibrant Y],
  HomotopicalAlgebra.BifibrantObject.HoCat.homEquivLeft =
    HomotopicalAlgebra.leftHomotopyClassEquivRightHomotopyClass.trans
      HomotopicalAlgebra.BifibrantObject.HoCat.homEquivRight
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.NormalWord.base_smul_eq_smul : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
  {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} [inst_2 : DecidableEq ι]
  [inst_3 : (i : ι) → DecidableEq (G i)] (h : H) (w : Monoid.PushoutI.NormalWord d),
  (Monoid.PushoutI.base φ) h • w = h • w