awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
Goal:
a : Ordinal.{u}
ι : Type u
f : ι → Ordinal.{u}
hf : lsub f = a
hι : #ι = a.cof
r : ι → ι → Prop
wo : IsWellOrder ι r
hr : (#ι).ord = type r
r' : { i : ι // ∀ (j : ι), r j i → f j < f i } → { i : ι // ∀ (j : ι), r j i → f j < f i } → Prop :=
  Subrel r fun (i : ι) ↦ ∀ (j : ι), r j i → f j < f i
hrr' : r' ↪r r := Subrel.relEmbedding r fun (i : ι) ↦ ∀ (j : ι), r j i → f j < f i
this : IsWellOrder { i : ι // ∀ (j : ι), r j i → f j < f i } r'
i : ι
h : ∃ (j : ι), r j i ∧ f i ≤ f j
hji : r (WellFounded.min (r := r) ⋯ (fun (x : ι) ↦ r x i ∧ f i ≤ f x) h) i
hij : f i ≤ f (WellFounded.min (r := r) ⋯ (fun (x : ι) ↦ r x i ∧ f i ≤ f x) h)
neg neg₁ neg₂ neg₃ :
  f i ≤
    f
      (↑(Subtype.mk (p := fun (i : ι) ↦ ∀ (j : ι), r j i → f j < f i)
            (WellFounded.min (r := r) ⋯ (fun (x : ι) ↦ r x i ∧ f i ≤ f x) h) ⋯) :
        ι)
⊢ f i ≤
    bfamilyOfFamily' r' (fun (i : { i : ι // ∀ (j : ι), r j i → f j < f i }) ↦ f (↑i : ι))
      (((typein r').toRelEmbedding (r := r') (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) :
          (a : { i : ι // ∀ (j : ι), r j i → f j < f i }) → Ordinal.{u})
        (Subtype.mk (p := fun (i : ι) ↦ ∀ (j : ι), r j i → f j < f i)
          (WellFounded.min (r := r) ⋯ (fun (x : ι) ↦ r x i ∧ f i ≤ f x) h) ⋯))
      ⋯

Tactic:
rwa [bfamilyOfFamily'_typein]

Premises used: Ordinal.bfamilyOfFamily'_typein
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
a o : Ordinal.{u}
ha : IsSuccLimit a
g : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hg : a.IsFundamentalSequence o g
⊢ (f a).IsFundamentalSequence o fun (b : Ordinal.{u}) (hb : b < o) ↦ f (g b hb)

Tactic:
⟨?_, @fun i j _ _ h => hf.strictMono (hg.2.1 _ _ h), ?_⟩

Premises used: Ordinal.IsFundamentalSequence, And.right, And.left, And.intro, Order.IsNormal.strictMono
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
a o : Ordinal.{u}
ha : IsSuccLimit a
g : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hg : a.IsFundamentalSequence o g
refine_1 : o ≤ (f a).cof.ord
refine_2 : (o.blsub fun (b : Ordinal.{u}) (hb : b < o) ↦ f (g b hb)) = f a
⊢ (f a).IsFundamentalSequence o fun (b : Ordinal.{u}) (hb : b < o) ↦ f (g b hb)

Tactic:
refine ⟨?_, @fun i j _ _ h => hf.strictMono (hg.2.1 _ _ h), ?_⟩
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
a o : Ordinal.{u}
ha : IsSuccLimit a
g : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hg : a.IsFundamentalSequence o g
⊢ o ≤ (f a).cof.ord

Tactic:
grind [Ordinal.IsFundamentalSequence, cof_map_of_isNormal]

Premises used: Ordinal.IsFundamentalSequence, Ordinal.cof_map_of_isNormal
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
a o : Ordinal.{u}
ha : IsSuccLimit a
g : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hg : a.IsFundamentalSequence o g
refine_2 : (a.blsub fun (b : Ordinal.{u}) (x : b < a) ↦ f b) = f a
⊢ (o.blsub fun (b : Ordinal.{u}) (hb : b < o) ↦ f (g b hb)) = f a

Tactic:
rw [@blsub_comp.{u, u, u} a _ (fun b _ => f b) (@fun i j _ _ h => hf.strictMono.monotone h) g
        hg.2.2]
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
a o : Ordinal.{u}
ha : IsSuccLimit a
g : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hg : a.IsFundamentalSequence o g
⊢ (a.blsub fun (b : Ordinal.{u}) (x : b < a) ↦ f b) = f a

Tactic:
IsNormal.blsub_eq.{u, u} hf ha

Premises used: Ordinal.IsNormal.blsub_eq
-- Module: Mathlib.SetTheory.Ordinal.FundamentalSequence
Goal:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
a o : Ordinal.{u}
ha : IsSuccLimit a
g : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hg : a.IsFundamentalSequence o g
⊢ (a.blsub fun (b : Ordinal.{u}) (x : b < a) ↦ f b) = f a

Tactic:
exact IsNormal.blsub_eq.{u, u} hf ha
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
⊢ zero = 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
⊢ repr 0 = 0

Tactic:
rfl

Premises used: ONote.repr, rfl
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
x y : ONote
⊢ x < y ↔ x.repr < y.repr

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
x y : ONote
⊢ x ≤ y ↔ x.repr ≤ y.repr

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
⊢ (↑0 : ONote) = 0

Tactic:
rfl

Premises used: ONote.ofNat, rfl
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
n : ℕ
⊢ (↑n.succ : ONote) = oadd 0 n.succPNat 0

Tactic:
rfl

Premises used: ONote.ofNat, rfl
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
⊢ (↑1 : ONote) = 1

Tactic:
rfl

Premises used: ONote.ofNat, Nat.succPNat, rfl
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
n : ℕ
zero : (↑0 : ONote).repr = (↑0 : Ordinal.{0})
succ : ∀ (n : ℕ), (↑(n + 1) : ONote).repr = (↑(n + 1) : Ordinal.{0})
⊢ (↑n : ONote).repr = (↑n : Ordinal.{0})

Tactic:
cases n
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
⊢ (↑0 : ONote).repr = (↑0 : Ordinal.{0})

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
n : ℕ
⊢ (↑(n + 1) : ONote).repr = (↑(n + 1) : Ordinal.{0})

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
⊢ repr 1 = (↑1 : Ordinal.{0})

Tactic:
repr_ofNat 1

Premises used: ONote.ofNat, Nat.succPNat, ONote.repr_ofNat, OfNat.ofNat
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a : ONote
⊢ ω ^ e.repr ≤ (e.oadd n a).repr

Tactic:
le_trans ?_ le_self_add

Premises used: le_self_add, le_trans
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a : ONote
refine : ω ^ e.repr ≤ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0})
⊢ ω ^ e.repr ≤ (e.oadd n a).repr

Tactic:
refine le_trans ?_ le_self_add

Premises used: le_self_add, le_trans
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a : ONote
⊢ ω ^ e.repr ≤ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0})

Tactic:
simpa using (mul_le_mul_iff_right₀ <| opow_pos (repr e) omega0_pos).2 (Nat.cast_le.2 n.2)

Premises used: Iff.mpr, Ordinal.omega0_pos, ONote.repr, Nat.cast_le, Ordinal.opow_pos, Subtype.property, mul_le_mul_iff_right₀
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a : ONote
⊢ 0 < e.oadd n a

Tactic:
@lt_of_lt_of_le _ _ _ (ω ^ repr e) _ (opow_pos (repr e) omega0_pos) (omega0_le_oadd e n a)

Premises used: Ordinal.omega0_pos, ONote.omega0_le_oadd, ONote.repr, Ordinal.opow_pos, lt_of_lt_of_le
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).cmp 0 = Ordering.eq
⊢ e.oadd n a = 0

Tactic:
injection h
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a : ONote
h : cmp 0 (e.oadd n a) = Ordering.eq
⊢ 0 = e.oadd n a

Tactic:
injection h
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h : (e₁.oadd n₁ a₁).cmp (e₂.oadd n₂ a₂) = Ordering.eq
revert : ∀ (h : (e₁.oadd n₁ a₁).cmp (e₂.oadd n₂ a₂) = Ordering.eq), e₁.oadd n₁ a₁ = e₂.oadd n₂ a₂
⊢ e₁.oadd n₁ a₁ = e₂.oadd n₂ a₂

Tactic:
revert h
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
lt :
  ∀ (h₁ : e₁.cmp e₂ = Ordering.lt)
    (h : Ordering.lt.then ((_root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ)).then (a₁.cmp a₂)) = Ordering.eq),
    e₁.oadd n₁ a₁ = e₂.oadd n₂ a₂
eq :
  ∀ (h₁ : e₁.cmp e₂ = Ordering.eq)
    (h : Ordering.eq.then ((_root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ)).then (a₁.cmp a₂)) = Ordering.eq),
    e₁.oadd n₁ a₁ = e₂.oadd n₂ a₂
gt :
  ∀ (h₁ : e₁.cmp e₂ = Ordering.gt)
    (h : Ordering.gt.then ((_root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ)).then (a₁.cmp a₂)) = Ordering.eq),
    e₁.oadd n₁ a₁ = e₂.oadd n₂ a₂
⊢ ∀ (h : (e₁.cmp e₂).then ((_root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ)).then (a₁.cmp a₂)) = Ordering.eq),
    e₁.oadd n₁ a₁ = e₂.oadd n₂ a₂

