awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
tfae_1_iff_2 :
  v.IsEquiv v' ↔
    ∀ {x y : K},
      LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ↔
        LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) ((v' : (a : K) → Γ'₀) y : Γ'₀)
tfae_1_iff_3 :
  v.IsEquiv v' ↔
    ∀ {x : K},
      LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
        LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
tfae_1_iff_4 :
  v.IsEquiv v' ↔
    ∀ {x : K},
      Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
        Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
⊢ v.IsEquiv v' ↔
    ∀ {x : K},
      LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
        LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)

Tactic:
1 ↔ 5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
tfae_1_iff_2 :
  v.IsEquiv v' ↔
    ∀ {x y : K},
      LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ↔
        LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) ((v' : (a : K) → Γ'₀) y : Γ'₀)
tfae_1_iff_3 :
  v.IsEquiv v' ↔
    ∀ {x : K},
      LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
        LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
tfae_1_iff_4 :
  v.IsEquiv v' ↔
    ∀ {x : K},
      Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
        Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
⊢ v.IsEquiv v' ↔
    ∀ {x : K},
      LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
        LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)

Tactic:
tfae_have 1 ↔ 5 := isEquiv_iff_val_lt_one

Premises used: Valuation.isEquiv_iff_val_lt_one
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
tfae_1_iff_2 :
  v.IsEquiv v' ↔
    ∀ {x y : K},
      LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ↔
        LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) ((v' : (a : K) → Γ'₀) y : Γ'₀)
tfae_1_iff_3 :
  v.IsEquiv v' ↔
    ∀ {x : K},
      LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
        LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
tfae_1_iff_4 :
  v.IsEquiv v' ↔
    ∀ {x : K},
      Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
        Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
tfae_1_iff_5 :
  v.IsEquiv v' ↔
    ∀ {x : K},
      LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
        LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
⊢ v.IsEquiv v'

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
tfae_1_iff_2 :
  v.IsEquiv v' ↔
    ∀ {x y : K},
      LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ↔
        LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) ((v' : (a : K) → Γ'₀) y : Γ'₀)
tfae_1_iff_3 :
  v.IsEquiv v' ↔
    ∀ {x : K},
      LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
        LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
tfae_1_iff_4 :
  v.IsEquiv v' ↔
    ∀ {x : K},
      Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
        Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
tfae_1_iff_5 :
  v.IsEquiv v' ↔
    ∀ {x : K},
      LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
        LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
⊢ ∀ {x : K},
    LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) (x - 1) : Γ₀) (1 : Γ₀) ↔
      LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) (x - 1) : Γ'₀) (1 : Γ'₀)

Tactic:
6

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
tfae_1_iff_2 :
  v.IsEquiv v' ↔
    ∀ {x y : K},
      LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ↔
        LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) ((v' : (a : K) → Γ'₀) y : Γ'₀)
tfae_1_iff_3 :
  v.IsEquiv v' ↔
    ∀ {x : K},
      LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
        LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
tfae_1_iff_4 :
  v.IsEquiv v' ↔
    ∀ {x : K},
      Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
        Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
tfae_1_iff_5 :
  v.IsEquiv v' ↔
    ∀ {x : K},
      LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
        LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
⊢ v.IsEquiv v' ↔
    ∀ {x : K},
      LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) (x - 1) : Γ₀) (1 : Γ₀) ↔
        LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) (x - 1) : Γ'₀) (1 : Γ'₀)

Tactic:
1 ↔ 6

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
tfae_1_iff_2 :
  v.IsEquiv v' ↔
    ∀ {x y : K},
      LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ↔
        LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) ((v' : (a : K) → Γ'₀) y : Γ'₀)
tfae_1_iff_3 :
  v.IsEquiv v' ↔
    ∀ {x : K},
      LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
        LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
tfae_1_iff_4 :
  v.IsEquiv v' ↔
    ∀ {x : K},
      Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
        Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
tfae_1_iff_5 :
  v.IsEquiv v' ↔
    ∀ {x : K},
      LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
        LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
⊢ v.IsEquiv v' ↔
    ∀ {x : K},
      LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) (x - 1) : Γ₀) (1 : Γ₀) ↔
        LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) (x - 1) : Γ'₀) (1 : Γ'₀)

Tactic:
tfae_have 1 ↔ 6 := isEquiv_iff_val_sub_one_lt_one

Premises used: Valuation.isEquiv_iff_val_sub_one_lt_one
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst_1 : LinearOrderedCommGroupWithZero Γ₀
inst_2 : LinearOrderedCommGroupWithZero Γ'₀
v : Valuation K Γ₀
v' : Valuation K Γ'₀
tfae_1_iff_2 :
  v.IsEquiv v' ↔
    ∀ {x y : K},
      LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ↔
        LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) ((v' : (a : K) → Γ'₀) y : Γ'₀)
tfae_1_iff_3 :
  v.IsEquiv v' ↔
    ∀ {x : K},
      LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
        LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
tfae_1_iff_4 :
  v.IsEquiv v' ↔
    ∀ {x : K},
      Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
        Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
tfae_1_iff_5 :
  v.IsEquiv v' ↔
    ∀ {x : K},
      LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
        LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
tfae_1_iff_6 :
  v.IsEquiv v' ↔
    ∀ {x : K},
      LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) (x - 1) : Γ₀) (1 : Γ₀) ↔
        LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) (x - 1) : Γ'₀) (1 : Γ'₀)
⊢ [v.IsEquiv v',
      ∀ {x y : K},
        LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀) ↔
          LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) ((v' : (a : K) → Γ'₀) y : Γ'₀),
      ∀ {x : K},
        LE.le.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
          LE.le.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀),
      ∀ {x : K},
        Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
          Eq.{u_5 + 1} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀),
      ∀ {x : K},
        LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
          LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) x : Γ'₀) (1 : Γ'₀),
      ∀ {x : K},
        LT.lt.{u_4} (α := Γ₀) ((v : (a : K) → Γ₀) (x - 1) : Γ₀) (1 : Γ₀) ↔
          LT.lt.{u_5} (α := Γ'₀) ((v' : (a : K) → Γ'₀) (x - 1) : Γ'₀) (1 : Γ'₀)].TFAE

Tactic:
tfae_finish
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : CommRing R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x : R
⊢ x ∈ v.supp ↔ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.RingTheory.Valuation.Basic
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 Γ₀
h : v.supp = ⊤
rw : Membership.mem (γ := Ideal R) ⊤ 1
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) 1 : Γ₀) (0 : Γ₀)

Tactic:
rw [← mem_supp_iff, h]

Premises used: Valuation.mem_supp_iff
-- Module: Mathlib.RingTheory.Valuation.Basic
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 Γ₀
h : v.supp = ⊤
⊢ Membership.mem (γ := Ideal R) ⊤ 1

Tactic:
Submodule.mem_top

Premises used: Set.Mem, Submodule.mem_top
-- Module: Mathlib.RingTheory.Valuation.Basic
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 Γ₀
h : v.supp = ⊤
⊢ Membership.mem (γ := Ideal R) ⊤ 1

Tactic:
exact Submodule.mem_top

Premises used: Submodule.mem_top
-- Module: Mathlib.RingTheory.Valuation.Basic
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 : x * y ∈ v.supp
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x * y) : Γ₀) (0 : Γ₀)

Tactic:
simp only [mem_supp_iff] at hxy ⊢

Premises used: Valuation.mem_supp_iff
-- Module: Mathlib.RingTheory.Valuation.Basic
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 : Γ₀)
⊢ HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) = 0

Tactic:
rw [v.map_mul x y] at hxy

Premises used: Valuation.map_mul
-- Module: Mathlib.RingTheory.Valuation.Basic
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 : HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) = 0
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀) ∨
    Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀)

Tactic:
eq_zero_or_eq_zero_of_mul_eq_zero hxy

Premises used: NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero
-- Module: Mathlib.RingTheory.Valuation.Basic
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 : HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) = 0
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀) ∨
    Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) (0 : Γ₀)

Tactic:
exact eq_zero_or_eq_zero_of_mul_eq_zero hxy

Premises used: NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero
-- Module: Mathlib.RingTheory.Valuation.Basic
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' : Γ₀)

Tactic:
le_trans (v.map_add a' s') (max_le le_rfl ?_)

Premises used: le_rfl, Valuation.map_add, max_le, le_trans
-- Module: Mathlib.RingTheory.Valuation.Basic
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 : Γ₀)
refine : LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) s' : Γ₀) ((v : (a : R) → Γ₀) a' : Γ₀)
⊢ LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (a' + s') : Γ₀) ((v : (a : R) → Γ₀) a' : Γ₀)

Tactic:
refine le_trans (v.map_add a' s') (max_le le_rfl ?_)

Premises used: le_rfl, Valuation.map_add, max_le, le_trans
-- Module: Mathlib.RingTheory.Valuation.Basic
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) → Γ₀) s' : Γ₀) ((v : (a : R) → Γ₀) a' : Γ₀)

Tactic:
simp [h']
-- Module: Mathlib.RingTheory.Valuation.Basic
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),
    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']
-- Module: Mathlib.RingTheory.Valuation.Basic
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 : Γ₀)
apply : LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) a : Γ₀) ((v : (a : R) → Γ₀) (a + s) : Γ₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (a + s) : Γ₀) ((v : (a : R) → Γ₀) a : Γ₀)

Tactic:
apply le_antisymm (aux a s h)

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.Valuation.Basic
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 : Γ₀) ((v : (a : R) → Γ₀) (a + s + -s) : Γ₀)

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.Basic
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 : Γ₀)
rwa rwa₁ rwa₂ 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 : Γ₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (-s) : Γ₀) (0 : Γ₀)

Tactic:
rwa [← Ideal.neg_mem_iff] at h

Premises used: Ideal.neg_mem_iff
-- Module: Mathlib.RingTheory.Valuation.Basic
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 : Γ₀)
v₁ : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) a : Γ₀) ((v : (a : R) → Γ₀) (a + s + -s) : Γ₀)
⊢ LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) a : Γ₀) ((v : (a : R) → Γ₀) (a + 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)

Premises used: HAdd.hAdd, DFunLike.coe, Neg.neg
-- Module: Mathlib.RingTheory.Valuation.Basic
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 : Γ₀)
rw₃ 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 : Γ₀)
⊢ x ∈ (comap f v).supp ↔ Membership.mem (γ := Ideal S) (Ideal.comap f v.supp) x

Tactic:
rw [mem_supp_iff, Ideal.mem_comap, mem_supp_iff, comap_apply]

Premises used: Valuation.mem_supp_iff, Valuation.comap_apply, Ideal.mem_comap
-- Module: Mathlib.RingTheory.Valuation.Basic
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 Γ₀
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
⊢ 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

Tactic:
cases f
-- Module: Mathlib.RingTheory.Valuation.Basic
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)
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 }
⊢ 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 g
-- Module: Mathlib.RingTheory.Valuation.Basic
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 Γ₀
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)
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:
simp +contextual
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀
f : R → Γ₀
h0 : f 0 = ⊤
h1 : f 1 = 0
hadd : ∀ (x y : R), min (f x) (f y) ≤ f (x + y)
hmul : ∀ (x y : R), f (x * y) = f x + f y
r : R
⊢ (of f h0 h1 hadd hmul : (a : R) → Γ₀) r = f r

Tactic:
rfl

Premises used: rfl