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

Tactic:
haveI := Classical.decEq ι

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 ι
⊢ #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 ι
x : ι
hx : x ∈ s
hc : x ∈ (↑s)ᶜ
a✝ : ⟨x, ⋯⟩ ∈ s'
⊢ False

Tactic:
exact absurd hx hc

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

Tactic:
rw [this, hus]

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') - #(s.biUnion t) ≤ #(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')
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✝

Tactic:
simp only [mem_biUnion, mem_sdiff, not_exists, mem_image, and_imp, mem_union, exists_and_right,
  exists_imp]

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 : α
⊢ ∀ (x : ι),
    (x ∈ s ∨ ∃ a ∈ s', ↑a = x) →
      t ∈ t✝ x → (∀ (x : ι), ¬(x ∈ s ∧ t ∈ t✝ x)) → ∃ a ∈ s', t ∈ t✝ ↑a ∧ ∀ (x : ι), ¬(x ∈ s ∧ t ∈ t✝ x)

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 ι
⊢ Disjoint s (image (fun z => ↑z) s')

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

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 ι
⊢ ∀ ⦃a : ι⦄, a ∈ s → ∀ (x : a ∈ (↑s)ᶜ), ⟨a, ⋯⟩ ∉ s'

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

Tactic:
refine (Nat.sub_le_sub_right (ht _) _).trans ?_

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)

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 ι
⊢ ∀ ⦃a : ι⦄, a ∈ s → ∀ (x : a ∈ (↑s)ᶜ), ⟨a, ⋯⟩ ∉ s'

Tactic:
intro x 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 ι
x : ι
hx : x ∈ s
hc : x ∈ (↑s)ᶜ
a✝ : ⟨x, ⋯⟩ ∈ s'
⊢ False

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
t : α
⊢ ∀ (x : ι),
    (x ∈ s ∨ ∃ a ∈ s', ↑a = x) →
      t ∈ t✝ x → (∀ (x : ι), ¬(x ∈ s ∧ t ∈ t✝ x)) → ∃ a ∈ s', t ∈ t✝ ↑a ∧ ∀ (x : ι), ¬(x ∈ s ∧ t ∈ t✝ x)

Tactic:
rintro x (hx | ⟨x', hx', rfl⟩) rat hs

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

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)

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.biUnion t ⊆ (s ∪ image (fun z => ↑z) s').biUnion t

Tactic:
apply biUnion_subset_biUnion_of_subset_left

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

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:
refine (card_le_card ?_).trans le_rfl

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