mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Polynomial.Eval.Degree
/-- A reformulation of the expansion of (1 + y)^d:
$$(d + 1) (1 + y)^d - (d + 1)y^d = \sum_{i = 0}^d {d + 1 \choose i} \cdot i \cdot y^{i - 1}.$$
 -/
Polynomial.eval_monomial_one_add_sub : ∀ {S : Type v} [inst : CommRing S] (d : ℕ) (y : S),
  Polynomial.eval (1 + y) ((Polynomial.monomial d) (↑d + 1)) - Polynomial.eval y ((Polynomial.monomial d) (↑d + 1)) =
    ∑ x_1 ∈ Finset.range (d + 1), ↑((d + 1).choose x_1) * (↑x_1 * y ^ (x_1 - 1))
-- Mathlib.Data.Finsupp.MonomialOrder
/-- The synonym type  -/
MonomialOrder.syn : {σ : Type u_1} → MonomialOrder σ → Type u_2
-- Init.Grind.Ordered.Order
Lean.Grind.LinearOrder.trichotomy : ∀ {α : Type u} [inst : LE α] [inst_1 : LT α] [Std.LawfulOrderLT α] [Std.IsLinearOrder α] (a b : α),
  a < b ∨ a = b ∨ b < a
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapLeftIso_unitIso_inv_app_right : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (R : CategoryTheory.Functor B T)
  {L₁ L₂ : CategoryTheory.Functor A T} (i : L₁ ≅ L₂) (X : CategoryTheory.Comma L₁ R),
  ((CategoryTheory.Comma.mapLeftIso R i).unitIso.inv.app X).right = CategoryTheory.CategoryStruct.id X.right
-- Mathlib.Topology.Constructions
Topology.isOpenEmbedding_sigmaMap : ∀ {ι : Type u_5} {κ : Type u_6} {σ : ι → Type u_7} {τ : κ → Type u_8} [inst : (i : ι) → TopologicalSpace (σ i)]
  [inst_1 : (k : κ) → TopologicalSpace (τ k)] {f₁ : ι → κ} {f₂ : (i : ι) → σ i → τ (f₁ i)},
  Function.Injective f₁ → (Topology.IsOpenEmbedding (Sigma.map f₁ f₂) ↔ ∀ (i : ι), Topology.IsOpenEmbedding (f₂ i))
-- Mathlib.Algebra.Category.AlgCat.Basic
/-- The category of R-algebras and their morphisms.  -/
AlgCat : (R : Type u) → [CommRing R] → Type (max u (v + 1))
-- Lean.Meta.Tactic.Grind.Theorems
Lean.Meta.Grind.instBEqOrigin : BEq Lean.Meta.Grind.Origin
-- Mathlib.Combinatorics.Graph.Simple
Graph.IsLink.ne : ∀ {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {e : β} [G.Loopless], G.IsLink e u v → u ≠ v
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
ENNReal.log_le_log : ∀ {x y : ENNReal}, x ≤ y → x.log ≤ y.log
-- Mathlib.Topology.ContinuousMap.Basic
ContinuousMap.comp_const : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] (f : C(β, γ)) (b : β), f.comp (ContinuousMap.const α b) = ContinuousMap.const α (f b)
-- Mathlib.Combinatorics.SimpleGraph.DeleteEdges
SimpleGraph.deleteEdges_univ : ∀ {V : Type u_1} {G : SimpleGraph V}, G.deleteEdges Set.univ = ⊥
-- Init.Data.UInt.Lemmas
USize.neg_ne_zero : ∀ {a : USize}, -a ≠ 0 ↔ a ≠ 0
-- Mathlib.RingTheory.Ideal.Maximal
Ideal.span_singleton_prime : ∀ {α : Type u} [inst : CommSemiring α] {p : α}, p ≠ 0 → ((Ideal.span {p}).IsPrime ↔ Prime p)
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.MeasurePreserving.smulInvariantMeasure_iterateMulAct : ∀ {α : Type w} {f : α → α} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α},
  MeasureTheory.MeasurePreserving f μ μ → MeasureTheory.SMulInvariantMeasure (IterateMulAct f) α μ
-- Mathlib.Probability.Martingale.Basic
MeasureTheory.Supermartingale.setIntegral_le : ∀ {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : Preorder ι] {m0 : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure Ω} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
  {ℱ : MeasureTheory.Filtration ι m0} [CompleteSpace E] [inst_4 : PartialOrder E] [IsOrderedAddMonoid E]
  [IsOrderedModule ℝ E] [ClosedIciTopology E] [MeasureTheory.SigmaFiniteFiltration μ ℱ] {f : ι → Ω → E},
  MeasureTheory.Supermartingale f ℱ μ →
    ∀ {i j : ι}, i ≤ j → ∀ {s : Set Ω}, MeasurableSet s → ∫ (ω : Ω) in s, f j ω ∂μ ≤ ∫ (ω : Ω) in s, f i ω ∂μ
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
/-- a lifting to the pullback  -/
CategoryTheory.Limits.ChosenPullback.LiftStruct.f : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X₁ X₂ S : C} →
      {f₁ : X₁ ⟶ S} →
        {f₂ : X₂ ⟶ S} →
          {h : CategoryTheory.Limits.ChosenPullback f₁ f₂} →
            {Y : C} → {g₁ : Y ⟶ X₁} → {g₂ : Y ⟶ X₂} → {b : Y ⟶ S} → h.LiftStruct g₁ g₂ b → (Y ⟶ h.pullback)
-- Mathlib.RingTheory.Ideal.Operations
Ideal.span_singleton_mul_left_mono : ∀ {R : Type u} [inst : Semiring R] {I J : Ideal R} [IsDomain R] [I.IsTwoSided] [J.IsTwoSided] {x : R},
  x ≠ 0 → (I * Ideal.span {x} ≤ J * Ideal.span {x} ↔ I ≤ J)
-- Mathlib.Tactic.FunProp.Core
/-- Prove function property of `fun x ↦ f x₁ ... xₙ` where `f` is free variable.  -/
Mathlib.Meta.FunProp.fvarAppCase : Mathlib.Meta.FunProp.FunPropDecl →
  Lean.Expr →
    Mathlib.Meta.FunProp.FunctionData →
      (Lean.Expr → Mathlib.Meta.FunProp.FunPropM (Option Mathlib.Meta.FunProp.Result)) →
        Mathlib.Meta.FunProp.FunPropM (Option Mathlib.Meta.FunProp.Result)
-- Init.Internal.Order.Lemmas
Lean.Order.Array.monotone_foldlM : ∀ {m : Type u → Type v} [inst : Monad m] [inst_1 : (α : Type u) → Lean.Order.PartialOrder (m α)] [Lean.Order.MonoBind m]
  {α β : Type u} {γ : Type w} [inst_3 : Lean.Order.PartialOrder γ] (f : γ → β → α → m β) (init : β) (xs : Array α)
  (start stop : ℕ), Lean.Order.monotone f → Lean.Order.monotone fun x => Array.foldlM (f x) init xs start stop
-- Init.Data.Int.Linear
Int.Internal.Linear.var_eq : ∀ (ctx : Int.Internal.Linear.Context) (x : Int.Internal.Linear.Var) (k : ℤ) (p : Int.Internal.Linear.Poly),
  Int.Internal.Linear.var_eq_cert x k p = true →
    Int.Internal.Linear.Poly.denote' ctx p = 0 → Int.Internal.Linear.Var.denote ctx x = k
-- Mathlib.AlgebraicGeometry.Cover.Sigma
AlgebraicGeometry.Scheme.Cover.Hom.sigma_h₀ : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {S : AlgebraicGeometry.Scheme}
  [inst : AlgebraicGeometry.IsZariskiLocalAtSource P] [inst_1 : UnivLE.{v, u}]
  {𝒰 𝒱 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) S} (f : 𝒰 ⟶ 𝒱) (x : 𝒰.sigma.I₀),
  (AlgebraicGeometry.Scheme.Cover.Hom.sigma f).h₀ x =
    CategoryTheory.Limits.Sigma.desc fun j =>
      CategoryTheory.CategoryStruct.comp (f.h₀ j) (CategoryTheory.Limits.Sigma.ι 𝒱.X (f.s₀ j))
-- Mathlib.Topology.Algebra.InfiniteSum.Group
cauchySeq_finset_iff_prod_vanishing : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : CommGroup α] [IsUniformGroup α] {f : β → α},
  (CauchySeq fun s => ∏ b ∈ s, f b) ↔ ∀ e ∈ nhds 1, ∃ s, ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
-- Mathlib.Order.CountableSupClosed
CountableInfClosed.finsetInf'_mem : ∀ {α : Type u_2} {s : Set α} {ι : Type u_4} {f : ι → α} {t : Finset ι} [inst : SemilatticeInf α],
  CountableInfClosed s → ∀ (ht : t.Nonempty), (∀ i ∈ t, f i ∈ s) → t.inf' ht f ∈ s
-- Mathlib.Algebra.Lie.Ideal
LieIdeal.comap_mono : ∀ {R : Type u} {L : Type v} {L' : Type w₂} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieRing L']
  [inst_3 : LieAlgebra R L'] [inst_4 : LieAlgebra R L] {f : L →ₗ⁅R⁆ L'}, Monotone (LieIdeal.comap f)
-- Mathlib.Topology.MetricSpace.Lipschitz
LocallyLipschitz.min_const : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {f : α → ℝ},
  LocallyLipschitz f → ∀ (a : ℝ), LocallyLipschitz fun x => min (f x) a
-- Mathlib.Analysis.Normed.Module.Normalize
NormedSpace.normalize_smul_of_neg : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] {r : ℝ},
  r < 0 → ∀ (x : V), NormedSpace.normalize (r • x) = -NormedSpace.normalize x
-- Mathlib.Algebra.Group.Equiv.TypeTags
ZeroHom.mk.congr_simp : ∀ {M : Type u_10} {N : Type u_11} [inst : Zero M] [inst_1 : Zero N] (toFun toFun_1 : M → N) (e_toFun : toFun = toFun_1)
  (map_zero' : toFun 0 = 0), { toFun := toFun, map_zero' := map_zero' } = { toFun := toFun_1, map_zero' := ⋯ }
-- Mathlib.RingTheory.Localization.Finiteness
/-- Let `S` be an `R`-algebra, `M` a submonoid of `R`, and `S' = M⁻¹S`.
If the image of some `x : S` falls in the span of some finite `s ⊆ S'` over `R`,
then there exists some `m : M` such that `m • x` falls in the
span of `IsLocalization.finsetIntegerMultiple _ s` over `R`.
 -/
IsLocalization.smul_mem_finsetIntegerMultiple_span : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] (M : Submonoid R) (S' : Type u_4)
  [inst_2 : CommSemiring S'] [inst_3 : Algebra S S'] [inst_4 : Algebra R S] [inst_5 : Algebra R S']
  [IsScalarTower R S S'] [inst_7 : IsLocalization (Submonoid.map (algebraMap R S) M) S'] (x : S) (s : Finset S'),
  (algebraMap S S') x ∈ Submodule.span R ↑s →
    ∃ m, m • x ∈ Submodule.span R ↑(IsLocalization.finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)
-- Mathlib.Logic.Equiv.Basic
Equiv.swap_apply_of_ne_of_ne : ∀ {α : Sort u_1} [inst : DecidableEq α] {a b x : α}, x ≠ a → x ≠ b → (Equiv.swap a b) x = x
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.Code.instantiateValueLevelParams.instFunDecl : List Lean.Name →
  List Lean.Level →
    Lean.Compiler.LCNF.FunDecl Lean.Compiler.LCNF.Purity.pure →
      Lean.Compiler.LCNF.FunDecl Lean.Compiler.LCNF.Purity.pure
-- Mathlib.CategoryTheory.Bicategory.Extension
/-- The isomorphism between left extensions induced by a right unitor.  -/
CategoryTheory.Bicategory.LeftExtension.whiskerOfCompIdIsoSelf : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f : a ⟶ b} →
        {g : a ⟶ c} →
          (t : CategoryTheory.Bicategory.LeftExtension f g) →
            (t.whisker (CategoryTheory.CategoryStruct.id c)).ofCompId ≅ t
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.induction_on : ∀ {α : Type u} {C : FreeAddGroup α → Prop} (z : FreeAddGroup α),
  C 0 →
    (∀ (x : α), C (FreeAddGroup.of x)) →
      (∀ (x : α), C (FreeAddGroup.of x) → C (-FreeAddGroup.of x)) →
        (∀ (x y : FreeAddGroup α), C x → C y → C (x + y)) → C z
-- Mathlib.Geometry.Manifold.StructureGroupoid
/-- Structure groupoids are stable under inverse.  -/
StructureGroupoid.symm' : ∀ {H : Type u_2} [inst : TopologicalSpace H] (self : StructureGroupoid H), ∀ e ∈ self.members, e.symm ∈ self.members
-- Mathlib.Algebra.Module.Injective
/-- An `R`-module `Q` satisfies Baer's criterion if any `R`-linear map from an `Ideal R` extends to
an `R`-linear map `R ⟶ Q`  -/
Module.Baer : (R : Type u) → [inst : Ring R] → (Q : Type v) → [inst_1 : AddCommGroup Q] → [Module R Q] → Prop
-- Mathlib.Analysis.Normed.Module.RCLike.Extend
/-- The extension `StrongDual.extendRCLike` as a continuous linear equivalence between
the strong duals when scalar multiplication (by `𝕜`) is jointly continuous.  -/
StrongDual.extendRCLikeL : {𝕜 : Type u_4} →
  {F : Type u_5} →
    [inst : RCLike 𝕜] →
      [inst_1 : TopologicalSpace F] →
        [inst_2 : AddCommGroup F] →
          [inst_3 : Module 𝕜 F] →
            [ContinuousSMul 𝕜 F] → [inst_5 : Module ℝ F] → [IsScalarTower ℝ 𝕜 F] → StrongDual ℝ F ≃L[ℝ] StrongDual 𝕜 F
-- Init.Data.BitVec.Basic
/-- Returns `zeroExtend (w+n) x <<< n` without needing to compute `x % 2^(2+n)`.
 -/
BitVec.shiftLeftZeroExtend : {w : ℕ} → BitVec w → (m : ℕ) → BitVec (w + m)
-- Init.Data.UInt.Lemmas
UInt8.toUInt64_toUInt32 : ∀ (n : UInt8), n.toUInt32.toUInt64 = n.toUInt64
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.Compacts.t2Space_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α], T2Space (TopologicalSpace.Compacts α) ↔ T2Space α
-- Mathlib.Algebra.Lie.Weights.Chain
/-- Given a (potential) root `α` relative to a Cartan subalgebra `H`, if we restrict to the ideal
`I = corootSpace α` of `H` (informally, `I = ⁅H(α), H(-α)⁆`), we may find an
integral linear combination between `α` and any weight `χ` of a representation.

This is Proposition 4.4 from [carter2005] and is a key step in the proof that the roots of a
semisimple Lie algebra form a root system. It shows that the restriction of `α` to `I` vanishes iff
the restriction of every root to `I` vanishes (which cannot happen in a semisimple Lie algebra).  -/
LieModule.exists_forall_mem_corootSpace_smul_add_eq_zero : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (M : Type u_3)
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  {H : LieSubalgebra R L} (α χ : ↥H → R) [inst_7 : H.IsCartanSubalgebra] [inst_8 : IsNoetherian R L] [IsDomain R]
  [IsPrincipalIdealRing R] [CharZero R] [Module.IsTorsionFree R M] [IsNoetherian R M],
  α ≠ 0 → LieModule.genWeightSpace M χ ≠ ⊥ → ∃ a b, 0 < b ∧ ∀ x ∈ LieAlgebra.corootSpace α, (a • α + b • χ) x = 0
-- Mathlib.Algebra.Polynomial.Expand
Polynomial.expand_eq_comp_X_pow : ∀ {R : Type u} [inst : CommSemiring R] (p : ℕ) {f : Polynomial R}, (Polynomial.expand R p) f = f.comp (Polynomial.X ^ p)
-- Mathlib.CategoryTheory.Triangulated.Basic
/-- the third object of a triangle  -/
CategoryTheory.Pretriangulated.Triangle.obj₃ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] → CategoryTheory.Pretriangulated.Triangle C → C
-- Mathlib.NumberTheory.LSeries.Dirichlet
/-- The L-series of the constant sequence `1` equals the Riemann zeta function on its
domain of convergence `1 < re s`.  -/
LSeriesHasSum_one : ∀ {s : ℂ}, 1 < s.re → LSeriesHasSum 1 s (riemannZeta s)
-- Mathlib.Topology.ContinuousOn
Filter.EventuallyEq.congr_continuousWithinAt : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f g : α → β} {s : Set α}
  {x : α}, f =ᶠ[nhdsWithin x s] g → f x = g x → (ContinuousWithinAt f s x ↔ ContinuousWithinAt g s x)
-- Mathlib.Algebra.RingQuot
RingQuot.instCommRing : {R : Type uR} → [inst : CommRing R] → (r : R → R → Prop) → CommRing (RingQuot r)
-- Mathlib.Algebra.GCDMonoid.Basic
lcm_comm' : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] (a b : α), Associated (lcm a b) (lcm b a)
-- Init.Data.Array.Attach
Array.unattach_append : ∀ {α : Type u_1} {p : α → Prop} {xs₁ xs₂ : Array { x // p x }}, (xs₁ ++ xs₂).unattach = xs₁.unattach ++ xs₂.unattach
-- Std.Data.HashSet.Lemmas
Std.HashSet.fold_eq_foldl_toList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} {δ : Type v} {f : δ → α → δ} {init : δ},
  Std.HashSet.fold f init m = List.foldl f init m.toList
-- Mathlib.MeasureTheory.Measure.Haar.OfBasis
/-- The closed parallelepiped spanned by a finite family of vectors.  -/
parallelepiped : {ι : Type u_1} → {E : Type u_3} → [Fintype ι] → [inst : AddCommGroup E] → [Module ℝ E] → (ι → E) → Set E
-- Mathlib.NumberTheory.ModularForms.Cusps
IsCusp.mono : ∀ {𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)} {c : OnePoint ℝ}, 𝒢 ≤ ℋ → IsCusp c 𝒢 → IsCusp c ℋ
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.constantCoeff_subst_eq_zero : ∀ {R : Type u_2} [inst : CommRing R] {τ : Type u_3} {S : Type u_4} [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {a : MvPowerSeries τ S},
  MvPowerSeries.constantCoeff a = 0 →
    ∀ (f : PowerSeries R), PowerSeries.constantCoeff f = 0 → MvPowerSeries.constantCoeff (PowerSeries.subst a f) = 0
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.ToIntInfo.upperThm? : Lean.Meta.Grind.Arith.Cutsat.ToIntInfo → Option Lean.Expr
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
spectralValueTerms_of_natDegree_le : ∀ {R : Type u_1} [inst : SeminormedRing R] (p : Polynomial R) {n : ℕ}, p.natDegree ≤ n → spectralValueTerms p n = 0
-- Aesop.Tree.Data
Aesop.Goal.children : Aesop.Goal → Array Aesop.RappRef
-- Lean.Meta.InferType
Lean.Meta.inferTypeImp : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.Category.MonCat.Limits
AddCommMonCat.forget_createsLimit.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommMonCat)
  [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddCommMonCat)).sections],
  AddCommMonCat.forget_createsLimit F =
    CategoryTheory.createsLimitOfNatIso
      (CategoryTheory.NatIso.ofComponents
          (fun x => CategoryTheory.Iso.refl ((CategoryTheory.forget AddCommMonCat).obj x))
          @AddCommMonCat.forget_createsLimit._proof_1).symm
-- Init.Data.Bool
Bool.bne_false : ∀ (b : Bool), (b != false) = b
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
CategoryTheory.Functor.CoconeTypes.IsColimitCore.mk.injEq : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {F : CategoryTheory.Functor J (Type w₀)} {c : F.CoconeTypes}
  (desc : (c' : F.CoconeTypes) → c.pt → c'.pt)
  (fac :
    autoParam (∀ (c' : F.CoconeTypes) (j : J), desc c' ∘ c.ι j = c'.ι j)
      CategoryTheory.Functor.CoconeTypes.IsColimitCore.fac._autoParam)
  (funext : ∀ {T : Type w₂} {f g : c.pt → T}, (∀ (j : J), f ∘ c.ι j = g ∘ c.ι j) → f = g)
  (desc_1 : (c' : F.CoconeTypes) → c.pt → c'.pt)
  (fac_1 :
    autoParam (∀ (c' : F.CoconeTypes) (j : J), desc_1 c' ∘ c.ι j = c'.ι j)
      CategoryTheory.Functor.CoconeTypes.IsColimitCore.fac._autoParam)
  (funext_1 : ∀ {T : Type w₂} {f g : c.pt → T}, (∀ (j : J), f ∘ c.ι j = g ∘ c.ι j) → f = g),
  ({ desc := desc, fac := fac, funext := funext } = { desc := desc_1, fac := fac_1, funext := funext_1 }) =
    (desc = desc_1)
-- Mathlib.Control.Monad.Writer
WriterT.instLawfulMonad : ∀ {M : Type u → Type v} {ω : Type u} [inst : Monad M] [inst_1 : Monoid ω] [LawfulMonad M], LawfulMonad (WriterT ω M)
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.buildPath : (Bool → Array Lean.Expr → Lean.Expr → Lean.MetaM (Lean.Meta.LazyDiscrTree.Key × Array Lean.Expr)) →
  Bool → Array Lean.Expr → Array Lean.Meta.LazyDiscrTree.Key → Lean.MetaM (Array Lean.Meta.LazyDiscrTree.Key)
-- Lean.Meta.Basic
Lean.Meta.withLocalDeclD : {n : Type → Type u_1} →
  [MonadControlT Lean.MetaM n] → [Monad n] → {α : Type} → Lean.Name → Lean.Expr → (Lean.Expr → n α) → n α
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Complex.sin_eq_one_iff : ∀ {x : ℂ}, Complex.sin x = 1 ↔ ∃ k, ↑Real.pi / 2 + ↑k * (2 * ↑Real.pi) = x
-- Mathlib.Analysis.Normed.Group.Defs
/-- A normed group is a group endowed with a norm for which `dist x y = ‖x⁻¹ * y‖` defines a metric
space structure.  -/
NormedGroup : Type u_8 → Type u_8
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
/-- Adding a top element to a conditionally complete lattice
gives a conditionally complete lattice  -/
WithTop.conditionallyCompleteLattice : {α : Type u_5} → [ConditionallyCompleteLattice α] → ConditionallyCompleteLattice (WithTop α)
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.monic_normalize : ∀ {R : Type u} [inst : Field R] {p : Polynomial R} [inst_1 : DecidableEq R], p ≠ 0 → (normalize p).Monic
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.fold_eq_foldl_toArray : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) {δ : Type w} {f : δ → (a : α) → β a → δ}
  {init : δ}, Std.DHashMap.Raw.fold f init ↑m = Array.foldl (fun a b => f a b.fst b.snd) init (↑m).toArray
-- Lean.Util.Diff
Lean.Diff.Action.delete.sizeOf_spec : sizeOf Lean.Diff.Action.delete = 1
-- Mathlib.Order.Filter.Prod
Filter.mem_prod_iff_right : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} {s : Set (α × β)},
  s ∈ f ×ˢ g ↔ ∃ t ∈ g, ∀ᶠ (x : α) in f, ∀ y ∈ t, (x, y) ∈ s
-- Mathlib.RepresentationTheory.Subrepresentation
Subrepresentation.instSetLike : {A : Type u_1} →
  {G : Type u_2} →
    {W : Type u_3} →
      [inst : Semiring A] →
        [inst_1 : Monoid G] →
          [inst_2 : AddCommMonoid W] →
            [inst_3 : Module A W] → {ρ : Representation A G W} → SetLike (Subrepresentation ρ) W
-- Mathlib.Algebra.MonoidAlgebra.Cardinal
AddMonoidAlgebra.cardinalMk_eq_max_lift_of_infinite' : ∀ (R : Type u) (M' : Type v) [inst : Semiring R] [Nonempty M'] [Infinite R],
  Cardinal.mk (AddMonoidAlgebra R M') =
    max (Cardinal.lift.{v, u} (Cardinal.mk R)) (Cardinal.lift.{u, v} (Cardinal.mk M'))
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyMapData.rightHomologyMap'_eq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData}
  (γ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂),
  CategoryTheory.ShortComplex.rightHomologyMap' φ h₁ h₂ = γ.φH
-- Mathlib.Order.Interval.Multiset
Multiset.Ioc_self : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] (a : α), Multiset.Ioc a a = 0
-- Std.Time.Internal.UnitVal
/-- Divides the `UnitVal` by an `Int`, resulting in a new `UnitVal` with an adjusted ratio. Using the
E-rounding convention (euclidean division)
 -/
Std.Time.Internal.UnitVal.ediv : {a : ℚ} → Std.Time.Internal.UnitVal a → (divisor : ℤ) → Std.Time.Internal.UnitVal (a * ↑divisor)
-- Mathlib.Combinatorics.SimpleGraph.UnitDistance.Basic
/-- Transfer a unit-distance embedding across a graph isomorphism.  -/
SimpleGraph.UnitDistEmbedding.iso : {V : Type u_1} →
  {W : Type u_2} →
    {G : SimpleGraph V} →
      {H : SimpleGraph W} →
        {E : Type u_3} → [inst : MetricSpace E] → G.UnitDistEmbedding E → G ≃g H → H.UnitDistEmbedding E
-- Mathlib.Data.Nat.DvdSequence
IsDvdSequence.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : Dvd α] [inst_1 : Dvd β] (f : α → β),
  IsDvdSequence f = ∀ (a b : α), a ∣ b → f a ∣ f b
-- Init.Data.Ord.Basic
List.compare_cons_cons : ∀ {α : Type u_1} [inst : Ord α] {x y : α} {xs ys : List α},
  compare (x :: xs) (y :: ys) = (compare x y).then (compare xs ys)
-- Mathlib.Topology.Metrizable.CompletelyMetrizable
TopologicalSpace.UpgradedIsCompletelyPseudoMetrizableSpace.toPseudoMetricSpace : {X : Type u_3} → [self : TopologicalSpace.UpgradedIsCompletelyPseudoMetrizableSpace X] → PseudoMetricSpace X
-- Mathlib.Algebra.Star.Basic
/-- `star` commutes with addition  -/
StarAddMonoid.star_add : ∀ {R : Type u} {inst : AddMonoid R} [self : StarAddMonoid R] (r s : R), star (r + s) = star r + star s
-- Mathlib.Algebra.Group.Units.Equiv
isLocalHom_equiv : ∀ {F : Type u_1} {M : Type u_3} {N : Type u_4} [inst : Monoid M] [inst_1 : Monoid N] [inst_2 : EquivLike F M N]
  [MulEquivClass F M N] (f : F), IsLocalHom f
-- Mathlib.Analysis.Complex.Circle
Circle.instSMulCommClass_left : ∀ {α : Type u_1} {β : Type u_2} [inst : SMul ℂ β] [inst_1 : SMul α β] [SMulCommClass ℂ α β], SMulCommClass Circle α β
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.distinct_keys_toList : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) t.toList
-- Lean.Elab.DeclNameGen
_private.Lean.Elab.DeclNameGen.0.Lean.Elab.Command.NameGen.winnowExpr.visit : Lean.Expr → Lean.MonadCacheT Lean.Expr Lean.Expr Lean.MetaM Lean.Expr
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.union_zeroLocus : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (s s' : Set A),
  ProjectiveSpectrum.zeroLocus 𝒜 s ∪ ProjectiveSpectrum.zeroLocus 𝒜 s' =
    ProjectiveSpectrum.zeroLocus 𝒜 ↑(Ideal.span s ⊓ Ideal.span s')
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.AddMod.id.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  {A : C} [inst_4 : CategoryTheory.AddMonObj A] (M : CategoryTheory.AddMod D A),
  M.id = { hom := CategoryTheory.CategoryStruct.id M.X, isAddModHom := ⋯ }
-- Mathlib.SetTheory.ZFC.PSet
/-- `x ∈ y` as pre-sets if `x` is extensionally equivalent to a member of the family `y`.  -/
PSet.Mem : PSet.{u} → PSet.{u} → Prop
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.RightFraction.cases : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  (α : W.RightFraction X Y), ∃ X' s, ∃ (hs : W s), ∃ f, α = { X' := X', s := s, hs := hs, f := f }
-- Mathlib.Algebra.Ring.Pointwise.Set
Set.mul_add_subset : ∀ {α : Type u_1} [inst : Distrib α] (s t u : Set α), s * (t + u) ⊆ s * t + s * u