mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : Ring α
x y x✝¹ : α
x✝ : ∃ a b, a * (x + y) + b * y = x✝¹
a b : α
h : a * (x + y) + b * y = x✝¹
⊢ a * x + (a * y + b * y) = x✝¹

Tactic:
← add_assoc,

Goal state after:
α : Type u
inst✝ : Ring α
x y x✝¹ : α
x✝ : ∃ a b, a * (x + y) + b * y = x✝¹
a b : α
h : a * (x + y) + b * y = x✝¹
⊢ a * x + a * y + b * y = x✝¹
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
⊢ (LinearMap.toSpanSingleton R R (1 - e)).ker = Ideal.span {e}

Tactic:
ker_toSpanSingleton_eq_span he.one_sub,

Goal state after:
R : Type u_1
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
⊢ Ideal.span {1 - (1 - e)} = Ideal.span {e}
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint ↑I ↑S
⊢ ∃ p, p.IsPrime ∧ I ≤ p ∧ Disjoint ↑p ↑S

Tactic:
have ⟨p, hIp, hp⟩ := zorn_le_nonempty₀ {p : Ideal α | Disjoint (p : Set α) S}
    (fun c hc hc' x hx ↦ ?_) I disjoint

Goal state after:
case refine_2
α : Type u
inst✝ : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint ↑I ↑S
p : Ideal α
hIp : I ≤ p
hp : Maximal (fun x ↦ x ∈ {p | Disjoint ↑p ↑S}) p
⊢ ∃ p, p.IsPrime ∧ I ≤ p ∧ Disjoint ↑p ↑S

case refine_1
α : Type u
inst✝ : CommSemiring α
I : Ideal α
S : Submonoid α
disjoint : Disjoint ↑I ↑S
c : Set (Ideal α)
hc : c ⊆ {p | Disjoint ↑p ↑S}
hc' : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
x : Ideal α
hx : x ∈ c
⊢ ∃ ub ∈ {p | Disjoint ↑p ↑S}, ∀ z ∈ c, z ≤ ub
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: n : ℕ
⊢ ∑ m ∈ range (n + 1), (-1) ^ m * ↑(n.choose m) = if n = 0 then 1 else 0

Tactic:
cases n with

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

Goal state before:
pp: α : Type u_2
inst✝¹ : CommSemiring α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : s.sum ^ (s.card * n + 1) ∈ span ↑(Multiset.map (fun x ↦ x ^ (n + 1)) s).toFinset
c : ℕ
_hc : c ∈ Finset.range ((s.card + 1) * n + 1 + 1)
h : c ≤ n
⊢ s.card * n + (1 + n) - c = s.card * n + 1 + (n - c)

Tactic:
← add_assoc,

Goal state after:
α : Type u_2
inst✝¹ : CommSemiring α
inst✝ : DecidableEq α
n : ℕ
a : α
s : Multiset α
hs : s.sum ^ (s.card * n + 1) ∈ span ↑(Multiset.map (fun x ↦ x ^ (n + 1)) s).toFinset
c : ℕ
_hc : c ∈ Finset.range ((s.card + 1) * n + 1 + 1)
h : c ≤ n
⊢ s.card * n + 1 + n - c = s.card * n + 1 + (n - c)
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: case succ
α : Type u_2
inst✝ : CommSemiring α
s : Set α
hs : ∃ l, (Finsupp.linearCombination α Subtype.val) l = 1
n : ℕ
⊢ 1 ∈ span ((fun x ↦ x ^ (n + 1)) '' s)

Tactic:
rcases hs with ⟨f, hf⟩

Goal state after:
case succ
α : Type u_2
inst✝ : CommSemiring α
s : Set α
n : ℕ
f : ↑s →₀ α
hf : (Finsupp.linearCombination α Subtype.val) f = 1
⊢ 1 ∈ span ((fun x ↦ x ^ (n + 1)) '' s)
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
p : ι → Prop
s : ι → Set α
h : IsBasis p s
⊢ h.filter = generate {U | ∃ i, p i ∧ s i = U}

Tactic:
IsBasis.filter,

Goal state after:
α : Type u_1
ι : Sort u_4
p : ι → Prop
s : ι → Set α
h : IsBasis p s
⊢ h.filterBasis.filter = generate {U | ∃ i, p i ∧ s i = U}
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
f : Filter α
p : α → Prop
q : Prop
⊢ (∃ᶠ (x : α) in f, p x ∧ q) ↔ (∃ᶠ (x : α) in f, p x) ∧ q

Tactic:
by
  simp only [@and_comm _ q, frequently_and_distrib_left]

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:

Tactic:
f '' V ∩ Z = f '' (V ∩ f ⁻¹' Z) := by rw [image_inter_preimage]
      _ ⊆ f '' (V ∩ W) := by gcongr
      _ = f '' f ⁻¹' U := by rw [h]
      _ ⊆ U := image_preimage_subset f U

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝³ : Preorder α
inst✝² : IsDirectedOrder α
inst✝¹ : Preorder β
inst✝ : IsDirectedOrder β
f : α → β
hf : Monotone f
b : β
this✝ : Nonempty α
g : β → α
hfg : ∀ (c : β), b ≤ c → f (g c) = c
hgle : ∀ (c : β), b ≤ c → ∀ (a : α), f a ≤ c ↔ a ≤ g c
this : Nonempty α
a : α
a✝ : True
c : β
hac : f a ≤ c
⊢ b ≤ c → c ∈ f '' Ici a

Tactic:
hbc

Goal state after:
α : Type u_3
β : Type u_4
inst✝³ : Preorder α
inst✝² : IsDirectedOrder α
inst✝¹ : Preorder β
inst✝ : IsDirectedOrder β
f : α → β
hf : Monotone f
b : β
this✝ : Nonempty α
g : β → α
hfg : ∀ (c : β), b ≤ c → f (g c) = c
hgle : ∀ (c : β), b ≤ c → ∀ (a : α), f a ≤ c ↔ a ≤ g c
this : Nonempty α
a : α
a✝ : True
c : β
hac : f a ≤ c
hbc : b ≤ c
⊢ c ∈ f '' Ici a
Module: Mathlib.Algebra.Module.TransferInstance

Goal state before:
pp: R : Type u_1
α : Type u_2
β : Type u_3
inst✝⁸ : Semiring R
A : Type u_4
inst✝⁷ : Semiring A
inst✝⁶ : Module R A
inst✝⁵ : AddCommMonoid α
inst✝⁴ : AddCommMonoid β
inst✝³ : Module A β
inst✝² : Module R α
inst✝¹ : Module R β
inst✝ : IsScalarTower R A β
e : α ≃ₗ[R] β
this : Module A α := AddEquiv.module A e.toAddEquiv
x : R
y : A
z : α
⊢ (x • y) • z = x • y • z

Tactic:
simp only [Equiv.smul_def, smul_assoc]

Goal state after:
R : Type u_1
α : Type u_2
β : Type u_3
inst✝⁸ : Semiring R
A : Type u_4
inst✝⁷ : Semiring A
inst✝⁶ : Module R A
inst✝⁵ : AddCommMonoid α
inst✝⁴ : AddCommMonoid β
inst✝³ : Module A β
inst✝² : Module R α
inst✝¹ : Module R β
inst✝ : IsScalarTower R A β
e : α ≃ₗ[R] β
this : Module A α := AddEquiv.module A e.toAddEquiv
x : R
y : A
z : α
⊢ { toFun := (↑e).toFun, invFun := e.invFun, left_inv := ⋯, right_inv := ⋯ }.symm
      (x • y • { toFun := (↑e).toFun, invFun := e.invFun, left_inv := ⋯, right_inv := ⋯ } z) =
    x •
      { toFun := (↑e).toFun, invFun := e.invFun, left_inv := ⋯, right_inv := ⋯ }.symm
        (y • { toFun := (↑e).toFun, invFun := e.invFun, left_inv := ⋯, right_inv := ⋯ } z)
Module: Mathlib.Data.Set.Finite.Lemmas

Goal state before:
pp: case inr
α : Type u
β : Type v
inst✝¹ : Nonempty α
inst✝ : LinearOrder β
s : Set α
f : α → β
h : s.Finite
hs : s.Nonempty
x₀ : α
left✝ : x₀ ∈ s
hx₀ : ∀ b ∈ s, f x₀ ≤ f b
⊢ ∃ a, ∀ b ∈ s, f a ≤ f b

Tactic:
exact ⟨x₀, fun x hx => hx₀ x hx⟩

Goal state after:
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
r : α → α → Prop
h : IsWellFounded α r
a b : α
hb : b ∈ Ici a
hb' : ∀ x ∈ Ici a, ¬r x b
c : α
hc : r c b
⊢ c < b

Tactic:
by_contra! hc'

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
r : α → α → Prop
h : IsWellFounded α r
a b : α
hb : b ∈ Ici a
hb' : ∀ x ∈ Ici a, ¬r x b
c : α
hc : r c b
hc' : b ≤ c
⊢ False
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 : IsCompactElement s
⊢ s.FG

Tactic:
CompleteLattice.isCompactElement_iff_exists_le_sSup_of_le_sSup

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
⊢ s.FG
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁸ : Semiring α
inst✝⁷ : PartialOrder α
inst✝⁶ : IsStrictOrderedRing α
inst✝⁵ : ExistsAddOfLE α
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulMono α β
a₁ a₂ : α
b₁ b₂ : β
ha : a₂ ≤ a₁
hb : b₂ ≤ b₁
⊢ a₁ • b₂ + a₂ • b₁ ≤ a₁ • b₁ + a₂ • b₂

Tactic:
add_comm (a₁ • _)

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁸ : Semiring α
inst✝⁷ : PartialOrder α
inst✝⁶ : IsStrictOrderedRing α
inst✝⁵ : ExistsAddOfLE α
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulMono α β
a₁ a₂ : α
b₁ b₂ : β
ha : a₂ ≤ a₁
hb : b₂ ≤ b₁
⊢ a₂ • b₁ + a₁ • b₂ ≤ a₂ • b₂ + a₁ • b₁
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁸ : Semiring α
inst✝⁷ : PartialOrder α
inst✝⁶ : IsStrictOrderedRing α
inst✝⁵ : ExistsAddOfLE α
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a₁ a₂ : α
b₁ b₂ : β
ha : a₂ < a₁
hb : b₂ < b₁
⊢ a₁ • b₂ + a₂ • b₁ < a₁ • b₁ + a₂ • b₂

Tactic:
add_comm (a₁ • _)

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁸ : Semiring α
inst✝⁷ : PartialOrder α
inst✝⁶ : IsStrictOrderedRing α
inst✝⁵ : ExistsAddOfLE α
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a₁ a₂ : α
b₁ b₂ : β
ha : a₂ < a₁
hb : b₂ < b₁
⊢ a₂ • b₁ + a₁ • b₂ < a₂ • b₂ + a₁ • b₁
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
⊢ Ideal.span ↑{1} = ⊤

Tactic:
simpa only [Finset.coe_singleton] using Ideal.span_singleton_one

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

Goal state before:
pp: α : Type u_4
r : α → α → Prop
wo : IsWellOrder α r
h : ∀ a < type r, succ a < type r
x : α
⊢ ∃ y, r x y

Tactic:
use enum r ⟨succ (typein r x), h _ (typein_lt_type r x)⟩
  convert! enum_lt_enum.mpr _
  · rw [enum_typein]
  · rw [Subtype.mk_lt_mk, lt_succ_iff]

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

Goal state before:
pp: case inr
o : Ordinal.{v}
ho : IsSuccPrelimit o
⊢ lift.{u, v} o.pred = (lift.{u, v} o).pred

Tactic:
· rwa [ho.ordinalPred_eq, eq_comm, pred_eq_iff_isSuccPrelimit, isSuccPrelimit_lift]

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

Goal state before:
pp: α β : Type u
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≃r s
o : Ordinal.{u}
γ : Type u
t : γ → γ → Prop
wo : IsWellOrder γ t
g : t ≺i r
h : t ≺i s
⊢ f ((enum r) ⟨type t, ⋯⟩) = (enum s) ⟨type t, ⋯⟩

Tactic:
enum_type g,

Goal state after:
α β : Type u
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≃r s
o : Ordinal.{u}
γ : Type u
t : γ → γ → Prop
wo : IsWellOrder γ t
g : t ≺i r
h : t ≺i s
⊢ f g.top = (enum s) ⟨type t, ⋯⟩
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case mp
a b c : Ordinal.{u_4}
hc : IsSuccLimit c
d : Ordinal.{u_4}
hd : d < c
ha : a ≤ b + d
⊢ a < b + (d + 1)

Tactic:
← add_assoc,

Goal state after:
case mp
a b c : Ordinal.{u_4}
hc : IsSuccLimit c
d : Ordinal.{u_4}
hd : d < c
ha : a ≤ b + d
⊢ a < b + d + 1
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: α : Type u_3
β : Type u_4
f : α ⊕ β → Ordinal.{u}
inst✝¹ : Small.{u, u_3} α
inst✝ : Small.{u, u_4} β
⊢ ⨆ a, f (Sum.inl a) ≤ ⨆ i, f i

Tactic:
apply csSup_le_csSup' bddAbove_of_small
    rintro i ⟨a, rfl⟩
    apply mem_range_self

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

Goal state before:
pp: α : Type u_3
β : Type u_4
f : α ⊕ β → Ordinal.{u}
inst✝¹ : Small.{u, u_3} α
inst✝ : Small.{u, u_4} β
⊢ ⨆ b, f (Sum.inr b) ≤ ⨆ i, f i

Tactic:
apply csSup_le_csSup' bddAbove_of_small
    rintro i ⟨a, rfl⟩
    apply mem_range_self

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

Goal state before:
pp: a b : Ordinal.{u_4}
hb : 0 < b
⊢ a = a * 1

Tactic:
rw [mul_one a]

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

Goal state before:
pp: ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
hf : ∀ a < lsub f, succ a < lsub f
i : ι
hle : iSup f ≤ f i
heq : succ (iSup f) = lsub f
⊢ ?m.88 < succ (iSup f)

Tactic:
exact lt_succ (iSup f)

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

Goal state before:
pp: case refine_2
a : Ordinal.{u_4}
h : 0 < a
a✝ : Ordinal.{u_4}
hb : IsSuccLimit a✝
⊢ IsLUB ((fun x ↦ a * x) '' Iio a✝) (a * a✝)

Tactic:
· simpa [IsLUB, IsLeast, upperBounds, lowerBounds, mul_le_iff_of_isSuccLimit hb] using
      fun c hc ↦ mul_le_mul_right hc.le a

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 * (c + 1) + b + (a + b) = a * (c + 1 + 1) + b

Tactic:
← add_assoc,

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 * (c + 1) + b + a + b = a * (c + 1 + 1) + b
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
x : α
h : (#α).ord = type r
⊢ ((typein r).toRelEmbedding x).card < #α

Tactic:
rw [← lt_ord, h]

Goal state after:
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
x : α
h : (#α).ord = type r
⊢ (typein r).toRelEmbedding x < type r
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
s : Set α
⊢ (#↑s).ord ≤ type r

Tactic:
by
  grw [← ord_le_type, ord_le_ord, le_mk_iff_exists_set]
  use s

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

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
f : (a : Ordinal.{u}) → a < type r → Ordinal.{max u v}
o : Ordinal.{max u v}
⊢ (type r).blsub f ≤ o ↔ (lsub fun a ↦ f ((typein r).toRelEmbedding a) ⋯) ≤ o

Tactic:
rw [blsub_le_iff, lsub_le_iff]
    exact ⟨fun H b => H _ _, fun H i h => by simpa only [typein_enum] using H (enum r ⟨i, h⟩)⟩

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

Goal state before:
pp: α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
o : Ordinal.{u}
a : α
as : List α
hl : (a :: as).SortedGT
hlt : ∀ i ∈ a :: as, (Ordinal.typein fun x1 x2 ↦ x1 < x2).toRelEmbedding i < o
b : α
bs : List α
hm : (b :: bs).SortedGT
hmltl : Lex (fun x1 x2 ↦ x1 < x2) (b :: bs) (a :: as)
i : α
hi : i ∈ b :: bs
h : i ≤ a
⊢ (Ordinal.typein fun x1 x2 ↦ x1 < x2).toRelEmbedding i < o

Tactic:
refine lt_of_le_of_lt ?_ (hlt a mem_cons_self)

Goal state after:
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
o : Ordinal.{u}
a : α
as : List α
hl : (a :: as).SortedGT
hlt : ∀ i ∈ a :: as, (Ordinal.typein fun x1 x2 ↦ x1 < x2).toRelEmbedding i < o
b : α
bs : List α
hm : (b :: bs).SortedGT
hmltl : Lex (fun x1 x2 ↦ x1 < x2) (b :: bs) (a :: as)
i : α
hi : i ∈ b :: bs
h : i ≤ a
⊢ (Ordinal.typein fun x1 x2 ↦ x1 < x2).toRelEmbedding i ≤ (Ordinal.typein fun x1 x2 ↦ x1 < x2).toRelEmbedding a
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inl
b x : ℕ
hx : x ≠ 0
hlt : 0 < b ^ x
⊢ log b 0 < x

pp: case inr
b x y : ℕ
hx : x ≠ 0
hlt : y < b ^ x
hy : y ≠ 0
⊢ log b y < x

Tactic:
· grind [log_zero_right]

Goal state after:
case inr
b x y : ℕ
hx : x ≠ 0
hlt : y < b ^ x
hy : y ≠ 0
⊢ log b y < x
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inr
a b c : Ordinal.{u_4}
ha : a ≠ 0
d : Ordinal.{u_4}
⊢ a * (b - c) ≤ d ↔ a * b - a * c ≤ d

Tactic:
rw [sub_le, mul_le_iff_le_div ha, sub_le, mul_le_iff_le_div ha, mul_add_div _ ha]

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

Goal state before:
pp: case h₁
b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ b * b ^ log b n ≤ n * b

Tactic:
Nat.mul_comm b

Goal state after:
case h₁
b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ b ^ log b n * b ≤ n * b
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case h₂
b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ n * b < b * b ^ (log b n + 1)

Tactic:
Nat.mul_comm b

Goal state after:
case h₂
b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ n * b < b ^ (log b n + 1) * b
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: w x : Ordinal.{u_4}
hw : w < x
y z : Ordinal.{u_4}
⊢ x * z * (y / z) + (x * (y % z) + w) = x * y + w

Tactic:
← add_assoc,

Goal state after:
w x : Ordinal.{u_4}
hw : w < x
y z : Ordinal.{u_4}
⊢ x * z * (y / z) + x * (y % z) + w = x * y + w
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inl.inr
b c : Ordinal.{u_1}
hc : 0 < c
this : b + c ≠ 0
⊢ b + c ≠ 0

Tactic:
exact (hc.trans_le le_add_self).ne'

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

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

Tactic:
← add_assoc,

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

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

Tactic:
opow_one

Goal state after:
a b : Ordinal.{u_1}
⊢ a * a ^ b = a * a ^ b
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: o : Ordinal.{u_4}
h : ω ≤ o
n : ℕ
⊢ ↑n + (ω + (o - ω)) = ω + (o - ω)

Tactic:
← add_assoc,

Goal state after:
o : Ordinal.{u_4}
h : ω ≤ o
n : ℕ
⊢ ↑n + ω + (o - ω) = ω + (o - ω)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

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

Tactic:
lt_mul_iff_div_lt omega0_ne_zero,

Goal state after:
case refine_1
a : Ordinal.{u_4}
l : IsSuccPrelimit a
x : Ordinal.{u_4}
hx : x < a
⊢ x / ω < a / ω
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inr
b n : ℕ
hb : 1 < b
⊢ log b n ≤ clog b n

Tactic:
cases n with

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

Goal state before:
pp: b o : Ordinal.{u_1}
hb : 1 < b
ho : o ≠ 0
hbo : b ≤ o
⊢ b ^ 1 ≤ o

Tactic:
opow_one

Goal state after:
b o : Ordinal.{u_1}
hb : 1 < b
ho : o ≠ 0
hbo : b ≤ o
⊢ b ≤ o
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inr.inr
b o : Ordinal.{u_1}
hbo : o < b
ho : o ≠ 0
hb : 1 < b
⊢ o < b ^ 1

Tactic:
opow_one

Goal state after:
case inr.inr
b o : Ordinal.{u_1}
hbo : o < b
ho : o ≠ 0
hb : 1 < b
⊢ o < b
Module: Mathlib.SetTheory.Ordinal.Exponential

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

Tactic:
cases n with

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

Goal state before:
pp: m n : ℕ
hm : m ≤ 1
⊢ ↑(Nat.log m n) = log ↑m ↑n

Tactic:
rw_mod_cast [Nat.log_of_left_le_one hm, log_of_left_le_one (mod_cast hm)]

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

Goal state before:
pp: case refine_2
a b : Ordinal.{u_1}
h : a * ω ≤ b
this : a * ω + (b - a * ω) = b
⊢ a + (a * ω + (b - a * ω)) = b

Tactic:
← add_assoc,

Goal state after:
case refine_2
a b : Ordinal.{u_1}
h : a * ω ≤ b
this : a * ω + (b - a * ω) = b
⊢ a + a * ω + (b - a * ω) = b
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: a b c : Ordinal.{u}
hb : IsPrincipal (fun x1 x2 ↦ x1 + x2) b
hab : a < b
hbc : b ≤ c
⊢ a + (b + (c - b)) = b + (c - b)

Tactic:
← add_assoc,

Goal state after:
a b c : Ordinal.{u}
hb : IsPrincipal (fun x1 x2 ↦ x1 + x2) b
hab : a < b
hbc : b ≤ c
⊢ a + b + (c - b) = b + (c - b)
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case inr
o : Ordinal.{u_1}
ha' : o ≠ 0
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) (ω ^ o)

Tactic:
· rw [isPrincipal_add_iff_add_self_lt]
    intro a ha
    obtain ⟨c, hc, m, hm⟩ := (lt_omega0_opow ha').1 ha
    apply (add_lt_add_of_le_of_lt hm.le hm).trans_le
    rw [← mul_add, ← Nat.cast_add]
    exact (opow_mul_lt_opow (natCast_lt_omega0 _) hc).le

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

Goal state before:
pp: case inr
a b c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
ha : a < c
hb : b < c
h : ℵ₀ ≤ max a b
⊢ max a b * max a b < c

Tactic:
rw [mul_eq_self h]
    exact max_lt ha hb

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

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

Tactic:
exact mul_eq_max_of_aleph0_le_right ha hb'

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ IsSuccLimit (ω_ o)

Tactic:
rw [← ord_aleph]
  exact isSuccLimit_ord (aleph0_le_aleph _)

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

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

Tactic:
by
  rcases eq_or_ne a 0 with (rfl | ha0); · simp
  rcases eq_or_ne b 0 with (rfl | hb0); · simp
  rcases le_or_gt ℵ₀ a with ha | ha
  · rw [mul_eq_max_of_aleph0_le_left ha hb0]
    exact le_max_left _ _
  · rcases le_or_gt ℵ₀ b with hb | hb
    · rw [mul_comm, mul_eq_max_of_aleph0_le_left hb ha0, max_comm]
      exact le_max_left _ _
    · exact le_max_of_le_right (mul_lt_aleph0 ha hb).le

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

Goal state before:
pp: case inl
a : Ordinal.{u}
a0 : 0 < a
h : a < ω ^ 1
⊢ a * ω ^ 1 = ω ^ 1

Tactic:
opow_one

Goal state after:
case inl
a : Ordinal.{u}
a0 : 0 < a
h : a < ω
⊢ a * ω = ω
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case add_one
f : Ordinal.{u_1} → Ordinal.{u_1}
hf : IsNormal f
a : Ordinal.{u_1}
a✝ : a + 1 = a → (a + 1).cof ≤ (f (a + 1)).cof
⊢ (a + 1).cof ≤ (f (a + 1)).cof

Tactic:
rw [cof_add_one, Cardinal.one_le_iff_ne_zero, cof_eq_zero.ne]

Goal state after:
case add_one
f : Ordinal.{u_1} → Ordinal.{u_1}
hf : IsNormal f
a : Ordinal.{u_1}
a✝ : a + 1 = a → (a + 1).cof ≤ (f (a + 1)).cof
⊢ f (a + 1) ≠ 0
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: ι : Type u
f : ι → Ordinal.{v}
⊢ Cardinal.lift.{u, v} (⨆ i, f i).card ≤ sum fun i ↦ (f i).card

Tactic:
by_cases! hf : ¬ BddAbove (range f)

Goal state after:
case pos
ι : Type u
f : ι → Ordinal.{v}
hf : ¬BddAbove (range f)
⊢ Cardinal.lift.{u, v} (⨆ i, f i).card ≤ sum fun i ↦ (f i).card

case neg
ι : Type u
f : ι → Ordinal.{v}
hf : BddAbove (range f)
⊢ Cardinal.lift.{u, v} (⨆ i, f i).card ≤ sum fun i ↦ (f i).card
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: a o : Ordinal.{u_1}
ha : o.cof.ord = a
⊢ ∃ f, IsFundamentalSeq f

Tactic:
subst ha

Goal state after:
o : Ordinal.{u_1}
⊢ ∃ f, IsFundamentalSeq f
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{u}
c : Ordinal.{u}
ho : o.card < c.cof
hf : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi < c
⊢ Cardinal.lift.{u, u} o.card < c.cof

Tactic:
rwa [o.card.lift_id]

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

Goal state before:
pp: o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{u}
c : Ordinal.{u}
ho : o.card < c.cof
⊢ Cardinal.lift.{u, u} o.card < c.cof

Tactic:
rwa [o.card.lift_id]

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

Goal state before:
pp: case inr.inl
a c : Ordinal.{u_1}
hb : succ c ≠ 0
⊢ (a + (c + 1)).cof = (c + 1).cof

Tactic:
← add_assoc,

Goal state after:
case inr.inl
a c : Ordinal.{u_1}
hb : succ c ≠ 0
⊢ (a + c + 1).cof = (c + 1).cof
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: case le_cof_ord
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
hc₀ : ℵ₀ ≤ succ c
⊢ succ c ≤ (succ c).ord.cof

Tactic:
by_contra! hc'

Goal state after:
case le_cof_ord
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
hc₀ : ℵ₀ ≤ succ c
hc' : (succ c).ord.cof < succ c
⊢ False
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_mul_ord
  rwa [aleph0_le_card]

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

Goal state before:
pp: case refine_1
α : Type u
s : Set α
c : Cardinal.{u}
⊢ { t // t ⊆ s ∧ #↑t ≤ c } ↪ Set ↑s

pp: case refine_2
α : Type u
s : Set α
c : Cardinal.{u}
⊢ ∀ (a : { t // t ⊆ s ∧ #↑t ≤ c }), ?refine_1 a ∈ fun t ↦ Quot.lift ((fun α β ↦ Nonempty (α ↪ β)) ↑t) ⋯ c

Tactic:
· use fun t => (↑) ⁻¹' t.1
    rintro ⟨t, ht1, ht2⟩ ⟨t', h1t', h2t'⟩ h
    apply Subtype.ext
    dsimp only at h ⊢
    refine (preimage_eq_preimage' ?_ ?_).1 h <;> rw [Subtype.range_coe] <;> assumption

Goal state after:
case refine_2
α : Type u
s : Set α
c : Cardinal.{u}
⊢ ∀ (a : { t // t ⊆ s ∧ #↑t ≤ c }),
    { toFun := fun t ↦ Subtype.val ⁻¹' ↑t, inj' := ⋯ } a ∈ fun t ↦ Quot.lift ((fun α β ↦ Nonempty (α ↪ β)) ↑t) ⋯ c