awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
ι : Type u
inst : Infinite ι
c : ι → Cardinal.{v}
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift.{u, v} (c i) ≤ lift.{v, u} #ι
i : ι
a : 2 ≤ c i
⊢ lift.{v, u} 2 ≤ lift.{u, v} (c i)

Tactic:
rw [lift_two, ← lift_two.{u, v}, lift_le]

Premises used: Cardinal.lift_two, Cardinal.lift_le
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
ι : Type u
inst : Infinite ι
c : ι → Cardinal.{v}
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift.{u, v} (c i) ≤ lift.{v, u} #ι
i : ι
⊢ 2 ≤ c i

Tactic:
h₁ i
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
ι : Type u
inst : Infinite ι
c : ι → Cardinal.{v}
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift.{u, v} (c i) ≤ lift.{v, u} #ι
i : ι
⊢ 2 ≤ c i

Tactic:
exact h₁ i
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
c₁ c₂ : Cardinal.{u_1}
h₁ : ℵ₀ ≤ c₁
h₂ : 2 ≤ c₂
h₂' : c₂ ≤ c₁
⊢ c₂ ^ c₁ = HPow.hPow (α := Cardinal.{u_1}) 2 c₁

Tactic:
le_antisymm (power_self_eq h₁ ▸ power_le_power_right h₂') (power_le_power_right h₂)

Premises used: Cardinal.power_le_power_right, le_antisymm
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
c : Cardinal.{u}
h : ℵ₀ ≤ c
n : ℕ
hn assumption_mod_cast assumption_mod_cast₁ assumption_mod_cast₂ assumption_mod_cast₃ : 2 ≤ n
⊢ LE.le.{u + 1} (α := Cardinal.{u}) 2 (↑n : Cardinal.{u})

Tactic:
assumption_mod_cast
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
c : Cardinal.{u}
n : ℕ
h : ℵ₀ ≤ c
⊢ c ^ n ≤ c

Tactic:
pow_le h natCast_lt_aleph0

Premises used: Cardinal.pow_le, Cardinal.natCast_lt_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
c : Cardinal.{u}
n : ℕ
h1 : ℵ₀ ≤ c
h2 : 1 ≤ n
⊢ c ^ n = c

Tactic:
pow_eq h1 (mod_cast h2) natCast_lt_aleph0

Premises used: Cardinal.pow_eq, congrArg, cast, Nat.cast_le._simp_1, LE.le, Cardinal.natCast_lt_aleph0, Nat.cast, congrFun', Eq.symm, Nat.cast_one, Eq.trans
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
c : Cardinal.{u}
n : ℕ
inl : ∀ (hc : ℵ₀ ≤ c), HPow.hPow (β := Cardinal.{u}) c (↑n : Cardinal.{u}) ≤ max c ℵ₀
inr : ∀ (hc : c < ℵ₀), HPow.hPow (β := Cardinal.{u}) c (↑n : Cardinal.{u}) ≤ max c ℵ₀
⊢ HPow.hPow (β := Cardinal.{u}) c (↑n : Cardinal.{u}) ≤ max c ℵ₀

Tactic:
rcases le_or_gt ℵ₀ c with hc | hc

Premises used: Cardinal.aleph0, le_or_gt
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
c : Cardinal.{u}
n : ℕ
hc : ℵ₀ ≤ c
⊢ HPow.hPow (β := Cardinal.{u}) c (↑n : Cardinal.{u}) ≤ max c ℵ₀

Tactic:
le_max_of_le_left (power_nat_le hc)

Premises used: Cardinal.power_nat_le, le_max_of_le_left
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
c : Cardinal.{u}
n : ℕ
hc : ℵ₀ ≤ c
⊢ HPow.hPow (β := Cardinal.{u}) c (↑n : Cardinal.{u}) ≤ max c ℵ₀

Tactic:
exact le_max_of_le_left (power_nat_le hc)

Premises used: Cardinal.power_nat_le, le_max_of_le_left
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
c : Cardinal.{u}
n : ℕ
hc : c < ℵ₀
⊢ HPow.hPow (β := Cardinal.{u}) c (↑n : Cardinal.{u}) ≤ max c ℵ₀

Tactic:
le_max_of_le_right (power_lt_aleph0 hc natCast_lt_aleph0).le

Premises used: LT.lt.le, Cardinal.natCast_lt_aleph0, le_max_of_le_right, Cardinal.power_lt_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
c : Cardinal.{u}
n : ℕ
hc : c < ℵ₀
⊢ HPow.hPow (β := Cardinal.{u}) c (↑n : Cardinal.{u}) ≤ max c ℵ₀

Tactic:
exact le_max_of_le_right (power_lt_aleph0 hc natCast_lt_aleph0).le

Premises used: LT.lt.le, Cardinal.natCast_lt_aleph0, le_max_of_le_right, Cardinal.power_lt_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u}
ha : a ≤ ℵ₀
hb : b < ℵ₀
⊢ b < ℵ₀

Tactic:
hb
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a b : Cardinal.{u}
ha : a ≤ ℵ₀
hb : b < ℵ₀
lift : ∀ (b : ℕ), HPow.hPow (β := Cardinal.{u}) a (↑b : Cardinal.{u}) ≤ ℵ₀
⊢ a ^ b ≤ ℵ₀

Tactic:
lift b to ℕ using hb
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
a : Cardinal.{u}
ha : a ≤ ℵ₀
b : ℕ
⊢ HPow.hPow (β := Cardinal.{u}) a (↑b : Cardinal.{u}) ≤ ℵ₀

Tactic:
simpa [ha] using power_nat_le_max (c := a)

Premises used: Cardinal.power_nat_le_max
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
a : c ^< ℵ₀ ≤ c
a₁ : c ≤ c ^< ℵ₀
⊢ c ^< ℵ₀ = c

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
a : ∀ x < ℵ₀, c ^ x ≤ c
⊢ c ^< ℵ₀ ≤ c

Tactic:
rw [powerlt_le]

Premises used: Cardinal.powerlt_le
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ ∀ x < ℵ₀, c ^ x ≤ c

Tactic:
fun _ a ↦ pow_le h a

Premises used: Cardinal.pow_le
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ ∀ x < ℵ₀, c ^ x ≤ c

Tactic:
exact fun _ a ↦ pow_le h a

Premises used: Cardinal.pow_le
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ HPow.hPow (β := Cardinal.{u_1}) c 1 ≤ c ^< ℵ₀

Tactic:
le_powerlt c one_lt_aleph0

Premises used: Cardinal.one_lt_aleph0, Cardinal.le_powerlt
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
h₁ : c = HPow.hPow (β := Cardinal.{u_1}) c 1
⊢ c ≤ c ^< ℵ₀

Tactic:
convert! le_powerlt c one_lt_aleph0

Premises used: Cardinal.one_lt_aleph0, Cardinal.le_powerlt
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
h₁ h₂ : c = c
⊢ c = HPow.hPow (β := Cardinal.{u_1}) c 1

Tactic:
rw [power_one]

Premises used: Cardinal.power_one
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
c : Cardinal.{u_1}
inl : ∀ (h : ℵ₀ ≤ c), c ^< ℵ₀ ≤ max c ℵ₀
inr : ∀ (h : c < ℵ₀), c ^< ℵ₀ ≤ max c ℵ₀
⊢ c ^< ℵ₀ ≤ max c ℵ₀

Tactic:
rcases le_or_gt ℵ₀ c with h | h

Premises used: Cardinal.aleph0, le_or_gt
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
inl : c ≤ max c ℵ₀
⊢ c ^< ℵ₀ ≤ max c ℵ₀

Tactic:
rw [powerlt_aleph0 h]

Premises used: Cardinal.powerlt_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c ≤ max c ℵ₀

Tactic:
apply le_max_left

Premises used: le_max_left
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
c : Cardinal.{u_1}
h : c < ℵ₀
inr : ∀ x < ℵ₀, c ^ x ≤ max c ℵ₀
⊢ c ^< ℵ₀ ≤ max c ℵ₀

