α✝ : Type ?u.79346
β : Type ?u.79349
γ : Type ?u.79352
δ : Type ?u.79355
α : Type u_1
inst✝ : Monoid α
x : α
h : ¬IsUnit x
this : (p : Prop) → Decidable p
⊢ Irreducible x ∨ ∃ a b, ¬IsUnit a ∧ ¬IsUnit b ∧ a * b = x
α✝ : Type ?u.79346
β : Type ?u.79349
γ : Type ?u.79352
δ : Type ?u.79355
α : Type u_1
inst✝ : Monoid α
x : α
h : ¬IsUnit x
⊢ Irreducible x ∨ ∃ a b, ¬IsUnit a ∧ ¬IsUnit b ∧ a * b = x
haveI := Classical.dec
α✝ : Type ?u.79346
β : Type ?u.79349
γ : Type ?u.79352
δ : Type ?u.79355
α : Type u_1
inst✝ : Monoid α
x : α
h : ¬IsUnit x
this : (p : Prop) → Decidable p
H : ¬∃ a b, ¬IsUnit a ∧ ¬IsUnit b ∧ a * b = x
⊢ Irreducible x
α✝ : Type ?u.79346
β : Type ?u.79349
γ : Type ?u.79352
δ : Type ?u.79355
α : Type u_1
inst✝ : Monoid α
x : α
h : ¬IsUnit x
this : (p : Prop) → Decidable p
⊢ Irreducible x ∨ ∃ a b, ¬IsUnit a ∧ ¬IsUnit b ∧ a * b = x
refine' or_iff_not_imp_right.2 fun H => _
α✝ : Type ?u.79346
β : Type ?u.79349
γ : Type ?u.79352
δ : Type ?u.79355
α : Type u_1
inst✝ : Monoid α
x : α
h : ¬IsUnit x
this : (p : Prop) → Decidable p
H : ∀ (x_1 : α), ¬IsUnit x_1 → ∀ (x_2 : α), ¬IsUnit x_2 → ¬x_1 * x_2 = x
⊢ ∀ (a b : α), x = a * b → IsUnit a ∨ IsUnit b
α✝ : Type ?u.79346
β : Type ?u.79349
γ : Type ?u.79352
δ : Type ?u.79355
α : Type u_1
inst✝ : Monoid α
x : α
h : ¬IsUnit x
this : (p : Prop) → Decidable p
H : ¬∃ a b, ¬IsUnit a ∧ ¬IsUnit b ∧ a * b = x
⊢ Irreducible x
simp [h, irreducible_iff] at H⊢
α✝ : Type ?u.79346
β : Type ?u.79349
γ : Type ?u.79352
δ : Type ?u.79355
α : Type u_1
inst✝ : Monoid α
x : α
h✝ : ¬IsUnit x
this : (p : Prop) → Decidable p
H : ∀ (x_1 : α), ¬IsUnit x_1 → ∀ (x_2 : α), ¬IsUnit x_2 → ¬x_1 * x_2 = x
a b : α
h : x = a * b
o : ¬(IsUnit a ∨ IsUnit b)
⊢ False
α✝ : Type ?u.79346
β : Type ?u.79349
γ : Type ?u.79352
δ : Type ?u.79355
α : Type u_1
inst✝ : Monoid α
x : α
h : ¬IsUnit x
this : (p : Prop) → Decidable p
H : ∀ (x_1 : α), ¬IsUnit x_1 → ∀ (x_2 : α), ¬IsUnit x_2 → ¬x_1 * x_2 = x
⊢ ∀ (a b : α), x = a * b → IsUnit a ∨ IsUnit b
refine' fun a b h => by_contradiction fun o => _
α✝ : Type ?u.79346
β : Type ?u.79349
γ : Type ?u.79352
δ : Type ?u.79355
α : Type u_1
inst✝ : Monoid α
x : α
h✝ : ¬IsUnit x
this : (p : Prop) → Decidable p
H : ∀ (x_1 : α), ¬IsUnit x_1 → ∀ (x_2 : α), ¬IsUnit x_2 → ¬x_1 * x_2 = x
a b : α
h : x = a * b
o : ¬IsUnit a ∧ ¬IsUnit b
⊢ False
α✝ : Type ?u.79346
β : Type ?u.79349
γ : Type ?u.79352
δ : Type ?u.79355
α : Type u_1
inst✝ : Monoid α
x : α
h✝ : ¬IsUnit x
this : (p : Prop) → Decidable p
H : ∀ (x_1 : α), ¬IsUnit x_1 → ∀ (x_2 : α), ¬IsUnit x_2 → ¬x_1 * x_2 = x
a b : α
h : x = a * b
o : ¬(IsUnit a ∨ IsUnit b)
⊢ False
simp [not_or] at o
no goals
α✝ : Type ?u.79346
β : Type ?u.79349
γ : Type ?u.79352
δ : Type ?u.79355
α : Type u_1
inst✝ : Monoid α
x : α
h✝ : ¬IsUnit x
this : (p : Prop) → Decidable p
H : ∀ (x_1 : α), ¬IsUnit x_1 → ∀ (x_2 : α), ¬IsUnit x_2 → ¬x_1 * x_2 = x
a b : α
h : x = a * b
o : ¬IsUnit a ∧ ¬IsUnit b
⊢ False
exact H _ o.1 _ o.2 h.symm