awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph β
e : α ≃ β
h : LocallyLinear.{u_1} (α := α) (SimpleGraph.comap (⇑e : (a : α) → β) G)
⊢ LocallyLinear.{u_2} (α := β)
    (SimpleGraph.map.{u_1, u_2} (V := α) (⇑e.toEmbedding : (a : α) → β)
      (SimpleGraph.comap (⇑e.toEmbedding : (a : α) → β) G))

Tactic:
h.map _

Premises used: SimpleGraph.LocallyLinear.map
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph β
e : α ≃ β
h : LocallyLinear.{u_1} (α := α) (SimpleGraph.comap (⇑e : (a : α) → β) G)
⊢ LocallyLinear.{u_2} (α := β)
    (SimpleGraph.map.{u_1, u_2} (V := α) (⇑e.toEmbedding : (a : α) → β)
      (SimpleGraph.comap (⇑e.toEmbedding : (a : α) → β) G))

Tactic:
exact h.map _

Premises used: SimpleGraph.LocallyLinear.map
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph β
e : α ≃ β
refine_2 : G.LocallyLinear → LocallyLinear.{u_1} (α := α) (SimpleGraph.map (⇑e.symm.toEmbedding : (a : β) → α) G)
⊢ G.LocallyLinear → LocallyLinear.{u_1} (α := α) (SimpleGraph.comap (⇑e : (a : α) → β) G)

Tactic:
rw [← Equiv.coe_toEmbedding, ← map_symm]

Premises used: Equiv.coe_toEmbedding, SimpleGraph.map_symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph β
e : α ≃ β
⊢ G.LocallyLinear → LocallyLinear.{u_1} (α := α) (SimpleGraph.map (⇑e.symm.toEmbedding : (a : β) → α) G)

Tactic:
LocallyLinear.map _

Premises used: SimpleGraph.LocallyLinear.map
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph β
e : α ≃ β
⊢ G.LocallyLinear → LocallyLinear.{u_1} (α := α) (SimpleGraph.map (⇑e.symm.toEmbedding : (a : β) → α) G)

Tactic:
exact LocallyLinear.map _

Premises used: SimpleGraph.LocallyLinear.map
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
a b : α
hab : a ≠ b
h :
  ∀ (s : Finset α),
    Membership.mem (γ := Set (Finset α)) {s : Finset α | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2} s ↔
      Membership.mem (γ := Set (Finset α)) {s : Finset α | G.Adj a b ∧ ∃ (c : α), G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}}
        s
⊢ Eq.{u_1 + 1} (α := Set (Finset α)) {s : Finset α | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2}
    {s : Finset α | G.Adj a b ∧ ∃ (c : α), G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}}

Tactic:
ext s
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
a b : α
hab : a ≠ b
s : Finset α
h :
  (∃ (a : α) (b : α) (c : α), G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}) ∧ a ∈ s ∧ b ∈ s ↔
    G.Adj a b ∧ ∃ (c : α), G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}
⊢ Membership.mem (γ := Set (Finset α)) {s : Finset α | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2} s ↔
    Membership.mem (γ := Set (Finset α)) {s : Finset α | G.Adj a b ∧ ∃ (c : α), G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}} s

Tactic:
simp only [mem_sym2_iff, Sym2.mem_iff, forall_eq_or_imp, forall_eq,
      mem_cliqueSet_iff, Set.mem_setOf_eq,
      is3Clique_iff]

Premises used: forall_eq, Finset.mem_sym2_iff, Set.mem_setOf_eq, forall_eq_or_imp, Sym2.mem_iff, SimpleGraph.is3Clique_iff, SimpleGraph.mem_cliqueSet_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
a b : α
hab : a ≠ b
s : Finset α
h :
  (∃ (a : α) (b : α) (c : α), G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}) ∧ a ∈ s ∧ b ∈ s →
    G.Adj a b ∧ ∃ (c : α), G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}
h₁ :
  (G.Adj a b ∧ ∃ (c : α), G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}) →
    (∃ (a : α) (b : α) (c : α), G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}) ∧ a ∈ s ∧ b ∈ s
⊢ (∃ (a : α) (b : α) (c : α), G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}) ∧ a ∈ s ∧ b ∈ s ↔
    G.Adj a b ∧ ∃ (c : α), G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
a b : α
hab_1 : a ≠ b
c d e : α
hcd : G.Adj c d
hce : G.Adj c e
hde : G.Adj d e
hab : Membership.mem (γ := Finset α) {c, d, e} a ∧ Membership.mem (γ := Finset α) {c, d, e} b
⊢ (a = c ∨ a = d ∨ a = e) ∧ (b = c ∨ b = d ∨ b = e)

Tactic:
simp only [mem_insert, mem_singleton] at hab

Premises used: Finset.mem_singleton, Finset.mem_insert
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
a b : α
hab_1 : a ≠ b
c d e : α
hcd : G.Adj c d
hce : G.Adj c e
hde : G.Adj d e
hab : (a = c ∨ a = d ∨ a = e) ∧ (b = c ∨ b = d ∨ b = e)
h :
  ∀ (hab : b ≠ b) (hcd : G.Adj b d) (hce : G.Adj b e),
    G.Adj b b ∧ ∃ (c : α), G.Adj b c ∧ G.Adj b c ∧ Eq (α := Finset α) {b, d, e} {b, b, c}
h₁ :
  ∀ (hce : G.Adj a e) (hde : G.Adj b e) (hcd : G.Adj a b),
    G.Adj a b ∧ ∃ (c : α), G.Adj a c ∧ G.Adj b c ∧ Eq (α := Finset α) {a, b, e} {a, b, c}
h₂ :
  ∀ (hcd : G.Adj a d) (hde : G.Adj d b) (hce : G.Adj a b),
    G.Adj a b ∧ ∃ (c : α), G.Adj a c ∧ G.Adj b c ∧ Eq (α := Finset α) {a, d, b} {a, b, c}
h₃ :
  ∀ (hde : G.Adj a e) (hce : G.Adj b e) (hcd : G.Adj b a),
    G.Adj a b ∧ ∃ (c : α), G.Adj a c ∧ G.Adj b c ∧ Eq (α := Finset α) {b, a, e} {a, b, c}
h₄ :
  ∀ (hab : b ≠ b) (hcd : G.Adj c b) (hde : G.Adj b e),
    G.Adj b b ∧ ∃ (c_1 : α), G.Adj b c_1 ∧ G.Adj b c_1 ∧ Eq (α := Finset α) {c, b, e} {b, b, c_1}
h₅ :
  ∀ (hcd : G.Adj c a) (hce : G.Adj c b) (hde : G.Adj a b),
    G.Adj a b ∧ ∃ (c_1 : α), G.Adj a c_1 ∧ G.Adj b c_1 ∧ Eq (α := Finset α) {c, a, b} {a, b, c_1}
h₆ :
  ∀ (hde : G.Adj d a) (hcd : G.Adj b d) (hce : G.Adj b a),
    G.Adj a b ∧ ∃ (c : α), G.Adj a c ∧ G.Adj b c ∧ Eq (α := Finset α) {b, d, a} {a, b, c}
h₇ :
  ∀ (hce : G.Adj c a) (hcd : G.Adj c b) (hde : G.Adj b a),
    G.Adj a b ∧ ∃ (c_1 : α), G.Adj a c_1 ∧ G.Adj b c_1 ∧ Eq (α := Finset α) {c, b, a} {a, b, c_1}
h₈ :
  ∀ (hab : b ≠ b) (hce : G.Adj c b) (hde : G.Adj d b),
    G.Adj b b ∧ ∃ (c_1 : α), G.Adj b c_1 ∧ G.Adj b c_1 ∧ Eq (α := Finset α) {c, d, b} {b, b, c_1}
⊢ G.Adj a b ∧ ∃ (c_1 : α), G.Adj a c_1 ∧ G.Adj b c_1 ∧ Eq (α := Finset α) {c, d, e} {a, b, c_1}

Tactic:
obtain ⟨rfl | rfl | rfl, rfl | rfl | rfl⟩ := hab

Premises used: rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
b d e : α
hde : G.Adj d e
hab : b ≠ b
hcd : G.Adj b d
hce : G.Adj b e
⊢ G.Adj b b ∧ ∃ (c : α), G.Adj b c ∧ G.Adj b c ∧ Eq (α := Finset α) {b, d, e} {b, b, c}

Tactic:
simp only [*, adj_comm, true_and, Ne, not_true] at *

Premises used: Ne, not_true, true_and, SimpleGraph.adj_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
a b : α
hab : a ≠ b
e : α
hce : G.Adj a e
hde : G.Adj b e
hcd : G.Adj a b
h : ∃ (c : α), G.Adj a c ∧ G.Adj b c ∧ Eq (α := Finset α) {a, b, e} {a, b, c}
⊢ G.Adj a b ∧ ∃ (c : α), G.Adj a c ∧ G.Adj b c ∧ Eq (α := Finset α) {a, b, e} {a, b, c}

Tactic:
simp only [*, adj_comm, true_and, Ne, not_true] at *

Premises used: Ne, not_true, true_and, SimpleGraph.adj_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
a b : α
hab : a ≠ b
d : α
hcd : G.Adj a d
hde : G.Adj d b
hce : G.Adj a b
h : ∀ (hde : G.Adj b d), ∃ (c : α), G.Adj a c ∧ G.Adj b c ∧ Eq (α := Finset α) {a, d, b} {a, b, c}
⊢ G.Adj a b ∧ ∃ (c : α), G.Adj a c ∧ G.Adj b c ∧ Eq (α := Finset α) {a, d, b} {a, b, c}

Tactic:
simp only [*, adj_comm, true_and, Ne, not_true] at *

Premises used: Ne, not_true, true_and, SimpleGraph.adj_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
a b : α
hab : a ≠ b
e : α
hde : G.Adj a e
hce : G.Adj b e
hcd : G.Adj b a
⊢ G.Adj a b

Tactic:
simp only [*, adj_comm, true_and, Ne, not_true] at *

Premises used: Ne, not_true, true_and, SimpleGraph.adj_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
b c e : α
hce : G.Adj c e
hab : b ≠ b
hcd : G.Adj c b
hde : G.Adj b e
⊢ G.Adj b b ∧ ∃ (c_1 : α), G.Adj b c_1 ∧ G.Adj b c_1 ∧ Eq (α := Finset α) {c, b, e} {b, b, c_1}

Tactic:
simp only [*, adj_comm, true_and, Ne, not_true] at *

Premises used: Ne, not_true, true_and, SimpleGraph.adj_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
a b : α
hab : a ≠ b
c : α
hcd : G.Adj c a
hce : G.Adj c b
hde : G.Adj a b
h :
  ∀ (hcd : G.Adj a c) (hce : G.Adj b c),
    ∃ (c_1 : α), G.Adj a c_1 ∧ G.Adj b c_1 ∧ Eq (α := Finset α) {c, a, b} {a, b, c_1}
⊢ G.Adj a b ∧ ∃ (c_1 : α), G.Adj a c_1 ∧ G.Adj b c_1 ∧ Eq (α := Finset α) {c, a, b} {a, b, c_1}

Tactic:
simp only [*, adj_comm, true_and, Ne, not_true] at *

Premises used: Ne, not_true, true_and, SimpleGraph.adj_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
a b : α
hab : a ≠ b
d : α
hde : G.Adj d a
hcd : G.Adj b d
hce : G.Adj b a
⊢ G.Adj a d

Tactic:
simp only [*, adj_comm, true_and, Ne, not_true] at *

Premises used: Ne, not_true, true_and, SimpleGraph.adj_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
a b : α
hab : a ≠ b
d : α
hde : G.Adj d a
hcd : G.Adj b d
hce : G.Adj b a
hde₁ : G.Adj a d
⊢ G.Adj a b

Tactic:
simp only [*, adj_comm, true_and, Ne, not_true] at *

Premises used: Ne, not_true, true_and, SimpleGraph.adj_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
a b : α
hab : a ≠ b
c : α
hce : G.Adj c a
hcd : G.Adj c b
hde : G.Adj b a
⊢ G.Adj a c

Tactic:
simp only [*, adj_comm, true_and, Ne, not_true] at *

Premises used: Ne, not_true, true_and, SimpleGraph.adj_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
a b : α
hab : a ≠ b
c : α
hce : G.Adj c a
hcd : G.Adj c b
hde : G.Adj b a
hce₁ : G.Adj a c
⊢ G.Adj b c

Tactic:
simp only [*, adj_comm, true_and, Ne, not_true] at *

