mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: case h.left
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h_ninj :
  ∃ a b,
    (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) a =
        (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) b ∧
      a ≠ b
a b : ↑(Set.Iio (SuccOrder.succ #α).ord)
h_fab :
  (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) a =
    (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) b
h_nab : a ≠ b
h_eq : ↑a = ↑b
⊢ False

Tactic:
;

Goal state after:
case h.left
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h_ninj :
  ∃ a b,
    (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) a =
        (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) b ∧
      a ≠ b
a b : ↑(Set.Iio (SuccOrder.succ #α).ord)
h_fab :
  (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) a =
    (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) b
h_nab : a ≠ b
h_eq : ↑a = ↑b
⊢ False
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: case h.left
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h_ninj :
  ∃ a b,
    (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) a =
        (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) b ∧
      a ≠ b
a b : ↑(Set.Iio (SuccOrder.succ #α).ord)
h_fab :
  (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) a =
    (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) b
h_nab : a ≠ b
h_eq : a = b
⊢ False

Tactic:
;

Goal state after:
case h.left
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h_ninj :
  ∃ a b,
    (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) a =
        (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) b ∧
      a ≠ b
a b : ↑(Set.Iio (SuccOrder.succ #α).ord)
h_fab :
  (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) a =
    (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) b
h_nab : a ≠ b
h_eq : a = b
⊢ False
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case atom.mp
α : Type u_1
inst✝ : DecidableEq α
a✝ : α
⊢ Lists'.atom a✝ = Lists'.atom a✝

Tactic:
;

Goal state after:
case atom.mp
α : Type u_1
inst✝ : DecidableEq α
a✝ : α
⊢ Lists'.atom a✝ = Lists'.atom a✝
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case atom.mpr
α : Type u_1
inst✝ : DecidableEq α
a✝ : α
⊢ ⟨false, Lists'.atom a✝⟩ = ⟨false, Lists'.atom a✝⟩

Tactic:
;

Goal state after:
case atom.mpr
α : Type u_1
inst✝ : DecidableEq α
a✝ : α
⊢ ⟨false, Lists'.atom a✝⟩ = ⟨false, Lists'.atom a✝⟩
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: case h
α : Type u
inst✝ : CompleteLattice α
f : α →o α
⊢ lfp f = ↑⊥

Tactic:
;

Goal state after:
case h
α : Type u
inst✝ : CompleteLattice α
f : α →o α
⊢ lfp f = ↑⊥
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : Lists α
b✝ : Bool
b : Lists' α b✝
l₂ : Lists' α true
this✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : Decidable (a ∈ l₂)
⊢ a ∈ b.cons' l₂ ↔ a ∈ Lists'.cons ⟨b✝, b⟩ l₂

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : Lists α
b✝ : Bool
b : Lists' α b✝
l₂ : Lists' α true
this✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : Decidable (a ∈ l₂)
⊢ a ∈ b.cons' l₂ ↔ a ∈ Lists'.cons ⟨b✝, b⟩ l₂
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
h_lfp : ∃ y, lfp f = ↑y
y : ↑(fixedPoints ⇑f)
h_y : lfp f = ↑y
⊢ lfpApprox f ⊥ (succ #α).ord ≤ lfp f

Tactic:
;

Goal state after:
case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
h_lfp : ∃ y, lfp f = ↑y
y : ↑(fixedPoints ⇑f)
h_y : lfp f = ↑y
⊢ lfpApprox f ⊥ (succ #α).ord ≤ lfp f
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
h_fix : ∃ y, lfpApprox f ⊥ (succ #α).ord = ↑y
x : ↑(fixedPoints ⇑f)
h_x : lfpApprox f ⊥ (succ #α).ord = ↑x
⊢ lfp f ≤ lfpApprox f ⊥ (succ #α).ord

Tactic:
;

Goal state after:
case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
h_fix : ∃ y, lfpApprox f ⊥ (succ #α).ord = ↑y
x : ↑(fixedPoints ⇑f)
h_x : lfpApprox f ⊥ (succ #α).ord = ↑x
⊢ lfp f ≤ lfpApprox f ⊥ (succ #α).ord
Module: Mathlib.Topology.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : LinearOrder α
inst✝⁶ : WellFoundedLT α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : WellFoundedLT β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
⊢ StrictMono f ∧ Continuous f → IsNormal f

Tactic:
by
    rintro ⟨hs, hc⟩
    refine ⟨hs, fun {a} ha ↦ (isLUB_of_mem_closure ?_ ?_).2⟩
    · rintro _ ⟨b, hb, rfl⟩
      exact (hs hb).le
    · apply image_closure_subset_closure_image hc (mem_image_of_mem ..)
      exact ha.isLUB_Iio.mem_closure (Iio_nonempty.2 ha.1)

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

Goal state before:
pp: case inl
b e : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
h : ∀ e' ∈ f.support, e' < e
⊢ eval b (single e 0 + f) = b ^ e * 0 + eval b f

pp: case inr
b e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
h : ∀ e' ∈ f.support, e' < e
hx : x ≠ 0
⊢ eval b (single e x + f) = b ^ e * x + eval b f

Tactic:
;

Goal state after:
case inl
b e : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
h : ∀ e' ∈ f.support, e' < e
⊢ eval b (single e 0 + f) = b ^ e * 0 + eval b f

case inr
b e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
h : ∀ e' ∈ f.support, e' < e
hx : x ≠ 0
⊢ eval b (single e x + f) = b ^ e * x + eval b f
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
⊢ (e₁.oadd n₁ a₁).cmp (e₂.oadd n₂ a₂) = Ordering.eq → e₁.oadd n₁ a₁ = e₂.oadd n₂ a₂

Tactic:
;

Goal state after:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
⊢ (e₁.oadd n₁ a₁).cmp (e₂.oadd n₂ a₂) = Ordering.eq → e₁.oadd n₁ a₁ = e₂.oadd n₂ a₂
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case eq
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : e₁.cmp e₁ = Ordering.eq
⊢ Ordering.eq.then ((_root_.cmp ↑n₁ ↑n₂).then (a₁.cmp a₂)) = Ordering.eq → e₁.oadd n₁ a₁ = e₁.oadd n₂ a₂

Tactic:
;

Goal state after:
case eq
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : e₁.cmp e₁ = Ordering.eq
⊢ Ordering.eq.then ((_root_.cmp ↑n₁ ↑n₂).then (a₁.cmp a₂)) = Ordering.eq → e₁.oadd n₁ a₁ = e₁.oadd n₂ a₂
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd'
e : ONote
n : ℕ+
a : ONote
b eb✝ : Ordinal.{0}
h₁ : e.NFBelow eb✝
h₂ : a.NFBelow e.repr
h₃ : e.repr < b
⊢ e.NF

Tactic:
;

Goal state after:
case oadd'
e : ONote
n : ℕ+
a : ONote
b eb✝ : Ordinal.{0}
h₁ : e.NFBelow eb✝
h₂ : a.NFBelow e.repr
h₃ : e.repr < b
⊢ e.NF
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd'
e : ONote
n : ℕ+
a : ONote
b eb✝ : Ordinal.{0}
h₁ : e.NFBelow eb✝
h₂ : a.NFBelow e.repr
h₃ : e.repr < b
⊢ a.NFBelow e.repr

Tactic:
;

Goal state after:
case oadd'
e : ONote
n : ℕ+
a : ONote
b eb✝ : Ordinal.{0}
h₁ : e.NFBelow eb✝
h₂ : a.NFBelow e.repr
h₃ : e.repr < b
⊢ a.NFBelow e.repr
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd'
e : ONote
n : ℕ+
a : ONote
b eb✝ : Ordinal.{0}
h₁ : e.NFBelow eb✝
h₂ : a.NFBelow e.repr
h₃ : e.repr < b
⊢ e.repr < b

Tactic:
;

Goal state after:
case oadd'
e : ONote
n : ℕ+
a : ONote
b eb✝ : Ordinal.{0}
h₁ : e.NFBelow eb✝
h₂ : a.NFBelow e.repr
h₃ : e.repr < b
⊢ e.repr < b
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd'.a
o : ONote
b₁ b₂ : Ordinal.{0}
e✝ : ONote
n✝ : ℕ+
a✝ : ONote
eb✝ b✝ : Ordinal.{0}
h₁ : e✝.NFBelow eb✝
h₂ : a✝.NFBelow e✝.repr
h₃ : e✝.repr < b✝
a_ih✝¹ : eb✝ ≤ b₂ → e✝.NFBelow b₂
a_ih✝ : e✝.repr ≤ b₂ → a✝.NFBelow b₂
bb : b✝ ≤ b₂
⊢ e✝.NFBelow ?oadd'.eb

pp: case oadd'.a
o : ONote
b₁ b₂ : Ordinal.{0}
e✝ : ONote
n✝ : ℕ+
a✝ : ONote
eb✝ b✝ : Ordinal.{0}
h₁ : e✝.NFBelow eb✝
h₂ : a✝.NFBelow e✝.repr
h₃ : e✝.repr < b✝
a_ih✝¹ : eb✝ ≤ b₂ → e✝.NFBelow b₂
a_ih✝ : e✝.repr ≤ b₂ → a✝.NFBelow b₂
bb : b✝ ≤ b₂
⊢ a✝.NFBelow e✝.repr

pp: case oadd'.a
o : ONote
b₁ b₂ : Ordinal.{0}
e✝ : ONote
n✝ : ℕ+
a✝ : ONote
eb✝ b✝ : Ordinal.{0}
h₁ : e✝.NFBelow eb✝
h₂ : a✝.NFBelow e✝.repr
h₃ : e✝.repr < b✝
a_ih✝¹ : eb✝ ≤ b₂ → e✝.NFBelow b₂
a_ih✝ : e✝.repr ≤ b₂ → a✝.NFBelow b₂
bb : b✝ ≤ b₂
⊢ e✝.repr < b₂

pp: case oadd'.eb
o : ONote
b₁ b₂ : Ordinal.{0}
e✝ : ONote
n✝ : ℕ+
a✝ : ONote
eb✝ b✝ : Ordinal.{0}
h₁ : e✝.NFBelow eb✝
h₂ : a✝.NFBelow e✝.repr
h₃ : e✝.repr < b✝
a_ih✝¹ : eb✝ ≤ b₂ → e✝.NFBelow b₂
a_ih✝ : e✝.repr ≤ b₂ → a✝.NFBelow b₂
bb : b✝ ≤ b₂
⊢ Ordinal.{0}

Tactic:
;

Goal state after:
case oadd'.a
o : ONote
b₁ b₂ : Ordinal.{0}
e✝ : ONote
n✝ : ℕ+
a✝ : ONote
eb✝ b✝ : Ordinal.{0}
h₁ : e✝.NFBelow eb✝
h₂ : a✝.NFBelow e✝.repr
h₃ : e✝.repr < b✝
a_ih✝¹ : eb✝ ≤ b₂ → e✝.NFBelow b₂
a_ih✝ : e✝.repr ≤ b₂ → a✝.NFBelow b₂
bb : b✝ ≤ b₂
⊢ e✝.NFBelow ?oadd'.eb

case oadd'.a
o : ONote
b₁ b₂ : Ordinal.{0}
e✝ : ONote
n✝ : ℕ+
a✝ : ONote
eb✝ b✝ : Ordinal.{0}
h₁ : e✝.NFBelow eb✝
h₂ : a✝.NFBelow e✝.repr
h₃ : e✝.repr < b✝
a_ih✝¹ : eb✝ ≤ b₂ → e✝.NFBelow b₂
a_ih✝ : e✝.repr ≤ b₂ → a✝.NFBelow b₂
bb : b✝ ≤ b₂
⊢ a✝.NFBelow e✝.repr

case oadd'.a
o : ONote
b₁ b₂ : Ordinal.{0}
e✝ : ONote
n✝ : ℕ+
a✝ : ONote
eb✝ b✝ : Ordinal.{0}
h₁ : e✝.NFBelow eb✝
h₂ : a✝.NFBelow e✝.repr
h₃ : e✝.repr < b✝
a_ih✝¹ : eb✝ ≤ b₂ → e✝.NFBelow b₂
a_ih✝ : e✝.repr ≤ b₂ → a✝.NFBelow b₂
bb : b✝ ≤ b₂
⊢ e✝.repr < b₂

case oadd'.eb
o : ONote
b₁ b₂ : Ordinal.{0}
e✝ : ONote
n✝ : ℕ+
a✝ : ONote
eb✝ b✝ : Ordinal.{0}
h₁ : e✝.NFBelow eb✝
h₂ : a✝.NFBelow e✝.repr
h₃ : e✝.repr < b✝
a_ih✝¹ : eb✝ ≤ b₂ → e✝.NFBelow b₂
a_ih✝ : e✝.repr ≤ b₂ → a✝.NFBelow b₂
bb : b✝ ≤ b₂
⊢ Ordinal.{0}
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd'
e : ONote
n : ℕ+
a : ONote
b : Ordinal.{0}
H : e.repr < b
b' eb✝ : Ordinal.{0}
h₁ : e.NFBelow eb✝
h₂ : a.NFBelow e.repr
h₃ : e.repr < b'
⊢ (e.oadd n a).NFBelow b

Tactic:
;

Goal state after:
case oadd'
e : ONote
n : ℕ+
a : ONote
b : Ordinal.{0}
H : e.repr < b
b' eb✝ : Ordinal.{0}
h₁ : e.NFBelow eb✝
h₂ : a.NFBelow e.repr
h₃ : e.repr < b'
⊢ (e.oadd n a).NFBelow b
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd'
e : ONote
n : ℕ+
a : ONote
b : Ordinal.{0}
H : e.repr < b
b' eb✝ : Ordinal.{0}
h₁ : e.NFBelow eb✝
h₂ : a.NFBelow e.repr
h₃ : e.repr < b'
⊢ (e.oadd n a).NFBelow b

Tactic:
exact NFBelow.oadd' h₁ h₂ H

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

Goal state before:
pp: ⊢ (↑1).NF

Tactic:
;

Goal state after:
⊢ (↑1).NF
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: e : ONote
n : ℕ+
a₁ a₂ : ONote
h : a₁ < a₂
⊢ (e.oadd n a₁).repr < (e.oadd n a₂).repr

Tactic:
;

Goal state after:
e : ONote
n : ℕ+
a₁ a₂ : ONote
h : a₁ < a₂
⊢ (e.oadd n a₁).repr < (e.oadd n a₂).repr
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: e : ONote
n : ℕ+
a₁ a₂ : ONote
h : a₁ < a₂
⊢ ω ^ e.repr * ↑↑n + a₁.repr < ω ^ e.repr * ↑↑n + a₂.repr

Tactic:
;

Goal state after:
e : ONote
n : ℕ+
a₁ a₂ : ONote
h : a₁ < a₂
⊢ ω ^ e.repr * ↑↑n + a₁.repr < ω ^ e.repr * ↑↑n + a₂.repr
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h✝¹ : o₁ = e₁.oadd n₁ a₁
o₂ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h✝ : o₂ = e₂.oadd n₂ a₂
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹).NF
h₂ : (namedPattern o₂ (e₂.oadd n₂ a₂) h✝).NF
IHe :
  match e₁.cmp e₂, e₁, e₂ with
  | Ordering.lt, a, b => a < b
  | Ordering.eq, a, b => a = b
  | Ordering.gt, a, b => b < a
⊢ ((e₁.cmp e₂).then ((_root_.cmp ↑n₁ ↑n₂).then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹)
    (namedPattern o₂ (e₂.oadd n₂ a₂) h✝)

Tactic:
;

Goal state after:
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h✝¹ : o₁ = e₁.oadd n₁ a₁
o₂ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h✝ : o₂ = e₂.oadd n₂ a₂
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹).NF
h₂ : (namedPattern o₂ (e₂.oadd n₂ a₂) h✝).NF
IHe :
  match e₁.cmp e₂, e₁, e₂ with
  | Ordering.lt, a, b => a < b
  | Ordering.eq, a, b => a = b
  | Ordering.gt, a, b => b < a
⊢ ((e₁.cmp e₂).then ((_root_.cmp ↑n₁ ↑n₂).then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹)
    (namedPattern o₂ (e₂.oadd n₂ a₂) h✝)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h✝¹ : o₁ = e₁.oadd n₁ a₁
o₂ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h✝ : o₂ = e₂.oadd n₂ a₂
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹).NF
h₂ : (namedPattern o₂ (e₂.oadd n₂ a₂) h✝).NF
IHe :
  match Ordering.lt, e₁, e₂ with
  | Ordering.lt, a, b => a < b
  | Ordering.eq, a, b => a = b
  | Ordering.gt, a, b => b < a
⊢ (Ordering.lt.then ((_root_.cmp ↑n₁ ↑n₂).then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹)
    (namedPattern o₂ (e₂.oadd n₂ a₂) h✝)

Tactic:
;

Goal state after:
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h✝¹ : o₁ = e₁.oadd n₁ a₁
o₂ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h✝ : o₂ = e₂.oadd n₂ a₂
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹).NF
h₂ : (namedPattern o₂ (e₂.oadd n₂ a₂) h✝).NF
IHe :
  match Ordering.lt, e₁, e₂ with
  | Ordering.lt, a, b => a < b
  | Ordering.eq, a, b => a = b
  | Ordering.gt, a, b => b < a
⊢ (Ordering.lt.then ((_root_.cmp ↑n₁ ↑n₂).then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹)
    (namedPattern o₂ (e₂.oadd n₂ a₂) h✝)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h✝¹ : o₁ = e₁.oadd n₁ a₁
o₂ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h✝ : o₂ = e₂.oadd n₂ a₂
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹).NF
h₂ : (namedPattern o₂ (e₂.oadd n₂ a₂) h✝).NF
IHe :
  match Ordering.gt, e₁, e₂ with
  | Ordering.lt, a, b => a < b
  | Ordering.eq, a, b => a = b
  | Ordering.gt, a, b => b < a
⊢ (Ordering.gt.then ((_root_.cmp ↑n₁ ↑n₂).then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹)
    (namedPattern o₂ (e₂.oadd n₂ a₂) h✝)

Tactic:
;

Goal state after:
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h✝¹ : o₁ = e₁.oadd n₁ a₁
o₂ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h✝ : o₂ = e₂.oadd n₂ a₂
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹).NF
h₂ : (namedPattern o₂ (e₂.oadd n₂ a₂) h✝).NF
IHe :
  match Ordering.gt, e₁, e₂ with
  | Ordering.lt, a, b => a < b
  | Ordering.eq, a, b => a = b
  | Ordering.gt, a, b => b < a
⊢ (Ordering.gt.then ((_root_.cmp ↑n₁ ↑n₂).then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹)
    (namedPattern o₂ (e₂.oadd n₂ a₂) h✝)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h✝¹ : o₁ = e₁.oadd n₁ a₁
o₂ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h✝ : o₂ = e₂.oadd n₂ a₂
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹).NF
h₂ : (namedPattern o₂ (e₂.oadd n₂ a₂) h✝).NF
IHe :
  match Ordering.eq, e₁, e₂ with
  | Ordering.lt, a, b => a < b
  | Ordering.eq, a, b => a = b
  | Ordering.gt, a, b => b < a
⊢ (Ordering.eq.then ((_root_.cmp ↑n₁ ↑n₂).then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹)
    (namedPattern o₂ (e₂.oadd n₂ a₂) h✝)

Tactic:
;

Goal state after:
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h✝¹ : o₁ = e₁.oadd n₁ a₁
o₂ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h✝ : o₂ = e₂.oadd n₂ a₂
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹).NF
h₂ : (namedPattern o₂ (e₂.oadd n₂ a₂) h✝).NF
IHe :
  match Ordering.eq, e₁, e₂ with
  | Ordering.lt, a, b => a < b
  | Ordering.eq, a, b => a = b
  | Ordering.gt, a, b => b < a
⊢ (Ordering.eq.then ((_root_.cmp ↑n₁ ↑n₂).then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹)
    (namedPattern o₂ (e₂.oadd n₂ a₂) h✝)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h✝¹ : o₁ = e₁.oadd n₁ a₁
o₂ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h✝ : o₂ = e₂.oadd n₂ a₂
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹).NF
h₂ : (namedPattern o₂ (e₂.oadd n₂ a₂) h✝).NF
IHe : e₁ = e₂
⊢ (Ordering.eq.then ((_root_.cmp ↑n₁ ↑n₂).then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹)
    (namedPattern o₂ (e₂.oadd n₂ a₂) h✝)

Tactic:
;

Goal state after:
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h✝¹ : o₁ = e₁.oadd n₁ a₁
o₂ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h✝ : o₂ = e₂.oadd n₂ a₂
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹).NF
h₂ : (namedPattern o₂ (e₂.oadd n₂ a₂) h✝).NF
IHe : e₁ = e₂
⊢ (Ordering.eq.then ((_root_.cmp ↑n₁ ↑n₂).then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹)
    (namedPattern o₂ (e₂.oadd n₂ a₂) h✝)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h✝¹ : o₁ = e₁.oadd n₁ a₁
o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹).NF
h✝ : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h✝).NF
⊢ (Ordering.eq.then ((cmpUsing (fun x1 x2 ↦ x1 < x2) ↑n₁ ↑n₂).then (a₁.cmp a₂))).Compares
    (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹) (namedPattern o₂ (e₁.oadd n₂ a₂) h✝)

Tactic:
;

Goal state after:
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h✝¹ : o₁ = e₁.oadd n₁ a₁
o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹).NF
h✝ : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h✝).NF
⊢ (Ordering.eq.then ((cmpUsing (fun x1 x2 ↦ x1 < x2) ↑n₁ ↑n₂).then (a₁.cmp a₂))).Compares
    (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹) (namedPattern o₂ (e₁.oadd n₂ a₂) h✝)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case inr
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h✝¹ : o₁ = e₁.oadd n₁ a₁
o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹).NF
h✝ : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h✝).NF
nh : ↑n₂ ≤ ↑n₁ ∧ (↑n₂ < ↑n₁ ∧ Ordering.gt = Ordering.lt ∨ ¬↑n₂ < ↑n₁ ∧ Ordering.eq = Ordering.lt)
⊢ (Ordering.eq.then (Ordering.lt.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝)

Tactic:
;

Goal state after:
case inr
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h✝¹ : o₁ = e₁.oadd n₁ a₁
o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹).NF
h✝ : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h✝).NF
nh : ↑n₂ ≤ ↑n₁ ∧ (↑n₂ < ↑n₁ ∧ Ordering.gt = Ordering.lt ∨ ¬↑n₂ < ↑n₁ ∧ Ordering.eq = Ordering.lt)
⊢ (Ordering.eq.then (Ordering.lt.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case inl.intro
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h✝¹ : o₁ = e₁.oadd n₁ a₁
o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹).NF
h✝ : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h✝).NF
left✝ : ↑n₁ < ↑n₂
right✝ : Ordering.lt = Ordering.gt
⊢ (Ordering.eq.then (Ordering.gt.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝)

Tactic:
;

Goal state after:
case inl.intro
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h✝¹ : o₁ = e₁.oadd n₁ a₁
o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹).NF
h✝ : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h✝).NF
left✝ : ↑n₁ < ↑n₂
right✝ : Ordering.lt = Ordering.gt
⊢ (Ordering.eq.then (Ordering.gt.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case inr
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h✝¹ : o₁ = e₁.oadd n₁ a₁
o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹).NF
h✝ : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h✝).NF
left✝ : ↑n₂ ≤ ↑n₁
nh : ↑n₂ < ↑n₁ ∧ Ordering.gt = Ordering.gt ∨ ¬↑n₂ < ↑n₁ ∧ Ordering.eq = Ordering.gt
⊢ (Ordering.eq.then (Ordering.gt.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝)

Tactic:
;

Goal state after:
case inr
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h✝¹ : o₁ = e₁.oadd n₁ a₁
o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹).NF
h✝ : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h✝).NF
left✝ : ↑n₂ ≤ ↑n₁
nh : ↑n₂ < ↑n₁ ∧ Ordering.gt = Ordering.gt ∨ ¬↑n₂ < ↑n₁ ∧ Ordering.eq = Ordering.gt
⊢ (Ordering.eq.then (Ordering.gt.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case inr.inr.intro
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h✝¹ : o₁ = e₁.oadd n₁ a₁
o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹).NF
h✝ : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h✝).NF
left✝¹ : ↑n₂ ≤ ↑n₁
left✝ : ¬↑n₂ < ↑n₁
right✝ : Ordering.eq = Ordering.gt
⊢ (Ordering.eq.then (Ordering.gt.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝)

Tactic:
;

Goal state after:
case inr.inr.intro
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h✝¹ : o₁ = e₁.oadd n₁ a₁
o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹).NF
h✝ : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h✝).NF
left✝¹ : ↑n₂ ≤ ↑n₁
left✝ : ¬↑n₂ < ↑n₁
right✝ : Ordering.eq = Ordering.gt
⊢ (Ordering.eq.then (Ordering.gt.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case eq.inl.intro
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h✝¹ : o₁ = e₁.oadd n₁ a₁
o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹).NF
h✝ : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h✝).NF
left✝ : ↑n₁ < ↑n₂
right✝ : Ordering.lt = Ordering.eq
⊢ (Ordering.eq.then (Ordering.eq.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝)

Tactic:
;

Goal state after:
case eq.inl.intro
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h✝¹ : o₁ = e₁.oadd n₁ a₁
o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹).NF
h✝ : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h✝).NF
left✝ : ↑n₁ < ↑n₂
right✝ : Ordering.lt = Ordering.eq
⊢ (Ordering.eq.then (Ordering.eq.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case eq.inr.inl.intro
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h✝¹ : o₁ = e₁.oadd n₁ a₁
o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹).NF
h✝ : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h✝).NF
nhl : ↑n₂ ≤ ↑n₁
left✝ : ↑n₂ < ↑n₁
right✝ : Ordering.gt = Ordering.eq
⊢ (Ordering.eq.then (Ordering.eq.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝)

Tactic:
;

Goal state after:
case eq.inr.inl.intro
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h✝¹ : o₁ = e₁.oadd n₁ a₁
o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹).NF
h✝ : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h✝).NF
nhl : ↑n₂ ≤ ↑n₁
left✝ : ↑n₂ < ↑n₁
right✝ : Ordering.gt = Ordering.eq
⊢ (Ordering.eq.then (Ordering.eq.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case eq.inr.inr
o₁ e₁ a₁ o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h✝¹ : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h✝¹).NF
h✝ : o₁ = e₁.oadd n₂ a₁
h₁ : (namedPattern o₁ (e₁.oadd n₂ a₁) h✝).NF
nhl : ↑n₂ ≤ ↑n₂
nhr : ¬↑n₂ < ↑n₂ ∧ Ordering.eq = Ordering.eq
⊢ (a₁.cmp a₂).Compares a₁ a₂ →
    (Ordering.eq.then (Ordering.eq.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₂ a₁) h✝)
      (namedPattern o₂ (e₁.oadd n₂ a₂) h✝¹)

Tactic:
;

Goal state after:
case eq.inr.inr
o₁ e₁ a₁ o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h✝¹ : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h✝¹).NF
h✝ : o₁ = e₁.oadd n₂ a₁
h₁ : (namedPattern o₁ (e₁.oadd n₂ a₁) h✝).NF
nhl : ↑n₂ ≤ ↑n₂
nhr : ¬↑n₂ < ↑n₂ ∧ Ordering.eq = Ordering.eq
⊢ (a₁.cmp a₂).Compares a₁ a₂ →
    (Ordering.eq.then (Ordering.eq.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₂ a₁) h✝)
      (namedPattern o₂ (e₁.oadd n₂ a₂) h✝¹)