awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) : β)
⊢ Eq (α := α ⊕ ULift.{u, 0} (Fin 1))
    (if h_1 :
        ∃ (x_1 : (↑s : Type u)),
          Eq (α := β) ((g : (a : (↑s : Type u)) → β) x_1 : β)
            ((g : (a : (↑s : Type u)) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x h) : β) then
      Sum.inl
        (↑(Classical.choose (p := fun (x_1 : (↑s : Type u)) ↦
              Eq (α := β) ((g : (a : (↑s : Type u)) → β) x_1 : β)
                ((g : (a : (↑s : Type u)) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x h) : β))
              h_1) :
          α)
    else Sum.inr { down := 0 })
    (Sum.inl x)
have h₁ : Eq (α := α ⊕ ULift.{u, 0} (Fin 1))
  (Sum.inl
    (↑(Classical.choose (p := fun (x_1 : (↑s : Type u)) ↦
          Eq (α := β) ((g : (a : (↑s : Type u)) → β) x_1 : β)
            ((g : (a : (↑s : Type u)) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x h) : β))
          this) :
      α))
  (Sum.inl x)
Tactic: rw [dif_pos this]
-- 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) : β)
⊢ Eq (α := α ⊕ ULift.{u, 0} (Fin 1))
    (Sum.inl
      (↑(Classical.choose (p := fun (x_1 : (↑s : Type u)) ↦
            Eq (α := β) ((g : (a : (↑s : Type u)) → β) x_1 : β)
              ((g : (a : (↑s : Type u)) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x h) : β))
            this) :
        α))
    (Sum.inl x)
have h₁ : (↑(Classical.choose (p := fun (x_1 : (↑s : Type u)) ↦
        Eq (α := β) ((g : (a : (↑s : Type u)) → β) x_1 : β)
          ((g : (a : (↑s : Type u)) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x h) : β))
        this) :
    α) =
  x
Tactic: congr
-- 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) : β)
⊢ (↑(Classical.choose (p := fun (x_1 : (↑s : Type u)) ↦
          Eq (α := β) ((g : (a : (↑s : Type u)) → β) x_1 : β)
            ((g : (a : (↑s : Type u)) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x h) : β))
          this) :
      α) =
    x
have h₁ : Classical.choose (p := fun (x_1 : (↑s : Type u)) ↦
    Eq (α := β) ((g : (a : (↑s : Type u)) → β) x_1 : β)
      ((g : (a : (↑s : Type u)) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x h) : β))
    this =
  Subtype.mk (p := fun (x : α) ↦ x ∈ s) x h
Tactic: suffices Classical.choose this = ⟨x, h⟩ from congr_arg Subtype.val this
-- 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) : β)
⊢ Classical.choose (p := fun (x_1 : (↑s : Type u)) ↦
      Eq (α := β) ((g : (a : (↑s : Type u)) → β) x_1 : β)
        ((g : (a : (↑s : Type u)) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x h) : β))
      this =
    Subtype.mk (p := fun (x : α) ↦ x ∈ s) x h
have h₁ : g.toFun
    (Classical.choose (p := fun (x_1 : (↑s : Type u)) ↦
      Eq (α := β) ((g : (a : (↑s : Type u)) → β) x_1 : β)
        ((g : (a : (↑s : Type u)) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x h) : β))
      this) =
  g.toFun (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x h)
Tactic: apply g.2
-- 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 w : (fun (α β : Type u) ↦ β → α) (α ⊕ ULift.{u, 0} (Fin 1)) β
Tactic: classical
  use fun y => if h : ∃ x : s, g x = y then Sum.inl (Classical.choose h).val
               else Sum.inr (ULift.up 0)
  apply Subtype.ext; ext x
  constructor
  · rintro ⟨y, h⟩
    dsimp only at h
    by_cases h' : ∃ z : s, g z = y
    · rw [dif_pos h'] at h
      cases Sum.inl.inj h
      exact (Classical.choose h').2
    · rw [dif_neg h'] at h
      cases h
  · intro h
    have : ∃ z : s, g z = g ⟨x, h⟩ := ⟨⟨x, h⟩, rfl⟩
    use g ⟨x, h⟩
    dsimp only
    rw [dif_pos this]
    congr
    suffices Classical.choose this = ⟨x, h⟩ from congr_arg Subtype.val this
    apply g.2
    exact Classical.choose_spec this
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
inst : Infinite α
β : Type u
s : Set α
g : (↑s : Type u) ↪ β
w : (fun (α β : Type u) ↦ β → α) (α ⊕ ULift.{u, 0} (Fin 1)) β
⊢ ∃ (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: classical
  use fun y => if h : ∃ x : s, g x = y then Sum.inl (Classical.choose h).val
               else Sum.inr (ULift.up 0)
  apply Subtype.ext; ext x
  constructor
  · rintro ⟨y, h⟩
    dsimp only at h
    by_cases h' : ∃ z : s, g z = y
    · rw [dif_pos h'] at h
      cases Sum.inl.inj h
      exact (Classical.choose h').2
    · rw [dif_neg h'] at h
      cases h
  · intro h
    have : ∃ z : s, g z = g ⟨x, h⟩ := ⟨⟨x, h⟩, rfl⟩
    use g ⟨x, h⟩
    dsimp only
    rw [dif_pos this]
    congr
    suffices Classical.choose this = ⟨x, h⟩ from congr_arg Subtype.val this
    apply g.2
    exact Classical.choose_spec this
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
inst : Infinite α
β : Type u
s : Set α
g : (↑s : Type u) ↪ β
w : (fun (α β : Type u) ↦ β → α) (α ⊕ ULift.{u, 0} (Fin 1)) β
h 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 ⋯)
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: classical
  use fun y => if h : ∃ x : s, g x = y then Sum.inl (Classical.choose h).val
               else Sum.inr (ULift.up 0)
  apply Subtype.ext; ext x
  constructor
  · rintro ⟨y, h⟩
    dsimp only at h
    by_cases h' : ∃ z : s, g z = y
    · rw [dif_pos h'] at h
      cases Sum.inl.inj h
      exact (Classical.choose h').2
    · rw [dif_neg h'] at h
      cases h
  · intro h
    have : ∃ z : s, g z = g ⟨x, h⟩ := ⟨⟨x, h⟩, rfl⟩
    use g ⟨x, h⟩
    dsimp only
    rw [dif_pos this]
    congr
    suffices Classical.choose this = ⟨x, h⟩ from congr_arg Subtype.val this
    apply g.2
    exact Classical.choose_spec this
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
inst : Infinite α
β : Type u
s : Set α
g : (↑s : Type u) ↪ β
w : (fun (α β : Type u) ↦ β → α) (α ⊕ ULift.{u, 0} (Fin 1)) β
h 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 ⋯)
h₂ 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 α)
⊢ ∃ (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₄ : ∀ (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: classical
  use fun y => if h : ∃ x : s, g x = y then Sum.inl (Classical.choose h).val
               else Sum.inr (ULift.up 0)
  apply Subtype.ext; ext x
  constructor
  · rintro ⟨y, h⟩
    dsimp only at h
    by_cases h' : ∃ z : s, g z = y
    · rw [dif_pos h'] at h
      cases Sum.inl.inj h
      exact (Classical.choose h').2
    · rw [dif_neg h'] at h
      cases h
  · intro h
    have : ∃ z : s, g z = g ⟨x, h⟩ := ⟨⟨x, h⟩, rfl⟩
    use g ⟨x, h⟩
    dsimp only
    rw [dif_pos this]
    congr
    suffices Classical.choose this = ⟨x, h⟩ from congr_arg Subtype.val this
    apply g.2
    exact Classical.choose_spec this
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
c : Cardinal.{u}
⊢ #{ t : Set α // #(↑t : Type u) ≤ c } ≤ max #α ℵ₀ ^ c
have trans : #{ t : Set α // #(↑t : Type u) ≤ c } ≤ #{ t : Set (ULift.{u, 0} ℕ ⊕ α) // #(↑t : Type u) ≤ c }
Tactic: trans #{ t : Set ((ULift.{u} ℕ) ⊕ α) // #t ≤ c }
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
c : Cardinal.{u}
trans : #{ t : Set α // #(↑t : Type u) ≤ c } ≤ #{ t : Set (ULift.{u, 0} ℕ ⊕ α) // #(↑t : Type u) ≤ c }
⊢ #{ t : Set α // #(↑t : Type u) ≤ c } ≤ max #α ℵ₀ ^ c
have trans₁ : #{ t : Set (ULift.{u, 0} ℕ ⊕ α) // #(↑t : Type u) ≤ c } ≤ max #α ℵ₀ ^ c
Tactic: trans #{ t : Set ((ULift.{u} ℕ) ⊕ α) // #t ≤ c }
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
c : Cardinal.{u}
⊢ #{ t : Set α // #(↑t : Type u) ≤ c } ≤ #{ t : Set (ULift.{u, 0} ℕ ⊕ α) // #(↑t : Type u) ≤ c }
have refine_1 : Set α ↪ Set (ULift.{u, 0} ℕ ⊕ α)
Tactic: refine ⟨Embedding.subtypeMap ?_ ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
c : Cardinal.{u}
refine_1 : Set α ↪ Set (ULift.{u, 0} ℕ ⊕ α)
⊢ #{ t : Set α // #(↑t : Type u) ≤ c } ≤ #{ t : Set (ULift.{u, 0} ℕ ⊕ α) // #(↑t : Type u) ≤ c }
have refine_2 : ∀ ⦃x : Set α⦄,
  #(↑x : Type u) ≤ c →
    #(↑((Embedding.image { toFun := Sum.inr, inj' := sorry : α ↪ ULift.{u, 0} ℕ ⊕ α } :
                (a : Set α) → Set (ULift.{u, 0} ℕ ⊕ α))
              x) :
          Type u) ≤
      c
Tactic: refine ⟨Embedding.subtypeMap ?_ ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
c : Cardinal.{u}
⊢ Set α ↪ Set (ULift.{u, 0} ℕ ⊕ α)
have refine_1 : α ↪ ULift.{u, 0} ℕ ⊕ α
Tactic: apply Embedding.image
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
c : Cardinal.{u}
⊢ α ↪ ULift.{u, 0} ℕ ⊕ α
have inj' : Injective.{u + 1, u + 1} (α := α) (β := ULift.{u, 0} ℕ ⊕ α) Sum.inr
Tactic: use Sum.inr
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
c : Cardinal.{u}
⊢ #{ t : Set (ULift.{u, 0} ℕ ⊕ α) // #(↑t : Type u) ≤ c } ≤ max #α ℵ₀ ^ c
have apply : #(ULift.{u, 0} ℕ ⊕ α) ^ c ≤ max #α ℵ₀ ^ c
Tactic: apply (mk_bounded_set_le_of_infinite ((ULift.{u} ℕ) ⊕ α) c).trans
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
c : Cardinal.{u}
⊢ #(ULift.{u, 0} ℕ ⊕ α) ^ c ≤ max #α ℵ₀ ^ c
have rw : #(ULift.{u, 0} ℕ ⊕ α) ^ c ≤ #(ULift.{u, 0} ℕ ⊕ α) ^ c
Tactic: rw [max_comm, ← add_eq_max]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
c : Cardinal.{u}
rw : #(ULift.{u, 0} ℕ ⊕ α) ^ c ≤ #(ULift.{u, 0} ℕ ⊕ α) ^ c
⊢ #(ULift.{u, 0} ℕ ⊕ α) ^ c ≤ max #α ℵ₀ ^ c
have rw₁ : ℵ₀ ≤ ℵ₀
Tactic: rw [max_comm, ← add_eq_max]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
s : Set α
c : Cardinal.{u}
⊢ #{ t : Set α // t ⊆ s ∧ #(↑t : Type u) ≤ c } ≤ max #(↑s : Type u) ℵ₀ ^ c
have refine : #{ t : Set α // t ⊆ s ∧ #(↑t : Type u) ≤ c } ≤ #{ t : Set (↑s : Type u) // #(↑t : Type u) ≤ c }
Tactic: refine le_trans ?_ (mk_bounded_set_le s c)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
s : Set α
c : Cardinal.{u}
⊢ #{ t : Set α // t ⊆ s ∧ #(↑t : Type u) ≤ c } ≤ #{ t : Set (↑s : Type u) // #(↑t : Type u) ≤ c }
have refine_1 : { t : Set α // t ⊆ s ∧ #(↑t : Type u) ≤ c } ↪ Set (↑s : Type u)
Tactic: refine ⟨Embedding.codRestrict _ ?_ ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
s : Set α
c : Cardinal.{u}
refine_1 : { t : Set α // t ⊆ s ∧ #(↑t : Type u) ≤ c } ↪ Set (↑s : Type u)
⊢ #{ t : Set α // t ⊆ s ∧ #(↑t : Type u) ≤ c } ≤ #{ t : Set (↑s : Type u) // #(↑t : Type u) ≤ c }
have refine_2 : ∀ (a : { t : Set α // t ⊆ s ∧ #(↑t : Type u) ≤ c }),
  Membership.mem (α := Set (↑s : Type u)) (γ := Set (Set (↑s : Type u)))
    (fun (t : Set (↑s : Type u)) ↦
      Quot.lift (r := HasEquiv.Equiv) ((fun (α β : Type u) ↦ Nonempty.{u + 1} (α ↪ β)) (↑t : Type u)) sorry c)
    (({
            toFun := fun (t : { t : Set α // t ⊆ s ∧ #(↑t : Type u) ≤ c }) ↦
              Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' (↑t : Set α),
            inj' := sorry } :
          (a : { t : Set α // t ⊆ s ∧ #(↑t : Type u) ≤ c }) → Set (↑s : Type u))
        a :
      Set (↑s : Type u))
Tactic: refine ⟨Embedding.codRestrict _ ?_ ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
s : Set α
c : Cardinal.{u}
⊢ { t : Set α // t ⊆ s ∧ #(↑t : Type u) ≤ c } ↪ Set (↑s : Type u)
have inj' : Injective (β := Set (↑s : Type u)) fun (t : { t : Set α // t ⊆ s ∧ #(↑t : Type u) ≤ c }) ↦
  Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' (↑t : Set α)
Tactic: use fun t => (↑) ⁻¹' t.1
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
s : Set α
c : Cardinal.{u}
t : Set α
ht1 : t ⊆ s
ht2 : #(↑t : Type u) ≤ c
t' : Set α
h1t' : t' ⊆ s
h2t' : #(↑t' : Type u) ≤ c
h :
  Eq.{u + 1} (α := Set (↑s : Type u))
    ((fun (t : { t : Set α // t ⊆ s ∧ #(↑t : Type u) ≤ c }) ↦
        (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' (↑t : Set α) : Set (↑s : Type u)))
      (Subtype.mk (p := fun (t : Set α) ↦ t ⊆ s ∧ #(↑t : Type u) ≤ c) t ⋯))
    ((fun (t : { t : Set α // t ⊆ s ∧ #(↑t : Type u) ≤ c }) ↦
        (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' (↑t : Set α) : Set (↑s : Type u)))
      (Subtype.mk (p := fun (t : Set α) ↦ t ⊆ s ∧ #(↑t : Type u) ≤ c) t' ⋯))
⊢ Eq (α := { t : Set α // t ⊆ s ∧ #(↑t : Type u) ≤ c })
    (Subtype.mk (p := fun (t : Set α) ↦ t ⊆ s ∧ #(↑t : Type u) ≤ c) t ⋯)
    (Subtype.mk (p := fun (t : Set α) ↦ t ⊆ s ∧ #(↑t : Type u) ≤ c) t' ⋯)
have inj' : (↑(Subtype.mk (p := fun (t : Set α) ↦ t ⊆ s ∧ #(↑t : Type u) ≤ c) t sorry) : Set α) =
  (↑(Subtype.mk (p := fun (t : Set α) ↦ t ⊆ s ∧ #(↑t : Type u) ≤ c) t' sorry) : Set α)
Tactic: apply Subtype.ext
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
s : Set α
c : Cardinal.{u}
t : Set α
ht1 : t ⊆ s
ht2 : #(↑t : Type u) ≤ c
t' : Set α
h1t' : t' ⊆ s
h2t' : #(↑t' : Type u) ≤ c
h :
  Eq.{u + 1} (α := Set (↑s : Type u))
    ((fun (t : { t : Set α // t ⊆ s ∧ #(↑t : Type u) ≤ c }) ↦
        (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' (↑t : Set α) : Set (↑s : Type u)))
      (Subtype.mk (p := fun (t : Set α) ↦ t ⊆ s ∧ #(↑t : Type u) ≤ c) t ⋯))
    ((fun (t : { t : Set α // t ⊆ s ∧ #(↑t : Type u) ≤ c }) ↦
        (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' (↑t : Set α) : Set (↑s : Type u)))
      (Subtype.mk (p := fun (t : Set α) ↦ t ⊆ s ∧ #(↑t : Type u) ≤ c) t' ⋯))
⊢ (↑(Subtype.mk (p := fun (t : Set α) ↦ t ⊆ s ∧ #(↑t : Type u) ≤ c) t ⋯) : Set α) =
    (↑(Subtype.mk (p := fun (t : Set α) ↦ t ⊆ s ∧ #(↑t : Type u) ≤ c) t' ⋯) : Set α)
have inj' : t = t'
Tactic: dsimp only at h ⊢
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
s : Set α
c : Cardinal.{u}
t : Set α
ht1 : t ⊆ s
ht2 : #(↑t : Type u) ≤ c
t' : Set α
h1t' : t' ⊆ s
h2t' : #(↑t' : Type u) ≤ c
h :
  Eq (α := Set (↑s : Type u)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t)
    (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t')
⊢ t = t'
have inj' : t ⊆ range (ι := (↑s : Type u)) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
Tactic: refine (preimage_eq_preimage' ?_ ?_).1 h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
s : Set α
c : Cardinal.{u}
t : Set α
ht1 : t ⊆ s
ht2 : #(↑t : Type u) ≤ c
t' : Set α
h1t' : t' ⊆ s
h2t' : #(↑t' : Type u) ≤ c
h :
  Eq (α := Set (↑s : Type u)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t)
    (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t')
inj' : t ⊆ range (ι := (↑s : Type u)) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
⊢ t = t'
have inj'₁ : t' ⊆ range (ι := (↑s : Type u)) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
Tactic: refine (preimage_eq_preimage' ?_ ?_).1 h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u_1
inst : Infinite α
s : Set α
h2 : #(↑s : Type u_1) < #α
⊢ #(↑sᶜ : Type u_1) = #α
have refine : #(↑s : Type u_1) + #(↑sᶜ : Type u_1) = #α
Tactic: refine eq_of_add_eq_of_aleph0_le ?_ h2 (aleph0_le_mk α)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u_1
inst : Infinite α
s : Finset α
⊢ #(↑(↑s : Set α)ᶜ : Type u_1) = #α
have h2 : #(↑(↑s : Set α) : Type u_1) < #α
Tactic: apply mk_compl_of_infinite
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u_1
inst : Infinite α
s t : Set α
hs : #(↑s : Type u_1) < #α
ht : #(↑t : Type u_1) < #α
⊢ #(↑sᶜ : Type u_1) = #(↑tᶜ : Type u_1)
have rw : #α = #(↑tᶜ : Type u_1)
Tactic: rw [mk_compl_of_infinite s hs, mk_compl_of_infinite t ht]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u_1
inst : Infinite α
s t : Set α
hs : #(↑s : Type u_1) < #α
ht : #(↑t : Type u_1) < #α
rw : #α = #(↑tᶜ : Type u_1)
⊢ #(↑sᶜ : Type u_1) = #(↑tᶜ : Type u_1)
have rw₁ : #α = #α
Tactic: rw [mk_compl_of_infinite s hs, mk_compl_of_infinite t ht]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
β : Type v
inst : Finite α
s : Set α
t : Set β
h1 : lift.{v, u} #α = lift.{u, v} #β
h2 : lift.{v, u} #(↑s : Type u) = lift.{u, v} #(↑t : Type v)
⊢ lift.{v, u} #(↑sᶜ : Type u) = lift.{u, v} #(↑tᶜ : Type v)
have intro : ∀ (val : Fintype α), lift.{v, u} #(↑sᶜ : Type u) = lift.{u, v} #(↑tᶜ : Type v)
Tactic: cases nonempty_fintype α
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
β : Type v
inst : Finite α
s : Set α
t : Set β
h1 : lift.{v, u} #α = lift.{u, v} #β
h2 : lift.{v, u} #(↑s : Type u) = lift.{u, v} #(↑t : Type v)
val : Fintype α
⊢ lift.{v, u} #(↑sᶜ : Type u) = lift.{u, v} #(↑tᶜ : Type v)
have intro : ∀ (e : α ≃ β), lift.{v, u} #(↑sᶜ : Type u) = lift.{u, v} #(↑tᶜ : Type v)
Tactic: rcases lift_mk_eq'.1 h1 with ⟨e⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (hypothesis)
Goal:
α : Type u
β : Type v
inst : Finite α
s : Set α
t : Set β
h1 : lift.{v, u} #α = lift.{u, v} #β
h2 : lift.{v, u} #(↑s : Type u) = lift.{u, v} #(↑t : Type v)
val : Fintype α
e : α ≃ β
this : Fintype β := Fintype.ofEquiv α e
⊢ lift.{v, u} #(↑sᶜ : Type u) = lift.{u, v} #(↑tᶜ : Type v)
have h1₁ : Fintype.card α = Fintype.card β
Tactic: replace h1 : Fintype.card α = Fintype.card β := (Fintype.ofEquiv_card _).symm
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
β : Type v
inst : Finite α
s : Set α
t : Set β
h2 : lift.{v, u} #(↑s : Type u) = lift.{u, v} #(↑t : Type v)
val : Fintype α
e : α ≃ β
this : Fintype β := Fintype.ofEquiv α e
h1 : Fintype.card α = Fintype.card β
⊢ lift.{v, u} #(↑sᶜ : Type u) = lift.{u, v} #(↑tᶜ : Type v)
have intro : ∀ (s : Finset α) (h2 : lift.{v, u} #(↑(↑s : Set α) : Type u) = lift.{u, v} #(↑t : Type v)),
  lift.{v, u} #(↑(↑s : Set α)ᶜ : Type u) = lift.{u, v} #(↑tᶜ : Type v)
Tactic: lift s to Finset α using s.toFinite
Cleared hypotheses: s, h2