α : Type u_1
β : Type ?u.321829
γ : Type ?u.321832
δ : Type ?u.321835
inst✝ : CommMonoidWithZero α
a b : α
⊢ (a ≠ 0 ∧ ∃ x, ¬IsUnit x ∧ Associates.mk b = Associates.mk a * x) ↔ a ≠ 0 ∧ ∃ x, ¬IsUnit x ∧ b = a * x
α : Type u_1
β : Type ?u.321829
γ : Type ?u.321832
δ : Type ?u.321835
inst✝ : CommMonoidWithZero α
a b : α
⊢ DvdNotUnit (Associates.mk a) (Associates.mk b) ↔ DvdNotUnit a b
rw [DvdNotUnit, DvdNotUnit, mk_ne_zero]
case h
α : Type u_1
β : Type ?u.321829
γ : Type ?u.321832
δ : Type ?u.321835
inst✝ : CommMonoidWithZero α
a b : α
⊢ a ≠ 0 → ((∃ x, ¬IsUnit x ∧ Associates.mk b = Associates.mk a * x) ↔ ∃ x, ¬IsUnit x ∧ b = a * x)
α : Type u_1
β : Type ?u.321829
γ : Type ?u.321832
δ : Type ?u.321835
inst✝ : CommMonoidWithZero α
a b : α
⊢ (a ≠ 0 ∧ ∃ x, ¬IsUnit x ∧ Associates.mk b = Associates.mk a * x) ↔ a ≠ 0 ∧ ∃ x, ¬IsUnit x ∧ b = a * x
apply and_congr_right
case h
α : Type u_1
β : Type ?u.321829
γ : Type ?u.321832
δ : Type ?u.321835
inst✝ : CommMonoidWithZero α
a b : α
a✝ : a ≠ 0
⊢ (∃ x, ¬IsUnit x ∧ Associates.mk b = Associates.mk a * x) ↔ ∃ x, ¬IsUnit x ∧ b = a * x
case h
α : Type u_1
β : Type ?u.321829
γ : Type ?u.321832
δ : Type ?u.321835
inst✝ : CommMonoidWithZero α
a b : α
⊢ a ≠ 0 → ((∃ x, ¬IsUnit x ∧ Associates.mk b = Associates.mk a * x) ↔ ∃ x, ¬IsUnit x ∧ b = a * x)
intro
case h.mp
α : Type u_1
β : Type ?u.321829
γ : Type ?u.321832
δ : Type ?u.321835
inst✝ : CommMonoidWithZero α
a b : α
a✝ : a ≠ 0
⊢ (∃ x, ¬IsUnit x ∧ Associates.mk b = Associates.mk a * x) → ∃ x, ¬IsUnit x ∧ b = a * x

case h.mpr
α : Type u_1
β : Type ?u.321829
γ : Type ?u.321832
δ : Type ?u.321835
inst✝ : CommMonoidWithZero α
a b : α
a✝ : a ≠ 0
⊢ (∃ x, ¬IsUnit x ∧ b = a * x) → ∃ x, ¬IsUnit x ∧ Associates.mk b = Associates.mk a * x
case h
α : Type u_1
β : Type ?u.321829
γ : Type ?u.321832
δ : Type ?u.321835
inst✝ : CommMonoidWithZero α
a b : α
a✝ : a ≠ 0
⊢ (∃ x, ¬IsUnit x ∧ Associates.mk b = Associates.mk a * x) ↔ ∃ x, ¬IsUnit x ∧ b = a * x
constructor
case h.mp
α : Type u_1
β : Type ?u.321829
γ : Type ?u.321832
δ : Type ?u.321835
inst✝ : CommMonoidWithZero α
a b : α
a✝ : a ≠ 0
⊢ (∀ (x : α), ¬IsUnit x → b ≠ a * x) → ∀ (x : Associates α), ¬IsUnit x → Associates.mk b ≠ Associates.mk a * x
case h.mp
α : Type u_1
β : Type ?u.321829
γ : Type ?u.321832
δ : Type ?u.321835
inst✝ : CommMonoidWithZero α
a b : α
a✝ : a ≠ 0
⊢ (∃ x, ¬IsUnit x ∧ Associates.mk b = Associates.mk a * x) → ∃ x, ¬IsUnit x ∧ b = a * x
contrapose!
case h.mp
α : Type u_1
β : Type ?u.321829
γ : Type ?u.321832
δ : Type ?u.321835
inst✝ : CommMonoidWithZero α
a b : α
a✝ : a ≠ 0
⊢ (∀ (x : α), ¬IsUnit x → b ≠ a * x) →
    ∀ (a_2 : α), ¬IsUnit (Associates.mk a_2) → Associates.mk b ≠ Associates.mk a * Associates.mk a_2
case h.mp
α : Type u_1
β : Type ?u.321829
γ : Type ?u.321832
δ : Type ?u.321835
inst✝ : CommMonoidWithZero α
a b : α
a✝ : a ≠ 0
⊢ (∀ (x : α), ¬IsUnit x → b ≠ a * x) → ∀ (x : Associates α), ¬IsUnit x → Associates.mk b ≠ Associates.mk a * x
rw [forall_associated]
case h.mp
α : Type u_1
β : Type ?u.321829
γ : Type ?u.321832
δ : Type ?u.321835
inst✝ : CommMonoidWithZero α
a b : α
a✝ : a ≠ 0
h : ∀ (x : α), ¬IsUnit x → b ≠ a * x
x : α
hx : ¬IsUnit (Associates.mk x)
hbax : Associates.mk b = Associates.mk a * Associates.mk x
⊢ False
case h.mp
α : Type u_1
β : Type ?u.321829
γ : Type ?u.321832
δ : Type ?u.321835
inst✝ : CommMonoidWithZero α
a b : α
a✝ : a ≠ 0
⊢ (∀ (x : α), ¬IsUnit x → b ≠ a * x) →
    ∀ (a_2 : α), ¬IsUnit (Associates.mk a_2) → Associates.mk b ≠ Associates.mk a * Associates.mk a_2
intro h x hx hbax
case h.mp
α : Type u_1
β : Type ?u.321829
γ : Type ?u.321832
δ : Type ?u.321835
inst✝ : CommMonoidWithZero α
a b : α
a✝ : a ≠ 0
h : ∀ (x : α), ¬IsUnit x → b ≠ a * x
x : α
hx : ¬IsUnit (Associates.mk x)
hbax : b ~ᵤ a * x
⊢ False
case h.mp
α : Type u_1
β : Type ?u.321829
γ : Type ?u.321832
δ : Type ?u.321835
inst✝ : CommMonoidWithZero α
a b : α
a✝ : a ≠ 0
h : ∀ (x : α), ¬IsUnit x → b ≠ a * x
x : α
hx : ¬IsUnit (Associates.mk x)
hbax : Associates.mk b = Associates.mk a * Associates.mk x
⊢ False
rw [mk_mul_mk, mk_eq_mk_iff_associated] at hbax
case h.mp.intro
α : Type u_1
β : Type ?u.321829
γ : Type ?u.321832
δ : Type ?u.321835
inst✝ : CommMonoidWithZero α
a b : α
a✝ : a ≠ 0
h : ∀ (x : α), ¬IsUnit x → b ≠ a * x
x : α
hx : ¬IsUnit (Associates.mk x)
u : αˣ
hu : b * ↑u = a * x
⊢ False
case h.mp
α : Type u_1
β : Type ?u.321829
γ : Type ?u.321832
δ : Type ?u.321835
inst✝ : CommMonoidWithZero α
a b : α
a✝ : a ≠ 0
h : ∀ (x : α), ¬IsUnit x → b ≠ a * x
x : α
hx : ¬IsUnit (Associates.mk x)
hbax : b ~ᵤ a * x
⊢ False
cases' hbax with u hu
case h.mp.intro._
α : Type u_1
β : Type ?u.321829
γ : Type ?u.321832
δ : Type ?u.321835
inst✝ : CommMonoidWithZero α
a b : α
a✝ : a ≠ 0
h : ∀ (x : α), ¬IsUnit x → b ≠ a * x
x : α
hx : ¬IsUnit (Associates.mk x)
u : αˣ
hu : b * ↑u = a * x
⊢ ¬IsUnit (x * ↑u⁻¹)

