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

case succ
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
F : ℕ → ℚ
hF✝ : ∀ (i : ℕ), i < n → 0 < padicValRat p (F i)
hn0✝ : ∑ i in Finset.range n, F i ≠ 0
d : ℕ
hd :
  (∀ (i : ℕ), i < d → 0 < padicValRat p (F i)) →
    ∑ i in Finset.range d, F i ≠ 0 → 0 < padicValRat p (∑ i in Finset.range d, F i)
hF : ∀ (i : ℕ), i < succ d → 0 < padicValRat p (F i)
hn0 : ∑ i in Finset.range (succ d), F i ≠ 0
⊢ 0 < padicValRat p (∑ i in Finset.range (succ d), F i)
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
F : ℕ → ℚ
hF : ∀ (i : ℕ), i < n → 0 < padicValRat p (F i)
hn0 : ∑ i in Finset.range n, F i ≠ 0
⊢ 0 < padicValRat p (∑ i in Finset.range n, F i)
induction' n with d hd
no goals
case zero
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
F : ℕ → ℚ
hF✝ : ∀ (i : ℕ), i < n → 0 < padicValRat p (F i)
hn0✝ : ∑ i in Finset.range n, F i ≠ 0
hF : ∀ (i : ℕ), i < zero → 0 < padicValRat p (F i)
hn0 : ∑ i in Finset.range zero, F i ≠ 0
⊢ 0 < padicValRat p (∑ i in Finset.range zero, F i)
exact False.elim (hn0 rfl)
case succ
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
F : ℕ → ℚ
hF✝ : ∀ (i : ℕ), i < n → 0 < padicValRat p (F i)
hn0✝ : ∑ i in Finset.range n, F i ≠ 0
d : ℕ
hd :
  (∀ (i : ℕ), i < d → 0 < padicValRat p (F i)) →
    ∑ i in Finset.range d, F i ≠ 0 → 0 < padicValRat p (∑ i in Finset.range d, F i)
hF : ∀ (i : ℕ), i < succ d → 0 < padicValRat p (F i)
hn0 : ∑ x in Finset.range d, F x + F d ≠ 0
⊢ 0 < padicValRat p (∑ x in Finset.range d, F x + F d)
case succ
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
F : ℕ → ℚ
hF✝ : ∀ (i : ℕ), i < n → 0 < padicValRat p (F i)
hn0✝ : ∑ i in Finset.range n, F i ≠ 0
d : ℕ
hd :
  (∀ (i : ℕ), i < d → 0 < padicValRat p (F i)) →
    ∑ i in Finset.range d, F i ≠ 0 → 0 < padicValRat p (∑ i in Finset.range d, F i)
hF : ∀ (i : ℕ), i < succ d → 0 < padicValRat p (F i)
hn0 : ∑ i in Finset.range (succ d), F i ≠ 0
⊢ 0 < padicValRat p (∑ i in Finset.range (succ d), F i)
rw [Finset.sum_range_succ] at hn0⊢
case pos
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
F : ℕ → ℚ
hF✝ : ∀ (i : ℕ), i < n → 0 < padicValRat p (F i)
hn0✝ : ∑ i in Finset.range n, F i ≠ 0
d : ℕ
hd :
  (∀ (i : ℕ), i < d → 0 < padicValRat p (F i)) →
    ∑ i in Finset.range d, F i ≠ 0 → 0 < padicValRat p (∑ i in Finset.range d, F i)
hF : ∀ (i : ℕ), i < succ d → 0 < padicValRat p (F i)
hn0 : ∑ x in Finset.range d, F x + F d ≠ 0
h : ∑ x in Finset.range d, F x = 0
⊢ 0 < padicValRat p (∑ x in Finset.range d, F x + F d)

case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
F : ℕ → ℚ
hF✝ : ∀ (i : ℕ), i < n → 0 < padicValRat p (F i)
hn0✝ : ∑ i in Finset.range n, F i ≠ 0
d : ℕ
hd :
  (∀ (i : ℕ), i < d → 0 < padicValRat p (F i)) →
    ∑ i in Finset.range d, F i ≠ 0 → 0 < padicValRat p (∑ i in Finset.range d, F i)
hF : ∀ (i : ℕ), i < succ d → 0 < padicValRat p (F i)
hn0 : ∑ x in Finset.range d, F x + F d ≠ 0
h : ¬∑ x in Finset.range d, F x = 0
⊢ 0 < padicValRat p (∑ x in Finset.range d, F x + F d)
case succ
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
F : ℕ → ℚ
hF✝ : ∀ (i : ℕ), i < n → 0 < padicValRat p (F i)
hn0✝ : ∑ i in Finset.range n, F i ≠ 0
d : ℕ
hd :
  (∀ (i : ℕ), i < d → 0 < padicValRat p (F i)) →
    ∑ i in Finset.range d, F i ≠ 0 → 0 < padicValRat p (∑ i in Finset.range d, F i)
hF : ∀ (i : ℕ), i < succ d → 0 < padicValRat p (F i)
hn0 : ∑ x in Finset.range d, F x + F d ≠ 0
⊢ 0 < padicValRat p (∑ x in Finset.range d, F x + F d)
by_cases h : (∑ x : ℕ in Finset.range d, F x) = 0
case pos
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
F : ℕ → ℚ
hF✝ : ∀ (i : ℕ), i < n → 0 < padicValRat p (F i)
hn0✝ : ∑ i in Finset.range n, F i ≠ 0
d : ℕ
hd :
  (∀ (i : ℕ), i < d → 0 < padicValRat p (F i)) →
    ∑ i in Finset.range d, F i ≠ 0 → 0 < padicValRat p (∑ i in Finset.range d, F i)
hF : ∀ (i : ℕ), i < succ d → 0 < padicValRat p (F i)
hn0 : ∑ x in Finset.range d, F x + F d ≠ 0
h : ∑ x in Finset.range d, F x = 0
⊢ 0 < padicValRat p (F d)
case pos
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
F : ℕ → ℚ
hF✝ : ∀ (i : ℕ), i < n → 0 < padicValRat p (F i)
hn0✝ : ∑ i in Finset.range n, F i ≠ 0
d : ℕ
hd :
  (∀ (i : ℕ), i < d → 0 < padicValRat p (F i)) →
    ∑ i in Finset.range d, F i ≠ 0 → 0 < padicValRat p (∑ i in Finset.range d, F i)
hF : ∀ (i : ℕ), i < succ d → 0 < padicValRat p (F i)
hn0 : ∑ x in Finset.range d, F x + F d ≠ 0
h : ∑ x in Finset.range d, F x = 0
⊢ 0 < padicValRat p (∑ x in Finset.range d, F x + F d)
rw [h, zero_add]
no goals
case pos
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
F : ℕ → ℚ
hF✝ : ∀ (i : ℕ), i < n → 0 < padicValRat p (F i)
hn0✝ : ∑ i in Finset.range n, F i ≠ 0
d : ℕ
hd :
  (∀ (i : ℕ), i < d → 0 < padicValRat p (F i)) →
    ∑ i in Finset.range d, F i ≠ 0 → 0 < padicValRat p (∑ i in Finset.range d, F i)
hF : ∀ (i : ℕ), i < succ d → 0 < padicValRat p (F i)
hn0 : ∑ x in Finset.range d, F x + F d ≠ 0
h : ∑ x in Finset.range d, F x = 0
⊢ 0 < padicValRat p (F d)
exact hF d (lt_add_one _)
case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
F : ℕ → ℚ
hF✝ : ∀ (i : ℕ), i < n → 0 < padicValRat p (F i)
hn0✝ : ∑ i in Finset.range n, F i ≠ 0
d : ℕ
hd :
  (∀ (i : ℕ), i < d → 0 < padicValRat p (F i)) →
    ∑ i in Finset.range d, F i ≠ 0 → 0 < padicValRat p (∑ i in Finset.range d, F i)
