α✝ : Type ?u.61826
inst✝⁴ : LinearOrderedField α✝
inst✝³ : Archimedean α✝
β : Type ?u.61890
inst✝² : Ring β
abv : β → α✝
inst✝¹ : IsAbsoluteValue abv
α : Type u_1
inst✝ : AddCommMonoid α
n : ℕ
f : ℕ → ℕ → α
⊢ ∑ x in Finset.sigma (range n) fun m => range (m + 1), f x.snd (x.fst - x.snd) =
    ∑ x in Finset.sigma (range n) fun m => range (n - m), f x.fst x.snd
α✝ : Type ?u.61826
inst✝⁴ : LinearOrderedField α✝
inst✝³ : Archimedean α✝
β : Type ?u.61890
inst✝² : Ring β
abv : β → α✝
inst✝¹ : IsAbsoluteValue abv
α : Type u_1
inst✝ : AddCommMonoid α
n : ℕ
f : ℕ → ℕ → α
⊢ ∑ m in range n, ∑ k in range (m + 1), f k (m - k) = ∑ m in range n, ∑ k in range (n - m), f m k
rw [sum_sigma', sum_sigma']
no goals
α✝ : Type ?u.61826
inst✝⁴ : LinearOrderedField α✝
inst✝³ : Archimedean α✝
β : Type ?u.61890
inst✝² : Ring β
abv : β → α✝
inst✝¹ : IsAbsoluteValue abv
α : Type u_1
inst✝ : AddCommMonoid α
n : ℕ
f : ℕ → ℕ → α
⊢ ∑ x in Finset.sigma (range n) fun m => range (m + 1), f x.snd (x.fst - x.snd) =
    ∑ x in Finset.sigma (range n) fun m => range (n - m), f x.fst x.snd
exact
  sum_bij (fun a _ => ⟨a.2, a.1 - a.2⟩)
    (fun a ha =>
      have h₁ : a.1 < n := mem_range.1 (mem_sigma.1 ha).1
      have h₂ : a.2 < Nat.succ a.1 := mem_range.1 (mem_sigma.1 ha).2
      mem_sigma.2
        ⟨mem_range.2 (lt_of_lt_of_le h₂ h₁),
          mem_range.2 ((tsub_lt_tsub_iff_right (Nat.le_of_lt_succ h₂)).2 h₁)⟩)
    (fun _ _ => rfl)
    (fun ⟨a₁, a₂⟩ ⟨b₁, b₂⟩ ha hb h =>
      have ha : a₁ < n ∧ a₂ ≤ a₁ :=
        ⟨mem_range.1 (mem_sigma.1 ha).1, Nat.le_of_lt_succ (mem_range.1 (mem_sigma.1 ha).2)⟩
      have hb : b₁ < n ∧ b₂ ≤ b₁ :=
        ⟨mem_range.1 (mem_sigma.1 hb).1, Nat.le_of_lt_succ (mem_range.1 (mem_sigma.1 hb).2)⟩
      have h : a₂ = b₂ ∧ _ := by simpa using h
      have h' : a₁ = b₁ - b₂ + a₂ := (tsub_eq_iff_eq_add_of_le ha.2).1 (eq_of_heq h.2)
      Sigma.mk.inj_iff.2 ⟨tsub_add_cancel_of_le hb.2 ▸ h'.symm ▸ h.1 ▸ rfl, heq_of_eq h.1⟩)
    fun ⟨a₁, a₂⟩ ha =>
    have ha : a₁ < n ∧ a₂ < n - a₁ :=
      ⟨mem_range.1 (mem_sigma.1 ha).1, mem_range.1 (mem_sigma.1 ha).2⟩
    ⟨⟨a₂ + a₁, a₁⟩,
      ⟨mem_sigma.2
          ⟨mem_range.2 (lt_tsub_iff_right.1 ha.2),
            mem_range.2 (Nat.lt_succ_of_le (Nat.le_add_left _ _))⟩,
        Sigma.mk.inj_iff.2 ⟨rfl, heq_of_eq (add_tsub_cancel_right _ _).symm⟩⟩⟩
no goals
α✝ : Type ?u.61826
inst✝⁴ : LinearOrderedField α✝
inst✝³ : Archimedean α✝
β : Type ?u.61890
inst✝² : Ring β
abv : β → α✝
inst✝¹ : IsAbsoluteValue abv
α : Type u_1
inst✝ : AddCommMonoid α
n : ℕ
f : ℕ → ℕ → α
x✝¹ x✝ : (_ : ℕ) × ℕ
a₁ a₂ : ℕ
ha✝ : { fst := a₁, snd := a₂ } ∈ Finset.sigma (range n) fun m => range (m + 1)
b₁ b₂ : ℕ
hb✝ : { fst := b₁, snd := b₂ } ∈ Finset.sigma (range n) fun m => range (m + 1)
h :
  (fun a x => { fst := a.snd, snd := a.fst - a.snd }) { fst := a₁, snd := a₂ } ha✝ =
    (fun a x => { fst := a.snd, snd := a.fst - a.snd }) { fst := b₁, snd := b₂ } hb✝
ha : a₁ < n ∧ a₂ ≤ a₁
hb : b₁ < n ∧ b₂ ≤ b₁
⊢ a₂ = b₂ ∧ HEq (a₁ - a₂) (b₁ - b₂)
simpa using h