awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ s.ncard = t.ncard ↔ (s \ t).ncard = (t \ s).ncard
have rw : (s ∩ t).ncard + (s \ t).ncard = t.ncard ↔ (s \ t).ncard = (t \ s).ncard
Tactic: rw [← ncard_inter_add_ncard_diff_eq_ncard s t hs, ← ncard_inter_add_ncard_diff_eq_ncard t s ht,
    inter_comm, add_right_inj]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
rw : (s ∩ t).ncard + (s \ t).ncard = t.ncard ↔ (s \ t).ncard = (t \ s).ncard
⊢ s.ncard = t.ncard ↔ (s \ t).ncard = (t \ s).ncard
have rw₁ : (s ∩ t).ncard + (s \ t).ncard = (t ∩ s).ncard + (t \ s).ncard ↔ (s \ t).ncard = (t \ s).ncard
Tactic: rw [← ncard_inter_add_ncard_diff_eq_ncard s t hs, ← ncard_inter_add_ncard_diff_eq_ncard t s ht,
    inter_comm, add_right_inj]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
rw : (s ∩ t).ncard + (s \ t).ncard = t.ncard ↔ (s \ t).ncard = (t \ s).ncard
rw₁ : (s ∩ t).ncard + (s \ t).ncard = (t ∩ s).ncard + (t \ s).ncard ↔ (s \ t).ncard = (t \ s).ncard
⊢ s.ncard = t.ncard ↔ (s \ t).ncard = (t \ s).ncard
have rw₂ : (t ∩ s).ncard + (s \ t).ncard = (t ∩ s).ncard + (t \ s).ncard ↔ (s \ t).ncard = (t \ s).ncard
Tactic: rw [← ncard_inter_add_ncard_diff_eq_ncard s t hs, ← ncard_inter_add_ncard_diff_eq_ncard t s ht,
    inter_comm, add_right_inj]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
rw : (s ∩ t).ncard + (s \ t).ncard = t.ncard ↔ (s \ t).ncard = (t \ s).ncard
rw₁ : (s ∩ t).ncard + (s \ t).ncard = (t ∩ s).ncard + (t \ s).ncard ↔ (s \ t).ncard = (t \ s).ncard
rw₂ : (t ∩ s).ncard + (s \ t).ncard = (t ∩ s).ncard + (t \ s).ncard ↔ (s \ t).ncard = (t \ s).ncard
⊢ s.ncard = t.ncard ↔ (s \ t).ncard = (t \ s).ncard
have rw₃ : (s \ t).ncard = (t \ s).ncard ↔ (s \ t).ncard = (t \ s).ncard
Tactic: rw [← ncard_inter_add_ncard_diff_eq_ncard s t hs, ← ncard_inter_add_ncard_diff_eq_ncard t s ht,
    inter_comm, add_right_inj]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ s.ncard ≤ t.ncard ↔ (s \ t).ncard ≤ (t \ s).ncard
have rw : (s ∩ t).ncard + (s \ t).ncard ≤ t.ncard ↔ (s \ t).ncard ≤ (t \ s).ncard
Tactic: rw [← ncard_inter_add_ncard_diff_eq_ncard s t hs, ← ncard_inter_add_ncard_diff_eq_ncard t s ht,
    inter_comm, add_le_add_iff_left]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
rw : (s ∩ t).ncard + (s \ t).ncard ≤ t.ncard ↔ (s \ t).ncard ≤ (t \ s).ncard
⊢ s.ncard ≤ t.ncard ↔ (s \ t).ncard ≤ (t \ s).ncard
have rw₁ : (s ∩ t).ncard + (s \ t).ncard ≤ (t ∩ s).ncard + (t \ s).ncard ↔ (s \ t).ncard ≤ (t \ s).ncard
Tactic: rw [← ncard_inter_add_ncard_diff_eq_ncard s t hs, ← ncard_inter_add_ncard_diff_eq_ncard t s ht,
    inter_comm, add_le_add_iff_left]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
rw : (s ∩ t).ncard + (s \ t).ncard ≤ t.ncard ↔ (s \ t).ncard ≤ (t \ s).ncard
rw₁ : (s ∩ t).ncard + (s \ t).ncard ≤ (t ∩ s).ncard + (t \ s).ncard ↔ (s \ t).ncard ≤ (t \ s).ncard
⊢ s.ncard ≤ t.ncard ↔ (s \ t).ncard ≤ (t \ s).ncard
have rw₂ : (t ∩ s).ncard + (s \ t).ncard ≤ (t ∩ s).ncard + (t \ s).ncard ↔ (s \ t).ncard ≤ (t \ s).ncard
Tactic: rw [← ncard_inter_add_ncard_diff_eq_ncard s t hs, ← ncard_inter_add_ncard_diff_eq_ncard t s ht,
    inter_comm, add_le_add_iff_left]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
rw : (s ∩ t).ncard + (s \ t).ncard ≤ t.ncard ↔ (s \ t).ncard ≤ (t \ s).ncard
rw₁ : (s ∩ t).ncard + (s \ t).ncard ≤ (t ∩ s).ncard + (t \ s).ncard ↔ (s \ t).ncard ≤ (t \ s).ncard
rw₂ : (t ∩ s).ncard + (s \ t).ncard ≤ (t ∩ s).ncard + (t \ s).ncard ↔ (s \ t).ncard ≤ (t \ s).ncard
⊢ s.ncard ≤ t.ncard ↔ (s \ t).ncard ≤ (t \ s).ncard
have rw₃ : (s \ t).ncard ≤ (t \ s).ncard ↔ (s \ t).ncard ≤ (t \ s).ncard
Tactic: rw [← ncard_inter_add_ncard_diff_eq_ncard s t hs, ← ncard_inter_add_ncard_diff_eq_ncard t s ht,
    inter_comm, add_le_add_iff_left]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ s.ncard < t.ncard ↔ (s \ t).ncard < (t \ s).ncard
have rw : (s ∩ t).ncard + (s \ t).ncard < t.ncard ↔ (s \ t).ncard < (t \ s).ncard
Tactic: rw [← ncard_inter_add_ncard_diff_eq_ncard s t hs, ← ncard_inter_add_ncard_diff_eq_ncard t s ht,
    inter_comm, add_lt_add_iff_left]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
rw : (s ∩ t).ncard + (s \ t).ncard < t.ncard ↔ (s \ t).ncard < (t \ s).ncard
⊢ s.ncard < t.ncard ↔ (s \ t).ncard < (t \ s).ncard
have rw₁ : (s ∩ t).ncard + (s \ t).ncard < (t ∩ s).ncard + (t \ s).ncard ↔ (s \ t).ncard < (t \ s).ncard
Tactic: rw [← ncard_inter_add_ncard_diff_eq_ncard s t hs, ← ncard_inter_add_ncard_diff_eq_ncard t s ht,
    inter_comm, add_lt_add_iff_left]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
rw : (s ∩ t).ncard + (s \ t).ncard < t.ncard ↔ (s \ t).ncard < (t \ s).ncard
rw₁ : (s ∩ t).ncard + (s \ t).ncard < (t ∩ s).ncard + (t \ s).ncard ↔ (s \ t).ncard < (t \ s).ncard
⊢ s.ncard < t.ncard ↔ (s \ t).ncard < (t \ s).ncard
have rw₂ : (t ∩ s).ncard + (s \ t).ncard < (t ∩ s).ncard + (t \ s).ncard ↔ (s \ t).ncard < (t \ s).ncard
Tactic: rw [← ncard_inter_add_ncard_diff_eq_ncard s t hs, ← ncard_inter_add_ncard_diff_eq_ncard t s ht,
    inter_comm, add_lt_add_iff_left]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
rw : (s ∩ t).ncard + (s \ t).ncard < t.ncard ↔ (s \ t).ncard < (t \ s).ncard
rw₁ : (s ∩ t).ncard + (s \ t).ncard < (t ∩ s).ncard + (t \ s).ncard ↔ (s \ t).ncard < (t \ s).ncard
rw₂ : (t ∩ s).ncard + (s \ t).ncard < (t ∩ s).ncard + (t \ s).ncard ↔ (s \ t).ncard < (t \ s).ncard
⊢ s.ncard < t.ncard ↔ (s \ t).ncard < (t \ s).ncard
have rw₃ : (s \ t).ncard < (t \ s).ncard ↔ (s \ t).ncard < (t \ s).ncard
Tactic: rw [← ncard_inter_add_ncard_diff_eq_ncard s t hs, ← ncard_inter_add_ncard_diff_eq_ncard t s ht,
    inter_comm, add_lt_add_iff_left]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
hs : s.Finite
hsc : sᶜ.Finite
⊢ s.ncard + sᶜ.ncard = Nat.card α
have rw : s.ncard + sᶜ.ncard = ncard.{u_1} (α := α) univ
Tactic: rw [← ncard_univ, ← ncard_union_eq (@disjoint_compl_right _ _ s) hs hsc, union_compl_self]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
hs : s.Finite
hsc : sᶜ.Finite
rw : s.ncard + sᶜ.ncard = ncard.{u_1} (α := α) univ
⊢ s.ncard + sᶜ.ncard = Nat.card α
have rw₁ : (s ∪ sᶜ).ncard = ncard.{u_1} (α := α) univ
Tactic: rw [← ncard_univ, ← ncard_union_eq (@disjoint_compl_right _ _ s) hs hsc, union_compl_self]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
hs : s.Finite
hsc : sᶜ.Finite
rw : s.ncard + sᶜ.ncard = ncard.{u_1} (α := α) univ
rw₁ : (s ∪ sᶜ).ncard = ncard.{u_1} (α := α) univ
⊢ s.ncard + sᶜ.ncard = Nat.card α
have rw₂ : ncard.{u_1} (α := α) univ = ncard.{u_1} (α := α) univ
Tactic: rw [← ncard_univ, ← ncard_union_eq (@disjoint_compl_right _ _ s) hs hsc, union_compl_self]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
hs : s.Finite
hsc : sᶜ.Finite
⊢ sᶜ.ncard = Nat.card α - s.ncard
have rw : sᶜ.ncard = s.ncard + sᶜ.ncard - s.ncard
Tactic: rw [← ncard_add_ncard_compl s hs hsc, Nat.add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
hs : s.Finite
hsc : sᶜ.Finite
rw : sᶜ.ncard = s.ncard + sᶜ.ncard - s.ncard
⊢ sᶜ.ncard = Nat.card α - s.ncard
have rw₁ : sᶜ.ncard = sᶜ.ncard
Tactic: rw [← ncard_add_ncard_compl s hs hsc, Nat.add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
inst : Finite α
s : Set α
⊢ s = univ ↔ s.ncard = Nat.card α
have rw : sᶜ = ∅ ↔ s.ncard = Nat.card α
Tactic: rw [← compl_empty_iff, ← ncard_eq_zero, ← ncard_add_ncard_compl s, left_eq_add]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
inst : Finite α
s : Set α
rw : sᶜ = ∅ ↔ s.ncard = Nat.card α
⊢ s = univ ↔ s.ncard = Nat.card α
have rw₁ : sᶜ.ncard = 0 ↔ s.ncard = Nat.card α
Tactic: rw [← compl_empty_iff, ← ncard_eq_zero, ← ncard_add_ncard_compl s, left_eq_add]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
inst : Finite α
s : Set α
rw : sᶜ = ∅ ↔ s.ncard = Nat.card α
rw₁ : sᶜ.ncard = 0 ↔ s.ncard = Nat.card α
⊢ s = univ ↔ s.ncard = Nat.card α
have rw₂ : sᶜ.ncard = 0 ↔ s.ncard = s.ncard + sᶜ.ncard
Tactic: rw [← compl_empty_iff, ← ncard_eq_zero, ← ncard_add_ncard_compl s, left_eq_add]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
inst : Finite α
s : Set α
rw : sᶜ = ∅ ↔ s.ncard = Nat.card α
rw₁ : sᶜ.ncard = 0 ↔ s.ncard = Nat.card α
rw₂ : sᶜ.ncard = 0 ↔ s.ncard = s.ncard + sᶜ.ncard
⊢ s = univ ↔ s.ncard = Nat.card α
have rw₃ : sᶜ.ncard = 0 ↔ sᶜ.ncard = 0
Tactic: rw [← compl_empty_iff, ← ncard_eq_zero, ← ncard_add_ncard_compl s, left_eq_add]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
inst : Finite α
heven : Even (Nat.card α)
s : Set α
⊢ Even sᶜ.ncard ↔ Even s.ncard
have rwa : Even s.ncard ↔ Even sᶜ.ncard
Tactic: rwa [iff_comm, ← Nat.even_add, ncard_add_ncard_compl]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
inst : Finite α
heven : Even (Nat.card α)
s : Set α
rwa : Even s.ncard ↔ Even sᶜ.ncard
⊢ Even sᶜ.ncard ↔ Even s.ncard
have rwa₁ : Even (s.ncard + sᶜ.ncard)
Tactic: rwa [iff_comm, ← Nat.even_add, ncard_add_ncard_compl]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
inst : Finite α
heven : Even (Nat.card α)
s : Set α
⊢ Odd sᶜ.ncard ↔ Odd s.ncard
have rw : ¬Even sᶜ.ncard ↔ Odd s.ncard
Tactic: rw [← Nat.not_even_iff_odd, even_ncard_compl_iff heven, Nat.not_even_iff_odd]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
inst : Finite α
heven : Even (Nat.card α)
s : Set α
rw : ¬Even sᶜ.ncard ↔ Odd s.ncard
⊢ Odd sᶜ.ncard ↔ Odd s.ncard
have rw₁ : ¬Even s.ncard ↔ Odd s.ncard
Tactic: rw [← Nat.not_even_iff_odd, even_ncard_compl_iff heven, Nat.not_even_iff_odd]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
inst : Finite α
heven : Even (Nat.card α)
s : Set α
rw : ¬Even sᶜ.ncard ↔ Odd s.ncard
rw₁ : ¬Even s.ncard ↔ Odd s.ncard
⊢ Odd sᶜ.ncard ↔ Odd s.ncard
have rw₂ : Odd s.ncard ↔ Odd s.ncard
Tactic: rw [← Nat.not_even_iff_odd, even_ncard_compl_iff heven, Nat.not_even_iff_odd]
-- Lean 4 proof step from Mathlib.Data.Set.Card (hypothesis)
Goal:
α : Type u_1
s t : Set α
inst : Finite α
h : Nat.card α < s.ncard + t.ncard
⊢ (s ∩ t).Nonempty
have h₁ : Nat.card α < (s ∪ t).ncard + (s ∩ t).ncard
Tactic: rw [← ncard_union_add_ncard_inter s t] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Set.Card (hypothesis)
Goal:
α : Type u_1
s t : Set α
inst : Finite α
h : Nat.card α < (s ∪ t).ncard + (s ∩ t).ncard
⊢ (s ∩ t).Nonempty
have h₁ : (s ∪ t).ncard < (s ∪ t).ncard + (s ∩ t).ncard
Tactic: replace h := (s ∪ t).ncard_le_card.trans_lt h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
inst : Finite α
h : (s ∪ t).ncard < (s ∪ t).ncard + (s ∩ t).ncard
⊢ (s ∩ t).Nonempty
have rwa : ∀ (h : 0 < (s ∩ t).ncard), (s ∩ t).Nonempty
Tactic: rwa [lt_add_iff_pos_right, ncard_pos] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
inst : Finite α
h : (s ∪ t).ncard < (s ∪ t).ncard + (s ∩ t).ncard
rwa : ∀ (h : 0 < (s ∩ t).ncard), (s ∩ t).Nonempty
⊢ (s ∩ t).Nonempty
have rwa₁ : ∀ (h : (s ∩ t).Nonempty), (s ∩ t).Nonempty
Tactic: rwa [lt_add_iff_pos_right, ncard_pos] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Set.Card (hypothesis)
Goal:
α : Type u_1
s t : Set α
inst : Finite α
h' : Nat.card α ≤ s.ncard + t.ncard
h : s ∪ t ≠ univ
⊢ (s ∩ t).Nonempty
have h'₁ : Nat.card α ≤ (s ∪ t).ncard + (s ∩ t).ncard
Tactic: rw [← ncard_union_add_ncard_inter s t] at h'
Cleared hypotheses: h', h
-- Lean 4 proof step from Mathlib.Data.Set.Card (hypothesis)
Goal:
α : Type u_1
s t : Set α
inst : Finite α
h' : Nat.card α ≤ (s ∪ t).ncard + (s ∩ t).ncard
h : s ∪ t ≠ univ
⊢ (s ∩ t).Nonempty
have h₁ : (s ∪ t).ncard < (s ∪ t).ncard + (s ∩ t).ncard
Tactic: replace h := (ncard_lt_card h).trans_le h'
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
inst : Finite α
h' : Nat.card α ≤ (s ∪ t).ncard + (s ∩ t).ncard
h : (s ∪ t).ncard < (s ∪ t).ncard + (s ∩ t).ncard
⊢ (s ∩ t).Nonempty
have rwa : ∀ (h : 0 < (s ∩ t).ncard), (s ∩ t).Nonempty
Tactic: rwa [lt_add_iff_pos_right, ncard_pos] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
inst : Finite α
h' : Nat.card α ≤ (s ∪ t).ncard + (s ∩ t).ncard
h : (s ∪ t).ncard < (s ∪ t).ncard + (s ∩ t).ncard
rwa : ∀ (h : 0 < (s ∩ t).ncard), (s ∩ t).Nonempty
⊢ (s ∩ t).Nonempty
have rwa₁ : ∀ (h : (s ∩ t).Nonempty), (s ∩ t).Nonempty
Tactic: rwa [lt_add_iff_pos_right, ncard_pos] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
h : s.ncard + t.ncard < Nat.card α
⊢ s ∪ t ≠ univ
have contrapose! : ∀ (h : s ∪ t = univ), Nat.card α ≤ s.ncard + t.ncard
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
h : s ∪ t = univ
⊢ Nat.card α ≤ s.ncard + t.ncard
have rw : (s ∪ t).ncard ≤ s.ncard + t.ncard
Tactic: rw [← ncard_univ, ← h]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
h : s.ncard + t.ncard < Nat.card α
⊢ (sᶜ ∩ tᶜ).Nonempty
have rw : s ∪ t ≠ univ
Tactic: rw [← compl_union, nonempty_compl]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
n : ℕ
hst : s ⊆ t
hsn : s.ncard ≤ n
hnt : n ≤ t.ncard
⊢ ∃ (u : Set α), s ⊆ u ∧ u ⊆ t ∧ u.ncard = n
have inl : ∀ (ht : t.Infinite), ∃ (u : Set α), s ⊆ u ∧ u ⊆ t ∧ u.ncard = n
Tactic: obtain ht | ht := t.infinite_or_finite
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
n : ℕ
hst : s ⊆ t
hsn : s.ncard ≤ n
hnt : n ≤ t.ncard
inl : ∀ (ht : t.Infinite), ∃ (u : Set α), s ⊆ u ∧ u ⊆ t ∧ u.ncard = n
⊢ ∃ (u : Set α), s ⊆ u ∧ u ⊆ t ∧ u.ncard = n
have inr : ∀ (ht : t.Finite), ∃ (u : Set α), s ⊆ u ∧ u ⊆ t ∧ u.ncard = n
Tactic: obtain ht | ht := t.infinite_or_finite
-- Lean 4 proof step from Mathlib.Data.Set.Card (hypothesis)
Goal:
α : Type u_1
s t : Set α
n : ℕ
hst : s ⊆ t
hsn : s.ncard ≤ n
hnt : n ≤ t.ncard
ht : t.Infinite
⊢ ∃ (u : Set α), s ⊆ u ∧ u ⊆ t ∧ u.ncard = n
have hnt₁ : n = t.ncard
Tactic: rw [ht.ncard, Nat.le_zero, ← ht.ncard] at hnt
Cleared hypotheses: hnt, ht
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
n : ℕ
hst : s ⊆ t
hsn : s.ncard ≤ n
hnt : n ≤ t.ncard
ht : t.Finite
⊢ ∃ (u : Set α), s ⊆ u ∧ u ⊆ t ∧ u.ncard = n
have inr : ∀ (s : Finset α) (hst : (↑s : Set α) ⊆ t) (hsn : (↑s : Set α).ncard ≤ n),
  ∃ (u : Set α), (↑s : Set α) ⊆ u ∧ u ⊆ t ∧ u.ncard = n
Tactic: lift s to Finset α using ht.subset hst
Cleared hypotheses: s, hst, hsn
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
t : Set α
n : ℕ
hnt : n ≤ t.ncard
ht : t.Finite
s : Finset α
hst : (↑s : Set α) ⊆ t
hsn : (↑s : Set α).ncard ≤ n
⊢ ∃ (u : Set α), (↑s : Set α) ⊆ u ∧ u ⊆ t ∧ u.ncard = n
have inr : ∀ (t : Finset α) (hnt : n ≤ (↑t : Set α).ncard) (hst : (↑s : Set α) ⊆ (↑t : Set α)),
  ∃ (u : Set α), (↑s : Set α) ⊆ u ∧ u ⊆ (↑t : Set α) ∧ u.ncard = n
Tactic: lift t to Finset α using ht
Cleared hypotheses: t, hnt, ht, hst
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
n : ℕ
s : Finset α
hsn : (↑s : Set α).ncard ≤ n
t : Finset α
hnt : n ≤ (↑t : Set α).ncard
hst : (↑s : Set α) ⊆ (↑t : Set α)
⊢ ∃ (u : Set α), (↑s : Set α) ⊆ u ∧ u ⊆ (↑t : Set α) ∧ u.ncard = n
have inr : ∀ (u : Finset α) (hsu : s ⊆ u) (hut : u ⊆ t) (hu : u.card = n),
  ∃ (u : Set α), (↑s : Set α) ⊆ u ∧ u ⊆ (↑t : Set α) ∧ u.ncard = n
Tactic: obtain ⟨u, hsu, hut, hu⟩ := Finset.exists_subsuperset_card_eq (mod_cast hst) (by simpa using hsn)
    (mod_cast hnt)
-- Lean 4 proof step from Mathlib.Data.Set.Card (hypothesis)
Goal:
α : Type u_1
s : Set α
hs : s.Infinite
k : ℕ
⊢ ∃ t ⊆ s, t.Finite ∧ t.ncard = k
have this : Infinite.{u_1 + 1} (↑s : Type u_1)
Tactic: have := hs.to_subtype
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
hs : s.Infinite
k : ℕ
this : Infinite.{u_1 + 1} (↑s : Type u_1)
⊢ ∃ t ⊆ s, t.Finite ∧ t.ncard = k
have obtain : ∀ (t' : Finset (↑s : Type u_1)), ∃ t ⊆ s, t.Finite ∧ t.ncard = t'.card
Tactic: obtain ⟨t', -, rfl⟩ := @Infinite.exists_subset_card_eq s univ infinite_univ k
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
hs : s.Infinite
this : Infinite.{u_1 + 1} (↑s : Type u_1)
t' : Finset (↑s : Type u_1)
⊢ ∃ t ⊆ s, t.Finite ∧ t.ncard = t'.card
have refine : (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' (↑t' : Set (↑s : Type u_1))).ncard = t'.card
Tactic: refine ⟨Subtype.val '' (t' : Set s), by simp, Finite.image _ (by simp), ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
hs : s.Infinite
this : Infinite.{u_1 + 1} (↑s : Type u_1)
t' : Finset (↑s : Type u_1)
⊢ (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' (↑t' : Set (↑s : Type u_1))).ncard = t'.card
have rw : (↑t' : Set (↑s : Type u_1)).ncard = t'.card
Tactic: rw [ncard_image_of_injective _ Subtype.coe_injective]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
ht : t.Infinite
hst : s ⊆ t
hs : s.Finite
k : ℕ
hsk : s.ncard ≤ k
⊢ ∃ (s' : Set α), s ⊆ s' ∧ s' ⊆ t ∧ s'.ncard = k
have obtain : ∀ (s₁ : Set α) (hs₁ : s₁ ⊆ t \ s) (hs₁fin : s₁.Finite) (hs₁card : s₁.ncard = k - s.ncard),
  ∃ (s' : Set α), s ⊆ s' ∧ s' ⊆ t ∧ s'.ncard = k
Tactic: obtain ⟨s₁, hs₁, hs₁fin, hs₁card⟩ := (ht.diff hs).exists_subset_ncard_eq (k - s.ncard)
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
ht : t.Infinite
hst : s ⊆ t
hs : s.Finite
k : ℕ
hsk : s.ncard ≤ k
s₁ : Set α
hs₁ : s₁ ⊆ t \ s
hs₁fin : s₁.Finite
hs₁card : s₁.ncard = k - s.ncard
⊢ ∃ (s' : Set α), s ⊆ s' ∧ s' ⊆ t ∧ s'.ncard = k
have refine : (s ∪ s₁).ncard = k
Tactic: refine ⟨s ∪ s₁, subset_union_left, union_subset hst (hs₁.trans diff_subset), ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
ht : t.Infinite
hst : s ⊆ t
hs : s.Finite
k : ℕ
hsk : s.ncard ≤ k
s₁ : Set α
hs₁ : s₁ ⊆ t \ s
hs₁fin : s₁.Finite
hs₁card : s₁.ncard = k - s.ncard
⊢ (s ∪ s₁).ncard = k
have rwa : s.ncard + s₁.ncard = k
Tactic: rwa [ncard_union_eq (disjoint_of_subset_right hs₁ disjoint_sdiff_right) hs hs₁fin, hs₁card,
    add_tsub_cancel_of_le]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
ht : t.Infinite
hst : s ⊆ t
hs : s.Finite
k : ℕ
hsk : s.ncard ≤ k
s₁ : Set α
hs₁ : s₁ ⊆ t \ s
hs₁fin : s₁.Finite
hs₁card : s₁.ncard = k - s.ncard
rwa : s.ncard + s₁.ncard = k
⊢ (s ∪ s₁).ncard = k
have rwa₁ : s.ncard + (k - s.ncard) = k
Tactic: rwa [ncard_union_eq (disjoint_of_subset_right hs₁ disjoint_sdiff_right) hs hs₁fin, hs₁card,
    add_tsub_cancel_of_le]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
ht : t.Infinite
hst : s ⊆ t
hs : s.Finite
k : ℕ
hsk : s.ncard ≤ k
s₁ : Set α
hs₁ : s₁ ⊆ t \ s
hs₁fin : s₁.Finite
hs₁card : s₁.ncard = k - s.ncard
rwa : s.ncard + s₁.ncard = k
rwa₁ : s.ncard + (k - s.ncard) = k
⊢ (s ∪ s₁).ncard = k
have rwa₂ : k = k
Tactic: rwa [ncard_union_eq (disjoint_of_subset_right hs₁ disjoint_sdiff_right) hs hs₁fin, hs₁card,
    add_tsub_cancel_of_le]
-- Lean 4 proof step from Mathlib.Data.Set.Card (hypothesis)
Goal:
α : Type u_1
s t : Set α
n : ℕ
hst : 2 * n < (s ∪ t).ncard
⊢ ∃ (r : Set α), n < r.ncard ∧ (r ⊆ s ∨ r ⊆ t)
have hu : (s ∪ t).Finite
Tactic: have hu := finite_of_ncard_ne_zero ((Nat.zero_le _).trans_lt hst).ne.symm
-- Lean 4 proof step from Mathlib.Data.Set.Card (hypothesis)
Goal:
α : Type u_1
s t : Set α
n : ℕ
hst : 2 * n < (s ∪ t).ncard
hu : (s ∪ t).Finite
⊢ ∃ (r : Set α), n < r.ncard ∧ (r ⊆ s ∨ r ⊆ t)
have hst₁ : 2 * n < (sorry.toFinset (s := s) ∪ sorry.toFinset (s := t)).card
Tactic: rw [ncard_eq_toFinset_card _ hu,
    Finite.toFinset_union (hu.subset subset_union_left)
      (hu.subset subset_union_right)] at hst
Cleared hypotheses: hst
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
n : ℕ
hu : (s ∪ t).Finite
hst : 2 * n < (⋯.toFinset (s := s) ∪ ⋯.toFinset (s := t)).card
⊢ ∃ (r : Set α), n < r.ncard ∧ (r ⊆ s ∨ r ⊆ t)
have obtain : ∀ (r' : Finset α) (hnr' : n < r'.card) (hr' : r' ⊆ sorry.toFinset (s := s) ∨ r' ⊆ sorry.toFinset (s := t)),
  ∃ (r : Set α), n < r.ncard ∧ (r ⊆ s ∨ r ⊆ t)
Tactic: obtain ⟨r', hnr', hr'⟩ := Finset.exists_subset_or_subset_of_two_mul_lt_card hst
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
n : ℕ
hst : 2 * n < (s ∪ t).ncard
⊢ ∃ (r : Set α), n < r.ncard ∧ (r ⊆ s ∨ r ⊆ t)
have have : ∀ (hu : (s ∪ t).Finite), ∃ (r : Set α), n < r.ncard ∧ (r ⊆ s ∨ r ⊆ t)
Tactic: classical
  have hu := finite_of_ncard_ne_zero ((Nat.zero_le _).trans_lt hst).ne.symm
  rw [ncard_eq_toFinset_card _ hu,
    Finite.toFinset_union (hu.subset subset_union_left)
      (hu.subset subset_union_right)] at hst
  obtain ⟨r', hnr', hr'⟩ := Finset.exists_subset_or_subset_of_two_mul_lt_card hst
  exact ⟨r', by simpa, by simpa using hr'⟩
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
n : ℕ
hst : 2 * n < (s ∪ t).ncard
have have₁ have₂ : ∀ (hu : (s ∪ t).Finite), ∃ (r : Set α), n < r.ncard ∧ (r ⊆ s ∨ r ⊆ t)
⊢ ∃ (r : Set α), n < r.ncard ∧ (r ⊆ s ∨ r ⊆ t)
have have₃ : ∀ (hu : (s ∪ t).Finite) (hst : 2 * n < (sorry.toFinset (s := s) ∪ sorry.toFinset (s := t)).card),
  ∃ (r : Set α), n < r.ncard ∧ (r ⊆ s ∨ r ⊆ t)
Tactic: classical
  have hu := finite_of_ncard_ne_zero ((Nat.zero_le _).trans_lt hst).ne.symm
  rw [ncard_eq_toFinset_card _ hu,
    Finite.toFinset_union (hu.subset subset_union_left)
      (hu.subset subset_union_right)] at hst
  obtain ⟨r', hnr', hr'⟩ := Finset.exists_subset_or_subset_of_two_mul_lt_card hst
  exact ⟨r', by simpa, by simpa using hr'⟩
Cleared hypotheses: hst
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
n : ℕ
hst : 2 * n < (s ∪ t).ncard
have have₁ have₂ : ∀ (hu : (s ∪ t).Finite), ∃ (r : Set α), n < r.ncard ∧ (r ⊆ s ∨ r ⊆ t)
have₃ :
  ∀ (hu : (s ∪ t).Finite) (hst : 2 * n < (⋯.toFinset (s := s) ∪ ⋯.toFinset (s := t)).card),
    ∃ (r : Set α), n < r.ncard ∧ (r ⊆ s ∨ r ⊆ t)
⊢ ∃ (r : Set α), n < r.ncard ∧ (r ⊆ s ∨ r ⊆ t)
have have₄ : ∀ (hu : (s ∪ t).Finite) (hst : 2 * n < (sorry.toFinset (s := s) ∪ sorry.toFinset (s := t)).card) (r' : Finset α)
  (hnr' : n < r'.card) (hr' : r' ⊆ sorry.toFinset (s := s) ∨ r' ⊆ sorry.toFinset (s := t)),
  ∃ (r : Set α), n < r.ncard ∧ (r ⊆ s ∨ r ⊆ t)
Tactic: classical
  have hu := finite_of_ncard_ne_zero ((Nat.zero_le _).trans_lt hst).ne.symm
  rw [ncard_eq_toFinset_card _ hu,
    Finite.toFinset_union (hu.subset subset_union_left)
      (hu.subset subset_union_right)] at hst
  obtain ⟨r', hnr', hr'⟩ := Finset.exists_subset_or_subset_of_two_mul_lt_card hst
  exact ⟨r', by simpa, by simpa using hr'⟩
Cleared hypotheses: hst
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Finset α
hs : (↑s.card : ℕ∞) < ENat.card α
⊢ ∃ (a : α), a ∉ s
have contrapose! : ∀ (hs : ∀ (a : α), a ∈ s), ENat.card α ≤ (↑s.card : ℕ∞)
Tactic: contrapose! hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
a : α
⊢ ncard (α := α) {a} = 1
have rw : Eq (α := ℕ) 1 1
Tactic: rw [ncard_singleton]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s : Set α
⊢ s.ncard = 1 ↔ ∃ (a : α), s = {a}
have refine : ∀ (h : s.ncard = 1), ∃ (a : α), s = {a}
Tactic: refine ⟨fun h ↦ ?_, by rintro ⟨a, rfl⟩; rw [ncard_singleton]⟩