α : Type u_1
β : Type ?u.160028
s t : Set α
a b x y : α
f : α → β
n : ℕ
h : ncard s = n + 1
hsf : Set.Finite s
⊢ ∃ a t, ¬a ∈ t ∧ insert a t = s ∧ ncard t = n
α : Type u_1
β : Type ?u.160028
s t : Set α
a b x y : α
f : α → β
n : ℕ
h : ncard s = n + 1
⊢ ∃ a t, ¬a ∈ t ∧ insert a t = s ∧ ncard t = n
have hsf := Finite_of_ncard_pos (n.zero_lt_succ.trans_eq h.symm)
α : Type u_1
β : Type ?u.160028
s t : Set α
a b x y : α
f : α → β
n : ℕ
hsf : Set.Finite s
h✝ : Finset.card (Finite.toFinset hsf) = n + 1
h : ∃ a t, ¬a ∈ t ∧ insert a t = Finite.toFinset hsf ∧ Finset.card t = n
⊢ ∃ a t, ¬a ∈ t ∧ insert a t = s ∧ ncard t = n
α : Type u_1
β : Type ?u.160028
s t : Set α
a b x y : α
f : α → β
n : ℕ
h : ncard s = n + 1
hsf : Set.Finite s
⊢ ∃ a t, ¬a ∈ t ∧ insert a t = s ∧ ncard t = n
rw [ncard_eq_toFinset_card _ hsf, Finset.card_eq_succ] at h
case intro.intro.intro.intro
α : Type u_1
β : Type ?u.160028
s t✝ : Set α
a✝ b x y : α
f : α → β
hsf : Set.Finite s
a : α
t : Finset α
hat : ¬a ∈ t
hts : insert a t = Finite.toFinset hsf
h : Finset.card (Finite.toFinset hsf) = Finset.card t + 1
⊢ ∃ a t_1, ¬a ∈ t_1 ∧ insert a t_1 = s ∧ ncard t_1 = Finset.card t
α : Type u_1
β : Type ?u.160028
s t : Set α
a b x y : α
f : α → β
n : ℕ
hsf : Set.Finite s
h✝ : Finset.card (Finite.toFinset hsf) = n + 1
h : ∃ a t, ¬a ∈ t ∧ insert a t = Finite.toFinset hsf ∧ Finset.card t = n
⊢ ∃ a t, ¬a ∈ t ∧ insert a t = s ∧ ncard t = n
obtain ⟨a, t, hat, hts, rfl⟩ := h
case intro.intro.intro.intro
α : Type u_1
β : Type ?u.160028
s t✝ : Set α
a✝ b x y : α
f : α → β
hsf : Set.Finite s
a : α
t : Finset α
hat : ¬a ∈ t
h : Finset.card (Finite.toFinset hsf) = Finset.card t + 1
hts : ∀ (a_1 : α), a_1 = a ∨ a_1 ∈ t ↔ a_1 ∈ s
⊢ ∃ a t_1, ¬a ∈ t_1 ∧ insert a t_1 = s ∧ ncard t_1 = Finset.card t
case intro.intro.intro.intro
α : Type u_1
β : Type ?u.160028
s t✝ : Set α
a✝ b x y : α
f : α → β
hsf : Set.Finite s
a : α
t : Finset α
hat : ¬a ∈ t
hts : insert a t = Finite.toFinset hsf
h : Finset.card (Finite.toFinset hsf) = Finset.card t + 1
⊢ ∃ a t_1, ¬a ∈ t_1 ∧ insert a t_1 = s ∧ ncard t_1 = Finset.card t
simp only [Finset.ext_iff, Finset.mem_insert, Finite.mem_toFinset] at hts
case intro.intro.intro.intro.refine'_1
α : Type u_1
β : Type ?u.160028
s t✝ : Set α
a✝ b x y : α
f : α → β
hsf : Set.Finite s
a : α
t : Finset α
hat : ¬a ∈ t
h : Finset.card (Finite.toFinset hsf) = Finset.card t + 1
hts : ∀ (a_1 : α), a_1 = a ∨ a_1 ∈ t ↔ a_1 ∈ s
⊢ insert a ↑t = s

case intro.intro.intro.intro.refine'_2
α : Type u_1
β : Type ?u.160028
s t✝ : Set α
a✝ b x y : α
f : α → β
hsf : Set.Finite s
a : α
t : Finset α
hat : ¬a ∈ t
h : Finset.card (Finite.toFinset hsf) = Finset.card t + 1
hts : ∀ (a_1 : α), a_1 = a ∨ a_1 ∈ t ↔ a_1 ∈ s
⊢ ncard ↑t = Finset.card t
case intro.intro.intro.intro
α : Type u_1
β : Type ?u.160028
s t✝ : Set α
a✝ b x y : α
f : α → β
hsf : Set.Finite s
a : α
t : Finset α
hat : ¬a ∈ t
h : Finset.card (Finite.toFinset hsf) = Finset.card t + 1
hts : ∀ (a_1 : α), a_1 = a ∨ a_1 ∈ t ↔ a_1 ∈ s
⊢ ∃ a t_1, ¬a ∈ t_1 ∧ insert a t_1 = s ∧ ncard t_1 = Finset.card t
refine' ⟨a, t, hat, _, _⟩
no goals
case intro.intro.intro.intro.refine'_2
α : Type u_1
β : Type ?u.160028
s t✝ : Set α
a✝ b x y : α
f : α → β
hsf : Set.Finite s
a : α
t : Finset α
hat : ¬a ∈ t
h : Finset.card (Finite.toFinset hsf) = Finset.card t + 1
hts : ∀ (a_1 : α), a_1 = a ∨ a_1 ∈ t ↔ a_1 ∈ s
⊢ ncard ↑t = Finset.card t
simp
case intro.intro.intro.intro.refine'_1
α : Type u_1
β : Type ?u.160028
s t✝ : Set α
a✝ b x y : α
f : α → β
hsf : Set.Finite s
a : α
t : Finset α
hat : ¬a ∈ t
h : Finset.card (Finite.toFinset hsf) = Finset.card t + 1
hts : ∀ (a_1 : α), a_1 = a ∨ a_1 ∈ t ↔ a_1 ∈ s
⊢ ∀ (x : α), x = a ∨ x ∈ t ↔ x ∈ s
case intro.intro.intro.intro.refine'_1
α : Type u_1
β : Type ?u.160028
s t✝ : Set α
a✝ b x y : α
f : α → β
hsf : Set.Finite s
a : α
t : Finset α
hat : ¬a ∈ t
h : Finset.card (Finite.toFinset hsf) = Finset.card t + 1
hts : ∀ (a_1 : α), a_1 = a ∨ a_1 ∈ t ↔ a_1 ∈ s
⊢ insert a ↑t = s
simp only [Finset.mem_coe, ext_iff, mem_insert_iff]
no goals
case intro.intro.intro.intro.refine'_1
α : Type u_1
β : Type ?u.160028
s t✝ : Set α
a✝ b x y : α
f : α → β
hsf : Set.Finite s
a : α
t : Finset α
hat : ¬a ∈ t
h : Finset.card (Finite.toFinset hsf) = Finset.card t + 1
hts : ∀ (a_1 : α), a_1 = a ∨ a_1 ∈ t ↔ a_1 ∈ s
⊢ ∀ (x : α), x = a ∨ x ∈ t ↔ x ∈ s
tauto