awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
vertexSet : Set α
IsLink : β → α → α → Prop
edgeSet : Set β
isLink_symm : ∀ ⦃e : β⦄, e ∈ edgeSet → Symmetric (IsLink e)
eq_or_eq_of_isLink_of_isLink : ∀ ⦃e : β⦄ ⦃x y v w : α⦄, IsLink e x y → IsLink e v w → x = v ∨ x = w
h : ∀ (e : β), e ∈ edgeSet ↔ ∃ (x : α) (y : α), IsLink e x y
left_mem_of_isLink : ∀ ⦃e : β⦄ ⦃x y : α⦄, IsLink e x y → x ∈ vertexSet
hE :
  ∀ (e : β),
    e ∈
        E({ vertexSet := vertexSet, IsLink := IsLink, edgeSet := edgeSet, isLink_symm := isLink_symm,
            eq_or_eq_of_isLink_of_isLink := eq_or_eq_of_isLink_of_isLink, edge_mem_iff_exists_isLink := h,
            left_mem_of_isLink := left_mem_of_isLink : Graph α β }) ↔
      ∃ (x : α) (y : α),
        { vertexSet := vertexSet, IsLink := IsLink, edgeSet := edgeSet, isLink_symm := isLink_symm,
              eq_or_eq_of_isLink_of_isLink := eq_or_eq_of_isLink_of_isLink, edge_mem_iff_exists_isLink := h,
              left_mem_of_isLink := left_mem_of_isLink : Graph α β }.IsLink
          e x y
⊢ {
      vertexSet :=
        V({ vertexSet := vertexSet, IsLink := IsLink, edgeSet := edgeSet, isLink_symm := isLink_symm,
            eq_or_eq_of_isLink_of_isLink := eq_or_eq_of_isLink_of_isLink, edge_mem_iff_exists_isLink := h,
            left_mem_of_isLink := left_mem_of_isLink : Graph α β }),
      IsLink :=
        { vertexSet := vertexSet, IsLink := IsLink, edgeSet := edgeSet, isLink_symm := isLink_symm,
            eq_or_eq_of_isLink_of_isLink := eq_or_eq_of_isLink_of_isLink, edge_mem_iff_exists_isLink := h,
            left_mem_of_isLink := left_mem_of_isLink : Graph α β }.IsLink,
      edgeSet :=
        E({ vertexSet := vertexSet, IsLink := IsLink, edgeSet := edgeSet, isLink_symm := isLink_symm,
            eq_or_eq_of_isLink_of_isLink := eq_or_eq_of_isLink_of_isLink, edge_mem_iff_exists_isLink := h,
            left_mem_of_isLink := left_mem_of_isLink : Graph α β }),
      isLink_symm := ⋯, eq_or_eq_of_isLink_of_isLink := ⋯, edge_mem_iff_exists_isLink := hE, left_mem_of_isLink := ⋯ :
      Graph α β } =
    { vertexSet := vertexSet, IsLink := IsLink, edgeSet := edgeSet, isLink_symm := isLink_symm,
      eq_or_eq_of_isLink_of_isLink := eq_or_eq_of_isLink_of_isLink, edge_mem_iff_exists_isLink := h,
      left_mem_of_isLink := left_mem_of_isLink }

