awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : Ring R
inst_2 : LinearOrderedCommMonoidWithZero Γ₀
inst_3 : LinearOrderedCommMonoidWithZero Γ'₀
inst_4 : LinearOrderedCommMonoidWithZero Γ''₀
g : Valuation R Γ₀
toFun : R → Γ₀
map_zero' : toFun 0 = 0
map_one' : { toFun := toFun, map_zero' := map_zero' : ZeroHom R Γ₀ }.toFun 1 = 1
map_mul' :
  ∀ (x y : R),
    { toFun := toFun, map_zero' := map_zero' : ZeroHom R Γ₀ }.toFun (x * y) =
      { toFun := toFun, map_zero' := map_zero' : ZeroHom R Γ₀ }.toFun x *
        { toFun := toFun, map_zero' := map_zero' : ZeroHom R Γ₀ }.toFun y
map_add_le_max' :
  ∀ (x y : R),
    (↑{ toFun := toFun, map_zero' := map_zero', map_one' := map_one', map_mul' := map_mul' : R →*₀ Γ₀ } :
            ZeroHom R Γ₀).toFun
        (x + y) ≤
      max
        ((↑{ toFun := toFun, map_zero' := map_zero', map_one' := map_one', map_mul' := map_mul' : R →*₀ Γ₀ } :
              ZeroHom R Γ₀).toFun
          x)
        ((↑{ toFun := toFun, map_zero' := map_zero', map_one' := map_one', map_mul' := map_mul' : R →*₀ Γ₀ } :
              ZeroHom R Γ₀).toFun
          y)
h :
  Eq (α := (a : R) → Γ₀)
    ((fun (f : Valuation R Γ₀) ↦ (↑f.toMonoidWithZeroHom : ZeroHom R Γ₀).toFun)
      { toFun := toFun, map_zero' := map_zero', map_one' := map_one', map_mul' := map_mul',
        map_add_le_max' := map_add_le_max' })
    ((fun (f : Valuation R Γ₀) ↦ (↑f.toMonoidWithZeroHom : ZeroHom R Γ₀).toFun) g)
⊢ { toFun := toFun, map_zero' := map_zero', map_one' := map_one', map_mul' := map_mul',
      map_add_le_max' := map_add_le_max' : Valuation R Γ₀ } =
    g

Tactic:
congr
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
f : R →*₀ Γ₀
h : ∀ (x y : R), (↑f : ZeroHom R Γ₀).toFun (x + y) ≤ max ((↑f : ZeroHom R Γ₀).toFun x) ((↑f : ZeroHom R Γ₀).toFun y)
⊢ Eq (α := (a : R) → Γ₀) (⇑{ toMonoidWithZeroHom := f, map_add_le_max' := h : Valuation R Γ₀ } : (a : R) → Γ₀)
    (⇑f : (a : R) → Γ₀)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
⊢ (↑v.toMonoidWithZeroHom : ZeroHom R Γ₀).toFun = (⇑v : (a : R) → Γ₀)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
⊢ Eq (α := (a : R) → Γ₀) (⇑v.toMonoidWithZeroHom : (a : R) → Γ₀) (⇑v : (a : R) → Γ₀)

Tactic:
rfl

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

Tactic:
DFunLike.ext _ _ h

Premises used: DFunLike.ext
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
⊢ Eq (α := (a : R) → Γ₀) (⇑(↑v : R →*₀ Γ₀) : (a : R) → Γ₀) (⇑v : (a : R) → Γ₀)

Tactic:
rfl

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

Tactic:
v.map_zero'

Premises used: ZeroHom.map_zero', MonoidWithZeroHom.toZeroHom, Valuation.toMonoidWithZeroHom
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) 1 : Γ₀) (1 : Γ₀)

Tactic:
v.map_one'

Premises used: MonoidWithZeroHom.map_one', Valuation.toMonoidWithZeroHom
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
⊢ ∀ (x y : R),
    (v : (a : R) → Γ₀) (x * y) = HMul.hMul (α := Γ₀) (β := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) ((v : (a : R) → Γ₀) y : Γ₀)

Tactic:
v.map_mul'

Premises used: Valuation.toMonoidWithZeroHom, MonoidWithZeroHom.map_mul'
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
⊢ ∀ (x y : R),
    LE.le.{u_4} (α := Γ₀) ((v : (a : R) → Γ₀) (x + y) : Γ₀) (max ((v : (a : R) → Γ₀) x) ((v : (a : R) → Γ₀) y) : Γ₀)

Tactic:
v.map_add_le_max'

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

Tactic:
rw [← le_max_iff]

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

Tactic:
apply v.map_add

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

Tactic:
le_trans (v.map_add x y) <| max_le hx hy

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

Tactic:
lt_of_le_of_lt (v.map_add x y) <| max_lt hx hy

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

Tactic:
Finset.induction_on s (fun _ => v.map_zero ▸ zero_le')
      (fun a s has ih hf => ?_) hf

Premises used: Finset.induction_on
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
ι : Type u_7
s : Finset ι
f : ι → R
g : Γ₀
hf : ∀ i ∈ s, (v : (a : R) → Γ₀) (f i) ≤ g
s₁ :
  ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
    (ih : (∀ i ∈ s, (v : (a : R) → Γ₀) (f i) ≤ g) → (v : (a : R) → Γ₀) (∑ i ∈ s, f i) ≤ g)
    (hf : ∀ i ∈ insert a s, (v : (a : R) → Γ₀) (f i) ≤ g), (v : (a : R) → Γ₀) (∑ i ∈ insert a s, f i) ≤ g
⊢ (v : (a : R) → Γ₀) (∑ i ∈ s, f i) ≤ g

Tactic:
refine
    Finset.induction_on s (fun _ => v.map_zero ▸ zero_le')
      (fun a s has ih hf => ?_) hf
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
ι : Type u_7
s_1 : Finset ι
f : ι → R
g : Γ₀
hf_1 : ∀ i ∈ s_1, (v : (a : R) → Γ₀) (f i) ≤ g
a : ι
s : Finset ι
has : a ∉ s
ih : (∀ i ∈ s, (v : (a : R) → Γ₀) (f i) ≤ g) → (v : (a : R) → Γ₀) (∑ i ∈ s, f i) ≤ g
hf : ∀ i ∈ insert a s, (v : (a : R) → Γ₀) (f i) ≤ g
⊢ (v : (a : R) → Γ₀) (f a) ≤ g ∧ ∀ x ∈ s, (v : (a : R) → Γ₀) (f x) ≤ g

Tactic:
rw [Finset.forall_mem_insert] at hf

Premises used: Finset.forall_mem_insert
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
ι : Type u_7
s_1 : Finset ι
f : ι → R
g : Γ₀
hf_1 : ∀ i ∈ s_1, (v : (a : R) → Γ₀) (f i) ≤ g
a : ι
s : Finset ι
has : a ∉ s
ih : (∀ i ∈ s, (v : (a : R) → Γ₀) (f i) ≤ g) → (v : (a : R) → Γ₀) (∑ i ∈ s, f i) ≤ g
hf : (v : (a : R) → Γ₀) (f a) ≤ g ∧ ∀ x ∈ s, (v : (a : R) → Γ₀) (f x) ≤ g
rw : (v : (a : R) → Γ₀) (f a + ∑ x ∈ s, f x) ≤ g
⊢ (v : (a : R) → Γ₀) (∑ i ∈ insert a s, f i) ≤ g

Tactic:
rw [Finset.sum_insert has]

Premises used: Finset.sum_insert
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
ι : Type u_7
s_1 : Finset ι
f : ι → R
g : Γ₀
hf_1 : ∀ i ∈ s_1, (v : (a : R) → Γ₀) (f i) ≤ g
a : ι
s : Finset ι
has : a ∉ s
ih : (∀ i ∈ s, (v : (a : R) → Γ₀) (f i) ≤ g) → (v : (a : R) → Γ₀) (∑ i ∈ s, f i) ≤ g
hf : (v : (a : R) → Γ₀) (f a) ≤ g ∧ ∀ x ∈ s, (v : (a : R) → Γ₀) (f x) ≤ g
⊢ (v : (a : R) → Γ₀) (f a + ∑ x ∈ s, f x) ≤ g

Tactic:
v.map_add_le hf.1 (ih hf.2)

Premises used: Valuation.map_add_le, And.right, And.left
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
ι : Type u_7
s_1 : Finset ι
f : ι → R
g : Γ₀
hf_1 : ∀ i ∈ s_1, (v : (a : R) → Γ₀) (f i) ≤ g
a : ι
s : Finset ι
has : a ∉ s
ih : (∀ i ∈ s, (v : (a : R) → Γ₀) (f i) ≤ g) → (v : (a : R) → Γ₀) (∑ i ∈ s, f i) ≤ g
hf : (v : (a : R) → Γ₀) (f a) ≤ g ∧ ∀ x ∈ s, (v : (a : R) → Γ₀) (f x) ≤ g
⊢ (v : (a : R) → Γ₀) (f a + ∑ x ∈ s, f x) ≤ g

Tactic:
exact v.map_add_le hf.1 (ih hf.2)

Premises used: Valuation.map_add_le, And.right, And.left
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
ι : Type u_7
s : Finset ι
f : ι → R
g : Γ₀
hf : ∀ i ∈ s, (v : (a : R) → Γ₀) (f i) ≤ g
s₁ :
  ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
    (ih : (∀ i ∈ s, (v : (a : R) → Γ₀) (f i) ≤ g) → (v : (a : R) → Γ₀) (∑ i ∈ s, f i) ≤ g)
    (hf : ∀ i ∈ insert a s, (v : (a : R) → Γ₀) (f i) ≤ g), (v : (a : R) → Γ₀) (∑ i ∈ insert a s, f i) ≤ g
s₂ s₃ :
  ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
    (ih : (∀ i ∈ s, (v : (a : R) → Γ₀) (f i) ≤ g) → (v : (a : R) → Γ₀) (∑ i ∈ s, f i) ≤ g)
    (hf : (v : (a : R) → Γ₀) (f a) ≤ g ∧ ∀ x ∈ s, (v : (a : R) → Γ₀) (f x) ≤ g),
    (v : (a : R) → Γ₀) (∑ i ∈ insert a s, f i) ≤ g
s₄ :
  ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
    (ih : (∀ i ∈ s, (v : (a : R) → Γ₀) (f i) ≤ g) → (v : (a : R) → Γ₀) (∑ i ∈ s, f i) ≤ g)
    (hf : (v : (a : R) → Γ₀) (f a) ≤ g ∧ ∀ x ∈ s, (v : (a : R) → Γ₀) (f x) ≤ g),
    (v : (a : R) → Γ₀) (f a + ∑ x ∈ s, f x) ≤ g
⊢ (v : (a : R) → Γ₀) (∑ i ∈ s, f i) ≤ g

Tactic:
classical
  refine
    Finset.induction_on s (fun _ => v.map_zero ▸ zero_le')
      (fun a s has ih hf => ?_) hf
  rw [Finset.forall_mem_insert] at hf; rw [Finset.sum_insert has]
  exact v.map_add_le hf.1 (ih hf.2)

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

Tactic:
Finset.induction_on s (fun _ => v.map_zero ▸ (zero_lt_iff.2 hg))
      (fun a s has ih hf => ?_) hf

Premises used: Finset.induction_on
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
ι : Type u_7
s : Finset ι
f : ι → R
g : Γ₀
hg : g ≠ 0
hf : ∀ i ∈ s, (v : (a : R) → Γ₀) (f i) < g
s₁ :
  ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
    (ih : (∀ i ∈ s, (v : (a : R) → Γ₀) (f i) < g) → (v : (a : R) → Γ₀) (∑ i ∈ s, f i) < g)
    (hf : ∀ i ∈ insert a s, (v : (a : R) → Γ₀) (f i) < g), (v : (a : R) → Γ₀) (∑ i ∈ insert a s, f i) < g
⊢ (v : (a : R) → Γ₀) (∑ i ∈ s, f i) < g

Tactic:
refine
    Finset.induction_on s (fun _ => v.map_zero ▸ (zero_lt_iff.2 hg))
      (fun a s has ih hf => ?_) hf
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
ι : Type u_7
s_1 : Finset ι
f : ι → R
g : Γ₀
hg : g ≠ 0
hf_1 : ∀ i ∈ s_1, (v : (a : R) → Γ₀) (f i) < g
a : ι
s : Finset ι
has : a ∉ s
ih : (∀ i ∈ s, (v : (a : R) → Γ₀) (f i) < g) → (v : (a : R) → Γ₀) (∑ i ∈ s, f i) < g
hf : ∀ i ∈ insert a s, (v : (a : R) → Γ₀) (f i) < g
⊢ (v : (a : R) → Γ₀) (f a) < g ∧ ∀ x ∈ s, (v : (a : R) → Γ₀) (f x) < g

Tactic:
rw [Finset.forall_mem_insert] at hf

Premises used: Finset.forall_mem_insert
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
ι : Type u_7
s_1 : Finset ι
f : ι → R
g : Γ₀
hg : g ≠ 0
hf_1 : ∀ i ∈ s_1, (v : (a : R) → Γ₀) (f i) < g
a : ι
s : Finset ι
has : a ∉ s
ih : (∀ i ∈ s, (v : (a : R) → Γ₀) (f i) < g) → (v : (a : R) → Γ₀) (∑ i ∈ s, f i) < g
hf : (v : (a : R) → Γ₀) (f a) < g ∧ ∀ x ∈ s, (v : (a : R) → Γ₀) (f x) < g
rw : (v : (a : R) → Γ₀) (f a + ∑ x ∈ s, f x) < g
⊢ (v : (a : R) → Γ₀) (∑ i ∈ insert a s, f i) < g

Tactic:
rw [Finset.sum_insert has]

Premises used: Finset.sum_insert
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
ι : Type u_7
s_1 : Finset ι
f : ι → R
g : Γ₀
hg : g ≠ 0
hf_1 : ∀ i ∈ s_1, (v : (a : R) → Γ₀) (f i) < g
a : ι
s : Finset ι
has : a ∉ s
ih : (∀ i ∈ s, (v : (a : R) → Γ₀) (f i) < g) → (v : (a : R) → Γ₀) (∑ i ∈ s, f i) < g
hf : (v : (a : R) → Γ₀) (f a) < g ∧ ∀ x ∈ s, (v : (a : R) → Γ₀) (f x) < g
⊢ (v : (a : R) → Γ₀) (f a + ∑ x ∈ s, f x) < g

Tactic:
v.map_add_lt hf.1 (ih hf.2)

Premises used: Valuation.map_add_lt, And.right, And.left
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
ι : Type u_7
s_1 : Finset ι
f : ι → R
g : Γ₀
hg : g ≠ 0
hf_1 : ∀ i ∈ s_1, (v : (a : R) → Γ₀) (f i) < g
a : ι
s : Finset ι
has : a ∉ s
ih : (∀ i ∈ s, (v : (a : R) → Γ₀) (f i) < g) → (v : (a : R) → Γ₀) (∑ i ∈ s, f i) < g
hf : (v : (a : R) → Γ₀) (f a) < g ∧ ∀ x ∈ s, (v : (a : R) → Γ₀) (f x) < g
⊢ (v : (a : R) → Γ₀) (f a + ∑ x ∈ s, f x) < g

Tactic:
exact v.map_add_lt hf.1 (ih hf.2)

Premises used: Valuation.map_add_lt, And.right, And.left
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
ι : Type u_7
s : Finset ι
f : ι → R
g : Γ₀
hg : g ≠ 0
hf : ∀ i ∈ s, (v : (a : R) → Γ₀) (f i) < g
s₁ :
  ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
    (ih : (∀ i ∈ s, (v : (a : R) → Γ₀) (f i) < g) → (v : (a : R) → Γ₀) (∑ i ∈ s, f i) < g)
    (hf : ∀ i ∈ insert a s, (v : (a : R) → Γ₀) (f i) < g), (v : (a : R) → Γ₀) (∑ i ∈ insert a s, f i) < g
s₂ s₃ :
  ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
    (ih : (∀ i ∈ s, (v : (a : R) → Γ₀) (f i) < g) → (v : (a : R) → Γ₀) (∑ i ∈ s, f i) < g)
    (hf : (v : (a : R) → Γ₀) (f a) < g ∧ ∀ x ∈ s, (v : (a : R) → Γ₀) (f x) < g),
    (v : (a : R) → Γ₀) (∑ i ∈ insert a s, f i) < g
s₄ :
  ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
    (ih : (∀ i ∈ s, (v : (a : R) → Γ₀) (f i) < g) → (v : (a : R) → Γ₀) (∑ i ∈ s, f i) < g)
    (hf : (v : (a : R) → Γ₀) (f a) < g ∧ ∀ x ∈ s, (v : (a : R) → Γ₀) (f x) < g),
    (v : (a : R) → Γ₀) (f a + ∑ x ∈ s, f x) < g
⊢ (v : (a : R) → Γ₀) (∑ i ∈ s, f i) < g

Tactic:
classical
  refine
    Finset.induction_on s (fun _ => v.map_zero ▸ (zero_lt_iff.2 hg))
      (fun a s has ih hf => ?_) hf
  rw [Finset.forall_mem_insert] at hf; rw [Finset.sum_insert has]
  exact v.map_add_lt hf.1 (ih hf.2)

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

Tactic:
v.map_sum_lt (ne_of_gt hg) hf

Premises used: ne_of_gt, Valuation.map_sum_lt
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
⊢ ∀ (x : R) (n : ℕ), (v : (a : R) → Γ₀) (x ^ n) = HPow.hPow (α := Γ₀) ((v : (a : R) → Γ₀) x : Γ₀) n

Tactic:
v.toMonoidWithZeroHom.toMonoidHom.map_pow

Premises used: Valuation.toMonoidWithZeroHom, MonoidWithZeroHom.toMonoidHom, MonoidHom.map_pow
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_4
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : Nontrivial Γ₀
v : Valuation K Γ₀
x : K
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀) ↔ x = 0

Tactic:
map_eq_zero v

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

Tactic:
map_ne_zero v

Premises used: map_ne_zero
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_4
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : Nontrivial Γ₀
v : Valuation K Γ₀
x : K
rw : Ne.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀) ↔ x ≠ 0
rw₁ rw₂ : x ≠ 0 ↔ x ≠ 0
⊢ LT.lt.{u_4} (α := Γ₀) (0 : Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) ↔ x ≠ 0

Tactic:
rw [zero_lt_iff, ne_zero_iff]

Premises used: Valuation.ne_zero_iff, zero_lt_iff
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
u : Rˣ
⊢ Eq.{u_4 + 1} (α := Γ₀) ((↑(((Units.map (↑v : R →* Γ₀) : MonoidHom.{u_3, u_4} Rˣ Γ₀ˣ) : (a : Rˣ) → Γ₀ˣ) u) : Γ₀) : Γ₀)
    ((v : (a : R) → Γ₀) (↑u : R) : Γ₀)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_4
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : Nontrivial Γ₀
v : Valuation K Γ₀
x : Kˣ
⊢ Ne.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) (↑x : K) : Γ₀) (0 : Γ₀)

Tactic:
simp only [ne_eq, Valuation.zero_iff, Units.ne_zero x, not_false_iff]

Premises used: Units.ne_zero, Valuation.zero_iff, ne_eq, not_false_iff
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
K : Type u_1
inst : DivisionRing K
Γ₀ : Type u_4
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
inst_2 : Nontrivial Γ₀
v : Valuation K Γ₀
x : K
hx : IsUnit x
⊢ Ne.{u_4 + 1} (α := Γ₀) ((v : (a : K) → Γ₀) x : Γ₀) (0 : Γ₀)

Tactic:
simpa [hx.choose_spec] using ne_zero_of_unit v hx.choose

Premises used: Exists.choose_spec, Valuation.ne_zero_of_unit, Exists.choose
-- 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 : Ring R
inst_2 : LinearOrderedCommMonoidWithZero Γ₀
inst_3 : LinearOrderedCommMonoidWithZero Γ'₀
inst_4 : LinearOrderedCommMonoidWithZero Γ''₀
v_1 : Valuation R Γ₀
S : Type u_7
inst_5 : Ring S
f : S →+* R
v : Valuation R Γ₀
x y : S
⊢ LE.le.{u_4} (α := Γ₀) (comp.{u_7 + 1, u_3 + 1, u_4 + 1} (β := R) (⇑v : (a : R) → Γ₀) (⇑f : (a : S) → R) (x + y))
    (max (comp.{u_7 + 1, u_3 + 1, u_4 + 1} (β := R) (⇑v : (a : R) → Γ₀) (⇑f : (a : S) → R) x)
      (comp.{u_7 + 1, u_3 + 1, u_4 + 1} (β := R) (⇑v : (a : R) → Γ₀) (⇑f : (a : S) → R) y))

Tactic:
simp
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
S : Type u_7
inst_2 : Ring S
f : S →+* R
v : Valuation R Γ₀
s : S
⊢ Eq.{u_4 + 1} (α := Γ₀) ((comap f v : (a : S) → Γ₀) s : Γ₀) ((v : (a : R) → Γ₀) ((f : (a : S) → R) s : R) : Γ₀)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
⊢ comap (RingHom.id R) v = v

Tactic:
ext fun _r => rfl

Premises used: Valuation.ext, rfl
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
S₁ : Type u_7
S₂ : Type u_8
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:
ext fun _r => rfl

Premises used: Valuation.ext, 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 Γ'₀
f : Γ₀ →*₀ Γ'₀
hf : Monotone.{u_4, u_5} (α := Γ₀) (β := Γ'₀) (⇑f : (a : Γ₀) → Γ'₀)
v : Valuation R Γ₀
r : R
⊢ Eq.{u_5 + 1} (α := Γ'₀) ((map f 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 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x : R
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (-x) : Γ₀) ((v : (a : R) → Γ₀) x : Γ₀)

Tactic:
v.toMonoidWithZeroHom.toMonoidHom.map_neg x

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

Tactic:
v.toMonoidWithZeroHom.toMonoidHom.map_sub_swap x y

Premises used: MonoidHom.map_sub_swap, Valuation.toMonoidWithZeroHom, MonoidWithZeroHom.toMonoidHom
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
rw rw₁ : Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x + -y) : Γ₀) ((v : (a : R) → Γ₀) (x + -y) : Γ₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) ((v : (a : R) → Γ₀) (x - y) : Γ₀) ((v : (a : R) → Γ₀) (x + -y) : Γ₀)

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 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
rw rw₁ :
  Eq.{u_4 + 1} (α := Γ₀) (max ((v : (a : R) → Γ₀) x) ((v : (a : R) → Γ₀) y) : Γ₀)
    (max ((v : (a : R) → Γ₀) x) ((v : (a : R) → Γ₀) y) : Γ₀)
⊢ Eq.{u_4 + 1} (α := Γ₀) (max ((v : (a : R) → Γ₀) x) ((v : (a : R) → Γ₀) (-y)) : Γ₀)
    (max ((v : (a : R) → Γ₀) x) ((v : (a : R) → Γ₀) y) : Γ₀)

Tactic:
rw [map_neg]

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

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 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
g : Γ₀
hx : (v : (a : R) → Γ₀) x ≤ g
hy : (v : (a : R) → Γ₀) y ≤ g
⊢ (v : (a : R) → Γ₀) (x + -y) ≤ g

Tactic:
v.map_add_le hx <| (v.map_neg y).trans_le hy

Premises used: Valuation.map_add_le, Eq.trans_le, Valuation.map_neg
-- Module: Mathlib.RingTheory.Valuation.Basic
Goal:
R : Type u_3
Γ₀ : Type u_4
inst : Ring R
inst_1 : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
x y : R
g : Γ₀
hx : (v : (a : R) → Γ₀) x ≤ g
hy : (v : (a : R) → Γ₀) y ≤ g
⊢ (v : (a : R) → Γ₀) (x + -y) ≤ g

Tactic:
exact v.map_add_le hx <| (v.map_neg y).trans_le hy

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

Tactic:
rw [sub_eq_add_neg]

Premises used: sub_eq_add_neg