internlm/Lean-Github huggingface dataset:
Theorem: OddPrimeOrFour.abs
Proof state before:
z : ℤ
h : OddPrimeOrFour z
⊢ OddPrimeOrFour (Abs.abs z)
Tactic:
obtain rfl | ⟨hp, ho⟩ := h
Proof state after:
case inl

⊢ OddPrimeOrFour (Abs.abs 4)

case inr.intro
z : ℤ
hp : Prime z
ho : Odd z
⊢ OddPrimeOrFour (Abs.abs z)
Theorem: OddPrimeOrFour.abs
Proof state before:
case inl

⊢ OddPrimeOrFour (Abs.abs 4)
Tactic:
left
Proof state after:
case inl.h

⊢ Abs.abs 4 = 4
Theorem: OddPrimeOrFour.abs
Proof state before:
case inl.h

⊢ Abs.abs 4 = 4
Tactic:
rw [abs_eq_self]
Proof state after:
case inl.h

⊢ 0 ≤ 4
Theorem: OddPrimeOrFour.abs
Proof state before:
case inl.h

⊢ 0 ≤ 4
Tactic:
norm_num
Proof state after:
no goals
Theorem: OddPrimeOrFour.abs
Proof state before:
case inr.intro
z : ℤ
hp : Prime z
ho : Odd z
⊢ OddPrimeOrFour (Abs.abs z)
Tactic:
right
Proof state after:
case inr.intro.h
z : ℤ
hp : Prime z
ho : Odd z
⊢ Prime (Abs.abs z) ∧ Odd (Abs.abs z)
Theorem: OddPrimeOrFour.abs
Proof state before:
case inr.intro.h
z : ℤ
hp : Prime z
ho : Odd z
⊢ Prime (Abs.abs z) ∧ Odd (Abs.abs z)
Tactic:
exact ⟨hp.abs, odd_abs.mpr ho⟩
Proof state after:
no goals
Theorem: OddPrimeOrFour.exists_and_dvd
Proof state before:
n : ℤ
n2 : 2 < n
⊢ ∃ p, p ∣ n ∧ OddPrimeOrFour p
Tactic:
lift n to ℕ using (zero_lt_two.trans n2).le
Proof state after:
case intro
n : ℕ
n2 : 2 < ↑n
⊢ ∃ p, p ∣ ↑n ∧ OddPrimeOrFour p
Theorem: OddPrimeOrFour.exists_and_dvd
Proof state before:
case intro
n : ℕ
n2 : 2 < ↑n
⊢ ∃ p, p ∣ ↑n ∧ OddPrimeOrFour p
Tactic:
norm_cast  at n2
Proof state after:
case intro
n : ℕ
n2 : 2 < n
⊢ ∃ p, p ∣ ↑n ∧ OddPrimeOrFour p
Theorem: OddPrimeOrFour.exists_and_dvd
Proof 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
Proof 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
Theorem: OddPrimeOrFour.exists_and_dvd
Proof 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⟩
Proof state after:
case intro.inl.intro
k : ℕ
n2 : 2 < 2 ^ k
⊢ ↑(2 ^ k) = 4 * 2 ^ (k - 2)
Theorem: OddPrimeOrFour.exists_and_dvd
Proof state before:
case intro.inl.intro
k : ℕ
n2 : 2 < 2 ^ k
⊢ ↑(2 ^ k) = 4 * 2 ^ (k - 2)
Tactic:
norm_cast
Proof state after:
case intro.inl.intro
k : ℕ
n2 : 2 < 2 ^ k
⊢ 2 ^ k = 4 * 2 ^ (k - 2)
Theorem: OddPrimeOrFour.exists_and_dvd
Proof 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
Proof state after:
case intro.inl.intro
k : ℕ
n2 : 2 < 2 ^ k
⊢ 2 ≤ k
Theorem: OddPrimeOrFour.exists_and_dvd
Proof state before:
case intro.inl.intro
k : ℕ
n2 : 2 < 2 ^ k
⊢ 2 ≤ k
Tactic:
rcases k with (_ | _ | _)
Proof 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✝)
Theorem: OddPrimeOrFour.exists_and_dvd
Proof state before:
k : ℕ
n2 : 2 < 2 ^ k
⊢ 2 ^ 2 * 2 ^ (k - 2) = 4 * 2 ^ (k - 2)
Tactic:
norm_num
Proof state after:
no goals
Theorem: OddPrimeOrFour.exists_and_dvd
Proof state before:
case intro.inl.intro.zero
n2 : 2 < 2 ^ Nat.zero
⊢ 2 ≤ Nat.zero
Tactic:
exfalso
Proof state after:
case intro.inl.intro.zero.h
n2 : 2 < 2 ^ Nat.zero
⊢ False
Theorem: OddPrimeOrFour.exists_and_dvd
Proof state before:
case intro.inl.intro.zero.h
n2 : 2 < 2 ^ Nat.zero
⊢ False
Tactic:
norm_num at n2
Proof state after:
no goals
Theorem: OddPrimeOrFour.exists_and_dvd
Proof state before:
case intro.inl.intro.succ.zero
n2 : 2 < 2 ^ Nat.succ Nat.zero
⊢ 2 ≤ Nat.succ Nat.zero
Tactic:
exfalso
Proof state after:
case intro.inl.intro.succ.zero.h
n2 : 2 < 2 ^ Nat.succ Nat.zero
⊢ False
Theorem: OddPrimeOrFour.exists_and_dvd
Proof state before:
case intro.inl.intro.succ.zero.h
n2 : 2 < 2 ^ Nat.succ Nat.zero
⊢ False
Tactic:
exact lt_irrefl _ n2
Proof state after:
no goals
Theorem: OddPrimeOrFour.exists_and_dvd
Proof 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
Proof state after:
no goals
Theorem: OddPrimeOrFour.exists_and_dvd
Proof 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
Proof 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
Theorem: OddPrimeOrFour.exists_and_dvd
Proof 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
Proof 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
Theorem: OddPrimeOrFour.exists_and_dvd
Proof 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⟩⟩
Proof state after:
no goals
Theorem: associated_of_dvd
Proof 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
Proof 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
Theorem: associated_of_dvd
Proof state before:
case inl.inl
h : 4 ∣ 4
⊢ Associated 4 4
Tactic:
rfl
Proof state after:
no goals
Theorem: associated_of_dvd
Proof state before:
case inl.inr.intro
p : ℤ
h : p ∣ 4
pp : Prime p
podd : Odd p
⊢ Associated p 4
Tactic:
exfalso
Proof state after:
case inl.inr.intro.h
p : ℤ
h : p ∣ 4
pp : Prime p
podd : Odd p
⊢ False
Theorem: associated_of_dvd
Proof 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
Proof state after:
case inl.inr.intro.h
p : ℤ
h : p ∣ 4
pp : Prime p
podd : Odd p
h0 : 4 = 2 ^ 2
⊢ False
Theorem: associated_of_dvd
Proof 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
Proof state after:
case inl.inr.intro.h
p : ℤ
h : p ∣ 2 ^ 2
pp : Prime p
podd : Odd p
h0 : 4 = 2 ^ 2
⊢ False
Theorem: associated_of_dvd
Proof 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
Proof state after:
case inl.inr.intro.h
p : ℤ
h : p ∣ 2 ^ 2
pp : Prime p
podd : Odd p
h0 : 4 = 2 ^ 2
⊢ Even p
Theorem: associated_of_dvd
Proof 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]
Proof state after:
case inl.inr.intro.h
p : ℤ
h : p ∣ 2 ^ 2
pp : Prime p
podd : Odd p
h0 : 4 = 2 ^ 2
⊢ 2 ∣ p
Theorem: associated_of_dvd
Proof 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 _
Proof state after:
p : ℤ
h : p ∣ 2 ^ 2
pp : Prime p
podd : Odd p
h0 : 4 = 2 ^ 2
⊢ Associated 2 p
Theorem: associated_of_dvd
Proof 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
Proof state after:
no goals
Theorem: associated_of_dvd
Proof state before:
p : ℤ
h : p ∣ 4
pp : Prime p
podd : Odd p
⊢ 4 = 2 ^ 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: associated_of_dvd
Proof state before:
case inr.intro.inl
a : ℤ
ap : Prime a
aodd : Odd a
h : 4 ∣ a
⊢ Associated 4 a
Tactic:
exfalso
Proof state after:
case inr.intro.inl.h
a : ℤ
ap : Prime a
aodd : Odd a
h : 4 ∣ a
⊢ False
Theorem: associated_of_dvd
Proof 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
Proof state after:
case inr.intro.inl.h
a : ℤ
ap : Prime a
aodd : ¬Even a
h : 4 ∣ a
⊢ False
Theorem: associated_of_dvd
Proof state before:
case inr.intro.inl.h
a : ℤ
ap : Prime a
aodd : ¬Even a
h : 4 ∣ a
⊢ False
Tactic:
refine' aodd _
Proof state after:
case inr.intro.inl.h
a : ℤ
ap : Prime a
aodd : ¬Even a
h : 4 ∣ a
⊢ Even a
Theorem: associated_of_dvd
Proof 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]
Proof state after:
case inr.intro.inl.h
a : ℤ
ap : Prime a
aodd : ¬Even a
h : 4 ∣ a
⊢ 2 ∣ a
Theorem: associated_of_dvd
Proof state before:
case inr.intro.inl.h
a : ℤ
ap : Prime a
aodd : ¬Even a
h : 4 ∣ a
⊢ 2 ∣ a
Tactic:
refine' dvd_trans _ h
Proof state after:
case inr.intro.inl.h
a : ℤ
ap : Prime a
aodd : ¬Even a
h : 4 ∣ a
⊢ 2 ∣ 4
Theorem: associated_of_dvd
Proof state before:
case inr.intro.inl.h
a : ℤ
ap : Prime a
aodd : ¬Even a
h : 4 ∣ a
⊢ 2 ∣ 4
Tactic:
norm_num
Proof state after:
no goals
Theorem: associated_of_dvd
Proof 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
Proof state after:
no goals
Theorem: dvd_or_dvd
Proof state before:
a p x : ℤ
ha : OddPrimeOrFour a
hp : OddPrimeOrFour p
hdvd : p ∣ a * x
⊢ p ∣ a ∨ p ∣ x
Tactic:
obtain rfl | ⟨pp, -⟩ := hp
Proof 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
Theorem: dvd_or_dvd
Proof state before:
case inl
a x : ℤ
ha : OddPrimeOrFour a
hdvd : 4 ∣ a * x
⊢ 4 ∣ a ∨ 4 ∣ x
Tactic:
obtain rfl | ⟨ap, aodd⟩ := ha
Proof 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
Theorem: dvd_or_dvd
Proof state before:
case inl.inl
x : ℤ
hdvd : 4 ∣ 4 * x
⊢ 4 ∣ 4 ∨ 4 ∣ x
Tactic:
exact Or.inl dvd_rfl
Proof state after:
no goals
Theorem: dvd_or_dvd
Proof state before:
case inl.inr.intro
a x : ℤ
hdvd : 4 ∣ a * x
ap : Prime a
aodd : Odd a
⊢ 4 ∣ a ∨ 4 ∣ x
Tactic:
right
Proof state after:
case inl.inr.intro.h
a x : ℤ
hdvd : 4 ∣ a * x
ap : Prime a
aodd : Odd a
⊢ 4 ∣ x
Theorem: dvd_or_dvd
Proof 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
Proof 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
Theorem: dvd_or_dvd
Proof 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⊢
Proof 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
Theorem: dvd_or_dvd
Proof 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
Proof state after:
a x : ℤ
hdvd : 2 ^ 2 ∣ a * x
ap : Prime a
aodd : Odd a
this : 4 = 2 ^ 2
⊢ ¬2 ∣ a
Theorem: dvd_or_dvd
Proof 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]
Proof state after:
no goals
Theorem: dvd_or_dvd
Proof state before:
a x : ℤ
hdvd : 4 ∣ a * x
ap : Prime a
aodd : Odd a
⊢ 4 = 2 ^ 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: dvd_or_dvd
Proof 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
Proof state after:
no goals
Theorem: exists_associated_mem_of_dvd_prod''
Proof state before:
p : ℤ
hp : OddPrimeOrFour p
s : Multiset ℤ
hs : ∀ (r : ℤ), r ∈ s → OddPrimeOrFour r
hdvd : p ∣ Multiset.prod s
⊢ ∃ q, q ∈ s ∧ Associated p q
Tactic:
induction' s using Multiset.induction_on with a s ih hs
Proof state after:
case h₁
p : ℤ
hp : OddPrimeOrFour p
s : Multiset ℤ
hs✝ : ∀ (r : ℤ), r ∈ s → OddPrimeOrFour r
hdvd✝ : p ∣ Multiset.prod s
hs : ∀ (r : ℤ), r ∈ 0 → OddPrimeOrFour r
hdvd : p ∣ Multiset.prod 0
⊢ ∃ q, q ∈ 0 ∧ Associated p q

case h₂
p : ℤ
hp : OddPrimeOrFour p
s✝ : Multiset ℤ
hs✝ : ∀ (r : ℤ), r ∈ s✝ → OddPrimeOrFour r
hdvd✝ : p ∣ Multiset.prod s✝
a : ℤ
s : Multiset ℤ
ih : (∀ (r : ℤ), r ∈ s → OddPrimeOrFour r) → p ∣ Multiset.prod s → ∃ q, q ∈ s ∧ Associated p q
hs : ∀ (r : ℤ), r ∈ a ::ₘ s → OddPrimeOrFour r
hdvd : p ∣ Multiset.prod (a ::ₘ s)
⊢ ∃ q, q ∈ a ::ₘ s ∧ Associated p q
Theorem: exists_associated_mem_of_dvd_prod''
Proof state before:
case h₁
p : ℤ
hp : OddPrimeOrFour p
s : Multiset ℤ
hs✝ : ∀ (r : ℤ), r ∈ s → OddPrimeOrFour r
hdvd✝ : p ∣ Multiset.prod s
hs : ∀ (r : ℤ), r ∈ 0 → OddPrimeOrFour r
hdvd : p ∣ Multiset.prod 0
⊢ ∃ q, q ∈ 0 ∧ Associated p q
Tactic:
simp [hp.not_unit, ← isUnit_iff_dvd_one] at hdvd
Proof state after:
no goals
Theorem: exists_associated_mem_of_dvd_prod''
Proof state before:
case h₂
p : ℤ
hp : OddPrimeOrFour p
s✝ : Multiset ℤ
hs✝ : ∀ (r : ℤ), r ∈ s✝ → OddPrimeOrFour r
hdvd✝ : p ∣ Multiset.prod s✝
a : ℤ
s : Multiset ℤ
ih : (∀ (r : ℤ), r ∈ s → OddPrimeOrFour r) → p ∣ Multiset.prod s → ∃ q, q ∈ s ∧ Associated p q
hs : ∀ (r : ℤ), r ∈ a ::ₘ s → OddPrimeOrFour r
hdvd : p ∣ Multiset.prod (a ::ₘ s)
⊢ ∃ q, q ∈ a ::ₘ s ∧ Associated p q
Tactic:
rw [Multiset.prod_cons] at hdvd
Proof state after:
case h₂
p : ℤ
hp : OddPrimeOrFour p
s✝ : Multiset ℤ
hs✝ : ∀ (r : ℤ), r ∈ s✝ → OddPrimeOrFour r
hdvd✝ : p ∣ Multiset.prod s✝
a : ℤ
s : Multiset ℤ
ih : (∀ (r : ℤ), r ∈ s → OddPrimeOrFour r) → p ∣ Multiset.prod s → ∃ q, q ∈ s ∧ Associated p q
hs : ∀ (r : ℤ), r ∈ a ::ₘ s → OddPrimeOrFour r
hdvd : p ∣ a * Multiset.prod s
⊢ ∃ q, q ∈ a ::ₘ s ∧ Associated p q
Theorem: exists_associated_mem_of_dvd_prod''
Proof state before:
case h₂
p : ℤ
hp : OddPrimeOrFour p
s✝ : Multiset ℤ
hs✝ : ∀ (r : ℤ), r ∈ s✝ → OddPrimeOrFour r
hdvd✝ : p ∣ Multiset.prod s✝
a : ℤ
s : Multiset ℤ
ih : (∀ (r : ℤ), r ∈ s → OddPrimeOrFour r) → p ∣ Multiset.prod s → ∃ q, q ∈ s ∧ Associated p q
hs : ∀ (r : ℤ), r ∈ a ::ₘ s → OddPrimeOrFour r
hdvd : p ∣ a * Multiset.prod s
⊢ ∃ q, q ∈ a ::ₘ s ∧ Associated p q
Tactic:
have := hs a (Multiset.mem_cons_self _ _)
Proof state after:
case h₂
p : ℤ
hp : OddPrimeOrFour p
s✝ : Multiset ℤ
hs✝ : ∀ (r : ℤ), r ∈ s✝ → OddPrimeOrFour r
hdvd✝ : p ∣ Multiset.prod s✝
a : ℤ
s : Multiset ℤ
ih : (∀ (r : ℤ), r ∈ s → OddPrimeOrFour r) → p ∣ Multiset.prod s → ∃ q, q ∈ s ∧ Associated p q
hs : ∀ (r : ℤ), r ∈ a ::ₘ s → OddPrimeOrFour r
hdvd : p ∣ a * Multiset.prod s
this : OddPrimeOrFour a
⊢ ∃ q, q ∈ a ::ₘ s ∧ Associated p q
Theorem: exists_associated_mem_of_dvd_prod''
Proof state before:
case h₂
p : ℤ
hp : OddPrimeOrFour p
s✝ : Multiset ℤ
hs✝ : ∀ (r : ℤ), r ∈ s✝ → OddPrimeOrFour r
hdvd✝ : p ∣ Multiset.prod s✝
a : ℤ
s : Multiset ℤ
ih : (∀ (r : ℤ), r ∈ s → OddPrimeOrFour r) → p ∣ Multiset.prod s → ∃ q, q ∈ s ∧ Associated p q
hs : ∀ (r : ℤ), r ∈ a ::ₘ s → OddPrimeOrFour r
hdvd : p ∣ a * Multiset.prod s
this : OddPrimeOrFour a
⊢ ∃ q, q ∈ a ::ₘ s ∧ Associated p q
Tactic:
obtain h | h := dvd_or_dvd this hp hdvd
Proof state after:
case h₂.inl
p : ℤ
hp : OddPrimeOrFour p
s✝ : Multiset ℤ
hs✝ : ∀ (r : ℤ), r ∈ s✝ → OddPrimeOrFour r
hdvd✝ : p ∣ Multiset.prod s✝
a : ℤ
s : Multiset ℤ
ih : (∀ (r : ℤ), r ∈ s → OddPrimeOrFour r) → p ∣ Multiset.prod s → ∃ q, q ∈ s ∧ Associated p q
hs : ∀ (r : ℤ), r ∈ a ::ₘ s → OddPrimeOrFour r
hdvd : p ∣ a * Multiset.prod s
this : OddPrimeOrFour a
h : p ∣ a
⊢ ∃ q, q ∈ a ::ₘ s ∧ Associated p q

