awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_2
Γ : Type u_3
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst_3 : v.Compatible
a : R
r : ↥(posSubmonoid R)
b : R
s : ↥(posSubmonoid R)
h :
  HMul.hMul (α := ValueGroupWithZero R) (β := ValueGroupWithZero R)
      ((valuation R : (a : R) → ValueGroupWithZero R) a : ValueGroupWithZero R)
      ((valuation R : (a : R) → ValueGroupWithZero R) (↑s : R) : ValueGroupWithZero R) <
    HMul.hMul (α := ValueGroupWithZero R) (β := ValueGroupWithZero R)
      ((valuation R : (a : R) → ValueGroupWithZero R) b : ValueGroupWithZero R)
      ((valuation R : (a : R) → ValueGroupWithZero R) (↑r : R) : ValueGroupWithZero R)
⊢ LT.lt (α := Γ) (0 : Γ)
    ((embedding : (a : ValueGroup₀ v.toMonoidWithZeroHom) → Γ)
        (((embed v : MonoidWithZeroHom.{u_2, u_3} (ValueGroupWithZero R) (ValueGroup₀ v)) :
              (a : ValueGroupWithZero R) → ValueGroup₀ v)
            ((valuation R : (a : R) → ValueGroupWithZero R) (↑s : R)) :
          ValueGroup₀ v) :
      Γ)
have hd : ¬Eq (α := Γ)
    ((embedding : (a : ValueGroup₀ v.toMonoidWithZeroHom) → Γ)
        (((embed v : MonoidWithZeroHom.{u_2, u_3} (ValueGroupWithZero R) (ValueGroup₀ v)) :
              (a : ValueGroupWithZero R) → ValueGroup₀ v)
            ((valuation R : (a : R) → ValueGroupWithZero R) (↑s : R)) :
          ValueGroup₀ v) :
      Γ)
    (0 : Γ)
Tactic: simp only [zero_lt_iff, ne_eq, Valuation.apply_posSubmonoid_ne_zero, not_false_eq_true]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (hypothesis)
Goal:
R : Type u_2
Γ : Type u_3
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst_3 : v.Compatible
a : R
r : ↥(posSubmonoid R)
b : R
s : ↥(posSubmonoid R)
h :
  HMul.hMul (α := ValueGroupWithZero R) (β := ValueGroupWithZero R)
      ((valuation R : (a : R) → ValueGroupWithZero R) a : ValueGroupWithZero R)
      ((valuation R : (a : R) → ValueGroupWithZero R) (↑s : R) : ValueGroupWithZero R) <
    HMul.hMul (α := ValueGroupWithZero R) (β := ValueGroupWithZero R)
      ((valuation R : (a : R) → ValueGroupWithZero R) b : ValueGroupWithZero R)
      ((valuation R : (a : R) → ValueGroupWithZero R) (↑r : R) : ValueGroupWithZero R)
⊢ HMul.hMul (α := Γ) (β := Γ)
      ((embedding : (a : ValueGroup₀ v.toMonoidWithZeroHom) → Γ)
          (((embed v : MonoidWithZeroHom.{u_2, u_3} (ValueGroupWithZero R) (ValueGroup₀ v)) :
                (a : ValueGroupWithZero R) → ValueGroup₀ v)
              ((valuation R : (a : R) → ValueGroupWithZero R) a) :
            ValueGroup₀ v) :
        Γ)
      ((embedding : (a : ValueGroup₀ v.toMonoidWithZeroHom) → Γ)
          (((embed v : MonoidWithZeroHom.{u_2, u_3} (ValueGroupWithZero R) (ValueGroup₀ v)) :
                (a : ValueGroupWithZero R) → ValueGroup₀ v)
              ((valuation R : (a : R) → ValueGroupWithZero R) (↑s : R)) :
            ValueGroup₀ v) :
        Γ) <
    HMul.hMul (α := Γ) (β := Γ)
      ((embedding : (a : ValueGroup₀ v.toMonoidWithZeroHom) → Γ)
          (((embed v : MonoidWithZeroHom.{u_2, u_3} (ValueGroupWithZero R) (ValueGroup₀ v)) :
                (a : ValueGroupWithZero R) → ValueGroup₀ v)
              ((valuation R : (a : R) → ValueGroupWithZero R) b) :
            ValueGroup₀ v) :
        Γ)
      ((embedding : (a : ValueGroup₀ v.toMonoidWithZeroHom) → Γ)
          (((embed v : MonoidWithZeroHom.{u_2, u_3} (ValueGroupWithZero R) (ValueGroup₀ v)) :
                (a : ValueGroupWithZero R) → ValueGroup₀ v)
              ((valuation R : (a : R) → ValueGroupWithZero R) (↑r : R)) :
            ValueGroup₀ v) :
        Γ)
have h₁ : LT.lt.{u_3} (α := Γ) ((v : (a : R) → Γ) (a * (↑s : R)) : Γ) ((v : (a : R) → Γ) (b * (↑r : R)) : Γ)
Tactic: rw [← map_mul, ← map_mul, (isEquiv (valuation R) v).lt_iff_lt] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_2
Γ : Type u_3
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst_3 : v.Compatible
a : R
r : ↥(posSubmonoid R)
b : R
s : ↥(posSubmonoid R)
h : LT.lt.{u_3} (α := Γ) ((v : (a : R) → Γ) (a * (↑s : R)) : Γ) ((v : (a : R) → Γ) (b * (↑r : R)) : Γ)
⊢ HMul.hMul (α := Γ) (β := Γ)
      ((embedding : (a : ValueGroup₀ v.toMonoidWithZeroHom) → Γ)
          (((embed v : MonoidWithZeroHom.{u_2, u_3} (ValueGroupWithZero R) (ValueGroup₀ v)) :
                (a : ValueGroupWithZero R) → ValueGroup₀ v)
              ((valuation R : (a : R) → ValueGroupWithZero R) a) :
            ValueGroup₀ v) :
        Γ)
      ((embedding : (a : ValueGroup₀ v.toMonoidWithZeroHom) → Γ)
          (((embed v : MonoidWithZeroHom.{u_2, u_3} (ValueGroupWithZero R) (ValueGroup₀ v)) :
                (a : ValueGroupWithZero R) → ValueGroup₀ v)
              ((valuation R : (a : R) → ValueGroupWithZero R) (↑s : R)) :
            ValueGroup₀ v) :
        Γ) <
    HMul.hMul (α := Γ) (β := Γ)
      ((embedding : (a : ValueGroup₀ v.toMonoidWithZeroHom) → Γ)
          (((embed v : MonoidWithZeroHom.{u_2, u_3} (ValueGroupWithZero R) (ValueGroup₀ v)) :
                (a : ValueGroupWithZero R) → ValueGroup₀ v)
              ((valuation R : (a : R) → ValueGroupWithZero R) b) :
            ValueGroup₀ v) :
        Γ)
      ((embedding : (a : ValueGroup₀ v.toMonoidWithZeroHom) → Γ)
          (((embed v : MonoidWithZeroHom.{u_2, u_3} (ValueGroupWithZero R) (ValueGroup₀ v)) :
                (a : ValueGroupWithZero R) → ValueGroup₀ v)
              ((valuation R : (a : R) → ValueGroupWithZero R) (↑r : R)) :
            ValueGroup₀ v) :
        Γ)
have simp : HMul.hMul (α := Γ) (β := Γ)
    ((embedding : (a : ValueGroup₀ v.toMonoidWithZeroHom) → Γ)
        (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) a : ValueGroup₀ v) :
      Γ)
    ((embedding : (a : ValueGroup₀ v.toMonoidWithZeroHom) → Γ)
        (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) (↑s : R) :
          ValueGroup₀ v) :
      Γ) <
  HMul.hMul (α := Γ) (β := Γ)
    ((embedding : (a : ValueGroup₀ v.toMonoidWithZeroHom) → Γ)
        (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) b : ValueGroup₀ v) :
      Γ)
    ((embedding : (a : ValueGroup₀ v.toMonoidWithZeroHom) → Γ)
        (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) (↑r : R) :
          ValueGroup₀ v) :
      Γ)
Tactic: simp only [embed, coe_mk, ZeroHom.coe_mk, lift_valuation,
      OneMemClass.coe_one, map_one, div_one]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_2
Γ : Type u_3
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst_3 : v.Compatible
a : R
r : ↥(posSubmonoid R)
b : R
s : ↥(posSubmonoid R)
h : LT.lt.{u_3} (α := Γ) ((v : (a : R) → Γ) (a * (↑s : R)) : Γ) ((v : (a : R) → Γ) (b * (↑r : R)) : Γ)
⊢ HMul.hMul (α := Γ) (β := Γ)
      ((embedding : (a : ValueGroup₀ v.toMonoidWithZeroHom) → Γ)
          (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) a :
            ValueGroup₀ v) :
        Γ)
      ((embedding : (a : ValueGroup₀ v.toMonoidWithZeroHom) → Γ)
          (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) (↑s : R) :
            ValueGroup₀ v) :
        Γ) <
    HMul.hMul (α := Γ) (β := Γ)
      ((embedding : (a : ValueGroup₀ v.toMonoidWithZeroHom) → Γ)
          (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) b :
            ValueGroup₀ v) :
        Γ)
      ((embedding : (a : ValueGroup₀ v.toMonoidWithZeroHom) → Γ)
          (((restrict₀ v : MonoidWithZeroHom.{u_2, u_3} R (ValueGroup₀ v)) : (a : R) → ValueGroup₀ v) (↑r : R) :
            ValueGroup₀ v) :
        Γ)
have erw : HMul.hMul (α := Γ) (β := Γ) ((v.toMonoidWithZeroHom : (a : R) → Γ) a : Γ)
    ((v.toMonoidWithZeroHom : (a : R) → Γ) (↑s : R) : Γ) <
  HMul.hMul (α := Γ) (β := Γ) ((v.toMonoidWithZeroHom : (a : R) → Γ) b : Γ)
    ((v.toMonoidWithZeroHom : (a : R) → Γ) (↑r : R) : Γ)
Tactic: erw [embedding_restrict₀ a, embedding_restrict₀ b, embedding_restrict₀ r.1,
      embedding_restrict₀ s.1]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_2
Γ : Type u_3
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst_3 : v.Compatible
Γ' : Type u_4
inst_4 : LinearOrderedCommGroupWithZero Γ'
w : Valuation R Γ'
inst_5 : w.Compatible
x : ValueGroupWithZero R
h : w.IsEquiv v
⊢ Eq.{u_3 + 1} (α := ValueGroup₀ v)
    ((h.orderMonoidIso : (a : ValueGroup₀ w) → ValueGroup₀ v)
        (((embed w : MonoidWithZeroHom.{u_2, u_4} (ValueGroupWithZero R) (ValueGroup₀ w)) :
            (a : ValueGroupWithZero R) → ValueGroup₀ w)
          x) :
      ValueGroup₀ v)
    (((embed v : MonoidWithZeroHom.{u_2, u_3} (ValueGroupWithZero R) (ValueGroup₀ v)) :
          (a : ValueGroupWithZero R) → ValueGroup₀ v)
        x :
      ValueGroup₀ v)
