ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>u : ℕ → ℝ<VAR>l : ℝ<VAR>hmono : Monotone u<VAR>c : ℕ → ℝ<VAR>cone : ∀ (k : ℕ), 1 < c k<VAR>clim : Tendsto c atTop (𝓝 1)<VAR>hc : ∀ (k : ℕ), Tendsto (fun n => u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)<VAR>a : ℝ<VAR>ha : 1 < a<VAR>k : ℕ<VAR>hk : c k < a<VAR>H : ∀ (n : ℕ), 0 < ↑⌊c k ^ n⌋₊<VAR>A : Tendsto (fun n => ↑⌊c k ^ (n + 1)⌋₊ / c k ^ (n + 1) * c k / (↑⌊c k ^ n⌋₊ / c k ^ n)) atTop (𝓝 (1 * c k / 1))<VAR>B : Tendsto (fun n => ↑⌊c k ^ (n + 1)⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 (c k))<GOAL>∀ᶠ (n : ℕ) in atTop, ↑((fun n => ⌊c k ^ n⌋₊) (n + 1)) ≤ a * ↑((fun n => ⌊c k ^ n⌋₊) n)
<VAR>u : ℕ → ℝ<VAR>l : ℝ<VAR>hmono : Monotone u<VAR>c : ℕ → ℝ<VAR>cone : ∀ (k : ℕ), 1 < c k<VAR>clim : Tendsto c atTop (𝓝 1)<VAR>hc : ∀ (k : ℕ), Tendsto (fun n => u ⌊c k ^ n⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 l)<VAR>a : ℝ<VAR>ha : 1 < a<VAR>k : ℕ<VAR>hk : c k < a<VAR>H : ∀ (n : ℕ), 0 < ↑⌊c k ^ n⌋₊<VAR>A : Tendsto (fun n => ↑⌊c k ^ (n + 1)⌋₊ / c k ^ (n + 1) * c k / (↑⌊c k ^ n⌋₊ / c k ^ n)) atTop (𝓝 (1 * c k / 1))<VAR>B : Tendsto (fun n => ↑⌊c k ^ (n + 1)⌋₊ / ↑⌊c k ^ n⌋₊) atTop (𝓝 (c k))<VAR>n : ℕ<VAR>hn : ↑⌊c k ^ (n + 1)⌋₊ / ↑⌊c k ^ n⌋₊ < a<GOAL>↑⌊c k ^ (n + 1)⌋₊ ≤ a * ↑⌊c k ^ n⌋₊
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>n : ℕ<GOAL>(PInfty ≫ QInfty).f n = HomologicalComplex.Hom.f 0 n
<VAR>α : Type u<VAR>a : α<VAR>inst✝² : Group α<VAR>inst✝¹ : Finite α<VAR>inst✝ : IsCyclic α<GOAL>∃ x, ∀ (y : α), y ∈ Submonoid.powers x
<VAR>α : Type u<VAR>a : α<VAR>inst✝² : Group α<VAR>inst✝¹ : Finite α<VAR>inst✝ : IsCyclic α<GOAL>∃ x, ∀ (y : α), y ∈ zpowers x
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x✝ y✝ x y : V<GOAL>sin (arccos (⟪x, y⟫_ℝ / (‖x‖ * ‖y‖))) * (‖x‖ * ‖y‖) = √(⟪x, x⟫_ℝ * ⟪y, y⟫_ℝ - ⟪x, y⟫_ℝ * ⟪x, y⟫_ℝ)
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x✝ y✝ x y : V<GOAL>√((1 - ⟪x, y⟫_ℝ / (‖x‖ * ‖y‖) * (⟪x, y⟫_ℝ / (‖x‖ * ‖y‖))) * (‖x‖ * ‖y‖ * (‖x‖ * ‖y‖))) = √(‖x‖ * ‖x‖ * (‖y‖ * ‖y‖) - ⟪x, y⟫_ℝ * ⟪x, y⟫_ℝ)
<VAR>α : Type u_1<VAR>inst✝ : OrderedCommGroup α<VAR>s t : Set α<VAR>a : α<GOAL>↑(lowerClosure (s * t)) = ↑(lowerClosure s * lowerClosure t)
<VAR>G : Type u<VAR>inst✝² : Group G<VAR>N : Subgroup G<VAR>nN : N.Normal<VAR>H : Type v<VAR>inst✝¹ : Group H<VAR>M : Type x<VAR>inst✝ : Monoid M<VAR>φ : G →* H<VAR>a✝ b✝ : G ⧸ φ.ker<VAR>a b : G<VAR>h : φ a = φ b<GOAL>Setoid.r a b
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁷ : NormedAddCommGroup D<VAR>inst✝⁶ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>s✝ s₁ t u : Set E<VAR>f : E → F →L[𝕜] G<VAR>g : E → F<VAR>s : Set E<VAR>x : E<VAR>N : ℕ∞<VAR>n : ℕ<VAR>hf : ContDiffOn 𝕜 N f s<VAR>hg : ContDiffOn 𝕜 N g s<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hx : x ∈ s<VAR>hn : ↑n ≤ N<VAR>B : (F →L[𝕜] G) →L[𝕜] F →L[𝕜] G := (ContinuousLinearMap.apply 𝕜 G).flip<GOAL>‖iteratedFDerivWithin 𝕜 n (fun y => (f y) (g y)) s x‖ ≤ ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁷ : NormedAddCommGroup D<VAR>inst✝⁶ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>s✝ s₁ t u : Set E<VAR>f : E → F →L[𝕜] G<VAR>g : E → F<VAR>s : Set E<VAR>x : E<VAR>N : ℕ∞<VAR>n : ℕ<VAR>hf : ContDiffOn 𝕜 N f s<VAR>hg : ContDiffOn 𝕜 N g s<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hx : x ∈ s<VAR>hn : ↑n ≤ N<VAR>B : (F →L[𝕜] G) →L[𝕜] F →L[𝕜] G := (ContinuousLinearMap.apply 𝕜 G).flip<VAR>hB : ‖B‖ ≤ 1<GOAL>‖iteratedFDerivWithin 𝕜 n (fun y => (f y) (g y)) s x‖ ≤ ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖
<VAR>M : Type u_1<VAR>α✝ : Type u_2<VAR>β✝ : Type u_3<VAR>inst✝⁹ : TopologicalSpace α✝<VAR>inst✝⁸ : Monoid M<VAR>inst✝⁷ : MulAction M α✝<VAR>inst✝⁶ : ContinuousConstSMul M α✝<VAR>N : Type u_4<VAR>inst✝⁵ : Monoid N<VAR>α : Type u_5<VAR>β : Type u_6<VAR>inst✝⁴ : MulAction M α<VAR>inst✝³ : MulAction N β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : T2Space β<VAR>inst✝ : ContinuousConstSMul N β<VAR>σ : M → N<GOAL>IsClosed {f | ∀ (c : M) (x : α), f (c • x) = σ c • f x}
<VAR>M : Type u_1<VAR>α✝ : Type u_2<VAR>β✝ : Type u_3<VAR>inst✝⁹ : TopologicalSpace α✝<VAR>inst✝⁸ : Monoid M<VAR>inst✝⁷ : MulAction M α✝<VAR>inst✝⁶ : ContinuousConstSMul M α✝<VAR>N : Type u_4<VAR>inst✝⁵ : Monoid N<VAR>α : Type u_5<VAR>β : Type u_6<VAR>inst✝⁴ : MulAction M α<VAR>inst✝³ : MulAction N β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : T2Space β<VAR>inst✝ : ContinuousConstSMul N β<VAR>σ : M → N<GOAL>IsClosed (⋂ i, ⋂ i_1, {x | x (i • i_1) = σ i • x i_1})
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>x y : RatFunc K<VAR>hxy : x + y ≠ 0<VAR>h_zero : x.num * y.denom + x.denom * y.num = 0<GOAL>False
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>x y : RatFunc K<VAR>hxy : x + y ≠ 0<VAR>h_zero : x.num * y.denom + x.denom * y.num = 0<VAR>h : (x + y).num * (x.denom * y.denom) = (x.num * y.denom + x.denom * y.num) * (x + y).denom<GOAL>False
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>x y : RatFunc K<VAR>hxy : x + y ≠ 0<VAR>h_zero : x.num * y.denom + x.denom * y.num = 0<VAR>h : (x + y).num * (x.denom * y.denom) = 0<GOAL>False
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : RCLike 𝕜<VAR>μ : Measure ℝ<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : CompleteSpace E<VAR>H : Type u_3<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>a b ε : ℝ<VAR>bound : ℝ → ℝ<VAR>F : H → ℝ → E<VAR>F' : ℝ → H →L[𝕜] E<VAR>x₀ : H<VAR>ε_pos : 0 < ε<VAR>hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))<VAR>hF_int : IntervalIntegrable (F x₀) μ a b<VAR>hF'_meas : AEStronglyMeasurable F' (μ.restrict (Ι a b))<VAR>h_lip : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → LipschitzOnWith (Real.nnabs (bound t)) (fun x => F x t) (ball x₀ ε)<VAR>bound_integrable : IntervalIntegrable bound μ a b<VAR>h_diff : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → HasFDerivAt (fun x => F x t) (F' t) x₀<GOAL>IntervalIntegrable F' μ a b ∧ HasFDerivAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' t ∂μ) x₀
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : RCLike 𝕜<VAR>μ : Measure ℝ<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : CompleteSpace E<VAR>H : Type u_3<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>a b ε : ℝ<VAR>bound : ℝ → ℝ<VAR>F : H → ℝ → E<VAR>F' : ℝ → H →L[𝕜] E<VAR>x₀ : H<VAR>ε_pos : 0 < ε<VAR>hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))<VAR>hF_int : IntervalIntegrable (F x₀) μ a b<VAR>hF'_meas : AEStronglyMeasurable F' (μ.restrict (Ι a b))<VAR>h_lip : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), LipschitzOnWith (Real.nnabs (bound x)) (fun x_1 => F x_1 x) (ball x₀ ε)<VAR>bound_integrable : IntervalIntegrable bound μ a b<VAR>h_diff : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), HasFDerivAt (fun x_1 => F x_1 x) (F' x) x₀<GOAL>IntervalIntegrable F' μ a b ∧ HasFDerivAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' t ∂μ) x₀
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : RCLike 𝕜<VAR>μ : Measure ℝ<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : CompleteSpace E<VAR>H : Type u_3<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>a b ε : ℝ<VAR>bound : ℝ → ℝ<VAR>F : H → ℝ → E<VAR>F' : ℝ → H →L[𝕜] E<VAR>x₀ : H<VAR>ε_pos : 0 < ε<VAR>hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))<VAR>hF'_meas : AEStronglyMeasurable F' (μ.restrict (Ι a b))<VAR>h_lip : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), LipschitzOnWith (Real.nnabs (bound x)) (fun x_1 => F x_1 x) (ball x₀ ε)<VAR>h_diff : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), HasFDerivAt (fun x_1 => F x_1 x) (F' x) x₀<VAR>hF_int : IntegrableOn (F x₀) (Ι a b) μ<VAR>bound_integrable : IntegrableOn bound (Ι a b) μ<GOAL>IntegrableOn F' (Ι a b) μ ∧ HasFDerivAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) (∫ (t : ℝ) in a..b, F' t ∂μ) x₀
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : RCLike 𝕜<VAR>μ : Measure ℝ<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : CompleteSpace E<VAR>H : Type u_3<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>a b ε : ℝ<VAR>bound : ℝ → ℝ<VAR>F : H → ℝ → E<VAR>F' : ℝ → H →L[𝕜] E<VAR>x₀ : H<VAR>ε_pos : 0 < ε<VAR>hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))<VAR>hF'_meas : AEStronglyMeasurable F' (μ.restrict (Ι a b))<VAR>h_lip : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), LipschitzOnWith (Real.nnabs (bound x)) (fun x_1 => F x_1 x) (ball x₀ ε)<VAR>h_diff : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), HasFDerivAt (fun x_1 => F x_1 x) (F' x) x₀<VAR>hF_int : IntegrableOn (F x₀) (Ι a b) μ<VAR>bound_integrable : IntegrableOn bound (Ι a b) μ<GOAL>IntegrableOn F' (Ι a b) μ ∧ HasFDerivAt (fun x => (if a ≤ b then 1 else -1) • ∫ (t : ℝ) in Ι a b, F x t ∂μ) ((if a ≤ b then 1 else -1) • ∫ (t : ℝ) in Ι a b, F' t ∂μ) x₀
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : RCLike 𝕜<VAR>μ : Measure ℝ<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>inst✝² : CompleteSpace E<VAR>H : Type u_3<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>a b ε : ℝ<VAR>bound : ℝ → ℝ<VAR>F : H → ℝ → E<VAR>F' : ℝ → H →L[𝕜] E<VAR>x₀ : H<VAR>ε_pos : 0 < ε<VAR>hF_meas : ∀ᶠ (x : H) in 𝓝 x₀, AEStronglyMeasurable (F x) (μ.restrict (Ι a b))<VAR>hF'_meas : AEStronglyMeasurable F' (μ.restrict (Ι a b))<VAR>h_lip : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), LipschitzOnWith (Real.nnabs (bound x)) (fun x_1 => F x_1 x) (ball x₀ ε)<VAR>h_diff : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), HasFDerivAt (fun x_1 => F x_1 x) (F' x) x₀<VAR>hF_int : IntegrableOn (F x₀) (Ι a b) μ<VAR>bound_integrable : IntegrableOn bound (Ι a b) μ<VAR>this : Integrable F' (μ.restrict (Ι a b)) ∧ HasFDerivAt (fun x => ∫ (a : ℝ) in Ι a b, F x a ∂μ) (∫ (a : ℝ) in Ι a b, F' a ∂μ) x₀<GOAL>IntegrableOn F' (Ι a b) μ ∧ HasFDerivAt (fun x => (if a ≤ b then 1 else -1) • ∫ (t : ℝ) in Ι a b, F x t ∂μ) ((if a ≤ b then 1 else -1) • ∫ (t : ℝ) in Ι a b, F' t ∂μ) x₀
<VAR>G✝ : Type u_1<VAR>inst✝² : Group G✝<VAR>H : Subgroup G✝<VAR>inst✝¹ : H.Normal<VAR>G : Type u_2<VAR>inst✝ : CommGroup G<GOAL>Group.nilpotencyClass G ≤ 1
<VAR>G✝ : Type u_1<VAR>inst✝² : Group G✝<VAR>H : Subgroup G✝<VAR>inst✝¹ : H.Normal<VAR>G : Type u_2<VAR>inst✝ : CommGroup G<GOAL>center G = ⊤
<VAR>α β : Type u<VAR>x : Cardinal.{u_1}<GOAL>x ∈ range Nat.cast ↔ x ∈ Iio ℵ₀
<VAR>α : Type u_1<VAR>A : Set α<VAR>β : Type u_2<VAR>inst✝¹ : Zero β<VAR>inst✝ : TopologicalSpace β<VAR>ι : Type u_3<VAR>L : Filter ι<VAR>As : ι → Set α<VAR>b : β<VAR>nhd_b : {0}ᶜ ∈ 𝓝 b<VAR>nhd_o : {b}ᶜ ∈ 𝓝 0<GOAL>Tendsto (fun i => (As i).indicator fun x => b) L (𝓝 (A.indicator fun x => b)) ↔ ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
<VAR>α : Type u_1<VAR>A : Set α<VAR>β : Type u_2<VAR>inst✝¹ : Zero β<VAR>inst✝ : TopologicalSpace β<VAR>ι : Type u_3<VAR>L : Filter ι<VAR>As : ι → Set α<VAR>b : β<VAR>nhd_b : {0}ᶜ ∈ 𝓝 b<VAR>nhd_o : {b}ᶜ ∈ 𝓝 0<GOAL>(∀ (x : α), Tendsto (fun i => (As i).indicator (fun x => b) x) L (𝓝 (A.indicator (fun x => b) x))) ↔ ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
<VAR>α : Type u_1<VAR>A : Set α<VAR>β : Type u_2<VAR>inst✝¹ : Zero β<VAR>inst✝ : TopologicalSpace β<VAR>ι : Type u_3<VAR>L : Filter ι<VAR>As : ι → Set α<VAR>b : β<VAR>nhd_b : {0}ᶜ ∈ 𝓝 b<VAR>nhd_o : {b}ᶜ ∈ 𝓝 0<GOAL>∀ (a : α), Tendsto (fun i => (As i).indicator (fun x => b) a) L (𝓝 (A.indicator (fun x => b) a)) ↔ ∀ᶠ (i : ι) in L, a ∈ As i ↔ a ∈ A
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁹ : Category.{u_3, u_1} C<VAR>inst✝⁸ : Category.{u_4, u_2} D<VAR>inst✝⁷ : HasZeroMorphisms C<VAR>inst✝⁶ : HasZeroMorphisms D<VAR>S : ShortComplex C<VAR>h₁✝ : S.LeftHomologyData<VAR>h₂✝ : S.RightHomologyData<VAR>F✝ : C ⥤ D<VAR>inst✝⁵ : F✝.PreservesZeroMorphisms<VAR>hl : S.LeftHomologyData<VAR>hr : S.RightHomologyData<VAR>S₁ S₂ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>hl₁ : S₁.LeftHomologyData<VAR>hr₁ : S₁.RightHomologyData<VAR>hl₂ : S₂.LeftHomologyData<VAR>hr₂ : S₂.RightHomologyData<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>F : C ⥤ D<VAR>inst✝⁴ : F.PreservesZeroMorphisms<VAR>inst✝³ : S₁.HasRightHomology<VAR>inst✝² : S₂.HasRightHomology<VAR>inst✝¹ : F.PreservesRightHomologyOf S₁<VAR>inst✝ : F.PreservesRightHomologyOf S₂<GOAL>F.map (opcyclesMap φ) ≫ (S₂.mapOpcyclesIso F).inv = (S₁.mapOpcyclesIso F).inv ≫ opcyclesMap (F.mapShortComplex.map φ)
<VAR>F : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>R : Type u_4<VAR>α : Type u_5<VAR>inst✝¹² : NonUnitalNonAssocSemiring α<VAR>inst✝¹¹ : Monoid M<VAR>inst✝¹⁰ : Monoid N<VAR>inst✝⁹ : Semiring R<VAR>inst✝⁸ : DistribMulAction M α<VAR>inst✝⁷ : SMulCommClass M α α<VAR>inst✝⁶ : IsScalarTower M α α<VAR>inst✝⁵ : DistribMulAction N α<VAR>inst✝⁴ : SMulCommClass N α α<VAR>inst✝³ : IsScalarTower N α α<VAR>inst✝² : Module R α<VAR>inst✝¹ : SMulCommClass R α α<VAR>inst✝ : IsScalarTower R α α<VAR>T S : CentroidHom α<VAR>a b : α<GOAL>(⇑T ∘ ⇑S) (a * b) = (⇑S ∘ ⇑T) (a * b)
<VAR>F : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>R : Type u_4<VAR>α : Type u_5<VAR>inst✝¹² : NonUnitalNonAssocSemiring α<VAR>inst✝¹¹ : Monoid M<VAR>inst✝¹⁰ : Monoid N<VAR>inst✝⁹ : Semiring R<VAR>inst✝⁸ : DistribMulAction M α<VAR>inst✝⁷ : SMulCommClass M α α<VAR>inst✝⁶ : IsScalarTower M α α<VAR>inst✝⁵ : DistribMulAction N α<VAR>inst✝⁴ : SMulCommClass N α α<VAR>inst✝³ : IsScalarTower N α α<VAR>inst✝² : Module R α<VAR>inst✝¹ : SMulCommClass R α α<VAR>inst✝ : IsScalarTower R α α<VAR>T S : CentroidHom α<VAR>a b : α<GOAL>T (S (a * b)) = S (T (a * b))
<VAR>n : Type u<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>R : Type v<VAR>inst✝¹ : CommRing R<VAR>S : Type u_1<VAR>inst✝ : CommRing S<VAR>i : n<VAR>A : ↥(center (SpecialLinearGroup n R))<VAR>this : Nonempty n<GOAL>↑↑A i i ^ ↑(Fintype.card n).toPNat' = 1
<VAR>n : Type u<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>R : Type v<VAR>inst✝¹ : CommRing R<VAR>S : Type u_1<VAR>inst✝ : CommRing S<VAR>i : n<VAR>A : ↥(center (SpecialLinearGroup n R))<VAR>this : Nonempty n<VAR>r : R<VAR>hr : r ^ Fintype.card n = 1<VAR>hr' : (scalar n) r = ↑↑A<GOAL>↑↑A i i ^ ↑(Fintype.card n).toPNat' = 1
<VAR>n : Type u<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>R : Type v<VAR>inst✝¹ : CommRing R<VAR>S : Type u_1<VAR>inst✝ : CommRing S<VAR>i : n<VAR>a : ↥(rootsOfUnity (Fintype.card n).toPNat' R)<VAR>B : SpecialLinearGroup n R<GOAL>↑(B * ⟨a • 1, ⋯⟩) = ↑(⟨a • 1, ⋯⟩ * B)
<VAR>n : Type u<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>R : Type v<VAR>inst✝¹ : CommRing R<VAR>S : Type u_1<VAR>inst✝ : CommRing S<VAR>i : n<VAR>A : ↥(center (SpecialLinearGroup n R))<GOAL>(fun a => ⟨⟨a • 1, ⋯⟩, ⋯⟩) ((fun A => rootsOfUnity.mkOfPowEq (↑↑A i i) ⋯) A) = A
<VAR>n : Type u<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>R : Type v<VAR>inst✝¹ : CommRing R<VAR>S : Type u_1<VAR>inst✝ : CommRing S<VAR>i : n<VAR>A : ↥(center (SpecialLinearGroup n R))<GOAL>↑↑((fun a => ⟨⟨a • 1, ⋯⟩, ⋯⟩) ((fun A => rootsOfUnity.mkOfPowEq (↑↑A i i) ⋯) A)) = ↑↑A
<VAR>n : Type u<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>R : Type v<VAR>inst✝¹ : CommRing R<VAR>S : Type u_1<VAR>inst✝ : CommRing S<VAR>i : n<VAR>A : ↥(center (SpecialLinearGroup n R))<VAR>r : R<VAR>left✝ : r ^ Fintype.card n = 1<VAR>hr : (scalar n) r = ↑↑A<GOAL>↑↑((fun a => ⟨⟨a • 1, ⋯⟩, ⋯⟩) ((fun A => rootsOfUnity.mkOfPowEq (↑↑A i i) ⋯) A)) = ↑↑A
<VAR>n : Type u<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>R : Type v<VAR>inst✝¹ : CommRing R<VAR>S : Type u_1<VAR>inst✝ : CommRing S<VAR>i : n<VAR>a inv✝ : R<VAR>val_inv✝ : a * inv✝ = 1<VAR>inv_val✝ : inv✝ * a = 1<VAR>ha : { val := a, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } ∈ rootsOfUnity (Fintype.card n).toPNat' R<GOAL>(fun A => rootsOfUnity.mkOfPowEq (↑↑A i i) ⋯) ((fun a => ⟨⟨a • 1, ⋯⟩, ⋯⟩) ⟨{ val := a, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }, ha⟩) = ⟨{ val := a, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }, ha⟩
<VAR>n : Type u<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>R : Type v<VAR>inst✝¹ : CommRing R<VAR>S : Type u_1<VAR>inst✝ : CommRing S<VAR>i : n<VAR>A B : ↥(center (SpecialLinearGroup n R))<GOAL>↑↑(rootsOfUnity.mkOfPowEq ((↑↑A * ↑↑B) i i) ⋯) = ↑↑(rootsOfUnity.mkOfPowEq (↑↑A i i) ⋯ * rootsOfUnity.mkOfPowEq (↑↑B i i) ⋯)
<VAR>n : Type u<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>R : Type v<VAR>inst✝¹ : CommRing R<VAR>S : Type u_1<VAR>inst✝ : CommRing S<VAR>i : n<VAR>A B : ↥(center (SpecialLinearGroup n R))<GOAL>(↑↑A * ↑↑B) i i = ↑↑A i i * ↑↑B i i
<VAR>n : Type u<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>R : Type v<VAR>inst✝¹ : CommRing R<VAR>S : Type u_1<VAR>inst✝ : CommRing S<VAR>i : n<VAR>A B : ↥(center (SpecialLinearGroup n R))<GOAL>((scalar n) (↑↑A i i) * (scalar n) (↑↑B i i)) i i = (scalar n) (↑↑A i i) i i * (scalar n) (↑↑B i i) i i
<VAR>𝕜₁ : Type u_1<VAR>inst✝²² : NontriviallyNormedField 𝕜₁<VAR>𝕜₂ : Type u_2<VAR>inst✝²¹ : NontriviallyNormedField 𝕜₂<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>iσ : RingHomIsometric σ<VAR>B : Type u_3<VAR>F₁ : Type u_4<VAR>inst✝²⁰ : NormedAddCommGroup F₁<VAR>inst✝¹⁹ : NormedSpace 𝕜₁ F₁<VAR>E₁ : B → Type u_5<VAR>inst✝¹⁸ : (x : B) → AddCommGroup (E₁ x)<VAR>inst✝¹⁷ : (x : B) → Module 𝕜₁ (E₁ x)<VAR>inst✝¹⁶ : TopologicalSpace (TotalSpace F₁ E₁)<VAR>F₂ : Type u_6<VAR>inst✝¹⁵ : NormedAddCommGroup F₂<VAR>inst✝¹⁴ : NormedSpace 𝕜₂ F₂<VAR>E₂ : B → Type u_7<VAR>inst✝¹³ : (x : B) → AddCommGroup (E₂ x)<VAR>inst✝¹² : (x : B) → Module 𝕜₂ (E₂ x)<VAR>inst✝¹¹ : TopologicalSpace (TotalSpace F₂ E₂)<VAR>inst✝¹⁰ : TopologicalSpace B<VAR>e₁ e₁' : Trivialization F₁ TotalSpace.proj<VAR>e₂ e₂' : Trivialization F₂ TotalSpace.proj<VAR>inst✝⁹ : (x : B) → TopologicalSpace (E₁ x)<VAR>inst✝⁸ : FiberBundle F₁ E₁<VAR>inst✝⁷ : (x : B) → TopologicalSpace (E₂ x)<VAR>ita : ∀ (x : B), TopologicalAddGroup (E₂ x)<VAR>inst✝⁶ : FiberBundle F₂ E₂<VAR>inst✝⁵ : VectorBundle 𝕜₁ F₁ E₁<VAR>inst✝⁴ : VectorBundle 𝕜₂ F₂ E₂<VAR>inst✝³ : MemTrivializationAtlas e₁<VAR>inst✝² : MemTrivializationAtlas e₁'<VAR>inst✝¹ : MemTrivializationAtlas e₂<VAR>inst✝ : MemTrivializationAtlas e₂'<GOAL>ContinuousOn (continuousLinearMapCoordChange σ e₁ e₁' e₂ e₂') (e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet))
<VAR>𝕜₁ : Type u_1<VAR>inst✝²² : NontriviallyNormedField 𝕜₁<VAR>𝕜₂ : Type u_2<VAR>inst✝²¹ : NontriviallyNormedField 𝕜₂<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>iσ : RingHomIsometric σ<VAR>B : Type u_3<VAR>F₁ : Type u_4<VAR>inst✝²⁰ : NormedAddCommGroup F₁<VAR>inst✝¹⁹ : NormedSpace 𝕜₁ F₁<VAR>E₁ : B → Type u_5<VAR>inst✝¹⁸ : (x : B) → AddCommGroup (E₁ x)<VAR>inst✝¹⁷ : (x : B) → Module 𝕜₁ (E₁ x)<VAR>inst✝¹⁶ : TopologicalSpace (TotalSpace F₁ E₁)<VAR>F₂ : Type u_6<VAR>inst✝¹⁵ : NormedAddCommGroup F₂<VAR>inst✝¹⁴ : NormedSpace 𝕜₂ F₂<VAR>E₂ : B → Type u_7<VAR>inst✝¹³ : (x : B) → AddCommGroup (E₂ x)<VAR>inst✝¹² : (x : B) → Module 𝕜₂ (E₂ x)<VAR>inst✝¹¹ : TopologicalSpace (TotalSpace F₂ E₂)<VAR>inst✝¹⁰ : TopologicalSpace B<VAR>e₁ e₁' : Trivialization F₁ TotalSpace.proj<VAR>e₂ e₂' : Trivialization F₂ TotalSpace.proj<VAR>inst✝⁹ : (x : B) → TopologicalSpace (E₁ x)<VAR>inst✝⁸ : FiberBundle F₁ E₁<VAR>inst✝⁷ : (x : B) → TopologicalSpace (E₂ x)<VAR>ita : ∀ (x : B), TopologicalAddGroup (E₂ x)<VAR>inst✝⁶ : FiberBundle F₂ E₂<VAR>inst✝⁵ : VectorBundle 𝕜₁ F₁ E₁<VAR>inst✝⁴ : VectorBundle 𝕜₂ F₂ E₂<VAR>inst✝³ : MemTrivializationAtlas e₁<VAR>inst✝² : MemTrivializationAtlas e₁'<VAR>inst✝¹ : MemTrivializationAtlas e₂<VAR>inst✝ : MemTrivializationAtlas e₂'<VAR>h₁ : Continuous ⇑(compSL F₁ F₂ F₂ σ (RingHom.id 𝕜₂))<GOAL>ContinuousOn (continuousLinearMapCoordChange σ e₁ e₁' e₂ e₂') (e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet))
<VAR>𝕜₁ : Type u_1<VAR>inst✝²² : NontriviallyNormedField 𝕜₁<VAR>𝕜₂ : Type u_2<VAR>inst✝²¹ : NontriviallyNormedField 𝕜₂<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>iσ : RingHomIsometric σ<VAR>B : Type u_3<VAR>F₁ : Type u_4<VAR>inst✝²⁰ : NormedAddCommGroup F₁<VAR>inst✝¹⁹ : NormedSpace 𝕜₁ F₁<VAR>E₁ : B → Type u_5<VAR>inst✝¹⁸ : (x : B) → AddCommGroup (E₁ x)<VAR>inst✝¹⁷ : (x : B) → Module 𝕜₁ (E₁ x)<VAR>inst✝¹⁶ : TopologicalSpace (TotalSpace F₁ E₁)<VAR>F₂ : Type u_6<VAR>inst✝¹⁵ : NormedAddCommGroup F₂<VAR>inst✝¹⁴ : NormedSpace 𝕜₂ F₂<VAR>E₂ : B → Type u_7<VAR>inst✝¹³ : (x : B) → AddCommGroup (E₂ x)<VAR>inst✝¹² : (x : B) → Module 𝕜₂ (E₂ x)<VAR>inst✝¹¹ : TopologicalSpace (TotalSpace F₂ E₂)<VAR>inst✝¹⁰ : TopologicalSpace B<VAR>e₁ e₁' : Trivialization F₁ TotalSpace.proj<VAR>e₂ e₂' : Trivialization F₂ TotalSpace.proj<VAR>inst✝⁹ : (x : B) → TopologicalSpace (E₁ x)<VAR>inst✝⁸ : FiberBundle F₁ E₁<VAR>inst✝⁷ : (x : B) → TopologicalSpace (E₂ x)<VAR>ita : ∀ (x : B), TopologicalAddGroup (E₂ x)<VAR>inst✝⁶ : FiberBundle F₂ E₂<VAR>inst✝⁵ : VectorBundle 𝕜₁ F₁ E₁<VAR>inst✝⁴ : VectorBundle 𝕜₂ F₂ E₂<VAR>inst✝³ : MemTrivializationAtlas e₁<VAR>inst✝² : MemTrivializationAtlas e₁'<VAR>inst✝¹ : MemTrivializationAtlas e₂<VAR>inst✝ : MemTrivializationAtlas e₂'<VAR>h₁ : Continuous ⇑(compSL F₁ F₂ F₂ σ (RingHom.id 𝕜₂))<VAR>h₂ : Continuous ⇑(compSL F₁ F₁ F₂ (RingHom.id 𝕜₁) σ).flip<GOAL>ContinuousOn (continuousLinearMapCoordChange σ e₁ e₁' e₂ e₂') (e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet))
<VAR>𝕜₁ : Type u_1<VAR>inst✝²² : NontriviallyNormedField 𝕜₁<VAR>𝕜₂ : Type u_2<VAR>inst✝²¹ : NontriviallyNormedField 𝕜₂<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>iσ : RingHomIsometric σ<VAR>B : Type u_3<VAR>F₁ : Type u_4<VAR>inst✝²⁰ : NormedAddCommGroup F₁<VAR>inst✝¹⁹ : NormedSpace 𝕜₁ F₁<VAR>E₁ : B → Type u_5<VAR>inst✝¹⁸ : (x : B) → AddCommGroup (E₁ x)<VAR>inst✝¹⁷ : (x : B) → Module 𝕜₁ (E₁ x)<VAR>inst✝¹⁶ : TopologicalSpace (TotalSpace F₁ E₁)<VAR>F₂ : Type u_6<VAR>inst✝¹⁵ : NormedAddCommGroup F₂<VAR>inst✝¹⁴ : NormedSpace 𝕜₂ F₂<VAR>E₂ : B → Type u_7<VAR>inst✝¹³ : (x : B) → AddCommGroup (E₂ x)<VAR>inst✝¹² : (x : B) → Module 𝕜₂ (E₂ x)<VAR>inst✝¹¹ : TopologicalSpace (TotalSpace F₂ E₂)<VAR>inst✝¹⁰ : TopologicalSpace B<VAR>e₁ e₁' : Trivialization F₁ TotalSpace.proj<VAR>e₂ e₂' : Trivialization F₂ TotalSpace.proj<VAR>inst✝⁹ : (x : B) → TopologicalSpace (E₁ x)<VAR>inst✝⁸ : FiberBundle F₁ E₁<VAR>inst✝⁷ : (x : B) → TopologicalSpace (E₂ x)<VAR>ita : ∀ (x : B), TopologicalAddGroup (E₂ x)<VAR>inst✝⁶ : FiberBundle F₂ E₂<VAR>inst✝⁵ : VectorBundle 𝕜₁ F₁ E₁<VAR>inst✝⁴ : VectorBundle 𝕜₂ F₂ E₂<VAR>inst✝³ : MemTrivializationAtlas e₁<VAR>inst✝² : MemTrivializationAtlas e₁'<VAR>inst✝¹ : MemTrivializationAtlas e₂<VAR>inst✝ : MemTrivializationAtlas e₂'<VAR>h₁ : Continuous ⇑(compSL F₁ F₂ F₂ σ (RingHom.id 𝕜₂))<VAR>h₂ : Continuous ⇑(compSL F₁ F₁ F₂ (RingHom.id 𝕜₁) σ).flip<VAR>h₃ : ContinuousOn (fun b => ↑(Trivialization.coordChangeL 𝕜₁ e₁' e₁ b)) (e₁'.baseSet ∩ e₁.baseSet)<GOAL>ContinuousOn (continuousLinearMapCoordChange σ e₁ e₁' e₂ e₂') (e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet))