Theorem: OddPrimeOrFour.exists_and_dvd (FltRegular/FltThree/OddPrimeOrFour.lean)

State before:
n : ℕ
n2 : 2 < n
⊢ ∃ p, p ∣ n ∧ OddPrimeOrFour p
Tactic:
obtain h4 | ⟨p, hpprime, hpdvd, hpodd⟩ := Nat.four_dvd_or_exists_odd_prime_and_dvd_of_two_lt n2
State after:
case inl
n : ℕ
n2 : 2 < n
h4 : 4 ∣ n
⊢ ∃ p, p ∣ n ∧ OddPrimeOrFour p

case inr.intro.intro.intro
n : ℕ
n2 : 2 < n
p : ℕ
hpprime : p.Prime
hpdvd : p ∣ n
hpodd : Odd p
⊢ ∃ p, p ∣ n ∧ OddPrimeOrFour p

State before:
case inl
n : ℕ
n2 : 2 < n
h4 : 4 ∣ n
⊢ ∃ p, p ∣ n ∧ OddPrimeOrFour p
Tactic:
exact ⟨4, h4, Or.inl rfl⟩
State after:
no goals

State before:
case inr.intro.intro.intro
n : ℕ
n2 : 2 < n
p : ℕ
hpprime : p.Prime
hpdvd : p ∣ n
hpodd : Odd p
⊢ ∃ p, p ∣ n ∧ OddPrimeOrFour p
Tactic:
exact ⟨p, hpdvd, Or.inr ⟨hpprime, hpodd⟩⟩
State after:
no goals