V : Type ?u.213712
V₁ : Type u_1
V₂ : Type u_2
V₃ : Type ?u.213721
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f✝ g f : NormedAddGroupHom V₁ V₂
K : AddSubgroup V₂
C C' : ℝ
h : SurjectiveOnWith f K C
H : C ≤ C'
k : V₂
k_in : k ∈ K
⊢ ∃ g, ↑f g = k ∧ ‖g‖ ≤ C' * ‖k‖
V : Type ?u.213712
V₁ : Type u_1
V₂ : Type u_2
V₃ : Type ?u.213721
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f✝ g f : NormedAddGroupHom V₁ V₂
K : AddSubgroup V₂
C C' : ℝ
h : SurjectiveOnWith f K C
H : C ≤ C'
⊢ SurjectiveOnWith f K C'
intro k k_in
case intro.intro
V : Type ?u.213712
V₁ : Type u_1
V₂ : Type u_2
V₃ : Type ?u.213721
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f✝ g✝ f : NormedAddGroupHom V₁ V₂
K : AddSubgroup V₂
C C' : ℝ
h : SurjectiveOnWith f K C
H : C ≤ C'
g : V₁
k_in : ↑f g ∈ K
hg : ‖g‖ ≤ C * ‖↑f g‖
⊢ ∃ g_1, ↑f g_1 = ↑f g ∧ ‖g_1‖ ≤ C' * ‖↑f g‖
V : Type ?u.213712
V₁ : Type u_1
V₂ : Type u_2
V₃ : Type ?u.213721
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f✝ g f : NormedAddGroupHom V₁ V₂
K : AddSubgroup V₂
C C' : ℝ
h : SurjectiveOnWith f K C
H : C ≤ C'
k : V₂
k_in : k ∈ K
⊢ ∃ g, ↑f g = k ∧ ‖g‖ ≤ C' * ‖k‖
rcases h k k_in with ⟨g, rfl, hg⟩
case intro.intro
V : Type ?u.213712
V₁ : Type u_1
V₂ : Type u_2
V₃ : Type ?u.213721
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f✝ g✝ f : NormedAddGroupHom V₁ V₂
K : AddSubgroup V₂
C C' : ℝ
h : SurjectiveOnWith f K C
H : C ≤ C'
g : V₁
k_in : ↑f g ∈ K
hg : ‖g‖ ≤ C * ‖↑f g‖
⊢ ‖g‖ ≤ C' * ‖↑f g‖
case intro.intro
V : Type ?u.213712
V₁ : Type u_1
V₂ : Type u_2
V₃ : Type ?u.213721
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f✝ g✝ f : NormedAddGroupHom V₁ V₂
K : AddSubgroup V₂
C C' : ℝ
h : SurjectiveOnWith f K C
H : C ≤ C'
g : V₁
k_in : ↑f g ∈ K
hg : ‖g‖ ≤ C * ‖↑f g‖
⊢ ∃ g_1, ↑f g_1 = ↑f g ∧ ‖g_1‖ ≤ C' * ‖↑f g‖
use g, rfl
case pos
V : Type ?u.213712
V₁ : Type u_1
V₂ : Type u_2
V₃ : Type ?u.213721
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f✝ g✝ f : NormedAddGroupHom V₁ V₂
K : AddSubgroup V₂
C C' : ℝ
h : SurjectiveOnWith f K C
H : C ≤ C'
g : V₁
k_in : ↑f g ∈ K
hg : ‖g‖ ≤ C * ‖↑f g‖
Hg : ‖↑f g‖ = 0
⊢ ‖g‖ ≤ C' * ‖↑f g‖

case neg
V : Type ?u.213712
V₁ : Type u_1
V₂ : Type u_2
V₃ : Type ?u.213721
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f✝ g✝ f : NormedAddGroupHom V₁ V₂
K : AddSubgroup V₂
C C' : ℝ
h : SurjectiveOnWith f K C
H : C ≤ C'
g : V₁
k_in : ↑f g ∈ K
hg : ‖g‖ ≤ C * ‖↑f g‖
Hg : ¬‖↑f g‖ = 0
⊢ ‖g‖ ≤ C' * ‖↑f g‖
case intro.intro
V : Type ?u.213712
V₁ : Type u_1
V₂ : Type u_2
V₃ : Type ?u.213721
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f✝ g✝ f : NormedAddGroupHom V₁ V₂
K : AddSubgroup V₂
C C' : ℝ
h : SurjectiveOnWith f K C
H : C ≤ C'
g : V₁
k_in : ↑f g ∈ K
hg : ‖g‖ ≤ C * ‖↑f g‖
⊢ ‖g‖ ≤ C' * ‖↑f g‖
by_cases Hg : ‖f g‖ = 0
no goals
case pos
V : Type ?u.213712
V₁ : Type u_1
V₂ : Type u_2
V₃ : Type ?u.213721
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f✝ g✝ f : NormedAddGroupHom V₁ V₂
K : AddSubgroup V₂
C C' : ℝ
h : SurjectiveOnWith f K C
H : C ≤ C'
g : V₁
k_in : ↑f g ∈ K
hg : ‖g‖ ≤ C * ‖↑f g‖
Hg : ‖↑f g‖ = 0
⊢ ‖g‖ ≤ C' * ‖↑f g‖
simpa [Hg] using hg
no goals
case neg
V : Type ?u.213712
V₁ : Type u_1
V₂ : Type u_2
V₃ : Type ?u.213721
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f✝ g✝ f : NormedAddGroupHom V₁ V₂
K : AddSubgroup V₂
C C' : ℝ
h : SurjectiveOnWith f K C
H : C ≤ C'
g : V₁
k_in : ↑f g ∈ K
hg : ‖g‖ ≤ C * ‖↑f g‖
Hg : ¬‖↑f g‖ = 0
⊢ ‖g‖ ≤ C' * ‖↑f g‖
exact hg.trans (by gcongr)
no goals
V : Type ?u.213712
V₁ : Type u_1
V₂ : Type u_2
V₃ : Type ?u.213721
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f✝ g✝ f : NormedAddGroupHom V₁ V₂
K : AddSubgroup V₂
C C' : ℝ
h : SurjectiveOnWith f K C
H : C ≤ C'
g : V₁
k_in : ↑f g ∈ K
hg : ‖g‖ ≤ C * ‖↑f g‖
Hg : ¬‖↑f g‖ = 0
⊢ C * ‖↑f g‖ ≤ C' * ‖↑f g‖
gcongr