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

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{max u v}
x✝ : (∀ (a : Ordinal.{u}), f a < f (succ a)) ∧ ∀ (o : Ordinal.{u}), IsSuccLimit o → (o.bsup fun x x_1 ↦ f x) = f o
h₁ : ∀ (a : Ordinal.{u}), f a < f (succ a)
h₂ : ∀ (o : Ordinal.{u}), IsSuccLimit o → (o.bsup fun x x_1 ↦ f x) = f o
a✝ : Ordinal.{u}
ho : IsSuccLimit a✝
⊢ IsLUB (f '' Iio a✝) (a✝.bsup fun x x_1 ↦ f x)

Tactic:
simpa using

Goal state after:
f : Ordinal.{u} → Ordinal.{max u v}
x✝ : (∀ (a : Ordinal.{u}), f a < f (succ a)) ∧ ∀ (o : Ordinal.{u}), IsSuccLimit o → (o.bsup fun x x_1 ↦ f x) = f o
h₁ : ∀ (a : Ordinal.{u}), f a < f (succ a)
h₂ : ∀ (o : Ordinal.{u}), IsSuccLimit o → (o.bsup fun x x_1 ↦ f x) = f o
a✝ : Ordinal.{u}
ho : IsSuccLimit a✝
⊢ ∀ a < a✝, f a ≤ a✝.bsup fun x x_1 ↦ f x
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b n : ℕ
⊢ log b n = 1 ↔ b ≤ n ∧ n < b * b

Tactic:
rw [log_eq_iff (Or.inl Nat.one_ne_zero), Nat.pow_add, Nat.pow_one]

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

Goal state before:
pp: a b c : Ordinal.{u_1}
b0 : b ≠ 0
h : IsSuccLimit c
⊢ a < b ^ c ↔ ∃ c' < c, a < b ^ c'

Tactic:
simpa using

Goal state after:
a b c : Ordinal.{u_1}
b0 : b ≠ 0
h : IsSuccLimit c
⊢ a < b ^ c ↔ ∃ c' < c, a < b ^ c'
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: a : Ordinal.{u_1}
⊢ a ^ 1 = a

Tactic:
simpa using

Goal state after:
a : Ordinal.{u_1}
⊢ a ^ 1 = a
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: b : Ordinal.{u_1}
l : IsSuccLimit b
IH : ∀ o' < b, 1 ^ o' = 1
c : Ordinal.{u_1}
H : ∀ b' < b, 1 ^ b' ≤ c
⊢ 1 ≤ c

Tactic:
simpa using

Goal state after:
b : Ordinal.{u_1}
l : IsSuccLimit b
IH : ∀ o' < b, 1 ^ o' = 1
c : Ordinal.{u_1}
H : ∀ b' < b, 1 ^ b' ≤ c
⊢ 1 ≤ c
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b : Ordinal.{u_4}
b0 : a * b ≠ 0
⊢ a ≤ a * b

Tactic:
simpa using

Goal state after:
a b : Ordinal.{u_4}
b0 : a * b ≠ 0
⊢ a ≤ a * b
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case add_one
a : Ordinal.{u_1}
a0 : 0 < a
h0 : 0 < a ^ 0
b : Ordinal.{u_1}
IH : 0 < a ^ b
⊢ 0 < a ^ (b + 1)

Tactic:
simpa using

Goal state after:
case add_one
a : Ordinal.{u_1}
a0 : 0 < a
h0 : 0 < a ^ 0
b : Ordinal.{u_1}
IH : 0 < a ^ b
⊢ 0 < a ^ b * a
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b : Ordinal.{u_4}
H : a % b = 0
⊢ a = b * (a / b)

Tactic:
simpa using

Goal state after:
a b : Ordinal.{u_4}
H : a % b = 0
⊢ a = b * (a / b)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: x y : Ordinal.{u_4}
⊢ x * y % x = 0

Tactic:
simpa using

Goal state after:
x y : Ordinal.{u_4}
⊢ x * y % x = 0
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case refine_1
a : Ordinal.{u_1}
h : 1 < a
ha : 0 < a
⊢ ∀ (a_1 : Ordinal.{u_1}), a ^ a_1 < a ^ succ a_1

Tactic:
simpa using

Goal state after:
case refine_1
a : Ordinal.{u_1}
h : 1 < a
ha : 0 < a
⊢ ∀ (a_1 : Ordinal.{u_1}), a ^ a_1 < a ^ a_1 * a
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inr
a b : Ordinal.{u_1}
h : a ≠ 1 ∧ b ≠ 0
ha : 1 < a
⊢ a ^ b ≠ 1

Tactic:
simpa using

Goal state after:
case inr
a b : Ordinal.{u_1}
h : a ≠ 1 ∧ b ≠ 0
ha : 1 < a
⊢ ¬a ^ b = 1
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u_1}
s : Set Ordinal.{u_1}
⊢ o * sSup s = sSup ((fun x ↦ o * x) '' s)

Tactic:
by
  rcases s.eq_empty_or_nonempty with (rfl | hs)
  · simp
  rcases eq_zero_or_pos o with (rfl | ho)
  · simp [hs.image_const]
  by_cases bdd : BddAbove s
  · exact (isNormal_mul_right ho).map_sSup hs bdd
  · rw [csSup_of_not_bddAbove bdd, csSup_empty, csSup_of_not_bddAbove]
    · simp
    exact fun ⟨u, hu⟩ ↦ bdd ⟨u, fun x hx ↦ (x.le_mul_right ho).trans (hu ⟨x, hx, rfl⟩)⟩

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

Goal state before:
pp: case neg.add_one
a b : Ordinal.{u_1}
ab : a ≤ b
ha : ¬a = 0
c : Ordinal.{u_1}
IH : a ^ c ≤ b ^ c
⊢ a ^ (c + 1) ≤ b ^ (c + 1)

Tactic:
simpa using

Goal state after:
case neg.add_one
a b : Ordinal.{u_1}
ab : a ≤ b
ha : ¬a = 0
c : Ordinal.{u_1}
IH : a ^ c ≤ b ^ c
⊢ a ^ c * a ≤ b ^ c * b
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case succ.inl
n : ℕ
hn : 1 < n
fuel : ℕ
ih :
  ∀ {b : ℕ},
    1 < b →
      n < b ^ fuel →
        (go n b fuel).fst = b ^ ((go n b fuel).snd + 1) / n ∧
          b ^ (go n b fuel).snd < n ∧ n ≤ b ^ ((go n b fuel).snd + 1)
b : ℕ
hb : 1 < b
hfuel : n < b ^ (fuel + 1)
hbn : b < n
ih₁ : (go n (b * b) fuel).fst = (b * b) ^ ((go n (b * b) fuel).snd + 1) / n
ih₂ : (b * b) ^ (go n (b * b) fuel).snd < n
ih₃ : n ≤ (b * b) ^ ((go n (b * b) fuel).snd + 1)
⊢ (go n b (fuel + 1)).fst = b ^ ((go n b (fuel + 1)).snd + 1) / n ∧
    b ^ (go n b (fuel + 1)).snd < n ∧ n ≤ b ^ ((go n b (fuel + 1)).snd + 1)

Tactic:
simp_all only [go, if_neg (Nat.not_le_of_gt hbn), ← Nat.pow_two, ← Nat.pow_mul,
        Nat.div_lt_iff_lt_mul (Nat.zero_lt_of_lt hbn), Nat.div_div_eq_div_mul,
        Nat.mul_comm n b, Nat.mul_add_one, @Nat.pow_add_one' _ (2 * _ + 1),
        Nat.mul_lt_mul_left, Nat.mul_div_mul_left, Nat.zero_lt_of_lt hb]

Goal state after:
case succ.inl
n : ℕ
hn : 1 < n
fuel : ℕ
ih :
  ∀ {b : ℕ},
    1 < b →
      n < b ^ fuel →
        (go n b fuel).fst = b ^ ((go n b fuel).snd + 1) / n ∧
          b ^ (go n b fuel).snd < n ∧ n ≤ b ^ ((go n b fuel).snd + 1)
