mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: A₁ : Type u_6
B₁ : Type u_7
A₂ : Type u_8
B₂ : Type u_9
inst✝⁶ : CommSemiring A₁
inst✝⁵ : CommSemiring B₁
inst✝⁴ : CommSemiring A₂
inst✝³ : Semiring B₂
inst✝² : Algebra A₁ B₁
inst✝¹ : Algebra A₂ B₂
e₁ : A₁ ≃+* A₂
e₂ : B₁ ≃+* B₂
he : (algebraMap A₂ B₂).comp ↑e₁ = (↑e₂).comp (algebraMap A₁ B₁)
inst✝ : Module.Finite A₁ B₁
this✝¹ : Algebra A₁ A₂ := e₁.toRingHom.toAlgebra
this✝ : Algebra A₂ B₁ := ((algebraMap A₁ B₁).comp e₁.symm.toRingHom).toAlgebra
this : IsScalarTower A₁ A₂ B₁
r : A₂
⊢ e₂.toFun ((algebraMap A₂ B₁) r) = (algebraMap A₂ B₂) r

Tactic:
simpa using

Goal state after:
A₁ : Type u_6
B₁ : Type u_7
A₂ : Type u_8
B₂ : Type u_9
inst✝⁶ : CommSemiring A₁
inst✝⁵ : CommSemiring B₁
inst✝⁴ : CommSemiring A₂
inst✝³ : Semiring B₂
inst✝² : Algebra A₁ B₁
inst✝¹ : Algebra A₂ B₂
e₁ : A₁ ≃+* A₂
e₂ : B₁ ≃+* B₂
he : (algebraMap A₂ B₂).comp ↑e₁ = (↑e₂).comp (algebraMap A₁ B₁)
inst✝ : Module.Finite A₁ B₁
this✝¹ : Algebra A₁ A₂ := e₁.toRingHom.toAlgebra
this✝ : Algebra A₂ B₁ := ((algebraMap A₁ B₁).comp e₁.symm.toRingHom).toAlgebra
this : IsScalarTower A₁ A₂ B₁
r : A₂
⊢ e₂ ((algebraMap A₁ B₁) (e₁.symm r)) = (algebraMap A₂ B₂) r
Module: Mathlib.Order.DirSupClosed

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

Tactic:
simpa using

Goal state after:
α : Type u_1
s t : Set α
inst✝ : Preorder α
hs : DirSupClosed s
ht : DirSupClosed t
⊢ DirSupClosed (s ∪ t)
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s t : Set α
inst✝ : Preorder α
hs : DirSupInacc s
ht : DirSupInacc t
⊢ DirSupInacc (s ∩ t)

Tactic:
simpa using

Goal state after:
α : Type u_1
s t : Set α
inst✝ : Preorder α
hs : DirSupInacc s
ht : DirSupInacc t
⊢ DirSupInacc (s ∩ t)
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
g : B →+* C
f : A →+* B
hg : g.Finite
hf : f.Finite
⊢ (g.comp f).Finite

Tactic:
algebraize [f, g, g.comp f]
  exact .trans B C

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

Goal state before:
pp: case inl
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
⊢ x ∈ Submodule.span R≥0 {1, -1}

Tactic:
simpa using

Goal state after:
case inl
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
⊢ x ∈ Submodule.span R≥0 {1, -1}
Module: Mathlib.Order.DirSupClosed

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

Tactic:
simpa using

Goal state after:
α : Type u_1
s : Set α
inst✝ : Preorder α
⊢ DirSupInacc s ↔
    ∀ ⦃d : Set α⦄,
      d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ∃ b ∈ d, Ici b ∩ d ⊆ s
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Preorder α
hs : DirSupInacc s
a b : α
h : AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) a b
⊢ a ∈ s ↔ b ∈ s

Tactic:
simpa using

