mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: case inl
M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
k m n : ℕ
h : m ≤ n + 1
this : ∀ i < m, i ≤ n
hkm : k < m
⊢ ∏ j ∈ Ico k m, f (n - j) = ∏ j ∈ Ico (n + 1 - m) (n + 1 - k), f j

pp: case inr
M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
k m n : ℕ
h : m ≤ n + 1
this : ∀ i < m, i ≤ n
hkm : m ≤ k
⊢ ∏ j ∈ Ico k m, f (n - j) = ∏ j ∈ Ico (n + 1 - m) (n + 1 - k), f j

Tactic:
· rw [← Nat.Ico_image_const_sub_eq_Ico (this _ hkm)]
    refine (prod_image ?_).symm
    simp only [mem_Ico, Set.InjOn, mem_coe]
    rintro i ⟨_, im⟩ j ⟨_, jm⟩ Hij
    rw [← tsub_tsub_cancel_of_le (this _ im), Hij, tsub_tsub_cancel_of_le (this _ jm)]

Goal state after:
case inr
M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
k m n : ℕ
h : m ≤ n + 1
this : ∀ i < m, i ≤ n
hkm : m ≤ k
⊢ ∏ j ∈ Ico k m, f (n - j) = ∏ j ∈ Ico (n + 1 - m) (n + 1 - k), f j
Module: Mathlib.Order.Disjointed

Goal state before:
pp: α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : OrderBot ι
f : ι → α
hf : Monotone f
m n : ι
hm : n ≤ m
⊢ (Ioc n m).sup (disjointed f) = f m \ f n

Tactic:
by
  let : SuccOrder ι := LinearLocallyFiniteOrder.succOrder ι
  induction hm using Succ.rec with
  | rfl => simp
  | succ m hm ih =>
    by_cases h'm : IsMax m
    · simpa [Order.succ_eq_iff_isMax.mpr h'm] using ih
    · rw [← Finset.insert_Ioc_right_eq_Ioc_succ_of_not_isMax hm h'm]
      simp only [sup_insert, hf.disjointed_succ h'm, ih]
      exact sdiff_sup_sdiff_cancel (hf (Order.le_succ m)) (hf hm)

Goal state after:
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : OrderBot ι
n : ℕ
⊢ (fun i ↦ (toZ ⊥ i).toNat) ((fun n ↦ succ^[n] ⊥) n) = n

Tactic:
dsimp only
    rw [toZ_iterate_succ]
    exact Int.toNat_natCast n

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

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
n : ℕ
f : ℕ × ℕ → M
⊢ f (0, n + 1).swap * ∏ p ∈ antidiagonal n, f (p.swap.1 + 1, p.swap.2).swap =
    f (n + 1, 0) * ∏ p ∈ antidiagonal n, f (p.1, p.2 + 1)
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
h : a * b * a = 0
this : a * a * b = 0
⊢ a * b = 0

Tactic:
ha.eq

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
h : a * b * a = 0
this : a * b = 0
⊢ a * b = 0
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝ : Semiring α
s : Set (Ideal α)
hs : s.Nonempty
hs' : IsChain (fun x1 x2 ↦ x1 ≤ x2) s
H : ∀ p ∈ s, p.IsPrime
x✝ y✝ : α
e : ∀ ⦃I : Ideal α⦄, I ∈ s → x✝ * y✝ ∈ I
hx : ¬∀ ⦃I : Ideal α⦄, I ∈ s → x✝ ∈ I
⊢ ∀ ⦃I : Ideal α⦄, I ∈ s → y✝ ∈ I

Tactic:
push Not at hx

Goal state after:
α : Type u
inst✝ : Semiring α
s : Set (Ideal α)
hs : s.Nonempty
hs' : IsChain (fun x1 x2 ↦ x1 ≤ x2) s
H : ∀ p ∈ s, p.IsPrime
x✝ y✝ : α
e : ∀ ⦃I : Ideal α⦄, I ∈ s → x✝ * y✝ ∈ I
hx : ∃ I ∈ s, x✝ ∉ I
⊢ ∀ ⦃I : Ideal α⦄, I ∈ s → y✝ ∈ I
Module: Mathlib.Algebra.Module.Submodule.IterateMapComap

Goal state before:
pp: case zero.succ
R : Type u_1
N : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f i : N →ₗ[R] M
K : Submodule R N
hf : Surjective ⇑f
hi : Injective ⇑i
heq : f.iterateMapComap i 0 K ≠ f.iterateMapComap i (0 + 1) K
m : ℕ
ih : f.iterateMapComap i m K ≠ f.iterateMapComap i (m + 1) K
⊢ ((fun K ↦ comap f (map i K)) ∘ (fun K ↦ comap f (map i K))^[m]) K ≠ (fun K ↦ comap f (map i K))^[m + 1 + 1] K

Tactic:
iterate_succ'

Goal state after:
case zero.succ
R : Type u_1
N : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f i : N →ₗ[R] M
K : Submodule R N
hf : Surjective ⇑f
hi : Injective ⇑i
heq : f.iterateMapComap i 0 K ≠ f.iterateMapComap i (0 + 1) K
m : ℕ
ih : f.iterateMapComap i m K ≠ f.iterateMapComap i (m + 1) K
⊢ ((fun K ↦ comap f (map i K)) ∘ (fun K ↦ comap f (map i K))^[m]) K ≠
    ((fun K ↦ comap f (map i K)) ∘ (fun K ↦ comap f (map i K))^[m + 1]) K
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
p : ι → Prop
s : ι → Set α
h : IsBasis p s
⊢ ∀ {x y : Set α},
    x ∈ {t | ∃ i, p i ∧ s i = t} → y ∈ {t | ∃ i, p i ∧ s i = t} → ∃ z ∈ {t | ∃ i, p i ∧ s i = t}, z ⊆ x ∩ y

Tactic:
rintro _ _ ⟨i, hi, rfl⟩ ⟨j, hj, rfl⟩
    rcases h.inter hi hj with ⟨k, hk, hk'⟩
    exact ⟨_, ⟨k, hk, rfl⟩, hk'⟩

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

Goal state before:
pp: α : Type u
ι : Sort x
f : ι → Filter α
s✝ : Set α
hs✝ : s✝ ∈ iInf f
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
p_of_f : ∀ (i : ι), ∀ s ∈ f i, p s
q : Set α → Prop := fun t ↦ t ∈ iInf f ∧ ∀ (t' : Set α), t ⊆ t' → p t'
q_mono : Monotone q
i : ι
s : Set α
hs : s ∈ f i
t : Set α
ht : q t
u : Set α
hu : s ∩ t ⊆ u
⊢ u = (u ∪ s) ∩ (u ∪ t)

Tactic:
rwa [← union_eq_left, union_inter_distrib_left, eq_comm] at hu

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

Goal state before:
pp: α : Type u_1
β : Type u_2
g : Filter β
m : α → β
h : g = ⊥
⊢ comap m ⊥ = ⊥

Tactic:
exact comap_bot

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

Goal state before:
pp: α : Type u_1
β : Type u_2
g₁ g₂ : Filter β
m : α → β
⊢ comap m (bif true then g₁ else g₂) ⊔ comap m (bif false then g₁ else g₂) = comap m g₁ ⊔ comap m g₂

Tactic:
Bool.cond_true,

Goal state after:
α : Type u_1
β : Type u_2
g₁ g₂ : Filter β
m : α → β
⊢ comap m g₁ ⊔ comap m (bif false then g₁ else g₂) = comap m g₁ ⊔ comap m g₂
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
t : Set α
⊢ (∃ x, (p x ∧ s x ⊆ t) ∧ ∃ i, p' i ∧ s' i ⊆ t) ↔ ∃ a b, (p a ∧ p' b) ∧ s a ⊆ t ∧ s' b ⊆ t

Tactic:
← exists_and_left

Goal state after:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l l' : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p' s'
t : Set α
⊢ (∃ x x_1, (p x ∧ s x ⊆ t) ∧ p' x_1 ∧ s' x_1 ⊆ t) ↔ ∃ a b, (p a ∧ p' b) ∧ s a ⊆ t ∧ s' b ⊆ t
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f g : Filter α
m : α → β
h : Injective m
⊢ map m (f ⊓ g) = map m f ⊓ map m g

Tactic:
refine map_inf_le.antisymm ?_
  rintro t ⟨s₁, hs₁, s₂, hs₂, ht : m ⁻¹' t = s₁ ∩ s₂⟩
  refine mem_inf_of_inter (image_mem_map hs₁) (image_mem_map hs₂) ?_
  rw [← image_inter h, image_subset_iff, ht]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
la : Filter α
sa : ι → Set α
lb : Filter β
p : ι → Prop
sb : ι → Set β
hla : la.HasBasis p sa
hlb : lb.HasBasis p sb
h_dir : ∀ {i j : ι}, p i → p j → ∃ k, p k ∧ sa k ⊆ sa i ∧ sb k ⊆ sb j
⊢ (la ×ˢ lb).HasBasis p fun i ↦ sa i ×ˢ sb i

Tactic:
simp only [hasBasis_iff, (hla.prod_pprod hlb).mem_iff]
  refine fun t => ⟨?_, ?_⟩
  · rintro ⟨⟨i, j⟩, ⟨hi, hj⟩, hsub : sa i ×ˢ sb j ⊆ t⟩
    rcases h_dir hi hj with ⟨k, hk, ki, kj⟩
    exact ⟨k, hk, (Set.prod_mono ki kj).trans hsub⟩
  · rintro ⟨i, hi, h⟩
    exact ⟨⟨i, i⟩, ⟨hi, hi⟩, h⟩

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

Goal state before:
pp: α : Type u
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ cof α ≤ 1 ↔ ∃ x, IsTop x

Tactic:
le_iff_lt_or_eq,

Goal state after:
α : Type u
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ cof α < 1 ∨ cof α = 1 ↔ ∃ x, IsTop x
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
a₁ a₂ : α
b₁ b₂ : β
inst✝⁶ : Zero α
inst✝⁵ : Zero β
inst✝⁴ : SMulWithZero α β
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : PosSMulStrictMono α β
inst✝ : SMulPosStrictMono α β
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
h₁ : 0 < a₁
h₂ : 0 < b₂
⊢ a₁ • b₁ = a₂ • b₂ ↔ a₁ = a₂ ∧ b₁ = b₂

Tactic:
refine ⟨fun h ↦ ?_, by rintro ⟨rfl, rfl⟩; rfl⟩
  simp only [eq_iff_le_not_lt, ha, hb, true_and]
  refine ⟨fun ha ↦ h.not_lt ?_, fun hb ↦ h.not_lt ?_⟩
  · exact (smul_le_smul_of_nonneg_left hb h₁.le).trans_lt (smul_lt_smul_of_pos_right ha h₂)
  · exact (smul_lt_smul_of_pos_left hb h₁).trans_le (smul_le_smul_of_nonneg_right ha h₂.le)

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: case refine_2
α : 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 β
H : BddAbove (f ⁻¹' Iic x)
⊢ x < f (succ (sSup (f ⁻¹' Iic x)))

Tactic:
· rw [← not_le, hf.le_iff_le_sSup ⟨⊥, hx⟩ H, not_le, lt_succ_iff]

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
f : α → α
hf : IsNormal f
s : Set α
hs : s ⊆ range f
hs₀ : s.Nonempty
a✝ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
a : α
ha : IsLUB s a
hf' : (f ⁻¹' s).Nonempty
this : Nonempty α
⊢ a ∈ range f

Tactic:
let := WellFoundedLT.toOrderBot α

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
f : α → α
hf : IsNormal f
s : Set α
hs : s ⊆ range f
hs₀ : s.Nonempty
a✝ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
a : α
ha : IsLUB s a
hf' : (f ⁻¹' s).Nonempty
this✝ : Nonempty α
this : OrderBot α := WellFoundedLT.toOrderBot α
⊢ a ∈ range f
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:
by
  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: α : Type u_1
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : IsSuccLimit (type r)
x b : α
hb : b ∈ {x}
⊢ r b ((enum r) ⟨succ ((typein r).toRelEmbedding x), ⋯⟩)

Tactic:
rw [mem_singleton_iff.1 hb]

Goal state after:
α : Type u_1
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : IsSuccLimit (type r)
x b : α
hb : b ∈ {x}
⊢ r x ((enum r) ⟨succ ((typein r).toRelEmbedding x), ⋯⟩)
Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
⊢ typeLT ↑s = typeLT α

Tactic:
apply (RelEmbedding.ofMonotone Subtype.val (by simp)).ordinal_type_le.antisymm
  rw [← ord_cardinalMk, ord_le, card_type, ← cof_eq_cardinalMk]
  exact cof_le hs

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
f : α → α
⊢ Subtype.val ∘ ⇑(enum s hs) = f ↔ StrictMono f ∧ range f = s

Tactic:
have H := (Subtype.strictMono_coe _).comp (enum s hs).strictMono

Goal state after:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
f : α → α
H : StrictMono (Subtype.val ∘ ⇑(enum s hs))
⊢ Subtype.val ∘ ⇑(enum s hs) = f ↔ StrictMono f ∧ range f = s
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)) :=
  StrictMono.comp (Subtype.strictMono_coe fun x ↦ x ∈ s) (OrderIso.strictMono (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 α
⊢ (Subtype.val ∘ ⇑(enum s hs)) a ≤ b

Tactic:
let := WellFoundedLT.toOrderBot α

Goal state after:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
H : StrictMono (Subtype.val ∘ ⇑(enum s hs)) :=
  StrictMono.comp (Subtype.strictMono_coe fun x ↦ x ∈ s) (OrderIso.strictMono (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 α := WellFoundedLT.toOrderBot α
⊢ (Subtype.val ∘ ⇑(enum s hs)) a ≤ b
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α✝ : Type u
β✝ : Type v
γ : Type w
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a : Ordinal.{v}
b : Ordinal.{max u v}
α : Type v
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type (max u v)
s : β → β → Prop
x✝ : IsWellOrder β s
h : Nonempty (s ≺i r)
⊢ type s ∈ range ⇑(RelEmbedding.ofMonotone lift.{u, v} liftInitialSeg._proof_1)

Tactic:
obtain ⟨f⟩ := h

Goal state after:
α✝ : Type u
β✝ : Type v
γ : Type w
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t : γ → γ → Prop
a : Ordinal.{v}
b : Ordinal.{max u v}
α : Type v
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type (max u v)
s : β → β → Prop
x✝ : IsWellOrder β s
f : s ≺i r
⊢ type s ∈ range ⇑(RelEmbedding.ofMonotone lift.{u, v} liftInitialSeg._proof_1)
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}
⊢ ⨆ a, f ↑a ⋯ = o.bsup f

Tactic:
bsup,

Goal state after:
o : Ordinal.{u_3}
f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_4 u_3}
⊢ ⨆ a, f ↑a ⋯ = iSup (o.familyOfBFamily f)
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: o : Ordinal.{u_1}
a : (succ o).ToType
⊢ a ≤ (enum fun x1 x2 ↦ x1 < x2) ⟨o, ⋯⟩

Tactic:
rw [← enum_typein (α := (succ o).ToType) (· < ·) a, enum_le_enum', Subtype.mk_le_mk,
    ← lt_succ_iff]
  apply typein_lt_self

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

Goal state before:
pp: case inl
b : Ordinal.{u_4}
hb : IsSuccLimit b
⊢ IsSuccPrelimit (0 * b)

Tactic:
rw [zero_mul]
    exact isSuccPrelimit_zero

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

Goal state before:
pp: case mpr
c : Cardinal.{u_1}
o : Ordinal.{u_1}
α β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : (#α).ord = type r
h : #α ≤ (type s).card
⊢ (#α).ord ≤ type s

Tactic:
obtain ⟨f⟩ := h

Goal state after:
case mpr
c : Cardinal.{u_1}
o : Ordinal.{u_1}
α β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
r : α → α → Prop
w✝ : IsWellOrder α r
e : (#α).ord = type r
f : α ↪ { α := β, r := s, wo := x✝ }.α
⊢ (#α).ord ≤ type s
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: case a
o o' : Ordinal.{max u v}
f : (a : Ordinal.{max u v}) → a < o → Ordinal.{max u v w}
hf : ∀ {i j : Ordinal.{max u v}} (hi : i < o) (hj : j < o), i ≤ j → f i hi ≤ f j hj
g : (a : Ordinal.{max u v}) → a < o' → Ordinal.{max u v}
hg : o'.blsub g = o
i : Ordinal.{max u v}
hi✝ : i < o
hi : ∃ i_1, ∃ (hi : i_1 < o'), i ≤ g i_1 hi
⊢ f i hi✝ ≤ o'.bsup fun a ha ↦ f (g a ha) ⋯

Tactic:
rcases hi with ⟨j, hj, hj'⟩

Goal state after:
case a
o o' : Ordinal.{max u v}
f : (a : Ordinal.{max u v}) → a < o → Ordinal.{max u v w}
hf : ∀ {i j : Ordinal.{max u v}} (hi : i < o) (hj : j < o), i ≤ j → f i hi ≤ f j hj
g : (a : Ordinal.{max u v}) → a < o' → Ordinal.{max u v}
hg : o'.blsub g = o
i : Ordinal.{max u v}
hi : i < o
j : Ordinal.{max u v}
hj : j < o'
hj' : i ≤ g j hj
⊢ f i hi ≤ o'.bsup fun a ha ↦ f (g a ha) ⋯
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u_1}
ι : Sort u_2
f : ι → Ordinal.{u_1}
⊢ o * ⨆ i, f i = ⨆ i, o * f i

Tactic:
← sSup_range,

Goal state after:
o : Ordinal.{u_1}
ι : Sort u_2
f : ι → Ordinal.{u_1}
⊢ o * sSup (range fun i ↦ f i) = ⨆ i, o * f i
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: n : ℕ
⊢ n.log2 = log 2 n

Tactic:
by
  rcases eq_or_ne n 0 with rfl | hn
  · rw [log2_zero, log_zero_right]
  apply eq_of_forall_le_iff
  intro m
  rw [Nat.le_log2 hn, Nat.le_log_iff_pow_le Nat.one_lt_two hn]

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

Goal state before:
pp: case inr.inl.inl
o : Ordinal.{u_1}
ho : o ≠ 0
hbo : o < 0
hb : 0 ≤ 1
⊢ log 0 o = 0

Tactic:
exact log_zero_left o

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
ho : IsPrincipal op o
n : ℕ
⊢ (op a)^[n] a < o

Tactic:
induction n with
  | zero => rwa [Function.iterate_zero]
  | succ n hn =>
    rw [Function.iterate_succ']
    exact ho hao hn

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

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
a : Ordinal.{u}
⊢ (∃ y, deriv f y = a) ↔ f a ≤ a

Tactic:
le_iff_deriv H

Goal state after:
f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
a : Ordinal.{u}
⊢ (∃ y, deriv f y = a) ↔ ∃ o, deriv f o = a
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case zero
a o : Ordinal.{u}
ho : IsPrincipal (fun x1 x2 ↦ x1 + x2) o
ha : a < o
⊢ a * ↑0 < o

Tactic:
simpa using ha.pos

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₁' : 0 < b
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) (a * b)

Tactic:
← one_le_iff_pos

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
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) (a * b)
Module: Mathlib.SetTheory.Cardinal.Aleph

Goal state before:
pp: ⊢ cof Cardinal.{u} = univ.{u, u + 1}

Tactic:
by
  simpa using preAleph.cof_congr.symm

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

Goal state before:
pp: case type
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
⊢ Cardinal.lift.{v, u} (typeLT α).cof = (lift.{v, u} (typeLT α)).cof

Tactic:
cof_type,

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

Goal state before:
pp: case type
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
⊢ Cardinal.lift.{v, u} (Order.cof α) = (typeLT ULift.{v, u} α).cof

Tactic:
cof_type,

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

Goal state before:
pp: case type
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
⊢ (typeLT α).cof = 1 ↔ typeLT α ∈ range succ

Tactic:
cof_type,

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set α
hs : IsCofinal s
hs' : typeLT ↑s = (Order.cof α).ord
⊢ (typeLT ↑s).cof = Order.cof α

Tactic:
cof_type,

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set α
hs : IsCofinal s
hs' : typeLT ↑s = (Order.cof α).ord
⊢ Order.cof ↑s = Order.cof α
Module: Mathlib.SetTheory.Cardinal.Arithmetic

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

Tactic:
rcases le_or_gt ℵ₀ b with hb | hb
    · rw [add_comm, add_eq_max hb, max_comm]
      exact le_max_left _ _
    · exact le_max_of_le_right (add_lt_aleph0 ha hb).le

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

Goal state before:
pp: case refine_2.inl
o : Ordinal.{u}
ho₂ : o ≤ 2
⊢ IsPrincipal (fun x1 x2 ↦ x1 * x2) o

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

Tactic:
· exact isPrincipal_mul_of_le_two ho₂

Goal state after:
case refine_2.inr
a : Ordinal.{u}
⊢ IsPrincipal (fun x1 x2 ↦ x1 * x2) ((fun x ↦ ω ^ ω ^ x) a)
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
c : Ordinal.{u}
hcb : c ∈ Set.Iio b
hb₁ : 1 < b
⊢ a * ↑⟨c, hcb⟩ ≤ b ^ succ (log b a)

Tactic:
have hbo₀ : b ^ log b a ≠ 0 := pos_iff_ne_zero.1 (opow_pos _ (zero_lt_one.trans hb₁))

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
c : Ordinal.{u}
hcb : c ∈ Set.Iio b
hb₁ : 1 < b
hbo₀ : b ^ log b a ≠ 0
⊢ a * ↑⟨c, hcb⟩ ≤ b ^ succ (log b a)
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

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

Tactic:
cof_type,

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

Goal state before:
pp: a o : Ordinal.{u_1}
f : ↑(Iio a) → ↑(Iio o)
g : Ordinal.{u_1} → Ordinal.{u_1}
hg : IsNormal g
hf : IsFundamentalSeq f
ho : IsSuccLimit o
⊢ a ≤ (g o).cof.ord

Tactic:
cof_map_of_isNormal hg ho,

Goal state after:
a o : Ordinal.{u_1}
f : ↑(Iio a) → ↑(Iio o)
g : Ordinal.{u_1} → Ordinal.{u_1}
hg : IsNormal g
hf : IsFundamentalSeq f
ho : IsSuccLimit o
⊢ a ≤ o.cof.ord
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

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

Tactic:
rw [← Cardinal.lift_lt.{_, u + 1}] at ha

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

Goal state before:
pp: case neg
ι : Type u
f : ι → Cardinal.{v}
c : Cardinal.{v}
h✝ : Nonempty ι
h0 : c ≠ 0
hf : ¬BddAbove (range f)
⊢ (⨆ i, f i) * c = ⨆ i, f i * c

Tactic:
have hfc : ¬ BddAbove (range (f · * c)) := fun bdd ↦ hf
      ⟨⨆ i, f i * c, forall_mem_range.mpr fun i ↦ (le_mul_right h0).trans (le_ciSup bdd i)⟩
    simp [iSup, csSup_of_not_bddAbove, hf, hfc]

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

Goal state before:
pp: o : Ordinal.{u}
⊢ (succ o).IsFundamentalSequence 1 fun x x_1 ↦ o

Tactic:
by
  refine ⟨?_, @fun i j hi hj h => ?_, blsub_const Ordinal.one_ne_zero o⟩
  · rw [cof_succ, ord_one]
  · rw [lt_one_iff_zero] at hi hj
    rw [hi, hj] at h
    exact h.false.elim

Goal state after:
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:
by
  rw [← ord_lt_ord, iSup_ord]
  apply Ordinal.lift_iSup_lt_of_lt_cof <;> simpa

Goal state after: