awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d : ℕ
f : Fin d → ℕ
h : LT.lt (α := ℕ) 0 (∏ i : Fin d, f i)
right : Ne (α := ℕ) (∏ i : Fin d, f i) 0
i : Fin d
⊢ 0 < f i
have pos : f i ≠ 0
Tactic: apply Nat.pos_of_ne_zero
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (hypothesis)
Goal:
d n : ℕ
f : Fin d → ℕ
h : ¬0 < n
⊢ Membership.mem (γ := Finset (Fin d → ℕ)) ∅ f ↔ ∏ i : Fin d, f i = n ∧ n ≠ 0
have h₁ : n = 0
Tactic: simp only [not_lt, nonpos_iff_eq_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d : ℕ
⊢ d.finMulAntidiag 1 = {fun (x : Fin d) ↦ 1}
have h : ∀ (a : Fin d → ℕ), a ∈ d.finMulAntidiag 1 ↔ Membership.mem (γ := Finset (Fin d → ℕ)) {fun (x : Fin d) ↦ 1} a
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d : ℕ
a : Fin d → ℕ
⊢ a ∈ d.finMulAntidiag 1 ↔ Membership.mem (γ := Finset (Fin d → ℕ)) {fun (x : Fin d) ↦ 1} a
have h : (∀ (i : Fin d), a i = 1) ↔ a = fun (x : Fin d) ↦ 1
Tactic: simp only [mem_finMulAntidiag, prod_eq_one_iff, mem_univ, forall_const, ne_eq, one_ne_zero,
    not_false_eq_true, and_true, mem_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
n : ℕ
hn : n ≠ 1
⊢ Eq (α := Finset (Fin 0 → ℕ)) (finMulAntidiag 0 n) ∅
have h : ∀ (a : Fin 0 → ℕ),
  Membership.mem (γ := Finset (Fin 0 → ℕ)) (finMulAntidiag 0 n) a ↔ Membership.mem (γ := Finset (Fin 0 → ℕ)) ∅ a
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
n d : ℕ
f : Fin d → ℕ
hf : f ∈ d.finMulAntidiag n
i : Fin d
⊢ f i ∣ n
have rw : ∀ (hf : ∏ i : Fin d, f i = n ∧ n ≠ 0) (i : Fin d), f i ∣ n
Tactic: rw [mem_finMulAntidiag] at hf
Cleared hypotheses: hf, i
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
n d : ℕ
f : Fin d → ℕ
hf : ∏ i : Fin d, f i = n ∧ n ≠ 0
i : Fin d
⊢ f i ∣ n
have rw : f i ∣ ∏ i : Fin d, f i
Tactic: rw [← hf.1]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
⊢ d.finMulAntidiag m =
    {f ∈ Fintype.piFinset (δ := fun (x : Fin d) ↦ ℕ) fun (x : Fin d) ↦ n.divisors | ∏ i : Fin d, f i = m}
have h : ∀ (f : Fin d → ℕ),
  f ∈ d.finMulAntidiag m ↔
    Membership.mem (γ := Finset (Fin d → ℕ))
      ({f ∈ Fintype.piFinset (δ := fun (x : Fin d) ↦ ℕ) fun (x : Fin d) ↦ n.divisors | ∏ i : Fin d, f i = m}) f
Tactic: ext f
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
f : Fin d → ℕ
⊢ f ∈ d.finMulAntidiag m ↔
    Membership.mem (γ := Finset (Fin d → ℕ))
      ({f ∈ Fintype.piFinset (δ := fun (x : Fin d) ↦ ℕ) fun (x : Fin d) ↦ n.divisors | ∏ i : Fin d, f i = m}) f
have h : f ∈ d.finMulAntidiag m ↔ (∀ (a : Fin d), f a ∣ n ∧ ¬n = 0) ∧ ∏ i : Fin d, f i = m
Tactic: simp only [ne_eq,
    Fintype.mem_piFinset, mem_divisors, mem_filter]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
f : Fin d → ℕ
⊢ f ∈ d.finMulAntidiag m ↔ (∀ (a : Fin d), f a ∣ n ∧ ¬n = 0) ∧ ∏ i : Fin d, f i = m
have h : f ∈ d.finMulAntidiag m → (∀ (a : Fin d), f a ∣ n ∧ ¬n = 0) ∧ ∏ i : Fin d, f i = m
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
f : Fin d → ℕ
h : f ∈ d.finMulAntidiag m → (∀ (a : Fin d), f a ∣ n ∧ ¬n = 0) ∧ ∏ i : Fin d, f i = m
⊢ f ∈ d.finMulAntidiag m ↔ (∀ (a : Fin d), f a ∣ n ∧ ¬n = 0) ∧ ∏ i : Fin d, f i = m
have h₁ : (∀ (a : Fin d), f a ∣ n ∧ ¬n = 0) ∧ ∏ i : Fin d, f i = m → f ∈ d.finMulAntidiag m
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
f : Fin d → ℕ
hf : f ∈ d.finMulAntidiag m
⊢ (∀ (a : Fin d), f a ∣ n ∧ ¬n = 0) ∧ ∏ i : Fin d, f i = m
have h : ∀ (a : Fin d), f a ∣ n ∧ ¬n = 0
Tactic: refine ⟨?_, prod_eq_of_mem_finMulAntidiag hf⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
f : Fin d → ℕ
⊢ (∀ (a : Fin d), f a ∣ n ∧ ¬n = 0) ∧ ∏ i : Fin d, f i = m → f ∈ d.finMulAntidiag m
have h : (∀ (a : Fin d), f a ∣ n ∧ ¬n = 0) ∧ ∏ i : Fin d, f i = m → ∏ i : Fin d, f i = m ∧ m ≠ 0
Tactic: rw [mem_finMulAntidiag]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d n : ℕ
i : Fin d
hd : d ≠ 1
⊢ image (fun (f : Fin d → ℕ) ↦ f i) (d.finMulAntidiag n) = n.divisors
have h : ∀ (k : ℕ), Membership.mem (γ := Finset ℕ) (image (fun (f : Fin d → ℕ) ↦ f i) (d.finMulAntidiag n)) k ↔ k ∈ n.divisors
Tactic: ext k
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d n : ℕ
i : Fin d
hd : d ≠ 1
k : ℕ
⊢ Membership.mem (γ := Finset ℕ) (image (fun (f : Fin d → ℕ) ↦ f i) (d.finMulAntidiag n)) k ↔ k ∈ n.divisors
have h : (∃ a ∈ d.finMulAntidiag n, a i = k) ↔ k ∣ n ∧ ¬n = 0
Tactic: simp only [mem_image, ne_eq, mem_divisors]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d n : ℕ
i : Fin d
hd : d ≠ 1
k : ℕ
⊢ (∃ a ∈ d.finMulAntidiag n, a i = k) ↔ k ∣ n ∧ ¬n = 0
have h : (∃ a ∈ d.finMulAntidiag n, a i = k) → k ∣ n ∧ ¬n = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d n : ℕ
i : Fin d
hd : d ≠ 1
k : ℕ
h : (∃ a ∈ d.finMulAntidiag n, a i = k) → k ∣ n ∧ ¬n = 0
⊢ (∃ a ∈ d.finMulAntidiag n, a i = k) ↔ k ∣ n ∧ ¬n = 0
have h₁ : k ∣ n ∧ ¬n = 0 → ∃ a ∈ d.finMulAntidiag n, a i = k
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d n : ℕ
i : Fin d
hd : d ≠ 1
k : ℕ
⊢ k ∣ n ∧ ¬n = 0 → ∃ a ∈ d.finMulAntidiag n, a i = k
have h : k ∣ n ∧ ¬n = 0 → ∃ (a : Fin d → ℕ), (∏ i : Fin d, a i = n ∧ n ≠ 0) ∧ a i = k
Tactic: simp_rw [mem_finMulAntidiag]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
⊢ Nontrivial (Fin d)
have rw : 2 ≤ d
Tactic: rw [Fin.nontrivial_iff_two_le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
⊢ 2 ≤ d
have inl : ∀ {i : Fin 0} (hd : Ne (α := ℕ) 0 1), LE.le (α := ℕ) 2 0
Tactic: obtain rfl | hd' := eq_or_ne d 0
Cleared hypotheses: d, i, hd
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
inl : ∀ {i : Fin 0} (hd : Ne (α := ℕ) 0 1), LE.le (α := ℕ) 2 0
⊢ 2 ≤ d
have inr : ∀ (hd' : d ≠ 0), 2 ≤ d
Tactic: obtain rfl | hd' := eq_or_ne d 0
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (hypothesis)
Goal:
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
⊢ ∃ (a : Fin d → ℕ), (∏ i : Fin d, a i = k * r ∧ k * r ≠ 0) ∧ a i = k
have hs : Nontrivial (Fin d)
Tactic: have hs : Nontrivial (Fin d) := by
      rw [Fin.nontrivial_iff_two_le]
      obtain rfl | hd' := eq_or_ne d 0
      · exact i.elim0
      lia
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hs : Nontrivial (Fin d)
⊢ ∃ (a : Fin d → ℕ), (∏ i : Fin d, a i = k * r ∧ k * r ≠ 0) ∧ a i = k
have h : ∀ (i' : Fin d) (hi_ne : i' ≠ i), ∃ (a : Fin d → ℕ), (∏ i : Fin d, a i = k * r ∧ k * r ≠ 0) ∧ a i = k
Tactic: obtain ⟨i', hi_ne⟩ := exists_ne i
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hs : Nontrivial (Fin d)
i' : Fin d
hi_ne : i' ≠ i
⊢ ∃ (a : Fin d → ℕ), (∏ i : Fin d, a i = k * r ∧ k * r ≠ 0) ∧ a i = k
have h : (∏ i_1 : Fin d, (fun (j : Fin d) ↦ if j = i then k else if j = i' then r else 1) i_1 = k * r ∧ k * r ≠ 0) ∧
  (fun (j : Fin d) ↦ if j = i then k else if j = i' then r else 1) i = k
Tactic: use fun j => if j = i then k else if j = i' then r else 1
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hs : Nontrivial (Fin d)
i' : Fin d
hi_ne : i' ≠ i
⊢ (∏ i_1 : Fin d, (fun (j : Fin d) ↦ if j = i then k else if j = i' then r else 1) i_1 = k * r ∧ k * r ≠ 0) ∧
    (fun (j : Fin d) ↦ if j = i then k else if j = i' then r else 1) i = k
have h : (∏ x : Fin d, if x = i then k else if x = i' then r else 1) = k * r ∧ k * r ≠ 0
Tactic: simp only [ite_true, and_true]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hs : Nontrivial (Fin d)
i' : Fin d
hi_ne : i' ≠ i
⊢ (∏ x : Fin d, if x = i then k else if x = i' then r else 1) = k * r ∧ k * r ≠ 0
have h : (if i = i then k else if i = i' then r else 1) *
      ((if i' = i then k else if i' = i' then r else 1) *
        ∏ x ∈ (erase univ i).erase i', if x = i then k else if x = i' then r else 1) =
    k * r ∧
  k * r ≠ 0
Tactic: rw [← Finset.mul_prod_erase (h := mem_univ i),
      ← Finset.mul_prod_erase (a := i')]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hs : Nontrivial (Fin d)
i' : Fin d
hi_ne : i' ≠ i
h :
  (if i = i then k else if i = i' then r else 1) *
        ((if i' = i then k else if i' = i' then r else 1) *
          ∏ x ∈ (erase univ i).erase i', if x = i then k else if x = i' then r else 1) =
      k * r ∧
    k * r ≠ 0
⊢ (∏ x : Fin d, if x = i then k else if x = i' then r else 1) = k * r ∧ k * r ≠ 0
have h₁ : i' ∈ erase univ i
Tactic: rw [← Finset.mul_prod_erase (h := mem_univ i),
      ← Finset.mul_prod_erase (a := i')]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
n : ℕ
⊢ image (α := (i : Fin 2) → ℕ) (⇑(piFinTwoEquiv fun (x : Fin 2) ↦ ℕ) : (a : (i : Fin 2) → ℕ) → ℕ × ℕ)
      (finMulAntidiag 2 n) =
    n.divisorsAntidiagonal
have h : ∀ (x : ℕ × ℕ),
  Membership.mem (γ := Finset (ℕ × ℕ))
      (image (α := (i : Fin 2) → ℕ) (⇑(piFinTwoEquiv fun (x : Fin 2) ↦ ℕ) : (a : (i : Fin 2) → ℕ) → ℕ × ℕ)
        (finMulAntidiag 2 n))
      x ↔
    x ∈ n.divisorsAntidiagonal
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (hypothesis)
Goal:
d n p : ℕ
hn : Squarefree n
hp : p ∈ n.primeFactorsList
f : Fin d → ℕ
hf : f ∈ d.finMulAntidiag n
⊢ ∃! i : Fin d, p ∣ f i
have hf₁ : ∏ i : Fin d, f i = n ∧ n ≠ 0
Tactic: rw [mem_finMulAntidiag] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d n p : ℕ
hn : Squarefree n
hp : p ∈ n.primeFactorsList
f : Fin d → ℕ
hf : ∏ i : Fin d, f i = n ∧ n ≠ 0
⊢ ∃! i : Fin d, p ∣ f i
have rw : ∀ (f : Fin d → ℕ) (hp : Prime p ∧ ∃ (a : Fin d), Membership.mem (γ := Finset (Fin d)) univ a ∧ p ∣ f a)
  (hf : ∏ i : Fin d, f i = n ∧ n ≠ 0), ∃! i : Fin d, p ∣ f i
Tactic: rw [mem_primeFactorsList hf.2, ← hf.1, hp.1.prime.dvd_finsetProd_iff] at hp
Cleared hypotheses: hp, f, hf
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d n p : ℕ
hn : Squarefree n
f : Fin d → ℕ
hp : Prime p ∧ ∃ (a : Fin d), Membership.mem (γ := Finset (Fin d)) univ a ∧ p ∣ f a
hf : ∏ i : Fin d, f i = n ∧ n ≠ 0
⊢ ∃! i : Fin d, p ∣ f i
have obtain : ∀ (i : Fin d) (his : Membership.mem (γ := Finset (Fin d)) univ i) (hi : p ∣ f i), ∃! i : Fin d, p ∣ f i
Tactic: obtain ⟨i, his, hi⟩ := hp.2
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d n p : ℕ
hn : Squarefree n
f : Fin d → ℕ
hp : Prime p ∧ ∃ (a : Fin d), Membership.mem (γ := Finset (Fin d)) univ a ∧ p ∣ f a
hf : ∏ i : Fin d, f i = n ∧ n ≠ 0
i : Fin d
his : Membership.mem (γ := Finset (Fin d)) univ i
hi : p ∣ f i
⊢ ∃! i : Fin d, p ∣ f i
have refine : ∀ (y : Fin d), (fun (i : Fin d) ↦ p ∣ f i) y → y = i
Tactic: refine ⟨i, hi, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d n p : ℕ
hn : Squarefree n
f : Fin d → ℕ
hp : Prime p ∧ ∃ (a : Fin d), Membership.mem (γ := Finset (Fin d)) univ a ∧ p ∣ f a
hf : ∏ i : Fin d, f i = n ∧ n ≠ 0
i : Fin d
his : Membership.mem (γ := Finset (Fin d)) univ i
hi : p ∣ f i
j : Fin d
hj : p ∣ f j
⊢ j = i
have by_contra : ∀ (hij : ¬j = i), False
Tactic: by_contra hij
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d n p : ℕ
hn : Squarefree n
f : Fin d → ℕ
hp : Prime p ∧ ∃ (a : Fin d), Membership.mem (γ := Finset (Fin d)) univ a ∧ p ∣ f a
hf : ∏ i : Fin d, f i = n ∧ n ≠ 0
i : Fin d
his : Membership.mem (γ := Finset (Fin d)) univ i
hi : p ∣ f i
j : Fin d
hj : p ∣ f j
hij : ¬j = i
⊢ False
have apply : (f i).Coprime (f j)
Tactic: apply Nat.Prime.not_coprime_iff_dvd.mpr ⟨p, hp.1, hi, hj⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d n p : ℕ
hn : Squarefree n
f : Fin d → ℕ
hp : Prime p ∧ ∃ (a : Fin d), Membership.mem (γ := Finset (Fin d)) univ a ∧ p ∣ f a
hf : ∏ i : Fin d, f i = n ∧ n ≠ 0
i : Fin d
his : Membership.mem (γ := Finset (Fin d)) univ i
hi : p ∣ f i
j : Fin d
hj : p ∣ f j
hij : ¬j = i
⊢ (f i).Coprime (f j)
have h : Squarefree (f i * f j)
Tactic: apply Nat.coprime_of_squarefree_mul
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d n p : ℕ
hn : Squarefree n
f : Fin d → ℕ
hp : Prime p ∧ ∃ (a : Fin d), Membership.mem (γ := Finset (Fin d)) univ a ∧ p ∣ f a
hf : ∏ i : Fin d, f i = n ∧ n ≠ 0
i : Fin d
his : Membership.mem (γ := Finset (Fin d)) univ i
hi : p ∣ f i
j : Fin d
hj : p ∣ f j
hij : ¬j = i
⊢ Squarefree (f i * f j)
have h : f i * f j ∣ n
Tactic: apply hn.squarefree_of_dvd
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d n p : ℕ
hn : Squarefree n
f : Fin d → ℕ
hp : Prime p ∧ ∃ (a : Fin d), Membership.mem (γ := Finset (Fin d)) univ a ∧ p ∣ f a
hf : ∏ i : Fin d, f i = n ∧ n ≠ 0
i : Fin d
his : Membership.mem (γ := Finset (Fin d)) univ i
hi : p ∣ f i
j : Fin d
hj : p ∣ f j
hij : ¬j = i
⊢ f i * f j ∣ n
have h : f i * f j ∣ f i * f j * ∏ x ∈ (erase univ i).erase j, f x
Tactic: rw [← hf.1, ← Finset.mul_prod_erase _ _ his,
    ← Finset.mul_prod_erase _ _ (mem_erase.mpr ⟨hij, mem_univ _⟩), ← mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d n : ℕ
hn : Squarefree n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf :
  Membership.mem (γ := Finset ((a : ℕ) → a ∈ n.primeFactors → Fin d))
    (n.primeFactors.pi (β := fun (p : ℕ) ↦ Fin d) fun (x : ℕ) ↦ univ) f
⊢ d.primeFactorsPiBij n f hf ∈ d.finMulAntidiag n
have rw : ∏ i : Fin d, d.primeFactorsPiBij n f hf i = n ∧ n ≠ 0
Tactic: rw [mem_finMulAntidiag]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d n : ℕ
hn : Squarefree n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf :
  Membership.mem (γ := Finset ((a : ℕ) → a ∈ n.primeFactors → Fin d))
    (n.primeFactors.pi (β := fun (p : ℕ) ↦ Fin d) fun (x : ℕ) ↦ univ) f
⊢ ∏ i : Fin d, d.primeFactorsPiBij n f hf i = n ∧ n ≠ 0
have refine : ∏ i : Fin d, d.primeFactorsPiBij n f hf i = n
Tactic: refine ⟨?_, hn.ne_zero⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d n : ℕ
hn : Squarefree n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf :
  Membership.mem (γ := Finset ((a : ℕ) → a ∈ n.primeFactors → Fin d))
    (n.primeFactors.pi (β := fun (p : ℕ) ↦ Fin d) fun (x : ℕ) ↦ univ) f
⊢ ∏ i : Fin d, ∏ p ∈ n.primeFactors.attach with f (↑p : ℕ) ⋯ = i, (↑p : ℕ) = n
have rw : ∏ x ∈ n.primeFactors, x = n
Tactic: rw [prod_fiberwise_of_maps_to, prod_attach (f := fun x => x)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d n : ℕ
hn : Squarefree n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf :
  Membership.mem (γ := Finset ((a : ℕ) → a ∈ n.primeFactors → Fin d))
    (n.primeFactors.pi (β := fun (p : ℕ) ↦ Fin d) fun (x : ℕ) ↦ univ) f
rw : ∏ x ∈ n.primeFactors, x = n
⊢ ∏ i : Fin d, ∏ p ∈ n.primeFactors.attach with f (↑p : ℕ) ⋯ = i, (↑p : ℕ) = n
have h : ∀ i ∈ n.primeFactors.attach, Membership.mem (γ := Finset (Fin d)) univ (f (↑i : ℕ) sorry)
Tactic: rw [prod_fiberwise_of_maps_to, prod_attach (f := fun x => x)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf :
  Membership.mem (γ := Finset ((a : ℕ) → a ∈ n.primeFactors → Fin d))
    (n.primeFactors.pi (β := fun (p : ℕ) ↦ Fin d) fun (x : ℕ) ↦ univ) f
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg :
  Membership.mem (γ := Finset ((a : ℕ) → a ∈ n.primeFactors → Fin d))
    (n.primeFactors.pi (β := fun (p : ℕ) ↦ Fin d) fun (x : ℕ) ↦ univ) g
⊢ d.primeFactorsPiBij n f hf = d.primeFactorsPiBij n g hg → f = g
have contrapose! : f ≠ g → d.primeFactorsPiBij n f hf ≠ d.primeFactorsPiBij n g hg
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf :
  Membership.mem (γ := Finset ((a : ℕ) → a ∈ n.primeFactors → Fin d))
    (n.primeFactors.pi (β := fun (p : ℕ) ↦ Fin d) fun (x : ℕ) ↦ univ) f
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg :
  Membership.mem (γ := Finset ((a : ℕ) → a ∈ n.primeFactors → Fin d))
    (n.primeFactors.pi (β := fun (p : ℕ) ↦ Fin d) fun (x : ℕ) ↦ univ) g
⊢ f ≠ g → d.primeFactorsPiBij n f hf ≠ d.primeFactorsPiBij n g hg
have simp_rw : (∃ (a : ℕ) (a_1 : a ∈ n.primeFactors), f a a_1 ≠ g a a_1) →
  ∃ (a : Fin d), d.primeFactorsPiBij n f hf a ≠ d.primeFactorsPiBij n g hg a
Tactic: simp_rw [Function.ne_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf :
  Membership.mem (γ := Finset ((a : ℕ) → a ∈ n.primeFactors → Fin d))
    (n.primeFactors.pi (β := fun (p : ℕ) ↦ Fin d) fun (x : ℕ) ↦ univ) f
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg :
  Membership.mem (γ := Finset ((a : ℕ) → a ∈ n.primeFactors → Fin d))
    (n.primeFactors.pi (β := fun (p : ℕ) ↦ Fin d) fun (x : ℕ) ↦ univ) g
p : ℕ
hp : p ∈ n.primeFactors
hfg : f p hp ≠ g p hp
⊢ ∃ (a : Fin d), d.primeFactorsPiBij n f hf a ≠ d.primeFactorsPiBij n g hg a
have h : d.primeFactorsPiBij n f hf (f p hp) ≠ d.primeFactorsPiBij n g hg (f p hp)
Tactic: use f p hp
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf :
  Membership.mem (γ := Finset ((a : ℕ) → a ∈ n.primeFactors → Fin d))
    (n.primeFactors.pi (β := fun (p : ℕ) ↦ Fin d) fun (x : ℕ) ↦ univ) f
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg :
  Membership.mem (γ := Finset ((a : ℕ) → a ∈ n.primeFactors → Fin d))
    (n.primeFactors.pi (β := fun (p : ℕ) ↦ Fin d) fun (x : ℕ) ↦ univ) g
p : ℕ
hp : p ∈ n.primeFactors
hfg : f p hp ≠ g p hp
⊢ Ne (α := ℕ) (∏ p ∈ n.primeFactors.attach with f (↑p : ℕ) ⋯ = f p hp, (↑p : ℕ))
    (∏ p ∈ n.primeFactors.attach with g (↑p : ℕ) ⋯ = f p hp, (↑p : ℕ))
have h : Membership.mem (γ := Set ℕ) {x : ℕ | p ∣ x} (∏ p ∈ n.primeFactors.attach with f (↑p : ℕ) sorry = f p hp, (↑p : ℕ))
Tactic: apply ne_of_mem_of_not_mem (s := {x | p ∣ x})
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf :
  Membership.mem (γ := Finset ((a : ℕ) → a ∈ n.primeFactors → Fin d))
    (n.primeFactors.pi (β := fun (p : ℕ) ↦ Fin d) fun (x : ℕ) ↦ univ) f
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg :
  Membership.mem (γ := Finset ((a : ℕ) → a ∈ n.primeFactors → Fin d))
    (n.primeFactors.pi (β := fun (p : ℕ) ↦ Fin d) fun (x : ℕ) ↦ univ) g
p : ℕ
hp : p ∈ n.primeFactors
hfg : f p hp ≠ g p hp
h : Membership.mem (γ := Set ℕ) {x : ℕ | p ∣ x} (∏ p ∈ n.primeFactors.attach with f (↑p : ℕ) ⋯ = f p hp, (↑p : ℕ))
⊢ Ne (α := ℕ) (∏ p ∈ n.primeFactors.attach with f (↑p : ℕ) ⋯ = f p hp, (↑p : ℕ))
    (∏ p ∈ n.primeFactors.attach with g (↑p : ℕ) ⋯ = f p hp, (↑p : ℕ))
have h₁ : ∏ p ∈ n.primeFactors.attach with g (↑p : ℕ) sorry = f p hp, (↑p : ℕ) ∉ {x : ℕ | p ∣ x}
Tactic: apply ne_of_mem_of_not_mem (s := {x | p ∣ x})
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf :
  Membership.mem (γ := Finset ((a : ℕ) → a ∈ n.primeFactors → Fin d))
    (n.primeFactors.pi (β := fun (p : ℕ) ↦ Fin d) fun (x : ℕ) ↦ univ) f
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg :
  Membership.mem (γ := Finset ((a : ℕ) → a ∈ n.primeFactors → Fin d))
    (n.primeFactors.pi (β := fun (p : ℕ) ↦ Fin d) fun (x : ℕ) ↦ univ) g
p : ℕ
hp : p ∈ n.primeFactors
hfg : f p hp ≠ g p hp
⊢ p ∣ ∏ p ∈ n.primeFactors.attach with f (↑p : ℕ) ⋯ = f p hp, (↑p : ℕ)
have h : p ∣ ∏ a ∈ n.primeFactors.attach, if f (↑a : ℕ) sorry = f p hp then (↑a : ℕ) else 1
Tactic: rw [Finset.prod_filter]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf :
  Membership.mem (γ := Finset ((a : ℕ) → a ∈ n.primeFactors → Fin d))
    (n.primeFactors.pi (β := fun (p : ℕ) ↦ Fin d) fun (x : ℕ) ↦ univ) f
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg :
  Membership.mem (γ := Finset ((a : ℕ) → a ∈ n.primeFactors → Fin d))
    (n.primeFactors.pi (β := fun (p : ℕ) ↦ Fin d) fun (x : ℕ) ↦ univ) g
p : ℕ
hp : p ∈ n.primeFactors
hfg : f p hp ≠ g p hp
⊢ p ∣ ∏ a ∈ n.primeFactors.attach, if f (↑a : ℕ) ⋯ = f p hp then (↑a : ℕ) else 1
have h : p =
  if f (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ n.primeFactors) p hp) : ℕ) sorry = f p hp then
    (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ n.primeFactors) p hp) : ℕ)
  else 1
Tactic: convert! Finset.dvd_prod_of_mem _ (mem_attach (n.primeFactors) ⟨p, hp⟩)
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf :
  Membership.mem (γ := Finset ((a : ℕ) → a ∈ n.primeFactors → Fin d))
    (n.primeFactors.pi (β := fun (p : ℕ) ↦ Fin d) fun (x : ℕ) ↦ univ) f
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg :
  Membership.mem (γ := Finset ((a : ℕ) → a ∈ n.primeFactors → Fin d))
    (n.primeFactors.pi (β := fun (p : ℕ) ↦ Fin d) fun (x : ℕ) ↦ univ) g
p : ℕ
hp : p ∈ n.primeFactors
hfg : f p hp ≠ g p hp
⊢ p =
    if f (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ n.primeFactors) p hp) : ℕ) ⋯ = f p hp then
      (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ n.primeFactors) p hp) : ℕ)
    else 1
have h : p = (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ n.primeFactors) p hp) : ℕ)
Tactic: rw [if_pos rfl]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (hypothesis)
Goal:
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf :
  Membership.mem (γ := Finset ((a : ℕ) → a ∈ n.primeFactors → Fin d))
    (n.primeFactors.pi (β := fun (p : ℕ) ↦ Fin d) fun (x : ℕ) ↦ univ) f
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg :
  Membership.mem (γ := Finset ((a : ℕ) → a ∈ n.primeFactors → Fin d))
    (n.primeFactors.pi (β := fun (p : ℕ) ↦ Fin d) fun (x : ℕ) ↦ univ) g
p : ℕ
hp : p ∈ n.primeFactors
hfg : f p hp ≠ g p hp
⊢ ¬p ∣ ∏ p ∈ n.primeFactors.attach with g (↑p : ℕ) ⋯ = f p hp, (↑p : ℕ)
have hp₁ : Prime p ∧ p ∣ n ∧ n ≠ 0
Tactic: rw [mem_primeFactors] at hp
Cleared hypotheses: hfg
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf :
  Membership.mem (γ := Finset ((a : ℕ) → a ∈ n.primeFactors → Fin d))
    (n.primeFactors.pi (β := fun (p : ℕ) ↦ Fin d) fun (x : ℕ) ↦ univ) f
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg :
  Membership.mem (γ := Finset ((a : ℕ) → a ∈ n.primeFactors → Fin d))
    (n.primeFactors.pi (β := fun (p : ℕ) ↦ Fin d) fun (x : ℕ) ↦ univ) g
p : ℕ
hp_1 : p ∈ n.primeFactors
hp : Prime p ∧ p ∣ n ∧ n ≠ 0
hfg : f p hp_1 ≠ g p hp_1
⊢ ¬p ∣ ∏ p ∈ n.primeFactors.attach with g (↑p : ℕ) ⋯ = f p hp_1, (↑p : ℕ)
have h : ¬∃ a ∈ {p_1 ∈ n.primeFactors.attach | g (↑p_1 : ℕ) sorry = f p hp_1}, p ∣ (↑a : ℕ)
Tactic: rw [Prime.dvd_finsetProd_iff hp.1.prime]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf :
  Membership.mem (γ := Finset ((a : ℕ) → a ∈ n.primeFactors → Fin d))
    (n.primeFactors.pi (β := fun (p : ℕ) ↦ Fin d) fun (x : ℕ) ↦ univ) f
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg :
  Membership.mem (γ := Finset ((a : ℕ) → a ∈ n.primeFactors → Fin d))
    (n.primeFactors.pi (β := fun (p : ℕ) ↦ Fin d) fun (x : ℕ) ↦ univ) g
p : ℕ
hp_1 : p ∈ n.primeFactors
hp : Prime p ∧ p ∣ n ∧ n ≠ 0
hfg : f p hp_1 ≠ g p hp_1
⊢ ¬∃ a ∈ {p_1 ∈ n.primeFactors.attach | g (↑p_1 : ℕ) ⋯ = f p hp_1}, p ∣ (↑a : ℕ)
have h : ∀ (a : ↥n.primeFactors) (_ : a ∈ {p_1 ∈ n.primeFactors.attach | g (↑p_1 : ℕ) sorry = f p hp_1}), ¬p ∣ (↑a : ℕ)
Tactic: push Not