Theorem: dist_inv_le_dist_div (RMT4/hurwitz.lean)

State before:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hη : 0 < η
hη' : 0 < η'
hx : x ∉ ball 0 η
hy : y ∉ ball 0 η'
⊢ dist x⁻¹ y⁻¹ ≤ dist x y / (η * η')
Tactic:
have h1 : x ≠ 0 := by contrapose! hx; simp only [hx, mem_ball_self, hη]
State after:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hη : 0 < η
hη' : 0 < η'
hx : x ∉ ball 0 η
hy : y ∉ ball 0 η'
h1 : x ≠ 0
⊢ dist x⁻¹ y⁻¹ ≤ dist x y / (η * η')

State before:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hη : 0 < η
hη' : 0 < η'
hx : x ∉ ball 0 η
hy : y ∉ ball 0 η'
h1 : x ≠ 0
⊢ dist x⁻¹ y⁻¹ ≤ dist x y / (η * η')
Tactic:
have h2 : y ≠ 0 := by contrapose! hy; simp only [hy, mem_ball_self, hη']
State after:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hη : 0 < η
hη' : 0 < η'
hx : x ∉ ball 0 η
hy : y ∉ ball 0 η'
h1 : x ≠ 0
h2 : y ≠ 0
⊢ dist x⁻¹ y⁻¹ ≤ dist x y / (η * η')

State before:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hη : 0 < η
hη' : 0 < η'
hx : x ∉ ball 0 η
hy : y ∉ ball 0 η'
h1 : x ≠ 0
h2 : y ≠ 0
⊢ dist x⁻¹ y⁻¹ ≤ dist x y / (η * η')
Tactic:
simp only [mem_ball, dist_eq_norm, sub_zero, not_lt] at hx hy
State after:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hη : 0 < η
hη' : 0 < η'
h1 : x ≠ 0
h2 : y ≠ 0
hx : η ≤ ‖x‖
hy : η' ≤ ‖y‖
⊢ dist x⁻¹ y⁻¹ ≤ dist x y / (η * η')

State before:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hη : 0 < η
hη' : 0 < η'
h1 : x ≠ 0
h2 : y ≠ 0
hx : η ≤ ‖x‖
hy : η' ≤ ‖y‖
⊢ dist x⁻¹ y⁻¹ ≤ dist x y / (η * η')
Tactic:
rw [dist_inv_inv₀ h1 h2]
State after:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hη : 0 < η
hη' : 0 < η'
h1 : x ≠ 0
h2 : y ≠ 0
hx : η ≤ ‖x‖
hy : η' ≤ ‖y‖
⊢ dist x y / (‖x‖ * ‖y‖) ≤ dist x y / (η * η')

State before:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hη : 0 < η
hη' : 0 < η'
h1 : x ≠ 0
h2 : y ≠ 0
hx : η ≤ ‖x‖
hy : η' ≤ ‖y‖
⊢ dist x y / (‖x‖ * ‖y‖) ≤ dist x y / (η * η')
Tactic:
gcongr
State after:
no goals

State before:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hη : 0 < η
hη' : 0 < η'
hx : x ∉ ball 0 η
hy : y ∉ ball 0 η'
⊢ x ≠ 0
Tactic:
contrapose! hx
State after:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hη : 0 < η
hη' : 0 < η'
hy : y ∉ ball 0 η'
hx : x = 0
⊢ x ∈ ball 0 η

State before:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hη : 0 < η
hη' : 0 < η'
hy : y ∉ ball 0 η'
hx : x = 0
⊢ x ∈ ball 0 η
Tactic:
simp only [hx, mem_ball_self, hη]
State after:
no goals

State before:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hη : 0 < η
hη' : 0 < η'
hx : x ∉ ball 0 η
hy : y ∉ ball 0 η'
h1 : x ≠ 0
⊢ y ≠ 0
Tactic:
contrapose! hy
State after:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hη : 0 < η
hη' : 0 < η'
hx : x ∉ ball 0 η
h1 : x ≠ 0
hy : y = 0
⊢ y ∈ ball 0 η'

State before:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hη : 0 < η
hη' : 0 < η'
hx : x ∉ ball 0 η
h1 : x ≠ 0
hy : y = 0
⊢ y ∈ ball 0 η'
Tactic:
simp only [hy, mem_ball_self, hη']
State after:
no goals