awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hall (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ s ⊆ p₁, s.ncard ≤ Set.ncard.{u_1} (α := V) (⋃ x ∈ s, G.neighborSet x)
f : (↑p₁ : Type u_1) → V
hf₁ : Injective f
hf₂ : ∀ (x : (↑p₁ : Type u_1)), f x ∈ G.neighborFinset (↑x : V)
this : ∀ (x : (↑p₁ : Type u_1)), f x ∉ p₁
v : V
hv : v ∈ p₁ ∨ ∃ (a : V) (b : a ∈ p₁), f (Subtype.mk (p := fun (a : V) ↦ a ∈ p₁) a b) = v
h :
  ∀ (h' : v ∈ p₁),
    ∃! w : V,
      if h : v ∈ p₁ then f (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) v h) = w
      else if h : w ∈ p₁ then f (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) w h) = v else False
⊢ ∃! w : V,
    if h : v ∈ p₁ then f (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) v h) = w
    else if h : w ∈ p₁ then f (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) w h) = v else False
have h₃ : ∀ (x : V) (hx₁ : x ∈ p₁) (hx₂ : f (Subtype.mk (p := fun (a : V) ↦ a ∈ p₁) x hx₁) = v),
  ∃! w : V,
    if h : v ∈ p₁ then f (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) v h) = w
    else if h : w ∈ p₁ then f (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) w h) = v else False
Tactic: rcases hv with h' | ⟨x, hx₁, hx₂⟩
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hall (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ s ⊆ p₁, s.ncard ≤ Set.ncard.{u_1} (α := V) (⋃ x ∈ s, G.neighborSet x)
f : (↑p₁ : Type u_1) → V
hf₁ : Injective f
hf₂ : ∀ (x : (↑p₁ : Type u_1)), f x ∈ G.neighborFinset (↑x : V)
this : ∀ (x : (↑p₁ : Type u_1)), f x ∉ p₁
v x : V
hx₁ : x ∈ p₁
hx₂ : f (Subtype.mk (p := fun (a : V) ↦ a ∈ p₁) x hx₁) = v
⊢ ∃! w : V,
    if h : v ∈ p₁ then f (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) v h) = w
    else if h : w ∈ p₁ then f (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) w h) = v else False
have h : (fun (w : V) ↦
      (if h : v ∈ p₁ then f (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) v h) = w
        else if h : w ∈ p₁ then f (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) w h) = v else False :
        Prop))
    x ∧
  ∀ (y : V),
    (fun (w : V) ↦
          (if h : v ∈ p₁ then f (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) v h) = w
            else if h : w ∈ p₁ then f (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) w h) = v else False :
            Prop))
        y →
      y = x
Tactic: use x
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hall (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
inst : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ s ⊆ p₁, s.ncard ≤ Set.ncard.{u_1} (α := V) (⋃ x ∈ s, G.neighborSet x)
f : (↑p₁ : Type u_1) → V
hf₁ : Injective f
hf₂ : ∀ (x : (↑p₁ : Type u_1)), f x ∈ G.neighborFinset (↑x : V)
this : ∀ (x : (↑p₁ : Type u_1)), f x ∉ p₁
v x : V
hx₁ : x ∈ p₁
hx₂ : f (Subtype.mk (p := fun (a : V) ↦ a ∈ p₁) x hx₁) = v
⊢ (fun (w : V) ↦
        (if h : v ∈ p₁ then f (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) v h) = w
          else if h : w ∈ p₁ then f (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) w h) = v else False :
          Prop))
      x ∧
    ∀ (y : V),
      (fun (w : V) ↦
            (if h : v ∈ p₁ then f (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) v h) = w
              else if h : w ∈ p₁ then f (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) w h) = v else False :
              Prop))
          y →
        y = x
have this₁ : v ∉ p₁
Tactic: have := hx₂ ▸ this ⟨x, hx₁⟩
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hall (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ s ⊆ p₁, s.ncard ≤ Set.ncard.{u_1} (α := V) (⋃ x ∈ s, G.neighborSet x)
f : (↑p₁ : Type u_1) → V
hf₁ : Injective f
hf₂ : ∀ (x : (↑p₁ : Type u_1)), f x ∈ G.neighborFinset (↑x : V)
this_1 : ∀ (x : (↑p₁ : Type u_1)), f x ∉ p₁
v x : V
hx₁ : x ∈ p₁
hx₂ : f (Subtype.mk (p := fun (a : V) ↦ a ∈ p₁) x hx₁) = v
this : v ∉ p₁
⊢ (fun (w : V) ↦
        (if h : v ∈ p₁ then f (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) v h) = w
          else if h : w ∈ p₁ then f (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) w h) = v else False :
          Prop))
      x ∧
    ∀ (y : V),
      (fun (w : V) ↦
            (if h : v ∈ p₁ then f (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) v h) = w
              else if h : w ∈ p₁ then f (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) w h) = v else False :
              Prop))
          y →
        y = x
have h : ∀ (y : V) (x_1 : y ∈ p₁) (h : f (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) y x_1) = v), y = x
Tactic: simp only [this, ↓reduceDIte, hx₁, hx₂, dite_else_false, forall_exists_index, true_and]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hall (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ s ⊆ p₁, s.ncard ≤ Set.ncard.{u_1} (α := V) (⋃ x ∈ s, G.neighborSet x)
⊢ ∃ (M : G.Subgraph), p₁ ⊆ M.verts ∧ M.IsMatching
have obtain : ∀ (f : (↑p₁ : Type u_1) → V) (hf₁ : Injective f) (hf₂ : ∀ (x : (↑p₁ : Type u_1)), f x ∈ G.neighborFinset (↑x : V)),
  ∃ (M : G.Subgraph), p₁ ⊆ M.verts ∧ M.IsMatching
Tactic: classical
  obtain ⟨f, hf₁, hf₂⟩ := Finset.all_card_le_biUnion_card_iff_exists_injective
      (fun (x : p₁) ↦ G.neighborFinset x) |>.mp fun s ↦ by
    have := h₂ (s.image Subtype.val) (by simp)
    rw [Set.ncard_coe_finset, Finset.card_image_of_injective _ Subtype.val_injective] at this
    simpa [← Set.ncard_coe_finset, neighborFinset_def]
  have (x : p₁) : f x ∉ p₁ := h₁.disjoint |>.notMem_of_mem_right <|
    isBipartiteWith_neighborSet_subset h₁ x.2 <| Set.mem_toFinset.mp <| hf₂ x
  use hall_subgraph f this (fun v ↦ G.mem_neighborFinset _ _ |>.mp <| hf₂ v)
  refine ⟨by simp, fun v hv ↦ ?_⟩
  simp only [Set.mem_union, Set.mem_range, Subtype.exists] at hv ⊢
  rcases hv with h' | ⟨x, hx₁, hx₂⟩
  · exact ⟨f ⟨v, h'⟩, by simp_all⟩
  · use x
    have := hx₂ ▸ this ⟨x, hx₁⟩
    simp only [this, ↓reduceDIte, hx₁, hx₂, dite_else_false, forall_exists_index, true_and]
    exact fun _ _ k ↦ Subtype.ext_iff.mp <| hf₁ (hx₂ ▸ k)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hall (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ s ⊆ p₁, s.ncard ≤ Set.ncard.{u_1} (α := V) (⋃ x ∈ s, G.neighborSet x)
obtain :
  ∀ (f : (↑p₁ : Type u_1) → V) (hf₁ : Injective f) (hf₂ : ∀ (x : (↑p₁ : Type u_1)), f x ∈ G.neighborFinset (↑x : V)),
    ∃ (M : G.Subgraph), p₁ ⊆ M.verts ∧ M.IsMatching
⊢ ∃ (M : G.Subgraph), p₁ ⊆ M.verts ∧ M.IsMatching
have obtain₁ : ∀ (f : (↑p₁ : Type u_1) → V) (hf₁ : Injective f) (hf₂ : ∀ (x : (↑p₁ : Type u_1)), f x ∈ G.neighborFinset (↑x : V))
  (this : ∀ (x : (↑p₁ : Type u_1)), f x ∉ p₁), ∃ (M : G.Subgraph), p₁ ⊆ M.verts ∧ M.IsMatching
Tactic: classical
  obtain ⟨f, hf₁, hf₂⟩ := Finset.all_card_le_biUnion_card_iff_exists_injective
      (fun (x : p₁) ↦ G.neighborFinset x) |>.mp fun s ↦ by
    have := h₂ (s.image Subtype.val) (by simp)
    rw [Set.ncard_coe_finset, Finset.card_image_of_injective _ Subtype.val_injective] at this
    simpa [← Set.ncard_coe_finset, neighborFinset_def]
  have (x : p₁) : f x ∉ p₁ := h₁.disjoint |>.notMem_of_mem_right <|
    isBipartiteWith_neighborSet_subset h₁ x.2 <| Set.mem_toFinset.mp <| hf₂ x
  use hall_subgraph f this (fun v ↦ G.mem_neighborFinset _ _ |>.mp <| hf₂ v)
  refine ⟨by simp, fun v hv ↦ ?_⟩
  simp only [Set.mem_union, Set.mem_range, Subtype.exists] at hv ⊢
  rcases hv with h' | ⟨x, hx₁, hx₂⟩
  · exact ⟨f ⟨v, h'⟩, by simp_all⟩
  · use x
    have := hx₂ ▸ this ⟨x, hx₁⟩
    simp only [this, ↓reduceDIte, hx₁, hx₂, dite_else_false, forall_exists_index, true_and]
    exact fun _ _ k ↦ Subtype.ext_iff.mp <| hf₁ (hx₂ ▸ k)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hall (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ s ⊆ p₁, s.ncard ≤ Set.ncard.{u_1} (α := V) (⋃ x ∈ s, G.neighborSet x)
obtain :
  ∀ (f : (↑p₁ : Type u_1) → V) (hf₁ : Injective f) (hf₂ : ∀ (x : (↑p₁ : Type u_1)), f x ∈ G.neighborFinset (↑x : V)),
    ∃ (M : G.Subgraph), p₁ ⊆ M.verts ∧ M.IsMatching
obtain₁ :
  ∀ (f : (↑p₁ : Type u_1) → V) (hf₁ : Injective f) (hf₂ : ∀ (x : (↑p₁ : Type u_1)), f x ∈ G.neighborFinset (↑x : V))
    (this : ∀ (x : (↑p₁ : Type u_1)), f x ∉ p₁), ∃ (M : G.Subgraph), p₁ ⊆ M.verts ∧ M.IsMatching
⊢ ∃ (M : G.Subgraph), p₁ ⊆ M.verts ∧ M.IsMatching
have h : ∀ (f : (↑p₁ : Type u_1) → V) (hf₁ : Injective f) (hf₂ : ∀ (x : (↑p₁ : Type u_1)), f x ∈ G.neighborFinset (↑x : V))
  (this : ∀ (x : (↑p₁ : Type u_1)), f x ∉ p₁),
  p₁ ⊆ Subgraph.verts (G := G) (hall_subgraph (p := p₁) f this sorry) ∧
    Subgraph.IsMatching (G := G) (hall_subgraph (p := p₁) f this sorry)
Tactic: classical
  obtain ⟨f, hf₁, hf₂⟩ := Finset.all_card_le_biUnion_card_iff_exists_injective
      (fun (x : p₁) ↦ G.neighborFinset x) |>.mp fun s ↦ by
    have := h₂ (s.image Subtype.val) (by simp)
    rw [Set.ncard_coe_finset, Finset.card_image_of_injective _ Subtype.val_injective] at this
    simpa [← Set.ncard_coe_finset, neighborFinset_def]
  have (x : p₁) : f x ∉ p₁ := h₁.disjoint |>.notMem_of_mem_right <|
    isBipartiteWith_neighborSet_subset h₁ x.2 <| Set.mem_toFinset.mp <| hf₂ x
  use hall_subgraph f this (fun v ↦ G.mem_neighborFinset _ _ |>.mp <| hf₂ v)
  refine ⟨by simp, fun v hv ↦ ?_⟩
  simp only [Set.mem_union, Set.mem_range, Subtype.exists] at hv ⊢
  rcases hv with h' | ⟨x, hx₁, hx₂⟩
  · exact ⟨f ⟨v, h'⟩, by simp_all⟩
  · use x
    have := hx₂ ▸ this ⟨x, hx₁⟩
    simp only [this, ↓reduceDIte, hx₁, hx₂, dite_else_false, forall_exists_index, true_and]
    exact fun _ _ k ↦ Subtype.ext_iff.mp <| hf₁ (hx₂ ▸ k)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hall (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ s ⊆ p₁, s.ncard ≤ Set.ncard.{u_1} (α := V) (⋃ x ∈ s, G.neighborSet x)
obtain :
  ∀ (f : (↑p₁ : Type u_1) → V) (hf₁ : Injective f) (hf₂ : ∀ (x : (↑p₁ : Type u_1)), f x ∈ G.neighborFinset (↑x : V)),
    ∃ (M : G.Subgraph), p₁ ⊆ M.verts ∧ M.IsMatching
obtain₁ :
  ∀ (f : (↑p₁ : Type u_1) → V) (hf₁ : Injective f) (hf₂ : ∀ (x : (↑p₁ : Type u_1)), f x ∈ G.neighborFinset (↑x : V))
    (this : ∀ (x : (↑p₁ : Type u_1)), f x ∉ p₁), ∃ (M : G.Subgraph), p₁ ⊆ M.verts ∧ M.IsMatching
h :
  ∀ (f : (↑p₁ : Type u_1) → V) (hf₁ : Injective f) (hf₂ : ∀ (x : (↑p₁ : Type u_1)), f x ∈ G.neighborFinset (↑x : V))
    (this : ∀ (x : (↑p₁ : Type u_1)), f x ∉ p₁),
    p₁ ⊆ Subgraph.verts (G := G) (hall_subgraph (p := p₁) f this ⋯) ∧
      Subgraph.IsMatching (G := G) (hall_subgraph (p := p₁) f this ⋯)
⊢ ∃ (M : G.Subgraph), p₁ ⊆ M.verts ∧ M.IsMatching
have h₃ : ∀ (f : (↑p₁ : Type u_1) → V) (hf₁ : Injective f) (hf₂ : ∀ (x : (↑p₁ : Type u_1)), f x ∈ G.neighborFinset (↑x : V))
  (this : ∀ (x : (↑p₁ : Type u_1)), f x ∉ p₁) (v : V)
  (hv : v ∈ Subgraph.verts (G := G) (hall_subgraph (p := p₁) f this sorry)),
  ∃! w : V, Subgraph.Adj (G := G) (hall_subgraph (p := p₁) f this sorry) v w
Tactic: classical
  obtain ⟨f, hf₁, hf₂⟩ := Finset.all_card_le_biUnion_card_iff_exists_injective
      (fun (x : p₁) ↦ G.neighborFinset x) |>.mp fun s ↦ by
    have := h₂ (s.image Subtype.val) (by simp)
    rw [Set.ncard_coe_finset, Finset.card_image_of_injective _ Subtype.val_injective] at this
    simpa [← Set.ncard_coe_finset, neighborFinset_def]
  have (x : p₁) : f x ∉ p₁ := h₁.disjoint |>.notMem_of_mem_right <|
    isBipartiteWith_neighborSet_subset h₁ x.2 <| Set.mem_toFinset.mp <| hf₂ x
  use hall_subgraph f this (fun v ↦ G.mem_neighborFinset _ _ |>.mp <| hf₂ v)
  refine ⟨by simp, fun v hv ↦ ?_⟩
  simp only [Set.mem_union, Set.mem_range, Subtype.exists] at hv ⊢
  rcases hv with h' | ⟨x, hx₁, hx₂⟩
  · exact ⟨f ⟨v, h'⟩, by simp_all⟩
  · use x
    have := hx₂ ▸ this ⟨x, hx₁⟩
    simp only [this, ↓reduceDIte, hx₁, hx₂, dite_else_false, forall_exists_index, true_and]
    exact fun _ _ k ↦ Subtype.ext_iff.mp <| hf₁ (hx₂ ▸ k)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hall (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ s ⊆ p₁, s.ncard ≤ Set.ncard.{u_1} (α := V) (⋃ x ∈ s, G.neighborSet x)
obtain :
  ∀ (f : (↑p₁ : Type u_1) → V) (hf₁ : Injective f) (hf₂ : ∀ (x : (↑p₁ : Type u_1)), f x ∈ G.neighborFinset (↑x : V)),
    ∃ (M : G.Subgraph), p₁ ⊆ M.verts ∧ M.IsMatching
obtain₁ :
  ∀ (f : (↑p₁ : Type u_1) → V) (hf₁ : Injective f) (hf₂ : ∀ (x : (↑p₁ : Type u_1)), f x ∈ G.neighborFinset (↑x : V))
    (this : ∀ (x : (↑p₁ : Type u_1)), f x ∉ p₁), ∃ (M : G.Subgraph), p₁ ⊆ M.verts ∧ M.IsMatching
h :
  ∀ (f : (↑p₁ : Type u_1) → V) (hf₁ : Injective f) (hf₂ : ∀ (x : (↑p₁ : Type u_1)), f x ∈ G.neighborFinset (↑x : V))
    (this : ∀ (x : (↑p₁ : Type u_1)), f x ∉ p₁),
    p₁ ⊆ Subgraph.verts (G := G) (hall_subgraph (p := p₁) f this ⋯) ∧
      Subgraph.IsMatching (G := G) (hall_subgraph (p := p₁) f this ⋯)
h₃ :
  ∀ (f : (↑p₁ : Type u_1) → V) (hf₁ : Injective f) (hf₂ : ∀ (x : (↑p₁ : Type u_1)), f x ∈ G.neighborFinset (↑x : V))
    (this : ∀ (x : (↑p₁ : Type u_1)), f x ∉ p₁) (v : V)
    (hv : v ∈ Subgraph.verts (G := G) (hall_subgraph (p := p₁) f this ⋯)),
    ∃! w : V, Subgraph.Adj (G := G) (hall_subgraph (p := p₁) f this ⋯) v w
⊢ ∃ (M : G.Subgraph), p₁ ⊆ M.verts ∧ M.IsMatching
have h₄ : ∀ (f : (↑p₁ : Type u_1) → V) (hf₁ : Injective f) (hf₂ : ∀ (x : (↑p₁ : Type u_1)), f x ∈ G.neighborFinset (↑x : V))
  (this : ∀ (x : (↑p₁ : Type u_1)), f x ∉ p₁) (v : V)
  (hv : v ∈ p₁ ∨ ∃ (a : V) (b : a ∈ p₁), f (Subtype.mk (p := fun (a : V) ↦ a ∈ p₁) a b) = v),
  ∃! w : V,
    if h : v ∈ p₁ then f (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) v h) = w
    else if h : w ∈ p₁ then f (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) w h) = v else False
Tactic: classical
  obtain ⟨f, hf₁, hf₂⟩ := Finset.all_card_le_biUnion_card_iff_exists_injective
      (fun (x : p₁) ↦ G.neighborFinset x) |>.mp fun s ↦ by
    have := h₂ (s.image Subtype.val) (by simp)
    rw [Set.ncard_coe_finset, Finset.card_image_of_injective _ Subtype.val_injective] at this
    simpa [← Set.ncard_coe_finset, neighborFinset_def]
  have (x : p₁) : f x ∉ p₁ := h₁.disjoint |>.notMem_of_mem_right <|
    isBipartiteWith_neighborSet_subset h₁ x.2 <| Set.mem_toFinset.mp <| hf₂ x
  use hall_subgraph f this (fun v ↦ G.mem_neighborFinset _ _ |>.mp <| hf₂ v)
  refine ⟨by simp, fun v hv ↦ ?_⟩
  simp only [Set.mem_union, Set.mem_range, Subtype.exists] at hv ⊢
  rcases hv with h' | ⟨x, hx₁, hx₂⟩
  · exact ⟨f ⟨v, h'⟩, by simp_all⟩
  · use x
    have := hx₂ ▸ this ⟨x, hx₁⟩
    simp only [this, ↓reduceDIte, hx₁, hx₂, dite_else_false, forall_exists_index, true_and]
    exact fun _ _ k ↦ Subtype.ext_iff.mp <| hf₁ (hx₂ ▸ k)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hall (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ s ⊆ p₁, s.ncard ≤ Set.ncard.{u_1} (α := V) (⋃ x ∈ s, G.neighborSet x)
obtain :
  ∀ (f : (↑p₁ : Type u_1) → V) (hf₁ : Injective f) (hf₂ : ∀ (x : (↑p₁ : Type u_1)), f x ∈ G.neighborFinset (↑x : V)),
    ∃ (M : G.Subgraph), p₁ ⊆ M.verts ∧ M.IsMatching
obtain₁ :
  ∀ (f : (↑p₁ : Type u_1) → V) (hf₁ : Injective f) (hf₂ : ∀ (x : (↑p₁ : Type u_1)), f x ∈ G.neighborFinset (↑x : V))
    (this : ∀ (x : (↑p₁ : Type u_1)), f x ∉ p₁), ∃ (M : G.Subgraph), p₁ ⊆ M.verts ∧ M.IsMatching
h :
  ∀ (f : (↑p₁ : Type u_1) → V) (hf₁ : Injective f) (hf₂ : ∀ (x : (↑p₁ : Type u_1)), f x ∈ G.neighborFinset (↑x : V))
    (this : ∀ (x : (↑p₁ : Type u_1)), f x ∉ p₁),
    p₁ ⊆ Subgraph.verts (G := G) (hall_subgraph (p := p₁) f this ⋯) ∧
      Subgraph.IsMatching (G := G) (hall_subgraph (p := p₁) f this ⋯)
h₃ :
  ∀ (f : (↑p₁ : Type u_1) → V) (hf₁ : Injective f) (hf₂ : ∀ (x : (↑p₁ : Type u_1)), f x ∈ G.neighborFinset (↑x : V))
    (this : ∀ (x : (↑p₁ : Type u_1)), f x ∉ p₁) (v : V)
    (hv : v ∈ Subgraph.verts (G := G) (hall_subgraph (p := p₁) f this ⋯)),
    ∃! w : V, Subgraph.Adj (G := G) (hall_subgraph (p := p₁) f this ⋯) v w
h₄ :
  ∀ (f : (↑p₁ : Type u_1) → V) (hf₁ : Injective f) (hf₂ : ∀ (x : (↑p₁ : Type u_1)), f x ∈ G.neighborFinset (↑x : V))
    (this : ∀ (x : (↑p₁ : Type u_1)), f x ∉ p₁) (v : V)
    (hv : v ∈ p₁ ∨ ∃ (a : V) (b : a ∈ p₁), f (Subtype.mk (p := fun (a : V) ↦ a ∈ p₁) a b) = v),
    ∃! w : V,
      if h : v ∈ p₁ then f (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) v h) = w
      else if h : w ∈ p₁ then f (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) w h) = v else False
⊢ ∃ (M : G.Subgraph), p₁ ⊆ M.verts ∧ M.IsMatching
have h₅ : ∀ (f : (↑p₁ : Type u_1) → V) (hf₁ : Injective f) (hf₂ : ∀ (x : (↑p₁ : Type u_1)), f x ∈ G.neighborFinset (↑x : V))
  (this : ∀ (x : (↑p₁ : Type u_1)), f x ∉ p₁) (v : V) (h' : v ∈ p₁),
  ∃! w : V,
    if h : v ∈ p₁ then f (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) v h) = w
    else if h : w ∈ p₁ then f (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) w h) = v else False
Tactic: classical
  obtain ⟨f, hf₁, hf₂⟩ := Finset.all_card_le_biUnion_card_iff_exists_injective
      (fun (x : p₁) ↦ G.neighborFinset x) |>.mp fun s ↦ by
    have := h₂ (s.image Subtype.val) (by simp)
    rw [Set.ncard_coe_finset, Finset.card_image_of_injective _ Subtype.val_injective] at this
    simpa [← Set.ncard_coe_finset, neighborFinset_def]
  have (x : p₁) : f x ∉ p₁ := h₁.disjoint |>.notMem_of_mem_right <|
    isBipartiteWith_neighborSet_subset h₁ x.2 <| Set.mem_toFinset.mp <| hf₂ x
  use hall_subgraph f this (fun v ↦ G.mem_neighborFinset _ _ |>.mp <| hf₂ v)
  refine ⟨by simp, fun v hv ↦ ?_⟩
  simp only [Set.mem_union, Set.mem_range, Subtype.exists] at hv ⊢
  rcases hv with h' | ⟨x, hx₁, hx₂⟩
  · exact ⟨f ⟨v, h'⟩, by simp_all⟩
  · use x
    have := hx₂ ▸ this ⟨x, hx₁⟩
    simp only [this, ↓reduceDIte, hx₁, hx₂, dite_else_false, forall_exists_index, true_and]
    exact fun _ _ k ↦ Subtype.ext_iff.mp <| hf₁ (hx₂ ▸ k)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hall (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
inst : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ (s : Set V), s.ncard ≤ Set.ncard.{u_1} (α := V) (⋃ x ∈ s, G.neighborSet x)
s : Finset V
⊢ s.card ≤ Finset.card (α := V) (s.biUnion fun (x : V) ↦ G.neighborFinset x)
have this : (↑s : Set V).ncard ≤ Set.ncard.{u_1} (α := V) (⋃ x ∈ (↑s : Set V), G.neighborSet x)
Tactic: have := h₂ s
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hall (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ (s : Set V), s.ncard ≤ Set.ncard.{u_1} (α := V) (⋃ x ∈ s, G.neighborSet x)
⊢ p₁ ∪ p₂ = Set.univ
have obtain : ∀ (f : V → V), Injective f → ∀ (hf₂ : ∀ (x : V), f x ∈ G.neighborFinset x), p₁ ∪ p₂ = Set.univ
Tactic: obtain ⟨f, _, hf₂⟩ := Finset.all_card_le_biUnion_card_iff_exists_injective
      (fun x ↦ G.neighborFinset x) |>.mp fun s ↦ by
    have := h₂ s
    simpa [← Set.ncard_coe_finset, neighborFinset_def]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hall (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ (s : Set V), s.ncard ≤ Set.ncard.{u_1} (α := V) (⋃ x ∈ s, G.neighborSet x)
f : V → V
left : Injective f
hf₂ : ∀ (x : V), f x ∈ G.neighborFinset x
⊢ p₁ ∪ p₂ = Set.univ
have refine : ∀ (x : V), x ∈ p₁ ∪ p₂
Tactic: refine Set.eq_univ_iff_forall.mpr fun x ↦ ?_
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hall (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
inst : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ (s : Set V), s.ncard ≤ Set.ncard.{u_1} (α := V) (⋃ x ∈ s, G.neighborSet x)
f : V → V
left : Injective f
hf₂ : ∀ (x : V), f x ∈ G.neighborFinset x
x : V
⊢ x ∈ p₁ ∪ p₂
have this : x ∈ p₁ ∧ f x ∈ p₂ ∨ x ∈ p₂ ∧ f x ∈ p₁
Tactic: have := h₁.mem_of_adj <| G.mem_neighborFinset _ _ |>.mp (hf₂ x)
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hall (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ (s : Set V), s.ncard ≤ Set.ncard.{u_1} (α := V) (⋃ x ∈ s, G.neighborSet x)
⊢ p₁ ∪ p₂ = Set.univ
have obtain : ∀ (f : V → V), Injective f → ∀ (hf₂ : ∀ (x : V), f x ∈ G.neighborFinset x), p₁ ∪ p₂ = Set.univ
Tactic: classical
  obtain ⟨f, _, hf₂⟩ := Finset.all_card_le_biUnion_card_iff_exists_injective
      (fun x ↦ G.neighborFinset x) |>.mp fun s ↦ by
    have := h₂ s
    simpa [← Set.ncard_coe_finset, neighborFinset_def]
  refine Set.eq_univ_iff_forall.mpr fun x ↦ ?_
  have := h₁.mem_of_adj <| G.mem_neighborFinset _ _ |>.mp (hf₂ x)
  grind
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hall (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ (s : Set V), s.ncard ≤ Set.ncard.{u_1} (α := V) (⋃ x ∈ s, G.neighborSet x)
obtain : ∀ (f : V → V), Injective f → ∀ (hf₂ : ∀ (x : V), f x ∈ G.neighborFinset x), p₁ ∪ p₂ = Set.univ
⊢ p₁ ∪ p₂ = Set.univ
have obtain₁ : ∀ (f : V → V), Injective f → ∀ (hf₂ : ∀ (x : V), f x ∈ G.neighborFinset x) (x : V), x ∈ p₁ ∪ p₂
Tactic: classical
  obtain ⟨f, _, hf₂⟩ := Finset.all_card_le_biUnion_card_iff_exists_injective
      (fun x ↦ G.neighborFinset x) |>.mp fun s ↦ by
    have := h₂ s
    simpa [← Set.ncard_coe_finset, neighborFinset_def]
  refine Set.eq_univ_iff_forall.mpr fun x ↦ ?_
  have := h₁.mem_of_adj <| G.mem_neighborFinset _ _ |>.mp (hf₂ x)
  grind
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hall (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ (s : Set V), s.ncard ≤ Set.ncard.{u_1} (α := V) (⋃ x ∈ s, G.neighborSet x)
obtain : ∀ (f : V → V), Injective f → ∀ (hf₂ : ∀ (x : V), f x ∈ G.neighborFinset x), p₁ ∪ p₂ = Set.univ
obtain₁ : ∀ (f : V → V), Injective f → ∀ (hf₂ : ∀ (x : V), f x ∈ G.neighborFinset x) (x : V), x ∈ p₁ ∪ p₂
⊢ p₁ ∪ p₂ = Set.univ
have obtain₂ : ∀ (f : V → V),
  Injective f →
    ∀ (hf₂ : ∀ (x : V), f x ∈ G.neighborFinset x) (x : V) (this : x ∈ p₁ ∧ f x ∈ p₂ ∨ x ∈ p₂ ∧ f x ∈ p₁), x ∈ p₁ ∪ p₂
Tactic: classical
  obtain ⟨f, _, hf₂⟩ := Finset.all_card_le_biUnion_card_iff_exists_injective
      (fun x ↦ G.neighborFinset x) |>.mp fun s ↦ by
    have := h₂ s
    simpa [← Set.ncard_coe_finset, neighborFinset_def]
  refine Set.eq_univ_iff_forall.mpr fun x ↦ ?_
  have := h₁.mem_of_adj <| G.mem_neighborFinset _ _ |>.mp (hf₂ x)
  grind
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hall (goal)
Goal:
V : Type u_1
G : SimpleGraph V
inst : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ (s : Set V), s.ncard ≤ Set.ncard.{u_1} (α := V) (⋃ x ∈ s, G.neighborSet x)
⊢ ∃ (h : (↑p₁ : Type u_1) → (↑p₂ : Type u_1)), Bijective h ∧ ∀ (a : (↑p₁ : Type u_1)), G.Adj (↑a : V) (↑(h a) : V)
have obtain : ∀ (f : V → V) (hf₁ : Injective f) (hf₂ : ∀ (x : V), f x ∈ G.neighborFinset x),
  ∃ (h : (↑p₁ : Type u_1) → (↑p₂ : Type u_1)), Bijective h ∧ ∀ (a : (↑p₁ : Type u_1)), G.Adj (↑a : V) (↑(h a) : V)
Tactic: obtain ⟨f, hf₁, hf₂⟩ := Finset.all_card_le_biUnion_card_iff_exists_injective
      (fun x ↦ G.neighborFinset x) |>.mp fun s ↦ by
    have := h₂ s
    simpa [← Set.ncard_coe_finset, neighborFinset_def]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hall (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
inst : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ (s : Set V), s.ncard ≤ Set.ncard.{u_1} (α := V) (⋃ x ∈ s, G.neighborSet x)
f : V → V
hf₁ : Injective f
hf₂ : ∀ (x : V), f x ∈ G.neighborFinset x
⊢ ∃ (h : (↑p₁ : Type u_1) → (↑p₂ : Type u_1)), Bijective h ∧ ∀ (a : (↑p₁ : Type u_1)), G.Adj (↑a : V) (↑(h a) : V)
have this : ∀ (x : V) (h : x ∈ p₁), f x ∉ p₁
Tactic: have (x : V) (h : x ∈ p₁) : f x ∉ p₁ := h₁.disjoint |>.notMem_of_mem_right <|
    isBipartiteWith_neighborSet_subset h₁ h <| Set.mem_toFinset.mp <| hf₂ x
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Hall (hypothesis)
Goal:
V : Type u_1
G : SimpleGraph V
inst : G.LocallyFinite
p₁ p₂ : Set V
h₁ : G.IsBipartiteWith p₁ p₂
h₂ : ∀ (s : Set V), s.ncard ≤ Set.ncard.{u_1} (α := V) (⋃ x ∈ s, G.neighborSet x)
f : V → V
hf₁ : Injective f
hf₂ : ∀ (x : V), f x ∈ G.neighborFinset x
this : ∀ (x : V) (h : x ∈ p₁), f x ∉ p₁
⊢ ∃ (h : (↑p₁ : Type u_1) → (↑p₂ : Type u_1)), Bijective h ∧ ∀ (a : (↑p₁ : Type u_1)), G.Adj (↑a : V) (↑(h a) : V)
have this₁ : ∀ (x : V) (h : x ∈ p₂), f x ∉ p₂
Tactic: have (x : V) (h : x ∈ p₂) : f x ∉ p₂ := h₁.disjoint |>.notMem_of_mem_left <|
    isBipartiteWith_neighborSet_subset h₁.symm h <| Set.mem_toFinset.mp <| hf₂ x