Goal state after:
α : Type u_1
s : Set α
inst✝ : Preorder α
hs : DirSupInacc s
a b : α
h : AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) a b
⊢ a ∈ s ↔ b ∈ s
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: case inr
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
⊢ x ∈ Submodule.span R≥0 {1, -1}

Tactic:
simpa using

Goal state after:
case inr
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
⊢ x ∈ Submodule.span R≥0 {1, -1}
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : Preorder α
inst✝⁵ : Preorder β
inst✝⁴ : Preorder γ
inst✝³ : SMul α β
inst✝² : SMul α γ
f : β → γ
inst✝¹ : Zero α
inst✝ : PosSMulReflectLE α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
smul : ∀ (a : α) (b : β), f (a • b) = a • f b
a : α
ha : 0 < a
b₁ b₂ : β
h : a • b₁ ≤ a • b₂
⊢ a • f b₁ ≤ a • f b₂

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : Preorder α
inst✝⁵ : Preorder β
inst✝⁴ : Preorder γ
inst✝³ : SMul α β
inst✝² : SMul α γ
f : β → γ
inst✝¹ : Zero α
inst✝ : PosSMulReflectLE α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
smul : ∀ (a : α) (b : β), f (a • b) = a • f b
a : α
ha : 0 < a
b₁ b₂ : β
h : a • b₁ ≤ a • b₂
⊢ a • f b₁ ≤ a • f b₂
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
b : β
⊢ f a ≤ b ↔ ∀ a' < a, f a' ≤ b

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
b : β
⊢ f a ≤ b ↔ ∀ a' < a, f a' ≤ b
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
b : β
⊢ b < f a ↔ ∃ a' < a, b < f a'

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
b : β
⊢ b < f a ↔ ∃ a' < a, b < f a'
Module: Mathlib.Order.IsNormal

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
hf : IsNormal f
s : Set α
hs : IsLUB s a
hs' : s.Nonempty
⊢ f a ∈ upperBounds (f '' s)

Tactic:
simpa using

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
hf : IsNormal f
s : Set α
hs : IsLUB s a
hs' : s.Nonempty
⊢ ∀ a_1 ∈ s, a_1 ≤ a
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
inst✝ : LinearOrder γ
hg : IsNormal g
hf : IsNormal f
a✝ : α
ha : IsSuccLimit a✝
b : γ
hb : ∀ ⦃x : α⦄, x ∈ Iio a✝ → g (f x) ≤ b
⊢ (g ∘ f) a✝ ≤ b

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
inst✝² : LinearOrder α
inst✝¹ : LinearOrder β
inst✝ : LinearOrder γ
hg : IsNormal g
hf : IsNormal f
a✝ : α
ha : IsSuccLimit a✝
b : γ
hb : ∀ ⦃x : α⦄, x ∈ Iio a✝ → g (f x) ≤ b
⊢ ∀ (a' : β), ∀ x < a✝, a' < f x → g a' ≤ b
Module: Mathlib.SetTheory.Ordinal.Univ

Goal state before:
pp: ⊢ ℵ₀ < univ.{u, v}

Tactic:
simpa using

Goal state after:
⊢ ℵ₀ < univ.{u, v}
Module: Mathlib.SetTheory.Ordinal.Univ

Goal state before:
pp: o : Ordinal.{max (u + 1) v}
h : o < Ordinal.univ.{u, v}
⊢ ?m.25 < Ordinal.liftPrincipalSeg.top

Tactic:
simpa using

Goal state after:
o : Ordinal.{max (u + 1) v}
h : o < Ordinal.univ.{u, v}
⊢ ?m.25 < Ordinal.univ.{?u.12, ?u.11}
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ✝ → γ✝ → Prop
c a✝ b : Ordinal.{u}
α : Type u
r : α → α → Prop
x✝³ : IsWellOrder α r
β : Type u
s : β → β → Prop
x✝² : IsWellOrder β s
γ : Type u
t : γ → γ → Prop
x✝¹ : IsWellOrder γ t
x✝ : type t + type r ≤ type t + type s
f : InitialSeg (Sum.Lex t r) (Sum.Lex t s)
a : γ
⊢ f (Sum.inl a) = Sum.inl a

Tactic:
simpa using

Goal state after:
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ✝ → γ✝ → Prop
c a✝ b : Ordinal.{u}
α : Type u
r : α → α → Prop
x✝³ : IsWellOrder α r
β : Type u
s : β → β → Prop
x✝² : IsWellOrder β s
γ : Type u
t : γ → γ → Prop
x✝¹ : IsWellOrder γ t
x✝ : type t + type r ≤ type t + type s
f : InitialSeg (Sum.Lex t r) (Sum.Lex t s)
a : γ
⊢ f (Sum.inl a) = Sum.inl a
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b c : Ordinal.{u_4}
h : (fun x ↦ a + x) b = (fun x ↦ a + x) c
⊢ b = c

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b c : Ordinal.{u_4}
h : (fun x ↦ a + x) b = (fun x ↦ a + x) c
⊢ b ≤ c ∧ c ≤ b
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b : Ordinal.{u_4}
n : ℕ
⊢ a + ↑(n + 1) ≤ b + ↑(n + 1) ↔ a ≤ b

Tactic:
simpa using

Goal state after:
a b : Ordinal.{u_4}
n : ℕ
⊢ a + ↑n ≤ b + ↑n ↔ a ≤ b
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: o : Ordinal.{u_4}
h : IsSuccLimit o
n : ℕ
⊢ ↑n < o

Tactic:
simpa using

Goal state after:
o : Ordinal.{u_4}
h : IsSuccLimit o
n : ℕ
⊢ ↑n < o
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: o : Ordinal.{u_4}
⊢ o = 0 ∨ o ∈ range succ ∨ IsSuccLimit o

Tactic:
simpa using

Goal state after:
o : Ordinal.{u_4}
⊢ o = 0 ∨ (∃ y, y + 1 = o) ∨ IsSuccLimit o
Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
inst✝² : WellFoundedLT α
inst✝¹ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
inst✝ : SuccOrder α
a o : α
ha : o ∈ s
H : ↑((enum s hs) a) < o
b : α
hb : b < succ a
⊢ ↑((enum s hs) b) ≤ ↑((enum s hs) a)

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : WellFoundedLT α
inst✝¹ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
inst✝ : SuccOrder α
a o : α
ha : o ∈ s
H : ↑((enum s hs) a) < o
b : α
hb : b < succ a
⊢ b ≤ a
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b : Ordinal.{u_4}
⊢ a + b - a = b

Tactic:
simpa using

Goal state after:
a b : Ordinal.{u_4}
⊢ a + b - a = b
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inr
a b : Ordinal.{u_4}
h : a < b
⊢ a ≤ b + (a - b)

Tactic:
simpa using

Goal state after:
case inr
a b : Ordinal.{u_4}
h : a < b
⊢ a ≤ b
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a : Ordinal.{u_4}
⊢ a - 0 = a

Tactic:
simpa using

Goal state after:
a : Ordinal.{u_4}
⊢ a - 0 = a
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a : Ordinal.{u_4}
⊢ 0 - a = 0

Tactic:
simpa using

Goal state after:
a : Ordinal.{u_4}
⊢ 0 - a = 0
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a : Ordinal.{u_4}
⊢ a - a = 0

Tactic:
simpa using

Goal state after:
a : Ordinal.{u_4}
⊢ a - a = 0
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b : Ordinal.{u_4}
⊢ a - b ≠ 0 ↔ b < a

Tactic:
simpa using

Goal state after:
a b : Ordinal.{u_4}
⊢ ¬a - b = 0 ↔ b < a
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b c : Ordinal.{u_4}
hb : b ≠ 0
⊢ a + b ≤ c ↔ ∀ d < b, a + d < c

Tactic:
simpa using

Goal state after:
a b c : Ordinal.{u_4}
hb : b ≠ 0
⊢ a + b ≤ c ↔ ∀ d < b, a + d < c
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))
he : IsNormal (Subtype.val ∘ ⇑(enum s hs))
⊢ DirSupClosed s

