ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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 : ℕ∞<VAR>x' : M<VAR>y : M'<VAR>hy : f x' ∈ (extChartAt I' y).source<VAR>e : PartialEquiv M E := extChartAt I x<VAR>hx : x' ∈ e.source<VAR>e' : PartialEquiv M' E' := extChartAt I' (f x)<VAR>hc : ContinuousWithinAt f s x'<GOAL>𝓝[↑e.symm ⁻¹' s ∩ range ↑I] ↑e x' = 𝓝[e.target ∩ ↑e.symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source)] ↑e 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 : ℕ∞<VAR>x' : M<VAR>y : M'<VAR>hy : f x' ∈ (extChartAt I' y).source<VAR>e : PartialEquiv M E := extChartAt I x<VAR>hx : x' ∈ e.source<VAR>e' : PartialEquiv M' E' := extChartAt I' (f x)<VAR>hc : ContinuousWithinAt f s x'<GOAL>f ⁻¹' (extChartAt I' y).source ∈ 𝓝[s] x'
<VAR>ι : Type u_1<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>c : ComplexShape ι<VAR>K L M K' L' : HomologicalComplex C c<VAR>φ : K ⟶ L<VAR>φ' : L ⟶ M<VAR>i : ι<VAR>inst✝² : K.HasHomology i<VAR>inst✝¹ : L.HasHomology i<VAR>inst✝ : M.HasHomology i<VAR>hφ : QuasiIsoAt φ i<VAR>hφφ' : QuasiIsoAt (φ ≫ φ') i<GOAL>QuasiIsoAt φ' i
<VAR>ι : Type u_1<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>c : ComplexShape ι<VAR>K L M K' L' : HomologicalComplex C c<VAR>φ : K ⟶ L<VAR>φ' : L ⟶ M<VAR>i : ι<VAR>inst✝² : K.HasHomology i<VAR>inst✝¹ : L.HasHomology i<VAR>inst✝ : M.HasHomology i<VAR>hφ : IsIso (homologyMap φ i)<VAR>hφφ' : IsIso (homologyMap (φ ≫ φ') i)<GOAL>IsIso (homologyMap φ' i)
<VAR>ι : Type u_1<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>c : ComplexShape ι<VAR>K L M K' L' : HomologicalComplex C c<VAR>φ : K ⟶ L<VAR>φ' : L ⟶ M<VAR>i : ι<VAR>inst✝² : K.HasHomology i<VAR>inst✝¹ : L.HasHomology i<VAR>inst✝ : M.HasHomology i<VAR>hφ : IsIso (homologyMap φ i)<VAR>hφφ' : IsIso (homologyMap φ i ≫ homologyMap φ' i)<GOAL>IsIso (homologyMap φ' i)
<VAR>α : Type u_1<VAR>a : α<VAR>f : α →₀ ℕ<GOAL>f.multinomial = (f.sum fun x => id).choose (f a) * (f.update a 0).multinomial
<VAR>α : Type u_1<VAR>a : α<VAR>f : α →₀ ℕ<GOAL>Nat.multinomial f.support ⇑f = (f.sum fun x => id).choose (f a) * Nat.multinomial (f.update a 0).support ⇑(f.update a 0)
<VAR>R : Type u_1<VAR>inst✝⁵ : Ring R<VAR>A : Type u_2<VAR>inst✝⁴ : CommRing A<VAR>M : Type u_3<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>U U₁ U₂ : Submodule R M<VAR>x x₁ x₂ y y₁ y₂ z z₁ z₂ : M<VAR>N : Type u_4<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>V V₁ V₂ : Submodule R N<VAR>hxy : x ≡ y [SMOD U]<VAR>n : ℕ<GOAL>n • x ≡ n • y [SMOD U]
<VAR>R : Type u_1<VAR>inst✝⁵ : Ring R<VAR>A : Type u_2<VAR>inst✝⁴ : CommRing A<VAR>M : Type u_3<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>U U₁ U₂ : Submodule R M<VAR>x x₁ x₂ y y₁ y₂ z z₁ z₂ : M<VAR>N : Type u_4<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>V V₁ V₂ : Submodule R N<VAR>hxy : Submodule.Quotient.mk x = Submodule.Quotient.mk y<VAR>n : ℕ<GOAL>Submodule.Quotient.mk (n • x) = Submodule.Quotient.mk (n • y)
<VAR>S : Set ℝ<VAR>f : ℝ → ℝ<VAR>x y f' : ℝ<VAR>hfc : StrictConcaveOn ℝ S f<VAR>hx : x ∈ S<VAR>hy : y ∈ S<VAR>hxy : x < y<VAR>hf' : HasDerivWithinAt f f' S y<GOAL>f' < slope f x y
<VAR>R : Type u<VAR>L : Type v<VAR>M : 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>N✝ N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>ι : Sort u_1<VAR>N : ι → LieSubmodule R L M<VAR>C : M → Prop<VAR>x : M<VAR>hx : x ∈ ⨆ i, N i<VAR>hN : ∀ (i : ι), ∀ y ∈ N i, C y<VAR>h0 : C 0<VAR>hadd : ∀ (y z : M), C y → C z → C (y + z)<GOAL>C x
<VAR>R : Type u<VAR>L : Type v<VAR>M : 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>N✝ N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>ι : Sort u_1<VAR>N : ι → LieSubmodule R L M<VAR>C : M → Prop<VAR>x : M<VAR>hx : x ∈ ⨆ i, ↑(N i)<VAR>hN : ∀ (i : ι), ∀ y ∈ N i, C y<VAR>h0 : C 0<VAR>hadd : ∀ (y z : M), C y → C z → C (y + z)<GOAL>C x
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>hn : p₂ ≠ p₃<VAR>h : dist p₁ p₂ = dist p₁ p₃<GOAL>∡ p₃ p₁ p₂ = ↑π - 2 • ∡ p₁ p₂ p₃
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>hn : p₂ ≠ p₃<VAR>h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖<GOAL>∡ p₃ p₁ p₂ = ↑π - 2 • ∡ p₁ p₂ p₃
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>hn : p₂ ≠ p₃<VAR>h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖<GOAL>o.oangle (p₃ -ᵥ p₁) (p₂ -ᵥ p₁) = ↑π - 2 • o.oangle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>hn : p₂ ≠ p₃<VAR>h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖<GOAL>o.oangle (p₃ -ᵥ p₁) (p₂ -ᵥ p₁) = o.oangle (p₁ -ᵥ p₃) (p₁ -ᵥ p₂)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>hn : p₂ ≠ p₃<VAR>h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖<GOAL>↑π - 2 • o.oangle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = ↑π - 2 • o.oangle (p₁ -ᵥ p₃ - (p₁ -ᵥ p₂)) (p₁ -ᵥ p₃)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>hn : p₂ ≠ p₃<VAR>h : ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖<GOAL>p₁ -ᵥ p₂ ≠ p₁ -ᵥ p₃
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>s t u v : Set α<VAR>inst✝ : PreconnectedSpace α<VAR>P : α → α → Prop<VAR>h : ∀ (x : α), ∀ᶠ (y : α) in 𝓝 x, P x y<VAR>h' : Transitive P<VAR>h'' : Symmetric P<VAR>x y : α<GOAL>P x y
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>s t u v : Set α<VAR>inst✝ : PreconnectedSpace α<VAR>P : α → α → Prop<VAR>h : ∀ (x : α), ∀ᶠ (y : α) in 𝓝 x, P x y<VAR>h' : Transitive P<VAR>h'' : Symmetric P<VAR>x y z : α<GOAL>∀ᶠ (y : α) in 𝓝 z, P z y ∧ P y z
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>s t u v : Set α<VAR>inst✝ : PreconnectedSpace α<VAR>P : α → α → Prop<VAR>h : ∀ (x : α), ∀ᶠ (y : α) in 𝓝 x, P x y<VAR>h' : Transitive P<VAR>h'' : Symmetric P<VAR>x y z a : α<VAR>ha : P z a<GOAL>P z a ∧ P a z
<VAR>R : Type u<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q✝ : R[X]<VAR>p q : R[ℕ]<GOAL>{ toFinsupp := p }.coeff = { toFinsupp := q }.coeff → { toFinsupp := p } = { toFinsupp := q }
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝² : H.IsCartanSubalgebra<VAR>inst✝¹ : IsTriangularizable K (↥H) L<VAR>inst✝ : IsKilling K L<VAR>x : L<VAR>hx : x ∈ H<VAR>hx' : _root_.IsNilpotent ((ad K L) x)<GOAL>⟨x, hx⟩ ∈ LinearMap.ker (traceForm K (↥H) L)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝² : H.IsCartanSubalgebra<VAR>inst✝¹ : IsTriangularizable K (↥H) L<VAR>inst✝ : IsKilling K L<VAR>x : L<VAR>hx : x ∈ H<VAR>hx' : _root_.IsNilpotent ((ad K L) x)<GOAL>(traceForm K (↥H) L) ⟨x, hx⟩ = 0
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝² : H.IsCartanSubalgebra<VAR>inst✝¹ : IsTriangularizable K (↥H) L<VAR>inst✝ : IsKilling K L<VAR>x : L<VAR>hx : x ∈ H<VAR>hx' : _root_.IsNilpotent ((ad K L) x)<VAR>y : ↥H<GOAL>((traceForm K (↥H) L) ⟨x, hx⟩) y = 0 y
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝² : H.IsCartanSubalgebra<VAR>inst✝¹ : IsTriangularizable K (↥H) L<VAR>inst✝ : IsKilling K L<VAR>x : L<VAR>hx : x ∈ H<VAR>hx' : _root_.IsNilpotent ((ad K L) x)<VAR>y : ↥H<VAR>comm : Commute ((toEnd K (↥H) L) ⟨x, hx⟩) ((toEnd K (↥H) L) y)<GOAL>((traceForm K (↥H) L) ⟨x, hx⟩) y = 0 y
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝² : H.IsCartanSubalgebra<VAR>inst✝¹ : IsTriangularizable K (↥H) L<VAR>inst✝ : IsKilling K L<VAR>x : L<VAR>hx : x ∈ H<VAR>hx' : _root_.IsNilpotent ((ad K L) x)<VAR>y : ↥H<VAR>comm : Commute ((toEnd K (↥H) L) ⟨x, hx⟩) ((toEnd K (↥H) L) y)<GOAL>(LinearMap.trace K L) ((toEnd K (↥H) L) ⟨x, hx⟩ * (toEnd K (↥H) L) y) = 0
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.220633, u_2} D<VAR>inst✝¹ : Abelian C<VAR>S : ShortComplex C<VAR>hS : S.Exact<VAR>P : C<VAR>f : P ⟶ S.X₂<VAR>inst✝ : Projective P<VAR>hf : f ≫ S.g = 0<GOAL>hS.liftFromProjective f hf ≫ S.f = f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.220633, u_2} D<VAR>inst✝¹ : Abelian C<VAR>S : ShortComplex C<VAR>hS : S.Exact<VAR>P : C<VAR>f : P ⟶ S.X₂<VAR>inst✝ : Projective P<VAR>hf : f ≫ S.g = 0<VAR>this : Epi S.toCycles<GOAL>hS.liftFromProjective f hf ≫ S.f = f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.220633, u_2} D<VAR>inst✝¹ : Abelian C<VAR>S : ShortComplex C<VAR>hS : S.Exact<VAR>P : C<VAR>f : P ⟶ S.X₂<VAR>inst✝ : Projective P<VAR>hf : f ≫ S.g = 0<VAR>this : Epi S.toCycles<GOAL>Projective.factorThru (S.liftCycles f hf) S.toCycles ≫ S.f = f
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝¹¹ : CommRing K<VAR>inst✝¹⁰ : CommRing L<VAR>inst✝⁹ : CommRing M<VAR>inst✝⁸ : CommRing N<VAR>i : K →+* L<VAR>j : K →+* M<VAR>k : K →+* N<VAR>f : L →+* M<VAR>g : L →+* N<VAR>p : ℕ<VAR>inst✝⁷ : ExpChar K p<VAR>inst✝⁶ : ExpChar L p<VAR>inst✝⁵ : ExpChar M p<VAR>inst✝⁴ : ExpChar N p<VAR>inst✝³ : PerfectRing M p<VAR>inst✝² : IsPRadical i p<VAR>inst✝¹ : IsPRadical g p<VAR>inst✝ : IsPRadical (g.comp i) p<GOAL>lift g (lift i j p) p = lift (g.comp i) j p
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝¹¹ : CommRing K<VAR>inst✝¹⁰ : CommRing L<VAR>inst✝⁹ : CommRing M<VAR>inst✝⁸ : CommRing N<VAR>i : K →+* L<VAR>j : K →+* M<VAR>k : K →+* N<VAR>f : L →+* M<VAR>g : L →+* N<VAR>p : ℕ<VAR>inst✝⁷ : ExpChar K p<VAR>inst✝⁶ : ExpChar L p<VAR>inst✝⁵ : ExpChar M p<VAR>inst✝⁴ : ExpChar N p<VAR>inst✝³ : PerfectRing M p<VAR>inst✝² : IsPRadical i p<VAR>inst✝¹ : IsPRadical g p<VAR>inst✝ : IsPRadical (g.comp i) p<GOAL>(fun f => f.comp (g.comp i)) (lift g (lift i j p) p) = (fun f => f.comp (g.comp i)) (lift (g.comp i) j p)
<VAR>a n✝ n : ℕ<GOAL>(2 * n).bitIndices = map (fun x => x + 1) n.bitIndices
<VAR>k : Type u_1<VAR>inst✝⁹ : Ring k<VAR>V : Type u_2<VAR>P : Type u_3<VAR>V₁ : Type u_4<VAR>P₁ : Type u_5<VAR>V₂ : Type u_6<VAR>P₂ : Type u_7<VAR>inst✝⁸ : AddCommGroup V<VAR>inst✝⁷ : Module k V<VAR>inst✝⁶ : AffineSpace V P<VAR>inst✝⁵ : AddCommGroup V₁<VAR>inst✝⁴ : Module k V₁<VAR>inst✝³ : AffineSpace V₁ P₁<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module k V₂<VAR>inst✝ : AffineSpace V₂ P₂<VAR>v : V<VAR>x✝ : P<GOAL>x✝ ∈ v +ᵥ ⊥ ↔ x✝ ∈ ⊥
<VAR>f✝ f g : ℝ → ℝ<VAR>hf : GrowsPolynomially f<VAR>hg : GrowsPolynomially g<GOAL>GrowsPolynomially fun x => f x * g x
<VAR>f✝ f g : ℝ → ℝ<VAR>hf : GrowsPolynomially f<VAR>hg : GrowsPolynomially g<GOAL>GrowsPolynomially fun x => |f x| * |g x|
<VAR>f✝ f g : ℝ → ℝ<VAR>hf : GrowsPolynomially f<VAR>hg : GrowsPolynomially g<VAR>b : ℝ<VAR>hb : b ∈ Set.Ioo 0 1<GOAL>∃ c₁ > 0, ∃ c₂ > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, (fun x => |f x| * |g x|) u ∈ Set.Icc (c₁ * (fun x => |f x| * |g x|) x) (c₂ * (fun x => |f x| * |g x|) x)
<VAR>f✝ f g : ℝ → ℝ<VAR>hf✝ : GrowsPolynomially f<VAR>hg : GrowsPolynomially g<VAR>b : ℝ<VAR>hb : b ∈ Set.Ioo 0 1<VAR>hf : ∃ c₁ > 0, ∃ c₂ > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, (fun x => |f x|) u ∈ Set.Icc (c₁ * (fun x => |f x|) x) (c₂ * (fun x => |f x|) x)<GOAL>∃ c₁ > 0, ∃ c₂ > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, (fun x => |f x| * |g x|) u ∈ Set.Icc (c₁ * (fun x => |f x| * |g x|) x) (c₂ * (fun x => |f x| * |g x|) x)
<VAR>f✝ f g : ℝ → ℝ<VAR>hf✝ : GrowsPolynomially f<VAR>hg✝ : GrowsPolynomially g<VAR>b : ℝ<VAR>hb : b ∈ Set.Ioo 0 1<VAR>hf : ∃ c₁ > 0, ∃ c₂ > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, (fun x => |f x|) u ∈ Set.Icc (c₁ * (fun x => |f x|) x) (c₂ * (fun x => |f x|) x)<VAR>hg : ∃ c₁ > 0, ∃ c₂ > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, (fun x => |g x|) u ∈ Set.Icc (c₁ * (fun x => |g x|) x) (c₂ * (fun x => |g x|) x)<GOAL>∃ c₁ > 0, ∃ c₂ > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, (fun x => |f x| * |g x|) u ∈ Set.Icc (c₁ * (fun x => |f x| * |g x|) x) (c₂ * (fun x => |f x| * |g x|) x)
<VAR>f✝ f g : ℝ → ℝ<VAR>hf✝ : GrowsPolynomially f<VAR>hg✝ : GrowsPolynomially g<VAR>b : ℝ<VAR>hb : b ∈ Set.Ioo 0 1<VAR>c₁ : ℝ<VAR>hc₁_mem : c₁ > 0<VAR>c₂ : ℝ<VAR>hc₂_mem : c₂ > 0<VAR>hf : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, (fun x => |f x|) u ∈ Set.Icc (c₁ * (fun x => |f x|) x) (c₂ * (fun x => |f x|) x)<VAR>c₃ : ℝ<VAR>hc₃_mem : c₃ > 0<VAR>c₄ : ℝ<VAR>hc₄_mem : c₄ > 0<VAR>hg : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, (fun x => |g x|) u ∈ Set.Icc (c₃ * (fun x => |g x|) x) (c₄ * (fun x => |g x|) x)<GOAL>∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, (fun x => |f x| * |g x|) u ∈ Set.Icc (c₁ * c₃ * (fun x => |f x| * |g x|) x) (c₂ * c₄ * (fun x => |f x| * |g x|) x)
<VAR>f✝ f g : ℝ → ℝ<VAR>hf✝¹ : GrowsPolynomially f<VAR>hg✝¹ : GrowsPolynomially g<VAR>b : ℝ<VAR>hb : b ∈ Set.Ioo 0 1<VAR>c₁ : ℝ<VAR>hc₁_mem : c₁ > 0<VAR>c₂ : ℝ<VAR>hc₂_mem : c₂ > 0<VAR>hf✝ : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, (fun x => |f x|) u ∈ Set.Icc (c₁ * (fun x => |f x|) x) (c₂ * (fun x => |f x|) x)<VAR>c₃ : ℝ<VAR>hc₃_mem : c₃ > 0<VAR>c₄ : ℝ<VAR>hc₄_mem : c₄ > 0<VAR>hg✝ : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, (fun x => |g x|) u ∈ Set.Icc (c₃ * (fun x => |g x|) x) (c₄ * (fun x => |g x|) x)<VAR>x : ℝ<VAR>hf : ∀ u ∈ Set.Icc (b * x) x, |f u| ∈ Set.Icc (c₁ * |f x|) (c₂ * |f x|)<VAR>hg : ∀ u ∈ Set.Icc (b * x) x, |g u| ∈ Set.Icc (c₃ * |g x|) (c₄ * |g x|)<GOAL>∀ u ∈ Set.Icc (b * x) x, |f u| * |g u| ∈ Set.Icc (c₁ * c₃ * (|f x| * |g x|)) (c₂ * c₄ * (|f x| * |g x|))
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝ : Semiring R<GOAL>coeffs 1 ⊆ {1}
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H : Subgroup G<GOAL>H.normalCore = (MulAction.toPermHom G (G ⧸ H)).ker
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H : Subgroup G<GOAL>H.normalCore ≤ (MulAction.toPermHom G (G ⧸ H)).ker
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H : Subgroup G<GOAL>(MulAction.toPermHom G (G ⧸ H)).ker ≤ H.normalCore
<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>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : ℝ → ℝ<VAR>a b : ℝ<VAR>μ : Measure ℝ<VAR>hab : a ≤ b<VAR>hf : IntervalIntegrable f μ a b<VAR>hg : IntervalIntegrable g μ a b<VAR>h : f ≤ᶠ[ae μ] g<GOAL>∫ (u : ℝ) in a..b, f u ∂μ ≤ ∫ (u : ℝ) in a..b, g u ∂μ
<VAR>m n : ℕ<GOAL>fib (m.gcd n) = (fib m).gcd (fib n)
<VAR>ι : Sort u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝ : LinearOrder α<VAR>a₁ a₂ b₁ b₂ : α<VAR>p : ι → Prop<VAR>f : (i : ι) → p i → α<VAR>a : α<GOAL>⋃ i, ⋃ (hi : p i), Ico (f i hi) a = Iio a ↔ ∀ x < a, ∃ i, ∃ (hi : p i), f i hi ≤ x
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>G' : G.Subgraph<VAR>s : Set (Sym2 V)<GOAL>G'.deleteEdges (s ∩ G'.edgeSet) = G'.deleteEdges s
<VAR>α : Type u<VAR>β : Type v<VAR>δ : Type w<VAR>l : List α<VAR>s : Stream' α<GOAL>corec (fun x => match x with | (a, snd) => a) (fun p => match p with | (l', s') => (l' ++ [s'.head], s'.tail)) (l, s) = l :: corec (fun x => match x with | (a, snd) => a) (fun p => match p with | (l', s') => (l' ++ [s'.head], s'.tail)) (l ++ [s.head], s.tail)
<VAR>C : Type u_4<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{u_3, u_4} C<VAR>inst✝⁴ : Category.{u_1, u_2} D<VAR>F : C ⥤ D<VAR>A : Type u_5<VAR>inst✝³ : AddMonoid A<VAR>inst✝² : HasShift C A<VAR>s : A → D ⥤ D<VAR>i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F<VAR>inst✝¹ : ((whiskeringLeft C D D).obj F).Full<VAR>inst✝ : ((whiskeringLeft C D D).obj F).Faithful<VAR>a b : A<VAR>X : C<GOAL>(add F s i a b).inv.app (F.obj X) = (s b).map ((i a).hom.app X) ≫ (i b).hom.app ((shiftFunctor C a).obj X) ≫ F.map ((shiftFunctorAdd C a b).inv.app X) ≫ (i (a + b)).inv.app X
<VAR>C : Type u_4<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{u_3, u_4} C<VAR>inst✝⁴ : Category.{u_1, u_2} D<VAR>F : C ⥤ D<VAR>A : Type u_5<VAR>inst✝³ : AddMonoid A<VAR>inst✝² : HasShift C A<VAR>s : A → D ⥤ D<VAR>i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F<VAR>inst✝¹ : ((whiskeringLeft C D D).obj F).Full<VAR>inst✝ : ((whiskeringLeft C D D).obj F).Faithful<VAR>a b : A<VAR>X : C<VAR>h : whiskerLeft F (add F s i a b).inv = (i (a + b) ≪≫ isoWhiskerRight (shiftFunctorAdd C a b) F ≪≫ (shiftFunctor C a).associator (shiftFunctor C b) F ≪≫ isoWhiskerLeft (shiftFunctor C a) (i b).symm ≪≫ ((shiftFunctor C a).associator F (s b)).symm ≪≫ isoWhiskerRight (i a).symm (s b) ≪≫ F.associator (s a) (s b)).inv<GOAL>(add F s i a b).inv.app (F.obj X) = (s b).map ((i a).hom.app X) ≫ (i b).hom.app ((shiftFunctor C a).obj X) ≫ F.map ((shiftFunctorAdd C a b).inv.app X) ≫ (i (a + b)).inv.app X
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y : α<GOAL>edist x y = ↑(nndist x y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CommMonoidWithZero α<VAR>a b : α<GOAL>DvdNotUnit (Associates.mk a) (Associates.mk b) ↔ DvdNotUnit a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CommMonoidWithZero α<VAR>a b : α<GOAL>(a ≠ 0 ∧ ∃ x, ¬IsUnit x ∧ a * x ~ᵤ b) ↔ a ≠ 0 ∧ ∃ x, ¬IsUnit x ∧ b = a * x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CommMonoidWithZero α<VAR>a b : α<GOAL>(∃ x, ¬IsUnit x ∧ a * x ~ᵤ b) ↔ ∃ x, ¬IsUnit x ∧ b = a * x
<VAR>n : ℕ<VAR>i : Fin n<VAR>M : Type u_1<VAR>inst✝ : Zero M<VAR>y : M<VAR>t : Fin (n + 1) →₀ M<VAR>s : Fin n →₀ M<VAR>h : s ≠ 0<GOAL>cons y s ≠ 0
<VAR>n : ℕ<VAR>i : Fin n<VAR>M : Type u_1<VAR>inst✝ : Zero M<VAR>y : M<VAR>t : Fin (n + 1) →₀ M<VAR>s : Fin n →₀ M<VAR>c : cons y s = 0<GOAL>s = 0
<VAR>n : ℕ<VAR>i : Fin n<VAR>M : Type u_1<VAR>inst✝ : Zero M<VAR>y : M<VAR>t : Fin (n + 1) →₀ M<VAR>s : Fin n →₀ M<VAR>c : cons y s = 0<VAR>a : Fin n<GOAL>s a = 0 a
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>G : C<VAR>hG : IsCodetector G<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>hf : ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h<VAR>H : C<VAR>hH : H ∈ {G}<VAR>h : X ⟶ H<GOAL>∃! h', f ≫ h' = h
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>H : C<VAR>h : X ⟶ H<VAR>hG : IsCodetector H<VAR>hf : ∀ (h : X ⟶ H), ∃! h', f ≫ h' = h<VAR>hH : H ∈ {H}<GOAL>∃! h', f ≫ h' = h