awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : (↑s : Type u_1) ≃ (↑t : Type u_1)
hadj : ∀ (v : (↑s : Type u_1)), G.Adj (↑v : V) (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) v) : V)
y : V
hys : y ∈ s
hl : (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) y hys)) : V) ∈ s
⊢ y =
    (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1))
          (Subtype.mk (p := fun (x : V) ↦ x ∈ s)
            (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) y hys)) : V) hl)) :
      V)

Tactic:
(h.ne_of_mem hl (f ⟨y, hys⟩).coe_prop rfl).elim

Premises used: Subtype.coe_prop, False.elim, Subtype.mk, Disjoint.ne_of_mem, DFunLike.coe, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : (↑s : Type u_1) ≃ (↑t : Type u_1)
hadj : ∀ (v : (↑s : Type u_1)), G.Adj (↑v : V) (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) v) : V)
y : V
hys : y ∈ s
hl : (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) y hys)) : V) ∈ s
⊢ y =
    (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1))
          (Subtype.mk (p := fun (x : V) ↦ x ∈ s)
            (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) y hys)) : V) hl)) :
      V)

Tactic:
exact (h.ne_of_mem hl (f ⟨y, hys⟩).coe_prop rfl).elim

Premises used: Subtype.coe_prop, False.elim, Subtype.mk, Disjoint.ne_of_mem, DFunLike.coe, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : (↑s : Type u_1) ≃ (↑t : Type u_1)
hadj : ∀ (v : (↑s : Type u_1)), G.Adj (↑v : V) (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) v) : V)
v : V
hr : v ∈ t
h₁ :
  (fun (w : V) ↦
        (∃ (h : v ∈ s),
            (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) v h)) : V) = w) ∨
          ∃ (h : w ∈ s),
            (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) w h)) : V) = v)
      (↑((f.symm : (a : (↑t : Type u_1)) → (↑s : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ t) v hr)) : V) ∧
    ∀ (y : V),
      (fun (w : V) ↦
            (∃ (h : v ∈ s),
                (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) v h)) : V) =
                  w) ∨
              ∃ (h : w ∈ s),
                (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) w h)) : V) = v)
          y →
        y = (↑((f.symm : (a : (↑t : Type u_1)) → (↑s : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ t) v hr)) : V)
⊢ ∃! w : V,
    (∃ (h : v ∈ s),
        (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) v h)) : V) = w) ∨
      ∃ (h : w ∈ s),
        (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) w h)) : V) = v

Tactic:
use f.symm ⟨v, hr⟩

Premises used: Subtype.mk, Equiv.symm, DFunLike.coe
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : (↑s : Type u_1) ≃ (↑t : Type u_1)
hadj : ∀ (v : (↑s : Type u_1)), G.Adj (↑v : V) (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) v) : V)
v : V
hr : v ∈ t
h₁ :
  ∀ (y : V),
    ((∃ (h : v ∈ s),
          (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) v h)) : V) = y) ∨
        ∃ (h : y ∈ s),
          (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) y h)) : V) = v) →
      y = (↑((f.symm : (a : (↑t : Type u_1)) → (↑s : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ t) v hr)) : V)
⊢ (fun (w : V) ↦
        (∃ (h : v ∈ s),
            (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) v h)) : V) = w) ∨
          ∃ (h : w ∈ s),
            (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) w h)) : V) = v)
      (↑((f.symm : (a : (↑t : Type u_1)) → (↑s : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ t) v hr)) : V) ∧
    ∀ (y : V),
      (fun (w : V) ↦
            (∃ (h : v ∈ s),
                (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) v h)) : V) =
                  w) ∨
              ∃ (h : w ∈ s),
                (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) w h)) : V) = v)
          y →
        y = (↑((f.symm : (a : (↑t : Type u_1)) → (↑s : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ t) v hr)) : V)

Tactic:
simp only [Subtype.coe_eta, Equiv.apply_symm_apply, Subtype.coe_prop, exists_const, or_true,
      true_and]

Premises used: Equiv.apply_symm_apply, Subtype.coe_prop, Subtype.coe_eta, exists_const, or_true, true_and
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : (↑s : Type u_1) ≃ (↑t : Type u_1)
hadj : ∀ (v : (↑s : Type u_1)), G.Adj (↑v : V) (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) v) : V)
v : V
hr : v ∈ t
hy : v ∈ s
⊢ Eq.{u_1 + 1} (α := V)
    (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) v hy)) : V)
    (↑((f.symm : (a : (↑t : Type u_1)) → (↑s : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ t) v hr)) : V)

Tactic:
(h.ne_of_mem hy hr rfl).elim

Premises used: False.elim, Disjoint.ne_of_mem, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : (↑s : Type u_1) ≃ (↑t : Type u_1)
hadj : ∀ (v : (↑s : Type u_1)), G.Adj (↑v : V) (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) v) : V)
v : V
hr : v ∈ t
hy : v ∈ s
⊢ Eq.{u_1 + 1} (α := V)
    (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) v hy)) : V)
    (↑((f.symm : (a : (↑t : Type u_1)) → (↑s : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ t) v hr)) : V)

Tactic:
exact (h.ne_of_mem hy hr rfl).elim

Premises used: False.elim, Disjoint.ne_of_mem, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : (↑s : Type u_1) ≃ (↑t : Type u_1)
hadj : ∀ (v : (↑s : Type u_1)), G.Adj (↑v : V) (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) v) : V)
y : V
hy : y ∈ s
hr : (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) y hy)) : V) ∈ t
⊢ y =
    (↑((f.symm : (a : (↑t : Type u_1)) → (↑s : Type u_1))
          (Subtype.mk (p := fun (x : V) ↦ x ∈ t)
            (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) y hy)) : V) hr)) :
      V)

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
M : G.Subgraph
f : G →g G'
hf : Injective.{u_1 + 1, u_2 + 1} (α := V) (β := W) (⇑f : (a : V) → W)
hM : M.IsMatching
v : V
hv : v ∈ M.verts
obtain :
  ∀ (v' : V) (hv' : (fun (w : V) ↦ M.Adj v w) v' ∧ ∀ (y : V), (fun (w : V) ↦ M.Adj v w) y → y = v'),
    ∃! w : W, (Subgraph.map f M).Adj ((f : (a : V) → W) v) w
⊢ ∃! w : W, (Subgraph.map f M).Adj ((f : (a : V) → W) v) w

Tactic:
obtain ⟨v', hv'⟩ := hM hv
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
M : G.Subgraph
f : G →g G'
hf : Injective.{u_1 + 1, u_2 + 1} (α := V) (β := W) (⇑f : (a : V) → W)
hM : M.IsMatching
v : V
hv : v ∈ M.verts
v' : V
hv' : (fun (w : V) ↦ M.Adj v w) v' ∧ ∀ (y : V), (fun (w : V) ↦ M.Adj v w) y → y = v'
h :
  (fun (w : W) ↦ (Subgraph.map f M).Adj ((f : (a : V) → W) v) w) ((f : (a : V) → W) v') ∧
    ∀ (y : W), (fun (w : W) ↦ (Subgraph.map f M).Adj ((f : (a : V) → W) v) w) y → y = (f : (a : V) → W) v'
⊢ ∃! w : W, (Subgraph.map f M).Adj ((f : (a : V) → W) v) w

Tactic:
use f v'

Premises used: DFunLike.coe
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
M : G.Subgraph
f : G →g G'
hf : Injective.{u_1 + 1, u_2 + 1} (α := V) (β := W) (⇑f : (a : V) → W)
hM : M.IsMatching
v : V
hv : v ∈ M.verts
v' : V
hv' : (fun (w : V) ↦ M.Adj v w) v' ∧ ∀ (y : V), (fun (w : V) ↦ M.Adj v w) y → y = v'
⊢ (fun (w : W) ↦ (Subgraph.map f M).Adj ((f : (a : V) → W) v) w) ((f : (a : V) → W) v') ∧
    ∀ (y : W), (fun (w : W) ↦ (Subgraph.map f M).Adj ((f : (a : V) → W) v) w) y → y = (f : (a : V) → W) v'

Tactic:
⟨⟨v, v', hv'.1, rfl, rfl⟩, ?_⟩

Premises used: And.left, And.intro, Exists.intro, rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
M : G.Subgraph
f : G →g G'
hf : Injective.{u_1 + 1, u_2 + 1} (α := V) (β := W) (⇑f : (a : V) → W)
hM : M.IsMatching
v : V
hv : v ∈ M.verts
v' : V
hv' : (fun (w : V) ↦ M.Adj v w) v' ∧ ∀ (y : V), (fun (w : V) ↦ M.Adj v w) y → y = v'
h : ∀ (y : W), (fun (w : W) ↦ (Subgraph.map f M).Adj ((f : (a : V) → W) v) w) y → y = (f : (a : V) → W) v'
⊢ (fun (w : W) ↦ (Subgraph.map f M).Adj ((f : (a : V) → W) v) w) ((f : (a : V) → W) v') ∧
    ∀ (y : W), (fun (w : W) ↦ (Subgraph.map f M).Adj ((f : (a : V) → W) v) w) y → y = (f : (a : V) → W) v'

Tactic:
refine ⟨⟨v, v', hv'.1, rfl, rfl⟩, ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
M : G.Subgraph
f : G →g G'
hf : Injective.{u_1 + 1, u_2 + 1} (α := V) (β := W) (⇑f : (a : V) → W)
hM : M.IsMatching
v : V
hv : v ∈ M.verts
v' : V
hv' : (fun (w : V) ↦ M.Adj v w) v' ∧ ∀ (y : V), (fun (w : V) ↦ M.Adj v w) y → y = v'
w w' : V
hw : M.Adj w w'
hw' : Eq.{u_2 + 1} (α := W) ((f : (a : V) → W) w : W) ((f : (a : V) → W) v : W)
⊢ M.Adj v w'

Tactic:
cases hf hw'.symm

Premises used: Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
M : G.Subgraph
f : G →g G'
hf : Injective.{u_1 + 1, u_2 + 1} (α := V) (β := W) (⇑f : (a : V) → W)
hM : M.IsMatching
v : V
hv : v ∈ M.verts
v' : V
hv' : (fun (w : V) ↦ M.Adj v w) v' ∧ ∀ (y : V), (fun (w : V) ↦ M.Adj v w) y → y = v'
w w' : V
hw : M.Adj w w'
hw' : Eq.{u_2 + 1} (α := W) ((f : (a : V) → W) w : W) ((f : (a : V) → W) v : W)
hw₁ : M.Adj v w'
⊢ Eq.{u_2 + 1} (α := W) ((f : (a : V) → W) v : W) ((f : (a : V) → W) v : W)

Tactic:
cases hf hw'.symm

Premises used: Eq.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
M : G.Subgraph
f : G →g G'
hf : Injective.{u_1 + 1, u_2 + 1} (α := V) (β := W) (⇑f : (a : V) → W)
hM : M.IsMatching
v : V
hv : v ∈ M.verts
v' : V
hv' : (fun (w : V) ↦ M.Adj v w) v' ∧ ∀ (y : V), (fun (w : V) ↦ M.Adj v w) y → y = v'
w' : V
hw : M.Adj v w'
hw' : Eq.{u_2 + 1} (α := W) ((f : (a : V) → W) v : W) ((f : (a : V) → W) v : W)
h h₁ : Eq.{u_2 + 1} (α := W) ((f : (a : V) → W) v' : W) ((f : (a : V) → W) v' : W)
⊢ Eq.{u_2 + 1} (α := W) ((f : (a : V) → W) w' : W) ((f : (a : V) → W) v' : W)

Tactic:
rw [hv'.2 w' hw]

Premises used: And.right
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
M : G.Subgraph
f : G ≃g G'
h : (Subgraph.map f.toHom M).IsMatching
⊢ M.IsMatching

Tactic:
simpa [← map_comp] using h.map f.symm.toHom f.symm.injective

Premises used: SimpleGraph.Subgraph.IsMatching.map, SimpleGraph.Subgraph.map_comp, SimpleGraph.Iso.toHom, RelIso.injective, SimpleGraph.Iso.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
⊢ M.verts = ⋃ e ∈ M.edgeSet, (↑e : Set V)

Tactic:
Set.ext fun v ↦ .trans ⟨fun hv ↦ ?_, fun ⟨e, he, hv⟩ ↦ ?_⟩ Set.mem_iUnion₂.symm

Premises used: Set.ext, Set.mem_iUnion₂, Iff.intro, Iff.trans, Iff.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
refine_1 : ∀ (v : V) (hv : v ∈ M.verts), ∃ (i : Sym2 V) (_ : i ∈ M.edgeSet), v ∈ (↑i : Set V)
refine_2 :
  ∀ (v : V),
    (∃ (i : Sym2 V) (_ : i ∈ M.edgeSet), v ∈ (↑i : Set V)) →
      ∀ (e : Sym2 V) (he : e ∈ M.edgeSet) (hv : v ∈ (↑e : Set V)), v ∈ M.verts
⊢ M.verts = ⋃ e ∈ M.edgeSet, (↑e : Set V)

Tactic:
refine Set.ext fun v ↦ .trans ⟨fun hv ↦ ?_, fun ⟨e, he, hv⟩ ↦ ?_⟩ Set.mem_iUnion₂.symm

Premises used: Set.ext, Set.mem_iUnion₂, Iff.intro, Iff.trans, Iff.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
v : V
hv : v ∈ M.verts
refine_1 :
  ∀ (u : V) (he : M.Adj v u),
    (∀ (y : V), (fun (w : V) ↦ M.Adj v w) y → y = u) → ∃ (i : Sym2 V) (_ : i ∈ M.edgeSet), v ∈ (↑i : Set V)
⊢ ∃ (i : Sym2 V) (_ : i ∈ M.edgeSet), v ∈ (↑i : Set V)

Tactic:
have ⟨u, he, _⟩ := h hv
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
v : V
hv : v ∈ M.verts
u : V
he : (fun (w : V) ↦ M.Adj v w) u
right : ∀ (y : V), (fun (w : V) ↦ M.Adj v w) y → y = u
⊢ ∃ (i : Sym2 V) (_ : i ∈ M.edgeSet), v ∈ (↑i : Set V)

Tactic:
⟨s(v, u), he, Sym2.mem_mk_left ..⟩

Premises used: Sym2.mk, Sym2.mem_mk_left, Exists.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
v : V
hv : v ∈ M.verts
u : V
he : (fun (w : V) ↦ M.Adj v w) u
right : ∀ (y : V), (fun (w : V) ↦ M.Adj v w) y → y = u
⊢ ∃ (i : Sym2 V) (_ : i ∈ M.edgeSet), v ∈ (↑i : Set V)

Tactic:
exact ⟨s(v, u), he, Sym2.mem_mk_left ..⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
v : V
h_1 : ∃ (i : Sym2 V) (_ : i ∈ M.edgeSet), v ∈ (↑i : Set V)
e : Sym2 V
he : e ∈ M.edgeSet
hv : v ∈ (↑e : Set V)
⊢ v ∈ M.verts

Tactic:
mem_verts_of_mem_edge he hv

Premises used: SimpleGraph.Subgraph.mem_verts_of_mem_edge
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
v : V
h_1 : ∃ (i : Sym2 V) (_ : i ∈ M.edgeSet), v ∈ (↑i : Set V)
e : Sym2 V
he : e ∈ M.edgeSet
hv : v ∈ (↑e : Set V)
⊢ v ∈ M.verts

Tactic:
exact mem_verts_of_mem_edge he hv

Premises used: SimpleGraph.Subgraph.mem_verts_of_mem_edge
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
⊢ Set.InjOn.{u_1, u_1} (α := G.Subgraph) edgeSet (setOf IsMatching)

Tactic:
fun M₁ h₁ M₂ h₂ h ↦ Subgraph.ext ?_ <| Sym2.fromRel_eq_fromRel_iff_eq .. |>.mp h

Premises used: SimpleGraph.Subgraph.symm, Sym2.fromRel_eq_fromRel_iff_eq, SimpleGraph.Subgraph.ext, Iff.mp, Set.InjOn
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
refine :
  ∀ (M₁ : G.Subgraph) (h₁ : Membership.mem (γ := Set G.Subgraph) (setOf IsMatching) M₁) (M₂ : G.Subgraph)
    (h₂ : Membership.mem (γ := Set G.Subgraph) (setOf IsMatching) M₂) (h : M₁.edgeSet = M₂.edgeSet), M₁.verts = M₂.verts
⊢ Set.InjOn.{u_1, u_1} (α := G.Subgraph) edgeSet (setOf IsMatching)

Tactic:
refine fun M₁ h₁ M₂ h₂ h ↦ Subgraph.ext ?_ <| Sym2.fromRel_eq_fromRel_iff_eq .. |>.mp h

Premises used: Sym2.fromRel_eq_fromRel_iff_eq, SimpleGraph.Subgraph.ext, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M₁ : G.Subgraph
h₁ : Membership.mem (γ := Set G.Subgraph) (setOf IsMatching) M₁
M₂ : G.Subgraph
h₂ : Membership.mem (γ := Set G.Subgraph) (setOf IsMatching) M₂
h : M₁.edgeSet = M₂.edgeSet
rw : ⋃ e ∈ M₁.edgeSet, (↑e : Set V) = M₂.verts
rw₁ : Eq.{u_1 + 1} (α := Set V) (⋃ e ∈ M₁.edgeSet, (↑e : Set V)) (⋃ e ∈ M₂.edgeSet, (↑e : Set V))
rw₂ rw₃ : Eq.{u_1 + 1} (α := Set V) (⋃ e ∈ M₂.edgeSet, (↑e : Set V)) (⋃ e ∈ M₂.edgeSet, (↑e : Set V))
⊢ M₁.verts = M₂.verts

Tactic:
rw [h₁.verts_eq_biUnion_edgeSet, h₂.verts_eq_biUnion_edgeSet, h]

Premises used: SimpleGraph.Subgraph.IsMatching.verts_eq_biUnion_edgeSet
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
⊢ StrictMonoOn.{u_1, u_1} (α := G.Subgraph) edgeSet (setOf IsMatching)

Tactic:
edgeSet_monotone.monotoneOn _ |>.strictMonoOn_of_injOn injOn_edgeSet

Premises used: SimpleGraph.Subgraph.edgeSet_monotone, MonotoneOn.strictMonoOn_of_injOn, SimpleGraph.Subgraph.IsMatching.injOn_edgeSet, Monotone.monotoneOn
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
⊢ M.support = M.verts

Tactic:
M.support_subset_verts.antisymm fun v hv => ?_

Premises used: SimpleGraph.Subgraph.support_subset_verts, HasSubset.Subset.antisymm
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
refine : ∀ (v : V) (hv : v ∈ M.verts), v ∈ M.support
⊢ M.support = M.verts

Tactic:
refine M.support_subset_verts.antisymm fun v hv => ?_

Premises used: SimpleGraph.Subgraph.support_subset_verts, HasSubset.Subset.antisymm
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
v : V
hv : v ∈ M.verts
obtain : ∀ (w : V) (hvw : M.Adj v w), v ∈ M.support
⊢ v ∈ M.support

Tactic:
obtain ⟨w, hvw, -⟩ := h hv
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
v : V
hv : v ∈ M.verts
w : V
hvw : M.Adj v w
⊢ v ∈ M.support

Tactic:
⟨_, hvw⟩

Premises used: Set.Mem, setOf, SetRel.dom, SimpleGraph.Subgraph.support, Exists.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
v : V
hv : v ∈ M.verts
w : V
hvw : M.Adj v w
⊢ v ∈ M.support

Tactic:
exact ⟨_, hvw⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst : (v : V) → Fintype (↑(M.neighborSet v) : Type u_1)
⊢ M.IsMatching ↔ ∀ v ∈ M.verts, M.degree v = 1

Tactic:
simp only [degree_eq_one_iff_existsUnique_adj, IsMatching]

Premises used: SimpleGraph.Subgraph.degree_eq_one_iff_existsUnique_adj, SimpleGraph.Subgraph.IsMatching
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst : Fintype (↑M.verts : Type u_1)
h : M.IsMatching
⊢ ∀ v ∈ M.verts, M.degree v = 1

Tactic:
rw [isMatching_iff_forall_degree] at h

Premises used: SimpleGraph.Subgraph.isMatching_iff_forall_degree
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst : Fintype (↑M.verts : Type u_1)
h : ∀ v ∈ M.verts, M.degree v = 1
h₁ : M.verts.toFinset.card = M.coe.edgeFinset.card + M.coe.edgeFinset.card
⊢ Even M.verts.toFinset.card

Tactic:
use M.coe.edgeFinset.card

Premises used: SimpleGraph.edgeFinset, SimpleGraph.Subgraph.coe, Finset.card
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst : Fintype (↑M.verts : Type u_1)
h : ∀ v ∈ M.verts, M.degree v = 1
h₁ : M.verts.toFinset.card = ∑ v : (↑M.verts : Type u_1), M.coe.degree v
⊢ M.verts.toFinset.card = M.coe.edgeFinset.card + M.coe.edgeFinset.card

Tactic:
rw [← two_mul, ← M.coe.sum_degrees_eq_twice_card_edges]

Premises used: SimpleGraph.sum_degrees_eq_twice_card_edges, two_mul, SimpleGraph.Subgraph.coe
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst : Fintype (↑M.verts : Type u_1)
h : ∀ v ∈ M.verts, M.degree v = 1
⊢ M.verts.toFinset.card = ∑ v : (↑M.verts : Type u_1), M.coe.degree v

Tactic:
simp [h, Finset.card_univ]

Premises used: Finset.card_univ
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst : Fintype (↑M.verts : Type u_1)
h : M.IsMatching
rw rw₁ rw₂ : ∀ (h : ∀ v ∈ M.verts, M.degree v = 1), Even M.verts.toFinset.card
h₁ : ∀ (h : ∀ v ∈ M.verts, M.degree v = 1), M.verts.toFinset.card = M.coe.edgeFinset.card + M.coe.edgeFinset.card
h₂ : ∀ (h : ∀ v ∈ M.verts, M.degree v = 1), M.verts.toFinset.card = ∑ v : (↑M.verts : Type u_1), M.coe.degree v
⊢ Even M.verts.toFinset.card

Tactic:
classical
  rw [isMatching_iff_forall_degree] at h
  use M.coe.edgeFinset.card
  rw [← two_mul, ← M.coe.sum_degrees_eq_twice_card_edges]
  simp [h, Finset.card_univ]

Premises used: Finset.card_univ, two_mul, SimpleGraph.Subgraph.isMatching_iff_forall_degree
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
⊢ M.IsPerfectMatching ↔ ∀ (v : V), ∃! w : V, M.Adj v w

Tactic:
⟨?_, fun hm => ⟨fun v _ => hm v, fun v => ?_⟩⟩

Premises used: And.intro, Iff.intro
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
refine_1 : M.IsPerfectMatching → ∀ (v : V), ∃! w : V, M.Adj v w
refine_2 : ∀ (hm : ∀ (v : V), ∃! w : V, M.Adj v w) (v : V), v ∈ M.verts
⊢ M.IsPerfectMatching ↔ ∀ (v : V), ∃! w : V, M.Adj v w

Tactic:
refine ⟨?_, fun hm => ⟨fun v _ => hm v, fun v => ?_⟩⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
hm : M.IsMatching
hs : M.IsSpanning
v : V
⊢ ∃! w : V, M.Adj v w

Tactic:
hm (hs v)
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
hm : M.IsMatching
hs : M.IsSpanning
v : V
⊢ ∃! w : V, M.Adj v w

Tactic:
exact hm (hs v)
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
hm : ∀ (v : V), ∃! w : V, M.Adj v w
v : V
refine_2 : ∀ (w : V) (hw : M.Adj v w), v ∈ M.verts
⊢ v ∈ M.verts

Tactic:
obtain ⟨w, hw, -⟩ := hm v
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
hm : ∀ (v : V), ∃! w : V, M.Adj v w
v w : V
hw : M.Adj v w
⊢ v ∈ M.verts

Tactic:
M.edge_vert hw

Premises used: SimpleGraph.Subgraph.edge_vert
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
hm : ∀ (v : V), ∃! w : V, M.Adj v w
v w : V
hw : M.Adj v w
⊢ v ∈ M.verts

Tactic:
exact M.edge_vert hw

Premises used: SimpleGraph.Subgraph.edge_vert
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst : (v : V) → Fintype (↑(M.neighborSet v) : Type u_1)
⊢ M.IsPerfectMatching ↔ ∀ (v : V), M.degree v = 1

Tactic:
simp [degree_eq_one_iff_existsUnique_adj, isPerfectMatching_iff]

Premises used: SimpleGraph.Subgraph.isPerfectMatching_iff, SimpleGraph.Subgraph.degree_eq_one_iff_existsUnique_adj
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst : Fintype V
h : M.IsPerfectMatching
⊢ Even (Fintype.card V)

Tactic:
simpa only [h.2.card_verts] using IsMatching.even_card h.1

Premises used: SimpleGraph.Subgraph.IsSpanning.card_verts, And.right, And.left, SimpleGraph.Subgraph.IsMatching.even_card
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst : Fintype V
h : M.IsPerfectMatching
⊢ Even (Fintype.card V)

Tactic:
classical
  simpa only [h.2.card_verts] using IsMatching.even_card h.1
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
c : G.ConnectedComponent
v : V
hv : v ∈ (M.induce (M.verts ∩ c.supp)).verts
obtain : ∀ (hv : v ∈ M.verts), ∃! w : V, (M.induce (M.verts ∩ (G.connectedComponentMk v).supp)).Adj v w
⊢ ∃! w : V, (M.induce (M.verts ∩ c.supp)).Adj v w

Tactic:
obtain ⟨hv, rfl⟩ := hv

Premises used: rfl
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
v : V
hv : v ∈ M.verts
obtain :
  ∀ (w : V) (hvw : M.Adj v w) (hw : ∀ (y : V), (fun (w : V) ↦ M.Adj v w) y → y = w),
    ∃! w : V, (M.induce (M.verts ∩ (G.connectedComponentMk v).supp)).Adj v w
⊢ ∃! w : V, (M.induce (M.verts ∩ (G.connectedComponentMk v).supp)).Adj v w

Tactic:
obtain ⟨w, hvw, hw⟩ := h hv
-- Module: Mathlib.Combinatorics.SimpleGraph.Matching
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
v : V
hv : v ∈ M.verts
w : V
hvw : M.Adj v w
hw : ∀ (y : V), (fun (w : V) ↦ M.Adj v w) y → y = w
h₁ :
  (fun (w : V) ↦ (M.induce (M.verts ∩ (G.connectedComponentMk v).supp)).Adj v w) w ∧
    ∀ (y : V), (fun (w : V) ↦ (M.induce (M.verts ∩ (G.connectedComponentMk v).supp)).Adj v w) y → y = w
⊢ ∃! w : V, (M.induce (M.verts ∩ (G.connectedComponentMk v).supp)).Adj v w

Tactic:
use w