mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- Eta-expanded form of `ContDiffAt.smul`

---

The scalar multiplication of two `C^n` functions at a point is `C^n` at this point.  -/
ContDiffAt.fun_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {x : E}
  {n : WithTop ℕ∞} {𝕜' : Type u_3} [inst_5 : NormedRing 𝕜'] [inst_6 : NormedAlgebra 𝕜 𝕜'] [inst_7 : Module 𝕜' F]
  [IsBoundedSMul 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {f : E → 𝕜'} {g : E → F},
  ContDiffAt 𝕜 n f x → ContDiffAt 𝕜 n g x → ContDiffAt 𝕜 n (fun i => f i • g i) x
-- Mathlib.Algebra.Group.AddChar
AddChar.inv_apply : ∀ {A : Type u_1} {M : Type u_2} [inst : AddCommGroup A] [inst_1 : CommMonoid M] (ψ : AddChar A M) (a : A),
  ψ⁻¹ a = ψ (-a)
-- Mathlib.LinearAlgebra.Projection
LinearMap.IsIdempotentElem.ker_eq_range_one_sub : ∀ {S : Type u_5} [inst : Semiring S] {E : Type u_7} [inst_1 : AddCommGroup E] [inst_2 : Module S E] {p : E →ₗ[S] E},
  IsIdempotentElem p → p.ker = (1 - p).range
-- Mathlib.RingTheory.Localization.Away.Basic
IsLocalization.Away.algebraMap_isUnit_iff : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (x : R)
  [IsLocalization.Away x S] {y : R}, IsUnit ((algebraMap R S) y) ↔ ∃ n, y ∣ x ^ n
-- Lean.Elab.Binders
Lean.Elab.Term.BinderView.id : Lean.Elab.Term.BinderView → Lean.Syntax
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.forget₂_map_restrictScalars : ∀ {R : Type u₁} {S : Type u₂} [inst : Ring R] [inst_1 : Ring S] (f : R →+* S) {M N : ModuleCat S} (g : M ⟶ N),
  (CategoryTheory.forget₂ (ModuleCat R) Ab).map ((ModuleCat.restrictScalars f).map g) =
    (CategoryTheory.forget₂ (ModuleCat S) Ab).map g
-- Mathlib.Topology.LocallyConstant.Algebra
/-- `LocallyConstant.const` as a linear map.  -/
LocallyConstant.constₗ : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      (R : Type u_6) →
        [inst_1 : Semiring R] → [inst_2 : AddCommMonoid Y] → [inst_3 : Module R Y] → Y →ₗ[R] LocallyConstant X Y
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
Set.Finite.measurableSet_biInter : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {f : β → Set α} {s : Set β},
  s.Finite → (∀ b ∈ s, MeasurableSet (f b)) → MeasurableSet (⋂ b ∈ s, f b)
-- Mathlib.CategoryTheory.Limits.Cones
/-- `mapCone` commutes with `postcompose`. In particular, for `F : J ⥤ C`, given a cone `c : Cone F`, a
natural transformation `α : F ⟶ G` and a functor `H : C ⥤ D`, we have two obvious ways of producing
a cone over `G ⋙ H`, and they are both isomorphic.
 -/
CategoryTheory.Functor.mapConePostcompose : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {D : Type u₄} →
          [inst_2 : CategoryTheory.Category.{v₄, u₄} D] →
            (H : CategoryTheory.Functor C D) →
              {F G : CategoryTheory.Functor J C} →
                {α : F ⟶ G} →
                  {c : CategoryTheory.Limits.Cone F} →
                    H.mapCone ((CategoryTheory.Limits.Cone.postcompose α).obj c) ≅
                      (CategoryTheory.Limits.Cone.postcompose (CategoryTheory.Functor.whiskerRight α H)).obj
                        (H.mapCone c)
-- Lean.Meta.Tactic.Grind.AC.Seq
/-- `p ++ s₁ ++ s == s₂`  -/
Lean.Grind.AC.SubseqResult.middle : Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Lean.Grind.AC.SubseqResult
-- Mathlib.Topology.Algebra.Group.Matrix
Matrix.SpecialLinearGroup.isInducing_mapGL : ∀ {n : Type u_1} {R : Type u_2} {S : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R]
  [inst_3 : TopologicalSpace R] [inst_4 : CommRing S] [inst_5 : TopologicalSpace S] [inst_6 : Algebra R S]
  [IsTopologicalRing S],
  Topology.IsInducing ⇑(algebraMap R S) → Topology.IsInducing ⇑(Matrix.SpecialLinearGroup.mapGL S)
-- Mathlib.Order.Heyting.Basic
BiheytingAlgebra.toCoheytingAlgebra : {α : Type u_4} → [self : BiheytingAlgebra α] → CoheytingAlgebra α
-- Lean.Meta.Basic
Lean.Meta.Diagnostics : Type
-- Lean.Data.Json.Basic
Lean.instHashableJsonNumber : Hashable Lean.JsonNumber
-- Mathlib.Data.ENNReal.Action
/-- A `MulAction` over `ℝ≥0∞` restricts to a `MulAction` over `ℝ≥0`.  -/
ENNReal.instMulActionNNReal : {M : Type u_1} → [MulAction ENNReal M] → MulAction NNReal M
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.vertexSet_not_nonempty_iff : ∀ {α : Type u_1} {β : Type u_2} {G : Graph α β}, ¬G.vertexSet.Nonempty ↔ G = ⊥
-- Mathlib.RingTheory.Congruence.Defs
RingCon.coe_pow : ∀ {R : Type u_1} [inst : Add R] [inst_1 : Monoid R] (c : RingCon R) (x : R) (n : ℕ), ↑(x ^ n) = ↑x ^ n
-- Mathlib.Analysis.Normed.Group.Basic
SeminormedAddCommGroup.induced.eq_1 : ∀ {𝓕 : Type u_1} (E : Type u_5) (F : Type u_6) [inst : FunLike 𝓕 E F] [inst_1 : AddCommGroup E]
  [inst_2 : SeminormedAddGroup F] [inst_3 : AddMonoidHomClass 𝓕 E F] (f : 𝓕),
  SeminormedAddCommGroup.induced E F f =
    { norm := fun a => ‖f a‖, toAddCommGroup := inst_1, dist := fun a a_1 => dist (f a) (f a_1), dist_self := ⋯,
      dist_comm := ⋯, dist_triangle := ⋯, edist := fun a a_1 => PseudoMetricSpace.edist (f a) (f a_1), edist_dist := ⋯,
      toUniformSpace :=
        { toTopologicalSpace := TopologicalSpace.induced (⇑f) PseudoMetricSpace.toUniformSpace.toTopologicalSpace,
          uniformity := Filter.comap (fun p => (f p.1, f p.2)) (uniformity F), symm := ⋯, comp := ⋯,
          nhds_eq_comap_uniformity := ⋯ },
      uniformity_dist := ⋯, toBornology := { cobounded := Filter.comap (⇑f) (Bornology.cobounded F), le_cofinite := ⋯ },
      cobounded_sets := ⋯, dist_eq := ⋯ }
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.any_eq_false_iff_forall_contains_get : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [LawfulBEq α]
  {p : α → β → Bool},
  m.WF → (m.any p = false ↔ ∀ (a : α) (h : m.contains a = true), p a (Std.DHashMap.Raw.Const.get m a h) = false)
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.add_le_of_le : ∀ {a b c : Cardinal.{u_1}}, Cardinal.aleph0 ≤ c → a ≤ c → b ≤ c → a + b ≤ c
-- Mathlib.Algebra.Group.Finsupp
Finsupp.instAddCommGroup : {ι : Type u_1} → {G : Type u_6} → [inst : AddCommGroup G] → AddCommGroup (ι →₀ G)
-- Init.Data.Float.Model.Format.Basic
/-- The number of bits in the mantissa, *including the implicit bit*.  -/
Float.Model.Format.mantissaBits : Float.Model.Format → ℕ
-- Mathlib.Algebra.CharP.Defs
CharP.intCast_eq_zero_iff : ∀ (R : Type u_1) [inst : AddGroupWithOne R] (p : ℕ) [CharP R p] (a : ℤ), ↑a = 0 ↔ ↑p ∣ a
-- Mathlib.Topology.Instances.Rat
Rat.isDenseEmbedding_coe_real : IsDenseEmbedding Rat.cast
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.mapPairId_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (x : CategoryTheory.Join C D),
  CategoryTheory.Join.mapPairId.inv.app x =
    match x with
    | CategoryTheory.Join.left x => CategoryTheory.CategoryStruct.id (CategoryTheory.Join.left x)
    | CategoryTheory.Join.right x => CategoryTheory.CategoryStruct.id (CategoryTheory.Join.right x)
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.sum_nat_eq_add_sum_succ : ∀ (f : ℕ → Cardinal.{u}), Cardinal.sum f = f 0 + Cardinal.sum fun i => f (i + 1)
-- Mathlib.Data.Num.Lemmas
Num.cast_to_nat : ∀ {α : Type u_1} [inst : AddMonoidWithOne α] (n : Num), ↑↑n = ↑n
-- Mathlib.Algebra.Star.SelfAdjoint
selfAdjoint.instInhabitedSubtypeMemAddSubgroup : {R : Type u_1} → [inst : AddGroup R] → [inst_1 : StarAddMonoid R] → Inhabited ↥(selfAdjoint R)
-- Mathlib.Algebra.Lie.Weights.Chain
LieModule.chainTop_neg : ∀ {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] [inst_8 : IsAddTorsionFree R] [inst_9 : IsDomain R]
  [inst_10 : Module.IsTorsionFree R M] [inst_11 : IsNoetherian R M] (α : L → R) (β : LieModule.Weight R L M),
  LieModule.chainTop (-α) β = LieModule.chainBot α β
-- Mathlib.Analysis.Normed.Module.HahnBanach
/-- **Hahn-Banach theorem** for continuous linear functions over `𝕜`
satisfying `IsRCLikeNormedField 𝕜`.  -/
exists_extension_norm_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] {E : Type u_2}
  [inst_2 : SeminormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] (p : Subspace 𝕜 E) (f : StrongDual 𝕜 ↥p),
  ∃ g, (∀ (x : ↥p), g ↑x = f x) ∧ ‖g‖ = ‖f‖
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
AffineSubspace.smul_vsub_vadd_mem' : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (self : AffineSubspace k P) (c : k) {p₁ p₂ p₃ : P},
  p₁ ∈ self.carrier → p₂ ∈ self.carrier → p₃ ∈ self.carrier → c • (p₁ -ᵥ p₂) +ᵥ p₃ ∈ self.carrier
-- Mathlib.RingTheory.Extension.Presentation.Core
Algebra.PreSubmersivePresentation.ofHasCoeffs_σ' : ∀ {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.PreSubmersivePresentation R S ι σ) (R₀ : Type u_5) [inst_3 : CommRing R₀]
  [inst_4 : Algebra R₀ R] [inst_5 : Algebra R₀ S] [inst_6 : IsScalarTower R₀ R S] [inst_7 : P.HasCoeffs R₀]
  (b : MvPolynomial ι R₀ ⧸ Ideal.span (Set.range (Algebra.Presentation.relationOfHasCoeffs R₀))),
  (P.ofHasCoeffs R₀).σ' b = Function.surjInv ⋯ b
-- Mathlib.Topology.Algebra.Group.Pointwise
compl_add_closure_zero_eq_iff : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G] {t : Set G},
  tᶜ + closure {0} = tᶜ ↔ t + closure {0} = t
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.Kernel.instAddCommMonoid : {α : Type u_1} →
  {β : Type u_2} → {mα : MeasurableSpace α} → {mβ : MeasurableSpace β} → AddCommMonoid (ProbabilityTheory.Kernel α β)
-- Mathlib.Algebra.Order.Ring.Synonym
OrderDual.instCommRing : {R : Type u_1} → [CommRing R] → CommRing Rᵒᵈ
-- Mathlib.Topology.Algebra.ConstMulAction
IsCompact.smul : ∀ {α : Type u_4} {β : Type u_5} [inst : SMul α β] [inst_1 : TopologicalSpace β] [ContinuousConstSMul α β] (a : α)
  {s : Set β}, IsCompact s → IsCompact (a • s)
-- Mathlib.AlgebraicGeometry.Morphisms.Flat
AlgebraicGeometry.Flat.iff_flat_stalkMap : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  AlgebraicGeometry.Flat f ↔ ∀ (x : ↥X), (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.stalkMap f x)).Flat
-- Mathlib.CategoryTheory.Monoidal.Functor
/-- **Alias** of `CategoryTheory.Functor.OplaxMonoidal.oplax_right_unitality`. -/
CategoryTheory.Functor.OplaxMonoidal.right_unitality : ∀ {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 D}
  (F : CategoryTheory.Functor C D) [self : F.OplaxMonoidal] (X : C),
  (CategoryTheory.MonoidalCategoryStruct.rightUnitor (F.obj X)).inv =
    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.OplaxMonoidal.δ F X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) (CategoryTheory.Functor.OplaxMonoidal.η F)))
-- Mathlib.Data.Finsupp.Single
Finsupp.single_ne_zero : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {a : α} {b : M}, (fun₀ | a => b) ≠ 0 ↔ b ≠ 0
-- Init.Data.List.Zip
List.zip_append : ∀ {α : Type u_1} {β : Type u_2} {l₁ r₁ : List α} {l₂ r₂ : List β},
  l₁.length = l₂.length → (l₁ ++ r₁).zip (l₂ ++ r₂) = l₁.zip l₂ ++ r₁.zip r₂
-- Init.Data.BitVec.Lemmas
/-- Interpreting the sign extension of `(x : BitVec w)` to width `v`
computes `x % 2^v` (where `%` is the balanced mod). See `toInt_signExtend` for a version stated
in terms of `toInt` instead of `toNat`.
 -/
BitVec.toInt_signExtend_eq_toNat_bmod : ∀ {w v : ℕ} (x : BitVec w), (BitVec.signExtend v x).toInt = (↑x.toNat).bmod (2 ^ min v w)
-- Mathlib.RingTheory.AdicCompletion.LocalRing
AdicCompletion.residueField_map_bijective_of_fg : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsLocalRing R] (fg : (IsLocalRing.maximalIdeal R).FG),
  Function.Bijective ⇑(IsLocalRing.ResidueField.map (algebraMap R (AdicCompletion (IsLocalRing.maximalIdeal R) R)))
-- Mathlib.Analysis.Complex.Exponential
Real.exp_le_two_add_div_two_sub : ∀ {x : ℝ}, 0 ≤ x → x < 2 → Real.exp x ≤ (2 + x) / (2 - x)
-- Lean.Server.InfoUtils
Lean.Elab.GoalsAtResult.mk.sizeOf_spec : ∀ (ctxInfo : Lean.Elab.ContextInfo) (tacticInfo : Lean.Elab.TacticInfo) (useAfter indented : Bool) (priority : ℕ),
  sizeOf
      { ctxInfo := ctxInfo, tacticInfo := tacticInfo, useAfter := useAfter, indented := indented,
        priority := priority } =
    1 + sizeOf ctxInfo + sizeOf tacticInfo + sizeOf useAfter + sizeOf indented + sizeOf priority
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRootMonic.liftPolyₗ_apply : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRootMonic S f) {T : Type u_1} [inst_3 : AddCommGroup T] [inst_4 : Module R T] (g : Polynomial R →ₗ[R] T)
  (x : S), (h.liftPolyₗ g) x = g (h.modByMonicHom x)
-- Mathlib.CategoryTheory.Triangulated.Functor
CategoryTheory.Functor.IsTriangulated.map_distinguished : ∀ {C : Type u_1} {D : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} C}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D} {inst_2 : CategoryTheory.HasShift C ℤ}
  {inst_3 : CategoryTheory.HasShift D ℤ} {F : CategoryTheory.Functor C D} {inst_4 : F.CommShift ℤ}
  {inst_5 : CategoryTheory.Limits.HasZeroObject C} {inst_6 : CategoryTheory.Limits.HasZeroObject D}
  {inst_7 : CategoryTheory.Preadditive C} {inst_8 : CategoryTheory.Preadditive D}
  {inst_9 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive}
  {inst_10 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive} {inst_11 : CategoryTheory.Pretriangulated C}
  {inst_12 : CategoryTheory.Pretriangulated D} [self : F.IsTriangulated],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
    F.mapTriangle.obj T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
-- Mathlib.CategoryTheory.MorphismProperty.CommaSites
CategoryTheory.MorphismProperty.toGrothendieck_comap_forget_eq_restrictedTopology : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.MorphismProperty C} {S : C}
  [P.IsStableUnderComposition] (K : CategoryTheory.Precoverage C) [K.HasIsos] [K.IsStableUnderBaseChange]
  [K.IsStableUnderComposition] [K.HasPullbacks],
  K ≤ P.precoverage →
    (CategoryTheory.Precoverage.comap
          ((CategoryTheory.MorphismProperty.Over.forget P ⊤ S).comp (CategoryTheory.Over.forget S)) K).toGrothendieck =
      (CategoryTheory.MorphismProperty.Over.forget P ⊤ S).restrictedTopology (K.toGrothendieck.over S)
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isBigOWith_of_le : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E} {g : α → F} (l : Filter α),
  (∀ (x : α), ‖f x‖ ≤ ‖g x‖) → Asymptotics.IsBigOWith 1 l f g
-- Mathlib.Combinatorics.Matroid.Circuit
/-- For an element `e` of a base `B`, the complement of the closure of `B \ {e}` is a cocircuit.  -/
Matroid.IsBase.compl_closure_sdiff_singleton_isCocircuit : ∀ {α : Type u_1} {M : Matroid α} {e : α} {B : Set α}, M.IsBase B → e ∈ B → M.IsCocircuit (M.E \ M.closure (B \ {e}))
-- Mathlib.Topology.EMetricSpace.BoundedVariation
/-- If a function has bounded variation, then the variation on closed semi-infinite
intervals tends to `0` at `+∞`.  -/
BoundedVariationOn.tendsto_eVariationOn_Ici_zero : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] {f : α → E} {s : Set α},
  BoundedVariationOn f s →
    Filter.Tendsto (fun y => eVariationOn f (s ∩ Set.Ici y)) (Filter.principal s ⊓ Filter.atTop) (nhds 0)
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
/-- The proposed colimit cocone is a colimit in `MonCat`.  -/
MonCat.FilteredColimits.colimitCoconeIsColimit : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J MonCat) →
      [inst_1 : CategoryTheory.IsFiltered J] → CategoryTheory.Limits.IsColimit (MonCat.FilteredColimits.colimitCocone F)
-- Mathlib.Topology.Algebra.UniformMulAction
UniformSpace.Completion.instSMul : (M : Type v) → (X : Type x) → [inst : UniformSpace X] → [SMul M X] → SMul M (UniformSpace.Completion X)
-- Mathlib.Topology.Algebra.Star
instContinuousStarProd : ∀ {R : Type u_1} {S : Type u_2} [inst : Star R] [inst_1 : Star S] [inst_2 : TopologicalSpace R]
  [inst_3 : TopologicalSpace S] [ContinuousStar R] [ContinuousStar S], ContinuousStar (R × S)
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.isCoprime_Y_Z : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S : FermatLastTheoremForThreeGen.Solution✝ hζ)
  [inst_1 : NumberField K] [inst_2 : IsCyclotomicExtension {3} ℚ K],
  IsCoprime (FermatLastTheoremForThreeGen.Solution.Y✝ S) (FermatLastTheoremForThreeGen.Solution.Z✝ S)
-- Mathlib.CategoryTheory.ConcreteCategory.Basic
CategoryTheory.NatTrans.naturality_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {FD : outParam (D → D → Type u_2)} {CD : outParam (D → Type w)}
  [inst_2 : outParam ((X Y : D) → FunLike (FD X Y) (CD X) (CD Y))] [inst_3 : CategoryTheory.ConcreteCategory D FD]
  {F G : CategoryTheory.Functor C D} (φ : F ⟶ G) {X Y : C} (f : X ⟶ Y) (x : CategoryTheory.ToType (F.obj X)),
  (CategoryTheory.ConcreteCategory.hom (φ.app Y)) ((CategoryTheory.ConcreteCategory.hom (F.map f)) x) =
    (CategoryTheory.ConcreteCategory.hom (G.map f)) ((CategoryTheory.ConcreteCategory.hom (φ.app X)) x)
-- Mathlib.Algebra.Category.ModuleCat.Abelian
ModuleCat.forget_reflectsLimits : ∀ {R : Type u} [inst : Ring R], CategoryTheory.Limits.ReflectsLimits (CategoryTheory.forget (ModuleCat R))
-- Mathlib.Algebra.Order.Group.Synonym
toDual_sub : ∀ {α : Type u_1} [inst : Sub α] (a b : α), OrderDual.toDual (a - b) = OrderDual.toDual a - OrderDual.toDual b
-- Mathlib.CategoryTheory.Functor.Derived.LeftDerived
CategoryTheory.Functor.hasLeftDerivedFunctor_iff : ∀ {C : Type u_1} {D : Type u_3} {H : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} D] [inst_2 : CategoryTheory.Category.{v_5, u_2} H]
  (F : CategoryTheory.Functor C H) (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C)
  [L.IsLocalization W], F.HasLeftDerivedFunctor W ↔ L.HasRightKanExtension F
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.HomotopyWith.extendProp : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ : C(X, Y)}
  {P : C(X, Y) → Prop} (F : f₀.HomotopyWith f₁ P) (t : ℝ), P (F.extend t)
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.mem_support : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] (x : HahnSeries Γ R) (a : Γ),
  a ∈ x.support ↔ x.coeff a ≠ 0
-- Mathlib.Algebra.Order.AbsoluteValue.Euclidean
/-- `abs : ℤ → ℤ` is a Euclidean absolute value  -/
AbsoluteValue.abs_isEuclidean : AbsoluteValue.abs.IsEuclidean
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.stepRet.eq_3 : ∀ (x ns : List ℕ) (k : Turing.ToPartrec.Cont),
  Turing.ToPartrec.stepRet (Turing.ToPartrec.Cont.cons₂ ns k) x = Turing.ToPartrec.stepRet k (ns.headI :: x)
-- Mathlib.CategoryTheory.Limits.VanKampen
CategoryTheory.isUniversalColimit_extendCofan : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {n : ℕ} (f : Fin (n + 1) → C)
  {c₁ : CategoryTheory.Limits.Cofan fun i => f i.succ} {c₂ : CategoryTheory.Limits.BinaryCofan (f 0) c₁.pt},
  CategoryTheory.IsUniversalColimit c₁ →
    CategoryTheory.IsUniversalColimit c₂ →
      ∀ [∀ {Z : C} (i : Z ⟶ c₂.pt), CategoryTheory.Limits.HasPullback c₂.inr i],
        CategoryTheory.IsUniversalColimit (CategoryTheory.extendCofan c₁ c₂)
-- Mathlib.Algebra.Module.Submodule.LinearMap
LinearMap.restrict_commute : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {f g : M →ₗ[R] M},
  Commute f g →
    ∀ {p : Submodule R M} (hf : Set.MapsTo ⇑f ↑p ↑p) (hg : Set.MapsTo ⇑g ↑p ↑p), Commute (f.restrict hf) (g.restrict hg)
-- Mathlib.Topology.Algebra.Ring.Real
Real.uniformContinuous_add : UniformContinuous fun p => p.1 + p.2
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.size_insertMany_emptyWithCapacity_list : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)},
  List.Pairwise (fun a b => (a.1 == b.1) = false) l →
    (↑↑(Std.DHashMap.Internal.Raw₀.Const.insertMany Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)).size = l.length
-- Mathlib.Topology.Algebra.ConstMulAction
Homeomorph.smulOfNeZero_apply : ∀ {α : Type u_2} {G₀ : Type u_4} [inst : TopologicalSpace α] [inst_1 : GroupWithZero G₀] [inst_2 : MulAction G₀ α]
  [inst_3 : ContinuousConstSMul G₀ α] (c : G₀) (hc : c ≠ 0), ⇑(Homeomorph.smulOfNeZero c hc) = fun x => c • x
-- Mathlib.Algebra.Star.Unitary
IsUnit.mem_unitary_iff_star_mul_self : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] {u : R}, IsUnit u → (u ∈ unitary R ↔ star u * u = 1)
-- Mathlib.Data.Set.Card
Set.toENat_cardinalMk : ∀ {α : Type u_1} (s : Set α), Cardinal.toENat (Cardinal.mk ↑s) = s.encard
-- Mathlib.Probability.CentralLimitTheorem
/-- **Central Limit Theorem:** Given a sequence of random variables `X : ℕ → Ω → ℝ` that are
independent, identically distributed, centered and with variance `1` and a random variable
`Y : Ω' → ℝ` following `gaussianReal 0 1`, the sequence
`n ↦ (√n)⁻¹ * ∑ k ∈ Finset.range n, X k` converges to `Y` in distribution.  -/
ProbabilityTheory.tendstoInDistribution_inv_sqrt_mul_sum : ∀ {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {P : MeasureTheory.Measure Ω}
  {P' : MeasureTheory.Measure Ω'} {X : ℕ → Ω → ℝ} {Y : Ω' → ℝ} [inst : MeasureTheory.IsProbabilityMeasure P]
  [inst_1 : MeasureTheory.IsProbabilityMeasure P'],
  ProbabilityTheory.HasLaw Y (ProbabilityTheory.gaussianReal 0 1) P' →
    ∫ (x : Ω), X 0 x ∂P = 0 →
      ∫ (x : Ω), (X 0 ^ 2) x ∂P = 1 →
        ProbabilityTheory.iIndepFun X P →
          (∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X i) (X 0) P P) →
            MeasureTheory.TendstoInDistribution (fun n ω => (√↑n)⁻¹ * ∑ k ∈ Finset.range n, X k ω) Filter.atTop Y
              (fun x => P) P'
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
/-- The class of morphisms that are of the form `i ≫ p` with `W₁ i` and `W₂ p`.  -/
CategoryTheory.MorphismProperty.comp : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    CategoryTheory.MorphismProperty C → CategoryTheory.MorphismProperty C → CategoryTheory.MorphismProperty C
-- Mathlib.Analysis.RCLike.Basic
RCLike.nonneg_iff_exists_ofReal : ∀ {K : Type u_1} [inst : RCLike K] {z : K}, 0 ≤ z ↔ ∃ x ≥ 0, ↑x = z
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.homMk_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : CategoryTheory.AddGrp C} (f : A.X ⟶ B.X) [inst_2 : CategoryTheory.IsAddMonHom f],
  (CategoryTheory.AddGrp.homMk f).hom.hom = f
-- Lean.Elab.MutualInductive
/-- Checks the universe constraints for each constructor.  -/
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.checkResultingUniverses : Array Lean.Elab.Command.InductiveView →
  Array Lean.Elab.Command.InductiveElabStep2 → ℕ → List Lean.InductiveType → Lean.Elab.TermElabM Unit