awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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)
⊢ lift.{v, u} #(↑(↑s : Set α)ᶜ : Type u) = lift.{u, v} #(↑tᶜ : Type v)

Tactic:
lift t to Finset β using t.toFinite

Premises used: Finset, Set.toFinite
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
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)
⊢ s.card = t.card

Tactic:
simp only [Finset.coe_sort_coe, mk_fintype, Fintype.card_coe, lift_natCast, Nat.cast_inj] at h2

Premises used: Finset.coe_sort_coe, Nat.cast_inj, Cardinal.mk_fintype, Cardinal.lift_natCast, Fintype.card_coe
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
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 : s.card = t.card
⊢ lift.{v, u} #(↑(↑s : Set α)ᶜ : Type u) = lift.{u, v} #(↑(↑t : Set β)ᶜ : Type v)

Tactic:
simp only [← Finset.coe_compl, Finset.coe_sort_coe, mk_coe_finset, Finset.card_compl,
      lift_natCast, h1, h2]

Premises used: Finset.coe_sort_coe, Finset.card_compl, Cardinal.mk_coe_finset, Finset.coe_compl, Cardinal.lift_natCast
-- 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)
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)
intro₂ :
  ∀ (s : Finset α) (t : Finset β) (h2 : s.card = t.card),
    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)

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]

Premises used: Finset.coe_sort_coe, Finset, Finset.card_compl, Cardinal.mk_coe_finset, Nat.cast_inj, Finset.coe_compl, Cardinal.mk_fintype, Set.toFinite, Cardinal.lift_natCast, Fintype.card_coe
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α β : Type u
inst : Finite α
s : Set α
t : Set β
h1 : #α = #β
h : #(↑s : Type u) = #(↑t : Type u)
rw : lift.{u, u} #(↑sᶜ : Type u) = lift.{u, u} #(↑tᶜ : Type u)
⊢ #(↑sᶜ : Type u) = #(↑tᶜ : Type u)

Tactic:
rw [← lift_inj.{u, u}]
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α β : Type u
inst : Finite α
s : Set α
t : Set β
h1 : #α = #β
h : #(↑s : Type u) = #(↑t : Type u)
h1₁ : lift.{u, u} #α = lift.{u, u} #β
h2 : lift.{u, u} #(↑s : Type u) = lift.{u, u} #(↑t : Type u)
⊢ lift.{u, u} #(↑sᶜ : Type u) = lift.{u, u} #(↑tᶜ : Type u)

Tactic:
apply mk_compl_eq_mk_compl_finite_lift.{u, u}
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α β : Type u
inst : Finite α
s : Set α
t : Set β
h1 : #α = #β
h : #(↑s : Type u) = #(↑t : Type u)
h1₁ h1₂ h1₃ h1₄ : #α = #β
⊢ lift.{u, u} #α = lift.{u, u} #β

Tactic:
rwa [lift_inj]

Premises used: Cardinal.lift_inj
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α β : Type u
inst : Finite α
s : Set α
t : Set β
h1 : #α = #β
h h2 h2₁ h2₂ h2₃ : #(↑s : Type u) = #(↑t : Type u)
⊢ lift.{u, u} #(↑s : Type u) = lift.{u, u} #(↑t : Type u)

Tactic:
rwa [lift_inj]

Premises used: Cardinal.lift_inj
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
inst : Finite α
s t : Set α
h : #(↑s : Type u) = #(↑t : Type u)
⊢ #(↑sᶜ : Type u) = #(↑tᶜ : Type u)

Tactic:
mk_compl_eq_mk_compl_finite.{u} rfl h

Premises used: Cardinal.mk_compl_eq_mk_compl_finite, rfl
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
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))
⊢ 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:
have := h
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
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))
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 : β)
⊢ ∃ (g : α ≃ β),
    ∀ (x : (↑s : Type u_1)),
      Eq.{u_2 + 1} (α := β) ((g : (a : α) → β) (↑x : α) : β) ((f : (a : (↑s : Type u_1)) → β) x : β)

Tactic:
obtain ⟨g⟩ := this
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
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 : β)

Tactic:
⟨h, ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
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)) → β))))
refine :
  ∀ (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 : β)

Tactic:
refine ⟨h, ?_⟩
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
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)) → β))))
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:
simp [h, Set.sumCompl_symm_apply_of_mem, hx]

Premises used: Equiv.Set.sumCompl_symm_apply_of_mem
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
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 : β)
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 : α) (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) : β)
⊢ ∃ (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]

Premises used: Equiv.Set.sumCompl_symm_apply_of_mem
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
β : Type v
inst : Finite α
s : Set α
f : Embedding.{u + 1, v + 1} (↑s : Type u) β
h : Nonempty (α ≃ β)
apply :
  Nonempty
    (Equiv.{u + 1, v + 1} (↑sᶜ : Type u)
      (↑(range.{v, u + 1} (ι := (↑s : Type u)) (⇑f : (a : (↑s : Type u)) → β))ᶜ : Type v))
⊢ ∃ (g : α ≃ β),
    ∀ (x : (↑s : Type u)), Eq.{v + 1} (α := β) ((g : (a : α) → β) (↑x : α) : β) ((f : (a : (↑s : Type u)) → β) x : β)

Tactic:
apply extend_function.{u, v} f
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
Goal:
α : Type u
β : Type v
inst : Finite α
s : Set α
f : Embedding.{u + 1, v + 1} (↑s : Type u) β
h : Nonempty (α ≃ β)
⊢ lift.{v, u} #α = lift.{u, v} #β

Tactic:
rw [← lift_mk_eq'] at h

Premises used: Cardinal.lift_mk_eq'
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
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} #β
rw :
  lift.{v, u} #(↑s : Type u) =
    lift.{u, v} #(↑(range.{v, u + 1} (ι := (↑s : Type u)) (⇑f : (a : (↑s : Type u)) → β)) : Type v)
⊢ Nonempty
    (Equiv.{u + 1, v + 1} (↑sᶜ : Type u)
      (↑(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]

Premises used: Cardinal.lift_mk_eq', Cardinal.mk_compl_eq_mk_compl_finite_lift
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
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} #β
rw : Injective.{u + 1, v + 1} (α := (↑s : Type u)) (β := β) (⇑f : (a : (↑s : Type u)) → β)
⊢ 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 [mk_range_eq_of_injective]

Premises used: Cardinal.mk_range_eq_of_injective
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
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} #β
⊢ Injective.{u + 1, v + 1} (α := (↑s : Type u)) (β := β) (⇑f : (a : (↑s : Type u)) → β)

Tactic:
f.2

Premises used: Function.Embedding.inj'
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
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} #β
⊢ Injective.{u + 1, v + 1} (α := (↑s : Type u)) (β := β) (⇑f : (a : (↑s : Type u)) → β)

Tactic:
exact f.2

Premises used: Function.Embedding.inj'
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
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 : β)
inr :
  Infinite α →
    ∃ (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 : β)

Tactic:
cases fintypeOrInfinite α

Premises used: fintypeOrInfinite
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
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 : Fintype α
⊢ ∃ (g : α ≃ β),
    ∀ (x : (↑s : Type u_1)),
      Eq.{u_2 + 1} (α := β) ((g : (a : α) → β) (↑x : α) : β) ((f : (a : (↑s : Type u_1)) → β) x : β)

Tactic:
extend_function_finite f h

Premises used: Cardinal.extend_function_finite
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
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 : Fintype α
⊢ ∃ (g : α ≃ β),
    ∀ (x : (↑s : Type u_1)),
      Eq.{u_2 + 1} (α := β) ((g : (a : α) → β) (↑x : α) : β) ((f : (a : (↑s : Type u_1)) → β) x : β)

Tactic:
exact extend_function_finite f h

Premises used: Cardinal.extend_function_finite
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
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 α
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))
⊢ ∃ (g : α ≃ β),
    ∀ (x : (↑s : Type u_1)),
      Eq.{u_2 + 1} (α := β) ((g : (a : α) → β) (↑x : α) : β) ((f : (a : (↑s : Type u_1)) → β) x : β)

Tactic:
apply extend_function f

Premises used: Cardinal.extend_function
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
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 α
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))
⊢ 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

Premises used: id
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
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 : α ≃ β
⊢ Infinite β

Tactic:
haveI := Infinite.of_injective _ g.injective
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
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 β
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)
⊢ 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:
rw [← lift_mk_eq'] at h ⊢

Premises used: Cardinal.lift_mk_eq'
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
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 : #(↑(range.{u_2, u_1 + 1} (ι := (↑s : Type u_1)) (⇑f : (a : (↑s : Type u_1)) → β)) : Type u_2) < #β
⊢ 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:
rwa [mk_compl_of_infinite s hs, mk_compl_of_infinite]

Premises used: Cardinal.mk_compl_of_infinite
-- Module: Mathlib.SetTheory.Cardinal.Arithmetic
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} #β
inr₂ : lift.{u_2, u_1} #(↑s : Type u_1) < lift.{u_2, u_1} #α
inr₃ inr₄ inr₅ inr₆ : #(↑s : Type u_1) < #α
⊢ #(↑(range.{u_2, u_1 + 1} (ι := (↑s : Type u_1)) (⇑f : (a : (↑s : Type u_1)) → β)) : Type u_2) < #β

Tactic:
rwa [← lift_lt, mk_range_eq_of_injective f.injective, ← h, lift_lt]

