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

Goal state before:
pp: case refine_2
a b : Ordinal.{u_1}
x✝ : 1 < a ∧ b ≠ 0
ha : 1 < a
hb : b ≠ 0
⊢ 1 < a ^ b

Tactic:
rwa [← opow_zero a, opow_lt_opow_iff_right ha, pos_iff_ne_zero]

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

Goal state before:
pp: case inl
a c : Ordinal.{u_4}
⊢ a < 0 * c ↔ ∃ q < c, ∃ r < 0, a = 0 * q + r

pp: case inr
a b c : Ordinal.{u_4}
hb₀ : b ≠ 0
⊢ a < b * c ↔ ∃ q < c, ∃ r < b, a = b * q + r

Tactic:
· simp

Goal state after:
case inr
a b c : Ordinal.{u_4}
hb₀ : b ≠ 0
⊢ a < b * c ↔ ∃ q < c, ∃ r < b, a = b * q + r
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inr
b c : Ordinal.{u_4}
hb₀ : b ≠ 0
q : Ordinal.{u_4}
hq : q < c
r : Ordinal.{u_4}
hr : r < b
⊢ b * q + r < b * c

Tactic:
grw [hr, ← mul_add_one, add_one_le_iff.2 hq]

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

Goal state before:
pp: case neg
o : Ordinal.{u_1}
s : Set Ordinal.{u_1}
hs : s.Nonempty
ho : 0 < o
bdd : ¬BddAbove s
⊢ o * ⊥ = sSup ∅

pp: case neg
o : Ordinal.{u_1}
s : Set Ordinal.{u_1}
hs : s.Nonempty
ho : 0 < o
bdd : ¬BddAbove s
⊢ ¬BddAbove ((fun x ↦ o * x) '' s)

Tactic:
· simp

Goal state after:
case neg
o : Ordinal.{u_1}
s : Set Ordinal.{u_1}
hs : s.Nonempty
ho : 0 < o
bdd : ¬BddAbove s
⊢ ¬BddAbove ((fun x ↦ o * x) '' s)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: m n : ℕ
⊢ ↑(m * n + m) = ↑m * ↑(n + 1)

Tactic:
Nat.cast_add,

Goal state after:
m n : ℕ
⊢ ↑(m * n) + ↑m = ↑m * ↑(n + 1)
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inl
b k : ℕ
⊢ log (b ^ k) 0 = log b 0 / k

pp: case inr
b k n : ℕ
hn : n ≠ 0
⊢ log (b ^ k) n = log b n / k

Tactic:
· simp

Goal state after:
case inr
b k n : ℕ
hn : n ≠ 0
⊢ log (b ^ k) n = log b n / k
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inr.inl
b n : ℕ
hn : n ≠ 0
⊢ log (b ^ 0) n = log b n / 0

pp: case inr.inr
b k n : ℕ
hn : n ≠ 0
hk : k > 0
⊢ log (b ^ k) n = log b n / k

Tactic:
· simp

Goal state after:
case inr.inr
b k n : ℕ
hn : n ≠ 0
hk : k > 0
⊢ log (b ^ k) n = log b n / k
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inl
m : ℕ
⊢ ↑(m / 0) = ↑m / ↑0

pp: case inr
m n : ℕ
hn : n ≠ 0
⊢ ↑(m / n) = ↑m / ↑n

Tactic:
· simp

Goal state after:
case inr
m n : ℕ
hn : n ≠ 0
⊢ ↑(m / n) = ↑m / ↑n
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inl.inl
b : Ordinal.{u_1}
⊢ 0 ^ (b + 0) = 0 ^ b * 0 ^ 0

pp: case inl.inr
b c : Ordinal.{u_1}
hc : 0 < c
⊢ 0 ^ (b + c) = 0 ^ b * 0 ^ c

Tactic:
· simp

Goal state after:
case inl.inr
b c : Ordinal.{u_1}
hc : 0 < c
⊢ 0 ^ (b + c) = 0 ^ b * 0 ^ c
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inr.inl
b c : Ordinal.{u_1}
ha : 0 < 1
⊢ 1 ^ (b + c) = 1 ^ b * 1 ^ c

pp: case inr.inr
a b c : Ordinal.{u_1}
ha : 0 < a
ha' : 1 < a
⊢ a ^ (b + c) = a ^ b * a ^ c

