mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Noetherian.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : M →ₗ[R] M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → (f ^ n).ker = (f ^ m).ker
m : ℕ
hm : n ≤ m
⊢ ⨆ m, (f ^ m).ker = (f ^ m).ker

Tactic:
refine le_antisymm (iSup_le fun l ↦ ?_) (le_iSup (fun i ↦ LinearMap.ker (f ^ i)) m)

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : M →ₗ[R] M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → (f ^ n).ker = (f ^ m).ker
m : ℕ
hm : n ≤ m
l : ℕ
⊢ (f ^ l).ker ≤ (f ^ m).ker
Module: Mathlib.RingTheory.Noetherian.Defs

Goal state before:
pp: case inl
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : M →ₗ[R] M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → (f ^ n).ker = (f ^ m).ker
m : ℕ
hm : n ≤ m
l : ℕ
h : m ≤ l
⊢ (f ^ n).ker ≤ (f ^ m).ker

Tactic:
hn _ hm

Goal state after:
case inl
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : M →ₗ[R] M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → (f ^ n).ker = (f ^ m).ker
m : ℕ
hm : n ≤ m
l : ℕ
h : m ≤ l
⊢ (f ^ m).ker ≤ (f ^ m).ker
Module: Mathlib.Order.SuccPred.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α ≤i β
⊢ IsSuccPrelimit (f a) ↔ IsSuccPrelimit a

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
β : Type u_2
a : α
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α ≤i β
⊢ IsSuccPrelimit (f a) → IsSuccPrelimit a

case mpr
α : Type u_1
β : Type u_2
a : α
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α ≤i β
⊢ IsSuccPrelimit a → IsSuccPrelimit (f a)
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_3
P : Type u_4
inst✝³ : Semiring S
inst✝² : AddCommMonoid P
inst✝¹ : Module S P
σ : R →+* S
inst✝ : RingHomSurjective σ
f : M →ₛₗ[σ] P
hf : Function.Injective ⇑f
N : Submodule R M
hfn : (map f N).FG
t : Finset P
ht : span S ↑t = map f N
⊢ map f N ≤ f.range

Tactic:
← map_top

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type u_3
P : Type u_4
inst✝³ : Semiring S
inst✝² : AddCommMonoid P
inst✝¹ : Module S P
σ : R →+* S
inst✝ : RingHomSurjective σ
f : M →ₛₗ[σ] P
hf : Function.Injective ⇑f
N : Submodule R M
hfn : (map f N).FG
t : Finset P
ht : span S ↑t = map f N
⊢ map f N ≤ map f ⊤
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: case a
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
M' : Submodule R M
N : ℕ →o Submodule R M
H : iSup ⇑N = M'
S : Finset M
hS : span R ↑S = M'
f : ↥S → ℕ
hf : ∀ (s : ↥S), ↑s ∈ N (f s)
⊢ N (S.attach.sup f) ≤ M'

Tactic:
rw [← H]
    exact le_iSup ..

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

Goal state before:
pp: 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
⊢ s.FG ↔ IsCompactElement s

Tactic:
constructor

Goal state after:
case mp
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 := ⋯
supr_rw : ∀ (t : Finset M), ⨆ x ∈ t, sp x = ⨆ x ∈ ↑t, sp x
⊢ s.FG → IsCompactElement s

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 := ⋯
supr_rw : ∀ (t : Finset M), ⨆ x ∈ t, sp x = ⨆ x ∈ ↑t, sp x
⊢ IsCompactElement s → s.FG
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁸ : Ring α
inst✝⁷ : PartialOrder α
inst✝⁶ : IsOrderedRing α
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module α β
inst✝¹ : PosSMulStrictMono α β
inst✝ : PosSMulReflectLT α β
ha : a < 0
⊢ a • b < 0 ↔ 0 < b

Tactic:
by
  simpa only [smul_zero] using smul_lt_smul_iff_of_neg_left ha (b₂ := (0 : β))

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s : Set α
D : Set (Set α)
inst✝ : CompleteLattice α
⊢ DirSupInaccOn D s ↔
    ∀ ⦃d : Set α⦄, d ∈ D → d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → sSup d ∈ s → (d ∩ s).Nonempty

