Theorem: titi (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 : ℝ
p q : Filter 𝕜
hp : p ⊓ 𝓝 0 = ⊥
hq : q ⊓ 𝓝 0 = ⊥
⊢ map (fun x => (x.1⁻¹, x.2⁻¹)) (𝓤 𝕜 ⊓ p ×ˢ q) ≤ 𝓤 𝕜
Tactic:
obtain ⟨U, hU, V, hV, hUV⟩ := inf_eq_bot_iff.mp hp
State after:
case intro.intro.intro.intro
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p✝ : Filter ι
mf mg : ℝ
p q : Filter 𝕜
hp : p ⊓ 𝓝 0 = ⊥
hq : q ⊓ 𝓝 0 = ⊥
U : Set 𝕜
hU : U ∈ p
V : Set 𝕜
hV : V ∈ 𝓝 0
hUV : U ∩ V = ∅
⊢ map (fun x => (x.1⁻¹, x.2⁻¹)) (𝓤 𝕜 ⊓ p ×ˢ q) ≤ 𝓤 𝕜

State before:
case intro.intro.intro.intro
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p✝ : Filter ι
mf mg : ℝ
p q : Filter 𝕜
hp : p ⊓ 𝓝 0 = ⊥
hq : q ⊓ 𝓝 0 = ⊥
U : Set 𝕜
hU : U ∈ p
V : Set 𝕜
hV : V ∈ 𝓝 0
hUV : U ∩ V = ∅
⊢ map (fun x => (x.1⁻¹, x.2⁻¹)) (𝓤 𝕜 ⊓ p ×ˢ q) ≤ 𝓤 𝕜
Tactic:
obtain ⟨U', hU', V', hV', hUV'⟩ := inf_eq_bot_iff.mp hq
State after:
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p✝ : Filter ι
mf mg : ℝ
p q : Filter 𝕜
hp : p ⊓ 𝓝 0 = ⊥
hq : q ⊓ 𝓝 0 = ⊥
U : Set 𝕜
hU : U ∈ p
V : Set 𝕜
hV : V ∈ 𝓝 0
hUV : U ∩ V = ∅
U' : Set 𝕜
hU' : U' ∈ q
V' : Set 𝕜
hV' : V' ∈ 𝓝 0
hUV' : U' ∩ V' = ∅
⊢ map (fun x => (x.1⁻¹, x.2⁻¹)) (𝓤 𝕜 ⊓ p ×ˢ q) ≤ 𝓤 𝕜

State before:
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p✝ : Filter ι
mf mg : ℝ
p q : Filter 𝕜
hp : p ⊓ 𝓝 0 = ⊥
hq : q ⊓ 𝓝 0 = ⊥
U : Set 𝕜
hU : U ∈ p
V : Set 𝕜
hV : V ∈ 𝓝 0
hUV : U ∩ V = ∅
U' : Set 𝕜
hU' : U' ∈ q
V' : Set 𝕜
hV' : V' ∈ 𝓝 0
hUV' : U' ∩ V' = ∅
⊢ map (fun x => (x.1⁻¹, x.2⁻¹)) (𝓤 𝕜 ⊓ p ×ˢ q) ≤ 𝓤 𝕜
Tactic:
obtain ⟨η, hη, hV⟩ := Metric.mem_nhds_iff.mp hV
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η✝ η' : ℝ
p✝ : Filter ι
mf mg : ℝ
p q : Filter 𝕜
hp : p ⊓ 𝓝 0 = ⊥
hq : q ⊓ 𝓝 0 = ⊥
U : Set 𝕜
hU : U ∈ p
V : Set 𝕜
hV✝ : V ∈ 𝓝 0
hUV : U ∩ V = ∅
U' : Set 𝕜
hU' : U' ∈ q
V' : Set 𝕜
hV' : V' ∈ 𝓝 0
hUV' : U' ∩ V' = ∅
η : ℝ
hη : η > 0
hV : ball 0 η ⊆ V
⊢ map (fun x => (x.1⁻¹, x.2⁻¹)) (𝓤 𝕜 ⊓ p ×ˢ q) ≤ 𝓤 𝕜

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η✝ η' : ℝ
p✝ : Filter ι
mf mg : ℝ
p q : Filter 𝕜
hp : p ⊓ 𝓝 0 = ⊥
hq : q ⊓ 𝓝 0 = ⊥
U : Set 𝕜
hU : U ∈ p
V : Set 𝕜
hV✝ : V ∈ 𝓝 0
hUV : U ∩ V = ∅
U' : Set 𝕜
hU' : U' ∈ q
V' : Set 𝕜
hV' : V' ∈ 𝓝 0
hUV' : U' ∩ V' = ∅
η : ℝ
hη : η > 0
hV : ball 0 η ⊆ V
⊢ map (fun x => (x.1⁻¹, x.2⁻¹)) (𝓤 𝕜 ⊓ p ×ˢ q) ≤ 𝓤 𝕜
Tactic:
obtain ⟨η', hη', hV'⟩ := Metric.mem_nhds_iff.mp hV'
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η✝ η'✝ : ℝ
p✝ : Filter ι
mf mg : ℝ
p q : Filter 𝕜
hp : p ⊓ 𝓝 0 = ⊥
hq : q ⊓ 𝓝 0 = ⊥
U : Set 𝕜
hU : U ∈ p
V : Set 𝕜
hV✝ : V ∈ 𝓝 0
hUV : U ∩ V = ∅
U' : Set 𝕜
hU' : U' ∈ q
V' : Set 𝕜
hV'✝ : V' ∈ 𝓝 0
hUV' : U' ∩ V' = ∅
η : ℝ
hη : η > 0
hV : ball 0 η ⊆ V
η' : ℝ
hη' : η' > 0
hV' : ball 0 η' ⊆ V'
⊢ map (fun x => (x.1⁻¹, x.2⁻¹)) (𝓤 𝕜 ⊓ p ×ˢ q) ≤ 𝓤 𝕜

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η✝ η'✝ : ℝ
p✝ : Filter ι
mf mg : ℝ
p q : Filter 𝕜
hp : p ⊓ 𝓝 0 = ⊥
hq : q ⊓ 𝓝 0 = ⊥
U : Set 𝕜
hU : U ∈ p
V : Set 𝕜
hV✝ : V ∈ 𝓝 0
hUV : U ∩ V = ∅
U' : Set 𝕜
hU' : U' ∈ q
V' : Set 𝕜
hV'✝ : V' ∈ 𝓝 0
hUV' : U' ∩ V' = ∅
η : ℝ
hη : η > 0
hV : ball 0 η ⊆ V
η' : ℝ
hη' : η' > 0
hV' : ball 0 η' ⊆ V'
⊢ map (fun x => (x.1⁻¹, x.2⁻¹)) (𝓤 𝕜 ⊓ p ×ˢ q) ≤ 𝓤 𝕜
Tactic:
have hηη' : 0 < η * η' := mul_pos hη hη'
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η✝ η'✝ : ℝ
p✝ : Filter ι
mf mg : ℝ
p q : Filter 𝕜
hp : p ⊓ 𝓝 0 = ⊥
hq : q ⊓ 𝓝 0 = ⊥
U : Set 𝕜
hU : U ∈ p
V : Set 𝕜
hV✝ : V ∈ 𝓝 0
hUV : U ∩ V = ∅
U' : Set 𝕜
hU' : U' ∈ q
V' : Set 𝕜
hV'✝ : V' ∈ 𝓝 0
hUV' : U' ∩ V' = ∅
η : ℝ
hη : η > 0
hV : ball 0 η ⊆ V
η' : ℝ
hη' : η' > 0
hV' : ball 0 η' ⊆ V'
hηη' : 0 < η * η'
⊢ map (fun x => (x.1⁻¹, x.2⁻¹)) (𝓤 𝕜 ⊓ p ×ˢ q) ≤ 𝓤 𝕜

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η✝ η'✝ : ℝ
p✝ : Filter ι
mf mg : ℝ
p q : Filter 𝕜
hp : p ⊓ 𝓝 0 = ⊥
hq : q ⊓ 𝓝 0 = ⊥
U : Set 𝕜
hU : U ∈ p
V : Set 𝕜
hV✝ : V ∈ 𝓝 0
hUV : U ∩ V = ∅
U' : Set 𝕜
hU' : U' ∈ q
V' : Set 𝕜
hV'✝ : V' ∈ 𝓝 0
hUV' : U' ∩ V' = ∅
η : ℝ
hη : η > 0
hV : ball 0 η ⊆ V
η' : ℝ
hη' : η' > 0
hV' : ball 0 η' ⊆ V'
hηη' : 0 < η * η'
⊢ map (fun x => (x.1⁻¹, x.2⁻¹)) (𝓤 𝕜 ⊓ p ×ˢ q) ≤ 𝓤 𝕜
Tactic:
intro u hu
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η✝ η'✝ : ℝ
p✝ : Filter ι
mf mg : ℝ
p q : Filter 𝕜
hp : p ⊓ 𝓝 0 = ⊥
hq : q ⊓ 𝓝 0 = ⊥
U : Set 𝕜
hU : U ∈ p
V : Set 𝕜
hV✝ : V ∈ 𝓝 0
hUV : U ∩ V = ∅
U' : Set 𝕜
hU' : U' ∈ q
V' : Set 𝕜
hV'✝ : V' ∈ 𝓝 0
hUV' : U' ∩ V' = ∅
η : ℝ
hη : η > 0
hV : ball 0 η ⊆ V
η' : ℝ
hη' : η' > 0
hV' : ball 0 η' ⊆ V'
hηη' : 0 < η * η'
u : Set (𝕜 × 𝕜)
hu : u ∈ 𝓤 𝕜
⊢ u ∈ map (fun x => (x.1⁻¹, x.2⁻¹)) (𝓤 𝕜 ⊓ p ×ˢ q)

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η✝ η'✝ : ℝ
p✝ : Filter ι
mf mg : ℝ
p q : Filter 𝕜
hp : p ⊓ 𝓝 0 = ⊥
hq : q ⊓ 𝓝 0 = ⊥
U : Set 𝕜
hU : U ∈ p
V : Set 𝕜
hV✝ : V ∈ 𝓝 0
hUV : U ∩ V = ∅
U' : Set 𝕜
hU' : U' ∈ q
V' : Set 𝕜
hV'✝ : V' ∈ 𝓝 0
hUV' : U' ∩ V' = ∅
η : ℝ
hη : η > 0
hV : ball 0 η ⊆ V
η' : ℝ
hη' : η' > 0
hV' : ball 0 η' ⊆ V'
hηη' : 0 < η * η'
u : Set (𝕜 × 𝕜)
hu : u ∈ 𝓤 𝕜
⊢ u ∈ map (fun x => (x.1⁻¹, x.2⁻¹)) (𝓤 𝕜 ⊓ p ×ˢ q)
Tactic:
obtain ⟨ε, hε, hu⟩ := mem_uniformity_dist.mp hu
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η✝ η'✝ : ℝ
p✝ : Filter ι
mf mg : ℝ
p q : Filter 𝕜
hp : p ⊓ 𝓝 0 = ⊥
hq : q ⊓ 𝓝 0 = ⊥
U : Set 𝕜
hU : U ∈ p
V : Set 𝕜
hV✝ : V ∈ 𝓝 0
hUV : U ∩ V = ∅
U' : Set 𝕜
hU' : U' ∈ q
V' : Set 𝕜
hV'✝ : V' ∈ 𝓝 0
hUV' : U' ∩ V' = ∅
η : ℝ
hη : η > 0
hV : ball 0 η ⊆ V
η' : ℝ
hη' : η' > 0
hV' : ball 0 η' ⊆ V'
hηη' : 0 < η * η'
u : Set (𝕜 × 𝕜)
hu✝ : u ∈ 𝓤 𝕜
ε : ℝ
hε : ε > 0
hu : ∀ {a b : 𝕜}, dist a b < ε → (a, b) ∈ u
⊢ u ∈ map (fun x => (x.1⁻¹, x.2⁻¹)) (𝓤 𝕜 ⊓ p ×ˢ q)

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η✝ η'✝ : ℝ
p✝ : Filter ι
mf mg : ℝ
p q : Filter 𝕜
hp : p ⊓ 𝓝 0 = ⊥
hq : q ⊓ 𝓝 0 = ⊥
U : Set 𝕜
hU : U ∈ p
V : Set 𝕜
hV✝ : V ∈ 𝓝 0
hUV : U ∩ V = ∅
U' : Set 𝕜
hU' : U' ∈ q
V' : Set 𝕜
hV'✝ : V' ∈ 𝓝 0
hUV' : U' ∩ V' = ∅
η : ℝ
hη : η > 0
hV : ball 0 η ⊆ V
η' : ℝ
hη' : η' > 0
hV' : ball 0 η' ⊆ V'
hηη' : 0 < η * η'
u : Set (𝕜 × 𝕜)
hu✝ : u ∈ 𝓤 𝕜
ε : ℝ
hε : ε > 0
hu : ∀ {a b : 𝕜}, dist a b < ε → (a, b) ∈ u
⊢ u ∈ map (fun x => (x.1⁻¹, x.2⁻¹)) (𝓤 𝕜 ⊓ p ×ˢ q)
Tactic:
rw [mem_map_iff_exists_image]
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η✝ η'✝ : ℝ
p✝ : Filter ι
mf mg : ℝ
p q : Filter 𝕜
hp : p ⊓ 𝓝 0 = ⊥
hq : q ⊓ 𝓝 0 = ⊥
U : Set 𝕜
hU : U ∈ p
V : Set 𝕜
hV✝ : V ∈ 𝓝 0
hUV : U ∩ V = ∅
U' : Set 𝕜
hU' : U' ∈ q
V' : Set 𝕜
hV'✝ : V' ∈ 𝓝 0
hUV' : U' ∩ V' = ∅
η : ℝ
hη : η > 0
hV : ball 0 η ⊆ V
η' : ℝ
hη' : η' > 0
hV' : ball 0 η' ⊆ V'
hηη' : 0 < η * η'
u : Set (𝕜 × 𝕜)
hu✝ : u ∈ 𝓤 𝕜
ε : ℝ
hε : ε > 0
hu : ∀ {a b : 𝕜}, dist a b < ε → (a, b) ∈ u
⊢ ∃ s ∈ 𝓤 𝕜 ⊓ p ×ˢ q, (fun x => (x.1⁻¹, x.2⁻¹)) '' s ⊆ u

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η✝ η'✝ : ℝ
p✝ : Filter ι
mf mg : ℝ
p q : Filter 𝕜
hp : p ⊓ 𝓝 0 = ⊥
hq : q ⊓ 𝓝 0 = ⊥
U : Set 𝕜
hU : U ∈ p
V : Set 𝕜
hV✝ : V ∈ 𝓝 0
hUV : U ∩ V = ∅
U' : Set 𝕜
hU' : U' ∈ q
V' : Set 𝕜
hV'✝ : V' ∈ 𝓝 0
hUV' : U' ∩ V' = ∅
η : ℝ
hη : η > 0
hV : ball 0 η ⊆ V
η' : ℝ
hη' : η' > 0
hV' : ball 0 η' ⊆ V'
hηη' : 0 < η * η'
u : Set (𝕜 × 𝕜)
hu✝ : u ∈ 𝓤 𝕜
ε : ℝ
hε : ε > 0
hu : ∀ {a b : 𝕜}, dist a b < ε → (a, b) ∈ u
⊢ ∃ s ∈ 𝓤 𝕜 ⊓ p ×ˢ q, (fun x => (x.1⁻¹, x.2⁻¹)) '' s ⊆ u
Tactic:
refine ⟨_, inter_mem_inf (dist_mem_uniformity (mul_pos hε hηη')) (prod_mem_prod hU hU'), ?_⟩
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η✝ η'✝ : ℝ
p✝ : Filter ι
mf mg : ℝ
p q : Filter 𝕜
hp : p ⊓ 𝓝 0 = ⊥
hq : q ⊓ 𝓝 0 = ⊥
U : Set 𝕜
hU : U ∈ p
V : Set 𝕜
hV✝ : V ∈ 𝓝 0
hUV : U ∩ V = ∅
U' : Set 𝕜
hU' : U' ∈ q
V' : Set 𝕜
hV'✝ : V' ∈ 𝓝 0
hUV' : U' ∩ V' = ∅
η : ℝ
hη : η > 0
hV : ball 0 η ⊆ V
η' : ℝ
hη' : η' > 0
hV' : ball 0 η' ⊆ V'
hηη' : 0 < η * η'
u : Set (𝕜 × 𝕜)
hu✝ : u ∈ 𝓤 𝕜
ε : ℝ
hε : ε > 0
hu : ∀ {a b : 𝕜}, dist a b < ε → (a, b) ∈ u
⊢ (fun x => (x.1⁻¹, x.2⁻¹)) '' ({p | dist p.1 p.2 < ε * (η * η')} ∩ U ×ˢ U') ⊆ u

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η✝ η'✝ : ℝ
p✝ : Filter ι
mf mg : ℝ
p q : Filter 𝕜
hp : p ⊓ 𝓝 0 = ⊥
hq : q ⊓ 𝓝 0 = ⊥
U : Set 𝕜
hU : U ∈ p
V : Set 𝕜
hV✝ : V ∈ 𝓝 0
hUV : U ∩ V = ∅
U' : Set 𝕜
hU' : U' ∈ q
V' : Set 𝕜
hV'✝ : V' ∈ 𝓝 0
hUV' : U' ∩ V' = ∅
η : ℝ
hη : η > 0
hV : ball 0 η ⊆ V
η' : ℝ
hη' : η' > 0
hV' : ball 0 η' ⊆ V'
hηη' : 0 < η * η'
u : Set (𝕜 × 𝕜)
hu✝ : u ∈ 𝓤 𝕜
ε : ℝ
hε : ε > 0
hu : ∀ {a b : 𝕜}, dist a b < ε → (a, b) ∈ u
⊢ (fun x => (x.1⁻¹, x.2⁻¹)) '' ({p | dist p.1 p.2 < ε * (η * η')} ∩ U ×ˢ U') ⊆ u
Tactic:
rintro z ⟨x, ⟨hx1, hx2⟩, rfl⟩
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x✝ y : 𝕜
η✝ η'✝ : ℝ
p✝ : Filter ι
mf mg : ℝ
p q : Filter 𝕜
hp : p ⊓ 𝓝 0 = ⊥
hq : q ⊓ 𝓝 0 = ⊥
U : Set 𝕜
hU : U ∈ p
V : Set 𝕜
hV✝ : V ∈ 𝓝 0
hUV : U ∩ V = ∅
U' : Set 𝕜
hU' : U' ∈ q
V' : Set 𝕜
hV'✝ : V' ∈ 𝓝 0
hUV' : U' ∩ V' = ∅
η : ℝ
hη : η > 0
hV : ball 0 η ⊆ V
η' : ℝ
hη' : η' > 0
hV' : ball 0 η' ⊆ V'
hηη' : 0 < η * η'
u : Set (𝕜 × 𝕜)
hu✝ : u ∈ 𝓤 𝕜
ε : ℝ
hε : ε > 0
hu : ∀ {a b : 𝕜}, dist a b < ε → (a, b) ∈ u
x : 𝕜 × 𝕜
hx1 : x ∈ {p | dist p.1 p.2 < ε * (η * η')}
hx2 : x ∈ U ×ˢ U'
⊢ (fun x => (x.1⁻¹, x.2⁻¹)) x ∈ u

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x✝ y : 𝕜
η✝ η'✝ : ℝ
p✝ : Filter ι
mf mg : ℝ
p q : Filter 𝕜
hp : p ⊓ 𝓝 0 = ⊥
hq : q ⊓ 𝓝 0 = ⊥
U : Set 𝕜
hU : U ∈ p
V : Set 𝕜
hV✝ : V ∈ 𝓝 0
hUV : U ∩ V = ∅
U' : Set 𝕜
hU' : U' ∈ q
V' : Set 𝕜
hV'✝ : V' ∈ 𝓝 0
hUV' : U' ∩ V' = ∅
η : ℝ
hη : η > 0
hV : ball 0 η ⊆ V
η' : ℝ
hη' : η' > 0
hV' : ball 0 η' ⊆ V'
hηη' : 0 < η * η'
u : Set (𝕜 × 𝕜)
hu✝ : u ∈ 𝓤 𝕜
ε : ℝ
hε : ε > 0
hu : ∀ {a b : 𝕜}, dist a b < ε → (a, b) ∈ u
x : 𝕜 × 𝕜
hx1 : x ∈ {p | dist p.1 p.2 < ε * (η * η')}
hx2 : x ∈ U ×ˢ U'
⊢ (fun x => (x.1⁻¹, x.2⁻¹)) x ∈ u
Tactic:
have hx'1 : x.1 ∉ ball (0 : 𝕜) η :=
  λ h => (Set.nonempty_of_mem (mem_inter hx2.1 (hV h))).ne_empty hUV
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x✝ y : 𝕜
η✝ η'✝ : ℝ
p✝ : Filter ι
mf mg : ℝ
p q : Filter 𝕜
hp : p ⊓ 𝓝 0 = ⊥
hq : q ⊓ 𝓝 0 = ⊥
U : Set 𝕜
hU : U ∈ p
V : Set 𝕜
hV✝ : V ∈ 𝓝 0
hUV : U ∩ V = ∅
U' : Set 𝕜
hU' : U' ∈ q
V' : Set 𝕜
hV'✝ : V' ∈ 𝓝 0
hUV' : U' ∩ V' = ∅
η : ℝ
hη : η > 0
hV : ball 0 η ⊆ V
η' : ℝ
hη' : η' > 0
hV' : ball 0 η' ⊆ V'
hηη' : 0 < η * η'
u : Set (𝕜 × 𝕜)
hu✝ : u ∈ 𝓤 𝕜
ε : ℝ
hε : ε > 0
hu : ∀ {a b : 𝕜}, dist a b < ε → (a, b) ∈ u
x : 𝕜 × 𝕜
hx1 : x ∈ {p | dist p.1 p.2 < ε * (η * η')}
hx2 : x ∈ U ×ˢ U'
hx'1 : x.1 ∉ ball 0 η
⊢ (fun x => (x.1⁻¹, x.2⁻¹)) x ∈ u

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x✝ y : 𝕜
η✝ η'✝ : ℝ
p✝ : Filter ι
mf mg : ℝ
p q : Filter 𝕜
hp : p ⊓ 𝓝 0 = ⊥
hq : q ⊓ 𝓝 0 = ⊥
U : Set 𝕜
hU : U ∈ p
V : Set 𝕜
hV✝ : V ∈ 𝓝 0
hUV : U ∩ V = ∅
U' : Set 𝕜
hU' : U' ∈ q
V' : Set 𝕜
hV'✝ : V' ∈ 𝓝 0
hUV' : U' ∩ V' = ∅
η : ℝ
hη : η > 0
hV : ball 0 η ⊆ V
η' : ℝ
hη' : η' > 0
hV' : ball 0 η' ⊆ V'
hηη' : 0 < η * η'
u : Set (𝕜 × 𝕜)
hu✝ : u ∈ 𝓤 𝕜
ε : ℝ
hε : ε > 0
hu : ∀ {a b : 𝕜}, dist a b < ε → (a, b) ∈ u
x : 𝕜 × 𝕜
hx1 : x ∈ {p | dist p.1 p.2 < ε * (η * η')}
hx2 : x ∈ U ×ˢ U'
hx'1 : x.1 ∉ ball 0 η
⊢ (fun x => (x.1⁻¹, x.2⁻¹)) x ∈ u
Tactic:
have hx'2 : x.2 ∉ ball (0 : 𝕜) η' :=
  λ h => (Set.nonempty_of_mem (mem_inter hx2.2 (hV' h))).ne_empty hUV'
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x✝ y : 𝕜
η✝ η'✝ : ℝ
p✝ : Filter ι
mf mg : ℝ
p q : Filter 𝕜
hp : p ⊓ 𝓝 0 = ⊥
hq : q ⊓ 𝓝 0 = ⊥
U : Set 𝕜
hU : U ∈ p
V : Set 𝕜
hV✝ : V ∈ 𝓝 0
hUV : U ∩ V = ∅
U' : Set 𝕜
hU' : U' ∈ q
V' : Set 𝕜
hV'✝ : V' ∈ 𝓝 0
hUV' : U' ∩ V' = ∅
η : ℝ
hη : η > 0
hV : ball 0 η ⊆ V
η' : ℝ
hη' : η' > 0
hV' : ball 0 η' ⊆ V'
hηη' : 0 < η * η'
u : Set (𝕜 × 𝕜)
hu✝ : u ∈ 𝓤 𝕜
ε : ℝ
hε : ε > 0
hu : ∀ {a b : 𝕜}, dist a b < ε → (a, b) ∈ u
x : 𝕜 × 𝕜
hx1 : x ∈ {p | dist p.1 p.2 < ε * (η * η')}
hx2 : x ∈ U ×ˢ U'
hx'1 : x.1 ∉ ball 0 η
hx'2 : x.2 ∉ ball 0 η'
⊢ (fun x => (x.1⁻¹, x.2⁻¹)) x ∈ u

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x✝ y : 𝕜
η✝ η'✝ : ℝ
p✝ : Filter ι
mf mg : ℝ
p q : Filter 𝕜
hp : p ⊓ 𝓝 0 = ⊥
hq : q ⊓ 𝓝 0 = ⊥
U : Set 𝕜
hU : U ∈ p
V : Set 𝕜
hV✝ : V ∈ 𝓝 0
hUV : U ∩ V = ∅
U' : Set 𝕜
hU' : U' ∈ q
V' : Set 𝕜
hV'✝ : V' ∈ 𝓝 0
hUV' : U' ∩ V' = ∅
η : ℝ
hη : η > 0
hV : ball 0 η ⊆ V
η' : ℝ
hη' : η' > 0
hV' : ball 0 η' ⊆ V'
hηη' : 0 < η * η'
u : Set (𝕜 × 𝕜)
hu✝ : u ∈ 𝓤 𝕜
ε : ℝ
hε : ε > 0
hu : ∀ {a b : 𝕜}, dist a b < ε → (a, b) ∈ u
x : 𝕜 × 𝕜
hx1 : x ∈ {p | dist p.1 p.2 < ε * (η * η')}
hx2 : x ∈ U ×ˢ U'
hx'1 : x.1 ∉ ball 0 η
hx'2 : x.2 ∉ ball 0 η'
⊢ (fun x => (x.1⁻¹, x.2⁻¹)) x ∈ u
Tactic:
refine hu ((dist_inv_le_dist_div hη hη' hx'1 hx'2).trans_lt ?_)
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x✝ y : 𝕜
η✝ η'✝ : ℝ
p✝ : Filter ι
mf mg : ℝ
p q : Filter 𝕜
hp : p ⊓ 𝓝 0 = ⊥
hq : q ⊓ 𝓝 0 = ⊥
U : Set 𝕜
hU : U ∈ p
V : Set 𝕜
hV✝ : V ∈ 𝓝 0
hUV : U ∩ V = ∅
U' : Set 𝕜
hU' : U' ∈ q
V' : Set 𝕜
hV'✝ : V' ∈ 𝓝 0
hUV' : U' ∩ V' = ∅
η : ℝ
hη : η > 0
hV : ball 0 η ⊆ V
η' : ℝ
hη' : η' > 0
hV' : ball 0 η' ⊆ V'
hηη' : 0 < η * η'
u : Set (𝕜 × 𝕜)
hu✝ : u ∈ 𝓤 𝕜
ε : ℝ
hε : ε > 0
hu : ∀ {a b : 𝕜}, dist a b < ε → (a, b) ∈ u
x : 𝕜 × 𝕜
hx1 : x ∈ {p | dist p.1 p.2 < ε * (η * η')}
hx2 : x ∈ U ×ˢ U'
hx'1 : x.1 ∉ ball 0 η
hx'2 : x.2 ∉ ball 0 η'
⊢ dist x.1 x.2 / (η * η') < ε

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x✝ y : 𝕜
η✝ η'✝ : ℝ
p✝ : Filter ι
mf mg : ℝ
p q : Filter 𝕜
hp : p ⊓ 𝓝 0 = ⊥
hq : q ⊓ 𝓝 0 = ⊥
U : Set 𝕜
hU : U ∈ p
V : Set 𝕜
hV✝ : V ∈ 𝓝 0
hUV : U ∩ V = ∅
U' : Set 𝕜
hU' : U' ∈ q
V' : Set 𝕜
hV'✝ : V' ∈ 𝓝 0
hUV' : U' ∩ V' = ∅
η : ℝ
hη : η > 0
hV : ball 0 η ⊆ V
η' : ℝ
hη' : η' > 0
hV' : ball 0 η' ⊆ V'
hηη' : 0 < η * η'
u : Set (𝕜 × 𝕜)
hu✝ : u ∈ 𝓤 𝕜
ε : ℝ
hε : ε > 0
hu : ∀ {a b : 𝕜}, dist a b < ε → (a, b) ∈ u
x : 𝕜 × 𝕜
hx1 : x ∈ {p | dist p.1 p.2 < ε * (η * η')}
hx2 : x ∈ U ×ˢ U'
hx'1 : x.1 ∉ ball 0 η
hx'2 : x.2 ∉ ball 0 η'
⊢ dist x.1 x.2 / (η * η') < ε
Tactic:
convert (div_lt_div_right hηη').mpr hx1
State after:
case h.e'_4
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x✝ y : 𝕜
η✝ η'✝ : ℝ
p✝ : Filter ι
mf mg : ℝ
p q : Filter 𝕜
hp : p ⊓ 𝓝 0 = ⊥
hq : q ⊓ 𝓝 0 = ⊥
U : Set 𝕜
hU : U ∈ p
V : Set 𝕜
hV✝ : V ∈ 𝓝 0
hUV : U ∩ V = ∅
U' : Set 𝕜
hU' : U' ∈ q
V' : Set 𝕜
hV'✝ : V' ∈ 𝓝 0
hUV' : U' ∩ V' = ∅
η : ℝ
hη : η > 0
hV : ball 0 η ⊆ V
η' : ℝ
hη' : η' > 0
hV' : ball 0 η' ⊆ V'
hηη' : 0 < η * η'
u : Set (𝕜 × 𝕜)
hu✝ : u ∈ 𝓤 𝕜
ε : ℝ
hε : ε > 0
hu : ∀ {a b : 𝕜}, dist a b < ε → (a, b) ∈ u
x : 𝕜 × 𝕜
hx1 : x ∈ {p | dist p.1 p.2 < ε * (η * η')}
hx2 : x ∈ U ×ˢ U'
hx'1 : x.1 ∉ ball 0 η
hx'2 : x.2 ∉ ball 0 η'
⊢ ε = ε * (η * η') / (η * η')

State before:
case h.e'_4
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x✝ y : 𝕜
η✝ η'✝ : ℝ
p✝ : Filter ι
mf mg : ℝ
p q : Filter 𝕜
hp : p ⊓ 𝓝 0 = ⊥
hq : q ⊓ 𝓝 0 = ⊥
U : Set 𝕜
hU : U ∈ p
V : Set 𝕜
hV✝ : V ∈ 𝓝 0
hUV : U ∩ V = ∅
U' : Set 𝕜
hU' : U' ∈ q
V' : Set 𝕜
hV'✝ : V' ∈ 𝓝 0
hUV' : U' ∩ V' = ∅
η : ℝ
hη : η > 0
hV : ball 0 η ⊆ V
η' : ℝ
hη' : η' > 0
hV' : ball 0 η' ⊆ V'
hηη' : 0 < η * η'
u : Set (𝕜 × 𝕜)
hu✝ : u ∈ 𝓤 𝕜
ε : ℝ
hε : ε > 0
hu : ∀ {a b : 𝕜}, dist a b < ε → (a, b) ∈ u
x : 𝕜 × 𝕜
hx1 : x ∈ {p | dist p.1 p.2 < ε * (η * η')}
hx2 : x ∈ U ×ˢ U'
hx'1 : x.1 ∉ ball 0 η
hx'2 : x.2 ∉ ball 0 η'
⊢ ε = ε * (η * η') / (η * η')
Tactic:
field_simp [hη.lt.ne.symm, hη'.lt.ne.symm]
State after:
no goals