Theorem: prod_Icc_succ_div (FormalBook/Chapter_01.lean)

State before:
n : ℕ
hn : 2 ≤ n
⊢ ∏ x ∈ Icc 1 n, (↑x + 1) / ↑x = ↑n + 1
Tactic:
rw [← Nat.Ico_succ_right]
State after:
n : ℕ
hn : 2 ≤ n
⊢ ∏ x ∈ Ico 1 n.succ, (↑x + 1) / ↑x = ↑n + 1

State before:
n : ℕ
hn : 2 ≤ n
⊢ ∏ x ∈ Ico 1 n.succ, (↑x + 1) / ↑x = ↑n + 1
Tactic:
induction' n with n h
State after:
case zero
hn : 2 ≤ 0
⊢ ∏ x ∈ Ico 1 (succ 0), (↑x + 1) / ↑x = ↑0 + 1

case succ
n : ℕ
h : 2 ≤ n → ∏ x ∈ Ico 1 n.succ, (↑x + 1) / ↑x = ↑n + 1
hn : 2 ≤ n + 1
⊢ ∏ x ∈ Ico 1 (n + 1).succ, (↑x + 1) / ↑x = ↑(n + 1) + 1

State before:
case zero
hn : 2 ≤ 0
⊢ ∏ x ∈ Ico 1 (succ 0), (↑x + 1) / ↑x = ↑0 + 1
Tactic:
simp
State after:
no goals

State before:
case succ
n : ℕ
h : 2 ≤ n → ∏ x ∈ Ico 1 n.succ, (↑x + 1) / ↑x = ↑n + 1
hn : 2 ≤ n + 1
⊢ ∏ x ∈ Ico 1 (n + 1).succ, (↑x + 1) / ↑x = ↑(n + 1) + 1
Tactic:
rw [Finset.prod_Ico_succ_top <| Nat.le_add_left 1 n]
State after:
case succ
n : ℕ
h : 2 ≤ n → ∏ x ∈ Ico 1 n.succ, (↑x + 1) / ↑x = ↑n + 1
hn : 2 ≤ n + 1
⊢ (∏ k ∈ Ico 1 (n + 1), (↑k + 1) / ↑k) * ((↑(n + 1) + 1) / ↑(n + 1)) = ↑(n + 1) + 1

State before:
case succ
n : ℕ
h : 2 ≤ n → ∏ x ∈ Ico 1 n.succ, (↑x + 1) / ↑x = ↑n + 1
hn : 2 ≤ n + 1
⊢ (∏ k ∈ Ico 1 (n + 1), (↑k + 1) / ↑k) * ((↑(n + 1) + 1) / ↑(n + 1)) = ↑(n + 1) + 1
Tactic:
norm_num
State after:
case succ
n : ℕ
h : 2 ≤ n → ∏ x ∈ Ico 1 n.succ, (↑x + 1) / ↑x = ↑n + 1
hn : 2 ≤ n + 1
⊢ ((∏ x ∈ Ico 1 (n + 1), (↑x + 1)) / ∏ x ∈ Ico 1 (n + 1), ↑x) * ((↑n + 1 + 1) / (↑n + 1)) = ↑n + 1 + 1

State before:
case succ
n : ℕ
h : 2 ≤ n → ∏ x ∈ Ico 1 n.succ, (↑x + 1) / ↑x = ↑n + 1
hn : 2 ≤ n + 1
⊢ ((∏ x ∈ Ico 1 (n + 1), (↑x + 1)) / ∏ x ∈ Ico 1 (n + 1), ↑x) * ((↑n + 1 + 1) / (↑n + 1)) = ↑n + 1 + 1
Tactic:
cases' lt_or_ge n 2 with _ h2
State after:
case succ.inl
n : ℕ
h : 2 ≤ n → ∏ x ∈ Ico 1 n.succ, (↑x + 1) / ↑x = ↑n + 1
hn : 2 ≤ n + 1
h✝ : n < 2
⊢ ((∏ x ∈ Ico 1 (n + 1), (↑x + 1)) / ∏ x ∈ Ico 1 (n + 1), ↑x) * ((↑n + 1 + 1) / (↑n + 1)) = ↑n + 1 + 1

case succ.inr
n : ℕ
h : 2 ≤ n → ∏ x ∈ Ico 1 n.succ, (↑x + 1) / ↑x = ↑n + 1
hn : 2 ≤ n + 1
h2 : n ≥ 2
⊢ ((∏ x ∈ Ico 1 (n + 1), (↑x + 1)) / ∏ x ∈ Ico 1 (n + 1), ↑x) * ((↑n + 1 + 1) / (↑n + 1)) = ↑n + 1 + 1

State before:
case succ.inr
n : ℕ
h : 2 ≤ n → ∏ x ∈ Ico 1 n.succ, (↑x + 1) / ↑x = ↑n + 1
hn : 2 ≤ n + 1
h2 : n ≥ 2
⊢ ((∏ x ∈ Ico 1 (n + 1), (↑x + 1)) / ∏ x ∈ Ico 1 (n + 1), ↑x) * ((↑n + 1 + 1) / (↑n + 1)) = ↑n + 1 + 1
Tactic:
specialize h h2
State after:
case succ.inr
n : ℕ
hn : 2 ≤ n + 1
h2 : n ≥ 2
h : ∏ x ∈ Ico 1 n.succ, (↑x + 1) / ↑x = ↑n + 1
⊢ ((∏ x ∈ Ico 1 (n + 1), (↑x + 1)) / ∏ x ∈ Ico 1 (n + 1), ↑x) * ((↑n + 1 + 1) / (↑n + 1)) = ↑n + 1 + 1

