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

State before:
d n : ℕ
i : Fin d
hd : d ≠ 1
⊢ image (fun f => f i) (d.finMulAntidiagonal n) = n.divisors
Tactic:
ext k
State after:
case a
d n : ℕ
i : Fin d
hd : d ≠ 1
k : ℕ
⊢ k ∈ image (fun f => f i) (d.finMulAntidiagonal n) ↔ k ∈ n.divisors

State before:
case a
d n : ℕ
i : Fin d
hd : d ≠ 1
k : ℕ
⊢ k ∈ image (fun f => f i) (d.finMulAntidiagonal n) ↔ k ∈ n.divisors
Tactic:
simp only [mem_image, ne_eq, mem_divisors, Nat.isUnit_iff]
State after:
case a
d n : ℕ
i : Fin d
hd : d ≠ 1
k : ℕ
⊢ (∃ a ∈ d.finMulAntidiagonal n, a i = k) ↔ k ∣ n ∧ ¬n = 0

State before:
case a
d n : ℕ
i : Fin d
hd : d ≠ 1
k : ℕ
⊢ (∃ a ∈ d.finMulAntidiagonal n, a i = k) ↔ k ∣ n ∧ ¬n = 0
Tactic:
constructor
State after:
case a.mp
d n : ℕ
i : Fin d
hd : d ≠ 1
k : ℕ
⊢ (∃ a ∈ d.finMulAntidiagonal n, a i = k) → k ∣ n ∧ ¬n = 0

case a.mpr
d n : ℕ
i : Fin d
hd : d ≠ 1
k : ℕ
⊢ k ∣ n ∧ ¬n = 0 → ∃ a ∈ d.finMulAntidiagonal n, a i = k

State before:
case a.mp
d n : ℕ
i : Fin d
hd : d ≠ 1
k : ℕ
⊢ (∃ a ∈ d.finMulAntidiagonal n, a i = k) → k ∣ n ∧ ¬n = 0
Tactic:
rintro ⟨f, hf, rfl⟩
State after:
case a.mp.intro.intro
d n : ℕ
i : Fin d
hd : d ≠ 1
f : Fin d → ℕ
hf : f ∈ d.finMulAntidiagonal n
⊢ f i ∣ n ∧ ¬n = 0

State before:
case a.mp.intro.intro
d n : ℕ
i : Fin d
hd : d ≠ 1
f : Fin d → ℕ
hf : f ∈ d.finMulAntidiagonal n
⊢ f i ∣ n ∧ ¬n = 0
Tactic:
refine ⟨dvd_of_mem_finMulAntidiagonal hf _, (mem_finMulAntidiagonal.mp hf).2⟩
State after:
no goals

State before:
case a.mpr
d n : ℕ
i : Fin d
hd : d ≠ 1
k : ℕ
⊢ k ∣ n ∧ ¬n = 0 → ∃ a ∈ d.finMulAntidiagonal n, a i = k
Tactic:
simp_rw [mem_finMulAntidiagonal]
State after:
case a.mpr
d n : ℕ
i : Fin d
hd : d ≠ 1
k : ℕ
⊢ k ∣ n ∧ ¬n = 0 → ∃ a, (∏ i : Fin d, a i = n ∧ n ≠ 0) ∧ a i = k

State before:
case a.mpr
d n : ℕ
i : Fin d
hd : d ≠ 1
k : ℕ
⊢ k ∣ n ∧ ¬n = 0 → ∃ a, (∏ i : Fin d, a i = n ∧ n ≠ 0) ∧ a i = k
Tactic:
rintro ⟨⟨r, rfl⟩, hn⟩
State after:
case a.mpr.intro.intro
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
⊢ ∃ a, (∏ i : Fin d, a i = k * r ∧ k * r ≠ 0) ∧ a i = k

State before:
case a.mpr.intro.intro
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hs : Nontrivial (Fin d)
⊢ ∃ a, (∏ i : Fin d, a i = k * r ∧ k * r ≠ 0) ∧ a i = k
Tactic:
obtain ⟨i', hi_ne⟩ := exists_ne i
State after:
case a.mpr.intro.intro.intro
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hs : Nontrivial (Fin d)
i' : Fin d
hi_ne : i' ≠ i
⊢ ∃ a, (∏ i : Fin d, a i = k * r ∧ k * r ≠ 0) ∧ a i = k

State before:
case a.mpr.intro.intro.intro
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hs : Nontrivial (Fin d)
i' : Fin d
hi_ne : i' ≠ i
⊢ ∃ a, (∏ i : Fin d, a i = k * r ∧ k * r ≠ 0) ∧ a i = k
Tactic:
use fun j => if j = i then k else if j = i' then r else 1
State after:
case h
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hs : Nontrivial (Fin d)
i' : Fin d
hi_ne : i' ≠ i
⊢ ((∏ i_1 : Fin d, if i_1 = i then k else if i_1 = i' then r else 1) = k * r ∧ k * r ≠ 0) ∧
    (if i = i then k else if i = i' then r else 1) = k

State before:
case h
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hs : Nontrivial (Fin d)
i' : Fin d
hi_ne : i' ≠ i
⊢ ((∏ i_1 : Fin d, if i_1 = i then k else if i_1 = i' then r else 1) = k * r ∧ k * r ≠ 0) ∧
    (if i = i then k else if i = i' then r else 1) = k
Tactic:
simp only [ite_true, and_true, hn]
State after:
case h
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hs : Nontrivial (Fin d)
i' : Fin d
hi_ne : i' ≠ i
⊢ (∏ i_1 : Fin d, if i_1 = i then k else if i_1 = i' then r else 1) = k * r ∧ k * r ≠ 0

State before:
case h
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hs : Nontrivial (Fin d)
i' : Fin d
hi_ne : i' ≠ i
⊢ (∏ i_1 : Fin d, if i_1 = i then k else if i_1 = i' then r else 1) = k * r ∧ k * r ≠ 0
Tactic:
rw [←Finset.mul_prod_erase (a:=i) (h:=mem_univ _),
  ←Finset.mul_prod_erase (a:= i')]
State after:
case h
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hs : Nontrivial (Fin d)
i' : Fin d
hi_ne : i' ≠ i
⊢ (if i = i then k else if i = i' then r else 1) *
        ((if i' = i then k else if i' = i' then r else 1) *
          ∏ x ∈ (univ.erase i).erase i', if x = i then k else if x = i' then r else 1) =
      k * r ∧
    k * r ≠ 0

case h.h
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hs : Nontrivial (Fin d)
i' : Fin d
hi_ne : i' ≠ i
⊢ i' ∈ univ.erase i

State before:
case h.h
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hs : Nontrivial (Fin d)
i' : Fin d
hi_ne : i' ≠ i
⊢ i' ∈ univ.erase i
Tactic:
exact mem_erase.mpr ⟨hi_ne, mem_univ _⟩
State after:
no goals

State before:
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
⊢ Nontrivial (Fin d)
Tactic:
rw[Fin.nontrivial_iff_two_le]
State after:
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
⊢ 2 ≤ d

State before:
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
⊢ 2 ≤ d
Tactic:
by_cases hd' : d = 0
State after:
case pos
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hd' : d = 0
⊢ 2 ≤ d

case neg
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hd' : ¬d = 0
⊢ 2 ≤ d

State before:
case neg
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hd' : ¬d = 0
⊢ 2 ≤ d
Tactic:
omega
State after:
no goals

State before:
case pos
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hd' : d = 0
⊢ 2 ≤ d
Tactic:
subst hd'
State after:
case pos
k r : ℕ
hn : ¬k * r = 0
i : Fin 0
hd : 0 ≠ 1
⊢ 2 ≤ 0

State before:
case pos
k r : ℕ
hn : ¬k * r = 0
i : Fin 0
hd : 0 ≠ 1
⊢ 2 ≤ 0
Tactic:
apply Fin.isEmpty.elim' i
State after:
no goals

State before:
case h
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hs : Nontrivial (Fin d)
i' : Fin d
hi_ne : i' ≠ i
⊢ (if i = i then k else if i = i' then r else 1) *
        ((if i' = i then k else if i' = i' then r else 1) *
          ∏ x ∈ (univ.erase i).erase i', if x = i then k else if x = i' then r else 1) =
      k * r ∧
    k * r ≠ 0
Tactic:
rw [if_neg hi_ne, if_pos rfl, if_pos rfl, prod_eq_one]
State after:
case h
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hs : Nontrivial (Fin d)
i' : Fin d
hi_ne : i' ≠ i
⊢ k * (r * 1) = k * r ∧ k * r ≠ 0

case h
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hs : Nontrivial (Fin d)
i' : Fin d
hi_ne : i' ≠ i
⊢ ∀ x ∈ (univ.erase i).erase i', (if x = i then k else if x = i' then r else 1) = 1

State before:
case h
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hs : Nontrivial (Fin d)
i' : Fin d
hi_ne : i' ≠ i
⊢ ∀ x ∈ (univ.erase i).erase i', (if x = i then k else if x = i' then r else 1) = 1
Tactic:
intro j hj
State after:
case h
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hs : Nontrivial (Fin d)
i' : Fin d
hi_ne : i' ≠ i
j : Fin d
hj : j ∈ (univ.erase i).erase i'
⊢ (if j = i then k else if j = i' then r else 1) = 1

State before:
case h
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hs : Nontrivial (Fin d)
i' : Fin d
hi_ne : i' ≠ i
j : Fin d
hj : j ∈ (univ.erase i).erase i'
⊢ (if j = i then k else if j = i' then r else 1) = 1
Tactic:
simp only [mem_erase, ne_eq, mem_univ, and_true] at hj
State after:
case h
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hs : Nontrivial (Fin d)
i' : Fin d
hi_ne : i' ≠ i
j : Fin d
hj : ¬j = i' ∧ ¬j = i
⊢ (if j = i then k else if j = i' then r else 1) = 1

State before:
case h
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hs : Nontrivial (Fin d)
i' : Fin d
hi_ne : i' ≠ i
j : Fin d
hj : ¬j = i' ∧ ¬j = i
⊢ (if j = i then k else if j = i' then r else 1) = 1
Tactic:
rw [if_neg hj.1, if_neg hj.2]
State after:
no goals

State before:
case h
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hs : Nontrivial (Fin d)
i' : Fin d
hi_ne : i' ≠ i
⊢ k * (r * 1) = k * r ∧ k * r ≠ 0
Tactic:
refine ⟨by ring, hn⟩
State after:
no goals

State before:
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
hs : Nontrivial (Fin d)
i' : Fin d
hi_ne : i' ≠ i
⊢ k * (r * 1) = k * r
Tactic:
ring
State after:
no goals