awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact ⟨e₁.sumMap e₂⟩
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α β : Type u
⊢ AddLeftMono Cardinal.{u_1}

Tactic:
⟨fun _ _ _ => add_le_add' le_rfl⟩

Premises used: CovariantClass.mk, le_rfl, _private.0.Cardinal.add_le_add'
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α β : Type u
⊢ AddRightMono Cardinal.{u_1}

Tactic:
⟨fun _ _ _ h => add_le_add' h le_rfl⟩

Premises used: CovariantClass.mk, le_rfl, _private.0.Cardinal.add_le_add'
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α_1 β_1 : Type u
a b : Cardinal.{u}
α β : Type u
h : #α ≤ #β
f : α → β
hf : Injective f
⊢ α ⊕ (↑(Set.range f)ᶜ : Type u) ≃ β

Tactic:
exact (Equiv.sumCongr (Equiv.ofInjective f hf) (Equiv.refl _)).trans <|
          Equiv.Set.sumCompl (range f)

Premises used: Equiv.trans, Equiv.Set.sumCompl, Equiv.ofInjective, Equiv.sumCongr, Set.range, Equiv.refl
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α_1 β_1 : Type u
a b : Cardinal.{u}
α β : Type u
h : #α ≤ #β
f : α → β
hf : Injective f
⊢ α ⊕ (↑(Set.range f)ᶜ : Type u) ≃ β

Tactic:
classical
        exact (Equiv.sumCongr (Equiv.ofInjective f hf) (Equiv.refl _)).trans <|
          Equiv.Set.sumCompl (range f)

Premises used: Equiv.trans, Equiv.ofInjective, Equiv.sumCongr, Equiv.refl
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
a : Cardinal.{u_1}
⊢ 0 ≤ a

Tactic:
zero_le

Premises used: zero_le
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α β : Type u
⊢ IsOrderedRing Cardinal.{u}

Tactic:
CanonicallyOrderedAdd.toIsOrderedRing

Premises used: CanonicallyOrderedAdd.toIsOrderedRing
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α_1 β_1 : Type u
a b : Cardinal.{u}
α β : Type u
⊢ #α * #β = 0 → #α = 0 ∨ #β = 0

Tactic:
simpa only [mul_def, mk_eq_zero_iff, isEmpty_prod] using id

Premises used: isEmpty_prod, id, Cardinal.mul_def, Cardinal.mk_eq_zero_iff
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
c : Cardinal.{u}
pos : ∀ (h : c = 0), HPow.hPow (α := Cardinal.{u}) 0 c ≤ 1
neg : ∀ (h : ¬c = 0), HPow.hPow (α := Cardinal.{u}) 0 c ≤ 1
⊢ HPow.hPow (α := Cardinal.{u}) 0 c ≤ 1

Tactic:
by_cases h : c = 0
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
c : Cardinal.{u}
h : c = 0
pos : HPow.hPow (α := Cardinal.{u}) (β := Cardinal.{u}) 0 0 ≤ 1
pos₁ pos₂ : LE.le.{u + 1} (α := Cardinal.{u}) 1 1
⊢ HPow.hPow (α := Cardinal.{u}) 0 c ≤ 1

Tactic:
rw [h, power_zero]

Premises used: Cardinal.power_zero
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
c : Cardinal.{u}
h : ¬c = 0
neg : LE.le.{u + 1} (α := Cardinal.{u}) 0 1
⊢ HPow.hPow (α := Cardinal.{u}) 0 c ≤ 1

Tactic:
rw [zero_power h]

Premises used: Cardinal.zero_power
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
c : Cardinal.{u}
h : ¬c = 0
⊢ LE.le.{u + 1} (α := Cardinal.{u}) 0 1

Tactic:
apply zero_le

Premises used: zero_le
-- 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
hα : Ne (α := Cardinal.{u_1}) (Quot.mk (⇑isEquivalent : Type u_1 → Type u_1 → Prop) α) 0
e : β ↪ γ
mk :
  ∀ (a : α),
    HPow.hPow (α := Cardinal.{u_1}) (β := Cardinal.{u_1}) (Quot.mk (⇑isEquivalent : Type u_1 → Type u_1 → Prop) α)
        (Quot.mk (⇑isEquivalent : Type u_1 → Type u_1 → Prop) β) ≤
      HPow.hPow (α := Cardinal.{u_1}) (β := Cardinal.{u_1}) (Quot.mk (⇑isEquivalent : Type u_1 → Type u_1 → Prop) α)
        (Quot.mk (⇑isEquivalent : Type u_1 → Type u_1 → Prop) γ)
