ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t✝ : Set α<VAR>inst✝ : Countable ι<VAR>s : ι → Set α<VAR>hd : Directed (fun x x_1 => x ⊆ x_1) s<VAR>t : Set α<VAR>ht : MeasurableSet t<GOAL>μ (⋃ i, t ∩ s i) = ⨆ i, μ (t ∩ s i)
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t✝ : Set α<VAR>inst✝ : Countable ι<VAR>s : ι → Set α<VAR>hd : Directed (fun x x_1 => x ⊆ x_1) s<VAR>t : Set α<VAR>ht : MeasurableSet t<GOAL>Directed (fun x x_1 => x ⊆ x_1) fun i => t ∩ s i
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>n : ℤ<VAR>hz : z ∈ 𝒟ᵒ<VAR>hg : T ^ n • z ∈ 𝒟ᵒ<GOAL>n = 0
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>n : ℤ<VAR>hz : z ∈ 𝒟ᵒ<VAR>hg : T ^ n • z ∈ 𝒟ᵒ<GOAL>|↑n| < 1
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>n : ℤ<VAR>hz : z ∈ 𝒟ᵒ<VAR>hg : T ^ n • z ∈ 𝒟ᵒ<VAR>h₁ : |z.re| < 1 / 2<GOAL>|↑n| < 1
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>n : ℤ<VAR>hz : z ∈ 𝒟ᵒ<VAR>hg : T ^ n • z ∈ 𝒟ᵒ<VAR>h₁ : |z.re| < 1 / 2<VAR>h₂ : |(T ^ n • z).re| < 1 / 2<GOAL>|↑n| < 1
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>n : ℤ<VAR>hz : z ∈ 𝒟ᵒ<VAR>hg : T ^ n • z ∈ 𝒟ᵒ<VAR>h₁ : |z.re| < 1 / 2<VAR>h₂ : |z.re + ↑n| < 1 / 2<GOAL>|↑n| < 1
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<GOAL>angle x (x - y) ≤ π / 2
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, -y⟫_ℝ = 0<GOAL>angle x (x - y) ≤ π / 2
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, -y⟫_ℝ = 0<GOAL>angle x (x + -y) ≤ π / 2
<VAR>R✝ : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₁' : Type u_9<VAR>M₂' : Type u_10<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>ι : Type u_16<VAR>R : Type u_17<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : Fintype n<VAR>inst✝⁶ : Fintype m<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : DecidableEq m<VAR>inst✝³ : Fintype n'<VAR>inst✝² : Fintype m'<VAR>inst✝¹ : DecidableEq n'<VAR>inst✝ : DecidableEq m'<VAR>B : (n → R) →ₗ[R] (m → R) →ₗ[R] R<VAR>f : (n' → R) →ₗ[R] n → R<GOAL>(toMatrix₂' R) (B ∘ₗ f) = (toMatrix' f)ᵀ * (toMatrix₂' R) B
<VAR>R✝ : Type u_1<VAR>R₁ : Type u_2<VAR>S₁ : Type u_3<VAR>R₂ : Type u_4<VAR>S₂ : Type u_5<VAR>M : Type u_6<VAR>M₁ : Type u_7<VAR>M₂ : Type u_8<VAR>M₁' : Type u_9<VAR>M₂' : Type u_10<VAR>N₂ : Type u_11<VAR>n : Type u_12<VAR>m : Type u_13<VAR>n' : Type u_14<VAR>m' : Type u_15<VAR>ι : Type u_16<VAR>R : Type u_17<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : Fintype n<VAR>inst✝⁶ : Fintype m<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : DecidableEq m<VAR>inst✝³ : Fintype n'<VAR>inst✝² : Fintype m'<VAR>inst✝¹ : DecidableEq n'<VAR>inst✝ : DecidableEq m'<VAR>B : (n → R) →ₗ[R] (m → R) →ₗ[R] R<VAR>f : (n' → R) →ₗ[R] n → R<GOAL>(toMatrix₂' R) (B.compl₁₂ f id) = (toMatrix' f)ᵀ * (toMatrix₂' R) B
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>ι : Type u_4<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>hgf : QuotientMap (g ∘ f)<GOAL>inst✝ ≤ coinduced g inst✝¹
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>ι : Type u_4<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>hf : Continuous f<VAR>hg : Continuous g<VAR>hgf : QuotientMap (g ∘ f)<GOAL>coinduced g (coinduced f inst✝²) ≤ coinduced g inst✝¹
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : K<VAR>i : Free.ChooseBasisIndex ℤ (𝓞 K)<GOAL>((latticeBasis K).repr ((canonicalEmbedding K) x)) i = ↑(((integralBasis K).repr x) i)
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : K<VAR>i : Free.ChooseBasisIndex ℤ (𝓞 K)<GOAL>((Basis.restrictScalars ℚ (latticeBasis K)).repr ⟨(canonicalEmbedding K) x, ⋯⟩) i = ((integralBasis K).repr x) i
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : K<VAR>i : Free.ChooseBasisIndex ℤ (𝓞 K)<VAR>f : K →ₗ[ℚ] ↥(Submodule.span ℚ (Set.range ⇑(latticeBasis K))) := LinearMap.codRestrict (Submodule.span ℚ (Set.range ⇑(latticeBasis K))) (canonicalEmbedding K).toRatAlgHom.toLinearMap ⋯<GOAL>((Basis.restrictScalars ℚ (latticeBasis K)).repr ⟨(canonicalEmbedding K) x, ⋯⟩) i = ((integralBasis K).repr x) i
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : K<VAR>i : Free.ChooseBasisIndex ℤ (𝓞 K)<VAR>f : K →ₗ[ℚ] ↥(Submodule.span ℚ (Set.range ⇑(latticeBasis K))) := LinearMap.codRestrict (Submodule.span ℚ (Set.range ⇑(latticeBasis K))) (canonicalEmbedding K).toRatAlgHom.toLinearMap ⋯<GOAL>↑(Basis.restrictScalars ℚ (latticeBasis K)).repr ∘ₗ f = ↑(integralBasis K).repr
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : K<VAR>i✝ : Free.ChooseBasisIndex ℤ (𝓞 K)<VAR>f : K →ₗ[ℚ] ↥(Submodule.span ℚ (Set.range ⇑(latticeBasis K))) := LinearMap.codRestrict (Submodule.span ℚ (Set.range ⇑(latticeBasis K))) (canonicalEmbedding K).toRatAlgHom.toLinearMap ⋯<VAR>i : Free.ChooseBasisIndex ℤ (𝓞 K)<GOAL>(↑(Basis.restrictScalars ℚ (latticeBasis K)).repr ∘ₗ f) ((integralBasis K) i) = ↑(integralBasis K).repr ((integralBasis K) i)
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : K<VAR>i✝ : Free.ChooseBasisIndex ℤ (𝓞 K)<VAR>f : K →ₗ[ℚ] ↥(Submodule.span ℚ (Set.range ⇑(latticeBasis K))) := LinearMap.codRestrict (Submodule.span ℚ (Set.range ⇑(latticeBasis K))) (canonicalEmbedding K).toRatAlgHom.toLinearMap ⋯<VAR>i : Free.ChooseBasisIndex ℤ (𝓞 K)<VAR>this : f ((integralBasis K) i) = (Basis.restrictScalars ℚ (latticeBasis K)) i<GOAL>(↑(Basis.restrictScalars ℚ (latticeBasis K)).repr ∘ₗ f) ((integralBasis K) i) = ↑(integralBasis K).repr ((integralBasis K) i)
<VAR>f : Ordinal.{u} → Ordinal.{u}<VAR>hf : IsNormal f<GOAL>Ordinal.sup (f ∘ Nat.cast) = f ω
<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>hx : AlgebraicIndependent R x<VAR>f : A →ₐ[R] A'<VAR>hfv : AlgebraicIndependent R (⇑f ∘ x)<VAR>this : aeval (⇑f ∘ x) = f.comp (aeval x)<GOAL>AlgebraicIndependent R 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>hx : AlgebraicIndependent R x<VAR>f : A →ₐ[R] A'<VAR>hfv : Injective (⇑f ∘ ⇑(aeval x))<VAR>this : aeval (⇑f ∘ x) = f.comp (aeval x)<GOAL>AlgebraicIndependent R x
<VAR>α : Type u_1<VAR>a : List α<VAR>l : List (List α)<GOAL>(↑(List.map (fun l => ↑l) (a :: l))).Sections = ↑(List.map (fun l => ↑l) (a :: l).sections)
<VAR>α : Type u_1<VAR>a : List α<VAR>l : List (List α)<GOAL>(↑(↑a :: List.map (fun l => ↑l) l)).Sections = ↑(List.map (fun l => ↑l) (l.sections.bind fun s => List.map (fun a => a :: s) a))
<VAR>α : Type u_1<VAR>a : List α<VAR>l : List (List α)<GOAL>((↑(List.map (fun l => ↑l) l.sections)).bind fun b => map (fun a => a ::ₘ b) ↑a) = ↑(List.map (fun l => ↑l) (l.sections.bind fun s => List.map (fun a => a :: s) a))
<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>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t : Set α<VAR>m : MeasurableSpace α<VAR>I : Finset ι<VAR>μ : ι → Measure α<VAR>s : Set α<GOAL>(∑ i ∈ I, μ i) s = ∑ i ∈ I, (μ i) s
<VAR>G : Type u_1<VAR>P : Type u_2<VAR>inst✝¹ : AddGroup G<VAR>inst✝ : AddTorsor G P<VAR>x y : P<GOAL>-(y -ᵥ (pointReflection x) y) = -(2 • (y -ᵥ x))
<VAR>z : ℍ<VAR>k : ℤ<VAR>hk : 3 ≤ k<VAR>N : ℕ<VAR>a : Fin 2 → ZMod N<VAR>hk' : 2 < ↑k<GOAL>TendstoLocallyUniformly (fun s x => ∑ x_1 ∈ s, eisSummand k (↑x_1) x) (fun x => eisensteinSeries a k x) Filter.atTop
<VAR>z : ℍ<VAR>k : ℤ<VAR>hk : 3 ≤ k<VAR>N : ℕ<VAR>a : Fin 2 → ZMod N<VAR>hk' : 2 < ↑k<VAR>p_sum : Summable fun x => ‖↑x‖ ^ (-k)<GOAL>TendstoLocallyUniformly (fun s x => ∑ x_1 ∈ s, eisSummand k (↑x_1) x) (fun x => eisensteinSeries a k x) Filter.atTop
<VAR>z : ℍ<VAR>k : ℤ<VAR>hk : 3 ≤ k<VAR>N : ℕ<VAR>a : Fin 2 → ZMod N<VAR>hk' : 2 < ↑k<VAR>p_sum : Summable fun x => ‖↑x‖ ^ (-k)<GOAL>∀ (K : Set ℍ), IsCompact K → TendstoUniformlyOn (fun s x => ∑ x_1 ∈ s, eisSummand k (↑x_1) x) (fun x => ∑' (x_1 : ↑(gammaSet N a)), eisSummand k (↑x_1) x) Filter.atTop K
<VAR>z : ℍ<VAR>k : ℤ<VAR>hk : 3 ≤ k<VAR>N : ℕ<VAR>a : Fin 2 → ZMod N<VAR>hk' : 2 < ↑k<VAR>p_sum : Summable fun x => ‖↑x‖ ^ (-k)<VAR>K : Set ℍ<VAR>hK : IsCompact K<GOAL>TendstoUniformlyOn (fun s x => ∑ x_1 ∈ s, eisSummand k (↑x_1) x) (fun x => ∑' (x_1 : ↑(gammaSet N a)), eisSummand k (↑x_1) x) Filter.atTop K
<VAR>z : ℍ<VAR>k : ℤ<VAR>hk : 3 ≤ k<VAR>N : ℕ<VAR>a : Fin 2 → ZMod N<VAR>hk' : 2 < ↑k<VAR>p_sum : Summable fun x => ‖↑x‖ ^ (-k)<VAR>K : Set ℍ<VAR>hK : IsCompact K<VAR>A B : ℝ<VAR>hB : 0 < B<VAR>HABK : K ⊆ verticalStrip A B<GOAL>TendstoUniformlyOn (fun s x => ∑ x_1 ∈ s, eisSummand k (↑x_1) x) (fun x => ∑' (x_1 : ↑(gammaSet N a)), eisSummand k (↑x_1) x) Filter.atTop K
<VAR>z✝ : ℍ<VAR>k : ℤ<VAR>hk : 3 ≤ k<VAR>N : ℕ<VAR>a : Fin 2 → ZMod N<VAR>hk' : 2 < ↑k<VAR>p_sum : Summable fun x => ‖↑x‖ ^ (-k)<VAR>K : Set ℍ<VAR>hK : IsCompact K<VAR>A B : ℝ<VAR>hB : 0 < B<VAR>HABK : K ⊆ verticalStrip A B<VAR>p : ↑(gammaSet N a)<VAR>z : ℍ<VAR>hz : z ∈ verticalStrip A B<GOAL>‖eisSummand k (↑p) z‖ ≤ r ⟨{ re := A, im := B }, hB⟩ ^ (-↑k) * ‖↑p‖ ^ (-k)
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>F G K L : CochainComplex C ℤ<VAR>n m : ℤ<VAR>hnm : ¬n + 1 = m<VAR>z : Cochain F G n<VAR>p q : ℤ<VAR>hpq : p + m = q<GOAL>(Cochain.mk fun p q hpq => z.v p (p + n) ⋯ ≫ G.d (p + n) q + m.negOnePow • F.d p (p + m - n) ≫ z.v (p + m - n) q ⋯).v p q hpq = Cochain.v 0 p q hpq
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>F G K L : CochainComplex C ℤ<VAR>n m : ℤ<VAR>hnm : ¬n + 1 = m<VAR>z : Cochain F G n<VAR>p q : ℤ<VAR>hpq : p + m = q<GOAL>¬(ComplexShape.up ℤ).Rel (p + n) q
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>F G K L : CochainComplex C ℤ<VAR>n m : ℤ<VAR>hnm : ¬n + 1 = m<VAR>z : Cochain F G n<VAR>p q : ℤ<VAR>hpq : p + m = q<GOAL>¬(ComplexShape.up ℤ).Rel p (p + m - n)
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>inst✝⁴ : Semiring R<VAR>φ : ι → Type u_3<VAR>inst✝³ : (i : ι) → AddCommMonoid (φ i)<VAR>inst✝² : (i : ι) → Module R (φ i)<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Finite ι<GOAL>⨆ i, range (stdBasis R φ i) = ⊤
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>inst✝⁴ : Semiring R<VAR>φ : ι → Type u_3<VAR>inst✝³ : (i : ι) → AddCommMonoid (φ i)<VAR>inst✝² : (i : ι) → Module R (φ i)<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Finite ι<VAR>val✝ : Fintype ι<GOAL>⨆ i, range (stdBasis R φ i) = ⊤
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>inst✝⁴ : Semiring R<VAR>φ : ι → Type u_3<VAR>inst✝³ : (i : ι) → AddCommMonoid (φ i)<VAR>inst✝² : (i : ι) → Module R (φ i)<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Finite ι<VAR>val✝ : Fintype ι<VAR>x✝ : ι<GOAL>range (stdBasis R φ x✝) = ⨆ (_ : x✝ ∈ ?intro.convert_1), range (stdBasis R φ x✝)
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>inst✝⁴ : Semiring R<VAR>φ : ι → Type u_3<VAR>inst✝³ : (i : ι) → AddCommMonoid (φ i)<VAR>inst✝² : (i : ι) → Module R (φ i)<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Finite ι<VAR>val✝ : Fintype ι<GOAL>Finset ι
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>inst✝⁴ : Semiring R<VAR>φ : ι → Type u_3<VAR>inst✝³ : (i : ι) → AddCommMonoid (φ i)<VAR>inst✝² : (i : ι) → Module R (φ i)<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Finite ι<VAR>val✝ : Fintype ι<GOAL>univ ⊆ ↑?intro.convert_1 ∪ ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a✝ a₁ a₂ : α<VAR>b b₁✝ b₂✝ : β<VAR>inst✝³ : LinearOrderedField α<VAR>inst✝² : OrderedAddCommGroup β<VAR>inst✝¹ : Module α β<VAR>a : α<VAR>b₁ b₂ : β<VAR>inst✝ : PosSMulMono α β<VAR>h : a < 0<GOAL>a⁻¹ • b₁ ≤ b₂ ↔ a • b₂ ≤ b₁
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>H : Type u_4<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_5<VAR>inst✝⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_6<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>inst✝⁵ : SmoothManifoldWithCorners I M<VAR>M' : Type u_7<VAR>inst✝⁴ : TopologicalSpace M'<VAR>inst✝³ : ChartedSpace H' M'<VAR>inst✝² : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>w x y z : M<VAR>v : E<VAR>h : z ∈ (extChartAt I w).source ∩ (extChartAt I x).source ∩ (extChartAt I y).source<GOAL>(tangentCoordChange I x y z) ((tangentCoordChange I w x z) v) = (tangentCoordChange I w y z) v
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>H : Type u_4<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_5<VAR>inst✝⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_6<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>inst✝⁵ : SmoothManifoldWithCorners I M<VAR>M' : Type u_7<VAR>inst✝⁴ : TopologicalSpace M'<VAR>inst✝³ : ChartedSpace H' M'<VAR>inst✝² : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>w x y z : M<VAR>v : E<VAR>h : z ∈ (extChartAt I w).source ∩ (extChartAt I x).source ∩ (extChartAt I y).source<GOAL>z ∈ (tangentBundleCore I M).baseSet (achart H w) ∩ (tangentBundleCore I M).baseSet (achart H x) ∩ (tangentBundleCore I M).baseSet (achart H y)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>H : Type u_4<VAR>inst✝⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_5<VAR>inst✝⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M : Type u_6<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>inst✝⁵ : SmoothManifoldWithCorners I M<VAR>M' : Type u_7<VAR>inst✝⁴ : TopologicalSpace M'<VAR>inst✝³ : ChartedSpace H' M'<VAR>inst✝² : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>w x y z : M<VAR>v : E<VAR>h : z ∈ (extChartAt I w).source ∩ (extChartAt I x).source ∩ (extChartAt I y).source<GOAL>z ∈ (extChartAt I w).source ∩ (extChartAt I x).source ∩ (extChartAt I y).source
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x✝ : α<VAR>inst✝¹ : AddGroup α<VAR>inst✝ : InvolutiveNeg β<VAR>h : Antiperiodic f c<VAR>x : α<GOAL>f (x - c) = -f x
<VAR>x y : ZFSet<GOAL>y ∈ ⋃₀ {x} ↔ y ∈ x
<VAR>K : Type u<VAR>inst✝¹ : CommRing K<VAR>inst✝ : IsDomain K<VAR>x✝¹ : RatFunc K<VAR>x✝ : FractionRing K[X]<VAR>x : K[X] × ↥K[X]⁰<GOAL>{ toFractionRing := Localization.mk x.1 x.2 }.toFractionRing = (IsLocalization.algEquiv K[X]⁰ (RatFunc K) (FractionRing K[X])) { toFractionRing := Localization.mk x.1 x.2 }
<VAR>K : Type u<VAR>inst✝¹ : CommRing K<VAR>inst✝ : IsDomain K<VAR>x✝¹ : RatFunc K<VAR>x✝ : FractionRing K[X]<VAR>x : K[X] × ↥K[X]⁰<GOAL>IsLocalization.mk' (Localization K[X]⁰) x.1 x.2 = IsLocalization.mk' (FractionRing K[X]) ((RingHom.id K[X]) x.1) ⟨(RingHom.id K[X]) ↑x.2, ⋯⟩
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>inst✝ : CommRing R<VAR>r x y z : R<VAR>a b c : ℍ[R]<GOAL>a * star a = ↑(normSq a)
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝² : PartialOrder Γ<VAR>inst✝¹ : Zero R<VAR>a b : Γ<VAR>r✝ : R<VAR>Γ' : Type u_3<VAR>inst✝ : PartialOrder Γ'<VAR>f : Γ ↪o Γ'<VAR>g : Γ<VAR>r : R<VAR>g' : Γ'<VAR>h : ¬g' = f g<GOAL>(embDomain f ((single g) r)).coeff g' = ((single (f g)) r).coeff g'
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝² : PartialOrder Γ<VAR>inst✝¹ : Zero R<VAR>a b : Γ<VAR>r✝ : R<VAR>Γ' : Type u_3<VAR>inst✝ : PartialOrder Γ'<VAR>f : Γ ↪o Γ'<VAR>g : Γ<VAR>r : R<VAR>g' : Γ'<VAR>h : ¬g' = f g<GOAL>g' ∉ ⇑f '' ((single g) r).support
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝² : PartialOrder Γ<VAR>inst✝¹ : Zero R<VAR>a b : Γ<VAR>r✝ : R<VAR>Γ' : Type u_3<VAR>inst✝ : PartialOrder Γ'<VAR>f : Γ ↪o Γ'<VAR>g : Γ<VAR>r : R<VAR>g' : Γ'<VAR>h : ¬g' = f g<VAR>hr : ¬r = 0<GOAL>g' ∉ ⇑f '' ((single g) r).support
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<GOAL>T2Space X ↔ Pairwise fun x y => Disjoint (𝓝 x) (𝓝 y)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>x y : X<VAR>x✝ : x ≠ y<GOAL>(fun x y => ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v) x y ↔ (fun x y => Disjoint (𝓝 x) (𝓝 y)) x y
<VAR>X Y Z : SemiNormedGrp<VAR>f : X ⟶ Y<VAR>e₁ e₂ : explicitCokernel f ⟶ Z<VAR>h : explicitCokernelπ f ≫ e₁ = explicitCokernelπ f ≫ e₂<VAR>g : Y ⟶ Z := explicitCokernelπ f ≫ e₂<VAR>w : f ≫ g = 0<GOAL>e₁ = e₂
<VAR>X Y Z : SemiNormedGrp<VAR>f : X ⟶ Y<VAR>e₁ e₂ : explicitCokernel f ⟶ Z<VAR>h : explicitCokernelπ f ≫ e₁ = explicitCokernelπ f ≫ e₂<VAR>g : Y ⟶ Z := explicitCokernelπ f ≫ e₂<VAR>w : f ≫ g = 0<VAR>this : e₂ = explicitCokernelDesc w<GOAL>e₁ = e₂
<VAR>X Y Z : SemiNormedGrp<VAR>f : X ⟶ Y<VAR>e₁ e₂ : explicitCokernel f ⟶ Z<VAR>h : explicitCokernelπ f ≫ e₁ = explicitCokernelπ f ≫ e₂<VAR>g : Y ⟶ Z := explicitCokernelπ f ≫ e₂<VAR>w : f ≫ g = 0<VAR>this : e₂ = explicitCokernelDesc w<GOAL>e₁ = explicitCokernelDesc w
<VAR>X Y Z : SemiNormedGrp<VAR>f : X ⟶ Y<VAR>e₁ e₂ : explicitCokernel f ⟶ Z<VAR>h : explicitCokernelπ f ≫ e₁ = explicitCokernelπ f ≫ e₂<VAR>g : Y ⟶ Z := explicitCokernelπ f ≫ e₂<VAR>w : f ≫ g = 0<VAR>this : e₂ = explicitCokernelDesc w<GOAL>explicitCokernelπ f ≫ e₁ = g
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Type u_2<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>A : Type u_3<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>f : M →ₗ[R] A<VAR>g : TensorAlgebra R M →ₐ[R] A<GOAL>g.toLinearMap ∘ₗ ι R = f ↔ g = (lift R) f
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Type u_2<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>A : Type u_3<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>f : M →ₗ[R] A<VAR>g : TensorAlgebra R M →ₐ[R] A<GOAL>g.toLinearMap ∘ₗ ι R = f ↔ (lift R).symm g = f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>s : Set α<VAR>t : Set β<VAR>f✝ : Filter α<VAR>g : Filter β<VAR>f : α → β → γ<VAR>a : α<VAR>B : Filter β<GOAL>map (Function.uncurry f) (pure a ×ˢ B) = map (f a) B
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>s : Set α<VAR>t : Set β<VAR>f✝ : Filter α<VAR>g : Filter β<VAR>f : α → β → γ<VAR>a : α<VAR>B : Filter β<GOAL>map (Function.uncurry f) (map (Prod.mk a) B) = map (f a) B
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r✝ : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>r : α → α → Prop<VAR>inst✝¹ : IsWellOrder α r<VAR>inst✝ : Fintype α<GOAL>type r = ↑(Fintype.card α)
<VAR>m n a b c d : ℤ<VAR>h : a / c ≡ b / c [ZMOD m / c]<VAR>ha✝¹ : c ∣ a<VAR>ha✝ : c ∣ b<VAR>ha : c ∣ m<GOAL>a ≡ b [ZMOD m]
<VAR>𝕂 : Type u_1<VAR>𝕂' : Type u_2<VAR>𝔸 : Type u_3<VAR>inst✝⁶ : Field 𝕂<VAR>inst✝⁵ : Field 𝕂'<VAR>inst✝⁴ : Ring 𝔸<VAR>inst✝³ : Algebra 𝕂 𝔸<VAR>inst✝² : Algebra 𝕂' 𝔸<VAR>inst✝¹ : TopologicalSpace 𝔸<VAR>inst✝ : TopologicalRing 𝔸<VAR>x : 𝔸<GOAL>(expSeries 𝕂 𝔸).sum x = (expSeries 𝕂' 𝔸).sum x
<VAR>𝕂 : Type u_1<VAR>𝕂' : Type u_2<VAR>𝔸 : Type u_3<VAR>inst✝⁶ : Field 𝕂<VAR>inst✝⁵ : Field 𝕂'<VAR>inst✝⁴ : Ring 𝔸<VAR>inst✝³ : Algebra 𝕂 𝔸<VAR>inst✝² : Algebra 𝕂' 𝔸<VAR>inst✝¹ : TopologicalSpace 𝔸<VAR>inst✝ : TopologicalRing 𝔸<VAR>x : 𝔸<VAR>n : ℕ<GOAL>((expSeries 𝕂 𝔸 n) fun x_1 => x) = (expSeries 𝕂' 𝔸 n) fun x_1 => x
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>κ : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝² : LinearOrderedField 𝕜<VAR>r : α → β → Prop<VAR>inst✝¹ : (a : α) → DecidablePred (r a)<VAR>s✝ s₁ s₂ : Finset α<VAR>t t₁ t₂ : Finset β<VAR>a : α<VAR>b : β<VAR>δ : 𝕜<VAR>inst✝ : DecidableEq β<VAR>s : Finset α<VAR>P : Finpartition t<GOAL>(interedges r s t).card = ∑ b ∈ P.parts, (interedges r s b).card
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>m : ι → MeasurableSpace α<VAR>S : Set ι<GOAL>generateFrom (piiUnionInter (fun n => {s | MeasurableSet s}) S) = ⨆ i ∈ S, m i
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>m : ι → MeasurableSpace α<VAR>S : Set ι<GOAL>generateFrom (piiUnionInter (fun n => {s | MeasurableSet s}) S) ≤ ⨆ i ∈ S, m i
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>m : ι → MeasurableSpace α<VAR>S : Set ι<GOAL>⨆ i ∈ S, m i ≤ generateFrom (piiUnionInter (fun n => {s | MeasurableSet s}) S)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁹ : MeasurableSpace X<VAR>μ : Measure X<VAR>𝕜 : Type u_5<VAR>inst✝⁸ : RCLike 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>p : ℝ≥0∞<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : CompleteSpace F<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>L : E →L[𝕜] F<VAR>φ : X → E<VAR>φ_int : Integrable φ μ<GOAL>∫ (x : X), L (φ x) ∂μ = L (∫ (x : X), φ x ∂μ)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁹ : MeasurableSpace X<VAR>μ : Measure X<VAR>𝕜 : Type u_5<VAR>inst✝⁸ : RCLike 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>p : ℝ≥0∞<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : CompleteSpace F<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>L : E →L[𝕜] F<VAR>φ : X → E<VAR>φ_int : Integrable φ μ<GOAL>∀ (c : E) ⦃s : Set X⦄, MeasurableSet s → μ s < ⊤ → (fun φ => ∫ (x : X), L (φ x) ∂μ = L (∫ (x : X), φ x ∂μ)) (s.indicator fun x => c)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁹ : MeasurableSpace X<VAR>μ : Measure X<VAR>𝕜 : Type u_5<VAR>inst✝⁸ : RCLike 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>p : ℝ≥0∞<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : CompleteSpace F<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>L : E →L[𝕜] F<VAR>φ : X → E<VAR>φ_int : Integrable φ μ<GOAL>∀ ⦃f g : X → E⦄, Disjoint (support f) (support g) → Integrable f μ → Integrable g μ → (fun φ => ∫ (x : X), L (φ x) ∂μ = L (∫ (x : X), φ x ∂μ)) f → (fun φ => ∫ (x : X), L (φ x) ∂μ = L (∫ (x : X), φ x ∂μ)) g → (fun φ => ∫ (x : X), L (φ x) ∂μ = L (∫ (x : X), φ x ∂μ)) (f + g)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁹ : MeasurableSpace X<VAR>μ : Measure X<VAR>𝕜 : Type u_5<VAR>inst✝⁸ : RCLike 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>p : ℝ≥0∞<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : CompleteSpace F<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>L : E →L[𝕜] F<VAR>φ : X → E<VAR>φ_int : Integrable φ μ<GOAL>IsClosed {f | (fun φ => ∫ (x : X), L (φ x) ∂μ = L (∫ (x : X), φ x ∂μ)) ↑↑f}