awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_7
inst : DivisionRing K
Γ₀ : Type u_8
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
hv : v.IsNontrivial
obtain :
  ∀ (x : Kˣ) (hx : Ne.{u_8 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) (↑x : K) : Γ₀) (1 : Γ₀)),
    ∃ (x : K), x ≠ 0 ∧ LT.lt.{u_8} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ ∃ (x : K), x ≠ 0 ∧ LT.lt.{u_8} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)

Tactic:
obtain ⟨x, hx⟩ := isNontrivial_iff_exists_unit.mp hv

Premises used: Valuation.isNontrivial_iff_exists_unit, Iff.mp
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_7
inst : DivisionRing K
Γ₀ : Type u_8
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
hv : v.IsNontrivial
x : Kˣ
hx : Ne.{u_8 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) (↑x : K) : Γ₀) (1 : Γ₀)
⊢ LT.lt.{u_8} (α := Γ₀) ((v : (a : K) → Γ₀) (↑x : K) : Γ₀) (1 : Γ₀) ∨
    LT.lt.{u_8} (α := Γ₀) (1 : Γ₀) ((v : (a : K) → Γ₀) (↑x : K) : Γ₀)

Tactic:
rw [ne_iff_lt_or_gt] at hx

Premises used: ne_iff_lt_or_gt
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_7
inst : DivisionRing K
Γ₀ : Type u_8
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
hv : v.IsNontrivial
x : Kˣ
hx :
  LT.lt.{u_8} (α := Γ₀) ((v : (a : K) → Γ₀) (↑x : K) : Γ₀) (1 : Γ₀) ∨
    LT.lt.{u_8} (α := Γ₀) (1 : Γ₀) ((v : (a : K) → Γ₀) (↑x : K) : Γ₀)
inl :
  ∀ (hx : LT.lt.{u_8} (α := Γ₀) ((v : (a : K) → Γ₀) (↑x : K) : Γ₀) (1 : Γ₀)),
    ∃ (x : K), x ≠ 0 ∧ LT.lt.{u_8} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
inr :
  ∀ (hx : LT.lt.{u_8} (α := Γ₀) (1 : Γ₀) ((v : (a : K) → Γ₀) (↑x : K) : Γ₀)),
    ∃ (x : K), x ≠ 0 ∧ LT.lt.{u_8} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ ∃ (x : K), x ≠ 0 ∧ LT.lt.{u_8} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)

Tactic:
rcases hx with hx | hx
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_7
inst : DivisionRing K
Γ₀ : Type u_8
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
hv : v.IsNontrivial
x : Kˣ
hx : LT.lt.{u_8} (α := Γ₀) ((v : (a : K) → Γ₀) (↑x : K) : Γ₀) (1 : Γ₀)
h : (↑x : K) ≠ 0 ∧ LT.lt.{u_8} (α := Γ₀) ((v : (a : K) → Γ₀) (↑x : K) : Γ₀) (1 : Γ₀)
⊢ ∃ (x : K), x ≠ 0 ∧ LT.lt.{u_8} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)

Tactic:
use x
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_7
inst : DivisionRing K
Γ₀ : Type u_8
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
hv : v.IsNontrivial
x : Kˣ
hx : LT.lt.{u_8} (α := Γ₀) ((v : (a : K) → Γ₀) (↑x : K) : Γ₀) (1 : Γ₀)
⊢ (↑x : K) ≠ 0 ∧ LT.lt.{u_8} (α := Γ₀) ((v : (a : K) → Γ₀) (↑x : K) : Γ₀) (1 : Γ₀)

Tactic:
simp [hx]
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_7
inst : DivisionRing K
Γ₀ : Type u_8
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
hv : v.IsNontrivial
x : Kˣ
hx : LT.lt.{u_8} (α := Γ₀) (1 : Γ₀) ((v : (a : K) → Γ₀) (↑x : K) : Γ₀)
h : (↑x : K)⁻¹ ≠ 0 ∧ LT.lt.{u_8} (α := Γ₀) ((v : (a : K) → Γ₀) (↑x : K)⁻¹ : Γ₀) (1 : Γ₀)
⊢ ∃ (x : K), x ≠ 0 ∧ LT.lt.{u_8} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)

Tactic:
use x⁻¹
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_7
inst : DivisionRing K
Γ₀ : Type u_8
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
hv : v.IsNontrivial
x : Kˣ
hx : LT.lt.{u_8} (α := Γ₀) (1 : Γ₀) ((v : (a : K) → Γ₀) (↑x : K) : Γ₀)
⊢ (↑x : K)⁻¹ ≠ 0 ∧ LT.lt.{u_8} (α := Γ₀) ((v : (a : K) → Γ₀) (↑x : K)⁻¹ : Γ₀) (1 : Γ₀)

Tactic:
simp [-map_inv₀, ← one_lt_val_iff, hx]

Premises used: Valuation.one_lt_val_iff, map_inv₀
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_7
inst : DivisionRing K
Γ₀ : Type u_8
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
h : v.IsNontrivial
⊢ ∃ (x : K), x ≠ 0 ∧ LT.lt.{u_8} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)

Tactic:
simpa using h.exists_lt_one (v := v)

Premises used: Valuation.IsNontrivial.exists_lt_one
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_7
inst : DivisionRing K
Γ₀ : Type u_8
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
h : ∃ (x : K), x ≠ 0 ∧ LT.lt.{u_8} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
x : K
hx0 : x ≠ 0
hx1 : LT.lt.{u_8} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ Ne.{u_8 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀) ∧
    Ne.{u_8 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)

Tactic:
simp [hx0, hx1.ne]

Premises used: LT.lt.ne
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_7
inst : DivisionRing K
Γ₀ : Type u_8
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
hv : v.IsNontrivial
obtain :
  ∀ (x : K) (h0 : x ≠ 0) (h1 : LT.lt.{u_8} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)),
    ∃ (x : K), LT.lt.{u_8} (α := Γ₀) (1 : Γ₀) ((v : (a : K) → Γ₀) x : Γ₀)
⊢ ∃ (x : K), LT.lt.{u_8} (α := Γ₀) (1 : Γ₀) ((v : (a : K) → Γ₀) x : Γ₀)

Tactic:
obtain ⟨x, h0, h1⟩ := hv.exists_lt_one

Premises used: Valuation.IsNontrivial.exists_lt_one
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_7
inst : DivisionRing K
Γ₀ : Type u_8
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
hv : v.IsNontrivial
x : K
h0 : x ≠ 0
h1 : LT.lt.{u_8} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
h : LT.lt.{u_8} (α := Γ₀) (1 : Γ₀) ((v : (a : K) → Γ₀) x⁻¹ : Γ₀)
⊢ ∃ (x : K), LT.lt.{u_8} (α := Γ₀) (1 : Γ₀) ((v : (a : K) → Γ₀) x : Γ₀)

Tactic:
use x⁻¹
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_7
inst : DivisionRing K
Γ₀ : Type u_8
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
hv : v.IsNontrivial
x : K
h0 : x ≠ 0
h1 : LT.lt.{u_8} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ Ne.{u_8 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀)

Tactic:
simp [h0]
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_7
inst : DivisionRing K
Γ₀ : Type u_8
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
hv : v.IsNontrivial
x : K
h0 : x ≠ 0
h1 : LT.lt.{u_8} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)
⊢ LT.lt.{u_8} (α := Γ₀) (1 : Γ₀) ((v : (a : K) → Γ₀) x⁻¹ : Γ₀)

Tactic:
simp [one_lt_inv₀ (zero_lt_iff.mpr (by simp [h0] : v x ≠ 0)), h1]

Premises used: Iff.mpr, zero_lt_iff, one_lt_inv₀
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_7
inst : DivisionRing K
Γ₀ : Type u_8
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
h : v.IsNontrivial
⊢ ∃ (x : K), LT.lt.{u_8} (α := Γ₀) (1 : Γ₀) ((v : (a : K) → Γ₀) x : Γ₀)

Tactic:
simpa using h.exists_one_lt (v := v)

