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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T S : E →ₗ[𝕜] E
hT : T.IsSymmetric
hS : S.IsSymmetric
x y : E
⊢ ⟪x, T y⟫ + ⟪S x, y⟫ = ⟪x, (T + S) y⟫

Tactic:
hS x y,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T S : E →ₗ[𝕜] E
hT : T.IsSymmetric
hS : S.IsSymmetric
x y : E
⊢ ⟪x, T y⟫ + ⟪x, S y⟫ = ⟪x, (T + S) y⟫
Module: Mathlib.Analysis.InnerProductSpace.Symmetric

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T S : E →ₗ[𝕜] E
hT : T.IsSymmetric
hS : S.IsSymmetric
x y : E
⊢ ⟪x, T y⟫ - ⟪S x, y⟫ = ⟪x, (T - S) y⟫

Tactic:
hS x y,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T S : E →ₗ[𝕜] E
hT : T.IsSymmetric
hS : S.IsSymmetric
x y : E
⊢ ⟪x, T y⟫ - ⟪x, S y⟫ = ⟪x, (T - S) y⟫
Module: Mathlib.Analysis.InnerProductSpace.Symmetric

Goal state before:
pp: case mpr
V : Type u_3
inst✝¹ : SeminormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
h : ∀ (v : V), (starRingEnd ℂ) ⟪T v, v⟫_ℂ = ⟪T v, v⟫_ℂ
x y : V
⊢ ⟪T x, y⟫_ℂ = (starRingEnd ℂ) ⟪T y, x⟫_ℂ

Tactic:
inner_map_polarization T x y

Goal state after:
case mpr
V : Type u_3
inst✝¹ : SeminormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
h : ∀ (v : V), (starRingEnd ℂ) ⟪T v, v⟫_ℂ = ⟪T v, v⟫_ℂ
x y : V
⊢ ⟪T x, y⟫_ℂ =
    (starRingEnd ℂ)
      ((⟪T (x + y), x + y⟫_ℂ - ⟪T (x - y), x - y⟫_ℂ + Complex.I * ⟪T (x + Complex.I • y), x + Complex.I • y⟫_ℂ -
          Complex.I * ⟪T (x - Complex.I • y), x - Complex.I • y⟫_ℂ) /
        4)
Module: Mathlib.Analysis.InnerProductSpace.Orthogonal

Goal state before:
pp: case e'_1.e'_6
𝕜 : 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
f : E ≃ₗᵢ[𝕜] F
U V : Submodule 𝕜 F
⊢ Submodule.comap (↑↑↑f) U = Submodule.map (↑↑↑f.symm) U

pp: case e'_1.e'_7
𝕜 : 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
f : E ≃ₗᵢ[𝕜] F
U V : Submodule 𝕜 F
⊢ Submodule.comap (↑↑↑f) V = Submodule.map (↑↑↑f.symm) V

Tactic:
<;>

Goal state after:
case e'_1.e'_6
𝕜 : 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
f : E ≃ₗᵢ[𝕜] F
U V : Submodule 𝕜 F
⊢ Submodule.comap (↑↑↑f) U = Submodule.map (↑↑↑f.symm) U

case e'_1.e'_7
𝕜 : 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
f : E ≃ₗᵢ[𝕜] F
U V : Submodule 𝕜 F
⊢ Submodule.comap (↑↑↑f) V = Submodule.map (↑↑↑f.symm) V
Module: Mathlib.Analysis.InnerProductSpace.Symmetric

Goal state before:
pp: case mpr
V : Type u_3
inst✝¹ : SeminormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
h : ∀ (v : V), (starRingEnd ℂ) ⟪T v, v⟫_ℂ = ⟪T v, v⟫_ℂ
x y : V
⊢ ⟪T x, y⟫_ℂ =
    (⟪T (x + y), x + y⟫_ℂ - ⟪T (x - y), x - y⟫_ℂ + ⟪T (x + Complex.I • y), x + Complex.I • y⟫_ℂ * -Complex.I -
        ⟪T (x - Complex.I • y), x - Complex.I • y⟫_ℂ * -Complex.I) /
      (starRingEnd ℂ) 4

