awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
⊢ Nat.card.{u_2} (↑(range f) : Type u_2) = Nat.card α
have rw : Nat.card.{u_1} (↑(f ⁻¹' range f) : Type u_1) = Nat.card α
Tactic: rw [← Nat.card_preimage_of_injective hf le_rfl]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
h : Nat.card α ≠ 0
⊢ α ≃ Fin (Nat.card α)
have inl : Fintype α → α ≃ Fin (Nat.card α)
Tactic: cases fintypeOrInfinite α
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
h : Nat.card α ≠ 0
inl : Fintype α → α ≃ Fin (Nat.card α)
⊢ α ≃ Fin (Nat.card α)
have inr : Infinite α → α ≃ Fin (Nat.card α)
Tactic: cases fintypeOrInfinite α
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_1
a : α
inst : Subsingleton α
this : Fintype α := Fintype.ofSubsingleton a
⊢ Nat.card α = 1
have rw : Fintype.card α = 1
Tactic: rw [card_eq_fintype_card, Fintype.card_ofSubsingleton a]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_1
a : α
inst : Subsingleton α
this : Fintype α := Fintype.ofSubsingleton a
rw : Fintype.card α = 1
⊢ Nat.card α = 1
have rw₁ : Eq (α := ℕ) 1 1
Tactic: rw [card_eq_fintype_card, Fintype.card_ofSubsingleton a]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_1
⊢ Nat.card α = 1 ↔ ∃ (x : α), ∀ (y : α), y = x
have rw : Subsingleton α ∧ Nonempty α ↔ ∃ (x : α), ∀ (y : α), y = x
Tactic: rw [card_eq_one_iff_unique]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
inst_1 : Finite β
⊢ Nat.card (α ⊕ β) = Nat.card α + Nat.card β
have have : ∀ (this : Fintype α), Nat.card (α ⊕ β) = Nat.card α + Nat.card β
Tactic: have := Fintype.ofFinite α
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
inst_1 : Finite β
this : Fintype α
⊢ Nat.card (α ⊕ β) = Nat.card α + Nat.card β
have have : ∀ (this : Fintype β), Nat.card (α ⊕ β) = Nat.card α + Nat.card β
Tactic: have := Fintype.ofFinite β
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
inst_1 : Finite β
this_1 : Fintype α
this : Fintype β
⊢ Nat.card (α ⊕ β) = Nat.card α + Nat.card β
have simp_rw : Fintype.card (α ⊕ β) = Fintype.card α + Fintype.card β
Tactic: simp_rw [Nat.card_eq_fintype_card, Fintype.card_sum]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_1
β : α → Type u_3
inst : Fintype α
inst_1 : ∀ (a : α), Finite.{u_3 + 1} (β a)
x : (a : α) → Fintype (β a) := fun (a : α) ↦ Fintype.ofFinite (β a)
⊢ Nat.card (Sigma β) = ∑ a : α, Nat.card.{u_3} (β a)
have simp_rw : Fintype.card (Sigma β) = ∑ x_1 : α, Fintype.card.{u_3} (β x_1)
Tactic: simp_rw [Nat.card_eq_fintype_card, Fintype.card_sigma]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_1
β : α → Type u_3
inst : Fintype α
⊢ Nat.card ((a : α) → β a) = ∏ a : α, Nat.card.{u_3} (β a)
have simp_rw : Eq (α := ℕ) ((toNat : (a : Cardinal.{max u_1 u_3}) → ℕ) #((a : α) → β a) : ℕ)
  (∏ x : α, (toNat : (a : Cardinal.{u_3}) → ℕ) #(β x) : ℕ)
Tactic: simp_rw [Nat.card, mk_pi, prod_eq_of_fintype, toNat_lift, _root_.map_prod]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_1
β : α → Type u_3
inst : Fintype α
simp_rw :
  Eq (α := ℕ) ((toNat : (a : Cardinal.{max u_1 u_3}) → ℕ) #((a : α) → β a) : ℕ)
    (∏ x : α, (toNat : (a : Cardinal.{u_3}) → ℕ) #(β x) : ℕ)
⊢ Nat.card ((a : α) → β a) = ∏ a : α, Nat.card.{u_3} (β a)
have simp_rw₁ : Eq (α := ℕ) ((toNat : (a : Cardinal.{max u_1 u_3}) → ℕ) (prod.{u_1, u_3} fun (i : α) ↦ #(β i)) : ℕ)
  (∏ x : α, (toNat : (a : Cardinal.{u_3}) → ℕ) #(β x) : ℕ)
Tactic: simp_rw [Nat.card, mk_pi, prod_eq_of_fintype, toNat_lift, _root_.map_prod]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_1
β : α → Type u_3
inst : Fintype α
simp_rw :
  Eq (α := ℕ) ((toNat : (a : Cardinal.{max u_1 u_3}) → ℕ) #((a : α) → β a) : ℕ)
    (∏ x : α, (toNat : (a : Cardinal.{u_3}) → ℕ) #(β x) : ℕ)
simp_rw₁ :
  Eq (α := ℕ) ((toNat : (a : Cardinal.{max u_1 u_3}) → ℕ) (prod.{u_1, u_3} fun (i : α) ↦ #(β i)) : ℕ)
    (∏ x : α, (toNat : (a : Cardinal.{u_3}) → ℕ) #(β x) : ℕ)
⊢ Nat.card ((a : α) → β a) = ∏ a : α, Nat.card.{u_3} (β a)
have simp_rw₂ : Eq (α := ℕ) ((toNat : (a : Cardinal.{max u_1 u_3}) → ℕ) (lift.{u_1, u_3} (∏ i : α, #(β i))) : ℕ)
  (∏ x : α, (toNat : (a : Cardinal.{u_3}) → ℕ) #(β x) : ℕ)
Tactic: simp_rw [Nat.card, mk_pi, prod_eq_of_fintype, toNat_lift, _root_.map_prod]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_1
β : α → Type u_3
inst : Fintype α
simp_rw :
  Eq (α := ℕ) ((toNat : (a : Cardinal.{max u_1 u_3}) → ℕ) #((a : α) → β a) : ℕ)
    (∏ x : α, (toNat : (a : Cardinal.{u_3}) → ℕ) #(β x) : ℕ)
simp_rw₁ :
  Eq (α := ℕ) ((toNat : (a : Cardinal.{max u_1 u_3}) → ℕ) (prod.{u_1, u_3} fun (i : α) ↦ #(β i)) : ℕ)
    (∏ x : α, (toNat : (a : Cardinal.{u_3}) → ℕ) #(β x) : ℕ)
simp_rw₂ :
  Eq (α := ℕ) ((toNat : (a : Cardinal.{max u_1 u_3}) → ℕ) (lift.{u_1, u_3} (∏ i : α, #(β i))) : ℕ)
    (∏ x : α, (toNat : (a : Cardinal.{u_3}) → ℕ) #(β x) : ℕ)
⊢ Nat.card ((a : α) → β a) = ∏ a : α, Nat.card.{u_3} (β a)
have simp_rw₃ : Eq (α := ℕ) ((toNat : (a : Cardinal.{u_3}) → ℕ) (∏ i : α, #(β i)) : ℕ)
  (∏ x : α, (toNat : (a : Cardinal.{u_3}) → ℕ) #(β x) : ℕ)
Tactic: simp_rw [Nat.card, mk_pi, prod_eq_of_fintype, toNat_lift, _root_.map_prod]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
⊢ Nat.card (α → β) = Nat.card β ^ Nat.card α
have haveI : ∀ (this : Fintype α), Nat.card (α → β) = Nat.card β ^ Nat.card α
Tactic: haveI := Fintype.ofFinite α
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
this : Fintype α
⊢ Nat.card (α → β) = Nat.card β ^ Nat.card α
have rw : ∏ a : α, Nat.card β = Nat.card β ^ Nat.card α
Tactic: rw [Nat.card_pi, Finset.prod_const, Finset.card_univ, ← Nat.card_eq_fintype_card]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
this : Fintype α
rw : ∏ a : α, Nat.card β = Nat.card β ^ Nat.card α
⊢ Nat.card (α → β) = Nat.card β ^ Nat.card α
have rw₁ : Nat.card β ^ Finset.card.{u_1} (α := α) Finset.univ = Nat.card β ^ Nat.card α
Tactic: rw [Nat.card_pi, Finset.prod_const, Finset.card_univ, ← Nat.card_eq_fintype_card]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
this : Fintype α
rw : ∏ a : α, Nat.card β = Nat.card β ^ Nat.card α
rw₁ : Nat.card β ^ Finset.card.{u_1} (α := α) Finset.univ = Nat.card β ^ Nat.card α
⊢ Nat.card (α → β) = Nat.card β ^ Nat.card α
have rw₂ : Nat.card β ^ Fintype.card α = Nat.card β ^ Nat.card α
Tactic: rw [Nat.card_pi, Finset.prod_const, Finset.card_univ, ← Nat.card_eq_fintype_card]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Finite α
this : Fintype α
rw : ∏ a : α, Nat.card β = Nat.card β ^ Nat.card α
rw₁ : Nat.card β ^ Finset.card.{u_1} (α := α) Finset.univ = Nat.card β ^ Nat.card α
rw₂ : Nat.card β ^ Fintype.card α = Nat.card β ^ Nat.card α
⊢ Nat.card (α → β) = Nat.card β ^ Nat.card α
have rw₃ : Nat.card β ^ Nat.card α = Nat.card β ^ Nat.card α
Tactic: rw [Nat.card_pi, Finset.prod_const, Finset.card_univ, ← Nat.card_eq_fintype_card]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
n : ℕ
⊢ Nat.card (ZMod n) = n
have zero : Nat.card (ZMod 0) = 0
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
n : ℕ
zero : Nat.card (ZMod 0) = 0
⊢ Nat.card (ZMod n) = n
have succ : ∀ (n : ℕ), Nat.card (ZMod (n + 1)) = n + 1
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
n : ℕ
⊢ Nat.card (ZMod (n + 1)) = n + 1
have succ : Fintype.card (ZMod (n + 1)) = n + 1
Tactic: rw [Nat.card_eq_fintype_card, ZMod.card]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
n : ℕ
succ : Fintype.card (ZMod (n + 1)) = n + 1
⊢ Nat.card (ZMod (n + 1)) = n + 1
have succ₁ : n + 1 = n + 1
Tactic: rw [Nat.card_eq_fintype_card, ZMod.card]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
a : α
t : Set β
⊢ Nat.card (↑(SProd.sprod (α := Set α) {a} t) : Type (max u_2 u_1)) = Nat.card.{u_2} (↑t : Type u_2)
have rw : Nat.card (↑(Prod.mk a '' t) : Type (max u_2 u_1)) = Nat.card.{u_2} (↑t : Type u_2)
Tactic: rw [singleton_prod, Nat.card_image_of_injective (Prod.mk_right_injective a)]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
a : α
t : Set β
rw : Nat.card (↑(Prod.mk a '' t) : Type (max u_2 u_1)) = Nat.card.{u_2} (↑t : Type u_2)
⊢ Nat.card (↑(SProd.sprod (α := Set α) {a} t) : Type (max u_2 u_1)) = Nat.card.{u_2} (↑t : Type u_2)
have rw₁ : Nat.card.{u_2} (↑t : Type u_2) = Nat.card.{u_2} (↑t : Type u_2)
Tactic: rw [singleton_prod, Nat.card_image_of_injective (Prod.mk_right_injective a)]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
b : β
⊢ Nat.card (↑(SProd.sprod (β := Set β) s {b}) : Type (max u_1 u_2)) = Nat.card.{u_1} (↑s : Type u_1)
have rw : Nat.card (↑((fun (a : α) ↦ (a, b)) '' s) : Type (max u_1 u_2)) = Nat.card.{u_1} (↑s : Type u_1)
Tactic: rw [prod_singleton, Nat.card_image_of_injective (Prod.mk_left_injective b)]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
b : β
rw : Nat.card (↑((fun (a : α) ↦ (a, b)) '' s) : Type (max u_1 u_2)) = Nat.card.{u_1} (↑s : Type u_1)
⊢ Nat.card (↑(SProd.sprod (β := Set β) s {b}) : Type (max u_1 u_2)) = Nat.card.{u_1} (↑s : Type u_1)
have rw₁ : Nat.card.{u_1} (↑s : Type u_1) = Nat.card.{u_1} (↑s : Type u_1)
Tactic: rw [prod_singleton, Nat.card_image_of_injective (Prod.mk_left_injective b)]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
⊢ Nat.card (↑(graphOn f s) : Type (max u_1 u_2)) = Nat.card.{u_1} (↑s : Type u_1)
have rw : Nat.card.{u_1} (↑(Prod.fst '' graphOn f s) : Type u_1) = Nat.card.{u_1} (↑s : Type u_1)
Tactic: rw [← Nat.card_image_of_injOn fst_injOn_graph, image_fst_graphOn]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
rw : Nat.card.{u_1} (↑(Prod.fst '' graphOn f s) : Type u_1) = Nat.card.{u_1} (↑s : Type u_1)
⊢ Nat.card (↑(graphOn f s) : Type (max u_1 u_2)) = Nat.card.{u_1} (↑s : Type u_1)
have rw₁ : Nat.card.{u_1} (↑s : Type u_1) = Nat.card.{u_1} (↑s : Type u_1)
Tactic: rw [← Nat.card_image_of_injOn fst_injOn_graph, image_fst_graphOn]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_3
β : Type u_4
f : α → β
hf : Injective f
⊢ card α ≤ card β
have rw : card (ULift.{u_4, u_3} α) ≤ card (ULift.{u_3, u_4} β)
Tactic: rw [← card_ulift α, ← card_ulift β]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
n : ℕ
c : Cardinal.{u_3}
⊢ LE.le (α := ℕ∞) ((↑n : ℕ∞) : ℕ∞) ((toENat : (a : Cardinal.{u_3}) → ℕ∞) c : ℕ∞) ↔ (↑n : Cardinal.{u_3}) ≤ c
have rw : LE.le (α := ℕ∞) ((toENat : (a : Cardinal.{u_3}) → ℕ∞) (↑n : Cardinal.{u_3}) : ℕ∞)
    ((toENat : (a : Cardinal.{u_3}) → ℕ∞) c : ℕ∞) ↔
  (↑n : Cardinal.{u_3}) ≤ c
Tactic: rw [← toENat_nat n, toENat_le_iff_of_le_aleph0 natCast_le_aleph0]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
n : ℕ
c : Cardinal.{u_3}
rw :
  LE.le (α := ℕ∞) ((toENat : (a : Cardinal.{u_3}) → ℕ∞) (↑n : Cardinal.{u_3}) : ℕ∞)
      ((toENat : (a : Cardinal.{u_3}) → ℕ∞) c : ℕ∞) ↔
    (↑n : Cardinal.{u_3}) ≤ c
⊢ LE.le (α := ℕ∞) ((↑n : ℕ∞) : ℕ∞) ((toENat : (a : Cardinal.{u_3}) → ℕ∞) c : ℕ∞) ↔ (↑n : Cardinal.{u_3}) ≤ c
have rw₁ : (↑n : Cardinal.{u_3}) ≤ c ↔ (↑n : Cardinal.{u_3}) ≤ c
Tactic: rw [← toENat_nat n, toENat_le_iff_of_le_aleph0 natCast_le_aleph0]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
n : ℕ
c : Cardinal.{u_3}
⊢ Eq (α := ℕ∞) ((↑n : ℕ∞) : ℕ∞) ((toENat : (a : Cardinal.{u_3}) → ℕ∞) c : ℕ∞) ↔ (↑n : Cardinal.{u_3}) = c
have rw : LE.le (α := ℕ∞) ((↑n : ℕ∞) : ℕ∞) ((toENat : (a : Cardinal.{u_3}) → ℕ∞) c : ℕ∞) ∧
    LE.le (α := ℕ∞) ((toENat : (a : Cardinal.{u_3}) → ℕ∞) c : ℕ∞) ((↑n : ℕ∞) : ℕ∞) ↔
  (↑n : Cardinal.{u_3}) = c
Tactic: rw [le_antisymm_iff, le_antisymm_iff, Cardinal.toENat_le_natCast, Cardinal.natCast_le_toENat]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
n : ℕ
c : Cardinal.{u_3}
rw :
  LE.le (α := ℕ∞) ((↑n : ℕ∞) : ℕ∞) ((toENat : (a : Cardinal.{u_3}) → ℕ∞) c : ℕ∞) ∧
      LE.le (α := ℕ∞) ((toENat : (a : Cardinal.{u_3}) → ℕ∞) c : ℕ∞) ((↑n : ℕ∞) : ℕ∞) ↔
    (↑n : Cardinal.{u_3}) = c
⊢ Eq (α := ℕ∞) ((↑n : ℕ∞) : ℕ∞) ((toENat : (a : Cardinal.{u_3}) → ℕ∞) c : ℕ∞) ↔ (↑n : Cardinal.{u_3}) = c
have rw₁ : LE.le (α := ℕ∞) ((↑n : ℕ∞) : ℕ∞) ((toENat : (a : Cardinal.{u_3}) → ℕ∞) c : ℕ∞) ∧
    LE.le (α := ℕ∞) ((toENat : (a : Cardinal.{u_3}) → ℕ∞) c : ℕ∞) ((↑n : ℕ∞) : ℕ∞) ↔
  (↑n : Cardinal.{u_3}) ≤ c ∧ c ≤ (↑n : Cardinal.{u_3})
Tactic: rw [le_antisymm_iff, le_antisymm_iff, Cardinal.toENat_le_natCast, Cardinal.natCast_le_toENat]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
n : ℕ
c : Cardinal.{u_3}
rw :
  LE.le (α := ℕ∞) ((↑n : ℕ∞) : ℕ∞) ((toENat : (a : Cardinal.{u_3}) → ℕ∞) c : ℕ∞) ∧
      LE.le (α := ℕ∞) ((toENat : (a : Cardinal.{u_3}) → ℕ∞) c : ℕ∞) ((↑n : ℕ∞) : ℕ∞) ↔
    (↑n : Cardinal.{u_3}) = c
rw₁ :
  LE.le (α := ℕ∞) ((↑n : ℕ∞) : ℕ∞) ((toENat : (a : Cardinal.{u_3}) → ℕ∞) c : ℕ∞) ∧
      LE.le (α := ℕ∞) ((toENat : (a : Cardinal.{u_3}) → ℕ∞) c : ℕ∞) ((↑n : ℕ∞) : ℕ∞) ↔
    (↑n : Cardinal.{u_3}) ≤ c ∧ c ≤ (↑n : Cardinal.{u_3})
⊢ Eq (α := ℕ∞) ((↑n : ℕ∞) : ℕ∞) ((toENat : (a : Cardinal.{u_3}) → ℕ∞) c : ℕ∞) ↔ (↑n : Cardinal.{u_3}) = c
have rw₂ : LE.le (α := ℕ∞) ((↑n : ℕ∞) : ℕ∞) ((toENat : (a : Cardinal.{u_3}) → ℕ∞) c : ℕ∞) ∧ c ≤ (↑n : Cardinal.{u_3}) ↔
  (↑n : Cardinal.{u_3}) ≤ c ∧ c ≤ (↑n : Cardinal.{u_3})
Tactic: rw [le_antisymm_iff, le_antisymm_iff, Cardinal.toENat_le_natCast, Cardinal.natCast_le_toENat]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
n : ℕ
c : Cardinal.{u_3}
rw :
  LE.le (α := ℕ∞) ((↑n : ℕ∞) : ℕ∞) ((toENat : (a : Cardinal.{u_3}) → ℕ∞) c : ℕ∞) ∧
      LE.le (α := ℕ∞) ((toENat : (a : Cardinal.{u_3}) → ℕ∞) c : ℕ∞) ((↑n : ℕ∞) : ℕ∞) ↔
    (↑n : Cardinal.{u_3}) = c
rw₁ :
  LE.le (α := ℕ∞) ((↑n : ℕ∞) : ℕ∞) ((toENat : (a : Cardinal.{u_3}) → ℕ∞) c : ℕ∞) ∧
      LE.le (α := ℕ∞) ((toENat : (a : Cardinal.{u_3}) → ℕ∞) c : ℕ∞) ((↑n : ℕ∞) : ℕ∞) ↔
    (↑n : Cardinal.{u_3}) ≤ c ∧ c ≤ (↑n : Cardinal.{u_3})
rw₂ :
  LE.le (α := ℕ∞) ((↑n : ℕ∞) : ℕ∞) ((toENat : (a : Cardinal.{u_3}) → ℕ∞) c : ℕ∞) ∧ c ≤ (↑n : Cardinal.{u_3}) ↔
    (↑n : Cardinal.{u_3}) ≤ c ∧ c ≤ (↑n : Cardinal.{u_3})
⊢ Eq (α := ℕ∞) ((↑n : ℕ∞) : ℕ∞) ((toENat : (a : Cardinal.{u_3}) → ℕ∞) c : ℕ∞) ↔ (↑n : Cardinal.{u_3}) = c
have rw₃ : (↑n : Cardinal.{u_3}) ≤ c ∧ c ≤ (↑n : Cardinal.{u_3}) ↔ (↑n : Cardinal.{u_3}) ≤ c ∧ c ≤ (↑n : Cardinal.{u_3})
Tactic: rw [le_antisymm_iff, le_antisymm_iff, Cardinal.toENat_le_natCast, Cardinal.natCast_le_toENat]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_3
⊢ card α = 0 ↔ IsEmpty α
have rw : card α = 0 ↔ #α = 0
Tactic: rw [← Cardinal.mk_eq_zero_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_3
⊢ card α ≤ 1 ↔ Subsingleton α
have rw : card α ≤ 1 ↔ #α ≤ 1
Tactic: rw [← le_one_iff_subsingleton]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_3
⊢ card α = 1 ↔ Nonempty.{max 1 (u_3 + 1)} (Unique α)
have rw : card α ≤ 1 ∧ 1 ≤ card α ↔ Subsingleton α ∧ Nonempty α
Tactic: rw [unique_iff_subsingleton_and_nonempty α, le_antisymm_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_3
⊢ 1 < card α ↔ Nontrivial α
have rw : 1 < card α ↔ 1 < #α
Tactic: rw [← Cardinal.one_lt_iff_nontrivial]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_3
⊢ 1 < card α ↔ (↑1 : Cardinal.{u_3}) < #α
have rw : 1 < card α ↔ LT.lt (α := ℕ∞) ((↑1 : ℕ∞) : ℕ∞) ((toENat : (a : Cardinal.{u_3}) → ℕ∞) #α : ℕ∞)
Tactic: rw [← natCast_lt_toENat]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_3
β : Type u_4
⊢ card (α → β) = card β ^ card α
have inl : ∀ (α_emp : IsEmpty α), card (α → β) = card β ^ card α
Tactic: rcases isEmpty_or_nonempty α with α_emp | α_emp
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_3
β : Type u_4
inl : ∀ (α_emp : IsEmpty α), card (α → β) = card β ^ card α
⊢ card (α → β) = card β ^ card α
have inr : ∀ (α_emp : Nonempty α), card (α → β) = card β ^ card α
Tactic: rcases isEmpty_or_nonempty α with α_emp | α_emp
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_3
β : Type u_4
α_emp : Nonempty α
⊢ card (α → β) = card β ^ card α
have inr : Finite α → card (α → β) = card β ^ card α
Tactic: rcases finite_or_infinite α
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_3
β : Type u_4
α_emp : Nonempty α
inr : Finite α → card (α → β) = card β ^ card α
⊢ card (α → β) = card β ^ card α
have inr₁ : Infinite α → card (α → β) = card β ^ card α
Tactic: rcases finite_or_infinite α
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h : Finite α
⊢ card (α → β) = card β ^ card α
have inr : Finite β → card (α → β) = card β ^ card α
Tactic: rcases finite_or_infinite β
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h : Finite α
inr : Finite β → card (α → β) = card β ^ card α
⊢ card (α → β) = card β ^ card α
have inr₁ : Infinite β → card (α → β) = card β ^ card α
Tactic: rcases finite_or_infinite β
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h : Finite α
h_1 : Infinite β
⊢ card (α → β) = card β ^ card α
have inr : ⊤ = HPow.hPow (α := ℕ∞) ⊤ (card α)
Tactic: simp only [card_eq_top_of_infinite]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h : Infinite α
⊢ card (α → β) = card β ^ card α
have inr : card (α → β) = HPow.hPow (β := ℕ∞) (card β) ⊤
Tactic: rw [card_eq_top_of_infinite (α := α)]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h : Infinite α
⊢ card (α → β) = HPow.hPow (β := ℕ∞) (card β) ⊤
have inr : ∀ (b_0 : card β < 1), card (α → β) = HPow.hPow (β := ℕ∞) (card β) ⊤
Tactic: rcases lt_trichotomy (card β) 1 with b_0 | b_1 | b_2
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h : Infinite α
inr : ∀ (b_0 : card β < 1), card (α → β) = HPow.hPow (β := ℕ∞) (card β) ⊤
⊢ card (α → β) = HPow.hPow (β := ℕ∞) (card β) ⊤
have inr₁ : ∀ (b_1 : card β = 1), card (α → β) = HPow.hPow (β := ℕ∞) (card β) ⊤
Tactic: rcases lt_trichotomy (card β) 1 with b_0 | b_1 | b_2
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h : Infinite α
inr : ∀ (b_0 : card β < 1), card (α → β) = HPow.hPow (β := ℕ∞) (card β) ⊤
inr₁ : ∀ (b_1 : card β = 1), card (α → β) = HPow.hPow (β := ℕ∞) (card β) ⊤
⊢ card (α → β) = HPow.hPow (β := ℕ∞) (card β) ⊤
have inr₂ : ∀ (b_2 : 1 < card β), card (α → β) = HPow.hPow (β := ℕ∞) (card β) ⊤
Tactic: rcases lt_trichotomy (card β) 1 with b_0 | b_1 | b_2
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (hypothesis)
Goal:
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h : Infinite α
b_0 : card β < 1
⊢ card (α → β) = HPow.hPow (β := ℕ∞) (card β) ⊤
have b_0₁ : IsEmpty β
Tactic: rw [lt_one_iff_eq_zero, card_eq_zero_iff_empty] at b_0
Cleared hypotheses: b_0
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h : Infinite α
b_0 : IsEmpty β
⊢ card (α → β) = HPow.hPow (β := ℕ∞) (card β) ⊤
have inr : IsEmpty (α → β)
Tactic: rw [(card_eq_zero_iff_empty β).2 b_0, zero_epow_top, card_eq_zero_iff_empty]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h : Infinite α
b_1 : card β = 1
⊢ card (α → β) = HPow.hPow (β := ℕ∞) (card β) ⊤
have inr : card (α → β) = 1
Tactic: rw [b_1, one_epow]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h : Infinite α
b_1 : card β = 1
⊢ card (α → β) = 1
have inr : card (α → β) ≤ 1
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h : Infinite α
b_1 : card β = 1
inr : card (α → β) ≤ 1
⊢ card (α → β) = 1
have inr₁ : 1 ≤ card (α → β)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h : Infinite α
b_2 : 1 < card β
⊢ card (α → β) = HPow.hPow (β := ℕ∞) (card β) ⊤
have inr : Infinite (α → β)
Tactic: rw [epow_top b_2, card_eq_top]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (hypothesis)
Goal:
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h : Infinite α
b_2 : 1 < card β
⊢ Infinite (α → β)
have b_2₁ : Nontrivial β
Tactic: rw [one_lt_card_iff_nontrivial β] at b_2
Cleared hypotheses: b_2
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_3
β : Type u_4
⊢ card (α → β) = card β ^ card α
have inl : ∀ (α_emp : IsEmpty α), card (α → β) = card β ^ card α
Tactic: classical
  rcases isEmpty_or_nonempty α with α_emp | α_emp
  · simp [(card_eq_zero_iff_empty α).2 α_emp]
  rcases finite_or_infinite α
  · rcases finite_or_infinite β
    · letI := Fintype.ofFinite α
      letI := Fintype.ofFinite β
      simp
    · simp only [card_eq_top_of_infinite]
      exact (top_epow (one_le_iff_ne_zero.1 ((one_le_card_iff_nonempty α).2 α_emp))).symm
  · rw [card_eq_top_of_infinite (α := α)]
    rcases lt_trichotomy (card β) 1 with b_0 | b_1 | b_2
    · rw [lt_one_iff_eq_zero, card_eq_zero_iff_empty] at b_0
      rw [(card_eq_zero_iff_empty β).2 b_0, zero_epow_top, card_eq_zero_iff_empty]
      simp [b_0]
    · rw [b_1, one_epow]
      apply le_antisymm
      · letI := (card_le_one_iff_subsingleton β).1 b_1.le
        exact (card_le_one_iff_subsingleton (α → β)).2 Pi.instSubsingleton
      · letI := (one_le_card_iff_nonempty β).1 b_1.ge
        exact (one_le_card_iff_nonempty (α → β)).2 Pi.instNonempty
    · rw [epow_top b_2, card_eq_top]
      rw [one_lt_card_iff_nontrivial β] at b_2
      exact Pi.infinite_of_left
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Finite (goal)
Goal:
α : Type u_3
β : Type u_4
inl : ∀ (α_emp : IsEmpty α), card (α → β) = card β ^ card α
⊢ card (α → β) = card β ^ card α
have inr : ∀ (α_emp : Nonempty α), card (α → β) = card β ^ card α
Tactic: classical
  rcases isEmpty_or_nonempty α with α_emp | α_emp
  · simp [(card_eq_zero_iff_empty α).2 α_emp]
  rcases finite_or_infinite α
  · rcases finite_or_infinite β
    · letI := Fintype.ofFinite α
      letI := Fintype.ofFinite β
      simp
    · simp only [card_eq_top_of_infinite]
      exact (top_epow (one_le_iff_ne_zero.1 ((one_le_card_iff_nonempty α).2 α_emp))).symm
  · rw [card_eq_top_of_infinite (α := α)]
    rcases lt_trichotomy (card β) 1 with b_0 | b_1 | b_2
    · rw [lt_one_iff_eq_zero, card_eq_zero_iff_empty] at b_0
      rw [(card_eq_zero_iff_empty β).2 b_0, zero_epow_top, card_eq_zero_iff_empty]
      simp [b_0]
    · rw [b_1, one_epow]
      apply le_antisymm
      · letI := (card_le_one_iff_subsingleton β).1 b_1.le
        exact (card_le_one_iff_subsingleton (α → β)).2 Pi.instSubsingleton
      · letI := (one_le_card_iff_nonempty β).1 b_1.ge
        exact (one_le_card_iff_nonempty (α → β)).2 Pi.instNonempty
    · rw [epow_top b_2, card_eq_top]
      rw [one_lt_card_iff_nontrivial β] at b_2
      exact Pi.infinite_of_left