mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.InnerProductSpace.TwoDim

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : ¬x = 0
a : ℝ := ((o.basisRightAngleRotation x hx).repr y) 0
b : ℝ := ((o.basisRightAngleRotation x hx).repr y) 1
this : 0 ≤ a * ‖x‖ ^ 2 ∧ b * ‖x‖ ^ 2 = 0 → SameRay ℝ x (a • x + b • o.rightAngleRotation x)
⊢ 0 ≤ ⟪x, y⟫ ∧ (o.areaForm x) y = 0 → SameRay ℝ x y

Tactic:
rw [← (o.basisRightAngleRotation x hx).sum_repr y]
      simp only [Fin.sum_univ_succ, coe_basisRightAngleRotation, Matrix.cons_val_zero,
        Fin.succ_zero_eq_one', Finset.univ_eq_empty, Finset.sum_empty, areaForm_apply_self,
        map_smul, map_add, real_inner_smul_right, inner_add_right, Matrix.cons_val_one,
        smul_eq_mul, areaForm_rightAngleRotation_right,
        mul_zero, add_zero, zero_add, neg_zero, inner_rightAngleRotation_right,
        real_inner_self_eq_norm_sq]
      exact this

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: u : ℂ
hu : 0 < u.re
⊢ ∫ (x : ℝ) in 0..1, ↑x ^ (u - 1) * 1 = 1 / u

Tactic:
mul_one

Goal state after:
u : ℂ
hu : 0 < u.re
⊢ ∫ (x : ℝ) in 0..1, ↑x ^ (u - 1) = 1 / u
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
⊢ 2 * n + 2 * 1 = 2 * n + 2

Tactic:
mul_one

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
⊢ 2 * n + 2 = 2 * n + 2
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: z : ℂ
A :
  Tendsto
    (fun n ↦
      ((↑π * z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) *
          ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)) /
        ↑(∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)))
    atTop (𝓝 (Complex.sin (↑π * z)))
⊢ 𝓝 (Complex.sin (↑π * z)) = 𝓝 (Complex.sin (↑π * z) * 1)

Tactic:
mul_one

Goal state after:
z : ℂ
A :
  Tendsto
    (fun n ↦
      ((↑π * z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) *
          ∫ (x : ℝ) in 0..π / 2, Complex.cos (2 * z * ↑x) * ↑(cos x) ^ (2 * n)) /
        ↑(∫ (x : ℝ) in 0..π / 2, cos x ^ (2 * n)))
    atTop (𝓝 (Complex.sin (↑π * z)))
⊢ 𝓝 (Complex.sin (↑π * z)) = 𝓝 (Complex.sin (↑π * z))
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: a s : ℂ
hs : 0 < s.re + a.re
this :
  MellinConvergent ((Ioc 0 1).indicator fun a_1 ↦ ↑a_1 ^ a * 1) s ∧
    mellin ((Ioc 0 1).indicator fun a_1 ↦ ↑a_1 ^ a * 1) s = 1 / (s + a)
⊢ HasMellin ((Ioc 0 1).indicator fun t ↦ ↑t ^ a) s (1 / (s + a))

Tactic:
mul_one

Goal state after:
a s : ℂ
hs : 0 < s.re + a.re
this :
  MellinConvergent ((Ioc 0 1).indicator fun a_1 ↦ ↑a_1 ^ a) s ∧
    mellin ((Ioc 0 1).indicator fun a_1 ↦ ↑a_1 ^ a) s = 1 / (s + a)
⊢ HasMellin ((Ioc 0 1).indicator fun t ↦ ↑t ^ a) s (1 / (s + a))
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
inst✝⁶ : TopologicalSpace k
inst✝⁵ : OrderTopology k
inst✝⁴ : IsStrictOrderedRing k
inst✝³ : IsTopologicalAddGroup V
inst✝² : ContinuousSMul k V
inst✝¹ : TopologicalSpace P
inst✝ : IsTopologicalAddTorsor P
v : V
s : Set P
h : s ∈ asymptoticNhds k P v
p : P
⊢ s ∈ (asymptoticNhds k P v).bind 𝓝

Tactic:
rw [asymptoticNhds_eq_smul_vadd _ p, vadd_pure] at h ⊢

Goal state after:
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
inst✝⁶ : TopologicalSpace k
inst✝⁵ : OrderTopology k
inst✝⁴ : IsStrictOrderedRing k
inst✝³ : IsTopologicalAddGroup V
inst✝² : ContinuousSMul k V
inst✝¹ : TopologicalSpace P
inst✝ : IsTopologicalAddTorsor P
v : V
s : Set P
p : P
h : s ∈ map (fun x ↦ x +ᵥ p) (atTop • 𝓝 v)
⊢ s ∈ (map (fun x ↦ x +ᵥ p) (atTop • 𝓝 v)).bind 𝓝
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: case inl
s : ℂ
hs : 0 < s.re
f : ℕ → ℝ → ℂ := fun n ↦ (Ioc 0 ↑n).indicator fun x ↦ ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)
f_ible : ∀ (n : ℕ), Integrable (f n) (volume.restrict (Ioi 0))
f_tends : ∀ x ∈ Ioi 0, Tendsto (fun n ↦ f n x) atTop (𝓝 (↑(rexp (-x)) * ↑x ^ (s - 1)))
n : ℕ
x : ℝ
hx : 0 < x
hxn : ↑n < x
⊢ ‖(Ioc 0 ↑n).indicator (fun x ↦ ↑((1 - x / ↑n) ^ n) * ↑x ^ (s - 1)) x‖ ≤ rexp (-x) * x ^ (s.re - 1)

Tactic:
rw [indicator_of_notMem (notMem_Ioc_of_gt hxn), norm_zero,
        mul_nonneg_iff_right_nonneg_of_pos (exp_pos _)]
      positivity

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

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_3
W : Type u_4
W₂ : Type u_5
inst✝⁶ : SeminormedAddCommGroup V
inst✝⁵ : SeminormedAddCommGroup W
inst✝⁴ : SeminormedAddCommGroup W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : V →ᴬ[𝕜] W
g : W₂ →ᴬ[𝕜] V
⊢ ‖f.comp g‖ ≤ ‖f‖ * ‖g‖ + ‖f 0‖

Tactic:
rw [norm_def, max_le_iff]

Goal state after:
𝕜 : Type u_1
V : Type u_3
W : Type u_4
W₂ : Type u_5
inst✝⁶ : SeminormedAddCommGroup V
inst✝⁵ : SeminormedAddCommGroup W
inst✝⁴ : SeminormedAddCommGroup W₂
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedSpace 𝕜 V
inst✝¹ : NormedSpace 𝕜 W
inst✝ : NormedSpace 𝕜 W₂
f : V →ᴬ[𝕜] W
g : W₂ →ᴬ[𝕜] V
⊢ ‖(f.comp g) 0‖ ≤ ‖f‖ * ‖g‖ + ‖f 0‖ ∧ ‖(f.comp g).contLinear‖ ≤ ‖f‖ * ‖g‖ + ‖f 0‖
Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: case inl.inr
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex R P n
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
h₁₂lt : i₁ < i₂
h₄₃lt : i₄ < i₃
⊢ dist (s.points i₁) (s.points i₂) ≠ dist (s.points i₃) (s.points i₄)

Tactic:
nth_rw 2 [dist_comm]

Goal state after:
case inl.inr
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex R P n
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
h₁₂lt : i₁ < i₂
h₄₃lt : i₄ < i₃
⊢ dist (s.points i₁) (s.points i₂) ≠ dist (s.points i₄) (s.points i₃)
Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: case inr.inr
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex R P n
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
h₂₁lt : i₂ < i₁
h₄₃lt : i₄ < i₃
⊢ dist (s.points i₂) (s.points i₁) ≠ dist (s.points i₃) (s.points i₄)

Tactic:
nth_rw 2 [dist_comm]

Goal state after:
case inr.inr
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Ring R
inst✝³ : SeminormedAddCommGroup V
inst✝² : PseudoMetricSpace P
inst✝¹ : Module R V
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex R P n
hs : s.Scalene
i₁ i₂ i₃ i₄ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₃₄ : i₃ ≠ i₄
h₁₂₃₄ : ¬i₁ = i₃ ∨ ¬i₂ = i₄
h₁₂₄₃ : ¬i₁ = i₄ ∨ ¬i₂ = i₃
h₂₁lt : i₂ < i₁
h₄₃lt : i₄ < i₃
⊢ dist (s.points i₂) (s.points i₁) ≠ dist (s.points i₄) (s.points i₃)
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
h✝ : Nontrivial k
w : ↑Set.univ → Fin 3 → k := fun i ↦ Finset.affineCombinationLineMapWeights (↑i + 1) (↑i + 2) (r ↑i)
hw : ∀ (i : ↑Set.univ), ∑ j, w i j = 1
w' : Fin (2 + 1) → k
hw' : ∑ j, w' j = 1
h : ∀ (i : ↑Set.univ), ∃ r, ∀ (j : Fin (2 + 1)), r * {↑i}ᶜ.indicator (w i) j = {↑i}ᶜ.indicator w' j
hp' :
  ∀ (i : Fin 3),
    (Finset.affineCombination k Finset.univ t.points) w' ∈
      line[k, t.points i, (AffineMap.lineMap (t.points (i + 1)) (t.points (i + 2))) (r i)]
