mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Hom.Instances
/-- See also `AddMonoid.End.intCast_def`.  -/
AddMonoid.End.intCast_apply : ∀ {M : Type uM} [inst : AddCommGroup M] (z : ℤ) (m : M), ↑z m = z • m
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.Copy.ofLE_comp : ∀ {V : Type u_1} {G₁ G₂ G₃ : SimpleGraph V} (h₁₂ : G₁ ≤ G₂) (h₂₃ : G₂ ≤ G₃),
  (SimpleGraph.Copy.ofLE G₂ G₃ h₂₃).comp (SimpleGraph.Copy.ofLE G₁ G₂ h₁₂) = SimpleGraph.Copy.ofLE G₁ G₃ ⋯
-- Std.Http.Protocol.H1
/-- Utility result for body parser branches that could not make progress this step.
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.bodyNoProgress : {dir : Std.Http.Protocol.H1.Direction} →
  Std.Http.Protocol.H1.Machine dir → Std.Http.Protocol.H1.Machine dir × Option Std.Http.Protocol.H1.PulledChunk × Bool
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.toArray_mapM : ∀ {α β γ : Type w} [inst : Std.Iterator α Id β] {it : Std.Iter β} {m : Type w → Type w'} [inst_1 : Monad m]
  [inst_2 : MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] [Std.Iterators.Finite α Id] {f : β → m γ},
  (Std.Iter.mapM f it).toArray = Array.mapM f it.toArray
-- Mathlib.Order.Interval.Basic
NonemptyInterval.instMembership : {α : Type u_1} → [inst : Preorder α] → Membership α (NonemptyInterval α)
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.closure_empty : ∀ {R : Type u} [inst : NonAssocSemiring R], Subsemiring.closure ∅ = ⊥
-- Mathlib.Order.Heyting.Basic
sup_sdiff_cancel_right : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, a ≤ b → a ⊔ b \ a = b
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.category_id_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (B : CategoryTheory.Limits.Cocone F),
  (CategoryTheory.CategoryStruct.id B).hom = CategoryTheory.CategoryStruct.id B.pt
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.isSome_minKey?_modify : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] {k : α}
  {f : β → β}, t.WF → (Std.DTreeMap.Internal.Impl.Const.modify k f t).minKey?.isSome = !t.isEmpty
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.toNonUnitalStarSubalgebra_toStarSubalgebra : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A] (S : StarSubalgebra R A),
  S.toNonUnitalStarSubalgebra.toStarSubalgebra ⋯ = S
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.CoreUnitCounit.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (unit : CategoryTheory.Functor.id C ⟶ F.comp G)
  (counit : G.comp F ⟶ CategoryTheory.Functor.id D)
  (left_triangle :
    autoParam
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight unit F)
          (CategoryTheory.CategoryStruct.comp (F.associator G F).hom (F.whiskerLeft counit)) =
        CategoryTheory.NatTrans.id ((CategoryTheory.Functor.id C).comp F))
      CategoryTheory.Adjunction.CoreUnitCounit.left_triangle._autoParam)
  (right_triangle :
    autoParam
      (CategoryTheory.CategoryStruct.comp (G.whiskerLeft unit)
          (CategoryTheory.CategoryStruct.comp (G.associator F G).inv (CategoryTheory.Functor.whiskerRight counit G)) =
        CategoryTheory.NatTrans.id (G.comp (CategoryTheory.Functor.id C)))
      CategoryTheory.Adjunction.CoreUnitCounit.right_triangle._autoParam)
  (unit_1 : CategoryTheory.Functor.id C ⟶ F.comp G) (counit_1 : G.comp F ⟶ CategoryTheory.Functor.id D)
  (left_triangle_1 :
    autoParam
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight unit_1 F)
          (CategoryTheory.CategoryStruct.comp (F.associator G F).hom (F.whiskerLeft counit_1)) =
        CategoryTheory.NatTrans.id ((CategoryTheory.Functor.id C).comp F))
      CategoryTheory.Adjunction.CoreUnitCounit.left_triangle._autoParam)
  (right_triangle_1 :
    autoParam
      (CategoryTheory.CategoryStruct.comp (G.whiskerLeft unit_1)
          (CategoryTheory.CategoryStruct.comp (G.associator F G).inv (CategoryTheory.Functor.whiskerRight counit_1 G)) =
        CategoryTheory.NatTrans.id (G.comp (CategoryTheory.Functor.id C)))
      CategoryTheory.Adjunction.CoreUnitCounit.right_triangle._autoParam),
  ({ unit := unit, counit := counit, left_triangle := left_triangle, right_triangle := right_triangle } =
      { unit := unit_1, counit := counit_1, left_triangle := left_triangle_1, right_triangle := right_triangle_1 }) =
    (unit = unit_1 ∧ counit = counit_1)
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.ForgetEnrichment.homTo_homOf : ∀ {C : Type u₁} (W : Type v) [inst : CategoryTheory.Category.{w, v} W] [inst_1 : CategoryTheory.MonoidalCategory W]
  [inst_2 : CategoryTheory.EnrichedCategory W C] {X Y : C}
  (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit W ⟶ X ⟶[W] Y),
  CategoryTheory.ForgetEnrichment.homTo W (CategoryTheory.ForgetEnrichment.homOf W f) = f
