Theorem: Usa1992P1.Finset.range_prod_odd (Compfiles/Usa1992P1.lean)

State before:
n : ℕ
f : ℕ → ℕ
hs : ∀ i ∈ Finset.range n, Odd (f i)
⊢ Odd (∏ i ∈ Finset.range n, f i)
Tactic:
revert hs
State after:
n : ℕ
f : ℕ → ℕ
⊢ (∀ i ∈ Finset.range n, Odd (f i)) → Odd (∏ i ∈ Finset.range n, f i)

State before:
n : ℕ
f : ℕ → ℕ
⊢ (∀ i ∈ Finset.range n, Odd (f i)) → Odd (∏ i ∈ Finset.range n, f i)
Tactic:
induction n
State after:
case zero
f : ℕ → ℕ
⊢ (∀ i ∈ Finset.range 0, Odd (f i)) → Odd (∏ i ∈ Finset.range 0, f i)

case succ
f : ℕ → ℕ
n✝ : ℕ
a✝ : (∀ i ∈ Finset.range n✝, Odd (f i)) → Odd (∏ i ∈ Finset.range n✝, f i)
⊢ (∀ i ∈ Finset.range (n✝ + 1), Odd (f i)) → Odd (∏ i ∈ Finset.range (n✝ + 1), f i)

State before:
f : ℕ → ℕ
⊢ (∀ i ∈ Finset.range 0, Odd (f i)) → Odd (∏ i ∈ Finset.range 0, f i)
Tactic:
case zero => simp
State after:
no goals

State before:
f : ℕ → ℕ
⊢ (∀ i ∈ Finset.range 0, Odd (f i)) → Odd (∏ i ∈ Finset.range 0, f i)
Tactic:
simp
State after:
no goals

State before:
f : ℕ → ℕ
n : ℕ
ih : (∀ i ∈ Finset.range n, Odd (f i)) → Odd (∏ i ∈ Finset.range n, f i)
⊢ (∀ i ∈ Finset.range (n + 1), Odd (f i)) → Odd (∏ i ∈ Finset.range (n + 1), f i)
Tactic:
intro hs
State after:
f : ℕ → ℕ
n : ℕ
ih : (∀ i ∈ Finset.range n, Odd (f i)) → Odd (∏ i ∈ Finset.range n, f i)
hs : ∀ i ∈ Finset.range (n + 1), Odd (f i)
⊢ Odd (∏ i ∈ Finset.range (n + 1), f i)

State before:
f : ℕ → ℕ
n : ℕ
ih : (∀ i ∈ Finset.range n, Odd (f i)) → Odd (∏ i ∈ Finset.range n, f i)
hs : ∀ i ∈ Finset.range (n + 1), Odd (f i)
⊢ Odd (∏ i ∈ Finset.range (n + 1), f i)
Tactic:
rw [Finset.prod_range_succ, Nat.odd_mul]
State after:
f : ℕ → ℕ
n : ℕ
ih : (∀ i ∈ Finset.range n, Odd (f i)) → Odd (∏ i ∈ Finset.range n, f i)
hs : ∀ i ∈ Finset.range (n + 1), Odd (f i)
⊢ Odd (∏ x ∈ Finset.range n, f x) ∧ Odd (f n)

State before:
f : ℕ → ℕ
n : ℕ
ih : (∀ i ∈ Finset.range n, Odd (f i)) → Odd (∏ i ∈ Finset.range n, f i)
hs : ∀ i ∈ Finset.range (n + 1), Odd (f i)
⊢ Odd (∏ x ∈ Finset.range n, f x) ∧ Odd (f n)
Tactic:
constructor
State after:
case left
f : ℕ → ℕ
n : ℕ
ih : (∀ i ∈ Finset.range n, Odd (f i)) → Odd (∏ i ∈ Finset.range n, f i)
hs : ∀ i ∈ Finset.range (n + 1), Odd (f i)
⊢ Odd (∏ x ∈ Finset.range n, f x)

case right
f : ℕ → ℕ
n : ℕ
ih : (∀ i ∈ Finset.range n, Odd (f i)) → Odd (∏ i ∈ Finset.range n, f i)
hs : ∀ i ∈ Finset.range (n + 1), Odd (f i)
⊢ Odd (f n)

State before:
case left
f : ℕ → ℕ
n : ℕ
ih : (∀ i ∈ Finset.range n, Odd (f i)) → Odd (∏ i ∈ Finset.range n, f i)
hs : ∀ i ∈ Finset.range (n + 1), Odd (f i)
⊢ Odd (∏ x ∈ Finset.range n, f x)
Tactic:
apply ih
State after:
case left
f : ℕ → ℕ
n : ℕ
ih : (∀ i ∈ Finset.range n, Odd (f i)) → Odd (∏ i ∈ Finset.range n, f i)
hs : ∀ i ∈ Finset.range (n + 1), Odd (f i)
⊢ ∀ i ∈ Finset.range n, Odd (f i)

State before:
case left
f : ℕ → ℕ
n : ℕ
ih : (∀ i ∈ Finset.range n, Odd (f i)) → Odd (∏ i ∈ Finset.range n, f i)
hs : ∀ i ∈ Finset.range (n + 1), Odd (f i)
⊢ ∀ i ∈ Finset.range n, Odd (f i)
Tactic:
intro i hi
State after:
case left
f : ℕ → ℕ
n : ℕ
ih : (∀ i ∈ Finset.range n, Odd (f i)) → Odd (∏ i ∈ Finset.range n, f i)
hs : ∀ i ∈ Finset.range (n + 1), Odd (f i)
i : ℕ
hi : i ∈ Finset.range n
⊢ Odd (f i)

State before:
case left
f : ℕ → ℕ
n : ℕ
ih : (∀ i ∈ Finset.range n, Odd (f i)) → Odd (∏ i ∈ Finset.range n, f i)
hs : ∀ i ∈ Finset.range (n + 1), Odd (f i)
i : ℕ
hi : i ∈ Finset.range n
⊢ Odd (f i)
Tactic:
have : i ∈ Finset.range (n + 1) := by
  rw [Finset.mem_range] at *
  exact Nat.lt_add_right 1 hi
State after:
case left
f : ℕ → ℕ
n : ℕ
ih : (∀ i ∈ Finset.range n, Odd (f i)) → Odd (∏ i ∈ Finset.range n, f i)
hs : ∀ i ∈ Finset.range (n + 1), Odd (f i)
i : ℕ
hi : i ∈ Finset.range n
this : i ∈ Finset.range (n + 1)
⊢ Odd (f i)

State before:
case left
f : ℕ → ℕ
n : ℕ
ih : (∀ i ∈ Finset.range n, Odd (f i)) → Odd (∏ i ∈ Finset.range n, f i)
hs : ∀ i ∈ Finset.range (n + 1), Odd (f i)
i : ℕ
hi : i ∈ Finset.range n
this : i ∈ Finset.range (n + 1)
⊢ Odd (f i)
Tactic:
exact hs i this
State after:
no goals

State before:
f : ℕ → ℕ
n : ℕ
ih : (∀ i ∈ Finset.range n, Odd (f i)) → Odd (∏ i ∈ Finset.range n, f i)
hs : ∀ i ∈ Finset.range (n + 1), Odd (f i)
i : ℕ
hi : i ∈ Finset.range n
⊢ i ∈ Finset.range (n + 1)
Tactic:
rw [Finset.mem_range] at *
State after:
f : ℕ → ℕ
n : ℕ
ih : (∀ i ∈ Finset.range n, Odd (f i)) → Odd (∏ i ∈ Finset.range n, f i)
hs : ∀ i ∈ Finset.range (n + 1), Odd (f i)
i : ℕ
hi : i < n
⊢ i < n + 1

State before:
f : ℕ → ℕ
n : ℕ
ih : (∀ i ∈ Finset.range n, Odd (f i)) → Odd (∏ i ∈ Finset.range n, f i)
hs : ∀ i ∈ Finset.range (n + 1), Odd (f i)
i : ℕ
hi : i < n
⊢ i < n + 1
Tactic:
exact Nat.lt_add_right 1 hi
State after:
no goals

State before:
case right
f : ℕ → ℕ
n : ℕ
ih : (∀ i ∈ Finset.range n, Odd (f i)) → Odd (∏ i ∈ Finset.range n, f i)
hs : ∀ i ∈ Finset.range (n + 1), Odd (f i)
⊢ Odd (f n)
Tactic:
apply hs
State after:
case right.a
f : ℕ → ℕ
n : ℕ
ih : (∀ i ∈ Finset.range n, Odd (f i)) → Odd (∏ i ∈ Finset.range n, f i)
hs : ∀ i ∈ Finset.range (n + 1), Odd (f i)
⊢ n ∈ Finset.range (n + 1)

State before:
case right.a
f : ℕ → ℕ
n : ℕ
ih : (∀ i ∈ Finset.range n, Odd (f i)) → Odd (∏ i ∈ Finset.range n, f i)
hs : ∀ i ∈ Finset.range (n + 1), Odd (f i)
⊢ n ∈ Finset.range (n + 1)
Tactic:
rw [Finset.mem_range]
State after:
case right.a
f : ℕ → ℕ
n : ℕ
ih : (∀ i ∈ Finset.range n, Odd (f i)) → Odd (∏ i ∈ Finset.range n, f i)
hs : ∀ i ∈ Finset.range (n + 1), Odd (f i)
⊢ n < n + 1

State before:
case right.a
f : ℕ → ℕ
n : ℕ
ih : (∀ i ∈ Finset.range n, Odd (f i)) → Odd (∏ i ∈ Finset.range n, f i)
hs : ∀ i ∈ Finset.range (n + 1), Odd (f i)
⊢ n < n + 1
Tactic:
exact lt_add_one n
State after:
no goals