-- Mathlib/Topology/Algebra/Valued/ValuationTopology.lean
theorem subgroups_basis : RingSubgroupsBasis fun γ : Γ₀ˣ => (v.ltAddSubgroup γ : AddSubgroup R) :=
  { inter

Proof state:
case h.intro.intro.intro.intro
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ γ₀ : Γ₀ˣ
h : γ₀ * γ₀ ≤ γ
r : R
r_in : v r < ↑γ₀
s : R
s_in : v s < ↑γ₀
⊢ (fun x1 x2 => x1 * x2) r s ∈ ↑(v.ltAddSubgroup γ)

Tactic:
calc
  (v (r * s) : Γ₀) = v r * v s := Valuation.map_mul _ _ _
  _ < γ₀ * γ₀ := by gcongr <;> exact zero_le'
  _ ≤ γ := mod_cast h

Result:
no goals

Proof state:
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ γx : Γ₀ˣ
Hx : v x = ↑γx
y : R
vy_lt : v y < ↑(γx⁻¹ * γ)
⊢ v y * ↑γx < ↑γ

Tactic:
rw [Units.val_mul, mul_comm] at vy_lt

Result:
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ γx : Γ₀ˣ
Hx : v x = ↑γx
y : R
vy_lt : v y < ↑γ * ↑γx⁻¹
⊢ v y * ↑γx < ↑γ

Proof state:
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ₀ γ₁ : Γ₀ˣ
⊢ ∀ (a : R), v a < ↑γ₀ → v a < ↑γ₁ → v a < ↑γ₀

Tactic:
tauto

Result:
no goals

Proof state:
case inr.intro
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ γx : Γ₀ˣ
Hx : v x = ↑γx
⊢ ∃ j, ↑(v.ltAddSubgroup j) ⊆ (fun x_1 => x * x_1) ⁻¹' ↑(v.ltAddSubgroup γ)

Tactic:
use γx⁻¹ * γ

Result:
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ γx : Γ₀ˣ
Hx : v x = ↑γx
⊢ ↑(v.ltAddSubgroup (γx⁻¹ * γ)) ⊆ (fun x_1 => x * x_1) ⁻¹' ↑(v.ltAddSubgroup γ)

Proof state:
case inl
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : Γ₀ˣ
Hx : v x = 0
⊢ ∃ j, ↑(v.ltAddSubgroup j) ⊆ (fun x_1 => x * x_1) ⁻¹' ↑(v.ltAddSubgroup γ)

Tactic:
use (1 : Γ₀ˣ)

Result:
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : Γ₀ˣ
Hx : v x = 0
⊢ ↑(v.ltAddSubgroup 1) ⊆ (fun x_1 => x * x_1) ⁻¹' ↑(v.ltAddSubgroup γ)

Proof state:
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : Γ₀ˣ
⊢ ∃ j, ↑(v.ltAddSubgroup j) ⊆ (fun x_1 => x_1 * x) ⁻¹' ↑(v.ltAddSubgroup γ)

Tactic:
rcases GroupWithZero.eq_zero_or_unit (v x) with (Hx | ⟨γx, Hx⟩)

Result:
case inl
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : Γ₀ˣ
Hx : v x = 0
⊢ ∃ j, ↑(v.ltAddSubgroup j) ⊆ (fun x_1 => x_1 * x) ⁻¹' ↑(v.ltAddSubgroup γ)

case inr.intro
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ γx : Γ₀ˣ
Hx : v x = ↑γx
⊢ ∃ j, ↑(v.ltAddSubgroup j) ⊆ (fun x_1 => x_1 * x) ⁻¹' ↑(v.ltAddSubgroup γ)

Proof state:
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ γx : Γ₀ˣ
Hx : v x = ↑γx
⊢ ↑(v.ltAddSubgroup (γx⁻¹ * γ)) ⊆ (fun x_1 => x * x_1) ⁻¹' ↑(v.ltAddSubgroup γ)

Tactic:
rintro y (vy_lt : v y < ↑(γx⁻¹ * γ))

Result:
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ γx : Γ₀ˣ
Hx : v x = ↑γx
y : R
vy_lt : v y < ↑(γx⁻¹ * γ)
⊢ y ∈ (fun x_1 => x * x_1) ⁻¹' ↑(v.ltAddSubgroup γ)

Proof state:
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 ∈ ↑(v.ltAddSubgroup 1)
⊢ 0 < ↑γ

Tactic:
exact Units.zero_lt γ

Result:
no goals

Proof state:
case intro
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ γ₀ : Γ₀ˣ
h : γ₀ * γ₀ ≤ γ
⊢ ∃ j, ↑(v.ltAddSubgroup j) * ↑(v.ltAddSubgroup j) ⊆ ↑(v.ltAddSubgroup γ)

Tactic:
use γ₀

Result:
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ γ₀ : Γ₀ˣ
h : γ₀ * γ₀ ≤ γ
⊢ ↑(v.ltAddSubgroup γ₀) * ↑(v.ltAddSubgroup γ₀) ⊆ ↑(v.ltAddSubgroup γ)

Proof state:
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 ∈ ↑(v.ltAddSubgroup 1)
⊢ v (x * y) < ↑γ

Tactic:
rw [Valuation.map_mul, Hx, zero_mul]

Result:
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 ∈ ↑(v.ltAddSubgroup 1)
⊢ 0 < ↑γ

Proof state:
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 ∈ ↑(v.ltAddSubgroup 1)
⊢ v (y * x) < ↑γ

Tactic:
rw [Valuation.map_mul, Hx, mul_zero]

Result:
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 ∈ ↑(v.ltAddSubgroup 1)
⊢ 0 < ↑γ

Proof state:
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
⊢ ∀ (i j : Γ₀ˣ), ∃ k, v.ltAddSubgroup k ≤ v.ltAddSubgroup i ⊓ v.ltAddSubgroup j

Tactic:
rintro γ₀ γ₁

Result:
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ₀ γ₁ : Γ₀ˣ
⊢ ∃ k, v.ltAddSubgroup k ≤ v.ltAddSubgroup γ₀ ⊓ v.ltAddSubgroup γ₁

Proof state:
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ γx : Γ₀ˣ
Hx : v x = ↑γx
⊢ ↑(v.ltAddSubgroup (γx⁻¹ * γ)) ⊆ (fun x_1 => x_1 * x) ⁻¹' ↑(v.ltAddSubgroup γ)

Tactic:
rintro y (vy_lt : v y < ↑(γx⁻¹ * γ))

Result:
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ γx : Γ₀ˣ
Hx : v x = ↑γx
y : R
vy_lt : v y < ↑(γx⁻¹ * γ)
⊢ y ∈ (fun x_1 => x_1 * x) ⁻¹' ↑(v.ltAddSubgroup γ)

Proof state:
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ γx : Γ₀ˣ
Hx : v x = ↑γx
y : R
vy_lt : v y < ↑(γx⁻¹ * γ)
⊢ y ∈ (fun x_1 => x_1 * x) ⁻¹' ↑(v.ltAddSubgroup γ)

Tactic:
change (v (y * x) : Γ₀) < γ

Result:
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ γx : Γ₀ˣ
Hx : v x = ↑γx
y : R
vy_lt : v y < ↑(γx⁻¹ * γ)
⊢ v (y * x) < ↑γ

Proof state:
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 ∈ ↑(v.ltAddSubgroup 1)
⊢ y ∈ (fun x_1 => x_1 * x) ⁻¹' ↑(v.ltAddSubgroup γ)

Tactic:
change v (y * x) < _

Result:
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 ∈ ↑(v.ltAddSubgroup 1)
⊢ v (y * x) < ↑γ

Proof state:
case h.intro.intro.intro.intro
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ γ₀ : Γ₀ˣ
h : γ₀ * γ₀ ≤ γ
r : R
r_in : r ∈ ↑(v.ltAddSubgroup γ₀)
s : R
s_in : s ∈ ↑(v.ltAddSubgroup γ₀)
⊢ (fun x1 x2 => x1 * x2) r s ∈ ↑(v.ltAddSubgroup γ)

Tactic:
simp only [ltAddSubgroup, AddSubgroup.coe_set_mk, mem_setOf_eq] at r_in s_in

Result:
case h.intro.intro.intro.intro
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ γ₀ : Γ₀ˣ
h : γ₀ * γ₀ ≤ γ
r : R
r_in : v r < ↑γ₀
s : R
s_in : v s < ↑γ₀
⊢ (fun x1 x2 => x1 * x2) r s ∈ ↑(v.ltAddSubgroup γ)

Proof state:
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ γx : Γ₀ˣ
Hx : v x = ↑γx
y : R
vy_lt : v y < ↑(γx⁻¹ * γ)
⊢ y ∈ (fun x_1 => x * x_1) ⁻¹' ↑(v.ltAddSubgroup γ)

Tactic:
change (v (x * y) : Γ₀) < γ

Result:
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ γx : Γ₀ˣ
Hx : v x = ↑γx
y : R
vy_lt : v y < ↑(γx⁻¹ * γ)
⊢ v (x * y) < ↑γ