awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
inst : Preorder α
a : α
b : (↑(Iio a) : Type u_1)
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ Iio a) '' Ioi b = Ioo (↑b : α) a

Tactic:
(Subtype.image_preimage_val (Iio a) (Ioi b)).trans <| inter_comm _ _

Premises used: Set.Ioi, Set.Mem, setOf, Set.inter_comm, Set.preimage, Subtype.image_preimage_val, Subtype.val, Set.Iio, Eq.trans
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
inst : Preorder α
a : α
b : (↑(Iio a) : Type u_1)
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ Iio a) '' Iio b = Iio (↑b : α)

Tactic:
image_subtype_val_Ioi_Ioi (α := αᵒᵈ) _

Premises used: Set.image_subtype_val_Ioi_Ioi, Set.Mem, setOf, OrderDual, Set.Iio
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
inst : Preorder α
a b : α
c : (↑(Icc a b) : Type u_1)
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b) '' Ici c = Icc (↑c : α) b

Tactic:
image_subtype_val_Ixx_Ixi c c.2.1.trans

Premises used: Set.Ici, Set.Mem, setOf, Set.Icc, And.left, LE.le.trans, _private.0.Set.image_subtype_val_Ixx_Ixi, Subtype.property
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
inst : Preorder α
a b : α
c : (↑(Icc a b) : Type u_1)
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b) '' Iic c = Icc a (↑c : α)

Tactic:
image_subtype_val_Ixx_Iix c (le_trans · c.2.2)

Premises used: Set.Mem, setOf, _private.0.Set.image_subtype_val_Ixx_Iix, Set.Icc, And.right, Set.Iic, Subtype.property, le_trans
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
inst : Preorder α
a b : α
c : (↑(Icc a b) : Type u_1)
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b) '' Ioi c = Ioc (↑c : α) b

Tactic:
image_subtype_val_Ixx_Ixi c (c.2.1.trans <| le_of_lt ·)

Premises used: Set.Ioc, Set.Ioi, Set.Mem, setOf, le_of_lt, Set.Icc, And.left, LE.le.trans, _private.0.Set.image_subtype_val_Ixx_Ixi, Subtype.property
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
inst : Preorder α
a b : α
c : (↑(Icc a b) : Type u_1)
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b) '' Iio c = Ico a (↑c : α)

Tactic:
image_subtype_val_Ixx_Iix c fun h ↦ (le_of_lt h).trans c.2.2

Premises used: Set.Mem, setOf, _private.0.Set.image_subtype_val_Ixx_Iix, le_of_lt, Set.Ico, Set.Icc, And.right, LE.le.trans, Set.Iio, Subtype.property
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
inst : Preorder α
a b : α
c : (↑(Ico a b) : Type u_1)
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ Ico a b) '' Ici c = Ico (↑c : α) b

Tactic:
image_subtype_val_Ixx_Ixi c c.2.1.trans

Premises used: Set.Ici, Set.Mem, setOf, Set.Ico, And.left, LE.le.trans, _private.0.Set.image_subtype_val_Ixx_Ixi, Subtype.property
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
inst : Preorder α
a b : α
c : (↑(Ico a b) : Type u_1)
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ Ico a b) '' Iic c = Icc a (↑c : α)

Tactic:
image_subtype_val_Ixx_Iix c (lt_of_le_of_lt · c.2.2)

Premises used: lt_of_le_of_lt, Set.Mem, setOf, _private.0.Set.image_subtype_val_Ixx_Iix, Set.Ico, Set.Icc, And.right, Set.Iic, Subtype.property
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
inst : Preorder α
a b : α
c : (↑(Ico a b) : Type u_1)
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ Ico a b) '' Ioi c = Ioo (↑c : α) b

Tactic:
image_subtype_val_Ixx_Ixi c (c.2.1.trans <| le_of_lt ·)

Premises used: Set.Ioi, Set.Mem, setOf, le_of_lt, Set.Ico, And.left, LE.le.trans, Set.Ioo, _private.0.Set.image_subtype_val_Ixx_Ixi, Subtype.property
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
inst : Preorder α
a b : α
c : (↑(Ico a b) : Type u_1)
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ Ico a b) '' Iio c = Ico a (↑c : α)

