K : Type ?u.668108
F : Type ?u.668111
R : Type u_3
inst✝⁴ : DivisionRing K
Γ₀ : Type u_2
Γ'₀ : Type ?u.668123
Γ''₀ : Type ?u.668126
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v : Valuation R Γ₀
x y z : R
ι : Type u_1
s✝ : Finset ι
f : ι → R
g : Γ₀
hg : g ≠ 0
hf✝ : ∀ (i : ι), i ∈ s✝ → ↑v (f i) < g
a : ι
s : Finset ι
has : ¬a ∈ s
ih : (∀ (i : ι), i ∈ s → ↑v (f i) < g) → ↑v (∑ i in s, f i) < g
hf : ∀ (i : ι), i ∈ insert a s → ↑v (f i) < g
⊢ ↑v (∑ i in insert a s, f i) < g
K : Type ?u.668108
F : Type ?u.668111
R : Type u_3
inst✝⁴ : DivisionRing K
Γ₀ : Type u_2
Γ'₀ : Type ?u.668123
Γ''₀ : Type ?u.668126
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v : Valuation R Γ₀
x y z : R
ι : Type u_1
s : Finset ι
f : ι → R
g : Γ₀
hg : g ≠ 0
hf : ∀ (i : ι), i ∈ s → ↑v (f i) < g
⊢ ↑v (∑ i in s, f i) < g
refine'
  Finset.induction_on s (fun _ => v.map_zero ▸ (zero_lt_iff.2 hg))
    (fun a s has ih hf => _) hf
K : Type ?u.668108
F : Type ?u.668111
R : Type u_3
inst✝⁴ : DivisionRing K
Γ₀ : Type u_2
Γ'₀ : Type ?u.668123
Γ''₀ : Type ?u.668126
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v : Valuation R Γ₀
x y z : R
ι : Type u_1
s✝ : Finset ι
f : ι → R
g : Γ₀
hg : g ≠ 0
hf✝ : ∀ (i : ι), i ∈ s✝ → ↑v (f i) < g
a : ι
s : Finset ι
has : ¬a ∈ s
ih : (∀ (i : ι), i ∈ s → ↑v (f i) < g) → ↑v (∑ i in s, f i) < g
hf : ↑v (f a) < g ∧ ∀ (x : ι), x ∈ s → ↑v (f x) < g
⊢ ↑v (∑ i in insert a s, f i) < g
K : Type ?u.668108
F : Type ?u.668111
R : Type u_3
inst✝⁴ : DivisionRing K
Γ₀ : Type u_2
Γ'₀ : Type ?u.668123
Γ''₀ : Type ?u.668126
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v : Valuation R Γ₀
x y z : R
ι : Type u_1
s✝ : Finset ι
f : ι → R
g : Γ₀
hg : g ≠ 0
hf✝ : ∀ (i : ι), i ∈ s✝ → ↑v (f i) < g
a : ι
s : Finset ι
has : ¬a ∈ s
ih : (∀ (i : ι), i ∈ s → ↑v (f i) < g) → ↑v (∑ i in s, f i) < g
hf : ∀ (i : ι), i ∈ insert a s → ↑v (f i) < g
⊢ ↑v (∑ i in insert a s, f i) < g
rw [Finset.forall_mem_insert] at hf
K : Type ?u.668108
F : Type ?u.668111
R : Type u_3
inst✝⁴ : DivisionRing K
Γ₀ : Type u_2
Γ'₀ : Type ?u.668123
Γ''₀ : Type ?u.668126
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v : Valuation R Γ₀
x y z : R
ι : Type u_1
s✝ : Finset ι
f : ι → R
g : Γ₀
hg : g ≠ 0
hf✝ : ∀ (i : ι), i ∈ s✝ → ↑v (f i) < g
a : ι
s : Finset ι
has : ¬a ∈ s
ih : (∀ (i : ι), i ∈ s → ↑v (f i) < g) → ↑v (∑ i in s, f i) < g
hf : ↑v (f a) < g ∧ ∀ (x : ι), x ∈ s → ↑v (f x) < g
⊢ ↑v (f a + ∑ x in s, f x) < g
K : Type ?u.668108
F : Type ?u.668111
R : Type u_3
inst✝⁴ : DivisionRing K
Γ₀ : Type u_2
Γ'₀ : Type ?u.668123
Γ''₀ : Type ?u.668126
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v : Valuation R Γ₀
x y z : R
ι : Type u_1
s✝ : Finset ι
f : ι → R
g : Γ₀
hg : g ≠ 0
hf✝ : ∀ (i : ι), i ∈ s✝ → ↑v (f i) < g
a : ι
s : Finset ι
has : ¬a ∈ s
ih : (∀ (i : ι), i ∈ s → ↑v (f i) < g) → ↑v (∑ i in s, f i) < g
hf : ↑v (f a) < g ∧ ∀ (x : ι), x ∈ s → ↑v (f x) < g
⊢ ↑v (∑ i in insert a s, f i) < g
rw [Finset.sum_insert has]
no goals
K : Type ?u.668108
F : Type ?u.668111
R : Type u_3
inst✝⁴ : DivisionRing K
Γ₀ : Type u_2
Γ'₀ : Type ?u.668123
Γ''₀ : Type ?u.668126
inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝² : Ring R
inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀
inst✝ : LinearOrderedCommMonoidWithZero Γ'₀
v : Valuation R Γ₀
x y z : R
ι : Type u_1
s✝ : Finset ι
f : ι → R
g : Γ₀
hg : g ≠ 0
hf✝ : ∀ (i : ι), i ∈ s✝ → ↑v (f i) < g
a : ι
s : Finset ι
has : ¬a ∈ s
ih : (∀ (i : ι), i ∈ s → ↑v (f i) < g) → ↑v (∑ i in s, f i) < g
hf : ↑v (f a) < g ∧ ∀ (x : ι), x ∈ s → ↑v (f x) < g
⊢ ↑v (f a + ∑ x in s, f x) < g
exact v.map_add_lt hf.1 (ih hf.2)