-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem mk_perm_eq_self_power : #(Equiv.Perm α) = #α ^ #α :=
  ((mk_equiv_le_embedding α α).trans (mk_embedding_le_arrow α α)).antisymm <| by
    suffices Nonempty ((α → Bool) ↪ Equiv.Perm (α × Bool)) by
      obtain ⟨e⟩ : Nonempty (α ≃ α × Bool)

Proof state:
case refine_2.h
α : Type u
inst✝ : Infinite α
f g : α → Bool
h :
  (fun f => Involutive.toPerm (fun x => (x.1, f x.1 ^^ x.2)) ⋯) f =
    (fun f => Involutive.toPerm (fun x => (x.1, f x.1 ^^ x.2)) ⋯) g
a : α
⊢ (f a ^^ false) = (g a ^^ false)

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

Result:
no goals

Proof state:
case refine_2.h
α : Type u
inst✝ : Infinite α
f g : α → Bool
h :
  (fun f => Involutive.toPerm (fun x => (x.1, f x.1 ^^ x.2)) ⋯) f =
    (fun f => Involutive.toPerm (fun x => (x.1, f x.1 ^^ x.2)) ⋯) g
a : α
⊢ f a = g a

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

Result:
case refine_2.h
α : Type u
inst✝ : Infinite α
f g : α → Bool
h :
  (fun f => Involutive.toPerm (fun x => (x.1, f x.1 ^^ x.2)) ⋯) f =
    (fun f => Involutive.toPerm (fun x => (x.1, f x.1 ^^ x.2)) ⋯) g
a : α
⊢ (f a ^^ false) = (g a ^^ false)

Proof state:
case refine_1
α : Type u
inst✝ : Infinite α
f : α → Bool
x : α × Bool
⊢ (fun x => (x.1, f x.1 ^^ x.2)) ((fun x => (x.1, f x.1 ^^ x.2)) x) = x

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

Result:
no goals

Proof state:
α : Type u
inst✝ : Infinite α
this : Nonempty ((α → Bool) ↪ Perm (α × Bool))
⊢ #(α → α) ≤ #(α ≃ α)

Tactic:
obtain ⟨e⟩ : Nonempty (α ≃ α × Bool) := by
  erw [← Cardinal.eq, mk_prod, lift_uzero, mk_bool,
    lift_natCast, mul_two, add_eq_self (aleph0_le_mk α)]

Result:
case intro
α : Type u
inst✝ : Infinite α
this : Nonempty ((α → Bool) ↪ Perm (α × Bool))
e : α ≃ α × Bool
⊢ #(α → α) ≤ #(α ≃ α)

Proof state:
case intro
α : Type u
inst✝ : Infinite α
this : ↑2 ^ #α ≤ #(Perm (α × Bool))
e : α ≃ α × Bool
⊢ #(α → α) ≤ #(α ≃ α)

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

Result:
no goals

Proof state:
α : Type u
inst✝ : Infinite α
⊢ #(α → α) ≤ #(α ≃ α)

Tactic:
suffices Nonempty ((α → Bool) ↪ Equiv.Perm (α × Bool)) by
  obtain ⟨e⟩ : Nonempty (α ≃ α × Bool) := by
    erw [← Cardinal.eq, mk_prod, lift_uzero, mk_bool,
      lift_natCast, mul_two, add_eq_self (aleph0_le_mk α)]
  erw [← le_def, mk_arrow, lift_uzero, mk_bool, lift_natCast 2] at this
  rwa [← power_def, power_self_eq (aleph0_le_mk α), e.permCongr.cardinal_eq]

Result:
α : Type u
inst✝ : Infinite α
⊢ Nonempty ((α → Bool) ↪ Perm (α × Bool))

Proof state:
case refine_2
α : Type u
inst✝ : Infinite α
f g : α → Bool
h :
  (fun f => Involutive.toPerm (fun x => (x.1, f x.1 ^^ x.2)) ⋯) f =
    (fun f => Involutive.toPerm (fun x => (x.1, f x.1 ^^ x.2)) ⋯) g
⊢ f = g

Tactic:
ext a

Result:
case refine_2.h
α : Type u
inst✝ : Infinite α
f g : α → Bool
h :
  (fun f => Involutive.toPerm (fun x => (x.1, f x.1 ^^ x.2)) ⋯) f =
    (fun f => Involutive.toPerm (fun x => (x.1, f x.1 ^^ x.2)) ⋯) g
a : α
⊢ f a = g a

Proof state:
α : Type u
inst✝ : Infinite α
this : Nonempty ((α → Bool) ↪ Perm (α × Bool))
⊢ Nonempty (α ≃ α × Bool)

Tactic:
erw [← Cardinal.eq, mk_prod, lift_uzero, mk_bool,
  lift_natCast, mul_two, add_eq_self (aleph0_le_mk α)]

Result:
no goals

Proof state:
case intro
α : Type u
inst✝ : Infinite α
this : Nonempty ((α → Bool) ↪ Perm (α × Bool))
e : α ≃ α × Bool
⊢ #(α → α) ≤ #(α ≃ α)

Tactic:
erw [← le_def, mk_arrow, lift_uzero, mk_bool, lift_natCast 2] at this

Result:
case intro
α : Type u
inst✝ : Infinite α
this : ↑2 ^ #α ≤ #(Perm (α × Bool))
e : α ≃ α × Bool
⊢ #(α → α) ≤ #(α ≃ α)

Proof state:
α : Type u
inst✝ : Infinite α
⊢ Nonempty ((α → 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 ↦ ?_⟩⟩

Result:
case refine_1
α : Type u
inst✝ : Infinite α
f : α → Bool
x : α × Bool
⊢ (fun x => (x.1, f x.1 ^^ x.2)) ((fun x => (x.1, f x.1 ^^ x.2)) x) = x

case refine_2
α : Type u
inst✝ : Infinite α
f g : α → Bool
h :
  (fun f => Involutive.toPerm (fun x => (x.1, f x.1 ^^ x.2)) ⋯) f =
    (fun f => Involutive.toPerm (fun x => (x.1, f x.1 ^^ x.2)) ⋯) g
⊢ f = g