State before:
case succ.inr
n : ℕ
hn : 2 ≤ n + 1
h2 : n ≥ 2
h : ∏ x ∈ Ico 1 n.succ, (↑x + 1) / ↑x = ↑n + 1
⊢ ((∏ x ∈ Ico 1 (n + 1), (↑x + 1)) / ∏ x ∈ Ico 1 (n + 1), ↑x) * ((↑n + 1 + 1) / (↑n + 1)) = ↑n + 1 + 1
Tactic:
field_simp [Finset.prod_eq_zero_iff] at h ⊢
State after:
case succ.inr
n : ℕ
hn : 2 ≤ n + 1
h2 : n ≥ 2
h : ∏ x ∈ Ico 1 (n + 1), (↑x + 1) = (↑n + 1) * ∏ x ∈ Ico 1 (n + 1), ↑x
⊢ (∏ x ∈ Ico 1 (n + 1), (↑x + 1)) * (↑n + 1 + 1) = (↑n + 1 + 1) * ((∏ x ∈ Ico 1 (n + 1), ↑x) * (↑n + 1))

State before:
case succ.inr
n : ℕ
hn : 2 ≤ n + 1
h2 : n ≥ 2
h : ∏ x ∈ Ico 1 (n + 1), (↑x + 1) = (↑n + 1) * ∏ x ∈ Ico 1 (n + 1), ↑x
⊢ (∏ x ∈ Ico 1 (n + 1), (↑x + 1)) * (↑n + 1 + 1) = (↑n + 1 + 1) * ((∏ x ∈ Ico 1 (n + 1), ↑x) * (↑n + 1))
Tactic:
rw [h]
State after:
case succ.inr
n : ℕ
hn : 2 ≤ n + 1
h2 : n ≥ 2
h : ∏ x ∈ Ico 1 (n + 1), (↑x + 1) = (↑n + 1) * ∏ x ∈ Ico 1 (n + 1), ↑x
⊢ ((↑n + 1) * ∏ x ∈ Ico 1 (n + 1), ↑x) * (↑n + 1 + 1) = (↑n + 1 + 1) * ((∏ x ∈ Ico 1 (n + 1), ↑x) * (↑n + 1))

State before:
case succ.inr
n : ℕ
hn : 2 ≤ n + 1
h2 : n ≥ 2
h : ∏ x ∈ Ico 1 (n + 1), (↑x + 1) = (↑n + 1) * ∏ x ∈ Ico 1 (n + 1), ↑x
⊢ ((↑n + 1) * ∏ x ∈ Ico 1 (n + 1), ↑x) * (↑n + 1 + 1) = (↑n + 1 + 1) * ((∏ x ∈ Ico 1 (n + 1), ↑x) * (↑n + 1))
Tactic:
ring
State after:
no goals

State before:
case succ.inl
n : ℕ
h : 2 ≤ n → ∏ x ∈ Ico 1 n.succ, (↑x + 1) / ↑x = ↑n + 1
hn : 2 ≤ n + 1
h✝ : n < 2
⊢ ((∏ x ∈ Ico 1 (n + 1), (↑x + 1)) / ∏ x ∈ Ico 1 (n + 1), ↑x) * ((↑n + 1 + 1) / (↑n + 1)) = ↑n + 1 + 1
Tactic:
interval_cases n
State after:
case succ.inl.«0»
n : ℕ
h : 2 ≤ 0 → ∏ x ∈ Ico 1 (succ 0), (↑x + 1) / ↑x = ↑0 + 1
hn : 2 ≤ 0 + 1
h✝ : 0 < 2
⊢ ((∏ x ∈ Ico 1 (0 + 1), (↑x + 1)) / ∏ x ∈ Ico 1 (0 + 1), ↑x) * ((↑0 + 1 + 1) / (↑0 + 1)) = ↑0 + 1 + 1

case succ.inl.«1»
n : ℕ
h : 2 ≤ 1 → ∏ x ∈ Ico 1 (succ 1), (↑x + 1) / ↑x = ↑1 + 1
hn : 2 ≤ 1 + 1
h✝ : 1 < 2
⊢ ((∏ x ∈ Ico 1 (1 + 1), (↑x + 1)) / ∏ x ∈ Ico 1 (1 + 1), ↑x) * ((↑1 + 1 + 1) / (↑1 + 1)) = ↑1 + 1 + 1

State before:
case succ.inl.«0»
n : ℕ
h : 2 ≤ 0 → ∏ x ∈ Ico 1 (succ 0), (↑x + 1) / ↑x = ↑0 + 1
hn : 2 ≤ 0 + 1
h✝ : 0 < 2
⊢ ((∏ x ∈ Ico 1 (0 + 1), (↑x + 1)) / ∏ x ∈ Ico 1 (0 + 1), ↑x) * ((↑0 + 1 + 1) / (↑0 + 1)) = ↑0 + 1 + 1
Tactic:
tauto
State after:
no goals

State before:
case succ.inl.«1»
n : ℕ
h : 2 ≤ 1 → ∏ x ∈ Ico 1 (succ 1), (↑x + 1) / ↑x = ↑1 + 1
hn : 2 ≤ 1 + 1
h✝ : 1 < 2
⊢ ((∏ x ∈ Ico 1 (1 + 1), (↑x + 1)) / ∏ x ∈ Ico 1 (1 + 1), ↑x) * ((↑1 + 1 + 1) / (↑1 + 1)) = ↑1 + 1 + 1
Tactic:
norm_num
State after:
no goals