mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Beta

Goal state before:
pp: s : ℂ
n : ℕ
hs : -s.re < ↑n
⊢ DifferentiableAt ℂ (fun s ↦ (Gamma s)⁻¹) s

Tactic:
induction n generalizing s with

Goal state after:
Module: Mathlib.Analysis.Polynomial.Factorization

Goal state before:
pp: case inl.inl
f : ℝ[X]
n : ℕ
g₁ g₂ : ℝ[X]
hf : (g₁ * g₂).IsMonicOfDegree (2 + n)
h : f = g₁ * g₂
hd₁ : g₁.IsMonicOfDegree 1
hg₂ : g₂.IsMonicOfDegree (n + 1)
p₁ p₂ : ℝ[X]
h' : g₂ = p₁ * p₂
hp₁ : p₁.IsMonicOfDegree 1
⊢ ∃ f₁ f₂, f₁.IsMonicOfDegree 2 ∧ f₂.IsMonicOfDegree n ∧ f = f₁ * f₂

pp: case inl.inr
f : ℝ[X]
n : ℕ
g₁ g₂ : ℝ[X]
hf : (g₁ * g₂).IsMonicOfDegree (2 + n)
h : f = g₁ * g₂
hd₁ : g₁.IsMonicOfDegree 1
hg₂ : g₂.IsMonicOfDegree (n + 1)
p₁ p₂ : ℝ[X]
h' : g₂ = p₁ * p₂
hp₂ : p₁.IsMonicOfDegree 2
⊢ ∃ f₁ f₂, f₁.IsMonicOfDegree 2 ∧ f₂.IsMonicOfDegree n ∧ f = f₁ * f₂

Tactic:
· rw [h', ← mul_assoc] at h hf
      exact ⟨g₁ * p₁, p₂, hd₁.mul hp₁, (hd₁.mul hp₁).of_mul_left hf, h⟩

Goal state after:
case inl.inr
f : ℝ[X]
n : ℕ
g₁ g₂ : ℝ[X]
hf : (g₁ * g₂).IsMonicOfDegree (2 + n)
h : f = g₁ * g₂
hd₁ : g₁.IsMonicOfDegree 1
hg₂ : g₂.IsMonicOfDegree (n + 1)
p₁ p₂ : ℝ[X]
h' : g₂ = p₁ * p₂
hp₂ : p₁.IsMonicOfDegree 2
⊢ ∃ f₁ f₂, f₁.IsMonicOfDegree 2 ∧ f₂.IsMonicOfDegree n ∧ f = f₁ * f₂
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 = 1

Tactic:
rw [← hw', Fin.sum_univ_three]

Goal state after:
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
Module: Mathlib.Analysis.Normed.Affine.Simplex

Goal state before:
pp: case refine_1
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
t : Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
x✝ : Simplex.Equilateral t
r : ℝ
hr : ∀ (i j : Fin (2 + 1)), i ≠ j → dist (t.points i) (t.points j) = r
⊢ dist (t.points i₁) (t.points i₂) = dist (t.points i₁) (t.points i₃) ∧
    dist (t.points i₁) (t.points i₂) = dist (t.points i₂) (t.points i₃)

pp: case refine_2
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
t : Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h :
  dist (t.points i₁) (t.points i₂) = dist (t.points i₁) (t.points i₃) ∧
    dist (t.points i₁) (t.points i₂) = dist (t.points i₂) (t.points i₃)
⊢ Simplex.Equilateral t

Tactic:
· simp [hr _ _ h₁₂, hr _ _ h₁₃, hr _ _ h₂₃]

Goal state after:
case refine_2
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
t : Triangle R P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h :
  dist (t.points i₁) (t.points i₂) = dist (t.points i₁) (t.points i₃) ∧
    dist (t.points i₁) (t.points i₂) = dist (t.points i₂) (t.points i₃)
⊢ Simplex.Equilateral t
Module: Mathlib.Analysis.Quaternion

Goal state before:
pp: a : ℍ
⊢ √(normSq (star a)) = √(normSq a)

Tactic:
normSq_star

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Series

Goal state before:
pp: case hdb
x : ℝ
i : ℕ
⊢ 2 ^ i * i ! ≤ (2 * i)!

Tactic:
exact Nat.two_pow_mul_factorial_le_factorial_two_mul _

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
inst✝ : NormMulClass F
x : F
z : ℝ × ℝ
h : IsMinOn (fun x_1 ↦ ‖φ x x_1‖) Set.univ z
H : ‖φ x z‖ ≠ 0
w : ℝ × ℝ
⊢ ‖φ x w‖ = ‖φ x z‖

Tactic:
by
  set M : ℝ := ‖φ x z‖ with hM
  have hM₀ : 0 < M := by positivity
  -- we use the key result `norm_eq_of_isMinOn_of_forall_le`
  refine norm_eq_of_isMinOn_of_forall_le hM₀ hM.symm h (continuous_φ x) (fun {w} u hw n hn ↦ ?_) w
  -- show `‖φ x u‖ ≤ M * (1 + (‖φ x u - φ x w‖ / M) ^ n)`
  have HH : M * (1 + (‖φ x u - φ x w‖ / M) ^ n) = (M ^ n + ‖φ x u - φ x w‖ ^ n) / M ^ (n - 1) := by
    simp only [field, div_pow, ← pow_succ', Nat.sub_add_cancel hn]
  rw [HH, le_div_iff₀ (by positivity)]; clear HH
  -- show `‖φ x u‖ * M ^ (n - 1) ≤ M ^ n + ‖φ x u - φ x w‖ ^ n`
  let q (y : ℝ × ℝ) : ℝ[X] := X ^ 2 - C y.1 * X + C y.2
  have hq (y : ℝ × ℝ) : IsMonicOfDegree (q y) 2 := isMonicOfDegree_sub_add_two ..
  have hsub : q w - q u = (C u.1 - C w.1) * X + C w.2 - C u.2 := by simp only [q]; ring
  have hdvd : q u ∣ q w ^ n - (q w - q u) ^ n := by
    nth_rewrite 1 [← sub_sub_self (q w) (q u)]
    exact sub_dvd_pow_sub_pow ..
  have H' : ((q w - q u) ^ n).natDegree < 2 * n := by rw [hsub]; compute_degree; grind
  -- write `q w ^ n = p * q u + (q w - q u) ^ n` with a monic polynomial `p` of deg. `2 * (n - 1)`,
  -- where `aeval x (q u) = φ x u` (*).
  obtain ⟨p, hp, hrel⟩ := ((hq w).pow n).of_dvd_sub (by grind) (hq u) H' hdvd; clear H' hdvd hsub
  rw [show 2 * n - 2 = 2 * (n - 1) by grind] at hp
  -- use that `‖aeval p x‖ ≥ M ^ (n - 1)`.
  grw [le_aeval_of_isMonicOfDegree hM₀.le (isMinOn_univ_iff.mp h) hp]
  -- from (*) above, deduce
  -- `‖φ x u‖ * ‖(aeval x) p‖ = ‖(aeval x) (q w ^ n) - (aeval x) ((q w - q u) ^ n)‖`
  -- and use that.
  rw [← sub_eq_iff_eq_add, eq_comm, mul_comm] at hrel
  apply_fun (‖aeval x ·‖) at hrel
  rw [map_mul, norm_mul, map_sub, aeval_eq_φ x u] at hrel
  rw [hrel, norm_sub_rev (φ ..)]
  exact (norm_sub_le ..).trans <| by simp [q, aeval_eq_φ, hw]

Goal state after:
Module: Mathlib.Analysis.Normed.Field.Ultra

Goal state before:
pp: case h
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm : max 1 (‖x‖ ^ m) = 1
hx : ‖x‖ ^ m ≤ 1
i : ℕ
hi : i ∈ Finset.range (m + 1)
⊢ ‖x‖ ^ i ≤ 1

pp: case ha
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm : max 1 (‖x‖ ^ m) = ‖x‖ ^ m
hx : 1 < ‖x‖ ^ m
i : ℕ
hi : i ∈ Finset.range (m + 1)
⊢ 1 ≤ ‖x‖

pp: case hmn
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm : max 1 (‖x‖ ^ m) = ‖x‖ ^ m
hx : 1 < ‖x‖ ^ m
i : ℕ
hi : i ∈ Finset.range (m + 1)
⊢ i ≤ m

Tactic:
· rcases eq_or_ne m 0 with rfl | hm
    · simp only [pow_zero, le_refl,
        show i = 0 by simpa only [zero_add, Finset.range_one, Finset.mem_singleton] using hi]
    · rw [pow_le_one_iff_of_nonneg (norm_nonneg _) hm] at hx
      exact pow_le_one₀ (norm_nonneg _) hx

Goal state after:
case ha
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm : max 1 (‖x‖ ^ m) = ‖x‖ ^ m
hx : 1 < ‖x‖ ^ m
i : ℕ
hi : i ∈ Finset.range (m + 1)
⊢ 1 ≤ ‖x‖

case hmn
R : Type u_1
inst✝ : NormedDivisionRing R
x : R
m : ℕ
h : ∀ (x : R) (n : ℕ), ‖n • x‖ ≤ ‖x‖
hm : max 1 (‖x‖ ^ m) = ‖x‖ ^ m
hx : 1 < ‖x‖ ^ m
i : ℕ
hi : i ∈ Finset.range (m + 1)
⊢ i ≤ m
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
u : ℝ
hu : IsMinOn (fun x_1 ↦ ‖x - (algebraMap ℝ F) x_1‖) univ u
⊢ ∃ z, IsMinOn (fun x_1 ↦ ‖φ x x_1‖) univ z

Tactic:
rcases eq_or_lt_of_le (norm_nonneg (x - algebraMap ℝ F u)) with hc₀ | hc₀

Goal state after:
case inl
F : Type u_1
inst✝² : NormedRing F
inst✝¹ : NormedAlgebra ℝ F
inst✝ : NormOneClass F
x : F
u : ℝ
hu : IsMinOn (fun x_1 ↦ ‖x - (algebraMap ℝ F) x_1‖) univ u
hc₀ : 0 = ‖x - (algebraMap ℝ F) u‖
⊢ ∃ z, IsMinOn (fun x_1 ↦ ‖φ x x_1‖) univ z

case inr
F : Type u_1
inst✝² : NormedRing F
inst✝¹ : NormedAlgebra ℝ F
inst✝ : NormOneClass F
x : F
u : ℝ
hu : IsMinOn (fun x_1 ↦ ‖x - (algebraMap ℝ F) x_1‖) univ u
hc₀ : 0 < ‖x - (algebraMap ℝ F) u‖
⊢ ∃ z, IsMinOn (fun x_1 ↦ ‖φ x x_1‖) univ z
Module: Mathlib.Analysis.Normed.Algebra.GelfandMazur

Goal state before:
pp: case inl
F : Type u_1
inst✝² : NormedRing F
inst✝¹ : NormedAlgebra ℝ F
inst✝ : NormOneClass F
x : F
u : ℝ
hu : IsMinOn (fun x_1 ↦ ‖x - (algebraMap ℝ F) x_1‖) univ u
hc₀ : 0 = ‖x - (algebraMap ℝ F) u‖
⊢ ∃ z, IsMinOn (fun x_1 ↦ ‖φ x x_1‖) univ z

pp: case inr
F : Type u_1
inst✝² : NormedRing F
inst✝¹ : NormedAlgebra ℝ F
inst✝ : NormOneClass F
x : F
u : ℝ
hu : IsMinOn (fun x_1 ↦ ‖x - (algebraMap ℝ F) x_1‖) univ u
hc₀ : 0 < ‖x - (algebraMap ℝ F) u‖
⊢ ∃ z, IsMinOn (fun x_1 ↦ ‖φ x x_1‖) univ z

Tactic:
· rw [eq_comm, norm_eq_zero, sub_eq_zero] at hc₀
    exact ⟨(u, 0), fun _ ↦ by simp [φ, hc₀, sq, Algebra.smul_def]⟩

Goal state after:
case inr
F : Type u_1
inst✝² : NormedRing F
inst✝¹ : NormedAlgebra ℝ F
inst✝ : NormOneClass F
x : F
u : ℝ
hu : IsMinOn (fun x_1 ↦ ‖x - (algebraMap ℝ F) x_1‖) univ u
hc₀ : 0 < ‖x - (algebraMap ℝ F) u‖
⊢ ∃ z, IsMinOn (fun x_1 ↦ ‖φ x x_1‖) univ z
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
H : φ x z ≠ 0
M : ℝ := ‖φ x z‖
h' : ∀ (r : ℝ), √M ≤ ‖x - (algebraMap ℝ F) r‖
this : Filter.Tendsto (fun x_1 ↦ ‖φ x z‖) (Bornology.cobounded (ℝ × ℝ)) Filter.atTop
⊢ False

Tactic:
exact Filter.not_tendsto_const_atTop _ _ this

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
h1 : ¬f 1 = 0
| f x / f 1

Tactic:
← mul_one x

Goal state after:
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
h1 : ¬f 1 = 0
| f (x * 1) / f 1
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
x y : L
⊢ (Classical.choose ⋯) (σ (x * y)) ≤ (Classical.choose ⋯) (σ x) * (Classical.choose ⋯) (σ y)

Tactic:
simp [map_mul σ, map_mul_le_mul]

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_zero : f 0 = 0
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
f_add : ∀ (a b : R), f (a + b) ≤ f a + f b
f_neg : ∀ (x : R), f (-x) = f x
h0 : ∀ (x : R), (seminormFromBounded f_zero f_nonneg f_mul f_add f_neg).toFun x = 0 → x = 0
⊢ f ⁻¹' {0} = {0}

Tactic:
← seminormFromBounded_ker f_nonneg f_mul

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_zero : f 0 = 0
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
f_add : ∀ (a b : R), f (a + b) ≤ f a + f b
f_neg : ∀ (x : R), f (-x) = f x
h0 : ∀ (x : R), (seminormFromBounded f_zero f_nonneg f_mul f_add f_neg).toFun x = 0 → x = 0
⊢ seminormFromBounded' f ⁻¹' {0} = {0}
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: R : Type u_1
inst✝¹ : SeminormedRing R
inst✝ : Nontrivial R
n : ℕ
⊢ (⨆ n_1, if n_1 < (X ^ n).natDegree then ‖(X ^ n).coeff n_1‖ ^ (1 / (↑(X ^ n).natDegree - ↑n_1)) else 0) = 0

Tactic:
simp_rw [coeff_X_pow n, natDegree_X_pow]

Goal state after:
R : Type u_1
inst✝¹ : SeminormedRing R
inst✝ : Nontrivial R
n : ℕ
⊢ (⨆ n_1, if n_1 < n then ‖if n_1 = n then 1 else 0‖ ^ (1 / (↑n - ↑n_1)) else 0) = 0
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: R : Type u_1
inst✝¹ : SeminormedRing R
inst✝ : Nontrivial R
n : ℕ
⊢ (⨆ n_1, if n_1 < n then ‖if n_1 = n then 1 else 0‖ ^ (1 / (↑n - ↑n_1)) else 0) = 0

Tactic:
convert! ciSup_const using 2

Goal state after:
case e'_2.e'_4
R : Type u_1
inst✝¹ : SeminormedRing R
inst✝ : Nontrivial R
n : ℕ
⊢ (fun n_1 ↦ if n_1 < n then ‖if n_1 = n then 1 else 0‖ ^ (1 / (↑n - ↑n_1)) else 0) = fun x ↦ 0

case convert_4
R : Type u_1
inst✝¹ : SeminormedRing R
inst✝ : Nontrivial R
n : ℕ
⊢ Nonempty ℕ
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
norm_sub_le : ∀ (a' : F), IsConjRoot L a a' → a ≠ a' → δ ≤ ‖a - a'‖
δpos : δ > 0
⊢ ∃ x, eval x f = 0

Tactic:
have hε : (δ / (max ‖a‖ 1)) ^ f.natDegree / (f.natDegree + 1) > 0 := by positivity

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
norm_sub_le : ∀ (a' : F), IsConjRoot L a a' → a ≠ a' → δ ≤ ‖a - a'‖
δpos : δ > 0
hε : (δ / max ‖a‖ 1) ^ f.natDegree / (↑f.natDegree + 1) > 0
⊢ ∃ x, eval x f = 0
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
norm_sub_le : ∀ (a' : F), IsConjRoot L a a' → a ≠ a' → δ ≤ ‖a - a'‖
δpos : δ > 0
hε : (δ / max ‖a‖ 1) ^ f.natDegree / (↑f.natDegree + 1) > 0
g : K[X]
gmon : g.Monic
gdeg : f.natDegree = g.natDegree
gcoeff : ∀ (n : ℕ), ‖(map (algebraMap K L) g).coeff n - f.coeff n‖ < (δ / max ‖a‖ 1) ^ f.natDegree / (↑f.natDegree + 1)
b : f.SplittingField
hb : b ∈ (map (algebraMap K L) g).aroots f.SplittingField
hab : ‖a - b‖ < (δ / max ‖a‖ 1) ^ 1 * max ‖a‖ 1
⊢ ‖a - b‖ < δ

Tactic:
simpa [mul_assoc, div_mul_cancel₀ _ (by positivity : (max ‖a‖ 1) > 0).ne'] using hab

Goal state after:
Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels

Goal state before:
pp: X Y Z : SemiNormedGrp
f : X ⟶ Y
e₁ e₂ : explicitCokernel f ⟶ Z
h : explicitCokernelπ f ≫ e₁ = explicitCokernelπ f ≫ e₂
g : Y ⟶ Z := explicitCokernelπ f ≫ e₂
⊢ e₁ = e₂

Tactic:
have w : f ≫ g = 0 := by simp [g]

Goal state after:
X Y Z : SemiNormedGrp
f : X ⟶ Y
e₁ e₂ : explicitCokernel f ⟶ Z
h : explicitCokernelπ f ≫ e₁ = explicitCokernelπ f ≫ e₂
g : Y ⟶ Z := explicitCokernelπ f ≫ e₂
w : f ≫ g = 0
⊢ e₁ = e₂
Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels

Goal state before:
pp: X Y Z : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ (explicitCokernelIso f).hom ≫ cokernel.desc f g w = explicitCokernelDesc w

Tactic:
ext1
  simp [explicitCokernelDesc, explicitCokernelπ, explicitCokernelIso,
    IsColimit.coconePointUniqueUpToIso]

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
h_fin : FiniteDimensional K L
hn : Normal K L
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
hf_na : IsNonarchimedean ⇑f
hf_ext : ∀ (x : K), f ((algebraMap K L) x) = ↑‖x‖₊
hf_iso : ∀ (σ : Gal(L/K)) (x : L), f x = f (σ x)
x : L
⊢ f x = spectralNorm K L x

Tactic:
have h_sup : (⨆ σ : Gal(L/K), f (σ x)) = f x := by
    rw [← @ciSup_const _ Gal(L/K) _ _ (f x)]
    exact iSup_congr fun σ ↦ by rw [hf_iso σ x]
  rw [spectralNorm_eq_iSup_of_finiteDimensional_normal K L hf_pm hf_na hf_ext, h_sup]

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.Finsupp

Goal state before:
pp: ι : Type u_1
X : Type u_2
inst✝² : Zero X
p : ℝ≥0
inst✝¹ : Fact (1 ≤ p)
inst✝ : PseudoMetricSpace X
f g : WithLp (↑p) (ι →₀ X)
⊢ edist f g = ENNReal.ofReal (((zipWith dist ⋯ f.ofLp g.ofLp).sum fun i r ↦ r ^ ↑p) ^ (↑p)⁻¹)

Tactic:
simp only [edist_def, sum, zipWith_apply, ← coe_nnreal_ennreal_nndist, NNReal.zero_le_coe,
        ← ENNReal.coe_rpow_of_nonneg, ← ENNReal.ofNNReal_finsetSum, inv_nonneg, ← coe_nndist,
        ← NNReal.coe_rpow, ← NNReal.coe_sum, ENNReal.ofReal_coe_nnreal, ENNReal.coe_inj]
      congr! 2
      ext i
      simp [← coe_nndist, ← coe_nnreal_ennreal_nndist]

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

Goal state before:
pp: R : Type u_1
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
x y : L
⊢ ↑(NNReal.mk ((fun x y ↦ spectralNorm K L (x - y)) x y) ⋯) = ENNReal.ofReal (spectralNorm K L (x - y))

Tactic:
rw [ENNReal.ofReal_eq_coe_nnreal]

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
hu : IsUltrametricDist K
inst✝⁵ : CompleteSpace K
x : L
E : Type u_2
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : Algebra L E
inst✝¹ : IsScalarTower K L E
inst✝ : Algebra.IsAlgebraic K E
a : E
ha : (mapAlg K E) (minpoly K x) ≠ 0 ∧ eval a ((mapAlg K E) (minpoly K x)) = 0
⊢ (aeval a) (minpoly K ((algebraMap L E) x)) = 0

Tactic:
← ha.2,

Goal state after:
K : Type u
inst✝⁸ : NontriviallyNormedField K
L : Type v
inst✝⁷ : Field L
inst✝⁶ : Algebra K L
hu : IsUltrametricDist K
inst✝⁵ : CompleteSpace K
x : L
E : Type u_2
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : Algebra L E
inst✝¹ : IsScalarTower K L E
inst✝ : Algebra.IsAlgebraic K E
a : E
ha : (mapAlg K E) (minpoly K x) ≠ 0 ∧ eval a ((mapAlg K E) (minpoly K x)) = 0
⊢ (aeval a) (minpoly K ((algebraMap L E) x)) = eval a ((mapAlg K E) (minpoly K x))
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: case pos
K : Type u
inst✝⁹ : NontriviallyNormedField K
L : Type v
inst✝⁸ : Field L
inst✝⁷ : Algebra K L
hu : IsUltrametricDist K
inst✝⁶ : CompleteSpace K
x : L
E : Type u_2
inst✝⁵ : Field E
inst✝⁴ : Algebra K E
inst✝³ : Algebra L E
inst✝² : IsScalarTower K L E
inst✝¹ : IsSplittingField L E ((mapAlg K L) (minpoly K x))
inst✝ : Algebra.IsAlgebraic K E
h_deg : (minpoly K x).natDegree = ((mapAlg K E) (minpoly K x)).roots.card
r : ℝ
hr : (spectralMulAlgNorm K E) ((algebraMap L E) x) = r
⊢ (minpoly K x).natDegree =
    Multiset.count r (Multiset.map (⇑(spectralMulAlgNorm K E)) ((mapAlg K E) (minpoly K x)).roots)

Tactic:
have h : ∀ s ∈ Multiset.map (spectralMulAlgNorm K E) ((mapAlg K E) (minpoly K x)).roots,
        r = s := by
      intro s hs
      obtain ⟨a, ha, has⟩ := Multiset.mem_map.mp hs
      rw [← hr, ← has, spectralMulAlgNorm_eq_of_mem_roots K L x ha]

Goal state after:
case pos
K : Type u
inst✝⁹ : NontriviallyNormedField K
L : Type v
inst✝⁸ : Field L
inst✝⁷ : Algebra K L
hu : IsUltrametricDist K
inst✝⁶ : CompleteSpace K
x : L
E : Type u_2
inst✝⁵ : Field E
inst✝⁴ : Algebra K E
inst✝³ : Algebra L E
inst✝² : IsScalarTower K L E
inst✝¹ : IsSplittingField L E ((mapAlg K L) (minpoly K x))
inst✝ : Algebra.IsAlgebraic K E
h_deg : (minpoly K x).natDegree = ((mapAlg K E) (minpoly K x)).roots.card
r : ℝ
hr : (spectralMulAlgNorm K E) ((algebraMap L E) x) = r
h : ∀ s ∈ Multiset.map (⇑(spectralMulAlgNorm K E)) ((mapAlg K E) (minpoly K x)).roots, r = s
⊢ (minpoly K x).natDegree =
    Multiset.count r (Multiset.map (⇑(spectralMulAlgNorm K E)) ((mapAlg K E) (minpoly K x)).roots)
Module: Mathlib.Analysis.Normed.Module.MStructure

Goal state before:
pp: X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q : M
h₁ : IsLprojection X P
h₂ : IsLprojection X Q
R : M
h₃ : IsLprojection X R
x : X
⊢ ‖R • P • R • x‖ + ‖(1 - R) • P • R • x‖ + (‖R • x - R • P • R • x‖ + ‖(1 - R) • P • R • x‖) =
    ‖R • P • R • x‖ + ‖R • x - R • P • R • x‖ + 2 • ‖(1 - R) • P • R • x‖

Tactic:
by abel

Goal state after:
Module: Mathlib.Topology.Maps.Strict.Module

Goal state before:
pp: R : Type u_1
M : Type u_3
Nₗ : Type u_5
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup Nₗ
inst✝³ : Module R M
inst✝² : Module R Nₗ
fₗ : M →ₗ[R] Nₗ
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalSpace Nₗ
⊢ IsStrictMap ⇑fₗ ↔ IsHomeomorph ⇑fₗ.quotKerEquivRange

Tactic:
simp_rw [isHomeomorph_iff_isStrictMap_bijective, EquivLike.bijective, and_true,
    fₗ.ker.isQuotientMap_mkQ.isStrictMap_iff, IsEmbedding.subtypeVal.isStrictMap_iff]

Goal state after:
R : Type u_1
M : Type u_3
Nₗ : Type u_5
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup Nₗ
inst✝³ : Module R M
inst✝² : Module R Nₗ
fₗ : M →ₗ[R] Nₗ
inst✝¹ : TopologicalSpace M
inst✝ : TopologicalSpace Nₗ
⊢ IsStrictMap ⇑fₗ ↔ IsStrictMap (Subtype.val ∘ ⇑fₗ.quotKerEquivRange ∘ ⇑fₗ.ker.mkQ)