-- 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
⊢ ¬(a = x ∧ b = y) ∧ ¬(a = x ∧ c = z) ∧ ¬(b = y ∧ c = z)

Tactic:
refine ⟨?_, ?_, ?_⟩

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

case refine_2
α : 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 ∧ c = z)

case refine_3
α : 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
⊢ ¬(b = y ∧ c = z)

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
this : ¬(a = x ∧ b = y) ∧ ¬(a = x ∧ c = z) ∧ ¬(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:
aesop

Result:
no goals