awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
q : ↥n.primeFactors
hq : q ∈ {p_1 ∈ n.primeFactors.attach | g (↑p_1 : ℕ) ⋯ = f p hp_1}
⊢ ¬p ∣ (↑q : ℕ)
have h : ¬p = (↑q : ℕ)
Tactic: rw [Nat.prime_dvd_prime_iff_eq hp.1 (Nat.prime_of_mem_primeFactorsList
      <| List.mem_toFinset.mp q.2)]
-- 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
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}
⊢ False
have hfg₁ : f (↑q : ℕ) hp_1 ≠ f (↑q : ℕ) hp_1
Tactic: rw [(mem_filter.mp hq).2] at hfg
Cleared hypotheses: hfg, hq
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (hypothesis)
Goal:
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiag n
⊢ ∃ (g : (a : ℕ) → a ∈ n.primeFactors → Fin d) (hg :
    Membership.mem (γ := Finset ((a : ℕ) → a ∈ n.primeFactors → Fin d))
      (n.primeFactors.pi (β := fun (a : ℕ) ↦ Fin d) fun (x : ℕ) ↦ univ) g),
    d.primeFactorsPiBij n g hg = t
have existsUnique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), ∃! i : Fin d, p ∣ t i
Tactic: have existsUnique := fun (p : ℕ) (hp : p ∈ n.primeFactors) =>
    (finMulAntidiag_existsUnique_prime_dvd hn
      (mem_primeFactors_iff_mem_primeFactorsList.mp hp) t ht)
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiag n
existsUnique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), ∃! i : Fin d, p ∣ t i
⊢ ∃ (g : (a : ℕ) → a ∈ n.primeFactors → Fin d) (hg :
    Membership.mem (γ := Finset ((a : ℕ) → a ∈ n.primeFactors → Fin d))
      (n.primeFactors.pi (β := fun (a : ℕ) ↦ Fin d) fun (x : ℕ) ↦ univ) g),
    d.primeFactorsPiBij n g hg = t
have choose : ∀ (f : (p : ℕ) → (hp : p ∈ n.primeFactors) → Fin d)
  (hf : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (fun (i : Fin d) ↦ p ∣ t i) (f p hp))
  (hf_unique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors) (y : Fin d), (fun (i : Fin d) ↦ p ∣ t i) y → y = f p hp),
  ∃ (g : (a : ℕ) → a ∈ n.primeFactors → Fin d) (hg :
    Membership.mem (γ := Finset ((a : ℕ) → a ∈ n.primeFactors → Fin d))
      (n.primeFactors.pi (β := fun (a : ℕ) ↦ Fin d) fun (x : ℕ) ↦ univ) g),
    d.primeFactorsPiBij n g hg = t
Tactic: choose f hf hf_unique using existsUnique
Cleared hypotheses: existsUnique
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiag n
f : (p : ℕ) → (hp : p ∈ n.primeFactors) → Fin d
hf : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (fun (i : Fin d) ↦ p ∣ t i) (f p hp)
hf_unique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors) (y : Fin d), (fun (i : Fin d) ↦ p ∣ t i) y → y = f p hp
⊢ ∃ (g : (a : ℕ) → a ∈ n.primeFactors → Fin d) (hg :
    Membership.mem (γ := Finset ((a : ℕ) → a ∈ n.primeFactors → Fin d))
      (n.primeFactors.pi (β := fun (a : ℕ) ↦ Fin d) fun (x : ℕ) ↦ univ) g),
    d.primeFactorsPiBij n g hg = t
have refine_1 : Membership.mem (γ := Finset ((a : ℕ) → a ∈ n.primeFactors → Fin d))
  (n.primeFactors.pi (β := fun (a : ℕ) ↦ Fin d) fun (x : ℕ) ↦ univ) f
Tactic: refine ⟨f, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiag n
f : (p : ℕ) → (hp : p ∈ n.primeFactors) → Fin d
hf : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (fun (i : Fin d) ↦ p ∣ t i) (f p hp)
hf_unique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors) (y : Fin d), (fun (i : Fin d) ↦ p ∣ t i) y → y = f p hp
refine_1 :
  Membership.mem (γ := Finset ((a : ℕ) → a ∈ n.primeFactors → Fin d))
    (n.primeFactors.pi (β := fun (a : ℕ) ↦ Fin d) fun (x : ℕ) ↦ univ) f