Premises used: Valuation.IsNontrivial.exists_one_lt
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_7
inst : DivisionRing K
Γ₀ : Type u_8
inst_1 : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
h : ∃ (x : K), LT.lt.{u_8} (α := Γ₀) (1 : Γ₀) ((v : (a : K) → Γ₀) x : Γ₀)
x : K
hx1 : LT.lt.{u_8} (α := Γ₀) (1 : Γ₀) ((v : (a : K) → Γ₀) x : Γ₀)
⊢ Ne.{u_8 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀) ∧
    Ne.{u_8 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (1 : Γ₀)

Tactic:
aesop
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
Γ₀ : Type u_4
inst : LinearOrderedCommMonoidWithZero Γ₀
B : Type u_7
A : Type u_8
inst_1 : CommSemiring A
inst_2 : Ring B
inst_3 : Algebra A B
v : Valuation B Γ₀
inst_4 : IsTrivialOn A v
a : A
pos : a = 0 → LE.le.{u_4} (α := Γ₀) ((v : (a : B) → Γ₀) ((algebraMap A B : (a : A) → B) a : B) : Γ₀) (1 : Γ₀)
neg : ¬a = 0 → LE.le.{u_4} (α := Γ₀) ((v : (a : B) → Γ₀) ((algebraMap A B : (a : A) → B) a : B) : Γ₀) (1 : Γ₀)
⊢ LE.le.{u_4} (α := Γ₀) ((v : (a : B) → Γ₀) ((algebraMap A B : (a : A) → B) a : B) : Γ₀) (1 : Γ₀)

Tactic:
by_cases a = 0
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
Γ₀ : Type u_4
inst : LinearOrderedCommMonoidWithZero Γ₀
B : Type u_7
A : Type u_8
inst_1 : CommSemiring A
inst_2 : Ring B
inst_3 : Algebra A B
v : Valuation B Γ₀
inst_4 : IsTrivialOn A v
a : A
h : a = 0
⊢ LE.le.{u_4} (α := Γ₀) ((v : (a : B) → Γ₀) ((algebraMap A B : (a : A) → B) a : B) : Γ₀) (1 : Γ₀)

Tactic:
grind [zero_le']

Premises used: zero_le'
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
Γ₀ : Type u_4
inst : LinearOrderedCommMonoidWithZero Γ₀
B : Type u_7
A : Type u_8
inst_1 : CommSemiring A
inst_2 : Ring B
inst_3 : Algebra A B
v : Valuation B Γ₀
inst_4 : IsTrivialOn A v
a : A
h : ¬a = 0
⊢ LE.le.{u_4} (α := Γ₀) ((v : (a : B) → Γ₀) ((algebraMap A B : (a : A) → B) a : B) : Γ₀) (1 : Γ₀)

Tactic:
grind [zero_le']

Premises used: zero_le'
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
⊢ v.IsEquiv v

Tactic:
fun _ _ => Iff.refl _

Premises used: Iff.refl, LE.le, Valuation.IsEquiv, DFunLike.coe
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : LinearOrderedCommMonoidWithZero Γ'₀
v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
h : v₁.IsEquiv v₂
⊢ v₂.IsEquiv v₁

Tactic:
fun _ _ => Iff.symm (h _ _)

Premises used: Valuation.IsEquiv, Iff.symm
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
Γ''₀ : Type u_6
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : LinearOrderedCommMonoidWithZero Γ'₀
inst_3 : LinearOrderedCommMonoidWithZero Γ''₀
v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
v₃ : Valuation R Γ''₀
h₁₂ : v₁.IsEquiv v₂
h₂₃ : v₂.IsEquiv v₃
⊢ v₁.IsEquiv v₃

Tactic:
fun _ _ =>
  Iff.trans (h₁₂ _ _) (h₂₃ _ _)

Premises used: Iff.trans, Valuation.IsEquiv
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v v' : Valuation R Γ₀
h : v = v'
subst : v.IsEquiv v
⊢ v.IsEquiv v'

Tactic:
subst h
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
⊢ v.IsEquiv v

Tactic:
rfl
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : LinearOrderedCommMonoidWithZero Γ'₀
v v' : Valuation R Γ₀
f : Γ₀ →*₀ Γ'₀
hf : Monotone.{u_4, u_5} (α := Γ₀) (β := Γ'₀) (⇑f : (a : Γ₀) → Γ'₀)
inf : Injective.{u_4 + 1, u_5 + 1} (α := Γ₀) (β := Γ'₀) (⇑f : (a : Γ₀) → Γ'₀)
h : v.IsEquiv v'
H : StrictMono.{u_4, u_5} (α := Γ₀) (β := Γ'₀) (⇑f : (a : Γ₀) → Γ'₀) := ⋯
r s : R
rw rw₁ :
  LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) ((v : (a : R) → Γ₀) s : Γ₀) ↔
    LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) ((v : (a : R) → Γ₀) s : Γ₀)
⊢ LE.le.{u_5} (α := Γ'₀) ((f : (a : Γ₀) → Γ'₀) ((v : (a : R) → Γ₀) r : Γ₀) : Γ'₀)
      ((f : (a : Γ₀) → Γ'₀) ((v : (a : R) → Γ₀) s : Γ₀) : Γ'₀) ↔
    LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) ((v : (a : R) → Γ₀) s : Γ₀)

Tactic:
rw [H.le_iff_le]

Premises used: StrictMono.le_iff_le
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : LinearOrderedCommMonoidWithZero Γ'₀
v v' : Valuation R Γ₀
f : Γ₀ →*₀ Γ'₀
hf : Monotone.{u_4, u_5} (α := Γ₀) (β := Γ'₀) (⇑f : (a : Γ₀) → Γ'₀)
inf : Injective.{u_4 + 1, u_5 + 1} (α := Γ₀) (β := Γ'₀) (⇑f : (a : Γ₀) → Γ'₀)
h : v.IsEquiv v'
H : StrictMono.{u_4, u_5} (α := Γ₀) (β := Γ'₀) (⇑f : (a : Γ₀) → Γ'₀) := ⋯
r s : R
rw rw₁ :
  LE.le.{u_4} (α := Γ₀) ((v' : (a : R) → Γ₀) r : Γ₀) ((v' : (a : R) → Γ₀) s : Γ₀) ↔
    LE.le.{u_4} (α := Γ₀) ((v' : (a : R) → Γ₀) r : Γ₀) ((v' : (a : R) → Γ₀) s : Γ₀)
⊢ LE.le.{u_4} (α := Γ₀) ((v' : (a : R) → Γ₀) r : Γ₀) ((v' : (a : R) → Γ₀) s : Γ₀) ↔
    LE.le.{u_5} (α := Γ'₀) ((f : (a : Γ₀) → Γ'₀) ((v' : (a : R) → Γ₀) r : Γ₀) : Γ'₀)
      ((f : (a : Γ₀) → Γ'₀) ((v' : (a : R) → Γ₀) s : Γ₀) : Γ'₀)

Tactic:
rw [H.le_iff_le]

Premises used: StrictMono.le_iff_le
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : LinearOrderedCommMonoidWithZero Γ'₀
v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
S : Type u_7
inst_3 : Ring S
f : S →+* R
h : v₁.IsEquiv v₂
⊢ (Valuation.comap f v₁).IsEquiv (Valuation.comap f v₂)

Tactic:
fun r s => h (f r) (f s)

Premises used: Valuation.IsEquiv, DFunLike.coe
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : LinearOrderedCommMonoidWithZero Γ'₀
v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
h : v₁.IsEquiv v₂
r s : R
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v₁ : (a : R) → Γ₀) r : Γ₀) ((v₁ : (a : R) → Γ₀) s : Γ₀) ↔
    Eq.{u_5 + 1} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) r : Γ'₀) ((v₂ : (a : R) → Γ'₀) s : Γ'₀)

