no goals
m n k : Nat
H1 : k ∣ m
H2 : k ∣ n
H0 : k = 0
⊢ gcd (m / k) (n / k) = gcd m n / k
simp [H0]
m n k : Nat
H1 : k ∣ m
H2 : k ∣ n
H3 : k > 0
⊢ gcd (m / k) (n / k) * k = gcd m n / k * k
m n k : Nat
H1 : k ∣ m
H2 : k ∣ n
H3 : k > 0
⊢ gcd (m / k) (n / k) = gcd m n / k
apply Nat.eq_of_mul_eq_mul_right H3
no goals
m n k : Nat
H1 : k ∣ m
H2 : k ∣ n
H3 : k > 0
⊢ gcd (m / k) (n / k) * k = gcd m n / k * k
rw [Nat.div_mul_cancel (dvd_gcd H1 H2), ← gcd_mul_right,
    Nat.div_mul_cancel H1, Nat.div_mul_cancel H2]