ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>u : δ → δ → Prop<VAR>e : r ≃r s<VAR>x : α<VAR>y : β<GOAL>r x (e.symm y) ↔ s (e x) y
<VAR>R : Type u_1<VAR>inst✝¹⁶ : CommSemiring R<VAR>R' : Type u_2<VAR>inst✝¹⁵ : Monoid R'<VAR>R'' : Type u_3<VAR>inst✝¹⁴ : Semiring R''<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>T : Type u_9<VAR>inst✝¹³ : AddCommMonoid M<VAR>inst✝¹² : AddCommMonoid N<VAR>inst✝¹¹ : AddCommMonoid P<VAR>inst✝¹⁰ : AddCommMonoid Q<VAR>inst✝⁹ : AddCommMonoid S<VAR>inst✝⁸ : AddCommMonoid T<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Module R P<VAR>inst✝⁴ : Module R Q<VAR>inst✝³ : Module R S<VAR>inst✝² : Module R T<VAR>inst✝¹ : DistribMulAction R' M<VAR>inst✝ : Module R'' M<VAR>f : M →ₗ[R] N →ₗ[R] P<VAR>g h : M ⊗[R] N →ₗ[R] P<VAR>H : (mk R M N).compr₂ g = (mk R M N).compr₂ h<GOAL>g = h
<VAR>σ : Type u_1<VAR>inst✝² : Fintype σ<VAR>inst✝¹ : DecidableEq σ<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>k : ℕ<GOAL>↑k * esymm σ R k = (-1) ^ k * ∑ t ∈ filter (fun t => t.1.card = k) (MvPolynomial.NewtonIdentities.pairs σ k), MvPolynomial.NewtonIdentities.weight σ R k t
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁷ : MeasurableSpace X<VAR>inst✝⁶ : TopologicalSpace X<VAR>inst✝⁵ : MeasurableSpace Y<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>f g : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝¹ : LocallyCompactSpace X<VAR>inst✝ : T2Space X<VAR>hs : IsClosed s ∨ IsOpen s<GOAL>LocallyIntegrableOn f s μ ↔ ∀ k ⊆ s, IsCompact k → IntegrableOn f k μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁷ : MeasurableSpace X<VAR>inst✝⁶ : TopologicalSpace X<VAR>inst✝⁵ : MeasurableSpace Y<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>f g : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝¹ : LocallyCompactSpace X<VAR>inst✝ : T2Space X<VAR>hs : IsClosed s ∨ IsOpen s<VAR>hf : ∀ k ⊆ s, IsCompact k → IntegrableOn f k μ<VAR>x : X<VAR>hx : x ∈ s<GOAL>IntegrableAtFilter f (𝓝[s] x) μ
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Ring R<VAR>p q : R[X]<VAR>pn : p.natDegree ≤ n<GOAL>(p - q).natDegree ≤ n ↔ q.natDegree ≤ n
<VAR>X : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : Semiring R<VAR>inst✝¹ : TopologicalSpace R<VAR>inst✝ : TopologicalSemiring R<VAR>f : C(X, R)<GOAL>f ∈ idealOfSet R ∅ ↔ f ∈ ⊥
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s t u v : Set α<VAR>hu : IsOpen u<VAR>hv : IsOpen v<VAR>huv : Disjoint u v<VAR>hsuv : s ⊆ u ∪ v<VAR>hsu : (s ∩ u).Nonempty<VAR>hs : IsPreconnected s<GOAL>Disjoint s v
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s t u v : Set α<VAR>hu : IsOpen u<VAR>hv : IsOpen v<VAR>huv : Disjoint u v<VAR>hsuv : s ⊆ u ∪ v<VAR>hsu : (s ∩ u).Nonempty<VAR>hs : IsPreconnected s<VAR>hsv : ¬Disjoint s v<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s t u v : Set α<VAR>hu : IsOpen u<VAR>hv : IsOpen v<VAR>huv : Disjoint u v<VAR>hsuv : s ⊆ u ∪ v<VAR>hsu : (s ∩ u).Nonempty<VAR>hs : IsPreconnected s<VAR>hsv : (s ∩ v).Nonempty<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s t u v : Set α<VAR>hu : IsOpen u<VAR>hv : IsOpen v<VAR>huv : Disjoint u v<VAR>hsuv : s ⊆ u ∪ v<VAR>hsu : (s ∩ u).Nonempty<VAR>hs : IsPreconnected s<VAR>hsv : (s ∩ v).Nonempty<VAR>x : α<VAR>left✝ : x ∈ s<VAR>hx : x ∈ u ∩ v<GOAL>False
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝ : GroupWithZero G₀<VAR>a✝ b c a : G₀<VAR>h : 1 / a ≠ 0<VAR>ha : a = 0<GOAL>False
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝ : GroupWithZero G₀<VAR>a✝ b c a : G₀<VAR>h : 0 ≠ 0<VAR>ha : a = 0<GOAL>False
<VAR>α : Type u_1<VAR>n : Num<GOAL>0 + n.succ = (0 + n).succ
<VAR>α : Type u_1<VAR>p : PosNum<GOAL>pos (p + 1) = (pos p + 0).succ
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝ : TopologicalSpace X<VAR>s : Set X<VAR>t : Set ↑s<VAR>ht : IsOpen t<VAR>hs : IsOpen s<GOAL>IsOpen (Subtype.val '' t)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝ : TopologicalSpace X<VAR>s : Set X<VAR>hs : IsOpen s<VAR>s' : Set X<VAR>hs' : IsOpen s'<VAR>ht : IsOpen (Subtype.val ⁻¹' s')<GOAL>IsOpen (Subtype.val '' (Subtype.val ⁻¹' s'))
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝ : TopologicalSpace X<VAR>s : Set X<VAR>hs : IsOpen s<VAR>s' : Set X<VAR>hs' : IsOpen s'<VAR>ht : IsOpen (Subtype.val ⁻¹' s')<GOAL>IsOpen (s ∩ s')
<VAR>α : Type u_1<VAR>inst✝² : DistribLattice α<VAR>inst✝¹ : OrderBot α<VAR>inst✝ : DecidableEq α<VAR>a b c : α<VAR>P : Finpartition a<VAR>Q✝ Q : (i : α) → i ∈ P.parts → Finpartition i<GOAL>(P.bind Q).parts.card = ∑ A ∈ P.parts.attach, (Q ↑A ⋯).parts.card
<VAR>α : Type u_1<VAR>inst✝² : DistribLattice α<VAR>inst✝¹ : OrderBot α<VAR>inst✝ : DecidableEq α<VAR>a b c : α<VAR>P : Finpartition a<VAR>Q✝ Q : (i : α) → i ∈ P.parts → Finpartition i<GOAL>∀ x ∈ P.parts.attach, ∀ y ∈ P.parts.attach, x ≠ y → Disjoint (Q ↑x ⋯).parts (Q ↑y ⋯).parts
<VAR>α : Type u_1<VAR>inst✝² : DistribLattice α<VAR>inst✝¹ : OrderBot α<VAR>inst✝ : DecidableEq α<VAR>a b✝ c✝ : α<VAR>P : Finpartition a<VAR>Q✝ Q : (i : α) → i ∈ P.parts → Finpartition i<VAR>b : α<VAR>hb : b ∈ P.parts<VAR>c : α<VAR>hc : c ∈ P.parts<VAR>hbc : ⟨b, hb⟩ ≠ ⟨c, hc⟩<GOAL>Disjoint (Q ↑⟨b, hb⟩ ⋯).parts (Q ↑⟨c, hc⟩ ⋯).parts
<VAR>α : Type u_1<VAR>inst✝² : DistribLattice α<VAR>inst✝¹ : OrderBot α<VAR>inst✝ : DecidableEq α<VAR>a b✝ c✝ : α<VAR>P : Finpartition a<VAR>Q✝ Q : (i : α) → i ∈ P.parts → Finpartition i<VAR>b : α<VAR>hb : b ∈ P.parts<VAR>c : α<VAR>hc : c ∈ P.parts<VAR>hbc : ⟨b, hb⟩ ≠ ⟨c, hc⟩<GOAL>∀ ⦃a_1 : α⦄, a_1 ∈ (Q ↑⟨b, hb⟩ ⋯).parts → a_1 ∉ (Q ↑⟨c, hc⟩ ⋯).parts
<VAR>α : Type u_1<VAR>inst✝² : DistribLattice α<VAR>inst✝¹ : OrderBot α<VAR>inst✝ : DecidableEq α<VAR>a b✝ c✝ : α<VAR>P : Finpartition a<VAR>Q✝ Q : (i : α) → i ∈ P.parts → Finpartition i<VAR>b : α<VAR>hb : b ∈ P.parts<VAR>c : α<VAR>hc : c ∈ P.parts<VAR>hbc : ⟨b, hb⟩ ≠ ⟨c, hc⟩<VAR>d : α<VAR>hdb : d ∈ (Q ↑⟨b, hb⟩ ⋯).parts<VAR>hdc : d ∈ (Q ↑⟨c, hc⟩ ⋯).parts<GOAL>False
<VAR>α : Type u_1<VAR>inst✝² : DistribLattice α<VAR>inst✝¹ : OrderBot α<VAR>inst✝ : DecidableEq α<VAR>a b✝ c✝ : α<VAR>P : Finpartition a<VAR>Q✝ Q : (i : α) → i ∈ P.parts → Finpartition i<VAR>b : α<VAR>hb : b ∈ P.parts<VAR>c : α<VAR>hc : c ∈ P.parts<VAR>hbc : ¬b = c<VAR>d : α<VAR>hdb : d ∈ (Q ↑⟨b, hb⟩ ⋯).parts<VAR>hdc : d ∈ (Q ↑⟨c, hc⟩ ⋯).parts<GOAL>False
<VAR>a b : ℤ<VAR>h : a ≤ b<GOAL>↑(Ico a b).card = b - a
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>se : SplitEpi f<VAR>Z✝ : C<VAR>g h : Y ⟶ Z✝<VAR>w : f ≫ g = f ≫ h<GOAL>g = h
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>se : SplitEpi f<VAR>Z✝ : C<VAR>g h : Y ⟶ Z✝<VAR>w : se.section_ ≫ f ≫ g = se.section_ ≫ f ≫ h<GOAL>g = h
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝² : PseudoEMetricSpace X<VAR>inst✝¹ : PseudoEMetricSpace Y<VAR>inst✝ : PseudoEMetricSpace Z<VAR>C r : ℝ≥0<VAR>f : X → Y<GOAL>HolderOnWith C r f univ ↔ HolderWith C r f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α ↪ β<VAR>s : Finset α<VAR>a b : ℕ<GOAL>_root_.Disjoint (range a) (map (addRightEmbedding a) (range b))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α ↪ β<VAR>s : Finset α<VAR>a b : ℕ<GOAL>∀ ⦃a_1 : ℕ⦄, a_1 < a → ∀ x < b, ¬x + a = a_1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>p : Set γ<VAR>f f₁ f₂ f₃ : α → β<VAR>g g₁ g₂ : β → γ<VAR>f' f₁' f₂' : β → α<VAR>g' : γ → β<VAR>a : α<VAR>b : β<VAR>h : InjOn f s<VAR>h₁ : s₁ ⊆ s<VAR>h₂ : s₂ ⊆ s<GOAL>f '' s₁ ⊂ f '' s₂ ↔ s₁ ⊂ s₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>hμν : μ ≪ ν<GOAL>(μ.rnDeriv ν)⁻¹ =ᶠ[ae μ] ν.rnDeriv μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>hμν : μ ≪ ν<GOAL>(μ.rnDeriv ν)⁻¹ =ᶠ[ae μ] (μ.rnDeriv (μ.withDensity (ν.rnDeriv μ)))⁻¹ ∧ ν.rnDeriv μ =ᶠ[ae μ] (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ
<VAR>ι : Sort u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝¹ : LinearOrder α<VAR>a₁ a₂ b₁ b₂ : α<VAR>inst✝ : DenselyOrdered α<GOAL>Disjoint (Ioo a₁ a₂) (Ioo b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝² : Preorder α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : Topology.IsUpperSet α<VAR>s : Set α<GOAL>IsOpen s ↔ IsUpperSet s
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>X : Type u_3<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>u v : V<VAR>G'' : SimpleGraph X<VAR>s : Set V<VAR>t : Set W<VAR>r : Set X<VAR>φ : G →g G'<VAR>φst : Set.MapsTo (⇑φ) s t<VAR>ψ : G' →g G''<VAR>ψtr : Set.MapsTo (⇑ψ) t r<VAR>hi : Set.InjOn (⇑φ) s<GOAL>Injective ⇑(induceHom φ φst)
<VAR>x✝ y x : ℂ<VAR>hx : cos x ≠ 0<GOAL>tan x ^ 2 / (1 + tan x ^ 2) = sin x ^ 2
<VAR>a : ℤ<VAR>b : ℕ<VAR>ha4 : a % 4 = 0<VAR>hb2 : b % 2 = 1<GOAL>J(a / 4 | b) = J(a | b)
<VAR>b : ℕ<VAR>hb2 : b % 2 = 1<VAR>a : ℤ<VAR>ha4 : 4 * a % 4 = 0<GOAL>J(4 * a / 4 | b) = J(4 * a | b)
<VAR>b : ℕ<VAR>hb2 : b % 2 = 1<VAR>a : ℤ<VAR>ha4 : 4 * a % 4 = 0<VAR>this : (↑2).gcd ↑b = 1<GOAL>J(4 * a / 4 | b) = J(4 * a | b)
<VAR>r : ℝ<VAR>hr : 0 < r<VAR>x : ℝ<VAR>h : 0 ≤ x<GOAL>∫⁻ (y : ℝ) in Iic x, exponentialPDF r y = ENNReal.ofReal (1 - rexp (-(r * x)))
<VAR>r : ℝ<VAR>hr : 0 < r<VAR>x : ℝ<VAR>h : ¬0 ≤ x<GOAL>∫⁻ (y : ℝ) in Iic x, exponentialPDF r y = ENNReal.ofReal 0
<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 α<GOAL>(f =O[l] fun x => -g' x) ↔ 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 α<GOAL>(∃ c, IsBigOWith c l f fun x => -g' x) ↔ ∃ c, IsBigOWith c l f g'
<VAR>m n : ℕ<GOAL>(m + n).Coprime m ↔ n.Coprime m
<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>ι : Type u_7<VAR>inst✝⁵ : Fintype l<VAR>inst✝⁴ : Fintype m<VAR>inst✝³ : Fintype n<VAR>inst✝² : Unique ι<VAR>inst✝¹ : SeminormedAddCommGroup α<VAR>inst✝ : DecidableEq m<VAR>v : m → α<GOAL>‖diagonal v‖₊ = ‖v‖₊
<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>ι : Type u_7<VAR>inst✝⁵ : Fintype l<VAR>inst✝⁴ : Fintype m<VAR>inst✝³ : Fintype n<VAR>inst✝² : Unique ι<VAR>inst✝¹ : SeminormedAddCommGroup α<VAR>inst✝ : DecidableEq m<VAR>v : m → α<GOAL>(Finset.univ.sup fun i => ∑ j : m, ‖diagonal v i j‖₊) = Finset.univ.sup fun b => ‖v b‖₊
<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>ι : Type u_7<VAR>inst✝⁵ : Fintype l<VAR>inst✝⁴ : Fintype m<VAR>inst✝³ : Fintype n<VAR>inst✝² : Unique ι<VAR>inst✝¹ : SeminormedAddCommGroup α<VAR>inst✝ : DecidableEq m<VAR>v : m → α<VAR>i : m<GOAL>∑ j : m, ‖diagonal v i j‖₊ = ‖v i‖₊
<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>ι : Type u_7<VAR>inst✝⁵ : Fintype l<VAR>inst✝⁴ : Fintype m<VAR>inst✝³ : Fintype n<VAR>inst✝² : Unique ι<VAR>inst✝¹ : SeminormedAddCommGroup α<VAR>inst✝ : DecidableEq m<VAR>v : m → α<VAR>i j : m<VAR>_hj : j ∈ Finset.univ<VAR>hij : j ≠ i<GOAL>‖diagonal v i j‖₊ = 0
<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>ι : Type u_7<VAR>inst✝⁵ : Fintype l<VAR>inst✝⁴ : Fintype m<VAR>inst✝³ : Fintype n<VAR>inst✝² : Unique ι<VAR>inst✝¹ : SeminormedAddCommGroup α<VAR>inst✝ : DecidableEq m<VAR>v : m → α<VAR>i : m<GOAL>‖diagonal v i i‖₊ = ‖v i‖₊
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>W : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace ℝ G<VAR>inst✝⁵ : NormedAddCommGroup W<VAR>inst✝⁴ : NormedSpace ℝ W<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>μ : Measure E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>f f' : E → F<VAR>g g' : E → G<VAR>v : E<VAR>B : F →L[ℝ] G →L[ℝ] W<VAR>hf'g : Integrable (fun x => (B (f' x)) (g x)) μ<VAR>hfg' : Integrable (fun x => (B (f x)) (g' x)) μ<VAR>hfg : Integrable (fun x => (B (f x)) (g x)) μ<VAR>hf : ∀ (x : E), HasLineDerivAt ℝ f (f' x) x v<VAR>hg : ∀ (x : E), HasLineDerivAt ℝ g (g' x) x v<VAR>hW : CompleteSpace W<GOAL>∫ (x : E), (B (f x)) (g' x) ∂μ = -∫ (x : E), (B (f' x)) (g x) ∂μ
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>W : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace ℝ G<VAR>inst✝⁵ : NormedAddCommGroup W<VAR>inst✝⁴ : NormedSpace ℝ W<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>μ : Measure E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>f f' : E → F<VAR>g g' : E → G<VAR>B : F →L[ℝ] G →L[ℝ] W<VAR>hf'g : Integrable (fun x => (B (f' x)) (g x)) μ<VAR>hfg' : Integrable (fun x => (B (f x)) (g' x)) μ<VAR>hfg : Integrable (fun x => (B (f x)) (g x)) μ<VAR>hW : CompleteSpace W<VAR>hf : ∀ (x : E), HasLineDerivAt ℝ f (f' x) x 0<VAR>hg : ∀ (x : E), HasLineDerivAt ℝ g (g' x) x 0<GOAL>∫ (x : E), (B (f x)) (g' x) ∂μ = -∫ (x : E), (B (f' x)) (g x) ∂μ
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>W : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace ℝ G<VAR>inst✝⁵ : NormedAddCommGroup W<VAR>inst✝⁴ : NormedSpace ℝ W<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>μ : Measure E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>f f' : E → F<VAR>g g' : E → G<VAR>v : E<VAR>B : F →L[ℝ] G →L[ℝ] W<VAR>hf'g : Integrable (fun x => (B (f' x)) (g x)) μ<VAR>hfg' : Integrable (fun x => (B (f x)) (g' x)) μ<VAR>hfg : Integrable (fun x => (B (f x)) (g x)) μ<VAR>hf : ∀ (x : E), HasLineDerivAt ℝ f (f' x) x v<VAR>hg : ∀ (x : E), HasLineDerivAt ℝ g (g' x) x v<VAR>hW : CompleteSpace W<VAR>hv : v ≠ 0<GOAL>∫ (x : E), (B (f x)) (g' x) ∂μ = -∫ (x : E), (B (f' x)) (g x) ∂μ
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>W : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace ℝ G<VAR>inst✝⁵ : NormedAddCommGroup W<VAR>inst✝⁴ : NormedSpace ℝ W<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>μ : Measure E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>f f' : E → F<VAR>g g' : E → G<VAR>v : E<VAR>B : F →L[ℝ] G →L[ℝ] W<VAR>hf'g : Integrable (fun x => (B (f' x)) (g x)) μ<VAR>hfg' : Integrable (fun x => (B (f x)) (g' x)) μ<VAR>hfg : Integrable (fun x => (B (f x)) (g x)) μ<VAR>hf : ∀ (x : E), HasLineDerivAt ℝ f (f' x) x v<VAR>hg : ∀ (x : E), HasLineDerivAt ℝ g (g' x) x v<VAR>hW : CompleteSpace W<VAR>hv : v ≠ 0<VAR>this : Nontrivial E<GOAL>∫ (x : E), (B (f x)) (g' x) ∂μ = -∫ (x : E), (B (f' x)) (g x) ∂μ
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>W : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace ℝ G<VAR>inst✝⁵ : NormedAddCommGroup W<VAR>inst✝⁴ : NormedSpace ℝ W<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>μ : Measure E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>f f' : E → F<VAR>g g' : E → G<VAR>v : E<VAR>B : F →L[ℝ] G →L[ℝ] W<VAR>hf'g : Integrable (fun x => (B (f' x)) (g x)) μ<VAR>hfg' : Integrable (fun x => (B (f x)) (g' x)) μ<VAR>hfg : Integrable (fun x => (B (f x)) (g x)) μ<VAR>hf : ∀ (x : E), HasLineDerivAt ℝ f (f' x) x v<VAR>hg : ∀ (x : E), HasLineDerivAt ℝ g (g' x) x v<VAR>hW : CompleteSpace W<VAR>hv : v ≠ 0<VAR>this : Nontrivial E<VAR>n : ℕ := finrank ℝ E<VAR>E' : Type := Fin (n - 1) → ℝ<VAR>L : E ≃L[ℝ] E' × ℝ<VAR>hL : L v = (0, 1)<VAR>ν : Measure (E' × ℝ) := map (⇑L) μ<GOAL>∫ (x : E), (B (f x)) (g' x) ∂μ = -∫ (x : E), (B (f' x)) (g x) ∂μ
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>W : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace ℝ G<VAR>inst✝⁵ : NormedAddCommGroup W<VAR>inst✝⁴ : NormedSpace ℝ W<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>μ : Measure E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>f f' : E → F<VAR>g g' : E → G<VAR>v : E<VAR>B : F →L[ℝ] G →L[ℝ] W<VAR>hf'g : Integrable (fun x => (B (f' x)) (g x)) μ<VAR>hfg' : Integrable (fun x => (B (f x)) (g' x)) μ<VAR>hfg : Integrable (fun x => (B (f x)) (g x)) μ<VAR>hf : ∀ (x : E), HasLineDerivAt ℝ f (f' x) x v<VAR>hg : ∀ (x : E), HasLineDerivAt ℝ g (g' x) x v<VAR>hW : CompleteSpace W<VAR>hv : v ≠ 0<VAR>this : Nontrivial E<VAR>n : ℕ := finrank ℝ E<VAR>E' : Type := Fin (n - 1) → ℝ<VAR>L : E ≃L[ℝ] E' × ℝ<VAR>hL : L v = (0, 1)<VAR>ν : Measure (E' × ℝ) := map (⇑L) μ<GOAL>∫ (x : E' × ℝ), (B (f (L.symm x))) (g' (L.symm x)) ∂ν = -∫ (x : E' × ℝ), (B (f' (L.symm x))) (g (L.symm x)) ∂ν
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>W : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace ℝ G<VAR>inst✝⁵ : NormedAddCommGroup W<VAR>inst✝⁴ : NormedSpace ℝ W<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>μ : Measure E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>f f' : E → F<VAR>g g' : E → G<VAR>v : E<VAR>B : F →L[ℝ] G →L[ℝ] W<VAR>hf'g : Integrable (fun x => (B (f' x)) (g x)) μ<VAR>hfg' : Integrable (fun x => (B (f x)) (g' x)) μ<VAR>hfg : Integrable (fun x => (B (f x)) (g x)) μ<VAR>hf : ∀ (x : E), HasLineDerivAt ℝ f (f' x) x v<VAR>hg : ∀ (x : E), HasLineDerivAt ℝ g (g' x) x v<VAR>hW : CompleteSpace W<VAR>hv : v ≠ 0<VAR>this : Nontrivial E<VAR>n : ℕ := finrank ℝ E<VAR>E' : Type := Fin (n - 1) → ℝ<VAR>L : E ≃L[ℝ] E' × ℝ<VAR>hL : L v = (0, 1)<VAR>ν : Measure (E' × ℝ) := map (⇑L) μ<VAR>L_emb : MeasurableEmbedding ⇑L<GOAL>∫ (x : E' × ℝ), (B (f (L.symm x))) (g' (L.symm x)) ∂ν = -∫ (x : E' × ℝ), (B (f' (L.symm x))) (g (L.symm x)) ∂ν
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>W : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace ℝ G<VAR>inst✝⁵ : NormedAddCommGroup W<VAR>inst✝⁴ : NormedSpace ℝ W<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>μ : Measure E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>f f' : E → F<VAR>g g' : E → G<VAR>v : E<VAR>B : F →L[ℝ] G →L[ℝ] W<VAR>hf'g : Integrable (fun x => (B (f' x)) (g x)) μ<VAR>hfg' : Integrable (fun x => (B (f x)) (g' x)) μ<VAR>hfg : Integrable (fun x => (B (f x)) (g x)) μ<VAR>hf : ∀ (x : E), HasLineDerivAt ℝ f (f' x) x v<VAR>hg : ∀ (x : E), HasLineDerivAt ℝ g (g' x) x v<VAR>hW : CompleteSpace W<VAR>hv : v ≠ 0<VAR>this : Nontrivial E<VAR>n : ℕ := finrank ℝ E<VAR>E' : Type := Fin (n - 1) → ℝ<VAR>L : E ≃L[ℝ] E' × ℝ<VAR>hL : L v = (0, 1)<VAR>ν : Measure (E' × ℝ) := map (⇑L) μ<VAR>L_emb : MeasurableEmbedding ⇑L<GOAL>Integrable (fun x => (B (f' (L.symm x))) (g (L.symm x))) ν
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>W : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace ℝ G<VAR>inst✝⁵ : NormedAddCommGroup W<VAR>inst✝⁴ : NormedSpace ℝ W<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>μ : Measure E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>f f' : E → F<VAR>g g' : E → G<VAR>v : E<VAR>B : F →L[ℝ] G →L[ℝ] W<VAR>hf'g : Integrable (fun x => (B (f' x)) (g x)) μ<VAR>hfg' : Integrable (fun x => (B (f x)) (g' x)) μ<VAR>hfg : Integrable (fun x => (B (f x)) (g x)) μ<VAR>hf : ∀ (x : E), HasLineDerivAt ℝ f (f' x) x v<VAR>hg : ∀ (x : E), HasLineDerivAt ℝ g (g' x) x v<VAR>hW : CompleteSpace W<VAR>hv : v ≠ 0<VAR>this : Nontrivial E<VAR>n : ℕ := finrank ℝ E<VAR>E' : Type := Fin (n - 1) → ℝ<VAR>L : E ≃L[ℝ] E' × ℝ<VAR>hL : L v = (0, 1)<VAR>ν : Measure (E' × ℝ) := map (⇑L) μ<VAR>L_emb : MeasurableEmbedding ⇑L<GOAL>Integrable (fun x => (B (f (L.symm x))) (g' (L.symm x))) ν
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>W : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace ℝ G<VAR>inst✝⁵ : NormedAddCommGroup W<VAR>inst✝⁴ : NormedSpace ℝ W<VAR>inst✝³ : MeasurableSpace E<VAR>inst✝² : BorelSpace E<VAR>μ : Measure E<VAR>inst✝¹ : FiniteDimensional ℝ E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>f f' : E → F<VAR>g g' : E → G<VAR>v : E<VAR>B : F →L[ℝ] G →L[ℝ] W<VAR>hf'g : Integrable (fun x => (B (f' x)) (g x)) μ<VAR>hfg' : Integrable (fun x => (B (f x)) (g' x)) μ<VAR>hfg : Integrable (fun x => (B (f x)) (g x)) μ<VAR>hf : ∀ (x : E), HasLineDerivAt ℝ f (f' x) x v<VAR>hg : ∀ (x : E), HasLineDerivAt ℝ g (g' x) x v<VAR>hW : CompleteSpace W<VAR>hv : v ≠ 0<VAR>this : Nontrivial E<VAR>n : ℕ := finrank ℝ E<VAR>E' : Type := Fin (n - 1) → ℝ<VAR>L : E ≃L[ℝ] E' × ℝ<VAR>hL : L v = (0, 1)<VAR>ν : Measure (E' × ℝ) := map (⇑L) μ<VAR>L_emb : MeasurableEmbedding ⇑L<GOAL>Integrable (fun x => (B (f (L.symm x))) (g (L.symm x))) ν