case mp
α : Type u_1
β : Type ?u.94330
γ : Type ?u.94333
δ : Type ?u.94336
inst✝ : Monoid α
a b : α
⊢ Irreducible (a * b) → Irreducible a ∧ IsUnit b ∨ Irreducible b ∧ IsUnit a

case mpr
α : Type u_1
β : Type ?u.94330
γ : Type ?u.94333
δ : Type ?u.94336
inst✝ : Monoid α
a b : α
⊢ Irreducible a ∧ IsUnit b ∨ Irreducible b ∧ IsUnit a → Irreducible (a * b)
α : Type u_1
β : Type ?u.94330
γ : Type ?u.94333
δ : Type ?u.94336
inst✝ : Monoid α
a b : α
⊢ Irreducible (a * b) ↔ Irreducible a ∧ IsUnit b ∨ Irreducible b ∧ IsUnit a
constructor
case mp.refine'_1
α : Type u_1
β : Type ?u.94330
γ : Type ?u.94333
δ : Type ?u.94336
inst✝ : Monoid α
a b : α
h : Irreducible (a * b)
h' : IsUnit b
⊢ Irreducible a

case mp.refine'_2
α : Type u_1
β : Type ?u.94330
γ : Type ?u.94333
δ : Type ?u.94336
inst✝ : Monoid α
a b : α
h : Irreducible (a * b)
h' : IsUnit a
⊢ Irreducible b
case mp
α : Type u_1
β : Type ?u.94330
γ : Type ?u.94333
δ : Type ?u.94336
inst✝ : Monoid α
a b : α
⊢ Irreducible (a * b) → Irreducible a ∧ IsUnit b ∨ Irreducible b ∧ IsUnit a
refine' fun h => Or.imp (fun h' => ⟨_, h'⟩) (fun h' => ⟨_, h'⟩) (h.isUnit_or_isUnit rfl).symm
no goals
case mp.refine'_1
α : Type u_1
β : Type ?u.94330
γ : Type ?u.94333
δ : Type ?u.94336
inst✝ : Monoid α
a b : α
h : Irreducible (a * b)
h' : IsUnit b
⊢ Irreducible a
rwa [irreducible_mul_isUnit h'] at h
no goals
case mp.refine'_2
α : Type u_1
β : Type ?u.94330
γ : Type ?u.94333
δ : Type ?u.94336
inst✝ : Monoid α
a b : α
h : Irreducible (a * b)
h' : IsUnit a
⊢ Irreducible b
rwa [irreducible_isUnit_mul h'] at h
case mpr.inl.intro
α : Type u_1
β : Type ?u.94330
γ : Type ?u.94333
δ : Type ?u.94336
inst✝ : Monoid α
a b : α
ha : Irreducible a
hb : IsUnit b
⊢ Irreducible (a * b)

case mpr.inr.intro
α : Type u_1
β : Type ?u.94330
γ : Type ?u.94333
δ : Type ?u.94336
inst✝ : Monoid α
a b : α
hb : Irreducible b
ha : IsUnit a
⊢ Irreducible (a * b)
case mpr
α : Type u_1
β : Type ?u.94330
γ : Type ?u.94333
δ : Type ?u.94336
inst✝ : Monoid α
a b : α
⊢ Irreducible a ∧ IsUnit b ∨ Irreducible b ∧ IsUnit a → Irreducible (a * b)
rintro (⟨ha, hb⟩ | ⟨hb, ha⟩)
no goals
case mpr.inl.intro
α : Type u_1
β : Type ?u.94330
γ : Type ?u.94333
δ : Type ?u.94336
inst✝ : Monoid α
a b : α
ha : Irreducible a
hb : IsUnit b
⊢ Irreducible (a * b)
rwa [irreducible_mul_isUnit hb]
no goals
case mpr.inr.intro
α : Type u_1
β : Type ?u.94330
γ : Type ?u.94333
δ : Type ?u.94336
inst✝ : Monoid α
a b : α
hb : Irreducible b
ha : IsUnit a
⊢ Irreducible (a * b)
rwa [irreducible_isUnit_mul ha]