⊢ HPow.hPow (α := Cardinal.{u_1}) (β := Cardinal.{u_1}) (Quot.mk (⇑isEquivalent : Type u_1 → Type u_1 → Prop) α)
      (Quot.mk (⇑isEquivalent : Type u_1 → Type u_1 → Prop) β) ≤
    HPow.hPow (α := Cardinal.{u_1}) (β := Cardinal.{u_1}) (Quot.mk (⇑isEquivalent : Type u_1 → Type u_1 → Prop) α)
      (Quot.mk (⇑isEquivalent : Type u_1 → Type u_1 → Prop) γ)

Tactic:
let ⟨a⟩ := mk_ne_zero_iff.1 hα
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
a_1 : Cardinal.{u_1}
α : Type u_1
b : Cardinal.{u_1}
β : Type u_1
c : Cardinal.{u_1}
γ : Type u_1
hα : Ne (α := Cardinal.{u_1}) (Quot.mk (⇑isEquivalent : Type u_1 → Type u_1 → Prop) α) 0
e : β ↪ γ
a : α
⊢ HPow.hPow (α := Cardinal.{u_1}) (β := Cardinal.{u_1}) (Quot.mk (⇑isEquivalent : Type u_1 → Type u_1 → Prop) α)
      (Quot.mk (⇑isEquivalent : Type u_1 → Type u_1 → Prop) β) ≤
    HPow.hPow (α := Cardinal.{u_1}) (β := Cardinal.{u_1}) (Quot.mk (⇑isEquivalent : Type u_1 → Type u_1 → Prop) α)
      (Quot.mk (⇑isEquivalent : Type u_1 → Type u_1 → Prop) γ)

Tactic:
⟨@Function.Embedding.arrowCongrLeft _ _ _ ⟨a⟩ e⟩

Premises used: Function.Embedding.arrowCongrLeft, Nonempty.intro
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
a_1 : Cardinal.{u_1}
α : Type u_1
b : Cardinal.{u_1}
β : Type u_1
c : Cardinal.{u_1}
γ : Type u_1
hα : Ne (α := Cardinal.{u_1}) (Quot.mk (⇑isEquivalent : Type u_1 → Type u_1 → Prop) α) 0
e : β ↪ γ
a : α
⊢ HPow.hPow (α := Cardinal.{u_1}) (β := Cardinal.{u_1}) (Quot.mk (⇑isEquivalent : Type u_1 → Type u_1 → Prop) α)
      (Quot.mk (⇑isEquivalent : Type u_1 → Type u_1 → Prop) β) ≤
    HPow.hPow (α := Cardinal.{u_1}) (β := Cardinal.{u_1}) (Quot.mk (⇑isEquivalent : Type u_1 → Type u_1 → Prop) α)
      (Quot.mk (⇑isEquivalent : Type u_1 → Type u_1 → Prop) γ)

Tactic:
exact ⟨@Function.Embedding.arrowCongrLeft _ _ _ ⟨a⟩ e⟩
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
a b : Cardinal.{u_1}
hb : 1 ≤ b
inl : 0 ≤ HPow.hPow (α := Cardinal.{u_1}) 0 b
inr : ∀ (ha : a ≠ 0), a ≤ a ^ b
⊢ a ≤ a ^ b

Tactic:
rcases eq_or_ne a 0 with (rfl | ha)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
b : Cardinal.{u_1}
hb : 1 ≤ b
⊢ 0 ≤ HPow.hPow (α := Cardinal.{u_1}) 0 b

Tactic:
zero_le

Premises used: zero_le
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
b : Cardinal.{u_1}
hb : 1 ≤ b
⊢ 0 ≤ HPow.hPow (α := Cardinal.{u_1}) 0 b

Tactic:
exact zero_le

Premises used: zero_le
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
a b : Cardinal.{u_1}
hb : 1 ≤ b
ha : a ≠ 0
⊢ HPow.hPow (β := Cardinal.{u_1}) a 1 ≤ a ^ b

Tactic:
power_le_power_left ha hb

Premises used: Cardinal.power_le_power_left
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
a b : Cardinal.{u_1}
hb : 1 ≤ b
ha : a ≠ 0
h : a = HPow.hPow (β := Cardinal.{u_1}) a 1
⊢ a ≤ a ^ b

Tactic:
convert! power_le_power_left ha hb

Premises used: Cardinal.power_le_power_left
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
a b : Cardinal.{u_1}
hb : 1 ≤ b
ha : a ≠ 0
⊢ a = HPow.hPow (β := Cardinal.{u_1}) a 1

Tactic:
(power_one a).symm

Premises used: Cardinal.power_one, Eq.symm
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
a b : Cardinal.{u_1}
hb : 1 ≤ b
ha : a ≠ 0
⊢ a = HPow.hPow (β := Cardinal.{u_1}) a 1

Tactic:
exact (power_one a).symm

Premises used: Cardinal.power_one, Eq.symm
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
a : Cardinal.{u}
mk : ∀ (α : Type u), #α < HPow.hPow (α := Cardinal.{u}) 2 #α
⊢ a < HPow.hPow (α := Cardinal.{u}) 2 a

Tactic:
induction a using Cardinal.inductionOn with | _ α
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α : Type u
mk : #α < #(Set α)
⊢ #α < HPow.hPow (α := Cardinal.{u}) 2 #α

Tactic:
rw [← mk_set]

Premises used: Cardinal.mk_set
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α : Type u
⊢ #α < #(Set α)

Tactic:
⟨⟨⟨singleton, fun a b => singleton_eq_singleton_iff.1⟩⟩, ?_⟩

Premises used: Function.Embedding.mk, Set.singleton_eq_singleton_iff, Nonempty.intro, And.intro, Iff.mp, Singleton.singleton
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α : Type u
mk : ¬#(Set α) ≤ #α
⊢ #α < #(Set α)

Tactic:
refine ⟨⟨⟨singleton, fun a b => singleton_eq_singleton_iff.1⟩⟩, ?_⟩
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α : Type u
f : Set α → α
hf : Injective f
⊢ False

Tactic:
cantor_injective f hf

Premises used: Function.cantor_injective
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α : Type u
f : Set α → α
hf : Injective f
⊢ False

Tactic:
exact cantor_injective f hf

Premises used: Function.cantor_injective
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
a b c : Cardinal.{u_1}
h : b ≤ c
pos : ∀ (ha : a = 0), a ^ b ≤ max (a ^ c) 1
neg : ∀ (ha : ¬a = 0), a ^ b ≤ max (a ^ c) 1
⊢ a ^ b ≤ max (a ^ c) 1

Tactic:
by_cases ha : a = 0
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
a b c : Cardinal.{u_1}
h : b ≤ c
ha : a = 0
⊢ a ^ b ≤ max (a ^ c) 1

Tactic:
simp [ha, zero_power_le]

Premises used: Cardinal.zero_power_le
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
a b c : Cardinal.{u_1}
h : b ≤ c
ha : ¬a = 0
⊢ a ^ b ≤ max (a ^ c) 1

Tactic:
(power_le_power_left ha h).trans (le_max_left _ _)

Premises used: LE.le.trans, le_max_left, Cardinal.power_le_power_left
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
a b c : Cardinal.{u_1}
h : b ≤ c
ha : ¬a = 0
⊢ a ^ b ≤ max (a ^ c) 1

Tactic:
exact (power_le_power_left ha h).trans (le_max_left _ _)

Premises used: LE.le.trans, le_max_left, Cardinal.power_le_power_left
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
a b c : Cardinal.{u_1}
⊢ a ≤ b → a ^ c ≤ b ^ c

Tactic:
inductionOn₃ a b c fun _ _ _ ⟨e⟩ => ⟨Embedding.arrowCongrRight e⟩

Premises used: Cardinal.inductionOn₃
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
a b : Cardinal.{u_1}
ha : 0 < a
⊢ 0 < a ^ b

