ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.25278, u_1} C<VAR>inst✝ : Category.{?u.25282, u_2} D<VAR>F G : C ⥤ Cat<VAR>α : F ⟶ G<VAR>X Y Z : Grothendieck F<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>(((eqToHom ⋯).app X.fiber ≫ eqToHom ⋯) ≫ (α.app Z.base).map ((F.map g.base).map f.fiber)) ≫ (α.app Z.base).map g.fiber = (((eqToHom ⋯ ≫ (G.map g.base).map ((eqToHom ⋯).app X.fiber)) ≫ (G.map g.base).map ((α.app Y.base).map f.fiber)) ≫ (eqToHom ⋯).app Y.fiber) ≫ (α.app Z.base).map g.fiber
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.25278, u_1} C<VAR>inst✝ : Category.{?u.25282, u_2} D<VAR>F G : C ⥤ Cat<VAR>α : F ⟶ G<VAR>X Y Z : Grothendieck F<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>((eqToHom ⋯).app X.fiber ≫ eqToHom ⋯) ≫ (α.app Z.base).map ((F.map g.base).map f.fiber) = ((eqToHom ⋯ ≫ (G.map g.base).map ((eqToHom ⋯).app X.fiber)) ≫ (G.map g.base).map ((α.app Y.base).map f.fiber)) ≫ (eqToHom ⋯).app Y.fiber
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.25278, u_1} C<VAR>inst✝ : Category.{?u.25282, u_2} D<VAR>F G : C ⥤ Cat<VAR>α : F ⟶ G<VAR>X Y Z : Grothendieck F<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>(eqToHom ⋯).app X.fiber ≫ eqToHom ⋯ ≫ (α.app Z.base).map ((F.map g.base).map f.fiber) = eqToHom ⋯ ≫ (G.map g.base).map ((eqToHom ⋯).app X.fiber) ≫ (G.map g.base).map ((α.app Y.base).map f.fiber) ≫ (eqToHom ⋯).app Y.fiber
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.25278, u_1} C<VAR>inst✝ : Category.{?u.25282, u_2} D<VAR>F G : C ⥤ Cat<VAR>α : F ⟶ G<VAR>X Y Z : Grothendieck F<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>eqToHom ⋯ ≫ eqToHom ⋯ ≫ (α.app Z.base).map ((F.map g.base).map f.fiber) = eqToHom ⋯ ≫ (G.map g.base).map (eqToHom ⋯) ≫ (G.map g.base).map ((α.app Y.base).map f.fiber) ≫ eqToHom ⋯
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.25278, u_1} C<VAR>inst✝ : Category.{?u.25282, u_2} D<VAR>F G : C ⥤ Cat<VAR>α : F ⟶ G<VAR>X Y Z : Grothendieck F<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>eqToHom ⋯ ≫ eqToHom ⋯ ≫ (α.app Z.base).map ((F.map g.base).map f.fiber) = eqToHom ⋯ ≫ (G.map g.base).map (eqToHom ⋯) ≫ (eqToHom ⋯ ≫ (F.map g.base ≫ α.app Z.base).map f.fiber ≫ eqToHom ⋯) ≫ eqToHom ⋯
<VAR>R : Type u_1<VAR>r : R<VAR>inst✝ : Semiring R<VAR>P : R[X]<VAR>n : ℕ<VAR>hnil : IsNilpotent r<GOAL>IsNilpotent (X ^ n * C r)
<VAR>R : Type u_1<VAR>r : R<VAR>inst✝ : Semiring R<VAR>P : R[X]<VAR>n : ℕ<VAR>hnil : IsNilpotent r<GOAL>IsNilpotent (C r * X ^ n)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>ι : Sort u_6<VAR>κ : ι → Sort u_7<VAR>inst✝³ : FunLike F α β<VAR>inst✝² : SupSet α<VAR>inst✝¹ : SupSet β<VAR>inst✝ : sSupHomClass F α β<VAR>f : F<VAR>g : ι → α<GOAL>f (⨆ i, g i) = ⨆ i, f (g i)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁵ : LinearOrderedCommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>P : RootPairing ι R M N<VAR>B : M →ₗ[R] M →ₗ[R] R<VAR>inst✝ : P.IsRootPositive B<VAR>i j : ι<GOAL>P.pairing i j = 0 ↔ P.pairing j i = 0
<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>H K : Subgroup G<VAR>ι : Sort u_5<VAR>S : ι → Subgroup G<GOAL>↑(⨅ i, S i) = ⋂ i, ↑(S i)
<VAR>x y : ℝ<GOAL>cos (x - y) = cos x * cos y + sin x * sin y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>n : ℕ<GOAL>(∑' (i : ℕ), if n ≤ i then 2⁻¹ ^ i else 0) = 2 * 2⁻¹ ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>n : ℕ<VAR>A : Summable fun i => if n ≤ i then 2⁻¹ ^ i else 0<GOAL>(∑' (i : ℕ), if n ≤ i then 2⁻¹ ^ i else 0) = 2 * 2⁻¹ ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>n : ℕ<VAR>A : Summable fun i => if n ≤ i then 2⁻¹ ^ i else 0<VAR>B : (∑ i ∈ Finset.range n, if n ≤ i then 2⁻¹ ^ i else 0) = 0<GOAL>(∑' (i : ℕ), if n ≤ i then 2⁻¹ ^ i else 0) = 2 * 2⁻¹ ^ n
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : CommMonoid M<VAR>f : α → M<VAR>a b : α<VAR>inst✝ : LocallyFiniteOrder α<VAR>h : a ≤ b<GOAL>(∏ x ∈ Ioc a b, f x) * f a = ∏ x ∈ Icc a b, f x
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p✝ q : MvPolynomial σ R<VAR>f : R →+* S₁<VAR>g : σ → S₁<VAR>p : MvPolynomial σ R<GOAL>eval₂ f g p = (eval₂Hom (RingHom.id S₁) g) ((eval₂Hom (C.comp f) X) p)
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p✝ q : MvPolynomial σ R<VAR>f : R →+* S₁<VAR>g : σ → S₁<VAR>p : MvPolynomial σ R<GOAL>eval₂ f g p = eval₂ (RingHom.id S₁) g (eval₂ (C.comp f) X p)
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p✝ q : MvPolynomial σ R<VAR>f : R →+* S₁<VAR>g : σ → S₁<VAR>p : MvPolynomial σ R<VAR>h : (eval₂Hom (RingHom.id S₁) g) (eval₂ (C.comp f) X p) = eval₂ ((eval₂Hom (RingHom.id S₁) g).comp (C.comp f)) (⇑(eval₂Hom (RingHom.id S₁) g) ∘ X) p<GOAL>eval₂ f g p = eval₂ (RingHom.id S₁) g (eval₂ (C.comp f) X p)
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p✝ q : MvPolynomial σ R<VAR>f : R →+* S₁<VAR>g : σ → S₁<VAR>p : MvPolynomial σ R<VAR>h : eval₂ (RingHom.id S₁) g (eval₂ (C.comp f) X p) = eval₂ ((eval₂Hom (RingHom.id S₁) g).comp (C.comp f)) (eval₂ (RingHom.id S₁) g ∘ X) p<GOAL>eval₂ f g p = eval₂ (RingHom.id S₁) g (eval₂ (C.comp f) X p)
<VAR>R : Type u<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : IsDomain R<VAR>inst✝⁴ : IsPrincipalIdealRing R<VAR>M : Type v<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>N : Type (max u v)<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>p : R<VAR>hp : Irreducible p<VAR>hM : IsTorsion' M ↥(Submonoid.powers p)<VAR>dec : (x : M) → Decidable (x = 0)<VAR>z : M<VAR>hz : IsTorsionBy R M (p ^ pOrder hM z)<VAR>k : ℕ<VAR>f : R ⧸ Submodule.span R {p ^ k} →ₗ[R] M ⧸ Submodule.span R {z}<GOAL>∃ x, p ^ k • x = 0 ∧ Submodule.Quotient.mk x = f 1
<VAR>R : Type u<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : IsDomain R<VAR>inst✝⁴ : IsPrincipalIdealRing R<VAR>M : Type v<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>N : Type (max u v)<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>p : R<VAR>hp : Irreducible p<VAR>hM : IsTorsion' M ↥(Submonoid.powers p)<VAR>dec : (x : M) → Decidable (x = 0)<VAR>z : M<VAR>hz : IsTorsionBy R M (p ^ pOrder hM z)<VAR>k : ℕ<VAR>f : R ⧸ Submodule.span R {p ^ k} →ₗ[R] M ⧸ Submodule.span R {z}<VAR>f1 : ∃ a, Submodule.Quotient.mk a = f 1<GOAL>∃ x, p ^ k • x = 0 ∧ Submodule.Quotient.mk x = f 1
<VAR>R : Type u<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : IsDomain R<VAR>inst✝⁴ : IsPrincipalIdealRing R<VAR>M : Type v<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>N : Type (max u v)<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>p : R<VAR>hp : Irreducible p<VAR>hM : IsTorsion' M ↥(Submonoid.powers p)<VAR>dec : (x : M) → Decidable (x = 0)<VAR>z : M<VAR>hz : IsTorsionBy R M (p ^ pOrder hM z)<VAR>k : ℕ<VAR>f : R ⧸ Submodule.span R {p ^ k} →ₗ[R] M ⧸ Submodule.span R {z}<VAR>f1 : ∃ a, Submodule.Quotient.mk a = f 1<VAR>this : p ^ k • f1.choose ∈ Submodule.span R {z}<GOAL>∃ x, p ^ k • x = 0 ∧ Submodule.Quotient.mk x = f 1
<VAR>R : Type u<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : IsDomain R<VAR>inst✝⁴ : IsPrincipalIdealRing R<VAR>M : Type v<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>N : Type (max u v)<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>p : R<VAR>hp : Irreducible p<VAR>hM : IsTorsion' M ↥(Submonoid.powers p)<VAR>dec : (x : M) → Decidable (x = 0)<VAR>z : M<VAR>hz : IsTorsionBy R M (p ^ pOrder hM z)<VAR>k : ℕ<VAR>f : R ⧸ Submodule.span R {p ^ k} →ₗ[R] M ⧸ Submodule.span R {z}<VAR>f1 : ∃ a, Submodule.Quotient.mk a = f 1<VAR>this : p ^ k • f1.choose ∈ Submodule.span R {z}<VAR>a : R<VAR>ha : p ^ k • f1.choose = p ^ k • a • z<GOAL>∃ x, p ^ k • x = 0 ∧ Submodule.Quotient.mk x = f 1
<VAR>R : Type u<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : IsDomain R<VAR>inst✝⁴ : IsPrincipalIdealRing R<VAR>M : Type v<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>N : Type (max u v)<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>p : R<VAR>hp : Irreducible p<VAR>hM : IsTorsion' M ↥(Submonoid.powers p)<VAR>dec : (x : M) → Decidable (x = 0)<VAR>z : M<VAR>hz : IsTorsionBy R M (p ^ pOrder hM z)<VAR>k : ℕ<VAR>f : R ⧸ Submodule.span R {p ^ k} →ₗ[R] M ⧸ Submodule.span R {z}<VAR>f1 : ∃ a, Submodule.Quotient.mk a = f 1<VAR>this : p ^ k • f1.choose ∈ Submodule.span R {z}<VAR>a : R<VAR>ha : p ^ k • f1.choose = p ^ k • a • z<GOAL>Submodule.Quotient.mk (f1.choose - a • z) = f 1
<VAR>m : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝⁴ : Fintype m<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : IsDomain A<VAR>inst✝ : DecidableEq m<VAR>M : Matrix m m A<VAR>hM : M.det ≠ 0<VAR>v : m → A<VAR>hv : M *ᵥ v = 0<GOAL>Mᵀ.det ≠ 0
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>E : Type u_2<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module R F<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Module R G<VAR>g : Submodule R (E × F)<VAR>hg : ∀ {x : E × F}, x ∈ g → x.1 = 0 → x.2 = 0<VAR>a : E<VAR>ha : a ∈ map (LinearMap.fst R E F) g<GOAL>∃! b, (a, b) ∈ g
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>E : Type u_2<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module R F<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Module R G<VAR>g : Submodule R (E × F)<VAR>hg : ∀ {x : E × F}, x ∈ g → x.1 = 0 → x.2 = 0<VAR>a : E<VAR>ha : a ∈ map (LinearMap.fst R E F) g<GOAL>∃ x, (a, x) ∈ g
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>E : Type u_2<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module R F<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Module R G<VAR>g : Submodule R (E × F)<VAR>hg : ∀ {x : E × F}, x ∈ g → x.1 = 0 → x.2 = 0<VAR>a : E<VAR>ha : a ∈ map (LinearMap.fst R E F) g<GOAL>∀ (y₁ y₂ : F), (a, y₁) ∈ g → (a, y₂) ∈ g → y₁ = y₂
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>E : Type u_2<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module R F<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Module R G<VAR>g : Submodule R (E × F)<VAR>hg : ∀ {x : E × F}, x ∈ g → x.1 = 0 → x.2 = 0<VAR>a : E<VAR>ha : a ∈ map (LinearMap.fst R E F) g<VAR>y₁ y₂ : F<VAR>hy₁ : (a, y₁) ∈ g<VAR>hy₂ : (a, y₂) ∈ g<GOAL>y₁ = y₂
<VAR>R : Type u_1<VAR>inst✝⁶ : Ring R<VAR>E : Type u_2<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module R E<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module R F<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup G<VAR>inst✝ : Module R G<VAR>g : Submodule R (E × F)<VAR>hg : ∀ {x : E × F}, x ∈ g → x.1 = 0 → x.2 = 0<VAR>a : E<VAR>ha : a ∈ map (LinearMap.fst R E F) g<VAR>y₁ y₂ : F<VAR>hy₁ : (a, y₁) ∈ g<VAR>hy₂ : (a, y₂) ∈ g<VAR>hy : (0, y₁ - y₂) ∈ g<GOAL>y₁ = y₂
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>hodd : p ≠ 2<GOAL>¬∃ n, ↑↑p ∣ hζ.toInteger - ↑n
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>inst✝¹ : Field K<VAR>inst✝ : CharZero K<VAR>ζ : K<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K<VAR>hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))<VAR>hodd : p ≠ 2<VAR>h : p ^ (k + 1) = 2<GOAL>False
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : LinearOrderedField β<VAR>a✝ a₁ a₂ : α<VAR>b✝ : β<VAR>q : ℚ<VAR>inst✝ : Archimedean α<VAR>a b : α<GOAL>cutMap β (a + b) = cutMap β a + cutMap β b
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : LinearOrderedField β<VAR>a✝ a₁ a₂ : α<VAR>b✝ : β<VAR>q✝ : ℚ<VAR>inst✝ : Archimedean α<VAR>a b : α<VAR>q : ℚ<VAR>hq : q ∈ {t | ↑t < a + b}<GOAL>q ∈ Rat.cast ⁻¹' (cutMap β a + cutMap β b)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : LinearOrderedField α<VAR>inst✝¹ : LinearOrderedField β<VAR>a✝ a₁ a₂ : α<VAR>b✝ : β<VAR>q : ℚ<VAR>inst✝ : Archimedean α<VAR>a b : α<GOAL>cutMap β a + cutMap β b ⊆ Rat.cast '' {t | ↑t < a + b}
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : Ring S<VAR>M : Type u_4<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>m : Submodule R M<VAR>N : Type u_5<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>inst✝ : IsSimpleModule R M<VAR>f : M →ₗ[R] N<GOAL>Function.Injective ⇑f ∨ f = 0
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : Ring S<VAR>M : Type u_4<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>m : Submodule R M<VAR>N : Type u_5<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>inst✝ : IsSimpleModule R M<VAR>f : M →ₗ[R] N<GOAL>ker f = ⊥ ∨ ker f = ⊤
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<GOAL>Flat R M ↔ ∀ (I : Ideal R), Function.Injective ⇑(rTensor M (Submodule.subtype I))
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<GOAL>(∀ ⦃I : Ideal R⦄, I.FG → Function.Injective ⇑(rTensor M (Submodule.subtype I))) ↔ ∀ (I : Ideal R), Function.Injective ⇑(rTensor M (Submodule.subtype I))
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>h : ∀ ⦃I : Ideal R⦄, I.FG → Function.Injective ⇑(rTensor M (Submodule.subtype I))<VAR>I : Ideal R<GOAL>Function.Injective ⇑(rTensor M (Submodule.subtype I))
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>h : ∀ ⦃I : Ideal R⦄, I.FG → Function.Injective ⇑(rTensor M (Submodule.subtype I))<VAR>I : Ideal R<GOAL>∀ (a : ↥I ⊗[R] M), (rTensor M (Submodule.subtype I)) a = 0 → a = 0
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>h : ∀ ⦃I : Ideal R⦄, I.FG → Function.Injective ⇑(rTensor M (Submodule.subtype I))<VAR>I : Ideal R<VAR>x : ↥I ⊗[R] M<VAR>hx₀ : (rTensor M (Submodule.subtype I)) x = 0<GOAL>x = 0
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>h : ∀ ⦃I : Ideal R⦄, I.FG → Function.Injective ⇑(rTensor M (Submodule.subtype I))<VAR>I : Ideal R<VAR>J : Submodule R R<VAR>hfg : J.FG<VAR>hle : J ≤ I<VAR>y : ↥J ⊗[R] M<VAR>hx₀ : (rTensor M (Submodule.subtype I)) ((rTensor M (inclusion hle)) y) = 0<GOAL>(rTensor M (inclusion hle)) y = 0
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>h : ∀ ⦃I : Ideal R⦄, I.FG → Function.Injective ⇑(rTensor M (Submodule.subtype I))<VAR>I : Ideal R<VAR>J : Submodule R R<VAR>hfg : J.FG<VAR>hle : J ≤ I<VAR>y : ↥J ⊗[R] M<VAR>hx₀ : (rTensor M (Submodule.subtype I ∘ₗ inclusion hle)) y = 0<GOAL>(rTensor M (inclusion hle)) y = 0
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S : Finset E<VAR>P : IntermediateField F E → Prop<VAR>base : P ⊥<VAR>ih : ∀ (K : IntermediateField F E), ∀ x ∈ S, P K → P (restrictScalars F (↥K)⟮x⟯)<GOAL>P (adjoin F ↑S)
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S : Finset E<VAR>P : IntermediateField F E → Prop<VAR>base : P ⊥<VAR>ih : ∀ (K : IntermediateField F E), ∀ x ∈ S, P K → P (restrictScalars F (↥K)⟮x⟯)<GOAL>P (adjoin F ↑∅)
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S : Finset E<VAR>P : IntermediateField F E → Prop<VAR>base : P ⊥<VAR>ih : ∀ (K : IntermediateField F E), ∀ x ∈ S, P K → P (restrictScalars F (↥K)⟮x⟯)<VAR>a✝ : E<VAR>s✝ : Finset E<VAR>ha : a✝ ∈ S<VAR>x✝¹ : s✝ ⊆ S<VAR>x✝ : a✝ ∉ s✝<VAR>h : P (adjoin F ↑s✝)<GOAL>P (adjoin F ↑(insert a✝ s✝))
<VAR>R : Type u_1<VAR>n✝ : ℕ<VAR>x y : ℤ<VAR>n : ℕ<VAR>hxy : 2 ∣ x - y<VAR>hx : ¬2 ∣ x<VAR>hn : Even n<GOAL>multiplicity 2 (x ^ n - y ^ n) + 1 = multiplicity 2 (x + y) + multiplicity 2 (x - y) + multiplicity 2 ↑n
<VAR>R : Type u_1<VAR>n✝ : ℕ<VAR>x y : ℤ<VAR>n : ℕ<VAR>hxy : 2 ∣ x - y<VAR>hx : ¬2 ∣ x<VAR>hn : Even n<VAR>hy : Odd y<GOAL>multiplicity 2 (x ^ n - y ^ n) + 1 = multiplicity 2 (x + y) + multiplicity 2 (x - y) + multiplicity 2 ↑n
<VAR>R : Type u_1<VAR>n : ℕ<VAR>x y : ℤ<VAR>hxy : 2 ∣ x - y<VAR>hx : ¬2 ∣ x<VAR>hy : Odd y<VAR>d : ℕ<GOAL>multiplicity 2 (x ^ (d + d) - y ^ (d + d)) + 1 = multiplicity 2 (x + y) + multiplicity 2 (x - y) + multiplicity 2 ↑(d + d)
<VAR>R : Type u_1<VAR>n : ℕ<VAR>x y : ℤ<VAR>hxy : 2 ∣ x - y<VAR>hx : ¬2 ∣ x<VAR>hy : Odd y<VAR>d : ℕ<GOAL>multiplicity 2 ((x ^ 2) ^ d - (y ^ 2) ^ d) + 1 = multiplicity 2 (x + y) + multiplicity 2 (x - y) + multiplicity 2 ↑(2 * d)
<VAR>R : Type u_1<VAR>n : ℕ<VAR>x y : ℤ<VAR>hxy : 2 ∣ x - y<VAR>hx : ¬2 ∣ x<VAR>hy : Odd y<VAR>d : ℕ<VAR>hxy4 : 4 ∣ x ^ 2 - y ^ 2<GOAL>multiplicity 2 ((x ^ 2) ^ d - (y ^ 2) ^ d) + 1 = multiplicity 2 (x + y) + multiplicity 2 (x - y) + multiplicity 2 ↑(2 * d)
<VAR>R : Type u_1<VAR>n : ℕ<VAR>x y : ℤ<VAR>hxy : 2 ∣ x - y<VAR>hx : ¬2 ∣ x<VAR>hy : Odd y<VAR>d : ℕ<VAR>hxy4 : 4 ∣ x ^ 2 - y ^ 2<GOAL>multiplicity 2 (x + y) + multiplicity 2 (x - y) + multiplicity 2 ↑d + 1 = multiplicity 2 (x + y) + multiplicity 2 (x - y) + (multiplicity 2 ↑2 + multiplicity 2 ↑d)
<VAR>R : Type u_1<VAR>n : ℕ<VAR>x y : ℤ<VAR>hxy : 2 ∣ x - y<VAR>hx : ¬2 ∣ x<VAR>hy : Odd y<VAR>d : ℕ<VAR>hxy4 : 4 ∣ x ^ 2 - y ^ 2<GOAL>¬2 ∣ x ^ 2
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : LieRingModule L M<VAR>inst✝¹ : LieModule R L M<VAR>inst✝ : IsNilpotent R L M<VAR>x : L<GOAL>posFittingCompOf R M x = ⊥
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁵ : MeasurableSpace X<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : MeasurableSpace Y<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedAddCommGroup F<VAR>f g✝ : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>hf : LocallyIntegrable f μ<VAR>g : X → F<VAR>hg : AEStronglyMeasurable g μ<VAR>h : ∀ᵐ (x : X) ∂μ, ‖g x‖ ≤ ‖f x‖<GOAL>LocallyIntegrable g μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁵ : MeasurableSpace X<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : MeasurableSpace Y<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedAddCommGroup F<VAR>f g✝ : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>hf : LocallyIntegrableOn f univ μ<VAR>g : X → F<VAR>hg : AEStronglyMeasurable g μ<VAR>h : ∀ᵐ (x : X) ∂μ, ‖g x‖ ≤ ‖f x‖<GOAL>LocallyIntegrableOn g univ μ
<VAR>α : Type u<VAR>inst✝² : Group α<VAR>inst✝¹ : LE α<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c d : α<GOAL>a / b ≤ 1 ↔ a ≤ b
<VAR>C : Type u₁<VAR>inst✝ : Category.{v, u₁} C<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>U : Y.Opens<GOAL>IsPullback ((pullbackRestrictIsoRestrict f U).inv ≫ pullback.snd f U.ι) (f ⁻¹ᵁ U).ι U.ι f
<VAR>C : Type u₁<VAR>inst✝ : Category.{v, u₁} C<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>U : Y.Opens<GOAL>IsPullback ((pullbackRestrictIsoRestrict (𝟙 X ≫ f) U).inv ≫ pullback.snd (𝟙 X ≫ f) U.ι) ((𝟙 X ≫ f) ⁻¹ᵁ U).ι U.ι (𝟙 X ≫ f)
<VAR>C : Type u₁<VAR>inst✝ : Category.{v, u₁} C<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>U : Y.Opens<GOAL>(pullbackRestrictIsoRestrict (𝟙 X ≫ f) U).inv ≫ pullback.fst f (Y.ofRestrict ⋯) = ((𝟙 X ≫ f) ⁻¹ᵁ U).ι ≫ 𝟙 X
<VAR>C : Type u₁<VAR>inst✝ : Category.{v, u₁} C<VAR>X Y : Scheme<VAR>f : X ⟶ Y<VAR>U : Y.Opens<GOAL>((𝟙 X ≫ f) ⁻¹ᵁ U).ι = ((𝟙 X ≫ f) ⁻¹ᵁ U).ι ≫ 𝟙 X
<VAR>R✝ : Type u_1<VAR>inst✝³ : CommMonoid R✝<VAR>R' : Type u_2<VAR>inst✝² : CommMonoidWithZero R'<VAR>R : Type u_3<VAR>inst✝¹ : CommMonoidWithZero R<VAR>inst✝ : Nontrivial R<VAR>χ : MulChar R R'<GOAL>χ 0 = 0
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : DecidableEq α<VAR>C : AList β → Sort u_1<VAR>H0 : C ∅<VAR>IH : (a : α) → (b : β a) → (l : AList β) → a ∉ l → C l → C (insert a b l)<VAR>c : Sigma β<VAR>l : List (Sigma β)<VAR>hl : l.NodupKeys<VAR>h : c.fst ∉ { entries := l, nodupKeys := hl }<GOAL>insertRec H0 IH (insert c.fst c.snd { entries := l, nodupKeys := hl }) = IH c.fst c.snd { entries := l, nodupKeys := hl } h (insertRec H0 IH { entries := l, nodupKeys := hl })
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : DecidableEq α<VAR>C : AList β → Sort u_1<VAR>H0 : C ∅<VAR>IH : (a : α) → (b : β a) → (l : AList β) → a ∉ l → C l → C (insert a b l)<VAR>c : Sigma β<VAR>l : List (Sigma β)<VAR>hl : l.NodupKeys<VAR>h : c.fst ∉ { entries := l, nodupKeys := hl }<GOAL>HEq (insertRec H0 IH { entries := c :: l, nodupKeys := ⋯ }) (IH c.fst c.snd { entries := l, nodupKeys := hl } h (insertRec H0 IH { entries := l, nodupKeys := hl }))
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : DecidableEq α<VAR>C : AList β → Sort u_1<VAR>H0 : C ∅<VAR>IH : (a : α) → (b : β a) → (l : AList β) → a ∉ l → C l → C (insert a b l)<VAR>c : Sigma β<VAR>l : List (Sigma β)<VAR>hl : l.NodupKeys<VAR>h : c.fst ∉ { entries := l, nodupKeys := hl }<GOAL>HEq (⋯.mpr (IH c.fst c.snd { entries := l, nodupKeys := ⋯ } ⋯ (insertRec H0 IH { entries := l, nodupKeys := ⋯ }))) (IH c.fst c.snd { entries := l, nodupKeys := hl } h (insertRec H0 IH { entries := l, nodupKeys := hl }))
<VAR>n : ℕ<VAR>P : ℤ[X]<VAR>h : map (Int.castRingHom ℂ) P = cyclotomic' n ℂ<GOAL>P = cyclotomic n ℤ
<VAR>n : ℕ<VAR>P : ℤ[X]<VAR>h : map (Int.castRingHom ℂ) P = cyclotomic' n ℂ<GOAL>map (Int.castRingHom ℂ) P = map (Int.castRingHom ℂ) (cyclotomic n ℤ)
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>hp : Fact (1 ≤ p)<VAR>inst✝¹ : SeminormedAddCommGroup α<VAR>inst✝ : SeminormedAddCommGroup β<VAR>y : β<GOAL>‖(WithLp.equiv p (α × β)).symm (0, y)‖₊ = ‖y‖₊
<VAR>y : ℝ<GOAL>Continuous fun a => a ^ y
<VAR>y : ℝ<VAR>x : ℝ≥0∞<GOAL>ContinuousAt (fun a => a ^ y) x
<VAR>y : ℝ<VAR>x : ℝ≥0∞<VAR>hy : 0 < y<GOAL>ContinuousAt (fun a => a ^ y) x
<VAR>x : ℝ≥0∞<GOAL>ContinuousAt (fun a => a ^ 0) x
<VAR>y : ℝ<VAR>x : ℝ≥0∞<VAR>hy : y < 0<GOAL>ContinuousAt (fun a => a ^ y) x
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<VAR>n : ℕ<VAR>x : α<VAR>h : ¬p x = true<GOAL>rtakeWhile p (l ++ [x]) = []
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>inst✝² : NormedRing 𝕜<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : BoundedSMul 𝕜 E<VAR>k : 𝕜<VAR>f : ↥(simpleFunc E p μ)<GOAL>↑(toSimpleFunc (k • f)) =ᶠ[ae μ] k • ↑(toSimpleFunc f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>inst✝² : NormedRing 𝕜<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : BoundedSMul 𝕜 E<VAR>k : 𝕜<VAR>f : ↥(simpleFunc E p μ)<VAR>a✝ : α<GOAL>↑(toSimpleFunc (k • f)) a✝ = ↑↑↑(k • f) a✝ → ↑(toSimpleFunc f) a✝ = ↑↑↑f a✝ → ↑↑(k • ↑f) a✝ = (k • ↑↑↑f) a✝ → ↑(toSimpleFunc (k • f)) a✝ = (k • ↑(toSimpleFunc f)) a✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝⁵ : MeasurableSpace α<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>inst✝² : NormedRing 𝕜<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : BoundedSMul 𝕜 E<VAR>k : 𝕜<VAR>f : ↥(simpleFunc E p μ)<VAR>a✝ : α<GOAL>↑(toSimpleFunc (k • f)) a✝ = ↑↑(k • ↑f) a✝ → ↑(toSimpleFunc f) a✝ = ↑↑↑f a✝ → ↑↑(k • ↑f) a✝ = k • ↑↑↑f a✝ → ↑(toSimpleFunc (k • f)) a✝ = k • ↑(toSimpleFunc f) a✝
<GOAL>DifferentiableOn ℝ negMulLog {0}ᶜ