awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
G : SimpleGraph V
⊢ spanningCoe (s := Set.univ) (induce Set.univ G) = G

Tactic:
G.spanningCoe_induce_eq_self _ |>.mpr G.support.subset_univ

Premises used: Iff.mpr, Set.subset_univ, SimpleGraph.support, SimpleGraph.spanningCoe_induce_eq_self
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
G : SimpleGraph V
s t : Set V
h : G.IsCompleteBetween s t
u : Set V
v₁ : (↑u : Type u_1)
hs : Membership.mem (γ := Set (↑u : Type u_1)) (u ↓∩ s) v₁
_ : ∀ ⦃v₂ : (↑u : Type u_1)⦄, Membership.mem (γ := Set (↑u : Type u_1)) (u ↓∩ t) v₂ → (SimpleGraph.induce u G).Adj v₁ v₂
⊢ ∀ ⦃v₂ : (↑u : Type u_1)⦄, Membership.mem (γ := Set (↑u : Type u_1)) (u ↓∩ t) v₂ → (SimpleGraph.induce u G).Adj v₁ v₂

Tactic:
_
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
G : SimpleGraph V
s t : Set V
h : G.IsCompleteBetween s t
u : Set V
v₁ : (↑u : Type u_1)
hs : Membership.mem (γ := Set (↑u : Type u_1)) (u ↓∩ s) v₁
v₂ : (↑u : Type u_1)
ht : Membership.mem (γ := Set (↑u : Type u_1)) (u ↓∩ t) v₂
rw : G.Adj (↑v₁ : V) (↑v₂ : V)
⊢ (SimpleGraph.induce u G).Adj v₁ v₂

Tactic:
rw [comap_adj, Embedding.coe_subtype]

Premises used: Function.Embedding.coe_subtype, SimpleGraph.comap_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
G : SimpleGraph V
s t : Set V
h : G.IsCompleteBetween s t
u : Set V
v₁ : (↑u : Type u_1)
hs : Membership.mem (γ := Set (↑u : Type u_1)) (u ↓∩ s) v₁
v₂ : (↑u : Type u_1)
ht : Membership.mem (γ := Set (↑u : Type u_1)) (u ↓∩ t) v₂
⊢ G.Adj (↑v₁ : V) (↑v₂ : V)

Tactic:
h hs ht
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
G : SimpleGraph V
s t : Set V
h : G.IsCompleteBetween s t
u : Set V
v₁ : (↑u : Type u_1)
hs : Membership.mem (γ := Set (↑u : Type u_1)) (u ↓∩ s) v₁
v₂ : (↑u : Type u_1)
ht : Membership.mem (γ := Set (↑u : Type u_1)) (u ↓∩ t) v₂
⊢ G.Adj (↑v₁ : V) (↑v₂ : V)

Tactic:
exact h hs ht
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
G : SimpleGraph V
⊢ Eq.{u_1 + 1} (α := (a : V) → V) (⇑Hom.id : (a : V) → V) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
X : Type u_3
G : SimpleGraph V
G' : SimpleGraph W
u v : V
G₁ G₂ : SimpleGraph V
H : SimpleGraph W
f : G →g G'
inst : IsEmpty (V → W)
⊢ IsEmpty (G →g H)

Tactic:
DFunLike.coe.isEmpty

Premises used: Function.isEmpty, DFunLike.coe
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
X : Type u_3
G : SimpleGraph V
G' : SimpleGraph W
u v : V
G₁ G₂ : SimpleGraph V
H : SimpleGraph W
f : G →g G'
inst : Subsingleton (V → W)
⊢ Subsingleton (G →g H)

Tactic:
DFunLike.coe_injective.subsingleton

Premises used: Function.Injective.subsingleton, DFunLike.coe_injective
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
X : Type u_3
G : SimpleGraph V
G' : SimpleGraph W
u v : V
G₁ G₂ : SimpleGraph V
H : SimpleGraph W
f : G →g G'
inst : Finite V
inst_1 : Finite W
⊢ Finite (G →g H)

Tactic:
DFunLike.finite _

Premises used: DFunLike.finite
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
h : G.Adj v w
⊢ G'.Adj ((f : (a : V) → W) v) ((f : (a : V) → W) w)

Tactic:
f.map_rel' h

Premises used: RelHom.map_rel'
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
e : Sym2 V
h : e ∈ G.edgeSet
⊢ Sym2.map (⇑f : (a : V) → W) e ∈ G'.edgeSet

Tactic:
Sym2.ind (fun _ _ => f.map_rel') e h

Premises used: Sym2.ind
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
⊢ G.edgeSet ⊆ Sym2.map (⇑f : (a : V) → W) ⁻¹' G'.edgeSet

Tactic:
fun _ ↦ f.map_mem_edgeSet

Premises used: Set.Mem, setOf, SimpleGraph.Hom.map_mem_edgeSet, Set.Subset, Set.preimage
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
⊢ Sym2.map (⇑f : (a : V) → W) '' G.edgeSet ⊆ G'.edgeSet

Tactic:
Set.image_subset_iff.mpr f.subset_preimage_edgeSet

Premises used: Iff.mpr, Set.image_subset_iff, SimpleGraph.Hom.subset_preimage_edgeSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
v w : V
h : w ∈ G.neighborSet v
⊢ Membership.mem (α := W) (G'.neighborSet ((f : (a : V) → W) v)) ((f : (a : V) → W) w : W)

Tactic:
map_adj f h

Premises used: Set.Mem, setOf, SimpleGraph.Hom.map_adj, SimpleGraph.neighborSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
v : V
f : G →g G'
⊢ G.neighborSet v ⊆ (⇑f : (a : V) → W) ⁻¹' G'.neighborSet ((f : (a : V) → W) v)

Tactic:
fun _ ↦ f.apply_mem_neighborSet

Premises used: Set.Mem, setOf, SimpleGraph.neighborSet, Set.Subset, Set.preimage, SimpleGraph.Hom.apply_mem_neighborSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
v : V
f : G →g G'
⊢ (⇑f : (a : V) → W) '' G.neighborSet v ⊆ G'.neighborSet ((f : (a : V) → W) v)

Tactic:
Set.image_subset_iff.mpr <| f.subset_preimage_neighborSet v

Premises used: Iff.mpr, SimpleGraph.Hom.subset_preimage_neighborSet, Set.image_subset_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
d : G.Dart
⊢ f.mapDart d = { toProd := Prod.map (⇑f : (a : V) → W) (⇑f : (a : V) → W) d.toProd, adj := ⋯ }

Tactic:
rfl

Premises used: SimpleGraph.Hom.mapDart, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
G₁ G₂ : SimpleGraph V
h : G₁ ≤ G₂
⊢ Eq (α := (a : V) → V) (⇑(ofLE h) : (a : V) → V) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
G₁ G₂ : SimpleGraph V
h : G₁ ≤ G₂
v : V
⊢ (ofLE h : (a : V) → V) v = v

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
hinj : Injective.{u_1 + 1, u_2 + 1} (α := V) (β := W) (⇑f : (a : V) → W)
e₁ : Sym2 V
h₁ : e₁ ∈ G.edgeSet
e₂ : Sym2 V
h₂ : e₂ ∈ G.edgeSet
dsimp :
  Subtype.mk (p := fun (x : Sym2 W) ↦ x ∈ G'.edgeSet) (Sym2.map (⇑f : (a : V) → W) e₁) ⋯ =
      Subtype.mk (p := fun (x : Sym2 W) ↦ x ∈ G'.edgeSet) (Sym2.map (⇑f : (a : V) → W) e₂) ⋯ →
    Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) e₁ h₁ = Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) e₂ h₂
⊢ f.mapEdgeSet (Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) e₁ h₁) =
      f.mapEdgeSet (Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) e₂ h₂) →
    Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) e₁ h₁ = Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) e₂ h₂

Tactic:
dsimp [Hom.mapEdgeSet]

Premises used: SimpleGraph.Hom.mapEdgeSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
hinj : Injective.{u_1 + 1, u_2 + 1} (α := V) (β := W) (⇑f : (a : V) → W)
e₁ : Sym2 V
h₁ : e₁ ∈ G.edgeSet
e₂ : Sym2 V
h₂ : e₂ ∈ G.edgeSet
rw :
  Eq.{u_2 + 1} (α := Sym2 W) (Sym2.map (⇑f : (a : V) → W) e₁) (Sym2.map (⇑f : (a : V) → W) e₂) →
    Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) e₁ h₁ = Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) e₂ h₂
