Theorem: Finset.lovasz_form (LeanCamCombi/KruskalKatona.lean)

State before:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
⊢ k.choose (r - i) ≤ (∂ ^[i] 𝒜).card
Tactic:
set range'k : Finset (Fin n) :=
  attachFin (range k) fun m ↦ by rw [mem_range]; apply forall_lt_iff_le.2 hkn
State after:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
⊢ k.choose (r - i) ≤ (∂ ^[i] 𝒜).card

State before:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
⊢ k.choose (r - i) ≤ (∂ ^[i] 𝒜).card
Tactic:
set 𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
State after:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
⊢ k.choose (r - i) ≤ (∂ ^[i] 𝒜).card

State before:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
⊢ k.choose (r - i) ≤ (∂ ^[i] 𝒜).card
Tactic:
have Ccard : 𝒞.card = k.choose r := by rw [card_powersetCard, card_attachFin, card_range]
State after:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
⊢ k.choose (r - i) ≤ (∂ ^[i] 𝒜).card

State before:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
⊢ k.choose (r - i) ≤ (∂ ^[i] 𝒜).card
Tactic:
have : (𝒞 : Set (Finset (Fin n))).Sized r := Set.sized_powersetCard _ _
State after:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this : Set.Sized r ↑𝒞
⊢ k.choose (r - i) ≤ (∂ ^[i] 𝒜).card

State before:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this : Set.Sized r ↑𝒞
⊢ k.choose (r - i) ≤ (∂ ^[i] 𝒜).card
Tactic:
suffices this : (∂^[i] 𝒞).card = k.choose  (r - i) by
  rw [← this]
  apply iterated_kk h₁ _ _
  rwa [Ccard]
  refine' ⟨‹_›, _⟩
  rintro A B hA ⟨HB₁, HB₂⟩
  rw [mem_powersetCard]
  refine' ⟨fun t ht ↦ _, ‹_›⟩
  rw [mem_attachFin, mem_range]
  have : toColex (image Fin.val B) < toColex (image Fin.val A) := by
    rwa [toColex_image_lt_toColex_image Fin.val_strictMono]
  apply Colex.forall_lt_mono this.le _ t (mem_image.2 ⟨t, ht, rfl⟩)
  simp_rw [mem_image]
  rintro _ ⟨a, ha, q⟩
  rw [mem_powersetCard] at hA
  rw [← q, ← mem_range]
  have := hA.1 ha
  rwa [mem_attachFin] at this
State after:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this : Set.Sized r ↑𝒞
⊢ (∂ ^[i] 𝒞).card = k.choose (r - i)

State before:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this : Set.Sized r ↑𝒞
⊢ (∂ ^[i] 𝒞).card = k.choose (r - i)
Tactic:
suffices ∂^[i] 𝒞 = powersetCard (r - i) range'k by
  rw [this, card_powersetCard, card_attachFin, card_range]
State after:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this : Set.Sized r ↑𝒞
⊢ ∂ ^[i] 𝒞 = powersetCard (r - i) range'k

State before:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this : Set.Sized r ↑𝒞
⊢ ∂ ^[i] 𝒞 = powersetCard (r - i) range'k
Tactic:
ext B
State after:
case a
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this : Set.Sized r ↑𝒞
B : Finset (Fin n)
⊢ B ∈ ∂ ^[i] 𝒞 ↔ B ∈ powersetCard (r - i) range'k

State before:
case a
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this : Set.Sized r ↑𝒞
B : Finset (Fin n)
⊢ B ∈ ∂ ^[i] 𝒞 ↔ B ∈ powersetCard (r - i) range'k
Tactic:
rw [mem_powersetCard, mem_shadow_iterate_iff_exists_sdiff]
State after:
case a
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this : Set.Sized r ↑𝒞
B : Finset (Fin n)
⊢ (∃ s ∈ 𝒞, B ⊆ s ∧ (s \ B).card = i) ↔ B ⊆ range'k ∧ B.card = r - i

State before:
case a
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this : Set.Sized r ↑𝒞
B : Finset (Fin n)
⊢ (∃ s ∈ 𝒞, B ⊆ s ∧ (s \ B).card = i) ↔ B ⊆ range'k ∧ B.card = r - i
Tactic:
constructor
State after:
case a.mp
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this : Set.Sized r ↑𝒞
B : Finset (Fin n)
⊢ (∃ s ∈ 𝒞, B ⊆ s ∧ (s \ B).card = i) → B ⊆ range'k ∧ B.card = r - i

case a.mpr
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this : Set.Sized r ↑𝒞
B : Finset (Fin n)
⊢ B ⊆ range'k ∧ B.card = r - i → ∃ s ∈ 𝒞, B ⊆ s ∧ (s \ B).card = i

State before:
case a.mpr
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this : Set.Sized r ↑𝒞
B : Finset (Fin n)
⊢ B ⊆ range'k ∧ B.card = r - i → ∃ s ∈ 𝒞, B ⊆ s ∧ (s \ B).card = i
Tactic:
rintro ⟨hBk, hB⟩
State after:
case a.mpr.intro
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this : Set.Sized r ↑𝒞
B : Finset (Fin n)
hBk : B ⊆ range'k
hB : B.card = r - i
⊢ ∃ s ∈ 𝒞, B ⊆ s ∧ (s \ B).card = i

State before:
case a.mpr.intro
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this : Set.Sized r ↑𝒞
B : Finset (Fin n)
hBk : B ⊆ range'k
hB : B.card = r - i
⊢ ∃ s ∈ 𝒞, B ⊆ s ∧ (s \ B).card = i
Tactic:
have := exists_intermediate_set i ?_ hBk
State after:
case a.mpr.intro.refine_2
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this✝ : Set.Sized r ↑𝒞
B : Finset (Fin n)
hBk : B ⊆ range'k
hB : B.card = r - i
this : ∃ C, B ⊆ C ∧ C ⊆ range'k ∧ C.card = i + B.card
⊢ ∃ s ∈ 𝒞, B ⊆ s ∧ (s \ B).card = i

case a.mpr.intro.refine_1
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this : Set.Sized r ↑𝒞
B : Finset (Fin n)
hBk : B ⊆ range'k
hB : B.card = r - i
⊢ i + B.card ≤ range'k.card

State before:
case a.mpr.intro.refine_2
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this✝ : Set.Sized r ↑𝒞
B : Finset (Fin n)
hBk : B ⊆ range'k
hB : B.card = r - i
this : ∃ C, B ⊆ C ∧ C ⊆ range'k ∧ C.card = i + B.card
⊢ ∃ s ∈ 𝒞, B ⊆ s ∧ (s \ B).card = i

case a.mpr.intro.refine_1
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this : Set.Sized r ↑𝒞
B : Finset (Fin n)
hBk : B ⊆ range'k
hB : B.card = r - i
⊢ i + B.card ≤ range'k.card
Tactic:
obtain ⟨C, BsubC, hCrange, hcard⟩ := this
State after:
case a.mpr.intro.refine_2.intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this : Set.Sized r ↑𝒞
B : Finset (Fin n)
hBk : B ⊆ range'k
hB : B.card = r - i
C : Finset (Fin n)
BsubC : B ⊆ C
hCrange : C ⊆ range'k
hcard : C.card = i + B.card
⊢ ∃ s ∈ 𝒞, B ⊆ s ∧ (s \ B).card = i

case a.mpr.intro.refine_1
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this : Set.Sized r ↑𝒞
B : Finset (Fin n)
hBk : B ⊆ range'k
hB : B.card = r - i
⊢ i + B.card ≤ range'k.card

State before:
case a.mpr.intro.refine_2.intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this : Set.Sized r ↑𝒞
B : Finset (Fin n)
hBk : B ⊆ range'k
hB : B.card = r - i
C : Finset (Fin n)
BsubC : B ⊆ C
hCrange : C ⊆ range'k
hcard : C.card = i + B.card
⊢ ∃ s ∈ 𝒞, B ⊆ s ∧ (s \ B).card = i

case a.mpr.intro.refine_1
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this : Set.Sized r ↑𝒞
B : Finset (Fin n)
hBk : B ⊆ range'k
hB : B.card = r - i
⊢ i + B.card ≤ range'k.card
Tactic:
rw [hB, ← Nat.add_sub_assoc hir, Nat.add_sub_cancel_left] at hcard
State after:
case a.mpr.intro.refine_2.intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this : Set.Sized r ↑𝒞
B : Finset (Fin n)
hBk : B ⊆ range'k
hB : B.card = r - i
C : Finset (Fin n)
BsubC : B ⊆ C
hCrange : C ⊆ range'k
hcard : C.card = r
⊢ ∃ s ∈ 𝒞, B ⊆ s ∧ (s \ B).card = i

