Theorem: Finset.le_card_upper_inter_lower (LeanCamCombi/Mathlib/Data/Finset/PosDiffs.lean)

State before:
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsUpperSet ↑ℬ
⊢ (𝒜 \₊ ℬ).card ≤ (𝒜 ∩ ℬ).card
Tactic:
refine' (card_le_card _).trans (card_posDiffs_self_le _)
State after:
case refine'_1
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsUpperSet ↑ℬ
⊢ 𝒜 \₊ ℬ ⊆ 𝒜 ∩ ℬ \₊ (𝒜 ∩ ℬ)

case refine'_2
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsUpperSet ↑ℬ
⊢ (↑(𝒜 ∩ ℬ)).OrdConnected

State before:
case refine'_1
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsUpperSet ↑ℬ
⊢ 𝒜 \₊ ℬ ⊆ 𝒜 ∩ ℬ \₊ (𝒜 ∩ ℬ)
Tactic:
simp_rw [subset_iff, mem_posDiffs, mem_inter]
State after:
case refine'_1
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsUpperSet ↑ℬ
⊢ ∀ ⦃x : Finset α⦄,
    (∃ b ∈ 𝒜, ∃ c ∈ ℬ, c ≤ b ∧ b \ c = x) → ∃ b, (b ∈ 𝒜 ∧ b ∈ ℬ) ∧ ∃ c, (c ∈ 𝒜 ∧ c ∈ ℬ) ∧ c ≤ b ∧ b \ c = x

State before:
case refine'_1
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsUpperSet ↑ℬ
⊢ ∀ ⦃x : Finset α⦄,
    (∃ b ∈ 𝒜, ∃ c ∈ ℬ, c ≤ b ∧ b \ c = x) → ∃ b, (b ∈ 𝒜 ∧ b ∈ ℬ) ∧ ∃ c, (c ∈ 𝒜 ∧ c ∈ ℬ) ∧ c ≤ b ∧ b \ c = x
Tactic:
rintro _ ⟨s, hs, t, ht, hts, rfl⟩
State after:
case refine'_1.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsUpperSet ↑ℬ
s : Finset α
hs : s ∈ 𝒜
t : Finset α
ht : t ∈ ℬ
hts : t ≤ s
⊢ ∃ b, (b ∈ 𝒜 ∧ b ∈ ℬ) ∧ ∃ c, (c ∈ 𝒜 ∧ c ∈ ℬ) ∧ c ≤ b ∧ b \ c = s \ t

State before:
case refine'_1.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsUpperSet ↑ℬ
s : Finset α
hs : s ∈ 𝒜
t : Finset α
ht : t ∈ ℬ
hts : t ≤ s
⊢ ∃ b, (b ∈ 𝒜 ∧ b ∈ ℬ) ∧ ∃ c, (c ∈ 𝒜 ∧ c ∈ ℬ) ∧ c ≤ b ∧ b \ c = s \ t
Tactic:
exact ⟨s, ⟨hs, hℬ hts ht⟩, t, ⟨h𝒜 hts hs, ht⟩, hts, rfl⟩
State after:
no goals

State before:
case refine'_2
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsUpperSet ↑ℬ
⊢ (↑(𝒜 ∩ ℬ)).OrdConnected
Tactic:
rw [coe_inter]
State after:
case refine'_2
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsUpperSet ↑ℬ
⊢ (↑𝒜 ∩ ↑ℬ).OrdConnected

State before:
case refine'_2
α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsUpperSet ↑ℬ
⊢ (↑𝒜 ∩ ↑ℬ).OrdConnected
Tactic:
exact h𝒜.ordConnected.inter hℬ.ordConnected
State after:
no goals