⊢ Subtype.mk (p := fun (x : Sym2 W) ↦ x ∈ G'.edgeSet) (Sym2.map (⇑f : (a : V) → W) e₁) ⋯ =
      Subtype.mk (p := fun (x : Sym2 W) ↦ x ∈ G'.edgeSet) (Sym2.map (⇑f : (a : V) → W) e₂) ⋯ →
    Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) e₁ h₁ = Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) e₂ h₂

Tactic:
rw [Subtype.mk_eq_mk]

Premises used: Subtype.mk_eq_mk
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
hinj : Injective.{u_1 + 1, u_2 + 1} (α := V) (β := W) (⇑f : (a : V) → W)
e₁ : Sym2 V
h₁ : e₁ ∈ G.edgeSet
e₂ : Sym2 V
h₂ : e₂ ∈ G.edgeSet
rw : Eq.{u_2 + 1} (α := Sym2 W) (Sym2.map (⇑f : (a : V) → W) e₁) (Sym2.map (⇑f : (a : V) → W) e₂) → e₁ = e₂
⊢ Eq.{u_2 + 1} (α := Sym2 W) (Sym2.map (⇑f : (a : V) → W) e₁) (Sym2.map (⇑f : (a : V) → W) e₂) →
    Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) e₁ h₁ = Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) e₂ h₂

Tactic:
rw [Subtype.mk_eq_mk]

Premises used: Subtype.mk_eq_mk
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
hinj : Injective.{u_1 + 1, u_2 + 1} (α := V) (β := W) (⇑f : (a : V) → W)
e₁ : Sym2 V
h₁ : e₁ ∈ G.edgeSet
e₂ : Sym2 V
h₂ : e₂ ∈ G.edgeSet
repeat : Eq.{u_2 + 1} (α := Sym2 W) (Sym2.map (⇑f : (a : V) → W) e₁) (Sym2.map (⇑f : (a : V) → W) e₂) → e₁ = e₂
⊢ Subtype.mk (p := fun (x : Sym2 W) ↦ x ∈ G'.edgeSet) (Sym2.map (⇑f : (a : V) → W) e₁) ⋯ =
      Subtype.mk (p := fun (x : Sym2 W) ↦ x ∈ G'.edgeSet) (Sym2.map (⇑f : (a : V) → W) e₂) ⋯ →
    Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) e₁ h₁ = Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ G.edgeSet) e₂ h₂

Tactic:
repeat rw [Subtype.mk_eq_mk]

Premises used: Subtype.mk_eq_mk
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
hinj : Injective.{u_1 + 1, u_2 + 1} (α := V) (β := W) (⇑f : (a : V) → W)
e₁ : Sym2 V
h₁ : e₁ ∈ G.edgeSet
e₂ : Sym2 V
h₂ : e₂ ∈ G.edgeSet
⊢ Eq.{u_2 + 1} (α := Sym2 W) (Sym2.map (⇑f : (a : V) → W) e₁) (Sym2.map (⇑f : (a : V) → W) e₂) → e₁ = e₂

Tactic:
apply Sym2.map.injective hinj

Premises used: Sym2.map.injective
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
G₁ G₂ : SimpleGraph V
hle : G₁ ≤ G₂
v : V
⊢ G₁.neighborSet v ⊆ G₂.neighborSet v

Tactic:
subset_preimage_neighborSet v <| .ofLE hle

Premises used: Set.Mem, setOf, SimpleGraph.neighborSet, SimpleGraph.Hom.subset_preimage_neighborSet, Set.preimage, SimpleGraph.Hom.ofLE
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
G' : SimpleGraph W
f : Hom.{u_1, u_2} (V := V) ⊤ G'
v w : V
h : Eq.{u_2 + 1} (α := W) ((f : (a : V) → W) v : W) ((f : (a : V) → W) w : W)
contrapose! : ∀ (h : v ≠ w), Ne.{u_2 + 1} (α := W) ((f : (a : V) → W) v : W) ((f : (a : V) → W) w : W)
⊢ v = w

Tactic:
contrapose! h
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
G' : SimpleGraph W
f : Hom.{u_1, u_2} (V := V) ⊤ G'
v w : V
h : v ≠ w
⊢ Ne.{u_2 + 1} (α := W) ((f : (a : V) → W) v : W) ((f : (a : V) → W) w : W)

Tactic:
G'.ne_of_adj (map_adj _ ((top_adj _ _).mpr h))

Premises used: Iff.mpr, SimpleGraph.ne_of_adj, SimpleGraph.Hom.map_adj, SimpleGraph.top_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
G' : SimpleGraph W
f : Hom.{u_1, u_2} (V := V) ⊤ G'
v w : V
h : v ≠ w
⊢ Ne.{u_2 + 1} (α := W) ((f : (a : V) → W) v : W) ((f : (a : V) → W) w : W)

Tactic:
exact G'.ne_of_adj (map_adj _ ((top_adj _ _).mpr h))

Premises used: Iff.mpr, SimpleGraph.ne_of_adj, SimpleGraph.Hom.map_adj, SimpleGraph.top_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
X : Type u_3
G_1 : SimpleGraph V
G' : SimpleGraph W
u v : V
G₁ G₂ : SimpleGraph V
H : SimpleGraph W
f_1 : G_1 →g G'
f : V → W
G : SimpleGraph W
⊢ ∀ {a b : V}, (SimpleGraph.comap f G).Adj a b → G.Adj (f a) (f b)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
f : H →g G
⊢ H ≤ SimpleGraph.comap (⇑f : (a : W) → V) G

Tactic:
fun _ _ ↦ f.map_adj

Premises used: SimpleGraph.Hom.map_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
⊢ Nonempty (H →g G) ↔ ∃ (f : W → V), H ≤ SimpleGraph.comap f G

Tactic:
⟨fun ⟨f⟩ ↦ ⟨f, f.le_comap⟩, fun ⟨f, h⟩ ↦ ⟨f, (h ·)⟩⟩