case a.mpr.intro.refine_1
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this : Set.Sized r ↑𝒞
B : Finset (Fin n)
hBk : B ⊆ range'k
hB : B.card = r - i
⊢ i + B.card ≤ range'k.card

State before:
case a.mpr.intro.refine_2.intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this : Set.Sized r ↑𝒞
B : Finset (Fin n)
hBk : B ⊆ range'k
hB : B.card = r - i
C : Finset (Fin n)
BsubC : B ⊆ C
hCrange : C ⊆ range'k
hcard : C.card = r
⊢ ∃ s ∈ 𝒞, B ⊆ s ∧ (s \ B).card = i

case a.mpr.intro.refine_1
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this : Set.Sized r ↑𝒞
B : Finset (Fin n)
hBk : B ⊆ range'k
hB : B.card = r - i
⊢ i + B.card ≤ range'k.card
Tactic:
refine' ⟨C, _, BsubC, _⟩
State after:
case a.mpr.intro.refine_2.intro.intro.intro.refine'_1
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this : Set.Sized r ↑𝒞
B : Finset (Fin n)
hBk : B ⊆ range'k
hB : B.card = r - i
C : Finset (Fin n)
BsubC : B ⊆ C
hCrange : C ⊆ range'k
hcard : C.card = r
⊢ C ∈ 𝒞

case a.mpr.intro.refine_2.intro.intro.intro.refine'_2
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this : Set.Sized r ↑𝒞
B : Finset (Fin n)
hBk : B ⊆ range'k
hB : B.card = r - i
C : Finset (Fin n)
BsubC : B ⊆ C
hCrange : C ⊆ range'k
hcard : C.card = r
⊢ (C \ B).card = i

case a.mpr.intro.refine_1
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this : Set.Sized r ↑𝒞
B : Finset (Fin n)
hBk : B ⊆ range'k
hB : B.card = r - i
⊢ i + B.card ≤ range'k.card

State before:
case a.mpr.intro.refine_2.intro.intro.intro.refine'_1
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this : Set.Sized r ↑𝒞
B : Finset (Fin n)
hBk : B ⊆ range'k
hB : B.card = r - i
C : Finset (Fin n)
BsubC : B ⊆ C
hCrange : C ⊆ range'k
hcard : C.card = r
⊢ C ∈ 𝒞

case a.mpr.intro.refine_2.intro.intro.intro.refine'_2
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this : Set.Sized r ↑𝒞
B : Finset (Fin n)
hBk : B ⊆ range'k
hB : B.card = r - i
C : Finset (Fin n)
BsubC : B ⊆ C
hCrange : C ⊆ range'k
hcard : C.card = r
⊢ (C \ B).card = i

case a.mpr.intro.refine_1
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this : Set.Sized r ↑𝒞
B : Finset (Fin n)
hBk : B ⊆ range'k
hB : B.card = r - i
⊢ i + B.card ≤ range'k.card
Tactic:
rw [mem_powersetCard]
State after:
case a.mpr.intro.refine_2.intro.intro.intro.refine'_1
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this : Set.Sized r ↑𝒞
B : Finset (Fin n)
hBk : B ⊆ range'k
hB : B.card = r - i
C : Finset (Fin n)
BsubC : B ⊆ C
hCrange : C ⊆ range'k
hcard : C.card = r
⊢ C ⊆ range'k ∧ C.card = r

case a.mpr.intro.refine_2.intro.intro.intro.refine'_2
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this : Set.Sized r ↑𝒞
B : Finset (Fin n)
hBk : B ⊆ range'k
hB : B.card = r - i
C : Finset (Fin n)
BsubC : B ⊆ C
hCrange : C ⊆ range'k
hcard : C.card = r
⊢ (C \ B).card = i

case a.mpr.intro.refine_1
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this : Set.Sized r ↑𝒞
B : Finset (Fin n)
hBk : B ⊆ range'k
hB : B.card = r - i
⊢ i + B.card ≤ range'k.card

