awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)ˣ
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)
have 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)
Tactic: use γ₀
-- 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)ˣ
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) : Γ₀)
⊢ (fun (x1 x2 : R) ↦ x1 * x2) r s ∈
    (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ)) : Set R)
have h₁ : LT.lt.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (r * s) : Γ₀) ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑γ : ValueGroup₀ v) : Γ₀)
Tactic: simp only [coe_ltAddSubgroup, Units.coe_map, MonoidHom.coe_coe, mem_setOf_eq]
-- 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)ˣ
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) : Γ₀)
⊢ LT.lt.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (r * s) : Γ₀)
    ((embedding : (a : ValueGroup₀ v) → Γ₀) (↑γ : ValueGroup₀ v) : Γ₀)
have 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)
Tactic: rw [← restrict_lt_iff_lt_embedding] at *
Cleared hypotheses: r_in, s, s_in
-- 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)ˣ
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)
⊢ 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)
have 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 →*₀ Γ₀))
Tactic: gcongr
-- 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)ˣ
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 →*₀ Γ₀))
⊢ 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)
have 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 →*₀ Γ₀))
Tactic: gcongr
-- 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)ˣ
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) < (↑γ : ValueGroup₀ v)
have 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: calc
        v.restrict (r * s) = v.restrict r * v.restrict s := Valuation.map_mul _ _ _
        _ < γ₀.1 * γ₀.1 := by gcongr <;> exact zero_le'
        _ ≤ γ := mod_cast 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 Γ₀
x : R
γ : (ValueGroup₀ v)ˣ
⊢ ∃ (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)
have 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)
Tactic: rcases GroupWithZero.eq_zero_or_unit (v x) with (Hx | ⟨γx, Hx⟩)
-- 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 Γ₀
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)
⊢ ∃ (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)
have 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)
Tactic: rcases GroupWithZero.eq_zero_or_unit (v x) with (Hx | ⟨γx, Hx⟩)
-- 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 Γ₀
x : R
γ : (ValueGroup₀ v)ˣ
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)
have 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)
Tactic: use (1 : (ValueGroup₀ v)ˣ)
-- 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 Γ₀
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 * x_1) ⁻¹'
      (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ)) : Set R))
    y
have h : LT.lt.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (x * y) : Γ₀)
  ((↑((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ) : Γ₀) : Γ₀)
Tactic: simp only [coe_ltAddSubgroup, preimage_setOf_eq, mem_setOf_eq]
-- 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 Γ₀
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} (α := Γ₀) ((v : (a : R) → Γ₀) (x * y) : Γ₀)
    ((↑((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ) : Γ₀) : Γ₀)
have h : LT.lt.{v} (α := Γ₀) 0 (↑((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ) : Γ₀)
Tactic: rw [Valuation.map_mul, Hx, zero_mul]
-- 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 Γ₀
x : R
γ : (ValueGroup₀ v)ˣ
γx : Γ₀ˣ
Hx : (v : (a : R) → Γ₀) x = (↑γx : Γ₀)
⊢ Ne.{v + 1} (α := ValueGroup₀ v)
    (((restrict₀ v : MonoidWithZeroHom.{u, v} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x : ValueGroup₀ v)
    (0 : ValueGroup₀ v)
have simp : ¬Eq.{v + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)
Tactic: simp [restrict₀_apply]
-- 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 Γ₀
x : R
γ : (ValueGroup₀ v)ˣ
γ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)
have hu_def : let u : (ValueGroup₀ v)ˣ :=
  Units.mk0 (((restrict₀ v : MonoidWithZeroHom.{u, v} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x) sorry;
u = Units.mk0 (((restrict₀ v : MonoidWithZeroHom.{u, v} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x) sorry
Tactic: set u : (ValueGroup₀ v)ˣ := Units.mk0 ((restrict₀ v) x)
          (by simp [restrict₀_apply]; aesop) with hu_def
-- 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 Γ₀
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) ⋯
⊢ ∃ (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)
have hu : (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]
-- 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 Γ₀
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⁻¹ : Γ₀)
⊢ ∃ (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)
have 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)
Tactic: use u⁻¹ * γ
-- 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 Γ₀
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) : Γ₀)
⊢ Membership.mem (γ := Set R)
    ((fun (x_1 : R) ↦ x * x_1) ⁻¹'
      (↑(v.ltAddSubgroup ((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ)) : Set R))
    y
have h : LT.lt.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (x * y) : Γ₀)
  ((↑((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ) : Γ₀) : Γ₀)
Tactic: simp only [coe_ltAddSubgroup, preimage_setOf_eq, mem_setOf_eq]
-- 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 Γ₀
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) : Γ₀)
⊢ LT.lt.{v} (α := Γ₀) ((v : (a : R) → Γ₀) (x * y) : Γ₀)
    ((↑((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ) : Γ₀) : Γ₀)
have h : HMul.hMul (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (↑γx : Γ₀) <
  (↑((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ) : Γ₀)
Tactic: rw [Valuation.map_mul, Hx, mul_comm]
-- 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 Γ₀
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) : Γ₀)
⊢ HMul.hMul (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (↑γx : Γ₀) <
    (↑((Units.map (↑embedding : ValueGroup₀ v →* Γ₀) : (a : (ValueGroup₀ v)ˣ) → Γ₀ˣ) γ) : Γ₀)
have vy_lt₁ : (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
Cleared hypotheses: vy_lt
-- 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 Γ₀
x : R
γ : (ValueGroup₀ v)ˣ
⊢ ∃ (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)
have 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)
Tactic: rcases GroupWithZero.eq_zero_or_unit (v x) with (Hx | ⟨γx, Hx⟩)
-- 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 Γ₀
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)
⊢ ∃ (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)
have 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)
Tactic: rcases GroupWithZero.eq_zero_or_unit (v x) with (Hx | ⟨γx, Hx⟩)
-- 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 Γ₀
x : R
γ : (ValueGroup₀ v)ˣ
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)
have 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)
Tactic: use 1
-- 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 Γ₀
x : R
γ : (ValueGroup₀ v)ˣ
γ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)
have hu_def : let u : (ValueGroup₀ v)ˣ :=
  Units.mk0 (((restrict₀ v : MonoidWithZeroHom.{u, v} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x) sorry;
u = Units.mk0 (((restrict₀ v : MonoidWithZeroHom.{u, v} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) x) sorry
Tactic: set u : (ValueGroup₀ v)ˣ := Units.mk0 ((restrict₀ v) x)
          (by simp [restrict₀_apply]; aesop) with hu_def
-- 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 Γ₀
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) ⋯
⊢ ∃ (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)
have hu : (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]