awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤ G
e : β
he : e ∈ E(H)
x : α
⊢ H.Inc e x ↔ G.Inc e x

Tactic:
hHG.inc_congr he

Premises used: Graph.IsSubgraph.inc_congr
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤ G
e : β
he : e ∈ E(H)
x : α
⊢ H.Inc e x ↔ G.Inc e x

Tactic:
exact hHG.inc_congr he

Premises used: Graph.IsSubgraph.inc_congr
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
x : α
e : β
G H : Graph α β
hHG : H ≤ G
h : H.IsLoopAt e x
⊢ G.IsLoopAt e x

Tactic:
IsLink.mono hHG h

Premises used: Graph.IsLink.mono, Graph.IsLoopAt
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
x : α
e : β
G H : Graph α β
hHG : H ≤ G
he : e ∈ E(H)
rw rw₁ : G.IsLink e x x ↔ G.IsLink e x x
⊢ H.IsLink e x x ↔ G.IsLink e x x

Tactic:
rw [hHG.isLink_iff he]

Premises used: Graph.IsSubgraph.isLink_iff
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤ G
e : β
he : e ∈ E(H)
h : ∀ (x : α), H.IsLoopAt e x ↔ G.IsLoopAt e x
⊢ H.IsLoopAt e = G.IsLoopAt e

Tactic:
ext x
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤ G
e : β
he : e ∈ E(H)
x : α
⊢ H.IsLoopAt e x ↔ G.IsLoopAt e x

Tactic:
hHG.isLoopAt_congr he

Premises used: Graph.IsSubgraph.isLoopAt_congr
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤ G
e : β
he : e ∈ E(H)
x : α
⊢ H.IsLoopAt e x ↔ G.IsLoopAt e x

Tactic:
exact hHG.isLoopAt_congr he

Premises used: Graph.IsSubgraph.isLoopAt_congr
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
x : α
e : β
G H : Graph α β
hHG : H ≤ G
h : H.IsNonloopAt e x
obtain : ∀ (y : α) (hxy : y ≠ x) (he : H.IsLink e x y), G.IsNonloopAt e x
⊢ G.IsNonloopAt e x

Tactic:
obtain ⟨y, hxy, he⟩ := h
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
x : α
e : β
G H : Graph α β
hHG : H ≤ G
y : α
hxy : y ≠ x
he : H.IsLink e x y
⊢ G.IsNonloopAt e x

Tactic:
⟨y, hxy, he.mono hHG⟩

Premises used: Graph.IsLink.mono, Graph.IsNonloopAt, And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
x : α
e : β
G H : Graph α β
hHG : H ≤ G
y : α
hxy : y ≠ x
he : H.IsLink e x y
⊢ G.IsNonloopAt e x

Tactic:
exact ⟨y, hxy, he.mono hHG⟩
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤ G
e : β
he : e ∈ E(H)
h : ∀ (x : α), H.IsNonloopAt e x ↔ G.IsNonloopAt e x
⊢ H.IsNonloopAt e = G.IsNonloopAt e

Tactic:
ext x
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤ G
e : β
he : e ∈ E(H)
x : α
⊢ H.IsNonloopAt e x ↔ G.IsNonloopAt e x

Tactic:
hHG.isNonloopAt_congr he

Premises used: Graph.IsSubgraph.isNonloopAt_congr
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤ G
e : β
he : e ∈ E(H)
x : α
⊢ H.IsNonloopAt e x ↔ G.IsNonloopAt e x

Tactic:
exact hHG.isNonloopAt_congr he

Premises used: Graph.IsSubgraph.isNonloopAt_congr
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
x y : α
G H : Graph α β
hHG : H ≤ G
h : H.Adj x y
⊢ G.Adj x y

Tactic:
(h.choose_spec.mono hHG).adj

Premises used: Graph.IsLink.mono, Exists.choose_spec, Graph.IsLink.adj
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
⊢ G ≤ H ↔ G.Compatible H ∧ V(G) ⊆ V(H) ∧ E(G) ⊆ E(H)