State before:
case a.mpr.intro.refine_2.intro.intro.intro.refine'_1
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this : Set.Sized r ↑𝒞
B : Finset (Fin n)
hBk : B ⊆ range'k
hB : B.card = r - i
C : Finset (Fin n)
BsubC : B ⊆ C
hCrange : C ⊆ range'k
hcard : C.card = r
⊢ C ⊆ range'k ∧ C.card = r

case a.mpr.intro.refine_2.intro.intro.intro.refine'_2
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this : Set.Sized r ↑𝒞
B : Finset (Fin n)
hBk : B ⊆ range'k
hB : B.card = r - i
C : Finset (Fin n)
BsubC : B ⊆ C
hCrange : C ⊆ range'k
hcard : C.card = r
⊢ (C \ B).card = i

case a.mpr.intro.refine_1
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this : Set.Sized r ↑𝒞
B : Finset (Fin n)
hBk : B ⊆ range'k
hB : B.card = r - i
⊢ i + B.card ≤ range'k.card
Tactic:
exact ⟨hCrange, hcard⟩
State after:
case a.mpr.intro.refine_2.intro.intro.intro.refine'_2
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this : Set.Sized r ↑𝒞
B : Finset (Fin n)
hBk : B ⊆ range'k
hB : B.card = r - i
C : Finset (Fin n)
BsubC : B ⊆ C
hCrange : C ⊆ range'k
hcard : C.card = r
⊢ (C \ B).card = i

case a.mpr.intro.refine_1
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this : Set.Sized r ↑𝒞
B : Finset (Fin n)
hBk : B ⊆ range'k
hB : B.card = r - i
⊢ i + B.card ≤ range'k.card

State before:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
m : ℕ
⊢ m ∈ range k → m < n
Tactic:
rw [mem_range]
State after:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
m : ℕ
⊢ m < k → m < n

State before:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
m : ℕ
⊢ m < k → m < n
Tactic:
apply forall_lt_iff_le.2 hkn
State after:
no goals

State before:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
⊢ 𝒞.card = k.choose r
Tactic:
rw [card_powersetCard, card_attachFin, card_range]
State after:
no goals

State before:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this✝ : Set.Sized r ↑𝒞
this : (∂ ^[i] 𝒞).card = k.choose (r - i)
⊢ k.choose (r - i) ≤ (∂ ^[i] 𝒜).card
Tactic:
rw [← this]
State after:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this✝ : Set.Sized r ↑𝒞
this : (∂ ^[i] 𝒞).card = k.choose (r - i)
⊢ (∂ ^[i] 𝒞).card ≤ (∂ ^[i] 𝒜).card

State before:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this✝ : Set.Sized r ↑𝒞
this : (∂ ^[i] 𝒞).card = k.choose (r - i)
⊢ (∂ ^[i] 𝒞).card ≤ (∂ ^[i] 𝒜).card
Tactic:
apply iterated_kk h₁ _ _
State after:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this✝ : Set.Sized r ↑𝒞
this : (∂ ^[i] 𝒞).card = k.choose (r - i)
⊢ 𝒞.card ≤ 𝒜.card

α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this✝ : Set.Sized r ↑𝒞
this : (∂ ^[i] 𝒞).card = k.choose (r - i)
⊢ IsInitSeg 𝒞 r

State before:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this✝ : Set.Sized r ↑𝒞
this : (∂ ^[i] 𝒞).card = k.choose (r - i)
⊢ 𝒞.card ≤ 𝒜.card

α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this✝ : Set.Sized r ↑𝒞
this : (∂ ^[i] 𝒞).card = k.choose (r - i)
⊢ IsInitSeg 𝒞 r
Tactic:
rwa [Ccard]
State after:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this✝ : Set.Sized r ↑𝒞
this : (∂ ^[i] 𝒞).card = k.choose (r - i)
⊢ IsInitSeg 𝒞 r

State before:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this✝ : Set.Sized r ↑𝒞
this : (∂ ^[i] 𝒞).card = k.choose (r - i)
⊢ IsInitSeg 𝒞 r
Tactic:
refine' ⟨‹_›, _⟩
State after:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this✝ : Set.Sized r ↑𝒞
this : (∂ ^[i] 𝒞).card = k.choose (r - i)
⊢ ∀ ⦃s t : Finset (Fin n)⦄, s ∈ 𝒞 → { ofColex := t } < { ofColex := s } ∧ t.card = r → t ∈ 𝒞

