mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type u_1
M₆ : Type u_2
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommGroup M₃
inst✝⁴ : AddCommGroup M₄
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R M₄
f : M →ₗ[R] M₂
g : M₃ →ₗ[R] M₄
a✝ b✝ : M × M₂
ha : a✝.2 = f a✝.1
hb : b✝.2 = f b✝.1
⊢ a✝.2 + b✝.2 = f (a✝.1 + b✝.1)

Tactic:
map_add,

Goal state after:
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type u_1
M₆ : Type u_2
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommGroup M₃
inst✝⁴ : AddCommGroup M₄
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R M₄
f : M →ₗ[R] M₂
g : M₃ →ₗ[R] M₄
a✝ b✝ : M × M₂
ha : a✝.2 = f a✝.1
hb : b✝.2 = f b✝.1
⊢ a✝.2 + b✝.2 = f a✝.1 + f b✝.1
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
i : ι
hn : IsMin i
⊢ disjointed f i = f i

Tactic:
by
  have : Iio i = ∅ := by rwa [← Finset.coe_eq_empty, coe_Iio, Set.Iio_eq_empty_iff]
  simp only [disjointed_apply, this, sup_empty, sdiff_bot]

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝⁶ : CommMonoid M
inst✝⁵ : LinearOrder α
inst✝⁴ : LocallyFiniteOrderBot α
inst✝³ : Add α
inst✝² : One α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
a : α
f : α → M
⊢ ∏ i < a + 1, f i = (∏ i < a, f i) * f a

Tactic:
prod_Iio_add_one_comm,

Goal state after:
α : Type u_1
M : Type u_2
inst✝⁶ : CommMonoid M
inst✝⁵ : LinearOrder α
inst✝⁴ : LocallyFiniteOrderBot α
inst✝³ : Add α
inst✝² : One α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
a : α
f : α → M
⊢ f a * ∏ i < a, f i = (∏ i < a, f i) * f a
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
m n k : ℕ
hmn : m ≤ n
hnk : n ≤ k
⊢ Disjoint (Ioc m n) (Ioc n k)

Tactic:
apply disjoint_left.2 fun x hx h'x => _

Goal state after:
M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
m n k : ℕ
hmn : m ≤ n
hnk : n ≤ k
⊢ ∀ x ∈ Ioc m n, x ∈ Ioc n k → False
Module: Mathlib.Algebra.BigOperators.NatAntidiagonal

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
n : ℕ
f : ℕ × ℕ → M
⊢ ∏ p ∈ antidiagonal (n + 1), f p = f (n + 1, 0) * ∏ p ∈ antidiagonal n, f (p.1, p.2 + 1)

Tactic:
rw [← prod_antidiagonal_swap, prod_antidiagonal_succ, ← prod_antidiagonal_swap]
  rfl

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

Goal state before:
pp: α : Type u
inst✝ : Semiring α
I : Ideal α
x y : α
hy : IsUnit y
h : y * x ∈ I
y' : α
hy' : y' * y = 1
this : y' * (y * x) ∈ I
⊢ x ∈ I

Tactic:
← mul_assoc,

Goal state after:
α : Type u
inst✝ : Semiring α
I : Ideal α
x y : α
hy : IsUnit y
h : y * x ∈ I
y' : α
hy' : y' * y = 1
this : y' * y * x ∈ I
⊢ x ∈ I
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
a b : R
mul : a * b = 0
add : a + b = 1
| a * a + a * b

Tactic:
mul,

Goal state after:
R : Type u_1
inst✝ : Semiring R
a b : R
mul : a * b = 0
add : a + b = 1
| a * a + 0
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
a b : R
mul : a * b = 0
add : a + b = 1
| a * b + b * b

Tactic:
mul,

Goal state after:
R : Type u_1
inst✝ : Semiring R
a b : R
mul : a * b = 0
add : a + b = 1
| 0 + b * b
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
a b : R
inst✝¹ : NonUnitalSemiring R
inst✝ : IsAddTorsionFree R
ha : IsIdempotentElem a
hab : a * b + b * a = 0
this : a * (a * (b * a)) + a * (b * a) = 0
⊢ (1 + 1) • (a * b * a) = 0

