awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
s : Set V
t : Set W
r : Set X
φ : G →g G'
φst : Set.MapsTo (⇑φ : (a : V) → W) s t
ψ : G' →g G''
ψtr : Set.MapsTo (⇑ψ : (a : W) → X) t r
h :
  ∀ (x : (↑s : Type u_1)),
    Eq.{u_3 + 1} (α := X)
      (↑(((induceHom (s := t) (t := r) ψ ψtr).comp (induceHom (s := s) (t := t) φ φst) :
              (a : (↑s : Type u_1)) → (↑r : Type u_3))
            x) :
        X)
      (↑((induceHom (s := s) (t := r) (ψ.comp φ) ⋯ : (a : (↑s : Type u_1)) → (↑r : Type u_3)) x) : X)
⊢ (induceHom (s := t) (t := r) ψ ψtr).comp (induceHom (s := s) (t := t) φ φst) =
    induceHom (s := s) (t := r) (ψ.comp φ) ⋯

Tactic:
ext x
-- 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
s : Set V
t : Set W
r : Set X
φ : G →g G'
φst : Set.MapsTo (⇑φ : (a : V) → W) s t
ψ : G' →g G''
ψtr : Set.MapsTo (⇑ψ : (a : W) → X) t r
x : (↑s : Type u_1)
⊢ Eq.{u_3 + 1} (α := X)
    (↑(((induceHom (s := t) (t := r) ψ ψtr).comp (induceHom (s := s) (t := t) φ φst) :
            (a : (↑s : Type u_1)) → (↑r : Type u_3))
          x) :
      X)
    (↑((induceHom (s := s) (t := r) (ψ.comp φ) ⋯ : (a : (↑s : Type u_1)) → (↑r : Type u_3)) x) : X)

Tactic:
rfl
-- 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
hi : Set.InjOn.{u_1, u_2} (β := W) (⇑φ : (a : V) → W) s
⊢ Injective.{u_1 + 1, u_2 + 1} (α := (↑s : Type u_1)) (β := (↑t : Type u_2))
    (⇑(induceHom (s := s) (t := t) φ φst) : (a : (↑s : Type u_1)) → (↑t : Type u_2))

Tactic:
simpa [Set.MapsTo.restrict_inj]

