awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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} #(α ≃ α) = #(α → β')
rw₁ : lift.{max u v, u} #(α ≃ α) = lift.{max u v, u} #(α → α)
⊢ #(α ≃ β') = #(α → β')
have rw₂ : #(α ≃ α) = #(α → α)
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} #(α ≃ α) = #(α → β')
rw₁ : lift.{max u v, u} #(α ≃ α) = lift.{max u v, u} #(α → α)
rw₂ : #(α ≃ α) = #(α → α)
⊢ #(α ≃ β') = #(α → β')
have rw₃ : #α ^ #α = #(α → α)
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} #(α ≃ α) = #(α → β')
rw₁ : lift.{max u v, u} #(α ≃ α) = lift.{max u v, u} #(α → α)
rw₂ : #(α ≃ α) = #(α → α)
rw₃ : #α ^ #α = #(α → α)
⊢ #(α ≃ β') = #(α → β')
have rw₄ : #(α → α) = #(α → α)
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
inst : Infinite α
eq : #α = #β
⊢ #(α ≃ β) = HPow.hPow (α := Cardinal.{u}) 2 #α
have rw : HPow.hPow (α := Cardinal.{u}) 2 (lift.{u, u} #α) = HPow.hPow (α := Cardinal.{u}) 2 #α
Tactic: rw [mk_equiv_of_lift_eq (lift_inj.mpr eq), lift_id]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α β : Type u
inst : Infinite α
eq : #α = #β
rw : HPow.hPow (α := Cardinal.{u}) 2 (lift.{u, u} #α) = HPow.hPow (α := Cardinal.{u}) 2 #α
⊢ #(α ≃ β) = HPow.hPow (α := Cardinal.{u}) 2 #α
have rw₁ : HPow.hPow (α := Cardinal.{u}) 2 #α = HPow.hPow (α := Cardinal.{u}) 2 #α
Tactic: rw [mk_equiv_of_lift_eq (lift_inj.mpr eq), lift_id]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
β' : Type v
inst : Infinite α
lle : lift.{u, v} #β' ≤ lift.{v, u} #α
| #(β' ↪ α)
have rw : #(Embedding.{v + 1, u + 1} β' (α × α))
Tactic: rw [← (Equiv.embeddingCongr (.refl _)
      (Cardinal.eq.mp <| mul_eq_self <| aleph0_le_mk α).some).cardinal_eq]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
β' : Type v
inst : Infinite α
lle : lift.{u, v} #β' ≤ lift.{v, u} #α
⊢ #(β' → α) ≤ #(β' ↪ α)
have 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]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
β' : Type v
inst : Infinite α
lle : lift.{u, v} #β' ≤ lift.{v, u} #α
⊢ #(β' → α) ≤ #(Embedding.{v + 1, u + 1} β' (α × α))
have obtain : ∀ (e : β' ↪ α), #(β' → α) ≤ #(Embedding.{v + 1, u + 1} β' (α × α))
Tactic: obtain ⟨e⟩ := lift_mk_le'.mp lle
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
β' : Type v
inst : Infinite α
lle : lift.{u, v} #β' ≤ lift.{v, u} #α
⊢ Nonempty (α ≃ α ⊕ β')
have simp_rw : lift.{max u v, u} #α = lift.{max v u, u} #α + lift.{u, v} #β'
Tactic: simp_rw [← lift_mk_eq', mk_sum, lift_add, lift_lift]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
β' : Type v
inst : Infinite α
lle : lift.{u, v} #β' ≤ lift.{v, u} #α
⊢ lift.{max u v, u} #α = lift.{max v u, u} #α + lift.{u, v} #β'
have rw : lift.{v, u} #α + lift.{u, v} #β' = lift.{v, u} #α
Tactic: rw [lift_umax.{u, v}, eq_comm]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
inst : Nonempty α
⊢ #(List α) = max ℵ₀ #α
have inl : Finite α → #(List α) = max ℵ₀ #α
Tactic: cases finite_or_infinite α
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
inst : Nonempty α
inl : Finite α → #(List α) = max ℵ₀ #α
⊢ #(List α) = max ℵ₀ #α
have inr : Infinite α → #(List α) = max ℵ₀ #α
Tactic: cases finite_or_infinite α
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
inst : Nonempty α
h : Finite α
⊢ #(List α) = max ℵ₀ #α
have inl : #α ≤ ℵ₀
Tactic: rw [mk_list_eq_aleph0, eq_comm, max_eq_left]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
inst : Nonempty α
h : Infinite α
⊢ #(List α) = max ℵ₀ #α
have inr : ℵ₀ ≤ #α
Tactic: rw [mk_list_eq_mk, eq_comm, max_eq_right]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
inst : Nonempty α
⊢ #(List α) = max #α ℵ₀
have rw : max ℵ₀ #α = max #α ℵ₀
Tactic: rw [mk_list_eq_max, max_comm]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
inst : Nonempty α
rw : max ℵ₀ #α = max #α ℵ₀
⊢ #(List α) = max #α ℵ₀
have rw₁ : max #α ℵ₀ = max #α ℵ₀
Tactic: rw [mk_list_eq_max, max_comm]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (hypothesis)
Goal:
x : Cardinal.{u_1}
h : x ≠ 0
⊢ (sum fun (n : ℕ) ↦ x ^ n) = max ℵ₀ x
have this : Nonempty.{u_1 + 1} (Quotient.out x)
Tactic: have := nonempty_out h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
x : Cardinal.{u_1}
h : x ≠ 0
this : Nonempty.{u_1 + 1} (Quotient.out x)
| sum fun (n : ℕ) ↦ x ^ n
have rw : max ℵ₀ x
Tactic: rw [← x.mk_out, ← mk_list_eq_sum_pow, mk_list_eq_max, mk_out]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
x : Cardinal.{u_1}
h : x ≠ 0
this : Nonempty.{u_1 + 1} (Quotient.out x)
⊢ (sum fun (n : ℕ) ↦ x ^ n) = max ℵ₀ x
have conv_lhs : (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]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
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
⊢ (sum fun (n : ℕ) ↦ x ^ n) = max ℵ₀ x
have conv_lhs₁ : max ℵ₀ x = max ℵ₀ x
Tactic: conv_lhs => rw [← x.mk_out, ← mk_list_eq_sum_pow, mk_list_eq_max, mk_out]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
⊢ #(List α) ≤ max ℵ₀ #α
have inl : Finite α → #(List α) ≤ max ℵ₀ #α
Tactic: cases finite_or_infinite α
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
inl : Finite α → #(List α) ≤ max ℵ₀ #α
⊢ #(List α) ≤ max ℵ₀ #α
have inr : Infinite α → #(List α) ≤ max ℵ₀ #α
Tactic: cases finite_or_infinite α
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
h : Infinite α
⊢ #(List α) ≤ max ℵ₀ #α
have inr : #α ≤ max ℵ₀ #α
Tactic: rw [mk_list_eq_mk]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
x : Cardinal.{u_1}
⊢ (sum fun (n : ℕ) ↦ x ^ n) ≤ max ℵ₀ x
have rw : #(List (Quotient.out x)) ≤ max ℵ₀ #(Quotient.out x)
Tactic: rw [← x.mk_out, ← mk_list_eq_sum_pow]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
inst : Infinite α
c : Cardinal.{u}
⊢ #{ t : Set α // #(↑t : Type u) ≤ c } ≤ #α ^ c
have rw : #{ t : Set α // #(↑t : Type u) ≤ c } ≤ (#α + 1) ^ c
Tactic: rw [← add_one_eq (aleph0_le_mk α)]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
inst : Infinite α
c : Cardinal.{u}
⊢ #{ t : Set α // #(↑t : Type u) ≤ c } ≤ (#α + 1) ^ c
have mk : ∀ (β : Type u), #{ t : Set α // #(↑t : Type u) ≤ #β } ≤ (#α + 1) ^ #β
Tactic: induction c using Cardinal.inductionOn with | _ β
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
inst : Infinite α
β : Type u
⊢ #{ t : Set α // #(↑t : Type u) ≤ #β } ≤ (#α + 1) ^ #β
have mk : (fun (α β : Type u) ↦ β → α) (α ⊕ ULift.{u, 0} (Fin 1)) β → { t : Set α // #(↑t : Type u) ≤ #β }
Tactic: fapply mk_le_of_surjective
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
inst : Infinite α
β : Type u
mk : (fun (α β : Type u) ↦ β → α) (α ⊕ ULift.{u, 0} (Fin 1)) β → { t : Set α // #(↑t : Type u) ≤ #β }
⊢ #{ t : Set α // #(↑t : Type u) ≤ #β } ≤ (#α + 1) ^ #β
have 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) sorry
Tactic: fapply mk_le_of_surjective
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
inst : Infinite α
β : Type u
f : (fun (α β : Type u) ↦ β → α) (α ⊕ ULift.{u, 0} (Fin 1)) β
⊢ { t : Set α // #(↑t : Type u) ≤ #β }
have property : #(↑(Sum.inl ⁻¹' range f) : Type u) ≤ #β
Tactic: use Sum.inl ⁻¹' range f
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
inst : Infinite α
β : Type u
f : (fun (α β : Type u) ↦ β → α) (α ⊕ ULift.{u, 0} (Fin 1)) β
⊢ #(↑(Sum.inl ⁻¹' range f) : Type u) ≤ #β
have property : #(↑(range f) : Type u) ≤ #β
Tactic: refine le_trans (mk_preimage_of_injective _ _ fun x y => Sum.inl.inj) ?_
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
inst : Infinite α
β : Type u
s : Set α
g : (↑s : Type u) ↪ β
⊢ ∃ (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 ⋯)
have 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) sorry :
        { 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 sorry)
Tactic: use fun y => if h : ∃ x : s, g x = y then Sum.inl (Classical.choose h).val
               else Sum.inr (ULift.up 0)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
inst : Infinite α
β : Type u
s : Set α
g : (↑s : Type u) ↪ β
⊢ 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 ⋯)
have h : (↑((fun (f : (fun (α β : Type u) ↦ β → α) (α ⊕ ULift.{u, 0} (Fin 1)) β) ↦
          (Subtype.mk (p := fun (t : Set α) ↦ #(↑t : Type u) ≤ #β) (Sum.inl ⁻¹' range f) sorry :
            { 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 sorry) : Set α)
Tactic: apply Subtype.ext
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
inst : Infinite α
β : Type u
s : Set α
g : (↑s : 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 }) :
      Set α) =
    (↑(Subtype.mk (p := fun (t : Set α) ↦ #(↑t : Type u) ≤ #β) s ⋯) : Set α)
have 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) sorry :
                { 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 sorry) : Set α)
Tactic: ext x
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
inst : Infinite α
β : Type u
s : Set α
g : (↑s : Type u) ↪ β
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 α)
have 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) sorry :
              { 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 sorry) : Set α)
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
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 α)
⊢ 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 α)
have h₁ : x ∈ (↑(Subtype.mk (p := fun (t : Set α) ↦ #(↑t : Type u) ≤ #β) s sorry) : 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) sorry :
              { 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
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)
⊢ x ∈ (↑(Subtype.mk (p := fun (t : Set α) ↦ #(↑t : Type u) ≤ #β) s ⋯) : Set α)
have pos : ∀ (h' : ∃ (z : (↑s : Type u)), (g : (a : (↑s : Type u)) → β) z = y),
  x ∈ (↑(Subtype.mk (p := fun (t : Set α) ↦ #(↑t : Type u) ≤ #β) s sorry) : Set α)
Tactic: by_cases h' : ∃ z : s, g z = y
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
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 α)
⊢ x ∈ (↑(Subtype.mk (p := fun (t : Set α) ↦ #(↑t : Type u) ≤ #β) s ⋯) : Set α)
have neg : ∀ (h' : ¬∃ (z : (↑s : Type u)), (g : (a : (↑s : Type u)) → β) z = y),
  x ∈ (↑(Subtype.mk (p := fun (t : Set α) ↦ #(↑t : Type u) ≤ #β) s sorry) : Set α)
Tactic: by_cases h' : ∃ z : s, g z = y
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (hypothesis)
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
⊢ x ∈ (↑(Subtype.mk (p := fun (t : Set α) ↦ #(↑t : Type u) ≤ #β) s ⋯) : Set α)
have 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)
Tactic: rw [dif_pos h'] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
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)
⊢ x ∈ (↑(Subtype.mk (p := fun (t : Set α) ↦ #(↑t : Type u) ≤ #β) s ⋯) : Set α)
have 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 sorry) : Set α)
Tactic: cases Sum.inl.inj h
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (hypothesis)
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
⊢ x ∈ (↑(Subtype.mk (p := fun (t : Set α) ↦ #(↑t : Type u) ≤ #β) s ⋯) : Set α)
have h₁ : Eq (α := α ⊕ ULift.{u, 0} (Fin 1)) (Sum.inr { down := 0 }) (Sum.inl x)
Tactic: rw [dif_neg h'] at h
Cleared hypotheses: h, h'
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (hypothesis)
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 α)
⊢ 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
have this : ∃ (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⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
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 α)
this :
  ∃ (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) : β)
⊢ 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
have h₁ : Eq (α := α ⊕ ULift.{u, 0} (Fin 1))
  ((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 } :
        α ⊕ ULift.{u, 0} (Fin 1)))
    ((g : (a : (↑s : Type u)) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x h)))
  (Sum.inl x)
Tactic: use g ⟨x, h⟩