case refine'_1
V : Type ?u.219726
V₁ : Type u_1
V₂ : Type u_2
V₃ : Type ?u.219735
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f✝ g f : NormedAddGroupHom V₁ V₂
K : AddSubgroup V₂
C : ℝ
h : SurjectiveOnWith f K C
⊢ abs C + 1 > 0

case refine'_2
V : Type ?u.219726
V₁ : Type u_1
V₂ : Type u_2
V₃ : Type ?u.219735
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f✝ g f : NormedAddGroupHom V₁ V₂
K : AddSubgroup V₂
C : ℝ
h : SurjectiveOnWith f K C
⊢ SurjectiveOnWith f K (abs C + 1)
V : Type ?u.219726
V₁ : Type u_1
V₂ : Type u_2
V₃ : Type ?u.219735
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f✝ g f : NormedAddGroupHom V₁ V₂
K : AddSubgroup V₂
C : ℝ
h : SurjectiveOnWith f K C
⊢ ∃ C', C' > 0 ∧ SurjectiveOnWith f K C'
refine' ⟨|C| + 1, _, _⟩
no goals
case refine'_1
V : Type ?u.219726
V₁ : Type u_1
V₂ : Type u_2
V₃ : Type ?u.219735
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f✝ g f : NormedAddGroupHom V₁ V₂
K : AddSubgroup V₂
C : ℝ
h : SurjectiveOnWith f K C
⊢ abs C + 1 > 0
linarith [abs_nonneg C]
case refine'_2
V : Type ?u.219726
V₁ : Type u_1
V₂ : Type u_2
V₃ : Type ?u.219735
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f✝ g f : NormedAddGroupHom V₁ V₂
K : AddSubgroup V₂
C : ℝ
h : SurjectiveOnWith f K C
⊢ C ≤ abs C + 1
case refine'_2
V : Type ?u.219726
V₁ : Type u_1
V₂ : Type u_2
V₃ : Type ?u.219735
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f✝ g f : NormedAddGroupHom V₁ V₂
K : AddSubgroup V₂
C : ℝ
h : SurjectiveOnWith f K C
⊢ SurjectiveOnWith f K (abs C + 1)
apply h.mono
no goals
case refine'_2
V : Type ?u.219726
V₁ : Type u_1
V₂ : Type u_2
V₃ : Type ?u.219735
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f✝ g f : NormedAddGroupHom V₁ V₂
K : AddSubgroup V₂
C : ℝ
h : SurjectiveOnWith f K C
⊢ C ≤ abs C + 1
linarith [le_abs_self C]