awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Cardinal.NatCount
Goal:
p : ℕ → Prop
inst : DecidablePred p
n : ℕ
⊢ Cardinal.mk { k : ℕ // k < n ∧ p k } ≤ Cardinal.mk (↑{k : ℕ | p k} : Type)

Tactic:
exact Cardinal.mk_subtype_mono fun x hx ↦ hx.2

Premises used: Cardinal.mk_subtype_mono
-- Module: Mathlib.SetTheory.Cardinal.NatCount
Goal:
p : ℕ → Prop
inst : DecidablePred p
n : ℕ
simp : (↑(count p n) : Cardinal.{0}) ≤ Cardinal.mk { k : ℕ // p k }
⊢ (↑(count p n) : ℕ∞) ≤ Set.encard (α := ℕ) {k : ℕ | p k}

Tactic:
simp only [Set.encard, ENat.card, Set.coe_setOf, Cardinal.natCast_le_toENat]

Premises used: Set.encard, Cardinal.natCast_le_toENat, Set.coe_setOf, ENat.card
-- Module: Mathlib.SetTheory.Cardinal.NatCount
Goal:
p : ℕ → Prop
inst : DecidablePred p
n : ℕ
⊢ (↑(count p n) : Cardinal.{0}) ≤ Cardinal.mk { k : ℕ // p k }

Tactic:
Nat.count_le_cardinal n

Premises used: Set.Mem, Nat.count_le_cardinal, setOf
-- Module: Mathlib.SetTheory.Cardinal.NatCount
Goal:
p : ℕ → Prop
inst : DecidablePred p
n : ℕ
⊢ (↑(count p n) : Cardinal.{0}) ≤ Cardinal.mk { k : ℕ // p k }

Tactic:
exact Nat.count_le_cardinal n

Premises used: Nat.count_le_cardinal
-- Module: Mathlib.SetTheory.Cardinal.NatCount
Goal:
p : ℕ → Prop
inst : DecidablePred p
n : ℕ
h : Set.Finite (α := ℕ) {k : ℕ | p k}
⊢ Set.encard (α := ℕ) {k : ℕ | p k} ≠ ⊤

Tactic:
simpa
-- Module: Mathlib.SetTheory.Cardinal.NatCount
Goal:
p : ℕ → Prop
inst : DecidablePred p
n : ℕ
h : Set.Finite (α := ℕ) {k : ℕ | p k}
rw : (↑(count p n) : ℕ∞) ≤ Set.encard (α := ℕ) {k : ℕ | p k}
⊢ count p n ≤ Set.ncard (α := ℕ) {k : ℕ | p k}

Tactic:
rw [Set.ncard_def, ← ENat.coe_le_coe, ENat.coe_toNat (by simpa)]

Premises used: Set.ncard_def, ENat.coe_toNat, ENat.coe_le_coe
-- Module: Mathlib.SetTheory.Cardinal.NatCount
Goal:
p : ℕ → Prop
inst : DecidablePred p
n : ℕ
h : Set.Finite (α := ℕ) {k : ℕ | p k}
⊢ (↑(count p n) : ℕ∞) ≤ Set.encard (α := ℕ) {k : ℕ | p k}

Tactic:
count_le_setENCard n

Premises used: Nat.count_le_setENCard
-- Module: Mathlib.SetTheory.Cardinal.NatCount
Goal:
p : ℕ → Prop
inst : DecidablePred p
n : ℕ
h : Set.Finite (α := ℕ) {k : ℕ | p k}
⊢ (↑(count p n) : ℕ∞) ≤ Set.encard (α := ℕ) {k : ℕ | p k}

Tactic:
exact count_le_setENCard n

Premises used: Nat.count_le_setENCard
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α_1 β : Type u
a : Cardinal.{u}
α : Type u
⊢ LE.le (α := Cardinal.{u}) (Quot.mk (⇑isEquivalent : Type u → Type u → Prop) α)
    (Quot.mk (⇑isEquivalent : Type u → Type u → Prop) α)

Tactic:
⟨Embedding.refl _⟩

Premises used: Nonempty.intro, Function.Embedding.refl
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α_1 β : Type u
a : Cardinal.{u}
α : Type u
⊢ LE.le (α := Cardinal.{u}) (Quot.mk (⇑isEquivalent : Type u → Type u → Prop) α)
    (Quot.mk (⇑isEquivalent : Type u → Type u → Prop) α)

Tactic:
exact ⟨Embedding.refl _⟩
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α_1 β_1 : Type u
a : Cardinal.{u}
α : Type u
b : Cardinal.{u}
β : Type u
c : Cardinal.{u}
γ : Type u
e₁ : α ↪ β
e₂ : β ↪ γ
⊢ LE.le (α := Cardinal.{u}) (Quot.mk (⇑isEquivalent : Type u → Type u → Prop) α)
    (Quot.mk (⇑isEquivalent : Type u → Type u → Prop) γ)

Tactic:
⟨e₁.trans e₂⟩

Premises used: Nonempty.intro, Function.Embedding.trans
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α_1 β_1 : Type u
a : Cardinal.{u}
α : Type u
b : Cardinal.{u}
β : Type u
c : Cardinal.{u}
γ : Type u
e₁ : α ↪ β
e₂ : β ↪ γ
⊢ LE.le (α := Cardinal.{u}) (Quot.mk (⇑isEquivalent : Type u → Type u → Prop) α)
    (Quot.mk (⇑isEquivalent : Type u → Type u → Prop) γ)

Tactic:
exact ⟨e₁.trans e₂⟩
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α_1 β_1 : Type u
a : Cardinal.{u}
α : Type u
b : Cardinal.{u}
β : Type u
e₁ : α ↪ β
e₂ : β ↪ α
⊢ Eq (α := Cardinal.{u}) (Quot.mk (⇑isEquivalent : Type u → Type u → Prop) α)
    (Quot.mk (⇑isEquivalent : Type u → Type u → Prop) β)

Tactic:
Quotient.sound (e₁.antisymm e₂)

Premises used: Cardinal, Function.Embedding.antisymm, Quotient.sound
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α_1 β_1 : Type u
a : Cardinal.{u}
α : Type u
b : Cardinal.{u}
β : Type u
e₁ : α ↪ β
e₂ : β ↪ α
⊢ Eq (α := Cardinal.{u}) (Quot.mk (⇑isEquivalent : Type u → Type u → Prop) α)
    (Quot.mk (⇑isEquivalent : Type u → Type u → Prop) β)

Tactic:
exact Quotient.sound (e₁.antisymm e₂)

Premises used: Quotient.sound
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α_1 β_1 : Type u
a : Cardinal.{u}
α : Type u
b : Cardinal.{u}
β : Type u
⊢ LE.le (α := Cardinal.{u}) (Quot.mk (⇑isEquivalent : Type u → Type u → Prop) α)
      (Quot.mk (⇑isEquivalent : Type u → Type u → Prop) β) ∨
    LE.le (α := Cardinal.{u}) (Quot.mk (⇑isEquivalent : Type u → Type u → Prop) β)
      (Quot.mk (⇑isEquivalent : Type u → Type u → Prop) α)

Tactic:
apply Embedding.total

Premises used: Function.Embedding.total
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α β : Type u
⊢ #α ≤ #β ↔ Nonempty.{max 1 (u + 1)} (α ↪ β)

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α β : Type u
f : α → β
hf : Injective f
⊢ #α ≤ #β

Tactic:
⟨⟨f, hf⟩⟩

Premises used: Function.Embedding.mk, Nonempty.intro
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α β : Type u
f : α ↪ β
⊢ #α ≤ #β

Tactic:
⟨f⟩

Premises used: Nonempty.intro
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α β : Type u
f : α → β
hf : Surjective f
⊢ #β ≤ #α

Tactic:
⟨Embedding.ofSurjective f hf⟩

Premises used: Function.Embedding.ofSurjective, Nonempty.intro
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
c : Cardinal.{u}
α : Type u
⊢ c ≤ #α ↔ ∃ (p : Set α), #(↑p : Type u) = c

Tactic:
⟨inductionOn c fun _ ⟨⟨f, hf⟩⟩ => ⟨Set.range f, (Equiv.ofInjective f hf).cardinal_eq.symm⟩,
    fun ⟨_, e⟩ => e ▸ ⟨⟨Subtype.val, fun _ _ => Subtype.ext⟩⟩⟩

Premises used: Cardinal.mk, Function.Embedding.mk, Eq.rec, LE.le, Nonempty.intro, _private.0.Cardinal.le_mk_iff_exists_set.match_2, Iff.intro, Cardinal.inductionOn, Subtype.val, Subtype.ext
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α : Type u
p : α → Prop
⊢ #(Subtype p) ≤ #α

Tactic:
⟨Embedding.subtype p⟩

Premises used: Nonempty.intro, Function.Embedding.subtype
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α : Type u
s : Set α
⊢ #(↑s : Type u) ≤ #α

Tactic:
mk_subtype_le (· ∈ s)

Premises used: Membership.mem, Cardinal.mk_subtype_le
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
c c' : Cardinal.{u_1}
rw : Nonempty.{u_1 + 1} (Quotient.out c ↪ Quotient.out c')
| c ≤ c'

Tactic:
rw [← Cardinal.mk_out c, ← Cardinal.mk_out c', le_def]

Premises used: Cardinal.mk_out, Cardinal.le_def
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
c c' : Cardinal.{u_1}
conv_lhs : c ≤ c' ↔ Nonempty.{u_1 + 1} (Quotient.out c ↪ Quotient.out c')
conv_lhs₁ :
  Nonempty.{u_1 + 1} (Quotient.out c ↪ Quotient.out c') ↔ Nonempty.{u_1 + 1} (Quotient.out c ↪ Quotient.out c')
⊢ c ≤ c' ↔ Nonempty.{u_1 + 1} (Quotient.out c ↪ Quotient.out c')

Tactic:
conv_lhs => rw [← Cardinal.mk_out c, ← Cardinal.mk_out c', le_def]

Premises used: Cardinal.mk_out, Cardinal.le_def
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α : Type v
β : Type w
⊢ lift.{max u w, v} #α ≤ lift.{max u v, w} #β ↔ Nonempty (α ↪ β)

Tactic:
⟨fun ⟨f⟩ => ⟨Embedding.congr Equiv.ulift Equiv.ulift f⟩, fun ⟨f⟩ =>
    ⟨Embedding.congr Equiv.ulift.symm Equiv.ulift.symm f⟩⟩

Premises used: Cardinal.lift, Cardinal.mk, Equiv.ulift, LE.le, Nonempty.intro, Function.Embedding, _private.0.Cardinal.lift_mk_le.match_1, Iff.intro, Nonempty, Function.Embedding.congr, Equiv.symm, _private.0.Cardinal.lift_mk_le.match_2
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α : Type u
β : Type v
⊢ lift.{v, u} #α ≤ lift.{u, v} #β ↔ Nonempty (α ↪ β)

Tactic:
lift_mk_le.{0}

Premises used: Cardinal.lift_mk_le
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α β : Type u
refine_1 : ∀ (a b : Cardinal.{u}), lift.{v, u} a ≤ lift.{v, u} b ↔ a ≤ b
refine_2 :
  ∀ (a : Cardinal.{u}),
    ∀
      b <
        (OrderEmbedding.ltEmbedding (OrderEmbedding.ofMapLEIff lift.{v, u} ⋯) : (a : Cardinal.{u}) → Cardinal.{max u v})
          a,
      Membership.mem (γ := Set Cardinal.{max u v})
        (Set.range (ι := Cardinal.{u})
          (⇑(OrderEmbedding.ltEmbedding (OrderEmbedding.ofMapLEIff lift.{v, u} ⋯)) :
            (a : Cardinal.{u}) → Cardinal.{max u v}))
        b
⊢ InitialSeg (fun (x1 x2 : Cardinal.{u}) ↦ x1 < x2) fun (x1 x2 : Cardinal.{max u v}) ↦ x1 < x2

Tactic:
refine ⟨(OrderEmbedding.ofMapLEIff lift ?_).ltEmbedding, ?_⟩
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α β : Type u
a b : Cardinal.{u}
⊢ lift.{v, u} a ≤ lift.{v, u} b ↔ a ≤ b

Tactic:
inductionOn₂ a b fun _ _ ↦ ?_

Premises used: Cardinal.inductionOn₂
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α β : Type u
a b : Cardinal.{u}
refine_1 : ∀ (x x_1 : Type u), lift.{v, u} #x ≤ lift.{v, u} #x_1 ↔ #x ≤ #x_1
⊢ lift.{v, u} a ≤ lift.{v, u} b ↔ a ≤ b

Tactic:
refine inductionOn₂ a b fun _ _ ↦ ?_
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α β : Type u
a b : Cardinal.{u}
x x_1 : Type u
refine_1 : lift.{max u v, u} #x ≤ lift.{max u v, u} #x_1 ↔ #x ≤ #x_1
refine_1₁ : Nonempty.{u + 1} (x ↪ x_1) ↔ #x ≤ #x_1
refine_1₂ refine_1₃ : Nonempty.{u + 1} (x ↪ x_1) ↔ Nonempty.{u + 1} (x ↪ x_1)
⊢ lift.{v, u} #x ≤ lift.{v, u} #x_1 ↔ #x ≤ #x_1

Tactic:
rw [← lift_umax, lift_mk_le.{v, u, u}, le_def]

Premises used: Cardinal.lift_umax, Cardinal.le_def
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α β : Type u
a : Cardinal.{u}
b : Cardinal.{max u v}
⊢ b <
      (OrderEmbedding.ltEmbedding (OrderEmbedding.ofMapLEIff lift.{v, u} ⋯) : (a : Cardinal.{u}) → Cardinal.{max u v})
        a →
    Membership.mem (γ := Set Cardinal.{max u v})
      (Set.range (ι := Cardinal.{u})
        (⇑(OrderEmbedding.ltEmbedding (OrderEmbedding.ofMapLEIff lift.{v, u} ⋯)) :
          (a : Cardinal.{u}) → Cardinal.{max u v}))
      b

Tactic:
inductionOn₂ a b fun α β h ↦ ?_

Premises used: Cardinal.inductionOn₂
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α β : Type u
a : Cardinal.{u}
b : Cardinal.{max u v}
refine_2 :
  ∀ (α : Type u) (β : Type (max u v))
    (h :
      #β <
        (OrderEmbedding.ltEmbedding (OrderEmbedding.ofMapLEIff lift.{v, u} ⋯) : (a : Cardinal.{u}) → Cardinal.{max u v})
          #α),
    Membership.mem (γ := Set Cardinal.{max u v})
      (Set.range (ι := Cardinal.{u})
        (⇑(OrderEmbedding.ltEmbedding (OrderEmbedding.ofMapLEIff lift.{v, u} ⋯)) :
          (a : Cardinal.{u}) → Cardinal.{max u v}))
      #β
⊢ b <
      (OrderEmbedding.ltEmbedding (OrderEmbedding.ofMapLEIff lift.{v, u} ⋯) : (a : Cardinal.{u}) → Cardinal.{max u v})
        a →
    Membership.mem (γ := Set Cardinal.{max u v})
      (Set.range (ι := Cardinal.{u})
        (⇑(OrderEmbedding.ltEmbedding (OrderEmbedding.ofMapLEIff lift.{v, u} ⋯)) :
          (a : Cardinal.{u}) → Cardinal.{max u v}))
      b

Tactic:
refine inductionOn₂ a b fun α β h ↦ ?_
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α_1 β_1 : Type u
a : Cardinal.{u}
b : Cardinal.{max u v}
α : Type u
β : Type (max u v)
h :
  #β <
    (OrderEmbedding.ltEmbedding (OrderEmbedding.ofMapLEIff lift.{v, u} ⋯) : (a : Cardinal.{u}) → Cardinal.{max u v}) #α
refine_2 :
  ∀ (e : β ↪ ULift.{v, u} α),
    Membership.mem (γ := Set Cardinal.{max u v})
      (Set.range (ι := Cardinal.{u})
        (⇑(OrderEmbedding.ltEmbedding (OrderEmbedding.ofMapLEIff lift.{v, u} ⋯)) :
          (a : Cardinal.{u}) → Cardinal.{max u v}))
      #β
⊢ Membership.mem (γ := Set Cardinal.{max u v})
    (Set.range (ι := Cardinal.{u})
      (⇑(OrderEmbedding.ltEmbedding (OrderEmbedding.ofMapLEIff lift.{v, u} ⋯)) :
        (a : Cardinal.{u}) → Cardinal.{max u v}))
    #β

Tactic:
obtain ⟨e⟩ := h.le

Premises used: LT.lt.le
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α_1 β_1 : Type u
a : Cardinal.{u}
b : Cardinal.{max u v}
α : Type u
β : Type (max u v)
h :
  #β <
    (OrderEmbedding.ltEmbedding (OrderEmbedding.ofMapLEIff lift.{v, u} ⋯) : (a : Cardinal.{u}) → Cardinal.{max u v}) #α
e : β ↪ ULift.{v, u} α
refine_2 :
  ∀ (e : β ↪ α),
    Membership.mem (γ := Set Cardinal.{max u v})
      (Set.range (ι := Cardinal.{u})
        (⇑(OrderEmbedding.ltEmbedding (OrderEmbedding.ofMapLEIff lift.{v, u} ⋯)) :
          (a : Cardinal.{u}) → Cardinal.{max u v}))
      #β
⊢ Membership.mem (γ := Set Cardinal.{max u v})
    (Set.range (ι := Cardinal.{u})
      (⇑(OrderEmbedding.ltEmbedding (OrderEmbedding.ofMapLEIff lift.{v, u} ⋯)) :
        (a : Cardinal.{u}) → Cardinal.{max u v}))
    #β

Tactic:
replace e := e.congr (Equiv.refl β) Equiv.ulift
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α_1 β_1 : Type u
a : Cardinal.{u}
b : Cardinal.{max u v}
α : Type u
β : Type (max u v)
h :
  #β <
    (OrderEmbedding.ltEmbedding (OrderEmbedding.ofMapLEIff lift.{v, u} ⋯) : (a : Cardinal.{u}) → Cardinal.{max u v}) #α
e : β ↪ α
⊢ Membership.mem (γ := Set Cardinal.{max u v})
    (Set.range (ι := Cardinal.{u})
      (⇑(OrderEmbedding.ltEmbedding (OrderEmbedding.ofMapLEIff lift.{v, u} ⋯)) :
        (a : Cardinal.{u}) → Cardinal.{max u v}))
    #β

Tactic:
⟨#(range e), mk_congr (Equiv.ulift.trans <| Equiv.symm ?_)⟩

Premises used: Set.Mem, Equiv.trans, setOf, Cardinal.mk, Equiv.ulift, Set.Elem, Exists.intro, Set.range, Equiv.symm, DFunLike.coe, Cardinal.mk_congr
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α_1 β_1 : Type u
a : Cardinal.{u}
b : Cardinal.{max u v}
α : Type u
β : Type (max u v)
h :
  #β <
    (OrderEmbedding.ltEmbedding (OrderEmbedding.ofMapLEIff lift.{v, u} ⋯) : (a : Cardinal.{u}) → Cardinal.{max u v}) #α
e : β ↪ α
refine_2 : β ≃ (↑(Set.range (ι := β) (⇑e : (a : β) → α)) : Type u)
⊢ Membership.mem (γ := Set Cardinal.{max u v})
    (Set.range (ι := Cardinal.{u})
      (⇑(OrderEmbedding.ltEmbedding (OrderEmbedding.ofMapLEIff lift.{v, u} ⋯)) :
        (a : Cardinal.{u}) → Cardinal.{max u v}))
    #β

Tactic:
refine ⟨#(range e), mk_congr (Equiv.ulift.trans <| Equiv.symm ?_)⟩
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α_1 β_1 : Type u
a : Cardinal.{u}
b : Cardinal.{max u v}
α : Type u
β : Type (max u v)
h :
  #β <
    (OrderEmbedding.ltEmbedding (OrderEmbedding.ofMapLEIff lift.{v, u} ⋯) : (a : Cardinal.{u}) → Cardinal.{max u v}) #α
e : β ↪ α
refine_2 :
  Surjective (α := β) (β := (↑(Set.range (ι := β) (⇑e : (a : β) → α)) : Type u))
    (⇑(Embedding.codRestrict (Set.range (ι := β) (⇑e : (a : β) → α)) e ⋯) :
      (a : β) → (↑(Set.range (⇑e : (a : β) → α)) : Type u))
⊢ β ≃ (↑(Set.range (ι := β) (⇑e : (a : β) → α)) : Type u)

Tactic:
apply (e.codRestrict _ mem_range_self).equivOfSurjective

Premises used: Set.mem_range_self, Function.Embedding.codRestrict, Function.Embedding.equivOfSurjective
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α_1 β_1 : Type u
a : Cardinal.{u}
b_1 : Cardinal.{max u v}
α : Type u
β : Type (max u v)
h :
  #β <
    (OrderEmbedding.ltEmbedding (OrderEmbedding.ofMapLEIff lift.{v, u} ⋯) : (a : Cardinal.{u}) → Cardinal.{max u v}) #α
e : β ↪ α
b : β
⊢ ∃ (a : β),
    Eq.{u + 1} (α := (↑(Set.range (ι := β) (⇑e : (a : β) → α)) : Type u))
      ((Embedding.codRestrict (Set.range (ι := β) (⇑e : (a : β) → α)) e ⋯ :
            (a : β) → (↑(Set.range (⇑e : (a : β) → α)) : Type u))
          a :
        (↑(Set.range (ι := β) (⇑e : (a : β) → α)) : Type u))
      (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) (Set.range (ι := β) (⇑e : (a : β) → α)) x)
          ((e : (a : β) → α) b) ⋯ :
        { x : α // Membership.mem (γ := Set α) (Set.range (ι := β) (⇑e : (a : β) → α)) x })

Tactic:
⟨b, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α_1 β_1 : Type u
a : Cardinal.{u}
b_1 : Cardinal.{max u v}
α : Type u
β : Type (max u v)
h :
  #β <
    (OrderEmbedding.ltEmbedding (OrderEmbedding.ofMapLEIff lift.{v, u} ⋯) : (a : Cardinal.{u}) → Cardinal.{max u v}) #α
e : β ↪ α
b : β
⊢ ∃ (a : β),
    Eq.{u + 1} (α := (↑(Set.range (ι := β) (⇑e : (a : β) → α)) : Type u))
      ((Embedding.codRestrict (Set.range (ι := β) (⇑e : (a : β) → α)) e ⋯ :
            (a : β) → (↑(Set.range (⇑e : (a : β) → α)) : Type u))
          a :
        (↑(Set.range (ι := β) (⇑e : (a : β) → α)) : Type u))
      (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Set α) (Set.range (ι := β) (⇑e : (a : β) → α)) x)
          ((e : (a : β) → α) b) ⋯ :
        { x : α // Membership.mem (γ := Set α) (Set.range (ι := β) (⇑e : (a : β) → α)) x })

Tactic:
exact ⟨b, rfl⟩
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
a : Cardinal.{u}
b : Cardinal.{max u v}
⊢ b ≤ lift.{v, u} a → b ∈ Set.range lift.{v, u}

Tactic:
liftInitialSeg.mem_range_of_le

Premises used: InitialSeg.mem_range_of_le, Set.Mem, Quotient.map, Cardinal.lift, Cardinal.map, Cardinal.liftInitialSeg, Quot.map
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
⊢ Injective lift.{u, v}

Tactic:
liftInitialSeg.injective

Premises used: RelEmbedding.injective, Quotient.map, Cardinal.lift, Cardinal.map, InitialSeg.toRelEmbedding, Cardinal.liftInitialSeg, Quot.map
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
a b : Cardinal.{u}
⊢ lift.{v, u} a = lift.{v, u} b ↔ a = b

Tactic:
lift_injective.eq_iff

Premises used: Function.Injective.eq_iff, Cardinal.lift_injective
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
a b : Cardinal.{v}
⊢ lift.{u, v} a ≤ lift.{u, v} b ↔ a ≤ b

Tactic:
liftInitialSeg.le_iff_le

Premises used: Quotient.map, Cardinal.lift, Cardinal.map, Cardinal.liftInitialSeg, Quot.map, InitialSeg.le_iff_le
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
a b : Cardinal.{u}
⊢ lift.{v, u} a < lift.{v, u} b ↔ a < b

Tactic:
liftInitialSeg.lt_iff_lt

Premises used: Quotient.map, Cardinal.lift, InitialSeg.lt_iff_lt, Cardinal.map, Cardinal.liftInitialSeg, Quot.map
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
⊢ StrictMono lift.{u_2, u_1}

Tactic:
fun _ _ => lift_lt.2

Premises used: Iff.mpr, StrictMono, Cardinal.lift_lt
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
⊢ Monotone lift.{u_2, u_1}

Tactic:
lift_strictMono.monotone

Premises used: StrictMono.monotone, Cardinal.lift_strictMono
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
a b : Cardinal.{v}
⊢ lift.{u, v} (min a b) = min (lift.{u, v} a) (lift.{u, v} b)

Tactic:
lift_monotone.map_min

Premises used: Cardinal.lift_monotone, Monotone.map_min
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
a b : Cardinal.{v}
⊢ lift.{u, v} (max a b) = max (lift.{u, v} a) (lift.{u, v} b)

Tactic:
lift_monotone.map_max

Premises used: Cardinal.lift_monotone, Monotone.map_max
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
a : Cardinal.{u}
b : Cardinal.{v}
rw : lift.{w, max v u} (lift.{v, u} a) = lift.{max u w, v} b ↔ lift.{v, u} a = lift.{u, v} b
rw₁ : lift.{w, max v u} (lift.{v, u} a) = lift.{w, max u v} (lift.{u, v} b) ↔ lift.{v, u} a = lift.{u, v} b
rw₂ rw₃ : lift.{v, u} a = lift.{u, v} b ↔ lift.{v, u} a = lift.{u, v} b
⊢ lift.{max v w, u} a = lift.{max u w, v} b ↔ lift.{v, u} a = lift.{u, v} b

Tactic:
rw [← lift_lift.{v, w, u}, ← lift_lift.{u, w, v}, lift_inj]

Premises used: Cardinal.lift_inj
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
a : Cardinal.{u}
b : Cardinal.{max u v}
⊢ b ≤ lift.{v, u} a ↔ ∃ a' ≤ a, lift.{v, u} a' = b

Tactic:
liftInitialSeg.le_apply_iff

Premises used: Quotient.map, Cardinal.lift, Cardinal.map, Cardinal.liftInitialSeg, Quot.map, InitialSeg.le_apply_iff
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
a : Cardinal.{u}
b : Cardinal.{max u v}
⊢ b < lift.{v, u} a ↔ ∃ a' < a, lift.{v, u} a' = b

Tactic:
liftInitialSeg.lt_apply_iff

Premises used: Quotient.map, Cardinal.lift, InitialSeg.lt_apply_iff, Cardinal.map, Cardinal.liftInitialSeg, Quot.map
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
a : Cardinal.{v}
⊢ lift.{u, v} a = 0 ↔ a = 0

Tactic:
lift_injective.eq_iff' lift_zero

Premises used: Cardinal.lift_zero, Function.Injective.eq_iff', Cardinal.lift_injective
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α : Type u
h : Fintype α
⊢ Fintype.card α = Fintype.card.{u} (ULift.{u, 0} (Fin (Fintype.card α)))

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
n : ℕ
rw : #(ULift.{u, 0} (Fin (n + 1))) = #(Option (ULift.{u, 0} (Fin n)))
⊢ #(ULift.{u, 0} (Fin (n + 1))) = #(ULift.{u, 0} (Fin n)) + 1

Tactic:
rw [← mk_option]

Premises used: Cardinal.mk_option
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
n : ℕ
⊢ #(ULift.{u, 0} (Fin (n + 1))) = #(Option (ULift.{u, 0} (Fin n)))

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α β : Type u
n : ℕ
c : Cardinal.{u}
rw : c ^ HAdd.hAdd (α := Cardinal.{u}) (↑n : Cardinal.{u}) 1 = HPow.hPow (β := Cardinal.{u}) c (↑n : Cardinal.{u}) * c
rw₁ :
  HPow.hPow (β := Cardinal.{u}) c (↑n : Cardinal.{u}) * HPow.hPow (β := Cardinal.{u}) c 1 =
    HPow.hPow (β := Cardinal.{u}) c (↑n : Cardinal.{u}) * c
rw₂ rw₃ :
  HPow.hPow (β := Cardinal.{u}) c (↑n : Cardinal.{u}) * c = HPow.hPow (β := Cardinal.{u}) c (↑n : Cardinal.{u}) * c
⊢ HPow.hPow (β := Cardinal.{u}) c (↑(n + 1) : Cardinal.{u}) = HPow.hPow (β := Cardinal.{u}) c (↑n : Cardinal.{u}) * c

Tactic:
rw [cast_succ, power_add, power_one]

Premises used: Cardinal.power_add, Cardinal.power_one, _private.0.Cardinal.cast_succ
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
⊢ #Bool = 2

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
⊢ #Prop = 2

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
a b c : Cardinal.{u_1}
rw : a ^ (c * b) = (a ^ b) ^ c
⊢ a ^ (b * c) = (a ^ b) ^ c

Tactic:
rw [mul_comm b c]

Premises used: mul_comm
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
a b c : Cardinal.{u_1}
⊢ a ^ (c * b) = (a ^ b) ^ c

Tactic:
inductionOn₃ a b c fun α β γ => mk_congr <| Equiv.curry γ β α

Premises used: Cardinal.inductionOn₃
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
a b c : Cardinal.{u_1}
⊢ a ^ (c * b) = (a ^ b) ^ c

Tactic:
exact inductionOn₃ a b c fun α β γ => mk_congr <| Equiv.curry γ β α
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
a : Cardinal.{u}
n : ℕ
⊢ HPow.hPow (β := Cardinal.{u}) a (↑n : Cardinal.{u}) = a ^ n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
a : Cardinal.{v}
⊢ lift.{u, v} a = 1 ↔ a = 1

Tactic:
lift_injective.eq_iff' lift_one

Premises used: Function.Injective.eq_iff', Cardinal.lift_one, Cardinal.lift_injective
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
a b : Cardinal.{u}
⊢ lift.{v, u} (a * b) = lift.{v, u} a * lift.{v, u} b

Tactic:
inductionOn₂ a b fun _ _ =>
    mk_congr <| Equiv.ulift.trans (Equiv.prodCongr Equiv.ulift Equiv.ulift).symm

Premises used: Cardinal.inductionOn₂
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
⊢ lift.{u, v} 2 = 2

Tactic:
simp [← one_add_one_eq_two]

Premises used: one_add_one_eq_two
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α : Type u
⊢ #(Set α) = HPow.hPow (α := Cardinal.{u}) 2 #α

Tactic:
simp [← mk_congr (Equiv.ofBijective _ Set.setOf_bijective), ← one_add_one_eq_two]

Premises used: one_add_one_eq_two, Equiv.ofBijective, Cardinal.mk_congr, Set.setOf_bijective
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α : Type u
s : Set α
⊢ #(↑(𝒫 s) : Type u) = HPow.hPow (α := Cardinal.{u}) 2 #(↑s : Type u)

Tactic:
(mk_congr (Equiv.Set.powerset s)).trans mk_set

Premises used: Equiv.Set.powerset, Cardinal.mk_set, Cardinal.mk_congr, Eq.trans
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
a : Cardinal.{u_1}
⊢ lift.{v, u_1} (HPow.hPow (α := Cardinal.{u_1}) 2 a) = HPow.hPow (α := Cardinal.{max u_1 v}) 2 (lift.{v, u_1} a)

Tactic:
simp [← one_add_one_eq_two]

Premises used: one_add_one_eq_two
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α_1 β : Type u
a : Cardinal.{u}
α : Type u
⊢ LE.le (α := Cardinal.{u}) 0 (Quot.mk (⇑isEquivalent : Type u → Type u → Prop) α)

Tactic:
⟨Embedding.ofIsEmpty⟩

Premises used: Function.Embedding.ofIsEmpty, Nonempty.intro
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α_1 β : Type u
a : Cardinal.{u}
α : Type u
⊢ LE.le (α := Cardinal.{u}) 0 (Quot.mk (⇑isEquivalent : Type u → Type u → Prop) α)

Tactic:
exact ⟨Embedding.ofIsEmpty⟩
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
a : Cardinal.{u_1}
α : Type u_1
b : Cardinal.{u_1}
β : Type u_1
c : Cardinal.{u_1}
γ : Type u_1
d : Cardinal.{u_1}
δ : Type u_1
e₁ : α ↪ β
e₂ : γ ↪ δ
⊢ HAdd.hAdd (α := Cardinal.{u_1}) (Quot.mk (⇑isEquivalent : Type u_1 → Type u_1 → Prop) α)
      (Quot.mk (⇑isEquivalent : Type u_1 → Type u_1 → Prop) γ) ≤
    HAdd.hAdd (α := Cardinal.{u_1}) (Quot.mk (⇑isEquivalent : Type u_1 → Type u_1 → Prop) β)
      (Quot.mk (⇑isEquivalent : Type u_1 → Type u_1 → Prop) δ)

Tactic:
⟨e₁.sumMap e₂⟩

Premises used: Function.Embedding.sumMap, Nonempty.intro