ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>inst✝¹⁰ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R M<VAR>Q : QuadraticForm R M<VAR>n : ℕ<VAR>A : Type u_3<VAR>inst✝⁷ : Semiring A<VAR>inst✝⁶ : Algebra R A<VAR>M₁ : Type u_4<VAR>M₂ : Type u_5<VAR>M₃ : Type u_6<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : AddCommGroup M₃<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : Module R M₂<VAR>inst✝ : Module R M₃<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>Q₃ : QuadraticForm R M₃<VAR>e : QuadraticMap.IsometryEquiv Q₁ Q₂<GOAL>map (e.toIsometry.comp e.symm.toIsometry) = AlgHom.id R (CliffordAlgebra Q₂)
<VAR>R : Type u_1<VAR>inst✝¹⁰ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R M<VAR>Q : QuadraticForm R M<VAR>n : ℕ<VAR>A : Type u_3<VAR>inst✝⁷ : Semiring A<VAR>inst✝⁶ : Algebra R A<VAR>M₁ : Type u_4<VAR>M₂ : Type u_5<VAR>M₃ : Type u_6<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : AddCommGroup M₃<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : Module R M₂<VAR>inst✝ : Module R M₃<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>Q₃ : QuadraticForm R M₃<VAR>e : QuadraticMap.IsometryEquiv Q₁ Q₂<GOAL>e.toIsometry.comp e.symm.toIsometry = QuadraticMap.Isometry.id Q₂
<VAR>R : Type u_1<VAR>inst✝¹⁰ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R M<VAR>Q : QuadraticForm R M<VAR>n : ℕ<VAR>A : Type u_3<VAR>inst✝⁷ : Semiring A<VAR>inst✝⁶ : Algebra R A<VAR>M₁ : Type u_4<VAR>M₂ : Type u_5<VAR>M₃ : Type u_6<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : AddCommGroup M₃<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : Module R M₂<VAR>inst✝ : Module R M₃<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>Q₃ : QuadraticForm R M₃<VAR>e : QuadraticMap.IsometryEquiv Q₁ Q₂<VAR>m : M₂<GOAL>(e.toIsometry.comp e.symm.toIsometry) m = (QuadraticMap.Isometry.id Q₂) m
<VAR>R : Type u_1<VAR>inst✝¹⁰ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R M<VAR>Q : QuadraticForm R M<VAR>n : ℕ<VAR>A : Type u_3<VAR>inst✝⁷ : Semiring A<VAR>inst✝⁶ : Algebra R A<VAR>M₁ : Type u_4<VAR>M₂ : Type u_5<VAR>M₃ : Type u_6<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : AddCommGroup M₃<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : Module R M₂<VAR>inst✝ : Module R M₃<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>Q₃ : QuadraticForm R M₃<VAR>e : QuadraticMap.IsometryEquiv Q₁ Q₂<GOAL>map (e.symm.toIsometry.comp e.toIsometry) = AlgHom.id R (CliffordAlgebra Q₁)
<VAR>R : Type u_1<VAR>inst✝¹⁰ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R M<VAR>Q : QuadraticForm R M<VAR>n : ℕ<VAR>A : Type u_3<VAR>inst✝⁷ : Semiring A<VAR>inst✝⁶ : Algebra R A<VAR>M₁ : Type u_4<VAR>M₂ : Type u_5<VAR>M₃ : Type u_6<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : AddCommGroup M₃<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : Module R M₂<VAR>inst✝ : Module R M₃<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>Q₃ : QuadraticForm R M₃<VAR>e : QuadraticMap.IsometryEquiv Q₁ Q₂<GOAL>e.symm.toIsometry.comp e.toIsometry = QuadraticMap.Isometry.id Q₁
<VAR>R : Type u_1<VAR>inst✝¹⁰ : CommRing R<VAR>M : Type u_2<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R M<VAR>Q : QuadraticForm R M<VAR>n : ℕ<VAR>A : Type u_3<VAR>inst✝⁷ : Semiring A<VAR>inst✝⁶ : Algebra R A<VAR>M₁ : Type u_4<VAR>M₂ : Type u_5<VAR>M₃ : Type u_6<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : AddCommGroup M₃<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : Module R M₂<VAR>inst✝ : Module R M₃<VAR>Q₁ : QuadraticForm R M₁<VAR>Q₂ : QuadraticForm R M₂<VAR>Q₃ : QuadraticForm R M₃<VAR>e : QuadraticMap.IsometryEquiv Q₁ Q₂<VAR>m : M₁<GOAL>(e.symm.toIsometry.comp e.toIsometry) m = (QuadraticMap.Isometry.id Q₁) m
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁵ : CommRing S<VAR>K : Type u_4<VAR>L : Type u_5<VAR>F : Type u_6<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : Field F<VAR>inst✝¹ : Algebra K S<VAR>inst✝ : Algebra K L<VAR>pb : PowerBasis K S<VAR>h_sep : IsSeparable K pb.gen<VAR>h_splits : Splits (algebraMap K L) (minpoly K pb.gen)<VAR>x✝ : Fintype (S →ₐ[K] L) := PowerBasis.AlgHom.fintype pb<GOAL>Fintype.card (S →ₐ[K] L) = pb.dim
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁵ : CommRing S<VAR>K : Type u_4<VAR>L : Type u_5<VAR>F : Type u_6<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : Field F<VAR>inst✝¹ : Algebra K S<VAR>inst✝ : Algebra K L<VAR>pb : PowerBasis K S<VAR>h_sep : IsSeparable K pb.gen<VAR>h_splits : Splits (algebraMap K L) (minpoly K pb.gen)<VAR>x✝ : Fintype (S →ₐ[K] L) := PowerBasis.AlgHom.fintype pb<GOAL>((minpoly K pb.gen).aroots L).Nodup
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝ : PartialOrder ι<VAR>τ : Ω → ι<VAR>f : Filtration ι m<VAR>hτ : IsStoppingTime f τ<VAR>h_countable : (Set.range τ).Countable<VAR>i : ι<GOAL>MeasurableSet {ω | τ ω < i}
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝ : PartialOrder ι<VAR>τ : Ω → ι<VAR>f : Filtration ι m<VAR>hτ : IsStoppingTime f τ<VAR>h_countable : (Set.range τ).Countable<VAR>i : ι<VAR>this : {ω | τ ω < i} = {ω | τ ω ≤ i} \ {ω | τ ω = i}<GOAL>MeasurableSet {ω | τ ω < i}
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝ : PartialOrder ι<VAR>τ : Ω → ι<VAR>f : Filtration ι m<VAR>hτ : IsStoppingTime f τ<VAR>h_countable : (Set.range τ).Countable<VAR>i : ι<VAR>this : {ω | τ ω < i} = {ω | τ ω ≤ i} \ {ω | τ ω = i}<GOAL>MeasurableSet ({ω | τ ω ≤ i} \ {ω | τ ω = i})
<VAR>α : Type u<VAR>l l' l✝ : List α<VAR>n m : ℕ<GOAL>l✝.rotate (n + m) = (l✝.rotate n).rotate m
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ✝ ε : ℝ<VAR>s t : Set α<VAR>x : α<VAR>δ : ℝ<VAR>E : Set α<GOAL>cthickening δ E = ⋂ ε, ⋂ (_ : max 0 δ < ε), thickening ε E
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ✝ ε : ℝ<VAR>s t : Set α<VAR>x : α<VAR>δ : ℝ<VAR>E : Set α<GOAL>0 ≤ max 0 δ
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>a b C : ℝ<VAR>f g : ℂ → E<VAR>z : ℂ<VAR>hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo a b)<VAR>hB : ∃ c < π / (b - a), ∃ B, f =O[comap (_root_.abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)] fun z => expR (B * expR (c * |z.re|))<VAR>hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C<VAR>hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C<VAR>hza : a ≤ z.im<VAR>hzb : z.im ≤ b<GOAL>‖f z‖ ≤ C
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>a b C : ℝ<VAR>f g : ℂ → E<VAR>z : ℂ<VAR>hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo a b)<VAR>hB : ∃ c < π / (b - a), ∃ B, f =O[comap (_root_.abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo a b)] fun z => expR (B * expR (c * |z.re|))<VAR>hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C<VAR>hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C<VAR>hza : a = z.im ∨ a < z.im<VAR>hzb : z.im = b ∨ z.im < b<GOAL>‖f z‖ ≤ C
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>C✝ : ℝ<VAR>f g : ℂ → E<VAR>z : ℂ<VAR>C : ℝ<VAR>hC₀ : 0 < C<VAR>a b : ℝ<VAR>hza : a - b < z.im<VAR>hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C<VAR>hzb : z.im < a + b<VAR>hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C<VAR>hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))<VAR>hB : ∃ c < π / (a + b - (a - b)), ∃ B, f =O[comap (_root_.abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))] fun z => expR (B * expR (c * |z.re|))<VAR>hab : a - b < a + b<GOAL>‖f z‖ ≤ C
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>C✝ : ℝ<VAR>f g : ℂ → E<VAR>z : ℂ<VAR>C : ℝ<VAR>hC₀ : 0 < C<VAR>a b : ℝ<VAR>hza : a - b < z.im<VAR>hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C<VAR>hzb : z.im < a + b<VAR>hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C<VAR>hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))<VAR>hB : ∃ c < π / (a + b - (a - b)), ∃ B, f =O[comap (_root_.abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))] fun z => expR (B * expR (c * |z.re|))<VAR>hab : a - b < a + b<VAR>hb : 0 < b<GOAL>‖f z‖ ≤ C
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>C✝ : ℝ<VAR>f g : ℂ → E<VAR>z : ℂ<VAR>C : ℝ<VAR>hC₀ : 0 < C<VAR>a b : ℝ<VAR>hza : a - b < z.im<VAR>hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C<VAR>hzb : z.im < a + b<VAR>hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C<VAR>hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))<VAR>hB : ∃ c < π / 2 / b, ∃ B, f =O[comap (_root_.abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))] fun z => expR (B * expR (c * |z.re|))<VAR>hab : a - b < a + b<VAR>hb : 0 < b<GOAL>‖f z‖ ≤ C
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>C✝ : ℝ<VAR>f g : ℂ → E<VAR>z : ℂ<VAR>C : ℝ<VAR>hC₀ : 0 < C<VAR>a b : ℝ<VAR>hza : a - b < z.im<VAR>hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C<VAR>hzb : z.im < a + b<VAR>hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C<VAR>hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))<VAR>hB : ∃ c < π / 2 / b, ∃ B, f =O[comap (_root_.abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))] fun z => expR (B * expR (c * |z.re|))<VAR>hab : a - b < a + b<VAR>hb : 0 < b<VAR>hπb : 0 < π / 2 / b<GOAL>‖f z‖ ≤ C
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>C✝ : ℝ<VAR>f g : ℂ → E<VAR>z : ℂ<VAR>C : ℝ<VAR>hC₀ : 0 < C<VAR>a b : ℝ<VAR>hza : a - b < z.im<VAR>hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C<VAR>hzb : z.im < a + b<VAR>hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C<VAR>hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))<VAR>hab : a - b < a + b<VAR>hb : 0 < b<VAR>hπb : 0 < π / 2 / b<VAR>c : ℝ<VAR>hc : c < π / 2 / b<VAR>B : ℝ<VAR>hO : f =O[comap (_root_.abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))] fun z => expR (B * expR (c * |z.re|))<GOAL>‖f z‖ ≤ C
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>C✝ : ℝ<VAR>f g : ℂ → E<VAR>z : ℂ<VAR>C : ℝ<VAR>hC₀ : 0 < C<VAR>a b : ℝ<VAR>hza : a - b < z.im<VAR>hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C<VAR>hzb : z.im < a + b<VAR>hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C<VAR>hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))<VAR>hab : a - b < a + b<VAR>hb : 0 < b<VAR>hπb : 0 < π / 2 / b<VAR>c : ℝ<VAR>hc : c < π / 2 / b<VAR>B : ℝ<VAR>hO : f =O[comap (_root_.abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))] fun z => expR (B * expR (c * |z.re|))<VAR>d : ℝ<VAR>hd : d < π / 2 / b<VAR>hcd : c < d<VAR>hd₀ : 0 < d<GOAL>‖f z‖ ≤ C
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>C✝ : ℝ<VAR>f g : ℂ → E<VAR>z : ℂ<VAR>C : ℝ<VAR>hC₀ : 0 < C<VAR>a b : ℝ<VAR>hza : a - b < z.im<VAR>hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C<VAR>hzb : z.im < a + b<VAR>hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C<VAR>hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))<VAR>hab : a - b < a + b<VAR>hb : 0 < b<VAR>hπb : 0 < π / 2 / b<VAR>c : ℝ<VAR>hc : c < π / 2 / b<VAR>B : ℝ<VAR>hO : f =O[comap (_root_.abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))] fun z => expR (B * expR (c * |z.re|))<VAR>d : ℝ<VAR>hd : d < π / 2 / b<VAR>hcd : c < d<VAR>hd₀ : 0 < d<VAR>hb' : d * b < π / 2<GOAL>‖f z‖ ≤ C
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>C✝ : ℝ<VAR>f g✝ : ℂ → E<VAR>z : ℂ<VAR>C : ℝ<VAR>hC₀ : 0 < C<VAR>a b : ℝ<VAR>hza : a - b < z.im<VAR>hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C<VAR>hzb : z.im < a + b<VAR>hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C<VAR>hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))<VAR>hab : a - b < a + b<VAR>hb : 0 < b<VAR>hπb : 0 < π / 2 / b<VAR>c : ℝ<VAR>hc : c < π / 2 / b<VAR>B : ℝ<VAR>hO : f =O[comap (_root_.abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))] fun z => expR (B * expR (c * |z.re|))<VAR>d : ℝ<VAR>hd : d < π / 2 / b<VAR>hcd : c < d<VAR>hd₀ : 0 < d<VAR>hb' : d * b < π / 2<VAR>aff : ℂ → ℂ := fun w => ↑d * (w - ↑a * I)<VAR>g : ℝ → ℂ → ℂ := fun ε w => cexp (↑ε * (cexp (aff w) + cexp (-aff w)))<GOAL>‖f z‖ ≤ C
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>C✝ : ℝ<VAR>f g✝ : ℂ → E<VAR>z : ℂ<VAR>C : ℝ<VAR>hC₀ : 0 < C<VAR>a b : ℝ<VAR>hza : a - b < z.im<VAR>hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C<VAR>hzb : z.im < a + b<VAR>hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C<VAR>hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))<VAR>hab : a - b < a + b<VAR>hb : 0 < b<VAR>hπb : 0 < π / 2 / b<VAR>c : ℝ<VAR>hc : c < π / 2 / b<VAR>B : ℝ<VAR>hO : f =O[comap (_root_.abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))] fun z => expR (B * expR (c * |z.re|))<VAR>d : ℝ<VAR>hd : d < π / 2 / b<VAR>hcd : c < d<VAR>hd₀ : 0 < d<VAR>hb' : d * b < π / 2<VAR>aff : ℂ → ℂ := fun w => ↑d * (w - ↑a * I)<VAR>g : ℝ → ℂ → ℂ := fun ε w => cexp (↑ε * (cexp (aff w) + cexp (-aff w)))<GOAL>∀ᶠ (ε : ℝ) in 𝓝[<] 0, ‖g ε z • f z‖ ≤ C
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>C✝ : ℝ<VAR>f g✝ : ℂ → E<VAR>z : ℂ<VAR>C : ℝ<VAR>hC₀ : 0 < C<VAR>a b : ℝ<VAR>hza : a - b < z.im<VAR>hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C<VAR>hzb : z.im < a + b<VAR>hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C<VAR>hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))<VAR>hab : a - b < a + b<VAR>hb : 0 < b<VAR>hπb : 0 < π / 2 / b<VAR>c : ℝ<VAR>hc : c < π / 2 / b<VAR>B : ℝ<VAR>hO : f =O[comap (_root_.abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))] fun z => expR (B * expR (c * |z.re|))<VAR>d : ℝ<VAR>hd : d < π / 2 / b<VAR>hcd : c < d<VAR>hd₀ : 0 < d<VAR>hb' : d * b < π / 2<VAR>aff : ℂ → ℂ := fun w => ↑d * (w - ↑a * I)<VAR>g : ℝ → ℂ → ℂ := fun ε w => cexp (↑ε * (cexp (aff w) + cexp (-aff w)))<VAR>ε : ℝ<VAR>ε₀ : ε ∈ Iio 0<GOAL>‖g ε z • f z‖ ≤ C
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>C✝ : ℝ<VAR>f g✝ : ℂ → E<VAR>z : ℂ<VAR>C : ℝ<VAR>hC₀ : 0 < C<VAR>a b : ℝ<VAR>hza : a - b < z.im<VAR>hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C<VAR>hzb : z.im < a + b<VAR>hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C<VAR>hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))<VAR>hab : a - b < a + b<VAR>hb : 0 < b<VAR>hπb : 0 < π / 2 / b<VAR>c : ℝ<VAR>hc : c < π / 2 / b<VAR>B : ℝ<VAR>hO : f =O[comap (_root_.abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))] fun z => expR (B * expR (c * |z.re|))<VAR>d : ℝ<VAR>hd : d < π / 2 / b<VAR>hcd : c < d<VAR>hd₀ : 0 < d<VAR>hb' : d * b < π / 2<VAR>aff : ℂ → ℂ := fun w => ↑d * (w - ↑a * I)<VAR>g : ℝ → ℂ → ℂ := fun ε w => cexp (↑ε * (cexp (aff w) + cexp (-aff w)))<VAR>ε : ℝ<VAR>ε₀ : ε < 0<GOAL>‖g ε z • f z‖ ≤ C
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>C✝ : ℝ<VAR>f g✝ : ℂ → E<VAR>z : ℂ<VAR>C : ℝ<VAR>hC₀ : 0 < C<VAR>a b : ℝ<VAR>hza : a - b < z.im<VAR>hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C<VAR>hzb : z.im < a + b<VAR>hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C<VAR>hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))<VAR>hab : a - b < a + b<VAR>hb : 0 < b<VAR>hπb : 0 < π / 2 / b<VAR>c : ℝ<VAR>hc : c < π / 2 / b<VAR>B : ℝ<VAR>hO : f =O[comap (_root_.abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))] fun z => expR (B * expR (c * |z.re|))<VAR>d : ℝ<VAR>hd : d < π / 2 / b<VAR>hcd : c < d<VAR>hd₀ : 0 < d<VAR>hb' : d * b < π / 2<VAR>aff : ℂ → ℂ := fun w => ↑d * (w - ↑a * I)<VAR>g : ℝ → ℂ → ℂ := fun ε w => cexp (↑ε * (cexp (aff w) + cexp (-aff w)))<VAR>ε : ℝ<VAR>ε₀ : ε < 0<VAR>δ : ℝ<VAR>δ₀ : δ < 0<VAR>hδ : ∀ ⦃w : ℂ⦄, w.im ∈ Icc (a - b) (a + b) → Complex.abs (g ε w) ≤ expR (δ * expR (d * |w.re|))<GOAL>‖g ε z • f z‖ ≤ C
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>C✝ : ℝ<VAR>f g✝ : ℂ → E<VAR>z : ℂ<VAR>C : ℝ<VAR>hC₀ : 0 < C<VAR>a b : ℝ<VAR>hza : a - b < z.im<VAR>hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C<VAR>hzb : z.im < a + b<VAR>hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C<VAR>hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))<VAR>hab : a - b < a + b<VAR>hb : 0 < b<VAR>hπb : 0 < π / 2 / b<VAR>c : ℝ<VAR>hc : c < π / 2 / b<VAR>B : ℝ<VAR>hO : f =O[comap (_root_.abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))] fun z => expR (B * expR (c * |z.re|))<VAR>d : ℝ<VAR>hd : d < π / 2 / b<VAR>hcd : c < d<VAR>hd₀ : 0 < d<VAR>hb' : d * b < π / 2<VAR>aff : ℂ → ℂ := fun w => ↑d * (w - ↑a * I)<VAR>g : ℝ → ℂ → ℂ := fun ε w => cexp (↑ε * (cexp (aff w) + cexp (-aff w)))<VAR>ε : ℝ<VAR>ε₀ : ε < 0<VAR>δ : ℝ<VAR>δ₀ : δ < 0<VAR>hδ : ∀ ⦃w : ℂ⦄, w.im ∈ Icc (a - b) (a + b) → Complex.abs (g ε w) ≤ expR (δ * expR (d * |w.re|))<VAR>hg₁ : ∀ (w : ℂ), w.im = a - b ∨ w.im = a + b → Complex.abs (g ε w) ≤ 1<GOAL>‖g ε z • f z‖ ≤ C
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>C✝ : ℝ<VAR>f g✝ : ℂ → E<VAR>z : ℂ<VAR>C : ℝ<VAR>hC₀ : 0 < C<VAR>a b : ℝ<VAR>hza : a - b < z.im<VAR>hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C<VAR>hzb : z.im < a + b<VAR>hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C<VAR>hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))<VAR>hab : a - b < a + b<VAR>hb : 0 < b<VAR>hπb : 0 < π / 2 / b<VAR>c : ℝ<VAR>hc : c < π / 2 / b<VAR>B : ℝ<VAR>hO : f =O[comap (_root_.abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))] fun z => expR (B * expR (c * |z.re|))<VAR>d : ℝ<VAR>hd : d < π / 2 / b<VAR>hcd : c < d<VAR>hd₀ : 0 < d<VAR>hb' : d * b < π / 2<VAR>aff : ℂ → ℂ := fun w => ↑d * (w - ↑a * I)<VAR>g : ℝ → ℂ → ℂ := fun ε w => cexp (↑ε * (cexp (aff w) + cexp (-aff w)))<VAR>ε : ℝ<VAR>ε₀ : ε < 0<VAR>δ : ℝ<VAR>δ₀ : δ < 0<VAR>hδ : ∀ ⦃w : ℂ⦄, w.im ∈ Icc (a - b) (a + b) → Complex.abs (g ε w) ≤ expR (δ * expR (d * |w.re|))<VAR>hg₁ : ∀ (w : ℂ), w.im = a - b ∨ w.im = a + b → Complex.abs (g ε w) ≤ 1<VAR>R : ℝ<VAR>hzR : |z.re| < R<VAR>hR : ∀ (w : ℂ), |w.re| = R → w.im ∈ Ioo (a - b) (a + b) → ‖g ε w • f w‖ ≤ C<GOAL>‖g ε z • f z‖ ≤ C
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>C✝ : ℝ<VAR>f g✝ : ℂ → E<VAR>z : ℂ<VAR>C : ℝ<VAR>hC₀ : 0 < C<VAR>a b : ℝ<VAR>hza : a - b < z.im<VAR>hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C<VAR>hzb : z.im < a + b<VAR>hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C<VAR>hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))<VAR>hab : a - b < a + b<VAR>hb : 0 < b<VAR>hπb : 0 < π / 2 / b<VAR>c : ℝ<VAR>hc : c < π / 2 / b<VAR>B : ℝ<VAR>hO : f =O[comap (_root_.abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))] fun z => expR (B * expR (c * |z.re|))<VAR>d : ℝ<VAR>hd : d < π / 2 / b<VAR>hcd : c < d<VAR>hd₀ : 0 < d<VAR>hb' : d * b < π / 2<VAR>aff : ℂ → ℂ := fun w => ↑d * (w - ↑a * I)<VAR>g : ℝ → ℂ → ℂ := fun ε w => cexp (↑ε * (cexp (aff w) + cexp (-aff w)))<VAR>ε : ℝ<VAR>ε₀ : ε < 0<VAR>δ : ℝ<VAR>δ₀ : δ < 0<VAR>hδ : ∀ ⦃w : ℂ⦄, w.im ∈ Icc (a - b) (a + b) → Complex.abs (g ε w) ≤ expR (δ * expR (d * |w.re|))<VAR>hg₁ : ∀ (w : ℂ), w.im = a - b ∨ w.im = a + b → Complex.abs (g ε w) ≤ 1<VAR>R : ℝ<VAR>hzR : |z.re| < R<VAR>hR : ∀ (w : ℂ), |w.re| = R → w.im ∈ Ioo (a - b) (a + b) → ‖g ε w • f w‖ ≤ C<VAR>hR₀ : 0 < R<GOAL>‖g ε z • f z‖ ≤ C
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>C✝ : ℝ<VAR>f g✝ : ℂ → E<VAR>z : ℂ<VAR>C : ℝ<VAR>hC₀ : 0 < C<VAR>a b : ℝ<VAR>hza : a - b < z.im<VAR>hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C<VAR>hzb : z.im < a + b<VAR>hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C<VAR>hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))<VAR>hab : a - b < a + b<VAR>hb : 0 < b<VAR>hπb : 0 < π / 2 / b<VAR>c : ℝ<VAR>hc : c < π / 2 / b<VAR>B : ℝ<VAR>hO : f =O[comap (_root_.abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))] fun z => expR (B * expR (c * |z.re|))<VAR>d : ℝ<VAR>hd : d < π / 2 / b<VAR>hcd : c < d<VAR>hd₀ : 0 < d<VAR>hb' : d * b < π / 2<VAR>aff : ℂ → ℂ := fun w => ↑d * (w - ↑a * I)<VAR>g : ℝ → ℂ → ℂ := fun ε w => cexp (↑ε * (cexp (aff w) + cexp (-aff w)))<VAR>ε : ℝ<VAR>ε₀ : ε < 0<VAR>δ : ℝ<VAR>δ₀ : δ < 0<VAR>hδ : ∀ ⦃w : ℂ⦄, w.im ∈ Icc (a - b) (a + b) → Complex.abs (g ε w) ≤ expR (δ * expR (d * |w.re|))<VAR>hg₁ : ∀ (w : ℂ), w.im = a - b ∨ w.im = a + b → Complex.abs (g ε w) ≤ 1<VAR>R : ℝ<VAR>hzR : |z.re| < R<VAR>hR : ∀ (w : ℂ), |w.re| = R → w.im ∈ Ioo (a - b) (a + b) → ‖g ε w • f w‖ ≤ C<VAR>hR₀ : 0 < R<VAR>hgd : Differentiable ℂ (g ε)<GOAL>‖g ε z • f z‖ ≤ C
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>C✝ : ℝ<VAR>f g✝ : ℂ → E<VAR>z : ℂ<VAR>C : ℝ<VAR>hC₀ : 0 < C<VAR>a b : ℝ<VAR>hza : a - b < z.im<VAR>hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C<VAR>hzb : z.im < a + b<VAR>hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C<VAR>hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))<VAR>hab : a - b < a + b<VAR>hb : 0 < b<VAR>hπb : 0 < π / 2 / b<VAR>c : ℝ<VAR>hc : c < π / 2 / b<VAR>B : ℝ<VAR>hO : f =O[comap (_root_.abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))] fun z => expR (B * expR (c * |z.re|))<VAR>d : ℝ<VAR>hcd : c < d<VAR>hd₀ : 0 < d<VAR>hb' : d * b < π / 2<VAR>aff : ℂ → ℂ := fun w => ↑d * (w - ↑a * I)<VAR>g : ℝ → ℂ → ℂ := fun ε w => cexp (↑ε * (cexp (aff w) + cexp (-aff w)))<VAR>ε : ℝ<VAR>ε₀ : ε < 0<VAR>δ : ℝ<VAR>δ₀ : δ < 0<VAR>hδ : ∀ ⦃w : ℂ⦄, w.im ∈ Icc (a - b) (a + b) → Complex.abs (g ε w) ≤ expR (δ * expR (d * |w.re|))<VAR>hg₁ : ∀ (w : ℂ), w.im = a - b ∨ w.im = a + b → Complex.abs (g ε w) ≤ 1<VAR>R : ℝ<VAR>hzR : |z.re| < R<VAR>hR : ∀ (w : ℂ), |w.re| = R → w.im ∈ Ioo (a - b) (a + b) → ‖g ε w • f w‖ ≤ C<VAR>hR₀ : 0 < R<VAR>hgd : Differentiable ℂ (g ε)<VAR>hd : DiffContOnCl ℂ (fun w => g ε w • f w) (Ioo (-R) R ×ℂ Ioo (a - b) (a + b))<GOAL>‖g ε z • f z‖ ≤ C
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>C✝ : ℝ<VAR>f g✝ : ℂ → E<VAR>z : ℂ<VAR>C : ℝ<VAR>hC₀ : 0 < C<VAR>a b : ℝ<VAR>hza : a - b < z.im<VAR>hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C<VAR>hzb : z.im < a + b<VAR>hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C<VAR>hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))<VAR>hab : a - b < a + b<VAR>hb : 0 < b<VAR>hπb : 0 < π / 2 / b<VAR>c : ℝ<VAR>hc : c < π / 2 / b<VAR>B : ℝ<VAR>hO : f =O[comap (_root_.abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))] fun z => expR (B * expR (c * |z.re|))<VAR>d : ℝ<VAR>hcd : c < d<VAR>hd₀ : 0 < d<VAR>hb' : d * b < π / 2<VAR>aff : ℂ → ℂ := fun w => ↑d * (w - ↑a * I)<VAR>g : ℝ → ℂ → ℂ := fun ε w => cexp (↑ε * (cexp (aff w) + cexp (-aff w)))<VAR>ε : ℝ<VAR>ε₀ : ε < 0<VAR>δ : ℝ<VAR>δ₀ : δ < 0<VAR>hδ : ∀ ⦃w : ℂ⦄, w.im ∈ Icc (a - b) (a + b) → Complex.abs (g ε w) ≤ expR (δ * expR (d * |w.re|))<VAR>hg₁ : ∀ (w : ℂ), w.im = a - b ∨ w.im = a + b → Complex.abs (g ε w) ≤ 1<VAR>R : ℝ<VAR>hzR : |z.re| < R<VAR>hR : ∀ (w : ℂ), |w.re| = R → w.im ∈ Ioo (a - b) (a + b) → ‖g ε w • f w‖ ≤ C<VAR>hR₀ : 0 < R<VAR>hgd : Differentiable ℂ (g ε)<VAR>hd : DiffContOnCl ℂ (fun w => g ε w • f w) (Ioo (-R) R ×ℂ Ioo (a - b) (a + b))<VAR>w : ℂ<VAR>hw : w ∈ frontier (Ioo (-R) R ×ℂ Ioo (a - b) (a + b))<GOAL>‖g ε w • f w‖ ≤ C
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>C✝ : ℝ<VAR>f g✝ : ℂ → E<VAR>z : ℂ<VAR>C : ℝ<VAR>hC₀ : 0 < C<VAR>a b : ℝ<VAR>hza : a - b < z.im<VAR>hle_a : ∀ (z : ℂ), z.im = a - b → ‖f z‖ ≤ C<VAR>hzb : z.im < a + b<VAR>hle_b : ∀ (z : ℂ), z.im = a + b → ‖f z‖ ≤ C<VAR>hfd : DiffContOnCl ℂ f (im ⁻¹' Ioo (a - b) (a + b))<VAR>hab : a - b < a + b<VAR>hb : 0 < b<VAR>hπb : 0 < π / 2 / b<VAR>c : ℝ<VAR>hc : c < π / 2 / b<VAR>B : ℝ<VAR>hO : f =O[comap (_root_.abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo (a - b) (a + b))] fun z => expR (B * expR (c * |z.re|))<VAR>d : ℝ<VAR>hcd : c < d<VAR>hd₀ : 0 < d<VAR>hb' : d * b < π / 2<VAR>aff : ℂ → ℂ := fun w => ↑d * (w - ↑a * I)<VAR>g : ℝ → ℂ → ℂ := fun ε w => cexp (↑ε * (cexp (aff w) + cexp (-aff w)))<VAR>ε : ℝ<VAR>ε₀ : ε < 0<VAR>δ : ℝ<VAR>δ₀ : δ < 0<VAR>hδ : ∀ ⦃w : ℂ⦄, w.im ∈ Icc (a - b) (a + b) → Complex.abs (g ε w) ≤ expR (δ * expR (d * |w.re|))<VAR>hg₁ : ∀ (w : ℂ), w.im = a - b ∨ w.im = a + b → Complex.abs (g ε w) ≤ 1<VAR>R : ℝ<VAR>hzR : |z.re| < R<VAR>hR : ∀ (w : ℂ), |w.re| = R → w.im ∈ Ioo (a - b) (a + b) → ‖g ε w • f w‖ ≤ C<VAR>hR₀ : 0 < R<VAR>hgd : Differentiable ℂ (g ε)<VAR>hd : DiffContOnCl ℂ (fun w => g ε w • f w) (Ioo (-R) R ×ℂ Ioo (a - b) (a + b))<GOAL>z ∈ closure (Ioo (-R) R ×ℂ Ioo (a - b) (a + b))
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : CommRing T<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra R T<VAR>ι κ : Type w<VAR>inst✝¹ : Fintype ι<VAR>b✝ : Basis ι R S<VAR>inst✝ : DecidableEq ι<VAR>b : Basis ι R S<VAR>s : S<GOAL>(trace R S) s = ((leftMulMatrix b) s).trace