Tactic:
rw [powerlt_le]

Premises used: Cardinal.powerlt_le
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
c : Cardinal.{u_1}
h : c < ℵ₀
⊢ ∀ x < ℵ₀, c ^ x ≤ max c ℵ₀

Tactic:
fun c' hc' => (power_lt_aleph0 h hc').le.trans (le_max_right _ _)

Premises used: le_max_right, LT.lt.le, Cardinal.aleph0, LE.le.trans, Cardinal.power_lt_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
c : Cardinal.{u_1}
h : c < ℵ₀
⊢ ∀ x < ℵ₀, c ^ x ≤ max c ℵ₀

Tactic:
exact fun c' hc' => (power_lt_aleph0 h hc').le.trans (le_max_right _ _)

Premises used: le_max_right, LT.lt.le, Cardinal.aleph0, LE.le.trans, Cardinal.power_lt_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
β' : Type v
rw : IsEmpty (α ≃ β') ↔ lift.{v, u} #α ≠ lift.{u, v} #β'
rw₁ : ¬Nonempty (α ≃ β') ↔ lift.{v, u} #α ≠ lift.{u, v} #β'
rw₂ rw₃ : ¬lift.{v, u} #α = lift.{u, v} #β' ↔ lift.{v, u} #α ≠ lift.{u, v} #β'
⊢ #(α ≃ β') = 0 ↔ lift.{v, u} #α ≠ lift.{u, v} #β'

Tactic:
rw [mk_eq_zero_iff, ← not_nonempty_iff, ← lift_mk_eq']

Premises used: Cardinal.lift_mk_eq', Cardinal.mk_eq_zero_iff, not_nonempty_iff
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α β : Type u
rw : lift.{u, u} #α ≠ lift.{u, u} #β ↔ #α ≠ #β
rw₁ : #α ≠ lift.{u, u} #β ↔ #α ≠ #β
rw₂ rw₃ : #α ≠ #β ↔ #α ≠ #β
⊢ #(α ≃ β) = 0 ↔ #α ≠ #β

Tactic:
rw [mk_equiv_eq_zero_iff_lift_ne, lift_id, lift_id]

Premises used: Cardinal.mk_equiv_eq_zero_iff_lift_ne, Cardinal.lift_id
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
β' : Type v
⊢ #(α ≃ β') = #(β' ≃ α)

Tactic:
(ofBijective _ symm_bijective).cardinal_eq

Premises used: Equiv.symm_bijective, Equiv.ofBijective, Equiv.cardinal_eq
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
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} #α
rw₃ rw₄ : lift.{u, v} #β' < lift.{v, u} #α ↔ lift.{u, v} #β' < lift.{v, u} #α
⊢ #(α ↪ β') = 0 ↔ lift.{u, v} #β' < lift.{v, u} #α

Tactic:
rw [mk_eq_zero_iff, ← not_nonempty_iff, ← lift_mk_le', not_le]

Premises used: not_le, Cardinal.mk_eq_zero_iff, not_nonempty_iff, Cardinal.lift_mk_le'
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α β : Type u
rw : lift.{u, u} #β < lift.{u, u} #α ↔ #β < #α
rw₁ rw₂ : #β < #α ↔ #β < #α
⊢ #(α ↪ β) = 0 ↔ #β < #α

Tactic:
rw [mk_embedding_eq_zero_iff_lift_lt, lift_lt]

Premises used: Cardinal.mk_embedding_eq_zero_iff_lift_lt, Cardinal.lift_lt
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
β' : Type v
simp_rw : IsEmpty (α → β') ↔ #α ≠ 0 ∧ IsEmpty β'
simp_rw₁ : IsEmpty (α → β') ↔ Nonempty α ∧ IsEmpty β'
⊢ #(α → β') = 0 ↔ #α ≠ 0 ∧ #β' = 0

Tactic:
simp_rw [mk_eq_zero_iff, mk_ne_zero_iff, isEmpty_fun]

Premises used: Cardinal.mk_ne_zero_iff, Cardinal.mk_eq_zero_iff, isEmpty_fun
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
β' : Type v
contrapose! :
  #(↑{f : α → β' | Surjective f} : Type (max u v)) ≠ 0 ↔ lift.{u, v} #β' ≤ lift.{v, u} #α ∧ (#α = 0 ∨ #β' ≠ 0)
⊢ #(↑{f : α → β' | Surjective f} : Type (max u v)) = 0 ↔ lift.{v, u} #α < lift.{u, v} #β' ∨ #α ≠ 0 ∧ #β' = 0

Tactic:
contrapose! +distrib
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
β' : Type v
rw : #(↑{f : α → β' | Surjective f} : Type (max u v)) ≠ 0 ↔ (#α = 0 ∨ #β' ≠ 0) ∧ Nonempty (β' ↪ α)
⊢ #(↑{f : α → β' | Surjective f} : Type (max u v)) ≠ 0 ↔ lift.{u, v} #β' ≤ lift.{v, u} #α ∧ (#α = 0 ∨ #β' ≠ 0)

Tactic:
rw [lift_mk_le', and_comm]

Premises used: and_comm, Cardinal.lift_mk_le'
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
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 (β' ↪ α)
simp_rw₅ : Nonempty (α → β') ∧ Nonempty (β' ↪ α) ↔ (IsEmpty α ∨ Nonempty β') ∧ Nonempty (β' ↪ α)
⊢ #(↑{f : α → β' | Surjective f} : Type (max u v)) ≠ 0 ↔ (#α = 0 ∨ #β' ≠ 0) ∧ Nonempty (β' ↪ α)

Tactic:
simp_rw [mk_ne_zero_iff, mk_eq_zero_iff, nonempty_coe_sort,
    Set.Nonempty, mem_setOf, exists_surjective_iff, nonempty_fun]

Premises used: Cardinal.mk_ne_zero_iff, Set.nonempty_coe_sort, nonempty_fun, Cardinal.mk_eq_zero_iff, Set.mem_setOf, Set.Nonempty, Function.exists_surjective_iff
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α β : Type u
rw : lift.{u, u} #α < lift.{u, u} #β ∨ #α ≠ 0 ∧ #β = 0 ↔ #α < #β ∨ #α ≠ 0 ∧ #β = 0
rw₁ rw₂ : #α < #β ∨ #α ≠ 0 ∧ #β = 0 ↔ #α < #β ∨ #α ≠ 0 ∧ #β = 0
⊢ #(↑{f : α → β | Surjective f} : Type u) = 0 ↔ #α < #β ∨ #α ≠ 0 ∧ #β = 0

Tactic:
rw [mk_surjective_eq_zero_iff_lift, lift_lt]

Premises used: Cardinal.lift_lt, Cardinal.mk_surjective_eq_zero_iff_lift
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
β' : Type v
⊢ #(α ≃ β') ≤ #(α ↪ β')

Tactic:
⟨⟨_, Equiv.toEmbedding_injective⟩⟩

Premises used: Equiv.toEmbedding_injective, Function.Embedding.mk, Nonempty.intro
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
β' : Type v
⊢ #(α ↪ β') ≤ #(α → β')

Tactic:
⟨⟨_, DFunLike.coe_injective⟩⟩

Premises used: Function.Embedding.mk, Nonempty.intro, DFunLike.coe_injective
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
inst : Infinite α
this : Nonempty.{max 1 (u + 1)} ((α → Bool) ↪ Perm (α × Bool))
⊢ Nonempty.{max 1 (u + 1)} (α ≃ α × Bool)

Tactic:
simp [← Cardinal.eq, mul_two]

Premises used: Cardinal.eq, mul_two
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
inst : Infinite α
this : Nonempty.{max 1 (u + 1)} ((α → Bool) ↪ Perm (α × Bool))
obtain : ∀ (e : α ≃ α × Bool), #(α → α) ≤ #(α ≃ α)
⊢ #(α → α) ≤ #(α ≃ α)

Tactic:
obtain ⟨e⟩ : Nonempty (α ≃ α × Bool) := by simp [← Cardinal.eq, mul_two]

Premises used: Equiv, Bool, Nonempty, Prod
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
inst : Infinite α
this : Nonempty.{max 1 (u + 1)} ((α → Bool) ↪ Perm (α × Bool))
e : α ≃ α × Bool
⊢ 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

Premises used: Nat.cast_ofNat, Cardinal.mk_pi, Cardinal.prod_const, Cardinal.mk_fintype, Cardinal.lift_uzero, Cardinal.lift_ofNat, Cardinal.le_def, Fintype.card_bool
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
inst : Infinite α
e : α ≃ α × Bool
this : HPow.hPow (α := Cardinal.{u}) 2 #α ≤ #(Perm (α × Bool))
rwa : #α ^ #α ≤ #(α ≃ α)
rwa₁ : HPow.hPow (α := Cardinal.{u}) 2 #α ≤ #(α ≃ α)
rwa₂ rwa₃ rwa₄ rwa₅ : HPow.hPow (α := Cardinal.{u}) 2 #α ≤ #(Perm (α × Bool))
⊢ #(α → α) ≤ #(α ≃ α)

Tactic:
rwa [← power_def, power_self_eq (aleph0_le_mk α), e.permCongr.cardinal_eq]

Premises used: Cardinal.power_self_eq, Equiv.permCongr, Cardinal.power_def, Cardinal.aleph0_le_mk, Equiv.cardinal_eq
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
inst : Infinite α
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]
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
inst : Infinite α
⊢ Nonempty.{max 1 (u + 1)} ((α → Bool) ↪ Perm (α × Bool))

Tactic:
⟨⟨fun f ↦ Involutive.toPerm (fun x ↦ ⟨x.1, xor (f x.1) x.2⟩) fun x ↦ ?_, fun f g h ↦ ?_⟩⟩

Premises used: Function.Embedding.mk, Prod.mk, Function.Involutive.toPerm, Nonempty.intro, Prod.fst, Bool.xor, Prod.snd
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
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
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)) ⋯ : Perm (α × Bool))) f)
        ((fun (f : α → Bool) ↦ (Involutive.toPerm (fun (x : α × Bool) ↦ (x.1, f x.1 ^^ x.2)) ⋯ : Perm (α × Bool))) g)),
    f = g
⊢ Nonempty.{max 1 (u + 1)} ((α → Bool) ↪ Perm (α × Bool))

Tactic:
refine ⟨⟨fun f ↦ Involutive.toPerm (fun x ↦ ⟨x.1, xor (f x.1) x.2⟩) fun x ↦ ?_, fun f g h ↦ ?_⟩⟩
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
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
refine_1₃ : (x.1, false ^^ 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

Tactic:
simp_rw [← Bool.xor_assoc, Bool.xor_self, Bool.false_xor]

Premises used: Bool.false_xor, Bool.xor_assoc, Bool.xor_self
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
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)
refine_2 : ∀ (a : α), f a = g a
⊢ f = g

Tactic:
ext a
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
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 : α
refine_2 : (f a ^^ false) = (g a ^^ false)
⊢ f a = g a

Tactic:
rw [← (f a).xor_false, ← (g a).xor_false]

Premises used: Bool.xor_false
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
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 ^^ false) = (g a ^^ false)

Tactic:
congr(($h ⟨a, false⟩).2)

Premises used: congrArg, id, Prod.mk, Bool.false, Prod.snd, DFunLike.coe
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
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 ^^ false) = (g a ^^ false)

Tactic:
exact congr(($h ⟨a, false⟩).2)
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
inst : Infinite α
rw : #α ^ #α = HPow.hPow (α := Cardinal.{u}) 2 #α
rw₁ rw₂ : HPow.hPow (α := Cardinal.{u}) 2 #α = HPow.hPow (α := Cardinal.{u}) 2 #α
⊢ #(Perm α) = HPow.hPow (α := Cardinal.{u}) 2 #α

Tactic:
rw [mk_perm_eq_self_power, power_self_eq (aleph0_le_mk α)]

Premises used: Cardinal.power_self_eq, Cardinal.mk_perm_eq_self_power, Cardinal.aleph0_le_mk
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
β' : Type v
inst : Infinite α
leq : lift.{v, u} #α = lift.{u, v} #β'
obtain : ∀ (e : α ≃ β'), #(α ≃ β') = #(α → β')
⊢ #(α ≃ β') = #(α → β')

Tactic:
obtain ⟨e⟩ := lift_mk_eq'.mp leq

Premises used: Cardinal.lift_mk_eq', Iff.mp
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
β' : Type v
inst : Infinite α
leq : lift.{v, u} #α = lift.{u, v} #β'
e : α ≃ β'
⊢ lift.{max u v, u} #(α ≃ α) = lift.{u, max u v} #(α ≃ β')

Tactic:
have e₁ := lift_mk_eq'.mpr ⟨.equivCongr (.refl α) e⟩
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
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} #(α ≃ β')
⊢ lift.{max u v, u} #(α → α) = lift.{u, max u v} #(α → β')

Tactic:
have e₂ := lift_mk_eq'.mpr ⟨.arrowCongr (.refl α) e⟩
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
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} #(α → β')
⊢ lift.{max u v, u} #(α ≃ α) = #(α ≃ β')

Tactic:
rw [lift_id'.{u, v}] at e₁ e₂
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
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} #(α ≃ α) = #(α ≃ β')
⊢ lift.{max u v, u} #(α → α) = #(α → β')

Tactic:
rw [lift_id'.{u, v}] at e₁ e₂
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
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} #(α ≃ α) = #(α → β')
rw₁ : lift.{max u v, u} #(α ≃ α) = lift.{max u v, u} #(α → α)
rw₂ : #(α ≃ α) = #(α → α)
rw₃ : #α ^ #α = #(α → α)
rw₄ rw₅ : #(α → α) = #(α → α)
⊢ #(α ≃ β') = #(α → β')

Tactic:
rw [← e₁, ← e₂, lift_inj, mk_perm_eq_self_power, power_def]

Premises used: Cardinal.lift_inj, Cardinal.mk_perm_eq_self_power, Cardinal.power_def
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α β : Type u
inst : Infinite α
eq : #α = #β
⊢ #(α ≃ β) = #(α → β)

Tactic:
mk_equiv_eq_arrow_of_lift_eq congr(lift $eq)

Premises used: congrArg, Cardinal.lift, id, Cardinal.mk_equiv_eq_arrow_of_lift_eq
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
β' : Type v
inst : Infinite α
leq : lift.{v, u} #α = lift.{u, v} #β'
⊢ #(α ≃ β') = HPow.hPow (α := Cardinal.{max u v}) 2 (lift.{v, u} #α)

Tactic:
simp [mk_equiv_eq_arrow_of_lift_eq leq, ← leq, power_self_eq]

Premises used: Cardinal.power_self_eq, Cardinal.mk_equiv_eq_arrow_of_lift_eq
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α β : Type u
inst : Infinite α
eq : #α = #β
rw : HPow.hPow (α := Cardinal.{u}) 2 (lift.{u, u} #α) = HPow.hPow (α := Cardinal.{u}) 2 #α
rw₁ rw₂ : HPow.hPow (α := Cardinal.{u}) 2 #α = HPow.hPow (α := Cardinal.{u}) 2 #α
⊢ #(α ≃ β) = HPow.hPow (α := Cardinal.{u}) 2 #α

Tactic:
rw [mk_equiv_of_lift_eq (lift_inj.mpr eq), lift_id]

Premises used: Iff.mpr, Cardinal.lift_inj, Cardinal.mk_equiv_of_lift_eq, Cardinal.lift_id
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
β' : Type v
inst : Infinite α
lle : lift.{u, v} #β' ≤ lift.{v, u} #α
rw : #(Embedding.{v + 1, u + 1} β' (α × α))
| #(β' ↪ α)

Tactic:
rw [← (Equiv.embeddingCongr (.refl _)
      (Cardinal.eq.mp <| mul_eq_self <| aleph0_le_mk α).some).cardinal_eq]

Premises used: Cardinal.mul_eq_self, Nonempty.some, Equiv.embeddingCongr, Cardinal.eq, Iff.mp, Equiv.refl, Cardinal.aleph0_le_mk, Equiv.cardinal_eq
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
β' : Type v
inst : Infinite α
lle : lift.{u, v} #β' ≤ lift.{v, u} #α
conv_rhs : #(β' → α) ≤ #(Embedding.{v + 1, u + 1} β' (α × α))
⊢ #(β' → α) ≤ #(β' ↪ α)

Tactic:
conv_rhs => rw [← (Equiv.embeddingCongr (.refl _)
      (Cardinal.eq.mp <| mul_eq_self <| aleph0_le_mk α).some).cardinal_eq]

Premises used: Cardinal.mul_eq_self, Nonempty.some, Equiv.embeddingCongr, Cardinal.eq, Iff.mp, Equiv.refl, Cardinal.aleph0_le_mk, Equiv.cardinal_eq
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
β' : Type v
inst : Infinite α
lle : lift.{u, v} #β' ≤ lift.{v, u} #α
obtain : ∀ (e : β' ↪ α), #(β' → α) ≤ #(Embedding.{v + 1, u + 1} β' (α × α))
⊢ #(β' → α) ≤ #(Embedding.{v + 1, u + 1} β' (α × α))

Tactic:
obtain ⟨e⟩ := lift_mk_le'.mp lle

Premises used: Iff.mp, Cardinal.lift_mk_le'
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
β' : Type v
inst : Infinite α
lle : lift.{u, v} #β' ≤ lift.{v, u} #α
e : β' ↪ α
⊢ #(β' → α) ≤ #(Embedding.{v + 1, u + 1} β' (α × α))

Tactic:
⟨⟨fun f ↦ ⟨fun b ↦ ⟨e b, f b⟩, fun _ _ h ↦ e.injective congr(Prod.fst $h)⟩,
      fun f g h ↦ funext fun b ↦ congr(Prod.snd <| $h b)⟩⟩

Premises used: congrArg, Function.Embedding.mk, id, Prod.mk, Nonempty.intro, Prod.fst, funext, Function.Embedding.injective, Prod.snd, DFunLike.coe
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
β' : Type v
inst : Infinite α
lle : lift.{u, v} #β' ≤ lift.{v, u} #α
e : β' ↪ α
⊢ #(β' → α) ≤ #(Embedding.{v + 1, u + 1} β' (α × α))

Tactic:
exact ⟨⟨fun f ↦ ⟨fun b ↦ ⟨e b, f b⟩, fun _ _ h ↦ e.injective congr(Prod.fst $h)⟩,
      fun f g h ↦ funext fun b ↦ congr(Prod.snd <| $h b)⟩⟩
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α β : Type u
inst : Infinite α
le : #β ≤ #α
⊢ #(β ↪ α) = #(β → α)

Tactic:
mk_embedding_eq_arrow_of_lift_le (lift_le.mpr le)

Premises used: Iff.mpr, Cardinal.lift_le, Cardinal.mk_embedding_eq_arrow_of_lift_le
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
β' : Type v
inst : Infinite α
lle : lift.{u, v} #β' ≤ lift.{v, u} #α
simp_rw : lift.{max u v, u} #α = lift.{max v u, u} #α + lift.{u, v} #β'
⊢ Nonempty (α ≃ α ⊕ β')

Tactic:
simp_rw [← lift_mk_eq', mk_sum, lift_add, lift_lift]

Premises used: Cardinal.lift_lift, Cardinal.lift_mk_eq', Cardinal.mk_sum, Cardinal.lift_add
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
β' : Type v
inst : Infinite α
lle : lift.{u, v} #β' ≤ lift.{v, u} #α
rw : lift.{v, u} #α + lift.{u, v} #β' = lift.{v, u} #α
⊢ lift.{max u v, u} #α = lift.{max v u, u} #α + lift.{u, v} #β'

Tactic:
rw [lift_umax.{u, v}, eq_comm]

Premises used: eq_comm