awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj_1 : ∀ b ∈ t, ∃ (a : α) (ha : a ∈ s), f a ha = b
hst : s.ncard ≤ t.ncard
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : s.Finite
f' : (↑s : Type u_1) → (↑t : Type u_2) :=
  fun (x : (↑s : Type u_1)) ↦ Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f (↑x : α) ⋯) ⋯
hsurj : Function.Surjective f'
this_1 : Fintype (↑s : Type u_1)
this : Fintype (↑t : Type u_2)
f'' : (a : α) → a ∈ s.toFinset → β := fun (a : α) (h : a ∈ s.toFinset) ↦ f a ⋯
⊢ s.toFinset.card ≤ t.toFinset.card
have rwa : s.ncard ≤ t.toFinset.card
Tactic: rwa [← ncard_eq_toFinset_card', ← ncard_eq_toFinset_card']
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj_1 : ∀ b ∈ t, ∃ (a : α) (ha : a ∈ s), f a ha = b
hst : s.ncard ≤ t.ncard
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : s.Finite
f' : (↑s : Type u_1) → (↑t : Type u_2) :=
  fun (x : (↑s : Type u_1)) ↦ Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f (↑x : α) ⋯) ⋯
hsurj : Function.Surjective f'
this_1 : Fintype (↑s : Type u_1)
this : Fintype (↑t : Type u_2)
f'' : (a : α) → a ∈ s.toFinset → β := fun (a : α) (h : a ∈ s.toFinset) ↦ f a ⋯
⊢ s.toFinset.card ≤ t.toFinset.card
have rwa : s.ncard ≤ t.toFinset.card
Tactic: { rwa [← ncard_eq_toFinset_card', ← ncard_eq_toFinset_card'] }
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj : ∀ b ∈ t, ∃ (a : α) (ha : a ∈ s), f a ha = b
hst : s.ncard ≤ t.ncard
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : s.Finite
set set₁ : a₁ = a₂
⊢ a₁ = a₂
have set₂ : let f' : (↑s : Type u_1) → (↑t : Type u_2) := fun (x : (↑s : Type u_1)) ↦
  Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f (↑x : α) sorry) sorry;
∀ (hsurj : Function.Surjective f'), a₁ = a₂
Tactic: classical
  set f' : s → t := fun x ↦ ⟨f x.1 x.2, hf _ _⟩
  have hsurj : f'.Surjective := by
    rintro ⟨y, hy⟩
    obtain ⟨a, ha, rfl⟩ := hsurj y hy
    simp only [Subtype.exists]
    exact ⟨_, ha, rfl⟩
  haveI := hs.fintype
  haveI := Fintype.ofSurjective _ hsurj
  set f'' : ∀ a, a ∈ s.toFinset → β := fun a h ↦ f a (by simpa using h)
  exact
    @Finset.inj_on_of_surj_on_of_card_le _ _ _ t.toFinset f''
      (fun a ha ↦ by { rw [mem_toFinset] at ha ⊢; exact hf a ha }) (by simpa)
      (by { rwa [← ncard_eq_toFinset_card', ← ncard_eq_toFinset_card'] }) a₁
      (by simpa) a₂ (by simpa) (by simpa)
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj : ∀ b ∈ t, ∃ (a : α) (ha : a ∈ s), f a ha = b
hst : s.ncard ≤ t.ncard
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : s.Finite
set set₁ : a₁ = a₂
set₂ :
  let f' : (↑s : Type u_1) → (↑t : Type u_2) := fun (x : (↑s : Type u_1)) ↦
    Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f (↑x : α) ⋯) ⋯;
  ∀ (hsurj : Function.Surjective f'), a₁ = a₂
⊢ a₁ = a₂
have set₃ : let f' : (↑s : Type u_1) → (↑t : Type u_2) := fun (x : (↑s : Type u_1)) ↦
  Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f (↑x : α) sorry) sorry;
∀ (hsurj : Function.Surjective f') (this : Fintype (↑s : Type u_1)), a₁ = a₂
Tactic: classical
  set f' : s → t := fun x ↦ ⟨f x.1 x.2, hf _ _⟩
  have hsurj : f'.Surjective := by
    rintro ⟨y, hy⟩
    obtain ⟨a, ha, rfl⟩ := hsurj y hy
    simp only [Subtype.exists]
    exact ⟨_, ha, rfl⟩
  haveI := hs.fintype
  haveI := Fintype.ofSurjective _ hsurj
  set f'' : ∀ a, a ∈ s.toFinset → β := fun a h ↦ f a (by simpa using h)
  exact
    @Finset.inj_on_of_surj_on_of_card_le _ _ _ t.toFinset f''
      (fun a ha ↦ by { rw [mem_toFinset] at ha ⊢; exact hf a ha }) (by simpa)
      (by { rwa [← ncard_eq_toFinset_card', ← ncard_eq_toFinset_card'] }) a₁
      (by simpa) a₂ (by simpa) (by simpa)
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : (a : α) → a ∈ s → β
hf : ∀ (a : α) (ha : a ∈ s), f a ha ∈ t
hsurj : ∀ b ∈ t, ∃ (a : α) (ha : a ∈ s), f a ha = b
hst : s.ncard ≤ t.ncard
a₁ : α
ha₁ : a₁ ∈ s
a₂ : α
ha₂ : a₂ ∈ s
ha₁a₂ : f a₁ ha₁ = f a₂ ha₂
hs : s.Finite
set set₁ : a₁ = a₂
set₂ :
  let f' : (↑s : Type u_1) → (↑t : Type u_2) := fun (x : (↑s : Type u_1)) ↦
    Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f (↑x : α) ⋯) ⋯;
  ∀ (hsurj : Function.Surjective f'), a₁ = a₂
set₃ :
  let f' : (↑s : Type u_1) → (↑t : Type u_2) := fun (x : (↑s : Type u_1)) ↦
    Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f (↑x : α) ⋯) ⋯;
  ∀ (hsurj : Function.Surjective f') (this : Fintype (↑s : Type u_1)), a₁ = a₂
⊢ a₁ = a₂
have set₄ : let f' : (↑s : Type u_1) → (↑t : Type u_2) := fun (x : (↑s : Type u_1)) ↦
  Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f (↑x : α) sorry) sorry;
∀ (hsurj : Function.Surjective f') (this : Fintype (↑s : Type u_1)) (this : Fintype (↑t : Type u_2)), a₁ = a₂
Tactic: classical
  set f' : s → t := fun x ↦ ⟨f x.1 x.2, hf _ _⟩
  have hsurj : f'.Surjective := by
    rintro ⟨y, hy⟩
    obtain ⟨a, ha, rfl⟩ := hsurj y hy
    simp only [Subtype.exists]
    exact ⟨_, ha, rfl⟩
  haveI := hs.fintype
  haveI := Fintype.ofSurjective _ hsurj
  set f'' : ∀ a, a ∈ s.toFinset → β := fun a h ↦ f a (by simpa using h)
  exact
    @Finset.inj_on_of_surj_on_of_card_le _ _ _ t.toFinset f''
      (fun a ha ↦ by { rw [mem_toFinset] at ha ⊢; exact hf a ha }) (by simpa)
      (by { rwa [← ncard_eq_toFinset_card', ← ncard_eq_toFinset_card'] }) a₁
      (by simpa) a₂ (by simpa) (by simpa)
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
⊢ (graphOn f s).ncard = s.ncard
have rw : (Prod.fst '' graphOn f s).ncard = s.ncard
Tactic: rw [← fst_injOn_graph.ncard_image, image_fst_graphOn]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
rw : (Prod.fst '' graphOn f s).ncard = s.ncard
⊢ (graphOn f s).ncard = s.ncard
have rw₁ : s.ncard = s.ncard
Tactic: rw [← fst_injOn_graph.ncard_image, image_fst_graphOn]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ (s ∪ t).ncard + (s ∩ t).ncard = s.ncard + t.ncard
have to_encard_tac : HAdd.hAdd (α := ℕ∞) (↑(s ∪ t).ncard : ℕ∞) (↑(s ∩ t).ncard : ℕ∞) = HAdd.hAdd (α := ℕ∞) (↑s.ncard : ℕ∞) (↑t.ncard : ℕ∞)
Tactic: to_encard_tac
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ HAdd.hAdd (α := ℕ∞) (↑(s ∪ t).ncard : ℕ∞) (↑(s ∩ t).ncard : ℕ∞) = HAdd.hAdd (α := ℕ∞) (↑s.ncard : ℕ∞) (↑t.ncard : ℕ∞)
have rw : HAdd.hAdd (α := ℕ∞) (↑(s ∪ t).ncard : ℕ∞) (↑(s ∩ t).ncard : ℕ∞) = s.encard + (↑t.ncard : ℕ∞)
Tactic: rw [hs.cast_ncard_eq, ht.cast_ncard_eq, (hs.union ht).cast_ncard_eq,
    (hs.subset inter_subset_left).cast_ncard_eq, encard_union_add_encard_inter]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
rw : HAdd.hAdd (α := ℕ∞) (↑(s ∪ t).ncard : ℕ∞) (↑(s ∩ t).ncard : ℕ∞) = s.encard + (↑t.ncard : ℕ∞)
⊢ HAdd.hAdd (α := ℕ∞) (↑(s ∪ t).ncard : ℕ∞) (↑(s ∩ t).ncard : ℕ∞) = HAdd.hAdd (α := ℕ∞) (↑s.ncard : ℕ∞) (↑t.ncard : ℕ∞)
have rw₁ : HAdd.hAdd (α := ℕ∞) (↑(s ∪ t).ncard : ℕ∞) (↑(s ∩ t).ncard : ℕ∞) = s.encard + t.encard
Tactic: rw [hs.cast_ncard_eq, ht.cast_ncard_eq, (hs.union ht).cast_ncard_eq,
    (hs.subset inter_subset_left).cast_ncard_eq, encard_union_add_encard_inter]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
rw : HAdd.hAdd (α := ℕ∞) (↑(s ∪ t).ncard : ℕ∞) (↑(s ∩ t).ncard : ℕ∞) = s.encard + (↑t.ncard : ℕ∞)
rw₁ : HAdd.hAdd (α := ℕ∞) (↑(s ∪ t).ncard : ℕ∞) (↑(s ∩ t).ncard : ℕ∞) = s.encard + t.encard
⊢ HAdd.hAdd (α := ℕ∞) (↑(s ∪ t).ncard : ℕ∞) (↑(s ∩ t).ncard : ℕ∞) = HAdd.hAdd (α := ℕ∞) (↑s.ncard : ℕ∞) (↑t.ncard : ℕ∞)
have rw₂ : (s ∪ t).encard + (↑(s ∩ t).ncard : ℕ∞) = s.encard + t.encard
Tactic: rw [hs.cast_ncard_eq, ht.cast_ncard_eq, (hs.union ht).cast_ncard_eq,
    (hs.subset inter_subset_left).cast_ncard_eq, encard_union_add_encard_inter]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
rw : HAdd.hAdd (α := ℕ∞) (↑(s ∪ t).ncard : ℕ∞) (↑(s ∩ t).ncard : ℕ∞) = s.encard + (↑t.ncard : ℕ∞)
rw₁ : HAdd.hAdd (α := ℕ∞) (↑(s ∪ t).ncard : ℕ∞) (↑(s ∩ t).ncard : ℕ∞) = s.encard + t.encard
rw₂ : (s ∪ t).encard + (↑(s ∩ t).ncard : ℕ∞) = s.encard + t.encard
⊢ HAdd.hAdd (α := ℕ∞) (↑(s ∪ t).ncard : ℕ∞) (↑(s ∩ t).ncard : ℕ∞) = HAdd.hAdd (α := ℕ∞) (↑s.ncard : ℕ∞) (↑t.ncard : ℕ∞)
have rw₃ : (s ∪ t).encard + (s ∩ t).encard = s.encard + t.encard
Tactic: rw [hs.cast_ncard_eq, ht.cast_ncard_eq, (hs.union ht).cast_ncard_eq,
    (hs.subset inter_subset_left).cast_ncard_eq, encard_union_add_encard_inter]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
rw : HAdd.hAdd (α := ℕ∞) (↑(s ∪ t).ncard : ℕ∞) (↑(s ∩ t).ncard : ℕ∞) = s.encard + (↑t.ncard : ℕ∞)
rw₁ : HAdd.hAdd (α := ℕ∞) (↑(s ∪ t).ncard : ℕ∞) (↑(s ∩ t).ncard : ℕ∞) = s.encard + t.encard
rw₂ : (s ∪ t).encard + (↑(s ∩ t).ncard : ℕ∞) = s.encard + t.encard
rw₃ : (s ∪ t).encard + (s ∩ t).encard = s.encard + t.encard
⊢ HAdd.hAdd (α := ℕ∞) (↑(s ∪ t).ncard : ℕ∞) (↑(s ∩ t).ncard : ℕ∞) = HAdd.hAdd (α := ℕ∞) (↑s.ncard : ℕ∞) (↑t.ncard : ℕ∞)
have rw₄ : s.encard + t.encard = s.encard + t.encard
Tactic: rw [hs.cast_ncard_eq, ht.cast_ncard_eq, (hs.union ht).cast_ncard_eq,
    (hs.subset inter_subset_left).cast_ncard_eq, encard_union_add_encard_inter]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ (s ∩ t).ncard + (s ∪ t).ncard = s.ncard + t.ncard
have rw : (s ∪ t).ncard + (s ∩ t).ncard = s.ncard + t.ncard
Tactic: rw [add_comm, ncard_union_add_ncard_inter _ _ hs ht]
-- 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 = s.ncard + t.ncard
⊢ (s ∩ t).ncard + (s ∪ t).ncard = s.ncard + t.ncard
have rw₁ : s.ncard + t.ncard = s.ncard + t.ncard
Tactic: rw [add_comm, ncard_union_add_ncard_inter _ _ hs ht]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
⊢ (s ∪ t).ncard ≤ s.ncard + t.ncard
have inl : ∀ (h : (s ∪ t).Finite), (s ∪ t).ncard ≤ s.ncard + t.ncard
Tactic: obtain (h | h) := (s ∪ t).finite_or_infinite
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
inl : ∀ (h : (s ∪ t).Finite), (s ∪ t).ncard ≤ s.ncard + t.ncard
⊢ (s ∪ t).ncard ≤ s.ncard + t.ncard
have inr : ∀ (h : (s ∪ t).Infinite), (s ∪ t).ncard ≤ s.ncard + t.ncard
Tactic: obtain (h | h) := (s ∪ t).finite_or_infinite
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
h : (s ∪ t).Finite
⊢ (s ∪ t).ncard ≤ s.ncard + t.ncard
have inl : (↑(s ∪ t).ncard : ℕ∞) ≤ HAdd.hAdd (α := ℕ∞) (↑s.ncard : ℕ∞) (↑t.ncard : ℕ∞)
Tactic: to_encard_tac
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
h : (s ∪ t).Finite
⊢ (↑(s ∪ t).ncard : ℕ∞) ≤ HAdd.hAdd (α := ℕ∞) (↑s.ncard : ℕ∞) (↑t.ncard : ℕ∞)
have inl : (s ∪ t).encard ≤ s.encard + t.encard
Tactic: rw [h.cast_ncard_eq, (h.subset subset_union_left).cast_ncard_eq,
      (h.subset subset_union_right).cast_ncard_eq]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
h : (s ∪ t).Infinite
⊢ (s ∪ t).ncard ≤ s.ncard + t.ncard
have inr : 0 ≤ s.ncard + t.ncard
Tactic: rw [h.ncard]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
h : Disjoint s t
hs : s.Finite
ht : t.Finite
⊢ (s ∪ t).ncard = s.ncard + t.ncard
have to_encard_tac : (↑(s ∪ t).ncard : ℕ∞) = HAdd.hAdd (α := ℕ∞) (↑s.ncard : ℕ∞) (↑t.ncard : ℕ∞)
Tactic: to_encard_tac
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
h : Disjoint s t
hs : s.Finite
ht : t.Finite
⊢ (↑(s ∪ t).ncard : ℕ∞) = HAdd.hAdd (α := ℕ∞) (↑s.ncard : ℕ∞) (↑t.ncard : ℕ∞)
have rw : (↑(s ∪ t).ncard : ℕ∞) = s.encard + (↑t.ncard : ℕ∞)
Tactic: rw [hs.cast_ncard_eq, ht.cast_ncard_eq, (hs.union ht).cast_ncard_eq, encard_union_eq h]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
h : Disjoint s t
hs : s.Finite
ht : t.Finite
rw : (↑(s ∪ t).ncard : ℕ∞) = s.encard + (↑t.ncard : ℕ∞)
⊢ (↑(s ∪ t).ncard : ℕ∞) = HAdd.hAdd (α := ℕ∞) (↑s.ncard : ℕ∞) (↑t.ncard : ℕ∞)
have rw₁ : (↑(s ∪ t).ncard : ℕ∞) = s.encard + t.encard
Tactic: rw [hs.cast_ncard_eq, ht.cast_ncard_eq, (hs.union ht).cast_ncard_eq, encard_union_eq h]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
h : Disjoint s t
hs : s.Finite
ht : t.Finite
rw : (↑(s ∪ t).ncard : ℕ∞) = s.encard + (↑t.ncard : ℕ∞)
rw₁ : (↑(s ∪ t).ncard : ℕ∞) = s.encard + t.encard
⊢ (↑(s ∪ t).ncard : ℕ∞) = HAdd.hAdd (α := ℕ∞) (↑s.ncard : ℕ∞) (↑t.ncard : ℕ∞)
have rw₂ : (s ∪ t).encard = s.encard + t.encard
Tactic: rw [hs.cast_ncard_eq, ht.cast_ncard_eq, (hs.union ht).cast_ncard_eq, encard_union_eq h]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
h : Disjoint s t
hs : s.Finite
ht : t.Finite
rw : (↑(s ∪ t).ncard : ℕ∞) = s.encard + (↑t.ncard : ℕ∞)
rw₁ : (↑(s ∪ t).ncard : ℕ∞) = s.encard + t.encard
rw₂ : (s ∪ t).encard = s.encard + t.encard
⊢ (↑(s ∪ t).ncard : ℕ∞) = HAdd.hAdd (α := ℕ∞) (↑s.ncard : ℕ∞) (↑t.ncard : ℕ∞)
have rw₃ : s.encard + t.encard = s.encard + t.encard
Tactic: rw [hs.cast_ncard_eq, ht.cast_ncard_eq, (hs.union ht).cast_ncard_eq, encard_union_eq h]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ (s ∪ t).ncard = s.ncard + t.ncard ↔ Disjoint s t
have rw : (s ∪ t).ncard = (s ∪ t).ncard + (s ∩ t).ncard ↔ Disjoint s t
Tactic: rw [← ncard_union_add_ncard_inter s t hs ht, left_eq_add,
    ncard_eq_zero (hs.inter_of_left t), disjoint_iff_inter_eq_empty]
-- 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 + (s ∩ t).ncard ↔ Disjoint s t
⊢ (s ∪ t).ncard = s.ncard + t.ncard ↔ Disjoint s t
have rw₁ : (s ∩ t).ncard = 0 ↔ Disjoint s t
Tactic: rw [← ncard_union_add_ncard_inter s t hs ht, left_eq_add,
    ncard_eq_zero (hs.inter_of_left t), disjoint_iff_inter_eq_empty]
-- 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 + (s ∩ t).ncard ↔ Disjoint s t
rw₁ : (s ∩ t).ncard = 0 ↔ Disjoint s t
⊢ (s ∪ t).ncard = s.ncard + t.ncard ↔ Disjoint s t
have rw₂ : s ∩ t = ∅ ↔ Disjoint s t
Tactic: rw [← ncard_union_add_ncard_inter s t hs ht, left_eq_add,
    ncard_eq_zero (hs.inter_of_left t), disjoint_iff_inter_eq_empty]
-- 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 + (s ∩ t).ncard ↔ Disjoint s t
rw₁ : (s ∩ t).ncard = 0 ↔ Disjoint s t
rw₂ : s ∩ t = ∅ ↔ Disjoint s t
⊢ (s ∪ t).ncard = s.ncard + t.ncard ↔ Disjoint s t
have rw₃ : s ∩ t = ∅ ↔ s ∩ t = ∅
Tactic: rw [← ncard_union_add_ncard_inter s t hs ht, left_eq_add,
    ncard_eq_zero (hs.inter_of_left t), disjoint_iff_inter_eq_empty]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
h : s ⊆ t
ht : t.Finite
⊢ (t \ s).ncard + s.ncard = t.ncard
have to_encard_tac : HAdd.hAdd (α := ℕ∞) (↑(t \ s).ncard : ℕ∞) (↑s.ncard : ℕ∞) = (↑t.ncard : ℕ∞)
Tactic: to_encard_tac
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
h : s ⊆ t
ht : t.Finite
⊢ HAdd.hAdd (α := ℕ∞) (↑(t \ s).ncard : ℕ∞) (↑s.ncard : ℕ∞) = (↑t.ncard : ℕ∞)
have rw : HAdd.hAdd (α := ℕ∞) (↑(t \ s).ncard : ℕ∞) (↑s.ncard : ℕ∞) = t.encard
Tactic: rw [ht.cast_ncard_eq, (ht.subset h).cast_ncard_eq, ht.diff.cast_ncard_eq,
    encard_diff_add_encard_of_subset h]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
h : s ⊆ t
ht : t.Finite
rw : HAdd.hAdd (α := ℕ∞) (↑(t \ s).ncard : ℕ∞) (↑s.ncard : ℕ∞) = t.encard
⊢ HAdd.hAdd (α := ℕ∞) (↑(t \ s).ncard : ℕ∞) (↑s.ncard : ℕ∞) = (↑t.ncard : ℕ∞)
have rw₁ : (↑(t \ s).ncard : ℕ∞) + s.encard = t.encard
Tactic: rw [ht.cast_ncard_eq, (ht.subset h).cast_ncard_eq, ht.diff.cast_ncard_eq,
    encard_diff_add_encard_of_subset h]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
h : s ⊆ t
ht : t.Finite
rw : HAdd.hAdd (α := ℕ∞) (↑(t \ s).ncard : ℕ∞) (↑s.ncard : ℕ∞) = t.encard
rw₁ : (↑(t \ s).ncard : ℕ∞) + s.encard = t.encard
⊢ HAdd.hAdd (α := ℕ∞) (↑(t \ s).ncard : ℕ∞) (↑s.ncard : ℕ∞) = (↑t.ncard : ℕ∞)
have rw₂ : (t \ s).encard + s.encard = t.encard
Tactic: rw [ht.cast_ncard_eq, (ht.subset h).cast_ncard_eq, ht.diff.cast_ncard_eq,
    encard_diff_add_encard_of_subset h]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
h : s ⊆ t
ht : t.Finite
rw : HAdd.hAdd (α := ℕ∞) (↑(t \ s).ncard : ℕ∞) (↑s.ncard : ℕ∞) = t.encard
rw₁ : (↑(t \ s).ncard : ℕ∞) + s.encard = t.encard
rw₂ : (t \ s).encard + s.encard = t.encard
⊢ HAdd.hAdd (α := ℕ∞) (↑(t \ s).ncard : ℕ∞) (↑s.ncard : ℕ∞) = (↑t.ncard : ℕ∞)
have rw₃ : t.encard = t.encard
Tactic: rw [ht.cast_ncard_eq, (ht.subset h).cast_ncard_eq, ht.diff.cast_ncard_eq,
    encard_diff_add_encard_of_subset h]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.Finite
⊢ (t \ s).ncard = t.ncard - s.ncard
have inl : ∀ (ht : t.Finite), (t \ s).ncard = t.ncard - s.ncard
Tactic: obtain ht | ht := t.finite_or_infinite
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.Finite
inl : ∀ (ht : t.Finite), (t \ s).ncard = t.ncard - s.ncard
⊢ (t \ s).ncard = t.ncard - s.ncard
have inr : ∀ (ht : t.Infinite), (t \ s).ncard = t.ncard - s.ncard
Tactic: obtain ht | ht := t.finite_or_infinite
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.Finite
ht : t.Finite
⊢ (t \ s).ncard = t.ncard - s.ncard
have inl : (t \ s).ncard = (t \ s).ncard + s.ncard - s.ncard
Tactic: rw [← ncard_diff_add_ncard_of_subset hst ht, add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.Finite
ht : t.Finite
inl : (t \ s).ncard = (t \ s).ncard + s.ncard - s.ncard
⊢ (t \ s).ncard = t.ncard - s.ncard
have inl₁ : (t \ s).ncard = (t \ s).ncard
Tactic: rw [← ncard_diff_add_ncard_of_subset hst ht, add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.Finite
ht : t.Infinite
⊢ (t \ s).ncard = t.ncard - s.ncard
have inr : (t \ s).ncard = 0 - s.ncard
Tactic: rw [ht.ncard, Nat.zero_sub, (ht.diff hs).ncard]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.Finite
ht : t.Infinite
inr : (t \ s).ncard = 0 - s.ncard
⊢ (t \ s).ncard = t.ncard - s.ncard
have inr₁ : (t \ s).ncard = 0
Tactic: rw [ht.ncard, Nat.zero_sub, (ht.diff hs).ncard]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
hst : s ⊆ t
hs : s.Finite
ht : t.Infinite
inr : (t \ s).ncard = 0 - s.ncard
inr₁ : (t \ s).ncard = 0
⊢ (t \ s).ncard = t.ncard - s.ncard
have inr₂ : Eq (α := ℕ) 0 0
Tactic: rw [ht.ncard, Nat.zero_sub, (ht.diff hs).ncard]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
R : Type u_3
inst : AddGroupWithOne R
hst : s ⊆ t
ht : t.Finite
⊢ (↑(t \ s).ncard : R) = HSub.hSub (α := R) (↑t.ncard : R) (↑s.ncard : R)
have rw : (↑(t.ncard - s.ncard) : R) = HSub.hSub (α := R) (↑t.ncard : R) (↑s.ncard : R)
Tactic: rw [ncard_diff hst (ht.subset hst), Nat.cast_sub (ncard_le_ncard hst ht)]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
R : Type u_3
inst : AddGroupWithOne R
hst : s ⊆ t
ht : t.Finite
rw : (↑(t.ncard - s.ncard) : R) = HSub.hSub (α := R) (↑t.ncard : R) (↑s.ncard : R)
⊢ (↑(t \ s).ncard : R) = HSub.hSub (α := R) (↑t.ncard : R) (↑s.ncard : R)
have rw₁ : HSub.hSub (α := R) (↑t.ncard : R) (↑s.ncard : R) = HSub.hSub (α := R) (↑t.ncard : R) (↑s.ncard : R)
Tactic: rw [ncard_diff hst (ht.subset hst), Nat.cast_sub (ncard_le_ncard hst ht)]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
ht : t.Finite
⊢ s.ncard ≤ (s \ t).ncard + t.ncard
have inl : ∀ (hs : s.Finite), s.ncard ≤ (s \ t).ncard + t.ncard
Tactic: rcases s.finite_or_infinite with hs | hs
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
ht : t.Finite
inl : ∀ (hs : s.Finite), s.ncard ≤ (s \ t).ncard + t.ncard
⊢ s.ncard ≤ (s \ t).ncard + t.ncard
have inr : ∀ (hs : s.Infinite), s.ncard ≤ (s \ t).ncard + t.ncard
Tactic: rcases s.finite_or_infinite with hs | hs
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
ht : t.Finite
hs : s.Finite
⊢ s.ncard ≤ (s \ t).ncard + t.ncard
have inl : (↑s.ncard : ℕ∞) ≤ HAdd.hAdd (α := ℕ∞) (↑(s \ t).ncard : ℕ∞) (↑t.ncard : ℕ∞)
Tactic: to_encard_tac
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
ht : t.Finite
hs : s.Finite
⊢ (↑s.ncard : ℕ∞) ≤ HAdd.hAdd (α := ℕ∞) (↑(s \ t).ncard : ℕ∞) (↑t.ncard : ℕ∞)
have inl : s.encard ≤ (s \ t).encard + t.encard
Tactic: rw [ht.cast_ncard_eq, hs.cast_ncard_eq, hs.diff.cast_ncard_eq]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
ht : t.Finite
hs : s.Infinite
⊢ s.ncard ≤ (s \ t).ncard + t.ncard
have h : s.ncard = 0
Tactic: convert! Nat.zero_le _
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
ht : t.Finite
hs : s.Infinite
⊢ s.ncard = 0
have h : Eq (α := ℕ) 0 0
Tactic: rw [hs.ncard]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
⊢ t.ncard ≤ s.ncard + (t \ s).ncard
have rw : t.ncard ≤ (t \ s).ncard + s.ncard
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ (s \ t).ncard + t.ncard = (s ∪ t).ncard
have rw : (s \ t ∪ t).ncard = (s ∪ t).ncard
Tactic: rw [← ncard_union_eq disjoint_sdiff_left hs.diff ht, diff_union_self]
-- 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 ∪ t).ncard = (s ∪ t).ncard
⊢ (s \ t).ncard + t.ncard = (s ∪ t).ncard
have rw₁ : (s ∪ t).ncard = (s ∪ t).ncard
Tactic: rw [← ncard_union_eq disjoint_sdiff_left hs.diff ht, diff_union_self]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
h : s.ncard < t.ncard
hs : s.Finite
⊢ (t \ s).Nonempty
have rw : ¬t ⊆ s
Tactic: rw [Set.nonempty_iff_ne_empty, Ne, diff_eq_empty]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
⊢ (s ∩ t).ncard + (s \ t).ncard = s.ncard
have rw : (s ∩ t ∪ s \ t).ncard = s.ncard
Tactic: rw [← ncard_union_eq (disjoint_of_subset_left inter_subset_right disjoint_sdiff_right)
    (hs.inter_of_left _) hs.diff, union_comm, diff_union_inter]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
rw : (s ∩ t ∪ s \ t).ncard = s.ncard
⊢ (s ∩ t).ncard + (s \ t).ncard = s.ncard
have rw₁ : (s \ t ∪ s ∩ t).ncard = s.ncard
Tactic: rw [← ncard_union_eq (disjoint_of_subset_left inter_subset_right disjoint_sdiff_right)
    (hs.inter_of_left _) hs.diff, union_comm, diff_union_inter]
-- Lean 4 proof step from Mathlib.Data.Set.Card (goal)
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
rw : (s ∩ t ∪ s \ t).ncard = s.ncard
rw₁ : (s \ t ∪ s ∩ t).ncard = s.ncard
⊢ (s ∩ t).ncard + (s \ t).ncard = s.ncard
have rw₂ : s.ncard = s.ncard
Tactic: rw [← ncard_union_eq (disjoint_of_subset_left inter_subset_right disjoint_sdiff_right)
    (hs.inter_of_left _) hs.diff, union_comm, diff_union_inter]