awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (hypothesis)
Goal:
K : Type u_1
F : Type u_2
R : Type u_3
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst_1 : CommRing R
inst_2 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
inst_3 : Nontrivial Γ₀
inst_4 : NoZeroDivisors Γ₀
x y : R
hxy : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x * y) : Γ₀) (0 : Γ₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀) ∨
    Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀)
have hxy₁ : HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) = 0
Tactic: rw [v.map_mul x y] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : CommRing R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
a s : R
h : s ∈ v.supp
a' s' : R
h' : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) s' : Γ₀) (0 : Γ₀)
⊢ LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (a' + s') : Γ₀) ((v : (a : R) → Γ₀) a' : Γ₀)
have refine : LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) s' : Γ₀) ((v : (a : R) → Γ₀) a' : Γ₀)
Tactic: refine le_trans (v.map_add a' s') (max_le le_rfl ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (hypothesis)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : CommRing R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
a s : R
h : s ∈ v.supp
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (a + s) : Γ₀) ((v : (a : R) → Γ₀) a : Γ₀)
have aux : ∀ (a s : R),
  Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) s : Γ₀) (0 : Γ₀) →
    LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (a + s) : Γ₀) ((v : (a : R) → Γ₀) a : Γ₀)
Tactic: have aux : ∀ a s, v s = 0 → v (a + s) ≤ v a := by
    intro a' s' h'
    refine le_trans (v.map_add a' s') (max_le le_rfl ?_)
    simp [h']
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : CommRing R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
a s : R
h : s ∈ v.supp
aux :
  ∀ (a s : R),
    Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) s : Γ₀) (0 : Γ₀) →
      LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (a + s) : Γ₀) ((v : (a : R) → Γ₀) a : Γ₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (a + s) : Γ₀) ((v : (a : R) → Γ₀) a : Γ₀)
have apply : LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) a : Γ₀) ((v : (a : R) → Γ₀) (a + s) : Γ₀)
Tactic: apply le_antisymm (aux a s h)
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : CommRing R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
a s : R
h : s ∈ v.supp
aux :
  ∀ (a s : R),
    Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) s : Γ₀) (0 : Γ₀) →
      LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (a + s) : Γ₀) ((v : (a : R) → Γ₀) a : Γ₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (-s) : Γ₀) (0 : Γ₀)
have rwa : ∀ (h : -s ∈ v.supp)
  (aux :
    ∀ (a s : R),
      Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) s : Γ₀) (0 : Γ₀) →
        LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (a + s) : Γ₀) ((v : (a : R) → Γ₀) a : Γ₀)),
  Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (-s) : Γ₀) (0 : Γ₀)
Tactic: rwa [← Ideal.neg_mem_iff] at h
Cleared hypotheses: h, aux
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : CommRing R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
a s : R
h : s ∈ v.supp
aux :
  ∀ (a s : R),
    Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) s : Γ₀) (0 : Γ₀) →
      LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (a + s) : Γ₀) ((v : (a : R) → Γ₀) a : Γ₀)
⊢ LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) a : Γ₀) ((v : (a : R) → Γ₀) (a + s) : Γ₀)
have v₁ : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) a : Γ₀) ((v : (a : R) → Γ₀) (a + s + -s) : Γ₀)
Tactic: calc
    v a = v (a + s + -s) := by simp
    _ ≤ v (a + s) := aux (a + s) (-s) (by rwa [← Ideal.neg_mem_iff] at h)
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : CommRing R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
S : Type u_7
inst_2 : CommRing S
f : S →+* R
x : S
⊢ x ∈ (comap f v).supp ↔ Membership.mem (γ := Ideal S) (Ideal.comap f v.supp) x
have rw : Eq.{u_4 + 1} (α := Γ₀) ((comap f v : (a : S) → Γ₀) x : Γ₀) (0 : Γ₀) ↔
  Membership.mem (γ := Ideal S) (Ideal.comap f v.supp) x
