awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
a : α
b : β
c : γ
h_1 : (a, b, c) ∈ t
a_1 : α
b_1 : β
h_2 : (a_1, b_1, c) ∈ t
c_1 : γ
h_3 : (a, b_1, c_1) ∈ t
a_2 : α ⊕ β ⊕ γ
h : a_2 = in₀ a ∨ a_2 = in₁ b_1 ∨ a_2 = in₂ c → a_2 = in₂ c ∨ a_2 = in₀ a ∨ a_2 = in₁ b_1
h₁ : a_2 = in₂ c ∨ a_2 = in₀ a ∨ a_2 = in₁ b_1 → a_2 = in₀ a ∨ a_2 = in₁ b_1 ∨ a_2 = in₂ c
h₂ : a_2 = in₀ a → a_2 = in₂ c ∨ a_2 = in₀ a ∨ a_2 = in₁ b_1
h₃ : a_2 = in₁ b_1 → a_2 = in₂ c ∨ a_2 = in₀ a ∨ a_2 = in₁ b_1
h₄ : a_2 = in₂ c → a_2 = in₂ c ∨ a_2 = in₀ a ∨ a_2 = in₁ b_1
h₅ : a_2 = in₀ a → a_2 = in₂ c ∨ a_2 = in₀ a ∨ a_2 = in₁ b_1
h₆ : a_2 = in₁ b_1 → a_2 = in₂ c ∨ a_2 = in₀ a ∨ a_2 = in₁ b_1
h₇ : a_2 = in₂ c → a_2 = in₂ c ∨ a_2 = in₀ a ∨ a_2 = in₁ b_1
h₈ : a_2 = in₀ a → ¬a_2 = in₂ c → a_2 = in₀ a ∨ a_2 = in₁ b_1
h₉ : a_2 = in₁ b_1 → ¬a_2 = in₂ c → a_2 = in₀ a ∨ a_2 = in₁ b_1
h₁₀ : a_2 = in₂ c → ¬a_2 = in₂ c → a_2 = in₀ a ∨ a_2 = in₁ b_1
h₁₁ : a_2 = in₂ c → a_2 = in₀ a ∨ a_2 = in₁ b_1 ∨ a_2 = in₂ c
h₁₂ : a_2 = in₀ a → a_2 = in₀ a ∨ a_2 = in₁ b_1 ∨ a_2 = in₂ c
h₁₃ : a_2 = in₁ b_1 → a_2 = in₀ a ∨ a_2 = in₁ b_1 ∨ a_2 = in₂ c
h₁₄ : a_2 = in₂ c → a_2 = in₀ a ∨ a_2 = in₁ b_1 ∨ a_2 = in₂ c
h₁₅ : a_2 = in₀ a → a_2 = in₀ a ∨ a_2 = in₁ b_1 ∨ a_2 = in₂ c
h₁₆ : a_2 = in₁ b_1 → a_2 = in₀ a ∨ a_2 = in₁ b_1 ∨ a_2 = in₂ c
h₁₇ : a_2 = in₂ c → ¬a_2 = in₀ a → a_2 = in₁ b_1 ∨ a_2 = in₂ c
h₁₈ : a_2 = in₀ a → ¬a_2 = in₀ a → a_2 = in₁ b_1 ∨ a_2 = in₂ c
h₁₉ : a_2 = in₁ b_1 → ¬a_2 = in₀ a → a_2 = in₁ b_1 ∨ a_2 = in₂ c
h₂₀ h₂₁ : a_2 = in₀ a → ¬a_2 = in₂ c → a_2 = in₀ a ∨ a_2 = in₁ b_1
h₂₂ : a_2 = in₀ a → ¬a_2 = in₂ c → ¬a_2 = in₀ a → a_2 = in₁ b_1
h₂₃ h₂₄ : a_2 = in₁ b_1 → ¬a_2 = in₂ c → a_2 = in₀ a ∨ a_2 = in₁ b_1
h₂₅ : a_2 = in₁ b_1 → ¬a_2 = in₂ c → ¬a_2 = in₀ a → a_2 = in₁ b_1
h₂₆ : a_2 = in₂ c → ¬a_2 = in₂ c → a_2 = in₀ a ∨ a_2 = in₁ b_1
h₂₇ h₂₈ : a_2 = in₂ c → ¬a_2 = in₀ a → a_2 = in₁ b_1 ∨ a_2 = in₂ c
h₂₉ : a_2 = in₂ c → ¬a_2 = in₀ a → ¬a_2 = in₁ b_1 → a_2 = in₂ c
h₃₀ : a_2 = in₀ a → ¬a_2 = in₀ a → a_2 = in₁ b_1 ∨ a_2 = in₂ c
h₃₁ h₃₂ : a_2 = in₁ b_1 → ¬a_2 = in₀ a → a_2 = in₁ b_1 ∨ a_2 = in₂ c
h₃₃ : a_2 = in₁ b_1 → ¬a_2 = in₀ a → ¬a_2 = in₁ b_1 → a_2 = in₂ c
h₃₄ : a_2 = in₀ a → ¬a_2 = in₂ c → ¬a_2 = in₀ a → a_2 = in₁ b_1
h₃₅ : a_2 = in₁ b_1 → ¬a_2 = in₀ a → ¬a_2 = in₁ b_1 → a_2 = in₂ c
⊢ a_2 = in₀ a ∨ a_2 = in₁ b_1 ∨ a_2 = in₂ c ↔ a_2 = in₂ c ∨ a_2 = in₀ a ∨ a_2 = in₁ b_1

