-- Mathlib/Algebra/DirectSum/Ring.lean
theorem ofList_dProd {α} (l : List α) (fι : α → ι) (fA : ∀ a, A (fι a)) :
    of A _ (l.dProd fι fA) = (l.map fun a => of A (fι a) (fA a)).prod

Proof state:
case cons
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
α : Type u_3
fι : α → ι
fA : (a : α) → A (fι a)
head : α
tail : List α
ih : (of A (tail.dProdIndex fι)) (tail.dProd fι fA) = (List.map (fun a => (of A (fι a)) (fA a)) tail).prod
⊢ (of A ((head :: tail).dProdIndex fι)) ((head :: tail).dProd fι fA) =
    (List.map (fun a => (of A (fι a)) (fA a)) (head :: tail)).prod

Tactic:
simp only [List.map_cons, List.prod_cons, List.dProd_cons, ← ih]

Result:
case cons
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
α : Type u_3
fι : α → ι
fA : (a : α) → A (fι a)
head : α
tail : List α
ih : (of A (tail.dProdIndex fι)) (tail.dProd fι fA) = (List.map (fun a => (of A (fι a)) (fA a)) tail).prod
⊢ (of A ((head :: tail).dProdIndex fι)) (GradedMonoid.GMul.mul (fA head) (tail.dProd fι fA)) =
    (of A (fι head)) (fA head) * (of A (tail.dProdIndex fι)) (tail.dProd fι fA)

Proof state:
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
α : Type u_3
l : List α
fι : α → ι
fA : (a : α) → A (fι a)
⊢ (of A (l.dProdIndex fι)) (l.dProd fι fA) = (List.map (fun a => (of A (fι a)) (fA a)) l).prod

Tactic:
induction l with
| nil => simp only [List.map_nil, List.prod_nil, List.dProd_nil]; rfl
| cons head tail =>
  rename_i ih
  simp only [List.map_cons, List.prod_cons, List.dProd_cons, ← ih]
  rw [DirectSum.of_mul_of (fA head)]
  rfl

Result:
no goals

Proof state:
case nil
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
α : Type u_3
fι : α → ι
fA : (a : α) → A (fι a)
⊢ (of A ([].dProdIndex fι)) ([].dProd fι fA) = (List.map (fun a => (of A (fι a)) (fA a)) []).prod

Tactic:
simp only [List.map_nil, List.prod_nil, List.dProd_nil]

Result:
case nil
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
α : Type u_3
fι : α → ι
fA : (a : α) → A (fι a)
⊢ (of A ([].dProdIndex fι)) GradedMonoid.GOne.one = 1

Proof state:
case cons
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
α : Type u_3
fι : α → ι
fA : (a : α) → A (fι a)
head : α
tail : List α
ih : (of A (tail.dProdIndex fι)) (tail.dProd fι fA) = (List.map (fun a => (of A (fι a)) (fA a)) tail).prod
⊢ (of A ((head :: tail).dProdIndex fι)) (GradedMonoid.GMul.mul (fA head) (tail.dProd fι fA)) =
    (of A (fι head + tail.dProdIndex fι)) (GradedMonoid.GMul.mul (fA head) (tail.dProd fι fA))

Tactic:
rfl

Result:
no goals

Proof state:
case cons
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
α : Type u_3
fι : α → ι
fA : (a : α) → A (fι a)
head : α
tail : List α
tail_ih✝ : (of A (tail.dProdIndex fι)) (tail.dProd fι fA) = (List.map (fun a => (of A (fι a)) (fA a)) tail).prod
⊢ (of A ((head :: tail).dProdIndex fι)) ((head :: tail).dProd fι fA) =
    (List.map (fun a => (of A (fι a)) (fA a)) (head :: tail)).prod

Tactic:
rename_i ih

Result:
case cons
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
α : Type u_3
fι : α → ι
fA : (a : α) → A (fι a)
head : α
tail : List α
ih : (of A (tail.dProdIndex fι)) (tail.dProd fι fA) = (List.map (fun a => (of A (fι a)) (fA a)) tail).prod
⊢ (of A ((head :: tail).dProdIndex fι)) ((head :: tail).dProd fι fA) =
    (List.map (fun a => (of A (fι a)) (fA a)) (head :: tail)).prod

Proof state:
case cons
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
α : Type u_3
fι : α → ι
fA : (a : α) → A (fι a)
head : α
tail : List α
ih : (of A (tail.dProdIndex fι)) (tail.dProd fι fA) = (List.map (fun a => (of A (fι a)) (fA a)) tail).prod
⊢ (of A ((head :: tail).dProdIndex fι)) (GradedMonoid.GMul.mul (fA head) (tail.dProd fι fA)) =
    (of A (fι head)) (fA head) * (of A (tail.dProdIndex fι)) (tail.dProd fι fA)

Tactic:
rw [DirectSum.of_mul_of (fA head)]

Result:
case cons
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
α : Type u_3
fι : α → ι
fA : (a : α) → A (fι a)
head : α
tail : List α
ih : (of A (tail.dProdIndex fι)) (tail.dProd fι fA) = (List.map (fun a => (of A (fι a)) (fA a)) tail).prod
⊢ (of A ((head :: tail).dProdIndex fι)) (GradedMonoid.GMul.mul (fA head) (tail.dProd fι fA)) =
    (of A (fι head + tail.dProdIndex fι)) (GradedMonoid.GMul.mul (fA head) (tail.dProd fι fA))

Proof state:
case nil
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
α : Type u_3
fι : α → ι
fA : (a : α) → A (fι a)
⊢ (of A ([].dProdIndex fι)) GradedMonoid.GOne.one = 1

Tactic:
rfl

Result:
no goals