mathlib-initiative/mathlib-tactics huggingface dataset:
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))^[m + 1] 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))^[m + 1 + 1] K
Module: Mathlib.Algebra.Module.Submodule.IterateMapComap

Goal state before:
pp: case 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
m : ℕ
heq : f.iterateMapComap i m K = f.iterateMapComap i (m + 1) K
hf : Surjective ⇑f
hi : Injective ⇑i
n : ℕ
ih : f.iterateMapComap i n K = f.iterateMapComap i (n + 1) K
⊢ (fun K ↦ comap f (map i K))^[n + 1] K = (fun K ↦ comap f (map i K))^[n + 1 + 1] K

Tactic:
iterate_succ',

Goal state after:
case 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
m : ℕ
heq : f.iterateMapComap i m K = f.iterateMapComap i (m + 1) K
hf : Surjective ⇑f
hi : Injective ⇑i
n : ℕ
ih : f.iterateMapComap i n K = f.iterateMapComap i (n + 1) K
⊢ ((fun K ↦ comap f (map i K)) ∘ (fun K ↦ comap f (map i K))^[n]) K = (fun K ↦ comap f (map i K))^[n + 1 + 1] K
Module: Mathlib.Algebra.Module.Submodule.IterateMapComap

Goal state before:
pp: case 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
m : ℕ
heq : f.iterateMapComap i m K = f.iterateMapComap i (m + 1) K
hf : Surjective ⇑f
hi : Injective ⇑i
n : ℕ
ih : f.iterateMapComap i n K = f.iterateMapComap i (n + 1) K
⊢ ((fun K ↦ comap f (map i K)) ∘ (fun K ↦ comap f (map i K))^[n]) K = (fun K ↦ comap f (map i K))^[n + 1 + 1] K

Tactic:
iterate_succ',

Goal state after:
case 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
m : ℕ
heq : f.iterateMapComap i m K = f.iterateMapComap i (m + 1) K
hf : Surjective ⇑f
hi : Injective ⇑i
n : ℕ
ih : f.iterateMapComap i n K = f.iterateMapComap i (n + 1) K
⊢ ((fun K ↦ comap f (map i K)) ∘ (fun K ↦ comap f (map i K))^[n]) K =
    ((fun K ↦ comap f (map i K)) ∘ (fun K ↦ comap f (map i K))^[n + 1]) K
Module: Mathlib.Order.Filter.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
f g : Filter α
s t : Set α
p : Set α → Prop
he : p ∅
hmono : ∀ (t : Set α), p t → ∀ (s : Set α), s ⊆ t → p s
hunion : ∀ (s : Set α), p s → ∀ (t : Set α), p t → p (s ∪ t)
⊢ univ ∈ {t | p tᶜ}

Tactic:
simpa

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: case inr.h.e_a.e_v
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : P × M →ₗ[R] M
inj : Injective ⇑f
n : ℕ
ih :
  ∀ m < n,
    ∀ ⦃x y : ℕ →₀ P⦄,
      let s := x.support ∪ y.support;
      ∀ (ne : s.Nonempty), m = s.max' ne → f.prodOfFinsuppNat x = f.prodOfFinsuppNat y → x = y
x y : ℕ →₀ P
s : Finset ℕ := x.support ∪ y.support
ne✝ : s.Nonempty
hn : n = s.max' ne✝
eq : f.prodOfFinsuppNat x = f.prodOfFinsuppNat y
ne : ¬(comapDomain.addMonoidHom ⋯) x = (comapDomain.addMonoidHom ⋯) y
⊢ False

Tactic:
apply ne (ih _ _ _ rfl (inj _))

Goal state after:
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : P × M →ₗ[R] M
inj : Injective ⇑f
n : ℕ
ih :
  ∀ m < n,
    ∀ ⦃x y : ℕ →₀ P⦄,
      let s := x.support ∪ y.support;
      ∀ (ne : s.Nonempty), m = s.max' ne → f.prodOfFinsuppNat x = f.prodOfFinsuppNat y → x = y
x y : ℕ →₀ P
s : Finset ℕ := ⋯
ne✝ : s.Nonempty
hn : n = s.max' ne✝
eq : f.prodOfFinsuppNat x = f.prodOfFinsuppNat y
ne : ¬(comapDomain.addMonoidHom ⋯) x = (comapDomain.addMonoidHom ⋯) y
⊢ (((comapDomain.addMonoidHom ⋯) x).support ∪ ((comapDomain.addMonoidHom ⋯) y).support).Nonempty