Tactic:
simpa using

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))
he : IsNormal (Subtype.val ∘ ⇑(enum s hs))
⊢ DirSupClosed s
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b c : Ordinal.{u_4}
hb : IsSuccLimit b
⊢ a + b ≤ c ↔ ∀ d < b, a + d ≤ c

Tactic:
simpa using

Goal state after:
a b c : Ordinal.{u_4}
hb : IsSuccLimit b
⊢ a + b ≤ c ↔ ∀ d < b, a + d ≤ c
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: s : Set Ordinal.{u}
inst✝ : Small.{u, u + 1} ↑s
a : Cardinal.{u}
ha : a ∈ upperBounds (succ ∘ card '' s)
b : Ordinal.{u}
hb : b ∈ s
⊢ b < a.ord

Tactic:
simpa using

Goal state after:
s : Set Ordinal.{u}
inst✝ : Small.{u, u + 1} ↑s
a : Cardinal.{u}
ha : a ∈ upperBounds (succ ∘ card '' s)
b : Ordinal.{u}
hb : b ∈ s
⊢ b.card < a
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: s : Set Ordinal.{u}
hf : BddAbove s
f : Ordinal.{u} → Ordinal.{max u v}
⊢ BddAbove (f '' s)

Tactic:
by
  rw [bddAbove_iff_small] at hf ⊢
  exact small_lift _

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

