-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
inst_3 : ExplicitDisjoint t
a : α
b : β
c : γ
habc : (a, b, c) ∈ t
x : α
y : β
z : γ
hxyz : (x, y, z) ∈ t
h' :
  ¬Eq (α := Finset (α ⊕ β ⊕ γ)) ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) (a, b, c) : Finset (α ⊕ β ⊕ γ))
      ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) (x, y, z) : Finset (α ⊕ β ⊕ γ))
this : a = x → b = y → ¬c = z
suffices : ¬(a = x ∧ b = y) ∧ ¬(a = x ∧ c = z) ∧ ¬(b = y ∧ c = z)
⊢ (∀ (a_1 : α),
      Eq (α := α ⊕ β ⊕ γ) (Sum.inl a_1) (Sum.inl a) ∨
          Eq (α := α ⊕ β ⊕ γ) (Sum.inl a_1) (Sum.inr (Sum.inl b)) ∨
            Eq (α := α ⊕ β ⊕ γ) (Sum.inl a_1) (Sum.inr (Sum.inr c)) →
        Eq (α := α ⊕ β ⊕ γ) (Sum.inl a_1) (Sum.inl x) ∨
            Eq (α := α ⊕ β ⊕ γ) (Sum.inl a_1) (Sum.inr (Sum.inl y)) ∨
              Eq (α := α ⊕ β ⊕ γ) (Sum.inl a_1) (Sum.inr (Sum.inr z)) →
          (∀ (a_4 : α),
              Eq (α := α ⊕ β ⊕ γ) (Sum.inl a_4) (Sum.inl a) ∨
                  Eq (α := α ⊕ β ⊕ γ) (Sum.inl a_4) (Sum.inr (Sum.inl b)) ∨
                    Eq (α := α ⊕ β ⊕ γ) (Sum.inl a_4) (Sum.inr (Sum.inr c)) →
                Eq (α := α ⊕ β ⊕ γ) (Sum.inl a_4) (Sum.inl x) ∨
                    Eq (α := α ⊕ β ⊕ γ) (Sum.inl a_4) (Sum.inr (Sum.inl y)) ∨
                      Eq (α := α ⊕ β ⊕ γ) (Sum.inl a_4) (Sum.inr (Sum.inr z)) →
                  Eq (α := α ⊕ β ⊕ γ) (Sum.inl a_1) (Sum.inl a_4)) ∧
            (∀ (a_4 : β),
                Eq (α := α ⊕ β ⊕ γ) (Sum.inr (Sum.inl a_4)) (Sum.inl a) ∨
                    Eq (α := α ⊕ β ⊕ γ) (Sum.inr (Sum.inl a_4)) (Sum.inr (Sum.inl b)) ∨
                      Eq (α := α ⊕ β ⊕ γ) (Sum.inr (Sum.inl a_4)) (Sum.inr (Sum.inr c)) →
                  Eq (α := α ⊕ β ⊕ γ) (Sum.inr (Sum.inl a_4)) (Sum.inl x) ∨
                      Eq (α := α ⊕ β ⊕ γ) (Sum.inr (Sum.inl a_4)) (Sum.inr (Sum.inl y)) ∨
                        Eq (α := α ⊕ β ⊕ γ) (Sum.inr (Sum.inl a_4)) (Sum.inr (Sum.inr z)) →
                    Eq (α := α ⊕ β ⊕ γ) (Sum.inl a_1) (Sum.inr (Sum.inl a_4))) ∧
              ∀ (b_1 : γ),
                Eq (α := α ⊕ β ⊕ γ) (Sum.inr (Sum.inr b_1)) (Sum.inl a) ∨
                    Eq (α := α ⊕ β ⊕ γ) (Sum.inr (Sum.inr b_1)) (Sum.inr (Sum.inl b)) ∨
                      Eq (α := α ⊕ β ⊕ γ) (Sum.inr (Sum.inr b_1)) (Sum.inr (Sum.inr c)) →
                  Eq (α := α ⊕ β ⊕ γ) (Sum.inr (Sum.inr b_1)) (Sum.inl x) ∨
                      Eq (α := α ⊕ β ⊕ γ) (Sum.inr (Sum.inr b_1)) (Sum.inr (Sum.inl y)) ∨
                        Eq (α := α ⊕ β ⊕ γ) (Sum.inr (Sum.inr b_1)) (Sum.inr (Sum.inr z)) →
                    Eq (α := α ⊕ β ⊕ γ) (Sum.inl a_1) (Sum.inr (Sum.inr b_1))) ∧
    (∀ (a_1 : β),
        Eq (α := α ⊕ β ⊕ γ) (Sum.inr (Sum.inl a_1)) (Sum.inl a) ∨
            Eq (α := α ⊕ β ⊕ γ) (Sum.inr (Sum.inl a_1)) (Sum.inr (Sum.inl b)) ∨
              Eq (α := α ⊕ β ⊕ γ) (Sum.inr (Sum.inl a_1)) (Sum.inr (Sum.inr c)) →
          Eq (α := α ⊕ β ⊕ γ) (Sum.inr (Sum.inl a_1)) (Sum.inl x) ∨
              Eq (α := α ⊕ β ⊕ γ) (Sum.inr (Sum.inl a_1)) (Sum.inr (Sum.inl y)) ∨
                Eq (α := α ⊕ β ⊕ γ) (Sum.inr (Sum.inl a_1)) (Sum.inr (Sum.inr z)) →
            (∀ (a_4 : α),
                Eq (α := α ⊕ β ⊕ γ) (Sum.inl a_4) (Sum.inl a) ∨
                    Eq (α := α ⊕ β ⊕ γ) (Sum.inl a_4) (Sum.inr (Sum.inl b)) ∨
                      Eq (α := α ⊕ β ⊕ γ) (Sum.inl a_4) (Sum.inr (Sum.inr c)) →
                  Eq (α := α ⊕ β ⊕ γ) (Sum.inl a_4) (Sum.inl x) ∨
                      Eq (α := α ⊕ β ⊕ γ) (Sum.inl a_4) (Sum.inr (Sum.inl y)) ∨
                        Eq (α := α ⊕ β ⊕ γ) (Sum.inl a_4) (Sum.inr (Sum.inr z)) →
                    Eq (α := α ⊕ β ⊕ γ) (Sum.inr (Sum.inl a_1)) (Sum.inl a_4)) ∧
              (∀ (a_4 : β),
                  Eq (α := α ⊕ β ⊕ γ) (Sum.inr (Sum.inl a_4)) (Sum.inl a) ∨
                      Eq (α := α ⊕ β ⊕ γ) (Sum.inr (Sum.inl a_4)) (Sum.inr (Sum.inl b)) ∨
                        Eq (α := α ⊕ β ⊕ γ) (Sum.inr (Sum.inl a_4)) (Sum.inr (Sum.inr c)) →
                    Eq (α := α ⊕ β ⊕ γ) (Sum.inr (Sum.inl a_4)) (Sum.inl x) ∨
                        Eq (α := α ⊕ β ⊕ γ) (Sum.inr (Sum.inl a_4)) (Sum.inr (Sum.inl y)) ∨
                          Eq (α := α ⊕ β ⊕ γ) (Sum.inr (Sum.inl a_4)) (Sum.inr (Sum.inr z)) →
                      Eq (α := α ⊕ β ⊕ γ) (Sum.inr (Sum.inl a_1)) (Sum.inr (Sum.inl a_4))) ∧
                ∀ (b_1 : γ),
                  Eq (α := α ⊕ β ⊕ γ) (Sum.inr (Sum.inr b_1)) (Sum.inl a) ∨
                      Eq (α := α ⊕ β ⊕ γ) (Sum.inr (Sum.inr b_1)) (Sum.inr (Sum.inl b)) ∨
                        Eq (α := α ⊕ β ⊕ γ) (Sum.inr (Sum.inr b_1)) (Sum.inr (Sum.inr c)) →
                    Eq (α := α ⊕ β ⊕ γ) (Sum.inr (Sum.inr b_1)) (Sum.inl x) ∨
                        Eq (α := α ⊕ β ⊕ γ) (Sum.inr (Sum.inr b_1)) (Sum.inr (Sum.inl y)) ∨
                          Eq (α := α ⊕ β ⊕ γ) (Sum.inr (Sum.inr b_1)) (Sum.inr (Sum.inr z)) →
                      Eq (α := α ⊕ β ⊕ γ) (Sum.inr (Sum.inl a_1)) (Sum.inr (Sum.inr b_1))) ∧
      ∀ (b_1 : γ),
        Eq (α := α ⊕ β ⊕ γ) (Sum.inr (Sum.inr b_1)) (Sum.inl a) ∨
            Eq (α := α ⊕ β ⊕ γ) (Sum.inr (Sum.inr b_1)) (Sum.inr (Sum.inl b)) ∨
              Eq (α := α ⊕ β ⊕ γ) (Sum.inr (Sum.inr b_1)) (Sum.inr (Sum.inr c)) →
          Eq (α := α ⊕ β ⊕ γ) (Sum.inr (Sum.inr b_1)) (Sum.inl x) ∨
              Eq (α := α ⊕ β ⊕ γ) (Sum.inr (Sum.inr b_1)) (Sum.inr (Sum.inl y)) ∨
                Eq (α := α ⊕ β ⊕ γ) (Sum.inr (Sum.inr b_1)) (Sum.inr (Sum.inr z)) →
            (∀ (a_3 : α),
                Eq (α := α ⊕ β ⊕ γ) (Sum.inl a_3) (Sum.inl a) ∨
                    Eq (α := α ⊕ β ⊕ γ) (Sum.inl a_3) (Sum.inr (Sum.inl b)) ∨
                      Eq (α := α ⊕ β ⊕ γ) (Sum.inl a_3) (Sum.inr (Sum.inr c)) →
                  Eq (α := α ⊕ β ⊕ γ) (Sum.inl a_3) (Sum.inl x) ∨
                      Eq (α := α ⊕ β ⊕ γ) (Sum.inl a_3) (Sum.inr (Sum.inl y)) ∨
                        Eq (α := α ⊕ β ⊕ γ) (Sum.inl a_3) (Sum.inr (Sum.inr z)) →
                    Eq (α := α ⊕ β ⊕ γ) (Sum.inr (Sum.inr b_1)) (Sum.inl a_3)) ∧
              (∀ (a_3 : β),
                  Eq (α := α ⊕ β ⊕ γ) (Sum.inr (Sum.inl a_3)) (Sum.inl a) ∨
                      Eq (α := α ⊕ β ⊕ γ) (Sum.inr (Sum.inl a_3)) (Sum.inr (Sum.inl b)) ∨
                        Eq (α := α ⊕ β ⊕ γ) (Sum.inr (Sum.inl a_3)) (Sum.inr (Sum.inr c)) →
                    Eq (α := α ⊕ β ⊕ γ) (Sum.inr (Sum.inl a_3)) (Sum.inl x) ∨
                        Eq (α := α ⊕ β ⊕ γ) (Sum.inr (Sum.inl a_3)) (Sum.inr (Sum.inl y)) ∨
                          Eq (α := α ⊕ β ⊕ γ) (Sum.inr (Sum.inl a_3)) (Sum.inr (Sum.inr z)) →
                      Eq (α := α ⊕ β ⊕ γ) (Sum.inr (Sum.inr b_1)) (Sum.inr (Sum.inl a_3))) ∧
                ∀ (b_2 : γ),
                  Eq (α := α ⊕ β ⊕ γ) (Sum.inr (Sum.inr b_2)) (Sum.inl a) ∨
                      Eq (α := α ⊕ β ⊕ γ) (Sum.inr (Sum.inr b_2)) (Sum.inr (Sum.inl b)) ∨
                        Eq (α := α ⊕ β ⊕ γ) (Sum.inr (Sum.inr b_2)) (Sum.inr (Sum.inr c)) →
                    Eq (α := α ⊕ β ⊕ γ) (Sum.inr (Sum.inr b_2)) (Sum.inl x) ∨
                        Eq (α := α ⊕ β ⊕ γ) (Sum.inr (Sum.inr b_2)) (Sum.inr (Sum.inl y)) ∨
                          Eq (α := α ⊕ β ⊕ γ) (Sum.inr (Sum.inr b_2)) (Sum.inr (Sum.inr z)) →
                      Eq (α := α ⊕ β ⊕ γ) (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