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
G' : G.Subgraph
M : G'.coe.Subgraph
hM : M.IsMatching
v : V
hv : v ∈ (Subgraph.coeSubgraph M).verts
w : (↑G'.verts : Type u_1)
hw :
  (fun (w : (↑G'.verts : Type u_1)) ↦ M.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v ⋯) w) w ∧
    ∀ (y : (↑G'.verts : Type u_1)),
      (fun (w : (↑G'.verts : Type u_1)) ↦ M.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v ⋯) w) y → y = w
⊢ (fun (w : V) ↦ (Subgraph.coeSubgraph M).Adj v w) (↑w : V)
have h : ∀ (v_1 : { x : V // x ∈ G'.verts }) (hv : v_1 ∈ M.verts ∧ (↑v_1 : V) = v), (Subgraph.coeSubgraph M).Adj v (↑w : V)
Tactic: obtain ⟨v, hv⟩ := (Set.mem_image _ _ _).mp <| (Subgraph.verts_coeSubgraph M).symm ▸ hv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
G' : G.Subgraph
M : G'.coe.Subgraph
hM : M.IsMatching
v_1 : V
hv_1 : v_1 ∈ (Subgraph.coeSubgraph M).verts
w : (↑G'.verts : Type u_1)
hw :
  (fun (w : (↑G'.verts : Type u_1)) ↦ M.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v_1 ⋯) w) w ∧
    ∀ (y : (↑G'.verts : Type u_1)),
      (fun (w : (↑G'.verts : Type u_1)) ↦ M.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v_1 ⋯) w) y → y = w
v : { x : V // x ∈ G'.verts }
hv : v ∈ M.verts ∧ (↑v : V) = v_1
⊢ (Subgraph.coeSubgraph M).Adj v_1 (↑w : V)
have h : ∃ (h : v_1 ∈ G'.verts), M.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v_1 sorry) w
Tactic: simp only [coeSubgraph_adj, Subtype.coe_eta, Subtype.coe_prop, exists_const]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
G' : G.Subgraph
M : G'.coe.Subgraph
hM : M.IsMatching
v : V
hv : v ∈ (Subgraph.coeSubgraph M).verts
w : (↑G'.verts : Type u_1)
hw :
  (fun (w : (↑G'.verts : Type u_1)) ↦ M.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v ⋯) w) w ∧
    ∀ (y : (↑G'.verts : Type u_1)),
      (fun (w : (↑G'.verts : Type u_1)) ↦ M.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v ⋯) w) y → y = w
y : V
hy : (fun (w : V) ↦ (Subgraph.coeSubgraph M).Adj v w) y
⊢ y = (↑w : V)
have w₁ : v ∈ G'.verts
Tactic: obtain ⟨_, hw', hvw⟩ := (coeSubgraph_adj _ _ _).mp hy
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
G' : G.Subgraph
M : G'.coe.Subgraph
hM : M.IsMatching
v : V
hv : v ∈ (Subgraph.coeSubgraph M).verts
w : (↑G'.verts : Type u_1)
hw :
  (fun (w : (↑G'.verts : Type u_1)) ↦ M.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v ⋯) w) w ∧
    ∀ (y : (↑G'.verts : Type u_1)),
      (fun (w : (↑G'.verts : Type u_1)) ↦ M.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v ⋯) w) y → y = w
y : V
hy : (fun (w : V) ↦ (Subgraph.coeSubgraph M).Adj v w) y
w₁ : v ∈ G'.verts
⊢ y = (↑w : V)
have hw' : y ∈ G'.verts
Tactic: obtain ⟨_, hw', hvw⟩ := (coeSubgraph_adj _ _ _).mp hy
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
G' : G.Subgraph
M : G'.coe.Subgraph
hM : M.IsMatching
v : V
hv : v ∈ (Subgraph.coeSubgraph M).verts
w : (↑G'.verts : Type u_1)
hw :
  (fun (w : (↑G'.verts : Type u_1)) ↦ M.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v ⋯) w) w ∧
    ∀ (y : (↑G'.verts : Type u_1)),
      (fun (w : (↑G'.verts : Type u_1)) ↦ M.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v ⋯) w) y → y = w
y : V
hy : (fun (w : V) ↦ (Subgraph.coeSubgraph M).Adj v w) y
w₁ : v ∈ G'.verts
hw' : y ∈ G'.verts
⊢ y = (↑w : V)
have hvw : M.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v w₁) (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) y hw')
Tactic: obtain ⟨_, hw', hvw⟩ := (coeSubgraph_adj _ _ _).mp hy
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
G' : G.Subgraph
M : G'.coe.Subgraph
hM : M.IsMatching
v : V
hv : v ∈ (Subgraph.coeSubgraph M).verts
w : (↑G'.verts : Type u_1)
hw :
  (fun (w : (↑G'.verts : Type u_1)) ↦ M.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v ⋯) w) w ∧
    ∀ (y : (↑G'.verts : Type u_1)),
      (fun (w : (↑G'.verts : Type u_1)) ↦ M.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v ⋯) w) y → y = w
y : V
hy : (fun (w : V) ↦ (Subgraph.coeSubgraph M).Adj v w) y
w_1 : v ∈ G'.verts
hw' : y ∈ G'.verts
hvw : M.Adj (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) v w_1) (Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) y hw')
⊢ y = (↑w : V)
have h : y = (↑(Subtype.mk (p := fun (x : V) ↦ x ∈ G'.verts) y hw') : V)
Tactic: rw [← hw.2 ⟨y, hw'⟩ hvw]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
s t : Set V
h_1 : 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 w : V
h :
  (∃ (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
⊢ G.Adj v w
have inl : ∀ (hv : v ∈ s),
  G.Adj v (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) v hv)) : V)
Tactic: obtain (⟨hv, rfl⟩ | ⟨hw, rfl⟩) := h
Cleared hypotheses: w, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
s t : Set V
h_1 : 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 w : V
h :
  (∃ (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
inl :
  ∀ (hv : v ∈ s),
    G.Adj v (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) v hv)) : V)
⊢ G.Adj v w
have inr : ∀ (hw : w ∈ s),
  G.Adj (↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) w hw)) : V) w
Tactic: obtain (⟨hv, rfl⟩ | ⟨hw, rfl⟩) := h
Cleared hypotheses: v, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
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)
⊢ ∃ (M : G.Subgraph), M.verts = s ∪ t ∧ M.IsMatching
have h₁ : verts (G := G)
      { verts := s ∪ t,
        Adj := fun (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,
        adj_sub := sorry, edge_vert := sorry, symm := sorry : G.Subgraph } =
    s ∪ t ∧
  IsMatching (G := G)
    { verts := s ∪ t,
      Adj := fun (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,
      adj_sub := sorry, edge_vert := sorry, symm := sorry }
Tactic: use {
    verts := s ∪ t
    Adj := fun v w ↦ (∃ h : v ∈ s, f ⟨v, h⟩ = w) ∨ (∃ h : w ∈ s, f ⟨w, h⟩ = v)
    adj_sub := by
      intro v w h
      obtain (⟨hv, rfl⟩ | ⟨hw, rfl⟩) := h
      · exact hadj ⟨v, _⟩
      · exact (hadj ⟨w, _⟩).symm
    edge_vert := by grind }
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
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)
⊢ verts (G := G)
        { verts := s ∪ t,
          Adj := fun (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,
          adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ : G.Subgraph } =
      s ∪ t ∧
    IsMatching (G := G)
      { verts := s ∪ t,
        Adj := fun (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,
        adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }
have h₁ : ∀ ⦃v : V⦄,
  v ∈ s ∨ v ∈ t →
    ∃! 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: simp only [Subgraph.IsMatching, Set.mem_union, true_and]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
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
hv : v ∈ s ∨ v ∈ t
⊢ ∃! 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
have h₁ : ∀ (hl : v ∈ s),
  ∃! 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: rcases hv with hl | hr
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
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
hv : v ∈ s ∨ v ∈ t
h₁ :
  ∀ (hl : v ∈ s),
    ∃! 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
⊢ ∃! 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
have h₂ : ∀ (hr : v ∈ t),
  ∃! 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: rcases hv with hl | hr
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
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
hl : v ∈ s
⊢ ∃! 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
have 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 : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) v hl)) : 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 : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) v hl)) : V)
Tactic: use f ⟨v, hl⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
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
hl : v ∈ s
⊢ (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 : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) v hl)) : 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 : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) v hl)) : V)
have h₁ : ∀ (y : V),
  ((↑((f : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) v sorry)) : 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 : (a : (↑s : Type u_1)) → (↑t : Type u_1)) (Subtype.mk (p := fun (x : V) ↦ x ∈ s) v hl)) : V)
Tactic: simp only [hl, exists_const, true_or, exists_true_left, true_and]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
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
⊢ ∃! 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
have 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)
Tactic: use f.symm ⟨v, hr⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
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
⊢ (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)
have 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)
Tactic: simp only [Subtype.coe_eta, Equiv.apply_symm_apply, Subtype.coe_prop, exists_const, or_true,
      true_and]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
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
⊢ ∃! w : W, (Subgraph.map f M).Adj ((f : (a : V) → W) v) w
have 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
Tactic: obtain ⟨v', hv'⟩ := hM hv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
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, (Subgraph.map f M).Adj ((f : (a : V) → W) v) w
have 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'
Tactic: use f v'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
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'
have h : ∀ (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⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (hypothesis)
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)
⊢ Eq.{u_2 + 1} (α := W) ((f : (a : V) → W) w' : W) ((f : (a : V) → W) v' : W)
have hw₁ : M.Adj v w'
Tactic: cases hf hw'.symm
Cleared hypotheses: w, hw, hw'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (hypothesis)
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) w' : W) ((f : (a : V) → W) v' : W)
have hw'₁ : Eq.{u_2 + 1} (α := W) ((f : (a : V) → W) v : W) ((f : (a : V) → W) v : W)
Tactic: cases hf hw'.symm
Cleared hypotheses: w, hw, hw'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
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)
⊢ Eq.{u_2 + 1} (α := W) ((f : (a : V) → W) w' : W) ((f : (a : V) → W) v' : W)
have h : Eq.{u_2 + 1} (α := W) ((f : (a : V) → W) v' : W) ((f : (a : V) → W) v' : W)
Tactic: rw [hv'.2 w' hw]
-- 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.verts = ⋃ e ∈ M.edgeSet, (↑e : Set V)
have refine_1 : ∀ (v : V) (hv : v ∈ M.verts), ∃ (i : Sym2 V) (_ : i ∈ M.edgeSet), v ∈ (↑i : Set V)
Tactic: refine Set.ext fun v ↦ .trans ⟨fun hv ↦ ?_, fun ⟨e, he, hv⟩ ↦ ?_⟩ Set.mem_iUnion₂.symm
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
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)
⊢ M.verts = ⋃ e ∈ M.edgeSet, (↑e : Set V)
have 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
Tactic: refine Set.ext fun v ↦ .trans ⟨fun hv ↦ ?_, fun ⟨e, he, hv⟩ ↦ ?_⟩ Set.mem_iUnion₂.symm
-- 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
⊢ ∃ (i : Sym2 V) (_ : i ∈ M.edgeSet), v ∈ (↑i : Set V)
have 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)
Tactic: have ⟨u, he, _⟩ := h hv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
⊢ Set.InjOn.{u_1, u_1} (α := G.Subgraph) edgeSet (setOf IsMatching)
have 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
Tactic: refine fun M₁ h₁ M₂ h₂ h ↦ Subgraph.ext ?_ <| Sym2.fromRel_eq_fromRel_iff_eq .. |>.mp 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
⊢ M₁.verts = M₂.verts
have rw : ⋃ e ∈ M₁.edgeSet, (↑e : Set V) = M₂.verts
Tactic: rw [h₁.verts_eq_biUnion_edgeSet, h₂.verts_eq_biUnion_edgeSet, h]