awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_1 : ∀ (x : V) (h : x ∈ p₁), f x ∉ p₁
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), f x ∈ p₁ ∨ f x ∈ p₂
Tactic: have (x : V) : f x ∈ p₁ ∨ f x ∈ p₂ := by
    simp [union_eq_univ_of_forall_ncard_le h₁ h₂, p₁.mem_union (f x) p₂ |>.mp]
-- 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
hf₁ : Injective f
hf₂ : ∀ (x : V), f x ∈ G.neighborFinset x
this_1 : ∀ (x : V) (h : x ∈ p₁), f x ∉ p₁
this_2 : ∀ (x : V) (h : x ∈ p₂), f x ∉ p₂
this : ∀ (x : V), f x ∈ p₁ ∨ f x ∈ p₂
f' : (x : (↑p₁ : Type u_1)) → (↑p₂ : Type u_1) :=
  fun (x : (↑p₁ : Type u_1)) ↦ Subtype.mk (p := fun (x : V) ↦ x ∈ p₂) (f (↑x : V)) ⋯
g' : (x : (↑p₂ : Type u_1)) → (↑p₁ : Type u_1) :=
  fun (x : (↑p₂ : Type u_1)) ↦ Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) (f (↑x : V)) ⋯
⊢ ∃ (h : (↑p₁ : Type u_1) → (↑p₂ : Type u_1)), Bijective h ∧ ∀ (a : (↑p₁ : Type u_1)), G.Adj (↑a : V) (↑(h a) : V)
have refine_1 : Injective f'
Tactic: refine Embedding.schroeder_bernstein_of_rel (f := f') (g := g') ?_ ?_ (fun x y ↦ G.Adj x y) ?_ ?_
-- 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
hf₁ : Injective f
hf₂ : ∀ (x : V), f x ∈ G.neighborFinset x
this_1 : ∀ (x : V) (h : x ∈ p₁), f x ∉ p₁
this_2 : ∀ (x : V) (h : x ∈ p₂), f x ∉ p₂
this : ∀ (x : V), f x ∈ p₁ ∨ f x ∈ p₂
f' : (x : (↑p₁ : Type u_1)) → (↑p₂ : Type u_1) :=
  fun (x : (↑p₁ : Type u_1)) ↦ Subtype.mk (p := fun (x : V) ↦ x ∈ p₂) (f (↑x : V)) ⋯
g' : (x : (↑p₂ : Type u_1)) → (↑p₁ : Type u_1) :=
  fun (x : (↑p₂ : Type u_1)) ↦ Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) (f (↑x : V)) ⋯
refine_1 : Injective f'
⊢ ∃ (h : (↑p₁ : Type u_1) → (↑p₂ : Type u_1)), Bijective h ∧ ∀ (a : (↑p₁ : Type u_1)), G.Adj (↑a : V) (↑(h a) : V)
have refine_2 : Injective g'
Tactic: refine Embedding.schroeder_bernstein_of_rel (f := f') (g := g') ?_ ?_ (fun x y ↦ G.Adj x y) ?_ ?_
-- 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
hf₁ : Injective f
hf₂ : ∀ (x : V), f x ∈ G.neighborFinset x
this_1 : ∀ (x : V) (h : x ∈ p₁), f x ∉ p₁
this_2 : ∀ (x : V) (h : x ∈ p₂), f x ∉ p₂
this : ∀ (x : V), f x ∈ p₁ ∨ f x ∈ p₂
f' : (x : (↑p₁ : Type u_1)) → (↑p₂ : Type u_1) :=
  fun (x : (↑p₁ : Type u_1)) ↦ Subtype.mk (p := fun (x : V) ↦ x ∈ p₂) (f (↑x : V)) ⋯
g' : (x : (↑p₂ : Type u_1)) → (↑p₁ : Type u_1) :=
  fun (x : (↑p₂ : Type u_1)) ↦ Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) (f (↑x : V)) ⋯
refine_1 : Injective f'
refine_2 : Injective g'
⊢ ∃ (h : (↑p₁ : Type u_1) → (↑p₂ : Type u_1)), Bijective h ∧ ∀ (a : (↑p₁ : Type u_1)), G.Adj (↑a : V) (↑(h a) : V)
have refine_3 : ∀ (a : (↑p₁ : Type u_1)), (fun (x : (↑p₁ : Type u_1)) (y : (↑p₂ : Type u_1)) ↦ G.Adj (↑x : V) (↑y : V)) a (f' a)
Tactic: refine Embedding.schroeder_bernstein_of_rel (f := f') (g := g') ?_ ?_ (fun x y ↦ G.Adj x y) ?_ ?_
-- 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
hf₁ : Injective f
hf₂ : ∀ (x : V), f x ∈ G.neighborFinset x
this_1 : ∀ (x : V) (h : x ∈ p₁), f x ∉ p₁
this_2 : ∀ (x : V) (h : x ∈ p₂), f x ∉ p₂
this : ∀ (x : V), f x ∈ p₁ ∨ f x ∈ p₂
f' : (x : (↑p₁ : Type u_1)) → (↑p₂ : Type u_1) :=
  fun (x : (↑p₁ : Type u_1)) ↦ Subtype.mk (p := fun (x : V) ↦ x ∈ p₂) (f (↑x : V)) ⋯
g' : (x : (↑p₂ : Type u_1)) → (↑p₁ : Type u_1) :=
  fun (x : (↑p₂ : Type u_1)) ↦ Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) (f (↑x : V)) ⋯
refine_1 : Injective f'
refine_2 : Injective g'
refine_3 :
  ∀ (a : (↑p₁ : Type u_1)), (fun (x : (↑p₁ : Type u_1)) (y : (↑p₂ : Type u_1)) ↦ G.Adj (↑x : V) (↑y : V)) a (f' a)
⊢ ∃ (h : (↑p₁ : Type u_1) → (↑p₂ : Type u_1)), Bijective h ∧ ∀ (a : (↑p₁ : Type u_1)), G.Adj (↑a : V) (↑(h a) : V)
have refine_4 : ∀ (b : (↑p₂ : Type u_1)), (fun (x : (↑p₁ : Type u_1)) (y : (↑p₂ : Type u_1)) ↦ G.Adj (↑x : V) (↑y : V)) (g' b) b
Tactic: refine Embedding.schroeder_bernstein_of_rel (f := f') (g := g') ?_ ?_ (fun x y ↦ G.Adj x y) ?_ ?_
-- 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: classical
  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]
  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
  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
  have (x : V) : f x ∈ p₁ ∨ f x ∈ p₂ := by
    simp [union_eq_univ_of_forall_ncard_le h₁ h₂, p₁.mem_union (f x) p₂ |>.mp]
  let f' (x : p₁) : p₂ := ⟨f x, by grind⟩
  let g' (x : p₂) : p₁ := ⟨f x, by grind⟩
  refine Embedding.schroeder_bernstein_of_rel (f := f') (g := g') ?_ ?_ (fun x y ↦ G.Adj x y) ?_ ?_
  · exact Injective.of_comp (f := Subtype.val) <| hf₁.comp Subtype.val_injective
  · exact Injective.of_comp (f := Subtype.val) <| hf₁.comp Subtype.val_injective
  · exact fun v ↦ mem_neighborFinset _ _ _ |>.mp (hf₂ v)
  · exact fun v ↦ mem_neighborFinset _ _ _ |>.mp (hf₂ v) |>.symm
-- 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) (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)
⊢ ∃ (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) (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)
Tactic: classical
  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]
  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
  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
  have (x : V) : f x ∈ p₁ ∨ f x ∈ p₂ := by
    simp [union_eq_univ_of_forall_ncard_le h₁ h₂, p₁.mem_union (f x) p₂ |>.mp]
  let f' (x : p₁) : p₂ := ⟨f x, by grind⟩
  let g' (x : p₂) : p₁ := ⟨f x, by grind⟩
  refine Embedding.schroeder_bernstein_of_rel (f := f') (g := g') ?_ ?_ (fun x y ↦ G.Adj x y) ?_ ?_
  · exact Injective.of_comp (f := Subtype.val) <| hf₁.comp Subtype.val_injective
  · exact Injective.of_comp (f := Subtype.val) <| hf₁.comp Subtype.val_injective
  · exact fun v ↦ mem_neighborFinset _ _ _ |>.mp (hf₂ v)
  · exact fun v ↦ mem_neighborFinset _ _ _ |>.mp (hf₂ v) |>.symm
-- 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) (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)
obtain₁ :
  ∀ (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)
⊢ ∃ (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) (this : ∀ (x : V) (h : x ∈ p₁), f x ∉ p₁)
  (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)
Tactic: classical
  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]
  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
  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
  have (x : V) : f x ∈ p₁ ∨ f x ∈ p₂ := by
    simp [union_eq_univ_of_forall_ncard_le h₁ h₂, p₁.mem_union (f x) p₂ |>.mp]
  let f' (x : p₁) : p₂ := ⟨f x, by grind⟩
  let g' (x : p₂) : p₁ := ⟨f x, by grind⟩
  refine Embedding.schroeder_bernstein_of_rel (f := f') (g := g') ?_ ?_ (fun x y ↦ G.Adj x y) ?_ ?_
  · exact Injective.of_comp (f := Subtype.val) <| hf₁.comp Subtype.val_injective
  · exact Injective.of_comp (f := Subtype.val) <| hf₁.comp Subtype.val_injective
  · exact fun v ↦ mem_neighborFinset _ _ _ |>.mp (hf₂ v)
  · exact fun v ↦ mem_neighborFinset _ _ _ |>.mp (hf₂ v) |>.symm
-- 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) (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)
obtain₁ :
  ∀ (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)
obtain₂ :
  ∀ (f : V → V) (hf₁ : Injective f) (hf₂ : ∀ (x : V), f x ∈ G.neighborFinset x)
    (this : ∀ (x : V) (h : x ∈ p₁), f x ∉ p₁) (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)
⊢ ∃ (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) (this : ∀ (x : V) (h : x ∈ p₁), f x ∉ p₁)
  (this : ∀ (x : V) (h : x ∈ p₂), f x ∉ p₂) (this : ∀ (x : V), f 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)
Tactic: classical
  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]
  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
  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
  have (x : V) : f x ∈ p₁ ∨ f x ∈ p₂ := by
    simp [union_eq_univ_of_forall_ncard_le h₁ h₂, p₁.mem_union (f x) p₂ |>.mp]
  let f' (x : p₁) : p₂ := ⟨f x, by grind⟩
  let g' (x : p₂) : p₁ := ⟨f x, by grind⟩
  refine Embedding.schroeder_bernstein_of_rel (f := f') (g := g') ?_ ?_ (fun x y ↦ G.Adj x y) ?_ ?_
  · exact Injective.of_comp (f := Subtype.val) <| hf₁.comp Subtype.val_injective
  · exact Injective.of_comp (f := Subtype.val) <| hf₁.comp Subtype.val_injective
  · exact fun v ↦ mem_neighborFinset _ _ _ |>.mp (hf₂ v)
  · exact fun v ↦ mem_neighborFinset _ _ _ |>.mp (hf₂ v) |>.symm
-- 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) (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)
obtain₁ :
  ∀ (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)
obtain₂ :
  ∀ (f : V → V) (hf₁ : Injective f) (hf₂ : ∀ (x : V), f x ∈ G.neighborFinset x)
    (this : ∀ (x : V) (h : x ∈ p₁), f x ∉ p₁) (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)
obtain₃ obtain₄ obtain₅ :
  ∀ (f : V → V) (hf₁ : Injective f) (hf₂ : ∀ (x : V), f x ∈ G.neighborFinset x)
    (this : ∀ (x : V) (h : x ∈ p₁), f x ∉ p₁) (this : ∀ (x : V) (h : x ∈ p₂), f x ∉ p₂)
    (this : ∀ (x : V), f 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)
⊢ ∃ (h : (↑p₁ : Type u_1) → (↑p₂ : Type u_1)), Bijective h ∧ ∀ (a : (↑p₁ : Type u_1)), G.Adj (↑a : V) (↑(h a) : V)
have refine_1 : ∀ (f : V → V) (hf₁ : Injective f) (hf₂ : ∀ (x : V), f x ∈ G.neighborFinset x) (this : ∀ (x : V) (h : x ∈ p₁), f x ∉ p₁)
  (this_1 : ∀ (x : V) (h : x ∈ p₂), f x ∉ p₂) (this_2 : ∀ (x : V), f x ∈ p₁ ∨ f x ∈ p₂),
  let f' : (x : (↑p₁ : Type u_1)) → (↑p₂ : Type u_1) := fun (x : (↑p₁ : Type u_1)) ↦
    Subtype.mk (p := fun (x : V) ↦ x ∈ p₂) (f (↑x : V)) sorry;
  Injective f'
Tactic: classical
  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]
  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
  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
  have (x : V) : f x ∈ p₁ ∨ f x ∈ p₂ := by
    simp [union_eq_univ_of_forall_ncard_le h₁ h₂, p₁.mem_union (f x) p₂ |>.mp]
  let f' (x : p₁) : p₂ := ⟨f x, by grind⟩
  let g' (x : p₂) : p₁ := ⟨f x, by grind⟩
  refine Embedding.schroeder_bernstein_of_rel (f := f') (g := g') ?_ ?_ (fun x y ↦ G.Adj x y) ?_ ?_
  · exact Injective.of_comp (f := Subtype.val) <| hf₁.comp Subtype.val_injective
  · exact Injective.of_comp (f := Subtype.val) <| hf₁.comp Subtype.val_injective
  · exact fun v ↦ mem_neighborFinset _ _ _ |>.mp (hf₂ v)
  · exact fun v ↦ mem_neighborFinset _ _ _ |>.mp (hf₂ v) |>.symm
-- 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)
⊢ ∃ (M : G.Subgraph), M.IsPerfectMatching
have obtain : ∀ (b : (↑p₁ : Type u_1) → (↑p₂ : Type u_1)) (hb₁ : Bijective b)
  (hb₂ : ∀ (a : (↑p₁ : Type u_1)), G.Adj (↑a : V) (↑(b a) : V)), ∃ (M : G.Subgraph), M.IsPerfectMatching
Tactic: obtain ⟨b, hb₁, hb₂⟩ := exists_bijective_of_forall_ncard_le h₁ h₂
-- 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)
b : (↑p₁ : Type u_1) → (↑p₂ : Type u_1)
hb₁ : Bijective b
hb₂ : ∀ (a : (↑p₁ : Type u_1)), G.Adj (↑a : V) (↑(b a) : V)
⊢ ∃ (M : G.Subgraph), M.IsPerfectMatching
have h : (hall_subgraph (p := p₁) (fun (v : (↑p₁ : Type u_1)) ↦ (↑(b v) : V)) sorry hb₂).IsPerfectMatching
Tactic: use hall_subgraph (fun v ↦ b v) (fun v ↦ h₁.disjoint.notMem_of_mem_right (b v).property) hb₂
-- 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)
b : (↑p₁ : Type u_1) → (↑p₂ : Type u_1)
hb₁ : Bijective b
hb₂ : ∀ (a : (↑p₁ : Type u_1)), G.Adj (↑a : V) (↑(b a) : V)
⊢ (p₁ ∪ Set.range fun (v : (↑p₁ : Type u_1)) ↦ (↑(b v) : V)) = Set.univ
have rw : p₁ ∪ p₂ = Set.univ
Tactic: rw [Set.range_comp', hb₁.surjective.range_eq, Subtype.coe_image_univ]
-- 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)
b : (↑p₁ : Type u_1) → (↑p₂ : Type u_1)
hb₁ : Bijective b
hb₂ : ∀ (a : (↑p₁ : Type u_1)), G.Adj (↑a : V) (↑(b a) : V)
⊢ (hall_subgraph (p := p₁) (fun (v : (↑p₁ : Type u_1)) ↦ (↑(b v) : V)) ⋯ hb₂).IsPerfectMatching
have this : (p₁ ∪ Set.range fun (v : (↑p₁ : Type u_1)) ↦ (↑(b v) : V)) = Set.univ
Tactic: have : p₁ ∪ Set.range (fun v ↦ (b v).1) = Set.univ := by
    rw [Set.range_comp', hb₁.surjective.range_eq, Subtype.coe_image_univ]
    exact union_eq_univ_of_forall_ncard_le h₁ h₂
-- 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)
b : (↑p₁ : Type u_1) → (↑p₂ : Type u_1)
hb₁ : Bijective b
hb₂ : ∀ (a : (↑p₁ : Type u_1)), G.Adj (↑a : V) (↑(b a) : V)
this : (p₁ ∪ Set.range fun (v : (↑p₁ : Type u_1)) ↦ (↑(b v) : V)) = Set.univ
⊢ (hall_subgraph (p := p₁) (fun (v : (↑p₁ : Type u_1)) ↦ (↑(b v) : V)) ⋯ hb₂).IsPerfectMatching
have h : ∀ v ∈ (hall_subgraph (p := p₁) (fun (v : (↑p₁ : Type u_1)) ↦ (↑(b v) : V)) sorry hb₂).verts,
  ∃! w : V, (hall_subgraph (p := p₁) (fun (v : (↑p₁ : Type u_1)) ↦ (↑(b v) : V)) sorry hb₂).Adj v w
Tactic: refine ⟨fun v _ ↦ ?_, Subgraph.isSpanning_iff.mpr this⟩
-- 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)
b : (↑p₁ : Type u_1) → (↑p₂ : Type u_1)
hb₁ : Bijective b
hb₂ : ∀ (a : (↑p₁ : Type u_1)), G.Adj (↑a : V) (↑(b a) : V)
this : (p₁ ∪ Set.range fun (v : (↑p₁ : Type u_1)) ↦ (↑(b v) : V)) = Set.univ
v : V
h : v ∈ (hall_subgraph (p := p₁) (fun (v : (↑p₁ : Type u_1)) ↦ (↑(b v) : V)) ⋯ hb₂).verts
⊢ ∃! w : V, (hall_subgraph (p := p₁) (fun (v : (↑p₁ : Type u_1)) ↦ (↑(b v) : V)) ⋯ hb₂).Adj v w
have h : ∃! w : V,
  if h : v ∈ p₁ then (↑(b (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) v sorry)) : V) = w
  else ∃ (h : w ∈ p₁), (↑(b (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) w sorry)) : V) = v
Tactic: simp only [dite_else_false]
-- 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)
b : (↑p₁ : Type u_1) → (↑p₂ : Type u_1)
hb₁ : Bijective b
hb₂ : ∀ (a : (↑p₁ : Type u_1)), G.Adj (↑a : V) (↑(b a) : V)
this : (p₁ ∪ Set.range fun (v : (↑p₁ : Type u_1)) ↦ (↑(b v) : V)) = Set.univ
v : V
h : v ∈ (hall_subgraph (p := p₁) (fun (v : (↑p₁ : Type u_1)) ↦ (↑(b v) : V)) ⋯ hb₂).verts
⊢ ∃! w : V,
    if h : v ∈ p₁ then (↑(b (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) v ⋯)) : V) = w
    else ∃ (h : w ∈ p₁), (↑(b (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) w ⋯)) : V) = v
have h : ∀ (h : v ∈ p₁), ∃! w : V, (↑(b (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) v sorry)) : V) = w
Tactic: split
-- 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)
b : (↑p₁ : Type u_1) → (↑p₂ : Type u_1)
hb₁ : Bijective b
hb₂ : ∀ (a : (↑p₁ : Type u_1)), G.Adj (↑a : V) (↑(b a) : V)
this : (p₁ ∪ Set.range fun (v : (↑p₁ : Type u_1)) ↦ (↑(b v) : V)) = Set.univ
v : V
h_1 : v ∈ (hall_subgraph (p := p₁) (fun (v : (↑p₁ : Type u_1)) ↦ (↑(b v) : V)) ⋯ hb₂).verts
h : ∀ (h : v ∈ p₁), ∃! w : V, (↑(b (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) v ⋯)) : V) = w
⊢ ∃! w : V,
    if h : v ∈ p₁ then (↑(b (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) v ⋯)) : V) = w
    else ∃ (h : w ∈ p₁), (↑(b (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) w ⋯)) : V) = v
have h₃ : v ∉ p₁ → ∃! w : V, ∃ (h : w ∈ p₁), (↑(b (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) w sorry)) : V) = v
Tactic: split
-- 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)
b : (↑p₁ : Type u_1) → (↑p₂ : Type u_1)
hb₁ : Bijective b
hb₂ : ∀ (a : (↑p₁ : Type u_1)), G.Adj (↑a : V) (↑(b a) : V)
this : (p₁ ∪ Set.range fun (v : (↑p₁ : Type u_1)) ↦ (↑(b v) : V)) = Set.univ
v : V
h : v ∈ (hall_subgraph (p := p₁) (fun (v : (↑p₁ : Type u_1)) ↦ (↑(b v) : V)) ⋯ hb₂).verts
h_1 : v ∉ p₁
⊢ ∃! w : V, ∃ (h : w ∈ p₁), (↑(b (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) w ⋯)) : V) = v
have h : ∀ (x : (↑p₁ : Type u_1)),
  ((fun (a : (↑p₁ : Type u_1)) ↦ b a = Subtype.mk (p := fun (x : V) ↦ x ∈ p₂) v sorry) x ∧
      ∀ (y : (↑p₁ : Type u_1)),
        (fun (a : (↑p₁ : Type u_1)) ↦ b a = Subtype.mk (p := fun (x : V) ↦ x ∈ p₂) v sorry) y → y = x) →
    ∃! w : V, ∃ (h : w ∈ p₁), (↑(b (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) w sorry)) : V) = v
Tactic: obtain ⟨x, _⟩ := hb₁.existsUnique ⟨v, by grind⟩