mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
/-- If there is a primitive `n`-th root of unity in `K`, then
`cyclotomic' n K = (X ^ k - 1) /ₘ (∏ i ∈ Nat.properDivisors k, cyclotomic' i K)`.  -/
Polynomial.cyclotomic'_eq_X_pow_sub_one_div : ∀ {K : Type u_2} [inst : CommRing K] [inst_1 : IsDomain K] {ζ : K} {n : ℕ},
  0 < n →
    IsPrimitiveRoot ζ n →
      Polynomial.cyclotomic' n K = (Polynomial.X ^ n - 1) /ₘ ∏ i ∈ n.properDivisors, Polynomial.cyclotomic' i K
-- Mathlib.Analysis.RCLike.Basic
RCLike.div_re : ∀ {K : Type u_1} [inst : RCLike K] (z w : K),
  RCLike.re (z / w) = RCLike.re z * RCLike.re w / RCLike.normSq w + RCLike.im z * RCLike.im w / RCLike.normSq w
-- Mathlib.NumberTheory.RamificationInertia.Inertia
/-- **Alias** of `Ideal.inertiaDeg'_algebraMap`. -/
Ideal.inertiaDeg_algebraMap : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R) (P : Ideal S)
  [inst_3 : P.LiesOver p], p.inertiaDeg' P = Module.finrank (R ⧸ p) (S ⧸ P)
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.closure_range_of : ∀ (α : Type u_1), AddSubgroup.closure (Set.range FreeAddGroup.of) = ⊤
-- Mathlib.SetTheory.Cardinal.Free
instCountableFreeRing : ∀ (α : Type u) [Countable α], Countable (FreeRing α)
-- Mathlib.GroupTheory.PGroup
/-- **Alias** of the forward direction of `isPGroup_iff_exponent_eq_pow`. -/
IsPGroup.exists_exponent_eq_pow : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] [Finite G] [Fact (Nat.Prime p)], IsPGroup p G → ∃ n, Monoid.exponent G = p ^ n
-- Mathlib.Algebra.CharP.Lemmas
sum_pow_char_pow : ∀ {R : Type u_3} [inst : CommSemiring R] (p n : ℕ) [ExpChar R p] {ι : Type u_4} (s : Finset ι) (f : ι → R),
  (∑ i ∈ s, f i) ^ p ^ n = ∑ i ∈ s, f i ^ p ^ n
-- Mathlib.Algebra.Order.Monoid.Lex
OrderMonoidHom.inlₗ_apply : ∀ (α : Type u_1) (β : Type u_2) [inst : Monoid α] [inst_1 : PartialOrder α] [inst_2 : Monoid β] [inst_3 : Preorder β]
  (a : α), (OrderMonoidHom.inlₗ α β) a = toLex (a, 1)
-- Mathlib.Algebra.FiniteSupport.Basic
/-- Eta-expanded form of `Function.HasFiniteSupport.add` -/
Function.HasFiniteSupport.fun_add : ∀ {α : Type u_1} {M : Type u_3} [inst : AddZeroClass M] {f g : α → M},
  Function.HasFiniteSupport f → Function.HasFiniteSupport g → Function.HasFiniteSupport fun i => f i + g i
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
/-- The tangent of an angle in a right-angled triangle multiplied by the adjacent side equals
the opposite side, version subtracting vectors.  -/
InnerProductGeometry.tan_angle_sub_mul_norm_of_inner_eq_zero : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
  inner ℝ x y = 0 → x ≠ 0 ∨ y = 0 → Real.tan (InnerProductGeometry.angle x (x - y)) * ‖x‖ = ‖y‖
-- Init.Data.Range.Polymorphic.UInt
UInt16.instLawfulHasSize_1 : Std.Rxo.LawfulHasSize UInt16
-- Mathlib.LinearAlgebra.RootSystem.IsValuedIn
RootPairing.rootSpan_mem_invtSubmodule_reflection : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (i : ι),
  P.rootSpan R ∈ Module.End.invtSubmodule ↑(P.reflection i)
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.map_star_eq_diagonal : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : AddMonoid α] [inst_2 : StarAddMonoid α]
  {M : Matrix n n α} {v : n → α}, M.map star = Matrix.diagonal v ↔ M = Matrix.diagonal (star v)
-- Mathlib.Analysis.Analytic.CPolynomial
ContinuousMultilinearMap.analyticOnNhd_uncurry_compContinuousLinearMap : ∀ {𝕜 : Type u_1} {G : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup G]
  [inst_2 : NormedSpace 𝕜 G] {ι : Type u_5} {Em : ι → Type u_6} {Fm : ι → Type u_7}
  [inst_3 : (i : ι) → NormedAddCommGroup (Em i)] [inst_4 : (i : ι) → NormedSpace 𝕜 (Em i)]
  [inst_5 : (i : ι) → NormedAddCommGroup (Fm i)] [inst_6 : (i : ι) → NormedSpace 𝕜 (Fm i)] [inst_7 : Fintype ι]
  {t : Set (((i : ι) → Fm i →L[𝕜] Em i) × ContinuousMultilinearMap 𝕜 Em G)},
  AnalyticOnNhd 𝕜 (fun p => p.2.compContinuousLinearMap p.1) t
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.Y.congr_simp : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3}
  (S S_1 : FermatLastTheoremForThreeGen.Solution✝ hζ),
  S = S_1 →
    ∀ [inst_1 : NumberField K] [inst_2 : IsCyclotomicExtension {3} ℚ K],
      FermatLastTheoremForThreeGen.Solution.Y✝ S = FermatLastTheoremForThreeGen.Solution.Y✝ S_1
-- Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Asymptotics.superpolynomialDecay_mul_param_pow_iff : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {k : α → β} (f : α → β) [inst : TopologicalSpace β] [inst_1 : Field β]
  [inst_2 : LinearOrder β] [IsStrictOrderedRing β] [OrderTopology β],
  Filter.Tendsto k l Filter.atTop →
    ∀ (n : ℕ), Asymptotics.SuperpolynomialDecay l k (f * k ^ n) ↔ Asymptotics.SuperpolynomialDecay l k f
-- Lean.Meta.Tactic.Congr
_private.Lean.Meta.Tactic.Congr.0.Lean.MVarId.congrN.go : Bool → Bool → ℕ → Lean.MVarId → StateRefT' IO.RealWorld (Array Lean.MVarId) Lean.MetaM Unit
-- Init.Grind.Order
Lean.Grind.Order.le_trans_k : ∀ {α : Type u_1} [inst : LE α] [inst_1 : LT α] [Std.LawfulOrderLT α] [inst_3 : Std.IsPreorder α]
  [inst_4 : Lean.Grind.Ring α] [Lean.Grind.OrderedRing α] {a b c : α} {k₁ k₂ : ℤ} (k : ℤ),
  a ≤ b + ↑k₁ → b ≤ c + ↑k₂ → (k == k₂ + k₁) = true → a ≤ c + ↑k
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue?_cons_of_false : ∀ {α : Type u} {β : Type v} [inst : BEq α] {l : List ((_ : α) × β)} {k a : α} {v : β},
  (k == a) = false → Std.Internal.List.getValue? a (⟨k, v⟩ :: l) = Std.Internal.List.getValue? a l
-- Mathlib.Algebra.Category.ModuleCat.ExteriorPower
/-- The isomorphism `M.exteriorPower 1 ≅ M`.  -/
ModuleCat.exteriorPower.iso₁ : {R : Type u} → [inst : CommRing R] → (M : ModuleCat R) → M.exteriorPower 1 ≅ M
-- Mathlib.Algebra.Lie.Cochain
LieModule.Cohomology.d₂₃.congr_simp : ∀ (R : Type u_1) [inst : CommRing R] (L : Type u_2) [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],
  LieModule.Cohomology.d₂₃ R L M = LieModule.Cohomology.d₂₃ R L M
-- Mathlib.Data.List.Intervals
List.Ico.map_sub : ∀ (n m k : ℕ), k ≤ n → List.map (fun x => x - k) (List.Ico n m) = List.Ico (n - k) (m - k)
-- Mathlib.CategoryTheory.Limits.Constructions.Equalizers
/-- Any category with pullbacks and binary products, has equalizers.  -/
CategoryTheory.Limits.hasCoequalizers_of_hasPushouts_and_binary_coproducts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C]
  [CategoryTheory.Limits.HasPushouts C], CategoryTheory.Limits.HasCoequalizers C
-- Mathlib.Tactic.Widget.StringDiagram
/-- The name of the context.  -/
Mathlib.Tactic.Widget.StringDiagram.Kind.name : Mathlib.Tactic.Widget.StringDiagram.Kind → Lean.Name
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.imI_mul : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} [inst : Ring R] (a b : QuaternionAlgebra R c₁ c₂ c₃),
  (a * b).imI = a.re * b.imI + a.imI * b.re + c₂ * a.imI * b.imI - c₃ * a.imJ * b.imK + c₃ * a.imK * b.imJ
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
HomologicalComplex.extendHomologyIso_hom_naturality_assoc : ∀ {ι : 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]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {K L : HomologicalComplex C c} (φ : K ⟶ L) (e : c.Embedding c')
  {j : ι} {j' : ι'} (hj' : e.f j = j') [inst_3 : K.HasHomology j] [inst_4 : L.HasHomology j]
  [inst_5 : (K.extend e).HasHomology j'] [inst_6 : (L.extend e).HasHomology j'] {Z : C} (h : L.homology j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (HomologicalComplex.extendMap φ e) j')
      (CategoryTheory.CategoryStruct.comp (L.extendHomologyIso e hj').hom h) =
    CategoryTheory.CategoryStruct.comp (K.extendHomologyIso e hj').hom
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap φ j) h)
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.mem_prod : ∀ {x y z : ZFSet.{u}}, z ∈ x.prod y ↔ ∃ a ∈ x, ∃ b ∈ y, z = a.pair b
-- Lean.Environment
Lean.importModulesCore : Array Lean.Import →
  (globalLevel : optParam Lean.OLeanLevel Lean.OLeanLevel.private) →
    optParam (Lean.NameMap Lean.ImportArtifacts) ∅ →
      optParam Bool (decide (globalLevel < Lean.OLeanLevel.private)) → optParam Bool false → Lean.ImportStateM Unit
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.sPolynomial_monomial_mul' : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommRing R] [NoZeroDivisors R] (p₁ p₂ : MvPolynomial σ R)
  (d₁ d₂ : σ →₀ ℕ) (c₁ c₂ : R),
  m.sPolynomial ((MvPolynomial.monomial d₁) c₁ * p₁) ((MvPolynomial.monomial d₂) c₂ * p₂) =
    (MvPolynomial.monomial
          (m.degree ((MvPolynomial.monomial d₁) c₁ * p₁) ⊔ m.degree ((MvPolynomial.monomial d₂) c₂ * p₂) -
            m.degree p₁ ⊔ m.degree p₂))
        (c₁ * c₂) *
      m.sPolynomial p₁ p₂
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
CategoryTheory.Lax.OplaxTrans.Modification.ext : ∀ {B : Type u₁} {inst : CategoryTheory.Bicategory B} {C : Type u₂} {inst_1 : CategoryTheory.Bicategory C}
  {F G : CategoryTheory.LaxFunctor B C} {η θ : F ⟶ G} {x y : CategoryTheory.Lax.OplaxTrans.Modification η θ},
  x.app = y.app → x = y
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.Triangle.mor₁_eq_zero_of_epi₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles, CategoryTheory.Epi T.mor₃ → T.mor₁ = 0
-- Mathlib.Topology.Closure
subset_interior_union : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, interior s ∪ interior t ⊆ interior (s ∪ t)
-- Mathlib.GroupTheory.GroupExtension.Basic
GroupExtension.Splitting.conjAct.eq_1 : ∀ {N : Type u_1} {G : Type u_2} [inst : Group N] [inst_1 : Group G] {E : Type u_3} [inst_2 : Group E]
  {S : GroupExtension N E G} (s : S.Splitting), s.conjAct = S.conjAct.comp ↑s
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
/-- **Alias** of `CovariantDerivative.ContMDiffCovariantDerivative.finiteAffineCombination`.

---

An affine combination of finitely many `C^k` connections is a `C^k` connection.  -/
CovariantDerivative.ContMDiffCovariantDerivative.finite_affine_combination : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : ∀ (x : M), IsTopologicalAddGroup (V x)]
  [inst_13 : ∀ (x : M), ContinuousSMul 𝕜 (V x)] [inst_14 : FiberBundle F V] [inst_15 : IsManifold I 1 M]
  [inst_16 : VectorBundle 𝕜 F V] {ι : Type u_7} {s : Finset ι} (cov : ι → CovariantDerivative I F V) {f : ι → M → 𝕜}
  (hf : ∑ i ∈ s, f i = 1) {n : WithTop ℕ∞},
  (∀ i ∈ s, ContMDiff I (modelWithCornersSelf 𝕜 𝕜) n (f i)) →
    (∀ i ∈ s, (cov i).ContMDiffCovariantDerivative n) →
      (CovariantDerivative.finiteAffineCombination cov hf).ContMDiffCovariantDerivative n
-- Lean.Meta.Tactic.FunIndInfo
Lean.Meta.FunIndInfo.mk.inj : ∀ {funName funIndName : Lean.Name} {levelMask : Array Bool} {params : Array Lean.Meta.FunIndParamKind}
  {funName_1 funIndName_1 : Lean.Name} {levelMask_1 : Array Bool} {params_1 : Array Lean.Meta.FunIndParamKind},
  { funName := funName, funIndName := funIndName, levelMask := levelMask, params := params } =
      { funName := funName_1, funIndName := funIndName_1, levelMask := levelMask_1, params := params_1 } →
    funName = funName_1 ∧ funIndName = funIndName_1 ∧ levelMask = levelMask_1 ∧ params = params_1
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.liftAddHom_apply : ∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : AddZeroClass M] [inst_1 : AddCommMonoid N] (F : α → M →+ N)
  (f : α →₀ M), (Finsupp.liftAddHom F) f = f.sum fun x => ⇑(F x)
-- Mathlib.CategoryTheory.Monoidal.Action.End
CategoryTheory.MonoidalCategory.MonoidalRightAction.actionOfMonoidalFunctorToEndofunctor_actionUnitIso_hom : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) [inst_3 : F.Monoidal] (d : D),
  (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso d).hom =
    (CategoryTheory.Functor.OplaxMonoidal.η F).app d
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKey!_eq_iff_mem_and_forall : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [inst_2 : Inhabited α],
  t ≠ ∅ → ∀ {km : α}, t.maxKey! = km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
CategoryTheory.StructuredArrow.instHasColimitsOfShapeOfIsConnected : ∀ {J : Type u'} [inst : CategoryTheory.Category.{v', u'} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {D : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} D] {K : CategoryTheory.Functor C D} {B : D}
  [CategoryTheory.IsConnected J] [CategoryTheory.Limits.HasColimitsOfShape J C],
  CategoryTheory.Limits.HasColimitsOfShape J (CategoryTheory.StructuredArrow B K)
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.pair_preimage_singleton : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] (f : MeasureTheory.SimpleFunc α β)
  (g : MeasureTheory.SimpleFunc α γ) (b : β) (c : γ), ⇑(f.pair g) ⁻¹' {(b, c)} = ⇑f ⁻¹' {b} ∩ ⇑g ⁻¹' {c}
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous
SheafOfModules.instIsRightAdjointPushforwardIdSheafRingCat : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {S : CategoryTheory.Sheaf J RingCat}, (SheafOfModules.pushforward (CategoryTheory.CategoryStruct.id S)).IsRightAdjoint
-- Mathlib.Data.List.Duplicate
List.duplicate_cons_iff_of_ne : ∀ {α : Type u_1} {l : List α} {x y : α}, x ≠ y → (List.Duplicate x (y :: l) ↔ List.Duplicate x l)
-- Init.Data.Float.Model.Unpacked.Round
/-- Given a finite float represented by a sign, mantissa and exponent, together with an
`Accuracy` datum, round it to conform to the given `Format`.

Important: this function will only drop bits from the mantissa and increase the exponent,
not the other way around. The result will only conform to the given specification if
the exponent was not too large to begin with. If this may be the case, you should call
`round` instead.
 -/
Float.Model.UnpackedFloat.roundWithAccuracy : Float.Model.Format →
  Float.Model.UnpackedFloat.Sign → ℕ → ℤ → Float.Model.UnpackedFloat.Accuracy → Float.Model.UnpackedFloat
-- Mathlib.RingTheory.Kaehler.Basic
/-- The endomorphisms of `Ω[S⁄R]` corresponds to sections of the surjection `S ⊗[R] S ⧸ J ^ 2 →ₐ[R] S`,
with `J` being the kernel of the multiplication map `S ⊗[R] S →ₐ[R] S`.
 -/
KaehlerDifferential.endEquiv : (R : Type u) →
  (S : Type v) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          Module.End S Ω[S⁄R] ≃ { f // (Algebra.TensorProduct.lmul' R).kerSquareLift.comp f = AlgHom.id R S }
-- Mathlib.Topology.UrysohnsLemma
Urysohns.CU.approx_le_lim : ∀ {X : Type u_1} [inst : TopologicalSpace X] {P : Set X → Set X → Prop} (c : Urysohns.CU P) (x : X) (n : ℕ),
  Urysohns.CU.approx n c x ≤ c.lim x
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instContinuousConstSMul : ∀ {α : Type u_1} [inst : TopologicalSpace α] {R : Type u_3} {M : Type u_5} [inst_1 : TopologicalSpace M]
  [inst_2 : SMul R M] [inst_3 : ContinuousConstSMul R M], ContinuousConstSMul R C(α, M)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
/-- The property of reflecting initial objects expressed in terms of `IsInitial`.  -/
CategoryTheory.Limits.IsInitial.isInitialOfObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor C D) →
          (X : C) →
            [CategoryTheory.Limits.ReflectsColimit (CategoryTheory.Functor.empty C) G] →
              CategoryTheory.Limits.IsInitial (G.obj X) → CategoryTheory.Limits.IsInitial X
-- Mathlib.CategoryTheory.WithTerminal.Cone
_private.Mathlib.CategoryTheory.WithTerminal.Cone.0.CategoryTheory.WithInitial.liftFromUnderComp.match_1.splitter : {J : Type u_1} →
  (motive : CategoryTheory.WithInitial J → Sort u_2) →
    (x : CategoryTheory.WithInitial J) →
      (Unit → motive CategoryTheory.WithInitial.star) → ((a : J) → motive (CategoryTheory.WithInitial.of a)) → motive x