have simp : (h.orderMonoidIso : (a : ValueGroup₀ w) → ValueGroup₀ v)
    (ValueGroupWithZero.lift
      (fun (r : R) (s : ↥(posSubmonoid R)) ↦
        HDiv.hDiv (α := ValueGroup₀ w) (β := ValueGroup₀ w)
          ((w.restrict : (a : R) → ValueGroup₀ (↑w : R →*₀ Γ')) r : ValueGroup₀ (F := R →*₀ Γ') (↑w : R →*₀ Γ'))
          ((w.restrict : (a : R) → ValueGroup₀ (↑w : R →*₀ Γ')) (↑s : R) : ValueGroup₀ (F := R →*₀ Γ') (↑w : R →*₀ Γ')))
      sorry x) =
  ValueGroupWithZero.lift
    (fun (r : R) (s : ↥(posSubmonoid R)) ↦
      HDiv.hDiv (α := ValueGroup₀ v) (β := ValueGroup₀ v)
        ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ)) r : ValueGroup₀ (F := R →*₀ Γ) (↑v : R →*₀ Γ))
        ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ)) (↑s : R) : ValueGroup₀ (F := R →*₀ Γ) (↑v : R →*₀ Γ)))
    sorry x
Tactic: simp only [embed, ← Valuation.restrict_def, coe_mk, ZeroHom.coe_mk]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_2
Γ : Type u_3
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst_3 : v.Compatible
Γ' : Type u_4
inst_4 : LinearOrderedCommGroupWithZero Γ'
w : Valuation R Γ'
inst_5 : w.Compatible
x : ValueGroupWithZero R
h : w.IsEquiv v
⊢ (h.orderMonoidIso : (a : ValueGroup₀ w) → ValueGroup₀ v)
      (ValueGroupWithZero.lift
        (fun (r : R) (s : ↥(posSubmonoid R)) ↦
          HDiv.hDiv (α := ValueGroup₀ w) (β := ValueGroup₀ w)
            ((w.restrict : (a : R) → ValueGroup₀ (↑w : R →*₀ Γ')) r : ValueGroup₀ (F := R →*₀ Γ') (↑w : R →*₀ Γ'))
            ((w.restrict : (a : R) → ValueGroup₀ (↑w : R →*₀ Γ')) (↑s : R) :
              ValueGroup₀ (F := R →*₀ Γ') (↑w : R →*₀ Γ')))
        ⋯ x) =
    ValueGroupWithZero.lift
      (fun (r : R) (s : ↥(posSubmonoid R)) ↦
        HDiv.hDiv (α := ValueGroup₀ v) (β := ValueGroup₀ v)
          ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ)) r : ValueGroup₀ (F := R →*₀ Γ) (↑v : R →*₀ Γ))
          ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ)) (↑s : R) : ValueGroup₀ (F := R →*₀ Γ) (↑v : R →*₀ Γ)))
      ⋯ x
have mk : ∀ (r : R) (s : ↥(posSubmonoid R)),
  (h.orderMonoidIso : (a : ValueGroup₀ w) → ValueGroup₀ v)
      (ValueGroupWithZero.lift
        (fun (r : R) (s : ↥(posSubmonoid R)) ↦
          HDiv.hDiv (α := ValueGroup₀ w) (β := ValueGroup₀ w)
            ((w.restrict : (a : R) → ValueGroup₀ (↑w : R →*₀ Γ')) r : ValueGroup₀ (F := R →*₀ Γ') (↑w : R →*₀ Γ'))
            ((w.restrict : (a : R) → ValueGroup₀ (↑w : R →*₀ Γ')) (↑s : R) :
              ValueGroup₀ (F := R →*₀ Γ') (↑w : R →*₀ Γ')))
        sorry (ValueGroupWithZero.mk r s)) =
    ValueGroupWithZero.lift
      (fun (r : R) (s : ↥(posSubmonoid R)) ↦
        HDiv.hDiv (α := ValueGroup₀ v) (β := ValueGroup₀ v)
          ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ)) r : ValueGroup₀ (F := R →*₀ Γ) (↑v : R →*₀ Γ))
          ((v.restrict : (a : R) → ValueGroup₀ (↑v : R →*₀ Γ)) (↑s : R) : ValueGroup₀ (F := R →*₀ Γ) (↑v : R →*₀ Γ)))
      sorry (ValueGroupWithZero.mk r s)
Tactic: induction x using ValueGroupWithZero.ind with
| mk r s =>
  simp
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R_1 : Type u_1
inst : CommRing R_1
inst_1 : ValuativeRel R_1
R : Type u_2
Γ : Type u_3
inst_2 : CommRing R
inst_3 : ValuativeRel R
inst_4 : LinearOrderedCommGroupWithZero Γ
v : Valuation R Γ
inst_5 : v.Compatible
⊢ Function.Injective.{u_3 + 1, u_2 + 1} (β := ValueGroupWithZero R) fun (x : ValueGroup₀ v) ↦
    (embedding : (a : ValueGroup₀ (valuation R)) → ValueGroupWithZero R)
      (((Valuation.IsEquiv.orderMonoidIso ⋯ :
            OrderMonoidIso.{u_3, u_2} (ValueGroup₀ v)
              (ValueGroup₀ (F := Valuation R (ValueGroupWithZero R)) (valuation R))) :
          (a : ValueGroup₀ v) → ValueGroup₀ (valuation R))
        x)
have rw : Function.Injective (α := ValueGroup₀ (F := Valuation R (ValueGroupWithZero R)) (valuation R)) (β :=
  ValueGroupWithZero R) (⇑embedding : (a : ValueGroup₀ (valuation R)) → ValueGroupWithZero R)
Tactic: rw [← Function.comp_def, EquivLike.injective_comp]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : ValuativeRel A
inst_3 : ValuativeRel B
inst_4 : Algebra A B
inst_5 : ValuativeExtension A B
a b : A
⊢ vlt.{u_2} (R := B) ((algebraMap A B : (a : A) → B) a : B) ((algebraMap A B : (a : A) → B) b : B) ↔ a <ᵥ b
have rw : ¬@vle.{u_2} B inst_1 _ ((algebraMap A B : (a : A) → B) b : B) ((algebraMap A B : (a : A) → B) a : B) ↔ a <ᵥ b
Tactic: rw [← not_vle, vle_iff_vle, not_vle]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : ValuativeRel A
inst_3 : ValuativeRel B
inst_4 : Algebra A B
inst_5 : ValuativeExtension A B
a b : A
rw : ¬@vle.{u_2} B inst_1 _ ((algebraMap A B : (a : A) → B) b : B) ((algebraMap A B : (a : A) → B) a : B) ↔ a <ᵥ b
⊢ vlt.{u_2} (R := B) ((algebraMap A B : (a : A) → B) a : B) ((algebraMap A B : (a : A) → B) b : B) ↔ a <ᵥ b
have rw₁ : ¬@vle _ inst _ b a ↔ a <ᵥ b
Tactic: rw [← not_vle, vle_iff_vle, not_vle]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : ValuativeRel A
inst_3 : ValuativeRel B
inst_4 : Algebra A B
inst_5 : ValuativeExtension A B
a b : A
rw : ¬@vle.{u_2} B inst_1 _ ((algebraMap A B : (a : A) → B) b : B) ((algebraMap A B : (a : A) → B) a : B) ↔ a <ᵥ b
rw₁ : ¬@vle _ inst _ b a ↔ a <ᵥ b
⊢ vlt.{u_2} (R := B) ((algebraMap A B : (a : A) → B) a : B) ((algebraMap A B : (a : A) → B) b : B) ↔ a <ᵥ b
have rw₂ : a <ᵥ b ↔ a <ᵥ b
Tactic: rw [← not_vle, vle_iff_vle, not_vle]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : ValuativeRel A
inst_3 : ValuativeRel B
inst_4 : Algebra A B
inst_5 : ValuativeExtension A B
Γ : Type u_3
inst_6 : LinearOrderedCommMonoidWithZero Γ
w : Valuation B Γ
inst_7 : w.Compatible
⊢ Valuation.Compatible.{u_1, u_3} (R := A) (Valuation.comap (algebraMap A B) w)
have vle_iff_le : ∀ (x y : A),
  @vle _ inst _ x y ↔
    LE.le.{u_3} (α := Γ) ((Valuation.comap (algebraMap A B) w : (a : A) → Γ) x : Γ)
      ((Valuation.comap (algebraMap A B) w : (a : A) → Γ) y : Γ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : ValuativeRel A
inst_3 : ValuativeRel B
inst_4 : Algebra A B
inst_5 : ValuativeExtension A B
inst_6 : IsRankLeOne B
⊢ IsRankLeOne A
have obtain : ∀ (f : ValueGroupWithZero B →*₀ NNReal)
  (hf : StrictMono (α := ValueGroupWithZero B) (β := NNReal) (⇑f : (a : ValueGroupWithZero B) → NNReal)), IsRankLeOne A
Tactic: obtain ⟨⟨f, hf⟩⟩ := IsRankLeOne.nonempty (R := B)
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Basic (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : ValuativeRel R
inst_2 : IsRankLeOne R
⊢ MulArchimedean.{u_1} (ValueGroupWithZero R)
have obtain : ∀ (f : ValueGroupWithZero R →*₀ NNReal)
  (hf : StrictMono (α := ValueGroupWithZero R) (β := NNReal) (⇑f : (a : ValueGroupWithZero R) → NNReal)),
  MulArchimedean.{u_1} (ValueGroupWithZero R)
Tactic: obtain ⟨⟨f, hf⟩⟩ := IsRankLeOne.nonempty (R := R)
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Trivial (goal)
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
x x_1 : R
⊢ (if x_1 = 0 then x = 0 else True) ∨ if x = 0 then x_1 = 0 else True
have pos : x_1 = 0 → x = 0 → x = 0 ∨ x_1 = 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Trivial (goal)
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
x x_1 : R
pos : x_1 = 0 → x = 0 → x = 0 ∨ x_1 = 0
⊢ (if x_1 = 0 then x = 0 else True) ∨ if x = 0 then x_1 = 0 else True
have neg : x_1 = 0 → ¬x = 0 → x = 0 ∨ True
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Trivial (goal)
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
x x_1 : R
pos : x_1 = 0 → x = 0 → x = 0 ∨ x_1 = 0
neg : x_1 = 0 → ¬x = 0 → x = 0 ∨ True
⊢ (if x_1 = 0 then x = 0 else True) ∨ if x = 0 then x_1 = 0 else True
have pos₁ : ¬x_1 = 0 → x = 0 → True ∨ x_1 = 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Trivial (goal)
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
x x_1 : R
pos : x_1 = 0 → x = 0 → x = 0 ∨ x_1 = 0
neg : x_1 = 0 → ¬x = 0 → x = 0 ∨ True
pos₁ : ¬x_1 = 0 → x = 0 → True ∨ x_1 = 0
⊢ (if x_1 = 0 then x = 0 else True) ∨ if x = 0 then x_1 = 0 else True
have neg₁ : ¬x_1 = 0 → ¬x = 0 → True ∨ True
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Trivial (goal)
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
z y x : R
h : if y = 0 then x = 0 else True
h_1 : if z = 0 then y = 0 else True
⊢ if z = 0 then x = 0 else True
have pos : z = 0 → x = 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Trivial (goal)
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
x y z : R
h : if z = 0 then x = 0 else True
h_1 : if z = 0 then y = 0 else True
⊢ if z = 0 then x + y = 0 else True
have pos : z = 0 → x + y = 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Trivial (goal)
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
x y : R
h : if y = 0 then x = 0 else True
x_1 : R
⊢ if y * x_1 = 0 then x * x_1 = 0 else True
have pos : y * x_1 = 0 → y = 0 → x = 0 → x * x_1 = 0
Tactic: split_ifs at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Trivial (goal)
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
x y : R
h : if y = 0 then x = 0 else True
x_1 : R
pos : y * x_1 = 0 → y = 0 → x = 0 → x * x_1 = 0
⊢ if y * x_1 = 0 then x * x_1 = 0 else True
have neg : y * x_1 = 0 → ¬y = 0 → True → x * x_1 = 0
Tactic: split_ifs at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Trivial (goal)
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
x y z : R
h : ¬if Eq (α := R) 0 0 then z = 0 else True
⊢ (if y * z = 0 then x * z = 0 else True) → if y = 0 then x = 0 else True
have pos : y * z = 0 → y = 0 → x * z = 0 → x = 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Trivial (goal)
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
x y z : R
h : ¬if Eq (α := R) 0 0 then z = 0 else True
pos : y * z = 0 → y = 0 → x * z = 0 → x = 0
⊢ (if y * z = 0 then x * z = 0 else True) → if y = 0 then x = 0 else True
have neg : y * z = 0 → ¬y = 0 → x * z = 0 → True
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Trivial (goal)
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
x y z : R
h : ¬if Eq (α := R) 0 0 then z = 0 else True
pos : y * z = 0 → y = 0 → x * z = 0 → x = 0
neg : y * z = 0 → ¬y = 0 → x * z = 0 → True
⊢ (if y * z = 0 then x * z = 0 else True) → if y = 0 then x = 0 else True
have pos₁ : ¬y * z = 0 → y = 0 → True → x = 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Trivial (goal)
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
x y z : R
h : ¬if Eq (α := R) 0 0 then z = 0 else True
pos : y * z = 0 → y = 0 → x * z = 0 → x = 0
neg : y * z = 0 → ¬y = 0 → x * z = 0 → True
pos₁ : ¬y * z = 0 → y = 0 → True → x = 0
⊢ (if y * z = 0 then x * z = 0 else True) → if y = 0 then x = 0 else True
have neg₁ : ¬y * z = 0 → ¬y = 0 → True → True
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Trivial (goal)
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
⊢ ¬if Eq (α := R) 0 0 then Eq (α := R) 1 0 else True
have pos : Eq (α := R) 0 0 → ¬Eq (α := R) 1 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Trivial (goal)
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
pos : Eq (α := R) 0 0 → ¬Eq (α := R) 1 0
⊢ ¬if Eq (α := R) 0 0 then Eq (α := R) 1 0 else True
have neg : ¬Eq (α := R) 0 0 → ¬True
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Trivial (goal)
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
h : ValuativeRel R
hv : Valuation.Compatible (R := R) (Γ := Γ) 1
⊢ h = trivialRel
have vle : ∀ (x x_1 : R), @vle _ inst _ x x_1 ↔ @vle _ inst _ x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Trivial (goal)
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
h : ValuativeRel R
hv : Valuation.Compatible (R := R) (Γ := Γ) 1
x x_1 : R
⊢ @vle _ inst _ x x_1 ↔ if x_1 = 0 then x = 0 else True
have vle : LE.le (α := Γ) ((1 : (a : R) → Γ) x : Γ) ((1 : (a : R) → Γ) x_1 : Γ) ↔ if x_1 = 0 then x = 0 else True
Tactic: rw [hv.vle_iff_le]
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Trivial (goal)
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
h : ValuativeRel R
hv : Valuation.Compatible (R := R) (Γ := Γ) 1
x x_1 : R
⊢ LE.le (α := Γ) ((1 : (a : R) → Γ) x : Γ) ((1 : (a : R) → Γ) x_1 : Γ) ↔ if x_1 = 0 then x = 0 else True
have pos : x_1 = 0 → (LE.le (α := Γ) ((1 : (a : R) → Γ) x : Γ) ((1 : (a : R) → Γ) x_1 : Γ) ↔ x = 0)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.Valuation.ValuativeRel.Trivial (goal)
Goal:
R Γ : Type
inst : CommRing R
inst_1 : DecidableEq R
inst_2 : IsDomain R
inst_3 : LinearOrderedCommGroupWithZero Γ
h : ValuativeRel R
hv : Valuation.Compatible (R := R) (Γ := Γ) 1
x x_1 : R
pos : x_1 = 0 → (LE.le (α := Γ) ((1 : (a : R) → Γ) x : Γ) ((1 : (a : R) → Γ) x_1 : Γ) ↔ x = 0)
⊢ LE.le (α := Γ) ((1 : (a : R) → Γ) x : Γ) ((1 : (a : R) → Γ) x_1 : Γ) ↔ if x_1 = 0 then x = 0 else True
have neg : ¬x_1 = 0 → (LE.le (α := Γ) ((1 : (a : R) → Γ) x : Γ) ((1 : (a : R) → Γ) x_1 : Γ) ↔ True)
Tactic: split_ifs