b : ℕ
hb : 1 < b
hfuel : n < b ^ (fuel + 1)
hbn : b < n
ih₁ : (go n (b ^ 2) fuel).fst = b * b ^ (2 * (go n (b ^ 2) fuel).snd + 1) / n
ih₂ : b ^ (2 * (go n (b ^ 2) fuel).snd) < n
ih₃ : n ≤ b * b ^ (2 * (go n (b ^ 2) fuel).snd + 1)
⊢ (if b ^ (2 * (go n (b ^ 2) fuel).snd + 1) < n then
          (b * b ^ (2 * (go n (b ^ 2) fuel).snd + 1) / n, 2 * (go n (b ^ 2) fuel).snd + 1)
        else (b ^ (2 * (go n (b ^ 2) fuel).snd + 1) / n, 2 * (go n (b ^ 2) fuel).snd)).fst =
      b ^
          ((if b ^ (2 * (go n (b ^ 2) fuel).snd + 1) < n then
                (b * b ^ (2 * (go n (b ^ 2) fuel).snd + 1) / n, 2 * (go n (b ^ 2) fuel).snd + 1)
              else (b ^ (2 * (go n (b ^ 2) fuel).snd + 1) / n, 2 * (go n (b ^ 2) fuel).snd)).snd +
            1) /
        n ∧
    b ^
          (if b ^ (2 * (go n (b ^ 2) fuel).snd + 1) < n then
              (b * b ^ (2 * (go n (b ^ 2) fuel).snd + 1) / n, 2 * (go n (b ^ 2) fuel).snd + 1)
            else (b ^ (2 * (go n (b ^ 2) fuel).snd + 1) / n, 2 * (go n (b ^ 2) fuel).snd)).snd <
        n ∧
      n ≤
        b ^
          ((if b ^ (2 * (go n (b ^ 2) fuel).snd + 1) < n then
                (b * b ^ (2 * (go n (b ^ 2) fuel).snd + 1) / n, 2 * (go n (b ^ 2) fuel).snd + 1)
              else (b ^ (2 * (go n (b ^ 2) fuel).snd + 1) / n, 2 * (go n (b ^ 2) fuel).snd)).snd +
            1)
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inr.inr.limit
a b : Ordinal.{u_1}
ha : 0 < a
ha' : 1 < a
c : Ordinal.{u_1}
l : IsSuccLimit c
IH : ∀ o' < c, a ^ (b + o') = a ^ b * a ^ o'
d : Ordinal.{u_1}
⊢ (∀ a' < c, ((fun x ↦ a ^ x) ∘ fun x ↦ b + x) a' ≤ d) ↔ a ^ b * a ^ c ≤ d

Tactic:
simpa using

Goal state after:
case inr.inr.limit
a b : Ordinal.{u_1}
ha : 0 < a
ha' : 1 < a
c : Ordinal.{u_1}
l : IsSuccLimit c
IH : ∀ o' < c, a ^ (b + o') = a ^ b * a ^ o'
d : Ordinal.{u_1}
⊢ (∀ a' < c, a ^ b * a ^ a' ≤ d) ↔ a ^ b * a ^ c ≤ d
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: ⊢ 1 < ω

Tactic:
simpa using

Goal state after:
⊢ 1 < ω
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inr.inr.inr.limit
a b : Ordinal.{u_1}
hb : 0 < b
ha : a ≠ 0
ha' : 1 < a
c : Ordinal.{u_1}
l : IsSuccLimit c
IH : ∀ o' < c, a ^ (b * o') = (a ^ b) ^ o'
d : Ordinal.{u_1}
⊢ (∀ a' < c, ((fun x ↦ a ^ x) ∘ fun x ↦ b * x) a' ≤ d) ↔ (a ^ b) ^ c ≤ d

Tactic:
simpa using

Goal state after:
case inr.inr.inr.limit
a b : Ordinal.{u_1}
hb : 0 < b
ha : a ≠ 0
ha' : 1 < a
c : Ordinal.{u_1}
l : IsSuccLimit c
IH : ∀ o' < c, a ^ (b * o') = (a ^ b) ^ o'
d : Ordinal.{u_1}
⊢ (∀ a' < c, (a ^ b) ^ a' ≤ d) ↔ (a ^ b) ^ c ≤ d
Module: Mathlib.SetTheory.Ordinal.Exponential

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

Tactic:
obtain rfl | hb := eq_zero_or_pos b; · simp
  obtain rfl | ha := eq_or_ne a 0
  · have := hb.ne'
    by_cases c = 0 <;> simp_all
  obtain rfl | ha' := (one_le_iff_ne_zero.2 ha).eq_or_lt; · simp
  induction c using limitRecOn with
  | zero => simp
  | add_one c IH => rw [mul_add_one, opow_add, IH, opow_add_one]
  | limit c l IH =>
    refine eq_of_forall_ge_iff fun d ↦
      (((isNormal_opow ha').comp (isNormal_mul_right hb)).le_iff_forall_le l).trans ?_
    simpa +contextual [IH] using (opow_le_of_isSuccLimit (opow_ne_zero _ ha) l).symm

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

Goal state before:
pp: b u v x : Ordinal.{u_1}
hv : v < b
hu : u < x
⊢ b ^ u * v < b ^ x

Tactic:
simpa using

Goal state after:
b u v x : Ordinal.{u_1}
hv : v < b
hu : u < x
⊢ b ^ u * v < b ^ x
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case not_isMin
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ ¬IsMin c.ord

Tactic:
simpa using

Goal state after:
case not_isMin
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ ¬c = 0
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inl
b c : Ordinal.{u_1}
hb : 1 < b
hc : c ≠ 0
⊢ b ^ c ≤ 0 ↔ c ≤ log b 0

Tactic:
simpa using

Goal state after:
case inl
b c : Ordinal.{u_1}
hb : 1 < b
hc : c ≠ 0
⊢ ¬b = 0
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inl
b c : Ordinal.{u_1}
hb : 1 < b
hc : c ≠ 0
⊢ b ^ c ≤ 0 ↔ c ≤ log b 0

pp: case inr
b x c : Ordinal.{u_1}
hb : 1 < b
hc : c ≠ 0
hx : x ≠ 0
⊢ b ^ c ≤ x ↔ c ≤ log b x

Tactic:
· simpa [hc] using hb.ne_bot

Goal state after:
case inr
b x c : Ordinal.{u_1}
hb : 1 < b
hc : c ≠ 0
hx : x ≠ 0
⊢ b ^ c ≤ x ↔ c ≤ log b x
Module: Mathlib.SetTheory.Ordinal.Exponential

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

Tactic:
simpa using

Goal state after:
case inl
b : Ordinal.{u_1}
hb : 1 < b
⊢ 0 < b
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inr
b x y : Ordinal.{u_1}
xy : x ≤ y
hx : x ≠ 0
⊢ log b x ≤ log b y

Tactic:
obtain hb | hb := lt_or_ge 1 b
    · exact (opow_le_iff_le_log hb (hx.bot_lt.trans_le xy).ne').1 <|
        (opow_log_le_self _ hx).trans xy
    · rw [log_of_left_le_one hb, log_of_left_le_one hb]

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

Goal state before:
pp: case inl
o : Ordinal.{u_1}
ho : o ≠ 0
⊢ o % 0 ^ log 0 o < o

Tactic:
simpa using

Goal state after:
case inl
o : Ordinal.{u_1}
ho : o ≠ 0
⊢ 0 < o
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: b v : Ordinal.{u_1}
hb : 1 < b
u : Ordinal.{u_1}
hv : v ≠ 0
⊢ log b (b ^ u * v) = u + log b v

Tactic:
simpa using

Goal state after:
b v : Ordinal.{u_1}
hb : 1 < b
u : Ordinal.{u_1}
hv : v ≠ 0
⊢ log b (b ^ u * v) = u + log b v
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inl
o : Ordinal.{u_1}
ho : o ≠ 0
⊢ 0 < o / 0 ^ log 0 o

Tactic:
simpa using

Goal state after:
case inl
o : Ordinal.{u_1}
ho : o ≠ 0
⊢ 0 < o
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case a
o : Ordinal.{u_1}
ho : o ≠ 0
⊢ o / 2 ^ log 2 o ≤ 1

Tactic:
simpa using

Goal state after:
case a
o : Ordinal.{u_1}
ho : o ≠ 0
⊢ o / (1 + 1) ^ log (1 + 1) o ≤ 1
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case a
o : Ordinal.{u_1}
ho : o ≠ 0
⊢ 1 ≤ o / 2 ^ log 2 o

Tactic:
simpa using

Goal state after:
case a
o : Ordinal.{u_1}
ho : o ≠ 0
⊢ ¬o / 2 ^ log 2 o = 0
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inr
x y b : Ordinal.{u_1}
hx : x ≠ 0
hy : y ≠ 0
hb : b ≤ 1
⊢ log b x + log b y ≤ log b (x * y)

Tactic:
simpa using

Goal state after:
case inr
x y b : Ordinal.{u_1}
hx : x ≠ 0
hy : y ≠ 0
hb : b ≤ 1
⊢ 0 ≤ 0
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: a : Ordinal.{u_1}
ha : a ≠ 0
n : ℕ
hn : a / ω ^ log ω a = ↑n
| a

Tactic:
← div_add_mod a (ω ^ log ω a),

Goal state after:
a : Ordinal.{u_1}
ha : a ≠ 0
n : ℕ
hn : a / ω ^ log ω a = ↑n
| ω ^ log ω a * (a / ω ^ log ω a) + a % ω ^ log ω a
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case a
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
⊢ ⨆ n, f^[n] a ≤ nfp f a

Tactic:
rw [Ordinal.iSup_le_iff]

Goal state after:
case a
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
⊢ ∀ (i : ℕ), f^[i] a ≤ nfp f a
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case zero
a : Ordinal.{u_1}
ha : a ≠ 0
hn : a / ω ^ log ω a = ↑0
⊢ ω ^ log ω a * ↑0 + a % ω ^ log ω a - ω ^ log ω a < a

Tactic:
simpa using

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

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
a b : Ordinal.{u}
h : b ≤ nfp f a
⊢ f b ≤ nfp f a

Tactic:
simpa using

Goal state after:
f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
a b : Ordinal.{u}
h : b ≤ nfp f a
⊢ f b ≤ nfp f a
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inl
o : Ordinal.{u_1}
ho : 0 < o
ho₁ : 1 < o
⊢ ⨆ n, o ^ n = o ^ ω

Tactic:
simpa using

Goal state after:
case inl
o : Ordinal.{u_1}
ho : 0 < o
ho₁ : 1 < o
⊢ ⨆ n, o ^ n = o ^ ω
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case zero
a o : Ordinal.{u}
ho : IsPrincipal (fun x1 x2 ↦ x1 + x2) o
ha : a < o
⊢ a * ↑0 < o

Tactic:
simpa using

Goal state after:
case zero
a o : Ordinal.{u}
ho : IsPrincipal (fun x1 x2 ↦ x1 + x2) o
ha : a < o
⊢ 0 < o
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case refine_2
o : Ordinal.{u}
h : ∀ a < o, a + o = o
a b : Ordinal.{u}
hao : a < o
hbo : b < o
⊢ (fun x1 x2 ↦ x1 + x2) a b < o

Tactic:
rw [← h a hao]

Goal state after:
case refine_2
o : Ordinal.{u}
h : ∀ a < o, a + o = o
a b : Ordinal.{u}
hao : a < o
hbo : b < o
⊢ (fun x1 x2 ↦ x1 + x2) a b < a + o
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: c : Cardinal.{u_1}
IH : ∀ y < c, ℵ₀ ≤ y → y * y = y
hc : ℵ₀ ≤ c
⊢ c ≤ c * c

Tactic:
simpa using

Goal state after:
c : Cardinal.{u_1}
IH : ∀ y < c, ℵ₀ ≤ y → y * y = y
hc : ℵ₀ ≤ c
⊢ c ≤ c * c
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: ⊢ typeLT Cardinal.{u} = Ordinal.univ.{u, u + 1}

Tactic:
simpa using

Goal state after:
⊢ typeLT Cardinal.{u} = Ordinal.univ.{u, u + 1}
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: ⊢ #Cardinal.{u} = univ.{u, u + 1}

Tactic:
simpa using

Goal state after:
⊢ #Cardinal.{u} = univ.{u, u + 1}
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: ⊢ cof Cardinal.{u} = univ.{u, u + 1}

Tactic:
simpa using

Goal state after:
⊢ cof Cardinal.{u} = univ.{u, u + 1}
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: c : Cardinal.{u_1}
⊢ c ≤ preAleph c.ord

Tactic:
simpa using

Goal state after:
c : Cardinal.{u_1}
⊢ c ≤ preAleph c.ord
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: a b : Ordinal.{u_1}
ha : a ≤ 1
hb : b ≤ 1
⊢ (fun x1 x2 ↦ x1 * x2) a b ≤ 1

Tactic:
simpa using

Goal state after:
a b : Ordinal.{u_1}
ha : a ≤ 1
hb : b ≤ 1
⊢ a * b ≤ 1
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a b : Cardinal.{u_1}
ha : ℵ₀ ≤ a
hb : ℵ₀ ≤ b
⊢ a ≤ a * b

Tactic:
simpa using

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

Goal state before:
pp: a b : Cardinal.{u_1}
ha : ℵ₀ ≤ a
hb : ℵ₀ ≤ b
⊢ b ≤ a * b

Tactic:
simpa using

Goal state after:
a b : Cardinal.{u_1}
ha : ℵ₀ ≤ a
hb : ℵ₀ ≤ b
⊢ b ≤ a * b
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: f : Ordinal.{u_1} → Cardinal.{u_1}
hf : StrictMono f
o : Ordinal.{u_1}
⊢ preAleph o ≤ f o

Tactic:
simpa using

Goal state after:
f : Ordinal.{u_1} → Cardinal.{u_1}
hf : StrictMono f
o : Ordinal.{u_1}
⊢ preAleph o ≤ f o
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a b : Cardinal.{u_1}
h : ℵ₀ ≤ b
⊢ a * b ≤ max a b

Tactic:
simpa using

Goal state after:
a b : Cardinal.{u_1}
h : ℵ₀ ≤ b
⊢ a * b ≤ max a b
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: c : Cardinal.{u_1}
⊢ c ≤ ℵ_ c.ord

Tactic:
simpa using

Goal state after:
c : Cardinal.{u_1}
⊢ c ≤ ℵ_ c.ord
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
⊢ o.cof ≤ o.card

Tactic:
simpa using

Goal state after:
o : Ordinal.{u_1}
⊢ o.cof ≤ o.card
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: c : Cardinal.{u_1}
⊢ c.ord.cof ≤ c

Tactic:
simpa using

Goal state after:
c : Cardinal.{u_1}
⊢ c.ord.cof ≤ c
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: ⊢ cof 1 = 1

Tactic:
simpa using

Goal state after:
⊢ cof 1 = 1
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
⊢ o.cof < ℵ₀ ↔ o.cof ≤ 1

Tactic:
simpa using

Goal state after:
o : Ordinal.{u_1}
⊢ o.cof < ℵ₀ ↔ o.cof ≤ 1
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
ho : IsSuccLimit o
ho' : o < ω_ 1
⊢ o.cof = ℵ₀

Tactic:
apply ((cof_le_card _).trans _).antisymm

Goal state after:
o : Ordinal.{u_1}
ho : IsSuccLimit o
ho' : o < ω_ 1
⊢ ℵ₀ ≤ o.cof

o : Ordinal.{u_1}
ho : IsSuccLimit o
ho' : o < ω_ 1
⊢ o.card ≤ ℵ₀
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
ho : ω ^ 2 ≤ o
⊢ preAleph o = ℵ_ o

Tactic:
simpa using

Goal state after:
o : Ordinal.{u_1}
ho : ω ^ 2 ≤ o
⊢ preOmega o = ω_ o
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: ⊢ preBeth 1 = 1

Tactic:
simpa using

Goal state after:
⊢ preBeth 1 = 1
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: case a
⊢ ℵ₀ ≤ preBeth ω

Tactic:
simpa using

Goal state after:
case a
⊢ ℵ₀ ≤ preBeth ω
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
⊢ 0 < preBeth o ↔ 0 < o

Tactic:
simpa using

Goal state after:
o : Ordinal.{u_1}
⊢ 0 < preBeth o ↔ 0 < o
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: c : Cardinal.{u_1}
⊢ c ≤ preBeth c.ord

Tactic:
simpa using

Goal state after:
c : Cardinal.{u_1}
⊢ c ≤ preBeth c.ord
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
⊢ preBeth o = 0 ↔ o = 0

Tactic:
simpa using

Goal state after:
o : Ordinal.{u_1}
⊢ preBeth o = 0 ↔ o = 0
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
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:
· rw [← ht']
    exact ((Subtype.strictMono_coe _).strictMonoOn _).orderIso.ordinalType_congr.symm

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

Goal state before:
pp: case refine_2
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
x : Cardinal.{u_1}
hx : x < ⨆ a, preBeth ↑a
a : ↑(Iio o)
ha : x < preBeth ↑a
⊢ 2 ^ x ≤ preBeth (↑a + 1)

Tactic:
simpa using

Goal state after:
case refine_2
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
x : Cardinal.{u_1}
hx : x < ⨆ a, preBeth ↑a
a : ↑(Iio o)
ha : x < preBeth ↑a
⊢ 2 ^ x ≤ 2 ^ preBeth ↑a
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
⊢ o.cof.ord.cof = o.cof

Tactic:
simpa using

Goal state after:
o : Ordinal.{u_1}
⊢ o.cof.ord.cof = o.cof
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c + c ≤ c

Tactic:
simpa using

Goal state after:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c + c ≤ c
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: c : Cardinal.{u_1}
⊢ c ≤ ℶ_ c.ord

Tactic:
simpa using

Goal state after:
c : Cardinal.{u_1}
⊢ c ≤ ℶ_ c.ord
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

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

Tactic:
simpa using

Goal state after:
γ : Type u
inst✝ : LinearOrder γ
f : γ → Ordinal.{u}
hf : StrictMono f
⊢ (⨆ i, f i + 1).cof = Order.cof γ
Module: Mathlib.SetTheory.Cardinal.Aleph

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

Tactic:
simpa using

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

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

Tactic:
simpa using

Goal state after:
c : Cardinal.{u}
⊢ ℵ_ 1 < lift.{v, u} c ↔ ℵ_ 1 < c
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:
simpa using

Goal state after:
γ : Type u
inst✝¹ : LinearOrder γ
inst✝ : NoMaxOrder γ
f : γ → Ordinal.{u}
hf : StrictMono f
⊢ (⨆ i, f i).cof = Order.cof γ
Module: Mathlib.SetTheory.Cardinal.Aleph

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

Tactic:
simpa using

Goal state after:
c : Cardinal.{u}
⊢ ℵ_ 1 = lift.{v, u} c ↔ ℵ_ 1 = c
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: a : Ordinal.{u_1}
f : ↑(Iio a) → Ordinal.{u_1}
hf : StrictMono f
⊢ (⨆ i, f i + 1).cof = a.cof

Tactic:
simpa using

Goal state after:
a : Ordinal.{u_1}
f : ↑(Iio a) → Ordinal.{u_1}
hf : StrictMono f
⊢ (⨆ i, f i + 1).cof = a.cof
Module: Mathlib.SetTheory.Cardinal.Aleph

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

Tactic:
simpa using

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

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

Tactic:
simpa using

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

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

Tactic:
simpa using

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

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

Tactic:
by
  simpa using lift_lt (a := ℵ_ n)

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

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

Tactic:
simpa using

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

Goal state before:
pp: c : Cardinal.{u}
n : ℕ
⊢ ℵ_ ↑n = lift.{v, u} c ↔ ℵ_ ↑n = c

Tactic:
simpa using

Goal state after:
c : Cardinal.{u}
n : ℕ
⊢ ℵ_ ↑n = lift.{v, u} c ↔ ℵ_ ↑n = c
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: c : Cardinal.{u}
n : ℕ
⊢ ℶ_ ↑n ≤ lift.{v, u} c ↔ ℶ_ ↑n ≤ c

Tactic:
simpa using

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

Goal state before:
pp: c : Cardinal.{u}
n : ℕ
⊢ lift.{v, u} c ≤ ℶ_ ↑n ↔ c ≤ ℶ_ ↑n

Tactic:
simpa using

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

Goal state before:
pp: c : Cardinal.{u}
n : ℕ
⊢ ℶ_ ↑n < lift.{v, u} c ↔ ℶ_ ↑n < c

Tactic:
simpa using

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

Goal state before:
pp: c : Cardinal.{u}
n : ℕ
⊢ lift.{v, u} c < ℶ_ ↑n ↔ c < ℶ_ ↑n

Tactic:
simpa using

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

Goal state before:
pp: c : Cardinal.{u}
n : ℕ
⊢ ℶ_ ↑n = lift.{v, u} c ↔ ℶ_ ↑n = c

Tactic:
simpa using

Goal state after:
c : Cardinal.{u}
n : ℕ
⊢ ℶ_ ↑n = lift.{v, u} c ↔ ℶ_ ↑n = c
Module: Mathlib.SetTheory.Cardinal.Arithmetic

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

Tactic:
add_eq_left_iff

Goal state after:
a b : Cardinal.{u_1}
⊢ max ℵ₀ a ≤ b ∨ a = 0 ↔ max ℵ₀ a ≤ b ∨ a = 0
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