Tactic:
cases h₁ : cmp e₁ e₂

Premises used: ONote.cmp
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : e₁.cmp e₂ = Ordering.lt
h : Ordering.lt.then ((_root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ)).then (a₁.cmp a₂)) = Ordering.eq
⊢ e₁.oadd n₁ a₁ = e₂.oadd n₂ a₂

Tactic:
cases h
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : e₁.cmp e₂ = Ordering.lt
h : Ordering.lt.then ((_root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ)).then (a₁.cmp a₂)) = Ordering.eq
⊢ e₁.oadd n₁ a₁ = e₂.oadd n₂ a₂

Tactic:
try cases h
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : e₁.cmp e₂ = Ordering.eq
h : Ordering.eq.then ((_root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ)).then (a₁.cmp a₂)) = Ordering.eq
⊢ e₁.oadd n₁ a₁ = e₂.oadd n₂ a₂

Tactic:
cases h
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : e₁.cmp e₂ = Ordering.gt
h : Ordering.gt.then ((_root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ)).then (a₁.cmp a₂)) = Ordering.eq
⊢ e₁.oadd n₁ a₁ = e₂.oadd n₂ a₂

Tactic:
cases h
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : e₁.cmp e₂ = Ordering.gt
h : Ordering.gt.then ((_root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ)).then (a₁.cmp a₂)) = Ordering.eq
⊢ e₁.oadd n₁ a₁ = e₂.oadd n₂ a₂

