mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: case h.left
P : ℕ → ℕ → Prop
u : ℕ → ℕ → ℕ
hu : ∀ (n a : ℕ), u n a > a
hu' : ∀ (n a : ℕ), P n (u n a)
⊢ StrictMono fun n ↦ Nat.recOn n (u 0 0) fun n v ↦ u (n + 1) v

pp: case h.right
P : ℕ → ℕ → Prop
u : ℕ → ℕ → ℕ
hu : ∀ (n a : ℕ), u n a > a
hu' : ∀ (n a : ℕ), P n (u n a)
⊢ ∀ (n : ℕ), P n (Nat.recOn n (u 0 0) fun n v ↦ u (n + 1) v)

Tactic:
· apply strictMono_nat_of_lt_succ
    intro n
    apply hu

Goal state after:
case h.right
P : ℕ → ℕ → Prop
u : ℕ → ℕ → ℕ
hu : ∀ (n a : ℕ), u n a > a
hu' : ∀ (n a : ℕ), P n (u n a)
⊢ ∀ (n : ℕ), P n (Nat.recOn n (u 0 0) fun n v ↦ u (n + 1) v)
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : IsDirectedOrder α
a : α
f : β → ↑(Ioi a)
l : Filter β
⊢ Tendsto f l atTop ↔ Tendsto (fun x ↦ ↑(f x)) l atTop

Tactic:
rw [atTop_Ioi_eq, tendsto_comap_iff, Function.comp_def]