Tactic:
rw [inner_map_polarization']

Goal state after:
case mpr
V : Type u_3
inst✝¹ : SeminormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
h : ∀ (v : V), (starRingEnd ℂ) ⟪T v, v⟫_ℂ = ⟪T v, v⟫_ℂ
x y : V
⊢ (⟪T (x + y), x + y⟫_ℂ - ⟪T (x - y), x - y⟫_ℂ - Complex.I * ⟪T (x + Complex.I • y), x + Complex.I • y⟫_ℂ +
        Complex.I * ⟪T (x - Complex.I • y), x - Complex.I • y⟫_ℂ) /
      4 =
    (⟪T (x + y), x + y⟫_ℂ - ⟪T (x - y), x - y⟫_ℂ + ⟪T (x + Complex.I • y), x + Complex.I • y⟫_ℂ * -Complex.I -
        ⟪T (x - Complex.I • y), x - Complex.I • y⟫_ℂ * -Complex.I) /
      (starRingEnd ℂ) 4
Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule

Goal state before:
pp: case mp
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : CompleteSpace E
⊢ Kᗮᗮ = ⊤ → Kᗮ = ⊥

pp: case mpr
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : CompleteSpace E
⊢ Kᗮ = ⊥ → Kᗮᗮ = ⊤

Tactic:
<;>

Goal state after:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : CompleteSpace E
⊢ Kᗮᗮ = ⊤ → Kᗮ = ⊥

case mpr
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : CompleteSpace E
⊢ Kᗮ = ⊥ → Kᗮᗮ = ⊤
Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : CompleteSpace E
⊢ K.topologicalClosure = ⊤ ↔ Kᗮ = ⊥

Tactic:
rw [← K.orthogonal_orthogonal_eq_closure]
  constructor <;> intro h
  · rw [← Submodule.triorthogonal_eq_orthogonal, h, Submodule.top_orthogonal_eq_bot]
  · rw [h, Submodule.bot_orthogonal_eq_top]

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic

Goal state before:
pp: case hvm
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
v : ↥K
⊢ ↑v ∈ K

pp: case hvo
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
v : ↥K
⊢ ∀ w ∈ K, ⟪↑v - ↑v, w⟫ = 0

Tactic:
<;>

Goal state after:
case hvm
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
v : ↥K
⊢ ↑v ∈ K

case hvo
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
v : ↥K
⊢ ∀ w ∈ K, ⟪↑v - ↑v, w⟫ = 0
Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
hK : K ≠ ⊥
⊢ ‖K.orthogonalProjectionOnto‖ = 1

Tactic:
refine le_antisymm K.orthogonalProjectionOnto_norm_le ?_

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
hK : K ≠ ⊥
⊢ 1 ≤ ‖K.orthogonalProjectionOnto‖
Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic

Goal state before:
pp: case e'_2
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v w : E
hv : ¬v = 0
hv' : ‖v‖ ≠ 0
key : ((↑(‖v‖ ^ 2))⁻¹ * ↑(‖v‖ ^ 2)) • (𝕜 ∙ v).starProjection w = ((↑(‖v‖ ^ 2))⁻¹ * ⟪v, w⟫) • v
⊢ (𝕜 ∙ v).starProjection w = ((↑(‖v‖ ^ 2))⁻¹ * ↑(‖v‖ ^ 2)) • (𝕜 ∙ v).starProjection w

pp: case e'_3
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v w : E
hv : ¬v = 0
hv' : ‖v‖ ≠ 0
key : ((↑(‖v‖ ^ 2))⁻¹ * ↑(‖v‖ ^ 2)) • (𝕜 ∙ v).starProjection w = ((↑(‖v‖ ^ 2))⁻¹ * ⟪v, w⟫) • v
⊢ (⟪v, w⟫ / ↑(‖v‖ ^ 2)) • v = ((↑(‖v‖ ^ 2))⁻¹ * ⟪v, w⟫) • v

Tactic:
<;>

Goal state after:
case e'_2
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v w : E
hv : ¬v = 0
hv' : ‖v‖ ≠ 0
key : ((↑(‖v‖ ^ 2))⁻¹ * ↑(‖v‖ ^ 2)) • (𝕜 ∙ v).starProjection w = ((↑(‖v‖ ^ 2))⁻¹ * ⟪v, w⟫) • v
⊢ (𝕜 ∙ v).starProjection w = ((↑(‖v‖ ^ 2))⁻¹ * ↑(‖v‖ ^ 2)) • (𝕜 ∙ v).starProjection w

case e'_3
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v w : E
hv : ¬v = 0
hv' : ‖v‖ ≠ 0
key : ((↑(‖v‖ ^ 2))⁻¹ * ↑(‖v‖ ^ 2)) • (𝕜 ∙ v).starProjection w = ((↑(‖v‖ ^ 2))⁻¹ * ⟪v, w⟫) • v
⊢ (⟪v, w⟫ / ↑(‖v‖ ^ 2)) • v = ((↑(‖v‖ ^ 2))⁻¹ * ⟪v, w⟫) • v
Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v w : E
hv : ¬v = 0
hv' : ‖v‖ ≠ 0
key : ((↑(‖v‖ ^ 2))⁻¹ * ↑(‖v‖ ^ 2)) • (𝕜 ∙ v).starProjection w = ((↑(‖v‖ ^ 2))⁻¹ * ⟪v, w⟫) • v
⊢ 1 = (↑‖v‖ ^ 2)⁻¹ * ↑‖v‖ ^ 2 * 1

pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v w : E
hv : ¬v = 0
hv' : ‖v‖ ≠ 0
key : ((↑(‖v‖ ^ 2))⁻¹ * ↑(‖v‖ ^ 2)) • (𝕜 ∙ v).starProjection w = ((↑(‖v‖ ^ 2))⁻¹ * ⟪v, w⟫) • v
⊢ ⟪v, w⟫ / ↑‖v‖ ^ 2 * 1 = (↑‖v‖ ^ 2)⁻¹ * ⟪v, w⟫ * 1

Tactic:
<;>

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v w : E
hv : ¬v = 0
hv' : ‖v‖ ≠ 0
key : ((↑(‖v‖ ^ 2))⁻¹ * ↑(‖v‖ ^ 2)) • (𝕜 ∙ v).starProjection w = ((↑(‖v‖ ^ 2))⁻¹ * ⟪v, w⟫) • v
⊢ 1 = (↑‖v‖ ^ 2)⁻¹ * ↑‖v‖ ^ 2 * 1

𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v w : E
hv : ¬v = 0
hv' : ‖v‖ ≠ 0
key : ((↑(‖v‖ ^ 2))⁻¹ * ↑(‖v‖ ^ 2)) • (𝕜 ∙ v).starProjection w = ((↑(‖v‖ ^ 2))⁻¹ * ⟪v, w⟫) • v
⊢ ⟪v, w⟫ / ↑‖v‖ ^ 2 * 1 = (↑‖v‖ ^ 2)⁻¹ * ⟪v, w⟫ * 1
Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : Kᗮ.HasOrthogonalProjection
v : E
hv : v ∈ K
⊢ ↑(Kᗮ.orthogonalProjectionOnto v) = 0

Tactic:
coe_eq_zero

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : Kᗮ.HasOrthogonalProjection
v : E
hv : v ∈ K
⊢ Kᗮ.orthogonalProjectionOnto v = 0
Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : Kᗮ.HasOrthogonalProjection
v : E
hv : v ∈ K
⊢ Kᗮ.orthogonalProjectionOnto v = 0

Tactic:
exact orthogonalProjectionOnto_orthogonal_apply_eq_zero hv

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v : E
⊢ ↑((𝕜 ∙ v)ᗮ.orthogonalProjectionOnto v) = 0

Tactic:
coe_eq_zero

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v : E
⊢ (𝕜 ∙ v)ᗮ.orthogonalProjectionOnto v = 0
Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
v : E
⊢ ‖v‖ * ‖v‖ - ‖↑(K.orthogonalProjectionOnto v) - v‖ * ‖↑(K.orthogonalProjectionOnto v) - v‖ =
    ‖K.orthogonalProjectionOnto v‖ * ‖K.orthogonalProjectionOnto v‖ * 2 -
      ‖↑(K.orthogonalProjectionOnto v)‖ * ‖↑(K.orthogonalProjectionOnto v)‖

Tactic:
coe_norm,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
v : E
⊢ ‖v‖ * ‖v‖ - ‖↑(K.orthogonalProjectionOnto v) - v‖ * ‖↑(K.orthogonalProjectionOnto v) - v‖ =
    ‖↑(K.orthogonalProjectionOnto v)‖ * ‖↑(K.orthogonalProjectionOnto v)‖ * 2 -
      ‖↑(K.orthogonalProjectionOnto v)‖ * ‖↑(K.orthogonalProjectionOnto v)‖
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: case h₁
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp✝ : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f g h : WithLp p (α × β)
hp : 1 ≤ p.toReal
⊢ edist f.fst h.fst ≤ edist f.fst g.fst + edist g.fst h.fst

pp: case h₁
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp✝ : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f g h : WithLp p (α × β)
hp : 1 ≤ p.toReal
⊢ edist f.snd h.snd ≤ edist f.snd g.snd + edist g.snd h.snd

Tactic:
<;>

Goal state after:
case h₁
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp✝ : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f g h : WithLp p (α × β)
hp : 1 ≤ p.toReal
⊢ edist f.fst h.fst ≤ edist f.fst g.fst + edist g.fst h.fst

case h₁
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp✝ : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f g h : WithLp p (α × β)
hp : 1 ≤ p.toReal
⊢ edist f.snd h.snd ≤ edist f.snd g.snd + edist g.snd h.snd
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: case pos
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f g : WithLp p (α × β)
h : 1 ≤ p.toReal
hp' : p = 0
h✝¹ : dist f.fst g.fst = 0
h✝ : dist f.snd g.snd = 0
⊢ 0 ≤ 0 + 0

pp: case neg
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f g : WithLp p (α × β)
h : 1 ≤ p.toReal
hp' : p = 0
h✝¹ : dist f.fst g.fst = 0
h✝ : ¬dist f.snd g.snd = 0
⊢ 0 ≤ 0 + 1

pp: case pos
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f g : WithLp p (α × β)
h : 1 ≤ p.toReal
hp' : p = 0
h✝¹ : ¬dist f.fst g.fst = 0
h✝ : dist f.snd g.snd = 0
⊢ 0 ≤ 1 + 0

pp: case neg
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f g : WithLp p (α × β)
h : 1 ≤ p.toReal
hp' : p = 0
h✝¹ : ¬dist f.fst g.fst = 0
h✝ : ¬dist f.snd g.snd = 0
⊢ 0 ≤ 1 + 1

pp: case pos
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f g : WithLp p (α × β)
h : 1 ≤ p.toReal
hp' : ¬p = 0
h✝ : p = ∞
⊢ 0 ≤ max (dist f.fst g.fst) (dist f.snd g.snd)

pp: case neg
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f g : WithLp p (α × β)
h : 1 ≤ p.toReal
hp' : ¬p = 0
h✝ : ¬p = ∞
⊢ 0 ≤ (dist f.fst g.fst ^ p.toReal + dist f.snd g.snd ^ p.toReal) ^ p.toReal⁻¹

Tactic:
<;>

Goal state after:
case pos
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f g : WithLp p (α × β)
h : 1 ≤ p.toReal
hp' : p = 0
h✝¹ : dist f.fst g.fst = 0
h✝ : dist f.snd g.snd = 0
⊢ 0 ≤ 0 + 0

case neg
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f g : WithLp p (α × β)
h : 1 ≤ p.toReal
hp' : p = 0
h✝¹ : dist f.fst g.fst = 0
h✝ : ¬dist f.snd g.snd = 0
⊢ 0 ≤ 0 + 1

case pos
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f g : WithLp p (α × β)
h : 1 ≤ p.toReal
hp' : p = 0
h✝¹ : ¬dist f.fst g.fst = 0
h✝ : dist f.snd g.snd = 0
⊢ 0 ≤ 1 + 0

case neg
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f g : WithLp p (α × β)
h : 1 ≤ p.toReal
hp' : p = 0
h✝¹ : ¬dist f.fst g.fst = 0
h✝ : ¬dist f.snd g.snd = 0
⊢ 0 ≤ 1 + 1

case pos
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f g : WithLp p (α × β)
h : 1 ≤ p.toReal
hp' : ¬p = 0
h✝ : p = ∞
⊢ 0 ≤ max (dist f.fst g.fst) (dist f.snd g.snd)

case neg
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f g : WithLp p (α × β)
h : 1 ≤ p.toReal
hp' : ¬p = 0
h✝ : ¬p = ∞
⊢ 0 ≤ (dist f.fst g.fst ^ p.toReal + dist f.snd g.snd ^ p.toReal) ^ p.toReal⁻¹
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: case h₁
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : WithLp p (α × β)
h : 1 ≤ p.toReal
pos : 0 < p.toReal
nonneg : 0 ≤ 1 / p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ edist x.fst y.fst ≤ edist x.ofLp y.ofLp

pp: case h₁
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : WithLp p (α × β)
h : 1 ≤ p.toReal
pos : 0 < p.toReal
nonneg : 0 ≤ 1 / p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ edist x.snd y.snd ≤ edist x.ofLp y.ofLp

Tactic:
<;>

Goal state after:
case h₁
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : WithLp p (α × β)
h : 1 ≤ p.toReal
pos : 0 < p.toReal
nonneg : 0 ≤ 1 / p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ edist x.fst y.fst ≤ edist x.ofLp y.ofLp

case h₁
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : WithLp p (α × β)
h : 1 ≤ p.toReal
pos : 0 < p.toReal
nonneg : 0 ≤ 1 / p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ edist x.snd y.snd ≤ edist x.ofLp y.ofLp
Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

Goal state before:
pp: case mp.refine_2.inl
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
he'' : e ∉ v
h_end : ∀ a ∈ v, ⟪a, e⟫_𝕜 = 0
a : E
ha' : a ∈ insert e v
ha : a = e
b : E
hb' : b ∈ insert e v
hab' : ⟨a, ha'⟩ ≠ ⟨b, hb'⟩
⊢ ⟪↑⟨a, ha'⟩, ↑⟨b, hb'⟩⟫_𝕜 = 0

Tactic:
have hb : b ∈ v := by grind

Goal state after:
case mp.refine_2.inl
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
x : E
hx' : x ∈ (span 𝕜 v)ᗮ
hx : x ≠ 0
e : E := (↑‖x‖)⁻¹ • x
he : ‖e‖ = 1
he' : e ∈ (span 𝕜 v)ᗮ
he'' : e ∉ v
h_end : ∀ a ∈ v, ⟪a, e⟫_𝕜 = 0
a : E
ha' : a ∈ insert e v
ha : a = e
b : E
hb' : b ∈ insert e v
hab' : ⟨a, ha'⟩ ≠ ⟨b, hb'⟩
hb : b ∈ v
⊢ ⟪↑⟨a, ha'⟩, ↑⟨b, hb'⟩⟫_𝕜 = 0
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x : WithLp p (α × β)
⊢ ‖x.fst‖ ≤ ‖x‖

Tactic:
simpa using dist_fst_le x 0

Goal state after:
Module: Mathlib.LinearAlgebra.UnitaryGroup

Goal state before:
pp: case left
n : Type u
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
R : Type u_1
m : Type u_2
inst✝³ : Semiring R
inst✝² : StarRing R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
U₁ : Matrix n n R
U₂ : Matrix m m R
hU₁ : U₁ ∈ unitary (Matrix n n R)
hU₂ : U₂ ∈ unitary (Matrix m m R)
⊢ (kroneckerMap (fun x1 x2 ↦ x1 * x2) U₂ᴴ U₁ᴴ).submatrix Prod.swap Prod.swap *
      kroneckerMap (fun x1 x2 ↦ x1 * x2) U₁ U₂ =
    1

pp: case right
n : Type u
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
R : Type u_1
m : Type u_2
inst✝³ : Semiring R
inst✝² : StarRing R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
U₁ : Matrix n n R
U₂ : Matrix m m R
hU₁ : U₁ ∈ unitary (Matrix n n R)
hU₂ : U₂ ∈ unitary (Matrix m m R)
⊢ kroneckerMap (fun x1 x2 ↦ x1 * x2) U₁ U₂ *
      (kroneckerMap (fun x1 x2 ↦ x1 * x2) U₂ᴴ U₁ᴴ).submatrix Prod.swap Prod.swap =
    1

Tactic:
<;>

Goal state after:
case left
n : Type u
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
R : Type u_1
m : Type u_2
inst✝³ : Semiring R
inst✝² : StarRing R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
U₁ : Matrix n n R
U₂ : Matrix m m R
hU₁ : U₁ ∈ unitary (Matrix n n R)
hU₂ : U₂ ∈ unitary (Matrix m m R)
⊢ (kroneckerMap (fun x1 x2 ↦ x1 * x2) U₂ᴴ U₁ᴴ).submatrix Prod.swap Prod.swap *
      kroneckerMap (fun x1 x2 ↦ x1 * x2) U₁ U₂ =
    1

case right
n : Type u
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
R : Type u_1
m : Type u_2
inst✝³ : Semiring R
inst✝² : StarRing R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
U₁ : Matrix n n R
U₂ : Matrix m m R
hU₁ : U₁ ∈ unitary (Matrix n n R)
hU₂ : U₂ ∈ unitary (Matrix m m R)
⊢ kroneckerMap (fun x1 x2 ↦ x1 * x2) U₁ U₂ *
      (kroneckerMap (fun x1 x2 ↦ x1 * x2) U₂ᴴ U₁ᴴ).submatrix Prod.swap Prod.swap =
    1
Module: Mathlib.LinearAlgebra.UnitaryGroup

Goal state before:
pp: case left
n : Type u
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
R : Type u_1
m : Type u_2
inst✝³ : Semiring R
inst✝² : StarRing R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
U₁ : Matrix n n R
U₂ : Matrix m m R
hU₁ : U₁ ∈ unitary (Matrix n n R)
hU₂ : U₂ ∈ unitary (Matrix m m R)
i✝ j✝ : n × m
⊢ ((kroneckerMap (fun x1 x2 ↦ x1 * x2) U₂ᴴ U₁ᴴ).submatrix Prod.swap Prod.swap *
        kroneckerMap (fun x1 x2 ↦ x1 * x2) U₁ U₂)
      i✝ j✝ =
    1 i✝ j✝

pp: case right
n : Type u
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
R : Type u_1
m : Type u_2
inst✝³ : Semiring R
inst✝² : StarRing R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
U₁ : Matrix n n R
U₂ : Matrix m m R
hU₁ : U₁ ∈ unitary (Matrix n n R)
hU₂ : U₂ ∈ unitary (Matrix m m R)
i✝ j✝ : n × m
⊢ (kroneckerMap (fun x1 x2 ↦ x1 * x2) U₁ U₂ *
        (kroneckerMap (fun x1 x2 ↦ x1 * x2) U₂ᴴ U₁ᴴ).submatrix Prod.swap Prod.swap)
      i✝ j✝ =
    1 i✝ j✝

Tactic:
<;>

Goal state after:
case left
n : Type u
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
R : Type u_1
m : Type u_2
inst✝³ : Semiring R
inst✝² : StarRing R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
U₁ : Matrix n n R
U₂ : Matrix m m R
hU₁ : U₁ ∈ unitary (Matrix n n R)
hU₂ : U₂ ∈ unitary (Matrix m m R)
i✝ j✝ : n × m
⊢ ((kroneckerMap (fun x1 x2 ↦ x1 * x2) U₂ᴴ U₁ᴴ).submatrix Prod.swap Prod.swap *
        kroneckerMap (fun x1 x2 ↦ x1 * x2) U₁ U₂)
      i✝ j✝ =
    1 i✝ j✝

case right
n : Type u
inst✝⁵ : DecidableEq n
inst✝⁴ : Fintype n
R : Type u_1
m : Type u_2
inst✝³ : Semiring R
inst✝² : StarRing R
inst✝¹ : Fintype m
inst✝ : DecidableEq m
U₁ : Matrix n n R
U₂ : Matrix m m R
hU₁ : U₁ ∈ unitary (Matrix n n R)
hU₂ : U₂ ∈ unitary (Matrix m m R)
i✝ j✝ : n × m
⊢ (kroneckerMap (fun x1 x2 ↦ x1 * x2) U₁ U₂ *
        (kroneckerMap (fun x1 x2 ↦ x1 * x2) U₂ᴴ U₁ᴴ).submatrix Prod.swap Prod.swap)
      i✝ j✝ =
    1 i✝ j✝
Module: Mathlib.Analysis.Normed.Lp.PiLp

Goal state before:
pp: ι : Type u_2
β : ι → Type u_4
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddCommGroup (β i)
p : ℝ≥0∞
i : ι
a b : β i
⊢ toLp p (Pi.single i a - Pi.single i b) = toLp p (Pi.single i a) - toLp p (Pi.single i b)

Tactic:
toLp_sub

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: case h₁
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp✝ : Fact (1 ≤ p)
inst✝⁶ : SeminormedAddCommGroup α
inst✝⁵ : SeminormedAddCommGroup β
inst✝⁴ : SeminormedRing 𝕜
inst✝³ : Module 𝕜 α
inst✝² : Module 𝕜 β
inst✝¹ : IsBoundedSMul 𝕜 α
inst✝ : IsBoundedSMul 𝕜 β
c : 𝕜
f : WithLp p (α × β)
hp : 1 ≤ p.toReal
hp0 : 0 < p.toReal
hpt : p ≠ ∞
⊢ ‖(c • f).fst‖₊ ≤ ‖c‖₊ * ‖f.fst‖₊

pp: case h₁
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp✝ : Fact (1 ≤ p)
inst✝⁶ : SeminormedAddCommGroup α
inst✝⁵ : SeminormedAddCommGroup β
inst✝⁴ : SeminormedRing 𝕜
inst✝³ : Module 𝕜 α
inst✝² : Module 𝕜 β
inst✝¹ : IsBoundedSMul 𝕜 α
inst✝ : IsBoundedSMul 𝕜 β
c : 𝕜
f : WithLp p (α × β)
hp : 1 ≤ p.toReal
hp0 : 0 < p.toReal
hpt : p ≠ ∞
⊢ ‖(c • f).snd‖₊ ≤ ‖c‖₊ * ‖f.snd‖₊

Tactic:
<;>

Goal state after:
case h₁
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp✝ : Fact (1 ≤ p)
inst✝⁶ : SeminormedAddCommGroup α
inst✝⁵ : SeminormedAddCommGroup β
inst✝⁴ : SeminormedRing 𝕜
inst✝³ : Module 𝕜 α
inst✝² : Module 𝕜 β
inst✝¹ : IsBoundedSMul 𝕜 α
inst✝ : IsBoundedSMul 𝕜 β
c : 𝕜
f : WithLp p (α × β)
hp : 1 ≤ p.toReal
hp0 : 0 < p.toReal
hpt : p ≠ ∞
⊢ ‖(c • f).fst‖₊ ≤ ‖c‖₊ * ‖f.fst‖₊

case h₁
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp✝ : Fact (1 ≤ p)
inst✝⁶ : SeminormedAddCommGroup α
inst✝⁵ : SeminormedAddCommGroup β
inst✝⁴ : SeminormedRing 𝕜
inst✝³ : Module 𝕜 α
inst✝² : Module 𝕜 β
inst✝¹ : IsBoundedSMul 𝕜 α
inst✝ : IsBoundedSMul 𝕜 β
c : 𝕜
f : WithLp p (α × β)
hp : 1 ≤ p.toReal
hp0 : 0 < p.toReal
hpt : p ≠ ∞
⊢ ‖(c • f).snd‖₊ ≤ ‖c‖₊ * ‖f.snd‖₊