Tactic:
← mul_assoc,

Goal state after:
R : Type u_1
a b : R
inst✝¹ : NonUnitalSemiring R
inst✝ : IsAddTorsionFree R
ha : IsIdempotentElem a
hab : a * b + b * a = 0
this : a * a * b * a + a * b * a = 0
⊢ (1 + 1) • (a * b * a) = 0
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalRing R
inst✝ : IsAddTorsionFree R
p q : R
hp : IsIdempotentElem p
hq : IsIdempotentElem q
h : p * (q - p) + (q - p) * p = 0
hqp : p * q + q * p - p = p
h2 : (p * q + q * p - p) * q = p * q
h1 : q * (p * q) + q * (q * p) - q * p = q * p
⊢ Commute p q

Tactic:
← mul_assoc,

Goal state after:
R : Type u_1
inst✝¹ : NonUnitalRing R
inst✝ : IsAddTorsionFree R
p q : R
hp : IsIdempotentElem p
hq : IsIdempotentElem q
h : p * (q - p) + (q - p) * p = 0
hqp : p * q + q * p - p = p
h2 : (p * q + q * p - p) * q = p * q
h1 : q * p * q + q * q * p - q * p = q * p
⊢ Commute p q
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: case zero
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
⊢ 1 = 1 * 1 * ↑(Nat.choose 0 0)

Tactic:
choose_self,

Goal state after:
case zero
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
h_middle : ∀ (n i : ℕ), i ∈ range n.succ → t n.succ i.succ = x * t n i + y * t n i.succ
⊢ 1 = 1 * 1 * ↑1
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: case mp
α : Type u
inst✝ : Semiring α
x y : α
I : Ideal α
⊢ (∃ y_1 ∈ span {y}, ∃ z ∈ I, y_1 + z = x) → ∃ a, ∃ b ∈ I, a * y + b = x

pp: case mpr
α : Type u
inst✝ : Semiring α
x y : α
I : Ideal α
⊢ (∃ a, ∃ b ∈ I, a * y + b = x) → ∃ y_1 ∈ span {y}, ∃ z ∈ I, y_1 + z = x

Tactic:
· rintro ⟨ya, hya, b, hb, rfl⟩
    obtain ⟨a, rfl⟩ := mem_span_singleton'.mp hya
    exact ⟨a, b, hb, rfl⟩

Goal state after:
case mpr
α : Type u
inst✝ : Semiring α
x y : α
I : Ideal α
⊢ (∃ a, ∃ b ∈ I, a * y + b = x) → ∃ y_1 ∈ span {y}, ∃ z ∈ I, y_1 + z = x
Module: Mathlib.RingTheory.Ideal.Basic

Goal state before:
pp: ι : Type u_1
R : ι → Type u_5
inst✝ : (i : ι) → Semiring (R i)
r : (i : ι) → R i
⊢ (pi fun x ↦ span {r x}) = span {r}

Tactic:
ext; simp_rw [mem_pi, mem_span_singleton', funext_iff, Classical.skolem, Pi.mul_def]

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: case inr
n k : ℕ
h : k ≤ n
⊢ ∑ m ∈ Icc k n, m.choose k = (n + 1).choose (k + 1)

Tactic:
induction n, h using le_induction with
    | base => simp
    | succ n _ ih =>
      rw [← Ico_insert_right (by lia), sum_insert (by simp), Ico_add_one_right_eq_Icc, ih,
        choose_succ_succ' (n + 1)]

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: n : ℕ
h : ¬n = 0
⊢ n * 2 ^ n = 2 * (n * 2 ^ (n - 1))

Tactic:
← mul_assoc,

Goal state after:
n : ℕ
h : ¬n = 0
⊢ n * 2 ^ n = 2 * n * 2 ^ (n - 1)
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝¹ : CommSemiring α
inst✝ : IsPrincipalIdealRing α
P : Ideal α
hP : P ≠ ⊥
⊢ (∃ p, Prime p ∧ P = span {p}) → P.IsPrime

Tactic:
rintro ⟨p, hp, rfl⟩

Goal state after:
α : Type u
inst✝¹ : CommSemiring α
inst✝ : IsPrincipalIdealRing α
p : α
hp : Prime p
hP : span {p} ≠ ⊥
⊢ (span {p}).IsPrime
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_5
p : α → Submodule R M
i : α
x : M
hx : x ∈ comap (lsingle i) (submodule p)
⊢ x ∈ p i

Tactic:
simpa using hx i

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
f : Filter α
h✝ : Nonempty β
⊢ (comap Prod.fst f).NeBot ↔ f.NeBot ∧ Nonempty β

Tactic:
· simp [comap_neBot_iff_frequently, *]

Goal state after:
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 α := ⋯
⊢ ∀ (x : R) (y : A) (z : α), (x • y) • z = x • y • z

Tactic:
intro x y z

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 : α
⊢ (x • y) • z = x • y • z
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: case inl
α : 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:
simp [← ha]

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

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
sp : M → Submodule R M := fun a ↦ R ∙ a
supr_rw : ∀ (t : Finset M), ⨆ x ∈ t, sp x = ⨆ x ∈ ↑t, sp x
t : Finset M
⊢ IsCompactElement (t.sup sp)

Tactic:
apply CompleteLattice.isCompactElement_finsetSup

Goal state after:
case mp
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
sp : M → Submodule R M := ⋯
supr_rw : ∀ (t : Finset M), ⨆ x ∈ t, sp x = ⨆ x ∈ ↑t, sp x
t : Finset M
⊢ ∀ x ∈ t, IsCompactElement (sp x)
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:
simp_rw [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:
simp_rw [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.SetTheory.Ordinal.Basic

Goal state before:
pp: δ : 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 γ
⊢ ⟦{ α := γ, r := fun x1 x2 ↦ x1 < x2, wo := ⋯ }⟧.liftOn' (fun w ↦ f w.α) ⋯ = f γ

Tactic:
Quotient.liftOn'_mk

Goal state after:
δ : 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 γ
⊢ f { α := γ, r := fun x1 x2 ↦ x1 < x2, wo := ⋯ }.α = f γ
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
a b : α
⊢ ¬(typein r).toRelEmbedding b < (typein r).toRelEmbedding a ↔ ¬r b a

Tactic:
typein_lt_typein

Goal state after:
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
a b : α
⊢ ¬r b a ↔ ¬r b a
Module: Mathlib.SetTheory.Ordinal.Arithmetic

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

Tactic:
· rwa [sub_lt_of_le hba]

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

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

Tactic:
rw [lt_add_iff hc.ne_bot]

Goal state after:
a b c : Ordinal.{u_4}
hc : IsSuccLimit c
⊢ (∃ d < c, a ≤ b + d) ↔ ∃ d < c, a < b + d
Module: Mathlib.SetTheory.Ordinal.Family

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

Tactic:
· exact le_max_of_le_right (Ordinal.le_iSup (fun x ↦ f (Sum.inr x)) i)

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
H : StrictMono (Subtype.val ∘ ⇑(enum s hs)) := ⋯
hs' : ∀ ⦃d : Set α⦄, d ⊆ s → d.Nonempty → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s
a : α
ha : IsSuccLimit a
b : α
hb : ∀ b_1 < a, (Subtype.val ∘ ⇑(enum s hs)) b_1 ≤ b
bdd : BddAbove (Subtype.val ∘ ⇑(enum s hs) '' Iio a)
this✝¹ : Nonempty α
this✝ : OrderBot α := ⋯
this : ConditionallyCompleteLinearOrderBot α := ⋯
⊢ sSup (Subtype.val ∘ ⇑(enum s hs) '' Iio a) ≤ b

Tactic:
apply csSup_le'

Goal state after:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
H : StrictMono (Subtype.val ∘ ⇑(enum s hs)) := ⋯
hs' : ∀ ⦃d : Set α⦄, d ⊆ s → d.Nonempty → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s
a : α
ha : IsSuccLimit a
b : α
hb : ∀ b_1 < a, (Subtype.val ∘ ⇑(enum s hs)) b_1 ≤ b
bdd : BddAbove (Subtype.val ∘ ⇑(enum s hs) '' Iio a)
this✝¹ : Nonempty α
this✝ : OrderBot α := ⋯
this : ConditionallyCompleteLinearOrderBot α := ⋯
⊢ b ∈ upperBounds (Subtype.val ∘ ⇑(enum s hs) '' Iio a)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case refine_1
a : Ordinal.{u_4}
h : 0 < a
b : Ordinal.{u_4}
⊢ a * b < a * succ b

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 [mul_add_one] using (add_lt_add_iff_left (a * b)).2 h

Goal state after:
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✝)
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
a : Ordinal.{max u v}
⊢ o.blsub f ≤ a ↔ ∀ (i : Ordinal.{u}) (h : i < o), f i h < a

Tactic:
convert! bsup_le_iff.{_, v} (f := fun a ha => succ (f a ha)) (a := a) using 2
  simp_rw [succ_le_iff]

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

Goal state before:
pp: n : ℕ
⊢ (↑n).ord = ↑n

Tactic:
apply (ord_le.2 (card_nat n).ge).antisymm

Goal state after:
n : ℕ
⊢ ↑n ≤ (↑n).ord
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ℵ₀.ord ≤ o ↔ ω ≤ o

Tactic:
ord_aleph0

Goal state after:
o : Ordinal.{u_1}
⊢ ω ≤ o ↔ ω ≤ o
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u_3}
f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_4 u_3}
⊢ lsub (o.familyOfBFamily f) = 0 ↔ o = 0

Tactic:
lsub_eq_zero_iff

Goal state after:
o : Ordinal.{u_3}
f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_4 u_3}
⊢ IsEmpty o.ToType ↔ o = 0
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inl
b n : ℕ
hb : 1 < b
⊢ log b n = 0 ↔ n < b ∨ b ≤ 1

pp: case inr
b n : ℕ
hb : 1 ≥ b
⊢ log b n = 0 ↔ n < b ∨ b ≤ 1

Tactic:
· rcases eq_or_ne n 0 with rfl | hn
    · grind [log_of_lt]
    · rw [← Nat.lt_one_iff, log_lt_iff_lt_pow hb hn, Nat.pow_one, or_iff_left (Nat.not_le_of_lt hb)]

Goal state after:
case inr
b n : ℕ
hb : 1 ≥ b
⊢ log b n = 0 ↔ n < b ∨ b ≤ 1
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: a : Cardinal.{u}
b : Ordinal.{max u v}
h : b.card ≤ Cardinal.lift.{v, u} a
⊢ b ∈ range lift.{v, u}

Tactic:
by
  rw [card_le_iff, ← lift_succ, ← lift_ord] at h
  exact mem_range_lift_of_le h.le

Goal state after:
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
⊢ succ (x / ω) ≤ a / ω

Tactic:
← mul_le_iff_le_div omega0_ne_zero,

Goal state after:
case refine_1
a : Ordinal.{u_4}
l : IsSuccPrelimit a
x : Ordinal.{u_4}
hx : x < a
⊢ ω * succ (x / ω) ≤ a
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a : Ordinal.{u_4}
⊢ a ≠ 0 ∧ IsSuccPrelimit a ↔ a ≠ 0 ∧ ω ∣ a

Tactic:
isSuccPrelimit_iff_omega0_dvd

Goal state after:
a : Ordinal.{u_4}
⊢ a ≠ 0 ∧ ω ∣ a ↔ a ≠ 0 ∧ ω ∣ 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
  | zero =>
    rw [log_zero_right]
    exact zero_le _
  | succ n =>
    exact (Nat.pow_le_pow_iff_right hb).1
      ((pow_log_le_self b n.succ_ne_zero).trans <| le_pow_clog hb _)

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

