awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.SimpleGraph.Girth
Goal:
α : Type u_1
G : SimpleGraph α
h : Nonempty.{u_1 + 1} ((i : α) × Subtype (α := G.Walk i i) Walk.IsCycle)
⊢ ∃ (x : (a : α) × { a_1 : G.Walk a a // a_1.IsCycle }),
    Eq (α := ℕ∞) (↑(↑(x.snd (β := fun (a : α) ↦ { a_1 : G.Walk a a // a_1.IsCycle })) : G.Walk x.fst x.fst).length : ℕ∞)
      (⨅ (x : (i : α) × Subtype (α := G.Walk i i) Walk.IsCycle),
        (↑(↑(x.snd (β := fun (i : α) ↦ Subtype (α := G.Walk i i) Walk.IsCycle)) : G.Walk x.fst x.fst).length : ℕ∞))

Tactic:
ciInf_mem _

Premises used: Set.Mem, setOf, ciInf_mem, Set.range
-- Module: Mathlib.Combinatorics.SimpleGraph.Girth
Goal:
α : Type u_1
G : SimpleGraph α
h : Nonempty.{u_1 + 1} ((i : α) × Subtype (α := G.Walk i i) Walk.IsCycle)
⊢ ∃ (x : (a : α) × { a_1 : G.Walk a a // a_1.IsCycle }),
    Eq (α := ℕ∞) (↑(↑(x.snd (β := fun (a : α) ↦ { a_1 : G.Walk a a // a_1.IsCycle })) : G.Walk x.fst x.fst).length : ℕ∞)
      (⨅ (x : (i : α) × Subtype (α := G.Walk i i) Walk.IsCycle),
        (↑(↑(x.snd (β := fun (i : α) ↦ Subtype (α := G.Walk i i) Walk.IsCycle)) : G.Walk x.fst x.fst).length : ℕ∞))

Tactic:
exact ciInf_mem _

Premises used: ciInf_mem
-- Module: Mathlib.Combinatorics.SimpleGraph.Girth
Goal:
α : Type u_1
G : SimpleGraph α
⊢ 3 ≤ G.egirth

Tactic:
simpa using fun _ _ a ↦ Walk.IsCycle.three_le_length a

Premises used: SimpleGraph.Walk.IsCycle.three_le_length
-- Module: Mathlib.Combinatorics.SimpleGraph.Girth
Goal:
α : Type u_1
⊢ egirth.{u_1} (α := α) ⊥ = ⊤

Tactic:
simp
-- Module: Mathlib.Combinatorics.SimpleGraph.Girth
Goal:
α : Type u_1
G : SimpleGraph α
a : α
w : G.Walk a a
h : w.IsCycle
⊢ G.girth ≤ w.length

Tactic:
ENat.coe_le_coe.mp <| G.egirth.coe_toNat_le_self.trans <| egirth_le_length h

Premises used: ENat.coe_toNat_le_self, ENat.coe_le_coe, Iff.mp, SimpleGraph.egirth_le_length, SimpleGraph.egirth, LE.le.trans
-- Module: Mathlib.Combinatorics.SimpleGraph.Girth
Goal:
α : Type u_1
G : SimpleGraph α
hG : ¬G.IsAcyclic
⊢ 3 ≤ G.girth

Tactic:
ENat.toNat_le_toNat three_le_egirth <| egirth_eq_top.not.mpr hG

Premises used: Iff.mpr, SimpleGraph.three_le_egirth, SimpleGraph.egirth_eq_top, Iff.not, SimpleGraph.girth, ENat.toNat_le_toNat, ENat.toNat, WithTop.untopD, WithTop.recTopCoe
-- Module: Mathlib.Combinatorics.SimpleGraph.Girth
Goal:
α : Type u_1
G : SimpleGraph α
h : G.girth = 0
⊢ ¬3 ≤ G.girth

Tactic:
lia
-- Module: Mathlib.Combinatorics.SimpleGraph.Girth
Goal:
α : Type u_1
G : SimpleGraph α
h : G.IsAcyclic
⊢ G.girth = 0

Tactic:
simp [girth, h]

Premises used: SimpleGraph.girth
-- Module: Mathlib.Combinatorics.SimpleGraph.Girth
Goal:
α : Type u_1
G G' : SimpleGraph α
hab : G ≤ G'
h : ¬G.IsAcyclic
⊢ G'.girth ≤ G.girth

Tactic:
ENat.toNat_le_toNat (egirth_anti hab) <| egirth_eq_top.not.mpr h

Premises used: Iff.mpr, SimpleGraph.egirth_eq_top, Iff.not, SimpleGraph.girth, ENat.toNat_le_toNat, SimpleGraph.egirth_anti
-- Module: Mathlib.Combinatorics.SimpleGraph.Girth
Goal:
α : Type u_1
G : SimpleGraph α
tauto tauto₁ : ∀ (w : α) (w_1 : G.Walk w w), w_1.IsCycle → G.girth = w_1.length → ¬G.IsAcyclic
tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ :
  ∀ (w : α) (w_1 : G.Walk w w), w_1.IsCycle → G.girth = w_1.length → G.IsAcyclic → False
⊢ (∃ (a : α) (w : G.Walk a a), w.IsCycle ∧ G.girth = w.length) → ¬G.IsAcyclic

Tactic:
tauto
-- Module: Mathlib.Combinatorics.SimpleGraph.Girth
Goal:
α : Type u_1
G : SimpleGraph α
refine : ∀ (h : ¬G.IsAcyclic), ∃ (a : α) (w : G.Walk a a), w.IsCycle ∧ G.girth = w.length
⊢ (∃ (a : α) (w : G.Walk a a), w.IsCycle ∧ G.girth = w.length) ↔ ¬G.IsAcyclic

Tactic:
refine ⟨by tauto, fun h ↦ ?_⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Girth
Goal:
α : Type u_1
G : SimpleGraph α
h : ¬G.IsAcyclic
obtain :
  ∀ (w : α) (w_1 : G.Walk w w),
    w_1.IsCycle ∧ G.egirth = (↑w_1.length : ℕ∞) → ∃ (a : α) (w : G.Walk a a), w.IsCycle ∧ G.girth = w.length
⊢ ∃ (a : α) (w : G.Walk a a), w.IsCycle ∧ G.girth = w.length

Tactic:
obtain ⟨_, _, _⟩ := exists_egirth_eq_length.mpr h

Premises used: Iff.mpr, SimpleGraph.exists_egirth_eq_length
-- Module: Mathlib.Combinatorics.SimpleGraph.Girth
Goal:
α : Type u_1
G : SimpleGraph α
h : ¬G.IsAcyclic
w : α
w_1 : G.Walk w w
h_1 : w_1.IsCycle ∧ G.egirth = (↑w_1.length : ℕ∞)
simp_all : ∃ (a : α) (w_2 : G.Walk a a), w_2.IsCycle ∧ w_1.length = w_2.length
⊢ ∃ (a : α) (w : G.Walk a a), w.IsCycle ∧ G.girth = w.length

Tactic:
simp_all only [girth, ENat.toNat_coe]

Premises used: SimpleGraph.girth, ENat.toNat_coe
-- Module: Mathlib.Combinatorics.SimpleGraph.Girth
Goal:
α : Type u_1
G : SimpleGraph α
h : ¬G.IsAcyclic
w_1 : α
w_2 : G.Walk w_1 w_1
h_1 : w_2.IsCycle ∧ G.egirth = (↑w_2.length : ℕ∞)
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ :
  w_2.IsCycle → G.egirth = (↑w_2.length : ℕ∞) → ∃ (a : α) (w : G.Walk a a), w.IsCycle ∧ w_2.length = w.length
h₁ : w_2.IsCycle → G.egirth = (↑w_2.length : ℕ∞) → ∃ (w : G.Walk w_1 w_1), w.IsCycle ∧ w_2.length = w.length
w : w_2.IsCycle → G.egirth = (↑w_2.length : ℕ∞) → α
h₂ : w_2.IsCycle → G.egirth = (↑w_2.length : ℕ∞) → ∃ (w : G.Walk w_1 w_1), w.IsCycle ∧ w_2.length = w.length
w₁ : w_2.IsCycle → G.egirth = (↑w_2.length : ℕ∞) → α
⊢ ∃ (a : α) (w : G.Walk a a), w.IsCycle ∧ w_2.length = w.length

Tactic:
tauto
-- Module: Mathlib.Combinatorics.SimpleGraph.Girth
Goal:
α : Type u_1
⊢ girth.{u_1} (α := α) ⊥ = 0

Tactic:
simp [girth]

Premises used: SimpleGraph.girth
-- Module: Mathlib.Combinatorics.SimpleGraph.Hall
Goal:
V : Type u_1
G : SimpleGraph V
p : Set V
inst : DecidablePred fun (x : V) ↦ x ∈ p
f : (↑p : Type u_1) → V
h₁ : ∀ (x : (↑p : Type u_1)), f x ∉ p
h₂ : ∀ (x : (↑p : Type u_1)), G.Adj (↑x : V) (f x)
v w : V
h :
  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
pos : ∀ (h : v ∈ p) (h : f (Subtype.mk (p := fun (x : V) ↦ x ∈ p) v h) = w), G.Adj v w
pos₁ : v ∉ p → ∀ (h : w ∈ p) (h : f (Subtype.mk (p := fun (x : V) ↦ x ∈ p) w h) = v), G.Adj v w
⊢ G.Adj v w

Tactic:
split_ifs at h
-- Module: Mathlib.Combinatorics.SimpleGraph.Hall
Goal:
V : Type u_1
G : SimpleGraph V
p : Set V
inst : DecidablePred fun (x : V) ↦ x ∈ p
f : (↑p : Type u_1) → V
h₁ : ∀ (x : (↑p : Type u_1)), f x ∉ p
h₂ : ∀ (x : (↑p : Type u_1)), G.Adj (↑x : V) (f x)
v w : V
h_1 : v ∈ p
h : f (Subtype.mk (p := fun (x : V) ↦ x ∈ p) v h_1) = w
⊢ v ∈ p

Tactic:
assumption
-- Module: Mathlib.Combinatorics.SimpleGraph.Hall
Goal:
V : Type u_1
G : SimpleGraph V
p : Set V
inst : DecidablePred fun (x : V) ↦ x ∈ p
f : (↑p : Type u_1) → V
h₁ : ∀ (x : (↑p : Type u_1)), f x ∉ p
h₂ : ∀ (x : (↑p : Type u_1)), G.Adj (↑x : V) (f x)
v w : V
h_1 : v ∈ p
h : f (Subtype.mk (p := fun (x : V) ↦ x ∈ p) v h_1) = w
⊢ G.Adj v w

Tactic:
exact h ▸ h₂ ⟨v, by assumption⟩
-- Module: Mathlib.Combinatorics.SimpleGraph.Hall
Goal:
V : Type u_1
G : SimpleGraph V
p : Set V
inst : DecidablePred fun (x : V) ↦ x ∈ p
f : (↑p : Type u_1) → V
h₁ : ∀ (x : (↑p : Type u_1)), f x ∉ p
h₂ : ∀ (x : (↑p : Type u_1)), G.Adj (↑x : V) (f x)
v w : V
h_1 : v ∉ p
h_2 : w ∈ p
h : f (Subtype.mk (p := fun (x : V) ↦ x ∈ p) w h_2) = v
⊢ w ∈ p

Tactic:
assumption
-- Module: Mathlib.Combinatorics.SimpleGraph.Hall
Goal:
V : Type u_1
G : SimpleGraph V
p : Set V
inst : DecidablePred fun (x : V) ↦ x ∈ p
f : (↑p : Type u_1) → V
h₁ : ∀ (x : (↑p : Type u_1)), f x ∉ p
h₂ : ∀ (x : (↑p : Type u_1)), G.Adj (↑x : V) (f x)
v w : V
h_1 : v ∉ p
h_2 : w ∈ p
h : f (Subtype.mk (p := fun (x : V) ↦ x ∈ p) w h_2) = v
⊢ G.Adj v w

Tactic:
exact h ▸ h₂ ⟨w, by assumption⟩ |>.symm
-- Module: Mathlib.Combinatorics.SimpleGraph.Hall
Goal:
V : Type u_1
G : SimpleGraph V
p : Set V
inst : DecidablePred fun (x : V) ↦ x ∈ p
f : (↑p : Type u_1) → V
h₁ : ∀ (x : (↑p : Type u_1)), f x ∉ p
h₂ : ∀ (x : (↑p : Type u_1)), G.Adj (↑x : V) (f x)
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) →
    v ∈ p ∪ Set.range f

Tactic:
grind
-- Module: Mathlib.Combinatorics.SimpleGraph.Hall
Goal:
V : Type u_1
G : SimpleGraph V
p : Set V
inst : DecidablePred fun (x : V) ↦ x ∈ p
f : (↑p : Type u_1) → V
h₁ : ∀ (x : (↑p : Type u_1)), f x ∉ p
h₂ : ∀ (x : (↑p : Type u_1)), G.Adj (↑x : V) (f x)
x y : V
⊢ (fun (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 :
          Prop))
      x y →
    (fun (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 :
          Prop))
      y x

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 ⊆ p₁, s.ncard ≤ Set.ncard.{u_1} (α := V) (⋃ x ∈ s, G.neighborSet x)
s : Finset (↑p₁ : Type u_1)
⊢ (↑(Finset.image (Subtype.val (p := fun (x : V) ↦ x ∈ p₁)) s) : Set V) ⊆ p₁

Tactic:
simp
-- 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 ⊆ p₁, s.ncard ≤ Set.ncard.{u_1} (α := V) (⋃ x ∈ s, G.neighborSet x)
s : Finset (↑p₁ : Type u_1)
⊢ (↑(Finset.image (Subtype.val (p := fun (x : V) ↦ x ∈ p₁)) s) : Set V).ncard ≤
    Set.ncard.{u_1} (α := V)
      (⋃ x ∈ (↑(Finset.image (Subtype.val (p := fun (x : V) ↦ x ∈ p₁)) s) : Set V), G.neighborSet x)

Tactic:
have := h₂ (s.image Subtype.val) (by simp)
-- 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 ⊆ p₁, s.ncard ≤ Set.ncard.{u_1} (α := V) (⋃ x ∈ s, G.neighborSet x)
s : Finset (↑p₁ : Type u_1)
this :
  (↑(Finset.image (Subtype.val (p := fun (x : V) ↦ x ∈ p₁)) s) : Set V).ncard ≤
    Set.ncard.{u_1} (α := V)
      (⋃ x ∈ (↑(Finset.image (Subtype.val (p := fun (x : V) ↦ x ∈ p₁)) s) : Set V), G.neighborSet x)
⊢ s.card ≤
    Set.ncard.{u_1} (α := V)
      (⋃ x ∈ (↑(Finset.image (Subtype.val (p := fun (x : V) ↦ x ∈ p₁)) s) : Set V), G.neighborSet x)

Tactic:
rw [Set.ncard_coe_finset, Finset.card_image_of_injective _ Subtype.val_injective] at this

Premises used: Subtype.val_injective, Finset.card_image_of_injective, Set.ncard_coe_finset
-- 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 ⊆ p₁, s.ncard ≤ Set.ncard.{u_1} (α := V) (⋃ x ∈ s, G.neighborSet x)
s : Finset (↑p₁ : Type u_1)
this :
  s.card ≤
    Set.ncard.{u_1} (α := V)
      (⋃ x ∈ (↑(Finset.image (Subtype.val (p := fun (x : V) ↦ x ∈ p₁)) s) : Set V), G.neighborSet x)
⊢ s.card ≤ Finset.card (α := V) (s.biUnion fun (x : (↑p₁ : Type u_1)) ↦ G.neighborFinset (↑x : V))

Tactic:
simpa [← Set.ncard_coe_finset, neighborFinset_def]

Premises used: SimpleGraph.neighborFinset_def, Set.ncard_coe_finset
-- 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 ⊆ 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

Tactic:
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]

Premises used: SimpleGraph.neighborFinset, Finset.all_card_le_biUnion_card_iff_exists_injective, 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 ⊆ 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)
⊢ ∀ (x : (↑p₁ : Type u_1)), f x ∉ p₁

Tactic:
have (x : p₁) : f x ∉ p₁ := h₁.disjoint |>.notMem_of_mem_right <|
    isBipartiteWith_neighborSet_subset h₁ x.2 <| 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 ⊆ 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₁
h :
  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

Tactic:
use hall_subgraph f this (fun v ↦ G.mem_neighborFinset _ _ |>.mp <| hf₂ v)

Premises used: _private.0.SimpleGraph.hall_subgraph, 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 ⊆ 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₁
⊢ p₁ ⊆ Subgraph.verts (G := G) (hall_subgraph (p := p₁) f this ⋯)

Tactic:
simp
-- 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 ⊆ 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₁
h :
  ∀ (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
⊢ p₁ ⊆ Subgraph.verts (G := G) (hall_subgraph (p := p₁) f this ⋯) ∧
    Subgraph.IsMatching (G := G) (hall_subgraph (p := p₁) f this ⋯)

Tactic:
refine ⟨by simp, fun v hv ↦ ?_⟩
-- 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 ⊆ 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 ∈ Subgraph.verts (G := G) (hall_subgraph (p := p₁) f this ⋯)
⊢ v ∈ p₁ ∨ ∃ (a : V) (b : a ∈ p₁), f (Subtype.mk (p := fun (a : V) ↦ a ∈ p₁) a b) = v

Tactic:
simp only [Set.mem_union, Set.mem_range, Subtype.exists] at hv ⊢

Premises used: Set.mem_union, Set.mem_range, Subtype.exists
-- 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 ⊆ 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
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
⊢ ∃! 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₂⟩
-- 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 ⊆ 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
h' : 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))
      (f (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) v h')) ∧
    ∀ (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 = f (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) v h')

Tactic:
simp_all
-- 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 ⊆ 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
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:
exact ⟨f ⟨v, h'⟩, by simp_all⟩
-- 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 ⊆ 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
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
⊢ ∃! 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:
use 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 ⊆ 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
⊢ v ∉ p₁

Tactic:
have := hx₂ ▸ this ⟨x, hx₁⟩
-- 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 ⊆ 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₁
h : ∀ (y : V) (x_1 : y ∈ p₁) (h : f (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) y x_1) = v), y = x
⊢ (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:
simp only [this, ↓reduceDIte, hx₁, hx₂, dite_else_false, forall_exists_index, true_and]

Premises used: dite_else_false, forall_exists_index, reduceDIte, true_and
-- 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 ⊆ 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₁
⊢ ∀ (y : V) (x_1 : y ∈ p₁) (h : f (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) y x_1) = v), y = x

Tactic:
fun _ _ k ↦ Subtype.ext_iff.mp <| hf₁ (hx₂ ▸ k)
-- 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 ⊆ 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₁
⊢ ∀ (y : V) (x_1 : y ∈ p₁) (h : f (Subtype.mk (p := fun (x : V) ↦ x ∈ p₁) y x_1) = v), y = x

Tactic:
exact fun _ _ k ↦ Subtype.ext_iff.mp <| hf₁ (hx₂ ▸ k)

Premises used: Subtype.ext_iff, 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)
s : Finset V
⊢ (↑s : Set V).ncard ≤ Set.ncard.{u_1} (α := V) (⋃ x ∈ (↑s : Set V), G.neighborSet x)

Tactic:
have := h₂ s
-- 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)
s : Finset V
this : (↑s : Set V).ncard ≤ Set.ncard.{u_1} (α := V) (⋃ x ∈ (↑s : Set V), G.neighborSet x)
⊢ s.card ≤ Finset.card (α := V) (s.biUnion fun (x : V) ↦ G.neighborFinset x)

Tactic:
simpa [← Set.ncard_coe_finset, neighborFinset_def]

Premises used: SimpleGraph.neighborFinset_def, Set.ncard_coe_finset
-- 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
⊢ 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]

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
left : Injective f
hf₂ : ∀ (x : V), f x ∈ G.neighborFinset x
⊢ p₁ ∪ p₂ = Set.univ

Tactic:
Set.eq_univ_iff_forall.mpr fun x ↦ ?_

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)
f : V → V
left : Injective f
hf₂ : ∀ (x : V), f x ∈ G.neighborFinset x
refine : ∀ (x : V), x ∈ p₁ ∪ p₂
⊢ p₁ ∪ p₂ = Set.univ

Tactic:
refine Set.eq_univ_iff_forall.mpr fun x ↦ ?_

Premises used: Iff.mpr, Set.eq_univ_iff_forall