awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
⊢ (s.Nonempty → ∃ (x : α), s = {x}) ↔ ∀ (a b : α), a ∈ s → b ∈ s → a = b
have refine : ∀ (h : s.Nonempty → ∃ (x : α), s = {x}) (a b : α) (has : a ∈ s) (hbs : 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))⟩⟩
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
h : s.Nonempty → ∃ (x : α), s = {x}
a b : α
has : a ∈ s
hbs : b ∈ s
⊢ a = b
have 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
Tactic: obtain ⟨x, rfl⟩ := h ⟨_, has⟩
Cleared hypotheses: s, h, has, hbs
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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
⊢ a = b
have rw : x = b
Tactic: rw [(has : a = x), (hbs : b = x)]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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
⊢ a = b
have rw₁ : x = x
Tactic: rw [(has : a = x), (hbs : b = x)]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
⊢ s.encard ≤ 1 ↔ s.Subsingleton
have rw : (∀ (a b : α), a ∈ s → b ∈ s → a = b) ↔ ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x = y
Tactic: rw [encard_le_one_iff, Set.Subsingleton]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
⊢ (∀ (a b : α), a ∈ s → b ∈ s → a = b) ↔ ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x = y
have mp : (∀ (a b : α), a ∈ s → b ∈ s → a = b) → ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x = y
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
mp : (∀ (a b : α), a ∈ s → b ∈ s → a = b) → ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x = y
⊢ (∀ (a b : α), a ∈ s → b ∈ s → a = b) ↔ ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x = y
have mpr : (∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x = y) → ∀ (a b : α), a ∈ s → b ∈ s → a = b
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
⊢ 1 < s.encard ↔ s.Nontrivial
have contrapose! : s.encard ≤ 1 ↔ s.Subsingleton
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
⊢ 1 < s.encard ↔ ∃ (a : α) (b : α), a ∈ s ∧ b ∈ s ∧ a ≠ b
have contrapose! : s.encard ≤ 1 ↔ ∀ (a b : α) (_ : a ∈ s) (_ : b ∈ s), a = b
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
h : 1 < s.encard
a : α
⊢ ∃ b ∈ s, b ≠ a
have by_contra! : ∀ (h' : ∀ (b : α) (_ : b ∈ s), b = a), False
Tactic: by_contra! h'
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
h : 1 < s.encard
a : α
h' : ∀ (b : α) (_ : b ∈ s), b = a
⊢ False
have obtain : ∀ (b b' : α) (hb : b ∈ s) (hb' : b' ∈ s) (hne : b ≠ b'), False
Tactic: obtain ⟨b, b', hb, hb', hne⟩ := one_lt_encard_iff.1 h
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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'
⊢ False
have apply : b = b'
Tactic: apply hne
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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'
⊢ b = b'
have rw : a = b'
Tactic: rw [h' b hb, h' b' hb']
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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'
⊢ b = b'
have rw₁ : a = a
Tactic: rw [h' b hb, h' b' hb']
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
h : ∃ (x : α) (y : α), x ≠ y ∧ s = {x, y}
x y : α
hne : x ≠ y
hs : s = {x, y}
⊢ s.encard = 2
have rw : encard (α := α) {x, y} = 2
Tactic: rw [hs, encard_pair hne]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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
⊢ s.encard = 2
have rw₁ : Eq (α := ℕ∞) 2 2
Tactic: rw [hs, encard_pair hne]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
⊢ s.encard = 2 ↔ ∃ (x : α) (y : α), x ≠ y ∧ s = {x, y}
have refine : ∀ (h : 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]⟩
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
h : s.encard = 2
⊢ s.encard ≠ 0
have rw : Ne (α := ℕ∞) 2 0
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
h : s.encard = 2
⊢ ∃ (x : α) (y : α), x ≠ y ∧ s = {x, y}
have obtain : ∀ (x : α) (hx : x ∈ s), ∃ (x : α) (y : α), x ≠ y ∧ s = {x, y}
Tactic: obtain ⟨x, hx⟩ := nonempty_of_encard_ne_zero (s := s) (by rw [h]; simp)
-- Lean 4 proof step from Mathlib.Data.Set.Card (hypothesis)
Goal:
α : Type u_1
s : Set α
h : s.encard = 2
x : α
hx : x ∈ s
⊢ ∃ (x : α) (y : α), x ≠ y ∧ s = {x, y}
have h₁ : ∃ (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
Cleared hypotheses: h, hx
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
x : α
h : ∃ (x_1 : α), s \ {x} = {x_1}
hx : x ∈ s
⊢ ∃ (x : α) (y : α), x ≠ y ∧ s = {x, y}
have obtain : ∀ (y : α) (h : s \ {x} = {y}), ∃ (x : α) (y : α), x ≠ y ∧ s = {x, y}
Tactic: obtain ⟨y, h⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y : α
h : s \ {x} = {y}
⊢ ∃ (x : α) (y : α), x ≠ y ∧ s = {x, y}
have refine : s = {x, y}
Tactic: refine ⟨x, y, by rintro rfl; exact (h.symm.subset rfl).2 rfl, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
⊢ s.encard = 3 ↔ ∃ (x : α) (y : α) (z : α), x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
have refine_1 : ∀ (h : 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⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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}
⊢ s.encard = 3 ↔ ∃ (x : α) (y : α) (z : α), x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
have 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
Tactic: refine ⟨fun h ↦ ?_, fun ⟨x, y, z, hxy, hyz, hxz, hs⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
h : s.encard = 3
⊢ s.encard ≠ 0
have rw : Ne (α := ℕ∞) 3 0
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
h : s.encard = 3
⊢ ∃ (x : α) (y : α) (z : α), x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
have refine_1 : ∀ (x : α) (hx : x ∈ s), ∃ (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)
-- Lean 4 proof step from Mathlib.Data.Set.Card (hypothesis)
Goal:
α : Type u_1
s : Set α
h : s.encard = 3
x : α
hx : x ∈ s
⊢ ∃ (x : α) (y : α) (z : α), x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
have h₁ : ∃ (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
Cleared hypotheses: h, hx
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
x : α
h : ∃ (x_1 : α) (y : α), x_1 ≠ y ∧ s \ {x} = {x_1, y}
hx : x ∈ s
⊢ ∃ (x : α) (y : α) (z : α), x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
have 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}
Tactic: obtain ⟨y, z, hne, hs⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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}
have refine_1 : x ≠ y
Tactic: refine ⟨x, y, z, ?_, ?_, hne, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z : α
hne : y ≠ z
hs : s \ {x} = {y, z}
refine_1 : x ≠ y
⊢ ∃ (x : α) (y : α) (z : α), x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
have refine_1₁ : x ≠ z
Tactic: refine ⟨x, y, z, ?_, ?_, hne, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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
⊢ ∃ (x : α) (y : α) (z : α), x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
have refine_1₂ : s = {x, y, z}
Tactic: refine ⟨x, y, z, ?_, ?_, hne, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z : α
hne : y ≠ z
hs : s \ {x} = {y, z}
⊢ s = {x, y, z}
have refine_1 : s = insert x (s \ {x})
Tactic: rw [← hs, insert_diff_singleton, insert_eq_of_mem hx]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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})
⊢ s = {x, y, z}
have refine_1₁ : s = insert x s
Tactic: rw [← hs, insert_diff_singleton, insert_eq_of_mem hx]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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
⊢ s = {x, y, z}
have refine_1₂ : s = s
Tactic: rw [← hs, insert_diff_singleton, insert_eq_of_mem hx]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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}
⊢ s.encard = 3
have refine_2 : HAdd.hAdd (α := ℕ∞) 1 1 + 1 = 3
Tactic: rw [hs, encard_insert_of_notMem, encard_insert_of_notMem, encard_singleton]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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
⊢ s.encard = 3
have refine_2₁ : y ∉ {z}
Tactic: rw [hs, encard_insert_of_notMem, encard_insert_of_notMem, encard_singleton]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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}
⊢ s.encard = 3
have refine_2₂ : x ∉ {y, z}
Tactic: rw [hs, encard_insert_of_notMem, encard_insert_of_notMem, encard_singleton]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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}
have 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}
Tactic: refine ⟨fun h ↦ ?_, fun ⟨x, y, z, w, hxy, hxz, hxw, hyz, hyw, hzw, hs⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
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}
⊢ s.encard = 4 ↔ ∃ (x : α) (y : α) (z : α) (w : α), x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}
have 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
Tactic: refine ⟨fun h ↦ ?_, fun ⟨x, y, z, w, hxy, hxz, hxw, hyz, hyw, hzw, hs⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
h : s.encard = 4
⊢ s.encard ≠ 0
have rw : Ne (α := ℕ∞) 4 0
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
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}
have 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}
Tactic: obtain ⟨x, hx⟩ := nonempty_of_encard_ne_zero (s := s) (by rw [h]; simp)
-- Lean 4 proof step from Mathlib.Data.Set.Card (hypothesis)
Goal:
α : Type u_1
s : Set α
h : s.encard = 4
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}
have h₁ : ∃ (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
Cleared hypotheses: h, hx
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
x : α
h : ∃ (x_1 : α) (y : α) (z : α), x_1 ≠ y ∧ x_1 ≠ z ∧ y ≠ z ∧ s \ {x} = {x_1, y, z}
hx : x ∈ s
⊢ ∃ (x : α) (y : α) (z : α) (w : α), x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}
have refine_1 : ∀ (y z w : α) (hyz : y ≠ z) (hyw : y ≠ w) (hzw : z ≠ w) (hs : 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 ⟨y, z, w, hyz, hyw, hzw, hs⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z w : α
hyz : y ≠ z
hyw : y ≠ w
hzw : z ≠ w
hs : 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}
have refine_1 : x ≠ y
Tactic: refine ⟨x, y, z, w, ?_, ?_, ?_, hyz, hyw, hzw, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z w : α
hyz : y ≠ z
hyw : y ≠ w
hzw : z ≠ w
hs : s \ {x} = {y, z, w}
refine_1 : x ≠ y
⊢ ∃ (x : α) (y : α) (z : α) (w : α), x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}
have refine_1₁ : x ≠ z
Tactic: refine ⟨x, y, z, w, ?_, ?_, ?_, hyz, hyw, hzw, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z w : α
hyz : y ≠ z
hyw : y ≠ w
hzw : z ≠ w
hs : s \ {x} = {y, z, w}
refine_1 : x ≠ y
refine_1₁ : x ≠ z
⊢ ∃ (x : α) (y : α) (z : α) (w : α), x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}
have refine_1₂ : x ≠ w
Tactic: refine ⟨x, y, z, w, ?_, ?_, ?_, hyz, hyw, hzw, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z w : α
hyz : y ≠ z
hyw : y ≠ w
hzw : z ≠ w
hs : s \ {x} = {y, z, w}
refine_1 : x ≠ y
refine_1₁ : x ≠ z
refine_1₂ : x ≠ w
⊢ ∃ (x : α) (y : α) (z : α) (w : α), x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}
have refine_1₃ : s = {x, y, z, w}
Tactic: refine ⟨x, y, z, w, ?_, ?_, ?_, hyz, hyw, hzw, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z w : α
hyz : y ≠ z
hyw : y ≠ w
hzw : z ≠ w
hs : s \ {x} = {y, z, w}
⊢ s = {x, y, z, w}
have refine_1 : s = insert x (s \ {x})
Tactic: rw [← hs, insert_diff_singleton, insert_eq_of_mem hx]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z w : α
hyz : y ≠ z
hyw : y ≠ w
hzw : z ≠ w
hs : s \ {x} = {y, z, w}
refine_1 : s = insert x (s \ {x})
⊢ s = {x, y, z, w}
have refine_1₁ : s = insert x s
Tactic: rw [← hs, insert_diff_singleton, insert_eq_of_mem hx]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
x : α
hx : x ∈ s
y z w : α
hyz : y ≠ z
hyw : y ≠ w
hzw : z ≠ w
hs : s \ {x} = {y, z, w}
refine_1 : s = insert x (s \ {x})
refine_1₁ : s = insert x s
⊢ s = {x, y, z, w}
have refine_1₂ : s = s
Tactic: rw [← hs, insert_diff_singleton, insert_eq_of_mem hx]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
h : ∃ (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
have refine_2 : HAdd.hAdd (α := ℕ∞) 1 1 + 1 + 1 = 4
Tactic: rw [hs, encard_insert_of_notMem, encard_insert_of_notMem, encard_insert_of_notMem,
    encard_singleton]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
h : ∃ (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}
refine_2 : HAdd.hAdd (α := ℕ∞) 1 1 + 1 + 1 = 4
⊢ s.encard = 4
have refine_2₁ : z ∉ {w}
Tactic: rw [hs, encard_insert_of_notMem, encard_insert_of_notMem, encard_insert_of_notMem,
    encard_singleton]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
h : ∃ (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}
refine_2 : HAdd.hAdd (α := ℕ∞) 1 1 + 1 + 1 = 4
refine_2₁ : z ∉ {w}
⊢ s.encard = 4
have refine_2₂ : y ∉ {z, w}
Tactic: rw [hs, encard_insert_of_notMem, encard_insert_of_notMem, encard_insert_of_notMem,
    encard_singleton]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
h : ∃ (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}
refine_2 : HAdd.hAdd (α := ℕ∞) 1 1 + 1 + 1 = 4
refine_2₁ : z ∉ {w}
refine_2₂ : y ∉ {z, w}
⊢ s.encard = 4
have refine_2₃ : x ∉ {y, z, w}
Tactic: rw [hs, encard_insert_of_notMem, encard_insert_of_notMem, encard_insert_of_notMem,
    encard_singleton]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
k : ℕ
⊢ encard (α := ℕ) {i : ℕ | i < k} = (↑k : ℕ∞)
have h : encard (α := ℕ) {i : ℕ | i < k} = (↑(Finset.range k) : Set ℕ).encard
Tactic: convert! encard_coe_eq_coe_finsetCard (Finset.range k) using 1
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
k : ℕ
h : encard (α := ℕ) {i : ℕ | i < k} = (↑(Finset.range k) : Set ℕ).encard
⊢ encard (α := ℕ) {i : ℕ | i < k} = (↑k : ℕ∞)
have h₁ : Eq (α := ℕ∞) (↑k : ℕ∞) (↑(Finset.range k).card : ℕ∞)
Tactic: convert! encard_coe_eq_coe_finsetCard (Finset.range k) using 1
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
k : ℕ
⊢ encard (α := ℕ) {i : ℕ | i < k} = (↑(Finset.range k) : Set ℕ).encard
have h : encard (α := ℕ) {i : ℕ | i < k} = (Iio k).encard
Tactic: rw [Finset.coe_range, Iio_def]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
k : ℕ
h : encard (α := ℕ) {i : ℕ | i < k} = (Iio k).encard
⊢ encard (α := ℕ) {i : ℕ | i < k} = (↑(Finset.range k) : Set ℕ).encard
have h₁ : (Iio k).encard = (Iio k).encard
Tactic: rw [Finset.coe_range, Iio_def]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
k : ℕ
⊢ Eq (α := ℕ∞) (↑k : ℕ∞) (↑(Finset.range k).card : ℕ∞)
have h : Eq (α := ℕ∞) (↑k : ℕ∞) (↑k : ℕ∞)
Tactic: rw [Finset.card_range]
-- Lean 4 proof step from Mathlib.Data.Set.Card (hypothesis)
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
h : s ⊆ t
hst : t.encard = s.encard + 1
⊢ ∃ (a : α), t = insert a s
have hst₁ : ∃ (x : α), t \ s = {x}
Tactic: rw [← encard_diff_add_encard_of_subset h, add_comm, WithTop.add_left_inj hs.encard_lt_top.ne,
    encard_eq_one] at hst
Cleared hypotheses: hst
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
h : s ⊆ t
hst : ∃ (x : α), t \ s = {x}
⊢ ∃ (a : α), t = insert a s
have obtain : ∀ (x : α) (hx : t \ s = {x}), ∃ (a : α), t = insert a s
Tactic: obtain ⟨x, hx⟩ := hst
Cleared hypotheses: hst
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
h : s ⊆ t
x : α
hx : t \ s = {x}
⊢ ∃ (a : α), t = insert a s
have h₁ : t = insert x s
Tactic: use x
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
h : s ⊆ t
x : α
hx : t \ s = {x}
⊢ t = insert x s
have h₁ : t \ s ∪ s = insert x s
Tactic: rw [← diff_union_of_subset h, hx, singleton_union]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
h : s ⊆ t
x : α
hx : t \ s = {x}
h₁ : t \ s ∪ s = insert x s
⊢ t = insert x s
have h₂ : {x} ∪ s = insert x s
Tactic: rw [← diff_union_of_subset h, hx, singleton_union]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
h : s ⊆ t
x : α
hx : t \ s = {x}
h₁ : t \ s ∪ s = insert x s
h₂ : {x} ∪ s = insert x s
⊢ t = insert x s
have h₃ : insert x s = insert x s
Tactic: rw [← diff_union_of_subset h, hx, singleton_union]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
n : ℕ
IH : ∀ (hk : (↑n : ℕ∞) ≤ s.encard), ∃ t ⊆ s, t.encard = (↑n : ℕ∞)
hk : (↑n.succ : ℕ∞) ≤ s.encard
⊢ ∃ t ⊆ s, t.encard = (↑n.succ : ℕ∞)
have succ : ∀ (t₀ : Set α) (ht₀s : t₀ ⊆ s) (ht₀ : t₀.encard = (↑n : ℕ∞)), ∃ t ⊆ s, t.encard = (↑n.succ : ℕ∞)
Tactic: obtain ⟨t₀, ht₀s, ht₀⟩ := IH (le_trans (by simp) hk)
-- Lean 4 proof step from Mathlib.Data.Set.Card (hypothesis)
Goal:
α : Type u_1
s : Set α
n : ℕ
IH : ∀ (hk : (↑n : ℕ∞) ≤ s.encard), ∃ t ⊆ s, t.encard = (↑n : ℕ∞)
hk : (↑n.succ : ℕ∞) ≤ s.encard
t₀ : Set α
ht₀s : t₀ ⊆ s
ht₀ : t₀.encard = (↑n : ℕ∞)
⊢ ∃ t ⊆ s, t.encard = (↑n.succ : ℕ∞)
have hk₁ : HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ s.encard
Tactic: simp only [Nat.cast_succ] at *
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.Data.Set.Card (hypothesis)
Goal:
α : Type u_1
n : ℕ
t₀ : Set α
ht₀ : t₀.encard = (↑n : ℕ∞)
IH : ∀ (hk : (↑n : ℕ∞) ≤ t₀.encard), ∃ t ⊆ t₀, t.encard = (↑n : ℕ∞)
ht₀s : t₀ ⊆ t₀
hk : HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ t₀.encard
⊢ False
have hk₁ : n + 1 ≤ n
Tactic: rw [ht₀, ← Nat.cast_one, ← Nat.cast_add, Nat.cast_le] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.Data.Set.Card (hypothesis)
Goal:
α : Type u_1
s : Set α
n : ℕ
IH : ∀ (hk : (↑n : ℕ∞) ≤ s.encard), ∃ t ⊆ s, t.encard = (↑n : ℕ∞)
t₀ : Set α
ht₀s : t₀ ⊆ s
ht₀ : t₀.encard = (↑n : ℕ∞)
hk : HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ s.encard
⊢ ∃ t ⊆ s, t.encard = HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1
have hne : t₀ ≠ s
Tactic: have hne : t₀ ≠ s := by
      rintro rfl; rw [ht₀, ← Nat.cast_one, ← Nat.cast_add, Nat.cast_le] at hk; simp at hk
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
n : ℕ
IH : ∀ (hk : (↑n : ℕ∞) ≤ s.encard), ∃ t ⊆ s, t.encard = (↑n : ℕ∞)
t₀ : Set α
ht₀s : t₀ ⊆ s
ht₀ : t₀.encard = (↑n : ℕ∞)
hk : HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ s.encard
hne : t₀ ≠ s
⊢ ∃ t ⊆ s, t.encard = HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1
have succ : ∀ (x : α) (hx : x ∈ s ∧ x ∉ t₀), ∃ t ⊆ s, t.encard = HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1
Tactic: obtain ⟨x, hx⟩ := exists_of_ssubset (ht₀s.ssubset_of_ne hne)
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
n : ℕ
IH : ∀ (hk : (↑n : ℕ∞) ≤ s.encard), ∃ t ⊆ s, t.encard = (↑n : ℕ∞)
t₀ : Set α
ht₀s : t₀ ⊆ s
ht₀ : t₀.encard = (↑n : ℕ∞)
hk : HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1 ≤ s.encard
hne : t₀ ≠ s
x : α
hx : x ∈ s ∧ x ∉ t₀
⊢ (insert x t₀).encard = HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1
have rw : t₀.encard + 1 = HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1
Tactic: rw [encard_insert_of_notMem hx.2, ht₀]