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 γ
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)
c' : γ
hc' : (a, b, c') ∈ t
refine_1 : ∀ (b' : β) (hb' : (a, b', c) ∈ t), (a, b, c) ∈ t
⊢ (a, b, c) ∈ t

Tactic:
obtain ⟨b', hb'⟩ := in₀₂_iff.1 hac

Premises used: SimpleGraph.TripartiteFromTriangles.Graph.in₀₂_iff, Iff.mp
-- 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)
c' : γ
hc' : (a, b, c') ∈ t
b' : β
hb' : (a, b', c) ∈ t
refine_1 : ∀ (a' : α) (ha' : (a', b, c) ∈ t), (a, b, c) ∈ t
⊢ (a, b, c) ∈ t

Tactic:
obtain ⟨a', ha'⟩ := in₁₂_iff.1 hbc

Premises used: Iff.mp, SimpleGraph.TripartiteFromTriangles.Graph.in₁₂_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
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)
c' : γ
hc' : (a, b, c') ∈ t
b' : β
hb' : (a, b', c) ∈ t
a' : α
ha' : (a', b, c) ∈ t
refine_1 refine_1₁ refine_1₂ : ∀ (hc' : (a, b, c) ∈ t), (a, b, c) ∈ t
⊢ (a, b, c) ∈ t

Tactic:
obtain rfl | rfl | rfl := NoAccidental.eq_or_eq_or_eq ha' hb' hc'

Premises used: SimpleGraph.TripartiteFromTriangles.NoAccidental.eq_or_eq_or_eq, 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
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)
c' : γ
hc' : (a, b, c') ∈ t
b' : β
hb' : (a, b', c) ∈ t
ha' : (a, b, 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 γ
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)
c' : γ
hc' : (a, b, c') ∈ t
a' : α
ha' : (a', b, c) ∈ t
hb' : (a, b, 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 γ
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)
b' : β
hb' : (a, b', c) ∈ t
a' : α
ha' : (a', b, c) ∈ t
hc' : (a, b, 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 γ
inst_3 : NoAccidental t
x : α × β × γ
hx : x ∈ t
⊢ (graph t).IsNClique 3 ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) x)

Tactic:
toTriangle_is3Clique hx

Premises used: SimpleGraph.TripartiteFromTriangles.toTriangle_is3Clique
-- 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 : α × β × γ
hx : x ∈ t
⊢ (graph t).IsNClique 3 ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) x)

Tactic:
exact toTriangle_is3Clique hx

Premises used: SimpleGraph.TripartiteFromTriangles.toTriangle_is3Clique
-- 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
⊢ Set.SurjOn (⇑toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) (↑t : Set (α × β × γ)) ((graph t).cliqueSet 3)

Tactic:
fun _ ↦ is3Clique_iff.1

Premises used: Set.Mem, setOf, Set.SurjOn, SimpleGraph.TripartiteFromTriangles.is3Clique_iff, Set.Subset, Iff.mp, Set.image, SimpleGraph.cliqueSet
-- 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 : ExplicitDisjoint t
x : Finset (α ⊕ β ⊕ γ)
simp :
  ∀ (x_1 : α) (x_2 : β) (x_3 : γ),
    (x_1, x_2, x_3) ∈ t →
      (toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) (x_1, x_2, x_3) = x →
        ∀ ⦃y : Finset (α ⊕ β ⊕ γ)⦄ (x_4 : α) (x_5 : β) (x_6 : γ),
          (x_4, x_5, x_6) ∈ t →
            (toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) (x_4, x_5, x_6) = y →
              ¬x = y → ((↑x : Set (α ⊕ β ⊕ γ)) ∩ (↑y : Set (α ⊕ β ⊕ γ))).Subsingleton
⊢ x ∈ (↑(map toTriangle t) : Set (Finset (α ⊕ β ⊕ γ))) →
    ∀ ⦃y : Finset (α ⊕ β ⊕ γ)⦄,
      y ∈ (↑(map toTriangle t) : Set (Finset (α ⊕ β ⊕ γ))) →
        x ≠ y → (fun (x y : Finset (α ⊕ β ⊕ γ)) ↦ ((↑x : Set (α ⊕ β ⊕ γ)) ∩ (↑y : Set (α ⊕ β ⊕ γ))).Subsingleton) x y

Tactic:
simp only [Finset.coe_map, Set.mem_image, Finset.mem_coe, Prod.exists, Ne,
    forall_exists_index, and_imp]

Premises used: and_imp, Set.mem_image, forall_exists_index, Ne, Finset.coe_map, Prod.exists, Finset.mem_coe
-- 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 : ExplicitDisjoint t
a : α
b : β
c : γ
habc : (a, b, c) ∈ t
x : α
y : β
z : γ
hxyz : (x, y, z) ∈ t
h' :
  ¬Eq (α := Finset (α ⊕ β ⊕ γ)) ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) (a, b, c) : Finset (α ⊕ β ⊕ γ))
      ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) (x, y, z) : Finset (α ⊕ β ⊕ γ))
⊢ (a, b, c) ≠ (x, y, z)

Tactic:
have := ne_of_apply_ne _ 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 : ExplicitDisjoint t
a : α
b : β
c : γ
habc : (a, b, c) ∈ t
x : α
y : β
z : γ
hxyz : (x, y, z) ∈ t
h' :
  ¬Eq (α := Finset (α ⊕ β ⊕ γ)) ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) (a, b, c) : Finset (α ⊕ β ⊕ γ))
      ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) (x, y, z) : Finset (α ⊕ β ⊕ γ))
this : (a, b, c) ≠ (x, y, z)
⊢ a = x → b = y → ¬c = z

Tactic:
simp only [Ne, Prod.mk_inj, not_and] at this

Premises used: Prod.mk_inj, Ne, not_and
-- 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 : ExplicitDisjoint t
a : α
b : β
c : γ
habc : (a, b, c) ∈ t
x : α
y : β
z : γ
hxyz : (x, y, z) ∈ t
h' :
  ¬Eq (α := Finset (α ⊕ β ⊕ γ)) ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) (a, b, c) : Finset (α ⊕ β ⊕ γ))
      ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) (x, y, z) : Finset (α ⊕ β ⊕ γ))
this : a = x → b = y → ¬c = z
⊢ ¬(a = x ∧ b = y) ∧ ¬(a = x ∧ c = z) ∧ ¬(b = y ∧ c = z)

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

Premises used: And.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 : ExplicitDisjoint t
a : α
b : β
c : γ
habc : (a, b, c) ∈ t
x : α
y : β
z : γ
hxyz : (x, y, z) ∈ t
h' :
  ¬Eq (α := Finset (α ⊕ β ⊕ γ)) ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) (a, b, c) : Finset (α ⊕ β ⊕ γ))
      ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) (x, y, z) : Finset (α ⊕ β ⊕ γ))
this : a = x → b = y → ¬c = z
refine_1 : ¬(a = x ∧ b = y)
refine_2 : ¬(a = x ∧ c = z)
refine_3 : ¬(b = y ∧ c = z)
⊢ ¬(a = x ∧ b = y) ∧ ¬(a = x ∧ c = z) ∧ ¬(b = y ∧ c = z)

Tactic:
refine ⟨?_, ?_, ?_⟩
-- 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 : ExplicitDisjoint t
a : α
b : β
c : γ
habc : (a, b, c) ∈ t
z : γ
hxyz : (a, b, z) ∈ t
h' :
  ¬Eq (α := Finset (α ⊕ β ⊕ γ)) ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) (a, b, c) : Finset (α ⊕ β ⊕ γ))
      ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) (a, b, z) : Finset (α ⊕ β ⊕ γ))
this : a = a → b = b → ¬c = z
⊢ False

Tactic:
this rfl rfl (ExplicitDisjoint.inj₂ habc hxyz)

Premises used: SimpleGraph.TripartiteFromTriangles.ExplicitDisjoint.inj₂, 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 : ExplicitDisjoint t
a : α
b : β
c : γ
habc : (a, b, c) ∈ t
z : γ
hxyz : (a, b, z) ∈ t
h' :
  ¬Eq (α := Finset (α ⊕ β ⊕ γ)) ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) (a, b, c) : Finset (α ⊕ β ⊕ γ))
      ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) (a, b, z) : Finset (α ⊕ β ⊕ γ))
this : a = a → b = b → ¬c = z
⊢ False

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

Premises used: SimpleGraph.TripartiteFromTriangles.ExplicitDisjoint.inj₂, 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 : ExplicitDisjoint t
a : α
b : β
c : γ
habc : (a, b, c) ∈ t
y : β
hxyz : (a, y, c) ∈ t
h' :
  ¬Eq (α := Finset (α ⊕ β ⊕ γ)) ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) (a, b, c) : Finset (α ⊕ β ⊕ γ))
      ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) (a, y, c) : Finset (α ⊕ β ⊕ γ))
