R : Type u
inst✝ : EuclideanDomain R
a b : R
h : a % b = 0
⊢ b ∣ b * (a / b)
R : Type u
inst✝ : EuclideanDomain R
a b : R
h : a % b = 0
⊢ b ∣ a
rw [← div_add_mod a b, h, add_zero]
no goals
R : Type u
inst✝ : EuclideanDomain R
a b : R
h : a % b = 0
⊢ b ∣ b * (a / b)
exact dvd_mul_right _ _
R : Type u
inst✝ : EuclideanDomain R
a b : R
x✝ : b ∣ a
c : R
e : a = b * c
⊢ b * c = b * (b * c / b)
R : Type u
inst✝ : EuclideanDomain R
a b : R
x✝ : b ∣ a
c : R
e : a = b * c
⊢ a % b = 0
rw [e, ← add_left_cancel_iff, div_add_mod, add_zero]
R : Type u
inst✝ : EuclideanDomain R
a b : R
x✝ : b ∣ a
c : R
e : a = b * c
this : (p : Prop) → Decidable p
⊢ b * c = b * (b * c / b)
R : Type u
inst✝ : EuclideanDomain R
a b : R
x✝ : b ∣ a
c : R
e : a = b * c
⊢ b * c = b * (b * c / b)
haveI := Classical.dec
case pos
R : Type u
inst✝ : EuclideanDomain R
a b : R
x✝ : b ∣ a
c : R
e : a = b * c
this : (p : Prop) → Decidable p
b0 : b = 0
⊢ b * c = b * (b * c / b)

case neg
R : Type u
inst✝ : EuclideanDomain R
a b : R
x✝ : b ∣ a
c : R
e : a = b * c
this : (p : Prop) → Decidable p
b0 : ¬b = 0
⊢ b * c = b * (b * c / b)
R : Type u
inst✝ : EuclideanDomain R
a b : R
x✝ : b ∣ a
c : R
e : a = b * c
this : (p : Prop) → Decidable p
⊢ b * c = b * (b * c / b)
by_cases b0 : b = 0
no goals
case pos
R : Type u
inst✝ : EuclideanDomain R
a b : R
x✝ : b ∣ a
c : R
e : a = b * c
this : (p : Prop) → Decidable p
b0 : b = 0
⊢ b * c = b * (b * c / b)
simp only [b0, zero_mul]
no goals
case neg
R : Type u
inst✝ : EuclideanDomain R
a b : R
x✝ : b ∣ a
c : R
e : a = b * c
this : (p : Prop) → Decidable p
b0 : ¬b = 0
⊢ b * c = b * (b * c / b)
rw [mul_div_cancel_left _ b0]