awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Hall
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₁ ∧ f x ∈ p₂ ∨ x ∈ p₂ ∧ f x ∈ p₁

Tactic:
have := h₁.mem_of_adj <| G.mem_neighborFinset _ _ |>.mp (hf₂ x)
-- Module: Mathlib.Combinatorics.SimpleGraph.Hall
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
this : x ∈ p₁ ∧ f x ∈ p₂ ∨ x ∈ p₂ ∧ f x ∈ p₁
⊢ x ∈ p₁ ∪ p₂

Tactic:
grind
-- Module: Mathlib.Combinatorics.SimpleGraph.Hall
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₂
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₂
⊢ 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

Premises used: Iff.mpr, Set.eq_univ_iff_forall
-- Module: Mathlib.Combinatorics.SimpleGraph.Hall
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)

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]

Premises used: SimpleGraph.neighborFinset, Finset.all_card_le_biUnion_card_iff_exists_injective, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Hall
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
⊢ ∀ (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
-- Module: Mathlib.Combinatorics.SimpleGraph.Hall
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₁
⊢ ∀ (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
-- Module: Mathlib.Combinatorics.SimpleGraph.Hall
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₂
x : V
⊢ f x ∈ p₁ ∨ f x ∈ p₂

Tactic:
simp [union_eq_univ_of_forall_ncard_le h₁ h₂, p₁.mem_union (f x) p₂ |>.mp]

Premises used: Set.mem_union, SimpleGraph.union_eq_univ_of_forall_ncard_le, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Hall
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₂
⊢ ∀ (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]
-- Module: Mathlib.Combinatorics.SimpleGraph.Hall
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₂
x : (↑p₁ : Type u_1)
⊢ f (↑x : V) ∈ p₂

Tactic:
grind
-- Module: Mathlib.Combinatorics.SimpleGraph.Hall
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)) ⋯
x : (↑p₂ : Type u_1)
⊢ f (↑x : V) ∈ p₁

Tactic:
grind
-- Module: Mathlib.Combinatorics.SimpleGraph.Hall
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)

Tactic:
Embedding.schroeder_bernstein_of_rel (f := f') (g := g') ?_ ?_ (fun x y ↦ G.Adj x y) ?_ ?_

Premises used: SimpleGraph.Adj, Function.Embedding.schroeder_bernstein_of_rel, Subtype.val
-- Module: Mathlib.Combinatorics.SimpleGraph.Hall
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)
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
⊢ ∃ (h : (↑p₁ : Type u_1) → (↑p₂ : Type u_1)), Bijective h ∧ ∀ (a : (↑p₁ : Type u_1)), G.Adj (↑a : V) (↑(h a) : V)

Tactic:
refine Embedding.schroeder_bernstein_of_rel (f := f') (g := g') ?_ ?_ (fun x y ↦ G.Adj x y) ?_ ?_

Premises used: SimpleGraph.Adj, Function.Embedding.schroeder_bernstein_of_rel, Subtype.val
-- Module: Mathlib.Combinatorics.SimpleGraph.Hall
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)) ⋯
⊢ Injective f'

Tactic:
Injective.of_comp (f := Subtype.val) <| hf₁.comp Subtype.val_injective

Premises used: Subtype.val_injective, Function.Injective.comp, Function.Injective.of_comp
-- Module: Mathlib.Combinatorics.SimpleGraph.Hall
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)) ⋯
⊢ Injective f'

Tactic:
exact Injective.of_comp (f := Subtype.val) <| hf₁.comp Subtype.val_injective

Premises used: Subtype.val_injective, Function.Injective.comp, Function.Injective.of_comp
-- Module: Mathlib.Combinatorics.SimpleGraph.Hall
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)) ⋯
⊢ Injective g'

Tactic:
Injective.of_comp (f := Subtype.val) <| hf₁.comp Subtype.val_injective

Premises used: Subtype.val_injective, Function.Injective.comp, Function.Injective.of_comp
-- Module: Mathlib.Combinatorics.SimpleGraph.Hall
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)) ⋯
⊢ Injective g'

Tactic:
exact Injective.of_comp (f := Subtype.val) <| hf₁.comp Subtype.val_injective

Premises used: Subtype.val_injective, Function.Injective.comp, Function.Injective.of_comp
-- Module: Mathlib.Combinatorics.SimpleGraph.Hall
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)) ⋯
⊢ ∀ (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:
fun v ↦ mem_neighborFinset _ _ _ |>.mp (hf₂ v)

Premises used: SimpleGraph.mem_neighborFinset, Iff.mp, Subtype.val
-- Module: Mathlib.Combinatorics.SimpleGraph.Hall
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)) ⋯
⊢ ∀ (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:
exact fun v ↦ mem_neighborFinset _ _ _ |>.mp (hf₂ v)

Premises used: SimpleGraph.mem_neighborFinset, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Hall
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)) ⋯
⊢ ∀ (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:
fun v ↦ mem_neighborFinset _ _ _ |>.mp (hf₂ v) |>.symm

Premises used: SimpleGraph.Adj.symm, SimpleGraph.mem_neighborFinset, Iff.mp, Subtype.val
-- Module: Mathlib.Combinatorics.SimpleGraph.Hall
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)) ⋯
⊢ ∀ (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:
exact fun v ↦ mem_neighborFinset _ _ _ |>.mp (hf₂ v) |>.symm

Premises used: SimpleGraph.Adj.symm, SimpleGraph.mem_neighborFinset, Iff.mp
-- Module: Mathlib.Combinatorics.SimpleGraph.Hall
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 :
  ∀ (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
⊢ ∃ (M : G.Subgraph), M.IsPerfectMatching

Tactic:
obtain ⟨b, hb₁, hb₂⟩ := exists_bijective_of_forall_ncard_le h₁ h₂

Premises used: SimpleGraph.exists_bijective_of_forall_ncard_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Hall
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)
h : (hall_subgraph (p := p₁) (fun (v : (↑p₁ : Type u_1)) ↦ (↑(b v) : V)) ⋯ hb₂).IsPerfectMatching
⊢ ∃ (M : G.Subgraph), M.IsPerfectMatching

Tactic:
use hall_subgraph (fun v ↦ b v) (fun v ↦ h₁.disjoint.notMem_of_mem_right (b v).property) hb₂

Premises used: _private.0.SimpleGraph.hall_subgraph
-- Module: Mathlib.Combinatorics.SimpleGraph.Hall
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)
rw : p₁ ∪ p₂ = Set.univ
⊢ (p₁ ∪ Set.range fun (v : (↑p₁ : Type u_1)) ↦ (↑(b v) : V)) = Set.univ

Tactic:
rw [Set.range_comp', hb₁.surjective.range_eq, Subtype.coe_image_univ]

Premises used: Function.Surjective.range_eq, Subtype.coe_image_univ, Function.Bijective.surjective, Set.range_comp'
-- Module: Mathlib.Combinatorics.SimpleGraph.Hall
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₁ ∪ p₂ = Set.univ

Tactic:
union_eq_univ_of_forall_ncard_le h₁ h₂

Premises used: SimpleGraph.union_eq_univ_of_forall_ncard_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Hall
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₁ ∪ p₂ = Set.univ

Tactic:
exact union_eq_univ_of_forall_ncard_le h₁ h₂

Premises used: SimpleGraph.union_eq_univ_of_forall_ncard_le
-- Module: Mathlib.Combinatorics.SimpleGraph.Hall
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

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₂
-- Module: Mathlib.Combinatorics.SimpleGraph.Hall
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

Tactic:
⟨fun v _ ↦ ?_, Subgraph.isSpanning_iff.mpr this⟩

Premises used: Iff.mpr, And.intro, SimpleGraph.Subgraph.IsPerfectMatching, SimpleGraph.Subgraph.isSpanning_iff
-- Module: Mathlib.Combinatorics.SimpleGraph.Hall
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
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
⊢ (hall_subgraph (p := p₁) (fun (v : (↑p₁ : Type u_1)) ↦ (↑(b v) : V)) ⋯ hb₂).IsPerfectMatching

Tactic:
refine ⟨fun v _ ↦ ?_, Subgraph.isSpanning_iff.mpr this⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Hall
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 :
  ∃! 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
⊢ ∃! w : V, (hall_subgraph (p := p₁) (fun (v : (↑p₁ : Type u_1)) ↦ (↑(b v) : V)) ⋯ hb₂).Adj v w

Tactic:
simp only [dite_else_false]

Premises used: dite_else_false
-- Module: Mathlib.Combinatorics.SimpleGraph.Hall
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
h₃ : v ∉ p₁ → ∃! w : V, ∃ (h : w ∈ p₁), (↑(b (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) w ⋯)) : V) = v
⊢ ∃! 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

Tactic:
split
-- Module: Mathlib.Combinatorics.SimpleGraph.Hall
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, (↑(b (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) v ⋯)) : V) = w

Tactic:
existsUnique_eq'

Premises used: existsUnique_eq'
-- Module: Mathlib.Combinatorics.SimpleGraph.Hall
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, (↑(b (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) v ⋯)) : V) = w

Tactic:
exact existsUnique_eq'

Premises used: existsUnique_eq'
-- Module: Mathlib.Combinatorics.SimpleGraph.Hall
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₁
⊢ v ∈ p₂

Tactic:
grind