awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
x : ℝ
m : ℤ
h : (f : (a : ℝ) → ℝ) x = x + (↑m : ℝ)
⊢ τ f = (↑m : ℝ)

Tactic:
le_antisymm (translationNumber_le_of_le_add_int f <| le_of_eq h)
    (le_translationNumber_of_add_int_le f <| le_of_eq h.symm)

Premises used: CircleDeg1Lift.le_translationNumber_of_add_int_le, CircleDeg1Lift.translationNumber_le_of_le_add_int, le_antisymm, le_of_eq, Eq.symm
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
x : ℝ
⊢ (↑⌊HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x⌋ : ℝ) ≤ τ f

Tactic:
le_translationNumber_of_add_int_le f <| le_sub_iff_add_le'.1 (floor_le <| f x - x)

Premises used: CircleDeg1Lift.le_translationNumber_of_add_int_le, HSub.hSub, le_sub_iff_add_le', Iff.mp, Int.floor_le, DFunLike.coe
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
x : ℝ
⊢ τ f ≤ (↑⌈HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x⌉ : ℝ)

Tactic:
translationNumber_le_of_le_add_int f <| sub_le_iff_le_add'.1 (le_ceil <| f x - x)

Premises used: Int.le_ceil, HSub.hSub, CircleDeg1Lift.translationNumber_le_of_le_add_int, sub_le_iff_le_add', Iff.mp, DFunLike.coe
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
n : ℤ
h : τ f < (↑n : ℝ)
x : ℝ
⊢ (f : (a : ℝ) → ℝ) x < x + (↑n : ℝ)

Tactic:
not_le.1 <| mt f.le_translationNumber_of_add_int_le <| not_le.2 h

Premises used: not_le, Iff.mpr, CircleDeg1Lift.le_translationNumber_of_add_int_le, mt, Iff.mp
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
n : ℕ
h : τ f < (↑n : ℝ)
x : ℝ
⊢ (f : (a : ℝ) → ℝ) x < x + (↑n : ℝ)

Tactic:
@map_lt_of_translationNumber_lt_int f n h x

Premises used: CircleDeg1Lift.map_lt_of_translationNumber_lt_int
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
x : ℝ
rw : (f : (a : ℝ) → ℝ) x < x + HAdd.hAdd (α := ℝ) (↑⌊τ f⌋ : ℝ) 1
⊢ (f : (a : ℝ) → ℝ) x < x + (↑⌊τ f⌋ : ℝ) + 1

Tactic:
rw [add_assoc]

Premises used: add_assoc
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
x : ℝ
norm_cast : (f : (a : ℝ) → ℝ) x < x + (↑(⌊τ f⌋ + 1) : ℝ)
⊢ (f : (a : ℝ) → ℝ) x < x + HAdd.hAdd (α := ℝ) (↑⌊τ f⌋ : ℝ) 1

Tactic:
norm_cast
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
x : ℝ
⊢ (f : (a : ℝ) → ℝ) x < x + (↑(⌊τ f⌋ + 1) : ℝ)

Tactic:
map_lt_of_translationNumber_lt_int _ ?_ _

Premises used: CircleDeg1Lift.map_lt_of_translationNumber_lt_int
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
x : ℝ
refine : τ f < (↑(⌊τ f⌋ + 1) : ℝ)
⊢ (f : (a : ℝ) → ℝ) x < x + (↑(⌊τ f⌋ + 1) : ℝ)

Tactic:
refine map_lt_of_translationNumber_lt_int _ ?_ _

Premises used: CircleDeg1Lift.map_lt_of_translationNumber_lt_int
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
x : ℝ
push_cast : τ f < HAdd.hAdd (α := ℝ) (↑⌊τ f⌋ : ℝ) 1
⊢ τ f < (↑(⌊τ f⌋ + 1) : ℝ)

Tactic:
push_cast
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
x : ℝ
⊢ τ f < HAdd.hAdd (α := ℝ) (↑⌊τ f⌋ : ℝ) 1

Tactic:
lt_floor_add_one _

Premises used: Int.lt_floor_add_one
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
x : ℝ
⊢ τ f < HAdd.hAdd (α := ℝ) (↑⌊τ f⌋ : ℝ) 1

Tactic:
exact lt_floor_add_one _

Premises used: Int.lt_floor_add_one
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
x : ℝ
bc : (↑⌊τ f⌋ : ℝ) ≤ τ f
⊢ x + (↑⌊τ f⌋ : ℝ) + 1 ≤ x + τ f + 1

Tactic:
gcongr
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
x : ℝ
⊢ (↑⌊τ f⌋ : ℝ) ≤ τ f

Tactic:
apply floor_le

Premises used: Int.floor_le
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
n : ℤ
h : (↑n : ℝ) < τ f
x : ℝ
⊢ x + (↑n : ℝ) < (f : (a : ℝ) → ℝ) x

Tactic:
not_le.1 <| mt f.translationNumber_le_of_le_add_int <| not_le.2 h

Premises used: not_le, Iff.mpr, mt, CircleDeg1Lift.translationNumber_le_of_le_add_int, Iff.mp
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
n : ℕ
h : (↑n : ℝ) < τ f
x : ℝ
⊢ x + (↑n : ℝ) < (f : (a : ℝ) → ℝ) x

Tactic:
@lt_map_of_int_lt_translationNumber f n h x

Premises used: CircleDeg1Lift.lt_map_of_int_lt_translationNumber
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
x : ℝ
n : ℕ
m : ℤ
h : (f ^ n : (a : ℝ) → ℝ) x = x + (↑m : ℝ)
hn : 0 < n
⊢ τ (f ^ n) = (↑m : ℝ)

Tactic:
have := (f ^ n).translationNumber_of_eq_add_int h
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
x : ℝ
n : ℕ
m : ℤ
h : (f ^ n : (a : ℝ) → ℝ) x = x + (↑m : ℝ)
hn : 0 < n
this : τ (f ^ n) = (↑m : ℝ)
rwa : ∀ (this : τ f * (↑n : ℝ) = (↑m : ℝ)), Ne (α := ℝ) (↑n : ℝ) 0
⊢ τ f = HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)

Tactic:
rwa [translationNumber_pow, mul_comm, ← eq_div_iff] at this

Premises used: mul_comm, CircleDeg1Lift.translationNumber_pow, eq_div_iff
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
x : ℝ
n : ℕ
m : ℤ
h : (f ^ n : (a : ℝ) → ℝ) x = x + (↑m : ℝ)
hn : 0 < n
this : τ f * (↑n : ℝ) = (↑m : ℝ)
⊢ Ne (α := ℝ) (↑n : ℝ) 0

Tactic:
Nat.cast_ne_zero.2 (ne_of_gt hn)

Premises used: Iff.mpr, ne_of_gt, Nat.cast_ne_zero
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
x : ℝ
n : ℕ
m : ℤ
h : (f ^ n : (a : ℝ) → ℝ) x = x + (↑m : ℝ)
hn : 0 < n
this : τ f * (↑n : ℝ) = (↑m : ℝ)
⊢ Ne (α := ℝ) (↑n : ℝ) 0

Tactic:
exact Nat.cast_ne_zero.2 (ne_of_gt hn)

Premises used: Iff.mpr, ne_of_gt, Nat.cast_ne_zero
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
P : ℝ → Prop
h : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Icc 0 1) x → P (HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x)
x : ℝ
⊢ P (HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x)

Tactic:
f.map_fract_sub_fract_eq x ▸ h _ ⟨fract_nonneg _, le_of_lt (fract_lt_one _)⟩

Premises used: le_of_lt, Eq.rec, And.intro, Int.fract_lt_one, CircleDeg1Lift.map_fract_sub_fract_eq, Int.fract_nonneg
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
hf : Continuous (X := ℝ) (Y := ℝ) (⇑f : (a : ℝ) → ℝ)
z : ℝ
hz : ∀ (x : ℝ), (f : (a : ℝ) → ℝ) x < x + z
⊢ ∃ (x : ℝ),
    Membership.mem (γ := Set ℝ) (Icc 0 1) x ∧
      ∀ (y : ℝ),
        Membership.mem (γ := Set ℝ) (Icc 0 1) y →
          HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) y : ℝ) y ≤ HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x

Tactic:
isCompact_Icc.exists_isMaxOn (nonempty_Icc.2 zero_le_one)
      (hf.sub continuous_id).continuousOn