⊢ ∃ (g : (a : ℕ) → a ∈ n.primeFactors → Fin d) (hg :
    Membership.mem (γ := Finset ((a : ℕ) → a ∈ n.primeFactors → Fin d))
      (n.primeFactors.pi (β := fun (a : ℕ) ↦ Fin d) fun (x : ℕ) ↦ univ) g),
    d.primeFactorsPiBij n g hg = t
have refine_2 : d.primeFactorsPiBij n f sorry = t
Tactic: refine ⟨f, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiag n
f : (p : ℕ) → (hp : p ∈ n.primeFactors) → Fin d
hf : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (fun (i : Fin d) ↦ p ∣ t i) (f p hp)
hf_unique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors) (y : Fin d), (fun (i : Fin d) ↦ p ∣ t i) y → y = f p hp
⊢ d.primeFactorsPiBij n f ⋯ = t
have refine_2 : ∀ (i : Fin d), d.primeFactorsPiBij n f sorry i = t i
Tactic: funext i
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (hypothesis)
Goal:
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiag n
f : (p : ℕ) → (hp : p ∈ n.primeFactors) → Fin d
hf : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (fun (i : Fin d) ↦ p ∣ t i) (f p hp)
hf_unique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors) (y : Fin d), (fun (i : Fin d) ↦ p ∣ t i) y → y = f p hp
i : Fin d
⊢ d.primeFactorsPiBij n f ⋯ i = t i
have this : t i ∣ n
Tactic: have : t i ∣ n := dvd_of_mem_finMulAntidiag ht _
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiag n
f : (p : ℕ) → (hp : p ∈ n.primeFactors) → Fin d
hf : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (fun (i : Fin d) ↦ p ∣ t i) (f p hp)
hf_unique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors) (y : Fin d), (fun (i : Fin d) ↦ p ∣ t i) y → y = f p hp
i : Fin d
this : t i ∣ n
⊢ d.primeFactorsPiBij n f ⋯ i = t i
have trans : d.primeFactorsPiBij n f sorry i = ∏ p ∈ n.primeFactors.attach, if (↑p : ℕ) ∣ t i then (↑p : ℕ) else 1
Tactic: trans (∏ p ∈ n.primeFactors.attach, if p.1 ∣ t i then p else 1)
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiag n
f : (p : ℕ) → (hp : p ∈ n.primeFactors) → Fin d
hf : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (fun (i : Fin d) ↦ p ∣ t i) (f p hp)
hf_unique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors) (y : Fin d), (fun (i : Fin d) ↦ p ∣ t i) y → y = f p hp
i : Fin d
this : t i ∣ n
trans : d.primeFactorsPiBij n f ⋯ i = ∏ p ∈ n.primeFactors.attach, if (↑p : ℕ) ∣ t i then (↑p : ℕ) else 1
⊢ d.primeFactorsPiBij n f ⋯ i = t i
have trans₁ : (∏ p ∈ n.primeFactors.attach, if (↑p : ℕ) ∣ t i then (↑p : ℕ) else 1) = t i
Tactic: trans (∏ p ∈ n.primeFactors.attach, if p.1 ∣ t i then p else 1)
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiag n
f : (p : ℕ) → (hp : p ∈ n.primeFactors) → Fin d
hf : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (fun (i : Fin d) ↦ p ∣ t i) (f p hp)
hf_unique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors) (y : Fin d), (fun (i : Fin d) ↦ p ∣ t i) y → y = f p hp
i : Fin d
this : t i ∣ n
⊢ d.primeFactorsPiBij n f ⋯ i = ∏ p ∈ n.primeFactors.attach, if (↑p : ℕ) ∣ t i then (↑p : ℕ) else 1
have rw : Eq (α := ℕ) (∏ p ∈ n.primeFactors.attach with f (↑p : ℕ) sorry = i, (↑p : ℕ))
  (∏ a ∈ n.primeFactors.attach with (↑a : ℕ) ∣ t i, (↑a : ℕ))
Tactic: rw [Nat.primeFactorsPiBij, ← prod_filter]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiag n
f : (p : ℕ) → (hp : p ∈ n.primeFactors) → Fin d
hf : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (fun (i : Fin d) ↦ p ∣ t i) (f p hp)
hf_unique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors) (y : Fin d), (fun (i : Fin d) ↦ p ∣ t i) y → y = f p hp
i : Fin d
this : t i ∣ n
⊢ Eq (α := ℕ) (∏ p ∈ n.primeFactors.attach with f (↑p : ℕ) ⋯ = i, (↑p : ℕ))
    (∏ a ∈ n.primeFactors.attach with (↑a : ℕ) ∣ t i, (↑a : ℕ))
have e_s : Eq (α := ↥n.primeFactors → Prop) (fun (p : ↥n.primeFactors) ↦ f (↑p : ℕ) sorry = i) fun (a : ↥n.primeFactors) ↦
  (↑a : ℕ) ∣ t i
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiag n
f : (p : ℕ) → (hp : p ∈ n.primeFactors) → Fin d
hf : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (fun (i : Fin d) ↦ p ∣ t i) (f p hp)
hf_unique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors) (y : Fin d), (fun (i : Fin d) ↦ p ∣ t i) y → y = f p hp
i : Fin d
this : t i ∣ n
⊢ (∏ p ∈ n.primeFactors.attach, if (↑p : ℕ) ∣ t i then (↑p : ℕ) else 1) = t i
have rw : ∏ a ∈ n.primeFactors with a ∣ t i, a = t i
Tactic: rw [prod_attach (f := fun p => if p ∣ t i then p else 1), ← Finset.prod_filter]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiag n
f : (p : ℕ) → (hp : p ∈ n.primeFactors) → Fin d
hf : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (fun (i : Fin d) ↦ p ∣ t i) (f p hp)
hf_unique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors) (y : Fin d), (fun (i : Fin d) ↦ p ∣ t i) y → y = f p hp
i : Fin d
this : t i ∣ n
⊢ ∏ a ∈ n.primeFactors with a ∣ t i, a = t i
have rw : ∏ a ∈ (t i).primeFactors, a = t i
Tactic: rw [primeFactors_filter_dvd_of_dvd hn.ne_zero this]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d n : ℕ
hn : Squarefree n
⊢ #(d.finMulAntidiag n) = HPow.hPow (β := ℕ) d ((ω : (a : ℕ) → ℕ) n : ℕ)
have rw : card (α := (a : ℕ) → a ∈ n.primeFactors → Fin d) (n.primeFactors.pi (β := fun (x : ℕ) ↦ Fin d) fun (x : ℕ) ↦ univ) =
  HPow.hPow (β := ℕ) d ((ω : (a : ℕ) → ℕ) n : ℕ)
Tactic: rw [← card_finMulAntidiag_pi d n hn, Finset.card_pi, Finset.prod_const,
    ArithmeticFunction.cardDistinctFactors_apply, ← List.card_toFinset, toFinset_factors,
    Finset.card_fin]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d n : ℕ
hn : Squarefree n
rw :
  card (α := (a : ℕ) → a ∈ n.primeFactors → Fin d) (n.primeFactors.pi (β := fun (x : ℕ) ↦ Fin d) fun (x : ℕ) ↦ univ) =
    HPow.hPow (β := ℕ) d ((ω : (a : ℕ) → ℕ) n : ℕ)
⊢ #(d.finMulAntidiag n) = HPow.hPow (β := ℕ) d ((ω : (a : ℕ) → ℕ) n : ℕ)
have rw₁ : ∏ i ∈ n.primeFactors, card (α := Fin d) univ = HPow.hPow (β := ℕ) d ((ω : (a : ℕ) → ℕ) n : ℕ)
Tactic: rw [← card_finMulAntidiag_pi d n hn, Finset.card_pi, Finset.prod_const,
    ArithmeticFunction.cardDistinctFactors_apply, ← List.card_toFinset, toFinset_factors,
    Finset.card_fin]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d n : ℕ
hn : Squarefree n
rw :
  card (α := (a : ℕ) → a ∈ n.primeFactors → Fin d) (n.primeFactors.pi (β := fun (x : ℕ) ↦ Fin d) fun (x : ℕ) ↦ univ) =
    HPow.hPow (β := ℕ) d ((ω : (a : ℕ) → ℕ) n : ℕ)
rw₁ : ∏ i ∈ n.primeFactors, card (α := Fin d) univ = HPow.hPow (β := ℕ) d ((ω : (a : ℕ) → ℕ) n : ℕ)
⊢ #(d.finMulAntidiag n) = HPow.hPow (β := ℕ) d ((ω : (a : ℕ) → ℕ) n : ℕ)
have rw₂ : card (α := Fin d) univ ^ #n.primeFactors = HPow.hPow (β := ℕ) d ((ω : (a : ℕ) → ℕ) n : ℕ)
Tactic: rw [← card_finMulAntidiag_pi d n hn, Finset.card_pi, Finset.prod_const,
    ArithmeticFunction.cardDistinctFactors_apply, ← List.card_toFinset, toFinset_factors,
    Finset.card_fin]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d n : ℕ
hn : Squarefree n
rw :
  card (α := (a : ℕ) → a ∈ n.primeFactors → Fin d) (n.primeFactors.pi (β := fun (x : ℕ) ↦ Fin d) fun (x : ℕ) ↦ univ) =
    HPow.hPow (β := ℕ) d ((ω : (a : ℕ) → ℕ) n : ℕ)
rw₁ : ∏ i ∈ n.primeFactors, card (α := Fin d) univ = HPow.hPow (β := ℕ) d ((ω : (a : ℕ) → ℕ) n : ℕ)
rw₂ : card (α := Fin d) univ ^ #n.primeFactors = HPow.hPow (β := ℕ) d ((ω : (a : ℕ) → ℕ) n : ℕ)
⊢ #(d.finMulAntidiag n) = HPow.hPow (β := ℕ) d ((ω : (a : ℕ) → ℕ) n : ℕ)
have rw₃ : card (α := Fin d) univ ^ #n.primeFactors = d ^ n.primeFactorsList.dedup.length
Tactic: rw [← card_finMulAntidiag_pi d n hn, Finset.card_pi, Finset.prod_const,
    ArithmeticFunction.cardDistinctFactors_apply, ← List.card_toFinset, toFinset_factors,
    Finset.card_fin]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d n : ℕ
hn : Squarefree n
rw :
  card (α := (a : ℕ) → a ∈ n.primeFactors → Fin d) (n.primeFactors.pi (β := fun (x : ℕ) ↦ Fin d) fun (x : ℕ) ↦ univ) =
    HPow.hPow (β := ℕ) d ((ω : (a : ℕ) → ℕ) n : ℕ)
rw₁ : ∏ i ∈ n.primeFactors, card (α := Fin d) univ = HPow.hPow (β := ℕ) d ((ω : (a : ℕ) → ℕ) n : ℕ)
rw₂ : card (α := Fin d) univ ^ #n.primeFactors = HPow.hPow (β := ℕ) d ((ω : (a : ℕ) → ℕ) n : ℕ)
rw₃ : card (α := Fin d) univ ^ #n.primeFactors = d ^ n.primeFactorsList.dedup.length
⊢ #(d.finMulAntidiag n) = HPow.hPow (β := ℕ) d ((ω : (a : ℕ) → ℕ) n : ℕ)
have rw₄ : card (α := Fin d) univ ^ #n.primeFactors = d ^ #n.primeFactorsList.toFinset
Tactic: rw [← card_finMulAntidiag_pi d n hn, Finset.card_pi, Finset.prod_const,
    ArithmeticFunction.cardDistinctFactors_apply, ← List.card_toFinset, toFinset_factors,
    Finset.card_fin]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d n : ℕ
hn : Squarefree n
rw :
  card (α := (a : ℕ) → a ∈ n.primeFactors → Fin d) (n.primeFactors.pi (β := fun (x : ℕ) ↦ Fin d) fun (x : ℕ) ↦ univ) =
    HPow.hPow (β := ℕ) d ((ω : (a : ℕ) → ℕ) n : ℕ)
rw₁ : ∏ i ∈ n.primeFactors, card (α := Fin d) univ = HPow.hPow (β := ℕ) d ((ω : (a : ℕ) → ℕ) n : ℕ)
rw₂ : card (α := Fin d) univ ^ #n.primeFactors = HPow.hPow (β := ℕ) d ((ω : (a : ℕ) → ℕ) n : ℕ)
rw₃ : card (α := Fin d) univ ^ #n.primeFactors = d ^ n.primeFactorsList.dedup.length
rw₄ : card (α := Fin d) univ ^ #n.primeFactors = d ^ #n.primeFactorsList.toFinset
⊢ #(d.finMulAntidiag n) = HPow.hPow (β := ℕ) d ((ω : (a : ℕ) → ℕ) n : ℕ)
have rw₅ : card (α := Fin d) univ ^ #n.primeFactors = d ^ #n.primeFactors
Tactic: rw [← card_finMulAntidiag_pi d n hn, Finset.card_pi, Finset.prod_const,
    ArithmeticFunction.cardDistinctFactors_apply, ← List.card_toFinset, toFinset_factors,
    Finset.card_fin]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
d n : ℕ
hn : Squarefree n
rw :
  card (α := (a : ℕ) → a ∈ n.primeFactors → Fin d) (n.primeFactors.pi (β := fun (x : ℕ) ↦ Fin d) fun (x : ℕ) ↦ univ) =
    HPow.hPow (β := ℕ) d ((ω : (a : ℕ) → ℕ) n : ℕ)
rw₁ : ∏ i ∈ n.primeFactors, card (α := Fin d) univ = HPow.hPow (β := ℕ) d ((ω : (a : ℕ) → ℕ) n : ℕ)
rw₂ : card (α := Fin d) univ ^ #n.primeFactors = HPow.hPow (β := ℕ) d ((ω : (a : ℕ) → ℕ) n : ℕ)
rw₃ : card (α := Fin d) univ ^ #n.primeFactors = d ^ n.primeFactorsList.dedup.length
rw₄ : card (α := Fin d) univ ^ #n.primeFactors = d ^ #n.primeFactorsList.toFinset
rw₅ : card (α := Fin d) univ ^ #n.primeFactors = d ^ #n.primeFactors
⊢ #(d.finMulAntidiag n) = HPow.hPow (β := ℕ) d ((ω : (a : ℕ) → ℕ) n : ℕ)
have rw₆ : d ^ #n.primeFactors = d ^ #n.primeFactors
Tactic: rw [← card_finMulAntidiag_pi d n hn, Finset.card_pi, Finset.prod_const,
    ArithmeticFunction.cardDistinctFactors_apply, ← List.card_toFinset, toFinset_factors,
    Finset.card_fin]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
n : ℕ
a : Fin 3 → ℕ
ha : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) a
⊢ a 0 * a 1 * a 2 = n
have rw : a 0 * a 1 * a 2 = ∏ i : Fin 3, a i
Tactic: rw [← (mem_finMulAntidiag.mp ha).1, Fin.prod_univ_three a]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
n : ℕ
a : Fin 3 → ℕ
ha : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) a
rw : a 0 * a 1 * a 2 = ∏ i : Fin 3, a i
⊢ a 0 * a 1 * a 2 = n
have rw₁ : a 0 * a 1 * a 2 = a 0 * a 1 * a 2
Tactic: rw [← (mem_finMulAntidiag.mp ha).1, Fin.prod_univ_three a]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) a
⊢ f a ha ∈
    {x ∈ n.divisors ×ˢ n.divisors |
      match (motive := ℕ × ℕ → Prop) x with
      | (x, y) => x.lcm y = n}
