case intro
α : Type u_1
β : Type ?u.199123
γ : Type ?u.199126
δ : Type ?u.199129
inst✝ : CancelMonoidWithZero α
a c : α
hba : a * c ∣ a
⊢ a ~ᵤ a * c
α : Type u_1
β : Type ?u.199123
γ : Type ?u.199126
δ : Type ?u.199129
inst✝ : CancelMonoidWithZero α
a b : α
hab : a ∣ b
hba : b ∣ a
⊢ a ~ᵤ b
rcases hab with ⟨c, rfl⟩
case intro.intro
α : Type u_1
β : Type ?u.199123
γ : Type ?u.199126
δ : Type ?u.199129
inst✝ : CancelMonoidWithZero α
a c d : α
a_eq : a = a * c * d
⊢ a ~ᵤ a * c
case intro
α : Type u_1
β : Type ?u.199123
γ : Type ?u.199126
δ : Type ?u.199129
inst✝ : CancelMonoidWithZero α
a c : α
hba : a * c ∣ a
⊢ a ~ᵤ a * c
rcases hba with ⟨d, a_eq⟩
case pos
α : Type u_1
β : Type ?u.199123
γ : Type ?u.199126
δ : Type ?u.199129
inst✝ : CancelMonoidWithZero α
a c d : α
a_eq : a = a * c * d
ha0 : a = 0
⊢ a ~ᵤ a * c

case neg
α : Type u_1
β : Type ?u.199123
γ : Type ?u.199126
δ : Type ?u.199129
inst✝ : CancelMonoidWithZero α
a c d : α
a_eq : a = a * c * d
ha0 : ¬a = 0
⊢ a ~ᵤ a * c
case intro.intro
α : Type u_1
β : Type ?u.199123
γ : Type ?u.199126
δ : Type ?u.199129
inst✝ : CancelMonoidWithZero α
a c d : α
a_eq : a = a * c * d
⊢ a ~ᵤ a * c
by_cases ha0 : a = 0
case neg
α : Type u_1
β : Type ?u.199123
γ : Type ?u.199126
δ : Type ?u.199129
inst✝ : CancelMonoidWithZero α
a c d : α
a_eq : a = a * c * d
ha0 : ¬a = 0
hac0 : a * c ≠ 0
⊢ a ~ᵤ a * c
case neg
α : Type u_1
β : Type ?u.199123
γ : Type ?u.199126
δ : Type ?u.199129
inst✝ : CancelMonoidWithZero α
a c d : α
a_eq : a = a * c * d
ha0 : ¬a = 0
⊢ a ~ᵤ a * c
have hac0 : a * c ≠ 0 := by
  intro con
  rw [con, zero_mul] at a_eq
  apply ha0 a_eq
case neg
α : Type u_1
β : Type ?u.199123
γ : Type ?u.199126
δ : Type ?u.199129
inst✝ : CancelMonoidWithZero α
a c d : α
a_eq : a = a * c * d
ha0 : ¬a = 0
hac0 : a * c ≠ 0
this : a * (c * d) = a * 1
⊢ a ~ᵤ a * c
case neg
α : Type u_1
β : Type ?u.199123
γ : Type ?u.199126
δ : Type ?u.199129
inst✝ : CancelMonoidWithZero α
a c d : α
a_eq : a = a * c * d
ha0 : ¬a = 0
hac0 : a * c ≠ 0
⊢ a ~ᵤ a * c
have : a * (c * d) = a * 1 := by rw [← mul_assoc, ← a_eq, mul_one]
case neg
α : Type u_1
β : Type ?u.199123
γ : Type ?u.199126
δ : Type ?u.199129
inst✝ : CancelMonoidWithZero α
a c d : α
a_eq : a = a * c * d
ha0 : ¬a = 0
hac0 : a * c ≠ 0
this : a * (c * d) = a * 1
hcd : c * d = 1
⊢ a ~ᵤ a * c
case neg
α : Type u_1
β : Type ?u.199123
γ : Type ?u.199126
δ : Type ?u.199129
inst✝ : CancelMonoidWithZero α
a c d : α
a_eq : a = a * c * d
ha0 : ¬a = 0
hac0 : a * c ≠ 0
this : a * (c * d) = a * 1
⊢ a ~ᵤ a * c
have hcd : c * d = 1 := mul_left_cancel₀ ha0 this
case neg
α : Type u_1
β : Type ?u.199123
γ : Type ?u.199126
δ : Type ?u.199129
inst✝ : CancelMonoidWithZero α
a c d : α
a_eq : a = a * c * d
ha0 : ¬a = 0
hac0 : a * c ≠ 0
this✝ : a * (c * d) = a * 1
hcd : c * d = 1
this : a * c * (d * c) = a * c * 1
⊢ a ~ᵤ a * c
case neg
α : Type u_1
β : Type ?u.199123
γ : Type ?u.199126
δ : Type ?u.199129
inst✝ : CancelMonoidWithZero α
a c d : α
a_eq : a = a * c * d
ha0 : ¬a = 0
hac0 : a * c ≠ 0
this : a * (c * d) = a * 1
hcd : c * d = 1
⊢ a ~ᵤ a * c
have : a * c * (d * c) = a * c * 1 := by rw [← mul_assoc, ← a_eq, mul_one]
case neg
α : Type u_1
β : Type ?u.199123
γ : Type ?u.199126
δ : Type ?u.199129
inst✝ : CancelMonoidWithZero α
a c d : α
a_eq : a = a * c * d
ha0 : ¬a = 0
hac0 : a * c ≠ 0
this✝ : a * (c * d) = a * 1
hcd : c * d = 1
this : a * c * (d * c) = a * c * 1
hdc : d * c = 1
⊢ a ~ᵤ a * c
case neg
α : Type u_1
β : Type ?u.199123
γ : Type ?u.199126
δ : Type ?u.199129
inst✝ : CancelMonoidWithZero α
a c d : α
a_eq : a = a * c * d
ha0 : ¬a = 0
hac0 : a * c ≠ 0
this✝ : a * (c * d) = a * 1
hcd : c * d = 1
this : a * c * (d * c) = a * c * 1
⊢ a ~ᵤ a * c
have hdc : d * c = 1 := mul_left_cancel₀ hac0 this
no goals
case neg
α : Type u_1
β : Type ?u.199123
γ : Type ?u.199126
δ : Type ?u.199129
inst✝ : CancelMonoidWithZero α
a c d : α
a_eq : a = a * c * d
ha0 : ¬a = 0
hac0 : a * c ≠ 0
this✝ : a * (c * d) = a * 1
hcd : c * d = 1
this : a * c * (d * c) = a * c * 1
hdc : d * c = 1
⊢ a ~ᵤ a * c
exact ⟨⟨c, d, hcd, hdc⟩, rfl⟩
case pos
α : Type u_1
β : Type ?u.199123
γ : Type ?u.199126
δ : Type ?u.199129
inst✝ : CancelMonoidWithZero α
a c d : α
ha0 : a = 0
⊢ 0 ~ᵤ 0
case pos
α : Type u_1
β : Type ?u.199123
γ : Type ?u.199126
δ : Type ?u.199129
inst✝ : CancelMonoidWithZero α
a c d : α
a_eq : a = a * c * d
ha0 : a = 0
⊢ a ~ᵤ a * c
simp_all
no goals
case pos
α : Type u_1
β : Type ?u.199123
γ : Type ?u.199126
δ : Type ?u.199129
inst✝ : CancelMonoidWithZero α
a c d : α
ha0 : a = 0
⊢ 0 ~ᵤ 0
rfl
α : Type u_1
β : Type ?u.199123
γ : Type ?u.199126
δ : Type ?u.199129
inst✝ : CancelMonoidWithZero α
a c d : α
a_eq : a = a * c * d
ha0 : ¬a = 0
con : a * c = 0
⊢ False
α : Type u_1
β : Type ?u.199123
γ : Type ?u.199126
δ : Type ?u.199129
inst✝ : CancelMonoidWithZero α
a c d : α
a_eq : a = a * c * d
ha0 : ¬a = 0
⊢ a * c ≠ 0
intro con
α : Type u_1
β : Type ?u.199123
γ : Type ?u.199126
δ : Type ?u.199129
inst✝ : CancelMonoidWithZero α
a c d : α
a_eq : a = 0
ha0 : ¬a = 0
con : a * c = 0
⊢ False
α : Type u_1
β : Type ?u.199123
γ : Type ?u.199126
δ : Type ?u.199129
inst✝ : CancelMonoidWithZero α
a c d : α
a_eq : a = a * c * d
ha0 : ¬a = 0
con : a * c = 0
⊢ False
rw [con, zero_mul] at a_eq
no goals
α : Type u_1
β : Type ?u.199123
γ : Type ?u.199126
δ : Type ?u.199129
inst✝ : CancelMonoidWithZero α
a c d : α
a_eq : a = 0
ha0 : ¬a = 0
con : a * c = 0
⊢ False
apply ha0 a_eq
no goals
α : Type u_1
β : Type ?u.199123
γ : Type ?u.199126
δ : Type ?u.199129
inst✝ : CancelMonoidWithZero α
a c d : α
a_eq : a = a * c * d
ha0 : ¬a = 0
hac0 : a * c ≠ 0
⊢ a * (c * d) = a * 1
rw [← mul_assoc, ← a_eq, mul_one]
no goals
α : Type u_1
β : Type ?u.199123
γ : Type ?u.199126
δ : Type ?u.199129
inst✝ : CancelMonoidWithZero α
a c d : α
a_eq : a = a * c * d
ha0 : ¬a = 0
hac0 : a * c ≠ 0
this : a * (c * d) = a * 1
hcd : c * d = 1
⊢ a * c * (d * c) = a * c * 1
rw [← mul_assoc, ← a_eq, mul_one]