Goal state after:
Module: Mathlib.RingTheory.Noetherian.Defs

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type (max 0 u_2) := ⋯
⊢ IsNoetherian R M → WellFoundedGT { N // N.FG }

Tactic:
intro H

Goal state after:
case mp
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type (max 0 u_2) := { N // N.FG }
H : IsNoetherian R M
⊢ WellFoundedGT { N // N.FG }
Module: Mathlib.RingTheory.Noetherian.Defs

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type (max 0 u_2) := ⋯
⊢ WellFoundedGT { N // N.FG } → IsNoetherian R M

Tactic:
intro H

Goal state after:
case mpr
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type (max 0 u_2) := { N // N.FG }
H : WellFoundedGT { N // N.FG }
⊢ IsNoetherian R M
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMulWithZero α β
inst✝¹ : PartialOrder α
inst✝ : Preorder β
h₀ : ∀ (a : α), 0 < a → ∀ (b₁ b₂ : β), b₁ ≤ b₂ → a • b₁ ≤ a • b₂
a : α
ha✝ : 0 ≤ a
b₁ b₂ : β
h : b₁ ≤ b₂
ha : 0 < a
⊢ a • b₁ ≤ a • b₂

Tactic:
exact h₀ _ ha _ _ h

Goal state after:
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMulWithZero α β
inst✝¹ : PartialOrder α
inst✝ : Preorder β
h₀ : ∀ (a : α), 0 < a → ∀ (b₁ b₂ : β), a • b₁ < a • b₂ → b₁ < b₂
a : α
ha✝ : 0 ≤ a
b₁ b₂ : β
h : a • b₁ < a • b₂
ha : 0 < a
⊢ b₁ < b₂

Tactic:
exact h₀ _ ha _ _ h

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

Goal state before:
pp: case h
α : Type u
inst✝ : Preorder α
h : cof α = 1
t : α
hs : IsCofinal {t}
⊢ IsTop t

Tactic:
rwa [isCofinal_singleton_iff] at hs

Goal state after:
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: case inr.inl
α : Type u_1
β : Type u_2
b : β
inst✝⁶ : Zero α
inst✝⁵ : Zero β
inst✝⁴ : SMulWithZero α β
inst✝³ : LinearOrder α
inst✝² : LinearOrder β
inst✝¹ : PosSMulMono α β
inst✝ : SMulPosMono α β
hab : 0 < 0 • b
⊢ 0 < 0 ∧ 0 < b ∨ 0 < 0 ∧ b < 0

Tactic:
rw [zero_smul] at hab
    exact hab.false.elim

Goal state after:
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁶ : Zero α
inst✝⁵ : Zero β
inst✝⁴ : SMulWithZero α β
inst✝³ : LinearOrder α
inst✝² : LinearOrder β
inst✝¹ : PosSMulMono α β
inst✝ : SMulPosMono α β
hab : 0 < a • b
ha : 0 < a
⊢ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

Tactic:
refine Or.inl ⟨ha, lt_imp_lt_of_le_imp_le (fun hb ↦ ?_) hab⟩
    exact smul_nonpos_of_nonneg_of_nonpos ha.le hb

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Submodule R M
sp : M → Submodule R M := fun a ↦ R ∙ a
supr_rw : ∀ (t : Finset M), ⨆ x ∈ t, sp x = ⨆ x ∈ ↑t, sp x
h : ∀ (s_1 : Set (Submodule R M)), s ≤ sSup s_1 → ∃ t, ↑t ⊆ s_1 ∧ s ≤ t.sup id
sSup' : s = sSup (sp '' ↑s)
t : Finset M
huspan : ↑(Finset.image sp t) ⊆ sp '' ↑s
husup : s ≤ (Finset.image sp t).sup id
ssup : s = span R ↑t
⊢ s.FG

Tactic:
eq_comm

Goal state after:
case mpr
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Submodule R M
sp : M → Submodule R M := fun a ↦ R ∙ a
supr_rw : ∀ (t : Finset M), ⨆ x ∈ t, sp x = ⨆ x ∈ ↑t, sp x
h : ∀ (s_1 : Set (Submodule R M)), s ≤ sSup s_1 → ∃ t, ↑t ⊆ s_1 ∧ s ≤ t.sup id
sSup' : s = sSup (sp '' ↑s)
t : Finset M
huspan : ↑(Finset.image sp t) ⊆ sp '' ↑s
husup : s ≤ (Finset.image sp t).sup id
ssup : span R ↑t = s
⊢ s.FG
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
a a₁✝ a₂✝ : α
b b₁ b₂ : β
inst✝⁷ : Ring α
inst✝⁶ : PartialOrder α
inst✝⁵ : IsOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulMono α β
_b : β
hb : 0 ≤ _b
a₁ a₂ : α
ha : a₁ ≤ a₂
⊢ 0 ≤ (a₂ - a₁) • _b

Tactic:
exact smul_nonneg (sub_nonneg.2 ha) hb

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
N : Type u_5
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : Finite M
val✝ : Fintype M
⊢ span R ↑Finset.univ = ⊤

Tactic:
by rw [Finset.coe_univ, span_univ]

Goal state after:
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst✝⁷ : Ring α
inst✝⁶ : PartialOrder α
inst✝⁵ : IsOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulReflectLE α β
h : a • b₁ ≤ a • b₂
ha : a < 0
⊢ b₂ ≤ b₁

Tactic:
rw [← neg_neg a, neg_smul, neg_smul (-a), neg_le_neg_iff] at h

Goal state after:
α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst✝⁷ : Ring α
inst✝⁶ : PartialOrder α
inst✝⁵ : IsOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulReflectLE α β
h : -a • b₂ ≤ -a • b₁
ha : a < 0
⊢ b₂ ≤ b₁
Module: Mathlib.Order.IsNormal

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
hf : IsNormal f
s : Set α
hs : IsLUB s a
hs' : s.Nonempty
b : β
ha : a ∉ s
ha' : IsSuccLimit a
c : α
hc : c < a
d : α
hd : d ∈ s
hcd : c < d
hda : d ≤ a
hb : ∀ x ∈ f '' s, x ≤ b
⊢ f c ≤ b

Tactic:
forall_mem_image

Goal state after:
case neg
α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
hf : IsNormal f
s : Set α
hs : IsLUB s a
hs' : s.Nonempty
b : β
ha : a ∉ s
ha' : IsSuccLimit a
c : α
hc : c < a
d : α
hd : d ∈ s
hcd : c < d
hda : d ≤ a
hb : ∀ ⦃x : α⦄, x ∈ s → f x ≤ b
⊢ f c ≤ b
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
inst✝ : LinearOrder γ
hg : IsNormal g
hf : IsNormal f
a✝ : α
ha : IsSuccLimit a✝
b : γ
hb : ∀ x ∈ (fun a ↦ g (f a)) '' Iio a✝, x ≤ b
⊢ (g ∘ f) a✝ ≤ b

Tactic:
forall_mem_image

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
inst✝ : LinearOrder γ
hg : IsNormal g
hf : IsNormal f
a✝ : α
ha : IsSuccLimit a✝
b : γ
hb : ∀ ⦃x : α⦄, x ∈ Iio a✝ → g (f x) ≤ b
⊢ (g ∘ f) a✝ ≤ b
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
hf : IsNormal f
a : α
⊢ IsNormal fun x ↦ ⟨f ↑x, ⋯⟩

Tactic:
rw [isNormal_iff]

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
hf : IsNormal f
a : α
⊢ (StrictMono fun x ↦ ⟨f ↑x, ⋯⟩) ∧
    ∀ (o : ↑(Iio a)), IsSuccLimit o → ∀ (a_2 : ↑(Iio (f a))), (∀ b < o, ⟨f ↑b, ⋯⟩ ≤ a_2) → ⟨f ↑o, ⋯⟩ ≤ a_2
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: o : Ordinal.{u_4}
⊢ o.pred < o ↔ ¬IsSuccPrelimit o

Tactic:
rw [(pred_le_self o).lt_iff_ne]

Goal state after:
o : Ordinal.{u_4}
⊢ o.pred ≠ o ↔ ¬IsSuccPrelimit o
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inl
a b c : Ordinal.{u_4}
h : a < b + c
hc : 0 < c
hab : a < b
⊢ a - b < c

Tactic:
rwa [Ordinal.sub_eq_zero_iff_le.2 hab.le]

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

Goal state before:
pp: a : Ordinal.{u_4}
⊢ IsNormal fun x ↦ a + x

Tactic:
rw [isNormal_iff]

Goal state after:
a : Ordinal.{u_4}
⊢ (StrictMono fun x ↦ a + x) ∧
    ∀ (o : Ordinal.{u_4}), IsSuccLimit o → ∀ (a_2 : Ordinal.{u_4}), (∀ b < o, a + b ≤ a_2) → a + o ≤ a_2
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: case mp
s : Set Ordinal.{u_3}
⊢ BddAbove ((fun x ↦ x + 1) '' s) → BddAbove s

Tactic:
rintro ⟨a, ha⟩

Goal state after:
case mp
s : Set Ordinal.{u_3}
a : Ordinal.{u_3}
ha : a ∈ upperBounds ((fun x ↦ x + 1) '' s)
⊢ BddAbove s
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: case mpr
s : Set Ordinal.{u_3}
⊢ BddAbove s → BddAbove ((fun x ↦ x + 1) '' s)

Tactic:
rintro ⟨a, ha⟩

Goal state after:
case mpr
s : Set Ordinal.{u_3}
a : Ordinal.{u_3}
ha : a ∈ upperBounds s
⊢ BddAbove ((fun x ↦ x + 1) '' s)
Module: Mathlib.SetTheory.Ordinal.Enum

Goal state before:
pp: case mpr
s : Set Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
hs : ¬BddAbove s
h₁ : StrictMono f
h₂ : range f = s
⊢ s = range f

Tactic:
eq_comm

Goal state after:
case mpr
s : Set Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
hs : ¬BddAbove s
h₁ : StrictMono f
h₂ : range f = s
⊢ range f = s
Module: Mathlib.SetTheory.Ordinal.Enum

Goal state before:
pp: s : Set Ordinal.{u}
H : ∀ t ⊆ s, t.Nonempty → BddAbove t → sSup t ∈ s
hs : ¬BddAbove s
⊢ IsNormal (enumOrd s)

Tactic:
by
  refine isNormal_iff.2 ⟨enumOrd_strictMono hs, fun o ho a ha ↦ ?_⟩
  trans ⨆ b : Iio o, enumOrd s b
  · refine enumOrd_le_of_forall_lt ?_ (fun b hb ↦ (enumOrd_strictMono hs (lt_succ b)).trans_le ?_)
    · have : Nonempty (Iio o) := ⟨0, ho.bot_lt⟩
      apply H _ _ (range_nonempty _) bddAbove_of_small
      rintro _ ⟨c, rfl⟩
      exact enumOrd_mem hs c
    · exact Ordinal.le_iSup _ (⟨_, ho.succ_lt hb⟩ : Iio o)
  · exact Ordinal.iSup_le fun x ↦ ha _ x.2

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

Goal state before:
pp: case inr
b : ℕ
hb : 1 < b
x y : ℕ
hy : y ≠ 0
H₁ : b ^ (log.go y b y).snd ≤ y
H₂ : y < b ^ ((log.go y b y).snd + 1)
h : (log.go y b y).snd ≥ x
⊢ (log.go y b y).snd < x ↔ y < b ^ x

Tactic:
refine iff_of_false (Nat.not_lt_of_ge h) <| Nat.not_lt_of_ge <| Nat.le_trans ?_ H₁
    exact Nat.pow_le_pow_right (Nat.zero_lt_of_lt hb) h

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

Goal state before:
pp: case mp
f : Ordinal.{u} → Ordinal.{max u v}
h : ∀ (a : Ordinal.{u}), f a < f (succ a)
⊢ (∀ (o : Ordinal.{u}), IsSuccLimit o → (o.bsup fun x x_1 ↦ f x) = f o) →
    ∀ (o : Ordinal.{u}), IsSuccLimit o → (o.blsub fun x x_1 ↦ f x) = f o

Tactic:
intro H

Goal state after:
case mp
f : Ordinal.{u} → Ordinal.{max u v}
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
⊢ ∀ (o : Ordinal.{u}), IsSuccLimit o → (o.blsub fun x x_1 ↦ f x) = f o
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: case mpr
f : Ordinal.{u} → Ordinal.{max u v}
h : ∀ (a : Ordinal.{u}), f a < f (succ a)
⊢ (∀ (o : Ordinal.{u}), IsSuccLimit o → (o.blsub fun x x_1 ↦ f x) = f o) →
    ∀ (o : Ordinal.{u}), IsSuccLimit o → (o.bsup fun x x_1 ↦ f x) = f o

Tactic:
intro H

Goal state after:
case mpr
f : Ordinal.{u} → Ordinal.{max u v}
h : ∀ (a : Ordinal.{u}), f a < f (succ a)
H : ∀ (o : Ordinal.{u}), IsSuccLimit o → (o.blsub fun x x_1 ↦ f x) = f o
⊢ ∀ (o : Ordinal.{u}), IsSuccLimit o → (o.bsup fun x x_1 ↦ f x) = f o
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inr.inr.inr
b k n : ℕ
hn : n ≠ 0
hk : k > 0
hb : 1 ≥ b
⊢ log (b ^ k) n = log b n / k

Tactic:
· rw [log_of_left_le_one hb, Nat.zero_div, log_of_left_le_one]
        rwa [Nat.pow_le_one_iff (Nat.ne_of_gt hk)]

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

Goal state before:
pp: case inr
m n : ℕ
h : n ≤ m
⊢ ↑n + ↑(m - n) = ↑n + (↑m - ↑n)

Tactic:
← Nat.cast_add,

Goal state after:
case inr
m n : ℕ
h : n ≤ m
⊢ ↑(n + (m - n)) = ↑n + (↑m - ↑n)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

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

Tactic:
← Nat.cast_add,

Goal state after:
m n : ℕ
⊢ ↑(n * (m / n) + m % n) = ↑m
Module: Mathlib.SetTheory.Ordinal.Arithmetic

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

Tactic:
add_comm,

Goal state after:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ 1 + c = c
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b : ℕ
hb : 1 < b
x : ℕ
hx : 1 < x
⊢ b ^ (clog b x).pred < x

Tactic:
by
  rw [← lt_clog_iff_pow_lt hb]
  exact pred_lt (clog_pos hb hx).ne'

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

Goal state before:
pp: case mpr
o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
h₁ : ∀ (a : Ordinal.{u}), Monotone (op a)
h₂ : ∀ (a : Ordinal.{u}), Monotone (Function.swap op a)
⊢ (∀ a < o, op a a < o) → IsPrincipal op o

Tactic:
intro H

Goal state after:
case mpr
o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
h₁ : ∀ (a : Ordinal.{u}), Monotone (op a)
h₂ : ∀ (a : Ordinal.{u}), Monotone (Function.swap op a)
H : ∀ a < o, op a a < o
⊢ IsPrincipal op o
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case e'_2.e'_5
o : Ordinal.{u_1}
ho : o ≠ 0
⊢ 2 ^ log 2 o = 2 ^ log 2 o * (o / 2 ^ log 2 o)

Tactic:
div_two_opow_log ho,

Goal state after:
case e'_2.e'_5
o : Ordinal.{u_1}
ho : o ≠ 0
⊢ 2 ^ log 2 o = 2 ^ log 2 o * 1
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:
add_comm,

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 inr.inr
m n : ℕ
hm : 1 < m
hn : ¬n = 0
⊢ ↑(Nat.log m n) = log ↑m ↑n

Tactic:
eq_comm

Goal state after:
case inr.inr
m n : ℕ
hm : 1 < m
hn : ¬n = 0
⊢ log ↑m ↑n = ↑(Nat.log m n)
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: a b : Ordinal.{u_1}
hba : b ≤ a * ω
⊢ nfp (fun x ↦ a + x) b = a * ω

Tactic:
apply le_antisymm (nfp_le_fp (isNormal_add_right a).monotone hba _)
  · rw [← nfp_add_zero]
    exact nfp_monotone (isNormal_add_right a).monotone zero_le
  · rw [← mul_one_add, one_add_omega0]

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

Goal state before:
pp: ⊢ ¬BddAbove {x | x.IsInitial}

Tactic:
rintro ⟨a, ha⟩

Goal state after:
a : Ordinal.{u_1}
ha : a ∈ upperBounds {x | x.IsInitial}
⊢ False
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
⊢ ¬BddAbove {o | IsPrincipal op o}

Tactic:
rintro ⟨a, ha⟩

Goal state after:
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
a : Ordinal.{u_1}
ha : a ∈ upperBounds {o | IsPrincipal op o}
⊢ False
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: ⊢ IsNormal ⇑preOmega

Tactic:
rw [isNormal_iff]

Goal state after:
⊢ StrictMono ⇑preOmega ∧
    ∀ (o : Ordinal.{u_1}), IsSuccLimit o → ∀ (a : Ordinal.{u_1}), (∀ b < o, preOmega b ≤ a) → preOmega o ≤ a
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: case mp
x : Ordinal.{u_1}
⊢ x ∈ range ⇑ω_ → x ∈ {x | ω ≤ x ∧ x.IsInitial}

Tactic:
rintro ⟨a, rfl⟩

Goal state after:
case mp
a : Ordinal.{u_1}
⊢ ω_ a ∈ {x | ω ≤ x ∧ x.IsInitial}
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case ind.mk.hbc.inr
α : Type u_1
IH : ∀ y < #α, ℵ₀ ≤ y → y * y = y
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
this✝ : NoMaxOrder α
g : α × α → α := uncurry max
f : α × α ↪ Lex (α × Lex (α × α)) := { toFun := fun p ↦ toLex (g p, toLex p), inj' := ⋯ }
s : α × α → α × α → Prop := ⇑f ⁻¹'o fun x1 x2 ↦ x1 < x2
this : IsWellOrder (α × α) s
p : α × α
h : (typein s).toRelEmbedding p < type s
q : α
hq' : g p < q
hq : ℵ₀ ≤ #↑(Iio q)
⊢ #↑(Iio q) * #↑(Iio q) < #α

Tactic:
have := mk_Iio_lt q hα
    rwa [IH _ this hq]

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

Goal state before:
pp: ⊢ ℵ_ 0 = ℵ₀

Tactic:
rw [aleph_eq_preAleph, add_zero, preAleph_omega0]

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

Goal state before:
pp: c : Cardinal.{u_1}
⊢ c < ℵ_ 1 ↔ c ≤ ℵ₀

Tactic:
rw [← succ_aleph0, lt_succ_iff]

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

Goal state before:
pp: α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set α
hs : IsCofinal s
hs' : #↑s = Order.cof α
r : ↑s → ↑s → Prop
hr : IsWellOrder (↑s) r
hr' : (#↑s).ord = type r
⊢ ∃ s, IsCofinal s ∧ typeLT ↑s = (Order.cof α).ord

Tactic:
have ht := hs.trans (isCofinal_setOfPred_imp_lt r)

Goal state after:
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set α
hs : IsCofinal s
hs' : #↑s = Order.cof α
r : ↑s → ↑s → Prop
hr : IsWellOrder (↑s) r
hr' : (#↑s).ord = type r
ht : IsCofinal (Subtype.val '' {a | ∀ (b : ↑s), r b a → b < a})
⊢ ∃ s, IsCofinal s ∧ typeLT ↑s = (Order.cof α).ord
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case refine_2.inr
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set α
hs : IsCofinal s
hs' : #↑s = Order.cof α
r : ↑s → ↑s → Prop
hr : IsWellOrder (↑s) r
hr' : (#↑s).ord = type r
ht : IsCofinal (Subtype.val '' {a | ∀ (b : ↑s), r b a → b < a})
x y : ↑(Subtype.val '' {a | ∀ (b : ↑s), r b a → b < a})
hxy : x < y
hxy' : r ⟨↑y, ⋯⟩ ⟨↑x, ⋯⟩
⊢ False

Tactic:
· obtain ⟨x, z, hz, rfl⟩ := x
      exact (hz _ hxy').asymm hxy

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

Goal state before:
pp: ⊢ IsNormal preBeth

Tactic:
rw [isNormal_iff]

Goal state after:
⊢ StrictMono preBeth ∧
    ∀ (o : Ordinal.{u_1}), IsSuccLimit o → ∀ (a : Cardinal.{u_1}), (∀ b < o, preBeth b ≤ a) → preBeth o ≤ a
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: case a
⊢ ∀ (i : ↑(Iio ω)), preBeth ↑i ≤ ℵ₀

Tactic:
rintro ⟨a, ha⟩

Goal state after:
case a
a : Ordinal.{u_1}
ha : a ∈ Iio ω
⊢ preBeth ↑⟨a, ha⟩ ≤ ℵ₀
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: case refine_1
o : Ordinal.{u_1}
⊢ o ∈ range succ → ∃ x < preBeth o, preBeth o ≤ 2 ^ x

Tactic:
rintro ⟨a, rfl⟩

Goal state after:
case refine_1
a : Ordinal.{u_1}
⊢ ∃ x < preBeth (succ a), preBeth (succ a) ≤ 2 ^ x
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

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

Tactic:
simpa using Order.cof_ord_cof o.ToType

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

Goal state before:
pp: case isSuccPrelimit.mpr
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
IH : ∀ b < o, lift.{v, u_1} (preBeth b) = preBeth (Ordinal.lift.{v, u_1} b)
i : Ordinal.{max u_1 v}
hi : i ∈ Iio (Ordinal.lift.{v, u_1} o)
⊢ (fun a ↦ preBeth ↑a) ⟨i, hi⟩ ∈ range fun i ↦ lift.{v, u_1} (preBeth ↑i)

Tactic:
obtain ⟨i, rfl⟩ := Ordinal.mem_range_lift_of_le hi.le

Goal state after:
case isSuccPrelimit.mpr
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
IH : ∀ b < o, lift.{v, u_1} (preBeth b) = preBeth (Ordinal.lift.{v, u_1} b)
i : Ordinal.{u_1}
hi : Ordinal.lift.{v, u_1} i ∈ Iio (Ordinal.lift.{v, u_1} o)
⊢ (fun a ↦ preBeth ↑a) ⟨Ordinal.lift.{v, u_1} i, hi⟩ ∈ range fun i ↦ lift.{v, u_1} (preBeth ↑i)
Module: Mathlib.SetTheory.Cardinal.Arithmetic

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

Tactic:
add_comm,

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

Goal state before:
pp: case inr.inl
a b : Cardinal.{u_1}
ha : a < ℵ₀
hb : ℵ₀ ≤ b
⊢ a + b ≤ max (max a b) ℵ₀

Tactic:
add_comm,

Goal state after:
case inr.inl
a b : Cardinal.{u_1}
ha : a < ℵ₀
hb : ℵ₀ ≤ b
⊢ b + a ≤ max (max a b) ℵ₀
Module: Mathlib.SetTheory.Cardinal.Arithmetic

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

Tactic:
add_comm,

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

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

Tactic:
add_comm,

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

Goal state before:
pp: a : Cardinal.{u_1}
n : ℕ
ha : ℵ₀ ≤ a
⊢ ↑n + a = a

Tactic:
add_comm,

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

Goal state before:
pp: case inl
a b c : Cardinal.{u_1}
h : b = a + c
ha : a < ℵ₀
hb : ℵ₀ ≤ b
this : a < b
⊢ b = c

Tactic:
eq_comm

Goal state after:
case inl
a b c : Cardinal.{u_1}
h : a + c = b
ha : a < ℵ₀
hb : ℵ₀ ≤ b
this : a < b
⊢ b = c
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{v}
inst✝ : Nonempty ι
hf : BddAbove (range f)
c : Cardinal.{v}
⊢ c + ⨆ i, f i = ⨆ i, c + f i

Tactic:
add_comm,

Goal state after:
ι : Type u
f : ι → Cardinal.{v}
inst✝ : Nonempty ι
hf : BddAbove (range f)
c : Cardinal.{v}
⊢ (⨆ i, f i) + c = ⨆ i, c + f i
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}
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
i : Ordinal.{u}
hi : i < o'
⊢ g i hi < o

Tactic:
rw [← hg.2.2]

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}
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
i : Ordinal.{u}
hi : i < o'
⊢ g i hi < o'.blsub g
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' ≤ o

Tactic:
exact hg.1.trans (ord_cof_le o)

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

Goal state before:
pp: o : Ordinal.{u}
S : Set o.ToType
hS : IsCofinal S
hS' : #↑S = Order.cof o.ToType
f : ↑S → Ordinal.{u} := fun s ↦ (typein LT.lt).toRelEmbedding ↑s
⊢ #↑S = o.cof

Tactic:
rwa [cof_toType] at hS'

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

Goal state before:
pp: o : Ordinal.{u_1}
h : o.IsInitial
ho : ω ≤ o
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) o

Tactic:
by
  rw [← h.ord_card]
  apply isPrincipal_add_ord
  rwa [aleph0_le_card]

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

Goal state before:
pp: case inl
c : Cardinal.{u}
n : ℕ
hc : ℵ₀ ≤ c
⊢ c ^ ↑n ≤ max c ℵ₀

Tactic:
exact le_max_of_le_left (power_nat_le hc)

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

Goal state before:
pp: case a
α : Type u_1
h : (#α).IsStrongPrelimit
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha✝ : #α ≠ 0
h' : (#α).IsStrongLimit
ha : ℵ₀ ≤ #α
⊢ #α ≤ #{ s // Bounded r s }

Tactic:
refine @mk_le_of_injective α _ (fun x => Subtype.mk {x} ?_) ?_

Goal state after:
case a.refine_1
α : Type u_1
h : (#α).IsStrongPrelimit
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha✝ : #α ≠ 0
h' : (#α).IsStrongLimit
ha : ℵ₀ ≤ #α
x : α
⊢ Bounded r {x}

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

Goal state before:
pp: α : Type u
β' : Type v
⊢ #↑{f | Surjective f} ≠ 0 ↔ lift.{u, v} #β' ≤ lift.{v, u} #α ∧ (#α = 0 ∨ #β' ≠ 0)

Tactic:
rw [lift_mk_le', and_comm]

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