internlm/Lean-Github huggingface dataset:
Theorem: FltRegular.caseI_easier
Proof state before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
hab : ¬a ≡ b [ZMOD ↑p]
caseI : ¬↑p ∣ a * b * c
hcycl : IsCyclotomicExtension {⟨p, ⋯⟩} ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ) := zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hζ : IsPrimitiveRoot (zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))) ↑⟨p, ⋯⟩
H : a ^ p + b ^ p = c ^ p
k₁ k₂ : Fin p
hcong : ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p]
hdiv :
  ↑p ∣
    ↑a + ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) - ↑a * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₁ -
      ↑b * zeta ⟨p, ⋯⟩ ℤ (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) ^ ↑k₂
key : ↑↑p ∣ ∑ i : Fin p, f a b ↑k₁ ↑k₂ ↑i • ζ ^ ↑i
⊢ (↑⟨p, ⋯⟩).Prime
Tactic:
exact hpri.out
Proof state after:
no goals
Theorem: OddPrimeOrFour.ne_zero
Proof state before:
z : ℕ
h : OddPrimeOrFour z
⊢ z ≠ 0
Tactic:
obtain rfl | ⟨h, -⟩ := h
Proof state after:
case inl

⊢ 4 ≠ 0

case inr.intro
z : ℕ
h : z.Prime
⊢ z ≠ 0
Theorem: OddPrimeOrFour.ne_zero
Proof state before:
case inl

⊢ 4 ≠ 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: OddPrimeOrFour.ne_zero
Proof state before:
case inr.intro
z : ℕ
h : z.Prime
⊢ z ≠ 0
Tactic:
exact h.ne_zero
Proof state after:
no goals
Theorem: OddPrimeOrFour.ne_one
Proof state before:
z : ℕ
h : OddPrimeOrFour z
⊢ z ≠ 1
Tactic:
obtain rfl | ⟨h, -⟩ := h
Proof state after:
case inl

⊢ 4 ≠ 1

case inr.intro
z : ℕ
h : z.Prime
⊢ z ≠ 1
Theorem: OddPrimeOrFour.ne_one
Proof state before:
case inl

⊢ 4 ≠ 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: OddPrimeOrFour.ne_one
Proof state before:
case inr.intro
z : ℕ
h : z.Prime
⊢ z ≠ 1
Tactic:
exact h.ne_one
Proof state after:
no goals
Theorem: OddPrimeOrFour.one_lt
Proof state before:
z : ℕ
h : OddPrimeOrFour z
⊢ 1 < z
Tactic:
obtain rfl | ⟨h, -⟩ := h
Proof state after:
case inl

⊢ 1 < 4

case inr.intro
z : ℕ
h : z.Prime
⊢ 1 < z
Theorem: OddPrimeOrFour.one_lt
Proof state before:
case inl

⊢ 1 < 4
Tactic:
norm_num
Proof state after:
no goals
Theorem: OddPrimeOrFour.one_lt
Proof state before:
case inr.intro
z : ℕ
h : z.Prime
⊢ 1 < z
Tactic:
exact h.one_lt
Proof state after:
no goals
Theorem: OddPrimeOrFour.not_unit
Proof state before:
z : ℕ
h : OddPrimeOrFour z
⊢ ¬IsUnit z
Tactic:
obtain rfl | ⟨h, -⟩ := h
Proof state after:
case inl

⊢ ¬IsUnit 4

case inr.intro
z : ℕ
h : z.Prime
⊢ ¬IsUnit z
Theorem: OddPrimeOrFour.not_unit
Proof state before:
case inl

⊢ ¬IsUnit 4
Tactic:
rw [isUnit_iff_dvd_one]
Proof state after:
case inl

⊢ ¬4 ∣ 1
Theorem: OddPrimeOrFour.not_unit
Proof state before:
case inl

