awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.NormedValued (goal)
Goal:
L : Type u_1
inst : Field L
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : RankOne.{u_1, u_2} (R := L) v
x : L
⊢ 1 < ‖x‖ ↔ LT.lt.{u_2} (α := Γ₀) (1 : Γ₀) ((v : (a : L) → Γ₀) x : Γ₀)
have rw : 1 < ‖x‖ ↔
  LT.lt.{u_2} (α := ValueGroup₀ (F := L →*₀ Γ₀) (↑v : L →*₀ Γ₀))
    ((Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) 1 : ValueGroup₀ (F := L →*₀ Γ₀) (↑v : L →*₀ Γ₀))
    ((Valuation.restrict v : (a : L) → ValueGroup₀ (↑v : L →*₀ Γ₀)) x : ValueGroup₀ (F := L →*₀ Γ₀) (↑v : L →*₀ Γ₀))
Tactic: rw [← map_one val.v, ← v.restrict_lt_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.NormedValued (goal)
Goal:
L : Type u_1
inst : Field L
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : RankOne.{u_1, u_2} (R := L) v
⊢ Eq.{u_1 + 1} (α := Set L) {x : L | Membership.mem (γ := Subring L) (integer v) x} (Metric.closedBall 0 1)
have h : ∀ (x : L),
  Membership.mem (γ := Set L) {x : L | Membership.mem (γ := Subring L) (integer v) x} x ↔
    Membership.mem (γ := Set L) (Metric.closedBall 0 1) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.NormedValued (goal)
Goal:
L : Type u_1
inst : Field L
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : RankOne.{u_1, u_2} (R := L) v
⊢ ∃ (x : L), 1 < ‖x‖
have obtain : ∀ (x : L)
  (hx :
    Ne.{u_2 + 1} (α := Γ₀) ((v : (a : L) → Γ₀) x : Γ₀) (0 : Γ₀) ∧
      Ne.{u_2 + 1} (α := Γ₀) ((v : (a : L) → Γ₀) x : Γ₀) (1 : Γ₀)),
  ∃ (x : L), 1 < ‖x‖
Tactic: obtain ⟨x, hx⟩ := Valuation.RankOne.nontrivial val.v
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.NormedValued (goal)
Goal:
L : Type u_1
inst : Field L
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : RankOne.{u_1, u_2} (R := L) v
x : L
hx :
  Ne.{u_2 + 1} (α := Γ₀) ((v : (a : L) → Γ₀) x : Γ₀) (0 : Γ₀) ∧
    Ne.{u_2 + 1} (α := Γ₀) ((v : (a : L) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ ∃ (x : L), 1 < ‖x‖
have inl : ∀ (h : LE.le.{u_2} (α := Γ₀) ((v : (a : L) → Γ₀) x : Γ₀) (1 : Γ₀)), ∃ (x : L), 1 < ‖x‖
Tactic: rcases Valuation.val_le_one_or_val_inv_le_one val.v x with h | h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.NormedValued (goal)
Goal:
L : Type u_1
inst : Field L
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : RankOne.{u_1, u_2} (R := L) v
x : L
hx :
  Ne.{u_2 + 1} (α := Γ₀) ((v : (a : L) → Γ₀) x : Γ₀) (0 : Γ₀) ∧
    Ne.{u_2 + 1} (α := Γ₀) ((v : (a : L) → Γ₀) x : Γ₀) (1 : Γ₀)
inl : ∀ (h : LE.le.{u_2} (α := Γ₀) ((v : (a : L) → Γ₀) x : Γ₀) (1 : Γ₀)), ∃ (x : L), 1 < ‖x‖
⊢ ∃ (x : L), 1 < ‖x‖
have inr : ∀ (h : LE.le.{u_2} (α := Γ₀) ((v : (a : L) → Γ₀) x⁻¹ : Γ₀) (1 : Γ₀)), ∃ (x : L), 1 < ‖x‖
Tactic: rcases Valuation.val_le_one_or_val_inv_le_one val.v x with h | h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.NormedValued (goal)
Goal:
L : Type u_1
inst : Field L
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : RankOne.{u_1, u_2} (R := L) v
x : L
hx :
  Ne.{u_2 + 1} (α := Γ₀) ((v : (a : L) → Γ₀) x : Γ₀) (0 : Γ₀) ∧
    Ne.{u_2 + 1} (α := Γ₀) ((v : (a : L) → Γ₀) x : Γ₀) (1 : Γ₀)
h : LE.le.{u_2} (α := Γ₀) ((v : (a : L) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ ∃ (x : L), 1 < ‖x‖
have h₁ : 1 < ‖x⁻¹‖
Tactic: use x⁻¹
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.NormedValued (goal)
Goal:
L : Type u_1
inst : Field L
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : RankOne.{u_1, u_2} (R := L) v
x : L
hx :
  Ne.{u_2 + 1} (α := Γ₀) ((v : (a : L) → Γ₀) x : Γ₀) (0 : Γ₀) ∧
    Ne.{u_2 + 1} (α := Γ₀) ((v : (a : L) → Γ₀) x : Γ₀) (1 : Γ₀)
h : LE.le.{u_2} (α := Γ₀) ((v : (a : L) → Γ₀) x⁻¹ : Γ₀) (1 : Γ₀)
⊢ ∃ (x : L), 1 < ‖x‖
have h₁ : 1 < ‖x‖
Tactic: use x
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.NormedValued (hypothesis)
Goal:
L : Type u_1
inst : Field L
Γ₀ : Type u_2
inst_1 : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : RankOne.{u_1, u_2} (R := L) v
x : L
hx :
  Ne.{u_2 + 1} (α := Γ₀) ((v : (a : L) → Γ₀) x : Γ₀) (0 : Γ₀) ∧
    Ne.{u_2 + 1} (α := Γ₀) ((v : (a : L) → Γ₀) x : Γ₀) (1 : Γ₀)
h : LE.le.{u_2} (α := Γ₀) ((v : (a : L) → Γ₀) x⁻¹ : Γ₀) (1 : Γ₀)
⊢ 1 < ‖x‖
have h₁ : LE.le.{u_2} (α := Γ₀) (1 : Γ₀) ((v : (a : L) → Γ₀) x : Γ₀)
Tactic: simp only [map_inv₀, inv_le_one₀ <| zero_lt_iff.mpr hx.1] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuationTopology (goal)
Goal:
K : Type u
inst : DivisionRing K
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : MulArchimedean Γ₀
v : Valuation K Γ₀
r : Γ₀
hr : r ≠ 0
h : ∀ (x : K), Ne.{v + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀) → r < (v : (a : K) → Γ₀) x
x : K
hx : Ne.{v + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀)
⊢ Eq.{v + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
have lift : ∀ (r : Γ₀ˣ) (hr : (↑r : Γ₀) ≠ 0)
  (h : ∀ (x : K), Ne.{v + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀) → (↑r : Γ₀) < (v : (a : K) → Γ₀) x),
  Eq.{v + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
Tactic: lift r to Γ₀ˣ using IsUnit.mk0 _ hr
Cleared hypotheses: r, hr, h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuationTopology (goal)
Goal:
K : Type u
inst : DivisionRing K
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : MulArchimedean Γ₀
v : Valuation K Γ₀
x : K
hx : Ne.{v + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀)
r : Γ₀ˣ
hr : (↑r : Γ₀) ≠ 0
h : ∀ (x : K), Ne.{v + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀) → (↑r : Γ₀) < (v : (a : K) → Γ₀) x
⊢ Eq.{v + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
have inl : ∀ (H : LT.lt.{v} (α := Γ₀ˣ) (Units.mk0 ((v : (a : K) → Γ₀) x) hx : Γ₀ˣ) (1 : Γ₀ˣ)),
  Eq.{v + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
Tactic: rcases lt_trichotomy (Units.mk0 _ hx) 1 with H | H | H
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuationTopology (goal)
Goal:
K : Type u
inst : DivisionRing K
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : MulArchimedean Γ₀
v : Valuation K Γ₀
x : K
hx : Ne.{v + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀)
r : Γ₀ˣ
hr : (↑r : Γ₀) ≠ 0
h : ∀ (x : K), Ne.{v + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀) → (↑r : Γ₀) < (v : (a : K) → Γ₀) x
inl :
  ∀ (H : LT.lt.{v} (α := Γ₀ˣ) (Units.mk0 ((v : (a : K) → Γ₀) x) hx : Γ₀ˣ) (1 : Γ₀ˣ)),
    Eq.{v + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ Eq.{v + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
have inr : ∀ (H : Eq.{v + 1} (α := Γ₀ˣ) (Units.mk0 ((v : (a : K) → Γ₀) x) hx : Γ₀ˣ) (1 : Γ₀ˣ)),
  Eq.{v + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
Tactic: rcases lt_trichotomy (Units.mk0 _ hx) 1 with H | H | H
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuationTopology (goal)
Goal:
K : Type u
inst : DivisionRing K
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : MulArchimedean Γ₀
v : Valuation K Γ₀
x : K
hx : Ne.{v + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀)
r : Γ₀ˣ
hr : (↑r : Γ₀) ≠ 0
h : ∀ (x : K), Ne.{v + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀) → (↑r : Γ₀) < (v : (a : K) → Γ₀) x
inl :
  ∀ (H : LT.lt.{v} (α := Γ₀ˣ) (Units.mk0 ((v : (a : K) → Γ₀) x) hx : Γ₀ˣ) (1 : Γ₀ˣ)),
    Eq.{v + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
inr :
  ∀ (H : Eq.{v + 1} (α := Γ₀ˣ) (Units.mk0 ((v : (a : K) → Γ₀) x) hx : Γ₀ˣ) (1 : Γ₀ˣ)),
    Eq.{v + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ Eq.{v + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
have inr₁ : ∀ (H : LT.lt.{v} (α := Γ₀ˣ) (1 : Γ₀ˣ) (Units.mk0 ((v : (a : K) → Γ₀) x) hx : Γ₀ˣ)),
  Eq.{v + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
Tactic: rcases lt_trichotomy (Units.mk0 _ hx) 1 with H | H | H
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuationTopology (goal)
Goal:
K : Type u
inst : DivisionRing K
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : MulArchimedean Γ₀
v : Valuation K Γ₀
x : K
hx : Ne.{v + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀)
r : Γ₀ˣ
hr : (↑r : Γ₀) ≠ 0
h : ∀ (x : K), Ne.{v + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀) → (↑r : Γ₀) < (v : (a : K) → Γ₀) x
H : LT.lt.{v} (α := Γ₀ˣ) (Units.mk0 ((v : (a : K) → Γ₀) x) hx : Γ₀ˣ) (1 : Γ₀ˣ)
⊢ Eq.{v + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
have inl : ∀ (k : ℕ) (hk : HPow.hPow (α := Γ₀ˣ) (Units.mk0 ((v : (a : K) → Γ₀) x) hx : Γ₀ˣ) k < r),
  Eq.{v + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
Tactic: obtain ⟨k, hk⟩ := exists_pow_lt H r
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuationTopology (hypothesis)
Goal:
K : Type u
inst : DivisionRing K
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : MulArchimedean Γ₀
v : Valuation K Γ₀
x : K
hx : Ne.{v + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀)
r : Γ₀ˣ
hr : (↑r : Γ₀) ≠ 0
h : ∀ (x : K), Ne.{v + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀) → (↑r : Γ₀) < (v : (a : K) → Γ₀) x
H : LT.lt.{v} (α := Γ₀ˣ) (Units.mk0 ((v : (a : K) → Γ₀) x) hx : Γ₀ˣ) (1 : Γ₀ˣ)
k : ℕ
hk : HPow.hPow (α := Γ₀ˣ) (Units.mk0 ((v : (a : K) → Γ₀) x) hx : Γ₀ˣ) k < r
⊢ Eq.{v + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
have h₁ : (↑r : Γ₀) < (v : (a : K) → Γ₀) (x ^ k)
Tactic: specialize h (x ^ k) (by simp [hx])
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuationTopology (hypothesis)
Goal:
K : Type u
inst : DivisionRing K
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : MulArchimedean Γ₀
v : Valuation K Γ₀
x : K
hx : Ne.{v + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀)
r : Γ₀ˣ
hr : (↑r : Γ₀) ≠ 0
h : ∀ (x : K), Ne.{v + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀) → (↑r : Γ₀) < (v : (a : K) → Γ₀) x
H : LT.lt.{v} (α := Γ₀ˣ) (1 : Γ₀ˣ) (Units.mk0 ((v : (a : K) → Γ₀) x) hx : Γ₀ˣ)
⊢ Eq.{v + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
have H₁ : LT.lt.{v} (α := Γ₀ˣ) ((Units.mk0 ((v : (a : K) → Γ₀) x) hx)⁻¹ : Γ₀ˣ) (1 : Γ₀ˣ)
Tactic: rw [← inv_lt_one'] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuationTopology (goal)
Goal:
K : Type u
inst : DivisionRing K
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : MulArchimedean Γ₀
v : Valuation K Γ₀
x : K
hx : Ne.{v + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀)
r : Γ₀ˣ
hr : (↑r : Γ₀) ≠ 0
h : ∀ (x : K), Ne.{v + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀) → (↑r : Γ₀) < (v : (a : K) → Γ₀) x
H : LT.lt.{v} (α := Γ₀ˣ) ((Units.mk0 ((v : (a : K) → Γ₀) x) hx)⁻¹ : Γ₀ˣ) (1 : Γ₀ˣ)
⊢ Eq.{v + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
have inr : ∀ (k : ℕ) (hk : HPow.hPow (α := Γ₀ˣ) ((Units.mk0 ((v : (a : K) → Γ₀) x) hx)⁻¹ : Γ₀ˣ) k < r),
  Eq.{v + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
Tactic: obtain ⟨k, hk⟩ := exists_pow_lt H r
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuationTopology (hypothesis)
Goal:
K : Type u
inst : DivisionRing K
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : MulArchimedean Γ₀
v : Valuation K Γ₀
x : K
hx : Ne.{v + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀)
r : Γ₀ˣ
hr : (↑r : Γ₀) ≠ 0
h : ∀ (x : K), Ne.{v + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀) → (↑r : Γ₀) < (v : (a : K) → Γ₀) x
H : LT.lt.{v} (α := Γ₀ˣ) ((Units.mk0 ((v : (a : K) → Γ₀) x) hx)⁻¹ : Γ₀ˣ) (1 : Γ₀ˣ)
k : ℕ
hk : HPow.hPow (α := Γ₀ˣ) ((Units.mk0 ((v : (a : K) → Γ₀) x) hx)⁻¹ : Γ₀ˣ) k < r
⊢ Eq.{v + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
have h₁ : (↑r : Γ₀) < (v : (a : K) → Γ₀) (HPow.hPow (β := ℤ) x (-(↑k : ℤ)))
Tactic: specialize h (x ^ (-k : ℤ)) (by simp [hx])
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuationTopology (hypothesis)
Goal:
K : Type u
inst : DivisionRing K
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : MulArchimedean Γ₀
v : Valuation K Γ₀
x : K
hx : Ne.{v + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀)
r : Γ₀ˣ
hr : (↑r : Γ₀) ≠ 0
H : LT.lt.{v} (α := Γ₀ˣ) ((Units.mk0 ((v : (a : K) → Γ₀) x) hx)⁻¹ : Γ₀ˣ) (1 : Γ₀ˣ)
k : ℕ
hk : HPow.hPow (α := Γ₀ˣ) ((Units.mk0 ((v : (a : K) → Γ₀) x) hx)⁻¹ : Γ₀ˣ) k < r
h : (↑r : Γ₀) < (v : (a : K) → Γ₀) (HPow.hPow (β := ℤ) x (-(↑k : ℤ)))
⊢ Eq.{v + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
have h₁ : (↑r : Γ₀) < (HPow.hPow (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) k)⁻¹
Tactic: simp only [zpow_neg, zpow_natCast, map_inv₀, map_pow] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuationTopology (goal)
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ₀ γ₁ : (ValueGroup₀ v)ˣ
⊢ ∃ (k : (ValueGroup₀ v)ˣ),
    v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) k) ≤
      v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ₀) ⊓
        v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ₁)
have h : v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) (min γ₀ γ₁)) ≤
  v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ₀) ⊓
    v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ₁)
Tactic: use min γ₀ γ₁
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuationTopology (hypothesis)
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ₀ γ₁ : (ValueGroup₀ v)ˣ
⊢ v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) (min γ₀ γ₁)) ≤
    v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ₀) ⊓
      v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ₁)
have hmin : Eq (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (min (↑γ₀ : ValueGroup₀ v) (↑γ₁ : ValueGroup₀ v)) : Γ₀)
  (min ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑γ₀ : ValueGroup₀ v))
      ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑γ₁ : ValueGroup₀ v)) :
    Γ₀)
Tactic: have hmin : embedding (min γ₀.1 γ₁.1) = min (embedding γ₀.1) (embedding γ₁.1) :=
        embedding_strictMono.monotone.map_inf γ₀.1 γ₁.1
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuationTopology (goal)
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ₀ γ₁ : (ValueGroup₀ v)ˣ
hmin :
  Eq (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (min (↑γ₀ : ValueGroup₀ v) (↑γ₁ : ValueGroup₀ v)) : Γ₀)
    (min ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑γ₀ : ValueGroup₀ v))
        ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑γ₁ : ValueGroup₀ v)) :
      Γ₀)
⊢ v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) (min γ₀ γ₁)) ≤
    v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ₀) ⊓
      v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ₁)
have h : ∀ (a : R),
  LT.lt.{v} (α := Γ₀) ((v : (a : R) → Γ₀) a : Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑γ₀ : ValueGroup₀ v) : Γ₀) →
    LT.lt.{v} (α := Γ₀) ((v : (a : R) → Γ₀) a : Γ₀)
        ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑γ₁ : ValueGroup₀ v) : Γ₀) →
      LT.lt.{v} (α := Γ₀) ((v : (a : R) → Γ₀) a : Γ₀)
        ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑γ₀ : ValueGroup₀ v) : Γ₀)
