ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>inst✝⁶ : HasZeroMorphisms C<VAR>inst✝⁵ : HasZeroMorphisms D<VAR>S : ShortComplex C<VAR>h₁✝ : S.LeftHomologyData<VAR>h₂✝ : S.RightHomologyData<VAR>F✝ : C ⥤ D<VAR>inst✝⁴ : F✝.PreservesZeroMorphisms<VAR>hl : S.LeftHomologyData<VAR>hr : S.RightHomologyData<VAR>S₁ S₂ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>hl₁ : S₁.LeftHomologyData<VAR>hr₁ : S₁.RightHomologyData<VAR>hl₂ : S₂.LeftHomologyData<VAR>hr₂ : S₂.RightHomologyData<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>F : C ⥤ D<VAR>inst✝³ : F.PreservesZeroMorphisms<VAR>inst✝² : S.HasHomology<VAR>inst✝¹ : F.PreservesLeftHomologyOf S<VAR>inst✝ : F.PreservesRightHomologyOf S<VAR>γ : HomologyMapData (𝟙 (S.map F)) (S.map F).homologyData (S.homologyData.map F)<VAR>eq : γ.left.φH ≫ (S.homologyData.map F).iso.hom = (S.map F).homologyData.iso.hom ≫ γ.right.φH<GOAL>(S.map F).homologyData.iso.hom ≫ rightHomologyMap' (𝟙 (S.map F)) (S.map F).homologyData.right (S.homologyData.right.map F) ≫ F.map S.homologyData.iso.inv = leftHomologyMap' (𝟙 (S.map F)) (S.map F).homologyData.left (S.homologyData.left.map F)
<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>inst✝⁶ : HasZeroMorphisms C<VAR>inst✝⁵ : HasZeroMorphisms D<VAR>S : ShortComplex C<VAR>h₁✝ : S.LeftHomologyData<VAR>h₂✝ : S.RightHomologyData<VAR>F✝ : C ⥤ D<VAR>inst✝⁴ : F✝.PreservesZeroMorphisms<VAR>hl : S.LeftHomologyData<VAR>hr : S.RightHomologyData<VAR>S₁ S₂ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>hl₁ : S₁.LeftHomologyData<VAR>hr₁ : S₁.RightHomologyData<VAR>hl₂ : S₂.LeftHomologyData<VAR>hr₂ : S₂.RightHomologyData<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>F : C ⥤ D<VAR>inst✝³ : F.PreservesZeroMorphisms<VAR>inst✝² : S.HasHomology<VAR>inst✝¹ : F.PreservesLeftHomologyOf S<VAR>inst✝ : F.PreservesRightHomologyOf S<VAR>γ : HomologyMapData (𝟙 (S.map F)) (S.map F).homologyData (S.homologyData.map F)<VAR>eq : leftHomologyMap' (𝟙 (S.map F)) (S.map F).homologyData.left (S.homologyData.map F).left ≫ (S.homologyData.map F).iso.hom = (S.map F).homologyData.iso.hom ≫ rightHomologyMap' (𝟙 (S.map F)) (S.map F).homologyData.right (S.homologyData.map F).right<GOAL>(S.map F).homologyData.iso.hom ≫ rightHomologyMap' (𝟙 (S.map F)) (S.map F).homologyData.right (S.homologyData.right.map F) ≫ F.map S.homologyData.iso.inv = leftHomologyMap' (𝟙 (S.map F)) (S.map F).homologyData.left (S.homologyData.left.map F)
<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>inst✝⁶ : HasZeroMorphisms C<VAR>inst✝⁵ : HasZeroMorphisms D<VAR>S : ShortComplex C<VAR>h₁✝ : S.LeftHomologyData<VAR>h₂✝ : S.RightHomologyData<VAR>F✝ : C ⥤ D<VAR>inst✝⁴ : F✝.PreservesZeroMorphisms<VAR>hl : S.LeftHomologyData<VAR>hr : S.RightHomologyData<VAR>S₁ S₂ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>hl₁ : S₁.LeftHomologyData<VAR>hr₁ : S₁.RightHomologyData<VAR>hl₂ : S₂.LeftHomologyData<VAR>hr₂ : S₂.RightHomologyData<VAR>h₁ : S₁.HomologyData<VAR>h₂ : S₂.HomologyData<VAR>F : C ⥤ D<VAR>inst✝³ : F.PreservesZeroMorphisms<VAR>inst✝² : S.HasHomology<VAR>inst✝¹ : F.PreservesLeftHomologyOf S<VAR>inst✝ : F.PreservesRightHomologyOf S<VAR>γ : HomologyMapData (𝟙 (S.map F)) (S.map F).homologyData (S.homologyData.map F)<VAR>eq : leftHomologyMap' (𝟙 (S.map F)) (S.map F).homologyData.left (S.homologyData.left.map F) ≫ F.map S.homologyData.iso.hom = (S.map F).homologyData.iso.hom ≫ rightHomologyMap' (𝟙 (S.map F)) (S.map F).homologyData.right (S.homologyData.right.map F)<GOAL>(S.map F).homologyData.iso.hom ≫ rightHomologyMap' (𝟙 (S.map F)) (S.map F).homologyData.right (S.homologyData.right.map F) ≫ F.map S.homologyData.iso.inv = leftHomologyMap' (𝟙 (S.map F)) (S.map F).homologyData.left (S.homologyData.left.map F)
<VAR>n : ℕ<VAR>n_big : 4 ≤ n<GOAL>4 ^ n < n * n.centralBinom
<VAR>n : ℕ<VAR>IH : ∀ m < n, 4 ≤ m → 4 ^ m < m * m.centralBinom<VAR>n_big : 4 ≤ n<GOAL>4 ^ n < n * n.centralBinom
<VAR>n : ℕ<VAR>IH : ∀ m < n, 4 ≤ m → 4 ^ m < m * m.centralBinom<VAR>n_big : 4 ≤ n<VAR>hn : n < 4<GOAL>4 ^ n < n * n.centralBinom
<VAR>IH : ∀ m < 4, 4 ≤ m → 4 ^ m < m * m.centralBinom<VAR>n_big : 4 ≤ 4<GOAL>4 ^ 4 < 4 * centralBinom 4
<VAR>n : ℕ<VAR>IH : ∀ m < n, 4 ≤ m → 4 ^ m < m * m.centralBinom<VAR>n_big : 4 ≤ n<VAR>hn : 4 < n<GOAL>4 ^ n < n * n.centralBinom
<VAR>n : ℕ<VAR>IH : ∀ m < n + 1, 4 ≤ m → 4 ^ m < m * m.centralBinom<VAR>n_big : 4 ≤ n + 1<VAR>hn : 4 < n + 1<GOAL>4 ^ (n + 1) < (n + 1) * (n + 1).centralBinom
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b c : α<VAR>n : ℤ<VAR>a : α<GOAL>toIcoMod hp a (a + p) = a
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b c : α<VAR>n : ℤ<VAR>a : α<GOAL>a < a + p ∧ ∃ z, a + p = a + z • p
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a✝ b : R<VAR>n✝ : ℕ<VAR>inst✝³ : Field R<VAR>p q : R[X]<VAR>inst✝² : CommRing S<VAR>inst✝¹ : IsDomain S<VAR>inst✝ : Algebra R S<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>a : R<VAR>ha : a ≠ 0<GOAL>((monomial n) a).rootSet S = {0}
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>f✝ f₀ f₁ g : 𝕜 → F<VAR>f'✝ f₀' f₁' g' : F<VAR>x✝ : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>𝕜' : Type u_1<VAR>inst✝³ : NontriviallyNormedField 𝕜'<VAR>inst✝² : NormedAlgebra 𝕜 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>inst✝ : IsScalarTower 𝕜 𝕜' F<VAR>s' t' : Set 𝕜'<VAR>h : 𝕜 → 𝕜'<VAR>h₁ : 𝕜 → 𝕜<VAR>h₂ : 𝕜' → 𝕜'<VAR>h' h₂' : 𝕜'<VAR>h₁' : 𝕜<VAR>g₁ : 𝕜' → F<VAR>g₁' : F<VAR>L' : Filter 𝕜'<VAR>y : 𝕜'<VAR>f : E → 𝕜'<VAR>f' : E →L[𝕜] 𝕜'<VAR>x : E<VAR>L'' : Filter E<VAR>hh₂ : HasDerivAtFilter h₂ h₂' (f x) L'<VAR>hf : HasFDerivAtFilter f f' x L''<VAR>hL : Tendsto f L'' L'<VAR>hy : y = f x<GOAL>HasFDerivAtFilter (h₂ ∘ f) (h₂' • f') x L''
<VAR>𝕜 : Type u_1<VAR>F : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>f : F → 𝕜<VAR>f' x : F<VAR>s : Set F<VAR>L : Filter F<VAR>frechet : F →L[𝕜] 𝕜<GOAL>HasFDerivAt f frechet x ↔ HasGradientAt f ((toDual 𝕜 F).symm frechet) x
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>s1 s2 : AffineSubspace k P<GOAL>s1 < s2 ↔ s1 ≤ s2 ∧ ∃ p ∈ s2, p ∉ s1
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<GOAL>count K v 1 = 0
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>h1 : 1 = spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑1<GOAL>count K v 1 = 0
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>k : Type u_3<VAR>V : Type u_4<VAR>P : Type u_5<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AffineSpace V P<VAR>inst✝¹ : DivisionRing k<VAR>inst✝ : Module k V<VAR>t : Set P<VAR>ht : affineSpan k t = ⊤<GOAL>∃ s ⊆ t, ∃ b, ⇑b = Subtype.val
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>k : Type u_3<VAR>V : Type u_4<VAR>P : Type u_5<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AffineSpace V P<VAR>inst✝¹ : DivisionRing k<VAR>inst✝ : Module k V<VAR>t : Set P<VAR>ht : affineSpan k t = ⊤<VAR>s : Set P<VAR>hst : s ⊆ t<VAR>h_tot : affineSpan k s = affineSpan k t<VAR>h_ind : AffineIndependent k Subtype.val<GOAL>∃ s ⊆ t, ∃ b, ⇑b = Subtype.val
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>k : Type u_3<VAR>V : Type u_4<VAR>P : Type u_5<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AffineSpace V P<VAR>inst✝¹ : DivisionRing k<VAR>inst✝ : Module k V<VAR>t : Set P<VAR>ht : affineSpan k t = ⊤<VAR>s : Set P<VAR>hst : s ⊆ t<VAR>h_tot : affineSpan k s = affineSpan k t<VAR>h_ind : AffineIndependent k Subtype.val<GOAL>affineSpan k (range Subtype.val) = ⊤
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : LinearOrderedField R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y p₂ : P<VAR>h : p₂ ∈ s<GOAL>s.SSameSide x y ↔ x ∉ s ∧ y ∉ s ∧ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : LinearOrderedField R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y p₂ : P<VAR>h : p₂ ∈ s<GOAL>(x ∉ s ∧ y ∉ s ∧ ∃ p₂_1 ∈ s, SameRay R (y -ᵥ p₂) (x -ᵥ p₂_1)) ↔ x ∉ s ∧ y ∉ s ∧ ∃ p₁ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)
<VAR>n p : ℕ<VAR>pp : Prime p<VAR>k a : ℕ<GOAL>a ∈ (p ^ k).properDivisors ↔ a ∈ map { toFun := fun x => p ^ x, inj' := ⋯ } (range k)
<VAR>n p : ℕ<VAR>pp : Prime p<VAR>k a : ℕ<GOAL>a ∣ p ^ k ∧ a < p ^ k ↔ ∃ a_1 < k, p ^ a_1 = a
<VAR>n p : ℕ<VAR>pp : Prime p<VAR>k a : ℕ<VAR>this : a ∈ (p ^ k).properDivisors ↔ ∃ j, ∃ (_ : j < k), a = p ^ j<GOAL>a ∣ p ^ k ∧ a < p ^ k ↔ ∃ a_1 < k, p ^ a_1 = a
<VAR>n p : ℕ<VAR>pp : Prime p<VAR>k a : ℕ<VAR>this : a ∣ p ^ k ∧ a < p ^ k ↔ ∃ j, ∃ (_ : j < k), a = p ^ j<GOAL>a ∣ p ^ k ∧ a < p ^ k ↔ ∃ a_1 < k, p ^ a_1 = a
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Simplex ℝ P n<GOAL>s.circumcenter = (affineCombination ℝ univ s.pointsWithCircumcenter) (circumcenterWeightsWithCircumcenter n)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Simplex ℝ P n<GOAL>s.pointsWithCircumcenter circumcenterIndex = (affineCombination ℝ univ s.pointsWithCircumcenter) (circumcenterWeightsWithCircumcenter n)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Simplex ℝ P n<GOAL>(affineCombination ℝ univ s.pointsWithCircumcenter) (circumcenterWeightsWithCircumcenter n) = s.pointsWithCircumcenter circumcenterIndex
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>n : ℕ<VAR>s : Simplex ℝ P n<GOAL>∀ i2 ∈ univ, i2 ≠ circumcenterIndex → circumcenterWeightsWithCircumcenter n i2 = 0
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : PseudoEMetricSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>f : α → β<VAR>x✝ y✝ z : α<VAR>s : Set α<VAR>h : Isometry f<VAR>x : α<VAR>r : ℝ≥0∞<VAR>y : α<GOAL>y ∈ f ⁻¹' EMetric.ball (f x) r ↔ y ∈ EMetric.ball x r
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>M : Type u_3<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : LieRingModule L M<VAR>inst✝¹ : LieModule R L M<VAR>H : LieSubalgebra R L<VAR>α χ : ↥H → R<VAR>p q : ℤ<VAR>inst✝ : LieAlgebra.IsNilpotent R ↥H<VAR>hq : weightSpace M (q • α + χ) = ⊥<VAR>x : L<VAR>hx : x ∈ rootSpace H α<VAR>y : M<VAR>hy : y ∈ weightSpaceChain M α χ p q<GOAL>⁅x, y⁆ ∈ weightSpaceChain M α χ p q
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>M : Type u_3<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : LieRingModule L M<VAR>inst✝¹ : LieModule R L M<VAR>H : LieSubalgebra R L<VAR>α χ : ↥H → R<VAR>p q : ℤ<VAR>inst✝ : LieAlgebra.IsNilpotent R ↥H<VAR>hq : weightSpace M (q • α + χ) = ⊥<VAR>x : L<VAR>hx : x ∈ rootSpace H α<VAR>y : M<VAR>hy : y ∈ ⨆ x, weightSpace M (↑x • α + χ)<GOAL>⁅x, y⁆ ∈ weightSpaceChain M α χ p q
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>M : Type u_3<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : LieRingModule L M<VAR>inst✝¹ : LieModule R L M<VAR>H : LieSubalgebra R L<VAR>α χ : ↥H → R<VAR>p q : ℤ<VAR>inst✝ : LieAlgebra.IsNilpotent R ↥H<VAR>hq : weightSpace M (q • α + χ) = ⊥<VAR>x : L<VAR>hx : x ∈ rootSpace H α<VAR>y : M<VAR>k : { k // k ∈ Ioo p q }<VAR>z : M<VAR>hz : z ∈ weightSpace M (↑k • α + χ)<GOAL>⁅x, z⁆ ∈ weightSpaceChain M α χ p q
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>M : Type u_3<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : LieRingModule L M<VAR>inst✝¹ : LieModule R L M<VAR>H : LieSubalgebra R L<VAR>α χ : ↥H → R<VAR>p q : ℤ<VAR>inst✝ : LieAlgebra.IsNilpotent R ↥H<VAR>hq : weightSpace M (q • α + χ) = ⊥<VAR>x : L<VAR>hx : x ∈ rootSpace H α<VAR>y : M<GOAL>⁅x, 0⁆ ∈ weightSpaceChain M α χ p q
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>M : Type u_3<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : LieRingModule L M<VAR>inst✝¹ : LieModule R L M<VAR>H : LieSubalgebra R L<VAR>α χ : ↥H → R<VAR>p q : ℤ<VAR>inst✝ : LieAlgebra.IsNilpotent R ↥H<VAR>hq : weightSpace M (q • α + χ) = ⊥<VAR>x : L<VAR>hx : x ∈ rootSpace H α<VAR>y z₁ z₂ : M<VAR>hx✝ : z₁ ∈ ⨆ i, weightSpace M (↑i • α + χ)<VAR>hy✝ : z₂ ∈ ⨆ i, weightSpace M (↑i • α + χ)<VAR>hz₁ : ⁅x, z₁⁆ ∈ weightSpaceChain M α χ p q<VAR>hz₂ : ⁅x, z₂⁆ ∈ weightSpaceChain M α χ p q<GOAL>⁅x, z₁ + z₂⁆ ∈ weightSpaceChain M α χ p q
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>C : Set (Set α)<VAR>D : Set (Set β)<VAR>s : ℕ → Set α<VAR>h1s : ∀ (n : ℕ), s n ∈ C<VAR>h2s : ⋃ n, s n = univ<VAR>t : ℕ → Set β<VAR>h1t : ∀ (n : ℕ), t n ∈ D<VAR>h2t : ⋃ n, t n = univ<GOAL>IsCountablySpanning (image2 (fun x x_1 => x ×ˢ x_1) C D)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>C : Set (Set α)<VAR>D : Set (Set β)<VAR>s : ℕ → Set α<VAR>h1s : ∀ (n : ℕ), s n ∈ C<VAR>h2s : ⋃ n, s n = univ<VAR>t : ℕ → Set β<VAR>h1t : ∀ (n : ℕ), t n ∈ D<VAR>h2t : ⋃ n, t n = univ<GOAL>⋃ n, (fun n => s (Nat.unpair n).1 ×ˢ t (Nat.unpair n).2) n = univ
<VAR>R : Type u_1<VAR>inst✝⁷ : CommRing R<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : CommRing B<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : Algebra R B<VAR>K : Type u_4<VAR>inst✝² : CommRing K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<GOAL>IsIntegrallyClosed R ↔ ∀ {x : K}, IsIntegral R x → ∃ y, (algebraMap R K) y = 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>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>n : ℕ<VAR>f : MvPolynomial (Fin (n + 1)) R<VAR>i : ℕ<GOAL>i ∈ ((finSuccEquiv R n) f).support ↔ i ∈ Finset.image (fun m => m 0) f.support
<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>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>n : ℕ<VAR>f : MvPolynomial (Fin (n + 1)) R<VAR>i : ℕ<GOAL>(∃ a, (((finSuccEquiv R n) f).coeff i) a ≠ 0 a) ↔ ∃ a ∈ f.support, a 0 = i
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P : Cubic F<VAR>inst✝¹ : Field F<VAR>inst✝ : Field K<VAR>φ : F →+* K<VAR>x y z : K<VAR>ha : P.a ≠ 0<VAR>h3 : (map φ P).roots = {x, y, z}<GOAL>φ P.disc = (φ P.a * φ P.a * (x - y) * (x - z) * (y - z)) ^ 2
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P : Cubic F<VAR>inst✝¹ : Field F<VAR>inst✝ : Field K<VAR>φ : F →+* K<VAR>x y z : K<VAR>ha : P.a ≠ 0<VAR>h3 : (map φ P).roots = {x, y, z}<GOAL>φ P.b ^ 2 * φ P.c ^ 2 - φ 4 * φ P.a * φ P.c ^ 3 - φ 4 * φ P.b ^ 3 * φ P.d - φ 27 * φ P.a ^ 2 * φ P.d ^ 2 + φ 18 * φ P.a * φ P.b * φ P.c * φ P.d = (φ P.a * φ P.a * (x - y) * (x - z) * (y - z)) ^ 2
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P : Cubic F<VAR>inst✝¹ : Field F<VAR>inst✝ : Field K<VAR>φ : F →+* K<VAR>x y z : K<VAR>ha : P.a ≠ 0<VAR>h3 : (map φ P).roots = {x, y, z}<VAR>f4 : φ 4 = 4<GOAL>φ P.b ^ 2 * φ P.c ^ 2 - φ 4 * φ P.a * φ P.c ^ 3 - φ 4 * φ P.b ^ 3 * φ P.d - φ 27 * φ P.a ^ 2 * φ P.d ^ 2 + φ 18 * φ P.a * φ P.b * φ P.c * φ P.d = (φ P.a * φ P.a * (x - y) * (x - z) * (y - z)) ^ 2
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P : Cubic F<VAR>inst✝¹ : Field F<VAR>inst✝ : Field K<VAR>φ : F →+* K<VAR>x y z : K<VAR>ha : P.a ≠ 0<VAR>h3 : (map φ P).roots = {x, y, z}<VAR>f4 : φ 4 = 4<VAR>f18 : φ 18 = 18<GOAL>φ P.b ^ 2 * φ P.c ^ 2 - φ 4 * φ P.a * φ P.c ^ 3 - φ 4 * φ P.b ^ 3 * φ P.d - φ 27 * φ P.a ^ 2 * φ P.d ^ 2 + φ 18 * φ P.a * φ P.b * φ P.c * φ P.d = (φ P.a * φ P.a * (x - y) * (x - z) * (y - z)) ^ 2
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P : Cubic F<VAR>inst✝¹ : Field F<VAR>inst✝ : Field K<VAR>φ : F →+* K<VAR>x y z : K<VAR>ha : P.a ≠ 0<VAR>h3 : (map φ P).roots = {x, y, z}<VAR>f4 : φ 4 = 4<VAR>f18 : φ 18 = 18<VAR>f27 : φ 27 = 27<GOAL>φ P.b ^ 2 * φ P.c ^ 2 - φ 4 * φ P.a * φ P.c ^ 3 - φ 4 * φ P.b ^ 3 * φ P.d - φ 27 * φ P.a ^ 2 * φ P.d ^ 2 + φ 18 * φ P.a * φ P.b * φ P.c * φ P.d = (φ P.a * φ P.a * (x - y) * (x - z) * (y - z)) ^ 2
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P : Cubic F<VAR>inst✝¹ : Field F<VAR>inst✝ : Field K<VAR>φ : F →+* K<VAR>x y z : K<VAR>ha : P.a ≠ 0<VAR>h3 : (map φ P).roots = {x, y, z}<VAR>f4 : φ 4 = 4<VAR>f18 : φ 18 = 18<VAR>f27 : φ 27 = 27<GOAL>(φ P.a * -(x + y + z)) ^ 2 * (φ P.a * (x * y + x * z + y * z)) ^ 2 - 4 * φ P.a * (φ P.a * (x * y + x * z + y * z)) ^ 3 - 4 * (φ P.a * -(x + y + z)) ^ 3 * (φ P.a * -(x * y * z)) - 27 * φ P.a ^ 2 * (φ P.a * -(x * y * z)) ^ 2 + 18 * φ P.a * (φ P.a * -(x + y + z)) * (φ P.a * (x * y + x * z + y * z)) * (φ P.a * -(x * y * z)) = (φ P.a * φ P.a * (x - y) * (x - z) * (y - z)) ^ 2
<VAR>ι : Type u_1<VAR>inst✝⁴ : DecidableEq ι<VAR>A : ι → Type u_2<VAR>R : Type u_3<VAR>inst✝³ : (i : ι) → AddCommMonoid (A i)<VAR>inst✝² : AddMonoid ι<VAR>inst✝¹ : GSemiring A<VAR>inst✝ : Semiring R<VAR>f : (i : ι) → A i →+ R<VAR>hone : (f 0) GradedMonoid.GOne.one = 1<VAR>hmul : ∀ {i j : ι} (ai : A i) (aj : A j), (f (i + j)) (GradedMonoid.GMul.mul ai aj) = (f i) ai * (f j) aj<GOAL>(toAddMonoid f) ((of A 0) GradedMonoid.GOne.one) = 1
<VAR>ι : Type u_1<VAR>inst✝⁴ : DecidableEq ι<VAR>A : ι → Type u_2<VAR>R : Type u_3<VAR>inst✝³ : (i : ι) → AddCommMonoid (A i)<VAR>inst✝² : AddMonoid ι<VAR>inst✝¹ : GSemiring A<VAR>inst✝ : Semiring R<VAR>f : (i : ι) → A i →+ R<VAR>hone : (f 0) GradedMonoid.GOne.one = 1<VAR>hmul : ∀ {i j : ι} (ai : A i) (aj : A j), (f (i + j)) (GradedMonoid.GMul.mul ai aj) = (f i) ai * (f j) aj<GOAL>(f 0) GradedMonoid.GOne.one = 1
<VAR>ι : Type u_1<VAR>inst✝⁴ : DecidableEq ι<VAR>A : ι → Type u_2<VAR>R : Type u_3<VAR>inst✝³ : (i : ι) → AddCommMonoid (A i)<VAR>inst✝² : AddMonoid ι<VAR>inst✝¹ : GSemiring A<VAR>inst✝ : Semiring R<VAR>f : (i : ι) → A i →+ R<VAR>hone : (f 0) GradedMonoid.GOne.one = 1<VAR>hmul : ∀ {i j : ι} (ai : A i) (aj : A j), (f (i + j)) (GradedMonoid.GMul.mul ai aj) = (f i) ai * (f j) aj<GOAL>∀ (x y : ⨁ (i : ι), A i), { toFun := ⇑(toAddMonoid f), map_one' := ⋯ }.toFun (x * y) = { toFun := ⇑(toAddMonoid f), map_one' := ⋯ }.toFun x * { toFun := ⇑(toAddMonoid f), map_one' := ⋯ }.toFun y
<VAR>ι : Type u_1<VAR>inst✝⁴ : DecidableEq ι<VAR>A : ι → Type u_2<VAR>R : Type u_3<VAR>inst✝³ : (i : ι) → AddCommMonoid (A i)<VAR>inst✝² : AddMonoid ι<VAR>inst✝¹ : GSemiring A<VAR>inst✝ : Semiring R<VAR>f : (i : ι) → A i →+ R<VAR>hone : (f 0) GradedMonoid.GOne.one = 1<VAR>hmul : ∀ {i j : ι} (ai : A i) (aj : A j), (f (i + j)) (GradedMonoid.GMul.mul ai aj) = (f i) ai * (f j) aj<GOAL>AddMonoidHom.mul.compr₂ (toAddMonoid f) = (AddMonoidHom.mul.comp (toAddMonoid f)).compl₂ (toAddMonoid f)
<VAR>ι : Type u_1<VAR>inst✝⁴ : DecidableEq ι<VAR>A : ι → Type u_2<VAR>R : Type u_3<VAR>inst✝³ : (i : ι) → AddCommMonoid (A i)<VAR>inst✝² : AddMonoid ι<VAR>inst✝¹ : GSemiring A<VAR>inst✝ : Semiring R<VAR>f : (i : ι) → A i →+ R<VAR>hone : (f 0) GradedMonoid.GOne.one = 1<VAR>hmul : ∀ {i j : ι} (ai : A i) (aj : A j), (f (i + j)) (GradedMonoid.GMul.mul ai aj) = (f i) ai * (f j) aj<VAR>xi : ι<VAR>xv : A xi<GOAL>((AddMonoidHom.mul.compr₂ (toAddMonoid f)).comp (of A xi)) xv = (((AddMonoidHom.mul.comp (toAddMonoid f)).compl₂ (toAddMonoid f)).comp (of A xi)) xv
<VAR>ι : Type u_1<VAR>inst✝⁴ : DecidableEq ι<VAR>A : ι → Type u_2<VAR>R : Type u_3<VAR>inst✝³ : (i : ι) → AddCommMonoid (A i)<VAR>inst✝² : AddMonoid ι<VAR>inst✝¹ : GSemiring A<VAR>inst✝ : Semiring R<VAR>f : (i : ι) → A i →+ R<VAR>hone : (f 0) GradedMonoid.GOne.one = 1<VAR>hmul : ∀ {i j : ι} (ai : A i) (aj : A j), (f (i + j)) (GradedMonoid.GMul.mul ai aj) = (f i) ai * (f j) aj<VAR>xi : ι<VAR>xv : A xi<VAR>yi : ι<VAR>yv : A yi<GOAL>((((AddMonoidHom.mul.compr₂ (toAddMonoid f)).comp (of A xi)) xv).comp (of A yi)) yv = (((((AddMonoidHom.mul.comp (toAddMonoid f)).compl₂ (toAddMonoid f)).comp (of A xi)) xv).comp (of A yi)) yv
<VAR>ι : Type u_1<VAR>inst✝⁴ : DecidableEq ι<VAR>A : ι → Type u_2<VAR>R : Type u_3<VAR>inst✝³ : (i : ι) → AddCommMonoid (A i)<VAR>inst✝² : AddMonoid ι<VAR>inst✝¹ : GSemiring A<VAR>inst✝ : Semiring R<VAR>f : (i : ι) → A i →+ R<VAR>hone : (f 0) GradedMonoid.GOne.one = 1<VAR>hmul : ∀ {i j : ι} (ai : A i) (aj : A j), (f (i + j)) (GradedMonoid.GMul.mul ai aj) = (f i) ai * (f j) aj<VAR>xi : ι<VAR>xv : A xi<VAR>yi : ι<VAR>yv : A yi<GOAL>(toAddMonoid f) ((of A xi) xv * (of A yi) yv) = (toAddMonoid f) ((of A xi) xv) * (toAddMonoid f) ((of A yi) yv)
<VAR>ι : Type u_1<VAR>inst✝⁴ : DecidableEq ι<VAR>A : ι → Type u_2<VAR>R : Type u_3<VAR>inst✝³ : (i : ι) → AddCommMonoid (A i)<VAR>inst✝² : AddMonoid ι<VAR>inst✝¹ : GSemiring A<VAR>inst✝ : Semiring R<VAR>f : (i : ι) → A i →+ R<VAR>hone : (f 0) GradedMonoid.GOne.one = 1<VAR>hmul : ∀ {i j : ι} (ai : A i) (aj : A j), (f (i + j)) (GradedMonoid.GMul.mul ai aj) = (f i) ai * (f j) aj<VAR>xi : ι<VAR>xv : A xi<VAR>yi : ι<VAR>yv : A yi<GOAL>(f (xi + yi)) (GradedMonoid.GMul.mul xv yv) = (f xi) xv * (f yi) yv
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>P2 : Type u_5<VAR>V3 : Type u_6<VAR>P3 : Type u_7<VAR>V4 : Type u_8<VAR>P4 : Type u_9<VAR>inst✝¹² : Ring k<VAR>inst✝¹¹ : AddCommGroup V1<VAR>inst✝¹⁰ : Module k V1<VAR>inst✝⁹ : AffineSpace V1 P1<VAR>inst✝⁸ : AddCommGroup V2<VAR>inst✝⁷ : Module k V2<VAR>inst✝⁶ : AffineSpace V2 P2<VAR>inst✝⁵ : AddCommGroup V3<VAR>inst✝⁴ : Module k V3<VAR>inst✝³ : AffineSpace V3 P3<VAR>inst✝² : AddCommGroup V4<VAR>inst✝¹ : Module k V4<VAR>inst✝ : AffineSpace V4 P4<VAR>p₀ p₁ : P1<VAR>c : k<GOAL>p₁ -ᵥ (lineMap p₀ p₁) c = (1 - c) • (p₁ -ᵥ p₀)
<VAR>R : Type u_1<VAR>inst✝⁵ : AddCommGroupWithOne R<VAR>inst✝⁴ : PartialOrder R<VAR>inst✝³ : CovariantClass R R (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝² : ZeroLEOneClass R<VAR>inst✝¹ : NeZero 1<VAR>inst✝ : Nontrivial R<VAR>m n : ℤ<GOAL>↑n ≤ 0 ↔ n ≤ 0
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>f : L.Functions 1<VAR>t : L.Term α<VAR>v : α → M<GOAL>(funMap f fun i => realize v (![t] i)) = funMap f ![realize v t]
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>f : L.Functions 1<VAR>t : L.Term α<VAR>v : α → M<VAR>i : Fin 1<GOAL>realize v (![t] i) = ![realize v t] i