mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Prod
AddMonoidHom.coprod_apply : ∀ {M : Type u_3} {N : Type u_4} {P : Type u_5} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
  [inst_2 : AddCommMonoid P] (f : M →+ P) (g : N →+ P) (p : M × N), (f.coprod g) p = f p.1 + g p.2
-- Mathlib.Data.Vector.Snoc
/-- Append a single element to the end of a vector  -/
List.Vector.snoc : {α : Type u_1} → {n : ℕ} → List.Vector α n → α → List.Vector α (n + 1)
-- Mathlib.Analysis.Calculus.FDeriv.Mul
HasFDerivAt.smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {x : E} {𝕜' : Type u_5} [inst_5 : NormedRing 𝕜'] [inst_6 : NormedAlgebra 𝕜 𝕜'] [inst_7 : Module 𝕜' F]
  [inst_8 : IsBoundedSMul 𝕜' F] [inst_9 : IsScalarTower 𝕜 𝕜' F] {c : E → 𝕜'} {c' : E →L[𝕜] 𝕜'},
  HasFDerivAt c c' x → HasFDerivAt f f' x → HasFDerivAt (c • f) (c x • f' + c'.smulRight (f x)) x
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.mk_mul_lt_mk_right_iff : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {a b : M},
  MulArchimedeanClass.mk (a * b) < MulArchimedeanClass.mk b ↔ MulArchimedeanClass.mk a < MulArchimedeanClass.mk b
-- Mathlib.Analysis.InnerProductSpace.OfNorm
InnerProductSpaceable.to_uniformConvexSpace : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [InnerProductSpaceable E] [NormedSpace ℝ E], UniformConvexSpace E
-- Mathlib.Logic.Equiv.Defs
Equiv.comp_bijective : ∀ {α : Sort u} {β : Sort v} {γ : Sort w} (f : α → β) (e : β ≃ γ), Function.Bijective (⇑e ∘ f) ↔ Function.Bijective f
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.contains_eq_containsₘ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (a : α),
  m.contains a = m.containsₘ a
-- Mathlib.RingTheory.PowerSeries.Trunc
_private.Mathlib.RingTheory.PowerSeries.Trunc.0.PowerSeries.truncAux.eq_1 : ∀ {R : Type u_1} [inst : Semiring R] (n : ℕ) (φ : PowerSeries R),
  PowerSeries.truncAux✝ n φ = ∑ m ∈ Finset.Ico 0 n, (Polynomial.monomial m) ((PowerSeries.coeff m) φ)
-- Init.System.ST
ST.Prim.Ref.modifyGetUnsafe : {σ α β : Type} → ST.Ref σ α → (α → β × α) → ST σ β
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- For `𝓕 : Filter (β × β)`, this is the filter generated by the filter basis
`UniformFun.basis α β 𝓕`. For `𝓕 = 𝓤 β`, this will be the uniformity of uniform
convergence on `α`.  -/
UniformFun.filter : (α : Type u_1) → (β : Type u_2) → Filter (β × β) → Filter (UniformFun α β × UniformFun α β)
-- Mathlib.Algebra.Group.Submonoid.Pointwise
AddSubmonoid.closure_neg : ∀ {G : Type u_2} [inst : AddGroup G] (s : Set G), AddSubmonoid.closure (-s) = -AddSubmonoid.closure s
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.collectUniverseConstraints.go : Array Lean.Elab.Command.InductiveView →
  Lean.Level →
    ℕ →
      ℕ →
        List Lean.InductiveType → Array Lean.LMVarId → StateT Lean.Elab.Command.AccLevelState✝ Lean.Elab.TermElabM Unit
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.rpow_eq_top_iff_of_pos : ∀ {x : ENNReal} {y : ℝ}, 0 < y → (x ^ y = ⊤ ↔ x = ⊤)
-- Mathlib.Algebra.Order.GroupWithZero.Basic
pow_le_of_le_one : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : Preorder M₀] {a : M₀} {n : ℕ} [PosMulMono M₀],
  0 ≤ a → a ≤ 1 → n ≠ 0 → a ^ n ≤ a
