awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
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
⊢ M₁.verts = M₂.verts
have rw₁ : Eq.{u_1 + 1} (α := Set V) (⋃ e ∈ M₁.edgeSet, (↑e : Set V)) (⋃ e ∈ M₂.edgeSet, (↑e : Set V))
Tactic: rw [h₁.verts_eq_biUnion_edgeSet, h₂.verts_eq_biUnion_edgeSet, h]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
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))
⊢ M₁.verts = M₂.verts
have rw₂ : Eq.{u_1 + 1} (α := Set V) (⋃ e ∈ M₂.edgeSet, (↑e : Set V)) (⋃ e ∈ M₂.edgeSet, (↑e : Set V))
Tactic: rw [h₁.verts_eq_biUnion_edgeSet, h₂.verts_eq_biUnion_edgeSet, h]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
⊢ M.support = M.verts
have refine : ∀ (v : V) (hv : v ∈ M.verts), v ∈ M.support
Tactic: refine M.support_subset_verts.antisymm fun v hv => ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
v : V
hv : v ∈ M.verts
⊢ v ∈ M.support
have obtain : ∀ (w : V) (hvw : M.Adj v w), v ∈ M.support
Tactic: obtain ⟨w, hvw, -⟩ := h hv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst : Fintype (↑M.verts : Type u_1)
h : M.IsMatching
⊢ Even M.verts.toFinset.card
have h₁ : ∀ v ∈ M.verts, M.degree v = 1
Tactic: rw [isMatching_iff_forall_degree] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
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
⊢ Even M.verts.toFinset.card
have h₁ : M.verts.toFinset.card = M.coe.edgeFinset.card + M.coe.edgeFinset.card
Tactic: use M.coe.edgeFinset.card
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
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 = M.coe.edgeFinset.card + M.coe.edgeFinset.card
have h₁ : M.verts.toFinset.card = ∑ v : (↑M.verts : Type u_1), M.coe.degree v
Tactic: rw [← two_mul, ← M.coe.sum_degrees_eq_twice_card_edges]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst : Fintype (↑M.verts : Type u_1)
h : M.IsMatching
⊢ Even M.verts.toFinset.card
have rw : ∀ (h : ∀ v ∈ M.verts, M.degree v = 1), 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]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
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
⊢ Even M.verts.toFinset.card
have h₁ : ∀ (h : ∀ v ∈ M.verts, M.degree v = 1), M.verts.toFinset.card = M.coe.edgeFinset.card + M.coe.edgeFinset.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]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
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
⊢ Even M.verts.toFinset.card
have h₂ : ∀ (h : ∀ v ∈ M.verts, M.degree v = 1), M.verts.toFinset.card = ∑ v : (↑M.verts : Type u_1), M.coe.degree v
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]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
⊢ M.IsPerfectMatching ↔ ∀ (v : V), ∃! w : V, M.Adj v w
have refine_1 : M.IsPerfectMatching → ∀ (v : V), ∃! w : V, M.Adj v w
Tactic: refine ⟨?_, fun hm => ⟨fun v _ => hm v, fun v => ?_⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
refine_1 : M.IsPerfectMatching → ∀ (v : V), ∃! w : V, M.Adj v w
⊢ M.IsPerfectMatching ↔ ∀ (v : V), ∃! w : V, M.Adj v w
have refine_2 : ∀ (hm : ∀ (v : V), ∃! w : V, M.Adj v w) (v : V), v ∈ M.verts
Tactic: refine ⟨?_, fun hm => ⟨fun v _ => hm v, fun v => ?_⟩⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
hm : ∀ (v : V), ∃! w : V, M.Adj v w
v : V
⊢ v ∈ M.verts
have refine_2 : ∀ (w : V) (hw : M.Adj v w), v ∈ M.verts
Tactic: obtain ⟨w, hw, -⟩ := hm v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
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
⊢ ∃! w : V, (M.induce (M.verts ∩ c.supp)).Adj v w
have obtain : ∀ (hv : v ∈ M.verts), ∃! w : V, (M.induce (M.verts ∩ (G.connectedComponentMk v).supp)).Adj v w
Tactic: obtain ⟨hv, rfl⟩ := hv
Cleared hypotheses: c, hv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
v : V
hv : v ∈ M.verts
⊢ ∃! w : V, (M.induce (M.verts ∩ (G.connectedComponentMk v).supp)).Adj v w
have 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
Tactic: obtain ⟨w, hvw, hw⟩ := h hv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
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
⊢ ∃! w : V, (M.induce (M.verts ∩ (G.connectedComponentMk v).supp)).Adj v w
have 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
Tactic: use w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u : Set V
hc : G.IsClique u
hu : u.Finite
⊢ Even u.ncard ↔ ∃ (M : G.Subgraph), M.verts = u ∧ M.IsMatching
have refine : ∀ (h : Even u.ncard), ∃ (M : G.Subgraph), M.verts = u ∧ M.IsMatching
Tactic: refine ⟨fun h ↦ ?_, by
    rintro ⟨M, rfl, hMr⟩
    simpa [Set.ncard_eq_toFinset_card _ hu, Set.toFinite_toFinset,
      ← Set.toFinset_card] using @hMr.even_card _ _ _ hu.fintype⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
