mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.SpecificGroups.Quaternion
_private.Mathlib.GroupTheory.SpecificGroups.Quaternion.0.instDecidableEqQuaternionGroup.decEq.match_1.splitter : {n : ℕ} →
  (motive : QuaternionGroup n → QuaternionGroup n → Sort u_1) →
    (x x_1 : QuaternionGroup n) →
      ((a b : ZMod (2 * n)) → motive (QuaternionGroup.a a) (QuaternionGroup.a b)) →
        ((a a_1 : ZMod (2 * n)) → motive (QuaternionGroup.a a) (QuaternionGroup.xa a_1)) →
          ((a a_1 : ZMod (2 * n)) → motive (QuaternionGroup.xa a) (QuaternionGroup.a a_1)) →
            ((a b : ZMod (2 * n)) → motive (QuaternionGroup.xa a) (QuaternionGroup.xa b)) → motive x x_1
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.mapRange_injective : ∀ {ι : Type u} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [inst : (i : ι) → Zero (β₁ i)] [inst_1 : (i : ι) → Zero (β₂ i)]
  (f : (i : ι) → β₁ i → β₂ i) (hf : ∀ (i : ι), f i 0 = 0),
  Function.Injective (DFinsupp.mapRange f hf) ↔ ∀ (i : ι), Function.Injective (f i)
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.coe_toRingHom : ∀ {R : Type u_4} {S : Type u_5} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (f : R ≃+* S), ⇑↑f = ⇑f
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.pow_subset_pow_mul_of_sq_subset_mul : ∀ {α : Type u_2} [inst : Monoid α] {s t : Set α} {n : ℕ}, s ^ 2 ⊆ t * s → n ≠ 0 → s ^ n ⊆ t ^ (n - 1) * s
-- Mathlib.GroupTheory.Solvable
derivedSeries_zero : ∀ (G : Type u_1) [inst : Group G], derivedSeries G 0 = ⊤
-- Mathlib.Analysis.PSeries
Real.summable_one_div_int_add_rpow : ∀ (a s : ℝ), (Summable fun n => 1 / |↑n + a| ^ s) ↔ 1 < s
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass
CategoryTheory.ShortComplex.ShortExact.extClass_comp_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) {Y : C} {n : ℕ}
  (γ : CategoryTheory.Abelian.Ext S.X₂ Y n) {n' : ℕ} {h : 1 + n = n'},
  hS.extClass.comp ((CategoryTheory.Abelian.Ext.mk₀ S.f).comp γ ⋯) h = 0
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.single.eq_1 : ∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k] (a : G) (b : k),
  SkewMonoidAlgebra.single a b = { coeff := fun₀ | a => b }
-- Mathlib.Order.CompletePartialOrder
/-- Create a `CompletePartialOrder` from a `PartialOrder` and `SupSet`
such that for every directed set `d`, `sSup d` is the least upper bound of `d`.

The bottom element is defined as `sSup ∅`.
 -/
CompletePartialOrder.ofLubOfDirected : (α : Type u_4) →
  [H1 : PartialOrder α] →
    [H2 : SupSet α] → (∀ (d : Set α), DirectedOn (fun x1 x2 => x1 ≤ x2) d → IsLUB d (sSup d)) → CompletePartialOrder α
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
BoxIntegral.IntegrationParams.toFilterDistortion_neBot : ∀ {ι : Type u_1} [inst : Fintype ι] (l : BoxIntegral.IntegrationParams) (I : BoxIntegral.Box ι),
  (l.toFilterDistortion I I.distortion).NeBot
-- Mathlib.Data.NNRat.Lemmas
Rat.toNNRat_div : ∀ {p q : ℚ}, 0 ≤ p → (p / q).toNNRat = p.toNNRat / q.toNNRat
-- Mathlib.Probability.Kernel.Composition.CompProd
/-- `Kernel.compProd` is associative. We have to insert `MeasurableEquiv.prodAssoc` in two places
because the products of types `α × β × γ` and `(α × β) × γ` are different.  -/
ProbabilityTheory.Kernel.compProd_assoc : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {δ : Type u_4} {mδ : MeasurableSpace δ} {κ : ProbabilityTheory.Kernel α β}
  {η : ProbabilityTheory.Kernel (α × β) γ} {ξ : ProbabilityTheory.Kernel (α × β × γ) δ},
  (κ.compProd (η.compProd (ξ.comap ⇑MeasurableEquiv.prodAssoc ⋯))).map ⇑MeasurableEquiv.prodAssoc.symm =
    (κ.compProd η).compProd ξ
-- Mathlib.RingTheory.Congruence.Hom
/-- A ring homomorphism `f` induces an injective homomorphism on the quotient by `f`'s kernel.  -/
RingCon.kerLiftₐ_injective : ∀ {M : Type u_1} {P : Type u_3} {R : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring M] [inst_2 : Algebra R M]
  [inst_3 : Semiring P] [inst_4 : Algebra R P] (f : M →ₐ[R] P), Function.Injective ⇑(RingCon.kerLiftₐ f)
-- Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
SimplexCategory.σ₀Iter_succ'_assoc : ∀ (i : ℕ) {n m : ℕ} (h : autoParam (n + i = m) SimplexCategory.σ₀Iter_succ'._auto_1) {Z : SimplexCategory}
  (h_1 : { len := n } ⟶ Z),
  CategoryTheory.CategoryStruct.comp (SimplexCategory.σ₀Iter (i + 1) ⋯) h_1 =
    CategoryTheory.CategoryStruct.comp (SimplexCategory.σ 0)
      (CategoryTheory.CategoryStruct.comp (SimplexCategory.σ₀Iter i h) h_1)
-- Mathlib.CategoryTheory.Limits.IndYoneda
CategoryTheory.Limits.coyonedaOpColimitIsoLimitCoyoneda'.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [inst_1 : CategoryTheory.Category.{v₂, v₁} I]
  (F : CategoryTheory.Functor Iᵒᵖ C) [inst_2 : CategoryTheory.Limits.HasColimit F],
  CategoryTheory.Limits.coyonedaOpColimitIsoLimitCoyoneda' F =
    CategoryTheory.coyoneda.mapIso (CategoryTheory.Limits.limitRightOpIsoOpColimit F).symm ≪≫
      CategoryTheory.preservesLimitIso CategoryTheory.coyoneda F.rightOp
-- Mathlib.Analysis.Calculus.FDeriv.Add
differentiableAt_comp_add_right : ∀ {𝕜 : 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}
  {x : E} (a : E), DifferentiableAt 𝕜 (fun x => f (x + a)) x ↔ DifferentiableAt 𝕜 f (x + a)
-- Mathlib.Analysis.Seminorm
Seminorm.preimage_metric_ball : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  (p : Seminorm 𝕜 E) {r : ℝ}, ⇑p ⁻¹' Metric.ball 0 r = {x | p x < r}
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.forM_eq_forIn : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] {n : Type w → Type w''}
  [inst_2 : Monad m] [inst_3 : Monad n] [LawfulMonad n] [inst_5 : Std.IteratorLoop α m n] [Std.LawfulIteratorLoop α m n]
  [inst_7 : MonadLiftT m n] {it : Std.IterM m β} {f : β → n PUnit.{w + 1}},
  forM it f =
    forIn it PUnit.unit fun out x => do
      f out
      pure (ForInStep.yield PUnit.unit)
-- Mathlib.Algebra.Module.Presentation.Tautological
_private.Mathlib.Algebra.Module.Presentation.Tautological.0.Module.Presentation.tautologicalRelations.match_1.eq_2 : ∀ (A : Type u_2) (M : Type u_1) (motive : Module.Presentation.tautological.R A M → Sort u_3) (a : A) (m : M)
  (h_1 : (m₁ m₂ : M) → motive (Module.Presentation.tautological.R.add m₁ m₂))
  (h_2 : (a : A) → (m : M) → motive (Module.Presentation.tautological.R.smul a m)),
  (match Module.Presentation.tautological.R.smul a m with
    | Module.Presentation.tautological.R.add m₁ m₂ => h_1 m₁ m₂
    | Module.Presentation.tautological.R.smul a m => h_2 a m) =
    h_2 a m
-- Lean.Meta.Tactic.Grind.Types
/-- Auxiliary field used to implement `grind.ematch.diagnostics`  -/
Lean.Meta.Grind.ENode.ematchDiagSource : Lean.Meta.Grind.ENode → Lean.Meta.Grind.EMatchDiagSource
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
/-- The functor `ι` is fully faithful.  -/
CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.fullyFaithulι : {C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {V : Type u₂} →
      {inst_1 : CategoryTheory.Category.{v₂, u₂} V} →
        {inst_2 : CategoryTheory.MonoidalCategory C} →
          {inst_3 : CategoryTheory.MonoidalCategory V} →
            {D : Type u₃} →
              {inst_4 : CategoryTheory.Category.{v₃, u₃} D} →
                [self : CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore C V D] →
                  (CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.ι C V
                      D).FullyFaithful
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.succ?_inj : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [Std.PRange.LinearlyUpwardEnumerable α] {a b : α},
  Std.PRange.succ? a = Std.PRange.succ? b ↔ a = b
-- Mathlib.GroupTheory.FixedPointFree
MonoidHom.FixedPointFree.commutatorMap_injective : ∀ {F : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : FunLike F G G] [MonoidHomClass F G G] {φ : F},
  MonoidHom.FixedPointFree ⇑φ → Function.Injective (MonoidHom.commutatorMap ⇑φ)
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.instCompleteLattice.eq_1 : ∀ {G : Type u_1} [inst : Group G],
  Subgroup.instCompleteLattice =
    { toSemilatticeSup := (completeLatticeOfInf (Subgroup G) ⋯).toSemilatticeSup, inf := fun x1 x2 => x1 ⊓ x2,
      inf_le_left := ⋯, inf_le_right := ⋯, le_inf := ⋯, toSupSet := (completeLatticeOfInf (Subgroup G) ⋯).toSupSet,
      isLUB_sSup := ⋯, toInfSet := (completeLatticeOfInf (Subgroup G) ⋯).toInfSet, isGLB_sInf := ⋯,
      toTop := Subgroup.instTop, le_top := ⋯, toBot := Subgroup.instBot, bot_le := ⋯ }
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.conjTranspose_zero : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : AddMonoid α] [inst_1 : StarAddMonoid α], Matrix.conjTranspose 0 = 0
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
Homeomorph.toOpenPartialHomeomorph_apply : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : X ≃ₜ Y),
  ↑e.toOpenPartialHomeomorph = ⇑e
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_empty : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} [Std.TransOrd α] [inst : Inhabited β] {a : α},
  Std.DTreeMap.Internal.Impl.Const.get! Std.DTreeMap.Internal.Impl.empty a = default
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.hasCokernels_of_hasCoequalizers : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasCoequalizers C], CategoryTheory.Limits.HasCokernels C
-- Mathlib.Topology.Category.LightProfinite.Basic
LightDiagram'.mk.inj : ∀ {diagram diagram_1 : CategoryTheory.Functor ℕᵒᵖ FintypeCat.Skeleton},
  { diagram := diagram } = { diagram := diagram_1 } → diagram = diagram_1
-- Mathlib.Order.Filter.Extr
IsMinOn.min : ∀ {α : Type u} {β : Type v} [inst : LinearOrder β] {f g : α → β} {a : α} {s : Set α},
  IsMinOn f s a → IsMinOn g s a → IsMinOn (fun x => min (f x) (g x)) s a
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.getEntryLE?_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  t₁.Equiv t₂ → t₁.getEntryLE? k = t₂.getEntryLE? k
-- Mathlib.FieldTheory.Finite.GaloisField
FiniteField.pow_finrank_eq_card : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] (k : Type u_3) [inst_1 : AddCommGroup k] [inst_2 : Fintype k]
  [inst_3 : Module (ZMod p) k], p ^ Module.finrank (ZMod p) k = Fintype.card k
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Real.deriv_rpow_const : ∀ (x p : ℝ), deriv (fun x => x ^ p) x = p * x ^ (p - 1)
-- Mathlib.Geometry.Euclidean.SignedDist
signedDist_le_dist : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (v : V) (p q : P), ((signedDist v) p) q ≤ dist p q
-- Lean.Meta.LazyDiscrTree
/-- Add partial match to cases if discriminator tree root map has potential matches.
 -/
Lean.Meta.LazyDiscrTree.pushRootCase : Std.HashMap Lean.Meta.LazyDiscrTree.Key Lean.Meta.LazyDiscrTree.TrieIndex →
  Lean.Meta.LazyDiscrTree.Key →
    Array Lean.Expr → Array Lean.Meta.LazyDiscrTree.PartialMatch → Array Lean.Meta.LazyDiscrTree.PartialMatch
-- Mathlib.RingTheory.Ideal.Cotangent
Ideal.cotangentIdeal_square : ∀ {R : Type u} [inst : CommRing R] (I : Ideal R), I.cotangentIdeal ^ 2 = ⊥
-- Init.Data.String.Lemmas.Splits
String.copy_sliceFrom_eq_iff_exists_splits : ∀ {s : String} {p : s.Pos} {t₂ : String}, (s.sliceFrom p).copy = t₂ ↔ ∃ t₁, p.Splits t₁ t₂
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prod.braiding_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P Q : C) [inst_1 : CategoryTheory.Limits.HasBinaryProduct P Q]
  [inst_2 : CategoryTheory.Limits.HasBinaryProduct Q P],
  (CategoryTheory.Limits.prod.braiding P Q).inv =
    CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst
-- Init.Data.Iterators.Lemmas.Combinators.FlatMap
Std.Iter.toArray_flatMap : ∀ {α α₂ β γ : Type w} [inst : Std.Iterator α Id β] [inst_1 : Std.Iterator α₂ Id γ] [Std.Iterators.Finite α Id]
  [Std.Iterators.Finite α₂ Id] [inst : Std.Iterator α Id β] [inst_2 : Std.Iterator α₂ Id γ] [Std.Iterators.Finite α Id]
  [Std.Iterators.Finite α₂ Id] {f : β → Std.Iter γ} {it₁ : Std.Iter β},
  (Std.Iter.flatMap f it₁).toArray = (Std.Iter.map (fun b => (f b).toArray) it₁).toArray.flatten
-- Mathlib.GroupTheory.Commutator.Basic
/-- **The Three Subgroups Lemma** (via the Hall-Witt identity)  -/
Subgroup.commutator_commutator_eq_bot_of_rotate : ∀ {G : Type u_1} [inst : Group G] {H₁ H₂ H₃ : Subgroup G}, ⁅⁅H₂, H₃⁆, H₁⁆ = ⊥ → ⁅⁅H₃, H₁⁆, H₂⁆ = ⊥ → ⁅⁅H₁, H₂⁆, H₃⁆ = ⊥
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Cylinder.IsGood.cofibration_i : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {A : C}
  {inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C} {P : HomotopicalAlgebra.Cylinder A}
  {inst_2 : CategoryTheory.Limits.HasBinaryCoproduct A A} {inst_3 : HomotopicalAlgebra.CategoryWithCofibrations C}
  [self : P.IsGood], HomotopicalAlgebra.Cofibration P.i
-- Mathlib.Computability.TuringMachine.Computable
Turing.TM2ComputableInPolyTime.mk.inj : ∀ {α β αΓ βΓ : Type} {ea : α → List αΓ} {eb : β → List βΓ} {f : α → β}
  {toTM2ComputableAux : Turing.TM2ComputableAux αΓ βΓ} {time : Polynomial ℕ}
  {outputsFun :
    (a : α) →
      Turing.TM2OutputsInTime toTM2ComputableAux.tm (List.map toTM2ComputableAux.inputAlphabet.invFun (ea a))
        (some (List.map toTM2ComputableAux.outputAlphabet.invFun (eb (f a)))) (Polynomial.eval (ea a).length time)}
  {toTM2ComputableAux_1 : Turing.TM2ComputableAux αΓ βΓ} {time_1 : Polynomial ℕ}
  {outputsFun_1 :
    (a : α) →
      Turing.TM2OutputsInTime toTM2ComputableAux_1.tm (List.map toTM2ComputableAux_1.inputAlphabet.invFun (ea a))
        (some (List.map toTM2ComputableAux_1.outputAlphabet.invFun (eb (f a)))) (Polynomial.eval (ea a).length time_1)},
  { toTM2ComputableAux := toTM2ComputableAux, time := time, outputsFun := outputsFun } =
      { toTM2ComputableAux := toTM2ComputableAux_1, time := time_1, outputsFun := outputsFun_1 } →
    toTM2ComputableAux = toTM2ComputableAux_1 ∧ time = time_1 ∧ outputsFun ≍ outputsFun_1
-- Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
/-- The bound on the power of the subgroup generated by the coefficients of the polynomials used to
describe the constructible set appearing in the case of `C : R → R[X]` of Chevalley's theorem with
complexity bound.  -/
_private.Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity.0.ChevalleyThm.PolynomialC.InductionObj.powBound : {R : Type u_2} → [inst : CommRing R] → {n : ℕ} → ChevalleyThm.PolynomialC.InductionObj✝ R n → ℕ
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.instCommRingFiniteElement : (K : Type u_1) →
  [inst : LinearOrder K] → [inst_1 : Field K] → [inst_2 : IsOrderedRing K] → CommRing (ArchimedeanClass.FiniteElement K)
-- ProofWidgets.Data.Html
ProofWidgets.Jsx.delabHtmlOfComponent : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.Algebra.Lie.Graded
/-- A class that ensures a Lie algebra has a bracket that preserves a decomposition.  -/
GradedLieAlgebra : {ι : Type u_1} →
  {R : Type u_3} →
    {L : Type u_4} →
      [DecidableEq ι] →
        [AddCommMonoid ι] →
          [inst : CommRing R] →
            [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → (ι → Submodule R L) → Type (max u_1 u_4)
-- Aesop.Frontend.Extension
Aesop.Frontend.declareRuleSetUnchecked : Aesop.RuleSetName → Bool → IO Unit
-- Mathlib.LinearAlgebra.Matrix.Permanent
Matrix.permanent_zero : ∀ {n : Type u_1} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type u_2} [inst_2 : CommSemiring R] [Nonempty n],
  Matrix.permanent 0 = 0
-- Mathlib.NumberTheory.Real.Irrational
Irrational.ratCast_sub : ∀ (q : ℚ) {x : ℝ}, Irrational x → Irrational (↑q - x)
-- Mathlib.Combinatorics.Schnirelmann
schnirelmannDensity_lt_iff : ∀ {A : Set ℕ} [inst : DecidablePred fun x => x ∈ A] {x : ℝ},
  schnirelmannDensity A < x ↔ ∃ n, 0 < n ∧ ↑{a ∈ Finset.Ioc 0 n | a ∈ A}.card / ↑n < x
