awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
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)
⊢ lift.{v, u} #(↑(↑s : Set α)ᶜ : Type u) = lift.{u, v} #(↑tᶜ : Type v)
have intro : ∀ (t : Finset β) (h2 : lift.{v, u} #(↑(↑s : Set α) : Type u) = lift.{u, v} #(↑(↑t : Set β) : Type v)),
  lift.{v, u} #(↑(↑s : Set α)ᶜ : Type u) = lift.{u, v} #(↑(↑t : Set β)ᶜ : Type v)
Tactic: lift t to Finset β using t.toFinite
Cleared hypotheses: t, h2
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (hypothesis)
Goal:
α : Type u
β : Type v
inst : Finite α
val : Fintype α
e : α ≃ β
this : Fintype β := Fintype.ofEquiv α e
h1 : Fintype.card α = Fintype.card β
s : Finset α
t : Finset β
h2 : lift.{v, u} #(↑(↑s : Set α) : Type u) = lift.{u, v} #(↑(↑t : Set β) : Type v)
⊢ lift.{v, u} #(↑(↑s : Set α)ᶜ : Type u) = lift.{u, v} #(↑(↑t : Set β)ᶜ : Type v)
have h2₁ : s.card = t.card
Tactic: simp only [Finset.coe_sort_coe, mk_fintype, Fintype.card_coe, lift_natCast, Nat.cast_inj] at h2
Cleared hypotheses: h2
-- 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: classical
    lift s to Finset α using s.toFinite
    lift t to Finset β using t.toFinite
    simp only [Finset.coe_sort_coe, mk_fintype, Fintype.card_coe, lift_natCast, Nat.cast_inj] at h2
    simp only [← Finset.coe_compl, Finset.coe_sort_coe, mk_coe_finset, Finset.card_compl,
      lift_natCast, h1, h2]
Cleared hypotheses: s, h2
-- 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 β
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)
have intro₁ : ∀ (s : Finset α) (t : Finset β) (h2 : lift.{v, u} #(↑(↑s : Set α) : Type u) = lift.{u, v} #(↑(↑t : Set β) : Type v)),
  lift.{v, u} #(↑(↑s : Set α)ᶜ : Type u) = lift.{u, v} #(↑(↑t : Set β)ᶜ : Type v)
Tactic: classical
    lift s to Finset α using s.toFinite
    lift t to Finset β using t.toFinite
    simp only [Finset.coe_sort_coe, mk_fintype, Fintype.card_coe, lift_natCast, Nat.cast_inj] at h2
    simp only [← Finset.coe_compl, Finset.coe_sort_coe, mk_coe_finset, Finset.card_compl,
      lift_natCast, h1, h2]
Cleared hypotheses: s, t, h2
-- 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 β
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)
intro₁ :
  ∀ (s : Finset α) (t : Finset β) (h2 : lift.{v, u} #(↑(↑s : Set α) : Type u) = lift.{u, v} #(↑(↑t : Set β) : Type v)),
    lift.{v, u} #(↑(↑s : Set α)ᶜ : Type u) = lift.{u, v} #(↑(↑t : Set β)ᶜ : Type v)
⊢ lift.{v, u} #(↑sᶜ : Type u) = lift.{u, v} #(↑tᶜ : Type v)
have intro₂ : ∀ (s : Finset α) (t : Finset β) (h2 : s.card = t.card),
  lift.{v, u} #(↑(↑s : Set α)ᶜ : Type u) = lift.{u, v} #(↑(↑t : Set β)ᶜ : Type v)
Tactic: classical
    lift s to Finset α using s.toFinite
    lift t to Finset β using t.toFinite
    simp only [Finset.coe_sort_coe, mk_fintype, Fintype.card_coe, lift_natCast, Nat.cast_inj] at h2
    simp only [← Finset.coe_compl, Finset.coe_sort_coe, mk_coe_finset, Finset.card_compl,
      lift_natCast, h1, h2]
Cleared hypotheses: s, t, h2
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α β : Type u
inst : Finite α
s : Set α
t : Set β
h1 : #α = #β
h : #(↑s : Type u) = #(↑t : Type u)
⊢ #(↑sᶜ : Type u) = #(↑tᶜ : Type u)
have rw : lift.{u, u} #(↑sᶜ : Type u) = lift.{u, u} #(↑tᶜ : Type u)
Tactic: rw [← lift_inj.{u, u}]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α β : Type u
inst : Finite α
s : Set α
t : Set β
h1 : #α = #β
h : #(↑s : Type u) = #(↑t : Type u)
⊢ lift.{u, u} #(↑sᶜ : Type u) = lift.{u, u} #(↑tᶜ : Type u)
have h1₁ : lift.{u, u} #α = lift.{u, u} #β
Tactic: apply mk_compl_eq_mk_compl_finite_lift.{u, u}
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α β : Type u
inst : Finite α
s : Set α
t : Set β
h1 : #α = #β
h : #(↑s : Type u) = #(↑t : Type u)
h1₁ : lift.{u, u} #α = lift.{u, u} #β
⊢ lift.{u, u} #(↑sᶜ : Type u) = lift.{u, u} #(↑tᶜ : Type u)
have h2 : lift.{u, u} #(↑s : Type u) = lift.{u, u} #(↑t : Type u)
Tactic: apply mk_compl_eq_mk_compl_finite_lift.{u, u}
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : Embedding.{u_1 + 1, u_2 + 1} (↑s : Type u_1) β
h this :
  Nonempty
    (Equiv.{u_1 + 1, u_2 + 1} (↑sᶜ : Type u_1)
      (↑(range.{u_2, u_1 + 1} (ι := (↑s : Type u_1)) (⇑f : (a : (↑s : Type u_1)) → β))ᶜ : Type u_2))
⊢ ∃ (g : α ≃ β),
    ∀ (x : (↑s : Type u_1)),
      Eq.{u_2 + 1} (α := β) ((g : (a : α) → β) (↑x : α) : β) ((f : (a : (↑s : Type u_1)) → β) x : β)
have obtain : ∀
  (g :
    Equiv.{u_1 + 1, u_2 + 1} (↑sᶜ : Type u_1)
      (↑(range.{u_2, u_1 + 1} (ι := (↑s : Type u_1)) (⇑f : (a : (↑s : Type u_1)) → β))ᶜ : Type u_2)),
  ∃ (g : α ≃ β),
    ∀ (x : (↑s : Type u_1)),
      Eq.{u_2 + 1} (α := β) ((g : (a : α) → β) (↑x : α) : β) ((f : (a : (↑s : Type u_1)) → β) x : β)
Tactic: obtain ⟨g⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : Embedding.{u_1 + 1, u_2 + 1} (↑s : Type u_1) β
h_1 :
  Nonempty
    (Equiv.{u_1 + 1, u_2 + 1} (↑sᶜ : Type u_1)
      (↑(range.{u_2, u_1 + 1} (ι := (↑s : Type u_1)) (⇑f : (a : (↑s : Type u_1)) → β))ᶜ : Type u_2))
g :
  Equiv.{u_1 + 1, u_2 + 1} (↑sᶜ : Type u_1)
    (↑(range.{u_2, u_1 + 1} (ι := (↑s : Type u_1)) (⇑f : (a : (↑s : Type u_1)) → β))ᶜ : Type u_2)
h : α ≃ β :=
  (Set.sumCompl s).symm.trans
    (((ofInjective (⇑f : (a : (↑s : Type u_1)) → β) ⋯).sumCongr g).trans
      (Set.sumCompl (range.{u_2, u_1 + 1} (ι := (↑s : Type u_1)) (⇑f : (a : (↑s : Type u_1)) → β))))
⊢ ∃ (g : α ≃ β),
    ∀ (x : (↑s : Type u_1)),
      Eq.{u_2 + 1} (α := β) ((g : (a : α) → β) (↑x : α) : β) ((f : (a : (↑s : Type u_1)) → β) x : β)
have refine : ∀ (x : (↑s : Type u_1)), Eq.{u_2 + 1} (α := β) ((h : (a : α) → β) (↑x : α) : β) ((f : (a : (↑s : Type u_1)) → β) x : β)
Tactic: refine ⟨h, ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : Embedding.{u_1 + 1, u_2 + 1} (↑s : Type u_1) β
h :
  Nonempty
    (Equiv.{u_1 + 1, u_2 + 1} (↑sᶜ : Type u_1)
      (↑(range.{u_2, u_1 + 1} (ι := (↑s : Type u_1)) (⇑f : (a : (↑s : Type u_1)) → β))ᶜ : Type u_2))
⊢ ∃ (g : α ≃ β),
    ∀ (x : (↑s : Type u_1)),
      Eq.{u_2 + 1} (α := β) ((g : (a : α) → β) (↑x : α) : β) ((f : (a : (↑s : Type u_1)) → β) x : β)
have have : ∀
  (this :
    Nonempty
      (Equiv.{u_1 + 1, u_2 + 1} (↑sᶜ : Type u_1)
        (↑(range.{u_2, u_1 + 1} (ι := (↑s : Type u_1)) (⇑f : (a : (↑s : Type u_1)) → β))ᶜ : Type u_2))),
  ∃ (g : α ≃ β),
    ∀ (x : (↑s : Type u_1)),
      Eq.{u_2 + 1} (α := β) ((g : (a : α) → β) (↑x : α) : β) ((f : (a : (↑s : Type u_1)) → β) x : β)
Tactic: classical
  have := h; obtain ⟨g⟩ := this
  let h : α ≃ β :=
    (Set.sumCompl (s : Set α)).symm.trans
      ((sumCongr (Equiv.ofInjective f f.2) g).trans (Set.sumCompl (range f)))
  refine ⟨h, ?_⟩; rintro ⟨x, hx⟩; simp [h, Set.sumCompl_symm_apply_of_mem, hx]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : Embedding.{u_1 + 1, u_2 + 1} (↑s : Type u_1) β
h :
  Nonempty
    (Equiv.{u_1 + 1, u_2 + 1} (↑sᶜ : Type u_1)
      (↑(range.{u_2, u_1 + 1} (ι := (↑s : Type u_1)) (⇑f : (a : (↑s : Type u_1)) → β))ᶜ : Type u_2))
have have₁ have₂ have₃ :
  ∀
    (this :
      Nonempty
        (Equiv.{u_1 + 1, u_2 + 1} (↑sᶜ : Type u_1)
          (↑(range.{u_2, u_1 + 1} (ι := (↑s : Type u_1)) (⇑f : (a : (↑s : Type u_1)) → β))ᶜ : Type u_2))),
    ∃ (g : α ≃ β),
      ∀ (x : (↑s : Type u_1)),
        Eq.{u_2 + 1} (α := β) ((g : (a : α) → β) (↑x : α) : β) ((f : (a : (↑s : Type u_1)) → β) x : β)
⊢ ∃ (g : α ≃ β),
    ∀ (x : (↑s : Type u_1)),
      Eq.{u_2 + 1} (α := β) ((g : (a : α) → β) (↑x : α) : β) ((f : (a : (↑s : Type u_1)) → β) x : β)
have have₄ : ∀
  (g :
    Equiv.{u_1 + 1, u_2 + 1} (↑sᶜ : Type u_1)
      (↑(range.{u_2, u_1 + 1} (ι := (↑s : Type u_1)) (⇑f : (a : (↑s : Type u_1)) → β))ᶜ : Type u_2)),
  ∃ (g : α ≃ β),
    ∀ (x : (↑s : Type u_1)),
      Eq.{u_2 + 1} (α := β) ((g : (a : α) → β) (↑x : α) : β) ((f : (a : (↑s : Type u_1)) → β) x : β)
Tactic: classical
  have := h; obtain ⟨g⟩ := this
  let h : α ≃ β :=
    (Set.sumCompl (s : Set α)).symm.trans
      ((sumCongr (Equiv.ofInjective f f.2) g).trans (Set.sumCompl (range f)))
  refine ⟨h, ?_⟩; rintro ⟨x, hx⟩; simp [h, Set.sumCompl_symm_apply_of_mem, hx]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : Embedding.{u_1 + 1, u_2 + 1} (↑s : Type u_1) β
h :
  Nonempty
    (Equiv.{u_1 + 1, u_2 + 1} (↑sᶜ : Type u_1)
      (↑(range.{u_2, u_1 + 1} (ι := (↑s : Type u_1)) (⇑f : (a : (↑s : Type u_1)) → β))ᶜ : Type u_2))
have have₁ have₂ have₃ :
  ∀
    (this :
      Nonempty
        (Equiv.{u_1 + 1, u_2 + 1} (↑sᶜ : Type u_1)
          (↑(range.{u_2, u_1 + 1} (ι := (↑s : Type u_1)) (⇑f : (a : (↑s : Type u_1)) → β))ᶜ : Type u_2))),
    ∃ (g : α ≃ β),
      ∀ (x : (↑s : Type u_1)),
        Eq.{u_2 + 1} (α := β) ((g : (a : α) → β) (↑x : α) : β) ((f : (a : (↑s : Type u_1)) → β) x : β)
have₄ have₅ :
  ∀
    (g :
      Equiv.{u_1 + 1, u_2 + 1} (↑sᶜ : Type u_1)
        (↑(range.{u_2, u_1 + 1} (ι := (↑s : Type u_1)) (⇑f : (a : (↑s : Type u_1)) → β))ᶜ : Type u_2)),
    ∃ (g : α ≃ β),
      ∀ (x : (↑s : Type u_1)),
        Eq.{u_2 + 1} (α := β) ((g : (a : α) → β) (↑x : α) : β) ((f : (a : (↑s : Type u_1)) → β) x : β)
⊢ ∃ (g : α ≃ β),
    ∀ (x : (↑s : Type u_1)),
      Eq.{u_2 + 1} (α := β) ((g : (a : α) → β) (↑x : α) : β) ((f : (a : (↑s : Type u_1)) → β) x : β)
have have₆ : ∀
  (g :
    Equiv.{u_1 + 1, u_2 + 1} (↑sᶜ : Type u_1)
      (↑(range.{u_2, u_1 + 1} (ι := (↑s : Type u_1)) (⇑f : (a : (↑s : Type u_1)) → β))ᶜ : Type u_2)),
  let h :=
    (Set.sumCompl s).symm.trans
      (((ofInjective (⇑f : (a : (↑s : Type u_1)) → β) sorry).sumCongr g).trans
        (Set.sumCompl (range.{u_2, u_1 + 1} (ι := (↑s : Type u_1)) (⇑f : (a : (↑s : Type u_1)) → β))));
  ∀ (x : (↑s : Type u_1)),
    Eq.{u_2 + 1} (α := β) ((h : (a : α) → β) (↑x : α) : β) ((f : (a : (↑s : Type u_1)) → β) x : β)
Tactic: classical
  have := h; obtain ⟨g⟩ := this
  let h : α ≃ β :=
    (Set.sumCompl (s : Set α)).symm.trans
      ((sumCongr (Equiv.ofInjective f f.2) g).trans (Set.sumCompl (range f)))
  refine ⟨h, ?_⟩; rintro ⟨x, hx⟩; simp [h, Set.sumCompl_symm_apply_of_mem, hx]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : Embedding.{u_1 + 1, u_2 + 1} (↑s : Type u_1) β
h :
  Nonempty
    (Equiv.{u_1 + 1, u_2 + 1} (↑sᶜ : Type u_1)
      (↑(range.{u_2, u_1 + 1} (ι := (↑s : Type u_1)) (⇑f : (a : (↑s : Type u_1)) → β))ᶜ : Type u_2))
have have₁ have₂ have₃ :
  ∀
    (this :
      Nonempty
        (Equiv.{u_1 + 1, u_2 + 1} (↑sᶜ : Type u_1)
          (↑(range.{u_2, u_1 + 1} (ι := (↑s : Type u_1)) (⇑f : (a : (↑s : Type u_1)) → β))ᶜ : Type u_2))),
    ∃ (g : α ≃ β),
      ∀ (x : (↑s : Type u_1)),
        Eq.{u_2 + 1} (α := β) ((g : (a : α) → β) (↑x : α) : β) ((f : (a : (↑s : Type u_1)) → β) x : β)
have₄ have₅ :
  ∀
    (g :
      Equiv.{u_1 + 1, u_2 + 1} (↑sᶜ : Type u_1)
        (↑(range.{u_2, u_1 + 1} (ι := (↑s : Type u_1)) (⇑f : (a : (↑s : Type u_1)) → β))ᶜ : Type u_2)),
    ∃ (g : α ≃ β),
      ∀ (x : (↑s : Type u_1)),
        Eq.{u_2 + 1} (α := β) ((g : (a : α) → β) (↑x : α) : β) ((f : (a : (↑s : Type u_1)) → β) x : β)
have₆ have₇ :
  ∀
    (g :
      Equiv.{u_1 + 1, u_2 + 1} (↑sᶜ : Type u_1)
        (↑(range.{u_2, u_1 + 1} (ι := (↑s : Type u_1)) (⇑f : (a : (↑s : Type u_1)) → β))ᶜ : Type u_2)),
    let h :=
      (Set.sumCompl s).symm.trans
        (((ofInjective (⇑f : (a : (↑s : Type u_1)) → β) ⋯).sumCongr g).trans
          (Set.sumCompl (range.{u_2, u_1 + 1} (ι := (↑s : Type u_1)) (⇑f : (a : (↑s : Type u_1)) → β))));
    ∀ (x : (↑s : Type u_1)),
      Eq.{u_2 + 1} (α := β) ((h : (a : α) → β) (↑x : α) : β) ((f : (a : (↑s : Type u_1)) → β) x : β)
⊢ ∃ (g : α ≃ β),
    ∀ (x : (↑s : Type u_1)),
      Eq.{u_2 + 1} (α := β) ((g : (a : α) → β) (↑x : α) : β) ((f : (a : (↑s : Type u_1)) → β) x : β)
have have₈ : ∀
  (g :
    Equiv.{u_1 + 1, u_2 + 1} (↑sᶜ : Type u_1)
      (↑(range.{u_2, u_1 + 1} (ι := (↑s : Type u_1)) (⇑f : (a : (↑s : Type u_1)) → β))ᶜ : Type u_2)),
  let h :=
    (Set.sumCompl s).symm.trans
      (((ofInjective (⇑f : (a : (↑s : Type u_1)) → β) sorry).sumCongr g).trans
        (Set.sumCompl (range.{u_2, u_1 + 1} (ι := (↑s : Type u_1)) (⇑f : (a : (↑s : Type u_1)) → β))));
  ∀ (x : α) (hx : x ∈ s),
    Eq.{u_2 + 1} (α := β) ((h : (a : α) → β) (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx) : α) : β)
      ((f : (a : (↑s : Type u_1)) → β) (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx) : β)