u : Set V
hc : G.IsClique u
hu : u.Finite
h : Even u.ncard
⊢ ∃ (M : G.Subgraph), M.verts = u ∧ M.IsMatching
have obtain : ∀ (t u : Set V) (hc : G.IsClique (t ∪ u)) (hu : (t ∪ u).Finite) (h : Even (t ∪ u).ncard) (hd : Disjoint t u)
  (hcard : t.ncard = u.ncard), ∃ (M : G.Subgraph), M.verts = t ∪ u ∧ M.IsMatching
Tactic: obtain ⟨t, u, rfl, hd, hcard⟩ := Set.exists_union_disjoint_ncard_eq_of_even h
Cleared hypotheses: u, hc, hu, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
t u : Set V
hc : G.IsClique (t ∪ u)
hu : (t ∪ u).Finite
h : Even (t ∪ u).ncard
hd : Disjoint t u
hcard : t.ncard = u.ncard
⊢ Nonempty.{max 1 (u_1 + 1)} ((↑t : Type u_1) ≃ (↑u : Type u_1))
have rw : Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑t.ncard : Cardinal.{u_1}) (↑u.ncard : Cardinal.{u_1})
Tactic: rw [← Cardinal.eq, ← t.cast_ncard (Set.finite_union.mp hu).1,
      ← u.cast_ncard (Set.finite_union.mp hu).2]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
t u : Set V
hc : G.IsClique (t ∪ u)
hu : (t ∪ u).Finite
h : Even (t ∪ u).ncard
hd : Disjoint t u
hcard : t.ncard = u.ncard
⊢ ∃ (M : G.Subgraph), M.verts = t ∪ u ∧ M.IsMatching
have obtain : ∀ (f : (↑t : Type u_1) ≃ (↑u : Type u_1)), ∃ (M : G.Subgraph), M.verts = t ∪ u ∧ M.IsMatching
Tactic: obtain ⟨f⟩ : Nonempty (t ≃ u) := by
    rw [← Cardinal.eq, ← t.cast_ncard (Set.finite_union.mp hu).1,
      ← u.cast_ncard (Set.finite_union.mp hu).2]
    exact congrArg Nat.cast hcard
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst : Fintype V
inst_1 : DecidableEq V
inst_2 : DecidableRel G.Adj
c : G.ConnectedComponent
hM : M.IsPerfectMatching
this : DecidablePred fun (x : V) ↦ x ∈ (M.induce c.supp).verts := fun (a : V) ↦ G.instDecidableMemSupp c a
⊢ Even (Fintype.card.{u_1} (↑c.supp : Type u_1))
have this₁ : Even (M.induce c.supp).verts.toFinset.card
Tactic: have := (hM.induce_connectedComponent_isMatching c).even_card
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst : Fintype V
inst_1 : DecidableEq V
inst_2 : DecidableRel G.Adj
c : G.ConnectedComponent
hM : M.IsPerfectMatching
this_1 : DecidablePred fun (x : V) ↦ x ∈ (M.induce c.supp).verts := fun (a : V) ↦ G.instDecidableMemSupp c a
this : Even (M.induce c.supp).verts.toFinset.card
⊢ Even (Fintype.card.{u_1} (↑c.supp : Type u_1))
have this₁ : Even (Fintype.card.{u_1} (↑c.supp : Type u_1))
Tactic: simp only [Subgraph.induce_verts, Set.toFinset_card] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst : Finite V
u : Set V
hM : M.IsPerfectMatching
c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)
⊢ ∃ w ∈ u,
    ∃ (v : (↑(Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) : Type u_1)),
      M.Adj (↑v : V) w ∧ v ∈ (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp
have by_contra! : ∀
  (h :
    ∀ (w : V) (_ : w ∈ u) (v : (↑(Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) : Type u_1))
      (_ : M.Adj (↑v : V) w), v ∉ (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp),
  False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst : Finite V
u : Set V
hM : M.IsPerfectMatching
c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)
h :
  ∀ (w : V) (_ : w ∈ u) (v : (↑(Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) : Type u_1)) (_ : M.Adj (↑v : V) w),
    v ∉ (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp
v : V
hv :
  v ∈
    (M.induce
        (Subtype.val (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) ''
          (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp)).verts
⊢ ∃! w : V,
    (M.induce
          (Subtype.val (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) ''
            (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp)).Adj
      v w
have obtain : ∀ (w : V) (hw : (fun (w : V) ↦ M.Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ M.Adj v w) y → y = w),
  ∃! w : V,
    (M.induce
          (Subtype.val (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) ''
            (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp)).Adj
      v w
Tactic: obtain ⟨w, hw⟩ := hM.1 (hM.2 v)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst : Finite V
u : Set V
hM : M.IsPerfectMatching
c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)
h :
  ∀ (w : V) (_ : w ∈ u) (v : (↑(Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) : Type u_1)) (_ : M.Adj (↑v : V) w),
    v ∉ (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp
v : V
hv :
  v ∈
    (M.induce
        (Subtype.val (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) ''
          (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp)).verts
w : V
hw : (fun (w : V) ↦ M.Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ M.Adj v w) y → y = w
⊢ ∃! w : V,
    (M.induce
          (Subtype.val (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) ''
            (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp)).Adj
      v w
have obtain : ∀ (v' : V) (hv' : v' ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u))
  (hv :
    Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv' ∈
      (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp)
  (hw :
    (fun (w : V) ↦
          M.Adj (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv') : V)
            w)
        w ∧
      ∀ (y : V),
        (fun (w : V) ↦
              M.Adj
                (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv') : V)
                w)
            y →
          y = w),
  ∃! w : V,
    (M.induce
          (Subtype.val (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) ''
            (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp)).Adj
      (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv') : V) w
Tactic: obtain ⟨⟨v', hv'⟩, ⟨hv, rfl⟩⟩ := hv
Cleared hypotheses: v, hv, hw
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst : Finite V
u : Set V
hM : M.IsPerfectMatching
c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)
h :
  ∀ (w : V) (_ : w ∈ u) (v : (↑(Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) : Type u_1)) (_ : M.Adj (↑v : V) w),
    v ∉ (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp
w v' : V
hv' : v' ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)
hv :
  Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv' ∈
    (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp
hw :
  (fun (w : V) ↦
        M.Adj (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv') : V) w)
      w ∧
    ∀ (y : V),
      (fun (w : V) ↦
            M.Adj (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv') : V)
              w)
          y →
        y = w
⊢ ∃! w : V,
    (M.induce
          (Subtype.val (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) ''
            (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp)).Adj
      (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv') : V) w
have h₁ : (fun (w : V) ↦
      (M.induce
            (Subtype.val (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) ''
              (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp)).Adj
        (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv') : V) w)
    w ∧
  ∀ (y : V),
    (fun (w : V) ↦
          (M.induce
                (Subtype.val (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) ''
                  (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp)).Adj
            (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv') : V) w)
        y →
      y = w
Tactic: use w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst : Finite V
u : Set V
hM : M.IsPerfectMatching
c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)
h :
  ∀ (w : V) (_ : w ∈ u) (v : (↑(Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) : Type u_1)) (_ : M.Adj (↑v : V) w),
    v ∉ (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp
w v' : V
hv' : v' ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)
hv :
  Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv' ∈
    (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp
hw :
  (fun (w : V) ↦
        M.Adj (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv') : V) w)
      w ∧
    ∀ (y : V),
      (fun (w : V) ↦
            M.Adj (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv') : V)
              w)
          y →
        y = w
⊢ (fun (w : V) ↦
        (M.induce
              (Subtype.val (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) ''
                (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp)).Adj
          (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv') : V) w)
      w ∧
    ∀ (y : V),
      (fun (w : V) ↦
            (M.induce
                  (Subtype.val (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) ''
                    (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp)).Adj
              (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv') : V) w)
          y →
        y = w
have hwnu : w ∉ u
Tactic: have hwnu : w ∉ u := fun hw' ↦ h w hw' ⟨v', hv'⟩ (hw.1) hv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst : Finite V
u : Set V
hM : M.IsPerfectMatching
c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)
h :
  ∀ (w : V) (_ : w ∈ u) (v : (↑(Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) : Type u_1)) (_ : M.Adj (↑v : V) w),
    v ∉ (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp
w v' : V
hv' : v' ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)
hv :
  Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv' ∈
    (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp
hw :
  (fun (w : V) ↦
        M.Adj (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv') : V) w)
      w ∧
    ∀ (y : V),
      (fun (w : V) ↦
            M.Adj (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv') : V)
              w)
          y →
        y = w
hwnu : w ∉ u
⊢ (fun (w : V) ↦
        (M.induce
              (Subtype.val (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) ''
                (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp)).Adj
          (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv') : V) w)
      w ∧
    ∀ (y : V),
      (fun (w : V) ↦
            (M.induce
                  (Subtype.val (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) ''
                    (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp)).Adj
              (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv') : V) w)
          y →
        y = w
have h₁ : w ∈
  Subtype.val (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) ''
    (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp
Tactic: refine ⟨⟨⟨⟨v', hv'⟩, hv, rfl⟩, ?_, hw.1⟩, fun _ hy ↦ hw.2 _ hy.2.2⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst : Finite V
u : Set V
hM : M.IsPerfectMatching
c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)
h :
  ∀ (w : V) (_ : w ∈ u) (v : (↑(Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) : Type u_1)) (_ : M.Adj (↑v : V) w),
    v ∉ (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp
w v' : V
hv' : v' ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)
hv :
  Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv' ∈
    (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp
hw :
  (fun (w : V) ↦
        M.Adj (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv') : V) w)
      w ∧
    ∀ (y : V),
      (fun (w : V) ↦
            M.Adj (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv') : V)
              w)
          y →
        y = w
hwnu : w ∉ u
⊢ w ∈
    Subtype.val (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) ''
      (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp
have h₁ : Subgraph.Adj (G := G) (Subgraph.deleteVerts ⊤ u)
  (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv') : V) w
Tactic: apply ConnectedComponent.mem_coe_supp_of_adj ⟨⟨v', hv'⟩, ⟨hv, rfl⟩⟩ ⟨by trivial, hwnu⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst : Finite V
u : Set V
hM : M.IsPerfectMatching
c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)
h :
  ∀ (w : V) (_ : w ∈ u) (v : (↑(Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) : Type u_1)) (_ : M.Adj (↑v : V) w),
    v ∉ (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp
w v' : V
hv' : v' ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)
hv :
  Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv' ∈
    (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp
hw :
  (fun (w : V) ↦
        M.Adj (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv') : V) w)
      w ∧
    ∀ (y : V),
      (fun (w : V) ↦
            M.Adj (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv') : V)
              w)
          y →
        y = w
hwnu : w ∉ u
⊢ Subgraph.Adj (G := G) (Subgraph.deleteVerts ⊤ u)
    (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) v' hv') : V) w
have h₁ : ∀ (hv' : v' ∉ u), v' ∉ u
Tactic: simp only [Subgraph.induce_verts, Subgraph.verts_top, Set.mem_diff, Set.mem_univ, true_and,
      Subgraph.induce_adj, hwnu, not_false_eq_true, and_self, Subgraph.top_adj, M.adj_sub hw.1,
      and_true] at hv' ⊢
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst : Finite V
u : Set V
hM : M.IsPerfectMatching
c : (↑(oddComponents (Subgraph.coe (Subgraph.deleteVerts ⊤ u))) : Type u_1)
h :
  ∀ (w : V) (_ : w ∈ u) (v : (↑(Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) : Type u_1)) (_ : M.Adj (↑v : V) w),
    v ∉ (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp
⊢ False
have hMmatch : (M.induce
    (Subtype.val (p := fun (x : V) ↦ x ∈ Subgraph.verts (G := G) (Subgraph.deleteVerts ⊤ u)) ''
      (↑c : (⊤.deleteVerts u).coe.ConnectedComponent).supp)).IsMatching
Tactic: have hMmatch : (M.induce c.val.supp).IsMatching := by
    intro v hv
    obtain ⟨w, hw⟩ := hM.1 (hM.2 v)
    obtain ⟨⟨v', hv'⟩, ⟨hv, rfl⟩⟩ := hv
    use w
    have hwnu : w ∉ u := fun hw' ↦ h w hw' ⟨v', hv'⟩ (hw.1) hv
    refine ⟨⟨⟨⟨v', hv'⟩, hv, rfl⟩, ?_, hw.1⟩, fun _ hy ↦ hw.2 _ hy.2.2⟩
    apply ConnectedComponent.mem_coe_supp_of_adj ⟨⟨v', hv'⟩, ⟨hv, rfl⟩⟩ ⟨by trivial, hwnu⟩
    simp only [Subgraph.induce_verts, Subgraph.verts_top, Set.mem_diff, Set.mem_univ, true_and,
      Subgraph.induce_adj, hwnu, not_false_eq_true, and_self, Subgraph.top_adj, M.adj_sub hw.1,
      and_true] at hv' ⊢
    trivial