State before:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this✝ : Set.Sized r ↑𝒞
this : (∂ ^[i] 𝒞).card = k.choose (r - i)
⊢ ∀ ⦃s t : Finset (Fin n)⦄, s ∈ 𝒞 → { ofColex := t } < { ofColex := s } ∧ t.card = r → t ∈ 𝒞
Tactic:
rintro A B hA ⟨HB₁, HB₂⟩
State after:
case intro
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this✝ : Set.Sized r ↑𝒞
this : (∂ ^[i] 𝒞).card = k.choose (r - i)
A B : Finset (Fin n)
hA : A ∈ 𝒞
HB₁ : { ofColex := B } < { ofColex := A }
HB₂ : B.card = r
⊢ B ∈ 𝒞

State before:
case intro
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this✝ : Set.Sized r ↑𝒞
this : (∂ ^[i] 𝒞).card = k.choose (r - i)
A B : Finset (Fin n)
hA : A ∈ 𝒞
HB₁ : { ofColex := B } < { ofColex := A }
HB₂ : B.card = r
⊢ B ∈ 𝒞
Tactic:
rw [mem_powersetCard]
State after:
case intro
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this✝ : Set.Sized r ↑𝒞
this : (∂ ^[i] 𝒞).card = k.choose (r - i)
A B : Finset (Fin n)
hA : A ∈ 𝒞
HB₁ : { ofColex := B } < { ofColex := A }
HB₂ : B.card = r
⊢ B ⊆ range'k ∧ B.card = r

State before:
case intro
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this✝ : Set.Sized r ↑𝒞
this : (∂ ^[i] 𝒞).card = k.choose (r - i)
A B : Finset (Fin n)
hA : A ∈ 𝒞
HB₁ : { ofColex := B } < { ofColex := A }
HB₂ : B.card = r
⊢ B ⊆ range'k ∧ B.card = r
Tactic:
refine' ⟨fun t ht ↦ _, ‹_›⟩
State after:
case intro
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this✝ : Set.Sized r ↑𝒞
this : (∂ ^[i] 𝒞).card = k.choose (r - i)
A B : Finset (Fin n)
hA : A ∈ 𝒞
HB₁ : { ofColex := B } < { ofColex := A }
HB₂ : B.card = r
t : Fin n
ht : t ∈ B
⊢ t ∈ range'k

State before:
case intro
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this✝ : Set.Sized r ↑𝒞
this : (∂ ^[i] 𝒞).card = k.choose (r - i)
A B : Finset (Fin n)
hA : A ∈ 𝒞
HB₁ : { ofColex := B } < { ofColex := A }
HB₂ : B.card = r
t : Fin n
ht : t ∈ B
⊢ t ∈ range'k
Tactic:
rw [mem_attachFin, mem_range]
State after:
case intro
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this✝ : Set.Sized r ↑𝒞
this : (∂ ^[i] 𝒞).card = k.choose (r - i)
A B : Finset (Fin n)
hA : A ∈ 𝒞
HB₁ : { ofColex := B } < { ofColex := A }
HB₂ : B.card = r
t : Fin n
ht : t ∈ B
⊢ ↑t < k

State before:
case intro
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this✝ : Set.Sized r ↑𝒞
this : (∂ ^[i] 𝒞).card = k.choose (r - i)
A B : Finset (Fin n)
hA : A ∈ 𝒞
HB₁ : { ofColex := B } < { ofColex := A }
HB₂ : B.card = r
t : Fin n
ht : t ∈ B
⊢ ↑t < k
Tactic:
have : toColex (image Fin.val B) < toColex (image Fin.val A) := by
  rwa [toColex_image_lt_toColex_image Fin.val_strictMono]
State after:
case intro
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this✝¹ : Set.Sized r ↑𝒞
this✝ : (∂ ^[i] 𝒞).card = k.choose (r - i)
A B : Finset (Fin n)
hA : A ∈ 𝒞
HB₁ : { ofColex := B } < { ofColex := A }
HB₂ : B.card = r
t : Fin n
ht : t ∈ B
this : { ofColex := image Fin.val B } < { ofColex := image Fin.val A }
⊢ ↑t < k

State before:
case intro
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this✝¹ : Set.Sized r ↑𝒞
this✝ : (∂ ^[i] 𝒞).card = k.choose (r - i)
A B : Finset (Fin n)
hA : A ∈ 𝒞
HB₁ : { ofColex := B } < { ofColex := A }
HB₂ : B.card = r
t : Fin n
ht : t ∈ B
this : { ofColex := image Fin.val B } < { ofColex := image Fin.val A }
⊢ ↑t < k
Tactic:
apply Colex.forall_lt_mono this.le _ t (mem_image.2 ⟨t, ht, rfl⟩)
State after:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this✝¹ : Set.Sized r ↑𝒞
this✝ : (∂ ^[i] 𝒞).card = k.choose (r - i)
A B : Finset (Fin n)
hA : A ∈ 𝒞
HB₁ : { ofColex := B } < { ofColex := A }
HB₂ : B.card = r
t : Fin n
ht : t ∈ B
this : { ofColex := image Fin.val B } < { ofColex := image Fin.val A }
⊢ ∀ b ∈ image Fin.val A, b < k

State before:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this✝¹ : Set.Sized r ↑𝒞
this✝ : (∂ ^[i] 𝒞).card = k.choose (r - i)
A B : Finset (Fin n)
hA : A ∈ 𝒞
HB₁ : { ofColex := B } < { ofColex := A }
HB₂ : B.card = r
t : Fin n
ht : t ∈ B
this : { ofColex := image Fin.val B } < { ofColex := image Fin.val A }
⊢ ∀ b ∈ image Fin.val A, b < k
Tactic:
simp_rw [mem_image]
State after:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this✝¹ : Set.Sized r ↑𝒞
this✝ : (∂ ^[i] 𝒞).card = k.choose (r - i)
A B : Finset (Fin n)
hA : A ∈ 𝒞
HB₁ : { ofColex := B } < { ofColex := A }
HB₂ : B.card = r
t : Fin n
ht : t ∈ B
this : { ofColex := image Fin.val B } < { ofColex := image Fin.val A }
⊢ ∀ (b : ℕ), (∃ a ∈ A, ↑a = b) → b < k

State before:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this✝¹ : Set.Sized r ↑𝒞
this✝ : (∂ ^[i] 𝒞).card = k.choose (r - i)
A B : Finset (Fin n)
hA : A ∈ 𝒞
HB₁ : { ofColex := B } < { ofColex := A }
HB₂ : B.card = r
t : Fin n
ht : t ∈ B
this : { ofColex := image Fin.val B } < { ofColex := image Fin.val A }
⊢ ∀ (b : ℕ), (∃ a ∈ A, ↑a = b) → b < k
Tactic:
rintro _ ⟨a, ha, q⟩
State after:
case intro.intro
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this✝¹ : Set.Sized r ↑𝒞
this✝ : (∂ ^[i] 𝒞).card = k.choose (r - i)
A B : Finset (Fin n)
hA : A ∈ 𝒞
HB₁ : { ofColex := B } < { ofColex := A }
HB₂ : B.card = r
t : Fin n
ht : t ∈ B
this : { ofColex := image Fin.val B } < { ofColex := image Fin.val A }
b✝ : ℕ
a : Fin n
ha : a ∈ A
q : ↑a = b✝
⊢ b✝ < k

State before:
case intro.intro
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this✝¹ : Set.Sized r ↑𝒞
this✝ : (∂ ^[i] 𝒞).card = k.choose (r - i)
A B : Finset (Fin n)
hA : A ∈ 𝒞
HB₁ : { ofColex := B } < { ofColex := A }
HB₂ : B.card = r
t : Fin n
ht : t ∈ B
this : { ofColex := image Fin.val B } < { ofColex := image Fin.val A }
b✝ : ℕ
a : Fin n
ha : a ∈ A
q : ↑a = b✝
⊢ b✝ < k
Tactic:
rw [mem_powersetCard] at hA
State after:
case intro.intro
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this✝¹ : Set.Sized r ↑𝒞
this✝ : (∂ ^[i] 𝒞).card = k.choose (r - i)
A B : Finset (Fin n)
hA : A ⊆ range'k ∧ A.card = r
HB₁ : { ofColex := B } < { ofColex := A }
HB₂ : B.card = r
t : Fin n
ht : t ∈ B
this : { ofColex := image Fin.val B } < { ofColex := image Fin.val A }
b✝ : ℕ
a : Fin n
ha : a ∈ A
q : ↑a = b✝
⊢ b✝ < k

State before:
case intro.intro
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this✝¹ : Set.Sized r ↑𝒞
this✝ : (∂ ^[i] 𝒞).card = k.choose (r - i)
A B : Finset (Fin n)
hA : A ⊆ range'k ∧ A.card = r
HB₁ : { ofColex := B } < { ofColex := A }
HB₂ : B.card = r
t : Fin n
ht : t ∈ B
this : { ofColex := image Fin.val B } < { ofColex := image Fin.val A }
b✝ : ℕ
a : Fin n
ha : a ∈ A
q : ↑a = b✝
⊢ b✝ < k
Tactic:
rw [← q, ← mem_range]
State after:
case intro.intro
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this✝¹ : Set.Sized r ↑𝒞
this✝ : (∂ ^[i] 𝒞).card = k.choose (r - i)
A B : Finset (Fin n)
hA : A ⊆ range'k ∧ A.card = r
HB₁ : { ofColex := B } < { ofColex := A }
HB₂ : B.card = r
t : Fin n
ht : t ∈ B
this : { ofColex := image Fin.val B } < { ofColex := image Fin.val A }
b✝ : ℕ
a : Fin n
ha : a ∈ A
q : ↑a = b✝
⊢ ↑a ∈ range k

State before:
case intro.intro
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this✝¹ : Set.Sized r ↑𝒞
this✝ : (∂ ^[i] 𝒞).card = k.choose (r - i)
A B : Finset (Fin n)
hA : A ⊆ range'k ∧ A.card = r
HB₁ : { ofColex := B } < { ofColex := A }
HB₂ : B.card = r
t : Fin n
ht : t ∈ B
this : { ofColex := image Fin.val B } < { ofColex := image Fin.val A }
b✝ : ℕ
a : Fin n
ha : a ∈ A
q : ↑a = b✝
⊢ ↑a ∈ range k
Tactic:
have := hA.1 ha
State after:
case intro.intro
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this✝² : Set.Sized r ↑𝒞
this✝¹ : (∂ ^[i] 𝒞).card = k.choose (r - i)
A B : Finset (Fin n)
hA : A ⊆ range'k ∧ A.card = r
HB₁ : { ofColex := B } < { ofColex := A }
HB₂ : B.card = r
t : Fin n
ht : t ∈ B
this✝ : { ofColex := image Fin.val B } < { ofColex := image Fin.val A }
b✝ : ℕ
a : Fin n
ha : a ∈ A
q : ↑a = b✝
this : a ∈ range'k
⊢ ↑a ∈ range k

State before:
case intro.intro
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this✝² : Set.Sized r ↑𝒞
this✝¹ : (∂ ^[i] 𝒞).card = k.choose (r - i)
A B : Finset (Fin n)
hA : A ⊆ range'k ∧ A.card = r
HB₁ : { ofColex := B } < { ofColex := A }
HB₂ : B.card = r
t : Fin n
ht : t ∈ B
this✝ : { ofColex := image Fin.val B } < { ofColex := image Fin.val A }
b✝ : ℕ
a : Fin n
ha : a ∈ A
q : ↑a = b✝
this : a ∈ range'k
⊢ ↑a ∈ range k
Tactic:
rwa [mem_attachFin] at this
State after:
no goals

State before:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this✝ : Set.Sized r ↑𝒞
this : (∂ ^[i] 𝒞).card = k.choose (r - i)
A B : Finset (Fin n)
hA : A ∈ 𝒞
HB₁ : { ofColex := B } < { ofColex := A }
HB₂ : B.card = r
t : Fin n
ht : t ∈ B
⊢ { ofColex := image Fin.val B } < { ofColex := image Fin.val A }
Tactic:
rwa [toColex_image_lt_toColex_image Fin.val_strictMono]
State after:
no goals

State before:
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this✝ : Set.Sized r ↑𝒞
this : ∂ ^[i] 𝒞 = powersetCard (r - i) range'k
⊢ (∂ ^[i] 𝒞).card = k.choose (r - i)
Tactic:
rw [this, card_powersetCard, card_attachFin, card_range]
State after:
no goals