this : a = a → b = y → ¬c = c
⊢ False

Tactic:
this rfl (ExplicitDisjoint.inj₁ habc hxyz) rfl

Premises used: SimpleGraph.TripartiteFromTriangles.ExplicitDisjoint.inj₁, 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 : ExplicitDisjoint t
a : α
b : β
c : γ
habc : (a, b, c) ∈ t
y : β
hxyz : (a, y, c) ∈ t
h' :
  ¬Eq (α := Finset (α ⊕ β ⊕ γ)) ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) (a, b, c) : Finset (α ⊕ β ⊕ γ))
      ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) (a, y, c) : Finset (α ⊕ β ⊕ γ))
this : a = a → b = y → ¬c = c
⊢ False

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

Premises used: SimpleGraph.TripartiteFromTriangles.ExplicitDisjoint.inj₁, 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 : ExplicitDisjoint t
a : α
b : β
c : γ
habc : (a, b, c) ∈ t
x : α
hxyz : (x, b, c) ∈ t
h' :
  ¬Eq (α := Finset (α ⊕ β ⊕ γ)) ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) (a, b, c) : Finset (α ⊕ β ⊕ γ))
      ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) (x, b, c) : Finset (α ⊕ β ⊕ γ))
this : a = x → b = b → ¬c = c
⊢ False

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

Premises used: SimpleGraph.TripartiteFromTriangles.ExplicitDisjoint.inj₀, 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 : ExplicitDisjoint t
a : α
b : β
c : γ
habc : (a, b, c) ∈ t
x : α
hxyz : (x, b, c) ∈ t
h' :
  ¬Eq (α := Finset (α ⊕ β ⊕ γ)) ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) (a, b, c) : Finset (α ⊕ β ⊕ γ))
      ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) (x, b, c) : Finset (α ⊕ β ⊕ γ))
this : a = x → b = b → ¬c = c
⊢ False

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

Premises used: SimpleGraph.TripartiteFromTriangles.ExplicitDisjoint.inj₀, 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
h :
  ∀ (x : Finset (α ⊕ β ⊕ γ)),
    x ∈ (graph t).cliqueSet 3 ↔
      Membership.mem (γ := Set (Finset (α ⊕ β ⊕ γ)))
        ((⇑toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) '' (↑t : Set (α × β × γ))) x
⊢ (graph t).cliqueSet 3 = (⇑toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) '' (↑t : Set (α × β × γ))

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 γ
inst_3 : NoAccidental t
x : Finset (α ⊕ β ⊕ γ)
⊢ x ∈ (graph t).cliqueSet 3 ↔
    Membership.mem (γ := Set (Finset (α ⊕ β ⊕ γ)))
      ((⇑toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) '' (↑t : Set (α × β × γ))) x

Tactic:
is3Clique_iff

Premises used: Set.Mem, setOf, SimpleGraph.TripartiteFromTriangles.is3Clique_iff, Set.image, SimpleGraph.cliqueSet
-- 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 : Finset (α ⊕ β ⊕ γ)
⊢ x ∈ (graph t).cliqueSet 3 ↔
    Membership.mem (γ := Set (Finset (α ⊕ β ⊕ γ)))
      ((⇑toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) '' (↑t : Set (α × β × γ))) x

Tactic:
exact is3Clique_iff

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 : Fintype α
inst_4 : Fintype β
inst_5 : Fintype γ
inst_6 : NoAccidental t
push_cast : (graph t).cliqueSet 3 = (⇑toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) '' (↑t : Set (α × β × γ))
⊢ (↑((graph t).cliqueFinset 3) : Set (Finset (α ⊕ β ⊕ γ))) =
    (↑(image (⇑toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) t) : Set (Finset (α ⊕ β ⊕ γ)))

Tactic:
push_cast
-- 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 : Fintype α
inst_4 : Fintype β
inst_5 : Fintype γ
inst_6 : NoAccidental t
⊢ (graph t).cliqueSet 3 = (⇑toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) '' (↑t : Set (α × β × γ))

Tactic:
cliqueSet_eq_image _