Tactic:
try tauto
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
a : α
b : β
c : γ
h : (a, b, c) ∈ t
a_1 : α
b_1 : β
h_1 : (a_1, b_1, c) ∈ t
c_1 : γ
h_2 : (a, b_1, c_1) ∈ t
in₂₀ : (graph t).Adj (in₀ a) (in₁ b_1)
in₂₁ : (graph t).Adj (in₀ a) (in₂ c)
in₂₂ : (graph t).Adj (in₁ b_1) (in₂ c)
⊢ ∃ (a_2 : α) (b : β) (c_2 : γ),
    Eq (α := Finset (α ⊕ β ⊕ γ)) {in₀ a_2, in₁ b, in₂ c_2} {in₂ c, in₀ a, in₁ b_1} ∧
      (graph t).Adj (in₀ a_2) (in₁ b) ∧ (graph t).Adj (in₀ a_2) (in₂ c_2) ∧ (graph t).Adj (in₁ b) (in₂ c_2)

Tactic:
refine ⟨_, _, _, by ext; simp only [Finset.mem_insert, Finset.mem_singleton]; try tauto,
      ?_, ?_, ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
a : α
b : β
c : γ
h_1 : (a, b, c) ∈ t
a_1 : α
c_1 : γ
h_2 : (a_1, b, c_1) ∈ t
b_1 : β
h_3 : (a_1, b_1, c) ∈ t
h :
  ∀ (a : α ⊕ β ⊕ γ),
    Membership.mem (γ := Finset (α ⊕ β ⊕ γ)) {in₀ a_1, in₁ b, in₂ c} a ↔
      Membership.mem (γ := Finset (α ⊕ β ⊕ γ)) {in₁ b, in₂ c, in₀ a_1} a
⊢ Eq (α := Finset (α ⊕ β ⊕ γ)) {in₀ a_1, in₁ b, in₂ c} {in₁ b, in₂ c, in₀ a_1}

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
a : α
b : β
c : γ
h_1 : (a, b, c) ∈ t
a_1 : α
c_1 : γ
h_2 : (a_1, b, c_1) ∈ t
b_1 : β
h_3 : (a_1, b_1, c) ∈ t
a_2 : α ⊕ β ⊕ γ
h : a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c ↔ a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
⊢ Membership.mem (γ := Finset (α ⊕ β ⊕ γ)) {in₀ a_1, in₁ b, in₂ c} a_2 ↔
    Membership.mem (γ := Finset (α ⊕ β ⊕ γ)) {in₁ b, in₂ c, in₀ a_1} a_2

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

