-- Mathlib/Algebra/Prime/Lemmas.lean
theorem irreducible_mul_units (a : Mˣ) (b : M) : Irreducible (b * ↑a) ↔ Irreducible b

Proof state:
M : Type u_1
inst✝ : Monoid M
a : Mˣ
b : M
⊢ ¬IsUnit b →
    ((∀ (a_2 b_1 : M), b * ↑a = a_2 * b_1 → IsUnit a_2 ∨ IsUnit b_1) ↔
      ∀ (a b_1 : M), b = a * b_1 → IsUnit a ∨ IsUnit b_1)

Tactic:
refine fun _ => ⟨fun h A B HAB => ?_, fun h A B HAB => ?_⟩

Result:
case refine_1
M : Type u_1
inst✝ : Monoid M
a : Mˣ
b : M
x✝ : ¬IsUnit b
h : ∀ (a_1 b_1 : M), b * ↑a = a_1 * b_1 → IsUnit a_1 ∨ IsUnit b_1
A B : M
HAB : b = A * B
⊢ IsUnit A ∨ IsUnit B

case refine_2
M : Type u_1
inst✝ : Monoid M
a : Mˣ
b : M
x✝ : ¬IsUnit b
h : ∀ (a b_1 : M), b = a * b_1 → IsUnit a ∨ IsUnit b_1
A B : M
HAB : b * ↑a = A * B
⊢ IsUnit A ∨ IsUnit B

Proof state:
case refine_1.a
M : Type u_1
inst✝ : Monoid M
a : Mˣ
b : M
x✝ : ¬IsUnit b
h : ∀ (a_1 b_1 : M), b * ↑a = a_1 * b_1 → IsUnit a_1 ∨ IsUnit b_1
A B : M
HAB : b = A * B
⊢ b * ↑a = A * (B * ↑a)

Tactic:
rw [← mul_assoc, ← HAB]

Result:
no goals

Proof state:
case refine_1
M : Type u_1
inst✝ : Monoid M
a : Mˣ
b : M
x✝ : ¬IsUnit b
h : ∀ (a_1 b_1 : M), b * ↑a = a_1 * b_1 → IsUnit a_1 ∨ IsUnit b_1
A B : M
HAB : b = A * B
⊢ IsUnit A ∨ IsUnit (B * ↑a)

Tactic:
apply h

Result:
case refine_1.a
M : Type u_1
inst✝ : Monoid M
a : Mˣ
b : M
x✝ : ¬IsUnit b
h : ∀ (a_1 b_1 : M), b * ↑a = a_1 * b_1 → IsUnit a_1 ∨ IsUnit b_1
A B : M
HAB : b = A * B
⊢ b * ↑a = A * (B * ↑a)

Proof state:
case refine_1
M : Type u_1
inst✝ : Monoid M
a : Mˣ
b : M
x✝ : ¬IsUnit b
h : ∀ (a_1 b_1 : M), b * ↑a = a_1 * b_1 → IsUnit a_1 ∨ IsUnit b_1
A B : M
HAB : b = A * B
⊢ IsUnit A ∨ IsUnit B

Tactic:
rw [← Units.isUnit_mul_units B a]

Result:
case refine_1
M : Type u_1
inst✝ : Monoid M
a : Mˣ
b : M
x✝ : ¬IsUnit b
h : ∀ (a_1 b_1 : M), b * ↑a = a_1 * b_1 → IsUnit a_1 ∨ IsUnit b_1
A B : M
HAB : b = A * B
⊢ IsUnit A ∨ IsUnit (B * ↑a)

Proof state:
case refine_2.a
M : Type u_1
inst✝ : Monoid M
a : Mˣ
b : M
x✝ : ¬IsUnit b
h : ∀ (a b_1 : M), b = a * b_1 → IsUnit a ∨ IsUnit b_1
A B : M
HAB : b * ↑a = A * B
⊢ b = A * (B * ↑a⁻¹)

Tactic:
rw [← mul_assoc, ← HAB, Units.mul_inv_cancel_right]

Result:
no goals

Proof state:
case refine_2
M : Type u_1
inst✝ : Monoid M
a : Mˣ
b : M
x✝ : ¬IsUnit b
h : ∀ (a b_1 : M), b = a * b_1 → IsUnit a ∨ IsUnit b_1
A B : M
HAB : b * ↑a = A * B
⊢ IsUnit A ∨ IsUnit B

Tactic:
rw [← Units.isUnit_mul_units B a⁻¹]

Result:
case refine_2
M : Type u_1
inst✝ : Monoid M
a : Mˣ
b : M
x✝ : ¬IsUnit b
h : ∀ (a b_1 : M), b = a * b_1 → IsUnit a ∨ IsUnit b_1
A B : M
HAB : b * ↑a = A * B
⊢ IsUnit A ∨ IsUnit (B * ↑a⁻¹)

Proof state:
M : Type u_1
inst✝ : Monoid M
a : Mˣ
b : M
⊢ Irreducible (b * ↑a) ↔ Irreducible b

Tactic:
simp only [irreducible_iff, Units.isUnit_mul_units, and_congr_right_iff]

Result:
M : Type u_1
inst✝ : Monoid M
a : Mˣ
b : M
⊢ ¬IsUnit b →
    ((∀ (a_2 b_1 : M), b * ↑a = a_2 * b_1 → IsUnit a_2 ∨ IsUnit b_1) ↔
      ∀ (a b_1 : M), b = a * b_1 → IsUnit a ∨ IsUnit b_1)

Proof state:
case refine_2
M : Type u_1
inst✝ : Monoid M
a : Mˣ
b : M
x✝ : ¬IsUnit b
h : ∀ (a b_1 : M), b = a * b_1 → IsUnit a ∨ IsUnit b_1
A B : M
HAB : b * ↑a = A * B
⊢ IsUnit A ∨ IsUnit (B * ↑a⁻¹)

Tactic:
apply h

Result:
case refine_2.a
M : Type u_1
inst✝ : Monoid M
a : Mˣ
b : M
x✝ : ¬IsUnit b
h : ∀ (a b_1 : M), b = a * b_1 → IsUnit a ∨ IsUnit b_1
A B : M
HAB : b * ↑a = A * B
⊢ b = A * (B * ↑a⁻¹)