ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>U : Type u_1<VAR>inst✝ : Quiver U<VAR>u v v' w : U<VAR>p : Path u v<VAR>p' : Path u v'<VAR>e : v ⟶ w<VAR>e' : v' ⟶ w<VAR>h : p.cons e = p'.cons e'<GOAL>HEq p p'
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>inst✝⁹ : RingHomInvPair σ σ'<VAR>inst✝⁸ : RingHomInvPair σ' σ<VAR>inst✝⁷ : RingHomIsometric σ<VAR>inst✝⁶ : RingHomIsometric σ'<VAR>E : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜' F<VAR>f : E →SL[σ] F<VAR>inst✝¹ : CompleteSpace F<VAR>inst✝ : CompleteSpace E<VAR>e : E ≃ₛₗ[σ] F<VAR>h : Continuous ⇑e<GOAL>Continuous ⇑e.symm
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>inst✝⁹ : RingHomInvPair σ σ'<VAR>inst✝⁸ : RingHomInvPair σ' σ<VAR>inst✝⁷ : RingHomIsometric σ<VAR>inst✝⁶ : RingHomIsometric σ'<VAR>E : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜' F<VAR>f : E →SL[σ] F<VAR>inst✝¹ : CompleteSpace F<VAR>inst✝ : CompleteSpace E<VAR>e : E ≃ₛₗ[σ] F<VAR>h : Continuous ⇑e<GOAL>∀ (s : Set E), IsOpen s → IsOpen (⇑e.symm ⁻¹' s)
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>inst✝⁹ : RingHomInvPair σ σ'<VAR>inst✝⁸ : RingHomInvPair σ' σ<VAR>inst✝⁷ : RingHomIsometric σ<VAR>inst✝⁶ : RingHomIsometric σ'<VAR>E : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜' F<VAR>f : E →SL[σ] F<VAR>inst✝¹ : CompleteSpace F<VAR>inst✝ : CompleteSpace E<VAR>e : E ≃ₛₗ[σ] F<VAR>h : Continuous ⇑e<VAR>s : Set E<VAR>hs : IsOpen s<GOAL>IsOpen (⇑e.symm ⁻¹' s)
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>inst✝⁹ : RingHomInvPair σ σ'<VAR>inst✝⁸ : RingHomInvPair σ' σ<VAR>inst✝⁷ : RingHomIsometric σ<VAR>inst✝⁶ : RingHomIsometric σ'<VAR>E : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜' F<VAR>f : E →SL[σ] F<VAR>inst✝¹ : CompleteSpace F<VAR>inst✝ : CompleteSpace E<VAR>e : E ≃ₛₗ[σ] F<VAR>h : Continuous ⇑e<VAR>s : Set E<VAR>hs : IsOpen s<GOAL>IsOpen (⇑e '' s)
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>inst✝⁹ : RingHomInvPair σ σ'<VAR>inst✝⁸ : RingHomInvPair σ' σ<VAR>inst✝⁷ : RingHomIsometric σ<VAR>inst✝⁶ : RingHomIsometric σ'<VAR>E : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜' F<VAR>f : E →SL[σ] F<VAR>inst✝¹ : CompleteSpace F<VAR>inst✝ : CompleteSpace E<VAR>e : E ≃ₛₗ[σ] F<VAR>h : Continuous ⇑↑e<VAR>s : Set E<VAR>hs : IsOpen s<GOAL>IsOpen (⇑↑e '' s)
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>inst✝² : AddCommGroup M<VAR>R : Type u_3<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Module R M<VAR>I : Ideal R<VAR>v : ι → M<VAR>hv : Submodule.span R (Set.range v) = ⊤<VAR>x✝ : M<GOAL>x✝ ∈ LinearMap.range (finsuppTotal ι M I v) ↔ x✝ ∈ I • Submodule.span R (Set.range v)
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>inst✝² : AddCommGroup M<VAR>R : Type u_3<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Module R M<VAR>I : Ideal R<VAR>v : ι → M<VAR>hv : Submodule.span R (Set.range v) = ⊤<VAR>x✝ : M<GOAL>x✝ ∈ LinearMap.range (finsuppTotal ι M I v) ↔ ∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c => c • v i) = x✝
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>inst✝² : AddCommGroup M<VAR>R : Type u_3<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Module R M<VAR>I : Ideal R<VAR>v : ι → M<VAR>hv : Submodule.span R (Set.range v) = ⊤<VAR>x✝ : M<GOAL>(∃ a, ∃ (_ : ∀ (i : ι), a i ∈ I), (a.sum fun i c => c • v i) = x✝) → x✝ ∈ LinearMap.range (finsuppTotal ι M I v)
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>f f₁ : E → F<VAR>f' f₀' f₁' : F<VAR>s t : Set E<VAR>x v : E<GOAL>LineDifferentiableWithinAt 𝕜 f univ x v ↔ LineDifferentiableAt 𝕜 f x v
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝ : Fintype ι<VAR>m : (i : ι) → OuterMeasure (α i)<VAR>s : Set ((i : ι) → α i)<GOAL>piPremeasure m (univ.pi fun i => eval i '' s) = piPremeasure m s
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝ : Fintype ι<VAR>m : (i : ι) → OuterMeasure (α i)<VAR>s : Set ((i : ι) → α i)<GOAL>∏ i : ι, (m i) ((fun a => a i) '' s) = piPremeasure m s
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : Semiring S<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommMonoid P<VAR>inst✝ : Module R P<VAR>s t : Set α<VAR>hs : Disjoint s t<GOAL>Disjoint (⨆ a ∈ s, LinearMap.range (lsingle a)) (⨆ a ∈ t, LinearMap.range (lsingle a))
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : Semiring S<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommMonoid P<VAR>inst✝ : Module R P<VAR>s t : Set α<VAR>hs : Disjoint s t<GOAL>Disjoint s sᶜ
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : Semiring S<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommMonoid P<VAR>inst✝ : Module R P<VAR>s t : Set α<VAR>hs : Disjoint s t<GOAL>Disjoint t tᶜ
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : Semiring S<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommMonoid P<VAR>inst✝ : Module R P<VAR>s t : Set α<VAR>hs : Disjoint s t<GOAL>Disjoint (⨅ a ∈ sᶜ, ker (lapply a)) (⨅ a ∈ tᶜ, ker (lapply a))
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : Semiring S<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommMonoid P<VAR>inst✝ : Module R P<VAR>s t : Set α<VAR>hs : Disjoint s t<GOAL>(⨅ a ∈ sᶜ, ker (lapply a)) ⊓ ⨅ a ∈ tᶜ, ker (lapply a) ≤ ⊥
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : Semiring S<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : AddCommMonoid N<VAR>inst✝² : Module R N<VAR>inst✝¹ : AddCommMonoid P<VAR>inst✝ : Module R P<VAR>s t : Set α<VAR>hs : Disjoint s t<VAR>i : α<GOAL>(⨅ a ∈ sᶜ, ker (lapply a)) ⊓ ⨅ a ∈ tᶜ, ker (lapply a) ≤ ker (lapply i)
<VAR>R : Type u_1<VAR>M✝ : Type u_2<VAR>inst✝¹⁸ : CommSemiring R<VAR>inst✝¹⁷ : AddCommMonoid M✝<VAR>inst✝¹⁶ : Module R M✝<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝¹⁵ : CommRing R₁<VAR>inst✝¹⁴ : AddCommGroup M₁<VAR>inst✝¹³ : Module R₁ M₁<VAR>R₂ : Type u_5<VAR>M₂ : Type u_6<VAR>inst✝¹² : CommSemiring R₂<VAR>inst✝¹¹ : AddCommMonoid M₂<VAR>inst✝¹⁰ : Module R₂ M₂<VAR>R₃ : Type u_7<VAR>M₃ : Type u_8<VAR>inst✝⁹ : CommRing R₃<VAR>inst✝⁸ : AddCommGroup M₃<VAR>inst✝⁷ : Module R₃ M₃<VAR>V : Type u_9<VAR>K : Type u_10<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module K V<VAR>B : BilinForm R M✝<VAR>B₁ : BilinForm R₁ M₁<VAR>B₂ : BilinForm R₂ M₂<VAR>n : Type u_11<VAR>o : Type u_12<VAR>inst✝³ : Fintype n<VAR>inst✝² : Fintype o<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : DecidableEq o<VAR>M : Matrix n n R₂<VAR>P Q : Matrix n o R₂<GOAL>BilinForm.toMatrix' ((toBilin' M).comp (toLin' P) (toLin' Q)) = BilinForm.toMatrix' (toBilin' (Pᵀ * M * Q))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f : α → E<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>_i : Fact (1 ≤ p)<VAR>hp_ne_top : p ≠ ⊤<VAR>P : (α → E) → Prop<VAR>h_ind : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → P (s.indicator fun x => c)<VAR>h_add : ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → Memℒp f p μ → Memℒp g p μ → P f → P g → P (f + g)<VAR>h_closed : IsClosed {f | P ↑↑f}<VAR>h_ae : ∀ ⦃f g : α → E⦄, f =ᶠ[ae μ] g → Memℒp f p μ → P f → P g<VAR>this : ∀ (f : α →ₛ E), Memℒp (↑f) p μ → P ↑f<GOAL>∀ ⦃f : α → E⦄, Memℒp f p μ → P f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f : α → E<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>_i : Fact (1 ≤ p)<VAR>hp_ne_top : p ≠ ⊤<VAR>P : (α → E) → Prop<VAR>h_ind : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → P (s.indicator fun x => c)<VAR>h_add : ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → Memℒp f p μ → Memℒp g p μ → P f → P g → P (f + g)<VAR>h_closed : IsClosed {f | P ↑↑f}<VAR>h_ae : ∀ ⦃f g : α → E⦄, f =ᶠ[ae μ] g → Memℒp f p μ → P f → P g<VAR>this✝ : ∀ (f : α →ₛ E), Memℒp (↑f) p μ → P ↑f<VAR>this : ∀ (f : ↥(Lp.simpleFunc E p μ)), P ↑↑↑f<GOAL>∀ ⦃f : α → E⦄, Memℒp f p μ → P f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : NormedAddCommGroup E<VAR>f : α → E<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>_i : Fact (1 ≤ p)<VAR>hp_ne_top : p ≠ ⊤<VAR>P : (α → E) → Prop<VAR>h_ind : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → P (s.indicator fun x => c)<VAR>h_add : ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → Memℒp f p μ → Memℒp g p μ → P f → P g → P (f + g)<VAR>h_closed : IsClosed {f | P ↑↑f}<VAR>h_ae : ∀ ⦃f g : α → E⦄, f =ᶠ[ae μ] g → Memℒp f p μ → P f → P g<VAR>this✝¹ : ∀ (f : α →ₛ E), Memℒp (↑f) p μ → P ↑f<VAR>this✝ : ∀ (f : ↥(Lp.simpleFunc E p μ)), P ↑↑↑f<VAR>this : ∀ (f : ↥(Lp E p μ)), P ↑↑f<GOAL>∀ ⦃f : α → E⦄, Memℒp f p μ → P f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : FunLike F (Set α) ℝ≥0∞<VAR>inst✝ : OuterMeasureClass F α<VAR>μ : F<VAR>s t : Set α<VAR>h : t =ᶠ[ae μ] ∅<GOAL>s ∩ t =ᶠ[ae μ] ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : FunLike F (Set α) ℝ≥0∞<VAR>inst✝ : OuterMeasureClass F α<VAR>μ : F<VAR>s t : Set α<VAR>h : t =ᶠ[ae μ] ∅<GOAL>∅ = s ∩ ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s✝ : Finset α<VAR>a✝ b a : α<VAR>s : Finset α<GOAL>s.val = {a} ↔ s = {a}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s✝ : Finset α<VAR>a✝ b a : α<VAR>s : Finset α<GOAL>s.val = {a} ↔ s.val = {a}.val
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Ring S<VAR>inst✝⁵ : Algebra R S<VAR>K : Type u_4<VAR>L : Type u_5<VAR>F : Type u_6<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : Field F<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : Algebra K F<VAR>ι : Type w<VAR>x : L<VAR>hf : Splits (algebraMap K F) (minpoly K x)<GOAL>(algebraMap K F) ((norm K) (AdjoinSimple.gen K x)) = ((minpoly K x).aroots F).prod
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Ring S<VAR>inst✝⁵ : Algebra R S<VAR>K : Type u_4<VAR>L : Type u_5<VAR>F : Type u_6<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : Field F<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : Algebra K F<VAR>ι : Type w<VAR>x : L<VAR>hf : Splits (algebraMap K F) (minpoly K x)<VAR>injKxL : Function.Injective ⇑(algebraMap (↥K⟮x⟯) L)<GOAL>(algebraMap K F) ((norm K) (AdjoinSimple.gen K x)) = ((minpoly K x).aroots F).prod
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Ring S<VAR>inst✝⁵ : Algebra R S<VAR>K : Type u_4<VAR>L : Type u_5<VAR>F : Type u_6<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : Field F<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : Algebra K F<VAR>ι : Type w<VAR>x : L<VAR>hf : Splits (algebraMap K F) (minpoly K x)<VAR>injKxL : Function.Injective ⇑(algebraMap (↥K⟮x⟯) L)<VAR>hx : IsIntegral K x<GOAL>(algebraMap K F) ((norm K) (AdjoinSimple.gen K x)) = ((minpoly K x).aroots F).prod
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Ring S<VAR>inst✝⁵ : Algebra R S<VAR>K : Type u_4<VAR>L : Type u_5<VAR>F : Type u_6<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : Field F<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : Algebra K F<VAR>ι : Type w<VAR>x : L<VAR>hf : Splits (algebraMap K F) (minpoly K x)<VAR>injKxL : Function.Injective ⇑(algebraMap (↥K⟮x⟯) L)<VAR>hx : IsIntegral K x<GOAL>Splits (algebraMap K F) (minpoly K x)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B B₁ B₂ : Set α<VAR>inst✝ : M.RkPos<VAR>hB : M.Base B<GOAL>B.Nonempty
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B B₁ B₂ : Set α<VAR>inst✝ : M.RkPos<VAR>hB : M.Base B<GOAL>B ≠ ∅
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B₁ B₂ : Set α<VAR>inst✝ : M.RkPos<VAR>hB : M.Base ∅<GOAL>False
<VAR>α : Type u<VAR>inst✝² : DecidableEq α<VAR>β : Type v<VAR>inst✝¹ : Fintype α<VAR>f : Perm α<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>h₁ : ∀ (x : α), p x ↔ p (f x)<VAR>h₂ : ∀ (x : α), f x ≠ x → p x<VAR>l : { l // l.prod = f.subtypePerm h₁ ∧ ∀ g ∈ l, g.IsSwap } := (f.subtypePerm h₁).truncSwapFactors.out<GOAL>sign (f.subtypePerm h₁) = sign f
<VAR>α : Type u<VAR>inst✝² : DecidableEq α<VAR>β : Type v<VAR>inst✝¹ : Fintype α<VAR>f : Perm α<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>h₁ : ∀ (x : α), p x ↔ p (f x)<VAR>h₂ : ∀ (x : α), f x ≠ x → p x<VAR>l : { l // l.prod = f.subtypePerm h₁ ∧ ∀ g ∈ l, g.IsSwap } := (f.subtypePerm h₁).truncSwapFactors.out<VAR>hl' : ∀ g' ∈ List.map ⇑ofSubtype ↑l, g'.IsSwap<GOAL>sign (f.subtypePerm h₁) = sign f
<VAR>α : Type u<VAR>inst✝² : DecidableEq α<VAR>β : Type v<VAR>inst✝¹ : Fintype α<VAR>f : Perm α<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>h₁ : ∀ (x : α), p x ↔ p (f x)<VAR>h₂ : ∀ (x : α), f x ≠ x → p x<VAR>l : { l // l.prod = f.subtypePerm h₁ ∧ ∀ g ∈ l, g.IsSwap } := (f.subtypePerm h₁).truncSwapFactors.out<VAR>hl' : ∀ g' ∈ List.map ⇑ofSubtype ↑l, g'.IsSwap<VAR>hl'₂ : (List.map ⇑ofSubtype ↑l).prod = f<GOAL>sign (f.subtypePerm h₁) = sign f
<VAR>α : Type u<VAR>inst✝² : DecidableEq α<VAR>β : Type v<VAR>inst✝¹ : Fintype α<VAR>f : Perm α<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>h₁ : ∀ (x : α), p x ↔ p (f x)<VAR>h₂ : ∀ (x : α), f x ≠ x → p x<VAR>l : { l // l.prod = f.subtypePerm h₁ ∧ ∀ g ∈ l, g.IsSwap } := (f.subtypePerm h₁).truncSwapFactors.out<VAR>hl' : ∀ g' ∈ List.map ⇑ofSubtype ↑l, g'.IsSwap<VAR>hl'₂ : (List.map ⇑ofSubtype ↑l).prod = f<GOAL>sign (↑l).prod = sign f
<VAR>α : Type u<VAR>inst✝² : DecidableEq α<VAR>β : Type v<VAR>inst✝¹ : Fintype α<VAR>f : Perm α<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>h₁ : ∀ (x : α), p x ↔ p (f x)<VAR>h₂ : ∀ (x : α), f x ≠ x → p x<VAR>l : { l // l.prod = f.subtypePerm h₁ ∧ ∀ g ∈ l, g.IsSwap } := (f.subtypePerm h₁).truncSwapFactors.out<VAR>hl' : ∀ g' ∈ List.map ⇑ofSubtype ↑l, g'.IsSwap<VAR>hl'₂ : (List.map ⇑ofSubtype ↑l).prod = f<GOAL>sign (↑l).prod = sign (List.map ⇑ofSubtype ↑l).prod
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f✝ g✝ : α → M<VAR>a b : α<VAR>s t : Set α<VAR>f : α → M<VAR>g : β → M<VAR>e : α → β<VAR>he₀ : Bijective e<VAR>he₁ : ∀ (x : α), f x = g (e x)<GOAL>∏ᶠ (i : α), f i = ∏ᶠ (j : β), g j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f✝ g✝ : α → M<VAR>a b : α<VAR>s t : Set α<VAR>f : α → M<VAR>g : β → M<VAR>e : α → β<VAR>he₀ : Bijective e<VAR>he₁ : ∀ (x : α), f x = g (e x)<GOAL>∏ᶠ (i : α) (_ : i ∈ univ), f i = ∏ᶠ (i : β) (_ : i ∈ univ), g i
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : NormedAddCommGroup F<VAR>s : Set α<VAR>f : ↥(Lp E 2 μ)<VAR>hs : MeasurableSet s<VAR>c : E<VAR>hμs : μ s ≠ ⊤<GOAL>⟪indicatorConstLp 2 hs hμs c, f⟫_𝕜 = ∫ (x : α) in s, ⟪c, ↑↑f x⟫_𝕜 ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : NormedAddCommGroup F<VAR>s : Set α<VAR>f : ↥(Lp E 2 μ)<VAR>hs : MeasurableSet s<VAR>c : E<VAR>hμs : μ s ≠ ⊤<GOAL>∫ (x : α) in s, ⟪↑↑(indicatorConstLp 2 hs hμs c) x, ↑↑f x⟫_𝕜 ∂μ + ∫ (x : α) in sᶜ, ⟪↑↑(indicatorConstLp 2 hs hμs c) x, ↑↑f x⟫_𝕜 ∂μ = ∫ (x : α) in s, ⟪c, ↑↑f x⟫_𝕜 ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : NormedAddCommGroup F<VAR>s : Set α<VAR>f : ↥(Lp E 2 μ)<VAR>hs : MeasurableSet s<VAR>c : E<VAR>hμs : μ s ≠ ⊤<VAR>h_left : ∫ (x : α) in s, ⟪↑↑(indicatorConstLp 2 hs hμs c) x, ↑↑f x⟫_𝕜 ∂μ = ∫ (x : α) in s, ⟪c, ↑↑f x⟫_𝕜 ∂μ<GOAL>∫ (x : α) in s, ⟪↑↑(indicatorConstLp 2 hs hμs c) x, ↑↑f x⟫_𝕜 ∂μ + ∫ (x : α) in sᶜ, ⟪↑↑(indicatorConstLp 2 hs hμs c) x, ↑↑f x⟫_𝕜 ∂μ = ∫ (x : α) in s, ⟪c, ↑↑f x⟫_𝕜 ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : NormedAddCommGroup F<VAR>s : Set α<VAR>f : ↥(Lp E 2 μ)<VAR>hs : MeasurableSet s<VAR>c : E<VAR>hμs : μ s ≠ ⊤<VAR>h_left : ∫ (x : α) in s, ⟪↑↑(indicatorConstLp 2 hs hμs c) x, ↑↑f x⟫_𝕜 ∂μ = ∫ (x : α) in s, ⟪c, ↑↑f x⟫_𝕜 ∂μ<VAR>h_right : ∫ (x : α) in sᶜ, ⟪↑↑(indicatorConstLp 2 hs hμs c) x, ↑↑f x⟫_𝕜 ∂μ = 0<GOAL>∫ (x : α) in s, ⟪↑↑(indicatorConstLp 2 hs hμs c) x, ↑↑f x⟫_𝕜 ∂μ + ∫ (x : α) in sᶜ, ⟪↑↑(indicatorConstLp 2 hs hμs c) x, ↑↑f x⟫_𝕜 ∂μ = ∫ (x : α) in s, ⟪c, ↑↑f x⟫_𝕜 ∂μ
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>e : Sym2 V<VAR>inst✝¹ : Fintype V<VAR>inst✝ : DecidableRel G.Adj<VAR>v : V<GOAL>G.degree v < Fintype.card V
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace ℝ G<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>Z : Type u_5<VAR>inst✝ : TopologicalSpace X<VAR>f g : X → Y<VAR>A : Set X<VAR>x : X<VAR>h : ∀ (x : X), (↑f).IsConstant<VAR>s : Set Y<GOAL>IsOpen (f ⁻¹' s)
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace ℝ G<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>Z : Type u_5<VAR>inst✝ : TopologicalSpace X<VAR>f g : X → Y<VAR>A : Set X<VAR>x : X<VAR>h : ∀ (x : X), (↑f).IsConstant<VAR>s : Set Y<GOAL>∀ x ∈ f ⁻¹' s, f ⁻¹' s ∈ 𝓝 x
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace ℝ G<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>Z : Type u_5<VAR>inst✝ : TopologicalSpace X<VAR>f g : X → Y<VAR>A : Set X<VAR>x : X<VAR>h : ∀ (x : X), (↑f).IsConstant<VAR>s : Set Y<VAR>a : X<VAR>ha : a ∈ f ⁻¹' s<VAR>b : Y<VAR>hb : f =ᶠ[𝓝 a] fun x => b<GOAL>f ⁻¹' s ∈ 𝓝 a
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace ℝ G<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>Z : Type u_5<VAR>inst✝ : TopologicalSpace X<VAR>f g : X → Y<VAR>A : Set X<VAR>x : X<VAR>h : ∀ (x : X), (↑f).IsConstant<VAR>s : Set Y<VAR>a : X<VAR>ha : a ∈ f ⁻¹' s<VAR>b : Y<VAR>hb : f =ᶠ[𝓝 a] fun x => b<GOAL>{x | (fun x => f x = (fun x => b) x) x} ⊆ f ⁻¹' s
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace ℝ G<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>Z : Type u_5<VAR>inst✝ : TopologicalSpace X<VAR>f g : X → Y<VAR>A : Set X<VAR>x✝ : X<VAR>h : ∀ (x : X), (↑f).IsConstant<VAR>s : Set Y<VAR>a : X<VAR>ha : a ∈ f ⁻¹' s<VAR>b : Y<VAR>hb : f =ᶠ[𝓝 a] fun x => b<VAR>x : X<VAR>hx : x ∈ {x | (fun x => f x = (fun x => b) x) x}<GOAL>x ∈ f ⁻¹' s
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace ℝ G<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>Z : Type u_5<VAR>inst✝ : TopologicalSpace X<VAR>f g : X → Y<VAR>A : Set X<VAR>x✝ : X<VAR>h : ∀ (x : X), (↑f).IsConstant<VAR>s : Set Y<VAR>a : X<VAR>ha : a ∈ f ⁻¹' s<VAR>b : Y<VAR>hb : f =ᶠ[𝓝 a] fun x => b<VAR>x : X<VAR>hx : x ∈ {x | (fun x => f x = (fun x => b) x) x}<VAR>this : f x = f a<GOAL>x ∈ f ⁻¹' s
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup G<VAR>inst✝¹ : NormedSpace ℝ G<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>Z : Type u_5<VAR>inst✝ : TopologicalSpace X<VAR>f g : X → Y<VAR>A : Set X<VAR>x✝ : X<VAR>h : ∀ (x : X), (↑f).IsConstant<VAR>s : Set Y<VAR>a : X<VAR>ha : a ∈ f ⁻¹' s<VAR>b : Y<VAR>hb : f =ᶠ[𝓝 a] fun x => b<VAR>x : X<VAR>hx : x ∈ {x | (fun x => f x = (fun x => b) x) x}<VAR>this : f x = f a<GOAL>f a ∈ s
<VAR>R : Type u<VAR>inst✝⁵ : CommRing R<VAR>M : Type u<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>N : Type u<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>ι : Type u<VAR>inst✝ : Fintype ι<VAR>m : ι → M<VAR>n : ι → N<VAR>hm : span R (Set.range m) = ⊤<VAR>hmn : ∑ i : ι, m i ⊗ₜ[R] n i = 0<VAR>G : (ι →₀ R) →ₗ[R] M := Finsupp.total ι M R m<VAR>hG : G = Finsupp.total ι M R m<GOAL>VanishesTrivially R m n
<VAR>R : Type u<VAR>inst✝⁵ : CommRing R<VAR>M : Type u<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>N : Type u<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>ι : Type u<VAR>inst✝ : Fintype ι<VAR>m : ι → M<VAR>n : ι → N<VAR>hm : span R (Set.range m) = ⊤<VAR>hmn : ∑ i : ι, m i ⊗ₜ[R] n i = 0<VAR>G : (ι →₀ R) →ₗ[R] M := Finsupp.total ι M R m<VAR>hG : G = Finsupp.total ι M R m<VAR>G_basis_eq : ∀ (i : ι), G (Finsupp.single i 1) = m i<GOAL>VanishesTrivially R m n
<VAR>R : Type u<VAR>inst✝⁵ : CommRing R<VAR>M : Type u<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>N : Type u<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>ι : Type u<VAR>inst✝ : Fintype ι<VAR>m : ι → M<VAR>n : ι → N<VAR>hm : span R (Set.range m) = ⊤<VAR>hmn : ∑ i : ι, m i ⊗ₜ[R] n i = 0<VAR>G : (ι →₀ R) →ₗ[R] M := Finsupp.total ι M R m<VAR>hG : G = Finsupp.total ι M R m<VAR>G_basis_eq : ∀ (i : ι), G (Finsupp.single i 1) = m i<VAR>G_surjective : Surjective ⇑G<GOAL>VanishesTrivially R m n
<VAR>R : Type u<VAR>inst✝⁵ : CommRing R<VAR>M : Type u<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>N : Type u<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>ι : Type u<VAR>inst✝ : Fintype ι<VAR>m : ι → M<VAR>n : ι → N<VAR>hm : span R (Set.range m) = ⊤<VAR>hmn : ∑ i : ι, m i ⊗ₜ[R] n i = 0<VAR>G : (ι →₀ R) →ₗ[R] M := Finsupp.total ι M R m<VAR>hG : G = Finsupp.total ι M R m<VAR>G_basis_eq : ∀ (i : ι), G (Finsupp.single i 1) = m i<VAR>G_surjective : Surjective ⇑G<VAR>en : (ι →₀ R) ⊗[R] N := ∑ i : ι, Finsupp.single i 1 ⊗ₜ[R] n i<VAR>hen : en = ∑ i : ι, Finsupp.single i 1 ⊗ₜ[R] n i<VAR>en_mem_ker : en ∈ ker (rTensor N G)<GOAL>VanishesTrivially R m n