ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>L : FirstOrder.Language<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>(i : ι) → L.Structure (G i)<VAR>f : (i j : ι) → i ≤ j → G i ↪[L] G j<VAR>DirectedSystem G fun i j h => ⇑(f i j h)<VAR>α : Type u_1<VAR>x : α → FirstOrder.Language.Structure.Sigma f<VAR>i j : ι<VAR>ij : i ≤ j<VAR>h : i ∈ upperBounds (Set.range (Sigma.fst ∘ x))<GOAL>⇑(f i j ij) ∘ FirstOrder.Language.DirectLimit.unify f x i h = FirstOrder.Language.DirectLimit.unify f x j ⋯
<VAR>L : FirstOrder.Language<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>(i : ι) → L.Structure (G i)<VAR>f : (i j : ι) → i ≤ j → G i ↪[L] G j<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>DirectedSystem G fun i j h => ⇑(f i j h)<VAR>x y : FirstOrder.Language.Structure.Sigma f<VAR>i : ι<VAR>hx : x.fst ≤ i<VAR>hy : y.fst ≤ i<GOAL>x ≈ y ↔ (f x.fst i hx) x.snd = (f y.fst i hy) y.snd
<VAR>L : FirstOrder.Language<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>(i : ι) → L.Structure (G i)<VAR>f : (i j : ι) → i ≤ j → G i ↪[L] G j<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>DirectedSystem G fun i j h => ⇑(f i j h)<VAR>n : ℕ<VAR>F : L.Functions n<VAR>x : Fin n → FirstOrder.Language.Structure.Sigma f<VAR>i j : ι<VAR>hi : i ∈ upperBounds (Set.range (Sigma.fst ∘ x))<VAR>hj : j ∈ upperBounds (Set.range (Sigma.fst ∘ x))<GOAL>FirstOrder.Language.Structure.Sigma.mk f i (FirstOrder.Language.Structure.funMap F (FirstOrder.Language.DirectLimit.unify f x i hi)) ≈ FirstOrder.Language.Structure.Sigma.mk f j (FirstOrder.Language.Structure.funMap F (FirstOrder.Language.DirectLimit.unify f x j hj))
<VAR>L : FirstOrder.Language<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>(i : ι) → L.Structure (G i)<VAR>f : (i j : ι) → i ≤ j → G i ↪[L] G j<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>DirectedSystem G fun i j h => ⇑(f i j h)<VAR>n : ℕ<VAR>R : L.Relations n<VAR>x : Fin n → FirstOrder.Language.Structure.Sigma f<VAR>i j : ι<VAR>hi : i ∈ upperBounds (Set.range (Sigma.fst ∘ x))<VAR>hj : j ∈ upperBounds (Set.range (Sigma.fst ∘ x))<GOAL>FirstOrder.Language.Structure.RelMap R (FirstOrder.Language.DirectLimit.unify f x i hi) = FirstOrder.Language.Structure.RelMap R (FirstOrder.Language.DirectLimit.unify f x j hj)
<VAR>L : FirstOrder.Language<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>(i : ι) → L.Structure (G i)<VAR>f : (i j : ι) → i ≤ j → G i ↪[L] G j<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>DirectedSystem G fun i j h => ⇑(f i j h)<VAR>Nonempty ι<VAR>α : Type u_1<VAR>Finite α<VAR>x y : α → FirstOrder.Language.Structure.Sigma f<VAR>xy : x ≈ y<GOAL>∃ i, ∃ (hx : i ∈ upperBounds (Set.range (Sigma.fst ∘ x))) (hy : i ∈ upperBounds (Set.range (Sigma.fst ∘ y))), FirstOrder.Language.DirectLimit.unify f x i hx = FirstOrder.Language.DirectLimit.unify f y i hy
<VAR>L : FirstOrder.Language<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>(i : ι) → L.Structure (G i)<VAR>f : (i j : ι) → i ≤ j → G i ↪[L] G j<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>DirectedSystem G fun i j h => ⇑(f i j h)<VAR>Nonempty ι<VAR>n : ℕ<VAR>F : L.Functions n<VAR>x : Fin n → FirstOrder.Language.Structure.Sigma f<VAR>i : ι<VAR>hi : i ∈ upperBounds (Set.range (Sigma.fst ∘ x))<GOAL>FirstOrder.Language.Structure.funMap F x ≈ FirstOrder.Language.Structure.Sigma.mk f i (FirstOrder.Language.Structure.funMap F (FirstOrder.Language.DirectLimit.unify f x i hi))
<VAR>L : FirstOrder.Language<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>(i : ι) → L.Structure (G i)<VAR>f : (i j : ι) → i ≤ j → G i ↪[L] G j<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>DirectedSystem G fun i j h => ⇑(f i j h)<VAR>Nonempty ι<VAR>n : ℕ<VAR>R : L.Relations n<VAR>x : Fin n → FirstOrder.Language.Structure.Sigma f<VAR>i : ι<VAR>hi : i ∈ upperBounds (Set.range (Sigma.fst ∘ x))<GOAL>FirstOrder.Language.Structure.RelMap R x = FirstOrder.Language.Structure.RelMap R (FirstOrder.Language.DirectLimit.unify f x i hi)
<VAR>L : FirstOrder.Language<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>(i : ι) → L.Structure (G i)<VAR>f : (i j : ι) → i ≤ j → G i ↪[L] G j<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>DirectedSystem G fun i j h => ⇑(f i j h)<VAR>Nonempty ι<VAR>n : ℕ<VAR>F : L.Functions n<VAR>i : ι<VAR>x : Fin n → G i<GOAL>(FirstOrder.Language.Structure.funMap F fun a => ⟦FirstOrder.Language.Structure.Sigma.mk f i (x a)⟧) = ⟦FirstOrder.Language.Structure.Sigma.mk f i (FirstOrder.Language.Structure.funMap F x)⟧
<VAR>L : FirstOrder.Language<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>(i : ι) → L.Structure (G i)<VAR>f : (i j : ι) → i ≤ j → G i ↪[L] G j<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>DirectedSystem G fun i j h => ⇑(f i j h)<VAR>Nonempty ι<VAR>n : ℕ<VAR>R : L.Relations n<VAR>i : ι<VAR>x : Fin n → G i<GOAL>(FirstOrder.Language.Structure.RelMap R fun a => ⟦FirstOrder.Language.Structure.Sigma.mk f i (x a)⟧) = FirstOrder.Language.Structure.RelMap R x
<VAR>L : FirstOrder.Language<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>(i : ι) → L.Structure (G i)<VAR>f : (i j : ι) → i ≤ j → G i ↪[L] G j<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>DirectedSystem G fun i j h => ⇑(f i j h)<VAR>Nonempty ι<VAR>α : Type u_1<VAR>Finite α<VAR>x : α → FirstOrder.Language.DirectLimit G f<GOAL>∃ i y, x = fun a => ⟦FirstOrder.Language.Structure.Sigma.mk f i (y a)⟧
<VAR>L : FirstOrder.Language<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>(i : ι) → L.Structure (G i)<VAR>f : (i j : ι) → i ≤ j → G i ↪[L] G j<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>DirectedSystem G fun i j h => ⇑(f i j h)<VAR>Nonempty ι<VAR>i : ι<VAR>x : G i<GOAL>(FirstOrder.Language.DirectLimit.of L ι G f i) x = ⟦FirstOrder.Language.Structure.Sigma.mk f i x⟧
<VAR>L : FirstOrder.Language<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>(i : ι) → L.Structure (G i)<VAR>f : (i j : ι) → i ≤ j → G i ↪[L] G j<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>DirectedSystem G fun i j h => ⇑(f i j h)<VAR>Nonempty ι<VAR>i j : ι<VAR>hij : i ≤ j<VAR>x : G i<GOAL>(FirstOrder.Language.DirectLimit.of L ι G f j) ((f i j hij) x) = (FirstOrder.Language.DirectLimit.of L ι G f i) x
<VAR>L : FirstOrder.Language<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>(i : ι) → L.Structure (G i)<VAR>f : (i j : ι) → i ≤ j → G i ↪[L] G j<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>DirectedSystem G fun i j h => ⇑(f i j h)<VAR>Nonempty ι<VAR>z : FirstOrder.Language.DirectLimit G f<GOAL>∃ i x, (FirstOrder.Language.DirectLimit.of L ι G f i) x = z
<VAR>L : FirstOrder.Language<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>(i : ι) → L.Structure (G i)<VAR>f : (i j : ι) → i ≤ j → G i ↪[L] G j<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>DirectedSystem G fun i j h => ⇑(f i j h)<VAR>Nonempty ι<VAR>C : FirstOrder.Language.DirectLimit G f → Prop<VAR>z : FirstOrder.Language.DirectLimit G f<VAR>ih : ∀ (i : ι) (x : G i), C ((FirstOrder.Language.DirectLimit.of L ι G f i) x)<GOAL>C z
<VAR>L : FirstOrder.Language<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>(i : ι) → L.Structure (G i)<VAR>f : (i j : ι) → i ≤ j → G i ↪[L] G j<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>DirectedSystem G fun i j h => ⇑(f i j h)<VAR>Nonempty ι<GOAL>⨆ i, (FirstOrder.Language.DirectLimit.of L ι G f i).toHom.range = ⊤
<VAR>L : FirstOrder.Language<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>(i : ι) → L.Structure (G i)<VAR>f : (i j : ι) → i ≤ j → G i ↪[L] G j<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>DirectedSystem G fun i j h => ⇑(f i j h)<VAR>Nonempty ι<VAR>S : L.Substructure (FirstOrder.Language.DirectLimit G f)<VAR>S_fg : S.FG<GOAL>∃ i T, FirstOrder.Language.Substructure.map (FirstOrder.Language.DirectLimit.of L ι G f i).toHom T = S
<VAR>L : FirstOrder.Language<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>(i : ι) → L.Structure (G i)<VAR>f : (i j : ι) → i ≤ j → G i ↪[L] G j<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>DirectedSystem G fun i j h => ⇑(f i j h)<VAR>Nonempty ι<VAR>P : Type u₁<VAR>L.Structure P<VAR>g : (i : ι) → G i ↪[L] P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x<VAR>i : ι<VAR>x : G i<GOAL>(FirstOrder.Language.DirectLimit.lift L ι G f g Hg) ⟦FirstOrder.Language.Structure.Sigma.mk f i x⟧ = (g i) x
<VAR>L : FirstOrder.Language<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>(i : ι) → L.Structure (G i)<VAR>f : (i j : ι) → i ≤ j → G i ↪[L] G j<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>DirectedSystem G fun i j h => ⇑(f i j h)<VAR>Nonempty ι<VAR>P : Type u₁<VAR>L.Structure P<VAR>g : (i : ι) → G i ↪[L] P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x<VAR>i : ι<VAR>x : G i<GOAL>(FirstOrder.Language.DirectLimit.lift L ι G f g Hg) ((FirstOrder.Language.DirectLimit.of L ι G f i) x) = (g i) x
<VAR>L : FirstOrder.Language<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>(i : ι) → L.Structure (G i)<VAR>f : (i j : ι) → i ≤ j → G i ↪[L] G j<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>DirectedSystem G fun i j h => ⇑(f i j h)<VAR>Nonempty ι<VAR>P : Type u₁<VAR>L.Structure P<VAR>F : FirstOrder.Language.DirectLimit G f ↪[L] P<VAR>x : FirstOrder.Language.DirectLimit G f<GOAL>F x = (FirstOrder.Language.DirectLimit.lift L ι G f (fun i => F.comp (FirstOrder.Language.DirectLimit.of L ι G f i)) ⋯) x
<VAR>L : FirstOrder.Language<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>(i : ι) → L.Structure (G i)<VAR>f : (i j : ι) → i ≤ j → G i ↪[L] G j<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>DirectedSystem G fun i j h => ⇑(f i j h)<VAR>Nonempty ι<VAR>P : Type u₁<VAR>L.Structure P<VAR>g : (i : ι) → G i ↪[L] P<VAR>Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x<GOAL>(FirstOrder.Language.DirectLimit.lift L ι G f g Hg).toHom.range = ⨆ i, (g i).toHom.range
<VAR>L : FirstOrder.Language<VAR>ι : Type v<VAR>Preorder ι<VAR>G : ι → Type w<VAR>(i : ι) → L.Structure (G i)<VAR>f : (i j : ι) → i ≤ j → G i ↪[L] G j<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>DirectedSystem G fun i j h => ⇑(f i j h)<VAR>Nonempty ι<VAR>G' : ι → Type w'<VAR>(i : ι) → L.Structure (G' i)<VAR>f' : (i j : ι) → i ≤ j → G' i ↪[L] G' j<VAR>g : (i : ι) → G i ≃[L] G' i<VAR>H_commuting : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (f' i j hij) ((g i) x)<VAR>DirectedSystem G' fun i j h => ⇑(f' i j h)<VAR>i : ι<VAR>x : G i<GOAL>(FirstOrder.Language.DirectLimit.equiv_lift L ι G f G' f' g H_commuting) ((FirstOrder.Language.DirectLimit.of L ι G f i) x) = (FirstOrder.Language.DirectLimit.of L ι G' f' i) ((g i) x)
<VAR>L : FirstOrder.Language<VAR>ι : Type u_1<VAR>Countable ι<VAR>Preorder ι<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>Nonempty ι<VAR>G : ι → Type w<VAR>(i : ι) → L.Structure (G i)<VAR>f : (i j : ι) → i ≤ j → G i ↪[L] G j<VAR>h : ∀ (i : ι), FirstOrder.Language.Structure.CG L (G i)<VAR>DirectedSystem G fun i j h => ⇑(f i j h)<GOAL>FirstOrder.Language.Structure.CG L (FirstOrder.Language.DirectLimit G f)
<VAR>L : FirstOrder.Language<VAR>ι : Type v<VAR>Preorder ι<VAR>Nonempty ι<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>M : Type u_1<VAR>L.Structure M<VAR>S : ι →o L.Substructure M<VAR>i : ι<VAR>x : ↥(S i)<GOAL>(FirstOrder.Language.DirectLimit.liftInclusion S) ((FirstOrder.Language.DirectLimit.of L ι (fun x => ↥(S x)) (fun x x_1 h => FirstOrder.Language.Substructure.inclusion ⋯) i) x) = (S i).subtype x
<VAR>L : FirstOrder.Language<VAR>ι : Type v<VAR>Preorder ι<VAR>Nonempty ι<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>M : Type u_1<VAR>L.Structure M<VAR>S : ι →o L.Substructure M<GOAL>(FirstOrder.Language.DirectLimit.liftInclusion S).toHom.range = ⨆ i, S i
<VAR>L : FirstOrder.Language<VAR>ι : Type v<VAR>Preorder ι<VAR>Nonempty ι<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>M : Type u_1<VAR>L.Structure M<VAR>S : ι →o L.Substructure M<VAR>i : ι<VAR>x : ↥(S i)<GOAL>(FirstOrder.Language.DirectLimit.Equiv_iSup S) ((FirstOrder.Language.DirectLimit.of L ι (fun x => ↥(S x)) (fun x x_1 h => FirstOrder.Language.Substructure.inclusion ⋯) i) x) = (FirstOrder.Language.Substructure.inclusion ⋯) x
<VAR>L : FirstOrder.Language<VAR>ι : Type v<VAR>Preorder ι<VAR>Nonempty ι<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>M : Type u_1<VAR>L.Structure M<VAR>S : ι →o L.Substructure M<VAR>i : ι<VAR>x : ↥(S i)<GOAL>(FirstOrder.Language.DirectLimit.Equiv_iSup S).symm ((FirstOrder.Language.Substructure.inclusion ⋯) x) = (FirstOrder.Language.DirectLimit.of L ι (fun x => ↥(S x)) (fun x x_1 h => FirstOrder.Language.Substructure.inclusion ⋯) i) x
<VAR>L : FirstOrder.Language<VAR>ι : Type v<VAR>Preorder ι<VAR>Nonempty ι<VAR>IsDirected ι fun x x_1 => x ≤ x_1<VAR>M : Type u_1<VAR>L.Structure M<VAR>S : ι →o L.Substructure M<VAR>i : ι<GOAL>(FirstOrder.Language.DirectLimit.Equiv_iSup S).symm.toEmbedding.comp (FirstOrder.Language.Substructure.inclusion ⋯) = FirstOrder.Language.DirectLimit.of L ι (fun x => ↥(S x)) (fun x x_1 h => FirstOrder.Language.Substructure.inclusion ⋯) i
<VAR>R : Type u_1<VAR>CommRing R<VAR>g : SL(2, R)<GOAL>IsCoprime (↑g 1 0) (↑g 1 1)
<VAR>R : Type u_1<VAR>CommRing R<GOAL>Set.SurjOn (fun g => ↑g 1) Set.univ {cd | IsCoprime (cd 0) (cd 1)}
<VAR>z : ℍ<GOAL>Filter.Tendsto (fun p => Complex.normSq (↑(p 0) * ↑z + ↑(p 1))) Filter.cofinite Filter.atTop
<VAR>p : Fin 2 → ℤ<VAR>g : Matrix (Fin 2) (Fin 2) ℝ<GOAL>(ModularGroup.lcRow0 p) g = ↑(p 0) * g 0 0 + ↑(p 1) * g 0 1
<VAR>cd : Fin 2 → ℤ<VAR>hcd : IsCoprime (cd 0) (cd 1)<VAR>f : (i : Fin 2) → (fun a => Fin 2 → ℝ) i<VAR>i : Fin 2<GOAL>∀ (a : Fin 2), (ModularGroup.lcRow0Extend hcd) f i a = (![(LinearMap.GeneralLinearGroup.generalLinearEquiv ℝ (Fin 2 → ℝ)) (Matrix.GeneralLinearGroup.toLinear (Matrix.planeConformalMatrix (↑(cd 0)) (-↑(cd 1)) ⋯)), LinearEquiv.refl ℝ (Fin 2 → ℝ)] i) (f i) a
<VAR>cd : Fin 2 → ℤ<VAR>hcd : IsCoprime (cd 0) (cd 1)<VAR>f : (i : Fin 2) → (fun a => Fin 2 → ℝ) i<VAR>i : Fin 2<GOAL>∀ (a : Fin 2), (ModularGroup.lcRow0Extend hcd).symm f i a = (![(LinearMap.GeneralLinearGroup.generalLinearEquiv ℝ (Fin 2 → ℝ)) (Matrix.GeneralLinearGroup.toLinear (Matrix.planeConformalMatrix (↑(cd 0)) (-↑(cd 1)) ⋯)), LinearEquiv.refl ℝ (Fin 2 → ℝ)] i).symm (f i) a
<VAR>cd : Fin 2 → ℤ<VAR>hcd : IsCoprime (cd 0) (cd 1)<GOAL>Filter.Tendsto (fun g => (ModularGroup.lcRow0 cd) ↑((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g)) Filter.cofinite (Filter.cocompact ℝ)
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>p : Fin 2 → ℤ<VAR>hp : IsCoprime (p 0) (p 1)<VAR>hg : ↑g 1 = p<GOAL>↑(g • z) = ↑((ModularGroup.lcRow0 p) ↑((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) / (↑(p 0) ^ 2 + ↑(p 1) ^ 2) + (↑(p 1) * ↑z - ↑(p 0)) / ((↑(p 0) ^ 2 + ↑(p 1) ^ 2) * (↑(p 0) * ↑z + ↑(p 1)))
<VAR>z : ℍ<VAR>p : Fin 2 → ℤ<VAR>hp : IsCoprime (p 0) (p 1)<GOAL>Filter.Tendsto (fun g => |(↑g • z).re|) Filter.cofinite Filter.atTop
<VAR>z : ℍ<GOAL>∃ g, ∀ (g' : SL(2, ℤ)), (g' • z).im ≤ (g • z).im
<VAR>z : ℍ<VAR>cd : Fin 2 → ℤ<VAR>hcd : IsCoprime (cd 0) (cd 1)<GOAL>∃ g, ↑g 1 = cd ∧ ∀ (g' : SL(2, ℤ)), ↑g 1 = ↑g' 1 → |(g • z).re| ≤ |(g' • z).re|
<VAR>z : ℍ<VAR>n : ℤ<GOAL>↑(ModularGroup.T ^ n • z) = ↑z + ↑n
<VAR>z : ℍ<VAR>n : ℤ<GOAL>(ModularGroup.T ^ n • z).re = z.re + ↑n
<VAR>z : ℍ<VAR>n : ℤ<GOAL>(ModularGroup.T ^ n • z).im = z.im
<VAR>z : ℍ<GOAL>(ModularGroup.T • z).re = z.re + 1
<VAR>z : ℍ<GOAL>(ModularGroup.T • z).im = z.im
<VAR>z : ℍ<GOAL>(ModularGroup.T⁻¹ • z).re = z.re - 1
<VAR>z : ℍ<GOAL>(ModularGroup.T⁻¹ • z).im = z.im
<VAR>g : SL(2, ℤ)<VAR>hc : ↑g 1 0 = 0<GOAL>∃ n, ∀ (z : ℍ), g • z = ModularGroup.T ^ n • z
<VAR>g : SL(2, ℤ)<VAR>hc : ↑g 1 0 = 1<GOAL>g = ModularGroup.T ^ ↑g 0 0 * ModularGroup.S * ModularGroup.T ^ ↑g 1 1
<VAR>z : ℍ<VAR>h : 1 < Complex.normSq ↑z<GOAL>Complex.normSq ↑(ModularGroup.S • z) < 1
<VAR>z : ℍ<VAR>h : Complex.normSq ↑z < 1<GOAL>z.im < (ModularGroup.S • z).im
<VAR>z : ℍ<VAR>h : z ∈ ModularGroup.fdo<GOAL>|2 * z.re| < 1
<VAR>z : ℍ<VAR>h : z ∈ ModularGroup.fdo<GOAL>3 < 4 * z.im ^ 2
<VAR>z : ℍ<VAR>hz : z ∈ ModularGroup.fdo<VAR>n : ℤ<GOAL>1 < Complex.normSq ↑(ModularGroup.T ^ n • z)
<VAR>z : ℍ<VAR>n : ℤ<VAR>hz : z ∈ ModularGroup.fdo<VAR>hg : ModularGroup.T ^ n • z ∈ ModularGroup.fdo<GOAL>n = 0
<VAR>z : ℍ<GOAL>∃ g, g • z ∈ ModularGroup.fd
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>hz : z ∈ ModularGroup.fdo<VAR>hg : g • z ∈ ModularGroup.fdo<GOAL>|↑g 1 0| ≤ 1
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>hz : z ∈ ModularGroup.fdo<VAR>hg : g • z ∈ ModularGroup.fdo<GOAL>↑g 1 0 = 0
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>hz : z ∈ ModularGroup.fdo<VAR>hg : g • z ∈ ModularGroup.fdo<GOAL>z = g • z
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G : MonCat<VAR>CategoryTheory.MonoidalCategory V<GOAL>(𝟙_ (Action V G)).V = 𝟙_ V
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G : MonCat<VAR>CategoryTheory.MonoidalCategory V<VAR>g : ↑G<GOAL>(𝟙_ (Action V G)).ρ g = 𝟙 (𝟙_ V)
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G : MonCat<VAR>CategoryTheory.MonoidalCategory V<VAR>X Y : Action V G<GOAL>(CategoryTheory.MonoidalCategory.tensorObj X Y).V = CategoryTheory.MonoidalCategory.tensorObj X.V Y.V
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G : MonCat<VAR>CategoryTheory.MonoidalCategory V<VAR>X Y : Action V G<VAR>g : ↑G<GOAL>(CategoryTheory.MonoidalCategory.tensorObj X Y).ρ g = CategoryTheory.MonoidalCategory.tensorHom (X.ρ g) (Y.ρ g)
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G : MonCat<VAR>CategoryTheory.MonoidalCategory V<VAR>W X Y Z : Action V G<VAR>f : W ⟶ X<VAR>g : Y ⟶ Z<GOAL>(CategoryTheory.MonoidalCategory.tensorHom f g).hom = CategoryTheory.MonoidalCategory.tensorHom f.hom g.hom
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G : MonCat<VAR>CategoryTheory.MonoidalCategory V<VAR>X : Action V G<VAR>Y Z : Action V G<VAR>f : Y ⟶ Z<GOAL>(CategoryTheory.MonoidalCategory.whiskerLeft X f).hom = CategoryTheory.MonoidalCategory.whiskerLeft X.V f.hom
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G : MonCat<VAR>CategoryTheory.MonoidalCategory V<VAR>X Y : Action V G<VAR>f : X ⟶ Y<VAR>Z : Action V G<GOAL>(CategoryTheory.MonoidalCategory.whiskerRight f Z).hom = CategoryTheory.MonoidalCategory.whiskerRight f.hom Z.V
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G : MonCat<VAR>CategoryTheory.MonoidalCategory V<VAR>X Y Z : Action V G<GOAL>(CategoryTheory.MonoidalCategory.associator X Y Z).hom.hom = (CategoryTheory.MonoidalCategory.associator X.V Y.V Z.V).hom
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G : MonCat<VAR>CategoryTheory.MonoidalCategory V<VAR>X Y Z : Action V G<GOAL>(CategoryTheory.MonoidalCategory.associator X Y Z).inv.hom = (CategoryTheory.MonoidalCategory.associator X.V Y.V Z.V).inv
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G : MonCat<VAR>CategoryTheory.MonoidalCategory V<VAR>X : Action V G<GOAL>(CategoryTheory.MonoidalCategory.leftUnitor X).hom.hom = (CategoryTheory.MonoidalCategory.leftUnitor X.V).hom
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G : MonCat<VAR>CategoryTheory.MonoidalCategory V<VAR>X : Action V G<GOAL>(CategoryTheory.MonoidalCategory.leftUnitor X).inv.hom = (CategoryTheory.MonoidalCategory.leftUnitor X.V).inv
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G : MonCat<VAR>CategoryTheory.MonoidalCategory V<VAR>X : Action V G<GOAL>(CategoryTheory.MonoidalCategory.rightUnitor X).hom.hom = (CategoryTheory.MonoidalCategory.rightUnitor X.V).hom
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G : MonCat<VAR>CategoryTheory.MonoidalCategory V<VAR>X : Action V G<GOAL>(CategoryTheory.MonoidalCategory.rightUnitor X).inv.hom = (CategoryTheory.MonoidalCategory.rightUnitor X.V).inv
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G : MonCat<VAR>CategoryTheory.MonoidalCategory V<GOAL>(Action.forgetMonoidal V G).ε = 𝟙 (𝟙_ V)
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G : MonCat<VAR>CategoryTheory.MonoidalCategory V<GOAL>(Action.forgetMonoidal V G).toFunctor = Action.forget V G
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G : MonCat<VAR>CategoryTheory.MonoidalCategory V<VAR>X Y : Action V G<GOAL>(Action.forgetMonoidal V G).μ X Y = 𝟙 (CategoryTheory.MonoidalCategory.tensorObj ((Action.forget V G).obj X) ((Action.forget V G).obj Y))
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G : MonCat<VAR>CategoryTheory.MonoidalCategory V<VAR>CategoryTheory.BraidedCategory V<GOAL>(Action.forgetBraided V G).ε = 𝟙 (𝟙_ V)
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G : MonCat<VAR>CategoryTheory.MonoidalCategory V<VAR>CategoryTheory.BraidedCategory V<GOAL>∀ {X Y : Action V G} (f : X ⟶ Y), (Action.forgetBraided V G).map f = f.hom
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G : MonCat<VAR>CategoryTheory.MonoidalCategory V<VAR>CategoryTheory.BraidedCategory V<VAR>X Y : Action V G<GOAL>(Action.forgetBraided V G).μ X Y = 𝟙 (CategoryTheory.MonoidalCategory.tensorObj X.V Y.V)
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G : MonCat<VAR>CategoryTheory.MonoidalCategory V<VAR>CategoryTheory.BraidedCategory V<VAR>M : Action V G<GOAL>(Action.forgetBraided V G).obj M = M.V
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G : MonCat<VAR>CategoryTheory.MonoidalCategory V<VAR>A B : Action V G<GOAL>((Action.functorCategoryMonoidalEquivalence V G).μ A B).app PUnit.unit = 𝟙 ((CategoryTheory.MonoidalCategory.tensorObj ((Action.functorCategoryMonoidalEquivalence V G).obj A) ((Action.functorCategoryMonoidalEquivalence V G).obj B)).obj PUnit.unit)
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G : MonCat<VAR>CategoryTheory.MonoidalCategory V<VAR>A B : Action V G<GOAL>((Action.functorCategoryMonoidalEquivalence V G).μIso A B).inv.app PUnit.unit = 𝟙 (((Action.functorCategoryMonoidalEquivalence V G).obj (CategoryTheory.MonoidalCategory.tensorObj A B)).obj PUnit.unit)
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G : MonCat<VAR>CategoryTheory.MonoidalCategory V<GOAL>(Action.functorCategoryMonoidalEquivalence V G).ε.app PUnit.unit = 𝟙 ((𝟙_ (CategoryTheory.SingleObj ↑G ⥤ V)).obj PUnit.unit)
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G : MonCat<VAR>CategoryTheory.MonoidalCategory V<VAR>A : Action V G<GOAL>((Action.functorCategoryMonoidalAdjunction V G).unit.app A).hom = 𝟙 ((𝟭 (Action V G)).obj A).V
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G : MonCat<VAR>CategoryTheory.MonoidalCategory V<VAR>A : CategoryTheory.SingleObj ↑G ⥤ V<GOAL>((Action.functorCategoryMonoidalAdjunction V G).counit.app A).app PUnit.unit = 𝟙 ((((Action.functorCategoryMonoidalEquivalenceInverse V G).toFunctor ⋙ (Action.functorCategoryMonoidalEquivalence V G).toFunctor).obj A).obj PUnit.unit)
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G : MonCat<VAR>CategoryTheory.MonoidalCategory V<VAR>A B : Action V G<VAR>f : A ⟶ B<GOAL>(Action.functorCategoryMonoidalEquivalence V G).map f = Action.FunctorCategoryEquivalence.functor.map f
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>G : MonCat<VAR>CategoryTheory.MonoidalCategory V<VAR>A B : CategoryTheory.SingleObj ↑G ⥤ V<VAR>f : A ⟶ B<GOAL>(Action.functorCategoryMonoidalEquivalenceInverse V G).map f = Action.FunctorCategoryEquivalence.inverse.map f
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>CategoryTheory.MonoidalCategory V<VAR>H : Grp<VAR>X : Action V ((CategoryTheory.forget₂ Grp MonCat).obj H)<VAR>CategoryTheory.RightRigidCategory V<GOAL>Xᘁ.V = X.Vᘁ
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>CategoryTheory.MonoidalCategory V<VAR>H : Grp<VAR>X : Action V ((CategoryTheory.forget₂ Grp MonCat).obj H)<VAR>CategoryTheory.LeftRigidCategory V<GOAL>(ᘁX).V = ᘁX.V
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>CategoryTheory.MonoidalCategory V<VAR>H : Grp<VAR>X : Action V ((CategoryTheory.forget₂ Grp MonCat).obj H)<VAR>CategoryTheory.RightRigidCategory V<VAR>h : ↑H<GOAL>Xᘁ.ρ h = X.ρ h⁻¹ᘁ
<VAR>V : Type (u + 1)<VAR>CategoryTheory.LargeCategory V<VAR>CategoryTheory.MonoidalCategory V<VAR>H : Grp<VAR>X : Action V ((CategoryTheory.forget₂ Grp MonCat).obj H)<VAR>CategoryTheory.LeftRigidCategory V<VAR>h : ↑H<GOAL>(ᘁX).ρ h = ᘁX.ρ h⁻¹
<VAR>G : Type u<VAR>Group G<VAR>X : Action (Type u) (MonCat.of G)<VAR>g : (CategoryTheory.MonoidalCategory.tensorObj (Action.leftRegular G) X).V<GOAL>(Action.leftRegularTensorIso G X).hom.hom g = (g.1, X.ρ g.1⁻¹ g.2)
<VAR>G : Type u<VAR>Group G<VAR>X : Action (Type u) (MonCat.of G)<VAR>g : (CategoryTheory.MonoidalCategory.tensorObj (Action.leftRegular G) { V := X.V, ρ := 1 }).V<GOAL>(Action.leftRegularTensorIso G X).inv.hom g = (g.1, X.ρ g.1 g.2)