Theorem: Nat.finMulAntidiagonal_univ_eq (PrimeNumberTheoremAnd/Mathlib/Data/Nat/FinMulAntidiagonal.lean)

State before:
d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
⊢ d.finMulAntidiagonal m = filter (fun f => ∏ i : Fin d, f i = m) (Fintype.piFinset fun x => n.divisors)
Tactic:
ext f
State after:
case a
d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
f : Fin d → ℕ
⊢ f ∈ d.finMulAntidiagonal m ↔ f ∈ filter (fun f => ∏ i : Fin d, f i = m) (Fintype.piFinset fun x => n.divisors)

State before:
case a
d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
f : Fin d → ℕ
⊢ f ∈ d.finMulAntidiagonal m ↔ f ∈ filter (fun f => ∏ i : Fin d, f i = m) (Fintype.piFinset fun x => n.divisors)
Tactic:
simp only [mem_univ, not_true, IsEmpty.forall_iff, implies_true, ne_eq, true_and,
  Fintype.mem_piFinset, mem_divisors, Nat.isUnit_iff, mem_filter]
State after:
case a
d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
f : Fin d → ℕ
⊢ f ∈ d.finMulAntidiagonal m ↔ (∀ (a : Fin d), f a ∣ n ∧ ¬n = 0) ∧ ∏ i : Fin d, f i = m

State before:
case a
d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
f : Fin d → ℕ
⊢ f ∈ d.finMulAntidiagonal m ↔ (∀ (a : Fin d), f a ∣ n ∧ ¬n = 0) ∧ ∏ i : Fin d, f i = m
Tactic:
constructor
State after:
case a.mp
d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
f : Fin d → ℕ
⊢ f ∈ d.finMulAntidiagonal m → (∀ (a : Fin d), f a ∣ n ∧ ¬n = 0) ∧ ∏ i : Fin d, f i = m

case a.mpr
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 → f ∈ d.finMulAntidiagonal m

State before:
case a.mp
d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
f : Fin d → ℕ
⊢ f ∈ d.finMulAntidiagonal m → (∀ (a : Fin d), f a ∣ n ∧ ¬n = 0) ∧ ∏ i : Fin d, f i = m
Tactic:
intro hf
State after:
case a.mp
d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
f : Fin d → ℕ
hf : f ∈ d.finMulAntidiagonal m
⊢ (∀ (a : Fin d), f a ∣ n ∧ ¬n = 0) ∧ ∏ i : Fin d, f i = m

State before:
case a.mp
d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
f : Fin d → ℕ
hf : f ∈ d.finMulAntidiagonal m
⊢ (∀ (a : Fin d), f a ∣ n ∧ ¬n = 0) ∧ ∏ i : Fin d, f i = m
Tactic:
refine ⟨?_, prod_eq_of_mem_finMulAntidiagonal hf⟩
State after:
case a.mp
d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
f : Fin d → ℕ
hf : f ∈ d.finMulAntidiagonal m
⊢ ∀ (a : Fin d), f a ∣ n ∧ ¬n = 0

State before:
case a.mp
d m n : ℕ
hmn : m ∣ n
hn : n ≠ 0
f : Fin d → ℕ
hf : f ∈ d.finMulAntidiagonal m
⊢ ∀ (a : Fin d), f a ∣ n ∧ ¬n = 0
Tactic:
exact fun i => ⟨(dvd_of_mem_finMulAntidiagonal hf i).trans hmn, hn⟩
State after:
no goals

State before:
case a.mpr
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 → f ∈ d.finMulAntidiagonal m
Tactic:
rw [mem_finMulAntidiagonal]
State after:
case a.mpr
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

State before:
case a.mpr
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⟩
State after:
no goals