-- 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
simp :
  (∀ (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))
⊢ ((↑((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) (a, b, c) : Finset (α ⊕ β ⊕ γ)) : Set (α ⊕ β ⊕ γ)) ∩
      (↑((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) (x, y, z) : Finset (α ⊕ β ⊕ γ)) :
        Set (α ⊕ β ⊕ γ))).Subsingleton

Tactic:
simp only [toTriangle_apply, in₀, in₁, in₂, Set.mem_inter_iff, mem_insert, mem_singleton,
    mem_coe, and_imp, Sum.forall,
    Set.Subsingleton]

Premises used: Finset.mem_singleton, and_imp, Set.mem_inter_iff, Sum3.in₂, Sum3.in₁, Finset.mem_insert, Set.Subsingleton, Sum3.in₀, Sum.forall, Finset.mem_coe, SimpleGraph.TripartiteFromTriangles.toTriangle_apply