n : ℕ
p q : ℕ × ℕ
hp : p ∈ antidiagonal n
hq : q ∈ antidiagonal n
h : p.fst = q.fst
⊢ q.fst + p.snd = q.fst + q.snd
n : ℕ
p q : ℕ × ℕ
hp : p ∈ antidiagonal n
hq : q ∈ antidiagonal n
⊢ p = q ↔ p.fst = q.fst
refine' ⟨congr_arg Prod.fst, fun h ↦ Prod.ext h ((add_right_inj q.fst).mp _)⟩
n : ℕ
p q : ℕ × ℕ
hp : p.fst + p.snd = n
hq : q.fst + q.snd = n
h : p.fst = q.fst
⊢ q.fst + p.snd = q.fst + q.snd
n : ℕ
p q : ℕ × ℕ
hp : p ∈ antidiagonal n
hq : q ∈ antidiagonal n
h : p.fst = q.fst
⊢ q.fst + p.snd = q.fst + q.snd
rw [mem_antidiagonal] at hp hq
no goals
n : ℕ
p q : ℕ × ℕ
hp : p.fst + p.snd = n
hq : q.fst + q.snd = n
h : p.fst = q.fst
⊢ q.fst + p.snd = q.fst + q.snd
rw [hq, ← h, hp]