mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
aux' : 2 * n.succ = 2 * n + 2
⊢ 1 / 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n.succ) =
    (2 * ↑n + 1) / (2 * ↑n + 2) * (1 / 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n))

Tactic:
aux',

Goal state after:
z : ℂ
hz : z ≠ 0
n : ℕ
A : ℂ := ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)
B : ℂ := ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)
C : ℝ := ∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)
hn : Complex.sin (↑π * z) = ↑π * z * A * B / ↑C
aux' : 2 * n.succ = 2 * n + 2
⊢ 1 / 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n + 2) =
    (2 * ↑n + 1) / (2 * ↑n + 2) * (1 / 2 * ∫ (x : ℝ) in 0..π, sin x ^ (2 * n))
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: f : ℝ → ℝ
x : ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
hx' : x ≤ 1
n : ℕ
⊢ f 1 + log ↑(n + 1 - 1)! + x * log ↑(n + 1) = f 1 + x * log (↑n + 1) - x * log ↑n + (x * log ↑n + log ↑n !)

Tactic:
Nat.add_sub_cancel,

Goal state after:
f : ℝ → ℝ
x : ℝ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
hx' : x ≤ 1
n : ℕ
⊢ f 1 + log ↑n ! + x * log ↑(n + 1) = f 1 + x * log (↑n + 1) - x * log ↑n + (x * log ↑n + log ↑n !)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: case refine_1
f : ℝ → ℝ
x : ℝ
n : ℕ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
hn : n ≠ 0
⊢ f 1 + (x * log ↑n + log ↑n !) = f 1 + log ↑(n + 1 - 1)! + x * log (↑(n + 1) - 1)

pp: case refine_1
f : ℝ → ℝ
x : ℝ
n : ℕ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
hn : n ≠ 0
⊢ n + 1 ≠ 0

Tactic:
Nat.add_sub_cancel,

Goal state after:
case refine_1
f : ℝ → ℝ
x : ℝ
n : ℕ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
hn : n ≠ 0
⊢ f 1 + (x * log ↑n + log ↑n !) = f 1 + log ↑n ! + x * log (↑(n + 1) - 1)

case refine_1
f : ℝ → ℝ
x : ℝ
n : ℕ
hf_conv : ConvexOn ℝ (Ioi 0) f
hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y
hx : 0 < x
hn : n ≠ 0
⊢ n + 1 ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: case e'_3
x : ℝ
n : ℕ
⊢ π * x * ∏ j ∈ Finset.range n, (1 - x ^ 2 / (↑j + 1) ^ 2) =
    (↑(π * x) * ∏ j ∈ Finset.range n, (1 - ↑x ^ 2 / (↑j + 1) ^ 2)).re

Tactic:
Complex.re_ofReal_mul

Goal state after:
case e'_3
x : ℝ
n : ℕ
⊢ π * x * ∏ j ∈ Finset.range n, (1 - x ^ 2 / (↑j + 1) ^ 2) =
    π * x * (∏ j ∈ Finset.range n, (1 - ↑x ^ 2 / (↑j + 1) ^ 2)).re
Module: Mathlib.Topology.Algebra.AsymptoticCone

Goal state before:
pp: case e_m
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Field k
inst✝⁴ : LinearOrder k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AddTorsor V P
inst✝ : TopologicalSpace V
u v✝ : V
p : P
v : V
⊢ ((fun b ↦ u +ᵥ b) ∘ fun x ↦ x +ᵥ p) v = v +ᵥ u +ᵥ p

Tactic:
exact vadd_comm u v p

Goal state after:
Module: Mathlib.Topology.Algebra.AsymptoticCone

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : Field k
inst✝⁴ : LinearOrder k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AddTorsor V P
inst✝ : TopologicalSpace V
α : Type u_4
l : Filter α
f : α → P
v u : V
hf : Tendsto f l (asymptoticNhds k P v)
⊢ Tendsto (fun x ↦ u +ᵥ f x) l (asymptoticNhds k P v)

Tactic:
by
  rw [← vadd_asymptoticNhds u, ← Filter.map_vadd]
  exact tendsto_map.comp hf

Goal state after:
Module: Mathlib.Analysis.Meromorphic.LogDeriv

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
U : Set 𝕜
ι : Type u_3
F : ι → 𝕜 → 𝕜'
d : ι → ℤ
hd : (support d).Finite
h : ∀ (i : ι), MeromorphicOn (F i) U
h' : ∀ (i : ι), ∀ x ∈ U, meromorphicOrderAt (F i) x ≠ ⊤
⊢ logDeriv (∏ᶠ (i : ι), F i ^ d i) =ᶠ[codiscreteWithin U] fun z ↦ ∑ᶠ (i : ι), d i • logDeriv (F i) z

Tactic:
have hA : ∀ᶠ y in codiscreteWithin U, ∀ i ∈ hd.toFinset, AnalyticAt 𝕜 (F i) y :=
    (eventually_all_finset hd.toFinset).2 fun i _ ↦ (h i).analyticAt_mem_codiscreteWithin
  have hN : ∀ᶠ y in codiscreteWithin U, ∀ i ∈ hd.toFinset, F i y ≠ 0 :=
    (eventually_all_finset hd.toFinset).2 fun i _ ↦ (h i).eventually_codiscreteWithin_apply_ne_zero
      (h' i)
  filter_upwards [hA, hN] with y h₁y h₂y
  have h₀ : ∏ᶠ i, F i ^ d i = ∏ i ∈ hd.toFinset, F i ^ d i :=
    finprod_eq_prod_of_mulSupport_subset _ <| by simp +contextual [Set.subset_def, not_imp_not]
  have hsub : support (fun i ↦ d i • logDeriv (F i) y) ⊆ hd.toFinset := by
    simp +contextual [-support_mul, -mul_eq_zero, Set.subset_def, not_imp_not]
  calc logDeriv (∏ᶠ i, F i ^ d i) y
      = logDeriv (fun z ↦ ∏ i ∈ hd.toFinset, (F i ^ d i) z) y := by rw [h₀, Finset.prod_fn]
    _ = ∑ i ∈ hd.toFinset, logDeriv (F i ^ d i) y :=
        logDeriv_prod (fun i hi ↦ zpow_ne_zero _ (h₂y i hi))
          (fun i hi ↦ ((h₁y i hi).zpow (h₂y i hi)).differentiableAt)
    _ = ∑ i ∈ hd.toFinset, d i • logDeriv (F i) y := by
        congr! with i hi
        rw [zsmul_eq_mul, Pi.pow_def]
        exact logDeriv_fun_zpow (h₁y i hi).differentiableAt (d i)
    _ = ∑ᶠ i, d i • logDeriv (F i) y := (finsum_eq_sum_of_support_subset _ hsub).symm

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.AsymptoticCone

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
hs : Bornology.IsBounded s
⊢ asymptoticCone ℝ s ⊆ {0}

Tactic:
intro v h
  by_contra! hv
  exact h (asymptoticNhds_le_cobounded hv hs)

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Ceva

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : CommRing k
inst✝³ : NoZeroDivisors k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
t : Triangle k P
r : Fin 3 → k
p' : P
hp' : ∀ (i : Fin 3), p' ∈ line[k, t.points i, (AffineMap.lineMap (t.points (i + 1)) (t.points (i + 2))) (r i)]
⊢ ∏ i, r i = ∏ i, (1 - r i)

Tactic:
by
  rcases subsingleton_or_nontrivial k
  · exact Subsingleton.elim _ _
  let w : ↑(Set.univ : Set (Fin 3)) → Fin 3 → k :=
    fun i ↦ Finset.affineCombinationLineMapWeights (i + 1) (i + 2) (r i)
  have hw : ∀ i, ∑ j, w i j = 1 := by simp [w]
  have hp'w : ∀ i : ↑(Set.univ : Set (Fin 3)),
      p' ∈ line[k, t.points i, Finset.univ.affineCombination k t.points (w i)] := by
    simpa [w] using hp'
  obtain ⟨w', hw', rfl, h⟩ :=
    t.independent.exists_affineCombination_eq_smul_eq_of_fintype (by simp) hw hp'w
  have h' : ∀ i : Fin 3, ∃ c : k, ∀ j ≠ i, c * w ⟨i, by simp⟩ j = w' j := by
    intro i
    obtain ⟨c, hc⟩ := h ⟨i, by simp⟩
    refine ⟨c, fun j hj ↦ ?_⟩
    simpa [hj] using hc j
  simp only [Fin.isValue, w] at h'
  let c : Fin 3 → k := fun i ↦ (h' i).choose
  have hc (i : Fin 3) : ∀ j : Fin 3, j ≠ i →
    c i * Finset.affineCombinationLineMapWeights (i + 1) (i + 2) (r i) j = w' j :=
      (h' i).choose_spec
  have hc1 (i : Fin 3) : c i * (1 - r i) = w' (i + 1) := by
    rw [← hc i (i + 1) (by simp)]
    simp
  have hc2 (i : Fin 3) : c i * r i = w' (i + 2) := by
    rw [← hc i (i + 2) (by simp)]
    simp
  have hcr : (∏ i, c i) * ∏ i, r i = (∏ i, c i) * ∏ i, (1 - r i) := by
    simp_rw [← Finset.prod_mul_distrib, Finset.prod_congr rfl (fun _ _ ↦ hc1 _),
      Finset.prod_congr rfl (fun _ _ ↦ hc2 _)]
    suffices ∏ i, (w' ∘ Equiv.addRight 2) i = ∏ i, (w' ∘ Equiv.addRight 1) i by
      simpa using this
    simp_rw [Finset.prod_comp_equiv]
    simp
  by_cases hc : ∏ i, c i = 0
  · rw [Finset.prod_eq_zero_iff] at hc
    obtain ⟨i, -, hi⟩ := hc
    have hw'i1 : w' (i + 1) = 0 := by simpa [hi] using (hc1 i).symm
    have hw'i2 : w' (i + 2) = 0 := by simpa [hi] using (hc2 i).symm
    have hw'i0 : w' i = 1 := by
      rw [← hw', Fin.sum_univ_three]
      fin_cases i <;> grind
    have hi1 : c (i + 1) * r (i + 1) = 1 := by simpa [add_assoc, hw'i0] using hc2 (i + 1)
    have hi1' : c (i + 1) * (1 - r (i + 1)) = 0 := by
     simpa [add_assoc, hw'i2] using hc1 (i + 1)
    have hci1 : c (i + 1) = 1 := by
      suffices c (i + 1) * (r (i + 1) + (1 - r (i + 1))) = 1 + 0 by simpa using this
      rw [mul_add, hi1, hi1']
    have hri1 : r (i + 1) = 1 := by simpa [hci1] using hi1
    have hi2 : c (i + 2) * (1 - r (i + 2)) = 1 := by simpa [add_assoc, hw'i0] using hc1 (i + 2)
    have hi2' : c (i + 2) * r (i + 2) = 0 := by simpa [add_assoc, hw'i1] using hc2 (i + 2)
    have hci2 : c (i + 2) = 1 := by
      suffices c (i + 2) * (r (i + 2) + (1 - r (i + 2))) = 0 + 1 by simpa using this
      rw [mul_add, hi2, hi2']
    have hri2 : r (i + 2) = 0 := by simpa [hci2] using hi2'
    rw [Finset.prod_eq_zero (by simp) hri2,
      Finset.prod_eq_zero (i := i + 1) (by simp) (by simp [hri1])]
  · exact mul_left_cancel₀ hc hcr

Goal state after:
Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur

Goal state before:
pp: F : Type u_1
inst✝² : NormedRing F
inst✝¹ : NormedAlgebra ℝ F
inst✝ : NormOneClass F
x : F
c : ℝ
hc₀ : 0 < c
hbd : ∀ (r : ℝ), c ≤ ‖x - (algebraMap ℝ F) r‖
this : Tendsto (fun y ↦ ‖y.1‖ * c) (cobounded ℝ ×ˢ ⊤) atTop
y : ℝ × ℝ
hy : y ∈ {0}ᶜ ×ˢ Set.univ
⊢ ‖y.1‖ * c ≤ ‖y.1‖ * ‖x - (algebraMap ℝ F) (y.1⁻¹ * y.2)‖

Tactic:
gcongr; exact hbd _

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
⊢ 0 ≤ c * f x

Tactic:
rcases (f_nonneg x).eq_or_lt' with hx | hx
  · simp [hx]
  · change 0 < f x at hx
    have hc : 0 ≤ c := by
      specialize f_mul x 1
      rw [mul_one, show c * f x * f 1 = c * f 1 * f x by ring, le_mul_iff_one_le_left hx] at f_mul
      replace f_nonneg : 0 ≤ f 1 := f_nonneg 1
      rcases f_nonneg.eq_or_lt' with h1 | h1
      · linarith [show (1 : ℝ) ≤ 0 by simpa [h1] using f_mul]
      · rw [← div_le_iff₀ h1] at f_mul
        linarith [one_div_pos.mpr h1]
    positivity

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.InvariantExtension

Goal state before:
pp: K : Type u_1
inst✝² : NormedField K
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
h_fin : FiniteDimensional K L
hu : IsUltrametricDist K
σ : L ≃ₐ[K] L
⊢ IsNonarchimedean ⇑(algNormOfAlgEquiv σ)

Tactic:
by
  intro x y
  simp only [algNormOfAlgEquiv_apply, map_add σ]
  exact (Classical.choose_spec (exists_nonarchimedean_pow_mul_seminorm_of_finiteDimensional
    h_fin hu.isNonarchimedean_norm)).2.2 _ _

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful

Goal state before:
pp: F : Type u_1
α : Type u_2
inst✝³ : Ring α
inst✝² : FunLike F α ℝ
inst✝¹ : RingSeminormClass F α ℝ
β : Type u_3
inst✝ : Ring β
nα : F
nβ : β → ℝ
hβ : IsPowMul nβ
f : α →+* β
x : α
C : ℝ
hC0 : 0 < C
hC : ∀ (x : α), nβ (f x) ≤ C * nα x
hlim : Tendsto (fun n ↦ C ^ (1 / ↑n) * nα x) atTop (𝓝 (nα x))
n : ℕ
hn : 1 ≤ n
hn0 : ↑n ≠ 0
⊢ C ^ ((↑n)⁻¹ * ↑n) = C

Tactic:
inv_mul_cancel₀ hn0,

Goal state after:
F : Type u_1
α : Type u_2
inst✝³ : Ring α
inst✝² : FunLike F α ℝ
inst✝¹ : RingSeminormClass F α ℝ
β : Type u_3
inst✝ : Ring β
nα : F
nβ : β → ℝ
hβ : IsPowMul nβ
f : α →+* β
x : α
C : ℝ
hC0 : 0 < C
hC : ∀ (x : α), nβ (f x) ≤ C * nα x
hlim : Tendsto (fun n ↦ C ^ (1 / ↑n) * nα x) atTop (𝓝 (nα x))
n : ℕ
hn : 1 ≤ n
hn0 : ↑n ≠ 0
⊢ C ^ 1 = C
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : μ x ≠ 0
L : ℝ := ⨅ n, μ (x ^ ↑n) ^ (1 / ↑↑n)
hL0 : 0 ≤ L
ε : ℝ
hε : ε > 0
m1 : ℕ+
hm1 : μ (x ^ ↑m1) ^ (1 / ↑↑m1) < (⨅ n, μ (x ^ ↑n) ^ (1 / ↑↑n)) + ε / 2
m2 : ℕ
hm2 : ∀ n ≥ m2, (L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n)) * (μ x ^ (n % ↑m1)) ^ (1 / ↑n) - 1 ≤ ε / (2 * (L + ε / 2))
n : ℕ
hn : n ≥ max (↑m1) m2
hn0 : 0 < n
⊢ L ≤ smoothingSeminormSeq μ x n

Tactic:
← PNat.mk_coe n hn0

Goal state after:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
x : R
hx : μ x ≠ 0
L : ℝ := ⨅ n, μ (x ^ ↑n) ^ (1 / ↑↑n)
hL0 : 0 ≤ L
ε : ℝ
hε : ε > 0
m1 : ℕ+
hm1 : μ (x ^ ↑m1) ^ (1 / ↑↑m1) < (⨅ n, μ (x ^ ↑n) ^ (1 / ↑↑n)) + ε / 2
m2 : ℕ
hm2 : ∀ n ≥ m2, (L + ε / 2) ^ (-(↑(n % ↑m1) / ↑n)) * (μ x ^ (n % ↑m1)) ^ (1 / ↑n) - 1 ≤ ε / (2 * (L + ε / 2))
n : ℕ
hn : n ≥ max (↑m1) m2
hn0 : 0 < n
⊢ L ≤ smoothingSeminormSeq μ x ↑⟨n, hn0⟩
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
⊢ seminormFromConst' c f x ≤ f x

Tactic:
apply le_of_tendsto (tendsto_seminormFromConst_seq_atTop hf1 hc hpm x)

Goal state after:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
⊢ ∀ᶠ (c_1 : ℕ) in atTop, seminormFromConst_seq c f x c_1 ≤ f x
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
x : R
hx : ∀ (y : R), f (x * y) = f x * f y
⊢ Tendsto (seminormFromConst_seq c f x) atTop (𝓝 (f x))

Tactic:
by
    have hseq : seminormFromConst_seq c f x = fun _n ↦ f x := by
      ext n
      by_cases hn : n = 0
      · simp only [seminormFromConst_seq, hn, pow_zero, mul_one, div_one]
      · simp only [seminormFromConst_seq, hx (c ^ n), hpm _ (Nat.one_le_iff_ne_zero.mpr hn),
          mul_div_assoc, div_self (pow_ne_zero n hc), mul_one]
    rw [hseq]
    exact tendsto_const_nhds

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromConst

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
⊢ Tendsto (seminormFromConst_seq c f c) atTop (𝓝 (f c))

Tactic:
have hseq : seminormFromConst_seq c f c = fun _n ↦ f c := by
      ext n
      simp only [seminormFromConst_seq]
      rw [mul_comm, ← pow_succ, hpm _ le_add_self, pow_succ, mul_comm, mul_div_assoc,
        div_self (pow_ne_zero n hc), mul_one]

Goal state after:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf1 : f 1 ≤ 1
hc : f c ≠ 0
hpm : IsPowMul ⇑f
hseq : seminormFromConst_seq c f c = fun _n ↦ f c
⊢ Tendsto (seminormFromConst_seq c f c) atTop (𝓝 (f c))
Module: Mathlib.FieldTheory.Minpoly.IsConjRoot

Goal state before:
pp: K : Type u_2
S : Type u_4
inst✝³ : CommRing S
inst✝² : Field K
inst✝¹ : Algebra K S
inst✝ : IsDomain S
x y : S
h : IsIntegral K x
⊢ IsConjRoot K x y ↔ y ∈ (minpoly K x).aroots S

Tactic:
rw [Polynomial.mem_aroots, isConjRoot_iff_aeval_eq_zero h]

Goal state after:
K : Type u_2
S : Type u_4
inst✝³ : CommRing S
inst✝² : Field K
inst✝¹ : Algebra K S
inst✝ : IsDomain S
x y : S
h : IsIntegral K x
⊢ (Polynomial.aeval y) (minpoly K x) = 0 ↔ minpoly K x ≠ 0 ∧ (Polynomial.aeval y) (minpoly K x) = 0
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: R : Type u_1
inst✝¹ : SeminormedRing R
inst✝ : Nontrivial R
r : R
⊢ spectralValue (X - C r) = ‖r‖

Tactic:
spectralValue

Goal state after:
R : Type u_1
inst✝¹ : SeminormedRing R
inst✝ : Nontrivial R
r : R
⊢ iSup (spectralValueTerms (X - C r)) = ‖r‖
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: R : Type u_1
inst✝¹ : SeminormedRing R
inst✝ : Nontrivial R
n : ℕ
⊢ spectralValue (X ^ n) = 0

Tactic:
spectralValue

Goal state after:
R : Type u_1
inst✝¹ : SeminormedRing R
inst✝ : Nontrivial R
n : ℕ
⊢ iSup (spectralValueTerms (X ^ n)) = 0
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: R : Type u_1
inst✝ : NormedDivisionRing R
P : R[X]
hP : P.Monic
⊢ spectralValue P ≤ 1 ↔ ∀ (n : ℕ), ‖P.coeff n‖ ≤ 1

Tactic:
spectralValue

Goal state after:
R : Type u_1
inst✝ : NormedDivisionRing R
P : R[X]
hP : P.Monic
⊢ iSup (spectralValueTerms P) ≤ 1 ↔ ∀ (n : ℕ), ‖P.coeff n‖ ≤ 1
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: case refine_1.inr.inl
R : Type u_1
inst✝ : NormedDivisionRing R
P : R[X]
hP : P.Monic
h : iSup (spectralValueTerms P) ≤ 1
n : ℕ
hPn : P.natDegree = n
⊢ ‖P.coeff n‖ ≤ 1

Tactic:
← hPn,

Goal state after:
case refine_1.inr.inl
R : Type u_1
inst✝ : NormedDivisionRing R
P : R[X]
hP : P.Monic
h : iSup (spectralValueTerms P) ≤ 1
n : ℕ
hPn : P.natDegree = n
⊢ ‖P.coeff P.natDegree‖ ≤ 1
Module: Mathlib.Analysis.Normed.Field.Dense

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁶ : Field K
inst✝⁵ : NontriviallyNormedField L
inst✝⁴ : CompleteSpace L
inst✝³ : CharZero L
inst✝² : IsUltrametricDist L
inst✝¹ : Algebra K L
hi : DenseRange ⇑(algebraMap K L)
inst✝ : IsAlgClosed K
f : L[X]
fmon : f.Monic
firr : Irreducible f
fnatdeg0 : f.natDegree ≠ 0
F : Type u_2 := f.SplittingField
this✝ : NormedField F := spectralNorm.normedField L F
this : NormedAlgebra L F := spectralNorm.normedAlgebra L F
a : f.SplittingField := rootOfSplits ⋯ ⋯
fa0 : (aeval a) f = 0
S : Finset F := {x ∈ (f.rootSet F).toFinset | x ≠ a}
δ : ℝ := if hS : S.Nonempty then (Finset.image (fun x ↦ ‖a - x‖) S).min' ⋯ else 1
a' : F
⊢ IsConjRoot L a a' → a ≠ a' → δ ≤ ‖a - a'‖

Tactic:
conj

Goal state after:
K : Type u_1
L : Type u_2
inst✝⁶ : Field K
inst✝⁵ : NontriviallyNormedField L
inst✝⁴ : CompleteSpace L
inst✝³ : CharZero L
inst✝² : IsUltrametricDist L
inst✝¹ : Algebra K L
hi : DenseRange ⇑(algebraMap K L)
inst✝ : IsAlgClosed K
f : L[X]
fmon : f.Monic
firr : Irreducible f
fnatdeg0 : f.natDegree ≠ 0
F : Type u_2 := f.SplittingField
this✝ : NormedField F := spectralNorm.normedField L F
this : NormedAlgebra L F := spectralNorm.normedAlgebra L F
a : f.SplittingField := rootOfSplits ⋯ ⋯
fa0 : (aeval a) f = 0
S : Finset F := {x ∈ (f.rootSet F).toFinset | x ≠ a}
δ : ℝ := if hS : S.Nonempty then (Finset.image (fun x ↦ ‖a - x‖) S).min' ⋯ else 1
a' : F
conj : IsConjRoot L a a'
⊢ a ≠ a' → δ ≤ ‖a - a'‖
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ_lim : Tendsto ((fun n ↦ ↑(s n) / ↑n) ∘ ψ) atTop (𝓝 0)
c : ℝ
⊢ c ∈ lowerBounds {a | ∀ᶠ (n : ℝ) in map (fun n ↦ μ x ^ (↑(s (ψ n)) * (1 / ↑(ψ n)))) atTop, n ≤ a} → c ≤ 1

Tactic:
hc_bd

Goal state after:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
ψ : ℕ → ℕ
hψ_lim : Tendsto ((fun n ↦ ↑(s n) / ↑n) ∘ ψ) atTop (𝓝 0)
c : ℝ
hc_bd : c ∈ lowerBounds {a | ∀ᶠ (n : ℝ) in map (fun n ↦ μ x ^ (↑(s (ψ n)) * (1 / ↑(ψ n)))) atTop, n ≤ a}
⊢ c ≤ 1
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
s : ℕ → ℕ
hs_le : ∀ (n : ℕ), s n ≤ n
x : R
a : ℝ
a_in : a ∈ Set.Icc 0 1
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun n ↦ ↑(s n) / ↑n) ∘ ψ) atTop (𝓝 a)
⊢ limsup (fun n ↦ μ (x ^ s (ψ n)) ^ (1 / ↑(ψ n))) atTop ≤ smoothingFun μ x ^ a

Tactic:
by
  by_cases ha : a = 0
  · rw [ha] at hψ_lim
    calc limsup (fun n : ℕ => μ (x ^ s (ψ n)) ^ (1 / (ψ n : ℝ))) atTop ≤
          limsup (fun n : ℕ => μ x ^ ((s (ψ n) : ℝ) * (1 / (ψ n : ℝ)))) atTop := by
          apply csInf_le_csInf _ (μ_nonempty μ hs_le ψ)
          · intro b hb
            simp only [eventually_map, eventually_atTop, Set.mem_ofPred_eq] at hb ⊢
            obtain ⟨m, hm⟩ := hb
            use m
            intro k hkm
            apply le_trans _ (hm k hkm)
            rw [rpow_mul (apply_nonneg μ x), rpow_natCast]
            gcongr
            exact map_pow_le_pow' hμ1 x _
          · use 0
            simp only [mem_lowerBounds, eventually_map, eventually_atTop,
              Set.mem_ofPred_eq, forall_exists_index]
            exact fun _ m hm ↦ le_trans (by positivity) (hm m (le_refl _))
      _ ≤ 1 := (μ_limsup_le_one μ hs_le hψ_lim)
      _ = smoothingFun μ x ^ a := by rw [ha, rpow_zero]
  · have ha_pos : 0 < a := lt_of_le_of_ne a_in.1 (Ne.symm ha)
    have h_eq : (fun n : ℕ =>
        (μ (x ^ s (ψ n)) ^ (1 / (s (ψ n) : ℝ))) ^ ((s (ψ n) : ℝ) / (ψ n : ℝ))) =ᶠ[atTop]
        fun n : ℕ => μ (x ^ s (ψ n)) ^ (1 / (ψ n : ℝ)) := by
      have h : (fun n : ℕ => (1 : ℝ) / (s (ψ n) : ℝ) * (s (ψ n) : ℝ)) =ᶠ[atTop] 1 := by
        apply Filter.EventuallyEq.div_mul_cancel_atTop
        exact (tendsto_natCast_atTop_atTop.comp hψ_mono.tendsto_atTop).num ha_pos hψ_lim
      simp_rw [← rpow_mul (apply_nonneg μ _), mul_div]
      exact EventuallyEq.comp₂ EventuallyEq.rfl HPow.hPow (h.div EventuallyEq.rfl)
    exact ((tendsto_smoothingFun_of_map_one_le_one μ hμ1 x |>.comp <|
      tendsto_natCast_atTop_iff.mp <| (tendsto_natCast_atTop_atTop.comp
        hψ_mono.tendsto_atTop).num ha_pos hψ_lim).rpow
          hψ_lim <| .inr ha_pos).congr' h_eq |>.limsup_eq.le

Goal state after:
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: K : Type u
inst✝⁴ : NontriviallyNormedField K
L : Type v
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
inst✝ : CompleteSpace K
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
x : L
E : Type v := id ↥K⟮x⟯
this✝ : Field E :=
  id
    (have this := inferInstance;
    this)
this : Module K E :=
  id
    (have this := inferInstance;
    this)
id1 : ↥K⟮x⟯ →ₗ[K] E := LinearMap.id
id2 : E →ₗ[K] ↥K⟮x⟯ := LinearMap.id
hs_norm : RingNorm E :=
  { toFun := fun y ↦ spectralNorm K L ↑(id2 y), map_zero' := ⋯, add_le' := ⋯, neg' := ⋯, mul_le' := ⋯,
    eq_zero_of_map_eq_zero' := ⋯ }
n1 : NormedRing E := hs_norm.toNormedRing
N1 : NormedSpace K E :=
  { toSMul := DistribMulAction.toDistribSMul.toSMul, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯,
    add_smul := ⋯, zero_smul := ⋯, norm_smul_le := ⋯ }
hf_norm : RingNorm ↥K⟮x⟯ :=
  { toFun := fun y ↦ f ((algebraMap (↥K⟮x⟯) L) y), map_zero' := ⋯, add_le' := ⋯, neg' := ⋯, mul_le' := ⋯,
    eq_zero_of_map_eq_zero' := ⋯ }
⊢ ∃ C₁ C₂,
    ∃ (_ : 0 < C₁) (_ : 0 < C₂),
      ∀ (x_3 : ↥K[x]), f ↑x_3 ≤ C₁ * (spectralAlgNorm K L) ↑x_3 ∧ (spectralAlgNorm K L) ↑x_3 ≤ C₂ * f ↑x_3

Tactic:
let n2 : NormedRing K⟮x⟯ := RingNorm.toNormedRing hf_norm

Goal state after:
K : Type u
inst✝⁴ : NontriviallyNormedField K
L : Type v
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
inst✝ : CompleteSpace K
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
x : L
E : Type v := id ↥K⟮x⟯
this✝ : Field E :=
  id
    (have this := inferInstance;
    this)
this : Module K E :=
  id
    (have this := inferInstance;
    this)
id1 : ↥K⟮x⟯ →ₗ[K] E := LinearMap.id
id2 : E →ₗ[K] ↥K⟮x⟯ := LinearMap.id
hs_norm : RingNorm E :=
  { toFun := fun y ↦ spectralNorm K L ↑(id2 y), map_zero' := ⋯, add_le' := ⋯, neg' := ⋯, mul_le' := ⋯,
    eq_zero_of_map_eq_zero' := ⋯ }
n1 : NormedRing E := hs_norm.toNormedRing
N1 : NormedSpace K E :=
  { toSMul := DistribMulAction.toDistribSMul.toSMul, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯,
    add_smul := ⋯, zero_smul := ⋯, norm_smul_le := ⋯ }
hf_norm : RingNorm ↥K⟮x⟯ :=
  { toFun := fun y ↦ f ((algebraMap (↥K⟮x⟯) L) y), map_zero' := ⋯, add_le' := ⋯, neg' := ⋯, mul_le' := ⋯,
    eq_zero_of_map_eq_zero' := ⋯ }
n2 : NormedRing ↥K⟮x⟯ := hf_norm.toNormedRing
⊢ ∃ C₁ C₂,
    ∃ (_ : 0 < C₁) (_ : 0 < C₂),
      ∀ (x_3 : ↥K[x]), f ↑x_3 ≤ C₁ * (spectralAlgNorm K L) ↑x_3 ∧ (spectralAlgNorm K L) ↑x_3 ≤ C₂ * f ↑x_3