case intro
𝕜✝ : Type ?u.748535
𝕜₂✝ : Type ?u.748538
𝕜₃ : Type ?u.748541
E✝ : Type ?u.748544
Eₗ : Type ?u.748547
F✝ : Type ?u.748550
Fₗ : Type ?u.748553
G : Type ?u.748556
Gₗ : Type ?u.748559
𝓕 : Type ?u.748562
inst✝²³ : SeminormedAddCommGroup E✝
inst✝²² : SeminormedAddCommGroup Eₗ
inst✝²¹ : SeminormedAddCommGroup F✝
inst✝²⁰ : SeminormedAddCommGroup Fₗ
inst✝¹⁹ : SeminormedAddCommGroup G
inst✝¹⁸ : SeminormedAddCommGroup Gₗ
inst✝¹⁷ : NontriviallyNormedField 𝕜✝
inst✝¹⁶ : NontriviallyNormedField 𝕜₂✝
inst✝¹⁵ : NontriviallyNormedField 𝕜₃
inst✝¹⁴ : NormedSpace 𝕜✝ E✝
inst✝¹³ : NormedSpace 𝕜✝ Eₗ
inst✝¹² : NormedSpace 𝕜₂✝ F✝
inst✝¹¹ : NormedSpace 𝕜✝ Fₗ
inst✝¹⁰ : NormedSpace 𝕜₃ G
inst✝⁹ : NormedSpace 𝕜✝ Gₗ
σ₁₂✝ : 𝕜✝ →+* 𝕜₂✝
σ₂₃ : 𝕜₂✝ →+* 𝕜₃
σ₁₃ : 𝕜✝ →+* 𝕜₃
inst✝⁸ : RingHomCompTriple σ₁₂✝ σ₂₃ σ₁₃
inst✝⁷ : RingHomIsometric σ₁₂✝
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : DenselyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
r : ℝ≥0
hr : r < ‖f‖₊
y : E
hy : r * ‖y‖₊ < ‖↑f y‖₊
⊢ ∃ x, ‖x‖₊ < 1 ∧ r < ‖↑f x‖₊
𝕜✝ : Type ?u.748535
𝕜₂✝ : Type ?u.748538
𝕜₃ : Type ?u.748541
E✝ : Type ?u.748544
Eₗ : Type ?u.748547
F✝ : Type ?u.748550
Fₗ : Type ?u.748553
G : Type ?u.748556
Gₗ : Type ?u.748559
𝓕 : Type ?u.748562
inst✝²³ : SeminormedAddCommGroup E✝
inst✝²² : SeminormedAddCommGroup Eₗ
inst✝²¹ : SeminormedAddCommGroup F✝
inst✝²⁰ : SeminormedAddCommGroup Fₗ
inst✝¹⁹ : SeminormedAddCommGroup G
inst✝¹⁸ : SeminormedAddCommGroup Gₗ
inst✝¹⁷ : NontriviallyNormedField 𝕜✝
inst✝¹⁶ : NontriviallyNormedField 𝕜₂✝
inst✝¹⁵ : NontriviallyNormedField 𝕜₃
inst✝¹⁴ : NormedSpace 𝕜✝ E✝
inst✝¹³ : NormedSpace 𝕜✝ Eₗ
inst✝¹² : NormedSpace 𝕜₂✝ F✝
inst✝¹¹ : NormedSpace 𝕜✝ Fₗ
inst✝¹⁰ : NormedSpace 𝕜₃ G
inst✝⁹ : NormedSpace 𝕜✝ Gₗ
σ₁₂✝ : 𝕜✝ →+* 𝕜₂✝
σ₂₃ : 𝕜₂✝ →+* 𝕜₃
σ₁₃ : 𝕜✝ →+* 𝕜₃
inst✝⁸ : RingHomCompTriple σ₁₂✝ σ₂₃ σ₁₃
inst✝⁷ : RingHomIsometric σ₁₂✝
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : DenselyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
r : ℝ≥0
hr : r < ‖f‖₊
⊢ ∃ x, ‖x‖₊ < 1 ∧ r < ‖↑f x‖₊
obtain ⟨y, hy⟩ := f.exists_mul_lt_apply_of_lt_op_nnnorm hr
case intro
𝕜✝ : Type ?u.748535
𝕜₂✝ : Type ?u.748538
𝕜₃ : Type ?u.748541
E✝ : Type ?u.748544
Eₗ : Type ?u.748547
F✝ : Type ?u.748550
Fₗ : Type ?u.748553
G : Type ?u.748556
Gₗ : Type ?u.748559
𝓕 : Type ?u.748562
inst✝²³ : SeminormedAddCommGroup E✝
inst✝²² : SeminormedAddCommGroup Eₗ
inst✝²¹ : SeminormedAddCommGroup F✝
inst✝²⁰ : SeminormedAddCommGroup Fₗ
inst✝¹⁹ : SeminormedAddCommGroup G
inst✝¹⁸ : SeminormedAddCommGroup Gₗ
inst✝¹⁷ : NontriviallyNormedField 𝕜✝
inst✝¹⁶ : NontriviallyNormedField 𝕜₂✝
inst✝¹⁵ : NontriviallyNormedField 𝕜₃
inst✝¹⁴ : NormedSpace 𝕜✝ E✝
inst✝¹³ : NormedSpace 𝕜✝ Eₗ
inst✝¹² : NormedSpace 𝕜₂✝ F✝
inst✝¹¹ : NormedSpace 𝕜✝ Fₗ
inst✝¹⁰ : NormedSpace 𝕜₃ G
inst✝⁹ : NormedSpace 𝕜✝ Gₗ
σ₁₂✝ : 𝕜✝ →+* 𝕜₂✝
σ₂₃ : 𝕜₂✝ →+* 𝕜₃
σ₁₃ : 𝕜✝ →+* 𝕜₃
inst✝⁸ : RingHomCompTriple σ₁₂✝ σ₂₃ σ₁₃
inst✝⁷ : RingHomIsometric σ₁₂✝
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : DenselyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
r : ℝ≥0
hr : r < ‖f‖₊
y : E
hy : r * ‖y‖₊ < ‖↑f y‖₊
hy' : ‖y‖₊ ≠ 0
⊢ ∃ x, ‖x‖₊ < 1 ∧ r < ‖↑f x‖₊
case intro
𝕜✝ : Type ?u.748535
𝕜₂✝ : Type ?u.748538
𝕜₃ : Type ?u.748541
E✝ : Type ?u.748544
Eₗ : Type ?u.748547
F✝ : Type ?u.748550
Fₗ : Type ?u.748553
G : Type ?u.748556
Gₗ : Type ?u.748559
𝓕 : Type ?u.748562
inst✝²³ : SeminormedAddCommGroup E✝
inst✝²² : SeminormedAddCommGroup Eₗ
inst✝²¹ : SeminormedAddCommGroup F✝
inst✝²⁰ : SeminormedAddCommGroup Fₗ
inst✝¹⁹ : SeminormedAddCommGroup G
inst✝¹⁸ : SeminormedAddCommGroup Gₗ
inst✝¹⁷ : NontriviallyNormedField 𝕜✝
inst✝¹⁶ : NontriviallyNormedField 𝕜₂✝
inst✝¹⁵ : NontriviallyNormedField 𝕜₃
inst✝¹⁴ : NormedSpace 𝕜✝ E✝
inst✝¹³ : NormedSpace 𝕜✝ Eₗ
inst✝¹² : NormedSpace 𝕜₂✝ F✝
inst✝¹¹ : NormedSpace 𝕜✝ Fₗ
inst✝¹⁰ : NormedSpace 𝕜₃ G
inst✝⁹ : NormedSpace 𝕜✝ Gₗ
σ₁₂✝ : 𝕜✝ →+* 𝕜₂✝
σ₂₃ : 𝕜₂✝ →+* 𝕜₃
σ₁₃ : 𝕜✝ →+* 𝕜₃
inst✝⁸ : RingHomCompTriple σ₁₂✝ σ₂₃ σ₁₃
inst✝⁷ : RingHomIsometric σ₁₂✝
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : DenselyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
r : ℝ≥0
hr : r < ‖f‖₊
y : E
hy : r * ‖y‖₊ < ‖↑f y‖₊
⊢ ∃ x, ‖x‖₊ < 1 ∧ r < ‖↑f x‖₊
have hy' : ‖y‖₊ ≠ 0 :=
  nnnorm_ne_zero_iff.2 fun heq => by
    simp [heq, nnnorm_zero, map_zero, not_lt_zero'] at hy
case intro
𝕜✝ : Type ?u.748535
𝕜₂✝ : Type ?u.748538
𝕜₃ : Type ?u.748541
E✝ : Type ?u.748544
Eₗ : Type ?u.748547
F✝ : Type ?u.748550
Fₗ : Type ?u.748553
G : Type ?u.748556
Gₗ : Type ?u.748559
𝓕 : Type ?u.748562
inst✝²³ : SeminormedAddCommGroup E✝
inst✝²² : SeminormedAddCommGroup Eₗ
inst✝²¹ : SeminormedAddCommGroup F✝
inst✝²⁰ : SeminormedAddCommGroup Fₗ
inst✝¹⁹ : SeminormedAddCommGroup G
inst✝¹⁸ : SeminormedAddCommGroup Gₗ
inst✝¹⁷ : NontriviallyNormedField 𝕜✝
inst✝¹⁶ : NontriviallyNormedField 𝕜₂✝
inst✝¹⁵ : NontriviallyNormedField 𝕜₃
inst✝¹⁴ : NormedSpace 𝕜✝ E✝
inst✝¹³ : NormedSpace 𝕜✝ Eₗ
inst✝¹² : NormedSpace 𝕜₂✝ F✝
inst✝¹¹ : NormedSpace 𝕜✝ Fₗ
inst✝¹⁰ : NormedSpace 𝕜₃ G
inst✝⁹ : NormedSpace 𝕜✝ Gₗ
σ₁₂✝ : 𝕜✝ →+* 𝕜₂✝
σ₂₃ : 𝕜₂✝ →+* 𝕜₃
σ₁₃ : 𝕜✝ →+* 𝕜₃
inst✝⁸ : RingHomCompTriple σ₁₂✝ σ₂₃ σ₁₃
inst✝⁷ : RingHomIsometric σ₁₂✝
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : DenselyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
r : ℝ≥0
hr : r < ‖f‖₊
y : E
hy : r * ‖y‖₊ < ‖↑f y‖₊
hy' : ‖y‖₊ ≠ 0
hfy : ‖↑f y‖₊ ≠ 0
⊢ ∃ x, ‖x‖₊ < 1 ∧ r < ‖↑f x‖₊
case intro
𝕜✝ : Type ?u.748535
𝕜₂✝ : Type ?u.748538
𝕜₃ : Type ?u.748541
E✝ : Type ?u.748544
Eₗ : Type ?u.748547
F✝ : Type ?u.748550
Fₗ : Type ?u.748553
G : Type ?u.748556
Gₗ : Type ?u.748559
𝓕 : Type ?u.748562
inst✝²³ : SeminormedAddCommGroup E✝
inst✝²² : SeminormedAddCommGroup Eₗ
inst✝²¹ : SeminormedAddCommGroup F✝
inst✝²⁰ : SeminormedAddCommGroup Fₗ
inst✝¹⁹ : SeminormedAddCommGroup G
inst✝¹⁸ : SeminormedAddCommGroup Gₗ
inst✝¹⁷ : NontriviallyNormedField 𝕜✝
inst✝¹⁶ : NontriviallyNormedField 𝕜₂✝
inst✝¹⁵ : NontriviallyNormedField 𝕜₃
inst✝¹⁴ : NormedSpace 𝕜✝ E✝
inst✝¹³ : NormedSpace 𝕜✝ Eₗ
inst✝¹² : NormedSpace 𝕜₂✝ F✝
inst✝¹¹ : NormedSpace 𝕜✝ Fₗ
inst✝¹⁰ : NormedSpace 𝕜₃ G
inst✝⁹ : NormedSpace 𝕜✝ Gₗ
σ₁₂✝ : 𝕜✝ →+* 𝕜₂✝
σ₂₃ : 𝕜₂✝ →+* 𝕜₃
σ₁₃ : 𝕜✝ →+* 𝕜₃
inst✝⁸ : RingHomCompTriple σ₁₂✝ σ₂₃ σ₁₃
inst✝⁷ : RingHomIsometric σ₁₂✝
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : DenselyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
r : ℝ≥0
hr : r < ‖f‖₊
y : E
hy : r * ‖y‖₊ < ‖↑f y‖₊
hy' : ‖y‖₊ ≠ 0
⊢ ∃ x, ‖x‖₊ < 1 ∧ r < ‖↑f x‖₊
have hfy : ‖f y‖₊ ≠ 0 := (zero_le'.trans_lt hy).ne'
case intro
𝕜✝ : Type ?u.748535
𝕜₂✝ : Type ?u.748538
𝕜₃ : Type ?u.748541
E✝ : Type ?u.748544
Eₗ : Type ?u.748547
F✝ : Type ?u.748550
Fₗ : Type ?u.748553
G : Type ?u.748556
Gₗ : Type ?u.748559
𝓕 : Type ?u.748562
inst✝²³ : SeminormedAddCommGroup E✝
inst✝²² : SeminormedAddCommGroup Eₗ
inst✝²¹ : SeminormedAddCommGroup F✝
inst✝²⁰ : SeminormedAddCommGroup Fₗ
inst✝¹⁹ : SeminormedAddCommGroup G
inst✝¹⁸ : SeminormedAddCommGroup Gₗ
inst✝¹⁷ : NontriviallyNormedField 𝕜✝
inst✝¹⁶ : NontriviallyNormedField 𝕜₂✝
inst✝¹⁵ : NontriviallyNormedField 𝕜₃
inst✝¹⁴ : NormedSpace 𝕜✝ E✝
inst✝¹³ : NormedSpace 𝕜✝ Eₗ
inst✝¹² : NormedSpace 𝕜₂✝ F✝
inst✝¹¹ : NormedSpace 𝕜✝ Fₗ
inst✝¹⁰ : NormedSpace 𝕜₃ G
inst✝⁹ : NormedSpace 𝕜✝ Gₗ
σ₁₂✝ : 𝕜✝ →+* 𝕜₂✝
σ₂₃ : 𝕜₂✝ →+* 𝕜₃
σ₁₃ : 𝕜✝ →+* 𝕜₃
inst✝⁸ : RingHomCompTriple σ₁₂✝ σ₂₃ σ₁₃
inst✝⁷ : RingHomIsometric σ₁₂✝
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : DenselyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
r : ℝ≥0
hr : r < ‖f‖₊
y : E
hy : r * ‖↑f y‖₊⁻¹ < ‖y‖₊⁻¹
hy' : ‖y‖₊ ≠ 0
hfy : ‖↑f y‖₊ ≠ 0
⊢ ∃ x, ‖x‖₊ < 1 ∧ r < ‖↑f x‖₊
case intro
𝕜✝ : Type ?u.748535
𝕜₂✝ : Type ?u.748538
𝕜₃ : Type ?u.748541
E✝ : Type ?u.748544
Eₗ : Type ?u.748547
F✝ : Type ?u.748550
Fₗ : Type ?u.748553
G : Type ?u.748556
Gₗ : Type ?u.748559
𝓕 : Type ?u.748562
inst✝²³ : SeminormedAddCommGroup E✝
inst✝²² : SeminormedAddCommGroup Eₗ
inst✝²¹ : SeminormedAddCommGroup F✝
inst✝²⁰ : SeminormedAddCommGroup Fₗ
inst✝¹⁹ : SeminormedAddCommGroup G
inst✝¹⁸ : SeminormedAddCommGroup Gₗ
inst✝¹⁷ : NontriviallyNormedField 𝕜✝
inst✝¹⁶ : NontriviallyNormedField 𝕜₂✝
inst✝¹⁵ : NontriviallyNormedField 𝕜₃
inst✝¹⁴ : NormedSpace 𝕜✝ E✝
inst✝¹³ : NormedSpace 𝕜✝ Eₗ
inst✝¹² : NormedSpace 𝕜₂✝ F✝
inst✝¹¹ : NormedSpace 𝕜✝ Fₗ
inst✝¹⁰ : NormedSpace 𝕜₃ G
inst✝⁹ : NormedSpace 𝕜✝ Gₗ
σ₁₂✝ : 𝕜✝ →+* 𝕜₂✝
σ₂₃ : 𝕜₂✝ →+* 𝕜₃
σ₁₃ : 𝕜✝ →+* 𝕜₃
inst✝⁸ : RingHomCompTriple σ₁₂✝ σ₂₃ σ₁₃
inst✝⁷ : RingHomIsometric σ₁₂✝
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : DenselyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
r : ℝ≥0
hr : r < ‖f‖₊
y : E
hy : r * ‖y‖₊ < ‖↑f y‖₊
hy' : ‖y‖₊ ≠ 0
hfy : ‖↑f y‖₊ ≠ 0
⊢ ∃ x, ‖x‖₊ < 1 ∧ r < ‖↑f x‖₊
rw [← inv_inv ‖f y‖₊, NNReal.lt_inv_iff_mul_lt (inv_ne_zero hfy), mul_assoc, mul_comm ‖y‖₊, ←
  mul_assoc, ← NNReal.lt_inv_iff_mul_lt hy'] at hy
case intro.intro.intro
𝕜✝ : Type ?u.748535
𝕜₂✝ : Type ?u.748538
𝕜₃ : Type ?u.748541
E✝ : Type ?u.748544
Eₗ : Type ?u.748547
F✝ : Type ?u.748550
Fₗ : Type ?u.748553
G : Type ?u.748556
Gₗ : Type ?u.748559
𝓕 : Type ?u.748562
inst✝²³ : SeminormedAddCommGroup E✝
inst✝²² : SeminormedAddCommGroup Eₗ
inst✝²¹ : SeminormedAddCommGroup F✝
inst✝²⁰ : SeminormedAddCommGroup Fₗ
inst✝¹⁹ : SeminormedAddCommGroup G
inst✝¹⁸ : SeminormedAddCommGroup Gₗ
inst✝¹⁷ : NontriviallyNormedField 𝕜✝
inst✝¹⁶ : NontriviallyNormedField 𝕜₂✝
inst✝¹⁵ : NontriviallyNormedField 𝕜₃
inst✝¹⁴ : NormedSpace 𝕜✝ E✝
inst✝¹³ : NormedSpace 𝕜✝ Eₗ
inst✝¹² : NormedSpace 𝕜₂✝ F✝
inst✝¹¹ : NormedSpace 𝕜✝ Fₗ
inst✝¹⁰ : NormedSpace 𝕜₃ G
inst✝⁹ : NormedSpace 𝕜✝ Gₗ
σ₁₂✝ : 𝕜✝ →+* 𝕜₂✝
σ₂₃ : 𝕜₂✝ →+* 𝕜₃
σ₁₃ : 𝕜✝ →+* 𝕜₃
inst✝⁸ : RingHomCompTriple σ₁₂✝ σ₂₃ σ₁₃
inst✝⁷ : RingHomIsometric σ₁₂✝
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : DenselyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
r : ℝ≥0
hr : r < ‖f‖₊
y : E
hy : r * ‖↑f y‖₊⁻¹ < ‖y‖₊⁻¹
hy' : ‖y‖₊ ≠ 0
hfy : ‖↑f y‖₊ ≠ 0
k : 𝕜
hk₁ : r * ‖↑f y‖₊⁻¹ < ‖k‖₊
hk₂ : ‖k‖₊ < ‖y‖₊⁻¹
⊢ ∃ x, ‖x‖₊ < 1 ∧ r < ‖↑f x‖₊
case intro
𝕜✝ : Type ?u.748535
𝕜₂✝ : Type ?u.748538
𝕜₃ : Type ?u.748541
E✝ : Type ?u.748544
Eₗ : Type ?u.748547
F✝ : Type ?u.748550
Fₗ : Type ?u.748553
G : Type ?u.748556
Gₗ : Type ?u.748559
𝓕 : Type ?u.748562
inst✝²³ : SeminormedAddCommGroup E✝
inst✝²² : SeminormedAddCommGroup Eₗ
inst✝²¹ : SeminormedAddCommGroup F✝
inst✝²⁰ : SeminormedAddCommGroup Fₗ
inst✝¹⁹ : SeminormedAddCommGroup G
inst✝¹⁸ : SeminormedAddCommGroup Gₗ
inst✝¹⁷ : NontriviallyNormedField 𝕜✝
inst✝¹⁶ : NontriviallyNormedField 𝕜₂✝
inst✝¹⁵ : NontriviallyNormedField 𝕜₃
inst✝¹⁴ : NormedSpace 𝕜✝ E✝
inst✝¹³ : NormedSpace 𝕜✝ Eₗ
inst✝¹² : NormedSpace 𝕜₂✝ F✝
inst✝¹¹ : NormedSpace 𝕜✝ Fₗ
inst✝¹⁰ : NormedSpace 𝕜₃ G
inst✝⁹ : NormedSpace 𝕜✝ Gₗ
σ₁₂✝ : 𝕜✝ →+* 𝕜₂✝
σ₂₃ : 𝕜₂✝ →+* 𝕜₃
σ₁₃ : 𝕜✝ →+* 𝕜₃
inst✝⁸ : RingHomCompTriple σ₁₂✝ σ₂₃ σ₁₃
inst✝⁷ : RingHomIsometric σ₁₂✝
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : DenselyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
r : ℝ≥0
hr : r < ‖f‖₊
y : E
hy : r * ‖↑f y‖₊⁻¹ < ‖y‖₊⁻¹
hy' : ‖y‖₊ ≠ 0
hfy : ‖↑f y‖₊ ≠ 0
⊢ ∃ x, ‖x‖₊ < 1 ∧ r < ‖↑f x‖₊
obtain ⟨k, hk₁, hk₂⟩ := NormedField.exists_lt_nnnorm_lt 𝕜 hy
case intro.intro.intro
𝕜✝ : Type ?u.748535
𝕜₂✝ : Type ?u.748538
𝕜₃ : Type ?u.748541
E✝ : Type ?u.748544
Eₗ : Type ?u.748547
F✝ : Type ?u.748550
Fₗ : Type ?u.748553
G : Type ?u.748556
Gₗ : Type ?u.748559
𝓕 : Type ?u.748562
inst✝²³ : SeminormedAddCommGroup E✝
inst✝²² : SeminormedAddCommGroup Eₗ
inst✝²¹ : SeminormedAddCommGroup F✝
inst✝²⁰ : SeminormedAddCommGroup Fₗ
inst✝¹⁹ : SeminormedAddCommGroup G
inst✝¹⁸ : SeminormedAddCommGroup Gₗ
inst✝¹⁷ : NontriviallyNormedField 𝕜✝
inst✝¹⁶ : NontriviallyNormedField 𝕜₂✝
inst✝¹⁵ : NontriviallyNormedField 𝕜₃
inst✝¹⁴ : NormedSpace 𝕜✝ E✝
inst✝¹³ : NormedSpace 𝕜✝ Eₗ
inst✝¹² : NormedSpace 𝕜₂✝ F✝
inst✝¹¹ : NormedSpace 𝕜✝ Fₗ
inst✝¹⁰ : NormedSpace 𝕜₃ G
inst✝⁹ : NormedSpace 𝕜✝ Gₗ
σ₁₂✝ : 𝕜✝ →+* 𝕜₂✝
σ₂₃ : 𝕜₂✝ →+* 𝕜₃
σ₁₃ : 𝕜✝ →+* 𝕜₃
inst✝⁸ : RingHomCompTriple σ₁₂✝ σ₂₃ σ₁₃
inst✝⁷ : RingHomIsometric σ₁₂✝
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : DenselyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
r : ℝ≥0
hr : r < ‖f‖₊
y : E
hy : r * ‖↑f y‖₊⁻¹ < ‖y‖₊⁻¹
hy' : ‖y‖₊ ≠ 0
hfy : ‖↑f y‖₊ ≠ 0
k : 𝕜
hk₁ : r * ‖↑f y‖₊⁻¹ < ‖k‖₊
hk₂ : ‖k‖₊ < ‖y‖₊⁻¹
⊢ r < ‖↑f (k • y)‖₊
case intro.intro.intro
𝕜✝ : Type ?u.748535
𝕜₂✝ : Type ?u.748538
𝕜₃ : Type ?u.748541
E✝ : Type ?u.748544
Eₗ : Type ?u.748547
F✝ : Type ?u.748550
Fₗ : Type ?u.748553
G : Type ?u.748556
Gₗ : Type ?u.748559
𝓕 : Type ?u.748562
inst✝²³ : SeminormedAddCommGroup E✝
inst✝²² : SeminormedAddCommGroup Eₗ
inst✝²¹ : SeminormedAddCommGroup F✝
inst✝²⁰ : SeminormedAddCommGroup Fₗ
inst✝¹⁹ : SeminormedAddCommGroup G
inst✝¹⁸ : SeminormedAddCommGroup Gₗ
inst✝¹⁷ : NontriviallyNormedField 𝕜✝
inst✝¹⁶ : NontriviallyNormedField 𝕜₂✝
inst✝¹⁵ : NontriviallyNormedField 𝕜₃
inst✝¹⁴ : NormedSpace 𝕜✝ E✝
inst✝¹³ : NormedSpace 𝕜✝ Eₗ
inst✝¹² : NormedSpace 𝕜₂✝ F✝
inst✝¹¹ : NormedSpace 𝕜✝ Fₗ
inst✝¹⁰ : NormedSpace 𝕜₃ G
inst✝⁹ : NormedSpace 𝕜✝ Gₗ
σ₁₂✝ : 𝕜✝ →+* 𝕜₂✝
σ₂₃ : 𝕜₂✝ →+* 𝕜₃
σ₁₃ : 𝕜✝ →+* 𝕜₃
inst✝⁸ : RingHomCompTriple σ₁₂✝ σ₂₃ σ₁₃
inst✝⁷ : RingHomIsometric σ₁₂✝
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : DenselyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
r : ℝ≥0
hr : r < ‖f‖₊
y : E
hy : r * ‖↑f y‖₊⁻¹ < ‖y‖₊⁻¹
hy' : ‖y‖₊ ≠ 0
hfy : ‖↑f y‖₊ ≠ 0
k : 𝕜
hk₁ : r * ‖↑f y‖₊⁻¹ < ‖k‖₊
hk₂ : ‖k‖₊ < ‖y‖₊⁻¹
⊢ ∃ x, ‖x‖₊ < 1 ∧ r < ‖↑f x‖₊
refine' ⟨k • y, (nnnorm_smul k y).symm ▸ (NNReal.lt_inv_iff_mul_lt hy').1 hk₂, _⟩
case intro.intro.intro
𝕜✝ : Type ?u.748535
𝕜₂✝ : Type ?u.748538
𝕜₃ : Type ?u.748541
E✝ : Type ?u.748544
Eₗ : Type ?u.748547
F✝ : Type ?u.748550
Fₗ : Type ?u.748553
G : Type ?u.748556
Gₗ : Type ?u.748559
𝓕 : Type ?u.748562
inst✝²³ : SeminormedAddCommGroup E✝
inst✝²² : SeminormedAddCommGroup Eₗ
inst✝²¹ : SeminormedAddCommGroup F✝
inst✝²⁰ : SeminormedAddCommGroup Fₗ
inst✝¹⁹ : SeminormedAddCommGroup G
inst✝¹⁸ : SeminormedAddCommGroup Gₗ
inst✝¹⁷ : NontriviallyNormedField 𝕜✝
inst✝¹⁶ : NontriviallyNormedField 𝕜₂✝
inst✝¹⁵ : NontriviallyNormedField 𝕜₃
inst✝¹⁴ : NormedSpace 𝕜✝ E✝
inst✝¹³ : NormedSpace 𝕜✝ Eₗ
inst✝¹² : NormedSpace 𝕜₂✝ F✝
inst✝¹¹ : NormedSpace 𝕜✝ Fₗ
inst✝¹⁰ : NormedSpace 𝕜₃ G
inst✝⁹ : NormedSpace 𝕜✝ Gₗ
σ₁₂✝ : 𝕜✝ →+* 𝕜₂✝
σ₂₃ : 𝕜₂✝ →+* 𝕜₃
σ₁₃ : 𝕜✝ →+* 𝕜₃
inst✝⁸ : RingHomCompTriple σ₁₂✝ σ₂₃ σ₁₃
inst✝⁷ : RingHomIsometric σ₁₂✝
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : DenselyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
r : ℝ≥0
hr : r < ‖f‖₊
y : E
hy : r * ‖↑f y‖₊⁻¹ < ‖y‖₊⁻¹
hy' : ‖y‖₊ ≠ 0
hfy : ‖↑f y‖₊ ≠ 0
k : 𝕜
hk₁ : r * ‖↑f y‖₊⁻¹ < ‖k‖₊
hk₂ : ‖k‖₊ < ‖y‖₊⁻¹
this : ‖↑σ₁₂ k‖₊ = ‖k‖₊
⊢ r < ‖↑f (k • y)‖₊
case intro.intro.intro
𝕜✝ : Type ?u.748535
𝕜₂✝ : Type ?u.748538
𝕜₃ : Type ?u.748541
E✝ : Type ?u.748544
Eₗ : Type ?u.748547
F✝ : Type ?u.748550
Fₗ : Type ?u.748553
G : Type ?u.748556
Gₗ : Type ?u.748559
𝓕 : Type ?u.748562
inst✝²³ : SeminormedAddCommGroup E✝
inst✝²² : SeminormedAddCommGroup Eₗ
inst✝²¹ : SeminormedAddCommGroup F✝
inst✝²⁰ : SeminormedAddCommGroup Fₗ
inst✝¹⁹ : SeminormedAddCommGroup G
inst✝¹⁸ : SeminormedAddCommGroup Gₗ
inst✝¹⁷ : NontriviallyNormedField 𝕜✝
inst✝¹⁶ : NontriviallyNormedField 𝕜₂✝
inst✝¹⁵ : NontriviallyNormedField 𝕜₃
inst✝¹⁴ : NormedSpace 𝕜✝ E✝
inst✝¹³ : NormedSpace 𝕜✝ Eₗ
inst✝¹² : NormedSpace 𝕜₂✝ F✝
inst✝¹¹ : NormedSpace 𝕜✝ Fₗ
inst✝¹⁰ : NormedSpace 𝕜₃ G
inst✝⁹ : NormedSpace 𝕜✝ Gₗ
σ₁₂✝ : 𝕜✝ →+* 𝕜₂✝
σ₂₃ : 𝕜₂✝ →+* 𝕜₃
σ₁₃ : 𝕜✝ →+* 𝕜₃
inst✝⁸ : RingHomCompTriple σ₁₂✝ σ₂₃ σ₁₃
inst✝⁷ : RingHomIsometric σ₁₂✝
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : DenselyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
r : ℝ≥0
hr : r < ‖f‖₊
y : E
hy : r * ‖↑f y‖₊⁻¹ < ‖y‖₊⁻¹
hy' : ‖y‖₊ ≠ 0
hfy : ‖↑f y‖₊ ≠ 0
k : 𝕜
hk₁ : r * ‖↑f y‖₊⁻¹ < ‖k‖₊
hk₂ : ‖k‖₊ < ‖y‖₊⁻¹
⊢ r < ‖↑f (k • y)‖₊
have : ‖σ₁₂ k‖₊ = ‖k‖₊ := Subtype.ext RingHomIsometric.is_iso
no goals
case intro.intro.intro
𝕜✝ : Type ?u.748535
𝕜₂✝ : Type ?u.748538
𝕜₃ : Type ?u.748541
E✝ : Type ?u.748544
Eₗ : Type ?u.748547
F✝ : Type ?u.748550
Fₗ : Type ?u.748553
G : Type ?u.748556
Gₗ : Type ?u.748559
𝓕 : Type ?u.748562
inst✝²³ : SeminormedAddCommGroup E✝
inst✝²² : SeminormedAddCommGroup Eₗ
inst✝²¹ : SeminormedAddCommGroup F✝
inst✝²⁰ : SeminormedAddCommGroup Fₗ
inst✝¹⁹ : SeminormedAddCommGroup G
inst✝¹⁸ : SeminormedAddCommGroup Gₗ
inst✝¹⁷ : NontriviallyNormedField 𝕜✝
inst✝¹⁶ : NontriviallyNormedField 𝕜₂✝
inst✝¹⁵ : NontriviallyNormedField 𝕜₃
inst✝¹⁴ : NormedSpace 𝕜✝ E✝
inst✝¹³ : NormedSpace 𝕜✝ Eₗ
inst✝¹² : NormedSpace 𝕜₂✝ F✝
inst✝¹¹ : NormedSpace 𝕜✝ Fₗ
inst✝¹⁰ : NormedSpace 𝕜₃ G
inst✝⁹ : NormedSpace 𝕜✝ Gₗ
σ₁₂✝ : 𝕜✝ →+* 𝕜₂✝
σ₂₃ : 𝕜₂✝ →+* 𝕜₃
σ₁₃ : 𝕜✝ →+* 𝕜₃
inst✝⁸ : RingHomCompTriple σ₁₂✝ σ₂₃ σ₁₃
inst✝⁷ : RingHomIsometric σ₁₂✝
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : DenselyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
r : ℝ≥0
hr : r < ‖f‖₊
y : E
hy : r * ‖↑f y‖₊⁻¹ < ‖y‖₊⁻¹
hy' : ‖y‖₊ ≠ 0
hfy : ‖↑f y‖₊ ≠ 0
k : 𝕜
hk₁ : r * ‖↑f y‖₊⁻¹ < ‖k‖₊
hk₂ : ‖k‖₊ < ‖y‖₊⁻¹
this : ‖↑σ₁₂ k‖₊ = ‖k‖₊
⊢ r < ‖↑f (k • y)‖₊
rwa [map_smulₛₗ f, nnnorm_smul, ← NNReal.div_lt_iff hfy, div_eq_mul_inv, this]
no goals
𝕜✝ : Type ?u.748535
𝕜₂✝ : Type ?u.748538
𝕜₃ : Type ?u.748541
E✝ : Type ?u.748544
Eₗ : Type ?u.748547
F✝ : Type ?u.748550
Fₗ : Type ?u.748553
G : Type ?u.748556
Gₗ : Type ?u.748559
𝓕 : Type ?u.748562
inst✝²³ : SeminormedAddCommGroup E✝
inst✝²² : SeminormedAddCommGroup Eₗ
inst✝²¹ : SeminormedAddCommGroup F✝
inst✝²⁰ : SeminormedAddCommGroup Fₗ
inst✝¹⁹ : SeminormedAddCommGroup G
inst✝¹⁸ : SeminormedAddCommGroup Gₗ
inst✝¹⁷ : NontriviallyNormedField 𝕜✝
inst✝¹⁶ : NontriviallyNormedField 𝕜₂✝
inst✝¹⁵ : NontriviallyNormedField 𝕜₃
inst✝¹⁴ : NormedSpace 𝕜✝ E✝
inst✝¹³ : NormedSpace 𝕜✝ Eₗ
inst✝¹² : NormedSpace 𝕜₂✝ F✝
inst✝¹¹ : NormedSpace 𝕜✝ Fₗ
inst✝¹⁰ : NormedSpace 𝕜₃ G
inst✝⁹ : NormedSpace 𝕜✝ Gₗ
σ₁₂✝ : 𝕜✝ →+* 𝕜₂✝
σ₂₃ : 𝕜₂✝ →+* 𝕜₃
σ₁₃ : 𝕜✝ →+* 𝕜₃
inst✝⁸ : RingHomCompTriple σ₁₂✝ σ₂₃ σ₁₃
inst✝⁷ : RingHomIsometric σ₁₂✝
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : DenselyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
r : ℝ≥0
hr : r < ‖f‖₊
y : E
hy : r * ‖y‖₊ < ‖↑f y‖₊
heq : y = 0
⊢ False
simp [heq, nnnorm_zero, map_zero, not_lt_zero'] at hy