[GOAL]
f g : CircleDeg1Lift
x : ℝ
⊢ ↑f (1 + x) = 1 + ↑f x
[PROOFSTEP]
rw [add_comm, map_add_one, add_comm 1]
[GOAL]
f✝ g✝ f g : CircleDeg1Lift
x : ℝ
⊢ OrderHom.toFun (OrderHom.comp f.toOrderHom g.toOrderHom) (x + 1) =
    OrderHom.toFun (OrderHom.comp f.toOrderHom g.toOrderHom) x + 1
[PROOFSTEP]
simp [map_add_one]
[GOAL]
f✝ g : CircleDeg1Lift
f : CircleDeg1Liftˣ
x : ℝ
⊢ ↑↑f⁻¹ (↑↑f x) = x
[PROOFSTEP]
simp only [← mul_apply, f.inv_mul, coe_one, id]
[GOAL]
f✝ g : CircleDeg1Lift
f : CircleDeg1Liftˣ
x : ℝ
⊢ ↑↑f (↑↑f⁻¹ x) = x
[PROOFSTEP]
simp only [← mul_apply, f.mul_inv, coe_one, id]
[GOAL]
f✝ g : CircleDeg1Lift
f : CircleDeg1Liftˣ
a✝ b✝ : ℝ
h :
  ↑{ toFun := ↑↑f, invFun := ↑↑f⁻¹, left_inv := (_ : ∀ (x : ℝ), ↑↑f⁻¹ (↑↑f x) = x),
          right_inv := (_ : ∀ (x : ℝ), ↑↑f (↑↑f⁻¹ x) = x) }
      a✝ ≤
    ↑{ toFun := ↑↑f, invFun := ↑↑f⁻¹, left_inv := (_ : ∀ (x : ℝ), ↑↑f⁻¹ (↑↑f x) = x),
          right_inv := (_ : ∀ (x : ℝ), ↑↑f (↑↑f⁻¹ x) = x) }
      b✝
⊢ a✝ ≤ b✝
[PROOFSTEP]
simpa using mono (↑f⁻¹) h
[GOAL]
f✝ g f : CircleDeg1Lift
h : Bijective ↑f
x y : ℝ
hxy : x ≤ y
⊢ ↑f (↑(Equiv.ofBijective (↑f) h).symm x) ≤ ↑f (↑(Equiv.ofBijective (↑f) h).symm y)
[PROOFSTEP]
simp only [Equiv.ofBijective_apply_symm_apply f h, hxy]
[GOAL]
f✝ g f : CircleDeg1Lift
h : Bijective ↑f
x : ℝ
⊢ ↑f
      (OrderHom.toFun
        { toFun := ↑(Equiv.ofBijective (↑f) h).symm,
          monotone' :=
            (_ : ∀ (x y : ℝ), x ≤ y → ↑(Equiv.ofBijective (↑f) h).symm x ≤ ↑(Equiv.ofBijective (↑f) h).symm y) }
        (x + 1)) =
    ↑f
      (OrderHom.toFun
          { toFun := ↑(Equiv.ofBijective (↑f) h).symm,
            monotone' :=
              (_ : ∀ (x y : ℝ), x ≤ y → ↑(Equiv.ofBijective (↑f) h).symm x ≤ ↑(Equiv.ofBijective (↑f) h).symm y) }
          x +
        1)
