ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasKernel f<VAR>X' Y' : C<VAR>f' : X' ⟶ Y'<VAR>CategoryTheory.Limits.HasKernel f'<VAR>sq : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk f'<GOAL>(CategoryTheory.Limits.kernelSubobjectIso f).hom ≫ CategoryTheory.Limits.kernel.map f f' sq.left sq.right ⋯ = CategoryTheory.Limits.kernelSubobjectMap sq ≫ (CategoryTheory.Limits.kernelSubobjectIso f').hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>A B : C<GOAL>CategoryTheory.Limits.kernelSubobject 0 = ⊤
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasKernel f<VAR>A : CategoryTheory.Subobject X<VAR>h : A.arrow ≫ f = 0<GOAL>A ≤ CategoryTheory.Limits.kernelSubobject f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X' : C<VAR>f : X' ⟶ X<VAR>CategoryTheory.IsIso f<VAR>g : X ⟶ Y<VAR>CategoryTheory.Limits.HasKernel g<GOAL>(CategoryTheory.Limits.kernelSubobjectIsoComp f g).hom ≫ (CategoryTheory.Limits.kernelSubobject g).arrow = (CategoryTheory.Limits.kernelSubobject (f ≫ g)).arrow ≫ f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X' : C<VAR>f : X' ⟶ X<VAR>CategoryTheory.IsIso f<VAR>g : X ⟶ Y<VAR>CategoryTheory.Limits.HasKernel g<GOAL>(CategoryTheory.Limits.kernelSubobjectIsoComp f g).inv ≫ (CategoryTheory.Limits.kernelSubobject (f ≫ g)).arrow = (CategoryTheory.Limits.kernelSubobject g).arrow ≫ CategoryTheory.inv f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasKernel f<VAR>Z : C<VAR>h : Y ⟶ Z<VAR>CategoryTheory.Limits.HasKernel (f ≫ h)<GOAL>CategoryTheory.Limits.kernelSubobject f ≤ CategoryTheory.Limits.kernelSubobject (f ≫ h)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasKernel f<VAR>Z : C<VAR>h : Y ⟶ Z<VAR>CategoryTheory.Mono h<GOAL>CategoryTheory.Limits.kernelSubobject (f ≫ h) = CategoryTheory.Limits.kernelSubobject f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasCokernels C<VAR>X : C<GOAL>∀ (a : CategoryTheory.Subobject X), (CategoryTheory.Limits.cokernelOrderHom X) a = CategoryTheory.Subobject.lift (fun A f x => CategoryTheory.Subobject.mk (CategoryTheory.Limits.cokernel.π f).op) ⋯ a
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasKernels C<VAR>X : C<GOAL>∀ (a : CategoryTheory.Subobject (Opposite.op X)), (CategoryTheory.Limits.kernelOrderHom X) a = CategoryTheory.Subobject.lift (fun A f x => CategoryTheory.Subobject.mk (CategoryTheory.Limits.kernel.ι f.unop)) ⋯ a
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasImage f<GOAL>(CategoryTheory.Limits.imageSubobjectIso f).hom ≫ CategoryTheory.Limits.image.ι f = (CategoryTheory.Limits.imageSubobject f).arrow
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasImage f<GOAL>(CategoryTheory.Limits.imageSubobjectIso f).inv ≫ (CategoryTheory.Limits.imageSubobject f).arrow = CategoryTheory.Limits.image.ι f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasImage f<GOAL>CategoryTheory.Limits.factorThruImageSubobject f ≫ (CategoryTheory.Limits.imageSubobject f).arrow = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>CategoryTheory.Limits.HasImage f<VAR>CategoryTheory.Epi (CategoryTheory.Limits.factorThruImageSubobject f)<VAR>h : f ≫ g = 0<GOAL>(CategoryTheory.Limits.imageSubobject f).arrow ≫ g = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasImage f<VAR>W : C<VAR>k : W ⟶ X<GOAL>(CategoryTheory.Limits.imageSubobject f).Factors (k ≫ f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasImage f<VAR>W : C<VAR>k : W ⟶ X<VAR>h : (CategoryTheory.Limits.imageSubobject f).Factors (k ≫ f)<GOAL>(CategoryTheory.Limits.imageSubobject f).factorThru (k ≫ f) h = k ≫ CategoryTheory.Limits.factorThruImageSubobject f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasImage f<VAR>W W' : C<VAR>k : W ⟶ W'<VAR>k' : W' ⟶ X<VAR>h : (CategoryTheory.Limits.imageSubobject f).Factors (k ≫ k' ≫ f)<GOAL>(CategoryTheory.Limits.imageSubobject f).factorThru (k ≫ k' ≫ f) h = k ≫ k' ≫ CategoryTheory.Limits.factorThruImageSubobject f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y X' : C<VAR>h : X' ⟶ X<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasImage f<VAR>CategoryTheory.Limits.HasImage (h ≫ f)<GOAL>CategoryTheory.Limits.imageSubobject (h ≫ f) ≤ CategoryTheory.Limits.imageSubobject f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasZeroObject C<GOAL>(CategoryTheory.Limits.imageSubobject 0).arrow = 0
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>CategoryTheory.Limits.HasZeroObject C<VAR>A B : C<GOAL>CategoryTheory.Limits.imageSubobject 0 = ⊥
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasEqualizers C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasImage f<VAR>Y' : C<VAR>h : Y ⟶ Y'<VAR>CategoryTheory.IsIso h<GOAL>(CategoryTheory.Limits.imageSubobjectCompIso f h).hom ≫ (CategoryTheory.Limits.imageSubobject f).arrow = (CategoryTheory.Limits.imageSubobject (f ≫ h)).arrow ≫ CategoryTheory.inv h
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasEqualizers C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasImage f<VAR>Y' : C<VAR>h : Y ⟶ Y'<VAR>CategoryTheory.IsIso h<GOAL>(CategoryTheory.Limits.imageSubobjectCompIso f h).inv ≫ (CategoryTheory.Limits.imageSubobject (f ≫ h)).arrow = (CategoryTheory.Limits.imageSubobject f).arrow ≫ h
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.Mono f<GOAL>CategoryTheory.Limits.imageSubobject f = CategoryTheory.Subobject.mk f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>X Y : C<VAR>CategoryTheory.Limits.HasEqualizers C<VAR>X' : C<VAR>h : X' ⟶ X<VAR>CategoryTheory.IsIso h<VAR>f : X ⟶ Y<VAR>CategoryTheory.Limits.HasImage f<GOAL>CategoryTheory.Limits.imageSubobject (h ≫ f) = CategoryTheory.Limits.imageSubobject f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A B : C<VAR>X : CategoryTheory.Subobject B<VAR>f : A ⟶ B<VAR>CategoryTheory.Limits.HasImage f<VAR>h : A ⟶ CategoryTheory.Subobject.underlying.obj X<VAR>w : h ≫ X.arrow = f<GOAL>CategoryTheory.Limits.imageSubobject f ≤ X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A B X : C<VAR>g : X ⟶ B<VAR>CategoryTheory.Mono g<VAR>f : A ⟶ B<VAR>CategoryTheory.Limits.HasImage f<VAR>h : A ⟶ X<VAR>w : h ≫ g = f<GOAL>CategoryTheory.Limits.imageSubobject f ≤ CategoryTheory.Subobject.mk g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>CategoryTheory.Limits.HasImage f<VAR>g : Y ⟶ Z<VAR>CategoryTheory.Limits.HasImage g<VAR>sq : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk g<VAR>CategoryTheory.Limits.HasImageMap sq<GOAL>CategoryTheory.Limits.imageSubobjectMap sq ≫ (CategoryTheory.Limits.imageSubobject g).arrow = (CategoryTheory.Limits.imageSubobject f).arrow ≫ sq.right
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>CategoryTheory.Limits.HasImage f<VAR>g : Y ⟶ Z<VAR>CategoryTheory.Limits.HasImage g<VAR>sq : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk g<VAR>CategoryTheory.Limits.HasImageMap sq<GOAL>CategoryTheory.Limits.image.map sq ≫ (CategoryTheory.Limits.imageSubobjectIso (CategoryTheory.Arrow.mk g).hom).inv = (CategoryTheory.Limits.imageSubobjectIso f).inv ≫ CategoryTheory.Limits.imageSubobjectMap sq
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>CategoryTheory.Limits.HasImage f<VAR>g : Y ⟶ Z<VAR>CategoryTheory.Limits.HasImage g<VAR>sq : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk g<VAR>CategoryTheory.Limits.HasImageMap sq<GOAL>(CategoryTheory.Limits.imageSubobjectIso (CategoryTheory.Arrow.mk f).hom).hom ≫ CategoryTheory.Limits.image.map sq = CategoryTheory.Limits.imageSubobjectMap sq ≫ (CategoryTheory.Limits.imageSubobjectIso g).hom
<VAR>R : Type u_1<VAR>C : Type u_2<VAR>Semiring R<VAR>CategoryTheory.Category.{u_3, u_2} C<VAR>CategoryTheory.Preadditive C<VAR>CategoryTheory.Linear R C<VAR>r : HomRel C<VAR>CategoryTheory.Congruence r<VAR>hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)<VAR>a : R<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>a • (CategoryTheory.Quotient.functor r).map f = (CategoryTheory.Quotient.functor r).map (a • f)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>P : C → Prop<VAR>self : CategoryTheory.ClosedUnderIsomorphisms P<VAR>X Y : C<GOAL>(X ≅ Y) → P X → P Y
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>P : C → Prop<VAR>CategoryTheory.ClosedUnderIsomorphisms P<VAR>X Y : C<VAR>e : X ≅ Y<VAR>hX : P X<GOAL>P Y
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>P : C → Prop<VAR>CategoryTheory.ClosedUnderIsomorphisms P<VAR>X Y : C<VAR>e : X ≅ Y<GOAL>P X ↔ P Y
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>P : C → Prop<VAR>CategoryTheory.ClosedUnderIsomorphisms P<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.IsIso f<VAR>hX : P X<GOAL>P Y
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>P : C → Prop<VAR>CategoryTheory.ClosedUnderIsomorphisms P<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>CategoryTheory.IsIso f<GOAL>P X ↔ P Y
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>P : C → Prop<VAR>X : C<GOAL>CategoryTheory.isoClosure P X ↔ ∃ Y x, Nonempty (X ≅ Y)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>P : C → Prop<VAR>X Y : C<VAR>h : P X<VAR>e : X ⟶ Y<VAR>CategoryTheory.IsIso e<GOAL>CategoryTheory.isoClosure P Y
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>P : C → Prop<GOAL>P ≤ CategoryTheory.isoClosure P
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>P Q : C → Prop<VAR>h : P ≤ Q<GOAL>CategoryTheory.isoClosure P ≤ CategoryTheory.isoClosure Q
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>P : C → Prop<VAR>CategoryTheory.ClosedUnderIsomorphisms P<GOAL>CategoryTheory.isoClosure P = P
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_2, u_1} C<VAR>P Q : C → Prop<VAR>CategoryTheory.ClosedUnderIsomorphisms Q<GOAL>CategoryTheory.isoClosure P ≤ Q ↔ P ≤ Q
<VAR>self : CircleDeg1Lift<VAR>x : ℝ<GOAL>self.toFun (x + 1) = self.toFun x + 1
<VAR>f : ℝ →o ℝ<VAR>h : ∀ (x : ℝ), f.toFun (x + 1) = f.toFun x + 1<GOAL>⇑{ toOrderHom := f, map_add_one' := h } = ⇑f
<VAR>f : CircleDeg1Lift<GOAL>⇑f.toOrderHom = ⇑f
<VAR>f : CircleDeg1Lift<GOAL>Monotone ⇑f
<VAR>f : CircleDeg1Lift<VAR>x y : ℝ<VAR>h : x ≤ y<GOAL>f x ≤ f y
<VAR>f : CircleDeg1Lift<GOAL>StrictMono ⇑f ↔ Function.Injective ⇑f
<VAR>f : CircleDeg1Lift<VAR>x : ℝ<GOAL>f (x + 1) = f x + 1
<VAR>f : CircleDeg1Lift<VAR>x : ℝ<GOAL>f (1 + x) = 1 + f x
<VAR>f g : CircleDeg1Lift<VAR>h : ∀ (x : ℝ), f x = g x<GOAL>f = g
<VAR>f g : CircleDeg1Lift<GOAL>f = g ↔ ∀ (x : ℝ), f x = g x
<VAR>f g : CircleDeg1Lift<GOAL>⇑(f * g) = ⇑f ∘ ⇑g
<VAR>f g : CircleDeg1Lift<VAR>x : ℝ<GOAL>(f * g) x = f (g x)
<VAR>f : CircleDeg1Liftˣ<VAR>x : ℝ<GOAL>↑f⁻¹ (↑f x) = x
<VAR>f : CircleDeg1Liftˣ<VAR>x : ℝ<GOAL>↑f (↑f⁻¹ x) = x
<VAR>f : CircleDeg1Liftˣ<GOAL>⇑(CircleDeg1Lift.toOrderIso f) = ⇑↑f
<VAR>f : CircleDeg1Liftˣ<GOAL>⇑(CircleDeg1Lift.toOrderIso f).symm = ⇑↑f⁻¹
<VAR>f : CircleDeg1Liftˣ<GOAL>⇑(CircleDeg1Lift.toOrderIso f)⁻¹ = ⇑↑f⁻¹
<VAR>f : CircleDeg1Lift<GOAL>IsUnit f ↔ Function.Bijective ⇑f
<VAR>f : CircleDeg1Lift<VAR>n : ℕ<GOAL>⇑(f ^ n) = (⇑f)^[n]
<VAR>f g₁ g₂ : CircleDeg1Lift<GOAL>SemiconjBy f g₁ g₂ ↔ Function.Semiconj ⇑f ⇑g₁ ⇑g₂
<VAR>f g : CircleDeg1Lift<GOAL>Commute f g ↔ Function.Commute ⇑f ⇑g
<VAR>x y : ℝ<GOAL>↑(CircleDeg1Lift.translate (Multiplicative.ofAdd x)) y = x + y
<VAR>x y : ℝ<GOAL>↑(CircleDeg1Lift.translate (Multiplicative.ofAdd x))⁻¹ y = -x + y
<VAR>x : ℝ<VAR>n : ℤ<GOAL>CircleDeg1Lift.translate (Multiplicative.ofAdd x) ^ n = CircleDeg1Lift.translate (Multiplicative.ofAdd (↑n * x))
<VAR>x : ℝ<VAR>n : ℕ<GOAL>CircleDeg1Lift.translate (Multiplicative.ofAdd x) ^ n = CircleDeg1Lift.translate (Multiplicative.ofAdd (↑n * x))
<VAR>x : ℝ<VAR>n : ℕ<GOAL>(⇑↑(CircleDeg1Lift.translate (Multiplicative.ofAdd x)))^[n] = ⇑↑(CircleDeg1Lift.translate (Multiplicative.ofAdd (↑n * x)))
<VAR>f : CircleDeg1Lift<VAR>n : ℕ<GOAL>Function.Commute ⇑f fun x => ↑n + x
<VAR>f : CircleDeg1Lift<VAR>n : ℕ<GOAL>Function.Commute ⇑f fun x => x + ↑n
<VAR>f : CircleDeg1Lift<VAR>n : ℕ<GOAL>Function.Commute ⇑f fun x => x - ↑n
<VAR>f : CircleDeg1Lift<VAR>n : ℤ<GOAL>Function.Commute ⇑f fun x => x + ↑n
<VAR>f : CircleDeg1Lift<VAR>n : ℤ<GOAL>Function.Commute ⇑f fun x => ↑n + x
<VAR>f : CircleDeg1Lift<VAR>n : ℤ<GOAL>Function.Commute ⇑f fun x => x - ↑n
<VAR>f : CircleDeg1Lift<VAR>m : ℤ<VAR>x : ℝ<GOAL>f (↑m + x) = ↑m + f x
<VAR>f : CircleDeg1Lift<VAR>x : ℝ<VAR>m : ℤ<GOAL>f (x + ↑m) = f x + ↑m
<VAR>f : CircleDeg1Lift<VAR>x : ℝ<VAR>n : ℤ<GOAL>f (x - ↑n) = f x - ↑n
<VAR>f : CircleDeg1Lift<VAR>x : ℝ<VAR>n : ℕ<GOAL>f (x + ↑n) = f x + ↑n
<VAR>f : CircleDeg1Lift<VAR>n : ℕ<VAR>x : ℝ<GOAL>f (↑n + x) = ↑n + f x
<VAR>f : CircleDeg1Lift<VAR>x : ℝ<VAR>n : ℕ<GOAL>f (x - ↑n) = f x - ↑n
<VAR>f : CircleDeg1Lift<VAR>n : ℤ<GOAL>f ↑n = f 0 + ↑n
<VAR>f : CircleDeg1Lift<VAR>x : ℝ<GOAL>f (Int.fract x) - Int.fract x = f x - x
<VAR>f g : CircleDeg1Lift<VAR>x : ℝ<GOAL>(f ⊔ g) x = max (f x) (g x)
<VAR>f g : CircleDeg1Lift<VAR>x : ℝ<GOAL>(f ⊓ g) x = min (f x) (g x)
<VAR>n : ℕ<GOAL>Monotone fun f => (⇑f)^[n]
<VAR>f g : CircleDeg1Lift<VAR>h : f ≤ g<VAR>n : ℕ<GOAL>(⇑f)^[n] ≤ (⇑g)^[n]
<VAR>f g : CircleDeg1Lift<VAR>h : f ≤ g<VAR>n : ℕ<GOAL>f ^ n ≤ g ^ n
<VAR>n : ℕ<GOAL>Monotone fun f => f ^ n
<VAR>f : CircleDeg1Lift<VAR>x : ℝ<GOAL>f x ≤ f 0 + ↑⌈x⌉
<VAR>f g : CircleDeg1Lift<GOAL>f (g 0) ≤ f 0 + ↑⌈g 0⌉
<VAR>f g : CircleDeg1Lift<GOAL>⌊f (g 0)⌋ ≤ ⌊f 0⌋ + ⌈g 0⌉
<VAR>f g : CircleDeg1Lift<GOAL>⌈f (g 0)⌉ ≤ ⌈f 0⌉ + ⌈g 0⌉
<VAR>f g : CircleDeg1Lift<GOAL>f (g 0) < f 0 + g 0 + 1
<VAR>f : CircleDeg1Lift<VAR>x : ℝ<GOAL>f 0 + ↑⌊x⌋ ≤ f x
<VAR>f g : CircleDeg1Lift<GOAL>f 0 + ↑⌊g 0⌋ ≤ f (g 0)
<VAR>f g : CircleDeg1Lift<GOAL>⌊f 0⌋ + ⌊g 0⌋ ≤ ⌊f (g 0)⌋
<VAR>f g : CircleDeg1Lift<GOAL>⌈f 0⌉ + ⌊g 0⌋ ≤ ⌈(f * g) 0⌉
<VAR>f g : CircleDeg1Lift<GOAL>f 0 + g 0 - 1 < f (g 0)
<VAR>f g₁ g₂ : CircleDeg1Lift<VAR>h : Function.Semiconj ⇑f ⇑g₁ ⇑g₂<GOAL>dist (g₁ 0) (g₂ 0) < 2
<VAR>f g₁ g₂ : CircleDeg1Lift<VAR>h : SemiconjBy f g₁ g₂<GOAL>dist (g₁ 0) (g₂ 0) < 2
<VAR>f : CircleDeg1Lift<GOAL>Filter.Tendsto (⇑f) Filter.atBot Filter.atBot
<VAR>f : CircleDeg1Lift<GOAL>Filter.Tendsto (⇑f) Filter.atTop Filter.atTop
<VAR>f : CircleDeg1Lift<GOAL>Continuous ⇑f ↔ Function.Surjective ⇑f
<VAR>f : CircleDeg1Lift<VAR>x : ℝ<VAR>m : ℤ<VAR>h : f x ≤ x + ↑m<VAR>n : ℕ<GOAL>(⇑f)^[n] x ≤ x + ↑n * ↑m
<VAR>f : CircleDeg1Lift<VAR>x : ℝ<VAR>m : ℤ<VAR>h : x + ↑m ≤ f x<VAR>n : ℕ<GOAL>x + ↑n * ↑m ≤ (⇑f)^[n] x
<VAR>f : CircleDeg1Lift<VAR>x : ℝ<VAR>m : ℤ<VAR>h : f x = x + ↑m<VAR>n : ℕ<GOAL>(⇑f)^[n] x = x + ↑n * ↑m
<VAR>f : CircleDeg1Lift<VAR>x : ℝ<VAR>m : ℤ<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>(⇑f)^[n] x ≤ x + ↑n * ↑m ↔ f x ≤ x + ↑m
<VAR>f : CircleDeg1Lift<VAR>x : ℝ<VAR>m : ℤ<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>(⇑f)^[n] x < x + ↑n * ↑m ↔ f x < x + ↑m
<VAR>f : CircleDeg1Lift<VAR>x : ℝ<VAR>m : ℤ<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>(⇑f)^[n] x = x + ↑n * ↑m ↔ f x = x + ↑m
<VAR>f : CircleDeg1Lift<VAR>x : ℝ<VAR>m : ℤ<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>x + ↑n * ↑m ≤ (⇑f)^[n] x ↔ x + ↑m ≤ f x
<VAR>f : CircleDeg1Lift<VAR>x : ℝ<VAR>m : ℤ<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>x + ↑n * ↑m < (⇑f)^[n] x ↔ x + ↑m < f x
<VAR>f : CircleDeg1Lift<VAR>n : ℕ<GOAL>↑n * ⌊f 0⌋ ≤ ⌊(⇑f)^[n] 0⌋
<VAR>f : CircleDeg1Lift<GOAL>f.transnumAuxSeq = fun n => (f ^ 2 ^ n) 0 / 2 ^ n
<VAR>f : CircleDeg1Lift<VAR>τ' : ℝ<VAR>h : Filter.Tendsto f.transnumAuxSeq Filter.atTop (𝓝 τ')<GOAL>f.translationNumber = τ'
<VAR>f : CircleDeg1Lift<VAR>τ' : ℝ<VAR>h : Filter.Tendsto (fun n => (⇑f)^[n] 0 / ↑n) Filter.atTop (𝓝 τ')<GOAL>f.translationNumber = τ'
<VAR>f : CircleDeg1Lift<VAR>τ' : ℝ<VAR>h : Filter.Tendsto (fun n => (⇑f)^[n + 1] 0 / (↑n + 1)) Filter.atTop (𝓝 τ')<GOAL>f.translationNumber = τ'
<VAR>f : CircleDeg1Lift<GOAL>f.transnumAuxSeq 0 = f 0
<VAR>f : CircleDeg1Lift<VAR>n : ℕ<GOAL>dist (f.transnumAuxSeq n) (f.transnumAuxSeq (n + 1)) < 1 / 2 / 2 ^ n
<VAR>f : CircleDeg1Lift<GOAL>Filter.Tendsto f.transnumAuxSeq Filter.atTop (𝓝 f.translationNumber)
<VAR>f : CircleDeg1Lift<GOAL>dist (f 0) f.translationNumber ≤ 1
<VAR>f : CircleDeg1Lift<VAR>x : ℕ → ℝ<VAR>C : ℝ<VAR>H : ∀ (n : ℕ), dist ((f ^ n) 0) (x n) ≤ C<GOAL>Filter.Tendsto (fun n => x (2 ^ n) / 2 ^ n) Filter.atTop (𝓝 f.translationNumber)
<VAR>f g : CircleDeg1Lift<VAR>C : ℝ<VAR>H : ∀ (n : ℕ), dist ((f ^ n) 0) ((g ^ n) 0) ≤ C<GOAL>f.translationNumber = g.translationNumber
<GOAL>CircleDeg1Lift.translationNumber 1 = 0
<VAR>f g₁ g₂ : CircleDeg1Lift<VAR>H : SemiconjBy f g₁ g₂<GOAL>g₁.translationNumber = g₂.translationNumber
<VAR>f g₁ g₂ : CircleDeg1Lift<VAR>H : Function.Semiconj ⇑f ⇑g₁ ⇑g₂<GOAL>g₁.translationNumber = g₂.translationNumber
<VAR>f g : CircleDeg1Lift<VAR>h : Commute f g<GOAL>(f * g).translationNumber = f.translationNumber + g.translationNumber
<VAR>f : CircleDeg1Liftˣ<GOAL>(↑f⁻¹).translationNumber = -(↑f).translationNumber
<VAR>f : CircleDeg1Lift<VAR>n : ℕ<GOAL>(f ^ n).translationNumber = ↑n * f.translationNumber
<VAR>f : CircleDeg1Liftˣ<VAR>n : ℤ<GOAL>(↑(f ^ n)).translationNumber = ↑n * (↑f).translationNumber
<VAR>f : CircleDeg1Liftˣ<VAR>g : CircleDeg1Lift<GOAL>(↑f * g * ↑f⁻¹).translationNumber = g.translationNumber
<VAR>f : CircleDeg1Liftˣ<VAR>g : CircleDeg1Lift<GOAL>(↑f⁻¹ * g * ↑f).translationNumber = g.translationNumber
<VAR>f : CircleDeg1Lift<VAR>n : ℕ<GOAL>dist ((f ^ n) 0) (↑n * f.translationNumber) ≤ 1
<VAR>f : CircleDeg1Lift<GOAL>Filter.Tendsto (fun n => (f ^ (n + 1)) 0 / (↑n + 1)) Filter.atTop (𝓝 f.translationNumber)
<VAR>f : CircleDeg1Lift<GOAL>Filter.Tendsto (fun n => (f ^ n) 0 / ↑n) Filter.atTop (𝓝 f.translationNumber)
<VAR>f : CircleDeg1Lift<VAR>x : ℝ<GOAL>Filter.Tendsto (fun n => ((f ^ n) x - x) / ↑n) Filter.atTop (𝓝 f.translationNumber)
<VAR>f : CircleDeg1Lift<VAR>x : ℝ<GOAL>Filter.Tendsto (fun n => ((f ^ (n + 1)) x - x) / (↑n + 1)) Filter.atTop (𝓝 f.translationNumber)
<VAR>x : ℝ<GOAL>(↑(CircleDeg1Lift.translate (Multiplicative.ofAdd x))).translationNumber = x
<VAR>f : CircleDeg1Lift<VAR>z : ℝ<VAR>hz : ∀ (x : ℝ), f x ≤ x + z<GOAL>f.translationNumber ≤ z
<VAR>f : CircleDeg1Lift<VAR>z : ℝ<VAR>hz : ∀ (x : ℝ), x + z ≤ f x<GOAL>z ≤ f.translationNumber
<VAR>f : CircleDeg1Lift<VAR>x : ℝ<VAR>m : ℤ<VAR>h : f x ≤ x + ↑m<GOAL>f.translationNumber ≤ ↑m
<VAR>f : CircleDeg1Lift<VAR>x : ℝ<VAR>m : ℕ<VAR>h : f x ≤ x + ↑m<GOAL>f.translationNumber ≤ ↑m
<VAR>f : CircleDeg1Lift<VAR>x : ℝ<VAR>m : ℤ<VAR>h : x + ↑m ≤ f x<GOAL>↑m ≤ f.translationNumber
<VAR>f : CircleDeg1Lift<VAR>x : ℝ<VAR>m : ℕ<VAR>h : x + ↑m ≤ f x<GOAL>↑m ≤ f.translationNumber
<VAR>f : CircleDeg1Lift<VAR>x : ℝ<VAR>m : ℤ<VAR>h : f x = x + ↑m<GOAL>f.translationNumber = ↑m
<VAR>f : CircleDeg1Lift<VAR>x : ℝ<GOAL>↑⌊f x - x⌋ ≤ f.translationNumber
<VAR>f : CircleDeg1Lift<VAR>x : ℝ<GOAL>f.translationNumber ≤ ↑⌈f x - x⌉
<VAR>f : CircleDeg1Lift<VAR>n : ℤ<VAR>h : f.translationNumber < ↑n<VAR>x : ℝ<GOAL>f x < x + ↑n
<VAR>f : CircleDeg1Lift<VAR>n : ℕ<VAR>h : f.translationNumber < ↑n<VAR>x : ℝ<GOAL>f x < x + ↑n
<VAR>f : CircleDeg1Lift<VAR>x : ℝ<GOAL>f x < x + ↑⌊f.translationNumber⌋ + 1
<VAR>f : CircleDeg1Lift<VAR>x : ℝ<GOAL>f x < x + f.translationNumber + 1
<VAR>f : CircleDeg1Lift<VAR>n : ℤ<VAR>h : ↑n < f.translationNumber<VAR>x : ℝ<GOAL>x + ↑n < f x
<VAR>f : CircleDeg1Lift<VAR>n : ℕ<VAR>h : ↑n < f.translationNumber<VAR>x : ℝ<GOAL>x + ↑n < f x
<VAR>f : CircleDeg1Lift<VAR>x : ℝ<VAR>n : ℕ<VAR>m : ℤ<VAR>h : (f ^ n) x = x + ↑m<VAR>hn : 0 < n<GOAL>f.translationNumber = ↑m / ↑n
<VAR>f : CircleDeg1Lift<VAR>P : ℝ → Prop<VAR>h : ∀ x ∈ Set.Icc 0 1, P (f x - x)<VAR>x : ℝ<GOAL>P (f x - x)
<VAR>f : CircleDeg1Lift<VAR>hf : Continuous ⇑f<VAR>z : ℝ<VAR>hz : ∀ (x : ℝ), f x < x + z<GOAL>f.translationNumber < z
<VAR>f : CircleDeg1Lift<VAR>hf : Continuous ⇑f<VAR>z : ℝ<VAR>hz : ∀ (x : ℝ), x + z < f x<GOAL>z < f.translationNumber
<VAR>f : CircleDeg1Lift<VAR>hf : Continuous ⇑f<GOAL>∃ x, f x = x + f.translationNumber
<VAR>f : CircleDeg1Lift<VAR>hf : Continuous ⇑f<VAR>m : ℤ<GOAL>f.translationNumber = ↑m ↔ ∃ x, f x = x + ↑m
<VAR>f : CircleDeg1Lift<VAR>hf : Continuous ⇑f<VAR>n : ℕ<GOAL>Continuous ⇑(f ^ n)
<VAR>f : CircleDeg1Lift<VAR>hf : Continuous ⇑f<VAR>m : ℤ<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>f.translationNumber = ↑m / ↑n ↔ ∃ x, (f ^ n) x = x + ↑m
<VAR>G : Type u_1<VAR>Group G<VAR>f₁ f₂ : G →* CircleDeg1Lift<VAR>h : ∀ (g : G), (f₁ g).translationNumber = (f₂ g).translationNumber<GOAL>∃ F, ∀ (g : G), Function.Semiconj ⇑F ⇑(f₁ g) ⇑(f₂ g)
<VAR>f₁ f₂ : CircleDeg1Liftˣ<VAR>h : (↑f₁).translationNumber = (↑f₂).translationNumber<GOAL>∃ F, Function.Semiconj ⇑F ⇑↑f₁ ⇑↑f₂
<VAR>f₁ f₂ : CircleDeg1Lift<VAR>h₁ : IsUnit f₁<VAR>h₂ : IsUnit f₂<VAR>h : f₁.translationNumber = f₂.translationNumber<GOAL>∃ F, Function.Semiconj ⇑F ⇑f₁ ⇑f₂
<VAR>f₁ f₂ : CircleDeg1Lift<VAR>h₁ : Function.Bijective ⇑f₁<VAR>h₂ : Function.Bijective ⇑f₂<VAR>h : f₁.translationNumber = f₂.translationNumber<GOAL>∃ F, Function.Semiconj ⇑F ⇑f₁ ⇑f₂
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v, u₂} D<VAR>S : D<VAR>T : CategoryTheory.Functor C D<VAR>CategoryTheory.Limits.HasLimits C<VAR>CategoryTheory.Limits.PreservesLimits T<VAR>A P : CategoryTheory.StructuredArrow S T<VAR>f : P ⟶ A<VAR>CategoryTheory.Mono f<GOAL>CategoryTheory.StructuredArrow.projectSubobject (CategoryTheory.Subobject.mk f) = CategoryTheory.Subobject.mk f.right
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v, u₂} D<VAR>S : D<VAR>T : CategoryTheory.Functor C D<VAR>CategoryTheory.Limits.HasLimits C<VAR>CategoryTheory.Limits.PreservesLimits T<VAR>A : CategoryTheory.StructuredArrow S T<VAR>P : CategoryTheory.Subobject A<GOAL>∃ q, CategoryTheory.CategoryStruct.comp q (T.map (CategoryTheory.StructuredArrow.projectSubobject P).arrow) = A.hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v, u₂} D<VAR>S : D<VAR>T : CategoryTheory.Functor C D<VAR>CategoryTheory.Limits.HasLimits C<VAR>CategoryTheory.Limits.PreservesLimits T<VAR>A : CategoryTheory.StructuredArrow S T<VAR>P : CategoryTheory.Subobject A<VAR>q : (CategoryTheory.Functor.fromPUnit S).obj A.left ⟶ T.obj (CategoryTheory.Subobject.underlying.obj (CategoryTheory.StructuredArrow.projectSubobject P))<VAR>hq : CategoryTheory.CategoryStruct.comp q (T.map (CategoryTheory.StructuredArrow.projectSubobject P).arrow) = A.hom<GOAL>CategoryTheory.StructuredArrow.liftSubobject (CategoryTheory.StructuredArrow.projectSubobject P) hq = P
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v, u₂} D<VAR>S : D<VAR>T : CategoryTheory.Functor C D<VAR>CategoryTheory.Limits.HasLimits C<VAR>CategoryTheory.Limits.PreservesLimits T<VAR>A : CategoryTheory.StructuredArrow S T<VAR>P : CategoryTheory.Subobject A<GOAL>↑(A.subobjectEquiv P) = CategoryTheory.StructuredArrow.projectSubobject P
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v, u₂} D<VAR>S : D<VAR>T : CategoryTheory.Functor C D<VAR>CategoryTheory.Limits.HasLimits C<VAR>CategoryTheory.Limits.PreservesLimits T<VAR>A : CategoryTheory.StructuredArrow S T<VAR>P : { P // ∃ q, CategoryTheory.CategoryStruct.comp q (T.map P.arrow) = A.hom }<GOAL>(RelIso.symm A.subobjectEquiv) P = CategoryTheory.Subobject.mk (CategoryTheory.StructuredArrow.homMk (↑P).arrow ⋯)