Premises used: Finset.mem_singleton, Finset.mem_insert
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
a : α
b : β
c : γ
h_1 : (a, b, c) ∈ t
a_1 : α
c_1 : γ
h_2 : (a_1, b, c_1) ∈ t
b_1 : β
h_3 : (a_1, b_1, c) ∈ t
a_2 : α ⊕ β ⊕ γ
h : a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₁ : a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1 → a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c
h₂ : a_2 = in₀ a_1 → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₃ : a_2 = in₁ b → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₄ : a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₅ : a_2 = in₀ a_1 → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₆ : a_2 = in₁ b → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₇ : a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₈ : a_2 = in₀ a_1 → ¬a_2 = in₁ b → a_2 = in₂ c ∨ a_2 = in₀ a_1
h₉ : a_2 = in₁ b → ¬a_2 = in₁ b → a_2 = in₂ c ∨ a_2 = in₀ a_1
h₁₀ : a_2 = in₂ c → ¬a_2 = in₁ b → a_2 = in₂ c ∨ a_2 = in₀ a_1
h₁₁ : a_2 = in₁ b → a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c
h₁₂ : a_2 = in₂ c → a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c
h₁₃ : a_2 = in₀ a_1 → a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c
h₁₄ : a_2 = in₁ b → a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c
h₁₅ : a_2 = in₂ c → a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c
h₁₆ : a_2 = in₀ a_1 → a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c
h₁₇ : a_2 = in₁ b → ¬a_2 = in₀ a_1 → a_2 = in₁ b ∨ a_2 = in₂ c
h₁₈ : a_2 = in₂ c → ¬a_2 = in₀ a_1 → a_2 = in₁ b ∨ a_2 = in₂ c
h₁₉ : a_2 = in₀ a_1 → ¬a_2 = in₀ a_1 → a_2 = in₁ b ∨ a_2 = in₂ c
h₂₀ h₂₁ : a_2 = in₀ a_1 → ¬a_2 = in₁ b → a_2 = in₂ c ∨ a_2 = in₀ a_1
h₂₂ : a_2 = in₀ a_1 → ¬a_2 = in₁ b → ¬a_2 = in₂ c → a_2 = in₀ a_1
h₂₃ : a_2 = in₁ b → ¬a_2 = in₁ b → a_2 = in₂ c ∨ a_2 = in₀ a_1
h₂₄ h₂₅ : a_2 = in₂ c → ¬a_2 = in₁ b → a_2 = in₂ c ∨ a_2 = in₀ a_1
h₂₆ : a_2 = in₂ c → ¬a_2 = in₁ b → ¬a_2 = in₂ c → a_2 = in₀ a_1
h₂₇ h₂₈ : a_2 = in₁ b → ¬a_2 = in₀ a_1 → a_2 = in₁ b ∨ a_2 = in₂ c
h₂₉ : a_2 = in₁ b → ¬a_2 = in₀ a_1 → ¬a_2 = in₁ b → a_2 = in₂ c
h₃₀ h₃₁ : a_2 = in₂ c → ¬a_2 = in₀ a_1 → a_2 = in₁ b ∨ a_2 = in₂ c
h₃₂ : a_2 = in₂ c → ¬a_2 = in₀ a_1 → ¬a_2 = in₁ b → a_2 = in₂ c
h₃₃ : a_2 = in₀ a_1 → ¬a_2 = in₀ a_1 → a_2 = in₁ b ∨ a_2 = in₂ c
h₃₄ : a_2 = in₂ c → ¬a_2 = in₁ b → ¬a_2 = in₂ c → a_2 = in₀ a_1
h₃₅ : a_2 = in₁ b → ¬a_2 = in₀ a_1 → ¬a_2 = in₁ b → a_2 = in₂ c
⊢ a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c ↔ a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1