Premises used: Iff.mpr, Continuous.continuousOn, Set.Mem, IsMaxOn, Filter.Eventually, setOf, Set.nonempty_Icc, CompactIccSpace.isCompact_Icc, Set.Subset, zero_le_one, continuous_id, Continuous.sub, IsCompact.exists_isMaxOn, IsMaxFilter
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
hf : Continuous (X := ℝ) (Y := ℝ) (⇑f : (a : ℝ) → ℝ)
z : ℝ
hz : ∀ (x : ℝ), (f : (a : ℝ) → ℝ) x < x + z
obtain :
  ∀ (x : ℝ)
    (hx :
      ∀ (y : ℝ),
        Membership.mem (γ := Set ℝ) (Icc 0 1) y →
          HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) y : ℝ) y ≤ HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x),
    τ f < z
⊢ τ f < z

Tactic:
obtain ⟨x, -, hx⟩ : ∃ x ∈ Icc (0 : ℝ) 1, ∀ y ∈ Icc (0 : ℝ) 1, f y - y ≤ f x - x :=
    isCompact_Icc.exists_isMaxOn (nonempty_Icc.2 zero_le_one)
      (hf.sub continuous_id).continuousOn

Premises used: Iff.mpr, Continuous.continuousOn, Set.nonempty_Icc, CompactIccSpace.isCompact_Icc, zero_le_one, continuous_id, Set.Icc, OfNat.ofNat, Continuous.sub, IsCompact.exists_isMaxOn
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
hf : Continuous (X := ℝ) (Y := ℝ) (⇑f : (a : ℝ) → ℝ)
z : ℝ
hz : ∀ (x : ℝ), (f : (a : ℝ) → ℝ) x < x + z
x : ℝ
hx :
  ∀ (y : ℝ),
    Membership.mem (γ := Set ℝ) (Icc 0 1) y →
      HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) y : ℝ) y ≤ HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x
⊢ τ f < z

Tactic:
lt_of_le_of_lt ?_ (sub_lt_iff_lt_add'.2 <| hz x)

Premises used: Iff.mpr, lt_of_le_of_lt, sub_lt_iff_lt_add'
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
hf : Continuous (X := ℝ) (Y := ℝ) (⇑f : (a : ℝ) → ℝ)
z : ℝ
hz : ∀ (x : ℝ), (f : (a : ℝ) → ℝ) x < x + z
x : ℝ
hx :
  ∀ (y : ℝ),
    Membership.mem (γ := Set ℝ) (Icc 0 1) y →
      HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) y : ℝ) y ≤ HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x
refine : τ f ≤ HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x
⊢ τ f < z

Tactic:
refine lt_of_le_of_lt ?_ (sub_lt_iff_lt_add'.2 <| hz x)

Premises used: Iff.mpr, lt_of_le_of_lt, sub_lt_iff_lt_add'
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
hf : Continuous (X := ℝ) (Y := ℝ) (⇑f : (a : ℝ) → ℝ)
z : ℝ
hz : ∀ (x : ℝ), (f : (a : ℝ) → ℝ) x < x + z
x : ℝ
hx :
  ∀ (y : ℝ),
    Membership.mem (γ := Set ℝ) (Icc 0 1) y →
      HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) y : ℝ) y ≤ HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x
hz₁ : ∀ (x_1 : ℝ), (f : (a : ℝ) → ℝ) x_1 ≤ x_1 + HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x
⊢ τ f ≤ HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x

Tactic:
apply translationNumber_le_of_le_add

Premises used: CircleDeg1Lift.translationNumber_le_of_le_add
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
hf : Continuous (X := ℝ) (Y := ℝ) (⇑f : (a : ℝ) → ℝ)
z : ℝ
hz : ∀ (x : ℝ), (f : (a : ℝ) → ℝ) x < x + z
x : ℝ
hx :
  ∀ (y : ℝ),
    Membership.mem (γ := Set ℝ) (Icc 0 1) y →
      HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) y : ℝ) y ≤ HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x
hz₁ : ∀ (x_1 : ℝ), HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x_1 : ℝ) x_1 ≤ HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x
⊢ ∀ (x_1 : ℝ), (f : (a : ℝ) → ℝ) x_1 ≤ x_1 + HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x

Tactic:
simp only [← sub_le_iff_le_add']

Premises used: sub_le_iff_le_add'
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
hf : Continuous (X := ℝ) (Y := ℝ) (⇑f : (a : ℝ) → ℝ)
z : ℝ
hz : ∀ (x : ℝ), (f : (a : ℝ) → ℝ) x < x + z
x : ℝ
hx :
  ∀ (y : ℝ),
    Membership.mem (γ := Set ℝ) (Icc 0 1) y →
      HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) y : ℝ) y ≤ HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x
⊢ ∀ (x_1 : ℝ), HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x_1 : ℝ) x_1 ≤ HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x

Tactic:
f.forall_map_sub_of_Icc (fun a => a ≤ f x - x) hx

Premises used: CircleDeg1Lift.forall_map_sub_of_Icc, HSub.hSub, LE.le, DFunLike.coe
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
hf : Continuous (X := ℝ) (Y := ℝ) (⇑f : (a : ℝ) → ℝ)
z : ℝ
hz : ∀ (x : ℝ), (f : (a : ℝ) → ℝ) x < x + z
x : ℝ
hx :
  ∀ (y : ℝ),
    Membership.mem (γ := Set ℝ) (Icc 0 1) y →
      HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) y : ℝ) y ≤ HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x
⊢ ∀ (x_1 : ℝ), HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x_1 : ℝ) x_1 ≤ HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x

Tactic:
exact f.forall_map_sub_of_Icc (fun a => a ≤ f x - x) hx

Premises used: CircleDeg1Lift.forall_map_sub_of_Icc, HSub.hSub, LE.le, DFunLike.coe
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
hf : Continuous (X := ℝ) (Y := ℝ) (⇑f : (a : ℝ) → ℝ)
z : ℝ
hz : ∀ (x : ℝ), x + z < (f : (a : ℝ) → ℝ) x
⊢ ∃ (x : ℝ),
    Membership.mem (γ := Set ℝ) (Icc 0 1) x ∧
      ∀ (y : ℝ),
        Membership.mem (γ := Set ℝ) (Icc 0 1) y →
          HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x ≤ HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) y : ℝ) y

Tactic:
isCompact_Icc.exists_isMinOn (nonempty_Icc.2 zero_le_one) (hf.sub continuous_id).continuousOn

Premises used: Iff.mpr, Continuous.continuousOn, Set.Mem, Filter.Eventually, setOf, IsMinFilter, Set.nonempty_Icc, IsMinOn, CompactIccSpace.isCompact_Icc, Set.Subset, zero_le_one, continuous_id, IsCompact.exists_isMinOn, Continuous.sub
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
hf : Continuous (X := ℝ) (Y := ℝ) (⇑f : (a : ℝ) → ℝ)
z : ℝ
hz : ∀ (x : ℝ), x + z < (f : (a : ℝ) → ℝ) x
obtain :
  ∀ (x : ℝ)
    (hx :
      ∀ (y : ℝ),
        Membership.mem (γ := Set ℝ) (Icc 0 1) y →
          HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x ≤ HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) y : ℝ) y),
    z < τ f
⊢ z < τ f

Tactic:
obtain ⟨x, -, hx⟩ : ∃ x ∈ Icc (0 : ℝ) 1, ∀ y ∈ Icc (0 : ℝ) 1, f x - x ≤ f y - y :=
    isCompact_Icc.exists_isMinOn (nonempty_Icc.2 zero_le_one) (hf.sub continuous_id).continuousOn

Premises used: Iff.mpr, Continuous.continuousOn, Set.nonempty_Icc, CompactIccSpace.isCompact_Icc, zero_le_one, continuous_id, Set.Icc, IsCompact.exists_isMinOn, OfNat.ofNat, Continuous.sub
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
hf : Continuous (X := ℝ) (Y := ℝ) (⇑f : (a : ℝ) → ℝ)
z : ℝ
hz : ∀ (x : ℝ), x + z < (f : (a : ℝ) → ℝ) x
x : ℝ
hx :
  ∀ (y : ℝ),
    Membership.mem (γ := Set ℝ) (Icc 0 1) y →
      HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x ≤ HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) y : ℝ) y
⊢ z < τ f

Tactic:
lt_of_lt_of_le (lt_sub_iff_add_lt'.2 <| hz x) ?_

Premises used: Iff.mpr, lt_sub_iff_add_lt', lt_of_lt_of_le
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
hf : Continuous (X := ℝ) (Y := ℝ) (⇑f : (a : ℝ) → ℝ)
z : ℝ
hz : ∀ (x : ℝ), x + z < (f : (a : ℝ) → ℝ) x
x : ℝ
hx :
  ∀ (y : ℝ),
    Membership.mem (γ := Set ℝ) (Icc 0 1) y →
      HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x ≤ HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) y : ℝ) y
refine : HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x ≤ τ f
⊢ z < τ f

Tactic:
refine lt_of_lt_of_le (lt_sub_iff_add_lt'.2 <| hz x) ?_

Premises used: Iff.mpr, lt_sub_iff_add_lt', lt_of_lt_of_le
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
hf : Continuous (X := ℝ) (Y := ℝ) (⇑f : (a : ℝ) → ℝ)
z : ℝ
hz : ∀ (x : ℝ), x + z < (f : (a : ℝ) → ℝ) x
x : ℝ
hx :
  ∀ (y : ℝ),
    Membership.mem (γ := Set ℝ) (Icc 0 1) y →
      HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x ≤ HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) y : ℝ) y
hz₁ : ∀ (x_1 : ℝ), x_1 + HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x ≤ (f : (a : ℝ) → ℝ) x_1
⊢ HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x ≤ τ f

Tactic:
apply le_translationNumber_of_add_le

Premises used: CircleDeg1Lift.le_translationNumber_of_add_le
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
hf : Continuous (X := ℝ) (Y := ℝ) (⇑f : (a : ℝ) → ℝ)
z : ℝ
hz : ∀ (x : ℝ), x + z < (f : (a : ℝ) → ℝ) x
x : ℝ
hx :
  ∀ (y : ℝ),
    Membership.mem (γ := Set ℝ) (Icc 0 1) y →
      HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x ≤ HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) y : ℝ) y
hz₁ : ∀ (x_1 : ℝ), HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x ≤ HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x_1 : ℝ) x_1
⊢ ∀ (x_1 : ℝ), x_1 + HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x ≤ (f : (a : ℝ) → ℝ) x_1

Tactic:
simp only [← le_sub_iff_add_le']

Premises used: le_sub_iff_add_le'
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
hf : Continuous (X := ℝ) (Y := ℝ) (⇑f : (a : ℝ) → ℝ)
z : ℝ
hz : ∀ (x : ℝ), x + z < (f : (a : ℝ) → ℝ) x
x : ℝ
hx :
  ∀ (y : ℝ),
    Membership.mem (γ := Set ℝ) (Icc 0 1) y →
      HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x ≤ HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) y : ℝ) y
⊢ ∀ (x_1 : ℝ), HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x ≤ HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x_1 : ℝ) x_1

Tactic:
f.forall_map_sub_of_Icc _ hx

Premises used: CircleDeg1Lift.forall_map_sub_of_Icc
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
hf : Continuous (X := ℝ) (Y := ℝ) (⇑f : (a : ℝ) → ℝ)
z : ℝ
hz : ∀ (x : ℝ), x + z < (f : (a : ℝ) → ℝ) x
x : ℝ
hx :
  ∀ (y : ℝ),
    Membership.mem (γ := Set ℝ) (Icc 0 1) y →
      HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x ≤ HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) y : ℝ) y
⊢ ∀ (x_1 : ℝ), HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x ≤ HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x_1 : ℝ) x_1

Tactic:
exact f.forall_map_sub_of_Icc _ hx

Premises used: CircleDeg1Lift.forall_map_sub_of_Icc
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
hf : Continuous (X := ℝ) (Y := ℝ) (⇑f : (a : ℝ) → ℝ)
by_contra! : ∀ (H : ∀ (x : ℝ), x + τ f < (f : (a : ℝ) → ℝ) x), False
⊢ ∃ (x : ℝ), (f : (a : ℝ) → ℝ) x ≤ x + τ f

Tactic:
by_contra! H
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
hf : Continuous (X := ℝ) (Y := ℝ) (⇑f : (a : ℝ) → ℝ)
H : ∀ (x : ℝ), x + τ f < (f : (a : ℝ) → ℝ) x
⊢ False

Tactic:
lt_irrefl _ (f.lt_translationNumber_of_forall_add_lt hf H)

Premises used: lt_irrefl, CircleDeg1Lift.lt_translationNumber_of_forall_add_lt
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
hf : Continuous (X := ℝ) (Y := ℝ) (⇑f : (a : ℝ) → ℝ)
H : ∀ (x : ℝ), x + τ f < (f : (a : ℝ) → ℝ) x
⊢ False

Tactic:
exact lt_irrefl _ (f.lt_translationNumber_of_forall_add_lt hf H)

Premises used: lt_irrefl, CircleDeg1Lift.lt_translationNumber_of_forall_add_lt
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
hf : Continuous (X := ℝ) (Y := ℝ) (⇑f : (a : ℝ) → ℝ)
obtain : ∀ (a : ℝ) (ha : (f : (a : ℝ) → ℝ) a ≤ a + τ f), ∃ (x : ℝ), (f : (a : ℝ) → ℝ) x = x + τ f
⊢ ∃ (x : ℝ), (f : (a : ℝ) → ℝ) x = x + τ f

Tactic:
obtain ⟨a, ha⟩ : ∃ x, f x ≤ x + τ f := by
    by_contra! H
    exact lt_irrefl _ (f.lt_translationNumber_of_forall_add_lt hf H)

Premises used: CircleDeg1Lift.translationNumber
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
hf : Continuous (X := ℝ) (Y := ℝ) (⇑f : (a : ℝ) → ℝ)
a : ℝ
ha : (f : (a : ℝ) → ℝ) a ≤ a + τ f
by_contra! : ∀ (H : ∀ (x : ℝ), (f : (a : ℝ) → ℝ) x < x + τ f), False
⊢ ∃ (x : ℝ), x + τ f ≤ (f : (a : ℝ) → ℝ) x

Tactic:
by_contra! H
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
hf : Continuous (X := ℝ) (Y := ℝ) (⇑f : (a : ℝ) → ℝ)
a : ℝ
ha : (f : (a : ℝ) → ℝ) a ≤ a + τ f
H : ∀ (x : ℝ), (f : (a : ℝ) → ℝ) x < x + τ f
⊢ False

Tactic:
lt_irrefl _ (f.translationNumber_lt_of_forall_lt_add hf H)

Premises used: lt_irrefl, CircleDeg1Lift.translationNumber_lt_of_forall_lt_add
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
hf : Continuous (X := ℝ) (Y := ℝ) (⇑f : (a : ℝ) → ℝ)
a : ℝ
ha : (f : (a : ℝ) → ℝ) a ≤ a + τ f
H : ∀ (x : ℝ), (f : (a : ℝ) → ℝ) x < x + τ f
⊢ False

Tactic:
exact lt_irrefl _ (f.translationNumber_lt_of_forall_lt_add hf H)

Premises used: lt_irrefl, CircleDeg1Lift.translationNumber_lt_of_forall_lt_add
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
hf : Continuous (X := ℝ) (Y := ℝ) (⇑f : (a : ℝ) → ℝ)
a : ℝ
ha : (f : (a : ℝ) → ℝ) a ≤ a + τ f
obtain : ∀ (b : ℝ) (hb : b + τ f ≤ (f : (a : ℝ) → ℝ) b), ∃ (x : ℝ), (f : (a : ℝ) → ℝ) x = x + τ f
⊢ ∃ (x : ℝ), (f : (a : ℝ) → ℝ) x = x + τ f

Tactic:
obtain ⟨b, hb⟩ : ∃ x, x + τ f ≤ f x := by
    by_contra! H
    exact lt_irrefl _ (f.translationNumber_lt_of_forall_lt_add hf H)

Premises used: CircleDeg1Lift.translationNumber
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
hf : Continuous (X := ℝ) (Y := ℝ) (⇑f : (a : ℝ) → ℝ)
a : ℝ
ha : (f : (a : ℝ) → ℝ) a ≤ a + τ f
b : ℝ
hb : b + τ f ≤ (f : (a : ℝ) → ℝ) b
⊢ Continuous (Y := ℝ) fun (x : ℝ) ↦ x + τ f

Tactic:
fun_prop
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
hf : Continuous (X := ℝ) (Y := ℝ) (⇑f : (a : ℝ) → ℝ)
a : ℝ
ha : (f : (a : ℝ) → ℝ) a ≤ a + τ f
b : ℝ
hb : b + τ f ≤ (f : (a : ℝ) → ℝ) b
⊢ ∃ (x : ℝ), (f : (a : ℝ) → ℝ) x = x + τ f

Tactic:
exact intermediate_value_univ₂ hf (by fun_prop) ha hb

Premises used: intermediate_value_univ₂
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
hf : Continuous (X := ℝ) (Y := ℝ) (⇑f : (a : ℝ) → ℝ)
m : ℤ
mp : τ f = (↑m : ℝ) → ∃ (x : ℝ), (f : (a : ℝ) → ℝ) x = x + (↑m : ℝ)
mpr : (∃ (x : ℝ), (f : (a : ℝ) → ℝ) x = x + (↑m : ℝ)) → τ f = (↑m : ℝ)
⊢ τ f = (↑m : ℝ) ↔ ∃ (x : ℝ), (f : (a : ℝ) → ℝ) x = x + (↑m : ℝ)

Tactic:
constructor
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
hf : Continuous (X := ℝ) (Y := ℝ) (⇑f : (a : ℝ) → ℝ)
m : ℤ
h : τ f = (↑m : ℝ)
mp : ∃ (x : ℝ), (f : (a : ℝ) → ℝ) x = x + τ f
⊢ ∃ (x : ℝ), (f : (a : ℝ) → ℝ) x = x + (↑m : ℝ)

Tactic:
simp only [← h]
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
hf : Continuous (X := ℝ) (Y := ℝ) (⇑f : (a : ℝ) → ℝ)
m : ℤ
h : τ f = (↑m : ℝ)
⊢ ∃ (x : ℝ), (f : (a : ℝ) → ℝ) x = x + τ f

Tactic:
f.exists_eq_add_translationNumber hf

Premises used: CircleDeg1Lift.exists_eq_add_translationNumber
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
hf : Continuous (X := ℝ) (Y := ℝ) (⇑f : (a : ℝ) → ℝ)
m : ℤ
h : τ f = (↑m : ℝ)
⊢ ∃ (x : ℝ), (f : (a : ℝ) → ℝ) x = x + τ f

Tactic:
exact f.exists_eq_add_translationNumber hf

Premises used: CircleDeg1Lift.exists_eq_add_translationNumber
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
hf : Continuous (X := ℝ) (Y := ℝ) (⇑f : (a : ℝ) → ℝ)
m : ℤ
x : ℝ
hx : (f : (a : ℝ) → ℝ) x = x + (↑m : ℝ)
⊢ τ f = (↑m : ℝ)

Tactic:
f.translationNumber_of_eq_add_int hx

Premises used: CircleDeg1Lift.translationNumber_of_eq_add_int
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
hf : Continuous (X := ℝ) (Y := ℝ) (⇑f : (a : ℝ) → ℝ)
m : ℤ
x : ℝ
hx : (f : (a : ℝ) → ℝ) x = x + (↑m : ℝ)
⊢ τ f = (↑m : ℝ)

Tactic:
exact f.translationNumber_of_eq_add_int hx

Premises used: CircleDeg1Lift.translationNumber_of_eq_add_int
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
hf : Continuous (X := ℝ) (Y := ℝ) (⇑f : (a : ℝ) → ℝ)
n : ℕ
rw : Continuous (X := ℝ) (⇑f : (a : ℝ) → ℝ)^[n]
⊢ Continuous (X := ℝ) (Y := ℝ) (⇑(f ^ n) : (a : ℝ) → ℝ)

Tactic:
rw [coe_pow]

Premises used: CircleDeg1Lift.coe_pow
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
hf : Continuous (X := ℝ) (Y := ℝ) (⇑f : (a : ℝ) → ℝ)
n : ℕ
⊢ Continuous (X := ℝ) (⇑f : (a : ℝ) → ℝ)^[n]

Tactic:
hf.iterate n

Premises used: Continuous.iterate
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
hf : Continuous (X := ℝ) (Y := ℝ) (⇑f : (a : ℝ) → ℝ)
n : ℕ
⊢ Continuous (X := ℝ) (⇑f : (a : ℝ) → ℝ)^[n]

Tactic:
exact hf.iterate n

Premises used: Continuous.iterate
-- 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 : ℝ)
rw₁ : Ne (α := ℝ) (↑n : ℝ) 0
⊢ τ f = HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ↔ ∃ (x : ℝ), (f ^ n : (a : ℝ) → ℝ) x = x + (↑m : ℝ)

Tactic:
rw [eq_div_iff, mul_comm, ← translationNumber_pow]

Premises used: 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
⊢ Ne (α := ℝ) (↑n : ℝ) 0

Tactic:
ne_of_gt (Nat.cast_pos.2 hn)

Premises used: Iff.mpr, Nat.cast_pos, ne_of_gt
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
hf : Continuous (X := ℝ) (Y := ℝ) (⇑f : (a : ℝ) → ℝ)
m : ℤ
n : ℕ
hn : 0 < n
⊢ Ne (α := ℝ) (↑n : ℝ) 0

Tactic:
exact ne_of_gt (Nat.cast_pos.2 hn)

Premises used: Iff.mpr, Nat.cast_pos, ne_of_gt