Premises used: Ne, not_true, true_and, SimpleGraph.adj_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
a b : α
hab : a ≠ b
c : α
hce : G.Adj c a
hcd : G.Adj c b
hde : G.Adj b a
hce₁ : G.Adj a c
hcd₁ : G.Adj b c
⊢ G.Adj a b

Tactic:
simp only [*, adj_comm, true_and, Ne, not_true] at *

Premises used: Ne, not_true, true_and, SimpleGraph.adj_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
b c d : α
hcd : G.Adj c d
hab : b ≠ b
hce : G.Adj c b
hde : G.Adj d b
⊢ G.Adj b b ∧ ∃ (c_1 : α), G.Adj b c_1 ∧ G.Adj b c_1 ∧ Eq (α := Finset α) {c, d, b} {b, b, c_1}

Tactic:
simp only [*, adj_comm, true_and, Ne, not_true] at *

Premises used: Ne, not_true, true_and, SimpleGraph.adj_comm
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
e : α
hce : G.Adj a e
hde : G.Adj b e
hcd : G.Adj a b
⊢ G.Adj a e ∧ G.Adj b e ∧ Eq (α := Finset α) {a, b, e} {a, b, e}

Tactic:
aesop
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
e : α
hce : G.Adj a e
hde : G.Adj b e
hcd : G.Adj a b
⊢ ∃ (c : α), G.Adj a c ∧ G.Adj b c ∧ Eq (α := Finset α) {a, b, e} {a, b, c}

Tactic:
exact ⟨e, by aesop⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
e : α
hce : G.Adj a e
hde : G.Adj b e
hcd : G.Adj a b
⊢ ∃ (c : α), G.Adj a c ∧ G.Adj b c ∧ Eq (α := Finset α) {a, b, e} {a, b, c}

Tactic:
first
        | exact ⟨c, by aesop⟩
        | exact ⟨d, by aesop⟩
        | exact ⟨e, by aesop⟩
        | simp only [*, true_and] at *
          exact ⟨c, by aesop⟩
        | simp only [*, true_and] at *
          exact ⟨d, by aesop⟩
        | simp only [*, true_and] at *
          exact ⟨e, by aesop⟩

Premises used: true_and
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
d : α
hcd : G.Adj a d
hce : G.Adj a b
hde : G.Adj b d
⊢ G.Adj a d ∧ G.Adj b d ∧ Eq (α := Finset α) {a, d, b} {a, b, d}

Tactic:
aesop
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
d : α
hcd : G.Adj a d
hce : G.Adj a b
hde : G.Adj b d
⊢ ∃ (c : α), G.Adj a c ∧ G.Adj b c ∧ Eq (α := Finset α) {a, d, b} {a, b, c}

Tactic:
exact ⟨d, by aesop⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
d : α
hcd : G.Adj a d
hce : G.Adj a b
hde : G.Adj b d
⊢ ∃ (c : α), G.Adj a c ∧ G.Adj b c ∧ Eq (α := Finset α) {a, d, b} {a, b, c}

Tactic:
first
        | exact ⟨c, by aesop⟩
        | exact ⟨d, by aesop⟩
        | exact ⟨e, by aesop⟩
        | simp only [*, true_and] at *
          exact ⟨c, by aesop⟩
        | simp only [*, true_and] at *
          exact ⟨d, by aesop⟩
        | simp only [*, true_and] at *
          exact ⟨e, by aesop⟩

Premises used: true_and
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
e : α
hde : G.Adj a e
hce : G.Adj b e
hcd : G.Adj a b
h : ∃ (c : α), G.Adj a c ∧ G.Adj b c ∧ Eq (α := Finset α) {b, a, e} {a, b, c}
⊢ G.Adj a b ∧ ∃ (c : α), G.Adj a c ∧ G.Adj b c ∧ Eq (α := Finset α) {b, a, e} {a, b, c}

Tactic:
simp only [*, true_and] at *

Premises used: true_and
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
e : α
hde : G.Adj a e
hce : G.Adj b e
hcd : G.Adj a b
⊢ G.Adj a e ∧ G.Adj b e ∧ Eq (α := Finset α) {b, a, e} {a, b, e}

Tactic:
aesop
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
e : α
hde : G.Adj a e
hce : G.Adj b e
hcd : G.Adj a b
⊢ ∃ (c : α), G.Adj a c ∧ G.Adj b c ∧ Eq (α := Finset α) {b, a, e} {a, b, c}

Tactic:
exact ⟨e, by aesop⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
c : α
hde : G.Adj a b
hcd : G.Adj a c
hce : G.Adj b c
⊢ G.Adj a c ∧ G.Adj b c ∧ Eq (α := Finset α) {c, a, b} {a, b, c}

Tactic:
aesop
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
c : α
hde : G.Adj a b
hcd : G.Adj a c
hce : G.Adj b c
⊢ ∃ (c_1 : α), G.Adj a c_1 ∧ G.Adj b c_1 ∧ Eq (α := Finset α) {c, a, b} {a, b, c_1}

Tactic:
exact ⟨c, by aesop⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
c : α
hde : G.Adj a b
hcd : G.Adj a c
hce : G.Adj b c
⊢ ∃ (c_1 : α), G.Adj a c_1 ∧ G.Adj b c_1 ∧ Eq (α := Finset α) {c, a, b} {a, b, c_1}

Tactic:
first
        | exact ⟨c, by aesop⟩
        | exact ⟨d, by aesop⟩
        | exact ⟨e, by aesop⟩
        | simp only [*, true_and] at *
          exact ⟨c, by aesop⟩
        | simp only [*, true_and] at *
          exact ⟨d, by aesop⟩
        | simp only [*, true_and] at *
          exact ⟨e, by aesop⟩

Premises used: true_and
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
d : α
hcd : G.Adj b d
hde : G.Adj a d
hce : G.Adj a b
h : ∃ (c : α), G.Adj a c ∧ G.Adj b c ∧ Eq (α := Finset α) {b, d, a} {a, b, c}
⊢ G.Adj a b ∧ ∃ (c : α), G.Adj a c ∧ G.Adj b c ∧ Eq (α := Finset α) {b, d, a} {a, b, c}

Tactic:
simp only [*, true_and] at *

Premises used: true_and
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
d : α
hcd : G.Adj b d
hde : G.Adj a d
hce : G.Adj a b
⊢ G.Adj a d ∧ G.Adj b d ∧ Eq (α := Finset α) {b, d, a} {a, b, d}

Tactic:
aesop
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
d : α
hcd : G.Adj b d
hde : G.Adj a d
hce : G.Adj a b
⊢ ∃ (c : α), G.Adj a c ∧ G.Adj b c ∧ Eq (α := Finset α) {b, d, a} {a, b, c}

Tactic:
exact ⟨d, by aesop⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
c : α
hce : G.Adj a c
hcd : G.Adj b c
hde : G.Adj a b
h : ∃ (c_1 : α), G.Adj a c_1 ∧ G.Adj b c_1 ∧ Eq (α := Finset α) {c, b, a} {a, b, c_1}
⊢ G.Adj a b ∧ ∃ (c_1 : α), G.Adj a c_1 ∧ G.Adj b c_1 ∧ Eq (α := Finset α) {c, b, a} {a, b, c_1}

Tactic:
simp only [*, true_and] at *

Premises used: true_and
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
c : α
hce : G.Adj a c
hcd : G.Adj b c
hde : G.Adj a b
⊢ G.Adj a c ∧ G.Adj b c ∧ Eq (α := Finset α) {c, b, a} {a, b, c}

Tactic:
aesop
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
c : α
hce : G.Adj a c
hcd : G.Adj b c
hde : G.Adj a b
⊢ ∃ (c_1 : α), G.Adj a c_1 ∧ G.Adj b c_1 ∧ Eq (α := Finset α) {c, b, a} {a, b, c_1}

Tactic:
exact ⟨c, by aesop⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
c : α
hce : G.Adj a c
hcd : G.Adj b c
hde : G.Adj a b
h : ∃ (c_1 : α), G.Adj a c_1 ∧ G.Adj b c_1 ∧ Eq (α := Finset α) {c, b, a} {a, b, c_1}
⊢ G.Adj a b ∧ ∃ (c_1 : α), G.Adj a c_1 ∧ G.Adj b c_1 ∧ Eq (α := Finset α) {c, b, a} {a, b, c_1}