Tactic:
tauto
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
a : α
b : β
c : γ
h_1 : (a, b, c) ∈ t
a_1 : α
c_1 : γ
h_2 : (a_1, b, c_1) ∈ t
b_1 : β
h_3 : (a_1, b_1, c) ∈ t
a_2 : α ⊕ β ⊕ γ
h : a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₁ : a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1 → a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c
h₂ : a_2 = in₀ a_1 → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₃ : a_2 = in₁ b → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₄ : a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₅ : a_2 = in₀ a_1 → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₆ : a_2 = in₁ b → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₇ : a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1
h₈ : a_2 = in₀ a_1 → ¬a_2 = in₁ b → a_2 = in₂ c ∨ a_2 = in₀ a_1
h₉ : a_2 = in₁ b → ¬a_2 = in₁ b → a_2 = in₂ c ∨ a_2 = in₀ a_1
h₁₀ : a_2 = in₂ c → ¬a_2 = in₁ b → a_2 = in₂ c ∨ a_2 = in₀ a_1
h₁₁ : a_2 = in₁ b → a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c
h₁₂ : a_2 = in₂ c → a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c
h₁₃ : a_2 = in₀ a_1 → a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c
h₁₄ : a_2 = in₁ b → a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c
h₁₅ : a_2 = in₂ c → a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c
h₁₆ : a_2 = in₀ a_1 → a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c
h₁₇ : a_2 = in₁ b → ¬a_2 = in₀ a_1 → a_2 = in₁ b ∨ a_2 = in₂ c
h₁₈ : a_2 = in₂ c → ¬a_2 = in₀ a_1 → a_2 = in₁ b ∨ a_2 = in₂ c
h₁₉ : a_2 = in₀ a_1 → ¬a_2 = in₀ a_1 → a_2 = in₁ b ∨ a_2 = in₂ c
h₂₀ h₂₁ : a_2 = in₀ a_1 → ¬a_2 = in₁ b → a_2 = in₂ c ∨ a_2 = in₀ a_1
h₂₂ : a_2 = in₀ a_1 → ¬a_2 = in₁ b → ¬a_2 = in₂ c → a_2 = in₀ a_1
h₂₃ : a_2 = in₁ b → ¬a_2 = in₁ b → a_2 = in₂ c ∨ a_2 = in₀ a_1
h₂₄ h₂₅ : a_2 = in₂ c → ¬a_2 = in₁ b → a_2 = in₂ c ∨ a_2 = in₀ a_1
h₂₆ : a_2 = in₂ c → ¬a_2 = in₁ b → ¬a_2 = in₂ c → a_2 = in₀ a_1
h₂₇ h₂₈ : a_2 = in₁ b → ¬a_2 = in₀ a_1 → a_2 = in₁ b ∨ a_2 = in₂ c
h₂₉ : a_2 = in₁ b → ¬a_2 = in₀ a_1 → ¬a_2 = in₁ b → a_2 = in₂ c
h₃₀ h₃₁ : a_2 = in₂ c → ¬a_2 = in₀ a_1 → a_2 = in₁ b ∨ a_2 = in₂ c
h₃₂ : a_2 = in₂ c → ¬a_2 = in₀ a_1 → ¬a_2 = in₁ b → a_2 = in₂ c
h₃₃ : a_2 = in₀ a_1 → ¬a_2 = in₀ a_1 → a_2 = in₁ b ∨ a_2 = in₂ c
h₃₄ : a_2 = in₂ c → ¬a_2 = in₁ b → ¬a_2 = in₂ c → a_2 = in₀ a_1
h₃₅ : a_2 = in₁ b → ¬a_2 = in₀ a_1 → ¬a_2 = in₁ b → a_2 = in₂ c
⊢ a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c ↔ a_2 = in₁ b ∨ a_2 = in₂ c ∨ a_2 = in₀ a_1

Tactic:
try tauto
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
a : α
b : β
c : γ
h : (a, b, c) ∈ t
a_1 : α
c_1 : γ
h_1 : (a_1, b, c_1) ∈ t
b_1 : β
h_2 : (a_1, b_1, c) ∈ t
in₁₂ : (graph t).Adj (in₀ a_1) (in₁ b)
in₁₃ : (graph t).Adj (in₀ a_1) (in₂ c)
in₁₄ : (graph t).Adj (in₁ b) (in₂ c)
⊢ ∃ (a : α) (b_2 : β) (c_2 : γ),
    Eq (α := Finset (α ⊕ β ⊕ γ)) {in₀ a, in₁ b_2, in₂ c_2} {in₁ b, in₂ c, in₀ a_1} ∧
      (graph t).Adj (in₀ a) (in₁ b_2) ∧ (graph t).Adj (in₀ a) (in₂ c_2) ∧ (graph t).Adj (in₁ b_2) (in₂ c_2)

Tactic:
refine ⟨_, _, _, by ext; simp only [Finset.mem_insert, Finset.mem_singleton]; try tauto,
      ?_, ?_, ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
a : α
b : β
c : γ
h_1 : (a, b, c) ∈ t
a_1 : α
b_1 : β
h_2 : (a_1, b_1, c) ∈ t
c_1 : γ
h_3 : (a_1, b, c_1) ∈ t
h :
  ∀ (a : α ⊕ β ⊕ γ),
    Membership.mem (γ := Finset (α ⊕ β ⊕ γ)) {in₀ a_1, in₁ b, in₂ c} a ↔
      Membership.mem (γ := Finset (α ⊕ β ⊕ γ)) {in₂ c, in₁ b, in₀ a_1} a
