case mp
α : Type u_1
β : Type ?u.47438
s✝ t✝ : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
s t : Finset α
⊢ (∃ a x, insert a s = t) → s ⊆ t ∧ card s + 1 = card t

case mpr
α : Type u_1
β : Type ?u.47438
s✝ t✝ : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
s t : Finset α
⊢ s ⊆ t ∧ card s + 1 = card t → ∃ a x, insert a s = t
α : Type u_1
β : Type ?u.47438
s✝ t✝ : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
s t : Finset α
⊢ (∃ a x, insert a s = t) ↔ s ⊆ t ∧ card s + 1 = card t
constructor
case mp.intro.intro
α : Type u_1
β : Type ?u.47438
s✝ t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
s : Finset α
a : α
ha : ¬a ∈ s
⊢ s ⊆ insert a s ∧ card s + 1 = card (insert a s)
case mp
α : Type u_1
β : Type ?u.47438
s✝ t✝ : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
s t : Finset α
⊢ (∃ a x, insert a s = t) → s ⊆ t ∧ card s + 1 = card t
rintro ⟨a, ha, rfl⟩
no goals
case mp.intro.intro
α : Type u_1
β : Type ?u.47438
s✝ t : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
s : Finset α
a : α
ha : ¬a ∈ s
⊢ s ⊆ insert a s ∧ card s + 1 = card (insert a s)
exact ⟨subset_insert _ _, (card_insert_of_not_mem ha).symm⟩
case mpr.intro
α : Type u_1
β : Type ?u.47438
s✝ t✝ : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
s t : Finset α
hst : s ⊆ t
h : card s + 1 = card t
⊢ ∃ a x, insert a s = t
case mpr
α : Type u_1
β : Type ?u.47438
s✝ t✝ : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
s t : Finset α
⊢ s ⊆ t ∧ card s + 1 = card t → ∃ a x, insert a s = t
rintro ⟨hst, h⟩
case mpr.intro.intro
α : Type u_1
β : Type ?u.47438
s✝ t✝ : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
s t : Finset α
hst : s ⊆ t
h : card s + 1 = card t
a : α
ha : t \ s = {a}
⊢ ∃ a x, insert a s = t
case mpr.intro
α : Type u_1
β : Type ?u.47438
s✝ t✝ : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
s t : Finset α
hst : s ⊆ t
h : card s + 1 = card t
⊢ ∃ a x, insert a s = t
obtain ⟨a, ha⟩ : ∃ a, t \ s = {a} :=
  card_eq_one.1 (by rw [card_sdiff hst, ← h, add_tsub_cancel_left])
case mpr.intro.intro
α : Type u_1
β : Type ?u.47438
s✝ t✝ : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
s t : Finset α
hst : s ⊆ t
h : card s + 1 = card t
a : α
ha : t \ s = {a}
hs : a ∈ s
⊢ ¬a ∈ {a}
case mpr.intro.intro
α : Type u_1
β : Type ?u.47438
s✝ t✝ : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
s t : Finset α
hst : s ⊆ t
h : card s + 1 = card t
a : α
ha : t \ s = {a}
⊢ ∃ a x, insert a s = t
refine'
  ⟨a, fun hs => (_ : a ∉ {a}) <| mem_singleton_self _, by
    rw [insert_eq, ← ha, sdiff_union_of_subset hst]⟩
case mpr.intro.intro
α : Type u_1
β : Type ?u.47438
s✝ t✝ : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
s t : Finset α
hst : s ⊆ t
h : card s + 1 = card t
a : α
ha : t \ s = {a}
hs : a ∈ s
⊢ ¬a ∈ t \ s
case mpr.intro.intro
α : Type u_1
β : Type ?u.47438
s✝ t✝ : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
s t : Finset α
hst : s ⊆ t
h : card s + 1 = card t
a : α
ha : t \ s = {a}
hs : a ∈ s
⊢ ¬a ∈ {a}
rw [← ha]
no goals
case mpr.intro.intro
α : Type u_1
β : Type ?u.47438
s✝ t✝ : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
s t : Finset α
hst : s ⊆ t
h : card s + 1 = card t
a : α
ha : t \ s = {a}
hs : a ∈ s
⊢ ¬a ∈ t \ s
exact not_mem_sdiff_of_mem_right hs
no goals
α : Type u_1
β : Type ?u.47438
s✝ t✝ : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
s t : Finset α
hst : s ⊆ t
h : card s + 1 = card t
⊢ card (t \ s) = 1
rw [card_sdiff hst, ← h, add_tsub_cancel_left]
no goals
α : Type u_1
β : Type ?u.47438
s✝ t✝ : Finset α
f : α → β
n : ℕ
inst✝ : DecidableEq α
s t : Finset α
hst : s ⊆ t
h : card s + 1 = card t
a : α
ha : t \ s = {a}
⊢ insert a s = t
rw [insert_eq, ← ha, sdiff_union_of_subset hst]