awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
a : Ordinal.{u_1}
f : (↑(Iio a) : Type (u_1 + 1)) → Ordinal.{u_1}
hf : StrictMono f
⊢ cof (⨆ (i : (↑(Iio a) : Type (u_1 + 1))), f i + 1) = a.cof

Tactic:
simpa [← lift_cof] using lift_cof_iSup_add_one hf

Premises used: Ordinal.lift_cof_iSup_add_one, Ordinal.lift_cof
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
a : Ordinal.{u_1}
f : (↑(Iio a) : Type (u_1 + 1)) → Ordinal.{u_1}
hf : StrictMono f
ha : IsSuccPrelimit a
rw : cof (⨆ (i : (↑(Iio a) : Type (u_1 + 1))), f i + 1) = a.cof
rw₁ rw₂ : a.cof = a.cof
⊢ cof (⨆ (i : (↑(Iio a) : Type (u_1 + 1))), f i) = a.cof

Tactic:
rw [← iSup_Iio_add_one hf ha, cof_iSup_Iio_add_one hf]

Premises used: Ordinal.cof_iSup_Iio_add_one, Ordinal.iSup_Iio_add_one
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
f : Ordinal.{u_1} → Ordinal.{u_1}
hf : IsNormal f
a : Ordinal.{u_1}
ha : IsSuccLimit a
rw : StrictMono (β := Ordinal.{u_1}) fun (b : (↑(Iio a) : Type (u_1 + 1))) ↦ f (↑b : Ordinal.{u_1})
⊢ (f a).cof = a.cof

Tactic:
rw [hf.apply_of_isSuccLimit ha, cof_iSup_Iio _ ha.isSuccPrelimit]

Premises used: Order.IsNormal.apply_of_isSuccLimit, Ordinal.cof_iSup_Iio, Order.IsSuccLimit.isSuccPrelimit
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
f : Ordinal.{u_1} → Ordinal.{u_1}
hf : IsNormal f
a : Ordinal.{u_1}
ha : IsSuccLimit a
⊢ StrictMono (β := Ordinal.{u_1}) fun (b : (↑(Iio a) : Type (u_1 + 1))) ↦ f (↑b : Ordinal.{u_1})

Tactic:
hf.strictMono.comp <| Subtype.strictMono_coe _

Premises used: StrictMono.comp, Order.IsNormal.strictMono, Subtype.strictMono_coe
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
f : Ordinal.{u_1} → Ordinal.{u_1}
hf : IsNormal f
a : Ordinal.{u_1}
ha : IsSuccLimit a
⊢ StrictMono (β := Ordinal.{u_1}) fun (b : (↑(Iio a) : Type (u_1 + 1))) ↦ f (↑b : Ordinal.{u_1})

Tactic:
exact hf.strictMono.comp <| Subtype.strictMono_coe _

Premises used: StrictMono.comp, Order.IsNormal.strictMono, Subtype.strictMono_coe
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
f : Ordinal.{u_1} → Ordinal.{u_1}
hf : IsNormal f
⊢ cof 0 ≤ (f 0).cof

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
f : Ordinal.{u_1} → Ordinal.{u_1}
hf : IsNormal f
a : Ordinal.{u_1}
h : ∀ (h : a + 1 = a), (a + 1).cof ≤ (f (a + 1)).cof
add_one : f (a + 1) ≠ 0
⊢ (a + 1).cof ≤ (f (a + 1)).cof

Tactic:
rw [cof_add_one, Cardinal.one_le_iff_ne_zero, cof_eq_zero.ne]

Premises used: Ordinal.cof_add_one, Cardinal.one_le_iff_ne_zero, Iff.ne, Ordinal.cof_eq_zero
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
f : Ordinal.{u_1} → Ordinal.{u_1}
hf : IsNormal f
a : Ordinal.{u_1}
h : ∀ (h : a + 1 = a), (a + 1).cof ≤ (f (a + 1)).cof
⊢ f (a + 1) ≠ 0

