awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
β' : Type v
inst : Infinite α
lle : lift.{u, v} #β' ≤ lift.{v, u} #α
⊢ lift.{v, u} #α + lift.{u, v} #β' = lift.{v, u} #α

Tactic:
add_eq_left (aleph0_le_lift.mpr <| aleph0_le_mk α) lle

Premises used: Iff.mpr, Cardinal.aleph0_le_lift, Cardinal.add_eq_left, Cardinal.aleph0_le_mk
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
β' : Type v
inst : Infinite α
lle : lift.{u, v} #β' ≤ lift.{v, u} #α
⊢ lift.{v, u} #α + lift.{u, v} #β' = lift.{v, u} #α

Tactic:
exact add_eq_left (aleph0_le_lift.mpr <| aleph0_le_mk α) lle

Premises used: Iff.mpr, Cardinal.aleph0_le_lift, Cardinal.add_eq_left, Cardinal.aleph0_le_mk
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
β' : Type v
inst : Infinite α
lle : lift.{u, v} #β' ≤ lift.{v, u} #α
e : α ≃ α ⊕ β'
f g : α → β'
h :
  Eq (α := (↑{f : α → β' | Surjective f} : Type (max u v)))
    ((fun (f : α → β') ↦
        (Subtype.mk (p := fun (x : α → β') ↦ Membership.mem (γ := Set (α → β')) {f : α → β' | Surjective f} x)
            (fun (a : α) ↦ Sum.elim f id ((e : (a : α) → α ⊕ β') a)) ⋯ :
          { x : α → β' // Membership.mem (γ := Set (α → β')) {f : α → β' | Surjective f} x }))
      f)
    ((fun (f : α → β') ↦
        (Subtype.mk (p := fun (x : α → β') ↦ Membership.mem (γ := Set (α → β')) {f : α → β' | Surjective f} x)
            (fun (a : α) ↦ Sum.elim f id ((e : (a : α) → α ⊕ β') a)) ⋯ :
          { x : α → β' // Membership.mem (γ := Set (α → β')) {f : α → β' | Surjective f} x }))
      g)
a : α
⊢ f a = g a

Tactic:
simpa only [e.apply_symm_apply] using congr_fun (Subtype.ext_iff.mp h) (e.symm <| .inl a)

Premises used: Equiv.apply_symm_apply, Sum.inl, Subtype.ext_iff, Iff.mp, congr_fun, Equiv.symm, DFunLike.coe
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α β : Type u
inst : Infinite α
le : #β ≤ #α
⊢ #(↑{f : α → β | Surjective f} : Type u) = #(α → β)

Tactic:
mk_surjective_eq_arrow_of_lift_le (lift_le.mpr le)

Premises used: Iff.mpr, Cardinal.mk_surjective_eq_arrow_of_lift_le, Cardinal.lift_le
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
inst : Infinite α
H1 : ℵ₀ ≤ #α
x : α
⊢ ∀ ⦃a₂ : α⦄, Eq.{u + 1} (α := List α) ((fun (a : α) ↦ [a]) x) ((fun (a : α) ↦ [a]) a₂) → x = a₂

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
inst : Infinite α
H1 : ℵ₀ ≤ #α
⊢ (sum fun (x : ℕ) ↦ #α) = #α

Tactic:
simp [H1]
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
inst : Countable α
inst_1 : Nonempty α
⊢ #(List α) = ℵ₀

Tactic:
mk_le_aleph0.antisymm (aleph0_le_mk _)

Premises used: Cardinal.mk_le_aleph0, LE.le.antisymm, Cardinal.aleph0_le_mk
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
inst : Nonempty α
inl : Finite α → #(List α) = max ℵ₀ #α
inr : Infinite α → #(List α) = max ℵ₀ #α
⊢ #(List α) = max ℵ₀ #α

Tactic:
cases finite_or_infinite α

Premises used: finite_or_infinite
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
inst : Nonempty α
h : Finite α
inl : #α ≤ ℵ₀
⊢ #(List α) = max ℵ₀ #α

Tactic:
rw [mk_list_eq_aleph0, eq_comm, max_eq_left]

Premises used: max_eq_left, eq_comm, Cardinal.mk_list_eq_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
inst : Nonempty α
h : Finite α
⊢ #α ≤ ℵ₀

Tactic:
mk_le_aleph0

Premises used: Cardinal.mk_le_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
inst : Nonempty α
h : Finite α
⊢ #α ≤ ℵ₀

Tactic:
exact mk_le_aleph0

Premises used: Cardinal.mk_le_aleph0
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
inst : Nonempty α
h : Infinite α
inr : ℵ₀ ≤ #α
⊢ #(List α) = max ℵ₀ #α

Tactic:
rw [mk_list_eq_mk, eq_comm, max_eq_right]

Premises used: Cardinal.mk_list_eq_mk, eq_comm, max_eq_right
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
inst : Nonempty α
h : Infinite α
⊢ ℵ₀ ≤ #α

Tactic:
aleph0_le_mk α

Premises used: Cardinal.aleph0_le_mk
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
inst : Nonempty α
h : Infinite α
⊢ ℵ₀ ≤ #α

Tactic:
exact aleph0_le_mk α

Premises used: Cardinal.aleph0_le_mk
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
inst : Nonempty α
rw : max ℵ₀ #α = max #α ℵ₀
rw₁ rw₂ : max #α ℵ₀ = max #α ℵ₀
⊢ #(List α) = max #α ℵ₀

Tactic:
rw [mk_list_eq_max, max_comm]

Premises used: Cardinal.mk_list_eq_max, max_comm
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
x : Cardinal.{u_1}
h : x ≠ 0
⊢ Nonempty.{u_1 + 1} (Quotient.out x)

Tactic:
have := nonempty_out h
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
x : Cardinal.{u_1}
h : x ≠ 0
this : Nonempty.{u_1 + 1} (Quotient.out x)
rw : max ℵ₀ x
| sum fun (n : ℕ) ↦ x ^ n

Tactic:
rw [← x.mk_out, ← mk_list_eq_sum_pow, mk_list_eq_max, mk_out]

Premises used: Cardinal.mk_list_eq_sum_pow, Cardinal.mk_out, Cardinal.mk_list_eq_max
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
x : Cardinal.{u_1}
h : x ≠ 0
this : Nonempty.{u_1 + 1} (Quotient.out x)
conv_lhs : (sum fun (n : ℕ) ↦ x ^ n) = max ℵ₀ x
conv_lhs₁ : max ℵ₀ x = max ℵ₀ x
⊢ (sum fun (n : ℕ) ↦ x ^ n) = max ℵ₀ x

Tactic:
conv_lhs => rw [← x.mk_out, ← mk_list_eq_sum_pow, mk_list_eq_max, mk_out]

Premises used: Cardinal.mk_list_eq_sum_pow, Cardinal.mk_out, Cardinal.mk_list_eq_max
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
inl : Finite α → #(List α) ≤ max ℵ₀ #α
inr : Infinite α → #(List α) ≤ max ℵ₀ #α
⊢ #(List α) ≤ max ℵ₀ #α

Tactic:
cases finite_or_infinite α

Premises used: finite_or_infinite
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
h : Finite α
⊢ #(List α) ≤ max ℵ₀ #α

Tactic:
mk_le_aleph0.trans (le_max_left _ _)

Premises used: Cardinal.mk_le_aleph0, LE.le.trans, le_max_left
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
h : Finite α
⊢ #(List α) ≤ max ℵ₀ #α

Tactic:
exact mk_le_aleph0.trans (le_max_left _ _)

Premises used: Cardinal.mk_le_aleph0, LE.le.trans, le_max_left
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
h : Infinite α
inr : #α ≤ max ℵ₀ #α
⊢ #(List α) ≤ max ℵ₀ #α

Tactic:
rw [mk_list_eq_mk]

Premises used: Cardinal.mk_list_eq_mk
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
h : Infinite α
⊢ #α ≤ max ℵ₀ #α

Tactic:
apply le_max_right

Premises used: le_max_right
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
x : Cardinal.{u_1}
rw : #(List (Quotient.out x)) ≤ max ℵ₀ #(Quotient.out x)
⊢ (sum fun (n : ℕ) ↦ x ^ n) ≤ max ℵ₀ x

Tactic:
rw [← x.mk_out, ← mk_list_eq_sum_pow]

Premises used: Cardinal.mk_list_eq_sum_pow, Cardinal.mk_out
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
x : Cardinal.{u_1}
⊢ #(List (Quotient.out x)) ≤ max ℵ₀ #(Quotient.out x)

Tactic:
mk_list_le_max _

Premises used: Cardinal.mk_list_le_max
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
x : Cardinal.{u_1}
⊢ #(List (Quotient.out x)) ≤ max ℵ₀ #(Quotient.out x)

Tactic:
exact mk_list_le_max _

Premises used: Cardinal.mk_list_le_max
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
inst : Infinite α
⊢ #(Finset α) = #α

Tactic:
Eq.symm <|
    le_antisymm (mk_le_of_injective fun _ _ => Finset.singleton_inj.1) <|
      calc
        #(Finset α) ≤ #(List α) := mk_le_of_surjective List.toFinset_surjective
        _ = #α := mk_list_eq_mk α

Premises used: Cardinal.mk_le_of_surjective, Trans.trans, Cardinal.mk_list_eq_mk, List.toFinset_surjective, le_antisymm, Finset.singleton_inj, Iff.mp, Cardinal.mk_le_of_injective, Eq.symm
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
inst : Infinite α
⊢ #(Finset α) = #α

Tactic:
exact Eq.symm <|
    le_antisymm (mk_le_of_injective fun _ _ => Finset.singleton_inj.1) <|
      calc
        #(Finset α) ≤ #(List α) := mk_le_of_surjective List.toFinset_surjective
        _ = #α := mk_list_eq_mk α

Premises used: Cardinal.mk_le_of_surjective, Finset, Cardinal.mk_list_eq_mk, List.toFinset_surjective, le_antisymm, List, Finset.singleton_inj, Iff.mp, Cardinal.mk_le_of_injective, Eq.symm
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
inst : Infinite α
⊢ #(Finset α) = #α

Tactic:
classical
  exact Eq.symm <|
    le_antisymm (mk_le_of_injective fun _ _ => Finset.singleton_inj.1) <|
      calc
        #(Finset α) ≤ #(List α) := mk_le_of_surjective List.toFinset_surjective
        _ = #α := mk_list_eq_mk α

Premises used: Cardinal.mk_le_of_surjective, Finset, Cardinal.mk_list_eq_mk, List.toFinset_surjective, le_antisymm, List, Finset.singleton_inj, Iff.mp, Cardinal.mk_le_of_injective, Eq.symm
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
inst : Infinite α
c : Cardinal.{u}
rw : #{ t : Set α // #(↑t : Type u) ≤ c } ≤ (#α + 1) ^ c
⊢ #{ t : Set α // #(↑t : Type u) ≤ c } ≤ #α ^ c

Tactic:
rw [← add_one_eq (aleph0_le_mk α)]

Premises used: Cardinal.add_one_eq, Cardinal.aleph0_le_mk
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
inst : Infinite α
c : Cardinal.{u}
mk : ∀ (β : Type u), #{ t : Set α // #(↑t : Type u) ≤ #β } ≤ (#α + 1) ^ #β
⊢ #{ t : Set α // #(↑t : Type u) ≤ c } ≤ (#α + 1) ^ c

Tactic:
induction c using Cardinal.inductionOn with | _ β
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
inst : Infinite α
β : Type u
mk : (fun (α β : Type u) ↦ β → α) (α ⊕ ULift.{u, 0} (Fin 1)) β → { t : Set α // #(↑t : Type u) ≤ #β }
mk₁ :
  Surjective (β := { t : Set α // #(↑t : Type u) ≤ #β })
    fun (f : (fun (α β : Type u) ↦ β → α) (α ⊕ ULift.{u, 0} (Fin 1)) β) ↦
    Subtype.mk (p := fun (t : Set α) ↦ #(↑t : Type u) ≤ #β) (Sum.inl ⁻¹' range f) ⋯
⊢ #{ t : Set α // #(↑t : Type u) ≤ #β } ≤ (#α + 1) ^ #β

Tactic:
fapply mk_le_of_surjective

Premises used: Cardinal.mk_le_of_surjective
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
inst : Infinite α
β : Type u
f : (fun (α β : Type u) ↦ β → α) (α ⊕ ULift.{u, 0} (Fin 1)) β
property : #(↑(Sum.inl ⁻¹' range f) : Type u) ≤ #β
⊢ { t : Set α // #(↑t : Type u) ≤ #β }

Tactic:
use Sum.inl ⁻¹' range f

Premises used: Sum.inl, Set.range
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
inst : Infinite α
β : Type u
f : (fun (α β : Type u) ↦ β → α) (α ⊕ ULift.{u, 0} (Fin 1)) β
⊢ #(↑(Sum.inl ⁻¹' range f) : Type u) ≤ #β

Tactic:
le_trans (mk_preimage_of_injective _ _ fun x y => Sum.inl.inj) ?_

Premises used: Sum.inl.inj, Cardinal.mk_preimage_of_injective, le_trans
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
inst : Infinite α
β : Type u
f : (fun (α β : Type u) ↦ β → α) (α ⊕ ULift.{u, 0} (Fin 1)) β
property : #(↑(range f) : Type u) ≤ #β
⊢ #(↑(Sum.inl ⁻¹' range f) : Type u) ≤ #β

Tactic:
refine le_trans (mk_preimage_of_injective _ _ fun x y => Sum.inl.inj) ?_

Premises used: Sum.inl.inj, Cardinal.mk_preimage_of_injective, le_trans
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
inst : Infinite α
β : Type u
f : (fun (α β : Type u) ↦ β → α) (α ⊕ ULift.{u, 0} (Fin 1)) β
⊢ #(↑(range f) : Type u) ≤ #β

Tactic:
apply mk_range_le

Premises used: Cardinal.mk_range_le
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
inst : Infinite α
β : Type u
s : Set α
g : (↑s : Type u) ↪ β
h :
  Eq (α := { t : Set α // #(↑t : Type u) ≤ #β })
    ((fun (f : (fun (α β : Type u) ↦ β → α) (α ⊕ ULift.{u, 0} (Fin 1)) β) ↦
        (Subtype.mk (p := fun (t : Set α) ↦ #(↑t : Type u) ≤ #β) (Sum.inl ⁻¹' range f) ⋯ :
          { t : Set α // #(↑t : Type u) ≤ #β }))
      fun (y : β) ↦
      if h : ∃ (x : (↑s : Type u)), (g : (a : (↑s : Type u)) → β) x = y then
        Sum.inl (↑(Classical.choose (p := fun (x : (↑s : Type u)) ↦ (g : (a : (↑s : Type u)) → β) x = y) h) : α)
      else Sum.inr { down := 0 })
    (Subtype.mk (p := fun (t : Set α) ↦ #(↑t : Type u) ≤ #β) s ⋯)
⊢ ∃ (a : (fun (α β : Type u) ↦ β → α) (α ⊕ ULift.{u, 0} (Fin 1)) β),
    Eq (α := { t : Set α // #(↑t : Type u) ≤ #β })
      ((fun (f : (fun (α β : Type u) ↦ β → α) (α ⊕ ULift.{u, 0} (Fin 1)) β) ↦
          (Subtype.mk (p := fun (t : Set α) ↦ #(↑t : Type u) ≤ #β) (Sum.inl ⁻¹' range f) ⋯ :
            { t : Set α // #(↑t : Type u) ≤ #β }))
        a)
      (Subtype.mk (p := fun (t : Set α) ↦ #(↑t : Type u) ≤ #β) s ⋯)

Tactic:
use fun y => if h : ∃ x : s, g x = y then Sum.inl (Classical.choose h).val
               else Sum.inr (ULift.up 0)

Premises used: Exists, Sum.inl, dite, Sum.inr, Classical.choose, OfNat.ofNat, ULift.up, Subtype.val, Eq, DFunLike.coe
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
inst : Infinite α
β : Type u
s : Set α
g : (↑s : Type u) ↪ β
h :
  (↑((fun (f : (fun (α β : Type u) ↦ β → α) (α ⊕ ULift.{u, 0} (Fin 1)) β) ↦
            (Subtype.mk (p := fun (t : Set α) ↦ #(↑t : Type u) ≤ #β) (Sum.inl ⁻¹' range f) ⋯ :
              { t : Set α // #(↑t : Type u) ≤ #β }))
          fun (y : β) ↦
          if h : ∃ (x : (↑s : Type u)), (g : (a : (↑s : Type u)) → β) x = y then
            Sum.inl (↑(Classical.choose (p := fun (x : (↑s : Type u)) ↦ (g : (a : (↑s : Type u)) → β) x = y) h) : α)
          else Sum.inr { down := 0 }) :
      Set α) =
    (↑(Subtype.mk (p := fun (t : Set α) ↦ #(↑t : Type u) ≤ #β) s ⋯) : Set α)
⊢ Eq (α := { t : Set α // #(↑t : Type u) ≤ #β })
    ((fun (f : (fun (α β : Type u) ↦ β → α) (α ⊕ ULift.{u, 0} (Fin 1)) β) ↦
        (Subtype.mk (p := fun (t : Set α) ↦ #(↑t : Type u) ≤ #β) (Sum.inl ⁻¹' range f) ⋯ :
          { t : Set α // #(↑t : Type u) ≤ #β }))
      fun (y : β) ↦
      if h : ∃ (x : (↑s : Type u)), (g : (a : (↑s : Type u)) → β) x = y then
        Sum.inl (↑(Classical.choose (p := fun (x : (↑s : Type u)) ↦ (g : (a : (↑s : Type u)) → β) x = y) h) : α)
      else Sum.inr { down := 0 })
    (Subtype.mk (p := fun (t : Set α) ↦ #(↑t : Type u) ≤ #β) s ⋯)

Tactic:
apply Subtype.ext

Premises used: Subtype.ext
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
inst : Infinite α
β : Type u
s : Set α
g : (↑s : Type u) ↪ β
h :
  ∀ (x : α),
    Membership.mem (γ := Set α)
        (↑((fun (f : (fun (α β : Type u) ↦ β → α) (α ⊕ ULift.{u, 0} (Fin 1)) β) ↦
                (Subtype.mk (p := fun (t : Set α) ↦ #(↑t : Type u) ≤ #β) (Sum.inl ⁻¹' range f) ⋯ :
                  { t : Set α // #(↑t : Type u) ≤ #β }))
              fun (y : β) ↦
              if h : ∃ (x : (↑s : Type u)), (g : (a : (↑s : Type u)) → β) x = y then
                Sum.inl (↑(Classical.choose (p := fun (x : (↑s : Type u)) ↦ (g : (a : (↑s : Type u)) → β) x = y) h) : α)
              else Sum.inr { down := 0 }) :
          Set α)
        x ↔
      x ∈ (↑(Subtype.mk (p := fun (t : Set α) ↦ #(↑t : Type u) ≤ #β) s ⋯) : Set α)
⊢ (↑((fun (f : (fun (α β : Type u) ↦ β → α) (α ⊕ ULift.{u, 0} (Fin 1)) β) ↦
            (Subtype.mk (p := fun (t : Set α) ↦ #(↑t : Type u) ≤ #β) (Sum.inl ⁻¹' range f) ⋯ :
              { t : Set α // #(↑t : Type u) ≤ #β }))
          fun (y : β) ↦
          if h : ∃ (x : (↑s : Type u)), (g : (a : (↑s : Type u)) → β) x = y then
            Sum.inl (↑(Classical.choose (p := fun (x : (↑s : Type u)) ↦ (g : (a : (↑s : Type u)) → β) x = y) h) : α)
          else Sum.inr { down := 0 }) :
      Set α) =
    (↑(Subtype.mk (p := fun (t : Set α) ↦ #(↑t : Type u) ≤ #β) s ⋯) : Set α)

Tactic:
ext x
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
inst : Infinite α
β : Type u
s : Set α
g : (↑s : Type u) ↪ β
x : α
h :
  Membership.mem (γ := Set α)
      (↑((fun (f : (fun (α β : Type u) ↦ β → α) (α ⊕ ULift.{u, 0} (Fin 1)) β) ↦
              (Subtype.mk (p := fun (t : Set α) ↦ #(↑t : Type u) ≤ #β) (Sum.inl ⁻¹' range f) ⋯ :
                { t : Set α // #(↑t : Type u) ≤ #β }))
            fun (y : β) ↦
            if h : ∃ (x : (↑s : Type u)), (g : (a : (↑s : Type u)) → β) x = y then
              Sum.inl (↑(Classical.choose (p := fun (x : (↑s : Type u)) ↦ (g : (a : (↑s : Type u)) → β) x = y) h) : α)
            else Sum.inr { down := 0 }) :
        Set α)
      x →
    x ∈ (↑(Subtype.mk (p := fun (t : Set α) ↦ #(↑t : Type u) ≤ #β) s ⋯) : Set α)
h₁ :
  x ∈ (↑(Subtype.mk (p := fun (t : Set α) ↦ #(↑t : Type u) ≤ #β) s ⋯) : Set α) →
    Membership.mem (γ := Set α)
      (↑((fun (f : (fun (α β : Type u) ↦ β → α) (α ⊕ ULift.{u, 0} (Fin 1)) β) ↦
              (Subtype.mk (p := fun (t : Set α) ↦ #(↑t : Type u) ≤ #β) (Sum.inl ⁻¹' range f) ⋯ :
                { t : Set α // #(↑t : Type u) ≤ #β }))
            fun (y : β) ↦
            if h : ∃ (x : (↑s : Type u)), (g : (a : (↑s : Type u)) → β) x = y then
              Sum.inl (↑(Classical.choose (p := fun (x : (↑s : Type u)) ↦ (g : (a : (↑s : Type u)) → β) x = y) h) : α)
            else Sum.inr { down := 0 }) :
        Set α)
      x
⊢ Membership.mem (γ := Set α)
      (↑((fun (f : (fun (α β : Type u) ↦ β → α) (α ⊕ ULift.{u, 0} (Fin 1)) β) ↦
              (Subtype.mk (p := fun (t : Set α) ↦ #(↑t : Type u) ≤ #β) (Sum.inl ⁻¹' range f) ⋯ :
                { t : Set α // #(↑t : Type u) ≤ #β }))
            fun (y : β) ↦
            if h : ∃ (x : (↑s : Type u)), (g : (a : (↑s : Type u)) → β) x = y then
              Sum.inl (↑(Classical.choose (p := fun (x : (↑s : Type u)) ↦ (g : (a : (↑s : Type u)) → β) x = y) h) : α)
            else Sum.inr { down := 0 }) :
        Set α)
      x ↔
    x ∈ (↑(Subtype.mk (p := fun (t : Set α) ↦ #(↑t : Type u) ≤ #β) s ⋯) : Set α)

Tactic:
constructor
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
inst : Infinite α
β : Type u
s : Set α
g : (↑s : Type u) ↪ β
x : α
y : β
h :
  Eq (α := α ⊕ ULift.{u, 0} (Fin 1))
    (if h : ∃ (x : (↑s : Type u)), (g : (a : (↑s : Type u)) → β) x = y then
      Sum.inl (↑(Classical.choose (p := fun (x : (↑s : Type u)) ↦ (g : (a : (↑s : Type u)) → β) x = y) h) : α)
    else Sum.inr { down := 0 })
    (Sum.inl x)
pos :
  ∀ (h' : ∃ (z : (↑s : Type u)), (g : (a : (↑s : Type u)) → β) z = y),
    x ∈ (↑(Subtype.mk (p := fun (t : Set α) ↦ #(↑t : Type u) ≤ #β) s ⋯) : Set α)
neg :
  ∀ (h' : ¬∃ (z : (↑s : Type u)), (g : (a : (↑s : Type u)) → β) z = y),
    x ∈ (↑(Subtype.mk (p := fun (t : Set α) ↦ #(↑t : Type u) ≤ #β) s ⋯) : Set α)
⊢ x ∈ (↑(Subtype.mk (p := fun (t : Set α) ↦ #(↑t : Type u) ≤ #β) s ⋯) : Set α)

Tactic:
by_cases h' : ∃ z : s, g z = y
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
inst : Infinite α
β : Type u
s : Set α
g : (↑s : Type u) ↪ β
x : α
y : β
h :
  Eq (α := α ⊕ ULift.{u, 0} (Fin 1))
    (if h : ∃ (x : (↑s : Type u)), (g : (a : (↑s : Type u)) → β) x = y then
      Sum.inl (↑(Classical.choose (p := fun (x : (↑s : Type u)) ↦ (g : (a : (↑s : Type u)) → β) x = y) h) : α)
    else Sum.inr { down := 0 })
    (Sum.inl x)
h' : ∃ (z : (↑s : Type u)), (g : (a : (↑s : Type u)) → β) z = y
⊢ Eq (α := α ⊕ ULift.{u, 0} (Fin 1))
    (Sum.inl (↑(Classical.choose (p := fun (x : (↑s : Type u)) ↦ (g : (a : (↑s : Type u)) → β) x = y) h') : α))
    (Sum.inl x)

Tactic:
rw [dif_pos h'] at h

Premises used: dif_pos
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
inst : Infinite α
β : Type u
s : Set α
g : (↑s : Type u) ↪ β
x : α
y : β
h' : ∃ (z : (↑s : Type u)), (g : (a : (↑s : Type u)) → β) z = y
h :
  Eq (α := α ⊕ ULift.{u, 0} (Fin 1))
    (Sum.inl (↑(Classical.choose (p := fun (x : (↑s : Type u)) ↦ (g : (a : (↑s : Type u)) → β) x = y) h') : α))
    (Sum.inl x)
pos :
  ∀
    (h :
      Eq (α := α ⊕ ULift.{u, 0} (Fin 1))
        (Sum.inl (↑(Classical.choose (p := fun (x : (↑s : Type u)) ↦ (g : (a : (↑s : Type u)) → β) x = y) h') : α))
        (Sum.inl (↑(Classical.choose (p := fun (x : (↑s : Type u)) ↦ (g : (a : (↑s : Type u)) → β) x = y) h') : α))),
    (↑(Classical.choose (p := fun (x : (↑s : Type u)) ↦ (g : (a : (↑s : Type u)) → β) x = y) h') : α) ∈
      (↑(Subtype.mk (p := fun (t : Set α) ↦ #(↑t : Type u) ≤ #β) s ⋯) : Set α)
⊢ x ∈ (↑(Subtype.mk (p := fun (t : Set α) ↦ #(↑t : Type u) ≤ #β) s ⋯) : Set α)

Tactic:
cases Sum.inl.inj h

Premises used: Sum.inl.inj
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
inst : Infinite α
β : Type u
s : Set α
g : (↑s : Type u) ↪ β
y : β
h' : ∃ (z : (↑s : Type u)), (g : (a : (↑s : Type u)) → β) z = y
h :
  Eq (α := α ⊕ ULift.{u, 0} (Fin 1))
    (Sum.inl (↑(Classical.choose (p := fun (x : (↑s : Type u)) ↦ (g : (a : (↑s : Type u)) → β) x = y) h') : α))
    (Sum.inl (↑(Classical.choose (p := fun (x : (↑s : Type u)) ↦ (g : (a : (↑s : Type u)) → β) x = y) h') : α))
⊢ (↑(Classical.choose (p := fun (x : (↑s : Type u)) ↦ (g : (a : (↑s : Type u)) → β) x = y) h') : α) ∈
    (↑(Subtype.mk (p := fun (t : Set α) ↦ #(↑t : Type u) ≤ #β) s ⋯) : Set α)

Tactic:
(Classical.choose h').2

Premises used: Set.Mem, Classical.choose, Subtype.property
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
inst : Infinite α
β : Type u
s : Set α
g : (↑s : Type u) ↪ β
y : β
h' : ∃ (z : (↑s : Type u)), (g : (a : (↑s : Type u)) → β) z = y
h :
  Eq (α := α ⊕ ULift.{u, 0} (Fin 1))
    (Sum.inl (↑(Classical.choose (p := fun (x : (↑s : Type u)) ↦ (g : (a : (↑s : Type u)) → β) x = y) h') : α))
    (Sum.inl (↑(Classical.choose (p := fun (x : (↑s : Type u)) ↦ (g : (a : (↑s : Type u)) → β) x = y) h') : α))
⊢ (↑(Classical.choose (p := fun (x : (↑s : Type u)) ↦ (g : (a : (↑s : Type u)) → β) x = y) h') : α) ∈
    (↑(Subtype.mk (p := fun (t : Set α) ↦ #(↑t : Type u) ≤ #β) s ⋯) : Set α)

Tactic:
exact (Classical.choose h').2

Premises used: Classical.choose, Subtype.property
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
inst : Infinite α
β : Type u
s : Set α
g : (↑s : Type u) ↪ β
x : α
y : β
h :
  Eq (α := α ⊕ ULift.{u, 0} (Fin 1))
    (if h : ∃ (x : (↑s : Type u)), (g : (a : (↑s : Type u)) → β) x = y then
      Sum.inl (↑(Classical.choose (p := fun (x : (↑s : Type u)) ↦ (g : (a : (↑s : Type u)) → β) x = y) h) : α)
    else Sum.inr { down := 0 })
    (Sum.inl x)
h' : ¬∃ (z : (↑s : Type u)), (g : (a : (↑s : Type u)) → β) z = y
⊢ Eq (α := α ⊕ ULift.{u, 0} (Fin 1)) (Sum.inr { down := 0 }) (Sum.inl x)

Tactic:
rw [dif_neg h'] at h

Premises used: dif_neg
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
inst : Infinite α
β : Type u
s : Set α
g : (↑s : Type u) ↪ β
x : α
y : β
h :
  Eq (α := α ⊕ ULift.{u, 0} (Fin 1))
    (if h : ∃ (x : (↑s : Type u)), (g : (a : (↑s : Type u)) → β) x = y then
      Sum.inl (↑(Classical.choose (p := fun (x : (↑s : Type u)) ↦ (g : (a : (↑s : Type u)) → β) x = y) h) : α)
    else Sum.inr { down := 0 })
    (Sum.inl x)
h' : ¬∃ (z : (↑s : Type u)), (g : (a : (↑s : Type u)) → β) z = y
h₁ : Eq (α := α ⊕ ULift.{u, 0} (Fin 1)) (Sum.inr { down := 0 }) (Sum.inl x)
⊢ ¬∃ (z : (↑s : Type u)), (g : (a : (↑s : Type u)) → β) z = y

Tactic:
rw [dif_neg h'] at h

Premises used: dif_neg
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
inst : Infinite α
β : Type u
s : Set α
g : (↑s : Type u) ↪ β
x : α
y : β
h : Eq (α := α ⊕ ULift.{u, 0} (Fin 1)) (Sum.inr { down := 0 }) (Sum.inl x)
h' : ¬∃ (z : (↑s : Type u)), (g : (a : (↑s : Type u)) → β) z = y
⊢ x ∈ (↑(Subtype.mk (p := fun (t : Set α) ↦ #(↑t : Type u) ≤ #β) s ⋯) : Set α)

Tactic:
cases h
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
inst : Infinite α
β : Type u
s : Set α
g : (↑s : Type u) ↪ β
x : α
h : x ∈ (↑(Subtype.mk (p := fun (t : Set α) ↦ #(↑t : Type u) ≤ #β) s ⋯) : Set α)
⊢ ∃ (z : (↑s : Type u)),
    Eq (α := β) ((g : (a : (↑s : Type u)) → β) z : β)
      ((g : (a : (↑s : Type u)) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x h) : β)

Tactic:
have : ∃ z : s, g z = g ⟨x, h⟩ := ⟨⟨x, h⟩, rfl⟩