mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: n : ℕ
a : Ordinal.{u_4}
ha : a < ↑n + ω
m : ℕ
hb' : ↑m < ω
hb : a ≤ ↑n + ↑m
⊢ ↑n + ↑m < ω

Tactic:
exact_mod_cast natCast_lt_omega0 (n + m)

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case pos
x : Ordinal.{u_1}
h : 1 ≤ 1
h✝ : 1 ∈ Iic x
⊢ sSup univ = 0

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case neg
x : Ordinal.{u_1}
h : 1 ≤ 1
h✝ : 1 ∉ Iic x
⊢ sSup ∅ = 0

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: x : Ordinal.{u_1}
⊢ log 0 x = 0

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: x : Ordinal.{u_1}
⊢ log 1 x = 0

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case isSuccPrelimit
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a : Ordinal.{u_1}
ha : c ≤ a.card + 1
⊢ ℵ₀ ≤ a.card + 1

pp: case isSuccPrelimit
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a : Ordinal.{u_1}
ha : c ≤ a.card + 1
⊢ IsSuccLimit ℵ₀.ord

Tactic:
· exact hc.trans ha

Goal state after:
case isSuccPrelimit
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a : Ordinal.{u_1}
ha : c ≤ a.card + 1
⊢ IsSuccLimit ℵ₀.ord
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case isSuccPrelimit
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a : Ordinal.{u_1}
ha : c ≤ a.card + 1
⊢ IsSuccLimit ℵ₀.ord

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inl
b n : ℕ
⊢ clog (b ^ 0) n = (clog b n + (0 - 1)) / 0

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inr
b : Ordinal.{u_1}
hb : 1 < b
x : Ordinal.{u_1}
hx : x ≠ 0
⊢ x < b ^ succ (log b x)

Tactic:
rw [lt_opow_iff_log_lt hb hx, lt_succ_iff]

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: ⊢ Nonempty ℵ₀.ord.ToType

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case add_one.inl
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
ha : ∀ (i : ι), f i a ≤ a
o : Ordinal.{u}
IH : a ≤ derivFamily f o → ∃ o, derivFamily f o = a
h₁ : a ≤ derivFamily f (o + 1)
h : a ≤ derivFamily f o
⊢ ∃ o, derivFamily f o = a

pp: case add_one.inr
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
ha : ∀ (i : ι), f i a ≤ a
o : Ordinal.{u}
IH : a ≤ derivFamily f o → ∃ o, derivFamily f o = a
h₁ : a ≤ derivFamily f (o + 1)
h : derivFamily f o < a
⊢ ∃ o, derivFamily f o = a

Tactic:
· exact IH h

Goal state after:
case add_one.inr
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
ha : ∀ (i : ι), f i a ≤ a
o : Ordinal.{u}
IH : a ≤ derivFamily f o → ∃ o, derivFamily f o = a
h₁ : a ≤ derivFamily f (o + 1)
h : derivFamily f o < a
⊢ ∃ o, derivFamily f o = a
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: a : Ordinal.{u_1}
ha : a ≠ 0
⊢ a - ω ^ log ω a < a

Tactic:
obtain ⟨n, hn⟩ := lt_omega0.1 <| div_opow_log_lt a one_lt_omega0

Goal state after:
a : Ordinal.{u_1}
ha : a ≠ 0
n : ℕ
hn : a / ω ^ log ω a = ↑n
⊢ a - ω ^ log ω a < a
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
⊢ derivFamily f = enumOrd (⋂ i, fixedPoints (f i))

