mathlib-initiative/mathlib-tactics huggingface dataset:
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✝ : DecidableEq L
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
hf_na : IsNonarchimedean ⇑f
hf1 : f 1 = 1
p : K[X]
s : Multiset L
hp : (mapAlg K L) p = (Multiset.map (fun a ↦ X - C a) s).prod
h_le : 0 ≤ ⨆ x, if x ∈ s then f x else 0
m : ℕ
hm : m < p.natDegree
⊢ m < p.natDegree

Tactic:
;

Goal state after:
K : Type u_2
inst✝³ : NormedField K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : DecidableEq L
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
hf_na : IsNonarchimedean ⇑f
hf1 : f 1 = 1
p : K[X]
s : Multiset L
hp : (mapAlg K L) p = (Multiset.map (fun a ↦ X - C a) s).prod
h_le : 0 ≤ ⨆ x, if x ∈ s then f x else 0
m : ℕ
hm : m < p.natDegree
⊢ m < p.natDegree
Module: Mathlib.Analysis.Normed.Group.ControlledClosure

Goal state before:
pp: case hbc
G : Type u_1
inst✝² : NormedAddCommGroup G
inst✝¹ : CompleteSpace G
H : Type u_2
inst✝ : NormedAddCommGroup H
f : NormedAddGroupHom G H
K : AddSubgroup H
C ε : ℝ
hC : 0 < C
hε : 0 < ε
hyp : f.SurjectiveOnWith K C
h : H
h_in : h ∈ K.topologicalClosure
hyp_h : ¬h = 0
b : ℕ → ℝ := ⋯
b_pos : ∀ (i : ℕ), 0 < b i
v : ℕ → H
lim_v : Tendsto (fun n ↦ ∑ k ∈ range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖-v 0 + h‖ < b 0
hv : ∀ n > 0, ‖v n‖ < b n
u : ℕ → G
hu : ∀ (n : ℕ), f (u n) = v n
hnorm_u : ∀ (n : ℕ), ‖u n‖ ≤ C * ‖v n‖
s : ℕ → G := ⋯
n : ℕ
hn : n ≥ 1
⊢ ‖v n‖ ≤ b n

Tactic:
;

Goal state after:
case hbc
G : Type u_1
inst✝² : NormedAddCommGroup G
inst✝¹ : CompleteSpace G
H : Type u_2
inst✝ : NormedAddCommGroup H
f : NormedAddGroupHom G H
K : AddSubgroup H
C ε : ℝ
hC : 0 < C
hε : 0 < ε
hyp : f.SurjectiveOnWith K C
h : H
h_in : h ∈ K.topologicalClosure
hyp_h : ¬h = 0
b : ℕ → ℝ := ⋯
b_pos : ∀ (i : ℕ), 0 < b i
v : ℕ → H
lim_v : Tendsto (fun n ↦ ∑ k ∈ range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖-v 0 + h‖ < b 0
hv : ∀ n > 0, ‖v n‖ < b n
u : ℕ → G
hu : ∀ (n : ℕ), f (u n) = v n
hnorm_u : ∀ (n : ℕ), ‖u n‖ ≤ C * ‖v n‖
s : ℕ → G := ⋯
n : ℕ
hn : n ≥ 1
⊢ ‖v n‖ ≤ b n
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✝ : DecidableEq L
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
hf_na : IsNonarchimedean ⇑f
hf1 : f 1 = 1
p : K[X]
s : Multiset L
hp : (mapAlg K L) p = (Multiset.map (fun a ↦ X - C a) s).prod
h_le : 0 ≤ ⨆ x, if x ∈ s then f x else 0
m : ℕ
hm : m < p.natDegree
h✝ : 0 < ↑p.natDegree - ↑m
hps : s.card = p.natDegree
hc : ‖p.coeff m‖ = f (((mapAlg K L) p).coeff m)
h : f ((-1) ^ (s.card - m) * s.esymm (s.card - m)) = f (s.esymm (s.card - m))
t : Multiset L
ht_card : t.card = s.card - m
hts : ∀ x ∈ t, x ∈ s
ht_ge : f (Multiset.map prod (powersetCard (s.card - m) s)).sum ≤ f t.prod
h_pr : f t.prod ≤ (Multiset.map (⇑f) t).prod
⊢ 0 < s.toFinset.card

Tactic:
have hs0 : 0 < s.card := hps ▸ hm.pos

Goal state after:
K : Type u_2
inst✝³ : NormedField K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : DecidableEq L
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
hf_na : IsNonarchimedean ⇑f
hf1 : f 1 = 1
p : K[X]
s : Multiset L
hp : (mapAlg K L) p = (Multiset.map (fun a ↦ X - C a) s).prod
h_le : 0 ≤ ⨆ x, if x ∈ s then f x else 0
m : ℕ
hm : m < p.natDegree
h✝ : 0 < ↑p.natDegree - ↑m
hps : s.card = p.natDegree
hc : ‖p.coeff m‖ = f (((mapAlg K L) p).coeff m)
h : f ((-1) ^ (s.card - m) * s.esymm (s.card - m)) = f (s.esymm (s.card - m))
t : Multiset L
ht_card : t.card = s.card - m
hts : ∀ x ∈ t, x ∈ s
ht_ge : f (Multiset.map prod (powersetCard (s.card - m) s)).sum ≤ f t.prod
h_pr : f t.prod ≤ (Multiset.map (⇑f) t).prod
hs0 : 0 < s.card
⊢ 0 < s.toFinset.card
Module: Mathlib.Analysis.Normed.Group.ControlledClosure

Goal state before:
pp: G : Type u_1
inst✝² : NormedAddCommGroup G
inst✝¹ : CompleteSpace G
H : Type u_2
inst✝ : NormedAddCommGroup H
f : NormedAddGroupHom G H
K : AddSubgroup H
C ε : ℝ
hC : 0 < C
hε : 0 < ε
hyp : f.SurjectiveOnWith K C
h : H
h_in : h ∈ K.topologicalClosure
hyp_h : ¬h = 0
b : ℕ → ℝ := fun i ↦ (1 / 2) ^ i * (ε * ‖h‖ / 2) / C
b_pos : ∀ (i : ℕ), 0 < b i
v : ℕ → H
lim_v : Tendsto (fun n ↦ ∑ k ∈ range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖-v 0 + h‖ < b 0
hv : ∀ n > 0, ‖v n‖ < b n
u : ℕ → G
hu : ∀ (n : ℕ), f (u n) = v n
hnorm_u : ∀ (n : ℕ), ‖u n‖ ≤ C * ‖v n‖
s : ℕ → G := fun n ↦ ∑ k ∈ range (n + 1), u k
this : CauchySeq s
g : G
hg : Tendsto s atTop (𝓝 g)
n : ℕ
⊢ ‖h‖ + ‖-v 0 + h‖ ≤ ‖h‖ + b 0

Tactic:
;

Goal state after:
G : Type u_1
inst✝² : NormedAddCommGroup G
inst✝¹ : CompleteSpace G
H : Type u_2
inst✝ : NormedAddCommGroup H
f : NormedAddGroupHom G H
K : AddSubgroup H
C ε : ℝ
hC : 0 < C
hε : 0 < ε
hyp : f.SurjectiveOnWith K C
h : H
h_in : h ∈ K.topologicalClosure
hyp_h : ¬h = 0
b : ℕ → ℝ := fun i ↦ (1 / 2) ^ i * (ε * ‖h‖ / 2) / C
b_pos : ∀ (i : ℕ), 0 < b i
v : ℕ → H
lim_v : Tendsto (fun n ↦ ∑ k ∈ range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖-v 0 + h‖ < b 0
hv : ∀ n > 0, ‖v n‖ < b n
u : ℕ → G
hu : ∀ (n : ℕ), f (u n) = v n
hnorm_u : ∀ (n : ℕ), ‖u n‖ ≤ C * ‖v n‖
s : ℕ → G := fun n ↦ ∑ k ∈ range (n + 1), u k
this : CauchySeq s
g : G
hg : Tendsto s atTop (𝓝 g)
n : ℕ
⊢ ‖h‖ + ‖-v 0 + h‖ ≤ ‖h‖ + b 0
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✝ : DecidableEq L
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
hf_na : IsNonarchimedean ⇑f
hf1 : f 1 = 1
p : K[X]
s : Multiset L
hp : (mapAlg K L) p = (Multiset.map (fun a ↦ X - C a) s).prod
h_le : 0 ≤ ⨆ x, if x ∈ s then f x else 0
m : ℕ
hm : m < p.natDegree
h✝ : 0 < ↑p.natDegree - ↑m
hps : s.card = p.natDegree
hc : ‖p.coeff m‖ = f (((mapAlg K L) p).coeff m)
h : f ((-1) ^ (s.card - m) * s.esymm (s.card - m)) = f (s.esymm (s.card - m))
t : Multiset L
ht_card : t.card = s.card - m
hts : ∀ x ∈ t, x ∈ s
ht_ge : f (Multiset.map prod (powersetCard (s.card - m) s)).sum ≤ f t.prod
h_pr : f t.prod ≤ (Multiset.map (⇑f) t).prod
hs_ne : s ≠ 0
y : L
hyx : y ∈ s
hy_max : ∀ z ∈ s, f z ≤ f y
g : L → NNReal := fun x ↦ ⟨f x, ⋯⟩
h_card : p.natDegree - m = (Multiset.map g t).card
⊢ ∀ x ∈ Multiset.map g t, x ≤ g y

Tactic:
intro r

Goal state after:
K : Type u_2
inst✝³ : NormedField K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : DecidableEq L
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
hf_na : IsNonarchimedean ⇑f
hf1 : f 1 = 1
p : K[X]
s : Multiset L
hp : (mapAlg K L) p = (Multiset.map (fun a ↦ X - C a) s).prod
h_le : 0 ≤ ⨆ x, if x ∈ s then f x else 0
m : ℕ
hm : m < p.natDegree
h✝ : 0 < ↑p.natDegree - ↑m
hps : s.card = p.natDegree
hc : ‖p.coeff m‖ = f (((mapAlg K L) p).coeff m)
h : f ((-1) ^ (s.card - m) * s.esymm (s.card - m)) = f (s.esymm (s.card - m))
t : Multiset L
ht_card : t.card = s.card - m
hts : ∀ x ∈ t, x ∈ s
ht_ge : f (Multiset.map prod (powersetCard (s.card - m) s)).sum ≤ f t.prod
h_pr : f t.prod ≤ (Multiset.map (⇑f) t).prod
hs_ne : s ≠ 0
y : L
hyx : y ∈ s
hy_max : ∀ z ∈ s, f z ≤ f y
g : L → NNReal := fun x ↦ ⟨f x, ⋯⟩
h_card : p.natDegree - m = (Multiset.map g t).card
r : NNReal
⊢ r ∈ Multiset.map g t → r ≤ g y
Module: Mathlib.Analysis.Normed.Group.ControlledClosure

Goal state before:
pp: case hbc
G : Type u_1
inst✝² : NormedAddCommGroup G
inst✝¹ : CompleteSpace G
H : Type u_2
inst✝ : NormedAddCommGroup H
f : NormedAddGroupHom G H
K : AddSubgroup H
C ε : ℝ
hC : 0 < C
hε : 0 < ε
hyp : f.SurjectiveOnWith K C
h : H
h_in : h ∈ K.topologicalClosure
hyp_h : ¬h = 0
b : ℕ → ℝ := ⋯
b_pos : ∀ (i : ℕ), 0 < b i
v : ℕ → H
lim_v : Tendsto (fun n ↦ ∑ k ∈ range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖-v 0 + h‖ < b 0
hv : ∀ n > 0, ‖v n‖ < b n
u : ℕ → G
hu : ∀ (n : ℕ), f (u n) = v n
hnorm_u : ∀ (n : ℕ), ‖u n‖ ≤ C * ‖v n‖
s : ℕ → G := ⋯
this : CauchySeq s
g : G
hg : Tendsto s atTop (𝓝 g)
n : ℕ
hnorm₀ : ‖u 0‖ ≤ C * b 0 + C * ‖h‖
⊢ ∑ k ∈ range (n + 1), (1 / 2) ^ k ≤ 2

Tactic:
;

Goal state after:
case hbc
G : Type u_1
inst✝² : NormedAddCommGroup G
inst✝¹ : CompleteSpace G
H : Type u_2
inst✝ : NormedAddCommGroup H
f : NormedAddGroupHom G H
K : AddSubgroup H
C ε : ℝ
hC : 0 < C
hε : 0 < ε
hyp : f.SurjectiveOnWith K C
h : H
h_in : h ∈ K.topologicalClosure
hyp_h : ¬h = 0
b : ℕ → ℝ := ⋯
b_pos : ∀ (i : ℕ), 0 < b i
v : ℕ → H
lim_v : Tendsto (fun n ↦ ∑ k ∈ range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖-v 0 + h‖ < b 0
hv : ∀ n > 0, ‖v n‖ < b n
u : ℕ → G
hu : ∀ (n : ℕ), f (u n) = v n
hnorm_u : ∀ (n : ℕ), ‖u n‖ ≤ C * ‖v n‖
s : ℕ → G := ⋯
this : CauchySeq s
g : G
hg : Tendsto s atTop (𝓝 g)
n : ℕ
hnorm₀ : ‖u 0‖ ≤ C * b 0 + C * ‖h‖
⊢ ∑ k ∈ range (n + 1), (1 / 2) ^ k ≤ 2
Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: case h
K : Type u_2
inst✝³ : NormedField K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : DecidableEq L
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
hf_na : IsNonarchimedean ⇑f
hf1 : f 1 = 1
p : K[X]
s : Multiset L
hp : (mapAlg K L) p = (Multiset.map (fun a ↦ X - C a) s).prod
h_le : 0 ≤ ⨆ x, if x ∈ s then f x else 0
m : ℕ
hm : m < p.natDegree
h✝ : 0 < ↑p.natDegree - ↑m
hps : s.card = p.natDegree
hc : ‖p.coeff m‖ = f (((mapAlg K L) p).coeff m)
h : f ((-1) ^ (s.card - m) * s.esymm (s.card - m)) = f (s.esymm (s.card - m))
t : Multiset L
ht_card : t.card = s.card - m
hts : ∀ x ∈ t, x ∈ s
ht_ge : f (Multiset.map prod (powersetCard (s.card - m) s)).sum ≤ f t.prod
h_pr : f t.prod ≤ (Multiset.map (⇑f) t).prod
hs_ne : s ≠ 0
y : L
hyx : y ∈ s
hy_max : ∀ z ∈ s, f z ≤ f y
this : (Multiset.map (⇑f) t).prod ≤ f y ^ (p.natDegree - m)
⊢ f y ∈ upperBounds (Set.range fun x ↦ if x ∈ s then f x else 0)

Tactic:
intro r

Goal state after:
case h
K : Type u_2
inst✝³ : NormedField K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : DecidableEq L
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
hf_na : IsNonarchimedean ⇑f
hf1 : f 1 = 1
p : K[X]
s : Multiset L
hp : (mapAlg K L) p = (Multiset.map (fun a ↦ X - C a) s).prod
h_le : 0 ≤ ⨆ x, if x ∈ s then f x else 0
m : ℕ
hm : m < p.natDegree
h✝ : 0 < ↑p.natDegree - ↑m
hps : s.card = p.natDegree
hc : ‖p.coeff m‖ = f (((mapAlg K L) p).coeff m)
h : f ((-1) ^ (s.card - m) * s.esymm (s.card - m)) = f (s.esymm (s.card - m))
t : Multiset L
ht_card : t.card = s.card - m
hts : ∀ x ∈ t, x ∈ s
ht_ge : f (Multiset.map prod (powersetCard (s.card - m) s)).sum ≤ f t.prod
h_pr : f t.prod ≤ (Multiset.map (⇑f) t).prod
hs_ne : s ≠ 0
y : L
hyx : y ∈ s
hy_max : ∀ z ∈ s, f z ≤ f y
this : (Multiset.map (⇑f) t).prod ≤ f y ^ (p.natDegree - m)
r : ℝ
⊢ (r ∈ Set.range fun x ↦ if x ∈ s then f x else 0) → r ≤ f y
Module: Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
hna : IsNonarchimedean ⇑μ
x y : R
hn : ∀ (n : ℕ), ∃ m < n + 1, μ ((x + y) ^ n) ^ (1 / ↑n) ≤ (μ (x ^ m) * μ (y ^ (n - m))) ^ (1 / ↑n)
mu : ℕ → ℕ := fun n ↦ _root_.mu μ hn n
nu : ℕ → ℕ := fun n ↦ n - mu n
hnu : nu = fun n ↦ n - mu n
hmu_le : ∀ (n : ℕ), mu n ≤ n
hmu_bdd : ∀ (n : ℕ), ↑(mu n) / ↑n ∈ Set.Icc 0 1
hs : Bornology.IsBounded (Set.Icc 0 1)
a : ℝ
a_in : a ∈ closure (Set.Icc 0 1)
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun n ↦ ↑(mu n) / ↑n) ∘ ψ) atTop (𝓝 a)
⊢ smoothingFun μ (x + y) ≤ max (smoothingFun μ x) (smoothingFun μ y)

Tactic:
closure_Icc

Goal state after:
R : Type u_1
inst✝ : CommRing R
μ : RingSeminorm R
hμ1 : μ 1 ≤ 1
hna : IsNonarchimedean ⇑μ
x y : R
hn : ∀ (n : ℕ), ∃ m < n + 1, μ ((x + y) ^ n) ^ (1 / ↑n) ≤ (μ (x ^ m) * μ (y ^ (n - m))) ^ (1 / ↑n)
mu : ℕ → ℕ := fun n ↦ _root_.mu μ hn n
nu : ℕ → ℕ := fun n ↦ n - mu n
hnu : nu = fun n ↦ n - mu n
hmu_le : ∀ (n : ℕ), mu n ≤ n
hmu_bdd : ∀ (n : ℕ), ↑(mu n) / ↑n ∈ Set.Icc 0 1
hs : Bornology.IsBounded (Set.Icc 0 1)
a : ℝ
a_in : a ∈ Set.Icc 0 1
ψ : ℕ → ℕ
hψ_mono : StrictMono ψ
hψ_lim : Tendsto ((fun n ↦ ↑(mu n) / ↑n) ∘ ψ) atTop (𝓝 a)
⊢ smoothingFun μ (x + y) ≤ max (smoothingFun μ x) (smoothingFun μ y)
Module: Mathlib.Analysis.Normed.Group.ControlledClosure

Goal state before:
pp: case h
G : Type u_1
inst✝² : NormedAddCommGroup G
inst✝¹ : CompleteSpace G
H : Type u_2
inst✝ : NormedAddCommGroup H
f : NormedAddGroupHom G H
K : AddSubgroup H
C ε : ℝ
hC : 0 < C
hε : 0 < ε
hyp : f.SurjectiveOnWith K C
h : H
h_in : h ∈ K.topologicalClosure
hyp_h : ¬h = 0
b : ℕ → ℝ := fun i ↦ (1 / 2) ^ i * (ε * ‖h‖ / 2) / C
b_pos : ∀ (i : ℕ), 0 < b i
v : ℕ → H
lim_v : Tendsto (fun n ↦ ∑ k ∈ range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖-v 0 + h‖ < b 0
hv : ∀ n > 0, ‖v n‖ < b n
u : ℕ → G
hu : ∀ (n : ℕ), f (u n) = v n
hnorm_u : ∀ (n : ℕ), ‖u n‖ ≤ C * ‖v n‖
s : ℕ → G := fun n ↦ ∑ k ∈ range (n + 1), u k
this✝ : CauchySeq s
g : G
hg : Tendsto s atTop (𝓝 g)
n : ℕ
hnorm₀ : ‖u 0‖ ≤ C * b 0 + C * ‖h‖
this : ∑ k ∈ range (n + 1), C * b k ≤ ε * ‖h‖
k : ℕ
a✝ : k ∈ range n
⊢ ‖u (k + 1)‖ ≤ C * ‖v (k + 1)‖

Tactic:
;

Goal state after:
case h
G : Type u_1
inst✝² : NormedAddCommGroup G
inst✝¹ : CompleteSpace G
H : Type u_2
inst✝ : NormedAddCommGroup H
f : NormedAddGroupHom G H
K : AddSubgroup H
C ε : ℝ
hC : 0 < C
hε : 0 < ε
hyp : f.SurjectiveOnWith K C
h : H
h_in : h ∈ K.topologicalClosure
hyp_h : ¬h = 0
b : ℕ → ℝ := fun i ↦ (1 / 2) ^ i * (ε * ‖h‖ / 2) / C
b_pos : ∀ (i : ℕ), 0 < b i
v : ℕ → H
lim_v : Tendsto (fun n ↦ ∑ k ∈ range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖-v 0 + h‖ < b 0
hv : ∀ n > 0, ‖v n‖ < b n
u : ℕ → G
hu : ∀ (n : ℕ), f (u n) = v n
hnorm_u : ∀ (n : ℕ), ‖u n‖ ≤ C * ‖v n‖
s : ℕ → G := fun n ↦ ∑ k ∈ range (n + 1), u k
this✝ : CauchySeq s
g : G
hg : Tendsto s atTop (𝓝 g)
n : ℕ
hnorm₀ : ‖u 0‖ ≤ C * b 0 + C * ‖h‖
this : ∑ k ∈ range (n + 1), C * b k ≤ ε * ‖h‖
k : ℕ
a✝ : k ∈ range n
⊢ ‖u (k + 1)‖ ≤ C * ‖v (k + 1)‖
Module: Mathlib.Analysis.Normed.Group.ControlledClosure

Goal state before:
pp: case hbc
G : Type u_1
inst✝² : NormedAddCommGroup G
inst✝¹ : CompleteSpace G
H : Type u_2
inst✝ : NormedAddCommGroup H
f : NormedAddGroupHom G H
K : AddSubgroup H
C ε : ℝ
hC : 0 < C
hε : 0 < ε
hyp : f.SurjectiveOnWith K C
h : H
h_in : h ∈ K.topologicalClosure
hyp_h : ¬h = 0
b : ℕ → ℝ := ⋯
b_pos : ∀ (i : ℕ), 0 < b i
v : ℕ → H
lim_v : Tendsto (fun n ↦ ∑ k ∈ range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖-v 0 + h‖ < b 0
hv : ∀ n > 0, ‖v n‖ < b n
u : ℕ → G
hu : ∀ (n : ℕ), f (u n) = v n
hnorm_u : ∀ (n : ℕ), ‖u n‖ ≤ C * ‖v n‖
s : ℕ → G := ⋯
this✝ : CauchySeq s
g : G
hg : Tendsto s atTop (𝓝 g)
n : ℕ
hnorm₀ : ‖u 0‖ ≤ C * b 0 + C * ‖h‖
this : ∑ k ∈ range (n + 1), C * b k ≤ ε * ‖h‖
k : ℕ
a✝ : k ∈ range n
⊢ ‖v (k + 1)‖ ≤ b (k + 1)

Tactic:
;

Goal state after:
case hbc
G : Type u_1
inst✝² : NormedAddCommGroup G
inst✝¹ : CompleteSpace G
H : Type u_2
inst✝ : NormedAddCommGroup H
f : NormedAddGroupHom G H
K : AddSubgroup H
C ε : ℝ
hC : 0 < C
hε : 0 < ε
hyp : f.SurjectiveOnWith K C
h : H
h_in : h ∈ K.topologicalClosure
hyp_h : ¬h = 0
b : ℕ → ℝ := ⋯
b_pos : ∀ (i : ℕ), 0 < b i
v : ℕ → H
lim_v : Tendsto (fun n ↦ ∑ k ∈ range (n + 1), v k) atTop (𝓝 h)
v_in : ∀ (n : ℕ), v n ∈ K
hv₀ : ‖-v 0 + h‖ < b 0
hv : ∀ n > 0, ‖v n‖ < b n
u : ℕ → G
hu : ∀ (n : ℕ), f (u n) = v n
hnorm_u : ∀ (n : ℕ), ‖u n‖ ≤ C * ‖v n‖
s : ℕ → G := ⋯
this✝ : CauchySeq s
g : G
hg : Tendsto s atTop (𝓝 g)
n : ℕ
hnorm₀ : ‖u 0‖ ≤ C * b 0 + C * ‖h‖
this : ∑ k ∈ range (n + 1), C * b k ≤ ε * ‖h‖
k : ℕ
a✝ : k ∈ range n
⊢ ‖v (k + 1)‖ ≤ b (k + 1)
Module: Mathlib.Analysis.Normed.Group.HomCompletion

Goal state before:
pp: G : Type u_1
inst✝² : SeminormedAddCommGroup G
H : Type u_2
inst✝¹ : SeminormedAddCommGroup H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
f : NormedAddGroupHom G H
g : NormedAddGroupHom H K
x : Completion G
⊢ (Completion.map ⇑g ∘ Completion.map ⇑f) x = Completion.map (⇑(g.comp f)) x

Tactic:
Completion.map_comp g.uniformContinuous f.uniformContinuous

Goal state after:
G : Type u_1
inst✝² : SeminormedAddCommGroup G
H : Type u_2
inst✝¹ : SeminormedAddCommGroup H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
f : NormedAddGroupHom G H
g : NormedAddGroupHom H K
x : Completion G
⊢ Completion.map (⇑g ∘ ⇑f) x = Completion.map (⇑(g.comp f)) x
Module: Mathlib.Analysis.Normed.Group.HomCompletion

Goal state before:
pp: G : Type u_1
inst✝¹ : SeminormedAddCommGroup G
H : Type u_2
inst✝ : SeminormedAddCommGroup H
f : NormedAddGroupHom G H
x : G
⊢ (f.completion.comp toCompl) x = (toCompl.comp f) x

Tactic:
;

Goal state after:
G : Type u_1
inst✝¹ : SeminormedAddCommGroup G
H : Type u_2
inst✝ : SeminormedAddCommGroup H
f : NormedAddGroupHom G H
x : G
⊢ (f.completion.comp toCompl) x = (toCompl.comp f) x
Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp

Goal state before:
pp: case refine_1
V : SemiNormedGrp
inst✝ : Subsingleton V.carrier
X : SemiNormedGrp
f : V ⟶ X
x : V.carrier
⊢ (Hom.hom f) x = (Hom.hom default) x

Tactic:
;

Goal state after:
case refine_1
V : SemiNormedGrp
inst✝ : Subsingleton V.carrier
X : SemiNormedGrp
f : V ⟶ X
x : V.carrier
⊢ (Hom.hom f) x = (Hom.hom default) x
Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp

Goal state before:
pp: case refine_1
V : SemiNormedGrp
inst✝ : Subsingleton V.carrier
X : SemiNormedGrp
f : V ⟶ X
x : V.carrier
this : x = 0
⊢ (Hom.hom f) x = (Hom.hom default) x

Tactic:
;

Goal state after:
case refine_1
V : SemiNormedGrp
inst✝ : Subsingleton V.carrier
X : SemiNormedGrp
f : V ⟶ X
x : V.carrier
this : x = 0
⊢ (Hom.hom f) x = (Hom.hom default) x
Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp

Goal state before:
pp: case refine_2
V : SemiNormedGrp
inst✝ : Subsingleton V.carrier
X : SemiNormedGrp
f : X ⟶ V
x✝ : X.carrier
⊢ (Hom.hom f) x✝ = (Hom.hom default) x✝

Tactic:
;

Goal state after:
case refine_2
V : SemiNormedGrp
inst✝ : Subsingleton V.carrier
X : SemiNormedGrp
f : X ⟶ V
x✝ : X.carrier
⊢ (Hom.hom f) x✝ = (Hom.hom default) x✝
Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp

Goal state before:
pp: case refine_1
V : SemiNormedGrp₁
inst✝ : Subsingleton V.carrier
X : SemiNormedGrp₁
f : V ⟶ X
x : V.carrier
⊢ ↑(Hom.hom f) x = ↑(Hom.hom default) x

Tactic:
;

Goal state after:
case refine_1
V : SemiNormedGrp₁
inst✝ : Subsingleton V.carrier
X : SemiNormedGrp₁
f : V ⟶ X
x : V.carrier
⊢ ↑(Hom.hom f) x = ↑(Hom.hom default) x
Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp

Goal state before:
pp: case refine_1
V : SemiNormedGrp₁
inst✝ : Subsingleton V.carrier
X : SemiNormedGrp₁
f : V ⟶ X
x : V.carrier
this : x = 0
⊢ ↑(Hom.hom f) x = ↑(Hom.hom default) x

Tactic:
;

Goal state after:
case refine_1
V : SemiNormedGrp₁
inst✝ : Subsingleton V.carrier
X : SemiNormedGrp₁
f : V ⟶ X
x : V.carrier
this : x = 0
⊢ ↑(Hom.hom f) x = ↑(Hom.hom default) x
Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp

Goal state before:
pp: case refine_2
V : SemiNormedGrp₁
inst✝ : Subsingleton V.carrier
X : SemiNormedGrp₁
f : X ⟶ V
x✝ : X.carrier
⊢ ↑(Hom.hom f) x✝ = ↑(Hom.hom default) x✝

Tactic:
;

Goal state after:
case refine_2
V : SemiNormedGrp₁
inst✝ : Subsingleton V.carrier
X : SemiNormedGrp₁
f : X ⟶ V
x✝ : X.carrier
⊢ ↑(Hom.hom f) x✝ = ↑(Hom.hom default) x✝
Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels

Goal state before:
pp: X Y : SemiNormedGrp₁
f : X ⟶ Y
x : X.carrier
⊢ (↑(Hom.hom f)).range.normedMk (↑(Hom.hom f) x) = ↑(Hom.hom 0) x

Tactic:
SemiNormedGrp₁.zero_apply,

Goal state after:
X Y : SemiNormedGrp₁
f : X ⟶ Y
x : X.carrier
⊢ (↑(Hom.hom f)).range.normedMk (↑(Hom.hom f) x) = 0
Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels

Goal state before:
pp: V W : SemiNormedGrp
f g✝ : V ⟶ W
this : ∀ (c : Fork f g✝), (NormedAddGroupHom.compHom (Hom.hom (f - g✝))) (Hom.hom c.ι) = 0
c : Fork f g✝
g : c.pt ⟶ (fork f g✝).pt
h : g ≫ (fork f g✝).ι = c.ι
x : c.pt.carrier
⊢ (Hom.hom g) x = (Hom.hom (ofHom (NormedAddGroupHom.ker.lift (Hom.hom c.ι) (Hom.hom (f - g✝)) ⋯))) x

Tactic:
;

Goal state after:
V W : SemiNormedGrp
f g✝ : V ⟶ W
this : ∀ (c : Fork f g✝), (NormedAddGroupHom.compHom (Hom.hom (f - g✝))) (Hom.hom c.ι) = 0
c : Fork f g✝
g : c.pt ⟶ (fork f g✝).pt
h : g ≫ (fork f g✝).ι = c.ι
x : c.pt.carrier
⊢ (Hom.hom g) x = (Hom.hom (ofHom (NormedAddGroupHom.ker.lift (Hom.hom c.ι) (Hom.hom (f - g✝)) ⋯))) x
Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels

Goal state before:
pp: V W : SemiNormedGrp
f g✝ : V ⟶ W
this : ∀ (c : Fork f g✝), (NormedAddGroupHom.compHom (Hom.hom (f - g✝))) (Hom.hom c.ι) = 0
c : Fork f g✝
g : c.pt ⟶ (fork f g✝).pt
h : g ≫ (fork f g✝).ι = c.ι
x : c.pt.carrier
⊢ (Hom.hom g) x = (Hom.hom (ofHom (NormedAddGroupHom.ker.lift (Hom.hom c.ι) (Hom.hom f - Hom.hom g✝) ⋯))) x

Tactic:
;

Goal state after:
V W : SemiNormedGrp
f g✝ : V ⟶ W
this : ∀ (c : Fork f g✝), (NormedAddGroupHom.compHom (Hom.hom (f - g✝))) (Hom.hom c.ι) = 0
c : Fork f g✝
g : c.pt ⟶ (fork f g✝).pt
h : g ≫ (fork f g✝).ι = c.ι
x : c.pt.carrier
⊢ (Hom.hom g) x = (Hom.hom (ofHom (NormedAddGroupHom.ker.lift (Hom.hom c.ι) (Hom.hom f - Hom.hom g✝) ⋯))) x
Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels

Goal state before:
pp: V W : SemiNormedGrp
f g✝ : V ⟶ W
this : ∀ (c : Fork f g✝), (NormedAddGroupHom.compHom (Hom.hom (f - g✝))) (Hom.hom c.ι) = 0
c : Fork f g✝
g : c.pt ⟶ (fork f g✝).pt
h : g ≫ (fork f g✝).ι = c.ι
x : c.pt.carrier
⊢ (Hom.hom g) x =
    (Hom.hom (ofHom (NormedAddGroupHom.ker.lift (Hom.hom (g ≫ (fork f g✝).ι)) (Hom.hom f - Hom.hom g✝) ⋯))) x

Tactic:
;

Goal state after:
V W : SemiNormedGrp
f g✝ : V ⟶ W
this : ∀ (c : Fork f g✝), (NormedAddGroupHom.compHom (Hom.hom (f - g✝))) (Hom.hom c.ι) = 0
c : Fork f g✝
g : c.pt ⟶ (fork f g✝).pt
h : g ≫ (fork f g✝).ι = c.ι
x : c.pt.carrier
⊢ (Hom.hom g) x =
    (Hom.hom (ofHom (NormedAddGroupHom.ker.lift (Hom.hom (g ≫ (fork f g✝).ι)) (Hom.hom f - Hom.hom g✝) ⋯))) x
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‖
x : L
hf1 : f 1 = 1
p : K[X] := minpoly K x
hp_sp : (Polynomial.map (algebraMap K L) (minpoly K x)).Splits
s : Multiset L
hs :
  Polynomial.map (algebraMap K L) (minpoly K x) =
    C (Polynomial.map (algebraMap K L) (minpoly K x)).leadingCoeff * (Multiset.map (fun x ↦ X - C x) s).prod
⊢ spectralNorm K L x ≤ ⨆ σ, f (σ x)

Tactic:
have h_lc : (algebraMap K L) (minpoly K x).leadingCoeff = 1 := by
      rw [minpoly.monic (hn.isIntegral x), map_one]

Goal state after:
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‖
x : L
hf1 : f 1 = 1
p : K[X] := minpoly K x
hp_sp : (Polynomial.map (algebraMap K L) (minpoly K x)).Splits
s : Multiset L
hs :
  Polynomial.map (algebraMap K L) (minpoly K x) =
    C (Polynomial.map (algebraMap K L) (minpoly K x)).leadingCoeff * (Multiset.map (fun x ↦ X - C x) s).prod
h_lc : (algebraMap K L) (minpoly K x).leadingCoeff = 1
⊢ spectralNorm K L x ≤ ⨆ σ, f (σ x)
Module: Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels

Goal state before:
pp: X Y : SemiNormedGrp
f : X ⟶ Y
x : X.carrier
⊢ (ConcreteCategory.hom 0) x = 0

Tactic:
;

Goal state after:
X Y : SemiNormedGrp
f : X ⟶ Y
x : X.carrier
⊢ (ConcreteCategory.hom 0) x = 0
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 := ⋯
w : f ≫ g = 0
⊢ explicitCokernelπ f ≫ e₂ = g

Tactic:
;

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 := ⋯
w : f ≫ g = 0
⊢ explicitCokernelπ f ≫ e₂ = g
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), (invariantExtension K L) (r + s) ≤ (invariantExtension K L) r + (invariantExtension K L) s

Tactic:
;

Goal state after:
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), (invariantExtension K L) (r + s) ≤ (invariantExtension K L) r + (invariantExtension K L) s