ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁸ : CommRing R₁<VAR>inst✝⁷ : AddCommGroup M₁<VAR>inst✝⁶ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M₂' : Type u_7<VAR>inst✝² : AddCommMonoid M₂'<VAR>inst✝¹ : Module R M₂'<VAR>n : Type w<VAR>inst✝ : Nontrivial R<VAR>B : BilinForm R M<VAR>v : Basis n R M<VAR>h : B.iIsOrtho ⇑v<VAR>hB : B.Nondegenerate<VAR>i : n<VAR>ho : B.IsOrtho (v i) (v i)<VAR>m : M<GOAL>(B (v i)) m = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁸ : CommRing R₁<VAR>inst✝⁷ : AddCommGroup M₁<VAR>inst✝⁶ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M₂' : Type u_7<VAR>inst✝² : AddCommMonoid M₂'<VAR>inst✝¹ : Module R M₂'<VAR>n : Type w<VAR>inst✝ : Nontrivial R<VAR>B : BilinForm R M<VAR>v : Basis n R M<VAR>h : B.iIsOrtho ⇑v<VAR>hB : B.Nondegenerate<VAR>i : n<VAR>ho : B.IsOrtho (v i) (v i)<VAR>vi : n →₀ R<GOAL>(B (v i)) (v.repr.symm vi) = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁸ : CommRing R₁<VAR>inst✝⁷ : AddCommGroup M₁<VAR>inst✝⁶ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M₂' : Type u_7<VAR>inst✝² : AddCommMonoid M₂'<VAR>inst✝¹ : Module R M₂'<VAR>n : Type w<VAR>inst✝ : Nontrivial R<VAR>B : BilinForm R M<VAR>v : Basis n R M<VAR>h : B.iIsOrtho ⇑v<VAR>hB : B.Nondegenerate<VAR>i : n<VAR>ho : B.IsOrtho (v i) (v i)<VAR>vi : n →₀ R<GOAL>∑ i_1 ∈ vi.support, (B (v i)) (vi i_1 • v i_1) = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁸ : CommRing R₁<VAR>inst✝⁷ : AddCommGroup M₁<VAR>inst✝⁶ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M₂' : Type u_7<VAR>inst✝² : AddCommMonoid M₂'<VAR>inst✝¹ : Module R M₂'<VAR>n : Type w<VAR>inst✝ : Nontrivial R<VAR>B : BilinForm R M<VAR>v : Basis n R M<VAR>h : B.iIsOrtho ⇑v<VAR>hB : B.Nondegenerate<VAR>i : n<VAR>ho : B.IsOrtho (v i) (v i)<VAR>vi : n →₀ R<GOAL>∀ x ∈ vi.support, (B (v i)) (vi x • v x) = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁸ : CommRing R₁<VAR>inst✝⁷ : AddCommGroup M₁<VAR>inst✝⁶ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M₂' : Type u_7<VAR>inst✝² : AddCommMonoid M₂'<VAR>inst✝¹ : Module R M₂'<VAR>n : Type w<VAR>inst✝ : Nontrivial R<VAR>B : BilinForm R M<VAR>v : Basis n R M<VAR>h : B.iIsOrtho ⇑v<VAR>hB : B.Nondegenerate<VAR>i : n<VAR>ho : B.IsOrtho (v i) (v i)<VAR>vi : n →₀ R<VAR>j : n<GOAL>(B (v i)) (vi j • v j) = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁸ : CommRing R₁<VAR>inst✝⁷ : AddCommGroup M₁<VAR>inst✝⁶ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M₂' : Type u_7<VAR>inst✝² : AddCommMonoid M₂'<VAR>inst✝¹ : Module R M₂'<VAR>n : Type w<VAR>inst✝ : Nontrivial R<VAR>B : BilinForm R M<VAR>v : Basis n R M<VAR>h : B.iIsOrtho ⇑v<VAR>hB : B.Nondegenerate<VAR>i : n<VAR>ho : B.IsOrtho (v i) (v i)<VAR>vi : n →₀ R<VAR>j : n<GOAL>vi j * (B (v i)) (v j) = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁸ : CommRing R₁<VAR>inst✝⁷ : AddCommGroup M₁<VAR>inst✝⁶ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M₂' : Type u_7<VAR>inst✝² : AddCommMonoid M₂'<VAR>inst✝¹ : Module R M₂'<VAR>n : Type w<VAR>inst✝ : Nontrivial R<VAR>B : BilinForm R M<VAR>v : Basis n R M<VAR>h : B.iIsOrtho ⇑v<VAR>hB : B.Nondegenerate<VAR>i : n<VAR>ho : B.IsOrtho (v i) (v i)<VAR>vi : n →₀ R<VAR>j : n<GOAL>(B (v i)) (v j) = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁸ : CommRing R₁<VAR>inst✝⁷ : AddCommGroup M₁<VAR>inst✝⁶ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M₂' : Type u_7<VAR>inst✝² : AddCommMonoid M₂'<VAR>inst✝¹ : Module R M₂'<VAR>n : Type w<VAR>inst✝ : Nontrivial R<VAR>B : BilinForm R M<VAR>v : Basis n R M<VAR>h : B.iIsOrtho ⇑v<VAR>hB : B.Nondegenerate<VAR>i : n<VAR>ho : B.IsOrtho (v i) (v i)<VAR>vi : n →₀ R<GOAL>(B (v i)) (v i) = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : Module R M<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝⁸ : CommRing R₁<VAR>inst✝⁷ : AddCommGroup M₁<VAR>inst✝⁶ : Module R₁ M₁<VAR>V : Type u_5<VAR>K : Type u_6<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>B✝ : BilinForm R M<VAR>B₁ : BilinForm R₁ M₁<VAR>M₂' : Type u_7<VAR>inst✝² : AddCommMonoid M₂'<VAR>inst✝¹ : Module R M₂'<VAR>n : Type w<VAR>inst✝ : Nontrivial R<VAR>B : BilinForm R M<VAR>v : Basis n R M<VAR>h : B.iIsOrtho ⇑v<VAR>hB : B.Nondegenerate<VAR>i : n<VAR>ho : B.IsOrtho (v i) (v i)<VAR>vi : n →₀ R<VAR>j : n<VAR>hij : i ≠ j<GOAL>(B (v i)) (v j) = 0
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝³ : Fintype m<VAR>inst✝² : Fintype n<VAR>inst✝¹ : AddCommMonoid α<VAR>inst✝ : CommSemigroup α<VAR>v w : m → α<GOAL>v ⬝ᵥ w = w ⬝ᵥ v
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝¹ : NormedAddCommGroup E<VAR>f : ℝ → E<VAR>a b : ℝ<VAR>μ : Measure ℝ<VAR>inst✝ : NoAtoms μ<VAR>hab : a ≤ b<GOAL>IntervalIntegrable f μ a b ↔ IntegrableOn f (Ico a b) μ
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>w₁ : InfinitePlace K<VAR>B : ℕ<VAR>hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B<VAR>x : 𝓞 K<VAR>hx : x ≠ 0<GOAL>∃ y, y ≠ 0 ∧ (∀ (w : InfinitePlace K), w ≠ w₁ → w ↑y < w ↑x) ∧ |(Algebra.norm ℚ) ↑y| ≤ ↑B
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>w₁ : InfinitePlace K<VAR>B : ℕ<VAR>hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B<VAR>x : 𝓞 K<VAR>hx : x ≠ 0<VAR>hx' : (algebraMap (𝓞 K) K) x ≠ 0<GOAL>∃ y, y ≠ 0 ∧ (∀ (w : InfinitePlace K), w ≠ w₁ → w ↑y < w ↑x) ∧ |(Algebra.norm ℚ) ↑y| ≤ ↑B
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>w₁ : InfinitePlace K<VAR>B : ℕ<VAR>hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B<VAR>x : 𝓞 K<VAR>hx : x ≠ 0<VAR>hx' : (algebraMap (𝓞 K) K) x ≠ 0<VAR>f : InfinitePlace K → ℝ≥0 := fun w => ⟨w ↑x / 2, ⋯⟩<GOAL>∃ y, y ≠ 0 ∧ (∀ (w : InfinitePlace K), w ≠ w₁ → w ↑y < w ↑x) ∧ |(Algebra.norm ℚ) ↑y| ≤ ↑B
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>w₁ : InfinitePlace K<VAR>B : ℕ<VAR>hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B<VAR>x : 𝓞 K<VAR>hx : x ≠ 0<VAR>hx' : (algebraMap (𝓞 K) K) x ≠ 0<VAR>f : InfinitePlace K → ℝ≥0 := fun w => ⟨w ↑x / 2, ⋯⟩<VAR>w✝ : InfinitePlace K<VAR>a✝ : w✝ ≠ w₁<GOAL>f w✝ ≠ 0
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>w₁ : InfinitePlace K<VAR>B : ℕ<VAR>hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B<VAR>x : 𝓞 K<VAR>hx : x ≠ 0<VAR>hx' : (algebraMap (𝓞 K) K) x ≠ 0<VAR>f : InfinitePlace K → ℝ≥0 := fun w => ⟨w ↑x / 2, ⋯⟩<VAR>w✝ : InfinitePlace K<VAR>a✝ : w✝ ≠ w₁<GOAL>¬↑x = 0 ∧ ¬2 = 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedCoheytingAlgebra α<VAR>a b c d : α<GOAL>(a \ b) ∆ b = a ⊔ b
<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✝⁴ : S₂.HasHomology<VAR>inst✝³ : (S₁.map F).HasHomology<VAR>inst✝² : (S₂.map F).HasHomology<VAR>inst✝¹ : F.PreservesLeftHomologyOf S₁<VAR>inst✝ : F.PreservesLeftHomologyOf S₂<GOAL>leftHomologyMap' (F.mapShortComplex.map φ) (S₁.map F).homologyData.left (S₂.map F).homologyData.left ≫ leftHomologyMap' (𝟙 (S₂.map F)) (S₂.map F).homologyData.left (S₂.map F).leftHomologyData ≫ leftHomologyMap' (𝟙 (S₂.map F)) (S₂.map F).leftHomologyData (S₂.homologyData.left.map F) = (leftHomologyMap' (𝟙 (S₁.map F)) (S₁.map F).homologyData.left (S₁.map F).leftHomologyData ≫ leftHomologyMap' (𝟙 (S₁.map F)) (S₁.map F).leftHomologyData (S₁.homologyData.left.map F)) ≫ F.map (leftHomologyMap' φ S₁.homologyData.left S₂.homologyData.left)
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : DiscreteValuationRing R<VAR>p q : R<VAR>hp : Irreducible p<VAR>hq : Irreducible q<VAR>u v : Rˣ<VAR>m n : ℕ<VAR>h : ↑u * p ^ m = ↑v * q ^ n<GOAL>m = n
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : DiscreteValuationRing R<VAR>p q : R<VAR>hp : Irreducible p<VAR>hq : Irreducible q<VAR>u v : Rˣ<VAR>m n : ℕ<VAR>h : ↑u * p ^ m = ↑v * q ^ n<VAR>key : Associated (Multiset.replicate m p).prod (Multiset.replicate n q).prod<GOAL>m = n
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : DiscreteValuationRing R<VAR>p q : R<VAR>hp : Irreducible p<VAR>hq : Irreducible q<VAR>u v : Rˣ<VAR>m n : ℕ<VAR>h : ↑u * p ^ m = ↑v * q ^ n<VAR>key : Associated (Multiset.replicate m p).prod (Multiset.replicate n q).prod<VAR>this : Multiset.card (Multiset.replicate m p) = Multiset.card (Multiset.replicate n q)<GOAL>m = n
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>f : ℕ → ℕ<VAR>hf : Bijective f<VAR>u : ℕ → α<GOAL>CauchySeq (u ∘ f) ↔ CauchySeq u
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>f : ℕ → ℕ<VAR>hf : Bijective f<VAR>u : ℕ → α<VAR>H : CauchySeq (u ∘ f)<GOAL>CauchySeq u
<VAR>b : ℝ<VAR>hb : 1 < b<GOAL>Tendsto (fun x => b ^ x) atBot (𝓝 0)
<VAR>b : ℝ<VAR>hb : 1 < b<GOAL>Tendsto (fun x => rexp (log b * x)) atBot (𝓝 0)
<VAR>b : ℝ<VAR>hb : 1 < b<GOAL>0 < log b
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>A : Type ?u.16903<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace A<VAR>f : X → Y<GOAL>IsLocallyInjective f ↔ OpenEmbedding (toPullbackDiag f)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>A : Type ?u.16903<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace A<VAR>f : X → Y<GOAL>IsOpen (Set.range (toPullbackDiag f)) ↔ OpenEmbedding (toPullbackDiag f)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>S : Set (Set X)<VAR>hS : S.Finite<GOAL>interior (⋂₀ S) = ⋂ s ∈ S, interior s
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝ : (i : ι) → MeasurableSpace (α i)<VAR>P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)<VAR>I✝ J✝ : Finset ι<VAR>hP : IsProjectiveMeasureFamily P<VAR>I J : Finset ι<GOAL>(P I) univ = (P J) univ
<GOAL>ContinuousOn tan {x | cos x ≠ 0}
<GOAL>ContinuousOn (fun x => sin x / cos x) {x | cos x ≠ 0}
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>inst✝⁸ : NontriviallyNormedField R<VAR>inst✝⁷ : (x : B) → AddCommMonoid (E x)<VAR>inst✝⁶ : (x : B) → Module R (E x)<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace R F<VAR>inst✝³ : TopologicalSpace B<VAR>inst✝² : TopologicalSpace (TotalSpace F E)<VAR>inst✝¹ : (x : B) → TopologicalSpace (E x)<VAR>inst✝ : FiberBundle F E<VAR>ι : Type u_5<VAR>Z : VectorBundleCore R B F ι<VAR>b✝ : B<VAR>a : F<VAR>i j : ι<VAR>b : B<VAR>hb : b ∈ Z.baseSet i<VAR>v : F<GOAL>(Trivialization.symmL R (Z.localTriv i) b) v = (Z.coordChange i (Z.indexAt b) b) v
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>inst✝⁸ : NontriviallyNormedField R<VAR>inst✝⁷ : (x : B) → AddCommMonoid (E x)<VAR>inst✝⁶ : (x : B) → Module R (E x)<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace R F<VAR>inst✝³ : TopologicalSpace B<VAR>inst✝² : TopologicalSpace (TotalSpace F E)<VAR>inst✝¹ : (x : B) → TopologicalSpace (E x)<VAR>inst✝ : FiberBundle F E<VAR>ι : Type u_5<VAR>Z : VectorBundleCore R B F ι<VAR>b✝ : B<VAR>a : F<VAR>i j : ι<VAR>b : B<VAR>hb : b ∈ Z.baseSet i<VAR>v : F<GOAL>cast ⋯ (↑(Z.localTriv i).symm (b, v)).snd = (Z.coordChange i (Z.indexAt b) b) v
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>inst✝⁸ : NontriviallyNormedField R<VAR>inst✝⁷ : (x : B) → AddCommMonoid (E x)<VAR>inst✝⁶ : (x : B) → Module R (E x)<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace R F<VAR>inst✝³ : TopologicalSpace B<VAR>inst✝² : TopologicalSpace (TotalSpace F E)<VAR>inst✝¹ : (x : B) → TopologicalSpace (E x)<VAR>inst✝ : FiberBundle F E<VAR>ι : Type u_5<VAR>Z : VectorBundleCore R B F ι<VAR>b✝ : B<VAR>a : F<VAR>i j : ι<VAR>b : B<VAR>hb : b ∈ Z.baseSet i<VAR>v : F<GOAL>b ∈ (Z.localTriv i).baseSet
<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>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace α'<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace β'<VAR>inst✝³ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : SFinite ν<VAR>inst✝ : SFinite μ<VAR>s : Set α<VAR>t : Set β<GOAL>(μ.restrict s).prod (ν.restrict t) = (μ.prod ν).restrict (s ×ˢ t)
<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>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace α'<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace β'<VAR>inst✝³ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : SFinite ν<VAR>inst✝ : SFinite μ<VAR>s : Set α<VAR>t : Set β<GOAL>(sum fun p => ((sFiniteSeq μ p.1).restrict s).prod ((sFiniteSeq ν p.2).restrict t)) = sum fun i => ((sFiniteSeq μ i.1).prod (sFiniteSeq ν i.2)).restrict (s ×ˢ t)
<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>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace α'<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace β'<VAR>inst✝³ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : SFinite ν<VAR>inst✝ : SFinite μ<VAR>s : Set α<VAR>t : Set β<VAR>i : ℕ × ℕ<GOAL>((sFiniteSeq μ i.1).restrict s).prod ((sFiniteSeq ν i.2).restrict t) = ((sFiniteSeq μ i.1).prod (sFiniteSeq ν i.2)).restrict (s ×ˢ t)
<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>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace α'<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace β'<VAR>inst✝³ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : SFinite ν<VAR>inst✝ : SFinite μ<VAR>s : Set α<VAR>t : Set β<VAR>i : ℕ × ℕ<VAR>s' : Set α<VAR>t' : Set β<VAR>hs' : MeasurableSet s'<VAR>ht' : MeasurableSet t'<GOAL>(((sFiniteSeq μ i.1).prod (sFiniteSeq ν i.2)).restrict (s ×ˢ t)) (s' ×ˢ t') = ((sFiniteSeq μ i.1).restrict s) s' * ((sFiniteSeq ν i.2).restrict t) t'
<VAR>R✝ : Type u<VAR>ι✝ : Type u_1<VAR>inst✝² : CommSemiring R✝<VAR>I✝ J K L : Ideal R✝<VAR>R : Type u_2<VAR>inst✝¹ : CommRing R<VAR>ι : Type u_3<VAR>inst✝ : Fintype ι<VAR>I : ι → ℕ<VAR>hI : Pairwise fun i j => (I i).Coprime (I j)<GOAL>⨅ i, span {↑(I i)} = span {↑(∏ i : ι, I i)}
<VAR>R✝ : Type u<VAR>ι✝ : Type u_1<VAR>inst✝² : CommSemiring R✝<VAR>I✝ J K L : Ideal R✝<VAR>R : Type u_2<VAR>inst✝¹ : CommRing R<VAR>ι : Type u_3<VAR>inst✝ : Fintype ι<VAR>I : ι → ℕ<VAR>hI : Pairwise fun i j => (I i).Coprime (I j)<GOAL>∀ (i j : ι), i ≠ j → IsCoprime ↑(I i) ↑(I j)
<GOAL>∀ᵐ (x : ℝ), ∀ p > 2, ¬LiouvilleWith p x
<VAR>x y : ℝ<GOAL>cos (3 * x) = 4 * cos x ^ 3 - 3 * cos x
<VAR>x y : ℝ<GOAL>↑(cos (3 * x)) = ↑(4 * cos x ^ 3 - 3 * cos x)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>A✝ : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} A✝<VAR>J : GrothendieckTopology C<VAR>A : Type u₂<VAR>inst✝ : Category.{v₂, u₂} A<VAR>E : A<VAR>X : C<VAR>P : Cᵒᵖ ⥤ A<VAR>hP : IsSheaf J P<VAR>S : J.Cover X<VAR>x : (I : S.Arrow) → E ⟶ P.obj (op I.Y)<VAR>hx : ∀ ⦃I₁ I₂ : S.Arrow⦄ (r : I₁.Relation I₂), x I₁ ≫ P.map r.g₁.op = x I₂ ≫ P.map r.g₂.op<VAR>I : S.Arrow<GOAL>hP.amalgamate S x hx ≫ P.map I.f.op = x I
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>inst✝²³ : NontriviallyNormedField 𝕜<VAR>EB : Type u_7<VAR>inst✝²² : NormedAddCommGroup EB<VAR>inst✝²¹ : NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>inst✝²⁰ : TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>inst✝¹⁹ : TopologicalSpace B<VAR>inst✝¹⁸ : ChartedSpace HB B<VAR>inst✝¹⁷ : SmoothManifoldWithCorners IB B<VAR>EM : Type u_9<VAR>inst✝¹⁶ : NormedAddCommGroup EM<VAR>inst✝¹⁵ : NormedSpace 𝕜 EM<VAR>HM : Type u_10<VAR>inst✝¹⁴ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>inst✝¹³ : TopologicalSpace M<VAR>inst✝¹² : ChartedSpace HM M<VAR>Is : SmoothManifoldWithCorners IM M<VAR>n : ℕ∞<VAR>inst✝¹¹ : (x : B) → AddCommMonoid (E x)<VAR>inst✝¹⁰ : (x : B) → Module 𝕜 (E x)<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>inst✝⁷ : TopologicalSpace (TotalSpace F E)<VAR>inst✝⁶ : (x : B) → TopologicalSpace (E x)<VAR>inst✝⁵ : FiberBundle F E<VAR>inst✝⁴ : VectorBundle 𝕜 F E<VAR>inst✝³ : SmoothVectorBundle F E IB<VAR>e✝ e' : Trivialization F TotalSpace.proj<VAR>inst✝² : MemTrivializationAtlas e✝<VAR>inst✝¹ : MemTrivializationAtlas e'<VAR>e : Trivialization F TotalSpace.proj<VAR>inst✝ : MemTrivializationAtlas e<GOAL>SmoothOn (IB.prod 𝓘(𝕜, F)) (IB.prod 𝓘(𝕜, F)) (↑e.symm) e.target
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>inst✝²³ : NontriviallyNormedField 𝕜<VAR>EB : Type u_7<VAR>inst✝²² : NormedAddCommGroup EB<VAR>inst✝²¹ : NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>inst✝²⁰ : TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>inst✝¹⁹ : TopologicalSpace B<VAR>inst✝¹⁸ : ChartedSpace HB B<VAR>inst✝¹⁷ : SmoothManifoldWithCorners IB B<VAR>EM : Type u_9<VAR>inst✝¹⁶ : NormedAddCommGroup EM<VAR>inst✝¹⁵ : NormedSpace 𝕜 EM<VAR>HM : Type u_10<VAR>inst✝¹⁴ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>inst✝¹³ : TopologicalSpace M<VAR>inst✝¹² : ChartedSpace HM M<VAR>Is : SmoothManifoldWithCorners IM M<VAR>n : ℕ∞<VAR>inst✝¹¹ : (x : B) → AddCommMonoid (E x)<VAR>inst✝¹⁰ : (x : B) → Module 𝕜 (E x)<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>inst✝⁷ : TopologicalSpace (TotalSpace F E)<VAR>inst✝⁶ : (x : B) → TopologicalSpace (E x)<VAR>inst✝⁵ : FiberBundle F E<VAR>inst✝⁴ : VectorBundle 𝕜 F E<VAR>inst✝³ : SmoothVectorBundle F E IB<VAR>e✝ e' : Trivialization F TotalSpace.proj<VAR>inst✝² : MemTrivializationAtlas e✝<VAR>inst✝¹ : MemTrivializationAtlas e'<VAR>e : Trivialization F TotalSpace.proj<VAR>inst✝ : MemTrivializationAtlas e<GOAL>SmoothOn (IB.prod 𝓘(𝕜, F)) IB (fun x => (↑e.symm x).proj) e.target ∧ SmoothOn (IB.prod 𝓘(𝕜, F)) 𝓘(𝕜, F) (fun x => (↑e (↑e.symm x)).2) e.target
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>inst✝²³ : NontriviallyNormedField 𝕜<VAR>EB : Type u_7<VAR>inst✝²² : NormedAddCommGroup EB<VAR>inst✝²¹ : NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>inst✝²⁰ : TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>inst✝¹⁹ : TopologicalSpace B<VAR>inst✝¹⁸ : ChartedSpace HB B<VAR>inst✝¹⁷ : SmoothManifoldWithCorners IB B<VAR>EM : Type u_9<VAR>inst✝¹⁶ : NormedAddCommGroup EM<VAR>inst✝¹⁵ : NormedSpace 𝕜 EM<VAR>HM : Type u_10<VAR>inst✝¹⁴ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>inst✝¹³ : TopologicalSpace M<VAR>inst✝¹² : ChartedSpace HM M<VAR>Is : SmoothManifoldWithCorners IM M<VAR>n : ℕ∞<VAR>inst✝¹¹ : (x : B) → AddCommMonoid (E x)<VAR>inst✝¹⁰ : (x : B) → Module 𝕜 (E x)<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>inst✝⁷ : TopologicalSpace (TotalSpace F E)<VAR>inst✝⁶ : (x : B) → TopologicalSpace (E x)<VAR>inst✝⁵ : FiberBundle F E<VAR>inst✝⁴ : VectorBundle 𝕜 F E<VAR>inst✝³ : SmoothVectorBundle F E IB<VAR>e✝ e' : Trivialization F TotalSpace.proj<VAR>inst✝² : MemTrivializationAtlas e✝<VAR>inst✝¹ : MemTrivializationAtlas e'<VAR>e : Trivialization F TotalSpace.proj<VAR>inst✝ : MemTrivializationAtlas e<VAR>x : B × F<VAR>hx : x ∈ e.target<GOAL>(↑e (↑e.symm x)).2 = x.2
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X : C<VAR>inst✝ : HasBinaryProducts C<VAR>A : (prodComonad X).Coalgebra<GOAL>(((𝟭 (prodComonad X).Coalgebra).obj A).a ≫ (prodComonad X).map (Iso.refl ((𝟭 (prodComonad X).Coalgebra).obj A).A).hom) ≫ prod.snd = ((Iso.refl ((𝟭 (prodComonad X).Coalgebra).obj A).A).hom ≫ ((coalgebraToOver X ⋙ overToCoalgebra X).obj A).a) ≫ prod.snd
<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>(o.kahler (o.rightAngleRotation x)) y = -Complex.I * (o.kahler x) y
<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>↑((o.areaForm x) y) + -↑⟪x, y⟫_ℝ * Complex.I = -Complex.I * (↑⟪x, y⟫_ℝ + ↑((o.areaForm x) y) * Complex.I)
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝¹ s₁ s₂ : Finset α<VAR>a✝ : α<VAR>f g : α → β<VAR>inst✝ : DecidableEq β<VAR>s✝ : Finset α<VAR>t : α → Finset β<VAR>this : DecidableEq α<VAR>a : α<VAR>s : Finset α<VAR>has : a ∉ s<VAR>ih : (s.biUnion t).card ≤ ∑ a ∈ s, (t a).card<GOAL>((insert a s).biUnion t).card ≤ (t a).card + (s.biUnion t).card
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝¹ s₁ s₂ : Finset α<VAR>a✝ : α<VAR>f g : α → β<VAR>inst✝ : DecidableEq β<VAR>s✝ : Finset α<VAR>t : α → Finset β<VAR>this : DecidableEq α<VAR>a : α<VAR>s : Finset α<VAR>has : a ∉ s<VAR>ih : (s.biUnion t).card ≤ ∑ a ∈ s, (t a).card<GOAL>(t a ∪ s.biUnion t).card ≤ (t a).card + (s.biUnion t).card
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝¹ s₁ s₂ : Finset α<VAR>a✝ : α<VAR>f g : α → β<VAR>inst✝ : DecidableEq β<VAR>s✝ : Finset α<VAR>t : α → Finset β<VAR>this : DecidableEq α<VAR>a : α<VAR>s : Finset α<VAR>has : a ∉ s<VAR>ih : (s.biUnion t).card ≤ ∑ a ∈ s, (t a).card<GOAL>(t a).card + (s.biUnion t).card ≤ ∑ a ∈ insert a s, (t a).card
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝¹ s₁ s₂ : Finset α<VAR>a✝ : α<VAR>f g : α → β<VAR>inst✝ : DecidableEq β<VAR>s✝ : Finset α<VAR>t : α → Finset β<VAR>this : DecidableEq α<VAR>a : α<VAR>s : Finset α<VAR>has : a ∉ s<VAR>ih : (s.biUnion t).card ≤ ∑ a ∈ s, (t a).card<GOAL>(t a).card + (s.biUnion t).card ≤ (t a).card + ∑ x ∈ s, (t x).card