-- Mathlib.RingTheory.TwoSidedIdeal.Operations
TwoSidedIdeal.span_le : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] {s : Set R} {I : TwoSidedIdeal R}, TwoSidedIdeal.span s ≤ I ↔ s ⊆ ↑I
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral
/-- An integrability criterion for the continuous functional calculus.
This version assumes joint continuity of `f`, see `integrable_cfcₙ'` for a statement
with weaker assumptions.  -/
integrable_cfcₙ : ∀ {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : MeasurableSpace X]
  {μ : MeasureTheory.Measure X} [inst_2 : NonUnitalNormedRing A] [inst_3 : StarRing A] [inst_4 : NormedSpace 𝕜 A]
  [inst_5 : IsScalarTower 𝕜 A A] [inst_6 : SMulCommClass 𝕜 A A] [inst_7 : NonUnitalContinuousFunctionalCalculus 𝕜 A p]
  [CompleteSpace A] [inst_9 : TopologicalSpace X] [OpensMeasurableSpace X] (f : X → 𝕜 → 𝕜) (bound : X → ℝ) (a : A)
  [SecondCountableTopologyEither X C(↑(quasispectrum 𝕜 a), 𝕜)],
  ContinuousOn (Function.uncurry f) (Set.univ ×ˢ quasispectrum 𝕜 a) →
    (∀ᵐ (x : X) ∂μ, f x 0 = 0) →
      (∀ᵐ (x : X) ∂μ, ∀ z ∈ quasispectrum 𝕜 a, ‖f x z‖ ≤ bound x) →
        MeasureTheory.HasFiniteIntegral bound μ →
          autoParam (p a) integrable_cfcₙ._auto_1 → MeasureTheory.Integrable (fun x => cfcₙ (f x) a) μ
-- Mathlib.Data.NNReal.Defs
NNReal.instPartialOrder : PartialOrder NNReal
-- Mathlib.GroupTheory.PGroup
IsPGroup.iff_orderOf : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] [Fact (Nat.Prime p)], IsPGroup p G ↔ ∀ (g : G), ∃ k, orderOf g = p ^ k
-- Mathlib.Data.Matrix.Mul
Matrix.vecMul_diagonal_const : ∀ {m : Type u_2} {α : Type v} [inst : NonAssocSemiring α] [inst_1 : Fintype m] [inst_2 : DecidableEq m] (x : α)
  (v : m → α), Matrix.vecMul v (Matrix.diagonal fun x_1 => x) = MulOpposite.op x • v
-- Mathlib.Algebra.Group.Submonoid.Defs
Submonoid.mk_eq_one : ∀ {M : Type u_4} [inst : MulOneClass M] (S : Submonoid M) {a : M} {ha : a ∈ S}, ⟨a, ha⟩ = 1 ↔ a = 1
-- Lean.Widget.TaggedText
Lean.Widget.instToJsonTaggedText : {α : Type u_1} → [Lean.ToJson α] → Lean.ToJson (Lean.Widget.TaggedText α)
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
/-- An additive action of an additive monoid `α` on a type `β` gives an additive action of `Set α`
on `Set β`  -/
Set.addAction : {α : Type u_2} → {β : Type u_3} → [inst : AddMonoid α] → [AddAction α β] → AddAction (Set α) (Set β)
-- Mathlib.Analysis.Complex.Hadamard
Complex.HadamardThreeLines.norm_mul_invInterpStrip_le_one_of_mem_verticalClosedStrip : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (f : ℂ → E) (ε : ℝ),
  0 < ε →
    ∀ (z : ℂ),
      DiffContOnCl ℂ f (Complex.HadamardThreeLines.verticalStrip 0 1) →
        BddAbove (norm ∘ f '' Complex.HadamardThreeLines.verticalClosedStrip 0 1) →
          z ∈ Complex.HadamardThreeLines.verticalClosedStrip 0 1 → ‖Complex.HadamardThreeLines.F f ε z‖ ≤ 1
-- Mathlib.CategoryTheory.Preadditive.Projective.Resolution
CategoryTheory.ProjectiveResolution.instEpiFNatπ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} (P : CategoryTheory.ProjectiveResolution Z) (n : ℕ),
  CategoryTheory.Epi (P.π.f n)
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Subgroup.smul_sup : ∀ {α : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : Monoid α] [inst_2 : MulDistribMulAction α G] (a : α)
  (S T : Subgroup G), a • (S ⊔ T) = a • S ⊔ a • T
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoOfRangeEq_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Z)
  [hf : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] (g : Y ⟶ Z)
  [inst_1 : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion g]
  (e :
    Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base) = Set.range ⇑(CategoryTheory.ConcreteCategory.hom g.base)),
  (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoOfRangeEq f g e).hom =
    AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.lift g f ⋯
-- Mathlib.Data.Finsupp.Single
Finsupp.single_eq_zero : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {a : α} {b : M}, (fun₀ | a => b) = 0 ↔ b = 0
-- Mathlib.Algebra.Group.Submonoid.Units
AddMonoidHom.isAddUnit_eqLocusM_mk_iff : ∀ {M : Type u_1} [inst : AddMonoid M] {N : Type u_2} [inst_1 : AddMonoid N] (f g : M →+ N) {r : M} (hr : f r = g r),
  IsAddUnit ⟨r, hr⟩ ↔ IsAddUnit r
-- Mathlib.Data.Nat.PrimeFin
/-- A version of `Nat.exists_infinite_primes` using the `Set.Infinite` predicate.  -/
Nat.infinite_setOfPred_prime : {p | Nat.Prime p}.Infinite
-- Mathlib.NumberTheory.ModularForms.NormTrace
ModularForm.trace.congr_simp : ∀ {𝒢 𝒢_1 : Subgroup (GL (Fin 2) ℝ)} (e_𝒢 : 𝒢 = 𝒢_1) (ℋ : Subgroup (GL (Fin 2) ℝ)) {F : Type u_1} (f f_1 : F),
  f = f_1 →
    ∀ [inst : FunLike F UpperHalfPlane ℂ] {k : ℤ} [inst_1 : 𝒢.IsFiniteRelIndex ℋ] [inst_2 : ModularFormClass F 𝒢 k],
      ModularForm.trace ℋ f = ModularForm.trace ℋ f_1
-- Mathlib.Topology.Algebra.Group.GroupTopology
GroupTopology.mk.injEq : ∀ {α : Type u} [inst : Group α] (toTopologicalSpace : TopologicalSpace α) (toIsTopologicalGroup : IsTopologicalGroup α)
  (toTopologicalSpace_1 : TopologicalSpace α) (toIsTopologicalGroup_1 : IsTopologicalGroup α),
  ({ toTopologicalSpace := toTopologicalSpace, toIsTopologicalGroup := toIsTopologicalGroup } =
      { toTopologicalSpace := toTopologicalSpace_1, toIsTopologicalGroup := toIsTopologicalGroup_1 }) =
    (toTopologicalSpace = toTopologicalSpace_1)
-- Mathlib.ModelTheory.Complexity
_private.Mathlib.ModelTheory.Complexity.0.FirstOrder.Language.BoundedFormula.toPrenex.match_1.splitter : {L : FirstOrder.Language} →
  {α : Type u_3} →
    (motive : (x : ℕ) → L.BoundedFormula α x → Sort u_4) →
      (x : ℕ) →
        (x_1 : L.BoundedFormula α x) →
          ((x : ℕ) → motive x FirstOrder.Language.BoundedFormula.falsum) →
            ((x : ℕ) → (t₁ t₂ : L.Term (α ⊕ Fin x)) → motive x (FirstOrder.Language.BoundedFormula.equal t₁ t₂)) →
              ((x l : ℕ) →
                  (R : L.Relations l) →
                    (ts : Fin l → L.Term (α ⊕ Fin x)) → motive x (FirstOrder.Language.BoundedFormula.rel R ts)) →
                ((x : ℕ) → (f₁ f₂ : L.BoundedFormula α x) → motive x (f₁.imp f₂)) →
                  ((x : ℕ) → (f : L.BoundedFormula α (x + 1)) → motive x f.all) → motive x x_1
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanFileProgressKind.fatalError : Lean.Lsp.LeanFileProgressKind
-- Mathlib.CategoryTheory.Join.Basic
/-- Elements of `Join C D` are either elements of `C` or elements of `D`.  -/
CategoryTheory.Join.«term_⋆_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Order.Module.HahnEmbedding
HahnEmbedding.Seed.mk : {K : Type u_1} →
  [inst : DivisionRing K] →
    [inst_1 : LinearOrder K] →
      [inst_2 : IsOrderedRing K] →
        [inst_3 : Archimedean K] →
          {M : Type u_2} →
            [inst_4 : AddCommGroup M] →
              [inst_5 : LinearOrder M] →
                [inst_6 : IsOrderedAddMonoid M] →
                  [inst_7 : Module K M] →
                    [inst_8 : IsOrderedModule K M] →
                      {R : Type u_3} →
                        [inst_9 : AddCommGroup R] →
                          [inst_10 : LinearOrder R] →
                            [inst_11 : Module K R] →
                              (toArchimedeanStrata : HahnEmbedding.ArchimedeanStrata K M) →
                                (coeff : (c : FiniteArchimedeanClass M) → ↥(toArchimedeanStrata.stratum c) →ₗ[K] R) →
                                  (∀ (c : FiniteArchimedeanClass M), StrictMono ⇑(coeff c)) → HahnEmbedding.Seed K M R
-- Mathlib.Data.QPF.Univariate.Basic
/-- A pre-congruence on `q.P.M` *viewed as an F-coalgebra*. Not necessarily symmetric.  -/
QPF.IsPrecongr : {F : Type u → Type u} → [q : QPF F] → ((QPF.P F).M → (QPF.P F).M → Prop) → Prop
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.iIndepFun.indepFun_prod_range_succ₀ : ∀ {α : Type u_1} {Ω : Type u_2} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω}
  {μ : MeasureTheory.Measure α} {β : Type u_8} {m : MeasurableSpace β} [inst : CommMonoid β] [MeasurableMul₂ β]
  {f : ℕ → Ω → β},
  ProbabilityTheory.Kernel.iIndepFun f κ μ →
    (∀ (i : ℕ), AEMeasurable (f i) (μ.bind ⇑κ)) →
      ∀ (n : ℕ), ProbabilityTheory.Kernel.IndepFun (∏ j ∈ Finset.range n, f j) (f n) κ μ
