awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
x y : W
a b : V
hadj : G.Adj a b
ha : (f : (a : V) → W) a = x
hb : (f : (a : V) → W) b = y
right : Sym2.map (⇑f : (a : V) → W) s(a, b) = s(x, y)
right₁ : s((f : (a : V) → W) a, (f : (a : V) → W) b) = s(x, y)
right₂ : s(x, (f : (a : V) → W) b) = s(x, y)
right₃ right₄ : s(x, y) = s(x, y)
⊢ (f.sym2Map : (a : Sym2 V) → Sym2 W) s(a, b) = s(x, y)

Tactic:
rw [Embedding.sym2Map_apply, Sym2.map_mk, ha, hb]

Premises used: Function.Embedding.sym2Map_apply, Sym2.map_mk
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
x y : W
e : Sym2 V
hadj : e ∈ G.edgeSet
he : (f.sym2Map : (a : Sym2 V) → Sym2 W) e = s(x, y)
h :
  ∀ (x_1 y_1 : V) (hadj : s(x_1, y_1) ∈ G.edgeSet) (he : (f.sym2Map : (a : Sym2 V) → Sym2 W) s(x_1, y_1) = s(x, y)),
    ∃ (u' : V) (v' : V), G.Adj u' v' ∧ (f : (a : V) → W) u' = x ∧ (f : (a : V) → W) v' = y
⊢ ∃ (u' : V) (v' : V), G.Adj u' v' ∧ (f : (a : V) → W) u' = x ∧ (f : (a : V) → W) v' = y

Tactic:
induction e
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
x y : W
x_1 y_1 : V
hadj : s(x_1, y_1) ∈ G.edgeSet
he : (f.sym2Map : (a : Sym2 V) → Sym2 W) s(x_1, y_1) = s(x, y)
⊢ (f : (a : V) → W) x_1 = x ∧ (f : (a : V) → W) y_1 = y ∨ (f : (a : V) → W) x_1 = y ∧ (f : (a : V) → W) y_1 = x

Tactic:
rw [Embedding.sym2Map_apply, Sym2.map_mk, Sym2.eq_iff] at he

Premises used: Function.Embedding.sym2Map_apply, Sym2.map_mk, Sym2.eq_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
x y : W
x_1 y_1 : V
hadj : s(x_1, y_1) ∈ G.edgeSet
he : (f : (a : V) → W) x_1 = x ∧ (f : (a : V) → W) y_1 = y ∨ (f : (a : V) → W) x_1 = y ∧ (f : (a : V) → W) y_1 = x
⊢ ∃ (u' : V) (v' : V), G.Adj u' v' ∧ (f : (a : V) → W) u' = x ∧ (f : (a : V) → W) v' = y

Tactic:
he.elim (fun ⟨h, h'⟩ ↦ ⟨_, _, hadj, h, h'⟩) (fun ⟨h', h⟩ ↦ ⟨_, _, hadj.symm, h, h'⟩)

Premises used: SimpleGraph.Adj.symm, SimpleGraph.Adj, Exists, Prod.mk, _private.0.SimpleGraph.edgeSet_map.match_4, Prod.fst, And, _private.0.SimpleGraph.edgeSet_map.match_3, And.intro, Exists.intro, Or.elim, Eq, Prod.snd, DFunLike.coe
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
x y : W
x_1 y_1 : V
hadj : s(x_1, y_1) ∈ G.edgeSet
he : (f : (a : V) → W) x_1 = x ∧ (f : (a : V) → W) y_1 = y ∨ (f : (a : V) → W) x_1 = y ∧ (f : (a : V) → W) y_1 = x
⊢ ∃ (u' : V) (v' : V), G.Adj u' v' ∧ (f : (a : V) → W) u' = x ∧ (f : (a : V) → W) v' = y

Tactic:
exact he.elim (fun ⟨h, h'⟩ ↦ ⟨_, _, hadj, h, h'⟩) (fun ⟨h', h⟩ ↦ ⟨_, _, hadj.symm, h, h'⟩)