Tactic:
by
  rw [eq_comm, eq_enumOrd _ (not_bddAbove_fp_family H)]
  use (isNormal_derivFamily f).strictMono
  rw [Set.range_eq_iff]
  refine ⟨?_, fun a ha => ?_⟩
  · rintro a S ⟨i, hi⟩
    rw [← hi]
    exact derivFamily_fp (H i) a
  rw [Set.mem_iInter] at ha
  rwa [← fp_iff_derivFamily H]

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
s : Set Ordinal.{u_1}
H : ∀ x ∈ s, IsPrincipal op x
⊢ IsPrincipal op (sSup ∅)

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case succ
a : Ordinal.{u_1}
ha : a ≠ 0
n : ℕ
hn : a / ω ^ log ω a = ↑(n + 1)
⊢ ↑n + 1 ≤ ↑(n + 1)

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case succ
a : Ordinal.{u_1}
ha : a ≠ 0
n : ℕ
hn : a / ω ^ log ω a = ↑(n + 1)
⊢ ω ^ log ω a ≠ 0

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: m : ℕ
⊢ ↑(m ^ 0) = ↑m ^ 0

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: m : ℕ
⊢ ∀ (n : ℕ), ↑(m ^ n) = ↑m ^ ↑n

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inr
ho : 0 < 1
⊢ ⨆ n, 1 ^ n = 1 ^ ω

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: m : ℕ
hm : 1 < m
⊢ ↑(Nat.log m 0) = log ↑m ↑0

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case succ
a : Ordinal.{u_1}
n✝ : ℕ
⊢ (0 ∘ 0^[n✝]) a ≤ 0^[0] a

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: a : Ordinal.{u_1}
ha : 0 < a
⊢ ⨆ n, (fun x ↦ a * x)^[n] 1 = ⨆ n, a ^ n

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: a : Ordinal.{u_1}
⊢ ∀ (n : ℕ), (fun x ↦ a * x)^[n] 0 ≤ 0

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: ⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) 1

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
ho : ω ^ ↑2 ≤ o
⊢ 1 < ↑2

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: ⊢ IsPrincipal (fun x1 x2 ↦ x1 * x2) 1

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: case inl
c : Cardinal.{u_1}
l : IsSuccPrelimit 0
⊢ preAleph 0 ≤ c ↔ ∀ o' < 0, preAleph o' ≤ c

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ℵ₀ * ℵ_ o = ℵ_ o

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ℵ_ o * ℵ₀ = ℵ_ o

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: case inl
ho : IsSuccPrelimit 0
⊢ preAleph 0 = ⨆ a, preAleph ↑a

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ℵ_ (o + 1) = succ (ℵ_ o)

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case inl
b : Cardinal.{u_1}
⊢ 0 * b ≤ max (max 0 b) ℵ₀

Tactic:
simp

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

Goal state before:
pp: ⊢ cof ℤ = ℵ₀

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case inr.inl
a : Cardinal.{u_1}
ha0 : a ≠ 0
⊢ a * 0 ≤ max (max a 0) ℵ₀

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: ⊢ ℵ₀ < ℵ_ 1

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: α : Type u_1
inst✝ : Uncountable α
⊢ ℵ_ 1 ≤ #α

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: ⊢ ⨆ a, 2 ^ preBeth ↑a = 0

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: ⊢ preBeth ↑0 = ↑((fun x ↦ 2 ^ x)^[0] 0)

Tactic:
simp

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

Goal state before:
pp: case refine_1
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set α
hs : IsCofinal s
t : Set ↑s
ht : IsCofinal t
ht' : typeLT ↑t = (Order.cof α).ord
⊢ Subtype.val '' t ⊆ s

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: case refine_1.refine_2
a : Ordinal.{u_1}
⊢ preBeth (succ a) ≤ 2 ^ preBeth a

Tactic:
simp

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

Goal state before:
pp: case refine_2.refine_2
β : Type v
inst✝¹ : LinearOrder β
inst✝ : Small.{u, v} β
f : β → Ordinal.{u}
hf : StrictMono f
this✝ : StrictMono fun i ↦ ⟨f i, ⋯⟩
this : Cardinal.lift.{u + 1, v} (Order.cof β) = Cardinal.lift.{v, u + 1} (Order.cof ↑(Iio (⨆ i, f i + 1)))
⊢ Cardinal.lift.{u + 1, max u v} (Cardinal.lift.{v, u} (⨆ i, f i + 1).cof) =
    Cardinal.lift.{v, u + 1} (Order.cof ↑(Iio (⨆ i, f i + 1)))

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case refine_2.inr.inl
a : Cardinal.{u_1}
⊢ a * 1 = a

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case refine_2.inr.inr
b : Cardinal.{u_1}
⊢ 0 * b = 0

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a b : Cardinal.{u_1}
ha : ℵ₀ ≤ b
⊢ b + a = max a b

Tactic:
max_comm,

Goal state after:
a b : Cardinal.{u_1}
ha : ℵ₀ ≤ b
⊢ b + a = max b a
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u_1
inst✝ : Infinite α
⊢ #α + #α = #α

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case refine_1.inr.inr.inl
ho : IsPrincipal (fun x1 x2 ↦ x1 * x2) ((fun x ↦ ω ^ x) 0)
ho₂ : 2 < (fun x ↦ ω ^ x) 0
⊢ (fun x ↦ ω ^ x) 0 ≤ 2 ∨ (fun x ↦ ω ^ x) 0 ∈ Set.range fun x ↦ ω ^ ω ^ x

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: c : Cardinal.{u}
⊢ ℵ_ 1 ≤ lift.{v, u} c ↔ ℵ_ 1 ≤ c

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: c : Cardinal.{u}
⊢ lift.{v, u} c < ℵ_ 1 ↔ c < ℵ_ 1

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: a : Ordinal.{u}
a0 : 0 < a
ha : a < ω
b : Ordinal.{u}
⊢ a * ω * b = ω * b

