ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasShift C ℤ<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive<VAR>hC : Pretriangulated C<VAR>T : Triangle C<VAR>hT : T ∈ distinguishedTriangles<VAR>X : C<VAR>f : T.obj₂ ⟶ X<VAR>hf : T.mor₁ ≫ f = 0<VAR>g : T.obj₃ ⟶ (mk 0 (𝟙 X) 0).obj₃<VAR>hg₁ : T.mor₂ ≫ g = f ≫ (mk 0 (𝟙 X) 0).mor₂<VAR>right✝ : T.mor₃ ≫ (CategoryTheory.shiftFunctor C 1).map 0 = g ≫ (mk 0 (𝟙 X) 0).mor₃<GOAL>∃ g, f = T.mor₂ ≫ g
<VAR>n m l : ℕ<VAR>hnl : n ≤ l<GOAL>filter (fun x => decide (l ≤ x)) (Ico n m) = Ico l m
<VAR>n m l : ℕ<VAR>hnl : n ≤ l<VAR>hlm : l ≤ m<GOAL>filter (fun x => decide (l ≤ x)) (Ico n m) = Ico l m
<VAR>n m l : ℕ<VAR>hnl : n ≤ l<VAR>hml : m ≤ l<GOAL>filter (fun x => decide (l ≤ x)) (Ico n m) = Ico l m
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>inst✝³ : Category.{?u.136944, u_1} C<VAR>inst✝² : Category.{?u.136948, u_2} D<VAR>inst✝¹ : Category.{?u.136952, u_3} H<VAR>L : C ⥤ D<VAR>F : C ⥤ H<VAR>inst✝ : L.HasPointwiseRightKanExtension F<VAR>X₁ X₂ : C<VAR>f : X₁ ⟶ X₂<GOAL>(L ⋙ L.pointwiseRightKanExtension F).map f ≫ (fun X => limit.π (StructuredArrow.proj (L.obj X) L ⋙ F) (StructuredArrow.mk (𝟙 (L.obj X)))) X₂ = (fun X => limit.π (StructuredArrow.proj (L.obj X) L ⋙ F) (StructuredArrow.mk (𝟙 (L.obj X)))) X₁ ≫ F.map f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>inst✝³ : Category.{?u.136944, u_1} C<VAR>inst✝² : Category.{?u.136948, u_2} D<VAR>inst✝¹ : Category.{?u.136952, u_3} H<VAR>L : C ⥤ D<VAR>F : C ⥤ H<VAR>inst✝ : L.HasPointwiseRightKanExtension F<VAR>X₁ X₂ : C<VAR>f : X₁ ⟶ X₂<GOAL>limit.π (StructuredArrow.proj (L.obj X₁) L ⋙ F) (StructuredArrow.mk (L.map f ≫ 𝟙 (L.obj X₂))) = limit.π (StructuredArrow.proj (L.obj X₁) L ⋙ F) (StructuredArrow.mk (𝟙 (L.obj X₁))) ≫ F.map f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>inst✝³ : Category.{?u.136944, u_1} C<VAR>inst✝² : Category.{?u.136948, u_2} D<VAR>inst✝¹ : Category.{?u.136952, u_3} H<VAR>L : C ⥤ D<VAR>F : C ⥤ H<VAR>inst✝ : L.HasPointwiseRightKanExtension F<VAR>X₁ X₂ : C<VAR>f : X₁ ⟶ X₂<GOAL>limit.π (StructuredArrow.proj (L.obj X₁) L ⋙ F) (StructuredArrow.mk (L.map f)) = limit.π (StructuredArrow.proj (L.obj X₁) L ⋙ F) (StructuredArrow.mk (𝟙 (L.obj X₁))) ≫ F.map f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>inst✝³ : Category.{?u.136944, u_1} C<VAR>inst✝² : Category.{?u.136948, u_2} D<VAR>inst✝¹ : Category.{?u.136952, u_3} H<VAR>L : C ⥤ D<VAR>F : C ⥤ H<VAR>inst✝ : L.HasPointwiseRightKanExtension F<VAR>X₁ X₂ : C<VAR>f : X₁ ⟶ X₂<VAR>φ : StructuredArrow.mk (𝟙 (L.obj X₁)) ⟶ StructuredArrow.mk (L.map f) := StructuredArrow.homMk f ⋯<GOAL>limit.π (StructuredArrow.proj (L.obj X₁) L ⋙ F) (StructuredArrow.mk (L.map f)) = limit.π (StructuredArrow.proj (L.obj X₁) L ⋙ F) (StructuredArrow.mk (𝟙 (L.obj X₁))) ≫ F.map f
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝⁹ : AddCommMonoid ι<VAR>inst✝⁸ : DecidableEq ι<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>inst✝⁴ : GradedAlgebra 𝒜<VAR>x : Submonoid A<VAR>α : Type u_4<VAR>inst✝³ : SMul α R<VAR>inst✝² : SMul α A<VAR>inst✝¹ : IsScalarTower α R A<VAR>inst✝ : IsScalarTower α A A<VAR>n : α<VAR>x✝ : NumDenSameDeg 𝒜 x<GOAL>(n • Quotient.mk'' x✝).val = n • val (Quotient.mk'' x✝)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝⁹ : AddCommMonoid ι<VAR>inst✝⁸ : DecidableEq ι<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>inst✝⁴ : GradedAlgebra 𝒜<VAR>x : Submonoid A<VAR>α : Type u_4<VAR>inst✝³ : SMul α R<VAR>inst✝² : SMul α A<VAR>inst✝¹ : IsScalarTower α R A<VAR>inst✝ : IsScalarTower α A A<VAR>n : α<VAR>x✝ : NumDenSameDeg 𝒜 x<GOAL>Localization.mk ↑(n • x✝).num ⟨↑(n • x✝).den, ⋯⟩ = Localization.mk (n • ↑x✝.num) ⟨↑x✝.den, ⋯⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝¹⁰ : Countable ι<VAR>f g : α → β<VAR>M : Type u_5<VAR>G : Type u_6<VAR>G₀ : Type u_7<VAR>inst✝⁹ : TopologicalSpace β<VAR>inst✝⁸ : Monoid M<VAR>inst✝⁷ : MulAction M β<VAR>inst✝⁶ : ContinuousConstSMul M β<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : MulAction G β<VAR>inst✝³ : ContinuousConstSMul G β<VAR>inst✝² : GroupWithZero G₀<VAR>inst✝¹ : MulAction G₀ β<VAR>inst✝ : ContinuousConstSMul G₀ β<VAR>m : MeasurableSpace α<VAR>c : G<VAR>h : StronglyMeasurable fun x => c • f x<GOAL>StronglyMeasurable f
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : CommSemiring α<VAR>inst✝² : Fintype m<VAR>inst✝¹ : DecidableEq m<VAR>inst✝ : Algebra R α<VAR>r : R<GOAL>{ toFun := fun M => MulOpposite.op Mᵀ, invFun := __src✝¹.invFun, left_inv := ⋯, right_inv := ⋯ }.toFun ((algebraMap R (Matrix m m α)) r) = (algebraMap R (Matrix m m α)ᵐᵒᵖ) r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ t u v : Finset α<VAR>a✝ b a : α<VAR>s : Finset α<VAR>h : a ∉ s<GOAL>(insert a s).erase a = s
<VAR>α : Type u_1<VAR>inst✝² : CanonicallyLinearOrderedAddCommMonoid α<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c d : α<VAR>ha : AddLECancellable a<GOAL>a - b < a ↔ 0 < a ∧ 0 < b
<VAR>α : Type u_1<VAR>inst✝² : CanonicallyLinearOrderedAddCommMonoid α<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c d : α<VAR>ha : AddLECancellable a<VAR>h : a - b < a<GOAL>0 ≠ b
<VAR>α : Type u_1<VAR>inst✝² : CanonicallyLinearOrderedAddCommMonoid α<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a c d : α<VAR>ha : AddLECancellable a<VAR>h : a - 0 < a<GOAL>False
<VAR>α : Type u_1<VAR>inst✝² : CanonicallyLinearOrderedAddCommMonoid α<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a c d : α<VAR>ha : AddLECancellable a<VAR>h : a < a<GOAL>False
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : E<GOAL>‖⟪x, y⟫_𝕜‖ ≤ ‖x‖ * ‖y‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : E<GOAL>‖⟪x, y⟫_𝕜‖ ≤ √(re ⟪x, x⟫_𝕜) * √(re ⟪y, y⟫_𝕜)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : E<VAR>this : InnerProductSpace.Core 𝕜 E := InnerProductSpace.toCore<GOAL>‖⟪x, y⟫_𝕜‖ ≤ √(re ⟪x, x⟫_𝕜) * √(re ⟪y, y⟫_𝕜)
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝ : Ring R<VAR>i : ℕ<GOAL>↑((restriction 1).coeff i) = ↑(coeff 1 i)
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝ : Ring R<VAR>i : ℕ<GOAL>(if i = 0 then 1 else 0) = ↑(if i = 0 then 1 else 0)
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : 𝓞 K<GOAL>IsUnit x ↔ |↑((RingOfIntegers.norm ℚ) x)| = 1
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : 𝓞 K<GOAL>|↑((RingOfIntegers.norm ℚ) x)| = 1 ↔ IsUnit ((RingOfIntegers.norm ℚ) x)
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁹ : CommRing A<VAR>inst✝¹⁸ : Field K<VAR>inst✝¹⁷ : CommRing B<VAR>inst✝¹⁶ : Field L<VAR>inst✝¹⁵ : Algebra A K<VAR>inst✝¹⁴ : Algebra B L<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : Algebra K L<VAR>inst✝¹¹ : Algebra A L<VAR>inst✝¹⁰ : IsScalarTower A K L<VAR>inst✝⁹ : IsScalarTower A B L<VAR>inst✝⁸ : IsDomain A<VAR>inst✝⁷ : IsFractionRing A K<VAR>inst✝⁶ : IsIntegralClosure B A L<VAR>inst✝⁵ : IsFractionRing B L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>inst✝² : IsDomain B<VAR>inst✝¹ : IsIntegrallyClosed A<VAR>inst✝ : NoZeroSMulDivisors A B<VAR>I : Submodule B (FractionRing B)<GOAL>Submodule.map (↑(FractionRing.algEquiv B L).toLinearEquiv) (traceDual A (FractionRing A) I) = (Submodule.map (↑(FractionRing.algEquiv B L).toLinearEquiv) I)ᵛ
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁹ : CommRing A<VAR>inst✝¹⁸ : Field K<VAR>inst✝¹⁷ : CommRing B<VAR>inst✝¹⁶ : Field L<VAR>inst✝¹⁵ : Algebra A K<VAR>inst✝¹⁴ : Algebra B L<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : Algebra K L<VAR>inst✝¹¹ : Algebra A L<VAR>inst✝¹⁰ : IsScalarTower A K L<VAR>inst✝⁹ : IsScalarTower A B L<VAR>inst✝⁸ : IsDomain A<VAR>inst✝⁷ : IsFractionRing A K<VAR>inst✝⁶ : IsIntegralClosure B A L<VAR>inst✝⁵ : IsFractionRing B L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>inst✝² : IsDomain B<VAR>inst✝¹ : IsIntegrallyClosed A<VAR>inst✝ : NoZeroSMulDivisors A B<VAR>I : Submodule B (FractionRing B)<GOAL>comap (↑(FractionRing.algEquiv B L).toLinearEquiv.symm) (traceDual A (FractionRing A) I) = (comap (↑(FractionRing.algEquiv B L).toLinearEquiv.symm) I)ᵛ
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁹ : CommRing A<VAR>inst✝¹⁸ : Field K<VAR>inst✝¹⁷ : CommRing B<VAR>inst✝¹⁶ : Field L<VAR>inst✝¹⁵ : Algebra A K<VAR>inst✝¹⁴ : Algebra B L<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : Algebra K L<VAR>inst✝¹¹ : Algebra A L<VAR>inst✝¹⁰ : IsScalarTower A K L<VAR>inst✝⁹ : IsScalarTower A B L<VAR>inst✝⁸ : IsDomain A<VAR>inst✝⁷ : IsFractionRing A K<VAR>inst✝⁶ : IsIntegralClosure B A L<VAR>inst✝⁵ : IsFractionRing B L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>inst✝² : IsDomain B<VAR>inst✝¹ : IsIntegrallyClosed A<VAR>inst✝ : NoZeroSMulDivisors A B<VAR>I : Submodule B (FractionRing B)<VAR>x : L<GOAL>x ∈ comap (↑(FractionRing.algEquiv B L).toLinearEquiv.symm) (traceDual A (FractionRing A) I) ↔ x ∈ (comap (↑(FractionRing.algEquiv B L).toLinearEquiv.symm) I)ᵛ
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁹ : CommRing A<VAR>inst✝¹⁸ : Field K<VAR>inst✝¹⁷ : CommRing B<VAR>inst✝¹⁶ : Field L<VAR>inst✝¹⁵ : Algebra A K<VAR>inst✝¹⁴ : Algebra B L<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : Algebra K L<VAR>inst✝¹¹ : Algebra A L<VAR>inst✝¹⁰ : IsScalarTower A K L<VAR>inst✝⁹ : IsScalarTower A B L<VAR>inst✝⁸ : IsDomain A<VAR>inst✝⁷ : IsFractionRing A K<VAR>inst✝⁶ : IsIntegralClosure B A L<VAR>inst✝⁵ : IsFractionRing B L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>inst✝² : IsDomain B<VAR>inst✝¹ : IsIntegrallyClosed A<VAR>inst✝ : NoZeroSMulDivisors A B<VAR>I : Submodule B (FractionRing B)<VAR>x : L<GOAL>(FractionRing.algEquiv B L).symm x ∈ ((traceForm (FractionRing A) (FractionRing B)).dualSubmodule (restrictScalars A I)).toAddSubmonoid ↔ x ∈ ((traceForm K L).dualSubmodule (restrictScalars A (comap (FractionRing.algEquiv B L).symm.toLinearMap I))).toAddSubmonoid
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁹ : CommRing A<VAR>inst✝¹⁸ : Field K<VAR>inst✝¹⁷ : CommRing B<VAR>inst✝¹⁶ : Field L<VAR>inst✝¹⁵ : Algebra A K<VAR>inst✝¹⁴ : Algebra B L<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : Algebra K L<VAR>inst✝¹¹ : Algebra A L<VAR>inst✝¹⁰ : IsScalarTower A K L<VAR>inst✝⁹ : IsScalarTower A B L<VAR>inst✝⁸ : IsDomain A<VAR>inst✝⁷ : IsFractionRing A K<VAR>inst✝⁶ : IsIntegralClosure B A L<VAR>inst✝⁵ : IsFractionRing B L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>inst✝² : IsDomain B<VAR>inst✝¹ : IsIntegrallyClosed A<VAR>inst✝ : NoZeroSMulDivisors A B<VAR>I : Submodule B (FractionRing B)<VAR>x : L<GOAL>∀ (a : FractionRing B), a ∈ restrictScalars A I → ((traceForm (FractionRing A) (FractionRing B)) ((FractionRing.algEquiv B L).symm x)) a ∈ 1 ↔ (FractionRing.algEquiv B L).toEquiv a ∈ restrictScalars A (comap (FractionRing.algEquiv B L).symm.toLinearMap I) → ((traceForm K L) x) ((FractionRing.algEquiv B L).toEquiv a) ∈ 1
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁹ : CommRing A<VAR>inst✝¹⁸ : Field K<VAR>inst✝¹⁷ : CommRing B<VAR>inst✝¹⁶ : Field L<VAR>inst✝¹⁵ : Algebra A K<VAR>inst✝¹⁴ : Algebra B L<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : Algebra K L<VAR>inst✝¹¹ : Algebra A L<VAR>inst✝¹⁰ : IsScalarTower A K L<VAR>inst✝⁹ : IsScalarTower A B L<VAR>inst✝⁸ : IsDomain A<VAR>inst✝⁷ : IsFractionRing A K<VAR>inst✝⁶ : IsIntegralClosure B A L<VAR>inst✝⁵ : IsFractionRing B L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>inst✝² : IsDomain B<VAR>inst✝¹ : IsIntegrallyClosed A<VAR>inst✝ : NoZeroSMulDivisors A B<VAR>I : Submodule B (FractionRing B)<VAR>x : L<GOAL>∀ (a : FractionRing B), a ∈ I → (Algebra.trace (FractionRing A) (FractionRing B)) ((FractionRing.algEquiv B L).symm x * a) ∈ 1 ↔ a ∈ I → (Algebra.trace K L) (x * (FractionRing.algEquiv B L) a) ∈ 1
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁹ : CommRing A<VAR>inst✝¹⁸ : Field K<VAR>inst✝¹⁷ : CommRing B<VAR>inst✝¹⁶ : Field L<VAR>inst✝¹⁵ : Algebra A K<VAR>inst✝¹⁴ : Algebra B L<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : Algebra K L<VAR>inst✝¹¹ : Algebra A L<VAR>inst✝¹⁰ : IsScalarTower A K L<VAR>inst✝⁹ : IsScalarTower A B L<VAR>inst✝⁸ : IsDomain A<VAR>inst✝⁷ : IsFractionRing A K<VAR>inst✝⁶ : IsIntegralClosure B A L<VAR>inst✝⁵ : IsFractionRing B L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>inst✝² : IsDomain B<VAR>inst✝¹ : IsIntegrallyClosed A<VAR>inst✝ : NoZeroSMulDivisors A B<VAR>I : Submodule B (FractionRing B)<VAR>x : L<VAR>y : FractionRing B<VAR>hy : y ∈ I<GOAL>(Algebra.trace (FractionRing A) (FractionRing B)) ((FractionRing.algEquiv B L).symm x * y) ∈ 1 ↔ (Algebra.trace K L) (x * (FractionRing.algEquiv B L) y) ∈ 1
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁹ : CommRing A<VAR>inst✝¹⁸ : Field K<VAR>inst✝¹⁷ : CommRing B<VAR>inst✝¹⁶ : Field L<VAR>inst✝¹⁵ : Algebra A K<VAR>inst✝¹⁴ : Algebra B L<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : Algebra K L<VAR>inst✝¹¹ : Algebra A L<VAR>inst✝¹⁰ : IsScalarTower A K L<VAR>inst✝⁹ : IsScalarTower A B L<VAR>inst✝⁸ : IsDomain A<VAR>inst✝⁷ : IsFractionRing A K<VAR>inst✝⁶ : IsIntegralClosure B A L<VAR>inst✝⁵ : IsFractionRing B L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>inst✝² : IsDomain B<VAR>inst✝¹ : IsIntegrallyClosed A<VAR>inst✝ : NoZeroSMulDivisors A B<VAR>I : Submodule B (FractionRing B)<VAR>x : L<VAR>y : FractionRing B<VAR>hy : y ∈ I<GOAL>(FractionRing.algEquiv A K).toRingEquiv.symm ((Algebra.trace K L) ((FractionRing.algEquiv B L).toRingEquiv ((FractionRing.algEquiv B L).symm x * y))) ∈ 1 ↔ (Algebra.trace K L) (x * (FractionRing.algEquiv B L) y) ∈ 1
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁹ : CommRing A<VAR>inst✝¹⁸ : Field K<VAR>inst✝¹⁷ : CommRing B<VAR>inst✝¹⁶ : Field L<VAR>inst✝¹⁵ : Algebra A K<VAR>inst✝¹⁴ : Algebra B L<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : Algebra K L<VAR>inst✝¹¹ : Algebra A L<VAR>inst✝¹⁰ : IsScalarTower A K L<VAR>inst✝⁹ : IsScalarTower A B L<VAR>inst✝⁸ : IsDomain A<VAR>inst✝⁷ : IsFractionRing A K<VAR>inst✝⁶ : IsIntegralClosure B A L<VAR>inst✝⁵ : IsFractionRing B L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>inst✝² : IsDomain B<VAR>inst✝¹ : IsIntegrallyClosed A<VAR>inst✝ : NoZeroSMulDivisors A B<VAR>I : Submodule B (FractionRing B)<VAR>x : L<VAR>y : FractionRing B<VAR>hy : y ∈ I<GOAL>(algebraMap K L).comp ↑(FractionRing.algEquiv A K).toRingEquiv = (↑(FractionRing.algEquiv B L).toRingEquiv).comp (algebraMap (FractionRing A) (FractionRing B))
<VAR>C✝ : Type u<VAR>𝒞 : Category.{v, u} C✝<VAR>inst✝² : MonoidalCategory C✝<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : MonoidalCategory C<VAR>U V W X✝ Y✝ Z X Y : C<GOAL>X ◁ (ρ_ Y).hom = (α_ X Y (𝟙_ C)).inv ≫ (ρ_ (X ⊗ Y)).hom
<VAR>a b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>hn : n % 2 = 1<GOAL>2 * (n / 2) = n - 1
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D✝ : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D✝<VAR>J : Type u<VAR>inst✝ : Category.{v, u} J<VAR>T : Comonad C<VAR>D : J ⥤ T.Coalgebra<VAR>c : Cocone (D ⋙ T.forget)<VAR>t : IsColimit c<VAR>X Y : J<VAR>f : X ⟶ Y<GOAL>(D.map f).f ≫ c.ι.app Y = c.ι.app X ≫ 𝟙 c.pt
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D✝ : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D✝<VAR>J : Type u<VAR>inst✝ : Category.{v, u} J<VAR>T : Comonad C<VAR>D : J ⥤ T.Coalgebra<VAR>c : Cocone (D ⋙ T.forget)<VAR>t : IsColimit c<VAR>X Y : J<VAR>f : X ⟶ Y<GOAL>c.ι.app X = c.ι.app X ≫ 𝟙 c.pt
<VAR>m n✝ n a✝ p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>a : ZMod p<VAR>h : a ≠ 0<GOAL>a * a⁻¹ = 1
<VAR>m n✝ n a p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>k : ℕ<VAR>h : ↑k ≠ 0<GOAL>↑k * (↑k)⁻¹ = 1
<VAR>m n✝ n a p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>k : ℕ<VAR>h : ↑k ≠ 0<GOAL>k.Coprime p
<VAR>m n✝ n a p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>k : ℕ<VAR>h : ↑k ≠ 0<GOAL>p.Coprime k
<VAR>x : PGame<VAR>h : x ≈ 0<GOAL>x⁻¹ = 0
<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>A : C<VAR>inst✝¹ : S₁.HasHomology<VAR>inst✝ : S₂.HasHomology<VAR>h : Mono (opcyclesMap φ)<GOAL>Mono (homologyMap φ)
<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>A : C<VAR>inst✝¹ : S₁.HasHomology<VAR>inst✝ : S₂.HasHomology<VAR>h : Mono (opcyclesMap φ)<VAR>this : Mono (homologyMap φ ≫ S₂.homologyι)<GOAL>Mono (homologyMap φ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹³ : Zero β<VAR>inst✝¹² : One β<VAR>inst✝¹¹ : Add β<VAR>inst✝¹⁰ : Mul β<VAR>inst✝⁹ : Neg β<VAR>inst✝⁸ : Sub β<VAR>inst✝⁷ : SMul ℕ β<VAR>inst✝⁶ : SMul ℤ β<VAR>inst✝⁵ : Pow β ℕ<VAR>inst✝⁴ : NatCast β<VAR>inst✝³ : IntCast β<VAR>f : α → β<VAR>hf : Surjective f<VAR>inst✝² : Mul α<VAR>inst✝¹ : Add α<VAR>inst✝ : LeftDistribClass α<VAR>add : ∀ (x y : α), f (x + y) = f x + f y<VAR>mul : ∀ (x y : α), f (x * y) = f x * f y<VAR>x y z : α<GOAL>f x * (f y + f z) = f x * f y + f x * f z
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝¹ : CommRing R<VAR>x y z : R<VAR>inst✝ : IsPrincipal (Ideal.span {x, y})<VAR>h : IsRelPrime x y<GOAL>IsCoprime x y
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝¹ : CommRing R<VAR>x y z : R<VAR>inst✝ : IsPrincipal (Ideal.span {x, y})<VAR>h : IsRelPrime x y<GOAL>IsUnit (gcd x y)
<VAR>a x z : ℂ<GOAL>arg 0 = 0
<VAR>R : Type<VAR>inst✝ : CommRing R<VAR>d : ℤ<VAR>a : ℤ√d<GOAL>a.norm = 1 ↔ a ∈ unitary (ℤ√d)
<VAR>R : Type<VAR>inst✝ : CommRing R<VAR>d : ℤ<VAR>a : ℤ√d<GOAL>a.norm = 1 ↔ ↑a.norm = 1
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>R✝ I J X Y : Set α<VAR>M : Matroid α<VAR>R : Set α<GOAL>M ↾ R ↾ R = M ↾ R
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : PseudoMetrizableSpace α<VAR>inst✝² : OpensMeasurableSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : PseudoMetrizableSpace β<VAR>f : α → β<VAR>s : Set α<VAR>μ : Measure α<VAR>hf : ContinuousOn f s<VAR>hs : MeasurableSet s<VAR>h's : IsSeparable s<VAR>this : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α<VAR>this✝¹ : MeasurableSpace β := borel β<VAR>this✝ : BorelSpace β<GOAL>AEStronglyMeasurable f (μ.restrict s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : PseudoMetrizableSpace α<VAR>inst✝² : OpensMeasurableSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : PseudoMetrizableSpace β<VAR>f : α → β<VAR>s : Set α<VAR>μ : Measure α<VAR>hf : ContinuousOn f s<VAR>hs : MeasurableSet s<VAR>h's : IsSeparable s<VAR>this : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α<VAR>this✝¹ : MeasurableSpace β := borel β<VAR>this✝ : BorelSpace β<GOAL>AEMeasurable f (μ.restrict s) ∧ ∃ t, IsSeparable t ∧ ∀ᵐ (x : α) ∂μ.restrict s, f x ∈ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : PseudoMetrizableSpace α<VAR>inst✝² : OpensMeasurableSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : PseudoMetrizableSpace β<VAR>f : α → β<VAR>s : Set α<VAR>μ : Measure α<VAR>hf : ContinuousOn f s<VAR>hs : MeasurableSet s<VAR>h's : IsSeparable s<VAR>this : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α<VAR>this✝¹ : MeasurableSpace β := borel β<VAR>this✝ : BorelSpace β<GOAL>∀ᵐ (x : α) ∂μ.restrict s, f x ∈ f '' s
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>M✝ : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₁' : Type u_9<VAR>M₂' : Type u_10<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>ι : Type u_16<VAR>inst✝¹⁸ : CommSemiring R<VAR>inst✝¹⁷ : AddCommMonoid M₁<VAR>inst✝¹⁶ : Module R M₁<VAR>inst✝¹⁵ : AddCommMonoid M₂<VAR>inst✝¹⁴ : Module R M₂<VAR>inst✝¹³ : AddCommMonoid N₂<VAR>inst✝¹² : Module R N₂<VAR>inst✝¹¹ : DecidableEq n<VAR>inst✝¹⁰ : Fintype n<VAR>inst✝⁹ : DecidableEq m<VAR>inst✝⁸ : Fintype m<VAR>b₁✝ : Basis n R M₁<VAR>b₂✝ : Basis m R M₂<VAR>b₁ : Basis n R M₁<VAR>b₂ : Basis m R M₂<VAR>inst✝⁷ : AddCommMonoid M₁'<VAR>inst✝⁶ : Module R M₁'<VAR>inst✝⁵ : AddCommMonoid M₂'<VAR>inst✝⁴ : Module R M₂'<VAR>b₁' : Basis n' R M₁'<VAR>b₂' : Basis m' R M₂'<VAR>inst✝³ : Fintype n'<VAR>inst✝² : Fintype m'<VAR>inst✝¹ : DecidableEq n'<VAR>inst✝ : DecidableEq m'<VAR>B : M₁ →ₗ[R] M₂ →ₗ[R] R<VAR>M : Matrix n' n R<GOAL>M * (toMatrix₂ b₁ b₂) B = (toMatrix₂ b₁' b₂) (B ∘ₗ (toLin b₁' b₁) Mᵀ)
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Field F<VAR>i : K →+* L<VAR>f : K[X]<VAR>s : Multiset L<VAR>hs : map i f = C (i f.leadingCoeff) * (Multiset.map (fun a => X - C a) s).prod<VAR>this : DecidableEq K := Classical.decEq K<VAR>hf0 : ¬f = 0<VAR>p : L[X]<VAR>hp : Irreducible p<VAR>hdp : p ∣ map i f<GOAL>p.degree = 1
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Field F<VAR>i : K →+* L<VAR>f : K[X]<VAR>s : Multiset L<VAR>hs : map i f = C (i f.leadingCoeff) * (Multiset.map (fun a => X - C a) s).prod<VAR>this : DecidableEq K := Classical.decEq K<VAR>hf0 : ¬f = 0<VAR>p : L[X]<VAR>hp : Prime p<VAR>hdp : p ∣ map i f<GOAL>p.degree = 1
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Field F<VAR>i : K →+* L<VAR>f : K[X]<VAR>s : Multiset L<VAR>hs : map i f = C (i f.leadingCoeff) * (Multiset.map (fun a => X - C a) s).prod<VAR>this : DecidableEq K := Classical.decEq K<VAR>hf0 : ¬f = 0<VAR>p : L[X]<VAR>hp : Prime p<VAR>hdp : p ∣ C (i f.leadingCoeff) * (Multiset.map (fun a => X - C a) s).toList.prod<GOAL>p.degree = 1
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Field F<VAR>i : K →+* L<VAR>f : K[X]<VAR>s : Multiset L<VAR>hs : map i f = C (i f.leadingCoeff) * (Multiset.map (fun a => X - C a) s).prod<VAR>this : DecidableEq K := Classical.decEq K<VAR>hf0 : ¬f = 0<VAR>p : L[X]<VAR>hp : Prime p<VAR>hdp : p ∣ C (i f.leadingCoeff) * (Multiset.map (fun a => X - C a) s).toList.prod<VAR>hd : p ∣ C (i f.leadingCoeff)<GOAL>p.degree = 1
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Field F<VAR>i : K →+* L<VAR>f : K[X]<VAR>s : Multiset L<VAR>hs : map i f = C (i f.leadingCoeff) * (Multiset.map (fun a => X - C a) s).prod<VAR>this : DecidableEq K := Classical.decEq K<VAR>hf0 : ¬f = 0<VAR>p : L[X]<VAR>hp : Prime p<VAR>hdp : p ∣ C (i f.leadingCoeff) * (Multiset.map (fun a => X - C a) s).toList.prod<VAR>hd : p ∣ (Multiset.map (fun a => X - C a) s).toList.prod<GOAL>p.degree = 1