awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G₁ G₂ : G.Subgraph
h :
  Eq.{u + 1} (α := Set V × SimpleGraph V) ((fun (G' : G.Subgraph) ↦ (G'.verts, G'.spanningCoe)) G₁)
    ((fun (G' : G.Subgraph) ↦ (G'.verts, G'.spanningCoe)) G₂)
⊢ Eq.{u + 1} (α := Set V) ((fun (G' : G.Subgraph) ↦ (G'.verts, G'.spanningCoe)) G₁).1
      ((fun (G' : G.Subgraph) ↦ (G'.verts, G'.spanningCoe)) G₂).1 ∧
    Eq.{u + 1} (α := SimpleGraph V) ((fun (G' : G.Subgraph) ↦ (G'.verts, G'.spanningCoe)) G₁).2
      ((fun (G' : G.Subgraph) ↦ (G'.verts, G'.spanningCoe)) G₂).2

Tactic:
rw [Prod.ext_iff] at h

Premises used: Prod.ext_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G₁ G₂ : G.Subgraph
h :
  Eq.{u + 1} (α := Set V) ((fun (G' : G.Subgraph) ↦ (G'.verts, G'.spanningCoe)) G₁).1
      ((fun (G' : G.Subgraph) ↦ (G'.verts, G'.spanningCoe)) G₂).1 ∧
    Eq.{u + 1} (α := SimpleGraph V) ((fun (G' : G.Subgraph) ↦ (G'.verts, G'.spanningCoe)) G₁).2
      ((fun (G' : G.Subgraph) ↦ (G'.verts, G'.spanningCoe)) G₂).2
⊢ G₁ = G₂

Tactic:
Subgraph.ext h.1 (spanningCoe_inj.1 h.2)

Premises used: SimpleGraph.Subgraph.spanningCoe_inj, And.right, And.left, SimpleGraph.Subgraph.ext, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G₁ G₂ : G.Subgraph
h :
  Eq.{u + 1} (α := Set V) ((fun (G' : G.Subgraph) ↦ (G'.verts, G'.spanningCoe)) G₁).1
      ((fun (G' : G.Subgraph) ↦ (G'.verts, G'.spanningCoe)) G₂).1 ∧
    Eq.{u + 1} (α := SimpleGraph V) ((fun (G' : G.Subgraph) ↦ (G'.verts, G'.spanningCoe)) G₁).2
      ((fun (G' : G.Subgraph) ↦ (G'.verts, G'.spanningCoe)) G₂).2
⊢ G₁ = G₂

Tactic:
exact Subgraph.ext h.1 (spanningCoe_inj.1 h.2)

Premises used: SimpleGraph.Subgraph.spanningCoe_inj, And.right, And.left, SimpleGraph.Subgraph.ext, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : G.Subgraph
a b : V
ι_1 : Type u
κ : ι_1 → Type u
f : (a : ι_1) → κ a → G.Subgraph
⊢ Eq.{u + 1} (α := Set V) (verts (G := G) (⨅ (a : ι_1), ⨆ (b : κ a), f a b))
    (verts (G := G) (⨆ (g : (a : ι_1) → κ a), ⨅ (a : ι_1), f a (g a)))

Tactic:
simpa using iInf_iSup_eq

Premises used: iInf_iSup_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : G.Subgraph
a b : V
ι_1 : Type u
κ : ι_1 → Type u
f : (a : ι_1) → κ a → G.Subgraph
h :
  ∀ (x x_1 : V),
    Adj (G := G) (⨅ (a : ι_1), ⨆ (b : κ a), f a b) x x_1 ↔
      Adj (G := G) (⨆ (g : (a : ι_1) → κ a), ⨅ (a : ι_1), f a (g a)) x x_1
⊢ Eq.{u + 1} (α := V → V → Prop) (Adj (G := G) (⨅ (a : ι_1), ⨆ (b : κ a), f a b))
    (Adj (G := G) (⨆ (g : (a : ι_1) → κ a), ⨅ (a : ι_1), f a (g a)))

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : G.Subgraph
a b : V
ι_1 : Type u
κ : ι_1 → Type u
f : (a : ι_1) → κ a → G.Subgraph
x x_1 : V
⊢ Adj (G := G) (⨅ (a : ι_1), ⨆ (b : κ a), f a b) x x_1 ↔
    Adj (G := G) (⨆ (g : (a : ι_1) → κ a), ⨅ (a : ι_1), f a (g a)) x x_1

Tactic:
simp [Classical.skolem]

Premises used: Classical.skolem
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
h : H ≤ H'
⊢ H.verts ⊆ H'.verts

Tactic:
h.1

Premises used: And.left
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
⊢ Monotone.{u, u} (α := G.Subgraph) verts

Tactic:
fun _ _ h ↦ h.1

Premises used: Monotone, And.left
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
v : V
⊢ (H ⊔ H').neighborSet v = H.neighborSet v ∪ H'.neighborSet v

Tactic:
rfl

Premises used: Set.union, Set.Mem, setOf, SimpleGraph.Subgraph.neighborSet, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
v : V
⊢ (H ⊓ H').neighborSet v = H.neighborSet v ∩ H'.neighborSet v

Tactic:
rfl

Premises used: Set.Mem, setOf, SimpleGraph.Subgraph.neighborSet, Set.inter, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v : V
⊢ neighborSet (G := G) ⊤ v = G.neighborSet v

Tactic:
rfl

Premises used: setOf, SimpleGraph.neighborSet, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
v : V
⊢ neighborSet (G := G) ⊥ v = ∅

Tactic:
rfl

Premises used: setOf, SimpleGraph.Subgraph.neighborSet, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
s : Set G.Subgraph
v : V
h : ∀ (x : V), x ∈ (sSup s).neighborSet v ↔ Membership.mem (γ := Set V) (⋃ G' ∈ s, G'.neighborSet v) x
⊢ (sSup s).neighborSet v = ⋃ G' ∈ s, G'.neighborSet v

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
s : Set G.Subgraph
v x : V
⊢ x ∈ (sSup s).neighborSet v ↔ Membership.mem (γ := Set V) (⋃ G' ∈ s, G'.neighborSet v) x

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
s : Set G.Subgraph
v : V
h : ∀ (x : V), x ∈ (sInf s).neighborSet v ↔ x ∈ (⋂ G' ∈ s, G'.neighborSet v) ∩ G.neighborSet v
⊢ (sInf s).neighborSet v = (⋂ G' ∈ s, G'.neighborSet v) ∩ G.neighborSet v

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
s : Set G.Subgraph
v x : V
⊢ x ∈ (sInf s).neighborSet v ↔ x ∈ (⋂ G' ∈ s, G'.neighborSet v) ∩ G.neighborSet v

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
ι : Sort u_1
V : Type u
G : SimpleGraph V
f : ι → G.Subgraph
v : V
⊢ neighborSet (G := G) (⨆ (i : ι), f i) v = ⋃ (i : ι), (f i).neighborSet v

Tactic:
simp [iSup]

Premises used: iSup
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
ι : Sort u_1
V : Type u
G : SimpleGraph V
f : ι → G.Subgraph
v : V
⊢ neighborSet (G := G) (⨅ (i : ι), f i) v = (⋂ (i : ι), (f i).neighborSet v) ∩ G.neighborSet v

Tactic:
simp [iInf]

Premises used: iInf
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
⊢ edgeSet (G := G) ⊤ = G.edgeSet

Tactic:
rfl

Premises used: setOf, Sym2.fromRel, SimpleGraph.Subgraph.edgeSet, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
⊢ ∀ (x y : V),
    Membership.mem (γ := Set (Sym2 V)) (edgeSet (G := G) ⊥) s(x, y) ↔ Membership.mem (γ := Set (Sym2 V)) ∅ s(x, y)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H₁ H₂ : G.Subgraph
⊢ ∀ (x y : V), s(x, y) ∈ (H₁ ⊓ H₂).edgeSet ↔ s(x, y) ∈ H₁.edgeSet ∩ H₂.edgeSet

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H₁ H₂ : G.Subgraph
⊢ ∀ (x y : V), s(x, y) ∈ (H₁ ⊔ H₂).edgeSet ↔ s(x, y) ∈ H₁.edgeSet ∪ H₂.edgeSet

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
s : Set G.Subgraph
h : ∀ (e : Sym2 V), e ∈ (sSup s).edgeSet ↔ Membership.mem (γ := Set (Sym2 V)) (⋃ G' ∈ s, G'.edgeSet) e
⊢ (sSup s).edgeSet = ⋃ G' ∈ s, G'.edgeSet

Tactic:
ext e
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
s : Set G.Subgraph
e : Sym2 V
h : ∀ (x y : V), s(x, y) ∈ (sSup s).edgeSet ↔ Membership.mem (γ := Set (Sym2 V)) (⋃ G' ∈ s, G'.edgeSet) s(x, y)
⊢ e ∈ (sSup s).edgeSet ↔ Membership.mem (γ := Set (Sym2 V)) (⋃ G' ∈ s, G'.edgeSet) e

Tactic:
induction e
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
s : Set G.Subgraph
x y : V
⊢ s(x, y) ∈ (sSup s).edgeSet ↔ Membership.mem (γ := Set (Sym2 V)) (⋃ G' ∈ s, G'.edgeSet) s(x, y)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
s : Set G.Subgraph
h : ∀ (e : Sym2 V), e ∈ (sInf s).edgeSet ↔ e ∈ (⋂ G' ∈ s, G'.edgeSet) ∩ G.edgeSet
⊢ (sInf s).edgeSet = (⋂ G' ∈ s, G'.edgeSet) ∩ G.edgeSet

Tactic:
ext e
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
s : Set G.Subgraph
e : Sym2 V
h : ∀ (x y : V), s(x, y) ∈ (sInf s).edgeSet ↔ s(x, y) ∈ (⋂ G' ∈ s, G'.edgeSet) ∩ G.edgeSet
⊢ e ∈ (sInf s).edgeSet ↔ e ∈ (⋂ G' ∈ s, G'.edgeSet) ∩ G.edgeSet

Tactic:
induction e
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
s : Set G.Subgraph
x y : V
⊢ s(x, y) ∈ (sInf s).edgeSet ↔ s(x, y) ∈ (⋂ G' ∈ s, G'.edgeSet) ∩ G.edgeSet

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
ι : Sort u_1
V : Type u
G : SimpleGraph V
f : ι → G.Subgraph
⊢ Eq.{u + 1} (α := Set (Sym2 V)) (edgeSet (G := G) (⨆ (i : ι), f i)) (⋃ (i : ι), (f i).edgeSet)

Tactic:
simp [iSup]

Premises used: iSup
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
ι : Sort u_1
V : Type u
G : SimpleGraph V
f : ι → G.Subgraph
⊢ edgeSet (G := G) (⨅ (i : ι), f i) = (⋂ (i : ι), (f i).edgeSet) ∩ G.edgeSet

Tactic:
simp [iInf]

Premises used: iInf
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
⊢ Subgraph.spanningCoe (G := G) ⊤ = G

Tactic:
rfl

Premises used: rfl, SimpleGraph.Subgraph.spanningCoe
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
⊢ Eq.{u + 1} (α := SimpleGraph V) (Subgraph.spanningCoe (G := G) ⊥) ⊥

Tactic:
rfl

Premises used: rfl, SimpleGraph.Subgraph.spanningCoe
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
h : H ≤ H'
⊢ H.support ⊆ H'.support

Tactic:
SetRel.dom_mono fun _ hvw ↦ h.2 hvw

Premises used: And.right, SimpleGraph.Subgraph.support, SetRel.dom_mono
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G H : SimpleGraph V
h : H ≤ G
⊢ (toSubgraph H h).IsSpanning

Tactic:
Set.mem_univ

Premises used: Set.Mem, Set.univ, setOf, Set.mem_univ, SimpleGraph.Subgraph.IsSpanning
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
h : H ≤ H'
⊢ H.spanningCoe ≤ H'.spanningCoe

Tactic:
h.2

Premises used: And.right
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
⊢ (H ⊔ H').spanningCoe = H.spanningCoe ⊔ H'.spanningCoe

Tactic:
rfl

Premises used: rfl, SimpleGraph.Subgraph.spanningCoe
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H₁ H₂ : G.Subgraph
h : H₁ ≤ H₂
⊢ H₁.edgeSet ≤ H₂.edgeSet

Tactic:
Sym2.ind h.2

Premises used: Set.Subset, Sym2.ind
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
⊢ Monotone.{u, u} (α := G.Subgraph) edgeSet

Tactic:
fun _ _ ↦ edgeSet_mono

Premises used: Monotone, SimpleGraph.Subgraph.edgeSet_mono
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H₁ H₂ : G.Subgraph
h : Disjoint H₁ H₂
⊢ H₁.edgeSet ⊓ H₂.edgeSet ≤ ⊥

Tactic:
simpa using edgeSet_mono h.le_bot

Premises used: Disjoint.le_bot, SimpleGraph.Subgraph.edgeSet_mono
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
mp : Disjoint H.verts H'.verts → Disjoint H H'
mpr : Disjoint H H' → Disjoint H.verts H'.verts
⊢ Disjoint H.verts H'.verts ↔ Disjoint H H'

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hdisj : Disjoint H.verts H'.verts
M' : G.Subgraph
hsub₀ : M'.verts ⊆ H.verts
right : ∀ ⦃v w : V⦄, M'.Adj v w → H.Adj v w
hsub₁ : M'.verts ⊆ H'.verts
right_1 : ∀ ⦃v w : V⦄, M'.Adj v w → H'.Adj v w
mp : M' = ⊥
⊢ M' ≤ ⊥

Tactic:
rw [le_bot_iff]

Premises used: le_bot_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hdisj : Disjoint H.verts H'.verts
M' : G.Subgraph
hsub₀ : M'.verts ⊆ H.verts
right : ∀ ⦃v w : V⦄, M'.Adj v w → H.Adj v w
hsub₁ : M'.verts ⊆ H'.verts
right_1 : ∀ ⦃v w : V⦄, M'.Adj v w → H'.Adj v w
mp : ∀ (x : V), x ∈ M'.verts ↔ Membership.mem (γ := Set V) (verts (G := G) ⊥) x
mp₁ : ∀ (x x_1 : V), M'.Adj x x_1 ↔ Adj (G := G) ⊥ x x_1
⊢ M' = ⊥

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hdisj : Disjoint H.verts H'.verts
M' : G.Subgraph
hsub₀ : M'.verts ⊆ H.verts
right : ∀ ⦃v w : V⦄, M'.Adj v w → H.Adj v w
hsub₁ : M'.verts ⊆ H'.verts
right_1 : ∀ ⦃v w : V⦄, M'.Adj v w → H'.Adj v w
x : V
⊢ x ∈ M'.verts ↔ Membership.mem (γ := Set V) (verts (G := G) ⊥) x

Tactic:
grind [verts_bot]

Premises used: SimpleGraph.Subgraph.verts_bot
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hdisj : Disjoint H.verts H'.verts
M' : G.Subgraph
hsub₀ : M'.verts ⊆ H.verts
right : ∀ ⦃v w : V⦄, M'.Adj v w → H.Adj v w
hsub₁ : M'.verts ⊆ H'.verts
right_1 : ∀ ⦃v w : V⦄, M'.Adj v w → H'.Adj v w
x x_1 : V
⊢ M'.Adj x x_1 ↔ Adj (G := G) ⊥ x x_1

Tactic:
⟨(hdisj hsub₀ hsub₁ <| M'.edge_vert · :), False.elim⟩

Premises used: SimpleGraph.Subgraph.edge_vert, False.elim, Iff.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hdisj : Disjoint H.verts H'.verts
M' : G.Subgraph
hsub₀ : M'.verts ⊆ H.verts
right : ∀ ⦃v w : V⦄, M'.Adj v w → H.Adj v w
hsub₁ : M'.verts ⊆ H'.verts
right_1 : ∀ ⦃v w : V⦄, M'.Adj v w → H'.Adj v w
x x_1 : V
⊢ M'.Adj x x_1 ↔ Adj (G := G) ⊥ x x_1

Tactic:
exact ⟨(hdisj hsub₀ hsub₁ <| M'.edge_vert · :), False.elim⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hdisj : Disjoint H H'
S : Set V
h₀ : S ≤ H.verts
h₁ : S ≤ H'.verts
v : V
hvS : v ∈ S
⊢ ∀ {v w : V}, ⊥ v w → G.Adj v w

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hdisj : Disjoint H H'
S : Set V
h₀ : S ≤ H.verts
h₁ : S ≤ H'.verts
v : V
hvS : v ∈ S
⊢ ∀ {v_1 w : V}, ⊥ v_1 w → Membership.mem (γ := Set V) {v} v_1

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hdisj : Disjoint H H'
S : Set V
h₀ : S ≤ H.verts
h₁ : S ≤ H'.verts
v : V
hvS : v ∈ S
M' : G.Subgraph := { verts := {v}, Adj := ⊥, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }
M : G.Subgraph
h : v ∈ M.verts
left : M'.verts ⊆ M.verts
right : ∀ ⦃v w : V⦄, M'.Adj v w → M.Adj v w
⊢ M' ≤ M

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hdisj : Disjoint H H'
S : Set V
h₀ : S ≤ H.verts
h₁ : S ≤ H'.verts
v : V
hvS : v ∈ S
M' : G.Subgraph := { verts := {v}, Adj := ⊥, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }
M : G.Subgraph
h : v ∈ M.verts
⊢ M'.verts ⊆ M.verts

Tactic:
simp [h, M']
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hdisj : Disjoint H H'
S : Set V
h₀ : S ≤ H.verts
h₁ : S ≤ H'.verts
v : V
hvS : v ∈ S
M' : G.Subgraph := { verts := {v}, Adj := ⊥, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }
M : G.Subgraph
h : v ∈ M.verts
⊢ ∀ ⦃v w : V⦄, M'.Adj v w → M.Adj v w

Tactic:
simp [h, M']
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hdisj : Disjoint H H'
S : Set V
h₀ : S ≤ H.verts
h₁ : S ≤ H'.verts
v : V
hvS : v ∈ S
M' : G.Subgraph := { verts := {v}, Adj := ⊥, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }
⊢ ∀ {M : G.Subgraph} (h : v ∈ M.verts), M' ≤ M

Tactic:
have hle {M : Subgraph G} (h : v ∈ M.verts) : M' ≤ M := by constructor <;> simp [h, M']
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hdisj : Disjoint H H'
S : Set V
h₀ : S ≤ H.verts
h₁ : S ≤ H'.verts
v : V
hvS : v ∈ S
M' : G.Subgraph := { verts := {v}, Adj := ⊥, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }
hle : ∀ {M : G.Subgraph} (h : v ∈ M.verts), M' ≤ M
⊢ Membership.mem (γ := Set V) ⊥ v

Tactic:
hdisj (hle <| h₀ hvS) (hle <| h₁ hvS) |>.left <| Set.mem_singleton v

Premises used: Set.mem_singleton, Set.Mem, And.left
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
hdisj : Disjoint H H'
S : Set V
h₀ : S ≤ H.verts
h₁ : S ≤ H'.verts
v : V
hvS : v ∈ S
M' : G.Subgraph := { verts := {v}, Adj := ⊥, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }
hle : ∀ {M : G.Subgraph} (h : v ∈ M.verts), M' ≤ M
⊢ Membership.mem (γ := Set V) ⊥ v

Tactic:
exact hdisj (hle <| h₀ hvS) (hle <| h₁ hvS) |>.left <| Set.mem_singleton v

Premises used: Set.mem_singleton, And.left
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : G.Subgraph
a b : V
G' : SimpleGraph W
f_1 f : G →g G'
H : G.Subgraph
u v : V
h : H.Adj u v
⊢ G'.Adj ((f : (a : V) → W) u) ((f : (a : V) → W) v)

Tactic:
f.map_rel (H.adj_sub h)

Premises used: SimpleGraph.Subgraph.adj_sub, RelHom.map_rel
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : G.Subgraph
a b : V
G' : SimpleGraph W
f_1 f : G →g G'
H : G.Subgraph
u v : V
h : H.Adj u v
⊢ G'.Adj ((f : (a : V) → W) u) ((f : (a : V) → W) v)

Tactic:
exact f.map_rel (H.adj_sub h)

Premises used: SimpleGraph.Subgraph.adj_sub, RelHom.map_rel
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : G.Subgraph
a b : V
G' : SimpleGraph W
f_1 f : G →g G'
H : G.Subgraph
u v : V
h : H.Adj u v
⊢ Membership.mem.{v, v} (α := W) (γ := Set W) ((⇑f : (a : V) → W) '' H.verts) ((f : (a : V) → W) u : W)

Tactic:
Set.mem_image_of_mem _ (H.edge_vert h)

Premises used: SimpleGraph.Subgraph.edge_vert, Set.mem_image_of_mem
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : G.Subgraph
a b : V
G' : SimpleGraph W
f_1 f : G →g G'
H : G.Subgraph
u v : V
h : H.Adj u v
⊢ Membership.mem.{v, v} (α := W) (γ := Set W) ((⇑f : (a : V) → W) '' H.verts) ((f : (a : V) → W) u : W)

Tactic:
exact Set.mem_image_of_mem _ (H.edge_vert h)

Premises used: SimpleGraph.Subgraph.edge_vert, Set.mem_image_of_mem
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : G.Subgraph
a b : V
G' : SimpleGraph W
f_1 f : G →g G'
H : G.Subgraph
u v : V
h : H.Adj u v
⊢ Relation.Map.{u + 1, u + 1, v + 1, v + 1} (γ := W) (δ := W) H.Adj ((⇑f : (a : V) → W) : (a : V) → W)
    ((⇑f : (a : V) → W) : (a : V) → W) ((f : (a : V) → W) v : W) ((f : (a : V) → W) u : W)

Tactic:
⟨v, u, H.symm h, rfl, rfl⟩

Premises used: SimpleGraph.Subgraph.symm, And.intro, Exists.intro, rfl, Relation.Map
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : G.Subgraph
a b : V
G' : SimpleGraph W
f_1 f : G →g G'
H : G.Subgraph
u v : V
h : H.Adj u v
⊢ Relation.Map.{u + 1, u + 1, v + 1, v + 1} (γ := W) (δ := W) H.Adj ((⇑f : (a : V) → W) : (a : V) → W)
    ((⇑f : (a : V) → W) : (a : V) → W) ((f : (a : V) → W) v : W) ((f : (a : V) → W) u : W)

Tactic:
exact ⟨v, u, H.symm h, rfl, rfl⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
verts : ∀ (x : V), x ∈ (Subgraph.map Hom.id H).verts ↔ x ∈ H.verts
Adj : ∀ (x x_1 : V), (Subgraph.map Hom.id H).Adj x x_1 ↔ H.Adj x x_1
⊢ Subgraph.map Hom.id H = H

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
x : V
⊢ x ∈ (Subgraph.map Hom.id H).verts ↔ x ∈ H.verts

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
H : G.Subgraph
x x_1 : V
⊢ (Subgraph.map Hom.id H).Adj x x_1 ↔ H.Adj x x_1

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
U : Type u_2
G'' : SimpleGraph U
H : G.Subgraph
f : G →g G'
g : G' →g G''
verts : ∀ (x : U), x ∈ (Subgraph.map (g.comp f) H).verts ↔ x ∈ (Subgraph.map g (Subgraph.map f H)).verts
Adj : ∀ (x x_1 : U), (Subgraph.map (g.comp f) H).Adj x x_1 ↔ (Subgraph.map g (Subgraph.map f H)).Adj x x_1
⊢ Subgraph.map (g.comp f) H = Subgraph.map g (Subgraph.map f H)

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
U : Type u_2
G'' : SimpleGraph U
H : G.Subgraph
f : G →g G'
g : G' →g G''
x : U
⊢ x ∈ (Subgraph.map (g.comp f) H).verts ↔ x ∈ (Subgraph.map g (Subgraph.map f H)).verts

Tactic:
simp [Subgraph.map]

Premises used: SimpleGraph.Subgraph.map
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
U : Type u_2
G'' : SimpleGraph U
H : G.Subgraph
f : G →g G'
g : G' →g G''
x x_1 : U
⊢ (Subgraph.map (g.comp f) H).Adj x x_1 ↔ (Subgraph.map g (Subgraph.map f H)).Adj x x_1

Tactic:
simp [Subgraph.map]

Premises used: SimpleGraph.Subgraph.map
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H₁ H₂ : G.Subgraph
hH : H₁ ≤ H₂
left : (Subgraph.map f H₁).verts ⊆ (Subgraph.map f H₂).verts
right : ∀ ⦃v w : W⦄, (Subgraph.map f H₁).Adj v w → (Subgraph.map f H₂).Adj v w
⊢ Subgraph.map f H₁ ≤ Subgraph.map f H₂

Tactic:
constructor
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H₁ H₂ : G.Subgraph
hH : H₁ ≤ H₂
a : W
left : ∀ x ∈ H₁.verts, (f : (a : V) → W) x = a → ∃ x ∈ H₂.verts, (f : (a : V) → W) x = a
⊢ a ∈ (Subgraph.map f H₁).verts → a ∈ (Subgraph.map f H₂).verts

Tactic:
simp only [map_verts, Set.mem_image, forall_exists_index, and_imp]

Premises used: and_imp, Set.mem_image, forall_exists_index, SimpleGraph.Subgraph.map_verts
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H₁ H₂ : G.Subgraph
hH : H₁ ≤ H₂
v : V
hv : v ∈ H₁.verts
⊢ ∃ x ∈ H₂.verts, Eq.{v + 1} (α := W) ((f : (a : V) → W) x : W) ((f : (a : V) → W) v : W)

Tactic:
⟨_, hH.1 hv, rfl⟩

Premises used: And.left, And.intro, Exists.intro, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H₁ H₂ : G.Subgraph
hH : H₁ ≤ H₂
v : V
hv : v ∈ H₁.verts
⊢ ∃ x ∈ H₂.verts, Eq.{v + 1} (α := W) ((f : (a : V) → W) x : W) ((f : (a : V) → W) v : W)

Tactic:
exact ⟨_, hH.1 hv, rfl⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H₁ H₂ : G.Subgraph
hH : H₁ ≤ H₂
u v : V
ha : H₁.Adj u v
⊢ (Subgraph.map f H₂).Adj ((f : (a : V) → W) u) ((f : (a : V) → W) v)

Tactic:
⟨_, _, hH.2 ha, rfl, rfl⟩

Premises used: And.right, And.intro, Exists.intro, rfl, Relation.Map
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H₁ H₂ : G.Subgraph
hH : H₁ ≤ H₂
u v : V
ha : H₁.Adj u v
⊢ (Subgraph.map f H₂).Adj ((f : (a : V) → W) u) ((f : (a : V) → W) v)

Tactic:
exact ⟨_, _, hH.2 ha, rfl, rfl⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
⊢ Monotone (Subgraph.map f)

Tactic:
fun _ _ ↦ map_mono

Premises used: Monotone, SimpleGraph.Subgraph.map_mono
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H₁ H₂ : G.Subgraph
verts : ∀ (x : W), x ∈ (Subgraph.map f (H₁ ⊔ H₂)).verts ↔ x ∈ (Subgraph.map f H₁ ⊔ Subgraph.map f H₂).verts
Adj : ∀ (x x_1 : W), (Subgraph.map f (H₁ ⊔ H₂)).Adj x x_1 ↔ (Subgraph.map f H₁ ⊔ Subgraph.map f H₂).Adj x x_1
⊢ Subgraph.map f (H₁ ⊔ H₂) = Subgraph.map f H₁ ⊔ Subgraph.map f H₂

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H₁ H₂ : G.Subgraph
x : W
⊢ x ∈ (Subgraph.map f (H₁ ⊔ H₂)).verts ↔ x ∈ (Subgraph.map f H₁ ⊔ Subgraph.map f H₂).verts

Tactic:
simp [Set.image_union, map_adj, sup_adj, Relation.Map, or_and_right, exists_or]

Premises used: SimpleGraph.Subgraph.sup_adj, exists_or, SimpleGraph.Subgraph.map_adj, or_and_right, Set.image_union, Relation.Map