Tactic:
simp
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
hE : ∀ (e : β), e ∈ E(G) ↔ ∃ (x : α) (y : α), G.IsLink e x y
mk :
  ∀ (vertexSet : Set α) (IsLink : β → α → α → Prop) (edgeSet : Set β)
    (isLink_symm : ∀ ⦃e : β⦄, e ∈ edgeSet → Symmetric (IsLink e))
    (eq_or_eq_of_isLink_of_isLink : ∀ ⦃e : β⦄ ⦃x y v w : α⦄, IsLink e x y → IsLink e v w → x = v ∨ x = w)
    (h : ∀ (e : β), e ∈ edgeSet ↔ ∃ (x : α) (y : α), IsLink e x y)
    (left_mem_of_isLink : ∀ ⦃e : β⦄ ⦃x y : α⦄, IsLink e x y → x ∈ vertexSet)
    (hE :
      ∀ (e : β),
        e ∈
            E({ vertexSet := vertexSet, IsLink := IsLink, edgeSet := edgeSet, isLink_symm := isLink_symm,
                eq_or_eq_of_isLink_of_isLink := eq_or_eq_of_isLink_of_isLink, edge_mem_iff_exists_isLink := h,
                left_mem_of_isLink := left_mem_of_isLink : Graph α β }) ↔
          ∃ (x : α) (y : α),
            { vertexSet := vertexSet, IsLink := IsLink, edgeSet := edgeSet, isLink_symm := isLink_symm,
                  eq_or_eq_of_isLink_of_isLink := eq_or_eq_of_isLink_of_isLink, edge_mem_iff_exists_isLink := h,
                  left_mem_of_isLink := left_mem_of_isLink : Graph α β }.IsLink
              e x y),
    {
        vertexSet :=
          V({ vertexSet := vertexSet, IsLink := IsLink, edgeSet := edgeSet, isLink_symm := isLink_symm,
              eq_or_eq_of_isLink_of_isLink := eq_or_eq_of_isLink_of_isLink, edge_mem_iff_exists_isLink := h,
              left_mem_of_isLink := left_mem_of_isLink : Graph α β }),
        IsLink :=
          { vertexSet := vertexSet, IsLink := IsLink, edgeSet := edgeSet, isLink_symm := isLink_symm,
              eq_or_eq_of_isLink_of_isLink := eq_or_eq_of_isLink_of_isLink, edge_mem_iff_exists_isLink := h,
              left_mem_of_isLink := left_mem_of_isLink : Graph α β }.IsLink,
        edgeSet :=
          E({ vertexSet := vertexSet, IsLink := IsLink, edgeSet := edgeSet, isLink_symm := isLink_symm,
              eq_or_eq_of_isLink_of_isLink := eq_or_eq_of_isLink_of_isLink, edge_mem_iff_exists_isLink := h,
              left_mem_of_isLink := left_mem_of_isLink : Graph α β }),
        isLink_symm := ⋯, eq_or_eq_of_isLink_of_isLink := ⋯, edge_mem_iff_exists_isLink := hE, left_mem_of_isLink := ⋯ :
        Graph α β } =
      { vertexSet := vertexSet, IsLink := IsLink, edgeSet := edgeSet, isLink_symm := isLink_symm,
        eq_or_eq_of_isLink_of_isLink := eq_or_eq_of_isLink_of_isLink, edge_mem_iff_exists_isLink := h,
        left_mem_of_isLink := left_mem_of_isLink }
⊢ { vertexSet := V(G), IsLink := G.IsLink, edgeSet := E(G), isLink_symm := ⋯, eq_or_eq_of_isLink_of_isLink := ⋯,
      edge_mem_iff_exists_isLink := hE, left_mem_of_isLink := ⋯ : Graph α β } =
    G

Tactic:
cases G with | _ _ _ _ _ _ h _ => simp
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
G₁ G₂ : Graph α β
hV : V(G₁) = V(G₂)
h : ∀ (e : β) (x y : α), G₁.IsLink e x y ↔ G₂.IsLink e x y
rw :
  { vertexSet := V(G₁), IsLink := G₁.IsLink, edgeSet := E(G₁), isLink_symm := ⋯, eq_or_eq_of_isLink_of_isLink := ⋯,
      edge_mem_iff_exists_isLink := ⋯, left_mem_of_isLink := ⋯ : Graph α β } =
    { vertexSet := V(G₂), IsLink := G₂.IsLink, edgeSet := E(G₂), isLink_symm := ⋯, eq_or_eq_of_isLink_of_isLink := ⋯,
      edge_mem_iff_exists_isLink := ⋯, left_mem_of_isLink := ⋯ }
⊢ G₁ = G₂

Tactic:
rw [← G₁.mk_eq_self G₁.edge_mem_iff_exists_isLink, ← G₂.mk_eq_self G₂.edge_mem_iff_exists_isLink]

