ι : Type ?u.50139
α✝ : Type ?u.50142
M : Type ?u.50145
N : Type ?u.50148
P : Type ?u.50151
M₀ : Type ?u.50154
G : Type ?u.50157
R : Type ?u.50160
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : Monoid P
l l₁ l₂ : List M
a : M
α : Type u_1
inst✝ : CommMonoid α
L : List α
h : IsUnit (prod L)
⊢ ∀ (m : α), m ∈ L → IsUnit m
ι : Type ?u.50139
α✝ : Type ?u.50142
M : Type ?u.50145
N : Type ?u.50148
P : Type ?u.50151
M₀ : Type ?u.50154
G : Type ?u.50157
R : Type ?u.50160
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : Monoid P
l l₁ l₂ : List M
a : M
α : Type u_1
inst✝ : CommMonoid α
L : List α
⊢ IsUnit (prod L) ↔ ∀ (m : α), m ∈ L → IsUnit m
refine' ⟨fun h => _, prod_isUnit⟩
case nil
ι : Type ?u.50139
α✝ : Type ?u.50142
M : Type ?u.50145
N : Type ?u.50148
P : Type ?u.50151
M₀ : Type ?u.50154
G : Type ?u.50157
R : Type ?u.50160
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : Monoid P
l l₁ l₂ : List M
a : M
α : Type u_1
inst✝ : CommMonoid α
L : List α
h✝ : IsUnit (prod L)
h : IsUnit (prod [])
⊢ ∀ (m : α), m ∈ [] → IsUnit m

case cons
ι : Type ?u.50139
α✝ : Type ?u.50142
M : Type ?u.50145
N : Type ?u.50148
P : Type ?u.50151
M₀ : Type ?u.50154
G : Type ?u.50157
R : Type ?u.50160
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : Monoid P
l l₁ l₂ : List M
a : M
α : Type u_1
inst✝ : CommMonoid α
L✝ : List α
h✝ : IsUnit (prod L✝)
m : α
L : List α
ih : IsUnit (prod L) → ∀ (m : α), m ∈ L → IsUnit m
h : IsUnit (prod (m :: L))
⊢ ∀ (m_1 : α), m_1 ∈ m :: L → IsUnit m_1
ι : Type ?u.50139
α✝ : Type ?u.50142
M : Type ?u.50145
N : Type ?u.50148
P : Type ?u.50151
M₀ : Type ?u.50154
G : Type ?u.50157
R : Type ?u.50160
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : Monoid P
l l₁ l₂ : List M
a : M
α : Type u_1
inst✝ : CommMonoid α
L : List α
h : IsUnit (prod L)
⊢ ∀ (m : α), m ∈ L → IsUnit m
induction' L with m L ih
case cons
ι : Type ?u.50139
α✝ : Type ?u.50142
M : Type ?u.50145
N : Type ?u.50148
P : Type ?u.50151
M₀ : Type ?u.50154
G : Type ?u.50157
R : Type ?u.50160
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : Monoid P
l l₁ l₂ : List M
a : M
α : Type u_1
inst✝ : CommMonoid α
L✝ : List α
h✝ : IsUnit (prod L✝)
m : α
L : List α
ih : IsUnit (prod L) → ∀ (m : α), m ∈ L → IsUnit m
h : IsUnit m ∧ IsUnit (prod L)
⊢ ∀ (m_1 : α), m_1 ∈ m :: L → IsUnit m_1
case cons
ι : Type ?u.50139
α✝ : Type ?u.50142
M : Type ?u.50145
N : Type ?u.50148
P : Type ?u.50151
M₀ : Type ?u.50154
G : Type ?u.50157
R : Type ?u.50160
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : Monoid P
l l₁ l₂ : List M
a : M
α : Type u_1
inst✝ : CommMonoid α
L✝ : List α
h✝ : IsUnit (prod L✝)
m : α
L : List α
ih : IsUnit (prod L) → ∀ (m : α), m ∈ L → IsUnit m
h : IsUnit (prod (m :: L))
⊢ ∀ (m_1 : α), m_1 ∈ m :: L → IsUnit m_1
rw [prod_cons, IsUnit.mul_iff] at h
no goals
case cons
ι : Type ?u.50139
α✝ : Type ?u.50142
M : Type ?u.50145
N : Type ?u.50148
P : Type ?u.50151
M₀ : Type ?u.50154
G : Type ?u.50157
R : Type ?u.50160
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : Monoid P
l l₁ l₂ : List M
a : M
α : Type u_1
inst✝ : CommMonoid α
L✝ : List α
h✝ : IsUnit (prod L✝)
m : α
L : List α
ih : IsUnit (prod L) → ∀ (m : α), m ∈ L → IsUnit m
h : IsUnit m ∧ IsUnit (prod L)
⊢ ∀ (m_1 : α), m_1 ∈ m :: L → IsUnit m_1
exact fun m' h' => Or.elim (eq_or_mem_of_mem_cons h') (fun H => H.substr h.1) fun H => ih h.2 _ H
no goals
case nil
ι : Type ?u.50139
α✝ : Type ?u.50142
M : Type ?u.50145
N : Type ?u.50148
P : Type ?u.50151
M₀ : Type ?u.50154
G : Type ?u.50157
R : Type ?u.50160
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : Monoid P
l l₁ l₂ : List M
a : M
α : Type u_1
inst✝ : CommMonoid α
L : List α
h✝ : IsUnit (prod L)
h : IsUnit (prod [])
⊢ ∀ (m : α), m ∈ [] → IsUnit m
exact fun m' h' => False.elim (not_mem_nil m' h')