-- Mathlib.Algebra.Order.Hom.Basic
GroupSeminormClass.toNonnegHomClass : ∀ {F : Type u_2} {α : Type u_3} {β : Type u_4} [inst : FunLike F α β] [inst_1 : Group α] [inst_2 : AddCommMonoid β]
  [inst_3 : LinearOrder β] [IsOrderedAddMonoid β] [GroupSeminormClass F α β], NonnegHomClass F α β
-- Mathlib.Combinatorics.Enumerative.Partition.Basic
Nat.Partition.ext_iff : ∀ {n : ℕ} {x y : n.Partition}, x = y ↔ x.parts = y.parts
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.adicCompletion.toCompletion_ofCompletion : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R)
  (x : (IsDedekindDomain.HeightOneSpectrum.valuation K v).Completion), { toCompletion := x }.toCompletion = x
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
DifferentiableWithinAt.csin : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {x : E} {s : Set E},
  DifferentiableWithinAt ℂ f s x → DifferentiableWithinAt ℂ (fun x => Complex.sin (f x)) s x
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.degreeOf.eq_1 : ∀ (x : Lean.Grind.CommRing.Var), Lean.Grind.CommRing.Mon.unit.degreeOf x = 0
-- Mathlib.Data.Nat.Cast.Defs
Nat.cast_add : ∀ {R : Type u_1} [inst : AddMonoidWithOne R] (m n : ℕ), ↑(m + n) = ↑m + ↑n
-- Lean.Meta.DiscrTree.Basic
_private.Lean.Meta.DiscrTree.Basic.0.Lean.Meta.DiscrTree.insertVal.loop : {α : Type u_1} → [BEq α] → Array α → α → ℕ → Array α
-- Mathlib.CategoryTheory.Sites.Grothendieck
/-- The trivial Grothendieck topology, in which only the maximal sieve is covering. This topology is
also known as the indiscrete, coarse, or chaotic topology.

See [MM92] Chapter III, Section 2, example (a), or
https://en.wikipedia.org/wiki/Grothendieck_topology#The_discrete_and_indiscrete_topologies
 -/
CategoryTheory.GrothendieckTopology.trivial : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.GrothendieckTopology C
-- Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange
CliffordAlgebra.toBaseChange_ofBaseChange : ∀ {R : Type u_1} (A : Type u_2) {V : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : AddCommGroup V]
  [inst_3 : Algebra R A] [inst_4 : Module R V] [inst_5 : Invertible 2] (Q : QuadraticForm R V)
  (x : TensorProduct R A (CliffordAlgebra Q)),
  (CliffordAlgebra.toBaseChange A Q) ((CliffordAlgebra.ofBaseChange A Q) x) = x
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddEquiv.coe_refl : ∀ (M : Type u_1) [inst : TopologicalSpace M] [inst_1 : Add M], ⇑(ContinuousAddEquiv.refl M) = id
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LitValue.nat.sizeOf_spec : ∀ (val : ℕ), sizeOf (Lean.Compiler.LCNF.LitValue.nat val) = 1 + sizeOf val
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.inverseImage_inverseImage : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {E : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} E] (P : CategoryTheory.MorphismProperty E)
  (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E),
  (P.inverseImage G).inverseImage F = P.inverseImage (F.comp G)
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.Approx.approx_eta : ∀ {F : PFunctor.{uA, uB}} {n : ℕ} (x : PFunctor.Approx.CofixA F (n + 1)),
  x = PFunctor.Approx.CofixA.intro (PFunctor.Approx.head' x) (PFunctor.Approx.children' x)
-- Mathlib.RingTheory.Extension.Presentation.Core
Algebra.Presentation.coeffs_relation_subset_core : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {P : Algebra.Presentation R S ι σ} (x : σ), ↑(MvPolynomial.coeffs (P.relation x)) ⊆ ↑P.core
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_le_of_le_log : ∀ {x y z : ℝ}, 0 < y → Real.log x ≤ z * Real.log y → x ≤ y ^ z
-- Mathlib.CategoryTheory.Discrete.Basic
CategoryTheory.Discrete.equivalence_counitIso : ∀ {I : Type u₁} {J : Type u₂} (e : I ≃ J),
  (CategoryTheory.Discrete.equivalence e).counitIso = CategoryTheory.Discrete.natIso fun j => CategoryTheory.eqToIso ⋯