-- Mathlib.Data.Num.Bitwise
/-- Bitwise "and" for `Num`.  -/
Num.land : Num → Num → Num
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
ContMDiff.mdifferentiableAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M} {n : WithTop ℕ∞},
  ContMDiff I I' n f → n ≠ 0 → MDiffAt f x
-- Mathlib.Order.Basic
min_rec : ∀ {α : Type u_2} [inst : LinearOrder α] {a b : α} {p : α → Prop}, (a ≤ b → p a) → (b ≤ a → p b) → p (min a b)
-- Mathlib.Algebra.Homology.Embedding.RestrictionHomology
HomologicalComplex.pOpcycles_restrictionOpcyclesIso_inv : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsRelIff] (i j : ι) (hi : c.prev j = i) {i' j' : ι'}
  (hi' : e.f i = i') (hj' : e.f j = j') (hi'' : c'.prev j' = i') [inst_3 : K.HasHomology j']
  [inst_4 : (K.restriction e).HasHomology j],
  CategoryTheory.CategoryStruct.comp (K.pOpcycles j') (K.restrictionOpcyclesIso e i j hi hi' hj' hi'').inv =
    CategoryTheory.CategoryStruct.comp (K.restrictionXIso e hj').inv ((K.restriction e).pOpcycles j)
-- Mathlib.Geometry.Diffeology.Basic
Diffeology.IsDTopologyCompatible.dTop_eq : ∀ (X : Type u_1) {t : TopologicalSpace X} {inst : DiffeologicalSpace X} [self : Diffeology.IsDTopologyCompatible X],
  Diffeology.dTopology = t
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.coe_div : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) (x y : ↥H), ↑(x / y) = ↑x / ↑y
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Pi.map.eq_1 : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : β → C}
  [inst_1 : CategoryTheory.Limits.HasProduct f] [inst_2 : CategoryTheory.Limits.HasProduct g] (p : (b : β) → f b ⟶ g b),
  CategoryTheory.Limits.Pi.map p = CategoryTheory.Limits.limMap (CategoryTheory.Discrete.natTrans fun X => p X.as)
-- Mathlib.Algebra.Lie.SkewAdjoint
skewAdjointMatricesLieSubalgebraEquiv.eq_1 : ∀ {R : Type u} {n : Type w} [inst : CommRing R] [inst_1 : Fintype n] (J : Matrix n n R) [inst_2 : DecidableEq n]
  (P : Matrix n n R) (h : Invertible P),
  skewAdjointMatricesLieSubalgebraEquiv J P h =
    LieEquiv.ofSubalgebras (skewAdjointMatricesLieSubalgebra J) (skewAdjointMatricesLieSubalgebra (P.transpose * J * P))
      (P.lieConj h).symm ⋯
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.mul_mk : ∀ {α : Type u} {L₁ L₂ : List (α × Bool)}, FreeGroup.mk L₁ * FreeGroup.mk L₂ = FreeGroup.mk (L₁ ++ L₂)
-- Mathlib.Algebra.Module.SpanRank
Submodule.spanFinrank_top : ∀ {R : Type u_1} {M : Type u} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (p : Submodule R M),
  ⊤.spanFinrank = p.spanFinrank
-- Mathlib.Topology.Algebra.UniformConvergence
instInvUniformFun : {α : Type u_1} → {β : Type u_2} → [Inv β] → Inv (UniformFun α β)
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.minEntry?ₘ'.match_1.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} [inst : Ord α]
  (motive : (Std.DTreeMap.Internal.Impl.ExplorationStep α β fun x => Ordering.lt) → Sort u_3) (ky : α)
  (a : Ordering.lt = Ordering.lt) (y : β ky) (a_1 : List ((a : α) × β a))
  (h_1 :
    (ky : α) →
      (a : Ordering.lt = Ordering.lt) →
        (y : β ky) → (a_2 : List ((a : α) × β a)) → motive (Std.DTreeMap.Internal.Impl.ExplorationStep.lt ky a y a_2))
  (h_2 :
    (a : List ((a : α) × β a)) →
      (a_2 : Std.DTreeMap.Internal.Cell α β fun x => Ordering.lt) →
        (r : List ((a : α) × β a)) → motive (Std.DTreeMap.Internal.Impl.ExplorationStep.eq a a_2 r)),
  (match Std.DTreeMap.Internal.Impl.ExplorationStep.lt ky a y a_1 with
    | Std.DTreeMap.Internal.Impl.ExplorationStep.lt ky a y a_2 => h_1 ky a y a_2
    | Std.DTreeMap.Internal.Impl.ExplorationStep.eq a a_2 r => h_2 a a_2 r) =
    h_1 ky a y a_1
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.getKey_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [inst : Std.TransCmp cmp] {k : α} {hk : k ∈ t₁}
  (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂), t₁.get k hk = t₂.get k ⋯
-- Mathlib.LinearAlgebra.Matrix.ZPow
Matrix.zpow_sub : ∀ {n' : Type u_1} [inst : DecidableEq n'] [inst_1 : Fintype n'] {R : Type u_2} [inst_2 : CommRing R]
  {A : Matrix n' n' R}, IsUnit A.det → ∀ (z1 z2 : ℤ), A ^ (z1 - z2) = A ^ z1 / A ^ z2
-- Mathlib.Topology.Algebra.Group.Basic
continuousOn_zsmul : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G] {s : Set G} (z : ℤ),
  ContinuousOn (fun x => z • x) s
-- Mathlib.Algebra.Group.Submonoid.Membership
AddSubmonoid.closure_eq_mrange : ∀ {M : Type u_1} [inst : AddMonoid M] (s : Set M),
  AddSubmonoid.closure s = AddMonoidHom.mrange (FreeAddMonoid.lift Subtype.val)
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.zmodRepr_spec : ∀ {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (x : ℤ_[p]), x.zmodRepr < p ∧ x - ↑x.zmodRepr ∈ IsLocalRing.maximalIdeal ℤ_[p]
-- Mathlib.Data.Multiset.ZeroCons
Multiset.rel_iff : ∀ {α : Type u_1} {β : Type v} (r : α → β → Prop) (a : Multiset α) (a_1 : Multiset β),
  Multiset.Rel r a a_1 ↔
    a = 0 ∧ a_1 = 0 ∨ ∃ a_2 b as bs, r a_2 b ∧ Multiset.Rel r as bs ∧ a = a_2 ::ₘ as ∧ a_1 = b ::ₘ bs
-- Mathlib.Control.ULift
ULift.rec.constant : ∀ {α : Type u} {β : Sort v} (b : β), (ULift.rec fun x => b) = fun x => b
-- Mathlib.Analysis.Normed.Lp.lpSpace
/-- The property that `f : ∀ i : α, E i`
* is finitely supported, if `p = 0`, or
* admits an upper bound for `Set.range (fun i ↦ ‖f i‖)`, if `p = ∞`, or
* has the series `∑' i, ‖f i‖ ^ p` be summable, if `0 < p < ∞`.  -/
Memℓp : {α : Type u_3} → {E : α → Type u_4} → [(i : α) → NormedAddCommGroup (E i)] → ((i : α) → E i) → ENNReal → Prop
-- Mathlib.Algebra.Group.Finsupp
Finsupp.mapRange_neg : ∀ {ι : Type u_1} {G : Type u_6} {H : Type u_7} [inst : NegZeroClass G] [inst_1 : NegZeroClass H] {f : G → H}
  {hf : f 0 = 0}, (∀ (x : G), f (-x) = -f x) → ∀ (v : ι →₀ G), Finsupp.mapRange f hf (-v) = -Finsupp.mapRange f hf v
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
indicator_iUnion_of_pairwise_disjoint : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] (s : γ → Set β),
  Pairwise (Function.onFun Disjoint s) →
    ∀ (f : β → α), (⋃ d, s d).indicator f = fun i => ∑' (d : γ), (s d).indicator f i
-- Lean.Meta.WHNF
Lean.Meta.ReduceMatcherResult.stuck : Lean.Expr → Lean.Meta.ReduceMatcherResult
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.sup_mul_left : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Mul α] {β : Type u_5} [inst_2 : SemilatticeSup β]
  [inst_3 : OrderBot β] (s t : Finset α) (f : α → β), (s * t).sup f = s.sup fun x => t.sup fun x_1 => f (x * x_1)