Premises used: Graph.edge_mem_iff_exists_isLink, Graph.mk_eq_self
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
G₁ G₂ : Graph α β
hV : V(G₁) = V(G₂)
h : ∀ (e : β) (x y : α), G₁.IsLink e x y ↔ G₂.IsLink e x y
⊢ { vertexSet := V(G₁), IsLink := G₁.IsLink, edgeSet := E(G₁), isLink_symm := ⋯, eq_or_eq_of_isLink_of_isLink := ⋯,
      edge_mem_iff_exists_isLink := ⋯, left_mem_of_isLink := ⋯ : Graph α β } =
    { vertexSet := V(G₁), IsLink := G₁.IsLink, edgeSet := E(G₁), isLink_symm := ⋯, eq_or_eq_of_isLink_of_isLink := ⋯,
      edge_mem_iff_exists_isLink := ⋯, left_mem_of_isLink := ⋯ }

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
G₁ G₂ : Graph α β
hV : V(G₁) = V(G₂)
h : ∀ (e : β) (x y : α), G₁.IsLink e x y ↔ G₂.IsLink e x y
h₁ : V(G₂) = V(G₁)
h₂ : G₂.IsLink = G₁.IsLink
h₃ : E(G₂) = E(G₁)
⊢ { vertexSet := V(G₁), IsLink := G₁.IsLink, edgeSet := E(G₁), isLink_symm := ⋯, eq_or_eq_of_isLink_of_isLink := ⋯,
      edge_mem_iff_exists_isLink := ⋯, left_mem_of_isLink := ⋯ : Graph α β } =
    { vertexSet := V(G₂), IsLink := G₂.IsLink, edgeSet := E(G₂), isLink_symm := ⋯, eq_or_eq_of_isLink_of_isLink := ⋯,
      edge_mem_iff_exists_isLink := ⋯, left_mem_of_isLink := ⋯ }

Tactic:
convert! rfl using 2

Premises used: rfl
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
G₁ G₂ : Graph α β
hV : V(G₁) = V(G₂)
h : ∀ (e : β) (x y : α), G₁.IsLink e x y ↔ G₂.IsLink e x y
⊢ V(G₂) = V(G₁)

Tactic:
hV.symm

Premises used: Eq.symm
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
G₁ G₂ : Graph α β
hV : V(G₁) = V(G₂)
h : ∀ (e : β) (x y : α), G₁.IsLink e x y ↔ G₂.IsLink e x y
⊢ V(G₂) = V(G₁)

Tactic:
exact hV.symm

Premises used: Eq.symm
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
G₁ G₂ : Graph α β
hV : V(G₁) = V(G₂)
h : ∀ (e : β) (x y : α), G₁.IsLink e x y ↔ G₂.IsLink e x y
⊢ G₂.IsLink = G₁.IsLink

Tactic:
simp [funext_iff, h]

Premises used: funext_iff
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
G₁ G₂ : Graph α β
hV : V(G₁) = V(G₂)
h : ∀ (e : β) (x y : α), G₁.IsLink e x y ↔ G₂.IsLink e x y
⊢ E(G₂) = E(G₁)

Tactic:
simp [edgeSet_eq_setOf_exists_isLink, h]

Premises used: Graph.edgeSet_eq_setOf_exists_isLink
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
G₁ G₂ : Graph α β
hV : V(G₁) = V(G₂)
h : ∀ (e : β) (x : α), G₁.Inc e x ↔ G₂.Inc e x
x : β
x_1 x_2 : α
simp_rw :
  (G₁.Inc x x_1 ∧ G₁.Inc x x_2 ∧ ∀ (z : α), G₁.Inc x z → z = x_1 ∨ z = x_2) ↔
    G₂.Inc x x_1 ∧ G₂.Inc x x_2 ∧ ∀ (z : α), G₂.Inc x z → z = x_1 ∨ z = x_2
⊢ G₁.IsLink x x_1 x_2 ↔ G₂.IsLink x x_1 x_2

Tactic:
simp_rw [isLink_iff_inc, h]

