α : Type u_1
β : Type ?u.87841
γ : Type ?u.87844
δ : Type ?u.87847
inst✝ : Monoid α
a : αˣ
b : α
⊢ ¬IsUnit b →
    ((∀ (a_2 b_1 : α), ↑a * b = a_2 * b_1 → IsUnit a_2 ∨ IsUnit b_1) ↔
      ∀ (a b_1 : α), b = a * b_1 → IsUnit a ∨ IsUnit b_1)
α : Type u_1
β : Type ?u.87841
γ : Type ?u.87844
δ : Type ?u.87847
inst✝ : Monoid α
a : αˣ
b : α
⊢ Irreducible (↑a * b) ↔ Irreducible b
simp only [irreducible_iff, Units.isUnit_units_mul, and_congr_right_iff]
case refine'_1
α : Type u_1
β : Type ?u.87841
γ : Type ?u.87844
δ : Type ?u.87847
inst✝ : Monoid α
a : αˣ
b : α
x✝ : ¬IsUnit b
h : ∀ (a_1 b_1 : α), ↑a * b = a_1 * b_1 → IsUnit a_1 ∨ IsUnit b_1
A B : α
HAB : b = A * B
⊢ IsUnit A ∨ IsUnit B

case refine'_2
α : Type u_1
β : Type ?u.87841
γ : Type ?u.87844
δ : Type ?u.87847
inst✝ : Monoid α
a : αˣ
b : α
x✝ : ¬IsUnit b
h : ∀ (a b_1 : α), b = a * b_1 → IsUnit a ∨ IsUnit b_1
A B : α
HAB : ↑a * b = A * B
⊢ IsUnit A ∨ IsUnit B
α : Type u_1
β : Type ?u.87841
γ : Type ?u.87844
δ : Type ?u.87847
inst✝ : Monoid α
a : αˣ
b : α
⊢ ¬IsUnit b →
    ((∀ (a_2 b_1 : α), ↑a * b = a_2 * b_1 → IsUnit a_2 ∨ IsUnit b_1) ↔
      ∀ (a b_1 : α), b = a * b_1 → IsUnit a ∨ IsUnit b_1)
refine' fun _ => ⟨fun h A B HAB => _, fun h A B HAB => _⟩
case refine'_1
α : Type u_1
β : Type ?u.87841
γ : Type ?u.87844
δ : Type ?u.87847
inst✝ : Monoid α
a : αˣ
b : α
x✝ : ¬IsUnit b
h : ∀ (a_1 b_1 : α), ↑a * b = a_1 * b_1 → IsUnit a_1 ∨ IsUnit b_1
A B : α
HAB : b = A * B
⊢ IsUnit (↑a * A) ∨ IsUnit B
case refine'_1
α : Type u_1
β : Type ?u.87841
γ : Type ?u.87844
δ : Type ?u.87847
inst✝ : Monoid α
a : αˣ
b : α
x✝ : ¬IsUnit b
h : ∀ (a_1 b_1 : α), ↑a * b = a_1 * b_1 → IsUnit a_1 ∨ IsUnit b_1
A B : α
HAB : b = A * B
⊢ IsUnit A ∨ IsUnit B
rw [← a.isUnit_units_mul]
case refine'_1.a
α : Type u_1
β : Type ?u.87841
γ : Type ?u.87844
δ : Type ?u.87847
inst✝ : Monoid α
a : αˣ
b : α
x✝ : ¬IsUnit b
h : ∀ (a_1 b_1 : α), ↑a * b = a_1 * b_1 → IsUnit a_1 ∨ IsUnit b_1
A B : α
HAB : b = A * B
⊢ ↑a * b = ↑a * A * B
case refine'_1
α : Type u_1
β : Type ?u.87841
γ : Type ?u.87844
δ : Type ?u.87847
inst✝ : Monoid α
a : αˣ
b : α
x✝ : ¬IsUnit b
h : ∀ (a_1 b_1 : α), ↑a * b = a_1 * b_1 → IsUnit a_1 ∨ IsUnit b_1
A B : α
HAB : b = A * B
⊢ IsUnit (↑a * A) ∨ IsUnit B
apply h
no goals
case refine'_1.a
α : Type u_1
β : Type ?u.87841
γ : Type ?u.87844
δ : Type ?u.87847
inst✝ : Monoid α
a : αˣ
b : α
x✝ : ¬IsUnit b
h : ∀ (a_1 b_1 : α), ↑a * b = a_1 * b_1 → IsUnit a_1 ∨ IsUnit b_1
A B : α
HAB : b = A * B
⊢ ↑a * b = ↑a * A * B
rw [mul_assoc, ← HAB]
case refine'_2
α : Type u_1
β : Type ?u.87841
γ : Type ?u.87844
δ : Type ?u.87847
inst✝ : Monoid α
a : αˣ
b : α
x✝ : ¬IsUnit b
h : ∀ (a b_1 : α), b = a * b_1 → IsUnit a ∨ IsUnit b_1
A B : α
HAB : ↑a * b = A * B
⊢ IsUnit (↑a⁻¹ * A) ∨ IsUnit B
case refine'_2
α : Type u_1
β : Type ?u.87841
γ : Type ?u.87844
δ : Type ?u.87847
inst✝ : Monoid α
a : αˣ
b : α
x✝ : ¬IsUnit b
h : ∀ (a b_1 : α), b = a * b_1 → IsUnit a ∨ IsUnit b_1
A B : α
HAB : ↑a * b = A * B
⊢ IsUnit A ∨ IsUnit B
rw [← a⁻¹.isUnit_units_mul]
case refine'_2.a
α : Type u_1
β : Type ?u.87841
γ : Type ?u.87844
δ : Type ?u.87847
inst✝ : Monoid α
a : αˣ
b : α
x✝ : ¬IsUnit b
h : ∀ (a b_1 : α), b = a * b_1 → IsUnit a ∨ IsUnit b_1
A B : α
HAB : ↑a * b = A * B
⊢ b = ↑a⁻¹ * A * B
case refine'_2
α : Type u_1
β : Type ?u.87841
γ : Type ?u.87844
δ : Type ?u.87847
inst✝ : Monoid α
a : αˣ
b : α
x✝ : ¬IsUnit b
h : ∀ (a b_1 : α), b = a * b_1 → IsUnit a ∨ IsUnit b_1
A B : α
HAB : ↑a * b = A * B
⊢ IsUnit (↑a⁻¹ * A) ∨ IsUnit B
apply h
no goals
case refine'_2.a
α : Type u_1
β : Type ?u.87841
γ : Type ?u.87844
δ : Type ?u.87847
inst✝ : Monoid α
a : αˣ
b : α
x✝ : ¬IsUnit b
h : ∀ (a b_1 : α), b = a * b_1 → IsUnit a ∨ IsUnit b_1
A B : α
HAB : ↑a * b = A * B
⊢ b = ↑a⁻¹ * A * B
rw [mul_assoc, ← HAB, Units.inv_mul_cancel_left]