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

Goal state before:
pp: α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
inst✝ : Nonempty ι
l : ι → Filter α
s : (i : ι) → ι' i → Set α
p : (i : ι) → ι' i → Prop
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
h : Directed (fun x1 x2 ↦ x1 ≥ x2) l
t : Set α
⊢ (∃ i, t ∈ l i) ↔ ∃ i, p i.fst i.snd ∧ s i.fst i.snd ⊆ t

Tactic:
Sigma.exists

Goal state after:
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
inst✝ : Nonempty ι
l : ι → Filter α
s : (i : ι) → ι' i → Set α
p : (i : ι) → ι' i → Prop
hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)
h : Directed (fun x1 x2 ↦ x1 ≥ x2) l
t : Set α
⊢ (∃ i, t ∈ l i) ↔ ∃ a b, p ⟨a, b⟩.fst ⟨a, b⟩.snd ∧ s ⟨a, b⟩.fst ⟨a, b⟩.snd ⊆ t
Module: Mathlib.Order.Interval.Set.Disjoint

Goal state before:
pp: α : Type v
inst✝ : Preorder α
a b : α
⊢ Disjoint (Ici a) (Iic b) ↔ ¬a ≤ b

Tactic:
Set.disjoint_iff_inter_eq_empty,

Goal state after:
α : Type v
inst✝ : Preorder α
a b : α
⊢ Ici a ∩ Iic b = ∅ ↔ ¬a ≤ b
Module: Mathlib.Order.Interval.Set.Disjoint

Goal state before:
pp: α : Type v
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
⊢ Disjoint (Ico a₁ a₂) (Ico b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁

Tactic:
Set.disjoint_iff_inter_eq_empty,

Goal state after:
α : Type v
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
⊢ Ico a₁ a₂ ∩ Ico b₁ b₂ = ∅ ↔ min a₂ b₂ ≤ max a₁ b₁
Module: Mathlib.Order.Interval.Set.Disjoint

Goal state before:
pp: α : Type v
inst✝¹ : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst✝ : DenselyOrdered α
⊢ Disjoint (Ioo a₁ a₂) (Ioo b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁

Tactic:
Set.disjoint_iff_inter_eq_empty,

Goal state after:
α : Type v
inst✝¹ : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst✝ : DenselyOrdered α
⊢ Ioo a₁ a₂ ∩ Ioo b₁ b₂ = ∅ ↔ min a₂ b₂ ≤ max a₁ b₁
Module: Mathlib.Order.Interval.Set.Disjoint

Goal state before:
pp: ι : Sort u
α : Type v
inst✝ : LinearOrder α
f : ι → α
a : α
⊢ ⋃ i, Icc a (f i) = Ici a ↔ ∀ x ≥ a, ∃ i, x ≤ f i

Tactic:
simp [← Ici_inter_Iic, ← inter_iUnion, subset_def]

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

Goal state before:
pp: α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
dom : Set ι
hdom : dom.Nonempty
l : ι → Filter α
s : (i : ι) → ι' i → Set α
p : (i : ι) → ι' i → Prop
hl : ∀ i ∈ dom, (l i).HasBasis (p i) (s i)
h : DirectedOn (l ⁻¹'o GE.ge) dom
t : Set α
⊢ (∃ i ∈ dom, t ∈ l i) ↔ ∃ i, (i.fst ∈ dom ∧ p i.fst i.snd) ∧ s i.fst i.snd ⊆ t

Tactic:
Sigma.exists

Goal state after:
α : Type u_1
ι : Type u_6
ι' : ι → Type u_7
dom : Set ι
hdom : dom.Nonempty
l : ι → Filter α
s : (i : ι) → ι' i → Set α
p : (i : ι) → ι' i → Prop
hl : ∀ i ∈ dom, (l i).HasBasis (p i) (s i)
h : DirectedOn (l ⁻¹'o GE.ge) dom
t : Set α
⊢ (∃ i ∈ dom, t ∈ l i) ↔ ∃ a b, (⟨a, b⟩.fst ∈ dom ∧ p ⟨a, b⟩.fst ⟨a, b⟩.snd) ∧ s ⟨a, b⟩.fst ⟨a, b⟩.snd ⊆ t
Module: Mathlib.Order.Interval.Set.Disjoint

Goal state before:
pp: α : Type v
inst✝ : LinearOrder α
s : Set α
a : α
a_glb : IsGLB s a
a_notMem : a ∉ s
⊢ ⋃ x ∈ s, Ici x = Ioi a

Tactic:
by
  refine (iUnion₂_subset fun x hx => ?_).antisymm fun x hx => ?_
  · exact Ici_subset_Ioi.mpr (lt_of_le_of_ne (a_glb.1 hx) fun h => (h ▸ a_notMem) hx)
  · rcases a_glb.exists_between hx with ⟨y, hys, _, hyx⟩
    rw [mem_iUnion₂]
    exact ⟨y, hys, hyx.le⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ map inl f ⊓ map inr g ≤ map inl ⊤ ⊓ map inr ⊤

Tactic:
apply inf_le_inf <;> simp

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

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

Tactic:
by_contra H

Goal state after:
α : Type u
p : α → Prop
f : Filter α
hp : ∃ᶠ (x : α) in f, p x
H : ¬∃ x, p x
⊢ False
Module: Mathlib.Order.Filter.Basic

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

Tactic:
by
  simp [Filter.Frequently]

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

Goal state before:
pp: α : Type u
f : Filter α
s : Set α
p : α → Prop
⊢ (∃ᶠ (x : α) in f ⊓ 𝓟 s, p x) ↔ ∃ᶠ (x : α) in f, x ∈ s ∧ p x

Tactic:
by
  simp only [Filter.Frequently, eventually_inf_principal, not_and]

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

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

Tactic:
cases n

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

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)
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: α : Type u_3
f : ℕ → α
l : Filter α
k : ℕ
⊢ Tendsto (f ∘ fun n ↦ n + k) atTop l ↔ Tendsto f atTop l

Tactic:
rw [← tendsto_map'_iff, map_add_atTop_eq_nat]

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
e✝ e : α ≃ β
inst✝¹ : AddCommMonoid β
inst✝ : Module R β
this : AddCommMonoid α := e.addCommMonoid
module : Module R α := Equiv.module R e
r : R
x : α
⊢ e.addEquiv.toEquiv (r • x) = r • e.addEquiv.toEquiv x

Tactic:
exact Iff.mp (eq_symm_apply _) rfl

Goal state after:
Module: Mathlib.Data.Set.Finite.Lemmas

Goal state before:
pp: α : Type u
s : Set α
h : s.Finite
⊢ range ⇑(Fintype.equivFin ↑↑h.toFinset).symm.asEmbedding = s

Tactic:
by
    simp only [Finset.coe_sort_coe, Equiv.asEmbedding_range, Finite.coe_toFinset, ofPred_mem_eq]

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

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
ι : Type u_5
M : ι → Type u_6
inst✝² : Finite ι
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
p : (i : ι) → Submodule R (M i)
t : (i : ι) → Set (M i)
htf : ∀ (i : ι), (t i).Finite
hts : ∀ (i : ι), span R (t i) = p i
⊢ ⨆ i, map (LinearMap.single R M i) (span R (t i)) = pi univ p

Tactic:
hts,

Goal state after:
R : Type u_1
inst✝³ : Semiring R
ι : Type u_5
M : ι → Type u_6
inst✝² : Finite ι
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
p : (i : ι) → Submodule R (M i)
t : (i : ι) → Set (M i)
htf : ∀ (i : ι), (t i).Finite
hts : ∀ (i : ι), span R (t i) = p i
⊢ ⨆ i, map (LinearMap.single R M i) (p i) = pi univ p
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
S : Type u_3
P : Type u_4
inst✝⁴ : Semiring S
inst✝³ : AddCommMonoid P
inst✝² : Module S P
σ : R →+* S
inst✝¹ : RingHomSurjective σ
inst✝ : Module.Finite R M
f : M →ₛₗ[σ] P
⊢ f.range.FG

Tactic:
rw [LinearMap.range_eq_map]
  exact Module.Finite.fg_top.map f

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

Goal state before:
pp: case inr.inl
α : Type u_1
β : Type u_2
b : β
inst✝⁶ : Zero α
inst✝⁵ : Zero β
inst✝⁴ : SMulWithZero α β
inst✝³ : LinearOrder α
inst✝² : LinearOrder β
inst✝¹ : PosSMulMono α β
inst✝ : SMulPosMono α β
hab : 0 < 0
⊢ 0 < 0 ∧ 0 < b ∨ 0 < 0 ∧ b < 0

Tactic:
exact hab.false.elim

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

Goal state before:
pp: case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
s : Set β
hs : IsCofinal s
g : ↑s → α
hg : ∀ (x : ↑s), ↑x ≤ f (g x)
a b : α
hb : f a ≤ f b
c : β
hc : c ∈ s
hc' : f b ≤ c
⊢ a ≤ g ⟨c, hc⟩

Tactic:
← hf.le_iff_le

Goal state after:
case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
s : Set β
hs : IsCofinal s
g : ↑s → α
hg : ∀ (x : ↑s), ↑x ≤ f (g x)
a b : α
hb : f a ≤ f b
c : β
hc : c ∈ s
hc' : f b ≤ c
⊢ f a ≤ f (g ⟨c, hc⟩)
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : β → α
g : α → β
h : GaloisConnection f g
⊢ lift.{u, v} (cof β) ≤ lift.{v, u} (cof α)

Tactic:
by
  rw [le_lift_cof_iff]
  exact fun s hs ↦ (lift_le.2 <| cof_le (h.map_isCofinal hs)).trans mk_image_le_lift

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ DirSupInacc Set.univ

Tactic:
simp [← compl_empty]

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s t : Set α
D : Set (Set α)
inst✝ : Preorder α
hDL : IsLowerSet D
hs : DirSupClosedOn D s
ht : DirSupClosedOn D t
⊢ DirSupClosedOn D (s ∪ t)

Tactic:
intro d hD hdu hd₀ hd₁ a ha
  have hdst : d ∩ s ∪ d ∩ t = d := by grind
  wlog h : DirectedOn (· ≤ ·) (d ∩ s) ∧ IsCofinalFor (d ∩ t) (d ∩ s)
  · rw [union_comm] at hdu hdst ⊢
    exact this hDL ht hs hD hdu hd₀ hd₁ ha hdst <|
      (directedOn_union_iff.mp (by rwa [hdst])).resolve_right h
  obtain ⟨hds, hcof⟩ := h
  have hcof' : IsCofinalFor d (d ∩ s) := hcof.union_right.mono_left hdst.ge
  exact .inl <| hs (hDL inter_subset_left hD) inter_subset_right
    (hcof'.nonempty hd₀) hds (ha.of_isCofinalFor inter_subset_left hcof')

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
β : ι → Type u_4
inst✝⁵ : Zero α
inst✝⁴ : (i : ι) → Zero (β i)
inst✝³ : PartialOrder α
inst✝² : (i : ι) → PartialOrder (β i)
inst✝¹ : (i : ι) → SMulWithZero α (β i)
inst✝ : ∀ (i : ι), SMulPosStrictMono α (β i)
a : (i : ι) → β i
ha : 0 ≤ a
i : ι
hi : 0 i < a i
_b₁ _b₂ : α
hb : _b₁ < _b₂
⊢ _b₁ • a ≤ _b₂ • a ∧ ∃ i, (_b₁ • a) i < (_b₂ • a) i

Tactic:
exact ⟨smul_le_smul_of_nonneg_right hb.le ha, i, smul_lt_smul_of_pos_right hb hi⟩

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
b : β
hb : b ⋖ f a
c : α
hc : c < a
hc'✝ : b < f c
hc' : f a ≤ f c
⊢ False

Tactic:
hf.strictMono.le_iff_le

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
b : β
hb : b ⋖ f a
c : α
hc : c < a
hc'✝ : b < f c
hc' : a ≤ c
⊢ False
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : WellFoundedLT α
inst✝⁴ : SuccOrder α
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder α
inst✝¹ : OrderBot α
inst✝ : WellFoundedLT β
f : α → β
x : β
hf : IsNormal f
hf' : ∃ y, x ≤ f y
hx : f ⊥ ≤ x
this✝¹ : Nonempty β
this✝ : OrderBot β := WellFoundedLT.toOrderBot β
this : ConditionallyCompleteLinearOrderBot α := WellFoundedLT.conditionallyCompleteLinearOrderBot α
⊢ ∃ a, f a ≤ x ∧ x < f (succ a)

Tactic:
let := WellFoundedLT.conditionallyCompleteLinearOrderBot β

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : WellFoundedLT α
inst✝⁴ : SuccOrder α
inst✝³ : LinearOrder β
inst✝² : NoMaxOrder α
inst✝¹ : OrderBot α
inst✝ : WellFoundedLT β
f : α → β
x : β
hf : IsNormal f
hf' : ∃ y, x ≤ f y
hx : f ⊥ ≤ x
this✝² : Nonempty β
this✝¹ : OrderBot β := WellFoundedLT.toOrderBot β
this✝ : ConditionallyCompleteLinearOrderBot α := WellFoundedLT.conditionallyCompleteLinearOrderBot α
this : ConditionallyCompleteLinearOrderBot β := WellFoundedLT.conditionallyCompleteLinearOrderBot β
⊢ ∃ a, f a ≤ x ∧ x < f (succ a)
Module: Mathlib.SetTheory.Ordinal.Univ

Goal state before:
pp: c : Cardinal.{u}
⊢ lift.{max (u + 1) v, u} c < univ.{u, v}

Tactic:
have := lift_lt.{_, max (u + 1) v}.2 (lift_lt_univ c)

Goal state after:
c : Cardinal.{u}
this : lift.{max (u + 1) v, u + 1} (lift.{u + 1, u} c) < lift.{max (u + 1) v, u + 1} univ.{u, u + 1}
⊢ lift.{max (u + 1) v, u} c < univ.{u, v}
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b : Ordinal.{u_4}
⊢ a.pred ≤ b ↔ a ≤ succ b

Tactic:
obtain ⟨a, rfl⟩ | ha := mem_range_succ_or_isSuccPrelimit a

Goal state after:
case inl
b a : Ordinal.{u_4}
⊢ (succ a).pred ≤ b ↔ succ a ≤ succ b

case inr
a b : Ordinal.{u_4}
ha : IsSuccPrelimit a
⊢ a.pred ≤ b ↔ a ≤ succ b
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' : r b₁✝ b₂✝
⊢ Prod.Lex t s ((a✝, b₁✝).1, f (a✝, b₁✝).2) ((a✝, b₂✝).1, f (a✝, b₂✝).2)

Tactic:
exact Prod.Lex.right _ (f.toRelEmbedding.map_rel_iff.2 h')

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

Tactic:
IH,

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.Arithmetic

Goal state before:
pp: a b c : Ordinal.{u_4}
h : c ∣ b
⊢ a % b % c = a % c

Tactic:
← div_add_mod a b

Goal state after:
a b c : Ordinal.{u_4}
h : c ∣ b
⊢ a % b % c = (b * (a / b) + a % b) % c
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inl
b n : ℕ
hb : b ≤ 1
⊢ log b (n / b * b) = log b n

pp: case inr
b n : ℕ
hb : 1 < b
⊢ log b (n / b * b) = log b n

Tactic:
· rw [log_of_left_le_one hb, log_of_left_le_one hb]

Goal state after:
case inr
b n : ℕ
hb : 1 < b
⊢ log b (n / b * b) = log b n
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) * a = a ^ b * a ^ (c + 1)

Tactic:
IH,

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

Tactic:
IH,

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

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

Tactic:
simp_rw [isSuccPrelimit_iff_succ_lt, succ_eq_add_one, lt_ord, card_add_one]
    refine fun a ha ↦ ?_
    contrapose! ha
    rwa [add_one_of_aleph0_le] at ha
    rw [← ord_le, ← IsSuccLimit.le_succ_iff, succ_eq_add_one, ord_le, card_add_one]
    · exact hc.trans ha
    · simp

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

Goal state before:
pp: case inr.inr
b x y : Ordinal.{u_1}
xy : x ≤ y
hx : x ≠ 0
hb : b ≤ 1
⊢ log b x ≤ log b y

Tactic:
· rw [log_of_left_le_one hb, log_of_left_le_one hb]

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

Goal state before:
pp: case mpr.a
b x : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
y : Ordinal.{u_1}
hx₁ : b ^ y ≤ x
hx₂ : x < b ^ (y + 1)
⊢ log b x ≤ y

Tactic:
rwa [← lt_add_one_iff, ← lt_opow_iff_log_lt hb hx]

Goal state after:
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
⊢ ∀ (i : ↑(Set.Iio o)), op a ↑i ≤ o

Tactic:
exact fun ⟨b, hbo⟩ ↦ (ho hao hbo).le

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

Goal state before:
pp: a : Ordinal.{u_1}
n : ℕ
⊢ 0^[n] a ≤ 0^[0] a

Tactic:
cases n

Goal state after:
case zero
a : Ordinal.{u_1}
⊢ 0^[0] a ≤ 0^[0] a

case succ
a : Ordinal.{u_1}
n✝ : ℕ
⊢ 0^[n✝ + 1] a ≤ 0^[0] a
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: ⊢ preOmega 0 = 0

Tactic:
rw [coe_preOmega, enumOrd_zero]

Goal state after:
⊢ sInf {x | x.IsInitial} = 0
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ω ≤ ω_ o

Tactic:
rw [← omega_zero, omega_le_omega]
  exact zero_le

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

Goal state before:
pp: case mpr.inl
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) 0

pp: case mpr.inr
a : Ordinal.{u}
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) ((fun x ↦ ω ^ x) a)

Tactic:
exacts [isPrincipal_zero, isPrincipal_add_omega0_opow a]

Goal state after:
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:
rw [← mul_assoc, ← opow_one_add, one_add_omega0]

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

Goal state before:
pp: case inr.inr
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : IsPrincipal (fun x1 x2 ↦ x1 + x2) b
h✝ : 0 < a
hb₁' : 1 ≤ b
c d : Ordinal.{u}
hc : ∃ c' < b, c < a * c'
hd : ∃ c' < b, d < a * c'
⊢ ∃ c' < b, (fun x1 x2 ↦ x1 + x2) c d < a * c'

Tactic:
rcases hc with ⟨x, hx, hx'⟩

Goal state after:
case inr.inr
a b : Ordinal.{u}
hb₁ : b ≠ 1
hb : IsPrincipal (fun x1 x2 ↦ x1 + x2) b
h✝ : 0 < a
hb₁' : 1 ≤ b
c d : Ordinal.{u}
hd : ∃ c' < b, d < a * c'
x : Ordinal.{u}
hx : x < b
hx' : c < a * x
⊢ ∃ c' < b, (fun x1 x2 ↦ x1 + x2) c d < a * c'
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:
by
  cases o using inductionOnWellOrder with | type α
  rw [cof_type, ← type_lt_ulift, cof_type, ← Cardinal.lift_id'.{u, v} (Order.cof (ULift _)),
    ← Cardinal.lift_umax, ← ULift.orderIso.lift_cof_congr]

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

Goal state before:
pp: case inr.inr
a b c : Ordinal.{u}
c0 : 0 < c
ha : a < ω ^ c
hb : b < ω
l : IsSuccLimit c
x : Ordinal.{u}
hx : x < c
ax : a < ω ^ x
⊢ ω ^ x * ω < ω ^ c

Tactic:
← opow_succ,

Goal state after:
case inr.inr
a b c : Ordinal.{u}
c0 : 0 < c
ha : a < ω ^ c
hb : b < ω
l : IsSuccLimit c
x : Ordinal.{u}
hx : x < c
ax : a < ω ^ x
⊢ ω ^ succ x < ω ^ c
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case refine_1
o : Ordinal.{u}
ho : IsPrincipal (fun x1 x2 ↦ x1 * x2) o
⊢ o ≤ 2 ∨ o ∈ Set.range fun x ↦ ω ^ ω ^ x

Tactic:
rcases le_or_gt o 2 with ho₂ | ho₂

Goal state after:
case refine_1.inl
o : Ordinal.{u}
ho : IsPrincipal (fun x1 x2 ↦ x1 * x2) o
ho₂ : o ≤ 2
⊢ o ≤ 2 ∨ o ∈ Set.range fun x ↦ ω ^ ω ^ x

case refine_1.inr
o : Ordinal.{u}
ho : IsPrincipal (fun x1 x2 ↦ x1 * x2) o
ho₂ : 2 < o
⊢ o ≤ 2 ∨ o ∈ Set.range fun x ↦ ω ^ ω ^ x
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
⊢ 1 < m → n * 1 < n * m

Tactic:
rw [Nat.mul_lt_mul_left]

Goal state after:
n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
⊢ 1 < m → 1 < m

n m : ℕ
h2a : 1 ≤ n
hb : 1 ≤ m
h : n * m = n
⊢ 0 < n
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)
  · simp [ciSup_of_not_bddAbove hf]
  simp_rw [← mk_toType]
  rw [← mk_sigma, ← Cardinal.lift_id'.{v} #(Σ _, _), ← Cardinal.lift_umax.{v, u}]
  apply lift_mk_le_lift_mk_of_surjective (f := .mk ∘ (⟨·.2.toOrd,
    (mem_Iio.mp (ToType.toOrd _).2).trans_le (le_ciSup hf _)⟩))
  rw [EquivLike.comp_surjective]
  rintro ⟨x, hx⟩
  obtain ⟨i, hi⟩ := (lt_ciSup_iff' hf).mp hx
  exact ⟨⟨i, .mk ⟨x, hi⟩⟩, by simp⟩

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

Goal state before:
pp: a o : Ordinal.{u_1}
f : ↑(Iio a) → ↑(Iio o)
hf : IsFundamentalSeq f
ha : 1 < a
⊢ 1 < o.cof

Tactic:
← ord_lt_ord,

Goal state after:
a o : Ordinal.{u_1}
f : ↑(Iio a) → ↑(Iio o)
hf : IsFundamentalSeq f
ha : 1 < a
⊢ ord 1 < o.cof.ord
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: s : Set Cardinal.{u}
a : Cardinal.{u}
ha : #↑s < (Cardinal.lift.{u + 1, u} a).ord.cof
hs : ∀ i ∈ s, i < a
⊢ sSup s < a

Tactic:
← ord_lt_ord,

Goal state after:
s : Set Cardinal.{u}
a : Cardinal.{u}
ha : #↑s < (Cardinal.lift.{u + 1, u} a).ord.cof
hs : ∀ i ∈ s, i < a
⊢ (sSup s).ord < a.ord
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

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

Tactic:
← ord_lt_ord,

Goal state after:
β : Type v
f : β → Cardinal.{u}
a : Cardinal.{u}
ha : Cardinal.lift.{u, v} #β < (Cardinal.lift.{v, u} a).ord.cof
hf : ∀ (i : β), f i < a
⊢ (⨆ i, f i).ord < a.ord
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

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

Tactic:
← ord_lt_ord,

Goal state after:
α : Type u
f : α → Cardinal.{u}
a : Cardinal.{u}
ha : #α < a.ord.cof
hf : ∀ (i : α), f i < a
⊢ (⨆ i, f i).ord < a.ord
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case inl
α : Type u_1
h : (#α).IsStrongPrelimit
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha : #α = 0
⊢ #{ s // Bounded r s } = #α

pp: case inr
α : Type u_1
h : (#α).IsStrongPrelimit
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha : #α ≠ 0
⊢ #{ s // Bounded r s } = #α

Tactic:
· rw [ha]
    have := mk_eq_zero_iff.1 ha
    rw [mk_eq_zero_iff]
    constructor
    rintro ⟨s, hs⟩
    exact (not_unbounded_iff s).2 hs (unbounded_of_isEmpty s)

Goal state after:
case inr
α : Type u_1
h : (#α).IsStrongPrelimit
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha : #α ≠ 0
⊢ #{ s // Bounded r s } = #α
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
a : Ordinal.{max u v}
ha : a < c.ord
⊢ ℵ₀ < c.ord.cof

Tactic:
rw [hc.cof_ord]

Goal state after:
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
a : Ordinal.{max u v}
ha : a < c.ord
⊢ ℵ₀ < c
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
a : Ordinal.{max u v}
ha : a < c.ord
⊢ lift.{v, u} #ι < c.ord.cof

Tactic:
rw [hc.cof_ord]

Goal state after:
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
a : Ordinal.{max u v}
ha : a < c.ord
⊢ lift.{v, u} #ι < c
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: f : Ordinal.{u_1} → Ordinal.{u_1}
c : Cardinal.{u_1}
hc : c.IsRegular
hc' : c ≠ ℵ₀
hf : ∀ i < c.ord, f i < c.ord
a : Ordinal.{u_1}
⊢ ℵ₀ < c.ord.cof

Tactic:
rw [hc.cof_ord]

Goal state after:
f : Ordinal.{u_1} → Ordinal.{u_1}
c : Cardinal.{u_1}
hc : c.IsRegular
hc' : c ≠ ℵ₀
hf : ∀ i < c.ord, f i < c.ord
a : Ordinal.{u_1}
⊢ ℵ₀ < c
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
a : Ordinal.{max u v}
⊢ ℵ₀ < c.ord.cof

Tactic:
rw [hc.cof_ord]

Goal state after:
ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
a : Ordinal.{max u v}
⊢ ℵ₀ < c
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u
β' : Type v
inst✝ : Infinite α
leq : lift.{v, u} #α = lift.{u, v} #β'
⊢ #(α ≃ β') = 2 ^ lift.{v, u} #α

Tactic:
simp [mk_equiv_eq_arrow_of_lift_eq leq, ← leq, power_self_eq]

Goal state after: