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

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

case inl.inr.intro
p : ℕ
h : p ∣ 4
pp : p.Prime
podd : Odd p
⊢ p = 4

case inr.intro.inl
a : ℕ
ap : a.Prime
aodd : Odd a
h : 4 ∣ a
⊢ 4 = a

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

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

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

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

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

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

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

State before:
case inl.inr.intro
p : ℕ
h : p ∣ 2 ^ 2
pp : p.Prime
podd : Odd p
h0 : 4 = 2 ^ 2
⊢ 2 ∣ p
Tactic:
exact pp.dvd_symm Nat.prime_two (pp.dvd_of_dvd_pow h)
State after:
no goals

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

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

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

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

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

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

State before:
case inr.intro.inl
a : ℕ
ap : a.Prime
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 : a.Prime
aodd : Odd a
pp : p.Prime
podd : Odd p
⊢ p = a
Tactic:
rwa [Nat.prime_dvd_prime_iff_eq pp ap] at h
State after:
no goals