awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
hG : G.LocallyLinear
⊢ LocallyLinear.{u_2} (α := β) (SimpleGraph.map (⇑f : (a : α) → β) G)
have refine : ∀ ⦃x y : β⦄,
  Adj (SimpleGraph.map (⇑f : (a : α) → β) G) x y →
    ∃ (s : Finset β), IsNClique (SimpleGraph.map (⇑f : (a : α) → β) G) 3 s ∧ x ∈ s ∧ y ∈ s
Tactic: refine ⟨hG.1.map _, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
hG : G.LocallyLinear
a b : α
h : G.Adj a b
⊢ ∃ (s : Finset β),
    IsNClique (SimpleGraph.map (⇑f : (a : α) → β) G) 3 s ∧
      Membership.mem (α := β) s ((f : (a : α) → β) a : β) ∧ Membership.mem (α := β) s ((f : (a : α) → β) b : β)
have obtain : ∀ (s : Finset α) (hs : G.IsNClique 3 s) (ha : a ∈ s) (hb : b ∈ s),
  ∃ (s : Finset β),
    IsNClique (SimpleGraph.map (⇑f : (a : α) → β) G) 3 s ∧
      Membership.mem (α := β) s ((f : (a : α) → β) a : β) ∧ Membership.mem (α := β) s ((f : (a : α) → β) b : β)
Tactic: obtain ⟨s, hs, ha, hb⟩ := hG.2 h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph β
e : α ≃ β
⊢ LocallyLinear.{u_1} (α := α) (SimpleGraph.comap (⇑e : (a : α) → β) G) ↔ G.LocallyLinear
have refine_1 : ∀ (h : LocallyLinear.{u_1} (α := α) (SimpleGraph.comap (⇑e : (a : α) → β) G)), G.LocallyLinear
Tactic: refine ⟨fun h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph β
e : α ≃ β
refine_1 : ∀ (h : LocallyLinear.{u_1} (α := α) (SimpleGraph.comap (⇑e : (a : α) → β) G)), G.LocallyLinear
⊢ LocallyLinear.{u_1} (α := α) (SimpleGraph.comap (⇑e : (a : α) → β) G) ↔ G.LocallyLinear
have refine_2 : G.LocallyLinear → LocallyLinear.{u_1} (α := α) (SimpleGraph.comap (⇑e : (a : α) → β) G)
Tactic: refine ⟨fun h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph β
e : α ≃ β
h : LocallyLinear.{u_1} (α := α) (SimpleGraph.comap (⇑e : (a : α) → β) G)
⊢ G.LocallyLinear
have refine_1 : LocallyLinear.{u_2} (α := β)
  (SimpleGraph.map.{u_1, u_2} (V := α) (⇑e.toEmbedding : (a : α) → β)
    (SimpleGraph.comap (⇑e.toEmbedding : (a : α) → β) G))
