-- Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
theorem semiconj_of_group_action_of_forall_translationNumber_eq {G : Type*} [Group G]
    (f₁ f₂ : G →* CircleDeg1Lift) (h : ∀ g, τ (f₁ g) = τ (f₂ g)) :
    ∃ F : CircleDeg1Lift, ∀ g, Semiconj F (f₁ g) (f₂ g)

Proof state:
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)

Tactic:
set F₁ := toOrderIso.comp f₁.toHomUnits

Result:
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 ℝ := toOrderIso.comp f₁.toHomUnits
⊢ ∃ F, ∀ (g : G), Semiconj ⇑F ⇑(f₁ g) ⇑(f₂ g)

Proof state:
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))

Tactic:
rintro _ ⟨g, rfl⟩

Result:
case intro
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

Proof state:
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)

Tactic:
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]

Result:
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)

Proof state:
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))

Tactic:
refine fun x => ⟨x + 2, ?_⟩

Result:
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))

Proof state:
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

Tactic:
simp [this, add_assoc, one_add_one_eq_two]

Result:
no goals

Proof state:
case intro
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

Tactic:
have : τ (f₂ g⁻¹) = -τ (f₂ g) := by
  rw [← MonoidHom.coe_toHomUnits, MonoidHom.map_inv, translationNumber_units_inv,
    MonoidHom.coe_toHomUnits]

Result:
case intro
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