-- Mathlib/Combinatorics/SimpleGraph/Triangle/Tripartite.lean
lemma map_toTriangle_disjoint [ExplicitDisjoint t] :
    (t.map toTriangle : Set (Finset (α ⊕ β ⊕ γ))).Pairwise
      fun x y ↦ (x ∩ y : Set (α ⊕ β ⊕ γ)).Subsingleton

Proof state:
α : 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
⊢ (↑(toTriangle (a, b, c)) ∩ ↑(toTriangle (x, y, z))).Subsingleton

Tactic:
simp only [toTriangle_apply, in₀, in₁, in₂, Set.mem_inter_iff, mem_insert, mem_singleton,
  mem_coe, and_imp, Sum.forall, or_false, forall_eq, false_or, eq_self_iff_true, imp_true_iff,
  true_and, and_true, Set.Subsingleton]

Result:
α : 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)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableEq γ
inst✝ : ExplicitDisjoint t
x✝ : Finset (α ⊕ β ⊕ γ)
⊢ x✝ ∈ ↑(map toTriangle t) →
    ∀ ⦃y : Finset (α ⊕ β ⊕ γ)⦄, y ∈ ↑(map toTriangle t) → x✝ ≠ y → (fun x y => (↑x ∩ ↑y).Subsingleton) x✝ y

Tactic:
simp only [Finset.coe_map, Set.mem_image, Finset.mem_coe, Prod.exists, Ne,
  forall_exists_index, and_imp]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableEq γ
inst✝ : ExplicitDisjoint t
x✝ : Finset (α ⊕ β ⊕ γ)
⊢ ∀ (x : α) (x_1 : β) (x_2 : γ),
    (x, x_1, x_2) ∈ t →
      toTriangle (x, x_1, x_2) = x✝ →
        ∀ ⦃y : Finset (α ⊕ β ⊕ γ)⦄ (x : α) (x_3 : β) (x_4 : γ),
          (x, x_3, x_4) ∈ t → toTriangle (x, x_3, x_4) = y → ¬x✝ = y → (↑x✝ ∩ ↑y).Subsingleton

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableEq γ
inst✝ : ExplicitDisjoint t
⊢ (↑(map toTriangle t)).Pairwise fun x y => (↑x ∩ ↑y).Subsingleton

Tactic:
intro

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableEq γ
inst✝ : ExplicitDisjoint t
x✝ : Finset (α ⊕ β ⊕ γ)
⊢ x✝ ∈ ↑(map toTriangle t) →
    ∀ ⦃y : Finset (α ⊕ β ⊕ γ)⦄, y ∈ ↑(map toTriangle t) → x✝ ≠ y → (fun x y => (↑x ∩ ↑y).Subsingleton) x✝ y