awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Dynamics.BirkhoffSum.NormedSpace
Goal:
𝕜 : Type u_1
X : Type u_2
E : Type u_3
inst : PseudoEMetricSpace X
inst_1 : RCLike 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
f : X → X
g : X → E
hf : LipschitzWith 1 f
hg : UniformContinuous g
ε : ℝ
hε : 0 < ε
δ : ℝ≥0∞
hδ₀ : 0 < δ
hδε :
  ∀ (x y : X),
    Membership.mem (γ := SetRel X X) {p : X × X | edist p.1 p.2 ≤ δ} (x, y) →
      Membership.mem (γ := Set (E × E)) {p : E × E | dist p.1 p.2 ≤ ε} (g x, g y)
x y : X
h : edist x y < δ
n : ℕ
inl : ∀ (hn : n = 0), (↑n : ℝ) * ε / (↑n : ℝ) ≤ ε
inr : ∀ (hn : n ≠ 0), (↑n : ℝ) * ε / (↑n : ℝ) ≤ ε
⊢ (↑n : ℝ) * ε / (↑n : ℝ) ≤ ε

Tactic:
rcases eq_or_ne n 0 with hn | hn

Premises used: eq_or_ne, OfNat.ofNat
-- Module: Mathlib.Dynamics.BirkhoffSum.NormedSpace
Goal:
𝕜 : Type u_1
X : Type u_2
E : Type u_3
inst : PseudoEMetricSpace X
inst_1 : RCLike 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
f : X → X
g : X → E
hf : LipschitzWith 1 f
hg : UniformContinuous g
ε : ℝ
hε : 0 < ε
δ : ℝ≥0∞
hδ₀ : 0 < δ
hδε :
  ∀ (x y : X),
    Membership.mem (γ := SetRel X X) {p : X × X | edist p.1 p.2 ≤ δ} (x, y) →
      Membership.mem (γ := Set (E × E)) {p : E × E | dist p.1 p.2 ≤ ε} (g x, g y)
x y : X
h : edist x y < δ
n : ℕ
hn : n = 0
⊢ (↑n : ℝ) * ε / (↑n : ℝ) ≤ ε

Tactic:
simp [hn, hε.le, mul_div_cancel_left₀]

Premises used: mul_div_cancel_left₀, LT.lt.le
-- Module: Mathlib.Dynamics.BirkhoffSum.NormedSpace
Goal:
𝕜 : Type u_1
X : Type u_2
E : Type u_3
inst : PseudoEMetricSpace X
inst_1 : RCLike 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
f : X → X
g : X → E
hf : LipschitzWith 1 f
hg : UniformContinuous g
ε : ℝ
hε : 0 < ε
δ : ℝ≥0∞
hδ₀ : 0 < δ
hδε :
  ∀ (x y : X),
    Membership.mem (γ := SetRel X X) {p : X × X | edist p.1 p.2 ≤ δ} (x, y) →
      Membership.mem (γ := Set (E × E)) {p : E × E | dist p.1 p.2 ≤ ε} (g x, g y)
x y : X
h : edist x y < δ
n : ℕ
hn : n ≠ 0
⊢ (↑n : ℝ) * ε / (↑n : ℝ) ≤ ε

Tactic:
simp [hn, hε.le, mul_div_cancel_left₀]

Premises used: mul_div_cancel_left₀, LT.lt.le
-- Module: Mathlib.Dynamics.BirkhoffSum.NormedSpace
Goal:
𝕜 : Type u_1
X : Type u_2
E : Type u_3
inst : PseudoEMetricSpace X
inst_1 : RCLike 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
f : X → X
g : X → E
hf : LipschitzWith 1 f
hg : UniformContinuous g
ε : ℝ
hε : 0 < ε
δ : ℝ≥0∞
hδ₀ : 0 < δ
hδε :
  ∀ (x y : X),
    Membership.mem (γ := SetRel X X) {p : X × X | edist p.1 p.2 ≤ δ} (x, y) →
      Membership.mem (γ := Set (E × E)) {p : E × E | Dist.dist p.1 p.2 ≤ ε} (g x, g y)
x y : X
h : edist x y < δ
n : ℕ
dist :
  HDiv.hDiv (α := ℝ) (∑ k ∈ Finset.range n, Dist.dist (g (f^[k] x)) (g (f^[k] y))) (↑n : ℝ) ≤
    HDiv.hDiv (α := ℝ) (∑ _k ∈ Finset.range n, ε) (↑n : ℝ)
dist₁ : HDiv.hDiv (α := ℝ) (∑ _k ∈ Finset.range n, ε) (↑n : ℝ) = (↑n : ℝ) * ε / (↑n : ℝ)
dist₂ : (↑n : ℝ) * ε / (↑n : ℝ) ≤ ε
⊢ Membership.mem (γ := Set (E × E)) {p : E × E | Dist.dist p.1 p.2 ≤ ε}
    (birkhoffAverage 𝕜 f g n (x, y).1, birkhoffAverage 𝕜 f g n (x, y).2)

Tactic:
calc
    dist (birkhoffAverage 𝕜 f g n x) (birkhoffAverage 𝕜 f g n y)
      ≤ (∑ k ∈ Finset.range n, dist (g (f^[k] x)) (g (f^[k] y))) / n :=
      dist_birkhoffAverage_birkhoffAverage_le ..
    _ ≤ (∑ _k ∈ Finset.range n, ε) / n := by
      gcongr
      refine hδε _ _ ?_
      simpa using (hf.iterate _).edist_le_mul_of_le h.le
    _ = n * ε / n := by simp
    _ ≤ ε := by
      rcases eq_or_ne n 0 with hn | hn <;> simp [hn, hε.le, mul_div_cancel_left₀]

Premises used: Nat.iterate, birkhoffAverage, Finset.range, Dist.dist, dist_birkhoffAverage_birkhoffAverage_le, Finset.sum
-- Module: Mathlib.Dynamics.BirkhoffSum.NormedSpace
Goal:
𝕜 : Type u_1
X : Type u_2
E : Type u_3
inst : PseudoEMetricSpace X
inst_1 : RCLike 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
f : X → X
g l : X → E
hf : LipschitzWith 1 f
hg : UniformContinuous g
hl :
  Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    l
⊢ IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace]
    {x : X | Tendsto (fun (x_1 : ℕ) ↦ birkhoffAverage 𝕜 f g x_1 x) atTop (𝓝 (l x))}

Tactic:
(uniformEquicontinuous_birkhoffAverage 𝕜 hf hg).equicontinuous.isClosed_setOf_tendsto hl

Premises used: Equicontinuous.isClosed_setOf_tendsto, UniformEquicontinuous.equicontinuous, uniformEquicontinuous_birkhoffAverage
-- Module: Mathlib.Dynamics.BirkhoffSum.QuasiMeasurePreserving
Goal:
α : Type u_1
M : Type u_2
inst : MeasurableSpace α
inst_1 : AddCommMonoid M
f : α → α
μ : Measure α
φ ψ : α → M
hf : QuasiMeasurePreserving f μ μ
hφ : φ =ᵐ[μ] ψ
n : ℕ
apply : ∀ᵐ (x : α) ∂μ, ∀ x_1 ∈ Finset.range n, φ (f^[x_1] x) = ψ (f^[x_1] x)
⊢ birkhoffSum f φ n =ᵐ[μ] birkhoffSum f ψ n

Tactic:
apply Eventually.mono _ (fun _ => Finset.sum_congr rfl)

Premises used: Filter.Eventually.mono, Finset.sum_congr, rfl
-- Module: Mathlib.Dynamics.BirkhoffSum.QuasiMeasurePreserving
Goal:
α : Type u_1
M : Type u_2
inst : MeasurableSpace α
inst_1 : AddCommMonoid M
f : α → α
μ : Measure α
φ ψ : α → M
hf : QuasiMeasurePreserving f μ μ
hφ : φ =ᵐ[μ] ψ
n : ℕ
apply : ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, i ∈ Finset.range n → φ (f^[i] a) = ψ (f^[i] a)
⊢ ∀ᵐ (x : α) ∂μ, ∀ x_1 ∈ Finset.range n, φ (f^[x_1] x) = ψ (f^[x_1] x)

Tactic:
apply ae_all_iff.mpr (fun i => ?_)

Premises used: Iff.mpr, MeasureTheory.ae_all_iff
-- Module: Mathlib.Dynamics.BirkhoffSum.QuasiMeasurePreserving
Goal:
α : Type u_1
M : Type u_2
inst : MeasurableSpace α
inst_1 : AddCommMonoid M
f : α → α
μ : Measure α
φ ψ : α → M
hf : QuasiMeasurePreserving f μ μ
hφ : φ =ᵐ[μ] ψ
n i : ℕ
⊢ ∀ᵐ (a : α) ∂μ, i ∈ Finset.range n → φ (f^[i] a) = ψ (f^[i] a)

Tactic:
(hf.iterate i).ae (hφ.mono (fun _ h _ => h))

Premises used: MeasureTheory.Measure.QuasiMeasurePreserving.ae, MeasureTheory.Measure.QuasiMeasurePreserving.iterate, Filter.Eventually.mono
-- Module: Mathlib.Dynamics.BirkhoffSum.QuasiMeasurePreserving
Goal:
α : Type u_1
M : Type u_2
inst : MeasurableSpace α
inst_1 : AddCommMonoid M
f : α → α
μ : Measure α
φ ψ : α → M
hf : QuasiMeasurePreserving f μ μ
hφ : φ =ᵐ[μ] ψ
n i : ℕ
⊢ ∀ᵐ (a : α) ∂μ, i ∈ Finset.range n → φ (f^[i] a) = ψ (f^[i] a)

Tactic:
exact (hf.iterate i).ae (hφ.mono (fun _ h _ => h))

Premises used: MeasureTheory.Measure.QuasiMeasurePreserving.ae, MeasureTheory.Measure.QuasiMeasurePreserving.iterate, Filter.Eventually.mono
-- Module: Mathlib.Dynamics.BirkhoffSum.QuasiMeasurePreserving
Goal:
α : Type u_1
M : Type u_2
inst : MeasurableSpace α
inst_1 : AddCommMonoid M
f : α → α
μ : Measure α
φ ψ : α → M
R : Type u_3
inst_2 : DivisionSemiring R
inst_3 : Module R M
hf : QuasiMeasurePreserving f μ μ
hφ : φ =ᵐ[μ] ψ
n : ℕ
⊢ birkhoffAverage R f φ n =ᵐ[μ] birkhoffAverage R f ψ n

Tactic:
EventuallyEq.const_smul (birkhoffSum_ae_eq_of_ae_eq hf hφ n) (n : R)⁻¹

Premises used: MeasureTheory.Measure.QuasiMeasurePreserving.birkhoffSum_ae_eq_of_ae_eq, Nat.cast, birkhoffAverage, Inv.inv, Filter.EventuallyEq.const_smul
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : ℝ →o ℝ
h : ∀ (x : ℝ), f.toFun (x + 1) = f.toFun x + 1
⊢ Eq (α := (a : ℝ) → ℝ) (⇑{ toOrderHom := f, map_add_one' := h : CircleDeg1Lift } : (a : ℝ) → ℝ) (⇑f : (a : ℝ) → ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
⊢ Eq (α := (a : ℝ) → ℝ) (⇑f.toOrderHom : (a : ℝ) → ℝ) (⇑f : (a : ℝ) → ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
⊢ Monotone (α := ℝ) (β := ℝ) (⇑f : (a : ℝ) → ℝ)

Tactic:
f.monotone'

Premises used: CircleDeg1Lift.toOrderHom, OrderHom.monotone'
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
x y : ℝ
h : x ≤ y
⊢ LE.le (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) ((f : (a : ℝ) → ℝ) y : ℝ)

Tactic:
f.monotone h

Premises used: CircleDeg1Lift.monotone
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
⊢ StrictMono (α := ℝ) (β := ℝ) (⇑f : (a : ℝ) → ℝ) ↔ Injective (α := ℝ) (β := ℝ) (⇑f : (a : ℝ) → ℝ)

Tactic:
f.monotone.strictMono_iff_injective

Premises used: Monotone.strictMono_iff_injective, CircleDeg1Lift.monotone
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
⊢ ∀ (x : ℝ), (f : (a : ℝ) → ℝ) (x + 1) = HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) (1 : ℝ)

Tactic:
f.map_add_one'

Premises used: CircleDeg1Lift.map_add_one'
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
x : ℝ
rw : (f : (a : ℝ) → ℝ) (x + 1) = HAdd.hAdd (α := ℝ) (β := ℝ) (1 : ℝ) ((f : (a : ℝ) → ℝ) x : ℝ)
rw₁ :
  HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) (1 : ℝ) =
    HAdd.hAdd (α := ℝ) (β := ℝ) (1 : ℝ) ((f : (a : ℝ) → ℝ) x : ℝ)
rw₂ rw₃ :
  HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) (1 : ℝ) =
    HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) (1 : ℝ)
⊢ (f : (a : ℝ) → ℝ) (1 + x) = HAdd.hAdd (α := ℝ) (β := ℝ) (1 : ℝ) ((f : (a : ℝ) → ℝ) x : ℝ)

Tactic:
rw [add_comm, map_add_one, add_comm 1]

Premises used: add_comm, OfNat.ofNat, CircleDeg1Lift.map_add_one
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f g : CircleDeg1Lift
h : ∀ (x : ℝ), Eq (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) ((g : (a : ℝ) → ℝ) x : ℝ)
⊢ f = g

Tactic:
DFunLike.ext f g h

Premises used: DFunLike.ext
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f_1 g_1 f g : CircleDeg1Lift
x : ℝ
⊢ (f.comp g.toOrderHom).toFun (x + 1) = (f.comp g.toOrderHom).toFun x + 1

Tactic:
simp [map_add_one]

Premises used: CircleDeg1Lift.map_add_one
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f g : CircleDeg1Lift
⊢ Eq (α := (a : ℝ) → ℝ) (⇑(f * g) : (a : ℝ) → ℝ) (comp (β := ℝ) (⇑f : (a : ℝ) → ℝ) (⇑g : (a : ℝ) → ℝ))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f g : CircleDeg1Lift
x : ℝ
⊢ Eq (α := ℝ) ((f * g : (a : ℝ) → ℝ) x : ℝ) ((f : (a : ℝ) → ℝ) ((g : (a : ℝ) → ℝ) x : ℝ) : ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
⊢ Eq (α := (a : ℝ) → ℝ) (⇑1 : (a : ℝ) → ℝ) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Liftˣ
x : ℝ
⊢ ((↑f⁻¹ : CircleDeg1Lift) : (a : ℝ) → ℝ) (((↑f : CircleDeg1Lift) : (a : ℝ) → ℝ) x : ℝ) = x

Tactic:
simp only [← mul_apply, f.inv_mul, coe_one, id]

Premises used: Units.inv_mul, CircleDeg1Lift.mul_apply, id, CircleDeg1Lift.coe_one
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Liftˣ
x : ℝ
⊢ ((↑f : CircleDeg1Lift) : (a : ℝ) → ℝ) (((↑f⁻¹ : CircleDeg1Lift) : (a : ℝ) → ℝ) x : ℝ) = x

Tactic:
simp only [← mul_apply, f.mul_inv, coe_one, id]

Premises used: CircleDeg1Lift.mul_apply, id, Units.mul_inv, CircleDeg1Lift.coe_one
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f_1 g : CircleDeg1Lift
f : CircleDeg1Liftˣ
a b : ℝ
h :
  LE.le (α := ℝ)
    (({ toFun := (⇑(↑f : CircleDeg1Lift) : (a : ℝ) → ℝ), invFun := (⇑(↑f⁻¹ : CircleDeg1Lift) : (a : ℝ) → ℝ),
            left_inv := ⋯, right_inv := ⋯ : ℝ ≃ ℝ } :
          (a : ℝ) → ℝ)
        a :
      ℝ)
    (({ toFun := (⇑(↑f : CircleDeg1Lift) : (a : ℝ) → ℝ), invFun := (⇑(↑f⁻¹ : CircleDeg1Lift) : (a : ℝ) → ℝ),
            left_inv := ⋯, right_inv := ⋯ : ℝ ≃ ℝ } :
          (a : ℝ) → ℝ)
        b :
      ℝ)
⊢ a ≤ b

Tactic:
simpa using mono (↑f⁻¹) h

Premises used: CircleDeg1Lift.mono, Units.val, Inv.inv
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Liftˣ
⊢ Eq (α := (a : ℝ) → ℝ) (⇑((toOrderIso : (a : CircleDeg1Liftˣ) → ℝ ≃o ℝ) f : ℝ ≃o ℝ) : (a : ℝ) → ℝ)
    (⇑(↑f : CircleDeg1Lift) : (a : ℝ) → ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Liftˣ
⊢ Eq (α := (a : ℝ) → ℝ) (⇑(OrderIso.symm ((toOrderIso : (a : CircleDeg1Liftˣ) → ℝ ≃o ℝ) f)) : (a : ℝ) → ℝ)
    (⇑(↑f⁻¹ : CircleDeg1Lift) : (a : ℝ) → ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Liftˣ
⊢ Eq (α := (a : ℝ) → ℝ) (⇑(((toOrderIso : (a : CircleDeg1Liftˣ) → ℝ ≃o ℝ) f)⁻¹ : ℝ ≃o ℝ) : (a : ℝ) → ℝ)
    (⇑(↑f⁻¹ : CircleDeg1Lift) : (a : ℝ) → ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
h : Bijective (α := ℝ) (β := ℝ) (⇑f : (a : ℝ) → ℝ)
x y : ℝ
hxy : x ≤ y
⊢ LE.le (α := ℝ) ((f : (a : ℝ) → ℝ) (((Equiv.ofBijective (⇑f : (a : ℝ) → ℝ) h).symm : (a : ℝ) → ℝ) x : ℝ) : ℝ)
    ((f : (a : ℝ) → ℝ) (((Equiv.ofBijective (⇑f : (a : ℝ) → ℝ) h).symm : (a : ℝ) → ℝ) y : ℝ) : ℝ)

Tactic:
simp only [Equiv.ofBijective_apply_symm_apply f h, hxy]

Premises used: Equiv.ofBijective_apply_symm_apply, DFunLike.coe
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
h : Bijective (α := ℝ) (β := ℝ) (⇑f : (a : ℝ) → ℝ)
x : ℝ
⊢ Eq (α := ℝ) ((f : (a : ℝ) → ℝ) (((Equiv.ofBijective (⇑f : (a : ℝ) → ℝ) h).symm : (a : ℝ) → ℝ) (x + 1) : ℝ) : ℝ)
    ((f : (a : ℝ) → ℝ)
        (HAdd.hAdd (α := ℝ) (β := ℝ) (((Equiv.ofBijective (⇑f : (a : ℝ) → ℝ) h).symm : (a : ℝ) → ℝ) x : ℝ) (1 : ℝ)) :
      ℝ)

Tactic:
simp only [Equiv.ofBijective_apply_symm_apply f, f.map_add_one]

Premises used: Equiv.ofBijective_apply_symm_apply, DFunLike.coe, CircleDeg1Lift.map_add_one
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
n : ℕ
⊢ Eq (α := (a : ℝ) → ℝ) (⇑(f ^ (n + 1)) : (a : ℝ) → ℝ) (⇑f : (a : ℝ) → ℝ)^[n + 1]

Tactic:
simp [coe_pow n, pow_succ]

Premises used: pow_succ
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f g₁ g₂ : CircleDeg1Lift
⊢ SemiconjBy f g₁ g₂ ↔ Semiconj (α := ℝ) (β := ℝ) (⇑f : (a : ℝ) → ℝ) (⇑g₁ : (a : ℝ) → ℝ) (⇑g₂ : (a : ℝ) → ℝ)

Tactic:
CircleDeg1Lift.ext_iff

Premises used: CircleDeg1Lift.ext_iff, SemiconjBy, Function.Semiconj
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f g : CircleDeg1Lift
⊢ Commute f g ↔ Function.Commute (α := ℝ) (⇑f : (a : ℝ) → ℝ) (⇑g : (a : ℝ) → ℝ)

Tactic:
CircleDeg1Lift.ext_iff

Premises used: CircleDeg1Lift.ext_iff, Function.Commute, SemiconjBy, Commute, Function.Semiconj
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
x y : ℝ
⊢ ((↑((translate : (a : Multiplicative ℝ) → CircleDeg1Liftˣ) ((Multiplicative.ofAdd : (a : ℝ) → Multiplicative ℝ) x)) :
          CircleDeg1Lift) :
        (a : ℝ) → ℝ)
      y =
    x + y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
x y : ℝ
⊢ ((↑((translate : (a : Multiplicative ℝ) → CircleDeg1Liftˣ)
                ((Multiplicative.ofAdd : (a : ℝ) → Multiplicative ℝ) x))⁻¹ :
          CircleDeg1Lift) :
        (a : ℝ) → ℝ)
      y =
    -x + y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
x : ℝ
n : ℤ
⊢ HPow.hPow (α := CircleDeg1Liftˣ)
      ((translate : (a : Multiplicative ℝ) → CircleDeg1Liftˣ) ((Multiplicative.ofAdd : (a : ℝ) → Multiplicative ℝ) x) :
        CircleDeg1Liftˣ)
      n =
    (translate : (a : Multiplicative ℝ) → CircleDeg1Liftˣ)
      ((Multiplicative.ofAdd : (a : ℝ) → Multiplicative ℝ) ((↑n : ℝ) * x))

Tactic:
simp only [← zsmul_eq_mul, ofAdd_zsmul, map_zpow]

Premises used: zsmul_eq_mul, map_zpow, ofAdd_zsmul
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
x : ℝ
n : ℕ
⊢ HPow.hPow (α := CircleDeg1Liftˣ)
      ((translate : (a : Multiplicative ℝ) → CircleDeg1Liftˣ) ((Multiplicative.ofAdd : (a : ℝ) → Multiplicative ℝ) x) :
        CircleDeg1Liftˣ)
      n =
    (translate : (a : Multiplicative ℝ) → CircleDeg1Liftˣ)
      ((Multiplicative.ofAdd : (a : ℝ) → Multiplicative ℝ) ((↑n : ℝ) * x))

Tactic:
translate_zpow x n

Premises used: Nat.cast, CircleDeg1Lift.translate_zpow
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
x : ℝ
n : ℕ
rw :
  Eq (α := ℝ → ℝ)
    (⇑(HPow.hPow (α := CircleDeg1Lift)
          (↑((translate : (a : Multiplicative ℝ) → CircleDeg1Liftˣ)
                ((Multiplicative.ofAdd : (a : ℝ) → Multiplicative ℝ) x)) :
            CircleDeg1Lift)
          n) :
      (a : ℝ) → ℝ)
    (⇑(↑((translate : (a : Multiplicative ℝ) → CircleDeg1Liftˣ)
              ((Multiplicative.ofAdd : (a : ℝ) → Multiplicative ℝ) ((↑n : ℝ) * x))) :
          CircleDeg1Lift) :
      (a : ℝ) → ℝ)
rw₁ :
  Eq (α := ℝ → ℝ)
    (⇑(↑(HPow.hPow (α := CircleDeg1Liftˣ)
              ((translate : (a : Multiplicative ℝ) → CircleDeg1Liftˣ)
                  ((Multiplicative.ofAdd : (a : ℝ) → Multiplicative ℝ) x) :
                CircleDeg1Liftˣ)
              n) :
          CircleDeg1Lift) :
      (a : ℝ) → ℝ)
    (⇑(↑((translate : (a : Multiplicative ℝ) → CircleDeg1Liftˣ)
              ((Multiplicative.ofAdd : (a : ℝ) → Multiplicative ℝ) ((↑n : ℝ) * x))) :
          CircleDeg1Lift) :
      (a : ℝ) → ℝ)
rw₂ rw₃ :
  Eq (α := ℝ → ℝ)
    (⇑(↑((translate : (a : Multiplicative ℝ) → CircleDeg1Liftˣ)
              ((Multiplicative.ofAdd : (a : ℝ) → Multiplicative ℝ) ((↑n : ℝ) * x))) :
          CircleDeg1Lift) :
      (a : ℝ) → ℝ)
    (⇑(↑((translate : (a : Multiplicative ℝ) → CircleDeg1Liftˣ)
              ((Multiplicative.ofAdd : (a : ℝ) → Multiplicative ℝ) ((↑n : ℝ) * x))) :
          CircleDeg1Lift) :
      (a : ℝ) → ℝ)
⊢ Eq (α := ℝ → ℝ)
    (⇑(↑((translate : (a : Multiplicative ℝ) → CircleDeg1Liftˣ)
                ((Multiplicative.ofAdd : (a : ℝ) → Multiplicative ℝ) x)) :
            CircleDeg1Lift) :
        (a : ℝ) → ℝ)^[n]
    (⇑(↑((translate : (a : Multiplicative ℝ) → CircleDeg1Liftˣ)
              ((Multiplicative.ofAdd : (a : ℝ) → Multiplicative ℝ) ((↑n : ℝ) * x))) :
          CircleDeg1Lift) :
      (a : ℝ) → ℝ)

Tactic:
rw [← coe_pow, ← Units.val_pow_eq_pow_val, translate_pow]

Premises used: CircleDeg1Lift.coe_pow, Units.val_pow_eq_pow_val, CircleDeg1Lift.translate_pow
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
n : ℕ
⊢ Function.Commute (⇑f : (a : ℝ) → ℝ) fun (x : ℝ) ↦ (↑n : ℝ) + x

Tactic:
simpa only [nsmul_one, add_left_iterate] using Function.Commute.iterate_right f.map_one_add n

Premises used: CircleDeg1Lift.map_one_add, add_left_iterate, Function.Commute.iterate_right, nsmul_one
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
n : ℕ
⊢ Function.Commute (⇑f : (a : ℝ) → ℝ) fun (x : ℝ) ↦ x + (↑n : ℝ)

Tactic:
simp only [add_comm _ (n : ℝ), f.commute_nat_add n]

Premises used: CircleDeg1Lift.commute_nat_add, Nat.cast, add_comm
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
n : ℕ
⊢ Function.Commute (⇑f : (a : ℝ) → ℝ) fun (x : ℝ) ↦ x - (↑n : ℝ)

Tactic:
simpa only [sub_eq_add_neg] using
    (f.commute_add_nat n).inverses_right (Equiv.addRight _).right_inv (Equiv.addRight _).left_inv

Premises used: Equiv.addRight, Equiv.right_inv, sub_eq_add_neg, Function.Semiconj.inverses_right, CircleDeg1Lift.commute_add_nat, Equiv.left_inv
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
n : ℕ
⊢ Function.Commute (⇑f : (a : ℝ) → ℝ) fun (x : ℝ) ↦ x + (↑-[n+1] : ℝ)

Tactic:
simpa [sub_eq_add_neg] using f.commute_sub_nat (n + 1)

Premises used: sub_eq_add_neg, HAdd.hAdd, OfNat.ofNat, CircleDeg1Lift.commute_sub_nat
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
n : ℤ
⊢ Function.Commute (⇑f : (a : ℝ) → ℝ) fun (x : ℝ) ↦ (↑n : ℝ) + x

Tactic:
simpa only [add_comm _ (n : ℝ)] using f.commute_add_int n

Premises used: Int.cast, CircleDeg1Lift.commute_add_int, add_comm
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
n : ℤ
⊢ Function.Commute (⇑f : (a : ℝ) → ℝ) fun (x : ℝ) ↦ x - (↑n : ℝ)

Tactic:
simpa only [sub_eq_add_neg] using
    (f.commute_add_int n).inverses_right (Equiv.addRight _).right_inv (Equiv.addRight _).left_inv

Premises used: Equiv.addRight, Equiv.right_inv, sub_eq_add_neg, Function.Semiconj.inverses_right, CircleDeg1Lift.commute_add_int, Equiv.left_inv
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
m : ℤ
x : ℝ
⊢ (f : (a : ℝ) → ℝ) ((↑m : ℝ) + x) = HAdd.hAdd (α := ℝ) (β := ℝ) ((↑m : ℝ) : ℝ) ((f : (a : ℝ) → ℝ) x : ℝ)

Tactic:
f.commute_int_add m x

Premises used: CircleDeg1Lift.commute_int_add
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
x : ℝ
m : ℤ
⊢ (f : (a : ℝ) → ℝ) (x + (↑m : ℝ)) = HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) ((↑m : ℝ) : ℝ)

Tactic:
f.commute_add_int m x

Premises used: CircleDeg1Lift.commute_add_int
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
x : ℝ
n : ℤ
⊢ (f : (a : ℝ) → ℝ) (x - (↑n : ℝ)) = HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) ((↑n : ℝ) : ℝ)

Tactic:
f.commute_sub_int n x

Premises used: CircleDeg1Lift.commute_sub_int
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
x : ℝ
n : ℕ
⊢ (f : (a : ℝ) → ℝ) (x + (↑n : ℝ)) = HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) ((↑n : ℝ) : ℝ)

Tactic:
f.map_add_int x n

Premises used: Nat.cast, CircleDeg1Lift.map_add_int
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
n : ℕ
x : ℝ
⊢ (f : (a : ℝ) → ℝ) ((↑n : ℝ) + x) = HAdd.hAdd (α := ℝ) (β := ℝ) ((↑n : ℝ) : ℝ) ((f : (a : ℝ) → ℝ) x : ℝ)

Tactic:
f.map_int_add n x

Premises used: Nat.cast, CircleDeg1Lift.map_int_add
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
x : ℝ
n : ℕ
⊢ (f : (a : ℝ) → ℝ) (x - (↑n : ℝ)) = HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) ((↑n : ℝ) : ℝ)

Tactic:
f.map_sub_int x n

Premises used: CircleDeg1Lift.map_sub_int, Nat.cast
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
n : ℤ
rw : Eq (α := ℝ) ((f : (a : ℝ) → ℝ) (↑n : ℝ) : ℝ) ((f : (a : ℝ) → ℝ) (HAdd.hAdd (α := ℝ) 0 (↑n : ℝ)) : ℝ)
rw₁ rw₂ : Eq (α := ℝ) ((f : (a : ℝ) → ℝ) (↑n : ℝ) : ℝ) ((f : (a : ℝ) → ℝ) (↑n : ℝ) : ℝ)
⊢ (f : (a : ℝ) → ℝ) (↑n : ℝ) = HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) ((↑n : ℝ) : ℝ)

Tactic:
rw [← f.map_add_int, zero_add]

Premises used: zero_add, CircleDeg1Lift.map_add_int
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
x : ℝ
rw :
  HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) (x - (↑⌊x⌋ : ℝ)) : ℝ) (x - (↑⌊x⌋ : ℝ)) =
    HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x
rw₁ :
  HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) ((↑⌊x⌋ : ℝ) : ℝ) - (x - (↑⌊x⌋ : ℝ)) =
    HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x
rw₂ rw₃ : HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x = HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x
⊢ HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) (fract x) : ℝ) (fract x) = HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x

Tactic:
rw [Int.fract, f.map_sub_int, sub_sub_sub_cancel_right]

Premises used: sub_sub_sub_cancel_right, CircleDeg1Lift.map_sub_int, Int.fract
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f_1 g_1 f g : CircleDeg1Lift
x : ℝ
⊢ max ((f : (a : ℝ) → ℝ) (x + 1)) ((g : (a : ℝ) → ℝ) (x + 1)) =
    HAdd.hAdd (α := ℝ) (β := ℝ) (max ((f : (a : ℝ) → ℝ) x) ((g : (a : ℝ) → ℝ) x) : ℝ) (1 : ℝ)

Tactic:
simp [max_add_add_right]

Premises used: max_add_add_right
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f_1 g_1 f g : CircleDeg1Lift
x : ℝ
⊢ min ((f : (a : ℝ) → ℝ) (x + 1)) ((g : (a : ℝ) → ℝ) (x + 1)) =
    HAdd.hAdd (α := ℝ) (β := ℝ) (min ((f : (a : ℝ) → ℝ) x) ((g : (a : ℝ) → ℝ) x) : ℝ) (1 : ℝ)

Tactic:
simp [min_add_add_right]

Premises used: min_add_add_right
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f g : CircleDeg1Lift
x : ℝ
⊢ Eq (α := ℝ) ((f ⊔ g : (a : ℝ) → ℝ) x : ℝ) (max ((f : (a : ℝ) → ℝ) x) ((g : (a : ℝ) → ℝ) x) : ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f g : CircleDeg1Lift
x : ℝ
⊢ Eq (α := ℝ) ((f ⊓ g : (a : ℝ) → ℝ) x : ℝ) (min ((f : (a : ℝ) → ℝ) x) ((g : (a : ℝ) → ℝ) x) : ℝ)

Tactic:
rfl

Premises used: rfl