-- Mathlib.Algebra.GroupWithZero.Defs
IsRightCancelMulZero.to_noZeroDivisors : ∀ (M₀ : Type u_1) [inst : MulZeroClass M₀] [IsRightCancelMulZero M₀], NoZeroDivisors M₀
-- Mathlib.Topology.Category.FinTopCat
FinTopCat.mk.sizeOf_spec : ∀ (toTop : TopCat) [fintype : Fintype ↑toTop],
  sizeOf { toTop := toTop, fintype := fintype } = 1 + sizeOf toTop + sizeOf fintype
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.instPow : {ι : Type u_1} →
  (R : ι → Type u_2) →
    {𝓕 : Filter ι} →
      {S : ι → Type u_3} →
        [inst : (i : ι) → SetLike (S i) (R i)] →
          {B : (i : ι) → S i} →
            [inst_1 : (i : ι) → Monoid (R i)] →
              [∀ (i : ι), SubmonoidClass (S i) (R i)] → Pow (RestrictedProduct (fun i => R i) (fun i => ↑(B i)) 𝓕) ℕ
-- Mathlib.Algebra.Group.Defs
npowBinRec.go.eq_1 : ∀ {M : Type u_2} [inst : Mul M] (k : ℕ),
  npowBinRec.go k =
    Nat.binaryRec (motive := fun x => M → M → M) (fun y x => y)
      (fun bn _n fn y x => fn (bif bn then y * x else y) (x * x)) k
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax
CategoryTheory.Lax.OplaxTrans.whiskerLeft_as_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G H : CategoryTheory.LaxFunctor B C} (η : F ⟶ G) {θ ι : G ⟶ H} (Γ : θ ⟶ ι) (a : B),
  (CategoryTheory.Lax.OplaxTrans.whiskerLeft η Γ).as.app a =
    CategoryTheory.Bicategory.whiskerLeft (η.app a) (Γ.as.app a)
