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
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
g₁ g₂ : G →L[𝕜] H
x✝ : E ⊗[𝕜] G
⊢ (mapL f (g₁ + g₂)) x✝ = (mapL f g₁ + mapL f g₂) x✝

Tactic:
;

Goal state after:
𝕜 : 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
g₁ g₂ : G →L[𝕜] H
x✝ : E ⊗[𝕜] G
⊢ (mapL f (g₁ + g₂)) x✝ = (mapL f g₁ + mapL f g₂) x✝
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
r : 𝕜
f : E →L[𝕜] F
g : G →L[𝕜] H
x✝ : E ⊗[𝕜] G
⊢ (mapL (r • f) g) x✝ = (r • mapL f g) x✝

Tactic:
;

Goal state after:
𝕜 : 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
r : 𝕜
f : E →L[𝕜] F
g : G →L[𝕜] H
x✝ : E ⊗[𝕜] G
⊢ (mapL (r • f) g) x✝ = (r • mapL f g) x✝
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: case neg
X : Type u_2
inst✝ : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
t : Set X
ht : t ∈ {s | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s}
s : Set X
S : ℕ → Set X := fun n ↦ {x | x ∈ s ∧ (↑n)⁻¹ ≤ infEDist x t}
Ssep : ∀ (n : ℕ), AreSeparated (S n) t
Ssep' : ∀ (n : ℕ), AreSeparated (S n) (s ∩ t)
S_sub : ∀ (n : ℕ), S n ⊆ s \ t
hSs : ∀ (n : ℕ), μ (s ∩ t) + μ (S n) ≤ μ s
iUnion_S : ⋃ n, S n = s \ t
htop : ¬μ (s \ t) = ∞
this : ∀ (n : ℕ), S n ⊆ S (n + 1)
⊢ ∑' (k : ℕ), μ (S (k + 1) \ S k) ≠ ∞

Tactic:
;

Goal state after:
case neg
X : Type u_2
inst✝ : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
t : Set X
ht : t ∈ {s | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s}
s : Set X
S : ℕ → Set X := fun n ↦ {x | x ∈ s ∧ (↑n)⁻¹ ≤ infEDist x t}
Ssep : ∀ (n : ℕ), AreSeparated (S n) t
Ssep' : ∀ (n : ℕ), AreSeparated (S n) (s ∩ t)
S_sub : ∀ (n : ℕ), S n ⊆ s \ t
hSs : ∀ (n : ℕ), μ (s ∩ t) + μ (S n) ≤ μ s
iUnion_S : ⋃ n, S n = s \ t
htop : ¬μ (s \ t) = ∞
this : ∀ (n : ℕ), S n ⊆ S (n + 1)
⊢ ∑' (k : ℕ), μ (S (k + 1) \ S k) ≠ ∞
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
r : 𝕜
f : E →L[𝕜] F
g : G →L[𝕜] H
x✝ : E ⊗[𝕜] G
⊢ (mapL f (r • g)) x✝ = (r • mapL f g) x✝

Tactic:
;

Goal state after:
𝕜 : 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
r : 𝕜
f : E →L[𝕜] F
g : G →L[𝕜] H
x✝ : E ⊗[𝕜] G
⊢ (mapL f (r • g)) x✝ = (r • mapL f g) x✝
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
g : G →L[𝕜] H
x✝¹ : E
x✝ : G
⊢ ((AlgebraTensorModule.curry ↑(mapL f g)) x✝¹) x✝ = ((AlgebraTensorModule.curry (map ↑f ↑g)) x✝¹) x✝

Tactic:
;

Goal state after:
𝕜 : 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
g : G →L[𝕜] H
x✝¹ : E
x✝ : G
⊢ ((AlgebraTensorModule.curry ↑(mapL f g)) x✝¹) x✝ = ((AlgebraTensorModule.curry (map ↑f ↑g)) x✝¹) x✝
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 →ₗᵢ[𝕜] F
g : G →ₗᵢ[𝕜] H
x✝ : E ⊗[𝕜] G
⊢ (mapIsometry f g).toContinuousLinearMap x✝ = (mapL f.toContinuousLinearMap g.toContinuousLinearMap) x✝

Tactic:
;

Goal state after:
𝕜 : 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 →ₗᵢ[𝕜] F
g : G →ₗᵢ[𝕜] H
x✝ : E ⊗[𝕜] G
⊢ (mapIsometry f g).toContinuousLinearMap x✝ = (mapL f.toContinuousLinearMap g.toContinuousLinearMap) x✝
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
A : Type u_6
B : Type u_7
inst✝³ : NormedAddCommGroup A
inst✝² : InnerProductSpace 𝕜 A
inst✝¹ : NormedAddCommGroup B
inst✝ : InnerProductSpace 𝕜 B
f₁ : E →L[𝕜] F
f₂ : A →L[𝕜] E
g₁ : G →L[𝕜] H
g₂ : B →L[𝕜] G
x✝ : A ⊗[𝕜] B
⊢ (mapL (f₁ ∘SL f₂) (g₁ ∘SL g₂)) x✝ = (mapL f₁ g₁ ∘SL mapL f₂ g₂) x✝

Tactic:
;

Goal state after:
𝕜 : 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
A : Type u_6
B : Type u_7
inst✝³ : NormedAddCommGroup A
inst✝² : InnerProductSpace 𝕜 A
inst✝¹ : NormedAddCommGroup B
inst✝ : InnerProductSpace 𝕜 B
f₁ : E →L[𝕜] F
f₂ : A →L[𝕜] E
g₁ : G →L[𝕜] H
g₂ : B →L[𝕜] G
x✝ : A ⊗[𝕜] B
⊢ (mapL (f₁ ∘SL f₂) (g₁ ∘SL g₂)) x✝ = (mapL f₁ g₁ ∘SL mapL f₂ g₂) x✝
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
A : Type u_6
inst✝¹ : NormedAddCommGroup A
inst✝ : InnerProductSpace 𝕜 A
f₁ : E →L[𝕜] F
f₂ : A →L[𝕜] E
g : G →L[𝕜] H
x✝ : A ⊗[𝕜] G
⊢ (mapL f₁ g ∘SL ContinuousLinearMap.rTensor G f₂) x✝ = (mapL (f₁ ∘SL f₂) g) x✝

Tactic:
;

Goal state after:
𝕜 : 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
A : Type u_6
inst✝¹ : NormedAddCommGroup A
inst✝ : InnerProductSpace 𝕜 A
f₁ : E →L[𝕜] F
f₂ : A →L[𝕜] E
g : G →L[𝕜] H
x✝ : A ⊗[𝕜] G
⊢ (mapL f₁ g ∘SL ContinuousLinearMap.rTensor G f₂) x✝ = (mapL (f₁ ∘SL f₂) g) x✝
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
A : Type u_6
inst✝¹ : NormedAddCommGroup A
inst✝ : InnerProductSpace 𝕜 A
f : E →L[𝕜] F
g₁ : G →L[𝕜] H
g₂ : A →L[𝕜] G
x✝ : E ⊗[𝕜] A
⊢ (mapL f g₁ ∘SL ContinuousLinearMap.lTensor E g₂) x✝ = (mapL f (g₁ ∘SL g₂)) x✝

Tactic:
;

Goal state after:
𝕜 : 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
A : Type u_6
inst✝¹ : NormedAddCommGroup A
inst✝ : InnerProductSpace 𝕜 A
f : E →L[𝕜] F
g₁ : G →L[𝕜] H
g₂ : A →L[𝕜] G
x✝ : E ⊗[𝕜] A
⊢ (mapL f g₁ ∘SL ContinuousLinearMap.lTensor E g₂) x✝ = (mapL f (g₁ ∘SL g₂)) x✝
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
A : Type u_6
inst✝¹ : NormedAddCommGroup A
inst✝ : InnerProductSpace 𝕜 A
f₁ : E →L[𝕜] F
f₂ : A →L[𝕜] E
g : G →L[𝕜] H
x✝ : A ⊗[𝕜] G
⊢ (ContinuousLinearMap.rTensor H f₁ ∘SL mapL f₂ g) x✝ = (mapL (f₁ ∘SL f₂) g) x✝

Tactic:
;

Goal state after:
𝕜 : 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
A : Type u_6
inst✝¹ : NormedAddCommGroup A
inst✝ : InnerProductSpace 𝕜 A
f₁ : E →L[𝕜] F
f₂ : A →L[𝕜] E
g : G →L[𝕜] H
x✝ : A ⊗[𝕜] G
⊢ (ContinuousLinearMap.rTensor H f₁ ∘SL mapL f₂ g) x✝ = (mapL (f₁ ∘SL f₂) g) x✝
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
A : Type u_6
inst✝¹ : NormedAddCommGroup A
inst✝ : InnerProductSpace 𝕜 A
f : E →L[𝕜] F
g₁ : G →L[𝕜] H
g₂ : A →L[𝕜] G
x✝ : E ⊗[𝕜] A
⊢ (ContinuousLinearMap.lTensor F g₁ ∘SL mapL f g₂) x✝ = (mapL f (g₁ ∘SL g₂)) x✝

Tactic:
;

Goal state after:
𝕜 : 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
A : Type u_6
inst✝¹ : NormedAddCommGroup A
inst✝ : InnerProductSpace 𝕜 A
f : E →L[𝕜] F
g₁ : G →L[𝕜] H
g₂ : A →L[𝕜] G
x✝ : E ⊗[𝕜] A
⊢ (ContinuousLinearMap.lTensor F g₁ ∘SL mapL f g₂) x✝ = (mapL f (g₁ ∘SL g₂)) x✝
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
g : G →L[𝕜] H
x✝ : G ⊗[𝕜] E
⊢ (ContinuousLinearMap.lTensor H f ∘SL ContinuousLinearMap.rTensor E g) x✝ = (mapL g f) x✝

Tactic:
;

Goal state after:
𝕜 : 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
g : G →L[𝕜] H
x✝ : G ⊗[𝕜] E
⊢ (ContinuousLinearMap.lTensor H f ∘SL ContinuousLinearMap.rTensor E g) x✝ = (mapL g f) x✝
Module: Mathlib.Analysis.InnerProductSpace.TensorProduct

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
G : Type u_4
H : Type u_5
inst✝¹¹ : RCLike 𝕜
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : InnerProductSpace 𝕜 E
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : InnerProductSpace 𝕜 G
inst✝⁶ : NormedAddCommGroup H
inst✝⁵ : InnerProductSpace 𝕜 H
inst✝⁴ : CompleteSpace E
inst✝³ : CompleteSpace G
inst✝² : CompleteSpace (E ⊗[𝕜] H)
inst✝¹ : CompleteSpace (E ⊗[𝕜] G)
inst✝ : CompleteSpace H
g : G →L[𝕜] H
⊢ ContinuousLinearMap.adjoint (ContinuousLinearMap.lTensor E g) =
    ContinuousLinearMap.lTensor E (ContinuousLinearMap.adjoint g)

Tactic:
by simp [ContinuousLinearMap.lTensor_eq_mapL]

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

Goal state before:
pp: F : Type u_3
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
E : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
inst✝ : FiniteDimensional ℝ F
u : E → F
s : Set E
hu : ContDiff ℝ 1 u
h2u : support u ⊆ s
p q : ℝ≥0
hp : 1 ≤ p
h2p : p < ↑(finrank ℝ E)
hpq : ↑p⁻¹ - (↑(finrank ℝ E))⁻¹ ≤ (↑q)⁻¹
hs : Bornology.IsBounded s
hq0 : ¬q = 0
p' : ℝ≥0 := (p⁻¹ - (↑(finrank ℝ E))⁻¹)⁻¹
hp' : ↑p'⁻¹ = ↑p⁻¹ - (↑(finrank ℝ E))⁻¹
this : ↑q ≤ ↑p'
t : ℝ≥0 := (μ s).toNNReal ^ (1 / ↑q - 1 / ↑p')
C : ℝ≥0 := SNormLESNormFDerivOfEqConst F μ ↑p
⊢ ↑C * eLpNorm (fderiv ℝ u) (↑p) μ * ↑t =
    ↑((μ s).toNNReal ^ (1 / ↑q - 1 / ↑(p⁻¹ - (↑(finrank ℝ E))⁻¹)⁻¹)) * ↑(SNormLESNormFDerivOfEqConst F μ ↑p) *
      eLpNorm (fderiv ℝ u) (↑p) μ

Tactic:
;

Goal state after:
F : Type u_3
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
E : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
inst✝ : FiniteDimensional ℝ F
u : E → F
s : Set E
hu : ContDiff ℝ 1 u
h2u : support u ⊆ s
p q : ℝ≥0
hp : 1 ≤ p
h2p : p < ↑(finrank ℝ E)
hpq : ↑p⁻¹ - (↑(finrank ℝ E))⁻¹ ≤ (↑q)⁻¹
hs : Bornology.IsBounded s
hq0 : ¬q = 0
p' : ℝ≥0 := (p⁻¹ - (↑(finrank ℝ E))⁻¹)⁻¹
hp' : ↑p'⁻¹ = ↑p⁻¹ - (↑(finrank ℝ E))⁻¹
this : ↑q ≤ ↑p'
t : ℝ≥0 := (μ s).toNNReal ^ (1 / ↑q - 1 / ↑p')
C : ℝ≥0 := SNormLESNormFDerivOfEqConst F μ ↑p
⊢ ↑C * eLpNorm (fderiv ℝ u) (↑p) μ * ↑t =
    ↑((μ s).toNNReal ^ (1 / ↑q - 1 / ↑(p⁻¹ - (↑(finrank ℝ E))⁻¹)⁻¹)) * ↑(SNormLESNormFDerivOfEqConst F μ ↑p) *
      eLpNorm (fderiv ℝ u) (↑p) μ
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
s : Set X
this✝¹ : MeasurableSpace X := borel X
this✝ : BorelSpace X
⊢ ℝ≥0∞

Tactic:
;

Goal state after:
ι : Type u_1
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
s : Set X
this✝¹ : MeasurableSpace X := borel X
this✝ : BorelSpace X
⊢ ℝ≥0∞
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: X : Type u_2
inst✝¹ : EMetricSpace X
s : Set X
inst✝ : BorelSpace X
this✝ : MeasurableSpace X := borel X
⊢ dimH s = ⨆ d, ⨆ (_ : μH[↑d] s = ∞), ↑d

Tactic:
;

Goal state after:
X : Type u_2
inst✝¹ : EMetricSpace X
s : Set X
inst✝ : BorelSpace X
this✝ : MeasurableSpace X := borel X
⊢ dimH s = ⨆ d, ⨆ (_ : μH[↑d] s = ∞), ↑d
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
⊢ dimH s = ⨆ d, ⨆ (_ : μH[↑d] s = ∞), ↑d

Tactic:
borelize X; rw [dimH]

Goal state after:
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
d : ℝ≥0
h : μH[↑d] s = ∞
⊢ ↑d ≤ ⨆ d, ⨆ (_ : μH[↑d] s = ∞), ↑d

Tactic:
;

Goal state after:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
d : ℝ≥0
h : μH[↑d] s = ∞
⊢ ↑d ≤ ⨆ d, ⨆ (_ : μH[↑d] s = ∞), ↑d
Module: Mathlib.Analysis.FunctionalSpaces.SobolevInequality

Goal state before:
pp: F : Type u_3
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace ℝ F
E : Type u_4
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
μ : Measure E
inst✝¹ : μ.IsAddHaarMeasure
inst✝ : FiniteDimensional ℝ F
u : E → F
s : Set E
hu : ContDiff ℝ 1 u
h2u : support u ⊆ s
p : ℝ≥0
hp : 1 ≤ p
h2p : p < ↑(finrank ℝ E)
hs : Bornology.IsBounded s
⊢ eLpNorm u (↑p) μ ≤ ↑(eLpNormLESNormFDerivOfLeConst F μ s p p) * eLpNorm (fderiv ℝ u) (↑p) μ

Tactic:
by
  refine eLpNorm_le_eLpNorm_fderiv_of_le μ hu h2u hp h2p ?_ hs
  norm_cast
  simp only [tsub_le_iff_right, le_add_iff_nonneg_right]
  positivity

Goal state after:
Module: Mathlib.Geometry.Euclidean.Volume.Measure

Goal state before:
pp: V : Type u_3
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : FiniteDimensional ℝ V
⊢ μHE[finrank ℝ V] = volume

Tactic:
rw [← (stdOrthonormalBasis ℝ V).measurePreserving_repr_symm.map_eq,
    ← (stdOrthonormalBasis ℝ V).repr.toIsometryEquiv
      |>.symm.measurePreserving_euclideanHausdorffMeasure _ |>.map_eq,
    EuclideanSpace.euclideanHausdorffMeasure_eq_volume]

Goal state after:
V : Type u_3
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : FiniteDimensional ℝ V
⊢ map (⇑(stdOrthonormalBasis ℝ V).repr.toIsometryEquiv.symm) volume = map (⇑(stdOrthonormalBasis ℝ V).repr.symm) volume
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: X : Type u_2
inst✝¹ : EMetricSpace X
inst✝ : SecondCountableTopology X
s : Set X
r : ℝ≥0∞
h : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, dimH t ≤ r
⊢ dimH s ≤ r

Tactic:
;

Goal state after:
X : Type u_2
inst✝¹ : EMetricSpace X
inst✝ : SecondCountableTopology X
s : Set X
r : ℝ≥0∞
h : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, dimH t ≤ r
⊢ dimH s ≤ r
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: case refine_2
X : Type u_2
inst✝¹ : EMetricSpace X
inst✝ : SecondCountableTopology X
s : Set X
r : ℝ≥0∞
hr : r < dimH s
x : X
hxs : x ∈ s
hxr : ∀ t ∈ 𝓝[s] x, r < dimH t
⊢ r ≤ limsup dimH (𝓝[s] x).smallSets

Tactic:
;

Goal state after:
case refine_2
X : Type u_2
inst✝¹ : EMetricSpace X
inst✝ : SecondCountableTopology X
s : Set X
r : ℝ≥0∞
hr : r < dimH s
x : X
hxs : x ∈ s
hxr : ∀ t ∈ 𝓝[s] x, r < dimH t
⊢ r ≤ limsup dimH (𝓝[s] x).smallSets
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: case refine_2
X : Type u_2
inst✝¹ : EMetricSpace X
inst✝ : SecondCountableTopology X
s : Set X
r : ℝ≥0∞
hr : r < dimH s
x : X
hxs : x ∈ s
hxr : ∀ t ∈ 𝓝[s] x, r < dimH t
⊢ r ≤ sInf {a | ∀ᶠ (n : Set X) in (𝓝[s] x).smallSets, dimH n ≤ a}

Tactic:
;

Goal state after:
case refine_2
X : Type u_2
inst✝¹ : EMetricSpace X
inst✝ : SecondCountableTopology X
s : Set X
r : ℝ≥0∞
hr : r < dimH s
x : X
hxs : x ∈ s
hxr : ∀ t ∈ 𝓝[s] x, r < dimH t
⊢ r ≤ sInf {a | ∀ᶠ (n : Set X) in (𝓝[s] x).smallSets, dimH n ≤ a}
Module: Mathlib.MeasureTheory.Measure.Hausdorff

Goal state before:
pp: X : Type u_2
inst✝ : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
t : Set X
ht : t ∈ {s | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s}
s : Set X
S : ℕ → Set X := fun n ↦ {x | x ∈ s ∧ (↑n)⁻¹ ≤ infEDist x t}
Ssep : ∀ (n : ℕ), AreSeparated (S n) t
Ssep' : ∀ (n : ℕ), AreSeparated (S n) (s ∩ t)
S_sub : ∀ (n : ℕ), S n ⊆ s \ t
hSs : ∀ (n : ℕ), μ (s ∩ t) + μ (S n) ≤ μ s
iUnion_S : ⋃ n, S n = s \ t
htop : ¬μ (s \ t) = ∞
r n i j : ℕ
hj : i < j
⊢ 2 * i + 1 + r < 2 * j + r

Tactic:
;

Goal state after:
X : Type u_2
inst✝ : EMetricSpace X
μ : OuterMeasure X
hm : μ.IsMetric
t : Set X
ht : t ∈ {s | IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s}
s : Set X
S : ℕ → Set X := fun n ↦ {x | x ∈ s ∧ (↑n)⁻¹ ≤ infEDist x t}
Ssep : ∀ (n : ℕ), AreSeparated (S n) t
Ssep' : ∀ (n : ℕ), AreSeparated (S n) (s ∩ t)
S_sub : ∀ (n : ℕ), S n ⊆ s \ t
hSs : ∀ (n : ℕ), μ (s ∩ t) + μ (S n) ≤ μ s
iUnion_S : ⋃ n, S n = s \ t
htop : ¬μ (s \ t) = ∞
r n i j : ℕ
hj : i < j
⊢ 2 * i + 1 + r < 2 * j + r
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: case refine_2
X : Type u_2
inst✝¹ : EMetricSpace X
inst✝ : SecondCountableTopology X
s : Set X
⊢ ⨆ x ∈ s, limsup dimH (𝓝[s] x).smallSets ≤ ⨆ x, limsup dimH (𝓝[s] x).smallSets

Tactic:
;

Goal state after:
case refine_2
X : Type u_2
inst✝¹ : EMetricSpace X
inst✝ : SecondCountableTopology X
s : Set X
⊢ ⨆ x ∈ s, limsup dimH (𝓝[s] x).smallSets ≤ ⨆ x, limsup dimH (𝓝[s] x).smallSets
Module: Mathlib.Topology.MetricSpace.HausdorffDimension

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
this✝³ : MeasurableSpace X := borel X
this✝² : BorelSpace X
this✝¹ : MeasurableSpace Y := borel Y
this✝ : BorelSpace Y
d : ℝ≥0
hd : μH[↑d] (f '' s) = ∞
this : ↑(C ^ ↑d) * μH[↑r * ↑d] s = ∞
Hrd : μH[↑(r * d)] s = ∞
⊢ ↑r * ↑d ≤ dimH s

pp: case h0
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
this✝³ : MeasurableSpace X := borel X
this✝² : BorelSpace X
this✝¹ : MeasurableSpace Y := borel Y
this✝ : BorelSpace Y
d : ℝ≥0
hd : μH[↑d] (f '' s) = ∞
this : ↑(C ^ ↑d) * μH[↑r * ↑d] s = ∞
Hrd : μH[↑(r * d)] s = ∞
⊢ ↑r ≠ 0 ∨ dimH s ≠ 0

pp: case ht
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
this✝³ : MeasurableSpace X := borel X
this✝² : BorelSpace X
this✝¹ : MeasurableSpace Y := borel Y
this✝ : BorelSpace Y
d : ℝ≥0
hd : μH[↑d] (f '' s) = ∞
this : ↑(C ^ ↑d) * μH[↑r * ↑d] s = ∞
Hrd : μH[↑(r * d)] s = ∞
⊢ ↑r ≠ ∞ ∨ dimH s ≠ ∞

Tactic:
← ENNReal.coe_mul

Goal state after:
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
this✝³ : MeasurableSpace X := borel X
this✝² : BorelSpace X
this✝¹ : MeasurableSpace Y := borel Y
this✝ : BorelSpace Y
d : ℝ≥0
hd : μH[↑d] (f '' s) = ∞
this : ↑(C ^ ↑d) * μH[↑r * ↑d] s = ∞
Hrd : μH[↑(r * d)] s = ∞
⊢ ↑(r * d) ≤ dimH s

case h0
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
this✝³ : MeasurableSpace X := borel X
this✝² : BorelSpace X
this✝¹ : MeasurableSpace Y := borel Y
this✝ : BorelSpace Y
d : ℝ≥0
hd : μH[↑d] (f '' s) = ∞
this : ↑(C ^ ↑d) * μH[↑r * ↑d] s = ∞
Hrd : μH[↑(r * d)] s = ∞
⊢ ↑r ≠ 0 ∨ dimH s ≠ 0

case ht
X : Type u_2
Y : Type u_3
inst✝¹ : EMetricSpace X
inst✝ : EMetricSpace Y
C r : ℝ≥0
f : X → Y
s : Set X
h : HolderOnWith C r f s
hr : 0 < r
this✝³ : MeasurableSpace X := borel X
this✝² : BorelSpace X
this✝¹ : MeasurableSpace Y := borel Y
this✝ : BorelSpace Y
d : ℝ≥0
hd : μH[↑d] (f '' s) = ∞
this : ↑(C ^ ↑d) * μH[↑r * ↑d] s = ∞
Hrd : μH[↑(r * d)] s = ∞
⊢ ↑r ≠ ∞ ∨ dimH s ≠ ∞