-- Mathlib.LinearAlgebra.TensorProduct.Basic
TensorProduct.mapOfCompatibleSMul_tmul : ∀ (R : Type u_1) [inst : CommSemiring R] (A : Type u_22) (S : Type u_23) (M : Type u_24) (N : Type u_25)
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N]
  [inst_5 : CommSemiring A] [inst_6 : Module A M] [inst_7 : Module A N] [inst_8 : SMulCommClass R A M]
  [inst_9 : CommSemiring S] [inst_10 : Module S M] [inst_11 : SMulCommClass R S M] [inst_12 : SMulCommClass A S M]
  [inst_13 : TensorProduct.CompatibleSMul R A M N] (m : M) (n : N),
  (TensorProduct.mapOfCompatibleSMul R A S M N) (m ⊗ₜ[A] n) = m ⊗ₜ[R] n
-- Mathlib.Algebra.Ring.Subring.MulOpposite
Subring.mem_unop : ∀ {R : Type u_2} [inst : NonAssocRing R] {x : R} {S : Subring Rᵐᵒᵖ}, x ∈ S.unop ↔ MulOpposite.op x ∈ S
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.toFinsupp_nsmul : ∀ {R : Type u} [inst : Semiring R] (a : ℕ) (b : Polynomial R), (a • b).toFinsupp = a • b.toFinsupp
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.imageAddMonoidHom.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] [inst_1 : DecidableEq β] [inst_2 : AddZeroClass α]
  [inst_3 : AddZeroClass β] [inst_4 : FunLike F α β] [inst_5 : AddMonoidHomClass F α β] (f : F),
  Finset.imageAddMonoidHom f = { toFun := (Finset.imageAddHom f).toFun, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Limits.snd_of_isColimit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C}
  {t : CategoryTheory.Limits.BinaryBicone X Y} (ht : CategoryTheory.Limits.IsColimit t.toCocone),
  t.snd = CategoryTheory.Limits.BinaryCofan.IsColimit.desc ht 0 (CategoryTheory.CategoryStruct.id Y)
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
/-- Auxiliary definition for `vComp`.  -/
CategoryTheory.Oplax.LaxTrans.vCompNaturality : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G H : CategoryTheory.OplaxFunctor B C} →
          (η : CategoryTheory.Oplax.LaxTrans F G) →
            (θ : CategoryTheory.Oplax.LaxTrans G H) →
              {a b : B} →
                (f : a ⟶ b) →
                  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (η.app a) (θ.app a))
                      (H.map f) ⟶
                    CategoryTheory.CategoryStruct.comp (F.map f)
                      (CategoryTheory.CategoryStruct.comp (η.app b) (θ.app b))
-- Init.Data.Int.Basic
Int.default_eq_zero : default = 0
-- Mathlib.Algebra.Homology.Embedding.Basic
ComplexShape.instIsTruncGEEmbeddingUp'Add : ∀ {A : Type u_3} [inst : AddCommSemigroup A] [inst_1 : IsRightCancelAdd A] (a b : A),
  (ComplexShape.embeddingUp'Add a b).IsTruncGE
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.coeffEquiv_symm_apply : ∀ (R : Type u_2) {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (coeff : ℕ →₀ M),
  (PolynomialModule.coeffEquiv R).symm coeff = { coeff := coeff }
-- Mathlib.Order.Interval.Finset.Floor
Int.cast_mem_Ici_iff : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] {a : α} {n : ℤ},
  ↑n ∈ Set.Ici a ↔ n ∈ Set.Ici ⌈a⌉