awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
Goal:
d n : ℕ
i : Fin d
hd : d ≠ 1
f : Fin d → ℕ
hf : f ∈ d.finMulAntidiag n
⊢ f i ∣ n ∧ ¬n = 0

Tactic:
⟨dvd_of_mem_finMulAntidiag hf _, (mem_finMulAntidiag.mp hf).2⟩

Premises used: Nat.mem_finMulAntidiag, Nat.dvd_of_mem_finMulAntidiag, And.right, And.intro, Iff.mp
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
Goal:
d n : ℕ
i : Fin d
hd : d ≠ 1
f : Fin d → ℕ
hf : f ∈ d.finMulAntidiag n
⊢ f i ∣ n ∧ ¬n = 0

Tactic:
exact ⟨dvd_of_mem_finMulAntidiag hf _, (mem_finMulAntidiag.mp hf).2⟩
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
Goal:
d n : ℕ
i : Fin d
hd : d ≠ 1
k : ℕ
h : k ∣ n ∧ ¬n = 0 → ∃ (a : Fin d → ℕ), (∏ i : Fin d, a i = n ∧ n ≠ 0) ∧ a i = k
⊢ k ∣ n ∧ ¬n = 0 → ∃ a ∈ d.finMulAntidiag n, a i = k

Tactic:
simp_rw [mem_finMulAntidiag]

Premises used: Nat.mem_finMulAntidiag
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
Goal:
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
rw : 2 ≤ d
⊢ Nontrivial (Fin d)

Tactic:
rw [Fin.nontrivial_iff_two_le]

Premises used: Fin.nontrivial_iff_two_le
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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
inr : ∀ (hd' : d ≠ 0), 2 ≤ d
⊢ 2 ≤ d

Tactic:
obtain rfl | hd' := eq_or_ne d 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
Goal:
k r : ℕ
hn : ¬k * r = 0
i : Fin 0
hd : Ne (α := ℕ) 0 1
⊢ LE.le (α := ℕ) 2 0

Tactic:
i.elim0

Premises used: Fin.elim0
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
Goal:
k r : ℕ
hn : ¬k * r = 0
i : Fin 0
hd : Ne (α := ℕ) 0 1
⊢ LE.le (α := ℕ) 2 0

Tactic:
exact i.elim0

Premises used: Fin.elim0
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
Goal:
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hd' : d ≠ 0
⊢ 2 ≤ d

Tactic:
lia
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
Goal:
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
⊢ 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
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
Goal:
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hs : Nontrivial (Fin d)
h : ∀ (i' : Fin d) (hi_ne : i' ≠ i), ∃ (a : Fin d → ℕ), (∏ i : Fin d, a i = k * r ∧ k * r ≠ 0) ∧ a i = k
⊢ ∃ (a : Fin d → ℕ), (∏ i : Fin d, a i = k * r ∧ k * r ≠ 0) ∧ a i = k

Tactic:
obtain ⟨i', hi_ne⟩ := exists_ne i

Premises used: exists_ne
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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 :
  (∏ 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
⊢ ∃ (a : Fin d → ℕ), (∏ i : Fin d, a i = k * r ∧ k * r ≠ 0) ∧ a i = k

Tactic:
use fun j => if j = i then k else if j = i' then r else 1

Premises used: OfNat.ofNat, Eq, ite
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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 : (∏ x : Fin d, if x = i then k else if x = i' then r else 1) = k * r ∧ k * r ≠ 0
⊢ (∏ 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:
simp only [ite_true, and_true]

Premises used: and_true, ite_true
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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
h₁ : i' ∈ erase univ i
⊢ (∏ x : Fin d, 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')]

Premises used: Finset.mem_univ, Finset.univ, Finset.mul_prod_erase
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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
⊢ (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:
simp_all
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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' ∈ erase univ i

Tactic:
mem_erase.mpr ⟨hi_ne, mem_univ _⟩

Premises used: Iff.mpr, Finset.mem_univ, Finset.mem_erase, And.intro
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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' ∈ erase univ i

Tactic:
exact mem_erase.mpr ⟨hi_ne, mem_univ _⟩

Premises used: Iff.mpr, Finset.mem_univ, Finset.mem_erase, And.intro
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
Goal:
n : ℕ
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
⊢ image (α := (i : Fin 2) → ℕ) (⇑(piFinTwoEquiv fun (x : Fin 2) ↦ ℕ) : (a : (i : Fin 2) → ℕ) → ℕ × ℕ)
      (finMulAntidiag 2 n) =
    n.divisorsAntidiagonal

Tactic:
ext x
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
Goal:
n : ℕ
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:
simp [(piFinTwoEquiv <| fun _ => ℕ).symm.surjective.exists]

Premises used: Function.Surjective.exists, Nat, Equiv.surjective, Equiv.symm, piFinTwoEquiv
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
Goal:
d n p : ℕ
hn : Squarefree n
hp : p ∈ n.primeFactorsList
f : Fin d → ℕ
hf : f ∈ d.finMulAntidiag n
⊢ ∏ i : Fin d, f i = n ∧ n ≠ 0

Tactic:
rw [mem_finMulAntidiag] at hf

Premises used: Nat.mem_finMulAntidiag
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
Goal:
d n p : ℕ
hn : Squarefree n
hp : p ∈ n.primeFactorsList
f : Fin d → ℕ
hf : ∏ i : Fin d, f i = n ∧ n ≠ 0
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
⊢ ∃! i : Fin d, p ∣ f i

Tactic:
rw [mem_primeFactorsList hf.2, ← hf.1, hp.1.prime.dvd_finsetProd_iff] at hp

Premises used: Nat.mem_primeFactorsList, And.right, And.left
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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
obtain : ∀ (i : Fin d) (his : Membership.mem (γ := Finset (Fin d)) univ i) (hi : p ∣ f i), ∃! i : Fin d, p ∣ f i
⊢ ∃! i : Fin d, p ∣ f i

Tactic:
obtain ⟨i, his, hi⟩ := hp.2

Premises used: And.right
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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

Tactic:
⟨i, hi, ?_⟩

Premises used: ExistsUnique, And.intro, Exists.intro
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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
refine : ∀ (y : Fin d), (fun (i : Fin d) ↦ p ∣ f i) y → y = i
⊢ ∃! i : Fin d, p ∣ f i

Tactic:
refine ⟨i, hi, ?_⟩
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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
by_contra : ∀ (hij : ¬j = i), False
⊢ j = i

Tactic:
by_contra hij
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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
apply : (f i).Coprime (f j)
⊢ False

Tactic:
apply Nat.Prime.not_coprime_iff_dvd.mpr ⟨p, hp.1, hi, hj⟩

Premises used: Iff.mpr, And.left, And.intro, Exists.intro, Nat.Prime.not_coprime_iff_dvd
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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
h : Squarefree (f i * f j)
⊢ (f i).Coprime (f j)

Tactic:
apply Nat.coprime_of_squarefree_mul

Premises used: Nat.coprime_of_squarefree_mul
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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
h : f i * f j ∣ n
⊢ Squarefree (f i * f j)

Tactic:
apply hn.squarefree_of_dvd

Premises used: Squarefree.squarefree_of_dvd
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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
h : f i * f j ∣ f i * f j * ∏ x ∈ (erase univ i).erase j, f x
⊢ f i * f j ∣ n

Tactic:
rw [← hf.1, ← Finset.mul_prod_erase _ _ his,
    ← Finset.mul_prod_erase _ _ (mem_erase.mpr ⟨hij, mem_univ _⟩), ← mul_assoc]

Premises used: Iff.mpr, Finset.mem_univ, mul_assoc, Finset.mul_prod_erase, Finset.mem_erase, And.left, And.intro
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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 ∣ f i * f j * ∏ x ∈ (erase univ i).erase j, f x

Tactic:
apply Nat.dvd_mul_right

Premises used: Nat.dvd_mul_right
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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 : ∏ i : Fin d, d.primeFactorsPiBij n f hf i = n ∧ n ≠ 0
⊢ d.primeFactorsPiBij n f hf ∈ d.finMulAntidiag n

Tactic:
rw [mem_finMulAntidiag]

Premises used: Nat.mem_finMulAntidiag
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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

Tactic:
⟨?_, hn.ne_zero⟩

Premises used: Squarefree.ne_zero, And.intro
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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
refine : ∏ i : Fin d, d.primeFactorsPiBij n f hf i = n
⊢ ∏ i : Fin d, d.primeFactorsPiBij n f hf i = n ∧ n ≠ 0

Tactic:
refine ⟨?_, hn.ne_zero⟩
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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
h : ∀ i ∈ n.primeFactors.attach, Membership.mem (γ := Finset (Fin d)) univ (f (↑i : ℕ) ⋯)
⊢ ∏ i : Fin d, ∏ p ∈ n.primeFactors.attach with f (↑p : ℕ) ⋯ = i, (↑p : ℕ) = n

Tactic:
rw [prod_fiberwise_of_maps_to, prod_attach (f := fun x => x)]

Premises used: Finset.prod_fiberwise_of_maps_to, Finset.prod_attach
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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
⊢ ∏ x ∈ n.primeFactors, x = n

Tactic:
apply prod_primeFactors_of_squarefree hn

Premises used: Nat.prod_primeFactors_of_squarefree
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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 ∈ n.primeFactors.attach, Membership.mem (γ := Finset (Fin d)) univ (f (↑i : ℕ) ⋯)

Tactic:
apply fun _ _ => mem_univ _

Premises used: Finset.mem_univ
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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
contrapose! : f ≠ g → d.primeFactorsPiBij n f hf ≠ d.primeFactorsPiBij n g hg
⊢ d.primeFactorsPiBij n f hf = d.primeFactorsPiBij n g hg → f = g

Tactic:
contrapose!
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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
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
⊢ f ≠ g → d.primeFactorsPiBij n f hf ≠ d.primeFactorsPiBij n g hg

Tactic:
simp_rw [Function.ne_iff]

Premises used: Function.ne_iff
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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 : d.primeFactorsPiBij n f hf (f p hp) ≠ d.primeFactorsPiBij n g hg (f p hp)
⊢ ∃ (a : Fin d), d.primeFactorsPiBij n f hf a ≠ d.primeFactorsPiBij n g hg a

Tactic:
use f p hp
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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 : ℕ))
h₁ : ∏ p ∈ n.primeFactors.attach with g (↑p : ℕ) ⋯ = f p hp, (↑p : ℕ) ∉ {x : ℕ | p ∣ x}
⊢ Ne (α := ℕ) (∏ p ∈ n.primeFactors.attach with f (↑p : ℕ) ⋯ = f p hp, (↑p : ℕ))
    (∏ p ∈ n.primeFactors.attach with g (↑p : ℕ) ⋯ = f p hp, (↑p : ℕ))

Tactic:
apply ne_of_mem_of_not_mem (s := {x | p ∣ x})

Premises used: ne_of_mem_of_not_mem
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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 : p ∣ ∏ a ∈ n.primeFactors.attach, if f (↑a : ℕ) ⋯ = f p hp then (↑a : ℕ) else 1
⊢ p ∣ ∏ p ∈ n.primeFactors.attach with f (↑p : ℕ) ⋯ = f p hp, (↑p : ℕ)

Tactic:
rw [Finset.prod_filter]

Premises used: Finset.prod_filter
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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
⊢ (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) ∣
    ∏ i ∈ n.primeFactors.attach, if f (↑i : ℕ) ⋯ = f p hp then (↑i : ℕ) else 1

Tactic:
Finset.dvd_prod_of_mem _ (mem_attach (n.primeFactors) ⟨p, hp⟩)

Premises used: Finset.dvd_prod_of_mem, Finset.mem_attach, Subtype.mk, Nat.primeFactors
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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 :
  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
⊢ p ∣ ∏ a ∈ n.primeFactors.attach, if f (↑a : ℕ) ⋯ = f p hp then (↑a : ℕ) else 1

Tactic:
convert! Finset.dvd_prod_of_mem _ (mem_attach (n.primeFactors) ⟨p, hp⟩)

Premises used: Finset.dvd_prod_of_mem, Finset.mem_attach, Subtype.mk, Nat.primeFactors
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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 h₁ : p = (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ n.primeFactors) 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

Tactic:
rw [if_pos rfl]

Premises used: if_pos, rfl
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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
⊢ Prime p ∧ p ∣ n ∧ n ≠ 0

Tactic:
rw [mem_primeFactors] at hp

Premises used: Nat.mem_primeFactors
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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
hp₁ : Prime p ∧ p ∣ n ∧ n ≠ 0
⊢ f p hp ≠ g p hp

Tactic:
rw [mem_primeFactors] at hp

Premises used: Nat.mem_primeFactors
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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
h : ¬∃ a ∈ {p_1 ∈ n.primeFactors.attach | g (↑p_1 : ℕ) ⋯ = f p hp_1}, p ∣ (↑a : ℕ)
⊢ ¬p ∣ ∏ p ∈ n.primeFactors.attach with g (↑p : ℕ) ⋯ = f p hp_1, (↑p : ℕ)

Tactic:
rw [Prime.dvd_finsetProd_iff hp.1.prime]

Premises used: Prime.dvd_finsetProd_iff, Nat.Prime.prime, And.left
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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
h : ∀ (a : ↥n.primeFactors) (_ : a ∈ {p_1 ∈ n.primeFactors.attach | g (↑p_1 : ℕ) ⋯ = f p hp_1}), ¬p ∣ (↑a : ℕ)
⊢ ¬∃ a ∈ {p_1 ∈ n.primeFactors.attach | g (↑p_1 : ℕ) ⋯ = f p hp_1}, p ∣ (↑a : ℕ)

Tactic:
push Not

Premises used: Not
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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
q : ↥n.primeFactors
hq : q ∈ {p_1 ∈ n.primeFactors.attach | g (↑p_1 : ℕ) ⋯ = f p hp_1}
h : ¬p = (↑q : ℕ)
⊢ ¬p ∣ (↑q : ℕ)

Tactic:
rw [Nat.prime_dvd_prime_iff_eq hp.1 (Nat.prime_of_mem_primeFactorsList
      <| List.mem_toFinset.mp q.2)]

Premises used: List.mem_toFinset, Nat.prime_of_mem_primeFactorsList, Nat.prime_dvd_prime_iff_eq, And.left, Iff.mp, Subtype.property
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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
q : ↥n.primeFactors
hp_1 : (↑q : ℕ) ∈ n.primeFactors
hp : Prime (↑q : ℕ) ∧ (↑q : ℕ) ∣ n ∧ n ≠ 0
hfg : f (↑q : ℕ) hp_1 ≠ g (↑q : ℕ) hp_1
hq : q ∈ {p ∈ n.primeFactors.attach | g (↑p : ℕ) ⋯ = f (↑q : ℕ) hp_1}
⊢ f (↑q : ℕ) hp_1 ≠ f (↑q : ℕ) hp_1

Tactic:
rw [(mem_filter.mp hq).2] at hfg

Premises used: And.right, Iff.mp, Finset.mem_filter