awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 x_1 : W
⊢ (Subgraph.map f (H₁ ⊔ H₂)).Adj x x_1 ↔ (Subgraph.map f H₁ ⊔ Subgraph.map f H₂).Adj x x_1

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
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
W : Type v
G : SimpleGraph V
H : SimpleGraph W
e : G ≃g H
verts : ∀ (x : W), x ∈ (Subgraph.map e.toHom ⊤).verts ↔ Membership.mem (γ := Set W) (Subgraph.verts (G := H) ⊤) x
Adj : ∀ (x x_1 : W), (Subgraph.map e.toHom ⊤).Adj x x_1 ↔ Subgraph.Adj (G := H) ⊤ x x_1
⊢ Subgraph.map e.toHom ⊤ = ⊤

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
W : Type v
G : SimpleGraph V
H : SimpleGraph W
e : G ≃g H
x : W
⊢ x ∈ (Subgraph.map e.toHom ⊤).verts ↔ Membership.mem (γ := Set W) (verts (G := H) ⊤) x

Tactic:
simp [Relation.Map, e.apply_eq_iff_eq_symm_apply, ← e.map_rel_iff]

Premises used: RelIso.apply_eq_iff_eq_symm_apply, RelIso.map_rel_iff, Relation.Map
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
W : Type v
G : SimpleGraph V
H : SimpleGraph W
e : G ≃g H
x x_1 : W
⊢ (Subgraph.map e.toHom ⊤).Adj x x_1 ↔ Adj (G := H) ⊤ x x_1

Tactic:
simp [Relation.Map, e.apply_eq_iff_eq_symm_apply, ← e.map_rel_iff]

Premises used: RelIso.apply_eq_iff_eq_symm_apply, RelIso.map_rel_iff, 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 : G.Subgraph
⊢ (Subgraph.map f H).edgeSet = Sym2.map (⇑f : (a : V) → W) '' H.edgeSet

Tactic:
Sym2.fromRel_relationMap ..

Premises used: Sym2.fromRel_relationMap, SimpleGraph.Subgraph.edgeSet, 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
h : H ≤ H'
left : (Subgraph.comap f H).verts ⊆ (Subgraph.comap f H').verts
right : ∀ ⦃v w : V⦄, (Subgraph.comap f H).Adj v w → (Subgraph.comap f H').Adj v w
⊢ Subgraph.comap f H ≤ Subgraph.comap 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
h : H ≤ H'
a : V
left :
  Membership.mem (α := W) H.verts ((f : (a : V) → W) a : W) → Membership.mem (α := W) H'.verts ((f : (a : V) → W) a : W)
⊢ a ∈ (Subgraph.comap f H).verts → a ∈ (Subgraph.comap f H').verts

Tactic:
simp only [comap_verts, Set.mem_preimage]

Premises used: SimpleGraph.Subgraph.comap_verts, Set.mem_preimage
-- 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
h : H ≤ H'
a : V
⊢ Membership.mem (α := W) H.verts ((f : (a : V) → W) a : W) → Membership.mem (α := W) H'.verts ((f : (a : V) → W) a : W)

Tactic:
apply h.1

Premises used: And.left
-- 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
h : H ≤ H'
v w : V
right :
  G.Adj v w → H.Adj ((f : (a : V) → W) v) ((f : (a : V) → W) w) → H'.Adj ((f : (a : V) → W) v) ((f : (a : V) → W) w)
⊢ (Subgraph.comap f H).Adj v w → (Subgraph.comap f H').Adj v w

Tactic:
simp +contextual only [comap_adj, and_imp, true_and]

Premises used: and_imp, true_and, SimpleGraph.Subgraph.comap_adj
-- 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
h : H ≤ H'
v w : V
h_1 : G.Adj v w
⊢ H.Adj ((f : (a : V) → W) v) ((f : (a : V) → W) w) → H'.Adj ((f : (a : V) → W) v) ((f : (a : V) → W) w)

Tactic:
apply h.2

Premises used: And.right
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
W : Type v
G : SimpleGraph V
H : SimpleGraph W
f : G →g H
verts : ∀ (x : V), x ∈ (Subgraph.comap f ⊤).verts ↔ Membership.mem (γ := Set V) (Subgraph.verts (G := G) ⊤) x
Adj : ∀ (x x_1 : V), (Subgraph.comap f ⊤).Adj x x_1 ↔ Subgraph.Adj (G := G) ⊤ x x_1
⊢ Subgraph.comap f ⊤ = ⊤

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
W : Type v
G : SimpleGraph V
H : SimpleGraph W
f : G →g H
x : V
⊢ x ∈ (Subgraph.comap f ⊤).verts ↔ Membership.mem (γ := Set V) (verts (G := G) ⊤) x

Tactic:
simp +contextual [f.map_adj]

Premises used: SimpleGraph.Hom.map_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
W : Type v
G : SimpleGraph V
H : SimpleGraph W
f : G →g H
x x_1 : V
⊢ (Subgraph.comap f ⊤).Adj x x_1 ↔ Adj (G := G) ⊤ x x_1

Tactic:
simp +contextual [f.map_adj]

Premises used: SimpleGraph.Hom.map_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H : G.Subgraph
H' : G'.Subgraph
⊢ Subgraph.map f H ≤ H' ↔ H ≤ Subgraph.comap f H'

Tactic:
⟨fun h ↦ ⟨fun v hv ↦ ?_, fun v w hvw ↦ ?_⟩, fun h ↦ ⟨fun v ↦ ?_, fun v w ↦ ?_⟩⟩

Premises used: And.intro, Iff.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H : G.Subgraph
H' : G'.Subgraph
refine_1 : ∀ (h : Subgraph.map f H ≤ H') (v : V) (hv : v ∈ H.verts), v ∈ (Subgraph.comap f H').verts
refine_2 : ∀ (h : Subgraph.map f H ≤ H') (v w : V) (hvw : H.Adj v w), (Subgraph.comap f H').Adj v w
refine_3 : ∀ (h : H ≤ Subgraph.comap f H'), ∀ v ∈ (Subgraph.map f H).verts, v ∈ H'.verts
refine_4 : ∀ (h : H ≤ Subgraph.comap f H') (v w : W), (Subgraph.map f H).Adj v w → H'.Adj v w
⊢ Subgraph.map f H ≤ H' ↔ H ≤ Subgraph.comap f H'

Tactic:
refine ⟨fun h ↦ ⟨fun v hv ↦ ?_, fun v w hvw ↦ ?_⟩, fun h ↦ ⟨fun v ↦ ?_, fun v w ↦ ?_⟩⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H : G.Subgraph
H' : G'.Subgraph
h : Subgraph.map f H ≤ H'
v : V
hv : v ∈ H.verts
refine_1 : Membership.mem (α := W) H'.verts ((f : (a : V) → W) v : W)
⊢ v ∈ (Subgraph.comap f H').verts

Tactic:
simp only [comap_verts, Set.mem_preimage]

Premises used: SimpleGraph.Subgraph.comap_verts, Set.mem_preimage
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H : G.Subgraph
H' : G'.Subgraph
h : Subgraph.map f H ≤ H'
v : V
hv : v ∈ H.verts
⊢ Membership.mem (α := W) H'.verts ((f : (a : V) → W) v : W)

Tactic:
h.1 ⟨v, 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 : G.Subgraph
H' : G'.Subgraph
h : Subgraph.map f H ≤ H'
v : V
hv : v ∈ H.verts
⊢ Membership.mem (α := W) H'.verts ((f : (a : V) → W) v : W)

Tactic:
exact h.1 ⟨v, 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 : G.Subgraph
H' : G'.Subgraph
h : Subgraph.map f H ≤ H'
v w : V
hvw : H.Adj v w
refine_2 : H'.Adj ((f : (a : V) → W) v) ((f : (a : V) → W) w)
⊢ (Subgraph.comap f H').Adj v w

Tactic:
simp only [H.adj_sub hvw, comap_adj, true_and]

Premises used: SimpleGraph.Subgraph.adj_sub, true_and, SimpleGraph.Subgraph.comap_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H : G.Subgraph
H' : G'.Subgraph
h : Subgraph.map f H ≤ H'
v w : V
hvw : H.Adj v w
⊢ H'.Adj ((f : (a : V) → W) v) ((f : (a : V) → W) w)

Tactic:
h.2 ⟨v, w, hvw, rfl, rfl⟩

Premises used: And.right, 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 : G.Subgraph
H' : G'.Subgraph
h : Subgraph.map f H ≤ H'
v w : V
hvw : H.Adj v w
⊢ H'.Adj ((f : (a : V) → W) v) ((f : (a : V) → W) w)

Tactic:
exact h.2 ⟨v, w, hvw, rfl, rfl⟩

Premises used: And.right, 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 : G.Subgraph
H' : G'.Subgraph
h : H ≤ Subgraph.comap f H'
v : W
refine_3 : ∀ x ∈ H.verts, (f : (a : V) → W) x = v → v ∈ H'.verts
⊢ v ∈ (Subgraph.map f H).verts → v ∈ 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 : G.Subgraph
H' : G'.Subgraph
h : H ≤ Subgraph.comap f H'
w : V
hw : w ∈ H.verts
⊢ Membership.mem (α := W) H'.verts ((f : (a : V) → W) w : W)

Tactic:
h.1 hw

Premises used: Set.Mem, setOf, Set.preimage, And.left
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H : G.Subgraph
H' : G'.Subgraph
h : H ≤ Subgraph.comap f H'
w : V
hw : w ∈ H.verts
⊢ Membership.mem (α := W) H'.verts ((f : (a : V) → W) w : W)

Tactic:
exact h.1 hw

Premises used: And.left
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H : G.Subgraph
H' : G'.Subgraph
h : H ≤ Subgraph.comap f H'
v w : W
refine_4 : ∀ (x x_1 : V), H.Adj x x_1 → (f : (a : V) → W) x = v → (f : (a : V) → W) x_1 = w → H'.Adj v w
⊢ (Subgraph.map f H).Adj v w → H'.Adj v w

Tactic:
simp only [Relation.Map, map_adj, forall_exists_index, and_imp]

Premises used: and_imp, forall_exists_index, SimpleGraph.Subgraph.map_adj, 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 : G.Subgraph
H' : G'.Subgraph
h : H ≤ Subgraph.comap f H'
u u' : V
hu : H.Adj u u'
⊢ H'.Adj ((f : (a : V) → W) u) ((f : (a : V) → W) u')

Tactic:
(h.2 hu).2

Premises used: And.right
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H : G.Subgraph
H' : G'.Subgraph
h : H ≤ Subgraph.comap f H'
u u' : V
hu : H.Adj u u'
⊢ H'.Adj ((f : (a : V) → W) u) ((f : (a : V) → W) u')

Tactic:
exact (h.2 hu).2

Premises used: And.right
-- 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
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
H :
  { H : Finset V × (V → V → Bool) //
    (∀ (a b : V), H.2 a b = true → G.Adj a b) ∧
      (∀ (a b : V), H.2 a b = true → a ∈ H.1) ∧ ∀ (a b : V), H.2 a b = H.2 b a }
⊢ Symmetric fun (a b : V) ↦ (↑H : Finset V × (V → V → Bool)).2 a b = true

Tactic:
simp [Symmetric, H.2.2.2]

Premises used: Symmetric, And.right, Subtype.property
-- 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
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
refine_1 :
  Function.Injective (β := G.Subgraph)
    fun
      (H :
        { H : Finset V × (V → V → Bool) //
          (∀ (a b : V), H.2 a b = true → G.Adj a b) ∧
            (∀ (a b : V), H.2 a b = true → a ∈ H.1) ∧ ∀ (a b : V), H.2 a b = H.2 b a }) ↦
    { verts := (↑(↑H : Finset V × (V → V → Bool)).1 : Set V),
      Adj := fun (a b : V) ↦ (↑H : Finset V × (V → V → Bool)).2 a b = true, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }
refine_2 :
  ∀ (H : G.Subgraph),
    ∃ (a :
      { H : Finset V × (V → V → Bool) //
        (∀ (a b : V), H.2 a b = true → G.Adj a b) ∧
          (∀ (a b : V), H.2 a b = true → a ∈ H.1) ∧ ∀ (a b : V), H.2 a b = H.2 b a }),
      (fun
              (H :
                { H : Finset V × (V → V → Bool) //
                  (∀ (a b : V), H.2 a b = true → G.Adj a b) ∧
                    (∀ (a b : V), H.2 a b = true → a ∈ H.1) ∧ ∀ (a b : V), H.2 a b = H.2 b a }) ↦
            { verts := (↑(↑H : Finset V × (V → V → Bool)).1 : Set V),
              Adj := fun (a b : V) ↦ (↑H : Finset V × (V → V → Bool)).2 a b = true, adj_sub := ⋯, edge_vert := ⋯,
              symm := ⋯ : G.Subgraph })
          a =
        H
⊢ Fintype G.Subgraph

Tactic:
refine .ofBijective
    (α := {H : Finset V × (V → V → Bool) //
      (∀ a b, H.2 a b → G.Adj a b) ∧ (∀ a b, H.2 a b → a ∈ H.1) ∧ ∀ a b, H.2 a b = H.2 b a})
    (fun H ↦ ⟨H.1.1, fun a b ↦ H.1.2 a b, @H.2.1, @H.2.2.1, by simp [Symmetric, H.2.2.2]⟩)
    ⟨?_, fun H ↦ ?_⟩
-- 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
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
fst : Finset V
snd : V → V → Bool
property :
  (∀ (a b : V), (fst, snd).2 a b = true → G.Adj a b) ∧
    (∀ (a b : V), (fst, snd).2 a b = true → a ∈ (fst, snd).1) ∧ ∀ (a b : V), (fst, snd).2 a b = (fst, snd).2 b a
fst_1 : Finset V
snd_1 : V → V → Bool
property_1 :
  (∀ (a b : V), (fst_1, snd_1).2 a b = true → G.Adj a b) ∧
    (∀ (a b : V), (fst_1, snd_1).2 a b = true → a ∈ (fst_1, snd_1).1) ∧
      ∀ (a b : V), (fst_1, snd_1).2 a b = (fst_1, snd_1).2 b a
⊢ Eq.{u + 1} (α := G.Subgraph)
      ((fun
            (H :
              { H : Finset V × (V → V → Bool) //
                (∀ (a b : V), H.2 a b = true → G.Adj a b) ∧
                  (∀ (a b : V), H.2 a b = true → a ∈ H.1) ∧ ∀ (a b : V), H.2 a b = H.2 b a }) ↦
          { verts := (↑(↑H : Finset V × (V → V → Bool)).1 : Set V),
            Adj := fun (a b : V) ↦ (↑H : Finset V × (V → V → Bool)).2 a b = true, adj_sub := ⋯, edge_vert := ⋯,
            symm := ⋯ : G.Subgraph })
        (Subtype.mk (p := fun (H : Finset V × (V → V → Bool)) ↦
          (∀ (a b : V), H.2 a b = true → G.Adj a b) ∧
            (∀ (a b : V), H.2 a b = true → a ∈ H.1) ∧ ∀ (a b : V), H.2 a b = H.2 b a)
          (fst, snd) property))
      ((fun
            (H :
              { H : Finset V × (V → V → Bool) //
                (∀ (a b : V), H.2 a b = true → G.Adj a b) ∧
                  (∀ (a b : V), H.2 a b = true → a ∈ H.1) ∧ ∀ (a b : V), H.2 a b = H.2 b a }) ↦
          { verts := (↑(↑H : Finset V × (V → V → Bool)).1 : Set V),
            Adj := fun (a b : V) ↦ (↑H : Finset V × (V → V → Bool)).2 a b = true, adj_sub := ⋯, edge_vert := ⋯,
            symm := ⋯ : G.Subgraph })
        (Subtype.mk (p := fun (H : Finset V × (V → V → Bool)) ↦
          (∀ (a b : V), H.2 a b = true → G.Adj a b) ∧
            (∀ (a b : V), H.2 a b = true → a ∈ H.1) ∧ ∀ (a b : V), H.2 a b = H.2 b a)
          (fst_1, snd_1) property_1)) →
    Eq (α :=
      { H : Finset V × (V → V → Bool) //
        (∀ (a b : V), H.2 a b = true → G.Adj a b) ∧
          (∀ (a b : V), H.2 a b = true → a ∈ H.1) ∧ ∀ (a b : V), H.2 a b = H.2 b a })
      (Subtype.mk (p := fun (H : Finset V × (V → V → Bool)) ↦
        (∀ (a b : V), H.2 a b = true → G.Adj a b) ∧
          (∀ (a b : V), H.2 a b = true → a ∈ H.1) ∧ ∀ (a b : V), H.2 a b = H.2 b a)
        (fst, snd) property)
      (Subtype.mk (p := fun (H : Finset V × (V → V → Bool)) ↦
        (∀ (a b : V), H.2 a b = true → G.Adj a b) ∧
          (∀ (a b : V), H.2 a b = true → a ∈ H.1) ∧ ∀ (a b : V), H.2 a b = H.2 b a)
        (fst_1, snd_1) property_1)

Tactic:
simp [funext_iff]

Premises used: funext_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : G.Subgraph
a_1 b_1 : V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
H : G.Subgraph
a b : V
⊢ (H.verts.toFinset, fun (a b : V) ↦ decide (H.Adj a b)).2 a b = true → G.Adj a b

Tactic:
simpa using H.adj_sub

Premises used: SimpleGraph.Subgraph.adj_sub
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : G.Subgraph
a_1 b_1 : V
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
H : G.Subgraph
a b : V
⊢ (H.verts.toFinset, fun (a b : V) ↦ decide (H.Adj a b)).2 a b = true →
    a ∈ (H.verts.toFinset, fun (a b : V) ↦ decide (H.Adj a b)).1

Tactic:
simpa using H.edge_vert

Premises used: SimpleGraph.Subgraph.edge_vert
-- 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
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
H : G.Subgraph
⊢ ∀ (a b : V),
    Eq (α := Bool) ((H.verts.toFinset, fun (a b : V) ↦ decide (H.Adj a b)).2 a b)
      ((H.verts.toFinset, fun (a b : V) ↦ decide (H.Adj a b)).2 b a)

Tactic:
simp [H.adj_comm]

Premises used: SimpleGraph.Subgraph.adj_comm
-- 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
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
H : G.Subgraph
⊢ (fun
          (H :
            { H : Finset V × (V → V → Bool) //
              (∀ (a b : V), H.2 a b = true → G.Adj a b) ∧
                (∀ (a b : V), H.2 a b = true → a ∈ H.1) ∧ ∀ (a b : V), H.2 a b = H.2 b a }) ↦
        { verts := (↑(↑H : Finset V × (V → V → Bool)).1 : Set V),
          Adj := fun (a b : V) ↦ (↑H : Finset V × (V → V → Bool)).2 a b = true, adj_sub := ⋯, edge_vert := ⋯,
          symm := ⋯ : G.Subgraph })
      (Subtype.mk (p := fun (H : Finset V × (V → V → Bool)) ↦
        (∀ (a b : V), H.2 a b = true → G.Adj a b) ∧
          (∀ (a b : V), H.2 a b = true → a ∈ H.1) ∧ ∀ (a b : V), H.2 a b = H.2 b a)
        (H.verts.toFinset, fun (a b : V) ↦ decide (H.Adj a b)) ⋯) =
    H

Tactic:
simp
-- 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
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
H : G.Subgraph
⊢ ∃ (a :
    { H : Finset V × (V → V → Bool) //
      (∀ (a b : V), H.2 a b = true → G.Adj a b) ∧
        (∀ (a b : V), H.2 a b = true → a ∈ H.1) ∧ ∀ (a b : V), H.2 a b = H.2 b a }),
    (fun
            (H :
              { H : Finset V × (V → V → Bool) //
                (∀ (a b : V), H.2 a b = true → G.Adj a b) ∧
                  (∀ (a b : V), H.2 a b = true → a ∈ H.1) ∧ ∀ (a b : V), H.2 a b = H.2 b a }) ↦
          { verts := (↑(↑H : Finset V × (V → V → Bool)).1 : Set V),
            Adj := fun (a b : V) ↦ (↑H : Finset V × (V → V → Bool)).2 a b = true, adj_sub := ⋯, edge_vert := ⋯,
            symm := ⋯ : G.Subgraph })
        a =
      H

Tactic:
exact ⟨⟨(H.verts.toFinset, fun a b ↦ H.Adj a b), fun a b ↦ by simpa using H.adj_sub,
      fun a b ↦ by simpa using H.edge_vert, by simp [H.adj_comm]⟩, by simp⟩
-- 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
inst : DecidableEq V
inst_1 : Fintype V
inst_2 : DecidableRel G.Adj
H : G.Subgraph
⊢ ∃ (a :
    { H : Finset V × (V → V → Bool) //
      (∀ (a b : V), H.2 a b = true → G.Adj a b) ∧
        (∀ (a b : V), H.2 a b = true → a ∈ H.1) ∧ ∀ (a b : V), H.2 a b = H.2 b a }),
    (fun
            (H :
              { H : Finset V × (V → V → Bool) //
                (∀ (a b : V), H.2 a b = true → G.Adj a b) ∧
                  (∀ (a b : V), H.2 a b = true → a ∈ H.1) ∧ ∀ (a b : V), H.2 a b = H.2 b a }) ↦
          { verts := (↑(↑H : Finset V × (V → V → Bool)).1 : Set V),
            Adj := fun (a b : V) ↦ (↑H : Finset V × (V → V → Bool)).2 a b = true, adj_sub := ⋯, edge_vert := ⋯,
            symm := ⋯ : G.Subgraph })
        a =
      H

Tactic:
classical
    exact ⟨⟨(H.verts.toFinset, fun a b ↦ H.Adj a b), fun a b ↦ by simpa using H.adj_sub,
      fun a b ↦ by simpa using H.edge_vert, by simp [H.adj_comm]⟩, by simp⟩
-- 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
inst : Finite V
intro : ∀ (val : Fintype V), Finite.{u + 1} G.Subgraph
⊢ Finite.{u + 1} G.Subgraph

Tactic:
cases nonempty_fintype V

Premises used: nonempty_fintype
-- 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
inst : Finite V
val : Fintype V
⊢ Finite.{u + 1} G.Subgraph

Tactic:
infer_instance
-- 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
inst : Finite V
intro intro₁ : ∀ (val : Fintype V), Finite.{u + 1} G.Subgraph
⊢ Finite.{u + 1} G.Subgraph

Tactic:
classical cases nonempty_fintype V; infer_instance

Premises used: nonempty_fintype
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
x y : G.Subgraph
h : x ≤ y
⊢ Function.Injective (α := (↑x.verts : Type u)) (β := (↑y.verts : Type u))
    (⇑(inclusion h) : (a : (↑x.verts : Type u)) → (↑y.verts : Type u))

Tactic:
fun _ _ h ↦ Subtype.ext congr(Subtype.val $h)

Premises used: congrArg, id, Function.Injective, Subtype.val, Subtype.ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
x : G.Subgraph
⊢ Eq (α := (a : (↑x.verts : Type u)) → V) (⇑x.hom : (a : (↑x.verts : Type u)) → V) fun (v : (↑x.verts : Type u)) ↦
    (↑v : V)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
x : G.Subgraph
⊢ Function.Injective (α := (↑x.verts : Type u)) (β := V) (⇑x.hom : (a : (↑x.verts : Type u)) → V)

Tactic:
fun _ _ ↦ Subtype.ext

Premises used: Function.Injective, Subtype.ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
⊢ Subgraph.map G'.hom ⊤ = G'

Tactic:
aesop (add unfold safe Relation.Map, unsafe G'.edge_vert, unsafe Adj.symm)

Premises used: SimpleGraph.Subgraph.edge_vert, SimpleGraph.Subgraph.Adj.symm, Relation.Map
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
x : G.Subgraph
⊢ Function.Injective (α := V) (β := V) (⇑x.spanningHom : (a : V) → V)

Tactic:
fun _ _ ↦ id

Premises used: id, Function.Injective
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
x y : G.Subgraph
h : x ≤ y
v : V
⊢ x.neighborSet v ⊆ y.neighborSet v

Tactic:
fun _ h' ↦ h.2 h'

Premises used: Set.Mem, setOf, SimpleGraph.Subgraph.neighborSet, Set.Subset, And.right
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
G' : G.Subgraph
inst_1 : Fintype (↑G'.verts : Type u)
h : G'.IsSpanning
simp : Finset.card.{u} (α := V) Finset.univ = Fintype.card V
⊢ G'.verts.toFinset.card = Fintype.card V

Tactic:
simp only [isSpanning_iff.1 h, Set.toFinset_univ]

Premises used: Iff.mp, Set.toFinset_univ, SimpleGraph.Subgraph.isSpanning_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
inst : Fintype V
G' : G.Subgraph
inst_1 : Fintype (↑G'.verts : Type u)
h : G'.IsSpanning
⊢ Finset.card.{u} (α := V) Finset.univ = Fintype.card V

Tactic:
congr
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
inst : Fintype (↑(G'.neighborSet v) : Type u)
rw : (G'.neighborSet v).toFinset.card = Fintype.card.{u} (↑(G'.neighborSet v) : Type u)
rw₁ rw₂ : Fintype.card.{u} (↑(G'.neighborSet v) : Type u) = Fintype.card.{u} (↑(G'.neighborSet v) : Type u)
⊢ (G'.neighborSet v).toFinset.card = G'.degree v

Tactic:
rw [degree, Set.toFinset_card]

Premises used: Set.toFinset_card, SimpleGraph.Subgraph.degree
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
inst : Fintype (↑(G'.neighborSet v) : Type u)
h : v ∉ G'.verts
rw : ∀ (x : V), x ∉ G'.neighborSet v
⊢ G'.degree v = 0

Tactic:
rw [degree, Fintype.card_eq_zero_iff, isEmpty_subtype]

Premises used: SimpleGraph.Subgraph.degree, Fintype.card_eq_zero_iff, isEmpty_subtype
-- Module: Mathlib.Combinatorics.SimpleGraph.Subgraph
Goal:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
v : V
inst : Fintype (↑(G'.neighborSet v) : Type u)
h : v ∉ G'.verts
w : V
by_contra : ∀ (hw : w ∈ G'.neighborSet v), False
⊢ w ∉ G'.neighborSet v

Tactic:
by_contra hw