Theorem: associated_of_dvd (Flt/OddPrimeOrFour.lean)

State before:
a p : ℤ
ha : OddPrimeOrFour a
hp : OddPrimeOrFour p
h : p ∣ a
⊢ Associated p a
Tactic:
obtain rfl | ⟨ap, aodd⟩ := ha <;> obtain rfl | ⟨pp, podd⟩ := hp
State after:
case inl.inl
h : 4 ∣ 4
⊢ Associated 4 4

case inl.inr.intro
p : ℤ
h : p ∣ 4
pp : Prime p
podd : Odd p
⊢ Associated p 4

case inr.intro.inl
a : ℤ
ap : Prime a
aodd : Odd a
h : 4 ∣ a
⊢ Associated 4 a

case inr.intro.inr.intro
a p : ℤ
h : p ∣ a
ap : Prime a
aodd : Odd a
pp : Prime p
podd : Odd p
⊢ Associated p a

State before:
case inl.inl
h : 4 ∣ 4
⊢ Associated 4 4
Tactic:
rfl
State after:
no goals

State before:
case inl.inr.intro
p : ℤ
h : p ∣ 4
pp : Prime p
podd : Odd p
⊢ Associated p 4
Tactic:
exfalso
State after:
case inl.inr.intro.h
p : ℤ
h : p ∣ 4
pp : Prime p
podd : Odd p
⊢ False

State before:
case inl.inr.intro.h
p : ℤ
h : p ∣ 4
pp : Prime p
podd : Odd p
⊢ False
Tactic:
have h0 : (4 : ℤ) = 2 ^ 2 := by norm_num
State after:
case inl.inr.intro.h
p : ℤ
h : p ∣ 4
pp : Prime p
podd : Odd p
h0 : 4 = 2 ^ 2
⊢ False

State before:
case inl.inr.intro.h
p : ℤ
h : p ∣ 4
pp : Prime p
podd : Odd p
h0 : 4 = 2 ^ 2
⊢ False
Tactic:
rw [h0] at h
State after:
case inl.inr.intro.h
p : ℤ
h : p ∣ 2 ^ 2
pp : Prime p
podd : Odd p
h0 : 4 = 2 ^ 2
⊢ False

State before:
case inl.inr.intro.h
p : ℤ
h : p ∣ 2 ^ 2
pp : Prime p
podd : Odd p
h0 : 4 = 2 ^ 2
⊢ False
Tactic:
refine' Int.even_iff_not_odd.mp _ podd
State after:
case inl.inr.intro.h
p : ℤ
h : p ∣ 2 ^ 2
pp : Prime p
podd : Odd p
h0 : 4 = 2 ^ 2
⊢ Even p

State before:
case inl.inr.intro.h
p : ℤ
h : p ∣ 2 ^ 2
pp : Prime p
podd : Odd p
h0 : 4 = 2 ^ 2
⊢ Even p
Tactic:
rw [even_iff_two_dvd]
State after:
case inl.inr.intro.h
p : ℤ
h : p ∣ 2 ^ 2
pp : Prime p
podd : Odd p
h0 : 4 = 2 ^ 2
⊢ 2 ∣ p

State before:
case inl.inr.intro.h
p : ℤ
h : p ∣ 2 ^ 2
pp : Prime p
podd : Odd p
h0 : 4 = 2 ^ 2
⊢ 2 ∣ p
Tactic:
apply Associated.dvd _
State after:
p : ℤ
h : p ∣ 2 ^ 2
pp : Prime p
podd : Odd p
h0 : 4 = 2 ^ 2
⊢ Associated 2 p

State before:
p : ℤ
h : p ∣ 2 ^ 2
pp : Prime p
podd : Odd p
h0 : 4 = 2 ^ 2
⊢ Associated 2 p
Tactic:
exact ((pp.dvd_prime_iff_associated Int.prime_two).mp (pp.dvd_of_dvd_pow h)).symm
State after:
no goals

State before:
p : ℤ
h : p ∣ 4
pp : Prime p
podd : Odd p
⊢ 4 = 2 ^ 2
Tactic:
norm_num
State after:
no goals

State before:
case inr.intro.inl
a : ℤ
ap : Prime a
aodd : Odd a
h : 4 ∣ a
⊢ Associated 4 a
Tactic:
exfalso
State after:
case inr.intro.inl.h
a : ℤ
ap : Prime a
aodd : Odd a
h : 4 ∣ a
⊢ False

State before:
case inr.intro.inl.h
a : ℤ
ap : Prime a
aodd : Odd a
h : 4 ∣ a
⊢ False
Tactic:
rw [Int.odd_iff_not_even] at aodd
State after:
case inr.intro.inl.h
a : ℤ
ap : Prime a
aodd : ¬Even a
h : 4 ∣ a
⊢ False

State before:
case inr.intro.inl.h
a : ℤ
ap : Prime a
aodd : ¬Even a
h : 4 ∣ a
⊢ False
Tactic:
refine' aodd _
State after:
case inr.intro.inl.h
a : ℤ
ap : Prime a
aodd : ¬Even a
h : 4 ∣ a
⊢ Even a

State before:
case inr.intro.inl.h
a : ℤ
ap : Prime a
aodd : ¬Even a
h : 4 ∣ a
⊢ Even a
Tactic:
rw [even_iff_two_dvd]
State after:
case inr.intro.inl.h
a : ℤ
ap : Prime a
aodd : ¬Even a
h : 4 ∣ a
⊢ 2 ∣ a

State before:
case inr.intro.inl.h
a : ℤ
ap : Prime a
aodd : ¬Even a
h : 4 ∣ a
⊢ 2 ∣ a
Tactic:
refine' dvd_trans _ h
State after:
case inr.intro.inl.h
a : ℤ
ap : Prime a
aodd : ¬Even a
h : 4 ∣ a
⊢ 2 ∣ 4

State before:
case inr.intro.inl.h
a : ℤ
ap : Prime a
aodd : ¬Even a
h : 4 ∣ a
⊢ 2 ∣ 4
Tactic:
norm_num
State after:
no goals

State before:
case inr.intro.inr.intro
a p : ℤ
h : p ∣ a
ap : Prime a
aodd : Odd a
pp : Prime p
podd : Odd p
⊢ Associated p a
Tactic:
rwa [Prime.dvd_prime_iff_associated pp ap] at h
State after:
no goals