-- Mathlib/Combinatorics/Hall/Finite.lean
theorem hall_cond_of_compl {ι : Type u} {t : ι → Finset α} {s : Finset ι}
    (hus : #s = #(s.biUnion t)) (ht : ∀ s : Finset ι, #s ≤ #(s.biUnion t))
    (s' : Finset (sᶜ : Set ι)) : #s' ≤ #(s'.biUnion fun x' => t x' \ s.biUnion t)

Proof state:
α : Type v
inst✝ : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
hus : #s = #(s.biUnion t)
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset ↑(↑s)ᶜ
this : DecidableEq ι
disj : Disjoint s (image (fun z => ↑z) s')
⊢ #s' = #(s ∪ image (fun z => ↑z) s') - #s

Tactic:
simp [disj, card_image_of_injective _ Subtype.coe_injective, Nat.add_sub_cancel_left]

Result:
no goals

Proof state:
α : Type v
inst✝ : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
hus : #s = #(s.biUnion t)
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset ↑(↑s)ᶜ
this✝ : DecidableEq ι
disj : Disjoint s (image (fun z => ↑z) s')
this : #s' = #(s ∪ image (fun z => ↑z) s') - #s
⊢ #((s ∪ image (fun z => ↑z) s').biUnion t) - #(s.biUnion t) ≤ #(s'.biUnion fun x' => t ↑x' \ s.biUnion t)

Tactic:
rw [← card_sdiff]

Result:
α : Type v
inst✝ : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
hus : #s = #(s.biUnion t)
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset ↑(↑s)ᶜ
this✝ : DecidableEq ι
disj : Disjoint s (image (fun z => ↑z) s')
this : #s' = #(s ∪ image (fun z => ↑z) s') - #s
⊢ #((s ∪ image (fun z => ↑z) s').biUnion t \ s.biUnion t) ≤ #(s'.biUnion fun x' => t ↑x' \ s.biUnion t)

α : Type v
inst✝ : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
hus : #s = #(s.biUnion t)
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset ↑(↑s)ᶜ
this✝ : DecidableEq ι
disj : Disjoint s (image (fun z => ↑z) s')
this : #s' = #(s ∪ image (fun z => ↑z) s') - #s
⊢ s.biUnion t ⊆ (s ∪ image (fun z => ↑z) s').biUnion t

Proof state:
α : Type v
inst✝ : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
hus : #s = #(s.biUnion t)
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset ↑(↑s)ᶜ
this : DecidableEq ι
disj : Disjoint s (image (fun z => ↑z) s')
⊢ #s' ≤ #(s'.biUnion fun x' => t ↑x' \ s.biUnion t)

Tactic:
have : #s' = #(s ∪ s'.image fun z => z.1) - #s := by
  simp [disj, card_image_of_injective _ Subtype.coe_injective, Nat.add_sub_cancel_left]

Result:
α : Type v
inst✝ : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
hus : #s = #(s.biUnion t)
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset ↑(↑s)ᶜ
this✝ : DecidableEq ι
disj : Disjoint s (image (fun z => ↑z) s')
this : #s' = #(s ∪ image (fun z => ↑z) s') - #s
⊢ #s' ≤ #(s'.biUnion fun x' => t ↑x' \ s.biUnion t)

Proof state:
α : Type v
inst✝ : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
hus : #s = #(s.biUnion t)
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset ↑(↑s)ᶜ
this : DecidableEq ι
⊢ #s' ≤ #(s'.biUnion fun x' => t ↑x' \ s.biUnion t)

Tactic:
have disj : Disjoint s (s'.image fun z => z.1) := by
  simp only [disjoint_left, not_exists, mem_image, exists_prop, SetCoe.exists, exists_and_right,
    exists_eq_right, Subtype.coe_mk]
  intro x hx hc _
  exact absurd hx hc

Result:
α : Type v
inst✝ : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
hus : #s = #(s.biUnion t)
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset ↑(↑s)ᶜ
this : DecidableEq ι
disj : Disjoint s (image (fun z => ↑z) s')
⊢ #s' ≤ #(s'.biUnion fun x' => t ↑x' \ s.biUnion t)

Proof state:
case inl
α : Type v
inst✝ : DecidableEq α
ι : Type u
t✝ : ι → Finset α
s : Finset ι
hus : #s = #(s.biUnion t✝)
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t✝)
s' : Finset ↑(↑s)ᶜ
this✝ : DecidableEq ι
disj : Disjoint s (image (fun z => ↑z) s')
this : #s' = #(s ∪ image (fun z => ↑z) s') - #s
t : α
x : ι
hx : x ∈ s
rat : t ∈ t✝ x
hs : ∀ (x : ι), ¬(x ∈ s ∧ t ∈ t✝ x)
⊢ ∃ a ∈ s', t ∈ t✝ ↑a ∧ ∀ (x : ι), ¬(x ∈ s ∧ t ∈ t✝ x)

Tactic:
exact False.elim <| (hs x) <| And.intro hx rat

Result:
no goals

Proof state:
case h
α : Type v
inst✝ : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
hus : #s = #(s.biUnion t)
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset ↑(↑s)ᶜ
this✝ : DecidableEq ι
disj : Disjoint s (image (fun z => ↑z) s')
this : #s' = #(s ∪ image (fun z => ↑z) s') - #s
⊢ s ⊆ s ∪ image (fun z => ↑z) s'

Tactic:
apply subset_union_left

Result:
no goals

Proof state:
α : Type v
inst✝ : DecidableEq α
ι : Type u
t : ι → Finset α
s : Finset ι
hus : #s = #(s.biUnion t)
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
s' : Finset ↑(↑s)ᶜ
this✝ : DecidableEq ι
disj : Disjoint s (image (fun z => ↑z) s')
this : #s' = #(s ∪ image (fun z => ↑z) s') - #s
⊢ (s ∪ image (fun z => ↑z) s').biUnion t \ s.biUnion t ⊆ s'.biUnion fun x' => t ↑x' \ s.biUnion t

Tactic:
intro t

Result:
α : Type v
inst✝ : DecidableEq α
ι : Type u
t✝ : ι → Finset α
s : Finset ι
hus : #s = #(s.biUnion t✝)
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t✝)
s' : Finset ↑(↑s)ᶜ
this✝ : DecidableEq ι
disj : Disjoint s (image (fun z => ↑z) s')
this : #s' = #(s ∪ image (fun z => ↑z) s') - #s
t : α
⊢ t ∈ (s ∪ image (fun z => ↑z) s').biUnion t✝ \ s.biUnion t✝ → t ∈ s'.biUnion fun x' => t✝ ↑x' \ s.biUnion t✝

Proof state:
case inr.intro.intro
α : Type v
inst✝ : DecidableEq α
ι : Type u
t✝ : ι → Finset α
s : Finset ι
hus : #s = #(s.biUnion t✝)
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t✝)
s' : Finset ↑(↑s)ᶜ
this✝ : DecidableEq ι
disj : Disjoint s (image (fun z => ↑z) s')
this : #s' = #(s ∪ image (fun z => ↑z) s') - #s
t : α
x' : ↑(↑s)ᶜ
hx' : x' ∈ s'
rat : t ∈ t✝ ↑x'
hs : ∀ (x : ι), ¬(x ∈ s ∧ t ∈ t✝ x)
⊢ ∃ a ∈ s', t ∈ t✝ ↑a ∧ ∀ (x : ι), ¬(x ∈ s ∧ t ∈ t✝ x)

Tactic:
use x', hx', rat, hs

Result:
no goals