-- Mathlib/Combinatorics/SimpleGraph/Triangle/Tripartite.lean
/-- This lemma reorders the elements of a triangle in the tripartite graph. It turns a triangle
`{x, y, z}` into a triangle `{a, b, c}` where `a : α `, `b : β`, `c : γ`. -/
 lemma graph_triple ⦃x y z⦄ :
  (graph t).Adj x y → (graph t).Adj x z → (graph t).Adj y z → ∃ a b c,
    ({in₀ a, in₁ b, in₂ c} : Finset (α ⊕ β ⊕ γ)) = {x, y, z} ∧ (graph t).Adj (in₀ a) (in₁ b) ∧
      (graph t).Adj (in₀ a) (in₂ c) ∧ (graph t).Adj (in₁ b) (in₂ c)

Proof state:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a✝⁵ : α
b✝¹ : β
c✝¹ : γ
a✝⁴ : (a✝⁵, b✝¹, c✝¹) ∈ t
a✝³ : α
b✝ : β
a✝² : (a✝³, b✝, c✝¹) ∈ t
c✝ : γ
a✝¹ : (a✝³, b✝¹, c✝) ∈ t
a✝ : α ⊕ β ⊕ γ
⊢ a✝ = in₀ ?m.58857 ∨ a✝ = in₁ ?m.58870 ∨ a✝ = in₂ ?m.58883 ↔ a✝ = in₂ c✝¹ ∨ a✝ = in₁ b✝¹ ∨ a✝ = in₀ a✝³

Tactic:
tauto

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
x y z : α ⊕ β ⊕ γ
⊢ (graph t).Adj x y →
    (graph t).Adj x z →
      (graph t).Adj y z →
        ∃ a b c,
          {in₀ a, in₁ b, in₂ c} = {x, y, z} ∧
            (graph t).Adj (in₀ a) (in₁ b) ∧ (graph t).Adj (in₀ a) (in₂ c) ∧ (graph t).Adj (in₁ b) (in₂ c)

Tactic:
rintro (_ | _ | _) (_ | _ | _) (_ | _ | _) <;>
  refine ⟨_, _, _, by ext; simp only [Finset.mem_insert, Finset.mem_singleton]; try tauto,
    ?_, ?_, ?_⟩ <;> constructor <;> assumption

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a✝⁴ : α
b✝¹ : β
c✝¹ : γ
a✝³ : (a✝⁴, b✝¹, c✝¹) ∈ t
a✝² : α
b✝ : β
a✝¹ : (a✝², b✝, c✝¹) ∈ t
c✝ : γ
a✝ : (a✝², b✝¹, c✝) ∈ t
⊢ {in₀ ?m.58857, in₁ ?m.58870, in₂ ?m.58883} = {in₂ c✝¹, in₁ b✝¹, in₀ a✝²}

Tactic:
ext

Result:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a✝⁵ : α
b✝¹ : β
c✝¹ : γ
a✝⁴ : (a✝⁵, b✝¹, c✝¹) ∈ t
a✝³ : α
b✝ : β
a✝² : (a✝³, b✝, c✝¹) ∈ t
c✝ : γ
a✝¹ : (a✝³, b✝¹, c✝) ∈ t
a✝ : α ⊕ β ⊕ γ
⊢ a✝ ∈ {in₀ ?m.58857, in₁ ?m.58870, in₂ ?m.58883} ↔ a✝ ∈ {in₂ c✝¹, in₁ b✝¹, in₀ a✝³}

Proof state:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a✝⁵ : α
b✝¹ : β
c✝¹ : γ
a✝⁴ : (a✝⁵, b✝¹, c✝¹) ∈ t
a✝³ : α
b✝ : β
a✝² : (a✝³, b✝, c✝¹) ∈ t
c✝ : γ
a✝¹ : (a✝³, b✝¹, c✝) ∈ t
a✝ : α ⊕ β ⊕ γ
⊢ a✝ = in₀ ?m.58857 ∨ a✝ = in₁ ?m.58870 ∨ a✝ = in₂ ?m.58883 ↔ a✝ = in₂ c✝¹ ∨ a✝ = in₁ b✝¹ ∨ a✝ = in₀ a✝³

Tactic:
try tauto

Result:
no goals

Proof state:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a✝⁵ : α
b✝¹ : β
c✝¹ : γ
a✝⁴ : (a✝⁵, b✝¹, c✝¹) ∈ t
a✝³ : α
b✝ : β
a✝² : (a✝³, b✝, c✝¹) ∈ t
c✝ : γ
a✝¹ : (a✝³, b✝¹, c✝) ∈ t
a✝ : α ⊕ β ⊕ γ
⊢ a✝ ∈ {in₀ ?m.58857, in₁ ?m.58870, in₂ ?m.58883} ↔ a✝ ∈ {in₂ c✝¹, in₁ b✝¹, in₀ a✝³}

Tactic:
simp only [Finset.mem_insert, Finset.mem_singleton]

Result:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
a✝⁵ : α
b✝¹ : β
c✝¹ : γ
a✝⁴ : (a✝⁵, b✝¹, c✝¹) ∈ t
a✝³ : α
b✝ : β
a✝² : (a✝³, b✝, c✝¹) ∈ t
c✝ : γ
a✝¹ : (a✝³, b✝¹, c✝) ∈ t
a✝ : α ⊕ β ⊕ γ
⊢ a✝ = in₀ ?m.58857 ∨ a✝ = in₁ ?m.58870 ∨ a✝ = in₂ ?m.58883 ↔ a✝ = in₂ c✝¹ ∨ a✝ = in₁ b✝¹ ∨ a✝ = in₀ a✝³