awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
R : Type u
Γ₀ : Type v
inst : CommRing R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O R
hv : v.Integers O
h : Nontrivial R
o0 : O
ho0 : Eq.{u + 1} (α := R) ((algebraMap O R : (a : O) → R) o0 : R) (0 : R)
⊢ Nontrivial O
have mpr : ∀ (o1 : O) (ho1 : Eq.{u + 1} (α := R) ((algebraMap O R : (a : O) → R) o1 : R) (1 : R)), Nontrivial O
Tactic: obtain ⟨o1, ho1⟩ := hv.exists_of_le_one (r := 1) (by simp)
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
R : Type u
Γ₀ : Type v
inst : CommRing R
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation R Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O R
hv : v.Integers O
h : Nontrivial R
o0 : O
ho0 : Eq.{u + 1} (α := R) ((algebraMap O R : (a : O) → R) o0 : R) (0 : R)
o1 : O
ho1 : Eq.{u + 1} (α := R) ((algebraMap O R : (a : O) → R) o1 : R) (1 : R)
⊢ Nontrivial O
have mpr : o0 ≠ o1
Tactic: refine ⟨o0, o1, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
F : Type u
Γ₀ : Type v
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O F
hv : v.Integers O
x y : O
h :
  LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀)
    ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) y : F) : Γ₀)
hy : Ne.{u + 1} (α := F) ((algebraMap O F : (a : O) → F) y : F) (0 : F)
⊢ LE.le.{v} (α := Γ₀)
    ((v : (a : F) → Γ₀)
        (HMul.hMul (α := F) (β := F) (((algebraMap O F : (a : O) → F) y)⁻¹ : F)
          ((algebraMap O F : (a : O) → F) x : F)) :
      Γ₀)
    (1 : Γ₀)
have grw : LE.le.{v} (α := Γ₀)
  ((v : (a : F) → Γ₀)
      (HMul.hMul (α := F) (β := F) (((algebraMap O F : (a : O) → F) y)⁻¹ : F) ((algebraMap O F : (a : O) → F) x : F)) :
    Γ₀)
  ((v : (a : F) → Γ₀) 1 : Γ₀)
Tactic: grw [← v.map_one, ← inv_mul_cancel₀ hy, v.map_mul, v.map_mul, h]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
F : Type u
Γ₀ : Type v
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O F
hv : v.Integers O
x y : O
h :
  LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀)
    ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) y : F) : Γ₀)
hy : Ne.{u + 1} (α := F) ((algebraMap O F : (a : O) → F) y : F) (0 : F)
grw :
  LE.le.{v} (α := Γ₀)
    ((v : (a : F) → Γ₀)
        (HMul.hMul (α := F) (β := F) (((algebraMap O F : (a : O) → F) y)⁻¹ : F)
          ((algebraMap O F : (a : O) → F) x : F)) :
      Γ₀)
    ((v : (a : F) → Γ₀) 1 : Γ₀)
⊢ LE.le.{v} (α := Γ₀)
    ((v : (a : F) → Γ₀)
        (HMul.hMul (α := F) (β := F) (((algebraMap O F : (a : O) → F) y)⁻¹ : F)
          ((algebraMap O F : (a : O) → F) x : F)) :
      Γ₀)
    (1 : Γ₀)
have grw₁ : LE.le.{v} (α := Γ₀)
  ((v : (a : F) → Γ₀)
      (HMul.hMul (α := F) (β := F) (((algebraMap O F : (a : O) → F) y)⁻¹ : F) ((algebraMap O F : (a : O) → F) x : F)) :
    Γ₀)
  ((v : (a : F) → Γ₀)
      (HMul.hMul (α := F) (β := F) (((algebraMap O F : (a : O) → F) y)⁻¹ : F) ((algebraMap O F : (a : O) → F) y : F)) :
    Γ₀)
Tactic: grw [← v.map_one, ← inv_mul_cancel₀ hy, v.map_mul, v.map_mul, h]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
F : Type u
Γ₀ : Type v
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O F
hv : v.Integers O
x y : O
h :
  LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀)
    ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) y : F) : Γ₀)
hy : Ne.{u + 1} (α := F) ((algebraMap O F : (a : O) → F) y : F) (0 : F)
grw :
  LE.le.{v} (α := Γ₀)
    ((v : (a : F) → Γ₀)
        (HMul.hMul (α := F) (β := F) (((algebraMap O F : (a : O) → F) y)⁻¹ : F)
          ((algebraMap O F : (a : O) → F) x : F)) :
      Γ₀)
    ((v : (a : F) → Γ₀) 1 : Γ₀)
grw₁ :
  LE.le.{v} (α := Γ₀)
    ((v : (a : F) → Γ₀)
        (HMul.hMul (α := F) (β := F) (((algebraMap O F : (a : O) → F) y)⁻¹ : F)
          ((algebraMap O F : (a : O) → F) x : F)) :
      Γ₀)
    ((v : (a : F) → Γ₀)
        (HMul.hMul (α := F) (β := F) (((algebraMap O F : (a : O) → F) y)⁻¹ : F)
          ((algebraMap O F : (a : O) → F) y : F)) :
      Γ₀)
⊢ LE.le.{v} (α := Γ₀)
    ((v : (a : F) → Γ₀)
        (HMul.hMul (α := F) (β := F) (((algebraMap O F : (a : O) → F) y)⁻¹ : F)
          ((algebraMap O F : (a : O) → F) x : F)) :
      Γ₀)
    (1 : Γ₀)
have grw₂ : HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : F) → Γ₀) (((algebraMap O F : (a : O) → F) y)⁻¹ : F) : Γ₀)
    ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀) ≤
  (v : (a : F) → Γ₀)
    (HMul.hMul (α := F) (β := F) (((algebraMap O F : (a : O) → F) y)⁻¹ : F) ((algebraMap O F : (a : O) → F) y : F))
Tactic: grw [← v.map_one, ← inv_mul_cancel₀ hy, v.map_mul, v.map_mul, h]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
F : Type u
Γ₀ : Type v
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O F
hv : v.Integers O
x y : O
h :
  LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀)
    ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) y : F) : Γ₀)
hy : Ne.{u + 1} (α := F) ((algebraMap O F : (a : O) → F) y : F) (0 : F)
grw :
  LE.le.{v} (α := Γ₀)
    ((v : (a : F) → Γ₀)
        (HMul.hMul (α := F) (β := F) (((algebraMap O F : (a : O) → F) y)⁻¹ : F)
          ((algebraMap O F : (a : O) → F) x : F)) :
      Γ₀)
    ((v : (a : F) → Γ₀) 1 : Γ₀)
grw₁ :
  LE.le.{v} (α := Γ₀)
    ((v : (a : F) → Γ₀)
        (HMul.hMul (α := F) (β := F) (((algebraMap O F : (a : O) → F) y)⁻¹ : F)
          ((algebraMap O F : (a : O) → F) x : F)) :
      Γ₀)
    ((v : (a : F) → Γ₀)
        (HMul.hMul (α := F) (β := F) (((algebraMap O F : (a : O) → F) y)⁻¹ : F)
          ((algebraMap O F : (a : O) → F) y : F)) :
      Γ₀)
grw₂ :
  HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : F) → Γ₀) (((algebraMap O F : (a : O) → F) y)⁻¹ : F) : Γ₀)
      ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀) ≤
    (v : (a : F) → Γ₀)
      (HMul.hMul (α := F) (β := F) (((algebraMap O F : (a : O) → F) y)⁻¹ : F) ((algebraMap O F : (a : O) → F) y : F))
⊢ LE.le.{v} (α := Γ₀)
    ((v : (a : F) → Γ₀)
        (HMul.hMul (α := F) (β := F) (((algebraMap O F : (a : O) → F) y)⁻¹ : F)
          ((algebraMap O F : (a : O) → F) x : F)) :
      Γ₀)
    (1 : Γ₀)
have grw₃ : HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : F) → Γ₀) (((algebraMap O F : (a : O) → F) y)⁻¹ : F) : Γ₀)
    ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀) ≤
  HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : F) → Γ₀) (((algebraMap O F : (a : O) → F) y)⁻¹ : F) : Γ₀)
    ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) y : F) : Γ₀)
Tactic: grw [← v.map_one, ← inv_mul_cancel₀ hy, v.map_mul, v.map_mul, h]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
F : Type u
Γ₀ : Type v
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O F
hv : v.Integers O
x y : O
h :
  LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀)
    ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) y : F) : Γ₀)
hy : Ne.{u + 1} (α := F) ((algebraMap O F : (a : O) → F) y : F) (0 : F)
grw :
  LE.le.{v} (α := Γ₀)
    ((v : (a : F) → Γ₀)
        (HMul.hMul (α := F) (β := F) (((algebraMap O F : (a : O) → F) y)⁻¹ : F)
          ((algebraMap O F : (a : O) → F) x : F)) :
      Γ₀)
    ((v : (a : F) → Γ₀) 1 : Γ₀)
