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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
s : Set (β → γ)
hs : s ∈ h
t : Set β
ht✝ : t ∈ g.seq x
u : Set (α → β)
hu : u ∈ g
v : Set α
hv : v ∈ x
ht : u.seq v ⊆ t
⊢ s.seq (u.seq v) ∈ ((map (fun x1 x2 ↦ x1 ∘ x2) h).seq g).seq x

Tactic:
rw [Set.seq_seq]

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
x : Filter α
g : Filter (α → β)
h : Filter (β → γ)
s : Set (β → γ)
hs : s ∈ h
t : Set β
ht✝ : t ∈ g.seq x
u : Set (α → β)
hu : u ∈ g
v : Set α
hv : v ∈ x
ht : u.seq v ⊆ t
⊢ (((fun x1 x2 ↦ x1 ∘ x2) '' s).seq u).seq v ∈ ((map (fun x1 x2 ↦ x1 ∘ x2) h).seq g).seq x
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: α : Type u_3
inst✝² : Preorder α
inst✝¹ : IsDirectedOrder α
p : α → Prop
inst✝ : Nonempty α
⊢ (∀ (i : α), True → ∃ x ∈ Ici i, p x) ↔ ∀ (a : α), ∃ b, a ≤ b ∧ p b

Tactic:
simp

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

Goal state before:
pp: α : Type u_3
inst✝³ : Preorder α
inst✝² : IsDirectedOrder α
p : α → Prop
inst✝¹ : Nonempty α
inst✝ : NoMaxOrder α
⊢ (∀ (i : α), True → ∃ x ∈ Ioi i, p x) ↔ ∀ (a : α), ∃ b > a, p b

Tactic:
simp

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 : α ≃ β
inst✝² : AddCommMonoid β
inst✝¹ : Module R β
inst✝ : Module.IsTorsionFree R β
this✝¹ : AddCommMonoid α := e.addCommMonoid
this✝ : Module R α := Equiv.module R e
⊢ ∀ (r : R) (m : α), (linearEquiv R e) (r • m) = r • (linearEquiv R e) m

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
⊢ N.FG ↔ ∃ n s, span R (range s) = N

Tactic:
rw [fg_def]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
⊢ (∃ S, S.Finite ∧ span R S = N) ↔ ∃ n s, span R (range s) = N
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
hN : N.FG
n : ℕ
f : Fin n → M
h : span A (range f) = N
x✝ : M
⊢ x✝ ∈ range (f ∘ ULift.down) ↔ x✝ ∈ range f

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹ : AddZeroClass M
inst✝ : DistribSMul S M
r : M → M → Prop
hr : ∀ (s : S) {m m' : M}, r m m' → r (s • m) (s • m')
s : S
x✝¹ x✝ : M
h : (addConGen r).toSetoid x✝¹ x✝
⊢ ∀ (x y : M),
    (DistribSMul.toAddMonoidHom M s) (x + y) = (DistribSMul.toAddMonoidHom M s) x + (DistribSMul.toAddMonoidHom M s) y

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
inst✝¹ : LE α
inst✝ : OrderTop α
⊢ IsCofinal {⊤}

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Cofinal

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
s : Set α
hs : IsCofinal s
⊢ ⋃ i ∈ s, Iio i = univ

Tactic:
eq_univ_iff_forall,

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
s : Set α
hs : IsCofinal s
⊢ ∀ (x : α), x ∈ ⋃ i ∈ s, Iio i
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: α : Type u
inst✝ : Preorder α
c : Cardinal.{max u v}
⊢ (∀ (i : { s // IsCofinal s }), c ≤ lift.{v, u} #↑↑i) ↔ ∀ (s : Set α), IsCofinal s → c ≤ lift.{v, u} #↑s

Tactic:
simp

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

Goal state before:
pp: α : Type u
inst✝ : Preorder α
⊢ cof α ≠ 0 ↔ Nonempty α

Tactic:
simpa using cof_eq_zero_iff.not

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

Goal state before:
pp: α : Type u
inst✝ : Preorder α
⊢ (∃ x, IsTop x) ↔ ¬∀ (x : α), ¬IsTop x

Tactic:
simp

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

Goal state before:
pp: α : Type u
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ (cof α = 0 ∨ ∃ x, IsTop x) ↔ ∃ x, IsTop x

Tactic:
simp

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

Goal state before:
pp: α : Type u
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ (∃ x, IsTop x) ↔ ¬∀ (x : α), ¬IsTop x

Tactic:
simp

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

Goal state before:
pp: α : Type u
inst✝² : LinearOrder α
inst✝¹ : Nonempty α
inst✝ : NoMaxOrder α
⊢ ℵ₀ ≤ cof α

Tactic:
simp

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

Goal state before:
pp: α : Type u
inst✝³ : LinearOrder α
inst✝² : NoMaxOrder α
inst✝¹ : Nonempty α
inst✝ : Countable α
⊢ ℵ₀ ≤ cof α

Tactic:
simp

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

Goal state before:
pp: ⊢ cof ℕ = ℵ₀

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Set (Set α)
h₁ : IsCofinal (⋃₀ s)
h₂ : ∀ x ∈ s, ∃ x_1, ∀ y ∈ x, y < x_1
⊢ cof α ≤ #↑s

Tactic:
choose f hf using h₂

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
s : Set (Set α)
h₁ : IsCofinal (⋃₀ s)
f : (x : Set α) → x ∈ s → α
hf : ∀ (x : Set α) (_ : x ∈ s), ∀ y ∈ x, y < f x _
⊢ cof α ≤ #↑s
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
D : Set (Set α)
inst✝¹ : Preorder α
inst✝ : IsEmpty α
s : Set α
⊢ DirSupClosedOn D s

Tactic:
simp

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
D : Set (Set α)
inst✝¹ : Preorder α
inst✝ : IsEmpty α
s : Set α
⊢ DirSupInaccOn D s

Tactic:
simp

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
D : Set (Set α)
inst✝ : Preorder α
⊢ DirSupClosedOn D ∅

Tactic:
simp

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
D : Set (Set α)
inst✝ : Preorder α
⊢ DirSupInaccOn D ∅

Tactic:
simp

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
D : Set (Set α)
inst✝ : Preorder α
⊢ DirSupClosedOn D Set.univ

Tactic:
simp

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
D : Set (Set α)
inst✝ : Preorder α
⊢ DirSupInaccOn D Set.univ

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
E : Type u_2
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
⊢ {1, -1}.Finite

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
E : Type u_2
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
x : R
hx : 0 ≤ x
⊢ 1 ∈ {1, -1}

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
E : Type u_2
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
inst✝² : IsOrderedRing R
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
x : R
hx : x ≤ 0
⊢ -1 ∈ {1, -1}

Tactic:
simp

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : ConditionallyCompleteLinearOrder β
ι : Sort u_4
inst✝ : Nonempty ι
g : ι → α
hf : IsNormal f
hg : BddAbove (range g)
x✝ : β
⊢ (x✝ ∈ range fun i ↦ f (g i)) ↔ x✝ ∈ f '' range g

Tactic:
simp

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
f : α → α
hf : IsNormal f
⊢ DirSupClosed (range f)

Tactic:
intro s hs hs₀ _ a ha

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
⊢ a ∈ range f
Module: Mathlib.SetTheory.Ordinal.Univ

Goal state before:
pp: case mpr
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝ : IsWellOrder β s
h : lift.{max (u + 1) v, max (u + 1) v} (type s) < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})
f : s ↪r fun x1 x2 ↦ x1 < x2
a : Ordinal.{u}
hf : ∀ (b : Ordinal.{u}), b ∈ Set.range ⇑f ↔ b < a
⊢ liftInitialSeg.toRelEmbedding a = lift.{max (u + 1) v, max (u + 1) v} (type s)

Tactic:
induction a using inductionOn with | type α r

Goal state after:
case mpr.type
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝¹ : IsWellOrder β s
h : lift.{max (u + 1) v, max (u + 1) v} (type s) < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})
f : s ↪r fun x1 x2 ↦ x1 < x2
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
hf : ∀ (b : Ordinal.{u}), b ∈ Set.range ⇑f ↔ b < type r
⊢ liftInitialSeg.toRelEmbedding (type r) = lift.{max (u + 1) v, max (u + 1) v} (type s)
Module: Mathlib.SetTheory.Ordinal.Univ

Goal state before:
pp: ⊢ liftPrincipalSeg.top = typeLT Ordinal.{u}

Tactic:
simp

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

Goal state before:
pp: a : Ordinal.{v}
⊢ lift.{u, v} (a + 1) = lift.{u, v} a + 1

Tactic:
simp

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

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
⊢ type r ≠ 0 ↔ Nonempty α

Tactic:
simp

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

Goal state before:
pp: a b : Ordinal.{u_4}
⊢ a + ↑0 ≤ b + ↑0 ↔ a ≤ b

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
⊢ typeLT ℕ ≤ (cof ℕ).ord

Tactic:
simp

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

Goal state before:
pp: case inr.intro
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : Subsingleton α
h✝ : Nonempty α
val✝ : Unique α
this : BoundedOrder α
⊢ typeLT α ≤ (cof α).ord

Tactic:
simp

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

Goal state before:
pp: α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set α
⊢ ∀ {a b : ↑s}, (Embedding.subtype fun x ↦ x ∈ s) a < (Embedding.subtype fun x ↦ x ∈ s) b ↔ a < b

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: o : Ordinal.{u_4}
⊢ o.pred ≤ o

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ ∀ (b : Ordinal.{?u.26}), b ≤ (succ b).pred

Tactic:
simp

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

Goal state before:
pp: case inl
a : Ordinal.{u_4}
⊢ (succ a).pred = succ a ↔ IsSuccPrelimit (succ a)

Tactic:
simp

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

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

Tactic:
simp

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
⊢ ∀ (a b : { x // x ∈ s }), a < b → ↑a < ↑b

Tactic:
simp

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

Goal state before:
pp: case inl
a : Ordinal.{v}
⊢ lift.{u, v} (succ a).pred = (lift.{u, v} (succ a)).pred

Tactic:
simp

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

Goal state before:
pp: case right
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
H : StrictMono (Subtype.val ∘ ⇑(enum s hs))
⊢ range (Subtype.val ∘ ⇑(enum s hs)) = s

Tactic:
simp

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

Goal state before:
pp: a b c : Ordinal.{u_4}
h : b ≤ a
⊢ c ≤ a - b ↔ b + c ≤ a

Tactic:
by
  rw [← add_le_add_iff_left b, Ordinal.add_sub_cancel_of_le h]

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

Goal state before:
pp: case mpr
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
f : α → α
hf : StrictMono f
hs : IsCofinal (range f)
H : StrictMono (Subtype.val ∘ ⇑(enum (range f) hs))
⊢ range (Subtype.val ∘ ⇑(enum (range f) hs)) = range f

Tactic:
simp

Goal state after:
case mpr
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
f : α → α
hf : StrictMono f
hs : IsCofinal (range f)
H : StrictMono (Subtype.val ∘ ⇑(enum (range f) hs))
⊢ {x | ∃ y, f y = x} = range f
Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
f : α → α
hf : StrictMono f
x : α
⊢ (range fun x ↦ ↑((StrictMono.orderIso f hf) x)) = range f

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
o : Ordinal.{u_3}
ho : o ≠ 0
c : α
⊢ (o.brange fun x x_1 ↦ c) = {c}

Tactic:
← range_familyOfBFamily

Goal state after:
α : Type u_1
o : Ordinal.{u_3}
ho : o ≠ 0
c : α
⊢ range (o.familyOfBFamily fun x x_1 ↦ c) = {c}
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: ι : Type u_3
f : ι → Ordinal.{u}
a : Ordinal.{u}
inst✝ : Small.{u, u_3} ι
⊢ ⨆ i, f i + 1 ≤ a ↔ ∀ (i : ι), f i < a

Tactic:
simp

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

Goal state before:
pp: ι : Type u_3
f : ι → Ordinal.{u}
a : Ordinal.{u}
inst✝ : Small.{u, u_3} ι
⊢ a < ⨆ i, f i + 1 ↔ ∃ i, a ≤ f i

Tactic:
simp

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

Goal state before:
pp: case inl
⊢ (sSup ∅).ord = sSup (ord '' ∅)

Tactic:
simp

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

Goal state before:
pp: case neg
s : Set Cardinal.{u_3}
hn : s.Nonempty
hs : ¬BddAbove s
⊢ (sSup ∅).ord = sSup ∅

Tactic:
simp

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

Goal state before:
pp: o : Ordinal.{u}
⊢ (typein LT.lt).toRelEmbedding o = lift.{u + 1, u} o

Tactic:
by
  nth_rw 2 [← o.type_toType]
  rw [← ToType.mk.toRelIsoLT.ordinal_lift_type_eq, lift_id'.{u, u + 1}, type_Iio_lt]

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

Goal state before:
pp: o : Ordinal.{u}
⊢ typeLT ↑(Iio o) = lift.{u + 1, u} o

Tactic:
simp

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ ∀ (a b : Ordinal.{v}), a < b → lift.{u, v} a < lift.{u, v} b

Tactic:
simp

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
o₁ o₂ o₃ : Ordinal.{u}
x✝² x✝¹ x✝ : WellOrder
⊢ ∀ {a b : (x✝².α ⊕ x✝¹.α) ⊕ x✝.α},
    Sum.Lex x✝².r (Sum.Lex x✝¹.r x✝.r) ((sumAssoc x✝².α x✝¹.α x✝.α) a) ((sumAssoc x✝².α x✝¹.α x✝.α) b) ↔
      Sum.Lex (Sum.Lex x✝².r x✝¹.r) x✝.r a b

Tactic:
simp

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ (o + 1).card = o.card + 1

Tactic:
simp

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

Goal state before:
pp: case zero
⊢ (↑0).card = ↑0

Tactic:
simp

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ (succ o).card = o.card + 1

Tactic:
simp

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ 0 ∈ Iio (typeLT ToType 1)

Tactic:
simp

Goal state after:
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
b' : β
a' : α
h : Prod.Lex s r (b', a') (b, a)
e : b = b'
⊢ r a' a

Tactic:
by grind [asymm_of s]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
x : ToType 1
⊢ 0 ∈ Iio (typeLT ToType 1)

Tactic:
simp

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

Goal state before:
pp: s : Set Ordinal.{u}
⊢ sInf (s ∩ {b | ∀ c < 0, enumOrd s c < b}) = sInf s

Tactic:
simp

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

Goal state before:
pp: o : Ordinal.{u_1}
x y : o.ToType
⊢ (typein fun x1 x2 ↦ x1 < x2).toRelEmbedding x ≤ (typein fun x1 x2 ↦ x1 < x2).toRelEmbedding y ↔ x ≤ y

Tactic:
simp

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

Goal state before:
pp: a b c : Ordinal.{u_4}
h : IsSuccLimit c
⊢ a < b * c ↔ ∃ c' < c, a < b * c'

Tactic:
by
  simpa using (mul_le_iff_of_isSuccLimit h).not

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

Goal state before:
pp: case inl
a c : Ordinal.{u_4}
⊢ a < 0 * (c + 1) ↔ ∃ d < 0, a ≤ 0 * c + d

Tactic:
simp

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

Goal state before:
pp: o : Ordinal.{u_3}
⊢ (fun b ↦ b < (typein fun x1 x2 ↦ x1 < x2).top) = fun x ↦ x ≤ o

Tactic:
simp

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

Goal state before:
pp: n : ℕ
IH : ↑n ≤ (↑n).ord
⊢ (↑n).ord < (↑(n + 1)).ord

Tactic:
simp

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

Goal state before:
pp: a : Cardinal.{u_1}
ha : IsSuccLimit a
⊢ a.ord ∈ lowerBounds (upperBounds (ord '' Iio a))

Tactic:
lowerBounds,

Goal state after:
a : Cardinal.{u_1}
ha : IsSuccLimit a
⊢ a.ord ∈ {x | ∀ ⦃a_1 : Ordinal.{u_1}⦄, a_1 ∈ upperBounds (ord '' Iio a) → x ≤ a_1}
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case zero
a b : Ordinal.{u_4}
ba : b + a = a
⊢ (a + b) * (0 + 1) = a * (0 + 1) + b

Tactic:
simp

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

Goal state before:
pp: c : Cardinal.{u_1}
⊢ #c.ord.ToType = c

Tactic:
simp

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

Goal state before:
pp: a : Ordinal.{u_4}
⊢ sSup ((fun x ↦ 0 * x) ⁻¹' Iic a) = 0

Tactic:
simp

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

Goal state before:
pp: a : Ordinal.{u_4}
ha : a ≠ 0
b c : Ordinal.{u_4}
⊢ 0 ∈ (fun x ↦ a * x) ⁻¹' Iic c

Tactic:
simp

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

Goal state before:
pp: case inl
a c : Ordinal.{u_4}
h : a ≤ 0 * c
⊢ a / 0 ≤ c

Tactic:
simp

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

Goal state before:
pp: o : Ordinal.{u_1}
n : ℕ
hc : ↑n < ℵ₀
⊢ o ≤ (↑n).ord ↔ o.card ≤ ↑n

Tactic:
simp

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

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
f : (a : Ordinal.{u}) → a < type r → Ordinal.{max u v}
o : Ordinal.{max u v}
⊢ (type r).blsub f ≤ o ↔ (lsub fun a ↦ f ((typein r).toRelEmbedding a) ⋯) ≤ o

Tactic:
rw [blsub_le_iff, lsub_le_iff]

Goal state after:
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
f : (a : Ordinal.{u}) → a < type r → Ordinal.{max u v}
o : Ordinal.{max u v}
⊢ (∀ (i : Ordinal.{u}) (h : i < type r), f i h < o) ↔ ∀ (i : α), f ((typein r).toRelEmbedding i) ⋯ < o
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b n : ℕ
⊢ 0 < log b n ↔ b ≤ n ∧ 1 < b

Tactic:
rw [Nat.pos_iff_ne_zero, Ne, log_eq_zero_iff, not_or, not_lt, not_le]

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

Goal state before:
pp: n : ℕ
⊢ typeLT Fin n = ↑n

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case zero
b n : ℕ
h : 1 < b
hn : b ≤ n
⊢ log b n < 0 ↔ log b (n / b) + 1 < 0

Tactic:
simp

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

Goal state before:
pp: case inl
b c : Ordinal.{u_4}
⊢ 0 * (b - c) = 0 * b - 0 * c

Tactic:
simp

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

Goal state before:
pp: case zero
⊢ 1 ^ 0 = 1

Tactic:
simp

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

Goal state before:
pp: a b : Ordinal.{u_1}
a0 : 0 < a
⊢ 0 < a ^ 0

Tactic:
simp

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

Goal state before:
pp: case inl
⊢ 0 % 0 = 0

Tactic:
simp

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

Goal state before:
pp: case inl
c : Ordinal.{u_4}
⊢ 0 * c % 0 = 0

Tactic:
simp

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

Goal state before:
pp: case inl
y z : Ordinal.{u_4}
⊢ (0 * y + z) % 0 = z % 0

Tactic:
simp

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

Goal state before:
pp: case inl
y z : Ordinal.{u_4}
⊢ 0 * y % (0 * z) = 0 * (y % z)

Tactic:
simp

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

Goal state before:
pp: case refine_1.inl.inr
b : Ordinal.{u_1}
⊢ 1 ^ b ≤ 1

Tactic:
simp

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

Goal state before:
pp: case refine_1.inr
a : Ordinal.{u_1}
⊢ a ^ 0 ≤ 1

Tactic:
simp

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

Goal state before:
pp: case inl
o : Ordinal.{u_1}
⊢ o * sSup ∅ = sSup ((fun x ↦ o * x) '' ∅)

Tactic:
simp

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

Goal state before:
pp: case inl
a c : Ordinal.{u_4}
⊢ a < 0 * c ↔ ∃ q < c, ∃ r < 0, a = 0 * q + r

Tactic:
simp

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

Goal state before:
pp: case neg
o : Ordinal.{u_1}
s : Set Ordinal.{u_1}
hs : s.Nonempty
ho : 0 < o
bdd : ¬BddAbove s
⊢ o * ⊥ = sSup ∅

Tactic:
simp

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

Goal state before:
pp: case neg.zero
a b : Ordinal.{u_1}
ab : a ≤ b
ha : ¬a = 0
⊢ a ^ 0 ≤ b ^ 0

Tactic:
simp

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

Goal state before:
pp: m : ℕ
⊢ ↑(m * 0) = ↑m * ↑0

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inl
b k : ℕ
⊢ log (b ^ k) 0 = log b 0 / k

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inr.inl
b n : ℕ
hn : n ≠ 0
⊢ log (b ^ 0) n = log b n / 0

Tactic:
simp

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

Goal state before:
pp: case inl
m : ℕ
⊢ ↑(m / 0) = ↑m / ↑0

Tactic:
simp

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

Goal state before:
pp: case inl.inl
b : Ordinal.{u_1}
⊢ 0 ^ (b + 0) = 0 ^ b * 0 ^ 0

Tactic:
simp

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

Goal state before:
pp: case inr.inl
b c : Ordinal.{u_1}
ha : 0 < 1
⊢ 1 ^ (b + c) = 1 ^ b * 1 ^ c

Tactic:
simp

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

Goal state before:
pp: case inr.inr.zero
a b : Ordinal.{u_1}
ha : 0 < a
ha' : 1 < a
⊢ a ^ (b + 0) = a ^ b * a ^ 0

Tactic:
simp

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

Goal state before:
pp: ⊢ lift.{u, v} ↑0 = ↑0

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
n : ℕ
x : Fin n
⊢ ↑↑x ∈ Iio (type LT.lt)

Tactic:
simp

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

Goal state before:
pp: case inl
a c : Ordinal.{u_1}
⊢ a ^ (0 * c) = (a ^ 0) ^ c

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
x : ℕ
⊢ ↑x ∈ Iio (type LT.lt)

Tactic:
simp

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

Goal state before:
pp: case inr
o : Ordinal.{u_4}
ho : ω ≤ o
⊢ (∃ n, o = ↑n) ∨ ω ≤ o

Tactic:
· exact Or.inr ho

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

Goal state before:
pp: case inr.inr.inl
b c : Ordinal.{u_1}
hb : 0 < b
ha : 1 ≠ 0
⊢ 1 ^ (b * c) = (1 ^ b) ^ c

Tactic:
simp

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

Goal state before:
pp: case inr.inr.inr.zero
a b : Ordinal.{u_1}
hb : 0 < b
ha : a ≠ 0
ha' : 1 < a
⊢ a ^ (b * 0) = (a ^ b) ^ 0

Tactic:
simp

Goal state after: