awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Valued.NormedValued
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⁻¹‖

Tactic:
simp only [toNormedField.one_lt_norm_iff, map_inv₀, one_lt_inv₀ (zero_lt_iff.mpr hx.1),
          lt_of_le_of_ne h hx.2]

Premises used: Iff.mpr, map_inv₀, Valued.toNormedField.one_lt_norm_iff, And.right, And.left, zero_lt_iff, lt_of_le_of_ne, one_lt_inv₀
-- Module: Mathlib.Topology.Algebra.Valued.NormedValued
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 : Γ₀)
h₁ : 1 < ‖x‖
⊢ ∃ (x : L), 1 < ‖x‖

Tactic:
use x
-- Module: Mathlib.Topology.Algebra.Valued.NormedValued
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 : Γ₀)
⊢ 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

Premises used: Iff.mpr, map_inv₀, And.left, zero_lt_iff, inv_le_one₀
-- Module: Mathlib.Topology.Algebra.Valued.NormedValued
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} (α := Γ₀) (1 : Γ₀) ((v : (a : L) → Γ₀) x : Γ₀)
⊢ 1 < ‖x‖

Tactic:
simp only [toNormedField.one_lt_norm_iff, lt_of_le_of_ne h hx.2.symm]

Premises used: Ne.symm, Valued.toNormedField.one_lt_norm_iff, And.right, lt_of_le_of_ne
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
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 : Γ₀)
⊢ IsUnit r

Tactic:
IsUnit.mk0 _ hr

Premises used: IsUnit.mk0
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
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 : Γ₀)
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 : Γ₀)
⊢ Eq.{v + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)

Tactic:
lift r to Γ₀ˣ using IsUnit.mk0 _ hr

Premises used: IsUnit.mk0
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
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 : Γ₀)
inr₁ :
  ∀ (H : LT.lt.{v} (α := Γ₀ˣ) (1 : Γ₀ˣ) (Units.mk0 ((v : (a : K) → Γ₀) x) hx : Γ₀ˣ)),
    Eq.{v + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ Eq.{v + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)

Tactic:
rcases lt_trichotomy (Units.mk0 _ hx) 1 with H | H | H

Premises used: Units.mk0, OfNat.ofNat, lt_trichotomy
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
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 : Γ₀ˣ)
inl :
  ∀ (k : ℕ) (hk : HPow.hPow (α := Γ₀ˣ) (Units.mk0 ((v : (a : K) → Γ₀) x) hx : Γ₀ˣ) k < r),
    Eq.{v + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ Eq.{v + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)

Tactic:
obtain ⟨k, hk⟩ := exists_pow_lt H r

Premises used: exists_pow_lt
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
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
⊢ Ne.{v + 1} (α := Γ₀) ((v : (a : K) → Γ₀) (x ^ k) : Γ₀) (0 : Γ₀)

Tactic:
simp [hx]
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
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
⊢ (↑r : Γ₀) < (v : (a : K) → Γ₀) (x ^ k)

Tactic:
specialize h (x ^ k) (by simp [hx])

Premises used: HPow.hPow
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
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) → Γ₀) (x ^ k)
⊢ Eq.{v + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)

Tactic:
simp [← Units.val_lt_val, ← map_pow, h.not_gt] at hk

Premises used: map_pow, LT.lt.not_gt, Units.val_lt_val
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
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 : Eq.{v + 1} (α := Γ₀ˣ) (Units.mk0 ((v : (a : K) → Γ₀) x) hx : Γ₀ˣ) (1 : Γ₀ˣ)
⊢ Eq.{v + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)

Tactic:
simpa [Units.ext_iff] using H

Premises used: Units.ext_iff
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
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 : Γ₀ˣ)
⊢ LT.lt.{v} (α := Γ₀ˣ) ((Units.mk0 ((v : (a : K) → Γ₀) x) hx)⁻¹ : Γ₀ˣ) (1 : Γ₀ˣ)