have rw : (((f a ha).1 ∣ n ∧ n ≠ 0) ∧ (f a ha).2 ∣ n ∧ n ≠ 0) ∧
  match (motive := ℕ × ℕ → Prop) f a ha with
  | (x, y) => x.lcm y = n
Tactic: rw [mem_filter, Finset.mem_product, mem_divisors, mem_divisors]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) a
⊢ (((f a ha).1 ∣ n ∧ n ≠ 0) ∧ (f a ha).2 ∣ n ∧ n ≠ 0) ∧
    match (motive := ℕ × ℕ → Prop) f a ha with
    | (x, y) => x.lcm y = n
have refine_1 : (f a ha).1 ∣ n
Tactic: refine ⟨⟨⟨?_, hn.ne_zero⟩, ⟨?_, hn.ne_zero⟩⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) a
refine_1 : (f a ha).1 ∣ n
⊢ (((f a ha).1 ∣ n ∧ n ≠ 0) ∧ (f a ha).2 ∣ n ∧ n ≠ 0) ∧
    match (motive := ℕ × ℕ → Prop) f a ha with
    | (x, y) => x.lcm y = n
have refine_2 : (f a ha).2 ∣ n
Tactic: refine ⟨⟨⟨?_, hn.ne_zero⟩, ⟨?_, hn.ne_zero⟩⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) a
refine_1 : (f a ha).1 ∣ n
refine_2 : (f a ha).2 ∣ n
⊢ (((f a ha).1 ∣ n ∧ n ≠ 0) ∧ (f a ha).2 ∣ n ∧ n ≠ 0) ∧
    match (motive := ℕ × ℕ → Prop) f a ha with
    | (x, y) => x.lcm y = n
have refine_3 : match (motive := ℕ × ℕ → Prop) f a ha with
| (x, y) => x.lcm y = n
Tactic: refine ⟨⟨⟨?_, hn.ne_zero⟩, ⟨?_, hn.ne_zero⟩⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) a
⊢ (f a ha).1 ∣ n
have refine_1 : (a 0 * a 1, a 0 * a 2).1 ∣ a 0 * a 1 * a 2
Tactic: rw [f, ← finMulAntidiag_three a ha]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) a
⊢ (f a ha).2 ∣ n
have refine_2 : (a 0 * a 1, a 0 * a 2).2 ∣ a 0 * a 1 * a 2
Tactic: rw [f, ← finMulAntidiag_three a ha]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) a
⊢ match (motive := ℕ × ℕ → Prop) f a ha with
  | (x, y) => x.lcm y = n