Premises used: Cardinal.mk_range_eq_of_injective, Cardinal.lift_lt, Function.Embedding.injective
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
s : Set α
rw : Nonempty ((↑(ULift.down ⁻¹' s) : Type (max u v)) ≃ ULift.{v, u} (↑s : Type u))
⊢ #(↑(ULift.down ⁻¹' s) : Type (max u v)) = lift.{v, u} #(↑s : Type u)

Tactic:
rw [← mk_uLift, Cardinal.eq]

Premises used: Cardinal.mk_uLift, Cardinal.eq
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
s : Set α
val : (↑(ULift.down ⁻¹' s) : Type (max u v)) ≃ ULift.{v, u} (↑s : Type u)
⊢ Nonempty ((↑(ULift.down ⁻¹' s) : Type (max u v)) ≃ ULift.{v, u} (↑s : Type u))

Tactic:
constructor
-- Module: Mathlib.SetTheory.Cardinal.Basic
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 }
⊢ Bijective f

Tactic:
have : Function.Bijective f :=
    ULift.up_bijective.comp (restrictPreimage_bijective _ (ULift.down_bijective))
-- Module: Mathlib.SetTheory.Cardinal.Basic
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 }
this : Bijective f
⊢ (↑(ULift.down ⁻¹' s) : Type (max u v)) ≃ ULift.{v, u} (↑s : Type u)

Tactic:
exact Equiv.ofBijective f this

Premises used: Equiv.ofBijective
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
inst : Small.{v, u} α
⊢ lift.{max u w, v} #(Shrink.{v, u} α) = lift.{max v w, u} #α

Tactic:
lift_mk_eq.2 ⟨(equivShrink α).symm⟩

Premises used: Iff.mpr, Cardinal.lift_mk_eq, Nonempty.intro, Equiv.symm, equivShrink
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
inst : Small.{v, u} α
⊢ lift.{u, v} #(Shrink.{v, u} α) = lift.{v, u} #α

Tactic:
lift_mk_shrink.{u, v, 0} α

Premises used: Cardinal.lift_mk_shrink
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type (max u v)
inst : Small.{v, max u v} α
rw : lift.{max v u, v} #(Shrink.{v, max u v} α) = #α
rw₁ : lift.{v, max u v} #α = #α
rw₂ : lift.{max u v, max u v} #α = #α
rw₃ rw₄ : #α = #α
⊢ lift.{u, v} #(Shrink.{v, max u v} α) = #α

Tactic:
rw [← lift_umax, lift_mk_shrink.{max u v, v, 0} α, ← lift_umax, lift_id]

Premises used: Cardinal.lift_umax, Cardinal.lift_id
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
h : Fintype α
f : α → Cardinal.{v}
revert : ∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i : α, f i)
⊢ prod f = lift.{u, v} (∏ i : α, f i)

Tactic:
revert f
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
h : Fintype α
⊢ ∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i : α, f i)

Tactic:
Fintype.induction_empty_option ?_ ?_ ?_ α (h_fintype := h)

Premises used: Fintype.induction_empty_option
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α : Type u
h : Fintype α
refine_1 :
  ∀ (α β : Type u) [inst : Fintype β] (e : α ≃ β),
    (∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i : α, f i)) →
      ∀ (f : β → Cardinal.{v}), prod f = lift.{u, v} (∏ i : β, f i)
refine_2 : ∀ (f : PEmpty.{u + 1} → Cardinal.{v}), prod f = lift.{u, v} (∏ i : PEmpty.{u + 1}, f i)
refine_3 :
  ∀ (α : Type u) [inst : Fintype α],
    (∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i : α, f i)) →
      ∀ (f : Option α → Cardinal.{v}), prod f = lift.{u, v} (∏ i : Option α, f i)
⊢ ∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i : α, f i)

Tactic:
refine Fintype.induction_empty_option ?_ ?_ ?_ α (h_fintype := h)
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α_1 : Type u
h_1 : Fintype α_1
α β : Type u
hβ : Fintype β
e : α ≃ β
h : ∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i : α, f i)
f : β → Cardinal.{v}
this : Fintype α := Fintype.ofEquiv β e.symm
refine_1 : prod f = prod.{u, v} fun (i : α) ↦ f ((e : (a : α) → β) i)
⊢ prod f = lift.{u, v} (∏ i : β, f i)

Tactic:
rw [← e.prod_comp f, ← h]

Premises used: Equiv.prod_comp
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α_1 : Type u
h_1 : Fintype α_1
α β : Type u
hβ : Fintype β
e : α ≃ β
h : ∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i : α, f i)
f : β → Cardinal.{v}
this : Fintype α := Fintype.ofEquiv β e.symm
⊢ prod f = prod.{u, v} fun (i : α) ↦ f ((e : (a : α) → β) i)

Tactic:
mk_congr (e.piCongrLeft _).symm

Premises used: Equiv.piCongrLeft, Cardinal.prod, Equiv.symm, Cardinal.mk_congr
-- Module: Mathlib.SetTheory.Cardinal.Basic
Goal:
α_1 : Type u
h_1 : Fintype α_1
α β : Type u
hβ : Fintype β
e : α ≃ β
h : ∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i : α, f i)
f : β → Cardinal.{v}
this : Fintype α := Fintype.ofEquiv β e.symm
⊢ prod f = prod.{u, v} fun (i : α) ↦ f ((e : (a : α) → β) i)

Tactic:
exact mk_congr (e.piCongrLeft _).symm

Premises used: Equiv.piCongrLeft, Equiv.symm, Cardinal.mk_congr