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

Goal state before:
pp: α : Type u_1
inst✝ : LE α
⊢ IsCofinal ∅ ↔ IsEmpty α

Tactic:
refine ⟨fun h ↦ ⟨fun a ↦ ?_⟩, fun h ↦ .of_isEmpty⟩
  simpa using h a

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
a : α
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α ≤i β
⊢ IsSuccPrelimit (f a) → IsSuccPrelimit a

pp: case mpr
α : Type u_1
β : Type u_2
a : α
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α ≤i β
⊢ IsSuccPrelimit a → IsSuccPrelimit (f a)

Tactic:
<;>

Goal state after:
case mp
α : Type u_1
β : Type u_2
a : α
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α ≤i β
⊢ IsSuccPrelimit (f a) → IsSuccPrelimit a

case mpr
α : Type u_1
β : Type u_2
a : α
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α ≤i β
⊢ IsSuccPrelimit a → IsSuccPrelimit (f a)
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
⊢ lift.{v, u} (cof α) ≤ lift.{u, v} (cof β)

pp: case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
⊢ lift.{u, v} (cof β) ≤ lift.{v, u} (cof α)

Tactic:
<;>

Goal state after:
case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
⊢ lift.{v, u} (cof α) ≤ lift.{u, v} (cof β)

case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
⊢ lift.{u, v} (cof β) ≤ lift.{v, u} (cof α)
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
⊢ ∀ (s : Set β), IsCofinal s → lift.{v, u} (cof α) ≤ lift.{u, v} #↑s

pp: case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
⊢ ∀ (s : Set α), IsCofinal s → lift.{u, v} (cof β) ≤ lift.{v, u} #↑s

Tactic:
<;>

Goal state after:
case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
⊢ ∀ (s : Set β), IsCofinal s → lift.{v, u} (cof α) ≤ lift.{u, v} #↑s

case a
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : StrictMono f
hf' : IsCofinal (range f)
⊢ ∀ (s : Set α), IsCofinal s → lift.{u, v} (cof β) ≤ lift.{v, u} #↑s
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: case refine_2
A : Type u_5
M : Type u_6
inst✝⁶ : Semiring A
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module A M
S : Submodule A M
R : Type u_7
inst✝³ : Semiring R
inst✝² : Module R M
inst✝¹ : SMul R A
inst✝ : IsScalarTower R A M
s : Finset M
e : span R ↑s = restrictScalars R S
⊢ restrictScalars R S ≤ restrictScalars R (span A ↑s)

Tactic:
rw [← e]
    exact span_le_restrictScalars ..

Goal state after:
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 hs.dirSupInaccOn.union ht.dirSupInaccOn (D := .univ)

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: case a
α : Type u_1
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : WellFoundedLT α
f : α → α
a : α
hf : IsNormal f
hf' : BddAbove (range fun n ↦ f^[n] a)
⊢ ⨆ i, f (f^[i] a) ≤ ⨆ n, f^[n] a

pp: case a
α : Type u_1
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : WellFoundedLT α
f : α → α
a : α
hf : IsNormal f
hf' : BddAbove (range fun n ↦ f^[n] a)
⊢ ⨆ n, f^[n] a ≤ ⨆ i, f (f^[i] a)

Tactic:
<;>

Goal state after:
case a
α : Type u_1
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : WellFoundedLT α
f : α → α
a : α
hf : IsNormal f
hf' : BddAbove (range fun n ↦ f^[n] a)
⊢ ⨆ i, f (f^[i] a) ≤ ⨆ n, f^[n] a

case a
α : Type u_1
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : WellFoundedLT α
f : α → α
a : α
hf : IsNormal f
hf' : BddAbove (range fun n ↦ f^[n] a)
⊢ ⨆ n, f^[n] a ≤ ⨆ i, f (f^[i] a)
Module: Mathlib.SetTheory.Ordinal.Univ

Goal state before:
pp: case mp
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝ : IsWellOrder β s
⊢ type s ∈ Set.range ⇑liftInitialSeg.toRelEmbedding → type s < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})

pp: case mpr
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝ : IsWellOrder β s
⊢ type s < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u}) → type s ∈ Set.range ⇑liftInitialSeg.toRelEmbedding

Tactic:
<;>

