-- Mathlib/Combinatorics/SetFamily/LYM.lean
theorem card_mul_le_card_shadow_mul (h𝒜 : (𝒜 : Set (Finset α)).Sized r) :
    #𝒜 * r ≤ #(∂ 𝒜) * (Fintype.card α - r + 1)

Proof state:
case refine_1
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x1 x2 => x1 ⊆ x2 := fun x x_1 => Classical.dec ((fun x1 x2 => x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ 𝒜
⊢ image s.erase s ⊆ bipartiteBelow (fun x1 x2 => x1 ⊆ x2) (∂ 𝒜) s

Tactic:
simp_rw [image_subset_iff, mem_bipartiteBelow]

Result:
case refine_1
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x1 x2 => x1 ⊆ x2 := fun x x_1 => Classical.dec ((fun x1 x2 => x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ 𝒜
⊢ ∀ x ∈ s, s.erase x ∈ ∂ 𝒜 ∧ s.erase x ⊆ s

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x1 x2 => x1 ⊆ x2 := fun x x_1 => Classical.dec ((fun x1 x2 => x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
t : Finset α
ht : t ∈ 𝒜 ∧ s ⊆ t
this : ∅ ∉ 𝒜
⊢ #s + 1 = #t

Tactic:
rw [(sized_shadow_iff this).1 (Set.Sized.shadow h𝒜) ht.1, (Set.Sized.shadow h𝒜) hs]

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x1 x2 => x1 ⊆ x2 := fun x x_1 => Classical.dec ((fun x1 x2 => x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
t : Finset α
ht : t ∈ 𝒜 ∧ s ⊆ t
⊢ ∅ ∉ 𝒜

Tactic:
rw [← mem_coe, h𝒜.empty_mem_iff, coe_eq_singleton]

Result:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x1 x2 => x1 ⊆ x2 := fun x x_1 => Classical.dec ((fun x1 x2 => x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
t : Finset α
ht : t ∈ 𝒜 ∧ s ⊆ t
⊢ ¬𝒜 = {∅}

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
r : ℕ
i : DecidableRel fun x1 x2 => x1 ⊆ x2 := fun x x_1 => Classical.dec ((fun x1 x2 => x1 ⊆ x2) x x_1)
s t : Finset α
h𝒜 : Set.Sized r ↑{∅}
hs : s ∈ ∅
ht : t ∈ {∅} ∧ s ⊆ t
⊢ False

Tactic:
exact not_mem_empty s hs

Result:
no goals

Proof state:
case refine_1
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x1 x2 => x1 ⊆ x2 := fun x x_1 => Classical.dec ((fun x1 x2 => x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ 𝒜
⊢ ∀ x ∈ s, s.erase x ∈ ∂ 𝒜 ∧ s.erase x ⊆ s

Tactic:
exact fun a ha => ⟨erase_mem_shadow hs ha, erase_subset _ _⟩

Result:
no goals

Proof state:
case refine_2
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x1 x2 => x1 ⊆ x2 := fun x x_1 => Classical.dec ((fun x1 x2 => x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
t : Finset α
ht : t ∈ bipartiteAbove (fun x1 x2 => x1 ⊆ x2) 𝒜 s
⊢ t ∈ image (fun a => insert a s) sᶜ

Tactic:
rw [mem_bipartiteAbove] at ht

Result:
case refine_2
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x1 x2 => x1 ⊆ x2 := fun x x_1 => Classical.dec ((fun x1 x2 => x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
t : Finset α
ht : t ∈ 𝒜 ∧ s ⊆ t
⊢ t ∈ image (fun a => insert a s) sᶜ

Proof state:
case refine_2
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x1 x2 => x1 ⊆ x2 := fun x x_1 => Classical.dec ((fun x1 x2 => x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
t : Finset α
ht : t ∈ 𝒜 ∧ s ⊆ t
this : ∅ ∉ 𝒜
h : ∃ a ∉ s, insert a s = t
⊢ t ∈ image (fun a => insert a s) sᶜ

Tactic:
rcases h with ⟨a, ha, rfl⟩

Result:
case refine_2.intro.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x1 x2 => x1 ⊆ x2 := fun x x_1 => Classical.dec ((fun x1 x2 => x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
this : ∅ ∉ 𝒜
a : α
ha : a ∉ s
ht : insert a s ∈ 𝒜 ∧ s ⊆ insert a s
⊢ insert a s ∈ image (fun a => insert a s) sᶜ

Proof state:
case refine_2.intro.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x1 x2 => x1 ⊆ x2 := fun x x_1 => Classical.dec ((fun x1 x2 => x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
this : ∅ ∉ 𝒜
a : α
ha : a ∉ s
ht : insert a s ∈ 𝒜 ∧ s ⊆ insert a s
⊢ insert a s ∈ image (fun a => insert a s) sᶜ

Tactic:
exact mem_image_of_mem _ (mem_compl.2 ha)

Result:
no goals

Proof state:
case refine_2
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x1 x2 => x1 ⊆ x2 := fun x x_1 => Classical.dec ((fun x1 x2 => x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
⊢ #(bipartiteAbove (fun x1 x2 => x1 ⊆ x2) 𝒜 s) ≤ #(image (fun a => insert a s) sᶜ)

Tactic:
refine card_le_card fun t ht => ?_

Result:
case refine_2
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x1 x2 => x1 ⊆ x2 := fun x x_1 => Classical.dec ((fun x1 x2 => x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
t : Finset α
ht : t ∈ bipartiteAbove (fun x1 x2 => x1 ⊆ x2) 𝒜 s
⊢ t ∈ image (fun a => insert a s) sᶜ

Proof state:
case refine_2
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x1 x2 => x1 ⊆ x2 := fun x x_1 => Classical.dec ((fun x1 x2 => x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
⊢ #(bipartiteAbove (fun x1 x2 => x1 ⊆ x2) 𝒜 s) ≤ Fintype.card α - (r - 1)

Tactic:
rw [← (Set.Sized.shadow h𝒜) hs, ← card_compl, ← card_image_of_injOn (insert_inj_on' _)]

Result:
case refine_2
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x1 x2 => x1 ⊆ x2 := fun x x_1 => Classical.dec ((fun x1 x2 => x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
⊢ #(bipartiteAbove (fun x1 x2 => x1 ⊆ x2) 𝒜 s) ≤ #(image (fun a => insert a s) sᶜ)

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
r : ℕ
i : DecidableRel fun x1 x2 => x1 ⊆ x2 := fun x x_1 => Classical.dec ((fun x1 x2 => x1 ⊆ x2) x x_1)
s t : Finset α
h𝒜 : Set.Sized r ↑{∅}
hs : s ∈ ∂ {∅}
ht : t ∈ {∅} ∧ s ⊆ t
⊢ False

Tactic:
rw [shadow_singleton_empty] at hs

Result:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
r : ℕ
i : DecidableRel fun x1 x2 => x1 ⊆ x2 := fun x x_1 => Classical.dec ((fun x1 x2 => x1 ⊆ x2) x x_1)
s t : Finset α
h𝒜 : Set.Sized r ↑{∅}
hs : s ∈ ∅
ht : t ∈ {∅} ∧ s ⊆ t
⊢ False

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x1 x2 => x1 ⊆ x2 := fun x x_1 => Classical.dec ((fun x1 x2 => x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
t : Finset α
ht : t ∈ 𝒜 ∧ s ⊆ t
⊢ ¬𝒜 = {∅}

Tactic:
rintro rfl

Result:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
r : ℕ
i : DecidableRel fun x1 x2 => x1 ⊆ x2 := fun x x_1 => Classical.dec ((fun x1 x2 => x1 ⊆ x2) x x_1)
s t : Finset α
h𝒜 : Set.Sized r ↑{∅}
hs : s ∈ ∂ {∅}
ht : t ∈ {∅} ∧ s ⊆ t
⊢ False

Proof state:
case refine_2
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x1 x2 => x1 ⊆ x2 := fun x x_1 => Classical.dec ((fun x1 x2 => x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
t : Finset α
ht : t ∈ 𝒜 ∧ s ⊆ t
this : ∅ ∉ 𝒜
⊢ t ∈ image (fun a => insert a s) sᶜ

Tactic:
have h := exists_eq_insert_iff.2 ⟨ht.2, by
  rw [(sized_shadow_iff this).1 (Set.Sized.shadow h𝒜) ht.1, (Set.Sized.shadow h𝒜) hs]⟩

Result:
case refine_2
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x1 x2 => x1 ⊆ x2 := fun x x_1 => Classical.dec ((fun x1 x2 => x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ ∂ 𝒜
t : Finset α
ht : t ∈ 𝒜 ∧ s ⊆ t
this : ∅ ∉ 𝒜
h : ∃ a ∉ s, insert a s = t
⊢ t ∈ image (fun a => insert a s) sᶜ