[GOAL]
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
⊢ ∀ (i j : Γ₀ˣ), ∃ k, ltAddSubgroup v k ≤ ltAddSubgroup v i ⊓ ltAddSubgroup v j
[PROOFSTEP]
rintro γ₀ γ₁
[GOAL]
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ₀ γ₁ : Γ₀ˣ
⊢ ∃ k, ltAddSubgroup v k ≤ ltAddSubgroup v γ₀ ⊓ ltAddSubgroup v γ₁
[PROOFSTEP]
use min γ₀ γ₁
[GOAL]
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ₀ γ₁ : Γ₀ˣ
⊢ ltAddSubgroup v (min γ₀ γ₁) ≤ ltAddSubgroup v γ₀ ⊓ ltAddSubgroup v γ₁
[PROOFSTEP]
simp [Valuation.ltAddSubgroup]
[GOAL]
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ₀ γ₁ : Γ₀ˣ
⊢ ∀ (a : R), ↑v a < ↑γ₀ → ↑v a < ↑γ₁ → ↑v a < ↑γ₀
[PROOFSTEP]
tauto
[GOAL]
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
⊢ ∀ (i : Γ₀ˣ), ∃ j, ↑(ltAddSubgroup v j) * ↑(ltAddSubgroup v j) ⊆ ↑(ltAddSubgroup v i)
[PROOFSTEP]
rintro γ
[GOAL]
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ : Γ₀ˣ
⊢ ∃ j, ↑(ltAddSubgroup v j) * ↑(ltAddSubgroup v j) ⊆ ↑(ltAddSubgroup v γ)
[PROOFSTEP]
cases' exists_square_le γ with γ₀ h
[GOAL]
case intro
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ γ₀ : Γ₀ˣ
h : γ₀ * γ₀ ≤ γ
⊢ ∃ j, ↑(ltAddSubgroup v j) * ↑(ltAddSubgroup v j) ⊆ ↑(ltAddSubgroup v γ)
[PROOFSTEP]
use γ₀
[GOAL]
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ γ₀ : Γ₀ˣ
h : γ₀ * γ₀ ≤ γ
⊢ ↑(ltAddSubgroup v γ₀) * ↑(ltAddSubgroup v γ₀) ⊆ ↑(ltAddSubgroup v γ)
[PROOFSTEP]
rintro - ⟨r, s, r_in, s_in, rfl⟩
[GOAL]
case h.intro.intro.intro.intro
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ γ₀ : Γ₀ˣ
h : γ₀ * γ₀ ≤ γ
r s : R
r_in : r ∈ ↑(ltAddSubgroup v γ₀)
s_in : s ∈ ↑(ltAddSubgroup v γ₀)
⊢ (fun x x_1 => x * x_1) r s ∈ ↑(ltAddSubgroup v γ)
[PROOFSTEP]
calc
  (v (r * s) : Γ₀) = v r * v s := Valuation.map_mul _ _ _
  _ < γ₀ * γ₀ := (mul_lt_mul₀ r_in s_in)
  _ ≤ γ := by exact_mod_cast h
[GOAL]
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ γ₀ : Γ₀ˣ
h : γ₀ * γ₀ ≤ γ
r s : R
r_in : r ∈ ↑(ltAddSubgroup v γ₀)
s_in : s ∈ ↑(ltAddSubgroup v γ₀)
⊢ ↑γ₀ * ↑γ₀ ≤ ↑γ
[PROOFSTEP]
exact_mod_cast h
[GOAL]
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
⊢ ∀ (x : R) (i : Γ₀ˣ), ∃ j, ↑(ltAddSubgroup v j) ⊆ (fun x_1 => x * x_1) ⁻¹' ↑(ltAddSubgroup v i)
[PROOFSTEP]
rintro x γ
[GOAL]
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : Γ₀ˣ
⊢ ∃ j, ↑(ltAddSubgroup v j) ⊆ (fun x_1 => x * x_1) ⁻¹' ↑(ltAddSubgroup v γ)
[PROOFSTEP]
rcases GroupWithZero.eq_zero_or_unit (v x) with (Hx | ⟨γx, Hx⟩)
[GOAL]
case inl
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : Γ₀ˣ
Hx : ↑v x = 0
⊢ ∃ j, ↑(ltAddSubgroup v j) ⊆ (fun x_1 => x * x_1) ⁻¹' ↑(ltAddSubgroup v γ)
[PROOFSTEP]
use(1 : Γ₀ˣ)
[GOAL]
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : Γ₀ˣ
Hx : ↑v x = 0
⊢ ↑(ltAddSubgroup v 1) ⊆ (fun x_1 => x * x_1) ⁻¹' ↑(ltAddSubgroup v γ)
[PROOFSTEP]
rintro y _
[GOAL]
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : Γ₀ˣ
Hx : ↑v x = 0
y : R
a✝ : y ∈ ↑(ltAddSubgroup v 1)
⊢ y ∈ (fun x_1 => x * x_1) ⁻¹' ↑(ltAddSubgroup v γ)
[PROOFSTEP]
change v (x * y) < _
[GOAL]
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : Γ₀ˣ
Hx : ↑v x = 0
y : R
a✝ : y ∈ ↑(ltAddSubgroup v 1)
⊢ ↑v (x * y) < ↑γ
[PROOFSTEP]
rw [Valuation.map_mul, Hx, zero_mul]
[GOAL]
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : Γ₀ˣ
Hx : ↑v x = 0
y : R
a✝ : y ∈ ↑(ltAddSubgroup v 1)
⊢ 0 < ↑γ
[PROOFSTEP]
exact Units.zero_lt γ
[GOAL]
case inr.intro
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : Γ₀ˣ
γx : ((fun x => Γ₀) x)ˣ
Hx : ↑v x = ↑γx
⊢ ∃ j, ↑(ltAddSubgroup v j) ⊆ (fun x_1 => x * x_1) ⁻¹' ↑(ltAddSubgroup v γ)
[PROOFSTEP]
use γx⁻¹ * γ
[GOAL]
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : Γ₀ˣ
γx : ((fun x => Γ₀) x)ˣ
Hx : ↑v x = ↑γx
⊢ ↑(ltAddSubgroup v (γx⁻¹ * γ)) ⊆ (fun x_1 => x * x_1) ⁻¹' ↑(ltAddSubgroup v γ)
[PROOFSTEP]
rintro y (vy_lt : v y < ↑(γx⁻¹ * γ))
[GOAL]
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : Γ₀ˣ
γx : ((fun x => Γ₀) x)ˣ
Hx : ↑v x = ↑γx
y : R
vy_lt : ↑v y < ↑(γx⁻¹ * γ)
⊢ y ∈ (fun x_1 => x * x_1) ⁻¹' ↑(ltAddSubgroup v γ)
[PROOFSTEP]
change (v (x * y) : Γ₀) < γ
[GOAL]
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : Γ₀ˣ
γx : ((fun x => Γ₀) x)ˣ
Hx : ↑v x = ↑γx
y : R
vy_lt : ↑v y < ↑(γx⁻¹ * γ)
⊢ ↑v (x * y) < ↑γ
[PROOFSTEP]
rw [Valuation.map_mul, Hx, mul_comm]
[GOAL]
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : Γ₀ˣ
γx : ((fun x => Γ₀) x)ˣ
Hx : ↑v x = ↑γx
y : R
vy_lt : ↑v y < ↑(γx⁻¹ * γ)
⊢ ↑v y * ↑γx < ↑γ
[PROOFSTEP]
rw [Units.val_mul, mul_comm] at vy_lt
[GOAL]
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : Γ₀ˣ
γx : ((fun x => Γ₀) x)ˣ
Hx : ↑v x = ↑γx
y : R
vy_lt : ↑v y < ↑γ * ↑γx⁻¹
⊢ ↑v y * ↑γx < ↑γ
[PROOFSTEP]
simpa using mul_inv_lt_of_lt_mul₀ vy_lt
[GOAL]
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
⊢ ∀ (x : R) (i : Γ₀ˣ), ∃ j, ↑(ltAddSubgroup v j) ⊆ (fun x_1 => x_1 * x) ⁻¹' ↑(ltAddSubgroup v i)
[PROOFSTEP]
rintro x γ
[GOAL]
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : Γ₀ˣ
⊢ ∃ j, ↑(ltAddSubgroup v j) ⊆ (fun x_1 => x_1 * x) ⁻¹' ↑(ltAddSubgroup v γ)
[PROOFSTEP]
rcases GroupWithZero.eq_zero_or_unit (v x) with (Hx | ⟨γx, Hx⟩)
[GOAL]
case inl
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : Γ₀ˣ
Hx : ↑v x = 0
⊢ ∃ j, ↑(ltAddSubgroup v j) ⊆ (fun x_1 => x_1 * x) ⁻¹' ↑(ltAddSubgroup v γ)
[PROOFSTEP]
use 1
[GOAL]
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : Γ₀ˣ
Hx : ↑v x = 0
⊢ ↑(ltAddSubgroup v 1) ⊆ (fun x_1 => x_1 * x) ⁻¹' ↑(ltAddSubgroup v γ)
[PROOFSTEP]
rintro y _
[GOAL]
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : Γ₀ˣ
Hx : ↑v x = 0
y : R
a✝ : y ∈ ↑(ltAddSubgroup v 1)
⊢ y ∈ (fun x_1 => x_1 * x) ⁻¹' ↑(ltAddSubgroup v γ)
[PROOFSTEP]
change v (y * x) < _
[GOAL]
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : Γ₀ˣ
Hx : ↑v x = 0
y : R
a✝ : y ∈ ↑(ltAddSubgroup v 1)
⊢ ↑v (y * x) < ↑γ
[PROOFSTEP]
rw [Valuation.map_mul, Hx, mul_zero]
[GOAL]
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : Γ₀ˣ
Hx : ↑v x = 0
y : R
a✝ : y ∈ ↑(ltAddSubgroup v 1)
⊢ 0 < ↑γ
[PROOFSTEP]
exact Units.zero_lt γ
[GOAL]
case inr.intro
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : Γ₀ˣ
γx : ((fun x => Γ₀) x)ˣ
Hx : ↑v x = ↑γx
⊢ ∃ j, ↑(ltAddSubgroup v j) ⊆ (fun x_1 => x_1 * x) ⁻¹' ↑(ltAddSubgroup v γ)
[PROOFSTEP]
use γx⁻¹ * γ
[GOAL]
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : Γ₀ˣ
γx : ((fun x => Γ₀) x)ˣ
Hx : ↑v x = ↑γx
⊢ ↑(ltAddSubgroup v (γx⁻¹ * γ)) ⊆ (fun x_1 => x_1 * x) ⁻¹' ↑(ltAddSubgroup v γ)
[PROOFSTEP]
rintro y (vy_lt : v y < ↑(γx⁻¹ * γ))
[GOAL]
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : Γ₀ˣ
γx : ((fun x => Γ₀) x)ˣ
Hx : ↑v x = ↑γx
y : R
vy_lt : ↑v y < ↑(γx⁻¹ * γ)
⊢ y ∈ (fun x_1 => x_1 * x) ⁻¹' ↑(ltAddSubgroup v γ)
[PROOFSTEP]
change (v (y * x) : Γ₀) < γ
[GOAL]
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : Γ₀ˣ
γx : ((fun x => Γ₀) x)ˣ
Hx : ↑v x = ↑γx
y : R
vy_lt : ↑v y < ↑(γx⁻¹ * γ)
⊢ ↑v (y * x) < ↑γ
[PROOFSTEP]
rw [Valuation.map_mul, Hx]
[GOAL]
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : Γ₀ˣ
γx : ((fun x => Γ₀) x)ˣ
Hx : ↑v x = ↑γx
y : R
vy_lt : ↑v y < ↑(γx⁻¹ * γ)
⊢ ↑v y * ↑γx < ↑γ
[PROOFSTEP]
rw [Units.val_mul, mul_comm] at vy_lt
[GOAL]
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : Γ₀ˣ
γx : ((fun x => Γ₀) x)ˣ
Hx : ↑v x = ↑γx
y : R
vy_lt : ↑v y < ↑γ * ↑γx⁻¹
⊢ ↑v y * ↑γx < ↑γ
[PROOFSTEP]
simpa using mul_inv_lt_of_lt_mul₀ vy_lt
[GOAL]
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
⊢ ∀ (s : Set R), s ∈ 𝓝 0 ↔ ∃ γ, {x | ↑v x < ↑γ} ⊆ s
[PROOFSTEP]
letI := @TopologicalAddGroup.toUniformSpace R _ v.subgroups_basis.topology _
[GOAL]
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
this : UniformSpace R := TopologicalAddGroup.toUniformSpace R
⊢ ∀ (s : Set R), s ∈ 𝓝 0 ↔ ∃ γ, {x | ↑v x < ↑γ} ⊆ s
[PROOFSTEP]
intro s
[GOAL]
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
this : UniformSpace R := TopologicalAddGroup.toUniformSpace R
s : Set R
⊢ s ∈ 𝓝 0 ↔ ∃ γ, {x | ↑v x < ↑γ} ⊆ s
[PROOFSTEP]
rw [Filter.hasBasis_iff.mp v.subgroups_basis.hasBasis_nhds_zero s]
[GOAL]
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
this : UniformSpace R := TopologicalAddGroup.toUniformSpace R
s : Set R
⊢ (∃ i, True ∧ ↑(ltAddSubgroup v i) ⊆ s) ↔ ∃ γ, {x | ↑v x < ↑γ} ⊆ s
[PROOFSTEP]
exact exists_congr fun γ => by rw [true_and]; rfl
[GOAL]
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
this : UniformSpace R := TopologicalAddGroup.toUniformSpace R
s : Set R
γ : Γ₀ˣ
⊢ True ∧ ↑(ltAddSubgroup v γ) ⊆ s ↔ {x | ↑v x < ↑γ} ⊆ s
[PROOFSTEP]
rw [true_and]
[GOAL]
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
this : UniformSpace R := TopologicalAddGroup.toUniformSpace R
s : Set R
γ : Γ₀ˣ
⊢ ↑(ltAddSubgroup v γ) ⊆ s ↔ {x | ↑v x < ↑γ} ⊆ s
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
⊢ Filter.HasBasis (𝓝 0) (fun x => True) fun γ => {x | ↑v x < ↑γ}
[PROOFSTEP]
simp [Filter.hasBasis_iff, is_topological_valuation]
[GOAL]
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
⊢ Filter.HasBasis (uniformity R) (fun x => True) fun γ => {p | ↑v (p.snd - p.fst) < ↑γ}
[PROOFSTEP]
rw [uniformity_eq_comap_nhds_zero]
[GOAL]
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
⊢ Filter.HasBasis (Filter.comap (fun x => x.snd - x.fst) (𝓝 0)) (fun x => True) fun γ => {p | ↑v (p.snd - p.fst) < ↑γ}
[PROOFSTEP]
exact (hasBasis_nhds_zero R Γ₀).comap _
[GOAL]
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
s : Set R
x : R
⊢ s ∈ 𝓝 x ↔ ∃ γ, {y | ↑v (y - x) < ↑γ} ⊆ s
[PROOFSTEP]
simp only [← nhds_translation_add_neg x, ← sub_eq_add_neg, preimage_setOf_eq, true_and,
  ((hasBasis_nhds_zero R Γ₀).comap fun y => y - x).mem_iff]
[GOAL]
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
s : Set R
⊢ s ∈ 𝓝 0 ↔ ∃ γ, {x | ↑v x < ↑γ} ⊆ s
[PROOFSTEP]
simp only [mem_nhds, sub_zero]
[GOAL]
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
x : R
h : ↑v x ≠ 0
⊢ {y | ↑v y = ↑v x} ∈ 𝓝 x
[PROOFSTEP]
rw [mem_nhds]
[GOAL]
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
x : R
h : ↑v x ≠ 0
⊢ ∃ γ, {y | ↑v (y - x) < ↑γ} ⊆ {y | ↑v y = ↑v x}
[PROOFSTEP]
rcases Units.exists_iff_ne_zero.mpr h with ⟨γ, hx⟩
[GOAL]
case intro
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
x : R
h : ↑v x ≠ 0
γ : ((fun x => Γ₀) x)ˣ
hx : ↑γ = ↑v x
⊢ ∃ γ, {y | ↑v (y - x) < ↑γ} ⊆ {y | ↑v y = ↑v x}
[PROOFSTEP]
use γ
[GOAL]
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
x : R
h : ↑v x ≠ 0
γ : ((fun x => Γ₀) x)ˣ
hx : ↑γ = ↑v x
⊢ {y | ↑v (y - x) < ↑γ} ⊆ {y | ↑v y = ↑v x}
[PROOFSTEP]
rw [hx]
[GOAL]
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
x : R
h : ↑v x ≠ 0
γ : ((fun x => Γ₀) x)ˣ
hx : ↑γ = ↑v x
⊢ {y | ↑v (y - x) < ↑v x} ⊆ {y | ↑v y = ↑v x}
[PROOFSTEP]
intro y y_in
[GOAL]
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
x : R
h : ↑v x ≠ 0
γ : ((fun x => Γ₀) x)ˣ
hx : ↑γ = ↑v x
y : R
y_in : y ∈ {y | ↑v (y - x) < ↑v x}
⊢ y ∈ {y | ↑v y = ↑v x}
[PROOFSTEP]
exact Valuation.map_eq_of_sub_lt _ y_in
[GOAL]
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
F : Filter R
⊢ Cauchy F ↔ Filter.NeBot F ∧ ∀ (γ : Γ₀ˣ), ∃ M, M ∈ F ∧ ∀ (x : R), x ∈ M → ∀ (y : R), y ∈ M → ↑v (y - x) < ↑γ
[PROOFSTEP]
rw [toUniformSpace_eq, AddGroupFilterBasis.cauchy_iff]
[GOAL]
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
F : Filter R
⊢ (Filter.NeBot F ∧
      ∀ (U : Set R),
        U ∈ RingFilterBasis.toAddGroupFilterBasis → ∃ M, M ∈ F ∧ ∀ (x : R), x ∈ M → ∀ (y : R), y ∈ M → y - x ∈ U) ↔
    Filter.NeBot F ∧ ∀ (γ : Γ₀ˣ), ∃ M, M ∈ F ∧ ∀ (x : R), x ∈ M → ∀ (y : R), y ∈ M → ↑v (y - x) < ↑γ
[PROOFSTEP]
apply and_congr Iff.rfl
[GOAL]
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
F : Filter R
⊢ (∀ (U : Set R),
      U ∈ RingFilterBasis.toAddGroupFilterBasis → ∃ M, M ∈ F ∧ ∀ (x : R), x ∈ M → ∀ (y : R), y ∈ M → y - x ∈ U) ↔
    ∀ (γ : Γ₀ˣ), ∃ M, M ∈ F ∧ ∀ (x : R), x ∈ M → ∀ (y : R), y ∈ M → ↑v (y - x) < ↑γ
[PROOFSTEP]
simp_rw [Valued.v.subgroups_basis.mem_addGroupFilterBasis_iff]
[GOAL]
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
F : Filter R
⊢ (∀ (U : Set R), (∃ i, U = ↑(ltAddSubgroup v i)) → ∃ M, M ∈ F ∧ ∀ (x : R), x ∈ M → ∀ (y : R), y ∈ M → y - x ∈ U) ↔
    ∀ (γ : Γ₀ˣ), ∃ M, M ∈ F ∧ ∀ (x : R), x ∈ M → ∀ (y : R), y ∈ M → ↑v (y - x) < ↑γ
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
F : Filter R
⊢ (∀ (U : Set R), (∃ i, U = ↑(ltAddSubgroup v i)) → ∃ M, M ∈ F ∧ ∀ (x : R), x ∈ M → ∀ (y : R), y ∈ M → y - x ∈ U) →
    ∀ (γ : Γ₀ˣ), ∃ M, M ∈ F ∧ ∀ (x : R), x ∈ M → ∀ (y : R), y ∈ M → ↑v (y - x) < ↑γ
[PROOFSTEP]
intro h γ
[GOAL]
case mp
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
F : Filter R
h : ∀ (U : Set R), (∃ i, U = ↑(ltAddSubgroup v i)) → ∃ M, M ∈ F ∧ ∀ (x : R), x ∈ M → ∀ (y : R), y ∈ M → y - x ∈ U
γ : Γ₀ˣ
⊢ ∃ M, M ∈ F ∧ ∀ (x : R), x ∈ M → ∀ (y : R), y ∈ M → ↑v (y - x) < ↑γ
[PROOFSTEP]
exact h _ (Valued.v.subgroups_basis.mem_addGroupFilterBasis _)
[GOAL]
case mpr
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
F : Filter R
⊢ (∀ (γ : Γ₀ˣ), ∃ M, M ∈ F ∧ ∀ (x : R), x ∈ M → ∀ (y : R), y ∈ M → ↑v (y - x) < ↑γ) →
    ∀ (U : Set R), (∃ i, U = ↑(ltAddSubgroup v i)) → ∃ M, M ∈ F ∧ ∀ (x : R), x ∈ M → ∀ (y : R), y ∈ M → y - x ∈ U
[PROOFSTEP]
rintro h - ⟨γ, rfl⟩
[GOAL]
case mpr.intro
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
F : Filter R
h : ∀ (γ : Γ₀ˣ), ∃ M, M ∈ F ∧ ∀ (x : R), x ∈ M → ∀ (y : R), y ∈ M → ↑v (y - x) < ↑γ
γ : Γ₀ˣ
⊢ ∃ M, M ∈ F ∧ ∀ (x : R), x ∈ M → ∀ (y : R), y ∈ M → y - x ∈ ↑(ltAddSubgroup v γ)
[PROOFSTEP]
exact h γ


[GOAL]
R : Type u
M : Type v
N : Type w
inst✝⁹ : Ring R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : ContinuousSMul R M
inst✝² : Module R N
inst✝¹ : ContinuousAdd M
inst✝ : IsSimpleModule R N
l : M →ₗ[R] N
⊢ IsClosed ↑(ker l) ∨ Dense ↑(ker l)
[PROOFSTEP]
rcases l.surjective_or_eq_zero with (hl | rfl)
[GOAL]
case inl
R : Type u
M : Type v
N : Type w
inst✝⁹ : Ring R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : ContinuousSMul R M
inst✝² : Module R N
inst✝¹ : ContinuousAdd M
inst✝ : IsSimpleModule R N
l : M →ₗ[R] N
hl : Function.Surjective ↑l
⊢ IsClosed ↑(ker l) ∨ Dense ↑(ker l)
[PROOFSTEP]
exact l.ker.isClosed_or_dense_of_isCoatom (LinearMap.isCoatom_ker_of_surjective hl)
[GOAL]
case inr
R : Type u
M : Type v
N : Type w
inst✝⁹ : Ring R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : ContinuousSMul R M
inst✝² : Module R N
inst✝¹ : ContinuousAdd M
inst✝ : IsSimpleModule R N
⊢ IsClosed ↑(ker 0) ∨ Dense ↑(ker 0)
[PROOFSTEP]
rw [LinearMap.ker_zero]
[GOAL]
case inr
R : Type u
M : Type v
N : Type w
inst✝⁹ : Ring R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : ContinuousSMul R M
inst✝² : Module R N
inst✝¹ : ContinuousAdd M
inst✝ : IsSimpleModule R N
⊢ IsClosed ↑⊤ ∨ Dense ↑⊤
[PROOFSTEP]
left
[GOAL]
case inr.h
R : Type u
M : Type v
N : Type w
inst✝⁹ : Ring R
inst✝⁸ : TopologicalSpace R
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : ContinuousSMul R M
inst✝² : Module R N
inst✝¹ : ContinuousAdd M
inst✝ : IsSimpleModule R N
⊢ IsClosed ↑⊤
[PROOFSTEP]
exact isClosed_univ


[GOAL]
A✝ : Type u_1
ι✝ : Type u_2
inst✝¹ : Ring A✝
A : Type u_3
ι : Type u_4
inst✝ : CommRing A
B : ι → AddSubgroup A
inter : ∀ (i j : ι), ∃ k, B k ≤ B i ⊓ B j
mul : ∀ (i : ι), ∃ j, ↑(B j) * ↑(B j) ⊆ ↑(B i)
leftMul : ∀ (x : A) (i : ι), ∃ j, ↑(B j) ⊆ (fun y => x * y) ⁻¹' ↑(B i)
⊢ ∀ (x : A) (i : ι), ∃ j, ↑(B j) ⊆ (fun x_1 => x_1 * x) ⁻¹' ↑(B i)
[PROOFSTEP]
intro x i
[GOAL]
A✝ : Type u_1
ι✝ : Type u_2
inst✝¹ : Ring A✝
A : Type u_3
ι : Type u_4
inst✝ : CommRing A
B : ι → AddSubgroup A
inter : ∀ (i j : ι), ∃ k, B k ≤ B i ⊓ B j
mul : ∀ (i : ι), ∃ j, ↑(B j) * ↑(B j) ⊆ ↑(B i)
leftMul : ∀ (x : A) (i : ι), ∃ j, ↑(B j) ⊆ (fun y => x * y) ⁻¹' ↑(B i)
x : A
i : ι
⊢ ∃ j, ↑(B j) ⊆ (fun x_1 => x_1 * x) ⁻¹' ↑(B i)
[PROOFSTEP]
cases' leftMul x i with j hj
[GOAL]
case intro
A✝ : Type u_1
ι✝ : Type u_2
inst✝¹ : Ring A✝
A : Type u_3
ι : Type u_4
inst✝ : CommRing A
B : ι → AddSubgroup A
inter : ∀ (i j : ι), ∃ k, B k ≤ B i ⊓ B j
mul : ∀ (i : ι), ∃ j, ↑(B j) * ↑(B j) ⊆ ↑(B i)
leftMul : ∀ (x : A) (i : ι), ∃ j, ↑(B j) ⊆ (fun y => x * y) ⁻¹' ↑(B i)
x : A
i j : ι
hj : ↑(B j) ⊆ (fun y => x * y) ⁻¹' ↑(B i)
⊢ ∃ j, ↑(B j) ⊆ (fun x_1 => x_1 * x) ⁻¹' ↑(B i)
[PROOFSTEP]
use j
[GOAL]
case h
A✝ : Type u_1
ι✝ : Type u_2
inst✝¹ : Ring A✝
A : Type u_3
ι : Type u_4
inst✝ : CommRing A
B : ι → AddSubgroup A
inter : ∀ (i j : ι), ∃ k, B k ≤ B i ⊓ B j
mul : ∀ (i : ι), ∃ j, ↑(B j) * ↑(B j) ⊆ ↑(B i)
leftMul : ∀ (x : A) (i : ι), ∃ j, ↑(B j) ⊆ (fun y => x * y) ⁻¹' ↑(B i)
x : A
i j : ι
hj : ↑(B j) ⊆ (fun y => x * y) ⁻¹' ↑(B i)
⊢ ↑(B j) ⊆ (fun x_1 => x_1 * x) ⁻¹' ↑(B i)
[PROOFSTEP]
simpa [mul_comm] using hj
[GOAL]
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
⊢ Set.Nonempty {U | ∃ i, U = ↑(B i)}
[PROOFSTEP]
inhabit ι
[GOAL]
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
inhabited_h : Inhabited ι
⊢ Set.Nonempty {U | ∃ i, U = ↑(B i)}
[PROOFSTEP]
exact ⟨B default, default, rfl⟩
[GOAL]
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
⊢ ∀ {x y : Set A}, x ∈ {U | ∃ i, U = ↑(B i)} → y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y
[PROOFSTEP]
rintro _ _ ⟨i, rfl⟩ ⟨j, rfl⟩
[GOAL]
case intro.intro
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i j : ι
⊢ ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ ↑(B i) ∩ ↑(B j)
[PROOFSTEP]
cases' hB.inter i j with k hk
[GOAL]
case intro.intro.intro
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i j k : ι
hk : B k ≤ B i ⊓ B j
⊢ ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ ↑(B i) ∩ ↑(B j)
[PROOFSTEP]
use B k
[GOAL]
case h
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i j k : ι
hk : B k ≤ B i ⊓ B j
⊢ ↑(B k) ∈ {U | ∃ i, U = ↑(B i)} ∧ ↑(B k) ⊆ ↑(B i) ∩ ↑(B j)
[PROOFSTEP]
constructor
[GOAL]
case h.left
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i j k : ι
hk : B k ≤ B i ⊓ B j
⊢ ↑(B k) ∈ {U | ∃ i, U = ↑(B i)}
[PROOFSTEP]
use k
[GOAL]
case h.right
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i j k : ι
hk : B k ≤ B i ⊓ B j
⊢ ↑(B k) ⊆ ↑(B i) ∩ ↑(B j)
[PROOFSTEP]
exact hk
[GOAL]
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
⊢ ∀ {U : Set A},
    U ∈
        { sets := {U | ∃ i, U = ↑(B i)}, nonempty := (_ : ∃ x, x ∈ {U | ∃ i, U = ↑(B i)}),
            inter_sets :=
              (_ :
                ∀ {x y : Set A},
                  x ∈ {U | ∃ i, U = ↑(B i)} →
                    y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y) }.sets →
      0 ∈ U
[PROOFSTEP]
rintro _ ⟨i, rfl⟩
[GOAL]
case intro
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i : ι
⊢ 0 ∈ ↑(B i)
[PROOFSTEP]
exact (B i).zero_mem
[GOAL]
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
⊢ ∀ {U : Set A},
    U ∈
        { sets := {U | ∃ i, U = ↑(B i)}, nonempty := (_ : ∃ x, x ∈ {U | ∃ i, U = ↑(B i)}),
            inter_sets :=
              (_ :
                ∀ {x y : Set A},
                  x ∈ {U | ∃ i, U = ↑(B i)} →
                    y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y) }.sets →
      ∃ V,
        V ∈
            { sets := {U | ∃ i, U = ↑(B i)}, nonempty := (_ : ∃ x, x ∈ {U | ∃ i, U = ↑(B i)}),
                inter_sets :=
                  (_ :
                    ∀ {x y : Set A},
                      x ∈ {U | ∃ i, U = ↑(B i)} →
                        y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y) }.sets ∧
          V + V ⊆ U
[PROOFSTEP]
rintro _ ⟨i, rfl⟩
[GOAL]
case intro
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i : ι
⊢ ∃ V,
    V ∈
        { sets := {U | ∃ i, U = ↑(B i)}, nonempty := (_ : ∃ x, x ∈ {U | ∃ i, U = ↑(B i)}),
            inter_sets :=
              (_ :
                ∀ {x y : Set A},
                  x ∈ {U | ∃ i, U = ↑(B i)} →
                    y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y) }.sets ∧
      V + V ⊆ ↑(B i)
[PROOFSTEP]
use B i
[GOAL]
case h
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i : ι
⊢ ↑(B i) ∈
      { sets := {U | ∃ i, U = ↑(B i)}, nonempty := (_ : ∃ x, x ∈ {U | ∃ i, U = ↑(B i)}),
          inter_sets :=
            (_ :
              ∀ {x y : Set A},
                x ∈ {U | ∃ i, U = ↑(B i)} →
                  y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y) }.sets ∧
    ↑(B i) + ↑(B i) ⊆ ↑(B i)
[PROOFSTEP]
constructor
[GOAL]
case h.left
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i : ι
⊢ ↑(B i) ∈
    { sets := {U | ∃ i, U = ↑(B i)}, nonempty := (_ : ∃ x, x ∈ {U | ∃ i, U = ↑(B i)}),
        inter_sets :=
          (_ :
            ∀ {x y : Set A},
              x ∈ {U | ∃ i, U = ↑(B i)} → y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y) }.sets
[PROOFSTEP]
use i
[GOAL]
case h.right
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i : ι
⊢ ↑(B i) + ↑(B i) ⊆ ↑(B i)
[PROOFSTEP]
rintro x ⟨y, z, y_in, z_in, rfl⟩
[GOAL]
case h.right.intro.intro.intro.intro
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i : ι
y z : A
y_in : y ∈ ↑(B i)
z_in : z ∈ ↑(B i)
⊢ (fun x x_1 => x + x_1) y z ∈ ↑(B i)
[PROOFSTEP]
exact (B i).add_mem y_in z_in
[GOAL]
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
⊢ ∀ {U : Set A},
    U ∈
        { sets := {U | ∃ i, U = ↑(B i)}, nonempty := (_ : ∃ x, x ∈ {U | ∃ i, U = ↑(B i)}),
            inter_sets :=
              (_ :
                ∀ {x y : Set A},
                  x ∈ {U | ∃ i, U = ↑(B i)} →
                    y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y) }.sets →
      ∃ V,
        V ∈
            { sets := {U | ∃ i, U = ↑(B i)}, nonempty := (_ : ∃ x, x ∈ {U | ∃ i, U = ↑(B i)}),
                inter_sets :=
                  (_ :
                    ∀ {x y : Set A},
                      x ∈ {U | ∃ i, U = ↑(B i)} →
                        y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y) }.sets ∧
          V ⊆ (fun x => -x) ⁻¹' U
[PROOFSTEP]
rintro _ ⟨i, rfl⟩
[GOAL]
case intro
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i : ι
⊢ ∃ V,
    V ∈
        { sets := {U | ∃ i, U = ↑(B i)}, nonempty := (_ : ∃ x, x ∈ {U | ∃ i, U = ↑(B i)}),
            inter_sets :=
              (_ :
                ∀ {x y : Set A},
                  x ∈ {U | ∃ i, U = ↑(B i)} →
                    y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y) }.sets ∧
      V ⊆ (fun x => -x) ⁻¹' ↑(B i)
[PROOFSTEP]
use B i
[GOAL]
case h
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i : ι
⊢ ↑(B i) ∈
      { sets := {U | ∃ i, U = ↑(B i)}, nonempty := (_ : ∃ x, x ∈ {U | ∃ i, U = ↑(B i)}),
          inter_sets :=
            (_ :
              ∀ {x y : Set A},
                x ∈ {U | ∃ i, U = ↑(B i)} →
                  y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y) }.sets ∧
    ↑(B i) ⊆ (fun x => -x) ⁻¹' ↑(B i)
[PROOFSTEP]
constructor
[GOAL]
case h.left
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i : ι
⊢ ↑(B i) ∈
    { sets := {U | ∃ i, U = ↑(B i)}, nonempty := (_ : ∃ x, x ∈ {U | ∃ i, U = ↑(B i)}),
        inter_sets :=
          (_ :
            ∀ {x y : Set A},
              x ∈ {U | ∃ i, U = ↑(B i)} → y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y) }.sets
[PROOFSTEP]
use i
[GOAL]
case h.right
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i : ι
⊢ ↑(B i) ⊆ (fun x => -x) ⁻¹' ↑(B i)
[PROOFSTEP]
intro x x_in
[GOAL]
case h.right
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i : ι
x : A
x_in : x ∈ ↑(B i)
⊢ x ∈ (fun x => -x) ⁻¹' ↑(B i)
[PROOFSTEP]
exact (B i).neg_mem x_in
[GOAL]
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
⊢ ∀ (x₀ : A) {U : Set A},
    U ∈
        { sets := {U | ∃ i, U = ↑(B i)}, nonempty := (_ : ∃ x, x ∈ {U | ∃ i, U = ↑(B i)}),
            inter_sets :=
              (_ :
                ∀ {x y : Set A},
                  x ∈ {U | ∃ i, U = ↑(B i)} →
                    y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y) }.sets →
      ∃ V,
        V ∈
            { sets := {U | ∃ i, U = ↑(B i)}, nonempty := (_ : ∃ x, x ∈ {U | ∃ i, U = ↑(B i)}),
                inter_sets :=
                  (_ :
                    ∀ {x y : Set A},
                      x ∈ {U | ∃ i, U = ↑(B i)} →
                        y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y) }.sets ∧
          V ⊆ (fun x => x₀ + x + -x₀) ⁻¹' U
[PROOFSTEP]
rintro x₀ _ ⟨i, rfl⟩
[GOAL]
case intro
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
x₀ : A
i : ι
⊢ ∃ V,
    V ∈
        { sets := {U | ∃ i, U = ↑(B i)}, nonempty := (_ : ∃ x, x ∈ {U | ∃ i, U = ↑(B i)}),
            inter_sets :=
              (_ :
                ∀ {x y : Set A},
                  x ∈ {U | ∃ i, U = ↑(B i)} →
                    y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y) }.sets ∧
      V ⊆ (fun x => x₀ + x + -x₀) ⁻¹' ↑(B i)
[PROOFSTEP]
use B i
[GOAL]
case h
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
x₀ : A
i : ι
⊢ ↑(B i) ∈
      { sets := {U | ∃ i, U = ↑(B i)}, nonempty := (_ : ∃ x, x ∈ {U | ∃ i, U = ↑(B i)}),
          inter_sets :=
            (_ :
              ∀ {x y : Set A},
                x ∈ {U | ∃ i, U = ↑(B i)} →
                  y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y) }.sets ∧
    ↑(B i) ⊆ (fun x => x₀ + x + -x₀) ⁻¹' ↑(B i)
[PROOFSTEP]
constructor
[GOAL]
case h.left
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
x₀ : A
i : ι
⊢ ↑(B i) ∈
    { sets := {U | ∃ i, U = ↑(B i)}, nonempty := (_ : ∃ x, x ∈ {U | ∃ i, U = ↑(B i)}),
        inter_sets :=
          (_ :
            ∀ {x y : Set A},
              x ∈ {U | ∃ i, U = ↑(B i)} → y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y) }.sets
[PROOFSTEP]
use i
[GOAL]
case h.right
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
x₀ : A
i : ι
⊢ ↑(B i) ⊆ (fun x => x₀ + x + -x₀) ⁻¹' ↑(B i)
[PROOFSTEP]
simp
[GOAL]
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
⊢ ∀ {U : Set A},
    U ∈ AddGroupFilterBasis.toFilterBasis.sets → ∃ V, V ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ V * V ⊆ U
[PROOFSTEP]
rintro _ ⟨i, rfl⟩
[GOAL]
case intro
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i : ι
⊢ ∃ V, V ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ V * V ⊆ ↑(B i)
[PROOFSTEP]
cases' hB.mul i with k hk
[GOAL]
case intro.intro
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i k : ι
hk : ↑(B k) * ↑(B k) ⊆ ↑(B i)
⊢ ∃ V, V ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ V * V ⊆ ↑(B i)
[PROOFSTEP]
use B k
[GOAL]
case h
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i k : ι
hk : ↑(B k) * ↑(B k) ⊆ ↑(B i)
⊢ ↑(B k) ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ ↑(B k) * ↑(B k) ⊆ ↑(B i)
[PROOFSTEP]
constructor
[GOAL]
case h.left
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i k : ι
hk : ↑(B k) * ↑(B k) ⊆ ↑(B i)
⊢ ↑(B k) ∈ AddGroupFilterBasis.toFilterBasis.sets
[PROOFSTEP]
use k
[GOAL]
case h.right
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i k : ι
hk : ↑(B k) * ↑(B k) ⊆ ↑(B i)
⊢ ↑(B k) * ↑(B k) ⊆ ↑(B i)
[PROOFSTEP]
exact hk
[GOAL]
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
⊢ ∀ (x₀ : A) {U : Set A},
    U ∈ AddGroupFilterBasis.toFilterBasis.sets →
      ∃ V, V ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ V ⊆ (fun x => x₀ * x) ⁻¹' U
[PROOFSTEP]
rintro x₀ _ ⟨i, rfl⟩
[GOAL]
case intro
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
x₀ : A
i : ι
⊢ ∃ V, V ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ V ⊆ (fun x => x₀ * x) ⁻¹' ↑(B i)
[PROOFSTEP]
cases' hB.leftMul x₀ i with k hk
[GOAL]
case intro.intro
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
x₀ : A
i k : ι
hk : ↑(B k) ⊆ (fun x => x₀ * x) ⁻¹' ↑(B i)
⊢ ∃ V, V ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ V ⊆ (fun x => x₀ * x) ⁻¹' ↑(B i)
[PROOFSTEP]
use B k
[GOAL]
case h
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
x₀ : A
i k : ι
hk : ↑(B k) ⊆ (fun x => x₀ * x) ⁻¹' ↑(B i)
⊢ ↑(B k) ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ ↑(B k) ⊆ (fun x => x₀ * x) ⁻¹' ↑(B i)
[PROOFSTEP]
constructor
[GOAL]
case h.left
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
x₀ : A
i k : ι
hk : ↑(B k) ⊆ (fun x => x₀ * x) ⁻¹' ↑(B i)
⊢ ↑(B k) ∈ AddGroupFilterBasis.toFilterBasis.sets
[PROOFSTEP]
use k
[GOAL]
case h.right
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
x₀ : A
i k : ι
hk : ↑(B k) ⊆ (fun x => x₀ * x) ⁻¹' ↑(B i)
⊢ ↑(B k) ⊆ (fun x => x₀ * x) ⁻¹' ↑(B i)
[PROOFSTEP]
exact hk
[GOAL]
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
⊢ ∀ (x₀ : A) {U : Set A},
    U ∈ AddGroupFilterBasis.toFilterBasis.sets →
      ∃ V, V ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ V ⊆ (fun x => x * x₀) ⁻¹' U
[PROOFSTEP]
rintro x₀ _ ⟨i, rfl⟩
[GOAL]
case intro
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
x₀ : A
i : ι
⊢ ∃ V, V ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ V ⊆ (fun x => x * x₀) ⁻¹' ↑(B i)
[PROOFSTEP]
cases' hB.rightMul x₀ i with k hk
[GOAL]
case intro.intro
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
x₀ : A
i k : ι
hk : ↑(B k) ⊆ (fun x => x * x₀) ⁻¹' ↑(B i)
⊢ ∃ V, V ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ V ⊆ (fun x => x * x₀) ⁻¹' ↑(B i)
[PROOFSTEP]
use B k
[GOAL]
case h
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
x₀ : A
i k : ι
hk : ↑(B k) ⊆ (fun x => x * x₀) ⁻¹' ↑(B i)
⊢ ↑(B k) ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ ↑(B k) ⊆ (fun x => x * x₀) ⁻¹' ↑(B i)
[PROOFSTEP]
constructor
[GOAL]
case h.left
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
x₀ : A
i k : ι
hk : ↑(B k) ⊆ (fun x => x * x₀) ⁻¹' ↑(B i)
⊢ ↑(B k) ∈ AddGroupFilterBasis.toFilterBasis.sets
[PROOFSTEP]
use k
[GOAL]
case h.right
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
x₀ : A
i k : ι
hk : ↑(B k) ⊆ (fun x => x * x₀) ⁻¹' ↑(B i)
⊢ ↑(B k) ⊆ (fun x => x * x₀) ⁻¹' ↑(B i)
[PROOFSTEP]
exact hk
[GOAL]
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
⊢ ∀ (t : Set A), t ∈ 𝓝 0 ↔ ∃ i, True ∧ ↑(B i) ⊆ t
[PROOFSTEP]
intro s
[GOAL]
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
s : Set A
⊢ s ∈ 𝓝 0 ↔ ∃ i, True ∧ ↑(B i) ⊆ s
[PROOFSTEP]
rw [hB.toRingFilterBasis.toAddGroupFilterBasis.nhds_zero_hasBasis.mem_iff]
[GOAL]
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
s : Set A
⊢ (∃ i, i ∈ RingFilterBasis.toAddGroupFilterBasis ∧ id i ⊆ s) ↔ ∃ i, True ∧ ↑(B i) ⊆ s
[PROOFSTEP]
constructor
[GOAL]
case mp
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
s : Set A
⊢ (∃ i, i ∈ RingFilterBasis.toAddGroupFilterBasis ∧ id i ⊆ s) → ∃ i, True ∧ ↑(B i) ⊆ s
[PROOFSTEP]
rintro ⟨-, ⟨i, rfl⟩, hi⟩
[GOAL]
case mp.intro.intro.intro
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
s : Set A
i : ι
hi : id ↑(B i) ⊆ s
⊢ ∃ i, True ∧ ↑(B i) ⊆ s
[PROOFSTEP]
exact ⟨i, trivial, hi⟩
[GOAL]
case mpr
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
s : Set A
⊢ (∃ i, True ∧ ↑(B i) ⊆ s) → ∃ i, i ∈ RingFilterBasis.toAddGroupFilterBasis ∧ id i ⊆ s
[PROOFSTEP]
rintro ⟨i, -, hi⟩
[GOAL]
case mpr.intro.intro
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
s : Set A
i : ι
hi : ↑(B i) ⊆ s
⊢ ∃ i, i ∈ RingFilterBasis.toAddGroupFilterBasis ∧ id i ⊆ s
[PROOFSTEP]
exact ⟨B i, ⟨i, rfl⟩, hi⟩
[GOAL]
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
⊢ ∀ (t : Set A), t ∈ 𝓝 a ↔ ∃ i, True ∧ {b | b - a ∈ B i} ⊆ t
[PROOFSTEP]
intro s
[GOAL]
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
⊢ s ∈ 𝓝 a ↔ ∃ i, True ∧ {b | b - a ∈ B i} ⊆ s
[PROOFSTEP]
rw [(hB.toRingFilterBasis.toAddGroupFilterBasis.nhds_hasBasis a).mem_iff]
[GOAL]
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
⊢ (∃ i, i ∈ RingFilterBasis.toAddGroupFilterBasis ∧ (fun y => a + y) '' i ⊆ s) ↔ ∃ i, True ∧ {b | b - a ∈ B i} ⊆ s
[PROOFSTEP]
simp only [true_and]
[GOAL]
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
⊢ (∃ i, i ∈ RingFilterBasis.toAddGroupFilterBasis ∧ (fun y => a + y) '' i ⊆ s) ↔ ∃ i, {b | b - a ∈ B i} ⊆ s
[PROOFSTEP]
constructor
[GOAL]
case mp
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
⊢ (∃ i, i ∈ RingFilterBasis.toAddGroupFilterBasis ∧ (fun y => a + y) '' i ⊆ s) → ∃ i, {b | b - a ∈ B i} ⊆ s
[PROOFSTEP]
rintro ⟨-, ⟨i, rfl⟩, hi⟩
[GOAL]
case mp.intro.intro.intro
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
i : ι
hi : (fun y => a + y) '' ↑(B i) ⊆ s
⊢ ∃ i, {b | b - a ∈ B i} ⊆ s
[PROOFSTEP]
use i
[GOAL]
case h
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
i : ι
hi : (fun y => a + y) '' ↑(B i) ⊆ s
⊢ {b | b - a ∈ B i} ⊆ s
[PROOFSTEP]
suffices h : {b : A | b - a ∈ B i} = (fun y => a + y) '' ↑(B i)
[GOAL]
case h
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
i : ι
hi : (fun y => a + y) '' ↑(B i) ⊆ s
h : {b | b - a ∈ B i} = (fun y => a + y) '' ↑(B i)
⊢ {b | b - a ∈ B i} ⊆ s
[PROOFSTEP]
rw [h]
[GOAL]
case h
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
i : ι
hi : (fun y => a + y) '' ↑(B i) ⊆ s
h : {b | b - a ∈ B i} = (fun y => a + y) '' ↑(B i)
⊢ (fun y => a + y) '' ↑(B i) ⊆ s
[PROOFSTEP]
assumption
[GOAL]
case h
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
i : ι
hi : (fun y => a + y) '' ↑(B i) ⊆ s
⊢ {b | b - a ∈ B i} = (fun y => a + y) '' ↑(B i)
[PROOFSTEP]
simp only [image_add_left, neg_add_eq_sub]
[GOAL]
case h
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
i : ι
hi : (fun y => a + y) '' ↑(B i) ⊆ s
⊢ {b | b - a ∈ B i} = (fun x => x - a) ⁻¹' ↑(B i)
[PROOFSTEP]
ext b
[GOAL]
case h.h
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
i : ι
hi : (fun y => a + y) '' ↑(B i) ⊆ s
b : A
⊢ b ∈ {b | b - a ∈ B i} ↔ b ∈ (fun x => x - a) ⁻¹' ↑(B i)
[PROOFSTEP]
simp
[GOAL]
case mpr
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
⊢ (∃ i, {b | b - a ∈ B i} ⊆ s) → ∃ i, i ∈ RingFilterBasis.toAddGroupFilterBasis ∧ (fun y => a + y) '' i ⊆ s
[PROOFSTEP]
rintro ⟨i, hi⟩
[GOAL]
case mpr.intro
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
i : ι
hi : {b | b - a ∈ B i} ⊆ s
⊢ ∃ i, i ∈ RingFilterBasis.toAddGroupFilterBasis ∧ (fun y => a + y) '' i ⊆ s
[PROOFSTEP]
use B i
[GOAL]
case h
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
i : ι
hi : {b | b - a ∈ B i} ⊆ s
⊢ ↑(B i) ∈ RingFilterBasis.toAddGroupFilterBasis ∧ (fun y => a + y) '' ↑(B i) ⊆ s
[PROOFSTEP]
constructor
[GOAL]
case h.left
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
i : ι
hi : {b | b - a ∈ B i} ⊆ s
⊢ ↑(B i) ∈ RingFilterBasis.toAddGroupFilterBasis
[PROOFSTEP]
use i
[GOAL]
case h.right
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
i : ι
hi : {b | b - a ∈ B i} ⊆ s
⊢ (fun y => a + y) '' ↑(B i) ⊆ s
[PROOFSTEP]
rw [image_subset_iff]
[GOAL]
case h.right
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
i : ι
hi : {b | b - a ∈ B i} ⊆ s
⊢ ↑(B i) ⊆ (fun y => a + y) ⁻¹' s
[PROOFSTEP]
rintro b b_in
[GOAL]
case h.right
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
i : ι
hi : {b | b - a ∈ B i} ⊆ s
b : A
b_in : b ∈ ↑(B i)
⊢ b ∈ (fun y => a + y) ⁻¹' s
[PROOFSTEP]
apply hi
[GOAL]
case h.right.a
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
a : A
s : Set A
i : ι
hi : {b | b - a ∈ B i} ⊆ s
b : A
b_in : b ∈ ↑(B i)
⊢ (fun y => a + y) b ∈ {b | b - a ∈ B i}
[PROOFSTEP]
simpa using b_in
[GOAL]
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i : ι
x✝ : TopologicalSpace A := topology hB
src✝ : AddSubgroup A := B i
⊢ IsOpen
    { toAddSubmonoid := src✝.toAddSubmonoid,
            neg_mem' := (_ : ∀ {x : A}, x ∈ src✝.carrier → -x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
rw [isOpen_iff_mem_nhds]
[GOAL]
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i : ι
x✝ : TopologicalSpace A := topology hB
src✝ : AddSubgroup A := B i
⊢ ∀ (a : A),
    a ∈
        { toAddSubmonoid := src✝.toAddSubmonoid,
                neg_mem' :=
                  (_ : ∀ {x : A}, x ∈ src✝.carrier → -x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier →
      { toAddSubmonoid := src✝.toAddSubmonoid,
                neg_mem' :=
                  (_ : ∀ {x : A}, x ∈ src✝.carrier → -x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier ∈
        𝓝 a
[PROOFSTEP]
intro a a_in
[GOAL]
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i : ι
x✝ : TopologicalSpace A := topology hB
src✝ : AddSubgroup A := B i
a : A
a_in :
  a ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            neg_mem' := (_ : ∀ {x : A}, x ∈ src✝.carrier → -x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
⊢ { toAddSubmonoid := src✝.toAddSubmonoid,
            neg_mem' :=
              (_ : ∀ {x : A}, x ∈ src✝.carrier → -x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier ∈
    𝓝 a
[PROOFSTEP]
rw [(hB.hasBasis_nhds a).mem_iff]
[GOAL]
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i : ι
x✝ : TopologicalSpace A := topology hB
src✝ : AddSubgroup A := B i
a : A
a_in :
  a ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            neg_mem' := (_ : ∀ {x : A}, x ∈ src✝.carrier → -x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
⊢ ∃ i,
    True ∧
      {b | b - a ∈ B i} ⊆
        { toAddSubmonoid := src✝.toAddSubmonoid,
                neg_mem' :=
                  (_ : ∀ {x : A}, x ∈ src✝.carrier → -x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
use i, trivial
[GOAL]
case right
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i : ι
x✝ : TopologicalSpace A := topology hB
src✝ : AddSubgroup A := B i
a : A
a_in :
  a ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            neg_mem' := (_ : ∀ {x : A}, x ∈ src✝.carrier → -x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
⊢ {b | b - a ∈ B i} ⊆
    { toAddSubmonoid := src✝.toAddSubmonoid,
            neg_mem' := (_ : ∀ {x : A}, x ∈ src✝.carrier → -x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
rintro b b_in
[GOAL]
case right
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
i : ι
x✝ : TopologicalSpace A := topology hB
src✝ : AddSubgroup A := B i
a : A
a_in :
  a ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            neg_mem' := (_ : ∀ {x : A}, x ∈ src✝.carrier → -x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
b : A
b_in : b ∈ {b | b - a ∈ B i}
⊢ b ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            neg_mem' := (_ : ∀ {x : A}, x ∈ src✝.carrier → -x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
simpa using (B i).add_mem a_in b_in
[GOAL]
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
⊢ NonarchimedeanRing A
[PROOFSTEP]
letI := hB.topology
[GOAL]
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
this : TopologicalSpace A := topology hB
⊢ NonarchimedeanRing A
[PROOFSTEP]
constructor
[GOAL]
case is_nonarchimedean
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
this : TopologicalSpace A := topology hB
⊢ ∀ (U : Set A), U ∈ 𝓝 0 → ∃ V, ↑V ⊆ U
[PROOFSTEP]
intro U hU
[GOAL]
case is_nonarchimedean
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
this : TopologicalSpace A := topology hB
U : Set A
hU : U ∈ 𝓝 0
⊢ ∃ V, ↑V ⊆ U
[PROOFSTEP]
obtain ⟨i, -, hi : (B i : Set A) ⊆ U⟩ := hB.hasBasis_nhds_zero.mem_iff.mp hU
[GOAL]
case is_nonarchimedean.intro.intro
A : Type u_1
ι : Type u_2
inst✝¹ : Ring A
inst✝ : Nonempty ι
B : ι → AddSubgroup A
hB : RingSubgroupsBasis B
this : TopologicalSpace A := topology hB
U : Set A
hU : U ∈ 𝓝 0
i : ι
hi : ↑(B i) ⊆ U
⊢ ∃ V, ↑V ⊆ U
[PROOFSTEP]
exact ⟨hB.openAddSubgroup i, hi⟩
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
B : ι → Submodule R A
hB✝ hB : SubmodulesRingBasis B
⊢ RingSubgroupsBasis fun i => Submodule.toAddSubgroup (B i)
[PROOFSTEP]
apply RingSubgroupsBasis.of_comm (fun i => (B i).toAddSubgroup) hB.inter hB.mul
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
B : ι → Submodule R A
hB✝ hB : SubmodulesRingBasis B
⊢ ∀ (x : A) (i : ι), ∃ j, ↑(Submodule.toAddSubgroup (B j)) ⊆ (fun y => x * y) ⁻¹' ↑(Submodule.toAddSubgroup (B i))
[PROOFSTEP]
intro a i
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
B : ι → Submodule R A
hB✝ hB : SubmodulesRingBasis B
a : A
i : ι
⊢ ∃ j, ↑(Submodule.toAddSubgroup (B j)) ⊆ (fun y => a * y) ⁻¹' ↑(Submodule.toAddSubgroup (B i))
[PROOFSTEP]
rcases hB.leftMul a i with ⟨j, hj⟩
[GOAL]
case intro
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
B : ι → Submodule R A
hB✝ hB : SubmodulesRingBasis B
a : A
i j : ι
hj : a • B j ≤ B i
⊢ ∃ j, ↑(Submodule.toAddSubgroup (B j)) ⊆ (fun y => a * y) ⁻¹' ↑(Submodule.toAddSubgroup (B i))
[PROOFSTEP]
use j
[GOAL]
case h
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
B : ι → Submodule R A
hB✝ hB : SubmodulesRingBasis B
a : A
i j : ι
hj : a • B j ≤ B i
⊢ ↑(Submodule.toAddSubgroup (B j)) ⊆ (fun y => a * y) ⁻¹' ↑(Submodule.toAddSubgroup (B i))
[PROOFSTEP]
rintro b (b_in : b ∈ B j)
[GOAL]
case h
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
B : ι → Submodule R A
hB✝ hB : SubmodulesRingBasis B
a : A
i j : ι
hj : a • B j ≤ B i
b : A
b_in : b ∈ B j
⊢ b ∈ (fun y => a * y) ⁻¹' ↑(Submodule.toAddSubgroup (B i))
[PROOFSTEP]
exact hj ⟨b, b_in, rfl⟩
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
⊢ Set.Nonempty {U | ∃ i, U = ↑(B i)}
[PROOFSTEP]
inhabit ι
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
inhabited_h : Inhabited ι
⊢ Set.Nonempty {U | ∃ i, U = ↑(B i)}
[PROOFSTEP]
exact ⟨B default, default, rfl⟩
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
⊢ ∀ {x y : Set M}, x ∈ {U | ∃ i, U = ↑(B i)} → y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y
[PROOFSTEP]
rintro _ _ ⟨i, rfl⟩ ⟨j, rfl⟩
[GOAL]
case intro.intro
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i j : ι
⊢ ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ ↑(B i) ∩ ↑(B j)
[PROOFSTEP]
cases' hB.inter i j with k hk
[GOAL]
case intro.intro.intro
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i j k : ι
hk : B k ≤ B i ⊓ B j
⊢ ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ ↑(B i) ∩ ↑(B j)
[PROOFSTEP]
use B k
[GOAL]
case h
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i j k : ι
hk : B k ≤ B i ⊓ B j
⊢ ↑(B k) ∈ {U | ∃ i, U = ↑(B i)} ∧ ↑(B k) ⊆ ↑(B i) ∩ ↑(B j)
[PROOFSTEP]
constructor
[GOAL]
case h.left
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i j k : ι
hk : B k ≤ B i ⊓ B j
⊢ ↑(B k) ∈ {U | ∃ i, U = ↑(B i)}
[PROOFSTEP]
use k
[GOAL]
case h.right
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i j k : ι
hk : B k ≤ B i ⊓ B j
⊢ ↑(B k) ⊆ ↑(B i) ∩ ↑(B j)
[PROOFSTEP]
exact hk
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
⊢ ∀ {U : Set M},
    U ∈
        { sets := {U | ∃ i, U = ↑(B i)}, nonempty := (_ : ∃ x, x ∈ {U | ∃ i, U = ↑(B i)}),
            inter_sets :=
              (_ :
                ∀ {x y : Set M},
                  x ∈ {U | ∃ i, U = ↑(B i)} →
                    y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y) }.sets →
      0 ∈ U
[PROOFSTEP]
rintro _ ⟨i, rfl⟩
[GOAL]
case intro
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
⊢ 0 ∈ ↑(B i)
[PROOFSTEP]
exact (B i).zero_mem
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
⊢ ∀ {U : Set M},
    U ∈
        { sets := {U | ∃ i, U = ↑(B i)}, nonempty := (_ : ∃ x, x ∈ {U | ∃ i, U = ↑(B i)}),
            inter_sets :=
              (_ :
                ∀ {x y : Set M},
                  x ∈ {U | ∃ i, U = ↑(B i)} →
                    y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y) }.sets →
      ∃ V,
        V ∈
            { sets := {U | ∃ i, U = ↑(B i)}, nonempty := (_ : ∃ x, x ∈ {U | ∃ i, U = ↑(B i)}),
                inter_sets :=
                  (_ :
                    ∀ {x y : Set M},
                      x ∈ {U | ∃ i, U = ↑(B i)} →
                        y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y) }.sets ∧
          V + V ⊆ U
[PROOFSTEP]
rintro _ ⟨i, rfl⟩
[GOAL]
case intro
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
⊢ ∃ V,
    V ∈
        { sets := {U | ∃ i, U = ↑(B i)}, nonempty := (_ : ∃ x, x ∈ {U | ∃ i, U = ↑(B i)}),
            inter_sets :=
              (_ :
                ∀ {x y : Set M},
                  x ∈ {U | ∃ i, U = ↑(B i)} →
                    y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y) }.sets ∧
      V + V ⊆ ↑(B i)
[PROOFSTEP]
use B i
[GOAL]
case h
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
⊢ ↑(B i) ∈
      { sets := {U | ∃ i, U = ↑(B i)}, nonempty := (_ : ∃ x, x ∈ {U | ∃ i, U = ↑(B i)}),
          inter_sets :=
            (_ :
              ∀ {x y : Set M},
                x ∈ {U | ∃ i, U = ↑(B i)} →
                  y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y) }.sets ∧
    ↑(B i) + ↑(B i) ⊆ ↑(B i)
[PROOFSTEP]
constructor
[GOAL]
case h.left
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
⊢ ↑(B i) ∈
    { sets := {U | ∃ i, U = ↑(B i)}, nonempty := (_ : ∃ x, x ∈ {U | ∃ i, U = ↑(B i)}),
        inter_sets :=
          (_ :
            ∀ {x y : Set M},
              x ∈ {U | ∃ i, U = ↑(B i)} → y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y) }.sets
[PROOFSTEP]
use i
[GOAL]
case h.right
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
⊢ ↑(B i) + ↑(B i) ⊆ ↑(B i)
[PROOFSTEP]
rintro x ⟨y, z, y_in, z_in, rfl⟩
[GOAL]
case h.right.intro.intro.intro.intro
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
y z : M
y_in : y ∈ ↑(B i)
z_in : z ∈ ↑(B i)
⊢ (fun x x_1 => x + x_1) y z ∈ ↑(B i)
[PROOFSTEP]
exact (B i).add_mem y_in z_in
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
⊢ ∀ {U : Set M},
    U ∈
        { sets := {U | ∃ i, U = ↑(B i)}, nonempty := (_ : ∃ x, x ∈ {U | ∃ i, U = ↑(B i)}),
            inter_sets :=
              (_ :
                ∀ {x y : Set M},
                  x ∈ {U | ∃ i, U = ↑(B i)} →
                    y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y) }.sets →
      ∃ V,
        V ∈
            { sets := {U | ∃ i, U = ↑(B i)}, nonempty := (_ : ∃ x, x ∈ {U | ∃ i, U = ↑(B i)}),
                inter_sets :=
                  (_ :
                    ∀ {x y : Set M},
                      x ∈ {U | ∃ i, U = ↑(B i)} →
                        y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y) }.sets ∧
          V ⊆ (fun x => -x) ⁻¹' U
[PROOFSTEP]
rintro _ ⟨i, rfl⟩
[GOAL]
case intro
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
⊢ ∃ V,
    V ∈
        { sets := {U | ∃ i, U = ↑(B i)}, nonempty := (_ : ∃ x, x ∈ {U | ∃ i, U = ↑(B i)}),
            inter_sets :=
              (_ :
                ∀ {x y : Set M},
                  x ∈ {U | ∃ i, U = ↑(B i)} →
                    y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y) }.sets ∧
      V ⊆ (fun x => -x) ⁻¹' ↑(B i)
[PROOFSTEP]
use B i
[GOAL]
case h
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
⊢ ↑(B i) ∈
      { sets := {U | ∃ i, U = ↑(B i)}, nonempty := (_ : ∃ x, x ∈ {U | ∃ i, U = ↑(B i)}),
          inter_sets :=
            (_ :
              ∀ {x y : Set M},
                x ∈ {U | ∃ i, U = ↑(B i)} →
                  y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y) }.sets ∧
    ↑(B i) ⊆ (fun x => -x) ⁻¹' ↑(B i)
[PROOFSTEP]
constructor
[GOAL]
case h.left
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
⊢ ↑(B i) ∈
    { sets := {U | ∃ i, U = ↑(B i)}, nonempty := (_ : ∃ x, x ∈ {U | ∃ i, U = ↑(B i)}),
        inter_sets :=
          (_ :
            ∀ {x y : Set M},
              x ∈ {U | ∃ i, U = ↑(B i)} → y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y) }.sets
[PROOFSTEP]
use i
[GOAL]
case h.right
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
⊢ ↑(B i) ⊆ (fun x => -x) ⁻¹' ↑(B i)
[PROOFSTEP]
intro x x_in
[GOAL]
case h.right
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
x : M
x_in : x ∈ ↑(B i)
⊢ x ∈ (fun x => -x) ⁻¹' ↑(B i)
[PROOFSTEP]
exact (B i).neg_mem x_in
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
⊢ ∀ (x₀ : M) {U : Set M},
    U ∈
        { sets := {U | ∃ i, U = ↑(B i)}, nonempty := (_ : ∃ x, x ∈ {U | ∃ i, U = ↑(B i)}),
            inter_sets :=
              (_ :
                ∀ {x y : Set M},
                  x ∈ {U | ∃ i, U = ↑(B i)} →
                    y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y) }.sets →
      ∃ V,
        V ∈
            { sets := {U | ∃ i, U = ↑(B i)}, nonempty := (_ : ∃ x, x ∈ {U | ∃ i, U = ↑(B i)}),
                inter_sets :=
                  (_ :
                    ∀ {x y : Set M},
                      x ∈ {U | ∃ i, U = ↑(B i)} →
                        y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y) }.sets ∧
          V ⊆ (fun x => x₀ + x + -x₀) ⁻¹' U
[PROOFSTEP]
rintro x₀ _ ⟨i, rfl⟩
[GOAL]
case intro
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
x₀ : M
i : ι
⊢ ∃ V,
    V ∈
        { sets := {U | ∃ i, U = ↑(B i)}, nonempty := (_ : ∃ x, x ∈ {U | ∃ i, U = ↑(B i)}),
            inter_sets :=
              (_ :
                ∀ {x y : Set M},
                  x ∈ {U | ∃ i, U = ↑(B i)} →
                    y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y) }.sets ∧
      V ⊆ (fun x => x₀ + x + -x₀) ⁻¹' ↑(B i)
[PROOFSTEP]
use B i
[GOAL]
case h
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
x₀ : M
i : ι
⊢ ↑(B i) ∈
      { sets := {U | ∃ i, U = ↑(B i)}, nonempty := (_ : ∃ x, x ∈ {U | ∃ i, U = ↑(B i)}),
          inter_sets :=
            (_ :
              ∀ {x y : Set M},
                x ∈ {U | ∃ i, U = ↑(B i)} →
                  y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y) }.sets ∧
    ↑(B i) ⊆ (fun x => x₀ + x + -x₀) ⁻¹' ↑(B i)
[PROOFSTEP]
constructor
[GOAL]
case h.left
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
x₀ : M
i : ι
⊢ ↑(B i) ∈
    { sets := {U | ∃ i, U = ↑(B i)}, nonempty := (_ : ∃ x, x ∈ {U | ∃ i, U = ↑(B i)}),
        inter_sets :=
          (_ :
            ∀ {x y : Set M},
              x ∈ {U | ∃ i, U = ↑(B i)} → y ∈ {U | ∃ i, U = ↑(B i)} → ∃ z, z ∈ {U | ∃ i, U = ↑(B i)} ∧ z ⊆ x ∩ y) }.sets
[PROOFSTEP]
use i
[GOAL]
case h.right
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
x₀ : M
i : ι
⊢ ↑(B i) ⊆ (fun x => x₀ + x + -x₀) ⁻¹' ↑(B i)
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
⊢ ∀ {U : Set M},
    U ∈ AddGroupFilterBasis.toFilterBasis.sets →
      ∃ V, V ∈ 𝓝 0 ∧ ∃ W, W ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ V • W ⊆ U
[PROOFSTEP]
rintro _ ⟨i, rfl⟩
[GOAL]
case intro
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
⊢ ∃ V, V ∈ 𝓝 0 ∧ ∃ W, W ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ V • W ⊆ ↑(B i)
[PROOFSTEP]
use univ
[GOAL]
case h
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
⊢ univ ∈ 𝓝 0 ∧ ∃ W, W ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ univ • W ⊆ ↑(B i)
[PROOFSTEP]
constructor
[GOAL]
case h.left
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
⊢ univ ∈ 𝓝 0
[PROOFSTEP]
exact univ_mem
[GOAL]
case h.right
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
⊢ ∃ W, W ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ univ • W ⊆ ↑(B i)
[PROOFSTEP]
use B i
[GOAL]
case h
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
⊢ ↑(B i) ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ univ • ↑(B i) ⊆ ↑(B i)
[PROOFSTEP]
constructor
[GOAL]
case h.left
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
⊢ ↑(B i) ∈ AddGroupFilterBasis.toFilterBasis.sets
[PROOFSTEP]
use i
[GOAL]
case h.right
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
⊢ univ • ↑(B i) ⊆ ↑(B i)
[PROOFSTEP]
rintro _ ⟨a, m, -, hm, rfl⟩
[GOAL]
case h.right.intro.intro.intro.intro
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
a : R
m : M
hm : m ∈ ↑(B i)
⊢ (fun x x_1 => x • x_1) a m ∈ ↑(B i)
[PROOFSTEP]
exact (B i).smul_mem _ hm
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
⊢ ∀ (x₀ : R) {U : Set M},
    U ∈ AddGroupFilterBasis.toFilterBasis.sets →
      ∃ V, V ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ V ⊆ (fun x => x₀ • x) ⁻¹' U
[PROOFSTEP]
rintro x₀ _ ⟨i, rfl⟩
[GOAL]
case intro
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
x₀ : R
i : ι
⊢ ∃ V, V ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ V ⊆ (fun x => x₀ • x) ⁻¹' ↑(B i)
[PROOFSTEP]
use B i
[GOAL]
case h
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
x₀ : R
i : ι
⊢ ↑(B i) ∈ AddGroupFilterBasis.toFilterBasis.sets ∧ ↑(B i) ⊆ (fun x => x₀ • x) ⁻¹' ↑(B i)
[PROOFSTEP]
constructor
[GOAL]
case h.left
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
x₀ : R
i : ι
⊢ ↑(B i) ∈ AddGroupFilterBasis.toFilterBasis.sets
[PROOFSTEP]
use i
[GOAL]
case h.right
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
x₀ : R
i : ι
⊢ ↑(B i) ⊆ (fun x => x₀ • x) ⁻¹' ↑(B i)
[PROOFSTEP]
intro m
[GOAL]
case h.right
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
x₀ : R
i : ι
m : M
⊢ m ∈ ↑(B i) → m ∈ (fun x => x₀ • x) ⁻¹' ↑(B i)
[PROOFSTEP]
exact (B i).smul_mem _
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
⊢ ∀ (m₀ : M) {U : Set M}, U ∈ AddGroupFilterBasis.toFilterBasis.sets → ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ U
[PROOFSTEP]
rintro m₀ _ ⟨i, rfl⟩
[GOAL]
case intro
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
m₀ : M
i : ι
⊢ ∀ᶠ (x : R) in 𝓝 0, x • m₀ ∈ ↑(B i)
[PROOFSTEP]
exact hB.smul m₀ i
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
x✝ : TopologicalSpace M := topology hB
src✝ : AddSubgroup M := Submodule.toAddSubgroup (B i)
⊢ IsOpen
    { toAddSubmonoid := src✝.toAddSubmonoid,
            neg_mem' := (_ : ∀ {x : M}, x ∈ src✝.carrier → -x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
letI := hB.topology
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
x✝ : TopologicalSpace M := topology hB
src✝ : AddSubgroup M := Submodule.toAddSubgroup (B i)
this : TopologicalSpace M := topology hB
⊢ IsOpen
    { toAddSubmonoid := src✝.toAddSubmonoid,
            neg_mem' := (_ : ∀ {x : M}, x ∈ src✝.carrier → -x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
rw [isOpen_iff_mem_nhds]
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
x✝ : TopologicalSpace M := topology hB
src✝ : AddSubgroup M := Submodule.toAddSubgroup (B i)
this : TopologicalSpace M := topology hB
⊢ ∀ (a : M),
    a ∈
        { toAddSubmonoid := src✝.toAddSubmonoid,
                neg_mem' :=
                  (_ : ∀ {x : M}, x ∈ src✝.carrier → -x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier →
      { toAddSubmonoid := src✝.toAddSubmonoid,
                neg_mem' :=
                  (_ : ∀ {x : M}, x ∈ src✝.carrier → -x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier ∈
        𝓝 a
[PROOFSTEP]
intro a a_in
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
x✝ : TopologicalSpace M := topology hB
src✝ : AddSubgroup M := Submodule.toAddSubgroup (B i)
this : TopologicalSpace M := topology hB
a : M
a_in :
  a ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            neg_mem' := (_ : ∀ {x : M}, x ∈ src✝.carrier → -x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
⊢ { toAddSubmonoid := src✝.toAddSubmonoid,
            neg_mem' :=
              (_ : ∀ {x : M}, x ∈ src✝.carrier → -x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier ∈
    𝓝 a
[PROOFSTEP]
rw [(hB.toModuleFilterBasis.toAddGroupFilterBasis.nhds_hasBasis a).mem_iff]
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
x✝ : TopologicalSpace M := topology hB
src✝ : AddSubgroup M := Submodule.toAddSubgroup (B i)
this : TopologicalSpace M := topology hB
a : M
a_in :
  a ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            neg_mem' := (_ : ∀ {x : M}, x ∈ src✝.carrier → -x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
⊢ ∃ i,
    i ∈ (toModuleFilterBasis hB).toAddGroupFilterBasis ∧
      (fun y => a + y) '' i ⊆
        { toAddSubmonoid := src✝.toAddSubmonoid,
                neg_mem' :=
                  (_ : ∀ {x : M}, x ∈ src✝.carrier → -x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
use B i
[GOAL]
case h
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
x✝ : TopologicalSpace M := topology hB
src✝ : AddSubgroup M := Submodule.toAddSubgroup (B i)
this : TopologicalSpace M := topology hB
a : M
a_in :
  a ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            neg_mem' := (_ : ∀ {x : M}, x ∈ src✝.carrier → -x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
⊢ ↑(B i) ∈ (toModuleFilterBasis hB).toAddGroupFilterBasis ∧
    (fun y => a + y) '' ↑(B i) ⊆
      { toAddSubmonoid := src✝.toAddSubmonoid,
              neg_mem' :=
                (_ : ∀ {x : M}, x ∈ src✝.carrier → -x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
constructor
[GOAL]
case h.left
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
x✝ : TopologicalSpace M := topology hB
src✝ : AddSubgroup M := Submodule.toAddSubgroup (B i)
this : TopologicalSpace M := topology hB
a : M
a_in :
  a ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            neg_mem' := (_ : ∀ {x : M}, x ∈ src✝.carrier → -x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
⊢ ↑(B i) ∈ (toModuleFilterBasis hB).toAddGroupFilterBasis
[PROOFSTEP]
use i
[GOAL]
case h.right
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
x✝ : TopologicalSpace M := topology hB
src✝ : AddSubgroup M := Submodule.toAddSubgroup (B i)
this : TopologicalSpace M := topology hB
a : M
a_in :
  a ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            neg_mem' := (_ : ∀ {x : M}, x ∈ src✝.carrier → -x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
⊢ (fun y => a + y) '' ↑(B i) ⊆
    { toAddSubmonoid := src✝.toAddSubmonoid,
            neg_mem' := (_ : ∀ {x : M}, x ∈ src✝.carrier → -x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
rintro - ⟨b, b_in, rfl⟩
[GOAL]
case h.right.intro.intro
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB : SubmodulesBasis B
i : ι
x✝ : TopologicalSpace M := topology hB
src✝ : AddSubgroup M := Submodule.toAddSubgroup (B i)
this : TopologicalSpace M := topology hB
a : M
a_in :
  a ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            neg_mem' := (_ : ∀ {x : M}, x ∈ src✝.carrier → -x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
b : M
b_in : b ∈ ↑(B i)
⊢ (fun y => a + y) b ∈
    { toAddSubmonoid := src✝.toAddSubmonoid,
            neg_mem' := (_ : ∀ {x : M}, x ∈ src✝.carrier → -x ∈ src✝.carrier) }.toAddSubmonoid.toAddSubsemigroup.carrier
[PROOFSTEP]
exact (B i).add_mem a_in b_in
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB✝ hB : SubmodulesBasis B
⊢ NonarchimedeanAddGroup M
[PROOFSTEP]
letI := hB.topology
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB✝ hB : SubmodulesBasis B
this : TopologicalSpace M := topology hB
⊢ NonarchimedeanAddGroup M
[PROOFSTEP]
constructor
[GOAL]
case is_nonarchimedean
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB✝ hB : SubmodulesBasis B
this : TopologicalSpace M := topology hB
⊢ ∀ (U : Set M), U ∈ 𝓝 0 → ∃ V, ↑V ⊆ U
[PROOFSTEP]
intro U hU
[GOAL]
case is_nonarchimedean
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB✝ hB : SubmodulesBasis B
this : TopologicalSpace M := topology hB
U : Set M
hU : U ∈ 𝓝 0
⊢ ∃ V, ↑V ⊆ U
[PROOFSTEP]
obtain ⟨-, ⟨i, rfl⟩, hi : (B i : Set M) ⊆ U⟩ :=
  hB.toModuleFilterBasis.toAddGroupFilterBasis.nhds_zero_hasBasis.mem_iff.mp hU
[GOAL]
case is_nonarchimedean.intro.intro.intro
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : TopologicalSpace R
inst✝ : Nonempty ι
B : ι → Submodule R M
hB✝ hB : SubmodulesBasis B
this : TopologicalSpace M := topology hB
U : Set M
hU : U ∈ 𝓝 0
i : ι
hi : ↑(B i) ⊆ U
⊢ ∃ V, ↑V ⊆ U
[PROOFSTEP]
exact ⟨hB.openAddSubgroup i, hi⟩
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
BR : RingFilterBasis R
B : ι → Submodule R M
hB : SubmodulesBasis BR B
x✝ : TopologicalSpace R := topology BR
⊢ ∀ (m : M) (i : ι), ∀ᶠ (a : R) in 𝓝 0, a • m ∈ B i
[PROOFSTEP]
letI := BR.topology
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
BR : RingFilterBasis R
B : ι → Submodule R M
hB : SubmodulesBasis BR B
x✝ : TopologicalSpace R := topology BR
this : TopologicalSpace R := topology BR
⊢ ∀ (m : M) (i : ι), ∀ᶠ (a : R) in 𝓝 0, a • m ∈ B i
[PROOFSTEP]
intro m i
[GOAL]
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
BR : RingFilterBasis R
B : ι → Submodule R M
hB : SubmodulesBasis BR B
x✝ : TopologicalSpace R := topology BR
this : TopologicalSpace R := topology BR
m : M
i : ι
⊢ ∀ᶠ (a : R) in 𝓝 0, a • m ∈ B i
[PROOFSTEP]
rcases hB.smul m i with ⟨V, V_in, hV⟩
[GOAL]
case intro.intro
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
BR : RingFilterBasis R
B : ι → Submodule R M
hB : SubmodulesBasis BR B
x✝ : TopologicalSpace R := topology BR
this : TopologicalSpace R := topology BR
m : M
i : ι
V : Set R
V_in : V ∈ BR
hV : V ⊆ (fun x => x • m) ⁻¹' ↑(B i)
⊢ ∀ᶠ (a : R) in 𝓝 0, a • m ∈ B i
[PROOFSTEP]
exact mem_of_superset (BR.toAddGroupFilterBasis.mem_nhds_zero V_in) hV


[GOAL]
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : NonarchimedeanGroup G
H : Type u_2
inst✝⁵ : Group H
inst✝⁴ : TopologicalSpace H
inst✝³ : TopologicalGroup H
K : Type u_3
inst✝² : Group K
inst✝¹ : TopologicalSpace K
inst✝ : NonarchimedeanGroup K
f : G →* H
emb : OpenEmbedding ↑f
U : Set H
hU : U ∈ nhds 1
⊢ ↑f ⁻¹' U ∈ nhds 1
[PROOFSTEP]
apply emb.continuous.tendsto
[GOAL]
case a
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : NonarchimedeanGroup G
H : Type u_2
inst✝⁵ : Group H
inst✝⁴ : TopologicalSpace H
inst✝³ : TopologicalGroup H
K : Type u_3
inst✝² : Group K
inst✝¹ : TopologicalSpace K
inst✝ : NonarchimedeanGroup K
f : G →* H
emb : OpenEmbedding ↑f
U : Set H
hU : U ∈ nhds 1
⊢ U ∈ nhds (↑f 1)
[PROOFSTEP]
rwa [f.map_one]
[GOAL]
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : NonarchimedeanGroup G
H : Type u_2
inst✝⁵ : Group H
inst✝⁴ : TopologicalSpace H
inst✝³ : TopologicalGroup H
K : Type u_3
inst✝² : Group K
inst✝¹ : TopologicalSpace K
inst✝ : NonarchimedeanGroup K
U : Set (G × K)
hU : U ∈ nhds 1
⊢ ∃ V W, ↑V ×ˢ ↑W ⊆ U
[PROOFSTEP]
erw [nhds_prod_eq, Filter.mem_prod_iff] at hU
[GOAL]
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : NonarchimedeanGroup G
H : Type u_2
inst✝⁵ : Group H
inst✝⁴ : TopologicalSpace H
inst✝³ : TopologicalGroup H
K : Type u_3
inst✝² : Group K
inst✝¹ : TopologicalSpace K
inst✝ : NonarchimedeanGroup K
U : Set (G × K)
hU : ∃ t₁, t₁ ∈ nhds 1 ∧ ∃ t₂, t₂ ∈ nhds 1 ∧ t₁ ×ˢ t₂ ⊆ U
⊢ ∃ V W, ↑V ×ˢ ↑W ⊆ U
[PROOFSTEP]
rcases hU with ⟨U₁, hU₁, U₂, hU₂, h⟩
[GOAL]
case intro.intro.intro.intro
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : NonarchimedeanGroup G
H : Type u_2
inst✝⁵ : Group H
inst✝⁴ : TopologicalSpace H
inst✝³ : TopologicalGroup H
K : Type u_3
inst✝² : Group K
inst✝¹ : TopologicalSpace K
inst✝ : NonarchimedeanGroup K
U : Set (G × K)
U₁ : Set G
hU₁ : U₁ ∈ nhds 1
U₂ : Set K
hU₂ : U₂ ∈ nhds 1
h : U₁ ×ˢ U₂ ⊆ U
⊢ ∃ V W, ↑V ×ˢ ↑W ⊆ U
[PROOFSTEP]
cases' is_nonarchimedean _ hU₁ with V hV
[GOAL]
case intro.intro.intro.intro.intro
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : NonarchimedeanGroup G
H : Type u_2
inst✝⁵ : Group H
inst✝⁴ : TopologicalSpace H
inst✝³ : TopologicalGroup H
K : Type u_3
inst✝² : Group K
inst✝¹ : TopologicalSpace K
inst✝ : NonarchimedeanGroup K
U : Set (G × K)
U₁ : Set G
hU₁ : U₁ ∈ nhds 1
U₂ : Set K
hU₂ : U₂ ∈ nhds 1
h : U₁ ×ˢ U₂ ⊆ U
V : OpenSubgroup G
hV : ↑V ⊆ U₁
⊢ ∃ V W, ↑V ×ˢ ↑W ⊆ U
[PROOFSTEP]
cases' is_nonarchimedean _ hU₂ with W hW
[GOAL]
case intro.intro.intro.intro.intro.intro
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : NonarchimedeanGroup G
H : Type u_2
inst✝⁵ : Group H
inst✝⁴ : TopologicalSpace H
inst✝³ : TopologicalGroup H
K : Type u_3
inst✝² : Group K
inst✝¹ : TopologicalSpace K
inst✝ : NonarchimedeanGroup K
U : Set (G × K)
U₁ : Set G
hU₁ : U₁ ∈ nhds 1
U₂ : Set K
hU₂ : U₂ ∈ nhds 1
h : U₁ ×ˢ U₂ ⊆ U
V : OpenSubgroup G
hV : ↑V ⊆ U₁
W : OpenSubgroup K
hW : ↑W ⊆ U₂
⊢ ∃ V W, ↑V ×ˢ ↑W ⊆ U
[PROOFSTEP]
use V
[GOAL]
case h
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : NonarchimedeanGroup G
H : Type u_2
inst✝⁵ : Group H
inst✝⁴ : TopologicalSpace H
inst✝³ : TopologicalGroup H
K : Type u_3
inst✝² : Group K
inst✝¹ : TopologicalSpace K
inst✝ : NonarchimedeanGroup K
U : Set (G × K)
U₁ : Set G
hU₁ : U₁ ∈ nhds 1
U₂ : Set K
hU₂ : U₂ ∈ nhds 1
h : U₁ ×ˢ U₂ ⊆ U
V : OpenSubgroup G
hV : ↑V ⊆ U₁
W : OpenSubgroup K
hW : ↑W ⊆ U₂
⊢ ∃ W, ↑V ×ˢ ↑W ⊆ U
[PROOFSTEP]
use W
[GOAL]
case h
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : NonarchimedeanGroup G
H : Type u_2
inst✝⁵ : Group H
inst✝⁴ : TopologicalSpace H
inst✝³ : TopologicalGroup H
K : Type u_3
inst✝² : Group K
inst✝¹ : TopologicalSpace K
inst✝ : NonarchimedeanGroup K
U : Set (G × K)
U₁ : Set G
hU₁ : U₁ ∈ nhds 1
U₂ : Set K
hU₂ : U₂ ∈ nhds 1
h : U₁ ×ˢ U₂ ⊆ U
V : OpenSubgroup G
hV : ↑V ⊆ U₁
W : OpenSubgroup K
hW : ↑W ⊆ U₂
⊢ ↑V ×ˢ ↑W ⊆ U
[PROOFSTEP]
rw [Set.prod_subset_iff]
[GOAL]
case h
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : NonarchimedeanGroup G
H : Type u_2
inst✝⁵ : Group H
inst✝⁴ : TopologicalSpace H
inst✝³ : TopologicalGroup H
K : Type u_3
inst✝² : Group K
inst✝¹ : TopologicalSpace K
inst✝ : NonarchimedeanGroup K
U : Set (G × K)
U₁ : Set G
hU₁ : U₁ ∈ nhds 1
U₂ : Set K
hU₂ : U₂ ∈ nhds 1
h : U₁ ×ˢ U₂ ⊆ U
V : OpenSubgroup G
hV : ↑V ⊆ U₁
W : OpenSubgroup K
hW : ↑W ⊆ U₂
⊢ ∀ (x : G), x ∈ ↑V → ∀ (y : K), y ∈ ↑W → (x, y) ∈ U
[PROOFSTEP]
intro x hX y hY
[GOAL]
case h
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : NonarchimedeanGroup G
H : Type u_2
inst✝⁵ : Group H
inst✝⁴ : TopologicalSpace H
inst✝³ : TopologicalGroup H
K : Type u_3
inst✝² : Group K
inst✝¹ : TopologicalSpace K
inst✝ : NonarchimedeanGroup K
U : Set (G × K)
U₁ : Set G
hU₁ : U₁ ∈ nhds 1
U₂ : Set K
hU₂ : U₂ ∈ nhds 1
h : U₁ ×ˢ U₂ ⊆ U
V : OpenSubgroup G
hV : ↑V ⊆ U₁
W : OpenSubgroup K
hW : ↑W ⊆ U₂
x : G
hX : x ∈ ↑V
y : K
hY : y ∈ ↑W
⊢ (x, y) ∈ U
[PROOFSTEP]
exact Set.Subset.trans (Set.prod_mono hV hW) h (Set.mem_sep hX hY)
[GOAL]
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : NonarchimedeanGroup G
H : Type u_2
inst✝⁵ : Group H
inst✝⁴ : TopologicalSpace H
inst✝³ : TopologicalGroup H
K : Type u_3
inst✝² : Group K
inst✝¹ : TopologicalSpace K
inst✝ : NonarchimedeanGroup K
U : Set (G × G)
hU : U ∈ nhds 1
V W : OpenSubgroup G
h : ↑V ×ˢ ↑W ⊆ U
⊢ ↑(V ⊓ W) ×ˢ ↑(V ⊓ W) ⊆ U
[PROOFSTEP]
refine' Set.Subset.trans (Set.prod_mono _ _) ‹_›
[GOAL]
case refine'_1
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : NonarchimedeanGroup G
H : Type u_2
inst✝⁵ : Group H
inst✝⁴ : TopologicalSpace H
inst✝³ : TopologicalGroup H
K : Type u_3
inst✝² : Group K
inst✝¹ : TopologicalSpace K
inst✝ : NonarchimedeanGroup K
U : Set (G × G)
hU : U ∈ nhds 1
V W : OpenSubgroup G
h : ↑V ×ˢ ↑W ⊆ U
⊢ ↑(V ⊓ W) ⊆ ↑V
[PROOFSTEP]
simp
[GOAL]
case refine'_2
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : NonarchimedeanGroup G
H : Type u_2
inst✝⁵ : Group H
inst✝⁴ : TopologicalSpace H
inst✝³ : TopologicalGroup H
K : Type u_3
inst✝² : Group K
inst✝¹ : TopologicalSpace K
inst✝ : NonarchimedeanGroup K
U : Set (G × G)
hU : U ∈ nhds 1
V W : OpenSubgroup G
h : ↑V ×ˢ ↑W ⊆ U
⊢ ↑(V ⊓ W) ⊆ ↑W
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
S : Type u_2
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
[PROOFSTEP]
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, mul_zero] using U.zero_mem))
[GOAL]
R : Type u_1
S : Type u_2
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
[PROOFSTEP]
simpa only [Set.mem_preimage, SetLike.mem_coe, Prod.snd_zero, mul_zero] using U.zero_mem
[GOAL]
R : Type u_1
S : Type u_2
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
[PROOFSTEP]
use V
[GOAL]
case h
R : Type u_1
S : Type u_2
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
[PROOFSTEP]
rintro v ⟨a, b, ha, hb, hv⟩
[GOAL]
case h.intro.intro.intro.intro
R : Type u_1
S : Type u_2
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
[PROOFSTEP]
have hy := H (Set.mk_mem_prod ha hb)
[GOAL]
case h.intro.intro.intro.intro
R : Type u_1
S : Type u_2
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
[PROOFSTEP]
simp only [Set.mem_preimage, SetLike.mem_coe, hv] at hy
[GOAL]
case h.intro.intro.intro.intro
R : Type u_1
S : Type u_2
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
[PROOFSTEP]
rw [SetLike.mem_coe]
[GOAL]
case h.intro.intro.intro.intro
R : Type u_1
S : Type u_2
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
[PROOFSTEP]
exact hy