awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
hG : G.FarFromTriangleFree ε
h : Nonempty α
hε : 0 < ε
l : ℕ := ⌈4 / ε⌉₊
hl : 4 / ε ≤ (↑l : ℝ)
hl' : Fintype.card α ≤ l
⊢ LE.le (α := ℝ) 1 (↑(#(G.cliqueFinset 3)) : ℝ)

Tactic:
simpa [one_le_iff_ne_zero] using (hG.cliqueFinset_nonempty hε).card_pos.ne'

Premises used: Finset.Nonempty.card_pos, SimpleGraph.FarFromTriangleFree.cliqueFinset_nonempty, LT.lt.ne', Nat.one_le_iff_ne_zero
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
hG : G.FarFromTriangleFree ε
h : Nonempty α
hε : 0 < ε
l : ℕ := ⌈4 / ε⌉₊
hl : 4 / ε ≤ (↑l : ℝ)
hl' : Fintype.card α ≤ l
_ :
  triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤
    triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑l : ℝ) 3
_₁ : LE.le (α := ℝ) 1 (↑(#(G.cliqueFinset 3)) : ℝ)
⊢ triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)

Tactic:
calc
      _ ≤ triangleRemovalBound ε * ↑l ^ 3 := by
        gcongr; exact (triangleRemovalBound_pos hε).le
      _ ≤ (1 : ℝ) := (triangleRemovalBound_mul_cube_lt hε).le
      _ ≤ _ := by simpa [one_le_iff_ne_zero] using (hG.cliqueFinset_nonempty hε).card_pos.ne'

Premises used: SimpleGraph.triangleRemovalBound_mul_cube_lt, LT.lt.le, SimpleGraph.triangleRemovalBound, OfNat.ofNat
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
hG : G.FarFromTriangleFree ε
h : Nonempty α
hε : 0 < ε
l : ℕ := ⌈4 / ε⌉₊
hl : 4 / ε ≤ (↑l : ℝ)
hl' : l ≤ Fintype.card α
⊢ 0 < ε / 8

Tactic:
positivity
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
hG : G.FarFromTriangleFree ε
h : Nonempty α
hε : 0 < ε
l : ℕ := ⌈4 / ε⌉₊
hl : 4 / ε ≤ (↑l : ℝ)
hl' : l ≤ Fintype.card α
inr :
  ∀ (P : Finpartition (α := Finset α) univ) (hP₁ : P.IsEquipartition) (hP₂ : l ≤ #P.parts)
    (hP₃ : #P.parts ≤ bound (ε / 8) l) (hP₄ : P.IsUniform G (ε / 8)),
    triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)
⊢ triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)

Tactic:
obtain ⟨P, hP₁, hP₂, hP₃, hP₄⟩ := szemeredi_regularity G (by positivity : 0 < ε / 8) hl'

Premises used: szemeredi_regularity
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
hG : G.FarFromTriangleFree ε
h : Nonempty α
hε : 0 < ε
l : ℕ := ⌈4 / ε⌉₊
hl : 4 / ε ≤ (↑l : ℝ)
hl' : l ≤ Fintype.card α
P : Finpartition (α := Finset α) univ
hP₁ : P.IsEquipartition
hP₂ : l ≤ #P.parts
hP₃ : #P.parts ≤ bound (ε / 8) l
hP₄ : P.IsUniform G (ε / 8)
⊢ 4 / ε ≤ (↑(#P.parts) : ℝ)

Tactic:
have : 4 / ε ≤ #P.parts := hl.trans (cast_le.2 hP₂)
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
hG : G.FarFromTriangleFree ε
h : Nonempty α
hε : 0 < ε
l : ℕ := ⌈4 / ε⌉₊
hl : 4 / ε ≤ (↑l : ℝ)
hl' : l ≤ Fintype.card α
P : Finpartition (α := Finset α) univ
hP₁ : P.IsEquipartition
hP₂ : l ≤ #P.parts
hP₃ : #P.parts ≤ bound (ε / 8) l
hP₄ : P.IsUniform G (ε / 8)
this : 4 / ε ≤ (↑(#P.parts) : ℝ)
⊢ 2 * HSub.hSub (α := ℝ) (↑(#G.edgeFinset) : ℝ) (↑(#(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset) : ℝ) <
    2 * ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : ℝ)

Tactic:
have k := regularityReduced_edges_card_aux hε hP₁ hP₄ this
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
hG : G.FarFromTriangleFree ε
h : Nonempty α
hε : 0 < ε
l : ℕ := ⌈4 / ε⌉₊
hl : 4 / ε ≤ (↑l : ℝ)
hl' : l ≤ Fintype.card α
P : Finpartition (α := Finset α) univ
hP₁ : P.IsEquipartition
hP₂ : l ≤ #P.parts
hP₃ : #P.parts ≤ bound (ε / 8) l
hP₄ : P.IsUniform G (ε / 8)
this : 4 / ε ≤ (↑(#P.parts) : ℝ)
k :
  2 * HSub.hSub (α := ℝ) (↑(#G.edgeFinset) : ℝ) (↑(#(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset) : ℝ) <
    2 * ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : ℝ)
⊢ 2 * HSub.hSub (α := ℝ) (↑(#G.edgeFinset) : ℝ) (↑(#(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset) : ℝ) <
    2 * (ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : ℝ))

Tactic:
rw [mul_assoc] at k

Premises used: mul_assoc
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
hG : G.FarFromTriangleFree ε
h : Nonempty α
hε : 0 < ε
l : ℕ := ⌈4 / ε⌉₊
hl : 4 / ε ≤ (↑l : ℝ)
hl' : l ≤ Fintype.card α
P : Finpartition (α := Finset α) univ
hP₁ : P.IsEquipartition
hP₂ : l ≤ #P.parts
hP₃ : #P.parts ≤ bound (ε / 8) l
hP₄ : P.IsUniform G (ε / 8)
this : 4 / ε ≤ (↑(#P.parts) : ℝ)
k :
  2 * HSub.hSub (α := ℝ) (↑(#G.edgeFinset) : ℝ) (↑(#(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset) : ℝ) <
    2 * (ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : ℝ))
⊢ HSub.hSub (α := ℝ) (↑(#G.edgeFinset) : ℝ) (↑(#(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset) : ℝ) <
    ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : ℝ)

Tactic:
replace k := lt_of_mul_lt_mul_left k zero_le_two
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
hG : G.FarFromTriangleFree ε
h : Nonempty α
hε : 0 < ε
l : ℕ := ⌈4 / ε⌉₊
hl : 4 / ε ≤ (↑l : ℝ)
hl' : l ≤ Fintype.card α
P : Finpartition (α := Finset α) univ
hP₁ : P.IsEquipartition
hP₂ : l ≤ #P.parts
hP₃ : #P.parts ≤ bound (ε / 8) l
hP₄ : P.IsUniform G (ε / 8)
this : 4 / ε ≤ (↑(#P.parts) : ℝ)
k :
  HSub.hSub (α := ℝ) (↑(#G.edgeFinset) : ℝ) (↑(#(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset) : ℝ) <
    ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : ℝ)
inr :
  ∀ (t : Finset α) (ht : t ∈ (regularityReduced P G (ε / 8) (ε / 4)).cliqueFinset 3),
    triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)
⊢ triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)

Tactic:
obtain ⟨t, ht⟩ := hG.cliqueFinset_nonempty' regularityReduced_le k

Premises used: SimpleGraph.FarFromTriangleFree.cliqueFinset_nonempty', SimpleGraph.regularityReduced_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
hG : G.FarFromTriangleFree ε
h : Nonempty α
hε : 0 < ε
l : ℕ := ⌈4 / ε⌉₊
hl : 4 / ε ≤ (↑l : ℝ)
hl' : l ≤ Fintype.card α
P : Finpartition (α := Finset α) univ
hP₁ : P.IsEquipartition
hP₂ : l ≤ #P.parts
hP₃ : #P.parts ≤ bound (ε / 8) l
hP₄ : P.IsUniform G (ε / 8)
this : 4 / ε ≤ (↑(#P.parts) : ℝ)
k :
  HSub.hSub (α := ℝ) (↑(#G.edgeFinset) : ℝ) (↑(#(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset) : ℝ) <
    ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : ℝ)
t : Finset α
ht : t ∈ (regularityReduced P G (ε / 8) (ε / 4)).cliqueFinset 3
⊢ triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)

Tactic:
triangle_removal_aux hε hG.lt_one.le hP₁ hP₃ ht

Premises used: LT.lt.le, _private.0.SimpleGraph.triangle_removal_aux, SimpleGraph.FarFromTriangleFree.lt_one
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
hG : G.FarFromTriangleFree ε
h : Nonempty α
hε : 0 < ε
l : ℕ := ⌈4 / ε⌉₊
hl : 4 / ε ≤ (↑l : ℝ)
hl' : l ≤ Fintype.card α
P : Finpartition (α := Finset α) univ
hP₁ : P.IsEquipartition
hP₂ : l ≤ #P.parts
hP₃ : #P.parts ≤ bound (ε / 8) l
hP₄ : P.IsUniform G (ε / 8)
this : 4 / ε ≤ (↑(#P.parts) : ℝ)
k :
  HSub.hSub (α := ℝ) (↑(#G.edgeFinset) : ℝ) (↑(#(regularityReduced P G (ε / 8) (ε / 4)).edgeFinset) : ℝ) <
    ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : ℝ)
t : Finset α
ht : t ∈ (regularityReduced P G (ε / 8) (ε / 4)).cliqueFinset 3
⊢ triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3 ≤ (↑(#(G.cliqueFinset 3)) : ℝ)

Tactic:
exact triangle_removal_aux hε hG.lt_one.le hP₁ hP₃ ht

Premises used: LT.lt.le, _private.0.SimpleGraph.triangle_removal_aux, SimpleGraph.FarFromTriangleFree.lt_one
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
hG : (↑(#(G.cliqueFinset 3)) : ℝ) < triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3
by_contra! :
  ∀
    (h :
      ∀ (G' : SimpleGraph α) (_ : G' ≤ G) (x : DecidableRel G'.Adj)
        (_ :
          HSub.hSub (α := ℝ) (↑(#G.edgeFinset) : ℝ) (↑(#G'.edgeFinset) : ℝ) <
            ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : ℝ)),
        ¬G'.CliqueFree 3),
    False
⊢ ∃ G' ≤ G,
    ∃ (x : DecidableRel G'.Adj),
      HSub.hSub (α := ℝ) (↑(#G.edgeFinset) : ℝ) (↑(#G'.edgeFinset) : ℝ) <
          ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : ℝ) ∧
        G'.CliqueFree 3

Tactic:
by_contra! h
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
hG : (↑(#(G.cliqueFinset 3)) : ℝ) < triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3
h :
  ∀ (G' : SimpleGraph α) (_ : G' ≤ G) (x : DecidableRel G'.Adj)
    (_ :
      HSub.hSub (α := ℝ) (↑(#G.edgeFinset) : ℝ) (↑(#G'.edgeFinset) : ℝ) <
        ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : ℝ)),
    ¬G'.CliqueFree 3
⊢ False

Tactic:
hG.not_ge (farFromTriangleFree_iff.2 ?_).le_card_cliqueFinset

Premises used: Iff.mpr, SimpleGraph.farFromTriangleFree_iff, SimpleGraph.FarFromTriangleFree.le_card_cliqueFinset, LT.lt.not_ge
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
hG : (↑(#(G.cliqueFinset 3)) : ℝ) < triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3
h :
  ∀ (G' : SimpleGraph α) (_ : G' ≤ G) (x : DecidableRel G'.Adj)
    (_ :
      HSub.hSub (α := ℝ) (↑(#G.edgeFinset) : ℝ) (↑(#G'.edgeFinset) : ℝ) <
        ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : ℝ)),
    ¬G'.CliqueFree 3
refine :
  ∀ ⦃H : SimpleGraph α⦄ [inst : DecidableRel H.Adj],
    H ≤ G →
      H.CliqueFree 3 →
        ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : ℝ) ≤
          HSub.hSub (α := ℝ) (↑(#G.edgeFinset) : ℝ) (↑(#H.edgeFinset) : ℝ)
⊢ False

Tactic:
refine hG.not_ge (farFromTriangleFree_iff.2 ?_).le_card_cliqueFinset

Premises used: Iff.mpr, SimpleGraph.farFromTriangleFree_iff, SimpleGraph.FarFromTriangleFree.le_card_cliqueFinset, LT.lt.not_ge
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
hG : (↑(#(G.cliqueFinset 3)) : ℝ) < triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3
h :
  ∀ (G' : SimpleGraph α) (_ : G' ≤ G) (x : DecidableRel G'.Adj)
    (_ :
      HSub.hSub (α := ℝ) (↑(#G.edgeFinset) : ℝ) (↑(#G'.edgeFinset) : ℝ) <
        ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : ℝ)),
    ¬G'.CliqueFree 3
G' : SimpleGraph α
_ :
  ∀ [inst : DecidableRel G'.Adj],
    G' ≤ G →
      G'.CliqueFree 3 →
        ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : ℝ) ≤
          HSub.hSub (α := ℝ) (↑(#G.edgeFinset) : ℝ) (↑(#G'.edgeFinset) : ℝ)
⊢ ∀ [inst : DecidableRel G'.Adj],
    G' ≤ G →
      G'.CliqueFree 3 →
        ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : ℝ) ≤
          HSub.hSub (α := ℝ) (↑(#G.edgeFinset) : ℝ) (↑(#G'.edgeFinset) : ℝ)

Tactic:
_
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
hG_1 : (↑(#(G.cliqueFinset 3)) : ℝ) < triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3
h :
  ∀ (G' : SimpleGraph α) (_ : G' ≤ G) (x : DecidableRel G'.Adj)
    (_ :
      HSub.hSub (α := ℝ) (↑(#G.edgeFinset) : ℝ) (↑(#G'.edgeFinset) : ℝ) <
        ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : ℝ)),
    ¬G'.CliqueFree 3
G' : SimpleGraph α
inst_3 : DecidableRel G'.Adj
hG : G' ≤ G
hG' : G'.CliqueFree 3
⊢ ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : ℝ) ≤ HSub.hSub (α := ℝ) (↑(#G.edgeFinset) : ℝ) (↑(#G'.edgeFinset) : ℝ)

Tactic:
le_of_not_gt fun i ↦ h G' hG _ i hG'

Premises used: le_of_not_gt
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
ε : ℝ
hG_1 : (↑(#(G.cliqueFinset 3)) : ℝ) < triangleRemovalBound ε * HPow.hPow (α := ℝ) (β := ℕ) (↑(Fintype.card α) : ℝ) 3
h :
  ∀ (G' : SimpleGraph α) (_ : G' ≤ G) (x : DecidableRel G'.Adj)
    (_ :
      HSub.hSub (α := ℝ) (↑(#G.edgeFinset) : ℝ) (↑(#G'.edgeFinset) : ℝ) <
        ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : ℝ)),
    ¬G'.CliqueFree 3
G' : SimpleGraph α
inst_3 : DecidableRel G'.Adj
hG : G' ≤ G
hG' : G'.CliqueFree 3
⊢ ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : ℝ) ≤ HSub.hSub (α := ℝ) (↑(#G.edgeFinset) : ℝ) (↑(#G'.edgeFinset) : ℝ)

Tactic:
exact le_of_not_gt fun i ↦ h G' hG _ i hG'

Premises used: le_of_not_gt
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
G : SimpleGraph α
inst_2 : DecidableRel G.Adj
s t : Finset α
P : Finpartition (α := Finset α) univ
ε_1 ε : ℝ
hε : 0 < ε
⊢ 0 < triangleRemovalBound ε

Tactic:
positivity
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
⊢ ∀ (x : α ⊕ β ⊕ γ), ¬Rel t x x

Tactic:
fun _x hx ↦ nomatch hx

Premises used: False, _private.0.SimpleGraph.TripartiteFromTriangles.rel_irrefl.match_1, Not
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
x y : α ⊕ β ⊕ γ
h : Rel t x y
in₀₁ : ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄, (a, b, c) ∈ t → Rel t (in₁ b) (in₀ a)
in₁₀ : ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄, (a, b, c) ∈ t → Rel t (in₀ a) (in₁ b)
in₀₂ : ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄, (a, b, c) ∈ t → Rel t (in₂ c) (in₀ a)
in₂₀ : ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄, (a, b, c) ∈ t → Rel t (in₀ a) (in₂ c)
in₁₂ : ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄, (a, b, c) ∈ t → Rel t (in₂ c) (in₁ b)
in₂₁ : ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄, (a, b, c) ∈ t → Rel t (in₁ b) (in₂ c)
⊢ Rel t y x

Tactic:
cases h
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h in₀₁ : (a, b, c) ∈ t
in₂ : γ
⊢ Rel t (in₁ b) (in₀ a)

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h in₁₀ : (a, b, c) ∈ t
in₁₁ : γ
⊢ Rel t (in₀ a) (in₁ b)

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h in₀₂ : (a, b, c) ∈ t
in₃ : β
⊢ Rel t (in₂ c) (in₀ a)

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h in₂₀ : (a, b, c) ∈ t
in₂₁ : β
⊢ Rel t (in₀ a) (in₂ c)

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h in₁₂ : (a, b, c) ∈ t
in₁₃ : α
⊢ Rel t (in₂ c) (in₁ b)

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h in₂₁ : (a, b, c) ∈ t
in₂₂ : α
⊢ Rel t (in₁ b) (in₂ c)

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (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 (α × β × γ)
a a' : α
⊢ ¬(graph t).Adj (in₀ a) (in₀ a')

Tactic:
fun h ↦ nomatch h

Premises used: False, _private.0.SimpleGraph.TripartiteFromTriangles.Graph.not_in₀₀.match_1, Not
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
b b' : β
⊢ ¬(graph t).Adj (in₁ b) (in₁ b')

Tactic:
fun h ↦ nomatch h

Premises used: False, Not, _private.0.SimpleGraph.TripartiteFromTriangles.Graph.not_in₁₁.match_1
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
c c' : γ
⊢ ¬(graph t).Adj (in₂ c) (in₂ c')

Tactic:
fun h ↦ nomatch h

Premises used: False, _private.0.SimpleGraph.TripartiteFromTriangles.Graph.not_in₂₂.match_1, Not
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ ∃ (c : γ), (a, b, c) ∈ t

Tactic:
⟨_, ‹_›⟩

Premises used: Exists.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ ∃ (c : γ), (a, b, c) ∈ t

Tactic:
exact ⟨_, ‹_›⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
c : γ
b : β
h : (a, b, c) ∈ t
⊢ ∃ (b : β), (a, b, c) ∈ t

Tactic:
⟨_, ‹_›⟩

Premises used: Exists.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
c : γ
b : β
h : (a, b, c) ∈ t
⊢ ∃ (b : β), (a, b, c) ∈ t

Tactic:
exact ⟨_, ‹_›⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
b : β
c : γ
a : α
h : (a, b, c) ∈ t
⊢ ∃ (a : α), (a, b, c) ∈ t

Tactic:
⟨_, ‹_›⟩

Premises used: Exists.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
b : β
c : γ
a : α
h : (a, b, c) ∈ t
⊢ ∃ (a : α), (a, b, c) ∈ t

Tactic:
exact ⟨_, ‹_›⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ (a, b, c).1 = a ∧ (a, b, c).2.1 = b

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ ∃ x ∈ t, x.1 = a ∧ x.2.1 = b

Tactic:
exact ⟨_, ‹_›, by simp⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
a₁ : ((a, b, c).1, (a, b, c).2.1, c) ∈ t
c₁ : γ
⊢ (graph t).Adj (in₀ (a, b, c).1) (in₁ (a, b, c).2.1)

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ (a, b, c).2.1 = b ∧ (a, b, c).1 = a

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ ∃ x ∈ t, x.2.1 = b ∧ x.1 = a

Tactic:
exact ⟨_, ‹_›, by simp⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
a₁ : ((a, b, c).1, (a, b, c).2.1, c) ∈ t
c₁ : γ
⊢ (graph t).Adj (in₁ (a, b, c).2.1) (in₀ (a, b, c).1)

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
c : γ
b : β
h : (a, b, c) ∈ t
⊢ (a, b, c).1 = a ∧ (a, b, c).2.2 = c

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
c : γ
b : β
h : (a, b, c) ∈ t
⊢ ∃ x ∈ t, x.1 = a ∧ x.2.2 = c

Tactic:
exact ⟨_, ‹_›, by simp⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
a₁ : ((a, b, c).1, b, (a, b, c).2.2) ∈ t
b₁ : β
⊢ (graph t).Adj (in₀ (a, b, c).1) (in₂ (a, b, c).2.2)

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
c : γ
b : β
h : (a, b, c) ∈ t
⊢ (a, b, c).2.2 = c ∧ (a, b, c).1 = a

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
c : γ
b : β
h : (a, b, c) ∈ t
⊢ ∃ x ∈ t, x.2.2 = c ∧ x.1 = a

Tactic:
exact ⟨_, ‹_›, by simp⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
a₁ : ((a, b, c).1, b, (a, b, c).2.2) ∈ t
b₁ : β
⊢ (graph t).Adj (in₂ (a, b, c).2.2) (in₀ (a, b, c).1)

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
b : β
c : γ
a : α
h : (a, b, c) ∈ t
⊢ (a, b, c).2.1 = b ∧ (a, b, c).2.2 = c

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
b : β
c : γ
a : α
h : (a, b, c) ∈ t
⊢ ∃ x ∈ t, x.2.1 = b ∧ x.2.2 = c

Tactic:
exact ⟨_, ‹_›, by simp⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
a₁ : (a, (a, b, c).2.1, (a, b, c).2.2) ∈ t
a₂ : α
⊢ (graph t).Adj (in₁ (a, b, c).2.1) (in₂ (a, b, c).2.2)

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
b : β
c : γ
a : α
h : (a, b, c) ∈ t
⊢ (a, b, c).2.2 = c ∧ (a, b, c).2.1 = b

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
b : β
c : γ
a : α
h : (a, b, c) ∈ t
⊢ ∃ x ∈ t, x.2.2 = c ∧ x.2.1 = b

Tactic:
exact ⟨_, ‹_›, by simp⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
a₁ : (a, (a, b, c).2.1, (a, b, c).2.2) ∈ t
a₂ : α
⊢ (graph t).Adj (in₂ (a, b, c).2.2) (in₁ (a, b, c).2.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_1 : (a, b, c) ∈ t
b_1 : β
c_1 : γ
h_2 : (a, b_1, c_1) ∈ t
a_1 : α
h_3 : (a_1, b, c_1) ∈ t
h :
  ∀ (a_2 : α ⊕ β ⊕ γ),
    Membership.mem (γ := Finset (α ⊕ β ⊕ γ)) {in₀ a, in₁ b, in₂ c_1} a_2 ↔
      Membership.mem (γ := Finset (α ⊕ β ⊕ γ)) {in₀ a, in₁ b, in₂ c_1} a_2
⊢ Eq (α := Finset (α ⊕ β ⊕ γ)) {in₀ a, in₁ b, in₂ c_1} {in₀ a, in₁ b, in₂ c_1}

Tactic:
ext