Tactic:
(hf.strictMono (lt_succ a)).ne_zero

Premises used: Order.succ, Order.lt_succ, Order.IsNormal.strictMono, LT.lt.ne_zero
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
f : Ordinal.{u_1} → Ordinal.{u_1}
hf : IsNormal f
a : Ordinal.{u_1}
h : ∀ (h : a + 1 = a), (a + 1).cof ≤ (f (a + 1)).cof
⊢ f (a + 1) ≠ 0

Tactic:
exact (hf.strictMono (lt_succ a)).ne_zero

Premises used: Order.lt_succ, Order.IsNormal.strictMono, LT.lt.ne_zero
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
f : Ordinal.{u_1} → Ordinal.{u_1}
hf : IsNormal f
a : Ordinal.{u_1}
ha : IsSuccLimit a
h : ∀ o' < a, ∀ (h : a = o'), a.cof ≤ (f a).cof
limit limit₁ : a.cof ≤ a.cof
⊢ a.cof ≤ (f a).cof

Tactic:
rw [cof_map_of_isNormal hf ha]

Premises used: Ordinal.cof_map_of_isNormal
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
f : Ordinal.{u_1} → Ordinal.{u_1}
hf : IsNormal f
a : Ordinal.{u_1}
zero : cof 0 ≤ (f 0).cof
add_one : ∀ (a : Ordinal.{u_1}), (∀ (h : a + 1 = a), (a + 1).cof ≤ (f (a + 1)).cof) → (a + 1).cof ≤ (f (a + 1)).cof
limit : ∀ (ha : IsSuccLimit a), (∀ o' < a, ∀ (h : a = o'), a.cof ≤ (f a).cof) → a.cof ≤ (f a).cof
⊢ a.cof ≤ (f a).cof

Tactic:
cases a using limitRecOn with
  | zero => simp
  | add_one a =>
    rw [cof_add_one, Cardinal.one_le_iff_ne_zero, cof_eq_zero.ne]
    exact (hf.strictMono (lt_succ a)).ne_zero
  | limit a ha => rw [cof_map_of_isNormal hf ha]

Premises used: Ordinal.cof_add_one, Cardinal.one_le_iff_ne_zero, Order.lt_succ, Ordinal.zero, Iff.ne, Ordinal.cof_eq_zero, Order.IsNormal.strictMono, LT.lt.ne_zero
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
s : Set Ordinal.{u}
a : Ordinal.{u}
ha : #(↑s : Type (u + 1)) < (lift.{u + 1, u} a).cof
hs : ∀ i ∈ s, i < a
f : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2)) ≃o (↑s : Type (u + 1)) :=
  OrderIso.ofRelIsoLT (enum fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)
⊢ Small.{u, u + 2} (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))

Tactic:
small_of_injective (β := Iio a) (f := fun x ↦ ⟨f x, hs _ (f x).2⟩) fun _ ↦ ?_

Premises used: small_of_injective
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
s : Set Ordinal.{u}
a : Ordinal.{u}
ha : #(↑s : Type (u + 1)) < (lift.{u + 1, u} a).cof
hs : ∀ i ∈ s, i < a
f : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2)) ≃o (↑s : Type (u + 1)) :=
  OrderIso.ofRelIsoLT (enum fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)
