[GOAL]
k : Type u_1
inst✝ : LinearOrderedField k
⊢ k ≃o ↑(Ioo (-1) 1)
[PROOFSTEP]
refine' StrictMono.orderIsoOfRightInverse _ _ (fun x ↦ x / (1 - |↑x|)) _
[GOAL]
case refine'_1
k : Type u_1
inst✝ : LinearOrderedField k
⊢ k → ↑(Ioo (-1) 1)
[PROOFSTEP]
refine' codRestrict (fun x ↦ x / (1 + |x|)) _ fun x ↦ abs_lt.1 _
[GOAL]
case refine'_1
k : Type u_1
inst✝ : LinearOrderedField k
x : k
⊢ |(fun x => x / (1 + |x|)) x| < 1
[PROOFSTEP]
have H : 0 < 1 + |x| := (abs_nonneg x).trans_lt (lt_one_add _)
[GOAL]
case refine'_1
k : Type u_1
inst✝ : LinearOrderedField k
x : k
H : 0 < 1 + |x|
⊢ |(fun x => x / (1 + |x|)) x| < 1
[PROOFSTEP]
calc
  |x / (1 + |x|)| = |x| / (1 + |x|) := by rw [abs_div, abs_of_pos H]
  _ < 1 := (div_lt_one H).2 (lt_one_add _)
[GOAL]
k : Type u_1
inst✝ : LinearOrderedField k
x : k
H : 0 < 1 + |x|
⊢ |x / (1 + |x|)| = |x| / (1 + |x|)
[PROOFSTEP]
rw [abs_div, abs_of_pos H]
[GOAL]
case refine'_2
k : Type u_1
inst✝ : LinearOrderedField k
⊢ StrictMono
    (codRestrict (fun x => x / (1 + |x|)) (Ioo (-1) 1)
      (_ : ∀ (x : k), -1 < (fun x => x / (1 + |x|)) x ∧ (fun x => x / (1 + |x|)) x < 1))
[PROOFSTEP]
refine' (strictMono_of_odd_strictMonoOn_nonneg _ _).codRestrict _
[GOAL]
case refine'_2.refine'_1
k : Type u_1
inst✝ : LinearOrderedField k
⊢ ∀ (x : k), -x / (1 + |(-x)|) = -(x / (1 + |x|))
[PROOFSTEP]
intro x
[GOAL]
case refine'_2.refine'_1
k : Type u_1
inst✝ : LinearOrderedField k
x : k
⊢ -x / (1 + |(-x)|) = -(x / (1 + |x|))
[PROOFSTEP]
simp only [abs_neg, neg_div]
[GOAL]
case refine'_2.refine'_2
k : Type u_1
inst✝ : LinearOrderedField k
⊢ StrictMonoOn (fun x => x / (1 + |x|)) (Ici 0)
[PROOFSTEP]
rintro x (hx : 0 ≤ x) y (hy : 0 ≤ y) hxy
[GOAL]
case refine'_2.refine'_2
k : Type u_1
inst✝ : LinearOrderedField k
x : k
hx : 0 ≤ x
y : k
hy : 0 ≤ y
hxy : x < y
⊢ (fun x => x / (1 + |x|)) x < (fun x => x / (1 + |x|)) y
[PROOFSTEP]
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 _), *]
[GOAL]
case refine'_3
k : Type u_1
inst✝ : LinearOrderedField k
⊢ Function.RightInverse (fun x => ↑x / (1 - |↑x|))
    (codRestrict (fun x => x / (1 + |x|)) (Ioo (-1) 1)
      (_ : ∀ (x : k), -1 < (fun x => x / (1 + |x|)) x ∧ (fun x => x / (1 + |x|)) x < 1))
[PROOFSTEP]
refine' fun x ↦ Subtype.ext _
[GOAL]
case refine'_3
k : Type u_1
inst✝ : LinearOrderedField k
x : ↑(Ioo (-1) 1)
⊢ ↑(codRestrict (fun x => x / (1 + |x|)) (Ioo (-1) 1)
        (_ : ∀ (x : k), -1 < (fun x => x / (1 + |x|)) x ∧ (fun x => x / (1 + |x|)) x < 1)
        ((fun x => ↑x / (1 - |↑x|)) x)) =
    ↑x
[PROOFSTEP]
have : 0 < 1 - |(x : k)| := sub_pos.2 (abs_lt.2 x.2)
[GOAL]
case refine'_3
k : Type u_1
inst✝ : LinearOrderedField k
x : ↑(Ioo (-1) 1)
this : 0 < 1 - |↑x|
⊢ ↑(codRestrict (fun x => x / (1 + |x|)) (Ioo (-1) 1)
        (_ : ∀ (x : k), -1 < (fun x => x / (1 + |x|)) x ∧ (fun x => x / (1 + |x|)) x < 1)
        ((fun x => ↑x / (1 - |↑x|)) x)) =
    ↑x
[PROOFSTEP]
field_simp [abs_div, this.ne', abs_of_pos this]