Goal state before:
pp: case h
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
H : StrictMono (Subtype.val ∘ ⇑(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
⊢ ↑((enum s hs) a) ∈ upperBounds (Subtype.val ∘ ⇑(enum s hs) '' Iio a)

Tactic:
simpa using

Goal state after:
case h
α : 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
⊢ ∀ a_1 < a, a_1 ≤ a
Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum

Goal state before:
pp: case refine_2
α : 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 α
this : ConditionallyCompleteLinearOrderBot α := WellFoundedLT.conditionallyCompleteLinearOrderBot α
⊢ (Subtype.val ∘ ⇑(enum s hs) '' Iio a).Nonempty

Tactic:
simpa using

Goal state after:
case refine_2
α : 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 α
this : ConditionallyCompleteLinearOrderBot α := WellFoundedLT.conditionallyCompleteLinearOrderBot α
⊢ ¬a = ⊥
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal.{u_1}
⊢ a ≤ b + a

Tactic:
simpa using

Goal state after:
α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal.{u_1}
⊢ a ≤ b + a
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal.{u_1}
⊢ a ≤ a + b

Tactic:
simpa using

Goal state after:
α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : Ordinal.{u_1}
⊢ a ≤ a + b
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case refine_1
a b : Ordinal.{u_1}
α : Type u_1
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
f : Sum.Lex r emptyRelation ≼i s
h : Surjective ⇑((InitialSeg.leAdd r emptyRelation).trans f)
⊢ False

Tactic:
simpa using

Goal state after:
case refine_1
a b : Ordinal.{u_1}
α : Type u_1
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
f : Sum.Lex r emptyRelation ≼i s
h : Surjective ⇑((InitialSeg.leAdd r emptyRelation).trans f)
⊢ False
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: a b : Ordinal.{u_1}
α : Type u_1
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
f : r ≺i s
⊢ ∀ (a b : α ⊕ PUnit.{u_1 + 1}),
    Sum.Lex r emptyRelation a b →
      s (Sum.recOn a ⇑f.toRelEmbedding fun x ↦ f.top) (Sum.recOn b ⇑f.toRelEmbedding fun x ↦ f.top)

Tactic:
simpa using

Goal state after:
a b : Ordinal.{u_1}
α : Type u_1
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
f : r ≺i s
⊢ ∀ (a : α), s (f.toRelEmbedding a) f.top
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
a : Ordinal.{max u v}
⊢ a < o.bsup f ↔ ∃ i, ∃ (hi : i < o), a < f i hi

Tactic:
simpa using

Goal state after:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
a : Ordinal.{max u v}
⊢ a < o.bsup f ↔ ∃ i, ∃ (hi : i < o), a < f i hi
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
a : Ordinal.{max u v}
⊢ a < o.bsup f ↔ ∃ i, ∃ (hi : i < o), a < f i hi

Tactic:
by
  simpa only [not_forall, not_le] using not_congr (@bsup_le_iff.{_, v} _ f a)

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

Goal state before:
pp: case mp.refine_2
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
a : Ordinal.{u}
ha : succ a = typeLT α
b : α
⊢ (typein fun x1 x2 ↦ x1 < x2).toRelEmbedding b < typeLT α

Tactic:
exact typein_lt_type ..

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

Goal state before:
pp: ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
a : Ordinal.{max u_3 u_4}
⊢ a < lsub f ↔ ∃ i, a ≤ f i

Tactic:
simpa using

Goal state after:
ι : Type u_3
f : ι → Ordinal.{max u_4 u_3}
a : Ordinal.{max u_3 u_4}
⊢ a < lsub f ↔ ∃ i, a ≤ f i
Module: Mathlib.SetTheory.Ordinal.Arithmetic

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

Tactic:
simpa using

Goal state after:
case refine_1
a : Ordinal.{u_4}
h : 0 < a
b : Ordinal.{u_4}
⊢ 0 < a
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case refine_2
a : Ordinal.{u_4}
h : 0 < a
a✝ : Ordinal.{u_4}
hb : IsSuccLimit a✝
⊢ IsLUB ((fun x ↦ a * x) '' Iio a✝) (a * a✝)

Tactic:
simpa using

Goal state after:
case refine_2
a : Ordinal.{u_4}
h : 0 < a
a✝ : Ordinal.{u_4}
hb : IsSuccLimit a✝
⊢ ∀ a_1 < a✝, a * a_1 ≤ a * a✝
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:
simpa using

Goal state after:
a b c : Ordinal.{u_4}
h : IsSuccLimit c
⊢ a < b * c ↔ ∃ c' < c, a < b * c'
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u}
h✝ : lsub ⇑(typein fun x1 x2 ↦ x1 < x2).toRelEmbedding < o
h : lsub ⇑(typein fun x1 x2 ↦ x1 < x2).toRelEmbedding < typeLT o.ToType
⊢ False

Tactic:
simpa using

Goal state after:
o : Ordinal.{u}
h✝ : lsub ⇑(typein fun x1 x2 ↦ x1 < x2).toRelEmbedding < o
h : lsub ⇑(typein fun x1 x2 ↦ x1 < x2).toRelEmbedding < typeLT o.ToType
⊢ False
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u}
ho : IsSuccPrelimit o
⊢ sSup {b | b < (typein fun x1 x2 ↦ x1 < x2).top} = o

Tactic:
simpa using

Goal state after:
o : Ordinal.{u}
ho : IsSuccPrelimit o
⊢ sSup (Iio o) = o
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v}
a : Ordinal.{max u v}
⊢ a < o.blsub f ↔ ∃ i, ∃ (hi : i < o), a ≤ f i hi

Tactic:
simpa using

Goal state after:
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v}
a : Ordinal.{max u v}
⊢ a < o.blsub f ↔ ∃ i, ∃ (hi : i < o), a ≤ f i hi
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: ⊢ ord 1 = 1

Tactic:
simpa using

Goal state after:
⊢ ord 1 = 1
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: a : Cardinal.{u_1}
ha : IsSuccLimit a
b : Ordinal.{u_1}
H : ∀ ⦃x : Cardinal.{u_1}⦄, x ∈ Iio a → x ≤ b.card
c : Cardinal.{u_1}
hc : c < a
⊢ c < b.card

Tactic:
simpa using