refine :
  ∀ (x : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2)))
    ⦃a₂ : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))⦄,
    Eq.{u + 2} (α := (↑(Iio a) : Type (u + 1)))
        ((fun (x : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) ↦
            (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio a)
                (↑((f :
                        (a : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) →
                          (↑s : Type (u + 1)))
                      x) :
                  Ordinal.{u})
                ⋯ :
              { x : Ordinal.{u} // x ∈ Iio a }))
          x)
        ((fun (x : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) ↦
            (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio a)
                (↑((f :
                        (a : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) →
                          (↑s : Type (u + 1)))
                      x) :
                  Ordinal.{u})
                ⋯ :
              { x : Ordinal.{u} // x ∈ Iio a }))
          a₂) →
      x = a₂
⊢ Small.{u, u + 2} (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))

Tactic:
refine small_of_injective (β := Iio a) (f := fun x ↦ ⟨f x, hs _ (f x).2⟩) fun _ ↦ ?_

Premises used: small_of_injective
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
s : Set Ordinal.{u}
a : Ordinal.{u}
ha : #(↑s : Type (u + 1)) < (lift.{u + 1, u} a).cof
hs : ∀ i ∈ s, i < a
f : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2)) ≃o (↑s : Type (u + 1)) :=
  OrderIso.ofRelIsoLT (enum fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)
x : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))
⊢ ∀ ⦃a₂ : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))⦄,
    Eq.{u + 2} (α := (↑(Iio a) : Type (u + 1)))
        ((fun (x : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) ↦
            (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio a)
                (↑((f :
                        (a : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) →
                          (↑s : Type (u + 1)))
                      x) :
                  Ordinal.{u})
                ⋯ :
              { x : Ordinal.{u} // x ∈ Iio a }))
          x)
        ((fun (x : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) ↦
            (Subtype.mk (p := fun (x : Ordinal.{u}) ↦ x ∈ Iio a)
                (↑((f :
                        (a : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) →
                          (↑s : Type (u + 1)))
                      x) :
                  Ordinal.{u})
                ⋯ :
              { x : Ordinal.{u} // x ∈ Iio a }))
          a₂) →
      x = a₂

Tactic:
simp [Subtype.val_inj]

Premises used: Subtype.val_inj
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
s : Set Ordinal.{u}
a : Ordinal.{u}
ha : #(↑s : Type (u + 1)) < (lift.{u + 1, u} a).cof
hs : ∀ i ∈ s, i < a
f : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2)) ≃o (↑s : Type (u + 1)) :=
  OrderIso.ofRelIsoLT (enum fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)
⊢ Small.{u, u + 2} (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))

Tactic:
have : Small.{u} (Iio (typeLT s)) := by
    refine small_of_injective (β := Iio a) (f := fun x ↦ ⟨f x, hs _ (f x).2⟩) fun _ ↦ ?_
    simp [Subtype.val_inj]
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
s : Set Ordinal.{u}
a : Ordinal.{u}
ha : #(↑s : Type (u + 1)) < (lift.{u + 1, u} a).cof
hs : ∀ i ∈ s, i < a
f : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2)) ≃o (↑s : Type (u + 1)) :=
  OrderIso.ofRelIsoLT (enum fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)
this : Small.{u, u + 2} (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))
⊢ Eq.{u + 2} (α := Set Ordinal.{u})
    (range (ι := (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2)))
      ((fun (x : Ordinal.{u}) ↦ x + 1) ∘
        fun (i : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) ↦
        (↑((f : (a : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) → (↑s : Type (u + 1)))
              i) :
          Ordinal.{u})))
    ((fun (x : Ordinal.{u}) ↦ x + 1) ''
      range fun (i : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) ↦
        (↑((f : (a : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) → (↑s : Type (u + 1)))
              i) :
          Ordinal.{u}))

Tactic:
range_comp (· + 1) (fun i ↦ (f i).1)

Premises used: Set.range_comp, HAdd.hAdd, OfNat.ofNat, Subtype.val, DFunLike.coe
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
s : Set Ordinal.{u}
a : Ordinal.{u}
ha : #(↑s : Type (u + 1)) < (lift.{u + 1, u} a).cof
hs : ∀ i ∈ s, i < a
f : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2)) ≃o (↑s : Type (u + 1)) :=
  OrderIso.ofRelIsoLT (enum fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)
this : Small.{u, u + 2} (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))
h :
  s =
    range fun (i : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) ↦
      (↑((f : (a : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) → (↑s : Type (u + 1)))
            i) :
        Ordinal.{u})
⊢ Eq (α := Set Ordinal.{u})
    (range fun (i : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) ↦
      HAdd.hAdd (α := Ordinal.{u})
        (↑((f : (a : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) → (↑s : Type (u + 1)))
              i) :
          Ordinal.{u})
        1)
    ((fun (x : Ordinal.{u}) ↦ x + 1) '' s)