Premises used: Exists, _private.0.SimpleGraph.Hom.nonempty_hom_iff_exists_le_comap.match_2, LE.le, SimpleGraph.Hom.le_comap, Nonempty.intro, SimpleGraph.comap, Iff.intro, Exists.intro, Nonempty, SimpleGraph.Hom, RelHom.mk, DFunLike.coe, _private.0.SimpleGraph.Hom.nonempty_hom_iff_exists_le_comap.match_1
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
X : Type u_3
G : SimpleGraph V
G' : SimpleGraph W
G'' : SimpleGraph X
f' : G' →g G''
f : G →g G'
⊢ Eq (α := (a : V) → X) (⇑(f'.comp f) : (a : V) → X)
    (Function.comp.{u_1 + 1, u_2 + 1, u_3 + 1} (β := W) (⇑f' : (a : W) → X) (⇑f : (a : V) → W))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
f : H →g G
⊢ comp (Hom.comap (⇑f : (a : W) → V) G) (ofLE ⋯) = f

Tactic:
rfl

Premises used: RelHom.comp, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
f : G ↪g H
⊢ Eq (α := (a : V) → W) (⇑f.toHom : (a : V) → W) (⇑f : (a : V) → W)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : G ↪g G'
v w : V
⊢ G'.Adj ((f : (a : V) → W) v) ((f : (a : V) → W) w) ↔ G.Adj v w

Tactic:
f.map_rel_iff

Premises used: RelEmbedding.map_rel_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : G ↪g G'
e : Sym2 V
⊢ Sym2.map (⇑f : (a : V) → W) e ∈ G'.edgeSet ↔ e ∈ G.edgeSet

Tactic:
Sym2.ind (fun _ _ => f.map_adj_iff) e

Premises used: Sym2.ind
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : G ↪g G'
⊢ Sym2.map (⇑f : (a : V) → W) ⁻¹' G'.edgeSet = G.edgeSet

Tactic:
Set.ext fun _ ↦ map_mem_edgeSet_iff f

Premises used: Set.ext, SimpleGraph.Embedding.map_mem_edgeSet_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : G ↪g G'
v w : V
⊢ Membership.mem (α := W) (G'.neighborSet ((f : (a : V) → W) v)) ((f : (a : V) → W) w : W) ↔ w ∈ G.neighborSet v

Tactic:
map_adj_iff f

Premises used: Set.Mem, SimpleGraph.Embedding.map_adj_iff, setOf, SimpleGraph.neighborSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
v : V
f : G ↪g G'
⊢ (⇑f : (a : V) → W) ⁻¹' G'.neighborSet ((f : (a : V) → W) v) = G.neighborSet v

Tactic:
Set.ext fun _ ↦ apply_mem_neighborSet_iff f

Premises used: Set.ext, SimpleGraph.Embedding.apply_mem_neighborSet_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
X : Type u_3
G : SimpleGraph V
G' : SimpleGraph W
u v_1 : V
H : SimpleGraph W
f : G ↪g G'
v w₁ : V
h₁ : w₁ ∈ G.neighborSet v
w₂ : V
h₂ : w₂ ∈ G.neighborSet v
h :
  Eq.{u_2 + 1} (α := (↑(G'.neighborSet ((f : (a : V) → W) v)) : Type u_2))
    ((fun (w : (↑(G.neighborSet v) : Type u_1)) ↦
        (Subtype.mk (p := fun (x : W) ↦ x ∈ G'.neighborSet ((f : (a : V) → W) v)) ((f : (a : V) → W) (↑w : V)) ⋯ :
          { x : W // x ∈ G'.neighborSet ((f : (a : V) → W) v) }))
      (Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet v) w₁ h₁))
    ((fun (w : (↑(G.neighborSet v) : Type u_1)) ↦
        (Subtype.mk (p := fun (x : W) ↦ x ∈ G'.neighborSet ((f : (a : V) → W) v)) ((f : (a : V) → W) (↑w : V)) ⋯ :
          { x : W // x ∈ G'.neighborSet ((f : (a : V) → W) v) }))
      (Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet v) w₂ h₂))
rw :
  ∀
    (h :
      Eq.{u_2 + 1} (α := W) ((f : (a : V) → W) (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet v) w₁ h₁) : V) : W)
        ((f : (a : V) → W) (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet v) w₂ h₂) : V) : W)),
    w₁ = w₂
⊢ Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet v) w₁ h₁ = Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet v) w₂ h₂

Tactic:
rw [Subtype.mk_eq_mk] at h ⊢

Premises used: Subtype.mk_eq_mk
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
X : Type u_3
G : SimpleGraph V
G' : SimpleGraph W
u v_1 : V
H : SimpleGraph W
f : G ↪g G'
v w₁ : V
h₁ : w₁ ∈ G.neighborSet v
w₂ : V
h₂ : w₂ ∈ G.neighborSet v
h :
  Eq.{u_2 + 1} (α := W) ((f : (a : V) → W) (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet v) w₁ h₁) : V) : W)
    ((f : (a : V) → W) (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet v) w₂ h₂) : V) : W)
⊢ w₁ = w₂

Tactic:
f.inj' h

Premises used: Function.Embedding.inj', RelEmbedding.toEmbedding
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
X : Type u_3
G : SimpleGraph V
G' : SimpleGraph W
u v_1 : V
H : SimpleGraph W
f : G ↪g G'
v w₁ : V
h₁ : w₁ ∈ G.neighborSet v
w₂ : V
h₂ : w₂ ∈ G.neighborSet v
h :
  Eq.{u_2 + 1} (α := W) ((f : (a : V) → W) (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet v) w₁ h₁) : V) : W)
    ((f : (a : V) → W) (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet v) w₂ h₂) : V) : W)
⊢ w₁ = w₂

Tactic:
exact f.inj' h

