𝕜 : Type ?u.24481
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ : Finset α
m n : ℕ
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
s : Finset α
h₂ : s ∈ 𝒜 # m
h₁ : ∃ t, ((∃ t_1, t_1 ∈ 𝒜 ∧ t ⊆ t_1) ∧ card t = n) ∧ ∃ a, a ∈ t ∧ erase t a = s
⊢ False
𝕜 : Type ?u.24481
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ : Finset α
m n : ℕ
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
s : Finset α
h₁ : s ∈ (∂ ) (falling n 𝒜)
h₂ : s ∈ 𝒜 # m
⊢ False
simp_rw [mem_shadow_iff, mem_falling] at h₁
case intro.intro.intro.intro.intro.intro.intro
𝕜 : Type ?u.24481
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ : Finset α
m n : ℕ
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
s : Finset α
right✝ : card s = n
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
a : α
ha : a ∈ s
h₂ : erase s a ∈ 𝒜 # m
⊢ False
𝕜 : Type ?u.24481
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ : Finset α
m n : ℕ
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
s : Finset α
h₂ : s ∈ 𝒜 # m
h₁ : ∃ t, ((∃ t_1, t_1 ∈ 𝒜 ∧ t ⊆ t_1) ∧ card t = n) ∧ ∃ a, a ∈ t ∧ erase t a = s
⊢ False
obtain ⟨s, ⟨⟨t, ht, hst⟩, _⟩, a, ha, rfl⟩ := h₁
case intro.intro.intro.intro.intro.intro.intro
𝕜 : Type ?u.24481
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ : Finset α
m n : ℕ
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
s : Finset α
right✝ : card s = n
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
a : α
ha : a ∈ s
h₂ : erase s a ∈ 𝒜 # m
⊢ erase s a ≠ t
case intro.intro.intro.intro.intro.intro.intro
𝕜 : Type ?u.24481
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ : Finset α
m n : ℕ
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
s : Finset α
right✝ : card s = n
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
a : α
ha : a ∈ s
h₂ : erase s a ∈ 𝒜 # m
⊢ False
refine' h𝒜 (slice_subset h₂) ht _ ((erase_subset _ _).trans hst)
case intro.intro.intro.intro.intro.intro.intro
𝕜 : Type ?u.24481
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ : Finset α
m n : ℕ
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
s : Finset α
right✝ : card s = n
a : α
ha : a ∈ s
h₂ : erase s a ∈ 𝒜 # m
ht : erase s a ∈ 𝒜
hst : s ⊆ erase s a
⊢ False
case intro.intro.intro.intro.intro.intro.intro
𝕜 : Type ?u.24481
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ : Finset α
m n : ℕ
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
s : Finset α
right✝ : card s = n
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
a : α
ha : a ∈ s
h₂ : erase s a ∈ 𝒜 # m
⊢ erase s a ≠ t
rintro rfl
no goals
case intro.intro.intro.intro.intro.intro.intro
𝕜 : Type ?u.24481
α : Type u_1
inst✝¹ : LinearOrderedField 𝕜
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s✝ : Finset α
m n : ℕ
h𝒜 : IsAntichain (fun x x_1 => x ⊆ x_1) ↑𝒜
s : Finset α
right✝ : card s = n
a : α
ha : a ∈ s
h₂ : erase s a ∈ 𝒜 # m
ht : erase s a ∈ 𝒜
hst : s ⊆ erase s a
⊢ False
exact not_mem_erase _ _ (hst ha)