awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Antidiag.FinsuppEquiv
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
s : Finset ι
n : μ
f : ↥(s.finsuppAntidiag n)
hf : ((↑f : ι →₀ μ).sum fun (x : ι) (x_1 : μ) ↦ x_1) = n ∧ (↑f : ι →₀ μ).support ⊆ s
⊢ (sum (subtypeDomain (fun (x : ι) ↦ x ∈ s) (↑f : ι →₀ μ)) fun (x : ↥s) ↦ id) = n

Tactic:
simpa [sum, filter_mem_eq_inter, inter_eq_left.mpr hf.2] using hf.1

Premises used: Iff.mpr, Finsupp.sum, And.right, And.left, Finset.inter_eq_left, Finset.filter_mem_eq_inter
-- Module: Mathlib.Algebra.Order.Antidiag.FinsuppEquiv
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
s : Finset ι
n : μ
f : { P : Finsupp.{u_1, u_2} (↥s) μ // (P.sum fun (x : ↥s) ↦ id) = n }
⊢ ((↑f : ↥s →₀ μ).extendDomain (P := fun (x : ι) ↦ x ∈ s).sum fun (x : ι) (x_1 : μ) ↦ x_1) = n

Tactic:
simpa [sum] using f.2

Premises used: Finsupp.sum, Subtype.property
-- Module: Mathlib.Algebra.Order.Antidiag.FinsuppEquiv
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
s : Finset ι
n : μ
f : { P : Finsupp.{u_1, u_2} (↥s) μ // (P.sum fun (x : ↥s) ↦ id) = n }
⊢ (↑f : ↥s →₀ μ).extendDomain (P := fun (x : ι) ↦ x ∈ s).support ⊆ s

Tactic:
simp [map_eq_image, image_subset_iff]

Premises used: Finset.image_subset_iff, Finset.map_eq_image
-- Module: Mathlib.Algebra.Order.Antidiag.FinsuppEquiv
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
s : Finset ι
n : μ
f : ↥(s.finsuppAntidiag n)
⊢ s.sum (⇑(↑f : ι →₀ μ) : (a : ι) → μ) = n

Tactic:
obtain ⟨hsum, hs⟩ := mem_finsuppAntidiag.mp f.prop

Premises used: Finset.mem_finsuppAntidiag, Subtype.prop, Iff.mp
-- Module: Mathlib.Algebra.Order.Antidiag.FinsuppEquiv
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
s : Finset ι
n : μ
f : ↥(s.finsuppAntidiag n)
hsum : s.sum (⇑(↑f : ι →₀ μ) : (a : ι) → μ) = n
⊢ (↑f : ι →₀ μ).support ⊆ s

Tactic:
obtain ⟨hsum, hs⟩ := mem_finsuppAntidiag.mp f.prop

Premises used: Finset.mem_finsuppAntidiag, Subtype.prop, Iff.mp
-- Module: Mathlib.Algebra.Order.Antidiag.FinsuppEquiv
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
s : Finset ι
n : μ
f : ↥(s.finsuppAntidiag n)
hsum : s.sum (⇑(↑f : ι →₀ μ) : (a : ι) → μ) = n
hs : (↑f : ι →₀ μ).support ⊆ s
a :
  (↑((fun (f : { P : Finsupp.{u_1, u_2} (↥s) μ // (P.sum fun (x : ↥s) ↦ id) = n }) ↦
            (Subtype.mk (p := fun (x : ι →₀ μ) ↦ Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag n) x)
                ((↑f : ↥s →₀ μ).extendDomain (P := fun (x : ι) ↦ x ∈ s)) ⋯ :
              ↥(s.finsuppAntidiag n)))
          ((fun (f : ↥(s.finsuppAntidiag n)) ↦
              (Subtype.mk (p := fun (P : Finsupp.{u_1, u_2} (↥s) μ) ↦ (P.sum fun (x : ↥s) ↦ id) = n)
                  (subtypeDomain (fun (x : ι) ↦ x ∈ s) (↑f : ι →₀ μ)) ⋯ :
                { P : Finsupp.{u_1, u_2} (↥s) μ // (P.sum fun (x : ↥s) ↦ id) = n }))
            f)) :
      ι →₀ μ) =
    (↑f : ι →₀ μ)
⊢ (fun (f : { P : Finsupp.{u_1, u_2} (↥s) μ // (P.sum fun (x : ↥s) ↦ id) = n }) ↦
        (Subtype.mk (p := fun (x : ι →₀ μ) ↦ Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag n) x)
            ((↑f : ↥s →₀ μ).extendDomain (P := fun (x : ι) ↦ x ∈ s)) ⋯ :
          ↥(s.finsuppAntidiag n)))
      ((fun (f : ↥(s.finsuppAntidiag n)) ↦
          (Subtype.mk (p := fun (P : Finsupp.{u_1, u_2} (↥s) μ) ↦ (P.sum fun (x : ↥s) ↦ id) = n)
              (subtypeDomain (fun (x : ι) ↦ x ∈ s) (↑f : ι →₀ μ)) ⋯ :
            { P : Finsupp.{u_1, u_2} (↥s) μ // (P.sum fun (x : ↥s) ↦ id) = n }))
        f) =
    f

Tactic:
ext1
-- Module: Mathlib.Algebra.Order.Antidiag.FinsuppEquiv
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
s : Finset ι
n : μ
f : ↥(s.finsuppAntidiag n)
hsum : s.sum (⇑(↑f : ι →₀ μ) : (a : ι) → μ) = n
hs : (↑f : ι →₀ μ).support ⊆ s
⊢ (↑((fun (f : { P : Finsupp.{u_1, u_2} (↥s) μ // (P.sum fun (x : ↥s) ↦ id) = n }) ↦
            (Subtype.mk (p := fun (x : ι →₀ μ) ↦ Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag n) x)
                ((↑f : ↥s →₀ μ).extendDomain (P := fun (x : ι) ↦ x ∈ s)) ⋯ :
              ↥(s.finsuppAntidiag n)))
          ((fun (f : ↥(s.finsuppAntidiag n)) ↦
              (Subtype.mk (p := fun (P : Finsupp.{u_1, u_2} (↥s) μ) ↦ (P.sum fun (x : ↥s) ↦ id) = n)
                  (subtypeDomain (fun (x : ι) ↦ x ∈ s) (↑f : ι →₀ μ)) ⋯ :
                { P : Finsupp.{u_1, u_2} (↥s) μ // (P.sum fun (x : ↥s) ↦ id) = n }))
            f)) :
      ι →₀ μ) =
    (↑f : ι →₀ μ)

Tactic:
extendDomain_subtypeDomain _ hs

Premises used: Finsupp.piecewise, Finsupp.extendDomain_subtypeDomain, Finsupp.extendDomain
-- Module: Mathlib.Algebra.Order.Antidiag.FinsuppEquiv
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
s : Finset ι
n : μ
f : ↥(s.finsuppAntidiag n)
hsum : s.sum (⇑(↑f : ι →₀ μ) : (a : ι) → μ) = n
hs : (↑f : ι →₀ μ).support ⊆ s
⊢ (↑((fun (f : { P : Finsupp.{u_1, u_2} (↥s) μ // (P.sum fun (x : ↥s) ↦ id) = n }) ↦
            (Subtype.mk (p := fun (x : ι →₀ μ) ↦ Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag n) x)
                ((↑f : ↥s →₀ μ).extendDomain (P := fun (x : ι) ↦ x ∈ s)) ⋯ :
              ↥(s.finsuppAntidiag n)))
          ((fun (f : ↥(s.finsuppAntidiag n)) ↦
              (Subtype.mk (p := fun (P : Finsupp.{u_1, u_2} (↥s) μ) ↦ (P.sum fun (x : ↥s) ↦ id) = n)
                  (subtypeDomain (fun (x : ι) ↦ x ∈ s) (↑f : ι →₀ μ)) ⋯ :
                { P : Finsupp.{u_1, u_2} (↥s) μ // (P.sum fun (x : ↥s) ↦ id) = n }))
            f)) :
      ι →₀ μ) =
    (↑f : ι →₀ μ)

Tactic:
exact extendDomain_subtypeDomain _ hs

Premises used: Finsupp.extendDomain_subtypeDomain
-- Module: Mathlib.Algebra.Order.Antidiag.FinsuppEquiv
Goal:
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst : DecidableEq ι
inst_1 : AddCommMonoid μ
inst_2 : HasAntidiagonal μ
inst_3 : DecidableEq μ
s : Finset ι
n : μ
f : { P : Finsupp.{u_1, u_2} (↥s) μ // (P.sum fun (x : ↥s) ↦ id) = n }
⊢ (fun (f : ↥(s.finsuppAntidiag n)) ↦
        (Subtype.mk (p := fun (P : Finsupp.{u_1, u_2} (↥s) μ) ↦ (P.sum fun (x : ↥s) ↦ id) = n)
            (subtypeDomain (fun (x : ι) ↦ x ∈ s) (↑f : ι →₀ μ)) ⋯ :
          { P : Finsupp.{u_1, u_2} (↥s) μ // (P.sum fun (x : ↥s) ↦ id) = n }))
      ((fun (f : { P : Finsupp.{u_1, u_2} (↥s) μ // (P.sum fun (x : ↥s) ↦ id) = n }) ↦
          (Subtype.mk (p := fun (x : ι →₀ μ) ↦ Membership.mem (γ := Finset (ι →₀ μ)) (s.finsuppAntidiag n) x)
              ((↑f : ↥s →₀ μ).extendDomain (P := fun (x : ι) ↦ x ∈ s)) ⋯ :
            ↥(s.finsuppAntidiag n)))
        f) =
    f

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Antidiag.FinsuppEquiv
Goal:
ι : Type u_1
inst : DecidableEq ι
s : Finset ι
n : ℕ
f : Sym (↥s) n
a : ↥s
⊢ ((↑((Equiv.symm (s.finsuppAntidiagEquiv n) : (a : Sym (↥s) n) → ↥(s.finsuppAntidiag n)) f) : ι →₀ ℕ) : (a : ι) → ℕ)
      (↑a : ι) =
    Multiset.count a (↑f : Multiset ↥s)

Tactic:
simp [finsuppAntidiagEquiv]

Premises used: Finset.finsuppAntidiagEquiv
-- Module: Mathlib.Algebra.Order.Antidiag.FinsuppEquiv
Goal:
ι : Type u_1
inst : DecidableEq ι
s : Finset ι
n : ℕ
f : ↥(s.finsuppAntidiag n)
a : ↥s
⊢ Multiset.count a (↑((s.finsuppAntidiagEquiv n : (a : ↥(s.finsuppAntidiag n)) → Sym (↥s) n) f) : Multiset ↥s) =
    ((↑f : ι →₀ ℕ) : (a : ι) → ℕ) (↑a : ι)

Tactic:
simp [finsuppAntidiagEquiv]

Premises used: Finset.finsuppAntidiagEquiv
-- Module: Mathlib.Algebra.Order.Antidiag.FinsuppEquiv
Goal:
ι : Type u_1
inst : DecidableEq ι
s : Finset ι
n : ℕ
⊢ card (α := ι →₀ ℕ) (s.finsuppAntidiag n) = (#s + n - 1).choose n

Tactic:
simp [card_eq_of_equiv_fintype (finsuppAntidiagEquiv s n), Sym.card_sym_eq_choose]

Premises used: Sym.card_sym_eq_choose, Finset.card_eq_of_equiv_fintype, Finset.finsuppAntidiagEquiv
-- Module: Mathlib.Algebra.Order.Antidiag.FinsuppEquiv
Goal:
ι : Type u_1
inst : DecidableEq ι
s : Finset ι
n : ℕ
⊢ card (α := ι →₀ ℕ) (s.finsuppAntidiag n) = (#s).multichoose n

Tactic:
simp [card_eq_of_equiv_fintype (finsuppAntidiagEquiv s n), Sym.card_sym_eq_multichoose]

Premises used: Finset.card_eq_of_equiv_fintype, Finset.finsuppAntidiagEquiv, Sym.card_sym_eq_multichoose
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
Goal:
divisorsAntidiagonal : (n : ℕ+) → Finset (ℕ+ × ℕ+) :=
  fun (n : ℕ+) ↦
    map
      {
        toFun := fun (x : ↥(↑n : ℕ).divisorsAntidiagonal) ↦
          (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (↑x : ℕ × ℕ).1 ⋯,
            Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (↑x : ℕ × ℕ).2 ⋯),
        inj' := ⋯ }
      (↑n : ℕ).divisorsAntidiagonal.attach
n : ℕ+
x : ℕ+ × ℕ+
simp_rw :
  (∃ (a : ℕ × ℕ) (h : a ∈ (↑n : ℕ).divisorsAntidiagonal),
      (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a.1 ⋯) : ℕ) = (↑x.1 : ℕ) ∧
        (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a.2 ⋯) : ℕ) = (↑x.2 : ℕ)) ↔
    (↑(x.1 * x.2) : ℕ) = (↑n : ℕ)
⊢ x ∈ divisorsAntidiagonal n ↔ x.1 * x.2 = n

Tactic:
simp_rw [divisorsAntidiagonal, Finset.mem_map, Finset.mem_attach, Function.Embedding.coeFn_mk,
      Prod.ext_iff, true_and, ← coe_inj, Subtype.exists]

Premises used: Finset.mem_attach, Subtype.exists, Prod.ext_iff, Function.Embedding.coeFn_mk, Finset.mem_map, PNat.coe_inj, true_and
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
Goal:
divisorsAntidiagonal : (n : ℕ+) → Finset (ℕ+ × ℕ+) :=
  fun (n : ℕ+) ↦
    map
      {
        toFun := fun (x : ↥(↑n : ℕ).divisorsAntidiagonal) ↦
          (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (↑x : ℕ × ℕ).1 ⋯,
            Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (↑x : ℕ × ℕ).2 ⋯),
        inj' := ⋯ }
      (↑n : ℕ).divisorsAntidiagonal.attach
n : ℕ+
x : ℕ+ × ℕ+
⊢ (∃ (a : ℕ × ℕ) (h : a ∈ (↑n : ℕ).divisorsAntidiagonal),
      (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a.1 ⋯) : ℕ) = (↑x.1 : ℕ) ∧
        (↑(Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) a.2 ⋯) : ℕ) = (↑x.2 : ℕ)) ↔
    (↑(x.1 * x.2) : ℕ) = (↑n : ℕ)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
Goal:
divisorsAntidiagonal : (n : ℕ+) → Finset (ℕ+ × ℕ+) :=
  fun (n : ℕ+) ↦
    map
      {
        toFun := fun (x : ↥(↑n : ℕ).divisorsAntidiagonal) ↦
          (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (↑x : ℕ × ℕ).1 ⋯,
            Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) (↑x : ℕ × ℕ).2 ⋯),
        inj' := ⋯ }
      (↑n : ℕ).divisorsAntidiagonal.attach
mem_divisorsAntidiagonal : ∀ {n : ℕ+} (x : ℕ+ × ℕ+), x ∈ divisorsAntidiagonal n ↔ x.1 * x.2 = n
⊢ ∀ {n : Additive ℕ+} {a : Additive ℕ+ × Additive ℕ+},
    a ∈
        map (Function.Embedding.prodMap (Equiv.toEmbedding Additive.ofMul) (Equiv.toEmbedding Additive.ofMul))
          (divisorsAntidiagonal ((Additive.toMul : (a : Additive ℕ+) → ℕ+) n)) ↔
      a.1 + a.2 = n

Tactic:
simp [← ofMul_mul, mem_divisorsAntidiagonal]

Premises used: ofMul_mul
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
Goal:
d n : ℕ
f : Fin d → ℕ
pos :
  ∀ (h : 0 < n),
    Membership.mem (γ := Finset (Fin d → ℕ))
        (map
          (Function.Embedding.trans (Equiv.toEmbedding Additive.toMul)
              { toFun := PNat.val, inj' := PNat.coe_injective : ℕ+ ↪ ℕ }).arrowCongrRight
          (finAntidiagonal d ((Additive.ofMul : (a : ℕ+) → Additive ℕ+) (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n h))))
        f ↔
      ∏ i : Fin d, f i = n ∧ n ≠ 0
neg : ∀ (h : ¬0 < n), Membership.mem (γ := Finset (Fin d → ℕ)) ∅ f ↔ ∏ i : Fin d, f i = n ∧ n ≠ 0
⊢ Membership.mem (γ := Finset (Fin d → ℕ))
      (if hn : 0 < n then
        map
          (Function.Embedding.trans (Equiv.toEmbedding Additive.toMul)
              { toFun := PNat.val, inj' := PNat.coe_injective : ℕ+ ↪ ℕ }).arrowCongrRight
          (finAntidiagonal d ((Additive.ofMul : (a : ℕ+) → Additive ℕ+) (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n hn)))
      else ∅)
      f ↔
    ∏ i : Fin d, f i = n ∧ n ≠ 0

Tactic:
split_ifs with h
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
Goal:
d n : ℕ
f : Fin d → ℕ
h : 0 < n
pos :
  (∃ (x : (a : Fin d) → ℕ+), ∏ i : Fin d, (↑(x i) : ℕ) = n ∧ (fun (i : Fin d) ↦ (↑(x i) : ℕ)) = f) ↔
    ∏ i : Fin d, f i = n ∧ n ≠ 0
⊢ Membership.mem (γ := Finset (Fin d → ℕ))
      (map
        (Function.Embedding.trans (Equiv.toEmbedding Additive.toMul)
            { toFun := PNat.val, inj' := PNat.coe_injective : ℕ+ ↪ ℕ }).arrowCongrRight
        (finAntidiagonal d ((Additive.ofMul : (a : ℕ+) → Additive ℕ+) (Subtype.mk (p := fun (n : ℕ) ↦ 0 < n) n h))))
      f ↔
    ∏ i : Fin d, f i = n ∧ n ≠ 0

Tactic:
simp_rw [mem_map, mem_finAntidiagonal, Function.Embedding.arrowCongrRight_apply,
      Function.comp_def, Function.Embedding.trans_apply, Equiv.coe_toEmbedding,
      Function.Embedding.coeFn_mk, ← Additive.ofMul.symm_apply_eq, Additive.ofMul_symm_eq,
      toMul_sum, (Equiv.piCongrRight fun _ => Additive.ofMul).surjective.exists,
      Equiv.piCongrRight_apply, Pi.map_apply, toMul_ofMul, ← PNat.coe_inj, PNat.mk_coe,
      PNat.coe_prod]

Premises used: toMul_ofMul, Equiv.coe_toEmbedding, Function.Surjective.exists, Function.Embedding.arrowCongrRight_apply, Equiv.symm_apply_eq, toMul_sum, Function.Embedding.trans_apply, Additive.ofMul, Function.comp_def, Equiv.piCongrRight_apply, Function.Embedding.coeFn_mk, Equiv.piCongrRight, Equiv.surjective, Finset.mem_map, Finset.PNat.coe_prod, PNat.coe_inj, Pi.map_apply, Additive.ofMul_symm_eq, PNat.mk_coe, Finset.mem_finAntidiagonal
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
Goal:
d n : ℕ
f : Fin d → ℕ
h : 0 < n
pos :
  (∃ (x : (a : Fin d) → ℕ+), ∏ i : Fin d, (↑(x i) : ℕ) = n ∧ (fun (i : Fin d) ↦ (↑(x i) : ℕ)) = f) →
    ∏ i : Fin d, f i = n ∧ n ≠ 0
pos₁ :
  ∏ i : Fin d, f i = n ∧ n ≠ 0 →
    ∃ (x : (a : Fin d) → ℕ+), ∏ i : Fin d, (↑(x i) : ℕ) = n ∧ (fun (i : Fin d) ↦ (↑(x i) : ℕ)) = f
⊢ (∃ (x : (a : Fin d) → ℕ+), ∏ i : Fin d, (↑(x i) : ℕ) = n ∧ (fun (i : Fin d) ↦ (↑(x i) : ℕ)) = f) ↔
    ∏ i : Fin d, f i = n ∧ n ≠ 0

Tactic:
constructor
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
Goal:
d n : ℕ
h : 0 < n
a : (a : Fin d) → ℕ+
ha_mem : ∏ i : Fin d, (↑(a i) : ℕ) = n
⊢ ∏ i : Fin d, (fun (i : Fin d) ↦ (↑(a i) : ℕ)) i = n ∧ n ≠ 0

Tactic:
⟨ha_mem, h.ne.symm⟩

Premises used: Ne.symm, And.intro, LT.lt.ne
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
Goal:
d n : ℕ
h : 0 < n
a : (a : Fin d) → ℕ+
ha_mem : ∏ i : Fin d, (↑(a i) : ℕ) = n
⊢ ∏ i : Fin d, (fun (i : Fin d) ↦ (↑(a i) : ℕ)) i = n ∧ n ≠ 0

Tactic:
exact ⟨ha_mem, h.ne.symm⟩
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
Goal:
d : ℕ
f : Fin d → ℕ
h : LT.lt (α := ℕ) 0 (∏ i : Fin d, f i)
right : Ne (α := ℕ) (∏ i : Fin d, f i) 0
⊢ ∃ (x : (a : Fin d) → ℕ+),
    Eq (α := ℕ) (∏ i : Fin d, (↑(x i) : ℕ)) (∏ i : Fin d, f i) ∧ (fun (i : Fin d) ↦ (↑(x i) : ℕ)) = f

Tactic:
⟨fun i ↦ ⟨f i, ?_⟩, rfl, funext fun _ => rfl⟩

Premises used: Subtype.mk, funext, And.intro, Exists.intro, rfl
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
Goal:
d : ℕ
f : Fin d → ℕ
h : LT.lt (α := ℕ) 0 (∏ i : Fin d, f i)
right : Ne (α := ℕ) (∏ i : Fin d, f i) 0
pos : ∀ (i : Fin d), 0 < f i
⊢ ∃ (x : (a : Fin d) → ℕ+),
    Eq (α := ℕ) (∏ i : Fin d, (↑(x i) : ℕ)) (∏ i : Fin d, f i) ∧ (fun (i : Fin d) ↦ (↑(x i) : ℕ)) = f

Tactic:
refine ⟨fun i ↦ ⟨f i, ?_⟩, rfl, funext fun _ => rfl⟩
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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
pos : f i ≠ 0
⊢ 0 < f i

Tactic:
apply Nat.pos_of_ne_zero

Premises used: Nat.pos_of_ne_zero
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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
⊢ f i ≠ 0

Tactic:
Finset.prod_ne_zero_iff.mp h.ne.symm _ (mem_univ _)

Premises used: Finset.mem_univ, Ne.symm, Finset.prod_ne_zero_iff, Iff.mp, LT.lt.ne
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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
⊢ f i ≠ 0

Tactic:
exact Finset.prod_ne_zero_iff.mp h.ne.symm _ (mem_univ _)

Premises used: Finset.mem_univ, Ne.symm, Finset.prod_ne_zero_iff, Iff.mp, LT.lt.ne
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
Goal:
d n : ℕ
f : Fin d → ℕ
h : ¬0 < n
⊢ n = 0

Tactic:
simp only [not_lt, nonpos_iff_eq_zero] at h

Premises used: not_lt, nonpos_iff_eq_zero
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
Goal:
d n : ℕ
f : Fin d → ℕ
h : n = 0
⊢ Membership.mem (γ := Finset (Fin d → ℕ)) ∅ f ↔ ∏ i : Fin d, f i = n ∧ n ≠ 0

Tactic:
simp only [h, notMem_empty, ne_eq, not_true_eq_false, and_false]

Premises used: not_true_eq_false, ne_eq, Finset.notMem_empty, and_false
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
Goal:
d : ℕ
⊢ d.finMulAntidiag 0 = ∅

Tactic:
rfl

Premises used: dite, Nat.finMulAntidiag, rfl
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
Goal:
d : ℕ
h : ∀ (a : Fin d → ℕ), a ∈ d.finMulAntidiag 1 ↔ Membership.mem (γ := Finset (Fin d → ℕ)) {fun (x : Fin d) ↦ 1} a
⊢ d.finMulAntidiag 1 = {fun (x : Fin d) ↦ 1}

Tactic:
ext
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
Goal:
d : ℕ
a : Fin d → ℕ
h : (∀ (i : Fin d), a i = 1) ↔ a = fun (x : Fin d) ↦ 1
⊢ a ∈ d.finMulAntidiag 1 ↔ Membership.mem (γ := Finset (Fin d → ℕ)) {fun (x : Fin d) ↦ 1} a

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]

Premises used: Finset.mem_univ, Finset.mem_singleton, Nat.mem_finMulAntidiag, and_true, ne_eq, Finset.prod_eq_one_iff, forall_const, one_ne_zero, not_false_eq_true
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
Goal:
d : ℕ
a : Fin d → ℕ
⊢ (∀ (i : Fin d), a i = 1) ↔ a = fun (x : Fin d) ↦ 1

Tactic:
grind
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
Goal:
n : ℕ
hn : n ≠ 1
h :
  ∀ (a : Fin 0 → ℕ),
    Membership.mem (γ := Finset (Fin 0 → ℕ)) (finMulAntidiag 0 n) a ↔ Membership.mem (γ := Finset (Fin 0 → ℕ)) ∅ a
⊢ Eq (α := Finset (Fin 0 → ℕ)) (finMulAntidiag 0 n) ∅

Tactic:
ext
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
Goal:
n : ℕ
hn : n ≠ 1
a : Fin 0 → ℕ
⊢ Membership.mem (γ := Finset (Fin 0 → ℕ)) (finMulAntidiag 0 n) a ↔ Membership.mem (γ := Finset (Fin 0 → ℕ)) ∅ a

Tactic:
simp [hn.symm]

Premises used: Ne.symm
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
Goal:
n d : ℕ
f : Fin d → ℕ
hf : f ∈ d.finMulAntidiag n
i : Fin d
rw : ∀ (hf : ∏ i : Fin d, f i = n ∧ n ≠ 0) (i : Fin d), f i ∣ n
⊢ f i ∣ n

Tactic:
rw [mem_finMulAntidiag] at hf

Premises used: Nat.mem_finMulAntidiag
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
Goal:
n d : ℕ
f : Fin d → ℕ
hf : ∏ i : Fin d, f i = n ∧ n ≠ 0
i : Fin d
rw : f i ∣ ∏ i : Fin d, f i
⊢ f i ∣ n

Tactic:
rw [← hf.1]

Premises used: And.left
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
Goal:
n d : ℕ
f : Fin d → ℕ
hf : ∏ i : Fin d, f i = n ∧ n ≠ 0
i : Fin d
⊢ f i ∣ ∏ i : Fin d, f i

Tactic:
dvd_prod_of_mem f (mem_univ i)

Premises used: Finset.mem_univ, Finset.dvd_prod_of_mem
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
Goal:
n d : ℕ
f : Fin d → ℕ
hf : ∏ i : Fin d, f i = n ∧ n ≠ 0
i : Fin d
⊢ f i ∣ ∏ i : Fin d, f i

Tactic:
exact dvd_prod_of_mem f (mem_univ i)

Premises used: Finset.mem_univ, Finset.dvd_prod_of_mem
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
Goal:
d n : ℕ
f : Fin d → ℕ
hf : f ∈ d.finMulAntidiag n
i : Fin d
⊢ f i ≠ 0

Tactic:
ne_zero_of_dvd_ne_zero (mem_finMulAntidiag.mp hf).2 (dvd_of_mem_finMulAntidiag hf i)

Premises used: Nat.mem_finMulAntidiag, Nat.dvd_of_mem_finMulAntidiag, And.right, Iff.mp, ne_zero_of_dvd_ne_zero
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
Goal:
d n : ℕ
f : Fin d → ℕ
hf : f ∈ d.finMulAntidiag n
⊢ ∏ i : Fin d, f i = n

Tactic:
(mem_finMulAntidiag.mp hf).1

Premises used: Nat.mem_finMulAntidiag, And.left, Iff.mp
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
Goal:
d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
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
⊢ d.finMulAntidiag m =
    {f ∈ Fintype.piFinset (δ := fun (x : Fin d) ↦ ℕ) fun (x : Fin d) ↦ n.divisors | ∏ i : Fin d, f i = m}

Tactic:
ext f
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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 ↔
    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:
simp only [ne_eq,
    Fintype.mem_piFinset, mem_divisors, mem_filter]

Premises used: Fintype.mem_piFinset, Nat.mem_divisors, ne_eq, Finset.mem_filter
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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
h₁ : (∀ (a : Fin d), f a ∣ n ∧ ¬n = 0) ∧ ∏ i : Fin d, f i = m → f ∈ d.finMulAntidiag m
⊢ f ∈ d.finMulAntidiag m ↔ (∀ (a : Fin d), f a ∣ n ∧ ¬n = 0) ∧ ∏ i : Fin d, f i = m

Tactic:
constructor
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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

Tactic:
⟨?_, prod_eq_of_mem_finMulAntidiag hf⟩

Premises used: Nat.prod_eq_of_mem_finMulAntidiag, And.intro
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
Goal:
d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
f : Fin d → ℕ
hf : f ∈ d.finMulAntidiag m
h : ∀ (a : Fin d), f a ∣ n ∧ ¬n = 0
⊢ (∀ (a : Fin d), f a ∣ n ∧ ¬n = 0) ∧ ∏ i : Fin d, f i = m

Tactic:
refine ⟨?_, prod_eq_of_mem_finMulAntidiag hf⟩
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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

Tactic:
fun i => ⟨(dvd_of_mem_finMulAntidiag hf i).trans hmn, hn⟩

Premises used: Nat.dvd_of_mem_finMulAntidiag, And.intro, Dvd.dvd.trans
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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

Tactic:
exact fun i => ⟨(dvd_of_mem_finMulAntidiag hf i).trans hmn, hn⟩
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
Goal:
d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
f : Fin d → ℕ
h : (∀ (a : Fin d), f a ∣ n ∧ ¬n = 0) ∧ ∏ i : Fin d, f i = m → ∏ i : Fin d, f i = m ∧ m ≠ 0
⊢ (∀ (a : Fin d), f a ∣ n ∧ ¬n = 0) ∧ ∏ i : Fin d, f i = m → f ∈ d.finMulAntidiag m

Tactic:
rw [mem_finMulAntidiag]

Premises used: Nat.mem_finMulAntidiag
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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 → ∏ i : Fin d, f i = m ∧ m ≠ 0

Tactic:
fun ⟨_, hprod⟩ => ⟨hprod, ne_zero_of_dvd_ne_zero hn hmn⟩

Premises used: Finset.univ, Ne, Finset.prod, And, And.intro, ne_zero_of_dvd_ne_zero, OfNat.ofNat, Eq, _private.0.Nat.finMulAntidiag_eq_piFinset_divisors_filter.match_3
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
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 → ∏ i : Fin d, f i = m ∧ m ≠ 0

Tactic:
exact fun ⟨_, hprod⟩ => ⟨hprod, ne_zero_of_dvd_ne_zero hn hmn⟩
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
Goal:
d n : ℕ
i : Fin d
hd : d ≠ 1
h :
  ∀ (k : ℕ), Membership.mem (γ := Finset ℕ) (image (fun (f : Fin d → ℕ) ↦ f i) (d.finMulAntidiag n)) k ↔ k ∈ n.divisors
⊢ image (fun (f : Fin d → ℕ) ↦ f i) (d.finMulAntidiag n) = n.divisors

Tactic:
ext k
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
Goal:
d n : ℕ
i : Fin d
hd : d ≠ 1
k : ℕ
h : (∃ a ∈ d.finMulAntidiag n, a i = k) ↔ k ∣ n ∧ ¬n = 0
⊢ Membership.mem (γ := Finset ℕ) (image (fun (f : Fin d → ℕ) ↦ f i) (d.finMulAntidiag n)) k ↔ k ∈ n.divisors

Tactic:
simp only [mem_image, ne_eq, mem_divisors]

Premises used: Finset.mem_image, Nat.mem_divisors, ne_eq
-- Module: Mathlib.Algebra.Order.Antidiag.Nat
Goal:
d n : ℕ
i : Fin d
hd : d ≠ 1
k : ℕ
h : (∃ a ∈ d.finMulAntidiag n, a i = k) → k ∣ n ∧ ¬n = 0
h₁ : k ∣ n ∧ ¬n = 0 → ∃ a ∈ d.finMulAntidiag n, a i = k
⊢ (∃ a ∈ d.finMulAntidiag n, a i = k) ↔ k ∣ n ∧ ¬n = 0

Tactic:
constructor