Theorem: dvd_or_dvd (Flt/OddPrimeOrFour.lean)

State before:
a p x : ℤ
ha : OddPrimeOrFour a
hp : OddPrimeOrFour p
hdvd : p ∣ a * x
⊢ p ∣ a ∨ p ∣ x
Tactic:
obtain rfl | ⟨pp, -⟩ := hp
State after:
case inl
a x : ℤ
ha : OddPrimeOrFour a
hdvd : 4 ∣ a * x
⊢ 4 ∣ a ∨ 4 ∣ x

case inr.intro
a p x : ℤ
ha : OddPrimeOrFour a
hdvd : p ∣ a * x
pp : Prime p
⊢ p ∣ a ∨ p ∣ x

State before:
case inl
a x : ℤ
ha : OddPrimeOrFour a
hdvd : 4 ∣ a * x
⊢ 4 ∣ a ∨ 4 ∣ x
Tactic:
obtain rfl | ⟨ap, aodd⟩ := ha
State after:
case inl.inl
x : ℤ
hdvd : 4 ∣ 4 * x
⊢ 4 ∣ 4 ∨ 4 ∣ x

case inl.inr.intro
a x : ℤ
hdvd : 4 ∣ a * x
ap : Prime a
aodd : Odd a
⊢ 4 ∣ a ∨ 4 ∣ x

State before:
case inl.inl
x : ℤ
hdvd : 4 ∣ 4 * x
⊢ 4 ∣ 4 ∨ 4 ∣ x
Tactic:
exact Or.inl dvd_rfl
State after:
no goals

State before:
case inl.inr.intro
a x : ℤ
hdvd : 4 ∣ a * x
ap : Prime a
aodd : Odd a
⊢ 4 ∣ a ∨ 4 ∣ x
Tactic:
right
State after:
case inl.inr.intro.h
a x : ℤ
hdvd : 4 ∣ a * x
ap : Prime a
aodd : Odd a
⊢ 4 ∣ x

State before:
case inl.inr.intro.h
a x : ℤ
hdvd : 4 ∣ a * x
ap : Prime a
aodd : Odd a
⊢ 4 ∣ x
Tactic:
have : (4 : ℤ) = 2 ^ 2 := by norm_num
State after:
case inl.inr.intro.h
a x : ℤ
hdvd : 4 ∣ a * x
ap : Prime a
aodd : Odd a
this : 4 = 2 ^ 2
⊢ 4 ∣ x

State before:
case inl.inr.intro.h
a x : ℤ
hdvd : 4 ∣ a * x
ap : Prime a
aodd : Odd a
this : 4 = 2 ^ 2
⊢ 4 ∣ x
Tactic:
rw [this] at hdvd⊢
State after:
case inl.inr.intro.h
a x : ℤ
hdvd : 2 ^ 2 ∣ a * x
ap : Prime a
aodd : Odd a
this : 4 = 2 ^ 2
⊢ 2 ^ 2 ∣ x

State before:
case inl.inr.intro.h
a x : ℤ
hdvd : 2 ^ 2 ∣ a * x
ap : Prime a
aodd : Odd a
this : 4 = 2 ^ 2
⊢ 2 ^ 2 ∣ x
Tactic:
apply Int.prime_two.pow_dvd_of_dvd_mul_left _ _ hdvd
State after:
a x : ℤ
hdvd : 2 ^ 2 ∣ a * x
ap : Prime a
aodd : Odd a
this : 4 = 2 ^ 2
⊢ ¬2 ∣ a

State before:
a x : ℤ
hdvd : 2 ^ 2 ∣ a * x
ap : Prime a
aodd : Odd a
this : 4 = 2 ^ 2
⊢ ¬2 ∣ a
Tactic:
rwa [← even_iff_two_dvd, ← Int.odd_iff_not_even]
State after:
no goals

State before:
a x : ℤ
hdvd : 4 ∣ a * x
ap : Prime a
aodd : Odd a
⊢ 4 = 2 ^ 2
Tactic:
norm_num
State after:
no goals

State before:
case inr.intro
a p x : ℤ
ha : OddPrimeOrFour a
hdvd : p ∣ a * x
pp : Prime p
⊢ p ∣ a ∨ p ∣ x
Tactic:
exact pp.dvd_or_dvd hdvd
State after:
no goals