Tactic:
simpa only [le_antisymm_iff] using and_congr (h r s) (h s r)

Premises used: le_antisymm_iff, and_congr
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : LinearOrderedCommMonoidWithZero Γ'₀
v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
h : v₁.IsEquiv v₂
r : R
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v₁ : (a : R) → Γ₀) r : Γ₀) ((v₁ : (a : R) → Γ₀) 0 : Γ₀) ↔
    Eq.{u_5 + 1} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) r : Γ'₀) ((v₂ : (a : R) → Γ'₀) 0 : Γ'₀)

Tactic:
have : v₁ r = v₁ 0 ↔ v₂ r = v₂ 0 := h.eq_iff
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : LinearOrderedCommMonoidWithZero Γ'₀
v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
h : v₁.IsEquiv v₂
r : R
this :
  Eq.{u_4 + 1} (α := Γ₀) ((v₁ : (a : R) → Γ₀) r : Γ₀) ((v₁ : (a : R) → Γ₀) 0 : Γ₀) ↔
    Eq.{u_5 + 1} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) r : Γ'₀) ((v₂ : (a : R) → Γ'₀) 0 : Γ'₀)
rwa :
  ∀
    (this :
      Eq.{u_4 + 1} (α := Γ₀) ((v₁ : (a : R) → Γ₀) r : Γ₀) (0 : Γ₀) ↔
        Eq.{u_5 + 1} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) r : Γ'₀) ((v₂ : (a : R) → Γ'₀) 0 : Γ'₀)),
    Eq.{u_4 + 1} (α := Γ₀) ((v₁ : (a : R) → Γ₀) r : Γ₀) (0 : Γ₀) ↔
      Eq.{u_5 + 1} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) r : Γ'₀) (0 : Γ'₀)
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀
    (this :
      Eq.{u_4 + 1} (α := Γ₀) ((v₁ : (a : R) → Γ₀) r : Γ₀) (0 : Γ₀) ↔
        Eq.{u_5 + 1} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) r : Γ'₀) (0 : Γ'₀)),
    Eq.{u_4 + 1} (α := Γ₀) ((v₁ : (a : R) → Γ₀) r : Γ₀) (0 : Γ₀) ↔
      Eq.{u_5 + 1} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) r : Γ'₀) (0 : Γ'₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v₁ : (a : R) → Γ₀) r : Γ₀) (0 : Γ₀) ↔
    Eq.{u_5 + 1} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) r : Γ'₀) (0 : Γ'₀)

Tactic:
rwa [v₁.map_zero, v₂.map_zero] at this

Premises used: Valuation.map_zero
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : LinearOrderedCommMonoidWithZero Γ'₀
v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
h : v₁.IsEquiv v₂
r : R
⊢ Ne.{u_4 + 1} (α := Γ₀) ((v₁ : (a : R) → Γ₀) r : Γ₀) (0 : Γ₀) ↔
    Ne.{u_5 + 1} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) r : Γ'₀) (0 : Γ'₀)

Tactic:
(eq_zero h).ne

Premises used: Valuation.IsEquiv.eq_zero, Iff.ne
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : LinearOrderedCommMonoidWithZero Γ'₀
v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
h : v₁.IsEquiv v₂
x : R
rw :
  Ne.{u_4 + 1} (α := Γ₀) ((v₁ : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀) ↔
    LT.lt.{u_5} (α := Γ'₀) (0 : Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀)
rw₁ :
  Ne.{u_4 + 1} (α := Γ₀) ((v₁ : (a : R) → Γ₀) x : Γ₀) (0 : Γ₀) ↔
    Ne.{u_5 + 1} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) (0 : Γ'₀)
rw₂ rw₃ :
  Ne.{u_5 + 1} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) (0 : Γ'₀) ↔
    Ne.{u_5 + 1} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) (0 : Γ'₀)
⊢ LT.lt.{u_4} (α := Γ₀) (0 : Γ₀) ((v₁ : (a : R) → Γ₀) x : Γ₀) ↔
    LT.lt.{u_5} (α := Γ'₀) (0 : Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀)

Tactic:
rw [zero_lt_iff, zero_lt_iff, h.eq_zero.ne]

Premises used: Valuation.IsEquiv.eq_zero, Iff.ne, zero_lt_iff
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : LinearOrderedCommMonoidWithZero Γ'₀
v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
h : v₁.IsEquiv v₂
x y : R
⊢ LE.le.{u_4} (α := Γ₀) ((v₁ : (a : R) → Γ₀) x : Γ₀) ((v₁ : (a : R) → Γ₀) y : Γ₀) ↔
    LE.le.{u_5} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) ((v₂ : (a : R) → Γ'₀) y : Γ'₀)

Tactic:
h x y
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : LinearOrderedCommMonoidWithZero Γ'₀
v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
h : v₁.IsEquiv v₂
x y : R
rw :
  LE.le.{u_4} (α := Γ₀) ((v₁ : (a : R) → Γ₀) y : Γ₀) ((v₁ : (a : R) → Γ₀) x : Γ₀) ↔
    LE.le.{u_5} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) y : Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀)
rw₁ rw₂ :
  LE.le.{u_5} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) y : Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) ↔
    LE.le.{u_5} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) y : Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀)
