awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a : Ordinal.{u}
ho : IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) ((fun (x : Ordinal.{u}) ↦ ω ^ x) a)
ho₂ : LT.lt.{u + 1} (α := Ordinal.{u}) 2 ((fun (x : Ordinal.{u}) ↦ ω ^ x) a)
refine_1 :
  ∀ (ho : IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) ((fun (x : Ordinal.{u}) ↦ ω ^ x) 0))
    (ho₂ : LT.lt.{u + 1} (α := Ordinal.{u}) 2 ((fun (x : Ordinal.{u}) ↦ ω ^ x) 0)),
    LE.le.{u + 1} (α := Ordinal.{u}) ((fun (x : Ordinal.{u}) ↦ ω ^ x) 0) 2 ∨
      Membership.mem (γ := Set Ordinal.{u}) (Set.range fun (x : Ordinal.{u}) ↦ ω ^ ω ^ x)
        ((fun (x : Ordinal.{u}) ↦ ω ^ x) 0)
refine_1₁ :
  ∀ (b : Ordinal.{u})
    (ho :
      IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2)
        ((fun (x : Ordinal.{u}) ↦ ω ^ x) ((fun (x : Ordinal.{u}) ↦ ω ^ x) b)))
    (ho₂ : LT.lt.{u + 1} (α := Ordinal.{u}) 2 ((fun (x : Ordinal.{u}) ↦ ω ^ x) ((fun (x : Ordinal.{u}) ↦ ω ^ x) b))),
    LE.le.{u + 1} (α := Ordinal.{u}) ((fun (x : Ordinal.{u}) ↦ ω ^ x) ((fun (x : Ordinal.{u}) ↦ ω ^ x) b)) 2 ∨
      Membership.mem (γ := Set Ordinal.{u}) (Set.range fun (x : Ordinal.{u}) ↦ ω ^ ω ^ x)
        ((fun (x : Ordinal.{u}) ↦ ω ^ x) ((fun (x : Ordinal.{u}) ↦ ω ^ x) b))
⊢ LE.le.{u + 1} (α := Ordinal.{u}) ((fun (x : Ordinal.{u}) ↦ ω ^ x) a) 2 ∨
    Membership.mem (γ := Set Ordinal.{u}) (Set.range fun (x : Ordinal.{u}) ↦ ω ^ ω ^ x)
      ((fun (x : Ordinal.{u}) ↦ ω ^ x) a)

Tactic:
rcases isPrincipal_add_iff_zero_or_omega0_opow.1
          (isPrincipal_add_of_isPrincipal_mul_opow one_lt_omega0 ho) with (rfl | ⟨b, rfl⟩)

Premises used: Ordinal.isPrincipal_add_iff_zero_or_omega0_opow, Iff.mp, Ordinal.isPrincipal_add_of_isPrincipal_mul_opow, Ordinal.one_lt_omega0, rfl
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
ho : IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) ((fun (x : Ordinal.{u}) ↦ ω ^ x) 0)
ho₂ : LT.lt.{u + 1} (α := Ordinal.{u}) 2 ((fun (x : Ordinal.{u}) ↦ ω ^ x) 0)
⊢ LE.le.{u + 1} (α := Ordinal.{u}) ((fun (x : Ordinal.{u}) ↦ ω ^ x) 0) 2 ∨
    Membership.mem (γ := Set Ordinal.{u}) (Set.range fun (x : Ordinal.{u}) ↦ ω ^ ω ^ x)
      ((fun (x : Ordinal.{u}) ↦ ω ^ x) 0)

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
b : Ordinal.{u}
ho :
  IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2)
    ((fun (x : Ordinal.{u}) ↦ ω ^ x) ((fun (x : Ordinal.{u}) ↦ ω ^ x) b))
ho₂ : LT.lt.{u + 1} (α := Ordinal.{u}) 2 ((fun (x : Ordinal.{u}) ↦ ω ^ x) ((fun (x : Ordinal.{u}) ↦ ω ^ x) b))
⊢ LE.le.{u + 1} (α := Ordinal.{u}) ((fun (x : Ordinal.{u}) ↦ ω ^ x) ((fun (x : Ordinal.{u}) ↦ ω ^ x) b)) 2 ∨
    Membership.mem (γ := Set Ordinal.{u}) (Set.range fun (x : Ordinal.{u}) ↦ ω ^ ω ^ x)
      ((fun (x : Ordinal.{u}) ↦ ω ^ x) ((fun (x : Ordinal.{u}) ↦ ω ^ x) b))

Tactic:
Or.inr ⟨b, rfl⟩

Premises used: Exists.intro, Or.inr, rfl
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
b : Ordinal.{u}
ho :
  IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2)
    ((fun (x : Ordinal.{u}) ↦ ω ^ x) ((fun (x : Ordinal.{u}) ↦ ω ^ x) b))
ho₂ : LT.lt.{u + 1} (α := Ordinal.{u}) 2 ((fun (x : Ordinal.{u}) ↦ ω ^ x) ((fun (x : Ordinal.{u}) ↦ ω ^ x) b))
⊢ LE.le.{u + 1} (α := Ordinal.{u}) ((fun (x : Ordinal.{u}) ↦ ω ^ x) ((fun (x : Ordinal.{u}) ↦ ω ^ x) b)) 2 ∨
    Membership.mem (γ := Set Ordinal.{u}) (Set.range fun (x : Ordinal.{u}) ↦ ω ^ ω ^ x)
      ((fun (x : Ordinal.{u}) ↦ ω ^ x) ((fun (x : Ordinal.{u}) ↦ ω ^ x) b))

Tactic:
exact Or.inr ⟨b, rfl⟩

Premises used: Or.inr
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u}
ho₂ : o ≤ 2
⊢ IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) o

Tactic:
isPrincipal_mul_of_le_two ho₂

Premises used: Ordinal.isPrincipal_mul_of_le_two
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u}
ho₂ : o ≤ 2
⊢ IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) o

Tactic:
exact isPrincipal_mul_of_le_two ho₂

Premises used: Ordinal.isPrincipal_mul_of_le_two
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a : Ordinal.{u}
⊢ IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) ((fun (x : Ordinal.{u}) ↦ ω ^ ω ^ x) a)

Tactic:
isPrincipal_mul_omega0_opow_opow a

Premises used: Ordinal.isPrincipal_mul_omega0_opow_opow
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a : Ordinal.{u}
⊢ IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) ((fun (x : Ordinal.{u}) ↦ ω ^ ω ^ x) a)

Tactic:
exact isPrincipal_mul_omega0_opow_opow a

Premises used: Ordinal.isPrincipal_mul_omega0_opow_opow
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a : Ordinal.{u}
a0 : 0 < a
ha : a < ω
b : Ordinal.{u}
rw : a * ω * b = ω * b
rw₁ rw₂ : ω * b = ω * b
⊢ a * (ω * b) = ω * b

Tactic:
rw [← mul_assoc, mul_omega0 a0 ha]

Premises used: mul_assoc, Ordinal.mul_omega0
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a b : Ordinal.{u}
ha : a ≠ 0
hb : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) b
hb₂ : 2 < b
a₁ : a * b ≤ b ^ succ (log b a)
a₂ : b ^ succ (log b a) ≤ a * b
⊢ a * b = b ^ succ (log b a)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a b : Ordinal.{u}
ha : a ≠ 0
hb : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) b
hb₂ : 2 < b
⊢ IsSuccLimit b

Tactic:
have hbl := isSuccLimit_of_isPrincipal_mul hb₂ hb
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a b : Ordinal.{u}
ha : a ≠ 0
hb : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) b
hb₂ : 2 < b
hbl : IsSuccLimit b
a₁ : ∀ (i : (↑(Set.Iio b) : Type (u + 1))), a * (↑i : Ordinal.{u}) ≤ b ^ succ (log b a)
⊢ a * b ≤ b ^ succ (log b a)

Tactic:
rw [(isNormal_mul_right (pos_iff_ne_zero.2 ha)).apply_of_isSuccLimit hbl,
      Ordinal.iSup_le_iff]

Premises used: Order.IsNormal.apply_of_isSuccLimit, Iff.mpr, Ordinal.isNormal_mul_right, Ordinal.iSup_le_iff, pos_iff_ne_zero
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a b : Ordinal.{u}
ha : a ≠ 0
hb : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) b
hb₂ : 2 < b
hbl : IsSuccLimit b
c : Ordinal.{u}
hcb : c ∈ Set.Iio b
⊢ 1 < b

Tactic:
have hb₁ : 1 < b := one_lt_two.trans hb₂
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a b : Ordinal.{u}
ha : a ≠ 0
hb : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) b
hb₂ : 2 < b
hbl : IsSuccLimit b
c : Ordinal.{u}
hcb : c ∈ Set.Iio b
hb₁ : 1 < b
⊢ b ^ log b a ≠ 0

Tactic:
have hbo₀ : b ^ log b a ≠ 0 := pos_iff_ne_zero.1 (opow_pos _ (zero_lt_one.trans hb₁))
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a b : Ordinal.{u}
ha : a ≠ 0
hb : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) b
hb₂ : 2 < b
hbl : IsSuccLimit b
c : Ordinal.{u}
hcb : c ∈ Set.Iio b
hb₁ : 1 < b
hbo₀ : b ^ log b a ≠ 0
a₁ : b ^ log b a * succ (a / b ^ log b a) * c ≤ b ^ succ (log b a)
⊢ a * (↑(Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Set.Iio b) c hcb) : Ordinal.{u}) ≤ b ^ succ (log b a)

Tactic:
apply (mul_le_mul_left (le_of_lt (lt_mul_succ_div a hbo₀)) c).trans

Premises used: Ordinal.lt_mul_succ_div, le_of_lt, mul_le_mul_left, LE.le.trans
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a b : Ordinal.{u}
ha : a ≠ 0
hb : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) b
hb₂ : 2 < b
hbl : IsSuccLimit b
c : Ordinal.{u}
hcb : c ∈ Set.Iio b
hb₁ : 1 < b
hbo₀ : b ^ log b a ≠ 0
a₁ : b ^ log b a * (succ (a / b ^ log b a) * c) ≤ b ^ log b a * b
⊢ b ^ log b a * succ (a / b ^ log b a) * c ≤ b ^ succ (log b a)

Tactic:
rw [mul_assoc, opow_succ]

Premises used: mul_assoc, Ordinal.opow_succ
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a b : Ordinal.{u}
ha : a ≠ 0
hb : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) b
hb₂ : 2 < b
hbl : IsSuccLimit b
c : Ordinal.{u}
hcb : c ∈ Set.Iio b
hb₁ : 1 < b
hbo₀ : b ^ log b a ≠ 0
a₁ : succ (a / b ^ log b a) * c ≤ b
⊢ b ^ log b a * (succ (a / b ^ log b a) * c) ≤ b ^ log b a * b

Tactic:
gcongr
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a b : Ordinal.{u}
ha : a ≠ 0
hb : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) b
hb₂ : 2 < b
hbl : IsSuccLimit b
c : Ordinal.{u}
hcb : c ∈ Set.Iio b
hb₁ : 1 < b
hbo₀ : b ^ log b a ≠ 0
⊢ succ (a / b ^ log b a) * c ≤ b

Tactic:
(hb (hbl.succ_lt ?_) hcb).le

Premises used: LT.lt.le, Order.IsSuccLimit.succ_lt
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a b : Ordinal.{u}
ha : a ≠ 0
hb : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) b
hb₂ : 2 < b
hbl : IsSuccLimit b
c : Ordinal.{u}
hcb : c ∈ Set.Iio b
hb₁ : 1 < b
hbo₀ : b ^ log b a ≠ 0
a₁ : a / b ^ log b a < b
⊢ succ (a / b ^ log b a) * c ≤ b

Tactic:
refine (hb (hbl.succ_lt ?_) hcb).le

Premises used: LT.lt.le, Order.IsSuccLimit.succ_lt
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a b : Ordinal.{u}
ha : a ≠ 0
hb : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) b
hb₂ : 2 < b
hbl : IsSuccLimit b
c : Ordinal.{u}
hcb : c ∈ Set.Iio b
hb₁ : 1 < b
hbo₀ : b ^ log b a ≠ 0
a₁ : a < b ^ succ (log b a)
⊢ a / b ^ log b a < b

Tactic:
rw [← lt_mul_iff_div_lt hbo₀, ← opow_succ]

Premises used: Ordinal.lt_mul_iff_div_lt, Ordinal.opow_succ
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a b : Ordinal.{u}
ha : a ≠ 0
hb : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) b
hb₂ : 2 < b
hbl : IsSuccLimit b
c : Ordinal.{u}
hcb : c ∈ Set.Iio b
hb₁ : 1 < b
hbo₀ : b ^ log b a ≠ 0
⊢ a < b ^ succ (log b a)

Tactic:
lt_opow_succ_log_self hb₁ _

Premises used: Ordinal.lt_opow_succ_log_self
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a b : Ordinal.{u}
ha : a ≠ 0
hb : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) b
hb₂ : 2 < b
hbl : IsSuccLimit b
c : Ordinal.{u}
hcb : c ∈ Set.Iio b
hb₁ : 1 < b
hbo₀ : b ^ log b a ≠ 0
⊢ a < b ^ succ (log b a)

Tactic:
exact lt_opow_succ_log_self hb₁ _

Premises used: Ordinal.lt_opow_succ_log_self
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a b : Ordinal.{u}
ha : a ≠ 0
hb : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 * x2) b
hb₂ : 2 < b
a₁ : b ^ log b a * b ≤ a * b
a₂ a₃ : a * b ≤ a * b
⊢ b ^ succ (log b a) ≤ a * b

Tactic:
grw [opow_succ, opow_log_le_self b ha]

Premises used: Ordinal.opow_log_le_self, Ordinal.opow_succ
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a b : Ordinal.{u_1}
m n : ℕ
ha : (↑m : Ordinal.{u_1}) < ω
hb : (↑n : Ordinal.{u_1}) < ω
⊢ (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 ^ x2) (↑m : Ordinal.{u_1}) (↑n : Ordinal.{u_1}) < ω

Tactic:
simp [← natCast_pow]

Premises used: Ordinal.natCast_pow
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a : Ordinal.{u}
a1 : 1 < a
h : a < ω
⊢ a ^ ω = ω

Tactic:
((opow_le_of_isSuccLimit (one_le_iff_ne_zero.1 <| le_of_lt a1) isSuccLimit_omega0).2 fun _ hb =>
      (isPrincipal_opow_omega0 h hb).le).antisymm
  (right_le_opow _ a1)

Premises used: Iff.mpr, Ordinal.isSuccLimit_omega0, Ordinal.right_le_opow, le_of_lt, LE.le.antisymm, LT.lt.le, Ordinal.isPrincipal_opow_omega0, Order.one_le_iff_ne_zero, Iff.mp, Ordinal.opow_le_of_isSuccLimit
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
n : ℕ
hn : 1 < n
⊢ HPow.hPow (α := Ordinal.{u_1}) (↑n : Ordinal.{u_1}) ω = ω

Tactic:
opow_omega0 (mod_cast hn) (natCast_lt_omega0 n)

