-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
theorem sum_pos_of_pos {n : ℕ} {F : ℕ → ℚ} (hF : ∀ i, i < n → 0 < padicValRat p (F i))
    (hn0 : ∑ i ∈ Finset.range n, F i ≠ 0) : 0 < padicValRat p (∑ i ∈ Finset.range n, F i)

Proof state:
case zero
p : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
hF : ∀ i < 0, 0 < padicValRat p (F i)
hn0 : ∑ i ∈ Finset.range 0, F i ≠ 0
⊢ 0 < padicValRat p (∑ i ∈ Finset.range 0, F i)

Tactic:
exact False.elim (hn0 rfl)

Result:
no goals

Proof state:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
d : ℕ
hd : (∀ i < d, 0 < padicValRat p (F i)) → ∑ i ∈ Finset.range d, F i ≠ 0 → 0 < padicValRat p (∑ i ∈ Finset.range d, F i)
hF : ∀ i < d + 1, 0 < padicValRat p (F i)
hn0 : ∑ x ∈ Finset.range d, F x + F d ≠ 0
h : ¬∑ x ∈ Finset.range d, F x = 0
i : ℕ
hi : i < d
⊢ 0 < padicValRat p (F i)

Tactic:
exact hF _ (lt_trans hi (lt_add_one _))

Result:
no goals

Proof state:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
d : ℕ
hd : (∀ i < d, 0 < padicValRat p (F i)) → ∑ i ∈ Finset.range d, F i ≠ 0 → 0 < padicValRat p (∑ i ∈ Finset.range d, F i)
hF : ∀ i < d + 1, 0 < padicValRat p (F i)
hn0 : ∑ x ∈ Finset.range d, F x + F d ≠ 0
h : ∑ x ∈ Finset.range d, F x = 0
⊢ 0 < padicValRat p (∑ x ∈ Finset.range d, F x + F d)

Tactic:
rw [h, zero_add]

Result:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
d : ℕ
hd : (∀ i < d, 0 < padicValRat p (F i)) → ∑ i ∈ Finset.range d, F i ≠ 0 → 0 < padicValRat p (∑ i ∈ Finset.range d, F i)
hF : ∀ i < d + 1, 0 < padicValRat p (F i)
hn0 : ∑ x ∈ Finset.range d, F x + F d ≠ 0
h : ∑ x ∈ Finset.range d, F x = 0
⊢ 0 < padicValRat p (F d)

Proof state:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
d : ℕ
hd : (∀ i < d, 0 < padicValRat p (F i)) → ∑ i ∈ Finset.range d, F i ≠ 0 → 0 < padicValRat p (∑ i ∈ Finset.range d, F i)
hF : ∀ i < d + 1, 0 < padicValRat p (F i)
hn0 : ∑ x ∈ Finset.range d, F x + F d ≠ 0
h : ∑ x ∈ Finset.range d, F x = 0
⊢ 0 < padicValRat p (F d)

Tactic:
exact hF d (lt_add_one _)

Result:
no goals

Proof state:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
d : ℕ
hd : (∀ i < d, 0 < padicValRat p (F i)) → ∑ i ∈ Finset.range d, F i ≠ 0 → 0 < padicValRat p (∑ i ∈ Finset.range d, F i)
hF : ∀ i < d + 1, 0 < padicValRat p (F i)
hn0 : ∑ x ∈ Finset.range d, F x + F d ≠ 0
h : ¬∑ x ∈ Finset.range d, F x = 0
⊢ 0 < padicValRat p (∑ x ∈ Finset.range d, F x + F d)

Tactic:
refine lt_of_lt_of_le ?_ (min_le_padicValRat_add hn0)

Result:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
d : ℕ
hd : (∀ i < d, 0 < padicValRat p (F i)) → ∑ i ∈ Finset.range d, F i ≠ 0 → 0 < padicValRat p (∑ i ∈ Finset.range d, F i)
hF : ∀ i < d + 1, 0 < padicValRat p (F i)
hn0 : ∑ x ∈ Finset.range d, F x + F d ≠ 0
h : ¬∑ x ∈ Finset.range d, F x = 0
⊢ 0 < padicValRat p (∑ x ∈ Finset.range d, F x) ⊓ padicValRat p (F d)

Proof state:
case succ
p : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
d : ℕ
hd : (∀ i < d, 0 < padicValRat p (F i)) → ∑ i ∈ Finset.range d, F i ≠ 0 → 0 < padicValRat p (∑ i ∈ Finset.range d, F i)
hF : ∀ i < d + 1, 0 < padicValRat p (F i)
hn0 : ∑ i ∈ Finset.range (d + 1), F i ≠ 0
⊢ 0 < padicValRat p (∑ i ∈ Finset.range (d + 1), F i)

Tactic:
rw [Finset.sum_range_succ] at hn0 ⊢

Result:
case succ
p : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
d : ℕ
hd : (∀ i < d, 0 < padicValRat p (F i)) → ∑ i ∈ Finset.range d, F i ≠ 0 → 0 < padicValRat p (∑ i ∈ Finset.range d, F i)
hF : ∀ i < d + 1, 0 < padicValRat p (F i)
hn0 : ∑ x ∈ Finset.range d, F x + F d ≠ 0
⊢ 0 < padicValRat p (∑ x ∈ Finset.range d, F x + F d)

Proof state:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
d : ℕ
hd : (∀ i < d, 0 < padicValRat p (F i)) → ∑ i ∈ Finset.range d, F i ≠ 0 → 0 < padicValRat p (∑ i ∈ Finset.range d, F i)
hF : ∀ i < d + 1, 0 < padicValRat p (F i)
hn0 : ∑ x ∈ Finset.range d, F x + F d ≠ 0
h : ¬∑ x ∈ Finset.range d, F x = 0
⊢ 0 < padicValRat p (∑ x ∈ Finset.range d, F x) ⊓ padicValRat p (F d)

Tactic:
refine lt_min (hd (fun i hi => ?_) h) (hF d (lt_add_one _))

Result:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
d : ℕ
hd : (∀ i < d, 0 < padicValRat p (F i)) → ∑ i ∈ Finset.range d, F i ≠ 0 → 0 < padicValRat p (∑ i ∈ Finset.range d, F i)
hF : ∀ i < d + 1, 0 < padicValRat p (F i)
hn0 : ∑ x ∈ Finset.range d, F x + F d ≠ 0
h : ¬∑ x ∈ Finset.range d, F x = 0
i : ℕ
hi : i < d
⊢ 0 < padicValRat p (F i)

Proof state:
case succ
p : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
d : ℕ
hd : (∀ i < d, 0 < padicValRat p (F i)) → ∑ i ∈ Finset.range d, F i ≠ 0 → 0 < padicValRat p (∑ i ∈ Finset.range d, F i)
hF : ∀ i < d + 1, 0 < padicValRat p (F i)
hn0 : ∑ x ∈ Finset.range d, F x + F d ≠ 0
⊢ 0 < padicValRat p (∑ x ∈ Finset.range d, F x + F d)

Tactic:
by_cases h : ∑ x ∈ Finset.range d, F x = 0

Result:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
d : ℕ
hd : (∀ i < d, 0 < padicValRat p (F i)) → ∑ i ∈ Finset.range d, F i ≠ 0 → 0 < padicValRat p (∑ i ∈ Finset.range d, F i)
hF : ∀ i < d + 1, 0 < padicValRat p (F i)
hn0 : ∑ x ∈ Finset.range d, F x + F d ≠ 0
h : ∑ x ∈ Finset.range d, F x = 0
⊢ 0 < padicValRat p (∑ x ∈ Finset.range d, F x + F d)

case neg
p : ℕ
hp : Fact (Nat.Prime p)
F : ℕ → ℚ
d : ℕ
hd : (∀ i < d, 0 < padicValRat p (F i)) → ∑ i ∈ Finset.range d, F i ≠ 0 → 0 < padicValRat p (∑ i ∈ Finset.range d, F i)
hF : ∀ i < d + 1, 0 < padicValRat p (F i)
hn0 : ∑ x ∈ Finset.range d, F x + F d ≠ 0
h : ¬∑ x ∈ Finset.range d, F x = 0
⊢ 0 < padicValRat p (∑ x ∈ Finset.range d, F x + F d)