Theorem: OddPrimeOrFour.exists_and_dvd (Flt/OddPrimeOrFour.lean)

State before:
n : ℤ
n2 : 2 < n
⊢ ∃ p, p ∣ n ∧ OddPrimeOrFour p
Tactic:
lift n to ℕ using (zero_lt_two.trans n2).le
State after:
case intro
n : ℕ
n2 : 2 < ↑n
⊢ ∃ p, p ∣ ↑n ∧ OddPrimeOrFour p

State before:
case intro
n : ℕ
n2 : 2 < ↑n
⊢ ∃ p, p ∣ ↑n ∧ OddPrimeOrFour p
Tactic:
norm_cast  at n2
State after:
case intro
n : ℕ
n2 : 2 < n
⊢ ∃ p, p ∣ ↑n ∧ OddPrimeOrFour p

State before:
case intro
n : ℕ
n2 : 2 < n
⊢ ∃ p, p ∣ ↑n ∧ OddPrimeOrFour p
Tactic:
obtain ⟨k, rfl⟩ | ⟨p, hp, hdvd, hodd⟩ := n.eq_two_pow_or_exists_odd_prime_and_dvd
State after:
case intro.inl.intro
k : ℕ
n2 : 2 < 2 ^ k
⊢ ∃ p, p ∣ ↑(2 ^ k) ∧ OddPrimeOrFour p

case intro.inr.intro.intro.intro
n : ℕ
n2 : 2 < n
p : ℕ
hp : Nat.Prime p
hdvd : p ∣ n
hodd : Odd p
⊢ ∃ p, p ∣ ↑n ∧ OddPrimeOrFour p

State before:
case intro.inl.intro
k : ℕ
n2 : 2 < 2 ^ k
⊢ ∃ p, p ∣ ↑(2 ^ k) ∧ OddPrimeOrFour p
Tactic:
refine' ⟨4, ⟨2 ^ (k - 2), _⟩, Or.inl rfl⟩
State after:
case intro.inl.intro
k : ℕ
n2 : 2 < 2 ^ k
⊢ ↑(2 ^ k) = 4 * 2 ^ (k - 2)

State before:
case intro.inl.intro
k : ℕ
n2 : 2 < 2 ^ k
⊢ ↑(2 ^ k) = 4 * 2 ^ (k - 2)
Tactic:
norm_cast
State after:
case intro.inl.intro
k : ℕ
n2 : 2 < 2 ^ k
⊢ 2 ^ k = 4 * 2 ^ (k - 2)

State before:
case intro.inl.intro
k : ℕ
n2 : 2 < 2 ^ k
⊢ 2 ^ k = 4 * 2 ^ (k - 2)
Tactic:
calc
  2 ^ k = 2 ^ 2 * 2 ^ (k - 2) := (pow_mul_pow_sub _ ?_).symm
  _ = 4 * 2 ^ (k - 2) := by norm_num
State after:
case intro.inl.intro
k : ℕ
n2 : 2 < 2 ^ k
⊢ 2 ≤ k

State before:
case intro.inl.intro
k : ℕ
n2 : 2 < 2 ^ k
⊢ 2 ≤ k
Tactic:
rcases k with (_ | _ | _)
State after:
case intro.inl.intro.zero
n2 : 2 < 2 ^ Nat.zero
⊢ 2 ≤ Nat.zero

case intro.inl.intro.succ.zero
n2 : 2 < 2 ^ Nat.succ Nat.zero
⊢ 2 ≤ Nat.succ Nat.zero

case intro.inl.intro.succ.succ
n✝ : ℕ
n2 : 2 < 2 ^ Nat.succ (Nat.succ n✝)
⊢ 2 ≤ Nat.succ (Nat.succ n✝)

State before:
k : ℕ
n2 : 2 < 2 ^ k
⊢ 2 ^ 2 * 2 ^ (k - 2) = 4 * 2 ^ (k - 2)
Tactic:
norm_num
State after:
no goals

State before:
case intro.inl.intro.zero
n2 : 2 < 2 ^ Nat.zero
⊢ 2 ≤ Nat.zero
Tactic:
exfalso
State after:
case intro.inl.intro.zero.h
n2 : 2 < 2 ^ Nat.zero
⊢ False

State before:
case intro.inl.intro.zero.h
n2 : 2 < 2 ^ Nat.zero
⊢ False
Tactic:
norm_num at n2
State after:
no goals

State before:
case intro.inl.intro.succ.zero
n2 : 2 < 2 ^ Nat.succ Nat.zero
⊢ 2 ≤ Nat.succ Nat.zero
Tactic:
exfalso
State after:
case intro.inl.intro.succ.zero.h
n2 : 2 < 2 ^ Nat.succ Nat.zero
⊢ False

State before:
case intro.inl.intro.succ.zero.h
n2 : 2 < 2 ^ Nat.succ Nat.zero
⊢ False
Tactic:
exact lt_irrefl _ n2
State after:
no goals

State before:
case intro.inl.intro.succ.succ
n✝ : ℕ
n2 : 2 < 2 ^ Nat.succ (Nat.succ n✝)
⊢ 2 ≤ Nat.succ (Nat.succ n✝)
Tactic:
exact le_add_self
State after:
no goals

State before:
case intro.inr.intro.intro.intro
n : ℕ
n2 : 2 < n
p : ℕ
hp : Nat.Prime p
hdvd : p ∣ n
hodd : Odd p
⊢ ∃ p, p ∣ ↑n ∧ OddPrimeOrFour p
Tactic:
rw [Nat.prime_iff_prime_int] at hp
State after:
case intro.inr.intro.intro.intro
n : ℕ
n2 : 2 < n
p : ℕ
hp : Prime ↑p
hdvd : p ∣ n
hodd : Odd p
⊢ ∃ p, p ∣ ↑n ∧ OddPrimeOrFour p

State before:
case intro.inr.intro.intro.intro
n : ℕ
n2 : 2 < n
p : ℕ
hp : Prime ↑p
hdvd : p ∣ n
hodd : Odd p
⊢ ∃ p, p ∣ ↑n ∧ OddPrimeOrFour p
Tactic:
rw [← Int.odd_coe_nat] at hodd
State after:
case intro.inr.intro.intro.intro
n : ℕ
n2 : 2 < n
p : ℕ
hp : Prime ↑p
hdvd : p ∣ n
hodd : Odd ↑p
⊢ ∃ p, p ∣ ↑n ∧ OddPrimeOrFour p

State before:
case intro.inr.intro.intro.intro
n : ℕ
n2 : 2 < n
p : ℕ
hp : Prime ↑p
hdvd : p ∣ n
hodd : Odd ↑p
⊢ ∃ p, p ∣ ↑n ∧ OddPrimeOrFour p
Tactic:
exact ⟨p, Int.coe_nat_dvd.mpr hdvd, Or.inr ⟨hp, hodd⟩⟩
State after:
no goals