-- Mathlib/Algebra/BigOperators/Fin.lean
theorem prod_take_ofFn {n : ℕ} (f : Fin n → α) (i : ℕ) :
    ((ofFn f).take i).prod = ∏ j ∈ Finset.univ.filter fun j : Fin n => j.val < i, f j

Proof state:
case neg
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j ∈ Finset.filter (fun j => ↑j < i) univ, f j
h : ¬i < n
⊢ (take (i + 1) (ofFn f)).prod = ∏ j ∈ Finset.filter (fun j => ↑j < i + 1) univ, f j

Tactic:
have A : (ofFn f).take i = (ofFn f).take i.succ := by
  rw [← length_ofFn f] at h
  have : length (ofFn f) ≤ i := not_lt.mp h
  rw [take_of_length_le this, take_of_length_le (le_trans this (Nat.le_succ _))]

Result:
case neg
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j ∈ Finset.filter (fun j => ↑j < i) univ, f j
h : ¬i < n
A : take i (ofFn f) = take i.succ (ofFn f)
⊢ (take (i + 1) (ofFn f)).prod = ∏ j ∈ Finset.filter (fun j => ↑j < i + 1) univ, f j

Proof state:
case pos
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j ∈ Finset.filter (fun j => ↑j < i) univ, f j
h : i < n
this : i < (ofFn f).length
⊢ (take i (ofFn f)).prod * (ofFn f)[i] = ∏ j ∈ Finset.filter (fun j => ↑j < i + 1) univ, f j

Tactic:
have A : ((Finset.univ : Finset (Fin n)).filter fun j => j.val < i + 1) =
    ((Finset.univ : Finset (Fin n)).filter fun j => j.val < i) ∪ {(⟨i, h⟩ : Fin n)} := by
  ext ⟨_, _⟩
  simp [Nat.lt_succ_iff_lt_or_eq]

Result:
case pos
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j ∈ Finset.filter (fun j => ↑j < i) univ, f j
h : i < n
this : i < (ofFn f).length
A : Finset.filter (fun j => ↑j < i + 1) univ = Finset.filter (fun j => ↑j < i) univ ∪ {⟨i, h⟩}
⊢ (take i (ofFn f)).prod * (ofFn f)[i] = ∏ j ∈ Finset.filter (fun j => ↑j < i + 1) univ, f j

Proof state:
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j ∈ Finset.filter (fun j => ↑j < i) univ, f j
h : i < n
this : i < (ofFn f).length
A : Finset.filter (fun j => ↑j < i + 1) univ = Finset.filter (fun j => ↑j < i) univ ∪ {⟨i, h⟩}
⊢ _root_.Disjoint (Finset.filter (fun j => ↑j < i) univ) {⟨i, h⟩}

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j ∈ Finset.filter (fun j => ↑j < i) univ, f j
h : ¬i < n
A : take i (ofFn f) = take i.succ (ofFn f)
j : Fin n
⊢ (↑j < i.succ) = (↑j < i)

Tactic:
have : (j : ℕ) < i := lt_of_lt_of_le j.2 (not_lt.mp h)

Result:
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j ∈ Finset.filter (fun j => ↑j < i) univ, f j
h : ¬i < n
A : take i (ofFn f) = take i.succ (ofFn f)
j : Fin n
this : ↑j < i
⊢ (↑j < i.succ) = (↑j < i)

Proof state:
case pos
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j ∈ Finset.filter (fun j => ↑j < i) univ, f j
h : i < n
this : i < (ofFn f).length
A : Finset.filter (fun j => ↑j < i + 1) univ = Finset.filter (fun j => ↑j < i) univ ∪ {⟨i, h⟩}
B : _root_.Disjoint (Finset.filter (fun j => ↑j < i) univ) {⟨i, h⟩}
⊢ (take i (ofFn f)).prod * (ofFn f)[i] = ∏ j ∈ Finset.filter (fun j => ↑j < i + 1) univ, f j

Tactic:
rw [A, Finset.prod_union B, IH]

Result:
case pos
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j ∈ Finset.filter (fun j => ↑j < i) univ, f j
h : i < n
this : i < (ofFn f).length
A : Finset.filter (fun j => ↑j < i + 1) univ = Finset.filter (fun j => ↑j < i) univ ∪ {⟨i, h⟩}
B : _root_.Disjoint (Finset.filter (fun j => ↑j < i) univ) {⟨i, h⟩}
⊢ (∏ j ∈ Finset.filter (fun j => ↑j < i) univ, f j) * (ofFn f)[i] =
    (∏ x ∈ Finset.filter (fun j => ↑j < i) univ, f x) * ∏ x ∈ {⟨i, h⟩}, f x

Proof state:
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j ∈ Finset.filter (fun j => ↑j < i) univ, f j
h : ¬i < (ofFn f).length
⊢ take i (ofFn f) = take i.succ (ofFn f)

Tactic:
have : length (ofFn f) ≤ i := not_lt.mp h

Result:
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j ∈ Finset.filter (fun j => ↑j < i) univ, f j
h : ¬i < (ofFn f).length
this : (ofFn f).length ≤ i
⊢ take i (ofFn f) = take i.succ (ofFn f)

Proof state:
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j ∈ Finset.filter (fun j => ↑j < i) univ, f j
h : ¬i < n
⊢ take i (ofFn f) = take i.succ (ofFn f)

Tactic:
rw [← length_ofFn f] at h

Result:
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j ∈ Finset.filter (fun j => ↑j < i) univ, f j
h : ¬i < (ofFn f).length
⊢ take i (ofFn f) = take i.succ (ofFn f)

Proof state:
case pos
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j ∈ Finset.filter (fun j => ↑j < i) univ, f j
h : i < n
this : i < (ofFn f).length
A : Finset.filter (fun j => ↑j < i + 1) univ = Finset.filter (fun j => ↑j < i) univ ∪ {⟨i, h⟩}
B : _root_.Disjoint (Finset.filter (fun j => ↑j < i) univ) {⟨i, h⟩}
⊢ (∏ j ∈ Finset.filter (fun j => ↑j < i) univ, f j) * (ofFn f)[i] =
    (∏ x ∈ Finset.filter (fun j => ↑j < i) univ, f x) * ∏ x ∈ {⟨i, h⟩}, f x

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j ∈ Finset.filter (fun j => ↑j < i) univ, f j
h : i < n
⊢ i < (ofFn f).length

Tactic:
rwa [length_ofFn f]

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j ∈ Finset.filter (fun j => ↑j < i) univ, f j
h : i < n
this : i < (ofFn f).length
A : Finset.filter (fun j => ↑j < i + 1) univ = Finset.filter (fun j => ↑j < i) univ ∪ {⟨i, h⟩}
⊢ (take i (ofFn f)).prod * (ofFn f)[i] = ∏ j ∈ Finset.filter (fun j => ↑j < i + 1) univ, f j

Tactic:
have B : _root_.Disjoint (Finset.filter (fun j : Fin n => j.val < i) Finset.univ)
    (singleton (⟨i, h⟩ : Fin n)) := by simp

Result:
case pos
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j ∈ Finset.filter (fun j => ↑j < i) univ, f j
h : i < n
this : i < (ofFn f).length
A : Finset.filter (fun j => ↑j < i + 1) univ = Finset.filter (fun j => ↑j < i) univ ∪ {⟨i, h⟩}
B : _root_.Disjoint (Finset.filter (fun j => ↑j < i) univ) {⟨i, h⟩}
⊢ (take i (ofFn f)).prod * (ofFn f)[i] = ∏ j ∈ Finset.filter (fun j => ↑j < i + 1) univ, f j

Proof state:
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j ∈ Finset.filter (fun j => ↑j < i) univ, f j
h : ¬i < n
A : take i (ofFn f) = take i.succ (ofFn f)
⊢ ∀ (j : Fin n), (↑j < i.succ) = (↑j < i)

Tactic:
intro j

Result:
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j ∈ Finset.filter (fun j => ↑j < i) univ, f j
h : ¬i < n
A : take i (ofFn f) = take i.succ (ofFn f)
j : Fin n
⊢ (↑j < i.succ) = (↑j < i)

Proof state:
case succ
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j ∈ Finset.filter (fun j => ↑j < i) univ, f j
⊢ (take (i + 1) (ofFn f)).prod = ∏ j ∈ Finset.filter (fun j => ↑j < i + 1) univ, f j

Tactic:
by_cases h : i < n

Result:
case pos
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j ∈ Finset.filter (fun j => ↑j < i) univ, f j
h : i < n
⊢ (take (i + 1) (ofFn f)).prod = ∏ j ∈ Finset.filter (fun j => ↑j < i + 1) univ, f j

case neg
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : (take i (ofFn f)).prod = ∏ j ∈ Finset.filter (fun j => ↑j < i) univ, f j
h : ¬i < n
⊢ (take (i + 1) (ofFn f)).prod = ∏ j ∈ Finset.filter (fun j => ↑j < i + 1) univ, f j