case a.mk
α : Type u
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 ∅
α : Type u
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 ∅
ext ⟨a, b⟩
case a.mk
α : Type u
f g : α →₀ ℕ
D : (p : (α →₀ ℕ) × (α →₀ ℕ)) → Decidable (p.snd = g)
a b : α →₀ ℕ
⊢ b = g → (a + b = f ↔ g ≤ f ∧ a = f - g)
case a.mk
α : Type u
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 ∅
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]
case a.mk
α : Type u
f a b : α →₀ ℕ
D : (p : (α →₀ ℕ) × (α →₀ ℕ)) → Decidable (p.snd = b)
⊢ a + b = f ↔ b ≤ f ∧ a = f - b
case a.mk
α : Type u
f g : α →₀ ℕ
D : (p : (α →₀ ℕ) × (α →₀ ℕ)) → Decidable (p.snd = g)
a b : α →₀ ℕ
⊢ b = g → (a + b = f ↔ g ≤ f ∧ a = f - g)
rintro rfl
case a.mk.mp
α : Type u
f a b : α →₀ ℕ
D : (p : (α →₀ ℕ) × (α →₀ ℕ)) → Decidable (p.snd = b)
⊢ a + b = f → b ≤ f ∧ a = f - b

case a.mk.mpr
α : Type u
f a b : α →₀ ℕ
D : (p : (α →₀ ℕ) × (α →₀ ℕ)) → Decidable (p.snd = b)
⊢ b ≤ f ∧ a = f - b → a + b = f
case a.mk
α : Type u
f a b : α →₀ ℕ
D : (p : (α →₀ ℕ) × (α →₀ ℕ)) → Decidable (p.snd = b)
⊢ a + b = f ↔ b ≤ f ∧ a = f - b
constructor
no goals
α : Type u
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 ∅
simpa [apply_ite (fun f ↦ (a, b) ∈ f), mem_filter, mem_antidiagonal, mem_singleton,
  Prod.mk.inj_iff, ← and_assoc, and_congr_left_iff]
case a.mk.mp
α : Type u
a b : α →₀ ℕ
D : (p : (α →₀ ℕ) × (α →₀ ℕ)) → Decidable (p.snd = b)
⊢ b ≤ a + b ∧ a = a + b - b
case a.mk.mp
α : Type u
f a b : α →₀ ℕ
D : (p : (α →₀ ℕ) × (α →₀ ℕ)) → Decidable (p.snd = b)
⊢ a + b = f → b ≤ f ∧ a = f - b
rintro rfl
no goals
case a.mk.mp
α : Type u
a b : α →₀ ℕ
D : (p : (α →₀ ℕ) × (α →₀ ℕ)) → Decidable (p.snd = b)
⊢ b ≤ a + b ∧ a = a + b - b
exact ⟨le_add_left le_rfl, (add_tsub_cancel_right _ _).symm⟩
case a.mk.mpr.intro
α : Type u
f b : α →₀ ℕ
D : (p : (α →₀ ℕ) × (α →₀ ℕ)) → Decidable (p.snd = b)
h : b ≤ f
⊢ f - b + b = f
case a.mk.mpr
α : Type u
f a b : α →₀ ℕ
D : (p : (α →₀ ℕ) × (α →₀ ℕ)) → Decidable (p.snd = b)
⊢ b ≤ f ∧ a = f - b → a + b = f
rintro ⟨h, rfl⟩
no goals
case a.mk.mpr.intro
α : Type u
f b : α →₀ ℕ
D : (p : (α →₀ ℕ) × (α →₀ ℕ)) → Decidable (p.snd = b)
h : b ≤ f
⊢ f - b + b = f
exact tsub_add_cancel_of_le h