Premises used: Ordinal.opow_omega0, congrArg, Nat.cast_lt._simp_1, cast, Nat.cast, Ordinal.natCast_lt_omega0, LT.lt, congrFun', Eq.symm, Nat.cast_one, Eq.trans
-- Module: Mathlib.SetTheory.Ordinal.Rank
Goal:
α : Type u
a : α
r : α → α → Prop
h : Acc r a
⊢ rank (r := fun (x : α) ↦ r x) ⋯ = ⨆ (b : { b : α // r b a }), Order.succ (⋯.rank (r := r))

Tactic:
rfl
-- Module: Mathlib.SetTheory.Ordinal.Rank
Goal:
α : Type u
a b : α
r : α → α → Prop
hb : Acc r b
h : r a b
rw : Order.succ (⋯.rank (r := r)) ≤ ⨆ (b_1 : { b_1 : α // r b_1 b }), Order.succ (⋯.rank (r := r))
⊢ Order.succ (⋯.rank (r := r)) ≤ hb.rank (r := r)

Tactic:
rw [hb.rank_eq]

Premises used: Acc.rank_eq
-- Module: Mathlib.SetTheory.Ordinal.Rank
Goal:
α : Type u
a b : α
r : α → α → Prop
hb : Acc r b
h : r a b
⊢ Order.succ (⋯.rank (r := r)) ≤ ⨆ (b_1 : { b_1 : α // r b_1 b }), Order.succ (⋯.rank (r := r))

Tactic:
Ordinal.le_iSup _ (⟨a, h⟩ : {a // r a b})

Premises used: Subtype.mk, Ordinal.le_iSup
-- Module: Mathlib.SetTheory.Ordinal.Rank
Goal:
α : Type u
a b : α
r : α → α → Prop
hb : Acc r b
h : r a b
⊢ Order.succ (⋯.rank (r := r)) ≤ ⨆ (b_1 : { b_1 : α // r b_1 b }), Order.succ (⋯.rank (r := r))

Tactic:
exact Ordinal.le_iSup _ (⟨a, h⟩ : {a // r a b})

Premises used: Subtype.mk, Ordinal.le_iSup
-- Module: Mathlib.SetTheory.Ordinal.Rank
Goal:
α : Type u
a : α
r : α → α → Prop
o : Ordinal.{u}
ha : Acc r a
ho : o ≤ ha.rank (r := r)
inl : ∀ (ho : ha.rank (r := r) ≤ ha.rank (r := r)), ∃ (b : α) (hb : Acc r b), hb.rank (r := r) = ha.rank (r := r)
inr : ∀ (ho : o < ha.rank (r := r)), ∃ (b : α) (hb : Acc r b), hb.rank (r := r) = o
⊢ ∃ (b : α) (hb : Acc r b), hb.rank (r := r) = o

Tactic:
obtain rfl | ho := ho.eq_or_lt

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.SetTheory.Ordinal.Rank
Goal:
α : Type u
a : α
r : α → α → Prop
ha : Acc r a
ho : ha.rank (r := r) ≤ ha.rank (r := r)
⊢ ∃ (b : α) (hb : Acc r b), hb.rank (r := r) = ha.rank (r := r)

Tactic:
⟨a, ha, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.SetTheory.Ordinal.Rank
Goal:
α : Type u
a : α
r : α → α → Prop
ha : Acc r a
ho : ha.rank (r := r) ≤ ha.rank (r := r)
⊢ ∃ (b : α) (hb : Acc r b), hb.rank (r := r) = ha.rank (r := r)

Tactic:
exact ⟨a, ha, rfl⟩
-- Module: Mathlib.SetTheory.Ordinal.Rank
Goal:
α : Type u
a : α
r : α → α → Prop
o : Ordinal.{u}
ha : Acc r a
ho_1 : o ≤ ha.rank (r := r)
ho : o < ha.rank (r := r)
inr : ∀ (ho : o < ha.rank (r := r)), ∃ (b : α) (hb : Acc r b), hb.rank (r := r) = o
⊢ ∃ (b : α) (hb : Acc r b), hb.rank (r := r) = o

Tactic:
revert ho
-- Module: Mathlib.SetTheory.Ordinal.Rank
Goal:
α : Type u
a : α
r : α → α → Prop
o : Ordinal.{u}
ha : Acc r a
ho : o ≤ ha.rank (r := r)
⊢ ∀ (ho : o < ha.rank (r := r)), ∃ (b : α) (hb : Acc r b), hb.rank (r := r) = o

Tactic:
ha.recOn fun a ha IH ho ↦ ?_

Premises used: Acc.recOn
-- Module: Mathlib.SetTheory.Ordinal.Rank
Goal:
α : Type u
a : α
r : α → α → Prop
o : Ordinal.{u}
ha : Acc r a
ho : o ≤ ha.rank (r := r)
inr :
  ∀ (a : α) (ha : ∀ (y : α), r y a → Acc r y)
    (IH : ∀ (y : α) (a : r y a) (ho : o < ⋯.rank (r := r)), ∃ (b : α) (hb : Acc r b), hb.rank (r := r) = o)
    (ho : o < ⋯.rank (r := r)), ∃ (b : α) (hb : Acc r b), hb.rank (r := r) = o
⊢ ∀ (ho : o < ha.rank (r := r)), ∃ (b : α) (hb : Acc r b), hb.rank (r := r) = o

Tactic:
refine ha.recOn fun a ha IH ho ↦ ?_
-- Module: Mathlib.SetTheory.Ordinal.Rank
Goal:
α : Type u
a_1 : α
r : α → α → Prop
o : Ordinal.{u}
ha_1 : Acc r a_1
ho_1 : o ≤ ha_1.rank (r := r)
a : α
ha : ∀ (y : α), r y a → Acc r y
IH : ∀ (y : α) (a : r y a) (ho : o < ⋯.rank (r := r)), ∃ (b : α) (hb : Acc r b), hb.rank (r := r) = o
ho : o < ⋯.rank (r := r)
⊢ ∃ (i : { b : α // r b a }), o < Order.succ (⋯.rank (r := r))

Tactic:
rw [rank_eq, Ordinal.lt_iSup_iff] at ho

Premises used: Acc.rank_eq, Ordinal.lt_iSup_iff
-- Module: Mathlib.SetTheory.Ordinal.Rank
Goal:
α : Type u
a_1 : α
r : α → α → Prop
o : Ordinal.{u}
ha_1 : Acc r a_1
ho_1 : o ≤ ha_1.rank (r := r)
a : α
ha : ∀ (y : α), r y a → Acc r y
IH : ∀ (y : α) (a : r y a) (ho : o < ⋯.rank (r := r)), ∃ (b : α) (hb : Acc r b), hb.rank (r := r) = o
ho : ∃ (i : { b : α // r b a }), o < Order.succ (⋯.rank (r := r))
inr :
  ∀ (b : α) (hb : r b a)
    (ho : o < Order.succ (rank (a := (↑(Subtype.mk (p := fun (b : α) ↦ r b a) b hb) : α)) (r := r) ⋯)),
    ∃ (b : α) (hb : Acc r b), hb.rank (r := r) = o
⊢ ∃ (b : α) (hb : Acc r b), hb.rank (r := r) = o

Tactic:
obtain ⟨⟨b, hb⟩, ho⟩ := ho
-- Module: Mathlib.SetTheory.Ordinal.Rank
Goal:
α : Type u
a_1 : α
r : α → α → Prop
o : Ordinal.{u}
ha_1 : Acc r a_1
ho_1 : o ≤ ha_1.rank (r := r)
a : α
ha : ∀ (y : α), r y a → Acc r y
IH : ∀ (y : α) (a : r y a) (ho : o < ⋯.rank (r := r)), ∃ (b : α) (hb : Acc r b), hb.rank (r := r) = o
b : α
hb : r b a
ho : o < Order.succ (rank (a := (↑(Subtype.mk (p := fun (b : α) ↦ r b a) b hb) : α)) (r := r) ⋯)
⊢ o ≤ rank (a := (↑(Subtype.mk (p := fun (b : α) ↦ r b a) b hb) : α)) (r := r) ⋯

Tactic:
rw [Order.lt_succ_iff] at ho

Premises used: Order.lt_succ_iff
-- Module: Mathlib.SetTheory.Ordinal.Rank
Goal:
α : Type u
a_1 : α
r : α → α → Prop
o : Ordinal.{u}
ha_1 : Acc r a_1
ho_1 : o ≤ ha_1.rank (r := r)
a : α
ha : ∀ (y : α), r y a → Acc r y
IH : ∀ (y : α) (a : r y a) (ho : o < ⋯.rank (r := r)), ∃ (b : α) (hb : Acc r b), hb.rank (r := r) = o
b : α
hb : r b a
ho : o ≤ rank (a := (↑(Subtype.mk (p := fun (b : α) ↦ r b a) b hb) : α)) (r := r) ⋯
inr :
  ∀ (ho : rank (a := (↑(Subtype.mk (p := fun (b : α) ↦ r b a) b hb) : α)) (r := r) ⋯ ≤ ha_1.rank (r := r))
    (IH :
      ∀ (y : α) (a_2 : r y a)
        (ho : rank (a := (↑(Subtype.mk (p := fun (b : α) ↦ r b a) b hb) : α)) (r := r) ⋯ < ⋯.rank (r := r)),
        ∃ (b_1 : α) (hb_1 : Acc r b_1),
          hb_1.rank (r := r) = rank (a := (↑(Subtype.mk (p := fun (b : α) ↦ r b a) b hb) : α)) (r := r) ⋯)
    (ho :
      rank (a := (↑(Subtype.mk (p := fun (b : α) ↦ r b a) b hb) : α)) (r := r) ⋯ ≤
        rank (a := (↑(Subtype.mk (p := fun (b : α) ↦ r b a) b hb) : α)) (r := r) ⋯),
    ∃ (b_1 : α) (hb_1 : Acc r b_1),
      hb_1.rank (r := r) = rank (a := (↑(Subtype.mk (p := fun (b : α) ↦ r b a) b hb) : α)) (r := r) ⋯
inr₁ :
  ∀ (ho : o < rank (a := (↑(Subtype.mk (p := fun (b : α) ↦ r b a) b hb) : α)) (r := r) ⋯),
    ∃ (b : α) (hb : Acc r b), hb.rank (r := r) = o
⊢ ∃ (b : α) (hb : Acc r b), hb.rank (r := r) = o

Tactic:
obtain rfl | ho := ho.eq_or_lt

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.SetTheory.Ordinal.Rank
Goal:
α : Type u
a_1 : α
r : α → α → Prop
ha_1 : Acc r a_1
a : α
ha : ∀ (y : α), r y a → Acc r y
b : α
hb : r b a
ho_1 : rank (a := (↑(Subtype.mk (p := fun (b : α) ↦ r b a) b hb) : α)) (r := r) ⋯ ≤ ha_1.rank (r := r)
IH :
  ∀ (y : α) (a_2 : r y a)
    (ho : rank (a := (↑(Subtype.mk (p := fun (b : α) ↦ r b a) b hb) : α)) (r := r) ⋯ < ⋯.rank (r := r)),
    ∃ (b_1 : α) (hb_1 : Acc r b_1),
      hb_1.rank (r := r) = rank (a := (↑(Subtype.mk (p := fun (b : α) ↦ r b a) b hb) : α)) (r := r) ⋯
ho :
  rank (a := (↑(Subtype.mk (p := fun (b : α) ↦ r b a) b hb) : α)) (r := r) ⋯ ≤
    rank (a := (↑(Subtype.mk (p := fun (b : α) ↦ r b a) b hb) : α)) (r := r) ⋯
⊢ ∃ (b_1 : α) (hb_1 : Acc r b_1),
    hb_1.rank (r := r) = rank (a := (↑(Subtype.mk (p := fun (b : α) ↦ r b a) b hb) : α)) (r := r) ⋯

Tactic:
⟨b, ha b hb, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.SetTheory.Ordinal.Rank
Goal:
α : Type u
a_1 : α
r : α → α → Prop
o : Ordinal.{u}
ha_1 : Acc r a_1
ho_1 : o ≤ ha_1.rank (r := r)
a : α
ha : ∀ (y : α), r y a → Acc r y
IH : ∀ (y : α) (a : r y a) (ho : o < ⋯.rank (r := r)), ∃ (b : α) (hb : Acc r b), hb.rank (r := r) = o
b : α
hb : r b a
ho_2 : o ≤ rank (a := (↑(Subtype.mk (p := fun (b : α) ↦ r b a) b hb) : α)) (r := r) ⋯
ho : o < rank (a := (↑(Subtype.mk (p := fun (b : α) ↦ r b a) b hb) : α)) (r := r) ⋯
⊢ ∃ (b : α) (hb : Acc r b), hb.rank (r := r) = o

Tactic:
IH _ hb ho
-- Module: Mathlib.SetTheory.Ordinal.Rank
Goal:
α : Type u
a_1 : α
r : α → α → Prop
ha_1 : Acc r a_1
a : α
ha : ∀ (y : α), r y a → Acc r y
b : α
hb : r b a
ho_1 : rank (a := (↑(Subtype.mk (p := fun (b : α) ↦ r b a) b hb) : α)) (r := r) ⋯ ≤ ha_1.rank (r := r)
IH :
  ∀ (y : α) (a_2 : r y a)
    (ho : rank (a := (↑(Subtype.mk (p := fun (b : α) ↦ r b a) b hb) : α)) (r := r) ⋯ < ⋯.rank (r := r)),
    ∃ (b_1 : α) (hb_1 : Acc r b_1),
      hb_1.rank (r := r) = rank (a := (↑(Subtype.mk (p := fun (b : α) ↦ r b a) b hb) : α)) (r := r) ⋯
ho :
  rank (a := (↑(Subtype.mk (p := fun (b : α) ↦ r b a) b hb) : α)) (r := r) ⋯ ≤
    rank (a := (↑(Subtype.mk (p := fun (b : α) ↦ r b a) b hb) : α)) (r := r) ⋯
⊢ ∃ (b_1 : α) (hb_1 : Acc r b_1),
    hb_1.rank (r := r) = rank (a := (↑(Subtype.mk (p := fun (b : α) ↦ r b a) b hb) : α)) (r := r) ⋯

Tactic:
exacts [⟨b, ha b hb, rfl⟩, IH _ hb ho]
-- Module: Mathlib.SetTheory.Ordinal.Rank
Goal:
α : Type u
r : α → α → Prop
hwf : IsWellFounded α r
a : α
⊢ rank r a = ⨆ (b : { b : α // r b a }), Order.succ (rank r (↑b : α))

Tactic:
(hwf.apply r a).rank_eq

Premises used: Acc.rank_eq, IsWellFounded.apply, IsWellFounded.rank
-- Module: Mathlib.SetTheory.Ordinal.Rank
Goal:
α : Type u
a b : α
r : α → α → Prop
hwf : IsWellFounded α r
h : r a b
⊢ rank r a < rank r b

Tactic:
Acc.rank_lt_of_rel _ h

Premises used: Acc.rank_lt_of_rel, IsWellFounded.rank
-- Module: Mathlib.SetTheory.Ordinal.Rank
Goal:
α : Type u
a : α
r : α → α → Prop
hwf : IsWellFounded α r
o : Ordinal.{u}
h : o ≤ rank r a
obtain : ∀ (b : α) (hb : Acc r b) (h : hb.rank (r := r) ≤ rank r a), hb.rank (r := r) ∈ Set.range (rank r)
⊢ o ∈ Set.range (rank r)

Tactic:
obtain ⟨b, hb, rfl⟩ := Acc.mem_range_rank_of_le (hwf.apply r a) h

Premises used: IsWellFounded.apply, Acc.mem_range_rank_of_le, rfl
-- Module: Mathlib.SetTheory.Ordinal.Rank
Goal:
α : Type u
a : α
r : α → α → Prop
hwf : IsWellFounded α r
b : α
hb : Acc r b
h : hb.rank (r := r) ≤ rank r a
⊢ hb.rank (r := r) ∈ Set.range (rank r)

Tactic:
⟨b, rfl⟩

Premises used: Set.Mem, setOf, Exists.intro, Set.range, rfl
-- Module: Mathlib.SetTheory.Ordinal.Rank
Goal:
α : Type u
a : α
r : α → α → Prop
hwf : IsWellFounded α r
b : α
hb : Acc r b
h : hb.rank (r := r) ≤ rank r a
⊢ hb.rank (r := r) ∈ Set.range (rank r)

Tactic:
exact ⟨b, rfl⟩
-- Module: Mathlib.SetTheory.Ordinal.Rank
Goal:
α : Type u
inst : Preorder α
inst_1 : WellFoundedLT α
⊢ StrictMono.{u, u + 1} (α := α) (IsWellFounded.rank fun (x1 x2 : α) ↦ x1 < x2)

Tactic:
fun _ _ => IsWellFounded.rank_lt_of_rel

Premises used: StrictMono, IsWellFounded.rank_lt_of_rel
-- Module: Mathlib.SetTheory.Ordinal.Rank
Goal:
α : Type u
inst : Preorder α
inst_1 : WellFoundedGT α
⊢ StrictAnti.{u, u + 1} (α := α) (IsWellFounded.rank fun (x1 x2 : α) ↦ x1 > x2)

Tactic:
fun _ _ a => IsWellFounded.rank_lt_of_rel a

Premises used: IsWellFounded.rank_lt_of_rel, StrictAnti
-- Module: Mathlib.SetTheory.Ordinal.Rank
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
this : LinearOrder α := linearOrderOfSTO r
h :
  ∀ (a : α),
    rank r a =
      ((Ordinal.typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) : (a : α) → Ordinal.{u}) a
⊢ rank r =
    (⇑((Ordinal.typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)) : (a : α) → Ordinal.{u})

Tactic:
ext a
-- Module: Mathlib.SetTheory.Ordinal.Rank
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
this : LinearOrder α := linearOrderOfSTO r
a : α
⊢ rank r a =
    ((Ordinal.typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) : (a : α) → Ordinal.{u}) a

Tactic:
InitialSeg.eq (⟨(OrderEmbedding.ofStrictMono _ WellFoundedLT.rank_strictMono).ltEmbedding,
    fun a b h ↦ mem_range_rank_of_le h.le⟩) (Ordinal.typein r) a

Premises used: Acc.rank, LT.lt.le, OrderEmbedding.ltEmbedding, WellFoundedLT.rank_strictMono, OrderEmbedding.ofStrictMono, IsWellFounded.mem_range_rank_of_le, InitialSeg.mk, IsWellFounded.rank, InitialSeg.eq
-- Module: Mathlib.SetTheory.Ordinal.Rank
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
this : LinearOrder α := linearOrderOfSTO r
a : α
⊢ rank r a =
    ((Ordinal.typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) : (a : α) → Ordinal.{u}) a

Tactic:
exact InitialSeg.eq (⟨(OrderEmbedding.ofStrictMono _ WellFoundedLT.rank_strictMono).ltEmbedding,
    fun a b h ↦ mem_range_rank_of_le h.le⟩) (Ordinal.typein r) a

Premises used: LT.lt.le, OrderEmbedding.ltEmbedding, WellFoundedLT.rank_strictMono, OrderEmbedding.ofStrictMono, IsWellFounded.mem_range_rank_of_le, InitialSeg.mk, InitialSeg.eq
-- Module: Mathlib.SetTheory.Ordinal.Rank
Goal:
α : Type u
r : α → α → Prop
inst : IsWellOrder α r
letI letI₁ letI₂ :
  rank r =
    (⇑((Ordinal.typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)) : (a : α) → Ordinal.{u})
h :
  ∀ (a : α),
    rank r a =
      ((Ordinal.typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2) : (a : α) → Ordinal.{u}) a
⊢ rank r =
    (⇑((Ordinal.typein r).toRelEmbedding (r := r) (s := fun (x1 x2 : Ordinal.{u}) ↦ x1 < x2)) : (a : α) → Ordinal.{u})

Tactic:
classical
  letI := linearOrderOfSTO r
  ext a
  exact InitialSeg.eq (⟨(OrderEmbedding.ofStrictMono _ WellFoundedLT.rank_strictMono).ltEmbedding,
    fun a b h ↦ mem_range_rank_of_le h.le⟩) (Ordinal.typein r) a
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
s : Set Ordinal.{u}
a : Ordinal.{u}
⊢ OrderTopology Ordinal.{u}

Tactic:
⟨rfl⟩

Premises used: OrderTopology.mk, rfl
-- Module: Mathlib.SetTheory.Ordinal.Topology
Goal:
a : Ordinal.{u}
⊢ IsOpen (X := Ordinal.{u}) {a} ↔ ¬IsSuccLimit a

Tactic:
SuccOrder.isOpen_singleton_iff

Premises used: SuccOrder.isOpen_singleton_iff