ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>W✝ : Affine R<VAR>f : R →+* S<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x₁ x₂ y₁ y₂ : F<VAR>h₁ : W.Equation x₁ y₁<VAR>h₂ : W.Equation x₂ y₂<VAR>hxy : x₁ = x₂ → y₁ ≠ W.negY x₂ y₂<VAR>hy₂ : y₂ = eval x₂ (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))<GOAL>Y - C (C (W.slope x₁ x₂ y₁ y₂ * (x₂ - x₁) + y₁)) + C (X - C x₂) * C (C (-W.slope x₁ x₂ y₁ y₂)) = Y - C (C (W.slope x₁ x₂ y₁ y₂) * (X - C x₁) + C y₁)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>W✝ : Affine R<VAR>f : R →+* S<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x₁ x₂ y₁ y₂ : F<VAR>h₁ : W.Equation x₁ y₁<VAR>h₂ : W.Equation x₂ y₂<VAR>hxy : x₁ = x₂ → y₁ ≠ W.negY x₂ y₂<VAR>hy₂ : y₂ = eval x₂ (linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))<GOAL>Y - (C (C (W.slope x₁ x₂ y₁ y₂)) * (C (C x₂) - C (C x₁)) + C (C y₁)) + (C X - C (C x₂)) * -C (C (W.slope x₁ x₂ y₁ y₂)) = Y - (C (C (W.slope x₁ x₂ y₁ y₂)) * (C X - C (C x₁)) + C (C y₁))
<VAR>k : ℕ<VAR>x : ℝ<VAR>hk : k ≠ 0<VAR>hx : x ∈ Icc 0 1<GOAL>sinZeta (↑x) (2 * ↑k + 1) = (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k + 1) / 2 / ↑(2 * k + 1)! * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))
<VAR>k : ℕ<VAR>x : ℝ<VAR>hk : k ≠ 0<VAR>hx : x ∈ Icc 0 1<GOAL>∑' (b : ℕ), ↑(Real.sin (2 * π * x * ↑b)) / ↑b ^ (2 * ↑k + 1) = (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k + 1) / 2 / ↑(2 * k + 1)! * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))
<VAR>k : ℕ<VAR>x : ℝ<VAR>hk : k ≠ 0<VAR>hx : x ∈ Icc 0 1<GOAL>1 < (2 * ↑k + 1).re
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝ : LinearOrderedField α<VAR>r : ℝ<VAR>ha : r ≤ 0<VAR>f : ι → ℝ<GOAL>(⨆ i, f i) * r = ⨅ i, f i * r
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝³ : Fintype m<VAR>inst✝² : Fintype n<VAR>K : Type u<VAR>inst✝¹ : Semifield K<VAR>inst✝ : DecidableEq m<VAR>w : m → K<GOAL>ker (toLin' (diagonal w)) = ⨆ i ∈ {i | w i = 0}, LinearMap.range (LinearMap.stdBasis K (fun x => K) i)
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝³ : Fintype m<VAR>inst✝² : Fintype n<VAR>K : Type u<VAR>inst✝¹ : Semifield K<VAR>inst✝ : DecidableEq m<VAR>w : m → K<GOAL>⨅ i, comap (toLin' (diagonal w)) (ker (proj i)) = ⨆ i ∈ {i | w i = 0}, LinearMap.range (LinearMap.stdBasis K (fun x => K) i)
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝³ : Fintype m<VAR>inst✝² : Fintype n<VAR>K : Type u<VAR>inst✝¹ : Semifield K<VAR>inst✝ : DecidableEq m<VAR>w : m → K<VAR>this : ∀ (i : m), ker (proj i ∘ₗ toLin' (diagonal w)) = comap (toLin' (diagonal w)) (ker (proj i))<GOAL>⨅ i, comap (toLin' (diagonal w)) (ker (proj i)) = ⨆ i ∈ {i | w i = 0}, LinearMap.range (LinearMap.stdBasis K (fun x => K) i)
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝³ : Fintype m<VAR>inst✝² : Fintype n<VAR>K : Type u<VAR>inst✝¹ : Semifield K<VAR>inst✝ : DecidableEq m<VAR>w : m → K<VAR>this : ∀ (i : m), ker (proj i ∘ₗ toLin' (diagonal w)) = comap (toLin' (diagonal w)) (ker (proj i))<GOAL>⨅ i, ⨅ (_ : w i ≠ 0), ker (proj i) = ⨆ i ∈ {i | w i = 0}, LinearMap.range (LinearMap.stdBasis K (fun x => K) i)
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝³ : Fintype m<VAR>inst✝² : Fintype n<VAR>K : Type u<VAR>inst✝¹ : Semifield K<VAR>inst✝ : DecidableEq m<VAR>w : m → K<VAR>this✝ : ∀ (i : m), ker (proj i ∘ₗ toLin' (diagonal w)) = comap (toLin' (diagonal w)) (ker (proj i))<VAR>this : univ ⊆ {i | w i = 0} ∪ {i | w i = 0}ᶜ<GOAL>⨅ i, ⨅ (_ : w i ≠ 0), ker (proj i) = ⨆ i ∈ {i | w i = 0}, LinearMap.range (LinearMap.stdBasis K (fun x => K) i)
<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>hq0_ne : q ≠ 0<VAR>hμ : μ ≠ 0<GOAL>eLpNorm' 0 q μ = 0
<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>hq0_ne : q ≠ 0<VAR>hμ : μ ≠ 0<VAR>hq0 : 0 ≤ q<GOAL>eLpNorm' 0 q μ = 0
<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>hq0_ne : q ≠ 0<VAR>hμ : μ ≠ 0<VAR>hq_neg : q < 0<GOAL>eLpNorm' 0 q μ = 0
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>H : Type u_3<VAR>inst✝⁴ : Category.{u_4, u_1} C<VAR>inst✝³ : Category.{u_5, u_2} D<VAR>inst✝² : Category.{u_6, u_3} H<VAR>L : C ⥤ D<VAR>F : C ⥤ H<VAR>E : L.LeftExtension F<VAR>X : C<VAR>h : E.IsPointwiseLeftKanExtensionAt (L.obj X)<VAR>inst✝¹ : L.Full<VAR>inst✝ : L.Faithful<GOAL>IsIso (E.hom.app X)
<VAR>G : Type w<VAR>inst✝¹ : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝ : R1Space G<VAR>f : G ≃ₜ G<VAR>h : ∀ ⦃K : Compacts G⦄, (fun s => ↑(μ.toFun s)) (Compacts.map ⇑f ⋯ K) = (fun s => ↑(μ.toFun s)) K<VAR>A : Set G<GOAL>μ.outerMeasure (⇑f ⁻¹' A) = μ.outerMeasure A
<VAR>G : Type w<VAR>inst✝¹ : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝ : R1Space G<VAR>f : G ≃ₜ G<VAR>h : ∀ ⦃K : Compacts G⦄, (fun s => ↑(μ.toFun s)) (Compacts.map ⇑f ⋯ K) = (fun s => ↑(μ.toFun s)) K<VAR>A : Set G<GOAL>∀ (s : Set G) (hs : IsOpen s), μ.innerContent { carrier := ⇑f.toEquiv ⁻¹' s, is_open' := ⋯ } = μ.innerContent { carrier := s, is_open' := hs }
<VAR>G : Type w<VAR>inst✝¹ : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝ : R1Space G<VAR>f : G ≃ₜ G<VAR>h : ∀ ⦃K : Compacts G⦄, (fun s => ↑(μ.toFun s)) (Compacts.map ⇑f ⋯ K) = (fun s => ↑(μ.toFun s)) K<VAR>A s : Set G<VAR>hs : IsOpen s<GOAL>μ.innerContent { carrier := ⇑f.toEquiv ⁻¹' s, is_open' := ⋯ } = μ.innerContent { carrier := s, is_open' := hs }
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : FiniteDimensional 𝕜 E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : T2Space E<VAR>F : ι → Set E<VAR>h_card : ↑(finrank 𝕜 E) + 1 ≤ PartENat.card ι<VAR>h_convex : ∀ (i : ι), Convex 𝕜 (F i)<VAR>h_compact : ∀ (i : ι), IsCompact (F i)<VAR>h_inter : ∀ (I : Finset ι), I.card = finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty<GOAL>(⋂ i, F i).Nonempty
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : FiniteDimensional 𝕜 E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : T2Space E<VAR>F : ι → Set E<VAR>h_card : ↑(finrank 𝕜 E) + 1 ≤ PartENat.card ι<VAR>h_convex : ∀ (i : ι), Convex 𝕜 (F i)<VAR>h_compact : ∀ (i : ι), IsCompact (F i)<VAR>h_inter : ∀ (I : Finset ι), I.card = finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty<GOAL>∀ (I : Finset ι), I.card ≤ finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : FiniteDimensional 𝕜 E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : T2Space E<VAR>F : ι → Set E<VAR>h_card : ↑(finrank 𝕜 E) + 1 ≤ PartENat.card ι<VAR>h_convex : ∀ (i : ι), Convex 𝕜 (F i)<VAR>h_compact : ∀ (i : ι), IsCompact (F i)<VAR>h_inter : ∀ (I : Finset ι), I.card = finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty<VAR>I : Finset ι<VAR>hI_card : I.card ≤ finrank 𝕜 E + 1<VAR>J : Finset ι<VAR>hJ_ss : I ⊆ J<VAR>hJ_card : J.card = finrank 𝕜 E + 1<GOAL>(⋂ i ∈ I, F i).Nonempty
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : FiniteDimensional 𝕜 E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : T2Space E<VAR>F : ι → Set E<VAR>h_card : ↑(finrank 𝕜 E) + 1 ≤ PartENat.card ι<VAR>h_convex : ∀ (i : ι), Convex 𝕜 (F i)<VAR>h_compact : ∀ (i : ι), IsCompact (F i)<VAR>h_inter : ∀ (I : Finset ι), I.card = finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty<VAR>I : Finset ι<VAR>hI_card : I.card ≤ finrank 𝕜 E + 1<VAR>J : Finset ι<VAR>hJ_ss : I ⊆ J<VAR>hJ_card : J.card = finrank 𝕜 E + 1<GOAL>(⋂ x ∈ fun a => a ∈ J.val, F x).Nonempty
<VAR>R : Type u_1<VAR>inst✝⁹ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁸ : CommSemiring S<VAR>inst✝⁷ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁶ : CommSemiring P<VAR>N : Submonoid S<VAR>T : Type u_4<VAR>inst✝⁵ : CommSemiring T<VAR>inst✝⁴ : Algebra R T<VAR>inst✝³ : Algebra S T<VAR>inst✝² : IsScalarTower R S T<VAR>inst✝¹ : IsLocalization M S<VAR>p : Ideal S<VAR>Hp : p.IsPrime<VAR>inst✝ : IsLocalization.AtPrime T p<GOAL>IsLocalization.AtPrime T (Ideal.comap (algebraMap R S) p)
<VAR>R : Type u_1<VAR>inst✝⁹ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁸ : CommSemiring S<VAR>inst✝⁷ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁶ : CommSemiring P<VAR>N : Submonoid S<VAR>T : Type u_4<VAR>inst✝⁵ : CommSemiring T<VAR>inst✝⁴ : Algebra R T<VAR>inst✝³ : Algebra S T<VAR>inst✝² : IsScalarTower R S T<VAR>inst✝¹ : IsLocalization M S<VAR>p : Ideal S<VAR>Hp : p.IsPrime<VAR>inst✝ : IsLocalization.AtPrime T p<GOAL>∀ (x : S), IsUnit x → x ∈ p.primeCompl
<VAR>R : Type u_1<VAR>inst✝⁹ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁸ : CommSemiring S<VAR>inst✝⁷ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁶ : CommSemiring P<VAR>N : Submonoid S<VAR>T : Type u_4<VAR>inst✝⁵ : CommSemiring T<VAR>inst✝⁴ : Algebra R T<VAR>inst✝³ : Algebra S T<VAR>inst✝² : IsScalarTower R S T<VAR>inst✝¹ : IsLocalization M S<VAR>p : Ideal S<VAR>Hp : p.IsPrime<VAR>inst✝ : IsLocalization.AtPrime T p<VAR>x : S<VAR>hx : IsUnit x<VAR>hx' : x ∈ ↑p<GOAL>False
<VAR>𝕜 : Type u_1<VAR>inst✝³⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³⁶ : NormedAddCommGroup E<VAR>inst✝³⁵ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝³⁴ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝³³ : TopologicalSpace M<VAR>inst✝³² : ChartedSpace H M<VAR>inst✝³¹ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝³⁰ : NormedAddCommGroup E'<VAR>inst✝²⁹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝²⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝²⁷ : TopologicalSpace M'<VAR>inst✝²⁶ : ChartedSpace H' M'<VAR>inst✝²⁵ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝²² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝²¹ : TopologicalSpace M''<VAR>inst✝²⁰ : ChartedSpace H'' M''<VAR>F : Type u_11<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f✝ f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x✝ : M<VAR>m n✝ n : ℕ∞<VAR>f : M → M'<VAR>x : M<GOAL>ContinuousAt f x ∧ ContDiffWithinAtProp I I' n (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) univ (↑(chartAt H x) x) ↔ ContinuousAt f x ∧ ContDiffWithinAt 𝕜 n (↑(extChartAt I' (f x)) ∘ f ∘ ↑(extChartAt I x).symm) (range ↑I) (↑(extChartAt I x) x)
<VAR>𝕜 : Type u_1<VAR>inst✝³⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³⁶ : NormedAddCommGroup E<VAR>inst✝³⁵ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝³⁴ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝³³ : TopologicalSpace M<VAR>inst✝³² : ChartedSpace H M<VAR>inst✝³¹ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝³⁰ : NormedAddCommGroup E'<VAR>inst✝²⁹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝²⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝²⁷ : TopologicalSpace M'<VAR>inst✝²⁶ : ChartedSpace H' M'<VAR>inst✝²⁵ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝²² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝²¹ : TopologicalSpace M''<VAR>inst✝²⁰ : ChartedSpace H'' M''<VAR>F : Type u_11<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f✝ f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x✝ : M<VAR>m n✝ n : ℕ∞<VAR>f : M → M'<VAR>x : M<GOAL>ContinuousAt f x ∧ ContDiffWithinAt 𝕜 n (↑I' ∘ (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) ∘ ↑I.symm) (range ↑I) (↑I (↑(chartAt H x) x)) ↔ ContinuousAt f x ∧ ContDiffWithinAt 𝕜 n (↑(extChartAt I' (f x)) ∘ f ∘ ↑(extChartAt I x).symm) (range ↑I) (↑(extChartAt I x) x)
<VAR>X : Type u<VAR>inst✝¹ : Lattice X<VAR>inst✝ : JordanHolderLattice X<VAR>s₁ s₂ : CompositionSeries X<VAR>h : s₁.Equivalent s₂<VAR>i : Fin s₂.length<GOAL>Iso (s₁.toFun ((Exists.choose h).symm i).castSucc, s₁.toFun ((Exists.choose h).symm i).succ) (s₂.toFun i.castSucc, s₂.toFun i.succ)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>J : Type u_4<VAR>inst✝² : Category.{u_5, u_1} C<VAR>inst✝¹ : Category.{u_6, u_2} D<VAR>inst✝ : Category.{?u.11066, u_3} E<VAR>X Y : GradedObject J C<VAR>e : X ≅ Y<VAR>F : C ⥤ D<VAR>j : J<GOAL>F.map (e.inv j) ≫ F.map (e.hom j) = 𝟙 (F.obj (Y j))
<VAR>Fq F : Type<VAR>inst✝² : Field Fq<VAR>inst✝¹ : Field F<VAR>inst✝ : DecidableEq (RatFunc Fq)<VAR>x : RatFunc Fq<VAR>hx : x ≠ 0<GOAL>inftyValuationDef Fq x = ↑(Multiplicative.ofAdd x.intDegree)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>a : α<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>inst✝ : IsSFiniteKernel η<VAR>f : α → β → ℝ≥0∞<VAR>hf : Measurable (uncurry f)<VAR>F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)<GOAL>Measurable fun a => ∫⁻ (b : β), f a b ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>a : α<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>inst✝ : IsSFiniteKernel η<VAR>f : α → β → ℝ≥0∞<VAR>hf : Measurable (uncurry f)<VAR>F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)<VAR>h : ∀ (a : α × β), ⨆ n, ↑(F n) a = uncurry f a<GOAL>Measurable fun a => ∫⁻ (b : β), f a b ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>a : α<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>inst✝ : IsSFiniteKernel η<VAR>f : α → β → ℝ≥0∞<VAR>hf : Measurable (uncurry f)<VAR>F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)<VAR>h : ∀ (a : α) (b : β), ⨆ n, ↑(F n) (a, b) = f a b<GOAL>Measurable fun a => ∫⁻ (b : β), f a b ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>a : α<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>inst✝ : IsSFiniteKernel η<VAR>f : α → β → ℝ≥0∞<VAR>hf : Measurable (uncurry f)<VAR>F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)<VAR>h : ∀ (a : α) (b : β), ⨆ n, ↑(F n) (a, b) = f a b<VAR>this : ∀ (a : α), ∫⁻ (b : β), ⨆ n, ↑(F n) (a, b) ∂κ a = ⨆ n, ∫⁻ (b : β), ↑(F n) (a, b) ∂κ a<GOAL>Measurable fun a => ⨆ n, ∫⁻ (b : β), ↑(F n) (a, b) ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>a : α<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>inst✝ : IsSFiniteKernel η<VAR>f : α → β → ℝ≥0∞<VAR>hf : Measurable (uncurry f)<VAR>F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)<VAR>h : ∀ (a : α) (b : β), ⨆ n, ↑(F n) (a, b) = f a b<VAR>this : ∀ (a : α), ∫⁻ (b : β), ⨆ n, ↑(F n) (a, b) ∂κ a = ⨆ n, ∫⁻ (b : β), ↑(F n) (a, b) ∂κ a<VAR>n : ℕ<GOAL>Measurable fun a => ∫⁻ (b : β), ↑(F n) (a, b) ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>a : α<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>inst✝ : IsSFiniteKernel η<VAR>f : α → β → ℝ≥0∞<VAR>hf : Measurable (uncurry f)<VAR>F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)<VAR>h : ∀ (a : α) (b : β), ⨆ n, ↑(F n) (a, b) = f a b<VAR>this : ∀ (a : α), ∫⁻ (b : β), ⨆ n, ↑(F n) (a, b) ∂κ a = ⨆ n, ∫⁻ (b : β), ↑(F n) (a, b) ∂κ a<VAR>n : ℕ<GOAL>∀ (c : ℝ≥0∞) {s : Set (α × β)} (hs : MeasurableSet s), (fun f => Measurable fun a => ∫⁻ (b : β), ↑f (a, b) ∂κ a) (SimpleFunc.piecewise s hs (SimpleFunc.const (α × β) c) (SimpleFunc.const (α × β) 0))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>a : α<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>inst✝ : IsSFiniteKernel η<VAR>f : α → β → ℝ≥0∞<VAR>hf : Measurable (uncurry f)<VAR>F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)<VAR>h : ∀ (a : α) (b : β), ⨆ n, ↑(F n) (a, b) = f a b<VAR>this : ∀ (a : α), ∫⁻ (b : β), ⨆ n, ↑(F n) (a, b) ∂κ a = ⨆ n, ∫⁻ (b : β), ↑(F n) (a, b) ∂κ a<VAR>n : ℕ<GOAL>∀ ⦃f g : SimpleFunc (α × β) ℝ≥0∞⦄, Disjoint (support ↑f) (support ↑g) → (fun f => Measurable fun a => ∫⁻ (b : β), ↑f (a, b) ∂κ a) f → (fun f => Measurable fun a => ∫⁻ (b : β), ↑f (a, b) ∂κ a) g → (fun f => Measurable fun a => ∫⁻ (b : β), ↑f (a, b) ∂κ a) (f + g)
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>E : Type u₃<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : Category.{v₃, u₃} E<VAR>F : C × D ⥤ E<VAR>W : C<VAR>X Y Z : D<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>F.map (𝟙 W, f ≫ g) = F.map (𝟙 W, f) ≫ F.map (𝟙 W, g)
<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>r : α → α → Prop<VAR>a b c d : α<VAR>h : ∀ (b : α), ¬r a b<GOAL>ReflTransGen r a b ↔ b = a
<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>r : α → α → Prop<VAR>a b c d : α<VAR>h : ∀ (b : α), ¬r a b<GOAL>(a = b ∨ ∃ c, r a c ∧ ReflTransGen r c b) ↔ b = a
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p q r : R[X]<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>x : S<GOAL>eval₂ f x 1 = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>f✝ f₁ f₂ : Filter α<VAR>g✝ g₁ g₂ : Set α → Filter β<VAR>inst✝ : Nonempty ι<VAR>f : ι → Filter α<VAR>g : Set α → Filter β<VAR>hf : Directed (fun x x_1 => x ≥ x_1) f<VAR>hg : Monotone g<VAR>s : Set β<GOAL>s ∈ (iInf f).lift g → s ∈ ⨅ i, (f i).lift g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>f✝ f₁ f₂ : Filter α<VAR>g✝ g₁ g₂ : Set α → Filter β<VAR>inst✝ : Nonempty ι<VAR>f : ι → Filter α<VAR>g : Set α → Filter β<VAR>hf : Directed (fun x x_1 => x ≥ x_1) f<VAR>hg : Monotone g<VAR>s : Set β<GOAL>∀ (x : Set α) (x_1 : ι), x ∈ f x_1 → s ∈ g x → s ∈ ⨅ i, (f i).lift g
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>X✝ Y✝ Z : C<VAR>D : Type u_1<VAR>E : Type u_2<VAR>inst✝¹ : Category.{u_3, u_1} D<VAR>inst✝ : Category.{?u.30099, u_2} E<VAR>X Y : C<VAR>e : X ≅ Y<VAR>F : C ⥤ D<GOAL>F.map e.hom ≫ F.map e.inv = 𝟙 (F.obj X)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s✝ s₁ s₂ t t₁ t₂ u : Set α<VAR>x : α<VAR>s : Set α<GOAL>s ⊆ insert x (s \ {x})
<VAR>x✝ y x : ℝ<VAR>hx : 0 ≤ x<GOAL>log √x = log x / 2
<VAR>x✝ y x : ℝ<VAR>hx : 0 ≤ x<GOAL>2 ≠ 0
<VAR>C : Type u₁<VAR>inst✝² : Category.{u₂, u₁} C<VAR>I : Type v₁<VAR>inst✝¹ : Category.{v₂, v₁} I<VAR>F : I ⥤ C<VAR>inst✝ : HasColimit F<VAR>i : I<GOAL>(limitOpIsoOpColimit F).hom ≫ (colimit.ι F i).op = limit.π F.op (op i)
<VAR>ι : Type u_1<VAR>R' : Type u_2<VAR>R : Type u_3<VAR>A : ι → Type u_4<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : (i : ι) → CommSemiring (A i)<VAR>inst✝ : (i : ι) → Algebra R (A i)<VAR>x y : ⨂[R] (i : ι), A i<GOAL>(mul x) y = (mul y) x
<VAR>ι : Type u_1<VAR>R' : Type u_2<VAR>R : Type u_3<VAR>A : ι → Type u_4<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : (i : ι) → CommSemiring (A i)<VAR>inst✝ : (i : ι) → Algebra R (A i)<VAR>x y : ⨂[R] (i : ι), A i<GOAL>mul = mul.flip
<VAR>ι : Type u_1<VAR>R' : Type u_2<VAR>R : Type u_3<VAR>A : ι → Type u_4<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : (i : ι) → CommSemiring (A i)<VAR>inst✝ : (i : ι) → Algebra R (A i)<VAR>x✝ y✝ : ⨂[R] (i : ι), A i<VAR>x y : (i : ι) → A i<GOAL>(mul ((tprod R) x)) ((tprod R) y) = (mul ((tprod R) y)) ((tprod R) x)
<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>g : γ → δ<VAR>f' : α → β' → δ<VAR>g' : β → β'<VAR>h_distrib : ∀ (a : α) (b : β), g (f a b) = f' a (g' b)<GOAL>g '' image2 f ↑s ↑t = image2 f' (↑s) (g' '' ↑t)
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝³ : FunLike F G H<VAR>a : G<VAR>b : H<VAR>inst✝² : AddGroup G<VAR>inst✝¹ : AddGroup H<VAR>inst✝ : AddConstMapClass F G H a b<VAR>f : F<VAR>x : G<VAR>n : ℤ<GOAL>f (x - n • a) = f x - n • b
<VAR>R : Type u<VAR>inst✝³ : NonUnitalSemiring R<VAR>inst✝² : PartialOrder R<VAR>inst✝¹ : StarRing R<VAR>inst✝ : StarOrderedRing R<VAR>x : R<GOAL>star x ≤ 0 ↔ x ≤ 0
<VAR>F : Type v'<VAR>R' : Type u'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>C : Type w'<VAR>inst✝¹⁶ : CommSemiring R<VAR>inst✝¹⁵ : StarRing R<VAR>inst✝¹⁴ : NonUnitalSemiring A<VAR>inst✝¹³ : StarRing A<VAR>inst✝¹² : Module R A<VAR>inst✝¹¹ : IsScalarTower R A A<VAR>inst✝¹⁰ : SMulCommClass R A A<VAR>inst✝⁹ : StarModule R A<VAR>inst✝⁸ : NonUnitalSemiring B<VAR>inst✝⁷ : StarRing B<VAR>inst✝⁶ : Module R B<VAR>inst✝⁵ : IsScalarTower R B B<VAR>inst✝⁴ : SMulCommClass R B B<VAR>inst✝³ : StarModule R B<VAR>inst✝² : FunLike F A B<VAR>inst✝¹ : NonUnitalAlgHomClass F R A B<VAR>inst✝ : NonUnitalStarAlgHomClass F R A B<VAR>S : NonUnitalStarSubalgebra R A<VAR>f : F<VAR>x : A<GOAL>map f (adjoin R {x}) = adjoin R {f x}
<VAR>n : ℤ<VAR>help : ∀ (m : ℤ), 0 ≤ m → m < 8 → χ₈ ↑m = if m % 2 = 0 then 0 else if m = 1 ∨ m = 7 then 1 else -1<GOAL>χ₈ ↑n = if n % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 7 then 1 else -1
<VAR>n : ℤ<VAR>help : ∀ (m : ℤ), 0 ≤ m → m < 8 → χ₈ ↑m = if m % 2 = 0 then 0 else if m = 1 ∨ m = 7 then 1 else -1<GOAL>χ₈ ↑(n % ↑8) = if n % 8 % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 7 then 1 else -1