-- Mathlib.Data.Nat.MaxPowDiv
Nat.maxPowDvdDiv.eq_def : ∀ (p n : ℕ), p.maxPowDvdDiv n = if H : 1 < p ∧ n ≠ 0 then Nat.maxPowDvdDiv.go n p H else (0, n)
-- Mathlib.Algebra.Lie.Weights.Chain
LieModule.genWeightSpaceChain.congr_simp : ∀ {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]
  [inst_7 : LieRing.IsNilpotent L] (χ₁ χ₁_1 : L → R),
  χ₁ = χ₁_1 →
    ∀ (χ₂ χ₂_1 : L → R),
      χ₂ = χ₂_1 →
        ∀ (p p_1 : ℤ),
          p = p_1 →
            ∀ (q q_1 : ℤ),
              q = q_1 → LieModule.genWeightSpaceChain M χ₁ χ₂ p q = LieModule.genWeightSpaceChain M χ₁_1 χ₂_1 p_1 q_1
-- Mathlib.Order.Filter.Ultrafilter.Defs
Ultrafilter.instInhabited : {α : Type u} → [Inhabited α] → Inhabited (Ultrafilter α)
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.Word.Pair.mk.sizeOf_spec : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] {i : ι} [inst_1 : SizeOf ι]
  [inst_2 : (a : ι) → SizeOf (M a)] (head : M i) (tail : Monoid.CoprodI.Word M) (fstIdx_ne : tail.fstIdx ≠ some i),
  sizeOf { head := head, tail := tail, fstIdx_ne := fstIdx_ne } = 1 + sizeOf head + sizeOf tail
-- Mathlib.Order.Atoms
isSimpleOrder_iff_isAtom_top : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : BoundedOrder α], IsSimpleOrder α ↔ IsAtom ⊤
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEFinStronglyMeasurable.ae_eq_zero_compl : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace β]
  {f : α → β} [inst_1 : Zero β] [inst_2 : T2Space β] (hf : MeasureTheory.AEFinStronglyMeasurable f μ),
  f =ᵐ[μ.restrict hf.sigmaFiniteSetᶜ] 0
-- Mathlib.Analysis.SpecialFunctions.CompareExp
/-- If `l : Filter ℂ` is an "exponential comparison filter", then for any complex `a` and any
positive real `b`, we have `(fun z ↦ z ^ a) =o[l] (fun z ↦ exp (b * z))`.  -/
Complex.IsExpCmpFilter.isLittleO_cpow_exp : ∀ {l : Filter ℂ},
  Complex.IsExpCmpFilter l → ∀ (a : ℂ) {b : ℝ}, 0 < b → (fun z => z ^ a) =o[l] fun z => Complex.exp (↑b * z)
-- Mathlib.Probability.Moments.IntegrableExpMul
/-- If `ω ↦ exp (t * X ω)` is integrable at `t` and `-t` for `t ≠ 0`, then `ω ↦ |X ω| ^ n` is
integrable for all `n : ℕ`. That is, all moments of `X` are finite.  -/
ProbabilityTheory.integrable_pow_abs_of_integrable_exp_mul : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ},
  t ≠ 0 →
    MeasureTheory.Integrable (fun ω => Real.exp (t * X ω)) μ →
      MeasureTheory.Integrable (fun ω => Real.exp (-t * X ω)) μ →
        ∀ (n : ℕ), MeasureTheory.Integrable (fun ω => |X ω| ^ n) μ
-- Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
/-- If `x` is a root of unity (spelled as `IsOfFinOrder x`) in an `n`-th cyclotomic extension of
`ℚ`, where `n` is odd, and `ζ` is a primitive `n`-th root of unity, then there exists `r < n`
such that `x = ζ^r` or `x = -ζ^r`.  -/
IsPrimitiveRoot.exists_pow_or_neg_mul_pow_of_isOfFinOrder : ∀ {n : ℕ} [NeZero n] {K : Type u} [inst : Field K] [inst_1 : NumberField K] [IsCyclotomicExtension {n} ℚ K],
  Odd n → ∀ {ζ x : K}, IsPrimitiveRoot ζ n → IsOfFinOrder x → ∃ r < n, x = ζ ^ r ∨ x = -ζ ^ r