case h.mp.intro.a
α : Type u_1
β : Type ?u.321829
γ : Type ?u.321832
δ : Type ?u.321835
inst✝ : CommMonoidWithZero α
a b : α
a✝ : a ≠ 0
h : ∀ (x : α), ¬IsUnit x → b ≠ a * x
x : α
hx : ¬IsUnit (Associates.mk x)
u : αˣ
hu : b * ↑u = a * x
⊢ b = a * (x * ↑u⁻¹)
case h.mp.intro
α : Type u_1
β : Type ?u.321829
γ : Type ?u.321832
δ : Type ?u.321835
inst✝ : CommMonoidWithZero α
a b : α
a✝ : a ≠ 0
h : ∀ (x : α), ¬IsUnit x → b ≠ a * x
x : α
hx : ¬IsUnit (Associates.mk x)
u : αˣ
hu : b * ↑u = a * x
⊢ False
apply h (x * ↑u⁻¹)
no goals
case h.mp.intro.a
α : Type u_1
β : Type ?u.321829
γ : Type ?u.321832
δ : Type ?u.321835
inst✝ : CommMonoidWithZero α
a b : α
a✝ : a ≠ 0
h : ∀ (x : α), ¬IsUnit x → b ≠ a * x
x : α
hx : ¬IsUnit (Associates.mk x)
u : αˣ
hu : b * ↑u = a * x
⊢ b = a * (x * ↑u⁻¹)
simp [← mul_assoc, ← hu]
case h.mp.intro._
α : Type u_1
β : Type ?u.321829
γ : Type ?u.321832
δ : Type ?u.321835
inst✝ : CommMonoidWithZero α
a b : α
a✝ : a ≠ 0
h : ∀ (x : α), ¬IsUnit x → b ≠ a * x
x : α
hx : ¬IsUnit x
u : αˣ
hu : b * ↑u = a * x
⊢ ¬IsUnit (x * ↑u⁻¹)
case h.mp.intro._
α : Type u_1
β : Type ?u.321829
γ : Type ?u.321832
δ : Type ?u.321835
inst✝ : CommMonoidWithZero α
a b : α
a✝ : a ≠ 0
h : ∀ (x : α), ¬IsUnit x → b ≠ a * x
x : α
hx : ¬IsUnit (Associates.mk x)
u : αˣ
hu : b * ↑u = a * x
⊢ ¬IsUnit (x * ↑u⁻¹)
rw [isUnit_mk] at hx
case h.mp.intro._
α : Type u_1
β : Type ?u.321829
γ : Type ?u.321832
δ : Type ?u.321835
inst✝ : CommMonoidWithZero α
a b : α
a✝ : a ≠ 0
h : ∀ (x : α), ¬IsUnit x → b ≠ a * x
x : α
hx : ¬IsUnit x
u : αˣ
hu : b * ↑u = a * x
⊢ ¬IsUnit ?m.324736

case h.mp.intro._
α : Type u_1
β : Type ?u.321829
γ : Type ?u.321832
δ : Type ?u.321835
inst✝ : CommMonoidWithZero α
a b : α
a✝ : a ≠ 0
h : ∀ (x : α), ¬IsUnit x → b ≠ a * x
x : α
hx : ¬IsUnit x
u : αˣ
hu : b * ↑u = a * x
⊢ x * ↑u⁻¹ ~ᵤ ?m.324736

α : Type u_1
β : Type ?u.321829
γ : Type ?u.321832
δ : Type ?u.321835
inst✝ : CommMonoidWithZero α
a b : α
a✝ : a ≠ 0
h : ∀ (x : α), ¬IsUnit x → b ≠ a * x
x : α
hx : ¬IsUnit x
u : αˣ
hu : b * ↑u = a * x
⊢ α
case h.mp.intro._
α : Type u_1
β : Type ?u.321829
γ : Type ?u.321832
δ : Type ?u.321835
inst✝ : CommMonoidWithZero α
a b : α
a✝ : a ≠ 0
h : ∀ (x : α), ¬IsUnit x → b ≠ a * x
x : α
hx : ¬IsUnit x
u : αˣ
hu : b * ↑u = a * x
⊢ ¬IsUnit (x * ↑u⁻¹)
rw [Associated.isUnit_iff]
case h.mp.intro._
α : Type u_1
β : Type ?u.321829
γ : Type ?u.321832
δ : Type ?u.321835
inst✝ : CommMonoidWithZero α
a b : α
a✝ : a ≠ 0
h : ∀ (x : α), ¬IsUnit x → b ≠ a * x
x : α
hx : ¬IsUnit x
u : αˣ
hu : b * ↑u = a * x
⊢ x * ↑u⁻¹ ~ᵤ x
case h.mp.intro._
α : Type u_1
β : Type ?u.321829
γ : Type ?u.321832
δ : Type ?u.321835
inst✝ : CommMonoidWithZero α
a b : α
a✝ : a ≠ 0
h : ∀ (x : α), ¬IsUnit x → b ≠ a * x
x : α
hx : ¬IsUnit x
u : αˣ
hu : b * ↑u = a * x
⊢ ¬IsUnit ?m.324736

case h.mp.intro._
α : Type u_1
β : Type ?u.321829
γ : Type ?u.321832
δ : Type ?u.321835
inst✝ : CommMonoidWithZero α
a b : α
a✝ : a ≠ 0
h : ∀ (x : α), ¬IsUnit x → b ≠ a * x
x : α
hx : ¬IsUnit x
u : αˣ
hu : b * ↑u = a * x
⊢ x * ↑u⁻¹ ~ᵤ ?m.324736

α : Type u_1
β : Type ?u.321829
γ : Type ?u.321832
δ : Type ?u.321835
inst✝ : CommMonoidWithZero α
a b : α
a✝ : a ≠ 0
h : ∀ (x : α), ¬IsUnit x → b ≠ a * x
x : α
hx : ¬IsUnit x
u : αˣ
hu : b * ↑u = a * x
⊢ α
apply hx
case h.mp.intro._
α : Type u_1
β : Type ?u.321829
γ : Type ?u.321832
δ : Type ?u.321835
inst✝ : CommMonoidWithZero α
a b : α
a✝ : a ≠ 0
h : ∀ (x : α), ¬IsUnit x → b ≠ a * x
x : α
hx : ¬IsUnit x
u : αˣ
hu : b * ↑u = a * x
⊢ x * ↑u⁻¹ * ↑u = x
case h.mp.intro._
α : Type u_1
β : Type ?u.321829
γ : Type ?u.321832
δ : Type ?u.321835
inst✝ : CommMonoidWithZero α
a b : α
a✝ : a ≠ 0
h : ∀ (x : α), ¬IsUnit x → b ≠ a * x
x : α
hx : ¬IsUnit x
u : αˣ
hu : b * ↑u = a * x
⊢ x * ↑u⁻¹ ~ᵤ x
use u
no goals
case h.mp.intro._
α : Type u_1
β : Type ?u.321829
γ : Type ?u.321832
δ : Type ?u.321835
inst✝ : CommMonoidWithZero α
a b : α
a✝ : a ≠ 0
h : ∀ (x : α), ¬IsUnit x → b ≠ a * x
x : α
hx : ¬IsUnit x
u : αˣ
hu : b * ↑u = a * x
⊢ x * ↑u⁻¹ * ↑u = x
simp
case h.mpr.intro.intro
α : Type u_1
β : Type ?u.321829
γ : Type ?u.321832
δ : Type ?u.321835
inst✝ : CommMonoidWithZero α
a : α
a✝ : a ≠ 0
x : α
hx : ¬IsUnit x
⊢ ∃ x_1, ¬IsUnit x_1 ∧ Associates.mk (a * x) = Associates.mk a * x_1
case h.mpr
α : Type u_1
β : Type ?u.321829
γ : Type ?u.321832
δ : Type ?u.321835
inst✝ : CommMonoidWithZero α
a b : α
a✝ : a ≠ 0
⊢ (∃ x, ¬IsUnit x ∧ b = a * x) → ∃ x, ¬IsUnit x ∧ Associates.mk b = Associates.mk a * x
rintro ⟨x, ⟨hx, rfl⟩⟩
case h.mpr.intro.intro
α : Type u_1
β : Type ?u.321829
γ : Type ?u.321832
δ : Type ?u.321835
inst✝ : CommMonoidWithZero α
a : α
a✝ : a ≠ 0
x : α
hx : ¬IsUnit x
⊢ ¬IsUnit (Associates.mk x) ∧ Associates.mk (a * x) = Associates.mk a * Associates.mk x
case h.mpr.intro.intro
α : Type u_1
β : Type ?u.321829
γ : Type ?u.321832
δ : Type ?u.321835
inst✝ : CommMonoidWithZero α
a : α
a✝ : a ≠ 0
x : α
hx : ¬IsUnit x
⊢ ∃ x_1, ¬IsUnit x_1 ∧ Associates.mk (a * x) = Associates.mk a * x_1
use Associates.mk x
no goals
case h.mpr.intro.intro
α : Type u_1
β : Type ?u.321829
γ : Type ?u.321832
δ : Type ?u.321835
inst✝ : CommMonoidWithZero α
a : α
a✝ : a ≠ 0
x : α
hx : ¬IsUnit x
⊢ ¬IsUnit (Associates.mk x) ∧ Associates.mk (a * x) = Associates.mk a * Associates.mk x
simp [isUnit_mk, mk_mul_mk, hx]