ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : NormedSpace ℝ V<VAR>inst✝¹ : NormedAddCommGroup W<VAR>inst✝ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f✝ f : V → E<VAR>K : ℕ∞<VAR>C : ℝ<VAR>hf : ContDiff ℝ K f<VAR>n k : ℕ<VAR>hk : ↑k ≤ K<VAR>v : V<VAR>hv : ∀ i ≤ k, ∀ j ≤ n, ‖v‖ ^ j * ‖iteratedFDeriv ℝ i f v‖ ≤ C<GOAL>‖iteratedFDeriv ℝ k (fun v => fourierPowSMulRight L f v n) v‖ ≤ (2 * π) ^ n * (2 * ↑n + 2) ^ k * ‖L‖ ^ n * C
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : NormedSpace ℝ V<VAR>inst✝¹ : NormedAddCommGroup W<VAR>inst✝ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f✝ f : V → E<VAR>K : ℕ∞<VAR>C : ℝ<VAR>hf : ContDiff ℝ K f<VAR>n k : ℕ<VAR>hk : ↑k ≤ K<VAR>v : V<VAR>hv : ∀ i ≤ k, ∀ j ≤ n, ‖v‖ ^ j * ‖iteratedFDeriv ℝ i f v‖ ≤ C<GOAL>‖iteratedFDeriv ℝ k (fun v => (-(2 * ↑π * I)) ^ n • ((smulRightL ℝ (fun x => W) E) ((ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ).compContinuousLinearMapLRight fun x => L v)) (f v)) v‖ ≤ (2 * π) ^ n * (2 * ↑n + 2) ^ k * ‖L‖ ^ n * C
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : NormedSpace ℝ V<VAR>inst✝¹ : NormedAddCommGroup W<VAR>inst✝ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f✝ f : V → E<VAR>K : ℕ∞<VAR>C : ℝ<VAR>hf : ContDiff ℝ K f<VAR>n k : ℕ<VAR>hk : ↑k ≤ K<VAR>v : V<VAR>hv : ∀ i ≤ k, ∀ j ≤ n, ‖v‖ ^ j * ‖iteratedFDeriv ℝ i f v‖ ≤ C<VAR>T : ContinuousMultilinearMap ℝ (fun i => W →L[ℝ] ℝ) (ContinuousMultilinearMap ℝ (fun i => W) ℝ) := (ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ).compContinuousLinearMapLRight<GOAL>‖iteratedFDeriv ℝ k (fun v => (-(2 * ↑π * I)) ^ n • ((smulRightL ℝ (fun x => W) E) ((ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ).compContinuousLinearMapLRight fun x => L v)) (f v)) v‖ ≤ (2 * π) ^ n * (2 * ↑n + 2) ^ k * ‖L‖ ^ n * C
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : NormedSpace ℝ V<VAR>inst✝¹ : NormedAddCommGroup W<VAR>inst✝ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f✝ f : V → E<VAR>K : ℕ∞<VAR>C : ℝ<VAR>hf : ContDiff ℝ K f<VAR>n k : ℕ<VAR>hk : ↑k ≤ K<VAR>v : V<VAR>hv : ∀ i ≤ k, ∀ j ≤ n, ‖v‖ ^ j * ‖iteratedFDeriv ℝ i f v‖ ≤ C<VAR>T : ContinuousMultilinearMap ℝ (fun i => W →L[ℝ] ℝ) (ContinuousMultilinearMap ℝ (fun i => W) ℝ) := (ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ).compContinuousLinearMapLRight<VAR>I₁ : ∀ (m : ℕ), ‖iteratedFDeriv ℝ m ⇑T fun x => L v‖ ≤ ↑(n.descFactorial m) * 1 * (‖L‖ * ‖v‖) ^ (n - m)<GOAL>‖iteratedFDeriv ℝ k (fun v => (-(2 * ↑π * I)) ^ n • ((smulRightL ℝ (fun x => W) E) ((ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ).compContinuousLinearMapLRight fun x => L v)) (f v)) v‖ ≤ (2 * π) ^ n * (2 * ↑n + 2) ^ k * ‖L‖ ^ n * C
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : NormedSpace ℝ V<VAR>inst✝¹ : NormedAddCommGroup W<VAR>inst✝ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f✝ f : V → E<VAR>K : ℕ∞<VAR>C : ℝ<VAR>hf : ContDiff ℝ K f<VAR>n k : ℕ<VAR>hk : ↑k ≤ K<VAR>v : V<VAR>hv : ∀ i ≤ k, ∀ j ≤ n, ‖v‖ ^ j * ‖iteratedFDeriv ℝ i f v‖ ≤ C<VAR>T : ContinuousMultilinearMap ℝ (fun i => W →L[ℝ] ℝ) (ContinuousMultilinearMap ℝ (fun i => W) ℝ) := (ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ).compContinuousLinearMapLRight<VAR>I₁ : ∀ (m : ℕ), ‖iteratedFDeriv ℝ m ⇑T fun x => L v‖ ≤ ↑(n.descFactorial m) * 1 * (‖L‖ * ‖v‖) ^ (n - m)<VAR>I₂ : ∀ (m : ℕ), ‖iteratedFDeriv ℝ m (⇑T ∘ ⇑(ContinuousLinearMap.pi fun x => L)) v‖ ≤ ↑(n.descFactorial m) * 1 * (‖L‖ * ‖v‖) ^ (n - m) * ‖L‖ ^ m<VAR>I₃ : ∀ (m : ℕ), ‖iteratedFDeriv ℝ m (⇑T ∘ ⇑(ContinuousLinearMap.pi fun x => L)) v‖ ≤ ↑(n.descFactorial m) * ‖L‖ ^ n * ‖v‖ ^ (n - m)<GOAL>‖iteratedFDeriv ℝ k (fun v => (-(2 * ↑π * I)) ^ n • ((smulRightL ℝ (fun x => W) E) ((ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ).compContinuousLinearMapLRight fun x => L v)) (f v)) v‖ ≤ (2 * π) ^ n * (2 * ↑n + 2) ^ k * ‖L‖ ^ n * C
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : NormedSpace ℝ V<VAR>inst✝¹ : NormedAddCommGroup W<VAR>inst✝ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f✝ f : V → E<VAR>K : ℕ∞<VAR>C : ℝ<VAR>hf : ContDiff ℝ K f<VAR>n k : ℕ<VAR>hk : ↑k ≤ K<VAR>v : V<VAR>hv : ∀ i ≤ k, ∀ j ≤ n, ‖v‖ ^ j * ‖iteratedFDeriv ℝ i f v‖ ≤ C<VAR>T : ContinuousMultilinearMap ℝ (fun i => W →L[ℝ] ℝ) (ContinuousMultilinearMap ℝ (fun i => W) ℝ) := (ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ).compContinuousLinearMapLRight<VAR>I₁ : ∀ (m : ℕ), ‖iteratedFDeriv ℝ m ⇑T fun x => L v‖ ≤ ↑(n.descFactorial m) * 1 * (‖L‖ * ‖v‖) ^ (n - m)<VAR>I₂ : ∀ (m : ℕ), ‖iteratedFDeriv ℝ m (⇑T ∘ ⇑(ContinuousLinearMap.pi fun x => L)) v‖ ≤ ↑(n.descFactorial m) * 1 * (‖L‖ * ‖v‖) ^ (n - m) * ‖L‖ ^ m<VAR>I₃ : ∀ (m : ℕ), ‖iteratedFDeriv ℝ m (⇑T ∘ ⇑(ContinuousLinearMap.pi fun x => L)) v‖ ≤ ↑(n.descFactorial m) * ‖L‖ ^ n * ‖v‖ ^ (n - m)<VAR>A : ContDiff ℝ K fun y => T fun x => L y<GOAL>‖iteratedFDeriv ℝ k (fun v => (-(2 * ↑π * I)) ^ n • ((smulRightL ℝ (fun x => W) E) ((ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ).compContinuousLinearMapLRight fun x => L v)) (f v)) v‖ ≤ (2 * π) ^ n * (2 * ↑n + 2) ^ k * ‖L‖ ^ n * C
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : NormedSpace ℝ V<VAR>inst✝¹ : NormedAddCommGroup W<VAR>inst✝ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f✝ f : V → E<VAR>K : ℕ∞<VAR>C : ℝ<VAR>hf : ContDiff ℝ K f<VAR>n k : ℕ<VAR>hk : ↑k ≤ K<VAR>v : V<VAR>hv : ∀ i ≤ k, ∀ j ≤ n, ‖v‖ ^ j * ‖iteratedFDeriv ℝ i f v‖ ≤ C<VAR>T : ContinuousMultilinearMap ℝ (fun i => W →L[ℝ] ℝ) (ContinuousMultilinearMap ℝ (fun i => W) ℝ) := (ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ).compContinuousLinearMapLRight<VAR>I₁ : ∀ (m : ℕ), ‖iteratedFDeriv ℝ m ⇑T fun x => L v‖ ≤ ↑(n.descFactorial m) * 1 * (‖L‖ * ‖v‖) ^ (n - m)<VAR>I₂ : ∀ (m : ℕ), ‖iteratedFDeriv ℝ m (⇑T ∘ ⇑(ContinuousLinearMap.pi fun x => L)) v‖ ≤ ↑(n.descFactorial m) * 1 * (‖L‖ * ‖v‖) ^ (n - m) * ‖L‖ ^ m<VAR>I₃ : ∀ (m : ℕ), ‖iteratedFDeriv ℝ m (⇑T ∘ ⇑(ContinuousLinearMap.pi fun x => L)) v‖ ≤ ↑(n.descFactorial m) * ‖L‖ ^ n * ‖v‖ ^ (n - m)<VAR>A : ContDiff ℝ K fun y => T fun x => L y<GOAL>‖(-(2 * ↑π * I)) ^ n‖ * ‖iteratedFDeriv ℝ k (fun x => ((smulRightL ℝ (fun x => W) E) (T fun x_1 => L x, f x).1) (T fun x_1 => L x, f x).2) v‖ ≤ (2 * π) ^ n * (2 * ↑n + 2) ^ k * ‖L‖ ^ n * C
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : NormedSpace ℝ V<VAR>inst✝¹ : NormedAddCommGroup W<VAR>inst✝ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f✝ f : V → E<VAR>K : ℕ∞<VAR>C : ℝ<VAR>hf : ContDiff ℝ K f<VAR>n k : ℕ<VAR>hk : ↑k ≤ K<VAR>v : V<VAR>hv : ∀ i ≤ k, ∀ j ≤ n, ‖v‖ ^ j * ‖iteratedFDeriv ℝ i f v‖ ≤ C<VAR>T : ContinuousMultilinearMap ℝ (fun i => W →L[ℝ] ℝ) (ContinuousMultilinearMap ℝ (fun i => W) ℝ) := (ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ).compContinuousLinearMapLRight<VAR>I₁ : ∀ (m : ℕ), ‖iteratedFDeriv ℝ m ⇑T fun x => L v‖ ≤ ↑(n.descFactorial m) * 1 * (‖L‖ * ‖v‖) ^ (n - m)<VAR>I₂ : ∀ (m : ℕ), ‖iteratedFDeriv ℝ m (⇑T ∘ ⇑(ContinuousLinearMap.pi fun x => L)) v‖ ≤ ↑(n.descFactorial m) * 1 * (‖L‖ * ‖v‖) ^ (n - m) * ‖L‖ ^ m<VAR>I₃ : ∀ (m : ℕ), ‖iteratedFDeriv ℝ m (⇑T ∘ ⇑(ContinuousLinearMap.pi fun x => L)) v‖ ≤ ↑(n.descFactorial m) * ‖L‖ ^ n * ‖v‖ ^ (n - m)<VAR>A : ContDiff ℝ K fun y => T fun x => L y<GOAL>(2 * π) ^ n * ‖iteratedFDeriv ℝ k (fun x => ((smulRightL ℝ (fun x => W) E) (T fun x_1 => L x)) (f x)) v‖ ≤ (2 * π) ^ n * ((2 * ↑n + 2) ^ k * (‖L‖ ^ n * C))
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : NormedSpace ℝ V<VAR>inst✝¹ : NormedAddCommGroup W<VAR>inst✝ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f✝ f : V → E<VAR>K : ℕ∞<VAR>C : ℝ<VAR>hf : ContDiff ℝ K f<VAR>n k : ℕ<VAR>hk : ↑k ≤ K<VAR>v : V<VAR>hv : ∀ i ≤ k, ∀ j ≤ n, ‖v‖ ^ j * ‖iteratedFDeriv ℝ i f v‖ ≤ C<VAR>T : ContinuousMultilinearMap ℝ (fun i => W →L[ℝ] ℝ) (ContinuousMultilinearMap ℝ (fun i => W) ℝ) := (ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ).compContinuousLinearMapLRight<VAR>I₁ : ∀ (m : ℕ), ‖iteratedFDeriv ℝ m ⇑T fun x => L v‖ ≤ ↑(n.descFactorial m) * 1 * (‖L‖ * ‖v‖) ^ (n - m)<VAR>I₂ : ∀ (m : ℕ), ‖iteratedFDeriv ℝ m (⇑T ∘ ⇑(ContinuousLinearMap.pi fun x => L)) v‖ ≤ ↑(n.descFactorial m) * 1 * (‖L‖ * ‖v‖) ^ (n - m) * ‖L‖ ^ m<VAR>I₃ : ∀ (m : ℕ), ‖iteratedFDeriv ℝ m (⇑T ∘ ⇑(ContinuousLinearMap.pi fun x => L)) v‖ ≤ ↑(n.descFactorial m) * ‖L‖ ^ n * ‖v‖ ^ (n - m)<VAR>A : ContDiff ℝ K fun y => T fun x => L y<GOAL>‖iteratedFDeriv ℝ k (fun x => ((smulRightL ℝ (fun x => W) E) (T fun x_1 => L x)) (f x)) v‖ ≤ (2 * ↑n + 2) ^ k * (‖L‖ ^ n * C)
<VAR>E : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : NormedSpace ℝ V<VAR>inst✝¹ : NormedAddCommGroup W<VAR>inst✝ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f✝ f : V → E<VAR>K : ℕ∞<VAR>C : ℝ<VAR>hf : ContDiff ℝ K f<VAR>n k : ℕ<VAR>hk : ↑k ≤ K<VAR>v : V<VAR>hv : ∀ i ≤ k, ∀ j ≤ n, ‖v‖ ^ j * ‖iteratedFDeriv ℝ i f v‖ ≤ C<VAR>T : ContinuousMultilinearMap ℝ (fun i => W →L[ℝ] ℝ) (ContinuousMultilinearMap ℝ (fun i => W) ℝ) := (ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ).compContinuousLinearMapLRight<VAR>I₁ : ∀ (m : ℕ), ‖iteratedFDeriv ℝ m ⇑T fun x => L v‖ ≤ ↑(n.descFactorial m) * 1 * (‖L‖ * ‖v‖) ^ (n - m)<VAR>I₂ : ∀ (m : ℕ), ‖iteratedFDeriv ℝ m (⇑T ∘ ⇑(ContinuousLinearMap.pi fun x => L)) v‖ ≤ ↑(n.descFactorial m) * 1 * (‖L‖ * ‖v‖) ^ (n - m) * ‖L‖ ^ m<VAR>I₃ : ∀ (m : ℕ), ‖iteratedFDeriv ℝ m (⇑T ∘ ⇑(ContinuousLinearMap.pi fun x => L)) v‖ ≤ ↑(n.descFactorial m) * ‖L‖ ^ n * ‖v‖ ^ (n - m)<VAR>A : ContDiff ℝ K fun y => T fun x => L y<GOAL>∑ i ∈ Finset.range (k + 1), ↑(k.choose i) * ‖iteratedFDeriv ℝ i (fun y => T fun x => L y) v‖ * ‖iteratedFDeriv ℝ (k - i) f v‖ ≤ (2 * ↑n + 2) ^ k * (‖L‖ ^ n * C)
<VAR>x✝ y : ℝ<VAR>C : ℝ → Prop<VAR>h : ∀ (y : CauSeq ℚ abs), C (mk y)<VAR>x : Cauchy abs<GOAL>C { cauchy := x }
<VAR>x✝ y : ℝ<VAR>C : ℝ → Prop<VAR>h : ∀ (y : CauSeq ℚ abs), C (mk y)<VAR>x : CauSeq ℚ abs<GOAL>C { cauchy := Quot.mk Setoid.r x }
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s t✝ u : Set α<VAR>f g : α → β<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝ : MeasurableSingletonClass α<VAR>hf : Measurable f<VAR>h : {x | f x ≠ g x}.Countable<VAR>t : Set β<VAR>ht : MeasurableSet t<GOAL>MeasurableSet (g ⁻¹' t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s t✝ u : Set α<VAR>f g : α → β<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝ : MeasurableSingletonClass α<VAR>hf : Measurable f<VAR>h : {x | f x ≠ g x}.Countable<VAR>t : Set β<VAR>ht : MeasurableSet t<VAR>this : g ⁻¹' t = g ⁻¹' t ∩ {x | f x = g x}ᶜ ∪ g ⁻¹' t ∩ {x | f x = g x}<GOAL>MeasurableSet (g ⁻¹' t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s t✝ u : Set α<VAR>f g : α → β<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝ : MeasurableSingletonClass α<VAR>hf : Measurable f<VAR>h : {x | f x ≠ g x}.Countable<VAR>t : Set β<VAR>ht : MeasurableSet t<VAR>this : g ⁻¹' t = g ⁻¹' t ∩ {x | f x = g x}ᶜ ∪ g ⁻¹' t ∩ {x | f x = g x}<GOAL>MeasurableSet (g ⁻¹' t ∩ {x | f x = g x}ᶜ ∪ g ⁻¹' t ∩ {x | f x = g x})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s t✝ u : Set α<VAR>f g : α → β<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝ : MeasurableSingletonClass α<VAR>hf : Measurable f<VAR>h : {x | f x ≠ g x}.Countable<VAR>t : Set β<VAR>ht : MeasurableSet t<VAR>this : g ⁻¹' t = g ⁻¹' t ∩ {x | f x = g x}ᶜ ∪ g ⁻¹' t ∩ {x | f x = g x}<GOAL>MeasurableSet (g ⁻¹' t ∩ {x | f x = g x})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s t✝ u : Set α<VAR>f g : α → β<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>inst✝ : MeasurableSingletonClass α<VAR>hf : Measurable f<VAR>h : {x | f x ≠ g x}.Countable<VAR>t : Set β<VAR>ht : MeasurableSet t<VAR>this✝ : g ⁻¹' t = g ⁻¹' t ∩ {x | f x = g x}ᶜ ∪ g ⁻¹' t ∩ {x | f x = g x}<VAR>this : g ⁻¹' t ∩ {x | f x = g x} = f ⁻¹' t ∩ {x | f x = g x}<GOAL>MeasurableSet (f ⁻¹' t ∩ {x | f x = g x})
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>N₁ : Type u_5<VAR>N₂ : Type u_6<VAR>P : Type u_7<VAR>Mᵢ : ι → Type u_8<VAR>Nᵢ : ι → Type u_9<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : (i : ι) → AddCommMonoid (Mᵢ i)<VAR>inst✝⁶ : (i : ι) → AddCommMonoid (Nᵢ i)<VAR>inst✝⁵ : AddCommMonoid P<VAR>inst✝⁴ : (i : ι) → Module R (Mᵢ i)<VAR>inst✝³ : (i : ι) → Module R (Nᵢ i)<VAR>inst✝² : Module R P<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>i : ι<VAR>Q : QuadraticMap R (Mᵢ i) P<VAR>m : (i : ι) → Mᵢ i<GOAL>Q (m i) = (pi (Pi.single i Q)) m
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M₁ : Type u_3<VAR>M₂ : Type u_4<VAR>N₁ : Type u_5<VAR>N₂ : Type u_6<VAR>P : Type u_7<VAR>Mᵢ : ι → Type u_8<VAR>Nᵢ : ι → Type u_9<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : (i : ι) → AddCommMonoid (Mᵢ i)<VAR>inst✝⁶ : (i : ι) → AddCommMonoid (Nᵢ i)<VAR>inst✝⁵ : AddCommMonoid P<VAR>inst✝⁴ : (i : ι) → Module R (Mᵢ i)<VAR>inst✝³ : (i : ι) → Module R (Nᵢ i)<VAR>inst✝² : Module R P<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>i : ι<VAR>Q : QuadraticMap R (Mᵢ i) P<VAR>m : (i : ι) → Mᵢ i<VAR>j : ι<VAR>hij : j ≠ i<GOAL>(Pi.single i Q j) (m j) = 0
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_2, u_1} C<VAR>inst✝³ : Preadditive C<VAR>K K' : ChainComplex C ℕ<VAR>f : K ⟶ K'<VAR>Δ✝ Δ'✝ Δ''✝ : SimplexCategory<VAR>inst✝² : HasFiniteCoproducts C<VAR>Δ Δ' : SimplexCategoryᵒᵖ<VAR>A : Splitting.IndexSet Δ<VAR>θ : Δ ⟶ Δ'<VAR>Δ'' : SimplexCategory<VAR>e : unop Δ' ⟶ Δ''<VAR>i : Δ'' ⟶ unop A.fst<VAR>inst✝¹ : Epi e<VAR>inst✝ : Mono i<VAR>fac : e ≫ i = θ.unop ≫ A.e<GOAL>((splitting K).ι (unop A.fst).len ≫ (obj K).map A.e.op) ≫ (obj K).map θ = Termwise.mapMono K i ≫ (splitting K).ι Δ''.len ≫ map K (Splitting.IndexSet.mk e).e.op
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_2, u_1} C<VAR>inst✝³ : Preadditive C<VAR>K K' : ChainComplex C ℕ<VAR>f : K ⟶ K'<VAR>Δ✝ Δ'✝ Δ''✝ : SimplexCategory<VAR>inst✝² : HasFiniteCoproducts C<VAR>Δ Δ' : SimplexCategoryᵒᵖ<VAR>A : Splitting.IndexSet Δ<VAR>θ : Δ ⟶ Δ'<VAR>Δ'' : SimplexCategory<VAR>e : unop Δ' ⟶ Δ''<VAR>i : Δ'' ⟶ unop A.fst<VAR>inst✝¹ : Epi e<VAR>inst✝ : Mono i<VAR>fac : e ≫ i = θ.unop ≫ A.e<GOAL>(splitting K).ι (unop A.fst).len ≫ (obj K).map (A.e.op ≫ θ) = Termwise.mapMono K i ≫ (splitting K).ι Δ''.len ≫ map K (Splitting.IndexSet.mk e).e.op
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_2, u_1} C<VAR>inst✝³ : Preadditive C<VAR>K K' : ChainComplex C ℕ<VAR>f : K ⟶ K'<VAR>Δ✝ Δ'✝ Δ''✝ : SimplexCategory<VAR>inst✝² : HasFiniteCoproducts C<VAR>Δ Δ' : SimplexCategoryᵒᵖ<VAR>A : Splitting.IndexSet Δ<VAR>θ : Δ ⟶ Δ'<VAR>Δ'' : SimplexCategory<VAR>e : unop Δ' ⟶ Δ''<VAR>i : Δ'' ⟶ unop A.fst<VAR>inst✝¹ : Epi e<VAR>inst✝ : Mono i<VAR>fac : e ≫ i = θ.unop ≫ A.e<GOAL>Sigma.ι (summand K A.fst) (Splitting.IndexSet.id A.fst) ≫ map K (A.e.op ≫ θ) = Termwise.mapMono K i ≫ Sigma.ι (summand K (op Δ'')) (Splitting.IndexSet.id (op Δ'')) ≫ map K (Splitting.IndexSet.mk e).e.op
<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>K L M : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ γ₁ γ₂ : Cochain K L n<VAR>a n' : ℤ<VAR>hn' : n + a = n'<VAR>γ' : Cochain L M 0<GOAL>(γ.comp γ' ⋯).leftShift a n' hn' = (γ.leftShift a n' hn').comp γ' ⋯
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → PartialOrder (α i)<VAR>f : (i : ι) → α i<VAR>i : ι<VAR>a : α i<GOAL>update f i '' Ico a (f i) = Ico (update f i a) f
<VAR>A : Type u_1<VAR>inst✝³ : AddCommGroup A<VAR>inst✝² : Module ℂ A<VAR>inst✝¹ : StarAddMonoid A<VAR>inst✝ : StarModule ℂ A<VAR>z : ℂ<VAR>a : A<GOAL>ℜ (z • a) = z.re • ℜ a - z.im • ℑ a
<VAR>A : Type u_1<VAR>inst✝³ : AddCommGroup A<VAR>inst✝² : Module ℂ A<VAR>inst✝¹ : StarAddMonoid A<VAR>inst✝ : StarModule ℂ A<VAR>z : ℂ<VAR>a : A<VAR>this : ℜ (z • a) = ℜ ((↑z.re + ↑z.im * I) • a)<GOAL>ℜ (z • a) = z.re • ℜ a - z.im • ℑ a
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁵ : Category.{max v u, w} D<VAR>inst✝⁴ : ConcreteCategory D<VAR>inst✝³ : PreservesLimits (forget D)<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>P : Cᵒᵖ ⥤ D<VAR>hsep : ∀ (X : C) (S : J.Cover X) (x y : (forget D).obj (P.obj (op X))), (∀ (I : S.Arrow), (P.map I.f.op) x = (P.map I.f.op) y) → x = y<VAR>X : C<VAR>x y : (forget D).obj (P.obj (op X))<VAR>h : ((J.toPlus P).app (op X)) x = ((J.toPlus P).app (op X)) y<GOAL>x = y
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁵ : Category.{max v u, w} D<VAR>inst✝⁴ : ConcreteCategory D<VAR>inst✝³ : PreservesLimits (forget D)<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>P : Cᵒᵖ ⥤ D<VAR>hsep : ∀ (X : C) (S : J.Cover X) (x y : (forget D).obj (P.obj (op X))), (∀ (I : S.Arrow), (P.map I.f.op) x = (P.map I.f.op) y) → x = y<VAR>X : C<VAR>x y : (forget D).obj (P.obj (op X))<VAR>h : mk (Meq.mk ⊤ x) = mk (Meq.mk ⊤ y)<GOAL>x = y
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁵ : Category.{max v u, w} D<VAR>inst✝⁴ : ConcreteCategory D<VAR>inst✝³ : PreservesLimits (forget D)<VAR>inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>P : Cᵒᵖ ⥤ D<VAR>hsep : ∀ (X : C) (S : J.Cover X) (x y : (forget D).obj (P.obj (op X))), (∀ (I : S.Arrow), (P.map I.f.op) x = (P.map I.f.op) y) → x = y<VAR>X : C<VAR>x y : (forget D).obj (P.obj (op X))<VAR>h : ∃ W h1 h2, (Meq.mk ⊤ x).refine h1 = (Meq.mk ⊤ y).refine h2<GOAL>x = y
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>P : IntermediateField F E → Prop<VAR>base : P ⊥<VAR>ih : ∀ (K : IntermediateField F E) (x : E), P K → P (restrictScalars F (↥K)⟮x⟯)<VAR>S : Finset E<GOAL>P (adjoin F ↑S)
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>κ : ι → Sort u_3<VAR>β : Type u_4<VAR>inst✝ : SetLike α β<VAR>l : LowerAdjoint SetLike.coe<VAR>x y : α<GOAL>l.toFun (↑(l.toFun ↑x) ∪ ↑(l.toFun ↑y)) = l.toFun (↑x ∪ ↑y)
<VAR>x y : ℝ<VAR>hx : 0 ≤ x<VAR>hy : 0 ≤ y<VAR>h : √x = y<GOAL>y * y = x
<VAR>x y : ℝ<VAR>hx : 0 ≤ x<VAR>hy : 0 ≤ y<VAR>h : y * y = x<GOAL>√x = y
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Preorder α<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<VAR>inst✝ : LocallyFiniteOrderTop α<GOAL>Ioo a b ⊆ Ioi a
<VAR>p : ℝ[X]<VAR>z : ℂ<VAR>h0 : (aeval z) p = 0<VAR>hz : z.im ≠ 0<GOAL>X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2) ∣ p
<VAR>p : ℝ[X]<VAR>z : ℂ<VAR>h0 : (aeval z) p = 0<VAR>hz : z.im ≠ 0<GOAL>map (algebraMap ℝ ℂ) (X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2)) ∣ map (algebraMap ℝ ℂ) p
<VAR>p : ℝ[X]<VAR>z : ℂ<VAR>h0 : (aeval z) p = 0<VAR>hz : z.im ≠ 0<GOAL>map (algebraMap ℝ ℂ) (X ^ 2 - C (2 * z.re) * X + C (‖z‖ ^ 2)) = (X - C ((starRingEnd ℂ) z)) * (X - C z)
<VAR>R : Type uR<VAR>inst✝³ : Semiring R<VAR>S : Type uS<VAR>inst✝² : CommSemiring S<VAR>T : Type uT<VAR>A : Type uA<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra S A<VAR>r✝ r : R → R → Prop<GOAL>Function.Surjective ⇑(mkRingHom r)
<VAR>R : Type uR<VAR>inst✝³ : Semiring R<VAR>S : Type uS<VAR>inst✝² : CommSemiring S<VAR>T : Type uT<VAR>A : Type uA<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra S A<VAR>r✝ r : R → R → Prop<GOAL>Function.Surjective fun x => { toQuot := Quot.mk (Rel r) x }
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝³ : OrderedCancelAddCommMonoid α<VAR>inst✝² : ExistsAddOfLE α<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>inst✝ : DecidableEq α<VAR>a b c : α<GOAL>image (fun x => c + x) (Ioc a b) = Ioc (c + a) (c + b)
<VAR>R : Type u_1<VAR>inst✝² : CommSemiring R<VAR>M : Type u_2<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>m : M<GOAL>(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m) = (ι R) m
<VAR>R : Type u_1<VAR>inst✝² : CommSemiring R<VAR>M : Type u_2<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>m : M<GOAL>(RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m) = { toFun := fun m => (RingQuot.mkAlgHom R (Rel R M)) (FreeAlgebra.ι R m), map_add' := ⋯, map_smul' := ⋯ } m
<VAR>α : Type u_1<VAR>β✝ : α → Type u<VAR>δ : α → Sort v<VAR>inst✝ : DecidableEq α<VAR>s✝ : Finset α<VAR>t : (a : α) → Finset (β✝ a)<VAR>β : Type u_2<VAR>s : Finset α<VAR>f : α → β<GOAL>(s.pi fun a => {f a}) = {fun a x => f a}
<VAR>α : Type u_1<VAR>β✝ : α → Type u<VAR>δ : α → Sort v<VAR>inst✝ : DecidableEq α<VAR>s✝ : Finset α<VAR>t : (a : α) → Finset (β✝ a)<VAR>β : Type u_2<VAR>s : Finset α<VAR>f : α → β<GOAL>((fun a x => f a) ∈ s.pi fun a => {f a}) ∧ ∀ x ∈ s.pi fun a => {f a}, x = fun a x => f a
<VAR>α : Type u_1<VAR>β✝ : α → Type u<VAR>δ : α → Sort v<VAR>inst✝ : DecidableEq α<VAR>s✝ : Finset α<VAR>t : (a : α) → Finset (β✝ a)<VAR>β : Type u_2<VAR>s : Finset α<VAR>f : α → β<VAR>a : (a : α) → a ∈ s → β<VAR>ha : a ∈ s.pi fun a => {f a}<VAR>i : α<VAR>hi : i ∈ s<GOAL>a i hi = f i
<VAR>α : Type u_1<VAR>β✝ : α → Type u<VAR>δ : α → Sort v<VAR>inst✝ : DecidableEq α<VAR>s✝ : Finset α<VAR>t : (a : α) → Finset (β✝ a)<VAR>β : Type u_2<VAR>s : Finset α<VAR>f : α → β<VAR>a : (a : α) → a ∈ s → β<VAR>ha : ∀ (a_1 : α) (h : a_1 ∈ s), a a_1 h ∈ {f a_1}<VAR>i : α<VAR>hi : i ∈ s<GOAL>a i hi = f i
<VAR>P : MorphismProperty Scheme<VAR>Q : AffineTargetMorphismProperty<VAR>inst✝¹ : HasAffineProperty P Q<VAR>X✝ Y✝ : Scheme<VAR>f✝ : X✝ ⟶ Y✝<VAR>hP' : Q.StableUnderBaseChange<VAR>X Y S : Scheme<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>inst✝ : IsAffine S<VAR>H : Q g<GOAL>P (pullback.fst f g)
<VAR>P : MorphismProperty Scheme<VAR>Q : AffineTargetMorphismProperty<VAR>inst✝¹ : HasAffineProperty P Q<VAR>X✝ Y✝ : Scheme<VAR>f✝ : X✝ ⟶ Y✝<VAR>hP' : Q.StableUnderBaseChange<VAR>X Y S : Scheme<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>inst✝ : IsAffine S<VAR>H : Q g<VAR>this : Q.IsLocal := isLocal_affineProperty P<GOAL>P (pullback.fst f g)
<VAR>P : MorphismProperty Scheme<VAR>Q : AffineTargetMorphismProperty<VAR>inst✝¹ : HasAffineProperty P Q<VAR>X✝ Y✝ : Scheme<VAR>f✝ : X✝ ⟶ Y✝<VAR>hP' : Q.StableUnderBaseChange<VAR>X Y S : Scheme<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>inst✝ : IsAffine S<VAR>H : Q g<VAR>this : Q.IsLocal := isLocal_affineProperty P<GOAL>∀ (i : (X.affineCover.pullbackCover (pullback.fst f g)).J), Q (X.affineCover.pullbackHom (pullback.fst f g) i)
<VAR>P : MorphismProperty Scheme<VAR>Q : AffineTargetMorphismProperty<VAR>inst✝¹ : HasAffineProperty P Q<VAR>X✝ Y✝ : Scheme<VAR>f✝ : X✝ ⟶ Y✝<VAR>hP' : Q.StableUnderBaseChange<VAR>X Y S : Scheme<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>inst✝ : IsAffine S<VAR>H : Q g<VAR>this✝ : Q.IsLocal := isLocal_affineProperty P<VAR>i : (X.affineCover.pullbackCover (pullback.fst f g)).J<VAR>e : pullback (pullback.fst f g) (X.affineCover.map i) ≅ pullback (X.affineCover.map i ≫ f) g := pullbackSymmetry (pullback.fst f g) (X.affineCover.map i) ≪≫ pullbackRightPullbackFstIso f g (X.affineCover.map i)<VAR>this : e.hom ≫ pullback.fst (X.affineCover.map i ≫ f) g = X.affineCover.pullbackHom (pullback.fst f g) i<GOAL>Q (X.affineCover.pullbackHom (pullback.fst f g) i)