Tactic:
try cases h
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : e₁.cmp e₂ = Ordering.eq
h : Ordering.eq.then ((_root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ)).then (a₁.cmp a₂)) = Ordering.eq
eq : ∀ (h₁ : e₁.cmp e₁ = Ordering.eq), e₁.oadd n₁ a₁ = e₁.oadd n₂ a₂
⊢ e₁.oadd n₁ a₁ = e₂.oadd n₂ a₂

Tactic:
obtain rfl := eq_of_cmp_eq h₁

Premises used: rfl
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h : Ordering.eq.then ((_root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ)).then (a₁.cmp a₂)) = Ordering.eq
h₁ : e₁.cmp e₁ = Ordering.eq
eq :
  ∀ (h : Ordering.eq.then ((_root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ)).then (a₁.cmp a₂)) = Ordering.eq),
    e₁.oadd n₁ a₁ = e₁.oadd n₂ a₂
⊢ e₁.oadd n₁ a₁ = e₁.oadd n₂ a₂

Tactic:
revert h
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : e₁.cmp e₁ = Ordering.eq
eq :
  ∀ (h₂ : _root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ) = Ordering.lt)
    (h : Ordering.eq.then (Ordering.lt.then (a₁.cmp a₂)) = Ordering.eq), e₁.oadd n₁ a₁ = e₁.oadd n₂ a₂
eq₁ :
  ∀ (h₂ : _root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ) = Ordering.eq)
    (h : Ordering.eq.then (Ordering.eq.then (a₁.cmp a₂)) = Ordering.eq), e₁.oadd n₁ a₁ = e₁.oadd n₂ a₂