⊢ Eq (α := Finset (α ⊕ β ⊕ γ)) {in₀ a_1, in₁ b, in₂ c} {in₂ c, in₁ b, in₀ a_1}

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
a : α
b : β
c : γ
h_1 : (a, b, c) ∈ t
a_1 : α
b_1 : β
h_2 : (a_1, b_1, c) ∈ t
c_1 : γ
h_3 : (a_1, b, c_1) ∈ t
a_2 : α ⊕ β ⊕ γ
h : a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c ↔ a_2 = in₂ c ∨ a_2 = in₁ b ∨ a_2 = in₀ a_1
⊢ Membership.mem (γ := Finset (α ⊕ β ⊕ γ)) {in₀ a_1, in₁ b, in₂ c} a_2 ↔
    Membership.mem (γ := Finset (α ⊕ β ⊕ γ)) {in₂ c, in₁ b, in₀ a_1} a_2

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

Premises used: Finset.mem_singleton, Finset.mem_insert
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
a : α
b : β
c : γ
h_1 : (a, b, c) ∈ t
a_1 : α
b_1 : β
h_2 : (a_1, b_1, c) ∈ t
c_1 : γ
h_3 : (a_1, b, c_1) ∈ t
a_2 : α ⊕ β ⊕ γ
h : a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c → a_2 = in₂ c ∨ a_2 = in₁ b ∨ a_2 = in₀ a_1
h₁ : a_2 = in₂ c ∨ a_2 = in₁ b ∨ a_2 = in₀ a_1 → a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c
h₂ : a_2 = in₀ a_1 → a_2 = in₂ c ∨ a_2 = in₁ b ∨ a_2 = in₀ a_1
h₃ : a_2 = in₁ b → a_2 = in₂ c ∨ a_2 = in₁ b ∨ a_2 = in₀ a_1
h₄ : a_2 = in₂ c → a_2 = in₂ c ∨ a_2 = in₁ b ∨ a_2 = in₀ a_1
h₅ : a_2 = in₀ a_1 → a_2 = in₂ c ∨ a_2 = in₁ b ∨ a_2 = in₀ a_1
h₆ : a_2 = in₁ b → a_2 = in₂ c ∨ a_2 = in₁ b ∨ a_2 = in₀ a_1
h₇ : a_2 = in₂ c → a_2 = in₂ c ∨ a_2 = in₁ b ∨ a_2 = in₀ a_1
h₈ : a_2 = in₀ a_1 → ¬a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₀ a_1
h₉ : a_2 = in₁ b → ¬a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₀ a_1
h₁₀ : a_2 = in₂ c → ¬a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₀ a_1
h₁₁ : a_2 = in₂ c → a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c
h₁₂ : a_2 = in₁ b → a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c
h₁₃ : a_2 = in₀ a_1 → a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c
h₁₄ : a_2 = in₂ c → a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c
h₁₅ : a_2 = in₁ b → a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c
h₁₆ : a_2 = in₀ a_1 → a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c
h₁₇ : a_2 = in₂ c → ¬a_2 = in₀ a_1 → a_2 = in₁ b ∨ a_2 = in₂ c
h₁₈ : a_2 = in₁ b → ¬a_2 = in₀ a_1 → a_2 = in₁ b ∨ a_2 = in₂ c
h₁₉ : a_2 = in₀ a_1 → ¬a_2 = in₀ a_1 → a_2 = in₁ b ∨ a_2 = in₂ c
h₂₀ h₂₁ : a_2 = in₀ a_1 → ¬a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₀ a_1
h₂₂ : a_2 = in₀ a_1 → ¬a_2 = in₂ c → ¬a_2 = in₁ b → a_2 = in₀ a_1
h₂₃ h₂₄ : a_2 = in₁ b → ¬a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₀ a_1
h₂₅ : a_2 = in₁ b → ¬a_2 = in₂ c → ¬a_2 = in₁ b → a_2 = in₀ a_1
h₂₆ : a_2 = in₂ c → ¬a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₀ a_1
h₂₇ h₂₈ : a_2 = in₂ c → ¬a_2 = in₀ a_1 → a_2 = in₁ b ∨ a_2 = in₂ c
h₂₉ : a_2 = in₂ c → ¬a_2 = in₀ a_1 → ¬a_2 = in₁ b → a_2 = in₂ c
h₃₀ h₃₁ : a_2 = in₁ b → ¬a_2 = in₀ a_1 → a_2 = in₁ b ∨ a_2 = in₂ c
h₃₂ : a_2 = in₁ b → ¬a_2 = in₀ a_1 → ¬a_2 = in₁ b → a_2 = in₂ c
h₃₃ : a_2 = in₀ a_1 → ¬a_2 = in₀ a_1 → a_2 = in₁ b ∨ a_2 = in₂ c
h₃₄ : a_2 = in₁ b → ¬a_2 = in₂ c → ¬a_2 = in₁ b → a_2 = in₀ a_1
h₃₅ : a_2 = in₁ b → ¬a_2 = in₀ a_1 → ¬a_2 = in₁ b → a_2 = in₂ c
⊢ a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c ↔ a_2 = in₂ c ∨ a_2 = in₁ b ∨ a_2 = in₀ a_1

Tactic:
tauto
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
a : α
b : β
c : γ
h_1 : (a, b, c) ∈ t
a_1 : α
b_1 : β
h_2 : (a_1, b_1, c) ∈ t
c_1 : γ
h_3 : (a_1, b, c_1) ∈ t
a_2 : α ⊕ β ⊕ γ
h : a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c → a_2 = in₂ c ∨ a_2 = in₁ b ∨ a_2 = in₀ a_1
h₁ : a_2 = in₂ c ∨ a_2 = in₁ b ∨ a_2 = in₀ a_1 → a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c
h₂ : a_2 = in₀ a_1 → a_2 = in₂ c ∨ a_2 = in₁ b ∨ a_2 = in₀ a_1
h₃ : a_2 = in₁ b → a_2 = in₂ c ∨ a_2 = in₁ b ∨ a_2 = in₀ a_1
h₄ : a_2 = in₂ c → a_2 = in₂ c ∨ a_2 = in₁ b ∨ a_2 = in₀ a_1
h₅ : a_2 = in₀ a_1 → a_2 = in₂ c ∨ a_2 = in₁ b ∨ a_2 = in₀ a_1
h₆ : a_2 = in₁ b → a_2 = in₂ c ∨ a_2 = in₁ b ∨ a_2 = in₀ a_1
h₇ : a_2 = in₂ c → a_2 = in₂ c ∨ a_2 = in₁ b ∨ a_2 = in₀ a_1
h₈ : a_2 = in₀ a_1 → ¬a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₀ a_1
h₉ : a_2 = in₁ b → ¬a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₀ a_1
h₁₀ : a_2 = in₂ c → ¬a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₀ a_1
h₁₁ : a_2 = in₂ c → a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c
h₁₂ : a_2 = in₁ b → a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c
h₁₃ : a_2 = in₀ a_1 → a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c
h₁₄ : a_2 = in₂ c → a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c
h₁₅ : a_2 = in₁ b → a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c
h₁₆ : a_2 = in₀ a_1 → a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c
h₁₇ : a_2 = in₂ c → ¬a_2 = in₀ a_1 → a_2 = in₁ b ∨ a_2 = in₂ c
h₁₈ : a_2 = in₁ b → ¬a_2 = in₀ a_1 → a_2 = in₁ b ∨ a_2 = in₂ c
h₁₉ : a_2 = in₀ a_1 → ¬a_2 = in₀ a_1 → a_2 = in₁ b ∨ a_2 = in₂ c
h₂₀ h₂₁ : a_2 = in₀ a_1 → ¬a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₀ a_1
h₂₂ : a_2 = in₀ a_1 → ¬a_2 = in₂ c → ¬a_2 = in₁ b → a_2 = in₀ a_1
h₂₃ h₂₄ : a_2 = in₁ b → ¬a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₀ a_1
h₂₅ : a_2 = in₁ b → ¬a_2 = in₂ c → ¬a_2 = in₁ b → a_2 = in₀ a_1
h₂₆ : a_2 = in₂ c → ¬a_2 = in₂ c → a_2 = in₁ b ∨ a_2 = in₀ a_1
h₂₇ h₂₈ : a_2 = in₂ c → ¬a_2 = in₀ a_1 → a_2 = in₁ b ∨ a_2 = in₂ c
h₂₉ : a_2 = in₂ c → ¬a_2 = in₀ a_1 → ¬a_2 = in₁ b → a_2 = in₂ c
h₃₀ h₃₁ : a_2 = in₁ b → ¬a_2 = in₀ a_1 → a_2 = in₁ b ∨ a_2 = in₂ c
h₃₂ : a_2 = in₁ b → ¬a_2 = in₀ a_1 → ¬a_2 = in₁ b → a_2 = in₂ c
h₃₃ : a_2 = in₀ a_1 → ¬a_2 = in₀ a_1 → a_2 = in₁ b ∨ a_2 = in₂ c
h₃₄ : a_2 = in₁ b → ¬a_2 = in₂ c → ¬a_2 = in₁ b → a_2 = in₀ a_1
h₃₅ : a_2 = in₁ b → ¬a_2 = in₀ a_1 → ¬a_2 = in₁ b → a_2 = in₂ c
⊢ a_2 = in₀ a_1 ∨ a_2 = in₁ b ∨ a_2 = in₂ c ↔ a_2 = in₂ c ∨ a_2 = in₁ b ∨ a_2 = in₀ a_1

Tactic:
try tauto
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
a : α
b : β
c : γ
h : (a, b, c) ∈ t
a_1 : α
b_1 : β
h_1 : (a_1, b_1, c) ∈ t
c_1 : γ
h_2 : (a_1, b, c_1) ∈ t
in₂₁ : (graph t).Adj (in₀ a_1) (in₁ b)
in₂₂ : (graph t).Adj (in₀ a_1) (in₂ c)
in₂₃ : (graph t).Adj (in₁ b) (in₂ c)
⊢ ∃ (a : α) (b_2 : β) (c_2 : γ),
    Eq (α := Finset (α ⊕ β ⊕ γ)) {in₀ a, in₁ b_2, in₂ c_2} {in₂ c, in₁ b, in₀ a_1} ∧
      (graph t).Adj (in₀ a) (in₁ b_2) ∧ (graph t).Adj (in₀ a) (in₂ c_2) ∧ (graph t).Adj (in₁ b_2) (in₂ c_2)

Tactic:
refine ⟨_, _, _, by ext; simp only [Finset.mem_insert, Finset.mem_singleton]; try tauto,
      ?_, ?_, ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
a : α
b : β
c : γ
h : (a, b, c) ∈ t
b_1 : β
c_1 : γ
h_1 : (a, b_1, c_1) ∈ t
a_1 : α
h_2 : (a_1, b, c_1) ∈ t
in₀₁ : (a, b, c) ∈ t
in₂ : γ
⊢ (graph t).Adj (in₀ a) (in₁ b)

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
a : α
b : β
c : γ
h : (a, b, c) ∈ t
b_1 : β
c_1 : γ
h_1 : (a, b_1, c_1) ∈ t
a_1 : α
h_2 : (a_1, b, c_1) ∈ t
in₀₁ : (a, b_1, c_1) ∈ t
in₂ : β
⊢ (graph t).Adj (in₀ a) (Sum3.in₂ c_1)

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
a : α
b : β
c : γ
h : (a, b, c) ∈ t
b_1 : β
c_1 : γ
h_1 : (a, b_1, c_1) ∈ t
a_1 : α
h_2 in₀₁ : (a_1, b, c_1) ∈ t
in₂ : α
⊢ (graph t).Adj (in₁ b) (Sum3.in₂ c_1)

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
a : α
b : β
c : γ
h : (a, b, c) ∈ t
a_1 : α
c_1 : γ
h_1 : (a_1, b, c_1) ∈ t
b_1 : β
h_2 : (a, b_1, c_1) ∈ t
in₁₀ : (a, b, c) ∈ t
in₁₁ : γ
⊢ (graph t).Adj (in₀ a) (in₁ b)

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
a : α
b : β
c : γ
h : (a, b, c) ∈ t
a_1 : α
c_1 : γ
h_1 : (a_1, b, c_1) ∈ t
b_1 : β
h_2 in₁₀ : (a, b_1, c_1) ∈ t
in₁₁ : β
⊢ (graph t).Adj (in₀ a) (in₂ c_1)

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
a : α
b : β
c : γ
h : (a, b, c) ∈ t
a_1 : α
c_1 : γ
h_1 : (a_1, b, c_1) ∈ t
b_1 : β
h_2 : (a, b_1, c_1) ∈ t
in₁₀ : (a_1, b, c_1) ∈ t
in₁₁ : α
⊢ (graph t).Adj (in₁ b) (in₂ c_1)

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
a : α
b : β
c : γ
h : (a, b, c) ∈ t
b_1 : β
c_1 : γ
h_1 : (a, b_1, c_1) ∈ t
a_1 : α
h_2 : (a_1, b_1, c) ∈ t
in₀₂ : (a, b_1, c_1) ∈ t
in₃ : γ
⊢ (graph t).Adj (in₀ a) (in₁ b_1)

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
a : α
b : β
c : γ
h : (a, b, c) ∈ t
b_1 : β
c_1 : γ
h_1 : (a, b_1, c_1) ∈ t
a_1 : α
h_2 : (a_1, b_1, c) ∈ t
in₀₂ : (a, b, c) ∈ t
in₃ : β
⊢ (graph t).Adj (in₀ a) (in₂ c)

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
a : α
b : β
c : γ
h : (a, b, c) ∈ t
b_1 : β
c_1 : γ
h_1 : (a, b_1, c_1) ∈ t
a_1 : α
h_2 in₀₂ : (a_1, b_1, c) ∈ t
in₃ : α
⊢ (graph t).Adj (in₁ b_1) (in₂ c)

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
a : α
b : β
c : γ
h : (a, b, c) ∈ t
a_1 : α
b_1 : β
h_1 : (a_1, b_1, c) ∈ t
c_1 : γ
h_2 in₂₀ : (a, b_1, c_1) ∈ t
in₂₁ : γ
⊢ (graph t).Adj (in₀ a) (in₁ b_1)

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
a : α
b : β
c : γ
h : (a, b, c) ∈ t
a_1 : α
b_1 : β
h_1 : (a_1, b_1, c) ∈ t
c_1 : γ
h_2 : (a, b_1, c_1) ∈ t
in₂₀ : (a, b, c) ∈ t
in₂₁ : β
⊢ (graph t).Adj (in₀ a) (in₂ c)

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
a : α
b : β
c : γ
h : (a, b, c) ∈ t
a_1 : α
b_1 : β
h_1 : (a_1, b_1, c) ∈ t
c_1 : γ
h_2 : (a, b_1, c_1) ∈ t
in₂₀ : (a_1, b_1, c) ∈ t
in₂₁ : α
⊢ (graph t).Adj (in₁ b_1) (in₂ c)

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
a : α
b : β
c : γ
h : (a, b, c) ∈ t
a_1 : α
c_1 : γ
h_1 : (a_1, b, c_1) ∈ t
b_1 : β
h_2 : (a_1, b_1, c) ∈ t
in₁₂ : (a_1, b, c_1) ∈ t
in₁₃ : γ
⊢ (graph t).Adj (in₀ a_1) (in₁ b)

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
a : α
b : β
c : γ
h : (a, b, c) ∈ t
a_1 : α
c_1 : γ
h_1 : (a_1, b, c_1) ∈ t
b_1 : β
h_2 in₁₂ : (a_1, b_1, c) ∈ t
in₁₃ : β
⊢ (graph t).Adj (in₀ a_1) (in₂ c)

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
a : α
b : β
c : γ
h : (a, b, c) ∈ t
a_1 : α
c_1 : γ
h_1 : (a_1, b, c_1) ∈ t
b_1 : β
h_2 : (a_1, b_1, c) ∈ t
in₁₂ : (a, b, c) ∈ t
in₁₃ : α
⊢ (graph t).Adj (in₁ b) (in₂ c)

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
a : α
b : β
c : γ
h : (a, b, c) ∈ t
a_1 : α
b_1 : β
h_1 : (a_1, b_1, c) ∈ t
c_1 : γ
h_2 in₂₁ : (a_1, b, c_1) ∈ t
in₂₂ : γ
⊢ (graph t).Adj (in₀ a_1) (in₁ b)

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
a : α
b : β
c : γ
h : (a, b, c) ∈ t
a_1 : α
b_1 : β
h_1 : (a_1, b_1, c) ∈ t
c_1 : γ
h_2 : (a_1, b, c_1) ∈ t
in₂₁ : (a_1, b_1, c) ∈ t
in₂₂ : β
⊢ (graph t).Adj (in₀ a_1) (in₂ c)

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
a : α
b : β
c : γ
h : (a, b, c) ∈ t
a_1 : α
b_1 : β
h_1 : (a_1, b_1, c) ∈ t
c_1 : γ
h_2 : (a_1, b, c_1) ∈ t
in₂₁ : (a, b, c) ∈ t
in₂₂ : α
⊢ (graph t).Adj (in₁ b) (in₂ c)

Tactic:
constructor