Premises used: Set.MapsTo.restrict_inj
-- 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
s s' : Set V
h_1 h : s ≤ s'
⊢ ∀ {a b : (↑s : Type u_1)},
    (induce s' G).Adj ((s.embeddingOfSubset s' h : (a : (↑s : Type u_1)) → (↑s' : Type u_1)) a)
        ((s.embeddingOfSubset s' h : (a : (↑s : Type u_1)) → (↑s' : Type u_1)) b) ↔
      (induce s G).Adj a b

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
G : SimpleGraph V
s s' : Set V
h : s ≤ s'
v : (↑s : Type u_1)
⊢ (G.induceHomOfLE (s := s) (s' := s') h : (a : (↑s : Type u_1)) → (↑s' : Type u_1)) v =
    Set.inclusion (s := s) (t := s') h v

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
G : SimpleGraph V
s s' : Set V
h : s ≤ s'
h₁ :
  ∀ (x : (↑s : Type u_1)),
    Eq.{u_1 + 1} (α := V)
      (↑(((G.induceHomOfLE (s := s) (s' := s') h).toHom : (a : (↑s : Type u_1)) → (↑s' : Type u_1)) x) : V)
      (↑((induceHom (s := s) (t := s') Hom.id ⋯ : (a : (↑s : Type u_1)) → (↑s' : Type u_1)) x) : V)
⊢ (G.induceHomOfLE (s := s) (s' := s') h).toHom = induceHom (s := s) (t := s') Hom.id ⋯

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

Tactic:
simp
-- 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: RelIso.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'
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: SimpleGraph.Iso.map_adj_iff, Set.Mem, 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'
rw :
  Set.image.{u_1, u_2} (α := V) (⇑f : (a : V) → W)
      ((⇑f.toEmbedding : (a : V) → W) ⁻¹' G'.neighborSet ((f.toEmbedding : (a : V) → W) v)) =
    G'.neighborSet ((f : (a : V) → W) v)
⊢ (⇑f : (a : V) → W) '' G.neighborSet v = G'.neighborSet ((f : (a : V) → W) v)

Tactic:
rw [← f.toEmbedding.preimage_neighborSet]

Premises used: SimpleGraph.Iso.toEmbedding, SimpleGraph.Embedding.preimage_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'
⊢ Set.image.{u_1, u_2} (α := V) (⇑f : (a : V) → W)
      ((⇑f.toEmbedding : (a : V) → W) ⁻¹' G'.neighborSet ((f.toEmbedding : (a : V) → W) v)) =
    G'.neighborSet ((f : (a : V) → W) v)

Tactic:
apply Equiv.image_preimage

Premises used: Equiv.image_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'
h : ∀ (v : V), Eq (α := V) ((f.symm.toHom.comp f.toHom : (a : V) → V) v : V) ((Hom.id : (a : V) → V) v : V)
⊢ f.symm.toHom.comp f.toHom = Hom.id

Tactic:
ext v
-- 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 : V
⊢ Eq (α := V) ((f.symm.toHom.comp f.toHom : (a : V) → V) v : V) ((Hom.id : (a : V) → V) v : V)

Tactic:
simp only [RelHom.comp_apply, RelEmbedding.coe_toRelHom, RelIso.coe_toRelEmbedding,
    RelIso.symm_apply_apply, RelHom.id_apply]

Premises used: RelEmbedding.coe_toRelHom, RelIso.symm_apply_apply, RelHom.comp_apply, RelIso.coe_toRelEmbedding, RelHom.id_apply
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : G ≃g G'
h : ∀ (v : W), Eq (α := W) ((f.toHom.comp f.symm.toHom : (a : W) → W) v : W) ((Hom.id : (a : W) → W) v : W)
⊢ f.toHom.comp f.symm.toHom = Hom.id

Tactic:
ext v
-- 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
⊢ Eq (α := W) ((f.toHom.comp f.symm.toHom : (a : W) → W) v : W) ((Hom.id : (a : W) → W) v : W)

Tactic:
simp only [RelHom.comp_apply, RelEmbedding.coe_toRelHom, RelIso.coe_toRelEmbedding,
    RelIso.apply_symm_apply, RelHom.id_apply]

Premises used: RelEmbedding.coe_toRelHom, RelIso.apply_symm_apply, RelHom.comp_apply, RelIso.coe_toRelEmbedding, RelHom.id_apply
-- 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
f : G ≃g G'
e : Sym2 V
h : e ∈ G.edgeSet
simp :
  Sym2.map
      (fun (x : V) ↦
        (RelHom.mk (r := G'.Adj) (s := G.Adj) (⇑(f.symm.toEquiv (r := G'.Adj) (s := G.Adj)) : (a : W) → V) ⋯ :
            (a : W) → V)
          ((RelHom.mk (r := G.Adj) (s := G'.Adj) (⇑(f.toEquiv (r := G.Adj) (s := G'.Adj)) : (a : V) → W) ⋯ :
                (a : V) → W)
              x :
            W))
      e =
    e
⊢ Hom.mapEdgeSet ((RelIso.toRelEmbedding (r := G'.Adj) (s := G.Adj) f.symm).toRelHom (r := G'.Adj) (s := G.Adj))
      (Hom.mapEdgeSet ((RelIso.toRelEmbedding (r := G.Adj) (s := G'.Adj) f).toRelHom (r := G.Adj) (s := G'.Adj))
        (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:
simp only [Hom.mapEdgeSet, RelEmbedding.toRelHom, Sym2.map_map, comp_apply, Subtype.mk.injEq]

Premises used: SimpleGraph.Hom.mapEdgeSet, Sym2.map_map, Subtype.mk.injEq, Function.comp_apply, RelEmbedding.toRelHom
-- 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
f : G ≃g G'
e : Sym2 V
h : e ∈ G.edgeSet
⊢ Sym2.map id e = id e

Tactic:
congr_fun Sym2.map_id e

Premises used: Sym2.map_id, congr_fun
-- 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
f : G ≃g G'
e : Sym2 V
h : e ∈ G.edgeSet
h₁ :
  ∀ x ∈ e,
    (RelHom.mk (r := G'.Adj) (s := G.Adj) (⇑(f.symm.toEquiv (r := G'.Adj) (s := G.Adj)) : (a : W) → V) ⋯ : (a : W) → V)
        ((RelHom.mk (r := G.Adj) (s := G'.Adj) (⇑(f.toEquiv (r := G.Adj) (s := G'.Adj)) : (a : V) → W) ⋯ : (a : V) → W)
            x :
          W) =
      id x
⊢ Sym2.map
      (fun (x : V) ↦
        (RelHom.mk (r := G'.Adj) (s := G.Adj) (⇑(f.symm.toEquiv (r := G'.Adj) (s := G.Adj)) : (a : W) → V) ⋯ :
            (a : W) → V)
          ((RelHom.mk (r := G.Adj) (s := G'.Adj) (⇑(f.toEquiv (r := G.Adj) (s := G'.Adj)) : (a : V) → W) ⋯ :
                (a : V) → W)
              x :
            W))
      e =
    e

Tactic:
convert! congr_fun Sym2.map_id e

Premises used: Sym2.map_id, congr_fun
-- 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
f : G ≃g G'
e : Sym2 V
h : e ∈ G.edgeSet
x : V
h_1 : x ∈ e
⊢ (RelHom.mk (r := G'.Adj) (s := G.Adj) (⇑(f.symm.toEquiv (r := G'.Adj) (s := G.Adj)) : (a : W) → V) ⋯ : (a : W) → V)
      ((RelHom.mk (r := G.Adj) (s := G'.Adj) (⇑(f.toEquiv (r := G.Adj) (s := G'.Adj)) : (a : V) → W) ⋯ : (a : V) → W)
          x :
        W) =
    id x

Tactic:
RelIso.symm_apply_apply _ _

Premises used: RelIso.symm_apply_apply
-- 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
f : G ≃g G'
e : Sym2 V
h : e ∈ G.edgeSet
x : V
h_1 : x ∈ e
⊢ (RelHom.mk (r := G'.Adj) (s := G.Adj) (⇑(f.symm.toEquiv (r := G'.Adj) (s := G.Adj)) : (a : W) → V) ⋯ : (a : W) → V)
      ((RelHom.mk (r := G.Adj) (s := G'.Adj) (⇑(f.toEquiv (r := G.Adj) (s := G'.Adj)) : (a : V) → W) ⋯ : (a : V) → W)
          x :
        W) =
    id x

Tactic:
exact RelIso.symm_apply_apply _ _

Premises used: RelIso.symm_apply_apply
-- 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
f : G ≃g G'
e : Sym2 W
h : e ∈ G'.edgeSet
simp :
  Sym2.map
      (fun (x : W) ↦
        (RelHom.mk (r := G.Adj) (s := G'.Adj) (⇑(f.toEquiv (r := G.Adj) (s := G'.Adj)) : (a : V) → W) ⋯ : (a : V) → W)
          ((RelHom.mk (r := G'.Adj) (s := G.Adj) (⇑(f.symm.toEquiv (r := G'.Adj) (s := G.Adj)) : (a : W) → V) ⋯ :
                (a : W) → V)
              x :
            V))
      e =
    e
⊢ Hom.mapEdgeSet ((RelIso.toRelEmbedding (r := G.Adj) (s := G'.Adj) f).toRelHom (r := G.Adj) (s := G'.Adj))
      (Hom.mapEdgeSet ((RelIso.toRelEmbedding (r := G'.Adj) (s := G.Adj) f.symm).toRelHom (r := G'.Adj) (s := G.Adj))
        (Subtype.mk (p := fun (x : Sym2 W) ↦ x ∈ G'.edgeSet) e h)) =
    Subtype.mk (p := fun (x : Sym2 W) ↦ x ∈ G'.edgeSet) e h

Tactic:
simp only [Hom.mapEdgeSet, RelEmbedding.toRelHom, Sym2.map_map, comp_apply, Subtype.mk.injEq]

Premises used: SimpleGraph.Hom.mapEdgeSet, Sym2.map_map, Subtype.mk.injEq, Function.comp_apply, RelEmbedding.toRelHom
-- 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
f : G ≃g G'
e : Sym2 W
h : e ∈ G'.edgeSet
⊢ Sym2.map id e = id e

Tactic:
congr_fun Sym2.map_id e

Premises used: Sym2.map_id, congr_fun
-- 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
f : G ≃g G'
e : Sym2 W
h : e ∈ G'.edgeSet
h₁ :
  ∀ x ∈ e,
    (RelHom.mk (r := G.Adj) (s := G'.Adj) (⇑(f.toEquiv (r := G.Adj) (s := G'.Adj)) : (a : V) → W) ⋯ : (a : V) → W)
        ((RelHom.mk (r := G'.Adj) (s := G.Adj) (⇑(f.symm.toEquiv (r := G'.Adj) (s := G.Adj)) : (a : W) → V) ⋯ :
              (a : W) → V)
            x :
          V) =
      id x
⊢ Sym2.map
      (fun (x : W) ↦
        (RelHom.mk (r := G.Adj) (s := G'.Adj) (⇑(f.toEquiv (r := G.Adj) (s := G'.Adj)) : (a : V) → W) ⋯ : (a : V) → W)
          ((RelHom.mk (r := G'.Adj) (s := G.Adj) (⇑(f.symm.toEquiv (r := G'.Adj) (s := G.Adj)) : (a : W) → V) ⋯ :
                (a : W) → V)
              x :
            V))
      e =
    e

Tactic:
convert! congr_fun Sym2.map_id e

Premises used: Sym2.map_id, congr_fun
-- 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
f : G ≃g G'
e : Sym2 W
h : e ∈ G'.edgeSet
x : W
h_1 : x ∈ e
⊢ (RelHom.mk (r := G.Adj) (s := G'.Adj) (⇑(f.toEquiv (r := G.Adj) (s := G'.Adj)) : (a : V) → W) ⋯ : (a : V) → W)
      ((RelHom.mk (r := G'.Adj) (s := G.Adj) (⇑(f.symm.toEquiv (r := G'.Adj) (s := G.Adj)) : (a : W) → V) ⋯ :
            (a : W) → V)
          x :
        V) =
    id x

Tactic:
RelIso.apply_symm_apply _ _

Premises used: RelIso.apply_symm_apply
-- 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
f : G ≃g G'
e : Sym2 W
h : e ∈ G'.edgeSet
x : W
h_1 : x ∈ e
⊢ (RelHom.mk (r := G.Adj) (s := G'.Adj) (⇑(f.toEquiv (r := G.Adj) (s := G'.Adj)) : (a : V) → W) ⋯ : (a : V) → W)
      ((RelHom.mk (r := G'.Adj) (s := G.Adj) (⇑(f.symm.toEquiv (r := G'.Adj) (s := G.Adj)) : (a : W) → V) ⋯ :
            (a : W) → V)
          x :
        V) =
    id x

Tactic:
exact RelIso.apply_symm_apply _ _

Premises used: RelIso.apply_symm_apply
-- 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
f : G ≃g G'
v : V
w : (↑(G'.neighborSet ((f : (a : V) → W) v)) : Type u_2)
⊢ Membership.mem (α := V) (G.neighborSet v) ((f.symm : (a : W) → V) (↑w : W) : V)

Tactic:
simpa [RelIso.symm_apply_apply] using f.symm.apply_mem_neighborSet_iff.mpr w.2

Premises used: Iff.mpr, SimpleGraph.Iso.apply_mem_neighborSet_iff, RelIso.symm_apply_apply, SimpleGraph.Iso.symm, Subtype.property
-- 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
f : G ≃g G'
v : V
w : (↑(G.neighborSet v) : Type u_1)
⊢ (fun (w : (↑(G'.neighborSet ((f : (a : V) → W) v)) : Type u_2)) ↦
        (Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet v) ((f.symm : (a : W) → V) (↑w : W)) ⋯ :
          { x : V // x ∈ G.neighborSet v }))
      ((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) }))
        w) =
    w

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
f : G ≃g G'
v : V
w : (↑(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) }))
      ((fun (w : (↑(G'.neighborSet ((f : (a : V) → W) v)) : Type u_2)) ↦
          (Subtype.mk (p := fun (x : V) ↦ x ∈ G.neighborSet v) ((f.symm : (a : W) → V) (↑w : W)) ⋯ :
            { x : V // x ∈ G.neighborSet v }))
        w) =
    w

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : G ≃g G'
inst : Fintype V
inst_1 : Fintype W
rw : Fintype.card W = Fintype.card W
⊢ Fintype.card V = Fintype.card W

Tactic:
rw [← Fintype.ofEquiv_card f.toEquiv]

Premises used: Fintype.ofEquiv_card, RelIso.toEquiv
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : G ≃g G'
inst : Fintype V
inst_1 : Fintype W
⊢ Fintype.card W = Fintype.card 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'
inst : Fintype V
inst_1 : Fintype W
⊢ Fintype.card W = Fintype.card W

Tactic:
convert! rfl

Premises used: rfl
-- 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
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.toEmbedding : (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) ((Iso.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
f : V ≃ W
G : SimpleGraph W
w : W
⊢ Eq.{u_1 + 1} (α := V) (((Iso.comap f G).symm : (a : W) → V) w : V) ((f.symm : (a : W) → V) w : V)

Tactic:
rfl

Premises used: rfl
-- 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
f_1 : G_1 ≃g G'
f : V ≃ W
G : SimpleGraph V
⊢ ∀ {a b : V},
    Adj.{u_2} (V := W) (SimpleGraph.map (⇑f.toEmbedding : (a : V) → W) G : SimpleGraph W) ((f : (a : V) → W) a : W)
        ((f : (a : V) → W) b : W) ↔
      G.Adj a b

Tactic:
aesop (add simp map_adj')

Premises used: SimpleGraph.map_adj'
-- 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) ((Iso.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
f : V ≃ W
G : SimpleGraph V
w : W
⊢ Eq.{u_1 + 1} (α := V) (((Iso.map f G).symm : (a : W) → V) w : V) ((f.symm : (a : W) → V) w : V)

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
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 : α ≃ β
⊢ (Iso.completeGraph f).toEmbedding = Embedding.completeGraph f.toEmbedding

Tactic:
rfl

Premises used: SimpleGraph.Embedding.completeGraph, 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
G' : SimpleGraph W
f : V → W
v : V
⊢ (SimpleGraph.comap f G').neighborSet v = f ⁻¹' G'.neighborSet (f v)

Tactic:
rfl

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

Tactic:
G.neighborSet_comap _ v

Premises used: SimpleGraph.neighborSet_comap
-- Module: Mathlib.Combinatorics.SimpleGraph.Maps
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
e : V ≃ W
w : W
⊢ neighborSet (SimpleGraph.map (⇑e : (a : V) → W) G) w =
    (⇑e.symm : (a : W) → V) ⁻¹' G.neighborSet ((e.symm : (a : W) → V) w)

Tactic:
Iso.map e G |>.symm.toEmbedding.preimage_neighborSet w |>.symm

Premises used: SimpleGraph.Iso.toEmbedding, SimpleGraph.Iso.map, SimpleGraph.Embedding.preimage_neighborSet, SimpleGraph.Iso.symm, Eq.symm
-- 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 : SimpleGraph V
⊢ ∀ {a b : (↑Set.univ : Type u_1)},
    G.Adj ((Equiv.Set.univ V : (a : (↑Set.univ : Type u_1)) → V) a)
        ((Equiv.Set.univ V : (a : (↑Set.univ : Type u_1)) → V) b) ↔
      Adj (induce Set.univ G) a b

Tactic:
simp only [Equiv.Set.univ, Equiv.coe_fn_mk, comap_adj, Embedding.coe_subtype,
                                implies_true]

Premises used: Function.Embedding.coe_subtype, SimpleGraph.comap_adj, Equiv.coe_fn_mk, implies_true, Equiv.Set.univ
-- 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
inst : Fintype V
n : ℕ
hc : Fintype.card V = n
x y : Fin n
simp_rw simp_rw₁ :
  G.Adj (((Fintype.equivFinOfCardEq hc).symm : (a : Fin n) → V) x)
      (((Fintype.equivFinOfCardEq hc).symm : (a : Fin n) → V) y) →
    G.Adj (((Fintype.equivFinOfCardEq hc).symm : (a : Fin n) → V) y)
      (((Fintype.equivFinOfCardEq hc).symm : (a : Fin n) → V) x)
simp_rw₂ :
  G.Adj (((Fintype.equivFinOfCardEq hc).symm : (a : Fin n) → V) x)
      (((Fintype.equivFinOfCardEq hc).symm : (a : Fin n) → V) y) →
    G.Adj (((Fintype.equivFinOfCardEq hc).symm : (a : Fin n) → V) x)
      (((Fintype.equivFinOfCardEq hc).symm : (a : Fin n) → V) y)
⊢ (fun (x y : Fin n) ↦
        G.Adj (((Fintype.equivFinOfCardEq hc).symm : (a : Fin n) → V) x)
          (((Fintype.equivFinOfCardEq hc).symm : (a : Fin n) → V) y))
      x y →
    (fun (x y : Fin n) ↦
        G.Adj (((Fintype.equivFinOfCardEq hc).symm : (a : Fin n) → V) x)
          (((Fintype.equivFinOfCardEq hc).symm : (a : Fin n) → V) y))
      y x

Tactic:
simp_rw [adj_comm, imp_self]

Premises used: imp_self, SimpleGraph.adj_comm
-- 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
inst : Fintype V
n : ℕ
hc : Fintype.card V = n
map_rel_iff' :
  ∀ {a b : V},
    (G.overFin hc).Adj ((Fintype.equivFinOfCardEq hc : (a : V) → Fin n) a)
        ((Fintype.equivFinOfCardEq hc : (a : V) → Fin n) b) ↔
      G.Adj a b
⊢ G ≃g G.overFin hc

Tactic:
use Fintype.equivFinOfCardEq hc

Premises used: Fintype.equivFinOfCardEq
-- 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
inst : Fintype V
n : ℕ
hc : Fintype.card V = n
⊢ ∀ {a b : V},
    (G.overFin hc).Adj ((Fintype.equivFinOfCardEq hc : (a : V) → Fin n) a)
        ((Fintype.equivFinOfCardEq hc : (a : V) → Fin n) b) ↔
      G.Adj a b

Tactic:
simp [overFin]

Premises used: SimpleGraph.overFin
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
v w : V
h : M.IsMatching
hvw : M.Adj v w
rw :
  Eq (α := (↑M.edgeSet : Type u_1))
    (Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ M.edgeSet)
      s((↑(Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) v ⋯) : V),
        Exists.choose (p := fun (x : V) ↦
          (fun (w_1 : V) ↦ M.Adj (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) v ⋯) : V) w_1) x ∧
            ∀ (y : V), M.Adj (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) v ⋯) : V) y → y = x)
          ⋯)
      ⋯)
    (Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ M.edgeSet) s(v, w) hvw)
rw₁ :
  s((↑(Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) v ⋯) : V),
      Exists.choose (p := fun (x : V) ↦
        (fun (w_1 : V) ↦ M.Adj (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) v ⋯) : V) w_1) x ∧
          ∀ (y : V), M.Adj (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) v ⋯) : V) y → y = x)
        ⋯) =
    s(v, w)
rw₂ rw₃ : s((↑(Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) v ⋯) : V), w) = s(v, w)
⊢ h.toEdge (Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) v ⋯) =
    Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ M.edgeSet) s(v, w) hvw

Tactic:
rw [IsMatching.toEdge, Subtype.mk_eq_mk, ← h hvw.fst_mem |>.choose_spec.right w hvw]

Premises used: Exists.choose_spec, SimpleGraph.Subgraph.IsMatching.toEdge, And.right, Subtype.mk_eq_mk, SimpleGraph.Subgraph.Adj.fst_mem