α : Type ?u.56017
β : Type u_1
γ : Type ?u.56023
inst✝ : CommMonoid β
n : ℕ
c : Fin n → β
⊢ ∀ (x : Fin n), x ∈ univ → c x = if h : ↑x < n then c { val := ↑x, isLt := h } else 1
α : Type ?u.56017
β : Type u_1
γ : Type ?u.56023
inst✝ : CommMonoid β
n : ℕ
c : Fin n → β
⊢ ∏ i : Fin n, c i = ∏ i in range n, if h : i < n then c { val := i, isLt := h } else 1
rw [← Fin.prod_univ_eq_prod_range, Finset.prod_congr rfl]
case mk
α : Type ?u.56017
β : Type u_1
γ : Type ?u.56023
inst✝ : CommMonoid β
n : ℕ
c : Fin n → β
i : ℕ
hi : i < n
a✝ : { val := i, isLt := hi } ∈ univ
⊢ c { val := i, isLt := hi } =
    if h : ↑{ val := i, isLt := hi } < n then c { val := ↑{ val := i, isLt := hi }, isLt := h } else 1
α : Type ?u.56017
β : Type u_1
γ : Type ?u.56023
inst✝ : CommMonoid β
n : ℕ
c : Fin n → β
⊢ ∀ (x : Fin n), x ∈ univ → c x = if h : ↑x < n then c { val := ↑x, isLt := h } else 1
rintro ⟨i, hi⟩ _
no goals
case mk
α : Type ?u.56017
β : Type u_1
γ : Type ?u.56023
inst✝ : CommMonoid β
n : ℕ
c : Fin n → β
i : ℕ
hi : i < n
a✝ : { val := i, isLt := hi } ∈ univ
⊢ c { val := i, isLt := hi } =
    if h : ↑{ val := i, isLt := hi } < n then c { val := ↑{ val := i, isLt := hi }, isLt := h } else 1
simp only [hi, dif_pos]