no goals
case zero
α : Type u_1
β : Type ?u.208372
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
⊢ prod (take Nat.zero (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < Nat.zero) univ, f j
simp
case pos
α : Type u_1
β : Type ?u.208372
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : prod (take i (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < i) univ, f j
h : i < n
⊢ prod (take (Nat.succ i) (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < Nat.succ i) univ, f j

case neg
α : Type u_1
β : Type ?u.208372
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : prod (take i (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < i) univ, f j
h : ¬i < n
⊢ prod (take (Nat.succ i) (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < Nat.succ i) univ, f j
case succ
α : Type u_1
β : Type ?u.208372
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : prod (take i (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < i) univ, f j
⊢ prod (take (Nat.succ i) (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < Nat.succ i) univ, f j
by_cases h : i < n
case pos
α : Type u_1
β : Type ?u.208372
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : prod (take i (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < i) univ, f j
h : i < n
this : i < length (ofFn f)
⊢ prod (take (Nat.succ i) (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < Nat.succ i) univ, f j
case pos
α : Type u_1
β : Type ?u.208372
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : prod (take i (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < i) univ, f j
h : i < n
⊢ prod (take (Nat.succ i) (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < Nat.succ i) univ, f j
have : i < length (ofFn f) := by rwa [length_ofFn f]
case pos
α : Type u_1
β : Type ?u.208372
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : prod (take i (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < i) univ, f j
h : i < n
this : i < length (ofFn f)
⊢ prod (take i (ofFn f)) * nthLe (ofFn f) i this = ∏ j in Finset.filter (fun j => ↑j < Nat.succ i) univ, f j
case pos
α : Type u_1
β : Type ?u.208372
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : prod (take i (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < i) univ, f j
h : i < n
this : i < length (ofFn f)
⊢ prod (take (Nat.succ i) (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < Nat.succ i) univ, f j
rw [prod_take_succ _ _ this]
case pos
α : Type u_1
β : Type ?u.208372
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : prod (take i (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < i) univ, f j
h : i < n
this : i < length (ofFn f)
A : Finset.filter (fun j => ↑j < i + 1) univ = Finset.filter (fun j => ↑j < i) univ ∪ {{ val := i, isLt := h }}
⊢ prod (take i (ofFn f)) * nthLe (ofFn f) i this = ∏ j in Finset.filter (fun j => ↑j < Nat.succ i) univ, f j
case pos
α : Type u_1
β : Type ?u.208372
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : prod (take i (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < i) univ, f j
h : i < n
this : i < length (ofFn f)
⊢ prod (take i (ofFn f)) * nthLe (ofFn f) i this = ∏ j in Finset.filter (fun j => ↑j < Nat.succ i) univ, f j
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]
case pos
α : Type u_1
β : Type ?u.208372
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : prod (take i (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < i) univ, f j
h : i < n
this : i < length (ofFn f)
A : Finset.filter (fun j => ↑j < i + 1) univ = Finset.filter (fun j => ↑j < i) univ ∪ {{ val := i, isLt := h }}
B : _root_.Disjoint (Finset.filter (fun j => ↑j < i) univ) {{ val := i, isLt := h }}
⊢ prod (take i (ofFn f)) * nthLe (ofFn f) i this = ∏ j in Finset.filter (fun j => ↑j < Nat.succ i) univ, f j
case pos
α : Type u_1
β : Type ?u.208372
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : prod (take i (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < i) univ, f j
h : i < n
this : i < length (ofFn f)
A : Finset.filter (fun j => ↑j < i + 1) univ = Finset.filter (fun j => ↑j < i) univ ∪ {{ val := i, isLt := h }}
⊢ prod (take i (ofFn f)) * nthLe (ofFn f) i this = ∏ j in Finset.filter (fun j => ↑j < Nat.succ i) univ, f j
have B : _root_.Disjoint (Finset.filter (fun j : Fin n => j.val < i) Finset.univ)
    (singleton (⟨i, h⟩ : Fin n)) := by simp
case pos
α : Type u_1
β : Type ?u.208372
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : prod (take i (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < i) univ, f j
h : i < n
this : i < length (ofFn f)
A : Finset.filter (fun j => ↑j < i + 1) univ = Finset.filter (fun j => ↑j < i) univ ∪ {{ val := i, isLt := h }}
B : _root_.Disjoint (Finset.filter (fun j => ↑j < i) univ) {{ val := i, isLt := h }}
⊢ (∏ j in Finset.filter (fun j => ↑j < i) univ, f j) * nthLe (ofFn f) i this =
    (∏ x in Finset.filter (fun j => ↑j < i) univ, f x) * ∏ x in {{ val := i, isLt := h }}, f x
case pos
α : Type u_1
β : Type ?u.208372
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : prod (take i (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < i) univ, f j
h : i < n
this : i < length (ofFn f)
A : Finset.filter (fun j => ↑j < i + 1) univ = Finset.filter (fun j => ↑j < i) univ ∪ {{ val := i, isLt := h }}
B : _root_.Disjoint (Finset.filter (fun j => ↑j < i) univ) {{ val := i, isLt := h }}
⊢ prod (take i (ofFn f)) * nthLe (ofFn f) i this = ∏ j in Finset.filter (fun j => ↑j < Nat.succ i) univ, f j
rw [A, Finset.prod_union B, IH]
no goals
case pos
α : Type u_1
β : Type ?u.208372
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : prod (take i (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < i) univ, f j
h : i < n
this : i < length (ofFn f)
A : Finset.filter (fun j => ↑j < i + 1) univ = Finset.filter (fun j => ↑j < i) univ ∪ {{ val := i, isLt := h }}
B : _root_.Disjoint (Finset.filter (fun j => ↑j < i) univ) {{ val := i, isLt := h }}
⊢ (∏ j in Finset.filter (fun j => ↑j < i) univ, f j) * nthLe (ofFn f) i this =
    (∏ x in Finset.filter (fun j => ↑j < i) univ, f x) * ∏ x in {{ val := i, isLt := h }}, f x
simp
no goals
α : Type u_1
β : Type ?u.208372
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : prod (take i (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < i) univ, f j
h : i < n
⊢ i < length (ofFn f)
rwa [length_ofFn f]
case a.mk
α : Type u_1
β : Type ?u.208372
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : prod (take i (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < i) univ, f j
h : i < n
this : i < length (ofFn f)
val✝ : ℕ
isLt✝ : val✝ < n
⊢ { val := val✝, isLt := isLt✝ } ∈ Finset.filter (fun j => ↑j < i + 1) univ ↔
    { val := val✝, isLt := isLt✝ } ∈ Finset.filter (fun j => ↑j < i) univ ∪ {{ val := i, isLt := h }}
α : Type u_1
β : Type ?u.208372
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : prod (take i (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < i) univ, f j
h : i < n
this : i < length (ofFn f)
⊢ Finset.filter (fun j => ↑j < i + 1) univ = Finset.filter (fun j => ↑j < i) univ ∪ {{ val := i, isLt := h }}
ext ⟨_, _⟩
no goals
case a.mk
α : Type u_1
β : Type ?u.208372
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : prod (take i (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < i) univ, f j
h : i < n
this : i < length (ofFn f)
val✝ : ℕ
isLt✝ : val✝ < n
⊢ { val := val✝, isLt := isLt✝ } ∈ Finset.filter (fun j => ↑j < i + 1) univ ↔
    { val := val✝, isLt := isLt✝ } ∈ Finset.filter (fun j => ↑j < i) univ ∪ {{ val := i, isLt := h }}
simp [Nat.lt_succ_iff_lt_or_eq]
no goals
α : Type u_1
β : Type ?u.208372
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : prod (take i (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < i) univ, f j
h : i < n
this : i < length (ofFn f)
A : Finset.filter (fun j => ↑j < i + 1) univ = Finset.filter (fun j => ↑j < i) univ ∪ {{ val := i, isLt := h }}
⊢ _root_.Disjoint (Finset.filter (fun j => ↑j < i) univ) {{ val := i, isLt := h }}
simp
case neg
α : Type u_1
β : Type ?u.208372
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : prod (take i (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < i) univ, f j
h : ¬i < n
A : take i (ofFn f) = take (Nat.succ i) (ofFn f)
⊢ prod (take (Nat.succ i) (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < Nat.succ i) univ, f j
case neg
α : Type u_1
β : Type ?u.208372
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : prod (take i (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < i) univ, f j
h : ¬i < n
⊢ prod (take (Nat.succ i) (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < Nat.succ i) univ, f j
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_all_of_le this, take_all_of_le (le_trans this (Nat.le_succ _))]
case neg
α : Type u_1
β : Type ?u.208372
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : prod (take i (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < i) univ, f j
h : ¬i < n
A : take i (ofFn f) = take (Nat.succ i) (ofFn f)
B : ∀ (j : Fin n), (↑j < Nat.succ i) = (↑j < i)
⊢ prod (take (Nat.succ i) (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < Nat.succ i) univ, f j
case neg
α : Type u_1
β : Type ?u.208372
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : prod (take i (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < i) univ, f j
h : ¬i < n
A : take i (ofFn f) = take (Nat.succ i) (ofFn f)
⊢ prod (take (Nat.succ i) (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < Nat.succ i) univ, f j
have B : ∀ j : Fin n, ((j : ℕ) < i.succ) = ((j : ℕ) < i) := by
  intro j
  have : (j : ℕ) < i := lt_of_lt_of_le j.2 (not_lt.mp h)
  simp [this, lt_trans this (Nat.lt_succ_self _)]
no goals
case neg
α : Type u_1
β : Type ?u.208372
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : prod (take i (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < i) univ, f j
h : ¬i < n
A : take i (ofFn f) = take (Nat.succ i) (ofFn f)
B : ∀ (j : Fin n), (↑j < Nat.succ i) = (↑j < i)
⊢ prod (take (Nat.succ i) (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < Nat.succ i) univ, f j
simp [← A, B, IH]
α : Type u_1
β : Type ?u.208372
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : prod (take i (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < i) univ, f j
h : ¬i < length (ofFn f)
⊢ take i (ofFn f) = take (Nat.succ i) (ofFn f)
α : Type u_1
β : Type ?u.208372
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : prod (take i (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < i) univ, f j
h : ¬i < n
⊢ take i (ofFn f) = take (Nat.succ i) (ofFn f)
rw [← length_ofFn f] at h
α : Type u_1
β : Type ?u.208372
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : prod (take i (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < i) univ, f j
h : ¬i < length (ofFn f)
this : length (ofFn f) ≤ i
⊢ take i (ofFn f) = take (Nat.succ i) (ofFn f)
α : Type u_1
β : Type ?u.208372
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : prod (take i (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < i) univ, f j
h : ¬i < length (ofFn f)
⊢ take i (ofFn f) = take (Nat.succ i) (ofFn f)
have : length (ofFn f) ≤ i := not_lt.mp h
no goals
α : Type u_1
β : Type ?u.208372
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : prod (take i (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < i) univ, f j
h : ¬i < length (ofFn f)
this : length (ofFn f) ≤ i
⊢ take i (ofFn f) = take (Nat.succ i) (ofFn f)
rw [take_all_of_le this, take_all_of_le (le_trans this (Nat.le_succ _))]
α : Type u_1
β : Type ?u.208372
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : prod (take i (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < i) univ, f j
h : ¬i < n
A : take i (ofFn f) = take (Nat.succ i) (ofFn f)
j : Fin n
⊢ (↑j < Nat.succ i) = (↑j < i)
α : Type u_1
β : Type ?u.208372
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : prod (take i (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < i) univ, f j
h : ¬i < n
A : take i (ofFn f) = take (Nat.succ i) (ofFn f)
⊢ ∀ (j : Fin n), (↑j < Nat.succ i) = (↑j < i)
intro j
α : Type u_1
β : Type ?u.208372
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : prod (take i (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < i) univ, f j
h : ¬i < n
A : take i (ofFn f) = take (Nat.succ i) (ofFn f)
j : Fin n
this : ↑j < i
⊢ (↑j < Nat.succ i) = (↑j < i)
α : Type u_1
β : Type ?u.208372
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : prod (take i (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < i) univ, f j
h : ¬i < n
A : take i (ofFn f) = take (Nat.succ i) (ofFn f)
j : Fin n
⊢ (↑j < Nat.succ i) = (↑j < i)
have : (j : ℕ) < i := lt_of_lt_of_le j.2 (not_lt.mp h)
no goals
α : Type u_1
β : Type ?u.208372
inst✝ : CommMonoid α
n : ℕ
f : Fin n → α
i : ℕ
IH : prod (take i (ofFn f)) = ∏ j in Finset.filter (fun j => ↑j < i) univ, f j
h : ¬i < n
A : take i (ofFn f) = take (Nat.succ i) (ofFn f)
j : Fin n
this : ↑j < i
⊢ (↑j < Nat.succ i) = (↑j < i)
simp [this, lt_trans this (Nat.lt_succ_self _)]