eq₂ :
  ∀ (h₂ : _root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ) = Ordering.gt)
    (h : Ordering.eq.then (Ordering.gt.then (a₁.cmp a₂)) = Ordering.eq), e₁.oadd n₁ a₁ = e₁.oadd n₂ a₂
⊢ ∀ (h : Ordering.eq.then ((_root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ)).then (a₁.cmp a₂)) = Ordering.eq),
    e₁.oadd n₁ a₁ = e₁.oadd n₂ a₂

Tactic:
cases h₂ : _root_.cmp (n₁ : ℕ) n₂

Premises used: PNat.val, cmp
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : e₁.cmp e₁ = Ordering.eq
h₂ : _root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ) = Ordering.lt
h : Ordering.eq.then (Ordering.lt.then (a₁.cmp a₂)) = Ordering.eq
⊢ e₁.oadd n₁ a₁ = e₁.oadd n₂ a₂

Tactic:
cases h
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : e₁.cmp e₁ = Ordering.eq
h₂ : _root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ) = Ordering.lt
h : Ordering.eq.then (Ordering.lt.then (a₁.cmp a₂)) = Ordering.eq
⊢ e₁.oadd n₁ a₁ = e₁.oadd n₂ a₂

Tactic:
try cases h
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : e₁.cmp e₁ = Ordering.eq
h₂ : _root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ) = Ordering.eq
h : Ordering.eq.then (Ordering.eq.then (a₁.cmp a₂)) = Ordering.eq
⊢ e₁.oadd n₁ a₁ = e₁.oadd n₂ a₂

Tactic:
cases h
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : e₁.cmp e₁ = Ordering.eq
h₂ : _root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ) = Ordering.gt
h : Ordering.eq.then (Ordering.gt.then (a₁.cmp a₂)) = Ordering.eq
⊢ e₁.oadd n₁ a₁ = e₁.oadd n₂ a₂

Tactic:
cases h
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : e₁.cmp e₁ = Ordering.eq
h₂ : _root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ) = Ordering.gt
h : Ordering.eq.then (Ordering.gt.then (a₁.cmp a₂)) = Ordering.eq
⊢ e₁.oadd n₁ a₁ = e₁.oadd n₂ a₂

Tactic:
try cases h
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : e₁.cmp e₁ = Ordering.eq
h₂ : _root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ) = Ordering.eq
h : Ordering.eq.then (Ordering.eq.then (a₁.cmp a₂)) = Ordering.eq
eq : ∀ (h : Ordering.eq.then (Ordering.eq.then (a₁.cmp a₁)) = Ordering.eq), e₁.oadd n₁ a₁ = e₁.oadd n₂ a₁
⊢ e₁.oadd n₁ a₁ = e₁.oadd n₂ a₂

Tactic:
obtain rfl := eq_of_cmp_eq h

Premises used: rfl
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
h₁ : e₁.cmp e₁ = Ordering.eq
h₂ : _root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ) = Ordering.eq
h : Ordering.eq.then (Ordering.eq.then (a₁.cmp a₁)) = Ordering.eq
⊢ (↑n₂ : ℕ) = (↑n₁ : ℕ)

Tactic:
rw [_root_.cmp, cmpUsing_eq_eq, not_lt, not_lt, ← le_antisymm_iff] at h₂

Premises used: cmp, not_lt, le_antisymm_iff, cmpUsing_eq_eq
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
h₁ : e₁.cmp e₁ = Ordering.eq
h₂ : _root_.cmp (↑n₁ : ℕ) (↑n₂ : ℕ) = Ordering.eq
h : Ordering.eq.then (Ordering.eq.then (a₁.cmp a₁)) = Ordering.eq
h₃ : (↑n₂ : ℕ) = (↑n₁ : ℕ)
⊢ Ordering.eq.then (Ordering.eq.then (a₁.cmp a₁)) = Ordering.eq

Tactic:
rw [_root_.cmp, cmpUsing_eq_eq, not_lt, not_lt, ← le_antisymm_iff] at h₂

Premises used: cmp, not_lt, le_antisymm_iff, cmpUsing_eq_eq
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
h₁ : e₁.cmp e₁ = Ordering.eq
h₂ : (↑n₂ : ℕ) = (↑n₁ : ℕ)
h : Ordering.eq.then (Ordering.eq.then (a₁.cmp a₁)) = Ordering.eq
eq : ∀ (h₂ : (↑n₂ : ℕ) = (↑n₂ : ℕ)), e₁.oadd n₂ a₁ = e₁.oadd n₂ a₁
⊢ e₁.oadd n₁ a₁ = e₁.oadd n₂ a₁

Tactic:
obtain rfl := Subtype.ext h₂

Premises used: rfl, Subtype.ext
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ a₁ : ONote
n₂ : ℕ+
h₁ : e₁.cmp e₁ = Ordering.eq
h : Ordering.eq.then (Ordering.eq.then (a₁.cmp a₁)) = Ordering.eq
h₂ : (↑n₂ : ℕ) = (↑n₂ : ℕ)
⊢ e₁.oadd n₂ a₁ = e₁.oadd n₂ a₁

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
⊢ LT.lt (α := ONote) 0 1

Tactic:
simp only [lt_def, repr_zero, repr_one, Nat.cast_one, zero_lt_one]

Premises used: ONote.repr_one, ONote.lt_def, ONote.repr_zero, zero_lt_one, Nat.cast_one
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
⊢ NF 0

Tactic:
⟨⟨0, NFBelow.zero⟩⟩

Premises used: ONote.NFBelow.zero, Exists.intro, OfNat.ofNat, ONote.NF.mk
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a : ONote
b : Ordinal.{0}
h : (e.oadd n a).NFBelow b
oadd' : ∀ {eb : Ordinal.{0}} (h₁ : e.NFBelow eb) (h₂ : a.NFBelow e.repr) (h₃ : e.repr < b), e.NF
⊢ e.NF

Tactic:
obtain - | ⟨h₁, h₂, h₃⟩ := h
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
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:
⟨⟨_, h₁⟩⟩

Premises used: Exists.intro, ONote.NF.mk
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
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:
exact ⟨⟨_, h₁⟩⟩
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a : ONote
b : Ordinal.{0}
h : (e.oadd n a).NFBelow b
oadd' : ∀ {eb : Ordinal.{0}} (h₁ : e.NFBelow eb) (h₂ : a.NFBelow e.repr) (h₃ : e.repr < b), a.NFBelow e.repr
⊢ a.NFBelow e.repr

Tactic:
obtain - | ⟨h₁, h₂, h₃⟩ := h
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
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:
h₂
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
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:
exact h₂
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
⊢ a.NF

Tactic:
⟨⟨_, h.snd'⟩⟩

Premises used: Exists.intro, ONote.NF.snd', ONote.NF.mk
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e a : ONote
h₁ : e.NF
n : ℕ+
h₂ : a.NFBelow e.repr
⊢ (e.oadd n a).NF

Tactic:
⟨⟨_, NFBelow.oadd h₁ h₂ (lt_succ _)⟩⟩

Premises used: ONote.NFBelow.oadd, Order.lt_succ, Exists.intro, ONote.NF.mk
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
h : e.NF
⊢ (e.oadd n 0).NF

Tactic:
h.oadd _ NFBelow.zero

Premises used: ONote.NF.oadd, ONote.NFBelow.zero
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a : ONote
b : Ordinal.{0}
h : (e.oadd n a).NFBelow b
oadd' : ∀ {eb : Ordinal.{0}} (h₁ : e.NFBelow eb) (h₂ : a.NFBelow e.repr) (h₃ : e.repr < b), e.repr < b
⊢ e.repr < b

Tactic:
obtain - | ⟨h₁, h₂, h₃⟩ := h
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
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:
h₃
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
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:
exact h₃
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
e0 : e = 0
⊢ a = 0

Tactic:
simpa [e0, NFBelow_zero] using h.snd'

Premises used: ONote.NFBelow_zero, ONote.NF.snd'
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o : ONote
b b_1 : Ordinal.{0}
⊢ repr 0 < ω ^ b_1

Tactic:
opow_pos _ omega0_pos

Premises used: Ordinal.omega0_pos, Ordinal.opow_pos
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o : ONote
b b_1 : Ordinal.{0}
⊢ repr 0 < ω ^ b_1

Tactic:
exact opow_pos _ omega0_pos

Premises used: Ordinal.omega0_pos, Ordinal.opow_pos
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o : ONote
b : Ordinal.{0}
e : ONote
n : ℕ+
a : ONote
eb b_1 : Ordinal.{0}
h : e.NFBelow eb
h_1 : a.NFBelow e.repr
h₃ : e.repr < b_1
a_ih : e.repr < ω ^ eb
IH : a.repr < ω ^ e.repr
oadd' : ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + ω ^ e.repr ≤ ω ^ b_1
⊢ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + a.repr < ω ^ b_1

Tactic:
apply (add_lt_add_right IH _).trans_le

Premises used: add_lt_add_right, LT.lt.trans_le
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o : ONote
b : Ordinal.{0}
e : ONote
n : ℕ+
a : ONote
eb b_1 : Ordinal.{0}
h : e.NFBelow eb
h_1 : a.NFBelow e.repr
h₃ : e.repr < b_1
a_ih : e.repr < ω ^ eb
IH : a.repr < ω ^ e.repr
h₁ : 0 < ω
⊢ ω ^ e.repr * (↑(↑n : ℕ) : Ordinal.{0}) + ω ^ e.repr ≤ ω ^ b_1

Tactic:
grw [← mul_succ, succ_le_of_lt (natCast_lt_omega0 _), ← opow_succ, succ_le_of_lt h₃]

Premises used: Order.succ_le_of_lt, Ordinal.mul_succ, Ordinal.natCast_lt_omega0, Ordinal.opow_succ
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o : ONote
b : Ordinal.{0}
e : ONote
n : ℕ+
a : ONote
eb b_1 : Ordinal.{0}
h : e.NFBelow eb
h_1 : a.NFBelow e.repr
h₃ : e.repr < b_1
a_ih : e.repr < ω ^ eb
IH : a.repr < ω ^ e.repr
⊢ 0 < ω

Tactic:
omega0_pos

Premises used: Ordinal.omega0_pos
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o : ONote
b : Ordinal.{0}
e : ONote
n : ℕ+
a : ONote
eb b_1 : Ordinal.{0}
h : e.NFBelow eb
h_1 : a.NFBelow e.repr
h₃ : e.repr < b_1
a_ih : e.repr < ω ^ eb
IH : a.repr < ω ^ e.repr
⊢ 0 < ω

Tactic:
exact omega0_pos

Premises used: Ordinal.omega0_pos
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o : ONote
b : Ordinal.{0}
h : o.NFBelow b
zero : ∀ {b : Ordinal.{0}}, repr 0 < ω ^ b
oadd' :
  ∀ {e : ONote} {n : ℕ+} {a : ONote} {eb b : Ordinal.{0}},
    e.NFBelow eb →
      a.NFBelow e.repr → ∀ (h₃ : e.repr < b), e.repr < ω ^ eb → ∀ (IH : a.repr < ω ^ e.repr), (e.oadd n a).repr < ω ^ b
⊢ o.repr < ω ^ b

Tactic:
induction h with
  | zero => exact opow_pos _ omega0_pos
  | oadd' _ _ h₃ _ IH =>
    rw [repr]
    apply (add_lt_add_right IH _).trans_le
    grw [← mul_succ, succ_le_of_lt (natCast_lt_omega0 _), ← opow_succ, succ_le_of_lt h₃]
    exact omega0_pos

Premises used: Ordinal.omega0_pos, Order.succ_le_of_lt, Ordinal.mul_succ, ONote.NFBelow.zero, Ordinal.natCast_lt_omega0, ONote.repr, Ordinal.opow_succ, Ordinal.opow_pos, ONote.NFBelow.oadd'
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o : ONote
b₁ b₂ b : Ordinal.{0}
bb : b ≤ b₂
⊢ NFBelow 0 b₂

Tactic:
zero

Premises used: ONote.NFBelow.zero
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o : ONote
b₁ b₂ b : Ordinal.{0}
bb : b ≤ b₂
⊢ NFBelow 0 b₂

Tactic:
exact zero

Premises used: ONote.NFBelow.zero
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
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 : ∀ (bb : eb ≤ b₂), e.NFBelow b₂
a_ih_1 : ∀ (bb : e.repr ≤ b₂), a.NFBelow b₂
bb : b ≤ b₂
oadd' : e.NFBelow eb
oadd'₁ : a.NFBelow e.repr
oadd'₂ : e.repr < b₂
oadd'₃ : Ordinal.{0}
⊢ (e.oadd n a).NFBelow b₂

Tactic:
constructor
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
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 : ∀ (bb : eb ≤ b₂), e.NFBelow b₂
a_ih_1 : ∀ (bb : e.repr ≤ b₂), a.NFBelow b₂
bb : b ≤ b₂
⊢ e.NFBelow eb

Tactic:
h₁
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
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 : ∀ (bb : eb ≤ b₂), e.NFBelow b₂
a_ih_1 : ∀ (bb : e.repr ≤ b₂), a.NFBelow b₂
bb : b ≤ b₂
⊢ a.NFBelow e.repr

Tactic:
h₂
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
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 : ∀ (bb : eb ≤ b₂), e.NFBelow b₂
a_ih_1 : ∀ (bb : e.repr ≤ b₂), a.NFBelow b₂
bb : b ≤ b₂
⊢ e.repr < b₂

Tactic:
lt_of_lt_of_le h₃ bb

Premises used: lt_of_lt_of_le
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
o : ONote
b₁ b₂ : Ordinal.{0}
bb : b₁ ≤ b₂
h : o.NFBelow b₁
zero : ∀ {b : Ordinal.{0}} (bb : b ≤ b₂), NFBelow 0 b₂
oadd' :
  ∀ {e : ONote} {n : ℕ+} {a : ONote} {eb b : Ordinal.{0}} (h₁ : e.NFBelow eb) (h₂ : a.NFBelow e.repr) (h₃ : e.repr < b),
    (∀ (bb : eb ≤ b₂), e.NFBelow b₂) → (∀ (bb : e.repr ≤ b₂), a.NFBelow b₂) → ∀ (bb : b ≤ b₂), (e.oadd n a).NFBelow b₂
⊢ o.NFBelow b₂

Tactic:
induction h with
  | zero => exact zero
  | oadd' h₁ h₂ h₃ _ _ => constructor; exacts [h₁, h₂, lt_of_lt_of_le h₃ bb]

Premises used: ONote.NFBelow.zero, ONote.NFBelow.oadd'
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e : ONote
n : ℕ+
a : ONote
b : Ordinal.{0}
H : e.repr < b
b' : Ordinal.{0}
h : (e.oadd n a).NFBelow b'
oadd' : ∀ {eb : Ordinal.{0}} (h₁ : e.NFBelow eb) (h₂ : a.NFBelow e.repr) (h₃ : e.repr < b'), (e.oadd n a).NFBelow b
⊢ (e.oadd n a).NFBelow b

Tactic:
obtain - | ⟨h₁, h₂, h₃⟩ := h
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
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:
NFBelow.oadd' h₁ h₂ H

Premises used: ONote.NFBelow.oadd'
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
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

Premises used: ONote.NFBelow.oadd'
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
n : ℕ
⊢ (↑n : ONote).NF

Tactic:
⟨⟨_, nfBelow_ofNat n⟩⟩

Premises used: Exists.intro, ONote.NF.mk, ONote.nfBelow_ofNat
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
⊢ (↑1 : ONote).NF

Tactic:
infer_instance
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
e₁ : ONote
n₁ : ℕ+
o₁ e₂ : ONote
n₂ : ℕ+
o₂ : ONote
h₁ : (e₁.oadd n₁ o₁).NF
h : e₁ < e₂
⊢ e₁.oadd n₁ o₁ < e₂.oadd n₂ o₂

Tactic:
@lt_of_lt_of_le _ _ (repr (oadd e₁ n₁ o₁)) _ _
    (NF.below_of_lt h h₁).repr_lt (omega0_le_oadd e₂ n₂ o₂)

Premises used: ONote.omega0_le_oadd, ONote.NF.below_of_lt, lt_of_lt_of_le, ONote.NFBelow.repr_lt