awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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}
hfg₁ : f (↑q : ℕ) hp_1 ≠ f (↑q : ℕ) hp_1
⊢ q ∈ {p ∈ n.primeFactors.attach | g (↑p : ℕ) ⋯ = f (↑q : ℕ) hp_1}

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

Premises used: And.right, Iff.mp, Finset.mem_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
q : ↥n.primeFactors
hp_1 : (↑q : ℕ) ∈ n.primeFactors
hp : Prime (↑q : ℕ) ∧ (↑q : ℕ) ∣ n ∧ n ≠ 0
hfg : f (↑q : ℕ) hp_1 ≠ f (↑q : ℕ) hp_1
hq : q ∈ {p ∈ n.primeFactors.attach | g (↑p : ℕ) ⋯ = f (↑q : ℕ) hp_1}
⊢ False

Tactic:
hfg rfl

Premises used: 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
q : ↥n.primeFactors
hp_1 : (↑q : ℕ) ∈ n.primeFactors
hp : Prime (↑q : ℕ) ∧ (↑q : ℕ) ∣ n ∧ n ≠ 0
hfg : f (↑q : ℕ) hp_1 ≠ f (↑q : ℕ) hp_1
hq : q ∈ {p ∈ n.primeFactors.attach | g (↑p : ℕ) ⋯ = f (↑q : ℕ) hp_1}
⊢ False

Tactic:
exact hfg rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
Goal:
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiag n
⊢ ∀ (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)
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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
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
⊢ ∃ (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
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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

Tactic:
⟨f, ?_, ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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
refine_2 : d.primeFactorsPiBij n f ⋯ = t
⊢ ∃ (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:
refine ⟨f, ?_, ?_⟩
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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
⊢ Membership.mem (γ := Finset ((a : ℕ) → a ∈ n.primeFactors → Fin d))
    (n.primeFactors.pi (β := fun (a : ℕ) ↦ Fin d) fun (x : ℕ) ↦ univ) f

Tactic:
simp only [mem_pi, mem_univ, forall_true_iff]

Premises used: Finset.mem_univ, Finset.mem_pi, forall_true_iff
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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_2 : ∀ (i : Fin d), d.primeFactorsPiBij n f ⋯ i = t i
⊢ d.primeFactorsPiBij n f ⋯ = t

Tactic:
funext i
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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
⊢ t i ∣ n

Tactic:
have : t i ∣ n := dvd_of_mem_finMulAntidiag ht _
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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
trans₁ : (∏ p ∈ n.primeFactors.attach, if (↑p : ℕ) ∣ t i then (↑p : ℕ) else 1) = t i
⊢ d.primeFactorsPiBij n f ⋯ i = t i

Tactic:
trans (∏ p ∈ n.primeFactors.attach, if p.1 ∣ t i then p else 1)
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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
rw :
  Eq (α := ℕ) (∏ p ∈ n.primeFactors.attach with f (↑p : ℕ) ⋯ = i, (↑p : ℕ))
    (∏ a ∈ n.primeFactors.attach with (↑a : ℕ) ∣ t i, (↑a : ℕ))
⊢ d.primeFactorsPiBij n f ⋯ i = ∏ p ∈ n.primeFactors.attach, if (↑p : ℕ) ∣ t i then (↑p : ℕ) else 1

Tactic:
rw [Nat.primeFactorsPiBij, ← prod_filter]

Premises used: _private.0.Nat.primeFactorsPiBij, Finset.prod_filter
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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
e_s :
  Eq (α := ↥n.primeFactors → Prop) (fun (p : ↥n.primeFactors) ↦ f (↑p : ℕ) ⋯ = i) fun (a : ↥n.primeFactors) ↦
    (↑a : ℕ) ∣ t i
⊢ Eq (α := ℕ) (∏ p ∈ n.primeFactors.attach with f (↑p : ℕ) ⋯ = i, (↑p : ℕ))
    (∏ a ∈ n.primeFactors.attach with (↑a : ℕ) ∣ t i, (↑a : ℕ))

Tactic:
congr
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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 (α := ↥n.primeFactors → Prop) (fun (p : ↥n.primeFactors) ↦ f (↑p : ℕ) ⋯ = i) fun (a : ↥n.primeFactors) ↦
    (↑a : ℕ) ∣ t i

Tactic:
grind
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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
rw : ∏ a ∈ n.primeFactors with a ∣ t i, a = t i
⊢ (∏ p ∈ n.primeFactors.attach, if (↑p : ℕ) ∣ t i then (↑p : ℕ) else 1) = t i

Tactic:
rw [prod_attach (f := fun p => if p ∣ t i then p else 1), ← Finset.prod_filter]

Premises used: Dvd.dvd, Finset.prod_filter, Finset.prod_attach, OfNat.ofNat, ite
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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
rw : ∏ a ∈ (t i).primeFactors, a = t i
⊢ ∏ a ∈ n.primeFactors with a ∣ t i, a = t i

Tactic:
rw [primeFactors_filter_dvd_of_dvd hn.ne_zero this]

Premises used: Squarefree.ne_zero, Nat.primeFactors_filter_dvd_of_dvd
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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 ∈ (t i).primeFactors, a = t i

Tactic:
prod_primeFactors_of_squarefree <| hn.squarefree_of_dvd this

Premises used: Nat.prod_primeFactors_of_squarefree, Squarefree.squarefree_of_dvd
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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 ∈ (t i).primeFactors, a = t i

Tactic:
exact prod_primeFactors_of_squarefree <| hn.squarefree_of_dvd this

Premises used: Nat.prod_primeFactors_of_squarefree, Squarefree.squarefree_of_dvd
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
Goal:
d n : ℕ
hn : Squarefree n
⊢ card (α := (a : ℕ) → a ∈ n.primeFactors → Fin d) (n.primeFactors.pi (β := fun (x : ℕ) ↦ Fin d) fun (x : ℕ) ↦ univ) =
    #(d.finMulAntidiag n)

Tactic:
apply Finset.card_bij (Nat.primeFactorsPiBij d n) (primeFactorsPiBij_img d n hn)
    (primeFactorsPiBij_inj d n) (primeFactorsPiBij_surj d n hn)

Premises used: _private.0.Nat.primeFactorsPiBij, _private.0.Nat.primeFactorsPiBij_inj, _private.0.Nat.primeFactorsPiBij_img, Finset.card_bij, _private.0.Nat.primeFactorsPiBij_surj
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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
rw₆ rw₇ : d ^ #n.primeFactors = d ^ #n.primeFactors
⊢ #(d.finMulAntidiag n) = 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]

Premises used: Finset.card_pi, ArithmeticFunction.cardDistinctFactors_apply, List.card_toFinset, Finset.prod_const, Nat.toFinset_factors, Finset.card_fin, _private.0.Nat.card_finMulAntidiag_pi
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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
rw₁ rw₂ : a 0 * a 1 * a 2 = a 0 * a 1 * a 2
⊢ a 0 * a 1 * a 2 = n

Tactic:
rw [← (mem_finMulAntidiag.mp ha).1, Fin.prod_univ_three a]

Premises used: Nat.mem_finMulAntidiag, And.left, Iff.mp, Fin.prod_univ_three
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
Goal:
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) a
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
⊢ f a ha ∈
    {x ∈ n.divisors ×ˢ n.divisors |
      match (motive := ℕ × ℕ → Prop) x with
      | (x, y) => x.lcm y = n}

Tactic:
rw [mem_filter, Finset.mem_product, mem_divisors, mem_divisors]

Premises used: Nat.mem_divisors, Finset.mem_filter, Finset.mem_product
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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

Tactic:
⟨⟨⟨?_, hn.ne_zero⟩, ⟨?_, hn.ne_zero⟩⟩, ?_⟩

Premises used: Squarefree.ne_zero, And.intro
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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
refine_3 :
  match (motive := ℕ × ℕ → Prop) f a ha with
  | (x, y) => x.lcm y = 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

Tactic:
refine ⟨⟨⟨?_, hn.ne_zero⟩, ⟨?_, hn.ne_zero⟩⟩, ?_⟩
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
Goal:
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) a
refine_1 : (a 0 * a 1, a 0 * a 2).1 ∣ a 0 * a 1 * a 2
⊢ (f a ha).1 ∣ n

Tactic:
rw [f, ← finMulAntidiag_three a ha]

Premises used: _private.0.Nat.card_pair_lcm_eq.f, Nat.finMulAntidiag_three
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
Goal:
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) a
refine_2 : (a 0 * a 1, a 0 * a 2).2 ∣ a 0 * a 1 * a 2
⊢ (f a ha).2 ∣ n

Tactic:
rw [f, ← finMulAntidiag_three a ha]

Premises used: _private.0.Nat.card_pair_lcm_eq.f, Nat.finMulAntidiag_three
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
Goal:
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) a
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
⊢ match (motive := ℕ × ℕ → Prop) f a ha with
  | (x, y) => x.lcm y = n

Tactic:
rw [f, ← finMulAntidiag_three a ha]

Premises used: _private.0.Nat.card_pair_lcm_eq.f, Nat.finMulAntidiag_three
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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).1 ∣ a 0 * a 1 * a 2

Tactic:
apply dvd_mul_right

Premises used: dvd_mul_right
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
Goal:
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) a
h : a 0 * a 1 * a 2 = (a 0 * a 1, a 0 * a 2).2 * a 1
⊢ (a 0 * a 1, a 0 * a 2).2 ∣ a 0 * a 1 * a 2

Tactic:
use a 1

Premises used: OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
Goal:
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) a
⊢ a 0 * a 1 * a 2 = (a 0 * a 1, a 0 * a 2).2 * a 1

Tactic:
ring
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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
refine_3₁ : (a 1).Coprime (a 2)
⊢ (a 0 * a 1).lcm (a 0 * a 2) = a 0 * a 1 * a 2

Tactic:
rw [lcm_mul_left, Nat.Coprime.lcm_eq_mul]

Premises used: Nat.Coprime.lcm_eq_mul, Nat.lcm_mul_left
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
Goal:
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) a
⊢ a 0 * (a 1 * a 2) = a 0 * a 1 * a 2

Tactic:
ring
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
Goal:
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) a
⊢ (a 1).Coprime (a 2)

Tactic:
coprime_of_squarefree_mul (hn.squarefree_of_dvd ?_)

Premises used: Squarefree.squarefree_of_dvd, Nat.coprime_of_squarefree_mul
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
Goal:
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) a
refine_3 : a 1 * a 2 ∣ n
⊢ (a 1).Coprime (a 2)

Tactic:
refine coprime_of_squarefree_mul (hn.squarefree_of_dvd ?_)

Premises used: Squarefree.squarefree_of_dvd, Nat.coprime_of_squarefree_mul
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
Goal:
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) a
h : n = a 1 * a 2 * a 0
⊢ a 1 * a 2 ∣ n

Tactic:
use a 0

Premises used: OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
Goal:
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) a
h : a 0 * a 1 * a 2 = a 1 * a 2 * a 0
⊢ n = a 1 * a 2 * a 0

Tactic:
rw [← finMulAntidiag_three a ha]

Premises used: Nat.finMulAntidiag_three
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
Goal:
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : Membership.mem (γ := Finset (Fin 3 → ℕ)) (finMulAntidiag 3 n) a
⊢ a 0 * a 1 * a 2 = a 1 * a 2 * a 0

Tactic:
ring
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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 0 * a 1 = b 0 * b 1

Tactic:
obtain ⟨hfab1, hfab2⟩ := Prod.mk.inj hfab

Premises used: Prod.mk.inj
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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 0 * a 2 = b 0 * b 2

Tactic:
obtain ⟨hfab1, hfab2⟩ := Prod.mk.inj hfab

Premises used: Prod.mk.inj
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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
rw₂ rw₃ : n = n
⊢ a 0 * a 1 * a 2 = a 0 * a 1 * b 2

Tactic:
rw [finMulAntidiag_three a ha, hfab1, finMulAntidiag_three b hb]

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

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]
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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 rw : a 0 * a 1 * a 2 = a 0 * a 1 * b 2
⊢ a 2 = b 2

Tactic:
rw [← mul_right_inj' <| mul_ne_zero (ne_zero_of_mem_finMulAntidiag ha 0)
      (ne_zero_of_mem_finMulAntidiag ha 1)]

Premises used: mul_right_inj', mul_ne_zero, OfNat.ofNat, Nat.ne_zero_of_mem_finMulAntidiag
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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 0 * a 1 * a 2 = a 0 * a 1 * b 2

Tactic:
hprods
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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 0 * a 1 * a 2 = a 0 * a 1 * b 2

Tactic:
exact hprods
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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 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
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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
hab2 : a 2 = b 2
⊢ a 0 * b 2 = b 0 * b 2

Tactic:
rw [hab2] at hfab2
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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
hab2 : a 2 = b 2
hfab2₁ : a 0 * b 2 = b 0 * b 2
⊢ a 0 * a 1 * a 2 = a 0 * a 1 * b 2

Tactic:
rw [hab2] at hfab2
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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
hab2 : a 2 = b 2
hfab2₁ : a 0 * b 2 = b 0 * b 2
hprods₁ : a 0 * a 1 * a 2 = a 0 * a 1 * b 2
⊢ a 2 = b 2

Tactic:
rw [hab2] at hfab2