awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.FinEnum (goal)
Goal:
α : Type u
β : α → Type v
inst : IsEmpty α
e : FinEnum α
⊢ { card := card α, equiv := equiv, decEq := fun (a b : α) ↦ decEq a b } =
    { card := 0, equiv := Equiv.equivOfIsEmpty α (Fin 0), decEq := fun (a b : α) ↦ decidableEq_of_subsingleton a b :
      FinEnum α }
have h : card α = 0
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Data.FinEnum (goal)
Goal:
α : Type u
β : α → Type v
inst : IsEmpty α
e : FinEnum α
h : card α = 0
⊢ { card := card α, equiv := equiv, decEq := fun (a b : α) ↦ decEq a b } =
    { card := 0, equiv := Equiv.equivOfIsEmpty α (Fin 0), decEq := fun (a b : α) ↦ decidableEq_of_subsingleton a b :
      FinEnum α }
have h₁ : HEq (α := α ≃ Fin (card α)) equiv (β := α ≃ Fin 0) (Equiv.equivOfIsEmpty α (Fin 0))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Data.FinEnum (goal)
Goal:
α : Type u
β : α → Type v
inst : IsEmpty α
e : FinEnum α
h : card α = 0
h₁ : HEq (α := α ≃ Fin (card α)) equiv (β := α ≃ Fin 0) (Equiv.equivOfIsEmpty α (Fin 0))
⊢ { card := card α, equiv := equiv, decEq := fun (a b : α) ↦ decEq a b } =
    { card := 0, equiv := Equiv.equivOfIsEmpty α (Fin 0), decEq := fun (a b : α) ↦ decidableEq_of_subsingleton a b :
      FinEnum α }
have h₂ : Eq.{u + 1} (α := DecidableEq α) (fun (a b : α) ↦ decEq a b) fun (a b : α) ↦ decidableEq_of_subsingleton a b
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Data.FinEnum (goal)
Goal:
α : Type u
β : α → Type v
inst : IsEmpty α
e : FinEnum α
⊢ HEq (α := α ≃ Fin (card α)) equiv (β := α ≃ Fin 0) (Equiv.equivOfIsEmpty α (Fin 0))
have h : (α ≃ Fin (card α)) = (α ≃ Fin 0)
Tactic: refine heq_of_cast_eq ?_ (Subsingleton.allEq _ _)
-- Lean 4 proof step from Mathlib.Data.FinEnum (goal)
Goal:
α : Type u
β : α → Type v
inst : IsEmpty α
e : FinEnum α
⊢ Eq.{u + 1} (α := DecidableEq α) (fun (a b : α) ↦ decEq a b) fun (a b : α) ↦ decidableEq_of_subsingleton a b
have h : ∀ (x : α),
  Eq.{u + 1} (α := (b : α) → Decidable (x = b)) (fun (b : α) ↦ decEq x b) fun (b : α) ↦ decidableEq_of_subsingleton x b
Tactic: funext x
-- Lean 4 proof step from Mathlib.Data.FinEnum (goal)
Goal:
α : Type u
β : α → Type v
inst : Unique α
e : FinEnum α
⊢ { card := card α, equiv := equiv, decEq := fun (a b : α) ↦ decEq a b } =
    { card := 1, equiv := Equiv.ofUnique α (Fin 1), decEq := fun (a b : α) ↦ decidableEq_of_subsingleton a b :
      FinEnum α }
have h : card α = 1
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Data.FinEnum (goal)
Goal:
α : Type u
β : α → Type v
inst : Unique α
e : FinEnum α
h : card α = 1
⊢ { card := card α, equiv := equiv, decEq := fun (a b : α) ↦ decEq a b } =
    { card := 1, equiv := Equiv.ofUnique α (Fin 1), decEq := fun (a b : α) ↦ decidableEq_of_subsingleton a b :
      FinEnum α }
have h₁ : HEq (α := α ≃ Fin (card α)) equiv (β := α ≃ Fin 1) (Equiv.ofUnique α (Fin 1))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Data.FinEnum (goal)
Goal:
α : Type u
β : α → Type v
inst : Unique α
e : FinEnum α
h : card α = 1
h₁ : HEq (α := α ≃ Fin (card α)) equiv (β := α ≃ Fin 1) (Equiv.ofUnique α (Fin 1))
⊢ { card := card α, equiv := equiv, decEq := fun (a b : α) ↦ decEq a b } =
    { card := 1, equiv := Equiv.ofUnique α (Fin 1), decEq := fun (a b : α) ↦ decidableEq_of_subsingleton a b :
      FinEnum α }
have h₂ : Eq.{u + 1} (α := DecidableEq α) (fun (a b : α) ↦ decEq a b) fun (a b : α) ↦ decidableEq_of_subsingleton a b
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Data.FinEnum (goal)
Goal:
α : Type u
β : α → Type v
inst : Unique α
e : FinEnum α
⊢ HEq (α := α ≃ Fin (card α)) equiv (β := α ≃ Fin 1) (Equiv.ofUnique α (Fin 1))
have h : (α ≃ Fin (card α)) = (α ≃ Fin 1)
Tactic: refine heq_of_cast_eq ?_ (Subsingleton.allEq _ _)
-- Lean 4 proof step from Mathlib.Data.Finite.Card (goal)
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
α : Type u_4
inst : Finite α
⊢ α ≃ Fin (Nat.card α)
have have : (this : α ≃ Fin (sorry.choose (p := fun (n : ℕ) ↦ Nonempty.{max 1 (u_4 + 1)} (α ≃ Fin n)))) → α ≃ Fin (Nat.card α)
Tactic: have := (Finite.exists_equiv_fin α).choose_spec.some
-- Lean 4 proof step from Mathlib.Data.Finite.Card (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Finite α
n : ℕ
h : Nat.card α = n
⊢ α ≃ Fin n
have subst : α ≃ Fin (Nat.card α)
Tactic: subst h
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Data.Finite.Card (goal)
Goal:
α : Type u_4
⊢ Nat.card α = if x : Finite α then Fintype.card α else 0
have inl : Finite α → Nat.card α = if x : Finite α then Fintype.card α else 0
Tactic: cases finite_or_infinite α
-- Lean 4 proof step from Mathlib.Data.Finite.Card (goal)
Goal:
α : Type u_4
inl : Finite α → Nat.card α = if x : Finite α then Fintype.card α else 0
⊢ Nat.card α = if x : Finite α then Fintype.card α else 0
have inr : Infinite α → Nat.card α = if x : Finite α then Fintype.card α else 0
Tactic: cases finite_or_infinite α
-- Lean 4 proof step from Mathlib.Data.Finite.Card (goal)
Goal:
α : Type u_1
inst : Finite α
⊢ 0 < Nat.card α ↔ Nonempty α
have haveI : ∀ (this : Fintype α), 0 < Nat.card α ↔ Nonempty α
Tactic: haveI := Fintype.ofFinite α
-- Lean 4 proof step from Mathlib.Data.Finite.Card (goal)
Goal:
α : Type u_1
inst : Finite α
this : Fintype α
⊢ 0 < Nat.card α ↔ Nonempty α
have rw : 0 < Fintype.card α ↔ Nonempty α
Tactic: rw [Nat.card_eq_fintype_card, Fintype.card_pos_iff]
-- Lean 4 proof step from Mathlib.Data.Finite.Card (goal)
Goal:
α : Type u_1
inst : Finite α
this : Fintype α
rw : 0 < Fintype.card α ↔ Nonempty α
⊢ 0 < Nat.card α ↔ Nonempty α
have rw₁ : Nonempty α ↔ Nonempty α
Tactic: rw [Nat.card_eq_fintype_card, Fintype.card_pos_iff]
-- Lean 4 proof step from Mathlib.Data.Finite.Card (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
inst_1 : Finite β
⊢ Nat.card α = Nat.card β ↔ Nonempty (α ≃ β)
have haveI : ∀ (this : Fintype α), Nat.card α = Nat.card β ↔ Nonempty (α ≃ β)
Tactic: haveI := Fintype.ofFinite α
-- Lean 4 proof step from Mathlib.Data.Finite.Card (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
inst_1 : Finite β
this : Fintype α
⊢ Nat.card α = Nat.card β ↔ Nonempty (α ≃ β)
have haveI : ∀ (this : Fintype β), Nat.card α = Nat.card β ↔ Nonempty (α ≃ β)
Tactic: haveI := Fintype.ofFinite β
-- Lean 4 proof step from Mathlib.Data.Finite.Card (goal)
Goal:
α : Type u_1
inst : Finite α
⊢ Nat.card α ≤ 1 ↔ Subsingleton α
have haveI : ∀ (this : Fintype α), Nat.card α ≤ 1 ↔ Subsingleton α
Tactic: haveI := Fintype.ofFinite α
-- Lean 4 proof step from Mathlib.Data.Finite.Card (goal)
Goal:
α : Type u_1
inst : Finite α
⊢ 1 < Nat.card α ↔ Nontrivial α
have haveI : ∀ (this : Fintype α), 1 < Nat.card α ↔ Nontrivial α
Tactic: haveI := Fintype.ofFinite α
-- Lean 4 proof step from Mathlib.Data.Finite.Card (goal)
Goal:
α : Type u_1
inst : Finite α
⊢ Nat.card.{u_1} (Option α) = Nat.card α + 1
have haveI : ∀ (this : Fintype α), Nat.card.{u_1} (Option α) = Nat.card α + 1
Tactic: haveI := Fintype.ofFinite α
-- Lean 4 proof step from Mathlib.Data.Finite.Card (goal)
Goal:
α : Type u_1
inst : Finite α
⊢ Nat.card α = 0 ↔ IsEmpty α
have haveI : ∀ (this : Fintype α), Nat.card α = 0 ↔ IsEmpty α
Tactic: haveI := Fintype.ofFinite α
-- Lean 4 proof step from Mathlib.Data.Finite.Card (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Function.Surjective f
h : Nat.card β = 0
⊢ Nat.card α = 0
have inl : Finite β → Nat.card α = 0
Tactic: cases finite_or_infinite β
-- Lean 4 proof step from Mathlib.Data.Finite.Card (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Function.Surjective f
h : Nat.card β = 0
inl : Finite β → Nat.card α = 0
⊢ Nat.card α = 0
have inr : Infinite β → Nat.card α = 0
Tactic: cases finite_or_infinite β
-- Lean 4 proof step from Mathlib.Data.Finite.Card (hypothesis)
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Function.Surjective f
h : Nat.card β = 0
h_1 : Finite β
⊢ Nat.card α = 0
have this : IsEmpty β
Tactic: haveI := card_eq_zero_iff.mp h
-- Lean 4 proof step from Mathlib.Data.Finite.Card (hypothesis)
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Function.Surjective f
h : Nat.card β = 0
h_1 : Finite β
this : IsEmpty β
⊢ Nat.card α = 0
have this₁ : IsEmpty α
Tactic: haveI := Function.isEmpty f
-- Lean 4 proof step from Mathlib.Data.Finite.Card (hypothesis)
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Function.Surjective f
h : Nat.card β = 0
h_1 : Infinite β
⊢ Nat.card α = 0
have this : Infinite α
Tactic: haveI := Infinite.of_surjective f hf
-- Lean 4 proof step from Mathlib.Data.Finite.Card (goal)
Goal:
α : Type u_1
inst : Finite α
p : α → Prop
⊢ Nat.card.{u_1} { x : α // p x } ≤ Nat.card α
have haveI : ∀ (this : Fintype α), Nat.card.{u_1} { x : α // p x } ≤ Nat.card α
Tactic: haveI := Fintype.ofFinite α
-- Lean 4 proof step from Mathlib.Data.Finite.Card (goal)
Goal:
α : Type u_1
inst : Finite α
p : α → Prop
⊢ Nat.card.{u_1} { x : α // p x } ≤ Nat.card α
have haveI : ∀ (this : Fintype α), Nat.card.{u_1} { x : α // p x } ≤ Nat.card α
Tactic: classical
  haveI := Fintype.ofFinite α
  simpa only [Nat.card_eq_fintype_card] using Fintype.card_subtype_le p
-- Lean 4 proof step from Mathlib.Data.Finite.Card (goal)
Goal:
α : Type u_1
inst : Finite α
p : α → Prop
x : α
hx : ¬p x
⊢ Nat.card.{u_1} { x : α // p x } < Nat.card α
have haveI : ∀ (this : Fintype α), Nat.card.{u_1} { x : α // p x } < Nat.card α
Tactic: haveI := Fintype.ofFinite α
-- Lean 4 proof step from Mathlib.Data.Finite.Card (goal)
Goal:
α : Type u_1
inst : Finite α
p : α → Prop
x : α
hx : ¬p x
⊢ Nat.card.{u_1} { x : α // p x } < Nat.card α
have haveI : ∀ (this : Fintype α), Nat.card.{u_1} { x : α // p x } < Nat.card α
Tactic: classical
  haveI := Fintype.ofFinite α
  simpa only [Nat.card_eq_fintype_card, gt_iff_lt] using Fintype.card_subtype_lt hx
-- Lean 4 proof step from Mathlib.Data.Finite.Card (goal)
Goal:
α : Type u_4
inst : Finite α
⊢ Eq (α := ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_4}) → ℕ∞) (Cardinal.mk α) : ℕ∞) ((↑(Nat.card α) : ℕ∞) : ℕ∞)
have a : Eq (α := ℕ∞) ((↑(Nat.card α) : ℕ∞) : ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_4}) → ℕ∞) (Cardinal.mk α) : ℕ∞)
Tactic: apply symm
-- Lean 4 proof step from Mathlib.Data.Finite.Card (goal)
Goal:
α : Type u_4
inst : Finite α
⊢ Eq (α := ℕ∞) ((↑(Nat.card α) : ℕ∞) : ℕ∞) ((Cardinal.toENat : (a : Cardinal.{u_4}) → ℕ∞) (Cardinal.mk α) : ℕ∞)
have a : (↑(Nat.card α) : Cardinal.{u_4}) = Cardinal.mk α
Tactic: rw [Cardinal.natCast_eq_toENat]
-- Lean 4 proof step from Mathlib.Data.Finite.Card (goal)
Goal:
α : Type u_1
s t : Set α
⊢ Nat.card.{u_1} (↑(s ∪ t) : Type u_1) ≤ Nat.card.{u_1} (↑s : Type u_1) + Nat.card.{u_1} (↑t : Type u_1)
have inl : ∀ (h : Finite.{u_1 + 1} (↑(s ∪ t) : Type u_1)),
  Nat.card.{u_1} (↑(s ∪ t) : Type u_1) ≤ Nat.card.{u_1} (↑s : Type u_1) + Nat.card.{u_1} (↑t : Type u_1)
Tactic: rcases _root_.finite_or_infinite (↥(s ∪ t)) with h | h
-- Lean 4 proof step from Mathlib.Data.Finite.Card (goal)
Goal:
α : Type u_1
s t : Set α
inl :
  ∀ (h : Finite.{u_1 + 1} (↑(s ∪ t) : Type u_1)),
    Nat.card.{u_1} (↑(s ∪ t) : Type u_1) ≤ Nat.card.{u_1} (↑s : Type u_1) + Nat.card.{u_1} (↑t : Type u_1)
⊢ Nat.card.{u_1} (↑(s ∪ t) : Type u_1) ≤ Nat.card.{u_1} (↑s : Type u_1) + Nat.card.{u_1} (↑t : Type u_1)
have inr : ∀ (h : Infinite.{u_1 + 1} (↑(s ∪ t) : Type u_1)),
  Nat.card.{u_1} (↑(s ∪ t) : Type u_1) ≤ Nat.card.{u_1} (↑s : Type u_1) + Nat.card.{u_1} (↑t : Type u_1)
Tactic: rcases _root_.finite_or_infinite (↥(s ∪ t)) with h | h
-- Lean 4 proof step from Mathlib.Data.Finite.Card (hypothesis)
Goal:
α : Type u_1
s t : Set α
h : Finite.{u_1 + 1} (↑(s ∪ t) : Type u_1)
⊢ Nat.card.{u_1} (↑(s ∪ t) : Type u_1) ≤ Nat.card.{u_1} (↑s : Type u_1) + Nat.card.{u_1} (↑t : Type u_1)
have h₁ : Finite.{u_1 + 1} (↑s : Type u_1) ∧ Finite.{u_1 + 1} (↑t : Type u_1)
Tactic: rw [finite_coe_iff, finite_union, ← finite_coe_iff, ← finite_coe_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Finite.Card (hypothesis)
Goal:
α : Type u_1
s t : Set α
h : Finite.{u_1 + 1} (↑s : Type u_1) ∧ Finite.{u_1 + 1} (↑t : Type u_1)
⊢ Nat.card.{u_1} (↑(s ∪ t) : Type u_1) ≤ Nat.card.{u_1} (↑s : Type u_1) + Nat.card.{u_1} (↑t : Type u_1)
have left : Finite.{u_1 + 1} (↑s : Type u_1)
Tactic: cases h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Finite.Card (hypothesis)
Goal:
α : Type u_1
s t : Set α
h : Finite.{u_1 + 1} (↑s : Type u_1) ∧ Finite.{u_1 + 1} (↑t : Type u_1)
left : Finite.{u_1 + 1} (↑s : Type u_1)
⊢ Nat.card.{u_1} (↑(s ∪ t) : Type u_1) ≤ Nat.card.{u_1} (↑s : Type u_1) + Nat.card.{u_1} (↑t : Type u_1)
have right : Finite.{u_1 + 1} (↑t : Type u_1)
Tactic: cases h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Finite.Card (goal)
Goal:
α : Type u_1
s t : Set α
left : Finite.{u_1 + 1} (↑s : Type u_1)
right : Finite.{u_1 + 1} (↑t : Type u_1)
⊢ Nat.card.{u_1} (↑(s ∪ t) : Type u_1) ≤ Nat.card.{u_1} (↑s : Type u_1) + Nat.card.{u_1} (↑t : Type u_1)
have inl : Cardinal.mk (↑(s ∪ t) : Type u_1) ≤ Cardinal.mk (↑s : Type u_1) + Cardinal.mk (↑t : Type u_1)
Tactic: rw [← @Nat.cast_le Cardinal, Nat.cast_add, Nat.cast_card, Nat.cast_card, Nat.cast_card]
-- Lean 4 proof step from Mathlib.Data.Finite.Card (goal)
Goal:
α : Type u_1
s t : Set α
ht : t.Finite
hsub : s ⊂ t
⊢ Nat.card.{u_1} (↑s : Type u_1) < Nat.card.{u_1} (↑t : Type u_1)
have have : ∀ (this : Fintype (↑t : Type u_1)), Nat.card.{u_1} (↑s : Type u_1) < Nat.card.{u_1} (↑t : Type u_1)
Tactic: have : Fintype t := Finite.fintype ht
-- Lean 4 proof step from Mathlib.Data.Finite.Card (goal)
Goal:
α : Type u_1
s t : Set α
ht : t.Finite
hsub : s ⊂ t
this : Fintype (↑t : Type u_1)
⊢ Nat.card.{u_1} (↑s : Type u_1) < Nat.card.{u_1} (↑t : Type u_1)
have have : ∀ (this : Fintype (↑s : Type u_1)), Nat.card.{u_1} (↑s : Type u_1) < Nat.card.{u_1} (↑t : Type u_1)
Tactic: have : Fintype s := Finite.fintype (subset ht (subset_of_ssubset hsub))
-- Lean 4 proof step from Mathlib.Data.Finite.Card (goal)
Goal:
α : Type u_1
s t : Set α
ht : t.Finite
hsub : s ⊂ t
this_1 : Fintype (↑t : Type u_1)
this : Fintype (↑s : Type u_1)
⊢ Nat.card.{u_1} (↑s : Type u_1) < Nat.card.{u_1} (↑t : Type u_1)
have simp : Fintype.card.{u_1} (↑s : Type u_1) < Fintype.card.{u_1} (↑t : Type u_1)
Tactic: simp only [Nat.card_eq_fintype_card]
-- Lean 4 proof step from Mathlib.Data.Finite.Card (goal)
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
hsub : s ⊂ t
⊢ ENat.card.{u_1} (↑s : Type u_1) < ENat.card.{u_1} (↑t : Type u_1)
have suffices : ENat.card.{u_1} (↑t : Type u_1) ≤ ENat.card.{u_1} (↑s : Type u_1) → t ⊆ s
Tactic: suffices ENat.card t ≤ ENat.card s → t ⊆ s from
    lt_of_le_not_ge (ecard_le_ecard hsub.subset) fun hle ↦ not_subset_of_ssubset hsub <| this hle
-- Lean 4 proof step from Mathlib.Data.Finite.Card (goal)
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
hsub : s ⊂ t
hle : ENat.card.{u_1} (↑t : Type u_1) ≤ ENat.card.{u_1} (↑s : Type u_1)
this : ENat.card.{u_1} (↑(t \ s) : Type u_1) ≤ 0
⊢ t ⊆ s
have rwa : t \ s = ∅
Tactic: rwa [← diff_eq_empty, ← Set.isEmpty_coe_sort, ← ENat.card_eq_zero_iff_empty,
      ← nonpos_iff_eq_zero]
-- Lean 4 proof step from Mathlib.Data.Finite.Card (goal)
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
hsub : s ⊂ t
hle : ENat.card.{u_1} (↑t : Type u_1) ≤ ENat.card.{u_1} (↑s : Type u_1)
this : ENat.card.{u_1} (↑(t \ s) : Type u_1) ≤ 0
rwa : t \ s = ∅
⊢ t ⊆ s
have rwa₁ : IsEmpty.{u_1 + 1} (↑(t \ s) : Type u_1)
Tactic: rwa [← diff_eq_empty, ← Set.isEmpty_coe_sort, ← ENat.card_eq_zero_iff_empty,
      ← nonpos_iff_eq_zero]
-- Lean 4 proof step from Mathlib.Data.Finite.Card (goal)
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
hsub : s ⊂ t
hle : ENat.card.{u_1} (↑t : Type u_1) ≤ ENat.card.{u_1} (↑s : Type u_1)
this : ENat.card.{u_1} (↑(t \ s) : Type u_1) ≤ 0
rwa : t \ s = ∅
rwa₁ : IsEmpty.{u_1 + 1} (↑(t \ s) : Type u_1)
⊢ t ⊆ s
have rwa₂ : ENat.card.{u_1} (↑(t \ s) : Type u_1) = 0
Tactic: rwa [← diff_eq_empty, ← Set.isEmpty_coe_sort, ← ENat.card_eq_zero_iff_empty,
      ← nonpos_iff_eq_zero]
-- Lean 4 proof step from Mathlib.Data.Finite.Card (goal)
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
hsub : s ⊂ t
hle : ENat.card.{u_1} (↑t : Type u_1) ≤ ENat.card.{u_1} (↑s : Type u_1)
⊢ t ⊆ s
have suffices : ENat.card.{u_1} (↑(t \ s) : Type u_1) ≤ 0
Tactic: suffices ENat.card ↑(t \ s) ≤ 0 by
    rwa [← diff_eq_empty, ← Set.isEmpty_coe_sort, ← ENat.card_eq_zero_iff_empty,
      ← nonpos_iff_eq_zero]
-- Lean 4 proof step from Mathlib.Data.Finite.Card (goal)
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
hsub : s ⊂ t
hle : ENat.card.{u_1} (↑t : Type u_1) ≤ ENat.card.{u_1} (↑s : Type u_1)
⊢ ENat.card.{u_1} (↑(t \ s) : Type u_1) ≤ 0
have suffices : ENat.card.{u_1} (↑(t \ s) : Type u_1) + ENat.card.{u_1} (↑s : Type u_1) ≤ 0 + ENat.card.{u_1} (↑s : Type u_1)
Tactic: suffices ENat.card ↑(t \ s) + ENat.card ↑s ≤ 0 + ENat.card ↑s from
    WithTop.le_of_add_le_add_right (ENat.card_lt_top.mpr hs).ne this
-- Lean 4 proof step from Mathlib.Data.Finite.Card (goal)
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
hsub : s ⊂ t
hle : ENat.card.{u_1} (↑t : Type u_1) ≤ ENat.card.{u_1} (↑s : Type u_1)
this : ENat.card.{u_1} (↑t : Type u_1) ≤ 0 + ENat.card.{u_1} (↑s : Type u_1)
⊢ ENat.card.{u_1} (↑(t \ s) : Type u_1) + ENat.card.{u_1} (↑s : Type u_1) ≤ 0 + ENat.card.{u_1} (↑s : Type u_1)
have rwa : ENat.card.{u_1} ((↑(t \ s) : Type u_1) ⊕ (↑s : Type u_1)) ≤ 0 + ENat.card.{u_1} (↑s : Type u_1)
Tactic: rwa [← ENat.card_sum, ← ENat.card_congr <| Equiv.Set.union disjoint_sdiff_left,
      diff_union_of_subset hsub.subset]
-- Lean 4 proof step from Mathlib.Data.Finite.Card (goal)
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
hsub : s ⊂ t
hle : ENat.card.{u_1} (↑t : Type u_1) ≤ ENat.card.{u_1} (↑s : Type u_1)
this : ENat.card.{u_1} (↑t : Type u_1) ≤ 0 + ENat.card.{u_1} (↑s : Type u_1)
rwa : ENat.card.{u_1} ((↑(t \ s) : Type u_1) ⊕ (↑s : Type u_1)) ≤ 0 + ENat.card.{u_1} (↑s : Type u_1)
⊢ ENat.card.{u_1} (↑(t \ s) : Type u_1) + ENat.card.{u_1} (↑s : Type u_1) ≤ 0 + ENat.card.{u_1} (↑s : Type u_1)
have rwa₁ : ENat.card.{u_1} (↑(t \ s ∪ s) : Type u_1) ≤ 0 + ENat.card.{u_1} (↑s : Type u_1)
Tactic: rwa [← ENat.card_sum, ← ENat.card_congr <| Equiv.Set.union disjoint_sdiff_left,
      diff_union_of_subset hsub.subset]
-- Lean 4 proof step from Mathlib.Data.Finite.Card (goal)
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
hsub : s ⊂ t
hle : ENat.card.{u_1} (↑t : Type u_1) ≤ ENat.card.{u_1} (↑s : Type u_1)
⊢ ENat.card.{u_1} (↑(t \ s) : Type u_1) + ENat.card.{u_1} (↑s : Type u_1) ≤ 0 + ENat.card.{u_1} (↑s : Type u_1)
have suffices : ENat.card.{u_1} (↑t : Type u_1) ≤ 0 + ENat.card.{u_1} (↑s : Type u_1)
Tactic: suffices ENat.card ↑t ≤ 0 + ENat.card ↑s by
    rwa [← ENat.card_sum, ← ENat.card_congr <| Equiv.Set.union disjoint_sdiff_left,
      diff_union_of_subset hsub.subset]
-- Lean 4 proof step from Mathlib.Data.Finite.Card (goal)
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
hsub : s ⊂ t
⊢ ENat.card.{u_1} (↑s : Type u_1) < ENat.card.{u_1} (↑t : Type u_1)
have suffices : ENat.card.{u_1} (↑t : Type u_1) ≤ ENat.card.{u_1} (↑s : Type u_1) → t ⊆ s
Tactic: classical
  suffices ENat.card t ≤ ENat.card s → t ⊆ s from
    lt_of_le_not_ge (ecard_le_ecard hsub.subset) fun hle ↦ not_subset_of_ssubset hsub <| this hle
  intro hle
  suffices ENat.card ↑(t \ s) ≤ 0 by
    rwa [← diff_eq_empty, ← Set.isEmpty_coe_sort, ← ENat.card_eq_zero_iff_empty,
      ← nonpos_iff_eq_zero]
  suffices ENat.card ↑(t \ s) + ENat.card ↑s ≤ 0 + ENat.card ↑s from
    WithTop.le_of_add_le_add_right (ENat.card_lt_top.mpr hs).ne this
  suffices ENat.card ↑t ≤ 0 + ENat.card ↑s by
    rwa [← ENat.card_sum, ← ENat.card_congr <| Equiv.Set.union disjoint_sdiff_left,
      diff_union_of_subset hsub.subset]
  exact le_add_of_le_right hle
-- Lean 4 proof step from Mathlib.Data.Finite.Card (goal)
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
hsub : s ⊂ t
suffices suffices₁ suffices₂ suffices₃ :
  ∀ (hle : ENat.card.{u_1} (↑t : Type u_1) ≤ ENat.card.{u_1} (↑s : Type u_1)), t ⊆ s
⊢ ENat.card.{u_1} (↑s : Type u_1) < ENat.card.{u_1} (↑t : Type u_1)
have suffices₄ : ∀ (hle : ENat.card.{u_1} (↑t : Type u_1) ≤ ENat.card.{u_1} (↑s : Type u_1)), ENat.card.{u_1} (↑(t \ s) : Type u_1) ≤ 0
Tactic: classical
  suffices ENat.card t ≤ ENat.card s → t ⊆ s from
    lt_of_le_not_ge (ecard_le_ecard hsub.subset) fun hle ↦ not_subset_of_ssubset hsub <| this hle
  intro hle
  suffices ENat.card ↑(t \ s) ≤ 0 by
    rwa [← diff_eq_empty, ← Set.isEmpty_coe_sort, ← ENat.card_eq_zero_iff_empty,
      ← nonpos_iff_eq_zero]
  suffices ENat.card ↑(t \ s) + ENat.card ↑s ≤ 0 + ENat.card ↑s from
    WithTop.le_of_add_le_add_right (ENat.card_lt_top.mpr hs).ne this
  suffices ENat.card ↑t ≤ 0 + ENat.card ↑s by
    rwa [← ENat.card_sum, ← ENat.card_congr <| Equiv.Set.union disjoint_sdiff_left,
      diff_union_of_subset hsub.subset]
  exact le_add_of_le_right hle
-- Lean 4 proof step from Mathlib.Data.Finite.Card (goal)
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
hsub : s ⊂ t
suffices suffices₁ suffices₂ suffices₃ :
  ∀ (hle : ENat.card.{u_1} (↑t : Type u_1) ≤ ENat.card.{u_1} (↑s : Type u_1)), t ⊆ s
suffices₄ :
  ∀ (hle : ENat.card.{u_1} (↑t : Type u_1) ≤ ENat.card.{u_1} (↑s : Type u_1)), ENat.card.{u_1} (↑(t \ s) : Type u_1) ≤ 0
⊢ ENat.card.{u_1} (↑s : Type u_1) < ENat.card.{u_1} (↑t : Type u_1)
have suffices₅ : ∀ (hle : ENat.card.{u_1} (↑t : Type u_1) ≤ ENat.card.{u_1} (↑s : Type u_1)),
  ENat.card.{u_1} (↑(t \ s) : Type u_1) + ENat.card.{u_1} (↑s : Type u_1) ≤ 0 + ENat.card.{u_1} (↑s : Type u_1)
Tactic: classical
  suffices ENat.card t ≤ ENat.card s → t ⊆ s from
    lt_of_le_not_ge (ecard_le_ecard hsub.subset) fun hle ↦ not_subset_of_ssubset hsub <| this hle
  intro hle
  suffices ENat.card ↑(t \ s) ≤ 0 by
    rwa [← diff_eq_empty, ← Set.isEmpty_coe_sort, ← ENat.card_eq_zero_iff_empty,
      ← nonpos_iff_eq_zero]
  suffices ENat.card ↑(t \ s) + ENat.card ↑s ≤ 0 + ENat.card ↑s from
    WithTop.le_of_add_le_add_right (ENat.card_lt_top.mpr hs).ne this
  suffices ENat.card ↑t ≤ 0 + ENat.card ↑s by
    rwa [← ENat.card_sum, ← ENat.card_congr <| Equiv.Set.union disjoint_sdiff_left,
      diff_union_of_subset hsub.subset]
  exact le_add_of_le_right hle
-- Lean 4 proof step from Mathlib.Data.Finite.Card (goal)
Goal:
α : Type u_1
s t : Set α
hs : s.Finite
hsub : s ⊂ t
suffices suffices₁ suffices₂ suffices₃ :
  ∀ (hle : ENat.card.{u_1} (↑t : Type u_1) ≤ ENat.card.{u_1} (↑s : Type u_1)), t ⊆ s
suffices₄ :
  ∀ (hle : ENat.card.{u_1} (↑t : Type u_1) ≤ ENat.card.{u_1} (↑s : Type u_1)), ENat.card.{u_1} (↑(t \ s) : Type u_1) ≤ 0
suffices₅ :
  ∀ (hle : ENat.card.{u_1} (↑t : Type u_1) ≤ ENat.card.{u_1} (↑s : Type u_1)),
    ENat.card.{u_1} (↑(t \ s) : Type u_1) + ENat.card.{u_1} (↑s : Type u_1) ≤ 0 + ENat.card.{u_1} (↑s : Type u_1)
⊢ ENat.card.{u_1} (↑s : Type u_1) < ENat.card.{u_1} (↑t : Type u_1)
have suffices₆ : ∀ (hle : ENat.card.{u_1} (↑t : Type u_1) ≤ ENat.card.{u_1} (↑s : Type u_1)),
  ENat.card.{u_1} (↑t : Type u_1) ≤ 0 + ENat.card.{u_1} (↑s : Type u_1)
Tactic: classical
  suffices ENat.card t ≤ ENat.card s → t ⊆ s from
    lt_of_le_not_ge (ecard_le_ecard hsub.subset) fun hle ↦ not_subset_of_ssubset hsub <| this hle
  intro hle
  suffices ENat.card ↑(t \ s) ≤ 0 by
    rwa [← diff_eq_empty, ← Set.isEmpty_coe_sort, ← ENat.card_eq_zero_iff_empty,
      ← nonpos_iff_eq_zero]
  suffices ENat.card ↑(t \ s) + ENat.card ↑s ≤ 0 + ENat.card ↑s from
    WithTop.le_of_add_le_add_right (ENat.card_lt_top.mpr hs).ne this
  suffices ENat.card ↑t ≤ 0 + ENat.card ↑s by
    rwa [← ENat.card_sum, ← ENat.card_congr <| Equiv.Set.union disjoint_sdiff_left,
      diff_union_of_subset hsub.subset]
  exact le_add_of_le_right hle
-- Lean 4 proof step from Mathlib.Data.Finite.Card (goal)
Goal:
α : Type u_1
s : Set α
e : α ≃ α
hs : s.Finite
h : (⇑e : (a : α) → α) '' s = s
⊢ (⇑e : (a : α) → α) '' s ⊆ s
have rw : s ⊆ s
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Data.Finite.Card (goal)
Goal:
α : Type u_1
l : List α
h : l.Nodup
inst : Finite α
⊢ l.length ≤ Nat.card α
have have : ∀ (this : Fintype α), l.length ≤ Nat.card α
Tactic: have := Fintype.ofFinite α
-- Lean 4 proof step from Mathlib.Data.Finite.Card (goal)
Goal:
α : Type u_1
l : List α
h : l.Nodup
inst : Finite α
this : Fintype α
⊢ l.length ≤ Nat.card α
have grw : Fintype.card α ≤ Nat.card α
Tactic: grw [h.length_le_card, Fintype.card_eq_nat_card]
-- Lean 4 proof step from Mathlib.Data.Finite.Card (goal)
Goal:
α : Type u_1
l : List α
h : l.Nodup
inst : Finite α
this : Fintype α
grw : Fintype.card α ≤ Nat.card α
⊢ l.length ≤ Nat.card α
have grw₁ : Nat.card α ≤ Nat.card α
Tactic: grw [h.length_le_card, Fintype.card_eq_nat_card]