Tactic:
simp [DirSupInaccOn, isLUB_iff_sSup_eq]

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : ConditionallyCompleteLinearOrder β
ι : Sort u_4
inst✝ : Nonempty ι
g : ι → α
hf : IsNormal f
hg : BddAbove (range g)
⊢ (range fun i ↦ f (g i)) = f '' range g

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : ConditionallyCompleteLinearOrder β
ι : Sort u_4
inst✝ : Nonempty ι
g : ι → α
hf : IsNormal f
hg : BddAbove (range g)
x✝ : β
⊢ (x✝ ∈ range fun i ↦ f (g i)) ↔ x✝ ∈ f '' range g
Module: Mathlib.Order.IsNormal

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
hf : IsNormal f
x : β
h₁ : (f ⁻¹' Iic x).Nonempty
h₂ : BddAbove (f ⁻¹' Iic x)
hy : sSup (f ⁻¹' Iic x) ∈ Iic (sSup (f ⁻¹' Iic x))
⊢ sSup (Iic x) ≤ x

Tactic:
csSup_Iic

Goal state after:
case inr
α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
hf : IsNormal f
x : β
h₁ : (f ⁻¹' Iic x).Nonempty
h₂ : BddAbove (f ⁻¹' Iic x)
hy : sSup (f ⁻¹' Iic x) ∈ Iic (sSup (f ⁻¹' Iic x))
⊢ x ≤ x
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝⁴ : LinearOrder α
inst✝³ : WellFoundedLT α
inst✝² : SuccOrder α
inst✝¹ : LinearOrder β
inst✝ : OrderBot α
g : α → β
hf : IsNormal f
hg : IsNormal g
⊢ f = g ↔ f ⊥ = g ⊥ ∧ ∀ (a : α), f a = g a → f (succ a) = g (succ a)

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
β : Type u_2
f : α → β
inst✝⁴ : LinearOrder α
inst✝³ : WellFoundedLT α
inst✝² : SuccOrder α
inst✝¹ : LinearOrder β
inst✝ : OrderBot α
g : α → β
hf : IsNormal f
hg : IsNormal g
⊢ f = g → f ⊥ = g ⊥ ∧ ∀ (a : α), f a = g a → f (succ a) = g (succ a)

case mpr
α : Type u_1
β : Type u_2
f : α → β
inst✝⁴ : LinearOrder α
inst✝³ : WellFoundedLT α
inst✝² : SuccOrder α
inst✝¹ : LinearOrder β
inst✝ : OrderBot α
g : α → β
hf : IsNormal f
hg : IsNormal g
⊢ (f ⊥ = g ⊥ ∧ ∀ (a : α), f a = g a → f (succ a) = g (succ a)) → f = g
Module: Mathlib.SetTheory.Ordinal.Univ

Goal state before:
pp: b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝ : IsWellOrder β s
⊢ type s ∈ Set.range ⇑liftInitialSeg.toRelEmbedding ↔ type s < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})

Tactic:
constructor

Goal state after:
case mp
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝ : IsWellOrder β s
⊢ type s ∈ Set.range ⇑liftInitialSeg.toRelEmbedding → type s < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})

case mpr
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝ : IsWellOrder β s
⊢ type s < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u}) → type s ∈ Set.range ⇑liftInitialSeg.toRelEmbedding
Module: Mathlib.SetTheory.Ordinal.Univ

Goal state before:
pp: α : Type u
⊢ Small.{v, u} α ↔ ∃ c', lift.{v + 1, u} #α = lift.{max u (v + 1), v} c'

Tactic:
constructor

Goal state after:
case mp
α : Type u
⊢ Small.{v, u} α → ∃ c', lift.{v + 1, u} #α = lift.{max u (v + 1), v} c'

case mpr
α : Type u
⊢ (∃ c', lift.{v + 1, u} #α = lift.{max u (v + 1), v} c') → Small.{v, u} α
Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
⊢ (#α).ord = typeLT α

Tactic:
by
  rw [← ord_cof_eq_type_lt, cof_eq_cardinalMk]

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
f : α → α
H : StrictMono (Subtype.val ∘ ⇑(enum s hs))
⊢ Subtype.val ∘ ⇑(enum s hs) = f ↔ StrictMono f ∧ range f = s

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
f : α → α
H : StrictMono (Subtype.val ∘ ⇑(enum s hs))
⊢ Subtype.val ∘ ⇑(enum s hs) = f → StrictMono f ∧ range f = s

case mpr
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
f : α → α
H : StrictMono (Subtype.val ∘ ⇑(enum s hs))
⊢ StrictMono f ∧ range f = s → Subtype.val ∘ ⇑(enum s hs) = f
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b c : Ordinal.{u_4}
hc : IsSuccLimit c
⊢ (∃ d < c, a ≤ b + d) ↔ ∃ d < c, a < b + d

Tactic:
constructor

Goal state after:
case mp
a b c : Ordinal.{u_4}
hc : IsSuccLimit c
⊢ (∃ d < c, a ≤ b + d) → ∃ d < c, a < b + d

case mpr
a b c : Ordinal.{u_4}
hc : IsSuccLimit c
⊢ (∃ d < c, a < b + d) → ∃ d < c, a ≤ b + d
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
⊢ lift.{max v w, u} (type r) ≤ lift.{max u w, v} (type s) ↔ Nonempty (r ≼i s)

Tactic:
constructor

Goal state after:
case mp
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
⊢ lift.{max v w, u} (type r) ≤ lift.{max u w, v} (type s) → Nonempty (r ≼i s)

case mpr
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
⊢ Nonempty (r ≼i s) → lift.{max v w, u} (type r) ≤ lift.{max u w, v} (type s)
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
⊢ lift.{max v w, u} (type r) < lift.{max u w, v} (type s) ↔ Nonempty (r ≺i s)

Tactic:
constructor

Goal state after:
case mp
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
⊢ lift.{max v w, u} (type r) < lift.{max u w, v} (type s) → Nonempty (r ≺i s)

case mpr
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
⊢ Nonempty (r ≺i s) → lift.{max v w, u} (type r) < lift.{max u w, v} (type s)
Module: Mathlib.SetTheory.Ordinal.Family

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

Tactic:
constructor

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

case mpr
s : Set Ordinal.{u_3}
⊢ BddAbove s → BddAbove ((fun x ↦ x + 1) '' s)
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: case neg
s : Set Ordinal.{u_3}
hs : ¬BddAbove s
⊢ sSup s ≤ sSup ((fun x ↦ x + 1) '' s)

Tactic:
rw [csSup_of_not_bddAbove hs, csSup_of_not_bddAbove (s := _ '' _)]

Goal state after:
case neg
s : Set Ordinal.{u_3}
hs : ¬BddAbove s
⊢ ¬BddAbove ((fun x ↦ x + 1) '' s)
Module: Mathlib.SetTheory.Ordinal.Enum

Goal state before:
pp: s : Set Ordinal.{u}
hs : ¬BddAbove s
o : Ordinal.{u}
⊢ (s ∩ {b | ∀ c < o, enumOrd s c < b}).Nonempty

Tactic:
by
  rw [not_bddAbove_iff] at hs
  obtain ⟨a, ha⟩ := bddAbove_of_small (s := enumOrd s '' Iio o)
  obtain ⟨b, hb, hba⟩ := hs a
  exact ⟨b, hb, fun c hc ↦ (ha (mem_image_of_mem _ hc)).trans_lt hba⟩

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

Goal state before:
pp: s : Set Ordinal.{u}
hs : ¬BddAbove s
a : Ordinal.{u}
t : Set Ordinal.{u} := {b | a ≤ enumOrd s b}
⊢ a ∈ range (enumOrd s) ↔ a ∈ s

Tactic:
constructor

Goal state after:
case mp
s : Set Ordinal.{u}
hs : ¬BddAbove s
a : Ordinal.{u}
t : Set Ordinal.{u} := ⋯
⊢ a ∈ range (enumOrd s) → a ∈ s

case mpr
s : Set Ordinal.{u}
hs : ¬BddAbove s
a : Ordinal.{u}
t : Set Ordinal.{u} := ⋯
⊢ a ∈ s → a ∈ range (enumOrd s)
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
⊢ typeLT α ∈ range succ ↔ ∃ x, IsTop x

Tactic:
constructor

Goal state after:
case mp
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
⊢ typeLT α ∈ range succ → ∃ x, IsTop x

case mpr
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
⊢ (∃ x, IsTop x) → typeLT α ∈ range succ
Module: Mathlib.SetTheory.Ordinal.Enum

Goal state before:
pp: s : Set Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
hs : ¬BddAbove s
⊢ enumOrd s = f ↔ StrictMono f ∧ range f = s

Tactic:
constructor

Goal state after:
case mp
s : Set Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
hs : ¬BddAbove s
⊢ enumOrd s = f → StrictMono f ∧ range f = s

case mpr
s : Set Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
hs : ¬BddAbove s
⊢ StrictMono f ∧ range f = s → enumOrd s = f
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: c : Cardinal.{u_1}
o : Ordinal.{u_1}
α β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : (#α).ord = type r
⊢ (#α).ord ≤ type s ↔ #α ≤ (type s).card

Tactic:
constructor

Goal state after:
case mp
c : Cardinal.{u_1}
o : Ordinal.{u_1}
α β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : (#α).ord = type r
⊢ (#α).ord ≤ type s → #α ≤ (type s).card

case mpr
c : Cardinal.{u_1}
o : Ordinal.{u_1}
α β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : (#α).ord = type r
⊢ #α ≤ (type s).card → (#α).ord ≤ type s
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b c : Ordinal.{u_4}
ba : b + a = a
⊢ (a + b) * (c + 1) = a * (c + 1) + b

Tactic:
by
  induction c using limitRecOn with
  | zero => simp
  | add_one c IH => rw [mul_add_one, IH, ← add_assoc, add_assoc _ b, ba, ← mul_add_one]
  | limit c l IH => rw [mul_add_one, add_mul_limit_aux ba l IH, mul_add_one, add_assoc]

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

Goal state before:
pp: case a
o o' : Ordinal.{max u v}
f : (a : Ordinal.{max u v}) → a < o → Ordinal.{max u v w}
hf : ∀ {i j : Ordinal.{max u v}} (hi : i < o) (hj : j < o), i ≤ j → f i hi ≤ f j hj
g : (a : Ordinal.{max u v}) → a < o' → Ordinal.{max u v}
hg : o'.blsub g = o
i : Ordinal.{max u v}
hi : i < o
⊢ f i hi ≤ o'.bsup fun a ha ↦ f (g a ha) ⋯

Tactic:
rw [← hg, lt_blsub_iff] at hi

Goal state after:
case a
o o' : Ordinal.{max u v}
f : (a : Ordinal.{max u v}) → a < o → Ordinal.{max u v w}
hf : ∀ {i j : Ordinal.{max u v}} (hi : i < o) (hj : j < o), i ≤ j → f i hi ≤ f j hj
g : (a : Ordinal.{max u v}) → a < o' → Ordinal.{max u v}
hg : o'.blsub g = o
i : Ordinal.{max u v}
hi✝ : i < o
hi : ∃ i_1, ∃ (hi : i_1 < o'), i ≤ g i_1 hi
⊢ f i hi✝ ≤ o'.bsup fun a ha ↦ f (g a ha) ⋯
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: 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:
constructor

Goal state after:
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

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
Module: Mathlib.SetTheory.Ordinal.Exponential

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

Tactic:
induction a using limitRecOn with

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

Goal state before:
pp: case inr.inr
o : Ordinal.{u_1}
s : Set Ordinal.{u_1}
hs : s.Nonempty
ho : 0 < o
⊢ o * sSup s = sSup ((fun x ↦ o * x) '' s)

Tactic:
by_cases bdd : BddAbove s

Goal state after:
case pos
o : Ordinal.{u_1}
s : Set Ordinal.{u_1}
hs : s.Nonempty
ho : 0 < o
bdd : BddAbove s
⊢ o * sSup s = sSup ((fun x ↦ o * x) '' s)

case neg
o : Ordinal.{u_1}
s : Set Ordinal.{u_1}
hs : s.Nonempty
ho : 0 < o
bdd : ¬BddAbove s
⊢ o * sSup s = sSup ((fun x ↦ o * x) '' s)
Module: Mathlib.Data.Nat.Log

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

Tactic:
· rcases Nat.lt_or_ge 1 b with hb | hb
      · refine eq_of_forall_le_iff fun c ↦ ?_
        rw [le_log_iff_pow_le (Nat.one_lt_pow (Nat.ne_of_gt hk) hb) hn, Nat.le_div_iff_mul_le hk,
          le_log_iff_pow_le hb hn, Nat.pow_mul']
      · 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 inl
o : Ordinal.{u_4}
ho : o < ω
⊢ (∃ n, o = ↑n) ∨ ω ≤ o

pp: case inr
o : Ordinal.{u_4}
ho : ω ≤ o
⊢ (∃ n, o = ↑n) ∨ ω ≤ o

Tactic:
· exact Or.inl <| lt_omega0.1 ho

Goal state after:
case inr
o : Ordinal.{u_4}
ho : ω ≤ o
⊢ (∃ n, o = ↑n) ∨ ω ≤ o
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b n : ℕ
hb : 1 < b
hn : 1 < n
⊢ 0 < clog b n

Tactic:
clog,

Goal state after:
b n : ℕ
hb : 1 < b
hn : 1 < n
⊢ 0 < if 1 < b ∧ 1 < n then (clog.go n b n).snd + 1 else 0
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ IsSuccLimit c.ord

Tactic:
constructor

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

case isSuccPrelimit
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ IsSuccPrelimit c.ord
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case a
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
a : Ordinal.{u}
l : List ι
⊢ f i (List.foldr f a l) ≤ ⨆ i, List.foldr f a i

Tactic:
exact Ordinal.le_iSup _ (i::l)

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

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

Tactic:
suffices (k - 1) / k = 0 by grind [clog_of_left_le_one, Nat.pow_le_one_iff]

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

Goal state before:
pp: b x : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
y : Ordinal.{u_1}
⊢ log b x = y ↔ b ^ y ≤ x ∧ x < b ^ (y + 1)

Tactic:
constructor

Goal state after:
case mp
b x : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
y : Ordinal.{u_1}
⊢ log b x = y → b ^ y ≤ x ∧ x < b ^ (y + 1)

case mpr
b x : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
y : Ordinal.{u_1}
⊢ b ^ y ≤ x ∧ x < b ^ (y + 1) → log b x = y
Module: Mathlib.SetTheory.Ordinal.Exponential

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

Tactic:
constructor

Goal state after:
case left
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hw : w < b ^ u
⊢ b ^ (u + log b v) ≤ b ^ u * v + w

case right
b u v w : Ordinal.{u_1}
hb : 1 < b
hv : v ≠ 0
hw : w < b ^ u
⊢ b ^ u * v + w < b ^ (u + log b v + 1)
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
⊢ IsPrincipal (Function.swap op) o ↔ IsPrincipal op o

Tactic:
constructor

Goal state after:
case mp
o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
⊢ IsPrincipal (Function.swap op) o → IsPrincipal op o

case mpr
o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
⊢ IsPrincipal op o → IsPrincipal (Function.swap op) o
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: ⊢ nfp id = id

Tactic:
ext

Goal state after:
x✝ : Ordinal.{u_1}
⊢ nfp id x✝ = id x✝
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: a b : Ordinal.{u_1}
hb : b ≠ 0
⊢ (∃ c, (∃ c_1 < b, ∃ n, c < ω ^ c_1 * ↑n) ∧ ∃ n, a < ω ^ c * ↑n) ↔ ∃ c < b, ∃ n, a < ω ^ (ω ^ c * ↑n)

Tactic:
constructor

Goal state after:
case mp
a b : Ordinal.{u_1}
hb : b ≠ 0
⊢ (∃ c, (∃ c_1 < b, ∃ n, c < ω ^ c_1 * ↑n) ∧ ∃ n, a < ω ^ c * ↑n) → ∃ c < b, ∃ n, a < ω ^ (ω ^ c * ↑n)

case mpr
a b : Ordinal.{u_1}
hb : b ≠ 0
⊢ (∃ c < b, ∃ n, a < ω ^ (ω ^ c * ↑n)) → ∃ c, (∃ c_1 < b, ∃ n, c < ω ^ c_1 * ↑n) ∧ ∃ n, a < ω ^ c * ↑n
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: ⊢ nfp 0 = id

Tactic:
ext

Goal state after:
x✝ : Ordinal.{u_1}
⊢ nfp 0 x✝ = id x✝
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: o : Ordinal.{u}
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) o ↔ ∀ a < o, a + o = o

Tactic:
by
  refine ⟨fun ho a hao => ?_, fun h a b hao hbo => ?_⟩
  · rcases lt_or_ge 1 o with ho₁ | ho₁
    · exact op_eq_self_of_isPrincipal hao (isNormal_add_right a) ho
        (isSuccLimit_of_isPrincipal_add ho₁ ho)
    · cases le_one_iff.1 ho₁ <;> simp_all
  · rw [← h a hao]
    exact (isNormal_add_right a).strictMono hbo

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

Goal state before:
pp: a : Ordinal.{u}
ha : ¬IsPrincipal (fun x1 x2 ↦ x1 + x2) a
⊢ ∃ b < a, ∃ c < a, b + c = a

Tactic:
rw [not_isPrincipal_iff] at ha
  rcases ha with ⟨b, hb, c, hc, H⟩
  refine
    ⟨b, hb, _, lt_of_le_of_ne (sub_le_self a b) fun hab => ?_, Ordinal.add_sub_cancel_of_le hb.le⟩
  rw [← sub_le, hab] at H
  exact H.not_gt hc

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

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

Tactic:
constructor

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

case mpr
x : Ordinal.{u_1}
⊢ x ∈ {x | ω ≤ x ∧ x.IsInitial} → x ∈ range ⇑ω_
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: o : Ordinal.{u}
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) o ↔ o = 0 ∨ o ∈ Set.range fun x ↦ ω ^ x

Tactic:
constructor

Goal state after:
case mp
o : Ordinal.{u}
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) o → o = 0 ∨ o ∈ Set.range fun x ↦ ω ^ x

case mpr
o : Ordinal.{u}
⊢ (o = 0 ∨ o ∈ Set.range fun x ↦ ω ^ x) → IsPrincipal (fun x1 x2 ↦ x1 + x2) o
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: a b : Ordinal.{u_1}
⊢ a * b = b ↔ a ^ ω ∣ b

Tactic:
by
  rcases eq_zero_or_pos a with ha | ha
  · rw [ha, zero_mul, zero_opow omega0_ne_zero, zero_dvd_iff]
    exact eq_comm
  refine ⟨fun hab => ?_, fun h => ?_⟩
  · rw [dvd_iff_mod_eq_zero]
    rw [← div_add_mod b (a ^ ω), mul_add, ← mul_assoc, ← opow_one_add, one_add_omega0,
      add_left_cancel_iff] at hab
    rcases eq_zero_or_opow_omega0_le_of_mul_eq_right hab with hab | hab
    · exact hab
    refine (not_lt_of_ge hab (mod_lt b (opow_ne_zero ω ?_))).elim
    rwa [← pos_iff_ne_zero]
  obtain ⟨c, hc⟩ := h
  rw [hc, ← mul_assoc, ← opow_one_add, one_add_omega0]

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

Goal state before:
pp: case type
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
⊢ (∃ x, IsTop x) ↔ ∃ x, IsMax x

Tactic:
isTop_iff_isMax

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

Goal state before:
pp: case right
a b : Cardinal.{u_1}
h : a * b = a
ha : ℵ₀ ≤ a
this : a ≠ 0
⊢ b ≤ a ∧ b ≠ 0

Tactic:
constructor

Goal state after:
case right.left
a b : Cardinal.{u_1}
h : a * b = a
ha : ℵ₀ ≤ a
this : a ≠ 0
⊢ b ≤ a

case right.right
a b : Cardinal.{u_1}
h : a * b = a
ha : ℵ₀ ≤ a
this : a ≠ 0
⊢ b ≠ 0
Module: Mathlib.SetTheory.Cardinal.Aleph

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

Tactic:
constructor

Goal state after:
case isSuccPrelimit.mp
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
IH : ∀ b < o, lift.{v, u_1} (preBeth b) = preBeth (Ordinal.lift.{v, u_1} b)
x : Cardinal.{max u_1 v}
⊢ (x ∈ range fun i ↦ lift.{v, u_1} (preBeth ↑i)) → x ∈ range fun a ↦ preBeth ↑a

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)
x : Cardinal.{max u_1 v}
⊢ (x ∈ range fun a ↦ preBeth ↑a) → x ∈ range fun i ↦ lift.{v, u_1} (preBeth ↑i)