-- Mathlib/Topology/Algebra/Nonarchimedean/Basic.lean
theorem mul_subset (U : OpenAddSubgroup R) : ∃ V : OpenAddSubgroup R, (V : Set R) * V ⊆ U

Proof state:
case h.intro.intro.intro.intro
R : Type u_1
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : NonarchimedeanRing R
U V : OpenAddSubgroup R
H : ↑V ×ˢ ↑V ⊆ (fun p => p.1 * p.2) ⁻¹' ↑U
v a : R
ha : a ∈ ↑V
b : R
hb : b ∈ ↑V
hv : (fun x1 x2 => x1 * x2) a b = v
⊢ v ∈ ↑U

Tactic:
have hy := H (Set.mk_mem_prod ha hb)

Result:
case h.intro.intro.intro.intro
R : Type u_1
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : NonarchimedeanRing R
U V : OpenAddSubgroup R
H : ↑V ×ˢ ↑V ⊆ (fun p => p.1 * p.2) ⁻¹' ↑U
v a : R
ha : a ∈ ↑V
b : R
hb : b ∈ ↑V
hv : (fun x1 x2 => x1 * x2) a b = v
hy : (a, b) ∈ (fun p => p.1 * p.2) ⁻¹' ↑U
⊢ v ∈ ↑U

Proof state:
case h
R : Type u_1
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : NonarchimedeanRing R
U V : OpenAddSubgroup R
H : ↑V ×ˢ ↑V ⊆ (fun p => p.1 * p.2) ⁻¹' ↑U
⊢ ↑V * ↑V ⊆ ↑U

Tactic:
rintro v ⟨a, ha, b, hb, hv⟩

Result:
case h.intro.intro.intro.intro
R : Type u_1
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : NonarchimedeanRing R
U V : OpenAddSubgroup R
H : ↑V ×ˢ ↑V ⊆ (fun p => p.1 * p.2) ⁻¹' ↑U
v a : R
ha : a ∈ ↑V
b : R
hb : b ∈ ↑V
hv : (fun x1 x2 => x1 * x2) a b = v
⊢ v ∈ ↑U

Proof state:
R : Type u_1
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : NonarchimedeanRing R
U : OpenAddSubgroup R
⊢ ∃ V, ↑V * ↑V ⊆ ↑U

Tactic:
let ⟨V, H⟩ := prod_self_subset <| (U.isOpen.preimage continuous_mul).mem_nhds <| by
  simpa only [Set.mem_preimage, Prod.snd_zero, mul_zero] using U.zero_mem

Result:
R : Type u_1
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : NonarchimedeanRing R
U V : OpenAddSubgroup R
H : ↑V ×ˢ ↑V ⊆ (fun p => p.1 * p.2) ⁻¹' ↑U
⊢ ∃ V, ↑V * ↑V ⊆ ↑U

Proof state:
case h.intro.intro.intro.intro
R : Type u_1
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : NonarchimedeanRing R
U V : OpenAddSubgroup R
H : ↑V ×ˢ ↑V ⊆ (fun p => p.1 * p.2) ⁻¹' ↑U
v a : R
ha : a ∈ ↑V
b : R
hb : b ∈ ↑V
hv : (fun x1 x2 => x1 * x2) a b = v
hy : v ∈ U
⊢ v ∈ U

Tactic:
exact hy

Result:
no goals

Proof state:
R : Type u_1
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : NonarchimedeanRing R
U : OpenAddSubgroup R
⊢ 0 ∈ (fun p => p.1 * p.2) ⁻¹' ↑U

Tactic:
simpa only [Set.mem_preimage, Prod.snd_zero, mul_zero] using U.zero_mem

Result:
no goals

Proof state:
case h.intro.intro.intro.intro
R : Type u_1
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : NonarchimedeanRing R
U V : OpenAddSubgroup R
H : ↑V ×ˢ ↑V ⊆ (fun p => p.1 * p.2) ⁻¹' ↑U
v a : R
ha : a ∈ ↑V
b : R
hb : b ∈ ↑V
hv : (fun x1 x2 => x1 * x2) a b = v
hy : (a, b) ∈ (fun p => p.1 * p.2) ⁻¹' ↑U
⊢ v ∈ ↑U

Tactic:
simp only [Set.mem_preimage, SetLike.mem_coe, hv] at hy

Result:
case h.intro.intro.intro.intro
R : Type u_1
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : NonarchimedeanRing R
U V : OpenAddSubgroup R
H : ↑V ×ˢ ↑V ⊆ (fun p => p.1 * p.2) ⁻¹' ↑U
v a : R
ha : a ∈ ↑V
b : R
hb : b ∈ ↑V
hv : (fun x1 x2 => x1 * x2) a b = v
hy : v ∈ U
⊢ v ∈ ↑U

Proof state:
case h.intro.intro.intro.intro
R : Type u_1
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : NonarchimedeanRing R
U V : OpenAddSubgroup R
H : ↑V ×ˢ ↑V ⊆ (fun p => p.1 * p.2) ⁻¹' ↑U
v a : R
ha : a ∈ ↑V
b : R
hb : b ∈ ↑V
hv : (fun x1 x2 => x1 * x2) a b = v
hy : v ∈ U
⊢ v ∈ ↑U

Tactic:
rw [SetLike.mem_coe]

Result:
case h.intro.intro.intro.intro
R : Type u_1
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : NonarchimedeanRing R
U V : OpenAddSubgroup R
H : ↑V ×ˢ ↑V ⊆ (fun p => p.1 * p.2) ⁻¹' ↑U
v a : R
ha : a ∈ ↑V
b : R
hb : b ∈ ↑V
hv : (fun x1 x2 => x1 * x2) a b = v
hy : v ∈ U
⊢ v ∈ U

Proof state:
R : Type u_1
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : NonarchimedeanRing R
U V : OpenAddSubgroup R
H : ↑V ×ˢ ↑V ⊆ (fun p => p.1 * p.2) ⁻¹' ↑U
⊢ ∃ V, ↑V * ↑V ⊆ ↑U

Tactic:
use V

Result:
case h
R : Type u_1
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : NonarchimedeanRing R
U V : OpenAddSubgroup R
H : ↑V ×ˢ ↑V ⊆ (fun p => p.1 * p.2) ⁻¹' ↑U
⊢ ↑V * ↑V ⊆ ↑U