Tactic:
rw [← inv_lt_one'] at H

Premises used: inv_lt_one'
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
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 : Γ₀ˣ)
inr :
  ∀ (k : ℕ) (hk : HPow.hPow (α := Γ₀ˣ) ((Units.mk0 ((v : (a : K) → Γ₀) x) hx)⁻¹ : Γ₀ˣ) k < r),
    Eq.{v + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ Eq.{v + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)

Tactic:
obtain ⟨k, hk⟩ := exists_pow_lt H r

Premises used: exists_pow_lt
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
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
⊢ Ne.{v + 1} (α := Γ₀) ((v : (a : K) → Γ₀) (HPow.hPow (β := ℤ) x (-(↑k : ℤ))) : Γ₀) (0 : Γ₀)

Tactic:
simp [hx]
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
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
⊢ (↑r : Γ₀) < (v : (a : K) → Γ₀) (HPow.hPow (β := ℤ) x (-(↑k : ℤ)))

Tactic:
specialize h (x ^ (-k : ℤ)) (by simp [hx])

Premises used: Nat.cast, HPow.hPow, Neg.neg
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
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 : ℤ)))
⊢ (↑r : Γ₀) < (HPow.hPow (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) k)⁻¹

Tactic:
simp only [zpow_neg, zpow_natCast, map_inv₀, map_pow] at h

Premises used: zpow_natCast, map_inv₀, map_pow, zpow_neg
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
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 : Γ₀) < (HPow.hPow (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) k)⁻¹
⊢ Eq.{v + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)

Tactic:
simp [← Units.val_lt_val, h.not_gt, inv_pow] at hk

Premises used: inv_pow, LT.lt.not_gt, Units.val_lt_val
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ₀ γ₁ : (ValueGroup₀ v)ˣ
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)ˣ) → Γ₀ˣ) γ₁)
⊢ ∃ (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)ˣ) → Γ₀ˣ) γ₁)

Tactic:
use min γ₀ γ₁

Premises used: Min.min
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
γ₀ γ₁ : (ValueGroup₀ v)ˣ
⊢ 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
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
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)) :
      Γ₀)
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) : Γ₀)
⊢ 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:
simp [ltAddSubgroup, hmin]

Premises used: Valuation.ltAddSubgroup
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
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)) :
      Γ₀)
h h₁ h₂ h₃ h₄ 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) : Γ₀)
⊢ ∀ (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:
tauto
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
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)ˣ) → Γ₀ˣ) γ₁)
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) : Γ₀)
⊢ ∀ (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)

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

Premises used: Valuation.ltAddSubgroup
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
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)ˣ
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)
⊢ ∃ (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 γ

Premises used: exists_square_le
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
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)ˣ
h : γ₀ * γ₀ ≤ γ
h₁ :
  (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ₀)) : Set R) *
      (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ₀)) : Set R) ⊆
    (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ)) : Set R)
⊢ ∃ (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:
use γ₀
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
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)ˣ
h : γ₀ * γ₀ ≤ γ
r : R
r_in :
  LT.lt.{v} (α := Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑γ₀ : ValueGroup₀ v) : Γ₀)
s : R
s_in :
  LT.lt.{v} (α := Γ₀) ((v : (a : R) → Γ₀) s : Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑γ₀ : ValueGroup₀ v) : Γ₀)
h₁ :
  LT.lt.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (r * s) : Γ₀)
    ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑γ : ValueGroup₀ v) : Γ₀)
⊢ (fun (x1 x2 : R) ↦ x1 * x2) r s ∈
    (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ)) : Set R)

Tactic:
simp only [coe_ltAddSubgroup, Units.coe_map, MonoidHom.coe_coe, mem_setOf_eq]

Premises used: Units.coe_map, MonoidHom.coe_coe, Set.mem_setOf_eq, Valuation.coe_ltAddSubgroup
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
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)ˣ
h : γ₀ * γ₀ ≤ γ
r : R
r_in :
  LT.lt.{v} (α := Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑γ₀ : ValueGroup₀ v) : Γ₀)
s : R
s_in :
  LT.lt.{v} (α := Γ₀) ((v : (a : R) → Γ₀) s : Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑γ₀ : ValueGroup₀ v) : Γ₀)
h₁ :
  ∀ (r_in : (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) r < (↑γ₀ : ValueGroup₀ v)) (s : R)
    (s_in : (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) s < (↑γ₀ : ValueGroup₀ v)),
    (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (r * s) < (↑γ : ValueGroup₀ v)
⊢ LT.lt.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (r * s) : Γ₀)
    ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑γ : ValueGroup₀ v) : Γ₀)

Tactic:
rw [← restrict_lt_iff_lt_embedding] at *

Premises used: Valuation.restrict_lt_iff_lt_embedding