R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : P × M →ₗ[R] M
inj : Injective ⇑f
n : ℕ
ih :
  ∀ m < n,
    ∀ ⦃x y : ℕ →₀ P⦄,
      let s := x.support ∪ y.support;
      ∀ (ne : s.Nonempty), m = s.max' ne → f.prodOfFinsuppNat x = f.prodOfFinsuppNat y → x = y
x y : ℕ →₀ P
s : Finset ℕ := ⋯
ne✝ : s.Nonempty
hn : n = s.max' ne✝
eq : f.prodOfFinsuppNat x = f.prodOfFinsuppNat y
ne : ¬(comapDomain.addMonoidHom ⋯) x = (comapDomain.addMonoidHom ⋯) y
⊢ (((comapDomain.addMonoidHom ⋯) x).support ∪ ((comapDomain.addMonoidHom ⋯) y).support).max' ?m.151 < n

R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
f : P × M →ₗ[R] M
inj : Injective ⇑f
n : ℕ
ih :
  ∀ m < n,
    ∀ ⦃x y : ℕ →₀ P⦄,
      let s := x.support ∪ y.support;
      ∀ (ne : s.Nonempty), m = s.max' ne → f.prodOfFinsuppNat x = f.prodOfFinsuppNat y → x = y
x y : ℕ →₀ P
s : Finset ℕ := ⋯
ne✝ : s.Nonempty
hn : n = s.max' ne✝
eq : f.prodOfFinsuppNat x = f.prodOfFinsuppNat y
ne : ¬(comapDomain.addMonoidHom ⋯) x = (comapDomain.addMonoidHom ⋯) y
⊢ f (f.prodOfFinsuppNat ((comapDomain.addMonoidHom ⋯) x)) = f (f.prodOfFinsuppNat ((comapDomain.addMonoidHom ⋯) y))
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
hf : f.ker = ⊥
I : Type u_6
⊢ (mapRange.linearMap f).range = submodule fun x ↦ f.range