-- Mathlib.Geometry.Manifold.MFDeriv.Tangent
/-- The derivative of the chart at a base point is the chart of the tangent bundle, composed with
the identification between the tangent bundle of the model space and the product space.  -/
tangentMap_chart : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [inst_6 : IsManifold I 1 M] {p q : TangentBundle I M},
  q.proj ∈ (chartAt H p.proj).source →
    tangentMap I I (↑(chartAt H p.proj)) q = (Bundle.TotalSpace.toProd H E).symm (↑(chartAt (ModelProd H E) p) q)
-- Mathlib.Topology.VectorBundle.Riemannian
Bundle.RiemannianMetric.mk.inj : ∀ {B : Type u_4} {E : B → Type u_6} {inst : (b : B) → TopologicalSpace (E b)} {inst_1 : (b : B) → AddCommGroup (E b)}
  {inst_2 : (b : B) → Module ℝ (E b)} {inner : (b : B) → E b →L[ℝ] E b →L[ℝ] ℝ}
  {symm : ∀ (b : B) (v w : E b), ((inner b) v) w = ((inner b) w) v}
  {pos : ∀ (b : B) (v : E b), v ≠ 0 → 0 < ((inner b) v) v}
  {continuousAt : ∀ (b : B), ContinuousAt (fun v => ((inner b) v) v) 0}
  {isVonNBounded : ∀ (b : B), Bornology.IsVonNBounded ℝ {v | ((inner b) v) v < 1}}
  {inner_1 : (b : B) → E b →L[ℝ] E b →L[ℝ] ℝ} {symm_1 : ∀ (b : B) (v w : E b), ((inner_1 b) v) w = ((inner_1 b) w) v}
  {pos_1 : ∀ (b : B) (v : E b), v ≠ 0 → 0 < ((inner_1 b) v) v}
  {continuousAt_1 : ∀ (b : B), ContinuousAt (fun v => ((inner_1 b) v) v) 0}
  {isVonNBounded_1 : ∀ (b : B), Bornology.IsVonNBounded ℝ {v | ((inner_1 b) v) v < 1}},
  { inner := inner, symm := symm, pos := pos, continuousAt := continuousAt, isVonNBounded := isVonNBounded } =
      { inner := inner_1, symm := symm_1, pos := pos_1, continuousAt := continuousAt_1,
        isVonNBounded := isVonNBounded_1 } →
    inner = inner_1
