ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>N✝ N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>ι : Sort u_1<VAR>N : ι → LieSubmodule R L M<VAR>C : (x : M) → x ∈ ⨆ i, N i → Prop<VAR>hN : ∀ (i : ι) (x : M) (hx : x ∈ N i), C x ⋯<VAR>h0 : C 0 ⋯<VAR>hadd : ∀ (x y : M) (hx : x ∈ ⨆ i, N i) (hy : y ∈ ⨆ i, N i), C x hx → C y hy → C (x + y) ⋯<VAR>x✝ : M<VAR>hx : x✝ ∈ ⨆ i, N i<VAR>x y : M<GOAL>(fun x => ∃ (hx : x ∈ ⨆ i, N i), C x hx) x → (fun x => ∃ (hx : x ∈ ⨆ i, N i), C x hx) y → (fun x => ∃ (hx : x ∈ ⨆ i, N i), C x hx) (x + y)
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>(o.kahler x) y = 0 ↔ x = 0 ∨ y = 0
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>x = 0 ∨ y = 0 → (o.kahler x) y = 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>m n✝ n : ℕ<GOAL>Xor' (Even n) (Odd n)
<VAR>R : Type u_1<VAR>p m : ℕ<VAR>inst✝² : Fact (Nat.Prime p)<VAR>inst✝¹ : Ring R<VAR>inst✝ : CharP R p<VAR>hm : ¬p ∣ m<VAR>x✝ : 0 < 1<GOAL>cyclotomic (p ^ 1 * m) R = cyclotomic m R ^ (p ^ 1 - p ^ (1 - 1))
<VAR>R : Type u_1<VAR>p m : ℕ<VAR>inst✝² : Fact (Nat.Prime p)<VAR>inst✝¹ : Ring R<VAR>inst✝ : CharP R p<VAR>hm : ¬p ∣ m<VAR>a : ℕ<VAR>x✝ : 0 < a + 2<GOAL>cyclotomic (p ^ (a + 2) * m) R = cyclotomic m R ^ (p ^ (a + 2) - p ^ (a + 2 - 1))
<VAR>R : Type u_1<VAR>p m : ℕ<VAR>inst✝² : Fact (Nat.Prime p)<VAR>inst✝¹ : Ring R<VAR>inst✝ : CharP R p<VAR>hm : ¬p ∣ m<VAR>a : ℕ<VAR>x✝ : 0 < a + 2<VAR>hdiv : p ∣ p ^ a.succ * m<GOAL>cyclotomic (p ^ (a + 2) * m) R = cyclotomic m R ^ (p ^ (a + 2) - p ^ (a + 2 - 1))
<VAR>R : Type u_1<VAR>p m : ℕ<VAR>inst✝² : Fact (Nat.Prime p)<VAR>inst✝¹ : Ring R<VAR>inst✝ : CharP R p<VAR>hm : ¬p ∣ m<VAR>a : ℕ<VAR>x✝ : 0 < a + 2<VAR>hdiv : p ∣ p ^ a.succ * m<GOAL>cyclotomic m R ^ ((p ^ a.succ - p ^ (a.succ - 1)) * p) = cyclotomic m R ^ (p * p ^ (a + 1) - p ^ (a + 2 - 1))
<VAR>R : Type u_1<VAR>p m : ℕ<VAR>inst✝² : Fact (Nat.Prime p)<VAR>inst✝¹ : Ring R<VAR>inst✝ : CharP R p<VAR>hm : ¬p ∣ m<VAR>a : ℕ<VAR>x✝ : 0 < a + 2<VAR>hdiv : p ∣ p ^ a.succ * m<GOAL>¬p ∣ m
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>hconn : G.Preconnected<VAR>u v : V<GOAL>Set.univ.Nonempty
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>hconn : G.Preconnected<VAR>u v : V<GOAL>Nonempty (G.Walk u v)
<VAR>V : Type u<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n k ℓ μ : ℕ<VAR>h : G.IsSRGWith n k ℓ μ<GOAL>Gᶜ.IsRegularOfDegree (n - k - 1)
<VAR>V : Type u<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n k ℓ μ : ℕ<VAR>h : G.IsSRGWith n k ℓ μ<GOAL>Gᶜ.IsRegularOfDegree (Fintype.card V - 1 - k)
<VAR>δ : Type u_1<VAR>δ' : Type u_2<VAR>π : δ → Type u_3<VAR>inst✝² : (x : δ) → MeasurableSpace (π x)<VAR>μ : (i : δ) → Measure (π i)<VAR>inst✝¹ : ∀ (i : δ), SigmaFinite (μ i)<VAR>inst✝ : DecidableEq δ<VAR>s t : Finset δ<VAR>f✝ g : ((i : δ) → π i) → ℝ≥0∞<VAR>x✝ y✝ : (i : δ) → π i<VAR>i✝ i : δ<VAR>f : ((i : δ) → π i) → ℝ≥0∞<VAR>hf : Measurable f<VAR>hi : i ∉ s<VAR>x : (i : δ) → π i<VAR>y : π i<GOAL>(∫⋯∫⁻_s, f ∂μ) (update x i y) = (∫⋯∫⁻_s, f ∘ fun x => update x i y ∂μ) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁷ : UniformSpace α<VAR>inst✝⁶ : Group α<VAR>inst✝⁵ : UniformGroup α<VAR>hom : Type u_3<VAR>inst✝⁴ : UniformSpace β<VAR>inst✝³ : Group β<VAR>inst✝² : UniformGroup β<VAR>inst✝¹ : FunLike hom α β<VAR>inst✝ : MonoidHomClass hom α β<VAR>f : hom<VAR>hf : ContinuousAt (⇑f) 1<GOAL>Tendsto (⇑f) (𝓝 1) (𝓝 1)
<VAR>u : XgcdType<VAR>hs : u.wp + u.zp + u.wp * u.zp = u.x * u.y<GOAL>u.y * u.q + u.zp + u.wp + (u.y * u.q + u.zp) * u.wp = u.y * ((u.wp + 1) * u.q + u.x)
<VAR>u : XgcdType<VAR>hs : u.wp + u.zp + u.wp * u.zp = u.x * u.y<GOAL>u.y * u.q + u.zp + u.wp + (u.y * u.q + u.zp) * u.wp = u.y * ((u.wp + 1) * u.q) + (u.wp + u.zp + u.wp * u.zp)
<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>he : e ∈ maximalAtlas I M<VAR>he' : e' ∈ maximalAtlas I' M'<VAR>hs : s ⊆ e.source<VAR>h2s : MapsTo f s e'.source<GOAL>ContMDiffOn I I' n f s ↔ ContinuousOn f s ∧ ContDiffOn 𝕜 n (↑(e'.extend I') ∘ f ∘ ↑(e.extend I).symm) (↑(e.extend I) '' s)
<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>he : e ∈ maximalAtlas I M<VAR>he' : e' ∈ maximalAtlas I' M'<VAR>hs : s ⊆ e.source<VAR>h2s : MapsTo f s e'.source<GOAL>(∀ x ∈ s, ContMDiffWithinAt I I' n f s x) ↔ ∀ x ∈ s, ContinuousWithinAt f s x ∧ ContDiffWithinAt 𝕜 n (↑(e'.extend I') ∘ f ∘ ↑(e.extend I).symm) (↑(e.extend I) '' s) (↑(e.extend I) x)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>E' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝⁸ : RCLike 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : InnerProductSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : InnerProductSpace 𝕜 F<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : InnerProductSpace 𝕜 G<VAR>inst✝¹ : NormedAddCommGroup E'<VAR>inst✝ : InnerProductSpace ℝ E'<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>x y : E<GOAL>⟪(↑ℝ T) x, y⟫_ℝ = ⟪x, (↑ℝ T) y⟫_ℝ
<VAR>ι✝ : Type u_1<VAR>ι'✝ : Type u_2<VAR>R : Type u_3<VAR>K : Type u_4<VAR>A : Type u_5<VAR>A' : Type u_6<VAR>A'' : Type u_7<VAR>V : Type u<VAR>V' : Type u_8<VAR>x : ι✝ → A<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing A'<VAR>inst✝³ : CommRing A''<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra R A'<VAR>inst✝ : Algebra R A''<VAR>a b : R<VAR>ι : Type u_9<VAR>ι' : Type u_10<VAR>s : Set ι<VAR>f : ι → ι'<VAR>g : ι' → A<VAR>hs : AlgebraicIndependent R fun x => g (f ↑x)<VAR>a✝ : Nontrivial R<GOAL>AlgebraicIndependent R fun x => g ↑x
<VAR>ι✝ : Type u_1<VAR>ι'✝ : Type u_2<VAR>R : Type u_3<VAR>K : Type u_4<VAR>A : Type u_5<VAR>A' : Type u_6<VAR>A'' : Type u_7<VAR>V : Type u<VAR>V' : Type u_8<VAR>x : ι✝ → A<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing A'<VAR>inst✝³ : CommRing A''<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Algebra R A'<VAR>inst✝ : Algebra R A''<VAR>a b : R<VAR>ι : Type u_9<VAR>ι' : Type u_10<VAR>s : Set ι<VAR>f : ι → ι'<VAR>g : ι' → A<VAR>hs : AlgebraicIndependent R fun x => g (f ↑x)<VAR>a✝ : Nontrivial R<VAR>this : InjOn f s<GOAL>AlgebraicIndependent R fun x => g ↑x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>k f g g' : α → β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : CommSemiring β<VAR>inst✝ : ContinuousMul β<VAR>hf : SuperpolynomialDecay l k f<VAR>hg : SuperpolynomialDecay l k g<VAR>z : ℕ<GOAL>Tendsto (fun a => k a ^ z * (f * g) a) l (𝓝 0)
<VAR>N : ℕ<VAR>a : Fin 2 → ZMod N<VAR>v : Fin 2 → ℤ<VAR>hv : v ∈ gammaSet N a<VAR>γ : SL(2, ℤ)<GOAL>v ᵥ* ↑γ ∈ gammaSet N (a ᵥ* ↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ))
<VAR>N : ℕ<VAR>a : Fin 2 → ZMod N<VAR>v : Fin 2 → ℤ<VAR>hv : v ∈ gammaSet N a<VAR>γ : SL(2, ℤ)<GOAL>Int.cast ∘ (v ᵥ* ↑γ) = a ᵥ* ↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ)
<VAR>N : ℕ<VAR>a : Fin 2 → ZMod N<VAR>v : Fin 2 → ℤ<VAR>hv : v ∈ gammaSet N a<VAR>γ : SL(2, ℤ)<VAR>this : ∀ (i : Fin 2), (Int.castRingHom (ZMod N)) ((v ᵥ* ↑γ) i) = (⇑(Int.castRingHom (ZMod N)) ∘ v ᵥ* (↑γ).map ⇑(Int.castRingHom (ZMod N))) i<GOAL>Int.cast ∘ (v ᵥ* ↑γ) = a ᵥ* ↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ)
<VAR>N : ℕ<VAR>a : Fin 2 → ZMod N<VAR>v : Fin 2 → ℤ<VAR>hv : v ∈ gammaSet N a<VAR>γ : SL(2, ℤ)<VAR>this : ∀ (i : Fin 2), ↑((v ᵥ* ↑γ) i) = ((fun x => ↑x) ∘ v ᵥ* (↑γ).map fun x => ↑x) i<GOAL>Int.cast ∘ (v ᵥ* ↑γ) = a ᵥ* ↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ)
<VAR>N : ℕ<VAR>a : Fin 2 → ZMod N<VAR>v : Fin 2 → ℤ<VAR>hv : v ∈ gammaSet N a<VAR>γ : SL(2, ℤ)<VAR>this : ∀ (i : Fin 2), ↑((v ᵥ* ↑γ) i) = ((fun x => ↑x) ∘ v ᵥ* (↑γ).map fun x => ↑x) i<GOAL>(fun x => (a ᵥ* (↑γ).map fun x => ↑x) x) = a ᵥ* ↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ)
<VAR>R : Type u_1<VAR>η : Type u_2<VAR>ιs : η → Type u_3<VAR>Ms : η → Type u_4<VAR>inst✝³ : Ring R<VAR>inst✝² : (i : η) → AddCommGroup (Ms i)<VAR>inst✝¹ : (i : η) → Module R (Ms i)<VAR>inst✝ : DecidableEq η<VAR>v : (j : η) → ιs j → Ms j<VAR>hs : ∀ (i : η), LinearIndependent R (v i)<GOAL>LinearIndependent R fun ji => (stdBasis R Ms ji.fst) (v ji.fst ji.snd)
<VAR>R : Type u_1<VAR>η : Type u_2<VAR>ιs : η → Type u_3<VAR>Ms : η → Type u_4<VAR>inst✝³ : Ring R<VAR>inst✝² : (i : η) → AddCommGroup (Ms i)<VAR>inst✝¹ : (i : η) → Module R (Ms i)<VAR>inst✝ : DecidableEq η<VAR>v : (j : η) → ιs j → Ms j<VAR>hs : ∀ (i : η), LinearIndependent R (v i)<VAR>hs' : ∀ (j : η), LinearIndependent R fun i => (stdBasis R Ms j) (v j i)<GOAL>LinearIndependent R fun ji => (stdBasis R Ms ji.fst) (v ji.fst ji.snd)
<VAR>R : Type u_1<VAR>η : Type u_2<VAR>ιs : η → Type u_3<VAR>Ms : η → Type u_4<VAR>inst✝³ : Ring R<VAR>inst✝² : (i : η) → AddCommGroup (Ms i)<VAR>inst✝¹ : (i : η) → Module R (Ms i)<VAR>inst✝ : DecidableEq η<VAR>v : (j : η) → ιs j → Ms j<VAR>hs : ∀ (i : η), LinearIndependent R (v i)<VAR>hs' : ∀ (j : η), LinearIndependent R fun i => (stdBasis R Ms j) (v j i)<GOAL>∀ (i : η) (t : Set η), t.Finite → i ∉ t → Disjoint (span R (Set.range fun i_1 => (stdBasis R Ms i) (v i i_1))) (⨆ i ∈ t, span R (Set.range fun i_1 => (stdBasis R Ms i) (v i i_1)))
<VAR>R : Type u_1<VAR>η : Type u_2<VAR>ιs : η → Type u_3<VAR>Ms : η → Type u_4<VAR>inst✝³ : Ring R<VAR>inst✝² : (i : η) → AddCommGroup (Ms i)<VAR>inst✝¹ : (i : η) → Module R (Ms i)<VAR>inst✝ : DecidableEq η<VAR>v : (j : η) → ιs j → Ms j<VAR>hs : ∀ (i : η), LinearIndependent R (v i)<VAR>hs' : ∀ (j : η), LinearIndependent R fun i => (stdBasis R Ms j) (v j i)<VAR>j : η<VAR>J : Set η<VAR>a✝ : J.Finite<VAR>hiJ : j ∉ J<GOAL>Disjoint (span R (Set.range fun i => (stdBasis R Ms j) (v j i))) (⨆ i ∈ J, span R (Set.range fun i_1 => (stdBasis R Ms i) (v i i_1)))
<VAR>R : Type u_1<VAR>η : Type u_2<VAR>ιs : η → Type u_3<VAR>Ms : η → Type u_4<VAR>inst✝³ : Ring R<VAR>inst✝² : (i : η) → AddCommGroup (Ms i)<VAR>inst✝¹ : (i : η) → Module R (Ms i)<VAR>inst✝ : DecidableEq η<VAR>v : (j : η) → ιs j → Ms j<VAR>hs : ∀ (i : η), LinearIndependent R (v i)<VAR>hs' : ∀ (j : η), LinearIndependent R fun i => (stdBasis R Ms j) (v j i)<VAR>j : η<VAR>J : Set η<VAR>a✝ : J.Finite<VAR>hiJ : j ∉ J<VAR>h₀ : ∀ (j : η), span R (Set.range fun i => (stdBasis R Ms j) (v j i)) ≤ LinearMap.range (stdBasis R Ms j)<GOAL>Disjoint (span R (Set.range fun i => (stdBasis R Ms j) (v j i))) (⨆ i ∈ J, span R (Set.range fun i_1 => (stdBasis R Ms i) (v i i_1)))
<VAR>R : Type u_1<VAR>η : Type u_2<VAR>ιs : η → Type u_3<VAR>Ms : η → Type u_4<VAR>inst✝³ : Ring R<VAR>inst✝² : (i : η) → AddCommGroup (Ms i)<VAR>inst✝¹ : (i : η) → Module R (Ms i)<VAR>inst✝ : DecidableEq η<VAR>v : (j : η) → ιs j → Ms j<VAR>hs : ∀ (i : η), LinearIndependent R (v i)<VAR>hs' : ∀ (j : η), LinearIndependent R fun i => (stdBasis R Ms j) (v j i)<VAR>j : η<VAR>J : Set η<VAR>a✝ : J.Finite<VAR>hiJ : j ∉ J<VAR>h₀ : ∀ (j : η), span R (Set.range fun i => (stdBasis R Ms j) (v j i)) ≤ LinearMap.range (stdBasis R Ms j)<VAR>h₁ : span R (Set.range fun i => (stdBasis R Ms j) (v j i)) ≤ ⨆ i ∈ {j}, LinearMap.range (stdBasis R Ms i)<GOAL>Disjoint (span R (Set.range fun i => (stdBasis R Ms j) (v j i))) (⨆ i ∈ J, span R (Set.range fun i_1 => (stdBasis R Ms i) (v i i_1)))
<VAR>R : Type u_1<VAR>η : Type u_2<VAR>ιs : η → Type u_3<VAR>Ms : η → Type u_4<VAR>inst✝³ : Ring R<VAR>inst✝² : (i : η) → AddCommGroup (Ms i)<VAR>inst✝¹ : (i : η) → Module R (Ms i)<VAR>inst✝ : DecidableEq η<VAR>v : (j : η) → ιs j → Ms j<VAR>hs : ∀ (i : η), LinearIndependent R (v i)<VAR>hs' : ∀ (j : η), LinearIndependent R fun i => (stdBasis R Ms j) (v j i)<VAR>j : η<VAR>J : Set η<VAR>a✝ : J.Finite<VAR>hiJ : j ∉ J<VAR>h₀ : ∀ (j : η), span R (Set.range fun i => (stdBasis R Ms j) (v j i)) ≤ LinearMap.range (stdBasis R Ms j)<VAR>h₁ : span R (Set.range fun i => (stdBasis R Ms j) (v j i)) ≤ ⨆ i ∈ {j}, LinearMap.range (stdBasis R Ms i)<VAR>h₂ : ⨆ j ∈ J, span R (Set.range fun i => (stdBasis R Ms j) (v j i)) ≤ ⨆ j ∈ J, LinearMap.range (stdBasis R (fun j => Ms j) j)<GOAL>Disjoint (span R (Set.range fun i => (stdBasis R Ms j) (v j i))) (⨆ i ∈ J, span R (Set.range fun i_1 => (stdBasis R Ms i) (v i i_1)))
<VAR>R : Type u_1<VAR>η : Type u_2<VAR>ιs : η → Type u_3<VAR>Ms : η → Type u_4<VAR>inst✝³ : Ring R<VAR>inst✝² : (i : η) → AddCommGroup (Ms i)<VAR>inst✝¹ : (i : η) → Module R (Ms i)<VAR>inst✝ : DecidableEq η<VAR>v : (j : η) → ιs j → Ms j<VAR>hs : ∀ (i : η), LinearIndependent R (v i)<VAR>hs' : ∀ (j : η), LinearIndependent R fun i => (stdBasis R Ms j) (v j i)<VAR>j : η<VAR>J : Set η<VAR>a✝ : J.Finite<VAR>hiJ : j ∉ J<VAR>h₀ : ∀ (j : η), span R (Set.range fun i => (stdBasis R Ms j) (v j i)) ≤ LinearMap.range (stdBasis R Ms j)<VAR>h₁ : span R (Set.range fun i => (stdBasis R Ms j) (v j i)) ≤ ⨆ i ∈ {j}, LinearMap.range (stdBasis R Ms i)<VAR>h₂ : ⨆ j ∈ J, span R (Set.range fun i => (stdBasis R Ms j) (v j i)) ≤ ⨆ j ∈ J, LinearMap.range (stdBasis R (fun j => Ms j) j)<VAR>h₃ : Disjoint (fun i => i ∈ {j}) J<GOAL>Disjoint (span R (Set.range fun i => (stdBasis R Ms j) (v j i))) (⨆ i ∈ J, span R (Set.range fun i_1 => (stdBasis R Ms i) (v i i_1)))
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>p q : A → Prop<VAR>inst✝²⁰ : Semifield R<VAR>inst✝¹⁹ : StarRing R<VAR>inst✝¹⁸ : MetricSpace R<VAR>inst✝¹⁷ : TopologicalSemiring R<VAR>inst✝¹⁶ : ContinuousStar R<VAR>inst✝¹⁵ : Semifield S<VAR>inst✝¹⁴ : StarRing S<VAR>inst✝¹³ : MetricSpace S<VAR>inst✝¹² : TopologicalSemiring S<VAR>inst✝¹¹ : ContinuousStar S<VAR>inst✝¹⁰ : TopologicalSpace A<VAR>inst✝⁹ : Ring A<VAR>inst✝⁸ : StarRing A<VAR>inst✝⁷ : Algebra S A<VAR>inst✝⁶ : ContinuousFunctionalCalculus S q<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : IsScalarTower R S A<VAR>inst✝² : StarModule R S<VAR>inst✝¹ : ContinuousSMul R S<VAR>inst✝ : CompleteSpace R<VAR>a : A<VAR>φ : C(↑(spectrum S a), S) →⋆ₐ[S] A<VAR>f : C(S, R)<VAR>h : SpectrumRestricts a ⇑f<VAR>h_id : φ (ContinuousMap.restrict (spectrum S a) (ContinuousMap.id S)) = a<GOAL>(starAlgHom φ h) (ContinuousMap.restrict (spectrum R a) (ContinuousMap.id R)) = a
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>p q : A → Prop<VAR>inst✝²⁰ : Semifield R<VAR>inst✝¹⁹ : StarRing R<VAR>inst✝¹⁸ : MetricSpace R<VAR>inst✝¹⁷ : TopologicalSemiring R<VAR>inst✝¹⁶ : ContinuousStar R<VAR>inst✝¹⁵ : Semifield S<VAR>inst✝¹⁴ : StarRing S<VAR>inst✝¹³ : MetricSpace S<VAR>inst✝¹² : TopologicalSemiring S<VAR>inst✝¹¹ : ContinuousStar S<VAR>inst✝¹⁰ : TopologicalSpace A<VAR>inst✝⁹ : Ring A<VAR>inst✝⁸ : StarRing A<VAR>inst✝⁷ : Algebra S A<VAR>inst✝⁶ : ContinuousFunctionalCalculus S q<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : IsScalarTower R S A<VAR>inst✝² : StarModule R S<VAR>inst✝¹ : ContinuousSMul R S<VAR>inst✝ : CompleteSpace R<VAR>a : A<VAR>φ : C(↑(spectrum S a), S) →⋆ₐ[S] A<VAR>f : C(S, R)<VAR>h : SpectrumRestricts a ⇑f<VAR>h_id : φ (ContinuousMap.restrict (spectrum S a) (ContinuousMap.id S)) = a<GOAL>φ ({ toFun := ⇑(StarAlgHom.ofId R S), continuous_toFun := ⋯ }.comp ((ContinuousMap.restrict (spectrum R a) (ContinuousMap.id R)).comp { toFun := Subtype.map ⇑f ⋯, continuous_toFun := ⋯ })) = a
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>p q : A → Prop<VAR>inst✝²⁰ : Semifield R<VAR>inst✝¹⁹ : StarRing R<VAR>inst✝¹⁸ : MetricSpace R<VAR>inst✝¹⁷ : TopologicalSemiring R<VAR>inst✝¹⁶ : ContinuousStar R<VAR>inst✝¹⁵ : Semifield S<VAR>inst✝¹⁴ : StarRing S<VAR>inst✝¹³ : MetricSpace S<VAR>inst✝¹² : TopologicalSemiring S<VAR>inst✝¹¹ : ContinuousStar S<VAR>inst✝¹⁰ : TopologicalSpace A<VAR>inst✝⁹ : Ring A<VAR>inst✝⁸ : StarRing A<VAR>inst✝⁷ : Algebra S A<VAR>inst✝⁶ : ContinuousFunctionalCalculus S q<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : IsScalarTower R S A<VAR>inst✝² : StarModule R S<VAR>inst✝¹ : ContinuousSMul R S<VAR>inst✝ : CompleteSpace R<VAR>a : A<VAR>φ : C(↑(spectrum S a), S) →⋆ₐ[S] A<VAR>f : C(S, R)<VAR>h : SpectrumRestricts a ⇑f<VAR>h_id : φ (ContinuousMap.restrict (spectrum S a) (ContinuousMap.id S)) = a<VAR>x : ↑(spectrum S a)<GOAL>({ toFun := ⇑(StarAlgHom.ofId R S), continuous_toFun := ⋯ }.comp ((ContinuousMap.restrict (spectrum R a) (ContinuousMap.id R)).comp { toFun := Subtype.map ⇑f ⋯, continuous_toFun := ⋯ })) x = (ContinuousMap.restrict (spectrum S a) (ContinuousMap.id S)) x
<VAR>V : Type u_1<VAR>inst✝¹ : Quiver V<VAR>W : Type u_2<VAR>σ : V → W<VAR>W' : Type u_3<VAR>inst✝ : Quiver W'<VAR>φ : V ⥤q W'<VAR>τ : W → W'<VAR>h : ∀ (x : V), φ.obj x = τ (σ x)<VAR>Φ : Push σ ⥤q W'<VAR>Φ₀ : Φ.obj = τ<VAR>Φcomp : of σ ⋙q Φ = φ<GOAL>Φ = { obj := τ, map := @PushQuiver.rec V inst✝¹ W σ (fun X Y x => τ X ⟶ τ Y) fun X Y f => id (⋯.mpr (⋯.mpr (φ.map f))) }
<VAR>V : Type u_1<VAR>inst✝¹ : Quiver V<VAR>W : Type u_2<VAR>σ : V → W<VAR>W' : Type u_3<VAR>inst✝ : Quiver W'<VAR>φ : V ⥤q W'<VAR>τ : W → W'<VAR>h : ∀ (x : V), φ.obj x = τ (σ x)<VAR>Φ : Push σ ⥤q W'<VAR>Φ₀ : Φ.obj = τ<VAR>Φcomp : of σ ⋙q Φ = φ<GOAL>∀ (X : Push σ), Φ.obj X = { obj := τ, map := @PushQuiver.rec V inst✝¹ W σ (fun X Y x => τ X ⟶ τ Y) fun X Y f => id (⋯.mpr (⋯.mpr (φ.map f))) }.obj X
<VAR>V : Type u_1<VAR>inst✝¹ : Quiver V<VAR>W : Type u_2<VAR>σ : V → W<VAR>W' : Type u_3<VAR>inst✝ : Quiver W'<VAR>φ : V ⥤q W'<VAR>τ : W → W'<VAR>h : ∀ (x : V), φ.obj x = τ (σ x)<VAR>Φ : Push σ ⥤q W'<VAR>Φ₀ : Φ.obj = τ<VAR>Φcomp : of σ ⋙q Φ = φ<GOAL>∀ (X Y : Push σ) (f : X ⟶ Y), Φ.map f = Eq.recOn ⋯ (Eq.recOn ⋯ ({ obj := τ, map := @PushQuiver.rec V inst✝¹ W σ (fun X Y x => τ X ⟶ τ Y) fun X Y f => id (⋯.mpr (⋯.mpr (φ.map f))) }.map f))
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : MeasurableSpace α'<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace β'<VAR>inst✝⁴ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : SFinite ν<VAR>𝕜 : Type u_7<VAR>inst✝¹ : NontriviallyNormedField 𝕜<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : α → 𝕜<VAR>g : β → E<VAR>hf : Integrable f μ<VAR>hg : Integrable g ν<GOAL>Integrable (fun z => f z.1 • g z.2) (μ.prod ν)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : MeasurableSpace α'<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace β'<VAR>inst✝⁴ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : SFinite ν<VAR>𝕜 : Type u_7<VAR>inst✝¹ : NontriviallyNormedField 𝕜<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : α → 𝕜<VAR>g : β → E<VAR>hf : Integrable f μ<VAR>hg : Integrable g ν<GOAL>AEStronglyMeasurable (fun z => f z.1 • g z.2) (μ.prod ν)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : MeasurableSpace α'<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace β'<VAR>inst✝⁴ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : SFinite ν<VAR>𝕜 : Type u_7<VAR>inst✝¹ : NontriviallyNormedField 𝕜<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : α → 𝕜<VAR>g : β → E<VAR>hf : Integrable f μ<VAR>hg : Integrable g ν<GOAL>∀ᵐ (x : α) ∂μ, Integrable (fun y => f (x, y).1 • g (x, y).2) ν
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : MeasurableSpace α'<VAR>inst✝⁶ : MeasurableSpace β<VAR>inst✝⁵ : MeasurableSpace β'<VAR>inst✝⁴ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : SFinite ν<VAR>𝕜 : Type u_7<VAR>inst✝¹ : NontriviallyNormedField 𝕜<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : α → 𝕜<VAR>g : β → E<VAR>hf : Integrable f μ<VAR>hg : Integrable g ν<GOAL>Integrable (fun x => ∫ (y : β), ‖f (x, y).1 • g (x, y).2‖ ∂ν) μ
<VAR>K : Type u_1<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>ι₁ : Type u_4<VAR>ι₂ : Type u_5<VAR>inst✝⁸ : Field K<VAR>inst✝⁷ : AddCommGroup V₁<VAR>inst✝⁶ : Module K V₁<VAR>inst✝⁵ : AddCommGroup V₂<VAR>inst✝⁴ : Module K V₂<VAR>inst✝³ : Fintype ι₁<VAR>inst✝² : Fintype ι₂<VAR>inst✝¹ : DecidableEq ι₁<VAR>inst✝ : DecidableEq ι₂<VAR>B₁ : Basis ι₁ K V₁<VAR>B₂ : Basis ι₂ K V₂<VAR>M : Matrix ι₁ ι₂ K<GOAL>(toLin B₁.dualBasis B₂.dualBasis) Mᵀ = Module.Dual.transpose ((toLin B₂ B₁) M)