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

State before:
n d : ℕ
f : Fin d → ℕ
hf : f ∈ d.finMulAntidiagonal n
i : Fin d
⊢ f i ∣ n
Tactic:
rw [mem_finMulAntidiagonal] at hf
State after:
n d : ℕ
f : Fin d → ℕ
hf : ∏ i : Fin d, f i = n ∧ n ≠ 0
i : Fin d
⊢ f i ∣ n

State before:
n d : ℕ
f : Fin d → ℕ
hf : ∏ i : Fin d, f i = n ∧ n ≠ 0
i : Fin d
⊢ f i ∣ n
Tactic:
rw [←hf.1]
State after:
n d : ℕ
f : Fin d → ℕ
hf : ∏ i : Fin d, f i = n ∧ n ≠ 0
i : Fin d
⊢ f i ∣ ∏ i : Fin d, f i

State before:
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)
State after:
no goals