ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : TopologicalSpace α<VAR>μ : Measure α<VAR>p q : Set α → Prop<VAR>U s✝ : Set α<VAR>ε r✝ : ℝ≥0∞<VAR>inst✝ : SigmaFinite μ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>r : ℝ≥0∞<VAR>hr : r < μ s<VAR>B : ℕ → Set α := spanningSets μ<VAR>hBU : ⋃ n, s ∩ B n = s<GOAL>∃ K ⊆ s, (fun s => MeasurableSet s ∧ μ s ≠ ⊤) K ∧ r < μ K
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : TopologicalSpace α<VAR>μ : Measure α<VAR>p q : Set α → Prop<VAR>U s✝ : Set α<VAR>ε r✝ : ℝ≥0∞<VAR>inst✝ : SigmaFinite μ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>r : ℝ≥0∞<VAR>hr : r < μ s<VAR>B : ℕ → Set α := spanningSets μ<VAR>hBU : ⋃ n, s ∩ B n = s<VAR>this : μ s = ⨆ n, μ (s ∩ B n)<GOAL>∃ K ⊆ s, (fun s => MeasurableSet s ∧ μ s ≠ ⊤) K ∧ r < μ K
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : TopologicalSpace α<VAR>μ : Measure α<VAR>p q : Set α → Prop<VAR>U s✝ : Set α<VAR>ε r✝ : ℝ≥0∞<VAR>inst✝ : SigmaFinite μ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>r : ℝ≥0∞<VAR>B : ℕ → Set α := spanningSets μ<VAR>hr : r < ⨆ n, μ (s ∩ B n)<VAR>hBU : ⋃ n, s ∩ B n = s<VAR>this : μ s = ⨆ n, μ (s ∩ B n)<GOAL>∃ K ⊆ s, (fun s => MeasurableSet s ∧ μ s ≠ ⊤) K ∧ r < μ K
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : TopologicalSpace α<VAR>μ : Measure α<VAR>p q : Set α → Prop<VAR>U s✝ : Set α<VAR>ε r✝ : ℝ≥0∞<VAR>inst✝ : SigmaFinite μ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>r : ℝ≥0∞<VAR>B : ℕ → Set α := spanningSets μ<VAR>hr : r < ⨆ n, μ (s ∩ B n)<VAR>hBU : ⋃ n, s ∩ B n = s<VAR>this : μ s = ⨆ n, μ (s ∩ B n)<VAR>n : ℕ<VAR>hn : r < μ (s ∩ B n)<GOAL>∃ K ⊆ s, (fun s => MeasurableSet s ∧ μ s ≠ ⊤) K ∧ r < μ K
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : TopologicalSpace α<VAR>μ : Measure α<VAR>p q : Set α → Prop<VAR>U s✝ : Set α<VAR>ε r✝ : ℝ≥0∞<VAR>inst✝ : SigmaFinite μ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>r : ℝ≥0∞<VAR>B : ℕ → Set α := spanningSets μ<VAR>hr : r < ⨆ n, μ (s ∩ B n)<VAR>hBU : ⋃ n, s ∩ B n = s<VAR>this : μ s = ⨆ n, μ (s ∩ B n)<VAR>n : ℕ<VAR>hn : r < μ (s ∩ B n)<GOAL>μ (s ∩ B n) ≠ ⊤
<VAR>X : Scheme<GOAL>⨆ i, ↑i = ⊤
<VAR>X : Scheme<GOAL>↑(⨆ i, ↑i) = ↑⊤
<VAR>X : Scheme<GOAL>⋃ i, ↑↑i = ↑⊤
<VAR>X : Scheme<GOAL>IsTopologicalBasis (Set.range fun i => ↑↑i)
<VAR>X : Scheme<GOAL>IsTopologicalBasis (SetLike.coe '' X.affineOpens)
<VAR>R : Type u<VAR>a✝ b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>a : R<GOAL>(C a * X).toFinsupp = Finsupp.single 1 a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a✝ b c d : α<VAR>n : ℤ<VAR>a : α<GOAL>|1 / a| = 1 / |a|
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f : α → β<VAR>x : α<GOAL>ContinuousWithinAt f {x} x
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<GOAL>n.pred = n ↔ n = 0
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : E → F<VAR>K : Set (E →L[𝕜] F)<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>r ε : ℝ<VAR>hε : 0 < ε<VAR>hr : 0 < r<VAR>x : E<VAR>L₁ L₂ : E →L[𝕜] F<VAR>h₁ : x ∈ A f L₁ r ε<VAR>h₂ : x ∈ A f L₂ r ε<GOAL>‖L₁ - L₂‖ ≤ 4 * ‖c‖ * ε
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : E → F<VAR>K : Set (E →L[𝕜] F)<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>r ε : ℝ<VAR>hε : 0 < ε<VAR>hr : 0 < r<VAR>x : E<VAR>L₁ L₂ : E →L[𝕜] F<VAR>h₁ : x ∈ A f L₁ r ε<VAR>h₂ : x ∈ A f L₂ r ε<GOAL>∀ (x : E), r / 2 / ‖c‖ ≤ ‖x‖ → ‖x‖ < r / 2 → ‖(L₁ - L₂) x‖ ≤ 4 * ‖c‖ * ε * ‖x‖
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : E → F<VAR>K : Set (E →L[𝕜] F)<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>r ε : ℝ<VAR>hε : 0 < ε<VAR>hr : 0 < r<VAR>x : E<VAR>L₁ L₂ : E →L[𝕜] F<VAR>h₁ : x ∈ A f L₁ r ε<VAR>h₂ : x ∈ A f L₂ r ε<VAR>y : E<VAR>ley : r / 2 / ‖c‖ ≤ ‖y‖<VAR>ylt : ‖y‖ < r / 2<GOAL>‖(L₁ - L₂) y‖ ≤ 4 * ‖c‖ * ε * ‖y‖
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : E → F<VAR>K : Set (E →L[𝕜] F)<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>r ε : ℝ<VAR>hε : 0 < ε<VAR>hr : 0 < r<VAR>x : E<VAR>L₁ L₂ : E →L[𝕜] F<VAR>h₁ : x ∈ A f L₁ r ε<VAR>h₂ : x ∈ A f L₂ r ε<VAR>y : E<VAR>ley : r ≤ 2 * ‖c‖ * ‖y‖<VAR>ylt : ‖y‖ < r / 2<GOAL>‖(L₁ - L₂) y‖ ≤ 4 * ‖c‖ * ε * ‖y‖
<VAR>R : Type u_1<VAR>inst✝⁹ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁸ : CommRing P<VAR>inst✝⁷ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝⁶ : CommRing R₁<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Field L<VAR>inst✝³ : Algebra R₁ K<VAR>inst✝² : IsFractionRing R₁ K<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsFractionRing K L<VAR>I : FractionalIdeal K⁰ L<GOAL>I = 0 ∨ I = 1
<VAR>R : Type u_1<VAR>inst✝⁹ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁸ : CommRing P<VAR>inst✝⁷ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝⁶ : CommRing R₁<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Field L<VAR>inst✝³ : Algebra R₁ K<VAR>inst✝² : IsFractionRing R₁ K<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsFractionRing K L<VAR>I : FractionalIdeal K⁰ L<GOAL>¬I = 0 → I = 1
<VAR>R : Type u_1<VAR>inst✝⁹ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁸ : CommRing P<VAR>inst✝⁷ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝⁶ : CommRing R₁<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Field L<VAR>inst✝³ : Algebra R₁ K<VAR>inst✝² : IsFractionRing R₁ K<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsFractionRing K L<VAR>I : FractionalIdeal K⁰ L<VAR>hI : ¬I = 0<GOAL>I = 1
<VAR>R : Type u_1<VAR>inst✝⁹ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁸ : CommRing P<VAR>inst✝⁷ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝⁶ : CommRing R₁<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Field L<VAR>inst✝³ : Algebra R₁ K<VAR>inst✝² : IsFractionRing R₁ K<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsFractionRing K L<VAR>I : FractionalIdeal K⁰ L<VAR>hI : ¬I = 0<GOAL>∀ (x : L), x ∈ I ↔ ∃ x', (algebraMap K L) x' = x
<VAR>R✝ : Type u_1<VAR>inst✝¹³ : CommSemiring R✝<VAR>A✝ : Type u_2<VAR>B✝ : Type u_3<VAR>inst✝¹² : Semiring A✝<VAR>inst✝¹¹ : Semiring B✝<VAR>inst✝¹⁰ : Algebra R✝ A✝<VAR>inst✝⁹ : Algebra R✝ B✝<VAR>R : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>A : Type u_5<VAR>B : Type u_6<VAR>C : Type u_7<VAR>D : Type u_8<VAR>inst✝⁷ : Ring A<VAR>inst✝⁶ : Ring B<VAR>inst✝⁵ : Ring C<VAR>inst✝⁴ : Ring D<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : Algebra R C<VAR>inst✝ : Algebra R D<VAR>f : A →ₐ[R] B<VAR>g : C →ₐ[R] D<VAR>hf : Function.Surjective ⇑f<GOAL>RingHom.ker (map f (AlgHom.id R C)) = Ideal.map includeLeft (RingHom.ker f)
<VAR>R✝ : Type u_1<VAR>inst✝¹³ : CommSemiring R✝<VAR>A✝ : Type u_2<VAR>B✝ : Type u_3<VAR>inst✝¹² : Semiring A✝<VAR>inst✝¹¹ : Semiring B✝<VAR>inst✝¹⁰ : Algebra R✝ A✝<VAR>inst✝⁹ : Algebra R✝ B✝<VAR>R : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>A : Type u_5<VAR>B : Type u_6<VAR>C : Type u_7<VAR>D : Type u_8<VAR>inst✝⁷ : Ring A<VAR>inst✝⁶ : Ring B<VAR>inst✝⁵ : Ring C<VAR>inst✝⁴ : Ring D<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : Algebra R C<VAR>inst✝ : Algebra R D<VAR>f : A →ₐ[R] B<VAR>g : C →ₐ[R] D<VAR>hf : Function.Surjective ⇑f<GOAL>Submodule.restrictScalars R (RingHom.ker (map f (AlgHom.id R C))) = Submodule.restrictScalars R (Ideal.map includeLeft (RingHom.ker f))
<VAR>R✝ : Type u_1<VAR>inst✝¹³ : CommSemiring R✝<VAR>A✝ : Type u_2<VAR>B✝ : Type u_3<VAR>inst✝¹² : Semiring A✝<VAR>inst✝¹¹ : Semiring B✝<VAR>inst✝¹⁰ : Algebra R✝ A✝<VAR>inst✝⁹ : Algebra R✝ B✝<VAR>R : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>A : Type u_5<VAR>B : Type u_6<VAR>C : Type u_7<VAR>D : Type u_8<VAR>inst✝⁷ : Ring A<VAR>inst✝⁶ : Ring B<VAR>inst✝⁵ : Ring C<VAR>inst✝⁴ : Ring D<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : Algebra R C<VAR>inst✝ : Algebra R D<VAR>f : A →ₐ[R] B<VAR>g : C →ₐ[R] D<VAR>hf : Function.Surjective ⇑f<VAR>this : Submodule.restrictScalars R (RingHom.ker (map f (AlgHom.id R C))) = LinearMap.ker (LinearMap.rTensor C f.toLinearMap)<GOAL>Submodule.restrictScalars R (RingHom.ker (map f (AlgHom.id R C))) = Submodule.restrictScalars R (Ideal.map includeLeft (RingHom.ker f))
<VAR>R✝ : Type u_1<VAR>inst✝¹³ : CommSemiring R✝<VAR>A✝ : Type u_2<VAR>B✝ : Type u_3<VAR>inst✝¹² : Semiring A✝<VAR>inst✝¹¹ : Semiring B✝<VAR>inst✝¹⁰ : Algebra R✝ A✝<VAR>inst✝⁹ : Algebra R✝ B✝<VAR>R : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>A : Type u_5<VAR>B : Type u_6<VAR>C : Type u_7<VAR>D : Type u_8<VAR>inst✝⁷ : Ring A<VAR>inst✝⁶ : Ring B<VAR>inst✝⁵ : Ring C<VAR>inst✝⁴ : Ring D<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : Algebra R C<VAR>inst✝ : Algebra R D<VAR>f : A →ₐ[R] B<VAR>g : C →ₐ[R] D<VAR>hf : Function.Surjective ⇑f<VAR>this : Submodule.restrictScalars R (RingHom.ker (map f (AlgHom.id R C))) = LinearMap.ker (LinearMap.rTensor C f.toLinearMap)<GOAL>LinearMap.ker (LinearMap.rTensor C f.toLinearMap) = LinearMap.range (LinearMap.rTensor C (Submodule.restrictScalars R (RingHom.ker f)).subtype)
<VAR>R✝ : Type u_1<VAR>inst✝¹³ : CommSemiring R✝<VAR>A✝ : Type u_2<VAR>B✝ : Type u_3<VAR>inst✝¹² : Semiring A✝<VAR>inst✝¹¹ : Semiring B✝<VAR>inst✝¹⁰ : Algebra R✝ A✝<VAR>inst✝⁹ : Algebra R✝ B✝<VAR>R : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>A : Type u_5<VAR>B : Type u_6<VAR>C : Type u_7<VAR>D : Type u_8<VAR>inst✝⁷ : Ring A<VAR>inst✝⁶ : Ring B<VAR>inst✝⁵ : Ring C<VAR>inst✝⁴ : Ring D<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : Algebra R C<VAR>inst✝ : Algebra R D<VAR>f : A →ₐ[R] B<VAR>g : C →ₐ[R] D<VAR>hf : Function.Surjective ⇑f<VAR>this : Submodule.restrictScalars R (RingHom.ker (map f (AlgHom.id R C))) = LinearMap.ker (LinearMap.rTensor C f.toLinearMap)<GOAL>LinearMap.range (LinearMap.rTensor C (LinearMap.ker f.toLinearMap).subtype) = LinearMap.range (LinearMap.rTensor C (Submodule.restrictScalars R (RingHom.ker f)).subtype)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ S₄ : ShortComplex C<VAR>φ✝ : S₁ ⟶ S₂<VAR>h₁✝ : S₁.HomologyData<VAR>h₂✝ : S₂.HomologyData<VAR>inst✝¹ : S₁.HasHomology<VAR>inst✝ : S₂.HasHomology<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.LeftHomologyData<VAR>h₂ : S₂.LeftHomologyData<GOAL>(leftHomologyMap' (𝟙 S₁) h₁ S₁.leftHomologyData ≫ leftHomologyMap' (𝟙 S₁) S₁.leftHomologyData S₁.homologyData.left) ≫ leftHomologyMap' φ S₁.homologyData.left S₂.homologyData.left = leftHomologyMap' φ h₁ h₂ ≫ leftHomologyMap' (𝟙 S₂) h₂ S₂.leftHomologyData ≫ leftHomologyMap' (𝟙 S₂) S₂.leftHomologyData S₂.homologyData.left
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>inst✝¹ : Category.{?u.43805, u_1} J<VAR>inst✝ : Category.{?u.43809, u_2} C<VAR>P✝ Q : Karoubi (J ⥤ C)<VAR>f : P✝ ⟶ Q<VAR>X : J<VAR>P : Karoubi (J ⥤ C)<VAR>j j' : J<VAR>φ : j ⟶ j'<GOAL>P.p.app j ≫ P.X.map φ = ((fun j => { X := P.X.obj j, p := P.p.app j, idem := ⋯ }) j).p ≫ (P.p.app j ≫ P.X.map φ) ≫ ((fun j => { X := P.X.obj j, p := P.p.app j, idem := ⋯ }) j').p
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>inst✝¹ : Category.{?u.43805, u_1} J<VAR>inst✝ : Category.{?u.43809, u_2} C<VAR>P✝ Q : Karoubi (J ⥤ C)<VAR>f : P✝ ⟶ Q<VAR>X : J<VAR>P : Karoubi (J ⥤ C)<VAR>j j' : J<VAR>φ : j ⟶ j'<GOAL>P.p.app j ≫ P.X.map φ = P.p.app j ≫ P.p.app j ≫ P.p.app j ≫ P.X.map φ
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>inst✝¹ : Category.{?u.43805, u_1} J<VAR>inst✝ : Category.{?u.43809, u_2} C<VAR>P✝ Q : Karoubi (J ⥤ C)<VAR>f : P✝ ⟶ Q<VAR>X : J<VAR>P : Karoubi (J ⥤ C)<VAR>j j' : J<VAR>φ : j ⟶ j'<VAR>h : (P.p ≫ P.p).app j = P.p.app j<GOAL>P.p.app j ≫ P.X.map φ = P.p.app j ≫ P.p.app j ≫ P.p.app j ≫ P.X.map φ
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>inst✝¹ : Category.{?u.43805, u_1} J<VAR>inst✝ : Category.{?u.43809, u_2} C<VAR>P✝ Q : Karoubi (J ⥤ C)<VAR>f : P✝ ⟶ Q<VAR>X : J<VAR>P : Karoubi (J ⥤ C)<VAR>j j' : J<VAR>φ : j ⟶ j'<VAR>h : P.p.app j ≫ P.p.app j = P.p.app j<GOAL>P.p.app j ≫ P.X.map φ = P.p.app j ≫ P.p.app j ≫ P.p.app j ≫ P.X.map φ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : MeasurableSingletonClass α<VAR>inst✝ : Fintype α<VAR>f : α → ℝ≥0∞<GOAL>∫⁻ (x : α), f x ∂μ = ∑ x : α, f x * μ {x}
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g : α → β<VAR>inst✝ : CommMonoid β<VAR>f : ℕ → β<VAR>n : ℕ<GOAL>∏ x ∈ range (n + 1), f x = (∏ x ∈ range n, f x) * f n
<VAR>ι✝ : Type u_1<VAR>κ✝ : Type u_2<VAR>α✝ : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s s₁ s₂ : Finset α✝<VAR>a : α✝<VAR>f✝ g✝ : α✝ → β<VAR>ι : Type u_6<VAR>κ : Type u_7<VAR>α : Type u_8<VAR>inst✝³ : Fintype ι<VAR>inst✝² : Fintype κ<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : DecidableEq κ<VAR>g : ι → κ<VAR>f : κ → α<GOAL>∏ j : κ, ∏ _i : { i // g i = j }, f j = ∏ i : ι, f (g i)
<VAR>ι✝ : Type u_1<VAR>κ✝ : Type u_2<VAR>α✝ : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s s₁ s₂ : Finset α✝<VAR>a : α✝<VAR>f✝ g✝ : α✝ → β<VAR>ι : Type u_6<VAR>κ : Type u_7<VAR>α : Type u_8<VAR>inst✝³ : Fintype ι<VAR>inst✝² : Fintype κ<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : DecidableEq κ<VAR>g : ι → κ<VAR>f : κ → α<GOAL>∏ j : κ, ∏ _i : { i // g i = j }, f j = ∏ j : κ, ∏ _i ∈ filter (fun i => g i = j) univ, f j
<VAR>ι✝ : Type u_1<VAR>κ✝ : Type u_2<VAR>α✝ : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s s₁ s₂ : Finset α✝<VAR>a : α✝<VAR>f✝ g✝ : α✝ → β<VAR>ι : Type u_6<VAR>κ : Type u_7<VAR>α : Type u_8<VAR>inst✝³ : Fintype ι<VAR>inst✝² : Fintype κ<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : DecidableEq κ<VAR>g : ι → κ<VAR>f : κ → α<VAR>j : κ<GOAL>∏ _i : { i // g i = j }, f j = ∏ _i ∈ filter (fun i => g i = j) univ, f j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>inst✝⁶ : Monoid α<VAR>inst✝⁵ : Zero α<VAR>inst✝⁴ : Zero β<VAR>inst✝³ : MulAction α β<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>inst✝ : SMulPosMono α β<VAR>hb : 0 ≤ b<VAR>h : 1 ≤ a<GOAL>b ≤ a • b
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>P Q : C<VAR>a : Pseudoelement P<VAR>a' : Over P<GOAL>pseudoApply 0 ⟦a'⟧ = 0
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>P Q : C<VAR>a : Pseudoelement P<VAR>a' : Over P<GOAL>⟦Over.mk (a'.hom ≫ 0)⟧ = ⟦Over.mk 0⟧
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>F G K L : CochainComplex C ℤ<VAR>n m n₁ n₂ n₁₂ : ℤ<VAR>z₁ : Cochain F G n₁<VAR>z₂ : Cochain G K n₂<VAR>h : n₁ + n₂ = n₁₂<VAR>m₁ m₂ m₁₂ : ℤ<VAR>h₁₂ : n₁₂ + 1 = m₁₂<VAR>h₁ : n₁ + 1 = m₁<VAR>h₂ : n₂ + 1 = m₂<GOAL>n₁ + m₂ = m₁₂
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>F G K L : CochainComplex C ℤ<VAR>n m n₁ n₂ n₁₂ : ℤ<VAR>z₁ : Cochain F G n₁<VAR>z₂ : Cochain G K n₂<VAR>h : n₁ + n₂ = n₁₂<VAR>m₁ m₂ m₁₂ : ℤ<VAR>h₁₂ : n₁₂ + 1 = m₁₂<VAR>h₁ : n₁ + 1 = m₁<VAR>h₂ : n₂ + 1 = m₂<GOAL>m₁ + n₂ = m₁₂
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>F G K L : CochainComplex C ℤ<VAR>n m n₁ n₂ : ℤ<VAR>z₁ : Cochain F G n₁<VAR>z₂ : Cochain G K n₂<VAR>p q : ℤ<VAR>hpq : p + (n₁ + n₂ + 1) = q<GOAL>(δ (n₁ + n₂) (n₁ + n₂ + 1) (z₁.comp z₂ ⋯)).v p q hpq = (z₁.comp (δ n₂ (n₂ + 1) z₂) ⋯).v p q hpq + n₂.negOnePow • ((δ n₁ (n₁ + 1) z₁).comp z₂ ⋯).v p q hpq
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>F G K L : CochainComplex C ℤ<VAR>n m n₁ n₂ : ℤ<VAR>z₁ : Cochain F G n₁<VAR>z₂ : Cochain G K n₂<VAR>p q : ℤ<VAR>hpq : p + (n₁ + n₂ + 1) = q<GOAL>(z₁.v p (p + n₁) ⋯ ≫ z₂.v (p + n₁) (p + n₁ + n₂) ⋯) ≫ K.d (p + n₁ + n₂) q + (n₁ + n₂ + 1).negOnePow • F.d p (p + 1) ≫ z₁.v (p + 1) (p + n₁ + 1) ⋯ ≫ z₂.v (p + n₁ + 1) q ⋯ = z₁.v p (p + n₁) ⋯ ≫ (z₂.v (p + n₁) (p + n₁ + n₂) ⋯ ≫ K.d (p + n₁ + n₂) q + (n₂ + 1).negOnePow • G.d (p + n₁) (p + n₁ + 1) ≫ z₂.v (p + n₁ + 1) q ⋯) + n₂.negOnePow • (z₁.v p (p + n₁) ⋯ ≫ G.d (p + n₁) (p + n₁ + 1) + (n₁ + 1).negOnePow • F.d p (p + 1) ≫ z₁.v (p + 1) (p + n₁ + 1) ⋯) ≫ z₂.v (p + n₁ + 1) q ⋯
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>F G K L : CochainComplex C ℤ<VAR>n m n₁ n₂ : ℤ<VAR>z₁ : Cochain F G n₁<VAR>z₂ : Cochain G K n₂<VAR>p q : ℤ<VAR>hpq : p + (n₁ + n₂ + 1) = q<GOAL>z₁.v p (p + n₁) ⋯ ≫ z₂.v (p + n₁) (p + n₁ + n₂) ⋯ ≫ K.d (p + n₁ + n₂) q + -((n₂.negOnePow * n₁.negOnePow) • F.d p (p + 1) ≫ z₁.v (p + 1) (p + n₁ + 1) ⋯ ≫ z₂.v (p + n₁ + 1) q ⋯) = z₁.v p (p + n₁) ⋯ ≫ z₂.v (p + n₁) (p + n₁ + n₂) ⋯ ≫ K.d (p + n₁ + n₂) q + -(n₂.negOnePow • z₁.v p (p + n₁) ⋯ ≫ G.d (p + n₁) (p + n₁ + 1) ≫ z₂.v (p + n₁ + 1) q ⋯) + (n₂.negOnePow • z₁.v p (p + n₁) ⋯ ≫ G.d (p + n₁) (p + n₁ + 1) ≫ z₂.v (p + n₁ + 1) q ⋯ + -((n₂.negOnePow * n₁.negOnePow) • F.d p (p + 1) ≫ z₁.v (p + 1) (p + n₁ + 1) ⋯ ≫ z₂.v (p + n₁ + 1) q ⋯))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁴ : Countable ι<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : Zero β<VAR>inst✝¹ : SemilatticeSup β<VAR>inst✝ : ContinuousSup β<VAR>hf : FinStronglyMeasurable f μ<VAR>hg : FinStronglyMeasurable g μ<GOAL>FinStronglyMeasurable (f ⊔ g) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁴ : Countable ι<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : Zero β<VAR>inst✝¹ : SemilatticeSup β<VAR>inst✝ : ContinuousSup β<VAR>hf : FinStronglyMeasurable f μ<VAR>hg : FinStronglyMeasurable g μ<VAR>n : ℕ<GOAL>μ (support ↑((fun n => hf.approx n ⊔ hg.approx n) n)) < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁴ : Countable ι<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : Zero β<VAR>inst✝¹ : SemilatticeSup β<VAR>inst✝ : ContinuousSup β<VAR>hf : FinStronglyMeasurable f μ<VAR>hg : FinStronglyMeasurable g μ<VAR>n : ℕ<GOAL>μ (support ↑(hf.approx n) ∪ support ↑(hg.approx n)) < ⊤
<VAR>M : Type u_1<VAR>inst✝² : Monoid M<VAR>s✝ : Set M<VAR>A : Type u_2<VAR>inst✝¹ : AddMonoid A<VAR>t : Set A<VAR>γ : Type u_3<VAR>inst✝ : Monoid γ<VAR>f : M → γ<VAR>hf : IsMonoidHom f<VAR>s : Set M<VAR>hs : IsSubmonoid s<VAR>a b : γ<VAR>x✝¹ : a ∈ f '' s<VAR>x✝ : b ∈ f '' s<VAR>x : M<VAR>hx : x ∈ s ∧ f x = a<VAR>y : M<VAR>hy : y ∈ s ∧ f y = b<GOAL>f (x * y) = a * b
<VAR>M✝ : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝³ : Monoid M✝<VAR>inst✝² : SetLike B M✝<VAR>inst✝¹ : SubmonoidClass B M✝<VAR>S✝ : B<VAR>s : Submonoid M✝<VAR>M : Type u_4<VAR>inst✝ : CommMonoid M<VAR>S : Submonoid M<VAR>m : Multiset ↥S<GOAL>(Multiset.map Subtype.val m).prod ∈ S
<VAR>M✝ : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝³ : Monoid M✝<VAR>inst✝² : SetLike B M✝<VAR>inst✝¹ : SubmonoidClass B M✝<VAR>S✝ : B<VAR>s : Submonoid M✝<VAR>M : Type u_4<VAR>inst✝ : CommMonoid M<VAR>S : Submonoid M<VAR>m : Multiset ↥S<GOAL>↑m.prod ∈ S
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>m n : ℕ<VAR>s : Simplex k P m<VAR>e : Fin (m + 1) ≃ Fin (n + 1)<GOAL>Set.range (s.reindex e).points = Set.range s.points
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : CommRing α<VAR>A B : Matrix n n α<VAR>inst✝ : StarRing α<GOAL>A⁻¹ᴴ = Aᴴ⁻¹
<VAR>R : Type u_1<VAR>n : ℕ<GOAL>Squarefree ↑n ↔ Squarefree n
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : _root_.Finite ι<VAR>P : RootSystem ι R M N<VAR>inst✝¹ : CharZero R<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>p : PerfectPairing R M N<VAR>root : ι ↪ M<VAR>coroot : ι ↪ N<VAR>hp : ∀ (i : ι), (p.toLin (root i)) (coroot i) = 2<VAR>hs : ∀ (i : ι), MapsTo (⇑(preReflection (root i) (p.toLin.flip (coroot i)))) (range ⇑root) (range ⇑root)<VAR>hsp : span R (range ⇑root) = ⊤<VAR>i j k : ι<VAR>α : M := root i<VAR>β : M := root j<VAR>α' : N := coroot i<VAR>β' : N := coroot j<VAR>sα : End R M := preReflection α (p.toLin.flip α')<VAR>hk : root k = sα β<VAR>sβ : End R M := preReflection β (p.toLin.flip β')<VAR>sα' : End R N := preReflection α' (p.toLin α)<GOAL>coroot k = (preReflection α' (p.toLin α)) β'
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : _root_.Finite ι<VAR>P : RootSystem ι R M N<VAR>inst✝¹ : CharZero R<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>p : PerfectPairing R M N<VAR>root : ι ↪ M<VAR>coroot : ι ↪ N<VAR>hp : ∀ (i : ι), (p.toLin (root i)) (coroot i) = 2<VAR>hs : ∀ (i : ι), MapsTo (⇑(preReflection (root i) (p.toLin.flip (coroot i)))) (range ⇑root) (range ⇑root)<VAR>hsp : span R (range ⇑root) = ⊤<VAR>i j k : ι<VAR>α : M := root i<VAR>β : M := root j<VAR>α' : N := coroot i<VAR>β' : N := coroot j<VAR>sα : End R M := preReflection α (p.toLin.flip α')<VAR>hk : root k = sα β<VAR>sβ : End R M := preReflection β (p.toLin.flip β')<VAR>sα' : End R N := preReflection α' (p.toLin α)<VAR>hij : preReflection (sα β) (p.toLin.flip (sα' β')) = sα ∘ₗ sβ ∘ₗ sα<GOAL>coroot k = (preReflection α' (p.toLin α)) β'
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : _root_.Finite ι<VAR>P : RootSystem ι R M N<VAR>inst✝¹ : CharZero R<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>p : PerfectPairing R M N<VAR>root : ι ↪ M<VAR>coroot : ι ↪ N<VAR>hp : ∀ (i : ι), (p.toLin (root i)) (coroot i) = 2<VAR>hs : ∀ (i : ι), MapsTo (⇑(preReflection (root i) (p.toLin.flip (coroot i)))) (range ⇑root) (range ⇑root)<VAR>hsp : span R (range ⇑root) = ⊤<VAR>i j k : ι<VAR>α : M := root i<VAR>β : M := root j<VAR>α' : N := coroot i<VAR>β' : N := coroot j<VAR>sα : End R M := preReflection α (p.toLin.flip α')<VAR>hk : root k = sα β<VAR>sβ : End R M := preReflection β (p.toLin.flip β')<VAR>sα' : End R N := preReflection α' (p.toLin α)<VAR>hij : preReflection (sα β) (p.toLin.flip (sα' β')) = sα ∘ₗ sβ ∘ₗ sα<VAR>hk₀ : root k ≠ 0<GOAL>coroot k = (preReflection α' (p.toLin α)) β'
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>inst✝² : _root_.Finite ι<VAR>P : RootSystem ι R M N<VAR>inst✝¹ : CharZero R<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>p : PerfectPairing R M N<VAR>root : ι ↪ M<VAR>coroot : ι ↪ N<VAR>hp : ∀ (i : ι), (p.toLin (root i)) (coroot i) = 2<VAR>hs : ∀ (i : ι), MapsTo (⇑(preReflection (root i) (p.toLin.flip (coroot i)))) (range ⇑root) (range ⇑root)<VAR>hsp : span R (range ⇑root) = ⊤<VAR>i j k : ι<VAR>α : M := root i<VAR>β : M := root j<VAR>α' : N := coroot i<VAR>β' : N := coroot j<VAR>sα : End R M := preReflection α (p.toLin.flip α')<VAR>hk : root k = sα β<VAR>sβ : End R M := preReflection β (p.toLin.flip β')<VAR>sα' : End R N := preReflection α' (p.toLin α)<VAR>hij : preReflection (sα β) (p.toLin.flip (sα' β')) = sα ∘ₗ sβ ∘ₗ sα<VAR>hk₀ : root k ≠ 0<GOAL>p.toLin.flip (coroot k) = p.toLin.flip ((preReflection α' (p.toLin α)) β')