case mp
a b m n✝ k n x y : ℕ
hn : n ≠ 0
hx : x ∣ n
hy : y ∣ n
⊢ n / x = n / y → x = y

case mpr
a b m n✝ k n x y : ℕ
hn : n ≠ 0
hx : x ∣ n
hy : y ∣ n
⊢ x = y → n / x = n / y
a b m n✝ k n x y : ℕ
hn : n ≠ 0
hx : x ∣ n
hy : y ∣ n
⊢ n / x = n / y ↔ x = y
constructor
case mp
a b m n✝ k n x y : ℕ
hn : n ≠ 0
hx : x ∣ n
hy : y ∣ n
h : n / x = n / y
⊢ x = y
case mp
a b m n✝ k n x y : ℕ
hn : n ≠ 0
hx : x ∣ n
hy : y ∣ n
⊢ n / x = n / y → x = y
intro h
case mp
a b m n✝ k n x y : ℕ
hn : n ≠ 0
hx : x ∣ n
hy : y ∣ n
h : n / x = n / y
⊢ n * x = n * y
case mp
a b m n✝ k n x y : ℕ
hn : n ≠ 0
hx : x ∣ n
hy : y ∣ n
h : n / x = n / y
⊢ x = y
rw [← mul_right_inj' hn]
case mp
a b m n✝ k n x y : ℕ
hn : n ≠ 0
hx : x ∣ n
hy : y ∣ n
h : n / x = n / y
⊢ n * x / y = n
case mp
a b m n✝ k n x y : ℕ
hn : n ≠ 0
hx : x ∣ n
hy : y ∣ n
h : n / x = n / y
⊢ n * x = n * y
apply Nat.eq_mul_of_div_eq_left (dvd_mul_of_dvd_left hy x)
case mp
a b m n✝ k n x y : ℕ
hn : n ≠ 0
hx : x ∣ n
hy : y ∣ n
h : n / x = n / y
⊢ n = x * (n / y)
case mp
a b m n✝ k n x y : ℕ
hn : n ≠ 0
hx : x ∣ n
hy : y ∣ n
h : n / x = n / y
⊢ n * x / y = n
rw [eq_comm, mul_comm, Nat.mul_div_assoc _ hy]
no goals
case mp
a b m n✝ k n x y : ℕ
hn : n ≠ 0
hx : x ∣ n
hy : y ∣ n
h : n / x = n / y
⊢ n = x * (n / y)
exact Nat.eq_mul_of_div_eq_right hx h
case mpr
a b m n✝ k n x y : ℕ
hn : n ≠ 0
hx : x ∣ n
hy : y ∣ n
h : x = y
⊢ n / x = n / y
case mpr
a b m n✝ k n x y : ℕ
hn : n ≠ 0
hx : x ∣ n
hy : y ∣ n
⊢ x = y → n / x = n / y
intro h
no goals
case mpr
a b m n✝ k n x y : ℕ
hn : n ≠ 0
hx : x ∣ n
hy : y ∣ n
h : x = y
⊢ n / x = n / y
rw [h]