Premises used: SimpleGraph.TripartiteFromTriangles.cliqueSet_eq_image
-- 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 : Fintype α
inst_4 : Fintype β
inst_5 : Fintype γ
inst_6 : NoAccidental t
⊢ (graph t).cliqueSet 3 = (⇑toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) '' (↑t : Set (α × β × γ))

Tactic:
exact cliqueSet_eq_image _

Premises used: SimpleGraph.TripartiteFromTriangles.cliqueSet_eq_image
-- 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 : Fintype α
inst_4 : Fintype β
inst_5 : Fintype γ
inst_6 : NoAccidental t
⊢ (graph t).cliqueFinset 3 = map toTriangle t

Tactic:
simp [cliqueFinset_eq_image, map_eq_image]

Premises used: SimpleGraph.TripartiteFromTriangles.cliqueFinset_eq_image, Finset.map_eq_image
-- 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 : Fintype α
inst_4 : Fintype β
inst_5 : Fintype γ
inst_6 : NoAccidental t
rw : #(map toTriangle t) = #t
rw₁ rw₂ : #t = #t
⊢ #((graph t).cliqueFinset 3) = #t

Tactic:
rw [cliqueFinset_eq_map, card_map]

Premises used: SimpleGraph.TripartiteFromTriangles.cliqueFinset_eq_map, Finset.card_map
-- 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 (α × β × γ)
inst_3 : DecidableEq α
inst_4 : DecidableEq β
inst_5 : DecidableEq γ
inst_6 : Fintype α
inst_7 : Fintype β
inst_8 : Fintype γ
inst_9 : ExplicitDisjoint t
ε : 𝕜
ht : ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α + Fintype.card β + Fintype.card γ) 2) : 𝕜) ≤ (↑(#t) : 𝕜)
x : α × β × γ
hx : x ∈ t
⊢ x ∈ ((graph t).cliqueFinset 3).preimage (⇑toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) ⋯

Tactic:
simpa using toTriangle_is3Clique hx

Premises used: SimpleGraph.TripartiteFromTriangles.toTriangle_is3Clique
-- 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 (α × β × γ)
inst_3 : DecidableEq α
inst_4 : DecidableEq β
inst_5 : DecidableEq γ
inst_6 : Fintype α
inst_7 : Fintype β
inst_8 : Fintype γ
inst_9 : ExplicitDisjoint t
ε : 𝕜
ht : ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α + Fintype.card β + Fintype.card γ) 2) : 𝕜) ≤ (↑(#t) : 𝕜)
⊢ ε * (↑(HPow.hPow (β := ℕ) (Fintype.card (α ⊕ β ⊕ γ)) 2) : 𝕜) ≤ (↑(#(map toTriangle t)) : 𝕜)

Tactic:
simpa [add_assoc] using ht

Premises used: add_assoc
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : ExplicitDisjoint t
inst_1 : NoAccidental t
⊢ (graph t).LocallyLinear

Tactic:
⟨?_, fun x y hxy ↦ ?_⟩

Premises used: SimpleGraph.LocallyLinear, And.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : ExplicitDisjoint t
inst_1 : NoAccidental t
refine_1 : (graph t).EdgeDisjointTriangles
refine_2 :
  ∀ (x y : α ⊕ β ⊕ γ) (hxy : (graph t).Adj x y), ∃ (s : Finset (α ⊕ β ⊕ γ)), (graph t).IsNClique 3 s ∧ x ∈ s ∧ y ∈ s
⊢ (graph t).LocallyLinear

Tactic:
refine ⟨?_, fun x y hxy ↦ ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : ExplicitDisjoint t
inst_1 : NoAccidental t
⊢ (↑(map toTriangle t) : Set (Finset (α ⊕ β ⊕ γ))).Pairwise fun (x y : Finset (α ⊕ β ⊕ γ)) ↦
    ((↑x : Set (α ⊕ β ⊕ γ)) ∩ (↑y : Set (α ⊕ β ⊕ γ))).Subsingleton

Tactic:
map_toTriangle_disjoint t

Premises used: SimpleGraph.TripartiteFromTriangles.map_toTriangle_disjoint
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : ExplicitDisjoint t
inst_1 : NoAccidental t
h : (graph t).cliqueSet 3 = (↑(map toTriangle t) : Set (Finset (α ⊕ β ⊕ γ)))
⊢ ((graph t).cliqueSet 3).Pairwise fun (x y : Finset (α ⊕ β ⊕ γ)) ↦
    ((↑x : Set (α ⊕ β ⊕ γ)) ∩ (↑y : Set (α ⊕ β ⊕ γ))).Subsingleton

Tactic:
convert! map_toTriangle_disjoint t

Premises used: SimpleGraph.TripartiteFromTriangles.map_toTriangle_disjoint
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : ExplicitDisjoint t
inst_1 : NoAccidental t
h :
  (⇑toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) '' (↑t : Set (α × β × γ)) =
    (↑(map toTriangle t) : Set (Finset (α ⊕ β ⊕ γ)))
h₁ h₂ :
  Eq (α := Set (Finset (α ⊕ β ⊕ γ))) ((⇑toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) '' (↑t : Set (α × β × γ)))
    ((⇑toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) '' (↑t : Set (α × β × γ)))
⊢ (graph t).cliqueSet 3 = (↑(map toTriangle t) : Set (Finset (α ⊕ β ⊕ γ)))

Tactic:
rw [cliqueSet_eq_image, coe_map]

Premises used: SimpleGraph.TripartiteFromTriangles.cliqueSet_eq_image, Finset.coe_map
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : ExplicitDisjoint t
inst_1 : NoAccidental t
x y : α ⊕ β ⊕ γ
hxy : (graph t).Adj x y
refine_2 :
  ∀ (z : α × β × γ) (hz : z ∈ t)
    (hxy :
      Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
          ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) x ∧
        Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
          ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) y),
    ∃ (s : Finset (α ⊕ β ⊕ γ)), (graph t).IsNClique 3 s ∧ x ∈ s ∧ y ∈ s
⊢ ∃ (s : Finset (α ⊕ β ⊕ γ)), (graph t).IsNClique 3 s ∧ x ∈ s ∧ y ∈ s

Tactic:
obtain ⟨z, hz, hxy⟩ := exists_mem_toTriangle hxy

Premises used: SimpleGraph.TripartiteFromTriangles.exists_mem_toTriangle
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : ExplicitDisjoint t
inst_1 : NoAccidental t
x y : α ⊕ β ⊕ γ
hxy_1 : (graph t).Adj x y
z : α × β × γ
hz : z ∈ t
hxy :
  Membership.mem (γ := Finset (α ⊕ β ⊕ γ)) ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ))
      x ∧
    Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
      ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) y
