ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>inst✝³⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³⁶ : NormedAddCommGroup E<VAR>inst✝³⁵ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝³⁴ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝³³ : TopologicalSpace M<VAR>inst✝³² : ChartedSpace H M<VAR>inst✝³¹ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝³⁰ : NormedAddCommGroup E'<VAR>inst✝²⁹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝²⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝²⁷ : TopologicalSpace M'<VAR>inst✝²⁶ : ChartedSpace H' M'<VAR>inst✝²⁵ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝²² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝²¹ : TopologicalSpace M''<VAR>inst✝²⁰ : ChartedSpace H'' M''<VAR>F : Type u_11<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f✝ f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<VAR>f : M → M'<VAR>g : M → N'<VAR>hf : ContinuousWithinAt f s x ∧ ContDiffWithinAt 𝕜 n (↑(extChartAt I' (f x)) ∘ f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x)<VAR>hg : ContinuousWithinAt g s x ∧ ContDiffWithinAt 𝕜 n (↑(extChartAt J' (g x)) ∘ g ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x)<GOAL>ContinuousWithinAt (fun x => (f x, g x)) s x ∧ ContDiffWithinAt 𝕜 n (↑(extChartAt (I'.prod J') (f x, g x)) ∘ (fun x => (f x, g x)) ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x)
<VAR>θ : Angle<GOAL>0 < θ.cos ↔ |θ.toReal| < π / 2
<VAR>θ : Angle<GOAL>|θ.toReal| ≤ π / 2 → (|θ.toReal| ≠ π / 2 ↔ 0 ≠ θ.cos)
<VAR>θ : Angle<GOAL>|θ.toReal| ≠ π / 2 ↔ 0 ≠ θ.cos
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.46503, u_1} C<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>G : C ⥤ D<VAR>A : Type w<VAR>inst✝² : Category.{w', w} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>inst✝¹ : G.IsCocontinuous J K<VAR>inst✝ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F<VAR>F : Cᵒᵖ ⥤ A<VAR>hF : Presheaf.IsSheaf J F<VAR>R : Dᵒᵖ ⥤ A<VAR>α : G.op ⋙ R ⟶ F<VAR>hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension<VAR>X : D<VAR>S : K.Cover X<VAR>s : Multifork (S.index R)<VAR>W : A<VAR>f g : W ⟶ R.obj (op X)<VAR>h : ∀ (i : S.Arrow), f ≫ R.map i.f.op = g ≫ R.map i.f.op<GOAL>f = g
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.46503, u_1} C<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>G : C ⥤ D<VAR>A : Type w<VAR>inst✝² : Category.{w', w} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>inst✝¹ : G.IsCocontinuous J K<VAR>inst✝ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F<VAR>F : Cᵒᵖ ⥤ A<VAR>hF : Presheaf.IsSheaf J F<VAR>R : Dᵒᵖ ⥤ A<VAR>α : G.op ⋙ R ⟶ F<VAR>hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension<VAR>X : D<VAR>S : K.Cover X<VAR>s : Multifork (S.index R)<VAR>W : A<VAR>f g : W ⟶ R.obj (op X)<VAR>h : ∀ (i : S.Arrow), f ≫ R.map i.f.op = g ≫ R.map i.f.op<GOAL>∀ (j : StructuredArrow (op X) G.op), f ≫ ((Functor.RightExtension.mk R α).coneAt (op X)).π.app j = g ≫ ((Functor.RightExtension.mk R α).coneAt (op X)).π.app j
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.46503, u_1} C<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>G : C ⥤ D<VAR>A : Type w<VAR>inst✝² : Category.{w', w} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>inst✝¹ : G.IsCocontinuous J K<VAR>inst✝ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F<VAR>F : Cᵒᵖ ⥤ A<VAR>hF : Presheaf.IsSheaf J F<VAR>R : Dᵒᵖ ⥤ A<VAR>α : G.op ⋙ R ⟶ F<VAR>hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension<VAR>X : D<VAR>S : K.Cover X<VAR>s : Multifork (S.index R)<VAR>W : A<VAR>f g : W ⟶ R.obj (op X)<VAR>h : ∀ (i : S.Arrow), f ≫ R.map i.f.op = g ≫ R.map i.f.op<VAR>j : StructuredArrow (op X) G.op<GOAL>f ≫ ((Functor.RightExtension.mk R α).coneAt (op X)).π.app j = g ≫ ((Functor.RightExtension.mk R α).coneAt (op X)).π.app j
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.46503, u_1} C<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>G : C ⥤ D<VAR>A : Type w<VAR>inst✝² : Category.{w', w} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>inst✝¹ : G.IsCocontinuous J K<VAR>inst✝ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F<VAR>F : Cᵒᵖ ⥤ A<VAR>hF : Presheaf.IsSheaf J F<VAR>R : Dᵒᵖ ⥤ A<VAR>α : G.op ⋙ R ⟶ F<VAR>hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension<VAR>X : D<VAR>S : K.Cover X<VAR>s : Multifork (S.index R)<VAR>W : A<VAR>f g : W ⟶ R.obj (op X)<VAR>h : ∀ (i : S.Arrow), f ≫ R.map i.f.op = g ≫ R.map i.f.op<VAR>j : StructuredArrow (op X) G.op<GOAL>∀ (I : GrothendieckTopology.Cover.Arrow ⟨Sieve.functorPullback G (Sieve.pullback j.hom.unop ↑S), ⋯⟩), (f ≫ ((Functor.RightExtension.mk R α).coneAt (op X)).π.app j) ≫ F.map I.f.op = (g ≫ ((Functor.RightExtension.mk R α).coneAt (op X)).π.app j) ≫ F.map I.f.op
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.46503, u_1} C<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>G : C ⥤ D<VAR>A : Type w<VAR>inst✝² : Category.{w', w} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>inst✝¹ : G.IsCocontinuous J K<VAR>inst✝ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F<VAR>F : Cᵒᵖ ⥤ A<VAR>hF : Presheaf.IsSheaf J F<VAR>R : Dᵒᵖ ⥤ A<VAR>α : G.op ⋙ R ⟶ F<VAR>hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension<VAR>X : D<VAR>S : K.Cover X<VAR>s : Multifork (S.index R)<VAR>W✝ : A<VAR>f g : W✝ ⟶ R.obj (op X)<VAR>h : ∀ (i : S.Arrow), f ≫ R.map i.f.op = g ≫ R.map i.f.op<VAR>j : StructuredArrow (op X) G.op<VAR>W : C<VAR>i : W ⟶ unop j.right<VAR>hi : (GrothendieckTopology.Cover.sieve ⟨Sieve.functorPullback G (Sieve.pullback j.hom.unop ↑S), ⋯⟩).arrows i<VAR>eq : f ≫ R.map (j.hom ≫ (G.map i).op) = g ≫ R.map (j.hom ≫ (G.map i).op)<GOAL>(f ≫ R.map j.hom ≫ α.app j.right) ≫ F.map i.op = (g ≫ R.map j.hom ≫ α.app j.right) ≫ F.map i.op
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{?u.46503, u_1} C<VAR>inst✝³ : Category.{u_3, u_2} D<VAR>G : C ⥤ D<VAR>A : Type w<VAR>inst✝² : Category.{w', w} A<VAR>J : GrothendieckTopology C<VAR>K : GrothendieckTopology D<VAR>inst✝¹ : G.IsCocontinuous J K<VAR>inst✝ : ∀ (F : Cᵒᵖ ⥤ A), G.op.HasPointwiseRightKanExtension F<VAR>F : Cᵒᵖ ⥤ A<VAR>hF : Presheaf.IsSheaf J F<VAR>R : Dᵒᵖ ⥤ A<VAR>α : G.op ⋙ R ⟶ F<VAR>hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension<VAR>X : D<VAR>S : K.Cover X<VAR>s : Multifork (S.index R)<VAR>W✝ : A<VAR>f g : W✝ ⟶ R.obj (op X)<VAR>h : ∀ (i : S.Arrow), f ≫ R.map i.f.op = g ≫ R.map i.f.op<VAR>j : StructuredArrow (op X) G.op<VAR>W : C<VAR>i : W ⟶ unop j.right<VAR>hi : (GrothendieckTopology.Cover.sieve ⟨Sieve.functorPullback G (Sieve.pullback j.hom.unop ↑S), ⋯⟩).arrows i<VAR>eq : f ≫ R.map (j.hom ≫ (G.map i).op) = g ≫ R.map (j.hom ≫ (G.map i).op)<GOAL>f ≫ R.map (j.hom ≫ (G.map i).op) ≫ α.app (op W) = g ≫ R.map (j.hom ≫ (G.map i).op) ≫ α.app (op W)
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<GOAL>toIcoMod hp a (-b) = p - toIocMod hp (-a) b
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<GOAL>-b - -(toIocDiv hp (-a) b • p + 1 • p) = p - (b - toIocDiv hp (-a) b • p)
<VAR>α : Type u_1<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s k : Set α<VAR>hs : μ.IsEverywherePos s<VAR>h : ∀ x ∈ s, ∃ t ∈ 𝓝 x, ∀ u ⊆ t, ν u = μ u<VAR>x : α<VAR>hx : x ∈ s<VAR>n : Set α<VAR>hn : n ∈ 𝓝[s] x<VAR>t : Set α<VAR>t_mem : t ∈ 𝓝 x<VAR>ht : ∀ u ⊆ t, ν u = μ u<GOAL>0 < ν n
<VAR>α : Type u_1<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s k : Set α<VAR>hs : μ.IsEverywherePos s<VAR>h : ∀ x ∈ s, ∃ t ∈ 𝓝 x, ∀ u ⊆ t, ν u = μ u<VAR>x : α<VAR>hx : x ∈ s<VAR>n : Set α<VAR>hn : n ∈ 𝓝[s] x<VAR>t : Set α<VAR>t_mem : t ∈ 𝓝 x<VAR>ht : ∀ u ⊆ t, ν u = μ u<GOAL>0 < ν (n ∩ t)
<VAR>α : Type u_1<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s k : Set α<VAR>hs : μ.IsEverywherePos s<VAR>h : ∀ x ∈ s, ∃ t ∈ 𝓝 x, ∀ u ⊆ t, ν u = μ u<VAR>x : α<VAR>hx : x ∈ s<VAR>n : Set α<VAR>hn : n ∈ 𝓝[s] x<VAR>t : Set α<VAR>t_mem : t ∈ 𝓝 x<VAR>ht : ∀ u ⊆ t, ν u = μ u<GOAL>0 < μ (n ∩ t)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemifield α<VAR>inst✝ : LinearOrderedSemifield β<VAR>s : Set ι<VAR>f f₁ f₂ : ι → α<VAR>g g₁ g₂ : ι → β<VAR>hf : ∀ i ∈ s, 0 < f i<VAR>hg : ∀ i ∈ s, 0 < g i<GOAL>MonovaryOn f⁻¹ g⁻¹ s ↔ MonovaryOn f g s
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>p✝ : Perm α<VAR>x✝ : α<VAR>p : Perm α<VAR>x y : α<VAR>hy : y ∈ p.toList x<GOAL>(p.toList x).next y hy = p y
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>p✝ : Perm α<VAR>x✝ : α<VAR>p : Perm α<VAR>x y : α<VAR>hy✝ : y ∈ p.toList x<VAR>hy : p.SameCycle x y ∧ x ∈ p.support<GOAL>(p.toList x).next y hy✝ = p y
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>p✝ : Perm α<VAR>x✝ : α<VAR>p : Perm α<VAR>x y : α<VAR>hy✝ : y ∈ p.toList x<VAR>hy : p.SameCycle x y ∧ x ∈ p.support<VAR>k : ℕ<VAR>hk : k < (p.cycleOf x).support.card<VAR>hk' : (p ^ k) x = y<GOAL>(p.toList x).next y hy✝ = p y
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>p✝ : Perm α<VAR>x✝ : α<VAR>p : Perm α<VAR>x y : α<VAR>hy✝ : y ∈ p.toList x<VAR>hy : p.SameCycle x y ∧ x ∈ p.support<VAR>k : ℕ<VAR>hk : k < (p.cycleOf x).support.card<VAR>hk' : (p.toList x).nthLe k ⋯ = y<GOAL>(p.toList x).next y hy✝ = p y
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>p✝ : Perm α<VAR>x✝ : α<VAR>p : Perm α<VAR>x y : α<VAR>hy✝ : y ∈ p.toList x<VAR>hy : p.SameCycle x y ∧ x ∈ p.support<VAR>k : ℕ<VAR>hk : k < (p.cycleOf x).support.card<VAR>hk' : (p.toList x).nthLe k ⋯ = y<GOAL>(p.toList x).next ((p.toList x).nthLe k ⋯) ⋯ = p ((p.toList x).nthLe k ⋯)
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>p✝ : Perm α<VAR>x✝ : α<VAR>p : Perm α<VAR>x y : α<VAR>hy✝ : y ∈ p.toList x<VAR>hy : p.SameCycle x y ∧ x ∈ p.support<VAR>k : ℕ<VAR>hk : k < (p.cycleOf x).support.card<VAR>hk' : (p.toList x).nthLe k ⋯ = y<GOAL>(p.cycleOf x).IsCycle
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : MulZeroClass α<VAR>a b : WithBot α<VAR>a✝¹ : α<VAR>ha : ¬↑a✝¹ = 0<VAR>a✝ : α<VAR>hb : ¬↑a✝ = 0<GOAL>unbot' 0 (↑a✝¹ * ↑a✝) = unbot' 0 ↑a✝¹ * unbot' 0 ↑a✝
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>m : MeasurableSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : T2Space Y<VAR>μ ν : Measure X<VAR>inst✝ : μ.IsOpenPosMeasure<VAR>s U F : Set X<VAR>x : X<VAR>f g : X → Y<VAR>h : f =ᶠ[ae (μ.restrict U)] g<VAR>hU : IsOpen U<VAR>hf : ContinuousOn f U<VAR>hg : ContinuousOn g U<GOAL>EqOn f g U
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>m : MeasurableSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : T2Space Y<VAR>μ ν : Measure X<VAR>inst✝ : μ.IsOpenPosMeasure<VAR>s U F : Set X<VAR>x : X<VAR>f g : X → Y<VAR>hU : IsOpen U<VAR>hf : ContinuousOn f U<VAR>hg : ContinuousOn g U<VAR>h : ∀ᵐ (x : X) ∂μ, x ∈ U → f x = g x<GOAL>EqOn f g U
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>m : MeasurableSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : T2Space Y<VAR>μ ν : Measure X<VAR>inst✝ : μ.IsOpenPosMeasure<VAR>s U F : Set X<VAR>x : X<VAR>f g : X → Y<VAR>hU : IsOpen U<VAR>hf : ContinuousOn f U<VAR>hg : ContinuousOn g U<VAR>h : μ {a | a ∈ U ∧ ¬f a = g a} = 0<GOAL>EqOn f g U
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>m : MeasurableSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : T2Space Y<VAR>μ ν : Measure X<VAR>inst✝ : μ.IsOpenPosMeasure<VAR>s U F : Set X<VAR>x : X<VAR>f g : X → Y<VAR>hU : IsOpen U<VAR>hf : ContinuousOn f U<VAR>hg : ContinuousOn g U<VAR>h : μ {a | a ∈ U ∧ ¬f a = g a} = 0<VAR>this : IsOpen (U ∩ {a | f a ≠ g a})<GOAL>EqOn f g U
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>m : MeasurableSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : T2Space Y<VAR>μ ν : Measure X<VAR>inst✝ : μ.IsOpenPosMeasure<VAR>s U F : Set X<VAR>x : X<VAR>f g : X → Y<VAR>hU : IsOpen U<VAR>hf : ContinuousOn f U<VAR>hg : ContinuousOn g U<VAR>h : μ {a | a ∈ U ∧ ¬f a = g a} = 0<VAR>this : U ∩ {a | f a ≠ g a} ≤ ∅<GOAL>EqOn f g U
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k✝ : ℤ<VAR>f✝ : ℍ → ℂ<VAR>k : ℤ<VAR>A B : ↥GL(2, ℝ)⁺<VAR>f : ℍ → ℂ<VAR>x : ℍ<GOAL>(f ∣[k](A * B)) x = ((f ∣[k]A) ∣[k]B) x
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k✝ : ℤ<VAR>f✝ : ℍ → ℂ<VAR>k : ℤ<VAR>A B : ↥GL(2, ℝ)⁺<VAR>f : ℍ → ℂ<VAR>x : ℍ<GOAL>f ((A * B) • x) * ↑(↑↑(A * B)).det ^ (k - 1) * (denom A (smulAux B x) * denom B x) ^ (-k) = f (A • B • x) * ↑(↑↑A).det ^ (k - 1) * denom A (B • x) ^ (-k) * ↑(↑↑B).det ^ (k - 1) * denom B x ^ (-k)
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k✝ : ℤ<VAR>f✝ : ℍ → ℂ<VAR>k : ℤ<VAR>A B : ↥GL(2, ℝ)⁺<VAR>f : ℍ → ℂ<VAR>x : ℍ<VAR>e3 : (A * B) • x = A • B • x<GOAL>f ((A * B) • x) * ↑(↑↑(A * B)).det ^ (k - 1) * (denom A (smulAux B x) * denom B x) ^ (-k) = f (A • B • x) * ↑(↑↑A).det ^ (k - 1) * denom A (B • x) ^ (-k) * ↑(↑↑B).det ^ (k - 1) * denom B x ^ (-k)
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k✝ : ℤ<VAR>f✝ : ℍ → ℂ<VAR>k : ℤ<VAR>A B : ↥GL(2, ℝ)⁺<VAR>f : ℍ → ℂ<VAR>x : ℍ<VAR>e3 : (A * B) • x = A • B • x<GOAL>f (A • B • x) * ↑(↑↑(A * B)).det ^ (k - 1) * (denom A (smulAux B x) * denom B x) ^ (-k) = f (A • B • x) * ↑(↑↑A).det ^ (k - 1) * denom A (B • x) ^ (-k) * ↑(↑↑B).det ^ (k - 1) * denom B x ^ (-k)
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k✝ : ℤ<VAR>f✝ : ℍ → ℂ<VAR>k : ℤ<VAR>A B : ↥GL(2, ℝ)⁺<VAR>f : ℍ → ℂ<VAR>x : ℍ<VAR>e3 : (A * B) • x = A • B • x<GOAL>f (A • B • x) * (↑(↑↑A).det * ↑(↑↑B).det) ^ (k - 1) * ((↑(↑↑A 1 0) * ((↑(↑↑B 0 0) * ↑x + ↑(↑↑B 0 1)) / (↑(↑↑B 1 0) * ↑x + ↑(↑↑B 1 1))) + ↑(↑↑A 1 1)) * (↑(↑↑B 1 0) * ↑x + ↑(↑↑B 1 1))) ^ (-k) = f (A • B • x) * ↑(↑↑A).det ^ (k - 1) * (↑(↑↑A 1 0) * ((↑(↑↑B 0 0) * ↑x + ↑(↑↑B 0 1)) / (↑(↑↑B 1 0) * ↑x + ↑(↑↑B 1 1))) + ↑(↑↑A 1 1)) ^ (-k) * ↑(↑↑B).det ^ (k - 1) * (↑(↑↑B 1 0) * ↑x + ↑(↑↑B 1 1)) ^ (-k)
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k✝ : ℤ<VAR>f✝ : ℍ → ℂ<VAR>k : ℤ<VAR>A B : ↥GL(2, ℝ)⁺<VAR>f : ℍ → ℂ<VAR>x : ℍ<VAR>e3 : (A * B) • x = A • B • x<GOAL>f (A • B • x) * (↑(↑↑A).det * ↑(↑↑B).det) ^ (k - 1) / ((↑(↑↑A 1 0) * (↑(↑↑B 0 0) * ↑x + ↑(↑↑B 0 1)) / (↑(↑↑B 1 0) * ↑x + ↑(↑↑B 1 1)) + ↑(↑↑A 1 1)) * (↑(↑↑B 1 0) * ↑x + ↑(↑↑B 1 1))) ^ k = f (A • B • x) * ↑(↑↑A).det ^ (k - 1) * ↑(↑↑B).det ^ (k - 1) / ((↑(↑↑A 1 0) * (↑(↑↑B 0 0) * ↑x + ↑(↑↑B 0 1)) / (↑(↑↑B 1 0) * ↑x + ↑(↑↑B 1 1)) + ↑(↑↑A 1 1)) ^ k * (↑(↑↑B 1 0) * ↑x + ↑(↑↑B 1 1)) ^ k)
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k✝ : ℤ<VAR>f✝ : ℍ → ℂ<VAR>k : ℤ<VAR>A B : ↥GL(2, ℝ)⁺<VAR>f : ℍ → ℂ<VAR>x : ℍ<VAR>e3 : (A * B) • x = A • B • x<VAR>this : (↑(↑↑A).det * ↑(↑↑B).det) ^ (k - 1) = ↑(↑↑A).det ^ (k - 1) * ↑(↑↑B).det ^ (k - 1)<GOAL>f (A • B • x) * (↑(↑↑A).det * ↑(↑↑B).det) ^ (k - 1) / ((↑(↑↑A 1 0) * (↑(↑↑B 0 0) * ↑x + ↑(↑↑B 0 1)) / (↑(↑↑B 1 0) * ↑x + ↑(↑↑B 1 1)) + ↑(↑↑A 1 1)) * (↑(↑↑B 1 0) * ↑x + ↑(↑↑B 1 1))) ^ k = f (A • B • x) * ↑(↑↑A).det ^ (k - 1) * ↑(↑↑B).det ^ (k - 1) / ((↑(↑↑A 1 0) * (↑(↑↑B 0 0) * ↑x + ↑(↑↑B 0 1)) / (↑(↑↑B 1 0) * ↑x + ↑(↑↑B 1 1)) + ↑(↑↑A 1 1)) ^ k * (↑(↑↑B 1 0) * ↑x + ↑(↑↑B 1 1)) ^ k)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>M₁ : Type u_4<VAR>M₂ : Type u_5<VAR>N : Type u_6<VAR>inst✝⁷ : Monoid R<VAR>inst✝⁶ : Monoid S<VAR>σ : R → S<VAR>inst✝⁵ : MulAction R M<VAR>inst✝⁴ : MulAction S N<VAR>inst✝³ : MulAction R M₁<VAR>inst✝² : MulAction R M₂<VAR>F : Type u_7<VAR>h : F<VAR>inst✝¹ : FunLike F M N<VAR>inst✝ : MulActionSemiHomClass F σ M N<VAR>c : R<VAR>s : Set M<VAR>t : Set N<VAR>y : M<VAR>hy : y ∈ ⇑h ⁻¹' t<GOAL>(fun x => c • x) y ∈ ⇑h ⁻¹' (σ c • t)
<VAR>α : Type u<VAR>β : Type v<VAR>S : WSeq (Computation α)<VAR>h : S.head ~> none<VAR>x✝ : (parallel S).Terminates<VAR>a : α<VAR>m : a ∈ parallel S<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>S : WSeq (Computation α)<VAR>h : S.head ~> none<VAR>x✝ : (parallel S).Terminates<VAR>a : α<VAR>m : a ∈ parallel S<VAR>c : Computation α<VAR>cs : c ∈ S<VAR>right✝ : a ∈ c<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>S : WSeq (Computation α)<VAR>h : S.head ~> none<VAR>x✝ : (parallel S).Terminates<VAR>a : α<VAR>m : a ∈ parallel S<VAR>c : Computation α<VAR>cs : c ∈ S<VAR>right✝ : a ∈ c<VAR>n : ℕ<VAR>nm : some c ∈ S.get? n<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>S : WSeq (Computation α)<VAR>h : S.head ~> none<VAR>x✝ : (parallel S).Terminates<VAR>a : α<VAR>m : a ∈ parallel S<VAR>c : Computation α<VAR>cs : c ∈ S<VAR>right✝ : a ∈ c<VAR>n : ℕ<VAR>nm : some c ∈ S.get? n<VAR>c' : Computation α<VAR>h' : some c' ∈ S.head<GOAL>False
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f✝ f₀ f₁ g : E → F<VAR>f'✝ f₀' f₁' g' e : E →L[𝕜] F<VAR>x✝ : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>iso : E ≃L[𝕜] F<VAR>f : F → G<VAR>x : E<VAR>f' : E →L[𝕜] G<GOAL>HasFDerivAt (f ∘ ⇑iso) f' x ↔ HasFDerivAt f (f'.comp ↑iso.symm) (iso x)
<VAR>n m p : ℕ<VAR>pp : 1 < p<VAR>h : 1 = 1 ∨ m ≤ minFac 1<VAR>d : p ∣ 1<GOAL>m ≤ p
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>A : Subalgebra ℝ C(X, ℝ)<VAR>w : A.SeparatesPoints<GOAL>A.topologicalClosure = ⊤
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>A : Subalgebra ℝ C(X, ℝ)<VAR>w : A.SeparatesPoints<GOAL>↑A.topologicalClosure = ↑⊤
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>A : Subalgebra ℝ C(X, ℝ)<VAR>w : A.SeparatesPoints<VAR>L : Subalgebra ℝ C(X, ℝ) := A.topologicalClosure<GOAL>↑A.topologicalClosure = ↑⊤
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>A : Subalgebra ℝ C(X, ℝ)<VAR>w : A.SeparatesPoints<VAR>L : Subalgebra ℝ C(X, ℝ) := A.topologicalClosure<VAR>n : (↑L).Nonempty<GOAL>↑A.topologicalClosure = ↑⊤
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>A : Subalgebra ℝ C(X, ℝ)<VAR>w : A.SeparatesPoints<VAR>L : Subalgebra ℝ C(X, ℝ) := A.topologicalClosure<VAR>n : (↑L).Nonempty<GOAL>↑A.topologicalClosure = closure ↑L
<VAR>m₁ : List Char<VAR>c : Char<VAR>m₂ : List Char<VAR>x✝ : Substring<VAR>h : x✝.Valid<VAR>e : x✝.toString.data = m₁ ++ c :: m₂<GOAL>x✝.get { byteIdx := utf8Len m₁ } = c
<VAR>m₁ : List Char<VAR>c : Char<VAR>m₂ : List Char<VAR>x✝ : Substring<VAR>h✝ : x✝.Valid<VAR>e : x✝.toString.data = m₁ ++ c :: m₂<VAR>l m r : List Char<VAR>h : ValidFor l m r x✝<GOAL>x✝.get { byteIdx := utf8Len m₁ } = c
<VAR>m₁ : List Char<VAR>c : Char<VAR>m₂ : List Char<VAR>x✝ : Substring<VAR>h✝ : x✝.Valid<VAR>l m r : List Char<VAR>h : ValidFor l m r x✝<VAR>e : m = m₁ ++ c :: m₂<GOAL>x✝.get { byteIdx := utf8Len m₁ } = c
<VAR>m₁ : List Char<VAR>c : Char<VAR>m₂ : List Char<VAR>x✝ : Substring<VAR>h✝ : x✝.Valid<VAR>l r : List Char<VAR>h : ValidFor l (m₁ ++ c :: m₂) r x✝<GOAL>x✝.get { byteIdx := utf8Len m₁ } = c
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₁' : Type u_9<VAR>M₂' : Type u_10<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>ι : Type u_16<VAR>inst✝¹¹ : Semiring R₁<VAR>inst✝¹⁰ : Semiring S₁<VAR>inst✝⁹ : Semiring R₂<VAR>inst✝⁸ : Semiring S₂<VAR>inst✝⁷ : AddCommMonoid N₂<VAR>inst✝⁶ : Module S₁ N₂<VAR>inst✝⁵ : Module S₂ N₂<VAR>inst✝⁴ : SMulCommClass S₂ S₁ N₂<VAR>inst✝³ : Fintype n<VAR>inst✝² : Fintype m<VAR>σ₁ : R₁ →+* S₁<VAR>σ₂ : R₂ →+* S₂<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : DecidableEq m<VAR>f : Matrix n m N₂<VAR>i : n<VAR>j : m<GOAL>((toLinearMap₂'Aux σ₁ σ₂ f) ((LinearMap.stdBasis R₁ (fun x => R₁) i) 1)) ((LinearMap.stdBasis R₂ (fun x => R₂) j) 1) = f i j
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₁' : Type u_9<VAR>M₂' : Type u_10<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>ι : Type u_16<VAR>inst✝¹¹ : Semiring R₁<VAR>inst✝¹⁰ : Semiring S₁<VAR>inst✝⁹ : Semiring R₂<VAR>inst✝⁸ : Semiring S₂<VAR>inst✝⁷ : AddCommMonoid N₂<VAR>inst✝⁶ : Module S₁ N₂<VAR>inst✝⁵ : Module S₂ N₂<VAR>inst✝⁴ : SMulCommClass S₂ S₁ N₂<VAR>inst✝³ : Fintype n<VAR>inst✝² : Fintype m<VAR>σ₁ : R₁ →+* S₁<VAR>σ₂ : R₂ →+* S₂<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : DecidableEq m<VAR>f : Matrix n m N₂<VAR>i : n<VAR>j : m<GOAL>∑ i_1 : n, ∑ j_1 : m, σ₂ ((LinearMap.stdBasis R₂ (fun x => R₂) j) 1 j_1) •> σ₁ ((LinearMap.stdBasis R₁ (fun x => R₁) i) 1 i_1) •> f i_1 j_1 = f i j
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₁' : Type u_9<VAR>M₂' : Type u_10<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>ι : Type u_16<VAR>inst✝¹¹ : Semiring R₁<VAR>inst✝¹⁰ : Semiring S₁<VAR>inst✝⁹ : Semiring R₂<VAR>inst✝⁸ : Semiring S₂<VAR>inst✝⁷ : AddCommMonoid N₂<VAR>inst✝⁶ : Module S₁ N₂<VAR>inst✝⁵ : Module S₂ N₂<VAR>inst✝⁴ : SMulCommClass S₂ S₁ N₂<VAR>inst✝³ : Fintype n<VAR>inst✝² : Fintype m<VAR>σ₁ : R₁ →+* S₁<VAR>σ₂ : R₂ →+* S₂<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : DecidableEq m<VAR>f : Matrix n m N₂<VAR>i : n<VAR>j : m<VAR>this : ∑ i' : n, ∑ j' : m, (if i = i' then 1 else 0) •> (if j = j' then 1 else 0) •> f i' j' = f i j<GOAL>∑ i_1 : n, ∑ j_1 : m, σ₂ ((LinearMap.stdBasis R₂ (fun x => R₂) j) 1 j_1) •> σ₁ ((LinearMap.stdBasis R₁ (fun x => R₁) i) 1 i_1) •> f i_1 j_1 = f i j
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₁' : Type u_9<VAR>M₂' : Type u_10<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>ι : Type u_16<VAR>inst✝¹¹ : Semiring R₁<VAR>inst✝¹⁰ : Semiring S₁<VAR>inst✝⁹ : Semiring R₂<VAR>inst✝⁸ : Semiring S₂<VAR>inst✝⁷ : AddCommMonoid N₂<VAR>inst✝⁶ : Module S₁ N₂<VAR>inst✝⁵ : Module S₂ N₂<VAR>inst✝⁴ : SMulCommClass S₂ S₁ N₂<VAR>inst✝³ : Fintype n<VAR>inst✝² : Fintype m<VAR>σ₁ : R₁ →+* S₁<VAR>σ₂ : R₂ →+* S₂<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : DecidableEq m<VAR>f : Matrix n m N₂<VAR>i : n<VAR>j : m<VAR>this : ∑ i' : n, ∑ j' : m, (if i = i' then 1 else 0) •> (if j = j' then 1 else 0) •> f i' j' = f i j<GOAL>∑ i_1 : n, ∑ j_1 : m, σ₂ ((LinearMap.stdBasis R₂ (fun x => R₂) j) 1 j_1) •> σ₁ ((LinearMap.stdBasis R₁ (fun x => R₁) i) 1 i_1) •> f i_1 j_1 = ∑ i' : n, ∑ j' : m, (if i = i' then 1 else 0) •> (if j = j' then 1 else 0) •> f i' j'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : LinearOrder α<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>x y : α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : OrderTopology α<GOAL>ContinuousWithinAt f (Iio x) x ↔ leftLim f x = f x