⊢ ¬4 ∣ 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: OddPrimeOrFour.not_unit
Proof state before:
case inr.intro
z : ℕ
h : z.Prime
⊢ ¬IsUnit z
Tactic:
exact h.not_unit
Proof state after:
no goals
Theorem: OddPrimeOrFour.exists_and_dvd
Proof 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
Proof 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
Theorem: OddPrimeOrFour.exists_and_dvd
Proof state before:
case inl
n : ℕ
n2 : 2 < n
h4 : 4 ∣ n
⊢ ∃ p, p ∣ n ∧ OddPrimeOrFour p
Tactic:
exact ⟨4, h4, Or.inl rfl⟩
Proof state after:
no goals
Theorem: OddPrimeOrFour.exists_and_dvd
Proof 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⟩⟩
Proof state after:
no goals
Theorem: eq_of_dvd
Proof 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
Proof 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
Theorem: eq_of_dvd
Proof state before:
case inl.inl
h : 4 ∣ 4
⊢ 4 = 4
Tactic:
rfl
Proof state after:
no goals
Theorem: eq_of_dvd
Proof state before:
case inl.inr.intro
p : ℕ
h : p ∣ 4
pp : p.Prime
podd : Odd p
⊢ p = 4
Tactic:
exfalso
Proof state after:
case inl.inr.intro
p : ℕ
h : p ∣ 4
pp : p.Prime
podd : Odd p
⊢ False
Theorem: eq_of_dvd
Proof 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
Proof state after:
case inl.inr.intro
p : ℕ
h : p ∣ 4
pp : p.Prime
podd : Odd p
h0 : 4 = 2 ^ 2
⊢ False
Theorem: eq_of_dvd
Proof 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
Proof state after:
case inl.inr.intro
p : ℕ
h : p ∣ 2 ^ 2
pp : p.Prime
podd : Odd p
h0 : 4 = 2 ^ 2
⊢ False
Theorem: eq_of_dvd
Proof 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
Proof state after:
case inl.inr.intro
p : ℕ
h : p ∣ 2 ^ 2
pp : p.Prime
podd : Odd p
h0 : 4 = 2 ^ 2
⊢ Even p
Theorem: eq_of_dvd
Proof 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]
Proof state after:
case inl.inr.intro
p : ℕ
h : p ∣ 2 ^ 2
pp : p.Prime
podd : Odd p
h0 : 4 = 2 ^ 2
⊢ 2 ∣ p
Theorem: eq_of_dvd
Proof 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)
Proof state after:
no goals
Theorem: eq_of_dvd
Proof state before:
p : ℕ
h : p ∣ 4
pp : p.Prime
podd : Odd p
⊢ 4 = 2 ^ 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: eq_of_dvd
Proof state before:
case inr.intro.inl
a : ℕ
ap : a.Prime
aodd : Odd a
h : 4 ∣ a
⊢ 4 = a
Tactic:
exfalso
Proof state after:
case inr.intro.inl
a : ℕ
ap : a.Prime
aodd : Odd a
h : 4 ∣ a
⊢ False
Theorem: eq_of_dvd
Proof 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
Proof state after:
case inr.intro.inl
a : ℕ
ap : a.Prime
aodd : ¬Even a
h : 4 ∣ a
⊢ False
Theorem: eq_of_dvd
Proof state before:
case inr.intro.inl
a : ℕ
ap : a.Prime
aodd : ¬Even a
h : 4 ∣ a
⊢ False
Tactic:
refine' aodd _
Proof state after:
case inr.intro.inl
a : ℕ
ap : a.Prime
aodd : ¬Even a
h : 4 ∣ a
⊢ Even a
Theorem: eq_of_dvd
Proof state before:
case inr.intro.inl
a : ℕ
ap : a.Prime
aodd : ¬Even a
h : 4 ∣ a
⊢ Even a
Tactic:
rw [even_iff_two_dvd]
Proof state after:
case inr.intro.inl
a : ℕ
ap : a.Prime
aodd : ¬Even a
h : 4 ∣ a
⊢ 2 ∣ a
Theorem: eq_of_dvd
Proof state before:
case inr.intro.inl
a : ℕ
ap : a.Prime
aodd : ¬Even a
h : 4 ∣ a
⊢ 2 ∣ a
Tactic:
refine' dvd_trans _ h
Proof state after:
case inr.intro.inl
a : ℕ
ap : a.Prime
aodd : ¬Even a
h : 4 ∣ a
⊢ 2 ∣ 4
Theorem: eq_of_dvd
Proof state before:
case inr.intro.inl
a : ℕ
ap : a.Prime
aodd : ¬Even a
h : 4 ∣ a
⊢ 2 ∣ 4
Tactic:
norm_num
Proof state after:
no goals
Theorem: eq_of_dvd
Proof 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
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 : p.Prime
⊢ 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 : a.Prime
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 : a.Prime
aodd : Odd a
⊢ 4 ∣ a ∨ 4 ∣ x
Tactic:
right
Proof state after:
case inl.inr.intro.h
a x : ℕ
hdvd : 4 ∣ a * x
ap : a.Prime
aodd : Odd a
⊢ 4 ∣ x
Theorem: dvd_or_dvd
Proof state before:
case inl.inr.intro.h
a x : ℕ
hdvd : 4 ∣ a * x
ap : a.Prime
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 : a.Prime
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 : a.Prime
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 : a.Prime
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 : a.Prime
aodd : Odd a
this : 4 = 2 ^ 2
⊢ 2 ^ 2 ∣ x
Tactic:
apply Nat.prime_two.prime.pow_dvd_of_dvd_mul_left _ _ hdvd
Proof state after:
a x : ℕ
hdvd : 2 ^ 2 ∣ a * x
ap : a.Prime
aodd : Odd a
this : 4 = 2 ^ 2
⊢ ¬2 ∣ a
Theorem: dvd_or_dvd
Proof state before:
a x : ℕ
hdvd : 2 ^ 2 ∣ a * x
ap : a.Prime
aodd : Odd a
this : 4 = 2 ^ 2
⊢ ¬2 ∣ a
Tactic:
rwa [← even_iff_two_dvd, ← Nat.odd_iff_not_even]
Proof state after:
no goals
Theorem: dvd_or_dvd
Proof state before:
a x : ℕ
hdvd : 4 ∣ a * x
ap : a.Prime
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 : p.Prime
⊢ p ∣ a ∨ p ∣ x
Tactic:
exact pp.dvd_mul.mp hdvd
Proof state after:
no goals
Theorem: mem_of_dvd_prod
Proof state before:
p : ℕ
hp : OddPrimeOrFour p
s : Multiset ℕ
hs : ∀ r ∈ s, OddPrimeOrFour r
hdvd : p ∣ s.prod
⊢ p ∈ s
Tactic:
induction' s using Multiset.induction_on with a s ih hs
Proof state after:
case empty
p : ℕ
hp : OddPrimeOrFour p
hs : ∀ r ∈ 0, OddPrimeOrFour r
hdvd : p ∣ Multiset.prod 0
⊢ p ∈ 0

case cons
p : ℕ
hp : OddPrimeOrFour p
a : ℕ
s : Multiset ℕ
ih : (∀ r ∈ s, OddPrimeOrFour r) → p ∣ s.prod → p ∈ s
hs : ∀ r ∈ a ::ₘ s, OddPrimeOrFour r
hdvd : p ∣ (a ::ₘ s).prod
⊢ p ∈ a ::ₘ s
Theorem: mem_of_dvd_prod
Proof state before:
case empty
p : ℕ
hp : OddPrimeOrFour p
hs : ∀ r ∈ 0, OddPrimeOrFour r
hdvd : p ∣ Multiset.prod 0
⊢ p ∈ 0
Tactic:
simp [hp.ne_one] at hdvd
Proof state after:
no goals
Theorem: mem_of_dvd_prod
Proof state before:
case cons
p : ℕ
hp : OddPrimeOrFour p
a : ℕ
s : Multiset ℕ
ih : (∀ r ∈ s, OddPrimeOrFour r) → p ∣ s.prod → p ∈ s
hs : ∀ r ∈ a ::ₘ s, OddPrimeOrFour r
hdvd : p ∣ (a ::ₘ s).prod
⊢ p ∈ a ::ₘ s
Tactic:
rw [Multiset.prod_cons] at hdvd
Proof state after:
case cons
p : ℕ
hp : OddPrimeOrFour p
a : ℕ
s : Multiset ℕ
ih : (∀ r ∈ s, OddPrimeOrFour r) → p ∣ s.prod → p ∈ s
hs : ∀ r ∈ a ::ₘ s, OddPrimeOrFour r
hdvd : p ∣ a * s.prod
⊢ p ∈ a ::ₘ s
Theorem: mem_of_dvd_prod
Proof state before:
case cons
p : ℕ
hp : OddPrimeOrFour p
a : ℕ
s : Multiset ℕ
ih : (∀ r ∈ s, OddPrimeOrFour r) → p ∣ s.prod → p ∈ s
hs : ∀ r ∈ a ::ₘ s, OddPrimeOrFour r
hdvd : p ∣ a * s.prod
⊢ p ∈ a ::ₘ s
Tactic:
have := hs a (Multiset.mem_cons_self _ _)
Proof state after:
case cons
p : ℕ
hp : OddPrimeOrFour p
a : ℕ
s : Multiset ℕ
ih : (∀ r ∈ s, OddPrimeOrFour r) → p ∣ s.prod → p ∈ s
hs : ∀ r ∈ a ::ₘ s, OddPrimeOrFour r
hdvd : p ∣ a * s.prod
this : OddPrimeOrFour a
⊢ p ∈ a ::ₘ s
Theorem: mem_of_dvd_prod
Proof state before:
case cons
p : ℕ
hp : OddPrimeOrFour p
a : ℕ
s : Multiset ℕ
ih : (∀ r ∈ s, OddPrimeOrFour r) → p ∣ s.prod → p ∈ s
hs : ∀ r ∈ a ::ₘ s, OddPrimeOrFour r
hdvd : p ∣ a * s.prod
this : OddPrimeOrFour a
⊢ p ∈ a ::ₘ s
Tactic:
obtain h | h := dvd_or_dvd this hp hdvd
Proof state after:
case cons.inl
p : ℕ
hp : OddPrimeOrFour p
a : ℕ
s : Multiset ℕ
ih : (∀ r ∈ s, OddPrimeOrFour r) → p ∣ s.prod → p ∈ s
hs : ∀ r ∈ a ::ₘ s, OddPrimeOrFour r
hdvd : p ∣ a * s.prod
this : OddPrimeOrFour a
h : p ∣ a
⊢ p ∈ a ::ₘ s

case cons.inr
p : ℕ
hp : OddPrimeOrFour p
a : ℕ
s : Multiset ℕ
ih : (∀ r ∈ s, OddPrimeOrFour r) → p ∣ s.prod → p ∈ s
hs : ∀ r ∈ a ::ₘ s, OddPrimeOrFour r
hdvd : p ∣ a * s.prod
this : OddPrimeOrFour a
h : p ∣ s.prod
⊢ p ∈ a ::ₘ s
Theorem: mem_of_dvd_prod
Proof state before:
case cons.inl
p : ℕ
hp : OddPrimeOrFour p
a : ℕ
s : Multiset ℕ
ih : (∀ r ∈ s, OddPrimeOrFour r) → p ∣ s.prod → p ∈ s
hs : ∀ r ∈ a ::ₘ s, OddPrimeOrFour r
hdvd : p ∣ a * s.prod
this : OddPrimeOrFour a
h : p ∣ a
⊢ p ∈ a ::ₘ s
Tactic:
rw [eq_of_dvd this hp h]
Proof state after:
case cons.inl
p : ℕ
hp : OddPrimeOrFour p
a : ℕ
s : Multiset ℕ
ih : (∀ r ∈ s, OddPrimeOrFour r) → p ∣ s.prod → p ∈ s
hs : ∀ r ∈ a ::ₘ s, OddPrimeOrFour r
hdvd : p ∣ a * s.prod
this : OddPrimeOrFour a
h : p ∣ a
⊢ a ∈ a ::ₘ s
Theorem: mem_of_dvd_prod
Proof state before:
case cons.inl
p : ℕ
hp : OddPrimeOrFour p
a : ℕ
s : Multiset ℕ
ih : (∀ r ∈ s, OddPrimeOrFour r) → p ∣ s.prod → p ∈ s
hs : ∀ r ∈ a ::ₘ s, OddPrimeOrFour r
hdvd : p ∣ a * s.prod
this : OddPrimeOrFour a
h : p ∣ a
⊢ a ∈ a ::ₘ s
Tactic:
exact Multiset.mem_cons_self _ _
Proof state after:
no goals
Theorem: mem_of_dvd_prod
Proof state before:
case cons.inr
p : ℕ
hp : OddPrimeOrFour p
a : ℕ
s : Multiset ℕ
ih : (∀ r ∈ s, OddPrimeOrFour r) → p ∣ s.prod → p ∈ s
hs : ∀ r ∈ a ::ₘ s, OddPrimeOrFour r
hdvd : p ∣ a * s.prod
this : OddPrimeOrFour a
h : p ∣ s.prod
⊢ p ∈ a ::ₘ s
Tactic:
have := ih (fun r hr => hs _ (Multiset.mem_cons_of_mem hr)) h
Proof state after:
case cons.inr
p : ℕ
hp : OddPrimeOrFour p
a : ℕ
s : Multiset ℕ
ih : (∀ r ∈ s, OddPrimeOrFour r) → p ∣ s.prod → p ∈ s
hs : ∀ r ∈ a ::ₘ s, OddPrimeOrFour r
hdvd : p ∣ a * s.prod
this✝ : OddPrimeOrFour a
h : p ∣ s.prod
this : p ∈ s
⊢ p ∈ a ::ₘ s
Theorem: mem_of_dvd_prod
Proof state before:
case cons.inr
p : ℕ
hp : OddPrimeOrFour p
a : ℕ
s : Multiset ℕ
ih : (∀ r ∈ s, OddPrimeOrFour r) → p ∣ s.prod → p ∈ s
hs : ∀ r ∈ a ::ₘ s, OddPrimeOrFour r
hdvd : p ∣ a * s.prod
this✝ : OddPrimeOrFour a
h : p ∣ s.prod
this : p ∈ s
⊢ p ∈ a ::ₘ s
Tactic:
exact Multiset.mem_cons_of_mem this
Proof state after:
no goals
Theorem: factors_unique_prod'
Proof state before:
⊢ ∀ {f g : Multiset ℕ}, (∀ x ∈ f, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → f.prod = g.prod → f = g
Tactic:
intro f
Proof state after:
f : Multiset ℕ
⊢ ∀ {g : Multiset ℕ}, (∀ x ∈ f, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → f.prod = g.prod → f = g
Theorem: factors_unique_prod'
Proof state before:
f : Multiset ℕ
⊢ ∀ {g : Multiset ℕ}, (∀ x ∈ f, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → f.prod = g.prod → f = g
Tactic:
induction' f using Multiset.induction_on with p f ih
Proof state after:
case empty

⊢ ∀ {g : Multiset ℕ}, (∀ x ∈ 0, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → Multiset.prod 0 = g.prod → 0 = g

case cons
p : ℕ
f : Multiset ℕ
ih : ∀ {g : Multiset ℕ}, (∀ x ∈ f, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → f.prod = g.prod → f = g
⊢ ∀ {g : Multiset ℕ},
    (∀ x ∈ p ::ₘ f, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → (p ::ₘ f).prod = g.prod → p ::ₘ f = g
Theorem: factors_unique_prod'
Proof state before:
case empty

⊢ ∀ {g : Multiset ℕ}, (∀ x ∈ 0, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → Multiset.prod 0 = g.prod → 0 = g
Tactic:
rintro g - hg h
Proof state after:
case empty
g : Multiset ℕ
hg : ∀ x ∈ g, OddPrimeOrFour x
h : Multiset.prod 0 = g.prod
⊢ 0 = g
Theorem: factors_unique_prod'
Proof state before:
case empty
g : Multiset ℕ
hg : ∀ x ∈ g, OddPrimeOrFour x
h : Multiset.prod 0 = g.prod
⊢ 0 = g
Tactic:
rw [Multiset.prod_zero] at h
Proof state after:
case empty
g : Multiset ℕ
hg : ∀ x ∈ g, OddPrimeOrFour x
h : 1 = g.prod
⊢ 0 = g
Theorem: factors_unique_prod'
Proof state before:
case empty
g : Multiset ℕ
hg : ∀ x ∈ g, OddPrimeOrFour x
h : 1 = g.prod
⊢ 0 = g
Tactic:
symm
Proof state after:
case empty
g : Multiset ℕ
hg : ∀ x ∈ g, OddPrimeOrFour x
h : 1 = g.prod
⊢ g = 0
Theorem: factors_unique_prod'
Proof state before:
case empty
g : Multiset ℕ
hg : ∀ x ∈ g, OddPrimeOrFour x
h : 1 = g.prod
⊢ g = 0
Tactic:
apply Multiset.eq_zero_of_forall_not_mem
Proof state after:
case empty.a
g : Multiset ℕ
hg : ∀ x ∈ g, OddPrimeOrFour x
h : 1 = g.prod
⊢ ∀ (x : ℕ), x ∉ g
Theorem: factors_unique_prod'
Proof state before:
case empty.a
g : Multiset ℕ
hg : ∀ x ∈ g, OddPrimeOrFour x
h : 1 = g.prod
⊢ ∀ (x : ℕ), x ∉ g
Tactic:
intro x hx
Proof state after:
case empty.a
g : Multiset ℕ
hg : ∀ x ∈ g, OddPrimeOrFour x
h : 1 = g.prod
x : ℕ
hx : x ∈ g
⊢ False
Theorem: factors_unique_prod'
Proof state before:
case empty.a
g : Multiset ℕ
hg : ∀ x ∈ g, OddPrimeOrFour x
h : 1 = g.prod
x : ℕ
hx : x ∈ g
⊢ False
Tactic:
apply (hg x hx).not_unit
Proof state after:
case empty.a
g : Multiset ℕ
hg : ∀ x ∈ g, OddPrimeOrFour x
h : 1 = g.prod
x : ℕ
hx : x ∈ g
⊢ IsUnit x
Theorem: factors_unique_prod'
Proof state before:
case empty.a
g : Multiset ℕ
hg : ∀ x ∈ g, OddPrimeOrFour x
h : 1 = g.prod
x : ℕ
hx : x ∈ g
⊢ IsUnit x
Tactic:
rw [isUnit_iff_dvd_one]
Proof state after:
case empty.a
g : Multiset ℕ
hg : ∀ x ∈ g, OddPrimeOrFour x
h : 1 = g.prod
x : ℕ
hx : x ∈ g
⊢ x ∣ 1
Theorem: factors_unique_prod'
Proof state before:
case empty.a
g : Multiset ℕ
hg : ∀ x ∈ g, OddPrimeOrFour x
h : 1 = g.prod
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 cons
p : ℕ
f : Multiset ℕ
ih : ∀ {g : Multiset ℕ}, (∀ x ∈ f, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → f.prod = g.prod → f = g
⊢ ∀ {g : Multiset ℕ},
    (∀ x ∈ p ::ₘ f, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → (p ::ₘ f).prod = g.prod → p ::ₘ f = g
Tactic:
intro g hf hg hfg
Proof state after:
case cons
p : ℕ
f : Multiset ℕ
ih : ∀ {g : Multiset ℕ}, (∀ x ∈ f, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → f.prod = g.prod → f = g
g : Multiset ℕ
hf : ∀ x ∈ p ::ₘ f, OddPrimeOrFour x
hg : ∀ x ∈ g, OddPrimeOrFour x
hfg : (p ::ₘ f).prod = g.prod
⊢ p ::ₘ f = g
Theorem: factors_unique_prod'
Proof state before:
case cons
p : ℕ
f : Multiset ℕ
ih : ∀ {g : Multiset ℕ}, (∀ x ∈ f, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → f.prod = g.prod → f = g
g : Multiset ℕ
hf : ∀ x ∈ p ::ₘ f, OddPrimeOrFour x
hg : ∀ x ∈ g, OddPrimeOrFour x
hfg : (p ::ₘ f).prod = g.prod
⊢ p ::ₘ f = g
Tactic:
have hp := hf p (Multiset.mem_cons_self _ _)
Proof state after:
case cons
p : ℕ
f : Multiset ℕ
ih : ∀ {g : Multiset ℕ}, (∀ x ∈ f, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → f.prod = g.prod → f = g
g : Multiset ℕ
hf : ∀ x ∈ p ::ₘ f, OddPrimeOrFour x
hg : ∀ x ∈ g, OddPrimeOrFour x
hfg : (p ::ₘ f).prod = g.prod
hp : OddPrimeOrFour p
⊢ p ::ₘ f = g
Theorem: factors_unique_prod'
Proof state before:
case cons
p : ℕ
f : Multiset ℕ
ih : ∀ {g : Multiset ℕ}, (∀ x ∈ f, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → f.prod = g.prod → f = g
g : Multiset ℕ
hf : ∀ x ∈ p ::ₘ f, OddPrimeOrFour x
hg : ∀ x ∈ g, OddPrimeOrFour x
hfg : (p ::ₘ f).prod = g.prod
hp : OddPrimeOrFour p
⊢ p ::ₘ f = g
Tactic:
have hdvd : p ∣ g.prod :=
  by
  rw [← hfg, Multiset.prod_cons]
  exact dvd_mul_right _ _
Proof state after:
case cons
p : ℕ
f : Multiset ℕ
ih : ∀ {g : Multiset ℕ}, (∀ x ∈ f, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → f.prod = g.prod → f = g
g : Multiset ℕ
hf : ∀ x ∈ p ::ₘ f, OddPrimeOrFour x
hg : ∀ x ∈ g, OddPrimeOrFour x
hfg : (p ::ₘ f).prod = g.prod
hp : OddPrimeOrFour p
hdvd : p ∣ g.prod
⊢ p ::ₘ f = g
Theorem: factors_unique_prod'
Proof state before:
case cons
p : ℕ
f : Multiset ℕ
ih : ∀ {g : Multiset ℕ}, (∀ x ∈ f, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → f.prod = g.prod → f = g
g : Multiset ℕ
hf : ∀ x ∈ p ::ₘ f, OddPrimeOrFour x
hg : ∀ x ∈ g, OddPrimeOrFour x
hfg : (p ::ₘ f).prod = g.prod
hp : OddPrimeOrFour p
hdvd : p ∣ g.prod
⊢ p ::ₘ f = g
Tactic:
have hbg := mem_of_dvd_prod hp hg hdvd
Proof state after:
case cons
p : ℕ
f : Multiset ℕ
ih : ∀ {g : Multiset ℕ}, (∀ x ∈ f, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → f.prod = g.prod → f = g
g : Multiset ℕ
hf : ∀ x ∈ p ::ₘ f, OddPrimeOrFour x
hg : ∀ x ∈ g, OddPrimeOrFour x
hfg : (p ::ₘ f).prod = g.prod
hp : OddPrimeOrFour p
hdvd : p ∣ g.prod
hbg : p ∈ g
⊢ p ::ₘ f = g
Theorem: factors_unique_prod'
Proof state before:
case cons
p : ℕ
f : Multiset ℕ
ih : ∀ {g : Multiset ℕ}, (∀ x ∈ f, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → f.prod = g.prod → f = g
g : Multiset ℕ
hf : ∀ x ∈ p ::ₘ f, OddPrimeOrFour x
hg : ∀ x ∈ g, OddPrimeOrFour x
hfg : (p ::ₘ f).prod = g.prod
hp : OddPrimeOrFour p
hdvd : p ∣ g.prod
hbg : p ∈ g
⊢ p ::ₘ f = g
Tactic:
rw [← Multiset.cons_erase hbg]
Proof state after:
case cons
p : ℕ
f : Multiset ℕ
ih : ∀ {g : Multiset ℕ}, (∀ x ∈ f, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → f.prod = g.prod → f = g
g : Multiset ℕ
hf : ∀ x ∈ p ::ₘ f, OddPrimeOrFour x
hg : ∀ x ∈ g, OddPrimeOrFour x
hfg : (p ::ₘ f).prod = g.prod
hp : OddPrimeOrFour p
hdvd : p ∣ g.prod
hbg : p ∈ g
⊢ p ::ₘ f = p ::ₘ g.erase p
Theorem: factors_unique_prod'
Proof state before:
case cons
p : ℕ
f : Multiset ℕ
ih : ∀ {g : Multiset ℕ}, (∀ x ∈ f, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → f.prod = g.prod → f = g
g : Multiset ℕ
hf : ∀ x ∈ p ::ₘ f, OddPrimeOrFour x
hg : ∀ x ∈ g, OddPrimeOrFour x
hfg : (p ::ₘ f).prod = g.prod
hp : OddPrimeOrFour p
hdvd : p ∣ g.prod
hbg : p ∈ g
⊢ p ::ₘ f = p ::ₘ g.erase p
Tactic:
congr
Proof state after:
case cons.e_s
p : ℕ
f : Multiset ℕ
ih : ∀ {g : Multiset ℕ}, (∀ x ∈ f, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → f.prod = g.prod → f = g
g : Multiset ℕ
hf : ∀ x ∈ p ::ₘ f, OddPrimeOrFour x
hg : ∀ x ∈ g, OddPrimeOrFour x
hfg : (p ::ₘ f).prod = g.prod
hp : OddPrimeOrFour p
hdvd : p ∣ g.prod
hbg : p ∈ g
⊢ f = g.erase p
Theorem: factors_unique_prod'
Proof state before:
case cons.e_s
p : ℕ
f : Multiset ℕ
ih : ∀ {g : Multiset ℕ}, (∀ x ∈ f, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → f.prod = g.prod → f = g
g : Multiset ℕ
hf : ∀ x ∈ p ::ₘ f, OddPrimeOrFour x
hg : ∀ x ∈ g, OddPrimeOrFour x
hfg : (p ::ₘ f).prod = g.prod
hp : OddPrimeOrFour p
hdvd : p ∣ g.prod
hbg : p ∈ g
⊢ f = g.erase p
Tactic:
apply ih _ _ _
Proof state after:
p : ℕ
f : Multiset ℕ
ih : ∀ {g : Multiset ℕ}, (∀ x ∈ f, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → f.prod = g.prod → f = g
g : Multiset ℕ
hf : ∀ x ∈ p ::ₘ f, OddPrimeOrFour x
hg : ∀ x ∈ g, OddPrimeOrFour x
hfg : (p ::ₘ f).prod = g.prod
hp : OddPrimeOrFour p
hdvd : p ∣ g.prod
hbg : p ∈ g
⊢ ∀ x ∈ f, OddPrimeOrFour x

p : ℕ
f : Multiset ℕ
ih : ∀ {g : Multiset ℕ}, (∀ x ∈ f, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → f.prod = g.prod → f = g
g : Multiset ℕ
hf : ∀ x ∈ p ::ₘ f, OddPrimeOrFour x
hg : ∀ x ∈ g, OddPrimeOrFour x
hfg : (p ::ₘ f).prod = g.prod
hp : OddPrimeOrFour p
hdvd : p ∣ g.prod
hbg : p ∈ g
⊢ ∀ x ∈ g.erase p, OddPrimeOrFour x

p : ℕ
f : Multiset ℕ
ih : ∀ {g : Multiset ℕ}, (∀ x ∈ f, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → f.prod = g.prod → f = g
g : Multiset ℕ
hf : ∀ x ∈ p ::ₘ f, OddPrimeOrFour x
hg : ∀ x ∈ g, OddPrimeOrFour x
hfg : (p ::ₘ f).prod = g.prod
hp : OddPrimeOrFour p
hdvd : p ∣ g.prod
hbg : p ∈ g
⊢ f.prod = (g.erase p).prod
Theorem: factors_unique_prod'
Proof state before:
p : ℕ
f : Multiset ℕ
ih : ∀ {g : Multiset ℕ}, (∀ x ∈ f, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → f.prod = g.prod → f = g
g : Multiset ℕ
hf : ∀ x ∈ p ::ₘ f, OddPrimeOrFour x
hg : ∀ x ∈ g, OddPrimeOrFour x
hfg : (p ::ₘ f).prod = g.prod
hp : OddPrimeOrFour p
⊢ p ∣ g.prod
Tactic:
rw [← hfg, Multiset.prod_cons]
Proof state after:
p : ℕ
f : Multiset ℕ
ih : ∀ {g : Multiset ℕ}, (∀ x ∈ f, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → f.prod = g.prod → f = g
g : Multiset ℕ
hf : ∀ x ∈ p ::ₘ f, OddPrimeOrFour x
hg : ∀ x ∈ g, OddPrimeOrFour x
hfg : (p ::ₘ f).prod = g.prod
hp : OddPrimeOrFour p
⊢ p ∣ p * f.prod
Theorem: factors_unique_prod'
Proof state before:
p : ℕ
f : Multiset ℕ
ih : ∀ {g : Multiset ℕ}, (∀ x ∈ f, OddPrimeOrFour x) → (∀ x ∈ g, OddPrimeOrFour x) → f.prod = g.prod → f = g
g : Multiset ℕ
hf : ∀ x ∈ p ::ₘ f, OddPrimeOrFour x
hg : ∀ x ∈ g, OddPrimeOrFour x
hfg : (p ::ₘ f).prod = g.prod
hp : OddPrimeOrFour p
⊢ p ∣ p * f.prod
Tactic:
exact dvd_mul_right _ _
Proof state after:
no goals