Tactic:
· simp

Goal state after:
case inr.inr
a b c : Ordinal.{u_1}
ha : 0 < a
ha' : 1 < a
⊢ a ^ (b + c) = a ^ b * a ^ c
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inl
a c : Ordinal.{u_1}
⊢ a ^ (0 * c) = (a ^ 0) ^ c

pp: case inr
a b c : Ordinal.{u_1}
hb : 0 < b
⊢ a ^ (b * c) = (a ^ b) ^ c

Tactic:
· simp

Goal state after:
case inr
a b c : Ordinal.{u_1}
hb : 0 < b
⊢ a ^ (b * c) = (a ^ b) ^ c
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inr.inr.inl
b c : Ordinal.{u_1}
hb : 0 < b
ha : 1 ≠ 0
⊢ 1 ^ (b * c) = (1 ^ b) ^ c

pp: case inr.inr.inr
a b c : Ordinal.{u_1}
hb : 0 < b
ha : a ≠ 0
ha' : 1 < a
⊢ a ^ (b * c) = (a ^ b) ^ c

Tactic:
· simp

Goal state after:
case inr.inr.inr
a b c : Ordinal.{u_1}
hb : 0 < b
ha : a ≠ 0
ha' : 1 < a
⊢ a ^ (b * c) = (a ^ b) ^ c
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case refine_1
a : Ordinal.{u_4}
l : IsSuccPrelimit a
x : Ordinal.{u_4}
hx : x < a
n : ℕ
hb : ↑n < ω
⊢ ω * (x / ω) + ↑n ≤ a

Tactic:
mul_div_le

Goal state after:
case refine_1
a : Ordinal.{u_4}
l : IsSuccPrelimit a
x : Ordinal.{u_4}
hx : x < a
n : ℕ
hb : ↑n < ω
⊢ x + ↑n ≤ a
Module: Mathlib.SetTheory.Ordinal.Exponential

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

Tactic:
apply (csSup_of_not_bddAbove _).trans csSup_empty

Goal state after:
x : Ordinal.{u_1}
h : 0 ≤ 1
⊢ ¬BddAbove ((fun x ↦ 0 ^ x) ⁻¹' Iic x)
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inr.succ
b : ℕ
hb : 1 < b
n : ℕ
⊢ log b (n + 1) ≤ clog b (n + 1)

Tactic:
| succ n =>

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

Goal state before:
pp: case refine_2
b n : ℕ
hb : 1 < b
H : b ^ clog b n = n
⊢ clog b n < clog b (n + 1)

Tactic:
rw [lt_clog_iff_pow_lt hb, H]

Goal state after:
case refine_2
b n : ℕ
hb : 1 < b
H : b ^ clog b n = n
⊢ n < n + 1
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

pp: case inr
b k n : ℕ
hk : k > 0
⊢ clog (b ^ k) n = (clog b n + (k - 1)) / k

Tactic:
· simp

Goal state after:
case inr
b k n : ℕ
hk : k > 0
⊢ clog (b ^ k) n = (clog b n + (k - 1)) / k
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inl
b : Ordinal.{u_1}
hb : 1 < b
⊢ log b 1 = 0

Tactic:
exact log_eq_zero hb

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 * ↑(1 + n) + a % ω ^ log ω a - ω ^ log ω a < a

Tactic:
Nat.cast_add,

Goal state after:
case succ
a : Ordinal.{u_1}
ha : a ≠ 0
n : ℕ
hn : a / ω ^ log ω a = ↑(n + 1)
⊢ ω ^ log ω a * (↑1 + ↑n) + a % ω ^ log ω a - ω ^ log ω a < a
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 * ↑(n + 1) + a % ω ^ log ω a - ω ^ log ω a < a

Tactic:
| succ n =>

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.FixedPoint

Goal state before:
pp: a : Ordinal.{u}
⊢ ∀ (b : Ordinal.{u}), deriv (fun x ↦ a + x) b = a * ω + b

Tactic:
rw [← funext_iff, IsNormal.ext_iff (isNormal_deriv _) (isNormal_add_right _)]

Goal state after:
a : Ordinal.{u}
⊢ deriv (fun x ↦ a + x) ⊥ = a * ω + ⊥ ∧
    ∀ (a_1 : Ordinal.{u}), deriv (fun x ↦ a + x) a_1 = a * ω + a_1 → deriv (fun x ↦ a + x) (succ a_1) = a * ω + succ a_1
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: a : Ordinal.{u}
H : ∀ b < a, ∀ c < a, b + c ≠ a
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) a

Tactic:
by_contra ha

Goal state after:
a : Ordinal.{u}
H : ∀ b < a, ∀ c < a, b + c ≠ a
ha : ¬IsPrincipal (fun x1 x2 ↦ x1 + x2) a
⊢ False
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u}
⊢ Ordinal.lift.{v, u} (preOmega o) = preOmega (Ordinal.lift.{v, u} o)

Tactic:
rw [← ord_preAleph, lift_ord, lift_preAleph, ord_preAleph]

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

pp: case inr
o : Ordinal.{u_1}
l : IsSuccPrelimit o
c : Cardinal.{u_1}
ho : o ≠ 0
⊢ preAleph o ≤ c ↔ ∀ o' < o, preAleph o' ≤ c

Tactic:
· simp

Goal state after:
case inr
o : Ordinal.{u_1}
l : IsSuccPrelimit o
c : Cardinal.{u_1}
ho : o ≠ 0
⊢ preAleph o ≤ c ↔ ∀ o' < o, preAleph o' ≤ c
Module: Mathlib.SetTheory.Cardinal.Aleph

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

pp: case inr
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
h : o ≠ 0
⊢ preAleph o = ⨆ a, preAleph ↑a

Tactic:
· simp

Goal state after:
case inr
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
h : o ≠ 0
⊢ preAleph o = ⨆ a, preAleph ↑a
Module: Mathlib.SetTheory.Cardinal.Arithmetic

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

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

Tactic:
· simp

Goal state after:
case inr
a b : Cardinal.{u_1}
ha0 : a ≠ 0
⊢ a * b ≤ max (max a b) ℵ₀
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) ℵ₀

pp: case inr.inr
a b : Cardinal.{u_1}
ha0 : a ≠ 0
hb0 : b ≠ 0
⊢ a * b ≤ max (max a b) ℵ₀

Tactic:
· simp

Goal state after:
case inr.inr
a b : Cardinal.{u_1}
ha0 : a ≠ 0
hb0 : b ≠ 0
⊢ a * b ≤ max (max a b) ℵ₀
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: a b : Ordinal.{u_1}
h : a < b
| preBeth b

Tactic:
preBeth

Goal state after:
a b : Ordinal.{u_1}
h : a < b
| ⨆ a, 2 ^ preBeth ↑a
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: ⊢ preBeth 0 = 0

Tactic:
preBeth

Goal state after:
⊢ ⨆ a, 2 ^ preBeth ↑a = 0
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
ho : IsSuccPrelimit o
⊢ preBeth o = ⨆ a, preBeth ↑a

Tactic:
preBeth

Goal state after:
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
⊢ ⨆ a, 2 ^ preBeth ↑a = ⨆ a, preBeth ↑a
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

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

Tactic:
· simp

Goal state after:
case refine_2
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set α
hs : IsCofinal s
t : Set ↑s
ht : IsCofinal t
ht' : typeLT ↑t = (Order.cof α).ord
⊢ typeLT ↑(Subtype.val '' t) = (Order.cof α).ord
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.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

pp: case refine_1.inr.inr.inr
b : Ordinal.{u}
ho : IsPrincipal (fun x1 x2 ↦ x1 * x2) ((fun x ↦ ω ^ x) ((fun x ↦ ω ^ x) b))
ho₂ : 2 < (fun x ↦ ω ^ x) ((fun x ↦ ω ^ x) b)
⊢ (fun x ↦ ω ^ x) ((fun x ↦ ω ^ x) b) ≤ 2 ∨ (fun x ↦ ω ^ x) ((fun x ↦ ω ^ x) b) ∈ Set.range fun x ↦ ω ^ ω ^ x

Tactic:
· simp

Goal state after:
case refine_1.inr.inr.inr
b : Ordinal.{u}
ho : IsPrincipal (fun x1 x2 ↦ x1 * x2) ((fun x ↦ ω ^ x) ((fun x ↦ ω ^ x) b))
ho₂ : 2 < (fun x ↦ ω ^ x) ((fun x ↦ ω ^ x) b)
⊢ (fun x ↦ ω ^ x) ((fun x ↦ ω ^ x) b) ≤ 2 ∨ (fun x ↦ ω ^ x) ((fun x ↦ ω ^ x) b) ∈ Set.range fun x ↦ ω ^ ω ^ x
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: γ : Type u
inst✝¹ : LinearOrder γ
inst✝ : NoMaxOrder γ
f : γ → Ordinal.{u}
hf : StrictMono f
⊢ (⨆ i, f i).cof = Order.cof γ

Tactic:
by
  simpa using lift_cof_iSup hf

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

Goal state before:
pp: a o : Ordinal.{u_1}
f : ↑(Iio a) → ↑(Iio o)
hf : IsFundamentalSeq f
ha : 1 < a
⊢ ⨆ i, ↑(f i) = o

Tactic:
by
  rw [← iSup_Iio_add_one hf.strictMono, hf.iSup_add_one_eq]
  rw [← hf.ord_cof]
  apply (isSuccLimit_ord _).isSuccPrelimit
  rwa [aleph0_le_cof_iff, ← ord_lt_ord, hf.ord_cof, ord_one]

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

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

Tactic:
· simp

Goal state after:
case inr
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h✝ : Nonempty ι
⊢ (⨆ i, f i) * c = ⨆ i, f i * c
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

pp: case inr.inr
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h✝ : Nonempty ι
h0 : c ≠ 0
⊢ (⨆ i, f i) * c = ⨆ i, f i * c

Tactic:
· simp

Goal state after:
case inr.inr
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h✝ : Nonempty ι
h0 : c ≠ 0
⊢ (⨆ i, f i) * c = ⨆ i, f i * c
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: c : Cardinal.{u}
s : Set Ordinal.{u}
hs : #↑s ≤ Cardinal.lift.{u + 1, u} c
hs' : ∀ x ∈ s, x.card ≤ c
⊢ (sSup s).card ≤ c

Tactic:
rw [sSup_eq_iSup']

Goal state after:
c : Cardinal.{u}
s : Set Ordinal.{u}
hs : #↑s ≤ Cardinal.lift.{u + 1, u} c
hs' : ∀ x ∈ s, x.card ≤ c
⊢ (⨆ a, ↑a).card ≤ c
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: case le_cof_ord
κ : Cardinal.{v}
h₁ : ℵ₀ ≤ κ
h₂ : κ ≤ κ.ord.cof
⊢ Cardinal.lift.{u, v} κ ≤ Cardinal.lift.{u, v} κ.ord.cof

Tactic:
lift_le

Goal state after:
case le_cof_ord
κ : Cardinal.{v}
h₁ : ℵ₀ ≤ κ
h₂ : κ ≤ κ.ord.cof
⊢ κ ≤ κ.ord.cof
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case a
ι : Type u
inst✝ : Infinite ι
c : ι → Cardinal.{v}
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift.{u, v} (c i) ≤ lift.{v, u} #ι
i : ι
⊢ lift.{u, v} 2 ≤ lift.{u, v} (c i)

Tactic:
lift_le

Goal state after:
case a
ι : Type u
inst✝ : Infinite ι
c : ι → Cardinal.{v}
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift.{u, v} (c i) ≤ lift.{v, u} #ι
i : ι
⊢ 2 ≤ c i
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: α β : Type u
s : Set α
t : (a : α) → a ∈ s → Set β
c : Cardinal.{u}
h : #↑(⋃ a, ⋃ (h : a ∈ s), t a h) < c
a : α
ha : a ∈ s
⊢ #↑(t a ha) < c

Tactic:
rw [biUnion_eq_iUnion] at h
  have := card_lt_of_card_iUnion_lt h
  simp_all only [iUnion_coe_set, Subtype.forall]

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

Goal state before:
pp: α : Type u
β' : Type v
inst✝ : Infinite α
lle : lift.{u, v} #β' ≤ lift.{v, u} #α
e : α ≃ α ⊕ β'
f g : α → β'
h : (fun f ↦ ⟨fun a ↦ Sum.elim f id (e a), ⋯⟩) f = (fun f ↦ ⟨fun a ↦ Sum.elim f id (e a), ⋯⟩) g
a : α
⊢ f a = g a

Tactic:
by
        simpa only [e.apply_symm_apply] using! congr_fun (Subtype.ext_iff.mp h) (e.symm <| .inl a)

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

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

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

pp: case inr.inr
o : Ordinal.{u_1}
ho : IsSuccLimit o
⊢ (ℵ_ o).IsSingular ↔ IsSuccLimit o ∧ o.cof < ℵ_ o

Tactic:
· simp

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

case inr.inr
o : Ordinal.{u_1}
ho : IsSuccLimit o
⊢ (ℵ_ o).IsSingular ↔ IsSuccLimit o ∧ o.cof < ℵ_ o
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)

pp: case inr.inr
o : Ordinal.{u_1}
ho : IsSuccLimit o
⊢ (ℵ_ o).IsSingular ↔ IsSuccLimit o ∧ o.cof < ℵ_ o

Tactic:
· simp

Goal state after:
case inr.inr
o : Ordinal.{u_1}
ho : IsSuccLimit o
⊢ (ℵ_ o).IsSingular ↔ IsSuccLimit o ∧ o.cof < ℵ_ o
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: case ind
c : Cardinal.{u_1}
hc : c.IsInaccessible
a : Ordinal.{u_1}
IH : ∀ y < a, y < c.ord → preBeth y < c
ha : a < c.ord
⊢ preBeth a < c

Tactic:
preBeth

Goal state after:
case ind
c : Cardinal.{u_1}
hc : c.IsInaccessible
a : Ordinal.{u_1}
IH : ∀ y < a, y < c.ord → preBeth y < c
ha : a < c.ord
⊢ ⨆ a_1, 2 ^ preBeth ↑a_1 < c
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u
s : Set α
c : Cardinal.{u}
⊢ #{ t // t ⊆ s ∧ #↑t ≤ c } ≤ max #↑s ℵ₀ ^ c

Tactic:
refine le_trans ?_ (mk_bounded_set_le s c)

Goal state after:
α : Type u
s : Set α
c : Cardinal.{u}
⊢ #{ t // t ⊆ s ∧ #↑t ≤ c } ≤ #{ t // #↑t ≤ c }
Module: Mathlib.Data.DFinsupp.Defs

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

Tactic:
by grind

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
f : Π₀ (i : ι), β i
i : ι
h : ¬p i
⊢ (filter p f) i = 0

Tactic:
by grind

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

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
s : Finset ι
⊢ Function.Injective (mk s)

Tactic:
intro x y H

Goal state after:
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
s : Finset ι
x y : (i : ↑↑s) → β ↑i
H : mk s x = mk s y
⊢ x = y
Module: Mathlib.Data.DFinsupp.Defs

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

pp: case mpr
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i j : ι
xi : β i
xj : β j
⊢ i = j ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0 → single i xi = single j xj

Tactic:
· intro h
    by_cases hij : i = j
    · subst hij
      exact Or.inl ⟨rfl, heq_of_eq (DFinsupp.single_injective h)⟩
    · have h_coe : ⇑(DFinsupp.single i xi) = DFinsupp.single j xj := congr_arg (⇑) h
      have hci := congr_fun h_coe i
      have hcj := congr_fun h_coe j
      rw [DFinsupp.single_eq_same] at hci hcj
      rw [DFinsupp.single_eq_of_ne hij] at hci
      rw [DFinsupp.single_eq_of_ne (Ne.symm hij)] at hcj
      exact Or.inr ⟨hci, hcj.symm⟩

Goal state after:
case mpr
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i j : ι
xi : β i
xj : β j
⊢ i = j ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0 → single i xi = single j xj
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: 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

pp: case inr
ι : Type u
inst✝¹ : DecidableEq ι
β : ι → Type u_1
inst✝ : (i : ι) → AddGroup (β i)
f : Π₀ (i : ι), β i
i j : ι
h : j ≠ i
⊢ (erase i f) j = (f - single i (f i)) j

Tactic:
· simp

Goal state after:
case inr
ι : Type u
inst✝¹ : DecidableEq ι
β : ι → Type u_1
inst✝ : (i : ι) → AddGroup (β i)
f : Π₀ (i : ι), β i
i j : ι
h : j ≠ i
⊢ (erase i f) j = (f - single i (f i)) j
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

pp: case inr
ι : 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 }
j : ι
hi : i ≠ j
⊢ j ∈ i ::ₘ ↑s ∨ Function.update (⇑f) i b j = 0

Tactic:
· simp

Goal state after:
case inr
ι : 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 }
j : ι
hi : i ≠ j
⊢ j ∈ i ::ₘ ↑s ∨ Function.update (⇑f) i b j = 0
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

pp: case inr
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), β i
i j : ι
hi : i ≠ j
⊢ (f.update i 0) j = (erase i f) j

Tactic:
· simp

Goal state after:
case inr
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), β i
i j : ι
hi : i ≠ j
⊢ (f.update i 0) j = (erase i f) j
Module: Mathlib.Data.DFinsupp.Module

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
κ : Type u_1
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → SMulZeroClass γ (β i)
h : κ → ι
hh : Function.Injective h
r : γ
f : Π₀ (i : ι), β i
i✝ : κ
⊢ r • f (h i✝) = r • (comapDomain h hh f) i✝

Tactic:
comapDomain_apply

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
κ : Type u_1
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → SMulZeroClass γ (β i)
h : κ → ι
hh : Function.Injective h
r : γ
f : Π₀ (i : ι), β i
i✝ : κ
⊢ r • f (h i✝) = r • f (h i✝)
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

pp: case inr
ι : Type u
inst✝¹ : DecidableEq ι
β : ι → Type u_1
inst✝ : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
i : ι
b : β i
j : ι
h : i ≠ j
⊢ (f.update i b) j = (single i b + erase i f) j

Tactic:
· simp

Goal state after:
case inr
ι : Type u
inst✝¹ : DecidableEq ι
β : ι → Type u_1
inst✝ : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
i : ι
b : β i
j : ι
h : i ≠ j
⊢ (f.update i b) j = (single i b + erase i f) j
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

pp: case inr
ι : Type u
inst✝¹ : DecidableEq ι
β : ι → Type u_1
inst✝ : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
i : ι
b : β i
j : ι
h : i ≠ j
⊢ (f.update i b) j = (erase i f + single i b) j

Tactic:
· simp

Goal state after:
case inr
ι : Type u
inst✝¹ : DecidableEq ι
β : ι → Type u_1
inst✝ : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
i : ι
b : β i
j : ι
h : i ≠ j
⊢ (f.update i b) j = (erase i f + single i b) j
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case h
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f i = 0 → b ≠ 0 → p f → p (single i b + f)
f : (i : ι) → β i
s : Multiset ι
H : ∀ (i : ι), i ∈ s ∨ f i = 0
⊢ p { toFun := f, support' := Trunc.mk ⟨s, H⟩ }

Tactic:
induction s using Multiset.induction_on generalizing f with

Goal state after:
case h.cons
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f i = 0 → b ≠ 0 → p f → p (single i b + f)
i : ι
s : Multiset ι
ih : ∀ (f : (i : ι) → β i) (H : ∀ (i : ι), i ∈ s ∨ f i = 0), p { toFun := f, support' := Trunc.mk ⟨s, H⟩ }
f : (i : ι) → β i
H : ∀ (i_1 : ι), i_1 ∈ i ::ₘ s ∨ f i_1 = 0
⊢ p { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ }
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
κ : Type u_1
inst✝² : DecidableEq ι
inst✝¹ : DecidableEq κ
inst✝ : (i : ι) → Zero (β i)
h : κ → ι
hh : Function.Injective h
k : κ
x : β (h k)
i : κ
⊢ (comapDomain h hh (single (h k) x)) i = (single k x) i

Tactic:
comapDomain_apply

Goal state after:
ι : Type u
β : ι → Type v
κ : Type u_1
inst✝² : DecidableEq ι
inst✝¹ : DecidableEq κ
inst✝ : (i : ι) → Zero (β i)
h : κ → ι
hh : Function.Injective h
k : κ
x : β (h k)
i : κ
⊢ (single (h k) x) (h i) = (single k x) i
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case some
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : Option ι → Type v
inst✝ : (i : Option ι) → Zero (α i)
f : Π₀ (i : Option ι), α i
i : ι
⊢ ((fun f ↦ (f none, comapDomain some ⋯ f)) f).2 i = f (some i)

Tactic:
comapDomain_apply

Goal state after:
case some
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : Option ι → Type v
inst✝ : (i : Option ι) → Zero (α i)
f : Π₀ (i : Option ι), α i
i : ι
⊢ f (some i) = f (some i)