Theorem: Imo2013P1.prod_lemma (Compfiles/Imo2013P1.lean)

State before:
m : ℕ → ℕ+
k : ℕ
nm : ℕ+
⊢ ∏ i ∈ Finset.range k, (1 + 1 / ↑↑(if i < k then m i else nm)) = ∏ i ∈ Finset.range k, (1 + 1 / ↑↑(m i))
Tactic:
suffices ∀ i, i ∈ Finset.range k → (1 : ℚ) + 1 / ↑(if i < k then m i else nm) = 1 + 1 / m i from
  Finset.prod_congr rfl this
State after:
m : ℕ → ℕ+
k : ℕ
nm : ℕ+
⊢ ∀ i ∈ Finset.range k, 1 + 1 / ↑↑(if i < k then m i else nm) = 1 + 1 / ↑↑(m i)

State before:
m : ℕ → ℕ+
k : ℕ
nm : ℕ+
⊢ ∀ i ∈ Finset.range k, 1 + 1 / ↑↑(if i < k then m i else nm) = 1 + 1 / ↑↑(m i)
Tactic:
intro i hi
State after:
m : ℕ → ℕ+
k : ℕ
nm : ℕ+
i : ℕ
hi : i ∈ Finset.range k
⊢ 1 + 1 / ↑↑(if i < k then m i else nm) = 1 + 1 / ↑↑(m i)

State before:
m : ℕ → ℕ+
k : ℕ
nm : ℕ+
i : ℕ
hi : i ∈ Finset.range k
⊢ 1 + 1 / ↑↑(if i < k then m i else nm) = 1 + 1 / ↑↑(m i)
Tactic:
simp [Finset.mem_range.mp hi]
State after:
no goals