R : Type u_1
S : Type ?u.66384
inst✝⁵ : Ring R
inst✝⁴ : TopologicalSpace R
inst✝³ : NonarchimedeanRing R
inst✝² : Ring S
inst✝¹ : TopologicalSpace S
inst✝ : NonarchimedeanRing S
U V : OpenAddSubgroup R
H : ↑V ×ˢ ↑V ⊆ (fun p => p.fst * p.snd) ⁻¹' ↑U
⊢ ∃ V, ↑V * ↑V ⊆ ↑U
R : Type u_1
S : Type ?u.66384
inst✝⁵ : Ring R
inst✝⁴ : TopologicalSpace R
inst✝³ : NonarchimedeanRing R
inst✝² : Ring S
inst✝¹ : TopologicalSpace S
inst✝ : NonarchimedeanRing S
U : OpenAddSubgroup R
⊢ ∃ V, ↑V * ↑V ⊆ ↑U
let ⟨V, H⟩ :=
  prod_self_subset
    (IsOpen.mem_nhds (IsOpen.preimage continuous_mul U.isOpen)
      (by simpa only [Set.mem_preimage, SetLike.mem_coe, Prod.snd_zero,
          MulZeroClass.mul_zero] using U.zero_mem))
R : Type u_1
S : Type ?u.66384
inst✝⁵ : Ring R
inst✝⁴ : TopologicalSpace R
inst✝³ : NonarchimedeanRing R
inst✝² : Ring S
inst✝¹ : TopologicalSpace S
inst✝ : NonarchimedeanRing S
U V : OpenAddSubgroup R
H : ↑V ×ˢ ↑V ⊆ (fun p => p.fst * p.snd) ⁻¹' ↑U
⊢ ↑V * ↑V ⊆ ↑U
R : Type u_1
S : Type ?u.66384
inst✝⁵ : Ring R
inst✝⁴ : TopologicalSpace R
inst✝³ : NonarchimedeanRing R
inst✝² : Ring S
inst✝¹ : TopologicalSpace S
inst✝ : NonarchimedeanRing S
U V : OpenAddSubgroup R
H : ↑V ×ˢ ↑V ⊆ (fun p => p.fst * p.snd) ⁻¹' ↑U
⊢ ∃ V, ↑V * ↑V ⊆ ↑U
use V
case intro.intro.intro.intro
R : Type u_1
S : Type ?u.66384
inst✝⁵ : Ring R
inst✝⁴ : TopologicalSpace R
inst✝³ : NonarchimedeanRing R
inst✝² : Ring S
inst✝¹ : TopologicalSpace S
inst✝ : NonarchimedeanRing S
U V : OpenAddSubgroup R
H : ↑V ×ˢ ↑V ⊆ (fun p => p.fst * p.snd) ⁻¹' ↑U
v a b : R
ha : a ∈ ↑V
hb : b ∈ ↑V
hv : (fun x x_1 => x * x_1) a b = v
⊢ v ∈ ↑U
R : Type u_1
S : Type ?u.66384
inst✝⁵ : Ring R
inst✝⁴ : TopologicalSpace R
inst✝³ : NonarchimedeanRing R
inst✝² : Ring S
inst✝¹ : TopologicalSpace S
inst✝ : NonarchimedeanRing S
U V : OpenAddSubgroup R
H : ↑V ×ˢ ↑V ⊆ (fun p => p.fst * p.snd) ⁻¹' ↑U
⊢ ↑V * ↑V ⊆ ↑U
rintro v ⟨a, b, ha, hb, hv⟩
case intro.intro.intro.intro
R : Type u_1
S : Type ?u.66384
inst✝⁵ : Ring R
inst✝⁴ : TopologicalSpace R
inst✝³ : NonarchimedeanRing R
inst✝² : Ring S
inst✝¹ : TopologicalSpace S
inst✝ : NonarchimedeanRing S
U V : OpenAddSubgroup R
H : ↑V ×ˢ ↑V ⊆ (fun p => p.fst * p.snd) ⁻¹' ↑U
v a b : R
ha : a ∈ ↑V
hb : b ∈ ↑V
hv : (fun x x_1 => x * x_1) a b = v
hy : (a, b) ∈ (fun p => p.fst * p.snd) ⁻¹' ↑U
⊢ v ∈ ↑U
case intro.intro.intro.intro
R : Type u_1
S : Type ?u.66384
inst✝⁵ : Ring R
inst✝⁴ : TopologicalSpace R
inst✝³ : NonarchimedeanRing R
inst✝² : Ring S
inst✝¹ : TopologicalSpace S
inst✝ : NonarchimedeanRing S
U V : OpenAddSubgroup R
H : ↑V ×ˢ ↑V ⊆ (fun p => p.fst * p.snd) ⁻¹' ↑U
v a b : R
ha : a ∈ ↑V
hb : b ∈ ↑V
hv : (fun x x_1 => x * x_1) a b = v
⊢ v ∈ ↑U
have hy := H (Set.mk_mem_prod ha hb)
case intro.intro.intro.intro
R : Type u_1
S : Type ?u.66384
inst✝⁵ : Ring R
inst✝⁴ : TopologicalSpace R
inst✝³ : NonarchimedeanRing R
inst✝² : Ring S
inst✝¹ : TopologicalSpace S
inst✝ : NonarchimedeanRing S
U V : OpenAddSubgroup R
H : ↑V ×ˢ ↑V ⊆ (fun p => p.fst * p.snd) ⁻¹' ↑U
v a b : R
ha : a ∈ ↑V
hb : b ∈ ↑V
hv : (fun x x_1 => x * x_1) a b = v
hy : v ∈ U
⊢ v ∈ ↑U
case intro.intro.intro.intro
R : Type u_1
S : Type ?u.66384
inst✝⁵ : Ring R
inst✝⁴ : TopologicalSpace R
inst✝³ : NonarchimedeanRing R
inst✝² : Ring S
inst✝¹ : TopologicalSpace S
inst✝ : NonarchimedeanRing S
U V : OpenAddSubgroup R
H : ↑V ×ˢ ↑V ⊆ (fun p => p.fst * p.snd) ⁻¹' ↑U
v a b : R
ha : a ∈ ↑V
hb : b ∈ ↑V
hv : (fun x x_1 => x * x_1) a b = v
hy : (a, b) ∈ (fun p => p.fst * p.snd) ⁻¹' ↑U
⊢ v ∈ ↑U
simp only [Set.mem_preimage, SetLike.mem_coe, hv] at hy
case intro.intro.intro.intro
R : Type u_1
S : Type ?u.66384
inst✝⁵ : Ring R
inst✝⁴ : TopologicalSpace R
inst✝³ : NonarchimedeanRing R
inst✝² : Ring S
inst✝¹ : TopologicalSpace S
inst✝ : NonarchimedeanRing S
U V : OpenAddSubgroup R
H : ↑V ×ˢ ↑V ⊆ (fun p => p.fst * p.snd) ⁻¹' ↑U
v a b : R
ha : a ∈ ↑V
hb : b ∈ ↑V
hv : (fun x x_1 => x * x_1) a b = v
hy : v ∈ U
⊢ v ∈ U
case intro.intro.intro.intro
R : Type u_1
S : Type ?u.66384
inst✝⁵ : Ring R
inst✝⁴ : TopologicalSpace R
inst✝³ : NonarchimedeanRing R
inst✝² : Ring S
inst✝¹ : TopologicalSpace S
inst✝ : NonarchimedeanRing S
U V : OpenAddSubgroup R
H : ↑V ×ˢ ↑V ⊆ (fun p => p.fst * p.snd) ⁻¹' ↑U
v a b : R
ha : a ∈ ↑V
hb : b ∈ ↑V
hv : (fun x x_1 => x * x_1) a b = v
hy : v ∈ U
⊢ v ∈ ↑U
rw [SetLike.mem_coe]
no goals
case intro.intro.intro.intro
R : Type u_1
S : Type ?u.66384
inst✝⁵ : Ring R
inst✝⁴ : TopologicalSpace R
inst✝³ : NonarchimedeanRing R
inst✝² : Ring S
inst✝¹ : TopologicalSpace S
inst✝ : NonarchimedeanRing S
U V : OpenAddSubgroup R
H : ↑V ×ˢ ↑V ⊆ (fun p => p.fst * p.snd) ⁻¹' ↑U
v a b : R
ha : a ∈ ↑V
hb : b ∈ ↑V
hv : (fun x x_1 => x * x_1) a b = v
hy : v ∈ U
⊢ v ∈ U
exact hy
no goals
R : Type u_1
S : Type ?u.66384
inst✝⁵ : Ring R
inst✝⁴ : TopologicalSpace R
inst✝³ : NonarchimedeanRing R
inst✝² : Ring S
inst✝¹ : TopologicalSpace S
inst✝ : NonarchimedeanRing S
U : OpenAddSubgroup R
⊢ 0 ∈ (fun p => p.fst * p.snd) ⁻¹' ↑U
simpa only [Set.mem_preimage, SetLike.mem_coe, Prod.snd_zero,
MulZeroClass.mul_zero] using U.zero_mem