ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>M : Type u_1<VAR>inst✝³ : CancelCommMonoidWithZero M<VAR>N : Type u_2<VAR>inst✝² : CancelCommMonoidWithZero N<VAR>inst✝¹ : Unique Mˣ<VAR>inst✝ : Unique Nˣ<VAR>m : M<VAR>n : N<VAR>d : { l // l ∣ m } ≃ { l // l ∣ n }<VAR>hd : ∀ (l l' : { l // l ∣ m }), ↑(d l) ∣ ↑(d l') ↔ ↑l ∣ ↑l'<VAR>x : Associates N<VAR>hx : x ∈ Set.Iic (Associates.mk n)<GOAL>x ≤ Associates.mk n
<VAR>M : Type u_1<VAR>inst✝³ : CancelCommMonoidWithZero M<VAR>N : Type u_2<VAR>inst✝² : CancelCommMonoidWithZero N<VAR>inst✝¹ : Unique Mˣ<VAR>inst✝ : Unique Nˣ<VAR>m : M<VAR>n : N<VAR>d : { l // l ∣ m } ≃ { l // l ∣ n }<VAR>hd : ∀ (l l' : { l // l ∣ m }), ↑(d l) ∣ ↑(d l') ↔ ↑l ∣ ↑l'<VAR>x✝ : ↑(Set.Iic (Associates.mk m))<VAR>l : Associates M<VAR>hl : l ∈ Set.Iic (Associates.mk m)<GOAL>(fun l => ⟨Associates.mk ↑(d.symm ⟨associatesEquivOfUniqueUnits ↑l, ⋯⟩), ⋯⟩) ((fun l => ⟨Associates.mk ↑(d ⟨associatesEquivOfUniqueUnits ↑l, ⋯⟩), ⋯⟩) ⟨l, hl⟩) = ⟨l, hl⟩
<VAR>M : Type u_1<VAR>inst✝³ : CancelCommMonoidWithZero M<VAR>N : Type u_2<VAR>inst✝² : CancelCommMonoidWithZero N<VAR>inst✝¹ : Unique Mˣ<VAR>inst✝ : Unique Nˣ<VAR>m : M<VAR>n : N<VAR>d : { l // l ∣ m } ≃ { l // l ∣ n }<VAR>hd : ∀ (l l' : { l // l ∣ m }), ↑(d l) ∣ ↑(d l') ↔ ↑l ∣ ↑l'<VAR>x✝ : ↑(Set.Iic (Associates.mk n))<VAR>l : Associates N<VAR>hl : l ∈ Set.Iic (Associates.mk n)<GOAL>(fun l => ⟨Associates.mk ↑(d ⟨associatesEquivOfUniqueUnits ↑l, ⋯⟩), ⋯⟩) ((fun l => ⟨Associates.mk ↑(d.symm ⟨associatesEquivOfUniqueUnits ↑l, ⋯⟩), ⋯⟩) ⟨l, hl⟩) = ⟨l, hl⟩
<VAR>M : Type u_1<VAR>inst✝³ : CancelCommMonoidWithZero M<VAR>N : Type u_2<VAR>inst✝² : CancelCommMonoidWithZero N<VAR>inst✝¹ : Unique Mˣ<VAR>inst✝ : Unique Nˣ<VAR>m : M<VAR>n : N<VAR>d : { l // l ∣ m } ≃ { l // l ∣ n }<VAR>hd : ∀ (l l' : { l // l ∣ m }), ↑(d l) ∣ ↑(d l') ↔ ↑l ∣ ↑l'<VAR>a : Associates M<VAR>ha : a ∈ Set.Iic (Associates.mk m)<VAR>b : Associates M<VAR>hb : b ∈ Set.Iic (Associates.mk m)<GOAL>{ toFun := fun l => ⟨Associates.mk ↑(d ⟨associatesEquivOfUniqueUnits ↑l, ⋯⟩), ⋯⟩, invFun := fun l => ⟨Associates.mk ↑(d.symm ⟨associatesEquivOfUniqueUnits ↑l, ⋯⟩), ⋯⟩, left_inv := ⋯, right_inv := ⋯ } ⟨a, ha⟩ ≤ { toFun := fun l => ⟨Associates.mk ↑(d ⟨associatesEquivOfUniqueUnits ↑l, ⋯⟩), ⋯⟩, invFun := fun l => ⟨Associates.mk ↑(d.symm ⟨associatesEquivOfUniqueUnits ↑l, ⋯⟩), ⋯⟩, left_inv := ⋯, right_inv := ⋯ } ⟨b, hb⟩ ↔ ⟨a, ha⟩ ≤ ⟨b, hb⟩
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f✝ g : Perm α<VAR>x y : α<VAR>p : β → Prop<VAR>inst✝ : DecidablePred p<VAR>f : α ≃ Subtype p<VAR>a : α<VAR>ha : g a ≠ a<VAR>ha' : ∀ ⦃y : α⦄, g y ≠ y → g.SameCycle a y<VAR>b : β<VAR>hb : (g.extendDomain f) b ≠ b<GOAL>(g.extendDomain f).SameCycle (↑(f a)) b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f✝ g : Perm α<VAR>x y : α<VAR>p : β → Prop<VAR>inst✝ : DecidablePred p<VAR>f : α ≃ Subtype p<VAR>a : α<VAR>ha : g a ≠ a<VAR>ha' : ∀ ⦃y : α⦄, g y ≠ y → g.SameCycle a y<VAR>b : β<VAR>hb : (g.extendDomain f) b ≠ b<VAR>h : b = ↑(f (f.symm ⟨b, ⋯⟩))<GOAL>(g.extendDomain f).SameCycle (↑(f a)) b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f✝ g : Perm α<VAR>x y : α<VAR>p : β → Prop<VAR>inst✝ : DecidablePred p<VAR>f : α ≃ Subtype p<VAR>a : α<VAR>ha : g a ≠ a<VAR>ha' : ∀ ⦃y : α⦄, g y ≠ y → g.SameCycle a y<VAR>b : β<VAR>hb✝ : (g.extendDomain f) b ≠ b<VAR>hb : (g.extendDomain f) ↑(f (f.symm ⟨b, ⋯⟩)) ≠ ↑(f (f.symm ⟨b, ⋯⟩))<VAR>h : b = ↑(f (f.symm ⟨b, ⋯⟩))<GOAL>(g.extendDomain f).SameCycle ↑(f a) ↑(f (f.symm ⟨b, ⋯⟩))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f✝ g : Perm α<VAR>x y : α<VAR>p : β → Prop<VAR>inst✝ : DecidablePred p<VAR>f : α ≃ Subtype p<VAR>a : α<VAR>ha : g a ≠ a<VAR>ha' : ∀ ⦃y : α⦄, g y ≠ y → g.SameCycle a y<VAR>b : β<VAR>hb✝ : (g.extendDomain f) b ≠ b<VAR>h : b = ↑(f (f.symm ⟨b, ⋯⟩))<VAR>hb : g (f.symm ⟨b, ⋯⟩) ≠ f.symm ⟨b, ⋯⟩<GOAL>(g.extendDomain f).SameCycle ↑(f a) ↑(f (f.symm ⟨b, ⋯⟩))
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>R₀ : Cᵒᵖ ⥤ RingCat<VAR>R : Sheaf J RingCat<VAR>α : R₀ ⟶ R.val<VAR>inst✝³ : Presheaf.IsLocallyInjective J α<VAR>inst✝² : Presheaf.IsLocallySurjective J α<VAR>M₀ : PresheafOfModules R₀<VAR>A : Sheaf J AddCommGrp<VAR>φ : M₀.presheaf ⟶ A.val<VAR>inst✝¹ : Presheaf.IsLocallyInjective J φ<VAR>inst✝ : Presheaf.IsLocallySurjective J φ<VAR>X : Cᵒᵖ<VAR>r₀ : ↑(R₀.obj X)<VAR>m₀ : ↑(M₀.presheaf.obj X)<GOAL>(φ.app X) (r₀ • m₀) = r₀ • (φ.app X) m₀
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{u_4, u_2} D<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasRightCalculusOfFractions<VAR>f : Arrow D<GOAL>f ∈ L.mapArrow.essImage
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{u_4, u_2} D<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasRightCalculusOfFractions<VAR>f : Arrow D<VAR>this : L.op.mapArrow.EssSurj<GOAL>f ∈ L.mapArrow.essImage
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{u_4, u_2} D<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasRightCalculusOfFractions<VAR>f : Arrow D<VAR>this : L.op.mapArrow.EssSurj<VAR>g : Arrow Cᵒᵖ<VAR>e : L.op.mapArrow.obj g ≅ Arrow.mk f.hom.op<GOAL>f ∈ L.mapArrow.essImage
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>I : Finset (Set α)<VAR>m m' : AddContent C<VAR>hC : IsSetSemiring C<VAR>hs : s ∈ C<VAR>ht : t ∈ C<VAR>hst : s ⊆ t<GOAL>m s ≤ m t
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>I : Finset (Set α)<VAR>m m' : AddContent C<VAR>hC : IsSetSemiring C<VAR>hs : s ∈ C<VAR>ht : t ∈ C<VAR>hst : s ⊆ t<VAR>h : ∑ u ∈ {s}, m u ≤ m t<GOAL>m s ≤ m t
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>I : Finset (Set α)<VAR>m m' : AddContent C<VAR>hC : IsSetSemiring C<VAR>hs : s ∈ C<VAR>ht : t ∈ C<VAR>hst : s ⊆ t<GOAL>↑{s} ⊆ C
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>I : Finset (Set α)<VAR>m m' : AddContent C<VAR>hC : IsSetSemiring C<VAR>hs : s ∈ C<VAR>ht : t ∈ C<VAR>hst : s ⊆ t<GOAL>(↑{s}).PairwiseDisjoint id
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>I : Finset (Set α)<VAR>m m' : AddContent C<VAR>hC : IsSetSemiring C<VAR>hs : s ∈ C<VAR>ht : t ∈ C<VAR>hst : s ⊆ t<GOAL>∀ s_1 ∈ {s}, s_1 ⊆ t
<VAR>A✝ : Type u_1<VAR>B : Type u_2<VAR>inst✝⁹ : Field A✝<VAR>inst✝⁸ : Ring B<VAR>inst✝⁷ : Algebra A✝ B<VAR>x✝ : B<VAR>A : Type u_3<VAR>K : Type u_4<VAR>R : Type u_5<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Algebra A K<VAR>inst✝² : Algebra A R<VAR>inst✝¹ : Algebra K R<VAR>inst✝ : IsScalarTower A K R<VAR>x : R<GOAL>minpoly K x ∣ map (algebraMap A K) (minpoly A x)
<VAR>A✝ : Type u_1<VAR>B : Type u_2<VAR>inst✝⁹ : Field A✝<VAR>inst✝⁸ : Ring B<VAR>inst✝⁷ : Algebra A✝ B<VAR>x✝ : B<VAR>A : Type u_3<VAR>K : Type u_4<VAR>R : Type u_5<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Algebra A K<VAR>inst✝² : Algebra A R<VAR>inst✝¹ : Algebra K R<VAR>inst✝ : IsScalarTower A K R<VAR>x : R<GOAL>(Polynomial.aeval x) (map (algebraMap A K) (minpoly A x)) = 0
<VAR>α : Type u_1<VAR>inst✝ : TopologicalSpace α<GOAL>(𝓝 ⊥).HasBasis (fun x => True) fun x => Iio ↑x
<VAR>α : Type u_1<VAR>inst✝ : TopologicalSpace α<VAR>x : EReal<VAR>hx : ⊥ < x<GOAL>∃ i', True ∧ Iio ↑i' ⊆ Iio x
<VAR>α : Type u_1<VAR>inst✝ : TopologicalSpace α<VAR>x : EReal<VAR>hx : ⊥ < x<VAR>y : ℚ<VAR>hxy : ↑↑y < x<GOAL>∃ i', True ∧ Iio ↑i' ⊆ Iio x
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<GOAL>λ ^ 2 ∣ S'.c
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<VAR>hm : multiplicity.Finite λ S'.c<GOAL>λ ^ 2 ∣ S'.c
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<VAR>hm : multiplicity.Finite λ S'.c<GOAL>2 ≤ (multiplicity λ S'.c).get hm
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<VAR>hm : multiplicity.Finite λ S'.c<VAR>this : λ ^ 4 ∣ S'.c ^ 3<GOAL>2 ≤ (multiplicity λ S'.c).get hm
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<VAR>hm : multiplicity.Finite λ S'.c<VAR>this : λ ^ 4 ∣ S'.c ^ 3<VAR>hm1 : ↑((multiplicity λ (S'.c ^ 3)).get ⋯) = multiplicity λ (S'.c ^ 3)<GOAL>2 ≤ (multiplicity λ S'.c).get hm
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<VAR>hm : multiplicity.Finite λ S'.c<VAR>this : 4 ≤ 3 * (multiplicity λ S'.c).get hm<VAR>hm1 : ↑((multiplicity λ (S'.c ^ 3)).get ⋯) = multiplicity λ (S'.c ^ 3)<GOAL>2 ≤ (multiplicity λ S'.c).get hm
<VAR>J : Type w<VAR>inst✝³ : SmallCategory J<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasLimitsOfShape J C<VAR>inst✝ : MonoidalCategory C<VAR>X✝ Y✝ X'✝ Y'✝ : J ⥤ C<VAR>f : X✝ ⟶ Y✝<VAR>g : X'✝ ⟶ Y'✝<VAR>j✝ : J<GOAL>((limMap f ⊗ limMap g) ≫ limit.lift (Y✝ ⊗ Y'✝) { pt := limit Y✝ ⊗ limit Y'✝, π := { app := fun j => limit.π Y✝ j ⊗ limit.π Y'✝ j, naturality := ⋯ } }) ≫ limit.π (Y✝ ⊗ Y'✝) j✝ = (limit.lift (X✝ ⊗ X'✝) { pt := limit X✝ ⊗ limit X'✝, π := { app := fun j => limit.π X✝ j ⊗ limit.π X'✝ j, naturality := ⋯ } } ≫ limMap (f ⊗ g)) ≫ limit.π (Y✝ ⊗ Y'✝) j✝
<VAR>J : Type w<VAR>inst✝³ : SmallCategory J<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasLimitsOfShape J C<VAR>inst✝ : MonoidalCategory C<VAR>X Y Z : J ⥤ C<VAR>j : J<GOAL>((limit.lift (X ⊗ Y) { pt := limit X ⊗ limit Y, π := { app := fun j => limit.π X j ⊗ limit.π Y j, naturality := ⋯ } } ⊗ 𝟙 (limit Z)) ≫ limit.lift ((X ⊗ Y) ⊗ Z) { pt := limit (X ⊗ Y) ⊗ limit Z, π := { app := fun j => limit.π (X ⊗ Y) j ⊗ limit.π Z j, naturality := ⋯ } } ≫ limMap (α_ X Y Z).hom) ≫ limit.π (X ⊗ Y ⊗ Z) j = ((α_ (limit X) (limit Y) (limit Z)).hom ≫ (𝟙 (limit X) ⊗ limit.lift (Y ⊗ Z) { pt := limit Y ⊗ limit Z, π := { app := fun j => limit.π Y j ⊗ limit.π Z j, naturality := ⋯ } }) ≫ limit.lift (X ⊗ Y ⊗ Z) { pt := limit X ⊗ limit (Y ⊗ Z), π := { app := fun j => limit.π X j ⊗ limit.π (Y ⊗ Z) j, naturality := ⋯ } }) ≫ limit.π (X ⊗ Y ⊗ Z) j
<VAR>J : Type w<VAR>inst✝³ : SmallCategory J<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasLimitsOfShape J C<VAR>inst✝ : MonoidalCategory C<VAR>X Y Z : J ⥤ C<VAR>j : J<GOAL>(limit.lift (X ⊗ Y) { pt := limit X ⊗ limit Y, π := { app := fun j => limit.π X j ⊗ limit.π Y j, naturality := ⋯ } } ⊗ 𝟙 (limit Z)) ≫ (limit.π (X ⊗ Y) j ⊗ limit.π Z j) ≫ (α_ (X.obj j) (Y.obj j) (Z.obj j)).hom = (α_ (limit X) (limit Y) (limit Z)).hom ≫ (𝟙 (limit X) ⊗ limit.lift (Y ⊗ Z) { pt := limit Y ⊗ limit Z, π := { app := fun j => limit.π Y j ⊗ limit.π Z j, naturality := ⋯ } }) ≫ (limit.π X j ⊗ limit.π (Y ⊗ Z) j)
<VAR>J : Type w<VAR>inst✝³ : SmallCategory J<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasLimitsOfShape J C<VAR>inst✝ : MonoidalCategory C<VAR>X Y Z : J ⥤ C<VAR>j : J<GOAL>(limit.lift (X ⊗ Y) { pt := limit X ⊗ limit Y, π := { app := fun j => limit.π X j ⊗ limit.π Y j, naturality := ⋯ } } ⊗ 𝟙 (limit Z)) ≫ ((limit.π (X ⊗ Y) j ⊗ 𝟙 (limit Z)) ≫ (𝟙 (X.obj j ⊗ Y.obj j) ⊗ limit.π Z j)) ≫ (α_ (X.obj j) (Y.obj j) (Z.obj j)).hom = (α_ (limit X) (limit Y) (limit Z)).hom ≫ (𝟙 (limit X) ⊗ limit.lift (Y ⊗ Z) { pt := limit Y ⊗ limit Z, π := { app := fun j => limit.π Y j ⊗ limit.π Z j, naturality := ⋯ } }) ≫ (limit.π X j ⊗ limit.π (Y ⊗ Z) j)
<VAR>J : Type w<VAR>inst✝³ : SmallCategory J<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasLimitsOfShape J C<VAR>inst✝ : MonoidalCategory C<VAR>X Y Z : J ⥤ C<VAR>j : J<GOAL>(((limit.π X j ⊗ limit.π Y j) ⊗ 𝟙 (limit Z)) ≫ (𝟙 (X.obj j ⊗ Y.obj j) ⊗ limit.π Z j)) ≫ (α_ (X.obj j) (Y.obj j) (Z.obj j)).hom = (α_ (limit X) (limit Y) (limit Z)).hom ≫ (𝟙 (limit X) ⊗ limit.lift (Y ⊗ Z) { pt := limit Y ⊗ limit Z, π := { app := fun j => limit.π Y j ⊗ limit.π Z j, naturality := ⋯ } }) ≫ (limit.π X j ⊗ limit.π (Y ⊗ Z) j)
<VAR>J : Type w<VAR>inst✝³ : SmallCategory J<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasLimitsOfShape J C<VAR>inst✝ : MonoidalCategory C<VAR>X Y Z : J ⥤ C<VAR>j : J<GOAL>((limit.π X j ⊗ limit.π Y j) ⊗ limit.π Z j) ≫ (α_ (X.obj j) (Y.obj j) (Z.obj j)).hom = (α_ (limit X) (limit Y) (limit Z)).hom ≫ (𝟙 (limit X) ⊗ limit.lift (Y ⊗ Z) { pt := limit Y ⊗ limit Z, π := { app := fun j => limit.π Y j ⊗ limit.π Z j, naturality := ⋯ } }) ≫ (limit.π X j ⊗ limit.π (Y ⊗ Z) j)
<VAR>J : Type w<VAR>inst✝³ : SmallCategory J<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasLimitsOfShape J C<VAR>inst✝ : MonoidalCategory C<VAR>X Y Z : J ⥤ C<VAR>j : J<GOAL>(α_ (limit X) (limit Y) (limit Z)).hom ≫ (limit.π X j ⊗ limit.π Y j ⊗ limit.π Z j) = (α_ (limit X) (limit Y) (limit Z)).hom ≫ (𝟙 (limit X) ⊗ limit.lift (Y ⊗ Z) { pt := limit Y ⊗ limit Z, π := { app := fun j => limit.π Y j ⊗ limit.π Z j, naturality := ⋯ } }) ≫ (limit.π X j ⊗ limit.π (Y ⊗ Z) j)
<VAR>J : Type w<VAR>inst✝³ : SmallCategory J<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasLimitsOfShape J C<VAR>inst✝ : MonoidalCategory C<VAR>X Y Z : J ⥤ C<VAR>j : J<GOAL>(α_ (limit X) (limit Y) (limit Z)).hom ≫ (limit.π X j ⊗ limit.π Y j ⊗ limit.π Z j) = (α_ (limit X) (limit Y) (limit Z)).hom ≫ (𝟙 (limit X) ⊗ limit.lift (Y ⊗ Z) { pt := limit Y ⊗ limit Z, π := { app := fun j => limit.π Y j ⊗ limit.π Z j, naturality := ⋯ } }) ≫ (𝟙 (limit X) ⊗ limit.π (Y ⊗ Z) j) ≫ (limit.π X j ⊗ 𝟙 ((Y ⊗ Z).obj j))
<VAR>J : Type w<VAR>inst✝³ : SmallCategory J<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasLimitsOfShape J C<VAR>inst✝ : MonoidalCategory C<VAR>X Y Z : J ⥤ C<VAR>j : J<GOAL>(α_ (limit X) (limit Y) (limit Z)).hom ≫ (limit.π X j ⊗ limit.π Y j ⊗ limit.π Z j) = (α_ (limit X) (limit Y) (limit Z)).hom ≫ (𝟙 (limit X) ⊗ limit.π Y j ⊗ limit.π Z j) ≫ (limit.π X j ⊗ 𝟙 ((Y ⊗ Z).obj j))
<VAR>J : Type w<VAR>inst✝³ : SmallCategory J<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasLimitsOfShape J C<VAR>inst✝ : MonoidalCategory C<VAR>X Y Z : J ⥤ C<VAR>j : J<GOAL>(α_ (limit X) (limit Y) (limit Z)).hom ≫ (limit.π X j ⊗ limit.π Y j ⊗ limit.π Z j) = (α_ (limit X) (limit Y) (limit Z)).hom ≫ (𝟙 (limit X) ⊗ limit.π Y j ⊗ limit.π Z j) ≫ (limit.π X j ⊗ 𝟙 (Y.obj j ⊗ Z.obj j))
<VAR>J : Type w<VAR>inst✝³ : SmallCategory J<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasLimitsOfShape J C<VAR>inst✝ : MonoidalCategory C<VAR>X : J ⥤ C<VAR>j : J<GOAL>(λ_ (limit X)).hom ≫ limit.π X j = ((limit.lift ((Functor.const J).obj (𝟙_ C)) { pt := 𝟙_ C, π := { app := fun j => 𝟙 (𝟙_ C), naturality := ⋯ } } ⊗ 𝟙 (limit X)) ≫ limit.lift (𝟙_ (J ⥤ C) ⊗ X) { pt := limit (𝟙_ (J ⥤ C)) ⊗ limit X, π := { app := fun j => limit.π (𝟙_ (J ⥤ C)) j ⊗ limit.π X j, naturality := ⋯ } } ≫ limMap (λ_ X).hom) ≫ limit.π X j
<VAR>J : Type w<VAR>inst✝³ : SmallCategory J<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasLimitsOfShape J C<VAR>inst✝ : MonoidalCategory C<VAR>X : J ⥤ C<VAR>j : J<GOAL>(λ_ (limit X)).hom ≫ limit.π X j = (limit.lift ((Functor.const J).obj (𝟙_ C)) { pt := 𝟙_ C, π := { app := fun j => 𝟙 (𝟙_ C), naturality := ⋯ } } ⊗ 𝟙 (limit X)) ≫ (limit.π (𝟙_ (J ⥤ C)) j ⊗ limit.π X j) ≫ (λ_ (X.obj j)).hom
<VAR>J : Type w<VAR>inst✝³ : SmallCategory J<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasLimitsOfShape J C<VAR>inst✝ : MonoidalCategory C<VAR>X : J ⥤ C<VAR>j : J<GOAL>(λ_ (limit X)).hom ≫ limit.π X j = (limit.lift ((Functor.const J).obj (𝟙_ C)) { pt := 𝟙_ C, π := { app := fun j => 𝟙 (𝟙_ C), naturality := ⋯ } } ⊗ 𝟙 (limit X)) ≫ ((limit.π (𝟙_ (J ⥤ C)) j ⊗ 𝟙 (limit X)) ≫ (𝟙 (𝟙_ C) ⊗ limit.π X j)) ≫ (λ_ (X.obj j)).hom
<VAR>J : Type w<VAR>inst✝³ : SmallCategory J<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasLimitsOfShape J C<VAR>inst✝ : MonoidalCategory C<VAR>X : J ⥤ C<VAR>j : J<GOAL>(λ_ (limit X)).hom ≫ limit.π X j = ((𝟙 (𝟙_ C) ⊗ 𝟙 (limit X)) ≫ (𝟙 (𝟙_ C) ⊗ limit.π X j)) ≫ (λ_ (X.obj j)).hom
<VAR>J : Type w<VAR>inst✝³ : SmallCategory J<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasLimitsOfShape J C<VAR>inst✝ : MonoidalCategory C<VAR>X : J ⥤ C<VAR>j : J<GOAL>(λ_ (limit X)).hom ≫ limit.π X j = (𝟙 (𝟙_ C) ⊗ 𝟙 (limit X)) ≫ (λ_ (limit X)).hom ≫ limit.π X j
<VAR>J : Type w<VAR>inst✝³ : SmallCategory J<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasLimitsOfShape J C<VAR>inst✝ : MonoidalCategory C<VAR>X : J ⥤ C<VAR>j : J<GOAL>(ρ_ (limit X)).hom ≫ limit.π X j = ((𝟙 (limit X) ⊗ limit.lift ((Functor.const J).obj (𝟙_ C)) { pt := 𝟙_ C, π := { app := fun j => 𝟙 (𝟙_ C), naturality := ⋯ } }) ≫ limit.lift (X ⊗ 𝟙_ (J ⥤ C)) { pt := limit X ⊗ limit (𝟙_ (J ⥤ C)), π := { app := fun j => limit.π X j ⊗ limit.π (𝟙_ (J ⥤ C)) j, naturality := ⋯ } } ≫ limMap (ρ_ X).hom) ≫ limit.π X j
<VAR>J : Type w<VAR>inst✝³ : SmallCategory J<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasLimitsOfShape J C<VAR>inst✝ : MonoidalCategory C<VAR>X : J ⥤ C<VAR>j : J<GOAL>(ρ_ (limit X)).hom ≫ limit.π X j = (𝟙 (limit X) ⊗ limit.lift ((Functor.const J).obj (𝟙_ C)) { pt := 𝟙_ C, π := { app := fun j => 𝟙 (𝟙_ C), naturality := ⋯ } }) ≫ (limit.π X j ⊗ limit.π (𝟙_ (J ⥤ C)) j) ≫ (ρ_ (X.obj j)).hom
<VAR>J : Type w<VAR>inst✝³ : SmallCategory J<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasLimitsOfShape J C<VAR>inst✝ : MonoidalCategory C<VAR>X : J ⥤ C<VAR>j : J<GOAL>(ρ_ (limit X)).hom ≫ limit.π X j = (𝟙 (limit X) ⊗ limit.lift ((Functor.const J).obj (𝟙_ C)) { pt := 𝟙_ C, π := { app := fun j => 𝟙 (𝟙_ C), naturality := ⋯ } }) ≫ ((𝟙 (limit X) ⊗ limit.π (𝟙_ (J ⥤ C)) j) ≫ (limit.π X j ⊗ 𝟙 (𝟙_ C))) ≫ (ρ_ (X.obj j)).hom
<VAR>J : Type w<VAR>inst✝³ : SmallCategory J<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasLimitsOfShape J C<VAR>inst✝ : MonoidalCategory C<VAR>X : J ⥤ C<VAR>j : J<GOAL>(ρ_ (limit X)).hom ≫ limit.π X j = ((𝟙 (limit X) ⊗ 𝟙 (𝟙_ C)) ≫ (limit.π X j ⊗ 𝟙 (𝟙_ C))) ≫ (ρ_ (X.obj j)).hom
<VAR>J : Type w<VAR>inst✝³ : SmallCategory J<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasLimitsOfShape J C<VAR>inst✝ : MonoidalCategory C<VAR>X : J ⥤ C<VAR>j : J<GOAL>(ρ_ (limit X)).hom ≫ limit.π X j = (𝟙 (limit X) ⊗ 𝟙 (𝟙_ C)) ≫ (ρ_ (limit X)).hom ≫ limit.π X j
<VAR>I : Type w₀<VAR>J : Type w₁<VAR>C : I → Type u₁<VAR>inst✝² : (i : I) → Category.{v₁, u₁} (C i)<VAR>D : I → Type u₂<VAR>inst✝¹ : (i : I) → Category.{v₂, u₂} (D i)<VAR>F✝ G✝ : (i : I) → C i ⥤ D i<VAR>E : Type u_1<VAR>inst✝ : Category.{?u.104939, u_1} E<VAR>F G : E ⥤ ((i : I) → C i)<VAR>τ : (i : I) → F ⋙ Pi.eval C i ⟶ G ⋙ Pi.eval C i<VAR>x✝¹ x✝ : E<VAR>f : x✝¹ ⟶ x✝<VAR>i : I<GOAL>(F.map f ≫ (fun X i => (τ i).app X) x✝) i = ((fun X i => (τ i).app X) x✝¹ ≫ G.map f) i
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>a b c u v✝ w✝ : V<VAR>e : Sym2 V<VAR>s : Set (Sym2 V)<VAR>v w : V<GOAL>(fromEdgeSet ∅).Adj v w ↔ ⊥.Adj v w
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>(o.oangle (x + y) y).tan = ‖x‖ / ‖y‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : (-o).oangle y x = ↑(π / 2)<GOAL>((-o).oangle y (x + y)).tan = ‖x‖ / ‖y‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : (-o).oangle y x = ↑(π / 2)<GOAL>((-o).oangle y (y + x)).tan = ‖x‖ / ‖y‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<GOAL>Iic b \ Iio a = Icc a b
<VAR>a : ℤ<VAR>n : ℕ<GOAL>succ^[n + 1] a = a + ↑(n + 1)
<VAR>a : ℤ<VAR>n : ℕ<GOAL>(succ ∘ succ^[n]) a = a + ↑n + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>inst✝ : MeasurableSpace δ<VAR>μa : Measure α<VAR>μb : Measure β<VAR>μc : Measure γ<VAR>μd : Measure δ<VAR>f : α → β<VAR>hf : MeasurePreserving f μa μb<VAR>h₂ : MeasurableEmbedding f<VAR>s : Set β<GOAL>map f (μa.restrict (f ⁻¹' s)) = μb.restrict s
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝¹ : Ring R<VAR>p✝ q : R[X]<VAR>inst✝ : DecidableEq R<VAR>p : R[X]<VAR>p0 : p ≠ 0<VAR>a : R<GOAL>(if h0 : p = 0 then 0 else Nat.find ⋯) = Nat.find ⋯
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p✝ q p : R[X]<VAR>p0 : p ≠ 0<VAR>a : R<GOAL>(if h0 : p = 0 then 0 else Nat.find ⋯) = Nat.find ⋯
<VAR>A : Type u<VAR>B✝ : Type v<VAR>C : Type z<VAR>ι : Type w<VAR>inst✝²² : DecidableEq ι<VAR>inst✝²¹ : CommRing A<VAR>inst✝²⁰ : CommRing B✝<VAR>inst✝¹⁹ : Algebra A B✝<VAR>inst✝¹⁸ : CommRing C<VAR>inst✝¹⁷ : Algebra A C<VAR>ι' : Type u_1<VAR>inst✝¹⁶ : Fintype ι'<VAR>inst✝¹⁵ : Fintype ι<VAR>inst✝¹⁴ : DecidableEq ι'<VAR>K : Type u<VAR>L : Type v<VAR>E : Type z<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : Field L<VAR>inst✝¹¹ : Field E<VAR>inst✝¹⁰ : Algebra K L<VAR>inst✝⁹ : Algebra K E<VAR>inst✝⁸ : Module.Finite K L<VAR>inst✝⁷ : IsAlgClosed E<VAR>b : ι → L<VAR>pb : PowerBasis K L<VAR>R : Type z<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : Algebra R K<VAR>inst✝⁴ : Algebra R L<VAR>inst✝³ : IsScalarTower R K L<VAR>inst✝² : Algebra.IsSeparable K L<VAR>inst✝¹ : IsIntegrallyClosed R<VAR>inst✝ : IsFractionRing R K<VAR>B : PowerBasis K L<VAR>hint : IsIntegral R B.gen<VAR>z : L<VAR>hz : IsIntegral R z<GOAL>discr K ⇑B.basis • z ∈ adjoin R {B.gen}
<VAR>A : Type u<VAR>B✝ : Type v<VAR>C : Type z<VAR>ι : Type w<VAR>inst✝²² : DecidableEq ι<VAR>inst✝²¹ : CommRing A<VAR>inst✝²⁰ : CommRing B✝<VAR>inst✝¹⁹ : Algebra A B✝<VAR>inst✝¹⁸ : CommRing C<VAR>inst✝¹⁷ : Algebra A C<VAR>ι' : Type u_1<VAR>inst✝¹⁶ : Fintype ι'<VAR>inst✝¹⁵ : Fintype ι<VAR>inst✝¹⁴ : DecidableEq ι'<VAR>K : Type u<VAR>L : Type v<VAR>E : Type z<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : Field L<VAR>inst✝¹¹ : Field E<VAR>inst✝¹⁰ : Algebra K L<VAR>inst✝⁹ : Algebra K E<VAR>inst✝⁸ : Module.Finite K L<VAR>inst✝⁷ : IsAlgClosed E<VAR>b : ι → L<VAR>pb : PowerBasis K L<VAR>R : Type z<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : Algebra R K<VAR>inst✝⁴ : Algebra R L<VAR>inst✝³ : IsScalarTower R K L<VAR>inst✝² : Algebra.IsSeparable K L<VAR>inst✝¹ : IsIntegrallyClosed R<VAR>inst✝ : IsFractionRing R K<VAR>B : PowerBasis K L<VAR>hint : IsIntegral R B.gen<VAR>z : L<VAR>hz : IsIntegral R z<VAR>hinv : IsUnit (traceMatrix K ⇑B.basis).det<GOAL>discr K ⇑B.basis • z ∈ adjoin R {B.gen}
<VAR>A : Type u<VAR>B✝ : Type v<VAR>C : Type z<VAR>ι : Type w<VAR>inst✝²² : DecidableEq ι<VAR>inst✝²¹ : CommRing A<VAR>inst✝²⁰ : CommRing B✝<VAR>inst✝¹⁹ : Algebra A B✝<VAR>inst✝¹⁸ : CommRing C<VAR>inst✝¹⁷ : Algebra A C<VAR>ι' : Type u_1<VAR>inst✝¹⁶ : Fintype ι'<VAR>inst✝¹⁵ : Fintype ι<VAR>inst✝¹⁴ : DecidableEq ι'<VAR>K : Type u<VAR>L : Type v<VAR>E : Type z<VAR>inst✝¹³ : Field K<VAR>inst✝¹² : Field L<VAR>inst✝¹¹ : Field E<VAR>inst✝¹⁰ : Algebra K L<VAR>inst✝⁹ : Algebra K E<VAR>inst✝⁸ : Module.Finite K L<VAR>inst✝⁷ : IsAlgClosed E<VAR>b : ι → L<VAR>pb : PowerBasis K L<VAR>R : Type z<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : Algebra R K<VAR>inst✝⁴ : Algebra R L<VAR>inst✝³ : IsScalarTower R K L<VAR>inst✝² : Algebra.IsSeparable K L<VAR>inst✝¹ : IsIntegrallyClosed R<VAR>inst✝ : IsFractionRing R K<VAR>B : PowerBasis K L<VAR>hint : IsIntegral R B.gen<VAR>z : L<VAR>hz : IsIntegral R z<VAR>hinv : IsUnit (traceMatrix K ⇑B.basis).det<VAR>H : (traceMatrix K ⇑B.basis).det • traceMatrix K ⇑B.basis *ᵥ B.basis.equivFun z = (traceMatrix K ⇑B.basis).det • fun i => (trace K L) (z * B.basis i)<GOAL>discr K ⇑B.basis • z ∈ adjoin R {B.gen}