awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
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₂ : (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 : ℝ)
have 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 : ℝ)
Tactic: rw [h, map_add_one]
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
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 : ℝ)
⊢ (((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 : ℝ)
have 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 : ℝ)
Tactic: rw [h, map_add_one]
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
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)
⊢ 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
have 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
Tactic: grw [map_lt_add_translationNumber_add_one]
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
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)
⊢ (fun (g : G) ↦
        ((((f₂ : (a : G) → CircleDeg1Lift) g⁻¹ : CircleDeg1Lift) : (a : ℝ) → ℝ)
            ((((f₁ : (a : G) → CircleDeg1Lift) g : CircleDeg1Lift) : (a : ℝ) → ℝ) x : ℝ) :
          ℝ))
      g ≤
    x + 2
have 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 : ℝ)
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]
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
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 : ℝ)
⊢ (fun (g : G) ↦
        ((((f₂ : (a : G) → CircleDeg1Lift) g⁻¹ : CircleDeg1Lift) : (a : ℝ) → ℝ)
            ((((f₁ : (a : G) → CircleDeg1Lift) g : CircleDeg1Lift) : (a : ℝ) → ℝ) x : ℝ) :
          ℝ))
      g ≤
    x + 2
have 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
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]
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
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
⊢ (fun (g : G) ↦
        ((((f₂ : (a : G) → CircleDeg1Lift) g⁻¹ : CircleDeg1Lift) : (a : ℝ) → ℝ)
            ((((f₁ : (a : G) → CircleDeg1Lift) g : CircleDeg1Lift) : (a : ℝ) → ℝ) x : ℝ) :
          ℝ))
      g ≤
    x + 2
have f₅ : x + τ ((f₂ : (a : G) → CircleDeg1Lift) g) + τ ((f₂ : (a : G) → CircleDeg1Lift) g⁻¹) + 1 + 1 = 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]
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (hypothesis)
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)
⊢ ∃ (F : CircleDeg1Lift),
    ∀ (g : G),
      Semiconj (α := ℝ) (β := ℝ) (⇑F : (a : ℝ) → ℝ)
        (⇑((f₁ : (a : G) → CircleDeg1Lift) g : CircleDeg1Lift) : (a : ℝ) → ℝ)
        (⇑((f₂ : (a : G) → CircleDeg1Lift) g : CircleDeg1Lift) : (a : ℝ) → ℝ)
have this : ∀ (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]
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (hypothesis)
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
⊢ ∃ (F : CircleDeg1Lift),
    ∀ (g : G),
      Semiconj (α := ℝ) (β := ℝ) (⇑F : (a : ℝ) → ℝ)
        (⇑((f₁ : (a : G) → CircleDeg1Lift) g : CircleDeg1Lift) : (a : ℝ) → ℝ)
        (⇑((f₂ : (a : G) → CircleDeg1Lift) g : CircleDeg1Lift) : (a : ℝ) → ℝ)
have hF₁ : ∀ (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
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (hypothesis)
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 : ℝ) → ℝ)
⊢ ∃ (F : CircleDeg1Lift),
    ∀ (g : G),
      Semiconj (α := ℝ) (β := ℝ) (⇑F : (a : ℝ) → ℝ)
        (⇑((f₁ : (a : G) → CircleDeg1Lift) g : CircleDeg1Lift) : (a : ℝ) → ℝ)
        (⇑((f₂ : (a : G) → CircleDeg1Lift) g : CircleDeg1Lift) : (a : ℝ) → ℝ)
have hF₂ : ∀ (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
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
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 : ℝ) → ℝ)
have 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)
Tactic: refine ⟨⟨⟨fun x ↦ ⨆ g', (F₂ g')⁻¹ (F₁ g' x), fun x y hxy => ?_⟩, fun x => ?_⟩,
    csSup_div_semiconj F₂ F₁ fun x => ?_⟩
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
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)
⊢ ∃ (F : CircleDeg1Lift),
    ∀ (g : G),
      Semiconj (α := ℝ) (β := ℝ) (⇑F : (a : ℝ) → ℝ)
        (⇑((f₁ : (a : G) → CircleDeg1Lift) g : CircleDeg1Lift) : (a : ℝ) → ℝ)
        (⇑((f₂ : (a : G) → CircleDeg1Lift) g : CircleDeg1Lift) : (a : ℝ) → ℝ)
have 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' := sorry }
      (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' := sorry : ℝ →o ℝ }
        x)
      1
Tactic: refine ⟨⟨⟨fun x ↦ ⨆ g', (F₂ g')⁻¹ (F₁ g' x), fun x y hxy => ?_⟩, fun x => ?_⟩,
    csSup_div_semiconj F₂ F₁ fun x => ?_⟩
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
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
⊢ ∃ (F : CircleDeg1Lift),
    ∀ (g : G),
      Semiconj (α := ℝ) (β := ℝ) (⇑F : (a : ℝ) → ℝ)
        (⇑((f₁ : (a : G) → CircleDeg1Lift) g : CircleDeg1Lift) : (a : ℝ) → ℝ)
        (⇑((f₂ : (a : G) → CircleDeg1Lift) g : CircleDeg1Lift) : (a : ℝ) → ℝ)
have refine_3 : ∀ (x : ℝ),
  BddAbove (α := ℝ)
    (range fun (g : G) ↦
      ((((F₂ : (a : G) → ℝ ≃o ℝ) g)⁻¹ : ℝ ≃o ℝ) : (a : ℝ) → ℝ)
        ((((F₁ : (a : G) → ℝ ≃o ℝ) g : ℝ ≃o ℝ) : (a : ℝ) → ℝ) x : ℝ))
Tactic: refine ⟨⟨⟨fun x ↦ ⨆ g', (F₂ g')⁻¹ (F₁ g' x), fun x y hxy => ?_⟩, fun x => ?_⟩,
    csSup_div_semiconj F₂ F₁ fun x => ?_⟩
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
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 (α := ℝ)
    ((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)
have 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 : ℝ))
Tactic: simp only [hF₁, hF₂, ← map_inv]
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
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 : ℝ
⊢ 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
have 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
Tactic: simp only [hF₁, hF₂, ← map_inv]
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
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 : ℝ
⊢ BddAbove (α := ℝ)
    (range fun (g : G) ↦
      ((((F₂ : (a : G) → ℝ ≃o ℝ) g)⁻¹ : ℝ ≃o ℝ) : (a : ℝ) → ℝ)
        ((((F₁ : (a : G) → ℝ ≃o ℝ) g : ℝ ≃o ℝ) : (a : ℝ) → ℝ) x : ℝ))
have refine_3 : BddAbove (α := ℝ)
  (range fun (g : G) ↦
    (((f₂ : (a : G) → CircleDeg1Lift) g⁻¹ : CircleDeg1Lift) : (a : ℝ) → ℝ)
      ((((f₁ : (a : G) → CircleDeg1Lift) g : CircleDeg1Lift) : (a : ℝ) → ℝ) x : ℝ))
Tactic: simp only [hF₁, hF₂, ← map_inv]