awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
k : ℕ∞
h : s.encard = k + 1
refine_1 : ∀ (a : α) (ha : a ∈ s), ∃ (a : α) (t : Set α), a ∉ t ∧ insert a t = s ∧ t.encard = k
⊢ ∃ (a : α) (t : Set α), a ∉ t ∧ insert a t = s ∧ t.encard = k

Tactic:
obtain ⟨a, ha⟩ := nonempty_of_encard_ne_zero (s := s) (by simp [h])

Premises used: Set.nonempty_of_encard_ne_zero
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
k : ℕ∞
h : s.encard = k + 1
a : α
ha : a ∈ s
rwa : insert a s = s
rwa₁ : s = s
rwa₂ : a ∈ s
rwa₃ : s = s
rwa₄ rwa₅ rwa₆ : a ∈ s
⊢ insert a (s \ {a}) = s

Tactic:
rwa [insert_diff_singleton, insert_eq_of_mem]

Premises used: Set.insert_eq_of_mem, Set.insert_diff_singleton
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
k : ℕ∞
h : s.encard = k + 1
a : α
ha : a ∈ s
refine_1 : (s \ {a}).encard = k
⊢ ∃ (a : α) (t : Set α), a ∉ t ∧ insert a t = s ∧ t.encard = k

Tactic:
refine ⟨a, s \ {a}, fun h ↦ h.2 rfl, by rwa [insert_diff_singleton, insert_eq_of_mem], ?_⟩
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
k : ℕ∞
h : s.encard = k + 1
a : α
ha : a ∈ s
refine_1 : (s \ {a}).encard + 1 = k + 1
refine_1₁ : (s \ {a}).encard + 1 = s.encard
refine_1₂ refine_1₃ : s.encard = s.encard
⊢ (s \ {a}).encard = k

Tactic:
rw [← WithTop.add_right_inj WithTop.one_ne_top, ← h,
      encard_diff_singleton_add_one ha]

Premises used: WithTop.one_ne_top, WithTop.add_right_inj, Set.encard_diff_singleton_add_one
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
a : α
t : Set α
h : a ∉ t
refine_2 refine_2₁ : t.encard + 1 = t.encard + 1
⊢ (insert a t).encard = t.encard + 1

Tactic:
rw [encard_insert_of_notMem h]

Premises used: Set.encard_insert_of_notMem
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
⊢ s = ∅ ∨ s.encard = ⊤ ∨ ∃ a ∈ s, (s \ {a}).encard < s.encard

Tactic:
s.eq_empty_or_nonempty.elim Or.inl (Or.inr ∘ fun ⟨a,ha⟩ ↦
    (s.finite_or_infinite.elim (fun hfin ↦ Or.inr ⟨a, ha, ?_⟩) (Or.inl ∘ Infinite.encard_eq)))

Premises used: Set.encard, Set.finite_or_infinite, Function.comp, Membership.mem, Exists, Set.eq_empty_or_nonempty, Set.Infinite.encard_eq, SDiff.sdiff, And, And.intro, LT.lt, Exists.intro, Or.inl, Or, Top.top, Or.elim, Singleton.singleton, Eq, _private.0.Set.eq_empty_or_encard_eq_top_or_encard_diff_singleton_lt.match_1, Or.inr
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
refine : s.Nonempty → ∀ (a : α) (ha : a ∈ s) (hfin : s.Finite), (s \ {a}).encard < s.encard
⊢ s = ∅ ∨ s.encard = ⊤ ∨ ∃ a ∈ s, (s \ {a}).encard < s.encard

Tactic:
refine s.eq_empty_or_nonempty.elim Or.inl (Or.inr ∘ fun ⟨a,ha⟩ ↦
    (s.finite_or_infinite.elim (fun hfin ↦ Or.inr ⟨a, ha, ?_⟩) (Or.inl ∘ Infinite.encard_eq)))

