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

State before:
d : ℕ
⊢ d.finMulAntidiagonal 1 = {fun x => 1}
Tactic:
ext f
State after:
case a
d : ℕ
f : Fin d → ℕ
⊢ f ∈ d.finMulAntidiagonal 1 ↔ f ∈ {fun x => 1}

State before:
case a
d : ℕ
f : Fin d → ℕ
⊢ f ∈ d.finMulAntidiagonal 1 ↔ f ∈ {fun x => 1}
Tactic:
simp only [mem_finMulAntidiagonal, and_true, mem_singleton]
State after:
case a
d : ℕ
f : Fin d → ℕ
⊢ ∏ i : Fin d, f i = 1 ∧ 1 ≠ 0 ↔ f = fun x => 1

State before:
case a
d : ℕ
f : Fin d → ℕ
⊢ ∏ i : Fin d, f i = 1 ∧ 1 ≠ 0 ↔ f = fun x => 1
Tactic:
constructor
State after:
case a.mp
d : ℕ
f : Fin d → ℕ
⊢ ∏ i : Fin d, f i = 1 ∧ 1 ≠ 0 → f = fun x => 1

case a.mpr
d : ℕ
f : Fin d → ℕ
⊢ (f = fun x => 1) → ∏ i : Fin d, f i = 1 ∧ 1 ≠ 0

State before:
case a.mp
d : ℕ
f : Fin d → ℕ
⊢ ∏ i : Fin d, f i = 1 ∧ 1 ≠ 0 → f = fun x => 1
Tactic:
intro ⟨hf, _⟩
State after:
case a.mp
d : ℕ
f : Fin d → ℕ
hf : ∏ i : Fin d, f i = 1
right✝ : 1 ≠ 0
⊢ f = fun x => 1

State before:
case a.mp
d : ℕ
f : Fin d → ℕ
hf : ∏ i : Fin d, f i = 1
right✝ : 1 ≠ 0
⊢ f = fun x => 1
Tactic:
ext i
State after:
case a.mp.h
d : ℕ
f : Fin d → ℕ
hf : ∏ i : Fin d, f i = 1
right✝ : 1 ≠ 0
i : Fin d
⊢ f i = 1

State before:
case a.mp.h
d : ℕ
f : Fin d → ℕ
hf : ∏ i : Fin d, f i = 1
right✝ : 1 ≠ 0
i : Fin d
⊢ f i = 1
Tactic:
rw [←Nat.dvd_one, ←hf]
State after:
case a.mp.h
d : ℕ
f : Fin d → ℕ
hf : ∏ i : Fin d, f i = 1
right✝ : 1 ≠ 0
i : Fin d
⊢ f i ∣ ∏ i : Fin d, f i

State before:
case a.mp.h
d : ℕ
f : Fin d → ℕ
hf : ∏ i : Fin d, f i = 1
right✝ : 1 ≠ 0
i : Fin d
⊢ f i ∣ ∏ i : Fin d, f i
Tactic:
exact dvd_prod_of_mem f (mem_univ _)
State after:
no goals

State before:
case a.mpr
d : ℕ
f : Fin d → ℕ
⊢ (f = fun x => 1) → ∏ i : Fin d, f i = 1 ∧ 1 ≠ 0
Tactic:
rintro rfl
State after:
case a.mpr
d : ℕ
⊢ ∏ i : Fin d, (fun x => 1) i = 1 ∧ 1 ≠ 0

State before:
case a.mpr
d : ℕ
⊢ ∏ i : Fin d, (fun x => 1) i = 1 ∧ 1 ≠ 0
Tactic:
simp only [prod_const_one, implies_true, ne_eq, one_ne_zero, not_false_eq_true,
and_self]
State after:
no goals