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

State before:
n : ℕ
⊢ image (⇑(piFinTwoEquiv fun x => ℕ)) (finMulAntidiagonal 2 n) = n.divisorsAntidiagonal
Tactic:
ext x
State after:
case a
n : ℕ
x : ℕ × ℕ
⊢ x ∈ image (⇑(piFinTwoEquiv fun x => ℕ)) (finMulAntidiagonal 2 n) ↔ x ∈ n.divisorsAntidiagonal

State before:
case a
n : ℕ
x : ℕ × ℕ
⊢ x ∈ image (⇑(piFinTwoEquiv fun x => ℕ)) (finMulAntidiagonal 2 n) ↔ x ∈ n.divisorsAntidiagonal
Tactic:
simp only [piFinTwoEquiv_apply, mem_image, mem_finMulAntidiagonal, Fin.prod_univ_two, ne_eq,
  mem_divisorsAntidiagonal]
State after:
case a
n : ℕ
x : ℕ × ℕ
⊢ (∃ a, (a 0 * a 1 = n ∧ ¬n = 0) ∧ (a 0, a 1) = x) ↔ x.1 * x.2 = n ∧ ¬n = 0

State before:
case a
n : ℕ
x : ℕ × ℕ
⊢ (∃ a, (a 0 * a 1 = n ∧ ¬n = 0) ∧ (a 0, a 1) = x) ↔ x.1 * x.2 = n ∧ ¬n = 0
Tactic:
constructor
State after:
case a.mp
n : ℕ
x : ℕ × ℕ
⊢ (∃ a, (a 0 * a 1 = n ∧ ¬n = 0) ∧ (a 0, a 1) = x) → x.1 * x.2 = n ∧ ¬n = 0

case a.mpr
n : ℕ
x : ℕ × ℕ
⊢ x.1 * x.2 = n ∧ ¬n = 0 → ∃ a, (a 0 * a 1 = n ∧ ¬n = 0) ∧ (a 0, a 1) = x

State before:
case a.mp
n : ℕ
x : ℕ × ℕ
⊢ (∃ a, (a 0 * a 1 = n ∧ ¬n = 0) ∧ (a 0, a 1) = x) → x.1 * x.2 = n ∧ ¬n = 0
Tactic:
rintro ⟨y, ⟨h1, h2⟩, rfl⟩
State after:
case a.mp.intro.intro.intro
n : ℕ
y : Fin 2 → ℕ
h1 : y 0 * y 1 = n
h2 : ¬n = 0
⊢ (y 0, y 1).1 * (y 0, y 1).2 = n ∧ ¬n = 0

State before:
case a.mp.intro.intro.intro
n : ℕ
y : Fin 2 → ℕ
h1 : y 0 * y 1 = n
h2 : ¬n = 0
⊢ (y 0, y 1).1 * (y 0, y 1).2 = n ∧ ¬n = 0
Tactic:
exact ⟨h1, h2⟩
State after:
no goals

State before:
case a.mpr
n : ℕ
x : ℕ × ℕ
⊢ x.1 * x.2 = n ∧ ¬n = 0 → ∃ a, (a 0 * a 1 = n ∧ ¬n = 0) ∧ (a 0, a 1) = x
Tactic:
rintro ⟨h, hn⟩
State after:
case a.mpr.intro
n : ℕ
x : ℕ × ℕ
h : x.1 * x.2 = n
hn : ¬n = 0
⊢ ∃ a, (a 0 * a 1 = n ∧ ¬n = 0) ∧ (a 0, a 1) = x

State before:
case a.mpr.intro
n : ℕ
x : ℕ × ℕ
h : x.1 * x.2 = n
hn : ¬n = 0
⊢ ∃ a, (a 0 * a 1 = n ∧ ¬n = 0) ∧ (a 0, a 1) = x
Tactic:
use fun i => if i = 0 then x.fst else x.snd
State after:
case h
n : ℕ
x : ℕ × ℕ
h : x.1 * x.2 = n
hn : ¬n = 0
⊢ (((if 0 = 0 then x.1 else x.2) * if 1 = 0 then x.1 else x.2) = n ∧ ¬n = 0) ∧
    (if 0 = 0 then x.1 else x.2, if 1 = 0 then x.1 else x.2) = x

State before:
case h
n : ℕ
x : ℕ × ℕ
h : x.1 * x.2 = n
hn : ¬n = 0
⊢ (((if 0 = 0 then x.1 else x.2) * if 1 = 0 then x.1 else x.2) = n ∧ ¬n = 0) ∧
    (if 0 = 0 then x.1 else x.2, if 1 = 0 then x.1 else x.2) = x
Tactic:
simp (config:={decide:=true}) only [ite_true, ite_false, h, mem_univ, not_true, IsEmpty.forall_iff, forall_const, not_false_eq_true,
  and_self, Prod.mk.eta, hn]
State after:
no goals