Tactic:
image_subtype_val_Ixx_Iix c (lt_trans · c.2.2)

Premises used: Set.Mem, setOf, lt_trans, _private.0.Set.image_subtype_val_Ixx_Iix, Set.Ico, And.right, Set.Iio, Subtype.property
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
inst : Preorder α
a b : α
c : (↑(Ioc a b) : Type u_1)
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ Ioc a b) '' Ici c = Icc (↑c : α) b

Tactic:
image_subtype_val_Ixx_Ixi c c.2.1.trans_le

Premises used: Set.Ioc, Set.Ici, Set.Mem, setOf, Set.Icc, And.left, LT.lt.trans_le, _private.0.Set.image_subtype_val_Ixx_Ixi, Subtype.property
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
inst : Preorder α
a b : α
c : (↑(Ioc a b) : Type u_1)
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ Ioc a b) '' Iic c = Ioc a (↑c : α)

Tactic:
image_subtype_val_Ixx_Iix c (le_trans · c.2.2)

Premises used: Set.Ioc, Set.Mem, setOf, _private.0.Set.image_subtype_val_Ixx_Iix, And.right, Set.Iic, Subtype.property, le_trans
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
inst : Preorder α
a b : α
c : (↑(Ioc a b) : Type u_1)
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ Ioc a b) '' Ioi c = Ioc (↑c : α) b

Tactic:
image_subtype_val_Ixx_Ixi c c.2.1.trans

Premises used: Set.Ioc, Set.Ioi, Set.Mem, setOf, And.left, LT.lt.trans, _private.0.Set.image_subtype_val_Ixx_Ixi, Subtype.property
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
inst : Preorder α
a b : α
c : (↑(Ioc a b) : Type u_1)
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ Ioc a b) '' Iio c = Ioo a (↑c : α)

Tactic:
image_subtype_val_Ixx_Iix c fun h ↦ (le_of_lt h).trans c.2.2

Premises used: Set.Ioc, Set.Mem, setOf, _private.0.Set.image_subtype_val_Ixx_Iix, le_of_lt, And.right, LE.le.trans, Set.Iio, Set.Ioo, Subtype.property
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
inst : Preorder α
a b : α
c : (↑(Ioo a b) : Type u_1)
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ Ioo a b) '' Ici c = Ico (↑c : α) b

Tactic:
image_subtype_val_Ixx_Ixi c c.2.1.trans_le

Premises used: Set.Ici, Set.Mem, setOf, Set.Ico, And.left, LT.lt.trans_le, Set.Ioo, _private.0.Set.image_subtype_val_Ixx_Ixi, Subtype.property
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
inst : Preorder α
a b : α
c : (↑(Ioo a b) : Type u_1)
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ Ioo a b) '' Iic c = Ioc a (↑c : α)

Tactic:
image_subtype_val_Ixx_Iix c (lt_of_le_of_lt · c.2.2)

Premises used: Set.Ioc, lt_of_le_of_lt, Set.Mem, setOf, _private.0.Set.image_subtype_val_Ixx_Iix, And.right, Set.Iic, Set.Ioo, Subtype.property
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
inst : Preorder α
a b : α
c : (↑(Ioo a b) : Type u_1)
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ Ioo a b) '' Ioi c = Ioo (↑c : α) b

Tactic:
image_subtype_val_Ixx_Ixi c c.2.1.trans

Premises used: Set.Ioi, Set.Mem, setOf, And.left, LT.lt.trans, Set.Ioo, _private.0.Set.image_subtype_val_Ixx_Ixi, Subtype.property
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
inst : Preorder α
a b : α
c : (↑(Ioo a b) : Type u_1)
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ Ioo a b) '' Iio c = Ioo a (↑c : α)

Tactic:
image_subtype_val_Ixx_Iix c (lt_trans · c.2.2)

Premises used: Set.Mem, setOf, lt_trans, _private.0.Set.image_subtype_val_Ixx_Iix, And.right, Set.Iio, Set.Ioo, Subtype.property
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
inst : Preorder α
b : α
⊢ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (Iic b)

