α : Type u_1
β : Type ?u.320045
γ : Type ?u.320048
δ : Type ?u.320051
inst✝ : CommMonoidWithZero α
a : α
⊢ (¬IsUnit a ∧ ∀ (a_1 b : Associates α), Associates.mk a = a_1 * b → IsUnit a_1 ∨ IsUnit b) ↔
    ¬IsUnit a ∧ ∀ (a_1 b : α), a = a_1 * b → IsUnit a_1 ∨ IsUnit b
α : Type u_1
β : Type ?u.320045
γ : Type ?u.320048
δ : Type ?u.320051
inst✝ : CommMonoidWithZero α
a : α
⊢ Irreducible (Associates.mk a) ↔ Irreducible a
simp only [irreducible_iff, isUnit_mk]
α : Type u_1
β : Type ?u.320045
γ : Type ?u.320048
δ : Type ?u.320051
inst✝ : CommMonoidWithZero α
a : α
⊢ (∀ (a_1 b : Associates α), Associates.mk a = a_1 * b → IsUnit a_1 ∨ IsUnit b) ↔
    ∀ (a_1 b : α), a = a_1 * b → IsUnit a_1 ∨ IsUnit b
α : Type u_1
β : Type ?u.320045
γ : Type ?u.320048
δ : Type ?u.320051
inst✝ : CommMonoidWithZero α
a : α
⊢ (¬IsUnit a ∧ ∀ (a_1 b : Associates α), Associates.mk a = a_1 * b → IsUnit a_1 ∨ IsUnit b) ↔
    ¬IsUnit a ∧ ∀ (a_1 b : α), a = a_1 * b → IsUnit a_1 ∨ IsUnit b
apply and_congr Iff.rfl
case mp
α : Type u_1
β : Type ?u.320045
γ : Type ?u.320048
δ : Type ?u.320051
inst✝ : CommMonoidWithZero α
a : α
⊢ (∀ (a_1 b : Associates α), Associates.mk a = a_1 * b → IsUnit a_1 ∨ IsUnit b) →
    ∀ (a_2 b : α), a = a_2 * b → IsUnit a_2 ∨ IsUnit b

case mpr
α : Type u_1
β : Type ?u.320045
γ : Type ?u.320048
δ : Type ?u.320051
inst✝ : CommMonoidWithZero α
a : α
⊢ (∀ (a_1 b : α), a = a_1 * b → IsUnit a_1 ∨ IsUnit b) →
    ∀ (a_2 b : Associates α), Associates.mk a = a_2 * b → IsUnit a_2 ∨ IsUnit b
α : Type u_1
β : Type ?u.320045
γ : Type ?u.320048
δ : Type ?u.320051
inst✝ : CommMonoidWithZero α
a : α
⊢ (∀ (a_1 b : Associates α), Associates.mk a = a_1 * b → IsUnit a_1 ∨ IsUnit b) ↔
    ∀ (a_1 b : α), a = a_1 * b → IsUnit a_1 ∨ IsUnit b
constructor
case mp
α : Type u_1
β : Type ?u.320045
γ : Type ?u.320048
δ : Type ?u.320051
inst✝ : CommMonoidWithZero α
x y : α
h : ∀ (a b : Associates α), Associates.mk (x * y) = a * b → IsUnit a ∨ IsUnit b
⊢ IsUnit x ∨ IsUnit y
case mp
α : Type u_1
β : Type ?u.320045
γ : Type ?u.320048
δ : Type ?u.320051
inst✝ : CommMonoidWithZero α
a : α
⊢ (∀ (a_1 b : Associates α), Associates.mk a = a_1 * b → IsUnit a_1 ∨ IsUnit b) →
    ∀ (a_2 b : α), a = a_2 * b → IsUnit a_2 ∨ IsUnit b
rintro h x y rfl
no goals
case mp
α : Type u_1
β : Type ?u.320045
γ : Type ?u.320048
δ : Type ?u.320051
inst✝ : CommMonoidWithZero α
x y : α
h : ∀ (a b : Associates α), Associates.mk (x * y) = a * b → IsUnit a ∨ IsUnit b
⊢ IsUnit x ∨ IsUnit y
simpa [isUnit_mk] using h (Associates.mk x) (Associates.mk y) rfl
case mpr
α : Type u_1
β : Type ?u.320045
γ : Type ?u.320048
δ : Type ?u.320051
inst✝ : CommMonoidWithZero α
a : α
h : ∀ (a_1 b : α), a = a_1 * b → IsUnit a_1 ∨ IsUnit b
x y : Associates α
⊢ Associates.mk a = x * y → IsUnit x ∨ IsUnit y
case mpr
α : Type u_1
β : Type ?u.320045
γ : Type ?u.320048
δ : Type ?u.320051
inst✝ : CommMonoidWithZero α
a : α
⊢ (∀ (a_1 b : α), a = a_1 * b → IsUnit a_1 ∨ IsUnit b) →
    ∀ (a_2 b : Associates α), Associates.mk a = a_2 * b → IsUnit a_2 ∨ IsUnit b
intro h x y
case mpr
α : Type u_1
β : Type ?u.320045
γ : Type ?u.320048
δ : Type ?u.320051
inst✝ : CommMonoidWithZero α
a : α
h : ∀ (a_1 b : α), a = a_1 * b → IsUnit a_1 ∨ IsUnit b
x✝ y✝ : Associates α
x y : α
a_eq : Associates.mk a = Quotient.mk (Associated.setoid α) x * Quotient.mk (Associated.setoid α) y
⊢ IsUnit (Quotient.mk (Associated.setoid α) x) ∨ IsUnit (Quotient.mk (Associated.setoid α) y)
case mpr
α : Type u_1
β : Type ?u.320045
γ : Type ?u.320048
δ : Type ?u.320051
inst✝ : CommMonoidWithZero α
a : α
h : ∀ (a_1 b : α), a = a_1 * b → IsUnit a_1 ∨ IsUnit b
x y : Associates α
⊢ Associates.mk a = x * y → IsUnit x ∨ IsUnit y
refine' Quotient.inductionOn₂ x y fun x y a_eq => _
case mpr.intro
α : Type u_1
β : Type ?u.320045
γ : Type ?u.320048
δ : Type ?u.320051
inst✝ : CommMonoidWithZero α
a : α
h : ∀ (a_1 b : α), a = a_1 * b → IsUnit a_1 ∨ IsUnit b
x✝ y✝ : Associates α
x y : α
a_eq✝ : Associates.mk a = Quotient.mk (Associated.setoid α) x * Quotient.mk (Associated.setoid α) y
u : αˣ
a_eq : x * y * ↑u = a
⊢ IsUnit (Quotient.mk (Associated.setoid α) x) ∨ IsUnit (Quotient.mk (Associated.setoid α) y)
case mpr
α : Type u_1
β : Type ?u.320045
γ : Type ?u.320048
δ : Type ?u.320051
inst✝ : CommMonoidWithZero α
a : α
h : ∀ (a_1 b : α), a = a_1 * b → IsUnit a_1 ∨ IsUnit b
x✝ y✝ : Associates α
x y : α
a_eq : Associates.mk a = Quotient.mk (Associated.setoid α) x * Quotient.mk (Associated.setoid α) y
⊢ IsUnit (Quotient.mk (Associated.setoid α) x) ∨ IsUnit (Quotient.mk (Associated.setoid α) y)
rcases Quotient.exact a_eq.symm with ⟨u, a_eq⟩
case mpr.intro
α : Type u_1
β : Type ?u.320045
γ : Type ?u.320048
δ : Type ?u.320051
inst✝ : CommMonoidWithZero α
a : α
h : ∀ (a_1 b : α), a = a_1 * b → IsUnit a_1 ∨ IsUnit b
x✝ y✝ : Associates α
x y : α
a_eq✝ : Associates.mk a = Quotient.mk (Associated.setoid α) x * Quotient.mk (Associated.setoid α) y
u : αˣ
a_eq : x * (y * ↑u) = a
⊢ IsUnit (Quotient.mk (Associated.setoid α) x) ∨ IsUnit (Quotient.mk (Associated.setoid α) y)
case mpr.intro
α : Type u_1
β : Type ?u.320045
γ : Type ?u.320048
δ : Type ?u.320051
inst✝ : CommMonoidWithZero α
a : α
h : ∀ (a_1 b : α), a = a_1 * b → IsUnit a_1 ∨ IsUnit b
x✝ y✝ : Associates α
x y : α
a_eq✝ : Associates.mk a = Quotient.mk (Associated.setoid α) x * Quotient.mk (Associated.setoid α) y
u : αˣ
a_eq : x * y * ↑u = a
⊢ IsUnit (Quotient.mk (Associated.setoid α) x) ∨ IsUnit (Quotient.mk (Associated.setoid α) y)
rw [mul_assoc] at a_eq
case mpr.intro
α : Type u_1
β : Type ?u.320045
γ : Type ?u.320048
δ : Type ?u.320051
inst✝ : CommMonoidWithZero α
a : α
h : ∀ (a_1 b : α), a = a_1 * b → IsUnit a_1 ∨ IsUnit b
x✝ y✝ : Associates α
x y : α
a_eq✝ : Associates.mk a = Quotient.mk (Associated.setoid α) x * Quotient.mk (Associated.setoid α) y
u : αˣ
a_eq : x * (y * ↑u) = a
⊢ IsUnit (Associates.mk x) ∨ IsUnit (Associates.mk y)
case mpr.intro
α : Type u_1
β : Type ?u.320045
γ : Type ?u.320048
δ : Type ?u.320051
inst✝ : CommMonoidWithZero α
a : α
h : ∀ (a_1 b : α), a = a_1 * b → IsUnit a_1 ∨ IsUnit b
x✝ y✝ : Associates α
x y : α
a_eq✝ : Associates.mk a = Quotient.mk (Associated.setoid α) x * Quotient.mk (Associated.setoid α) y
u : αˣ
a_eq : x * (y * ↑u) = a
⊢ IsUnit (Quotient.mk (Associated.setoid α) x) ∨ IsUnit (Quotient.mk (Associated.setoid α) y)
show IsUnit (Associates.mk x) ∨ IsUnit (Associates.mk y)
no goals
case mpr.intro
α : Type u_1
β : Type ?u.320045
γ : Type ?u.320048
δ : Type ?u.320051
inst✝ : CommMonoidWithZero α
a : α
h : ∀ (a_1 b : α), a = a_1 * b → IsUnit a_1 ∨ IsUnit b
x✝ y✝ : Associates α
x y : α
a_eq✝ : Associates.mk a = Quotient.mk (Associated.setoid α) x * Quotient.mk (Associated.setoid α) y
u : αˣ
a_eq : x * (y * ↑u) = a
⊢ IsUnit (Associates.mk x) ∨ IsUnit (Associates.mk y)
simpa [isUnit_mk] using h _ _ a_eq.symm