Premises used: Graph.isLink_iff_inc
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x_1 y_1 z u v w : α
e_1 f : β
G_1 H G : Graph α β
vertexSet : Set α
edgeSet : Set β
IsLink : β → α → α → Prop
hvertexSet : V(G) = vertexSet
hedgeSet : E(G) = edgeSet
hIsLink : ∀ (e : β) (x y : α), G.IsLink e x y ↔ IsLink e x y
e : β
he : e ∈ edgeSet
x y : α
simp_rw : G.IsLink e x y → G.IsLink e y x
⊢ IsLink e x y → IsLink e y x

Tactic:
simp_rw [← hIsLink]
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x_1 y_1 z u v w : α
e_1 f : β
G_1 H G : Graph α β
vertexSet : Set α
edgeSet : Set β
IsLink : β → α → α → Prop
hvertexSet : V(G) = vertexSet
hedgeSet : E(G) = edgeSet
hIsLink : ∀ (e : β) (x y : α), G.IsLink e x y ↔ IsLink e x y
e : β
he : e ∈ edgeSet
x y : α
⊢ G.IsLink e x y → G.IsLink e y x

Tactic:
apply G.isLink_symm (hedgeSet ▸ he)

Premises used: Graph.isLink_symm
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x y z u v w : α
e f : β
G_1 H G : Graph α β
vertexSet : Set α
edgeSet : Set β
IsLink : β → α → α → Prop
hvertexSet : V(G) = vertexSet
hedgeSet : E(G) = edgeSet
hIsLink : ∀ (e : β) (x y : α), G.IsLink e x y ↔ IsLink e x y
simp_rw : ∀ ⦃e : β⦄ ⦃x y v w : α⦄, G.IsLink e x y → G.IsLink e v w → x = v ∨ x = w
⊢ ∀ ⦃e : β⦄ ⦃x y v w : α⦄, IsLink e x y → IsLink e v w → x = v ∨ x = w

Tactic:
simp_rw [← hIsLink]
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x y z u v w : α
e f : β
G_1 H G : Graph α β
vertexSet : Set α
edgeSet : Set β
IsLink : β → α → α → Prop
hvertexSet : V(G) = vertexSet
hedgeSet : E(G) = edgeSet
hIsLink : ∀ (e : β) (x y : α), G.IsLink e x y ↔ IsLink e x y
⊢ ∀ ⦃e : β⦄ ⦃x y v w : α⦄, G.IsLink e x y → G.IsLink e v w → x = v ∨ x = w

Tactic:
G.eq_or_eq_of_isLink_of_isLink

Premises used: Graph.eq_or_eq_of_isLink_of_isLink
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x y z u v w : α
e f : β
G_1 H G : Graph α β
vertexSet : Set α
edgeSet : Set β
IsLink : β → α → α → Prop
hvertexSet : V(G) = vertexSet
hedgeSet : E(G) = edgeSet
hIsLink : ∀ (e : β) (x y : α), G.IsLink e x y ↔ IsLink e x y
⊢ ∀ ⦃e : β⦄ ⦃x y v w : α⦄, G.IsLink e x y → G.IsLink e v w → x = v ∨ x = w

Tactic:
exact G.eq_or_eq_of_isLink_of_isLink

Premises used: Graph.eq_or_eq_of_isLink_of_isLink
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x y z u v w : α
e f : β
G_1 H G : Graph α β
vertexSet : Set α
edgeSet : Set β
IsLink : β → α → α → Prop
hvertexSet : V(G) = vertexSet
hedgeSet : E(G) = edgeSet
hIsLink : ∀ (e : β) (x y : α), G.IsLink e x y ↔ IsLink e x y
simp_rw : ∀ (e : β), e ∈ E(G) ↔ ∃ (x : α) (y : α), G.IsLink e x y
⊢ ∀ (e : β), e ∈ edgeSet ↔ ∃ (x : α) (y : α), IsLink e x y