Premises used: Function.Embedding.inj', RelEmbedding.toEmbedding
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
X : Type u_3
G : SimpleGraph V
G' : SimpleGraph W
u v : V
H : SimpleGraph W
f : G ↪g G'
⊢ ∀ {a b : V},
    Adj (V := (↑(Set.range.{u_2, u_1 + 1} (ι := V) (⇑f : (a : V) → W)) : Type u_2))
        (induce (Set.range.{u_2, u_1 + 1} (ι := V) (⇑f : (a : V) → W)) G')
        ((Equiv.ofInjective (⇑f : (a : V) → W) ⋯ : (a : V) → (↑(Set.range (⇑f : (a : V) → W)) : Type u_2)) a)
        ((Equiv.ofInjective (⇑f : (a : V) → W) ⋯ : (a : V) → (↑(Set.range (⇑f : (a : V) → W)) : Type u_2)) b) ↔
      G.Adj a b

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
X : Type u_3
G_1 : SimpleGraph V
G' : SimpleGraph W
u v : V
H : SimpleGraph W
f_1 : G_1 ↪g G'
f : V ↪ W
G : SimpleGraph W
⊢ ∀ {a b : V}, G.Adj ((f : (a : V) → W) a) ((f : (a : V) → W) b) ↔ Adj (SimpleGraph.comap (⇑f : (a : V) → W) G) a b

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph W
v : V
⊢ Eq.{u_2 + 1} (α := W) ((Embedding.comap f G : (a : V) → W) v : W) ((f : (a : V) → W) v : W)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
f : H ↪g G
Adj : ∀ (x x_1 : W), SimpleGraph.Adj (SimpleGraph.comap (⇑f : (a : W) → V) G) x x_1 ↔ H.Adj x x_1
⊢ SimpleGraph.comap (⇑f : (a : W) → V) G = H

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
f : H ↪g G
x x_1 : W
⊢ Adj (SimpleGraph.comap (⇑f : (a : W) → V) G) x x_1 ↔ H.Adj x x_1

Tactic:
f.map_adj_iff

Premises used: SimpleGraph.Embedding.map_adj_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
f : H ↪g G
x x_1 : W
⊢ Adj (SimpleGraph.comap (⇑f : (a : W) → V) G) x x_1 ↔ H.Adj x x_1

Tactic:
exact f.map_adj_iff

Premises used: SimpleGraph.Embedding.map_adj_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
X : Type u_3
G_1 : SimpleGraph V
G' : SimpleGraph W
u v : V
H : SimpleGraph W
f_1 : G_1 ↪g G'
f : V ↪ W
G : SimpleGraph V
⊢ ∀ {a b : V},
    Adj.{u_2} (V := W) (SimpleGraph.map (⇑f : (a : V) → W) G : SimpleGraph W) ((f : (a : V) → W) a : W)
        ((f : (a : V) → W) b : W) ↔
      G.Adj a b

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
v : V
⊢ Eq.{u_2 + 1} (α := W) ((Embedding.map f G : (a : V) → W) v : W) ((f : (a : V) → W) v : W)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
X : Type u_3
G : SimpleGraph V
G' : SimpleGraph W
u v : V
H : SimpleGraph W
f_1 : G ↪g G'
α : Type u_4
β : Type u_5
f : α ↪ β
⊢ ∀ {a b : α}, (completeGraph β).Adj ((f : (a : α) → β) a) ((f : (a : α) → β) b) ↔ (completeGraph α).Adj a b

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
α : Type u_4
β : Type u_5
f : α ↪ β
⊢ Eq (α := (a : α) → β) (⇑(Embedding.completeGraph f) : (a : α) → β) (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
X : Type u_3
G : SimpleGraph V
G' : SimpleGraph W
G'' : SimpleGraph X
f' : G' ↪g G''
f : G ↪g G'
⊢ Eq (α := (a : V) → X) (⇑(f'.comp f) : (a : V) → X)
    (Function.comp.{u_1 + 1, u_2 + 1, u_3 + 1} (β := W) (⇑f' : (a : W) → X) (⇑f : (a : V) → W))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
X : Type u_3
G : SimpleGraph V
G' : SimpleGraph W
u v : V
H : SimpleGraph W
f_1 : G ↪g G'
G'' : SimpleGraph X
f : G ↪g H
⊢ ∀ {a b : V},
    Hᶜ.Adj ((f.toEmbedding (r := G.Adj) (s := H.Adj) : (a : V) → W) a)
        ((f.toEmbedding (r := G.Adj) (s := H.Adj) : (a : V) → W) b) ↔
      Gᶜ.Adj a b

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
X : Type u_3
G : SimpleGraph V
G' : SimpleGraph W
u v_1 : V
H : SimpleGraph W
f_1 : G ↪g G'
G'' : SimpleGraph X
f : Gᶜ ↪g Hᶜ
v w : V
inl :
  H.Adj ((f.toEmbedding (r := Gᶜ.Adj) (s := Hᶜ.Adj) : (a : V) → W) v)
      ((f.toEmbedding (r := Gᶜ.Adj) (s := Hᶜ.Adj) : (a : V) → W) v) ↔
    G.Adj v v
inr :
  ∀ (hvw : v ≠ w),
    H.Adj ((f.toEmbedding (r := Gᶜ.Adj) (s := Hᶜ.Adj) : (a : V) → W) v)
        ((f.toEmbedding (r := Gᶜ.Adj) (s := Hᶜ.Adj) : (a : V) → W) w) ↔
      G.Adj v w
⊢ H.Adj ((f.toEmbedding (r := Gᶜ.Adj) (s := Hᶜ.Adj) : (a : V) → W) v)
      ((f.toEmbedding (r := Gᶜ.Adj) (s := Hᶜ.Adj) : (a : V) → W) w) ↔
    G.Adj v w

Tactic:
obtain rfl | hvw := eq_or_ne v w

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
X : Type u_3
G : SimpleGraph V
G' : SimpleGraph W
u v_1 : V
H : SimpleGraph W
f_1 : G ↪g G'
G'' : SimpleGraph X
f : Gᶜ ↪g Hᶜ
v : V
⊢ H.Adj ((f.toEmbedding (r := Gᶜ.Adj) (s := Hᶜ.Adj) : (a : V) → W) v)
      ((f.toEmbedding (r := Gᶜ.Adj) (s := Hᶜ.Adj) : (a : V) → W) v) ↔
    G.Adj v v

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
X : Type u_3
G : SimpleGraph V
G' : SimpleGraph W
u v_1 : V
H : SimpleGraph W
f_1 : G ↪g G'
G'' : SimpleGraph X
f : Gᶜ ↪g Hᶜ
v w : V
hvw : v ≠ w
⊢ H.Adj ((f.toEmbedding (r := Gᶜ.Adj) (s := Hᶜ.Adj) : (a : V) → W) v)
      ((f.toEmbedding (r := Gᶜ.Adj) (s := Hᶜ.Adj) : (a : V) → W) w) ↔
    G.Adj v w

Tactic:
simpa [hvw, not_iff_not] using f.map_adj_iff (v := v) (w := w)

Premises used: not_iff_not, SimpleGraph.Embedding.map_adj_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
s : Set V
t : Set W
φ : G →g G'
φst : Set.MapsTo (⇑φ : (a : V) → W) s t
⊢ (⇑(induceHom (s := s) (t := t) φ φst) : (a : (↑s : Type u_1)) → (↑t : Type u_2)) =
    Set.MapsTo.restrict (⇑φ : (a : V) → W) s t φst

Tactic:
rfl

Premises used: Subtype.map, Set.MapsTo.restrict, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
G : SimpleGraph V
s : Set V
h :
  ∀ (x : (↑s : Type u_1)),
    Eq.{u_1 + 1} (α := V) (↑((induceHom (s := s) (t := s) Hom.id ⋯ : (a : (↑s : Type u_1)) → (↑s : Type u_1)) x) : V)
      (↑((Hom.id : (a : (↑s : Type u_1)) → (↑s : Type u_1)) x) : V)
⊢ Eq.{u_1 + 1} (α := induce s G →g induce s G) (induceHom (s := s) (t := s) Hom.id ⋯) Hom.id

Tactic:
ext x
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
G : SimpleGraph V
s : Set V
x : (↑s : Type u_1)
⊢ Eq.{u_1 + 1} (α := V) (↑((induceHom (s := s) (t := s) Hom.id ⋯ : (a : (↑s : Type u_1)) → (↑s : Type u_1)) x) : V)
    (↑((Hom.id : (a : (↑s : Type u_1)) → (↑s : Type u_1)) x) : V)

Tactic:
rfl