Tactic:
convert! range_comp (· + 1) (fun i ↦ (f i).1)

Premises used: Set.range_comp, HAdd.hAdd, OfNat.ofNat, Subtype.val, DFunLike.coe
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
s : Set Ordinal.{u}
a : Ordinal.{u}
ha : #(↑s : Type (u + 1)) < (lift.{u + 1, u} a).cof
hs : ∀ i ∈ s, i < a
f : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2)) ≃o (↑s : Type (u + 1)) :=
  OrderIso.ofRelIsoLT (enum fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)
this : Small.{u, u + 2} (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))
h : s = image (α := (↑s : Type (u + 1))) (Subtype.val (p := fun (x : Ordinal.{u}) ↦ x ∈ s)) Set.univ
⊢ s =
    range fun (i : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) ↦
      (↑((f : (a : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) → (↑s : Type (u + 1)))
            i) :
        Ordinal.{u})

Tactic:
rw [range_comp', f.range_eq]

Premises used: OrderIso.range_eq, Set.range_comp'
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
s : Set Ordinal.{u}
a : Ordinal.{u}
ha : #(↑s : Type (u + 1)) < (lift.{u + 1, u} a).cof
hs : ∀ i ∈ s, i < a
f : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2)) ≃o (↑s : Type (u + 1)) :=
  OrderIso.ofRelIsoLT (enum fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)
this : Small.{u, u + 2} (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))
⊢ s = image (α := (↑s : Type (u + 1))) (Subtype.val (p := fun (x : Ordinal.{u}) ↦ x ∈ s)) Set.univ

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
s : Set Ordinal.{u}
a : Ordinal.{u}
ha : #(↑s : Type (u + 1)) < (lift.{u + 1, u} a).cof
hs : ∀ i ∈ s, i < a
f : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2)) ≃o (↑s : Type (u + 1)) :=
  OrderIso.ofRelIsoLT (enum fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)
this : Small.{u, u + 2} (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))
⊢ Eq (α := Set Ordinal.{u})
    (range fun (i : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) ↦
      HAdd.hAdd (α := Ordinal.{u})
        (↑((f : (a : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) → (↑s : Type (u + 1)))
              i) :
          Ordinal.{u})
        1)
    ((fun (x : Ordinal.{u}) ↦ x + 1) '' s)

Tactic:
have : range (fun i ↦ (f i).1 + 1) = (· + 1) '' s := by
    convert! range_comp (· + 1) (fun i ↦ (f i).1)
    rw [range_comp', f.range_eq]
    simp
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
s : Set Ordinal.{u}
a : Ordinal.{u}
ha : #(↑s : Type (u + 1)) < (lift.{u + 1, u} a).cof
hs : ∀ i ∈ s, i < a
f : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2)) ≃o (↑s : Type (u + 1)) :=
  OrderIso.ofRelIsoLT (enum fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)
this_1 : Small.{u, u + 2} (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))
this :
  Eq (α := Set Ordinal.{u})
    (range fun (i : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) ↦
      HAdd.hAdd (α := Ordinal.{u})
        (↑((f : (a : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) → (↑s : Type (u + 1)))
              i) :
          Ordinal.{u})
        1)
    ((fun (x : Ordinal.{u}) ↦ x + 1) '' s)
rw :
  ⨆ (i : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))),
      HAdd.hAdd (α := Ordinal.{u})
        (↑((f : (a : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) → (↑s : Type (u + 1)))
              i) :
          Ordinal.{u})
        1 <
    a
⊢ sSup ((fun (x : Ordinal.{u}) ↦ x + 1) '' s) < a

Tactic:
rw [← this, sSup_range]

Premises used: sSup_range
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
s : Set Ordinal.{u}
a : Ordinal.{u}
ha : #(↑s : Type (u + 1)) < (lift.{u + 1, u} a).cof
hs : ∀ i ∈ s, i < a
f : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2)) ≃o (↑s : Type (u + 1)) :=
  OrderIso.ofRelIsoLT (enum fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)