Goal state before:
pp: case inr
b o : Ordinal.{u_1}
hb : 1 < b
hbo : b ≤ o
h : o % b ^ log b o ≠ 0
⊢ log b (o % b ^ log b o) < log b o

Tactic:
rw [← lt_opow_iff_log_lt hb h]

Goal state after:
case inr
b o : Ordinal.{u_1}
hb : 1 < b
hbo : b ≤ o
h : o % b ^ log b o ≠ 0
⊢ o % b ^ log b o < b ^ log b o
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
a b : Ordinal.{u}
⊢ f b < nfpFamily (fun x ↦ f) a ↔ ∀ (i : Unit), f b < nfpFamily (fun x ↦ f) a

Tactic:
exact ⟨fun h _ => h, fun h => h Unit.unit⟩

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

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
a : Ordinal.{u}
⊢ f a ≤ a ↔ ∀ (i : Unit), f a ≤ a

Tactic:
exact ⟨fun h _ => h, fun h => h Unit.unit⟩

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

Goal state before:
pp: a : Ordinal.{u_1}
⊢ ⨆ n, 0^[n] a = a

Tactic:
apply (Ordinal.iSup_le ?_).antisymm (Ordinal.le_iSup _ 0)

Goal state after:
a : Ordinal.{u_1}
⊢ ∀ (i : ℕ), 0^[i] a ≤ 0^[0] a
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: ⊢ IsInitial 0

Tactic:
by
  exact_mod_cast isInitial_natCast 0

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

Goal state before:
pp: ⊢ ℵ₀.ord = ω

Tactic:
ord_aleph0

Goal state after:
⊢ ω = ω
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case inr.refine_1
a b : Ordinal.{u_1}
ha : 0 < a
hab : a * (a ^ ω * (b / a ^ ω)) + a * (b % a ^ ω) = a ^ ω * (b / a ^ ω) + b % a ^ ω
⊢ b % a ^ ω = 0

Tactic:
← mul_assoc,

Goal state after:
case inr.refine_1
a b : Ordinal.{u_1}
ha : 0 < a
hab : a * a ^ ω * (b / a ^ ω) + a * (b % a ^ ω) = a ^ ω * (b / a ^ ω) + b % a ^ ω
⊢ b % a ^ ω = 0
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case inr.refine_2
a b : Ordinal.{u_1}
ha : 0 < a
c : Ordinal.{u_1}
hc : b = a ^ ω * c
⊢ a * (a ^ ω * c) = a ^ ω * c

Tactic:
← mul_assoc,

Goal state after:
case inr.refine_2
a b : Ordinal.{u_1}
ha : 0 < a
c : Ordinal.{u_1}
hc : b = a ^ ω * c
⊢ a * a ^ ω * c = a ^ ω * c
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case a.h
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
⊢ a * (a ^ ω * succ b) ≤ a ^ ω * succ b

Tactic:
← mul_assoc,

Goal state after:
case a.h
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
⊢ a * a ^ ω * succ b ≤ a ^ ω * succ b
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u}
⊢ Cardinal.lift.{v, u} o.cof = (lift.{v, u} o).cof

Tactic:
cases o using inductionOnWellOrder with | type α
   =>  _ 

Goal state after:
case type
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
⊢ Cardinal.lift.{v, u} (typeLT α).cof = (lift.{v, u} (typeLT α)).cof
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
⊢ o.cof = 1 ↔ o ∈ range succ

Tactic:
cases o using inductionOnWellOrder with | type α
   =>  _ 

Goal state after:
case type
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
⊢ (typeLT α).cof = 1 ↔ typeLT α ∈ range succ
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: a : Ordinal.{u}
a0 : 0 < a
ha : a < ω
b : Ordinal.{u}
⊢ a * (ω * b) = ω * b

Tactic:
← mul_assoc,

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

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

Tactic:
by
  simpa [← lift_cof] using lift_cof_iSup_add_one hf

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

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

Tactic:
by
  rw [max_le_iff]
  refine ⟨fun h => ?_, ?_⟩
  · rcases le_or_gt ℵ₀ a with ha | ha
    · left
      use ha
      rw [← not_lt]
      apply fun hb => ne_of_gt _ h
      intro hb
      exact hb.trans_le (self_le_add_left b a)
    right
    rw [← h, add_lt_aleph0_iff, lt_aleph0, lt_aleph0] at ha
    rcases ha with ⟨⟨n, rfl⟩, ⟨m, rfl⟩⟩
    norm_cast at h ⊢
    rw [← add_right_inj, h, add_zero]
  · rintro (⟨h1, h2⟩ | h3)
    · rw [add_eq_max h1, max_eq_left h2]
    · rw [h3, add_zero]

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

Goal state before:
pp: case e'_3
s : Set Ordinal.{u}
a : Ordinal.{u}
ha : #↑s < (lift.{u + 1, u} a).cof
hs : ∀ i ∈ s, i < a
f : ↑(Iio (typeLT ↑s)) ≃o ↑s := OrderIso.ofRelIsoLT (enum fun x1 x2 ↦ x1 < x2)
this : Small.{u, u + 2} ↑(Iio (typeLT ↑s))
⊢ s = Subtype.val '' range ⇑f

Tactic:
f.range_eq

Goal state after:
case e'_3
s : Set Ordinal.{u}
a : Ordinal.{u}
ha : #↑s < (lift.{u + 1, u} a).cof
hs : ∀ i ∈ s, i < a
f : ↑(Iio (typeLT ↑s)) ≃o ↑s := OrderIso.ofRelIsoLT (enum fun x1 x2 ↦ x1 < x2)
this : Small.{u, u + 2} ↑(Iio (typeLT ↑s))
⊢ s = Subtype.val '' Set.univ
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: case neg
ι : Type u
f : ι → Ordinal.{v}
hf : BddAbove (range f)
⊢ Cardinal.lift.{u, v} #(⨆ i, f i).ToType ≤ sum fun i ↦ #(f i).ToType

Tactic:
rw [← mk_sigma, ← Cardinal.lift_id'.{v} #(Σ _, _), ← Cardinal.lift_umax.{v, u}]

Goal state after:
case neg
ι : Type u
f : ι → Ordinal.{v}
hf : BddAbove (range f)
⊢ Cardinal.lift.{max v u, v} #(⨆ i, f i).ToType ≤ Cardinal.lift.{v, max v u} #((x : ι) × (f x).ToType)
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: o : Ordinal.{u_1}
s : Set o.ToType
hs : IsCofinal s
hs' : typeLT ↑s = (Order.cof o.ToType).ord
⊢ ∃ f, IsFundamentalSeq f

Tactic:
cof_toType

Goal state after:
o : Ordinal.{u_1}
s : Set o.ToType
hs : IsCofinal s
hs' : typeLT ↑s = o.cof.ord
⊢ ∃ f, IsFundamentalSeq f
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:
cof_toType

Goal state after:
o : Ordinal.{u}
S : Set o.ToType
hS : IsCofinal S
hS' : #↑S = o.cof
f : ↑S → Ordinal.{u} := fun s ↦ (typein LT.lt).toRelEmbedding ↑s
⊢ #↑S = o.cof
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: a b : Ordinal.{u_1}
ha : ω ≤ a
hb : 0 < b
⊢ (a ^ b).card = max a.card b.card

Tactic:
by
  apply (card_opow_le_of_omega0_le_left ha b).antisymm (max_le _ _) <;> apply card_le_card
  · exact left_le_opow a hb
  · exact right_le_opow b (one_lt_omega0.trans_le ha)

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

Goal state before:
pp: x : Cardinal.{u_1}
⊢ (sum fun n ↦ x ^ n) ≤ max ℵ₀ x

Tactic:
rw [← x.mk_out, ← mk_list_eq_sum_pow]

Goal state after:
x : Cardinal.{u_1}
⊢ #(List (Quotient.out x)) ≤ max ℵ₀ #(Quotient.out x)