awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
hf : Continuous (X := ℝ) (Y := ℝ) (⇑f : (a : ℝ) → ℝ)
m : ℤ
n : ℕ
hn : 0 < n
rw : τ (f ^ n) = (↑m : ℝ) ↔ ∃ (x : ℝ), (f ^ n : (a : ℝ) → ℝ) x = x + (↑m : ℝ)
⊢ τ f = HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ↔ ∃ (x : ℝ), (f ^ n : (a : ℝ) → ℝ) x = x + (↑m : ℝ)

Tactic:
rw [eq_div_iff, mul_comm, ← translationNumber_pow] <;> [skip; exact ne_of_gt (Nat.cast_pos.2 hn)]

Premises used: Iff.mpr, Nat.cast_pos, ne_of_gt, mul_comm, CircleDeg1Lift.translationNumber_pow, eq_div_iff
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
hf : Continuous (X := ℝ) (Y := ℝ) (⇑f : (a : ℝ) → ℝ)
m : ℤ
n : ℕ
hn : 0 < n
⊢ τ (f ^ n) = (↑m : ℝ) ↔ ∃ (x : ℝ), (f ^ n : (a : ℝ) → ℝ) x = x + (↑m : ℝ)

Tactic:
(f ^ n).translationNumber_eq_int_iff (f.continuous_pow hf n)

Premises used: CircleDeg1Lift.continuous_pow, HPow.hPow, CircleDeg1Lift.translationNumber_eq_int_iff
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
hf : Continuous (X := ℝ) (Y := ℝ) (⇑f : (a : ℝ) → ℝ)
m : ℤ
n : ℕ
hn : 0 < n
⊢ τ (f ^ n) = (↑m : ℝ) ↔ ∃ (x : ℝ), (f ^ n : (a : ℝ) → ℝ) x = x + (↑m : ℝ)

Tactic:
exact (f ^ n).translationNumber_eq_int_iff (f.continuous_pow hf n)

Premises used: CircleDeg1Lift.continuous_pow, HPow.hPow, CircleDeg1Lift.translationNumber_eq_int_iff
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
G : Type u_1
inst : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ ((f₁ : (a : G) → CircleDeg1Lift) g) = τ ((f₂ : (a : G) → CircleDeg1Lift) g)
⊢ ∀ (x : ℝ),
    BddAbove (α := ℝ)
      (range fun (g : G) ↦
        (((f₂ : (a : G) → CircleDeg1Lift) g⁻¹ : CircleDeg1Lift) : (a : ℝ) → ℝ)
          ((((f₁ : (a : G) → CircleDeg1Lift) g : CircleDeg1Lift) : (a : ℝ) → ℝ) x : ℝ))

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

Premises used: BddAbove, Set.Nonempty, HAdd.hAdd, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
G : Type u_1
inst : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ ((f₁ : (a : G) → CircleDeg1Lift) g) = τ ((f₂ : (a : G) → CircleDeg1Lift) g)
refine :
  ∀ (x : ℝ),
    Membership.mem (γ := Set ℝ)
      (upperBounds
        (range fun (g : G) ↦
          (((f₂ : (a : G) → CircleDeg1Lift) g⁻¹ : CircleDeg1Lift) : (a : ℝ) → ℝ)
            ((((f₁ : (a : G) → CircleDeg1Lift) g : CircleDeg1Lift) : (a : ℝ) → ℝ) x : ℝ)))
      (x + 2)
⊢ ∀ (x : ℝ),
    BddAbove (α := ℝ)
      (range fun (g : G) ↦
        (((f₂ : (a : G) → CircleDeg1Lift) g⁻¹ : CircleDeg1Lift) : (a : ℝ) → ℝ)
          ((((f₁ : (a : G) → CircleDeg1Lift) g : CircleDeg1Lift) : (a : ℝ) → ℝ) x : ℝ))

Tactic:
refine fun x => ⟨x + 2, ?_⟩
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
G : Type u_1
inst : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ ((f₁ : (a : G) → CircleDeg1Lift) g) = τ ((f₂ : (a : G) → CircleDeg1Lift) g)
x : ℝ
g : G
rw : τ (↑((f₂.toHomUnits : (a : G) → CircleDeg1Liftˣ) g⁻¹) : CircleDeg1Lift) = -τ ((f₂ : (a : G) → CircleDeg1Lift) g)
rw₁ : τ (↑((f₂.toHomUnits : (a : G) → CircleDeg1Liftˣ) g)⁻¹ : CircleDeg1Lift) = -τ ((f₂ : (a : G) → CircleDeg1Lift) g)
rw₂ : -τ (↑((f₂.toHomUnits : (a : G) → CircleDeg1Liftˣ) g) : CircleDeg1Lift) = -τ ((f₂ : (a : G) → CircleDeg1Lift) g)
rw₃ rw₄ : -τ ((f₂ : (a : G) → CircleDeg1Lift) g) = -τ ((f₂ : (a : G) → CircleDeg1Lift) g)
⊢ τ ((f₂ : (a : G) → CircleDeg1Lift) g⁻¹) = -τ ((f₂ : (a : G) → CircleDeg1Lift) g)

Tactic:
rw [← MonoidHom.coe_toHomUnits, map_inv, translationNumber_units_inv,
        MonoidHom.coe_toHomUnits]

Premises used: map_inv, MonoidHom.coe_toHomUnits, CircleDeg1Lift.translationNumber_units_inv
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
G : Type u_1
inst : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ ((f₁ : (a : G) → CircleDeg1Lift) g) = τ ((f₂ : (a : G) → CircleDeg1Lift) g)
x : ℝ
g : G
⊢ τ ((f₂ : (a : G) → CircleDeg1Lift) g⁻¹) = -τ ((f₂ : (a : G) → CircleDeg1Lift) g)

Tactic:
have : τ (f₂ g⁻¹) = -τ (f₂ g) := by
      rw [← MonoidHom.coe_toHomUnits, map_inv, translationNumber_units_inv,
        MonoidHom.coe_toHomUnits]
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
G : Type u_1
inst : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ ((f₁ : (a : G) → CircleDeg1Lift) g) = τ ((f₂ : (a : G) → CircleDeg1Lift) g)
x : ℝ
g : G
this : τ ((f₂ : (a : G) → CircleDeg1Lift) g⁻¹) = -τ ((f₂ : (a : G) → CircleDeg1Lift) g)
⊢ LE.le (α := ℝ)
    ((((f₂ : (a : G) → CircleDeg1Lift) g⁻¹ : CircleDeg1Lift) : (a : ℝ) → ℝ)
        ((((f₁ : (a : G) → CircleDeg1Lift) g : CircleDeg1Lift) : (a : ℝ) → ℝ) x : ℝ) :
      ℝ)
    ((((f₂ : (a : G) → CircleDeg1Lift) g⁻¹ : CircleDeg1Lift) : (a : ℝ) → ℝ)
        (x + τ ((f₁ : (a : G) → CircleDeg1Lift) g) + 1) :
      ℝ)

Tactic:
mono _ (map_lt_add_translationNumber_add_one _ _).le

Premises used: CircleDeg1Lift.mono, LT.lt.le, CircleDeg1Lift.map_lt_add_translationNumber_add_one
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
G : Type u_1
inst : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ ((f₁ : (a : G) → CircleDeg1Lift) g) = τ ((f₂ : (a : G) → CircleDeg1Lift) g)
x : ℝ
g : G
this : τ ((f₂ : (a : G) → CircleDeg1Lift) g⁻¹) = -τ ((f₂ : (a : G) → CircleDeg1Lift) g)
rw :
  (((f₂ : (a : G) → CircleDeg1Lift) g⁻¹ : CircleDeg1Lift) : (a : ℝ) → ℝ)
      (x + τ ((f₂ : (a : G) → CircleDeg1Lift) g) + 1) =
    HAdd.hAdd (α := ℝ) (β := ℝ)
      ((((f₂ : (a : G) → CircleDeg1Lift) g⁻¹ : CircleDeg1Lift) : (a : ℝ) → ℝ)
          (x + τ ((f₂ : (a : G) → CircleDeg1Lift) g)) :
        ℝ)
      (1 : ℝ)
rw₁ rw₂ :
  HAdd.hAdd (α := ℝ) (β := ℝ)
      ((((f₂ : (a : G) → CircleDeg1Lift) g⁻¹ : CircleDeg1Lift) : (a : ℝ) → ℝ)
          (x + τ ((f₂ : (a : G) → CircleDeg1Lift) g)) :
        ℝ)
      (1 : ℝ) =
    HAdd.hAdd (α := ℝ) (β := ℝ)
      ((((f₂ : (a : G) → CircleDeg1Lift) g⁻¹ : CircleDeg1Lift) : (a : ℝ) → ℝ)
          (x + τ ((f₂ : (a : G) → CircleDeg1Lift) g)) :
        ℝ)
      (1 : ℝ)
⊢ (((f₂ : (a : G) → CircleDeg1Lift) g⁻¹ : CircleDeg1Lift) : (a : ℝ) → ℝ)
      (x + τ ((f₁ : (a : G) → CircleDeg1Lift) g) + 1) =
    HAdd.hAdd (α := ℝ) (β := ℝ)
      ((((f₂ : (a : G) → CircleDeg1Lift) g⁻¹ : CircleDeg1Lift) : (a : ℝ) → ℝ)
          (x + τ ((f₂ : (a : G) → CircleDeg1Lift) g)) :
        ℝ)
      (1 : ℝ)

Tactic:
rw [h, map_add_one]

Premises used: CircleDeg1Lift.map_add_one
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
G : Type u_1
inst : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ ((f₁ : (a : G) → CircleDeg1Lift) g) = τ ((f₂ : (a : G) → CircleDeg1Lift) g)
x : ℝ
g : G
this : τ ((f₂ : (a : G) → CircleDeg1Lift) g⁻¹) = -τ ((f₂ : (a : G) → CircleDeg1Lift) g)
grw grw₁ :
  x + τ ((f₂ : (a : G) → CircleDeg1Lift) g) + τ ((f₂ : (a : G) → CircleDeg1Lift) g⁻¹) + 1 + 1 ≤
    x + τ ((f₂ : (a : G) → CircleDeg1Lift) g) + τ ((f₂ : (a : G) → CircleDeg1Lift) g⁻¹) + 1 + 1
⊢ HAdd.hAdd (α := ℝ) (β := ℝ)
      ((((f₂ : (a : G) → CircleDeg1Lift) g⁻¹ : CircleDeg1Lift) : (a : ℝ) → ℝ)
          (x + τ ((f₂ : (a : G) → CircleDeg1Lift) g)) :
        ℝ)
      (1 : ℝ) ≤
    x + τ ((f₂ : (a : G) → CircleDeg1Lift) g) + τ ((f₂ : (a : G) → CircleDeg1Lift) g⁻¹) + 1 + 1

Tactic:
grw [map_lt_add_translationNumber_add_one]

Premises used: CircleDeg1Lift.map_lt_add_translationNumber_add_one
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
G : Type u_1
inst : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ ((f₁ : (a : G) → CircleDeg1Lift) g) = τ ((f₂ : (a : G) → CircleDeg1Lift) g)
x : ℝ
g : G
this : τ ((f₂ : (a : G) → CircleDeg1Lift) g⁻¹) = -τ ((f₂ : (a : G) → CircleDeg1Lift) g)
⊢ x + τ ((f₂ : (a : G) → CircleDeg1Lift) g) + τ ((f₂ : (a : G) → CircleDeg1Lift) g⁻¹) + 1 + 1 = x + 2

Tactic:
simp [this, add_assoc, one_add_one_eq_two]

Premises used: add_assoc, one_add_one_eq_two
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
G : Type u_1
inst : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ ((f₁ : (a : G) → CircleDeg1Lift) g) = τ ((f₂ : (a : G) → CircleDeg1Lift) g)
x : ℝ
g : G
this : τ ((f₂ : (a : G) → CircleDeg1Lift) g⁻¹) = -τ ((f₂ : (a : G) → CircleDeg1Lift) g)
f₃ :
  (((f₂ : (a : G) → CircleDeg1Lift) g⁻¹ : CircleDeg1Lift) : (a : ℝ) → ℝ)
      (x + τ ((f₁ : (a : G) → CircleDeg1Lift) g) + 1) =
    HAdd.hAdd (α := ℝ) (β := ℝ)
      ((((f₂ : (a : G) → CircleDeg1Lift) g⁻¹ : CircleDeg1Lift) : (a : ℝ) → ℝ)
          (x + τ ((f₂ : (a : G) → CircleDeg1Lift) g)) :
        ℝ)
      (1 : ℝ)
f₄ :
  HAdd.hAdd (α := ℝ) (β := ℝ)
      ((((f₂ : (a : G) → CircleDeg1Lift) g⁻¹ : CircleDeg1Lift) : (a : ℝ) → ℝ)
          (x + τ ((f₂ : (a : G) → CircleDeg1Lift) g)) :
        ℝ)
      (1 : ℝ) ≤
    x + τ ((f₂ : (a : G) → CircleDeg1Lift) g) + τ ((f₂ : (a : G) → CircleDeg1Lift) g⁻¹) + 1 + 1
f₅ : x + τ ((f₂ : (a : G) → CircleDeg1Lift) g) + τ ((f₂ : (a : G) → CircleDeg1Lift) g⁻¹) + 1 + 1 = x + 2
⊢ (fun (g : G) ↦
        ((((f₂ : (a : G) → CircleDeg1Lift) g⁻¹ : CircleDeg1Lift) : (a : ℝ) → ℝ)
            ((((f₁ : (a : G) → CircleDeg1Lift) g : CircleDeg1Lift) : (a : ℝ) → ℝ) x : ℝ) :
          ℝ))
      g ≤
    x + 2

Tactic:
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 := by grw [map_lt_add_translationNumber_add_one]
      _ = x + 2 := by simp [this, add_assoc, one_add_one_eq_two]

Premises used: CircleDeg1Lift.mono, CircleDeg1Lift.translationNumber, LT.lt.le, Inv.inv, HAdd.hAdd, CircleDeg1Lift.map_lt_add_translationNumber_add_one, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
G : Type u_1
inst : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ ((f₁ : (a : G) → CircleDeg1Lift) g) = τ ((f₂ : (a : G) → CircleDeg1Lift) g)
⊢ ∀ (x : ℝ),
    BddAbove (α := ℝ)
      (range fun (g : G) ↦
        (((f₂ : (a : G) → CircleDeg1Lift) g⁻¹ : CircleDeg1Lift) : (a : ℝ) → ℝ)
          ((((f₁ : (a : G) → CircleDeg1Lift) g : CircleDeg1Lift) : (a : ℝ) → ℝ) x : ℝ))

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, 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 := by grw [map_lt_add_translationNumber_add_one]
      _ = x + 2 := by simp [this, add_assoc, one_add_one_eq_two]
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
G : Type u_1
inst : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ ((f₁ : (a : G) → CircleDeg1Lift) g) = τ ((f₂ : (a : G) → CircleDeg1Lift) g)
this :
  ∀ (x : ℝ),
    BddAbove (α := ℝ)
      (range fun (g : G) ↦
        (((f₂ : (a : G) → CircleDeg1Lift) g⁻¹ : CircleDeg1Lift) : (a : ℝ) → ℝ)
          ((((f₁ : (a : G) → CircleDeg1Lift) g : CircleDeg1Lift) : (a : ℝ) → ℝ) x : ℝ))
F₁ : G →* ℝ ≃o ℝ := toOrderIso.comp f₁.toHomUnits
F₂ : G →* ℝ ≃o ℝ := toOrderIso.comp f₂.toHomUnits
⊢ ∀ (g : G),
    Eq (α := (a : ℝ) → ℝ) (⇑((F₁ : (a : G) → ℝ ≃o ℝ) g : ℝ ≃o ℝ) : (a : ℝ) → ℝ)
      (⇑((f₁ : (a : G) → CircleDeg1Lift) g : CircleDeg1Lift) : (a : ℝ) → ℝ)

Tactic:
have hF₁ : ∀ g, ⇑(F₁ g) = f₁ g := fun _ => rfl
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
G : Type u_1
inst : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ ((f₁ : (a : G) → CircleDeg1Lift) g) = τ ((f₂ : (a : G) → CircleDeg1Lift) g)
this :
  ∀ (x : ℝ),
    BddAbove (α := ℝ)
      (range fun (g : G) ↦
        (((f₂ : (a : G) → CircleDeg1Lift) g⁻¹ : CircleDeg1Lift) : (a : ℝ) → ℝ)
          ((((f₁ : (a : G) → CircleDeg1Lift) g : CircleDeg1Lift) : (a : ℝ) → ℝ) x : ℝ))
F₁ : G →* ℝ ≃o ℝ := toOrderIso.comp f₁.toHomUnits
F₂ : G →* ℝ ≃o ℝ := toOrderIso.comp f₂.toHomUnits
hF₁ :
  ∀ (g : G),
    Eq (α := (a : ℝ) → ℝ) (⇑((F₁ : (a : G) → ℝ ≃o ℝ) g : ℝ ≃o ℝ) : (a : ℝ) → ℝ)
      (⇑((f₁ : (a : G) → CircleDeg1Lift) g : CircleDeg1Lift) : (a : ℝ) → ℝ)
⊢ ∀ (g : G),
    Eq (α := (a : ℝ) → ℝ) (⇑((F₂ : (a : G) → ℝ ≃o ℝ) g : ℝ ≃o ℝ) : (a : ℝ) → ℝ)
      (⇑((f₂ : (a : G) → CircleDeg1Lift) g : CircleDeg1Lift) : (a : ℝ) → ℝ)

Tactic:
have hF₂ : ∀ g, ⇑(F₂ g) = f₂ g := fun _ => rfl
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
G : Type u_1
inst : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ ((f₁ : (a : G) → CircleDeg1Lift) g) = τ ((f₂ : (a : G) → CircleDeg1Lift) g)
this :
  ∀ (x : ℝ),
    BddAbove (α := ℝ)
      (range fun (g : G) ↦
        (((f₂ : (a : G) → CircleDeg1Lift) g⁻¹ : CircleDeg1Lift) : (a : ℝ) → ℝ)
          ((((f₁ : (a : G) → CircleDeg1Lift) g : CircleDeg1Lift) : (a : ℝ) → ℝ) x : ℝ))
F₁ : G →* ℝ ≃o ℝ := toOrderIso.comp f₁.toHomUnits
F₂ : G →* ℝ ≃o ℝ := toOrderIso.comp f₂.toHomUnits
hF₁ :
  ∀ (g : G),
    Eq (α := (a : ℝ) → ℝ) (⇑((F₁ : (a : G) → ℝ ≃o ℝ) g : ℝ ≃o ℝ) : (a : ℝ) → ℝ)
      (⇑((f₁ : (a : G) → CircleDeg1Lift) g : CircleDeg1Lift) : (a : ℝ) → ℝ)
hF₂ :
  ∀ (g : G),
    Eq (α := (a : ℝ) → ℝ) (⇑((F₂ : (a : G) → ℝ ≃o ℝ) g : ℝ ≃o ℝ) : (a : ℝ) → ℝ)
      (⇑((f₂ : (a : G) → CircleDeg1Lift) g : CircleDeg1Lift) : (a : ℝ) → ℝ)
⊢ ∃ (F : CircleDeg1Lift),
    ∀ (g : G),
      Semiconj (α := ℝ) (β := ℝ) (⇑F : (a : ℝ) → ℝ)
        (⇑((f₁ : (a : G) → CircleDeg1Lift) g : CircleDeg1Lift) : (a : ℝ) → ℝ)
        (⇑((f₂ : (a : G) → CircleDeg1Lift) g : CircleDeg1Lift) : (a : ℝ) → ℝ)

Tactic:
⟨⟨⟨fun x ↦ ⨆ g', (F₂ g')⁻¹ (F₁ g' x), fun x y hxy => ?_⟩, fun x => ?_⟩,
    csSup_div_semiconj F₂ F₁ fun x => ?_⟩

Premises used: Function.csSup_div_semiconj, iSup, Inv.inv, Exists.intro, OrderHom.mk, CircleDeg1Lift.mk, DFunLike.coe
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
G : Type u_1
inst : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ ((f₁ : (a : G) → CircleDeg1Lift) g) = τ ((f₂ : (a : G) → CircleDeg1Lift) g)
this :
  ∀ (x : ℝ),
    BddAbove (α := ℝ)
      (range fun (g : G) ↦
        (((f₂ : (a : G) → CircleDeg1Lift) g⁻¹ : CircleDeg1Lift) : (a : ℝ) → ℝ)
          ((((f₁ : (a : G) → CircleDeg1Lift) g : CircleDeg1Lift) : (a : ℝ) → ℝ) x : ℝ))
F₁ : G →* ℝ ≃o ℝ := toOrderIso.comp f₁.toHomUnits
F₂ : G →* ℝ ≃o ℝ := toOrderIso.comp f₂.toHomUnits
hF₁ :
  ∀ (g : G),
    Eq (α := (a : ℝ) → ℝ) (⇑((F₁ : (a : G) → ℝ ≃o ℝ) g : ℝ ≃o ℝ) : (a : ℝ) → ℝ)
      (⇑((f₁ : (a : G) → CircleDeg1Lift) g : CircleDeg1Lift) : (a : ℝ) → ℝ)
hF₂ :
  ∀ (g : G),
    Eq (α := (a : ℝ) → ℝ) (⇑((F₂ : (a : G) → ℝ ≃o ℝ) g : ℝ ≃o ℝ) : (a : ℝ) → ℝ)
      (⇑((f₂ : (a : G) → CircleDeg1Lift) g : CircleDeg1Lift) : (a : ℝ) → ℝ)
refine_1 :
  ∀ (x y : ℝ) (hxy : x ≤ y),
    LE.le (α := ℝ)
      ((fun (x : ℝ) ↦
          (⨆ (g' : G),
              ((((F₂ : (a : G) → ℝ ≃o ℝ) g')⁻¹ : ℝ ≃o ℝ) : (a : ℝ) → ℝ)
                ((((F₁ : (a : G) → ℝ ≃o ℝ) g' : ℝ ≃o ℝ) : (a : ℝ) → ℝ) x : ℝ) :
            ℝ))
        x)
      ((fun (x : ℝ) ↦
          (⨆ (g' : G),
              ((((F₂ : (a : G) → ℝ ≃o ℝ) g')⁻¹ : ℝ ≃o ℝ) : (a : ℝ) → ℝ)
                ((((F₁ : (a : G) → ℝ ≃o ℝ) g' : ℝ ≃o ℝ) : (a : ℝ) → ℝ) x : ℝ) :
            ℝ))
        y)
refine_2 :
  ∀ (x : ℝ),
    OrderHom.toFun
        {
          toFun := fun (x : ℝ) ↦
            ⨆ (g' : G),
              ((((F₂ : (a : G) → ℝ ≃o ℝ) g')⁻¹ : ℝ ≃o ℝ) : (a : ℝ) → ℝ)
                ((((F₁ : (a : G) → ℝ ≃o ℝ) g' : ℝ ≃o ℝ) : (a : ℝ) → ℝ) x : ℝ),
          monotone' := ⋯ }
        (x + 1) =
      HAdd.hAdd (α := ℝ)
        (OrderHom.toFun
          {
            toFun := fun (x : ℝ) ↦
              ⨆ (g' : G),
                ((((F₂ : (a : G) → ℝ ≃o ℝ) g')⁻¹ : ℝ ≃o ℝ) : (a : ℝ) → ℝ)
                  ((((F₁ : (a : G) → ℝ ≃o ℝ) g' : ℝ ≃o ℝ) : (a : ℝ) → ℝ) x : ℝ),
            monotone' := ⋯ : ℝ →o ℝ }
          x)
        1
refine_3 :
  ∀ (x : ℝ),
    BddAbove (α := ℝ)
      (range fun (g : G) ↦
        ((((F₂ : (a : G) → ℝ ≃o ℝ) g)⁻¹ : ℝ ≃o ℝ) : (a : ℝ) → ℝ)
          ((((F₁ : (a : G) → ℝ ≃o ℝ) g : ℝ ≃o ℝ) : (a : ℝ) → ℝ) x : ℝ))
⊢ ∃ (F : CircleDeg1Lift),
    ∀ (g : G),
      Semiconj (α := ℝ) (β := ℝ) (⇑F : (a : ℝ) → ℝ)
        (⇑((f₁ : (a : G) → CircleDeg1Lift) g : CircleDeg1Lift) : (a : ℝ) → ℝ)
        (⇑((f₂ : (a : G) → CircleDeg1Lift) g : CircleDeg1Lift) : (a : ℝ) → ℝ)

Tactic:
refine ⟨⟨⟨fun x ↦ ⨆ g', (F₂ g')⁻¹ (F₁ g' x), fun x y hxy => ?_⟩, fun x => ?_⟩,
    csSup_div_semiconj F₂ F₁ fun x => ?_⟩
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
G : Type u_1
inst : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ ((f₁ : (a : G) → CircleDeg1Lift) g) = τ ((f₂ : (a : G) → CircleDeg1Lift) g)
this :
  ∀ (x : ℝ),
    BddAbove (α := ℝ)
      (range fun (g : G) ↦
        (((f₂ : (a : G) → CircleDeg1Lift) g⁻¹ : CircleDeg1Lift) : (a : ℝ) → ℝ)
          ((((f₁ : (a : G) → CircleDeg1Lift) g : CircleDeg1Lift) : (a : ℝ) → ℝ) x : ℝ))
F₁ : G →* ℝ ≃o ℝ := toOrderIso.comp f₁.toHomUnits
F₂ : G →* ℝ ≃o ℝ := toOrderIso.comp f₂.toHomUnits
hF₁ :
  ∀ (g : G),
    Eq (α := (a : ℝ) → ℝ) (⇑((F₁ : (a : G) → ℝ ≃o ℝ) g : ℝ ≃o ℝ) : (a : ℝ) → ℝ)
      (⇑((f₁ : (a : G) → CircleDeg1Lift) g : CircleDeg1Lift) : (a : ℝ) → ℝ)
hF₂ :
  ∀ (g : G),
    Eq (α := (a : ℝ) → ℝ) (⇑((F₂ : (a : G) → ℝ ≃o ℝ) g : ℝ ≃o ℝ) : (a : ℝ) → ℝ)
      (⇑((f₂ : (a : G) → CircleDeg1Lift) g : CircleDeg1Lift) : (a : ℝ) → ℝ)
x y : ℝ
hxy : x ≤ y
refine_1 :
  LE.le (α := ℝ)
    (⨆ (g' : G),
      (((f₂ : (a : G) → CircleDeg1Lift) g'⁻¹ : CircleDeg1Lift) : (a : ℝ) → ℝ)
        ((((f₁ : (a : G) → CircleDeg1Lift) g' : CircleDeg1Lift) : (a : ℝ) → ℝ) x : ℝ))
    (⨆ (g' : G),
      (((f₂ : (a : G) → CircleDeg1Lift) g'⁻¹ : CircleDeg1Lift) : (a : ℝ) → ℝ)
        ((((f₁ : (a : G) → CircleDeg1Lift) g' : CircleDeg1Lift) : (a : ℝ) → ℝ) y : ℝ))
⊢ LE.le (α := ℝ)
    ((fun (x : ℝ) ↦
        (⨆ (g' : G),
            ((((F₂ : (a : G) → ℝ ≃o ℝ) g')⁻¹ : ℝ ≃o ℝ) : (a : ℝ) → ℝ)
              ((((F₁ : (a : G) → ℝ ≃o ℝ) g' : ℝ ≃o ℝ) : (a : ℝ) → ℝ) x : ℝ) :
          ℝ))
      x)
    ((fun (x : ℝ) ↦
        (⨆ (g' : G),
            ((((F₂ : (a : G) → ℝ ≃o ℝ) g')⁻¹ : ℝ ≃o ℝ) : (a : ℝ) → ℝ)
              ((((F₁ : (a : G) → ℝ ≃o ℝ) g' : ℝ ≃o ℝ) : (a : ℝ) → ℝ) x : ℝ) :
          ℝ))
      y)

Tactic:
simp only [hF₁, hF₂, ← map_inv]

Premises used: map_inv
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
G : Type u_1
inst : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ ((f₁ : (a : G) → CircleDeg1Lift) g) = τ ((f₂ : (a : G) → CircleDeg1Lift) g)
this :
  ∀ (x : ℝ),
    BddAbove (α := ℝ)
      (range fun (g : G) ↦
        (((f₂ : (a : G) → CircleDeg1Lift) g⁻¹ : CircleDeg1Lift) : (a : ℝ) → ℝ)
          ((((f₁ : (a : G) → CircleDeg1Lift) g : CircleDeg1Lift) : (a : ℝ) → ℝ) x : ℝ))
F₁ : G →* ℝ ≃o ℝ := toOrderIso.comp f₁.toHomUnits
F₂ : G →* ℝ ≃o ℝ := toOrderIso.comp f₂.toHomUnits
hF₁ :
  ∀ (g : G),
    Eq (α := (a : ℝ) → ℝ) (⇑((F₁ : (a : G) → ℝ ≃o ℝ) g : ℝ ≃o ℝ) : (a : ℝ) → ℝ)
      (⇑((f₁ : (a : G) → CircleDeg1Lift) g : CircleDeg1Lift) : (a : ℝ) → ℝ)
hF₂ :
  ∀ (g : G),
    Eq (α := (a : ℝ) → ℝ) (⇑((F₂ : (a : G) → ℝ ≃o ℝ) g : ℝ ≃o ℝ) : (a : ℝ) → ℝ)
      (⇑((f₂ : (a : G) → CircleDeg1Lift) g : CircleDeg1Lift) : (a : ℝ) → ℝ)
x : ℝ
refine_2 :
  ⨆ (g' : G),
      (((f₂ : (a : G) → CircleDeg1Lift) g'⁻¹ : CircleDeg1Lift) : (a : ℝ) → ℝ)
        ((((f₁ : (a : G) → CircleDeg1Lift) g' : CircleDeg1Lift) : (a : ℝ) → ℝ) (x + 1) : ℝ) =
    HAdd.hAdd (α := ℝ)
      (⨆ (g' : G),
        (((f₂ : (a : G) → CircleDeg1Lift) g'⁻¹ : CircleDeg1Lift) : (a : ℝ) → ℝ)
          ((((f₁ : (a : G) → CircleDeg1Lift) g' : CircleDeg1Lift) : (a : ℝ) → ℝ) x : ℝ))
      1
⊢ OrderHom.toFun
      {
        toFun := fun (x : ℝ) ↦
          ⨆ (g' : G),
            ((((F₂ : (a : G) → ℝ ≃o ℝ) g')⁻¹ : ℝ ≃o ℝ) : (a : ℝ) → ℝ)
              ((((F₁ : (a : G) → ℝ ≃o ℝ) g' : ℝ ≃o ℝ) : (a : ℝ) → ℝ) x : ℝ),
        monotone' := ⋯ }
      (x + 1) =
    HAdd.hAdd (α := ℝ)
      (OrderHom.toFun
        {
          toFun := fun (x : ℝ) ↦
            ⨆ (g' : G),
              ((((F₂ : (a : G) → ℝ ≃o ℝ) g')⁻¹ : ℝ ≃o ℝ) : (a : ℝ) → ℝ)
                ((((F₁ : (a : G) → ℝ ≃o ℝ) g' : ℝ ≃o ℝ) : (a : ℝ) → ℝ) x : ℝ),
          monotone' := ⋯ : ℝ →o ℝ }
        x)
      1

Tactic:
simp only [hF₁, hF₂, ← map_inv]

Premises used: map_inv
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
G : Type u_1
inst : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ ((f₁ : (a : G) → CircleDeg1Lift) g) = τ ((f₂ : (a : G) → CircleDeg1Lift) g)
this :
  ∀ (x : ℝ),
    BddAbove (α := ℝ)
      (range fun (g : G) ↦
        (((f₂ : (a : G) → CircleDeg1Lift) g⁻¹ : CircleDeg1Lift) : (a : ℝ) → ℝ)
          ((((f₁ : (a : G) → CircleDeg1Lift) g : CircleDeg1Lift) : (a : ℝ) → ℝ) x : ℝ))
F₁ : G →* ℝ ≃o ℝ := toOrderIso.comp f₁.toHomUnits
F₂ : G →* ℝ ≃o ℝ := toOrderIso.comp f₂.toHomUnits
hF₁ :
  ∀ (g : G),
    Eq (α := (a : ℝ) → ℝ) (⇑((F₁ : (a : G) → ℝ ≃o ℝ) g : ℝ ≃o ℝ) : (a : ℝ) → ℝ)
      (⇑((f₁ : (a : G) → CircleDeg1Lift) g : CircleDeg1Lift) : (a : ℝ) → ℝ)
hF₂ :
  ∀ (g : G),
    Eq (α := (a : ℝ) → ℝ) (⇑((F₂ : (a : G) → ℝ ≃o ℝ) g : ℝ ≃o ℝ) : (a : ℝ) → ℝ)
      (⇑((f₂ : (a : G) → CircleDeg1Lift) g : CircleDeg1Lift) : (a : ℝ) → ℝ)
x : ℝ
refine_3 :
  BddAbove (α := ℝ)
    (range fun (g : G) ↦
      (((f₂ : (a : G) → CircleDeg1Lift) g⁻¹ : CircleDeg1Lift) : (a : ℝ) → ℝ)
        ((((f₁ : (a : G) → CircleDeg1Lift) g : CircleDeg1Lift) : (a : ℝ) → ℝ) x : ℝ))
⊢ BddAbove (α := ℝ)
    (range fun (g : G) ↦
      ((((F₂ : (a : G) → ℝ ≃o ℝ) g)⁻¹ : ℝ ≃o ℝ) : (a : ℝ) → ℝ)
        ((((F₁ : (a : G) → ℝ ≃o ℝ) g : ℝ ≃o ℝ) : (a : ℝ) → ℝ) x : ℝ))

Tactic:
simp only [hF₁, hF₂, ← map_inv]

Premises used: map_inv
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
G : Type u_1
inst : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ ((f₁ : (a : G) → CircleDeg1Lift) g) = τ ((f₂ : (a : G) → CircleDeg1Lift) g)
this :
  ∀ (x : ℝ),
    BddAbove (α := ℝ)
      (range fun (g : G) ↦
        (((f₂ : (a : G) → CircleDeg1Lift) g⁻¹ : CircleDeg1Lift) : (a : ℝ) → ℝ)
          ((((f₁ : (a : G) → CircleDeg1Lift) g : CircleDeg1Lift) : (a : ℝ) → ℝ) x : ℝ))
F₁ : G →* ℝ ≃o ℝ := toOrderIso.comp f₁.toHomUnits
F₂ : G →* ℝ ≃o ℝ := toOrderIso.comp f₂.toHomUnits
hF₁ :
  ∀ (g : G),
    Eq (α := (a : ℝ) → ℝ) (⇑((F₁ : (a : G) → ℝ ≃o ℝ) g : ℝ ≃o ℝ) : (a : ℝ) → ℝ)
      (⇑((f₁ : (a : G) → CircleDeg1Lift) g : CircleDeg1Lift) : (a : ℝ) → ℝ)
hF₂ :
  ∀ (g : G),
    Eq (α := (a : ℝ) → ℝ) (⇑((F₂ : (a : G) → ℝ ≃o ℝ) g : ℝ ≃o ℝ) : (a : ℝ) → ℝ)
      (⇑((f₂ : (a : G) → CircleDeg1Lift) g : CircleDeg1Lift) : (a : ℝ) → ℝ)
x y : ℝ
hxy : x ≤ y
⊢ LE.le (α := ℝ)
    (⨆ (g' : G),
      (((f₂ : (a : G) → CircleDeg1Lift) g'⁻¹ : CircleDeg1Lift) : (a : ℝ) → ℝ)
        ((((f₁ : (a : G) → CircleDeg1Lift) g' : CircleDeg1Lift) : (a : ℝ) → ℝ) x : ℝ))
    (⨆ (g' : G),
      (((f₂ : (a : G) → CircleDeg1Lift) g'⁻¹ : CircleDeg1Lift) : (a : ℝ) → ℝ)
        ((((f₁ : (a : G) → CircleDeg1Lift) g' : CircleDeg1Lift) : (a : ℝ) → ℝ) y : ℝ))

Tactic:
ciSup_mono (this y) fun g => mono _ (mono _ hxy)

Premises used: CircleDeg1Lift.mono, Inv.inv, DFunLike.coe, ciSup_mono