Tactic: classical
  have := h; obtain ⟨g⟩ := this
  let h : α ≃ β :=
    (Set.sumCompl (s : Set α)).symm.trans
      ((sumCongr (Equiv.ofInjective f f.2) g).trans (Set.sumCompl (range f)))
  refine ⟨h, ?_⟩; rintro ⟨x, hx⟩; simp [h, Set.sumCompl_symm_apply_of_mem, hx]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
β : Type v
inst : Finite α
s : Set α
f : Embedding.{u + 1, v + 1} (↑s : Type u) β
h : Nonempty (α ≃ β)
⊢ ∃ (g : α ≃ β),
    ∀ (x : (↑s : Type u)), Eq.{v + 1} (α := β) ((g : (a : α) → β) (↑x : α) : β) ((f : (a : (↑s : Type u)) → β) x : β)
have apply : Nonempty
  (Equiv.{u + 1, v + 1} (↑sᶜ : Type u)
    (↑(range.{v, u + 1} (ι := (↑s : Type u)) (⇑f : (a : (↑s : Type u)) → β))ᶜ : Type v))
Tactic: apply extend_function.{u, v} f
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (hypothesis)
Goal:
α : Type u
β : Type v
inst : Finite α
s : Set α
f : Embedding.{u + 1, v + 1} (↑s : Type u) β
h : Nonempty (α ≃ β)
⊢ Nonempty
    (Equiv.{u + 1, v + 1} (↑sᶜ : Type u)
      (↑(range.{v, u + 1} (ι := (↑s : Type u)) (⇑f : (a : (↑s : Type u)) → β))ᶜ : Type v))
have h₁ : lift.{v, u} #α = lift.{u, v} #β
Tactic: rw [← lift_mk_eq'] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
β : Type v
inst : Finite α
s : Set α
f : Embedding.{u + 1, v + 1} (↑s : Type u) β
h : lift.{v, u} #α = lift.{u, v} #β
⊢ Nonempty
    (Equiv.{u + 1, v + 1} (↑sᶜ : Type u)
      (↑(range.{v, u + 1} (ι := (↑s : Type u)) (⇑f : (a : (↑s : Type u)) → β))ᶜ : Type v))
have rw : lift.{v, u} #(↑s : Type u) =
  lift.{u, v} #(↑(range.{v, u + 1} (ι := (↑s : Type u)) (⇑f : (a : (↑s : Type u)) → β)) : Type v)
Tactic: rw [← lift_mk_eq', mk_compl_eq_mk_compl_finite_lift h]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u
β : Type v
inst : Finite α
s : Set α
f : Embedding.{u + 1, v + 1} (↑s : Type u) β
h : lift.{v, u} #α = lift.{u, v} #β
⊢ lift.{v, u} #(↑s : Type u) =
    lift.{u, v} #(↑(range.{v, u + 1} (ι := (↑s : Type u)) (⇑f : (a : (↑s : Type u)) → β)) : Type v)
have rw : Injective.{u + 1, v + 1} (α := (↑s : Type u)) (β := β) (⇑f : (a : (↑s : Type u)) → β)
Tactic: rw [mk_range_eq_of_injective]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : Embedding.{u_1 + 1, u_2 + 1} (↑s : Type u_1) β
hs : #(↑s : Type u_1) < #α
h : Nonempty (α ≃ β)
⊢ ∃ (g : α ≃ β),
    ∀ (x : (↑s : Type u_1)),
      Eq.{u_2 + 1} (α := β) ((g : (a : α) → β) (↑x : α) : β) ((f : (a : (↑s : Type u_1)) → β) x : β)
have inl : ∀ (val : Fintype α),
  ∃ (g : α ≃ β),
    ∀ (x : (↑s : Type u_1)),
      Eq.{u_2 + 1} (α := β) ((g : (a : α) → β) (↑x : α) : β) ((f : (a : (↑s : Type u_1)) → β) x : β)
Tactic: cases fintypeOrInfinite α
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : Embedding.{u_1 + 1, u_2 + 1} (↑s : Type u_1) β
hs : #(↑s : Type u_1) < #α
h : Nonempty (α ≃ β)
inl :
  ∀ (val : Fintype α),
    ∃ (g : α ≃ β),
      ∀ (x : (↑s : Type u_1)),
        Eq.{u_2 + 1} (α := β) ((g : (a : α) → β) (↑x : α) : β) ((f : (a : (↑s : Type u_1)) → β) x : β)
⊢ ∃ (g : α ≃ β),
    ∀ (x : (↑s : Type u_1)),
      Eq.{u_2 + 1} (α := β) ((g : (a : α) → β) (↑x : α) : β) ((f : (a : (↑s : Type u_1)) → β) x : β)
have inr : Infinite α →
  ∃ (g : α ≃ β),
    ∀ (x : (↑s : Type u_1)),
      Eq.{u_2 + 1} (α := β) ((g : (a : α) → β) (↑x : α) : β) ((f : (a : (↑s : Type u_1)) → β) x : β)
Tactic: cases fintypeOrInfinite α
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : Embedding.{u_1 + 1, u_2 + 1} (↑s : Type u_1) β
hs : #(↑s : Type u_1) < #α
h : Nonempty (α ≃ β)
val : Infinite α
⊢ ∃ (g : α ≃ β),
    ∀ (x : (↑s : Type u_1)),
      Eq.{u_2 + 1} (α := β) ((g : (a : α) → β) (↑x : α) : β) ((f : (a : (↑s : Type u_1)) → β) x : β)
have inr : Nonempty
  (Equiv.{u_1 + 1, u_2 + 1} (↑sᶜ : Type u_1)
    (↑(range.{u_2, u_1 + 1} (ι := (↑s : Type u_1)) (⇑f : (a : (↑s : Type u_1)) → β))ᶜ : Type u_2))
Tactic: apply extend_function f
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : Embedding.{u_1 + 1, u_2 + 1} (↑s : Type u_1) β
hs : #(↑s : Type u_1) < #α
h : Nonempty (α ≃ β)
val : Infinite α
⊢ Nonempty
    (Equiv.{u_1 + 1, u_2 + 1} (↑sᶜ : Type u_1)
      (↑(range.{u_2, u_1 + 1} (ι := (↑s : Type u_1)) (⇑f : (a : (↑s : Type u_1)) → β))ᶜ : Type u_2))
have inr : ∀ (g : α ≃ β),
  Nonempty
    (Equiv.{u_1 + 1, u_2 + 1} (↑sᶜ : Type u_1)
      (↑(range.{u_2, u_1 + 1} (ι := (↑s : Type u_1)) (⇑f : (a : (↑s : Type u_1)) → β))ᶜ : Type u_2))
Tactic: obtain ⟨g⟩ := id h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : Embedding.{u_1 + 1, u_2 + 1} (↑s : Type u_1) β
hs : #(↑s : Type u_1) < #α
h : Nonempty (α ≃ β)
val : Infinite α
g : α ≃ β
⊢ Nonempty
    (Equiv.{u_1 + 1, u_2 + 1} (↑sᶜ : Type u_1)
      (↑(range.{u_2, u_1 + 1} (ι := (↑s : Type u_1)) (⇑f : (a : (↑s : Type u_1)) → β))ᶜ : Type u_2))
have this : Infinite β
Tactic: haveI := Infinite.of_injective _ g.injective
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : Embedding.{u_1 + 1, u_2 + 1} (↑s : Type u_1) β
hs : #(↑s : Type u_1) < #α
h : Nonempty (α ≃ β)
val : Infinite α
g : α ≃ β
this : Infinite β
⊢ Nonempty
    (Equiv.{u_1 + 1, u_2 + 1} (↑sᶜ : Type u_1)
      (↑(range.{u_2, u_1 + 1} (ι := (↑s : Type u_1)) (⇑f : (a : (↑s : Type u_1)) → β))ᶜ : Type u_2))
have inr : ∀ (h : lift.{u_2, u_1} #α = lift.{u_1, u_2} #β),
  Infinite α →
    ∀ (g : α ≃ β) (this : Infinite β),
      lift.{u_2, u_1} #(↑sᶜ : Type u_1) =
        lift.{u_1, u_2} #(↑(range.{u_2, u_1 + 1} (ι := (↑s : Type u_1)) (⇑f : (a : (↑s : Type u_1)) → β))ᶜ : Type u_2)
Tactic: rw [← lift_mk_eq'] at h ⊢
Cleared hypotheses: h, val, g, this
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : Embedding.{u_1 + 1, u_2 + 1} (↑s : Type u_1) β
hs : #(↑s : Type u_1) < #α
h : lift.{u_2, u_1} #α = lift.{u_1, u_2} #β
val : Infinite α
g : α ≃ β
this : Infinite β
⊢ lift.{u_2, u_1} #(↑sᶜ : Type u_1) =
    lift.{u_1, u_2} #(↑(range.{u_2, u_1 + 1} (ι := (↑s : Type u_1)) (⇑f : (a : (↑s : Type u_1)) → β))ᶜ : Type u_2)
have inr : #(↑(range.{u_2, u_1 + 1} (ι := (↑s : Type u_1)) (⇑f : (a : (↑s : Type u_1)) → β)) : Type u_2) < #β
Tactic: rwa [mk_compl_of_infinite s hs, mk_compl_of_infinite]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : Embedding.{u_1 + 1, u_2 + 1} (↑s : Type u_1) β
hs : #(↑s : Type u_1) < #α
h : lift.{u_2, u_1} #α = lift.{u_1, u_2} #β
val : Infinite α
g : α ≃ β
this : Infinite β
⊢ #(↑(range.{u_2, u_1 + 1} (ι := (↑s : Type u_1)) (⇑f : (a : (↑s : Type u_1)) → β)) : Type u_2) < #β
have inr : lift.{u_1, u_2} #(↑(range.{u_2, u_1 + 1} (ι := (↑s : Type u_1)) (⇑f : (a : (↑s : Type u_1)) → β)) : Type u_2) <
  lift.{u_1, u_2} #β
Tactic: rwa [← lift_lt, mk_range_eq_of_injective f.injective, ← h, lift_lt]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : Embedding.{u_1 + 1, u_2 + 1} (↑s : Type u_1) β
hs : #(↑s : Type u_1) < #α
h : lift.{u_2, u_1} #α = lift.{u_1, u_2} #β
val : Infinite α
g : α ≃ β
this : Infinite β
inr :
  lift.{u_1, u_2} #(↑(range.{u_2, u_1 + 1} (ι := (↑s : Type u_1)) (⇑f : (a : (↑s : Type u_1)) → β)) : Type u_2) <
    lift.{u_1, u_2} #β
⊢ #(↑(range.{u_2, u_1 + 1} (ι := (↑s : Type u_1)) (⇑f : (a : (↑s : Type u_1)) → β)) : Type u_2) < #β
have inr₁ : lift.{u_2, u_1} #(↑s : Type u_1) < lift.{u_1, u_2} #β
Tactic: rwa [← lift_lt, mk_range_eq_of_injective f.injective, ← h, lift_lt]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Arithmetic (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : Embedding.{u_1 + 1, u_2 + 1} (↑s : Type u_1) β
hs : #(↑s : Type u_1) < #α
h : lift.{u_2, u_1} #α = lift.{u_1, u_2} #β
val : Infinite α
g : α ≃ β
this : Infinite β
inr :
  lift.{u_1, u_2} #(↑(range.{u_2, u_1 + 1} (ι := (↑s : Type u_1)) (⇑f : (a : (↑s : Type u_1)) → β)) : Type u_2) <
    lift.{u_1, u_2} #β
inr₁ : lift.{u_2, u_1} #(↑s : Type u_1) < lift.{u_1, u_2} #β
⊢ #(↑(range.{u_2, u_1 + 1} (ι := (↑s : Type u_1)) (⇑f : (a : (↑s : Type u_1)) → β)) : Type u_2) < #β
have inr₂ : lift.{u_2, u_1} #(↑s : Type u_1) < lift.{u_2, u_1} #α
Tactic: rwa [← lift_lt, mk_range_eq_of_injective f.injective, ← h, lift_lt]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
s : Set α
⊢ #(↑(ULift.down ⁻¹' s) : Type (max u v)) = lift.{v, u} #(↑s : Type u)
have rw : Nonempty ((↑(ULift.down ⁻¹' s) : Type (max u v)) ≃ ULift.{v, u} (↑s : Type u))
Tactic: rw [← mk_uLift, Cardinal.eq]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type u
s : Set α
⊢ Nonempty ((↑(ULift.down ⁻¹' s) : Type (max u v)) ≃ ULift.{v, u} (↑s : Type u))
have val : (↑(ULift.down ⁻¹' s) : Type (max u v)) ≃ ULift.{v, u} (↑s : Type u)
Tactic: constructor
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (hypothesis)
Goal:
α : Type u
s : Set α
f : (↑(ULift.down ⁻¹' s) : Type (max u v)) → ULift.{v, u} (↑s : Type u) :=
  fun (x : (↑(ULift.down ⁻¹' s) : Type (max u v))) ↦ { down := s.restrictPreimage ULift.down x }
⊢ (↑(ULift.down ⁻¹' s) : Type (max u v)) ≃ ULift.{v, u} (↑s : Type u)
have this : Bijective f
Tactic: have : Function.Bijective f :=
    ULift.up_bijective.comp (restrictPreimage_bijective _ (ULift.down_bijective))
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type (max u v)
inst : Small.{v, max u v} α
⊢ lift.{u, v} #(Shrink.{v, max u v} α) = #α
have rw : lift.{max v u, v} #(Shrink.{v, max u v} α) = #α
Tactic: rw [← lift_umax, lift_mk_shrink.{max u v, v, 0} α, ← lift_umax, lift_id]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Basic (goal)
Goal:
α : Type (max u v)
inst : Small.{v, max u v} α
rw : lift.{max v u, v} #(Shrink.{v, max u v} α) = #α
⊢ lift.{u, v} #(Shrink.{v, max u v} α) = #α
have rw₁ : lift.{v, max u v} #α = #α
Tactic: rw [← lift_umax, lift_mk_shrink.{max u v, v, 0} α, ← lift_umax, lift_id]