Tactic:
(power_ne_zero _ ha.ne').bot_lt

Premises used: Cardinal.power_ne_zero, LT.lt.ne', Ne.bot_lt
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
a : Cardinal.{u}
h : ¬Acc (fun (x1 x2 : Cardinal.{u}) ↦ x1 < x2) a
ι : Type (max 0 (u + 1)) := { c : Cardinal.{u} // ¬Acc (fun (x1 x2 : Cardinal.{u}) ↦ x1 < x2) c }
f : ι → Cardinal.{u} := Subtype.val (p := fun (c : Cardinal.{u}) ↦ ¬Acc (fun (x1 x2 : Cardinal.{u}) ↦ x1 < x2) c)
⊢ Nonempty ι

Tactic:
haveI hι : Nonempty ι := ⟨⟨_, h⟩⟩
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
a : Cardinal.{u}
h : ¬Acc (fun (x1 x2 : Cardinal.{u}) ↦ x1 < x2) a
ι : Type (max 0 (u + 1)) := { c : Cardinal.{u} // ¬Acc (fun (x1 x2 : Cardinal.{u}) ↦ x1 < x2) c }
f : ι → Cardinal.{u} := Subtype.val (p := fun (c : Cardinal.{u}) ↦ ¬Acc (fun (x1 x2 : Cardinal.{u}) ↦ x1 < x2) c)
hι : Nonempty ι
obtain :
  ∀ (c : Cardinal.{u}) (hc : ¬Acc (fun (x1 x2 : Cardinal.{u}) ↦ x1 < x2) c)
    (h_1 :
      (j : ι) →
        Quotient.out
            (f (Subtype.mk (p := fun (c : Cardinal.{u}) ↦ ¬Acc (fun (x1 x2 : Cardinal.{u}) ↦ x1 < x2) c) c hc)) ↪
          Quotient.out (f j)),
    False
⊢ False

Tactic:
obtain ⟨⟨c : Cardinal, hc : ¬Acc (· < ·) c⟩, ⟨h_1 : ∀ j, (f ⟨c, hc⟩).out ↪ (f j).out⟩⟩ :=
        Embedding.min_injective fun i => (f i).out

Premises used: Cardinal, Quotient.out, Function.Embedding.min_injective
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
a : Cardinal.{u}
h : ¬Acc (fun (x1 x2 : Cardinal.{u}) ↦ x1 < x2) a
ι : Type (max 0 (u + 1)) := { c : Cardinal.{u} // ¬Acc (fun (x1 x2 : Cardinal.{u}) ↦ x1 < x2) c }
f : ι → Cardinal.{u} := Subtype.val (p := fun (c : Cardinal.{u}) ↦ ¬Acc (fun (x1 x2 : Cardinal.{u}) ↦ x1 < x2) c)
hι : Nonempty ι
c : Cardinal.{u}
hc : ¬Acc (fun (x1 x2 : Cardinal.{u}) ↦ x1 < x2) c
h_1 :
  (j : ι) →
    Quotient.out (f (Subtype.mk (p := fun (c : Cardinal.{u}) ↦ ¬Acc (fun (x1 x2 : Cardinal.{u}) ↦ x1 < x2) c) c hc)) ↪
      Quotient.out (f j)
⊢ False

Tactic:
hc (Acc.intro _ fun j h' => by_contradiction fun hj => h'.2 ?_)

Premises used: And.right, by_contradiction, Acc.intro
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
a : Cardinal.{u}
h : ¬Acc (fun (x1 x2 : Cardinal.{u}) ↦ x1 < x2) a
ι : Type (max 0 (u + 1)) := { c : Cardinal.{u} // ¬Acc (fun (x1 x2 : Cardinal.{u}) ↦ x1 < x2) c }
f : ι → Cardinal.{u} := Subtype.val (p := fun (c : Cardinal.{u}) ↦ ¬Acc (fun (x1 x2 : Cardinal.{u}) ↦ x1 < x2) c)
hι : Nonempty ι
c : Cardinal.{u}
hc : ¬Acc (fun (x1 x2 : Cardinal.{u}) ↦ x1 < x2) c
h_1 :
  (j : ι) →
    Quotient.out (f (Subtype.mk (p := fun (c : Cardinal.{u}) ↦ ¬Acc (fun (x1 x2 : Cardinal.{u}) ↦ x1 < x2) c) c hc)) ↪
      Quotient.out (f j)
refine : ∀ (j : Cardinal.{u}) (h' : j < c) (hj : ¬Acc (fun (x1 x2 : Cardinal.{u}) ↦ x1 < x2) j), c ≤ j
⊢ False

Tactic:
refine hc (Acc.intro _ fun j h' => by_contradiction fun hj => h'.2 ?_)

Premises used: And.right, by_contradiction, Acc.intro
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
a : Cardinal.{u}
h : ¬Acc (fun (x1 x2 : Cardinal.{u}) ↦ x1 < x2) a
ι : Type (max 0 (u + 1)) := { c : Cardinal.{u} // ¬Acc (fun (x1 x2 : Cardinal.{u}) ↦ x1 < x2) c }
f : ι → Cardinal.{u} := Subtype.val (p := fun (c : Cardinal.{u}) ↦ ¬Acc (fun (x1 x2 : Cardinal.{u}) ↦ x1 < x2) c)
hι : Nonempty ι
c : Cardinal.{u}
hc : ¬Acc (fun (x1 x2 : Cardinal.{u}) ↦ x1 < x2) c
h_1 :
  (j : ι) →
    Quotient.out (f (Subtype.mk (p := fun (c : Cardinal.{u}) ↦ ¬Acc (fun (x1 x2 : Cardinal.{u}) ↦ x1 < x2) c) c hc)) ↪
      Quotient.out (f j)
j : Cardinal.{u}
h' : j < c
hj : ¬Acc (fun (x1 x2 : Cardinal.{u}) ↦ x1 < x2) j
⊢ #(Quotient.out (f (Subtype.mk (p := fun (c : Cardinal.{u}) ↦ ¬Acc (fun (x1 x2 : Cardinal.{u}) ↦ x1 < x2) c) c hc))) ≤
    #(Quotient.out (f (Subtype.mk (p := fun (c : Cardinal.{u}) ↦ ¬Acc (fun (x1 x2 : Cardinal.{u}) ↦ x1 < x2) c) j hj)))

Tactic:
have : #_ ≤ #_ := ⟨h_1 ⟨j, hj⟩⟩
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
a : Cardinal.{u}
h : ¬Acc (fun (x1 x2 : Cardinal.{u}) ↦ x1 < x2) a
ι : Type (max 0 (u + 1)) := { c : Cardinal.{u} // ¬Acc (fun (x1 x2 : Cardinal.{u}) ↦ x1 < x2) c }
f : ι → Cardinal.{u} := Subtype.val (p := fun (c : Cardinal.{u}) ↦ ¬Acc (fun (x1 x2 : Cardinal.{u}) ↦ x1 < x2) c)
hι : Nonempty ι
c : Cardinal.{u}
hc : ¬Acc (fun (x1 x2 : Cardinal.{u}) ↦ x1 < x2) c
h_1 :
  (j : ι) →
    Quotient.out (f (Subtype.mk (p := fun (c : Cardinal.{u}) ↦ ¬Acc (fun (x1 x2 : Cardinal.{u}) ↦ x1 < x2) c) c hc)) ↪
      Quotient.out (f j)
j : Cardinal.{u}
h' : j < c
hj : ¬Acc (fun (x1 x2 : Cardinal.{u}) ↦ x1 < x2) j
this :
  #(Quotient.out (f (Subtype.mk (p := fun (c : Cardinal.{u}) ↦ ¬Acc (fun (x1 x2 : Cardinal.{u}) ↦ x1 < x2) c) c hc))) ≤
    #(Quotient.out (f (Subtype.mk (p := fun (c : Cardinal.{u}) ↦ ¬Acc (fun (x1 x2 : Cardinal.{u}) ↦ x1 < x2) c) j hj)))
⊢ c ≤ j

Tactic:
simpa only [mk_out] using this

Premises used: Cardinal.mk_out
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α β : Type u
⊢ WellFoundedLT Cardinal.{u}

Tactic:
⟨Cardinal.lt_wf⟩

Premises used: IsWellFounded.mk, Cardinal.lt_wf
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
⊢ Eq.{u + 2} (α := Cardinal.{u}) (sInf ∅) 0

Tactic:
dif_neg Set.not_nonempty_empty

Premises used: Set.not_nonempty_empty, dif_neg
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
c : Cardinal.{u_1}
⊢ succ c = sInf {c' : Cardinal.{u_1} | c < c'}

Tactic:
Order.succ_eq_csInf c

Premises used: Set.Ioi, setOf, Order.succ_eq_csInf
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
⊢ ∀ (c : Cardinal.{u_1}), 0 < succ c

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
c : Cardinal.{u_1}
⊢ succ c ≠ 0

Tactic:
(succ_pos _).ne'

Premises used: LT.lt.ne', Cardinal.succ_pos
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
a b : Cardinal.{u_1}
h : a < b
mk : ∀ (α β : Type u_1) (h : #α < #β), #α + 1 ≤ #β
⊢ a + 1 ≤ b

Tactic:
induction a, b using Cardinal.inductionOn₂ with | mk α β

Premises used: Cardinal.mk
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α β : Type u_1
h : #α < #β
mk : ∀ (f : α ↪ β), #α + 1 ≤ #β
⊢ #α + 1 ≤ #β

Tactic:
obtain ⟨f⟩ := h.le

Premises used: LT.lt.le
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α β : Type u_1
h : #α < #β
f : α ↪ β
⊢ ¬Surjective (α := α) (β := β) (⇑f : (a : α) → β)

Tactic:
have hf : ¬Surjective f := fun hn ↦ h.not_ge (mk_le_of_surjective hn)
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α β : Type u_1
h : #α < #β
f : α ↪ β
hf : ¬Surjective (α := α) (β := β) (⇑f : (a : α) → β)
⊢ ∃ (x : β), ¬∃ (a : α), (f : (a : α) → β) a = x

Tactic:
rw [Surjective, not_forall] at hf

Premises used: Classical.not_forall, Function.Surjective
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α β : Type u_1
h : #α < #β
f : α ↪ β
hf : ∃ (x : β), ¬∃ (a : α), (f : (a : α) → β) a = x
mk : ∀ (b : β) (hb : ¬∃ (a : α), (f : (a : α) → β) a = b), #α + 1 ≤ #β
⊢ #α + 1 ≤ #β

Tactic:
obtain ⟨b, hb⟩ := hf
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α β : Type u_1
h : #α < #β
f : α ↪ β
b : β
hb : ¬∃ (a : α), (f : (a : α) → β) a = b
mk : #(Option α) ≤ #β
⊢ #α + 1 ≤ #β

Tactic:
rw [← mk_option]

Premises used: Cardinal.mk_option
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α β : Type u_1
h : #α < #β
f : α ↪ β
b : β
hb : ¬∃ (a : α), (f : (a : α) → β) a = b
⊢ #(Option α) ≤ #β

Tactic:
(f.optionElim b hb).cardinal_le

Premises used: Function.Embedding.optionElim, Function.Embedding.cardinal_le
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α β : Type u_1
h : #α < #β
f : α ↪ β
b : β
hb : ¬∃ (a : α), (f : (a : α) → β) a = b
⊢ #(Option α) ≤ #β

Tactic:
exact (f.optionElim b hb).cardinal_le

Premises used: Function.Embedding.optionElim, Function.Embedding.cardinal_le
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
c : Cardinal.{u_1}
⊢ c + 1 ≤ succ c

Tactic:
add_one_le_of_lt (lt_succ c)

Premises used: Order.lt_succ, Cardinal.add_one_le_of_lt
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
a : Cardinal.{u}
apply : lift.{v, u} (succ a) ≤ succ (lift.{v, u} a)
⊢ lift.{v, u} (succ a) = succ (lift.{v, u} a)

Tactic:
apply (succ_le_of_lt <| lift_lt.2 <| lt_succ a).antisymm'

Premises used: Iff.mpr, LE.le.antisymm', Order.succ_le_of_lt, Order.lt_succ, Cardinal.lift_lt
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
a : Cardinal.{u}
by_contra! : ∀ (h : succ (lift.{v, u} a) < lift.{v, u} (succ a)), False
⊢ lift.{v, u} (succ a) ≤ succ (lift.{v, u} a)

Tactic:
by_contra! h
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
a : Cardinal.{u}
h : succ (lift.{v, u} a) < lift.{v, u} (succ a)
rcases : ∀ (b : Cardinal.{u}) (h : b < succ a) (hb : lift.{v, u} b = succ (lift.{v, u} a)), False
⊢ False

Tactic:
rcases lt_lift_iff.1 h with ⟨b, h, hb⟩

Premises used: Cardinal.lt_lift_iff, Iff.mp
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
a : Cardinal.{u}
h_1 : succ (lift.{v, u} a) < lift.{v, u} (succ a)
b : Cardinal.{u}
h : b < succ a
hb : lift.{v, u} b = succ (lift.{v, u} a)
⊢ succ (lift.{v, u} a) ≤ lift.{v, u} a

Tactic:
rw [lt_succ_iff, ← lift_le, hb] at h

Premises used: Order.lt_succ_iff, Cardinal.lift_le
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
a : Cardinal.{u}
h_1 : succ (lift.{v, u} a) < lift.{v, u} (succ a)
b : Cardinal.{u}
h : b < succ a
hb : lift.{v, u} b = succ (lift.{v, u} a)
h₁ : succ (lift.{v, u} a) ≤ lift.{v, u} a
⊢ lift.{v, u} b = succ (lift.{v, u} a)

Tactic:
rw [lt_succ_iff, ← lift_le, hb] at h

Premises used: Order.lt_succ_iff, Cardinal.lift_le
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
a : Cardinal.{u}
h_1 : succ (lift.{v, u} a) < lift.{v, u} (succ a)
b : Cardinal.{u}
h : succ (lift.{v, u} a) ≤ lift.{v, u} a
hb : lift.{v, u} b = succ (lift.{v, u} a)
⊢ False

Tactic:
h.not_gt (lt_succ _)

Premises used: Order.lt_succ, LE.le.not_gt
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
a : Cardinal.{u}
h_1 : succ (lift.{v, u} a) < lift.{v, u} (succ a)
b : Cardinal.{u}
h : succ (lift.{v, u} a) ≤ lift.{v, u} a
hb : lift.{v, u} b = succ (lift.{v, u} a)
⊢ False

Tactic:
exact h.not_gt (lt_succ _)

Premises used: Order.lt_succ, LE.le.not_gt
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
c : ℕ
h : IsSuccLimit c
⊢ c ≠ 0

Tactic:
h.ne_bot

Premises used: Order.IsSuccLimit.ne_bot
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
⊢ IsSuccPrelimit.{u_1 + 1} (α := Cardinal.{u_1}) 0

Tactic:
isSuccPrelimit_bot

Premises used: Order.isSuccPrelimit_bot
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
c : Cardinal.{u_1}
⊢ IsSuccLimit c ↔ c ≠ 0 ∧ IsSuccPrelimit c

Tactic:
isSuccLimit_iff_of_orderBot

Premises used: Order.isSuccLimit_iff_of_orderBot
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
⊢ ¬IsSuccLimit.{u_1 + 1} (α := Cardinal.{u_1}) 0

Tactic:
not_isSuccLimit_bot

Premises used: Order.not_isSuccLimit_bot
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
c : Cardinal.{u_1}
hc : c.IsStrongPrelimit
⊢ IsSuccPrelimit c

Tactic:
isSuccPrelimit_of_succ_lt fun x hx ↦ (succ_le_of_lt <| cantor x).trans_lt (hc hx)

Premises used: Order.succ_le_of_lt, Cardinal.cantor, LE.le.trans_lt, Order.isSuccPrelimit_of_succ_lt
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
c : Cardinal.{u_1}
hc : c.IsStrongLimit
rw : c ≠ 0 ∧ IsSuccPrelimit c
⊢ IsSuccLimit c

Tactic:
rw [Cardinal.isSuccLimit_iff]

Premises used: Cardinal.isSuccLimit_iff
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
c : Cardinal.{u_1}
hc : c.IsStrongLimit
⊢ c ≠ 0 ∧ IsSuccPrelimit c

Tactic:
⟨hc.ne_zero, hc.isStrongPrelimit.isSuccPrelimit⟩

Premises used: Cardinal.IsStrongPrelimit.isSuccPrelimit, Cardinal.IsStrongLimit.ne_zero, And.intro, Cardinal.IsStrongLimit.isStrongPrelimit
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
c : Cardinal.{u_1}
hc : c.IsStrongLimit
⊢ c ≠ 0 ∧ IsSuccPrelimit c

Tactic:
exact ⟨hc.ne_zero, hc.isStrongPrelimit.isSuccPrelimit⟩
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
c : Cardinal.{u_1}
H : c.IsStrongLimit
⊢ IsSuccPrelimit c

Tactic:
H.isSuccLimit.isSuccPrelimit

Premises used: Cardinal.IsStrongLimit.isSuccLimit, Order.IsSuccLimit.isSuccPrelimit
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
c : Cardinal.{u_1}
⊢ ¬c.IsStrongPrelimit ↔ ∃ x < c, c ≤ HPow.hPow (α := Cardinal.{u_1}) 2 x

Tactic:
simp [IsStrongPrelimit]

Premises used: Cardinal.IsStrongPrelimit
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
⊢ IsStrongPrelimit.{u_1} 0

Tactic:
simp [IsStrongPrelimit]

Premises used: Cardinal.IsStrongPrelimit
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
⊢ ¬IsStrongLimit.{u_1} 0

Tactic:
fun h ↦ h.ne_zero rfl

Premises used: Cardinal.IsStrongLimit.ne_zero, Not, rfl
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
ι : Type u
f : ι → Cardinal.{v}
i : ι
rw : lift.{u, v} ⟦Quotient.out (f i)⟧ ≤ sum f
⊢ lift.{u, v} (f i) ≤ sum f

Tactic:
rw [← Quotient.out_eq (f i)]

Premises used: Quotient.out_eq
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
ι : Type u
f : ι → Cardinal.{v}
i : ι
a b : ULift.{u, v} (Quotient.out (f i))
h :
  Eq (α := (i : ι) × Quotient.out (f i))
    ((fun (a : ULift.{u, v} (Quotient.out (f i))) ↦
        (Sigma.mk (β := fun (i : ι) ↦ Quotient.out (f i)) i a.down : (i : ι) × Quotient.out (f i)))
      a)
    ((fun (a : ULift.{u, v} (Quotient.out (f i))) ↦
        (Sigma.mk (β := fun (i : ι) ↦ Quotient.out (f i)) i a.down : (i : ι) × Quotient.out (f i)))
      b)
⊢ a = b

Tactic:
simpa using h
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
ι : Type u
f : ι → Cardinal.{v}
i : ι
⊢ lift.{u, v} ⟦Quotient.out (f i)⟧ ≤ sum f

Tactic:
exact ⟨⟨fun a => ⟨i, a.down⟩, fun a b h => by simpa using h⟩⟩
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
ι : Type u
f : ι → Cardinal.{max u v}
i : ι
⊢ f i ≤ sum f

Tactic:
simpa [← lift_umax] using lift_le_sum f i

Premises used: Cardinal.lift_umax, Cardinal.lift_le_sum
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
ι : Type u_1
f : ι → Cardinal.{max u_1 u_2}
⊢ iSup f ≤ sum f

Tactic:
ciSup_le' <| le_sum _

Premises used: Cardinal.le_sum, ciSup_le'
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
ι : Type u_1
f g : ι → Cardinal.{u_2}
⊢ #((i : ι) × ((Quotient.out ∘ f) i ⊕ (Quotient.out ∘ g) i)) =
    #((i : ι) × (Quotient.out ∘ f) i ⊕ (i : ι) × (Quotient.out ∘ g) i)

Tactic:
have := mk_congr (Equiv.sigmaSumDistrib (Quotient.out ∘ f) (Quotient.out ∘ g))
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
ι : Type u_1
f g : ι → Cardinal.{u_2}
this :
  #((i : ι) × ((Quotient.out ∘ f) i ⊕ (Quotient.out ∘ g) i)) =
    #((i : ι) × (Quotient.out ∘ f) i ⊕ (i : ι) × (Quotient.out ∘ g) i)
⊢ (sum.{u_1, u_2} fun (i : ι) ↦ f i + g i) = (sum.{u_1, u_2} fun (i : ι) ↦ f i) + sum.{u_1, u_2} fun (i : ι) ↦ g i

Tactic:
simp only [comp_apply, mk_sigma, mk_sum, mk_out, lift_id] at this

Premises used: Cardinal.mk_out, Cardinal.mk_sigma, Cardinal.mk_sum, Function.comp_apply, Cardinal.lift_id
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
ι : Type u_1
f g : ι → Cardinal.{u_2}
this : (sum.{u_1, u_2} fun (i : ι) ↦ f i + g i) = (sum.{u_1, u_2} fun (i : ι) ↦ f i) + sum.{u_1, u_2} fun (i : ι) ↦ g i
⊢ sum (f + g) = sum f + sum g

Tactic:
this