-- Mathlib/Data/Set/Card.lean
theorem exists_eq_insert_iff_ncard (hs : s.Finite

Proof state:
α : Type u_1
s t : Set α
hs : autoParam s.Finite _auto✝
⊢ (∃ a ∉ s, insert a s = t) ↔ s ⊆ t ∧ s.ncard + 1 = t.ncard

Tactic:
rcases t.finite_or_infinite with ht | ht

Result:
case inl
α : Type u_1
s t : Set α
hs : autoParam s.Finite _auto✝
ht : t.Finite
⊢ (∃ a ∉ s, insert a s = t) ↔ s ⊆ t ∧ s.ncard + 1 = t.ncard

case inr
α : Type u_1
s t : Set α
hs : autoParam s.Finite _auto✝
ht : t.Infinite
⊢ (∃ a ∉ s, insert a s = t) ↔ s ⊆ t ∧ s.ncard + 1 = t.ncard

Proof state:
case inl
α : Type u_1
s t : Set α
hs : autoParam s.Finite _auto✝
ht : t.Finite
⊢ (∃ a ∉ s, insert a s = t) ↔ ∃ a ∉ Finite.toFinset hs, insert a (Finite.toFinset hs) = ht.toFinset

Tactic:
convert Iff.rfl using 2

Result:
case h.e'_2.h.e'_2
α : Type u_1
s t : Set α
hs : autoParam s.Finite _auto✝
ht : t.Finite
⊢ (fun a => a ∉ Finite.toFinset hs ∧ insert a (Finite.toFinset hs) = ht.toFinset) = fun a => a ∉ s ∧ insert a s = t

Proof state:
case inr
α : Type u_1
s t : Set α
hs : autoParam s.Finite _auto✝
ht : t.Infinite
⊢ ∀ x ∉ s, ¬insert x s = t

Tactic:
rintro x - rfl

Result:
case inr
α : Type u_1
s : Set α
hs : autoParam s.Finite _auto✝
x : α
ht : (insert x s).Infinite
⊢ False

Proof state:
case inr
α : Type u_1
s : Set α
hs : autoParam s.Finite _auto✝
x : α
ht : (insert x s).Infinite
⊢ False

Tactic:
exact ht (hs.insert x)

Result:
no goals

Proof state:
case inl
α : Type u_1
s t : Set α
hs : autoParam s.Finite _auto✝
ht : t.Finite
⊢ (∃ a ∉ s, insert a s = t) ↔ s ⊆ t ∧ s.ncard + 1 = t.ncard

Tactic:
rw [ncard_eq_toFinset_card _ hs, ncard_eq_toFinset_card _ ht,
  ← @Finite.toFinset_subset_toFinset _ _ _ hs ht, ← Finset.exists_eq_insert_iff]

Result:
case inl
α : Type u_1
s t : Set α
hs : autoParam s.Finite _auto✝
ht : t.Finite
⊢ (∃ a ∉ s, insert a s = t) ↔ ∃ a ∉ Finite.toFinset hs, insert a (Finite.toFinset hs) = ht.toFinset

Proof state:
case inr
α : Type u_1
s t : Set α
hs : autoParam s.Finite _auto✝
ht : t.Infinite
⊢ (∃ a ∉ s, insert a s = t) ↔ s ⊆ t ∧ s.ncard + 1 = t.ncard

Tactic:
simp only [ht.ncard, exists_prop, add_eq_zero, and_false, iff_false, not_exists, not_and,
  reduceCtorEq]

Result:
case inr
α : Type u_1
s t : Set α
hs : autoParam s.Finite _auto✝
ht : t.Infinite
⊢ ∀ x ∉ s, ¬insert x s = t

Proof state:
case h.e'_2.h.e'_2.h.a
α : Type u_1
s t : Set α
hs : autoParam s.Finite _auto✝
ht : t.Finite
x : α
⊢ x ∉ s ∧ insert x (Finite.toFinset hs) = ht.toFinset ↔ x ∉ s ∧ insert x s = t

Tactic:
simp [Finset.ext_iff, Set.ext_iff]

Result:
no goals

Proof state:
case h.e'_2.h.e'_2
α : Type u_1
s t : Set α
hs : autoParam s.Finite _auto✝
ht : t.Finite
⊢ (fun a => a ∉ Finite.toFinset hs ∧ insert a (Finite.toFinset hs) = ht.toFinset) = fun a => a ∉ s ∧ insert a s = t

Tactic:
simp only [Finite.mem_toFinset]

Result:
case h.e'_2.h.e'_2
α : Type u_1
s t : Set α
hs : autoParam s.Finite _auto✝
ht : t.Finite
⊢ (fun a => a ∉ s ∧ insert a (Finite.toFinset hs) = ht.toFinset) = fun a => a ∉ s ∧ insert a s = t

Proof state:
case h.e'_2.h.e'_2
α : Type u_1
s t : Set α
hs : autoParam s.Finite _auto✝
ht : t.Finite
⊢ (fun a => a ∉ s ∧ insert a (Finite.toFinset hs) = ht.toFinset) = fun a => a ∉ s ∧ insert a s = t

Tactic:
ext x

Result:
case h.e'_2.h.e'_2.h.a
α : Type u_1
s t : Set α
hs : autoParam s.Finite _auto✝
ht : t.Finite
x : α
⊢ x ∉ s ∧ insert x (Finite.toFinset hs) = ht.toFinset ↔ x ∉ s ∧ insert x s = t