no goals
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
exi1 : ∃ x, m = n * x
exi2 : ∃ y, k = l * y
hn : n = 0
⊢ m / n * (k / l) = m * k / (n * l)
simp [hn]
no goals
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
exi1 : ∃ x, m = n * x
exi2 : ∃ y, k = l * y
hn : ¬n = 0
this : 0 < n
hl : l = 0
⊢ m / n * (k / l) = m * k / (n * l)
simp [hl]
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
exi1 : ∃ x, m = n * x
exi2 : ∃ y, k = l * y
hn : ¬n = 0
this✝ : 0 < n
hl : ¬l = 0
this : 0 < l
⊢ m / n * (k / l) = m * k / (n * l)
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
exi1 : ∃ x, m = n * x
exi2 : ∃ y, k = l * y
hn : ¬n = 0
this : 0 < n
hl : ¬l = 0
⊢ m / n * (k / l) = m * k / (n * l)
have : 0 < l := Nat.pos_of_ne_zero hl
case intro
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
exi2 : ∃ y, k = l * y
hn : ¬n = 0
this✝ : 0 < n
hl : ¬l = 0
this : 0 < l
x : ℕ
hx : m = n * x
⊢ m / n * (k / l) = m * k / (n * l)
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
exi1 : ∃ x, m = n * x
exi2 : ∃ y, k = l * y
hn : ¬n = 0
this✝ : 0 < n
hl : ¬l = 0
this : 0 < l
⊢ m / n * (k / l) = m * k / (n * l)
cases' exi1 with x hx
case intro.intro
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
hn : ¬n = 0
this✝ : 0 < n
hl : ¬l = 0
this : 0 < l
x : ℕ
hx : m = n * x
y : ℕ
hy : k = l * y
⊢ m / n * (k / l) = m * k / (n * l)
case intro
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
exi2 : ∃ y, k = l * y
hn : ¬n = 0
this✝ : 0 < n
hl : ¬l = 0
this : 0 < l
x : ℕ
hx : m = n * x
⊢ m / n * (k / l) = m * k / (n * l)
cases' exi2 with y hy
case intro.intro
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
hn : ¬n = 0
this✝ : 0 < n
hl : ¬l = 0
this : 0 < l
x : ℕ
hx : m = n * x
y : ℕ
hy : k = l * y
⊢ x * y = n * x * (l * y) / (n * l)

case intro.intro.H
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
hn : ¬n = 0
this✝ : 0 < n
hl : ¬l = 0
this : 0 < l
x : ℕ
hx : m = n * x
y : ℕ
hy : k = l * y
⊢ 0 < l

case intro.intro.H
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
hn : ¬n = 0
this✝ : 0 < n
hl : ¬l = 0
this : 0 < l
x : ℕ
hx : m = n * x
y : ℕ
hy : k = l * y
⊢ 0 < n
case intro.intro
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
hn : ¬n = 0
this✝ : 0 < n
hl : ¬l = 0
this : 0 < l
x : ℕ
hx : m = n * x
y : ℕ
hy : k = l * y
⊢ m / n * (k / l) = m * k / (n * l)
rw [hx, hy, Nat.mul_div_cancel_left, Nat.mul_div_cancel_left]
case intro.intro.h
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
hn : ¬n = 0
this✝ : 0 < n
hl : ¬l = 0
this : 0 < l
x : ℕ
hx : m = n * x
y : ℕ
hy : k = l * y
⊢ n * x * (l * y) / (n * l) = x * y

case intro.intro.H
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
hn : ¬n = 0
this✝ : 0 < n
hl : ¬l = 0
this : 0 < l
x : ℕ
hx : m = n * x
y : ℕ
hy : k = l * y
⊢ 0 < l

case intro.intro.H
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
hn : ¬n = 0
this✝ : 0 < n
hl : ¬l = 0
this : 0 < l
x : ℕ
hx : m = n * x
y : ℕ
hy : k = l * y
⊢ 0 < n
case intro.intro
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
hn : ¬n = 0
this✝ : 0 < n
hl : ¬l = 0
this : 0 < l
x : ℕ
hx : m = n * x
y : ℕ
hy : k = l * y
⊢ x * y = n * x * (l * y) / (n * l)

case intro.intro.H
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
hn : ¬n = 0
this✝ : 0 < n
hl : ¬l = 0
this : 0 < l
x : ℕ
hx : m = n * x
y : ℕ
hy : k = l * y
⊢ 0 < l

case intro.intro.H
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
hn : ¬n = 0
this✝ : 0 < n
hl : ¬l = 0
this : 0 < l
x : ℕ
hx : m = n * x
y : ℕ
hy : k = l * y
⊢ 0 < n
apply Eq.symm
case intro.intro.h.H1
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
hn : ¬n = 0
this✝ : 0 < n
hl : ¬l = 0
this : 0 < l
x : ℕ
hx : m = n * x
y : ℕ
hy : k = l * y
⊢ 0 < n * l

case intro.intro.h.H2
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
hn : ¬n = 0
this✝ : 0 < n
hl : ¬l = 0
this : 0 < l
x : ℕ
hx : m = n * x
y : ℕ
hy : k = l * y
⊢ n * x * (l * y) = x * y * (n * l)

case intro.intro.H
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
hn : ¬n = 0
this✝ : 0 < n
hl : ¬l = 0
this : 0 < l
x : ℕ
hx : m = n * x
y : ℕ
hy : k = l * y
⊢ 0 < l

case intro.intro.H
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
hn : ¬n = 0
this✝ : 0 < n
hl : ¬l = 0
this : 0 < l
x : ℕ
hx : m = n * x
y : ℕ
hy : k = l * y
⊢ 0 < n
case intro.intro.h
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
hn : ¬n = 0
this✝ : 0 < n
hl : ¬l = 0
this : 0 < l
x : ℕ
hx : m = n * x
y : ℕ
hy : k = l * y
⊢ n * x * (l * y) / (n * l) = x * y

case intro.intro.H
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
hn : ¬n = 0
this✝ : 0 < n
hl : ¬l = 0
this : 0 < l
x : ℕ
hx : m = n * x
y : ℕ
hy : k = l * y
⊢ 0 < l

case intro.intro.H
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
hn : ¬n = 0
this✝ : 0 < n
hl : ¬l = 0
this : 0 < l
x : ℕ
hx : m = n * x
y : ℕ
hy : k = l * y
⊢ 0 < n
apply Nat.div_eq_of_eq_mul_left
case intro.intro.h.H1.ha
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
hn : ¬n = 0
this✝ : 0 < n
hl : ¬l = 0
this : 0 < l
x : ℕ
hx : m = n * x
y : ℕ
hy : k = l * y
⊢ 0 < n

case intro.intro.h.H1.hb
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
hn : ¬n = 0
this✝ : 0 < n
hl : ¬l = 0
this : 0 < l
x : ℕ
hx : m = n * x
y : ℕ
hy : k = l * y
⊢ 0 < l

case intro.intro.h.H2
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
hn : ¬n = 0
this✝ : 0 < n
hl : ¬l = 0
this : 0 < l
x : ℕ
hx : m = n * x
y : ℕ
hy : k = l * y
⊢ n * x * (l * y) = x * y * (n * l)

case intro.intro.H
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
hn : ¬n = 0
this✝ : 0 < n
hl : ¬l = 0
this : 0 < l
x : ℕ
hx : m = n * x
y : ℕ
hy : k = l * y
⊢ 0 < l

case intro.intro.H
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
hn : ¬n = 0
this✝ : 0 < n
hl : ¬l = 0
this : 0 < l
x : ℕ
hx : m = n * x
y : ℕ
hy : k = l * y
⊢ 0 < n
case intro.intro.h.H1
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
hn : ¬n = 0
this✝ : 0 < n
hl : ¬l = 0
this : 0 < l
x : ℕ
hx : m = n * x
y : ℕ
hy : k = l * y
⊢ 0 < n * l

case intro.intro.h.H2
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
hn : ¬n = 0
this✝ : 0 < n
hl : ¬l = 0
this : 0 < l
x : ℕ
hx : m = n * x
y : ℕ
hy : k = l * y
⊢ n * x * (l * y) = x * y * (n * l)

case intro.intro.H
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
hn : ¬n = 0
this✝ : 0 < n
hl : ¬l = 0
this : 0 < l
x : ℕ
hx : m = n * x
y : ℕ
hy : k = l * y
⊢ 0 < l

case intro.intro.H
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
hn : ¬n = 0
this✝ : 0 < n
hl : ¬l = 0
this : 0 < l
x : ℕ
hx : m = n * x
y : ℕ
hy : k = l * y
⊢ 0 < n
apply mul_pos
case intro.intro.h.H2
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
hn : ¬n = 0
this✝ : 0 < n
hl : ¬l = 0
this : 0 < l
x : ℕ
hx : m = n * x
y : ℕ
hy : k = l * y
⊢ n * x * (l * y) = x * y * (n * l)
case intro.intro.h.H1.ha
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
hn : ¬n = 0
this✝ : 0 < n
hl : ¬l = 0
this : 0 < l
x : ℕ
hx : m = n * x
y : ℕ
hy : k = l * y
⊢ 0 < n

case intro.intro.h.H1.hb
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
hn : ¬n = 0
this✝ : 0 < n
hl : ¬l = 0
this : 0 < l
x : ℕ
hx : m = n * x
y : ℕ
hy : k = l * y
⊢ 0 < l

case intro.intro.h.H2
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
hn : ¬n = 0
this✝ : 0 < n
hl : ¬l = 0
this : 0 < l
x : ℕ
hx : m = n * x
y : ℕ
hy : k = l * y
⊢ n * x * (l * y) = x * y * (n * l)

case intro.intro.H
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
hn : ¬n = 0
this✝ : 0 < n
hl : ¬l = 0
this : 0 < l
x : ℕ
hx : m = n * x
y : ℕ
hy : k = l * y
⊢ 0 < l

case intro.intro.H
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
hn : ¬n = 0
this✝ : 0 < n
hl : ¬l = 0
this : 0 < l
x : ℕ
hx : m = n * x
y : ℕ
hy : k = l * y
⊢ 0 < n
repeat' assumption
no goals
case intro.intro.h.H2
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
hn : ¬n = 0
this✝ : 0 < n
hl : ¬l = 0
this : 0 < l
x : ℕ
hx : m = n * x
y : ℕ
hy : k = l * y
⊢ n * x * (l * y) = x * y * (n * l)
simp only [mul_comm, mul_left_comm, mul_assoc]
no goals
case intro.intro.H
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
hn : ¬n = 0
this✝ : 0 < n
hl : ¬l = 0
this : 0 < l
x : ℕ
hx : m = n * x
y : ℕ
hy : k = l * y
⊢ 0 < n
assumption