ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝² : Zero M<VAR>inst✝¹ : Zero N<VAR>inst✝ : Zero P<VAR>f : M → N → P<VAR>hf : f 0 0 = 0<VAR>a : α<VAR>m : M<VAR>n : N<VAR>a' : α<GOAL>f ((single a m) a') ((single a n) a') = (single a (f m n)) a'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝² : Zero M<VAR>inst✝¹ : Zero N<VAR>inst✝ : Zero P<VAR>f : M → N → P<VAR>hf : f 0 0 = 0<VAR>a : α<VAR>m : M<VAR>n : N<GOAL>f ((single a m) a) ((single a n) a) = (single a (f m n)) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝² : Zero M<VAR>inst✝¹ : Zero N<VAR>inst✝ : Zero P<VAR>f : M → N → P<VAR>hf : f 0 0 = 0<VAR>a : α<VAR>m : M<VAR>n : N<VAR>a' : α<VAR>ha' : a ≠ a'<GOAL>f ((single a m) a') ((single a n) a') = (single a (f m n)) a'
<VAR>R S : Type u<VAR>M : Type v<VAR>M' : Type v'<VAR>M₁ : Type v<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝⁸ : Ring R<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : AddCommGroup M₁<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M₁<VAR>inst✝ : StrongRankCondition R<VAR>s : Finset M<GOAL>Module.rank R ↥(span R ↑s) ≤ ↑s.card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : BooleanRing α<VAR>a b : α<GOAL>a = -b ↔ a = b
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹² : MeasurableSpace X<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝¹¹ : TopologicalSpace X<VAR>inst✝¹⁰ : TopologicalSpace Y<VAR>inst✝⁹ : MeasurableSpace Y<VAR>inst✝⁸ : OpensMeasurableSpace Y<VAR>μ : Measure Y<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace 𝕜 G<VAR>inst✝ : NormedSpace 𝕜 E<VAR>L : F →L[𝕜] G →L[𝕜] E<VAR>f : X → Y → G<VAR>s : Set X<VAR>k : Set Y<VAR>g : Y → F<VAR>hk : IsCompact k<VAR>hf : ContinuousOn (uncurry f) (s ×ˢ univ)<VAR>hfs : ∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0<VAR>hg : IntegrableOn g k μ<GOAL>ContinuousOn (fun x => ∫ (y : Y), (L (g y)) (f x y) ∂μ) s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹² : MeasurableSpace X<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝¹¹ : TopologicalSpace X<VAR>inst✝¹⁰ : TopologicalSpace Y<VAR>inst✝⁹ : MeasurableSpace Y<VAR>inst✝⁸ : OpensMeasurableSpace Y<VAR>μ : Measure Y<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace 𝕜 G<VAR>inst✝ : NormedSpace 𝕜 E<VAR>L : F →L[𝕜] G →L[𝕜] E<VAR>f : X → Y → G<VAR>s : Set X<VAR>k : Set Y<VAR>g : Y → F<VAR>hk : IsCompact k<VAR>hf : ContinuousOn (uncurry f) (s ×ˢ univ)<VAR>hfs : ∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0<VAR>hg : IntegrableOn g k μ<VAR>A : ∀ p ∈ s, Continuous (f p)<GOAL>ContinuousOn (fun x => ∫ (y : Y), (L (g y)) (f x y) ∂μ) s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹² : MeasurableSpace X<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝¹¹ : TopologicalSpace X<VAR>inst✝¹⁰ : TopologicalSpace Y<VAR>inst✝⁹ : MeasurableSpace Y<VAR>inst✝⁸ : OpensMeasurableSpace Y<VAR>μ : Measure Y<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace 𝕜 G<VAR>inst✝ : NormedSpace 𝕜 E<VAR>L : F →L[𝕜] G →L[𝕜] E<VAR>f : X → Y → G<VAR>s : Set X<VAR>k : Set Y<VAR>g : Y → F<VAR>hk : IsCompact k<VAR>hf : ContinuousOn (uncurry f) (s ×ˢ univ)<VAR>hfs : ∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0<VAR>hg : IntegrableOn g k μ<VAR>A : ∀ p ∈ s, Continuous (f p)<VAR>q : X<VAR>hq : q ∈ s<GOAL>ContinuousWithinAt (fun x => ∫ (y : Y), (L (g y)) (f x y) ∂μ) s q
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹² : MeasurableSpace X<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝¹¹ : TopologicalSpace X<VAR>inst✝¹⁰ : TopologicalSpace Y<VAR>inst✝⁹ : MeasurableSpace Y<VAR>inst✝⁸ : OpensMeasurableSpace Y<VAR>μ : Measure Y<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace 𝕜 G<VAR>inst✝ : NormedSpace 𝕜 E<VAR>L : F →L[𝕜] G →L[𝕜] E<VAR>f : X → Y → G<VAR>s : Set X<VAR>k : Set Y<VAR>g : Y → F<VAR>hk : IsCompact k<VAR>hf : ContinuousOn (uncurry f) (s ×ˢ univ)<VAR>hfs : ∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0<VAR>hg : IntegrableOn g k μ<VAR>A : ∀ p ∈ s, Continuous (f p)<VAR>q : X<VAR>hq : q ∈ s<VAR>ε : ℝ<VAR>εpos : ε > 0<GOAL>∀ᶠ (x : X) in 𝓝[s] q, dist (∫ (y : Y), (L (g y)) (f x y) ∂μ) (∫ (y : Y), (L (g y)) (f q y) ∂μ) < ε
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹² : MeasurableSpace X<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝¹¹ : TopologicalSpace X<VAR>inst✝¹⁰ : TopologicalSpace Y<VAR>inst✝⁹ : MeasurableSpace Y<VAR>inst✝⁸ : OpensMeasurableSpace Y<VAR>μ : Measure Y<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace 𝕜 G<VAR>inst✝ : NormedSpace 𝕜 E<VAR>L : F →L[𝕜] G →L[𝕜] E<VAR>f : X → Y → G<VAR>s : Set X<VAR>k : Set Y<VAR>g : Y → F<VAR>hk : IsCompact k<VAR>hf : ContinuousOn (uncurry f) (s ×ˢ univ)<VAR>hfs : ∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0<VAR>hg : IntegrableOn g k μ<VAR>A : ∀ p ∈ s, Continuous (f p)<VAR>q : X<VAR>hq : q ∈ s<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>δ : ℝ<VAR>δpos : 0 < δ<VAR>hδ : ∫ (x : Y) in k, ‖L‖ * ‖g x‖ * δ ∂μ < ε<GOAL>∀ᶠ (x : X) in 𝓝[s] q, dist (∫ (y : Y), (L (g y)) (f x y) ∂μ) (∫ (y : Y), (L (g y)) (f q y) ∂μ) < ε
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹² : MeasurableSpace X<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝¹¹ : TopologicalSpace X<VAR>inst✝¹⁰ : TopologicalSpace Y<VAR>inst✝⁹ : MeasurableSpace Y<VAR>inst✝⁸ : OpensMeasurableSpace Y<VAR>μ : Measure Y<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace 𝕜 G<VAR>inst✝ : NormedSpace 𝕜 E<VAR>L : F →L[𝕜] G →L[𝕜] E<VAR>f : X → Y → G<VAR>s : Set X<VAR>k : Set Y<VAR>g : Y → F<VAR>hk : IsCompact k<VAR>hf : ContinuousOn (uncurry f) (s ×ˢ univ)<VAR>hfs : ∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0<VAR>hg : IntegrableOn g k μ<VAR>A : ∀ p ∈ s, Continuous (f p)<VAR>q : X<VAR>hq : q ∈ s<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>δ : ℝ<VAR>δpos : 0 < δ<VAR>hδ : ∫ (x : Y) in k, ‖L‖ * ‖g x‖ * δ ∂μ < ε<VAR>v : Set X<VAR>v_mem : v ∈ 𝓝[s] q<VAR>hv : ∀ p ∈ v, ∀ x ∈ k, dist (f p x) (f q x) < δ<GOAL>∀ᶠ (x : X) in 𝓝[s] q, dist (∫ (y : Y), (L (g y)) (f x y) ∂μ) (∫ (y : Y), (L (g y)) (f q y) ∂μ) < ε
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹² : MeasurableSpace X<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝¹¹ : TopologicalSpace X<VAR>inst✝¹⁰ : TopologicalSpace Y<VAR>inst✝⁹ : MeasurableSpace Y<VAR>inst✝⁸ : OpensMeasurableSpace Y<VAR>μ : Measure Y<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace 𝕜 G<VAR>inst✝ : NormedSpace 𝕜 E<VAR>L : F →L[𝕜] G →L[𝕜] E<VAR>f : X → Y → G<VAR>s : Set X<VAR>k : Set Y<VAR>g : Y → F<VAR>hk : IsCompact k<VAR>hf : ContinuousOn (uncurry f) (s ×ˢ univ)<VAR>hfs : ∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0<VAR>hg : IntegrableOn g k μ<VAR>A : ∀ p ∈ s, Continuous (f p)<VAR>q : X<VAR>hq : q ∈ s<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>δ : ℝ<VAR>δpos : 0 < δ<VAR>hδ : ∫ (x : Y) in k, ‖L‖ * ‖g x‖ * δ ∂μ < ε<VAR>v : Set X<VAR>v_mem : v ∈ 𝓝[s] q<VAR>hv : ∀ p ∈ v, ∀ x ∈ k, ‖f p x - f q x‖ < δ<VAR>I : ∀ p ∈ s, IntegrableOn (fun y => (L (g y)) (f p y)) k μ<GOAL>∀ᶠ (x : X) in 𝓝[s] q, ‖∫ (y : Y), (L (g y)) (f x y) ∂μ - ∫ (y : Y), (L (g y)) (f q y) ∂μ‖ < ε
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝¹² : MeasurableSpace X<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝¹¹ : TopologicalSpace X<VAR>inst✝¹⁰ : TopologicalSpace Y<VAR>inst✝⁹ : MeasurableSpace Y<VAR>inst✝⁸ : OpensMeasurableSpace Y<VAR>μ : Measure Y<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace 𝕜 G<VAR>inst✝ : NormedSpace 𝕜 E<VAR>L : F →L[𝕜] G →L[𝕜] E<VAR>f : X → Y → G<VAR>s : Set X<VAR>k : Set Y<VAR>g : Y → F<VAR>hk : IsCompact k<VAR>hf : ContinuousOn (uncurry f) (s ×ˢ univ)<VAR>hfs : ∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0<VAR>hg : IntegrableOn g k μ<VAR>A : ∀ p ∈ s, Continuous (f p)<VAR>q : X<VAR>hq : q ∈ s<VAR>ε : ℝ<VAR>εpos : ε > 0<VAR>δ : ℝ<VAR>δpos : 0 < δ<VAR>hδ : ∫ (x : Y) in k, ‖L‖ * ‖g x‖ * δ ∂μ < ε<VAR>v : Set X<VAR>v_mem : v ∈ 𝓝[s] q<VAR>hv : ∀ p ∈ v, ∀ x ∈ k, ‖f p x - f q x‖ < δ<VAR>I : ∀ p ∈ s, IntegrableOn (fun y => (L (g y)) (f p y)) k μ<VAR>p : X<VAR>hp : p ∈ v<VAR>h'p : p ∈ s<GOAL>‖∫ (y : Y), (L (g y)) (f p y) ∂μ - ∫ (y : Y), (L (g y)) (f q y) ∂μ‖ < ε
<VAR>G : Type w<VAR>H : Type x<VAR>α✝ : Type u<VAR>β✝ : Type v<VAR>inst✝¹ : Group α✝<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : TopologicalSpace α<VAR>inst✝ : Group β<VAR>f : α → β<GOAL>Continuous f
<VAR>G : Type w<VAR>H : Type x<VAR>α✝ : Type u<VAR>β✝ : Type v<VAR>inst✝¹ : Group α✝<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : TopologicalSpace α<VAR>inst✝ : Group β<VAR>f : α → β<GOAL>∀ t_1 ∈ toTopologicalSpace '' {b | TopologicalSpace.coinduced f t ≤ b.toTopologicalSpace}, Continuous f
<VAR>G : Type w<VAR>H : Type x<VAR>α✝ : Type u<VAR>β✝ : Type v<VAR>inst✝¹ : Group α✝<VAR>α : Type u_1<VAR>β : Type u_2<VAR>t : TopologicalSpace α<VAR>inst✝ : Group β<VAR>f : α → β<VAR>t' : GroupTopology β<VAR>ht' : t' ∈ {b | TopologicalSpace.coinduced f t ≤ b.toTopologicalSpace}<GOAL>Continuous f
<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✝¹⁷ : CommSemiring R<VAR>inst✝¹⁶ : AddCommMonoid N₂<VAR>inst✝¹⁵ : Module R N₂<VAR>inst✝¹⁴ : Semiring R₁<VAR>inst✝¹³ : Semiring R₂<VAR>inst✝¹² : SMulCommClass R R N₂<VAR>inst✝¹¹ : Semiring S₁<VAR>inst✝¹⁰ : Semiring S₂<VAR>inst✝⁹ : Module S₁ N₂<VAR>inst✝⁸ : Module S₂ N₂<VAR>inst✝⁷ : SMulCommClass S₁ R N₂<VAR>inst✝⁶ : SMulCommClass S₂ R N₂<VAR>inst✝⁵ : SMulCommClass S₂ S₁ N₂<VAR>σ₁ : R₁ →+* S₁<VAR>σ₂ : R₂ →+* S₂<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : Fintype m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : DecidableEq m<VAR>T : Type u_17<VAR>inst✝ : CommSemiring T<VAR>M : Matrix n m T<VAR>v : n → T<VAR>w : m → T<GOAL>(((toLinearMap₂' T) M) v) w = v ⬝ᵥ M *ᵥ w
<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✝¹⁷ : CommSemiring R<VAR>inst✝¹⁶ : AddCommMonoid N₂<VAR>inst✝¹⁵ : Module R N₂<VAR>inst✝¹⁴ : Semiring R₁<VAR>inst✝¹³ : Semiring R₂<VAR>inst✝¹² : SMulCommClass R R N₂<VAR>inst✝¹¹ : Semiring S₁<VAR>inst✝¹⁰ : Semiring S₂<VAR>inst✝⁹ : Module S₁ N₂<VAR>inst✝⁸ : Module S₂ N₂<VAR>inst✝⁷ : SMulCommClass S₁ R N₂<VAR>inst✝⁶ : SMulCommClass S₂ R N₂<VAR>inst✝⁵ : SMulCommClass S₂ S₁ N₂<VAR>σ₁ : R₁ →+* S₁<VAR>σ₂ : R₂ →+* S₂<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : Fintype m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : DecidableEq m<VAR>T : Type u_17<VAR>inst✝ : CommSemiring T<VAR>M : Matrix n m T<VAR>v : n → T<VAR>w : m → T<GOAL>∑ i : n, ∑ j : m, v i •> w j •> M i j = ∑ x : n, v x * ∑ x_1 : m, M x x_1 * w x_1
<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✝¹⁷ : CommSemiring R<VAR>inst✝¹⁶ : AddCommMonoid N₂<VAR>inst✝¹⁵ : Module R N₂<VAR>inst✝¹⁴ : Semiring R₁<VAR>inst✝¹³ : Semiring R₂<VAR>inst✝¹² : SMulCommClass R R N₂<VAR>inst✝¹¹ : Semiring S₁<VAR>inst✝¹⁰ : Semiring S₂<VAR>inst✝⁹ : Module S₁ N₂<VAR>inst✝⁸ : Module S₂ N₂<VAR>inst✝⁷ : SMulCommClass S₁ R N₂<VAR>inst✝⁶ : SMulCommClass S₂ R N₂<VAR>inst✝⁵ : SMulCommClass S₂ S₁ N₂<VAR>σ₁ : R₁ →+* S₁<VAR>σ₂ : R₂ →+* S₂<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : Fintype m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : DecidableEq m<VAR>T : Type u_17<VAR>inst✝ : CommSemiring T<VAR>M : Matrix n m T<VAR>v : n → T<VAR>w : m → T<VAR>x✝¹ : n<VAR>x✝ : x✝¹ ∈ univ<GOAL>∑ j : m, v x✝¹ •> w j •> M x✝¹ j = v x✝¹ * ∑ x : m, M x✝¹ x * w x
<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✝¹⁷ : CommSemiring R<VAR>inst✝¹⁶ : AddCommMonoid N₂<VAR>inst✝¹⁵ : Module R N₂<VAR>inst✝¹⁴ : Semiring R₁<VAR>inst✝¹³ : Semiring R₂<VAR>inst✝¹² : SMulCommClass R R N₂<VAR>inst✝¹¹ : Semiring S₁<VAR>inst✝¹⁰ : Semiring S₂<VAR>inst✝⁹ : Module S₁ N₂<VAR>inst✝⁸ : Module S₂ N₂<VAR>inst✝⁷ : SMulCommClass S₁ R N₂<VAR>inst✝⁶ : SMulCommClass S₂ R N₂<VAR>inst✝⁵ : SMulCommClass S₂ S₁ N₂<VAR>σ₁ : R₁ →+* S₁<VAR>σ₂ : R₂ →+* S₂<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : Fintype m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : DecidableEq m<VAR>T : Type u_17<VAR>inst✝ : CommSemiring T<VAR>M : Matrix n m T<VAR>v : n → T<VAR>w : m → T<VAR>x✝¹ : n<VAR>x✝ : x✝¹ ∈ univ<GOAL>∑ j : m, v x✝¹ •> w j •> M x✝¹ j = ∑ i : m, v x✝¹ * (M x✝¹ i * w i)
<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✝¹⁷ : CommSemiring R<VAR>inst✝¹⁶ : AddCommMonoid N₂<VAR>inst✝¹⁵ : Module R N₂<VAR>inst✝¹⁴ : Semiring R₁<VAR>inst✝¹³ : Semiring R₂<VAR>inst✝¹² : SMulCommClass R R N₂<VAR>inst✝¹¹ : Semiring S₁<VAR>inst✝¹⁰ : Semiring S₂<VAR>inst✝⁹ : Module S₁ N₂<VAR>inst✝⁸ : Module S₂ N₂<VAR>inst✝⁷ : SMulCommClass S₁ R N₂<VAR>inst✝⁶ : SMulCommClass S₂ R N₂<VAR>inst✝⁵ : SMulCommClass S₂ S₁ N₂<VAR>σ₁ : R₁ →+* S₁<VAR>σ₂ : R₂ →+* S₂<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : Fintype m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : DecidableEq m<VAR>T : Type u_17<VAR>inst✝ : CommSemiring T<VAR>M : Matrix n m T<VAR>v : n → T<VAR>w : m → T<VAR>x✝³ : n<VAR>x✝² : x✝³ ∈ univ<VAR>x✝¹ : m<VAR>x✝ : x✝¹ ∈ univ<GOAL>v x✝³ •> w x✝¹ •> M x✝³ x✝¹ = v x✝³ * (M x✝³ x✝¹ * w x✝¹)
<VAR>α : Type u<VAR>β : Type v<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>as : List α<GOAL>indexesValues (fun b => decide (p b)) as = filter ((fun b => decide (p b)) ∘ Prod.snd) as.enum
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>a✝ a b c : α<VAR>h : c < 0<GOAL>(fun x => x * c) ⁻¹' Ico a b = Ioc (b / c) (a / c)
<VAR>o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}<VAR>ho : o ≠ 0<VAR>H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)<VAR>a : Ordinal.{max v u}<VAR>b : Ordinal.{max u v}<VAR>h : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi b < o.nfpBFamily f a<GOAL>b < o.nfpBFamily f a
<VAR>o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}<VAR>ho : o ≠ 0<VAR>H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)<VAR>a : Ordinal.{max v u}<VAR>b : Ordinal.{max u v}<VAR>h : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi b < o.nfpBFamily f a<VAR>this : Nonempty (Quotient.out o).α<GOAL>b < o.nfpBFamily f a
<VAR>o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}<VAR>ho : o ≠ 0<VAR>H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)<VAR>a : Ordinal.{max v u}<VAR>b : Ordinal.{max u v}<VAR>h : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi b < o.nfpBFamily f a<VAR>this : Nonempty (Quotient.out o).α<GOAL>∀ (i : (Quotient.out o).α), IsNormal (o.familyOfBFamily f i)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x y z : X<VAR>s✝ : Set X<VAR>f g : X → Y<VAR>t : Set (SeparationQuotient X)<VAR>hf : ∀ (x y : X), (x ~ᵢ y) → f x = f y<VAR>s : Set (SeparationQuotient X)<GOAL>ContinuousOn (lift f hf) s ↔ ContinuousOn f (mk ⁻¹' s)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : SimplicialObject C<VAR>n : ℕ<VAR>i : Fin (n + 1)<GOAL>X.σ i ≫ X.δ i.castSucc = 𝟙 (X _[n])
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n✝ l : ℕ<VAR>φ✝ ψ : L.BoundedFormula α l<VAR>θ : L.BoundedFormula α l.succ<VAR>v✝ : α → M<VAR>xs✝ : Fin l → M<VAR>m n : ℕ<VAR>φ : L.BoundedFormula α n<VAR>g : α → β ⊕ Fin m<VAR>v : β → M<VAR>xs : Fin (m + n) → M<GOAL>(relabel g φ).Realize v xs ↔ φ.Realize (Sum.elim v (xs ∘ castAdd n) ∘ g) (xs ∘ natAdd m)
<VAR>R : Type u<VAR>inst✝⁷ : Ring R<VAR>Q : Type v<VAR>inst✝⁶ : AddCommGroup Q<VAR>inst✝⁵ : Module R Q<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R N<VAR>i : M →ₗ[R] N<VAR>f : M →ₗ[R] Q<VAR>inst✝ : Fact (Function.Injective ⇑i)<VAR>h : Baer R Q<VAR>y : N<VAR>x : ↥(extensionOfMax i f).domain<VAR>x' : ↥(extensionOfMaxAdjoin i f h y).domain<VAR>EQ : ↑x = ↑x'<GOAL>ExtensionOfMaxAdjoin.extensionToFun i f h x' = ↑(extensionOfMax i f).toLinearPMap x
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<VAR>h : H.IsComplement' K<GOAL>IsCompl H K
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<VAR>h : H.IsComplement' K<VAR>g : G<VAR>x✝ : g ∈ ⊤<GOAL>g ∈ H ⊔ K
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<VAR>h✝ : H.IsComplement' K<VAR>h : ↑↑H<VAR>k : ↑↑K<VAR>x✝ : (fun x => ↑x.1 * ↑x.2) (h, k) ∈ ⊤<GOAL>(fun x => ↑x.1 * ↑x.2) (h, k) ∈ H ⊔ K
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>A : C ⥤ Type w<VAR>I : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} I<VAR>inst✝² : Small.{w, u₁} I<VAR>F : I ⥤ A.Elements<VAR>inst✝¹ : HasLimitsOfShape I C<VAR>inst✝ : PreservesLimitsOfShape I A<VAR>c : Cone F<GOAL>A.map (limit.lift (F ⋙ π A) ((π A).mapCone c)) c.pt.snd = liftedConeElement F
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>A : C ⥤ Type w<VAR>I : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} I<VAR>inst✝² : Small.{w, u₁} I<VAR>F : I ⥤ A.Elements<VAR>inst✝¹ : HasLimitsOfShape I C<VAR>inst✝ : PreservesLimitsOfShape I A<VAR>c : Cone F<GOAL>(preservesLimitIso A (F ⋙ π A)).toEquiv (A.map (limit.lift (F ⋙ π A) ((π A).mapCone c)) c.pt.snd) = (preservesLimitIso A (F ⋙ π A)).toEquiv (liftedConeElement F)
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>A : C ⥤ Type w<VAR>I : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} I<VAR>inst✝² : Small.{w, u₁} I<VAR>F : I ⥤ A.Elements<VAR>inst✝¹ : HasLimitsOfShape I C<VAR>inst✝ : PreservesLimitsOfShape I A<VAR>c : Cone F<VAR>i : I<GOAL>limit.π ((F ⋙ π A) ⋙ A) i ((preservesLimitIso A (F ⋙ π A)).toEquiv (A.map (limit.lift (F ⋙ π A) ((π A).mapCone c)) c.pt.snd)) = limit.π ((F ⋙ π A) ⋙ A) i ((preservesLimitIso A (F ⋙ π A)).toEquiv (liftedConeElement F))
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>A : C ⥤ Type w<VAR>I : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} I<VAR>inst✝² : Small.{w, u₁} I<VAR>F : I ⥤ A.Elements<VAR>inst✝¹ : HasLimitsOfShape I C<VAR>inst✝ : PreservesLimitsOfShape I A<VAR>c : Cone F<VAR>i : I<VAR>h₁ : ((preservesLimitIso A (F ⋙ π A)).hom ≫ limit.π ((F ⋙ π A) ⋙ A) i) (A.map (limit.lift (F ⋙ π A) ((π A).mapCone c)) c.pt.snd) = A.map (limit.π (F ⋙ π A) i) (A.map (limit.lift (F ⋙ π A) ((π A).mapCone c)) c.pt.snd)<GOAL>limit.π ((F ⋙ π A) ⋙ A) i ((preservesLimitIso A (F ⋙ π A)).toEquiv (A.map (limit.lift (F ⋙ π A) ((π A).mapCone c)) c.pt.snd)) = limit.π ((F ⋙ π A) ⋙ A) i ((preservesLimitIso A (F ⋙ π A)).toEquiv (liftedConeElement F))
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>A : C ⥤ Type w<VAR>I : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} I<VAR>inst✝² : Small.{w, u₁} I<VAR>F : I ⥤ A.Elements<VAR>inst✝¹ : HasLimitsOfShape I C<VAR>inst✝ : PreservesLimitsOfShape I A<VAR>c : Cone F<VAR>i : I<VAR>h₁ : ((preservesLimitIso A (F ⋙ π A)).hom ≫ limit.π ((F ⋙ π A) ⋙ A) i) (A.map (limit.lift (F ⋙ π A) ((π A).mapCone c)) c.pt.snd) = A.map (limit.π (F ⋙ π A) i) (A.map (limit.lift (F ⋙ π A) ((π A).mapCone c)) c.pt.snd)<VAR>h₂ : A.map (↑(c.π.app i)) (((Functor.const I).obj c.pt).obj i).snd = (F.obj i).snd<GOAL>limit.π ((F ⋙ π A) ⋙ A) i ((preservesLimitIso A (F ⋙ π A)).toEquiv (A.map (limit.lift (F ⋙ π A) ((π A).mapCone c)) c.pt.snd)) = limit.π ((F ⋙ π A) ⋙ A) i ((preservesLimitIso A (F ⋙ π A)).toEquiv (liftedConeElement F))
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<GOAL>HasDerivAt f f' x ↔ Tendsto (fun t => t⁻¹ • (f (x + t) - f x)) (𝓝[≠] 0) (𝓝 f')
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>this : 𝓝[≠] x = map (fun t => x + t) (𝓝[≠] 0)<GOAL>HasDerivAt f f' x ↔ Tendsto (fun t => t⁻¹ • (f (x + t) - f x)) (𝓝[≠] 0) (𝓝 f')
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P<VAR>X Y Z : Scheme<VAR>e : X ≅ Y<VAR>f : Y ⟶ Z<VAR>hf : stalkwise (fun {R S} [CommRing R] [CommRing S] => P) f<GOAL>stalkwise (fun {R S} [CommRing R] [CommRing S] => P) (e.hom ≫ f)
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P<VAR>X Y Z : Scheme<VAR>e : X ≅ Y<VAR>f : Y ⟶ Z<VAR>hf : stalkwise (fun {R S} [CommRing R] [CommRing S] => P) f<GOAL>∀ (x : ↑↑X.toPresheafedSpace), P (Scheme.Hom.stalkMap (e.hom ≫ f) x)
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P<VAR>X Y Z : Scheme<VAR>e : X ≅ Y<VAR>f : Y ⟶ Z<VAR>hf : stalkwise (fun {R S} [CommRing R] [CommRing S] => P) f<VAR>x : ↑↑X.toPresheafedSpace<GOAL>P (Scheme.Hom.stalkMap (e.hom ≫ f) x)
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P<VAR>X Y Z : Scheme<VAR>e : X ≅ Y<VAR>f : Y ⟶ Z<VAR>hf : stalkwise (fun {R S} [CommRing R] [CommRing S] => P) f<VAR>x : ↑↑X.toPresheafedSpace<GOAL>P (Scheme.Hom.stalkMap f (e.hom.val.base x) ≫ Scheme.Hom.stalkMap e.hom x)