-- Init.Grind.AC
Lean.Grind.AC.Seq.unionFuel.match_1.congr_eq_2 : ∀ (motive : Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Sort u_1) (s₁ s₂ : Lean.Grind.AC.Seq)
  (h_1 : (x₁ x₂ : Lean.Grind.AC.Var) → motive (Lean.Grind.AC.Seq.var x₁) (Lean.Grind.AC.Seq.var x₂))
  (h_2 :
    (x₁ x : Lean.Grind.AC.Var) →
      (s : Lean.Grind.AC.Seq) → motive (Lean.Grind.AC.Seq.var x₁) (Lean.Grind.AC.Seq.cons x s))
  (h_3 :
    (x : Lean.Grind.AC.Var) →
      (s : Lean.Grind.AC.Seq) →
        (x₂ : Lean.Grind.AC.Var) → motive (Lean.Grind.AC.Seq.cons x s) (Lean.Grind.AC.Seq.var x₂))
  (h_4 :
    (x₁ : Lean.Grind.AC.Var) →
      (s₁ : Lean.Grind.AC.Seq) →
        (x₂ : Lean.Grind.AC.Var) →
          (s₂ : Lean.Grind.AC.Seq) → motive (Lean.Grind.AC.Seq.cons x₁ s₁) (Lean.Grind.AC.Seq.cons x₂ s₂))
  (x₁ x : Lean.Grind.AC.Var) (s : Lean.Grind.AC.Seq),
  s₁ = Lean.Grind.AC.Seq.var x₁ →
    s₂ = Lean.Grind.AC.Seq.cons x s →
      (match s₁, s₂ with
        | Lean.Grind.AC.Seq.var x₁, Lean.Grind.AC.Seq.var x₂ => h_1 x₁ x₂
        | Lean.Grind.AC.Seq.var x₁, Lean.Grind.AC.Seq.cons x s => h_2 x₁ x s
        | Lean.Grind.AC.Seq.cons x s, Lean.Grind.AC.Seq.var x₂ => h_3 x s x₂
        | Lean.Grind.AC.Seq.cons x₁ s₁, Lean.Grind.AC.Seq.cons x₂ s₂ => h_4 x₁ s₁ x₂ s₂) ≍
        h_2 x₁ x s
-- Mathlib.Topology.Convenient.Category
/-- The type of morphisms in the category `ContinuousGeneratedByCat X` is
a one-field structure containing a field of type `ContinuousMapGeneratedBy`,
i.e. `X`-continuous maps.  -/
ContinuousGeneratedByCat.Hom : {ι : Type t} →
  {X : ι → Type u} →
    [inst : (i : ι) → TopologicalSpace (X i)] → ContinuousGeneratedByCat X → ContinuousGeneratedByCat X → Type v
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.instVAddCoeOfVAddMemClass.eq_1 : ∀ {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)]
  {B : (i : ι) → S i} {G : Type u_4} [inst_1 : (i : ι) → VAdd G (R i)] [inst_2 : ∀ (i : ι), VAddMemClass (S i) G (R i)],
  RestrictedProduct.instVAddCoeOfVAddMemClass R = { vadd := fun g x => ⟨fun i => g +ᵥ x i, ⋯⟩ }
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.ofLp_listSum : ∀ (p : ENNReal) (V : Type u_4) [inst : AddCommGroup V] (l : List (WithLp p V)),
  l.sum.ofLp = (List.map WithLp.ofLp l).sum
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.ElabLink.mk.inj : ∀ {name name_1 : Lean.StrLit}, { name := name } = { name := name_1 } → name = name_1
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.map_eval : ∀ {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring S₁] {S₂ : Type u_2} [inst_1 : CommSemiring S₂] (q : S₁ →+* S₂)
  (g : σ → S₁) (p : MvPolynomial σ S₁),
  q ((MvPolynomial.eval g) p) = (MvPolynomial.eval (⇑q ∘ g)) ((MvPolynomial.map q) p)
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.includeRight_bijective : ∀ {R : Type uR} {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B],
  Function.Bijective ⇑(algebraMap R A) → Function.Bijective ⇑Algebra.TensorProduct.includeRight
-- Mathlib.GroupTheory.Sylow
/-- Sylow subgroups are isomorphic  -/
Sylow.equiv : {p : ℕ} →
  {G : Type u_1} → [inst : Group G] → [Fact (Nat.Prime p)] → [Finite (Sylow p G)] → (P Q : Sylow p G) → ↥↑P ≃* ↥↑Q
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Finset.aestronglyMeasurable_fun_sum : ∀ {α : Type u_1} {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {M : Type u_5} [inst : AddCommMonoid M]
  [inst_1 : TopologicalSpace M] [ContinuousAdd M] {ι : Type u_6} {f : ι → α → M} (s : Finset ι),
  (∀ i ∈ s, MeasureTheory.AEStronglyMeasurable (f i) μ) → MeasureTheory.AEStronglyMeasurable (fun a => ∑ i ∈ s, f i a) μ
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.sub : {m : Type u_2} → {n : Type u_3} → {α : Type v} → [Sub α] → Sub (Matrix m n α)
-- Mathlib.Topology.LocallyConstant.Basic
LocallyConstant.apply_eq_of_preconnectedSpace : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [PreconnectedSpace X] (f : LocallyConstant X Y) (x y : X),
  f x = f y
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.Hom.ext : ∀ {R : Type u} {inst : Ring R} {M N : ModuleCat R} {x y : M.Hom N}, x.hom' = y.hom' → x = y
-- Std.Http.Data.Response
/-- Sets the HTTP status code for the response being built.
 -/
Std.Http.Response.Builder.status : Std.Http.Response.Builder → Std.Http.Status → Std.Http.Response.Builder
-- Init.Data.String.Lemmas.Pattern.Char
_private.Init.Data.String.Lemmas.Pattern.Char.0.String.Slice.takeEndWhile.eq_1 : ∀ {ρ : Type} (s : String.Slice) (pat : ρ) [inst : String.Slice.Pattern.BackwardPattern pat],
  s.takeEndWhile pat = s.sliceFrom (s.skipSuffixWhile pat)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
measurableSet_le : ∀ {α : Type u_1} {δ : Type u_4} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α]
  {mδ : MeasurableSpace δ} [inst_2 : PartialOrder α] [OrderClosedTopology α] [SecondCountableTopology α] {f g : δ → α},
  Measurable f → Measurable g → MeasurableSet {a | f a ≤ g a}
-- Mathlib.Order.CompleteLattice.Basic
Monotone.le_map_sSup : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] {s : Set α} {f : α → β},
  Monotone f → ⨆ a ∈ s, f a ≤ f (sSup s)
-- Mathlib.Topology.EMetricSpace.Defs
uniformSpace_edist : ∀ {α : Type u} [inst : PseudoEMetricSpace α], PseudoEMetricSpace.toUniformSpace = uniformSpaceOfEDist edist ⋯ ⋯ ⋯
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.Point.ext_iff : ∀ {R : Type r} {inst : CommRing R} {W' : WeierstrassCurve.Projective R} {x y : W'.Point}, x = y ↔ x.point = y.point
-- Lean.Meta.Match.MatchEqsExt
Lean.Meta.Match.MatchEqnsExtState.mk : Lean.PHashMap Lean.Name Lean.Meta.Match.MatchEqns → Lean.PHashSet Lean.Name → Lean.Meta.Match.MatchEqnsExtState
-- Mathlib.CategoryTheory.Limits.Over
CategoryTheory.Under.mono_iff_mono_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} [CategoryTheory.Limits.HasPullbacks C]
  {f g : CategoryTheory.Under X} (h : f ⟶ g),
  CategoryTheory.Mono h ↔ CategoryTheory.Mono (CategoryTheory.Under.Hom.right h)
-- Mathlib.Data.Nat.Fib.Basic
Nat.fib_le_fib_succ : ∀ {n : ℕ}, Nat.fib n ≤ Nat.fib (n + 1)
-- Lean.Environment
Lean.Kernel.Exception.appTypeMismatch.inj : ∀ {env : Lean.Kernel.Environment} {lctx : Lean.LocalContext} {app funType argType : Lean.Expr}
  {env_1 : Lean.Kernel.Environment} {lctx_1 : Lean.LocalContext} {app_1 funType_1 argType_1 : Lean.Expr},
  Lean.Kernel.Exception.appTypeMismatch env lctx app funType argType =
      Lean.Kernel.Exception.appTypeMismatch env_1 lctx_1 app_1 funType_1 argType_1 →
    env = env_1 ∧ lctx = lctx_1 ∧ app = app_1 ∧ funType = funType_1 ∧ argType = argType_1
-- Init.Data.UInt.Lemmas
UInt64.mul_neg : ∀ (a b : UInt64), a * -b = -(a * b)