ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : Semiring R<VAR>n : σ →₀ ℕ<VAR>φ : MvPowerSeries σ R<VAR>a : R<GOAL>(coeff R n) ((C σ R) a * φ) = a * (coeff R n) φ
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝⁴ : Category.{v, u} V<VAR>inst✝³ : HasZeroMorphisms V<VAR>α : Type u_2<VAR>inst✝² : AddRightCancelSemigroup α<VAR>inst✝¹ : One α<VAR>inst✝ : DecidableEq α<VAR>X : α → V<VAR>d : (n : α) → X (n + 1) ⟶ X n<VAR>sq : ∀ (n : α), d (n + 1) ≫ d n = 0<VAR>j : α<GOAL>(if j + 1 = j + 1 then 𝟙 (X (j + 1)) ≫ d j else 0) = d j
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>C : Type u_6<VAR>inst✝⁵ : AddCommMonoid A<VAR>inst✝⁴ : AddCommMonoid B<VAR>inst✝³ : AddCommMonoid C<VAR>t : ι → A → C<VAR>h0 : ∀ (i : ι), t i 0 = 0<VAR>h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y<VAR>s : Finset α<VAR>f✝ : α → ι →₀ A<VAR>i : ι<VAR>g✝ : ι →₀ A<VAR>k : ι → A → γ → B<VAR>x : γ<VAR>β : Type u_7<VAR>M : Type u_8<VAR>M' : Type u_9<VAR>N : Type u_10<VAR>P : Type u_11<VAR>G : Type u_12<VAR>H : Type u_13<VAR>R : Type u_14<VAR>S : Type u_15<VAR>inst✝² : Zero M<VAR>inst✝¹ : Zero M'<VAR>inst✝ : CommMonoid N<VAR>f : α →₀ M<VAR>a : α<VAR>g : α → M → N<VAR>h₀ : ∀ (b : α), f b ≠ 0 → b ≠ a → g b (f b) = 1<VAR>h₁ : f a = 0 → g a 0 = 1<GOAL>f.prod g = g a (f a)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>C : Type u_6<VAR>inst✝⁵ : AddCommMonoid A<VAR>inst✝⁴ : AddCommMonoid B<VAR>inst✝³ : AddCommMonoid C<VAR>t : ι → A → C<VAR>h0 : ∀ (i : ι), t i 0 = 0<VAR>h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y<VAR>s : Finset α<VAR>f✝ : α → ι →₀ A<VAR>i : ι<VAR>g✝ : ι →₀ A<VAR>k : ι → A → γ → B<VAR>x : γ<VAR>β : Type u_7<VAR>M : Type u_8<VAR>M' : Type u_9<VAR>N : Type u_10<VAR>P : Type u_11<VAR>G : Type u_12<VAR>H : Type u_13<VAR>R : Type u_14<VAR>S : Type u_15<VAR>inst✝² : Zero M<VAR>inst✝¹ : Zero M'<VAR>inst✝ : CommMonoid N<VAR>f : α →₀ M<VAR>a : α<VAR>g : α → M → N<VAR>h₀ : ∀ (b : α), f b ≠ 0 → b ≠ a → g b (f b) = 1<VAR>h₁ : f a = 0 → g a 0 = 1<VAR>b : α<VAR>hb₁ : b ∈ f.support<VAR>hb₂ : b ≠ a<GOAL>g b (f b) = 1
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>C : Type u_6<VAR>inst✝⁵ : AddCommMonoid A<VAR>inst✝⁴ : AddCommMonoid B<VAR>inst✝³ : AddCommMonoid C<VAR>t : ι → A → C<VAR>h0 : ∀ (i : ι), t i 0 = 0<VAR>h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y<VAR>s : Finset α<VAR>f✝ : α → ι →₀ A<VAR>i : ι<VAR>g✝ : ι →₀ A<VAR>k : ι → A → γ → B<VAR>x : γ<VAR>β : Type u_7<VAR>M : Type u_8<VAR>M' : Type u_9<VAR>N : Type u_10<VAR>P : Type u_11<VAR>G : Type u_12<VAR>H : Type u_13<VAR>R : Type u_14<VAR>S : Type u_15<VAR>inst✝² : Zero M<VAR>inst✝¹ : Zero M'<VAR>inst✝ : CommMonoid N<VAR>f : α →₀ M<VAR>a : α<VAR>g : α → M → N<VAR>h₀ : ∀ (b : α), f b ≠ 0 → b ≠ a → g b (f b) = 1<VAR>h₁ : f a = 0 → g a 0 = 1<VAR>h : a ∉ f.support<GOAL>g a (f a) = 1
<VAR>F : Type u_1<VAR>inst✝³ : Field F<VAR>E : Type u_2<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>H : Subgroup (E ≃ₐ[F] E)<VAR>K : IntermediateField F E<VAR>inst✝ : FiniteDimensional F E<VAR>h : IsGalois F E<GOAL>IntermediateField.fixedField K.fixingSubgroup = K
<VAR>F : Type u_1<VAR>inst✝³ : Field F<VAR>E : Type u_2<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>H : Subgroup (E ≃ₐ[F] E)<VAR>K : IntermediateField F E<VAR>inst✝ : FiniteDimensional F E<VAR>h : IsGalois F E<VAR>K_le : K ≤ IntermediateField.fixedField K.fixingSubgroup<GOAL>IntermediateField.fixedField K.fixingSubgroup = K
<VAR>F : Type u_1<VAR>inst✝³ : Field F<VAR>E : Type u_2<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>H : Subgroup (E ≃ₐ[F] E)<VAR>K : IntermediateField F E<VAR>inst✝ : FiniteDimensional F E<VAR>h : IsGalois F E<VAR>K_le : K ≤ IntermediateField.fixedField K.fixingSubgroup<GOAL>finrank (↥K) E = finrank (↥(IntermediateField.fixedField K.fixingSubgroup)) E
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t : Set α<VAR>f g : α → ℝ≥0∞<VAR>h : s =ᶠ[ae μ] t<GOAL>⨍⁻ (x : α) in s, f x ∂μ = ⨍⁻ (x : α) in t, f x ∂μ
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>inst✝ : PseudoMetricSpace γ<VAR>f g : α →ᵇ β<VAR>x : α<VAR>C : ℝ<GOAL>⨆ x, dist (f x) (g x) = ↑(⨆ x, nndist (f x) (g x))
<VAR>a b : ℝ<VAR>f f' : ℝ → ℝ<VAR>s : Set ℝ<VAR>hs : s.OrdConnected<VAR>hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x<GOAL>(f' '' s).OrdConnected
<VAR>a b : ℝ<VAR>f f' : ℝ → ℝ<VAR>s : Set ℝ<VAR>hs : s.OrdConnected<VAR>hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x<GOAL>∀ x ∈ f' '' s, ∀ y ∈ f' '' s, x < y → Ioo x y ⊆ f' '' s
<VAR>a✝ b✝ : ℝ<VAR>f f' : ℝ → ℝ<VAR>s : Set ℝ<VAR>hs : s.OrdConnected<VAR>hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x<VAR>a : ℝ<VAR>ha : a ∈ s<VAR>b : ℝ<VAR>hb : b ∈ s<VAR>m : ℝ<VAR>hma : f' a < m<VAR>hmb : m < f' b<GOAL>m ∈ f' '' s
<VAR>a✝ b✝ : ℝ<VAR>f f' : ℝ → ℝ<VAR>s : Set ℝ<VAR>hs : s.OrdConnected<VAR>hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x<VAR>a : ℝ<VAR>ha : a ∈ s<VAR>b : ℝ<VAR>hb : b ∈ s<VAR>m : ℝ<VAR>hma : f' a < m<VAR>hmb : m < f' b<VAR>hab : a ≤ b<GOAL>m ∈ f' '' s
<VAR>a✝ b✝ : ℝ<VAR>f f' : ℝ → ℝ<VAR>s : Set ℝ<VAR>hs : s.OrdConnected<VAR>hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x<VAR>a : ℝ<VAR>ha : a ∈ s<VAR>b : ℝ<VAR>hb : b ∈ s<VAR>m : ℝ<VAR>hma : f' a < m<VAR>hmb : m < f' b<VAR>hab : b ≤ a<GOAL>m ∈ f' '' s
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : Semiring α<VAR>I : Ideal α<VAR>a b : α<GOAL>CompleteLattice.IsCompactElement ⊤
<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>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>inst✝⁷ : DecidableEq α'<VAR>inst✝⁶ : DecidableEq β'<VAR>inst✝⁵ : DecidableEq γ<VAR>inst✝⁴ : DecidableEq γ'<VAR>inst✝³ : DecidableEq δ<VAR>inst✝² : DecidableEq δ'<VAR>inst✝¹ : DecidableEq ε<VAR>inst✝ : DecidableEq ε'<VAR>f✝ f' : α → β → γ<VAR>g g' : α → β → γ → δ<VAR>s✝ s' : Finset α<VAR>t✝ t' : Finset β<VAR>u u' : Finset γ<VAR>a a' : α<VAR>b b' : β<VAR>c : γ<VAR>f : α → β → γ<VAR>s : Finset α<VAR>t : Finset β<GOAL>image2 f ↑s ↑t = image2 (fun a b => f b a) ↑t ↑s
<VAR>α : Type u<VAR>l l' : List α<GOAL>(l ++ l').rotate l.length = l' ++ l
<VAR>α : Type u<VAR>l l' : List α<GOAL>(l ++ l').rotate' l.length = l' ++ l
<VAR>R✝ : Type u<VAR>S✝ : Type v<VAR>A✝ : Type w<VAR>B : Type u₁<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : CommSemiring S<VAR>inst✝⁴ : Semiring A<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra S A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : IsScalarTower R S A<VAR>hRS : ⊤.FG<VAR>hSA : ⊤.FG<VAR>s : Finset S<VAR>hs : adjoin R ↑s = ⊤<VAR>t : Finset A<VAR>ht : adjoin S ↑t = ⊤<GOAL>adjoin R ↑(Finset.image (⇑(algebraMap S A)) s ∪ t) = ⊤
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<GOAL>μ.withDensity f = 0 ↔ f =ᶠ[ae μ] 0
<VAR>G : Type u<VAR>inst✝ : Monoid G<VAR>n : ℕ<GOAL>exponent G ∣ n ↔ ∀ (g : G), orderOf g ∣ n
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : ClosedIicTopology α<VAR>inst✝ : TopologicalSpace β<VAR>a b c : α<VAR>f : α → β<VAR>H : a < b<GOAL>Ioo a b ∈ 𝓝[<] b
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Preadditive C<VAR>D : Type u_2<VAR>inst✝² : Category.{u_3, u_2} D<VAR>inst✝¹ : Preadditive D<VAR>F : C ⥤ D<VAR>inst✝ : F.Additive<GOAL>alternatingFaceMapComplex C ⋙ F.mapHomologicalComplex (ComplexShape.down ℕ) = (SimplicialObject.whiskering C D).obj F ⋙ alternatingFaceMapComplex D
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Preadditive C<VAR>D : Type u_2<VAR>inst✝² : Category.{u_3, u_2} D<VAR>inst✝¹ : Preadditive D<VAR>F : C ⥤ D<VAR>inst✝ : F.Additive<GOAL>autoParam (∀ (X Y : SimplicialObject C) (f : X ⟶ Y), (alternatingFaceMapComplex C ⋙ F.mapHomologicalComplex (ComplexShape.down ℕ)).map f = eqToHom ⋯ ≫ ((SimplicialObject.whiskering C D).obj F ⋙ alternatingFaceMapComplex D).map f ≫ eqToHom ⋯) _auto✝
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Preadditive C<VAR>D : Type u_2<VAR>inst✝² : Category.{u_3, u_2} D<VAR>inst✝¹ : Preadditive D<VAR>F : C ⥤ D<VAR>inst✝ : F.Additive<GOAL>∀ (X : SimplicialObject C), (alternatingFaceMapComplex C ⋙ F.mapHomologicalComplex (ComplexShape.down ℕ)).obj X = ((SimplicialObject.whiskering C D).obj F ⋙ alternatingFaceMapComplex D).obj X
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>c : E<VAR>f✝ : α → E<VAR>hf : AEStronglyMeasurable f✝ μ<VAR>s : Set α<VAR>f : α → F<VAR>hs : MeasurableSet s<GOAL>eLpNormEssSup (s.indicator f) μ = eLpNormEssSup f (μ.restrict s)
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝ : DivisionRing α<VAR>p q : ℚ<VAR>a b : ℤ<VAR>b0 : ↑b ≠ 0<GOAL>↑(a /. b) = ↑a / ↑b
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝ : DivisionRing α<VAR>p q : ℚ<VAR>a b : ℤ<VAR>b0 : ↑b ≠ 0<VAR>b0' : b ≠ 0<GOAL>↑(a /. b) = ↑a / ↑b
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝ : DivisionRing α<VAR>p q : ℚ<VAR>a b : ℤ<VAR>b0 : ↑b ≠ 0<VAR>b0' : b ≠ 0<VAR>n : ℤ<VAR>d : ℕ<VAR>h : d ≠ 0<VAR>c : n.natAbs.Coprime d<VAR>e : a /. b = { num := n, den := d, den_nz := h, reduced := c }<GOAL>↑{ num := n, den := d, den_nz := h, reduced := c } = ↑a / ↑b
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝ : DivisionRing α<VAR>p q : ℚ<VAR>a b : ℤ<VAR>b0 : ↑b ≠ 0<VAR>b0' : b ≠ 0<VAR>n : ℤ<VAR>d : ℕ<VAR>h : d ≠ 0<VAR>c : n.natAbs.Coprime d<VAR>e : a /. b = { num := n, den := d, den_nz := h, reduced := c }<VAR>d0 : ↑d ≠ 0<GOAL>↑{ num := n, den := d, den_nz := h, reduced := c } = ↑a / ↑b
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝ : DivisionRing α<VAR>p q : ℚ<VAR>a b : ℤ<VAR>b0 : ↑b ≠ 0<VAR>b0' : b ≠ 0<VAR>n : ℤ<VAR>d : ℕ<VAR>h : d ≠ 0<VAR>c : n.natAbs.Coprime d<VAR>e : a /. b = n /. ↑d<VAR>d0 : ↑d ≠ 0<GOAL>↑{ num := n, den := d, den_nz := h, reduced := c } = ↑a / ↑b
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝ : DivisionRing α<VAR>p q : ℚ<VAR>a b : ℤ<VAR>b0 : ↑b ≠ 0<VAR>b0' : b ≠ 0<VAR>n : ℤ<VAR>d : ℕ<VAR>h : d ≠ 0<VAR>c : n.natAbs.Coprime d<VAR>e : a /. b = n /. ↑d<VAR>d0 : ↑d ≠ 0<VAR>this : ↑(a * ↑d) = ↑(n * b)<GOAL>↑{ num := n, den := d, den_nz := h, reduced := c } = ↑a / ↑b
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝ : DivisionRing α<VAR>p q : ℚ<VAR>a b : ℤ<VAR>b0 : ↑b ≠ 0<VAR>b0' : b ≠ 0<VAR>n : ℤ<VAR>d : ℕ<VAR>h : d ≠ 0<VAR>c : n.natAbs.Coprime d<VAR>e : a /. b = n /. ↑d<VAR>d0 : ↑d ≠ 0<VAR>this : ↑a * ↑d = ↑n * ↑b<GOAL>↑{ num := n, den := d, den_nz := h, reduced := c } = ↑a / ↑b
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : StarRing R<VAR>inst✝¹⁰ : TopologicalSpace A<VAR>inst✝⁹ : Semiring A<VAR>inst✝⁸ : Algebra R A<VAR>inst✝⁷ : StarRing A<VAR>inst✝⁶ : StarModule R A<VAR>inst✝⁵ : TopologicalSemiring A<VAR>inst✝⁴ : ContinuousStar A<VAR>inst✝³ : TopologicalSpace B<VAR>inst✝² : Semiring B<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : StarRing B<VAR>s : Subalgebra R A<GOAL>(star s).topologicalClosure = star s.topologicalClosure
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : StarRing R<VAR>inst✝¹⁰ : TopologicalSpace A<VAR>inst✝⁹ : Semiring A<VAR>inst✝⁸ : Algebra R A<VAR>inst✝⁷ : StarRing A<VAR>inst✝⁶ : StarModule R A<VAR>inst✝⁵ : TopologicalSemiring A<VAR>inst✝⁴ : ContinuousStar A<VAR>inst✝³ : TopologicalSpace B<VAR>inst✝² : Semiring B<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : StarRing B<VAR>s : Subalgebra R A<GOAL>∀ (t : Subalgebra R A), (star t).topologicalClosure ≤ star t.topologicalClosure
<VAR>n m : ℕ<VAR>hnm : n < m<GOAL>filter (fun x => decide (x < n + 1)) (Ico n m) = [n]
<VAR>n m : ℕ<VAR>hnm : n < m<VAR>r : min m (n + 1) = n + 1<GOAL>filter (fun x => decide (x < n + 1)) (Ico n m) = [n]
<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 ≠ 0 ↔ (map φ P).roots.Nodup
<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>x ≠ y ∧ x ≠ z ∧ y ≠ z ↔ {x, y, z}.Nodup
<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>x ≠ y ∧ x ≠ z ∧ y ≠ z ↔ (x ::ₘ y ::ₘ {z}).Nodup
<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>x ≠ y ∧ x ≠ z ∧ y ≠ z ↔ ¬(x = y ∨ x = z) ∧ ¬y = z ∧ {z}.Nodup
<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>x ≠ y ∧ x ≠ z ∧ y ≠ z ↔ ¬(x = y ∨ x = z) ∧ ¬y = z ∧ True
<VAR>𝕜 : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : MeasurableSpace H<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ : Measure G<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalGroup G<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>K : Set G<VAR>hK : IsCompact K<VAR>h : μ K ≠ 0<VAR>U : Set G<VAR>hU : IsOpen U<VAR>hne : U.Nonempty<GOAL>μ U ≠ 0
<VAR>𝕜 : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : MeasurableSpace H<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ : Measure G<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalGroup G<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>K : Set G<VAR>hK : IsCompact K<VAR>U : Set G<VAR>hU : IsOpen U<VAR>hne : U.Nonempty<VAR>h : μ U = 0<GOAL>μ K = 0
<VAR>𝕜 : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : MeasurableSpace H<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ : Measure G<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalGroup G<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>K : Set G<VAR>hK : IsCompact K<VAR>U : Set G<VAR>hU : IsOpen U<VAR>hne : U.Nonempty<VAR>h : μ U = 0<GOAL>μ K ≤ 0
<VAR>𝕜 : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : MeasurableSpace H<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ : Measure G<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalGroup G<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>K : Set G<VAR>hK : IsCompact K<VAR>U : Set G<VAR>hU : IsOpen U<VAR>hne : (interior U).Nonempty<VAR>h : μ U = 0<GOAL>μ K ≤ 0
<VAR>𝕜 : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : MeasurableSpace H<VAR>inst✝⁴ : TopologicalSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ : Measure G<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalGroup G<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>K : Set G<VAR>hK : IsCompact K<VAR>U : Set G<VAR>hU : IsOpen U<VAR>hne : (interior U).Nonempty<VAR>h : μ U = 0<VAR>t : Finset G<VAR>hKt : K ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' U<GOAL>μ K ≤ 0
<VAR>l m₁ : List Char<VAR>c : Char<VAR>m₂ r : List Char<GOAL>{ str := { data := l ++ (m₁ ++ c :: m₂) ++ r }, startPos := { byteIdx := utf8Len l }, stopPos := { byteIdx := utf8Len l + utf8Len (m₁ ++ c :: m₂) } }.next { byteIdx := utf8Len m₁ } = { byteIdx := utf8Len m₁ + c.utf8Size }
<VAR>l m₁ : List Char<VAR>c : Char<VAR>m₂ r : List Char<GOAL>(if { byteIdx := utf8Len l } + { byteIdx := utf8Len m₁ } = { byteIdx := utf8Len l + (utf8Len m₁ + (utf8Len m₂ + c.utf8Size)) } then { byteIdx := utf8Len m₁ } else { byteIdx := ({ data := l ++ (m₁ ++ c :: (m₂ ++ r)) }.next ({ byteIdx := utf8Len l } + { byteIdx := utf8Len m₁ })).byteIdx - utf8Len l }) = { byteIdx := utf8Len m₁ + c.utf8Size }
<VAR>l m₁ : List Char<VAR>c : Char<VAR>m₂ r : List Char<GOAL>{ byteIdx := ({ data := l ++ (m₁ ++ c :: (m₂ ++ r)) }.next ({ byteIdx := utf8Len l } + { byteIdx := utf8Len m₁ })).byteIdx - utf8Len l } = { byteIdx := utf8Len m₁ + c.utf8Size }
<VAR>l m₁ : List Char<VAR>c : Char<VAR>m₂ r : List Char<GOAL>¬({ byteIdx := utf8Len l } + { byteIdx := utf8Len m₁ }).byteIdx = { byteIdx := utf8Len l + (utf8Len m₁ + (utf8Len m₂ + c.utf8Size)) }.byteIdx
<VAR>l m₁ : List Char<VAR>c : Char<VAR>m₂ r : List Char<VAR>this : { data := l ++ m₁ ++ c :: (m₂ ++ r) }.next { byteIdx := utf8Len (l ++ m₁) } = { byteIdx := utf8Len (l ++ m₁) + c.utf8Size }<GOAL>{ byteIdx := ({ data := l ++ (m₁ ++ c :: (m₂ ++ r)) }.next ({ byteIdx := utf8Len l } + { byteIdx := utf8Len m₁ })).byteIdx - utf8Len l } = { byteIdx := utf8Len m₁ + c.utf8Size }
<VAR>l m₁ : List Char<VAR>c : Char<VAR>m₂ r : List Char<VAR>this : { data := l ++ (m₁ ++ c :: (m₂ ++ r)) }.next { byteIdx := utf8Len l + utf8Len m₁ } = { byteIdx := utf8Len l + utf8Len m₁ + c.utf8Size }<GOAL>{ byteIdx := ({ data := l ++ (m₁ ++ c :: (m₂ ++ r)) }.next { byteIdx := utf8Len l + utf8Len m₁ }).byteIdx - utf8Len l } = { byteIdx := utf8Len m₁ + c.utf8Size }
<VAR>l m₁ : List Char<VAR>c : Char<VAR>m₂ r : List Char<VAR>this : { data := l ++ (m₁ ++ c :: (m₂ ++ r)) }.next { byteIdx := utf8Len l + utf8Len m₁ } = { byteIdx := utf8Len l + utf8Len m₁ + c.utf8Size }<GOAL>{ byteIdx := { byteIdx := utf8Len l + utf8Len m₁ + c.utf8Size }.byteIdx - utf8Len l } = { byteIdx := utf8Len m₁ + c.utf8Size }
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Abelian C<VAR>P Q : C<VAR>f : P ⟶ Q<VAR>inst✝ : Epi f<VAR>qbar : Pseudoelement Q<VAR>q : Over Q<GOAL>𝟙 (pullback f q.hom) ≫ ((fun g => app f g) (Over.mk (pullback.fst f q.hom))).hom = pullback.snd f q.hom ≫ q.hom
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x : E<GOAL>o.rightAngleRotationAux₁ (o.rightAngleRotationAux₁ x) = -x
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x : E<GOAL>∀ (v : E), ⟪v, o.rightAngleRotationAux₁ (o.rightAngleRotationAux₁ x)⟫_ℝ = ⟪v, -x⟫_ℝ
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<GOAL>⟪y, o.rightAngleRotationAux₁ (o.rightAngleRotationAux₁ x)⟫_ℝ = ⟪y, -x⟫_ℝ
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<VAR>this : ⟪o.rightAngleRotationAux₁ y, o.rightAngleRotationAux₁ x⟫_ℝ = ⟪y, x⟫_ℝ<GOAL>⟪y, o.rightAngleRotationAux₁ (o.rightAngleRotationAux₁ x)⟫_ℝ = ⟪y, -x⟫_ℝ
<VAR>x y z : ℝ<VAR>n : ℕ<GOAL>rexp 1 ^ n = rexp ↑n
<VAR>n : Type u_1<VAR>α : Type u_2<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>inst✝ : CommRing α<VAR>A : Matrix n n α<GOAL>(X • 1 + A.map ⇑C).det.leadingCoeff = 1
<VAR>n : Type u_1<VAR>α : Type u_2<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>inst✝ : CommRing α<VAR>A : Matrix n n α<VAR>h✝ : Subsingleton α<GOAL>(X • 1 + A.map ⇑C).det.leadingCoeff = 1
<VAR>n : Type u_1<VAR>α : Type u_2<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>inst✝ : CommRing α<VAR>A : Matrix n n α<VAR>h✝ : Nontrivial α<GOAL>(X • 1 + A.map ⇑C).det.leadingCoeff = 1
<VAR>n : Type u_1<VAR>α : Type u_2<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>inst✝ : CommRing α<VAR>A : Matrix n n α<VAR>h✝ : Nontrivial α<GOAL>(X • 1 + A.map ⇑C).det.coeff (X • 1 + A.map ⇑C).det.natDegree = (X • Matrix.map 1 ⇑C + A.map ⇑C).det.coeff (Fintype.card n)
<VAR>n : Type u_1<VAR>α : Type u_2<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>inst✝ : CommRing α<VAR>A : Matrix n n α<VAR>h✝ : Nontrivial α<GOAL>(X • 1 + A.map ⇑C).det.coeff (X • 1 + A.map ⇑C).det.natDegree = (X • 1 + A.map ⇑C).det.coeff (Fintype.card n)
<VAR>n : Type u_1<VAR>α : Type u_2<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>inst✝ : CommRing α<VAR>A : Matrix n n α<VAR>h✝ : Nontrivial α<VAR>h : (X • Matrix.map 1 ⇑C + A.map ⇑C).det.natDegree = Fintype.card n<GOAL>(X • 1 + A.map ⇑C).det.coeff (X • 1 + A.map ⇑C).det.natDegree = (X • 1 + A.map ⇑C).det.coeff (Fintype.card n)
<VAR>n : Type u_1<VAR>α : Type u_2<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>inst✝ : CommRing α<VAR>A : Matrix n n α<VAR>h✝ : Nontrivial α<VAR>h : (X • Matrix.map 1 ⇑C + A.map ⇑C).det.natDegree < Fintype.card n<GOAL>(X • 1 + A.map ⇑C).det.coeff (X • 1 + A.map ⇑C).det.natDegree = (X • 1 + A.map ⇑C).det.coeff (Fintype.card n)
<VAR>a b : ℝ<VAR>n : ℕ<GOAL>∫ (x : ℝ) in a..b, cos x = sin b - sin a
<VAR>a b : ℝ<VAR>n : ℕ<GOAL>deriv sin = cos
<VAR>a b : ℝ<VAR>n : ℕ<GOAL>∀ x ∈ [[a, b]], DifferentiableAt ℝ sin x
<VAR>a b : ℝ<VAR>n : ℕ<GOAL>ContinuousOn cos [[a, b]]
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>K : Type u_4<VAR>A : Type u_5<VAR>A' : Type u_6<VAR>A'' : Type u_7<VAR>V : Type u<VAR>V' : Type u_8<VAR>x : ι → A<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : CommRing A'<VAR>inst✝⁴ : CommRing A''<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R A'<VAR>inst✝¹ : Algebra R A''<VAR>a✝ b : R<VAR>inst✝ : Nontrivial R<VAR>hx : IsTranscendenceBasis R x<VAR>a : A<GOAL>_root_.IsAlgebraic (↥(adjoin R (range x))) a
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>K : Type u_4<VAR>A : Type u_5<VAR>A' : Type u_6<VAR>A'' : Type u_7<VAR>V : Type u<VAR>V' : Type u_8<VAR>x : ι → A<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : CommRing A'<VAR>inst✝⁴ : CommRing A''<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R A'<VAR>inst✝¹ : Algebra R A''<VAR>a✝ b : R<VAR>inst✝ : Nontrivial R<VAR>hx : IsTranscendenceBasis R x<VAR>a : A<GOAL>¬AlgebraicIndependent R fun o => o.elim a x
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>K : Type u_4<VAR>A : Type u_5<VAR>A' : Type u_6<VAR>A'' : Type u_7<VAR>V : Type u<VAR>V' : Type u_8<VAR>x : ι → A<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : CommRing A'<VAR>inst✝⁴ : CommRing A''<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R A'<VAR>inst✝¹ : Algebra R A''<VAR>a✝ b : R<VAR>inst✝ : Nontrivial R<VAR>hx : IsTranscendenceBasis R x<VAR>a : A<VAR>ai : AlgebraicIndependent R fun o => o.elim a x<VAR>h₁ : range x ⊆ range fun o => o.elim a x<GOAL>False
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>K : Type u_4<VAR>A : Type u_5<VAR>A' : Type u_6<VAR>A'' : Type u_7<VAR>V : Type u<VAR>V' : Type u_8<VAR>x : ι → A<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : CommRing A'<VAR>inst✝⁴ : CommRing A''<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R A'<VAR>inst✝¹ : Algebra R A''<VAR>a✝ b : R<VAR>inst✝ : Nontrivial R<VAR>hx : IsTranscendenceBasis R x<VAR>a : A<VAR>ai : AlgebraicIndependent R fun o => o.elim a x<VAR>h₁ : range x ⊆ range fun o => o.elim a x<VAR>h₂ : range x ≠ range fun o => o.elim a x<GOAL>False
<VAR>R : Type u_1<VAR>inst✝⁴ : AddCommMonoid R<VAR>inst✝³ : Pow R ℕ<VAR>inst✝² : BinomialRing R<VAR>inst✝¹ : MulOneClass R<VAR>inst✝ : NatPowAssoc R<VAR>r : R<GOAL>multichoose r 0 = 1
<VAR>R : Type u<VAR>inst✝¹⁴ : CommSemiring R<VAR>S : Type ?u.116938<VAR>inst✝¹³ : Semiring S<VAR>inst✝¹² : Algebra R S<VAR>ι₁ : Type v₁<VAR>ι₂ : Type v₂<VAR>inst✝¹¹ : DecidableEq ι₁<VAR>inst✝¹⁰ : DecidableEq ι₂<VAR>M₁ : ι₁ → Type w₁<VAR>M₁' : Type w₁'<VAR>M₂ : ι₂ → Type w₂<VAR>M₂' : Type w₂'<VAR>inst✝⁹ : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)<VAR>inst✝⁸ : AddCommMonoid M₁'<VAR>inst✝⁷ : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)<VAR>inst✝⁶ : AddCommMonoid M₂'<VAR>inst✝⁵ : (i₁ : ι₁) → Module R (M₁ i₁)<VAR>inst✝⁴ : Module R M₁'<VAR>inst✝³ : (i₂ : ι₂) → Module R (M₂ i₂)<VAR>inst✝² : Module R M₂'<VAR>inst✝¹ : (i₁ : ι₁) → Module S (M₁ i₁)<VAR>inst✝ : ∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)<VAR>i : ι₁<VAR>x : M₁ i<VAR>y : M₂'<GOAL>(directSumLeft R M₁ M₂') ((lof R ι₁ M₁ i) x ⊗ₜ[R] y) = (lof R ι₁ (fun i => M₁ i ⊗[R] M₂') i) (x ⊗ₜ[R] y)