-- Mathlib.Order.Filter.Ring
Filter.Germ.instIsOrderedRing : ∀ {α : Type u} {β : Type v} {l : Filter α} [inst : Semiring β] [inst_1 : PartialOrder β] [IsOrderedRing β],
  IsOrderedRing (l.Germ β)
-- Mathlib.Algebra.Quaternion
Quaternion.instRing : {R : Type u_3} → [inst : CommRing R] → Ring (Quaternion R)
-- Mathlib.RingTheory.TwoSidedIdeal.Operations
TwoSidedIdeal.top_asIdeal : ∀ {R : Type u_1} [inst : Ring R], TwoSidedIdeal.asIdeal ⊤ = ⊤
-- Mathlib.Order.Hom.Basic
OrderIso.equivEmbeddingSurjective_symm_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β] (f : { f // Function.Surjective ⇑f }),
  OrderIso.equivEmbeddingSurjective.symm f = OrderIso.ofSurjective ↑f ⋯
-- Init.Sym.Lemmas
Lean.Sym.Int32.eq_eq_false : ∀ (a b : Int32), decide (a = b) = false → (a = b) = False
-- Init.Prelude
Nat.lt_of_le_of_ne : ∀ {n m : ℕ}, n ≤ m → ¬n = m → n < m
-- Init.Prelude
instMonadEvalOfMonadLift : {m : Type u_1 → Type u_2} → {n : Type u_1 → Type u_3} → [MonadLift m n] → MonadEval m n
-- Mathlib.Algebra.Group.Ext
AddCommMonoid.ext : ∀ {M : Type u_1} ⦃m₁ m₂ : AddCommMonoid M⦄, HAdd.hAdd = HAdd.hAdd → m₁ = m₂
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
AntitoneOn.sSup_image_Icc : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : ConditionallyCompleteLattice β] {f : α → β} {a b : α},
  b ≤ a → AntitoneOn f (Set.Icc b a) → sSup (f '' Set.Icc b a) = f b
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey!_insertIfNew!_le_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α],
  t.WF → ∀ {k : α} {v : β k}, (compare (Std.DTreeMap.Internal.Impl.insertIfNew! k v t).minKey! k).isLE = true
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey?_eq_some_getKey! : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {a : α}, a ∈ m → m.getKey? a = some (m.getKey! a)
-- Std.Http.Data.URI.Basic
Std.Http.instInhabitedRequestTarget.default : Std.Http.RequestTarget
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.Φ_two : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R),
  W.Φ 2 =
    Polynomial.X ^ 4 - Polynomial.C W.b₄ * Polynomial.X ^ 2 - Polynomial.C (2 * W.b₆) * Polynomial.X - Polynomial.C W.b₈
-- Mathlib.Data.Sum.Interval
Sum.Lex.Ico_inl_inl : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : LocallyFiniteOrder β] [inst_4 : LocallyFiniteOrderTop α] [inst_5 : LocallyFiniteOrderBot β] (a₁ a₂ : α),
  Finset.Ico (Sum.inlₗ a₁) (Sum.inlₗ a₂) =
    Finset.map (Function.Embedding.inl.trans toLex.toEmbedding) (Finset.Ico a₁ a₂)
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
/-- A precylinder for `A : C` is the data of a morphism
`π : I ⟶ A` equipped with two sections.  -/
HomotopicalAlgebra.Precylinder : {C : Type u} → [CategoryTheory.Category.{v, u} C] → C → Type (max u v)
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
/-- **Alias** of `Matrix.charpoly_of_isUpperTriangular`. -/
Matrix.charpoly_of_upperTriangular : ∀ {R : Type u_1} [inst : CommRing R] {n : Type u_4} [inst_1 : DecidableEq n] [inst_2 : Fintype n]
  [inst_3 : LinearOrder n] (M : Matrix n n R),
  M.IsUpperTriangular → M.charpoly = ∏ i, (Polynomial.X - Polynomial.C (M i i))
-- Mathlib.CategoryTheory.Filtered.Small
CategoryTheory.IsFiltered.instEssentiallySmallFullSubcategoryFilteredClosure : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsFilteredOrEmpty C] {α : Type w}
  (f : α → C),
  CategoryTheory.EssentiallySmall.{max v w, v, u} (CategoryTheory.IsFiltered.filteredClosure f).FullSubcategory
-- Lean.Meta.Basic
Lean.Meta.instInhabitedInfoCacheKey.default : Lean.Meta.InfoCacheKey
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.nonempty_def : ∀ (u : ZFSet.{u_1}), u.Nonempty ↔ ∃ x, x ∈ u
-- Mathlib.NumberTheory.FLT.Three
/-- Given `S' : Solution'`, we have that `2 ≤ S'.multiplicity`.  -/
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution'.two_le_multiplicity : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S' : FermatLastTheoremForThreeGen.Solution'✝ hζ)
  [inst_1 : NumberField K] [IsCyclotomicExtension {3} ℚ K], 2 ≤ FermatLastTheoremForThreeGen.Solution'.multiplicity✝ S'
-- Mathlib.Topology.MetricSpace.MetricSeparated
Metric.IsSeparated.anti : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {s : Set X} {ε δ : ENNReal},
  ε ≤ δ → Metric.IsSeparated δ s → Metric.IsSeparated ε s
-- Mathlib.Algebra.Ring.GeomSum
one_geom_sum : ∀ {R : Type u_1} [inst : Semiring R] (n : ℕ), ∑ i ∈ Finset.range n, 1 ^ i = ↑n
-- Batteries.Recycling.RBTree.Basic
/-- The ordering invariant of a red-black tree, which is a binary search tree.
This says that every element of a left subtree is less than the root, and
every element in the right subtree is greater than the root, where the
less than relation `x < y` is understood to mean `cmp x y = .lt`.

Because we do not assume that `cmp` is lawful when stating this property,
we write it in such a way that if `cmp` is not lawful then the condition holds trivially.
That way we can prove the ordering invariants without assuming `cmp` is lawful.
 -/
