Theorem: Imo2005P4.find_specified_factor (Compfiles/Imo2005P4.lean)

State before:
p : ℕ
hp : p.Prime
hp2 : p ≠ 2
hp3 : p ≠ 3
⊢ ↑p ∣ a (p - 2)
Tactic:
rw [Ne, ← Nat.prime_dvd_prime_iff_eq hp (by decide), ← Nat.Prime.coprime_iff_not_dvd hp]
  at hp2 hp3
State after:
p : ℕ
hp : p.Prime
hp2 : p.Coprime 2
hp3 : p.Coprime 3
⊢ ↑p ∣ a (p - 2)

State before:
p : ℕ
hp : p.Prime
hp2 : p.Coprime 2
hp3 : p.Coprime 3
⊢ ↑p ∣ a (p - 2)
Tactic:
have : Int.gcd p 6 = 1 := Nat.coprime_mul_iff_right.2 ⟨hp2, hp3⟩
State after:
p : ℕ
hp : p.Prime
hp2 : p.Coprime 2
hp3 : p.Coprime 3
this : (↑p).gcd 6 = 1
⊢ ↑p ∣ a (p - 2)

State before:
p : ℕ
hp : p.Prime
hp2 : p.Coprime 2
hp3 : p.Coprime 3
this : (↑p).gcd 6 = 1
⊢ ↑p ∣ a (p - 2)
Tactic:
have hp' : p - 1 = p - 2 + 1 := Eq.symm <| Nat.succ_pred <| (tsub_pos_of_lt hp.one_lt).ne'
State after:
p : ℕ
hp : p.Prime
hp2 : p.Coprime 2
hp3 : p.Coprime 3
this : (↑p).gcd 6 = 1
hp' : p - 1 = p - 2 + 1
⊢ ↑p ∣ a (p - 2)

State before:
p : ℕ
hp : p.Prime
hp2 : p.Coprime 2
hp3 : p.Coprime 3
this : (↑p).gcd 6 = 1
hp' : p - 1 = p - 2 + 1
⊢ ↑p ∣ a (p - 2)
Tactic:
rw [← Int.modEq_zero_iff_dvd, ← Int.ediv_one p, ← Nat.cast_one, ← this]
State after:
p : ℕ
hp : p.Prime
hp2 : p.Coprime 2
hp3 : p.Coprime 3
this : (↑p).gcd 6 = 1
hp' : p - 1 = p - 2 + 1
⊢ a (p - 2) ≡ 0 [ZMOD ↑p / ↑((↑p).gcd 6)]

State before:
p : ℕ
hp : p.Prime
hp2 : p.Coprime 2
hp3 : p.Coprime 3
this : (↑p).gcd 6 = 1
hp' : p - 1 = p - 2 + 1
⊢ a (p - 2) ≡ 0 [ZMOD ↑p / ↑((↑p).gcd 6)]
Tactic:
refine Int.ModEq.cancel_left_div_gcd (Nat.cast_pos.2 hp.pos) ?_
State after:
p : ℕ
hp : p.Prime
hp2 : p.Coprime 2
hp3 : p.Coprime 3
this : (↑p).gcd 6 = 1
hp' : p - 1 = p - 2 + 1
⊢ 6 * a (p - 2) ≡ 6 * 0 [ZMOD ↑p]

State before:
p : ℕ
hp : p.Prime
hp2 : p.Coprime 2
hp3 : p.Coprime 3
this : (↑p).gcd 6 = 1
hp' : p - 1 = p - 2 + 1
⊢ 6 * a (p - 2) ≡ 6 * 0 [ZMOD ↑p]
Tactic:
calc
  6 * a (p - 2) = 3 * 2 ^ (p - 1) + 2 * 3 ^ (p - 1) + (2 * 3) ^ (p - 1) - 6 := by
    simp only [a, hp', pow_succ']; ring
  _ ≡ 3 * 1 + 2 * 1 + 1 - 6 [ZMOD p] := by
    gcongr <;> apply Int.ModEq.pow_card_sub_one_eq_one hp <;>
      rwa [Int.isCoprime_iff_gcd_eq_one, Int.gcd_comm]
  _ = 0 := rfl
State after:
no goals

State before:
p : ℕ
hp : p.Prime
hp2 : ¬p ∣ 2
hp3 : ¬p = 3
⊢ Nat.Prime 3
Tactic:
decide
State after:
no goals

State before:
p : ℕ
hp : p.Prime
hp2 : p.Coprime 2
hp3 : p.Coprime 3
this : (↑p).gcd 6 = 1
hp' : p - 1 = p - 2 + 1
⊢ 6 * a (p - 2) = 3 * 2 ^ (p - 1) + 2 * 3 ^ (p - 1) + (2 * 3) ^ (p - 1) - 6
Tactic:
simp only [a, hp', pow_succ']
State after:
p : ℕ
hp : p.Prime
hp2 : p.Coprime 2
hp3 : p.Coprime 3
this : (↑p).gcd 6 = 1
hp' : p - 1 = p - 2 + 1
⊢ 6 * (2 ^ (p - 2) + 3 ^ (p - 2) + 6 ^ (p - 2) - 1) =
    3 * (2 * 2 ^ (p - 2)) + 2 * (3 * 3 ^ (p - 2)) + 2 * 3 * (2 * 3) ^ (p - 2) - 6

State before:
p : ℕ
hp : p.Prime
hp2 : p.Coprime 2
hp3 : p.Coprime 3
this : (↑p).gcd 6 = 1
hp' : p - 1 = p - 2 + 1
⊢ 6 * (2 ^ (p - 2) + 3 ^ (p - 2) + 6 ^ (p - 2) - 1) =
    3 * (2 * 2 ^ (p - 2)) + 2 * (3 * 3 ^ (p - 2)) + 2 * 3 * (2 * 3) ^ (p - 2) - 6
Tactic:
ring
State after:
no goals

State before:
p : ℕ
hp : p.Prime
hp2 : p.Coprime 2
hp3 : p.Coprime 3
this : (↑p).gcd 6 = 1
hp' : p - 1 = p - 2 + 1
⊢ 3 * 2 ^ (p - 1) + 2 * 3 ^ (p - 1) + (2 * 3) ^ (p - 1) - 6 ≡ 3 * 1 + 2 * 1 + 1 - 6 [ZMOD ↑p]
Tactic:
gcongr <;> apply Int.ModEq.pow_card_sub_one_eq_one hp <;>
  rwa [Int.isCoprime_iff_gcd_eq_one, Int.gcd_comm]
State after:
no goals