Premises used: Function.comp, Set.eq_empty_or_nonempty, Or.inl, Or.elim, Or.inr
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
h : s.Nonempty
a : α
ha : a ∈ s
hfin : s.Finite
rw : (s \ {a}).encard < (s \ {a}).encard + 1
⊢ (s \ {a}).encard < s.encard

Tactic:
rw [← encard_diff_singleton_add_one ha]

Premises used: Set.encard_diff_singleton_add_one
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
h : s.Nonempty
a : α
ha : a ∈ s
hfin : s.Finite
nth_rw : (s \ {a}).encard + 0 < (s \ {a}).encard + 1
⊢ (s \ {a}).encard < (s \ {a}).encard + 1

Tactic:
nth_rw 1 [← add_zero (encard _)]

Premises used: Set.encard, add_zero
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
h : s.Nonempty
a : α
ha : a ∈ s
hfin : s.Finite
⊢ (s \ {a}).encard + 0 < (s \ {a}).encard + 1

Tactic:
WithTop.add_lt_add_left hfin.diff.encard_lt_top.ne zero_lt_one

Premises used: Set.Finite.encard_lt_top, Set.Finite.diff, zero_lt_one, ENat, WithTop.add_lt_add_left, LT.lt.ne, WithTop
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
h : s.Nonempty
a : α
ha : a ∈ s
hfin : s.Finite
⊢ (s \ {a}).encard + 0 < (s \ {a}).encard + 1

Tactic:
exact WithTop.add_lt_add_left hfin.diff.encard_lt_top.ne zero_lt_one

Premises used: Set.Finite.encard_lt_top, Set.Finite.diff, zero_lt_one, WithTop.add_lt_add_left, LT.lt.ne
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
x y : α
hne : x ≠ y
⊢ x ∉ {y}

Tactic:
simpa
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
x y : α
hne : x ≠ y
rw : encard (α := α) {y} + 1 = 2
rw₁ : encard (α := α) {y} + 1 = HAdd.hAdd (α := ℕ∞) 1 1
rw₂ : encard (α := α) {y} = 1
rw₃ rw₄ : Eq (α := WithTop ℕ) 1 1
⊢ encard (α := α) {x, y} = 2

Tactic:
rw [encard_insert_of_notMem (by simpa), ← one_add_one_eq_two,
    WithTop.add_right_inj WithTop.one_ne_top, encard_singleton]

Premises used: WithTop.one_ne_top, one_add_one_eq_two, WithTop.add_right_inj, Set.encard_insert_of_notMem, Set.encard_singleton
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
h : ∃ (x : α), s = {x}
x : α
hx : s = {x}
rw : encard (α := α) {x} = 1
rw₁ rw₂ : Eq (α := ℕ∞) 1 1
⊢ s.encard = 1

Tactic:
rw [hx, encard_singleton]

Premises used: Set.encard_singleton
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
refine : ∀ (h : s.encard = 1), ∃ (x : α), s = {x}
⊢ s.encard = 1 ↔ ∃ (x : α), s = {x}

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨x, hx⟩ ↦ by rw [hx, encard_singleton]⟩
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
h : s.encard = 1
rw : Ne (α := ℕ∞) 1 0
⊢ s.encard ≠ 0

Tactic:
rw [h]
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
h : s.encard = 1
⊢ Ne (α := ℕ∞) 1 0

Tactic:
simp
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
h : s.encard = 1
obtain : ∀ (x : α) (hx : x ∈ s), ∃ (x : α), s = {x}
⊢ ∃ (x : α), s = {x}

Tactic:
obtain ⟨x, hx⟩ := nonempty_of_encard_ne_zero (s := s) (by rw [h]; simp)

Premises used: Set.nonempty_of_encard_ne_zero
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
h : s.encard = 1
x : α
hx : x ∈ s
⊢ {x} ⊆ s

Tactic:
simpa
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
h : s.encard = 1
x : α
hx : x ∈ s
⊢ s.encard ≤ encard (α := α) {x}

Tactic:
simp [h]
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
h : s.encard = 1
x : α
hx : x ∈ s
⊢ ∃ (x : α), s = {x}