RBTree.RBNode.Ordered : {α : Type u_1} → (α → α → Ordering) → RBTree.RBNode α → Prop
-- Mathlib.Analysis.SpecialFunctions.Exponential
Real.exp_eq_exp_ℝ : Real.exp = NormedSpace.exp
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero
/-- A homology data saying that the singular homology in degree `0`
of a simplicial set with coefficients in `R` identify to a coproduct
of copies of `X` indexed by `π₀ X`.  -/
SSet.homologyData₀ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasCoproducts C] →
      [inst_2 : CategoryTheory.Preadditive C] →
        (X : SSet) → (R : C) → (HomologicalComplex.sc' (X.chainComplex R) 1 0 0).HomologyData
-- Init.Notation
/-- `a ||| b` computes the bitwise OR of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `|||` in identifiers is `or`. -/
«term_|||_» : Lean.TrailingParserDescr
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKey!_modify_eq_maxKey! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [inst_2 : Inhabited α] {k : α} {f : β → β}, (t.modify k f).maxKey! = t.maxKey!
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
/-- A special case of `CategoryTheory.Limits.cokernel.map` adapted to `explicitCokernel`.  -/
SemiNormedGrp.explicitCokernel.map : {A B C D : SemiNormedGrp} →
  {fab : A ⟶ B} →
    {fbd : B ⟶ D} →
      {fac : A ⟶ C} →
        {fcd : C ⟶ D} →
          CategoryTheory.CategoryStruct.comp fab fbd = CategoryTheory.CategoryStruct.comp fac fcd →
            (SemiNormedGrp.explicitCokernel fab ⟶ SemiNormedGrp.explicitCokernel fcd)
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
OpenPartialHomeomorph.extend_image_target_mem_nhds : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  (f : OpenPartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} {x : M},
  x ∈ f.source → ↑I '' f.target ∈ nhdsWithin (↑(f.extend I) x) (Set.range ↑I)
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.fst_comp_inl : ∀ {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst_1 : Monoid N],
  Monoid.Coprod.fst.comp Monoid.Coprod.inl = MonoidHom.id M
-- Mathlib.Algebra.Module.ZLattice.Basic
ZSpan.smul : ∀ {E : Type u_1} {ι : Type u_2} {K : Type u_3} [inst : NormedField K] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace K E] (b : Module.Basis ι K E) {c : K} (hc : c ≠ 0),
  c • Submodule.span ℤ (Set.range ⇑b) = Submodule.span ℤ (Set.range ⇑(b.isUnitSMul ⋯))
-- Mathlib.Algebra.Group.Action.Prod
Prod.addAction : {M : Type u_1} →
  {α : Type u_5} → {β : Type u_6} → [inst : AddMonoid M] → [AddAction M α] → [AddAction M β] → AddAction M (α × β)
-- Mathlib.CategoryTheory.Sites.Sheaf
CategoryTheory.sheafSectionsNatIsoEvaluation_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u₂)
  [inst_1 : CategoryTheory.Category.{v₂, u₂} A] {X : C} (X_1 : CategoryTheory.Sheaf J A),
  (CategoryTheory.sheafSectionsNatIsoEvaluation J A).hom.app X_1 =
    CategoryTheory.CategoryStruct.id (X_1.obj.obj (Opposite.op X))
-- Mathlib.Geometry.Manifold.VectorBundle.Hom
_private.Mathlib.Geometry.Manifold.VectorBundle.Hom.0.termLE₁E₂ : Lean.ParserDescr
-- Mathlib.Tactic.Ring.Compare
/-- **Alias** of `Mathlib.Tactic.Ring.leOfPartialOrder`.

---

`PartialOrder` implies `LE`.  -/
Mathlib.Tactic.Ring.le_of_po : (α : Type u_1) → [PartialOrder α] → LE α
-- Mathlib.Order.SuccPred.IntervalSucc
/-- If `α` is a linear succ order, `β` is a preorder, and `f : α → β` is a monotone function, then
the intervals `Set.Ioc (f n) (f (Order.succ n))` are pairwise disjoint.  -/
Monotone.pairwise_disjoint_on_Ioc_succ : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : SuccOrder α] [inst_2 : Preorder β] {f : α → β},
  Monotone f → Pairwise (Function.onFun Disjoint fun n => Set.Ioc (f n) (f (Order.succ n)))
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidHom.coe_addMonoidHom : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : AddZeroClass α]
  [inst_3 : AddZeroClass β] (f : α →+o β), ⇑↑f = ⇑f
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
/-- The condition that a cochain complex `K` is (cohomologically) `≤ n`.  -/
CochainComplex.IsLE : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] → CochainComplex C ℤ → ℤ → Prop