awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 α)
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) : β)
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)
⊢ 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

Tactic:
use g ⟨x, h⟩

Premises used: Subtype.mk, DFunLike.coe
-- 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 α)
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) : β)
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)
⊢ 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)

Tactic:
rw [dif_pos this]

Premises used: dif_pos
-- 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 α)
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) : β)
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
⊢ 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:
congr
-- 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 α)
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) : β)
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
⊢ (↑(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:
suffices Classical.choose this = ⟨x, h⟩ from congr_arg Subtype.val this
-- 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 α)
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) : β)
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)
⊢ 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:
apply g.2

Premises used: Function.Embedding.inj'
-- 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 α)
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) : β)
⊢ 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:
Classical.choose_spec this

Premises used: Classical.choose_spec
-- 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 α)
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) : β)
⊢ 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:
exact Classical.choose_spec this

Premises used: Classical.choose_spec
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
c : Cardinal.{u}
trans : #{ t : Set α // #(↑t : Type u) ≤ c } ≤ #{ t : Set (ULift.{u, 0} ℕ ⊕ α) // #(↑t : Type u) ≤ c }
trans₁ : #{ t : Set (ULift.{u, 0} ℕ ⊕ α) // #(↑t : Type u) ≤ c } ≤ max #α ℵ₀ ^ c
⊢ #{ t : Set α // #(↑t : Type u) ≤ c } ≤ max #α ℵ₀ ^ c

Tactic:
trans #{ t : Set ((ULift.{u} ℕ) ⊕ α) // #t ≤ c }
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
c : Cardinal.{u}
⊢ #{ t : Set α // #(↑t : Type u) ≤ c } ≤ #{ t : Set (ULift.{u, 0} ℕ ⊕ α) // #(↑t : Type u) ≤ c }

Tactic:
⟨Embedding.subtypeMap ?_ ?_⟩

Premises used: Nonempty.intro, Function.Embedding.subtypeMap
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
c : Cardinal.{u}
refine_1 : Set α ↪ Set (ULift.{u, 0} ℕ ⊕ α)
refine_2 :
  ∀ ⦃x : Set α⦄,
    #(↑x : Type u) ≤ c →
      #(↑((Embedding.image { toFun := Sum.inr, inj' := ⋯ : α ↪ ULift.{u, 0} ℕ ⊕ α } :
                  (a : Set α) → Set (ULift.{u, 0} ℕ ⊕ α))
                x) :
            Type u) ≤
        c
⊢ #{ t : Set α // #(↑t : Type u) ≤ c } ≤ #{ t : Set (ULift.{u, 0} ℕ ⊕ α) // #(↑t : Type u) ≤ c }

Tactic:
refine ⟨Embedding.subtypeMap ?_ ?_⟩
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
c : Cardinal.{u}
refine_1 : α ↪ ULift.{u, 0} ℕ ⊕ α
⊢ Set α ↪ Set (ULift.{u, 0} ℕ ⊕ α)

Tactic:
apply Embedding.image

Premises used: Function.Embedding.image
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
c : Cardinal.{u}
inj' : Injective.{u + 1, u + 1} (α := α) (β := ULift.{u, 0} ℕ ⊕ α) Sum.inr
⊢ α ↪ ULift.{u, 0} ℕ ⊕ α

Tactic:
use Sum.inr

Premises used: Sum.inr
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
c : Cardinal.{u}
⊢ Injective.{u + 1, u + 1} (α := α) (β := ULift.{u, 0} ℕ ⊕ α) Sum.inr

Tactic:
apply Sum.inr.inj

Premises used: Sum.inr.inj
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
c : Cardinal.{u}
s : Set α
hs : #(↑s : Type u) ≤ c
⊢ #(↑((Embedding.image { toFun := Sum.inr, inj' := ⋯ : α ↪ ULift.{u, 0} ℕ ⊕ α } :
              (a : Set α) → Set (ULift.{u, 0} ℕ ⊕ α))
            s) :
        Type u) ≤
    c

