ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>o : Type u_5<VAR>m' : α → Type u_6<VAR>n' : α → Type u_7<VAR>R : Type v<VAR>inst✝⁶ : CommRing R<VAR>M✝ N : Matrix m m R<VAR>b : m → α<VAR>inst✝⁵ : DecidableEq m<VAR>inst✝⁴ : Fintype m<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>M : Matrix m m R<VAR>p q : m → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : DecidablePred q<VAR>e : ∀ (x : m), q x ↔ p x<GOAL>(M.toSquareBlockProp p).det = (M.toSquareBlockProp q).det
<VAR>X : LightCondSet<VAR>S : LightProfinite<VAR>x : X.val.obj (Opposite.op S)<GOAL>∀ (i : (T : LightProfinite) × X.val.obj (Opposite.op T)), Continuous fun a => LightCondSet.coinducingCoprod X ⟨i, a⟩
<VAR>X : LightCondSet<VAR>S : LightProfinite<VAR>x : X.val.obj (Opposite.op S)<GOAL>Continuous (LightCondSet.coinducingCoprod X)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q : ℚ<VAR>hq : q ≠ 0<VAR>k : ℕ<GOAL>padicValRat p (q ^ k) = ↑k * padicValRat p q
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Monoid M<VAR>inst✝ : Nontrivial R<VAR>m : M<VAR>S : Set M<GOAL>(of R M) m ∈ span R (⇑(of R M) '' S) ↔ m ∈ S
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Monoid M<VAR>inst✝ : Nontrivial R<VAR>m : M<VAR>S : Set M<VAR>h : (of R M) m ∈ span R (⇑(of R M) '' S)<GOAL>m ∈ S
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Monoid M<VAR>inst✝ : Nontrivial R<VAR>m : M<VAR>S : Set M<VAR>h : ↑{m} ⊆ S<GOAL>m ∈ S
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>l : Filter α<VAR>f g✝ h : α → β<VAR>lc : Filter γ<VAR>g : γ → α<VAR>hg : Tendsto g lc l<VAR>b : β<VAR>hb : f =ᶠ[l] fun x => b<GOAL>(↑(f ∘ g)).IsConstant
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : NonUnitalNonAssocSemiring A<VAR>inst✝⁷ : Module R A<VAR>inst✝⁶ : IsScalarTower R A A<VAR>inst✝⁵ : SMulCommClass R A A<VAR>inst✝⁴ : NonUnitalNonAssocSemiring B<VAR>inst✝³ : Module R B<VAR>inst✝² : IsScalarTower R B B<VAR>inst✝¹ : SMulCommClass R B B<VAR>S : NonUnitalSubalgebra R A<VAR>ι : Type u_1<VAR>inst✝ : Nonempty ι<VAR>K : ι → NonUnitalSubalgebra R A<VAR>dir : Directed (fun x x_1 => x ≤ x_1) K<VAR>f : (i : ι) → ↥(K i) →ₙₐ[R] B<VAR>hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)<VAR>i : ι<VAR>x : ↥(iSup K)<VAR>hx : ↑x ∈ K i<GOAL>Set.iUnionLift (fun i => ↑(K i)) (fun i x => (f i) x) ⋯ ↑(iSup K) ⋯ x = (f i) ⟨↑x, hx⟩
<VAR>a b d m n : ℤ<VAR>h : b ∣ a<VAR>e : ℤ<GOAL>a ∣ b * (a / b * e)
<VAR>a b d m n : ℤ<VAR>h : b ∣ a<VAR>e : ℤ<GOAL>a ∣ a * e
<VAR>R : Type u_1<VAR>K : 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✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : LieRingModule L M<VAR>inst✝⁵ : LieModule R L M<VAR>inst✝⁴ : Module.Free R M<VAR>inst✝³ : Module.Finite R M<VAR>inst✝² : LieAlgebra.IsNilpotent R L<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : IsPrincipalIdealRing R<VAR>h : LinearMap.ker (traceForm R L M) = ⊥<GOAL>IsLieAbelian L
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>P Q : C<VAR>i : P ≅ Q<VAR>hP : Injective P<VAR>X✝ Y✝ : C<VAR>g : X✝ ⟶ Q<VAR>f : X✝ ⟶ Y✝<VAR>mono : Mono f<GOAL>∃ h, f ≫ h = g
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>P Q : C<VAR>i : P ≅ Q<VAR>hP : Injective P<VAR>X✝ Y✝ : C<VAR>g : X✝ ⟶ Q<VAR>f : X✝ ⟶ Y✝<VAR>mono : Mono f<VAR>h : Y✝ ⟶ P<VAR>h_eq : f ≫ h = g ≫ i.inv<GOAL>∃ h, f ≫ h = g
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>P Q : C<VAR>i : P ≅ Q<VAR>hP : Injective P<VAR>X✝ Y✝ : C<VAR>g : X✝ ⟶ Q<VAR>f : X✝ ⟶ Y✝<VAR>mono : Mono f<VAR>h : Y✝ ⟶ P<VAR>h_eq : f ≫ h = g ≫ i.inv<GOAL>f ≫ h ≫ i.hom = g
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : Ring S<VAR>inst✝¹ : Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>N' : Submodule R S<VAR>h : N' ≤ N<VAR>inst✝ : Module.Flat R ↥M<VAR>i : ↥M ⊗[R] ↥N' →ₗ[R] S := M.mulMap N ∘ₗ LinearMap.lTensor (↥M) (inclusion h)<GOAL>M.LinearDisjoint N'
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : Ring S<VAR>inst✝¹ : Algebra R S<VAR>M N : Submodule R S<VAR>H : M.LinearDisjoint N<VAR>N' : Submodule R S<VAR>h : N' ≤ N<VAR>inst✝ : Module.Flat R ↥M<VAR>i : ↥M ⊗[R] ↥N' →ₗ[R] S := M.mulMap N ∘ₗ LinearMap.lTensor (↥M) (inclusion h)<VAR>hi : Function.Injective ⇑i<GOAL>M.LinearDisjoint N'
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℕ<GOAL>↑(WeierstrassCurve.expCoeff n) = if Even n then ↑n / 2 else ↑n
<VAR>ι : Type u_1<VAR>I J✝ J₁ J₂ : Box ι<VAR>π π₁ π₂ : Prepartition I<VAR>x : ι → ℝ<VAR>πi πi₁ πi₂ : (J : Box ι) → Prepartition J<VAR>boxes : Finset (WithBot (Box ι))<VAR>le_of_mem : ∀ J ∈ boxes, J ≤ ↑I<VAR>pairwise_disjoint : (↑boxes).Pairwise Disjoint<VAR>H : ∀ J ∈ π, ∃ J' ∈ boxes, ↑J ≤ J'<VAR>J : Box ι<VAR>hJ : J ∈ π<VAR>J' : WithBot (Box ι)<VAR>J'mem : J' ∈ boxes<VAR>hle : ↑J ≤ J'<GOAL>∃ I' ∈ ofWithBot boxes le_of_mem pairwise_disjoint, J ≤ I'
<VAR>ι : Type u_1<VAR>I J✝ J₁ J₂ : Box ι<VAR>π π₁ π₂ : Prepartition I<VAR>x : ι → ℝ<VAR>πi πi₁ πi₂ : (J : Box ι) → Prepartition J<VAR>boxes : Finset (WithBot (Box ι))<VAR>le_of_mem : ∀ J ∈ boxes, J ≤ ↑I<VAR>pairwise_disjoint : (↑boxes).Pairwise Disjoint<VAR>H : ∀ J ∈ π, ∃ J' ∈ boxes, ↑J ≤ J'<VAR>J : Box ι<VAR>hJ : J ∈ π<VAR>J' : Box ι<VAR>J'mem : ↑J' ∈ boxes<VAR>hle : ↑J ≤ ↑J'<GOAL>∃ I' ∈ ofWithBot boxes le_of_mem pairwise_disjoint, J ≤ I'
<VAR>ι : Type u_1<VAR>α✝ : Type u_2<VAR>β✝ : Type u_3<VAR>γ : Type u_4<VAR>𝕜 : Type u_5<VAR>R : Type u_6<VAR>M : Type u_7<VAR>N : Type u_8<VAR>α : Type u_9<VAR>β : Type u_10<VAR>inst✝⁵ : DivisionSemiring α<VAR>inst✝⁴ : NeZero 2<VAR>inst✝³ : Lattice β<VAR>inst✝² : AddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : CovariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>x y : β<GOAL>x ⊔ y = 2⁻¹ • (x + y + |y - x|)
<VAR>ι : Type u_1<VAR>α✝ : Type u_2<VAR>β✝ : Type u_3<VAR>γ : Type u_4<VAR>𝕜 : Type u_5<VAR>R : Type u_6<VAR>M : Type u_7<VAR>N : Type u_8<VAR>α : Type u_9<VAR>β : Type u_10<VAR>inst✝⁵ : DivisionSemiring α<VAR>inst✝⁴ : NeZero 2<VAR>inst✝³ : Lattice β<VAR>inst✝² : AddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : CovariantClass β β (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>x y : β<VAR>this : Invertible 2 := invertibleOfNonzero ⋯<GOAL>x ⊔ y = 2⁻¹ • (x + y + |y - x|)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : TopologicalSpace α<VAR>t : Set α<VAR>a : α<VAR>s : Set α<GOAL>t ∈ 𝓝[s] a ↔ ∃ u, IsOpen u ∧ a ∈ u ∧ u ∩ s ⊆ t
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>K : Type u_4<VAR>K₂ : Type u_5<VAR>M : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>V : Type u_9<VAR>V₂ : Type u_10<VAR>inst✝¹³ : Semiring R<VAR>inst✝¹² : Semiring R₂<VAR>inst✝¹¹ : Semiring R₃<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : AddCommMonoid M₂<VAR>inst✝⁸ : AddCommMonoid M₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>inst✝⁷ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R₂ M₂<VAR>inst✝⁴ : Module R₃ M₃<VAR>σ₂₁ : R₂ →+* R<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₃ : R₂ →+* R₃<VAR>τ₁₃ : R →+* R₃<VAR>inst✝³ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃<VAR>F : Type u_11<VAR>inst✝² : FunLike F M M₂<VAR>inst✝¹ : SemilinearMapClass F τ₁₂ M M₂<VAR>inst✝ : RingHomSurjective τ₁₂<VAR>f : F<VAR>q : Submodule R₂ M₂<VAR>h : q ≤ range f<GOAL>map f (comap f q) = q
<VAR>k : Type u_1<VAR>inst✝⁸ : Field k<VAR>K : Type u_2<VAR>inst✝⁷ : Field K<VAR>F : Type u_3<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : NumberField K<VAR>inst✝⁴ : Algebra k K<VAR>inst✝³ : Algebra k F<VAR>inst✝² : Algebra K F<VAR>inst✝¹ : IsScalarTower k K F<VAR>σ : K ≃ₐ[k] K<VAR>w : InfinitePlace K<VAR>inst✝ : IsGalois k K<GOAL>IsUnramified k w ↔ Nat.card ↥(Stab w) = 1
<VAR>p a b : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>h : b ∣ a<GOAL>padicValNat p (a / b) = padicValNat p a - padicValNat p b
<VAR>p b : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>h : b ∣ 0<GOAL>padicValNat p (0 / b) = padicValNat p 0 - padicValNat p b
<VAR>p a b : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>h : b ∣ a<VAR>ha : a ≠ 0<GOAL>padicValNat p (a / b) = padicValNat p a - padicValNat p b
<VAR>p b : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : ℕ<VAR>ha : b * k ≠ 0<GOAL>padicValNat p (b * k / b) = padicValNat p (b * k) - padicValNat p b
<VAR>p b : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>k : ℕ<VAR>ha : b * k ≠ 0<VAR>hb : b ≠ 0<VAR>hk : k ≠ 0<GOAL>padicValNat p (b * k / b) = padicValNat p (b * k) - padicValNat p b
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>ℰ : Type u₂<VAR>inst✝³ : Category.{v₁, u₂} ℰ<VAR>A✝ A : C ⥤ ℰ<VAR>inst✝² : yoneda.HasPointwiseLeftKanExtension A<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₁, u₂} D<VAR>F : C ⥤ D<VAR>inst✝ : ∀ (P : Cᵒᵖ ⥤ Type v₁), F.op.HasLeftKanExtension P<VAR>X✝ : C<VAR>G : (Cᵒᵖ ⥤ Type v₁) ⥤ Dᵒᵖ ⥤ Type v₁<VAR>φ : F ⋙ yoneda ⟶ yoneda ⋙ G<VAR>P : Cᵒᵖ ⥤ Type v₁<VAR>X : C<VAR>f : yoneda.obj X ⟶ P<GOAL>yonedaEquiv (f ≫ presheafHom φ P) = (G.map f).app (Opposite.op (F.obj X)) ((φ.app X).app (Opposite.op (F.obj X)) (𝟙 (Opposite.unop (Opposite.op (F.obj X)))))
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>ℰ : Type u₂<VAR>inst✝³ : Category.{v₁, u₂} ℰ<VAR>A✝ A : C ⥤ ℰ<VAR>inst✝² : yoneda.HasPointwiseLeftKanExtension A<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₁, u₂} D<VAR>F : C ⥤ D<VAR>inst✝ : ∀ (P : Cᵒᵖ ⥤ Type v₁), F.op.HasLeftKanExtension P<VAR>X✝ : C<VAR>G : (Cᵒᵖ ⥤ Type v₁) ⥤ Dᵒᵖ ⥤ Type v₁<VAR>φ : F ⋙ yoneda ⟶ yoneda ⋙ G<VAR>P : Cᵒᵖ ⥤ Type v₁<VAR>X : C<VAR>x : P.obj (Opposite.op X)<GOAL>yonedaEquiv (yonedaEquiv.symm x ≫ presheafHom φ P) = (G.map (yonedaEquiv.symm x)).app (Opposite.op (F.obj X)) ((φ.app X).app (Opposite.op (F.obj X)) (𝟙 (Opposite.unop (Opposite.op (F.obj X)))))
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>ℰ : Type u₂<VAR>inst✝³ : Category.{v₁, u₂} ℰ<VAR>A✝ A : C ⥤ ℰ<VAR>inst✝² : yoneda.HasPointwiseLeftKanExtension A<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₁, u₂} D<VAR>F : C ⥤ D<VAR>inst✝ : ∀ (P : Cᵒᵖ ⥤ Type v₁), F.op.HasLeftKanExtension P<VAR>X✝ : C<VAR>G : (Cᵒᵖ ⥤ Type v₁) ⥤ Dᵒᵖ ⥤ Type v₁<VAR>φ : F ⋙ yoneda ⟶ yoneda ⋙ G<VAR>P : Cᵒᵖ ⥤ Type v₁<VAR>X : C<VAR>x : P.obj (Opposite.op X)<GOAL>yonedaEquiv ({ pt := { obj := fun X => (G.obj P).obj (F.op.obj X), map := fun {X Y} f => (G.obj P).map (F.op.map f), map_id := ⋯, map_comp := ⋯ }, ι := { app := fun x => coconeApp φ (Opposite.unop x), naturality := ⋯ } }.ι.app (Opposite.op (P.elementsMk (Opposite.op X) x))) = (G.map (yonedaEquiv.symm x)).app (Opposite.op (F.obj X)) ((φ.app X).app (Opposite.op (F.obj X)) (𝟙 (Opposite.unop (Opposite.op (F.obj X)))))
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>ℰ : Type u₂<VAR>inst✝³ : Category.{v₁, u₂} ℰ<VAR>A✝ A : C ⥤ ℰ<VAR>inst✝² : yoneda.HasPointwiseLeftKanExtension A<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₁, u₂} D<VAR>F : C ⥤ D<VAR>inst✝ : ∀ (P : Cᵒᵖ ⥤ Type v₁), F.op.HasLeftKanExtension P<VAR>X✝ : C<VAR>G : (Cᵒᵖ ⥤ Type v₁) ⥤ Dᵒᵖ ⥤ Type v₁<VAR>φ : F ⋙ yoneda ⟶ yoneda ⋙ G<VAR>P : Cᵒᵖ ⥤ Type v₁<VAR>X : C<VAR>x : P.obj (Opposite.op X)<GOAL>yonedaEquiv (yonedaEquiv.symm ((G.map (yonedaEquiv.symm x)).app (F.op.obj (Opposite.op X)) ((φ.app X).app (F.op.obj (Opposite.op X)) (𝟙 (Opposite.unop (F.op.obj (Opposite.op X))))))) = (G.map (yonedaEquiv.symm x)).app (Opposite.op (F.obj X)) ((φ.app X).app (Opposite.op (F.obj X)) (𝟙 (F.obj X)))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>op : α → α → α<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>inst✝ : DecidableEq α<VAR>hi : Std.IdempotentOp op<VAR>s✝ : Multiset α<VAR>b a : α<VAR>s : Multiset α<VAR>IH : fold op b s.dedup = fold op b s<VAR>h : a ∈ s<GOAL>fold op b s = op a (fold op b s)
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>R : Type u_4<VAR>α : Type u_5<VAR>inst✝⁴ : DecidableEq l<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Semiring α<VAR>inst✝ : SMulZeroClass R α<VAR>r : R<VAR>i : m<VAR>j : n<VAR>a : α<VAR>i✝ : m<VAR>j✝ : n<GOAL>(r • fun i' j' => if i = i' ∧ j = j' then a else 0) i✝ j✝ = if i = i✝ ∧ j = j✝ then r • a else 0
<VAR>n m : ℕ<VAR>a b c : Fin n<GOAL>a ≤ b → a = b ∨ a < b
<VAR>n m : ℕ<VAR>a b c : Fin n<GOAL>a ≤ b → ↑a = ↑b ∨ a < b
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>P✝ : Sylow p G<VAR>K : Type u_2<VAR>inst✝ : Group K<VAR>ϕ : K →* G<VAR>N : Subgroup G<VAR>P Q : Sylow p G<VAR>hP : ↑P ≤ N<VAR>hQ : ↑Q ≤ N<VAR>h : P.subtype hP = Q.subtype hQ<GOAL>P = Q
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>P✝ : Sylow p G<VAR>K : Type u_2<VAR>inst✝ : Group K<VAR>ϕ : K →* G<VAR>N : Subgroup G<VAR>P Q : Sylow p G<VAR>hP : ↑P ≤ N<VAR>hQ : ↑Q ≤ N<VAR>h : ∀ (x : ↥N), x ∈ P.subtype hP ↔ x ∈ Q.subtype hQ<GOAL>∀ (x : G), x ∈ P ↔ x ∈ Q
<VAR>n : ℕ<VAR>K : Type u_1<VAR>inst✝² : CommRing K<VAR>μ : K<VAR>h : IsPrimitiveRoot μ n<VAR>inst✝¹ : IsDomain K<VAR>inst✝ : CharZero K<VAR>p : ℕ<VAR>hdiv : ¬p ∣ n<GOAL>minpoly ℤ μ ∣ (expand ℤ p) (minpoly ℤ (μ ^ p))
<VAR>K : Type u_1<VAR>inst✝² : CommRing K<VAR>μ : K<VAR>inst✝¹ : IsDomain K<VAR>inst✝ : CharZero K<VAR>p : ℕ<VAR>h : IsPrimitiveRoot μ 0<VAR>hdiv : ¬p ∣ 0<GOAL>minpoly ℤ μ ∣ (expand ℤ p) (minpoly ℤ (μ ^ p))
<VAR>n : ℕ<VAR>K : Type u_1<VAR>inst✝² : CommRing K<VAR>μ : K<VAR>h : IsPrimitiveRoot μ n<VAR>inst✝¹ : IsDomain K<VAR>inst✝ : CharZero K<VAR>p : ℕ<VAR>hdiv : ¬p ∣ n<VAR>hpos : n > 0<GOAL>minpoly ℤ μ ∣ (expand ℤ p) (minpoly ℤ (μ ^ p))
<VAR>n : ℕ<VAR>K : Type u_1<VAR>inst✝² : CommRing K<VAR>μ : K<VAR>h : IsPrimitiveRoot μ n<VAR>inst✝¹ : IsDomain K<VAR>inst✝ : CharZero K<VAR>p : ℕ<VAR>hdiv : ¬p ∣ n<VAR>hpos : n > 0<VAR>this : IsIntegrallyClosed ℤ := GCDMonoid.toIsIntegrallyClosed<GOAL>minpoly ℤ μ ∣ (expand ℤ p) (minpoly ℤ (μ ^ p))
<VAR>n : ℕ<VAR>K : Type u_1<VAR>inst✝² : CommRing K<VAR>μ : K<VAR>h : IsPrimitiveRoot μ n<VAR>inst✝¹ : IsDomain K<VAR>inst✝ : CharZero K<VAR>p : ℕ<VAR>hdiv : ¬p ∣ n<VAR>hpos : n > 0<VAR>this : IsIntegrallyClosed ℤ := GCDMonoid.toIsIntegrallyClosed<GOAL>(Polynomial.aeval μ) ((expand ℤ p) (minpoly ℤ (μ ^ p))) = 0
<VAR>n : ℕ<VAR>K : Type u_1<VAR>inst✝² : CommRing K<VAR>μ : K<VAR>h : IsPrimitiveRoot μ n<VAR>inst✝¹ : IsDomain K<VAR>inst✝ : CharZero K<VAR>p : ℕ<VAR>hdiv : ¬p ∣ n<VAR>hpos : n > 0<VAR>this : IsIntegrallyClosed ℤ := GCDMonoid.toIsIntegrallyClosed<GOAL>(Polynomial.aeval (μ ^ p)) (minpoly ℤ (μ ^ p)) = 0
<VAR>α : Type u<VAR>inst✝ : OmegaCompletePartialOrder α<VAR>s : Set (Set α)<VAR>hs : ∀ t ∈ s, Continuous' fun x => x ∈ t<GOAL>Continuous' fun x => x ∈ ⋃₀ s
<VAR>α : Type u<VAR>inst✝ : OmegaCompletePartialOrder α<VAR>s : Set (Set α)<VAR>hs : ∀ t ∈ s, Continuous' fun x => x ∈ t<VAR>x✝ : α<GOAL>x✝ ∈ ⋃₀ s ↔ sSup (setOf ⁻¹' s) x✝
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s t : Set α<VAR>inst✝ : Infinite α<VAR>hs : s.Finite<GOAL>∃ a, a ∉ s
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>s t : Set α<VAR>inst✝ : Infinite α<VAR>hs : s.Finite<VAR>h : ∀ (a : α), a ∈ s<GOAL>False
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<VAR>f : R →+* S<GOAL>(W.map f).Ψ₂Sq = Polynomial.map f W.Ψ₂Sq
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<VAR>f : R →+* S<GOAL>C 4 * X ^ 3 + C (f W.b₂) * X ^ 2 + C (2 * f W.b₄) * X + C (f W.b₆) = Polynomial.map f (C 4 * X ^ 3 + C W.b₂ * X ^ 2 + C (2 * W.b₄) * X + C W.b₆)
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝¹¹ : Nonempty ι<VAR>inst✝¹⁰ : Nonempty ι'<VAR>inst✝⁹ : NormedField 𝕜<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module 𝕜 E<VAR>inst✝⁶ : NormedField 𝕜₂<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : Module 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝³ : RingHomIsometric σ₁₂<VAR>inst✝² : Preorder ι<VAR>inst✝¹ : LocallyFiniteOrderBot ι<VAR>p : SeminormFamily 𝕜 E ι<VAR>inst✝ : TopologicalSpace E<VAR>hp : WithSeminorms p<GOAL>WithSeminorms fun i => (Finset.Iic i).sup p
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝¹¹ : Nonempty ι<VAR>inst✝¹⁰ : Nonempty ι'<VAR>inst✝⁹ : NormedField 𝕜<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module 𝕜 E<VAR>inst✝⁶ : NormedField 𝕜₂<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : Module 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝³ : RingHomIsometric σ₁₂<VAR>inst✝² : Preorder ι<VAR>inst✝¹ : LocallyFiniteOrderBot ι<VAR>p : SeminormFamily 𝕜 E ι<VAR>inst✝ : TopologicalSpace E<VAR>hp : WithSeminorms p<GOAL>Seminorm.IsBounded p (fun i => (Finset.Iic i).sup p) LinearMap.id
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝¹¹ : Nonempty ι<VAR>inst✝¹⁰ : Nonempty ι'<VAR>inst✝⁹ : NormedField 𝕜<VAR>inst✝⁸ : AddCommGroup E<VAR>inst✝⁷ : Module 𝕜 E<VAR>inst✝⁶ : NormedField 𝕜₂<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : Module 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝³ : RingHomIsometric σ₁₂<VAR>inst✝² : Preorder ι<VAR>inst✝¹ : LocallyFiniteOrderBot ι<VAR>p : SeminormFamily 𝕜 E ι<VAR>inst✝ : TopologicalSpace E<VAR>hp : WithSeminorms p<GOAL>Seminorm.IsBounded (fun i => (Finset.Iic i).sup p) p LinearMap.id
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : CommSemiring A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>I : Ideal B<VAR>hI : I ^ 2 = ⊥<VAR>inst✝¹ : Algebra A B<VAR>inst✝ : IsScalarTower R A B<VAR>d : Derivation R A ↥I<VAR>x : A<GOAL>(Ideal.Quotient.mk I) ((liftOfDerivationToSquareZero I hI d) x) = (algebraMap A (B ⧸ I)) x
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : CommSemiring A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>I : Ideal B<VAR>hI : I ^ 2 = ⊥<VAR>inst✝¹ : Algebra A B<VAR>inst✝ : IsScalarTower R A B<VAR>d : Derivation R A ↥I<VAR>x : A<GOAL>(Ideal.Quotient.mk I) ((algebraMap A B) x) = (algebraMap A (B ⧸ I)) x
<VAR>cs cs' : List Char<GOAL>{ data := cs ++ cs' }.atEnd { byteIdx := utf8Len cs } = true ↔ cs' = []
<VAR>cs cs' : List Char<GOAL>{ data := cs ++ cs' }.endPos ≤ { byteIdx := utf8Len cs } ↔ cs' = []
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : SemilatticeInf α<VAR>b c : α<VAR>inst✝ : OrderTop α<VAR>s : Finset ι<VAR>f : ι → α<VAR>ha : InfPrime ⊤<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ε : Type u_5<VAR>ι : Type u_6<VAR>f : α → β<VAR>s : Set α<VAR>a : α<VAR>b : β<GOAL>b ∈ res f s a ↔ a ∈ s ∧ f a = b
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasZeroObject C<VAR>inst✝ : HasZeroMorphisms C<VAR>Z : C<VAR>P : ProjectiveResolution Z<VAR>n : ℕ<GOAL>ExactAt P.complex (n + 1)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasZeroObject C<VAR>inst✝ : HasZeroMorphisms C<VAR>Z : C<VAR>P : ProjectiveResolution Z<VAR>n : ℕ<GOAL>QuasiIsoAt P.π (n + 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>α₁ : Type u_6<VAR>α₂ : Type u_7<VAR>β₁ : Type u_8<VAR>β₂ : Type u_9<VAR>s₁ : Set α₁<VAR>s₂ : Set α₂<VAR>t₁ : Set β₁<VAR>t₂ : Set β₂<VAR>f₁ : α₁ → β₁<VAR>f₂ : α₂ → β₂<VAR>g₁ : β₁ → α₁<VAR>g₂ : β₂ → α₂<VAR>h₁ : SurjOn f₁ s₁ t₁<VAR>h₂ : SurjOn f₂ s₂ t₂<VAR>x : β₁ × β₂<VAR>hx : x ∈ t₁ ×ˢ t₂<GOAL>x ∈ (fun x => (f₁ x.1, f₂ x.2)) '' s₁ ×ˢ s₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>α₁ : Type u_6<VAR>α₂ : Type u_7<VAR>β₁ : Type u_8<VAR>β₂ : Type u_9<VAR>s₁ : Set α₁<VAR>s₂ : Set α₂<VAR>t₁ : Set β₁<VAR>t₂ : Set β₂<VAR>f₁ : α₁ → β₁<VAR>f₂ : α₂ → β₂<VAR>g₁ : β₁ → α₁<VAR>g₂ : β₂ → α₂<VAR>h₁ : SurjOn f₁ s₁ t₁<VAR>h₂ : SurjOn f₂ s₂ t₂<VAR>x : β₁ × β₂<VAR>hx : x ∈ t₁ ×ˢ t₂<VAR>a₁ : α₁<VAR>ha₁ : a₁ ∈ s₁<VAR>hx₁ : f₁ a₁ = x.1<GOAL>x ∈ (fun x => (f₁ x.1, f₂ x.2)) '' s₁ ×ˢ s₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>α₁ : Type u_6<VAR>α₂ : Type u_7<VAR>β₁ : Type u_8<VAR>β₂ : Type u_9<VAR>s₁ : Set α₁<VAR>s₂ : Set α₂<VAR>t₁ : Set β₁<VAR>t₂ : Set β₂<VAR>f₁ : α₁ → β₁<VAR>f₂ : α₂ → β₂<VAR>g₁ : β₁ → α₁<VAR>g₂ : β₂ → α₂<VAR>h₁ : SurjOn f₁ s₁ t₁<VAR>h₂ : SurjOn f₂ s₂ t₂<VAR>x : β₁ × β₂<VAR>hx : x ∈ t₁ ×ˢ t₂<VAR>a₁ : α₁<VAR>ha₁ : a₁ ∈ s₁<VAR>hx₁ : f₁ a₁ = x.1<VAR>a₂ : α₂<VAR>ha₂ : a₂ ∈ s₂<VAR>hx₂ : f₂ a₂ = x.2<GOAL>x ∈ (fun x => (f₁ x.1, f₂ x.2)) '' s₁ ×ˢ s₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>t : α<VAR>ts is : List α<VAR>IH1 : map (map f) (ts.permutationsAux (t :: is)) = (map f ts).permutationsAux (map f (t :: is))<VAR>IH2 : map (map f) (is.permutationsAux []) = (map f is).permutationsAux []<GOAL>map (map f) ((t :: ts).permutationsAux is) = (map f (t :: ts)).permutationsAux (map f is)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x y : R<VAR>inst✝ : Ring R<VAR>r u : R<VAR>hnil : IsNilpotent r<VAR>hu : IsUnit u<VAR>h_comm : Commute r u<GOAL>IsUnit (u + r)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x y : R<VAR>inst✝ : Ring R<VAR>r u : R<VAR>hnil : IsNilpotent r<VAR>hu : IsUnit u<VAR>h_comm : Commute r u<GOAL>IsUnit (1 + r * ↑hu.unit⁻¹)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x y : R<VAR>inst✝ : Ring R<VAR>r u : R<VAR>hnil : IsNilpotent r<VAR>hu : IsUnit u<VAR>h_comm : Commute r ↑hu.unit⁻¹<GOAL>IsUnit (1 + r * ↑hu.unit⁻¹)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x y : R<VAR>inst✝ : Ring R<VAR>r u : R<VAR>hnil : IsNilpotent r<VAR>hu : IsUnit u<VAR>h_comm : Commute r ↑hu.unit⁻¹<GOAL>IsNilpotent (r * ↑hu.unit⁻¹)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>G : SimpleGraph α<VAR>H : SimpleGraph β<VAR>x : α × β<VAR>a' : α<VAR>b' : β<GOAL>(a', b') ∈ (G □ H).neighborSet x ↔ (a', b') ∈ G.neighborSet x.1 ×ˢ {x.2} ∪ {x.1} ×ˢ H.neighborSet x.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>G : SimpleGraph α<VAR>H : SimpleGraph β<VAR>x : α × β<VAR>a' : α<VAR>b' : β<GOAL>G.Adj x.1 a' ∧ x.2 = b' ∨ H.Adj x.2 b' ∧ x.1 = a' ↔ G.Adj x.1 a' ∧ b' = x.2 ∨ a' = x.1 ∧ H.Adj x.2 b'
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝⁴ : LinearOrderedRing α<VAR>inst✝³ : LinearOrderedAddCommGroup β<VAR>inst✝² : Module α β<VAR>inst✝¹ : OrderedSMul α β<VAR>s : Finset ι<VAR>σ : Perm ι<VAR>f : ι → α<VAR>g : ι → β<VAR>inst✝ : Fintype ι<VAR>hfg : Monovary f g<GOAL>∑ i : ι, f (σ i) • g i < ∑ i : ι, f i • g i ↔ ¬Monovary (f ∘ ⇑σ) g
<VAR>α : Type u_1<VAR>x : α<VAR>l : List α<VAR>n : Nat<VAR>h : n < l.length<GOAL>l[n] = x ↔ l[n]? = some x
<VAR>α : Type u_1<VAR>x : α<VAR>l : List α<VAR>n : Nat<VAR>h : n < l.length<GOAL>l[n] = x ↔ ∃ h, l[n] = x
<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>F : J ⥤ MonCatMax<VAR>inst✝ : IsFiltered J<VAR>j₁ : J<VAR>y : ↑(F.obj j₁)<VAR>j₂ : J<VAR>x : ↑(F.obj j₂)<VAR>j₃ : J<VAR>y' : ↑(F.obj j₃)<VAR>l : J<VAR>f : ⟨j₁, y⟩.fst ⟶ l<VAR>g : ⟨j₃, y'⟩.fst ⟶ l<VAR>hfg : (F ⋙ forget MonCat).map f ⟨j₁, y⟩.snd = (F ⋙ forget MonCat).map g ⟨j₃, y'⟩.snd<GOAL>colimitMulAux F ⟨j₂, x⟩ ⟨j₁, y⟩ = colimitMulAux F ⟨j₂, x⟩ ⟨j₃, y'⟩
<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>F : J ⥤ MonCatMax<VAR>inst✝ : IsFiltered J<VAR>j₁ : J<VAR>y : ↑(F.obj j₁)<VAR>j₂ : J<VAR>x : ↑(F.obj j₂)<VAR>j₃ : J<VAR>y' : ↑(F.obj j₃)<VAR>l : J<VAR>f : ⟨j₁, y⟩.fst ⟶ l<VAR>g : ⟨j₃, y'⟩.fst ⟶ l<VAR>hfg : (F.map f) y = (F.map g) y'<GOAL>colimitMulAux F ⟨j₂, x⟩ ⟨j₁, y⟩ = colimitMulAux F ⟨j₂, x⟩ ⟨j₃, y'⟩
<VAR>J : Type v<VAR>inst✝¹ : SmallCategory J<VAR>F : J ⥤ MonCatMax<VAR>inst✝ : IsFiltered J<VAR>j₁ : J<VAR>y : ↑(F.obj j₁)<VAR>j₂ : J<VAR>x : ↑(F.obj j₂)<VAR>j₃ : J<VAR>y' : ↑(F.obj j₃)<VAR>l : J<VAR>f : ⟨j₁, y⟩.fst ⟶ l<VAR>g : ⟨j₃, y'⟩.fst ⟶ l<VAR>hfg : (F.map f) y = (F.map g) y'<VAR>s : J<VAR>α : IsFiltered.max j₂ j₁ ⟶ s<VAR>β : l ⟶ s<VAR>γ : IsFiltered.max j₂ j₃ ⟶ s<VAR>h₁ : IsFiltered.rightToMax j₂ j₁ ≫ α = f ≫ β<VAR>h₂ : IsFiltered.leftToMax j₂ j₁ ≫ α = IsFiltered.leftToMax j₂ j₃ ≫ γ<VAR>h₃ : IsFiltered.rightToMax j₂ j₃ ≫ γ = g ≫ β<GOAL>colimitMulAux F ⟨j₂, x⟩ ⟨j₁, y⟩ = colimitMulAux F ⟨j₂, x⟩ ⟨j₃, y'⟩