-- Mathlib/Algebra/Order/Antidiag/Prod.lean
theorem filter_fst_eq_antidiagonal (n m : A) [DecidablePred (· = m)] [Decidable (m ≤ n)] :
    filter (fun x : A × A ↦ x.fst = m) (antidiagonal n) = if m ≤ n then {(m, n - m)} else ∅

Proof state:
case h.mk.mpr
A : Type u_1
inst✝⁷ : OrderedAddCommMonoid A
inst✝⁶ : CanonicallyOrderedAdd A
inst✝⁵ : Sub A
inst✝⁴ : OrderedSub A
inst✝³ : AddLeftReflectLE A
inst✝² : HasAntidiagonal A
n a b : A
inst✝¹ : DecidablePred fun x => x = a
inst✝ : Decidable (a ≤ n)
⊢ a ≤ n ∧ b = n - a → a + b = n

Tactic:
rintro ⟨h, rfl⟩

Result:
case h.mk.mpr.intro
A : Type u_1
inst✝⁷ : OrderedAddCommMonoid A
inst✝⁶ : CanonicallyOrderedAdd A
inst✝⁵ : Sub A
inst✝⁴ : OrderedSub A
inst✝³ : AddLeftReflectLE A
inst✝² : HasAntidiagonal A
n a : A
inst✝¹ : DecidablePred fun x => x = a
inst✝ : Decidable (a ≤ n)
h : a ≤ n
⊢ a + (n - a) = n

Proof state:
A : Type u_1
inst✝⁷ : OrderedAddCommMonoid A
inst✝⁶ : CanonicallyOrderedAdd A
inst✝⁵ : Sub A
inst✝⁴ : OrderedSub A
inst✝³ : AddLeftReflectLE A
inst✝² : HasAntidiagonal A
n m : A
inst✝¹ : DecidablePred fun x => x = m
inst✝ : Decidable (m ≤ n)
a b : A
this : a = m → (a + b = n ↔ m ≤ n ∧ b = n - m)
⊢ (a, b).1 + (a, b).2 = n ∧ (a, b).1 = m ↔ m ≤ n ∧ a = m ∧ b = n - m ∨ ¬m ≤ n ∧ (a, b) ∈ ∅

Tactic:
simpa [← and_assoc, @and_right_comm _ (a = _), and_congr_left_iff]

Result:
no goals

Proof state:
case h.mk.mpr.intro
A : Type u_1
inst✝⁷ : OrderedAddCommMonoid A
inst✝⁶ : CanonicallyOrderedAdd A
inst✝⁵ : Sub A
inst✝⁴ : OrderedSub A
inst✝³ : AddLeftReflectLE A
inst✝² : HasAntidiagonal A
n a : A
inst✝¹ : DecidablePred fun x => x = a
inst✝ : Decidable (a ≤ n)
h : a ≤ n
⊢ a + (n - a) = n

Tactic:
exact add_tsub_cancel_of_le h

Result:
no goals

Proof state:
case h.mk
A : Type u_1
inst✝⁷ : OrderedAddCommMonoid A
inst✝⁶ : CanonicallyOrderedAdd A
inst✝⁵ : Sub A
inst✝⁴ : OrderedSub A
inst✝³ : AddLeftReflectLE A
inst✝² : HasAntidiagonal A
n a b : A
inst✝¹ : DecidablePred fun x => x = a
inst✝ : Decidable (a ≤ n)
⊢ a + b = n ↔ a ≤ n ∧ b = n - a

Tactic:
constructor

Result:
case h.mk.mp
A : Type u_1
inst✝⁷ : OrderedAddCommMonoid A
inst✝⁶ : CanonicallyOrderedAdd A
inst✝⁵ : Sub A
inst✝⁴ : OrderedSub A
inst✝³ : AddLeftReflectLE A
inst✝² : HasAntidiagonal A
n a b : A
inst✝¹ : DecidablePred fun x => x = a
inst✝ : Decidable (a ≤ n)
⊢ a + b = n → a ≤ n ∧ b = n - a

case h.mk.mpr
A : Type u_1
inst✝⁷ : OrderedAddCommMonoid A
inst✝⁶ : CanonicallyOrderedAdd A
inst✝⁵ : Sub A
inst✝⁴ : OrderedSub A
inst✝³ : AddLeftReflectLE A
inst✝² : HasAntidiagonal A
n a b : A
inst✝¹ : DecidablePred fun x => x = a
inst✝ : Decidable (a ≤ n)
⊢ a ≤ n ∧ b = n - a → a + b = n

Proof state:
case h.mk
A : Type u_1
inst✝⁷ : OrderedAddCommMonoid A
inst✝⁶ : CanonicallyOrderedAdd A
inst✝⁵ : Sub A
inst✝⁴ : OrderedSub A
inst✝³ : AddLeftReflectLE A
inst✝² : HasAntidiagonal A
n m : A
inst✝¹ : DecidablePred fun x => x = m
inst✝ : Decidable (m ≤ n)
a b : A
⊢ a = m → (a + b = n ↔ m ≤ n ∧ b = n - m)

Tactic:
rintro rfl

Result:
case h.mk
A : Type u_1
inst✝⁷ : OrderedAddCommMonoid A
inst✝⁶ : CanonicallyOrderedAdd A
inst✝⁵ : Sub A
inst✝⁴ : OrderedSub A
inst✝³ : AddLeftReflectLE A
inst✝² : HasAntidiagonal A
n a b : A
inst✝¹ : DecidablePred fun x => x = a
inst✝ : Decidable (a ≤ n)
⊢ a + b = n ↔ a ≤ n ∧ b = n - a

Proof state:
case h.mk.mp
A : Type u_1
inst✝⁷ : OrderedAddCommMonoid A
inst✝⁶ : CanonicallyOrderedAdd A
inst✝⁵ : Sub A
inst✝⁴ : OrderedSub A
inst✝³ : AddLeftReflectLE A
inst✝² : HasAntidiagonal A
n a b : A
inst✝¹ : DecidablePred fun x => x = a
inst✝ : Decidable (a ≤ n)
⊢ a + b = n → a ≤ n ∧ b = n - a

Tactic:
rintro rfl

Result:
case h.mk.mp
A : Type u_1
inst✝⁷ : OrderedAddCommMonoid A
inst✝⁶ : CanonicallyOrderedAdd A
inst✝⁵ : Sub A
inst✝⁴ : OrderedSub A
inst✝³ : AddLeftReflectLE A
inst✝² : HasAntidiagonal A
a b : A
inst✝¹ : DecidablePred fun x => x = a
inst✝ : Decidable (a ≤ a + b)
⊢ a ≤ a + b ∧ b = a + b - a

Proof state:
case h.mk.mp
A : Type u_1
inst✝⁷ : OrderedAddCommMonoid A
inst✝⁶ : CanonicallyOrderedAdd A
inst✝⁵ : Sub A
inst✝⁴ : OrderedSub A
inst✝³ : AddLeftReflectLE A
inst✝² : HasAntidiagonal A
a b : A
inst✝¹ : DecidablePred fun x => x = a
inst✝ : Decidable (a ≤ a + b)
⊢ a ≤ a + b ∧ b = a + b - a

Tactic:
exact ⟨le_add_right le_rfl, (add_tsub_cancel_left _ _).symm⟩

Result:
no goals

Proof state:
case h.mk
A : Type u_1
inst✝⁷ : OrderedAddCommMonoid A
inst✝⁶ : CanonicallyOrderedAdd A
inst✝⁵ : Sub A
inst✝⁴ : OrderedSub A
inst✝³ : AddLeftReflectLE A
inst✝² : HasAntidiagonal A
n m : A
inst✝¹ : DecidablePred fun x => x = m
inst✝ : Decidable (m ≤ n)
a b : A
⊢ (a, b) ∈ filter (fun x => x.1 = m) (antidiagonal n) ↔ (a, b) ∈ if m ≤ n then {(m, n - m)} else ∅

Tactic:
suffices a = m → (a + b = n ↔ m ≤ n ∧ b = n - m) by
  rw [mem_filter, mem_antidiagonal, apply_ite (fun n ↦ (a, b) ∈ n), mem_singleton,
    Prod.mk.inj_iff, ite_prop_iff_or]
  simpa [← and_assoc, @and_right_comm _ (a = _), and_congr_left_iff]

Result:
case h.mk
A : Type u_1
inst✝⁷ : OrderedAddCommMonoid A
inst✝⁶ : CanonicallyOrderedAdd A
inst✝⁵ : Sub A
inst✝⁴ : OrderedSub A
inst✝³ : AddLeftReflectLE A
inst✝² : HasAntidiagonal A
n m : A
inst✝¹ : DecidablePred fun x => x = m
inst✝ : Decidable (m ≤ n)
a b : A
⊢ a = m → (a + b = n ↔ m ≤ n ∧ b = n - m)

Proof state:
A : Type u_1
inst✝⁷ : OrderedAddCommMonoid A
inst✝⁶ : CanonicallyOrderedAdd A
inst✝⁵ : Sub A
inst✝⁴ : OrderedSub A
inst✝³ : AddLeftReflectLE A
inst✝² : HasAntidiagonal A
n m : A
inst✝¹ : DecidablePred fun x => x = m
inst✝ : Decidable (m ≤ n)
⊢ filter (fun x => x.1 = m) (antidiagonal n) = if m ≤ n then {(m, n - m)} else ∅

Tactic:
ext ⟨a, b⟩

Result:
case h.mk
A : Type u_1
inst✝⁷ : OrderedAddCommMonoid A
inst✝⁶ : CanonicallyOrderedAdd A
inst✝⁵ : Sub A
inst✝⁴ : OrderedSub A
inst✝³ : AddLeftReflectLE A
inst✝² : HasAntidiagonal A
n m : A
inst✝¹ : DecidablePred fun x => x = m
inst✝ : Decidable (m ≤ n)
a b : A
⊢ (a, b) ∈ filter (fun x => x.1 = m) (antidiagonal n) ↔ (a, b) ∈ if m ≤ n then {(m, n - m)} else ∅

Proof state:
A : Type u_1
inst✝⁷ : OrderedAddCommMonoid A
inst✝⁶ : CanonicallyOrderedAdd A
inst✝⁵ : Sub A
inst✝⁴ : OrderedSub A
inst✝³ : AddLeftReflectLE A
inst✝² : HasAntidiagonal A
n m : A
inst✝¹ : DecidablePred fun x => x = m
inst✝ : Decidable (m ≤ n)
a b : A
this : a = m → (a + b = n ↔ m ≤ n ∧ b = n - m)
⊢ (a, b) ∈ filter (fun x => x.1 = m) (antidiagonal n) ↔ (a, b) ∈ if m ≤ n then {(m, n - m)} else ∅

Tactic:
rw [mem_filter, mem_antidiagonal, apply_ite (fun n ↦ (a, b) ∈ n), mem_singleton,
  Prod.mk.inj_iff, ite_prop_iff_or]

Result:
A : Type u_1
inst✝⁷ : OrderedAddCommMonoid A
inst✝⁶ : CanonicallyOrderedAdd A
inst✝⁵ : Sub A
inst✝⁴ : OrderedSub A
inst✝³ : AddLeftReflectLE A
inst✝² : HasAntidiagonal A
n m : A
inst✝¹ : DecidablePred fun x => x = m
inst✝ : Decidable (m ≤ n)
a b : A
this : a = m → (a + b = n ↔ m ≤ n ∧ b = n - m)
⊢ (a, b).1 + (a, b).2 = n ∧ (a, b).1 = m ↔ m ≤ n ∧ a = m ∧ b = n - m ∨ ¬m ≤ n ∧ (a, b) ∈ ∅