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

Goal state before:
pp: α : Type u
ι : Sort x
f : ι → Filter α
h : Directed (fun x1 x2 ↦ x1 ≥ x2) f
ne : Nonempty ι
i : ι
x y : Set α
a : ι
⊢ x ∈ (f a).sets → ∀ (x_1 : ι), y ∈ (f x_1).sets → ∃ i, x ∩ y ∈ (f i).sets

Tactic:
hx

Goal state after:
α : Type u
ι : Sort x
f : ι → Filter α
h : Directed (fun x1 x2 ↦ x1 ≥ x2) f
ne : Nonempty ι
i : ι
x y : Set α
a : ι
hx : x ∈ (f a).sets
⊢ ∀ (x_1 : ι), y ∈ (f x_1).sets → ∃ i, x ∩ y ∈ (f i).sets
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
s t x✝ : Set α
⊢ x✝ ∈ 𝓟 s \ 𝓟 t ↔ x✝ ∈ 𝓟 (s \ t)

Tactic:
simp [← le_principal_iff, principal_mono]

Goal state after:
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
f : β → α
hl : l.HasBasis p s
t : Set β
i : ι
h : f ⁻¹' s i ⊆ t
y : α
hy : y ∈ s i
x : β
hx : f x = y
⊢ f x ∈ s i

Tactic:
hx

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
f : β → α
hl : l.HasBasis p s
t : Set β
i : ι
h : f ⁻¹' s i ⊆ t
y : α
hy : y ∈ s i
x : β
hx : f x = y
⊢ y ∈ s i
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
g₁ g₂ : α → Filter β
hf : f₁ ≤ f₂
hg : g₁ ≤ᶠ[f₁] g₂
s : Set β
hs : g₂ ⁻¹' {t | s ∈ t} ∈ f₁
a✝ : α
⊢ g₁ a✝ ≤ g₂ a✝ → a✝ ∈ g₂ ⁻¹' {t | s ∈ t} → s ∈ g₁ a✝

Tactic:
hx

Goal state after:
α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
g₁ g₂ : α → Filter β
hf : f₁ ≤ f₂
hg : g₁ ≤ᶠ[f₁] g₂
s : Set β
hs : g₂ ⁻¹' {t | s ∈ t} ∈ f₁
a✝ : α
hx : g₁ a✝ ≤ g₂ a✝
⊢ a✝ ∈ g₂ ⁻¹' {t | s ∈ t} → s ∈ g₁ a✝
Module: Mathlib.Algebra.Group.TransferInstance

Goal state before:
pp: M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Semigroup β
mul : Mul α := e.mul
x✝ y✝ : α
⊢ e (x✝ * y✝) = e x✝ * e y✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Group.TransferInstance

Goal state before:
pp: M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommSemigroup β
mul : Mul α := e.mul
x✝ y✝ : α
⊢ e (x✝ * y✝) = e x✝ * e y✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Group.TransferInstance

Goal state before:
pp: case one
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : MulOneClass β
one : One α := ⋯
mul : Mul α := ⋯
⊢ e 1 = 1

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Group.TransferInstance

Goal state before:
pp: case mul
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : MulOneClass β
one : One α := e.one
mul : Mul α := e.mul
x✝ y✝ : α
⊢ e (x✝ * y✝) = e x✝ * e y✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Group.TransferInstance

Goal state before:
pp: case one
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Monoid β
one : One α := ⋯
mul : Mul α := ⋯
pow : Pow α ℕ := ⋯
⊢ e 1 = 1

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Group.TransferInstance

Goal state before:
pp: case mul
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Monoid β
one : One α := e.one
mul : Mul α := e.mul
pow : Pow α ℕ := Equiv.pow ℕ e
x✝ y✝ : α
⊢ e (x✝ * y✝) = e x✝ * e y✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Group.TransferInstance

Goal state before:
pp: case npow
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Monoid β
one : One α := e.one
mul : Mul α := e.mul
pow : Pow α ℕ := Equiv.pow ℕ e
x✝ : α
n✝ : ℕ
⊢ e (x✝ ^ n✝) = e x✝ ^ n✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Group.TransferInstance

Goal state before:
pp: case one
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommMonoid β
one : One α := ⋯
mul : Mul α := ⋯
pow : Pow α ℕ := ⋯
⊢ e 1 = 1

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Group.TransferInstance

Goal state before:
pp: case mul
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommMonoid β
one : One α := e.one
mul : Mul α := e.mul
pow : Pow α ℕ := Equiv.pow ℕ e
x✝ y✝ : α
⊢ e (x✝ * y✝) = e x✝ * e y✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Group.TransferInstance

Goal state before:
pp: case npow
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommMonoid β
one : One α := e.one
mul : Mul α := e.mul
pow : Pow α ℕ := Equiv.pow ℕ e
x✝ : α
n✝ : ℕ
⊢ e (x✝ ^ n✝) = e x✝ ^ n✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Group.TransferInstance

Goal state before:
pp: case one
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Group β
one : One α := ⋯
mul : Mul α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
⊢ e 1 = 1

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Group.TransferInstance

Goal state before:
pp: case mul
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Group β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
x✝ y✝ : α
⊢ e (x✝ * y✝) = e x✝ * e y✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Group.TransferInstance

Goal state before:
pp: case inv
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Group β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
x✝ : α
⊢ e x✝⁻¹ = (e x✝)⁻¹

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Group.TransferInstance

Goal state before:
pp: case div
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Group β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
x✝ y✝ : α
⊢ e (x✝ / y✝) = e x✝ / e y✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Group.TransferInstance

Goal state before:
pp: case npow
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Group β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
x✝ : α
n✝ : ℕ
⊢ e (x✝ ^ n✝) = e x✝ ^ n✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Group.TransferInstance

Goal state before:
pp: case zpow
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : Group β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
x✝ : α
n✝ : ℤ
⊢ e (x✝ ^ n✝) = e x✝ ^ n✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Group.TransferInstance

Goal state before:
pp: case one
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommGroup β
one : One α := ⋯
mul : Mul α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
⊢ e 1 = 1

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Group.TransferInstance

Goal state before:
pp: case mul
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommGroup β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
x✝ y✝ : α
⊢ e (x✝ * y✝) = e x✝ * e y✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Group.TransferInstance

Goal state before:
pp: case inv
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommGroup β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
x✝ : α
⊢ e x✝⁻¹ = (e x✝)⁻¹

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Group.TransferInstance

Goal state before:
pp: case div
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommGroup β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
x✝ y✝ : α
⊢ e (x✝ / y✝) = e x✝ / e y✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Group.TransferInstance

Goal state before:
pp: case npow
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommGroup β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
x✝ : α
n✝ : ℕ
⊢ e (x✝ ^ n✝) = e x✝ ^ n✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Group.TransferInstance

Goal state before:
pp: case zpow
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : CommGroup β
one : One α := e.one
mul : Mul α := e.mul
inv : Inv α := e.Inv
div : Div α := e.div
npow : Pow α ℕ := Equiv.pow ℕ e
zpow : Pow α ℤ := Equiv.pow ℤ e
x✝ : α
n✝ : ℤ
⊢ e (x✝ ^ n✝) = e x✝ ^ n✝

Tactic:
exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝³ : Preorder α
inst✝² : IsDirectedOrder α
u : α → β
inst✝¹ : Preorder β
inst✝ : NoMaxOrder β
h : Tendsto u atTop atTop
a : α
b b' : β
hb' : b < b'
a' : α
ha' : a ≤ a'
ha'' : b' ≤ u a'
⊢ ∃ a', a ≤ a' ∧ b < u a'

Tactic:
exact ⟨a', ha', lt_of_lt_of_le hb' ha''⟩

Goal state after:
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 : End R M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → LinearMap.ker (f ^ n) = LinearMap.ker (f ^ m)
m : ℕ
hm : n ≤ m
x : M
hx : x ∈ LinearMap.ker (f ^ (n + m))
⊢ (f ^ n) x = 0

Tactic:
rwa [← hn _ (n.le_add_right m)] at hx

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

Goal state before:
pp: case a
α : Type u
inst✝ : Preorder α
x✝ : ∃ x, IsTop x
t : α
ht : IsTop t
⊢ 1 ≤ cof α

Tactic:
· rw [Cardinal.one_le_iff_ne_zero, cof_ne_zero_iff]
      use t

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

Goal state before:
pp: case refine_1
A : Type u_5
M : Type u_6
inst✝⁶ : Semiring A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module A M
S : Submodule A M
R : Type u_7
inst✝³ : Semiring R
inst✝² : Module R M
inst✝¹ : SMul R A
inst✝ : IsScalarTower R A M
s : Finset M
e : span R ↑s = restrictScalars R S
⊢ restrictScalars R (span A ↑s) ≤ restrictScalars R S

pp: case refine_2
A : Type u_5
M : Type u_6
inst✝⁶ : Semiring A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module A M
S : Submodule A M
R : Type u_7
inst✝³ : Semiring R
inst✝² : Module R M
inst✝¹ : SMul R A
inst✝ : IsScalarTower R A M
s : Finset M
e : span R ↑s = restrictScalars R S
⊢ restrictScalars R S ≤ restrictScalars R (span A ↑s)

Tactic:
· have := span_le.mp e.le
    rwa [restrictScalars_le, span_le]

Goal state after:
case refine_2
A : Type u_5
M : Type u_6
inst✝⁶ : Semiring A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module A M
S : Submodule A M
R : Type u_7
inst✝³ : Semiring R
inst✝² : Module R M
inst✝¹ : SMul R A
inst✝ : IsScalarTower R A M
s : Finset M
e : span R ↑s = restrictScalars R S
⊢ restrictScalars R S ≤ restrictScalars R (span A ↑s)
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
D : Set (Set α)
inst✝ : Preorder α
s : Set (Set α)
hs : ∀ x ∈ s, DirSupInaccOn D x
⊢ DirSupInaccOn D (⋃₀ s)

Tactic:
by
  rw [← dirSupClosedOn_compl, Set.compl_sUnion]
  apply DirSupClosedOn.sInter
  rintro x ⟨x, hx, rfl⟩
  exact (hs x hx).compl

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

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
f : A →+* B
g : B →+* C
h : (g.comp f).Finite
⊢ g.Finite

Tactic:
by
  algebraize [f, g, g.comp f]
  exact .of_restrictScalars_finite A B C

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : SMul α β
inst✝³ : SMul α γ
f : β → γ
inst✝² : Zero β
inst✝¹ : Zero γ
inst✝ : SMulPosMono α γ
b : β
a₁ a₂ : α
ha : a₁ ≤ a₂
hf : ∀ {b₁ b₂ : β}, True
smul : ∀ (a : α) (b : β), True
zero : True
hb : 0 ≤ f b
⊢ a₁ • f b ≤ a₂ • f b

Tactic:
exact smul_le_smul_of_nonneg_right ha hb

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

Goal state before:
pp: c : Cardinal.{u + 1}
h : c < univ.{u, u + 1}
this✝ : c.ord < Ordinal.univ.{u, u + 1}
o : Ordinal.{u}
e : Ordinal.liftPrincipalSeg.toRelEmbedding o = c.ord
this : c.ord.card = c
⊢ ∃ c', c = lift.{u + 1, u} c'

Tactic:
rw [← e, Ordinal.liftPrincipalSeg_coe, ← Ordinal.lift_card] at this

Goal state after:
c : Cardinal.{u + 1}
h : c < univ.{u, u + 1}
this✝ : c.ord < Ordinal.univ.{u, u + 1}
o : Ordinal.{u}
e : Ordinal.liftPrincipalSeg.toRelEmbedding o = c.ord
this : lift.{u + 1, u} o.card = c
⊢ ∃ c', c = lift.{u + 1, u} c'
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case e_2
δ : Sort v
f : (α : Type u_1) → [inst : LinearOrder α] → [WellFoundedLT α] → δ
c :
  ∀ (α : Type u_1) [inst : LinearOrder α] [inst_1 : WellFoundedLT α] (β : Type u_1) [inst_2 : LinearOrder β]
    [inst_3 : WellFoundedLT β], typeLT α = typeLT β → f α = f β
γ : Type u_1
inst✝¹ : LinearOrder γ
inst✝ : WellFoundedLT γ
⊢ linearOrderOfSTO { α := γ, r := fun x1 x2 ↦ x1 < x2, wo := ⋯ }.r = inst✝¹

Tactic:
exact LinearOrder.ext_lt fun _ _ ↦ Iff.rfl

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

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
x : α
⊢ (enum Set.univ ⋯) x = ⟨x, ⋯⟩

Tactic:
rw [← Subsingleton.allEq OrderIso.Set.univ.symm (enum univ .univ)]

Goal state after:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
x : α
⊢ OrderIso.Set.univ.symm x = ⟨x, ⋯⟩
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a : Ordinal.{u_4}
⊢ a - a = 0

Tactic:
by simpa only [add_zero] using add_sub_cancel a 0

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

Goal state before:
pp: a b c : Ordinal.{u_4}
h : b + c ≤ a
⊢ c ≤ a - b

Tactic:
by
  rw [← add_le_add_iff_left b]
  exact h.trans (le_add_sub a b)

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ho : 0 < 0
⊢ False

Tactic:
simp at ho

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

