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>ι✝ : Sort y<VAR>s t u : Set α<VAR>inst✝¹ : MeasurableSpace α<VAR>ι : Type u_5<VAR>inst✝ : Countable ι<VAR>f : ι → α → ℝ≥0∞<VAR>h : ∀ (i : ι), Measurable (f i)<GOAL>Measurable (∑' (i : ι), f i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι✝ : Sort y<VAR>s t u : Set α<VAR>inst✝¹ : MeasurableSpace α<VAR>ι : Type u_5<VAR>inst✝ : Countable ι<VAR>f : ι → α → ℝ≥0∞<VAR>h : ∀ (i : ι), Measurable (f i)<VAR>x : α<GOAL>tsum (fun i => f i) x = ∑' (i : ι), f i x
<VAR>α : Type u<VAR>a✝ : α<VAR>inst✝⁵ : Group α<VAR>inst✝⁴ : DecidableEq α<VAR>inst✝³ : Fintype α<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : Fintype G<VAR>inst✝ : IsCyclic G<VAR>d : ℕ<VAR>a b : ZMod d<VAR>hGcard : Fintype.card G = d<VAR>h : ∀ (t : G), t ^ a.val = t ^ b.val<GOAL>a = b
<VAR>α : Type u<VAR>a✝ : α<VAR>inst✝⁵ : Group α<VAR>inst✝⁴ : DecidableEq α<VAR>inst✝³ : Fintype α<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : Fintype G<VAR>inst✝ : IsCyclic G<VAR>d : ℕ<VAR>a b : ZMod d<VAR>hGcard : Fintype.card G = d<VAR>h : ∀ (t : G), t ^ a.val = t ^ b.val<VAR>g : G<VAR>hg : ∀ (x : G), x ∈ zpowers g<GOAL>a = b
<VAR>α : Type u<VAR>a✝ : α<VAR>inst✝⁵ : Group α<VAR>inst✝⁴ : DecidableEq α<VAR>inst✝³ : Fintype α<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : Fintype G<VAR>inst✝ : IsCyclic G<VAR>g : G<VAR>hg : ∀ (x : G), x ∈ zpowers g<VAR>a b : ZMod (Fintype.card G)<VAR>h : g ^ a.val = g ^ b.val<GOAL>a = b
<VAR>α : Type u<VAR>a✝ : α<VAR>inst✝⁵ : Group α<VAR>inst✝⁴ : DecidableEq α<VAR>inst✝³ : Fintype α<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : Fintype G<VAR>inst✝ : IsCyclic G<VAR>g : G<VAR>hg : ∀ (x : G), x ∈ zpowers g<VAR>a b : ZMod (Fintype.card G)<VAR>h : ↑a.val = ↑b.val<GOAL>a = b
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝³ : LinearOrderedField R<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module R V<VAR>inst✝ : AddTorsor V P<VAR>x y : P<VAR>h✝ : x ≠ y<VAR>h : midpoint R x y ≠ x<GOAL>Sbtw R x (midpoint R x y) y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝³ : LinearOrderedField R<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module R V<VAR>inst✝ : AddTorsor V P<VAR>x y : P<VAR>h✝ : x ≠ y<VAR>h : midpoint R x y ≠ x<GOAL>y = (pointReflection R (midpoint R x y)) x
<VAR>R : Type uR<VAR>M₁ : Type uM₁<VAR>M₂ : Type uM₂<VAR>M₃ : Type uM₃<VAR>M₄ : Type uM₄<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : AddCommGroup M₁<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✝¹ : Module R M₄<VAR>inst✝ : Invertible 2<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>Q₃ : QuadraticForm R M₃<VAR>Q₄ : QuadraticForm R M₄<VAR>f : Q₁ →qᵢ Q₂<VAR>g : Q₃ →qᵢ Q₄<GOAL>comp (Q₂.tmul Q₄) (TensorProduct.map f.toLinearMap g.toLinearMap) = Q₁.tmul Q₃
<VAR>R : Type uR<VAR>M₁ : Type uM₁<VAR>M₂ : Type uM₂<VAR>M₃ : Type uM₃<VAR>M₄ : Type uM₄<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : AddCommGroup M₁<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✝¹ : Module R M₄<VAR>inst✝ : Invertible 2<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>Q₃ : QuadraticForm R M₃<VAR>Q₄ : QuadraticForm R M₄<VAR>f : Q₁ →qᵢ Q₂<VAR>g : Q₃ →qᵢ Q₄<VAR>h₁ : Q₁ = comp Q₂ f.toLinearMap<GOAL>comp (Q₂.tmul Q₄) (TensorProduct.map f.toLinearMap g.toLinearMap) = Q₁.tmul Q₃
<VAR>R : Type uR<VAR>M₁ : Type uM₁<VAR>M₂ : Type uM₂<VAR>M₃ : Type uM₃<VAR>M₄ : Type uM₄<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : AddCommGroup M₁<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✝¹ : Module R M₄<VAR>inst✝ : Invertible 2<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>Q₃ : QuadraticForm R M₃<VAR>Q₄ : QuadraticForm R M₄<VAR>f : Q₁ →qᵢ Q₂<VAR>g : Q₃ →qᵢ Q₄<VAR>h₁ : Q₁ = comp Q₂ f.toLinearMap<VAR>h₃ : Q₃ = comp Q₄ g.toLinearMap<GOAL>comp (Q₂.tmul Q₄) (TensorProduct.map f.toLinearMap g.toLinearMap) = Q₁.tmul Q₃
<VAR>R : Type uR<VAR>M₁ : Type uM₁<VAR>M₂ : Type uM₂<VAR>M₃ : Type uM₃<VAR>M₄ : Type uM₄<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : AddCommGroup M₁<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✝¹ : Module R M₄<VAR>inst✝ : Invertible 2<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>Q₃ : QuadraticForm R M₃<VAR>Q₄ : QuadraticForm R M₄<VAR>f : Q₁ →qᵢ Q₂<VAR>g : Q₃ →qᵢ Q₄<VAR>h₁ : Q₁ = comp Q₂ f.toLinearMap<VAR>h₃ : Q₃ = comp Q₄ g.toLinearMap<GOAL>(associatedHom R) (comp (Q₂.tmul Q₄) (TensorProduct.map f.toLinearMap g.toLinearMap)) = (associatedHom R) (Q₁.tmul Q₃)
<VAR>R : Type uR<VAR>M₁ : Type uM₁<VAR>M₂ : Type uM₂<VAR>M₃ : Type uM₃<VAR>M₄ : Type uM₄<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : AddCommGroup M₁<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✝¹ : Module R M₄<VAR>inst✝ : Invertible 2<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>Q₃ : QuadraticForm R M₃<VAR>Q₄ : QuadraticForm R M₄<VAR>f : Q₁ →qᵢ Q₂<VAR>g : Q₃ →qᵢ Q₄<VAR>h₁ : Q₁ = comp Q₂ f.toLinearMap<VAR>h₃ : Q₃ = comp Q₄ g.toLinearMap<VAR>m₁ : M₁<VAR>m₃ : M₃<VAR>m₁' : M₁<VAR>m₃' : M₃<GOAL>((TensorProduct.AlgebraTensorModule.curry (((TensorProduct.AlgebraTensorModule.curry ((associatedHom R) (comp (Q₂.tmul Q₄) (TensorProduct.map f.toLinearMap g.toLinearMap)))) m₁) m₃)) m₁') m₃' = ((TensorProduct.AlgebraTensorModule.curry (((TensorProduct.AlgebraTensorModule.curry ((associatedHom R) (Q₁.tmul Q₃))) m₁) m₃)) m₁') m₃'
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>ι : Type u_4<VAR>v : ι → E<VAR>hv : Orthonormal 𝕜 v<VAR>s : Set ι<VAR>i : ι<VAR>hi : i ∉ s<VAR>l : ι →₀ 𝕜<VAR>hl : l ∈ Finsupp.supported 𝕜 𝕜 s<GOAL>⟪(Finsupp.total ι E 𝕜 v) l, v i⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>ι : Type u_4<VAR>v : ι → E<VAR>hv : Orthonormal 𝕜 v<VAR>s : Set ι<VAR>i : ι<VAR>hi : i ∉ s<VAR>l : ι →₀ 𝕜<VAR>hl : ∀ x ∉ s, l x = 0<GOAL>⟪(Finsupp.total ι E 𝕜 v) l, v i⟫_𝕜 = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>seq : ℕ → Set β<VAR>hseq : Antitone seq<VAR>hseq_iInter : ⋂ i, seq i = ∅<VAR>hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)<GOAL>∀ᵐ (x : γ) ∂ν a, Tendsto (fun m => κ.density ν a x (seq m)) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>seq : ℕ → Set β<VAR>hseq : Antitone seq<VAR>hseq_iInter : ⋂ i, seq i = ∅<VAR>hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)<GOAL>∀ (n : ℕ), Integrable (fun x => κ.density ν a x (seq n)) (ν a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>seq : ℕ → Set β<VAR>hseq : Antitone seq<VAR>hseq_iInter : ⋂ i, seq i = ∅<VAR>hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)<GOAL>Tendsto (fun i => ∫ (a_1 : γ), κ.density ν a a_1 (seq i) ∂ν a) atTop (𝓝 (∫ (a : γ), 0 ∂ν a))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>seq : ℕ → Set β<VAR>hseq : Antitone seq<VAR>hseq_iInter : ⋂ i, seq i = ∅<VAR>hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)<GOAL>∀ᵐ (a_1 : γ) ∂ν a, Antitone fun i => κ.density ν a a_1 (seq i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝¹ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>inst✝ : IsFiniteKernel ν<VAR>a : α<VAR>seq : ℕ → Set β<VAR>hseq : Antitone seq<VAR>hseq_iInter : ⋂ i, seq i = ∅<VAR>hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)<GOAL>∀ᵐ (a_1 : γ) ∂ν a, ∀ (i : ℕ), 0 ≤ κ.density ν a a_1 (seq i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b₁✝ b₁ : α<VAR>h : (fun b => s(a, b)) b₁✝ = (fun b => s(a, b)) b₁<GOAL>b₁✝ = b₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b₁✝ b₁ : α<VAR>h : b₁✝ = b₁ ∨ a = b₁ ∧ b₁✝ = a<GOAL>b₁✝ = b₁
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : FiniteDimensional ℝ E<VAR>inst✝⁵ : MeasurableSpace E<VAR>inst✝⁴ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f✝ g : E → ℝ<VAR>s : Set E<VAR>μ : Measure E<VAR>inst✝¹ : μ.IsAddHaarMeasure<VAR>inst✝ : FiniteDimensional ℝ F<VAR>f : E → F<VAR>hf : LipschitzOnWith C f s<VAR>A : F ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ F) → ℝ<GOAL>∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ f s x
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : FiniteDimensional ℝ E<VAR>inst✝⁵ : MeasurableSpace E<VAR>inst✝⁴ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f✝ g : E → ℝ<VAR>s : Set E<VAR>μ : Measure E<VAR>inst✝¹ : μ.IsAddHaarMeasure<VAR>inst✝ : FiniteDimensional ℝ F<VAR>f : E → F<VAR>hf : LipschitzOnWith C f s<VAR>A : F ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ F) → ℝ<GOAL>∀ᵐ (x : E) ∂μ, x ∈ s → DifferentiableWithinAt ℝ (⇑A ∘ f) s x
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : FiniteDimensional ℝ E<VAR>inst✝⁵ : MeasurableSpace E<VAR>inst✝⁴ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f✝ g : E → ℝ<VAR>s : Set E<VAR>μ : Measure E<VAR>inst✝¹ : μ.IsAddHaarMeasure<VAR>inst✝ : FiniteDimensional ℝ F<VAR>f : E → F<VAR>hf : LipschitzOnWith C f s<VAR>A : F ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ F) → ℝ<GOAL>LipschitzOnWith ?C (⇑A ∘ f) s
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : FiniteDimensional ℝ E<VAR>inst✝⁵ : MeasurableSpace E<VAR>inst✝⁴ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f✝ g : E → ℝ<VAR>s : Set E<VAR>μ : Measure E<VAR>inst✝¹ : μ.IsAddHaarMeasure<VAR>inst✝ : FiniteDimensional ℝ F<VAR>f : E → F<VAR>hf : LipschitzOnWith C f s<VAR>A : F ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ F) → ℝ<GOAL>ℝ≥0
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ φ' : S₁ ⟶ S₂<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<GOAL>leftHomologyMap' (φ - φ') h₁ h₂ = leftHomologyMap' φ h₁ h₂ - leftHomologyMap' φ' h₁ h₂
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R✝ : Type u_2<VAR>K : Type u_3<VAR>M✝ : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M✝<VAR>inst✝¹⁰ : Ring R✝<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>a✝ b✝ : R✝<VAR>x✝ y✝ : M✝<VAR>R : Type u_8<VAR>M : Type u_9<VAR>inst✝³ : CommRing R<VAR>inst✝² : NoZeroDivisors R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>x y : M<VAR>h : LinearIndependent R ![x, y]<VAR>a b c d : R<VAR>h' : a * d - b * c ≠ 0<GOAL>LinearIndependent R ![a • x + b • y, c • x + d • y]
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R✝ : Type u_2<VAR>K : Type u_3<VAR>M✝ : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M✝<VAR>inst✝¹⁰ : Ring R✝<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>a✝ b✝ : R✝<VAR>x✝ y✝ : M✝<VAR>R : Type u_8<VAR>M : Type u_9<VAR>inst✝³ : CommRing R<VAR>inst✝² : NoZeroDivisors R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>x y : M<VAR>h : LinearIndependent R ![x, y]<VAR>a b c d : R<VAR>h' : a * d - b * c ≠ 0<VAR>s t : R<VAR>hst : s • (a • x + b • y) + t • (c • x + d • y) = 0<GOAL>s = 0 ∧ t = 0
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R✝ : Type u_2<VAR>K : Type u_3<VAR>M✝ : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M✝<VAR>inst✝¹⁰ : Ring R✝<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>a✝ b✝ : R✝<VAR>x✝ y✝ : M✝<VAR>R : Type u_8<VAR>M : Type u_9<VAR>inst✝³ : CommRing R<VAR>inst✝² : NoZeroDivisors R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>x y : M<VAR>h : LinearIndependent R ![x, y]<VAR>a b c d : R<VAR>h' : a * d - b * c ≠ 0<VAR>s t : R<VAR>hst : s • (a • x + b • y) + t • (c • x + d • y) = 0<VAR>H : (s * a + t * c) • x + (s * b + t * d) • y = 0<GOAL>s = 0 ∧ t = 0
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R✝ : Type u_2<VAR>K : Type u_3<VAR>M✝ : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M✝<VAR>inst✝¹⁰ : Ring R✝<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>a✝ b✝ : R✝<VAR>x✝ y✝ : M✝<VAR>R : Type u_8<VAR>M : Type u_9<VAR>inst✝³ : CommRing R<VAR>inst✝² : NoZeroDivisors R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>x y : M<VAR>h : LinearIndependent R ![x, y]<VAR>a b c d : R<VAR>h' : a * d - b * c ≠ 0<VAR>s t : R<VAR>hst : s • (a • x + b • y) + t • (c • x + d • y) = 0<VAR>H : (s * a + t * c) • x + (s * b + t * d) • y = 0<VAR>I1 : s * a + t * c = 0<GOAL>s = 0 ∧ t = 0
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R✝ : Type u_2<VAR>K : Type u_3<VAR>M✝ : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M✝<VAR>inst✝¹⁰ : Ring R✝<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>a✝ b✝ : R✝<VAR>x✝ y✝ : M✝<VAR>R : Type u_8<VAR>M : Type u_9<VAR>inst✝³ : CommRing R<VAR>inst✝² : NoZeroDivisors R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>x y : M<VAR>h : LinearIndependent R ![x, y]<VAR>a b c d : R<VAR>h' : a * d - b * c ≠ 0<VAR>s t : R<VAR>hst : s • (a • x + b • y) + t • (c • x + d • y) = 0<VAR>H : (s * a + t * c) • x + (s * b + t * d) • y = 0<VAR>I1 : s * a + t * c = 0<VAR>I2 : s * b + t * d = 0<GOAL>s = 0 ∧ t = 0
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R✝ : Type u_2<VAR>K : Type u_3<VAR>M✝ : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M✝<VAR>inst✝¹⁰ : Ring R✝<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>a✝ b✝ : R✝<VAR>x✝ y✝ : M✝<VAR>R : Type u_8<VAR>M : Type u_9<VAR>inst✝³ : CommRing R<VAR>inst✝² : NoZeroDivisors R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>x y : M<VAR>h : LinearIndependent R ![x, y]<VAR>a b c d : R<VAR>h' : a * d - b * c ≠ 0<VAR>s t : R<VAR>hst : s • (a • x + b • y) + t • (c • x + d • y) = 0<VAR>H : (s * a + t * c) • x + (s * b + t * d) • y = 0<VAR>I1 : s * a + t * c = 0<VAR>I2 : s * b + t * d = 0<VAR>J1 : (a * d - b * c) * s = 0<GOAL>s = 0 ∧ t = 0
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R✝ : Type u_2<VAR>K : Type u_3<VAR>M✝ : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M✝<VAR>inst✝¹⁰ : Ring R✝<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>a✝ b✝ : R✝<VAR>x✝ y✝ : M✝<VAR>R : Type u_8<VAR>M : Type u_9<VAR>inst✝³ : CommRing R<VAR>inst✝² : NoZeroDivisors R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>x y : M<VAR>h : LinearIndependent R ![x, y]<VAR>a b c d : R<VAR>h' : a * d - b * c ≠ 0<VAR>s t : R<VAR>hst : s • (a • x + b • y) + t • (c • x + d • y) = 0<VAR>H : (s * a + t * c) • x + (s * b + t * d) • y = 0<VAR>I1 : s * a + t * c = 0<VAR>I2 : s * b + t * d = 0<VAR>J1 : (a * d - b * c) * s = 0<VAR>J2 : (a * d - b * c) * t = 0<GOAL>s = 0 ∧ t = 0
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>a : α<VAR>l : List α<GOAL>sublistsLen (a :: l).length (a :: l) = [a :: l]
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : MonoidalCategory C<VAR>X Y : C<GOAL>(λ_ X).inv ⊗ 𝟙 Y = (λ_ (X ⊗ Y)).inv ≫ (α_ (𝟙_ C) X Y).inv
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>inst✝¹ : SemilatticeSup β<VAR>inst✝ : Nonempty β<VAR>U : β → Set (α × α)<VAR>hU : ∀ s ∈ 𝓤 α, ∃ n, U n ⊆ s<VAR>f : β → α<VAR>hf : ∀ ⦃N m n : β⦄, N ≤ m → N ≤ n → (f m, f n) ∈ U N<VAR>s : Set (α × α)<VAR>hs : s ∈ 𝓤 α<GOAL>s ∈ map (Prod.map f f) atTop
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>inst✝¹ : SemilatticeSup β<VAR>inst✝ : Nonempty β<VAR>U : β → Set (α × α)<VAR>hU : ∀ s ∈ 𝓤 α, ∃ n, U n ⊆ s<VAR>f : β → α<VAR>hf : ∀ ⦃N m n : β⦄, N ≤ m → N ≤ n → (f m, f n) ∈ U N<VAR>s : Set (α × α)<VAR>hs : s ∈ 𝓤 α<GOAL>∃ a, ∀ b ≥ a, b ∈ Prod.map f f ⁻¹' s
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>inst✝¹ : SemilatticeSup β<VAR>inst✝ : Nonempty β<VAR>U : β → Set (α × α)<VAR>hU : ∀ s ∈ 𝓤 α, ∃ n, U n ⊆ s<VAR>f : β → α<VAR>hf : ∀ ⦃N m n : β⦄, N ≤ m → N ≤ n → (f m, f n) ∈ U N<VAR>s : Set (α × α)<VAR>hs : s ∈ 𝓤 α<VAR>N : β<VAR>hN : U N ⊆ s<VAR>m n : β<VAR>hmn : (m, n) ≥ (N, N)<GOAL>(m, n) ∈ Prod.map f f ⁻¹' s
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝⁴ : Category.{v, u} V<VAR>inst✝³ : HasZeroMorphisms V<VAR>A B C : V<VAR>f : A ⟶ B<VAR>inst✝² : HasImage f<VAR>g : B ⟶ C<VAR>inst✝¹ : HasKernel g<VAR>inst✝ : ConcreteCategory V<VAR>w : f ≫ g = 0<VAR>x : (forget V).obj (Subobject.underlying.obj (imageSubobject f))<GOAL>(kernelSubobject g).arrow ((imageToKernel f g w) x) = (imageSubobject f).arrow x
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>f : Perm α<VAR>x y : α<VAR>hy : (swap x (f x) * f) y ≠ y<GOAL>f y ≠ y ∧ y ≠ x
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>f : Perm α<VAR>x y : α<VAR>hy : (if f y = x then f x else if y = x then x else f y) ≠ y<GOAL>f y ≠ y ∧ y ≠ x
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : CompleteSpace E<VAR>F : Type u_3<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>a : E<VAR>hf : HasStrictFDerivAt f f' a<VAR>hf' : range f' = ⊤<VAR>hker : (LinearMap.ker f').ClosedComplemented<VAR>y : ↥(LinearMap.ker f')<GOAL>↑(implicitToPartialHomeomorphOfComplemented f f' hf hf' hker) (↑y + a) = (f (↑y + a), y)
<VAR>n : ℕ<GOAL>n.descFactorial 0 = 0 ↔ n < 0
<VAR>n k : ℕ<GOAL>n.descFactorial k.succ = 0 ↔ n < k.succ
<VAR>n k : ℕ<GOAL>n ≤ k → n ≠ k → n ≤ k
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : (i : ι) → AddZeroClass (β i)<VAR>inst✝¹ : (i : ι) → AddZeroClass (β₁ i)<VAR>inst✝ : (i : ι) → AddZeroClass (β₂ i)<VAR>f : (i : ι) → β₁ i →+ β₂ i<VAR>f₂ : (i : ι) → β i →+ β₁ i<GOAL>(addMonoidHom fun i => (f i).comp (f₂ i)) = (addMonoidHom f).comp (addMonoidHom f₂)
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : (i : ι) → AddZeroClass (β i)<VAR>inst✝¹ : (i : ι) → AddZeroClass (β₁ i)<VAR>inst✝ : (i : ι) → AddZeroClass (β₂ i)<VAR>f : (i : ι) → β₁ i →+ β₂ i<VAR>f₂ : (i : ι) → β i →+ β₁ i<GOAL>∀ (i : ι), (fun i x => (f i) x) i 0 = 0
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : (i : ι) → AddZeroClass (β i)<VAR>inst✝¹ : (i : ι) → AddZeroClass (β₁ i)<VAR>inst✝ : (i : ι) → AddZeroClass (β₂ i)<VAR>f : (i : ι) → β₁ i →+ β₂ i<VAR>f₂ : (i : ι) → β i →+ β₁ i<GOAL>∀ (i : ι), (fun i x => (f₂ i) x) i 0 = 0
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : (i : ι) → AddZeroClass (β i)<VAR>inst✝¹ : (i : ι) → AddZeroClass (β₁ i)<VAR>inst✝ : (i : ι) → AddZeroClass (β₂ i)<VAR>f : (i : ι) → β₁ i →+ β₂ i<VAR>f₂ : (i : ι) → β i →+ β₁ i<GOAL>∀ (i : ι), ((fun i x => (f i) x) i ∘ (fun i x => (f₂ i) x) i) 0 = 0
<VAR>α✝ : Sort u<VAR>β : Sort v<VAR>γ : Sort w<VAR>α : Type u_1<VAR>s : Set α<VAR>inst✝ : DecidablePred fun x => x ∈ s<VAR>x : α<VAR>hx : x ∈ sᶜ<GOAL>(Set.sumCompl s).symm ↑⟨x, hx⟩ = Sum.inr ⟨x, hx⟩
<VAR>α✝ : Type u_1<VAR>r : α✝ → α✝ → Prop<VAR>β α : Type u<VAR>f : β → α<VAR>w : #α < #β<VAR>w' : ℵ₀ ≤ #α<GOAL>∃ a, #α < #↑(f ⁻¹' {a})
<VAR>α✝ : Type u_1<VAR>r : α✝ → α✝ → Prop<VAR>β α : Type u<VAR>f : β → α<VAR>w : #α < #β<VAR>w' : ℵ₀ ≤ #α<GOAL>∃ a, succ #α ≤ #↑(f ⁻¹' {a})
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝³ : Field R<VAR>p q : R[X]<VAR>inst✝² : Field k<VAR>inst✝¹ : DecidableEq R<VAR>inst✝ : DecidableEq k<VAR>f : R →+* k<VAR>x : R[X]<GOAL>EuclideanDomain.gcd (map f 0) (map f x) = map f (EuclideanDomain.gcd 0 x)
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝³ : Field R<VAR>p q : R[X]<VAR>inst✝² : Field k<VAR>inst✝¹ : DecidableEq R<VAR>inst✝ : DecidableEq k<VAR>f : R →+* k<VAR>x y : R[X]<VAR>x✝ : x ≠ 0<VAR>ih : EuclideanDomain.gcd (map f (y % x)) (map f x) = map f (EuclideanDomain.gcd (y % x) x)<GOAL>EuclideanDomain.gcd (map f x) (map f y) = map f (EuclideanDomain.gcd x y)
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>P : Sylow p G<VAR>x✝ : G<GOAL>x✝ ∈ stabilizer G P ↔ x✝ ∈ (↑P).normalizer
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f✝ : ℕ → Ω → E<VAR>ℱ : Filtration ℕ m0<VAR>n✝ : ℕ<VAR>inst✝ : SigmaFiniteFiltration μ ℱ<VAR>f g : ℕ → Ω → E<VAR>hf : Martingale f ℱ μ<VAR>hg : Adapted ℱ fun n => g (n + 1)<VAR>hg0 : g 0 = 0<VAR>hgint : ∀ (n : ℕ), Integrable (g n) μ<VAR>n : ℕ<VAR>h : ℕ → Ω → E := f - martingalePart (f + g) ℱ μ<VAR>hhdef : h = f - martingalePart (f + g) ℱ μ<GOAL>martingalePart (f + g) ℱ μ n =ᶠ[ae μ] f n
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f✝ : ℕ → Ω → E<VAR>ℱ : Filtration ℕ m0<VAR>n✝ : ℕ<VAR>inst✝ : SigmaFiniteFiltration μ ℱ<VAR>f g : ℕ → Ω → E<VAR>hf : Martingale f ℱ μ<VAR>hg : Adapted ℱ fun n => g (n + 1)<VAR>hg0 : g 0 = 0<VAR>hgint : ∀ (n : ℕ), Integrable (g n) μ<VAR>n : ℕ<VAR>h : ℕ → Ω → E := f - martingalePart (f + g) ℱ μ<VAR>hhdef : h = f - martingalePart (f + g) ℱ μ<VAR>hh : h = predictablePart (f + g) ℱ μ - g<GOAL>martingalePart (f + g) ℱ μ n =ᶠ[ae μ] f n
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>f✝ : ℕ → Ω → E<VAR>ℱ : Filtration ℕ m0<VAR>n✝ : ℕ<VAR>inst✝ : SigmaFiniteFiltration μ ℱ<VAR>f g : ℕ → Ω → E<VAR>hf : Martingale f ℱ μ<VAR>hg : Adapted ℱ fun n => g (n + 1)<VAR>hg0 : g 0 = 0<VAR>hgint : ∀ (n : ℕ), Integrable (g n) μ<VAR>n : ℕ<VAR>h : ℕ → Ω → E := f - martingalePart (f + g) ℱ μ<VAR>hhdef : h = f - martingalePart (f + g) ℱ μ<VAR>hh : h = predictablePart (f + g) ℱ μ - g<VAR>hhpred : Adapted ℱ fun n => h (n + 1)<GOAL>martingalePart (f + g) ℱ μ n =ᶠ[ae μ] f n