case nil
ι : Type ?u.143653
α : Type ?u.143656
M : Type u_1
N : Type ?u.143662
P : Type ?u.143665
M₀ : Type ?u.143668
G : Type ?u.143671
R : Type ?u.143674
inst✝ : Monoid M
l : List M
hl✝ : ∀ (x : M), x ∈ l → x = 1
hl : ∀ (x : M), x ∈ [] → x = 1
⊢ prod [] = 1

case cons
ι : Type ?u.143653
α : Type ?u.143656
M : Type u_1
N : Type ?u.143662
P : Type ?u.143665
M₀ : Type ?u.143668
G : Type ?u.143671
R : Type ?u.143674
inst✝ : Monoid M
l✝ : List M
hl✝ : ∀ (x : M), x ∈ l✝ → x = 1
i : M
l : List M
hil : (∀ (x : M), x ∈ l → x = 1) → prod l = 1
hl : ∀ (x : M), x ∈ i :: l → x = 1
⊢ prod (i :: l) = 1
ι : Type ?u.143653
α : Type ?u.143656
M : Type u_1
N : Type ?u.143662
P : Type ?u.143665
M₀ : Type ?u.143668
G : Type ?u.143671
R : Type ?u.143674
inst✝ : Monoid M
l : List M
hl : ∀ (x : M), x ∈ l → x = 1
⊢ prod l = 1
induction' l with i l hil
no goals
case cons
ι : Type ?u.143653
α : Type ?u.143656
M : Type u_1
N : Type ?u.143662
P : Type ?u.143665
M₀ : Type ?u.143668
G : Type ?u.143671
R : Type ?u.143674
inst✝ : Monoid M
l✝ : List M
hl✝ : ∀ (x : M), x ∈ l✝ → x = 1
i : M
l : List M
hil : (∀ (x : M), x ∈ l → x = 1) → prod l = 1
hl : ∀ (x : M), x ∈ i :: l → x = 1
⊢ prod (i :: l) = 1
rw [List.prod_cons, hil fun x hx => hl _ (mem_cons_of_mem i hx), hl _ (mem_cons_self i l),
  one_mul]
no goals
case nil
ι : Type ?u.143653
α : Type ?u.143656
M : Type u_1
N : Type ?u.143662
P : Type ?u.143665
M₀ : Type ?u.143668
G : Type ?u.143671
R : Type ?u.143674
inst✝ : Monoid M
l : List M
hl✝ : ∀ (x : M), x ∈ l → x = 1
hl : ∀ (x : M), x ∈ [] → x = 1
⊢ prod [] = 1
rfl