Tactic:
mul_omega0 a0 ha

Goal state after:
a : Ordinal.{u}
a0 : 0 < a
ha : a < ω
b : Ordinal.{u}
⊢ ω * b = ω * b
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case zero
f : Ordinal.{u_1} → Ordinal.{u_1}
hf : IsNormal f
⊢ cof 0 ≤ (f 0).cof

Tactic:
simp

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

Goal state before:
pp: case e'_3
s : Set Ordinal.{u}
a : Ordinal.{u}
ha : #↑s < (lift.{u + 1, u} a).cof
hs : ∀ i ∈ s, i < a
f : ↑(Iio (typeLT ↑s)) ≃o ↑s := OrderIso.ofRelIsoLT (enum fun x1 x2 ↦ x1 < x2)
this : Small.{u, u + 2} ↑(Iio (typeLT ↑s))
⊢ s = Subtype.val '' Set.univ

Tactic:
simp

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

Goal state before:
pp: ι : Type u
f : ι → Ordinal.{v}
hf : BddAbove (range f)
x : Ordinal.{v}
hx : x ∈ Iio (⨆ i, f i)
i : ι
hi : x < f i
⊢ (fun x ↦ ⟨↑x.snd.toOrd, ⋯⟩) ⟨i, ToType.mk ⟨x, hi⟩⟩ = ⟨x, hx⟩

Tactic:
simp

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

Goal state before:
pp: s : Set Ordinal.{u}
f : ↑(Iio (typeLT ↑s)) ≃o ↑s := OrderIso.ofRelIsoLT (enum fun x1 x2 ↦ x1 < x2)
this✝ : Small.{u, u + 2} ↑(Iio (typeLT ↑s))
this : (range fun i ↦ ↑(f i) + 1) = (fun x ↦ x + 1) '' s
ha : Cardinal.lift.{u + 2, u + 1} #↑s < Cardinal.lift.{u + 2, u} (⨆ i, ↑(f i) + 1).cof
hs : ∀ i ∈ s, i < ⨆ i, ↑(f i) + 1
x✝ : ↑(Iio (typeLT ↑s))
⊢ ∀ ⦃b : ↑(Iio (typeLT ↑s))⦄, x✝ < b → ↑(f x✝) < ↑(f b)

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: o : Ordinal.{u_1}
ho : o ≤ o.cof.ord
⊢ IsCofinal (range id)

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: f : ↑(Iio 0) → ↑(Iio 0)
⊢ 0 ≤ (cof 0).ord

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: f : ↑(Iio 0) → ↑(Iio 0)
x✝ : ↑(Iio 0)
⊢ ∀ ⦃b : ↑(Iio 0)⦄, x✝ < b → f x✝ < f b

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: o : Ordinal.{u_1}
⊢ 1 ≤ (o + 1).cof.ord

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: o : Ordinal.{u_1}
x✝ : ↑(Iio 1)
⊢ ∀ ⦃b : ↑(Iio 1)⦄, x✝ < b → (fun x ↦ ⟨o, ⋯⟩) x✝ < (fun x ↦ ⟨o, ⋯⟩) b

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: a o : Ordinal.{u_1}
f : ↑(Iio a) → ↑(Iio o)
g : Ordinal.{u_1} → Ordinal.{u_1}
hg : IsNormal g
hf : IsFundamentalSeq f
ho : IsSuccLimit o
b : Ordinal.{u_1}
hb : b ∈ Iio (g o)
c : Ordinal.{u_1}
hc : c < o
hc' : b < g c
d : ↑(Iio a)
hd : ⟨c, hc⟩ ≤ f d
⊢ ⟨g ↑(f d), ⋯⟩ ∈ range fun i ↦ ⟨g ↑(f i), ⋯⟩

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case inl
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h✝ : IsEmpty ι
⊢ (⨆ i, f i) * c = ⨆ i, f i * c

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case inr.inl
ι : Type u
f : ι → Cardinal.{v}
h✝ : Nonempty ι
⊢ (⨆ i, f i) * 0 = ⨆ i, f i * 0

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: o : Ordinal.{u_1}
s : Set o.ToType
hs : IsCofinal s
hs' : typeLT ↑s = o.cof.ord
g : ↑(Iio o.cof.ord) ≃o ↑s :=
  (OrderIso.setCongr (Iio o.cof.ord) (Iio (typeLT ↑s)) ⋯).trans (OrderIso.ofRelIsoLT (enum fun x1 x2 ↦ x1 < x2))
