Theorem: two_pow_three_pow_unique_factorization' (meetings/ex4.lean)

State before:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
⊢ 2 ^ m * 3 ^ n = 2 ^ p * 3 ^ q → m = p ∧ n = q
Tactic:
intro hfac
State after:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : 2 ^ m * 3 ^ n = 2 ^ p * 3 ^ q
⊢ m = p ∧ n = q

State before:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : 2 ^ m * 3 ^ n = 2 ^ p * 3 ^ q
⊢ m = p ∧ n = q
Tactic:
have hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n := by
  exact dvd_mul_of_dvd_right (pow_dvd_pow 3 h₂) (2 ^ m)
State after:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : 2 ^ m * 3 ^ n = 2 ^ p * 3 ^ q
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
⊢ m = p ∧ n = q

State before:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : 2 ^ m * 3 ^ n = 2 ^ p * 3 ^ q
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
⊢ m = p ∧ n = q
Tactic:
rw [←Nat.div_eq_iff_eq_mul_left (by simp) hdvd3,
    Nat.mul_div_assoc (2^m)
      (by rw [pow_dvd_pow_iff (by simp) (by simp)]; exact h₂),
    Nat.pow_div h₂ (by simp)] at hfac
State after:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : 2 ^ m * 3 ^ (n - q) = 2 ^ p
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
⊢ m = p ∧ n = q

State before:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : 2 ^ m * 3 ^ (n - q) = 2 ^ p
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
⊢ m = p ∧ n = q
Tactic:
rw [mul_comm, ←one_mul (2^p)] at hfac
State after:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : 3 ^ (n - q) * 2 ^ m = 1 * 2 ^ p
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
⊢ m = p ∧ n = q

State before:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : 3 ^ (n - q) * 2 ^ m = 1 * 2 ^ p
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
⊢ m = p ∧ n = q
Tactic:
have hdvd2 : 2 ^ p ∣ 3 ^ (n - q) * 2 ^ m := by
  exact dvd_mul_of_dvd_right (pow_dvd_pow 2 h₁) (3 ^ (n - q))
State after:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : 3 ^ (n - q) * 2 ^ m = 1 * 2 ^ p
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
hdvd2 : 2 ^ p ∣ 3 ^ (n - q) * 2 ^ m
⊢ m = p ∧ n = q

State before:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : 3 ^ (n - q) * 2 ^ m = 1 * 2 ^ p
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
hdvd2 : 2 ^ p ∣ 3 ^ (n - q) * 2 ^ m
⊢ m = p ∧ n = q
Tactic:
rw [←Nat.div_eq_iff_eq_mul_left (by simp) hdvd2,
    Nat.mul_div_assoc (3^(n-q))
      (by rw [pow_dvd_pow_iff (by simp) (by simp)]; exact h₁),
    Nat.pow_div h₁ (by simp)] at hfac
State after:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : 3 ^ (n - q) * 2 ^ (m - p) = 1
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
hdvd2 : 2 ^ p ∣ 3 ^ (n - q) * 2 ^ m
⊢ m = p ∧ n = q

State before:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : 3 ^ (n - q) * 2 ^ (m - p) = 1
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
hdvd2 : 2 ^ p ∣ 3 ^ (n - q) * 2 ^ m
⊢ m = p ∧ n = q
Tactic:
rw [mul_eq_one_iff' (Nat.one_le_pow' (n - q) 2) (Nat.one_le_two_pow (m - p))] at hfac
State after:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : (2 + 1) ^ (n - q) = 1 ∧ 2 ^ (m - p) = 1
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
hdvd2 : 2 ^ p ∣ 3 ^ (n - q) * 2 ^ m
⊢ m = p ∧ n = q

State before:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : (2 + 1) ^ (n - q) = 1 ∧ 2 ^ (m - p) = 1
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
hdvd2 : 2 ^ p ∣ 3 ^ (n - q) * 2 ^ m
⊢ m = p ∧ n = q
Tactic:
rcases hfac with ⟨h3, h2⟩
State after:
case intro
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
hdvd2 : 2 ^ p ∣ 3 ^ (n - q) * 2 ^ m
h3 : (2 + 1) ^ (n - q) = 1
h2 : 2 ^ (m - p) = 1
⊢ m = p ∧ n = q

State before:
case intro
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
hdvd2 : 2 ^ p ∣ 3 ^ (n - q) * 2 ^ m
h3 : (2 + 1) ^ (n - q) = 1
h2 : 2 ^ (m - p) = 1
⊢ m = p ∧ n = q
Tactic:
ring_nf at *
State after:
case intro
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
h2 : 2 ^ (m - p) = 1
h3 : 3 ^ (n - q) = 1
hdvd2 : 2 ^ p ∣ 2 ^ m * 3 ^ (n - q)
⊢ m = p ∧ n = q

State before:
case intro
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
h2 : 2 ^ (m - p) = 1
h3 : 3 ^ (n - q) = 1
hdvd2 : 2 ^ p ∣ 2 ^ m * 3 ^ (n - q)
⊢ m = p ∧ n = q
Tactic:
apply_fun (λ e => Nat.log 2 e) at h2
State after:
case intro
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
h3 : 3 ^ (n - q) = 1
hdvd2 : 2 ^ p ∣ 2 ^ m * 3 ^ (n - q)
h2 : Nat.log 2 (2 ^ (m - p)) = Nat.log 2 1
⊢ m = p ∧ n = q

State before:
case intro
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
h3 : 3 ^ (n - q) = 1
hdvd2 : 2 ^ p ∣ 2 ^ m * 3 ^ (n - q)
h2 : Nat.log 2 (2 ^ (m - p)) = Nat.log 2 1
⊢ m = p ∧ n = q
Tactic:
rw [Nat.log_pow (by simp)] at h2
State after:
case intro
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
h3 : 3 ^ (n - q) = 1
hdvd2 : 2 ^ p ∣ 2 ^ m * 3 ^ (n - q)
h2 : m - p = Nat.log 2 1
⊢ m = p ∧ n = q

State before:
case intro
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
h3 : 3 ^ (n - q) = 1
hdvd2 : 2 ^ p ∣ 2 ^ m * 3 ^ (n - q)
h2 : m - p = Nat.log 2 1
⊢ m = p ∧ n = q
Tactic:
simp at h2
State after:
case intro
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
h3 : 3 ^ (n - q) = 1
hdvd2 : 2 ^ p ∣ 2 ^ m * 3 ^ (n - q)
h2 : m ≤ p
⊢ m = p ∧ n = q

State before:
case intro
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
h3 : 3 ^ (n - q) = 1
hdvd2 : 2 ^ p ∣ 2 ^ m * 3 ^ (n - q)
h2 : m ≤ p
⊢ m = p ∧ n = q
Tactic:
have heq₁ : m = p := by
  linarith
State after:
case intro
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
h3 : 3 ^ (n - q) = 1
hdvd2 : 2 ^ p ∣ 2 ^ m * 3 ^ (n - q)
h2 : m ≤ p
heq₁ : m = p
⊢ m = p ∧ n = q

State before:
case intro
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
h3 : 3 ^ (n - q) = 1
hdvd2 : 2 ^ p ∣ 2 ^ m * 3 ^ (n - q)
h2 : m ≤ p
heq₁ : m = p
⊢ m = p ∧ n = q
Tactic:
apply_fun (λ e => Nat.log 3 e) at h3
State after:
case intro
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
hdvd2 : 2 ^ p ∣ 2 ^ m * 3 ^ (n - q)
h2 : m ≤ p
heq₁ : m = p
h3 : Nat.log 3 (3 ^ (n - q)) = Nat.log 3 1
⊢ m = p ∧ n = q

State before:
case intro
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
hdvd2 : 2 ^ p ∣ 2 ^ m * 3 ^ (n - q)
h2 : m ≤ p
heq₁ : m = p
h3 : Nat.log 3 (3 ^ (n - q)) = Nat.log 3 1
⊢ m = p ∧ n = q
Tactic:
rw [Nat.log_pow (by simp)] at h3
State after:
case intro
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
hdvd2 : 2 ^ p ∣ 2 ^ m * 3 ^ (n - q)
h2 : m ≤ p
heq₁ : m = p
h3 : n - q = Nat.log 3 1
⊢ m = p ∧ n = q

State before:
case intro
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
hdvd2 : 2 ^ p ∣ 2 ^ m * 3 ^ (n - q)
h2 : m ≤ p
heq₁ : m = p
h3 : n - q = Nat.log 3 1
⊢ m = p ∧ n = q
Tactic:
simp at h3
State after:
case intro
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
hdvd2 : 2 ^ p ∣ 2 ^ m * 3 ^ (n - q)
h2 : m ≤ p
heq₁ : m = p
h3 : n ≤ q
⊢ m = p ∧ n = q

State before:
case intro
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
hdvd2 : 2 ^ p ∣ 2 ^ m * 3 ^ (n - q)
h2 : m ≤ p
heq₁ : m = p
h3 : n ≤ q
⊢ m = p ∧ n = q
Tactic:
have heq₂ : n = q := by
  linarith
State after:
case intro
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
hdvd2 : 2 ^ p ∣ 2 ^ m * 3 ^ (n - q)
h2 : m ≤ p
heq₁ : m = p
h3 : n ≤ q
heq₂ : n = q
⊢ m = p ∧ n = q

State before:
case intro
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
hdvd2 : 2 ^ p ∣ 2 ^ m * 3 ^ (n - q)
h2 : m ≤ p
heq₁ : m = p
h3 : n ≤ q
heq₂ : n = q
⊢ m = p ∧ n = q
Tactic:
exact ⟨heq₁, heq₂⟩
State after:
no goals

State before:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : 2 ^ m * 3 ^ n = 2 ^ p * 3 ^ q
⊢ 3 ^ q ∣ 2 ^ m * 3 ^ n
Tactic:
exact dvd_mul_of_dvd_right (pow_dvd_pow 3 h₂) (2 ^ m)
State after:
no goals

State before:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : 2 ^ m * 3 ^ n = 2 ^ p * 3 ^ q
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
⊢ 0 < 3 ^ q
Tactic:
simp
State after:
no goals

State before:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : 2 ^ m * 3 ^ n / 3 ^ q = 2 ^ p
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
⊢ 3 ^ q ∣ 3 ^ n
Tactic:
rw [pow_dvd_pow_iff (by simp) (by simp)]
State after:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : 2 ^ m * 3 ^ n / 3 ^ q = 2 ^ p
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
⊢ q ≤ n

State before:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : 2 ^ m * 3 ^ n / 3 ^ q = 2 ^ p
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
⊢ q ≤ n
Tactic:
exact h₂
State after:
no goals

State before:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : 2 ^ m * 3 ^ n / 3 ^ q = 2 ^ p
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
⊢ 3 ≠ 0
Tactic:
simp
State after:
no goals

State before:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : 2 ^ m * 3 ^ n / 3 ^ q = 2 ^ p
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
⊢ ¬IsUnit 3
Tactic:
simp
State after:
no goals

State before:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : 2 ^ m * (3 ^ n / 3 ^ q) = 2 ^ p
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
⊢ 0 < 3
Tactic:
simp
State after:
no goals

State before:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : 3 ^ (n - q) * 2 ^ m = 1 * 2 ^ p
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
⊢ 2 ^ p ∣ 3 ^ (n - q) * 2 ^ m
Tactic:
exact dvd_mul_of_dvd_right (pow_dvd_pow 2 h₁) (3 ^ (n - q))
State after:
no goals

State before:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : 3 ^ (n - q) * 2 ^ m = 1 * 2 ^ p
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
hdvd2 : 2 ^ p ∣ 3 ^ (n - q) * 2 ^ m
⊢ 0 < 2 ^ p
Tactic:
simp
State after:
no goals

State before:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : 3 ^ (n - q) * 2 ^ m / 2 ^ p = 1
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
hdvd2 : 2 ^ p ∣ 3 ^ (n - q) * 2 ^ m
⊢ 2 ^ p ∣ 2 ^ m
Tactic:
rw [pow_dvd_pow_iff (by simp) (by simp)]
State after:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : 3 ^ (n - q) * 2 ^ m / 2 ^ p = 1
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
hdvd2 : 2 ^ p ∣ 3 ^ (n - q) * 2 ^ m
⊢ p ≤ m

State before:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : 3 ^ (n - q) * 2 ^ m / 2 ^ p = 1
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
hdvd2 : 2 ^ p ∣ 3 ^ (n - q) * 2 ^ m
⊢ p ≤ m
Tactic:
exact h₁
State after:
no goals

State before:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : 3 ^ (n - q) * 2 ^ m / 2 ^ p = 1
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
hdvd2 : 2 ^ p ∣ 3 ^ (n - q) * 2 ^ m
⊢ 2 ≠ 0
Tactic:
simp
State after:
no goals

State before:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : 3 ^ (n - q) * 2 ^ m / 2 ^ p = 1
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
hdvd2 : 2 ^ p ∣ 3 ^ (n - q) * 2 ^ m
⊢ ¬IsUnit 2
Tactic:
simp
State after:
no goals

State before:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hfac : 3 ^ (n - q) * (2 ^ m / 2 ^ p) = 1
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
hdvd2 : 2 ^ p ∣ 3 ^ (n - q) * 2 ^ m
⊢ 0 < 2
Tactic:
simp
State after:
no goals

State before:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
h3 : 3 ^ (n - q) = 1
hdvd2 : 2 ^ p ∣ 2 ^ m * 3 ^ (n - q)
h2 : Nat.log 2 (2 ^ (m - p)) = Nat.log 2 1
⊢ 1 < 2
Tactic:
simp
State after:
no goals

State before:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
h3 : 3 ^ (n - q) = 1
hdvd2 : 2 ^ p ∣ 2 ^ m * 3 ^ (n - q)
h2 : m ≤ p
⊢ m = p
Tactic:
linarith
State after:
no goals

State before:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
hdvd2 : 2 ^ p ∣ 2 ^ m * 3 ^ (n - q)
h2 : m ≤ p
heq₁ : m = p
h3 : Nat.log 3 (3 ^ (n - q)) = Nat.log 3 1
⊢ 1 < 3
Tactic:
simp
State after:
no goals

State before:
m n q p : ℕ
h₁ : p ≤ m
h₂ : q ≤ n
hdvd3 : 3 ^ q ∣ 2 ^ m * 3 ^ n
hdvd2 : 2 ^ p ∣ 2 ^ m * 3 ^ (n - q)
h2 : m ≤ p
heq₁ : m = p
h3 : n ≤ q
⊢ n = q
Tactic:
linarith
State after:
no goals