Tactic:
ext x
  constructor
  · rintro ⟨y, hy⟩
    simp [← hy]
  · intro hx
    choose y hy using hx
    refine ⟨⟨x.support, y, fun i => ?_⟩, by ext; simp_all⟩
    constructor
    <;> contrapose
    <;> simp_all +contextual [← hy, map_zero, LinearMap.ker_eq_bot'.1 hf]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
δ : Type u_1
ι : Sort x
f✝ g : Filter α
s t : Set α
f : Filter α
⊢ ⊤ \ f = ￢f

Tactic:
by
    ext s
    simp only [mem_sdiff_iff_union, Filter.hnot_def, mem_principal, compl_subset_iff_union,
      mem_top_iff_forall, eq_univ_iff_forall, ker, mem_union, mem_sInter, Filter.mem_sets]
    grind

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

Goal state before:
pp: case a
α : Type u_1
β : Type u_2
f : α → β
F : Filter α
G : Filter β
⊢ map f (F ⊓ comap f G) ≤ map f F ⊓ G

Tactic:
calc
      map f (F ⊓ comap f G) ≤ map f F ⊓ (map f <| comap f G) := map_inf_le
      _ ≤ map f F ⊓ G := inf_le_inf_left (map f F) map_comap_le

Goal state after:
Module: Mathlib.Algebra.Group.TransferInstance

Goal state before:
pp: M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : MulOneClass β
one : One α := e.one
mul : Mul α := e.mul
⊢ MulOneClass α

Tactic:
apply e.injective.mulOneClass _

Goal state after:
case one
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : MulOneClass β
one : One α := ⋯
mul : Mul α := ⋯
⊢ e 1 = 1

case mul
M : Type u_1
α : Type u_2
β : Type u_3
e : α ≃ β
inst✝ : MulOneClass β
one : One α := ⋯
mul : Mul α := ⋯
⊢ ∀ (x y : α), e (x * y) = e x * e y
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
⊢ ∀ (r s : R) (x : α), (r + s) • x = r • x + s • x

Tactic:
simp [add_def, smul_def, add_smul]

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

Goal state before:
pp: A : Type u
inst✝² : Semiring A
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module A M
N : Submodule A M
G : Type w
w✝ : Finite G
g : G → M
hg : span A (range g) = N
this : Fintype ↑(range g)
⊢ span A ↑(range g).toFinset = N

Tactic:
simpa

Goal state after:
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set α
t : Set ↑s
hs : IsCofinal s
ht : IsCofinal t
⊢ IsCofinal (range Subtype.val)

Tactic:
simpa

Goal state after:
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
s : Set α
hs : IsCofinal s
⊢ ∀ (x : α), x ∈ ⋃ i ∈ s, Iio i

Tactic:
mem_iUnion,

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
s : Set α
hs : IsCofinal s
⊢ ∀ (x : α), ∃ i, ∃ (_ : i ∈ s), x ∈ Iio i
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMulZeroClass α β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : PosSMulReflectLE α β
h : 0 ≤ a • b
ha : 0 < a
⊢ a • 0 ≤ a • b

Tactic:
simpa

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMulZeroClass α β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : PosSMulReflectLE α β
h : a • b ≤ 0
ha : 0 < a
⊢ a • b ≤ a • 0

Tactic:
simpa

Goal state after:
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Set α
h : ¬IsCofinal s
⊢ BddAbove s

Tactic:
exact .of_not_isCofinal h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMulWithZero α β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : SMulPosReflectLE α β
h : 0 ≤ a • b
hb : 0 < b
⊢ 0 • b ≤ a • b

Tactic:
simpa

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMulWithZero α β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : SMulPosReflectLE α β
h : a • b ≤ 0
hb : 0 < b
⊢ a • b ≤ 0 • b

Tactic:
simpa

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁸ : Zero α
inst✝⁷ : Zero β
inst✝⁶ : SMulWithZero α β
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : MulOneClass β
inst✝² : PosMulMono β
inst✝¹ : MulPosMono β
inst✝ : IsScalarTower α β β
h : Monotone fun x ↦ x • 1
x✝² : α
ha : 0 ≤ x✝²
x✝¹ x✝ : β
hb : x✝¹ ≤ x✝
this : x✝² • 1 * x✝¹ ≤ x✝² • 1 * x✝
⊢ x✝² • x✝¹ ≤ x✝² • x✝

Tactic:
simpa

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

Goal state before:
pp: α : Type u
inst✝ : LinearOrder α
s : Set α
hs : IsCofinal s
⊢ IsCofinal (range Subtype.val)

Tactic:
simpa

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

Goal state before:
pp: α : Type u
inst✝ : LinearOrder α
h : cof α < ℵ₀
s : Set α
hs : IsCofinal s
hs' : #↑s = cof α
hf : s.Finite
t : Set α
ht : t.Subsingleton
ht' : IsCofinal t
⊢ #↑t ≤ 1

Tactic:
simpa

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
D : Set (Set α)
inst✝ : Preorder α
ι : Sort u_2
f : ι → Set α
hs : ∀ (i : ι), DirSupClosedOn D (f i)
⊢ ∀ x ∈ range f, DirSupClosedOn D x

Tactic:
simpa

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
ι : Sort u_2
f : ι → Set α
hs : ∀ (i : ι), DirSupClosed (f i)
⊢ ∀ x ∈ range f, DirSupClosed x

Tactic:
simpa

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
D : Set (Set α)
inst✝ : Preorder α
ι : Sort u_2
f : ι → Set α
hs : ∀ (i : ι), DirSupInaccOn D (f i)
⊢ ∀ x ∈ range f, DirSupInaccOn D x

Tactic:
simpa

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
ι : Sort u_2
f : ι → Set α
hs : ∀ (i : ι), DirSupInacc (f i)
⊢ ∀ x ∈ range f, DirSupInacc x

Tactic:
simpa

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_7
P : Type u_6
inst✝² : Semiring S
inst✝¹ : AddCommMonoid P
inst✝ : Module S P
σ : R →+* S
f : M →ₛₗ[σ] P
hf : Surjective ⇑f
s : Set M
hsfin : s.Finite
hs : span R s = ⊤
p : P
x✝ : p ∈ ⊤
⊢ p ∈ ⇑f '' ↑(span R s)

Tactic:
simpa [hs] using hf p

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Preorder α
h :
  ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ∃ b ∈ d, Ici b ∩ d ⊆ s
⊢ ∀ ⦃d : Set α⦄,
    d ∈ Set.univ →
      d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ∃ b ∈ d, Ici b ∩ d ⊆ s

Tactic:
simpa

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : ConditionallyCompleteLinearOrder β
hf : IsNormal f
x : β
h₁ : (f ⁻¹' Iic x).Nonempty
h₂ : BddAbove (f ⁻¹' Iic x)
hy : sSup (f ⁻¹' Iic x) ∈ Iic (sSup (f ⁻¹' Iic x))
⊢ (f '' f ⁻¹' Iic x).Nonempty

Tactic:
simpa

Goal state after:
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)
  rw [lift_lift, lift_univ, univ_umax.{u, v}] at this
  exact this

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

Goal state before:
pp: c : Cardinal.{u + 1}
h : c < univ.{u, u + 1}
this : c.ord < Ordinal.univ.{u, u + 1}
⊢ ?m.46 < Ordinal.liftPrincipalSeg.top

Tactic:
simpa

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

Goal state before:
pp: case inl
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : Subsingleton α
h✝ : IsEmpty α
⊢ typeLT α ≤ (cof α).ord

Tactic:
simpa

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

Goal state before:
pp: case ind
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
t : Set α
h : s ⊆ t
x : α
IH : ∀ y < x, ↑((enum t ⋯) y) ≤ ↑((enum s hs) y)
⊢ ↑((enum t ⋯) x) ≤ ↑((enum s hs) x)

Tactic:
exact enum_le_of_forall_lt (h (Subtype.prop _)) fun y hy ↦
    (IH y hy).trans_lt ((enum s hs).strictMono hy)

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

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

Tactic:
lt_add_one_iff

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

Goal state before:
pp: ι : Sort u_3
f : ι → Ordinal.{u}
a : Ordinal.{u}
h : ∀ (i : ι), f i < a
⊢ ∀ (i : ι), f i + 1 ≤ a

Tactic:
simpa

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

Goal state before:
pp: case refine_3
α : 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 < a, (Subtype.val ∘ ⇑(enum s hs)) b ≤ b✝
bdd : BddAbove (Subtype.val ∘ ⇑(enum s hs) '' Iio a)
this✝¹ : Nonempty α
this✝ : OrderBot α := WellFoundedLT.toOrderBot α
this : ConditionallyCompleteLinearOrderBot α := WellFoundedLT.conditionallyCompleteLinearOrderBot α
b : α
hb : b < a
⊢ ↑((enum s hs) b) < sSup (Subtype.val ∘ ⇑(enum s hs) '' Iio a)

Tactic:
obtain ⟨c, hca, hbc⟩ := ha.lt_iff_exists_lt.1 hb

Goal state after:
case refine_3
α : 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 < a, (Subtype.val ∘ ⇑(enum s hs)) b ≤ b✝
bdd : BddAbove (Subtype.val ∘ ⇑(enum s hs) '' Iio a)
this✝¹ : Nonempty α
this✝ : OrderBot α := WellFoundedLT.toOrderBot α
this : ConditionallyCompleteLinearOrderBot α := WellFoundedLT.conditionallyCompleteLinearOrderBot α
b : α
hb : b < a
c : α
hca : c < a
hbc : b < c
⊢ ↑((enum s hs) b) < sSup (Subtype.val ∘ ⇑(enum s hs) '' Iio a)
Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum

Goal state before:
pp: case refine_3
α : 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 < a, (Subtype.val ∘ ⇑(enum s hs)) b ≤ b✝
bdd : BddAbove (Subtype.val ∘ ⇑(enum s hs) '' Iio a)
this✝¹ : Nonempty α
this✝ : OrderBot α := WellFoundedLT.toOrderBot α
this : ConditionallyCompleteLinearOrderBot α := WellFoundedLT.conditionallyCompleteLinearOrderBot α
b : α
hb : b < a
c : α
hca : c < a
hbc : b < c
⊢ c ∈ Iio a ∧ (Subtype.val ∘ ⇑(enum s hs)) c = (Subtype.val ∘ ⇑(enum s hs)) c

Tactic:
simpa

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

Goal state before:
pp: o : Ordinal.{u_1}
c : Cardinal.{u_1}
ho : o ≤ c.ord
⊢ o.card ≤ c.ord.card

Tactic:
exact Ordinal.card_le_card ho

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

Goal state before:
pp: o : Ordinal.{u_1}
c : Cardinal.{u_1}
ho : o ≤ c.ord
⊢ o.card ≤ c

Tactic:
by
  rw [← card_ord c]; exact Ordinal.card_le_card ho

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

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

Tactic:
simpa

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

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

Tactic:
intro i hi

Goal state after:
case cons.nil
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
o : Ordinal.{u}
a : α
as : List α
hl : (a :: as).SortedGT
hlt : ∀ i ∈ a :: as, (Ordinal.typein fun x1 x2 ↦ x1 < x2).toRelEmbedding i < o
hm : [].SortedGT
hmltl : Lex (fun x1 x2 ↦ x1 < x2) [] (a :: as)
i : α
hi : i ∈ []
⊢ (Ordinal.typein fun x1 x2 ↦ x1 < x2).toRelEmbedding i < o
Module: Mathlib.SetTheory.Ordinal.Basic

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

Tactic:
intro i hi

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

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

Tactic:
simpa

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

Goal state before:
pp: case inl
a : Ordinal.{u_4}
h : IsSuccLimit a
⊢ IsSuccLimit 0 ∨ 0 = 0 ∧ IsSuccLimit a ↔ IsSuccPrelimit 0

Tactic:
simpa

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

Goal state before:
pp: case inl.inl
x : Ordinal.{u_1}
hx : 1 ≤ x
hb : 0 ≤ 1
⊢ 0 ^ log 0 x ≤ x

Tactic:
simpa

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

Goal state before:
pp: case inl.inr
x : Ordinal.{u_1}
hx : 1 ≤ x
hb : 1 ≤ 1
⊢ 1 ^ log 1 x ≤ x

Tactic:
simpa

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

Goal state before:
pp: case right.refine_2
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
ha : a ∈ ⋂ i, fixedPoints (f i)
⊢ ∃ a_1, derivFamily f a_1 = a

Tactic:
rw [Set.mem_iInter] at ha

Goal state after:
case right.refine_2
ι : Type u_1
f : ι → Ordinal.{u} → Ordinal.{u}
inst✝ : Small.{u, u_1} ι
H : ∀ (i : ι), IsNormal (f i)
a : Ordinal.{u}
ha : ∀ (i : ι), a ∈ fixedPoints (f i)
⊢ ∃ a_1, derivFamily f a_1 = a
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: op : Ordinal.{u_2} → Ordinal.{u_2} → Ordinal.{u_2}
ι : Sort u_1
f : ι → Ordinal.{u_2}
H : ∀ (i : ι), IsPrincipal op (f i)
⊢ ∀ x ∈ Set.range fun i ↦ f i, IsPrincipal op x

Tactic:
simpa

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

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

Tactic:
intro ⟨a, ha, ⟨n, hn⟩⟩

Goal state after:
case mpr
a✝ b : Ordinal.{u_1}
hb : b ≠ 0
a : Ordinal.{u_1}
ha : a < b
n : ℕ
hn : a✝ < ω ^ (ω ^ a * ↑n)
⊢ ∃ c, (∃ c_1 < b, ∃ n, c < ω ^ c_1 * ↑n) ∧ ∃ n, a✝ < ω ^ c * ↑n
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case mpr.refine_2
a✝ b : Ordinal.{u_1}
hb : b ≠ 0
a : Ordinal.{u_1}
ha : a < b
n : ℕ
hn : a✝ < ω ^ (ω ^ a * ↑n)
⊢ a✝ < ω ^ (ω ^ a * ↑n) * ↑1

Tactic:
simpa

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

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

Tactic:
← this

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

Goal state before:
pp: case inr
a b : Ordinal.{u_1}
hab : a * b = b
ha : 0 < a
hb : ¬b = 0
⊢ nfp (fun x ↦ a * x) 1 ≤ b

Tactic:
← Ne,

Goal state after:
case inr
a b : Ordinal.{u_1}
hab : a * b = b
ha : 0 < a
hb : b ≠ 0
⊢ nfp (fun x ↦ a * x) 1 ≤ b
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case mp
o : Ordinal.{u}
H : IsPrincipal (fun x1 x2 ↦ x1 + x2) o
ho : ¬o = 0
n : ℕ
hn : o < ω ^ log ω o * ↑n
⊢ ¬ω ^ log ω o < o

Tactic:
exact fun h ↦ hn.not_gt <| H.mul_natCast_lt h n

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

Goal state before:
pp: o : Ordinal.{u_1}
l : IsSuccPrelimit o
c : Cardinal.{u_1}
ho : o ≠ 0
⊢ ¬IsMin o

Tactic:
simpa

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

Goal state before:
pp: o : Ordinal.{u_1}
ho : IsSuccPrelimit o
h : o ≠ 0
⊢ ¬IsMin o

Tactic:
simpa

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

Goal state before:
pp: case isSuccPrelimit.mp
o : Ordinal.{u_1}
ho : IsSuccPrelimit o
IH : ∀ b < o, lift.{v, u_1} (preBeth b) = preBeth (Ordinal.lift.{v, u_1} b)
i : Ordinal.{u_1}
hi : i ∈ Iio o
⊢ Ordinal.lift.{v, u_1} i ∈ Iio (Ordinal.lift.{v, u_1} o)

Tactic:
simpa

Goal state after: