awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
ι : Type u
inst : Infinite ι
c : ι → Cardinal.{v}
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift.{u, v} (c i) ≤ lift.{v, u} #ι
a : lift.{u, max u v} (lift.{v, u} #ι) ^ lift.{max u v, u} #ι = lift.{v, u} (HPow.hPow (α := Cardinal.{u}) 2 #ι)
a₁ : lift.{max v u, u} #ι ^ lift.{max u v, u} #ι = lift.{v, u} (HPow.hPow (α := Cardinal.{u}) 2 #ι)
a₂ : lift.{max u v, u} (#ι ^ #ι) = lift.{v, u} (HPow.hPow (α := Cardinal.{u}) 2 #ι)
⊢ (prod fun (i : ι) ↦ lift.{v, u} #ι) = lift.{v, u} (HPow.hPow (α := Cardinal.{u}) 2 #ι)
have a₃ : lift.{max u v, u} (HPow.hPow (α := Cardinal.{u}) 2 #ι) = lift.{v, u} (HPow.hPow (α := Cardinal.{u}) 2 #ι)
Tactic: rw [prod_const, lift_lift, ← lift_power, power_self_eq (aleph0_le_mk ι), lift_umax.{u, v}]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
ι : Type u
inst : Infinite ι
c : ι → Cardinal.{v}
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift.{u, v} (c i) ≤ lift.{v, u} #ι
a : lift.{u, max u v} (lift.{v, u} #ι) ^ lift.{max u v, u} #ι = lift.{v, u} (HPow.hPow (α := Cardinal.{u}) 2 #ι)
a₁ : lift.{max v u, u} #ι ^ lift.{max u v, u} #ι = lift.{v, u} (HPow.hPow (α := Cardinal.{u}) 2 #ι)
a₂ : lift.{max u v, u} (#ι ^ #ι) = lift.{v, u} (HPow.hPow (α := Cardinal.{u}) 2 #ι)
a₃ : lift.{max u v, u} (HPow.hPow (α := Cardinal.{u}) 2 #ι) = lift.{v, u} (HPow.hPow (α := Cardinal.{u}) 2 #ι)
⊢ (prod fun (i : ι) ↦ lift.{v, u} #ι) = lift.{v, u} (HPow.hPow (α := Cardinal.{u}) 2 #ι)
have a₄ : lift.{v, u} (HPow.hPow (α := Cardinal.{u}) 2 #ι) = lift.{v, u} (HPow.hPow (α := Cardinal.{u}) 2 #ι)
Tactic: rw [prod_const, lift_lift, ← lift_power, power_self_eq (aleph0_le_mk ι), lift_umax.{u, v}]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
ι : Type u
inst : Infinite ι
c : ι → Cardinal.{v}
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift.{u, v} (c i) ≤ lift.{v, u} #ι
⊢ lift.{v, u} (HPow.hPow (α := Cardinal.{u}) 2 #ι) ≤ prod fun (i : ι) ↦ lift.{u, v} (c i)
have a : (prod fun (i : ι) ↦ lift.{v, u} 2) ≤ prod fun (i : ι) ↦ lift.{u, v} (c i)
Tactic: rw [← prod_const', lift_prod]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
ι : Type u
inst : Infinite ι
c : ι → Cardinal.{v}
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift.{u, v} (c i) ≤ lift.{v, u} #ι
⊢ (prod fun (i : ι) ↦ lift.{v, u} 2) ≤ prod fun (i : ι) ↦ lift.{u, v} (c i)
have a : ∀ (i : ι), lift.{v, u} 2 ≤ lift.{u, v} (c i)
Tactic: refine prod_le_prod _ _ fun i => ?_
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
ι : Type u
inst : Infinite ι
c : ι → Cardinal.{v}
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift.{u, v} (c i) ≤ lift.{v, u} #ι
i : ι
⊢ lift.{v, u} 2 ≤ lift.{u, v} (c i)
have a : 2 ≤ c i
Tactic: rw [lift_two, ← lift_two.{u, v}, lift_le]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
c : Cardinal.{u}
n : ℕ
⊢ HPow.hPow (β := Cardinal.{u}) c (↑n : Cardinal.{u}) ≤ max c ℵ₀
have inl : ∀ (hc : ℵ₀ ≤ c), HPow.hPow (β := Cardinal.{u}) c (↑n : Cardinal.{u}) ≤ max c ℵ₀
Tactic: rcases le_or_gt ℵ₀ c with hc | hc
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
c : Cardinal.{u}
n : ℕ
inl : ∀ (hc : ℵ₀ ≤ c), HPow.hPow (β := Cardinal.{u}) c (↑n : Cardinal.{u}) ≤ max c ℵ₀
⊢ HPow.hPow (β := Cardinal.{u}) c (↑n : Cardinal.{u}) ≤ max c ℵ₀
have inr : ∀ (hc : c < ℵ₀), HPow.hPow (β := Cardinal.{u}) c (↑n : Cardinal.{u}) ≤ max c ℵ₀
Tactic: rcases le_or_gt ℵ₀ c with hc | hc
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
a b : Cardinal.{u}
ha : a ≤ ℵ₀
hb : b < ℵ₀
⊢ a ^ b ≤ ℵ₀
have lift : ∀ (b : ℕ), HPow.hPow (β := Cardinal.{u}) a (↑b : Cardinal.{u}) ≤ ℵ₀
Tactic: lift b to ℕ using hb
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c ^< ℵ₀ = c
have a : c ^< ℵ₀ ≤ c
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
a : c ^< ℵ₀ ≤ c
⊢ c ^< ℵ₀ = c
have a₁ : c ≤ c ^< ℵ₀
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c ^< ℵ₀ ≤ c
have a : ∀ x < ℵ₀, c ^ x ≤ c
Tactic: rw [powerlt_le]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c ≤ c ^< ℵ₀
have h₁ : c = HPow.hPow (β := Cardinal.{u_1}) c 1
Tactic: convert! le_powerlt c one_lt_aleph0
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c = HPow.hPow (β := Cardinal.{u_1}) c 1
have h₁ : c = c
Tactic: rw [power_one]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
c : Cardinal.{u_1}
⊢ c ^< ℵ₀ ≤ max c ℵ₀
have inl : ∀ (h : ℵ₀ ≤ c), c ^< ℵ₀ ≤ max c ℵ₀
Tactic: rcases le_or_gt ℵ₀ c with h | h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
c : Cardinal.{u_1}
inl : ∀ (h : ℵ₀ ≤ c), c ^< ℵ₀ ≤ max c ℵ₀
⊢ c ^< ℵ₀ ≤ max c ℵ₀
have inr : ∀ (h : c < ℵ₀), c ^< ℵ₀ ≤ max c ℵ₀
Tactic: rcases le_or_gt ℵ₀ c with h | h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c ^< ℵ₀ ≤ max c ℵ₀
have inl : c ≤ max c ℵ₀
Tactic: rw [powerlt_aleph0 h]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
c : Cardinal.{u_1}
h : c < ℵ₀
⊢ c ^< ℵ₀ ≤ max c ℵ₀
have inr : ∀ x < ℵ₀, c ^ x ≤ max c ℵ₀
Tactic: rw [powerlt_le]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
β' : Type v
⊢ #(α ≃ β') = 0 ↔ lift.{v, u} #α ≠ lift.{u, v} #β'
have rw : IsEmpty (α ≃ β') ↔ lift.{v, u} #α ≠ lift.{u, v} #β'
Tactic: rw [mk_eq_zero_iff, ← not_nonempty_iff, ← lift_mk_eq']
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
β' : Type v
rw : IsEmpty (α ≃ β') ↔ lift.{v, u} #α ≠ lift.{u, v} #β'
⊢ #(α ≃ β') = 0 ↔ lift.{v, u} #α ≠ lift.{u, v} #β'
have rw₁ : ¬Nonempty (α ≃ β') ↔ lift.{v, u} #α ≠ lift.{u, v} #β'
Tactic: rw [mk_eq_zero_iff, ← not_nonempty_iff, ← lift_mk_eq']
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
β' : Type v
rw : IsEmpty (α ≃ β') ↔ lift.{v, u} #α ≠ lift.{u, v} #β'
rw₁ : ¬Nonempty (α ≃ β') ↔ lift.{v, u} #α ≠ lift.{u, v} #β'
⊢ #(α ≃ β') = 0 ↔ lift.{v, u} #α ≠ lift.{u, v} #β'
have rw₂ : ¬lift.{v, u} #α = lift.{u, v} #β' ↔ lift.{v, u} #α ≠ lift.{u, v} #β'
Tactic: rw [mk_eq_zero_iff, ← not_nonempty_iff, ← lift_mk_eq']
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α β : Type u
⊢ #(α ≃ β) = 0 ↔ #α ≠ #β
have rw : lift.{u, u} #α ≠ lift.{u, u} #β ↔ #α ≠ #β
Tactic: rw [mk_equiv_eq_zero_iff_lift_ne, lift_id, lift_id]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α β : Type u
rw : lift.{u, u} #α ≠ lift.{u, u} #β ↔ #α ≠ #β
⊢ #(α ≃ β) = 0 ↔ #α ≠ #β
have rw₁ : #α ≠ lift.{u, u} #β ↔ #α ≠ #β
Tactic: rw [mk_equiv_eq_zero_iff_lift_ne, lift_id, lift_id]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α β : Type u
rw : lift.{u, u} #α ≠ lift.{u, u} #β ↔ #α ≠ #β
rw₁ : #α ≠ lift.{u, u} #β ↔ #α ≠ #β
⊢ #(α ≃ β) = 0 ↔ #α ≠ #β
have rw₂ : #α ≠ #β ↔ #α ≠ #β
Tactic: rw [mk_equiv_eq_zero_iff_lift_ne, lift_id, lift_id]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
β' : Type v
⊢ #(α ↪ β') = 0 ↔ lift.{u, v} #β' < lift.{v, u} #α
have rw : IsEmpty (α ↪ β') ↔ lift.{u, v} #β' < lift.{v, u} #α
Tactic: rw [mk_eq_zero_iff, ← not_nonempty_iff, ← lift_mk_le', not_le]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
β' : Type v
rw : IsEmpty (α ↪ β') ↔ lift.{u, v} #β' < lift.{v, u} #α
⊢ #(α ↪ β') = 0 ↔ lift.{u, v} #β' < lift.{v, u} #α
have rw₁ : ¬Nonempty (α ↪ β') ↔ lift.{u, v} #β' < lift.{v, u} #α
Tactic: rw [mk_eq_zero_iff, ← not_nonempty_iff, ← lift_mk_le', not_le]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
β' : Type v
rw : IsEmpty (α ↪ β') ↔ lift.{u, v} #β' < lift.{v, u} #α
rw₁ : ¬Nonempty (α ↪ β') ↔ lift.{u, v} #β' < lift.{v, u} #α
⊢ #(α ↪ β') = 0 ↔ lift.{u, v} #β' < lift.{v, u} #α
have rw₂ : ¬lift.{v, u} #α ≤ lift.{u, v} #β' ↔ lift.{u, v} #β' < lift.{v, u} #α
Tactic: rw [mk_eq_zero_iff, ← not_nonempty_iff, ← lift_mk_le', not_le]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
β' : Type v
rw : IsEmpty (α ↪ β') ↔ lift.{u, v} #β' < lift.{v, u} #α
rw₁ : ¬Nonempty (α ↪ β') ↔ lift.{u, v} #β' < lift.{v, u} #α
rw₂ : ¬lift.{v, u} #α ≤ lift.{u, v} #β' ↔ lift.{u, v} #β' < lift.{v, u} #α
⊢ #(α ↪ β') = 0 ↔ lift.{u, v} #β' < lift.{v, u} #α
have rw₃ : lift.{u, v} #β' < lift.{v, u} #α ↔ lift.{u, v} #β' < lift.{v, u} #α
Tactic: rw [mk_eq_zero_iff, ← not_nonempty_iff, ← lift_mk_le', not_le]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α β : Type u
⊢ #(α ↪ β) = 0 ↔ #β < #α
have rw : lift.{u, u} #β < lift.{u, u} #α ↔ #β < #α
Tactic: rw [mk_embedding_eq_zero_iff_lift_lt, lift_lt]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α β : Type u
rw : lift.{u, u} #β < lift.{u, u} #α ↔ #β < #α
⊢ #(α ↪ β) = 0 ↔ #β < #α
have rw₁ : #β < #α ↔ #β < #α
Tactic: rw [mk_embedding_eq_zero_iff_lift_lt, lift_lt]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
β' : Type v
⊢ #(α → β') = 0 ↔ #α ≠ 0 ∧ #β' = 0
have simp_rw : IsEmpty (α → β') ↔ #α ≠ 0 ∧ IsEmpty β'
Tactic: simp_rw [mk_eq_zero_iff, mk_ne_zero_iff, isEmpty_fun]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
β' : Type v
simp_rw : IsEmpty (α → β') ↔ #α ≠ 0 ∧ IsEmpty β'
⊢ #(α → β') = 0 ↔ #α ≠ 0 ∧ #β' = 0
have simp_rw₁ : IsEmpty (α → β') ↔ Nonempty α ∧ IsEmpty β'
Tactic: simp_rw [mk_eq_zero_iff, mk_ne_zero_iff, isEmpty_fun]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
β' : Type v
⊢ #(↑{f : α → β' | Surjective f} : Type (max u v)) = 0 ↔ lift.{v, u} #α < lift.{u, v} #β' ∨ #α ≠ 0 ∧ #β' = 0
have contrapose! : #(↑{f : α → β' | Surjective f} : Type (max u v)) ≠ 0 ↔ lift.{u, v} #β' ≤ lift.{v, u} #α ∧ (#α = 0 ∨ #β' ≠ 0)
Tactic: contrapose! +distrib
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
β' : Type v
⊢ #(↑{f : α → β' | Surjective f} : Type (max u v)) ≠ 0 ↔ lift.{u, v} #β' ≤ lift.{v, u} #α ∧ (#α = 0 ∨ #β' ≠ 0)
have rw : #(↑{f : α → β' | Surjective f} : Type (max u v)) ≠ 0 ↔ (#α = 0 ∨ #β' ≠ 0) ∧ Nonempty (β' ↪ α)
Tactic: rw [lift_mk_le', and_comm]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
β' : Type v
⊢ #(↑{f : α → β' | Surjective f} : Type (max u v)) ≠ 0 ↔ (#α = 0 ∨ #β' ≠ 0) ∧ Nonempty (β' ↪ α)
have simp_rw : Nonempty (↑{f : α → β' | Surjective f} : Type (max u v)) ↔ (#α = 0 ∨ Nonempty β') ∧ Nonempty (β' ↪ α)
Tactic: simp_rw [mk_ne_zero_iff, mk_eq_zero_iff, nonempty_coe_sort,
    Set.Nonempty, mem_setOf, exists_surjective_iff, nonempty_fun]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
β' : Type v
simp_rw : Nonempty (↑{f : α → β' | Surjective f} : Type (max u v)) ↔ (#α = 0 ∨ Nonempty β') ∧ Nonempty (β' ↪ α)
⊢ #(↑{f : α → β' | Surjective f} : Type (max u v)) ≠ 0 ↔ (#α = 0 ∨ #β' ≠ 0) ∧ Nonempty (β' ↪ α)
have simp_rw₁ : Nonempty (↑{f : α → β' | Surjective f} : Type (max u v)) ↔ (IsEmpty α ∨ Nonempty β') ∧ Nonempty (β' ↪ α)
Tactic: simp_rw [mk_ne_zero_iff, mk_eq_zero_iff, nonempty_coe_sort,
    Set.Nonempty, mem_setOf, exists_surjective_iff, nonempty_fun]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
β' : Type v
simp_rw : Nonempty (↑{f : α → β' | Surjective f} : Type (max u v)) ↔ (#α = 0 ∨ Nonempty β') ∧ Nonempty (β' ↪ α)
simp_rw₁ : Nonempty (↑{f : α → β' | Surjective f} : Type (max u v)) ↔ (IsEmpty α ∨ Nonempty β') ∧ Nonempty (β' ↪ α)
⊢ #(↑{f : α → β' | Surjective f} : Type (max u v)) ≠ 0 ↔ (#α = 0 ∨ #β' ≠ 0) ∧ Nonempty (β' ↪ α)
have simp_rw₂ : Set.Nonempty (α := α → β') {f : α → β' | Surjective f} ↔ (IsEmpty α ∨ Nonempty β') ∧ Nonempty (β' ↪ α)
Tactic: simp_rw [mk_ne_zero_iff, mk_eq_zero_iff, nonempty_coe_sort,
    Set.Nonempty, mem_setOf, exists_surjective_iff, nonempty_fun]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
β' : Type v
simp_rw : Nonempty (↑{f : α → β' | Surjective f} : Type (max u v)) ↔ (#α = 0 ∨ Nonempty β') ∧ Nonempty (β' ↪ α)
simp_rw₁ : Nonempty (↑{f : α → β' | Surjective f} : Type (max u v)) ↔ (IsEmpty α ∨ Nonempty β') ∧ Nonempty (β' ↪ α)
simp_rw₂ : Set.Nonempty (α := α → β') {f : α → β' | Surjective f} ↔ (IsEmpty α ∨ Nonempty β') ∧ Nonempty (β' ↪ α)
⊢ #(↑{f : α → β' | Surjective f} : Type (max u v)) ≠ 0 ↔ (#α = 0 ∨ #β' ≠ 0) ∧ Nonempty (β' ↪ α)
have simp_rw₃ : (∃ (x : α → β'), Membership.mem (γ := Set (α → β')) {f : α → β' | Surjective f} x) ↔
  (IsEmpty α ∨ Nonempty β') ∧ Nonempty (β' ↪ α)
Tactic: simp_rw [mk_ne_zero_iff, mk_eq_zero_iff, nonempty_coe_sort,
    Set.Nonempty, mem_setOf, exists_surjective_iff, nonempty_fun]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
β' : Type v
simp_rw : Nonempty (↑{f : α → β' | Surjective f} : Type (max u v)) ↔ (#α = 0 ∨ Nonempty β') ∧ Nonempty (β' ↪ α)
simp_rw₁ : Nonempty (↑{f : α → β' | Surjective f} : Type (max u v)) ↔ (IsEmpty α ∨ Nonempty β') ∧ Nonempty (β' ↪ α)
simp_rw₂ : Set.Nonempty (α := α → β') {f : α → β' | Surjective f} ↔ (IsEmpty α ∨ Nonempty β') ∧ Nonempty (β' ↪ α)
simp_rw₃ :
  (∃ (x : α → β'), Membership.mem (γ := Set (α → β')) {f : α → β' | Surjective f} x) ↔
    (IsEmpty α ∨ Nonempty β') ∧ Nonempty (β' ↪ α)
⊢ #(↑{f : α → β' | Surjective f} : Type (max u v)) ≠ 0 ↔ (#α = 0 ∨ #β' ≠ 0) ∧ Nonempty (β' ↪ α)
have simp_rw₄ : (∃ (f : α → β'), Surjective f) ↔ (IsEmpty α ∨ Nonempty β') ∧ Nonempty (β' ↪ α)
Tactic: simp_rw [mk_ne_zero_iff, mk_eq_zero_iff, nonempty_coe_sort,
    Set.Nonempty, mem_setOf, exists_surjective_iff, nonempty_fun]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
β' : Type v
simp_rw : Nonempty (↑{f : α → β' | Surjective f} : Type (max u v)) ↔ (#α = 0 ∨ Nonempty β') ∧ Nonempty (β' ↪ α)
simp_rw₁ : Nonempty (↑{f : α → β' | Surjective f} : Type (max u v)) ↔ (IsEmpty α ∨ Nonempty β') ∧ Nonempty (β' ↪ α)
simp_rw₂ : Set.Nonempty (α := α → β') {f : α → β' | Surjective f} ↔ (IsEmpty α ∨ Nonempty β') ∧ Nonempty (β' ↪ α)
simp_rw₃ :
  (∃ (x : α → β'), Membership.mem (γ := Set (α → β')) {f : α → β' | Surjective f} x) ↔
    (IsEmpty α ∨ Nonempty β') ∧ Nonempty (β' ↪ α)
simp_rw₄ : (∃ (f : α → β'), Surjective f) ↔ (IsEmpty α ∨ Nonempty β') ∧ Nonempty (β' ↪ α)
⊢ #(↑{f : α → β' | Surjective f} : Type (max u v)) ≠ 0 ↔ (#α = 0 ∨ #β' ≠ 0) ∧ Nonempty (β' ↪ α)
have simp_rw₅ : Nonempty (α → β') ∧ Nonempty (β' ↪ α) ↔ (IsEmpty α ∨ Nonempty β') ∧ Nonempty (β' ↪ α)
Tactic: simp_rw [mk_ne_zero_iff, mk_eq_zero_iff, nonempty_coe_sort,
    Set.Nonempty, mem_setOf, exists_surjective_iff, nonempty_fun]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α β : Type u
⊢ #(↑{f : α → β | Surjective f} : Type u) = 0 ↔ #α < #β ∨ #α ≠ 0 ∧ #β = 0
have rw : lift.{u, u} #α < lift.{u, u} #β ∨ #α ≠ 0 ∧ #β = 0 ↔ #α < #β ∨ #α ≠ 0 ∧ #β = 0
Tactic: rw [mk_surjective_eq_zero_iff_lift, lift_lt]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α β : Type u
rw : lift.{u, u} #α < lift.{u, u} #β ∨ #α ≠ 0 ∧ #β = 0 ↔ #α < #β ∨ #α ≠ 0 ∧ #β = 0
⊢ #(↑{f : α → β | Surjective f} : Type u) = 0 ↔ #α < #β ∨ #α ≠ 0 ∧ #β = 0
have rw₁ : #α < #β ∨ #α ≠ 0 ∧ #β = 0 ↔ #α < #β ∨ #α ≠ 0 ∧ #β = 0
Tactic: rw [mk_surjective_eq_zero_iff_lift, lift_lt]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
inst : Infinite α
this : Nonempty.{max 1 (u + 1)} ((α → Bool) ↪ Perm (α × Bool))
⊢ #(α → α) ≤ #(α ≃ α)
have obtain : ∀ (e : α ≃ α × Bool), #(α → α) ≤ #(α ≃ α)
Tactic: obtain ⟨e⟩ : Nonempty (α ≃ α × Bool) := by simp [← Cardinal.eq, mul_two]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (hypothesis)
Goal:
α : Type u
inst : Infinite α
this : Nonempty.{max 1 (u + 1)} ((α → Bool) ↪ Perm (α × Bool))
e : α ≃ α × Bool
⊢ #(α → α) ≤ #(α ≃ α)
have this₁ : HPow.hPow (α := Cardinal.{u}) 2 #α ≤ #(Perm (α × Bool))
Tactic: simp only [← le_def, mk_pi, mk_fintype, Fintype.card_bool, Nat.cast_ofNat,
        prod_const, lift_ofNat, lift_uzero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
inst : Infinite α
e : α ≃ α × Bool
this : HPow.hPow (α := Cardinal.{u}) 2 #α ≤ #(Perm (α × Bool))
⊢ #(α → α) ≤ #(α ≃ α)
have rwa : #α ^ #α ≤ #(α ≃ α)
Tactic: rwa [← power_def, power_self_eq (aleph0_le_mk α), e.permCongr.cardinal_eq]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
inst : Infinite α
e : α ≃ α × Bool
this : HPow.hPow (α := Cardinal.{u}) 2 #α ≤ #(Perm (α × Bool))
rwa : #α ^ #α ≤ #(α ≃ α)
⊢ #(α → α) ≤ #(α ≃ α)
have rwa₁ : HPow.hPow (α := Cardinal.{u}) 2 #α ≤ #(α ≃ α)
Tactic: rwa [← power_def, power_self_eq (aleph0_le_mk α), e.permCongr.cardinal_eq]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
inst : Infinite α
⊢ #(α → α) ≤ #(α ≃ α)
have suffices : Nonempty.{max 1 (u + 1)} ((α → Bool) ↪ Perm (α × Bool))
Tactic: suffices Nonempty ((α → Bool) ↪ Equiv.Perm (α × Bool)) by
      obtain ⟨e⟩ : Nonempty (α ≃ α × Bool) := by simp [← Cardinal.eq, mul_two]
      simp only [← le_def, mk_pi, mk_fintype, Fintype.card_bool, Nat.cast_ofNat,
        prod_const, lift_ofNat, lift_uzero] at this
      rwa [← power_def, power_self_eq (aleph0_le_mk α), e.permCongr.cardinal_eq]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
inst : Infinite α
⊢ Nonempty.{max 1 (u + 1)} ((α → Bool) ↪ Perm (α × Bool))
have refine_1 : ∀ (f : α → Bool) (x : α × Bool),
  (fun (x : α × Bool) ↦ (x.1, f x.1 ^^ x.2)) ((fun (x : α × Bool) ↦ (x.1, f x.1 ^^ x.2)) x) = x
Tactic: refine ⟨⟨fun f ↦ Involutive.toPerm (fun x ↦ ⟨x.1, xor (f x.1) x.2⟩) fun x ↦ ?_, fun f g h ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
inst : Infinite α
refine_1 :
  ∀ (f : α → Bool) (x : α × Bool),
    (fun (x : α × Bool) ↦ (x.1, f x.1 ^^ x.2)) ((fun (x : α × Bool) ↦ (x.1, f x.1 ^^ x.2)) x) = x
⊢ Nonempty.{max 1 (u + 1)} ((α → Bool) ↪ Perm (α × Bool))
have refine_2 : ∀ (f g : α → Bool)
  (h :
    Eq.{u + 1} (α := Perm (α × Bool))
      ((fun (f : α → Bool) ↦ (Involutive.toPerm (fun (x : α × Bool) ↦ (x.1, f x.1 ^^ x.2)) sorry : Perm (α × Bool))) f)
      ((fun (f : α → Bool) ↦ (Involutive.toPerm (fun (x : α × Bool) ↦ (x.1, f x.1 ^^ x.2)) sorry : Perm (α × Bool))) g)),
  f = g
Tactic: refine ⟨⟨fun f ↦ Involutive.toPerm (fun x ↦ ⟨x.1, xor (f x.1) x.2⟩) fun x ↦ ?_, fun f g h ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
inst : Infinite α
f : α → Bool
x : α × Bool
⊢ (fun (x : α × Bool) ↦ (x.1, f x.1 ^^ x.2)) ((fun (x : α × Bool) ↦ (x.1, f x.1 ^^ x.2)) x) = x
have refine_1 : (x.1, f x.1 ^^ (f x.1 ^^ x.2)) = x
Tactic: simp_rw [← Bool.xor_assoc, Bool.xor_self, Bool.false_xor]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
inst : Infinite α
f : α → Bool
x : α × Bool
refine_1 refine_1₁ : (x.1, f x.1 ^^ (f x.1 ^^ x.2)) = x
⊢ (fun (x : α × Bool) ↦ (x.1, f x.1 ^^ x.2)) ((fun (x : α × Bool) ↦ (x.1, f x.1 ^^ x.2)) x) = x
have refine_1₂ : (x.1, f x.1 ^^ f x.1 ^^ x.2) = x
Tactic: simp_rw [← Bool.xor_assoc, Bool.xor_self, Bool.false_xor]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
inst : Infinite α
f : α → Bool
x : α × Bool
refine_1 refine_1₁ : (x.1, f x.1 ^^ (f x.1 ^^ x.2)) = x
refine_1₂ : (x.1, f x.1 ^^ f x.1 ^^ x.2) = x
⊢ (fun (x : α × Bool) ↦ (x.1, f x.1 ^^ x.2)) ((fun (x : α × Bool) ↦ (x.1, f x.1 ^^ x.2)) x) = x
have refine_1₃ : (x.1, false ^^ x.2) = x
Tactic: simp_rw [← Bool.xor_assoc, Bool.xor_self, Bool.false_xor]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
inst : Infinite α
f g : α → Bool
h :
  Eq.{u + 1} (α := Perm (α × Bool))
    ((fun (f : α → Bool) ↦ (Involutive.toPerm (fun (x : α × Bool) ↦ (x.1, f x.1 ^^ x.2)) ⋯ : Perm (α × Bool))) f)
    ((fun (f : α → Bool) ↦ (Involutive.toPerm (fun (x : α × Bool) ↦ (x.1, f x.1 ^^ x.2)) ⋯ : Perm (α × Bool))) g)
⊢ f = g
have refine_2 : ∀ (a : α), f a = g a
Tactic: ext a
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
inst : Infinite α
f g : α → Bool
h :
  Eq.{u + 1} (α := Perm (α × Bool))
    ((fun (f : α → Bool) ↦ (Involutive.toPerm (fun (x : α × Bool) ↦ (x.1, f x.1 ^^ x.2)) ⋯ : Perm (α × Bool))) f)
    ((fun (f : α → Bool) ↦ (Involutive.toPerm (fun (x : α × Bool) ↦ (x.1, f x.1 ^^ x.2)) ⋯ : Perm (α × Bool))) g)
a : α
⊢ f a = g a
have refine_2 : (f a ^^ false) = (g a ^^ false)
Tactic: rw [← (f a).xor_false, ← (g a).xor_false]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
inst : Infinite α
⊢ #(Perm α) = HPow.hPow (α := Cardinal.{u}) 2 #α
have rw : #α ^ #α = HPow.hPow (α := Cardinal.{u}) 2 #α
Tactic: rw [mk_perm_eq_self_power, power_self_eq (aleph0_le_mk α)]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
inst : Infinite α
rw : #α ^ #α = HPow.hPow (α := Cardinal.{u}) 2 #α
⊢ #(Perm α) = HPow.hPow (α := Cardinal.{u}) 2 #α
have rw₁ : HPow.hPow (α := Cardinal.{u}) 2 #α = HPow.hPow (α := Cardinal.{u}) 2 #α
Tactic: rw [mk_perm_eq_self_power, power_self_eq (aleph0_le_mk α)]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
β' : Type v
inst : Infinite α
leq : lift.{v, u} #α = lift.{u, v} #β'
⊢ #(α ≃ β') = #(α → β')
have obtain : ∀ (e : α ≃ β'), #(α ≃ β') = #(α → β')
Tactic: obtain ⟨e⟩ := lift_mk_eq'.mp leq
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (hypothesis)
Goal:
α : Type u
β' : Type v
inst : Infinite α
leq : lift.{v, u} #α = lift.{u, v} #β'
e : α ≃ β'
⊢ #(α ≃ β') = #(α → β')
have e₁ : lift.{max u v, u} #(α ≃ α) = lift.{u, max u v} #(α ≃ β')
Tactic: have e₁ := lift_mk_eq'.mpr ⟨.equivCongr (.refl α) e⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (hypothesis)
Goal:
α : Type u
β' : Type v
inst : Infinite α
leq : lift.{v, u} #α = lift.{u, v} #β'
e : α ≃ β'
e₁ : lift.{max u v, u} #(α ≃ α) = lift.{u, max u v} #(α ≃ β')
⊢ #(α ≃ β') = #(α → β')
have e₂ : lift.{max u v, u} #(α → α) = lift.{u, max u v} #(α → β')
Tactic: have e₂ := lift_mk_eq'.mpr ⟨.arrowCongr (.refl α) e⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (hypothesis)
Goal:
α : Type u
β' : Type v
inst : Infinite α
leq : lift.{v, u} #α = lift.{u, v} #β'
e : α ≃ β'
e₁ : lift.{max u v, u} #(α ≃ α) = lift.{u, max u v} #(α ≃ β')
e₂ : lift.{max u v, u} #(α → α) = lift.{u, max u v} #(α → β')
⊢ #(α ≃ β') = #(α → β')
have e₃ : lift.{max u v, u} #(α ≃ α) = #(α ≃ β')
Tactic: rw [lift_id'.{u, v}] at e₁ e₂
Cleared hypotheses: e₁, e₂
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (hypothesis)
Goal:
α : Type u
β' : Type v
inst : Infinite α
leq : lift.{v, u} #α = lift.{u, v} #β'
e : α ≃ β'
e₁ : lift.{max u v, u} #(α ≃ α) = lift.{u, max u v} #(α ≃ β')
e₂ : lift.{max u v, u} #(α → α) = lift.{u, max u v} #(α → β')
e₃ : lift.{max u v, u} #(α ≃ α) = #(α ≃ β')
⊢ #(α ≃ β') = #(α → β')
have e₄ : lift.{max u v, u} #(α → α) = #(α → β')
Tactic: rw [lift_id'.{u, v}] at e₁ e₂
Cleared hypotheses: e₁, e₂
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
β' : Type v
inst : Infinite α
leq : lift.{v, u} #α = lift.{u, v} #β'
e : α ≃ β'
e₁ : lift.{max u v, u} #(α ≃ α) = #(α ≃ β')
e₂ : lift.{max u v, u} #(α → α) = #(α → β')
⊢ #(α ≃ β') = #(α → β')
have rw : lift.{max u v, u} #(α ≃ α) = #(α → β')
Tactic: rw [← e₁, ← e₂, lift_inj, mk_perm_eq_self_power, power_def]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
β' : Type v
inst : Infinite α
leq : lift.{v, u} #α = lift.{u, v} #β'
e : α ≃ β'
e₁ : lift.{max u v, u} #(α ≃ α) = #(α ≃ β')
e₂ : lift.{max u v, u} #(α → α) = #(α → β')
rw : lift.{max u v, u} #(α ≃ α) = #(α → β')
⊢ #(α ≃ β') = #(α → β')
have rw₁ : lift.{max u v, u} #(α ≃ α) = lift.{max u v, u} #(α → α)
Tactic: rw [← e₁, ← e₂, lift_inj, mk_perm_eq_self_power, power_def]