ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝² : AddMonoid A<VAR>inst✝¹ : AddMonoid B<VAR>φ : A →+ B<VAR>inst✝ : HasShift C B<VAR>X : PullbackShift C φ<VAR>a₁ a₂ : A<VAR>b₃ : B<VAR>h₃ : b₃ = φ (a₁ + a₂)<GOAL>(shiftFunctorAdd' (PullbackShift C φ) a₁ a₂ (a₁ + a₂) ⋯).inv.app X = (shiftFunctor (PullbackShift C φ) a₂).map ((pullbackShiftIso C φ a₁ (φ a₁) ⋯).hom.app X) ≫ (pullbackShiftIso C φ a₂ (φ a₂) ⋯).hom.app ((shiftFunctor C (φ a₁)).obj X) ≫ (shiftFunctorAdd' C (φ a₁) (φ a₂) b₃ ⋯).inv.app X ≫ (pullbackShiftIso C φ (a₁ + a₂) b₃ h₃).inv.app X
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝² : AddMonoid A<VAR>inst✝¹ : AddMonoid B<VAR>φ : A →+ B<VAR>inst✝ : HasShift C B<VAR>X : PullbackShift C φ<VAR>a₁ a₂ : A<VAR>h₃ : φ a₁ + φ a₂ = φ (a₁ + a₂)<GOAL>(shiftFunctorAdd' (PullbackShift C φ) a₁ a₂ (a₁ + a₂) ⋯).inv.app X = (shiftFunctor (PullbackShift C φ) a₂).map ((pullbackShiftIso C φ a₁ (φ a₁) ⋯).hom.app X) ≫ (pullbackShiftIso C φ a₂ (φ a₂) ⋯).hom.app ((shiftFunctor C (φ a₁)).obj X) ≫ (shiftFunctorAdd' C (φ a₁) (φ a₂) (φ a₁ + φ a₂) ⋯).inv.app X ≫ (pullbackShiftIso C φ (a₁ + a₂) (φ a₁ + φ a₂) h₃).inv.app X
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝² : AddMonoid A<VAR>inst✝¹ : AddMonoid B<VAR>φ : A →+ B<VAR>inst✝ : HasShift C B<VAR>X : PullbackShift C φ<VAR>a₁ a₂ : A<VAR>h₃ : φ a₁ + φ a₂ = φ (a₁ + a₂)<GOAL>(shiftFunctorAdd (PullbackShift C φ) a₁ a₂).inv.app X = (shiftFunctorAdd C (φ a₁) (φ a₂)).inv.app X ≫ (pullbackShiftIso C φ (a₁ + a₂) (φ a₁ + φ a₂) h₃).inv.app X
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝² : AddMonoid A<VAR>inst✝¹ : AddMonoid B<VAR>φ : A →+ B<VAR>inst✝ : HasShift C B<VAR>X : PullbackShift C φ<VAR>a₁ a₂ : A<VAR>h₃ : φ a₁ + φ a₂ = φ (a₁ + a₂)<GOAL>HasShift.shift.map (eqToHom ⋯) = (pullbackShiftIso C φ (a₁ + a₂) (φ a₁ + φ a₂) h₃).inv
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>x✝ y z : α<VAR>ε ε₁ ε₂ : ℝ≥0∞<VAR>s t✝ t : Set α<VAR>h : (s ∩ t).Nonempty<VAR>x : α<VAR>xs : x ∈ s<VAR>xt : x ∈ t<GOAL>diam (s ∪ t) ≤ diam s + diam t
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s : Finset α<VAR>a : α<VAR>n : ℕ<VAR>h : 𝒜.Shatters s<VAR>u : Finset α<VAR>left✝ : u ∈ 𝒜<GOAL>s ∩ u ⊆ s
<VAR>α : Type u<VAR>L✝ L₁ L₂ L₃ L₄ : List (α × Bool)<VAR>inst✝ : DecidableEq α<VAR>x✝ : FreeGroup α<VAR>L : List (α × Bool)<GOAL>mk (toWord (Quot.mk Red.Step L)) = Quot.mk Red.Step L
<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>k : ℕ<VAR>N : LieSubmodule R L M<VAR>M₂ : Type w₁<VAR>inst✝⁵ : AddCommGroup M₂<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : LieRingModule L M₂<VAR>inst✝² : LieModule R L M₂<VAR>inst✝¹ : Nontrivial M<VAR>inst✝ : IsNilpotent R L M<GOAL>Nontrivial ↥↑(lowerCentralSeriesLast R L M)
<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>k : ℕ<VAR>N : LieSubmodule R L M<VAR>M₂ : Type w₁<VAR>inst✝⁵ : AddCommGroup M₂<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : LieRingModule L M₂<VAR>inst✝² : LieModule R L M₂<VAR>inst✝¹ : Nontrivial M<VAR>inst✝ : IsNilpotent R L M<GOAL>(match nilpotencyLength R L M with | 0 => ⊥ | k.succ => lowerCentralSeries R L M k) ≠ ⊥
<VAR>x y : ℂ<GOAL>cosh (x - y) = cosh x * cosh y - sinh x * sinh y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α →ₛ ℝ≥0∞<GOAL>(map Prod.fst (f.pair g)).lintegral μ ⊔ (map Prod.snd (f.pair g)).lintegral μ ≤ ∑ x ∈ (f.pair g).range, (x.1 ⊔ x.2) * μ (↑(f.pair g) ⁻¹' {x})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α →ₛ ℝ≥0∞<GOAL>(∑ x ∈ (f.pair g).range, x.1 * μ (↑(f.pair g) ⁻¹' {x})) ⊔ ∑ x ∈ (f.pair g).range, x.2 * μ (↑(f.pair g) ⁻¹' {x}) ≤ ∑ x ∈ (f.pair g).range, (x.1 ⊔ x.2) * μ (↑(f.pair g) ⁻¹' {x})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α →ₛ ℝ≥0∞<VAR>a : ℝ≥0∞ × ℝ≥0∞<VAR>x✝ : a ∈ (f.pair g).range<GOAL>a.1 ≤ a.1 ⊔ a.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α →ₛ ℝ≥0∞<VAR>a : ℝ≥0∞ × ℝ≥0∞<VAR>x✝ : a ∈ (f.pair g).range<GOAL>a.2 ≤ a.1 ⊔ a.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α →ₛ ℝ≥0∞<GOAL>∑ x ∈ (f.pair g).range, (x.1 ⊔ x.2) * μ (↑(f.pair g) ⁻¹' {x}) = (f ⊔ g).lintegral μ
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>h_nonempty : Nonempty ((i : ι) → α i)<VAR>s : Finset ι<VAR>S : Set ((i : { x // x ∈ s }) → α ↑i)<GOAL>cylinder s S = ∅ ↔ S = ∅
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>h_nonempty : Nonempty ((i : ι) → α i)<VAR>s : Finset ι<VAR>S : Set ((i : { x // x ∈ s }) → α ↑i)<VAR>h : cylinder s S = ∅<GOAL>S = ∅
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>h_nonempty : Nonempty ((i : ι) → α i)<VAR>s : Finset ι<VAR>S : Set ((i : { x // x ∈ s }) → α ↑i)<VAR>h : cylinder s S = ∅<VAR>hS : ¬S = ∅<GOAL>False
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>h_nonempty : Nonempty ((i : ι) → α i)<VAR>s : Finset ι<VAR>S : Set ((i : { x // x ∈ s }) → α ↑i)<VAR>h : cylinder s S = ∅<VAR>hS : S.Nonempty<GOAL>False
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>h_nonempty : Nonempty ((i : ι) → α i)<VAR>s : Finset ι<VAR>S : Set ((i : { x // x ∈ s }) → α ↑i)<VAR>h : cylinder s S = ∅<VAR>hS : S.Nonempty<VAR>f : (i : { x // x ∈ s }) → α ↑i := hS.some<GOAL>False
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>h_nonempty : Nonempty ((i : ι) → α i)<VAR>s : Finset ι<VAR>S : Set ((i : { x // x ∈ s }) → α ↑i)<VAR>h : cylinder s S = ∅<VAR>hS : S.Nonempty<VAR>f : (i : { x // x ∈ s }) → α ↑i := hS.some<VAR>hf : f ∈ S<GOAL>False
<VAR>R : Type u<VAR>inst✝⁶ : CommSemiring R<VAR>M : Type v<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>ι : Type w<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Fintype ι<VAR>κ : Type u_1<VAR>inst✝¹ : DecidableEq κ<VAR>inst✝ : Fintype κ<VAR>b : Basis ι R M<VAR>c : Basis κ R M<VAR>f g h : M →ₗ[R] M<GOAL>(trace R M) (f * g * h) = (trace R M) (h * f * g)
<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 - n⁆ = ⁅x, m⁆ - ⁅x, n⁆
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>n : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>ιM : Type u_7<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : AddCommGroup L<VAR>inst✝¹⁰ : Module R L<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>inst✝⁷ : Fintype ι<VAR>inst✝⁶ : Fintype ι'<VAR>inst✝⁵ : Fintype ιM<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : DecidableEq ι'<VAR>inst✝² : DecidableEq ιM<VAR>b : Basis ι R L<VAR>bₘ : Basis ιM R M<VAR>inst✝¹ : Module.Finite R M<VAR>inst✝ : Module.Free R M<VAR>x : L<VAR>a✝ : Nontrivial R<GOAL>Polynomial.map (MvPolynomial.eval ⇑(b.repr x)) (φ.polyCharpolyAux b bₘ) = charpoly (φ x)
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Type u_4<VAR>inst✝ : TopologicalSpace β<VAR>f : Filter τ<VAR>ϕ : τ → α → β<VAR>s s₁ s₂ : Set α<VAR>p : ι → Set α<GOAL>⋃ i, ω f ϕ (p i) ⊆ ω f ϕ (⋃ i, p i)
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Type u_4<VAR>inst✝ : TopologicalSpace β<VAR>f : Filter τ<VAR>ϕ : τ → α → β<VAR>s s₁ s₂ : Set α<VAR>p : ι → Set α<GOAL>∀ (i : ι), ω f ϕ (p i) ⊆ ω f ϕ (⋃ i, p i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>ι : Sort u_5<VAR>f : ι → α → ℝ≥0∞<GOAL>⨆ i, ∫⁻ (a : α), f i a ∂μ ≤ ∫⁻ (a : α), ⨆ i, f i a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>ι : Sort u_5<VAR>f : ι → α → ℝ≥0∞<GOAL>⨆ i, ∫⁻ (a : α), f i a ∂μ ≤ ∫⁻ (a : α), (⨆ i, f i) a ∂μ
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>a : α<VAR>r₁✝ r₁ : List (List α)<VAR>l : List α<VAR>ih : ∀ (r₂ : List (List α)), sublists'Aux a r₁ r₂ = r₂ ++ map (cons a) r₁<VAR>r₂ : List (List α)<GOAL>sublists'Aux a (r₁ ++ [l]) r₂ = r₂ ++ map (cons a) (r₁ ++ [l])
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>a : α<VAR>r₁✝ r₁ : List (List α)<VAR>l : List α<VAR>ih : ∀ (r₂ : List (List α)), sublists'Aux a r₁ r₂ = r₂ ++ map (cons a) r₁<VAR>r₂ : List (List α)<GOAL>foldl (fun r l => r ++ [a :: l]) (foldl (fun r l => r ++ [a :: l]) r₂ r₁ ++ [a :: l]) [] = sublists'Aux a r₁ r₂ ++ [a :: l]
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>a : α<VAR>b : β<GOAL>_root_.Disjoint (s ×ˢ t) (s' ×ˢ t') ↔ _root_.Disjoint s s' ∨ _root_.Disjoint t t'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹⁷ : Norm E<VAR>inst✝¹⁶ : Norm F<VAR>inst✝¹⁵ : Norm G<VAR>inst✝¹⁴ : SeminormedAddCommGroup E'<VAR>inst✝¹³ : SeminormedAddCommGroup F'<VAR>inst✝¹² : SeminormedAddCommGroup G'<VAR>inst✝¹¹ : NormedAddCommGroup E''<VAR>inst✝¹⁰ : NormedAddCommGroup F''<VAR>inst✝⁹ : NormedAddCommGroup G''<VAR>inst✝⁸ : SeminormedRing R<VAR>inst✝⁷ : SeminormedAddGroup E'''<VAR>inst✝⁶ : SeminormedRing R'<VAR>inst✝⁵ : NormedDivisionRing 𝕜<VAR>inst✝⁴ : NormedDivisionRing 𝕜'<VAR>c✝ c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>inst✝³ : Module R E'<VAR>inst✝² : BoundedSMul R E'<VAR>inst✝¹ : Module 𝕜 E'<VAR>inst✝ : BoundedSMul 𝕜 E'<VAR>c : 𝕜<VAR>hc : c ≠ 0<GOAL>(fun x => c • f' x) =O[l] g ↔ f' =O[l] g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹⁷ : Norm E<VAR>inst✝¹⁶ : Norm F<VAR>inst✝¹⁵ : Norm G<VAR>inst✝¹⁴ : SeminormedAddCommGroup E'<VAR>inst✝¹³ : SeminormedAddCommGroup F'<VAR>inst✝¹² : SeminormedAddCommGroup G'<VAR>inst✝¹¹ : NormedAddCommGroup E''<VAR>inst✝¹⁰ : NormedAddCommGroup F''<VAR>inst✝⁹ : NormedAddCommGroup G''<VAR>inst✝⁸ : SeminormedRing R<VAR>inst✝⁷ : SeminormedAddGroup E'''<VAR>inst✝⁶ : SeminormedRing R'<VAR>inst✝⁵ : NormedDivisionRing 𝕜<VAR>inst✝⁴ : NormedDivisionRing 𝕜'<VAR>c✝ c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>inst✝³ : Module R E'<VAR>inst✝² : BoundedSMul R E'<VAR>inst✝¹ : Module 𝕜 E'<VAR>inst✝ : BoundedSMul 𝕜 E'<VAR>c : 𝕜<VAR>hc : c ≠ 0<VAR>cne0 : ‖c‖ ≠ 0<GOAL>(fun x => c • f' x) =O[l] g ↔ f' =O[l] g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹⁷ : Norm E<VAR>inst✝¹⁶ : Norm F<VAR>inst✝¹⁵ : Norm G<VAR>inst✝¹⁴ : SeminormedAddCommGroup E'<VAR>inst✝¹³ : SeminormedAddCommGroup F'<VAR>inst✝¹² : SeminormedAddCommGroup G'<VAR>inst✝¹¹ : NormedAddCommGroup E''<VAR>inst✝¹⁰ : NormedAddCommGroup F''<VAR>inst✝⁹ : NormedAddCommGroup G''<VAR>inst✝⁸ : SeminormedRing R<VAR>inst✝⁷ : SeminormedAddGroup E'''<VAR>inst✝⁶ : SeminormedRing R'<VAR>inst✝⁵ : NormedDivisionRing 𝕜<VAR>inst✝⁴ : NormedDivisionRing 𝕜'<VAR>c✝ c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>inst✝³ : Module R E'<VAR>inst✝² : BoundedSMul R E'<VAR>inst✝¹ : Module 𝕜 E'<VAR>inst✝ : BoundedSMul 𝕜 E'<VAR>c : 𝕜<VAR>hc : c ≠ 0<VAR>cne0 : ‖c‖ ≠ 0<GOAL>(fun x => ‖c • f' x‖) =O[l] g ↔ f' =O[l] g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹⁷ : Norm E<VAR>inst✝¹⁶ : Norm F<VAR>inst✝¹⁵ : Norm G<VAR>inst✝¹⁴ : SeminormedAddCommGroup E'<VAR>inst✝¹³ : SeminormedAddCommGroup F'<VAR>inst✝¹² : SeminormedAddCommGroup G'<VAR>inst✝¹¹ : NormedAddCommGroup E''<VAR>inst✝¹⁰ : NormedAddCommGroup F''<VAR>inst✝⁹ : NormedAddCommGroup G''<VAR>inst✝⁸ : SeminormedRing R<VAR>inst✝⁷ : SeminormedAddGroup E'''<VAR>inst✝⁶ : SeminormedRing R'<VAR>inst✝⁵ : NormedDivisionRing 𝕜<VAR>inst✝⁴ : NormedDivisionRing 𝕜'<VAR>c✝ c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>inst✝³ : Module R E'<VAR>inst✝² : BoundedSMul R E'<VAR>inst✝¹ : Module 𝕜 E'<VAR>inst✝ : BoundedSMul 𝕜 E'<VAR>c : 𝕜<VAR>hc : c ≠ 0<VAR>cne0 : ‖c‖ ≠ 0<GOAL>(fun x => ‖c‖ * ‖f' x‖) =O[l] g ↔ f' =O[l] g
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁸ : OrderedRing R<VAR>inst✝⁷ : AddCommGroup V<VAR>inst✝⁶ : Module R V<VAR>inst✝⁵ : AddTorsor V P<VAR>inst✝⁴ : AddCommGroup V'<VAR>inst✝³ : Module R V'<VAR>inst✝² : AddTorsor V' P'<VAR>inst✝¹ : NoZeroDivisors R<VAR>inst✝ : NoZeroSMulDivisors R V<VAR>ι : Type u_6<VAR>p : ι → P<VAR>ha : AffineIndependent R p<VAR>w w₁ w₂ : ι → R<VAR>s : Finset ι<VAR>hw : ∑ i ∈ s, w i = 1<VAR>hw₁ : ∑ i ∈ s, w₁ i = 1<VAR>hw₂ : ∑ i ∈ s, w₂ i = 1<VAR>h : (Finset.affineCombination R s p) w ∈ affineSpan R {(Finset.affineCombination R s p) w₁, (Finset.affineCombination R s p) w₂}<VAR>i : ι<VAR>his : i ∈ s<VAR>hs : Sbtw R (w₁ i) (w i) (w₂ i)<GOAL>Sbtw R ((Finset.affineCombination R s p) w₁) ((Finset.affineCombination R s p) w) ((Finset.affineCombination R s p) w₂)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁸ : OrderedRing R<VAR>inst✝⁷ : AddCommGroup V<VAR>inst✝⁶ : Module R V<VAR>inst✝⁵ : AddTorsor V P<VAR>inst✝⁴ : AddCommGroup V'<VAR>inst✝³ : Module R V'<VAR>inst✝² : AddTorsor V' P'<VAR>inst✝¹ : NoZeroDivisors R<VAR>inst✝ : NoZeroSMulDivisors R V<VAR>ι : Type u_6<VAR>p : ι → P<VAR>ha : AffineIndependent R p<VAR>w w₁ w₂ : ι → R<VAR>s : Finset ι<VAR>hw : ∑ i ∈ s, w i = 1<VAR>hw₁ : ∑ i ∈ s, w₁ i = 1<VAR>hw₂ : ∑ i ∈ s, w₂ i = 1<VAR>h : ∃ r, ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i<VAR>i : ι<VAR>his : i ∈ s<VAR>hs : Sbtw R (w₁ i) (w i) (w₂ i)<GOAL>Sbtw R ((Finset.affineCombination R s p) w₁) ((Finset.affineCombination R s p) w) ((Finset.affineCombination R s p) w₂)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁸ : OrderedRing R<VAR>inst✝⁷ : AddCommGroup V<VAR>inst✝⁶ : Module R V<VAR>inst✝⁵ : AddTorsor V P<VAR>inst✝⁴ : AddCommGroup V'<VAR>inst✝³ : Module R V'<VAR>inst✝² : AddTorsor V' P'<VAR>inst✝¹ : NoZeroDivisors R<VAR>inst✝ : NoZeroSMulDivisors R V<VAR>ι : Type u_6<VAR>p : ι → P<VAR>ha : AffineIndependent R p<VAR>w w₁ w₂ : ι → R<VAR>s : Finset ι<VAR>hw : ∑ i ∈ s, w i = 1<VAR>hw₁ : ∑ i ∈ s, w₁ i = 1<VAR>hw₂ : ∑ i ∈ s, w₂ i = 1<VAR>i : ι<VAR>his : i ∈ s<VAR>hs : Sbtw R (w₁ i) (w i) (w₂ i)<VAR>r : R<VAR>hr : ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i<GOAL>Sbtw R ((Finset.affineCombination R s p) w₁) ((Finset.affineCombination R s p) w) ((Finset.affineCombination R s p) w₂)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁸ : OrderedRing R<VAR>inst✝⁷ : AddCommGroup V<VAR>inst✝⁶ : Module R V<VAR>inst✝⁵ : AddTorsor V P<VAR>inst✝⁴ : AddCommGroup V'<VAR>inst✝³ : Module R V'<VAR>inst✝² : AddTorsor V' P'<VAR>inst✝¹ : NoZeroDivisors R<VAR>inst✝ : NoZeroSMulDivisors R V<VAR>ι : Type u_6<VAR>p : ι → P<VAR>ha : AffineIndependent R p<VAR>w w₁ w₂ : ι → R<VAR>s : Finset ι<VAR>hw : ∑ i ∈ s, w i = 1<VAR>hw₁ : ∑ i ∈ s, w₁ i = 1<VAR>hw₂ : ∑ i ∈ s, w₂ i = 1<VAR>i : ι<VAR>his : i ∈ s<VAR>r : R<VAR>hs : w₁ i ≠ w₂ i ∧ r ∈ Set.Ioo 0 1<VAR>hr : ∀ i ∈ s, w i = r * (w₂ i - w₁ i) + w₁ i<GOAL>Sbtw R ((Finset.affineCombination R s p) w₁) ((Finset.affineCombination R s p) w) ((Finset.affineCombination R s p) w₂)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁸ : OrderedRing R<VAR>inst✝⁷ : AddCommGroup V<VAR>inst✝⁶ : Module R V<VAR>inst✝⁵ : AddTorsor V P<VAR>inst✝⁴ : AddCommGroup V'<VAR>inst✝³ : Module R V'<VAR>inst✝² : AddTorsor V' P'<VAR>inst✝¹ : NoZeroDivisors R<VAR>inst✝ : NoZeroSMulDivisors R V<VAR>ι : Type u_6<VAR>p : ι → P<VAR>ha : AffineIndependent R p<VAR>w w₁ w₂ : ι → R<VAR>s : Finset ι<VAR>hw : ∑ i ∈ s, w i = 1<VAR>hw₁ : ∑ i ∈ s, w₁ i = 1<VAR>hw₂ : ∑ i ∈ s, w₂ i = 1<VAR>i : ι<VAR>his : i ∈ s<VAR>r : R<VAR>hs : w₁ i ≠ w₂ i ∧ r ∈ Set.Ioo 0 1<VAR>hr : ∀ i ∈ s, w i = (r • (w₂ - w₁) + w₁) i<GOAL>Sbtw R ((Finset.affineCombination R s p) w₁) ((Finset.affineCombination R s p) w) ((Finset.affineCombination R s p) w₂)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁸ : OrderedRing R<VAR>inst✝⁷ : AddCommGroup V<VAR>inst✝⁶ : Module R V<VAR>inst✝⁵ : AddTorsor V P<VAR>inst✝⁴ : AddCommGroup V'<VAR>inst✝³ : Module R V'<VAR>inst✝² : AddTorsor V' P'<VAR>inst✝¹ : NoZeroDivisors R<VAR>inst✝ : NoZeroSMulDivisors R V<VAR>ι : Type u_6<VAR>p : ι → P<VAR>ha : AffineIndependent R p<VAR>w w₁ w₂ : ι → R<VAR>s : Finset ι<VAR>hw : ∑ i ∈ s, w i = 1<VAR>hw₁ : ∑ i ∈ s, w₁ i = 1<VAR>hw₂ : ∑ i ∈ s, w₂ i = 1<VAR>i : ι<VAR>his : i ∈ s<VAR>r : R<VAR>hs : w₁ i ≠ w₂ i ∧ r ∈ Set.Ioo 0 1<VAR>hr : ∀ i ∈ s, w i = (r • (w₂ - w₁) + w₁) i<GOAL>Sbtw R ((Finset.affineCombination R s p) w₁) ((Finset.affineCombination R s p) (r • (w₂ - w₁) + w₁)) ((Finset.affineCombination R s p) w₂)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁸ : OrderedRing R<VAR>inst✝⁷ : AddCommGroup V<VAR>inst✝⁶ : Module R V<VAR>inst✝⁵ : AddTorsor V P<VAR>inst✝⁴ : AddCommGroup V'<VAR>inst✝³ : Module R V'<VAR>inst✝² : AddTorsor V' P'<VAR>inst✝¹ : NoZeroDivisors R<VAR>inst✝ : NoZeroSMulDivisors R V<VAR>ι : Type u_6<VAR>p : ι → P<VAR>ha : AffineIndependent R p<VAR>w w₁ w₂ : ι → R<VAR>s : Finset ι<VAR>hw : ∑ i ∈ s, w i = 1<VAR>hw₁ : ∑ i ∈ s, w₁ i = 1<VAR>hw₂ : ∑ i ∈ s, w₂ i = 1<VAR>i : ι<VAR>his : i ∈ s<VAR>r : R<VAR>hs : w₁ i ≠ w₂ i ∧ r ∈ Set.Ioo 0 1<VAR>hr : ∀ i ∈ s, w i = (r • (w₂ - w₁) + w₁) i<GOAL>(s.weightedVSub p) (w₁ - w₂) ≠ 0
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁸ : OrderedRing R<VAR>inst✝⁷ : AddCommGroup V<VAR>inst✝⁶ : Module R V<VAR>inst✝⁵ : AddTorsor V P<VAR>inst✝⁴ : AddCommGroup V'<VAR>inst✝³ : Module R V'<VAR>inst✝² : AddTorsor V' P'<VAR>inst✝¹ : NoZeroDivisors R<VAR>inst✝ : NoZeroSMulDivisors R V<VAR>ι : Type u_6<VAR>p : ι → P<VAR>ha : AffineIndependent R p<VAR>w w₁ w₂ : ι → R<VAR>s : Finset ι<VAR>hw : ∑ i ∈ s, w i = 1<VAR>hw₁ : ∑ i ∈ s, w₁ i = 1<VAR>hw₂ : ∑ i ∈ s, w₂ i = 1<VAR>i : ι<VAR>his : i ∈ s<VAR>r : R<VAR>hs : w₁ i ≠ w₂ i ∧ r ∈ Set.Ioo 0 1<VAR>hr : ∀ i ∈ s, w i = (r • (w₂ - w₁) + w₁) i<VAR>hz : (s.weightedVSub p) (w₁ - w₂) = 0<GOAL>False
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁸ : OrderedRing R<VAR>inst✝⁷ : AddCommGroup V<VAR>inst✝⁶ : Module R V<VAR>inst✝⁵ : AddTorsor V P<VAR>inst✝⁴ : AddCommGroup V'<VAR>inst✝³ : Module R V'<VAR>inst✝² : AddTorsor V' P'<VAR>inst✝¹ : NoZeroDivisors R<VAR>inst✝ : NoZeroSMulDivisors R V<VAR>ι : Type u_6<VAR>p : ι → P<VAR>ha : AffineIndependent R p<VAR>w w₁ w₂ : ι → R<VAR>s : Finset ι<VAR>hw : ∑ i ∈ s, w i = 1<VAR>hw₁ : ∑ i ∈ s, w₁ i = 1<VAR>hw₂ : ∑ i ∈ s, w₂ i = 1<VAR>i : ι<VAR>his : i ∈ s<VAR>r : R<VAR>hs : w₁ i ≠ w₂ i ∧ r ∈ Set.Ioo 0 1<VAR>hr : ∀ i ∈ s, w i = (r • (w₂ - w₁) + w₁) i<VAR>hz : (s.weightedVSub p) (w₁ - w₂) = 0<VAR>hw₁w₂ : ∑ i ∈ s, (w₁ - w₂) i = 0<GOAL>False
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁸ : OrderedRing R<VAR>inst✝⁷ : AddCommGroup V<VAR>inst✝⁶ : Module R V<VAR>inst✝⁵ : AddTorsor V P<VAR>inst✝⁴ : AddCommGroup V'<VAR>inst✝³ : Module R V'<VAR>inst✝² : AddTorsor V' P'<VAR>inst✝¹ : NoZeroDivisors R<VAR>inst✝ : NoZeroSMulDivisors R V<VAR>ι : Type u_6<VAR>p : ι → P<VAR>ha : AffineIndependent R p<VAR>w w₁ w₂ : ι → R<VAR>s : Finset ι<VAR>hw : ∑ i ∈ s, w i = 1<VAR>hw₁ : ∑ i ∈ s, w₁ i = 1<VAR>hw₂ : ∑ i ∈ s, w₂ i = 1<VAR>i : ι<VAR>his : i ∈ s<VAR>r : R<VAR>hs : w₁ i ≠ w₂ i ∧ r ∈ Set.Ioo 0 1<VAR>hr : ∀ i ∈ s, w i = (r • (w₂ - w₁) + w₁) i<VAR>hz : (s.weightedVSub p) (w₁ - w₂) = 0<VAR>hw₁w₂ : ∑ i ∈ s, (w₁ - w₂) i = 0<GOAL>w₁ i = w₂ i
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁸ : OrderedRing R<VAR>inst✝⁷ : AddCommGroup V<VAR>inst✝⁶ : Module R V<VAR>inst✝⁵ : AddTorsor V P<VAR>inst✝⁴ : AddCommGroup V'<VAR>inst✝³ : Module R V'<VAR>inst✝² : AddTorsor V' P'<VAR>inst✝¹ : NoZeroDivisors R<VAR>inst✝ : NoZeroSMulDivisors R V<VAR>ι : Type u_6<VAR>p : ι → P<VAR>ha : AffineIndependent R p<VAR>w w₁ w₂ : ι → R<VAR>s : Finset ι<VAR>hw : ∑ i ∈ s, w i = 1<VAR>hw₁ : ∑ i ∈ s, w₁ i = 1<VAR>hw₂ : ∑ i ∈ s, w₂ i = 1<VAR>i : ι<VAR>his : i ∈ s<VAR>r : R<VAR>hs : w₁ i ≠ w₂ i ∧ r ∈ Set.Ioo 0 1<VAR>hr : ∀ i ∈ s, w i = (r • (w₂ - w₁) + w₁) i<VAR>hz : (s.weightedVSub p) (w₁ - w₂) = 0<VAR>hw₁w₂ : ∑ i ∈ s, (w₁ - w₂) i = 0<VAR>ha' : (w₁ - w₂) i = 0<GOAL>w₁ i = w₂ i
<VAR>ι : Sort u_1<VAR>α✝ : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α✝<VAR>δ✝ ε : ℝ<VAR>s t : Set α✝<VAR>x✝ : α✝<VAR>α : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x : α<VAR>E : Set α<VAR>hx : x ∈ E<VAR>δ : ℝ<GOAL>closedBall x δ ⊆ cthickening δ E
<VAR>ι : Sort u_1<VAR>α✝ : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α✝<VAR>δ✝ ε : ℝ<VAR>s t : Set α✝<VAR>x✝ : α✝<VAR>α : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x : α<VAR>E : Set α<VAR>hx : x ∈ E<VAR>δ : ℝ<GOAL>{x} ⊆ E
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f✝ : ℂ → E<VAR>z✝ : ℂ<VAR>f : ℂ → E<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>z : ℂ<VAR>hd : DiffContOnCl ℂ f (verticalStrip 0 1)<VAR>hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)<VAR>hz : z ∈ verticalClosedStrip 0 1<GOAL>‖F f ε z‖ ≤ 1
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f✝ : ℂ → E<VAR>z✝ : ℂ<VAR>f : ℂ → E<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>z : ℂ<VAR>hd : DiffContOnCl ℂ f (verticalStrip 0 1)<VAR>hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)<VAR>hz : z ∈ verticalClosedStrip 0 1<GOAL>∃ c < Real.pi / (1 - 0), ∃ B, (fun x => invInterpStrip f x ε • f x) =O[comap (_root_.abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo 0 1)] fun z => Real.exp (B * Real.exp (c * |z.im|))
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f✝ : ℂ → E<VAR>z✝ : ℂ<VAR>f : ℂ → E<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>z : ℂ<VAR>hd : DiffContOnCl ℂ f (verticalStrip 0 1)<VAR>hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)<VAR>hz : z ∈ verticalClosedStrip 0 1<GOAL>0 < Real.pi / (1 - 0) ∧ ∃ B, (fun x => invInterpStrip f x ε • f x) =O[comap (_root_.abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo 0 1)] fun z => Real.exp (B * Real.exp (0 * |z.im|))
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f✝ : ℂ → E<VAR>z✝ : ℂ<VAR>f : ℂ → E<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>z : ℂ<VAR>hd : DiffContOnCl ℂ f (verticalStrip 0 1)<VAR>hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)<VAR>hz : z ∈ verticalClosedStrip 0 1<GOAL>0 < Real.pi ∧ ∃ B, (fun x => invInterpStrip f x ε • f x) =O[comap (_root_.abs ∘ im) atTop ⊓ 𝓟 (re ⁻¹' Ioo 0 1)] fun z => Real.exp (B * Real.exp (0 * |z.im|))