Tactic:
⟨fun h ↦ ⟨.of_le h, h.1, h.edgeSet_mono⟩, fun ⟨h, hV, hE⟩ ↦
    ⟨hV, fun _ _ _ hxy ↦ h hxy.edge_mem (hE hxy.edge_mem) .. |>.mp hxy⟩⟩

Premises used: Graph.IsLink.edge_mem, Graph.IsSubgraph.mk, Graph.IsSubgraph.edgeSet_mono, LE.le, _private.0.Graph.le_iff_compatible_subset_subset.match_1, Graph.Compatible.of_le, And.intro, Iff.intro, Iff.mp, Graph.IsSubgraph.vertexSet_mono
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
H₁ H₂ : Graph α β
hH : H₁.Compatible H₂
mp : H₁.Compatible H₂ ∧ V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂) → V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂)
mpr : V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂) → H₁.Compatible H₂ ∧ V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂)
mp₁ mp₂ : H₁.Compatible H₂ → V(H₁) ⊆ V(H₂) → E(H₁) ⊆ E(H₂) → V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂)
mp₃ : H₁.Compatible H₂ → V(H₁) ⊆ V(H₂) → E(H₁) ⊆ E(H₂) → V(H₁) ⊆ V(H₂)
mp₄ : H₁.Compatible H₂ → V(H₁) ⊆ V(H₂) → E(H₁) ⊆ E(H₂) → E(H₁) ⊆ E(H₂)
mpr₁ mpr₂ : V(H₁) ⊆ V(H₂) → E(H₁) ⊆ E(H₂) → H₁.Compatible H₂ ∧ V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂)
mpr₃ : V(H₁) ⊆ V(H₂) → E(H₁) ⊆ E(H₂) → H₁.Compatible H₂
mpr₄ : V(H₁) ⊆ V(H₂) → E(H₁) ⊆ E(H₂) → V(H₁) ⊆ V(H₂)
mpr₅ : V(H₁) ⊆ V(H₂) → E(H₁) ⊆ E(H₂) → E(H₁) ⊆ E(H₂)
⊢ H₁.Compatible H₂ ∧ V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂) ↔ V(H₁) ⊆ V(H₂) ∧ E(H₁) ⊆ E(H₂)

Tactic:
tauto
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
H₁ H₂ : Graph α β
hV : V(H₁) = V(H₂)
hE : E(H₁) = E(H₂)
h : H₁.Compatible H₂
⊢ H₁ = H₂

Tactic:
(h.le_iff.mpr ⟨hV.subset, hE.subset⟩).antisymm <| h.symm.le_iff.mpr ⟨hV.superset, hE.superset⟩

Premises used: Iff.mpr, LE.le.antisymm, Eq.subset, Graph.Compatible.le_iff, And.intro, Graph.Compatible.symm, Eq.superset
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
hGH : G < H
⊢ G ≤ H ∧ G ≠ H

Tactic:
rw [lt_iff_le_and_ne] at hGH

Premises used: lt_iff_le_and_ne
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
hGH : G ≤ H ∧ G ≠ H
simp : ¬V(G) = V(H) ∨ ¬E(G) = E(H)
⊢ V(G) ⊂ V(H) ∨ E(G) ⊂ E(H)

Tactic:
simp only [ssubset_iff_subset_ne, hGH.1.vertexSet_mono, ne_eq, true_and, hGH.1.edgeSet_mono]

Premises used: Graph.IsSubgraph.edgeSet_mono, ne_eq, And.left, Graph.IsSubgraph.vertexSet_mono, true_and, ssubset_iff_subset_ne
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
hGH : G ≤ H ∧ G ≠ H
by_contra! : ∀ (heq : V(G) = V(H) ∧ E(G) = E(H)), False
⊢ ¬V(G) = V(H) ∨ ¬E(G) = E(H)

Tactic:
by_contra! heq
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
hGH : G ≤ H ∧ G ≠ H
heq : V(G) = V(H) ∧ E(G) = E(H)
⊢ False

Tactic:
hGH.2 <| hGH.1.compatible.ext heq.1 heq.2

Premises used: Graph.IsSubgraph.compatible, Graph.Compatible.ext, And.right, And.left
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
hGH : G ≤ H ∧ G ≠ H
heq : V(G) = V(H) ∧ E(G) = E(H)
⊢ False

