mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.InnerProductSpace.TensorProduct

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
x x' : E
y y' : F
⊢ nndist (x ⊗ₜ[𝕜] y) (x' ⊗ₜ[𝕜] y') ≤ ‖x‖₊ * ‖y‖₊ + ‖x'‖₊ * ‖y'‖₊

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TensorProduct

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
x x' : E
y y' : F
⊢ edist (x ⊗ₜ[𝕜] y) (x' ⊗ₜ[𝕜] y') ≤ ‖x‖ₑ * ‖y‖ₑ + ‖x'‖ₑ * ‖y'‖ₑ

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: E : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
μ : Measure E
inst✝² : μ.IsAddHaarMeasure
F' : Type u_5
inst✝¹ : NormedAddCommGroup F'
inst✝ : InnerProductSpace ℝ F'
u : E → F'
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp✝ : 1 ≤ p
hp'0 : ¬p' = 0
n : ℕ := finrank ℝ E
hn✝ : 0 < n
hp' : (↑p')⁻¹ = ↑p⁻¹ - (↑n)⁻¹
n' : ℝ≥0 := (↑n).conjExponent
h2p : ↑p < ↑n
h0n : 2 ≤ n
hn : (↑n).HolderConjugate n'
h1n : 1 ≤ ↑n
h2n : 0 < ↑n - 1
hnp : 0 < ↑n - ↑p
hp : 1 < p
q : ℝ := (↑p).conjExponent
hq : (↑p).HolderConjugate q
h0p : p ≠ 0
h1p : ↑p ≠ 1
h3p : ↑p - 1 ≠ 0
h2q : 1 / ↑n' - 1 / q = 1 / ↑p'
γ : ℝ≥0 := NNReal.mk (↑p * (↑n - 1) / (↑n - ↑p)) ⋯
h0γ : ↑γ = ↑p * (↑n - 1) / (↑n - ↑p)
h1γ : 1 < ↑γ
h2γ : γ * n' = p'
h3γ : (↑γ - 1) * q = ↑p'
h4γ : ↑γ ≠ 0
h3u : ¬∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ = 0
h4u : ∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ ≠ ∞
h5u : (∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ) ^ (1 / q) ≠ 0
h6u : (∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ) ^ (1 / q) ≠ ∞
h7u : Continuous u
v : E → ℝ := fun x ↦ ‖u x‖ ^ ↑γ
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
C : ℝ≥0 := eLpNormLESNormFDerivOneConst μ ↑n'
⊢ ↑C * ↑γ * ∫⁻ (x : E), ‖u x‖ₑ ^ (↑γ - 1) * ‖fderiv ℝ u x‖ₑ ∂μ ≤
    ↑C * ↑γ * ((∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ) ^ (1 / q) * (∫⁻ (x : E), ‖fderiv ℝ u x‖ₑ ^ ↑p ∂μ) ^ (1 / ↑p))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TensorProduct

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
a b c d : 𝕜
⊢ inner 𝕜 (a ⊗ₜ[𝕜] b) (c ⊗ₜ[𝕜] d) = inner 𝕜 (a * b) (c * d)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TensorProduct

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
x y : E ⊗[𝕜] F
⊢ x = y ↔ ∀ (a : E) (b : F), inner 𝕜 (a ⊗ₜ[𝕜] b) x = inner 𝕜 (a ⊗ₜ[𝕜] b) y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TensorProduct

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : InnerProductSpace 𝕜 G
x y : E ⊗[𝕜] F ⊗[𝕜] G
⊢ x = y ↔ ∀ (a : E) (b : F) (c : G), inner 𝕜 (a ⊗ₜ[𝕜] b ⊗ₜ[𝕜] c) x = inner 𝕜 (a ⊗ₜ[𝕜] b ⊗ₜ[𝕜] c) y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TensorProduct

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace 𝕜 H
x✝¹ : E
x✝ : F
⊢ ‖((mk 𝕜 E F) x✝¹) x✝‖ ≤ 1 * ‖x✝¹‖ * ‖x✝‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TensorProduct

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
⊢ mapIsometry LinearIsometry.id LinearIsometry.id = LinearIsometry.id

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: E : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
μ : Measure E
inst✝² : μ.IsAddHaarMeasure
F' : Type u_5
inst✝¹ : NormedAddCommGroup F'
inst✝ : InnerProductSpace ℝ F'
u : E → F'
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp✝ : 1 ≤ p
hp'0 : ¬p' = 0
n : ℕ := finrank ℝ E
hn✝ : 0 < n
hp' : (↑p')⁻¹ = ↑p⁻¹ - (↑n)⁻¹
n' : ℝ≥0 := (↑n).conjExponent
h2p : ↑p < ↑n
h0n : 2 ≤ n
hn : (↑n).HolderConjugate n'
h1n : 1 ≤ ↑n
h2n : 0 < ↑n - 1
hnp : 0 < ↑n - ↑p
hp : 1 < p
q : ℝ := (↑p).conjExponent
hq : (↑p).HolderConjugate q
h0p : p ≠ 0
h1p : ↑p ≠ 1
h3p : ↑p - 1 ≠ 0
h2q : 1 / ↑n' - 1 / q = 1 / ↑p'
γ : ℝ≥0 := NNReal.mk (↑p * (↑n - 1) / (↑n - ↑p)) ⋯
h0γ : ↑γ = ↑p * (↑n - 1) / (↑n - ↑p)
h1γ : 1 < ↑γ
h2γ : γ * n' = p'
h3γ : (↑γ - 1) * q = ↑p'
h4γ : ↑γ ≠ 0
h3u : ¬∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ = 0
h4u : ∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ ≠ ∞
h5u : (∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ) ^ (1 / q) ≠ 0
h6u : (∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ) ^ (1 / q) ≠ ∞
h7u : Continuous u
v : E → ℝ := fun x ↦ ‖u x‖ ^ ↑γ
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
C : ℝ≥0 := eLpNormLESNormFDerivOneConst μ ↑n'
⊢ ↑C * ↑γ * ((∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ) ^ (1 / q) * (∫⁻ (x : E), ‖fderiv ℝ u x‖ₑ ^ ↑p ∂μ) ^ (1 / ↑p)) =
    ↑C * ↑γ * (∫⁻ (x : E), ‖fderiv ℝ u x‖ₑ ^ ↑p ∂μ) ^ (1 / ↑p) * (∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ) ^ (1 / q)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TensorProduct

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
⊢ ↑(congrIsometry (LinearIsometryEquiv.refl 𝕜 E) (LinearIsometryEquiv.refl 𝕜 F)).toLinearEquiv =
    ↑(LinearIsometryEquiv.refl 𝕜 (E ⊗[𝕜] F)).toLinearEquiv

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TensorProduct

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
x y : E ⊗[𝕜] F
⊢ inner 𝕜 ((TensorProduct.comm 𝕜 E F) 0) ((TensorProduct.comm 𝕜 E F) y) = inner 𝕜 0 y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TensorProduct

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
x y : E ⊗[𝕜] F
x✝¹ : E
x✝ : F
⊢ inner 𝕜 ((TensorProduct.comm 𝕜 E F) (x✝¹ ⊗ₜ[𝕜] x✝)) ((TensorProduct.comm 𝕜 E F) 0) = inner 𝕜 (x✝¹ ⊗ₜ[𝕜] x✝) 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TensorProduct

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
x y : E ⊗[𝕜] F
x✝¹ : E
x✝ : F
⊢ ∀ (x : E) (y : F),
    inner 𝕜 ((TensorProduct.comm 𝕜 E F) (x✝¹ ⊗ₜ[𝕜] x✝)) ((TensorProduct.comm 𝕜 E F) (x ⊗ₜ[𝕜] y)) =
      inner 𝕜 (x✝¹ ⊗ₜ[𝕜] x✝) (x ⊗ₜ[𝕜] y)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TensorProduct

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
x y : E ⊗[𝕜] F
x✝³ : E
x✝² : F
x✝¹ x✝ : E ⊗[𝕜] F
h1 : inner 𝕜 ((TensorProduct.comm 𝕜 E F) (x✝³ ⊗ₜ[𝕜] x✝²)) ((TensorProduct.comm 𝕜 E F) x✝¹) = inner 𝕜 (x✝³ ⊗ₜ[𝕜] x✝²) x✝¹
h2 : inner 𝕜 ((TensorProduct.comm 𝕜 E F) (x✝³ ⊗ₜ[𝕜] x✝²)) ((TensorProduct.comm 𝕜 E F) x✝) = inner 𝕜 (x✝³ ⊗ₜ[𝕜] x✝²) x✝
⊢ inner 𝕜 ((TensorProduct.comm 𝕜 E F) (x✝³ ⊗ₜ[𝕜] x✝²)) ((TensorProduct.comm 𝕜 E F) (x✝¹ + x✝)) =
    inner 𝕜 (x✝³ ⊗ₜ[𝕜] x✝²) (x✝¹ + x✝)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TensorProduct

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
x y x✝¹ x✝ : E ⊗[𝕜] F
h1 : inner 𝕜 ((TensorProduct.comm 𝕜 E F) x✝¹) ((TensorProduct.comm 𝕜 E F) y) = inner 𝕜 x✝¹ y
h2 : inner 𝕜 ((TensorProduct.comm 𝕜 E F) x✝) ((TensorProduct.comm 𝕜 E F) y) = inner 𝕜 x✝ y
⊢ inner 𝕜 ((TensorProduct.comm 𝕜 E F) (x✝¹ + x✝)) ((TensorProduct.comm 𝕜 E F) y) = inner 𝕜 (x✝¹ + x✝) y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TensorProduct

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : 𝕜 ⊗[𝕜] E
⊢ inner 𝕜 ((TensorProduct.lid 𝕜 E) 0) ((TensorProduct.lid 𝕜 E) y) = inner 𝕜 0 y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TensorProduct

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : 𝕜 ⊗[𝕜] E
x✝¹ : 𝕜
x✝ : E
⊢ inner 𝕜 ((TensorProduct.lid 𝕜 E) (x✝¹ ⊗ₜ[𝕜] x✝)) ((TensorProduct.lid 𝕜 E) 0) = inner 𝕜 (x✝¹ ⊗ₜ[𝕜] x✝) 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: E : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
μ : Measure E
inst✝² : μ.IsAddHaarMeasure
F' : Type u_5
inst✝¹ : NormedAddCommGroup F'
inst✝ : InnerProductSpace ℝ F'
u : E → F'
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp✝ : 1 ≤ p
hp'0 : ¬p' = 0
n : ℕ := finrank ℝ E
hn✝ : 0 < n
hp' : (↑p')⁻¹ = ↑p⁻¹ - (↑n)⁻¹
n' : ℝ≥0 := (↑n).conjExponent
h2p : ↑p < ↑n
h0n : 2 ≤ n
hn : (↑n).HolderConjugate n'
h1n : 1 ≤ ↑n
h2n : 0 < ↑n - 1
hnp : 0 < ↑n - ↑p
hp : 1 < p
q : ℝ := (↑p).conjExponent
hq : (↑p).HolderConjugate q
h0p : p ≠ 0
h1p : ↑p ≠ 1
h3p : ↑p - 1 ≠ 0
h2q : 1 / ↑n' - 1 / q = 1 / ↑p'
γ : ℝ≥0 := NNReal.mk (↑p * (↑n - 1) / (↑n - ↑p)) ⋯
h0γ : ↑γ = ↑p * (↑n - 1) / (↑n - ↑p)
h1γ : 1 < ↑γ
h2γ : γ * n' = p'
h3γ : (↑γ - 1) * q = ↑p'
h4γ : ↑γ ≠ 0
h3u : ¬∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ = 0
h4u : ∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ ≠ ∞
h5u : (∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ) ^ (1 / q) ≠ 0
h6u : (∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ) ^ (1 / q) ≠ ∞
h7u : Continuous u
v : E → ℝ := fun x ↦ ‖u x‖ ^ ↑γ
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
C : ℝ≥0 := eLpNormLESNormFDerivOneConst μ ↑n'
this :
  (∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ) ^ (1 / ↑n') ≤
    ↑C * ↑γ * (∫⁻ (x : E), ‖fderiv ℝ u x‖ₑ ^ ↑p ∂μ) ^ (1 / ↑p) * (∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ) ^ (1 / q)
⊢ (∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ) ^ (1 / ↑p') ≤ ↑C * ↑γ * (∫⁻ (x : E), ‖fderiv ℝ u x‖ₑ ^ ↑p ∂μ) ^ (1 / ↑p)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TensorProduct

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : 𝕜 ⊗[𝕜] E
x✝¹ : 𝕜
x✝ : E
⊢ ∀ (x : 𝕜) (y : E),
    inner 𝕜 ((TensorProduct.lid 𝕜 E) (x✝¹ ⊗ₜ[𝕜] x✝)) ((TensorProduct.lid 𝕜 E) (x ⊗ₜ[𝕜] y)) =
      inner 𝕜 (x✝¹ ⊗ₜ[𝕜] x✝) (x ⊗ₜ[𝕜] y)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TensorProduct

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : 𝕜 ⊗[𝕜] E
x✝³ : 𝕜
x✝² : E
x✝¹ x✝ : 𝕜 ⊗[𝕜] E
h1 : inner 𝕜 ((TensorProduct.lid 𝕜 E) (x✝³ ⊗ₜ[𝕜] x✝²)) ((TensorProduct.lid 𝕜 E) x✝¹) = inner 𝕜 (x✝³ ⊗ₜ[𝕜] x✝²) x✝¹
h2 : inner 𝕜 ((TensorProduct.lid 𝕜 E) (x✝³ ⊗ₜ[𝕜] x✝²)) ((TensorProduct.lid 𝕜 E) x✝) = inner 𝕜 (x✝³ ⊗ₜ[𝕜] x✝²) x✝
⊢ inner 𝕜 ((TensorProduct.lid 𝕜 E) (x✝³ ⊗ₜ[𝕜] x✝²)) ((TensorProduct.lid 𝕜 E) (x✝¹ + x✝)) =
    inner 𝕜 (x✝³ ⊗ₜ[𝕜] x✝²) (x✝¹ + x✝)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TensorProduct

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y x✝¹ x✝ : 𝕜 ⊗[𝕜] E
h1 : inner 𝕜 ((TensorProduct.lid 𝕜 E) x✝¹) ((TensorProduct.lid 𝕜 E) y) = inner 𝕜 x✝¹ y
h2 : inner 𝕜 ((TensorProduct.lid 𝕜 E) x✝) ((TensorProduct.lid 𝕜 E) y) = inner 𝕜 x✝ y
⊢ inner 𝕜 ((TensorProduct.lid 𝕜 E) (x✝¹ + x✝)) ((TensorProduct.lid 𝕜 E) y) = inner 𝕜 (x✝¹ + x✝) y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TensorProduct

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E ⊗[𝕜] 𝕜
⊢ inner 𝕜 ((TensorProduct.rid 𝕜 E) x) ((TensorProduct.rid 𝕜 E) y) = inner 𝕜 x y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TensorProduct

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
⊢ lidIsometry 𝕜 𝕜 = ridIsometry 𝕜 𝕜

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TensorProduct

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : E ⊗[𝕜] 𝕜
⊢ ‖(TensorProduct.rid 𝕜 E) x‖₊ = ‖x‖₊

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TensorProduct

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
⊢ (commIsometry 𝕜 E 𝕜).trans (lidIsometry 𝕜 E) = ridIsometry 𝕜 E

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TensorProduct

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
⊢ (commIsometry 𝕜 𝕜 E).trans (ridIsometry 𝕜 E) = lidIsometry 𝕜 E

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TensorProduct

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : InnerProductSpace 𝕜 G
x y : E ⊗[𝕜] F ⊗[𝕜] G
⊢ inner 𝕜 ((TensorProduct.assoc 𝕜 E F G) 0) ((TensorProduct.assoc 𝕜 E F G) y) = inner 𝕜 0 y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TensorProduct

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : InnerProductSpace 𝕜 G
x y : E ⊗[𝕜] F ⊗[𝕜] G
a : E ⊗[𝕜] F
x✝ : G
⊢ inner 𝕜 ((TensorProduct.assoc 𝕜 E F G) (a ⊗ₜ[𝕜] x✝)) ((TensorProduct.assoc 𝕜 E F G) 0) = inner 𝕜 (a ⊗ₜ[𝕜] x✝) 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TensorProduct

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : InnerProductSpace 𝕜 G
x y : E ⊗[𝕜] F ⊗[𝕜] G
a : E ⊗[𝕜] F
x✝¹ : G
c : E ⊗[𝕜] F
x✝ : G
⊢ inner 𝕜 ((TensorProduct.assoc 𝕜 E F G) (0 ⊗ₜ[𝕜] x✝¹)) ((TensorProduct.assoc 𝕜 E F G) (c ⊗ₜ[𝕜] x✝)) =
    inner 𝕜 (0 ⊗ₜ[𝕜] x✝¹) (c ⊗ₜ[𝕜] x✝)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TensorProduct

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : InnerProductSpace 𝕜 G
x y : E ⊗[𝕜] F ⊗[𝕜] G
a : E ⊗[𝕜] F
x✝³ : G
c : E ⊗[𝕜] F
x✝² : G
x✝¹ : E
x✝ : F
⊢ inner 𝕜 ((TensorProduct.assoc 𝕜 E F G) (x✝¹ ⊗ₜ[𝕜] x✝ ⊗ₜ[𝕜] x✝³)) ((TensorProduct.assoc 𝕜 E F G) (0 ⊗ₜ[𝕜] x✝²)) =
    inner 𝕜 (x✝¹ ⊗ₜ[𝕜] x✝ ⊗ₜ[𝕜] x✝³) (0 ⊗ₜ[𝕜] x✝²)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TensorProduct

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : InnerProductSpace 𝕜 G
x y : E ⊗[𝕜] F ⊗[𝕜] G
a : E ⊗[𝕜] F
x✝³ : G
c : E ⊗[𝕜] F
x✝² : G
x✝¹ : E
x✝ : F
⊢ ∀ (x : E) (y : F),
    inner 𝕜 ((TensorProduct.assoc 𝕜 E F G) (x✝¹ ⊗ₜ[𝕜] x✝ ⊗ₜ[𝕜] x✝³))
        ((TensorProduct.assoc 𝕜 E F G) (x ⊗ₜ[𝕜] y ⊗ₜ[𝕜] x✝²)) =
      inner 𝕜 (x✝¹ ⊗ₜ[𝕜] x✝ ⊗ₜ[𝕜] x✝³) (x ⊗ₜ[𝕜] y ⊗ₜ[𝕜] x✝²)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TensorProduct

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : InnerProductSpace 𝕜 G
x y : E ⊗[𝕜] F ⊗[𝕜] G
a : E ⊗[𝕜] F
x✝⁵ : G
c : E ⊗[𝕜] F
x✝⁴ : G
x✝³ : E
x✝² : F
x✝¹ x✝ : E ⊗[𝕜] F
h1 :
  inner 𝕜 ((TensorProduct.assoc 𝕜 E F G) (x✝³ ⊗ₜ[𝕜] x✝² ⊗ₜ[𝕜] x✝⁵)) ((TensorProduct.assoc 𝕜 E F G) (x✝¹ ⊗ₜ[𝕜] x✝⁴)) =
    inner 𝕜 (x✝³ ⊗ₜ[𝕜] x✝² ⊗ₜ[𝕜] x✝⁵) (x✝¹ ⊗ₜ[𝕜] x✝⁴)
h2 :
  inner 𝕜 ((TensorProduct.assoc 𝕜 E F G) (x✝³ ⊗ₜ[𝕜] x✝² ⊗ₜ[𝕜] x✝⁵)) ((TensorProduct.assoc 𝕜 E F G) (x✝ ⊗ₜ[𝕜] x✝⁴)) =
    inner 𝕜 (x✝³ ⊗ₜ[𝕜] x✝² ⊗ₜ[𝕜] x✝⁵) (x✝ ⊗ₜ[𝕜] x✝⁴)
⊢ inner 𝕜 ((TensorProduct.assoc 𝕜 E F G) (x✝³ ⊗ₜ[𝕜] x✝² ⊗ₜ[𝕜] x✝⁵))
      ((TensorProduct.assoc 𝕜 E F G) ((x✝¹ + x✝) ⊗ₜ[𝕜] x✝⁴)) =
    inner 𝕜 (x✝³ ⊗ₜ[𝕜] x✝² ⊗ₜ[𝕜] x✝⁵) ((x✝¹ + x✝) ⊗ₜ[𝕜] x✝⁴)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TensorProduct

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : InnerProductSpace 𝕜 G
x y : E ⊗[𝕜] F ⊗[𝕜] G
a : E ⊗[𝕜] F
x✝³ : G
c : E ⊗[𝕜] F
x✝² : G
x✝¹ x✝ : E ⊗[𝕜] F
h1 :
  inner 𝕜 ((TensorProduct.assoc 𝕜 E F G) (x✝¹ ⊗ₜ[𝕜] x✝³)) ((TensorProduct.assoc 𝕜 E F G) (c ⊗ₜ[𝕜] x✝²)) =
    inner 𝕜 (x✝¹ ⊗ₜ[𝕜] x✝³) (c ⊗ₜ[𝕜] x✝²)
h2 :
  inner 𝕜 ((TensorProduct.assoc 𝕜 E F G) (x✝ ⊗ₜ[𝕜] x✝³)) ((TensorProduct.assoc 𝕜 E F G) (c ⊗ₜ[𝕜] x✝²)) =
    inner 𝕜 (x✝ ⊗ₜ[𝕜] x✝³) (c ⊗ₜ[𝕜] x✝²)
⊢ inner 𝕜 ((TensorProduct.assoc 𝕜 E F G) ((x✝¹ + x✝) ⊗ₜ[𝕜] x✝³)) ((TensorProduct.assoc 𝕜 E F G) (c ⊗ₜ[𝕜] x✝²)) =
    inner 𝕜 ((x✝¹ + x✝) ⊗ₜ[𝕜] x✝³) (c ⊗ₜ[𝕜] x✝²)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TensorProduct

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : InnerProductSpace 𝕜 G
x y : E ⊗[𝕜] F ⊗[𝕜] G
a : E ⊗[𝕜] F
x✝² : G
x✝¹ x✝ : E ⊗[𝕜] F ⊗[𝕜] G
h1 :
  inner 𝕜 ((TensorProduct.assoc 𝕜 E F G) (a ⊗ₜ[𝕜] x✝²)) ((TensorProduct.assoc 𝕜 E F G) x✝¹) = inner 𝕜 (a ⊗ₜ[𝕜] x✝²) x✝¹
h2 : inner 𝕜 ((TensorProduct.assoc 𝕜 E F G) (a ⊗ₜ[𝕜] x✝²)) ((TensorProduct.assoc 𝕜 E F G) x✝) = inner 𝕜 (a ⊗ₜ[𝕜] x✝²) x✝
⊢ inner 𝕜 ((TensorProduct.assoc 𝕜 E F G) (a ⊗ₜ[𝕜] x✝²)) ((TensorProduct.assoc 𝕜 E F G) (x✝¹ + x✝)) =
    inner 𝕜 (a ⊗ₜ[𝕜] x✝²) (x✝¹ + x✝)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TensorProduct

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : InnerProductSpace 𝕜 G
x y : E ⊗[𝕜] F ⊗[𝕜] G
x✝¹ x✝ : E ⊗[𝕜] F ⊗[𝕜] G
h1 : inner 𝕜 ((TensorProduct.assoc 𝕜 E F G) x✝¹) ((TensorProduct.assoc 𝕜 E F G) y) = inner 𝕜 x✝¹ y
h2 : inner 𝕜 ((TensorProduct.assoc 𝕜 E F G) x✝) ((TensorProduct.assoc 𝕜 E F G) y) = inner 𝕜 x✝ y
⊢ inner 𝕜 ((TensorProduct.assoc 𝕜 E F G) (x✝¹ + x✝)) ((TensorProduct.assoc 𝕜 E F G) y) = inner 𝕜 (x✝¹ + x✝) y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.TensorProduct

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
H : Type u_5
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 F
inst✝³ : NormedAddCommGroup G
inst✝² : InnerProductSpace 𝕜 G
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace 𝕜 H
f : E →L[𝕜] F
x : E ⊗[𝕜] G
n : ℕ
e : Fin n → E
g : Fin n → G
hx : x = ∑ j, e j ⊗ₜ[𝕜] g j
c : E ⊗[𝕜] G →₀ 𝕜
hc_supp : ↑c.support ⊆ {t | ∃ m n, m ⊗ₜ[𝕜] n = t}
hc : (c.sum fun mi r ↦ r • mi) = x
m : ℕ
A : Fin m → Fin n → 𝕜
hA :
  ‖f‖ ^ 2 • @Matrix.gram E (Fin n) 𝕜 inst✝⁶.toInner e - @Matrix.gram F (Fin n) 𝕜 inst✝⁴.toInner (⇑f ∘ e) =
    ∑ i, Matrix.vecMulVec (A i) (star (A i))
⊢ 0 ≤ ‖f‖ * ‖x‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: E : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
μ : Measure E
inst✝² : μ.IsAddHaarMeasure
F' : Type u_5
inst✝¹ : NormedAddCommGroup F'
inst✝ : InnerProductSpace ℝ F'
u : E → F'
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp✝ : 1 ≤ p
hp'0 : ¬p' = 0
n : ℕ := finrank ℝ E
hn✝ : 0 < n
hp' : (↑p')⁻¹ = ↑p⁻¹ - (↑n)⁻¹
n' : ℝ≥0 := (↑n).conjExponent
h2p : ↑p < ↑n
h0n : 2 ≤ n
hn : (↑n).HolderConjugate n'
h1n : 1 ≤ ↑n
h2n : 0 < ↑n - 1
hnp : 0 < ↑n - ↑p
hp : 1 < p
q : ℝ := (↑p).conjExponent
hq : (↑p).HolderConjugate q
h0p : p ≠ 0
h1p : ↑p ≠ 1
h3p : ↑p - 1 ≠ 0
h2q : 1 / ↑n' - 1 / q = 1 / ↑p'
γ : ℝ≥0 := NNReal.mk (↑p * (↑n - 1) / (↑n - ↑p)) ⋯
h0γ : ↑γ = ↑p * (↑n - 1) / (↑n - ↑p)
h1γ : 1 < ↑γ
h2γ : γ * n' = p'
h3γ : (↑γ - 1) * q = ↑p'
h4γ : ↑γ ≠ 0
h3u : ¬∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ = 0
h4u : ∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ ≠ ∞
h5u : (∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ) ^ (1 / q) ≠ 0
h6u : (∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ) ^ (1 / q) ≠ ∞
h7u : Continuous u
v : E → ℝ := fun x ↦ ‖u x‖ ^ ↑γ
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
C : ℝ≥0 := eLpNormLESNormFDerivOneConst μ ↑n'
this✝ :
  (∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ) ^ (1 / ↑n') ≤
    ↑C * ↑γ * (∫⁻ (x : E), ‖fderiv ℝ u x‖ₑ ^ ↑p ∂μ) ^ (1 / ↑p) * (∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ) ^ (1 / q)
this : ↑C * ↑γ = ↑(eLpNormLESNormFDerivOfEqInnerConst μ ↑p)
⊢ ↑C * ↑γ * (∫⁻ (x : E), ‖fderiv ℝ u x‖ₑ ^ ↑p ∂μ) ^ (1 / ↑p) =
    ↑(eLpNormLESNormFDerivOfEqInnerConst μ ↑p) * eLpNorm (fderiv ℝ u) (↑p) μ

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: E : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : FiniteDimensional ℝ E
μ : Measure E
inst✝² : μ.IsAddHaarMeasure
F' : Type u_5
inst✝¹ : NormedAddCommGroup F'
inst✝ : InnerProductSpace ℝ F'
u : E → F'
hu : ContDiff ℝ 1 u
h2u : HasCompactSupport u
p p' : ℝ≥0
hp✝ : 1 ≤ p
hp'0 : ¬p' = 0
n : ℕ := finrank ℝ E
hn✝ : 0 < n
hp' : (↑p')⁻¹ = ↑p⁻¹ - (↑n)⁻¹
n' : ℝ≥0 := (↑n).conjExponent
h2p : ↑p < ↑n
h0n : 2 ≤ n
hn : (↑n).HolderConjugate n'
h1n : 1 ≤ ↑n
h2n : 0 < ↑n - 1
hnp : 0 < ↑n - ↑p
hp : 1 < p
q : ℝ := (↑p).conjExponent
hq : (↑p).HolderConjugate q
h0p : p ≠ 0
h1p : ↑p ≠ 1
h3p : ↑p - 1 ≠ 0
h2q : 1 / ↑n' - 1 / q = 1 / ↑p'
γ : ℝ≥0 := NNReal.mk (↑p * (↑n - 1) / (↑n - ↑p)) ⋯
h0γ : ↑γ = ↑p * (↑n - 1) / (↑n - ↑p)
h1γ : 1 < ↑γ
h2γ : γ * n' = p'
h3γ : (↑γ - 1) * q = ↑p'
h4γ : ↑γ ≠ 0
h3u : ¬∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ = 0
h4u : ∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ ≠ ∞
h5u : (∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ) ^ (1 / q) ≠ 0
h6u : (∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ) ^ (1 / q) ≠ ∞
h7u : Continuous u
v : E → ℝ := fun x ↦ ‖u x‖ ^ ↑γ
hv : ContDiff ℝ 1 v
h2v : HasCompactSupport v
C : ℝ≥0 := eLpNormLESNormFDerivOneConst μ ↑n'
this :
  (∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ) ^ (1 / ↑n') ≤
    ↑C * ↑γ * (∫⁻ (x : E), ‖fderiv ℝ u x‖ₑ ^ ↑p ∂μ) ^ (1 / ↑p) * (∫⁻ (x : E), ‖u x‖ₑ ^ ↑p' ∂μ) ^ (1 / q)
⊢ ↑C * ↑γ * (∫⁻ (x : E), ‖fderiv ℝ u x‖ₑ ^ ↑p ∂μ) ^ (1 / ↑p) =
    ↑(eLpNormLESNormFDerivOfEqInnerConst μ ↑p) * eLpNorm (fderiv ℝ u) (↑p) μ

Tactic:
by

Goal state after: