awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀
⊢ Eq (α := AddValuation R Γ₀ ≃ Valuation.{u_3, u_4} R (Multiplicative Γ₀ᵒᵈ)) (Equiv.symm ofValuation) toValuation

Tactic:
rfl

Premises used: AddValuation.toValuation, AddValuation, Equiv.symm, Equiv.refl, rfl
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀
⊢ Eq (α := Valuation.{u_3, u_4} R (Multiplicative Γ₀ᵒᵈ) ≃ AddValuation R Γ₀) (Equiv.symm toValuation) ofValuation

Tactic:
rfl

Premises used: AddValuation.ofValuation, AddValuation, Equiv.symm, Equiv.refl, rfl
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀
v : AddValuation R Γ₀
⊢ (ofValuation : (a : Valuation R (Multiplicative Γ₀ᵒᵈ)) → AddValuation R Γ₀)
      ((toValuation : (a : AddValuation R Γ₀) → Valuation R (Multiplicative Γ₀ᵒᵈ)) v) =
    v

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀
v : Valuation.{u_3, u_4} R (Multiplicative Γ₀ᵒᵈ)
⊢ (toValuation : (a : AddValuation R Γ₀) → Valuation R (Multiplicative Γ₀ᵒᵈ))
      ((ofValuation : (a : Valuation R (Multiplicative Γ₀ᵒᵈ)) → AddValuation R Γ₀) v) =
    v

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀
v : AddValuation R Γ₀
r : R
⊢ Eq.{u_4 + 1} (α := Multiplicative Γ₀ᵒᵈ)
    ((((toValuation : (a : AddValuation R Γ₀) → Valuation R (Multiplicative Γ₀ᵒᵈ)) v :
            Valuation.{u_3, u_4} R (Multiplicative Γ₀ᵒᵈ)) :
          (a : R) → Multiplicative Γ₀ᵒᵈ)
        r :
      Multiplicative Γ₀ᵒᵈ)
    ((Multiplicative.ofAdd : (a : Γ₀ᵒᵈ) → Multiplicative Γ₀ᵒᵈ)
        ((OrderDual.toDual : (a : Γ₀) → Γ₀ᵒᵈ) ((v : (a : R) → Γ₀) r : Γ₀) : Γ₀ᵒᵈ) :
      Multiplicative Γ₀ᵒᵈ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀
v : Valuation.{u_3, u_4} R (Multiplicative Γ₀ᵒᵈ)
r : R
⊢ Eq.{u_4 + 1} (α := Γ₀)
    ((((ofValuation : (a : Valuation R (Multiplicative Γ₀ᵒᵈ)) → AddValuation R Γ₀) v : AddValuation R Γ₀) :
          (a : R) → Γ₀)
        r :
      Γ₀)
    ((OrderDual.ofDual : (a : Γ₀ᵒᵈ) → Γ₀)
        ((Multiplicative.toAdd : (a : Multiplicative Γ₀ᵒᵈ) → Γ₀ᵒᵈ)
            ((v : (a : R) → Multiplicative Γ₀ᵒᵈ) r : Multiplicative Γ₀ᵒᵈ) :
          Γ₀ᵒᵈ) :
      Γ₀)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀
v : AddValuation R Γ₀
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) 0 : Γ₀) ⊤

Tactic:
Valuation.map_zero v

Premises used: Multiplicative, OrderDual, Valuation.map_zero
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀
v : AddValuation R Γ₀
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) 1 : Γ₀) 0

Tactic:
Valuation.map_one v

Premises used: Valuation.map_one, Multiplicative, OrderDual
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀
v : AddValuation R Γ₀
⊢ ∀ (x y : R),
    (v : (a : R) → Γ₀) (x * y) = HAdd.hAdd (α := Γ₀) (β := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)

Tactic:
Valuation.map_mul v

Premises used: Valuation.map_mul, Multiplicative, OrderDual
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀
v : AddValuation R Γ₀
⊢ ∀ (x y : R),
    LE.le.{u_4} (α := Γ₀) (min ((v : (a : R) → Γ₀) x) ((v : (a : R) → Γ₀) y) : Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀)

Tactic:
Valuation.map_add v

Premises used: Valuation.map_add
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀
v : AddValuation R Γ₀
x y : R
rw : LE.le.{u_4} (α := Γ₀) (min ((v : (a : R) → Γ₀) x) ((v : (a : R) → Γ₀) y) : Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀)
⊢ LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) ∨
    LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀)

Tactic:
rw [← min_le_iff]

