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 : (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
⊢ (a, b, c) ∈ t

Tactic:
assumption
-- 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
⊢ (a, b_1, c_1) ∈ t

Tactic:
assumption
-- 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
⊢ (a_1, b, c_1) ∈ t

Tactic:
assumption
-- 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
⊢ (a, b, c) ∈ t

Tactic:
assumption
-- 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
⊢ (a, b_1, c_1) ∈ t

Tactic:
assumption
-- 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
⊢ (a_1, b, c_1) ∈ t

Tactic:
assumption
-- 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
⊢ (a, b_1, c_1) ∈ t

Tactic:
assumption
-- 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
⊢ (a, b, c) ∈ t

Tactic:
assumption
-- 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
⊢ (a_1, b_1, c) ∈ t

Tactic:
assumption
-- 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
⊢ (a, b_1, c_1) ∈ t

Tactic:
assumption
-- 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
⊢ (a, b, c) ∈ t

Tactic:
assumption
-- 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
⊢ (a_1, b_1, c) ∈ t

Tactic:
assumption
-- 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
⊢ (a_1, b, c_1) ∈ t

Tactic:
assumption
-- 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
⊢ (a_1, b_1, c) ∈ t

Tactic:
assumption
-- 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
⊢ (a, b, c) ∈ t

Tactic:
assumption
-- 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
⊢ (a_1, b, c_1) ∈ t

Tactic:
assumption
-- 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
⊢ (a_1, b_1, c) ∈ t

Tactic:
assumption
-- 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
⊢ (a, b, c) ∈ t

Tactic:
assumption
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
t : Finset (α × β × γ)
a_1 a'_1 : α
b_1 b'_1 : β
c_1 c'_1 : γ
x : α × β × γ
inst_3 : DecidableEq α
inst_4 : DecidableEq β
inst_5 : DecidableEq γ
x_1 x_2 : α × β × γ
a : α
b : β
c : γ
a' : α
b' : β
c' : γ
⊢ Eq (α := Finset (α ⊕ β ⊕ γ))
      ((fun (x : α × β × γ) ↦ ({in₀ x.1, in₁ x.2.1, in₂ x.2.2} : Finset (α ⊕ β ⊕ γ))) (a, b, c))
      ((fun (x : α × β × γ) ↦ ({in₀ x.1, in₁ x.2.1, in₂ x.2.2} : Finset (α ⊕ β ⊕ γ))) (a', b', c')) →
    (a, b, c) = (a', b', c')

Tactic:
simpa only [Finset.Subset.antisymm_iff, Finset.subset_iff,
    mem_insert, mem_singleton, forall_eq_or_imp, forall_eq, Prod.mk_inj, or_false, false_or,
    in₀, in₁, in₂, Sum.inl.inj_iff, Sum.inr.inj_iff, reduceCtorEq] using And.left

Premises used: reduceCtorEq, Finset.mem_singleton, Sum3.in₂, Prod.mk_inj, Finset.Subset.antisymm_iff, forall_eq, Sum3.in₁, Finset.mem_insert, false_or, forall_eq_or_imp, And.left, Finset.subset_iff, Sum.inr.inj_iff, Sum3.in₀, Sum.inl.inj_iff, or_false
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
x : α × β × γ
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
hx : x ∈ t
simp : (∃ (c : γ), (x.1, x.2.1, c) ∈ t) ∧ (∃ (b : β), (x.1, b, x.2.2) ∈ t) ∧ ∃ (a : α), (a, x.2.1, x.2.2) ∈ t
⊢ (graph t).IsNClique 3 ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) x)

Tactic:
simp only [toTriangle_apply, is3Clique_triple_iff, in₀₁_iff, in₀₂_iff, in₁₂_iff]

Premises used: SimpleGraph.TripartiteFromTriangles.Graph.in₀₂_iff, SimpleGraph.TripartiteFromTriangles.Graph.in₀₁_iff, SimpleGraph.TripartiteFromTriangles.Graph.in₁₂_iff, SimpleGraph.is3Clique_triple_iff, SimpleGraph.TripartiteFromTriangles.toTriangle_apply
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
x : α × β × γ
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
hx : x ∈ t
⊢ (∃ (c : γ), (x.1, x.2.1, c) ∈ t) ∧ (∃ (b : β), (x.1, b, x.2.2) ∈ t) ∧ ∃ (a : α), (a, x.2.1, x.2.2) ∈ t

Tactic:
⟨⟨_, hx⟩, ⟨_, hx⟩, _, hx⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
x : α × β × γ
inst : DecidableEq α
inst_1 : DecidableEq β
inst_2 : DecidableEq γ
hx : x ∈ t
⊢ (∃ (c : γ), (x.1, x.2.1, c) ∈ t) ∧ (∃ (b : β), (x.1, b, x.2.2) ∈ t) ∧ ∃ (a : α), (a, x.2.1, x.2.2) ∈ t

Tactic:
exact ⟨⟨_, hx⟩, ⟨_, hx⟩, _, hx⟩
-- 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 γ
x y : α ⊕ β ⊕ γ
hxy : (graph t).Adj x y
in₀₁ :
  ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄,
    (a, b, c) ∈ t →
      ∃ z ∈ t,
        Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
            ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₀ a) ∧
          Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
            ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₁ b)
in₁₀ :
  ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄,
    (a, b, c) ∈ t →
      ∃ z ∈ t,
        Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
            ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₁ b) ∧
          Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
            ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₀ a)
in₀₂ :
  ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄,
    (a, b, c) ∈ t →
      ∃ z ∈ t,
        Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
            ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₀ a) ∧
          Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
            ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₂ c)
in₂₀ :
  ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄,
    (a, b, c) ∈ t →
      ∃ z ∈ t,
        Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
            ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₂ c) ∧
          Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
            ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₀ a)
in₁₂ :
  ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄,
    (a, b, c) ∈ t →
      ∃ z ∈ t,
        Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
            ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₁ b) ∧
          Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
            ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₂ c)
in₂₁ :
  ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄,
    (a, b, c) ∈ t →
      ∃ z ∈ t,
        Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
            ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₂ c) ∧
          Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
            ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₁ b)
⊢ ∃ z ∈ t,
    Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
        ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) x ∧
      Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
        ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) y

Tactic:
cases hxy
-- 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
⊢ Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
      ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) (a, b, c) : Finset (α ⊕ β ⊕ γ)) (in₀ a) ∧
    Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
      ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) (a, b, c) : Finset (α ⊕ β ⊕ γ)) (in₁ b)

Tactic:
simp
-- 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
⊢ ∃ z ∈ t,
    Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
        ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₀ a) ∧
      Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
        ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₁ b)

Tactic:
exact ⟨_, ‹_›, by simp⟩
-- 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
⊢ Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
      ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) (a, b, c) : Finset (α ⊕ β ⊕ γ)) (in₁ b) ∧
    Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
      ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) (a, b, c) : Finset (α ⊕ β ⊕ γ)) (in₀ a)

Tactic:
simp
-- 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
⊢ ∃ z ∈ t,
    Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
        ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₁ b) ∧
      Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
        ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₀ a)

Tactic:
exact ⟨_, ‹_›, by simp⟩
-- 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
⊢ Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
      ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) (a, b, c) : Finset (α ⊕ β ⊕ γ)) (in₀ a) ∧
    Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
      ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) (a, b, c) : Finset (α ⊕ β ⊕ γ)) (in₂ c)

Tactic:
simp
-- 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
⊢ ∃ z ∈ t,
    Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
        ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₀ a) ∧
      Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
        ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₂ c)

Tactic:
exact ⟨_, ‹_›, by simp⟩
-- 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
⊢ Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
      ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) (a, b, c) : Finset (α ⊕ β ⊕ γ)) (in₂ c) ∧
    Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
      ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) (a, b, c) : Finset (α ⊕ β ⊕ γ)) (in₀ a)

Tactic:
simp
-- 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
⊢ ∃ z ∈ t,
    Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
        ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₂ c) ∧
      Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
        ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₀ a)

Tactic:
exact ⟨_, ‹_›, by simp⟩
-- 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
⊢ Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
      ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) (a, b, c) : Finset (α ⊕ β ⊕ γ)) (in₁ b) ∧
    Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
      ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) (a, b, c) : Finset (α ⊕ β ⊕ γ)) (in₂ c)

Tactic:
simp
-- 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
⊢ ∃ z ∈ t,
    Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
        ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₁ b) ∧
      Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
        ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₂ c)

Tactic:
exact ⟨_, ‹_›, by simp⟩
-- 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
⊢ Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
      ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) (a, b, c) : Finset (α ⊕ β ⊕ γ)) (in₂ c) ∧
    Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
      ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) (a, b, c) : Finset (α ⊕ β ⊕ γ)) (in₁ b)

Tactic:
simp
-- 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
⊢ ∃ z ∈ t,
    Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
        ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₂ c) ∧
      Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
        ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) (in₁ b)

Tactic:
exact ⟨_, ‹_›, by simp⟩
-- 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 γ
inst_3 : NoAccidental t
s : Finset (α ⊕ β ⊕ γ)
⊢ (graph t).IsNClique 3 s ↔ ∃ x ∈ t, (toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) x = s

Tactic:
⟨fun h ↦ ?_, ?_⟩

Premises used: Iff.intro
-- 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 γ
inst_3 : NoAccidental t
s : Finset (α ⊕ β ⊕ γ)
refine_1 : ∀ (h : (graph t).IsNClique 3 s), ∃ x ∈ t, (toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) x = s
refine_2 : (∃ x ∈ t, (toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) x = s) → (graph t).IsNClique 3 s
⊢ (graph t).IsNClique 3 s ↔ ∃ x ∈ t, (toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) x = s

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩
-- 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 γ
inst_3 : NoAccidental t
s : Finset (α ⊕ β ⊕ γ)
h : (graph t).IsNClique 3 s
⊢ ∃ (a : α ⊕ β ⊕ γ) (b : α ⊕ β ⊕ γ) (c : α ⊕ β ⊕ γ),
    (graph t).Adj a b ∧ (graph t).Adj a c ∧ (graph t).Adj b c ∧ s = {a, b, c}

Tactic:
rw [is3Clique_iff] at h

Premises used: SimpleGraph.TripartiteFromTriangles.is3Clique_iff
-- 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 γ
inst_3 : NoAccidental t
s : Finset (α ⊕ β ⊕ γ)
h :
  ∃ (a : α ⊕ β ⊕ γ) (b : α ⊕ β ⊕ γ) (c : α ⊕ β ⊕ γ),
    (graph t).Adj a b ∧ (graph t).Adj a c ∧ (graph t).Adj b c ∧ s = {a, b, c}
refine_1 :
  ∀ (x y z : α ⊕ β ⊕ γ) (hxy : (graph t).Adj x y) (hxz : (graph t).Adj x z) (hyz : (graph t).Adj y z),
    ∃ x_1 ∈ t,
      Eq (α := Finset (α ⊕ β ⊕ γ)) ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) x_1 : Finset (α ⊕ β ⊕ γ))
        ({x, y, z} : Finset (α ⊕ β ⊕ γ))
⊢ ∃ x ∈ t, (toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) x = s

Tactic:
obtain ⟨x, y, z, hxy, hxz, hyz, rfl⟩ := h

Premises used: rfl
-- 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 γ
inst_3 : NoAccidental t
x y z : α ⊕ β ⊕ γ
hxy : (graph t).Adj x y
hxz : (graph t).Adj x z
hyz : (graph t).Adj y z
refine_1 :
  ∀ (a : α) (b : β) (c : γ) (habc : Eq (α := Finset (α ⊕ β ⊕ γ)) {in₀ a, in₁ b, in₂ c} {x, y, z})
    (hab : (graph t).Adj (in₀ a) (in₁ b)) (hac : (graph t).Adj (in₀ a) (in₂ c)) (hbc : (graph t).Adj (in₁ b) (in₂ c)),
    ∃ x_1 ∈ t,
      Eq (α := Finset (α ⊕ β ⊕ γ)) ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) x_1 : Finset (α ⊕ β ⊕ γ))
        ({x, y, z} : Finset (α ⊕ β ⊕ γ))
⊢ ∃ x_1 ∈ t,
    Eq (α := Finset (α ⊕ β ⊕ γ)) ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) x_1 : Finset (α ⊕ β ⊕ γ))
      ({x, y, z} : Finset (α ⊕ β ⊕ γ))

Tactic:
obtain ⟨a, b, c, habc, hab, hac, hbc⟩ := graph_triple hxy hxz hyz

Premises used: SimpleGraph.TripartiteFromTriangles.graph_triple
-- 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 γ
inst_3 : NoAccidental t
x y z : α ⊕ β ⊕ γ
hxy : (graph t).Adj x y
hxz : (graph t).Adj x z
hyz : (graph t).Adj y z
a : α
b : β
c : γ
habc : Eq (α := Finset (α ⊕ β ⊕ γ)) {in₀ a, in₁ b, in₂ c} {x, y, z}
hab : (graph t).Adj (in₀ a) (in₁ b)
hac : (graph t).Adj (in₀ a) (in₂ c)
hbc : (graph t).Adj (in₁ b) (in₂ c)
⊢ ∃ x_1 ∈ t,
    Eq (α := Finset (α ⊕ β ⊕ γ)) ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) x_1 : Finset (α ⊕ β ⊕ γ))
      ({x, y, z} : Finset (α ⊕ β ⊕ γ))

Tactic:
⟨(a, b, c), ?_, habc⟩

Premises used: Prod.mk, And.intro, Exists.intro
-- 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 γ
inst_3 : NoAccidental t
x y z : α ⊕ β ⊕ γ
hxy : (graph t).Adj x y
hxz : (graph t).Adj x z
hyz : (graph t).Adj y z
a : α
b : β
c : γ
habc : Eq (α := Finset (α ⊕ β ⊕ γ)) {in₀ a, in₁ b, in₂ c} {x, y, z}
hab : (graph t).Adj (in₀ a) (in₁ b)
hac : (graph t).Adj (in₀ a) (in₂ c)
hbc : (graph t).Adj (in₁ b) (in₂ c)
refine_1 : (a, b, c) ∈ t
⊢ ∃ x_1 ∈ t,
    Eq (α := Finset (α ⊕ β ⊕ γ)) ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) x_1 : Finset (α ⊕ β ⊕ γ))
      ({x, y, z} : Finset (α ⊕ β ⊕ γ))

Tactic:
refine ⟨(a, b, c), ?_, habc⟩
-- 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 γ
inst_3 : NoAccidental t
x y z : α ⊕ β ⊕ γ
hxy : (graph t).Adj x y
hxz : (graph t).Adj x z
hyz : (graph t).Adj y z
a : α
b : β
c : γ
habc : Eq (α := Finset (α ⊕ β ⊕ γ)) {in₀ a, in₁ b, in₂ c} {x, y, z}
hab : (graph t).Adj (in₀ a) (in₁ b)
hac : (graph t).Adj (in₀ a) (in₂ c)
hbc : (graph t).Adj (in₁ b) (in₂ c)
refine_1 : ∀ (c' : γ) (hc' : (a, b, c') ∈ t), (a, b, c) ∈ t
⊢ (a, b, c) ∈ t

Tactic:
obtain ⟨c', hc'⟩ := in₀₁_iff.1 hab

Premises used: SimpleGraph.TripartiteFromTriangles.Graph.in₀₁_iff, Iff.mp