Tactic:
mk_image_le.trans hs

Premises used: setOf, Cardinal.mk_image_le, Set.image, LE.le.trans
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
c : Cardinal.{u}
s : Set α
hs : #(↑s : Type u) ≤ c
⊢ #(↑((Embedding.image { toFun := Sum.inr, inj' := ⋯ : α ↪ ULift.{u, 0} ℕ ⊕ α } :
              (a : Set α) → Set (ULift.{u, 0} ℕ ⊕ α))
            s) :
        Type u) ≤
    c

Tactic:
exact mk_image_le.trans hs

Premises used: Cardinal.mk_image_le, LE.le.trans
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
c : Cardinal.{u}
apply : #(ULift.{u, 0} ℕ ⊕ α) ^ c ≤ max #α ℵ₀ ^ c
⊢ #{ t : Set (ULift.{u, 0} ℕ ⊕ α) // #(↑t : Type u) ≤ c } ≤ max #α ℵ₀ ^ c

Tactic:
apply (mk_bounded_set_le_of_infinite ((ULift.{u} ℕ) ⊕ α) c).trans
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
c : Cardinal.{u}
rw : #(ULift.{u, 0} ℕ ⊕ α) ^ c ≤ #(ULift.{u, 0} ℕ ⊕ α) ^ c
rw₁ : ℵ₀ ≤ ℵ₀
⊢ #(ULift.{u, 0} ℕ ⊕ α) ^ c ≤ max #α ℵ₀ ^ c

Tactic:
rw [max_comm, ← add_eq_max]

Premises used: Cardinal.add_eq_max, max_comm
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
c : Cardinal.{u}
⊢ #(ULift.{u, 0} ℕ ⊕ α) ^ c ≤ #(ULift.{u, 0} ℕ ⊕ α) ^ c

Tactic:
rfl
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
c : Cardinal.{u}
⊢ ℵ₀ ≤ ℵ₀

Tactic:
rfl
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
s : Set α
c : Cardinal.{u}
⊢ #{ t : Set α // t ⊆ s ∧ #(↑t : Type u) ≤ c } ≤ max #(↑s : Type u) ℵ₀ ^ c

Tactic:
le_trans ?_ (mk_bounded_set_le s c)

Premises used: Cardinal.mk_bounded_set_le, Set.Elem, le_trans
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
s : Set α
c : Cardinal.{u}
refine : #{ t : Set α // t ⊆ s ∧ #(↑t : Type u) ≤ c } ≤ #{ t : Set (↑s : Type u) // #(↑t : Type u) ≤ c }
⊢ #{ t : Set α // t ⊆ s ∧ #(↑t : Type u) ≤ c } ≤ max #(↑s : Type u) ℵ₀ ^ c

Tactic:
refine le_trans ?_ (mk_bounded_set_le s c)

Premises used: Cardinal.mk_bounded_set_le, Set.Elem, le_trans
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
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 }

Tactic:
⟨Embedding.codRestrict _ ?_ ?_⟩

Premises used: Function.Embedding.codRestrict, Nonempty.intro
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
s : Set α
c : Cardinal.{u}
refine_1 : { t : Set α // t ⊆ s ∧ #(↑t : Type u) ≤ c } ↪ Set (↑s : Type u)
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)) ⋯ c)
      (({
              toFun := fun (t : { t : Set α // t ⊆ s ∧ #(↑t : Type u) ≤ c }) ↦
                Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' (↑t : Set α),
              inj' := ⋯ } :
            (a : { t : Set α // t ⊆ s ∧ #(↑t : Type u) ≤ c }) → Set (↑s : Type u))
          a :
        Set (↑s : Type u))
⊢ #{ t : Set α // t ⊆ s ∧ #(↑t : Type u) ≤ c } ≤ #{ t : Set (↑s : Type u) // #(↑t : Type u) ≤ c }

Tactic:
refine ⟨Embedding.codRestrict _ ?_ ?_⟩
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
s : Set α
c : Cardinal.{u}
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 α)
⊢ { t : Set α // t ⊆ s ∧ #(↑t : Type u) ≤ c } ↪ Set (↑s : Type u)

Tactic:
use fun t => (↑) ⁻¹' t.1

Premises used: Set.preimage
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
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' ⋯))
inj' :
  (↑(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 α)
⊢ 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' ⋯)

Tactic:
apply Subtype.ext

Premises used: Subtype.ext
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
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' ⋯))
inj' : t = 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 α)

Tactic:
dsimp only at h ⊢
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
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'

Tactic:
(preimage_eq_preimage' ?_ ?_).1 h

Premises used: Set.preimage_eq_preimage', Iff.mp
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
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))
inj'₁ : t' ⊆ range (ι := (↑s : Type u)) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
⊢ t = t'

Tactic:
refine (preimage_eq_preimage' ?_ ?_).1 h

Premises used: Set.preimage_eq_preimage', Iff.mp
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
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 ⊆ s
⊢ t ⊆ range (ι := (↑s : Type u)) (Subtype.val (p := fun (x : α) ↦ x ∈ s))

Tactic:
rw [Subtype.range_coe]

Premises used: Subtype.range_coe
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
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' ⊆ s
⊢ t' ⊆ range (ι := (↑s : Type u)) (Subtype.val (p := fun (x : α) ↦ x ∈ s))

Tactic:
rw [Subtype.range_coe]

Premises used: Subtype.range_coe
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
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 ⊆ s

Tactic:
assumption
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
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' ⊆ s

Tactic:
assumption
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
s : Set α
c : Cardinal.{u}
t : Set α
left : t ⊆ s
h2t : #(↑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)) ⋯ c)
    (({
            toFun := fun (t : { t : Set α // t ⊆ s ∧ #(↑t : Type u) ≤ c }) ↦
              Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' (↑t : Set α),
            inj' := ⋯ } :
          (a : { t : Set α // t ⊆ s ∧ #(↑t : Type u) ≤ c }) → Set (↑s : Type u))
        (Subtype.mk (p := fun (t : Set α) ↦ t ⊆ s ∧ #(↑t : Type u) ≤ c) t ⋯) :
      Set (↑s : Type u))

Tactic:
(mk_preimage_of_injective _ _ Subtype.val_injective).trans h2t

Premises used: Set.Mem, Subtype.val_injective, setOf, Set.preimage, LE.le.trans, Cardinal.mk_preimage_of_injective
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
s : Set α
c : Cardinal.{u}
t : Set α
left : t ⊆ s
h2t : #(↑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)) ⋯ c)
    (({
            toFun := fun (t : { t : Set α // t ⊆ s ∧ #(↑t : Type u) ≤ c }) ↦
              Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' (↑t : Set α),
            inj' := ⋯ } :
          (a : { t : Set α // t ⊆ s ∧ #(↑t : Type u) ≤ c }) → Set (↑s : Type u))
        (Subtype.mk (p := fun (t : Set α) ↦ t ⊆ s ∧ #(↑t : Type u) ≤ c) t ⋯) :
      Set (↑s : Type u))

Tactic:
exact (mk_preimage_of_injective _ _ Subtype.val_injective).trans h2t

Premises used: Subtype.val_injective, LE.le.trans, Cardinal.mk_preimage_of_injective
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u_1
inst : Infinite α
s : Set α
h2 : #(↑s : Type u_1) < #α
⊢ #(↑sᶜ : Type u_1) = #α

Tactic:
eq_of_add_eq_of_aleph0_le ?_ h2 (aleph0_le_mk α)

Premises used: Cardinal.eq_of_add_eq_of_aleph0_le, Cardinal.aleph0_le_mk
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u_1
inst : Infinite α
s : Set α
h2 : #(↑s : Type u_1) < #α
refine : #(↑s : Type u_1) + #(↑sᶜ : Type u_1) = #α
⊢ #(↑sᶜ : Type u_1) = #α

Tactic:
refine eq_of_add_eq_of_aleph0_le ?_ h2 (aleph0_le_mk α)

Premises used: Cardinal.eq_of_add_eq_of_aleph0_le, Cardinal.aleph0_le_mk
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u_1
inst : Infinite α
s : Set α
h2 : #(↑s : Type u_1) < #α
⊢ #(↑s : Type u_1) + #(↑sᶜ : Type u_1) = #α

Tactic:
mk_sum_compl s

Premises used: Cardinal.mk_sum_compl
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u_1
inst : Infinite α
s : Set α
h2 : #(↑s : Type u_1) < #α
⊢ #(↑s : Type u_1) + #(↑sᶜ : Type u_1) = #α

Tactic:
exact mk_sum_compl s

Premises used: Cardinal.mk_sum_compl
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u_1
inst : Infinite α
s : Finset α
h2 : #(↑(↑s : Set α) : Type u_1) < #α
⊢ #(↑(↑s : Set α)ᶜ : Type u_1) = #α

Tactic:
apply mk_compl_of_infinite

Premises used: Cardinal.mk_compl_of_infinite
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u_1
inst : Infinite α
s : Finset α
⊢ #(↑(↑s : Set α) : Type u_1) < #α

Tactic:
(finset_card_lt_aleph0 s).trans_le (aleph0_le_mk α)

Premises used: LT.lt.trans_le, Cardinal.finset_card_lt_aleph0, Cardinal.aleph0_le_mk
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u_1
inst : Infinite α
s : Finset α
⊢ #(↑(↑s : Set α) : Type u_1) < #α

Tactic:
exact (finset_card_lt_aleph0 s).trans_le (aleph0_le_mk α)

Premises used: LT.lt.trans_le, Cardinal.finset_card_lt_aleph0, Cardinal.aleph0_le_mk
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u_1
inst : Infinite α
s t : Set α
hs : #(↑s : Type u_1) < #α
ht : #(↑t : Type u_1) < #α
rw : #α = #(↑tᶜ : Type u_1)
rw₁ rw₂ : #α = #α
⊢ #(↑sᶜ : Type u_1) = #(↑tᶜ : Type u_1)

Tactic:
rw [mk_compl_of_infinite s hs, mk_compl_of_infinite t ht]

Premises used: Cardinal.mk_compl_of_infinite
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
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)
intro : ∀ (val : Fintype α), lift.{v, u} #(↑sᶜ : Type u) = lift.{u, v} #(↑tᶜ : Type v)
⊢ lift.{v, u} #(↑sᶜ : Type u) = lift.{u, v} #(↑tᶜ : Type v)

Tactic:
cases nonempty_fintype α

Premises used: nonempty_fintype
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
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 α
intro : ∀ (e : α ≃ β), lift.{v, u} #(↑sᶜ : Type u) = lift.{u, v} #(↑tᶜ : Type v)
⊢ lift.{v, u} #(↑sᶜ : Type u) = lift.{u, v} #(↑tᶜ : Type v)

Tactic:
rcases lift_mk_eq'.1 h1 with ⟨e⟩

Premises used: Cardinal.lift_mk_eq', Iff.mp
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
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
⊢ Fintype.card α = Fintype.card β

Tactic:
replace h1 : Fintype.card α = Fintype.card β := (Fintype.ofEquiv_card _).symm
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
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 β
⊢ s.Finite

Tactic:
s.toFinite

Premises used: Set.toFinite
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
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 β
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)
⊢ lift.{v, u} #(↑sᶜ : Type u) = lift.{u, v} #(↑tᶜ : Type v)

Tactic:
lift s to Finset α using s.toFinite

Premises used: Finset, Set.toFinite
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
β : Type v
inst : Finite α
t : Set β
val : Fintype α
e : α ≃ β
this : Fintype β := Fintype.ofEquiv α e
h1 : Fintype.card α = Fintype.card β
s : Finset α
h2 : lift.{v, u} #(↑(↑s : Set α) : Type u) = lift.{u, v} #(↑t : Type v)
⊢ t.Finite

Tactic:
t.toFinite

Premises used: Set.toFinite