grw₁ :
  LE.le.{v} (α := Γ₀)
    ((v : (a : F) → Γ₀)
        (HMul.hMul (α := F) (β := F) (((algebraMap O F : (a : O) → F) y)⁻¹ : F)
          ((algebraMap O F : (a : O) → F) x : F)) :
      Γ₀)
    ((v : (a : F) → Γ₀)
        (HMul.hMul (α := F) (β := F) (((algebraMap O F : (a : O) → F) y)⁻¹ : F)
          ((algebraMap O F : (a : O) → F) y : F)) :
      Γ₀)
grw₂ :
  HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : F) → Γ₀) (((algebraMap O F : (a : O) → F) y)⁻¹ : F) : Γ₀)
      ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀) ≤
    (v : (a : F) → Γ₀)
      (HMul.hMul (α := F) (β := F) (((algebraMap O F : (a : O) → F) y)⁻¹ : F) ((algebraMap O F : (a : O) → F) y : F))
grw₃ :
  HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : F) → Γ₀) (((algebraMap O F : (a : O) → F) y)⁻¹ : F) : Γ₀)
      ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀) ≤
    HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : F) → Γ₀) (((algebraMap O F : (a : O) → F) y)⁻¹ : F) : Γ₀)
      ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) y : F) : Γ₀)
⊢ LE.le.{v} (α := Γ₀)
    ((v : (a : F) → Γ₀)
        (HMul.hMul (α := F) (β := F) (((algebraMap O F : (a : O) → F) y)⁻¹ : F)
          ((algebraMap O F : (a : O) → F) x : F)) :
      Γ₀)
    (1 : Γ₀)
have grw₄ : HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : F) → Γ₀) (((algebraMap O F : (a : O) → F) y)⁻¹ : F) : Γ₀)
    ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) y : F) : Γ₀) ≤
  HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : F) → Γ₀) (((algebraMap O F : (a : O) → F) y)⁻¹ : F) : Γ₀)
    ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) y : F) : Γ₀)
Tactic: grw [← v.map_one, ← inv_mul_cancel₀ hy, v.map_mul, v.map_mul, h]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
F : Type u
Γ₀ : Type v
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O F
hv : v.Integers O
x : O
hvx : Eq.{v + 1} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀) (1 : Γ₀)
⊢ IsUnit x
have refine : Ne.{u + 1} (α := F) ((algebraMap O F : (a : O) → F) x : F) (0 : F)
Tactic: refine isUnit_of_one hv (IsUnit.mk0 _ ?_) hvx
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
F : Type u
Γ₀ : Type v
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O F
hv : v.Integers O
x : O
⊢ LT.lt.{v} (α := Γ₀) (0 : Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀) ↔ x ≠ 0
have rw : ¬LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀) (0 : Γ₀) ↔ x ≠ 0
Tactic: rw [← not_le]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
F : Type u
Γ₀ : Type v
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O F
hv : v.Integers O
x : O
⊢ ¬LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀) (0 : Γ₀) ↔ x ≠ 0
have refine : LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀) (0 : Γ₀) ↔ x = 0
Tactic: refine not_congr ?_
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
F : Type u
Γ₀ : Type v
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O F
hv : v.Integers O
x y : O
⊢ DvdNotUnit x y ↔
    LT.lt.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) y : F) : Γ₀)
      ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀)
have rw : DvdNotUnit x y ↔ x ∣ y ∧ ¬y ∣ x
Tactic: rw [lt_iff_le_not_ge, hv.le_iff_dvd, hv.le_iff_dvd]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
F : Type u
Γ₀ : Type v
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O F
hv : v.Integers O
x y : O
⊢ DvdNotUnit x y ↔ x ∣ y ∧ ¬y ∣ x
have refine : DvdNotUnit x y → x ∣ y ∧ ¬y ∣ x
Tactic: refine ⟨?_, And.elim dvdNotUnit_of_dvd_of_not_dvd⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
F : Type u
Γ₀ : Type v
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O F
hv : v.Integers O
x : O
hx0 : x ≠ 0
d : O
hdu : ¬IsUnit d
⊢ x ∣ x * d ∧ ¬x * d ∣ x
have refine : ¬x * d ∣ x
Tactic: refine ⟨⟨d, rfl⟩, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (hypothesis)
Goal:
F : Type u
Γ₀ : Type v
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O F
hv : v.Integers O
x : O
hx0 : x ≠ 0
d : O
hdu : ¬IsUnit d
⊢ ¬x * d ∣ x
have hdu₁ : LT.lt.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) d : F) : Γ₀) (1 : Γ₀)
Tactic: rw [hv.isUnit_iff_valuation_eq_one, ← ne_eq, ne_iff_lt_iff_le.mpr (hv.map_le_one d)] at hdu
Cleared hypotheses: hdu
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
F : Type u
Γ₀ : Type v
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O F
hv : v.Integers O
x : O
hx0 : x ≠ 0
d : O
hdu : LT.lt.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) d : F) : Γ₀) (1 : Γ₀)
⊢ ¬x * d ∣ x
have rw : ¬LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀)
    ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) (x * d) : F) : Γ₀)
Tactic: rw [dvd_iff_le hv]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
F : Type u
Γ₀ : Type v
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O F
hv : v.Integers O
x : O
hx0 : x ≠ 0
d : O
hdu : LT.lt.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) d : F) : Γ₀) (1 : Γ₀)
⊢ ¬LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀)
      ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) (x * d) : F) : Γ₀)
have simp : HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀)
    ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) d : F) : Γ₀) <
  (v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F)
Tactic: simp only [map_mul, not_le]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
F : Type u
Γ₀ : Type v
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O F
hv : v.Integers O
x : O
hx0 : x ≠ 0
d : O
hdu : LT.lt.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) d : F) : Γ₀) (1 : Γ₀)
⊢ HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀)
      ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) d : F) : Γ₀) <
    (v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F)
have contrapose! : ∀
  (hdu :
    (v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) ≤
      HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀)
        ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) d : F) : Γ₀)),
  LE.le.{v} (α := Γ₀) (1 : Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) d : F) : Γ₀)
Tactic: contrapose! hdu
Cleared hypotheses: hdu
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
F : Type u
Γ₀ : Type v
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O F
hv : v.Integers O
x : O
hx0 : x ≠ 0
d : O
hdu :
  (v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) ≤
    HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀)
      ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) d : F) : Γ₀)
⊢ LE.le.{v} (α := Γ₀) (1 : Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) d : F) : Γ₀)
have refine : LT.lt.{v} (α := Γ₀) (0 : Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀)
Tactic: refine one_le_of_le_mul_left₀ ?_ hdu
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
F : Type u
Γ₀ : Type v
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O F
hv : v.Integers O
x : F
⊢ ∃ (a : O), x = (algebraMap O F : (a : O) → F) a ∨ x⁻¹ = (algebraMap O F : (a : O) → F) a
have inl : ∀ (h : LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) x : Γ₀) (1 : Γ₀)),
  ∃ (a : O), x = (algebraMap O F : (a : O) → F) a ∨ x⁻¹ = (algebraMap O F : (a : O) → F) a
Tactic: rcases val_le_one_or_val_inv_le_one v x with h | h
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
F : Type u
Γ₀ : Type v
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O F
hv : v.Integers O
x : F
inl :
  ∀ (h : LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) x : Γ₀) (1 : Γ₀)),
    ∃ (a : O), x = (algebraMap O F : (a : O) → F) a ∨ x⁻¹ = (algebraMap O F : (a : O) → F) a
⊢ ∃ (a : O), x = (algebraMap O F : (a : O) → F) a ∨ x⁻¹ = (algebraMap O F : (a : O) → F) a
have inr : ∀ (h : LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) x⁻¹ : Γ₀) (1 : Γ₀)),
  ∃ (a : O), x = (algebraMap O F : (a : O) → F) a ∨ x⁻¹ = (algebraMap O F : (a : O) → F) a
Tactic: rcases val_le_one_or_val_inv_le_one v x with h | h
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
F : Type u
Γ₀ : Type v
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O F
hv : v.Integers O
x : F
h : LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ ∃ (a : O), x = (algebraMap O F : (a : O) → F) a ∨ x⁻¹ = (algebraMap O F : (a : O) → F) a
have inl : ∀ (a : O) (ha : (algebraMap O F : (a : O) → F) a = x),
  ∃ (a : O), x = (algebraMap O F : (a : O) → F) a ∨ x⁻¹ = (algebraMap O F : (a : O) → F) a
Tactic: obtain ⟨a, ha⟩ := exists_of_le_one hv h
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
F : Type u
Γ₀ : Type v
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O F
hv : v.Integers O
x : F
h : LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) x⁻¹ : Γ₀) (1 : Γ₀)
⊢ ∃ (a : O), x = (algebraMap O F : (a : O) → F) a ∨ x⁻¹ = (algebraMap O F : (a : O) → F) a
have inr : ∀ (a : O) (ha : (algebraMap O F : (a : O) → F) a = x⁻¹),
  ∃ (a : O), x = (algebraMap O F : (a : O) → F) a ∨ x⁻¹ = (algebraMap O F : (a : O) → F) a
Tactic: obtain ⟨a, ha⟩ := exists_of_le_one hv h
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
F : Type u
Γ₀ : Type v
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O F
hv : v.Integers O
x : O
⊢ (↑(Ideal.span {x}) : Set O) =
    {y : O |
      LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) y : F) : Γ₀)
        ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀)}
have inl : (↑(Ideal.span {0}) : Set O) =
  {y : O |
    LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) y : F) : Γ₀)
      ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) 0 : F) : Γ₀)}
Tactic: rcases eq_or_ne x 0 with rfl | hx
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
F : Type u
Γ₀ : Type v
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O F
hv : v.Integers O
x : O
inl :
  (↑(Ideal.span {0}) : Set O) =
    {y : O |
      LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) y : F) : Γ₀)
        ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) 0 : F) : Γ₀)}
⊢ (↑(Ideal.span {x}) : Set O) =
    {y : O |
      LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) y : F) : Γ₀)
        ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀)}
have inr : ∀ (hx : x ≠ 0),
  (↑(Ideal.span {x}) : Set O) =
    {y : O |
      LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) y : F) : Γ₀)
        ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀)}
Tactic: rcases eq_or_ne x 0 with rfl | hx
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
F : Type u
Γ₀ : Type v
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O F
hv : v.Integers O
x : O
hx : x ≠ 0
⊢ (↑(Ideal.span {x}) : Set O) =
    {y : O |
      LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) y : F) : Γ₀)
        ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀)}
have inr : ∀ (x_1 : O),
  x_1 ∈ (↑(Ideal.span {x}) : Set O) ↔
    Membership.mem (γ := Set O)
      {y : O |
        LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) y : F) : Γ₀)
          ((v : (a : F) → Γ₀) ((algebraMap O F : (a : O) → F) x : F) : Γ₀)}
      x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
F : Type u
Γ₀ : Type v
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O F
hv : v.Integers O
inst_4 : Subsingleton.{v + 1} (↥(MonoidHom.mrange v))ˣ
⊢ Function.Bijective.{w + 1, u + 1} (α := O) (β := F) (⇑(algebraMap O F) : (a : O) → F)
have refine : ∀ (x : F), LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) x : Γ₀) (1 : Γ₀)
Tactic: refine ⟨hv.hom_inj, fun x ↦ hv.exists_of_le_one ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
F : Type u
Γ₀ : Type v
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O F
hv : v.Integers O
inst_4 : Subsingleton.{v + 1} (↥(MonoidHom.mrange v))ˣ
x : F
⊢ LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) x : Γ₀) (1 : Γ₀)
have inl : LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) 0 : Γ₀) (1 : Γ₀)
Tactic: rcases eq_or_ne x 0 with rfl | hx
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
F : Type u
Γ₀ : Type v
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O F
hv : v.Integers O
inst_4 : Subsingleton.{v + 1} (↥(MonoidHom.mrange v))ˣ
x : F
inl : LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) 0 : Γ₀) (1 : Γ₀)
⊢ LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) x : Γ₀) (1 : Γ₀)
have inr : ∀ (hx : x ≠ 0), LE.le.{v} (α := Γ₀) ((v : (a : F) → Γ₀) x : Γ₀) (1 : Γ₀)
Tactic: rcases eq_or_ne x 0 with rfl | hx
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
F : Type u
Γ₀ : Type v
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O F
hv : v.Integers O
I : Ideal O
⊢ Submodule.IsPrincipal I ↔
    ∃ (x : Γ₀),
      IsGreatest
        (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) ''
          (↑I : Set O))
        x
have mp : Submodule.IsPrincipal I →
  ∃ (x : Γ₀),
    IsGreatest
      (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) ''
        (↑I : Set O))
      x
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.Integers (goal)
Goal:
F : Type u
Γ₀ : Type v
inst : Field F
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst_2 : CommRing O
inst_3 : Algebra O F
hv : v.Integers O
I : Ideal O
mp :
  Submodule.IsPrincipal I →
    ∃ (x : Γ₀),
      IsGreatest
        (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) ''
          (↑I : Set O))
        x
⊢ Submodule.IsPrincipal I ↔
    ∃ (x : Γ₀),
      IsGreatest
        (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) ''
          (↑I : Set O))
        x
have mpr : (∃ (x : Γ₀),
    IsGreatest
      (Function.comp.{w + 1, u + 1, v + 1} (β := F) (⇑v : (a : F) → Γ₀) (⇑(algebraMap O F) : (a : O) → F) ''
        (↑I : Set O))
      x) →
  Submodule.IsPrincipal I
Tactic: constructor