hp'w :
  ∀ (i : ↑Set.univ),
    (Finset.affineCombination k Finset.univ t.points) w' ∈
      line[k, t.points ↑i, (Finset.affineCombination k Finset.univ t.points) (w i)]
h' :
  ∀ (i : Fin 3), ∃ c, ∀ (j : Fin 3), j ≠ i → c * Finset.affineCombinationLineMapWeights (i + 1) (i + 2) (r i) j = w' j
c : Fin 3 → k := fun i ↦ ⋯.choose
hc : ∀ (i j : Fin 3), j ≠ i → c i * Finset.affineCombinationLineMapWeights (i + 1) (i + 2) (r i) j = w' j
hc1 : ∀ (i : Fin 3), c i * (1 - r i) = w' (i + 1)
hc2 : ∀ (i : Fin 3), c i * r i = w' (i + 2)
hcr : (∏ i, c i) * ∏ i, r i = (∏ i, c i) * ∏ i, (1 - r i)
i : Fin 3
hi : c i = 0
hw'i1 : w' (i + 1) = 0
hw'i2 : w' (i + 2) = 0
⊢ w' i = w' 0 + w' 1 + w' 2

Tactic:
fin_cases i <;> grind

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

Goal state before:
pp: X : Type u_1
E : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : PreconnectedSpace X
inst✝ : SeminormedAddCommGroup E
f : X → E
M : ℝ
x : X
hM : 0 < M
hx : ‖f x‖ = M
h : IsMinOn (fun x ↦ ‖f x‖) univ x
hf : Continuous[inst✝², PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
H : ∀ {y : X} (z : X), ‖f y‖ = M → ∀ n > 0, ‖f z‖ ≤ M * (1 + (‖f z - f y‖ / M) ^ n)
y : X
⊢ {y | ‖f y‖ = M} = univ

Tactic:
refine IsClopen.eq_univ ⟨isClosed_eq (by fun_prop) (by fun_prop), ?_⟩ <| nonempty_of_mem hx

Goal state after:
X : Type u_1
E : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : PreconnectedSpace X
inst✝ : SeminormedAddCommGroup E
f : X → E
M : ℝ
x : X
hM : 0 < M
hx : ‖f x‖ = M
h : IsMinOn (fun x ↦ ‖f x‖) univ x
hf : Continuous[inst✝², PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
H : ∀ {y : X} (z : X), ‖f y‖ = M → ∀ n > 0, ‖f z‖ ≤ M * (1 + (‖f z - f y‖ / M) ^ n)
y : X
⊢ IsOpen[inst✝²] {y | ‖f y‖ = M}
Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur

Goal state before:
pp: case inr
F : Type u_1
inst✝³ : NormedRing F
inst✝² : NormOneClass F
inst✝¹ : NormMulClass F
inst✝ : NormedAlgebra ℂ F
x : F
z : ℂ
hz : IsMinOn (fun x_1 ↦ ‖x - (algebraMap ℂ F) x_1‖) Set.univ z
M : ℝ := ‖x - (algebraMap ℂ F) z‖
hM : M = ‖x - (algebraMap ℂ F) z‖
hM₀ : 0 < M
H : ∀ (z : ℂ), ‖x - (algebraMap ℂ F) z‖ ≠ 0
key : ‖↑‖x‖ + ↑M + 1‖ * 1 - ‖x‖ ≤ M
⊢ False

Tactic:
mul_one

Goal state after:
case inr
F : Type u_1
inst✝³ : NormedRing F
inst✝² : NormOneClass F
inst✝¹ : NormMulClass F
inst✝ : NormedAlgebra ℂ F
x : F
z : ℂ
hz : IsMinOn (fun x_1 ↦ ‖x - (algebraMap ℂ F) x_1‖) Set.univ z
M : ℝ := ‖x - (algebraMap ℂ F) z‖
hM : M = ‖x - (algebraMap ℂ F) z‖
hM₀ : 0 < M
H : ∀ (z : ℂ), ‖x - (algebraMap ℂ F) z‖ ≠ 0
key : ‖↑‖x‖ + ↑M + 1‖ - ‖x‖ ≤ M
⊢ False
Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur

Goal state before:
pp: case succ
F : Type u_1
inst✝³ : NormedRing F
inst✝² : NormedAlgebra ℝ F
inst✝¹ : NormOneClass F
inst✝ : NormMulClass F
x : F
M : ℝ
hM : 0 ≤ M
h : ∀ (z : ℝ × ℝ), M ≤ ‖φ x z‖
n : ℕ
ih : ∀ {p : ℝ[X]}, p.IsMonicOfDegree (2 * n) → M ^ n ≤ ‖(aeval x) p‖
p : ℝ[X]
hp : p.IsMonicOfDegree (2 * n + 2 * 1)
⊢ M ^ (n + 1) ≤ ‖(aeval x) p‖

Tactic:
mul_one

Goal state after:
case succ
F : Type u_1
inst✝³ : NormedRing F
inst✝² : NormedAlgebra ℝ F
inst✝¹ : NormOneClass F
inst✝ : NormMulClass F
x : F
M : ℝ
hM : 0 ≤ M
h : ∀ (z : ℝ × ℝ), M ≤ ‖φ x z‖
n : ℕ
ih : ∀ {p : ℝ[X]}, p.IsMonicOfDegree (2 * n) → M ^ n ≤ ‖(aeval x) p‖
p : ℝ[X]
hp : p.IsMonicOfDegree (2 * n + 2)
⊢ M ^ (n + 1) ≤ ‖(aeval x) p‖
Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur

Goal state before:
pp: F : Type u_1
inst✝³ : NormedRing F
inst✝² : NormedAlgebra ℝ F
inst✝¹ : NormOneClass F
inst✝ : NormMulClass F
x : F
z : ℝ × ℝ
h : IsMinOn (fun x_1 ↦ ‖φ x x_1‖) Set.univ z
w✝ : ℝ × ℝ
M : ℝ := ‖φ x z‖
H : M ≠ 0
hM : M = ‖φ x z‖
hM₀ : 0 < M
w u : ℝ × ℝ
hw : ‖φ x w‖ = M
n : ℕ
hn : n > 0
q : ℝ × ℝ → ℝ[X] := fun y ↦ X ^ 2 - C y.1 * X + C y.2
hq : ∀ (y : ℝ × ℝ), (q y).IsMonicOfDegree 2
p : ℝ[X]
hp : p.IsMonicOfDegree (2 * (n - 1))
hrel : q w ^ n = p * q u + (q w - q u) ^ n
⊢ ‖φ x u‖ * M ^ (n - 1) ≤ M ^ n + ‖φ x u - φ x w‖ ^ n

Tactic:
le_aeval_of_isMonicOfDegree hM₀.le (isMinOn_univ_iff.mp h) hp

Goal state after:
F : Type u_1
inst✝³ : NormedRing F
inst✝² : NormedAlgebra ℝ F
inst✝¹ : NormOneClass F
inst✝ : NormMulClass F
x : F
z : ℝ × ℝ
h : IsMinOn (fun x_1 ↦ ‖φ x x_1‖) Set.univ z
w✝ : ℝ × ℝ
M : ℝ := ‖φ x z‖
H : M ≠ 0
hM : M = ‖φ x z‖
hM₀ : 0 < M
w u : ℝ × ℝ
hw : ‖φ x w‖ = M
n : ℕ
hn : n > 0
q : ℝ × ℝ → ℝ[X] := fun y ↦ X ^ 2 - C y.1 * X + C y.2
hq : ∀ (y : ℝ × ℝ), (q y).IsMonicOfDegree 2
p : ℝ[X]
hp : p.IsMonicOfDegree (2 * (n - 1))
hrel : q w ^ n = p * q u + (q w - q u) ^ n
⊢ ‖φ x u‖ * ‖(aeval x) p‖ ≤ M ^ n + ‖φ x u - φ x w‖ ^ n
Module: Mathlib.Analysis.Normed.Field.Ultra

Goal state before:
pp: case inr
R : Type u_1
inst✝ : NormedDivisionRing R
h : ∀ (x : R), ‖x‖ ≤ 1 → ‖x + 1‖ ≤ 1
x : R
H : 1 < ‖x‖
⊢ ‖1 / x‖ ≤ 1

Tactic:
simp [inv_le_one_iff₀, H.le]

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

Goal state before:
pp: q : ℍ
⊢ exp q.re ^ 2 * 1 = exp q.re ^ 2

Tactic:
mul_one

Goal state after:
q : ℍ
⊢ exp q.re ^ 2 = exp q.re ^ 2
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‖
⊢ Tendsto (fun x_1 ↦ x ^ 2 - (x_1.1 • x - (algebraMap ℝ F) x_1.2)) (cobounded (ℝ × ℝ)) (cobounded F)

Tactic:
refine tendsto_const_sub_cobounded _ |>.comp ?_

Goal state after:
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‖
⊢ Tendsto (fun x_1 ↦ x_1.1 • x - (algebraMap ℝ F) x_1.2) (cobounded (ℝ × ℝ)) (cobounded F)
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
x : R
f_mul : f x ≤ c * f 1 * f x
hx : 0 < f x
⊢ 0 ≤ c

Tactic:
le_mul_iff_one_le_left hx

Goal state after:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
x : R
f_mul : 1 ≤ c * f 1
hx : 0 < f x
⊢ 0 ≤ c
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
⊢ seminormFromBounded' f x = 0 ↔ f x = 0

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · have hf := seminormFromBounded_ge f_nonneg f_mul x
    rw [h, mul_zero] at hf
    exact hf.antisymm (f_nonneg _)
  · have hf : seminormFromBounded' f x ≤ c * f x :=
      seminormFromBounded_le f_nonneg f_mul x
    rw [h, mul_zero] at hf
    exact hf.antisymm (seminormFromBounded_nonneg f_nonneg f_mul x)

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

Goal state before:
pp: case neg
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
f_ne_zero : f = 0
⊢ seminormFromBounded' f 1 ≤ 1

Tactic:
· simp_rw [seminormFromBounded', one_mul]
    refine ciSup_le (fun _ ↦ ?_)
    simp only [f_ne_zero, Pi.zero_apply, div_zero, zero_le_one]

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

Goal state before:
pp: case neg
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
hx✝ : ∀ (y : R), f (x✝ * y) = f x✝ * f y
x : R
hx : ¬f x = 0
⊢ f x✝ * 1 ≤ f x✝

Tactic:
mul_one

Goal state after:
case neg
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
hx✝ : ∀ (y : R), f (x✝ * y) = f x✝ * f y
x : R
hx : ¬f x = 0
⊢ f x✝ ≤ f x✝
Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
hx : ∀ (y : R), f (x * y) ≤ f x * f y
h_one : f 1 ≤ 1
y : R
hy0 : ¬f y = 0
⊢ f (x * y) ≤ f x * 1 * f y

Tactic:
mul_one

Goal state after:
case neg
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
hx : ∀ (y : R), f (x * y) ≤ f x * f y
h_one : f 1 ≤ 1
y : R
hy0 : ¬f y = 0
⊢ f (x * y) ≤ f x * f y
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
n : ℕ
⊢ f c * 1 = f c

Tactic:
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
n : ℕ
⊢ f c = f c
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
hlim : Tendsto (fun n ↦ seminormFromConst_seq c f x (n + 1)) atTop (𝓝 (seminormFromConst' c f x))
n : ℕ
⊢ f (c * c ^ n * x) * (f c)⁻¹ ^ n = f (c * c ^ n * x) * 1 * (f c)⁻¹ ^ n

Tactic:
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
x : R
hlim : Tendsto (fun n ↦ seminormFromConst_seq c f x (n + 1)) atTop (𝓝 (seminormFromConst' c f x))
n : ℕ
⊢ f (c * c ^ n * x) * (f c)⁻¹ ^ n = f (c * c ^ n * x) * (f c)⁻¹ ^ n
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

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

Tactic:
simp only [spectralValueTerms_of_lt_natDegree _ hPn]

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

Goal state before:
pp: case pos
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
norm_sub_le : ∀ (a' : F), IsConjRoot L a a' → a ≠ a' → δ ≤ ‖a - a'‖
hS : S.Nonempty
⊢ ∀ a_1 ∈ S, 0 < ‖a - a_1‖

Tactic:
rintro a' ha'

Goal state after:
case pos
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
norm_sub_le : ∀ (a' : F), IsConjRoot L a a' → a ≠ a' → δ ≤ ‖a - a'‖
hS : S.Nonempty
a' : f.SplittingField
ha' : a' ∈ S
⊢ 0 < ‖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)
⊢ sInf {a | ∀ᶠ (n : ℝ) in map (fun n ↦ μ x ^ (↑(s (ψ n)) * (1 / ↑(ψ n)))) atTop, n ≤ a} ≤ 1

Tactic:
rw [csInf_le_iff (μ_bddBelow μ s ψ) (μ_nonempty μ hs_le ψ)]

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)
⊢ ∀ b ∈ lowerBounds {a | ∀ᶠ (n : ℝ) in map (fun n ↦ μ x ^ (↑(s (ψ n)) * (1 / ↑(ψ n)))) atTop, n ≤ a}, b ≤ 1
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝³ : NormedField K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
E : IntermediateField K L
y : L
h_fin : FiniteDimensional K L
hn : Normal K L
inst✝ : IsUltrametricDist K
⊢ ∀ (r s : L), spectralNorm K L (r + s) ≤ spectralNorm K L r + spectralNorm K L s

Tactic:
rw [spectralNorm_eq_invariantExtension]; exact map_add_le_add _

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

Goal state before:
pp: K : Type u_2
inst✝³ : NormedField K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsUltrametricDist K
y : L
hy✝ : IsAlgebraic K y
E : IntermediateField K L := K⟮y⟯
h_finiteDimensional_E : FiniteDimensional K ↥E
g : ↥K⟮y⟯ := AdjoinSimple.gen K y
hy : -y = (algebraMap (↥K⟮y⟯) L) (-g)
⊢ spectralNorm K (↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯)))
      (-(algebraMap ↥K⟮y⟯ ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯))) g) =
    spectralNorm K (↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯)))
      ((algebraMap ↥K⟮y⟯ ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯))) g)

Tactic:
← spectralAlgNorm_of_finiteDimensional_normal_def

Goal state after:
K : Type u_2
inst✝³ : NormedField K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsUltrametricDist K
y : L
hy✝ : IsAlgebraic K y
E : IntermediateField K L := K⟮y⟯
h_finiteDimensional_E : FiniteDimensional K ↥E
g : ↥K⟮y⟯ := AdjoinSimple.gen K y
hy : -y = (algebraMap (↥K⟮y⟯) L) (-g)
⊢ (spectralAlgNorm_of_finiteDimensional_normal K ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯)))
      (-(algebraMap ↥K⟮y⟯ ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯))) g) =
    spectralNorm K (↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯)))
      ((algebraMap ↥K⟮y⟯ ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯))) g)
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: K : Type u_2
inst✝³ : NormedField K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsUltrametricDist K
k : K
y : L
hy : IsAlgebraic K y
E : IntermediateField K L := K⟮y⟯
h_finiteDimensional_E : FiniteDimensional K ↥E
g : ↥K⟮y⟯ := AdjoinSimple.gen K y
hgy : k • y = (algebraMap (↥K⟮y⟯) L) (k • g)
h :
  (algebraMap ↥K⟮y⟯ ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯))) (k • g) =
    k • (algebraMap ↥K⟮y⟯ ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯))) g
⊢ spectralNorm K (↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯)))
      (k • (algebraMap ↥K⟮y⟯ ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯))) g) =
    ↑‖k‖₊ *
      spectralNorm K (↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯)))
        ((algebraMap ↥K⟮y⟯ ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯))) g)

Tactic:
← spectralAlgNorm_of_finiteDimensional_normal_def

Goal state after:
K : Type u_2
inst✝³ : NormedField K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsUltrametricDist K
k : K
y : L
hy : IsAlgebraic K y
E : IntermediateField K L := K⟮y⟯
h_finiteDimensional_E : FiniteDimensional K ↥E
g : ↥K⟮y⟯ := AdjoinSimple.gen K y
hgy : k • y = (algebraMap (↥K⟮y⟯) L) (k • g)
h :
  (algebraMap ↥K⟮y⟯ ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯))) (k • g) =
    k • (algebraMap ↥K⟮y⟯ ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯))) g
⊢ (spectralAlgNorm_of_finiteDimensional_normal K ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯)))
      (k • (algebraMap ↥K⟮y⟯ ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯))) g) =
    ↑‖k‖₊ *
      spectralNorm K (↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯)))
        ((algebraMap ↥K⟮y⟯ ↥(normalClosure K (↥K⟮y⟯) (AlgebraicClosure ↥K⟮y⟯))) g)