State before:
case a.mp
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this : Set.Sized r ↑𝒞
B : Finset (Fin n)
⊢ (∃ s ∈ 𝒞, B ⊆ s ∧ (s \ B).card = i) → B ⊆ range'k ∧ B.card = r - i
Tactic:
rintro ⟨A, Ah, BsubA, card_sdiff_i⟩
State after:
case a.mp.intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this : Set.Sized r ↑𝒞
B A : Finset (Fin n)
Ah : A ∈ 𝒞
BsubA : B ⊆ A
card_sdiff_i : (A \ B).card = i
⊢ B ⊆ range'k ∧ B.card = r - i

State before:
case a.mp.intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this : Set.Sized r ↑𝒞
B A : Finset (Fin n)
Ah : A ∈ 𝒞
BsubA : B ⊆ A
card_sdiff_i : (A \ B).card = i
⊢ B ⊆ range'k ∧ B.card = r - i
Tactic:
rw [mem_powersetCard] at Ah
State after:
case a.mp.intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this : Set.Sized r ↑𝒞
B A : Finset (Fin n)
Ah : A ⊆ range'k ∧ A.card = r
BsubA : B ⊆ A
card_sdiff_i : (A \ B).card = i
⊢ B ⊆ range'k ∧ B.card = r - i

State before:
case a.mp.intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this : Set.Sized r ↑𝒞
B A : Finset (Fin n)
Ah : A ⊆ range'k ∧ A.card = r
BsubA : B ⊆ A
card_sdiff_i : (A \ B).card = i
⊢ B ⊆ range'k ∧ B.card = r - i
Tactic:
refine' ⟨BsubA.trans Ah.1, _⟩
State after:
case a.mp.intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this : Set.Sized r ↑𝒞
B A : Finset (Fin n)
Ah : A ⊆ range'k ∧ A.card = r
BsubA : B ⊆ A
card_sdiff_i : (A \ B).card = i
⊢ B.card = r - i

State before:
case a.mp.intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this : Set.Sized r ↑𝒞
B A : Finset (Fin n)
Ah : A ⊆ range'k ∧ A.card = r
BsubA : B ⊆ A
card_sdiff_i : (A \ B).card = i
⊢ B.card = r - i
Tactic:
symm
State after:
case a.mp.intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this : Set.Sized r ↑𝒞
B A : Finset (Fin n)
Ah : A ⊆ range'k ∧ A.card = r
BsubA : B ⊆ A
card_sdiff_i : (A \ B).card = i
⊢ r - i = B.card

State before:
case a.mp.intro.intro.intro
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this : Set.Sized r ↑𝒞
B A : Finset (Fin n)
Ah : A ⊆ range'k ∧ A.card = r
BsubA : B ⊆ A
card_sdiff_i : (A \ B).card = i
⊢ r - i = B.card
Tactic:
rw [Nat.sub_eq_iff_eq_add hir, ← Ah.2, ← card_sdiff_i, ← card_union_of_disjoint disjoint_sdiff,
  union_sdiff_of_subset BsubA]
State after:
no goals

State before:
case a.mpr.intro.refine_2.intro.intro.intro.refine'_2
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this : Set.Sized r ↑𝒞
B : Finset (Fin n)
hBk : B ⊆ range'k
hB : B.card = r - i
C : Finset (Fin n)
BsubC : B ⊆ C
hCrange : C ⊆ range'k
hcard : C.card = r
⊢ (C \ B).card = i
Tactic:
rw [card_sdiff BsubC, hcard, hB, Nat.sub_sub_self hir]
State after:
no goals

State before:
case a.mpr.intro.refine_1
α : Type u_1
inst✝ : LinearOrder α
s U V : Finset α
n r k i : ℕ
𝒜 𝒞✝ : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ 𝒜.card
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
Ccard : 𝒞.card = k.choose r
this : Set.Sized r ↑𝒞
B : Finset (Fin n)
hBk : B ⊆ range'k
hB : B.card = r - i
⊢ i + B.card ≤ range'k.card
Tactic:
rwa [hB, card_attachFin, card_range, ← Nat.add_sub_assoc hir, Nat.add_sub_cancel_left]
State after:
no goals