Tactic: simp [ltAddSubgroup, hmin]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuationTopology (goal)
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
rintro :
  ∀ (γ₀ γ₁ : (ValueGroup₀ v)ˣ),
    ∃ (k : (ValueGroup₀ v)ˣ),
      v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) k) ≤
        v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ₀) ⊓
          v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ₁)
⊢ ∀ (i j : (ValueGroup₀ v)ˣ),
    ∃ (k : (ValueGroup₀ v)ˣ),
      v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) k) ≤
        v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) i) ⊓
          v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) j)
have h : ∀ (γ₀ γ₁ : (ValueGroup₀ v)ˣ),
  v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) (min γ₀ γ₁)) ≤
    v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ₀) ⊓
      v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ₁)
Tactic: classical
      rintro γ₀ γ₁
      use min γ₀ γ₁
      have hmin : embedding (min γ₀.1 γ₁.1) = min (embedding γ₀.1) (embedding γ₁.1) :=
        embedding_strictMono.monotone.map_inf γ₀.1 γ₁.1
      simp [ltAddSubgroup, hmin]
      tauto
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuationTopology (goal)
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
rintro :
  ∀ (γ₀ γ₁ : (ValueGroup₀ v)ˣ),
    ∃ (k : (ValueGroup₀ v)ˣ),
      v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) k) ≤
        v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ₀) ⊓
          v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ₁)
h :
  ∀ (γ₀ γ₁ : (ValueGroup₀ v)ˣ),
    v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) (min γ₀ γ₁)) ≤
      v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ₀) ⊓
        v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ₁)
⊢ ∀ (i j : (ValueGroup₀ v)ˣ),
    ∃ (k : (ValueGroup₀ v)ˣ),
      v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) k) ≤
        v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) i) ⊓
          v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) j)
have h₁ : ∀ (γ₀ γ₁ : (ValueGroup₀ v)ˣ)
  (hmin :
    Eq (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (min (↑γ₀ : ValueGroup₀ v) (↑γ₁ : ValueGroup₀ v)) : Γ₀)
      (min ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑γ₀ : ValueGroup₀ v))
          ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑γ₁ : ValueGroup₀ v)) :
        Γ₀)),
  v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) (min γ₀ γ₁)) ≤
    v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ₀) ⊓
      v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ₁)
Tactic: classical
      rintro γ₀ γ₁
      use min γ₀ γ₁
      have hmin : embedding (min γ₀.1 γ₁.1) = min (embedding γ₀.1) (embedding γ₁.1) :=
        embedding_strictMono.monotone.map_inf γ₀.1 γ₁.1
      simp [ltAddSubgroup, hmin]
      tauto
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuationTopology (goal)
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
rintro :
  ∀ (γ₀ γ₁ : (ValueGroup₀ v)ˣ),
    ∃ (k : (ValueGroup₀ v)ˣ),
      v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) k) ≤
        v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ₀) ⊓
          v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ₁)
h :
  ∀ (γ₀ γ₁ : (ValueGroup₀ v)ˣ),
    v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) (min γ₀ γ₁)) ≤
      v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ₀) ⊓
        v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ₁)
h₁ :
  ∀ (γ₀ γ₁ : (ValueGroup₀ v)ˣ)
    (hmin :
      Eq (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (min (↑γ₀ : ValueGroup₀ v) (↑γ₁ : ValueGroup₀ v)) : Γ₀)
        (min ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑γ₀ : ValueGroup₀ v))
            ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑γ₁ : ValueGroup₀ v)) :
          Γ₀)),
    v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) (min γ₀ γ₁)) ≤
      v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ₀) ⊓
        v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ₁)
⊢ ∀ (i j : (ValueGroup₀ v)ˣ),
    ∃ (k : (ValueGroup₀ v)ˣ),
      v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) k) ≤
        v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) i) ⊓
          v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) j)
have h₂ : ∀ (γ₀ γ₁ : (ValueGroup₀ v)ˣ)
  (hmin :
    Eq (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (min (↑γ₀ : ValueGroup₀ v) (↑γ₁ : ValueGroup₀ v)) : Γ₀)
      (min ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑γ₀ : ValueGroup₀ v))
          ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑γ₁ : ValueGroup₀ v)) :
        Γ₀))
  (a : R),
  LT.lt.{v} (α := Γ₀) ((v : (a : R) → Γ₀) a : Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑γ₀ : ValueGroup₀ v) : Γ₀) →
    LT.lt.{v} (α := Γ₀) ((v : (a : R) → Γ₀) a : Γ₀)
        ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑γ₁ : ValueGroup₀ v) : Γ₀) →
      LT.lt.{v} (α := Γ₀) ((v : (a : R) → Γ₀) a : Γ₀)
        ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑γ₀ : ValueGroup₀ v) : Γ₀)
Tactic: classical
      rintro γ₀ γ₁
      use min γ₀ γ₁
      have hmin : embedding (min γ₀.1 γ₁.1) = min (embedding γ₀.1) (embedding γ₁.1) :=
        embedding_strictMono.monotone.map_inf γ₀.1 γ₁.1
      simp [ltAddSubgroup, hmin]
      tauto
-- Lean 4 proof step from Mathlib.Topology.Algebra.Valued.ValuationTopology (goal)
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
this : LinearOrderedCommGroupWithZero (ValueGroup₀ v) :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
γ : (ValueGroup₀ v)ˣ
⊢ ∃ (j : (ValueGroup₀ v)ˣ),
    (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) j)) : Set R) *
        (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) j)) : Set R) ⊆
      (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ)) : Set R)
have obtain : ∀ (γ₀ : (ValueGroup₀ v)ˣ) (h : γ₀ * γ₀ ≤ γ),
  ∃ (j : (ValueGroup₀ v)ˣ),
    (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) j)) : Set R) *
        (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) j)) : Set R) ⊆
      (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ)) : Set R)
Tactic: obtain ⟨γ₀, h⟩ := exists_square_le γ