Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableEq γ
inst✝ : ExplicitDisjoint t
a : α
b : β
c : γ
habc : (a, b, c) ∈ t
x : α
y : β
z : γ
hxyz : (x, y, z) ∈ t
h' : ¬toTriangle (a, b, c) = toTriangle (x, y, z)
this : a = x → b = y → ¬c = z
⊢ (∀ (a_1 : α),
      Sum.inl a_1 = Sum.inl a ∨ Sum.inl a_1 = Sum.inr (Sum.inl b) ∨ Sum.inl a_1 = Sum.inr (Sum.inr c) →
        Sum.inl a_1 = Sum.inl x ∨ Sum.inl a_1 = Sum.inr (Sum.inl y) ∨ Sum.inl a_1 = Sum.inr (Sum.inr z) →
          (∀ (a_4 : α),
              Sum.inl a_4 = Sum.inl a ∨ Sum.inl a_4 = Sum.inr (Sum.inl b) ∨ Sum.inl a_4 = Sum.inr (Sum.inr c) →
                Sum.inl a_4 = Sum.inl x ∨ Sum.inl a_4 = Sum.inr (Sum.inl y) ∨ Sum.inl a_4 = Sum.inr (Sum.inr z) →
                  Sum.inl a_1 = Sum.inl a_4) ∧
            (∀ (a_4 : β),
                Sum.inr (Sum.inl a_4) = Sum.inl a ∨
                    Sum.inr (Sum.inl a_4) = Sum.inr (Sum.inl b) ∨ Sum.inr (Sum.inl a_4) = Sum.inr (Sum.inr c) →
                  Sum.inr (Sum.inl a_4) = Sum.inl x ∨
                      Sum.inr (Sum.inl a_4) = Sum.inr (Sum.inl y) ∨ Sum.inr (Sum.inl a_4) = Sum.inr (Sum.inr z) →
                    Sum.inl a_1 = Sum.inr (Sum.inl a_4)) ∧
              ∀ (b_1 : γ),
                Sum.inr (Sum.inr b_1) = Sum.inl a ∨
                    Sum.inr (Sum.inr b_1) = Sum.inr (Sum.inl b) ∨ Sum.inr (Sum.inr b_1) = Sum.inr (Sum.inr c) →
                  Sum.inr (Sum.inr b_1) = Sum.inl x ∨
                      Sum.inr (Sum.inr b_1) = Sum.inr (Sum.inl y) ∨ Sum.inr (Sum.inr b_1) = Sum.inr (Sum.inr z) →
                    Sum.inl a_1 = Sum.inr (Sum.inr b_1)) ∧
    (∀ (a_1 : β),
        Sum.inr (Sum.inl a_1) = Sum.inl a ∨
            Sum.inr (Sum.inl a_1) = Sum.inr (Sum.inl b) ∨ Sum.inr (Sum.inl a_1) = Sum.inr (Sum.inr c) →
          Sum.inr (Sum.inl a_1) = Sum.inl x ∨
              Sum.inr (Sum.inl a_1) = Sum.inr (Sum.inl y) ∨ Sum.inr (Sum.inl a_1) = Sum.inr (Sum.inr z) →
            (∀ (a_4 : α),
                Sum.inl a_4 = Sum.inl a ∨ Sum.inl a_4 = Sum.inr (Sum.inl b) ∨ Sum.inl a_4 = Sum.inr (Sum.inr c) →
                  Sum.inl a_4 = Sum.inl x ∨ Sum.inl a_4 = Sum.inr (Sum.inl y) ∨ Sum.inl a_4 = Sum.inr (Sum.inr z) →
                    Sum.inr (Sum.inl a_1) = Sum.inl a_4) ∧
              (∀ (a_4 : β),
                  Sum.inr (Sum.inl a_4) = Sum.inl a ∨
                      Sum.inr (Sum.inl a_4) = Sum.inr (Sum.inl b) ∨ Sum.inr (Sum.inl a_4) = Sum.inr (Sum.inr c) →
                    Sum.inr (Sum.inl a_4) = Sum.inl x ∨
                        Sum.inr (Sum.inl a_4) = Sum.inr (Sum.inl y) ∨ Sum.inr (Sum.inl a_4) = Sum.inr (Sum.inr z) →
                      Sum.inr (Sum.inl a_1) = Sum.inr (Sum.inl a_4)) ∧
                ∀ (b_1 : γ),
                  Sum.inr (Sum.inr b_1) = Sum.inl a ∨
                      Sum.inr (Sum.inr b_1) = Sum.inr (Sum.inl b) ∨ Sum.inr (Sum.inr b_1) = Sum.inr (Sum.inr c) →
                    Sum.inr (Sum.inr b_1) = Sum.inl x ∨
                        Sum.inr (Sum.inr b_1) = Sum.inr (Sum.inl y) ∨ Sum.inr (Sum.inr b_1) = Sum.inr (Sum.inr z) →
                      Sum.inr (Sum.inl a_1) = Sum.inr (Sum.inr b_1)) ∧
      ∀ (b_1 : γ),
        Sum.inr (Sum.inr b_1) = Sum.inl a ∨
            Sum.inr (Sum.inr b_1) = Sum.inr (Sum.inl b) ∨ Sum.inr (Sum.inr b_1) = Sum.inr (Sum.inr c) →
          Sum.inr (Sum.inr b_1) = Sum.inl x ∨
              Sum.inr (Sum.inr b_1) = Sum.inr (Sum.inl y) ∨ Sum.inr (Sum.inr b_1) = Sum.inr (Sum.inr z) →
            (∀ (a_3 : α),
                Sum.inl a_3 = Sum.inl a ∨ Sum.inl a_3 = Sum.inr (Sum.inl b) ∨ Sum.inl a_3 = Sum.inr (Sum.inr c) →
                  Sum.inl a_3 = Sum.inl x ∨ Sum.inl a_3 = Sum.inr (Sum.inl y) ∨ Sum.inl a_3 = Sum.inr (Sum.inr z) →
                    Sum.inr (Sum.inr b_1) = Sum.inl a_3) ∧
              (∀ (a_3 : β),
                  Sum.inr (Sum.inl a_3) = Sum.inl a ∨
                      Sum.inr (Sum.inl a_3) = Sum.inr (Sum.inl b) ∨ Sum.inr (Sum.inl a_3) = Sum.inr (Sum.inr c) →
                    Sum.inr (Sum.inl a_3) = Sum.inl x ∨
                        Sum.inr (Sum.inl a_3) = Sum.inr (Sum.inl y) ∨ Sum.inr (Sum.inl a_3) = Sum.inr (Sum.inr z) →
                      Sum.inr (Sum.inr b_1) = Sum.inr (Sum.inl a_3)) ∧
                ∀ (b_2 : γ),
                  Sum.inr (Sum.inr b_2) = Sum.inl a ∨
                      Sum.inr (Sum.inr b_2) = Sum.inr (Sum.inl b) ∨ Sum.inr (Sum.inr b_2) = Sum.inr (Sum.inr c) →
                    Sum.inr (Sum.inr b_2) = Sum.inl x ∨
                        Sum.inr (Sum.inr b_2) = Sum.inr (Sum.inl y) ∨ Sum.inr (Sum.inr b_2) = Sum.inr (Sum.inr z) →
                      Sum.inr (Sum.inr b_1) = Sum.inr (Sum.inr b_2)

Tactic:
suffices ¬ (a = x ∧ b = y) ∧ ¬ (a = x ∧ c = z) ∧ ¬ (b = y ∧ c = z) by aesop

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableEq γ
inst✝ : ExplicitDisjoint t
a : α
b : β
c : γ
habc : (a, b, c) ∈ t
x : α
y : β
z : γ
hxyz : (x, y, z) ∈ t
h' : ¬toTriangle (a, b, c) = toTriangle (x, y, z)
this : a = x → b = y → ¬c = z
⊢ ¬(a = x ∧ b = y) ∧ ¬(a = x ∧ c = z) ∧ ¬(b = y ∧ c = z)