⊢ LT.lt.{u_4} (α := Γ₀) ((v₁ : (a : R) → Γ₀) x : Γ₀) ((v₁ : (a : R) → Γ₀) y : Γ₀) ↔
    LT.lt.{u_5} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) ((v₂ : (a : R) → Γ'₀) y : Γ'₀)

Tactic:
rw [← le_iff_le_iff_lt_iff_lt, h]

Premises used: le_iff_le_iff_lt_iff_lt
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : LinearOrderedCommMonoidWithZero Γ'₀
v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
h : v₁.IsEquiv v₂
x : R
rw :
  LE.le.{u_4} (α := Γ₀) ((v₁ : (a : R) → Γ₀) x : Γ₀) ((v₁ : (a : R) → Γ₀) 1 : Γ₀) ↔
    LE.le.{u_5} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
rw₁ :
  LE.le.{u_5} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) ((v₂ : (a : R) → Γ'₀) 1 : Γ'₀) ↔
    LE.le.{u_5} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
rw₂ rw₃ :
  LE.le.{u_5} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) (1 : Γ'₀) ↔
    LE.le.{u_5} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
⊢ LE.le.{u_4} (α := Γ₀) ((v₁ : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
    LE.le.{u_5} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) (1 : Γ'₀)

Tactic:
rw [← v₁.map_one, h, map_one]

Premises used: Valuation.map_one, map_one
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : LinearOrderedCommMonoidWithZero Γ'₀
v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
h : v₁.IsEquiv v₂
x : R
rw :
  LE.le.{u_4} (α := Γ₀) ((v₁ : (a : R) → Γ₀) 1 : Γ₀) ((v₁ : (a : R) → Γ₀) x : Γ₀) ↔
    LE.le.{u_5} (α := Γ'₀) (1 : Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀)
rw₁ :
  LE.le.{u_5} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) 1 : Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) ↔
    LE.le.{u_5} (α := Γ'₀) (1 : Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀)
rw₂ rw₃ :
  LE.le.{u_5} (α := Γ'₀) (1 : Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) ↔
    LE.le.{u_5} (α := Γ'₀) (1 : Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀)
⊢ LE.le.{u_4} (α := Γ₀) (1 : Γ₀) ((v₁ : (a : R) → Γ₀) x : Γ₀) ↔
    LE.le.{u_5} (α := Γ'₀) (1 : Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀)

Tactic:
rw [← v₁.map_one, h, map_one]

Premises used: Valuation.map_one, map_one
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : LinearOrderedCommMonoidWithZero Γ'₀
v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
h : v₁.IsEquiv v₂
x : R
rw :
  Eq.{u_4 + 1} (α := Γ₀) ((v₁ : (a : R) → Γ₀) x : Γ₀) ((v₁ : (a : R) → Γ₀) 1 : Γ₀) ↔
    Eq.{u_5 + 1} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
rw₁ :
  Eq.{u_5 + 1} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) ((v₂ : (a : R) → Γ'₀) 1 : Γ'₀) ↔
    Eq.{u_5 + 1} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
rw₂ rw₃ :
  Eq.{u_5 + 1} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) (1 : Γ'₀) ↔
    Eq.{u_5 + 1} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v₁ : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
    Eq.{u_5 + 1} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) (1 : Γ'₀)

Tactic:
rw [← v₁.map_one, h.eq_iff, map_one]

Premises used: Valuation.map_one, map_one, Valuation.IsEquiv.eq_iff
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : LinearOrderedCommMonoidWithZero Γ'₀
v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
h : v₁.IsEquiv v₂
x : R
rw :
  LT.lt.{u_4} (α := Γ₀) ((v₁ : (a : R) → Γ₀) x : Γ₀) ((v₁ : (a : R) → Γ₀) 1 : Γ₀) ↔
    LT.lt.{u_5} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
rw₁ :
  LT.lt.{u_5} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) ((v₂ : (a : R) → Γ'₀) 1 : Γ'₀) ↔
    LT.lt.{u_5} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
rw₂ rw₃ :
  LT.lt.{u_5} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) (1 : Γ'₀) ↔
    LT.lt.{u_5} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) (1 : Γ'₀)
⊢ LT.lt.{u_4} (α := Γ₀) ((v₁ : (a : R) → Γ₀) x : Γ₀) (1 : Γ₀) ↔
    LT.lt.{u_5} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) (1 : Γ'₀)

Tactic:
rw [← v₁.map_one, h.lt_iff_lt, map_one]

Premises used: Valuation.IsEquiv.lt_iff_lt, Valuation.map_one, map_one
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : LinearOrderedCommMonoidWithZero Γ'₀
v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
h : v₁.IsEquiv v₂
x : R
rw :
  LT.lt.{u_4} (α := Γ₀) ((v₁ : (a : R) → Γ₀) 1 : Γ₀) ((v₁ : (a : R) → Γ₀) x : Γ₀) ↔
    LT.lt.{u_5} (α := Γ'₀) (1 : Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀)
rw₁ :
  LT.lt.{u_5} (α := Γ'₀) ((v₂ : (a : R) → Γ'₀) 1 : Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) ↔
    LT.lt.{u_5} (α := Γ'₀) (1 : Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀)
rw₂ rw₃ :
  LT.lt.{u_5} (α := Γ'₀) (1 : Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀) ↔
    LT.lt.{u_5} (α := Γ'₀) (1 : Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀)
⊢ LT.lt.{u_4} (α := Γ₀) (1 : Γ₀) ((v₁ : (a : R) → Γ₀) x : Γ₀) ↔
    LT.lt.{u_5} (α := Γ'₀) (1 : Γ'₀) ((v₂ : (a : R) → Γ'₀) x : Γ'₀)

Tactic:
rw [← v₁.map_one, h.lt_iff_lt, map_one]

Premises used: Valuation.IsEquiv.lt_iff_lt, Valuation.map_one, map_one
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : LinearOrderedCommMonoidWithZero Γ'₀
v₁ : Valuation R Γ₀
v₂ : Valuation R Γ'₀
A : Type u_7
inst_3 : CommSemiring A
inst_4 : Algebra A R
h : v₁.IsEquiv v₂
⊢ IsTrivialOn A v₁ ↔ IsTrivialOn A v₂

Tactic:
⟨fun h₁ ↦ h.isTrivialOn h₁, fun h₂ ↦ h.symm.isTrivialOn h₂⟩

Premises used: Iff.intro, Valuation.IsEquiv.symm, Valuation.IsEquiv.isTrivialOn
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : LinearOrderedCommMonoidWithZero Γ'₀
v : Valuation R Γ₀
f : Γ₀ →*₀ Γ'₀
H : StrictMono.{u_4, u_5} (α := Γ₀) (β := Γ'₀) (⇑f : (a : Γ₀) → Γ'₀)
⊢ (map f ⋯ v).IsEquiv v

Tactic:
fun _x _y =>
  ⟨H.le_iff_le.mp, fun h => H.monotone h⟩

Premises used: StrictMono.monotone, Iff.intro, Iff.mp, Valuation.IsEquiv, StrictMono.le_iff_le
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : LinearOrderedCommMonoidWithZero Γ'₀
v : Valuation R Γ₀
v' : Valuation R Γ'₀
simp :
  (∀ (r s : R),
      LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) s : Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) ↔
        LT.lt.{u_5} (α := Γ'₀) ((v' : (a : R) → Γ'₀) s : Γ'₀) ((v' : (a : R) → Γ'₀) r : Γ'₀)) ↔
    ∀ {x y : R},
      LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ↔
        LT.lt.{u_5} (α := Γ'₀) ((v' : (a : R) → Γ'₀) x : Γ'₀) ((v' : (a : R) → Γ'₀) y : Γ'₀)
⊢ v.IsEquiv v' ↔
    ∀ {x y : R},
      LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ↔
        LT.lt.{u_5} (α := Γ'₀) ((v' : (a : R) → Γ'₀) x : Γ'₀) ((v' : (a : R) → Γ'₀) y : Γ'₀)

Tactic:
simp only [IsEquiv, le_iff_le_iff_lt_iff_lt]

Premises used: le_iff_le_iff_lt_iff_lt, Valuation.IsEquiv