Tactic:
exact ⟨x, ((finite_singleton x).eq_of_subset_of_encard_le (by simpa) (by simp [h])).symm⟩
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
rw : s.encard < 1 ∨ s.encard = 1 ↔ s = ∅ ∨ ∃ (x : α), s = {x}
rw₁ : ¬1 ≤ s.encard ∨ s.encard = 1 ↔ s = ∅ ∨ ∃ (x : α), s = {x}
rw₂ : ¬s.encard ≠ 0 ∨ s.encard = 1 ↔ s = ∅ ∨ ∃ (x : α), s = {x}
rw₃ : s.encard = 0 ∨ s.encard = 1 ↔ s = ∅ ∨ ∃ (x : α), s = {x}
rw₄ : s = ∅ ∨ s.encard = 1 ↔ s = ∅ ∨ ∃ (x : α), s = {x}
rw₅ rw₆ : (s = ∅ ∨ ∃ (x : α), s = {x}) ↔ s = ∅ ∨ ∃ (x : α), s = {x}
⊢ s.encard ≤ 1 ↔ s = ∅ ∨ ∃ (x : α), s = {x}

Tactic:
rw [le_iff_lt_or_eq, lt_iff_not_ge, ENat.one_le_iff_ne_zero, not_not, encard_eq_zero,
    encard_eq_one]

Premises used: Set.encard_eq_zero, lt_iff_not_ge, Classical.not_not, le_iff_lt_or_eq, Set.encard_eq_one, ENat.one_le_iff_ne_zero
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
rw : (s.Nonempty → ∃ (x : α), s = {x}) ↔ ∀ (a b : α), a ∈ s → b ∈ s → a = b
⊢ s.encard ≤ 1 ↔ ∀ (a b : α), a ∈ s → b ∈ s → a = b

Tactic:
rw [encard_le_one_iff_eq, or_iff_not_imp_left, ← Ne, ← nonempty_iff_ne_empty]

Premises used: Ne, Classical.or_iff_not_imp_left, Set.nonempty_iff_ne_empty, Set.encard_le_one_iff_eq
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
⊢ (s.Nonempty → ∃ (x : α), s = {x}) ↔ ∀ (a b : α), a ∈ s → b ∈ s → a = b

Tactic:
⟨fun h a b has hbs ↦ ?_,
    fun h ⟨x, hx⟩ ↦ ⟨x, ((singleton_subset_iff.2 hx).antisymm' (fun y hy ↦ h _ _ hy hx))⟩⟩

Premises used: Iff.mpr, Set.singleton_subset_iff, Exists, Iff.intro, Exists.intro, Singleton.singleton, Eq, _private.0.Set.eq_empty_or_encard_eq_top_or_encard_diff_singleton_lt.match_1, HasSubset.Subset.antisymm'
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
refine : ∀ (h : s.Nonempty → ∃ (x : α), s = {x}) (a b : α) (has : a ∈ s) (hbs : b ∈ s), a = b
⊢ (s.Nonempty → ∃ (x : α), s = {x}) ↔ ∀ (a b : α), a ∈ s → b ∈ s → a = b

Tactic:
refine ⟨fun h a b has hbs ↦ ?_,
    fun h ⟨x, hx⟩ ↦ ⟨x, ((singleton_subset_iff.2 hx).antisymm' (fun y hy ↦ h _ _ hy hx))⟩⟩
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
h : s.Nonempty → ∃ (x : α), s = {x}
a b : α
has : a ∈ s
hbs : b ∈ s
obtain :
  ∀ (x : α) (h : Set.Nonempty (α := α) {x} → ∃ (x_1 : α), Eq (α := Set α) {x} {x_1})
    (has : Membership.mem (γ := Set α) {x} a) (hbs : Membership.mem (γ := Set α) {x} b), a = b
⊢ a = b

Tactic:
obtain ⟨x, rfl⟩ := h ⟨_, has⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
a b x : α
h : Set.Nonempty (α := α) {x} → ∃ (x_1 : α), Eq (α := Set α) {x} {x_1}
has : Membership.mem (γ := Set α) {x} a
hbs : Membership.mem (γ := Set α) {x} b
rw : x = b
rw₁ rw₂ : x = x
⊢ a = b

Tactic:
rw [(has : a = x), (hbs : b = x)]
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
rw : (∀ (a b : α), a ∈ s → b ∈ s → a = b) ↔ ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x = y
⊢ s.encard ≤ 1 ↔ s.Subsingleton

Tactic:
rw [encard_le_one_iff, Set.Subsingleton]

Premises used: Set.Subsingleton, Set.encard_le_one_iff
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
mp : (∀ (a b : α), a ∈ s → b ∈ s → a = b) → ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x = y
mpr : (∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x = y) → ∀ (a b : α), a ∈ s → b ∈ s → a = b
mp₁ mp₂ mp₃ : (∀ (a b : α), a ∈ s → b ∈ s → a = b) → ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x = y
mpr₁ mpr₂ mpr₃ : (∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x = y) → ∀ (a b : α), a ∈ s → b ∈ s → a = b
mp₄ mp₅ mp₆ : (∀ (a b : α), a ∈ s → b ∈ s → a = b) → ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x = y
mpr₄ mpr₅ mpr₆ : (∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x = y) → ∀ (a b : α), a ∈ s → b ∈ s → a = b
mp₇ mp₈ mp₉ : (∀ (a b : α), a ∈ s → b ∈ s → a = b) → ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x = y
mpr₇ mpr₈ mpr₉ : (∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x = y) → ∀ (a b : α), a ∈ s → b ∈ s → a = b
mp₁₀ mp₁₁ mp₁₂ : (∀ (a b : α), a ∈ s → b ∈ s → a = b) → ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x = y
mpr₁₀ mpr₁₁ mpr₁₂ : (∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x = y) → ∀ (a b : α), a ∈ s → b ∈ s → a = b
mp₁₃ mp₁₄ : (∀ (a b : α), a ∈ s → b ∈ s → a = b) → ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x = y
mpr₁₃ mpr₁₄ : (∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x = y) → ∀ (a b : α), a ∈ s → b ∈ s → a = b
⊢ (∀ (a b : α), a ∈ s → b ∈ s → a = b) ↔ ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x = y

Tactic:
tauto
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
contrapose! : s.encard ≤ 1 ↔ s.Subsingleton
⊢ 1 < s.encard ↔ s.Nontrivial

Tactic:
contrapose!
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
⊢ s.encard ≤ 1 ↔ s.Subsingleton

Tactic:
encard_le_one_iff_subsingleton

Premises used: Set.encard_le_one_iff_subsingleton
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
⊢ s.encard ≤ 1 ↔ s.Subsingleton

Tactic:
exact encard_le_one_iff_subsingleton

Premises used: Set.encard_le_one_iff_subsingleton
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
contrapose! : s.encard ≤ 1 ↔ ∀ (a b : α) (_ : a ∈ s) (_ : b ∈ s), a = b
⊢ 1 < s.encard ↔ ∃ (a : α) (b : α), a ∈ s ∧ b ∈ s ∧ a ≠ b

Tactic:
contrapose!
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
⊢ s.encard ≤ 1 ↔ ∀ (a b : α) (_ : a ∈ s) (_ : b ∈ s), a = b

Tactic:
encard_le_one_iff

Premises used: Set.encard_le_one_iff
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
⊢ s.encard ≤ 1 ↔ ∀ (a b : α) (_ : a ∈ s) (_ : b ∈ s), a = b

Tactic:
exact encard_le_one_iff

Premises used: Set.encard_le_one_iff
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
h : 1 < s.encard
a : α
by_contra! : ∀ (h' : ∀ (b : α) (_ : b ∈ s), b = a), False
⊢ ∃ b ∈ s, b ≠ a

Tactic:
by_contra! h'
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
h : 1 < s.encard
a : α
h' : ∀ (b : α) (_ : b ∈ s), b = a
obtain : ∀ (b b' : α) (hb : b ∈ s) (hb' : b' ∈ s) (hne : b ≠ b'), False
⊢ False

Tactic:
obtain ⟨b, b', hb, hb', hne⟩ := one_lt_encard_iff.1 h

Premises used: Iff.mp, Set.one_lt_encard_iff
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
h : 1 < s.encard
a : α
h' : ∀ (b : α) (_ : b ∈ s), b = a
b b' : α
hb : b ∈ s
hb' : b' ∈ s
hne : b ≠ b'
apply : b = b'
⊢ False

Tactic:
apply hne
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
h : 1 < s.encard
a : α
h' : ∀ (b : α) (_ : b ∈ s), b = a
b b' : α
hb : b ∈ s
hb' : b' ∈ s
hne : b ≠ b'
rw : a = b'
rw₁ rw₂ : a = a
⊢ b = b'

Tactic:
rw [h' b hb, h' b' hb']
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
h : ∃ (x : α) (y : α), x ≠ y ∧ s = {x, y}
x y : α
hne : x ≠ y
hs : s = {x, y}
rw : encard (α := α) {x, y} = 2
rw₁ rw₂ : Eq (α := ℕ∞) 2 2
⊢ s.encard = 2

Tactic:
rw [hs, encard_pair hne]

Premises used: Set.encard_pair
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
refine : ∀ (h : s.encard = 2), ∃ (x : α) (y : α), x ≠ y ∧ s = {x, y}
⊢ s.encard = 2 ↔ ∃ (x : α) (y : α), x ≠ y ∧ s = {x, y}

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨x, y, hne, hs⟩ ↦ by rw [hs, encard_pair hne]⟩
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
h : s.encard = 2
rw : Ne (α := ℕ∞) 2 0
⊢ s.encard ≠ 0

Tactic:
rw [h]
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
h : s.encard = 2
⊢ Ne (α := ℕ∞) 2 0

Tactic:
simp
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
h : s.encard = 2
obtain : ∀ (x : α) (hx : x ∈ s), ∃ (x : α) (y : α), x ≠ y ∧ s = {x, y}
⊢ ∃ (x : α) (y : α), x ≠ y ∧ s = {x, y}

Tactic:
obtain ⟨x, hx⟩ := nonempty_of_encard_ne_zero (s := s) (by rw [h]; simp)

Premises used: Set.nonempty_of_encard_ne_zero
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
h : s.encard = 2
x : α
hx : x ∈ s
⊢ ∃ (x_1 : α), s \ {x} = {x_1}

Tactic:
rw [← insert_eq_of_mem hx, ← insert_diff_singleton, encard_insert_of_notMem (fun h ↦ h.2 rfl),
    ← one_add_one_eq_two, WithTop.add_right_inj (WithTop.one_ne_top), encard_eq_one] at h

Premises used: WithTop.one_ne_top, Set.insert_eq_of_mem, one_add_one_eq_two, WithTop.add_right_inj, Set.encard_eq_one, Set.insert_diff_singleton, Set.encard_insert_of_notMem
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
h : s.encard = 2
x : α
hx : x ∈ s
h₁ : ∃ (x_1 : α), s \ {x} = {x_1}
⊢ x ∈ s

Tactic:
rw [← insert_eq_of_mem hx, ← insert_diff_singleton, encard_insert_of_notMem (fun h ↦ h.2 rfl),
    ← one_add_one_eq_two, WithTop.add_right_inj (WithTop.one_ne_top), encard_eq_one] at h

Premises used: WithTop.one_ne_top, Set.insert_eq_of_mem, one_add_one_eq_two, WithTop.add_right_inj, Set.encard_eq_one, Set.insert_diff_singleton, Set.encard_insert_of_notMem
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
x : α
h : ∃ (x_1 : α), s \ {x} = {x_1}
hx : x ∈ s
obtain : ∀ (y : α) (h : s \ {x} = {y}), ∃ (x : α) (y : α), x ≠ y ∧ s = {x, y}
⊢ ∃ (x : α) (y : α), x ≠ y ∧ s = {x, y}

Tactic:
obtain ⟨y, h⟩ := h
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
x : α
hx : x ∈ s
h : s \ {x} = {x}
⊢ False

Tactic:
(h.symm.subset rfl).2 rfl

Premises used: Eq.subset, And.right, Eq.symm, rfl
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
x : α
hx : x ∈ s
h : s \ {x} = {x}
⊢ False

Tactic:
exact (h.symm.subset rfl).2 rfl

Premises used: Eq.subset, And.right, Eq.symm, rfl
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y : α
h : s \ {x} = {y}
refine : s = {x, y}
⊢ ∃ (x : α) (y : α), x ≠ y ∧ s = {x, y}

Tactic:
refine ⟨x, y, by rintro rfl; exact (h.symm.subset rfl).2 rfl, ?_⟩
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
⊢ s.encard = 3 ↔ ∃ (x : α) (y : α) (z : α), x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}

Tactic:
⟨fun h ↦ ?_, fun ⟨x, y, z, hxy, hyz, hxz, hs⟩ ↦ ?_⟩

Premises used: Set.encard, Iff.intro, OfNat.ofNat, Eq, _private.0.Set.encard_eq_three.match_1
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
refine_1 : ∀ (h : s.encard = 3), ∃ (x : α) (y : α) (z : α), x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
refine_2 :
  (∃ (x : α) (y : α) (z : α), x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}) →
    ∀ (x y z : α) (hxy : x ≠ y) (hyz : x ≠ z) (hxz : y ≠ z) (hs : s = {x, y, z}), s.encard = 3
⊢ s.encard = 3 ↔ ∃ (x : α) (y : α) (z : α), x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨x, y, z, hxy, hyz, hxz, hs⟩ ↦ ?_⟩
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
h : s.encard = 3
rw : Ne (α := ℕ∞) 3 0
⊢ s.encard ≠ 0

Tactic:
rw [h]
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
h : s.encard = 3
⊢ Ne (α := ℕ∞) 3 0

Tactic:
simp
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
h : s.encard = 3
refine_1 : ∀ (x : α) (hx : x ∈ s), ∃ (x : α) (y : α) (z : α), x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
⊢ ∃ (x : α) (y : α) (z : α), x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}