Goal state after:
case mp
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝ : IsWellOrder β s
⊢ type s ∈ Set.range ⇑liftInitialSeg.toRelEmbedding → type s < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})

case mpr
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝ : IsWellOrder β s
⊢ type s < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u}) → type s ∈ Set.range ⇑liftInitialSeg.toRelEmbedding
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case mp
a b c : Ordinal.{u_4}
hc : IsSuccLimit c
⊢ (∃ d < c, a ≤ b + d) → ∃ d < c, a < b + d

pp: case mpr
a b c : Ordinal.{u_4}
hc : IsSuccLimit c
⊢ (∃ d < c, a < b + d) → ∃ d < c, a ≤ b + d

Tactic:
<;>

Goal state after:
case mp
a b c : Ordinal.{u_4}
hc : IsSuccLimit c
⊢ (∃ d < c, a ≤ b + d) → ∃ d < c, a < b + d

case mpr
a b c : Ordinal.{u_4}
hc : IsSuccLimit c
⊢ (∃ d < c, a < b + d) → ∃ d < c, a ≤ b + d
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case mp
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
⊢ lift.{max v w, u} (type r) ≤ lift.{max u w, v} (type s) → Nonempty (r ≼i s)

pp: case mpr
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
⊢ Nonempty (r ≼i s) → lift.{max v w, u} (type r) ≤ lift.{max u w, v} (type s)

Tactic:
<;>

Goal state after:
case mp
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
⊢ lift.{max v w, u} (type r) ≤ lift.{max u w, v} (type s) → Nonempty (r ≼i s)

case mpr
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
⊢ Nonempty (r ≼i s) → lift.{max v w, u} (type r) ≤ lift.{max u w, v} (type s)
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case refine_1
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
⊢ isEquivalent
      { α := ULift.{max v w, u} { α := α, r := r, wo := inst✝¹ }.α,
        r := ULift.down ⁻¹'o { α := α, r := r, wo := inst✝¹ }.r, wo := ⋯ }
      { α := ULift.{max u w, v} { α := β, r := s, wo := inst✝ }.α,
        r := ULift.down ⁻¹'o { α := β, r := s, wo := inst✝ }.r, wo := ⋯ } →
    Nonempty (r ≃r s)

pp: case refine_2
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
⊢ Nonempty (r ≃r s) →
    isEquivalent
      { α := ULift.{max v w, u} { α := α, r := r, wo := inst✝¹ }.α,
        r := ULift.down ⁻¹'o { α := α, r := r, wo := inst✝¹ }.r, wo := ⋯ }
      { α := ULift.{max u w, v} { α := β, r := s, wo := inst✝ }.α,
        r := ULift.down ⁻¹'o { α := β, r := s, wo := inst✝ }.r, wo := ⋯ }

Tactic:
<;>

Goal state after:
case refine_1
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
⊢ isEquivalent
      { α := ULift.{max v w, u} { α := α, r := r, wo := inst✝¹ }.α,
        r := ULift.down ⁻¹'o { α := α, r := r, wo := inst✝¹ }.r, wo := ⋯ }
      { α := ULift.{max u w, v} { α := β, r := s, wo := inst✝ }.α,
        r := ULift.down ⁻¹'o { α := β, r := s, wo := inst✝ }.r, wo := ⋯ } →
    Nonempty (r ≃r s)

case refine_2
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
⊢ Nonempty (r ≃r s) →
    isEquivalent
      { α := ULift.{max v w, u} { α := α, r := r, wo := inst✝¹ }.α,
        r := ULift.down ⁻¹'o { α := α, r := r, wo := inst✝¹ }.r, wo := ⋯ }
      { α := ULift.{max u w, v} { α := β, r := s, wo := inst✝ }.α,
        r := ULift.down ⁻¹'o { α := β, r := s, wo := inst✝ }.r, wo := ⋯ }
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case mp
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
⊢ lift.{max v w, u} (type r) < lift.{max u w, v} (type s) → Nonempty (r ≺i s)

pp: case mpr
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
⊢ Nonempty (r ≺i s) → lift.{max v w, u} (type r) < lift.{max u w, v} (type s)

Tactic:
<;>

Goal state after:
case mp
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
⊢ lift.{max v w, u} (type r) < lift.{max u w, v} (type s) → Nonempty (r ≺i s)

case mpr
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
⊢ Nonempty (r ≺i s) → lift.{max v w, u} (type r) < lift.{max u w, v} (type s)
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: case mp
s : Set Ordinal.{u_3}
⊢ BddAbove ((fun x ↦ x + 1) '' s) → BddAbove s

pp: case mpr
s : Set Ordinal.{u_3}
⊢ BddAbove s → BddAbove ((fun x ↦ x + 1) '' s)

Tactic:
<;>

Goal state after:
case mp
s : Set Ordinal.{u_3}
⊢ BddAbove ((fun x ↦ x + 1) '' s) → BddAbove s

case mpr
s : Set Ordinal.{u_3}
⊢ BddAbove s → BddAbove ((fun x ↦ x + 1) '' s)
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 * succ ((typein s).toRelEmbedding b) ≤ c
⊢ (typein (Prod.Lex s r)).toRelEmbedding (b, a) < c

Tactic:
rw [mul_succ] at this

Goal state after:
α β : 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
⊢ (typein (Prod.Lex s r)).toRelEmbedding (b, a) < c
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
⊢ type r + 1 ≤ type s → type r < type s

pp: case refine_2
a b : Ordinal.{u_1}
α : Type u_1
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
⊢ type r < type s → type r + 1 ≤ type s

Tactic:
<;>

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
⊢ type r + 1 ≤ type s → type r < type s

case refine_2
a b : Ordinal.{u_1}
α : Type u_1
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
⊢ type r < type s → type r + 1 ≤ type s
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u_3}
f : (a : Ordinal.{u_3}) → a < o → Ordinal.{max u_3 u_4}
⊢ sSup (o.brange f) = o.bsup f

Tactic:
congr
  rw [range_familyOfBFamily]

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

Goal state before:
pp: f : Ordinal.{max u_3 u_4} → Ordinal.{max u_4 u_5}
H : IsNormal f
o : Ordinal.{u_4}
α : Type u_4
r : α → α → Prop
x✝ : IsWellOrder α r
g : (a : Ordinal.{u_4}) → a < type r → Ordinal.{max u_4 u_3}
h : type r ≠ 0
this : Nonempty α
⊢ ⨆ i, f (familyOfBFamily' r ?ho✝ g i) = iSup (familyOfBFamily' r ?ho fun a h ↦ f (g a h))

pp: case ho
f : Ordinal.{max u_3 u_4} → Ordinal.{max u_4 u_5}
H : IsNormal f
o : Ordinal.{u_4}
α : Type u_4
r : α → α → Prop
x✝ : IsWellOrder α r
g : (a : Ordinal.{u_4}) → a < type r → Ordinal.{max u_4 u_3}
h : type r ≠ 0
this : Nonempty α
⊢ type r = type r

pp: case ho
f : Ordinal.{max u_3 u_4} → Ordinal.{max u_4 u_5}
H : IsNormal f
o : Ordinal.{u_4}
α : Type u_4
r : α → α → Prop
x✝ : IsWellOrder α r
g : (a : Ordinal.{u_4}) → a < type r → Ordinal.{max u_4 u_3}
h : type r ≠ 0
this : Nonempty α
⊢ type r = type r

Tactic:
<;>

Goal state after:
f : Ordinal.{max u_3 u_4} → Ordinal.{max u_4 u_5}
H : IsNormal f
o : Ordinal.{u_4}
α : Type u_4
r : α → α → Prop
x✝ : IsWellOrder α r
g : (a : Ordinal.{u_4}) → a < type r → Ordinal.{max u_4 u_3}
h : type r ≠ 0
this : Nonempty α
⊢ ⨆ i, f (familyOfBFamily' r ?ho✝ g i) = iSup (familyOfBFamily' r ?ho fun a h ↦ f (g a h))

case ho
f : Ordinal.{max u_3 u_4} → Ordinal.{max u_4 u_5}
H : IsNormal f
o : Ordinal.{u_4}
α : Type u_4
r : α → α → Prop
x✝ : IsWellOrder α r
g : (a : Ordinal.{u_4}) → a < type r → Ordinal.{max u_4 u_3}
h : type r ≠ 0
this : Nonempty α
⊢ type r = type r

case ho
f : Ordinal.{max u_3 u_4} → Ordinal.{max u_4 u_5}
H : IsNormal f
o : Ordinal.{u_4}
α : Type u_4
r : α → α → Prop
x✝ : IsWellOrder α r
g : (a : Ordinal.{u_4}) → a < type r → Ordinal.{max u_4 u_3}
h : type r ≠ 0
this : Nonempty α
⊢ type r = type r
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case mp
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
⊢ typeLT α ∈ range succ → ∃ x, IsTop x

pp: case mpr
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
⊢ (∃ x, IsTop x) → typeLT α ∈ range succ

Tactic:
<;>

Goal state after:
case mp
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
⊢ typeLT α ∈ range succ → ∃ x, IsTop x

case mpr
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
⊢ (∃ x, IsTop x) → typeLT α ∈ range succ
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case refine_1
α✝ : Type u
β✝ : Type v
γ : Type w
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
c : Cardinal.{u}
α β : Type u
f : α ≃ β
o : Ordinal.{u}
⊢ (o ∈ range fun r ↦ type ↑r) → o ∈ range fun r ↦ type ↑r

pp: case refine_2
α✝ : Type u
β✝ : Type v
γ : Type w
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
c : Cardinal.{u}
α β : Type u
f : α ≃ β
o : Ordinal.{u}
⊢ (o ∈ range fun r ↦ type ↑r) → o ∈ range fun r ↦ type ↑r

Tactic:
<;>

Goal state after:
case refine_1
α✝ : Type u
β✝ : Type v
γ : Type w
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
c : Cardinal.{u}
α β : Type u
f : α ≃ β
o : Ordinal.{u}
⊢ (o ∈ range fun r ↦ type ↑r) → o ∈ range fun r ↦ type ↑r

case refine_2
α✝ : Type u
β✝ : Type v
γ : Type w
r : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
c : Cardinal.{u}
α β : Type u
f : α ≃ β
o : Ordinal.{u}
⊢ (o ∈ range fun r ↦ type ↑r) → o ∈ range fun r ↦ type ↑r
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: case e'_3
ι : Type u
ι' : Type v
f : ι → Ordinal.{max (max u v) w}
g : ι' → Ordinal.{max (max u v) w}
h : range f ⊆ range g
⊢ range (succ ∘ f) = ?convert_2 '' range f

pp: case e'_4
ι : Type u
ι' : Type v
f : ι → Ordinal.{max (max u v) w}
g : ι' → Ordinal.{max (max u v) w}
h : range f ⊆ range g
⊢ range (succ ∘ g) = ?convert_2 '' range g

pp: case convert_2
ι : Type u
ι' : Type v
f : ι → Ordinal.{max (max u v) w}
g : ι' → Ordinal.{max (max u v) w}
h : range f ⊆ range g
⊢ Ordinal.{max (max u v) w} → Ordinal.{max u v w}

Tactic:
<;>

Goal state after:
case e'_3
ι : Type u
ι' : Type v
f : ι → Ordinal.{max (max u v) w}
g : ι' → Ordinal.{max (max u v) w}
h : range f ⊆ range g
⊢ range (succ ∘ f) = ?convert_2 '' range f

case e'_4
ι : Type u
ι' : Type v
f : ι → Ordinal.{max (max u v) w}
g : ι' → Ordinal.{max (max u v) w}
h : range f ⊆ range g
⊢ range (succ ∘ g) = ?convert_2 '' range g

case convert_2
ι : Type u
ι' : Type v
f : ι → Ordinal.{max (max u v) w}
g : ι' → Ordinal.{max (max u v) w}
h : range f ⊆ range g
⊢ Ordinal.{max (max u v) w} → Ordinal.{max u v w}
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case refine_1
α✝ : Type u
β✝ : Type v
γ : Type w
r✝ : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
c : Cardinal.{u}
α β : Type u
f : α ≃ β
r : α → α → Prop
hr : IsWellOrder α r
⊢ (fun r ↦ type ↑r) ⟨r, hr⟩ ∈ range fun r ↦ type ↑r

pp: case refine_2
α✝ : Type u
β✝ : Type v
γ : Type w
r✝ : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
c : Cardinal.{u}
α β : Type u
f : α ≃ β
r : β → β → Prop
hr : IsWellOrder β r
⊢ (fun r ↦ type ↑r) ⟨r, hr⟩ ∈ range fun r ↦ type ↑r

Tactic:
<;>

Goal state after:
case refine_1
α✝ : Type u
β✝ : Type v
γ : Type w
r✝ : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
c : Cardinal.{u}
α β : Type u
f : α ≃ β
r : α → α → Prop
hr : IsWellOrder α r
⊢ (fun r ↦ type ↑r) ⟨r, hr⟩ ∈ range fun r ↦ type ↑r

case refine_2
α✝ : Type u
β✝ : Type v
γ : Type w
r✝ : α✝ → α✝ → Prop
s : β✝ → β✝ → Prop
t : γ → γ → Prop
c : Cardinal.{u}
α β : Type u
f : α ≃ β
r : β → β → Prop
hr : IsWellOrder β r
⊢ (fun r ↦ type ↑r) ⟨r, hr⟩ ∈ range fun r ↦ type ↑r
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case mp
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
⊢ (#α).ord ≤ type s → #α ≤ (type s).card

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
⊢ #α ≤ (type s).card → (#α).ord ≤ type s

Tactic:
<;>

Goal state after:
case mp
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
⊢ (#α).ord ≤ type s → #α ≤ (type s).card

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
⊢ #α ≤ (type s).card → (#α).ord ≤ type s
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
f : α ↪ { α := β, r := s, wo := x✝ }.α
g : ⇑f ⁻¹'o s ↪r s
this : IsWellOrder α (⇑f ⁻¹'o s)
⊢ (#α).ord ≤ type s

Tactic:
exact (ord_le_type _).trans g.ordinal_type_le

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

Goal state before:
pp: case refine_1
c : Cardinal.{v}
a : Ordinal.{max v u}
ha : a < Ordinal.lift.{u, v} c.ord
⊢ a < (lift.{u, v} c).ord

Tactic:
rcases Ordinal.lt_lift_iff.1 ha with ⟨a, _, rfl⟩

Goal state after:
case refine_1
c : Cardinal.{v}
a : Ordinal.{v}
left✝ : a < c.ord
ha : Ordinal.lift.{u, v} a < Ordinal.lift.{u, v} c.ord
⊢ Ordinal.lift.{u, v} a < (lift.{u, v} c).ord
Module: Mathlib.SetTheory.Ordinal.Family

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

Tactic:
by
  refine ⟨fun h => ?_, ?_⟩
  · by_contra! hf
    exact
      ne_of_lt (succ_le_iff.1 h)
        (le_antisymm (bsup_le_blsub f) (blsub_le (lt_bsup_of_ne_bsup.1 hf)))
  rintro ⟨_, _, hf⟩
  rw [succ_le_iff, ← hf]
  exact lt_blsub _ _ _

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

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

Tactic:
rw [h]
    apply lt_blsub

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

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

Tactic:
div_zero

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

Goal state before:
pp: case inl
a c : Ordinal.{u_4}
hc : c < a
b : Ordinal.{u_4}
⊢ 0 = b / 0

Tactic:
div_zero

Goal state after:
case inl
a c : Ordinal.{u_4}
hc : c < a
b : Ordinal.{u_4}
⊢ 0 = 0
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case succ
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
this : n / b ≠ 0
⊢ 0 < b

pp: case succ.hb
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
this : n / b ≠ 0
⊢ 1 < b

pp: case succ.hy
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
this : n / b ≠ 0
⊢ n / b ≠ 0

pp: case succ.hb
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
this : n / b ≠ 0
⊢ 1 < b

pp: case succ.hy
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
this : n / b ≠ 0
⊢ n ≠ 0

Tactic:
<;>

Goal state after:
case succ
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
this : n / b ≠ 0
⊢ 0 < b

case succ.hb
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
this : n / b ≠ 0
⊢ 1 < b

case succ.hy
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
this : n / b ≠ 0
⊢ n / b ≠ 0

case succ.hb
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
this : n / b ≠ 0
⊢ 1 < b

case succ.hy
b n : ℕ
h : 1 < b
hn : b ≤ n
c : ℕ
this : n / b ≠ 0
⊢ n ≠ 0
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
⊢ (o'.bsup fun a ha ↦ f (g a ha) ⋯) ≤ o.bsup f

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
⊢ o.bsup f ≤ o'.bsup fun a ha ↦ f (g a ha) ⋯

Tactic:
<;>

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
⊢ (o'.bsup fun a ha ↦ f (g a ha) ⋯) ≤ o.bsup f

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
⊢ o.bsup f ≤ o'.bsup fun a ha ↦ f (g a ha) ⋯
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inl.hb
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hb : 1 < b
hn : n ≠ 0
⊢ 1 < b

pp: case inl.hy
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hb : 1 < b
hn : n ≠ 0
⊢ n ≠ 0

pp: case inl.hb
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hb : 1 < b
hn : n ≠ 0
⊢ 1 < b

pp: case inl.hy
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hb : 1 < b
hn : n ≠ 0
⊢ n ≠ 0

Tactic:
<;>

Goal state after:
case inl.hb
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hb : 1 < b
hn : n ≠ 0
⊢ 1 < b

case inl.hy
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hb : 1 < b
hn : n ≠ 0
⊢ n ≠ 0

case inl.hb
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hb : 1 < b
hn : n ≠ 0
⊢ 1 < b

case inl.hy
b m n : ℕ
h : m ≠ 0 ∨ 1 < b ∧ n ≠ 0
hb : 1 < b
hn : n ≠ 0
⊢ n ≠ 0
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inr.inl.inl
m n : ℕ
hm : m ≠ 0
h : m ≠ 0 ∨ 1 < 0 ∧ n ≠ 0
hb : 0 ≤ 1
⊢ log 0 n = m ↔ 0 ^ m ≤ n ∧ n < 0 ^ (m + 1)

pp: case inr.inl.inr
m n : ℕ
hm : m ≠ 0
h : m ≠ 0 ∨ 1 < 1 ∧ n ≠ 0
hb : 1 ≤ 1
⊢ log 1 n = m ↔ 1 ^ m ≤ n ∧ n < 1 ^ (m + 1)

Tactic:
<;>

Goal state after:
case inr.inl.inl
m n : ℕ
hm : m ≠ 0
h : m ≠ 0 ∨ 1 < 0 ∧ n ≠ 0
hb : 0 ≤ 1
⊢ log 0 n = m ↔ 0 ^ m ≤ n ∧ n < 0 ^ (m + 1)

case inr.inl.inr
m n : ℕ
hm : m ≠ 0
h : m ≠ 0 ∨ 1 < 1 ∧ n ≠ 0
hb : 1 ≤ 1
⊢ log 1 n = m ↔ 1 ^ m ≤ n ∧ n < 1 ^ (m + 1)
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inr.inl.inl
m n : ℕ
hm : m ≠ 0
h : m ≠ 0 ∨ 1 < 0 ∧ n ≠ 0
hb : 0 ≤ 1
⊢ 0 = m ↔ 0 ^ m ≤ n ∧ n < 0 ^ (m + 1)

pp: case inr.inl.inr
m n : ℕ
hm : m ≠ 0
h : m ≠ 0 ∨ 1 < 1 ∧ n ≠ 0
hb : 1 ≤ 1
⊢ 0 = m ↔ 1 ^ m ≤ n ∧ n < 1 ^ (m + 1)

Tactic:
<;>

Goal state after:
case inr.inl.inl
m n : ℕ
hm : m ≠ 0
h : m ≠ 0 ∨ 1 < 0 ∧ n ≠ 0
hb : 0 ≤ 1
⊢ 0 = m ↔ 0 ^ m ≤ n ∧ n < 0 ^ (m + 1)

case inr.inl.inr
m n : ℕ
hm : m ≠ 0
h : m ≠ 0 ∨ 1 < 1 ∧ n ≠ 0
hb : 1 ≤ 1
⊢ 0 = m ↔ 1 ^ m ≤ n ∧ n < 1 ^ (m + 1)
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case h₁
b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ b ^ (log b n + 1) ≤ n * b

pp: case h₂
b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ n * b < b ^ (log b n + 1 + 1)

Tactic:
<;>

Goal state after:
case h₁
b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ b ^ (log b n + 1) ≤ n * b

case h₂
b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ n * b < b ^ (log b n + 1 + 1)