case h₂.inr
p : ℤ
hp : OddPrimeOrFour p
s✝ : Multiset ℤ
hs✝ : ∀ (r : ℤ), r ∈ s✝ → OddPrimeOrFour r
hdvd✝ : p ∣ Multiset.prod s✝
a : ℤ
s : Multiset ℤ
ih : (∀ (r : ℤ), r ∈ s → OddPrimeOrFour r) → p ∣ Multiset.prod s → ∃ q, q ∈ s ∧ Associated p q
hs : ∀ (r : ℤ), r ∈ a ::ₘ s → OddPrimeOrFour r
hdvd : p ∣ a * Multiset.prod s
this : OddPrimeOrFour a
h : p ∣ Multiset.prod s
⊢ ∃ q, q ∈ a ::ₘ s ∧ Associated p q
Theorem: exists_associated_mem_of_dvd_prod''
Proof state before:
case h₂.inl
p : ℤ
hp : OddPrimeOrFour p
s✝ : Multiset ℤ
hs✝ : ∀ (r : ℤ), r ∈ s✝ → OddPrimeOrFour r
hdvd✝ : p ∣ Multiset.prod s✝
a : ℤ
s : Multiset ℤ
ih : (∀ (r : ℤ), r ∈ s → OddPrimeOrFour r) → p ∣ Multiset.prod s → ∃ q, q ∈ s ∧ Associated p q
hs : ∀ (r : ℤ), r ∈ a ::ₘ s → OddPrimeOrFour r
hdvd : p ∣ a * Multiset.prod s
this : OddPrimeOrFour a
h : p ∣ a
⊢ ∃ q, q ∈ a ::ₘ s ∧ Associated p q
Tactic:
exact ⟨a, Multiset.mem_cons_self _ _, associated_of_dvd this hp h⟩
Proof state after:
no goals
Theorem: exists_associated_mem_of_dvd_prod''
Proof state before:
case h₂.inr
p : ℤ
hp : OddPrimeOrFour p
s✝ : Multiset ℤ
hs✝ : ∀ (r : ℤ), r ∈ s✝ → OddPrimeOrFour r
hdvd✝ : p ∣ Multiset.prod s✝
a : ℤ
s : Multiset ℤ
ih : (∀ (r : ℤ), r ∈ s → OddPrimeOrFour r) → p ∣ Multiset.prod s → ∃ q, q ∈ s ∧ Associated p q
hs : ∀ (r : ℤ), r ∈ a ::ₘ s → OddPrimeOrFour r
hdvd : p ∣ a * Multiset.prod s
this : OddPrimeOrFour a
h : p ∣ Multiset.prod s
⊢ ∃ q, q ∈ a ::ₘ s ∧ Associated p q
Tactic:
obtain ⟨q, hq₁, hq₂⟩ := ih (fun r hr => hs _ (Multiset.mem_cons_of_mem hr)) h
Proof state after:
case h₂.inr.intro.intro
p : ℤ
hp : OddPrimeOrFour p
s✝ : Multiset ℤ
hs✝ : ∀ (r : ℤ), r ∈ s✝ → OddPrimeOrFour r
hdvd✝ : p ∣ Multiset.prod s✝
a : ℤ
s : Multiset ℤ
ih : (∀ (r : ℤ), r ∈ s → OddPrimeOrFour r) → p ∣ Multiset.prod s → ∃ q, q ∈ s ∧ Associated p q
hs : ∀ (r : ℤ), r ∈ a ::ₘ s → OddPrimeOrFour r
hdvd : p ∣ a * Multiset.prod s
this : OddPrimeOrFour a
h : p ∣ Multiset.prod s
q : ℤ
hq₁ : q ∈ s
hq₂ : Associated p q
⊢ ∃ q, q ∈ a ::ₘ s ∧ Associated p q
Theorem: exists_associated_mem_of_dvd_prod''
Proof state before:
case h₂.inr.intro.intro
p : ℤ
hp : OddPrimeOrFour p
s✝ : Multiset ℤ
hs✝ : ∀ (r : ℤ), r ∈ s✝ → OddPrimeOrFour r
hdvd✝ : p ∣ Multiset.prod s✝
a : ℤ
s : Multiset ℤ
ih : (∀ (r : ℤ), r ∈ s → OddPrimeOrFour r) → p ∣ Multiset.prod s → ∃ q, q ∈ s ∧ Associated p q
hs : ∀ (r : ℤ), r ∈ a ::ₘ s → OddPrimeOrFour r
hdvd : p ∣ a * Multiset.prod s
this : OddPrimeOrFour a
h : p ∣ Multiset.prod s
q : ℤ
hq₁ : q ∈ s
hq₂ : Associated p q
⊢ ∃ q, q ∈ a ::ₘ s ∧ Associated p q
Tactic:
exact ⟨q, Multiset.mem_cons_of_mem hq₁, hq₂⟩
Proof state after:
no goals
Theorem: factors_unique_prod'
Proof state before:
⊢ ∀ {f g : Multiset ℤ},
    (∀ (x : ℤ), x ∈ f → OddPrimeOrFour x) →
      (∀ (x : ℤ), x ∈ g → OddPrimeOrFour x) →
        Associated (Multiset.prod f) (Multiset.prod g) → Multiset.Rel Associated f g
Tactic:
intro f
Proof state after:
f : Multiset ℤ
⊢ ∀ {g : Multiset ℤ},
    (∀ (x : ℤ), x ∈ f → OddPrimeOrFour x) →
      (∀ (x : ℤ), x ∈ g → OddPrimeOrFour x) →
        Associated (Multiset.prod f) (Multiset.prod g) → Multiset.Rel Associated f g
Theorem: factors_unique_prod'
Proof state before:
f : Multiset ℤ
⊢ ∀ {g : Multiset ℤ},
    (∀ (x : ℤ), x ∈ f → OddPrimeOrFour x) →
      (∀ (x : ℤ), x ∈ g → OddPrimeOrFour x) →
        Associated (Multiset.prod f) (Multiset.prod g) → Multiset.Rel Associated f g
Tactic:
induction' f using Multiset.induction_on with p f ih
Proof state after:
case h₁

⊢ ∀ {g : Multiset ℤ},
    (∀ (x : ℤ), x ∈ 0 → OddPrimeOrFour x) →
      (∀ (x : ℤ), x ∈ g → OddPrimeOrFour x) →
        Associated (Multiset.prod 0) (Multiset.prod g) → Multiset.Rel Associated 0 g

case h₂
p : ℤ
f : Multiset ℤ
ih :
  ∀ {g : Multiset ℤ},
    (∀ (x : ℤ), x ∈ f → OddPrimeOrFour x) →
      (∀ (x : ℤ), x ∈ g → OddPrimeOrFour x) →
        Associated (Multiset.prod f) (Multiset.prod g) → Multiset.Rel Associated f g
⊢ ∀ {g : Multiset ℤ},
    (∀ (x : ℤ), x ∈ p ::ₘ f → OddPrimeOrFour x) →
      (∀ (x : ℤ), x ∈ g → OddPrimeOrFour x) →
        Associated (Multiset.prod (p ::ₘ f)) (Multiset.prod g) → Multiset.Rel Associated (p ::ₘ f) g
Theorem: factors_unique_prod'
Proof state before:
case h₁

⊢ ∀ {g : Multiset ℤ},
    (∀ (x : ℤ), x ∈ 0 → OddPrimeOrFour x) →
      (∀ (x : ℤ), x ∈ g → OddPrimeOrFour x) →
        Associated (Multiset.prod 0) (Multiset.prod g) → Multiset.Rel Associated 0 g
Tactic:
rintro g - hg h
Proof state after:
case h₁
g : Multiset ℤ
hg : ∀ (x : ℤ), x ∈ g → OddPrimeOrFour x
h : Associated (Multiset.prod 0) (Multiset.prod g)
⊢ Multiset.Rel Associated 0 g
Theorem: factors_unique_prod'
Proof state before:
case h₁
g : Multiset ℤ
hg : ∀ (x : ℤ), x ∈ g → OddPrimeOrFour x
h : Associated (Multiset.prod 0) (Multiset.prod g)
⊢ Multiset.Rel Associated 0 g
Tactic:
rw [Multiset.prod_zero] at h
Proof state after:
case h₁
g : Multiset ℤ
hg : ∀ (x : ℤ), x ∈ g → OddPrimeOrFour x
h : Associated 1 (Multiset.prod g)
⊢ Multiset.Rel Associated 0 g
Theorem: factors_unique_prod'
Proof state before:
case h₁
g : Multiset ℤ
hg : ∀ (x : ℤ), x ∈ g → OddPrimeOrFour x
h : Associated 1 (Multiset.prod g)
⊢ Multiset.Rel Associated 0 g
Tactic:
rw [Multiset.rel_zero_left]
Proof state after:
case h₁
g : Multiset ℤ
hg : ∀ (x : ℤ), x ∈ g → OddPrimeOrFour x
h : Associated 1 (Multiset.prod g)
⊢ g = 0
Theorem: factors_unique_prod'
Proof state before:
case h₁
g : Multiset ℤ
hg : ∀ (x : ℤ), x ∈ g → OddPrimeOrFour x
h : Associated 1 (Multiset.prod g)
⊢ g = 0
Tactic:
apply Multiset.eq_zero_of_forall_not_mem
Proof state after:
case h₁.a
g : Multiset ℤ
hg : ∀ (x : ℤ), x ∈ g → OddPrimeOrFour x
h : Associated 1 (Multiset.prod g)
⊢ ∀ (x : ℤ), ¬x ∈ g
Theorem: factors_unique_prod'
Proof state before:
case h₁.a
g : Multiset ℤ
hg : ∀ (x : ℤ), x ∈ g → OddPrimeOrFour x
h : Associated 1 (Multiset.prod g)
⊢ ∀ (x : ℤ), ¬x ∈ g
Tactic:
intro x hx
Proof state after:
case h₁.a
g : Multiset ℤ
hg : ∀ (x : ℤ), x ∈ g → OddPrimeOrFour x
h : Associated 1 (Multiset.prod g)
x : ℤ
hx : x ∈ g
⊢ False
Theorem: factors_unique_prod'
Proof state before:
case h₁.a
g : Multiset ℤ
hg : ∀ (x : ℤ), x ∈ g → OddPrimeOrFour x
h : Associated 1 (Multiset.prod g)
x : ℤ
hx : x ∈ g
⊢ False
Tactic:
apply (hg x hx).not_unit
Proof state after:
case h₁.a
g : Multiset ℤ
hg : ∀ (x : ℤ), x ∈ g → OddPrimeOrFour x
h : Associated 1 (Multiset.prod g)
x : ℤ
hx : x ∈ g
⊢ IsUnit x
Theorem: factors_unique_prod'
Proof state before:
case h₁.a
g : Multiset ℤ
hg : ∀ (x : ℤ), x ∈ g → OddPrimeOrFour x
h : Associated 1 (Multiset.prod g)
x : ℤ
hx : x ∈ g
⊢ IsUnit x
Tactic:
rw [isUnit_iff_dvd_one]
Proof state after:
case h₁.a
g : Multiset ℤ
hg : ∀ (x : ℤ), x ∈ g → OddPrimeOrFour x
h : Associated 1 (Multiset.prod g)
x : ℤ
hx : x ∈ g
⊢ x ∣ 1
Theorem: factors_unique_prod'
Proof state before:
case h₁.a
g : Multiset ℤ
hg : ∀ (x : ℤ), x ∈ g → OddPrimeOrFour x
h : Associated 1 (Multiset.prod g)
x : ℤ
hx : x ∈ g
⊢ x ∣ 1
Tactic:
exact dvd_trans (Multiset.dvd_prod hx) h.symm.dvd
Proof state after:
no goals
Theorem: factors_unique_prod'
Proof state before:
case h₂
p : ℤ
f : Multiset ℤ
ih :
  ∀ {g : Multiset ℤ},
    (∀ (x : ℤ), x ∈ f → OddPrimeOrFour x) →
      (∀ (x : ℤ), x ∈ g → OddPrimeOrFour x) →
        Associated (Multiset.prod f) (Multiset.prod g) → Multiset.Rel Associated f g
⊢ ∀ {g : Multiset ℤ},
    (∀ (x : ℤ), x ∈ p ::ₘ f → OddPrimeOrFour x) →
      (∀ (x : ℤ), x ∈ g → OddPrimeOrFour x) →
        Associated (Multiset.prod (p ::ₘ f)) (Multiset.prod g) → Multiset.Rel Associated (p ::ₘ f) g
Tactic:
intro g hf hg hfg
Proof state after:
case h₂
p : ℤ
f : Multiset ℤ
ih :
  ∀ {g : Multiset ℤ},
    (∀ (x : ℤ), x ∈ f → OddPrimeOrFour x) →
      (∀ (x : ℤ), x ∈ g → OddPrimeOrFour x) →
        Associated (Multiset.prod f) (Multiset.prod g) → Multiset.Rel Associated f g
g : Multiset ℤ
hf : ∀ (x : ℤ), x ∈ p ::ₘ f → OddPrimeOrFour x
hg : ∀ (x : ℤ), x ∈ g → OddPrimeOrFour x
hfg : Associated (Multiset.prod (p ::ₘ f)) (Multiset.prod g)
⊢ Multiset.Rel Associated (p ::ₘ f) g