Tactic:
simp_rw [← hIsLink, ← hedgeSet]
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x y z u v w : α
e f : β
G_1 H G : Graph α β
vertexSet : Set α
edgeSet : Set β
IsLink : β → α → α → Prop
hvertexSet : V(G) = vertexSet
hedgeSet : E(G) = edgeSet
hIsLink : ∀ (e : β) (x y : α), G.IsLink e x y ↔ IsLink e x y
⊢ ∀ (e : β), e ∈ E(G) ↔ ∃ (x : α) (y : α), G.IsLink e x y

Tactic:
G.edge_mem_iff_exists_isLink

Premises used: Graph.edge_mem_iff_exists_isLink
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x y z u v w : α
e f : β
G_1 H G : Graph α β
vertexSet : Set α
edgeSet : Set β
IsLink : β → α → α → Prop
hvertexSet : V(G) = vertexSet
hedgeSet : E(G) = edgeSet
hIsLink : ∀ (e : β) (x y : α), G.IsLink e x y ↔ IsLink e x y
⊢ ∀ (e : β), e ∈ E(G) ↔ ∃ (x : α) (y : α), G.IsLink e x y

Tactic:
exact G.edge_mem_iff_exists_isLink

Premises used: Graph.edge_mem_iff_exists_isLink
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x y z u v w : α
e f : β
G_1 H G : Graph α β
vertexSet : Set α
edgeSet : Set β
IsLink : β → α → α → Prop
hvertexSet : V(G) = vertexSet
hedgeSet : E(G) = edgeSet
hIsLink : ∀ (e : β) (x y : α), G.IsLink e x y ↔ IsLink e x y
simp_rw : ∀ ⦃e : β⦄ ⦃x y : α⦄, G.IsLink e x y → x ∈ V(G)
⊢ ∀ ⦃e : β⦄ ⦃x y : α⦄, IsLink e x y → x ∈ vertexSet

Tactic:
simp_rw [← hIsLink, ← hvertexSet]
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x y z u v w : α
e f : β
G_1 H G : Graph α β
vertexSet : Set α
edgeSet : Set β
IsLink : β → α → α → Prop
hvertexSet : V(G) = vertexSet
hedgeSet : E(G) = edgeSet
hIsLink : ∀ (e : β) (x y : α), G.IsLink e x y ↔ IsLink e x y
⊢ ∀ ⦃e : β⦄ ⦃x y : α⦄, G.IsLink e x y → x ∈ V(G)

Tactic:
G.left_mem_of_isLink

Premises used: Graph.left_mem_of_isLink
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x y z u v w : α
e f : β
G_1 H G : Graph α β
vertexSet : Set α
edgeSet : Set β
IsLink : β → α → α → Prop
hvertexSet : V(G) = vertexSet
hedgeSet : E(G) = edgeSet
hIsLink : ∀ (e : β) (x y : α), G.IsLink e x y ↔ IsLink e x y
⊢ ∀ ⦃e : β⦄ ⦃x y : α⦄, G.IsLink e x y → x ∈ V(G)

Tactic:
exact G.left_mem_of_isLink

Premises used: Graph.left_mem_of_isLink
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
V : Set α
E : Set β
IsLink : β → α → α → Prop
hV : V(G) = V
hE : E(G) = E
h_isLink : ∀ (e : β) (x y : α), G.IsLink e x y ↔ IsLink e x y
hV₁ : ∀ (x : α), x ∈ V(G.copy (vertexSet := V) (edgeSet := E) (IsLink := IsLink) hV hE h_isLink) ↔ x ∈ V(G)
h :
  ∀ (e : β) (x y : α),
    (G.copy (vertexSet := V) (edgeSet := E) (IsLink := IsLink) hV hE h_isLink).IsLink e x y ↔ G.IsLink e x y
⊢ G.copy (vertexSet := V) (edgeSet := E) (IsLink := IsLink) hV hE h_isLink = G

Tactic:
ext
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
V : Set α
E : Set β
IsLink : β → α → α → Prop
hV : V(G) = V
hE : E(G) = E
h_isLink : ∀ (e : β) (x y : α), G.IsLink e x y ↔ IsLink e x y
x : α
⊢ x ∈ V(G.copy (vertexSet := V) (edgeSet := E) (IsLink := IsLink) hV hE h_isLink) ↔ x ∈ V(G)

Tactic:
simp_all
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
V : Set α
E : Set β
IsLink : β → α → α → Prop
hV : V(G) = V
hE : E(G) = E
h_isLink : ∀ (e : β) (x y : α), G.IsLink e x y ↔ IsLink e x y
e : β
x y : α
⊢ (G.copy (vertexSet := V) (edgeSet := E) (IsLink := IsLink) hV hE h_isLink).IsLink e x y ↔ G.IsLink e x y

Tactic:
simp_all
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
x : α
e : β
⊢ Membership.mem (γ := Set β) (incidenceSet (G := G) x) e ↔ G.Inc e x

Tactic:
Iff.rfl

Premises used: Set.Mem, Graph.incidenceSet, Graph.Inc, Iff.rfl, setOf
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
x : α
⊢ incidenceSet (G := G) x ⊆ E(G)

Tactic:
fun _ ⟨_, hy⟩ ↦ hy.edge_mem

Premises used: Graph.IsLink.edge_mem, Membership.mem, Set.Subset, Graph.edgeSet, _private.0.Graph.incidenceSet_subset_edgeSet.match_1
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
x : α
e : β
⊢ Membership.mem (γ := Set β) (loopSet (G := G) x) e ↔ G.IsLoopAt e x

Tactic:
Iff.rfl

Premises used: Graph.IsLoopAt, Set.Mem, Iff.rfl, setOf, Graph.loopSet
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
x : α
⊢ Subset.{u_2} (α := Set β) (loopSet (G := G) x) (incidenceSet (G := G) x)

Tactic:
fun _ he ↦ ⟨x, he⟩

Premises used: Set.Mem, Graph.incidenceSet, Graph.Inc, setOf, Set.Subset, Exists.intro
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
e : β
G H : Graph α β
heG : e ∈ E(G)
heH : e ∈ E(H)
h : G.Compatible H
x y : α
⊢ G.IsLink e x y ↔ H.IsLink e x y

Tactic:
h heG heH x y
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
⊢ G.Compatible G

Tactic:
fun _ _ _ _ _ => .rfl

Premises used: Iff.rfl, Graph.Compatible
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
⊢ G.Compatible G

Tactic:
.refl _

Premises used: Graph.Compatible.refl
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
h : G.Compatible H
⊢ H.Compatible G

Tactic:
fun _ heH heG x y => (h heG heH x y).symm

Premises used: Graph.Compatible, Iff.symm
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
hGH : G.Compatible H
heH : e ∈ E(H)
h : G.IsLink e x y
⊢ H.IsLink e x y

Tactic:
(hGH h.edge_mem heH x y).mp h

Premises used: Graph.IsLink.edge_mem, Iff.mp
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
h : Disjoint E(G) E(H)
⊢ G.Compatible H

Tactic:
fun _ heG heH _ _ ↦ h.notMem_of_mem_left heG heH |>.elim

Premises used: False.elim, Graph.Compatible, Disjoint.notMem_of_mem_left
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x : α
e : β
G H : Graph α β
hGH : G.Compatible H
heH : e ∈ E(H)
h : G.Inc e x
obtain : ∀ (y : α) (hy : G.IsLink e x y), H.Inc e x
⊢ H.Inc e x

Tactic:
obtain ⟨y, hy⟩ := h
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x : α
e : β
G H : Graph α β
hGH : G.Compatible H
heH : e ∈ E(H)
y : α
hy : G.IsLink e x y
⊢ H.Inc e x

Tactic:
⟨y, hy.of_compatible hGH heH⟩

Premises used: Graph.Inc, Graph.IsLink.of_compatible, Exists.intro
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x : α
e : β
G H : Graph α β
hGH : G.Compatible H
heH : e ∈ E(H)
y : α
hy : G.IsLink e x y
⊢ H.Inc e x

Tactic:
exact ⟨y, hy.of_compatible hGH heH⟩
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x : α
e : β
G H : Graph α β
hGH : G.Compatible H
heH : e ∈ E(H)
h : G.IsLoopAt e x
⊢ H.IsLoopAt e x