Tactic:
obtain ⟨x, hx⟩ := nonempty_of_encard_ne_zero (s := s) (by rw [h]; simp)

Premises used: Set.nonempty_of_encard_ne_zero
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
x : α
h : (s \ {x}).encard + 1 = 3
hx : x ∈ s
⊢ 3 = HAdd.hAdd (α := ℕ∞) 2 1

Tactic:
rfl

Premises used: WithTop.map₂, ENat, rfl, Option.map₂, WithTop
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
x : α
h : (s \ {x}).encard + 1 = 3
hx : x ∈ s
⊢ 3 = HAdd.hAdd (α := ℕ∞) 2 1

Tactic:
exact rfl

Premises used: rfl
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
h : s.encard = 3
x : α
hx : x ∈ s
⊢ ∃ (x_1 : α) (y : α), x_1 ≠ y ∧ s \ {x} = {x_1, y}

Tactic:
rw [← insert_eq_of_mem hx, ← insert_diff_singleton,
      encard_insert_of_notMem (fun h ↦ h.2 rfl), (by exact rfl : (3 : ℕ∞) = 2 + 1),
      WithTop.add_right_inj WithTop.one_ne_top, encard_eq_two] at h

Premises used: WithTop.one_ne_top, Set.insert_eq_of_mem, WithTop.add_right_inj, Set.encard_eq_two, Set.insert_diff_singleton, Set.encard_insert_of_notMem
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
h : s.encard = 3
x : α
hx : x ∈ s
h₁ : ∃ (x_1 : α) (y : α), x_1 ≠ y ∧ s \ {x} = {x_1, y}
⊢ x ∈ s

Tactic:
rw [← insert_eq_of_mem hx, ← insert_diff_singleton,
      encard_insert_of_notMem (fun h ↦ h.2 rfl), (by exact rfl : (3 : ℕ∞) = 2 + 1),
      WithTop.add_right_inj WithTop.one_ne_top, encard_eq_two] at h

Premises used: WithTop.one_ne_top, Set.insert_eq_of_mem, WithTop.add_right_inj, Set.encard_eq_two, Set.insert_diff_singleton, Set.encard_insert_of_notMem
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
x : α
h : ∃ (x_1 : α) (y : α), x_1 ≠ y ∧ s \ {x} = {x_1, y}
hx : x ∈ s
refine_1 :
  ∀ (y z : α) (hne : y ≠ z) (hs : s \ {x} = {y, z}), ∃ (x : α) (y : α) (z : α), x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
⊢ ∃ (x : α) (y : α) (z : α), x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}

Tactic:
obtain ⟨y, z, hne, hs⟩ := h
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z : α
hne : y ≠ z
hs : s \ {x} = {y, z}
⊢ ∃ (x : α) (y : α) (z : α), x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}

Tactic:
⟨x, y, z, ?_, ?_, hne, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z : α
hne : y ≠ z
hs : s \ {x} = {y, z}
refine_1 : x ≠ y
refine_1₁ : x ≠ z
refine_1₂ : s = {x, y, z}
⊢ ∃ (x : α) (y : α) (z : α), x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}

Tactic:
refine ⟨x, y, z, ?_, ?_, hne, ?_⟩
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
x : α
hx : x ∈ s
z : α
hne : x ≠ z
hs : s \ {x} = {x, z}
⊢ False

Tactic:
(hs.symm.subset (Or.inl rfl)).2 rfl

Premises used: Eq.subset, And.right, Or.inl, Eq.symm, rfl
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
x : α
hx : x ∈ s
z : α
hne : x ≠ z
hs : s \ {x} = {x, z}
⊢ False

Tactic:
exact (hs.symm.subset (Or.inl rfl)).2 rfl

Premises used: Eq.subset, And.right, Or.inl, Eq.symm, rfl
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y : α
hne : y ≠ x
hs : s \ {x} = {y, x}
⊢ False

Tactic:
(hs.symm.subset (Or.inr rfl)).2 rfl

Premises used: Eq.subset, And.right, Eq.symm, Or.inr, rfl
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y : α
hne : y ≠ x
hs : s \ {x} = {y, x}
⊢ False

Tactic:
exact (hs.symm.subset (Or.inr rfl)).2 rfl

Premises used: Eq.subset, And.right, Eq.symm, Or.inr, rfl
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z : α
hne : y ≠ z
hs : s \ {x} = {y, z}
refine_1 : s = insert x (s \ {x})
refine_1₁ : s = insert x s
refine_1₂ refine_1₃ : s = s
⊢ s = {x, y, z}

Tactic:
rw [← hs, insert_diff_singleton, insert_eq_of_mem hx]

Premises used: Set.insert_eq_of_mem, Set.insert_diff_singleton
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
h : ∃ (x : α) (y : α) (z : α), x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
x y z : α
hxy : x ≠ y
hyz : x ≠ z
hxz : y ≠ z
hs : s = {x, y, z}
refine_2 : HAdd.hAdd (α := ℕ∞) 1 1 + 1 = 3
refine_2₁ : y ∉ {z}
refine_2₂ : x ∉ {y, z}
⊢ s.encard = 3

Tactic:
rw [hs, encard_insert_of_notMem, encard_insert_of_notMem, encard_singleton]

Premises used: Set.encard_insert_of_notMem, Set.encard_singleton
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
h : ∃ (x : α) (y : α) (z : α), x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
x y z : α
hxy : x ≠ y
hyz : x ≠ z
hxz : y ≠ z
hs : s = {x, y, z}
⊢ HAdd.hAdd (α := ℕ∞) 1 1 + 1 = 3

Tactic:
aesop
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
h : ∃ (x : α) (y : α) (z : α), x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
x y z : α
hxy : x ≠ y
hyz : x ≠ z
hxz : y ≠ z
hs : s = {x, y, z}
⊢ y ∉ {z}

Tactic:
aesop
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
h : ∃ (x : α) (y : α) (z : α), x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
x y z : α
hxy : x ≠ y
hyz : x ≠ z
hxz : y ≠ z
hs : s = {x, y, z}
⊢ x ∉ {y, z}

Tactic:
aesop
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
⊢ s.encard = 4 ↔ ∃ (x : α) (y : α) (z : α) (w : α), x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}

Tactic:
⟨fun h ↦ ?_, fun ⟨x, y, z, w, hxy, hxz, hxw, hyz, hyw, hzw, hs⟩ ↦ ?_⟩

Premises used: Set.encard, _private.0.Set.encard_eq_four.match_1, Iff.intro, OfNat.ofNat, Eq
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
refine_1 :
  ∀ (h : s.encard = 4),
    ∃ (x : α) (y : α) (z : α) (w : α), x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}
refine_2 :
  (∃ (x : α) (y : α) (z : α) (w : α), x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}) →
    ∀ (x y z w : α) (hxy : x ≠ y) (hxz : x ≠ z) (hxw : x ≠ w) (hyz : y ≠ z) (hyw : y ≠ w) (hzw : z ≠ w)
      (hs : s = {x, y, z, w}), s.encard = 4
⊢ s.encard = 4 ↔ ∃ (x : α) (y : α) (z : α) (w : α), x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨x, y, z, w, hxy, hxz, hxw, hyz, hyw, hzw, hs⟩ ↦ ?_⟩
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
h : s.encard = 4
rw : Ne (α := ℕ∞) 4 0
⊢ s.encard ≠ 0

Tactic:
rw [h]
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
h : s.encard = 4
⊢ Ne (α := ℕ∞) 4 0

Tactic:
simp
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
h : s.encard = 4
refine_1 :
  ∀ (x : α) (hx : x ∈ s),
    ∃ (x : α) (y : α) (z : α) (w : α), x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}
⊢ ∃ (x : α) (y : α) (z : α) (w : α), x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}

Tactic:
obtain ⟨x, hx⟩ := nonempty_of_encard_ne_zero (s := s) (by rw [h]; simp)

Premises used: Set.nonempty_of_encard_ne_zero
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
x : α
h : (s \ {x}).encard + 1 = 4
hx : x ∈ s
⊢ 4 = HAdd.hAdd (α := ℕ∞) 3 1

Tactic:
rfl

Premises used: WithTop.map₂, ENat, rfl, Option.map₂, WithTop
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
x : α
h : (s \ {x}).encard + 1 = 4
hx : x ∈ s
⊢ 4 = HAdd.hAdd (α := ℕ∞) 3 1

Tactic:
exact rfl

Premises used: rfl
-- Module: Mathlib.Data.Set.Card
Goal:
α : Type u_1
s : Set α
h : s.encard = 4
x : α
hx : x ∈ s
⊢ ∃ (x_1 : α) (y : α) (z : α), x_1 ≠ y ∧ x_1 ≠ z ∧ y ≠ z ∧ s \ {x} = {x_1, y, z}

Tactic:
rw [← insert_eq_of_mem hx, ← insert_diff_singleton,
      encard_insert_of_notMem (fun h ↦ h.2 rfl), (by exact rfl : (4 : ℕ∞) = 3 + 1),
      WithTop.add_right_inj WithTop.one_ne_top, encard_eq_three] at h

Premises used: WithTop.one_ne_top, Set.encard_eq_three, Set.insert_eq_of_mem, WithTop.add_right_inj, Set.insert_diff_singleton, Set.encard_insert_of_notMem