case hyp
G : Type u_1
inst✝³ : NormedAddCommGroup G
inst✝² : CompleteSpace G
H : Type u_2
inst✝¹ : NormedAddCommGroup H
f : NormedAddGroupHom G H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
j : NormedAddGroupHom K H
hj : ∀ (x : K), ‖↑j x‖ = ‖x‖
C ε : ℝ
hC : 0 < C
hε : 0 < ε
hyp : ∀ (k : K), ∃ g, ↑f g = ↑j k ∧ ‖g‖ ≤ C * ‖k‖
⊢ ∀ (h : H), h ∈ NormedAddGroupHom.range j → ∃ g, ↑f g = h ∧ ‖g‖ ≤ C * ‖h‖

G : Type u_1
inst✝³ : NormedAddCommGroup G
inst✝² : CompleteSpace G
H : Type u_2
inst✝¹ : NormedAddCommGroup H
f : NormedAddGroupHom G H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
j : NormedAddGroupHom K H
hj : ∀ (x : K), ‖↑j x‖ = ‖x‖
C ε : ℝ
hC : 0 < C
hε : 0 < ε
hyp : ∀ (h : H), h ∈ NormedAddGroupHom.range j → ∃ g, ↑f g = h ∧ ‖g‖ ≤ C * ‖h‖
⊢ NormedAddGroupHom.SurjectiveOnWith f (AddSubgroup.topologicalClosure (NormedAddGroupHom.range j)) (C + ε)
G : Type u_1
inst✝³ : NormedAddCommGroup G
inst✝² : CompleteSpace G
H : Type u_2
inst✝¹ : NormedAddCommGroup H
f : NormedAddGroupHom G H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
j : NormedAddGroupHom K H
hj : ∀ (x : K), ‖↑j x‖ = ‖x‖
C ε : ℝ
hC : 0 < C
hε : 0 < ε
hyp : ∀ (k : K), ∃ g, ↑f g = ↑j k ∧ ‖g‖ ≤ C * ‖k‖
⊢ NormedAddGroupHom.SurjectiveOnWith f (AddSubgroup.topologicalClosure (NormedAddGroupHom.range j)) (C + ε)
replace hyp : ∀ h ∈ j.range, ∃ g, f g = h ∧ ‖g‖ ≤ C * ‖h‖
no goals
G : Type u_1
inst✝³ : NormedAddCommGroup G
inst✝² : CompleteSpace G
H : Type u_2
inst✝¹ : NormedAddCommGroup H
f : NormedAddGroupHom G H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
j : NormedAddGroupHom K H
hj : ∀ (x : K), ‖↑j x‖ = ‖x‖
C ε : ℝ
hC : 0 < C
hε : 0 < ε
hyp : ∀ (h : H), h ∈ NormedAddGroupHom.range j → ∃ g, ↑f g = h ∧ ‖g‖ ≤ C * ‖h‖
⊢ NormedAddGroupHom.SurjectiveOnWith f (AddSubgroup.topologicalClosure (NormedAddGroupHom.range j)) (C + ε)
exact controlled_closure_of_complete hC hε hyp
case hyp
G : Type u_1
inst✝³ : NormedAddCommGroup G
inst✝² : CompleteSpace G
H : Type u_2
inst✝¹ : NormedAddCommGroup H
f : NormedAddGroupHom G H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
j : NormedAddGroupHom K H
hj : ∀ (x : K), ‖↑j x‖ = ‖x‖
C ε : ℝ
hC : 0 < C
hε : 0 < ε
hyp : ∀ (k : K), ∃ g, ↑f g = ↑j k ∧ ‖g‖ ≤ C * ‖k‖
h : H
h_in : h ∈ NormedAddGroupHom.range j
⊢ ∃ g, ↑f g = h ∧ ‖g‖ ≤ C * ‖h‖
case hyp
G : Type u_1
inst✝³ : NormedAddCommGroup G
inst✝² : CompleteSpace G
H : Type u_2
inst✝¹ : NormedAddCommGroup H
f : NormedAddGroupHom G H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
j : NormedAddGroupHom K H
hj : ∀ (x : K), ‖↑j x‖ = ‖x‖
C ε : ℝ
hC : 0 < C
hε : 0 < ε
hyp : ∀ (k : K), ∃ g, ↑f g = ↑j k ∧ ‖g‖ ≤ C * ‖k‖
⊢ ∀ (h : H), h ∈ NormedAddGroupHom.range j → ∃ g, ↑f g = h ∧ ‖g‖ ≤ C * ‖h‖
intro h h_in
case hyp.intro
G : Type u_1
inst✝³ : NormedAddCommGroup G
inst✝² : CompleteSpace G
H : Type u_2
inst✝¹ : NormedAddCommGroup H
f : NormedAddGroupHom G H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
j : NormedAddGroupHom K H
hj : ∀ (x : K), ‖↑j x‖ = ‖x‖
C ε : ℝ
hC : 0 < C
hε : 0 < ε
hyp : ∀ (k : K), ∃ g, ↑f g = ↑j k ∧ ‖g‖ ≤ C * ‖k‖
k : K
h_in : ↑j k ∈ NormedAddGroupHom.range j
⊢ ∃ g, ↑f g = ↑j k ∧ ‖g‖ ≤ C * ‖↑j k‖
case hyp
G : Type u_1
inst✝³ : NormedAddCommGroup G
inst✝² : CompleteSpace G
H : Type u_2
inst✝¹ : NormedAddCommGroup H
f : NormedAddGroupHom G H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
j : NormedAddGroupHom K H
hj : ∀ (x : K), ‖↑j x‖ = ‖x‖
C ε : ℝ
hC : 0 < C
hε : 0 < ε
hyp : ∀ (k : K), ∃ g, ↑f g = ↑j k ∧ ‖g‖ ≤ C * ‖k‖
h : H
h_in : h ∈ NormedAddGroupHom.range j
⊢ ∃ g, ↑f g = h ∧ ‖g‖ ≤ C * ‖h‖
rcases(j.mem_range _).mp h_in with ⟨k, rfl⟩
case hyp.intro
G : Type u_1
inst✝³ : NormedAddCommGroup G
inst✝² : CompleteSpace G
H : Type u_2
inst✝¹ : NormedAddCommGroup H
f : NormedAddGroupHom G H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
j : NormedAddGroupHom K H
hj : ∀ (x : K), ‖↑j x‖ = ‖x‖
C ε : ℝ
hC : 0 < C
hε : 0 < ε
hyp : ∀ (k : K), ∃ g, ↑f g = ↑j k ∧ ‖g‖ ≤ C * ‖k‖
k : K
h_in : ↑j k ∈ NormedAddGroupHom.range j
⊢ ∃ g, ↑f g = ↑j k ∧ ‖g‖ ≤ C * ‖k‖
case hyp.intro
G : Type u_1
inst✝³ : NormedAddCommGroup G
inst✝² : CompleteSpace G
H : Type u_2
inst✝¹ : NormedAddCommGroup H
f : NormedAddGroupHom G H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
j : NormedAddGroupHom K H
hj : ∀ (x : K), ‖↑j x‖ = ‖x‖
C ε : ℝ
hC : 0 < C
hε : 0 < ε
hyp : ∀ (k : K), ∃ g, ↑f g = ↑j k ∧ ‖g‖ ≤ C * ‖k‖
k : K
h_in : ↑j k ∈ NormedAddGroupHom.range j
⊢ ∃ g, ↑f g = ↑j k ∧ ‖g‖ ≤ C * ‖↑j k‖
rw [hj]
no goals
case hyp.intro
G : Type u_1
inst✝³ : NormedAddCommGroup G
inst✝² : CompleteSpace G
H : Type u_2
inst✝¹ : NormedAddCommGroup H
f : NormedAddGroupHom G H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
j : NormedAddGroupHom K H
hj : ∀ (x : K), ‖↑j x‖ = ‖x‖
C ε : ℝ
hC : 0 < C
hε : 0 < ε
hyp : ∀ (k : K), ∃ g, ↑f g = ↑j k ∧ ‖g‖ ≤ C * ‖k‖
k : K
h_in : ↑j k ∈ NormedAddGroupHom.range j
⊢ ∃ g, ↑f g = ↑j k ∧ ‖g‖ ≤ C * ‖k‖
exact hyp k