Tactic:
IsLink.of_compatible hGH heH h

Premises used: Graph.IsLoopAt, Graph.IsLink.of_compatible
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x : α
e : β
G H : Graph α β
hGH : G.Compatible H
heH : e ∈ E(H)
h : G.IsNonloopAt e x
obtain : ∀ (y : α) (hne : y ≠ x) (hy : G.IsLink e x y), H.IsNonloopAt e x
⊢ H.IsNonloopAt e x

Tactic:
obtain ⟨y, hne, hy⟩ := h
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x : α
e : β
G H : Graph α β
hGH : G.Compatible H
heH : e ∈ E(H)
y : α
hne : y ≠ x
hy : G.IsLink e x y
⊢ H.IsNonloopAt e x

Tactic:
⟨y, hne, hy.of_compatible hGH heH⟩

Premises used: Graph.IsLink.of_compatible, Graph.IsNonloopAt, And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x : α
e : β
G H : Graph α β
hGH : G.Compatible H
heH : e ∈ E(H)
y : α
hne : y ≠ x
hy : G.IsLink e x y
⊢ H.IsNonloopAt e x

Tactic:
exact ⟨y, hne, hy.of_compatible hGH heH⟩
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β_1 : Type u_2
x y z u v w : α
e f : β_1
G H : Graph α β_1
vertexSet : Set α
β : Type u_3
⊢ ∀ ⦃e : β⦄, Membership.mem (γ := Set β) ∅ e → Symmetric fun (x x_1 : α) ↦ False

Tactic:
simp
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β_1 : Type u_2
x y z u v w : α
e f : β_1
G H : Graph α β_1
vertexSet : Set α
β : Type u_3
⊢ ∀ ⦃e : β⦄ ⦃x y v w : α⦄, False → False → x = v ∨ x = w

Tactic:
simp
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β_1 : Type u_2
x y z u v w : α
e f : β_1
G H : Graph α β_1
vertexSet : Set α
β : Type u_3
⊢ ∀ (e : β), Membership.mem (γ := Set β) ∅ e ↔ ∃ (x : α) (y : α), False

Tactic:
simp
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
h : G = noEdge V(G) β
rw : E(noEdge V(G) β) = ∅
rw₁ rw₂ : Eq.{u_2 + 1} (α := Set β) ∅ ∅
⊢ E(G) = ∅

Tactic:
rw [h, edgeSet_noEdge]

Premises used: Graph.edgeSet_noEdge
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
refine : ∀ (h : E(G) = ∅) (e : β) (x y : α), G.IsLink e x y ↔ (noEdge V(G) β).IsLink e x y
⊢ E(G) = ∅ ↔ G = noEdge V(G) β

Tactic:
refine ⟨fun h ↦ Graph.ext rfl ?_, fun h ↦ by rw [h, edgeSet_noEdge]⟩
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
h : E(G) = ∅
simp : ∀ (e : β) (x y : α), ¬G.IsLink e x y
⊢ ∀ (e : β) (x y : α), G.IsLink e x y ↔ (noEdge V(G) β).IsLink e x y

Tactic:
simp only [noEdge_isLink, iff_false]

Premises used: iff_false, Graph.noEdge_isLink
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
h : E(G) = ∅
⊢ ∀ (e : β) (x y : α), ¬G.IsLink e x y

Tactic:
fun e x y he ↦ ?_

Premises used: Not
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
h : E(G) = ∅
refine : ∀ (e : β) (x y : α) (he : G.IsLink e x y), False
⊢ ∀ (e : β) (x y : α), ¬G.IsLink e x y

Tactic:
refine fun e x y he ↦ ?_
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
h : E(G) = ∅
e : β
x y : α
he : G.IsLink e x y
⊢ Membership.mem (γ := Set β) ∅ e

Tactic:
have := h ▸ he.edge_mem
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
h : E(G) = ∅
e : β
x y : α
he : G.IsLink e x y
this : Membership.mem (γ := Set β) ∅ e
⊢ False