Tactic: rw [mem_supp_iff, Ideal.mem_comap, mem_supp_iff, comap_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : CommRing R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
S : Type u_7
inst_2 : CommRing S
f : S →+* R
x : S
rw :
  Eq.{u_4 + 1} (α := Γ₀) ((comap f v : (a : S) → Γ₀) x : Γ₀) (0 : Γ₀) ↔
    Membership.mem (γ := Ideal S) (Ideal.comap f v.supp) x
⊢ x ∈ (comap f v).supp ↔ Membership.mem (γ := Ideal S) (Ideal.comap f v.supp) x
have rw₁ : Eq.{u_4 + 1} (α := Γ₀) ((comap f v : (a : S) → Γ₀) x : Γ₀) (0 : Γ₀) ↔
  Membership.mem (α := R) v.supp ((f : (a : S) → R) x : R)
Tactic: rw [mem_supp_iff, Ideal.mem_comap, mem_supp_iff, comap_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : CommRing R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
S : Type u_7
inst_2 : CommRing S
f : S →+* R
x : S
rw :
  Eq.{u_4 + 1} (α := Γ₀) ((comap f v : (a : S) → Γ₀) x : Γ₀) (0 : Γ₀) ↔
    Membership.mem (γ := Ideal S) (Ideal.comap f v.supp) x
rw₁ :
  Eq.{u_4 + 1} (α := Γ₀) ((comap f v : (a : S) → Γ₀) x : Γ₀) (0 : Γ₀) ↔
    Membership.mem (α := R) v.supp ((f : (a : S) → R) x : R)
⊢ x ∈ (comap f v).supp ↔ Membership.mem (γ := Ideal S) (Ideal.comap f v.supp) x
have rw₂ : Eq.{u_4 + 1} (α := Γ₀) ((comap f v : (a : S) → Γ₀) x : Γ₀) (0 : Γ₀) ↔
  Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) ((f : (a : S) → R) x : R) : Γ₀) (0 : Γ₀)
Tactic: rw [mem_supp_iff, Ideal.mem_comap, mem_supp_iff, comap_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : CommRing R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
S : Type u_7
inst_2 : CommRing S
f : S →+* R
x : S
rw :
  Eq.{u_4 + 1} (α := Γ₀) ((comap f v : (a : S) → Γ₀) x : Γ₀) (0 : Γ₀) ↔
    Membership.mem (γ := Ideal S) (Ideal.comap f v.supp) x
rw₁ :
  Eq.{u_4 + 1} (α := Γ₀) ((comap f v : (a : S) → Γ₀) x : Γ₀) (0 : Γ₀) ↔
    Membership.mem (α := R) v.supp ((f : (a : S) → R) x : R)
rw₂ :
  Eq.{u_4 + 1} (α := Γ₀) ((comap f v : (a : S) → Γ₀) x : Γ₀) (0 : Γ₀) ↔
    Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) ((f : (a : S) → R) x : R) : Γ₀) (0 : Γ₀)
⊢ x ∈ (comap f v).supp ↔ Membership.mem (γ := Ideal S) (Ideal.comap f v.supp) x
have rw₃ : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) ((f : (a : S) → R) x : R) : Γ₀) (0 : Γ₀) ↔
  Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) ((f : (a : S) → R) x : R) : Γ₀) (0 : Γ₀)
Tactic: rw [mem_supp_iff, Ideal.mem_comap, mem_supp_iff, comap_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
K : Type u_1
F : Type u_2
R_1 : Type u_3
inst : DivisionRing K
Γ₀_1 : Type u_4
Γ'₀ : Type u_5
R : Type u_6
Γ₀ : Type u_7
inst_1 : Ring R
inst_2 : LinearOrderedAddCommMonoidWithTop Γ₀
f g : AddValuation R Γ₀
⊢ Eq (α := (a : R) → Γ₀)
      ((fun (v : AddValuation R Γ₀) ↦ (↑v.toMonoidWithZeroHom : ZeroHom R (Multiplicative Γ₀ᵒᵈ)).toFun) f)
      ((fun (v : AddValuation R Γ₀) ↦ (↑v.toMonoidWithZeroHom : ZeroHom R (Multiplicative Γ₀ᵒᵈ)).toFun) g) →
    f = g
have mk : ∀ (toMonoidWithZeroHom : MonoidWithZeroHom.{u_6, u_7} R (Multiplicative Γ₀ᵒᵈ))
  (map_add_le_max' :
    ∀ (x y : R),
      (↑toMonoidWithZeroHom : ZeroHom R (Multiplicative Γ₀ᵒᵈ)).toFun (x + y) ≤
        max ((↑toMonoidWithZeroHom : ZeroHom R (Multiplicative Γ₀ᵒᵈ)).toFun x)
          ((↑toMonoidWithZeroHom : ZeroHom R (Multiplicative Γ₀ᵒᵈ)).toFun y)),
  Eq (α := (a : R) → Γ₀)
      ((fun (v : AddValuation R Γ₀) ↦ (↑v.toMonoidWithZeroHom : ZeroHom R (Multiplicative Γ₀ᵒᵈ)).toFun)
        { toMonoidWithZeroHom := toMonoidWithZeroHom, map_add_le_max' := map_add_le_max' })
      ((fun (v : AddValuation R Γ₀) ↦ (↑v.toMonoidWithZeroHom : ZeroHom R (Multiplicative Γ₀ᵒᵈ)).toFun) g) →
    { toMonoidWithZeroHom := toMonoidWithZeroHom, map_add_le_max' := map_add_le_max' :
        Valuation.{u_6, u_7} R (Multiplicative Γ₀ᵒᵈ) } =
      g
Tactic: cases f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
K : Type u_1
F : Type u_2
R_1 : Type u_3
inst : DivisionRing K
Γ₀_1 : Type u_4
Γ'₀ : Type u_5
R : Type u_6
Γ₀ : Type u_7
inst_1 : Ring R
inst_2 : LinearOrderedAddCommMonoidWithTop Γ₀
g : AddValuation R Γ₀
toMonoidWithZeroHom : MonoidWithZeroHom.{u_6, u_7} R (Multiplicative Γ₀ᵒᵈ)
map_add_le_max' :
  ∀ (x y : R),
    (↑toMonoidWithZeroHom : ZeroHom R (Multiplicative Γ₀ᵒᵈ)).toFun (x + y) ≤
      max ((↑toMonoidWithZeroHom : ZeroHom R (Multiplicative Γ₀ᵒᵈ)).toFun x)
        ((↑toMonoidWithZeroHom : ZeroHom R (Multiplicative Γ₀ᵒᵈ)).toFun y)
⊢ Eq (α := (a : R) → Γ₀)
      ((fun (v : AddValuation R Γ₀) ↦ (↑v.toMonoidWithZeroHom : ZeroHom R (Multiplicative Γ₀ᵒᵈ)).toFun)
        { toMonoidWithZeroHom := toMonoidWithZeroHom, map_add_le_max' := map_add_le_max' })
      ((fun (v : AddValuation R Γ₀) ↦ (↑v.toMonoidWithZeroHom : ZeroHom R (Multiplicative Γ₀ᵒᵈ)).toFun) g) →
    { toMonoidWithZeroHom := toMonoidWithZeroHom, map_add_le_max' := map_add_le_max' :
        Valuation.{u_6, u_7} R (Multiplicative Γ₀ᵒᵈ) } =
      g
have mk : ∀ (toMonoidWithZeroHom_1 : MonoidWithZeroHom.{u_6, u_7} R (Multiplicative Γ₀ᵒᵈ))
  (map_add_le_max'_1 :
    ∀ (x y : R),
      (↑toMonoidWithZeroHom_1 : ZeroHom R (Multiplicative Γ₀ᵒᵈ)).toFun (x + y) ≤
        max ((↑toMonoidWithZeroHom_1 : ZeroHom R (Multiplicative Γ₀ᵒᵈ)).toFun x)
          ((↑toMonoidWithZeroHom_1 : ZeroHom R (Multiplicative Γ₀ᵒᵈ)).toFun y)),
  Eq (α := (a : R) → Γ₀)
      ((fun (v : AddValuation R Γ₀) ↦ (↑v.toMonoidWithZeroHom : ZeroHom R (Multiplicative Γ₀ᵒᵈ)).toFun)
        { toMonoidWithZeroHom := toMonoidWithZeroHom, map_add_le_max' := map_add_le_max' })
      ((fun (v : AddValuation R Γ₀) ↦ (↑v.toMonoidWithZeroHom : ZeroHom R (Multiplicative Γ₀ᵒᵈ)).toFun)
        { toMonoidWithZeroHom := toMonoidWithZeroHom_1, map_add_le_max' := map_add_le_max'_1 }) →
    { toMonoidWithZeroHom := toMonoidWithZeroHom, map_add_le_max' := map_add_le_max' :
        Valuation.{u_6, u_7} R (Multiplicative Γ₀ᵒᵈ) } =
      { toMonoidWithZeroHom := toMonoidWithZeroHom_1, map_add_le_max' := map_add_le_max'_1 }
Tactic: cases g
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀
v : AddValuation R Γ₀
x y : R
⊢ LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) ∨
    LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀)
have rw : LE.le.{u_4} (α := Γ₀) (min ((v : (a : R) → Γ₀) x) ((v : (a : R) → Γ₀) y) : Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀)
Tactic: rw [← min_le_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀
v : AddValuation R Γ₀
x y : R
h : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
have rw : Eq.{u_4 + 1} (α := Γ₀) (min ((v : (a : R) → Γ₀) x) ((v : (a : R) → Γ₀) y) : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
Tactic: rw [map_add_of_distinct_val _ h.ne, min_eq_left h.le]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀
v : AddValuation R Γ₀
x y : R
h : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
rw : Eq.{u_4 + 1} (α := Γ₀) (min ((v : (a : R) → Γ₀) x) ((v : (a : R) → Γ₀) y) : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
have rw₁ : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
Tactic: rw [map_add_of_distinct_val _ h.ne, min_eq_left h.le]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀
v : AddValuation R Γ₀
x y : R
hx : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x - y) : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
have rw : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x + -y) : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
Tactic: rw [sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Basic (goal)
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀
v : AddValuation R Γ₀
x y : R
hx : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x + -y) : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
have h : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) (-y) : Γ₀)
Tactic: apply map_add_eq_of_lt_left
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : Ring A
v : Valuation A Γ
inst_2 : v.IsRankOneDiscrete
⊢ Membership.mem (γ := Subgroup Γˣ) (valueGroup v) (generator v)
have rw : Membership.mem (γ := Subgroup Γˣ) (zpowers (generator v)) (generator v)
Tactic: rw [← IsRankOneDiscrete.generator_zpowers_eq_valueGroup]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_3
inst_1 : Field K
w : Valuation K Γ
inst_2 : w.IsRankOneDiscrete
⊢ Units.val '' (↑(zpowers (generator w)) : Set Γˣ) = range.{u_1, u_3 + 1} (ι := K) (⇑w : (a : K) → Γ) \ {0}
have rw : Units.val '' (↑(valueGroup w) : Set Γˣ) = range.{u_1, u_3 + 1} (ι := K) (⇑w : (a : K) → Γ) \ {0}
Tactic: rw [generator_zpowers_eq_valueGroup, valueGroup_eq_range]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_3
inst_1 : Field K
w : Valuation K Γ
inst_2 : w.IsRankOneDiscrete
rw : Units.val '' (↑(valueGroup w) : Set Γˣ) = range.{u_1, u_3 + 1} (ι := K) (⇑w : (a : K) → Γ) \ {0}
⊢ Units.val '' (↑(zpowers (generator w)) : Set Γˣ) = range.{u_1, u_3 + 1} (ι := K) (⇑w : (a : K) → Γ) \ {0}
have rw₁ : Eq (α := Set Γ) (range.{u_1, u_3 + 1} (ι := K) (⇑w : (a : K) → Γ) \ {0})
  (range.{u_1, u_3 + 1} (ι := K) (⇑w : (a : K) → Γ) \ {0})
Tactic: rw [generator_zpowers_eq_valueGroup, valueGroup_eq_range]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_3
inst_1 : Field K
w : Valuation K Γ
inst_2 : w.IsRankOneDiscrete
⊢ Membership.mem (γ := Set Γ) (range.{u_1, u_3 + 1} (ι := K) (⇑w : (a : K) → Γ)) (↑(generator w) : Γ)
have a : Membership.mem (γ := Set Γ) (range.{u_1, u_3 + 1} (ι := K) (⇑w : (a : K) → Γ) \ {0}) (↑(generator w) : Γ)
Tactic: apply diff_subset
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_3
inst_1 : Field K
w : Valuation K Γ
inst_2 : w.IsRankOneDiscrete
a : Membership.mem (γ := Set Γ) (range.{u_1, u_3 + 1} (ι := K) (⇑w : (a : K) → Γ) \ {0}) (↑(generator w) : Γ)
⊢ Membership.mem (γ := Set Γ) (range.{u_1, u_3 + 1} (ι := K) (⇑w : (a : K) → Γ)) (↑(generator w) : Γ)
have t : Set Γ
Tactic: apply diff_subset
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : Ring A
v : Valuation A Γ
inst_2 : v.IsRankOneDiscrete
⊢ Eq (α := Subgroup ↥(valueGroup v)) (zpowers (generator' v)) ⊤
have rw : zpowers (↑(generator' v) : Γˣ) = valueGroup v
Tactic: rw [← map_subtype_inj, MonoidHom.map_zpowers,
    subtype_apply, ← MonoidHom.range_eq_map, Subgroup.subtype_range]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : Ring A
v : Valuation A Γ
inst_2 : v.IsRankOneDiscrete
⊢ IsCyclic.{u_1} ↥(valueGroup v)
have rw : IsCyclic.{u_1} ↥(zpowers (generator v))
Tactic: rw [← generator_zpowers_eq_valueGroup]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : Ring A
v : Valuation A Γ
inst_2 : v.IsRankOneDiscrete
⊢ v.IsNontrivial
have exists_val_nontrivial : ∃ (x : A),
  Ne.{u_1 + 1} (α := Γ) ((v : (a : A) → Γ) x : Γ) (0 : Γ) ∧ Ne.{u_1 + 1} (α := Γ) ((v : (a : A) → Γ) x : Γ) (1 : Γ)
Tactic: apply IsNontrivial.mk
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : Ring A
v : Valuation A Γ
inst_2 : v.IsRankOneDiscrete
⊢ ∃ (x : A),
    Ne.{u_1 + 1} (α := Γ) ((v : (a : A) → Γ) x : Γ) (0 : Γ) ∧ Ne.{u_1 + 1} (α := Γ) ((v : (a : A) → Γ) x : Γ) (1 : Γ)
have exists_val_nontrivial : ∀
  (h1 :
    ∀ (x : A) (_ : Ne.{u_1 + 1} (α := Γ) ((v : (a : A) → Γ) x : Γ) (0 : Γ)),
      Eq.{u_1 + 1} (α := Γ) ((v : (a : A) → Γ) x : Γ) (1 : Γ)),
  False
Tactic: by_contra! h1
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : Ring A
v : Valuation A Γ
inst_2 : v.IsRankOneDiscrete
h1 :
  ∀ (x : A) (_ : Ne.{u_1 + 1} (α := Γ) ((v : (a : A) → Γ) x : Γ) (0 : Γ)),
    Eq.{u_1 + 1} (α := Γ) ((v : (a : A) → Γ) x : Γ) (1 : Γ)
⊢ Eq (α := Subgroup Γˣ) (valueGroup v) ⊥
have simp : ∀ (y : Γˣ) (x : A) (h : (v : (a : A) → Γ) x = (↑y : Γ)), (↑y : Γ) = (↑1 : Γ)
Tactic: simp only [valueGroup, valueMonoid, Submonoid.coe_set_mk, Subsemigroup.coe_set_mk,
      closure_eq_bot_iff, subset_singleton_iff, mem_preimage, mem_range, forall_exists_index,
      Units.ext_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (hypothesis)
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : Ring A
v : Valuation A Γ
inst_2 : v.IsRankOneDiscrete
h1 :
  ∀ (x : A) (_ : Ne.{u_1 + 1} (α := Γ) ((v : (a : A) → Γ) x : Γ) (0 : Γ)),
    Eq.{u_1 + 1} (α := Γ) ((v : (a : A) → Γ) x : Γ) (1 : Γ)
y : Γˣ
x : A
⊢ ∀ (h : (v : (a : A) → Γ) x = (↑y : Γ)), (↑y : Γ) = (↑1 : Γ)
have h1₁ : ∀ (_ : Ne.{u_1 + 1} (α := Γ) ((v : (a : A) → Γ) x : Γ) (0 : Γ)), Eq.{u_1 + 1} (α := Γ) ((v : (a : A) → Γ) x : Γ) (1 : Γ)
Tactic: specialize h1 x
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (hypothesis)
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : Ring A
v : Valuation A Γ
inst_2 : v.IsRankOneDiscrete
h1 :
  ∀ (x : A) (_ : Ne.{u_1 + 1} (α := Γ) ((v : (a : A) → Γ) x : Γ) (0 : Γ)),
    Eq.{u_1 + 1} (α := Γ) ((v : (a : A) → Γ) x : Γ) (1 : Γ)
⊢ False
have hvalueGroup : Eq (α := Subgroup Γˣ) (valueGroup v) ⊥
Tactic: have hvalueGroup : valueGroup v = ⊥ := by
    simp only [valueGroup, valueMonoid, Submonoid.coe_set_mk, Subsemigroup.coe_set_mk,
      closure_eq_bot_iff, subset_singleton_iff, mem_preimage, mem_range, forall_exists_index,
      Units.ext_iff]
    intro y x
    specialize h1 x
    aesop
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (hypothesis)
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : Ring A
v : Valuation A Γ
hv : v.IsRankOneDiscrete
π : A
hπ : v.IsUniformizer π
h0 : π = 0
⊢ False
have hπ₁ : 0 = (↑(IsRankOneDiscrete.generator v) : Γ)
Tactic: rw [h0, IsUniformizer, map_zero] at hπ
Cleared hypotheses: hπ, h0
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (hypothesis)
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : Ring A
v : Valuation A Γ
hv : v.IsRankOneDiscrete
π : A
hπ : v.IsUniformizer π
h0 : Eq.{u_1 + 1} (α := Γ) ((v : (a : A) → Γ) π : Γ) (0 : Γ)
⊢ False
have hπ₁ : 0 = (↑(IsRankOneDiscrete.generator v) : Γ)
Tactic: simp only [IsUniformizer, h0] at hπ
Cleared hypotheses: hπ
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (hypothesis)
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : Ring A
v : Valuation A Γ
hv : v.IsRankOneDiscrete
π : A
hπ : v.IsUniformizer π
⊢ LT.lt.{u_1} (α := Γ) (0 : Γ) ((v : (a : A) → Γ) π : Γ)
have hπ₁ : (v : (a : A) → Γ) π = (↑(IsRankOneDiscrete.generator v) : Γ)
Tactic: rw [IsUniformizer.iff] at hπ
Cleared hypotheses: hπ
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : Ring A
v : Valuation A Γ
hv : v.IsRankOneDiscrete
π : A
hπ : v.IsUniformizer π
⊢ Eq (α := Subgroup Γˣ) (valueGroup v) (zpowers (Units.mk0 ((v : (a : A) → Γ) π) ⋯))
have rw : Eq.{u_1 + 1} (α := Subgroup Γˣ) (zpowers (Subgroup.genLTOne (valueGroup v)) : Subgroup Γˣ)
  (zpowers (Units.mk0 ((v : (a : A) → Γ) π) sorry) : Subgroup Γˣ)
Tactic: rw [← (valueGroup v).genLTOne_zpowers_eq_top]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : Ring A
v : Valuation A Γ
hv : v.IsRankOneDiscrete
π : A
hπ : v.IsUniformizer π
⊢ Eq.{u_1 + 1} (α := Subgroup Γˣ) (zpowers (Subgroup.genLTOne (valueGroup v)) : Subgroup Γˣ)
    (zpowers (Units.mk0 ((v : (a : A) → Γ) π) ⋯) : Subgroup Γˣ)
have e_g : Eq.{u_1 + 1} (α := Γˣ) (Subgroup.genLTOne (valueGroup v) : Γˣ) (Units.mk0 ((v : (a : A) → Γ) π) sorry : Γˣ)
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : Ring A
v : Valuation A Γ
hv : v.IsRankOneDiscrete
π : A
hπ : v.IsUniformizer π
⊢ Eq.{u_1 + 1} (α := Γˣ) (Subgroup.genLTOne (valueGroup v) : Γˣ) (Units.mk0 ((v : (a : A) → Γ) π) ⋯ : Γˣ)
have e_g : Subgroup.genLTOne (valueGroup v) = IsRankOneDiscrete.generator v
Tactic: simp only [val, Units.mk0_val, hπ]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
inst_2 : IsCyclic.{u_1} ↥(valueGroup v)
inst_3 : Nontrivial.{u_1} ↥(valueGroup v)
⊢ ∃ (π : ↥v.valuationSubring), v.IsUniformizer (↑π : K)
have simp : ∃ (a : K), LE.le.{u_1} (α := Γ) ((v : (a : K) → Γ) a : Γ) (1 : Γ) ∧ (v : (a : K) → Γ) a = (↑(generator v) : Γ)
Tactic: simp only [IsUniformizer.iff, Subtype.exists, mem_valuationSubring_iff, exists_prop]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (hypothesis)
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
inst_2 : IsCyclic.{u_1} ↥(valueGroup v)
inst_3 : Nontrivial.{u_1} ↥(valueGroup v)
⊢ ∃ (a : K), LE.le.{u_1} (α := Γ) ((v : (a : K) → Γ) a : Γ) (1 : Γ) ∧ (v : (a : K) → Γ) a = (↑(generator v) : Γ)
have hg : let g : Γˣ := Subgroup.genLTOne (valueGroup v);
g = Subgroup.genLTOne (valueGroup v)
Tactic: set g := (valueGroup v).genLTOne with hg
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Discrete.Basic (goal)
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
K : Type u_2
inst_1 : Field K
v : Valuation K Γ
inst_2 : IsCyclic.{u_1} ↥(valueGroup v)
inst_3 : Nontrivial.{u_1} ↥(valueGroup v)
g : Γˣ := Subgroup.genLTOne (valueGroup v)
hg : g = Subgroup.genLTOne (valueGroup v)
⊢ Membership.mem (γ := Set Γ) (range.{u_1, u_2 + 1} (ι := K) (⇑v : (a : K) → Γ) \ {0}) (↑g : Γ)
have rw : (↑(Subgroup.genLTOne (valueGroup v)) : Γ) ∈ Units.val '' (↑(valueGroup v) : Set Γˣ)
Tactic: rw [← valueGroup_eq_range, hg]