awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : (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) =
    HMul.hMul (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) (β := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) r : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) s : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))

Tactic:
Valuation.map_mul _ _ _

Premises used: Set.Mem, setOf, Valuation.map_mul
-- 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 : (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) r < (↑γ₀ : ValueGroup₀ v)
s : R
s_in : (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) s < (↑γ₀ : ValueGroup₀ v)
a0 :
  LE.le.{v} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) (0 : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
    ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) r : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
c0 :
  LE.le.{v} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) (0 : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
    ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) s : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
⊢ HMul.hMul (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) (β := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) r : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) s : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) <
    (↑γ₀ : ValueGroup₀ v) * (↑γ₀ : ValueGroup₀ v)

Tactic:
gcongr
-- 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 : (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) r < (↑γ₀ : ValueGroup₀ v)
s : R
s_in : (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) s < (↑γ₀ : ValueGroup₀ v)
⊢ LE.le.{v} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) (0 : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
    ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) r : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))

Tactic:
zero_le'

Premises used: zero_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 : γ₀ * γ₀ ≤ γ
r : R
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)
⊢ LE.le.{v} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) (0 : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
    ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) r : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))

Tactic:
exact zero_le'

Premises used: zero_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 : γ₀ * γ₀ ≤ γ
r : R
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)
⊢ LE.le.{v} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) (0 : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
    ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) s : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))

Tactic:
zero_le'

Premises used: zero_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 : γ₀ * γ₀ ≤ γ
r : R
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)
⊢ LE.le.{v} (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) (0 : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
    ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) s : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))

Tactic:
exact zero_le'

Premises used: zero_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 : γ₀ * γ₀ ≤ γ
r : R
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)
⊢ (↑γ₀ : ValueGroup₀ v) * (↑γ₀ : ValueGroup₀ v) ≤ (↑γ : ValueGroup₀ v)

Tactic:
mod_cast h

Premises used: Units.val_le_val._simp_2, Set.Mem, cast, Eq.symm
-- 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 : (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) r < (↑γ₀ : ValueGroup₀ v)
s : R
s_in : (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) s < (↑γ₀ : ValueGroup₀ v)
r₁ :
  HMul.hMul (α := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) (β := ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) r : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀))
      ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) s : ValueGroup₀ (F := R →*₀ Γ₀) (↑v : R →*₀ Γ₀)) <
    (↑γ₀ : ValueGroup₀ v) * (↑γ₀ : ValueGroup₀ v)
⊢ (v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ₀)) (r * s) < (↑γ : ValueGroup₀ v)

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

Premises used: Units.val, HMul.hMul, Valuation.map_mul, DFunLike.coe, Valuation.restrict
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : (ValueGroup₀ v)ˣ
inl :
  ∀ (Hx : Eq.{v + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)),
    ∃ (j : (ValueGroup₀ v)ˣ),
      (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) j)) : Set R) ⊆
        (fun (x_1 : R) ↦ x * x_1) ⁻¹'
          (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ)) : Set R)
inr :
  ∀ (γx : Γ₀ˣ) (Hx : (v : (a : R) → Γ₀) x = (↑γx : Γ₀)),
    ∃ (j : (ValueGroup₀ v)ˣ),
      (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) j)) : Set R) ⊆
        (fun (x_1 : R) ↦ x * x_1) ⁻¹'
          (↑(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) ⊆
      (fun (x_1 : R) ↦ x * x_1) ⁻¹'
        (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ)) : Set R)

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

Premises used: GroupWithZero.eq_zero_or_unit, DFunLike.coe
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : (ValueGroup₀ v)ˣ
Hx : Eq.{v + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
h :
  (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) 1)) : Set R) ⊆
    (fun (x_1 : R) ↦ x * x_1) ⁻¹'
      (↑(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) ⊆
      (fun (x_1 : R) ↦ x * x_1) ⁻¹'
        (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ)) : Set R)

Tactic:
use (1 : (ValueGroup₀ v)ˣ)

Premises used: OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : (ValueGroup₀ v)ˣ
Hx : Eq.{v + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
y : R
h_1 : y ∈ (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) 1)) : Set R)
h :
  LT.lt.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (x * y) : Γ₀)
    ((↑((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ) : Γ₀) : Γ₀)
⊢ Membership.mem (γ := Set R)
    ((fun (x_1 : R) ↦ x * x_1) ⁻¹'
      (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ)) : Set R))
    y

Tactic:
simp only [coe_ltAddSubgroup, preimage_setOf_eq, mem_setOf_eq]

Premises used: Set.mem_setOf_eq, Set.preimage_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 Γ₀
x : R
γ : (ValueGroup₀ v)ˣ
Hx : Eq.{v + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
y : R
h_1 : y ∈ (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) 1)) : Set R)
h : LT.lt.{v} (α := Γ₀) 0 (↑((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ) : Γ₀)
⊢ LT.lt.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (x * y) : Γ₀)
    ((↑((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ) : Γ₀) : Γ₀)

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

Premises used: MulZeroClass.zero_mul, Valuation.map_mul
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : (ValueGroup₀ v)ˣ
Hx : Eq.{v + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
y : R
h : y ∈ (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) 1)) : Set R)
⊢ LT.lt.{v} (α := Γ₀) 0 (↑((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ) : Γ₀)

Tactic:
Units.zero_lt _

Premises used: Units.zero_lt
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : (ValueGroup₀ v)ˣ
Hx : Eq.{v + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
y : R
h : y ∈ (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) 1)) : Set R)
⊢ LT.lt.{v} (α := Γ₀) 0 (↑((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ) : Γ₀)

Tactic:
exact Units.zero_lt _

Premises used: Units.zero_lt
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : (ValueGroup₀ v)ˣ
γx : Γ₀ˣ
Hx : (v : (a : R) → Γ₀) x = (↑γx : Γ₀)
simp : ¬Eq.{v + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
⊢ Ne.{v + 1} (α := ValueGroup₀ v)
    (((restrict₀ v : MonoidWithZeroHom.{u, v} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x : ValueGroup₀ v)
    (0 : ValueGroup₀ v)

Tactic:
simp [restrict₀_apply]

Premises used: MonoidWithZeroHom.ValueGroup₀.restrict₀_apply
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : (ValueGroup₀ v)ˣ
γx : Γ₀ˣ
Hx : (v : (a : R) → Γ₀) x = (↑γx : Γ₀)
⊢ ¬Eq.{v + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)

Tactic:
aesop
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : (ValueGroup₀ v)ˣ
γx : Γ₀ˣ
Hx : (v : (a : R) → Γ₀) x = (↑γx : Γ₀)
⊢ let u : (ValueGroup₀ v)ˣ :=
    Units.mk0 (((restrict₀ v : MonoidWithZeroHom.{u, v} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x) ⋯;
  u = Units.mk0 (((restrict₀ v : MonoidWithZeroHom.{u, v} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x) ⋯

Tactic:
set u : (ValueGroup₀ v)ˣ := Units.mk0 ((restrict₀ v) x)
          (by simp [restrict₀_apply]; aesop) with hu_def

Premises used: Units.mk0, MonoidWithZeroHom.ValueGroup₀.restrict₀, MonoidWithZeroHom.ValueGroup₀, DFunLike.coe
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : (ValueGroup₀ v)ˣ
γx : Γ₀ˣ
Hx : (v : (a : R) → Γ₀) x = (↑γx : Γ₀)
u : (ValueGroup₀ v)ˣ :=
  Units.mk0 (((restrict₀ v : MonoidWithZeroHom.{u, v} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x) ⋯
hu_def : u = Units.mk0 (((restrict₀ v : MonoidWithZeroHom.{u, v} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x) ⋯
⊢ (embedding : (a : ValueGroup₀ v) → Γ₀) (↑u⁻¹ : ValueGroup₀ v) = (↑γx⁻¹ : Γ₀)

Tactic:
simp [restrict₀_apply, embedding_apply, hu_def, Hx]

Premises used: MonoidWithZeroHom.ValueGroup₀.embedding_apply, MonoidWithZeroHom.ValueGroup₀.restrict₀_apply
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : (ValueGroup₀ v)ˣ
γx : Γ₀ˣ
Hx : (v : (a : R) → Γ₀) x = (↑γx : Γ₀)
u : (ValueGroup₀ v)ˣ :=
  Units.mk0 (((restrict₀ v : MonoidWithZeroHom.{u, v} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x) ⋯
hu_def : u = Units.mk0 (((restrict₀ v : MonoidWithZeroHom.{u, v} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x) ⋯
⊢ (embedding : (a : ValueGroup₀ v) → Γ₀) (↑u⁻¹ : ValueGroup₀ v) = (↑γx⁻¹ : Γ₀)

Tactic:
have hu : ValueGroup₀.embedding u⁻¹.1 = γx⁻¹ := by
          simp [restrict₀_apply, embedding_apply, hu_def, Hx]
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : (ValueGroup₀ v)ˣ
γx : Γ₀ˣ
Hx : (v : (a : R) → Γ₀) x = (↑γx : Γ₀)
u : (ValueGroup₀ v)ˣ :=
  Units.mk0 (((restrict₀ v : MonoidWithZeroHom.{u, v} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x) ⋯
hu_def : u = Units.mk0 (((restrict₀ v : MonoidWithZeroHom.{u, v} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x) ⋯
hu : (embedding : (a : ValueGroup₀ v) → Γ₀) (↑u⁻¹ : ValueGroup₀ v) = (↑γx⁻¹ : Γ₀)
h :
  (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) (u⁻¹ * γ))) :
      Set R) ⊆
    (fun (x_1 : R) ↦ x * x_1) ⁻¹'
      (↑(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) ⊆
      (fun (x_1 : R) ↦ x * x_1) ⁻¹'
        (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ)) : Set R)

Tactic:
use u⁻¹ * γ
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : (ValueGroup₀ v)ˣ
γx : Γ₀ˣ
Hx : (v : (a : R) → Γ₀) x = (↑γx : Γ₀)
u : (ValueGroup₀ v)ˣ :=
  Units.mk0 (((restrict₀ v : MonoidWithZeroHom.{u, v} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x) ⋯
hu_def : u = Units.mk0 (((restrict₀ v : MonoidWithZeroHom.{u, v} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x) ⋯
hu : (embedding : (a : ValueGroup₀ v) → Γ₀) (↑u⁻¹ : ValueGroup₀ v) = (↑γx⁻¹ : Γ₀)
y : R
vy_lt :
  LT.lt.{v} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
    ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑(u⁻¹ * γ) : ValueGroup₀ v) : Γ₀)
h :
  LT.lt.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (x * y) : Γ₀)
    ((↑((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ) : Γ₀) : Γ₀)
⊢ Membership.mem (γ := Set R)
    ((fun (x_1 : R) ↦ x * x_1) ⁻¹'
      (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ)) : Set R))
    y

Tactic:
simp only [coe_ltAddSubgroup, preimage_setOf_eq, mem_setOf_eq]

Premises used: Set.mem_setOf_eq, Set.preimage_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 Γ₀
x : R
γ : (ValueGroup₀ v)ˣ
γx : Γ₀ˣ
Hx : (v : (a : R) → Γ₀) x = (↑γx : Γ₀)
u : (ValueGroup₀ v)ˣ :=
  Units.mk0 (((restrict₀ v : MonoidWithZeroHom.{u, v} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x) ⋯
hu_def : u = Units.mk0 (((restrict₀ v : MonoidWithZeroHom.{u, v} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x) ⋯
hu : (embedding : (a : ValueGroup₀ v) → Γ₀) (↑u⁻¹ : ValueGroup₀ v) = (↑γx⁻¹ : Γ₀)
y : R
vy_lt :
  LT.lt.{v} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
    ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑(u⁻¹ * γ) : ValueGroup₀ v) : Γ₀)
h :
  HMul.hMul (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (↑γx : Γ₀) <
    (↑((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ) : Γ₀)
⊢ LT.lt.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (x * y) : Γ₀)
    ((↑((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ) : Γ₀) : Γ₀)

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

Premises used: Valuation.map_mul, mul_comm
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : (ValueGroup₀ v)ˣ
γx : Γ₀ˣ
Hx : (v : (a : R) → Γ₀) x = (↑γx : Γ₀)
u : (ValueGroup₀ v)ˣ :=
  Units.mk0 (((restrict₀ v : MonoidWithZeroHom.{u, v} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x) ⋯
hu_def : u = Units.mk0 (((restrict₀ v : MonoidWithZeroHom.{u, v} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x) ⋯
hu : (embedding : (a : ValueGroup₀ v) → Γ₀) (↑u⁻¹ : ValueGroup₀ v) = (↑γx⁻¹ : Γ₀)
y : R
vy_lt :
  LT.lt.{v} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
    ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑(u⁻¹ * γ) : ValueGroup₀ v) : Γ₀)
⊢ (v : (a : R) → Γ₀) y <
    HMul.hMul (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑γ : ValueGroup₀ v) : Γ₀) (↑γx⁻¹ : Γ₀)

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

Premises used: map_mul, mul_comm, Units.val_mul
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : (ValueGroup₀ v)ˣ
γx : Γ₀ˣ
Hx : (v : (a : R) → Γ₀) x = (↑γx : Γ₀)
u : (ValueGroup₀ v)ˣ :=
  Units.mk0 (((restrict₀ v : MonoidWithZeroHom.{u, v} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x) ⋯
hu_def : u = Units.mk0 (((restrict₀ v : MonoidWithZeroHom.{u, v} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x) ⋯
hu : (embedding : (a : ValueGroup₀ v) → Γ₀) (↑u⁻¹ : ValueGroup₀ v) = (↑γx⁻¹ : Γ₀)
y : R
vy_lt :
  (v : (a : R) → Γ₀) y <
    HMul.hMul (α := Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑γ : ValueGroup₀ v) : Γ₀) (↑γx⁻¹ : Γ₀)
⊢ HMul.hMul (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (↑γx : Γ₀) <
    (↑((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ) : Γ₀)

Tactic:
simpa using mul_inv_lt_of_lt_mul₀ vy_lt

Premises used: mul_inv_lt_of_lt_mul₀
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : (ValueGroup₀ v)ˣ
inl :
  ∀ (Hx : Eq.{v + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)),
    ∃ (j : (ValueGroup₀ v)ˣ),
      (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) j)) : Set R) ⊆
        (fun (x_1 : R) ↦ x_1 * x) ⁻¹'
          (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ)) : Set R)
inr :
  ∀ (γx : Γ₀ˣ) (Hx : (v : (a : R) → Γ₀) x = (↑γx : Γ₀)),
    ∃ (j : (ValueGroup₀ v)ˣ),
      (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) j)) : Set R) ⊆
        (fun (x_1 : R) ↦ x_1 * x) ⁻¹'
          (↑(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) ⊆
      (fun (x_1 : R) ↦ x_1 * x) ⁻¹'
        (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ)) : Set R)

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

Premises used: GroupWithZero.eq_zero_or_unit, DFunLike.coe
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : (ValueGroup₀ v)ˣ
Hx : Eq.{v + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
h :
  (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) 1)) : Set R) ⊆
    (fun (x_1 : R) ↦ x_1 * x) ⁻¹'
      (↑(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) ⊆
      (fun (x_1 : R) ↦ x_1 * x) ⁻¹'
        (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ)) : Set R)

Tactic:
use 1
-- Module: Mathlib.Topology.Algebra.Valued.ValuationTopology
Goal:
R : Type u
inst : Ring R
Γ₀ : Type v
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
x : R
γ : (ValueGroup₀ v)ˣ
Hx : Eq.{v + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
y : R
h : y ∈ (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) 1)) : Set R)
⊢ Membership.mem (γ := Set R)
    ((fun (x_1 : R) ↦ x_1 * x) ⁻¹'
      (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ)) : Set R))
    y

Tactic:
simp only [coe_ltAddSubgroup, preimage_setOf_eq, mem_setOf_eq, Valuation.map_mul, Hx,
          mul_zero, Units.zero_lt]

Premises used: Set.mem_setOf_eq, Valuation.map_mul, MulZeroClass.mul_zero, Set.preimage_setOf_eq, Valuation.coe_ltAddSubgroup, Units.zero_lt