x✝ : ↑(Iio o.cof.ord)
⊢ ∀ ⦃b : ↑(Iio o.cof.ord)⦄, x✝ < b → (↑(g x✝)).toOrd < (↑(g b)).toOrd

Tactic:
simp

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

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

Tactic:
apply Ordinal.iSup_lt_of_lt_cof <;> simpa

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case inl.refine_1.hbc
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hinf : ℵ₀ ≤ κ₂ + μ₂
⊢ κ₂ ≤ κ₂ + μ₂

Tactic:
simp

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

Goal state before:
pp: o : Ordinal.{u}
a : Cardinal.{u}
⊢ a ≤ o.cof ↔ ∀ {ι : Type u} (f : ι → Ordinal.{u}), lsub f = o → a ≤ #ι

Tactic:
by
  rw [cof_eq_sInf_lsub]
  exact
    (le_csInf_iff'' (cof_lsub_def_nonempty o)).trans
      ⟨fun H ι f hf => H _ ⟨ι, f, hf, rfl⟩, fun H b ⟨ι, f, hf, hb⟩ => by
        rw [← hb]
        exact H _ hf⟩

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case inl.refine_2.hbc
κ₁ κ₂ μ₁ μ₂ : Cardinal.{u_1}
hκ : κ₁ < κ₂
hμ : μ₁ < μ₂
hinf : ℵ₀ ≤ κ₂ + μ₂
⊢ μ₂ ≤ κ₂ + μ₂

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ StrictMono fun a ↦ ↑n * a

Tactic:
match n, hn with
  | 1, _ => simpa using! strictMono_id
  | (n + 1) + 1, hneq1 =>
    intro a μ hlt
    push_cast
    conv_lhs => rw [add_mul, one_mul]
    conv_rhs => rw [add_mul, one_mul]
    refine Cardinal.add_lt_add ?_ hlt
    simpa using! (natCast_mul_strictMono (Nat.succ_ne_zero n) hlt)

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: ⊢ ℵ₀ ≤ ℵ₀.ord.cof

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: α : Type u_1
inst✝ : Countable α
f : α → Ordinal.{u_2}
⊢ lift.{u_2, u_1} #α < (Ordinal.lift.{u_1, u_2} (ω_ 1)).cof

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Pigeonhole

Goal state before:
pp: β α : Type u
f : β → α
h : #α < #β
inst✝ : Uncountable β
hα : #α < ℵ₀
⊢ ℵ_ 1 ≤ #β

Tactic:
simp

Goal state after:
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))
b : β
⊢ f ⋯.choose ∈ range f

Tactic:
simp

Goal state after:
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 : α
⊢ f a ∈ range f

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u
inst✝ : Infinite α
H1 : ℵ₀ ≤ #α
x✝ : α
⊢ ∀ ⦃a₂ : α⦄, (fun a ↦ [a]) x✝ = (fun a ↦ [a]) a₂ → x✝ = a₂

Tactic:
simp

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Cardinality

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial M
ι : Type u_1
s : Set (ι →₀ M)
hs : s.Finite
hsspan : span R s = ⊤
this : ⋃ i ∈ s, ↑i.support = Set.univ
x✝¹ : ι →₀ M
x✝ : x✝¹ ∈ s
⊢ (↑x✝¹.support).Finite

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: case inl
⊢ (ℵ_ 0).IsSingular ↔ IsSuccLimit 0 ∧ Ordinal.cof 0 < ℵ_ 0

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: case inr.inl
a : Ordinal.{u_1}
⊢ (ℵ_ (succ a)).IsSingular ↔ IsSuccLimit (succ a) ∧ (succ a).cof < ℵ_ (succ a)

Tactic:
simp

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u
c : Cardinal.{u}
⊢ #(ULift.{u, 0} ℕ ⊕ α) ^ c ≤ max #α ℵ₀ ^ c

Tactic:
max_comm,

Goal state after:
α : Type u
c : Cardinal.{u}
⊢ #(ULift.{u, 0} ℕ ⊕ α) ^ c ≤ max ℵ₀ #α ^ c
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: ⊢ Cardinal.univ.{u, v} ≤ Cardinal.univ.{u, v}.ord.cof