Premises used: min_le_iff
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀
v : AddValuation R Γ₀
x y : R
⊢ LE.le.{u_4} (α := Γ₀) (min ((v : (a : R) → Γ₀) x) ((v : (a : R) → Γ₀) y) : Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀)

Tactic:
apply map_add

Premises used: AddValuation.map_add
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀
v : AddValuation R Γ₀
x y : R
g : Γ₀
hx : g ≤ (v : (a : R) → Γ₀) x
hy : g ≤ (v : (a : R) → Γ₀) y
⊢ g ≤ (v : (a : R) → Γ₀) (x + y)

Tactic:
Valuation.map_add_le v hx hy

Premises used: Valuation.map_add_le
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀
v : AddValuation R Γ₀
x y : R
g : Γ₀
hx : g < (v : (a : R) → Γ₀) x
hy : g < (v : (a : R) → Γ₀) y
⊢ g < (v : (a : R) → Γ₀) (x + y)

Tactic:
Valuation.map_add_lt v hx hy

Premises used: Valuation.map_add_lt
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀
v : AddValuation R Γ₀
ι : Type u_6
s : Finset ι
f : ι → R
g : Γ₀
hf : ∀ i ∈ s, g ≤ (v : (a : R) → Γ₀) (f i)
⊢ g ≤ (v : (a : R) → Γ₀) (∑ i ∈ s, f i)

Tactic:
v.map_sum_le hf

Premises used: Valuation.map_sum_le
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀
v : AddValuation R Γ₀
ι : Type u_6
s : Finset ι
f : ι → R
g : Γ₀
hg : g ≠ ⊤
hf : ∀ i ∈ s, g < (v : (a : R) → Γ₀) (f i)
⊢ g < (v : (a : R) → Γ₀) (∑ i ∈ s, f i)

Tactic:
v.map_sum_lt hg hf

Premises used: Valuation.map_sum_lt
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀
v : AddValuation R Γ₀
ι : Type u_6
s : Finset ι
f : ι → R
g : Γ₀
hg : g < ⊤
hf : ∀ i ∈ s, g < (v : (a : R) → Γ₀) (f i)
⊢ g < (v : (a : R) → Γ₀) (∑ i ∈ s, f i)

Tactic:
v.map_sum_lt' hg hf

Premises used: Valuation.map_sum_lt'
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀
v : AddValuation R Γ₀
⊢ ∀ (x : R) (n : ℕ), (v : (a : R) → Γ₀) (x ^ n) = HSMul.hSMul (β := Γ₀) n ((v : (a : R) → Γ₀) x : Γ₀)

Tactic:
Valuation.map_pow v

Premises used: Multiplicative, Valuation.map_pow, OrderDual
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀
v₁ v₂ : AddValuation R Γ₀
h : ∀ (r : R), Eq.{u_4 + 1} (α := Γ₀) ((v₁ : (a : R) → Γ₀) r : Γ₀) ((v₂ : (a : R) → Γ₀) r : Γ₀)
⊢ v₁ = v₂

Tactic:
Valuation.ext h

Premises used: AddValuation, Valuation.ext
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_4
inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀
inst_2 : Nontrivial Γ₀
v : AddValuation K Γ₀
x : K
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (⊤ : Γ₀) ↔ x = 0

Tactic:
v.zero_iff

Premises used: Valuation.zero_iff, Multiplicative, OrderDual
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_4
inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀
inst_2 : Nontrivial Γ₀
v : AddValuation K Γ₀
x : K
⊢ Ne.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (⊤ : Γ₀) ↔ x ≠ 0

Tactic:
v.ne_zero_iff

Premises used: Valuation.ne_zero_iff, Multiplicative, OrderDual
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀
v : AddValuation R Γ₀
⊢ comap (RingHom.id R) v = v

Tactic:
Valuation.comap_id v

Premises used: AddValuation.comap, Valuation.comap_id, AddValuation
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀
v : AddValuation R Γ₀
S₁ : Type u_6
S₂ : Type u_7
inst_2 : Ring S₁
inst_3 : Ring S₂
f : S₁ →+* S₂
g : S₂ →+* R
⊢ comap (g.comp f) v = comap f (comap g v)

Tactic:
Valuation.comap_comp v f g

Premises used: AddValuation.comap, Valuation.comap_comp, AddValuation
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : Ring R
inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀
inst_2 : LinearOrderedAddCommMonoidWithTop Γ'₀
f : Γ₀ →+ Γ'₀
ht : Eq.{u_5 + 1} (α := Γ'₀) ((f : (a : Γ₀) → Γ'₀) ⊤ : Γ'₀) (⊤ : Γ'₀)
hf : Monotone.{u_4, u_5} (α := Γ₀) (β := Γ'₀) (⇑f : (a : Γ₀) → Γ'₀)
v : AddValuation R Γ₀
r : R
⊢ Eq.{u_5 + 1} (α := Γ'₀) ((map f ht hf v : (a : R) → Γ'₀) r : Γ'₀)
    ((f : (a : Γ₀) → Γ'₀) ((v : (a : R) → Γ₀) r : Γ₀) : Γ'₀)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀
v : AddValuation R Γ₀
x : R
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (-x) : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)