Tactic:
fun _x hx _y hy ↦ ⟨b, le_rfl, hx, hy⟩

Premises used: le_rfl, DirectedOn, And.intro, Exists.intro
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (Icc a b)

Tactic:
fun _x hx _y hy ↦ ⟨b, right_mem_Icc.2 <| hx.1.trans hx.2, hx.2, hy.2⟩

Premises used: Iff.mpr, Set.right_mem_Icc, DirectedOn, And.right, And.left, And.intro, Exists.intro, LE.le.trans
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (Ioc a b)

Tactic:
fun _x hx _y hy ↦ ⟨b, right_mem_Ioc.2 <| hx.1.trans_le hx.2, hx.2, hy.2⟩

Premises used: Iff.mpr, DirectedOn, And.right, And.left, LT.lt.trans_le, And.intro, Exists.intro, Set.right_mem_Ioc
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ DirectedOn (fun (x1 x2 : α) ↦ x1 ≥ x2) (Ici a)

Tactic:
fun _x hx _y hy ↦ ⟨a, le_rfl, hx, hy⟩

Premises used: le_rfl, DirectedOn, And.intro, Exists.intro
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ DirectedOn (fun (x1 x2 : α) ↦ x1 ≥ x2) (Icc a b)

Tactic:
fun _x hx _y hy ↦ ⟨a, left_mem_Icc.2 <| hx.1.trans hx.2, hx.1, hy.1⟩

Premises used: Iff.mpr, DirectedOn, And.right, And.left, Set.left_mem_Icc, And.intro, Exists.intro, LE.le.trans
-- Module: Mathlib.Order.Interval.Set.Image
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ DirectedOn (fun (x1 x2 : α) ↦ x1 ≥ x2) (Ico a b)

Tactic:
fun _x hx _y hy ↦ ⟨a, left_mem_Ico.2 <| hx.1.trans_lt hx.2, hx.1, hy.1⟩

Premises used: Iff.mpr, Set.left_mem_Ico, DirectedOn, And.right, And.left, And.intro, Exists.intro, LE.le.trans_lt
-- Module: Mathlib.Order.Interval.Set.Infinite
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
inst_2 : NoMaxOrder α
⊢ Infinite α

Tactic:
let ⟨f, hf⟩ := Nat.exists_strictMono α
  Infinite.of_injective f hf.injective

Premises used: Nat.exists_strictMono, Infinite.of_injective, _private.0.NoMaxOrder.infinite.match_1, StrictMono.injective, Infinite
-- Module: Mathlib.Order.Interval.Set.Infinite
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
inst_2 : NoMinOrder α
⊢ Infinite α

Tactic:
@NoMaxOrder.infinite αᵒᵈ _ _ _

Premises used: OrderDual, NoMaxOrder.infinite
-- Module: Mathlib.Order.Interval.Set.Infinite
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DenselyOrdered α
a b : α
h : a < b
⊢ Infinite.{u_1 + 1} (↑(Ioo a b) : Type u_1)

Tactic:
@NoMaxOrder.infinite _ _ (nonempty_Ioo_subtype h) _

Premises used: NoMaxOrder.infinite
-- Module: Mathlib.Order.Interval.Set.Infinite
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DenselyOrdered α
a b : α
h : a < b
⊢ (Ioo a b).Infinite

Tactic:
infinite_coe_iff.1 <| Ioo.infinite h

Premises used: Set.Ioo.infinite, Set.infinite_coe_iff, Iff.mp
-- Module: Mathlib.Order.Interval.Set.Infinite
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DenselyOrdered α
a b : α
h : a < b
⊢ (Ico a b).Infinite

Tactic:
(Ioo_infinite h).mono Ioo_subset_Ico_self

Premises used: Set.Infinite.mono, Set.Ioo_subset_Ico_self, Set.Ioo_infinite
-- Module: Mathlib.Order.Interval.Set.Infinite
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DenselyOrdered α
a b : α
h : a < b
⊢ Infinite.{u_1 + 1} (↑(Ico a b) : Type u_1)

Tactic:
infinite_coe_iff.2 <| Ico_infinite h

Premises used: Iff.mpr, Set.infinite_coe_iff, Set.Ico_infinite
-- Module: Mathlib.Order.Interval.Set.Infinite
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DenselyOrdered α
a b : α
h : a < b
⊢ (Ioc a b).Infinite

Tactic:
(Ioo_infinite h).mono Ioo_subset_Ioc_self

Premises used: Set.Infinite.mono, Set.Ioo_subset_Ioc_self, Set.Ioo_infinite
-- Module: Mathlib.Order.Interval.Set.Infinite
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DenselyOrdered α
a b : α
h : a < b
⊢ Infinite.{u_1 + 1} (↑(Ioc a b) : Type u_1)

Tactic:
infinite_coe_iff.2 <| Ioc_infinite h

Premises used: Iff.mpr, Set.infinite_coe_iff, Set.Ioc_infinite
-- Module: Mathlib.Order.Interval.Set.Infinite
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DenselyOrdered α
a b : α
h : a < b
⊢ (Icc a b).Infinite

Tactic:
(Ioo_infinite h).mono Ioo_subset_Icc_self

Premises used: Set.Infinite.mono, Set.Ioo_subset_Icc_self, Set.Ioo_infinite
-- Module: Mathlib.Order.Interval.Set.Infinite
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DenselyOrdered α
a b : α
h : a < b
⊢ Infinite.{u_1 + 1} (↑(Icc a b) : Type u_1)

Tactic:
infinite_coe_iff.2 <| Icc_infinite h

Premises used: Iff.mpr, Set.infinite_coe_iff, Set.Icc_infinite
-- Module: Mathlib.Order.Interval.Set.Infinite
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoMinOrder α
a : α
⊢ Infinite.{u_1 + 1} (↑(Iio a) : Type u_1)

Tactic:
NoMinOrder.infinite

Premises used: NoMinOrder.infinite
-- Module: Mathlib.Order.Interval.Set.Infinite
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoMinOrder α
a : α
⊢ (Iio a).Infinite

Tactic:
infinite_coe_iff.1 inferInstance

Premises used: inferInstance, Set.infinite_coe_iff, Iff.mp
-- Module: Mathlib.Order.Interval.Set.Infinite
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoMinOrder α
a : α
⊢ Infinite.{u_1 + 1} (↑(Iic a) : Type u_1)

Tactic:
NoMinOrder.infinite

Premises used: NoMinOrder.infinite
-- Module: Mathlib.Order.Interval.Set.Infinite
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoMinOrder α
a : α
⊢ (Iic a).Infinite

Tactic:
infinite_coe_iff.1 inferInstance

Premises used: inferInstance, Set.infinite_coe_iff, Iff.mp
-- Module: Mathlib.Order.Interval.Set.Infinite
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoMaxOrder α
a : α
⊢ Infinite.{u_1 + 1} (↑(Ioi a) : Type u_1)

Tactic:
NoMaxOrder.infinite

Premises used: NoMaxOrder.infinite
-- Module: Mathlib.Order.Interval.Set.Infinite
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoMaxOrder α
a : α
⊢ (Ioi a).Infinite

Tactic:
infinite_coe_iff.1 inferInstance

Premises used: inferInstance, Set.infinite_coe_iff, Iff.mp
-- Module: Mathlib.Order.Interval.Set.Infinite
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoMaxOrder α
a : α
⊢ Infinite.{u_1 + 1} (↑(Ici a) : Type u_1)

Tactic:
NoMaxOrder.infinite

Premises used: NoMaxOrder.infinite
-- Module: Mathlib.Order.Interval.Set.Infinite
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoMaxOrder α
a : α
⊢ (Ici a).Infinite

Tactic:
infinite_coe_iff.1 inferInstance

Premises used: inferInstance, Set.infinite_coe_iff, Iff.mp
-- Module: Mathlib.Order.Interval.Set.InitialSeg
Goal:
α : Type u_1
inst : Preorder α
i j_1 j : α
x x_1 : (↑(Iic j) : Type u_1)
h :
  Eq.{u_1 + 1} (α := α) ((fun (j_2 : (↑(Iic j) : Type u_1)) ↦ (↑j_2 : α)) x)
    ((fun (j_2 : (↑(Iic j) : Type u_1)) ↦ (↑j_2 : α)) x_1)
⊢ x = x_1

Tactic:
aesop
-- Module: Mathlib.Order.Interval.Set.InitialSeg
Goal:
α : Type u_1
inst : Preorder α
i j_1 j : α
⊢ ∀ {a b : (↑(Iic j) : Type u_1)},
    LT.lt (α := α)
        (({ toFun := fun (j_2 : (↑(Iic j) : Type u_1)) ↦ (↑j_2 : α), inj' := ⋯ } : (a : (↑(Iic j) : Type u_1)) → α) a :
          α)
        (({ toFun := fun (j_2 : (↑(Iic j) : Type u_1)) ↦ (↑j_2 : α), inj' := ⋯ } : (a : (↑(Iic j) : Type u_1)) → α) b :
          α) ↔
      a < b

Tactic:
aesop
-- Module: Mathlib.Order.Interval.Set.InitialSeg
Goal:
α : Type u_1
inst : Preorder α
i j_1 j : α
x : (↑(Iic j) : Type u_1)
k : α
h :
  k <
    (RelEmbedding.mk (r := fun (x1 x2 : (↑(Iic j) : Type u_1)) ↦ x1 < x2) (s := fun (x1 x2 : α) ↦ x1 < x2)
          { toFun := fun (j_2 : (↑(Iic j) : Type u_1)) ↦ (↑j_2 : α), inj' := ⋯ } ⋯ :
        (a : (↑(Iic j) : Type u_1)) → α)
      x
⊢ Membership.mem (γ := Set α)
    (range (ι := (↑(Iic j) : Type u_1))
      (⇑(RelEmbedding.mk (r := fun (x1 x2 : (↑(Iic j) : Type u_1)) ↦ x1 < x2) (s := fun (x1 x2 : α) ↦ x1 < x2)
            { toFun := fun (j_2 : (↑(Iic j) : Type u_1)) ↦ (↑j_2 : α), inj' := ⋯ } ⋯) :
        (a : (↑(Iic j) : Type u_1)) → α))
    k

Tactic:
simpa using h.le.trans x.2

Premises used: LT.lt.le, LE.le.trans, Subtype.property
-- Module: Mathlib.Order.Interval.Set.InitialSeg
Goal:
α : Type u_1
inst : Preorder α
i j_1 j : α
x x_1 : (↑(Iio j) : Type u_1)
h :
  Eq.{u_1 + 1} (α := α) ((fun (j_2 : (↑(Iio j) : Type u_1)) ↦ (↑j_2 : α)) x)
    ((fun (j_2 : (↑(Iio j) : Type u_1)) ↦ (↑j_2 : α)) x_1)
⊢ x = x_1

Tactic:
aesop
-- Module: Mathlib.Order.Interval.Set.InitialSeg
Goal:
α : Type u_1
inst : Preorder α
i j_1 j : α
⊢ ∀ {a b : (↑(Iio j) : Type u_1)},
    LT.lt (α := α)
        (({ toFun := fun (j_2 : (↑(Iio j) : Type u_1)) ↦ (↑j_2 : α), inj' := ⋯ } : (a : (↑(Iio j) : Type u_1)) → α) a :
          α)
        (({ toFun := fun (j_2 : (↑(Iio j) : Type u_1)) ↦ (↑j_2 : α), inj' := ⋯ } : (a : (↑(Iio j) : Type u_1)) → α) b :
          α) ↔
      a < b

Tactic:
aesop
-- Module: Mathlib.Order.Interval.Set.InitialSeg
Goal:
α : Type u_1
inst : Preorder α
i j_1 j : α
⊢ ∀ (b : α),
    Membership.mem (γ := Set α)
        (range (ι := (↑(Iio j) : Type u_1))
          (⇑(RelEmbedding.mk (r := fun (x1 x2 : (↑(Iio j) : Type u_1)) ↦ x1 < x2) (s := fun (x1 x2 : α) ↦ x1 < x2)
                { toFun := fun (j_2 : (↑(Iio j) : Type u_1)) ↦ (↑j_2 : α), inj' := ⋯ } ⋯) :
            (a : (↑(Iio j) : Type u_1)) → α))
        b ↔
      b < j

Tactic:
aesop
-- Module: Mathlib.Order.Interval.Set.InitialSeg
Goal:
α : Type u_1
inst : Preorder α
j : α
k : (↑(Iio j) : Type u_1)
⊢ (PrincipalSeg.toRelEmbedding (r := fun (x1 x2 : (↑(Iio j) : Type u_1)) ↦ x1 < x2) (s := fun (x1 x2 : α) ↦ x1 < x2)
          (principalSegIio j) :
        (a : (↑(Iio j) : Type u_1)) → α)
      k =
    (↑k : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Interval.Set.InitialSeg
Goal:
α : Type u_1
inst : Preorder α
i j : α
h : i ≤ j
x x_1 : (↑(Iic i) : Type u_1)
h_1 :
  Eq.{u_1 + 1} (α := (↑(Iic j) : Type u_1))
    ((fun (k : (↑(Iic i) : Type u_1)) ↦ (Subtype.mk (p := fun (x : α) ↦ x ∈ Iic j) (↑k : α) ⋯ : { x : α // x ∈ Iic j }))
      x)
    ((fun (k : (↑(Iic i) : Type u_1)) ↦ (Subtype.mk (p := fun (x : α) ↦ x ∈ Iic j) (↑k : α) ⋯ : { x : α // x ∈ Iic j }))
      x_1)
⊢ x = x_1

Tactic:
aesop
-- Module: Mathlib.Order.Interval.Set.InitialSeg
Goal:
α : Type u_1
inst : Preorder α
i j : α
h : i ≤ j
⊢ ∀ {a b : (↑(Iic i) : Type u_1)},
    LT.lt (α := (↑(Iic j) : Type u_1))
        (({ toFun := fun (k : (↑(Iic i) : Type u_1)) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ Iic j) (↑k : α) ⋯,
                inj' := ⋯ } :
              (a : (↑(Iic i) : Type u_1)) → (↑(Iic j) : Type u_1))
            a :
          (↑(Iic j) : Type u_1))
        (({ toFun := fun (k : (↑(Iic i) : Type u_1)) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ Iic j) (↑k : α) ⋯,
                inj' := ⋯ } :
              (a : (↑(Iic i) : Type u_1)) → (↑(Iic j) : Type u_1))
            b :
          (↑(Iic j) : Type u_1)) ↔
      a < b

Tactic:
aesop
-- Module: Mathlib.Order.Interval.Set.InitialSeg
Goal:
α : Type u_1
inst : Preorder α
i j : α
h : i ≤ j
x x_1 : (↑(Iio i) : Type u_1)
h_1 :
  Eq.{u_1 + 1} (α := (↑(Iic j) : Type u_1))
    ((fun (k : (↑(Iio i) : Type u_1)) ↦ (Subtype.mk (p := fun (x : α) ↦ x ∈ Iic j) (↑k : α) ⋯ : { x : α // x ∈ Iic j }))
      x)
    ((fun (k : (↑(Iio i) : Type u_1)) ↦ (Subtype.mk (p := fun (x : α) ↦ x ∈ Iic j) (↑k : α) ⋯ : { x : α // x ∈ Iic j }))
      x_1)
⊢ x = x_1

Tactic:
aesop
-- Module: Mathlib.Order.Interval.Set.InitialSeg
Goal:
α : Type u_1
inst : Preorder α
i j : α
h : i ≤ j
⊢ ∀ {a b : (↑(Iio i) : Type u_1)},
    LT.lt (α := (↑(Iic j) : Type u_1))
        (({ toFun := fun (k : (↑(Iio i) : Type u_1)) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ Iic j) (↑k : α) ⋯,
                inj' := ⋯ } :
              (a : (↑(Iio i) : Type u_1)) → (↑(Iic j) : Type u_1))
            a :
          (↑(Iic j) : Type u_1))
        (({ toFun := fun (k : (↑(Iio i) : Type u_1)) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ Iic j) (↑k : α) ⋯,
                inj' := ⋯ } :
              (a : (↑(Iio i) : Type u_1)) → (↑(Iic j) : Type u_1))
            b :
          (↑(Iic j) : Type u_1)) ↔
      a < b

Tactic:
aesop
-- Module: Mathlib.Order.Interval.Set.InitialSeg
Goal:
α : Type u_1
inst : Preorder α
i j : α
h : i ≤ j
⊢ ∀ (b : (↑(Iic j) : Type u_1)),
    Membership.mem (γ := Set (↑(Iic j) : Type u_1))
        (range (ι := (↑(Iio i) : Type u_1))
          (⇑(RelEmbedding.mk (r := fun (x1 x2 : (↑(Iio i) : Type u_1)) ↦ x1 < x2) (s :=
                fun (x1 x2 : (↑(Iic j) : Type u_1)) ↦ x1 < x2)
                { toFun := fun (k : (↑(Iio i) : Type u_1)) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ Iic j) (↑k : α) ⋯,
                  inj' := ⋯ : (↑(Iio i) : Type u_1) ↪ (↑(Iic j) : Type u_1) }
                ⋯) :
            (a : (↑(Iio i) : Type u_1)) → (↑(Iic j) : Type u_1)))
        b ↔
      b < Subtype.mk (p := fun (x : α) ↦ x ∈ Iic j) i h

Tactic:
aesop
-- Module: Mathlib.Order.Interval.Set.InitialSeg
Goal:
α : Type u_1
inst : Preorder α
i j : α
h : i ≤ j
k : (↑(Iio i) : Type u_1)
⊢ Eq (α := (↑(Iic j) : Type u_1))
    (((principalSegIioIicOfLE h).toRelEmbedding (r := fun (x1 x2 : (↑(Iio i) : Type u_1)) ↦ x1 < x2) (s :=
            fun (x1 x2 : (↑(Iic j) : Type u_1)) ↦ x1 < x2) :
          (a : (↑(Iio i) : Type u_1)) → (↑(Iic j) : Type u_1))
        k :
      (↑(Iic j) : Type u_1))
    (Subtype.mk (p := fun (x : α) ↦ x ∈ Iic j) (↑k : α) ⋯ : { x : α // x ∈ Iic j })

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Interval.Set.IsoIoo
Goal:
k : Type u_1
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
refine_1 : k → (↑(Ioo (-1) 1) : Type u_1)
refine_2 :
  StrictMono.{u_1, u_1} (α := k) (β := (↑(Ioo (-1) 1) : Type u_1))
    (codRestrict (fun (x : k) ↦ x / (1 + |x|)) (Ioo (-1) 1) ⋯)
refine_3 :
  Function.RightInverse (α := k) (fun (x : (↑(Ioo (-1) 1) : Type u_1)) ↦ (↑x : k) / (1 - |(↑x : k)|))
    (codRestrict (fun (x : k) ↦ x / (1 + |x|)) (Ioo (-1) 1) ⋯)
⊢ k ≃o (↑(Ioo (-1) 1) : Type u_1)

Tactic:
refine StrictMono.orderIsoOfRightInverse ?_ ?_ (fun x ↦ x / (1 - |↑x|)) ?_

Premises used: abs, HSub.hSub, HDiv.hDiv, StrictMono.orderIsoOfRightInverse, OfNat.ofNat
-- Module: Mathlib.Order.Interval.Set.IsoIoo
Goal:
k : Type u_1
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
refine_1 : ∀ (x : k), LT.lt.{u_1} (α := k) |(fun (x : k) ↦ x / (1 + |x|)) x| 1
⊢ k → (↑(Ioo (-1) 1) : Type u_1)

Tactic:
refine codRestrict (fun x ↦ x / (1 + |x|)) _ fun x ↦ abs_lt.1 ?_

Premises used: abs, HDiv.hDiv, HAdd.hAdd, Set.codRestrict, OfNat.ofNat
-- Module: Mathlib.Order.Interval.Set.IsoIoo
Goal:
k : Type u_1
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
x : k
⊢ 0 < 1 + |x|

Tactic:
have H : 0 < 1 + |x| := (abs_nonneg x).trans_lt (lt_one_add _)
-- Module: Mathlib.Order.Interval.Set.IsoIoo
Goal:
k : Type u_1
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
x : k
H : 0 < 1 + |x|
rw : |x| / |1 + |x|| = |x| / (1 + |x|)
rw₁ rw₂ : |x| / (1 + |x|) = |x| / (1 + |x|)
⊢ |x / (1 + |x|)| = |x| / (1 + |x|)

Tactic:
rw [abs_div, abs_of_pos H]

Premises used: abs_div, abs_of_pos
-- Module: Mathlib.Order.Interval.Set.IsoIoo
Goal:
k : Type u_1
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
x : k
H : 0 < 1 + |x|
⊢ |x| / (1 + |x|) < 1

Tactic:
(div_lt_one H).2 (lt_one_add _)

Premises used: Iff.mpr, div_lt_one, lt_one_add
-- Module: Mathlib.Order.Interval.Set.IsoIoo
Goal:
k : Type u_1
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
x : k
H : 0 < 1 + |x|
by : |x / (1 + |x|)| = |x| / (1 + |x|)
⊢ LT.lt.{u_1} (α := k) |(fun (x : k) ↦ x / (1 + |x|)) x| 1

Tactic:
calc
      |x / (1 + |x|)| = |x| / (1 + |x|) := by rw [abs_div, abs_of_pos H]
      _ < 1 := (div_lt_one H).2 (lt_one_add _)

Premises used: Iff.mpr, abs, HAdd.hAdd, div_lt_one, OfNat.ofNat, lt_one_add
-- Module: Mathlib.Order.Interval.Set.IsoIoo
Goal:
k : Type u_1
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
⊢ StrictMono.{u_1, u_1} (α := k) (β := (↑(Ioo (-1) 1) : Type u_1))
    (codRestrict (fun (x : k) ↦ x / (1 + |x|)) (Ioo (-1) 1) ⋯)

Tactic:
(strictMono_of_odd_strictMonoOn_nonneg ?_ ?_).codRestrict _

Premises used: strictMono_of_odd_strictMonoOn_nonneg, StrictMono.codRestrict
-- Module: Mathlib.Order.Interval.Set.IsoIoo
Goal:
k : Type u_1
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
refine_2 : ∀ (x : k), -x / (1 + |(-x)|) = -(x / (1 + |x|))
refine_2₁ : StrictMonoOn (β := k) (fun (x : k) ↦ x / (1 + |x|)) (Ici 0)
⊢ StrictMono.{u_1, u_1} (α := k) (β := (↑(Ioo (-1) 1) : Type u_1))
    (codRestrict (fun (x : k) ↦ x / (1 + |x|)) (Ioo (-1) 1) ⋯)

Tactic:
refine (strictMono_of_odd_strictMonoOn_nonneg ?_ ?_).codRestrict _

Premises used: strictMono_of_odd_strictMonoOn_nonneg, StrictMono.codRestrict
-- Module: Mathlib.Order.Interval.Set.IsoIoo
Goal:
k : Type u_1
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
x : k
⊢ -x / (1 + |(-x)|) = -(x / (1 + |x|))

Tactic:
simp only [abs_neg, neg_div]

Premises used: abs_neg, neg_div
-- Module: Mathlib.Order.Interval.Set.IsoIoo
Goal:
k : Type u_1
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
x : k
hx : 0 ≤ x
y : k
hy : 0 ≤ y
hxy : x < y
⊢ LT.lt.{u_1} (α := k) ((fun (x : k) ↦ x / (1 + |x|)) x) ((fun (x : k) ↦ x / (1 + |x|)) y)

Tactic:
simp [abs_of_nonneg, mul_add, mul_comm x y, div_lt_div_iff₀, hx.trans_lt (lt_one_add _),
        hy.trans_lt (lt_one_add _), *]

Premises used: mul_comm, abs_of_nonneg, mul_add, div_lt_div_iff₀, LE.le.trans_lt, lt_one_add