Tactic: rw [← comap_map_eq e.symm.toEmbedding G, comap_symm, map_symm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
G : SimpleGraph β
e : α ≃ β
⊢ G.LocallyLinear → LocallyLinear.{u_1} (α := α) (SimpleGraph.comap (⇑e : (a : α) → β) G)
have refine_2 : G.LocallyLinear → LocallyLinear.{u_1} (α := α) (SimpleGraph.map (⇑e.symm.toEmbedding : (a : β) → α) G)
Tactic: rw [← Equiv.coe_toEmbedding, ← map_symm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
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}}
have 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
Tactic: ext s
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
G : SimpleGraph α
a b : α
hab : a ≠ b
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
have 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}
Tactic: simp only [mem_sym2_iff, Sym2.mem_iff, forall_eq_or_imp, forall_eq,
      mem_cliqueSet_iff, Set.mem_setOf_eq,
      is3Clique_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
Goal:
α : Type u_1
G : SimpleGraph α
a b : α
hab : a ≠ b
s : Finset α
⊢ (∃ (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}
have 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}
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
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}
⊢ (∃ (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}
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (hypothesis)
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
⊢ 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}
have hab₁ : (a = c ∨ a = d ∨ a = e) ∧ (b = c ∨ b = d ∨ b = e)
Tactic: simp only [mem_insert, mem_singleton] at hab
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
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)
⊢ 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}
have 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}
Tactic: obtain ⟨rfl | rfl | rfl, rfl | rfl | rfl⟩ := hab
Cleared hypotheses: a, hab_1, c, hcd, hce, hab
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
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}
⊢ 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}
have 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}
Tactic: obtain ⟨rfl | rfl | rfl, rfl | rfl | rfl⟩ := hab
Cleared hypotheses: c, d, hcd, hce, hde, hab
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
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}
⊢ 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}
have 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}
Tactic: obtain ⟨rfl | rfl | rfl, rfl | rfl | rfl⟩ := hab
Cleared hypotheses: c, e, hcd, hce, hde, hab
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
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}
⊢ 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}
have 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}
Tactic: obtain ⟨rfl | rfl | rfl, rfl | rfl | rfl⟩ := hab
Cleared hypotheses: c, d, hcd, hce, hde, hab
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
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}
⊢ 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}
have 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}
Tactic: obtain ⟨rfl | rfl | rfl, rfl | rfl | rfl⟩ := hab
Cleared hypotheses: a, hab_1, d, hcd, hde, hab
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
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}
⊢ 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}
have 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}
Tactic: obtain ⟨rfl | rfl | rfl, rfl | rfl | rfl⟩ := hab
Cleared hypotheses: d, e, hcd, hce, hde, hab
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
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}
⊢ 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}
have 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}
Tactic: obtain ⟨rfl | rfl | rfl, rfl | rfl | rfl⟩ := hab
Cleared hypotheses: c, e, hcd, hce, hde, hab
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
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}
⊢ 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}
have 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}
Tactic: obtain ⟨rfl | rfl | rfl, rfl | rfl | rfl⟩ := hab
Cleared hypotheses: d, e, hcd, hce, hde, hab
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
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}
⊢ 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}
have 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}
Tactic: obtain ⟨rfl | rfl | rfl, rfl | rfl | rfl⟩ := hab
Cleared hypotheses: a, hab_1, e, hce, hde, hab
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
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 b ∧ ∃ (c : α), G.Adj a c ∧ G.Adj b c ∧ Eq (α := Finset α) {a, b, e} {a, b, c}
have h : ∃ (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 *
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
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
⊢ G.Adj a b ∧ ∃ (c : α), G.Adj a c ∧ G.Adj b c ∧ Eq (α := Finset α) {a, d, b} {a, b, c}
have h : ∀ (hde : G.Adj b d), ∃ (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 *
Cleared hypotheses: hde
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (hypothesis)
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 ∧ ∃ (c : α), G.Adj a c ∧ G.Adj b c ∧ Eq (α := Finset α) {b, a, e} {a, b, c}
have hcd₁ : G.Adj a b
Tactic: simp only [*, adj_comm, true_and, Ne, not_true] at *
Cleared hypotheses: hcd
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
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
⊢ 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}
have 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}
Tactic: simp only [*, adj_comm, true_and, Ne, not_true] at *
Cleared hypotheses: hcd, hce
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (hypothesis)
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 b ∧ ∃ (c : α), G.Adj a c ∧ G.Adj b c ∧ Eq (α := Finset α) {b, d, a} {a, b, c}
have hde₁ : G.Adj a d
Tactic: simp only [*, adj_comm, true_and, Ne, not_true] at *
Cleared hypotheses: hde, hce
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (hypothesis)
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 ∧ ∃ (c : α), G.Adj a c ∧ G.Adj b c ∧ Eq (α := Finset α) {b, d, a} {a, b, c}
have hce₁ : G.Adj a b
Tactic: simp only [*, adj_comm, true_and, Ne, not_true] at *
Cleared hypotheses: hde, hce
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (hypothesis)
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 b ∧ ∃ (c_1 : α), G.Adj a c_1 ∧ G.Adj b c_1 ∧ Eq (α := Finset α) {c, b, a} {a, b, c_1}
have hce₁ : G.Adj a c
Tactic: simp only [*, adj_comm, true_and, Ne, not_true] at *
Cleared hypotheses: hce, hcd, hde
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (hypothesis)
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 a b ∧ ∃ (c_1 : α), G.Adj a c_1 ∧ G.Adj b c_1 ∧ Eq (α := Finset α) {c, b, a} {a, b, c_1}
have hcd₁ : G.Adj b c
Tactic: simp only [*, adj_comm, true_and, Ne, not_true] at *
Cleared hypotheses: hce, hcd, hde
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (hypothesis)
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 ∧ ∃ (c_1 : α), G.Adj a c_1 ∧ G.Adj b c_1 ∧ Eq (α := Finset α) {c, b, a} {a, b, c_1}
have hde₁ : G.Adj a b
Tactic: simp only [*, adj_comm, true_and, Ne, not_true] at *
Cleared hypotheses: hce, hcd, hde
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
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 b ∧ ∃ (c : α), G.Adj a c ∧ G.Adj b c ∧ Eq (α := Finset α) {b, a, e} {a, b, c}
have h : ∃ (c : α), G.Adj a c ∧ G.Adj b c ∧ Eq (α := Finset α) {b, a, e} {a, b, c}
Tactic: simp only [*, true_and] at *
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
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 b ∧ ∃ (c : α), G.Adj a c ∧ G.Adj b c ∧ Eq (α := Finset α) {b, d, a} {a, b, c}
have h : ∃ (c : α), G.Adj a c ∧ G.Adj b c ∧ Eq (α := Finset α) {b, d, a} {a, b, c}
Tactic: simp only [*, true_and] at *
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
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 b ∧ ∃ (c_1 : α), G.Adj a c_1 ∧ G.Adj b c_1 ∧ Eq (α := Finset α) {c, b, a} {a, b, c_1}
have h : ∃ (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 *
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
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 b ∧ ∃ (c_1 : α), G.Adj a c_1 ∧ G.Adj b c_1 ∧ Eq (α := Finset α) {c, b, a} {a, b, c_1}
have h : ∃ (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⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
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
have h : G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ Eq (α := Finset α) {a, b, c} {a, b, c}
Tactic: refine ⟨⟨a, b, c, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Triangle.Basic (goal)
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}
⊢ (∃ (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
have h₁ : Membership.mem (γ := Finset α) {a, b, c} a ∧ Membership.mem (γ := Finset α) {a, b, c} b
Tactic: refine ⟨⟨a, b, c, ?_⟩, ?_⟩