awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableEq α
inst_1 : Fintype α
inst_2 : DecidableRel G.Adj
hG : G.LocallyLinear
a b c : α
hab : G.Adj a b
hac : G.Adj a c
hbc : G.Adj b c
refine_2 :
  ∀ (x y : α),
    G.Adj x y →
      x = a ∨ x = b ∨ x = c → y = a ∨ y = b ∨ y = c → s(x, y) = s(a, b) ∨ s(x, y) = s(a, c) ∨ s(x, y) = s(b, c)
⊢ bipartiteBelow (fun (e : Sym2 α) (s : Finset α) ↦ e ∈ s.sym2) G.edgeFinset {a, b, c} ⊆ {s(a, b), s(a, c), s(b, c)}

Tactic:
simp only [subset_iff, Sym2.forall, mem_sym2_iff, mem_bipartiteBelow, mem_insert,
    mem_edgeFinset, mem_singleton, and_imp, mem_edgeSet, Sym2.mem_iff, forall_eq_or_imp,
    forall_eq]

Premises used: Finset.mem_singleton, and_imp, forall_eq, Finset.mem_sym2_iff, Finset.mem_insert, forall_eq_or_imp, Sym2.forall, Sym2.mem_iff, Finset.mem_bipartiteBelow, Finset.subset_iff, SimpleGraph.mem_edgeFinset, SimpleGraph.mem_edgeSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableEq α
inst_1 : Fintype α
inst_2 : DecidableRel G.Adj
hG : G.LocallyLinear
b c : α
hbc : G.Adj b c
e : α
hde : G.Adj e e
hab : G.Adj e b
hac : G.Adj e c
⊢ s(e, e) = s(e, b) ∨ s(e, e) = s(e, c) ∨ s(e, e) = s(b, c)

Tactic:
simp [*] at *
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableEq α
inst_1 : Fintype α
inst_2 : DecidableRel G.Adj
hG : G.LocallyLinear
c d e : α
hde : G.Adj d e
hac : G.Adj d c
hbc : G.Adj e c
hab : G.Adj d e
⊢ s(d, e) = s(d, e) ∨ s(d, e) = s(d, c) ∨ s(d, e) = s(e, c)

Tactic:
simp [*] at *
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableEq α
inst_1 : Fintype α
inst_2 : DecidableRel G.Adj
hG : G.LocallyLinear
b d e : α
hde : G.Adj d e
hab : G.Adj d b
hbc : G.Adj b e
hac : G.Adj d e
⊢ s(d, e) = s(d, b) ∨ s(d, e) = s(d, e) ∨ s(d, e) = s(b, e)

Tactic:
simp [*] at *
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableEq α
inst_1 : Fintype α
inst_2 : DecidableRel G.Adj
hG : G.LocallyLinear
c d e : α
hde : G.Adj d e
hbc : G.Adj d c
hac : G.Adj e c
hab : G.Adj e d
⊢ s(d, e) = s(e, d) ∨ s(d, e) = s(e, c) ∨ s(d, e) = s(d, c)

Tactic:
simp [*] at *
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableEq α
inst_1 : Fintype α
inst_2 : DecidableRel G.Adj
hG : G.LocallyLinear
a c : α
hac : G.Adj a c
e : α
hde : G.Adj e e
hab : G.Adj a e
hbc : G.Adj e c
⊢ s(e, e) = s(a, e) ∨ s(e, e) = s(a, c) ∨ s(e, e) = s(e, c)

Tactic:
simp [*] at *
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableEq α
inst_1 : Fintype α
inst_2 : DecidableRel G.Adj
hG : G.LocallyLinear
a d e : α
hde : G.Adj d e
hab : G.Adj a d
hac : G.Adj a e
hbc : G.Adj d e
⊢ s(d, e) = s(a, d) ∨ s(d, e) = s(a, e) ∨ s(d, e) = s(d, e)

Tactic:
simp [*] at *
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableEq α
inst_1 : Fintype α
inst_2 : DecidableRel G.Adj
hG : G.LocallyLinear
b d e : α
hde : G.Adj d e
hbc : G.Adj b d
hab : G.Adj e b
hac : G.Adj e d
⊢ s(d, e) = s(e, b) ∨ s(d, e) = s(e, d) ∨ s(d, e) = s(b, d)