this_1 : Small.{u, u + 2} (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))
this :
  Eq (α := Set Ordinal.{u})
    (range fun (i : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) ↦
      HAdd.hAdd (α := Ordinal.{u})
        (↑((f : (a : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) → (↑s : Type (u + 1)))
              i) :
          Ordinal.{u})
        1)
    ((fun (x : Ordinal.{u}) ↦ x + 1) '' s)
a₁ :
  ⨆ (i : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))),
      HAdd.hAdd (α := Ordinal.{u})
        (↑((f : (a : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) → (↑s : Type (u + 1)))
              i) :
          Ordinal.{u})
        1 ≤
    a
a₂ :
  ⨆ (i : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))),
      HAdd.hAdd (α := Ordinal.{u})
        (↑((f : (a : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) → (↑s : Type (u + 1)))
              i) :
          Ordinal.{u})
        1 ≠
    a
⊢ ⨆ (i : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))),
      HAdd.hAdd (α := Ordinal.{u})
        (↑((f : (a : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) → (↑s : Type (u + 1)))
              i) :
          Ordinal.{u})
        1 <
    a

Tactic:
apply lt_of_le_of_ne

Premises used: lt_of_le_of_ne
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
s : Set Ordinal.{u}
a : Ordinal.{u}
ha : #(↑s : Type (u + 1)) < (lift.{u + 1, u} a).cof
hs : ∀ i ∈ s, i < a
f : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2)) ≃o (↑s : Type (u + 1)) :=
  OrderIso.ofRelIsoLT (enum fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)
this_1 : Small.{u, u + 2} (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))
this :
  Eq (α := Set Ordinal.{u})
    (range fun (i : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) ↦
      HAdd.hAdd (α := Ordinal.{u})
        (↑((f : (a : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) → (↑s : Type (u + 1)))
              i) :
          Ordinal.{u})
        1)
    ((fun (x : Ordinal.{u}) ↦ x + 1) '' s)
⊢ ⨆ (i : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))),
      HAdd.hAdd (α := Ordinal.{u})
        (↑((f : (a : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) → (↑s : Type (u + 1)))
              i) :
          Ordinal.{u})
        1 ≤
    a

Tactic:
simp [hs]
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
s : Set Ordinal.{u}
f : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2)) ≃o (↑s : Type (u + 1)) :=
  OrderIso.ofRelIsoLT (enum fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)
this_1 : Small.{u, u + 2} (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))
this :
  Eq (α := Set Ordinal.{u})
    (range fun (i : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) ↦
      HAdd.hAdd (α := Ordinal.{u})
        (↑((f : (a : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) → (↑s : Type (u + 1)))
              i) :
          Ordinal.{u})
        1)
    ((fun (x : Ordinal.{u}) ↦ x + 1) '' s)
ha :
  Cardinal.lift.{u + 2, u + 1} #(↑s : Type (u + 1)) <
    Cardinal.lift.{u + 2, u}
      (cof
        (⨆ (i : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))),
          HAdd.hAdd (α := Ordinal.{u})
            (↑((f :
                    (a : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) →
                      (↑s : Type (u + 1)))
                  i) :
              Ordinal.{u})
            1))
hs :
  ∀ i ∈ s,
    i <
      ⨆ (i : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))),
        HAdd.hAdd (α := Ordinal.{u})
          (↑((f :
                  (a : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) →
                    (↑s : Type (u + 1)))
                i) :
            Ordinal.{u})
          1
x : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))
⊢ ∀ ⦃b : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))⦄,
    x < b →
      LT.lt.{u + 1} (α := Ordinal.{u})
        (↑((f : (a : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) → (↑s : Type (u + 1)))
              x) :
          Ordinal.{u})
        (↑((f : (a : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) → (↑s : Type (u + 1)))
              b) :
          Ordinal.{u})

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
s : Set Ordinal.{u}
f : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2)) ≃o (↑s : Type (u + 1)) :=
  OrderIso.ofRelIsoLT (enum fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)
this_1 : Small.{u, u + 2} (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))
this :
  Eq (α := Set Ordinal.{u})
    (range fun (i : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) ↦
      HAdd.hAdd (α := Ordinal.{u})
        (↑((f : (a : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) → (↑s : Type (u + 1)))
              i) :
          Ordinal.{u})
        1)
    ((fun (x : Ordinal.{u}) ↦ x + 1) '' s)
ha :
  #(↑s : Type (u + 1)) <
    (lift.{u + 1, u}
        (⨆ (i : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))),
          HAdd.hAdd (α := Ordinal.{u})
            (↑((f :
                    (a : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) →
                      (↑s : Type (u + 1)))
                  i) :
              Ordinal.{u})
            1)).cof
hs :
  ∀ i ∈ s,
    i <
      ⨆ (i : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))),
        HAdd.hAdd (α := Ordinal.{u})
          (↑((f :
                  (a : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) →
                    (↑s : Type (u + 1)))
                i) :
            Ordinal.{u})
          1
⊢ #(↑s : Type (u + 1)) < Order.cof (↑s : Type (u + 1))

Tactic:
rw [← lift_cof, ← Cardinal.lift_lt.{_, u + 2}, Cardinal.lift_lift,
      lift_cof_iSup_add_one fun _ ↦ by simp, cof_Iio, ← lift_cof, cof_type,
      Cardinal.lift_lift, Cardinal.lift_lt] at ha

Premises used: Ordinal.cof_Iio, Cardinal.lift_lift, Ordinal.cof_type, Ordinal.lift_cof_iSup_add_one, Cardinal.lift_lt, Ordinal.lift_cof
-- Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Goal:
s : Set Ordinal.{u}
f : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2)) ≃o (↑s : Type (u + 1)) :=
  OrderIso.ofRelIsoLT (enum fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)
this_1 : Small.{u, u + 2} (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))
this :
  Eq (α := Set Ordinal.{u})
    (range fun (i : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) ↦
      HAdd.hAdd (α := Ordinal.{u})
        (↑((f : (a : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) → (↑s : Type (u + 1)))
              i) :
          Ordinal.{u})
        1)
    ((fun (x : Ordinal.{u}) ↦ x + 1) '' s)
ha :
  #(↑s : Type (u + 1)) <
    (lift.{u + 1, u}
        (⨆ (i : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))),
          HAdd.hAdd (α := Ordinal.{u})
            (↑((f :
                    (a : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) →
                      (↑s : Type (u + 1)))
                  i) :
              Ordinal.{u})
            1)).cof
hs :
  ∀ i ∈ s,
    i <
      ⨆ (i : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))),
        HAdd.hAdd (α := Ordinal.{u})
          (↑((f :
                  (a : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) →
                    (↑s : Type (u + 1)))
                i) :
            Ordinal.{u})
          1
ha₁ : #(↑s : Type (u + 1)) < Order.cof (↑s : Type (u + 1))
⊢ ∀ i ∈ s,
    i <
      ⨆ (i : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))),
        HAdd.hAdd (α := Ordinal.{u})
          (↑((f :
                  (a : (↑(Iio (type fun (x1 x2 : (↑s : Type (u + 1))) ↦ x1 < x2)) : Type (u + 2))) →
                    (↑s : Type (u + 1)))
                i) :
            Ordinal.{u})
          1

Tactic:
rw [← lift_cof, ← Cardinal.lift_lt.{_, u + 2}, Cardinal.lift_lift,
      lift_cof_iSup_add_one fun _ ↦ by simp, cof_Iio, ← lift_cof, cof_type,
      Cardinal.lift_lift, Cardinal.lift_lt] at ha

Premises used: Ordinal.cof_Iio, Cardinal.lift_lift, Ordinal.cof_type, Ordinal.lift_cof_iSup_add_one, Cardinal.lift_lt, Ordinal.lift_cof