mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.b₈_of_char_two : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) [CharP R 2],
  W.b₈ = W.a₁ ^ 2 * W.a₆ + W.a₁ * W.a₃ * W.a₄ + W.a₂ * W.a₃ ^ 2 + W.a₄ ^ 2
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey!_erase_eq_of_not_compare_minKey!_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α]
  {k : α}, (t.erase k).isEmpty = false → ¬cmp k t.minKey! = Ordering.eq → (t.erase k).minKey! = t.minKey!
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.categoryStruct_comp_naturality_inv : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {X Y Z : CategoryTheory.Pseudofunctor B C} (η : X.StrongTrans Y) (θ : Y.StrongTrans Z) {a b : B} (f : a ⟶ b),
  ((CategoryTheory.CategoryStruct.comp η θ).naturality f).inv =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (η.app a) (θ.app a) (Z.map f)).hom
            (CategoryTheory.Bicategory.whiskerLeft (η.app a) (θ.naturality f).inv))
          (CategoryTheory.Bicategory.associator (η.app a) (Y.map f) (θ.app b)).inv)
        (CategoryTheory.Bicategory.whiskerRight (η.naturality f).inv (θ.app b)))
      (CategoryTheory.Bicategory.associator (X.map f) (η.app b) (θ.app b)).hom
-- Mathlib.ModelTheory.DirectLimit
FirstOrder.Language.DirectLimit.funMap_quotient_mk'_sigma_mk' : ∀ {L : FirstOrder.Language} {ι : Type v} [inst : Preorder ι] (G : ι → Type w) [inst_1 : (i : ι) → L.Structure (G i)]
  (f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j)) [inst_2 : IsDirectedOrder ι]
  [inst_3 : DirectedSystem G fun i j h => ⇑(f i j h)] [inst_4 : Nonempty ι] {n : ℕ} {F : L.Functions n} {i : ι}
  {x : Fin n → G i},
  (FirstOrder.Language.Structure.funMap F fun a => ⟦FirstOrder.Language.Structure.Sigma.mk f i (x a)⟧) =
    ⟦FirstOrder.Language.Structure.Sigma.mk f i (FirstOrder.Language.Structure.funMap F x)⟧
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Trivialization.symm_continuousLinearEquivAt_eq : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : NontriviallyNormedField R]
  [inst_1 : (x : B) → AddCommMonoid (E x)] [inst_2 : (x : B) → Module R (E x)] [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace R F] [inst_5 : TopologicalSpace B] [inst_6 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_7 : (x : B) → TopologicalSpace (E x)] [inst_8 : FiberBundle F E]
  (e : Bundle.Trivialization F Bundle.TotalSpace.proj) [inst_9 : Bundle.Trivialization.IsLinear R e] {b : B}
  (hb : b ∈ e.baseSet),
  ⇑(Bundle.Trivialization.continuousLinearEquivAt R e b hb).symm = ⇑(Bundle.Trivialization.symmL R e b)
-- Mathlib.Probability.Distributions.Gaussian.CharFun
ProbabilityTheory.IsGaussian.charFun_eq' : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [SecondCountableTopology E] [CompleteSpace E]
  [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] {μ : MeasureTheory.Measure E} [inst_5 : InnerProductSpace ℝ E]
  [ProbabilityTheory.IsGaussian μ] (t : E),
  MeasureTheory.charFun μ t =
    Complex.exp (↑(inner ℝ t (∫ (x : E), id x ∂μ)) * Complex.I - ↑(((ProbabilityTheory.covarianceBilin μ) t) t) / 2)
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
mem_measurableAtom_self : ∀ {β : Type u_2} [inst : MeasurableSpace β] (x : β), x ∈ measurableAtom x
-- Mathlib.Algebra.Homology.Embedding.RestrictionHomology
HomologicalComplex.restriction.sc'Iso_hom_τ₂ : ∀ {ι : 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 k : ι) {i' j' k' : ι'}
  (hi' : e.f i = i') (hj' : e.f j = j') (hk' : e.f k = k') (hi'' : c'.prev j' = i') (hk'' : c'.next j' = k'),
  (HomologicalComplex.restriction.sc'Iso K e i j k hi' hj' hk' hi'' hk'').hom.τ₂ = (K.restrictionXIso e hj').hom
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.Nonempty.of_vsub_left : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] [inst_1 : DecidableEq α] {s t : Finset β},
  (s -ᵥ t).Nonempty → s.Nonempty
-- Mathlib.Computability.Encoding
/-- The decoding function  -/
Computability.Encoding.decode : {α : Type u} → {Γ : Type v} → Computability.Encoding α Γ → List Γ → Option α
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.Decidable.isLongestRevMatchAtChain_iff_isLongestRevMatchAtChain_decide : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String.Slice} {pos pos' : s.Pos},
  String.Slice.Pattern.Model.IsLongestRevMatchAtChain p pos pos' ↔
    String.Slice.Pattern.Model.IsLongestRevMatchAtChain (fun x => decide (p x)) pos pos'
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.mapCycles₂_comp_assoc : ∀ {k : Type u} [inst : CommRing k] {G H K : Type u} [inst_1 : Group G] [inst_2 : Group H] [inst_3 : Group K]
  {A : Rep.{u, u, u} k G} {B : Rep.{u, u, u} k H} {C : Rep.{u, u, u} k K} (f : G →* H) (g : H →* K)
  (φ : A ⟶ Rep.res f B) (ψ : B ⟶ Rep.res g C) {Z : ModuleCat k} (h : ModuleCat.of k ↥(groupHomology.cycles₂ C) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (groupHomology.mapCycles₂ (g.comp f) (CategoryTheory.CategoryStruct.comp φ (Rep.resMap f ψ))) h =
    CategoryTheory.CategoryStruct.comp (groupHomology.mapCycles₂ f φ)
      (CategoryTheory.CategoryStruct.comp (groupHomology.mapCycles₂ g ψ) h)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry!_cons_of_true : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k}
  [inst_1 : Inhabited ((a : α) × β a)], (k == a) = true → Std.Internal.List.getEntry! a (⟨k, v⟩ :: l) = ⟨k, v⟩
-- Mathlib.Algebra.Group.Defs
/-- Shortcut instance for `IsCommutativeHMul M → IsDedekindFiniteMonoid M`.

This is assigned default rather than low priority because it gives the most common examples
of Dedekind-finite monoids and is used the most often. Benchmark results indicate default
priority performs better than low or high priority.  -/
instIsDedekindFiniteMonoid : ∀ (M : Type u_2) [inst : CommMonoid M], IsDedekindFiniteMonoid M
-- Mathlib.Order.Fin.Clamp
Fin.clamp_monotone : ∀ {m : ℕ}, Monotone fun n => Fin.clamp n m
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.ofCoeff.injEq : ∀ (R : Type u_1) {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (coeff coeff_1 : ℕ →₀ M), ({ coeff := coeff } = { coeff := coeff_1 }) = (coeff = coeff_1)
-- Lean.Elab.Tactic.Basic
/-- Return the first goal, and remove it from the goal list.

See also: `Lean.Elab.Tactic.pushGoal` and `Lean.Elab.Tactic.pushGoals`.
 -/
Lean.Elab.Tactic.popMainGoal : Lean.Elab.Tactic.TacticM Lean.MVarId
-- Mathlib.Algebra.Quaternion
Quaternion.imK_zero : ∀ {R : Type u_3} [inst : CommRing R], QuaternionAlgebra.imK 0 = 0
-- Mathlib.Data.FunLike.Basic
DFunLike.coe_eq_coe_fn : ∀ {F : Sort u_1} {α : Sort u_2} {β : α → Sort u_3} [i : DFunLike F α β], DFunLike.coe = fun f => ⇑f
-- Mathlib.Topology.ClusterPt
ClusterPt.frequently : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {F : Filter X} {p : X → Prop},
  ClusterPt x F → (∀ᶠ (y : X) in nhds x, p y) → ∃ᶠ (y : X) in F, p y
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.max!_erase_le_max! : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.WF → ∀ {k : α}, (t.erase k).isEmpty = false → (cmp (t.erase k).max! t.max!).isLE = true
-- Mathlib.MeasureTheory.Group.Arithmetic
MeasurableSet.neg : ∀ {G : Type u_2} [inst : Neg G] [inst_1 : MeasurableSpace G] [MeasurableNeg G] {s : Set G},
  MeasurableSet s → MeasurableSet (-s)
-- Mathlib.Order.Interval.Set.Fin
Fin.image_castAdd_uIcc : ∀ {n : ℕ} (m : ℕ) (i j : Fin n), Fin.castAdd m '' Set.uIcc i j = Set.uIcc (Fin.castAdd m i) (Fin.castAdd m j)
-- Mathlib.Data.Int.Bitwise
Int.testBit_bit_zero : ∀ (b : Bool) (n : ℤ), (Int.bit b n).testBit 0 = b
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.coeIdeal_eq_zero' : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  [loc : IsLocalization S P] {I : Ideal R}, S ≤ nonZeroDivisors R → (↑I = 0 ↔ I = ⊥)
-- ProofWidgets.Component.PenroseDiagram
ProofWidgets.Penrose.DiagramState.mk.injEq : ∀ (sub : String) (embeds : Std.HashMap String (String × ProofWidgets.Html)) (sub_1 : String)
  (embeds_1 : Std.HashMap String (String × ProofWidgets.Html)),
  ({ sub := sub, embeds := embeds } = { sub := sub_1, embeds := embeds_1 }) = (sub = sub_1 ∧ embeds = embeds_1)
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
SimpleGraph.isUniform_singleton : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {G : SimpleGraph α}
  [inst_3 : DecidableRel G.Adj] {ε : 𝕜} {a b : α}, G.IsUniform ε {a} {b} ↔ 0 < ε
-- Mathlib.NumberTheory.Pell
/-- If we multiply a positive solution with the inverse of a fundamental solution,
the `y`-coordinate remains nonnegative.  -/
Pell.IsFundamental.mul_inv_y_nonneg : ∀ {d : ℤ} {a₁ : Pell.Solution₁ d},
  Pell.IsFundamental a₁ → ∀ {a : Pell.Solution₁ d}, 1 < a.x → 0 < a.y → 0 ≤ (a * a₁⁻¹).y
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
/-- The horn in the standard simplex corresponding to a cell
of a rank function for a proper pairing of a subcomplex of
a simplicial set.  -/
SSet.Subcomplex.Pairing.RankFunction.Cell.horn : {X : SSet} →
  {A : X.Subcomplex} →
    {P : A.Pairing} →
      {ι : Type v} →
        [inst : LinearOrder ι] →
          {f : P.RankFunction ι} →
            {i : ι} → (c : f.Cell i) → [P.IsProper] → (SSet.stdSimplex.obj { len := c.dim + 1 }).Subcomplex
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.reverse_surjective : ∀ {V : Type u} {G : SimpleGraph V} {u v : V}, Function.Surjective SimpleGraph.Walk.reverse
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
neg_add_lt_iff_lt_add' : ∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : LT α] [AddLeftStrictMono α] {a b c : α}, -c + a < b ↔ a < b + c
-- Mathlib.Algebra.Ring.Defs
NonAssocCommRing.mk : {α : Type u} → [toNonAssocRing : NonAssocRing α] → (∀ (a b : α), a * b = b * a) → NonAssocCommRing α
-- Mathlib.LinearAlgebra.Complex.Module
span_selfAdjoint : ∀ {A : Type u_1} [inst : AddCommGroup A] [inst_1 : Module ℂ A] [inst_2 : StarAddMonoid A] [StarModule ℂ A],
  Submodule.span ℂ ↑(selfAdjoint A) = ⊤
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
SSet.toNormalizedChainComplex_normalizedChainComplexMap_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] {X Y : SSet} (f : X ⟶ Y) (R : C) {Z : ChainComplex C ℕ}
  (h : Y.normalizedChainComplex R ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.toNormalizedChainComplex R)
      (CategoryTheory.CategoryStruct.comp (SSet.normalizedChainComplexMap f R) h) =
    CategoryTheory.CategoryStruct.comp (SSet.chainComplexMap f R)
      (CategoryTheory.CategoryStruct.comp (Y.toNormalizedChainComplex R) h)
-- Std.Data.DTreeMap.Basic
/-- Tries to retrieve the key-value pair with the largest key that is less than or equal to the
given key, returning `none` if no such pair exists.
 -/
Std.DTreeMap.getEntryLE? : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap α β cmp → α → Option ((a : α) × β a)
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.maximalSpectrumToPiLocalization_surjective_of_discreteTopology : ∀ (R : Type u) [inst : CommSemiring R] [DiscreteTopology (PrimeSpectrum R)],
  Function.Surjective ⇑(MaximalSpectrum.toPiLocalization R)
-- Mathlib.RingTheory.Algebraic.Basic
inv_eq_of_aeval_divX_ne_zero : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {x : L} {p : Polynomial K},
  (Polynomial.aeval x) p.divX ≠ 0 →
    x⁻¹ = (Polynomial.aeval x) p.divX / ((Polynomial.aeval x) p - (algebraMap K L) (p.coeff 0))
-- Mathlib.Topology.Algebra.Group.Quotient
QuotientGroup.isOpenQuotientMap_mk : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [SeparatelyContinuousMul G] {N : Subgroup G},
  IsOpenQuotientMap QuotientGroup.mk
-- Mathlib.MeasureTheory.Measure.NullMeasurable
MeasureTheory.Measure.IsComplete.mk : ∀ {α : Type u_2} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α},
  (∀ (s : Set α), μ s = 0 → MeasurableSet s) → μ.IsComplete
-- Mathlib.Analysis.LocallyConvex.AbsConvex
absConvexHull_eq_iInter : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] [inst_2 : AddCommMonoid E]
  [inst_3 : PartialOrder 𝕜] (s : Set E), (absConvexHull 𝕜) s = ⋂ t, ⋂ (_ : s ⊆ t), ⋂ (_ : AbsConvex 𝕜 t), t
-- Init.Omega.Coeffs
/-- Shim for `IntList.set`.  -/
Lean.Omega.Coeffs.set : Lean.Omega.Coeffs → ℕ → ℤ → Lean.Omega.Coeffs
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.coe_inv : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : InvolutiveInv α] (s : Finset α), ↑s⁻¹ = (↑s)⁻¹
-- Mathlib.Analysis.Normed.Group.Basic
norm_div_sub_norm_div_le_norm_div : ∀ {E : Type u_5} [inst : SeminormedGroup E] (u v w : E), ‖u / w‖ - ‖v / w‖ ≤ ‖u / v‖
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.uIcc.eq_1 : ∀ {α : Type u_1} [inst : Lattice α] (a b : α), Set.uIcc a b = Set.Icc (a ⊓ b) (a ⊔ b)
-- Mathlib.Algebra.Star.Basic
/-- `StarHomClass F R S` states that `F` is a type of `star`-preserving maps from `R` to `S`.  -/
StarHomClass : (F : Type u_1) → (R : outParam (Type u_2)) → (S : outParam (Type u_3)) → [Star R] → [Star S] → [FunLike F R S] → Prop
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.Hom.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X Y : C),
  (CategoryTheory.WithTerminal.of X).Hom (CategoryTheory.WithTerminal.of Y) = (X ⟶ Y)
-- Std.Internal.Do.WP.Conjunctive
/-- `ExceptT` lifts conjunctivity from its base monad.  -/
Std.Internal.Do.ExceptT.instWPConjunctive : ∀ {m : Type u → Type v} {ε α : Type u} {Pred : Type w} {EPred : Type z} [inst : Monad m]
  [inst_1 : Std.Internal.Do.Assertion Pred] [inst_2 : Std.Internal.Do.Assertion EPred]
  [inst_3 : Std.Internal.Do.WPMonad m Pred EPred]
  [Std.Internal.Do.WPConjunctive (m (Except ε α)) (Except ε α) Pred EPred],
  Std.Internal.Do.WPConjunctive (ExceptT ε m α) α Pred (EPost.Cons✝ (ε → Pred) EPred)
-- Mathlib.Algebra.IsPrimePow
Prime.isPrimePow : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {p : R}, Prime p → IsPrimePow p
-- Mathlib.Geometry.Manifold.Instances.Sphere
range_mfderiv_coe_sphere : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {n : ℕ}
  [inst_2 : Fact (Module.finrank ℝ E = n + 1)] (v : ↑(Metric.sphere 0 1)), (↑(mfderiv% Subtype.val v)).range = (ℝ ∙ ↑v)ᗮ
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.eq_zero_or_one : ∀ {K : Type u_4} {L : Type u_5} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [IsFractionRing K L]
  (I : FractionalIdeal (nonZeroDivisors K) L), I = 0 ∨ I = 1
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.minKey?_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.minKey? = t₂.minKey?
-- Init.GetElem
List.getElem?_eq_getElem : ∀ {α : Type u_1} {l : List α} {i : ℕ} (h : i < l.length), l[i]? = some l[i]
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_of_containsKey_filterMap : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : BEq α] [EquivBEq α] {f : (a : α) → β a → Option (γ a)}
  {l : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.containsKey k (List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) l) =
        true →
      Std.Internal.List.containsKey k l = true
-- Init.Data.List.Lemmas
List.contains_congr : ∀ {α : Type u_1} [inst : BEq α] [PartialEquivBEq α] {l : List α} {x y : α},
  (x == y) = true → l.contains x = l.contains y
-- Mathlib.Algebra.Category.CommAlgCat.Basic
CommAlgCat.hom_ext : ∀ {R : Type u} [inst : CommRing R] {A B : CommAlgCat R} {f g : A ⟶ B},
  CommAlgCat.Hom.hom f = CommAlgCat.Hom.hom g → f = g
-- Mathlib.Data.Nat.Factorization.Defs
/-- We introduce the notations `ordProj[p] n` for the largest power of the prime `p` that
divides `n` and `ordCompl[p] n` for the complementary part. The `ord` naming comes from
the $p$-adic order/valuation of a number, and `proj` and `compl` are for the projection and
complementary projection. The term `n.factorization p` is the $p$-adic order itself.
For example, `ordProj[2] n` is the even part of `n` and `ordCompl[2] n` is the odd part.  -/
Nat.«termOrdProj[_]_» : Lean.ParserDescr
-- Init.Data.Array.Lemmas
Array.forall_mem_push : ∀ {α : Type u_1} {p : α → Prop} {xs : Array α} {a : α}, (∀ x ∈ xs.push a, p x) ↔ p a ∧ ∀ x ∈ xs, p x
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
orderOf_eq_card_of_forall_mem_powers : ∀ {α : Type u_1} [inst : Group α] {g : α}, (∀ (x : α), x ∈ Submonoid.powers g) → orderOf g = Nat.card α
-- Mathlib.CategoryTheory.GradedObject.Unitor
CategoryTheory.GradedObject.ι_mapBifunctorLeftUnitor_hom_apply_assoc : ∀ {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : Zero I] [inst_3 : DecidableEq I]
  [inst_4 : CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) (X : C)
  (e : F.obj X ≅ CategoryTheory.Functor.id D)
  [inst_5 : ∀ (Y : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.flip.obj Y)]
  (p : I × J → J) (hp : ∀ (j : J), p (0, j) = j) (Y : CategoryTheory.GradedObject J D)
  [inst_6 :
    (((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj
          Y).HasMap
      p]
  (j : J) {Z : D} (h : Y j ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.GradedObject.ιMapBifunctorMapObj F p ((CategoryTheory.GradedObject.single₀ I).obj X) Y 0 j j ⋯)
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.GradedObject.mapBifunctorLeftUnitor F X e p hp Y).hom j) h) =
    CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.GradedObject.singleObjApplyIso 0 X).hom).app (Y j))
      (CategoryTheory.CategoryStruct.comp (e.hom.app (Y j)) h)
-- Mathlib.Algebra.CubicDiscriminant
Cubic.of_c_eq_zero' : ∀ {R : Type u_1} {d : R} [inst : Semiring R], { a := 0, b := 0, c := 0, d := d }.toPoly = Polynomial.C d
-- Mathlib.Analysis.Complex.Trigonometric
Complex.sin_three_mul : ∀ (x : ℂ), Complex.sin (3 * x) = 3 * Complex.sin x - 4 * Complex.sin x ^ 3
-- Lean.LibrarySuggestions.Basic
_private.Lean.LibrarySuggestions.Basic.0.Lean.Expr.FoldRelevantConstantsImpl.State.visitedConsts : Lean.Expr.FoldRelevantConstantsImpl.State✝ → Lean.NameHashSet
-- Mathlib.Order.Interval.Finset.Basic
Finset.uIcc_subset_uIcc_iff_le' : ∀ {α : Type u_2} [inst : Lattice α] [inst_1 : LocallyFiniteOrder α] {a₁ a₂ b₁ b₂ : α},
  Finset.uIcc a₁ b₁ ⊆ Finset.uIcc a₂ b₂ ↔ a₂ ⊓ b₂ ≤ a₁ ⊓ b₁ ∧ a₁ ⊔ b₁ ≤ a₂ ⊔ b₂
-- Mathlib.CategoryTheory.Presentable.Type
HasCardinalLT.Set.isFiltered_of_aleph0_le : ∀ (X : Type u) (κ : Cardinal.{u}), Cardinal.aleph0 ≤ κ → CategoryTheory.IsFiltered (HasCardinalLT.Set X κ)
-- Mathlib.Combinatorics.SimpleGraph.CycleGraph
_private.Mathlib.Combinatorics.SimpleGraph.CycleGraph.0.SimpleGraph.cycleGraph.cycleCons.match_1.splitter : (n : ℕ) →
  (motive : Fin (n + 3) → Sort u_1) →
    (x : Fin (n + 3)) →
      ((h : 0 < n + 3) → motive ⟨0, h⟩) → ((m : ℕ) → (h : m + 1 < n + 3) → motive ⟨m.succ, h⟩) → motive x
-- Mathlib.Data.Matrix.Basis
Matrix.sum_single_natCast : ∀ {m : Type u_2} {α : Type u_7} [inst : DecidableEq m] [inst_1 : AddCommMonoidWithOne α] [inst_2 : Fintype m] (n : ℕ),
  ∑ i, Matrix.single i i ↑n = ↑n
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Submonoid.subsemiringClosure_toAddSubmonoid : ∀ {R : Type u} [inst : NonAssocSemiring R] (M : Submonoid R),
  M.subsemiringClosure.toAddSubmonoid = AddSubmonoid.closure ↑M
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.MethodsRef.toMethods : Lean.Meta.Simp.MethodsRef → Lean.Meta.Simp.Methods
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidIso.toMulEquiv : {α : Type u_6} →
  {β : Type u_7} →
    [inst : Preorder α] → [inst_1 : Preorder β] → [inst_2 : Mul α] → [inst_3 : Mul β] → (α ≃*o β) → α ≃* β
-- Mathlib.Topology.ContinuousMap.Lattice
ContinuousMap.abs_apply : ∀ {α : Type u_1} [inst : TopologicalSpace α] {β : Type u_2} [inst_1 : TopologicalSpace β] [inst_2 : AddGroup β]
  [inst_3 : IsTopologicalAddGroup β] [inst_4 : Lattice β] [inst_5 : TopologicalLattice β] (f : C(α, β)) (x : α),
  |f| x = |f x|
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Icc.mk_one : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R] (h : 1 ∈ Set.Icc 0 1),
  ⟨1, h⟩ = 1
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instHashableLitValue : Hashable Lean.Compiler.LCNF.LitValue
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.π_natTransTruncGEOfLE_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a ≤ b) {Z : CategoryTheory.Functor C C}
  (h_1 : t.truncGE b ⟶ Z),
  CategoryTheory.CategoryStruct.comp (t.truncGEπ a)
      (CategoryTheory.CategoryStruct.comp (t.natTransTruncGEOfLE a b h) h_1) =
    CategoryTheory.CategoryStruct.comp (t.truncGEπ b) h_1
-- Init.Data.Int.Cooper
/-- `resolve_left` is bounded above by `lcm a (a * d / gcd (a * d) c)`.  -/
Int.Cooper.resolve_left_lt_lcm : ∀ (a c d p x : ℤ), 0 < a → 0 < d → p ≤ a * x → Int.Cooper.resolve_left a c d p x < ↑(a.lcm (a * d / ↑((a * d).gcd c)))
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.instInhabitedMCasesPat.default : Lean.Parser.Tactic.MCasesPat
-- Mathlib.Data.Multiset.ZeroCons
Multiset.card_eq_succ_iff : ∀ {α : Type u_1} {s : Multiset α} {n : ℕ}, s.card = n + 1 ↔ ∃ a t, a ::ₘ t = s ∧ t.card = n
-- Mathlib.Analysis.Normed.Group.Basic
abs_norm_sub_norm_le_norm_inv_mul : ∀ {E : Type u_5} [inst : SeminormedGroup E] (a b : E), |‖a‖ - ‖b‖| ≤ ‖a⁻¹ * b‖
-- Mathlib.Order.SuccPred.Limit
Order.IsSuccLimit.succ_lt_iff : ∀ {α : Type u_1} {a b : α} [inst : PartialOrder α] [inst_1 : SuccOrder α],
  Order.IsSuccLimit b → (Order.succ a < b ↔ a < b)
-- Mathlib.Topology.Category.Sequential
/-- Construct a homeomorphism from an isomorphism.  -/
Sequential.homeoOfIso : {X Y : Sequential} → (X ≅ Y) → ↑X.toTop ≃ₜ ↑Y.toTop
-- Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence
/-- Close the goal of the form `η = θ`, where `η` and `θ` are 2-isomorphisms made up only of
associators, unitors, and identities.
```lean
example {C : Type} [Category* C] [MonoidalCategory C] :
  (λ_ (𝟙_ C)).hom = (ρ_ (𝟙_ C)).hom := by
  monoidal_coherence
```
 -/
Mathlib.Tactic.Monoidal.tacticMonoidal_coherence : Lean.ParserDescr
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.isNormal_veblen : ∀ (o : Ordinal.{u_1}), Order.IsNormal (Ordinal.veblen o)
-- Mathlib.Topology.Order.IntermediateValue
intermediate_value_Ioc : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ] [OrderClosedTopology δ]
  {a b : α}, a ≤ b → ∀ {f : α → δ}, ContinuousOn f (Set.Icc a b) → Set.Ioc (f a) (f b) ⊆ f '' Set.Ioc a b
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Hom.range_comp_le_range : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} {P : Type u_2} [inst : L.Structure M] [inst_1 : L.Structure N]
  [inst_2 : L.Structure P] (f : L.Hom M N) (g : L.Hom N P), (g.comp f).range ≤ g.range