mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u}
⊢ lift.{v, u} o ≤ ω_ 1 ↔ o ≤ ω_ 1

Tactic:
simpa using

Goal state after:
o : Ordinal.{u}
⊢ lift.{v, u} o ≤ ω_ 1 ↔ o ≤ ω_ 1
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u}
⊢ ω_ 1 < lift.{v, u} o ↔ ω_ 1 < o

Tactic:
simpa using

Goal state after:
o : Ordinal.{u}
⊢ ω_ 1 < lift.{v, u} o ↔ ω_ 1 < o
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u}
⊢ lift.{v, u} o < ω_ 1 ↔ o < ω_ 1

Tactic:
simpa using

Goal state after:
o : Ordinal.{u}
⊢ lift.{v, u} o < ω_ 1 ↔ o < ω_ 1
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u}
⊢ ω_ 1 = lift.{v, u} o ↔ ω_ 1 = o

Tactic:
simpa using

Goal state after:
o : Ordinal.{u}
⊢ ω_ 1 = lift.{v, u} o ↔ ω_ 1 = o
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u}
n : ℕ
⊢ ω_ ↑n ≤ lift.{v, u} o ↔ ω_ ↑n ≤ o

Tactic:
simpa using

Goal state after:
o : Ordinal.{u}
n : ℕ
⊢ ω_ ↑n ≤ lift.{v, u} o ↔ ω_ ↑n ≤ o
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u}
n : ℕ
⊢ lift.{v, u} o ≤ ω_ ↑n ↔ o ≤ ω_ ↑n

Tactic:
simpa using

Goal state after:
o : Ordinal.{u}
n : ℕ
⊢ lift.{v, u} o ≤ ω_ ↑n ↔ o ≤ ω_ ↑n
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u}
n : ℕ
⊢ ω_ ↑n < lift.{v, u} o ↔ ω_ ↑n < o

Tactic:
simpa using

Goal state after:
o : Ordinal.{u}
n : ℕ
⊢ ω_ ↑n < lift.{v, u} o ↔ ω_ ↑n < o
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: β : Type v
o : Ordinal.{u}
c : Cardinal.{v}
ho : lift.{v, u} o.card ≤ lift.{u, v} c
hc : ℵ₀ ≤ c
A : Ordinal.{u} → Set β
hA : ∀ j < o, #↑(A j) ≤ c
i : o.ToType
⊢ lift.{u, v} #↑(((fun x ↦ A ↑x) ∘ ⇑ToType.mk.symm) i) ≤ lift.{u, v} c

Tactic:
simpa using

Goal state after:
β : Type v
o : Ordinal.{u}
c : Cardinal.{v}
ho : lift.{v, u} o.card ≤ lift.{u, v} c
hc : ℵ₀ ≤ c
A : Ordinal.{u} → Set β
hA : ∀ j < o, #↑(A j) ≤ c
i : o.ToType
⊢ #↑(A ↑(ToType.mk.symm i)) ≤ c
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u}
n : ℕ
⊢ lift.{v, u} o < ω_ ↑n ↔ o < ω_ ↑n

Tactic:
simpa using

Goal state after:
o : Ordinal.{u}
n : ℕ
⊢ lift.{v, u} o < ω_ ↑n ↔ o < ω_ ↑n
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u}
n : ℕ
⊢ ω_ ↑n = lift.{v, u} o ↔ ω_ ↑n = o

Tactic:
simpa using

Goal state after:
o : Ordinal.{u}
n : ℕ
⊢ ω_ ↑n = lift.{v, u} o ↔ ω_ ↑n = o
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: o : Ordinal.{u}
f : ↑(Iio o) → Ordinal.{max u v}
⊢ ⨆ i, f i.toOrd = ⨆ a, f a

Tactic:
simpa using

Goal state after:
o : Ordinal.{u}
f : ↑(Iio o) → Ordinal.{max u v}
⊢ ⨆ i, f i.toOrd = ⨆ a, f a
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: case pos
ι : Type u
f : ι → Ordinal.{v}
n : ℕ
hι : Cardinal.lift.{v, u} #ι ≤ Cardinal.lift.{u, v} ↑n
hf : ∀ (i : ι), (f i).card ≤ ↑n
hc : ↑n < ℵ₀
i : ι
⊢ f i ≤ ↑n

Tactic:
simpa using

Goal state after:
case pos
ι : Type u
f : ι → Ordinal.{v}
n : ℕ
hι : Cardinal.lift.{v, u} #ι ≤ Cardinal.lift.{u, v} ↑n
hf : ∀ (i : ι), (f i).card ≤ ↑n
hc : ↑n < ℵ₀
i : ι
⊢ f i ≤ ↑n
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: ι : Type u_1
c : Cardinal.{u_1}
f : ι → Ordinal.{u_1}
hι : Cardinal.lift.{?u.23, u_1} #ι ≤ Cardinal.lift.{?u.23, u_1} c
hf : ∀ (i : ι), (f i).card ≤ c
⊢ (⨆ i, f i).card ≤ c

Tactic:
simpa using

Goal state after:
ι : Type u_1
c : Cardinal.{u_1}
f : ι → Ordinal.{u_1}
hι : Cardinal.lift.{?u.23, u_1} #ι ≤ Cardinal.lift.{?u.23, u_1} c
hf : ∀ (i : ι), (f i).card ≤ c
⊢ (⨆ i, f i).card ≤ c
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: β : Type v
f : β → Ordinal.{u}
a : Ordinal.{u}
ha : Cardinal.lift.{u + 1, max u v} (Cardinal.lift.{u, v} #β) < Cardinal.lift.{u + 1, max u v} (lift.{v, u} a).cof
hf : ∀ (i : β), f i < a
⊢ Cardinal.lift.{u + 1, v} #β < Cardinal.lift.{v, u + 1} (lift.{u + 1, u} a).cof

Tactic:
simpa using

Goal state after:
β : Type v
f : β → Ordinal.{u}
a : Ordinal.{u}
ha : Cardinal.lift.{u + 1, max u v} (Cardinal.lift.{u, v} #β) < Cardinal.lift.{u + 1, max u v} (lift.{v, u} a).cof
hf : ∀ (i : β), f i < a
⊢ Cardinal.lift.{u + 1, v} #β < Cardinal.lift.{max (u + 1) v, u} a.cof
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: α : Type u
f : α → Ordinal.{u}
a : Ordinal.{u}
ha : Cardinal.lift.{u, u} #α < (lift.{u, u} a).cof
hf : ∀ (i : α), f i < a
⊢ ⨆ i, f i + 1 < a

Tactic:
simpa using

Goal state after:
α : Type u
f : α → Ordinal.{u}
a : Ordinal.{u}
ha : Cardinal.lift.{u, u} #α < (lift.{u, u} a).cof
hf : ∀ (i : α), f i < a
⊢ ⨆ i, f i + 1 < a
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: α : Type u
f : α → Ordinal.{u}
a : Ordinal.{u}
ha : Cardinal.lift.{u, u} #α < (lift.{u, u} a).cof
hf : ∀ (i : α), f i < a
⊢ ⨆ i, f i < a

Tactic:
simpa using

Goal state after:
α : Type u
f : α → Ordinal.{u}
a : Ordinal.{u}
ha : Cardinal.lift.{u, u} #α < (lift.{u, u} a).cof
hf : ∀ (i : α), f i < a
⊢ ⨆ i, f i < a
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: a✝ : Ordinal.{?u.2}
b : Ordinal.{?u.4}
o✝ : Ordinal.{?u.6}
a o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
i : Ordinal.{u}
hi : i < a.cof.ord
⊢ a.cof.ord ≤ o

Tactic:
hf.cof_eq

Goal state after:
a✝ : Ordinal.{?u.2}
b : Ordinal.{?u.4}
o✝ : Ordinal.{?u.6}
a o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
i : Ordinal.{u}
hi : i < a.cof.ord
⊢ o ≤ o
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
c : Cardinal.{u_1}
f : ↑(Iio o) → Ordinal.{u_1}
hι : Cardinal.lift.{?u.27, u_1} o.card ≤ Cardinal.lift.{?u.27, u_1} c
hf : ∀ (i : ↑(Iio o)), (f i).card ≤ c
⊢ (⨆ i, f i).card ≤ c

Tactic:
simpa using

Goal state after:
o : Ordinal.{u_1}
c : Cardinal.{u_1}
f : ↑(Iio o) → Ordinal.{u_1}
hι : Cardinal.lift.{?u.27, u_1} o.card ≤ Cardinal.lift.{?u.27, u_1} c
hf : ∀ (i : ↑(Iio o)), (f i).card ≤ c
⊢ (⨆ i, f i).card ≤ c
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: α : Type u
f : α → Ordinal.{u}
⊢ (⨆ i, f i + 1).cof ≤ #α

Tactic:
simpa using

Goal state after:
α : Type u
f : α → Ordinal.{u}
⊢ (⨆ i, f i + 1).cof ≤ #α
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: case zero
a : Ordinal.{u_1}
ha : ω ≤ a
⊢ (a ^ 0).card ≤ max a.card (card 0)

Tactic:
simpa using

Goal state after:
case zero
a : Ordinal.{u_1}
ha : ω ≤ a
⊢ 1 ≤ a
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: case refine_1
a o o' : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
g : (b : Ordinal.{u}) → b < o' → Ordinal.{u}
hg : o.IsFundamentalSequence o' g
⊢ o' ≤ a.cof.ord

Tactic:
hf.cof_eq

Goal state after:
case refine_1
a o o' : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
g : (b : Ordinal.{u}) → b < o' → Ordinal.{u}
hg : o.IsFundamentalSequence o' g
⊢ o' ≤ o
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a b c : Cardinal.{u_1}
hc : c < ℵ₀
⊢ c + a < c + b ↔ a < b

Tactic:
simpa using

Goal state after:
a b c : Cardinal.{u_1}
hc : c < ℵ₀
⊢ a + c < b + c ↔ a < b
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: ι : Type u
f : ι → Ordinal.{max u v}
H : ∀ (i : ι), f i < iSup f
hf : Cardinal.lift.{v, u} #ι < (iSup f).cof
⊢ False

Tactic:
apply (lift_iSup_lt_of_lt_cof _ H).false

Goal state after:
ι : Type u
f : ι → Ordinal.{max u v}
H : ∀ (i : ι), f i < iSup f
hf : Cardinal.lift.{v, u} #ι < (iSup f).cof
⊢ Cardinal.lift.{max u v, u} #ι < (lift.{u, max u v} (iSup f)).cof
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case inr.hbc
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hfin : κ₂ + μ₂ < ℵ₀
hfin_ : κ₂ < ℵ₀ ∧ μ₂ < ℵ₀
⊢ κ₂ + μ₁ < κ₂ + μ₂

Tactic:
simpa using

Goal state after:
case inr.hbc
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hfin : κ₂ + μ₂ < ℵ₀
hfin_ : κ₂ < ℵ₀ ∧ μ₂ < ℵ₀
⊢ κ₂ + μ₁ < κ₂ + μ₂
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: f : Ordinal.{u_1} → Ordinal.{u_1}
c : Ordinal.{u_1}
hc : ℵ₀ < c.cof
hf : ∀ i < c, f i < c
a : Ordinal.{u_1}
⊢ Cardinal.lift.{u_1, 0} #Unit < c.cof

Tactic:
simpa using

Goal state after:
f : Ordinal.{u_1} → Ordinal.{u_1}
c : Ordinal.{u_1}
hc : ℵ₀ < c.cof
hf : ∀ i < c, f i < c
a : Ordinal.{u_1}
⊢ 1 < c.cof
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: n : ℕ
hn : n ≠ 0
x✝¹ x✝ : Cardinal.{u_1}
hlt : x✝¹ < x✝
⊢ (fun a ↦ a * ↑n) x✝¹ < (fun a ↦ a * ↑n) x✝

Tactic:
simpa using

Goal state after:
n : ℕ
hn : n ≠ 0
x✝¹ x✝ : Cardinal.{u_1}
hlt : x✝¹ < x✝
⊢ x✝¹ * ↑n < x✝ * ↑n
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: b : Ordinal.{u}
a : Cardinal.{u}
H : ∀ {ι : Type u} (f : ι → Ordinal.{u}), lsub f = b → a ≤ #ι
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{u}
hf : o.blsub f = b
⊢ a ≤ o.card

Tactic:
simpa using

Goal state after:
b : Ordinal.{u}
a : Cardinal.{u}
H : ∀ {ι : Type u} (f : ι → Ordinal.{u}), lsub f = b → a ≤ #ι
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{u}
hf : o.blsub f = b
⊢ a ≤ o.card
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: b : Ordinal.{u}
a : Cardinal.{u}
H : ∀ {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), o.blsub f = b → a ≤ o.card
ι : Type u
f : ι → Ordinal.{u}
r : ι → ι → Prop
hr : IsWellOrder ι r
hf : (type r).blsub (bfamilyOfFamily' r f) = b
hι' : (#ι).ord = type r
⊢ a ≤ #ι

Tactic:
simpa using

Goal state after:
b : Ordinal.{u}
a : Cardinal.{u}
H : ∀ {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), o.blsub f = b → a ≤ o.card
ι : Type u
f : ι → Ordinal.{u}
r : ι → ι → Prop
hr : IsWellOrder ι r
hf : (type r).blsub (bfamilyOfFamily' r f) = b
hι' : (#ι).ord = type r
⊢ a ≤ #ι
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
c : Ordinal.{max u v}
ho : Cardinal.lift.{v, u} o.card < c.cof
hf : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi < c
h : o.blsub f = c
⊢ c.cof ≤ Cardinal.lift.{v, u} o.card

Tactic:
simpa using

Goal state after:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
c : Ordinal.{max u v}
ho : Cardinal.lift.{v, u} o.card < c.cof
hf : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi < c
h : o.blsub f = c
⊢ c.cof ≤ (lift.{v, u} o).card
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
c : Ordinal.{max u v}
ho : Cardinal.lift.{v, u} o.card < c.cof
hf : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi < c
h : o.blsub f = c
⊢ c.cof ≤ Cardinal.lift.{v, u} o.card

Tactic:
simpa [← iSup_ord, hf, h] using cof_blsub_le_lift.{u, v} f

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{u}
c : Ordinal.{u}
ho : o.card < c.cof
hf : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi < c
⊢ Cardinal.lift.{u, u} o.card < c.cof

Tactic:
o.card.lift_id

Goal state after:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{u}
c : Ordinal.{u}
ho : o.card < c.cof
hf : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi < c
⊢ o.card < c.cof
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{u}
c : Ordinal.{u}
ho : o.card < c.cof
⊢ Cardinal.lift.{u, u} o.card < c.cof

Tactic:
o.card.lift_id

Goal state after:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{u}
c : Ordinal.{u}
ho : o.card < c.cof
⊢ o.card < c.cof
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: o : Ordinal.{u_1}
H : (ℵ_ o).IsRegular
⊢ (ℵ_ o).ord.cof = ℵ_ o

Tactic:
H.cof_ord

Goal state after:
o : Ordinal.{u_1}
H : (ℵ_ o).IsRegular
⊢ ℵ_ o = ℵ_ o
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ (succ c).IsRegular

Tactic:
have hc₀ := hc.trans (le_succ c)

Goal state after:
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
hc₀ : ℵ₀ ≤ succ c
⊢ (succ c).IsRegular
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: case le_cof_ord.refine_1
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
hc₀ : ℵ₀ ≤ succ c
hc' : (succ c).ord.cof < succ c
f : ↑(Iio (succ c).ord.cof.ord) → ↑(Iio (succ c).ord)
hf : IsFundamentalSeq f
⊢ (succ c).ord.cof.ord.card ≤ c

Tactic:
simpa using

Goal state after:
case le_cof_ord.refine_1
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
hc₀ : ℵ₀ ≤ succ c
hc' : (succ c).ord.cof < succ c
f : ↑(Iio (succ c).ord.cof.ord) → ↑(Iio (succ c).ord)
hf : IsFundamentalSeq f
⊢ (succ c).ord.cof ≤ c
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: ⊢ (ω_ 1).cof = ℵ_ 1

Tactic:
simpa using

Goal state after:
⊢ (ω_ 1).cof = ℵ_ 1
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: κ : Cardinal.{v}
x✝ : (lift.{u, v} κ).IsRegular
h₁ : ℵ₀ ≤ lift.{u, v} κ
h₂ : lift.{u, v} κ ≤ (lift.{u, v} κ).ord.cof
⊢ ℵ₀ ≤ κ

Tactic:
simpa using

Goal state after:
κ : Cardinal.{v}
x✝ : (lift.{u, v} κ).IsRegular
h₁ : ℵ₀ ≤ lift.{u, v} κ
h₂ : lift.{u, v} κ ≤ (lift.{u, v} κ).ord.cof
⊢ ℵ₀ ≤ κ
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a : Cardinal.{u}
ha : a ≤ ℵ₀
b : ℕ
⊢ a ^ ↑b ≤ ℵ₀

Tactic:
simpa using

Goal state after:
a : Cardinal.{u}
ha : a ≤ ℵ₀
b : ℕ
⊢ a ^ b ≤ ℵ₀
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u
β' : Type v
⊢ #(α ≃ β') = 0 ↔ lift.{v, u} #α ≠ lift.{u, v} #β'

Tactic:
mk_eq_zero_iff,

Goal state after:
α : Type u
β' : Type v
⊢ IsEmpty (α ≃ β') ↔ lift.{v, u} #α ≠ lift.{u, v} #β'
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u
β' : Type v
⊢ #(α ↪ β') = 0 ↔ lift.{u, v} #β' < lift.{v, u} #α

Tactic:
mk_eq_zero_iff,

Goal state after:
α : Type u
β' : Type v
⊢ IsEmpty (α ↪ β') ↔ lift.{u, v} #β' < lift.{v, u} #α
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u
β' : Type v
⊢ #(α → β') = 0 ↔ #α ≠ 0 ∧ #β' = 0

Tactic:
mk_eq_zero_iff,

Goal state after:
α : Type u
β' : Type v
⊢ IsEmpty (α → β') ↔ #α ≠ 0 ∧ IsEmpty β'
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case a.refine_2
α : Type u_1
h : (#α).IsStrongPrelimit
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha✝ : #α ≠ 0
h' : (#α).IsStrongLimit
ha : ℵ₀ ≤ #α
a b : α
hab : (fun x ↦ ⟨{x}, ⋯⟩) a = (fun x ↦ ⟨{x}, ⋯⟩) b
⊢ a = b

Tactic:
simpa using

Goal state after:
case a.refine_2
α : Type u_1
h : (#α).IsStrongPrelimit
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha✝ : #α ≠ 0
h' : (#α).IsStrongLimit
ha : ℵ₀ ≤ #α
a b : α
hab : (fun x ↦ ⟨{x}, ⋯⟩) a = (fun x ↦ ⟨{x}, ⋯⟩) b
⊢ a = b
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u
β' : Type v
⊢ Nonempty ↑{f | Surjective f} ↔ (#α = 0 ∨ Nonempty β') ∧ Nonempty (β' ↪ α)

Tactic:
mk_eq_zero_iff,

Goal state after:
α : Type u
β' : Type v
⊢ Nonempty ↑{f | Surjective f} ↔ (IsEmpty α ∨ Nonempty β') ∧ Nonempty (β' ↪ α)
Module: Mathlib.SetTheory.Cardinal.Pigeonhole

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Infinite β
f : α → Finset β
w : ⋃ a, ↑(f a) = Set.univ
h : #↑(range f) < #β
b : β
⊢ ∃ a, b ∈ f a

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Infinite β
f : α → Finset β
w : ⋃ a, ↑(f a) = Set.univ
h : #↑(range f) < #β
b : β
⊢ ∃ a, b ∈ f a
Module: Mathlib.SetTheory.Cardinal.Pigeonhole

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Infinite β
f : α → Finset β
w : ⋃ a, ↑(f a) = Set.univ
h : #↑(range f) < #β
u : ∀ (b : β), ∃ a, b ∈ f a :=
  fun b ↦
    Eq.mp (Eq.trans mem_iUnion._simp_1 (congrArg Exists (funext fun i ↦ SetLike.mem_coe._simp_1)))
      (Eq.ge w (mem_univ b))
u' : β → ↑(range f) := fun b ↦ ⟨f ⋯.choose, ⋯⟩
a : α
p : β
m : p ∈ u' ⁻¹' {⟨f a, ⋯⟩}
⊢ f ⋯.choose = f a

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Infinite β
f : α → Finset β
w : ⋃ a, ↑(f a) = Set.univ
h : #↑(range f) < #β
u : ∀ (b : β), ∃ a, b ∈ f a :=
  fun b ↦
    Eq.mp (Eq.trans mem_iUnion._simp_1 (congrArg Exists (funext fun i ↦ SetLike.mem_coe._simp_1)))
      (Eq.ge w (mem_univ b))
u' : β → ↑(range f) := fun b ↦ ⟨f ⋯.choose, ⋯⟩
a : α
p : β
m : p ∈ u' ⁻¹' {⟨f a, ⋯⟩}
⊢ f ⋯.choose = f a
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case a.refine_2
α : Type u_1
h : (#α).IsStrongPrelimit
ha : #α ≠ 0
h' : (#α).IsStrongLimit
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := linearOrderOfSTO r
a b : α
hab : (fun x ↦ ⟨{x}, ⋯⟩) a = (fun x ↦ ⟨{x}, ⋯⟩) b
⊢ a = b

Tactic:
simpa using

Goal state after:
case a.refine_2
α : Type u_1
h : (#α).IsStrongPrelimit
ha : #α ≠ 0
h' : (#α).IsStrongLimit
r : α → α → Prop
wo : IsWellOrder α r
hr : (#α).ord = type r
this : LinearOrder α := linearOrderOfSTO r
a b : α
hab : (fun x ↦ ⟨{x}, ⋯⟩) a = (fun x ↦ ⟨{x}, ⋯⟩) b
⊢ a = b
Module: Mathlib.LinearAlgebra.Basis.Cardinality

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Nontrivial R
inst✝ : Module R M
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
ind : LinearIndependent R v
m : ind.Maximal
i : ι
w : ∀ (x : κ), (b.repr (v x)) i = 0
repr_eq_zero : ∀ (l : κ →₀ R), (b.repr ((linearCombination R v) l)) i = 0
v' : Option κ → M := fun o ↦ o.elim (b i) v
r : range v ⊆ range v'
x✝ : b i ∈ range v
k : κ
p : v k = b i
⊢ False

Tactic:
simpa using

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Nontrivial R
inst✝ : Module R M
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
ind : LinearIndependent R v
m : ind.Maximal
i : ι
w : ∀ (x : κ), (b.repr (v x)) i = 0
repr_eq_zero : ∀ (l : κ →₀ R), (b.repr ((linearCombination R v) l)) i = 0
v' : Option κ → M := fun o ↦ o.elim (b i) v
r : range v ⊆ range v'
x✝ : b i ∈ range v
k : κ
p : v k = b i
⊢ False
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: case limit.ha
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
hω : ℵ₀ < c.ord.cof
b : Ordinal.{max u v}
hb : IsSuccLimit b
H : ∀ o' < b, o' < c.ord → derivFamily f o' < c.ord
hb' : b < c.ord
⊢ lift.{max u v, max (u + 1) (v + 1)} #↑(Iio b) < lift.{max (u + 1) (v + 1), max u v} c.ord.cof

Tactic:
hc.cof_ord,

Goal state after:
case limit.ha
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
hω : ℵ₀ < c.ord.cof
b : Ordinal.{max u v}
hb : IsSuccLimit b
H : ∀ o' < b, o' < c.ord → derivFamily f o' < c.ord
hb' : b < c.ord
⊢ lift.{max u v, max (u + 1) (v + 1)} #↑(Iio b) < lift.{max (u + 1) (v + 1), max u v} c
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
c : Cardinal.{u}
hc : c.IsRegular
hc' : c ≠ ℵ₀
hf : ∀ i < c.ord, f i < c.ord
a : Ordinal.{u}
⊢ lift.{u, 0} #Unit < c

Tactic:
simpa using

Goal state after:
f : Ordinal.{u} → Ordinal.{u}
c : Cardinal.{u}
hc : c.IsRegular
hc' : c ≠ ℵ₀
hf : ∀ i < c.ord, f i < c.ord
a : Ordinal.{u}
⊢ 1 < c
Module: Mathlib.LinearAlgebra.Basis.Cardinality

Goal state before:
pp: case none
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Nontrivial R
inst✝ : Module R M
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
ind : LinearIndependent R v
m : ind.Maximal
i : ι
w : ∀ (x : κ), (b.repr (v x)) i = 0
repr_eq_zero : ∀ (l : κ →₀ R), (b.repr ((linearCombination R v) l)) i = 0
v' : Option κ → M := fun o ↦ o.elim (b i) v
r : range v ⊆ range v'
r' : b i ∉ range v
r'' : range v ≠ range v'
l l' : Option κ →₀ R
z : l none • b i + (linearCombination R v) l.some = l' none • b i + (linearCombination R v) l'.some
⊢ l none = l' none

Tactic:
simpa using

Goal state after:
case none
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Nontrivial R
inst✝ : Module R M
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
ind : LinearIndependent R v
m : ind.Maximal
i : ι
w : ∀ (x : κ), (b.repr (v x)) i = 0
repr_eq_zero : ∀ (l : κ →₀ R), (b.repr ((linearCombination R v) l)) i = 0
v' : Option κ → M := fun o ↦ o.elim (b i) v
r : range v ⊆ range v'
r' : b i ∉ range v
r'' : range v ≠ range v'
l l' : Option κ →₀ R
z : l none • b i + (linearCombination R v) l.some = l' none • b i + (linearCombination R v) l'.some
⊢ l none = l' none
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: ⊢ preBeth Ordinal.univ.{u, v} = univ.{u, v}

Tactic:
simpa using

Goal state after:
⊢ preBeth Ordinal.univ.{u, v} = univ.{u, v}
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: ⊢ ℶ_ Ordinal.univ.{u, v} = univ.{u, v}

Tactic:
simpa using

Goal state after:
⊢ ℶ_ Ordinal.univ.{u, v} = univ.{u, v}
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: ⊢ preAleph Ordinal.univ.{u, v} = univ.{u, v}

Tactic:
simpa using

Goal state after:
⊢ preAleph Ordinal.univ.{u, v} = univ.{u, v}
Module: Mathlib.LinearAlgebra.Basis.Cardinality

Goal state before:
pp: case inr
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Nontrivial R
inst✝ : Module R M
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
ind : LinearIndependent R v
m : ind.Maximal
i : ι
w : ∀ (x : κ), (b.repr (v x)) i = 0
repr_eq_zero : ∀ (l : κ →₀ R), (b.repr ((linearCombination R v) l)) i = 0
v' : Option κ → M := fun o ↦ o.elim (b i) v
r : range v ⊆ range v'
r' : b i ∉ range v
r'' : range v ≠ range v'
l l' : Option κ →₀ R
z : l none • b i + (linearCombination R v) l.some = l' none • b i + (linearCombination R v) l'.some
a : κ
j : ι
ne : i ≠ j
⊢ (b.repr ((linearCombination R v) l.some)) j = (b.repr ((linearCombination R v) l'.some)) j

Tactic:
simpa using

Goal state after:
case inr
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Nontrivial R
inst✝ : Module R M
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
ind : LinearIndependent R v
m : ind.Maximal
i : ι
w : ∀ (x : κ), (b.repr (v x)) i = 0
repr_eq_zero : ∀ (l : κ →₀ R), (b.repr ((linearCombination R v) l)) i = 0
v' : Option κ → M := fun o ↦ o.elim (b i) v
r : range v ⊆ range v'
r' : b i ∉ range v
r'' : range v ≠ range v'
l l' : Option κ →₀ R
z : l none • b i + (linearCombination R v) l.some = l' none • b i + (linearCombination R v) l'.some
a : κ
j : ι
ne : i ≠ j
⊢ (b.repr ((linearCombination R v) l.some)) j = (b.repr ((linearCombination R v) l'.some)) j
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: ⊢ ℵ_ Ordinal.univ.{u, v} = univ.{u, v}

Tactic:
simpa using

Goal state after:
⊢ ℵ_ Ordinal.univ.{u, v} = univ.{u, v}
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: ⊢ preOmega Ordinal.univ.{u, v} = Ordinal.univ.{u, v}

Tactic:
simpa using

Goal state after:
⊢ preOmega Ordinal.univ.{u, v} = Ordinal.univ.{u, v}
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: ⊢ ω_ Ordinal.univ.{u, v} = Ordinal.univ.{u, v}

Tactic:
simpa using

Goal state after:
⊢ ω_ Ordinal.univ.{u, v} = Ordinal.univ.{u, v}
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : #↑s < #α
h : Nonempty (α ≃ β)
val✝ : Infinite α
⊢ ∃ g, ∀ (x : ↑s), g ↑x = f x

Tactic:
· apply extend_function f
    obtain ⟨g⟩ := id h
    have := Infinite.of_injective _ g.injective
    rw [← lift_mk_eq'] at h ⊢
    rwa [mk_compl_of_infinite s hs, mk_compl_of_infinite]
    rwa [← lift_lt, mk_range_eq_of_injective f.injective, ← h, lift_lt]

Goal state after:
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), β i
i i✝ : ι
⊢ (if i = i✝ then f i✝ else 0) = (single i (f i)) i✝

Tactic:
single_apply

Goal state after:
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), β i
i i✝ : ι
⊢ (if i = i✝ then f i✝ else 0) = if h : i = i✝ then Eq.recOn h (f i) else 0