awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u : V
p : G.Walk u u
hinj : Injective.{u + 1, v + 1} (α := V) (β := V') (⇑f : (a : V) → V')
rw : (Walk.map f p).IsTrail ∧ Walk.map f p ≠ nil ∧ (Walk.map f p).support.tail.Nodup ↔ p.IsCycle
rw₁ :
  (Walk.map f p).IsTrail ∧ Walk.map f p ≠ nil ∧ (Walk.map f p).support.tail.Nodup ↔
    p.IsTrail ∧ p ≠ nil ∧ p.support.tail.Nodup
rw₂ : p.IsTrail ∧ Walk.map f p ≠ nil ∧ (Walk.map f p).support.tail.Nodup ↔ p.IsTrail ∧ p ≠ nil ∧ p.support.tail.Nodup
rw₃ : p.IsTrail ∧ ¬Walk.map f p = nil ∧ (Walk.map f p).support.tail.Nodup ↔ p.IsTrail ∧ p ≠ nil ∧ p.support.tail.Nodup
rw₄ : p.IsTrail ∧ ¬Walk.map f p = nil ∧ (Walk.map f p).support.tail.Nodup ↔ p.IsTrail ∧ ¬p = nil ∧ p.support.tail.Nodup
rw₅ : p.IsTrail ∧ ¬(Walk.map f p).Nil ∧ (Walk.map f p).support.tail.Nodup ↔ p.IsTrail ∧ ¬p = nil ∧ p.support.tail.Nodup
rw₆ : p.IsTrail ∧ ¬(Walk.map f p).Nil ∧ (Walk.map f p).support.tail.Nodup ↔ p.IsTrail ∧ ¬p.Nil ∧ p.support.tail.Nodup
rw₇ : p.IsTrail ∧ ¬p.Nil ∧ (Walk.map f p).support.tail.Nodup ↔ p.IsTrail ∧ ¬p.Nil ∧ p.support.tail.Nodup
rw₈ :
  p.IsTrail ∧ ¬p.Nil ∧ List.Nodup.{v} (α := V') (List.tail (List.map (⇑f : (a : V) → V') p.support)) ↔
    p.IsTrail ∧ ¬p.Nil ∧ p.support.tail.Nodup
rw₉ :
  p.IsTrail ∧ ¬p.Nil ∧ List.Nodup.{v} (α := V') (List.map (⇑f : (a : V) → V') p.support.tail) ↔
    p.IsTrail ∧ ¬p.Nil ∧ p.support.tail.Nodup
rw₁₀ rw₁₁ : p.IsTrail ∧ ¬p.Nil ∧ p.support.tail.Nodup ↔ p.IsTrail ∧ ¬p.Nil ∧ p.support.tail.Nodup
⊢ (Walk.map f p).IsCycle ↔ p.IsCycle

Tactic:
rw [isCycle_def, isCycle_def, map_isTrail_iff_of_injective hinj, ne_eq, ne_eq, eq_nil_iff_nil,
    eq_nil_iff_nil, nil_map_iff, support_map, ← List.map_tail, List.nodup_map_iff hinj]

Premises used: List.map_tail, SimpleGraph.Walk.isCycle_def, SimpleGraph.Walk.eq_nil_iff_nil, ne_eq, SimpleGraph.Walk.map_isTrail_iff_of_injective, SimpleGraph.Walk.support_map, List.nodup_map_iff, SimpleGraph.Walk.nil_map_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G G' : SimpleGraph V
h : G ≤ G'
u v : V
p : G.Walk u v
⊢ (mapLe h p).IsTrail ↔ p.IsTrail

Tactic:
map_isTrail_iff_of_injective Function.injective_id

Premises used: Function.injective_id, SimpleGraph.Walk.map_isTrail_iff_of_injective
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G G' : SimpleGraph V
h : G ≤ G'
u v : V
p : G.Walk u v
⊢ (mapLe h p).IsPath ↔ p.IsPath

Tactic:
map_isPath_iff_of_injective Function.injective_id

Premises used: SimpleGraph.Walk.map_isPath_iff_of_injective, Function.injective_id
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G G' : SimpleGraph V
h : G ≤ G'
u : V
p : G.Walk u u
⊢ (mapLe h p).IsCycle ↔ p.IsCycle

