-- Mathlib/Algebra/Order/Antidiag/Nat.lean
lemma image_apply_finMulAntidiag {d n : ℕ} {i : Fin d} (hd : d ≠ 1) :
    (finMulAntidiag d n).image (fun f => f i) = divisors n

Proof state:
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

Result:
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

Proof state:
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
⊢ 2 ≤ d

Tactic:
obtain rfl | hd' := eq_or_ne d 0

Result:
case inl
k r : ℕ
hn : ¬k * r = 0
i : Fin 0
hd : 0 ≠ 1
⊢ 2 ≤ 0

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

Proof state:
d : ℕ
i : Fin d
hd : d ≠ 1
k r : ℕ
hn : ¬k * r = 0
⊢ Nontrivial (Fin d)

Tactic:
rw [Fin.nontrivial_iff_two_le]

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

Proof state:
case h.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

Result:
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, (fun j => if j = i then k else if j = i' then r else 1) i_1 = k * r ∧ k * r ≠ 0) ∧
    (fun j => if j = i then k else if j = i' then r else 1) i = k

Proof state:
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:
exact ⟨by ring, hn⟩

Result:
no goals

Proof state:
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

Result:
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

Proof state:
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]

Result:
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

Proof state:
case h.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

Result:
case h.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

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

Tactic:
simp_rw [mem_finMulAntidiag]

Result:
case h.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

Proof state:
case h.mp.intro.intro
d n : ℕ
i : Fin d
hd : d ≠ 1
f : Fin d → ℕ
hf : f ∈ d.finMulAntidiag n
⊢ f i ∣ n ∧ ¬n = 0

Tactic:
exact ⟨dvd_of_mem_finMulAntidiag hf _, (mem_finMulAntidiag.mp hf).2⟩

Result:
no goals

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

Tactic:
omega

Result:
no goals

Proof state:
d n : ℕ
i : Fin d
hd : d ≠ 1
⊢ image (fun f => f i) (d.finMulAntidiag n) = n.divisors

Tactic:
ext k

Result:
case h
d n : ℕ
i : Fin d
hd : d ≠ 1
k : ℕ
⊢ k ∈ image (fun f => f i) (d.finMulAntidiag n) ↔ k ∈ n.divisors

Proof state:
case h.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⟩

Result:
case h.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

Proof state:
case h
d n : ℕ
i : Fin d
hd : d ≠ 1
k : ℕ
⊢ (∃ a ∈ d.finMulAntidiag n, a i = k) ↔ k ∣ n ∧ ¬n = 0

Tactic:
constructor

Result:
case h.mp
d n : ℕ
i : Fin d
hd : d ≠ 1
k : ℕ
⊢ (∃ a ∈ d.finMulAntidiag n, a i = k) → k ∣ n ∧ ¬n = 0

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

Proof state:
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 : Fin d, if x = i then k else if x = i' then r else 1) = k * r ∧ k * r ≠ 0

Tactic:
rw [← Finset.mul_prod_erase (h := mem_univ i),
  ← Finset.mul_prod_erase (a := i')]

Result:
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

Proof state:
case h.mp
d n : ℕ
i : Fin d
hd : d ≠ 1
k : ℕ
⊢ (∃ a ∈ d.finMulAntidiag n, a i = k) → k ∣ n ∧ ¬n = 0

Tactic:
rintro ⟨f, hf, rfl⟩

Result:
case h.mp.intro.intro
d n : ℕ
i : Fin d
hd : d ≠ 1
f : Fin d → ℕ
hf : f ∈ d.finMulAntidiag n
⊢ f i ∣ n ∧ ¬n = 0

Proof state:
case inl
k r : ℕ
hn : ¬k * r = 0
i : Fin 0
hd : 0 ≠ 1
⊢ 2 ≤ 0

Tactic:
exact i.elim0

Result:
no goals

Proof state:
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]

Result:
no goals

Proof state:
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 _⟩

Result:
no goals

Proof state:
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, (fun j => if j = i then k else if j = i' then r else 1) i_1 = k * r ∧ k * r ≠ 0) ∧
    (fun j => if j = i then k else if j = i' then r else 1) i = k

Tactic:
simp only [ite_true, and_true, hn]

Result:
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 : Fin d, if x = i then k else if x = i' then r else 1) = k * r ∧ k * r ≠ 0

Proof state:
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

Result:
no goals

Proof state:
case h
d n : ℕ
i : Fin d
hd : d ≠ 1
k : ℕ
⊢ k ∈ image (fun f => f i) (d.finMulAntidiag n) ↔ k ∈ n.divisors

Tactic:
simp only [mem_image, ne_eq, mem_divisors, Nat.isUnit_iff]

Result:
case h
d n : ℕ
i : Fin d
hd : d ≠ 1
k : ℕ
⊢ (∃ a ∈ d.finMulAntidiag n, a i = k) ↔ k ∣ n ∧ ¬n = 0