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

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

Proof state:
case refine_3.intro
α : 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 : α
hxyz : (x, b, c) ∈ t
h' : ¬toTriangle (a, b, c) = toTriangle (x, b, c)
this : a = x → b = b → ¬c = c
⊢ False

Tactic:
exact this (ExplicitDisjoint.inj₀ habc hxyz) rfl rfl

Result:
no goals

Proof state:
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)

Tactic:
rintro ⟨rfl, rfl⟩

Result:
case refine_2.intro
α : 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
y : β
hxyz : (a, y, c) ∈ t
h' : ¬toTriangle (a, b, c) = toTriangle (a, y, c)
this : a = a → b = y → ¬c = c
⊢ False