have refine_3 : match (motive := ℕ × ℕ → Prop) (a 0 * a 1, a 0 * a 2) with
| (x, y) => x.lcm y = a 0 * a 1 * a 2
Tactic: rw [f, ← finMulAntidiag_three a ha]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) a
⊢ (a 0 * a 1, a 0 * a 2).2 ∣ a 0 * a 1 * a 2
have h : a 0 * a 1 * a 2 = (a 0 * a 1, a 0 * a 2).2 * a 1
Tactic: use a 1
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) a
⊢ (a 0 * a 1).lcm (a 0 * a 2) = a 0 * a 1 * a 2
have refine_3 : a 0 * (a 1 * a 2) = a 0 * a 1 * a 2
Tactic: rw [lcm_mul_left, Nat.Coprime.lcm_eq_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) a
refine_3 : a 0 * (a 1 * a 2) = a 0 * a 1 * a 2
⊢ (a 0 * a 1).lcm (a 0 * a 2) = a 0 * a 1 * a 2
have refine_3₁ : (a 1).Coprime (a 2)
Tactic: rw [lcm_mul_left, Nat.Coprime.lcm_eq_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) a
⊢ (a 1).Coprime (a 2)
have refine_3 : a 1 * a 2 ∣ n
Tactic: refine coprime_of_squarefree_mul (hn.squarefree_of_dvd ?_)
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) a
⊢ a 1 * a 2 ∣ n
have h : n = a 1 * a 2 * a 0
Tactic: use a 0
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) a
⊢ n = a 1 * a 2 * a 0
have h : a 0 * a 1 * a 2 = a 1 * a 2 * a 0
Tactic: rw [← finMulAntidiag_three a ha]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (hypothesis)
Goal:
n : ℕ
a : Fin 3 → ℕ
ha : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) a
b : Fin 3 → ℕ
hb : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) b
hfab : f a ha = f b hb
⊢ a = b
have hfab1 : a 0 * a 1 = b 0 * b 1
Tactic: obtain ⟨hfab1, hfab2⟩ := Prod.mk.inj hfab
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (hypothesis)
Goal:
n : ℕ
a : Fin 3 → ℕ
ha : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) a
b : Fin 3 → ℕ
hb : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) b
hfab : f a ha = f b hb
hfab1 : a 0 * a 1 = b 0 * b 1
⊢ a = b
have hfab2 : a 0 * a 2 = b 0 * b 2
Tactic: obtain ⟨hfab1, hfab2⟩ := Prod.mk.inj hfab
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
n : ℕ
a : Fin 3 → ℕ
ha : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) a
b : Fin 3 → ℕ
hb : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) b
hfab : f a ha = f b hb
hfab1 : a 0 * a 1 = b 0 * b 1
hfab2 : a 0 * a 2 = b 0 * b 2
⊢ a 0 * a 1 * a 2 = a 0 * a 1 * b 2
have rw : n = a 0 * a 1 * b 2
Tactic: rw [finMulAntidiag_three a ha, hfab1, finMulAntidiag_three b hb]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
n : ℕ
a : Fin 3 → ℕ
ha : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) a
b : Fin 3 → ℕ
hb : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) b
hfab : f a ha = f b hb
hfab1 : a 0 * a 1 = b 0 * b 1
hfab2 : a 0 * a 2 = b 0 * b 2
rw : n = a 0 * a 1 * b 2
⊢ a 0 * a 1 * a 2 = a 0 * a 1 * b 2
have rw₁ : n = b 0 * b 1 * b 2
Tactic: rw [finMulAntidiag_three a ha, hfab1, finMulAntidiag_three b hb]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (goal)
Goal:
n : ℕ
a : Fin 3 → ℕ
ha : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) a
b : Fin 3 → ℕ
hb : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) b
hfab : f a ha = f b hb
hfab1 : a 0 * a 1 = b 0 * b 1
hfab2 : a 0 * a 2 = b 0 * b 2
rw : n = a 0 * a 1 * b 2
rw₁ : n = b 0 * b 1 * b 2
⊢ a 0 * a 1 * a 2 = a 0 * a 1 * b 2
have rw₂ : n = n
Tactic: rw [finMulAntidiag_three a ha, hfab1, finMulAntidiag_three b hb]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (hypothesis)
Goal:
n : ℕ
a : Fin 3 → ℕ
ha : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) a
b : Fin 3 → ℕ
hb : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) b
hfab : f a ha = f b hb
hfab1 : a 0 * a 1 = b 0 * b 1
hfab2 : a 0 * a 2 = b 0 * b 2
⊢ a = b
have hprods : a 0 * a 1 * a 2 = a 0 * a 1 * b 2
Tactic: have hprods : a 0 * a 1 * a 2 = a 0 * a 1 * b 2 := by
    rw [finMulAntidiag_three a ha, hfab1, finMulAntidiag_three b hb]
-- Lean 4 proof step from Mathlib.Algebra.Order.Antidiag.Nat (hypothesis)
Goal:
n : ℕ
a : Fin 3 → ℕ
ha : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) a
b : Fin 3 → ℕ
hb : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) b
hfab : f a ha = f b hb
hfab1 : a 0 * a 1 = b 0 * b 1
hfab2 : a 0 * a 2 = b 0 * b 2
hprods : a 0 * a 1 * a 2 = a 0 * a 1 * b 2
⊢ a = b
have hab2 : a 2 = b 2
Tactic: have hab2 : a 2 = b 2 := by
    rw [← mul_right_inj' <| mul_ne_zero (ne_zero_of_mem_finMulAntidiag ha 0)
      (ne_zero_of_mem_finMulAntidiag ha 1)]
    exact hprods