[GOAL]
α : Type u
inst✝ : DecidableEq α
f : α →₀ ℕ
p : (α →₀ ℕ) × (α →₀ ℕ)
⊢ p ∈ antidiagonal f ↔ p.fst + p.snd = f
[PROOFSTEP]
rcases p with ⟨p₁, p₂⟩
[GOAL]
case mk
α : Type u
inst✝ : DecidableEq α
f p₁ p₂ : α →₀ ℕ
⊢ (p₁, p₂) ∈ antidiagonal f ↔ (p₁, p₂).fst + (p₁, p₂).snd = f
[PROOFSTEP]
simp [antidiagonal, antidiagonal', ← and_assoc, Multiset.toFinsupp_eq_iff, ← Multiset.toFinsupp_eq_iff (f := f)]
[GOAL]
α : Type u
inst✝ : DecidableEq α
n : α →₀ ℕ
f : (α →₀ ℕ) × (α →₀ ℕ)
⊢ Prod.swap f ∈ antidiagonal n ↔ f ∈ antidiagonal n
[PROOFSTEP]
simp only [mem_antidiagonal, add_comm, Prod.swap]
[GOAL]
α : Type u
inst✝ : DecidableEq α
f g : α →₀ ℕ
D : (p : (α →₀ ℕ) × (α →₀ ℕ)) → Decidable (p.fst = g)
⊢ Finset.filter (fun p => p.fst = g) (antidiagonal f) = if g ≤ f then {(g, f - g)} else ∅
[PROOFSTEP]
ext ⟨a, b⟩
[GOAL]
case a.mk
α : Type u
inst✝ : DecidableEq α
f g : α →₀ ℕ
D : (p : (α →₀ ℕ) × (α →₀ ℕ)) → Decidable (p.fst = g)
a b : α →₀ ℕ
⊢ (a, b) ∈ Finset.filter (fun p => p.fst = g) (antidiagonal f) ↔ (a, b) ∈ if g ≤ f then {(g, f - g)} else ∅
[PROOFSTEP]
suffices a = g → (a + b = f ↔ g ≤ f ∧ b = f - g) by
  simpa [apply_ite (fun f ↦ (a, b) ∈ f), mem_filter, mem_antidiagonal, mem_singleton, Prod.mk.inj_iff, ← and_assoc,
    @and_right_comm _ (a = _), and_congr_left_iff]
[GOAL]
α : Type u
inst✝ : DecidableEq α
f g : α →₀ ℕ
D : (p : (α →₀ ℕ) × (α →₀ ℕ)) → Decidable (p.fst = g)
a b : α →₀ ℕ
this : a = g → (a + b = f ↔ g ≤ f ∧ b = f - g)
⊢ (a, b) ∈ Finset.filter (fun p => p.fst = g) (antidiagonal f) ↔ (a, b) ∈ if g ≤ f then {(g, f - g)} else ∅
[PROOFSTEP]
simpa [apply_ite (fun f ↦ (a, b) ∈ f), mem_filter, mem_antidiagonal, mem_singleton, Prod.mk.inj_iff, ← and_assoc,
  @and_right_comm _ (a = _), and_congr_left_iff]
[GOAL]
case a.mk
α : Type u
inst✝ : DecidableEq α
f g : α →₀ ℕ
D : (p : (α →₀ ℕ) × (α →₀ ℕ)) → Decidable (p.fst = g)
a b : α →₀ ℕ
⊢ a = g → (a + b = f ↔ g ≤ f ∧ b = f - g)
[PROOFSTEP]
rintro rfl
[GOAL]
case a.mk
α : Type u
inst✝ : DecidableEq α
f a b : α →₀ ℕ
D : (p : (α →₀ ℕ) × (α →₀ ℕ)) → Decidable (p.fst = a)
⊢ a + b = f ↔ a ≤ f ∧ b = f - a
[PROOFSTEP]
constructor
[GOAL]
case a.mk.mp
α : Type u
inst✝ : DecidableEq α
f a b : α →₀ ℕ
D : (p : (α →₀ ℕ) × (α →₀ ℕ)) → Decidable (p.fst = a)
⊢ a + b = f → a ≤ f ∧ b = f - a
[PROOFSTEP]
rintro rfl
[GOAL]
case a.mk.mp
α : Type u
inst✝ : DecidableEq α
a b : α →₀ ℕ
D : (p : (α →₀ ℕ) × (α →₀ ℕ)) → Decidable (p.fst = a)
⊢ a ≤ a + b ∧ b = a + b - a
[PROOFSTEP]
exact ⟨le_add_right le_rfl, (add_tsub_cancel_left _ _).symm⟩
[GOAL]
case a.mk.mpr
α : Type u
inst✝ : DecidableEq α
f a b : α →₀ ℕ
D : (p : (α →₀ ℕ) × (α →₀ ℕ)) → Decidable (p.fst = a)
⊢ a ≤ f ∧ b = f - a → a + b = f
[PROOFSTEP]
rintro ⟨h, rfl⟩
[GOAL]
case a.mk.mpr.intro
α : Type u
inst✝ : DecidableEq α
f a : α →₀ ℕ
D : (p : (α →₀ ℕ) × (α →₀ ℕ)) → Decidable (p.fst = a)
h : a ≤ f
⊢ a + (f - a) = f
[PROOFSTEP]
exact add_tsub_cancel_of_le h
[GOAL]
α : Type u
inst✝ : DecidableEq α
f g : α →₀ ℕ
D : (p : (α →₀ ℕ) × (α →₀ ℕ)) → Decidable (p.snd = g)
⊢ Finset.filter (fun p => p.snd = g) (antidiagonal f) = if g ≤ f then {(f - g, g)} else ∅
[PROOFSTEP]
ext ⟨a, b⟩
[GOAL]
case a.mk
α : Type u
inst✝ : DecidableEq α
f g : α →₀ ℕ
D : (p : (α →₀ ℕ) × (α →₀ ℕ)) → Decidable (p.snd = g)
a b : α →₀ ℕ
⊢ (a, b) ∈ Finset.filter (fun p => p.snd = g) (antidiagonal f) ↔ (a, b) ∈ if g ≤ f then {(f - g, g)} else ∅
[PROOFSTEP]
suffices b = g → (a + b = f ↔ g ≤ f ∧ a = f - g) by
  simpa [apply_ite (fun f ↦ (a, b) ∈ f), mem_filter, mem_antidiagonal, mem_singleton, Prod.mk.inj_iff, ← and_assoc,
    and_congr_left_iff]
[GOAL]
α : Type u
inst✝ : DecidableEq α
f g : α →₀ ℕ
D : (p : (α →₀ ℕ) × (α →₀ ℕ)) → Decidable (p.snd = g)
a b : α →₀ ℕ
this : b = g → (a + b = f ↔ g ≤ f ∧ a = f - g)
⊢ (a, b) ∈ Finset.filter (fun p => p.snd = g) (antidiagonal f) ↔ (a, b) ∈ if g ≤ f then {(f - g, g)} else ∅
[PROOFSTEP]
simpa [apply_ite (fun f ↦ (a, b) ∈ f), mem_filter, mem_antidiagonal, mem_singleton, Prod.mk.inj_iff, ← and_assoc,
  and_congr_left_iff]
[GOAL]
case a.mk
α : Type u
inst✝ : DecidableEq α
f g : α →₀ ℕ
D : (p : (α →₀ ℕ) × (α →₀ ℕ)) → Decidable (p.snd = g)
a b : α →₀ ℕ
⊢ b = g → (a + b = f ↔ g ≤ f ∧ a = f - g)
[PROOFSTEP]
rintro rfl
[GOAL]
case a.mk
α : Type u
inst✝ : DecidableEq α
f a b : α →₀ ℕ
D : (p : (α →₀ ℕ) × (α →₀ ℕ)) → Decidable (p.snd = b)
⊢ a + b = f ↔ b ≤ f ∧ a = f - b
[PROOFSTEP]
constructor
[GOAL]
case a.mk.mp
α : Type u
inst✝ : DecidableEq α
f a b : α →₀ ℕ
D : (p : (α →₀ ℕ) × (α →₀ ℕ)) → Decidable (p.snd = b)
⊢ a + b = f → b ≤ f ∧ a = f - b
[PROOFSTEP]
rintro rfl
[GOAL]
case a.mk.mp
α : Type u
inst✝ : DecidableEq α
a b : α →₀ ℕ
D : (p : (α →₀ ℕ) × (α →₀ ℕ)) → Decidable (p.snd = b)
⊢ b ≤ a + b ∧ a = a + b - b
[PROOFSTEP]
exact ⟨le_add_left le_rfl, (add_tsub_cancel_right _ _).symm⟩
[GOAL]
case a.mk.mpr
α : Type u
inst✝ : DecidableEq α
f a b : α →₀ ℕ
D : (p : (α →₀ ℕ) × (α →₀ ℕ)) → Decidable (p.snd = b)
⊢ b ≤ f ∧ a = f - b → a + b = f
[PROOFSTEP]
rintro ⟨h, rfl⟩
[GOAL]
case a.mk.mpr.intro
α : Type u
inst✝ : DecidableEq α
f b : α →₀ ℕ
D : (p : (α →₀ ℕ) × (α →₀ ℕ)) → Decidable (p.snd = b)
h : b ≤ f
⊢ f - b + b = f
[PROOFSTEP]
exact tsub_add_cancel_of_le h
[GOAL]
α : Type u
inst✝ : DecidableEq α
a : α
n : ℕ
⊢ antidiagonal (single a n) =
    map
      (Function.Embedding.prodMap { toFun := single a, inj' := (_ : Function.Injective (single a)) }
        { toFun := single a, inj' := (_ : Function.Injective (single a)) })
      (Nat.antidiagonal n)
[PROOFSTEP]
ext ⟨x, y⟩
[GOAL]
case a.mk
α : Type u
inst✝ : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
⊢ (x, y) ∈ antidiagonal (single a n) ↔
    (x, y) ∈
      map
        (Function.Embedding.prodMap { toFun := single a, inj' := (_ : Function.Injective (single a)) }
          { toFun := single a, inj' := (_ : Function.Injective (single a)) })
        (Nat.antidiagonal n)
[PROOFSTEP]
simp only [mem_antidiagonal, mem_map, Nat.mem_antidiagonal, Function.Embedding.coe_prodMap, Function.Embedding.coeFn_mk,
  Prod_map, Prod.mk.injEq, Prod.exists]
[GOAL]
case a.mk
α : Type u
inst✝ : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
⊢ x + y = single a n ↔ ∃ a_1 b, a_1 + b = n ∧ single a a_1 = x ∧ single a b = y
[PROOFSTEP]
constructor
[GOAL]
case a.mk.mp
α : Type u
inst✝ : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
⊢ x + y = single a n → ∃ a_2 b, a_2 + b = n ∧ single a a_2 = x ∧ single a b = y
[PROOFSTEP]
intro h
[GOAL]
case a.mk.mp
α : Type u
inst✝ : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
h : x + y = single a n
⊢ ∃ a_1 b, a_1 + b = n ∧ single a a_1 = x ∧ single a b = y
[PROOFSTEP]
refine ⟨x a, y a, FunLike.congr_fun h a |>.trans single_eq_same, ?_⟩
[GOAL]
case a.mk.mp
α : Type u
inst✝ : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
h : x + y = single a n
⊢ single a (↑x a) = x ∧ single a (↑y a) = y
[PROOFSTEP]
simp_rw [FunLike.ext_iff, ← forall_and]
[GOAL]
case a.mk.mp
α : Type u
inst✝ : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
h : x + y = single a n
⊢ ∀ (x_1 : α), ↑(single a (↑x a)) x_1 = ↑x x_1 ∧ ↑(single a (↑y a)) x_1 = ↑y x_1
[PROOFSTEP]
intro i
[GOAL]
case a.mk.mp
α : Type u
inst✝ : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
h : x + y = single a n
i : α
⊢ ↑(single a (↑x a)) i = ↑x i ∧ ↑(single a (↑y a)) i = ↑y i
[PROOFSTEP]
replace h := FunLike.congr_fun h i
[GOAL]
case a.mk.mp
α : Type u
inst✝ : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
i : α
h : ↑(x + y) i = ↑(single a n) i
⊢ ↑(single a (↑x a)) i = ↑x i ∧ ↑(single a (↑y a)) i = ↑y i
[PROOFSTEP]
simp_rw [single_apply, Finsupp.add_apply] at h ⊢
[GOAL]
case a.mk.mp
α : Type u
inst✝ : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
i : α
h : ↑x i + ↑y i = if a = i then n else 0
⊢ (if a = i then ↑x a else 0) = ↑x i ∧ (if a = i then ↑y a else 0) = ↑y i
[PROOFSTEP]
obtain rfl | hai := Decidable.eq_or_ne a i
[GOAL]
case a.mk.mp.inl
α : Type u
inst✝ : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
h : ↑x a + ↑y a = if a = a then n else 0
⊢ (if a = a then ↑x a else 0) = ↑x a ∧ (if a = a then ↑y a else 0) = ↑y a
[PROOFSTEP]
exact ⟨if_pos rfl, if_pos rfl⟩
[GOAL]
case a.mk.mp.inr
α : Type u
inst✝ : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
i : α
h : ↑x i + ↑y i = if a = i then n else 0
hai : a ≠ i
⊢ (if a = i then ↑x a else 0) = ↑x i ∧ (if a = i then ↑y a else 0) = ↑y i
[PROOFSTEP]
simp_rw [if_neg hai, _root_.add_eq_zero_iff] at h ⊢
[GOAL]
case a.mk.mp.inr
α : Type u
inst✝ : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
i : α
hai : a ≠ i
h : ↑x i = 0 ∧ ↑y i = 0
⊢ 0 = ↑x i ∧ 0 = ↑y i
[PROOFSTEP]
exact h.imp Eq.symm Eq.symm
[GOAL]
case a.mk.mpr
α : Type u
inst✝ : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
⊢ (∃ a_1 b, a_1 + b = n ∧ single a a_1 = x ∧ single a b = y) → x + y = single a n
[PROOFSTEP]
rintro ⟨a, b, rfl, rfl, rfl⟩
[GOAL]
case a.mk.mpr.intro.intro.intro.intro
α : Type u
inst✝ : DecidableEq α
a✝ : α
a b : ℕ
⊢ single a✝ a + single a✝ b = single a✝ (a + b)
[PROOFSTEP]
exact (single_add _ _ _).symm
