-- Mathlib/Combinatorics/Hall/Finite.lean
theorem hall_cond_of_erase {x : ι} (a : α)
    (ha : ∀ s : Finset ι, s.Nonempty → s ≠ univ → #s < #(s.biUnion t))
    (s' : Finset { x' : ι | x' ≠ x }) : #s' ≤ #(s'.biUnion fun x' => (t x').erase a)

Proof state:
case pos
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
s' : Finset ↑{x' | x' ≠ x}
this : DecidableEq ι
ha : s'.Nonempty → image (fun z => ↑z) s' ≠ univ → #s' < #((image (fun z => ↑z) s').biUnion t)
he : s'.Nonempty
ha' : #s' < #(s'.biUnion fun x_1 => t ↑x_1)
hb : a ∈ s'.biUnion fun x_1 => t ↑x_1
⊢ #s' ≤ #((s'.biUnion fun x' => t ↑x').erase a)

Tactic:
rw [card_erase_of_mem hb]

Result:
case pos
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
s' : Finset ↑{x' | x' ≠ x}
this : DecidableEq ι
ha : s'.Nonempty → image (fun z => ↑z) s' ≠ univ → #s' < #((image (fun z => ↑z) s').biUnion t)
he : s'.Nonempty
ha' : #s' < #(s'.biUnion fun x_1 => t ↑x_1)
hb : a ∈ s'.biUnion fun x_1 => t ↑x_1
⊢ #s' ≤ #(s'.biUnion fun x_1 => t ↑x_1) - 1

Proof state:
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
s' : Finset ↑{x' | x' ≠ x}
this : DecidableEq ι
ha :
  (image (fun z => ↑z) s').Nonempty →
    image (fun z => ↑z) s' ≠ univ → #(image (fun z => ↑z) s') < #((image (fun z => ↑z) s').biUnion t)
⊢ #s' ≤ #(s'.biUnion fun x' => (t ↑x').erase a)

Tactic:
rw [image_nonempty, Finset.card_image_of_injective s' Subtype.coe_injective] at ha

Result:
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
s' : Finset ↑{x' | x' ≠ x}
this : DecidableEq ι
ha : s'.Nonempty → image (fun z => ↑z) s' ≠ univ → #s' < #((image (fun z => ↑z) s').biUnion t)
⊢ #s' ≤ #(s'.biUnion fun x' => (t ↑x').erase a)

Proof state:
case neg
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
s' : Finset ↑{x' | x' ≠ x}
this : DecidableEq ι
ha : s'.Nonempty → image (fun z => ↑z) s' ≠ univ → #s' < #((image (fun z => ↑z) s').biUnion t)
he : s' = ∅
⊢ #s' ≤ #(s'.biUnion fun x' => (t ↑x').erase a)

Tactic:
subst s'

Result:
case neg
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
this : DecidableEq ι
ha : ∅.Nonempty → image (fun z => ↑z) ∅ ≠ univ → #∅ < #((image (fun z => ↑z) ∅).biUnion t)
⊢ #∅ ≤ #(∅.biUnion fun x' => (t ↑x').erase a)

Proof state:
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
s' : Finset ↑{x' | x' ≠ x}
this : DecidableEq ι
ha : s'.Nonempty → image (fun z => ↑z) s' ≠ univ → #s' < #((image (fun z => ↑z) s').biUnion t)
he : s'.Nonempty
h : image (fun z => ↑z) s' = univ
⊢ False

Tactic:
simpa [← h] using mem_univ x

Result:
no goals

Proof state:
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
s' : Finset ↑{x' | x' ≠ x}
this : DecidableEq ι
ha : s'.Nonempty → image (fun z => ↑z) s' ≠ univ → #s' < #((image (fun z => ↑z) s').biUnion t)
⊢ #s' ≤ #(s'.biUnion fun x' => (t ↑x').erase a)

Tactic:
by_cases he : s'.Nonempty

Result:
case pos
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
s' : Finset ↑{x' | x' ≠ x}
this : DecidableEq ι
ha : s'.Nonempty → image (fun z => ↑z) s' ≠ univ → #s' < #((image (fun z => ↑z) s').biUnion t)
he : s'.Nonempty
⊢ #s' ≤ #(s'.biUnion fun x' => (t ↑x').erase a)

case neg
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
s' : Finset ↑{x' | x' ≠ x}
this : DecidableEq ι
ha : s'.Nonempty → image (fun z => ↑z) s' ≠ univ → #s' < #((image (fun z => ↑z) s').biUnion t)
he : ¬s'.Nonempty
⊢ #s' ≤ #(s'.biUnion fun x' => (t ↑x').erase a)

Proof state:
case neg
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
s' : Finset ↑{x' | x' ≠ x}
this : DecidableEq ι
ha : s'.Nonempty → image (fun z => ↑z) s' ≠ univ → #s' < #((image (fun z => ↑z) s').biUnion t)
he : s'.Nonempty
ha' : #s' < #(s'.biUnion fun x_1 => t ↑x_1)
hb : a ∉ s'.biUnion fun x_1 => t ↑x_1
⊢ #s' ≤ #(s'.biUnion fun x_1 => t ↑x_1)

Tactic:
exact Nat.le_of_lt ha'

Result:
no goals

Proof state:
case neg
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
this : DecidableEq ι
ha : ∅.Nonempty → image (fun z => ↑z) ∅ ≠ univ → #∅ < #((image (fun z => ↑z) ∅).biUnion t)
⊢ #∅ ≤ #(∅.biUnion fun x' => (t ↑x').erase a)

Tactic:
simp

Result:
no goals

Proof state:
case pos
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
s' : Finset ↑{x' | x' ≠ x}
this : DecidableEq ι
ha : s'.Nonempty → image (fun z => ↑z) s' ≠ univ → #s' < #((image (fun z => ↑z) s').biUnion t)
he : s'.Nonempty
ha' : #s' < #(s'.biUnion fun x_1 => t ↑x_1)
⊢ #s' ≤ #(s'.biUnion fun x' => (t ↑x').erase a)

Tactic:
rw [← erase_biUnion]

Result:
case pos
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
s' : Finset ↑{x' | x' ≠ x}
this : DecidableEq ι
ha : s'.Nonempty → image (fun z => ↑z) s' ≠ univ → #s' < #((image (fun z => ↑z) s').biUnion t)
he : s'.Nonempty
ha' : #s' < #(s'.biUnion fun x_1 => t ↑x_1)
⊢ #s' ≤ #((s'.biUnion fun x' => t ↑x').erase a)

Proof state:
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
ha : ∀ (s : Finset ι), s.Nonempty → s ≠ univ → #s < #(s.biUnion t)
s' : Finset ↑{x' | x' ≠ x}
⊢ #s' ≤ #(s'.biUnion fun x' => (t ↑x').erase a)

Tactic:
haveI := Classical.decEq ι

Result:
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
ha : ∀ (s : Finset ι), s.Nonempty → s ≠ univ → #s < #(s.biUnion t)
s' : Finset ↑{x' | x' ≠ x}
this : DecidableEq ι
⊢ #s' ≤ #(s'.biUnion fun x' => (t ↑x').erase a)

Proof state:
case neg
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
s' : Finset ↑{x' | x' ≠ x}
this : DecidableEq ι
ha : s'.Nonempty → image (fun z => ↑z) s' ≠ univ → #s' < #((image (fun z => ↑z) s').biUnion t)
he : ¬s'.Nonempty
⊢ #s' ≤ #(s'.biUnion fun x' => (t ↑x').erase a)

Tactic:
rw [nonempty_iff_ne_empty, not_not] at he

Result:
case neg
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
s' : Finset ↑{x' | x' ≠ x}
this : DecidableEq ι
ha : s'.Nonempty → image (fun z => ↑z) s' ≠ univ → #s' < #((image (fun z => ↑z) s').biUnion t)
he : s' = ∅
⊢ #s' ≤ #(s'.biUnion fun x' => (t ↑x').erase a)

Proof state:
case pos
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
s' : Finset ↑{x' | x' ≠ x}
this : DecidableEq ι
ha : s'.Nonempty → image (fun z => ↑z) s' ≠ univ → #s' < #((image (fun z => ↑z) s').biUnion t)
he : s'.Nonempty
ha' : #s' < #(s'.biUnion fun x_1 => t ↑x_1)
⊢ #s' ≤ #((s'.biUnion fun x' => t ↑x').erase a)

Tactic:
by_cases hb : a ∈ s'.biUnion fun x => t x

Result:
case pos
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
s' : Finset ↑{x' | x' ≠ x}
this : DecidableEq ι
ha : s'.Nonempty → image (fun z => ↑z) s' ≠ univ → #s' < #((image (fun z => ↑z) s').biUnion t)
he : s'.Nonempty
ha' : #s' < #(s'.biUnion fun x_1 => t ↑x_1)
hb : a ∈ s'.biUnion fun x_1 => t ↑x_1
⊢ #s' ≤ #((s'.biUnion fun x' => t ↑x').erase a)

case neg
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
x : ι
a : α
s' : Finset ↑{x' | x' ≠ x}
this : DecidableEq ι
ha : s'.Nonempty → image (fun z => ↑z) s' ≠ univ → #s' < #((image (fun z => ↑z) s').biUnion t)
he : s'.Nonempty
ha' : #s' < #(s'.biUnion fun x_1 => t ↑x_1)
hb : a ∉ s'.biUnion fun x_1 => t ↑x_1
⊢ #s' ≤ #((s'.biUnion fun x' => t ↑x').erase a)