-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite (goal)
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
⊢ ((↑((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) (a, b, c) : Finset (α ⊕ β ⊕ γ)) : Set (α ⊕ β ⊕ γ)) ∩
      (↑((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) (x, y, z) : Finset (α ⊕ β ⊕ γ)) :
        Set (α ⊕ β ⊕ γ))).Subsingleton
have 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))
Tactic: simp only [toTriangle_apply, in₀, in₁, in₂, Set.mem_inter_iff, mem_insert, mem_singleton,
    mem_coe, and_imp, Sum.forall,
    Set.Subsingleton]