Tactic:
first
        | exact ⟨c, by aesop⟩
        | exact ⟨d, by aesop⟩
        | exact ⟨e, by aesop⟩
        | simp only [*, true_and] at *
          exact ⟨c, by aesop⟩
        | simp only [*, true_and] at *
          exact ⟨d, by aesop⟩
        | simp only [*, true_and] at *
          exact ⟨e, by aesop⟩

Premises used: true_and
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
a b : α
hab_1 : a ≠ b
hab : G.Adj a b
c : α
hac : G.Adj a c
hbc : G.Adj b c
⊢ (∃ (a_1 : α) (b_1 : α) (c_1 : α),
      G.Adj a_1 b_1 ∧ G.Adj a_1 c_1 ∧ G.Adj b_1 c_1 ∧ Eq (α := Finset α) {a, b, c} {a_1, b_1, c_1}) ∧
    Membership.mem (γ := Finset α) {a, b, c} a ∧ Membership.mem (γ := Finset α) {a, b, c} b

Tactic:
⟨⟨a, b, c, ?_⟩, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
a b : α
hab_1 : a ≠ b
hab : G.Adj a b
c : α
hac : G.Adj a c
hbc : G.Adj b c
h : G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ Eq (α := Finset α) {a, b, c} {a, b, c}
h₁ : Membership.mem (γ := Finset α) {a, b, c} a ∧ Membership.mem (γ := Finset α) {a, b, c} b
⊢ (∃ (a_1 : α) (b_1 : α) (c_1 : α),
      G.Adj a_1 b_1 ∧ G.Adj a_1 c_1 ∧ G.Adj b_1 c_1 ∧ Eq (α := Finset α) {a, b, c} {a_1, b_1, c_1}) ∧
    Membership.mem (γ := Finset α) {a, b, c} a ∧ Membership.mem (γ := Finset α) {a, b, c} b

Tactic:
refine ⟨⟨a, b, c, ?_⟩, ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
a b : α
hab_1 : a ≠ b
hab : G.Adj a b
c : α
hac : G.Adj a c
hbc : G.Adj b c
⊢ G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ Eq (α := Finset α) {a, b, c} {a, b, c}

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
a b : α
hab_1 : a ≠ b
hab : G.Adj a b
c : α
hac : G.Adj a c
hbc : G.Adj b c
⊢ Membership.mem (γ := Finset α) {a, b, c} a ∧ Membership.mem (γ := Finset α) {a, b, c} b

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
⊢ ∀ (a b : α) (hab : a ≠ b),
    Eq.{u_1 + 1} (α := Set (Finset α)) {s : Finset α | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2}
      {s : Finset α | G.Adj a b ∧ ∃ (c : α), G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}}

Tactic:
have (a b) (hab : a ≠ b) : {s ∈ (G.cliqueSet 3 : Set (Finset α)) | s(a, b) ∈ (s : Finset α).sym2}
    = {s | G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}} := by
    ext s
    simp only [mem_sym2_iff, Sym2.mem_iff, forall_eq_or_imp, forall_eq,
      mem_cliqueSet_iff, Set.mem_setOf_eq,
      is3Clique_iff]
    constructor
    · rintro ⟨⟨c, d, e, hcd, hce, hde, rfl⟩, hab⟩
      simp only [mem_insert, mem_singleton] at hab
      obtain ⟨rfl | rfl | rfl, rfl | rfl | rfl⟩ := hab
      any_goals
        simp only [*, adj_comm, true_and, Ne, not_true] at *
      any_goals
        first
        | exact ⟨c, by aesop⟩
        | exact ⟨d, by aesop⟩
        | exact ⟨e, by aesop⟩
        | simp only [*, true_and] at *
          exact ⟨c, by aesop⟩
        | simp only [*, true_and] at *
          exact ⟨d, by aesop⟩
        | simp only [*, true_and] at *
          exact ⟨e, by aesop⟩
    · rintro ⟨hab, c, hac, hbc, rfl⟩
      refine ⟨⟨a, b, c, ?_⟩, ?_⟩ <;> simp [*]
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
this :
  ∀ (a b : α) (hab : a ≠ b),
    Eq.{u_1 + 1} (α := Set (Finset α)) {s : Finset α | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2}
      {s : Finset α | G.Adj a b ∧ ∃ (c : α), G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}}