Tactic:
exact hGH.2 <| hGH.1.compatible.ext heq.1 heq.2

Premises used: Graph.IsSubgraph.compatible, Graph.Compatible.ext, And.right, And.left
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
X : Set α
h : X ⊆ V(G)
⊢ ∀ ⦃e : β⦄ ⦃x y : α⦄, (noEdge X β).IsLink e x y → G.IsLink e x y

Tactic:
simp
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
X : Set α
h : V(G) ⊆ X ∧ E(G) = ∅
e : β
x y : α
he : G.IsLink e x y
⊢ (noEdge X β).IsLink e x y

Tactic:
simpa [h] using he.edge_mem

Premises used: Graph.IsLink.edge_mem
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G G₁ G₂ : Graph α β
h₁ : G ≤s G₁
h₂ : G₁ ≤s G₂
⊢ G ≤s G₂

Tactic:
⟨h₁.le.trans h₂.le, h₁.vertexSet_eq.trans h₂.vertexSet_eq⟩

Premises used: Graph.IsSubgraph.trans, Graph.IsSpanningSubgraph.vertexSet_eq, Graph.IsSpanningSubgraph.mk, Graph.IsSpanningSubgraph.le, Eq.trans
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
⊢ G ≤s G

Tactic:
refl G

Premises used: refl
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
hE : E(H) = E(G)
h : H ≤s G
⊢ H = G

Tactic:
h.compatible.ext h.vertexSet_eq hE

Premises used: Graph.IsSubgraph.compatible, Graph.Compatible.ext, Graph.IsSpanningSubgraph.vertexSet_eq, Graph.IsSpanningSubgraph.le
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G G₁ G₂ : Graph α β
h₁ : G ≤i G₁
h₂ : G₁ ≤i G₂
⊢ G ≤i G₂

Tactic:
⟨h₁.le.trans h₂.le, fun _ _ _ h hx hy ↦ h₁.isLink_of_mem_mem
    (h₂.isLink_of_mem_mem h (h₁.vertexSet_mono hx) (h₁.vertexSet_mono hy)) hx hy⟩

Premises used: Graph.IsInducedSubgraph.mk, Graph.IsInducedSubgraph.le, Graph.IsSubgraph.trans, Graph.IsInducedSubgraph.isLink_of_mem_mem, Graph.IsSubgraph.vertexSet_mono
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
x y z u v w : α
e f : β
G_1 G₁ G₂ H H₁ H₂ K : Graph α β
F F₁ F₂ : Set β
X Y : Set α
G : Graph α β
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ tauto₈ :
  ∀ ⦃e : β⦄ ⦃x y : α⦄, G.IsLink e x y → x ∈ V(G) → y ∈ V(G) → G.IsLink e x y
⊢ ∀ ⦃e : β⦄ ⦃x y : α⦄, G.IsLink e x y → x ∈ V(G) → y ∈ V(G) → G.IsLink e x y

Tactic:
tauto
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
⊢ G ≤i G

Tactic:
refl G

Premises used: refl
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
hx : x ∈ V(H)
hy : y ∈ V(H)
h : H ≤i G
⊢ H.IsLink e x y ↔ G.IsLink e x y

Tactic:
⟨(·.mono h.le), fun hxy ↦ h.isLink_of_mem_mem hxy hx hy⟩

Premises used: Graph.IsLink.mono, Graph.IsInducedSubgraph.le, Iff.intro, Graph.IsInducedSubgraph.isLink_of_mem_mem
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
x y : α
G H : Graph α β
hx : x ∈ V(H)
hy : y ∈ V(H)
h : H ≤i G
⊢ H.Adj x y ↔ G.Adj x y

Tactic:
⟨(·.mono h.le), fun ⟨_, hxy⟩ ↦ (h.isLink_of_mem_mem hxy hx hy).adj⟩

Premises used: Graph.Adj.mono, Graph.IsLink.adj, Graph.Adj, Graph.IsInducedSubgraph.le, Iff.intro, Graph.IsInducedSubgraph.isLink_of_mem_mem, _private.0.Graph.IsInducedSubgraph.adj_congr.match_1
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G H K : Graph α β
h' : K ≤ G
hsu : V(K) ⊆ V(H)
h : H ≤i G
⊢ K ≤ H

Tactic:
(Compatible.of_le_le h' h.le).le_iff.mpr ⟨hsu, fun e he ↦ ?_⟩

Premises used: Iff.mpr, Graph.Compatible.le_iff, And.intro, Graph.IsInducedSubgraph.le, Graph.Compatible.of_le_le
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G H K : Graph α β
h' : K ≤ G
hsu : V(K) ⊆ V(H)
h : H ≤i G
refine : ∀ (e : β) (he : e ∈ E(K)), e ∈ E(H)
⊢ K ≤ H

Tactic:
refine (Compatible.of_le_le h' h.le).le_iff.mpr ⟨hsu, fun e he ↦ ?_⟩

Premises used: Iff.mpr, Graph.Compatible.le_iff, And.intro, Graph.IsInducedSubgraph.le, Graph.Compatible.of_le_le
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G H K : Graph α β
h' : K ≤ G
hsu : V(K) ⊆ V(H)
h : H ≤i G
e : β
he : e ∈ E(K)
obtain : ∀ (u v : α) (huv : K.IsLink e u v), e ∈ E(H)
⊢ e ∈ E(H)

Tactic:
obtain ⟨u, v, huv⟩ := K.exists_isLink_of_mem_edgeSet he

Premises used: Graph.exists_isLink_of_mem_edgeSet
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G H K : Graph α β
h' : K ≤ G
hsu : V(K) ⊆ V(H)
h : H ≤i G
e : β
he : e ∈ E(K)
u v : α
huv : K.IsLink e u v
⊢ e ∈ E(H)

Tactic:
h.2 (huv.mono h') (hsu huv.left_mem) (hsu huv.right_mem) |>.edge_mem

Premises used: Graph.IsLink.edge_mem, Graph.IsLink.mono, Graph.IsLink.right_mem, Graph.IsLink.left_mem, Graph.IsInducedSubgraph.isLink_of_mem_mem
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G H K : Graph α β
h' : K ≤ G
hsu : V(K) ⊆ V(H)
h : H ≤i G
e : β
he : e ∈ E(K)
u v : α
huv : K.IsLink e u v
⊢ e ∈ E(H)

Tactic:
exact h.2 (huv.mono h') (hsu huv.left_mem) (hsu huv.right_mem) |>.edge_mem

Premises used: Graph.IsLink.edge_mem, Graph.IsLink.mono, Graph.IsLink.right_mem, Graph.IsLink.left_mem, Graph.IsInducedSubgraph.isLink_of_mem_mem
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
hV : V(H) = V(G)
h : H ≤i G
e : β
he : e ∈ E(G)
obtain : ∀ (w w_1 : α) (hxy : G.IsLink e w w_1), e ∈ E(H)
⊢ e ∈ E(H)

Tactic:
obtain ⟨_, _, hxy⟩ := G.exists_isLink_of_mem_edgeSet he

Premises used: Graph.exists_isLink_of_mem_edgeSet
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
hV : V(H) = V(G)
h : H ≤i G
e : β
he : e ∈ E(G)
w w_1 : α
hxy : G.IsLink e w w_1
⊢ e ∈ E(H)

Tactic:
h.isLink_of_mem_mem hxy (hV ▸ hxy.left_mem) (hV ▸ hxy.right_mem) |>.edge_mem

Premises used: Graph.IsLink.edge_mem, Graph.IsLink.right_mem, Eq.rec, Graph.IsLink.left_mem, Graph.IsInducedSubgraph.isLink_of_mem_mem, Eq.symm
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
hV : V(H) = V(G)
h : H ≤i G
e : β
he : e ∈ E(G)
w w_1 : α
hxy : G.IsLink e w w_1
⊢ e ∈ E(H)

Tactic:
exact h.isLink_of_mem_mem hxy (hV ▸ hxy.left_mem) (hV ▸ hxy.right_mem) |>.edge_mem

Premises used: Graph.IsLink.edge_mem, Graph.IsLink.right_mem, Eq.rec, Graph.IsLink.left_mem, Graph.IsInducedSubgraph.isLink_of_mem_mem, Eq.symm
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤ G
contrapose! : H ≤i G ↔ ∀ (e : β) (x y : α) (_ : G.IsLink e x y) (_ : x ∈ V(H)) (_ : y ∈ V(H)), e ∈ E(H)
⊢ ¬H ≤i G ↔ ∃ (e : β) (x : α) (y : α), G.IsLink e x y ∧ x ∈ V(H) ∧ y ∈ V(H) ∧ e ∉ E(H)

Tactic:
contrapose!
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤ G
symm : (∀ (e : β) (x y : α) (_ : G.IsLink e x y) (_ : x ∈ V(H)) (_ : y ∈ V(H)), e ∈ E(H)) ↔ H ≤i G
⊢ H ≤i G ↔ ∀ (e : β) (x y : α) (_ : G.IsLink e x y) (_ : x ∈ V(H)) (_ : y ∈ V(H)), e ∈ E(H)

Tactic:
symm
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤ G
⊢ (∀ (e : β) (x y : α) (_ : G.IsLink e x y) (_ : x ∈ V(H)) (_ : y ∈ V(H)), e ∈ E(H)) ↔ H ≤i G

Tactic:
⟨fun hnind ↦ ⟨hHG, fun e x y hxy hx hy => hxy.anti_of_mem hHG (hnind e x y hxy hx hy)⟩,
    fun hind _ _ _ hexy hx hy ↦ hind.isLink_of_mem_mem hexy hx hy |>.edge_mem⟩

Premises used: Graph.IsLink.edge_mem, Graph.IsInducedSubgraph.mk, _private.0.Graph.IsLink.anti_of_mem, Iff.intro, Graph.IsInducedSubgraph.isLink_of_mem_mem
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G H : Graph α β
hHG : H ≤ G
⊢ (∀ (e : β) (x y : α) (_ : G.IsLink e x y) (_ : x ∈ V(H)) (_ : y ∈ V(H)), e ∈ E(H)) ↔ H ≤i G

Tactic:
exact ⟨fun hnind ↦ ⟨hHG, fun e x y hxy hx hy => hxy.anti_of_mem hHG (hnind e x y hxy hx hy)⟩,
    fun hind _ _ _ hexy hx hy ↦ hind.isLink_of_mem_mem hexy hx hy |>.edge_mem⟩
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G G₁ G₂ : Graph α β
h₁ : G ≤c G₁
h₂ : G₁ ≤c G₂
⊢ G ≤c G₂

Tactic:
mk' (h₁.le.trans h₂.le) fun _ _ h hx ↦ h₁.closed (h.of_compatible h₂.compatible'
    (h₂.closed h (h₁.vertexSet_mono hx))) hx

Premises used: Graph.IsClosedSubgraph.mk', Graph.IsClosedSubgraph.isInducedSubgraph, Graph.Inc.of_compatible, Graph.IsSubgraph.compatible', Graph.IsClosedSubgraph.closed, Graph.IsInducedSubgraph.le, Graph.IsSubgraph.trans, Graph.IsSubgraph.vertexSet_mono
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
G : Graph α β
⊢ G ≤c G

Tactic:
refl G

Premises used: refl
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
x : α
e : β
G H : Graph α β
hx : x ∈ V(H)
hHG : H ≤c G
⊢ H.Inc e x ↔ G.Inc e x

Tactic:
⟨(·.mono hHG.le), fun he ↦ he.of_compatible hHG.compatible' (hHG.closed he hx)⟩

Premises used: Graph.IsClosedSubgraph.isInducedSubgraph, Graph.Inc.of_compatible, Graph.Inc.mono, Graph.IsSubgraph.compatible', Graph.IsClosedSubgraph.closed, Graph.IsInducedSubgraph.le, Iff.intro
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
hx : x ∈ V(H)
hHG : H ≤c G
⊢ H.IsLink e x y ↔ G.IsLink e x y

Tactic:
⟨(·.mono hHG.le), fun h ↦ h.anti_of_mem hHG.le ((hHG.inc_congr hx).mpr h.inc_left).edge_mem⟩

Premises used: Iff.mpr, Graph.IsLink.mono, Graph.IsLink.inc_left, _private.0.Graph.IsLink.anti_of_mem, Graph.IsClosedSubgraph.isInducedSubgraph, Graph.IsClosedSubgraph.inc_congr, Graph.IsInducedSubgraph.le, Iff.intro, Graph.Inc.edge_mem
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
he : G.IsLink e x y
hHG : H ≤c G
⊢ x ∈ V(H) ↔ y ∈ V(H)

Tactic:
⟨fun hin ↦ ?_, fun hin ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
he : G.IsLink e x y
hHG : H ≤c G
refine_1 : ∀ (hin : x ∈ V(H)), y ∈ V(H)
refine_2 : ∀ (hin : y ∈ V(H)), x ∈ V(H)
⊢ x ∈ V(H) ↔ y ∈ V(H)

Tactic:
refine ⟨fun hin ↦ ?_, fun hin ↦ ?_⟩
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
he : G.IsLink e x y
hHG : H ≤c G
hin : y ∈ V(H)
⊢ G.IsLink e y x

Tactic:
rw [isLink_comm] at he

Premises used: Graph.isLink_comm
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
he : G.IsLink e x y
hHG : H ≤c G
hin : y ∈ V(H)
he₁ : G.IsLink e y x
⊢ H ≤c G

Tactic:
rw [isLink_comm] at he

Premises used: Graph.isLink_comm
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
he : G.IsLink e x y
hHG : H ≤c G
hin : y ∈ V(H)
he₁ : G.IsLink e y x
hHG₁ : H ≤c G
⊢ y ∈ V(H)

Tactic:
rw [isLink_comm] at he

Premises used: Graph.isLink_comm
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
he : G.IsLink e x y
hHG : H ≤c G
hin : y ∈ V(H)
⊢ G.IsLink e y x

Tactic:
on_goal 2 => rw [isLink_comm] at he

Premises used: Graph.isLink_comm
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
he : G.IsLink e x y
hHG : H ≤c G
hin : y ∈ V(H)
he₁ : G.IsLink e y x
⊢ H ≤c G

Tactic:
on_goal 2 => rw [isLink_comm] at he

Premises used: Graph.isLink_comm
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
he : G.IsLink e x y
hHG : H ≤c G
hin : y ∈ V(H)
he₁ : G.IsLink e y x
hHG₁ : H ≤c G
⊢ y ∈ V(H)

Tactic:
on_goal 2 => rw [isLink_comm] at he

Premises used: Graph.isLink_comm
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
he : G.IsLink e x y
hHG : H ≤c G
hin : x ∈ V(H)
⊢ H.IsLink e x y

Tactic:
rw [← hHG.isLink_congr hin] at he

Premises used: Graph.IsClosedSubgraph.isLink_congr
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
he : G.IsLink e x y
hHG : H ≤c G
hin : x ∈ V(H)
he₁ : H.IsLink e x y
⊢ H ≤c G

Tactic:
rw [← hHG.isLink_congr hin] at he

Premises used: Graph.IsClosedSubgraph.isLink_congr
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
he : G.IsLink e x y
hHG : H ≤c G
hin : x ∈ V(H)
he₁ : H.IsLink e x y
hHG₁ : H ≤c G
⊢ x ∈ V(H)

Tactic:
rw [← hHG.isLink_congr hin] at he

Premises used: Graph.IsClosedSubgraph.isLink_congr
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
he : H.IsLink e x y
hHG : H ≤c G
hin : x ∈ V(H)
⊢ y ∈ V(H)

Tactic:
he.right_mem

Premises used: Graph.IsLink.right_mem
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
he : H.IsLink e x y
hHG : H ≤c G
hin : x ∈ V(H)
⊢ y ∈ V(H)

Tactic:
exact he.right_mem

Premises used: Graph.IsLink.right_mem
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
he : G.IsLink e y x
hHG : H ≤c G
hin : y ∈ V(H)
⊢ H.IsLink e y x

Tactic:
rw [← hHG.isLink_congr hin] at he

Premises used: Graph.IsClosedSubgraph.isLink_congr
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
he : G.IsLink e y x
hHG : H ≤c G
hin : y ∈ V(H)
he₁ : H.IsLink e y x
⊢ H ≤c G

Tactic:
rw [← hHG.isLink_congr hin] at he

Premises used: Graph.IsClosedSubgraph.isLink_congr
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
he : G.IsLink e y x
hHG : H ≤c G
hin : y ∈ V(H)
he₁ : H.IsLink e y x
hHG₁ : H ≤c G
⊢ y ∈ V(H)

Tactic:
rw [← hHG.isLink_congr hin] at he

Premises used: Graph.IsClosedSubgraph.isLink_congr
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
he : H.IsLink e y x
hHG : H ≤c G
hin : y ∈ V(H)
⊢ x ∈ V(H)

Tactic:
he.right_mem

Premises used: Graph.IsLink.right_mem
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
he : H.IsLink e y x
hHG : H ≤c G
hin : y ∈ V(H)
⊢ x ∈ V(H)

Tactic:
exact he.right_mem

Premises used: Graph.IsLink.right_mem
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
he : G.IsLink e x y
hHG : H ≤c G
⊢ x ∈ V(H)

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
he : G.IsLink e x y
hHG : H ≤c G
⊢ y ∈ V(H)

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
he : G.IsLink e x y
hHG : H ≤c G
⊢ ∀ (a : x ∈ V(H)), y ∈ V(H)

Tactic:
1 → 2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
he : G.IsLink e x y
hHG : H ≤c G
⊢ ∀ (a : x ∈ V(H)), y ∈ V(H)

Tactic:
tfae_have 1 → 2 := (hHG.mem_iff_of_isLink he).mp

Premises used: Iff.mp, Graph.IsClosedSubgraph.mem_iff_of_isLink
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
he : G.IsLink e x y
hHG : H ≤c G
tfae_1_to_2 : ∀ (a : x ∈ V(H)), y ∈ V(H)
⊢ y ∈ V(H)

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
he : G.IsLink e x y
hHG : H ≤c G
tfae_1_to_2 : ∀ (a : x ∈ V(H)), y ∈ V(H)
⊢ e ∈ E(H)

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
he : G.IsLink e x y
hHG : H ≤c G
tfae_1_to_2 : ∀ (a : x ∈ V(H)), y ∈ V(H)
⊢ ∀ (a : y ∈ V(H)), e ∈ E(H)

Tactic:
2 → 3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
he : G.IsLink e x y
hHG : H ≤c G
tfae_1_to_2 : ∀ (a : x ∈ V(H)), y ∈ V(H)
⊢ ∀ (a : y ∈ V(H)), e ∈ E(H)

Tactic:
tfae_have 2 → 3 := (hHG.isLink_congr · |>.mpr he.symm |>.edge_mem)

Premises used: Graph.IsLink.edge_mem, Iff.mpr, Graph.IsClosedSubgraph.isLink_congr, Graph.IsLink.symm
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
he : G.IsLink e x y
hHG : H ≤c G
tfae_1_to_2 : ∀ (a : x ∈ V(H)), y ∈ V(H)
tfae_2_to_3 : ∀ (a : y ∈ V(H)), e ∈ E(H)
⊢ e ∈ E(H)

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
he : G.IsLink e x y
hHG : H ≤c G
tfae_1_to_2 : ∀ (a : x ∈ V(H)), y ∈ V(H)
tfae_2_to_3 : ∀ (a : y ∈ V(H)), e ∈ E(H)
⊢ x ∈ V(H)

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Combinatorics.Graph.Subgraph
Goal:
α : Type u_1
β : Type u_2
x y : α
e : β
G H : Graph α β
he : G.IsLink e x y
hHG : H ≤c G
tfae_1_to_2 : ∀ (a : x ∈ V(H)), y ∈ V(H)
tfae_2_to_3 : ∀ (a : y ∈ V(H)), e ∈ E(H)
⊢ ∀ (a : e ∈ E(H)), x ∈ V(H)

Tactic:
3 → 1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false