-- Mathlib/Algebra/Order/Antidiag/Nat.lean
theorem mem_finMulAntidiag {d n : ℕ} {f : Fin d → ℕ} :
    f ∈ finMulAntidiag d n ↔ ∏ i, f i = n ∧ n ≠ 0

Proof state:
case pos.mpr.intro
d : ℕ
f : Fin d → ℕ
h : 0 < ∏ i : Fin d, f i
right✝ : ∏ i : Fin d, f i ≠ 0
i : Fin d
⊢ 0 < f i

Tactic:
apply Nat.pos_of_ne_zero

Result:
case pos.mpr.intro.a
d : ℕ
f : Fin d → ℕ
h : 0 < ∏ i : Fin d, f i
right✝ : ∏ i : Fin d, f i ≠ 0
i : Fin d
⊢ f i ≠ 0

Proof state:
case neg
d n : ℕ
f : Fin d → ℕ
h : ¬0 < n
⊢ f ∈ ∅ ↔ ∏ i : Fin d, f i = n ∧ n ≠ 0

Tactic:
simp only [not_lt, nonpos_iff_eq_zero] at h

Result:
case neg
d n : ℕ
f : Fin d → ℕ
h : n = 0
⊢ f ∈ ∅ ↔ ∏ i : Fin d, f i = n ∧ n ≠ 0

Proof state:
case pos.mp
d n : ℕ
f : Fin d → ℕ
h : 0 < n
⊢ (∃ x, ∏ i : Fin d, ↑(x i) = n ∧ (fun i => ↑(x i)) = f) → ∏ i : Fin d, f i = n ∧ n ≠ 0

Tactic:
rintro ⟨a, ha_mem, rfl⟩

Result:
case pos.mp.intro.intro
d n : ℕ
h : 0 < n
a : Fin d → ℕ+
ha_mem : ∏ i : Fin d, ↑(a i) = n
⊢ ∏ i : Fin d, (fun i => ↑(a i)) i = n ∧ n ≠ 0

Proof state:
case neg
d n : ℕ
f : Fin d → ℕ
h : n = 0
⊢ f ∈ ∅ ↔ ∏ i : Fin d, f i = n ∧ n ≠ 0

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

Result:
no goals

Proof state:
d n : ℕ
f : Fin d → ℕ
⊢ f ∈ d.finMulAntidiag n ↔ ∏ i : Fin d, f i = n ∧ n ≠ 0

Tactic:
unfold finMulAntidiag

Result:
d n : ℕ
f : Fin d → ℕ
⊢ (f ∈
      if hn : 0 < n then
        map (Additive.toMul.toEmbedding.trans { toFun := PNat.val, inj' := PNat.coe_injective }).arrowCongrRight
          (finAntidiagonal d (Additive.ofMul ⟨n, hn⟩))
      else ∅) ↔
    ∏ i : Fin d, f i = n ∧ n ≠ 0

Proof state:
case pos.mpr
d n : ℕ
f : Fin d → ℕ
h : 0 < n
⊢ ∏ i : Fin d, f i = n ∧ n ≠ 0 → ∃ x, ∏ i : Fin d, ↑(x i) = n ∧ (fun i => ↑(x i)) = f

Tactic:
rintro ⟨rfl, _⟩

Result:
case pos.mpr.intro
d : ℕ
f : Fin d → ℕ
h : 0 < ∏ i : Fin d, f i
right✝ : ∏ i : Fin d, f i ≠ 0
⊢ ∃ x, ∏ i : Fin d, ↑(x i) = ∏ i : Fin d, f i ∧ (fun i => ↑(x i)) = f

Proof state:
d n : ℕ
f : Fin d → ℕ
⊢ (f ∈
      if hn : 0 < n then
        map (Additive.toMul.toEmbedding.trans { toFun := PNat.val, inj' := PNat.coe_injective }).arrowCongrRight
          (finAntidiagonal d (Additive.ofMul ⟨n, hn⟩))
      else ∅) ↔
    ∏ i : Fin d, f i = n ∧ n ≠ 0

Tactic:
split_ifs with h

Result:
case pos
d n : ℕ
f : Fin d → ℕ
h : 0 < n
⊢ f ∈
      map (Additive.toMul.toEmbedding.trans { toFun := PNat.val, inj' := PNat.coe_injective }).arrowCongrRight
        (finAntidiagonal d (Additive.ofMul ⟨n, h⟩)) ↔
    ∏ i : Fin d, f i = n ∧ n ≠ 0

case neg
d n : ℕ
f : Fin d → ℕ
h : ¬0 < n
⊢ f ∈ ∅ ↔ ∏ i : Fin d, f i = n ∧ n ≠ 0

Proof state:
case pos.mpr.intro
d : ℕ
f : Fin d → ℕ
h : 0 < ∏ i : Fin d, f i
right✝ : ∏ i : Fin d, f i ≠ 0
⊢ ∃ x, ∏ i : Fin d, ↑(x i) = ∏ i : Fin d, f i ∧ (fun i => ↑(x i)) = f

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

Result:
case pos.mpr.intro
d : ℕ
f : Fin d → ℕ
h : 0 < ∏ i : Fin d, f i
right✝ : ∏ i : Fin d, f i ≠ 0
i : Fin d
⊢ 0 < f i

Proof state:
case pos
d n : ℕ
f : Fin d → ℕ
h : 0 < n
⊢ f ∈
      map (Additive.toMul.toEmbedding.trans { toFun := PNat.val, inj' := PNat.coe_injective }).arrowCongrRight
        (finAntidiagonal d (Additive.ofMul ⟨n, h⟩)) ↔
    ∏ 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]

Result:
case pos
d n : ℕ
f : Fin d → ℕ
h : 0 < n
⊢ (∃ x, ∏ i : Fin d, ↑(x i) = n ∧ (fun i => ↑(x i)) = f) ↔ ∏ i : Fin d, f i = n ∧ n ≠ 0

Proof state:
case pos
d n : ℕ
f : Fin d → ℕ
h : 0 < n
⊢ (∃ x, ∏ i : Fin d, ↑(x i) = n ∧ (fun i => ↑(x i)) = f) ↔ ∏ i : Fin d, f i = n ∧ n ≠ 0

Tactic:
constructor

Result:
case pos.mp
d n : ℕ
f : Fin d → ℕ
h : 0 < n
⊢ (∃ x, ∏ i : Fin d, ↑(x i) = n ∧ (fun i => ↑(x i)) = f) → ∏ i : Fin d, f i = n ∧ n ≠ 0

case pos.mpr
d n : ℕ
f : Fin d → ℕ
h : 0 < n
⊢ ∏ i : Fin d, f i = n ∧ n ≠ 0 → ∃ x, ∏ i : Fin d, ↑(x i) = n ∧ (fun i => ↑(x i)) = f

Proof state:
case pos.mpr.intro.a
d : ℕ
f : Fin d → ℕ
h : 0 < ∏ i : Fin d, f i
right✝ : ∏ 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 _)

Result:
no goals

Proof state:
case pos.mp.intro.intro
d n : ℕ
h : 0 < n
a : Fin d → ℕ+
ha_mem : ∏ i : Fin d, ↑(a i) = n
⊢ ∏ i : Fin d, (fun i => ↑(a i)) i = n ∧ n ≠ 0

Tactic:
exact ⟨ha_mem, h.ne.symm⟩

Result:
no goals