⊢ ∃ (s : Finset (α ⊕ β ⊕ γ)), (graph t).IsNClique 3 s ∧ x ∈ s ∧ y ∈ s

Tactic:
⟨_, toTriangle_is3Clique hz, hxy⟩

Premises used: SimpleGraph.TripartiteFromTriangles.toTriangle_is3Clique, And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : ExplicitDisjoint t
inst_1 : NoAccidental t
x y : α ⊕ β ⊕ γ
hxy_1 : (graph t).Adj x y
z : α × β × γ
hz : z ∈ t
hxy :
  Membership.mem (γ := Finset (α ⊕ β ⊕ γ)) ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ))
      x ∧
    Membership.mem (γ := Finset (α ⊕ β ⊕ γ))
      ((toTriangle : (a : α × β × γ) → Finset (α ⊕ β ⊕ γ)) z : Finset (α ⊕ β ⊕ γ)) y
⊢ ∃ (s : Finset (α ⊕ β ⊕ γ)), (graph t).IsNClique 3 s ∧ x ∈ s ∧ y ∈ s

Tactic:
exact ⟨_, toTriangle_is3Clique hz, hxy⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst : ExplicitDisjoint t
inst_1 : NoAccidental t
refine_1 : (graph t).EdgeDisjointTriangles
refine_2 refine_2₁ :
  ∀ (x y : α ⊕ β ⊕ γ) (hxy : (graph t).Adj x y), ∃ (s : Finset (α ⊕ β ⊕ γ)), (graph t).IsNClique 3 s ∧ x ∈ s ∧ y ∈ s
⊢ (graph t).LocallyLinear

Tactic:
classical
  refine ⟨?_, fun x y hxy ↦ ?_⟩
  · unfold EdgeDisjointTriangles
    convert! map_toTriangle_disjoint t
    rw [cliqueSet_eq_image, coe_map]
  · obtain ⟨z, hz, hxy⟩ := exists_mem_toTriangle hxy
    exact ⟨_, toTriangle_is3Clique hz, hxy⟩

Premises used: SimpleGraph.EdgeDisjointTriangles, SimpleGraph.TripartiteFromTriangles.cliqueSet_eq_image, Finset.coe_map