-- Mathlib.Combinatorics.SimpleGraph.StronglyRegular
_private.Mathlib.Combinatorics.SimpleGraph.StronglyRegular.0.SimpleGraph.conway_99 : ProofWanted (∃ α x g x_1, g.IsSRGWith 99 14 1 2)
-- Mathlib.LinearAlgebra.CliffordAlgebra.Fold
CliffordAlgebra.foldl_algebraMap : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] (Q : QuadraticForm R M) (f : M →ₗ[R] N →ₗ[R] N)
  (hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x) (n : N) (r : R),
  ((CliffordAlgebra.foldl Q f hf) n) ((algebraMap R (CliffordAlgebra Q)) r) = r • n
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.erase_emptyWithCapacity : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {k : α} {c : ℕ},
  (Std.DHashMap.emptyWithCapacity c).erase k = Std.DHashMap.emptyWithCapacity c
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
ContinuousLinearMap.lTensor_pow : ∀ {𝕜 : Type u_1} {E : Type u_2} (G : Type u_4) [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup G] [inst_4 : InnerProductSpace 𝕜 G] (f : E →L[𝕜] E)
  (n : ℕ), ContinuousLinearMap.lTensor G (f ^ n) = ContinuousLinearMap.lTensor G f ^ n
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSpace.mkOfClosure_sets : ∀ {α : Type u_1} {s : Set (Set α)} {hs : {t | MeasurableSet t} = s},
  MeasurableSpace.mkOfClosure s hs = MeasurableSpace.generateFrom s
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Iso.isoFunctorOfIsoInverse_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {G G' : C ≌ D} (i : G.inverse ≅ G'.inverse) (X : C),
  i.isoFunctorOfIsoInverse.hom.app X =
    CategoryTheory.CategoryStruct.comp (G'.counitIso.inv.app (G.functor.obj X))
      (CategoryTheory.CategoryStruct.comp (G'.functor.map (i.inv.app (G.functor.obj X)))
        (G'.functor.map (G.unitIso.inv.app X)))
-- Lean.Data.Json.Basic
Lean.Json.bool : Bool → Lean.Json
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.cof_bsup_le_lift : ∀ {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}},
  (∀ (i : Ordinal.{u}) (h : i < o), f i h < o.bsup f) → (o.bsup f).cof ≤ Cardinal.lift.{v, u} o.card
-- Mathlib.CategoryTheory.Category.ULift
/-- The obvious function `ULiftHom C → C`.  -/
CategoryTheory.ULiftHom.objDown : {C : Type u_1} → CategoryTheory.ULiftHom C → C
-- Mathlib.Analysis.Normed.Group.Defs
/-- A seminormed group is an additive group endowed with a norm for which `dist x y = ‖-x + y‖`
defines a pseudometric space structure.  -/
SeminormedAddCommGroup : Type u_8 → Type u_8
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- The product of `f g : SkewMonoidAlgebra k G` is the finitely supported function whose value
at `a` is the sum of `f x * (x • g y)` over all pairs `x, y` such that `x * y = a`.
(Think of a skew group ring.)  -/
SkewMonoidAlgebra.instMul : {k : Type u_1} →
  {G : Type u_2} → [Mul G] → [SMul G k] → [inst : NonUnitalNonAssocSemiring k] → Mul (SkewMonoidAlgebra k G)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.denote_powC : ∀ {α : Type u_1} {c : ℕ} [inst : Lean.Grind.CommRing α] [Lean.Grind.IsCharP α c] (ctx : Lean.Grind.CommRing.Context α)
  (p : Lean.Grind.CommRing.Poly) (k : ℕ),
  Lean.Grind.CommRing.Poly.denote ctx (p.powC k c) = Lean.Grind.CommRing.Poly.denote ctx p ^ k
-- Mathlib.Algebra.Lie.Weights.Killing
/-- The `sl₂` subalgebra associated to a root, regarded as a Lie submodule over the Cartan
subalgebra.  -/
LieAlgebra.IsKilling.sl2SubmoduleOfRoot : {K : Type u_2} →
  {L : Type u_3} →
    [inst : LieRing L] →
      [inst_1 : Field K] →
        [inst_2 : LieAlgebra K L] →
          [FiniteDimensional K L] →
            {H : LieSubalgebra K L} →
              [inst_4 : H.IsCartanSubalgebra] →
                [LieAlgebra.IsKilling K L] →
                  [LieModule.IsTriangularizable K (↥H) L] →
                    [CharZero K] → {α : LieModule.Weight K (↥H) L} → α.IsNonZero → LieSubmodule K (↥H) L
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.norm_map : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (e : E ≃ₛₗᵢ[σ₁₂] E₂) (x : E), ‖e x‖ = ‖x‖
-- Lean.Expr
Lean.instInhabitedFVarId : Inhabited Lean.FVarId
-- Mathlib.CategoryTheory.Join.Basic
_private.Mathlib.CategoryTheory.Join.Basic.0.CategoryTheory.Join.Hom.match_1.eq_2 : ∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_1, u_3} C] {D : Type u_4}
  [inst_1 : CategoryTheory.Category.{u_2, u_4} D]
  (motive : CategoryTheory.Join C D → CategoryTheory.Join C D → Sort u_5) (x y : D)
  (h_1 : (x y : C) → motive (CategoryTheory.Join.left x) (CategoryTheory.Join.left y))
  (h_2 : (x y : D) → motive (CategoryTheory.Join.right x) (CategoryTheory.Join.right y))
  (h_3 : (a : C) → (a_1 : D) → motive (CategoryTheory.Join.left a) (CategoryTheory.Join.right a_1))
  (h_4 : (a : D) → (a_1 : C) → motive (CategoryTheory.Join.right a) (CategoryTheory.Join.left a_1)),
  (match CategoryTheory.Join.right x, CategoryTheory.Join.right y with
    | CategoryTheory.Join.left x, CategoryTheory.Join.left y => h_1 x y
    | CategoryTheory.Join.right x, CategoryTheory.Join.right y => h_2 x y
    | CategoryTheory.Join.left a, CategoryTheory.Join.right a_1 => h_3 a a_1
    | CategoryTheory.Join.right a, CategoryTheory.Join.left a_1 => h_4 a a_1) =
    h_2 x y
-- Init.Data.Nat.Lemmas
Nat.pow_dvd_pow_iff_le_right' : ∀ {b k l : ℕ}, (b + 2) ^ k ∣ (b + 2) ^ l ↔ k ≤ l
-- Mathlib.Topology.Path
Path.refl_trans_refl : ∀ {X : Type u_1} [inst : TopologicalSpace X] {a : X}, (Path.refl a).trans (Path.refl a) = Path.refl a
-- Mathlib.Data.Matrix.Basic
Equiv.mapMatrix_trans : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_11} {β : Type u_12} {γ : Type u_13} (f : α ≃ β) (g : β ≃ γ),
  f.mapMatrix.trans g.mapMatrix = (f.trans g).mapMatrix
-- Mathlib.GroupTheory.Coset.Basic
orbit_subgroup_one_eq_self : ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α), MulAction.orbit (↥s) 1 = ↑s
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.norm_eq_ciSup : ∀ {α : Type u_3} {E : α → Type u_4} [inst : (i : α) → NormedAddCommGroup (E i)] (f : ↥(lp E ⊤)), ‖f‖ = ⨆ i, ‖↑f i‖
-- Mathlib.Order.Hom.WithTopBot
LatticeHom.withTop'_toFun : ∀ {α : Type u_1} {β : Type u_2} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : OrderTop β] (f : LatticeHom α β)
  (a : WithTop α), f.withTop' a = Option.elim a ⊤ ⇑f
-- Mathlib.ModelTheory.Definability
Function.tupleGraph.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (f : (α → β) → β), Function.tupleGraph f = {v | f (v ∘ some) = v none}
-- Mathlib.Topology.WithTopology
/-- Injectivity lemma for the constructor `toTopology t`.

It is not marked as `@[simp]`, because its autogenerated version
is already in the default `simp` set.  -/
WithTopology.toTopology_inj : ∀ {X : Type u_1} (t : TopologicalSpace X) {x y : X}, WithTopology.toTopology t x = WithTopology.toTopology t y ↔ x = y