Premises used: Or.elim
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
f : V ↪ W
v : V
⊢ Eq.{u_2 + 1} (α := Set W) (neighborSet (SimpleGraph.map (⇑f : (a : V) → W) G) ((f : (a : V) → W) v) : Set W)
    ((⇑f : (a : V) → W) '' G.neighborSet v : Set W)

Tactic:
Set.ext fun u ↦ ⟨?_, ?_⟩

Premises used: Set.ext, Iff.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
f : V ↪ W
v : V
refine_1 :
  ∀ (u : W),
    Membership.mem (γ := Set W) (neighborSet (SimpleGraph.map (⇑f : (a : V) → W) G) ((f : (a : V) → W) v) : Set W) u →
      Membership.mem (γ := Set W) ((⇑f : (a : V) → W) '' G.neighborSet v) u
refine_2 :
  ∀ (u : W),
    Membership.mem (γ := Set W) ((⇑f : (a : V) → W) '' G.neighborSet v) u →
      Membership.mem (γ := Set W) (neighborSet (SimpleGraph.map (⇑f : (a : V) → W) G) ((f : (a : V) → W) v) : Set W) u
⊢ Eq.{u_2 + 1} (α := Set W) (neighborSet (SimpleGraph.map (⇑f : (a : V) → W) G) ((f : (a : V) → W) v) : Set W)
    ((⇑f : (a : V) → W) '' G.neighborSet v : Set W)

Tactic:
refine Set.ext fun u ↦ ⟨?_, ?_⟩

Premises used: Set.ext, Iff.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
f : V ↪ W
v : V
u : W
⊢ Membership.mem (γ := Set W) (neighborSet (SimpleGraph.map (⇑f : (a : V) → W) G) ((f : (a : V) → W) v) : Set W) u →
    Membership.mem (γ := Set W) ((⇑f : (a : V) → W) '' G.neighborSet v) u

Tactic:
fun ⟨hne, v', u', hadj, hv, hu⟩ ↦ ⟨u', f.injective hv ▸ hadj, hu⟩

Premises used: Membership.mem, SimpleGraph.neighborSet, Eq.rec, And.intro, Exists.intro, Function.Embedding.injective, Set.image, _private.0.SimpleGraph.neighborSet_map.match_1, DFunLike.coe
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
f : V ↪ W
v : V
u : W
⊢ Membership.mem (γ := Set W) (neighborSet (SimpleGraph.map (⇑f : (a : V) → W) G) ((f : (a : V) → W) v) : Set W) u →
    Membership.mem (γ := Set W) ((⇑f : (a : V) → W) '' G.neighborSet v) u

Tactic:
exact fun ⟨hne, v', u', hadj, hv, hu⟩ ↦ ⟨u', f.injective hv ▸ hadj, hu⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
f : V ↪ W
v : V
u : W
⊢ Membership.mem (γ := Set W) ((⇑f : (a : V) → W) '' G.neighborSet v) u →
    Membership.mem (γ := Set W) (neighborSet (SimpleGraph.map (⇑f : (a : V) → W) G) ((f : (a : V) → W) v) : Set W) u

Tactic:
fun ⟨u', hadj, hu⟩ ↦ ⟨hu ▸ f.injective.ne hadj.ne, v, u', hadj, rfl, hu⟩

Premises used: SimpleGraph.Adj.ne, Function.Injective.ne, Membership.mem, SimpleGraph.neighborSet, Eq.rec, _private.0.SimpleGraph.neighborSet_map.match_2, And.intro, Exists.intro, Function.Embedding.injective, DFunLike.coe, rfl, SimpleGraph.map
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
f : V ↪ W
v : V
u : W
⊢ Membership.mem (γ := Set W) ((⇑f : (a : V) → W) '' G.neighborSet v) u →
    Membership.mem (γ := Set W) (neighborSet (SimpleGraph.map (⇑f : (a : V) → W) G) ((f : (a : V) → W) v) : Set W) u

Tactic:
exact fun ⟨u', hadj, hu⟩ ↦ ⟨hu ▸ f.injective.ne hadj.ne, v, u', hadj, rfl, hu⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
f : V ↪ W
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
G : SimpleGraph V
u v : V
f : V → W
hadj : G.Adj u v
hne : f u ≠ f v
⊢ (SimpleGraph.map f G).Adj (f u) (f v)

Tactic:
⟨hne, u, v, hadj, rfl, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
f : V → W
G G' : SimpleGraph V
h : G ≤ G'
u v : V
ha : G.Adj u v
huv : f u ≠ f v
⊢ (SimpleGraph.map f G').Adj (f u) (f v)

Tactic:
⟨huv, _, _, h ha, rfl, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
f : V → W
G G' : SimpleGraph V
h : G ≤ G'
u v : V
ha : G.Adj u v
huv : f u ≠ f v
⊢ (SimpleGraph.map f G').Adj (f u) (f v)

Tactic:
exact ⟨huv, _, _, h ha, rfl, rfl⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
G : SimpleGraph V
Adj : ∀ (x x_1 : V), (SimpleGraph.map id G).Adj x x_1 ↔ G.Adj x x_1
⊢ SimpleGraph.map id G = G

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
G : SimpleGraph V
x x_1 : V
Adj : (¬x = x_1 ∧ ∃ (a : V) (b : V), G.Adj a b ∧ a = x ∧ b = x_1) ↔ G.Adj x x_1
⊢ (SimpleGraph.map id G).Adj x x_1 ↔ G.Adj x x_1

Tactic:
dsimp [SimpleGraph.map, Relation.Map]

Premises used: SimpleGraph.map, Relation.Map
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
G : SimpleGraph V
x x_1 : V
⊢ (¬x = x_1 ∧ ∃ (a : V) (b : V), G.Adj a b ∧ a = x ∧ b = x_1) ↔ G.Adj x x_1

Tactic:
grind [SimpleGraph.Adj.ne]

Premises used: SimpleGraph.Adj.ne
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
X : Type u_3
G : SimpleGraph V
f : V → W
g : W → X
Adj : ∀ (x x_1 : X), (SimpleGraph.map g (SimpleGraph.map f G)).Adj x x_1 ↔ (SimpleGraph.map (g ∘ f) G).Adj x x_1
⊢ SimpleGraph.map g (SimpleGraph.map f G) = SimpleGraph.map (g ∘ f) G

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
X : Type u_3
G : SimpleGraph V
f : V → W
g : W → X
x x_1 : X
Adj :
  (¬x = x_1 ∧
      ∃ (a : W) (b : W),
        (¬a = b ∧ ∃ (a_1 : V) (b_1 : V), G.Adj a_1 b_1 ∧ f a_1 = a ∧ f b_1 = b) ∧ g a = x ∧ g b = x_1) ↔
    ¬x = x_1 ∧ ∃ (a : V) (b : V), G.Adj a b ∧ g (f a) = x ∧ g (f b) = x_1
⊢ (SimpleGraph.map g (SimpleGraph.map f G)).Adj x x_1 ↔ (SimpleGraph.map (g ∘ f) G).Adj x x_1

Tactic:
dsimp [SimpleGraph.map, Relation.Map]

Premises used: SimpleGraph.map, Relation.Map
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
X : Type u_3
G : SimpleGraph V
f : V → W
g : W → X
x x_1 : X
⊢ (¬x = x_1 ∧
      ∃ (a : W) (b : W),
        (¬a = b ∧ ∃ (a_1 : V) (b_1 : V), G.Adj a_1 b_1 ∧ f a_1 = a ∧ f b_1 = b) ∧ g a = x ∧ g b = x_1) ↔
    ¬x = x_1 ∧ ∃ (a : V) (b : V), G.Adj a b ∧ g (f a) = x ∧ g (f b) = x_1

Tactic:
grind [SimpleGraph.Adj.ne]

Premises used: SimpleGraph.Adj.ne
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
h :
  ∀ (x : W),
    Membership.mem (γ := Set W) (support (SimpleGraph.map (⇑f : (a : V) → W) G)) x ↔
      Membership.mem (γ := Set W) ((⇑f : (a : V) → W) '' G.support) x
⊢ Eq.{u_2 + 1} (α := Set W) (support (SimpleGraph.map (⇑f : (a : V) → W) G)) ((⇑f : (a : V) → W) '' G.support)

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
x : W
⊢ Membership.mem (γ := Set W) (support (SimpleGraph.map (⇑f : (a : V) → W) G)) x ↔
    Membership.mem (γ := Set W) ((⇑f : (a : V) → W) '' G.support) x

Tactic:
simp [mem_support]

Premises used: SimpleGraph.mem_support
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
u v : V
G : SimpleGraph W
f : V → W
⊢ (SimpleGraph.comap f G).Adj u v ↔ G.Adj (f u) (f v)

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
G : SimpleGraph V
⊢ SimpleGraph.comap id G = G

Tactic:
SimpleGraph.ext rfl

Premises used: SimpleGraph.ext, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
X : Type u_3
G : SimpleGraph X
f : V → W
g : W → X
⊢ SimpleGraph.comap f (SimpleGraph.comap g G) = SimpleGraph.comap (g ∘ f) G

Tactic:
rfl

Premises used: SimpleGraph.comap, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
f : V → W
G : SimpleGraph W
⊢ (SimpleGraph.comap f G).support ⊆ f ⁻¹' G.support

Tactic:
fun _ ⟨v, h⟩ ↦ ⟨f v, h⟩

Premises used: Membership.mem, _private.0.SimpleGraph.support_comap_subset.match_1, Set.Subset, Set.preimage, SimpleGraph.support, Exists.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
e : V ≃ W
Adj :
  ∀ (x x_1 : W),
    SimpleGraph.Adj (SimpleGraph.comap (⇑e.symm.toEmbedding : (a : W) → V) G) x x_1 ↔
      SimpleGraph.Adj (SimpleGraph.map (⇑e.toEmbedding : (a : V) → W) G) x x_1
⊢ Eq.{u_2 + 1} (α := SimpleGraph W) (SimpleGraph.comap (⇑e.symm.toEmbedding : (a : W) → V) G)
    (SimpleGraph.map (⇑e.toEmbedding : (a : V) → W) G)

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
e : V ≃ W
x x_1 : W
⊢ Adj (SimpleGraph.comap (⇑e.symm.toEmbedding : (a : W) → V) G) x x_1 ↔
    Adj (SimpleGraph.map (⇑e.toEmbedding : (a : V) → W) G) x x_1

Tactic:
simp only [Equiv.apply_eq_iff_eq_symm_apply, comap_adj, map_adj, Equiv.toEmbedding_apply,
    exists_eq_right_right, exists_eq_right]

Premises used: exists_eq_right_right, Equiv.toEmbedding_apply, exists_eq_right, SimpleGraph.map_adj, SimpleGraph.comap_adj, Equiv.apply_eq_iff_eq_symm_apply
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph W
e : V ≃ W
rw :
  Eq.{u_1 + 1} (α := SimpleGraph V) (SimpleGraph.comap (⇑e.symm.symm.toEmbedding : (a : V) → W) G)
    (SimpleGraph.comap (⇑e.toEmbedding : (a : V) → W) G)
rw₁ rw₂ :
  Eq.{u_1 + 1} (α := SimpleGraph V) (SimpleGraph.comap (⇑e.toEmbedding : (a : V) → W) G)
    (SimpleGraph.comap (⇑e.toEmbedding : (a : V) → W) G)
⊢ Eq.{u_1 + 1} (α := SimpleGraph V) (SimpleGraph.map (⇑e.symm.toEmbedding : (a : W) → V) G)
    (SimpleGraph.comap (⇑e.toEmbedding : (a : V) → W) G)

Tactic:
rw [← comap_symm, e.symm_symm]

Premises used: Equiv.symm_symm, SimpleGraph.comap_symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
f : V ↪ W
⊢ Monotone.{u_2, u_1} (α := SimpleGraph W) (β := SimpleGraph V) (SimpleGraph.comap (⇑f : (a : V) → W))

Tactic:
fun _ _ h _ _ ha ↦ h ha

Premises used: Monotone
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
f : V → W
⊢ SimpleGraph.comap f (emptyGraph W) = emptyGraph V

Tactic:
rfl

Premises used: SimpleGraph.comap, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
f : V → W
hf : Injective f
Adj : ∀ (x x_1 : V), (SimpleGraph.comap f (completeGraph W)).Adj x x_1 ↔ (completeGraph V).Adj x x_1
⊢ SimpleGraph.comap f (completeGraph W) = completeGraph V

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
f : V → W
hf : Injective f
x x_1 : V
⊢ (SimpleGraph.comap f (completeGraph W)).Adj x x_1 ↔ (completeGraph V).Adj x x_1

Tactic:
simp [hf.eq_iff]

Premises used: Function.Injective.eq_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
Adj :
  ∀ (x x_1 : V),
    SimpleGraph.Adj (SimpleGraph.comap.{u_1, u_2} (W := W) (⇑f : (a : V) → W) (SimpleGraph.map (⇑f : (a : V) → W) G)) x
        x_1 ↔
      G.Adj x x_1
⊢ SimpleGraph.comap.{u_1, u_2} (W := W) (⇑f : (a : V) → W) (SimpleGraph.map (⇑f : (a : V) → W) G) = G

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

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
f : V ↪ W
⊢ LeftInverse.{u_1 + 1, u_2 + 1} (α := SimpleGraph V) (β := SimpleGraph W) (SimpleGraph.comap (⇑f : (a : V) → W))
    (SimpleGraph.map (⇑f : (a : V) → W))

Tactic:
comap_map_eq f

Premises used: Function.LeftInverse, SimpleGraph.comap_map_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
f : V ↪ W
⊢ Injective.{u_1 + 1, u_2 + 1} (α := SimpleGraph V) (β := SimpleGraph W) (SimpleGraph.map (⇑f : (a : V) → W))

Tactic:
(leftInverse_comap_map f).injective

Premises used: Function.LeftInverse.injective, SimpleGraph.leftInverse_comap_map
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
f : V ↪ W
⊢ Surjective.{u_2 + 1, u_1 + 1} (α := SimpleGraph W) (β := SimpleGraph V) (SimpleGraph.comap (⇑f : (a : V) → W))

Tactic:
(leftInverse_comap_map f).surjective

Premises used: SimpleGraph.leftInverse_comap_map, Function.LeftInverse.surjective
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
G' : SimpleGraph W
h : G ≤ SimpleGraph.comap (⇑f : (a : V) → W) G'
u v : V
ha : G.Adj u v
⊢ G'.Adj ((f : (a : V) → W) u) ((f : (a : V) → W) v)

Tactic:
h ha
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
G' : SimpleGraph W
h : G ≤ SimpleGraph.comap (⇑f : (a : V) → W) G'
u v : V
ha : G.Adj u v
⊢ G'.Adj ((f : (a : V) → W) u) ((f : (a : V) → W) v)

Tactic:
exact h ha
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph W
rw rw₁ :
  LE.le.{u_1} (α := SimpleGraph V) (SimpleGraph.comap (⇑f : (a : V) → W) G) (SimpleGraph.comap (⇑f : (a : V) → W) G)
⊢ SimpleGraph.map.{u_1, u_2} (V := V) (⇑f : (a : V) → W) (SimpleGraph.comap (⇑f : (a : V) → W) G) ≤ G

Tactic:
rw [map_le_iff_le_comap]

Premises used: SimpleGraph.map_le_iff_le_comap
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : V → W
inst : Subsingleton V
v w : V
⊢ G.Adj v w → (SimpleGraph.comap f G').Adj v w

Tactic:
simp [Subsingleton.elim v w]

Premises used: Subsingleton.elim
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : V ↪ W
inst : Subsingleton V
rw : G ≤ SimpleGraph.comap (⇑f : (a : V) → W) G'
⊢ SimpleGraph.map (⇑f : (a : V) → W) G ≤ G'

Tactic:
rw [map_le_iff_le_comap]

Premises used: SimpleGraph.map_le_iff_le_comap
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : V ↪ W
inst : Subsingleton V
⊢ G ≤ SimpleGraph.comap (⇑f : (a : V) → W) G'

Tactic:
apply le_comap_of_subsingleton

Premises used: SimpleGraph.le_comap_of_subsingleton
-- 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
e : V ≃ W
x : SimpleGraph V
⊢ SimpleGraph.comap.{u_1, u_2} (W := W) (⇑e : (a : V) → W) (SimpleGraph.comap (⇑e.symm : (a : W) → V) x) = x

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 : V
e : V ≃ W
x : SimpleGraph W
⊢ SimpleGraph.comap.{u_2, u_1} (W := V) (⇑e.symm : (a : W) → V) (SimpleGraph.comap (⇑e : (a : V) → W) x) = x

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
H :
  ∀ (x : SimpleGraph V) (x_1 x_2 : V),
    Adj (((Equiv.refl V).simpleGraph : (a : SimpleGraph V) → SimpleGraph V) x) x_1 x_2 ↔
      Adj ((Equiv.refl (SimpleGraph V) : (a : SimpleGraph V) → SimpleGraph V) x) x_1 x_2
⊢ (Equiv.refl V).simpleGraph = Equiv.refl (SimpleGraph V)

Tactic:
ext
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
x : SimpleGraph V
x_1 x_2 : V
⊢ Adj (((Equiv.refl V).simpleGraph : (a : SimpleGraph V) → SimpleGraph V) x) x_1 x_2 ↔
    Adj ((Equiv.refl (SimpleGraph V) : (a : SimpleGraph V) → SimpleGraph V) x) x_1 x_2

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
X : Type u_3
e₁ : V ≃ W
e₂ : W ≃ X
⊢ (e₁.trans e₂).simpleGraph = e₁.simpleGraph.trans e₂.simpleGraph

Tactic:
rfl

Premises used: Equiv.trans, SimpleGraph.comap, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
e : V ≃ W
⊢ e.simpleGraph.symm = e.symm.simpleGraph

Tactic:
rfl

Premises used: SimpleGraph.comap, Equiv.symm, Equiv.simpleGraph, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
G : SimpleGraph V
s : Set V
u v : (↑s : Type u_1)
⊢ (induce s G).Adj u v ↔ G.Adj (↑u : V) (↑v : V)

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
s : Set V
⊢ induce s (completeGraph V) = completeGraph (↑s : Type u_1)

Tactic:
comap_top Subtype.val_injective

Premises used: Subtype.val_injective, SimpleGraph.comap_top
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
s : Set V
⊢ induce s ⊥ = ⊥

Tactic:
dsimp
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
G : SimpleGraph V
s : Set V
⊢ (induce s G).support ⊆ Subtype.val (p := fun (x : V) ↦ x ∈ s) ⁻¹' s

Tactic:
fun v _ ↦ v.prop

Premises used: Set.Mem, setOf, Set.Subset, Set.preimage, Subtype.prop
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
G : SimpleGraph V
s : Set V
⊢ (induce s G).support ⊆ Subtype.val (p := fun (x : V) ↦ x ∈ s) ⁻¹' G.support

Tactic:
fun _ ⟨v, hadj⟩ ↦ ⟨v, hadj⟩

Premises used: Membership.mem, Set.Subset, Set.preimage, SimpleGraph.support, Exists.intro, _private.0.SimpleGraph.support_induce_subset_coe_preimage_support.match_1, Subtype.val
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
G : SimpleGraph V
v : V
rw : LE.le (α := SimpleGraph (↑{v} : Type u_1)) ⊤ (induce {v} G)
⊢ Eq (α := SimpleGraph (↑{v} : Type u_1)) (induce {v} G) ⊤

Tactic:
rw [eq_top_iff]

Premises used: eq_top_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
G : SimpleGraph V
v : V
⊢ LE.le (α := SimpleGraph (↑{v} : Type u_1)) ⊤ (induce {v} G)

Tactic:
apply le_comap_of_subsingleton

Premises used: SimpleGraph.le_comap_of_subsingleton
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
s : Set V
G : SimpleGraph (↑s : Type u_1)
⊢ G.spanningCoe (s := s).support = Subtype.val (p := fun (x : V) ↦ x ∈ s) '' G.support

Tactic:
G.support_map _

Premises used: SimpleGraph.support_map
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
s : Set V
G : SimpleGraph (↑s : Type u_1)
⊢ induce s (G.spanningCoe (s := s)) = G

Tactic:
comap_map_eq _ _

Premises used: SimpleGraph.comap_map_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
G : SimpleGraph V
s : Set V
⊢ (induce s G).spanningCoe (s := s) ≤ G

Tactic:
map_comap_le _ _

Premises used: SimpleGraph.map_comap_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
G : SimpleGraph V
s : Set V
⊢ (induce s G).spanningCoe (s := s) = G ↔ G.support ⊆ s

Tactic:
⟨fun h v hv ↦ ?_, fun h ↦ le_antisymm (G.spanningCoe_induce_le s) fun u v hadj ↦ ?_⟩

Premises used: SimpleGraph.spanningCoe_induce_le, le_antisymm, Iff.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
G : SimpleGraph V
s : Set V
refine_1 : ∀ (h : (induce s G).spanningCoe (s := s) = G) (v : V) (hv : v ∈ G.support), v ∈ s
refine_2 : ∀ (h : G.support ⊆ s) (u v : V) (hadj : G.Adj u v), (induce s G).spanningCoe (s := s).Adj u v
⊢ (induce s G).spanningCoe (s := s) = G ↔ G.support ⊆ s

Tactic:
refine ⟨fun h v hv ↦ ?_, fun h ↦ le_antisymm (G.spanningCoe_induce_le s) fun u v hadj ↦ ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
G : SimpleGraph V
s : Set V
h : (induce s G).spanningCoe (s := s) = G
v : V
hv : v ∈ G.support
⊢ v ∈ Subtype.val (p := fun (x : V) ↦ x ∈ s) '' (induce s G).support

Tactic:
rw [← h, support_spanningCoe] at hv

Premises used: SimpleGraph.support_spanningCoe
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
G : SimpleGraph V
s : Set V
h : (induce s G).spanningCoe (s := s) = G
v : V
hv : v ∈ Subtype.val (p := fun (x : V) ↦ x ∈ s) '' (induce s G).support
refine_1 : ∀ u ∈ (induce s G).support, ∀ (hvu : (↑u : V) = v), v ∈ s
⊢ v ∈ s

Tactic:
have ⟨u, _, hvu⟩ := hv
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
G : SimpleGraph V
s : Set V
h : (induce s G).spanningCoe (s := s) = G
v : V
hv : v ∈ Subtype.val (p := fun (x : V) ↦ x ∈ s) '' (induce s G).support
u : (↑s : Type u_1)
left : u ∈ (induce s G).support
hvu : (↑u : V) = v
⊢ v ∈ s

Tactic:
hvu ▸ u.prop

Premises used: Eq.rec, Subtype.prop
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
G : SimpleGraph V
s : Set V
h : (induce s G).spanningCoe (s := s) = G
v : V
hv : v ∈ Subtype.val (p := fun (x : V) ↦ x ∈ s) '' (induce s G).support
u : (↑s : Type u_1)
left : u ∈ (induce s G).support
hvu : (↑u : V) = v
⊢ v ∈ s

Tactic:
exact hvu ▸ u.prop
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
G : SimpleGraph V
s : Set V
h : G.support ⊆ s
u v : V
hadj : G.Adj u v
⊢ (induce s G).spanningCoe (s := s).Adj u v

Tactic:
⟨hadj.ne, ⟨u, h hadj.left_mem_support⟩, ⟨v, h hadj.right_mem_support⟩, hadj, rfl, rfl⟩

Premises used: SimpleGraph.Adj.ne, SimpleGraph.Adj.right_mem_support, Subtype.mk, And.intro, Exists.intro, SimpleGraph.Adj.left_mem_support, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
G : SimpleGraph V
s : Set V
h : G.support ⊆ s
u v : V
hadj : G.Adj u v
⊢ (induce s G).spanningCoe (s := s).Adj u v

Tactic:
exact ⟨hadj.ne, ⟨u, h hadj.left_mem_support⟩, ⟨v, h hadj.right_mem_support⟩, hadj, rfl, rfl⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
G : SimpleGraph V
⊢ (induce G.support G).spanningCoe (s := G.support) = G

Tactic:
G.spanningCoe_induce_eq_self _ |>.mpr .rfl

Premises used: Iff.mpr, Set.Subset.rfl, SimpleGraph.spanningCoe_induce_eq_self