mathlib-initiative/mathlib-tactics huggingface dataset:
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 α := ⋯
mul : Mul α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
⊢ ∀ (x : α) (n : ℤ), e (x ^ n) = e x ^ n

Tactic:
intros

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

Goal state after:
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
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 α := ⋯
mul : Mul α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
⊢ ∀ (x y : α), e (x * y) = e x * e y

Tactic:
intros

Goal state after:
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✝
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 α := ⋯
mul : Mul α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
⊢ ∀ (x : α), e x⁻¹ = (e x)⁻¹

Tactic:
intros

Goal state after:
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✝)⁻¹
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 α := ⋯
mul : Mul α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
⊢ ∀ (x y : α), e (x / y) = e x / e y

Tactic:
intros

Goal state after:
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✝
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 α := ⋯
mul : Mul α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
⊢ ∀ (x : α) (n : ℕ), e (x ^ n) = e x ^ n

Tactic:
intros

Goal state after:
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✝
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 α := ⋯
mul : Mul α := ⋯
inv : Inv α := ⋯
div : Div α := ⋯
npow : Pow α ℕ := ⋯
zpow : Pow α ℤ := ⋯
⊢ ∀ (x : α) (n : ℤ), e (x ^ n) = e x ^ n

Tactic:
intros

Goal state after:
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✝
Module: Mathlib.Order.Filter.AtTopBot.Basic

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

Tactic:
simp [hu']

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

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

Tactic:
simp [hu']

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

Goal state before:
pp: R : Type u_6
A : Type u_7
M : Type u_8
inst✝⁶ : Semiring R
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
s : Finset A
hs : span R ↑s = ⊤
t : Finset M
ht : span A ↑t = ⊤
⊢ span R (image2 (fun x1 x2 ↦ x1 • x2) ↑s ↑t) = ⊤

Tactic:
rw [image2_smul, span_smul_of_span_eq_top hs (↑t : Set M), ht, restrictScalars_top]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a a₁ a₂ : α
b b₁ b₂ : β
γ : Type u_3
inst✝⁹ : Zero α
inst✝⁸ : Preorder α
inst✝⁷ : Preorder β
inst✝⁶ : Preorder γ
inst✝⁵ : SMul α β
inst✝⁴ : SMul α γ
inst✝³ : Zero β
inst✝² : Zero γ
inst✝¹ : SMulPosReflectLE α β
inst✝ : SMulPosReflectLE α γ
_b : β × γ
hb : 0 < _b
_a₁ _a₂ : α
h : _a₁ • _b ≤ _a₂ • _b
⊢ _a₁ ≤ _a₂

Tactic:
rcases lt_iff.mp hb with ⟨h₁, -⟩ | ⟨-, h₁⟩
    · exact le_of_smul_le_smul_right h.1 h₁
    · exact le_of_smul_le_smul_right h.2 h₁

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

Goal state before:
pp: R : Type u_1
inst✝⁷ : Semiring R
M : Type u_2
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
A : Type u_3
inst✝⁴ : Semiring A
inst✝³ : Module R A
inst✝² : Module A M
inst✝¹ : IsScalarTower R A M
S : Submodule A M
inst✝ : Module.Finite R A
hS : S.FG
⊢ (Submodule.restrictScalars R S).FG

Tactic:
rw [← Module.Finite.iff_fg] at *

Goal state after:
R : Type u_1
inst✝⁷ : Semiring R
M : Type u_2
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
A : Type u_3
inst✝⁴ : Semiring A
inst✝³ : Module R A
inst✝² : Module A M
inst✝¹ : IsScalarTower R A M
S : Submodule A M
inst✝ : Module.Finite R A
hS : Module.Finite A ↥S
⊢ Module.Finite R ↥(Submodule.restrictScalars R S)
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: case refine_2
α : Type u_1
ι : Type u
r : ι → ι → Prop
inst✝ : IsWellOrder ι r
f : ι → α
a : α
⊢ a ∈ range f → a ∈ (type r).brange (bfamilyOfFamily' r f)

Tactic:
· rintro ⟨b, rfl⟩
    exact ⟨_, _, bfamilyOfFamily'_typein _ _ _⟩

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

Goal state before:
pp: case right
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ✝ → γ✝ → Prop
c a b : Ordinal.{u}
x✝³ x✝² x✝¹ : WellOrder
α : Type u
r : α → α → Prop
wo✝² : IsWellOrder α r
β : Type u
s : β → β → Prop
wo✝¹ : IsWellOrder β s
x✝ : ⟦{ α := α, r := r, wo := wo✝² }⟧ ≤ ⟦{ α := β, r := s, wo := wo✝¹ }⟧
γ : Type u
t : γ → γ → Prop
wo✝ : IsWellOrder γ t
f : InitialSeg r s
a✝ : α
b₁✝ b₂✝ : γ
h' : t b₁✝ b₂✝
⊢ Prod.Lex s t (f (a✝, b₁✝).1, (a✝, b₁✝).2) (f (a✝, b₂✝).1, (a✝, b₂✝).2)

Tactic:
exact Prod.Lex.right _ h'

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

Goal state before:
pp: ι : Type u
f : ι → Ordinal.{max u v}
⊢ sInf (range f)ᶜ < (succ (Cardinal.lift.{v, u} #ι)).ord

Tactic:
← card_le_iff

Goal state after:
ι : Type u
f : ι → Ordinal.{max u v}
⊢ (sInf (range f)ᶜ).card ≤ Cardinal.lift.{v, u} #ι
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: α β : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
c : Ordinal.{u_4}
h : IsSuccLimit (type s)
H : ∀ b' < type s, type r * b' ≤ c
l : c < type r * type s
a : α
b : β
this✝ : type r * (typein s).toRelEmbedding b + type r ≤ c
this : type r * (typein s).toRelEmbedding b + (typein r).toRelEmbedding a < c
⊢ (typein (Prod.Lex s r)).toRelEmbedding (b, a) < c

Tactic:
refine (RelEmbedding.ofMonotone (fun a => ?_) fun a b => ?_).ordinal_type_le.trans_lt this

Goal state after:
case refine_1
α β : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
c : Ordinal.{u_4}
h : IsSuccLimit (type s)
H : ∀ b' < type s, type r * b' ≤ c
l : c < type r * type s
a✝ : α
b : β
this✝ : type r * (typein s).toRelEmbedding b + type r ≤ c
this : type r * (typein s).toRelEmbedding b + (typein r).toRelEmbedding a✝ < c
a : { x // Prod.Lex s r x (b, a✝) }
⊢ { x // s x b } × α ⊕ { x // r x a✝ }

case refine_2
α β : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
c : Ordinal.{u_4}
h : IsSuccLimit (type s)
H : ∀ b' < type s, type r * b' ≤ c
l : c < type r * type s
a✝ : α
b✝ : β
this✝ : type r * (typein s).toRelEmbedding b✝ + type r ≤ c
this : type r * (typein s).toRelEmbedding b✝ + (typein r).toRelEmbedding a✝ < c
a b : { x // Prod.Lex s r x (b✝, a✝) }
⊢ Subrel (Prod.Lex s r) (fun x ↦ Prod.Lex s r x (b✝, a✝)) a b →
    Sum.Lex (Prod.Lex (Subrel s fun x ↦ s x b✝) r) (Subrel r fun x ↦ r x a✝) ?refine_1 ?refine_1
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: case refine_1
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
h : succ (iSup f) ≤ lsub f
⊢ ∃ i, f i = iSup f

pp: case refine_2
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
⊢ (∃ i, f i = iSup f) → succ (iSup f) ≤ lsub f

Tactic:
· by_contra! hf
    have := forall_congr' fun i ↦ (Ordinal.le_iSup f i).lt_iff_ne.symm
    exact (succ_le_iff.1 h).ne ((iSup_le_lsub f).antisymm (lsub_le (this.1 hf)))

Goal state after:
case refine_2
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
⊢ (∃ i, f i = iSup f) → succ (iSup f) ≤ lsub f
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case succ
n : ℕ
hn : n ≠ 0
fuel : ℕ
ih :
  ∀ {b : ℕ},
    1 < b →
      n < b ^ fuel →
        (go n b fuel).fst = n / b ^ (go n b fuel).snd ∧ b ^ (go n b fuel).snd ≤ n ∧ n < b ^ ((go n b fuel).snd + 1)
b : ℕ
hb : 1 < b
hfuel : n < b ^ (fuel + 1)
x✝ : n < b ∨ n ≥ b
⊢ (go n b (fuel + 1)).fst = n / b ^ (go n b (fuel + 1)).snd ∧
    b ^ (go n b (fuel + 1)).snd ≤ n ∧ n < b ^ ((go n b (fuel + 1)).snd + 1)

Tactic:
cases Nat.lt_or_ge n b with

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

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

Tactic:
and_congr_right_iff

Goal state after:
f : Ordinal.{u} → Ordinal.{max u v}
⊢ (∀ (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)
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: b : Ordinal.{u_1}
l : IsSuccLimit b
IH : ∀ o' < b, 1 ^ o' = 1
c : Ordinal.{u_1}
H : 1 ≤ c
b' : Ordinal.{u_1}
h : b' < b
⊢ 1 ^ b' ≤ c

Tactic:
rwa [IH _ h]

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 ↦ ?_

Goal state after:
case inr.inr.inl
b k n : ℕ
hn : n ≠ 0
hk : k > 0
hb : 1 < b
c : ℕ
⊢ c ≤ log (b ^ k) n ↔ c ≤ log b n / k
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: n : ℕ
⊢ lift.{u, v} ↑(n + 1) = ↑(n + 1)

Tactic:
by simp [lift_natCast n]

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

Goal state before:
pp: x : ℕ
this : Fintype ↑(Iio x)
⊢ Fintype.card ↑(Iio x) = x

Tactic:
← Fintype.card_fin x

Goal state after:
x : ℕ
this : Fintype ↑(Iio x)
⊢ Fintype.card ↑(Iio x) = Fintype.card (Fin x)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: n : ℕ
o : Ordinal.{u_4}
⊢ o ∈ Nat.cast '' Iio n ↔ o ∈ Iio ↑n

Tactic:
have := @eq_natCast_of_le_natCast o

Goal state after:
n : ℕ
o : Ordinal.{u_4}
this : ∀ {b : ℕ}, o ≤ ↑b → ∃ c, o = ↑c
⊢ o ∈ Nat.cast '' Iio n ↔ o ∈ Iio ↑n
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b n : ℕ
hb : 1 < b
⊢ clog b n < clog b (n + 1) ↔ b ^ clog b n = n

Tactic:
refine ⟨fun H ↦ ?_, fun H ↦ ?_⟩
  · apply le_antisymm _ (le_pow_clog hb n)
    apply le_of_lt_succ
    exact (lt_clog_iff_pow_lt hb).mp H
  · rw [lt_clog_iff_pow_lt hb, H]
    exact n.lt_add_one

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

Goal state before:
pp: case limit
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
o : Ordinal.{u}
l : IsSuccLimit o
IH : ∀ o' < o, f i (derivFamily f o') = derivFamily f o'
this : Nonempty ↑(Set.Iio o)
c : Ordinal.{u}
⊢ (∀ (i_1 : ↑(Set.Iio o)), f i (derivFamily f ↑i_1) ≤ c) ↔ ⨆ b, derivFamily f ↑b ≤ c

Tactic:
Ordinal.iSup_le_iff

Goal state after:
case limit
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
i : ι
H : IsNormal (f i)
o : Ordinal.{u}
l : IsSuccLimit o
IH : ∀ o' < o, f i (derivFamily f o') = derivFamily f o'
this : Nonempty ↑(Set.Iio o)
c : Ordinal.{u}
⊢ (∀ (i_1 : ↑(Set.Iio o)), f i (derivFamily f ↑i_1) ≤ c) ↔ ∀ (i : ↑(Set.Iio o)), derivFamily f ↑i ≤ c
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: a o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
hao : a < o
H : IsNormal (op a)
ho : IsPrincipal op o
ho' : IsSuccLimit o
⊢ ⨆ b, op a ↑b ≤ o

Tactic:
Ordinal.iSup_le_iff

Goal state after:
a o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
hao : a < o
H : IsNormal (op a)
ho : IsPrincipal op o
ho' : IsSuccLimit o
⊢ ∀ (i : ↑(Set.Iio o)), op a ↑i ≤ o
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case a
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
⊢ ⨆ n, f^[n] a ≤ nfp f a

Tactic:
Ordinal.iSup_le_iff

Goal state after:
case a
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
⊢ ∀ (i : ℕ), f^[i] a ≤ nfp f a
Module: Mathlib.SetTheory.Ordinal.Exponential

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

Tactic:
by
  simp_rw [lt_omega0_opow (opow_ne_zero _ omega0_ne_zero), lt_omega0_opow hb]
  constructor
  · intro ⟨a, ⟨b, hb, ⟨m, hm⟩⟩, ⟨n, hn⟩⟩
    exact ⟨_, hb, _, hn.trans <| opow_mul_lt_opow (natCast_lt_omega0 _) <|
      hm.trans_le (mul_le_mul_right (Nat.cast_le.2 m.le_succ) _)⟩
  · intro ⟨a, ha, ⟨n, hn⟩⟩
    refine ⟨ω ^ a * n, ⟨a, ha, n + 1, ?_⟩, 1, ?_⟩
    · simp [mul_lt_mul_iff_right₀, opow_pos]
    · simpa

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

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

Tactic:
obtain rfl | hn := eq_or_ne n 0

Goal state after:
case inr.inl
m : ℕ
hm : 1 < m
⊢ ↑(Nat.log m 0) = log ↑m ↑0

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

Goal state before:
pp: a b : Ordinal.{u_1}
hba : b ≤ a * ω
⊢ a + a * ω ≤ a * ω

Tactic:
← mul_one_add,

Goal state after:
a b : Ordinal.{u_1}
hba : b ≤ a * ω
⊢ a * (1 + ω) ≤ a * ω
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:
← mul_one_add,

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

Goal state before:
pp: case refine_2
a✝ a : Ordinal.{u}
h : deriv (fun x ↦ a✝ + x) a = a✝ * ω + a
⊢ deriv (fun x ↦ a✝ + x) (succ a) = a✝ * ω + succ a

Tactic:
rw [succ_eq_add_one, deriv_add_one, h, ← add_assoc]

Goal state after:
case refine_2
a✝ a : Ordinal.{u}
h : deriv (fun x ↦ a✝ + x) a = a✝ * ω + a
⊢ nfp (fun x ↦ a✝ + x) (a✝ * ω + a + 1) = a✝ * ω + a + 1
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: case h
a : Ordinal.{u_1}
ha' : ω ≤ preOmega a
ha : (preOmega a).IsInitial
⊢ ω_ (a - ω) = preOmega a

Tactic:
omega0_le_preOmega_iff

Goal state after:
case h
a : Ordinal.{u_1}
ha' : ω ≤ a
ha : (preOmega a).IsInitial
⊢ ω_ (a - ω) = preOmega a
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case inr.inr.inl
a b : Cardinal.{u_1}
ha0 : a ≠ 0
hb0 : b ≠ 0
ha : ℵ₀ ≤ a
⊢ max a b ≤ max (max a b) ℵ₀

Tactic:
exact le_max_left _ _

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

Goal state before:
pp: case refine_2
o : Ordinal.{u}
h : ∀ (a : Ordinal.{u}), 0 < a → a < o → a * o = o
a b : Ordinal.{u}
hao : a < o
hbo : b < o
⊢ (fun x1 x2 ↦ x1 * x2) a b < o

Tactic:
· rcases eq_or_ne a 0 with (rfl | ha)
    · dsimp only; rwa [zero_mul]
    rw [← pos_iff_ne_zero] at ha
    rw [← h a ha hao]
    exact (isNormal_mul_right ha).strictMono hbo

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

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

Tactic:
exact le_max_left _ _

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

Goal state before:
pp: o : Ordinal.{u_1}
ho : ω ^ 2 ≤ o
⊢ preAleph o = ℵ_ o

Tactic:
by
  simpa [← ord_inj] using preOmega_of_omega0_sq_le ho

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

Goal state before:
pp: a b c : Ordinal.{u}
c0 : 0 < c
ha : a < ω ^ c
hb : b < ω
⊢ a * b < ω ^ c

Tactic:
by
  rcases zero_or_succ_or_isSuccLimit c with (rfl | ⟨c, rfl⟩ | l)
  · exact (lt_irrefl _).elim c0
  · rw [opow_succ] at ha
    obtain ⟨n, hn, an⟩ :=
      ((isNormal_mul_right <| opow_pos _ omega0_pos).lt_iff_exists_lt isSuccLimit_omega0).1 ha
    grw [an, opow_succ, mul_assoc]
    gcongr
    exacts [opow_pos _ omega0_pos, isPrincipal_mul_omega0 hn hb]
  · rcases ((isNormal_opow one_lt_omega0).lt_iff_exists_lt l).1 ha with ⟨x, hx, ax⟩
    refine (mul_le_mul' (le_of_lt ax) (le_of_lt hb)).trans_lt ?_
    rw [← opow_succ, opow_lt_opow_iff_right one_lt_omega0]
    exact l.succ_lt hx

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

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

Tactic:
exact le_max_left _ _

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

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

Tactic:
exact le_max_left _ _

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

Goal state before:
pp: case a
a b : Ordinal.{u}
ha : a ≠ 0
hb : IsPrincipal (fun x1 x2 ↦ x1 * x2) b
hb₂ : 2 < b
hbl : IsSuccLimit b
⊢ ⨆ b_1, a * ↑b_1 ≤ b ^ succ (log b a)

Tactic:
Ordinal.iSup_le_iff

Goal state after:
case a
a b : Ordinal.{u}
ha : a ≠ 0
hb : IsPrincipal (fun x1 x2 ↦ x1 * x2) b
hb₂ : 2 < b
hbl : IsSuccLimit b
⊢ ∀ (i : ↑(Set.Iio b)), a * ↑i ≤ b ^ succ (log b a)
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: c : Cardinal.{u}
n : ℕ
⊢ ℵ_ ↑n = lift.{v, u} c ↔ ℵ_ ↑n = c

Tactic:
by
  simpa using lift_inj (a := ℵ_ n)

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

Goal state before:
pp: α : Type u
f : α → Ordinal.{u}
a : Ordinal.{u}
ha : Cardinal.lift.{u, u} #α < (lift.{u, u} a).cof
hf : ∀ (i : α), f i < a
⊢ ⨆ i, f i < a

Tactic:
simpa using lift_iSup_lt_of_lt_cof ha hf

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

Goal state before:
pp: case le_cof_ord
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
hc₀ : ℵ₀ ≤ succ c
hc' : (succ c).ord.cof < succ c
f : ↑(Iio (succ c).ord.cof.ord) → ↑(Iio (succ c).ord)
hf : IsFundamentalSeq f
⊢ ⨆ i, ↑(f i) + 1 < (succ c).ord

Tactic:
← card_le_iff

Goal state after:
case le_cof_ord
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
hc₀ : ℵ₀ ≤ succ c
hc' : (succ c).ord.cof < succ c
f : ↑(Iio (succ c).ord.cof.ord) → ↑(Iio (succ c).ord)
hf : IsFundamentalSeq f
⊢ (⨆ i, ↑(f i) + 1).card ≤ c
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: ι : Type u
inst✝ : Infinite ι
c : ι → Cardinal.{v}
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift.{u, v} (c i) ≤ lift.{v, u} #ι
⊢ prod c = 2 ^ lift.{v, u} #ι

Tactic:
rw [← lift_id'.{u, v} (prod.{u, v} c), lift_prod, ← lift_two_power]

Goal state after:
ι : Type u
inst✝ : Infinite ι
c : ι → Cardinal.{v}
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift.{u, v} (c i) ≤ lift.{v, u} #ι
⊢ (prod fun i ↦ lift.{u, v} (c i)) = lift.{v, u} (2 ^ #ι)
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case pos
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
h : IsMin o
⊢ (preOmega o).cof = o.cof

pp: case neg
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
h : ¬IsMin o
⊢ (preOmega o).cof = o.cof

Tactic:
· simp [h.eq_bot]

Goal state after:
case neg
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
h : ¬IsMin o
⊢ (preOmega o).cof = o.cof
Module: Mathlib.SetTheory.Cardinal.Arithmetic

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

Tactic:
rcases le_or_gt ℵ₀ c with hc | hc
  · exact le_max_of_le_left (power_nat_le hc)
  · exact le_max_of_le_right (power_lt_aleph0 hc natCast_lt_aleph0).le

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

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

Tactic:
apply bounded_singleton
      rw [← hr]
      apply isSuccLimit_ord ha

Goal state after:
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case inr
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), β i
i : ι
b : β i
s : { s // ∀ (i : ι), i ∈ s ∨ f.toFun i = 0 }
j : ι
hi : i ≠ j
⊢ j ∈ i ::ₘ ↑s ∨ Function.update (⇑f) i b j = 0

Tactic:
· obtain hj | (hj : f j = 0) := s.prop j
          · exact Or.inl (Multiset.mem_cons_of_mem hj)
          · exact Or.inr ((Function.update_of_ne hi.symm b _).trans hj)

Goal state after:
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case h.cons
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f i = 0 → b ≠ 0 → p f → p (single i b + f)
i : ι
s : Multiset ι
ih : ∀ (f : (i : ι) → β i) (H : ∀ (i : ι), i ∈ s ∨ f i = 0), p { toFun := f, support' := Trunc.mk ⟨s, H⟩ }
f : (i : ι) → β i
H : ∀ (i_1 : ι), i_1 ∈ i ::ₘ s ∨ f i_1 = 0
⊢ p { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ }

Tactic:
have H2 : p (erase i ⟨f, Trunc.mk ⟨i ::ₘ s, H⟩⟩) := by
    dsimp only [erase, Trunc.map, Trunc.bind, Trunc.liftOn, Trunc.lift_mk,
      Function.comp, Subtype.coe_mk]
    have H2 : ∀ j, j ∈ s ∨ ite (j = i) 0 (f j) = 0 := by grind
    have H3 : ∀ aux, (⟨fun j : ι => ite (j = i) 0 (f j), Trunc.mk ⟨i ::ₘ s, aux⟩⟩ : Π₀ i, β i) =
        ⟨fun j : ι => ite (j = i) 0 (f j), Trunc.mk ⟨s, H2⟩⟩ :=
      fun _ ↦ ext fun _ => rfl
    rw [H3]
    apply ih

Goal state after:
case h.cons
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f i = 0 → b ≠ 0 → p f → p (single i b + f)
i : ι
s : Multiset ι
ih : ∀ (f : (i : ι) → β i) (H : ∀ (i : ι), i ∈ s ∨ f i = 0), p { toFun := f, support' := Trunc.mk ⟨s, H⟩ }
f : (i : ι) → β i
H : ∀ (i_1 : ι), i_1 ∈ i ::ₘ s ∨ f i_1 = 0
H2 : p (erase i { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ })
⊢ p { toFun := f, support' := Trunc.mk ⟨i ::ₘ s, H⟩ }
Module: Mathlib.LinearAlgebra.Finsupp.SumProd

Goal state before:
pp: α✝ : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
α : Type u_7
β : Type u_8
⊢ ∀ (m : R) (x : α ⊕ β →₀ M),
    sumFinsuppAddEquivProdFinsupp.toFun (m • x) = (RingHom.id R) m • sumFinsuppAddEquivProdFinsupp.toFun x

Tactic:
intros

Goal state after:
α✝ : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
α : Type u_7
β : Type u_8
m✝ : R
x✝ : α ⊕ β →₀ M
⊢ sumFinsuppAddEquivProdFinsupp.toFun (m✝ • x✝) = (RingHom.id R) m✝ • sumFinsuppAddEquivProdFinsupp.toFun x✝