-- 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
⊢ #s' ≤ #(s'.biUnion fun x' => (t ↑x').erase a)

Tactic:
have ha' : #s' < #(s'.biUnion fun x => t x) := by
  convert ha he fun h => by simpa [← h] using mem_univ x using 2
  ext x
  simp only [mem_image, mem_biUnion, exists_prop, SetCoe.exists, exists_and_right,
    exists_eq_right, Subtype.coe_mk]

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

Tactic:
exact Nat.le_sub_one_of_lt ha'

Result:
no goals

Proof state:
case h.e'_4.h.e'_2
ι : 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'.biUnion fun x_1 => t ↑x_1) = (image (fun z => ↑z) s').biUnion t

Tactic:
ext x

Result:
case h.e'_4.h.e'_2.h
ι : 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
x : α
⊢ (x ∈ s'.biUnion fun x => t ↑x) ↔ x ∈ (image (fun z => ↑z) s').biUnion t

Proof state:
case h.e'_4.h.e'_2.h
ι : 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
x : α
⊢ (x ∈ s'.biUnion fun x => t ↑x) ↔ x ∈ (image (fun z => ↑z) s').biUnion t

Tactic:
simp only [mem_image, mem_biUnion, exists_prop, SetCoe.exists, exists_and_right,
  exists_eq_right, Subtype.coe_mk]

Result:
no goals

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' => t ↑x').erase a)

Tactic:
rw [erase_eq_of_not_mem hb]

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'.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)

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}
this : DecidableEq ι
⊢ #s' ≤ #(s'.biUnion fun x' => (t ↑x').erase a)

Tactic:
specialize ha (s'.image fun z => z.1)

Result:
ι : 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)

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
⊢ #s' < #(s'.biUnion fun x_1 => t ↑x_1)

Tactic:
convert ha he fun h => by simpa [← h] using mem_univ x using 2

Result:
case h.e'_4.h.e'_2
ι : 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'.biUnion fun x_1 => t ↑x_1) = (image (fun z => ↑z) s').biUnion t