hF : ∀ (i : ℕ), i < succ d → 0 < padicValRat p (F i)
hn0 : ∑ x in Finset.range d, F x + F d ≠ 0
h : ¬∑ x in Finset.range d, F x = 0
⊢ 0 < min (padicValRat p (∑ x in Finset.range d, F x)) (padicValRat p (F d))
case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
F : ℕ → ℚ
hF✝ : ∀ (i : ℕ), i < n → 0 < padicValRat p (F i)
hn0✝ : ∑ i in Finset.range n, F i ≠ 0
d : ℕ
hd :
  (∀ (i : ℕ), i < d → 0 < padicValRat p (F i)) →
    ∑ i in Finset.range d, F i ≠ 0 → 0 < padicValRat p (∑ i in Finset.range d, F i)
hF : ∀ (i : ℕ), i < succ d → 0 < padicValRat p (F i)
hn0 : ∑ x in Finset.range d, F x + F d ≠ 0
h : ¬∑ x in Finset.range d, F x = 0
⊢ 0 < padicValRat p (∑ x in Finset.range d, F x + F d)
refine' lt_of_lt_of_le _ (min_le_padicValRat_add hn0)
case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
F : ℕ → ℚ
hF✝ : ∀ (i : ℕ), i < n → 0 < padicValRat p (F i)
hn0✝ : ∑ i in Finset.range n, F i ≠ 0
d : ℕ
hd :
  (∀ (i : ℕ), i < d → 0 < padicValRat p (F i)) →
    ∑ i in Finset.range d, F i ≠ 0 → 0 < padicValRat p (∑ i in Finset.range d, F i)
hF : ∀ (i : ℕ), i < succ d → 0 < padicValRat p (F i)
hn0 : ∑ x in Finset.range d, F x + F d ≠ 0
h : ¬∑ x in Finset.range d, F x = 0
i : ℕ
hi : i < d
⊢ 0 < padicValRat p (F i)
case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
F : ℕ → ℚ
hF✝ : ∀ (i : ℕ), i < n → 0 < padicValRat p (F i)
hn0✝ : ∑ i in Finset.range n, F i ≠ 0
d : ℕ
hd :
  (∀ (i : ℕ), i < d → 0 < padicValRat p (F i)) →
    ∑ i in Finset.range d, F i ≠ 0 → 0 < padicValRat p (∑ i in Finset.range d, F i)
hF : ∀ (i : ℕ), i < succ d → 0 < padicValRat p (F i)
hn0 : ∑ x in Finset.range d, F x + F d ≠ 0
h : ¬∑ x in Finset.range d, F x = 0
⊢ 0 < min (padicValRat p (∑ x in Finset.range d, F x)) (padicValRat p (F d))
refine' lt_min (hd (fun i hi => _) h) (hF d (lt_add_one _))
no goals
case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
F : ℕ → ℚ
hF✝ : ∀ (i : ℕ), i < n → 0 < padicValRat p (F i)
hn0✝ : ∑ i in Finset.range n, F i ≠ 0
d : ℕ
hd :
  (∀ (i : ℕ), i < d → 0 < padicValRat p (F i)) →
    ∑ i in Finset.range d, F i ≠ 0 → 0 < padicValRat p (∑ i in Finset.range d, F i)
hF : ∀ (i : ℕ), i < succ d → 0 < padicValRat p (F i)
hn0 : ∑ x in Finset.range d, F x + F d ≠ 0
h : ¬∑ x in Finset.range d, F x = 0
i : ℕ
hi : i < d
⊢ 0 < padicValRat p (F i)
exact hF _ (lt_trans hi (lt_add_one _))