Tactic:
simp at this
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x y z u_1 v_1 w : α
e f : β
G H : Graph α β
vertexSet : Set α
edgeSet_1 : Set β
u v : α
edgeSet : Set β
x_1 : β
h : x_1 ∈ edgeSet
x_2 : α
⊢ ∀ ⦃y : α⦄,
    (fun (x y : α) ↦ x_1 ∈ edgeSet ∧ (x = u ∧ y = v ∨ x = v ∧ y = u)) x_2 y →
      (fun (x y : α) ↦ x_1 ∈ edgeSet ∧ (x = u ∧ y = v ∨ x = v ∧ y = u)) y x_2

Tactic:
aesop
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x y z u_1 v_1 w : α
e f : β
G H : Graph α β
vertexSet : Set α
edgeSet_1 : Set β
u v : α
edgeSet : Set β
⊢ ∀ ⦃e : β⦄ ⦃x y v_2 w : α⦄,
    e ∈ edgeSet ∧ (x = u ∧ y = v ∨ x = v ∧ y = u) → e ∈ edgeSet ∧ (v_2 = u ∧ w = v ∨ v_2 = v ∧ w = u) → x = v_2 ∨ x = w

Tactic:
aesop
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x y z u_1 v_1 w : α
e f : β
G H : Graph α β
vertexSet : Set α
edgeSet_1 : Set β
u v : α
edgeSet : Set β
⊢ ∀ (e : β), e ∈ edgeSet ↔ ∃ (x : α) (y : α), e ∈ edgeSet ∧ (x = u ∧ y = v ∨ x = v ∧ y = u)

Tactic:
aesop
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x u v : α
e : β
edgeSet : Set β
simp : e ∈ edgeSet → ((∃ (x_1 : α), x = u ∧ x_1 = v ∨ x = v ∧ x_1 = u) ↔ x = u ∨ x = v)
⊢ (banana u v edgeSet).Inc e x ↔ e ∈ edgeSet ∧ (x = u ∨ x = v)

Tactic:
simp only [Inc, banana_isLink, exists_and_left, and_congr_right_iff]

Premises used: Graph.Inc, Graph.banana_isLink, exists_and_left, and_congr_right_iff
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x u v : α
e : β
edgeSet : Set β
⊢ e ∈ edgeSet → ((∃ (x_1 : α), x = u ∧ x_1 = v ∨ x = v ∧ x_1 = u) ↔ x = u ∨ x = v)

Tactic:
aesop
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
u v : α
edgeSet : Set β
⊢ ∀ (e : β) (x : α), (banana u v edgeSet).Inc e x ↔ (banana v u edgeSet).Inc e x

Tactic:
simp [or_comm]

Premises used: or_comm
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x u v : α
e : β
edgeSet : Set β
simp_rw :
  (e ∈ edgeSet ∧ (x = u ∨ x = v)) ∧ ¬(e ∈ edgeSet ∧ (x = u ∧ x = v ∨ x = v ∧ x = u)) ↔
    e ∈ edgeSet ∧ (x = u ∨ x = v) ∧ u ≠ v
⊢ (banana u v edgeSet).IsNonloopAt e x ↔ e ∈ edgeSet ∧ (x = u ∨ x = v) ∧ u ≠ v

Tactic:
simp_rw [isNonloopAt_iff_inc_not_isLoopAt, ← isLink_self_iff, banana_isLink, banana_inc]

Premises used: Graph.banana_inc, Graph.banana_isLink, Graph.isNonloopAt_iff_inc_not_isLoopAt, Graph.isLink_self_iff
-- Module: Mathlib.Combinatorics.Graph.Basic
Goal:
α : Type u_1
β : Type u_2
x u v : α
e : β
edgeSet : Set β
⊢ (e ∈ edgeSet ∧ (x = u ∨ x = v)) ∧ ¬(e ∈ edgeSet ∧ (x = u ∧ x = v ∨ x = v ∧ x = u)) ↔
    e ∈ edgeSet ∧ (x = u ∨ x = v) ∧ u ≠ v

Tactic:
aesop