Tactic:
Valuation.map_neg v x

Premises used: Multiplicative, Valuation.map_neg, OrderDual
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀
v : AddValuation R Γ₀
x y : R
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x - y) : Γ₀) ((v : (a : R) → Γ₀) (y - x) : Γ₀)

Tactic:
Valuation.map_sub_swap v x y

Premises used: Valuation.map_sub_swap, Multiplicative, OrderDual
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀
v : AddValuation R Γ₀
x y : R
⊢ LE.le.{u_4} (α := Γ₀) (min ((v : (a : R) → Γ₀) x) ((v : (a : R) → Γ₀) y) : Γ₀) ((v : (a : R) → Γ₀) (x - y) : Γ₀)

Tactic:
Valuation.map_sub v x y

Premises used: Valuation.map_sub
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀
v : AddValuation R Γ₀
x y : R
g : Γ₀
hx : g ≤ (v : (a : R) → Γ₀) x
hy : g ≤ (v : (a : R) → Γ₀) y
⊢ g ≤ (v : (a : R) → Γ₀) (x - y)

Tactic:
Valuation.map_sub_le v hx hy

Premises used: Valuation.map_sub_le
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀
v : AddValuation R Γ₀
x y : R
h : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) (min ((v : (a : R) → Γ₀) x) ((v : (a : R) → Γ₀) y) : Γ₀)

Tactic:
Valuation.map_add_of_distinct_val v h

Premises used: Valuation.map_add_of_distinct_val, Multiplicative, OrderDual
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀
v : AddValuation R Γ₀
x y : R
h : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
rw : Eq.{u_4 + 1} (α := Γ₀) (min ((v : (a : R) → Γ₀) x) ((v : (a : R) → Γ₀) y) : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
rw₁ rw₂ : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)

Tactic:
rw [map_add_of_distinct_val _ h.ne, min_eq_left h.le]

Premises used: AddValuation.map_add_of_distinct_val, LT.lt.le, min_eq_left, LT.lt.ne
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀
v : AddValuation R Γ₀
x y : R
hx : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)

Tactic:
add_comm y x ▸ map_add_eq_of_lt_left v hx

Premises used: Eq.rec, add_comm, AddValuation.map_add_eq_of_lt_left
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀
v : AddValuation R Γ₀
x y : R
hx : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
rw : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x + -y) : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x - y) : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)

Tactic:
rw [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀
v : AddValuation R Γ₀
x y : R
hx : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
h : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) (-y) : Γ₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x + -y) : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)

Tactic:
apply map_add_eq_of_lt_left

Premises used: AddValuation.map_add_eq_of_lt_left
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀
v : AddValuation R Γ₀
x y : R
hx h h₁ h₂ h₃ : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)
⊢ LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) (-y) : Γ₀)

Tactic:
rwa [map_neg]

Premises used: AddValuation.map_neg
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀
v : AddValuation R Γ₀
x y : R
hx : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x - y) : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)

Tactic:
map_sub_swap v x y ▸ map_sub_eq_of_lt_left v hx

Premises used: AddValuation.map_sub_swap, Eq.rec, AddValuation.map_sub_eq_of_lt_left, Eq.symm
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀
v : AddValuation R Γ₀
x y : R
h : LT.lt.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) (y - x) : Γ₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) y : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)

Tactic:
Valuation.map_eq_of_sub_lt v h

Premises used: Multiplicative, Valuation.map_eq_of_sub_lt, OrderDual
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_4
inst_1 : LinearOrderedAddCommGroupWithTop Γ₀
v : AddValuation K Γ₀
x : K
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x⁻¹ : Γ₀) (-(v : (a : K) → Γ₀) x : Γ₀)

Tactic:
map_inv₀ (toValuation v) x

Premises used: AddValuation.toValuation, map_inv₀, Multiplicative, OrderDual, DFunLike.coe
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_4
inst_1 : LinearOrderedAddCommGroupWithTop Γ₀
v : AddValuation K Γ₀
x y : K
⊢ (v : (a : K) → Γ₀) (x / y) = HSub.hSub (α := Γ₀) (β := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ((v : (a : K) → Γ₀) y : Γ₀)

Tactic:
map_div₀ (toValuation v) x y

Premises used: AddValuation.toValuation, Multiplicative, map_div₀, OrderDual, DFunLike.coe
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : LinearOrderedAddCommMonoidWithTop Γ₀
inst_1 : Ring R
v : AddValuation R Γ₀
⊢ v.IsEquiv v

Tactic:
Valuation.IsEquiv.refl

Premises used: AddValuation.IsEquiv, Valuation.IsEquiv.refl
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : LinearOrderedAddCommMonoidWithTop Γ₀
inst_1 : LinearOrderedAddCommMonoidWithTop Γ'₀
inst_2 : Ring R
v₁ : AddValuation R Γ₀
v₂ : AddValuation R Γ'₀
h : v₁.IsEquiv v₂
⊢ v₂.IsEquiv v₁

Tactic:
Valuation.IsEquiv.symm h

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

Tactic:
Valuation.IsEquiv.trans h₁₂ h₂₃

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

Tactic:
Valuation.IsEquiv.of_eq h

Premises used: AddValuation.IsEquiv, Valuation.IsEquiv.of_eq
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : LinearOrderedAddCommMonoidWithTop Γ₀
inst_1 : LinearOrderedAddCommMonoidWithTop Γ'₀
inst_2 : Ring R
v v' : AddValuation R Γ₀
f : Γ₀ →+ Γ'₀
ht : Eq.{u_5 + 1} (α := Γ'₀) ((f : (a : Γ₀) → Γ'₀) ⊤ : Γ'₀) (⊤ : Γ'₀)
hf : Monotone.{u_4, u_5} (α := Γ₀) (β := Γ'₀) (⇑f : (a : Γ₀) → Γ'₀)
inf : Injective.{u_4 + 1, u_5 + 1} (α := Γ₀) (β := Γ'₀) (⇑f : (a : Γ₀) → Γ'₀)
h : v.IsEquiv v'
⊢ (AddValuation.map f ht hf v).IsEquiv (AddValuation.map f ht hf v')

Tactic:
@Valuation.IsEquiv.map R (Multiplicative Γ₀ᵒᵈ) (Multiplicative Γ'₀ᵒᵈ) _ _ _ _ _
    { toFun := f
      map_mul' := f.map_add
      map_one' := f.map_zero
      map_zero' := ht } (fun _x _y h => hf h) inf h

Premises used: Valuation.IsEquiv.map, AddMonoidHom.map_zero, ZeroHom.mk, AddValuation.IsEquiv, AddValuation.map, AddMonoidHom.map_add, DFunLike.coe, MonoidWithZeroHom.mk
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : LinearOrderedAddCommMonoidWithTop Γ₀
inst_1 : LinearOrderedAddCommMonoidWithTop Γ'₀
inst_2 : Ring R
v₁ : AddValuation R Γ₀
v₂ : AddValuation R Γ'₀
S : Type u_7
inst_3 : Ring S
f : S →+* R
h : v₁.IsEquiv v₂
⊢ (AddValuation.comap f v₁).IsEquiv (AddValuation.comap f v₂)

Tactic:
Valuation.IsEquiv.comap f h

Premises used: AddValuation.comap, AddValuation.IsEquiv, Valuation.IsEquiv.comap
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
Γ'₀ : Type u_5
inst : LinearOrderedAddCommMonoidWithTop Γ₀
inst_1 : LinearOrderedAddCommMonoidWithTop Γ'₀
inst_2 : Ring R
v₁ : AddValuation R Γ₀
v₂ : AddValuation 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:
Valuation.IsEquiv.eq_iff h

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

Tactic:
(Valuation.IsEquiv.eq_zero h).ne

Premises used: Multiplicative, Valuation.IsEquiv.eq_zero, Iff.ne, OrderDual
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : LinearOrderedAddCommMonoidWithTop Γ₀
inst_1 : CommRing R
v : AddValuation R Γ₀
x : R
⊢ x ∈ v.supp ↔ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) (⊤ : Γ₀)

Tactic:
Valuation.mem_supp_iff v x

Premises used: Valuation.mem_supp_iff, Set.Mem, Multiplicative, OrderDual
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : LinearOrderedAddCommMonoidWithTop Γ₀
inst_1 : CommRing R
v : AddValuation R Γ₀
a s : R
h : s ∈ v.supp
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (a + s) : Γ₀) ((v : (a : R) → Γ₀) a : Γ₀)

Tactic:
Valuation.map_add_supp v a h

Premises used: Multiplicative, OrderDual, Valuation.map_add_supp
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_5
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
⊢ Eq (α := Valuation R Γ₀ ≃ AddValuation.{u_3, u_5} R (Additive Γ₀)ᵒᵈ) (Equiv.symm ofAddValuation) toAddValuation

Tactic:
rfl

Premises used: Equiv.trans, Valuation.toAddValuation, Equiv.symm, rfl, Valuation.map
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_5
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
⊢ Eq (α := AddValuation.{u_3, u_5} R (Additive Γ₀)ᵒᵈ ≃ Valuation R Γ₀) (Equiv.symm toAddValuation) ofAddValuation

Tactic:
rfl

Premises used: Equiv.trans, Valuation.ofAddValuation, Equiv.symm, rfl, Valuation.map
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_5
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
⊢ (ofAddValuation : (a : AddValuation R (Additive Γ₀)ᵒᵈ) → Valuation R Γ₀)
      ((toAddValuation : (a : Valuation R Γ₀) → AddValuation R (Additive Γ₀)ᵒᵈ) v) =
    v

Tactic:
rfl

Premises used: rfl, Valuation.map
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_5
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : AddValuation.{u_3, u_5} R (Additive Γ₀)ᵒᵈ
⊢ (toAddValuation : (a : Valuation R Γ₀) → AddValuation R (Additive Γ₀)ᵒᵈ)
      ((ofAddValuation : (a : AddValuation R (Additive Γ₀)ᵒᵈ) → Valuation R Γ₀) v) =
    v

Tactic:
rfl

Premises used: AddValuation, rfl, Valuation.map
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_5
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
r : R
⊢ Eq.{u_5 + 1} (α := (Additive Γ₀)ᵒᵈ)
    ((((toAddValuation : (a : Valuation R Γ₀) → AddValuation R (Additive Γ₀)ᵒᵈ) v :
            AddValuation.{u_3, u_5} R (Additive Γ₀)ᵒᵈ) :
          (a : R) → (Additive Γ₀)ᵒᵈ)
        r :
      (Additive Γ₀)ᵒᵈ)
    ((OrderDual.toDual : (a : Additive Γ₀) → (Additive Γ₀)ᵒᵈ)
        ((Additive.ofMul : (a : Γ₀) → Additive Γ₀) ((v : (a : R) → Γ₀) r : Γ₀) : Additive Γ₀) :
      (Additive Γ₀)ᵒᵈ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_5
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : AddValuation.{u_3, u_5} R (Additive Γ₀)ᵒᵈ
r : R
⊢ Eq.{u_5 + 1} (α := Γ₀)
    ((((ofAddValuation : (a : AddValuation R (Additive Γ₀)ᵒᵈ) → Valuation R Γ₀) v : Valuation R Γ₀) : (a : R) → Γ₀) r :
      Γ₀)
    ((Additive.toMul : (a : Additive Γ₀) → Γ₀)
        ((OrderDual.ofDual : (a : (Additive Γ₀)ᵒᵈ) → Additive Γ₀)
            ((v : (a : R) → (Additive Γ₀)ᵒᵈ) r : (Additive Γ₀)ᵒᵈ) :
          Additive Γ₀) :
      Γ₀)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_5
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
⊢ Eq.{u_5 + 1} (α := Γ₀) (↑0 : Γ₀) 0

Tactic:
rfl
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : Ring A
v : Valuation A Γ
inst_2 : v.IsRankOneDiscrete
⊢ ∃ (γ : Γˣ), zpowers γ = valueGroup v ∧ γ < 1

Tactic:
exists_generator_lt_one'

Premises used: Valuation.IsRankOneDiscrete.exists_generator_lt_one'
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : Ring A
v : Valuation A Γ
inst_2 : v.IsRankOneDiscrete
⊢ zpowers (generator v) = valueGroup v

Tactic:
(exists_generator_lt_one v).choose_spec.1

Premises used: Exists.choose_spec, And.left, Valuation.IsRankOneDiscrete.exists_generator_lt_one, Valuation.IsRankOneDiscrete.generator
-- Module: Mathlib.RingTheory.Valuation.Discrete.Basic
Goal:
Γ : Type u_1
inst : LinearOrderedCommGroupWithZero Γ
A : Type u_2
inst_1 : Ring A
v : Valuation A Γ
inst_2 : v.IsRankOneDiscrete
rw : Membership.mem (γ := Subgroup Γˣ) (zpowers (generator v)) (generator v)
⊢ Membership.mem (γ := Subgroup Γˣ) (valueGroup v) (generator v)

Tactic:
rw [← IsRankOneDiscrete.generator_zpowers_eq_valueGroup]

Premises used: Valuation.IsRankOneDiscrete.generator_zpowers_eq_valueGroup