Tactic:
simp

Goal state after:
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 [single_apply, ne] using congr(b.repr $z j)

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

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
p : ι → Prop
inst✝ : DecidablePred p
i✝ : ι
⊢ (filter p 0) i✝ = 0 i✝

Tactic:
simp

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

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i : ι
b : β i
j : ι
⊢ j = i → j ∈ {i}

Tactic:
simp

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

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i : ι
xi : β i
⊢ i = i ∧ xi ≍ 0 ∨ xi = 0 ∧ 0 = 0 ↔ xi = 0

Tactic:
simp

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

Goal state before:
pp: case isTrue
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), β i
i✝ : ι
⊢ f i✝ = Eq.recOn ⋯ (f i✝)

Tactic:
simp

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

Goal state before:
pp: case isFalse
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), β i
i i✝ : ι
h✝ : ¬i = i✝
⊢ 0 = 0

Tactic:
simp

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 : ι
⊢ filter (fun x ↦ i = x) f = single i (f i)

Tactic:
ext
  rw [filter_apply, single_apply]
  split
  · subst i
    simp
  · simp

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

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

Tactic:
simp

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

Goal state before:
pp: case inl
ι : Type u
inst✝¹ : DecidableEq ι
β : ι → Type u_1
inst✝ : (i : ι) → AddGroup (β i)
f : Π₀ (i : ι), β i
j : ι
⊢ (erase j f) j = (f - single j (f j)) j

Tactic:
simp

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

Goal state before:
pp: case inl
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), β i
i : ι
b : β i
s : { s // ∀ (i : ι), i ∈ s ∨ f.toFun i = 0 }
⊢ i ∈ i ::ₘ ↑s ∨ Function.update (⇑f) i b i = 0

Tactic:
simp

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✝ : ι
⊢ (f.update i (f i)) i✝ = f i✝

Tactic:
simp

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

Goal state before:
pp: case inl
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), β i
i : ι
⊢ (f.update i 0) i = (erase i f) i

Tactic:
simp

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

Goal state before:
pp: case inl
ι : Type u
inst✝¹ : DecidableEq ι
β : ι → Type u_1
inst✝ : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
i : ι
b : β i
⊢ (f.update i b) i = (single i b + erase i f) i

Tactic:
simp

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

Goal state before:
pp: case inl
ι : Type u
inst✝¹ : DecidableEq ι
β : ι → Type u_1
inst✝ : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
i : ι
b : β i
⊢ (f.update i b) i = (erase i f + single i b) i

Tactic:
simp

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

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
s : Finset ι
f : (i : ↥s) → { x // x ≠ 0 }
i : ι
⊢ i ∈ (mk s fun i ↦ ↑(f i)).support ↔ ∃ (h : i ∈ s), ↑(f ⟨i, h⟩) ≠ 0

Tactic:
simp

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

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
s : Finset ι
f : (i : ↥s) → { x // x ≠ 0 }
i : ι
⊢ (∃ (_ : i ∈ s), True) ↔ i ∈ s

Tactic:
simp

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

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
s : Finset ι
f : (i : ↥s) → { x // x ≠ 0 }
⊢ (fun x ↦
        match (motive := { f // f.support = s } → (i : ↥s) → { x // x ≠ 0 }) x with
        | ⟨f, hf⟩ => fun x ↦
          match x with
          | ⟨i, hi⟩ => ⟨f i, ⋯⟩)
      ((fun f ↦ ⟨mk s fun i ↦ ↑(f i), ⋯⟩) f) =
    f

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Fintype.Quotient

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
C : ((i : ι) → Quotient (S i)) → Sort u_4
a : (i : ι) → α i
⊢ (fun f h ↦ finHRecOn (fun x ↦ ⟦a x⟧) f ⋯) = fun f x ↦ f a

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Fintype.Quotient

Goal state before:
pp: ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
α : ι → Sort u_2
C : ((i : ι) → Trunc (α i)) → Sort u_4
a : (i : ι) → α i
⊢ (fun f h ↦ Quotient.finRecOn (fun x ↦ ⟦a x⟧) (fun x ↦ f x) ⋯) = fun f x ↦ f a

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finsupp.ToDFinsupp

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Zero M
inst✝ : (m : M) → Decidable (m ≠ 0)
f : ι →₀ M
a✝ : ι
⊢ a✝ ∈ f.toDFinsupp.support ↔ a✝ ∈ f.support

Tactic:
simp

Goal state after: