Theorem: two_pow_three_pow_unique_factorization (meetings/ex4.lean)

State before:
m n q p : ℕ
h : 2 ^ m * 3 ^ n = 2 ^ p * 3 ^ q
⊢ m = p ∧ n = q
Tactic:
apply_fun Nat.factorization at h
State after:
m n q p : ℕ
h : Nat.factorization (2 ^ m * 3 ^ n) = Nat.factorization (2 ^ p * 3 ^ q)
⊢ m = p ∧ n = q

State before:
m n q p : ℕ
h : Nat.factorization (2 ^ m * 3 ^ n) = Nat.factorization (2 ^ p * 3 ^ q)
⊢ m = p ∧ n = q
Tactic:
rw [Nat.factorization_mul, Nat.factorization_mul] at h
State after:
m n q p : ℕ
h : Nat.factorization (2 ^ m) + Nat.factorization (3 ^ n) = Nat.factorization (2 ^ p) + Nat.factorization (3 ^ q)
⊢ m = p ∧ n = q

case ha
m n q p : ℕ
h : Nat.factorization (2 ^ m) + Nat.factorization (3 ^ n) = Nat.factorization (2 ^ p * 3 ^ q)
⊢ 2 ^ p ≠ 0

case hb
m n q p : ℕ
h : Nat.factorization (2 ^ m) + Nat.factorization (3 ^ n) = Nat.factorization (2 ^ p * 3 ^ q)
⊢ 3 ^ q ≠ 0

case ha
m n q p : ℕ
h : Nat.factorization (2 ^ m * 3 ^ n) = Nat.factorization (2 ^ p * 3 ^ q)
⊢ 2 ^ m ≠ 0

case hb
m n q p : ℕ
h : Nat.factorization (2 ^ m * 3 ^ n) = Nat.factorization (2 ^ p * 3 ^ q)
⊢ 3 ^ n ≠ 0

State before:
case ha
m n q p : ℕ
h : Nat.factorization (2 ^ m) + Nat.factorization (3 ^ n) = Nat.factorization (2 ^ p * 3 ^ q)
⊢ 2 ^ p ≠ 0

case hb
m n q p : ℕ
h : Nat.factorization (2 ^ m) + Nat.factorization (3 ^ n) = Nat.factorization (2 ^ p * 3 ^ q)
⊢ 3 ^ q ≠ 0

case ha
m n q p : ℕ
h : Nat.factorization (2 ^ m * 3 ^ n) = Nat.factorization (2 ^ p * 3 ^ q)
⊢ 2 ^ m ≠ 0

case hb
m n q p : ℕ
h : Nat.factorization (2 ^ m * 3 ^ n) = Nat.factorization (2 ^ p * 3 ^ q)
⊢ 3 ^ n ≠ 0
Tactic:
all_goals positivity
State after:
no goals

State before:
m n q p : ℕ
h : Nat.factorization (2 ^ m) + Nat.factorization (3 ^ n) = Nat.factorization (2 ^ p) + Nat.factorization (3 ^ q)
⊢ m = p ∧ n = q
Tactic:
simp_rw [Nat.factorization_pow] at h
State after:
m n q p : ℕ
h : m • Nat.factorization 2 + n • Nat.factorization 3 = p • Nat.factorization 2 + q • Nat.factorization 3
⊢ m = p ∧ n = q

State before:
m n q p : ℕ
h : m • Nat.factorization 2 + n • Nat.factorization 3 = p • Nat.factorization 2 + q • Nat.factorization 3
⊢ m = p ∧ n = q
Tactic:
constructor
State after:
case left
m n q p : ℕ
h : m • Nat.factorization 2 + n • Nat.factorization 3 = p • Nat.factorization 2 + q • Nat.factorization 3
⊢ m = p

case right
m n q p : ℕ
h : m • Nat.factorization 2 + n • Nat.factorization 3 = p • Nat.factorization 2 + q • Nat.factorization 3
⊢ n = q

State before:
case left
m n q p : ℕ
h : m • Nat.factorization 2 + n • Nat.factorization 3 = p • Nat.factorization 2 + q • Nat.factorization 3
⊢ m = p
Tactic:
replace h := FunLike.congr_fun h 2
State after:
case left
m n q p : ℕ
h : ↑(m • Nat.factorization 2 + n • Nat.factorization 3) 2 = ↑(p • Nat.factorization 2 + q • Nat.factorization 3) 2
⊢ m = p

State before:
case left
m n q p : ℕ
h : ↑(m • Nat.factorization 2 + n • Nat.factorization 3) 2 = ↑(p • Nat.factorization 2 + q • Nat.factorization 3) 2
⊢ m = p
Tactic:
have : ¬ 2 ∣ 3 := by norm_num
State after:
case left
m n q p : ℕ
h : ↑(m • Nat.factorization 2 + n • Nat.factorization 3) 2 = ↑(p • Nat.factorization 2 + q • Nat.factorization 3) 2
this : ¬2 ∣ 3
⊢ m = p

State before:
case left
m n q p : ℕ
h : ↑(m • Nat.factorization 2 + n • Nat.factorization 3) 2 = ↑(p • Nat.factorization 2 + q • Nat.factorization 3) 2
this : ¬2 ∣ 3
⊢ m = p
Tactic:
simp_rw [Finsupp.add_apply, Finsupp.smul_apply, Nat.prime_two.factorization_self,
  nsmul_one, Nat.factorization_eq_zero_of_not_dvd this, smul_zero, add_zero] at h
State after:
case left
m n q p : ℕ
this : ¬2 ∣ 3
h : ↑m = ↑p
⊢ m = p

State before:
case left
m n q p : ℕ
this : ¬2 ∣ 3
h : ↑m = ↑p
⊢ m = p
Tactic:
exact h
State after:
no goals

State before:
m n q p : ℕ
h : ↑(m • Nat.factorization 2 + n • Nat.factorization 3) 2 = ↑(p • Nat.factorization 2 + q • Nat.factorization 3) 2
⊢ ¬2 ∣ 3
Tactic:
norm_num
State after:
no goals

State before:
case right
m n q p : ℕ
h : m • Nat.factorization 2 + n • Nat.factorization 3 = p • Nat.factorization 2 + q • Nat.factorization 3
⊢ n = q
Tactic:
replace h := FunLike.congr_fun h 3
State after:
case right
m n q p : ℕ
h : ↑(m • Nat.factorization 2 + n • Nat.factorization 3) 3 = ↑(p • Nat.factorization 2 + q • Nat.factorization 3) 3
⊢ n = q

State before:
case right
m n q p : ℕ
h : ↑(m • Nat.factorization 2 + n • Nat.factorization 3) 3 = ↑(p • Nat.factorization 2 + q • Nat.factorization 3) 3
⊢ n = q
Tactic:
have : ¬ 3 ∣ 2 := Nat.not_dvd_of_pos_of_lt (by simp) (by simp)
State after:
case right
m n q p : ℕ
h : ↑(m • Nat.factorization 2 + n • Nat.factorization 3) 3 = ↑(p • Nat.factorization 2 + q • Nat.factorization 3) 3
this : ¬3 ∣ 2
⊢ n = q

State before:
case right
m n q p : ℕ
h : ↑(m • Nat.factorization 2 + n • Nat.factorization 3) 3 = ↑(p • Nat.factorization 2 + q • Nat.factorization 3) 3
this : ¬3 ∣ 2
⊢ n = q
Tactic:
simp_rw [Finsupp.add_apply, Finsupp.smul_apply, Nat.prime_three.factorization_self,
  nsmul_one, Nat.factorization_eq_zero_of_not_dvd this, smul_zero, zero_add] at h
State after:
case right
m n q p : ℕ
this : ¬3 ∣ 2
h : ↑n = ↑q
⊢ n = q

State before:
case right
m n q p : ℕ
this : ¬3 ∣ 2
h : ↑n = ↑q
⊢ n = q
Tactic:
exact h
State after:
no goals

State before:
m n q p : ℕ
h : ↑(m • Nat.factorization 2 + n • Nat.factorization 3) 3 = ↑(p • Nat.factorization 2 + q • Nat.factorization 3) 3
⊢ 0 < 2
Tactic:
simp
State after:
no goals

State before:
m n q p : ℕ
h : ↑(m • Nat.factorization 2 + n • Nat.factorization 3) 3 = ↑(p • Nat.factorization 2 + q • Nat.factorization 3) 3
⊢ 2 < 3
Tactic:
simp
State after:
no goals

State before:
case hb
m n q p : ℕ
h : Nat.factorization (2 ^ m * 3 ^ n) = Nat.factorization (2 ^ p * 3 ^ q)
⊢ 3 ^ n ≠ 0
Tactic:
positivity
State after:
no goals