mp :
  G.EdgeDisjointTriangles →
    ∀ ⦃e : Sym2 α⦄, ¬e.IsDiag → Set.Subsingleton.{u_1} (α := Finset α) {s : Finset α | s ∈ G.cliqueSet 3 ∧ e ∈ s.sym2}
mpr :
  (∀ ⦃e : Sym2 α⦄, ¬e.IsDiag → Set.Subsingleton.{u_1} (α := Finset α) {s : Finset α | s ∈ G.cliqueSet 3 ∧ e ∈ s.sym2}) →
    G.EdgeDisjointTriangles
⊢ G.EdgeDisjointTriangles ↔
    ∀ ⦃e : Sym2 α⦄, ¬e.IsDiag → Set.Subsingleton.{u_1} (α := Finset α) {s : Finset α | s ∈ G.cliqueSet 3 ∧ e ∈ s.sym2}

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
this :
  ∀ (a b : α) (hab : a ≠ b),
    Eq.{u_1 + 1} (α := Set (Finset α)) {s : Finset α | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2}
      {s : Finset α | G.Adj a b ∧ ∃ (c : α), G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}}
mp :
  G.EdgeDisjointTriangles →
    ∀ (x y : α),
      ¬s(x, y).IsDiag → Set.Subsingleton.{u_1} (α := Finset α) {s : Finset α | s ∈ G.cliqueSet 3 ∧ s(x, y) ∈ s.sym2}
⊢ G.EdgeDisjointTriangles →
    ∀ ⦃e : Sym2 α⦄, ¬e.IsDiag → Set.Subsingleton.{u_1} (α := Finset α) {s : Finset α | s ∈ G.cliqueSet 3 ∧ e ∈ s.sym2}

Tactic:
rw [Sym2.forall]

Premises used: Sym2.forall
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
this :
  ∀ (a b : α) (hab : a ≠ b),
    Eq.{u_1 + 1} (α := Set (Finset α)) {s : Finset α | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2}
      {s : Finset α | G.Adj a b ∧ ∃ (c : α), G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}}
hG : G.EdgeDisjointTriangles
a b : α
hab : ¬s(a, b).IsDiag
⊢ ¬a = b

Tactic:
simp only [Sym2.mk_isDiag_iff] at hab

Premises used: Sym2.mk_isDiag_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
this :
  ∀ (a b : α) (hab : a ≠ b),
    Eq.{u_1 + 1} (α := Set (Finset α)) {s : Finset α | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2}
      {s : Finset α | G.Adj a b ∧ ∃ (c : α), G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}}
hG : G.EdgeDisjointTriangles
a b : α
hab : ¬a = b
mp :
  Set.Subsingleton.{u_1} (α := Finset α)
    {s : Finset α |
      G.Adj (a, b).1 (a, b).2 ∧ ∃ (c : α), G.Adj (a, b).1 c ∧ G.Adj (a, b).2 c ∧ s = {(a, b).1, (a, b).2, c}}
⊢ Set.Subsingleton.{u_1} (α := Finset α) {s : Finset α | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2}

Tactic:
rw [this _ _ (Sym2.mk_isDiag_iff.not.2 hab)]

Premises used: Iff.mpr, Iff.not, Sym2.mk_isDiag_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
Goal:
α : Type u_1
G : SimpleGraph α
this :
  ∀ (a b : α) (hab : a ≠ b),
    Eq.{u_1 + 1} (α := Set (Finset α)) {s : Finset α | s ∈ G.cliqueSet 3 ∧ s(a, b) ∈ s.sym2}
      {s : Finset α | G.Adj a b ∧ ∃ (c : α), G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}}
hG : G.EdgeDisjointTriangles
a b : α
hab_1 : ¬a = b
hab : G.Adj (a, b).1 (a, b).2
c : α
hac : G.Adj (a, b).1 c
hbc : G.Adj (a, b).2 c
d : α
had : G.Adj (a, b).1 d
hbd : G.Adj (a, b).2 d
⊢ Eq (α := Finset α) {(a, b).1, (a, b).2, c} {(a, b).1, (a, b).2, d}

Tactic:
hG.eq ?_ ?_ (Set.Nontrivial.not_subsingleton ⟨a, ?_, b, ?_, hab.ne⟩)

Premises used: SimpleGraph.Adj.ne, Set.Nontrivial.not_subsingleton, And.intro, Exists.intro, Set.Pairwise.eq