ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>M : Type u_4<VAR>inst✝¹¹ : CommSemiring R<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : Semiring A<VAR>inst✝⁷ : Semiring B<VAR>inst✝⁶ : Module A M<VAR>inst✝⁵ : Module B M<VAR>inst✝⁴ : Algebra R A<VAR>inst✝³ : Algebra R B<VAR>inst✝² : IsScalarTower R A M<VAR>inst✝¹ : IsScalarTower R B M<VAR>inst✝ : SMulCommClass A B M<VAR>p : Submodule (A ⊗[R] B) M<VAR>b : B<VAR>m : M<VAR>hm : m ∈ p<GOAL>b • m = 1 ⊗ₜ[R] b • m
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : L.Structure M<VAR>inst✝³ : L.Structure N<VAR>inst✝² : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n : ℕ<VAR>T✝ : L.Theory<VAR>inst✝¹ : L'.Structure M<VAR>φ : L →ᴸ L'<VAR>inst✝ : φ.IsExpansionOn M<VAR>T : L.Theory<GOAL>M ⊨ φ.onTheory T ↔ M ⊨ T
<VAR>S : Type u_1<VAR>inst✝² : CommRing S<VAR>inst✝¹ : IsDomain S<VAR>P : Ideal S<VAR>P_prime : P.IsPrime<VAR>hP : P ≠ ⊥<VAR>inst✝ : IsDedekindDomain S<VAR>i : ℕ<VAR>a c : S<VAR>a_mem : a ∈ P ^ i<VAR>a_not_mem : a ∉ P ^ (i + 1)<VAR>c_mem : c ∈ P ^ i<GOAL>∃ d, ∃ e ∈ P ^ (i + 1), a * d + e = c
<VAR>S : Type u_1<VAR>inst✝² : CommRing S<VAR>inst✝¹ : IsDomain S<VAR>P : Ideal S<VAR>P_prime : P.IsPrime<VAR>hP : P ≠ ⊥<VAR>inst✝ : IsDedekindDomain S<VAR>i : ℕ<VAR>a c : S<VAR>a_mem : a ∈ P ^ i<VAR>a_not_mem : a ∉ P ^ (i + 1)<VAR>c_mem : c ∈ P ^ i<GOAL>P ^ i = span {a} ⊔ P ^ (i + 1)
<VAR>S : Type u_1<VAR>inst✝² : CommRing S<VAR>inst✝¹ : IsDomain S<VAR>P : Ideal S<VAR>P_prime : P.IsPrime<VAR>hP : P ≠ ⊥<VAR>inst✝ : IsDedekindDomain S<VAR>i : ℕ<VAR>a c : S<VAR>a_mem : a ∈ P ^ i<VAR>a_not_mem : a ∉ P ^ (i + 1)<VAR>c_mem : c ∈ P ^ i<GOAL>P ^ (i + 1) ≠ span {a} ⊔ P ^ (i + 1)
<VAR>S : Type u_1<VAR>inst✝² : CommRing S<VAR>inst✝¹ : IsDomain S<VAR>P : Ideal S<VAR>P_prime : P.IsPrime<VAR>hP : P ≠ ⊥<VAR>inst✝ : IsDedekindDomain S<VAR>i : ℕ<VAR>a c : S<VAR>a_mem : a ∈ P ^ i<VAR>c_mem : c ∈ P ^ i<VAR>this : P ^ (i + 1) = span {a} ⊔ P ^ (i + 1)<GOAL>a ∈ P ^ (i + 1)
<VAR>S : Type u_1<VAR>inst✝² : CommRing S<VAR>inst✝¹ : IsDomain S<VAR>P : Ideal S<VAR>P_prime : P.IsPrime<VAR>hP : P ≠ ⊥<VAR>inst✝ : IsDedekindDomain S<VAR>i : ℕ<VAR>a c : S<VAR>a_mem : a ∈ P ^ i<VAR>c_mem : c ∈ P ^ i<VAR>this : P ^ (i + 1) = span {a} ⊔ P ^ (i + 1)<GOAL>a ∈ span {a} ⊔ P ^ (i + 1)
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>ht : t ∈ 𝓝 x<GOAL>fderivWithin 𝕜 f (s ∩ t) x = fderivWithin 𝕜 f s x
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>ht : t ∈ 𝓝 x<VAR>A : 𝓝[(s ∩ t) \ {x}] x = 𝓝[s \ {x}] x<GOAL>fderivWithin 𝕜 f (s ∩ t) x = fderivWithin 𝕜 f s x
<VAR>𝕜 : Type u_1<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>f✝ : E → F<VAR>K : Set (E →L[𝕜] F)<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : OpensMeasurableSpace E<VAR>inst✝² : CompleteSpace F<VAR>inst✝¹ : MeasurableSpace 𝕜<VAR>inst✝ : OpensMeasurableSpace 𝕜<VAR>h : SecondCountableTopologyEither 𝕜 F<VAR>f : 𝕜 → F<VAR>this✝¹ : MeasurableSpace F := borel F<VAR>this✝ : BorelSpace F<GOAL>StronglyMeasurable (deriv f)
<VAR>𝕜 : Type u_1<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>f✝ : E → F<VAR>K : Set (E →L[𝕜] F)<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : OpensMeasurableSpace E<VAR>inst✝² : CompleteSpace F<VAR>inst✝¹ : MeasurableSpace 𝕜<VAR>inst✝ : OpensMeasurableSpace 𝕜<VAR>h : SecondCountableTopologyEither 𝕜 F<VAR>f : 𝕜 → F<VAR>this✝¹ : MeasurableSpace F := borel F<VAR>this✝ : BorelSpace F<VAR>h𝕜 : SecondCountableTopology 𝕜<GOAL>StronglyMeasurable (deriv f)
<VAR>𝕜 : Type u_1<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>f✝ : E → F<VAR>K : Set (E →L[𝕜] F)<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : OpensMeasurableSpace E<VAR>inst✝² : CompleteSpace F<VAR>inst✝¹ : MeasurableSpace 𝕜<VAR>inst✝ : OpensMeasurableSpace 𝕜<VAR>h : SecondCountableTopologyEither 𝕜 F<VAR>f : 𝕜 → F<VAR>this✝¹ : MeasurableSpace F := borel F<VAR>this✝ : BorelSpace F<VAR>hF : SecondCountableTopology F<GOAL>StronglyMeasurable (deriv f)
<VAR>A : Type u_1<VAR>inst✝³ : AddCommGroup A<VAR>inst✝² : Module ℂ A<VAR>inst✝¹ : StarAddMonoid A<VAR>inst✝ : StarModule ℂ A<GOAL>span ℂ ↑(selfAdjoint A) = ⊤
<VAR>A : Type u_1<VAR>inst✝³ : AddCommGroup A<VAR>inst✝² : Module ℂ A<VAR>inst✝¹ : StarAddMonoid A<VAR>inst✝ : StarModule ℂ A<VAR>x : A<GOAL>x ∈ span ℂ ↑(selfAdjoint A)
<VAR>A : Type u_1<VAR>inst✝³ : AddCommGroup A<VAR>inst✝² : Module ℂ A<VAR>inst✝¹ : StarAddMonoid A<VAR>inst✝ : StarModule ℂ A<VAR>x : A<GOAL>↑(ℜ x) + I • ↑(ℑ x) ∈ span ℂ ↑(selfAdjoint A)
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>op : α → α → α<VAR>ha : Std.Associative op<VAR>hc : Std.Commutative op<VAR>l : List α<VAR>a₁ a₂ : α<GOAL>((a₁ :: l) <*> a₂) = op a₁ (l <*> a₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>inst✝² : One M<VAR>inst✝¹ : One N<VAR>inst✝ : One P<VAR>f : α → M<GOAL>range f ⊆ insert 1 (f '' mulSupport f)
<VAR>G : Type u_1<VAR>inst✝² : CommGroup G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<GOAL>UniformGroup G
<VAR>G : Type u_1<VAR>inst✝² : CommGroup G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>this : Tendsto ((fun p => p.1 / p.2) ∘ fun p => (p.1.2 / p.1.1, p.2.2 / p.2.1)) (comap (fun p => (p.1.2 / p.1.1, p.2.2 / p.2.1)) ((𝓝 1).prod (𝓝 1))) (𝓝 (1 / 1))<GOAL>UniformGroup G
<VAR>G : Type u_1<VAR>inst✝² : CommGroup G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>this : Tendsto ((fun p => p.1 / p.2) ∘ fun p => (p.1.2 / p.1.1, p.2.2 / p.2.1)) (comap (fun p => (p.1.2 / p.1.1, p.2.2 / p.2.1)) ((𝓝 1).prod (𝓝 1))) (𝓝 (1 / 1))<GOAL>UniformContinuous fun p => p.1 / p.2
<VAR>G : Type u_1<VAR>inst✝² : CommGroup G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>this : Tendsto ((fun p => p.1 / p.2) ∘ fun p => (p.1.2 / p.1.1, p.2.2 / p.2.1)) (comap (fun p => (p.1.2 / p.1.1, p.2.2 / p.2.1)) ((𝓝 1).prod (𝓝 1))) (𝓝 (1 / 1))<GOAL>Tendsto ((fun p => p.2 / p.1) ∘ (fun x => (x.1.1 / x.1.2, x.2.1 / x.2.2)) ∘ fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) (comap (fun p => (p.1.2 / p.1.1, p.2.2 / p.2.1)) (𝓝 1 ×ˢ 𝓝 1)) (𝓝 1)
<VAR>G : Type u_1<VAR>inst✝² : CommGroup G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>this : Tendsto (fun x => x.2.1 * (x.1.2 * x.1.1⁻¹ * x.2.2⁻¹)) (comap (fun p => (p.1.2 * p.1.1⁻¹, p.2.2 * p.2.1⁻¹)) ((𝓝 1).prod (𝓝 1))) (𝓝 (1 * 1⁻¹))<GOAL>Tendsto (fun x => x.1.2 * (x.2.1 * x.1.1⁻¹ * x.2.2⁻¹)) (comap (fun p => (p.1.2 * p.1.1⁻¹, p.2.2 * p.2.1⁻¹)) (𝓝 1 ×ˢ 𝓝 1)) (𝓝 1)
<VAR>G : Type u_1<VAR>inst✝² : CommGroup G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>this : Tendsto (fun x => x.2.1 * x.1.2 * x.1.1⁻¹ * x.2.2⁻¹) (comap (fun p => (p.1.2 * p.1.1⁻¹, p.2.2 * p.2.1⁻¹)) ((𝓝 1).prod (𝓝 1))) (𝓝 1)<GOAL>Tendsto (fun x => x.1.2 * (x.2.1 * x.1.1⁻¹ * x.2.2⁻¹)) (comap (fun p => (p.1.2 * p.1.1⁻¹, p.2.2 * p.2.1⁻¹)) (𝓝 1 ×ˢ 𝓝 1)) (𝓝 1)
<VAR>G : Type u_1<VAR>inst✝² : CommGroup G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>this : Tendsto (fun x => x.2.1 * x.1.2 * x.1.1⁻¹ * x.2.2⁻¹) (comap (fun p => (p.1.2 * p.1.1⁻¹, p.2.2 * p.2.1⁻¹)) ((𝓝 1).prod (𝓝 1))) (𝓝 1)<GOAL>Tendsto (fun x => x.2.1 * x.1.2 * x.1.1⁻¹ * x.2.2⁻¹) (comap (fun p => (p.1.2 * p.1.1⁻¹, p.2.2 * p.2.1⁻¹)) (𝓝 1 ×ˢ 𝓝 1)) (𝓝 1)
<VAR>α : Type u_1<VAR>m p : PosNum<GOAL>↑(m * p) + ↑(m * p) = ↑m * (↑p + ↑p)
<VAR>α : Type u_1<VAR>m p : PosNum<GOAL>↑(m * p) + ↑(m * p) + ↑m = ↑m * (↑p + ↑p) + ↑m
<VAR>α : Type u<VAR>l : List α<VAR>n m : ℕ<GOAL>(l.rotate n).rotate m = l.rotate (n + m)
<VAR>F : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>C : Type u_5<VAR>inst✝¹³ : CommSemiring R<VAR>inst✝¹² : StarRing R<VAR>inst✝¹¹ : Semiring A<VAR>inst✝¹⁰ : StarRing A<VAR>inst✝⁹ : Algebra R A<VAR>inst✝⁸ : StarModule R A<VAR>inst✝⁷ : Semiring B<VAR>inst✝⁶ : StarRing B<VAR>inst✝⁵ : Algebra R B<VAR>inst✝⁴ : StarModule R B<VAR>inst✝³ : Semiring C<VAR>inst✝² : StarRing C<VAR>inst✝¹ : Algebra R C<VAR>inst✝ : StarModule R C<VAR>S✝ : StarSubalgebra R A<VAR>S : StarSubalgebra R C<VAR>g : B →⋆ₐ[R] C<VAR>f : A →⋆ₐ[R] B<GOAL>↑(comap f (comap g S)) = ↑(comap (g.comp f) S)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s : Set α<VAR>x✝ y✝ : α<VAR>inst✝¹ : SemilatticeInf α<VAR>inst✝ : SemilatticeSup β<VAR>h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → f (x ⊓ y) = f x ⊔ f y<VAR>x : α<VAR>hx : x ∈ s<VAR>y : α<VAR>hy : y ∈ s<VAR>hxy : x ≤ y<GOAL>f x ⊔ f y = f x
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e✝ : PartialHomeomorph X Y<VAR>e : X ≃ₜ Y<GOAL>⇑e '' univ = univ
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : HasContDiffBump E<VAR>inst✝⁵ : MeasurableSpace E<VAR>c : E<VAR>f : ContDiffBump c<VAR>x : E<VAR>n : ℕ∞<VAR>μ : Measure E<VAR>inst✝⁴ : BorelSpace E<VAR>inst✝³ : FiniteDimensional ℝ E<VAR>inst✝² : IsLocallyFiniteMeasure μ<VAR>inst✝¹ : μ.IsOpenPosMeasure<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>K : ℝ<VAR>h : f.rOut ≤ K * f.rIn<GOAL>(μ (closedBall c f.rOut)).toReal / K ^ finrank ℝ E ≤ ∫ (x : E), ↑f x ∂μ
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : HasContDiffBump E<VAR>inst✝⁵ : MeasurableSpace E<VAR>c : E<VAR>f : ContDiffBump c<VAR>x : E<VAR>n : ℕ∞<VAR>μ : Measure E<VAR>inst✝⁴ : BorelSpace E<VAR>inst✝³ : FiniteDimensional ℝ E<VAR>inst✝² : IsLocallyFiniteMeasure μ<VAR>inst✝¹ : μ.IsOpenPosMeasure<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>K : ℝ<VAR>h : f.rOut ≤ K * f.rIn<VAR>K_pos : 0 < K<GOAL>(μ (closedBall c f.rOut)).toReal / K ^ finrank ℝ E ≤ ∫ (x : E), ↑f x ∂μ
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : HasContDiffBump E<VAR>inst✝⁵ : MeasurableSpace E<VAR>c : E<VAR>f : ContDiffBump c<VAR>x : E<VAR>n : ℕ∞<VAR>μ : Measure E<VAR>inst✝⁴ : BorelSpace E<VAR>inst✝³ : FiniteDimensional ℝ E<VAR>inst✝² : IsLocallyFiniteMeasure μ<VAR>inst✝¹ : μ.IsOpenPosMeasure<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>K : ℝ<VAR>h : f.rOut ≤ K * f.rIn<VAR>K_pos : 0 < K<GOAL>(μ (closedBall c f.rOut)).toReal / K ^ finrank ℝ E ≤ (μ (closedBall c f.rIn)).toReal
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : HasContDiffBump E<VAR>inst✝⁵ : MeasurableSpace E<VAR>c : E<VAR>f : ContDiffBump c<VAR>x : E<VAR>n : ℕ∞<VAR>μ : Measure E<VAR>inst✝⁴ : BorelSpace E<VAR>inst✝³ : FiniteDimensional ℝ E<VAR>inst✝² : IsLocallyFiniteMeasure μ<VAR>inst✝¹ : μ.IsOpenPosMeasure<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>K : ℝ<VAR>h : f.rOut ≤ K * f.rIn<VAR>K_pos : 0 < K<GOAL>f.rOut ^ finrank ℝ E * (μ (closedBall 0 1)).toReal ≤ (K * f.rIn) ^ finrank ℝ E * (μ (closedBall 0 1)).toReal
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : HasContDiffBump E<VAR>inst✝⁵ : MeasurableSpace E<VAR>c : E<VAR>f : ContDiffBump c<VAR>x : E<VAR>n : ℕ∞<VAR>μ : Measure E<VAR>inst✝⁴ : BorelSpace E<VAR>inst✝³ : FiniteDimensional ℝ E<VAR>inst✝² : IsLocallyFiniteMeasure μ<VAR>inst✝¹ : μ.IsOpenPosMeasure<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>K : ℝ<VAR>h : f.rOut ≤ K * f.rIn<VAR>K_pos : 0 < K<GOAL>0 ≤ f.rOut
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝ : Category.{v', u'} D<VAR>F : C ⥤ D<VAR>X✝ Y✝ : Square C<VAR>φ : X✝ ⟶ Y✝<GOAL>((fun sq => sq.map F) X✝).f₁₂ ≫ F.map φ.τ₂ = F.map φ.τ₁ ≫ ((fun sq => sq.map F) Y✝).f₁₂
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝ : Category.{v', u'} D<VAR>F : C ⥤ D<VAR>X✝ Y✝ : Square C<VAR>φ : X✝ ⟶ Y✝<GOAL>((fun sq => sq.map F) X✝).f₁₃ ≫ F.map φ.τ₃ = F.map φ.τ₁ ≫ ((fun sq => sq.map F) Y✝).f₁₃
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝ : Category.{v', u'} D<VAR>F : C ⥤ D<VAR>X✝ Y✝ : Square C<VAR>φ : X✝ ⟶ Y✝<GOAL>((fun sq => sq.map F) X✝).f₂₄ ≫ F.map φ.τ₄ = F.map φ.τ₂ ≫ ((fun sq => sq.map F) Y✝).f₂₄
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝ : Category.{v', u'} D<VAR>F : C ⥤ D<VAR>X✝ Y✝ : Square C<VAR>φ : X✝ ⟶ Y✝<GOAL>((fun sq => sq.map F) X✝).f₃₄ ≫ F.map φ.τ₄ = F.map φ.τ₃ ≫ ((fun sq => sq.map F) Y✝).f₃₄
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Algebra F K<VAR>S : Set E<VAR>hK : ∀ s ∈ S, IsIntegral F s ∧ Splits (algebraMap F K) (minpoly F s)<VAR>hK' : ∀ (s : E), IsIntegral F s ∧ Splits (algebraMap F K) (minpoly F s)<VAR>L : IntermediateField F E<VAR>f : ↥L →ₐ[F] K<VAR>hL : L ≤ adjoin F S<GOAL>∃ φ, φ.comp (inclusion hL) = f
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Algebra F K<VAR>S : Set E<VAR>hK : ∀ s ∈ S, IsIntegral F s ∧ Splits (algebraMap F K) (minpoly F s)<VAR>hK' : ∀ (s : E), IsIntegral F s ∧ Splits (algebraMap F K) (minpoly F s)<VAR>L : IntermediateField F E<VAR>f : ↥L →ₐ[F] K<VAR>hL : L ≤ adjoin F S<VAR>φ : Lifts F E K<VAR>hfφ : { carrier := L, emb := f } ≤ φ<VAR>hφ : ∀ (z : Lifts F E K), φ ≤ z → z ≤ φ<GOAL>∃ φ, φ.comp (inclusion hL) = f
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Algebra F K<VAR>S : Set E<VAR>hK : ∀ s ∈ S, IsIntegral F s ∧ Splits (algebraMap F K) (minpoly F s)<VAR>hK' : ∀ (s : E), IsIntegral F s ∧ Splits (algebraMap F K) (minpoly F s)<VAR>L : IntermediateField F E<VAR>f : ↥L →ₐ[F] K<VAR>hL : L ≤ adjoin F S<VAR>φ : Lifts F E K<VAR>hfφ : { carrier := L, emb := f } ≤ φ<VAR>hφ : ∀ (z : Lifts F E K), φ ≤ z → z ≤ φ<VAR>s : E<VAR>hs : s ∈ S<GOAL>s ∈ ↑φ.carrier
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>K : Type u_3<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Algebra F K<VAR>S : Set E<VAR>hK : ∀ s ∈ S, IsIntegral F s ∧ Splits (algebraMap F K) (minpoly F s)<VAR>hK' : ∀ (s : E), IsIntegral F s ∧ Splits (algebraMap F K) (minpoly F s)<VAR>L : IntermediateField F E<VAR>f : ↥L →ₐ[F] K<VAR>hL : L ≤ adjoin F S<VAR>φ : Lifts F E K<VAR>hfφ : { carrier := L, emb := f } ≤ φ<VAR>hφ : ∀ (z : Lifts F E K), φ ≤ z → z ≤ φ<GOAL>(φ.emb.comp (inclusion ⋯)).comp (inclusion hL) = f
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>inst✝¹ : LieRingModule L N<VAR>inst✝ : LieModule R L N<VAR>t : R<VAR>x y z : L<VAR>m n : M<GOAL>⁅-x, m⁆ = -⁅x, m⁆
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>N : Type w₁<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>inst✝¹ : LieRingModule L N<VAR>inst✝ : LieModule R L N<VAR>t : R<VAR>x y z : L<VAR>m n : M<GOAL>⁅-x + x, m⁆ = 0
<VAR>F : Type u_1<VAR>inst✝³ : Field F<VAR>E : Type u_2<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : FiniteDimensional F E<VAR>h : IntermediateField.fixedField ⊤ = ⊥<GOAL>IsGalois F E
<VAR>F : Type u_1<VAR>inst✝³ : Field F<VAR>E : Type u_2<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : FiniteDimensional F E<VAR>h : IntermediateField.fixedField ⊤ = ⊥<GOAL>IsGalois (↥(IntermediateField.fixedField ⊤)) E
<VAR>C : Type u_2<VAR>inst✝¹ : Category.{u_1, u_2} C<VAR>r : HomRel C<VAR>D : Type u_4<VAR>inst✝ : Category.{u_3, u_4} D<VAR>F : C ⥤ D<VAR>H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(lift r F H).map ((functor r).map f) = F.map f
<VAR>C : Type u_2<VAR>inst✝¹ : Category.{u_1, u_2} C<VAR>r : HomRel C<VAR>D : Type u_4<VAR>inst✝ : Category.{u_3, u_4} D<VAR>F : C ⥤ D<VAR>H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(lift r F H).map ((functor r).map f) = (lift.isLift r F H).inv.app X ≫ (functor r ⋙ lift r F H).map f ≫ (lift.isLift r F H).hom.app Y
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>A : Type u_3<VAR>inst✝¹ : MulOneClass M<VAR>s✝ : Set M<VAR>inst✝ : AddZeroClass A<VAR>t : Set A<VAR>S : Submonoid M<VAR>s : Set M<GOAL>↑(closure s) = {1} ∪ ↑(Subsemigroup.closure s)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>A : Type u_3<VAR>inst✝¹ : MulOneClass M<VAR>s✝ : Set M<VAR>inst✝ : AddZeroClass A<VAR>t : Set A<VAR>S : Submonoid M<VAR>s : Set M<GOAL>↑(closure s) ≤ {1} ∪ ↑(Subsemigroup.closure s)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>A : Type u_3<VAR>inst✝¹ : MulOneClass M<VAR>s✝ : Set M<VAR>inst✝ : AddZeroClass A<VAR>t : Set A<VAR>S : Submonoid M<VAR>s : Set M<GOAL>{1} ∪ ↑(Subsemigroup.closure s) ≤ ↑(closure s)
<VAR>ι : Type u_1<VAR>K : Type u_2<VAR>V : Type u_3<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f : ι → ℙ K V<VAR>u v : ℙ K V<GOAL>Dependent ![u, v] ↔ u = v
<VAR>ι : Type u_1<VAR>K : Type u_2<VAR>V : Type u_3<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f : ι → ℙ K V<VAR>u v : ℙ K V<GOAL>¬(¬v.rep = 0 ∧ ∀ (a : K), a • v.rep ≠ (Projectivization.rep ∘ ![u, v]) 0) ↔ u = v
<VAR>ι : Type u_1<VAR>K : Type u_2<VAR>V : Type u_3<VAR>inst✝² : DivisionRing K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f : ι → ℙ K V<VAR>u v : ℙ K V<GOAL>¬v.rep = 0 ∨ u = v
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝⁸ : Category.{v, u} V<VAR>inst✝⁷ : Preadditive V<VAR>W : Type u_2<VAR>inst✝⁶ : Category.{?u.23606, u_2} W<VAR>inst✝⁵ : Preadditive W<VAR>W₁ : Type u_3<VAR>W₂ : Type u_4<VAR>inst✝⁴ : Category.{?u.23631, u_3} W₁<VAR>inst✝³ : Category.{?u.23635, u_4} W₂<VAR>inst✝² : HasZeroMorphisms W₁<VAR>inst✝¹ : HasZeroMorphisms W₂<VAR>c✝ : ComplexShape ι<VAR>C✝ D E : HomologicalComplex V c✝<VAR>f g : C✝ ⟶ D<VAR>h k : D ⟶ E<VAR>i✝ : ι<VAR>F : W₁ ⥤ W₂<VAR>inst✝ : F.PreservesZeroMorphisms<VAR>c : ComplexShape ι<VAR>C : HomologicalComplex W₁ c<VAR>i j : ι<VAR>w : ¬c.Rel i j<GOAL>F.map (C.d i j) = 0
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝⁸ : Category.{v, u} V<VAR>inst✝⁷ : Preadditive V<VAR>W : Type u_2<VAR>inst✝⁶ : Category.{?u.23606, u_2} W<VAR>inst✝⁵ : Preadditive W<VAR>W₁ : Type u_3<VAR>W₂ : Type u_4<VAR>inst✝⁴ : Category.{?u.23631, u_3} W₁<VAR>inst✝³ : Category.{?u.23635, u_4} W₂<VAR>inst✝² : HasZeroMorphisms W₁<VAR>inst✝¹ : HasZeroMorphisms W₂<VAR>c✝ : ComplexShape ι<VAR>C✝ D E : HomologicalComplex V c✝<VAR>f g : C✝ ⟶ D<VAR>h k✝ : D ⟶ E<VAR>i✝ : ι<VAR>F : W₁ ⥤ W₂<VAR>inst✝ : F.PreservesZeroMorphisms<VAR>c : ComplexShape ι<VAR>C : HomologicalComplex W₁ c<VAR>i j k : ι<VAR>x✝¹ : c.Rel i j<VAR>x✝ : c.Rel j k<GOAL>(fun i j => F.map (C.d i j)) i j ≫ (fun i j => F.map (C.d i j)) j k = 0
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝⁸ : Category.{v, u} V<VAR>inst✝⁷ : Preadditive V<VAR>W : Type u_2<VAR>inst✝⁶ : Category.{?u.23606, u_2} W<VAR>inst✝⁵ : Preadditive W<VAR>W₁ : Type u_3<VAR>W₂ : Type u_4<VAR>inst✝⁴ : Category.{?u.23631, u_3} W₁<VAR>inst✝³ : Category.{?u.23635, u_4} W₂<VAR>inst✝² : HasZeroMorphisms W₁<VAR>inst✝¹ : HasZeroMorphisms W₂<VAR>c✝ : ComplexShape ι<VAR>C D E : HomologicalComplex V c✝<VAR>f✝ g : C ⟶ D<VAR>h k : D ⟶ E<VAR>i✝ : ι<VAR>F : W₁ ⥤ W₂<VAR>inst✝ : F.PreservesZeroMorphisms<VAR>c : ComplexShape ι<VAR>X✝ Y✝ : HomologicalComplex W₁ c<VAR>f : X✝ ⟶ Y✝<VAR>i j : ι<VAR>x✝ : c.Rel i j<GOAL>F.map (f.f i) ≫ F.map (Y✝.d i j) = F.map (X✝.d i j) ≫ F.map (f.f j)
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>hs : HasFDerivWithinAt f f' s x<VAR>ht : HasFDerivWithinAt f f' t x<GOAL>HasFDerivWithinAt f f' (s ∪ t) x
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>hs : HasFDerivWithinAt f f' s x<VAR>ht : HasFDerivWithinAt f f' t x<GOAL>HasFDerivAtFilter f f' x (𝓝[s] x ⊔ 𝓝[t] x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>s : ι → Set α<VAR>x : α<VAR>hx : x ∈ ⋃ i, s i<GOAL>Nonempty ι
<VAR>α : Sort u_1<VAR>r : α → α → Prop<VAR>C : α → Sort u_2<VAR>F : (x : α) → ((y : α) → r y x → C y) → C x<VAR>x : α<VAR>a : Acc r x<GOAL>fixF F x a = WellFounded.fixFC F x a
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝⁹ : Field A<VAR>inst✝⁸ : Ring B<VAR>inst✝⁷ : Algebra A B<VAR>x : B<VAR>F : Type u_3<VAR>E : Type u_4<VAR>K : Type u_5<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : Ring E<VAR>inst✝⁴ : CommRing K<VAR>inst✝³ : IsDomain K<VAR>inst✝² : Algebra F E<VAR>inst✝¹ : Algebra F K<VAR>inst✝ : FiniteDimensional F E<VAR>f g : E →ₐ[F] K<VAR>h : rootsOfMinPolyPiType F E K f = rootsOfMinPolyPiType F E K g<GOAL>f = g
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝⁹ : Field A<VAR>inst✝⁸ : Ring B<VAR>inst✝⁷ : Algebra A B<VAR>x : B<VAR>F : Type u_3<VAR>E : Type u_4<VAR>K : Type u_5<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : Ring E<VAR>inst✝⁴ : CommRing K<VAR>inst✝³ : IsDomain K<VAR>inst✝² : Algebra F E<VAR>inst✝¹ : Algebra F K<VAR>inst✝ : FiniteDimensional F E<VAR>f g : E →ₐ[F] K<VAR>h : rootsOfMinPolyPiType F E K f = rootsOfMinPolyPiType F E K g<GOAL>(↑f).toLinearMap = (↑g).toLinearMap
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝⁹ : Field A<VAR>inst✝⁸ : Ring B<VAR>inst✝⁷ : Algebra A B<VAR>x : B<VAR>F : Type u_3<VAR>E : Type u_4<VAR>K : Type u_5<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : Ring E<VAR>inst✝⁴ : CommRing K<VAR>inst✝³ : IsDomain K<VAR>inst✝² : Algebra F E<VAR>inst✝¹ : Algebra F K<VAR>inst✝ : FiniteDimensional F E<VAR>f g : E →ₐ[F] K<VAR>h : ∀ (a : ↑(range ⇑(FiniteDimensional.finBasis F E))), rootsOfMinPolyPiType F E K f a = rootsOfMinPolyPiType F E K g a<GOAL>(↑f).toLinearMap = (↑g).toLinearMap
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁹ : RCLike 𝕜<VAR>p : A → Prop<VAR>inst✝⁸ : PartialOrder A<VAR>inst✝⁷ : NormedRing A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : StarOrderedRing A<VAR>inst✝⁴ : TopologicalRing A<VAR>inst✝³ : NormedAlgebra 𝕜 A<VAR>inst✝² : CompleteSpace A<VAR>inst✝¹ : ContinuousFunctionalCalculus 𝕜 p<VAR>inst✝ : UniqueContinuousFunctionalCalculus 𝕜 A<VAR>a : A<VAR>ha : autoParam (p a) _auto✝<GOAL>cfc (exp 𝕜) a = exp 𝕜 a