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
v w : V
h : M.IsMatching
ha : M.Adj v w
⊢ h.toEdge (Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) v ⋯) =
    h.toEdge (Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) w ⋯)
have rw : Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ M.edgeSet) s(v, w) ha =
  h.toEdge (Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) w sorry)
Tactic: rw [h.toEdge_eq_of_adj ha, h.toEdge_eq_of_adj ha.symm, Subtype.mk_eq_mk, Sym2.eq_swap]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
v w : V
h : M.IsMatching
ha : M.Adj v w
rw :
  Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ M.edgeSet) s(v, w) ha =
    h.toEdge (Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) w ⋯)
⊢ h.toEdge (Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) v ⋯) =
    h.toEdge (Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) w ⋯)
have rw₁ : Eq (α := (↑M.edgeSet : Type u_1)) (Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ M.edgeSet) s(v, w) ha)
  (Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ M.edgeSet) s(w, v) sorry)
Tactic: rw [h.toEdge_eq_of_adj ha, h.toEdge_eq_of_adj ha.symm, Subtype.mk_eq_mk, Sym2.eq_swap]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
v w : V
h : M.IsMatching
ha : M.Adj v w
rw :
  Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ M.edgeSet) s(v, w) ha =
    h.toEdge (Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) w ⋯)
rw₁ :
  Eq (α := (↑M.edgeSet : Type u_1)) (Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ M.edgeSet) s(v, w) ha)
    (Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ M.edgeSet) s(w, v) ⋯)
⊢ h.toEdge (Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) v ⋯) =
    h.toEdge (Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) w ⋯)
have rw₂ : s(v, w) = s(w, v)
Tactic: rw [h.toEdge_eq_of_adj ha, h.toEdge_eq_of_adj ha.symm, Subtype.mk_eq_mk, Sym2.eq_swap]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
v w : V
h : M.IsMatching
ha : M.Adj v w
rw :
  Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ M.edgeSet) s(v, w) ha =
    h.toEdge (Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) w ⋯)
rw₁ :
  Eq (α := (↑M.edgeSet : Type u_1)) (Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ M.edgeSet) s(v, w) ha)
    (Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ M.edgeSet) s(w, v) ⋯)
rw₂ : s(v, w) = s(w, v)
⊢ h.toEdge (Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) v ⋯) =
    h.toEdge (Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) w ⋯)
have rw₃ : s(w, v) = s(w, v)
Tactic: rw [h.toEdge_eq_of_adj ha, h.toEdge_eq_of_adj ha.symm, Subtype.mk_eq_mk, Sym2.eq_swap]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
u v : V
h : M.IsMatching
huv : M.Adj u v
⊢ h.toEdge ⁻¹' {Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ M.edgeSet) s(u, v) huv} =
    {Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) u ⋯, Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) v ⋯}
have refine_1 : ∀ (w : (↑M.verts : Type u_1)) (hw : w ∈ h.toEdge ⁻¹' {Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ M.edgeSet) s(u, v) huv}),
  Membership.mem (γ := Set (↑M.verts : Type u_1))
    {Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) u sorry, Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) v sorry} w
Tactic: refine Set.ext fun w ↦ ⟨fun hw ↦ ?_, fun hw ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
u v : V
h : M.IsMatching
huv : M.Adj u v
refine_1 :
  ∀ (w : (↑M.verts : Type u_1))
    (hw : w ∈ h.toEdge ⁻¹' {Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ M.edgeSet) s(u, v) huv}),
    Membership.mem (γ := Set (↑M.verts : Type u_1))
      {Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) u ⋯, Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) v ⋯} w
⊢ h.toEdge ⁻¹' {Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ M.edgeSet) s(u, v) huv} =
    {Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) u ⋯, Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) v ⋯}
have refine_2 : ∀ (w : (↑M.verts : Type u_1))
  (hw :
    Membership.mem (γ := Set (↑M.verts : Type u_1))
      {Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) u sorry, Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) v sorry} w),
  w ∈ h.toEdge ⁻¹' {Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ M.edgeSet) s(u, v) huv}
Tactic: refine Set.ext fun w ↦ ⟨fun hw ↦ ?_, fun hw ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
u v : V
h : M.IsMatching
huv : M.Adj u v
w : (↑M.verts : Type u_1)
hw :
  Membership.mem (γ := Set (↑M.verts : Type u_1))
    {Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) u ⋯, Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) v ⋯} w
⊢ w ∈ h.toEdge ⁻¹' {Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ M.edgeSet) s(u, v) huv}
have refine_2 : Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) u sorry ∈
  h.toEdge ⁻¹' {Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ M.edgeSet) s(u, v) huv}
Tactic: rcases hw with rfl | rfl
Cleared hypotheses: w, hw
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
u v : V
h : M.IsMatching
huv : M.Adj u v
w : (↑M.verts : Type u_1)
hw :
  Membership.mem (γ := Set (↑M.verts : Type u_1))
    {Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) u ⋯, Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) v ⋯} w
refine_2 :
  Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) u ⋯ ∈
    h.toEdge ⁻¹' {Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ M.edgeSet) s(u, v) huv}
⊢ w ∈ h.toEdge ⁻¹' {Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ M.edgeSet) s(u, v) huv}
have refine_2₁ : Subtype.mk (p := fun (x : V) ↦ x ∈ M.verts) v sorry ∈
  h.toEdge ⁻¹' {Subtype.mk (p := fun (x : Sym2 V) ↦ x ∈ M.edgeSet) s(u, v) huv}
Tactic: rcases hw with rfl | rfl
Cleared hypotheses: w, hw
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
hGG' : G ≤ G'
v : V
hv : v ∈ (Subgraph.map (Hom.ofLE hGG') M).verts
⊢ ∃! w : V, (Subgraph.map (Hom.ofLE hGG') M).Adj v w
have obtain : ∀ (w : V) (hv : w ∈ M.verts) (hv' : (Hom.ofLE hGG' : (a : V) → V) w = v),
  ∃! w : V, (Subgraph.map (Hom.ofLE hGG') M).Adj v w
Tactic: obtain ⟨_, hv, hv'⟩ := Set.mem_image _ _ _ |>.mp hv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
hGG' : G ≤ G'
v : V
hv_1 : v ∈ (Subgraph.map (Hom.ofLE hGG') M).verts
w : V
hv : w ∈ M.verts
hv' : (Hom.ofLE hGG' : (a : V) → V) w = v
⊢ ∃! w : V, (Subgraph.map (Hom.ofLE hGG') M).Adj v w
have obtain : ∀ (w_1 : V) (hw : (fun (w_2 : V) ↦ M.Adj w w_2) w_1 ∧ ∀ (y : V), (fun (w_2 : V) ↦ M.Adj w w_2) y → y = w_1),
  ∃! w : V, (Subgraph.map (Hom.ofLE hGG') M).Adj v w
Tactic: obtain ⟨w, hw⟩ := h hv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
hGG' : G ≤ G'
v : V
hv_1 : v ∈ (Subgraph.map (Hom.ofLE hGG') M).verts
w_1 : V
hv : w_1 ∈ M.verts
hv' : (Hom.ofLE hGG' : (a : V) → V) w_1 = v
w : V
hw : (fun (w : V) ↦ M.Adj w_1 w) w ∧ ∀ (y : V), (fun (w : V) ↦ M.Adj w_1 w) y → y = w
⊢ ∃! w : V, (Subgraph.map (Hom.ofLE hGG') M).Adj v w
have h₁ : (fun (w : V) ↦ (Subgraph.map (Hom.ofLE hGG') M).Adj v w) w ∧
  ∀ (y : V), (fun (w : V) ↦ (Subgraph.map (Hom.ofLE hGG') M).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
M M' : G.Subgraph
hM : M.IsMatching
hM' : M'.IsMatching
hd_1 : Disjoint M.support M'.support
v : V
hv : v ∈ (M ⊔ M').verts
N N' : G.Subgraph
hN : N.IsMatching
hd : Disjoint N.support N'.support
hmN : v ∈ N.verts
⊢ ∃! w : V, (N ⊔ N').Adj v w
have obtain : ∀ (w : V) (hw : (fun (w : V) ↦ N.Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ N.Adj v w) y → y = w),
  ∃! w : V, (N ⊔ N').Adj v w
Tactic: obtain ⟨w, hw⟩ := hN hmN
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
M M' : G.Subgraph
hM : M.IsMatching
hM' : M'.IsMatching
hd_1 : Disjoint M.support M'.support
v : V
hv : v ∈ (M ⊔ M').verts
N N' : G.Subgraph
hN : N.IsMatching
hd : Disjoint N.support N'.support
hmN : v ∈ N.verts
w : V
hw : (fun (w : V) ↦ N.Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ N.Adj v w) y → y = w
⊢ ∃! w : V, (N ⊔ N').Adj v w
have h : (fun (w : V) ↦ (N ⊔ N').Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ (N ⊔ N').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
M M' : G.Subgraph
hM : M.IsMatching
hM' : M'.IsMatching
hd_1 : Disjoint M.support M'.support
v : V
hv : v ∈ (M ⊔ M').verts
N N' : G.Subgraph
hN : N.IsMatching
hd : Disjoint N.support N'.support
hmN : v ∈ N.verts
w : V
hw : (fun (w : V) ↦ N.Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ N.Adj v w) y → y = w
⊢ (fun (w : V) ↦ (N ⊔ N').Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ (N ⊔ N').Adj v w) y → y = w
have h : ∀ (y : V), (fun (w : V) ↦ (N ⊔ N').Adj v w) y → y = w
Tactic: refine ⟨sup_adj.mpr (.inl hw.1), ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
M M' : G.Subgraph
hM : M.IsMatching
hM' : M'.IsMatching
hd_1 : Disjoint M.support M'.support
v : V
hv : v ∈ (M ⊔ M').verts
N N' : G.Subgraph
hN : N.IsMatching
hd : Disjoint N.support N'.support
hmN : v ∈ N.verts
w : V
hw : (fun (w : V) ↦ N.Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ N.Adj v w) y → y = w
y : V
h : N'.Adj v y
⊢ y = w
have h₁ : ∀ (hd : ∀ ⦃a : V⦄, a ∈ N.support → a ∉ N'.support) (hmN : v ∈ N.verts) (w : V)
  (hw : (fun (w : V) ↦ N.Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ N.Adj v w) y → y = w) (y : V) (h : N'.Adj v y), y = w
Tactic: rw [Set.disjoint_left] at hd
Cleared hypotheses: hd, hmN, w, hw, y, h
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
M M' : G.Subgraph
hM : M.IsMatching
hM' : M'.IsMatching
hd_1 : Disjoint M.support M'.support
v : V
hv : v ∈ (M ⊔ M').verts
N N' : G.Subgraph
hN : N.IsMatching
hd : Disjoint N.support N'.support
hmN : v ∈ N.verts
w : V
hw : (fun (w : V) ↦ N.Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ N.Adj v w) y → y = w
y : V
hy : (N ⊔ N').Adj v y
⊢ y = w
have h : ∀ (h : N.Adj v y), y = w
Tactic: cases hy with
    | inl h => exact hw.2 y h
    | inr h =>
      rw [Set.disjoint_left] at hd
      simpa [(mem_support _).mpr ⟨w, hw.1⟩, (mem_support _).mpr ⟨y, h⟩] using @hd v
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
M M' : G.Subgraph
hM : M.IsMatching
hM' : M'.IsMatching
hd_1 : Disjoint M.support M'.support
v : V
hv : v ∈ (M ⊔ M').verts
N N' : G.Subgraph
hN : N.IsMatching
hd : Disjoint N.support N'.support
hmN : v ∈ N.verts
w : V
hw : (fun (w : V) ↦ N.Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ N.Adj v w) y → y = w
y : V
hy : (N ⊔ N').Adj v y
h : ∀ (h : N.Adj v y), y = w
⊢ y = w
have h₁ : ∀ (h : N'.Adj v y), y = w
Tactic: cases hy with
    | inl h => exact hw.2 y h
    | inr h =>
      rw [Set.disjoint_left] at hd
      simpa [(mem_support _).mpr ⟨w, hw.1⟩, (mem_support _).mpr ⟨y, h⟩] using @hd v
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
M M' : G.Subgraph
hM : M.IsMatching
hM' : M'.IsMatching
hd : Disjoint M.support M'.support
v : V
hv : v ∈ (M ⊔ M').verts
⊢ ∃! w : V, (M ⊔ M').Adj v w
have aux : ∀ {N N' : G.Subgraph} (hN : N.IsMatching) (hd : Disjoint N.support N'.support) (hmN : v ∈ N.verts),
  ∃! w : V, (N ⊔ N').Adj v w
Tactic: have aux {N N' : Subgraph G} (hN : N.IsMatching) (hd : Disjoint N.support N'.support)
    (hmN : v ∈ N.verts) : ∃! w, (N ⊔ N').Adj v w := by
    obtain ⟨w, hw⟩ := hN hmN
    use w
    refine ⟨sup_adj.mpr (.inl hw.1), ?_⟩
    intro y hy
    cases hy with
    | inl h => exact hw.2 y h
    | inr h =>
      rw [Set.disjoint_left] at hd
      simpa [(mem_support _).mpr ⟨w, hw.1⟩, (mem_support _).mpr ⟨y, h⟩] using @hd v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
M M' : G.Subgraph
hM : M.IsMatching
hM' : M'.IsMatching
hd : Disjoint M.support M'.support
v : V
hv : v ∈ (M ⊔ M').verts
aux :
  ∀ {N N' : G.Subgraph} (hN : N.IsMatching) (hd : Disjoint N.support N'.support) (hmN : v ∈ N.verts),
    ∃! w : V, (N ⊔ N').Adj v w
hmM' : v ∈ M'.verts
⊢ ∃! w : V, (M ⊔ M').Adj v w
have inr : ∃! w : V, (M' ⊔ M).Adj v w
Tactic: rw [sup_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
M M' : G.Subgraph
hM : M.IsMatching
hM' : M'.IsMatching
hd : Disjoint M.support M'.support
v : V
hv : v ∈ (M ⊔ M').verts
aux :
  ∀ {N N' : G.Subgraph} (hN : N.IsMatching) (hd : Disjoint N.support N'.support) (hmN : v ∈ N.verts),
    ∃! w : V, (N ⊔ N').Adj v w
⊢ ∃! w : V, (M ⊔ M').Adj v w
have x : v ∈ M.verts ∨ v ∈ M'.verts
Tactic: cases Set.mem_or_mem_of_mem_union hv with
  | inl hmM => exact aux hM hd hmM
  | inr hmM' =>
    rw [sup_comm]
    exact aux hM' (Disjoint.symm hd) hmM'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
ι : Type u_3
f : ι → G.Subgraph
hM : ∀ (i : ι), (f i).IsMatching
hd : Pairwise fun (i j : ι) ↦ Disjoint (f i).support (f j).support
v : V
hv : Membership.mem (γ := Set V) (verts (G := G) (⨆ (i : ι), f i)) v
⊢ ∃! w : V, Adj (G := G) (⨆ (i : ι), f i) v w
have obtain : ∀ (i : ι) (hi : v ∈ (f i).verts), ∃! w : V, Adj (G := G) (⨆ (i : ι), f i) v w
Tactic: obtain ⟨i, hi⟩ := Set.mem_iUnion.mp (verts_iSup ▸ hv)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
ι : Type u_3
f : ι → G.Subgraph
hM : ∀ (i : ι), (f i).IsMatching
hd : Pairwise fun (i j : ι) ↦ Disjoint (f i).support (f j).support
v : V
hv : Membership.mem (γ := Set V) (verts (G := G) (⨆ (i : ι), f i)) v
i : ι
hi : v ∈ (f i).verts
⊢ ∃! w : V, Adj (G := G) (⨆ (i : ι), f i) v w
have obtain : ∀ (w : V) (hw : (fun (w : V) ↦ (f i).Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ (f i).Adj v w) y → y = w),
  ∃! w : V, Adj (G := G) (⨆ (i : ι), f i) v w
Tactic: obtain ⟨w, hw⟩ := hM i hi
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
ι : Type u_3
f : ι → G.Subgraph
hM : ∀ (i : ι), (f i).IsMatching
hd : Pairwise fun (i j : ι) ↦ Disjoint (f i).support (f j).support
v : V
hv : Membership.mem (γ := Set V) (verts (G := G) (⨆ (i : ι), f i)) v
i : ι
hi : v ∈ (f i).verts
w : V
hw : (fun (w : V) ↦ (f i).Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ (f i).Adj v w) y → y = w
⊢ ∃! w : V, Adj (G := G) (⨆ (i : ι), f i) v w
have h : (fun (w : V) ↦ Adj (G := G) (⨆ (i : ι), f i) v w) w ∧
  ∀ (y : V), (fun (w : V) ↦ Adj (G := G) (⨆ (i : ι), f i) 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
ι : Type u_3
f : ι → G.Subgraph
hM : ∀ (i : ι), (f i).IsMatching
hd : Pairwise fun (i j : ι) ↦ Disjoint (f i).support (f j).support
v : V
hv : Membership.mem (γ := Set V) (verts (G := G) (⨆ (i : ι), f i)) v
i : ι
hi : v ∈ (f i).verts
w : V
hw : (fun (w : V) ↦ (f i).Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ (f i).Adj v w) y → y = w
⊢ (fun (w : V) ↦ Adj (G := G) (⨆ (i : ι), f i) v w) w ∧
    ∀ (y : V), (fun (w : V) ↦ Adj (G := G) (⨆ (i : ι), f i) v w) y → y = w
have h : ∀ (y : V), (fun (w : V) ↦ Adj (G := G) (⨆ (i : ι), f i) v w) y → y = w
Tactic: refine ⟨iSup_adj.mpr ⟨i, hw.1⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
ι : Type u_3
f : ι → G.Subgraph
hM : ∀ (i : ι), (f i).IsMatching
hd : Pairwise fun (i j : ι) ↦ Disjoint (f i).support (f j).support
v : V
hv : Membership.mem (γ := Set V) (verts (G := G) (⨆ (i : ι), f i)) v
i : ι
hi : v ∈ (f i).verts
w : V
hw : (fun (w : V) ↦ (f i).Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ (f i).Adj v w) y → y = w
y : V
hy : Adj (G := G) (⨆ (i : ι), f i) v y
⊢ y = w
have h : ∀ (i' : ι) (hi' : (f i').Adj v y), y = w
Tactic: obtain ⟨i', hi'⟩ := iSup_adj.mp hy
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
ι : Type u_3
f : ι → G.Subgraph
hM : ∀ (i : ι), (f i).IsMatching
hd : Pairwise fun (i j : ι) ↦ Disjoint (f i).support (f j).support
v : V
hv : Membership.mem (γ := Set V) (verts (G := G) (⨆ (i : ι), f i)) v
i : ι
hi : v ∈ (f i).verts
w : V
hw : (fun (w : V) ↦ (f i).Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ (f i).Adj v w) y → y = w
y : V
hy : Adj (G := G) (⨆ (i : ι), f i) v y
i' : ι
hi' : (f i').Adj v y
⊢ y = w
have pos : ∀ (heq : i = i'), y = w
Tactic: by_cases heq : i = i'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
ι : Type u_3
f : ι → G.Subgraph
hM : ∀ (i : ι), (f i).IsMatching
hd : Pairwise fun (i j : ι) ↦ Disjoint (f i).support (f j).support
v : V
hv : Membership.mem (γ := Set V) (verts (G := G) (⨆ (i : ι), f i)) v
i : ι
hi : v ∈ (f i).verts
w : V
hw : (fun (w : V) ↦ (f i).Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ (f i).Adj v w) y → y = w
y : V
hy : Adj (G := G) (⨆ (i : ι), f i) v y
i' : ι
hi' : (f i').Adj v y
pos : ∀ (heq : i = i'), y = w
⊢ y = w
have neg : ∀ (heq : ¬i = i'), y = w
Tactic: by_cases heq : i = i'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
ι : Type u_3
f : ι → G.Subgraph
hM : ∀ (i : ι), (f i).IsMatching
hd : Pairwise fun (i j : ι) ↦ Disjoint (f i).support (f j).support
v : V
hv : Membership.mem (γ := Set V) (verts (G := G) (⨆ (i : ι), f i)) v
i : ι
hi : v ∈ (f i).verts
w : V
hw : (fun (w : V) ↦ (f i).Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ (f i).Adj v w) y → y = w
y : V
hy : Adj (G := G) (⨆ (i : ι), f i) v y
i' : ι
hi' : (f i').Adj v y
heq : ¬i = i'
⊢ y = w
have this : (fun (i j : ι) ↦ Disjoint (f i).support (f j).support) i i'
Tactic: have := hd heq
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
ι : Type u_3
f : ι → G.Subgraph
hM : ∀ (i : ι), (f i).IsMatching
hd : Pairwise fun (i j : ι) ↦ Disjoint (f i).support (f j).support
v : V
hv : Membership.mem (γ := Set V) (verts (G := G) (⨆ (i : ι), f i)) v
i : ι
hi : v ∈ (f i).verts
w : V
hw : (fun (w : V) ↦ (f i).Adj v w) w ∧ ∀ (y : V), (fun (w : V) ↦ (f i).Adj v w) y → y = w
y : V
hy : Adj (G := G) (⨆ (i : ι), f i) v y
i' : ι
hi' : (f i').Adj v y
heq : ¬i = i'
this : (fun (i j : ι) ↦ Disjoint (f i).support (f j).support) i i'
⊢ y = w
have this₁ : ∀ ⦃a : V⦄, a ∈ (f i).support → a ∉ (f i').support
Tactic: simp only [Set.disjoint_left] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
v w : V
h : G.Adj v w
v_1 : V
hv : v_1 ∈ (G.subgraphOfAdj h).verts
⊢ ∃! w_1 : V, (G.subgraphOfAdj h).Adj v_1 w_1
have hv₁ : v_1 = v ∨ v_1 = w
Tactic: rw [subgraphOfAdj_verts, Set.mem_insert_iff, Set.mem_singleton_iff] at hv
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
v w : V
h : G.Adj v w
v_1 : V
h_1 : v_1 = v
⊢ ∃! w_1 : V, (G.subgraphOfAdj h).Adj v_1 w_1
have h₁ : (fun (w_1 : V) ↦ (G.subgraphOfAdj h).Adj v_1 w_1) w ∧
  ∀ (y : V), (fun (w_1 : V) ↦ (G.subgraphOfAdj h).Adj v_1 w_1) y → y = w
Tactic: use w
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
v w : V
h : G.Adj v w
v_1 : V
h_1 : v_1 = w
⊢ ∃! w_1 : V, (G.subgraphOfAdj h).Adj v_1 w_1
have h₁ : (fun (w_1 : V) ↦ (G.subgraphOfAdj h).Adj v_1 w_1) v ∧
  ∀ (y : V), (fun (w_1 : V) ↦ (G.subgraphOfAdj h).Adj v_1 w_1) y → y = v
Tactic: use v
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
v w : V
h : G.Adj v w
v_1 : V
hv : v_1 = v ∨ v_1 = w
⊢ ∃! w_1 : V, (G.subgraphOfAdj h).Adj v_1 w_1
have inl : v_1 = v → ∃! w_1 : V, (G.subgraphOfAdj h).Adj v_1 w_1
Tactic: cases hv with
  | inl => use w; aesop
  | inr => use v; aesop
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Matching (goal)
Goal:
V : Type u_1
G : SimpleGraph V
v w : V
h : G.Adj v w
v_1 : V
hv : v_1 = v ∨ v_1 = w
inl : v_1 = v → ∃! w_1 : V, (G.subgraphOfAdj h).Adj v_1 w_1
⊢ ∃! w_1 : V, (G.subgraphOfAdj h).Adj v_1 w_1
have inr : v_1 = w → ∃! w_1 : V, (G.subgraphOfAdj h).Adj v_1 w_1
Tactic: cases hv with
  | inl => use w; aesop
  | inr => use v; aesop
Cleared hypotheses: 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 : V
hv : v ∈ (Subgraph.coeSubgraph M).verts
⊢ ∃! w : V, (Subgraph.coeSubgraph M).Adj v w
have obtain : ∀ (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 sorry) 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 sorry) w) y → y = w),
  ∃! w : V, (Subgraph.coeSubgraph M).Adj v w
Tactic: obtain ⟨w, hw⟩ := hM <| Set.mem_of_mem_image_val <| (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 : 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
⊢ ∃! w : V, (Subgraph.coeSubgraph M).Adj v w
have h : (fun (w : V) ↦ (Subgraph.coeSubgraph M).Adj v w) (↑w : V) ∧
  ∀ (y : V), (fun (w : V) ↦ (Subgraph.coeSubgraph M).Adj v w) y → y = (↑w : V)
Tactic: use w
-- 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) ∧
    ∀ (y : V), (fun (w : V) ↦ (Subgraph.coeSubgraph M).Adj v w) y → y = (↑w : V)
have h : (fun (w : V) ↦ (Subgraph.coeSubgraph M).Adj v w) (↑w : V)
Tactic: refine ⟨?_, fun y 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
h : (fun (w : V) ↦ (Subgraph.coeSubgraph M).Adj v w) (↑w : V)
⊢ (fun (w : V) ↦ (Subgraph.coeSubgraph M).Adj v w) (↑w : V) ∧
    ∀ (y : V), (fun (w : V) ↦ (Subgraph.coeSubgraph M).Adj v w) y → y = (↑w : V)
have h₁ : ∀ (y : V) (hy : (fun (w : V) ↦ (Subgraph.coeSubgraph M).Adj v w) y), y = (↑w : V)
Tactic: refine ⟨?_, fun y hy => ?_⟩