Goal state after:
a : Cardinal.{u_1}
ha : IsSuccLimit a
b : Ordinal.{u_1}
H : ∀ ⦃x : Cardinal.{u_1}⦄, x ∈ Iio a → x ≤ b.card
c : Cardinal.{u_1}
hc : c < a
⊢ c < b.card
Module: Mathlib.SetTheory.Ordinal.Basic

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

Tactic:
by
    intro a ha
    simp_rw [lowerBounds, upperBounds, mem_ofPred, forall_mem_image, ord_le]
    refine fun b H ↦ le_of_forall_lt fun c hc ↦ ?_
    simpa using H (ha.succ_lt hc)

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

Goal state before:
pp: c : Cardinal.{u_1}
i : c.ord.ToType
⊢ #↑(Iio i) < c

Tactic:
simpa using

Goal state after:
c : Cardinal.{u_1}
i : c.ord.ToType
⊢ #↑(Iio i) < c
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b : Ordinal.{u_4}
h : b ≠ 0
⊢ a < b * (a / b) + b

Tactic:
simpa using

Goal state after:
a b : Ordinal.{u_4}
h : b ≠ 0
⊢ a < b * (a / b) + b
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: o : Ordinal.{u_1}
⊢ 1 ≤ o.card ↔ 1 ≤ o

Tactic:
simpa using

Goal state after:
o : Ordinal.{u_1}
⊢ 1 ≤ o.card ↔ 1 ≤ o
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: o : Ordinal.{u_1}
⊢ 0 < o.card ↔ 0 < o

Tactic:
simpa using

Goal state after:
o : Ordinal.{u_1}
⊢ 0 < o.card ↔ 0 < o
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: o : Ordinal.{u_1}
⊢ 1 < o.card ↔ 1 < o

Tactic:
simpa using

Goal state after:
o : Ordinal.{u_1}
⊢ 1 < o.card ↔ 1 < o
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: o : Ordinal.{u_1}
⊢ o.card ≤ 1 ↔ o ≤ 1

Tactic:
simpa using

Goal state after:
o : Ordinal.{u_1}
⊢ o.card ≤ 1 ↔ o ≤ 1
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: o : Ordinal.{u_1}
⊢ o.card = 0 ↔ o = 0

Tactic:
simpa using

Goal state after:
o : Ordinal.{u_1}
⊢ o.card = 0 ↔ o = 0
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: o : Ordinal.{u_1}
⊢ o.card = 1 ↔ o = 1

Tactic:
simpa using

Goal state after:
o : Ordinal.{u_1}
⊢ o.card = 1 ↔ o = 1
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝¹ : IsWellOrder α r
inst✝ : Fintype α
⊢ type r = ↑(Fintype.card α)

Tactic:
← card_eq_nat,

Goal state after:
α : Type u
r : α → α → Prop
inst✝¹ : IsWellOrder α r
inst✝ : Fintype α
⊢ (type r).card = ↑(Fintype.card α)
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}
H : ∀ (i : α), f ((typein r).toRelEmbedding i) ⋯ < o
i : Ordinal.{u}
h : i < type r
⊢ f i h < o

Tactic:
simpa using

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}
H : ∀ (i : α), f ((typein r).toRelEmbedding i) ⋯ < o
i : Ordinal.{u}
h : i < type r
⊢ f i h < o
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a b : Ordinal.{u_4}
b0 : b ≠ 0
⊢ b * a / b = a

Tactic:
simpa using

Goal state after:
a b : Ordinal.{u_4}
b0 : b ≠ 0
⊢ b * a / b = a
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a : Ordinal.{u_4}
⊢ a / 1 = a

Tactic:
simpa using

Goal state after:
a : Ordinal.{u_4}
⊢ a / 1 = a
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a : Ordinal.{u_4}
h : a ≠ 0
⊢ a / a = 1

Tactic:
simpa using

Goal state after:
a : Ordinal.{u_4}
h : a ≠ 0
⊢ a / a = 1