[PROOFSTEP]
simp only [Equiv.ofBijective_apply_symm_apply f, f.map_add_one]
[GOAL]
f g : CircleDeg1Lift
n : ℕ
⊢ ↑(f ^ (n + 1)) = (↑f)^[n + 1]
[PROOFSTEP]
ext x
[GOAL]
case h
f g : CircleDeg1Lift
n : ℕ
x : ℝ
⊢ ↑(f ^ (n + 1)) x = (↑f)^[n + 1] x
[PROOFSTEP]
simp [coe_pow n, pow_succ']
[GOAL]
f g : CircleDeg1Lift
x : ℝ
n : ℤ
⊢ ↑translate (↑Multiplicative.ofAdd x) ^ n = ↑translate (↑Multiplicative.ofAdd (↑n * x))
[PROOFSTEP]
simp only [← zsmul_eq_mul, ofAdd_zsmul, MonoidHom.map_zpow]
[GOAL]
f g : CircleDeg1Lift
x : ℝ
n : ℕ
⊢ (↑↑(↑translate (↑Multiplicative.ofAdd x)))^[n] = ↑↑(↑translate (↑Multiplicative.ofAdd (↑n * x)))
[PROOFSTEP]
rw [← coe_pow, ← Units.val_pow_eq_pow_val, translate_pow]
[GOAL]
f g : CircleDeg1Lift
n : ℕ
⊢ Function.Commute ↑f fun x => ↑n + x
[PROOFSTEP]
simpa only [nsmul_one, add_left_iterate] using Function.Commute.iterate_right f.map_one_add n
[GOAL]
f g : CircleDeg1Lift
n : ℕ
⊢ Function.Commute ↑f fun x => x + ↑n
[PROOFSTEP]
simp only [add_comm _ (n : ℝ), f.commute_nat_add n]
[GOAL]
f g : CircleDeg1Lift
n : ℕ
⊢ Function.Commute ↑f fun x => x - ↑n
[PROOFSTEP]
simpa only [sub_eq_add_neg] using
  (f.commute_add_nat n).inverses_right (Equiv.addRight _).right_inv (Equiv.addRight _).left_inv
[GOAL]
f g : CircleDeg1Lift
n : ℕ
⊢ Function.Commute ↑f fun x => x + ↑-[n+1]
[PROOFSTEP]
simpa [sub_eq_add_neg] using f.commute_sub_nat (n + 1)
[GOAL]
f g : CircleDeg1Lift
n : ℤ
⊢ Function.Commute ↑f fun x => ↑n + x
[PROOFSTEP]
simpa only [add_comm _ (n : ℝ)] using f.commute_add_int n
[GOAL]
f g : CircleDeg1Lift
n : ℤ
⊢ Function.Commute ↑f fun x => x - ↑n
[PROOFSTEP]
simpa only [sub_eq_add_neg] using
  (f.commute_add_int n).inverses_right (Equiv.addRight _).right_inv (Equiv.addRight _).left_inv
[GOAL]
f g : CircleDeg1Lift
n : ℤ
⊢ ↑f ↑n = ↑f 0 + ↑n
[PROOFSTEP]
rw [← f.map_add_int, zero_add]
[GOAL]
f g : CircleDeg1Lift
x : ℝ
⊢ ↑f (fract x) - fract x = ↑f x - x
[PROOFSTEP]
rw [Int.fract, f.map_sub_int, sub_sub_sub_cancel_right]
[GOAL]
f✝ g✝ f g : CircleDeg1Lift
x : ℝ
⊢ OrderHom.toFun
      { toFun := fun x => max (↑f x) (↑g x),
        monotone' := (_ : ∀ (x y : ℝ), x ≤ y → max (↑f x) (↑g x) ≤ max (↑f y) (↑g y)) }
      (x + 1) =
    OrderHom.toFun
        { toFun := fun x => max (↑f x) (↑g x),
          monotone' := (_ : ∀ (x y : ℝ), x ≤ y → max (↑f x) (↑g x) ≤ max (↑f y) (↑g y)) }
        x +
      1
[PROOFSTEP]
simp [max_add_add_right]
[GOAL]
f✝ g✝ f g : CircleDeg1Lift
x : ℝ
⊢ OrderHom.toFun
      { toFun := fun x => min (↑f x) (↑g x),
        monotone' := (_ : ∀ (x y : ℝ), x ≤ y → min (↑f x) (↑g x) ≤ min (↑f y) (↑g y)) }
      (x + 1) =
    OrderHom.toFun
        { toFun := fun x => min (↑f x) (↑g x),
          monotone' := (_ : ∀ (x y : ℝ), x ≤ y → min (↑f x) (↑g x) ≤ min (↑f y) (↑g y)) }
        x +
      1
[PROOFSTEP]
simp [min_add_add_right]
[GOAL]
f✝ g✝ f g : CircleDeg1Lift
h : f ≤ g
n : ℕ
x : ℝ
⊢ ↑(f ^ n) x ≤ ↑(g ^ n) x
[PROOFSTEP]
simp only [coe_pow, iterate_mono h n x]
[GOAL]
f g : CircleDeg1Lift
⊢ dist (↑f 0 + ↑g 0) (↑f (↑g 0)) < 1
[PROOFSTEP]
rw [dist_comm, Real.dist_eq, abs_lt, lt_sub_iff_add_lt', sub_lt_iff_lt_add', ← sub_eq_add_neg]
[GOAL]
f g : CircleDeg1Lift
⊢ ↑f 0 + ↑g 0 - 1 < ↑f (↑g 0) ∧ ↑f (↑g 0) < ↑f 0 + ↑g 0 + 1
[PROOFSTEP]
exact ⟨f.lt_map_map_zero g, f.map_map_zero_lt g⟩
[GOAL]
f✝ g f g₁ g₂ : CircleDeg1Lift
h : Semiconj ↑f ↑g₁ ↑g₂
⊢ dist (↑g₁ 0) (↑f (↑g₁ 0) - ↑f 0) + dist (↑f (↑g₁ 0) - ↑f 0) (↑g₂ 0) =
    dist (↑f 0 + ↑g₁ 0) (↑f (↑g₁ 0)) + dist (↑g₂ 0 + ↑f 0) (↑g₂ (↑f 0))
[PROOFSTEP]
simp only [h.eq, Real.dist_eq, sub_sub, add_comm (f 0), sub_sub_eq_add_sub, abs_sub_comm (g₂ (f 0))]
[GOAL]
f g : CircleDeg1Lift
⊢ Tendsto (fun x => x - 1) atTop atTop
[PROOFSTEP]
simpa [sub_eq_add_neg] using tendsto_atTop_add_const_right _ _ tendsto_id
[GOAL]
f g : CircleDeg1Lift
x : ℝ
m : ℤ
h : ↑f x ≤ x + ↑m
n : ℕ
⊢ (↑f)^[n] x ≤ x + ↑n * ↑m
[PROOFSTEP]
simpa only [nsmul_eq_mul, add_right_iterate] using
  (f.commute_add_int m).iterate_le_of_map_le f.monotone (monotone_id.add_const (m : ℝ)) h n
[GOAL]
f g : CircleDeg1Lift
x : ℝ
m : ℤ
h : x + ↑m ≤ ↑f x
n : ℕ
⊢ x + ↑n * ↑m ≤ (↑f)^[n] x
[PROOFSTEP]
simpa only [nsmul_eq_mul, add_right_iterate] using
  (f.commute_add_int m).symm.iterate_le_of_map_le (monotone_id.add_const (m : ℝ)) f.monotone h n
[GOAL]
f g : CircleDeg1Lift
x : ℝ
m : ℤ
h : ↑f x = x + ↑m
n : ℕ
⊢ (↑f)^[n] x = x + ↑n * ↑m
[PROOFSTEP]
simpa only [nsmul_eq_mul, add_right_iterate] using (f.commute_add_int m).iterate_eq_of_map_eq n h
[GOAL]
f g : CircleDeg1Lift
x : ℝ
m : ℤ
n : ℕ
hn : 0 < n
⊢ (↑f)^[n] x ≤ x + ↑n * ↑m ↔ ↑f x ≤ x + ↑m
[PROOFSTEP]
simpa only [nsmul_eq_mul, add_right_iterate] using
  (f.commute_add_int m).iterate_pos_le_iff_map_le f.monotone (strictMono_id.add_const (m : ℝ)) hn
[GOAL]
f g : CircleDeg1Lift
x : ℝ
m : ℤ
n : ℕ
hn : 0 < n
⊢ (↑f)^[n] x < x + ↑n * ↑m ↔ ↑f x < x + ↑m
[PROOFSTEP]
simpa only [nsmul_eq_mul, add_right_iterate] using
  (f.commute_add_int m).iterate_pos_lt_iff_map_lt f.monotone (strictMono_id.add_const (m : ℝ)) hn
[GOAL]
f g : CircleDeg1Lift
x : ℝ
m : ℤ
n : ℕ
hn : 0 < n
⊢ (↑f)^[n] x = x + ↑n * ↑m ↔ ↑f x = x + ↑m
[PROOFSTEP]
simpa only [nsmul_eq_mul, add_right_iterate] using
  (f.commute_add_int m).iterate_pos_eq_iff_map_eq f.monotone (strictMono_id.add_const (m : ℝ)) hn
[GOAL]
f g : CircleDeg1Lift
x : ℝ
m : ℤ
n : ℕ
hn : 0 < n
⊢ x + ↑n * ↑m ≤ (↑f)^[n] x ↔ x + ↑m ≤ ↑f x
[PROOFSTEP]
simpa only [not_lt] using not_congr (f.iterate_pos_lt_iff hn)
[GOAL]
f g : CircleDeg1Lift
x : ℝ
m : ℤ
n : ℕ
hn : 0 < n
⊢ x + ↑n * ↑m < (↑f)^[n] x ↔ x + ↑m < ↑f x
[PROOFSTEP]
simpa only [not_le] using not_congr (f.iterate_pos_le_iff hn)
[GOAL]
f g : CircleDeg1Lift
n : ℕ
⊢ ↑n * ⌊↑f 0⌋ ≤ ⌊(↑f)^[n] 0⌋
[PROOFSTEP]
rw [le_floor, Int.cast_mul, Int.cast_ofNat, ← zero_add ((n : ℝ) * _)]
[GOAL]
f g : CircleDeg1Lift
n : ℕ
⊢ 0 + ↑n * ↑⌊↑f 0⌋ ≤ (↑f)^[n] 0
[PROOFSTEP]
apply le_iterate_of_add_int_le_map
[GOAL]
case h
f g : CircleDeg1Lift
n : ℕ
⊢ 0 + ↑⌊↑f 0⌋ ≤ ↑f 0
[PROOFSTEP]
simp [floor_le]
[GOAL]
f g : CircleDeg1Lift
τ' : ℝ
h : Tendsto (fun n => (↑f)^[n] 0 / ↑n) atTop (𝓝 τ')
⊢ Tendsto (transnumAuxSeq f) atTop (𝓝 τ')
[PROOFSTEP]
simpa [(· ∘ ·), transnumAuxSeq_def, coe_pow] using h.comp (Nat.tendsto_pow_atTop_atTop_of_one_lt one_lt_two)
[GOAL]
f g : CircleDeg1Lift
τ' : ℝ
h : Tendsto (fun n => (↑f)^[n + 1] 0 / (↑n + 1)) atTop (𝓝 τ')
⊢ Tendsto (fun n => (↑f)^[n + 1] 0 / ↑(n + 1)) atTop (𝓝 τ')
[PROOFSTEP]
exact_mod_cast h
[GOAL]
f g : CircleDeg1Lift
⊢ transnumAuxSeq f 0 = ↑f 0
[PROOFSTEP]
simp [transnumAuxSeq]
[GOAL]
f g : CircleDeg1Lift
n : ℕ
⊢ dist (transnumAuxSeq f n) (transnumAuxSeq f (n + 1)) < 1 / 2 / 2 ^ n
[PROOFSTEP]
have : 0 < (2 ^ (n + 1) : ℝ) := pow_pos zero_lt_two _
[GOAL]
f g : CircleDeg1Lift
n : ℕ
this : 0 < 2 ^ (n + 1)
⊢ dist (transnumAuxSeq f n) (transnumAuxSeq f (n + 1)) < 1 / 2 / 2 ^ n
[PROOFSTEP]
rw [div_div, ← pow_succ, ← abs_of_pos this]
[GOAL]
f g : CircleDeg1Lift
n : ℕ
this : 0 < 2 ^ (n + 1)
⊢ dist (transnumAuxSeq f n) (transnumAuxSeq f (n + 1)) < 1 / |2 ^ (n + 1)|
[PROOFSTEP]
replace := abs_pos.2 (ne_of_gt this)
[GOAL]
f g : CircleDeg1Lift
n : ℕ
this : 0 < |2 ^ (n + 1)|
⊢ dist (transnumAuxSeq f n) (transnumAuxSeq f (n + 1)) < 1 / |2 ^ (n + 1)|
[PROOFSTEP]
convert (div_lt_div_right this).2 ((f ^ 2 ^ n).dist_map_map_zero_lt (f ^ 2 ^ n)) using 1
[GOAL]
case h.e'_3
f g : CircleDeg1Lift
n : ℕ
this : 0 < |2 ^ (n + 1)|
⊢ dist (transnumAuxSeq f n) (transnumAuxSeq f (n + 1)) =
    dist (↑(f ^ 2 ^ n) 0 + ↑(f ^ 2 ^ n) 0) (↑(f ^ 2 ^ n) (↑(f ^ 2 ^ n) 0)) / |2 ^ (n + 1)|
[PROOFSTEP]
simp_rw [transnumAuxSeq, Real.dist_eq]
[GOAL]
case h.e'_3
f g : CircleDeg1Lift
n : ℕ
this : 0 < |2 ^ (n + 1)|
⊢ |↑(f ^ 2 ^ n) 0 / 2 ^ n - ↑(f ^ 2 ^ (n + 1)) 0 / 2 ^ (n + 1)| =
    |↑(f ^ 2 ^ n) 0 + ↑(f ^ 2 ^ n) 0 - ↑(f ^ 2 ^ n) (↑(f ^ 2 ^ n) 0)| / |2 ^ (n + 1)|
[PROOFSTEP]
rw [← abs_div, sub_div, pow_succ', pow_succ, ← two_mul, mul_div_mul_left _ _ (two_ne_zero' ℝ), pow_mul, sq, mul_apply]
[GOAL]
f g : CircleDeg1Lift
x : ℕ → ℝ
C : ℝ
H : ∀ (n : ℕ), dist (↑(f ^ n) 0) (x n) ≤ C
⊢ Tendsto (fun n => x (2 ^ n) / 2 ^ n) atTop (𝓝 (τ f))
[PROOFSTEP]
refine' f.tendsto_translationNumber_aux.congr_dist (squeeze_zero (fun _ => dist_nonneg) _ _)
[GOAL]
case refine'_1
f g : CircleDeg1Lift
x : ℕ → ℝ
C : ℝ
H : ∀ (n : ℕ), dist (↑(f ^ n) 0) (x n) ≤ C
⊢ ℕ → ℝ
[PROOFSTEP]
exact fun n => C / 2 ^ n
[GOAL]
case refine'_2
f g : CircleDeg1Lift
x : ℕ → ℝ
C : ℝ
H : ∀ (n : ℕ), dist (↑(f ^ n) 0) (x n) ≤ C
⊢ ∀ (t : ℕ), dist (transnumAuxSeq f t) (x (2 ^ t) / 2 ^ t) ≤ C / 2 ^ t
[PROOFSTEP]
intro n
[GOAL]
case refine'_2
f g : CircleDeg1Lift
x : ℕ → ℝ
C : ℝ
H : ∀ (n : ℕ), dist (↑(f ^ n) 0) (x n) ≤ C
n : ℕ
⊢ dist (transnumAuxSeq f n) (x (2 ^ n) / 2 ^ n) ≤ C / 2 ^ n
[PROOFSTEP]
have : 0 < (2 ^ n : ℝ) := pow_pos zero_lt_two _
[GOAL]
case refine'_2
f g : CircleDeg1Lift
x : ℕ → ℝ
C : ℝ
H : ∀ (n : ℕ), dist (↑(f ^ n) 0) (x n) ≤ C
n : ℕ
this : 0 < 2 ^ n
⊢ dist (transnumAuxSeq f n) (x (2 ^ n) / 2 ^ n) ≤ C / 2 ^ n
[PROOFSTEP]
convert (div_le_div_right this).2 (H (2 ^ n)) using 1
[GOAL]
case h.e'_3
f g : CircleDeg1Lift
x : ℕ → ℝ
C : ℝ
H : ∀ (n : ℕ), dist (↑(f ^ n) 0) (x n) ≤ C
n : ℕ
this : 0 < 2 ^ n
⊢ dist (transnumAuxSeq f n) (x (2 ^ n) / 2 ^ n) = dist (↑(f ^ 2 ^ n) 0) (x (2 ^ n)) / 2 ^ n
[PROOFSTEP]
rw [transnumAuxSeq, Real.dist_eq, ← sub_div, abs_div, abs_of_pos this, Real.dist_eq]
[GOAL]
case refine'_3
f g : CircleDeg1Lift
x : ℕ → ℝ
C : ℝ
H : ∀ (n : ℕ), dist (↑(f ^ n) 0) (x n) ≤ C
⊢ Tendsto (fun n => C / 2 ^ n) atTop (𝓝 0)
[PROOFSTEP]
exact mul_zero C ▸ tendsto_const_nhds.mul <| tendsto_inv_atTop_zero.comp <| tendsto_pow_atTop_atTop_of_one_lt one_lt_two
[GOAL]
f g : CircleDeg1Lift
⊢ Tendsto (fun n => (↑1)^[n] 0 / ↑n) atTop (𝓝 0)
[PROOFSTEP]
simp [tendsto_const_nhds]
[GOAL]
f✝ g✝ f g : CircleDeg1Lift
h : Commute f g
⊢ τ (f * g) = τ f + τ g
[PROOFSTEP]
refine tendsto_nhds_unique ?_ (f.tendsto_translationNumber_aux.add g.tendsto_translationNumber_aux)
[GOAL]
f✝ g✝ f g : CircleDeg1Lift
h : Commute f g
⊢ Tendsto (fun x => transnumAuxSeq f x + transnumAuxSeq g x) atTop (𝓝 (τ (f * g)))
[PROOFSTEP]
simp only [transnumAuxSeq, ← add_div]
[GOAL]
f✝ g✝ f g : CircleDeg1Lift
h : Commute f g
⊢ Tendsto (fun x => (↑(f ^ 2 ^ x) 0 + ↑(g ^ 2 ^ x) 0) / 2 ^ x) atTop (𝓝 (τ (f * g)))
[PROOFSTEP]
refine (f * g).tendsto_translationNumber_of_dist_bounded_aux (fun n ↦ (f ^ n) 0 + (g ^ n) 0) 1 fun n ↦ ?_
[GOAL]
f✝ g✝ f g : CircleDeg1Lift
h : Commute f g
n : ℕ
⊢ dist (↑((f * g) ^ n) 0) ((fun n => ↑(f ^ n) 0 + ↑(g ^ n) 0) n) ≤ 1
[PROOFSTEP]
rw [h.mul_pow, dist_comm]
[GOAL]
f✝ g✝ f g : CircleDeg1Lift
h : Commute f g
n : ℕ
⊢ dist ((fun n => ↑(f ^ n) 0 + ↑(g ^ n) 0) n) (↑(f ^ n * g ^ n) 0) ≤ 1
[PROOFSTEP]
exact le_of_lt ((f ^ n).dist_map_map_zero_lt (g ^ n))
[GOAL]
f✝ g : CircleDeg1Lift
f : CircleDeg1Liftˣ
⊢ τ ↑f⁻¹ + τ ↑f = 0
[PROOFSTEP]
simp [← translationNumber_mul_of_commute (Commute.refl _).units_inv_left]
[GOAL]
f g : CircleDeg1Lift
⊢ τ (f ^ 0) = ↑0 * τ f
[PROOFSTEP]
simp
[GOAL]
f g : CircleDeg1Lift
n : ℕ
⊢ τ (f ^ (n + 1)) = ↑(n + 1) * τ f
[PROOFSTEP]
rw [pow_succ', translationNumber_mul_of_commute (Commute.pow_self f n), translationNumber_pow n, Nat.cast_add_one,
  add_mul, one_mul]
[GOAL]
f✝ g : CircleDeg1Lift
f : CircleDeg1Liftˣ
n : ℕ
⊢ τ ↑(f ^ ↑n) = ↑↑n * τ ↑f
[PROOFSTEP]
simp [translationNumber_pow f n]
[GOAL]
f✝ g : CircleDeg1Lift
f : CircleDeg1Liftˣ
n : ℕ
⊢ τ ↑(f ^ -[n+1]) = ↑-[n+1] * τ ↑f
[PROOFSTEP]
simp
[GOAL]
f✝ g : CircleDeg1Lift
f : CircleDeg1Liftˣ
n : ℕ
⊢ -((↑n + 1) * τ ↑f) = (-1 + -↑n) * τ ↑f
[PROOFSTEP]
ring
[GOAL]
f g : CircleDeg1Lift
⊢ Tendsto (fun n => ↑(f ^ (n + 1)) 0 / (↑n + 1)) atTop (𝓝 (τ f))
[PROOFSTEP]
refine'
  tendsto_iff_dist_tendsto_zero.2 <|
    squeeze_zero (fun _ => dist_nonneg) (fun n => _)
      ((tendsto_const_div_atTop_nhds_0_nat 1).comp (tendsto_add_atTop_nat 1))
[GOAL]
f g : CircleDeg1Lift
n : ℕ
⊢ dist (↑(f ^ (n + 1)) 0 / (↑n + 1)) (τ f) ≤ ((fun n => 1 / ↑n) ∘ fun a => a + 1) n
[PROOFSTEP]
dsimp
[GOAL]
f g : CircleDeg1Lift
n : ℕ
⊢ dist (↑(f ^ (n + 1)) 0 / (↑n + 1)) (τ f) ≤ 1 / ↑(n + 1)
[PROOFSTEP]
have : (0 : ℝ) < n + 1 := n.cast_add_one_pos
[GOAL]
f g : CircleDeg1Lift
n : ℕ
this : 0 < ↑n + 1
⊢ dist (↑(f ^ (n + 1)) 0 / (↑n + 1)) (τ f) ≤ 1 / ↑(n + 1)
[PROOFSTEP]
rw [Real.dist_eq, div_sub' _ _ _ (ne_of_gt this), abs_div, ← Real.dist_eq, abs_of_pos this, Nat.cast_add_one,
  div_le_div_right this, ← Nat.cast_add_one]
[GOAL]
f g : CircleDeg1Lift
n : ℕ
this : 0 < ↑n + 1
⊢ dist (↑(f ^ (n + 1)) 0) (↑(n + 1) * τ f) ≤ 1
[PROOFSTEP]
apply dist_pow_map_zero_mul_translationNumber_le
[GOAL]
f g : CircleDeg1Lift
⊢ Tendsto (fun n => ↑(f ^ (n + 1)) 0 / ↑(n + 1)) atTop (𝓝 (τ f))
[PROOFSTEP]
exact_mod_cast f.tendsto_translation_number₀'
[GOAL]
f g : CircleDeg1Lift
x : ℝ
⊢ Tendsto (fun n => (↑(f ^ n) x - x) / ↑n) atTop (𝓝 (τ f))
[PROOFSTEP]
rw [← translationNumber_conj_eq' (translate <| Multiplicative.ofAdd x)]
[GOAL]
f g : CircleDeg1Lift
x : ℝ
⊢ Tendsto (fun n => (↑(f ^ n) x - x) / ↑n) atTop
    (𝓝 (τ (↑(↑translate (↑Multiplicative.ofAdd x))⁻¹ * f * ↑(↑translate (↑Multiplicative.ofAdd x)))))
[PROOFSTEP]
refine (tendsto_translation_number₀ _).congr fun n ↦ ?_
[GOAL]
f g : CircleDeg1Lift
x : ℝ
n : ℕ
⊢ ↑((↑(↑translate (↑Multiplicative.ofAdd x))⁻¹ * f * ↑(↑translate (↑Multiplicative.ofAdd x))) ^ n) 0 / ↑n =
    (↑(f ^ n) x - x) / ↑n
[PROOFSTEP]
simp [sub_eq_neg_add, Units.conj_pow']
[GOAL]
f g : CircleDeg1Lift
x : ℝ
⊢ Tendsto (fun n => (↑(f ^ (n + 1)) x - x) / (↑n + 1)) atTop (𝓝 (τ f))
[PROOFSTEP]
exact_mod_cast (tendsto_add_atTop_iff_nat 1).2 (f.tendsto_translationNumber x)
[GOAL]
f g : CircleDeg1Lift
x : ℝ
⊢ Tendsto (fun n => (↑↑(↑translate (↑Multiplicative.ofAdd x)))^[n + 1] 0 / (↑n + 1)) atTop (𝓝 x)
[PROOFSTEP]
simp only [translate_iterate, translate_apply, add_zero, Nat.cast_succ,
  mul_div_cancel_left (G₀ := ℝ) _ (Nat.cast_add_one_ne_zero _), tendsto_const_nhds]
[GOAL]
f g : CircleDeg1Lift
x : ℝ
m : ℤ
h : x + ↑m ≤ ↑f x
n : ℕ
⊢ x + ↑m * (↑n + 1) ≤ ↑(f ^ (n + 1)) x
[PROOFSTEP]
simp only [coe_pow, mul_comm (m : ℝ), ← Nat.cast_add_one, f.le_iterate_of_add_int_le_map h]
[GOAL]
f g : CircleDeg1Lift
x : ℝ
⊢ ↑f x < x + ↑⌊τ f⌋ + 1
[PROOFSTEP]
rw [add_assoc]
[GOAL]
f g : CircleDeg1Lift
x : ℝ
⊢ ↑f x < x + (↑⌊τ f⌋ + 1)
[PROOFSTEP]
norm_cast
[GOAL]
f g : CircleDeg1Lift
x : ℝ
⊢ ↑f x < x + ↑(⌊τ f⌋ + 1)
[PROOFSTEP]
refine' map_lt_of_translationNumber_lt_int _ _ _
[GOAL]
f g : CircleDeg1Lift
x : ℝ
⊢ τ f < ↑(⌊τ f⌋ + 1)
[PROOFSTEP]
push_cast
[GOAL]
f g : CircleDeg1Lift
x : ℝ
⊢ τ f < ↑⌊τ f⌋ + 1
[PROOFSTEP]
exact lt_floor_add_one _
[GOAL]
f g : CircleDeg1Lift
x : ℝ
⊢ x + ↑⌊τ f⌋ + 1 ≤ x + τ f + 1
[PROOFSTEP]
gcongr
[GOAL]
case bc.bc
f g : CircleDeg1Lift
x : ℝ
⊢ ↑⌊τ f⌋ ≤ τ f
[PROOFSTEP]
apply floor_le
[GOAL]
f g : CircleDeg1Lift
x : ℝ
n : ℕ
m : ℤ
h : ↑(f ^ n) x = x + ↑m
hn : 0 < n
⊢ τ f = ↑m / ↑n
[PROOFSTEP]
have := (f ^ n).translationNumber_of_eq_add_int h
[GOAL]
f g : CircleDeg1Lift
x : ℝ
n : ℕ
m : ℤ
h : ↑(f ^ n) x = x + ↑m
hn : 0 < n
this : τ (f ^ n) = ↑m
⊢ τ f = ↑m / ↑n
[PROOFSTEP]
rwa [translationNumber_pow, mul_comm, ← eq_div_iff] at this 
[GOAL]
f g : CircleDeg1Lift
x : ℝ
n : ℕ
m : ℤ
h : ↑(f ^ n) x = x + ↑m
hn : 0 < n
this : τ f * ↑n = ↑m
⊢ ↑n ≠ 0
[PROOFSTEP]
exact Nat.cast_ne_zero.2 (ne_of_gt hn)
[GOAL]
f g : CircleDeg1Lift
hf : Continuous ↑f
z : ℝ
hz : ∀ (x : ℝ), ↑f x < x + z
⊢ τ f < z
[PROOFSTEP]
obtain ⟨x, -, hx⟩ : ∃ x ∈ Icc (0 : ℝ) 1, ∀ y ∈ Icc (0 : ℝ) 1, f y - y ≤ f x - x :=
  isCompact_Icc.exists_forall_ge (nonempty_Icc.2 zero_le_one) (hf.sub continuous_id).continuousOn
[GOAL]
case intro.intro
f g : CircleDeg1Lift
hf : Continuous ↑f
z : ℝ
hz : ∀ (x : ℝ), ↑f x < x + z
x : ℝ
hx : ∀ (y : ℝ), y ∈ Icc 0 1 → ↑f y - y ≤ ↑f x - x
⊢ τ f < z
[PROOFSTEP]
refine' lt_of_le_of_lt _ (sub_lt_iff_lt_add'.2 <| hz x)
[GOAL]
case intro.intro
f g : CircleDeg1Lift
hf : Continuous ↑f
z : ℝ
hz : ∀ (x : ℝ), ↑f x < x + z
x : ℝ
hx : ∀ (y : ℝ), y ∈ Icc 0 1 → ↑f y - y ≤ ↑f x - x
⊢ τ f ≤ ↑f x - x
[PROOFSTEP]
apply translationNumber_le_of_le_add
[GOAL]
case intro.intro.hz
f g : CircleDeg1Lift
hf : Continuous ↑f
z : ℝ
hz : ∀ (x : ℝ), ↑f x < x + z
x : ℝ
hx : ∀ (y : ℝ), y ∈ Icc 0 1 → ↑f y - y ≤ ↑f x - x
⊢ ∀ (x_1 : ℝ), ↑f x_1 ≤ x_1 + (↑f x - x)
[PROOFSTEP]
simp only [← sub_le_iff_le_add']
[GOAL]
case intro.intro.hz
f g : CircleDeg1Lift
hf : Continuous ↑f
z : ℝ
hz : ∀ (x : ℝ), ↑f x < x + z
x : ℝ
hx : ∀ (y : ℝ), y ∈ Icc 0 1 → ↑f y - y ≤ ↑f x - x
⊢ ∀ (x_1 : ℝ), ↑f x_1 - x_1 ≤ ↑f x - x
[PROOFSTEP]
exact f.forall_map_sub_of_Icc (fun a => a ≤ f x - x) hx
[GOAL]
f g : CircleDeg1Lift
hf : Continuous ↑f
z : ℝ
hz : ∀ (x : ℝ), x + z < ↑f x
⊢ z < τ f
[PROOFSTEP]
obtain ⟨x, -, hx⟩ : ∃ x ∈ Icc (0 : ℝ) 1, ∀ y ∈ Icc (0 : ℝ) 1, f x - x ≤ f y - y
[GOAL]
f g : CircleDeg1Lift
hf : Continuous ↑f
z : ℝ
hz : ∀ (x : ℝ), x + z < ↑f x
⊢ ∃ x, x ∈ Icc 0 1 ∧ ∀ (y : ℝ), y ∈ Icc 0 1 → ↑f x - x ≤ ↑f y - y
case intro.intro
f g : CircleDeg1Lift
hf : Continuous ↑f
z : ℝ
hz : ∀ (x : ℝ), x + z < ↑f x
x : ℝ
hx : ∀ (y : ℝ), y ∈ Icc 0 1 → ↑f x - x ≤ ↑f y - y
⊢ z < τ f
[PROOFSTEP]
exact isCompact_Icc.exists_forall_le (nonempty_Icc.2 zero_le_one) (hf.sub continuous_id).continuousOn
[GOAL]
case intro.intro
f g : CircleDeg1Lift
hf : Continuous ↑f
z : ℝ
hz : ∀ (x : ℝ), x + z < ↑f x
x : ℝ
hx : ∀ (y : ℝ), y ∈ Icc 0 1 → ↑f x - x ≤ ↑f y - y
⊢ z < τ f
[PROOFSTEP]
refine' lt_of_lt_of_le (lt_sub_iff_add_lt'.2 <| hz x) _
[GOAL]
case intro.intro
f g : CircleDeg1Lift
hf : Continuous ↑f
z : ℝ
hz : ∀ (x : ℝ), x + z < ↑f x
x : ℝ
hx : ∀ (y : ℝ), y ∈ Icc 0 1 → ↑f x - x ≤ ↑f y - y
⊢ ↑f x - x ≤ τ f
[PROOFSTEP]
apply le_translationNumber_of_add_le
[GOAL]
case intro.intro.hz
f g : CircleDeg1Lift
hf : Continuous ↑f
z : ℝ
hz : ∀ (x : ℝ), x + z < ↑f x
x : ℝ
hx : ∀ (y : ℝ), y ∈ Icc 0 1 → ↑f x - x ≤ ↑f y - y
⊢ ∀ (x_1 : ℝ), x_1 + (↑f x - x) ≤ ↑f x_1
[PROOFSTEP]
simp only [← le_sub_iff_add_le']
[GOAL]
case intro.intro.hz
f g : CircleDeg1Lift
hf : Continuous ↑f
z : ℝ
hz : ∀ (x : ℝ), x + z < ↑f x
x : ℝ
hx : ∀ (y : ℝ), y ∈ Icc 0 1 → ↑f x - x ≤ ↑f y - y
⊢ ∀ (x_1 : ℝ), ↑f x - x ≤ ↑f x_1 - x_1
[PROOFSTEP]
exact f.forall_map_sub_of_Icc _ hx
[GOAL]
f g : CircleDeg1Lift
hf : Continuous ↑f
⊢ ∃ x, ↑f x = x + τ f
[PROOFSTEP]
obtain ⟨a, ha⟩ : ∃ x, f x ≤ x + τ f := by
  by_contra' H
  exact lt_irrefl _ (f.lt_translationNumber_of_forall_add_lt hf H)
[GOAL]
f g : CircleDeg1Lift
hf : Continuous ↑f
⊢ ∃ x, ↑f x ≤ x + τ f
[PROOFSTEP]
by_contra' H
[GOAL]
f g : CircleDeg1Lift
hf : Continuous ↑f
H : ∀ (x : ℝ), x + τ f < ↑f x
⊢ False
[PROOFSTEP]
exact lt_irrefl _ (f.lt_translationNumber_of_forall_add_lt hf H)
[GOAL]
case intro
f g : CircleDeg1Lift
hf : Continuous ↑f
a : ℝ
ha : ↑f a ≤ a + τ f
⊢ ∃ x, ↑f x = x + τ f
[PROOFSTEP]
obtain ⟨b, hb⟩ : ∃ x, x + τ f ≤ f x := by
  by_contra' H
  exact lt_irrefl _ (f.translationNumber_lt_of_forall_lt_add hf H)
[GOAL]
f g : CircleDeg1Lift
hf : Continuous ↑f
a : ℝ
ha : ↑f a ≤ a + τ f
⊢ ∃ x, x + τ f ≤ ↑f x
[PROOFSTEP]
by_contra' H
[GOAL]
f g : CircleDeg1Lift
hf : Continuous ↑f
a : ℝ
ha : ↑f a ≤ a + τ f
H : ∀ (x : ℝ), ↑f x < x + τ f
⊢ False
[PROOFSTEP]
exact lt_irrefl _ (f.translationNumber_lt_of_forall_lt_add hf H)
[GOAL]
case intro.intro
f g : CircleDeg1Lift
hf : Continuous ↑f
a : ℝ
ha : ↑f a ≤ a + τ f
b : ℝ
hb : b + τ f ≤ ↑f b
⊢ ∃ x, ↑f x = x + τ f
[PROOFSTEP]
exact intermediate_value_univ₂ hf (continuous_id.add continuous_const) ha hb
[GOAL]
f g : CircleDeg1Lift
hf : Continuous ↑f
m : ℤ
⊢ τ f = ↑m ↔ ∃ x, ↑f x = x + ↑m
[PROOFSTEP]
constructor
[GOAL]
case mp
f g : CircleDeg1Lift
hf : Continuous ↑f
m : ℤ
⊢ τ f = ↑m → ∃ x, ↑f x = x + ↑m
[PROOFSTEP]
intro h
[GOAL]
case mp
f g : CircleDeg1Lift
hf : Continuous ↑f
m : ℤ
h : τ f = ↑m
⊢ ∃ x, ↑f x = x + ↑m
[PROOFSTEP]
simp only [← h]
[GOAL]
case mp
f g : CircleDeg1Lift
hf : Continuous ↑f
m : ℤ
h : τ f = ↑m
⊢ ∃ x, ↑f x = x + τ f
[PROOFSTEP]
exact f.exists_eq_add_translationNumber hf
[GOAL]
case mpr
f g : CircleDeg1Lift
hf : Continuous ↑f
m : ℤ
⊢ (∃ x, ↑f x = x + ↑m) → τ f = ↑m
[PROOFSTEP]
rintro ⟨x, hx⟩
[GOAL]
case mpr.intro
f g : CircleDeg1Lift
hf : Continuous ↑f
m : ℤ
x : ℝ
hx : ↑f x = x + ↑m
⊢ τ f = ↑m
[PROOFSTEP]
exact f.translationNumber_of_eq_add_int hx
[GOAL]
f g : CircleDeg1Lift
hf : Continuous ↑f
n : ℕ
⊢ Continuous ↑(f ^ n)
[PROOFSTEP]
rw [coe_pow]
[GOAL]
f g : CircleDeg1Lift
hf : Continuous ↑f
n : ℕ
⊢ Continuous (↑f)^[n]
[PROOFSTEP]
exact hf.iterate n
[GOAL]
f g : CircleDeg1Lift
hf : Continuous ↑f
m : ℤ
n : ℕ
hn : 0 < n
⊢ τ f = ↑m / ↑n ↔ ∃ x, ↑(f ^ n) x = x + ↑m
[PROOFSTEP]
rw [eq_div_iff, mul_comm, ← translationNumber_pow] <;> [skip; exact ne_of_gt (Nat.cast_pos.2 hn)]
[GOAL]
f g : CircleDeg1Lift
hf : Continuous ↑f
m : ℤ
n : ℕ
hn : 0 < n
⊢ τ f = ↑m / ↑n ↔ ∃ x, ↑(f ^ n) x = x + ↑m
[PROOFSTEP]
rw [eq_div_iff, mul_comm, ← translationNumber_pow]
[GOAL]
f g : CircleDeg1Lift
hf : Continuous ↑f
m : ℤ
n : ℕ
hn : 0 < n
⊢ τ (f ^ n) = ↑m ↔ ∃ x, ↑(f ^ n) x = x + ↑m
[PROOFSTEP]
skip
[GOAL]
f g : CircleDeg1Lift
hf : Continuous ↑f
m : ℤ
n : ℕ
hn : 0 < n
⊢ ↑n ≠ 0
[PROOFSTEP]
exact ne_of_gt (Nat.cast_pos.2 hn)
[GOAL]
f g : CircleDeg1Lift
hf : Continuous ↑f
m : ℤ
n : ℕ
hn : 0 < n
⊢ τ (f ^ n) = ↑m ↔ ∃ x, ↑(f ^ n) x = x + ↑m
[PROOFSTEP]
exact (f ^ n).translationNumber_eq_int_iff (f.continuous_pow hf n)
[GOAL]
f g : CircleDeg1Lift
G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (↑f₁ g) = τ (↑f₂ g)
⊢ ∃ F, ∀ (g : G), Semiconj ↑F ↑(↑f₁ g) ↑(↑f₂ g)
[PROOFSTEP]
have : ∀ x, BddAbove (range fun g => f₂ g⁻¹ (f₁ g x)) :=
  by
  refine' fun x => ⟨x + 2, _⟩
  rintro _ ⟨g, rfl⟩
  have : τ (f₂ g⁻¹) = -τ (f₂ g) := by
    rw [← MonoidHom.coe_toHomUnits, MonoidHom.map_inv, translationNumber_units_inv, MonoidHom.coe_toHomUnits]
  calc
    f₂ g⁻¹ (f₁ g x) ≤ f₂ g⁻¹ (x + τ (f₁ g) + 1) := mono _ (map_lt_add_translationNumber_add_one _ _).le
    _ = f₂ g⁻¹ (x + τ (f₂ g)) + 1 := by rw [h, map_add_one]
    _ ≤ x + τ (f₂ g) + τ (f₂ g⁻¹) + 1 + 1 := (add_le_add_right (map_lt_add_translationNumber_add_one _ _).le _)
    _ = x + 2 := by
      simp [this, add_assoc, one_add_one_eq_two]
        -- We have a theorem about actions by `OrderIso`, so we introduce auxiliary maps
          -- to `ℝ ≃o ℝ`.
[GOAL]
f g : CircleDeg1Lift
G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (↑f₁ g) = τ (↑f₂ g)
⊢ ∀ (x : ℝ), BddAbove (range fun g => ↑(↑f₂ g⁻¹) (↑(↑f₁ g) x))
[PROOFSTEP]
refine' fun x => ⟨x + 2, _⟩
[GOAL]
f g : CircleDeg1Lift
G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (↑f₁ g) = τ (↑f₂ g)
x : ℝ
⊢ x + 2 ∈ upperBounds (range fun g => ↑(↑f₂ g⁻¹) (↑(↑f₁ g) x))
[PROOFSTEP]
rintro _ ⟨g, rfl⟩
[GOAL]
case intro
f g✝ : CircleDeg1Lift
G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (↑f₁ g) = τ (↑f₂ g)
x : ℝ
g : G
⊢ (fun g => ↑(↑f₂ g⁻¹) (↑(↑f₁ g) x)) g ≤ x + 2
[PROOFSTEP]
have : τ (f₂ g⁻¹) = -τ (f₂ g) := by
  rw [← MonoidHom.coe_toHomUnits, MonoidHom.map_inv, translationNumber_units_inv, MonoidHom.coe_toHomUnits]
[GOAL]
f g✝ : CircleDeg1Lift
G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (↑f₁ g) = τ (↑f₂ g)
x : ℝ
g : G
⊢ τ (↑f₂ g⁻¹) = -τ (↑f₂ g)
[PROOFSTEP]
rw [← MonoidHom.coe_toHomUnits, MonoidHom.map_inv, translationNumber_units_inv, MonoidHom.coe_toHomUnits]
[GOAL]
case intro
f g✝ : CircleDeg1Lift
G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (↑f₁ g) = τ (↑f₂ g)
x : ℝ
g : G
this : τ (↑f₂ g⁻¹) = -τ (↑f₂ g)
⊢ (fun g => ↑(↑f₂ g⁻¹) (↑(↑f₁ g) x)) g ≤ x + 2
[PROOFSTEP]
calc
  f₂ g⁻¹ (f₁ g x) ≤ f₂ g⁻¹ (x + τ (f₁ g) + 1) := mono _ (map_lt_add_translationNumber_add_one _ _).le
  _ = f₂ g⁻¹ (x + τ (f₂ g)) + 1 := by rw [h, map_add_one]
  _ ≤ x + τ (f₂ g) + τ (f₂ g⁻¹) + 1 + 1 := (add_le_add_right (map_lt_add_translationNumber_add_one _ _).le _)
  _ = x + 2 := by
    simp [this, add_assoc, one_add_one_eq_two]
      -- We have a theorem about actions by `OrderIso`, so we introduce auxiliary maps
        -- to `ℝ ≃o ℝ`.
[GOAL]
f g✝ : CircleDeg1Lift
G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (↑f₁ g) = τ (↑f₂ g)
x : ℝ
g : G
this : τ (↑f₂ g⁻¹) = -τ (↑f₂ g)
⊢ ↑(↑f₂ g⁻¹) (x + τ (↑f₁ g) + 1) = ↑(↑f₂ g⁻¹) (x + τ (↑f₂ g)) + 1
[PROOFSTEP]
rw [h, map_add_one]
[GOAL]
f g✝ : CircleDeg1Lift
G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (↑f₁ g) = τ (↑f₂ g)
x : ℝ
g : G
this : τ (↑f₂ g⁻¹) = -τ (↑f₂ g)
⊢ x + τ (↑f₂ g) + τ (↑f₂ g⁻¹) + 1 + 1 = x + 2
[PROOFSTEP]
simp [this, add_assoc, one_add_one_eq_two]
  -- We have a theorem about actions by `OrderIso`, so we introduce auxiliary maps
    -- to `ℝ ≃o ℝ`.
[GOAL]
f g : CircleDeg1Lift
G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (↑f₁ g) = τ (↑f₂ g)
this : ∀ (x : ℝ), BddAbove (range fun g => ↑(↑f₂ g⁻¹) (↑(↑f₁ g) x))
⊢ ∃ F, ∀ (g : G), Semiconj ↑F ↑(↑f₁ g) ↑(↑f₂ g)
[PROOFSTEP]
set F₁ := toOrderIso.comp f₁.toHomUnits
[GOAL]
f g : CircleDeg1Lift
G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (↑f₁ g) = τ (↑f₂ g)
this : ∀ (x : ℝ), BddAbove (range fun g => ↑(↑f₂ g⁻¹) (↑(↑f₁ g) x))
F₁ : G →* ℝ ≃o ℝ := MonoidHom.comp toOrderIso (MonoidHom.toHomUnits f₁)
⊢ ∃ F, ∀ (g : G), Semiconj ↑F ↑(↑f₁ g) ↑(↑f₂ g)
[PROOFSTEP]
set F₂ := toOrderIso.comp f₂.toHomUnits
[GOAL]
f g : CircleDeg1Lift
G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (↑f₁ g) = τ (↑f₂ g)
this : ∀ (x : ℝ), BddAbove (range fun g => ↑(↑f₂ g⁻¹) (↑(↑f₁ g) x))
F₁ : G →* ℝ ≃o ℝ := MonoidHom.comp toOrderIso (MonoidHom.toHomUnits f₁)
F₂ : G →* ℝ ≃o ℝ := MonoidHom.comp toOrderIso (MonoidHom.toHomUnits f₂)
⊢ ∃ F, ∀ (g : G), Semiconj ↑F ↑(↑f₁ g) ↑(↑f₂ g)
[PROOFSTEP]
have hF₁ : ∀ g, ⇑(F₁ g) = f₁ g := fun _ => rfl
[GOAL]
f g : CircleDeg1Lift
G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (↑f₁ g) = τ (↑f₂ g)
this : ∀ (x : ℝ), BddAbove (range fun g => ↑(↑f₂ g⁻¹) (↑(↑f₁ g) x))
F₁ : G →* ℝ ≃o ℝ := MonoidHom.comp toOrderIso (MonoidHom.toHomUnits f₁)
F₂ : G →* ℝ ≃o ℝ := MonoidHom.comp toOrderIso (MonoidHom.toHomUnits f₂)
hF₁ : ∀ (g : G), ↑(↑F₁ g) = ↑(↑f₁ g)
⊢ ∃ F, ∀ (g : G), Semiconj ↑F ↑(↑f₁ g) ↑(↑f₂ g)
[PROOFSTEP]
have hF₂ : ∀ g, ⇑(F₂ g) = f₂ g := fun _ => rfl
[GOAL]
f g : CircleDeg1Lift
G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (↑f₁ g) = τ (↑f₂ g)
this : ∀ (x : ℝ), BddAbove (range fun g => ↑(↑f₂ g⁻¹) (↑(↑f₁ g) x))
F₁ : G →* ℝ ≃o ℝ := MonoidHom.comp toOrderIso (MonoidHom.toHomUnits f₁)
F₂ : G →* ℝ ≃o ℝ := MonoidHom.comp toOrderIso (MonoidHom.toHomUnits f₂)
hF₁ : ∀ (g : G), ↑(↑F₁ g) = ↑(↑f₁ g)
hF₂ : ∀ (g : G), ↑(↑F₂ g) = ↑(↑f₂ g)
⊢ ∃ F, ∀ (g : G), Semiconj ↑F ↑(↑f₁ g) ↑(↑f₂ g)
[PROOFSTEP]
refine' ⟨⟨⟨_, fun x y hxy => _⟩, fun x => _⟩, csSup_div_semiconj F₂ F₁ fun x => _⟩
[GOAL]
case refine'_1
f g : CircleDeg1Lift
G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (↑f₁ g) = τ (↑f₂ g)
this : ∀ (x : ℝ), BddAbove (range fun g => ↑(↑f₂ g⁻¹) (↑(↑f₁ g) x))
F₁ : G →* ℝ ≃o ℝ := MonoidHom.comp toOrderIso (MonoidHom.toHomUnits f₁)
F₂ : G →* ℝ ≃o ℝ := MonoidHom.comp toOrderIso (MonoidHom.toHomUnits f₂)
hF₁ : ∀ (g : G), ↑(↑F₁ g) = ↑(↑f₁ g)
hF₂ : ∀ (g : G), ↑(↑F₂ g) = ↑(↑f₂ g)
x y : ℝ
hxy : x ≤ y
⊢ sSup (range fun g' => ↑(↑F₂ g')⁻¹ (↑(↑F₁ g') x)) ≤ sSup (range fun g' => ↑(↑F₂ g')⁻¹ (↑(↑F₁ g') y))
[PROOFSTEP]
simp only [hF₁, hF₂, ← map_inv, coe_mk]
[GOAL]
case refine'_2
f g : CircleDeg1Lift
G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (↑f₁ g) = τ (↑f₂ g)
this : ∀ (x : ℝ), BddAbove (range fun g => ↑(↑f₂ g⁻¹) (↑(↑f₁ g) x))
F₁ : G →* ℝ ≃o ℝ := MonoidHom.comp toOrderIso (MonoidHom.toHomUnits f₁)
F₂ : G →* ℝ ≃o ℝ := MonoidHom.comp toOrderIso (MonoidHom.toHomUnits f₂)
hF₁ : ∀ (g : G), ↑(↑F₁ g) = ↑(↑f₁ g)
hF₂ : ∀ (g : G), ↑(↑F₂ g) = ↑(↑f₂ g)
x : ℝ
⊢ OrderHom.toFun
      { toFun := fun x => sSup (range fun g' => ↑(↑F₂ g')⁻¹ (↑(↑F₁ g') x)),
        monotone' :=
          (_ :
            ∀ (x y : ℝ),
              x ≤ y →
                sSup (range fun g' => ↑(↑F₂ g')⁻¹ (↑(↑F₁ g') x)) ≤ sSup (range fun g' => ↑(↑F₂ g')⁻¹ (↑(↑F₁ g') y))) }
      (x + 1) =
    OrderHom.toFun
        { toFun := fun x => sSup (range fun g' => ↑(↑F₂ g')⁻¹ (↑(↑F₁ g') x)),
          monotone' :=
            (_ :
              ∀ (x y : ℝ),
                x ≤ y →
                  sSup (range fun g' => ↑(↑F₂ g')⁻¹ (↑(↑F₁ g') x)) ≤ sSup (range fun g' => ↑(↑F₂ g')⁻¹ (↑(↑F₁ g') y))) }
        x +
      1
[PROOFSTEP]
simp only [hF₁, hF₂, ← map_inv, coe_mk]
[GOAL]
case refine'_3
f g : CircleDeg1Lift
G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (↑f₁ g) = τ (↑f₂ g)
this : ∀ (x : ℝ), BddAbove (range fun g => ↑(↑f₂ g⁻¹) (↑(↑f₁ g) x))
F₁ : G →* ℝ ≃o ℝ := MonoidHom.comp toOrderIso (MonoidHom.toHomUnits f₁)
F₂ : G →* ℝ ≃o ℝ := MonoidHom.comp toOrderIso (MonoidHom.toHomUnits f₂)
hF₁ : ∀ (g : G), ↑(↑F₁ g) = ↑(↑f₁ g)
hF₂ : ∀ (g : G), ↑(↑F₂ g) = ↑(↑f₂ g)
x : ℝ
⊢ BddAbove (range fun g => ↑(↑F₂ g)⁻¹ (↑(↑F₁ g) x))
[PROOFSTEP]
simp only [hF₁, hF₂, ← map_inv, coe_mk]
[GOAL]
case refine'_1
f g : CircleDeg1Lift
G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (↑f₁ g) = τ (↑f₂ g)
this : ∀ (x : ℝ), BddAbove (range fun g => ↑(↑f₂ g⁻¹) (↑(↑f₁ g) x))
F₁ : G →* ℝ ≃o ℝ := MonoidHom.comp toOrderIso (MonoidHom.toHomUnits f₁)
F₂ : G →* ℝ ≃o ℝ := MonoidHom.comp toOrderIso (MonoidHom.toHomUnits f₂)
hF₁ : ∀ (g : G), ↑(↑F₁ g) = ↑(↑f₁ g)
hF₂ : ∀ (g : G), ↑(↑F₂ g) = ↑(↑f₂ g)
x y : ℝ
hxy : x ≤ y
⊢ sSup (range fun g' => ↑(↑f₂ g'⁻¹) (↑(↑f₁ g') x)) ≤ sSup (range fun g' => ↑(↑f₂ g'⁻¹) (↑(↑f₁ g') y))
[PROOFSTEP]
exact ciSup_mono (this y) fun g => mono _ (mono _ hxy)
[GOAL]
case refine'_2
f g : CircleDeg1Lift
G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (↑f₁ g) = τ (↑f₂ g)
this : ∀ (x : ℝ), BddAbove (range fun g => ↑(↑f₂ g⁻¹) (↑(↑f₁ g) x))
F₁ : G →* ℝ ≃o ℝ := MonoidHom.comp toOrderIso (MonoidHom.toHomUnits f₁)
F₂ : G →* ℝ ≃o ℝ := MonoidHom.comp toOrderIso (MonoidHom.toHomUnits f₂)
hF₁ : ∀ (g : G), ↑(↑F₁ g) = ↑(↑f₁ g)
hF₂ : ∀ (g : G), ↑(↑F₂ g) = ↑(↑f₂ g)
x : ℝ
⊢ sSup (range fun g' => ↑(↑f₂ g'⁻¹) (↑(↑f₁ g') (x + 1))) = sSup (range fun g' => ↑(↑f₂ g'⁻¹) (↑(↑f₁ g') x)) + 1
[PROOFSTEP]
simp only [map_add_one]
[GOAL]
case refine'_2
f g : CircleDeg1Lift
G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (↑f₁ g) = τ (↑f₂ g)
this : ∀ (x : ℝ), BddAbove (range fun g => ↑(↑f₂ g⁻¹) (↑(↑f₁ g) x))
F₁ : G →* ℝ ≃o ℝ := MonoidHom.comp toOrderIso (MonoidHom.toHomUnits f₁)
F₂ : G →* ℝ ≃o ℝ := MonoidHom.comp toOrderIso (MonoidHom.toHomUnits f₂)
hF₁ : ∀ (g : G), ↑(↑F₁ g) = ↑(↑f₁ g)
hF₂ : ∀ (g : G), ↑(↑F₂ g) = ↑(↑f₂ g)
x : ℝ
⊢ sSup (range fun g' => ↑(↑f₂ g'⁻¹) (↑(↑f₁ g') x) + 1) = sSup (range fun g' => ↑(↑f₂ g'⁻¹) (↑(↑f₁ g') x)) + 1
[PROOFSTEP]
exact
  (Monotone.map_ciSup_of_continuousAt (continuousAt_id.add continuousAt_const) (monotone_id.add_const (1 : ℝ))
      (this x)).symm
[GOAL]
case refine'_3
f g : CircleDeg1Lift
G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (↑f₁ g) = τ (↑f₂ g)
this : ∀ (x : ℝ), BddAbove (range fun g => ↑(↑f₂ g⁻¹) (↑(↑f₁ g) x))
F₁ : G →* ℝ ≃o ℝ := MonoidHom.comp toOrderIso (MonoidHom.toHomUnits f₁)
F₂ : G →* ℝ ≃o ℝ := MonoidHom.comp toOrderIso (MonoidHom.toHomUnits f₂)
hF₁ : ∀ (g : G), ↑(↑F₁ g) = ↑(↑f₁ g)
hF₂ : ∀ (g : G), ↑(↑F₂ g) = ↑(↑f₂ g)
x : ℝ
⊢ BddAbove (range fun g => ↑(↑f₂ g⁻¹) (↑(↑f₁ g) x))
[PROOFSTEP]
exact this x
[GOAL]
f g : CircleDeg1Lift
f₁ f₂ : CircleDeg1Liftˣ
h : τ ↑f₁ = τ ↑f₂
n : Multiplicative ℤ
⊢ τ (↑(MonoidHom.comp (Units.coeHom CircleDeg1Lift) (↑(zpowersHom CircleDeg1Liftˣ) f₁)) n) =
    τ (↑(MonoidHom.comp (Units.coeHom CircleDeg1Lift) (↑(zpowersHom CircleDeg1Liftˣ) f₂)) n)
[PROOFSTEP]
simp [h]
[GOAL]
f g : CircleDeg1Lift
f₁ f₂ : CircleDeg1Liftˣ
h : τ ↑f₁ = τ ↑f₂
this :
  ∀ (n : Multiplicative ℤ),
    τ (↑(MonoidHom.comp (Units.coeHom CircleDeg1Lift) (↑(zpowersHom CircleDeg1Liftˣ) f₁)) n) =
      τ (↑(MonoidHom.comp (Units.coeHom CircleDeg1Lift) (↑(zpowersHom CircleDeg1Liftˣ) f₂)) n)
F : CircleDeg1Lift
hF :
  ∀ (g : Multiplicative ℤ),
    Semiconj ↑F ↑(↑(MonoidHom.comp (Units.coeHom CircleDeg1Lift) (↑(zpowersHom CircleDeg1Liftˣ) f₁)) g)
      ↑(↑(MonoidHom.comp (Units.coeHom CircleDeg1Lift) (↑(zpowersHom CircleDeg1Liftˣ) f₂)) g)
⊢ Semiconj ↑F ↑↑f₁ ↑↑f₂
[PROOFSTEP]
simpa using hF (Multiplicative.ofAdd 1)
[GOAL]
f g f₁ f₂ : CircleDeg1Lift
h₁ : IsUnit f₁
h₂ : IsUnit f₂
h : τ f₁ = τ f₂
⊢ ∃ F, Semiconj ↑F ↑f₁ ↑f₂
[PROOFSTEP]
rcases h₁, h₂ with ⟨⟨f₁, rfl⟩, ⟨f₂, rfl⟩⟩
[GOAL]
case intro.intro
f g : CircleDeg1Lift
f₁ f₂ : CircleDeg1Liftˣ
h : τ ↑f₁ = τ ↑f₂
⊢ ∃ F, Semiconj ↑F ↑↑f₁ ↑↑f₂
[PROOFSTEP]
exact units_semiconj_of_translationNumber_eq h
