awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ #(s \ t) + #t = #(s ∪ t)
have rw : #(s \ t ∪ t) = #(s ∪ t)
Tactic: rw [← card_union_of_disjoint sdiff_disjoint, sdiff_union_self_eq_union]
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
rw : #(s \ t ∪ t) = #(s ∪ t)
⊢ #(s \ t) + #t = #(s ∪ t)
have rw₁ : #(s ∪ t) = #(s ∪ t)
Tactic: rw [← card_union_of_disjoint sdiff_disjoint, sdiff_union_self_eq_union]
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
⊢ #(s \ t) + #(s ∩ t) = #s
have rw : #(s \ t ∪ s ∩ t) = #s
Tactic: rw [← card_union_of_disjoint (disjoint_sdiff_inter _ _), sdiff_union_inter]
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Finset α
rw : #(s \ t ∪ s ∩ t) = #s
⊢ #(s \ t) + #(s ∩ t) = #s
have rw₁ : #s = #s
Tactic: rw [← card_union_of_disjoint (disjoint_sdiff_inter _ _), sdiff_union_inter]
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s t u : Finset α
inst : DecidableEq α
hts : t ⊆ s
hus : u ⊆ s
hstu : #s < #t + #u
⊢ (t ∩ u).Nonempty
have contrapose! : ∀ (hstu : t ∩ u = ∅), #t + #u ≤ #s
Tactic: contrapose! hstu
Cleared hypotheses: hstu
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s t u : Finset α
inst : DecidableEq α
hts : t ⊆ s
hus : u ⊆ s
hstu : t ∩ u = ∅
⊢ #(t ∪ u) ≤ #s
have a : t ∪ u ⊆ s
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s t u : Finset α
inst : DecidableEq α
hts : t ⊆ s
hus : u ⊆ s
hstu : t ∩ u = ∅
⊢ #t + #u ≤ #s
have _ : #t + #u = #(t ∪ u)
Tactic: calc
    _ = #(t ∪ u) := by simp [← card_union_add_card_inter, hstu]
    _ ≤ #s := by gcongr; exact union_subset hts hus
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s t u : Finset α
inst : DecidableEq α
hts : t ⊆ s
hus : u ⊆ s
hstu : t ∩ u = ∅
_ : #t + #u = #(t ∪ u)
⊢ #t + #u ≤ #s
have _₁ : #(t ∪ u) ≤ #s
Tactic: calc
    _ = #(t ∪ u) := by simp [← card_union_add_card_inter, hstu]
    _ ≤ #s := by gcongr; exact union_subset hts hus
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s : Finset α
p : α → Prop
inst : DecidablePred p
inst_1 : (x : α) → Decidable ¬p x
⊢ #(filter p s) + #({a ∈ s | ¬p a}) = #s
have rw : #(filter p s ∪ {a ∈ s | ¬p a}) = #s
Tactic: rw [← card_union_of_disjoint (disjoint_filter_filter_not _ _ _), filter_union_filter_not_eq]
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s : Finset α
p : α → Prop
inst : DecidablePred p
inst_1 : (x : α) → Decidable ¬p x
rw : #(filter p s ∪ {a ∈ s | ¬p a}) = #s
⊢ #(filter p s) + #({a ∈ s | ¬p a}) = #s
have rw₁ : #s = #s
Tactic: rw [← card_union_of_disjoint (disjoint_filter_filter_not _ _ _), filter_union_filter_not_eq]
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s : Finset α
p : α → Prop
inst : DecidablePred p
inst_1 : (x : α) → Decidable ¬p x
⊢ #(filter p s) + #({a ∈ s | ¬p a}) = #s
have rw : #(filter p s ∪ {a ∈ s | ¬p a}) = #s
Tactic: classical
  rw [← card_union_of_disjoint (disjoint_filter_filter_not _ _ _), filter_union_filter_not_eq]
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s : Finset α
p : α → Prop
inst : DecidablePred p
inst_1 : (x : α) → Decidable ¬p x
rw : #(filter p s ∪ {a ∈ s | ¬p a}) = #s
⊢ #(filter p s) + #({a ∈ s | ¬p a}) = #s
have rw₁ : #s = #s
Tactic: classical
  rw [← card_union_of_disjoint (disjoint_filter_filter_not _ _ _), filter_union_filter_not_eq]
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
hnt : n ≤ #t
⊢ ∃ (u : Finset α), s ⊆ u ∧ u ⊆ t ∧ #u = n
have refine : ∀ k < #t, n ≤ k → (∃ (u : Finset α), s ⊆ u ∧ u ⊆ t ∧ #u = k + 1) → ∃ (u : Finset α), s ⊆ u ∧ u ⊆ t ∧ #u = k
Tactic: refine Nat.decreasingInduction' ?_ hnt ⟨t, by simp [hst]⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
hnt : n ≤ #t
k : ℕ
h : k < #t
hnk : n ≤ k
⊢ (∃ (u : Finset α), s ⊆ u ∧ u ⊆ t ∧ #u = k + 1) → ∃ (u : Finset α), s ⊆ u ∧ u ⊆ t ∧ #u = k
have this : ∀ (u : Finset α) (hu₁ : s ⊆ u) (hu₂ : u ⊆ t) (hu₃ : #u = k + 1), ∃ (u : Finset α), s ⊆ u ∧ u ⊆ t ∧ #u = k
Tactic: ⟨u, hu₁, hu₂, hu₃⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
hnt : n ≤ #t
k : ℕ
h : k < #t
hnk : n ≤ k
u : Finset α
hu₁ : s ⊆ u
hu₂ : u ⊆ t
hu₃ : #u = k + 1
⊢ ∃ (u : Finset α), s ⊆ u ∧ u ⊆ t ∧ #u = k
have obtain : ∀ (a : α) (ha : a ∈ u \ s), ∃ (u : Finset α), s ⊆ u ∧ u ⊆ t ∧ #u = k
Tactic: obtain ⟨a, ha⟩ : (u \ s).Nonempty := by grind
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
hnt : n ≤ #t
⊢ ∃ (u : Finset α), s ⊆ u ∧ u ⊆ t ∧ #u = n
have refine : ∀ k < #t, n ≤ k → (∃ (u : Finset α), s ⊆ u ∧ u ⊆ t ∧ #u = k + 1) → ∃ (u : Finset α), s ⊆ u ∧ u ⊆ t ∧ #u = k
Tactic: classical
  refine Nat.decreasingInduction' ?_ hnt ⟨t, by simp [hst]⟩
  intro k _ hnk ⟨u, hu₁, hu₂, hu₃⟩
  obtain ⟨a, ha⟩ : (u \ s).Nonempty := by grind
  exact ⟨u.erase a, by grind⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
hnt : n ≤ #t
refine : ∀ k < #t, n ≤ k → (∃ (u : Finset α), s ⊆ u ∧ u ⊆ t ∧ #u = k + 1) → ∃ (u : Finset α), s ⊆ u ∧ u ⊆ t ∧ #u = k
⊢ ∃ (u : Finset α), s ⊆ u ∧ u ⊆ t ∧ #u = n
have refine₁ : ∀ k < #t,
  ∀ (hnk : n ≤ k) (u : Finset α) (hu₁ : s ⊆ u) (hu₂ : u ⊆ t) (hu₃ : #u = k + 1),
    ∃ (u : Finset α), s ⊆ u ∧ u ⊆ t ∧ #u = k
Tactic: classical
  refine Nat.decreasingInduction' ?_ hnt ⟨t, by simp [hst]⟩
  intro k _ hnk ⟨u, hu₁, hu₂, hu₃⟩
  obtain ⟨a, ha⟩ : (u \ s).Nonempty := by grind
  exact ⟨u.erase a, by grind⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s t : Finset α
n : ℕ
hst : s ⊆ t
hsn : #s ≤ n
hnt : n ≤ #t
refine : ∀ k < #t, n ≤ k → (∃ (u : Finset α), s ⊆ u ∧ u ⊆ t ∧ #u = k + 1) → ∃ (u : Finset α), s ⊆ u ∧ u ⊆ t ∧ #u = k
refine₁ :
  ∀ k < #t,
    ∀ (hnk : n ≤ k) (u : Finset α) (hu₁ : s ⊆ u) (hu₂ : u ⊆ t) (hu₃ : #u = k + 1),
      ∃ (u : Finset α), s ⊆ u ∧ u ⊆ t ∧ #u = k
⊢ ∃ (u : Finset α), s ⊆ u ∧ u ⊆ t ∧ #u = n
have refine₂ : ∀ k < #t,
  ∀ (hnk : n ≤ k) (u : Finset α) (hu₁ : s ⊆ u) (hu₂ : u ⊆ t) (hu₃ : #u = k + 1) (a : α) (ha : a ∈ u \ s),
    ∃ (u : Finset α), s ⊆ u ∧ u ⊆ t ∧ #u = k
Tactic: classical
  refine Nat.decreasingInduction' ?_ hnt ⟨t, by simp [hst]⟩
  intro k _ hnk ⟨u, hu₁, hu₂, hu₃⟩
  obtain ⟨a, ha⟩ : (u \ s).Nonempty := by grind
  exact ⟨u.erase a, by grind⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s : Finset α
n : ℕ
⊢ n ≤ #s ↔ ∃ t ⊆ s, #t = n
have refine : ∀ (h : n ≤ #s), ∃ t ⊆ s, #t = n
Tactic: refine ⟨fun h => ?_, fun ⟨t, hst, ht⟩ => ht ▸ card_le_card hst⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s : Finset α
⊢ #s = 1 ↔ ∃ (a : α), s = {a}
have mk : ∀ (val : Multiset α) (nodup : val.Nodup),
  #{ val := val, nodup := nodup : Finset α } = 1 ↔ ∃ (a : α), { val := val, nodup := nodup : Finset α } = {a}
Tactic: cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s t : Finset α
inst : DecidableEq α
⊢ (∃ a ∉ s, insert a s = t) ↔ s ⊆ t ∧ #s + 1 = #t
have mp : (∃ a ∉ s, insert a s = t) → s ⊆ t ∧ #s + 1 = #t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s t : Finset α
inst : DecidableEq α
mp : (∃ a ∉ s, insert a s = t) → s ⊆ t ∧ #s + 1 = #t
⊢ (∃ a ∉ s, insert a s = t) ↔ s ⊆ t ∧ #s + 1 = #t
have mpr : s ⊆ t ∧ #s + 1 = #t → ∃ a ∉ s, insert a s = t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s t : Finset α
inst : DecidableEq α
hst : s ⊆ t
h : #s + 1 = #t
⊢ ∃ a ∉ s, insert a s = t
have mpr : ∀ (a : α) (ha : t \ s = {a}), ∃ a ∉ s, insert a s = t
Tactic: obtain ⟨a, ha⟩ : ∃ a, t \ s = {a} := card_eq_one.mp (by grind)
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s : Finset α
⊢ #s ≤ 1 ↔ ∀ a ∈ s, ∀ b ∈ s, a = b
have inl : card.{u_1} (α := α) ∅ ≤ 1 ↔
  ∀ (a : α), Membership.mem (γ := Finset α) ∅ a → ∀ (b : α), Membership.mem (γ := Finset α) ∅ b → a = b
Tactic: obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s : Finset α
inl :
  card.{u_1} (α := α) ∅ ≤ 1 ↔
    ∀ (a : α), Membership.mem (γ := Finset α) ∅ a → ∀ (b : α), Membership.mem (γ := Finset α) ∅ b → a = b
⊢ #s ≤ 1 ↔ ∀ a ∈ s, ∀ b ∈ s, a = b
have inr : ∀ (x : α) (hx : x ∈ s), #s ≤ 1 ↔ ∀ a ∈ s, ∀ b ∈ s, a = b
Tactic: obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s : Finset α
x : α
hx : x ∈ s
⊢ #s ≤ 1 ↔ ∀ a ∈ s, ∀ b ∈ s, a = b
have inr : (∃ (a : α), s = {a}) → ∀ a ∈ s, ∀ b ∈ s, a = b
Tactic: refine (Nat.succ_le_of_lt (card_pos.2 ⟨x, hx⟩)).ge_iff_eq'.trans (card_eq_one.trans ⟨?_, ?_⟩)
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s : Finset α
x : α
hx : x ∈ s
inr : (∃ (a : α), s = {a}) → ∀ a ∈ s, ∀ b ∈ s, a = b
⊢ #s ≤ 1 ↔ ∀ a ∈ s, ∀ b ∈ s, a = b
have inr₁ : (∀ a ∈ s, ∀ b ∈ s, a = b) → ∃ (a : α), s = {a}
Tactic: refine (Nat.succ_le_of_lt (card_pos.2 ⟨x, hx⟩)).ge_iff_eq'.trans (card_eq_one.trans ⟨?_, ?_⟩)
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s : Finset α
⊢ #s ≤ 1 ↔ (↑s : Set α).Subsingleton
have rw : Subsingleton.{u_1 + 1} ↥s ↔ (↑s : Set α).Subsingleton
Tactic: rw [card_le_one_iff_subsingleton_coe, ← Set.subsingleton_coe, SetLike.coe_sort_coe]
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s : Finset α
rw : Subsingleton.{u_1 + 1} ↥s ↔ (↑s : Set α).Subsingleton
⊢ #s ≤ 1 ↔ (↑s : Set α).Subsingleton
have rw₁ : Subsingleton.{u_1 + 1} ↥s ↔ Subsingleton.{u_1 + 1} (↑(↑s : Set α) : Type u_1)
Tactic: rw [card_le_one_iff_subsingleton_coe, ← Set.subsingleton_coe, SetLike.coe_sort_coe]
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s : Finset α
rw : Subsingleton.{u_1 + 1} ↥s ↔ (↑s : Set α).Subsingleton
rw₁ : Subsingleton.{u_1 + 1} ↥s ↔ Subsingleton.{u_1 + 1} (↑(↑s : Set α) : Type u_1)
⊢ #s ≤ 1 ↔ (↑s : Set α).Subsingleton
have rw₂ : Subsingleton.{u_1 + 1} ↥s ↔ Subsingleton.{u_1 + 1} ↥s
Tactic: rw [card_le_one_iff_subsingleton_coe, ← Set.subsingleton_coe, SetLike.coe_sort_coe]
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s : Finset α
inst : Nonempty α
⊢ #s ≤ 1 ↔ ∃ (x : α), s ⊆ {x}
have refine_1 : ∀ (H : #s ≤ 1), ∃ (x : α), s ⊆ {x}
Tactic: refine ⟨fun H => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s : Finset α
inst : Nonempty α
refine_1 : ∀ (H : #s ≤ 1), ∃ (x : α), s ⊆ {x}
⊢ #s ≤ 1 ↔ ∃ (x : α), s ⊆ {x}
have refine_2 : (∃ (x : α), s ⊆ {x}) → #s ≤ 1
Tactic: refine ⟨fun H => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s : Finset α
inst : Nonempty α
H : #s ≤ 1
⊢ ∃ (x : α), s ⊆ {x}
have refine_1 : ∀ (H : card.{u_1} (α := α) ∅ ≤ 1), ∃ (x : α), Subset (α := Finset α) ∅ {x}
Tactic: obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty
Cleared hypotheses: s, H
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s : Finset α
inst : Nonempty α
H : #s ≤ 1
refine_1 : ∀ (H : card.{u_1} (α := α) ∅ ≤ 1), ∃ (x : α), Subset (α := Finset α) ∅ {x}
⊢ ∃ (x : α), s ⊆ {x}
have refine_1₁ : ∀ (x : α) (hx : x ∈ s), ∃ (x : α), s ⊆ {x}
Tactic: obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s : Finset α
inst : Nonempty α
H : #s ≤ 1
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ Membership.mem (γ := Finset α) {x} y
have rw : Membership.mem (γ := Finset α) {x} x
Tactic: rw [card_le_one.1 H y hy x hx, mem_singleton]
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s : Finset α
inst : Nonempty α
H : #s ≤ 1
x : α
hx : x ∈ s
y : α
hy : y ∈ s
rw : Membership.mem (γ := Finset α) {x} x
⊢ Membership.mem (γ := Finset α) {x} y
have rw₁ : x = x
Tactic: rw [card_le_one.1 H y hy x hx, mem_singleton]
-- Lean 4 proof step from Mathlib.Data.Finset.Card (hypothesis)
Goal:
α : Type u_1
s : Finset α
hs : 1 < #s
a : α
⊢ ∃ b ∈ s, b ≠ a
have this : Nonempty α
Tactic: have : Nonempty α := ⟨a⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s : Finset α
hs : 1 < #s
a : α
this : Nonempty α
⊢ ∃ b ∈ s, b ≠ a
have by_contra! : ∀ (this : ∀ (b : α) (_ : b ∈ s), b = a), False
Tactic: by_contra!
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s : Finset α
⊢ 1 < #s ↔ ∃ a ∈ s, ∃ b ∈ s, a ≠ b
have contrapose! : #s ≤ 1 ↔ ∀ (a : α) (_ : a ∈ s) (b : α) (_ : b ∈ s), a = b
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s : Finset α
⊢ 1 < #s ↔ ∃ (a : α) (b : α), a ∈ s ∧ b ∈ s ∧ a ≠ b
have rw : (∃ a ∈ s, ∃ b ∈ s, a ≠ b) ↔ ∃ (a : α) (b : α), a ∈ s ∧ b ∈ s ∧ a ≠ b
Tactic: rw [one_lt_card]
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s : Finset α
⊢ 1 < #s ↔ s.Nontrivial
have rw : ¬1 < #s ↔ ¬s.Nontrivial
Tactic: rw [← not_iff_not, not_lt, Finset.Nontrivial, ← Set.nontrivial_coe_sort,
    not_nontrivial_iff_subsingleton, card_le_one_iff_subsingleton_coe, coe_sort_coe]
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s : Finset α
rw : ¬1 < #s ↔ ¬s.Nontrivial
⊢ 1 < #s ↔ s.Nontrivial
have rw₁ : #s ≤ 1 ↔ ¬s.Nontrivial
Tactic: rw [← not_iff_not, not_lt, Finset.Nontrivial, ← Set.nontrivial_coe_sort,
    not_nontrivial_iff_subsingleton, card_le_one_iff_subsingleton_coe, coe_sort_coe]
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s : Finset α
rw : ¬1 < #s ↔ ¬s.Nontrivial
rw₁ : #s ≤ 1 ↔ ¬s.Nontrivial
⊢ 1 < #s ↔ s.Nontrivial
have rw₂ : #s ≤ 1 ↔ ¬(↑s : Set α).Nontrivial
Tactic: rw [← not_iff_not, not_lt, Finset.Nontrivial, ← Set.nontrivial_coe_sort,
    not_nontrivial_iff_subsingleton, card_le_one_iff_subsingleton_coe, coe_sort_coe]
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s : Finset α
rw : ¬1 < #s ↔ ¬s.Nontrivial
rw₁ : #s ≤ 1 ↔ ¬s.Nontrivial
rw₂ : #s ≤ 1 ↔ ¬(↑s : Set α).Nontrivial
⊢ 1 < #s ↔ s.Nontrivial
have rw₃ : #s ≤ 1 ↔ ¬Nontrivial.{u_1} (↑(↑s : Set α) : Type u_1)
Tactic: rw [← not_iff_not, not_lt, Finset.Nontrivial, ← Set.nontrivial_coe_sort,
    not_nontrivial_iff_subsingleton, card_le_one_iff_subsingleton_coe, coe_sort_coe]
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s : Finset α
rw : ¬1 < #s ↔ ¬s.Nontrivial
rw₁ : #s ≤ 1 ↔ ¬s.Nontrivial
rw₂ : #s ≤ 1 ↔ ¬(↑s : Set α).Nontrivial
rw₃ : #s ≤ 1 ↔ ¬Nontrivial.{u_1} (↑(↑s : Set α) : Type u_1)
⊢ 1 < #s ↔ s.Nontrivial
have rw₄ : #s ≤ 1 ↔ Subsingleton.{u_1 + 1} (↑(↑s : Set α) : Type u_1)
Tactic: rw [← not_iff_not, not_lt, Finset.Nontrivial, ← Set.nontrivial_coe_sort,
    not_nontrivial_iff_subsingleton, card_le_one_iff_subsingleton_coe, coe_sort_coe]
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s : Finset α
rw : ¬1 < #s ↔ ¬s.Nontrivial
rw₁ : #s ≤ 1 ↔ ¬s.Nontrivial
rw₂ : #s ≤ 1 ↔ ¬(↑s : Set α).Nontrivial
rw₃ : #s ≤ 1 ↔ ¬Nontrivial.{u_1} (↑(↑s : Set α) : Type u_1)
rw₄ : #s ≤ 1 ↔ Subsingleton.{u_1 + 1} (↑(↑s : Set α) : Type u_1)
⊢ 1 < #s ↔ s.Nontrivial
have rw₅ : Subsingleton.{u_1 + 1} ↥s ↔ Subsingleton.{u_1 + 1} (↑(↑s : Set α) : Type u_1)
Tactic: rw [← not_iff_not, not_lt, Finset.Nontrivial, ← Set.nontrivial_coe_sort,
    not_nontrivial_iff_subsingleton, card_le_one_iff_subsingleton_coe, coe_sort_coe]
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s : Finset α
rw : ¬1 < #s ↔ ¬s.Nontrivial
rw₁ : #s ≤ 1 ↔ ¬s.Nontrivial
rw₂ : #s ≤ 1 ↔ ¬(↑s : Set α).Nontrivial
rw₃ : #s ≤ 1 ↔ ¬Nontrivial.{u_1} (↑(↑s : Set α) : Type u_1)
rw₄ : #s ≤ 1 ↔ Subsingleton.{u_1 + 1} (↑(↑s : Set α) : Type u_1)
rw₅ : Subsingleton.{u_1 + 1} ↥s ↔ Subsingleton.{u_1 + 1} (↑(↑s : Set α) : Type u_1)
⊢ 1 < #s ↔ s.Nontrivial
have rw₆ : Subsingleton.{u_1 + 1} ↥s ↔ Subsingleton.{u_1 + 1} ↥s
Tactic: rw [← not_iff_not, not_lt, Finset.Nontrivial, ← Set.nontrivial_coe_sort,
    not_nontrivial_iff_subsingleton, card_le_one_iff_subsingleton_coe, coe_sort_coe]
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
ι : Type u_4
α : ι → Type u_5
inst : (i : ι) → DecidableEq (α i)
s : Finset ((i : ι) → α i)
h : 1 < #s
⊢ ∃ (i : ι), 1 < card.{u_5} (α := α i) (image (fun (x : (i : ι) → α i) ↦ x i) s) ∧ ∀ (ai : α i), {x ∈ s | x i = ai} ⊂ s
have simp_rw : ∀ (h : ∃ (a : (i : ι) → α i) (b : (i : ι) → α i), a ∈ s ∧ b ∈ s ∧ ∃ (a_1 : ι), a a_1 ≠ b a_1),
  ∃ (i : ι),
    (∃ (a : α i) (b : α i),
        Membership.mem (γ := Finset (α i)) (image (fun (x : (i : ι) → α i) ↦ x i) s) a ∧
          Membership.mem (γ := Finset (α i)) (image (fun (x : (i : ι) → α i) ↦ x i) s) b ∧ a ≠ b) ∧
      ∀ (ai : α i), {x ∈ s | x i = ai} ⊂ s
Tactic: simp_rw [one_lt_card_iff, Function.ne_iff] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
ι : Type u_4
α : ι → Type u_5
inst : (i : ι) → DecidableEq (α i)
s : Finset ((i : ι) → α i)
h : ∃ (a : (i : ι) → α i) (b : (i : ι) → α i), a ∈ s ∧ b ∈ s ∧ ∃ (a_1 : ι), a a_1 ≠ b a_1
⊢ ∃ (i : ι),
    (∃ (a : α i) (b : α i),
        Membership.mem (γ := Finset (α i)) (image (fun (x : (i : ι) → α i) ↦ x i) s) a ∧
          Membership.mem (γ := Finset (α i)) (image (fun (x : (i : ι) → α i) ↦ x i) s) b ∧ a ≠ b) ∧
      ∀ (ai : α i), {x ∈ s | x i = ai} ⊂ s
have obtain : ∀ (a1 a2 : (i : ι) → α i) (h1 : a1 ∈ s) (h2 : a2 ∈ s) (i : ι) (hne : a1 i ≠ a2 i),
  ∃ (i : ι),
    (∃ (a : α i) (b : α i),
        Membership.mem (γ := Finset (α i)) (image (fun (x : (i : ι) → α i) ↦ x i) s) a ∧
          Membership.mem (γ := Finset (α i)) (image (fun (x : (i : ι) → α i) ↦ x i) s) b ∧ a ≠ b) ∧
      ∀ (ai : α i), {x ∈ s | x i = ai} ⊂ s
Tactic: obtain ⟨a1, a2, h1, h2, i, hne⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
ι : Type u_4
α : ι → Type u_5
inst : (i : ι) → DecidableEq (α i)
s : Finset ((i : ι) → α i)
a1 a2 : (i : ι) → α i
h1 : a1 ∈ s
h2 : a2 ∈ s
i : ι
hne : a1 i ≠ a2 i
⊢ ∃ (i : ι),
    (∃ (a : α i) (b : α i),
        Membership.mem (γ := Finset (α i)) (image (fun (x : (i : ι) → α i) ↦ x i) s) a ∧
          Membership.mem (γ := Finset (α i)) (image (fun (x : (i : ι) → α i) ↦ x i) s) b ∧ a ≠ b) ∧
      ∀ (ai : α i), {x ∈ s | x i = ai} ⊂ s
have refine : ∀ (ai : α i), {x ∈ s | x i = ai} ⊂ s
Tactic: refine ⟨i, ⟨_, _, mem_image_of_mem _ h1, mem_image_of_mem _ h2, hne⟩, fun ai => ?_⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
ι : Type u_4
α : ι → Type u_5
inst : (i : ι) → DecidableEq (α i)
s : Finset ((i : ι) → α i)
a1 a2 : (i : ι) → α i
h1 : a1 ∈ s
h2 : a2 ∈ s
i : ι
hne : a1 i ≠ a2 i
ai : α i
⊢ {x ∈ s | x i = ai} ⊂ s
have rw : ∃ x ∈ s, ¬x i = ai
Tactic: rw [filter_ssubset]
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
ι : Type u_4
α : ι → Type u_5
inst : (i : ι) → DecidableEq (α i)
s : Finset ((i : ι) → α i)
a1 a2 : (i : ι) → α i
h1 : a1 ∈ s
h2 : a2 ∈ s
i : ι
hne : a1 i ≠ a2 i
ai : α i
⊢ ∃ x ∈ s, ¬x i = ai
have inl : ∃ x ∈ s, ¬x i = a2 i
Tactic: obtain rfl | hne := eq_or_ne (a2 i) ai
Cleared hypotheses: ai
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
ι : Type u_4
α : ι → Type u_5
inst : (i : ι) → DecidableEq (α i)
s : Finset ((i : ι) → α i)
a1 a2 : (i : ι) → α i
h1 : a1 ∈ s
h2 : a2 ∈ s
i : ι
hne : a1 i ≠ a2 i
ai : α i
inl : ∃ x ∈ s, ¬x i = a2 i
⊢ ∃ x ∈ s, ¬x i = ai
have inr : ∀ (hne : a2 i ≠ ai), ∃ x ∈ s, ¬x i = ai
Tactic: obtain rfl | hne := eq_or_ne (a2 i) ai
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
⊢ #s = 2 ↔ ∃ (x : α) (y : α), x ≠ y ∧ s = {x, y}
have mp : #s = 2 → ∃ (x : α) (y : α), x ≠ y ∧ s = {x, y}
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
mp : #s = 2 → ∃ (x : α) (y : α), x ≠ y ∧ s = {x, y}
⊢ #s = 2 ↔ ∃ (x : α) (y : α), x ≠ y ∧ s = {x, y}
have mpr : (∃ (x : α) (y : α), x ≠ y ∧ s = {x, y}) → #s = 2
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
⊢ #s = 2 → ∃ (x : α) (y : α), x ≠ y ∧ s = {x, y}
have mp : (∃ (a : α) (t : Finset α), a ∉ t ∧ insert a t = s ∧ #t = 1) → ∃ (x : α) (y : α), x ≠ y ∧ s = {x, y}
Tactic: rw [card_eq_succ]
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
⊢ #s = 3 ↔ ∃ (x : α) (y : α) (z : α), x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
have mp : #s = 3 → ∃ (x : α) (y : α) (z : α), x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
mp : #s = 3 → ∃ (x : α) (y : α) (z : α), x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
⊢ #s = 3 ↔ ∃ (x : α) (y : α) (z : α), x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
have mpr : (∃ (x : α) (y : α) (z : α), x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}) → #s = 3
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
⊢ #s = 3 → ∃ (x : α) (y : α) (z : α), x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
have mp : (∃ (a : α) (t : Finset α), a ∉ t ∧ insert a t = s ∧ #t = 2) →
  ∃ (x : α) (y : α) (z : α), x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z}
Tactic: rw [card_eq_succ]
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
⊢ #s = 4 ↔ ∃ (x : α) (y : α) (z : α) (w : α), x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}
have mp : #s = 4 → ∃ (x : α) (y : α) (z : α) (w : α), x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
mp : #s = 4 → ∃ (x : α) (y : α) (z : α) (w : α), x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}
⊢ #s = 4 ↔ ∃ (x : α) (y : α) (z : α) (w : α), x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}
have mpr : (∃ (x : α) (y : α) (z : α) (w : α), x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}) → #s = 4
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s : Finset α
inst : DecidableEq α
⊢ #s = 4 → ∃ (x : α) (y : α) (z : α) (w : α), x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}
have mp : (∃ (a : α) (t : Finset α), a ∉ t ∧ insert a t = s ∧ #t = 3) →
  ∃ (x : α) (y : α) (z : α) (w : α), x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w}
Tactic: rw [card_eq_succ]
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s : Finset α
⊢ 2 < #s ↔ ∃ (a : α) (b : α) (c : α), a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
have simp_rw : (∃ (b : α) (b_1 : α) (b_2 : α), ∃ a ⊆ s, b ≠ b_1 ∧ b ≠ b_2 ∧ b_1 ≠ b_2 ∧ a = {b, b_1, b_2}) ↔
  ∃ (a : α) (b : α) (c : α), a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
Tactic: simp_rw [lt_iff_add_one_le, le_card_iff_exists_subset_card, reduceAdd, card_eq_three,
      ← exists_and_left, exists_comm (α := Finset α)]
-- Lean 4 proof step from Mathlib.Data.Finset.Card (goal)
Goal:
α : Type u_1
s : Finset α
⊢ (∃ (b : α) (b_1 : α) (b_2 : α), ∃ a ⊆ s, b ≠ b_1 ∧ b ≠ b_2 ∧ b_1 ≠ b_2 ∧ a = {b, b_1, b_2}) ↔
    ∃ (a : α) (b : α) (c : α), a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
have mp : (∃ (b : α) (b_1 : α) (b_2 : α), ∃ a ⊆ s, b ≠ b_1 ∧ b ≠ b_2 ∧ b_1 ≠ b_2 ∧ a = {b, b_1, b_2}) →
  ∃ (a : α) (b : α) (c : α), a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
Tactic: constructor