Tactic:
map_isCycle_iff_of_injective Function.injective_id

Premises used: SimpleGraph.Walk.map_isCycle_iff_of_injective, Function.injective_id
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
hinj : Injective.{u + 1, v + 1} (α := V) (β := V') (⇑f : (a : V) → V')
u v : V
p : G.Walk u v
hp : p.IsPath
p' : G.Walk u v
hp' : p'.IsPath
h :
  Path.map f hinj (Subtype.mk (p := fun (p : G.Walk u v) ↦ p.IsPath) p hp) =
    Path.map f hinj (Subtype.mk (p := fun (p : G.Walk u v) ↦ p.IsPath) p' hp')
⊢ Walk.map f p = Walk.map f p'

Tactic:
simp only [Path.map, Subtype.mk.injEq] at h

Premises used: Subtype.mk.injEq, SimpleGraph.Path.map
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
hinj : Injective.{u + 1, v + 1} (α := V) (β := V') (⇑f : (a : V) → V')
u v : V
p : G.Walk u v
hp : p.IsPath
p' : G.Walk u v
hp' : p'.IsPath
h : Walk.map f p = Walk.map f p'
⊢ Subtype.mk (p := fun (p : G.Walk u v) ↦ p.IsPath) p hp = Subtype.mk (p := fun (p : G.Walk u v) ↦ p.IsPath) p' hp'

Tactic:
simp [Walk.map_injective_of_injective hinj u v h]

Premises used: SimpleGraph.Walk.map_injective_of_injective
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G ↪g G'
u v : V
⊢ Injective (α := G.Path u v) (Path.mapEmbedding f)

Tactic:
map_injective f.injective u v

Premises used: SimpleGraph.Path.mapEmbedding, SimpleGraph.Path.map_injective
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
H : SimpleGraph V
p : G.Walk u v
u_1 : V
hp : ∀ (e : Sym2 V), Membership.mem (γ := List (Sym2 V)) (edges (G := G) (u := u_1) Walk.nil) e → e ∈ H.edgeSet
pp : IsPath.{u} (V := V) (G := G) (u := u_1) Walk.nil
⊢ (Walk.transfer Walk.nil H hp).IsPath

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
H : SimpleGraph V
p : G.Walk u v
u_1 v_1 w : V
h : G.Adj u_1 v_1
p_1 : G.Walk v_1 w
ih : ∀ (hp : ∀ e ∈ p_1.edges, e ∈ H.edgeSet) (pp : p_1.IsPath), (p_1.transfer H hp).IsPath
hp : ∀ e ∈ (Walk.cons h p_1).edges, e ∈ H.edgeSet
pp : (Walk.cons h p_1).IsPath
cons : ∀ (pp : p_1.IsPath ∧ u_1 ∉ p_1.support), (p_1.transfer H ⋯).IsPath ∧ u_1 ∉ p_1.support
⊢ ((Walk.cons h p_1).transfer H hp).IsPath

Tactic:
simp only [Walk.transfer, cons_isPath_iff, support_transfer _] at pp ⊢

Premises used: SimpleGraph.Walk.support_transfer, SimpleGraph.Walk.transfer, SimpleGraph.Walk.cons_isPath_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
H : SimpleGraph V
p : G.Walk u v
u_1 v_1 w : V
h : G.Adj u_1 v_1
p_1 : G.Walk v_1 w
ih : ∀ (hp : ∀ e ∈ p_1.edges, e ∈ H.edgeSet) (pp : p_1.IsPath), (p_1.transfer H hp).IsPath
hp : ∀ e ∈ (cons h p_1).edges, e ∈ H.edgeSet
pp : p_1.IsPath ∧ u_1 ∉ p_1.support
⊢ (p_1.transfer H ⋯).IsPath ∧ u_1 ∉ p_1.support

Tactic:
⟨ih _ pp.1, pp.2⟩

Premises used: And.right, And.left, And.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
H : SimpleGraph V
p : G.Walk u v
u_1 v_1 w : V
h : G.Adj u_1 v_1
p_1 : G.Walk v_1 w
ih : ∀ (hp : ∀ e ∈ p_1.edges, e ∈ H.edgeSet) (pp : p_1.IsPath), (p_1.transfer H hp).IsPath
hp : ∀ e ∈ (cons h p_1).edges, e ∈ H.edgeSet
pp : p_1.IsPath ∧ u_1 ∉ p_1.support
⊢ (p_1.transfer H ⋯).IsPath ∧ u_1 ∉ p_1.support

Tactic:
exact ⟨ih _ pp.1, pp.2⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u v : V
H : SimpleGraph V
p : G.Walk u v
hp : ∀ e ∈ p.edges, e ∈ H.edgeSet
pp : p.IsPath
nil :
  ∀ {u : V}
    (hp : ∀ (e : Sym2 V), Membership.mem (γ := List (Sym2 V)) (edges (G := G) (u := u) Walk.nil) e → e ∈ H.edgeSet)
    (pp : IsPath.{u} (V := V) (G := G) (u := u) Walk.nil), (Walk.transfer Walk.nil H hp).IsPath
cons :
  ∀ {u v w : V} (h : G.Adj u v) (p : G.Walk v w)
    (ih : ∀ (hp : ∀ e ∈ p.edges, e ∈ H.edgeSet) (pp : p.IsPath), (p.transfer H hp).IsPath)
    (hp : ∀ e ∈ (Walk.cons h p).edges, e ∈ H.edgeSet) (pp : (Walk.cons h p).IsPath),
    ((Walk.cons h p).transfer H hp).IsPath
⊢ (p.transfer H hp).IsPath

Tactic:
induction p with
  | nil => simp
  | cons _ _ ih =>
    simp only [Walk.transfer, cons_isPath_iff, support_transfer _] at pp ⊢
    exact ⟨ih _ pp.1, pp.2⟩

Premises used: SimpleGraph.Walk.support_transfer, SimpleGraph.Walk.cons, SimpleGraph.Walk.IsPath.nil, SimpleGraph.Walk.transfer, SimpleGraph.Walk.cons_isPath_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u : V
H : SimpleGraph V
qc : IsCycle.{u} (V := V) (G := G) (u := u) nil
hq : ∀ (e : Sym2 V), Membership.mem (γ := List (Sym2 V)) (edges (G := G) (u := u) nil) e → e ∈ H.edgeSet
⊢ (Walk.transfer nil H hq).IsCycle

Tactic:
simp at qc
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u : V
H : SimpleGraph V
v : V
h : G.Adj u v
q : G.Walk v u
qc : (cons h q).IsCycle
hq : ∀ e ∈ (cons h q).edges, e ∈ H.edgeSet
⊢ s(u, v) ∈ H.edgeSet ∧ ∀ a ∈ q.edges, a ∈ H.edgeSet

Tactic:
simp only [edges_cons, List.mem_cons, forall_eq_or_imp] at hq

Premises used: forall_eq_or_imp, SimpleGraph.Walk.edges_cons, List.mem_cons
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u : V
H : SimpleGraph V
v : V
h : G.Adj u v
q : G.Walk v u
qc : (Walk.cons h q).IsCycle
hq_1 : ∀ e ∈ (Walk.cons h q).edges, e ∈ H.edgeSet
hq : s(u, v) ∈ H.edgeSet ∧ ∀ a ∈ q.edges, a ∈ H.edgeSet
cons : ∀ (qc : q.IsPath ∧ s(u, v) ∉ q.edges), (q.transfer H ⋯).IsPath ∧ s(u, v) ∉ q.edges
⊢ ((Walk.cons h q).transfer H hq_1).IsCycle

Tactic:
simp only [Walk.transfer, cons_isCycle_iff, edges_transfer q hq.2] at qc ⊢

Premises used: SimpleGraph.Walk.cons_isCycle_iff, SimpleGraph.Walk.edges_transfer, And.right, SimpleGraph.Walk.transfer
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u : V
H : SimpleGraph V
v : V
h : G.Adj u v
q : G.Walk v u
hq_1 : ∀ e ∈ (cons h q).edges, e ∈ H.edgeSet
hq : s(u, v) ∈ H.edgeSet ∧ ∀ a ∈ q.edges, a ∈ H.edgeSet
qc : q.IsPath ∧ s(u, v) ∉ q.edges
⊢ (q.transfer H ⋯).IsPath ∧ s(u, v) ∉ q.edges

Tactic:
⟨qc.1.transfer hq.2, qc.2⟩

Premises used: SimpleGraph.Walk.IsPath.transfer, And.right, And.left, And.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u : V
H : SimpleGraph V
v : V
h : G.Adj u v
q : G.Walk v u
hq_1 : ∀ e ∈ (cons h q).edges, e ∈ H.edgeSet
hq : s(u, v) ∈ H.edgeSet ∧ ∀ a ∈ q.edges, a ∈ H.edgeSet
qc : q.IsPath ∧ s(u, v) ∉ q.edges
⊢ (q.transfer H ⋯).IsPath ∧ s(u, v) ∉ q.edges

Tactic:
exact ⟨qc.1.transfer hq.2, qc.2⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u : V
H : SimpleGraph V
q : G.Walk u u
qc : q.IsCycle
hq : ∀ e ∈ q.edges, e ∈ H.edgeSet
nil :
  ∀ (qc : IsCycle.{u} (V := V) (G := G) (u := u) Walk.nil)
    (hq : ∀ (e : Sym2 V), Membership.mem (γ := List (Sym2 V)) (edges (G := G) (u := u) Walk.nil) e → e ∈ H.edgeSet),
    (Walk.transfer Walk.nil H hq).IsCycle
cons :
  ∀ {v : V} (h : G.Adj u v) (q : G.Walk v u) (qc : (Walk.cons h q).IsCycle)
    (hq : ∀ e ∈ (Walk.cons h q).edges, e ∈ H.edgeSet), ((Walk.cons h q).transfer H hq).IsCycle
⊢ (q.transfer H hq).IsCycle

Tactic:
cases q with
  | nil => simp at qc
  | cons _ q =>
    simp only [edges_cons, List.mem_cons, forall_eq_or_imp] at hq
    simp only [Walk.transfer, cons_isCycle_iff, edges_transfer q hq.2] at qc ⊢
    exact ⟨qc.1.transfer hq.2, qc.2⟩

Premises used: SimpleGraph.Walk.cons_isCycle_iff, forall_eq_or_imp, SimpleGraph.Walk.cons, SimpleGraph.Walk.edges_cons, SimpleGraph.Walk.nil, SimpleGraph.Walk.transfer, List.mem_cons
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
v w : V
s : Set (Sym2 V)
p : G.Walk v w
h : p.IsPath
hp : ∀ e ∈ p.edges, e ∉ s
⊢ (toDeleteEdges s p hp).IsPath

Tactic:
h.transfer _

Premises used: SimpleGraph.Walk.IsPath.transfer
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
v : V
s : Set (Sym2 V)
p : G.Walk v v
h : p.IsCycle
hp : ∀ e ∈ p.edges, e ∉ s
⊢ (toDeleteEdges s p hp).IsCycle

Tactic:
h.transfer _

Premises used: SimpleGraph.Walk.IsCycle.transfer
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
v_1 w v u u' v' : V
s : Set (Sym2 V)
p : G.Walk u v
hu : u = u'
hv : v = v'
h : ∀ e ∈ (p.copy hu hv).edges, e ∉ s
subst_vars : ∀ (p : G.Walk u' v') (h : ∀ e ∈ (p.copy ⋯ ⋯).edges, e ∉ s), ∀ e ∈ p.edges, e ∉ s
⊢ ∀ e ∈ p.edges, e ∉ s

Tactic:
subst_vars
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
v w u' v' : V
s : Set (Sym2 V)
p : G.Walk u' v'
h : ∀ e ∈ (p.copy ⋯ ⋯).edges, e ∉ s
⊢ ∀ e ∈ p.edges, e ∉ s

Tactic:
h

Premises used: SimpleGraph.Walk.copy
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
v w u' v' : V
s : Set (Sym2 V)
p : G.Walk u' v'
h : ∀ e ∈ (p.copy ⋯ ⋯).edges, e ∉ s
⊢ ∀ e ∈ p.edges, e ∉ s

Tactic:
exact h
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
v u u' v' : V
s : Set (Sym2 V)
p : G.Walk u v
hu : u = u'
hv : v = v'
h : ∀ e ∈ (p.copy hu hv).edges, e ∉ s
subst_vars :
  ∀ (p : G.Walk u' v') (h : ∀ e ∈ (p.copy ⋯ ⋯).edges, e ∉ s),
    toDeleteEdges s (p.copy ⋯ ⋯) h = (toDeleteEdges s p ⋯).copy ⋯ ⋯
⊢ toDeleteEdges s (p.copy hu hv) h = (toDeleteEdges s p ⋯).copy hu hv

Tactic:
subst_vars
-- Module: Mathlib.Combinatorics.SimpleGraph.Paths
Goal:
V : Type u
G : SimpleGraph V
u' v' : V
s : Set (Sym2 V)
p : G.Walk u' v'
h : ∀ e ∈ (p.copy ⋯ ⋯).edges, e ∉ s
⊢ toDeleteEdges s (p.copy ⋯ ⋯) h = (toDeleteEdges s p ⋯).copy ⋯ ⋯

Tactic:
rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.UniversalVerts
Goal:
V : Type u_1
G : SimpleGraph V
⊢ G.IsClique G.universalVerts

Tactic:
fun _ _ _ hy hxy ↦ hy hxy.symm

Premises used: Ne.symm, Set.Pairwise
-- Module: Mathlib.Combinatorics.SimpleGraph.UniversalVerts
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
s : Set V
h : Disjoint G.universalVerts s
hc : s.ncard ≤ G.universalVerts.ncard
obtain :
  ∀ (t : Set V) (ht : t ⊆ G.universalVerts ∧ t.ncard = s.ncard),
    ∃ t ⊆ G.universalVerts, ∃ (M : G.Subgraph), M.verts = s ∪ t ∧ M.IsMatching
⊢ ∃ t ⊆ G.universalVerts, ∃ (M : G.Subgraph), M.verts = s ∪ t ∧ M.IsMatching

Tactic:
obtain ⟨t, ht⟩ := Set.exists_subset_card_eq hc

Premises used: Set.exists_subset_card_eq
-- Module: Mathlib.Combinatorics.SimpleGraph.UniversalVerts
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
s : Set V
h : Disjoint G.universalVerts s
hc : s.ncard ≤ G.universalVerts.ncard
t : Set V
ht : t ⊆ G.universalVerts ∧ t.ncard = s.ncard
⊢ ∃ t ⊆ G.universalVerts, ∃ (M : G.Subgraph), M.verts = s ∪ t ∧ M.IsMatching

Tactic:
⟨t, ht.1, ?_⟩

Premises used: And.left, And.intro, Exists.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.UniversalVerts
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
s : Set V
h : Disjoint G.universalVerts s
hc : s.ncard ≤ G.universalVerts.ncard
t : Set V
ht : t ⊆ G.universalVerts ∧ t.ncard = s.ncard
refine : ∃ (M : G.Subgraph), M.verts = s ∪ t ∧ M.IsMatching
⊢ ∃ t ⊆ G.universalVerts, ∃ (M : G.Subgraph), M.verts = s ∪ t ∧ M.IsMatching

Tactic:
refine ⟨t, ht.1, ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.UniversalVerts
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
s : Set V
h : Disjoint G.universalVerts s
hc : s.ncard ≤ G.universalVerts.ncard
t : Set V
ht : t ⊆ G.universalVerts ∧ t.ncard = s.ncard
rw : Cardinal.mk (↑s : Type u_1) = Cardinal.mk (↑t : Type u_1)
rw₁ : Cardinal.mk (↑s : Type u_1) = (↑t.ncard : Cardinal.{u_1})
rw₂ : Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑s.ncard : Cardinal.{u_1}) (↑t.ncard : Cardinal.{u_1})
rw₃ rw₄ : Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑s.ncard : Cardinal.{u_1}) (↑s.ncard : Cardinal.{u_1})
⊢ Nonempty.{max 1 (u_1 + 1)} ((↑s : Type u_1) ≃ (↑t : Type u_1))

Tactic:
rw [← Cardinal.eq, ← t.cast_ncard t.toFinite, ← s.cast_ncard s.toFinite, ht.2]

Premises used: Set.toFinite, And.right, Cardinal.eq, Set.cast_ncard
-- Module: Mathlib.Combinatorics.SimpleGraph.UniversalVerts
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
s : Set V
h : Disjoint G.universalVerts s
hc : s.ncard ≤ G.universalVerts.ncard
t : Set V
ht : t ⊆ G.universalVerts ∧ t.ncard = s.ncard
obtain : ∀ (f : (↑s : Type u_1) ≃ (↑t : Type u_1)), ∃ (M : G.Subgraph), M.verts = s ∪ t ∧ M.IsMatching
⊢ ∃ (M : G.Subgraph), M.verts = s ∪ t ∧ M.IsMatching

Tactic:
obtain ⟨f⟩ : Nonempty (s ≃ t) := by
    rw [← Cardinal.eq, ← t.cast_ncard t.toFinite, ← s.cast_ncard s.toFinite, ht.2]

Premises used: Set.Elem, Equiv, Nonempty
-- Module: Mathlib.Combinatorics.SimpleGraph.UniversalVerts
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
s : Set V
h : Disjoint G.universalVerts s
hc : s.ncard ≤ G.universalVerts.ncard
t : Set V
ht : t ⊆ G.universalVerts ∧ t.ncard = s.ncard
f : (↑s : Type u_1) ≃ (↑t : Type u_1)
hd : Disjoint t s := ⋯
⊢ ∀ (v : (↑s : Type u_1)), G.Adj (↑v : V) (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) v) : V)

Tactic:
have hadj (v : s) : G.Adj v (f v) := ht.1 (f v).2 (hd.ne_of_mem (f v).2 v.2)
-- Module: Mathlib.Combinatorics.SimpleGraph.UniversalVerts
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
s : Set V
h : Disjoint G.universalVerts s
hc : s.ncard ≤ G.universalVerts.ncard
t : Set V
ht : t ⊆ G.universalVerts ∧ t.ncard = s.ncard
f : (↑s : Type u_1) ≃ (↑t : Type u_1)
hd : Disjoint t s := ⋯
hadj : ∀ (v : (↑s : Type u_1)), G.Adj (↑v : V) (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) v) : V)
⊢ ∃ (M : G.Subgraph), M.verts = s ∪ t ∧ M.IsMatching

Tactic:
Subgraph.IsMatching.exists_of_disjoint_sets_of_equiv hd.symm f hadj

Premises used: SimpleGraph.Subgraph.IsMatching.exists_of_disjoint_sets_of_equiv, Disjoint.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.UniversalVerts
Goal:
V : Type u_1
G : SimpleGraph V
inst : Finite V
s : Set V
h : Disjoint G.universalVerts s
hc : s.ncard ≤ G.universalVerts.ncard
t : Set V
ht : t ⊆ G.universalVerts ∧ t.ncard = s.ncard
f : (↑s : Type u_1) ≃ (↑t : Type u_1)
hd : Disjoint t s := ⋯
hadj : ∀ (v : (↑s : Type u_1)), G.Adj (↑v : V) (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) v) : V)
⊢ ∃ (M : G.Subgraph), M.verts = s ∪ t ∧ M.IsMatching

Tactic:
exact Subgraph.IsMatching.exists_of_disjoint_sets_of_equiv hd.symm f hadj

Premises used: SimpleGraph.Subgraph.IsMatching.exists_of_disjoint_sets_of_equiv, Disjoint.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.UniversalVerts
Goal:
V : Type u_1
G : SimpleGraph V
s : Set (↑G.deleteUniversalVerts.verts : Type u_1)
⊢ Disjoint (Subtype.val (p := fun (x : V) ↦ x ∈ G.deleteUniversalVerts.verts) '' s) G.universalVerts

Tactic:
simpa [← Set.disjoint_compl_right_iff_subset, Set.compl_eq_univ_diff] using
    Subtype.coe_image_subset _ s

Premises used: Subtype.coe_image_subset, Set.disjoint_compl_right_iff_subset, Set.compl_eq_univ_diff
-- Module: Mathlib.Combinatorics.SimpleGraph.UniversalVerts
Goal:
V : Type u_1
G : SimpleGraph V
t : Set V
s : Set (↑G.deleteUniversalVerts.verts : Type u_1)
K : G.deleteUniversalVerts.coe.ConnectedComponent
h : t ⊆ G.universalVerts
hrep : ConnectedComponent.Represents s G.deleteUniversalVerts.coe.oddComponents
⊢ Even
    (Subtype.val (p := fun (x : V) ↦ x ∈ G.deleteUniversalVerts.verts) '' K.supp \
        (Subtype.val (p := fun (x : V) ↦ x ∈ G.deleteUniversalVerts.verts) '' s ∪ t)).ncard

Tactic:
simp [-deleteUniversalVerts_verts, ← Set.diff_inter_diff, ← Set.image_diff Subtype.val_injective,
    sdiff_eq_left.mpr <| Set.disjoint_of_subset_right h (disjoint_image_val_universalVerts _),
    Set.inter_diff_distrib_right, ← Set.image_inter Subtype.val_injective,
    Set.ncard_image_of_injective _ Subtype.val_injective, K.even_ncard_supp_sdiff_rep hrep]

Premises used: Iff.mpr, SimpleGraph.deleteUniversalVerts_verts, Subtype.val_injective, SimpleGraph.ConnectedComponent.even_ncard_supp_sdiff_rep, Set.image_diff, Set.image_inter, Set.inter_diff_distrib_right, SimpleGraph.disjoint_image_val_universalVerts, Set.ncard_image_of_injective, sdiff_eq_left, Set.diff_inter_diff, Set.disjoint_of_subset_right
-- Module: Mathlib.Computability.MyhillNerode
Goal:
α : Type u
L : Language α
⊢ L.leftQuotient [] = L

Tactic:
rfl

Premises used: Set.Mem, setOf, Language.leftQuotient, List.append, rfl
-- Module: Mathlib.Computability.MyhillNerode
Goal:
α : Type u
L : Language α
x y : List α
⊢ L.leftQuotient (x ++ y) = (L.leftQuotient x).leftQuotient y

Tactic:
simp [leftQuotient, Language]

Premises used: Language.leftQuotient, Language
-- Module: Mathlib.Computability.MyhillNerode
Goal:
α : Type u
L : Language α
x y : List α
⊢ y ∈ L.leftQuotient x ↔ x ++ y ∈ L

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Language.leftQuotient
-- Module: Mathlib.Computability.MyhillNerode
Goal:
α : Type u
σ : Type v
M : DFA α σ
x : List α
h : ∀ (y : List α), y ∈ M.accepts.leftQuotient x ↔ y ∈ M.acceptsFrom (M.eval x)
⊢ M.accepts.leftQuotient x = M.acceptsFrom (M.eval x)

Tactic:
ext y
-- Module: Mathlib.Computability.MyhillNerode
Goal:
α : Type u
σ : Type v
M : DFA α σ
x y : List α
⊢ y ∈ M.accepts.leftQuotient x ↔ y ∈ M.acceptsFrom (M.eval x)

Tactic:
simp [DFA.mem_accepts, DFA.mem_acceptsFrom, DFA.eval, DFA.evalFrom_of_append]

Premises used: DFA.evalFrom_of_append, DFA.mem_acceptsFrom, DFA.eval, DFA.mem_accepts
-- Module: Mathlib.Computability.MyhillNerode
Goal:
α : Type u
σ : Type v
M : DFA α σ
⊢ M.accepts.leftQuotient = M.acceptsFrom ∘ M.eval

Tactic:
funext <| leftQuotient_accepts_apply M

Premises used: funext, Language.leftQuotient_accepts_apply
-- Module: Mathlib.Computability.MyhillNerode
Goal:
α : Type u
L : Language α
h : L.IsRegular
have : ∀ (σ : Type) (x : Fintype σ) (M : DFA α σ) (hM : M.accepts = L), (Set.range L.leftQuotient).Finite
⊢ (Set.range L.leftQuotient).Finite

Tactic:
have ⟨σ, x, M, hM⟩ := h
-- Module: Mathlib.Computability.MyhillNerode
Goal:
α : Type u
L : Language α
h : L.IsRegular
σ : Type
x : Fintype σ
M : DFA α σ
hM : M.accepts = L
rw : (Set.range (M.acceptsFrom ∘ M.eval)).Finite
⊢ (Set.range L.leftQuotient).Finite

Tactic:
rw [← hM, leftQuotient_accepts]

Premises used: Language.leftQuotient_accepts
-- Module: Mathlib.Computability.MyhillNerode
Goal:
α : Type u
L : Language α
h : L.IsRegular
σ : Type
x : Fintype σ
M : DFA α σ
hM : M.accepts = L
⊢ (Set.range (M.acceptsFrom ∘ M.eval)).Finite

Tactic:
Set.finite_of_finite_preimage (Set.toFinite _)
    (Set.range_comp_subset_range M.eval M.acceptsFrom)

Premises used: Set.range_comp_subset_range, Set.finite_of_finite_preimage, DFA.acceptsFrom, Set.toFinite, DFA.eval
-- Module: Mathlib.Computability.MyhillNerode
Goal:
α : Type u
L : Language α
h : L.IsRegular
σ : Type
x : Fintype σ
M : DFA α σ
hM : M.accepts = L
⊢ (Set.range (M.acceptsFrom ∘ M.eval)).Finite

Tactic:
exact Set.finite_of_finite_preimage (Set.toFinite _)
    (Set.range_comp_subset_range M.eval M.acceptsFrom)

Premises used: Set.range_comp_subset_range, Set.finite_of_finite_preimage, DFA.acceptsFrom, Set.toFinite, DFA.eval
-- Module: Mathlib.Computability.MyhillNerode
Goal:
α : Type u
σ : Type v
L : Language α
s : (↑(Set.range L.leftQuotient) : Type u)
a : α
refine : (↑s : Language α).leftQuotient [a] ∈ Set.range L.leftQuotient
⊢ (↑(Set.range L.leftQuotient) : Type u)

Tactic:
refine ⟨s.val.leftQuotient [a], ?_⟩
-- Module: Mathlib.Computability.MyhillNerode
Goal:
α : Type u
σ : Type v
L : Language α
s : (↑(Set.range L.leftQuotient) : Type u)
a : α
obtain :
  ∀ (y : List α) (hy : L.leftQuotient y = (↑s : Language α)),
    (↑s : Language α).leftQuotient [a] ∈ Set.range L.leftQuotient
⊢ (↑s : Language α).leftQuotient [a] ∈ Set.range L.leftQuotient

Tactic:
obtain ⟨y, hy⟩ := s.prop

Premises used: Subtype.prop
-- Module: Mathlib.Computability.MyhillNerode
Goal:
α : Type u
σ : Type v
L : Language α
s : (↑(Set.range L.leftQuotient) : Type u)
a : α
y : List α
hy : L.leftQuotient y = (↑s : Language α)
exists : L.leftQuotient (y ++ [a]) = (↑s : Language α).leftQuotient [a]
⊢ (↑s : Language α).leftQuotient [a] ∈ Set.range L.leftQuotient

Tactic:
exists y ++ [a]
-- Module: Mathlib.Computability.MyhillNerode
Goal:
α : Type u
σ : Type v
L : Language α
s : (↑(Set.range L.leftQuotient) : Type u)
a : α
y : List α
hy : L.leftQuotient y = (↑s : Language α)
rw : L.leftQuotient (y ++ [a]) = (L.leftQuotient y).leftQuotient [a]
rw₁ rw₂ : (L.leftQuotient y).leftQuotient [a] = (L.leftQuotient y).leftQuotient [a]
⊢ L.leftQuotient (y ++ [a]) = (↑s : Language α).leftQuotient [a]

Tactic:
rw [← hy, leftQuotient_append]

Premises used: Language.leftQuotient_append
-- Module: Mathlib.Computability.MyhillNerode
Goal:
α : Type u
σ : Type v
L : Language α
exists exists₁ : L.leftQuotient [] = L
⊢ L ∈ Set.range L.leftQuotient

Tactic:
exists []
-- Module: Mathlib.Computability.MyhillNerode
Goal:
α : Type u
L : Language α
s : (↑(Set.range L.leftQuotient) : Type u)
⊢ s ∈ L.toDFA.accept ↔ [] ∈ (↑s : Language α)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Computability.MyhillNerode
Goal:
α : Type u
L : Language α
s : (↑(Set.range L.leftQuotient) : Type u)
a : α
⊢ (↑(L.toDFA.step s a) : Language α) = (↑s : Language α).leftQuotient [a]

Tactic:
rfl

Premises used: setOf, Language.leftQuotient, rfl
-- Module: Mathlib.Computability.MyhillNerode
Goal:
α : Type u
L : Language α
⊢ (↑L.toDFA.start : Language α) = L

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Computability.MyhillNerode
Goal:
α : Type u
L : Language α
h : ∀ (x : List α), x ∈ L.toDFA.accepts ↔ x ∈ L
⊢ L.toDFA.accepts = L

Tactic:
ext x