Goal state before:
pp: case refine_2
α : Type u_1
ι : Type u
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
o : Ordinal.{u}
ho : type r = o
f : (a : Ordinal.{u}) → a < o → α
a : α
⊢ a ∈ o.brange f → a ∈ range (familyOfBFamily' r ho f)

Tactic:
· rintro ⟨i, hi, rfl⟩
    exact ⟨_, familyOfBFamily'_enum _ _ _ _ _⟩

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

Goal state before:
pp: case inr
a b c : Ordinal.{u_4}
hb : b ≠ 0
⊢ a < b * (c + 1) ↔ ∃ d < b, a ≤ b * c + d

Tactic:
mul_add_one,

Goal state after:
case inr
a b c : Ordinal.{u_4}
hb : b ≠ 0
⊢ a < b * c + b ↔ ∃ d < b, a ≤ b * c + d
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: ⊢ ord 1 = 1

Tactic:
by simpa using ord_natCast 1

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

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

Tactic:
mul_add_one,

Goal state after:
case add_one
a b : Ordinal.{u_4}
ba : b + a = a
c : Ordinal.{u_4}
IH : (a + b) * (c + 1) = a * (c + 1) + b
⊢ (a + b) * (c + 1) + (a + b) = a * (c + 1 + 1) + b
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case limit
a b : Ordinal.{u_4}
ba : b + a = a
c : Ordinal.{u_4}
l : IsSuccLimit c
IH : ∀ o' < c, (a + b) * (o' + 1) = a * (o' + 1) + b
⊢ (a + b) * (c + 1) = a * (c + 1) + b

Tactic:
mul_add_one,

Goal state after:
case limit
a b : Ordinal.{u_4}
ba : b + a = a
c : Ordinal.{u_4}
l : IsSuccLimit c
IH : ∀ o' < c, (a + b) * (o' + 1) = a * (o' + 1) + b
⊢ (a + b) * c + (a + b) = a * (c + 1) + b
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case limit
a b : Ordinal.{u_4}
ba : b + a = a
c : Ordinal.{u_4}
l : IsSuccLimit c
IH : ∀ o' < c, (a + b) * (o' + 1) = a * (o' + 1) + b
⊢ a * c + (a + b) = a * (c + 1) + b

Tactic:
mul_add_one,

Goal state after:
case limit
a b : Ordinal.{u_4}
ba : b + a = a
c : Ordinal.{u_4}
l : IsSuccLimit c
IH : ∀ o' < c, (a + b) * (o' + 1) = a * (o' + 1) + b
⊢ a * c + (a + b) = a * c + a + b
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a : Ordinal.{u_4}
⊢ a / 0 = 0

Tactic:
by
  change sSup _ = _
  simp

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

Goal state before:
pp: case a
a b : Ordinal.{u_4}
b0 : b ≠ 0
c : Ordinal.{u_4}
⊢ (b * a + c) / b ≤ a + c / b

Tactic:
apply (div_le b0).2
    rw [mul_succ, mul_add, add_assoc, add_lt_add_iff_left]
    apply lt_mul_div_add _ b0

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

Goal state before:
pp: b x y : ℕ
hy : y ≠ 0
h : x ≤ log b y
⊢ b ^ x ≤ y

Tactic:
refine (le_or_gt b 1).elim (fun hb => ?_) fun hb => (le_log_iff_pow_le hb hy).1 h
  rw [log_of_left_le_one hb, Nat.le_zero] at h
  rwa [h, Nat.pow_zero, one_le_iff_ne_zero]

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

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

Tactic:
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']

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

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

Tactic:
mul_add_one,

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

Goal state before:
pp: o : Ordinal.{u_4}
H : ∀ (n : ℕ), ↑n ≤ o
a : Ordinal.{u_4}
h : a < ω
⊢ a < o

Tactic:
let ⟨n, e⟩ := lt_omega0.1 h

Goal state after:
o : Ordinal.{u_4}
H : ∀ (n : ℕ), ↑n ≤ o
a : Ordinal.{u_4}
h : a < ω
n : ℕ
e : a = ↑n
⊢ a < o
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case hab
b u w x v : Ordinal.{u_1}
hw : w < b ^ u
hv : v < x
⊢ b ^ u * v + w < b ^ u * (v + 1)

Tactic:
mul_add_one,

Goal state after:
case hab
b u w x v : Ordinal.{u_1}
hw : w < b ^ u
hv : v < x
⊢ b ^ u * v + w < b ^ u * v + b ^ u
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b c n : ℕ
hc : 1 < c
hb : c ≤ b
⊢ clog b n ≤ clog c n

Tactic:
by
  rw [clog_le_iff_le_pow (lt_of_lt_of_le hc hb)]
  calc
    n ≤ c ^ clog c n := le_pow_clog hc _
    _ ≤ b ^ clog c n := Nat.pow_le_pow_left hb _

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

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

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

Tactic:
· refine eq_of_forall_lt_iff fun c ↦ ?_
      rw [lt_clog_iff_pow_lt (Nat.one_lt_pow (Nat.ne_of_gt hk) hb), Nat.lt_div_iff_mul_lt hk,
        Nat.add_sub_cancel, lt_clog_iff_pow_lt hb, Nat.pow_mul']

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

Goal state before:
pp: case refine_1
ι : Type u_1
inst✝ : Small.{u, u_1} ι
f : ι → Ordinal.{u} → Ordinal.{u}
o : Ordinal.{u}
⊢ derivFamily f o < derivFamily f (succ o)

Tactic:
rw [derivFamily_succ, ← succ_le_iff]
    exact le_nfpFamily _ _

Goal state after:
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]
    exact (isNormal_add_right a).strictMono hbo

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

Goal state before:
pp: case ind.mk
α : 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
⊢ (typein s).toRelEmbedding p < typeLT α

Tactic:
rw [← hα, lt_ord]

Goal state after:
case ind.mk
α : 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
⊢ ((typein s).toRelEmbedding p).card < #α
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case inl
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a * b
ha : a ≠ 0
hb : b ≠ 0
ha' : ℵ₀ ≤ a
⊢ a * b = max a b

Tactic:
exact mul_eq_max_of_aleph0_le_left ha' hb

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

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

Tactic:
use ha

Goal state after:
case right
a b : Cardinal.{u_1}
h : a * b = a
ha : ℵ₀ ≤ a
this : a ≠ 0
⊢ b ≤ a ∧ b ≠ 0
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: b o : Ordinal.{u}
hb : 1 < b
ho : IsPrincipal (fun x1 x2 ↦ x1 * x2) (b ^ o)
x y : Ordinal.{u}
⊢ x < o → y < o → (fun x1 x2 ↦ x1 + x2) x y < o

Tactic:
hx

Goal state after:
b o : Ordinal.{u}
hb : 1 < b
ho : IsPrincipal (fun x1 x2 ↦ x1 * x2) (b ^ o)
x y : Ordinal.{u}
hx : x < o
⊢ y < o → (fun x1 x2 ↦ x1 + x2) x y < o
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case refine_1.inl
a b : Cardinal.{u_1}
h : a + b = a
ha : ℵ₀ ≤ a
⊢ ℵ₀ ≤ a ∧ b ≤ a

Tactic:
use ha

Goal state after:
case right
a b : Cardinal.{u_1}
h : a + b = a
ha : ℵ₀ ≤ a
⊢ b ≤ a
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

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

Tactic:
apply le_antisymm
  · simp_rw [Ordinal.iSup_le_iff, add_one_le_iff]
    exact fun i ↦ (f i).2
  · refine le_of_forall_lt fun b hb ↦ ?_
    obtain ⟨_, ⟨c, rfl⟩, hc : b ≤ _⟩ := hf.isCofinal_range ⟨b, hb⟩
    apply hc.trans_lt
    rw [← add_one_le_iff]
    apply Ordinal.le_iSup

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

Goal state before:
pp: case inl
a o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
i j : Ordinal.{u}
hi : i < o
hj : j < o
hij✝ : i ≤ j
hij : i < j
⊢ f i hi ≤ f j hj

pp: case inr
a o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
i : Ordinal.{u}
hi hj : i < o
hij : i ≤ i
⊢ f i hi ≤ f i hj

Tactic:
· exact (hf.2.1 hi hj hij).le

Goal state after:
case inr
a o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hf : a.IsFundamentalSequence o f
i : Ordinal.{u}
hi hj : i < o
hij : i ≤ i
⊢ f i hi ≤ f i hj
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: case inl
b : Ordinal.{u_1}
hb : ω ≤ b
n : ℕ
⊢ (ω ^ b).card ≤ max (↑n).card b.card

Tactic:
apply (card_opow_le_of_omega0_le_left le_rfl _).trans

Goal state after:
case inl
b : Ordinal.{u_1}
hb : ω ≤ b
n : ℕ
⊢ max ω.card b.card ≤ max (↑n).card b.card
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
⊢ (o.blsub f).cof ≤ Cardinal.lift.{v, u} o.card

Tactic:
← mk_toType o

Goal state after:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
⊢ (o.blsub f).cof ≤ Cardinal.lift.{v, u} #o.ToType
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ (2 ^ c) ^ c ≤ 2 ^ c

Tactic:
· rw [← power_mul, mul_eq_self h]

Goal state after: