-- Mathlib/Algebra/Prime/Defs.lean
theorem irreducible_or_factor {M} [Monoid M] (x : M) (h : ¬IsUnit x) :
    Irreducible x ∨ ∃ a b, ¬IsUnit a ∧ ¬IsUnit b ∧ a * b = x

Proof state:
M : Type u_2
inst✝ : Monoid M
x : M
h : ¬IsUnit x
⊢ Irreducible x ∨ ∃ a b, ¬IsUnit a ∧ ¬IsUnit b ∧ a * b = x

Tactic:
haveI := Classical.dec

Result:
M : Type u_2
inst✝ : Monoid M
x : M
h : ¬IsUnit x
this : (p : Prop) → Decidable p
⊢ Irreducible x ∨ ∃ a b, ¬IsUnit a ∧ ¬IsUnit b ∧ a * b = x

Proof state:
M : Type u_2
inst✝ : Monoid M
x : M
h✝ : ¬IsUnit x
this : (p : Prop) → Decidable p
H : ∀ (x_1 : M), ¬IsUnit x_1 → ∀ (x_2 : M), ¬IsUnit x_2 → ¬x_1 * x_2 = x
a b : M
h : x = a * b
o : ¬(IsUnit a ∨ IsUnit b)
⊢ False

Tactic:
simp only [not_or] at o

Result:
M : Type u_2
inst✝ : Monoid M
x : M
h✝ : ¬IsUnit x
this : (p : Prop) → Decidable p
H : ∀ (x_1 : M), ¬IsUnit x_1 → ∀ (x_2 : M), ¬IsUnit x_2 → ¬x_1 * x_2 = x
a b : M
h : x = a * b
o : ¬IsUnit a ∧ ¬IsUnit b
⊢ False

Proof state:
M : Type u_2
inst✝ : Monoid M
x : M
h : ¬IsUnit x
this : (p : Prop) → Decidable p
⊢ Irreducible x ∨ ∃ a b, ¬IsUnit a ∧ ¬IsUnit b ∧ a * b = x

Tactic:
refine or_iff_not_imp_right.2 fun H => ?_

Result:
M : Type u_2
inst✝ : Monoid M
x : M
h : ¬IsUnit x
this : (p : Prop) → Decidable p
H : ¬∃ a b, ¬IsUnit a ∧ ¬IsUnit b ∧ a * b = x
⊢ Irreducible x

Proof state:
M : Type u_2
inst✝ : Monoid M
x : M
h✝ : ¬IsUnit x
this : (p : Prop) → Decidable p
H : ∀ (x_1 : M), ¬IsUnit x_1 → ∀ (x_2 : M), ¬IsUnit x_2 → ¬x_1 * x_2 = x
a b : M
h : x = a * b
o : ¬(IsUnit a ∨ IsUnit b)
⊢ False

Tactic:
simp? [not_or] at o says simp only [not_or] at o

Result:
M : Type u_2
inst✝ : Monoid M
x : M
h✝ : ¬IsUnit x
this : (p : Prop) → Decidable p
H : ∀ (x_1 : M), ¬IsUnit x_1 → ∀ (x_2 : M), ¬IsUnit x_2 → ¬x_1 * x_2 = x
a b : M
h : x = a * b
o : ¬IsUnit a ∧ ¬IsUnit b
⊢ False

Proof state:
M : Type u_2
inst✝ : Monoid M
x : M
h : ¬IsUnit x
this : (p : Prop) → Decidable p
H : ∀ (x_1 : M), ¬IsUnit x_1 → ∀ (x_2 : M), ¬IsUnit x_2 → ¬x_1 * x_2 = x
⊢ ∀ (a b : M), x = a * b → IsUnit a ∨ IsUnit b

Tactic:
refine fun a b h => by_contradiction fun o => ?_

Result:
M : Type u_2
inst✝ : Monoid M
x : M
h✝ : ¬IsUnit x
this : (p : Prop) → Decidable p
H : ∀ (x_1 : M), ¬IsUnit x_1 → ∀ (x_2 : M), ¬IsUnit x_2 → ¬x_1 * x_2 = x
a b : M
h : x = a * b
o : ¬(IsUnit a ∨ IsUnit b)
⊢ False

Proof state:
M : Type u_2
inst✝ : Monoid M
x : M
h : ¬IsUnit x
this : (p : Prop) → Decidable p
H : ¬∃ a b, ¬IsUnit a ∧ ¬IsUnit b ∧ a * b = x
⊢ Irreducible x

Tactic:
simp only [exists_and_left, not_exists, not_and, irreducible_iff, h, not_false_eq_true,
  true_and] at H ⊢

Result:
M : Type u_2
inst✝ : Monoid M
x : M
h : ¬IsUnit x
this : (p : Prop) → Decidable p
H : ∀ (x_1 : M), ¬IsUnit x_1 → ∀ (x_2 : M), ¬IsUnit x_2 → ¬x_1 * x_2 = x
⊢ ∀ (a b : M), x = a * b → IsUnit a ∨ IsUnit b

Proof state:
M : Type u_2
inst✝ : Monoid M
x : M
h : ¬IsUnit x
this : (p : Prop) → Decidable p
H : ¬∃ a b, ¬IsUnit a ∧ ¬IsUnit b ∧ a * b = x
⊢ Irreducible x

Tactic:
simp? [h, irreducible_iff] at H ⊢ says
  simp only [exists_and_left, not_exists, not_and, irreducible_iff, h, not_false_eq_true,
    true_and] at H ⊢

Result:
M : Type u_2
inst✝ : Monoid M
x : M
h : ¬IsUnit x
this : (p : Prop) → Decidable p
H : ∀ (x_1 : M), ¬IsUnit x_1 → ∀ (x_2 : M), ¬IsUnit x_2 → ¬x_1 * x_2 = x
⊢ ∀ (a b : M), x = a * b → IsUnit a ∨ IsUnit b

Proof state:
M : Type u_2
inst✝ : Monoid M
x : M
h✝ : ¬IsUnit x
this : (p : Prop) → Decidable p
H : ∀ (x_1 : M), ¬IsUnit x_1 → ∀ (x_2 : M), ¬IsUnit x_2 → ¬x_1 * x_2 = x
a b : M
h : x = a * b
o : ¬IsUnit a ∧ ¬IsUnit b
⊢ False

Tactic:
exact H _ o.1 _ o.2 h.symm

Result:
no goals