Tactic:
simp [*] at *
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableEq α
inst_1 : Fintype α
inst_2 : DecidableRel G.Adj
hG : G.LocallyLinear
a d e : α
hde : G.Adj d e
hac : G.Adj a d
hab : G.Adj a e
hbc : G.Adj e d
⊢ s(d, e) = s(a, e) ∨ s(d, e) = s(a, d) ∨ s(d, e) = s(e, d)

Tactic:
simp [*] at *
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
inst : DecidableEq α
inst_1 : Fintype α
inst_2 : DecidableRel G.Adj
hG : G.LocallyLinear
a b : α
hab : G.Adj a b
e : α
hde : G.Adj e e
hac : G.Adj a e
hbc : G.Adj b e
⊢ s(e, e) = s(a, b) ∨ s(e, e) = s(a, e) ∨ s(e, e) = s(b, e)

Tactic:
simp [*] at *
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
G : SimpleGraph α
ε : 𝕜
inst_2 : Fintype α
inst_3 : DecidableRel G.Adj
⊢ G.FarFromTriangleFree ε ↔
    ∀ ⦃H : SimpleGraph α⦄ [inst_4 : DecidableRel H.Adj],
      H ≤ G →
        H.CliqueFree 3 →
          ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : 𝕜) ≤
            HSub.hSub (α := 𝕜) (↑(#G.edgeFinset) : 𝕜) (↑(#H.edgeFinset) : 𝕜)

Tactic:
deleteFar_iff

Premises used: SimpleGraph.deleteFar_iff, SimpleGraph.FarFromTriangleFree
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
G : SimpleGraph α
ε δ : 𝕜
inst_3 : Fintype α
inst_4 : DecidableRel G.Adj
hε : G.FarFromTriangleFree ε
h : δ ≤ ε
ha : LE.le.{u_3} (α := 𝕜) 0 (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : 𝕜)
⊢ δ * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : 𝕜) ≤ ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : 𝕜)

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
G H : SimpleGraph α
ε : 𝕜
inst_2 : Fintype α
inst_3 : DecidableRel G.Adj
inst_4 : DecidableRel H.Adj
inst_5 : DecidableEq α
hH : H ≤ G
hG : G.FarFromTriangleFree ε
hcard :
  HSub.hSub (α := 𝕜) (↑(#G.edgeFinset) : 𝕜) (↑(#H.edgeFinset) : 𝕜) < ε * (↑(HPow.hPow (β := ℕ) (Fintype.card α) 2) : 𝕜)
⊢ (H.cliqueFinset 3).Nonempty

Tactic:
nonempty_of_ne_empty <|
    cliqueFinset_eq_empty_iff.not.2 fun hH' => (hG.le_card_sub_card hH hH').not_gt hcard

Premises used: Iff.mpr, SimpleGraph.cliqueFinset_eq_empty_iff, SimpleGraph.DeleteFar.le_card_sub_card, Iff.not, LE.le.not_gt, Finset.nonempty_of_ne_empty
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G H : SimpleGraph α
inst : Fintype α
inst_1 : DecidableRel G.Adj
inst_2 : DecidableRel H.Adj
inst_3 : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris : Set (Finset α)).Pairwise fun (x y : Finset α) ↦ ((↑x : Set α) ∩ (↑y : Set α)).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
rw : #tris.attach ≤ #(G.edgeFinset \ H.edgeFinset)
⊢ #tris ≤ #G.edgeFinset - #H.edgeFinset

Tactic:
rw [← card_sdiff_of_subset (edgeFinset_mono hHG), ← card_attach]

Premises used: SimpleGraph.edgeFinset_mono, Finset.card_sdiff_of_subset, Finset.card_attach
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G H : SimpleGraph α
inst : Fintype α
inst_1 : DecidableRel G.Adj
inst_2 : DecidableRel H.Adj
inst_3 : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris : Set (Finset α)).Pairwise fun (x y : Finset α) ↦ ((↑x : Set α) ∩ (↑y : Set α)).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
by_contra! : ∀ (hG : #(G.edgeFinset \ H.edgeFinset) < #tris.attach), False
⊢ #tris.attach ≤ #(G.edgeFinset \ H.edgeFinset)

Tactic:
by_contra! hG
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G H : SimpleGraph α
inst : Fintype α
inst_1 : DecidableRel G.Adj
inst_2 : DecidableRel H.Adj
inst_3 : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris : Set (Finset α)).Pairwise fun (x y : Finset α) ↦ ((↑x : Set α) ∩ (↑y : Set α)).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
hG : #(G.edgeFinset \ H.edgeFinset) < #tris.attach
t : Finset α
ht : t ∈ tris
by_contra! : ∀ (h : ∀ (x y : α) (_ : x ∈ t) (_ : y ∈ t) (_ : x ≠ y), s(x, y) ∉ G.edgeFinset \ H.edgeFinset), False
⊢ ∃ (x : α) (y : α), x ∈ t ∧ y ∈ t ∧ x ≠ y ∧ s(x, y) ∈ G.edgeFinset \ H.edgeFinset

Tactic:
by_contra! h
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G H : SimpleGraph α
inst : Fintype α
inst_1 : DecidableRel G.Adj
inst_2 : DecidableRel H.Adj
inst_3 : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris : Set (Finset α)).Pairwise fun (x y : Finset α) ↦ ((↑x : Set α) ∩ (↑y : Set α)).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
hG : #(G.edgeFinset \ H.edgeFinset) < #tris.attach
t : Finset α
ht : t ∈ tris
h : ∀ (x y : α) (_ : x ∈ t) (_ : y ∈ t) (_ : x ≠ y), s(x, y) ∉ G.edgeFinset \ H.edgeFinset
⊢ False

Tactic:
hH t ?_
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G H : SimpleGraph α
inst : Fintype α
inst_1 : DecidableRel G.Adj
inst_2 : DecidableRel H.Adj
inst_3 : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris : Set (Finset α)).Pairwise fun (x y : Finset α) ↦ ((↑x : Set α) ∩ (↑y : Set α)).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
hG : #(G.edgeFinset \ H.edgeFinset) < #tris.attach
t : Finset α
ht : t ∈ tris
h : ∀ (x y : α) (_ : x ∈ t) (_ : y ∈ t) (_ : x ≠ y), s(x, y) ∉ G.edgeFinset \ H.edgeFinset
refine : H.IsNClique 3 t
⊢ False

Tactic:
refine hH t ?_
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G H : SimpleGraph α
inst : Fintype α
inst_1 : DecidableRel G.Adj
inst_2 : DecidableRel H.Adj
inst_3 : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris : Set (Finset α)).Pairwise fun (x y : Finset α) ↦ ((↑x : Set α) ∩ (↑y : Set α)).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
hG : #(G.edgeFinset \ H.edgeFinset) < #tris.attach
t : Finset α
ht : t ∈ tris
h : ∀ (x y : α) (_ : x ∈ t) (_ : y ∈ t) (_ : x ≠ y), s(x, y) ∉ G.edgeFinset \ H.edgeFinset
⊢ ∀ (x y : α) (_ : x ∈ t) (_ : y ∈ t) (_ : x ≠ y), G.Adj x y → H.Adj x y

Tactic:
simp only [not_and, mem_sdiff, not_not, mem_edgeFinset, mem_edgeSet] at h

Premises used: Classical.not_not, Finset.mem_sdiff, SimpleGraph.mem_edgeFinset, not_and, SimpleGraph.mem_edgeSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G H : SimpleGraph α
inst : Fintype α
inst_1 : DecidableRel G.Adj
inst_2 : DecidableRel H.Adj
inst_3 : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris : Set (Finset α)).Pairwise fun (x y : Finset α) ↦ ((↑x : Set α) ∩ (↑y : Set α)).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
hG : #(G.edgeFinset \ H.edgeFinset) < #tris.attach
t : Finset α
ht : t ∈ tris
h : ∀ (x y : α) (_ : x ∈ t) (_ : y ∈ t) (_ : x ≠ y), G.Adj x y → H.Adj x y
obtain :
  ∀ (x y z : α) (xy : G.Adj x y) (xz : G.Adj x z) (yz : G.Adj y z) (ht : {x, y, z} ∈ tris)
    (h :
      ∀ (x_1 y_1 : α) (_ : Membership.mem (γ := Finset α) {x, y, z} x_1)
        (_ : Membership.mem (γ := Finset α) {x, y, z} y_1) (_ : x_1 ≠ y_1), G.Adj x_1 y_1 → H.Adj x_1 y_1),
    H.IsNClique 3 {x, y, z}
⊢ H.IsNClique 3 t

Tactic:
obtain ⟨x, y, z, xy, xz, yz, rfl⟩ := is3Clique_iff.1 (mem_cliqueFinset_iff.1 <| htris ht)

Premises used: SimpleGraph.is3Clique_iff, SimpleGraph.mem_cliqueFinset_iff, Iff.mp, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G H : SimpleGraph α
inst : Fintype α
inst_1 : DecidableRel G.Adj
inst_2 : DecidableRel H.Adj
inst_3 : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris : Set (Finset α)).Pairwise fun (x y : Finset α) ↦ ((↑x : Set α) ∩ (↑y : Set α)).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
hG : #(G.edgeFinset \ H.edgeFinset) < #tris.attach
x y z : α
xy : G.Adj x y
xz : G.Adj x z
yz : G.Adj y z
ht : {x, y, z} ∈ tris
h :
  ∀ (x_1 y_1 : α) (_ : Membership.mem (γ := Finset α) {x, y, z} x_1) (_ : Membership.mem (γ := Finset α) {x, y, z} y_1)
    (_ : x_1 ≠ y_1), G.Adj x_1 y_1 → H.Adj x_1 y_1
rw : H.Adj x y ∧ H.Adj x z ∧ H.Adj y z
⊢ H.IsNClique 3 {x, y, z}

Tactic:
rw [is3Clique_triple_iff]

Premises used: SimpleGraph.is3Clique_triple_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G H : SimpleGraph α
inst : Fintype α
inst_1 : DecidableRel G.Adj
inst_2 : DecidableRel H.Adj
inst_3 : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris : Set (Finset α)).Pairwise fun (x y : Finset α) ↦ ((↑x : Set α) ∩ (↑y : Set α)).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
hG : #(G.edgeFinset \ H.edgeFinset) < #tris.attach
x y z : α
xy : G.Adj x y
xz : G.Adj x z
yz : G.Adj y z
ht : {x, y, z} ∈ tris
h :
  ∀ (x_1 y_1 : α) (_ : Membership.mem (γ := Finset α) {x, y, z} x_1) (_ : Membership.mem (γ := Finset α) {x, y, z} y_1)
    (_ : x_1 ≠ y_1), G.Adj x_1 y_1 → H.Adj x_1 y_1
⊢ H.Adj x y ∧ H.Adj x z ∧ H.Adj y z

Tactic:
⟨h _ _ ?_ ?_ xy.ne xy, h _ _ ?_ ?_ xz.ne xz, h _ _ ?_ ?_ yz.ne yz⟩

Premises used: SimpleGraph.Adj.ne, And.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G H : SimpleGraph α
inst : Fintype α
inst_1 : DecidableRel G.Adj
inst_2 : DecidableRel H.Adj
inst_3 : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris : Set (Finset α)).Pairwise fun (x y : Finset α) ↦ ((↑x : Set α) ∩ (↑y : Set α)).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
hG : #(G.edgeFinset \ H.edgeFinset) < #tris.attach
x y z : α
xy : G.Adj x y
xz : G.Adj x z
yz : G.Adj y z
ht : {x, y, z} ∈ tris
h :
  ∀ (x_1 y_1 : α) (_ : Membership.mem (γ := Finset α) {x, y, z} x_1) (_ : Membership.mem (γ := Finset α) {x, y, z} y_1)
    (_ : x_1 ≠ y_1), G.Adj x_1 y_1 → H.Adj x_1 y_1
refine_1 : Membership.mem (γ := Finset α) {x, y, z} x
refine_2 : Membership.mem (γ := Finset α) {x, y, z} y
refine_3 : Membership.mem (γ := Finset α) {x, y, z} x
refine_4 : Membership.mem (γ := Finset α) {x, y, z} z
refine_5 : Membership.mem (γ := Finset α) {x, y, z} y
refine_6 : Membership.mem (γ := Finset α) {x, y, z} z
⊢ H.Adj x y ∧ H.Adj x z ∧ H.Adj y z

Tactic:
refine ⟨h _ _ ?_ ?_ xy.ne xy, h _ _ ?_ ?_ xz.ne xz, h _ _ ?_ ?_ yz.ne yz⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G H : SimpleGraph α
inst : Fintype α
inst_1 : DecidableRel G.Adj
inst_2 : DecidableRel H.Adj
inst_3 : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris : Set (Finset α)).Pairwise fun (x y : Finset α) ↦ ((↑x : Set α) ∩ (↑y : Set α)).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
hG : #(G.edgeFinset \ H.edgeFinset) < #tris.attach
x y z : α
xy : G.Adj x y
xz : G.Adj x z
yz : G.Adj y z
ht : {x, y, z} ∈ tris
h :
  ∀ (x_1 y_1 : α) (_ : Membership.mem (γ := Finset α) {x, y, z} x_1) (_ : Membership.mem (γ := Finset α) {x, y, z} y_1)
    (_ : x_1 ≠ y_1), G.Adj x_1 y_1 → H.Adj x_1 y_1
⊢ Membership.mem (γ := Finset α) {x, y, z} x

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G H : SimpleGraph α
inst : Fintype α
inst_1 : DecidableRel G.Adj
inst_2 : DecidableRel H.Adj
inst_3 : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris : Set (Finset α)).Pairwise fun (x y : Finset α) ↦ ((↑x : Set α) ∩ (↑y : Set α)).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
hG : #(G.edgeFinset \ H.edgeFinset) < #tris.attach
x y z : α
xy : G.Adj x y
xz : G.Adj x z
yz : G.Adj y z
ht : {x, y, z} ∈ tris
h :
  ∀ (x_1 y_1 : α) (_ : Membership.mem (γ := Finset α) {x, y, z} x_1) (_ : Membership.mem (γ := Finset α) {x, y, z} y_1)
    (_ : x_1 ≠ y_1), G.Adj x_1 y_1 → H.Adj x_1 y_1
⊢ Membership.mem (γ := Finset α) {x, y, z} y

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G H : SimpleGraph α
inst : Fintype α
inst_1 : DecidableRel G.Adj
inst_2 : DecidableRel H.Adj
inst_3 : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris : Set (Finset α)).Pairwise fun (x y : Finset α) ↦ ((↑x : Set α) ∩ (↑y : Set α)).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
hG : #(G.edgeFinset \ H.edgeFinset) < #tris.attach
x y z : α
xy : G.Adj x y
xz : G.Adj x z
yz : G.Adj y z
ht : {x, y, z} ∈ tris
h :
  ∀ (x_1 y_1 : α) (_ : Membership.mem (γ := Finset α) {x, y, z} x_1) (_ : Membership.mem (γ := Finset α) {x, y, z} y_1)
    (_ : x_1 ≠ y_1), G.Adj x_1 y_1 → H.Adj x_1 y_1
⊢ Membership.mem (γ := Finset α) {x, y, z} z

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G H : SimpleGraph α
inst : Fintype α
inst_1 : DecidableRel G.Adj
inst_2 : DecidableRel H.Adj
inst_3 : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris : Set (Finset α)).Pairwise fun (x y : Finset α) ↦ ((↑x : Set α) ∩ (↑y : Set α)).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
hG : #(G.edgeFinset \ H.edgeFinset) < #tris.attach
⊢ ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), ∃ (x : α) (y : α), x ∈ t ∧ y ∈ t ∧ x ≠ y ∧ s(x, y) ∈ G.edgeFinset \ H.edgeFinset

Tactic:
have ⦃t⦄ (ht : t ∈ tris) :
    ∃ x y, x ∈ t ∧ y ∈ t ∧ x ≠ y ∧ s(x, y) ∈ G.edgeFinset \ H.edgeFinset := by
    by_contra! h
    refine hH t ?_
    simp only [not_and, mem_sdiff, not_not, mem_edgeFinset, mem_edgeSet] at h
    obtain ⟨x, y, z, xy, xz, yz, rfl⟩ := is3Clique_iff.1 (mem_cliqueFinset_iff.1 <| htris ht)
    rw [is3Clique_triple_iff]
    refine ⟨h _ _ ?_ ?_ xy.ne xy, h _ _ ?_ ?_ xz.ne xz, h _ _ ?_ ?_ yz.ne yz⟩ <;> simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G H : SimpleGraph α
inst : Fintype α
inst_1 : DecidableRel G.Adj
inst_2 : DecidableRel H.Adj
inst_3 : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris : Set (Finset α)).Pairwise fun (x y : Finset α) ↦ ((↑x : Set α) ∩ (↑y : Set α)).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
hG : #(G.edgeFinset \ H.edgeFinset) < #tris.attach
this :
  ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), ∃ (x : α) (y : α), x ∈ t ∧ y ∈ t ∧ x ≠ y ∧ s(x, y) ∈ G.edgeFinset \ H.edgeFinset
choose :
  ∀ (fx fy : ⦃t : Finset α⦄ → (ht : t ∈ tris) → α) (hfx : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fx ht ∈ t)
    (hfy : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fy ht ∈ t) (hfne : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fx ht ≠ fy ht)
    (fmem : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), s(fx ht, fy ht) ∈ G.edgeFinset \ H.edgeFinset), False
⊢ False

Tactic:
choose fx fy hfx hfy hfne fmem using this
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G H : SimpleGraph α
inst : Fintype α
inst_1 : DecidableRel G.Adj
inst_2 : DecidableRel H.Adj
inst_3 : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris : Set (Finset α)).Pairwise fun (x y : Finset α) ↦ ((↑x : Set α) ∩ (↑y : Set α)).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
hG : #(G.edgeFinset \ H.edgeFinset) < #tris.attach
fx fy : ⦃t : Finset α⦄ → (ht : t ∈ tris) → α
hfx : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fx ht ∈ t
hfy : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fy ht ∈ t
hfne : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fx ht ≠ fy ht
fmem : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), s(fx ht, fy ht) ∈ G.edgeFinset \ H.edgeFinset
f : (t : ↥tris) → Sym2 α := fun (t : ↥tris) ↦ s(fx ⋯, fy ⋯)
⊢ ∀ x ∈ tris.attach, f x ∈ G.edgeFinset \ H.edgeFinset

Tactic:
have hf (x) (_ : x ∈ tris.attach) : f x ∈ G.edgeFinset \ H.edgeFinset := fmem _
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G H : SimpleGraph α
inst : Fintype α
inst_1 : DecidableRel G.Adj
inst_2 : DecidableRel H.Adj
inst_3 : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris : Set (Finset α)).Pairwise fun (x y : Finset α) ↦ ((↑x : Set α) ∩ (↑y : Set α)).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
hG : #(G.edgeFinset \ H.edgeFinset) < #tris.attach
fx fy : ⦃t : Finset α⦄ → (ht : t ∈ tris) → α
hfx : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fx ht ∈ t
hfy : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fy ht ∈ t
hfne : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fx ht ≠ fy ht
fmem : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), s(fx ht, fy ht) ∈ G.edgeFinset \ H.edgeFinset
f : (t : ↥tris) → Sym2 α := fun (t : ↥tris) ↦ s(fx ⋯, fy ⋯)
hf : ∀ x ∈ tris.attach, f x ∈ G.edgeFinset \ H.edgeFinset
obtain :
  ∀ (t₁ : Finset α) (ht₁ : t₁ ∈ tris) (t₂ : Finset α) (ht₂ : t₂ ∈ tris)
    (tne :
      Subtype.mk (p := fun (x : Finset α) ↦ x ∈ tris) t₁ ht₁ ≠ Subtype.mk (p := fun (x : Finset α) ↦ x ∈ tris) t₂ ht₂)
    (t : s(fx ⋯, fy ⋯) = s(fx ⋯, fy ⋯)), False
⊢ False

Tactic:
obtain ⟨⟨t₁, ht₁⟩, -, ⟨t₂, ht₂⟩, -, tne, t : s(_, _) = s(_, _)⟩ :=
    exists_ne_map_eq_of_card_lt_of_maps_to hG hf

Premises used: Finset.exists_ne_map_eq_of_card_lt_of_maps_to
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G H : SimpleGraph α
inst : Fintype α
inst_1 : DecidableRel G.Adj
inst_2 : DecidableRel H.Adj
inst_3 : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris : Set (Finset α)).Pairwise fun (x y : Finset α) ↦ ((↑x : Set α) ∩ (↑y : Set α)).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
hG : #(G.edgeFinset \ H.edgeFinset) < #tris.attach
fx fy : ⦃t : Finset α⦄ → (ht : t ∈ tris) → α
hfx : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fx ht ∈ t
hfy : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fy ht ∈ t
hfne : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fx ht ≠ fy ht
fmem : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), s(fx ht, fy ht) ∈ G.edgeFinset \ H.edgeFinset
f : (t : ↥tris) → Sym2 α := fun (t : ↥tris) ↦ s(fx ⋯, fy ⋯)
hf : ∀ x ∈ tris.attach, f x ∈ G.edgeFinset \ H.edgeFinset
t₁ : Finset α
ht₁ : t₁ ∈ tris
t₂ : Finset α
ht₂ : t₂ ∈ tris
tne : Subtype.mk (p := fun (x : Finset α) ↦ x ∈ tris) t₁ ht₁ ≠ Subtype.mk (p := fun (x : Finset α) ↦ x ∈ tris) t₂ ht₂
t : s(fx ⋯, fy ⋯) = s(fx ⋯, fy ⋯)
⊢ (fun (x y : Finset α) ↦ ((↑x : Set α) ∩ (↑y : Set α)).Subsingleton) t₁ t₂

Tactic:
have i := pd ht₁ ht₂ (Subtype.val_injective.ne tne)
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G H : SimpleGraph α
inst : Fintype α
inst_1 : DecidableRel G.Adj
inst_2 : DecidableRel H.Adj
inst_3 : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris : Set (Finset α)).Pairwise fun (x y : Finset α) ↦ ((↑x : Set α) ∩ (↑y : Set α)).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
hG : #(G.edgeFinset \ H.edgeFinset) < #tris.attach
fx fy : ⦃t : Finset α⦄ → (ht : t ∈ tris) → α
hfx : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fx ht ∈ t
hfy : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fy ht ∈ t
hfne : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fx ht ≠ fy ht
fmem : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), s(fx ht, fy ht) ∈ G.edgeFinset \ H.edgeFinset
f : (t : ↥tris) → Sym2 α := fun (t : ↥tris) ↦ s(fx ⋯, fy ⋯)
hf : ∀ x ∈ tris.attach, f x ∈ G.edgeFinset \ H.edgeFinset
t₁ : Finset α
ht₁ : t₁ ∈ tris
t₂ : Finset α
ht₂ : t₂ ∈ tris
tne : Subtype.mk (p := fun (x : Finset α) ↦ x ∈ tris) t₁ ht₁ ≠ Subtype.mk (p := fun (x : Finset α) ↦ x ∈ tris) t₂ ht₂
t : s(fx ⋯, fy ⋯) = s(fx ⋯, fy ⋯)
i : (fun (x y : Finset α) ↦ ((↑x : Set α) ∩ (↑y : Set α)).Subsingleton) t₁ t₂
⊢ fx ⋯ = fx ⋯ ∧ fy ⋯ = fy ⋯ ∨ fx ⋯ = fy ⋯ ∧ fy ⋯ = fx ⋯

Tactic:
rw [Sym2.eq_iff] at t

Premises used: Sym2.eq_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G H : SimpleGraph α
inst : Fintype α
inst_1 : DecidableRel G.Adj
inst_2 : DecidableRel H.Adj
inst_3 : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris : Set (Finset α)).Pairwise fun (x y : Finset α) ↦ ((↑x : Set α) ∩ (↑y : Set α)).Subsingleton
hHG : H ≤ G
hH : H.CliqueFree 3
hG : #(G.edgeFinset \ H.edgeFinset) < #tris.attach
fx fy : ⦃t : Finset α⦄ → (ht : t ∈ tris) → α
hfx : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fx ht ∈ t
hfy : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fy ht ∈ t
hfne : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), fx ht ≠ fy ht
fmem : ∀ ⦃t : Finset α⦄ (ht : t ∈ tris), s(fx ht, fy ht) ∈ G.edgeFinset \ H.edgeFinset
f : (t : ↥tris) → Sym2 α := fun (t : ↥tris) ↦ s(fx ⋯, fy ⋯)
hf : ∀ x ∈ tris.attach, f x ∈ G.edgeFinset \ H.edgeFinset
t₁ : Finset α
ht₁ : t₁ ∈ tris
t₂ : Finset α
ht₂ : t₂ ∈ tris
tne : Subtype.mk (p := fun (x : Finset α) ↦ x ∈ tris) t₁ ht₁ ≠ Subtype.mk (p := fun (x : Finset α) ↦ x ∈ tris) t₂ ht₂
t : s(fx ⋯, fy ⋯) = s(fx ⋯, fy ⋯)
i : (fun (x y : Finset α) ↦ ((↑x : Set α) ∩ (↑y : Set α)).Subsingleton) t₁ t₂
t₃ : fx ⋯ = fx ⋯ ∧ fy ⋯ = fy ⋯ ∨ fx ⋯ = fy ⋯ ∧ fy ⋯ = fx ⋯
⊢ ((↑t₁ : Set α) ∩ (↑t₂ : Set α)).Subsingleton

Tactic:
rw [Sym2.eq_iff] at t

Premises used: Sym2.eq_iff