ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : Group G'<VAR>inst✝⁴ : Group G''<VAR>A : Type u_4<VAR>inst✝³ : AddGroup A<VAR>N : Type u_5<VAR>P : Type u_6<VAR>inst✝² : Group N<VAR>inst✝¹ : Group P<VAR>K : Subgroup G<VAR>M : Type u_7<VAR>inst✝ : MulOneClass M<VAR>f : G →* M<VAR>h : f.ker = ⊥<VAR>x y : G<VAR>hxy : f x = f y<GOAL>x = y
<VAR>X : Type u_1<VAR>k : ℕ<VAR>h : k ≠ 0<VAR>a : FreeAbelianGroup X<GOAL>(k • a).support = a.support
<VAR>X : Type u_1<VAR>k : ℕ<VAR>h : k ≠ 0<VAR>a : FreeAbelianGroup X<GOAL>↑k ≠ 0
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝¹¹ : CommSemiring ι<VAR>inst✝¹⁰ : Module ι (Additive ℤˣ)<VAR>inst✝⁹ : DecidableEq ι<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Ring A<VAR>inst✝⁶ : Ring B<VAR>inst✝⁵ : Algebra R A<VAR>inst✝⁴ : Algebra R B<VAR>𝒜 : ι → Submodule R A<VAR>ℬ : ι → Submodule R B<VAR>inst✝³ : GradedAlgebra 𝒜<VAR>inst✝² : GradedAlgebra ℬ<VAR>C : Type ?u.815509<VAR>inst✝¹ : Ring C<VAR>inst✝ : Algebra R C<VAR>i j : ι<VAR>a : ↥(𝒜 i)<VAR>b : ↥(ℬ j)<GOAL>(auxEquiv R ℬ 𝒜) ((comm 𝒜 ℬ) (↑a ᵍ⊗ₜ[R] ↑b)) = (auxEquiv R ℬ 𝒜) ((-1) ^ (j * i) • ↑b ᵍ⊗ₜ[R] ↑a)
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝¹¹ : CommSemiring ι<VAR>inst✝¹⁰ : Module ι (Additive ℤˣ)<VAR>inst✝⁹ : DecidableEq ι<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Ring A<VAR>inst✝⁶ : Ring B<VAR>inst✝⁵ : Algebra R A<VAR>inst✝⁴ : Algebra R B<VAR>𝒜 : ι → Submodule R A<VAR>ℬ : ι → Submodule R B<VAR>inst✝³ : GradedAlgebra 𝒜<VAR>inst✝² : GradedAlgebra ℬ<VAR>C : Type ?u.815509<VAR>inst✝¹ : Ring C<VAR>inst✝ : Algebra R C<VAR>i j : ι<VAR>a : ↥(𝒜 i)<VAR>b : ↥(ℬ j)<GOAL>↑↑((-1) ^ (j * i)) • (lof R ι (fun x => ↥(ℬ x)) j) b ⊗ₜ[R] (lof R ι (fun x => ↥(𝒜 x)) i) a = (auxEquiv R ℬ 𝒜) (↑↑((-1) ^ (j * i)) • ↑b ᵍ⊗ₜ[R] ↑a)
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝¹¹ : CommSemiring ι<VAR>inst✝¹⁰ : Module ι (Additive ℤˣ)<VAR>inst✝⁹ : DecidableEq ι<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : Ring A<VAR>inst✝⁶ : Ring B<VAR>inst✝⁵ : Algebra R A<VAR>inst✝⁴ : Algebra R B<VAR>𝒜 : ι → Submodule R A<VAR>ℬ : ι → Submodule R B<VAR>inst✝³ : GradedAlgebra 𝒜<VAR>inst✝² : GradedAlgebra ℬ<VAR>C : Type ?u.815509<VAR>inst✝¹ : Ring C<VAR>inst✝ : Algebra R C<VAR>i j : ι<VAR>a : ↥(𝒜 i)<VAR>b : ↥(ℬ j)<GOAL>↑↑((-1) ^ (j * i)) • (lof R ι (fun x => ↥(ℬ x)) j) b ⊗ₜ[R] (lof R ι (fun x => ↥(𝒜 x)) i) a = ↑↑((-1) ^ (j * i)) • (decompose ℬ) ↑b ⊗ₜ[R] (decompose 𝒜) ↑a
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹² : Category.{u_4, u_1} C<VAR>inst✝¹¹ : Category.{u_6, u_2} D<VAR>F : C ⥤ D<VAR>ι : Type u_3<VAR>c : ComplexShape ι<VAR>inst✝¹⁰ : Preadditive C<VAR>inst✝⁹ : Preadditive D<VAR>inst✝⁸ : CategoryWithHomology C<VAR>inst✝⁷ : CategoryWithHomology D<VAR>inst✝⁶ : (HomologicalComplex.quasiIso C c).HasLocalization<VAR>inst✝⁵ : (HomologicalComplex.quasiIso D c).HasLocalization<VAR>inst✝⁴ : F.Additive<VAR>inst✝³ : F.PreservesHomology<VAR>inst✝² : c.QFactorsThroughHomotopy C<VAR>inst✝¹ : c.QFactorsThroughHomotopy D<VAR>inst✝ : (HomotopyCategory.quotient C c).IsLocalization (HomologicalComplex.homotopyEquivalences C c)<VAR>K : HomologicalComplex C c<GOAL>(Localization.liftNatTrans (HomotopyCategory.quotient C c) (HomologicalComplex.homotopyEquivalences C c) (HomotopyCategory.quotient C c ⋙ HomologicalComplexUpToQuasiIso.Qh ⋙ F.mapHomologicalComplexUpToQuasiIso c) (HomotopyCategory.quotient C c ⋙ F.mapHomotopyCategory c ⋙ HomologicalComplexUpToQuasiIso.Qh) (HomologicalComplexUpToQuasiIso.Qh ⋙ F.mapHomologicalComplexUpToQuasiIso c) (F.mapHomotopyCategory c ⋙ HomologicalComplexUpToQuasiIso.Qh) (F.mapHomologicalComplexUpToQuasiIsoFactors c).hom).app ((HomotopyCategory.quotient C c).obj K) = (F.mapHomologicalComplexUpToQuasiIso c).map ((HomologicalComplexUpToQuasiIso.quotientCompQhIso C c).hom.app K) ≫ (F.mapHomologicalComplexUpToQuasiIsoFactors c).hom.app K ≫ (HomologicalComplexUpToQuasiIso.quotientCompQhIso D c).inv.app ((F.mapHomologicalComplex c).obj K) ≫ HomologicalComplexUpToQuasiIso.Qh.map ((F.mapHomotopyCategoryFactors c).inv.app K)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹² : Category.{u_4, u_1} C<VAR>inst✝¹¹ : Category.{u_6, u_2} D<VAR>F : C ⥤ D<VAR>ι : Type u_3<VAR>c : ComplexShape ι<VAR>inst✝¹⁰ : Preadditive C<VAR>inst✝⁹ : Preadditive D<VAR>inst✝⁸ : CategoryWithHomology C<VAR>inst✝⁷ : CategoryWithHomology D<VAR>inst✝⁶ : (HomologicalComplex.quasiIso C c).HasLocalization<VAR>inst✝⁵ : (HomologicalComplex.quasiIso D c).HasLocalization<VAR>inst✝⁴ : F.Additive<VAR>inst✝³ : F.PreservesHomology<VAR>inst✝² : c.QFactorsThroughHomotopy C<VAR>inst✝¹ : c.QFactorsThroughHomotopy D<VAR>inst✝ : (HomotopyCategory.quotient C c).IsLocalization (HomologicalComplex.homotopyEquivalences C c)<VAR>K : HomologicalComplex C c<GOAL>(Localization.Lifting.iso (HomotopyCategory.quotient C c) (HomologicalComplex.homotopyEquivalences C c) (HomotopyCategory.quotient C c ⋙ HomologicalComplexUpToQuasiIso.Qh ⋙ F.mapHomologicalComplexUpToQuasiIso c) (HomologicalComplexUpToQuasiIso.Qh ⋙ F.mapHomologicalComplexUpToQuasiIso c)).hom.app K ≫ (F.mapHomologicalComplexUpToQuasiIsoFactors c).hom.app K ≫ (Localization.Lifting.iso (HomotopyCategory.quotient C c) (HomologicalComplex.homotopyEquivalences C c) (HomotopyCategory.quotient C c ⋙ F.mapHomotopyCategory c ⋙ HomologicalComplexUpToQuasiIso.Qh) (F.mapHomotopyCategory c ⋙ HomologicalComplexUpToQuasiIso.Qh)).inv.app K = (F.mapHomologicalComplexUpToQuasiIso c).map ((HomologicalComplexUpToQuasiIso.quotientCompQhIso C c).hom.app K) ≫ (F.mapHomologicalComplexUpToQuasiIsoFactors c).hom.app K ≫ (HomologicalComplexUpToQuasiIso.quotientCompQhIso D c).inv.app ((F.mapHomologicalComplex c).obj K) ≫ HomologicalComplexUpToQuasiIso.Qh.map ((F.mapHomotopyCategoryFactors c).inv.app K)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹² : Category.{u_4, u_1} C<VAR>inst✝¹¹ : Category.{u_6, u_2} D<VAR>F : C ⥤ D<VAR>ι : Type u_3<VAR>c : ComplexShape ι<VAR>inst✝¹⁰ : Preadditive C<VAR>inst✝⁹ : Preadditive D<VAR>inst✝⁸ : CategoryWithHomology C<VAR>inst✝⁷ : CategoryWithHomology D<VAR>inst✝⁶ : (HomologicalComplex.quasiIso C c).HasLocalization<VAR>inst✝⁵ : (HomologicalComplex.quasiIso D c).HasLocalization<VAR>inst✝⁴ : F.Additive<VAR>inst✝³ : F.PreservesHomology<VAR>inst✝² : c.QFactorsThroughHomotopy C<VAR>inst✝¹ : c.QFactorsThroughHomotopy D<VAR>inst✝ : (HomotopyCategory.quotient C c).IsLocalization (HomologicalComplex.homotopyEquivalences C c)<VAR>K : HomologicalComplex C c<GOAL>𝟙 ((F.mapHomologicalComplexUpToQuasiIso c).obj (HomologicalComplexUpToQuasiIso.Qh.obj ((HomotopyCategory.quotient C c).obj K))) ≫ (F.mapHomologicalComplexUpToQuasiIsoFactors c).hom.app K ≫ 𝟙 (HomologicalComplexUpToQuasiIso.Qh.obj ((HomotopyCategory.quotient D c).obj ((F.mapHomologicalComplex c).obj ((HomotopyCategory.quotient C c).obj K).as))) = (F.mapHomologicalComplexUpToQuasiIso c).map ((HomologicalComplexUpToQuasiIso.quotientCompQhIso C c).hom.app K) ≫ (F.mapHomologicalComplexUpToQuasiIsoFactors c).hom.app K ≫ (HomologicalComplexUpToQuasiIso.quotientCompQhIso D c).inv.app ((F.mapHomologicalComplex c).obj K) ≫ HomologicalComplexUpToQuasiIso.Qh.map ((F.mapHomotopyCategoryFactors c).inv.app K)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹² : Category.{u_4, u_1} C<VAR>inst✝¹¹ : Category.{u_6, u_2} D<VAR>F : C ⥤ D<VAR>ι : Type u_3<VAR>c : ComplexShape ι<VAR>inst✝¹⁰ : Preadditive C<VAR>inst✝⁹ : Preadditive D<VAR>inst✝⁸ : CategoryWithHomology C<VAR>inst✝⁷ : CategoryWithHomology D<VAR>inst✝⁶ : (HomologicalComplex.quasiIso C c).HasLocalization<VAR>inst✝⁵ : (HomologicalComplex.quasiIso D c).HasLocalization<VAR>inst✝⁴ : F.Additive<VAR>inst✝³ : F.PreservesHomology<VAR>inst✝² : c.QFactorsThroughHomotopy C<VAR>inst✝¹ : c.QFactorsThroughHomotopy D<VAR>inst✝ : (HomotopyCategory.quotient C c).IsLocalization (HomologicalComplex.homotopyEquivalences C c)<VAR>K : HomologicalComplex C c<GOAL>(F.mapHomologicalComplexUpToQuasiIsoFactors c).hom.app K = (F.mapHomologicalComplexUpToQuasiIso c).map ((HomologicalComplexUpToQuasiIso.quotientCompQhIso C c).hom.app K) ≫ (F.mapHomologicalComplexUpToQuasiIsoFactors c).hom.app K ≫ (HomologicalComplexUpToQuasiIso.quotientCompQhIso D c).inv.app ((F.mapHomologicalComplex c).obj K) ≫ HomologicalComplexUpToQuasiIso.Qh.map ((F.mapHomotopyCategoryFactors c).inv.app K)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹² : Category.{u_4, u_1} C<VAR>inst✝¹¹ : Category.{u_6, u_2} D<VAR>F : C ⥤ D<VAR>ι : Type u_3<VAR>c : ComplexShape ι<VAR>inst✝¹⁰ : Preadditive C<VAR>inst✝⁹ : Preadditive D<VAR>inst✝⁸ : CategoryWithHomology C<VAR>inst✝⁷ : CategoryWithHomology D<VAR>inst✝⁶ : (HomologicalComplex.quasiIso C c).HasLocalization<VAR>inst✝⁵ : (HomologicalComplex.quasiIso D c).HasLocalization<VAR>inst✝⁴ : F.Additive<VAR>inst✝³ : F.PreservesHomology<VAR>inst✝² : c.QFactorsThroughHomotopy C<VAR>inst✝¹ : c.QFactorsThroughHomotopy D<VAR>inst✝ : (HomotopyCategory.quotient C c).IsLocalization (HomologicalComplex.homotopyEquivalences C c)<VAR>K : HomologicalComplex C c<GOAL>(F.mapHomologicalComplexUpToQuasiIsoFactors c).hom.app K = (F.mapHomologicalComplexUpToQuasiIso c).map (𝟙 (HomologicalComplexUpToQuasiIso.Qh.obj ((HomotopyCategory.quotient C c).obj K))) ≫ (F.mapHomologicalComplexUpToQuasiIsoFactors c).hom.app K ≫ 𝟙 (HomologicalComplexUpToQuasiIso.Qh.obj ((F.mapHomotopyCategory c).obj ((HomotopyCategory.quotient C c).obj K))) ≫ HomologicalComplexUpToQuasiIso.Qh.map (𝟙 ((F.mapHomotopyCategory c).obj ((HomotopyCategory.quotient C c).obj K)))
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>f : R → ℝ<VAR>c : ℝ<VAR>f_nonneg : 0 ≤ f<VAR>f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y<VAR>x : R<GOAL>BddAbove (Set.range fun y => f (x * y) / f y)
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>f : R → ℝ<VAR>c : ℝ<VAR>f_nonneg : 0 ≤ f<VAR>f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y<VAR>x : R<GOAL>c * f x ∈ upperBounds (Set.range fun y => f (x * y) / f y)
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>F : J ⥤ Cat<VAR>X Y Z : limit (F ⋙ objects)<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>j j' : J<VAR>h : j ⟶ j'<GOAL>(homDiagram X Z).map h ((fun j => limit.π (homDiagram X Y) j f ≫ limit.π (homDiagram Y Z) j g) j) = (fun j => limit.π (homDiagram X Y) j f ≫ limit.π (homDiagram Y Z) j g) j'
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>F : J ⥤ Cat<VAR>X✝ Y✝ : limit (F ⋙ objects)<VAR>x✝ : X✝ ⟶ Y✝<GOAL>𝟙 X✝ ≫ x✝ = x✝
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>F : J ⥤ Cat<VAR>X✝ Y✝ : limit (F ⋙ objects)<VAR>x✝ : X✝ ⟶ Y✝<GOAL>∀ (j : J), limit.π (homDiagram X✝ Y✝) j (𝟙 X✝ ≫ x✝) = limit.π (homDiagram X✝ Y✝) j x✝
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>F : J ⥤ Cat<VAR>X✝ Y✝ : limit (F ⋙ objects)<VAR>x✝ : X✝ ⟶ Y✝<GOAL>x✝ ≫ 𝟙 Y✝ = x✝
<VAR>J : Type v<VAR>inst✝ : SmallCategory J<VAR>F : J ⥤ Cat<VAR>X✝ Y✝ : limit (F ⋙ objects)<VAR>x✝ : X✝ ⟶ Y✝<GOAL>∀ (j : J), limit.π (homDiagram X✝ Y✝) j (x✝ ≫ 𝟙 Y✝) = limit.π (homDiagram X✝ Y✝) j x✝
<VAR>n : ℕ+<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : Algebra A B<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>h : IsCyclotomicExtension (S ∪ T) A B<VAR>this : {b | ∃ n ∈ S ∪ T, b ^ ↑n = 1} = {b | ∃ n ∈ S, b ^ ↑n = 1} ∪ {b | ∃ n ∈ T, b ^ ↑n = 1}<GOAL>IsCyclotomicExtension T (↥(adjoin A {b | ∃ a ∈ S, b ^ ↑a = 1})) B
<VAR>n : ℕ+<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : Algebra A B<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>h : IsCyclotomicExtension (S ∪ T) A B<VAR>this : {b | ∃ n ∈ S ∪ T, b ^ ↑n = 1} = {b | ∃ n ∈ S, b ^ ↑n = 1} ∪ {b | ∃ n ∈ T, b ^ ↑n = 1}<VAR>b : B<GOAL>b ∈ adjoin ↥(adjoin A {b | ∃ a ∈ S, b ^ ↑a = 1}) {b | ∃ n ∈ T, b ^ ↑n = 1}
<VAR>n : ℕ+<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : Algebra A B<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>this : {b | ∃ n ∈ S ∪ T, b ^ ↑n = 1} = {b | ∃ n ∈ S, b ^ ↑n = 1} ∪ {b | ∃ n ∈ T, b ^ ↑n = 1}<VAR>b : B<VAR>h : b ∈ adjoin A {b | ∃ n ∈ S ∪ T, b ^ ↑n = 1}<GOAL>b ∈ adjoin ↥(adjoin A {b | ∃ a ∈ S, b ^ ↑a = 1}) {b | ∃ n ∈ T, b ^ ↑n = 1}
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type x<VAR>inst✝ : OrderedAddCommGroup β<VAR>f g : α → β<VAR>a : α<VAR>s : Set α<VAR>l : Filter α<VAR>hf : IsMinOn f s a<VAR>hg : IsMaxOn g s a<GOAL>IsMinOn (fun x => f x - g x) s a
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>p✝ q : R[X]<VAR>inst✝ : Infinite R<VAR>p : R[X]<VAR>h : ∀ (x : R), eval x p = 0<GOAL>p = 0
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor E P<VAR>s t : Set E<VAR>a : E<VAR>r : ℝ<GOAL>Convex ℝ (closedBall a r)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν✝ μ ν : Measure α<VAR>inst✝ : μ.HaveLebesgueDecomposition ν<GOAL>ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν = μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>u : δ → δ → Prop<VAR>f : r ↪r s<VAR>b : β<VAR>a : α<VAR>H : ∀ (y : β), s y (f a) → Acc s y<VAR>IH : ∀ (y : β), s y (f a) → ∀ (a : α), f a = y → Acc r a<GOAL>Acc r 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>a a' : α<VAR>b b' : M<VAR>hb : b ≠ 0<VAR>hb' : b' ≠ 0<VAR>i j : α<GOAL>Disjoint (single i b).support (single j b').support ↔ i ≠ j
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : MeasurableSpace E<VAR>inst✝⁵ : BorelSpace E<VAR>inst✝⁴ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝³ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>r : ℝ<VAR>hr : 0 ≤ r<VAR>s : Set E<GOAL>μ (r • s) = ENNReal.ofReal (r ^ finrank ℝ E) * μ s
<VAR>c : Cardinal.{u_1}<VAR>h : ℵ₀ ≤ c<GOAL>c = aleph (c.alephIdx - ω)
<VAR>c : Cardinal.{u_1}<VAR>h : ℵ₀ ≤ c<GOAL>ω ≤ c.alephIdx
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝³ : Monoid M<VAR>inst✝² : Monoid N<VAR>F : Type u_7<VAR>inst✝¹ : FunLike F M N<VAR>inst✝ : MonoidHomClass F M N<VAR>f : F<VAR>x y : M<VAR>u : Mˣ<VAR>ha : x * ↑u = y<GOAL>f x ~ᵤ f y
<VAR>n✝ m : ℕ<VAR>p : Fin (n✝ + 1)<VAR>i✝ j✝ : Fin n✝<VAR>n : ℕ<VAR>i : Fin (n + 1)<VAR>j : Fin n<GOAL>i.castSucc.succAbove j.castSucc = (i.succAbove j).castSucc
<VAR>n✝ m : ℕ<VAR>p : Fin (n✝ + 1)<VAR>i✝ j✝ : Fin n✝<VAR>n : ℕ<VAR>i : Fin (n + 1)<VAR>j : Fin n<VAR>h : i ≤ j.castSucc<GOAL>i.castSucc.succAbove j.castSucc = (i.succAbove j).castSucc
<VAR>n✝ m : ℕ<VAR>p : Fin (n✝ + 1)<VAR>i✝ j✝ : Fin n✝<VAR>n : ℕ<VAR>i : Fin (n + 1)<VAR>j : Fin n<VAR>h : j.castSucc < i<GOAL>i.castSucc.succAbove j.castSucc = (i.succAbove j).castSucc
<VAR>R : Type u_1<VAR>inst✝⁹ : CommRing R<VAR>S : Type u_2<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : Algebra R S<VAR>inst✝⁶ : IsDomain R<VAR>inst✝⁵ : IsDomain S<VAR>inst✝⁴ : IsDedekindDomain R<VAR>inst✝³ : IsDedekindDomain S<VAR>inst✝² : Module.Finite R S<VAR>inst✝¹ : Module.Free R S<VAR>I J : Ideal S<VAR>inst✝ : Nontrivial R<GOAL>spanNorm R (I * J) = spanNorm R I * spanNorm R J
<VAR>R : Type u_1<VAR>inst✝⁹ : CommRing R<VAR>S : Type u_2<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : Algebra R S<VAR>inst✝⁶ : IsDomain R<VAR>inst✝⁵ : IsDomain S<VAR>inst✝⁴ : IsDedekindDomain R<VAR>inst✝³ : IsDedekindDomain S<VAR>inst✝² : Module.Finite R S<VAR>inst✝¹ : Module.Free R S<VAR>I J : Ideal S<VAR>inst✝ : Nontrivial R<VAR>h✝ : Subsingleton S<GOAL>spanNorm R (I * J) = spanNorm R I * spanNorm R J
<VAR>R : Type u_1<VAR>inst✝⁹ : CommRing R<VAR>S : Type u_2<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : Algebra R S<VAR>inst✝⁶ : IsDomain R<VAR>inst✝⁵ : IsDomain S<VAR>inst✝⁴ : IsDedekindDomain R<VAR>inst✝³ : IsDedekindDomain S<VAR>inst✝² : Module.Finite R S<VAR>inst✝¹ : Module.Free R S<VAR>I J : Ideal S<VAR>inst✝ : Nontrivial R<VAR>h✝ : Nontrivial S<GOAL>spanNorm R (I * J) = spanNorm R I * spanNorm R J
<VAR>R : Type u_1<VAR>inst✝⁹ : CommRing R<VAR>S : Type u_2<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : Algebra R S<VAR>inst✝⁶ : IsDomain R<VAR>inst✝⁵ : IsDomain S<VAR>inst✝⁴ : IsDedekindDomain R<VAR>inst✝³ : IsDedekindDomain S<VAR>inst✝² : Module.Finite R S<VAR>inst✝¹ : Module.Free R S<VAR>I J : Ideal S<VAR>inst✝ : Nontrivial R<VAR>h✝ : Nontrivial S<GOAL>∀ (P : Ideal R) (x : P.IsMaximal), map (algebraMap R (Localization.AtPrime P)) (spanNorm R (I * J)) = map (algebraMap R (Localization.AtPrime P)) (spanNorm R I * spanNorm R J)
<VAR>R : Type u_1<VAR>inst✝⁹ : CommRing R<VAR>S : Type u_2<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : Algebra R S<VAR>inst✝⁶ : IsDomain R<VAR>inst✝⁵ : IsDomain S<VAR>inst✝⁴ : IsDedekindDomain R<VAR>inst✝³ : IsDedekindDomain S<VAR>inst✝² : Module.Finite R S<VAR>inst✝¹ : Module.Free R S<VAR>I J : Ideal S<VAR>inst✝ : Nontrivial R<VAR>h✝ : Nontrivial S<VAR>P : Ideal R<VAR>hP : P.IsMaximal<VAR>hP0 : ¬P = ⊥<VAR>P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl<VAR>this : Algebra (Localization.AtPrime P) (Localization P') := localizationAlgebra P.primeCompl S<GOAL>map (algebraMap R (Localization.AtPrime P)) (spanNorm R (I * J)) = map (algebraMap R (Localization.AtPrime P)) (spanNorm R I * spanNorm R J)
<VAR>R : Type u_1<VAR>inst✝⁹ : CommRing R<VAR>S : Type u_2<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : Algebra R S<VAR>inst✝⁶ : IsDomain R<VAR>inst✝⁵ : IsDomain S<VAR>inst✝⁴ : IsDedekindDomain R<VAR>inst✝³ : IsDedekindDomain S<VAR>inst✝² : Module.Finite R S<VAR>inst✝¹ : Module.Free R S<VAR>I J : Ideal S<VAR>inst✝ : Nontrivial R<VAR>h✝ : Nontrivial S<VAR>P : Ideal R<VAR>hP : P.IsMaximal<VAR>hP0 : ¬P = ⊥<VAR>P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl<VAR>this✝ : Algebra (Localization.AtPrime P) (Localization P') := localizationAlgebra P.primeCompl S<VAR>this : IsScalarTower R (Localization.AtPrime P) (Localization P')<GOAL>map (algebraMap R (Localization.AtPrime P)) (spanNorm R (I * J)) = map (algebraMap R (Localization.AtPrime P)) (spanNorm R I * spanNorm R J)
<VAR>R : Type u_1<VAR>inst✝⁹ : CommRing R<VAR>S : Type u_2<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : Algebra R S<VAR>inst✝⁶ : IsDomain R<VAR>inst✝⁵ : IsDomain S<VAR>inst✝⁴ : IsDedekindDomain R<VAR>inst✝³ : IsDedekindDomain S<VAR>inst✝² : Module.Finite R S<VAR>inst✝¹ : Module.Free R S<VAR>I J : Ideal S<VAR>inst✝ : Nontrivial R<VAR>h✝ : Nontrivial S<VAR>P : Ideal R<VAR>hP : P.IsMaximal<VAR>hP0 : ¬P = ⊥<VAR>P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl<VAR>this✝ : Algebra (Localization.AtPrime P) (Localization P') := localizationAlgebra P.primeCompl S<VAR>this : IsScalarTower R (Localization.AtPrime P) (Localization P')<VAR>h : P' ≤ S⁰<GOAL>map (algebraMap R (Localization.AtPrime P)) (spanNorm R (I * J)) = map (algebraMap R (Localization.AtPrime P)) (spanNorm R I * spanNorm R J)
<VAR>R : Type u_1<VAR>inst✝⁹ : CommRing R<VAR>S : Type u_2<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : Algebra R S<VAR>inst✝⁶ : IsDomain R<VAR>inst✝⁵ : IsDomain S<VAR>inst✝⁴ : IsDedekindDomain R<VAR>inst✝³ : IsDedekindDomain S<VAR>inst✝² : Module.Finite R S<VAR>inst✝¹ : Module.Free R S<VAR>I J : Ideal S<VAR>inst✝ : Nontrivial R<VAR>h✝ : Nontrivial S<VAR>P : Ideal R<VAR>hP : P.IsMaximal<VAR>hP0 : ¬P = ⊥<VAR>P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl<VAR>this✝¹ : Algebra (Localization.AtPrime P) (Localization P') := localizationAlgebra P.primeCompl S<VAR>this✝ : IsScalarTower R (Localization.AtPrime P) (Localization P')<VAR>h : P' ≤ S⁰<VAR>this : IsDomain (Localization P')<GOAL>map (algebraMap R (Localization.AtPrime P)) (spanNorm R (I * J)) = map (algebraMap R (Localization.AtPrime P)) (spanNorm R I * spanNorm R J)
<VAR>R : Type u_1<VAR>inst✝⁹ : CommRing R<VAR>S : Type u_2<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : Algebra R S<VAR>inst✝⁶ : IsDomain R<VAR>inst✝⁵ : IsDomain S<VAR>inst✝⁴ : IsDedekindDomain R<VAR>inst✝³ : IsDedekindDomain S<VAR>inst✝² : Module.Finite R S<VAR>inst✝¹ : Module.Free R S<VAR>I J : Ideal S<VAR>inst✝ : Nontrivial R<VAR>h✝ : Nontrivial S<VAR>P : Ideal R<VAR>hP : P.IsMaximal<VAR>hP0 : ¬P = ⊥<VAR>P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl<VAR>this✝² : Algebra (Localization.AtPrime P) (Localization P') := localizationAlgebra P.primeCompl S<VAR>this✝¹ : IsScalarTower R (Localization.AtPrime P) (Localization P')<VAR>h : P' ≤ S⁰<VAR>this✝ : IsDomain (Localization P')<VAR>this : IsDedekindDomain (Localization P')<GOAL>map (algebraMap R (Localization.AtPrime P)) (spanNorm R (I * J)) = map (algebraMap R (Localization.AtPrime P)) (spanNorm R I * spanNorm R J)
<VAR>R : Type u_1<VAR>inst✝⁹ : CommRing R<VAR>S : Type u_2<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : Algebra R S<VAR>inst✝⁶ : IsDomain R<VAR>inst✝⁵ : IsDomain S<VAR>inst✝⁴ : IsDedekindDomain R<VAR>inst✝³ : IsDedekindDomain S<VAR>inst✝² : Module.Finite R S<VAR>inst✝¹ : Module.Free R S<VAR>I J : Ideal S<VAR>inst✝ : Nontrivial R<VAR>h✝ : Nontrivial S<VAR>P : Ideal R<VAR>hP : P.IsMaximal<VAR>hP0 : ¬P = ⊥<VAR>P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl<VAR>this✝³ : Algebra (Localization.AtPrime P) (Localization P') := localizationAlgebra P.primeCompl S<VAR>this✝² : IsScalarTower R (Localization.AtPrime P) (Localization P')<VAR>h : P' ≤ S⁰<VAR>this✝¹ : IsDomain (Localization P')<VAR>this✝ : IsDedekindDomain (Localization P')<VAR>this : DecidableEq (Ideal (Localization P')) := Classical.decEq (Ideal (Localization P'))<GOAL>map (algebraMap R (Localization.AtPrime P)) (spanNorm R (I * J)) = map (algebraMap R (Localization.AtPrime P)) (spanNorm R I * spanNorm R J)
<VAR>R : Type u_1<VAR>inst✝⁹ : CommRing R<VAR>S : Type u_2<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : Algebra R S<VAR>inst✝⁶ : IsDomain R<VAR>inst✝⁵ : IsDomain S<VAR>inst✝⁴ : IsDedekindDomain R<VAR>inst✝³ : IsDedekindDomain S<VAR>inst✝² : Module.Finite R S<VAR>inst✝¹ : Module.Free R S<VAR>I J : Ideal S<VAR>inst✝ : Nontrivial R<VAR>h✝ : Nontrivial S<VAR>P : Ideal R<VAR>hP : P.IsMaximal<VAR>hP0 : ¬P = ⊥<VAR>P' : Submonoid S := Algebra.algebraMapSubmonoid S P.primeCompl<VAR>this✝⁴ : Algebra (Localization.AtPrime P) (Localization P') := localizationAlgebra P.primeCompl S<VAR>this✝³ : IsScalarTower R (Localization.AtPrime P) (Localization P')<VAR>h : P' ≤ S⁰<VAR>this✝² : IsDomain (Localization P')<VAR>this✝¹ : IsDedekindDomain (Localization P')<VAR>this✝ : DecidableEq (Ideal (Localization P')) := Classical.decEq (Ideal (Localization P'))<VAR>this : IsPrincipalIdealRing (Localization P')<GOAL>map (algebraMap R (Localization.AtPrime P)) (spanNorm R (I * J)) = map (algebraMap R (Localization.AtPrime P)) (spanNorm R I * spanNorm R J)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Seq α<GOAL>(↑s).destruct.destruct = Sum.inl (Option.map (fun a => (a, ↑s.tail)) s.head)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Seq α<GOAL>(match match Option.map (fun a' => (a', (some <$> s).tail)) ((some <$> s).get? 0) with | none => Sum.inl none | some (none, s') => Sum.inr s' | some (some a, s') => Sum.inl (some (a, s')) with | Sum.inl a => Sum.inl a | Sum.inr b => Sum.inr (Computation.corec (fun s => match Option.map (fun a' => (a', Seq.tail s)) (Seq.get? s 0) with | none => Sum.inl none | some (none, s') => Sum.inr s' | some (some a, s') => Sum.inl (some (a, s'))) b)) = Sum.inl (Option.map (fun a => (a, some <$> s.tail)) (s.get? 0))
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Seq α<GOAL>(match match Option.map (fun a' => (a', (some <$> s).tail)) (some <$> s.get? 0) with | none => Sum.inl none | some (none, s') => Sum.inr s' | some (some a, s') => Sum.inl (some (a, s')) with | Sum.inl a => Sum.inl a | Sum.inr b => Sum.inr (Computation.corec (fun s => match Option.map (fun a' => (a', Seq.tail s)) (Seq.get? s 0) with | none => Sum.inl none | some (none, s') => Sum.inr s' | some (some a, s') => Sum.inl (some (a, s'))) b)) = Sum.inl (Option.map (fun a => (a, some <$> s.tail)) (s.get? 0))