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

case a.mk.mpr
α : Type u
f a b : α →₀ ℕ
D : (p : (α →₀ ℕ) × (α →₀ ℕ)) → Decidable (p.fst = a)
⊢ a ≤ f ∧ b = f - a → a + b = f
case a.mk
α : Type u
f a b : α →₀ ℕ
D : (p : (α →₀ ℕ) × (α →₀ ℕ)) → Decidable (p.fst = a)
⊢ a + b = f ↔ a ≤ f ∧ b = f - a
constructor
no goals
α : Type u
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 ∅
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]
case a.mk.mp
α : Type u
a b : α →₀ ℕ
D : (p : (α →₀ ℕ) × (α →₀ ℕ)) → Decidable (p.fst = a)
⊢ a ≤ a + b ∧ b = a + b - a
case a.mk.mp
α : Type u
f a b : α →₀ ℕ
D : (p : (α →₀ ℕ) × (α →₀ ℕ)) → Decidable (p.fst = a)
⊢ a + b = f → a ≤ f ∧ b = f - a
rintro rfl
no goals
case a.mk.mp
α : Type u
a b : α →₀ ℕ
D : (p : (α →₀ ℕ) × (α →₀ ℕ)) → Decidable (p.fst = a)
⊢ a ≤ a + b ∧ b = a + b - a
exact ⟨le_add_right le_rfl, (add_tsub_cancel_left _ _).symm⟩
case a.mk.mpr.intro
α : Type u
f a : α →₀ ℕ
D : (p : (α →₀ ℕ) × (α →₀ ℕ)) → Decidable (p.fst = a)
h : a ≤ f
⊢ a + (f - a) = f
case a.mk.mpr
α : Type u
f a b : α →₀ ℕ
D : (p : (α →₀ ℕ) × (α →₀ ℕ)) → Decidable (p.fst = a)
⊢ a ≤ f ∧ b = f - a → a + b = f
rintro ⟨h, rfl⟩
no goals
case a.mk.mpr.intro
α : Type u
f a : α →₀ ℕ
D : (p : (α →₀ ℕ) × (α →₀ ℕ)) → Decidable (p.fst = a)
h : a ≤ f
⊢ a + (f - a) = f
exact add_tsub_cancel_of_le h