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

Goal state before:
pp: case of.inl
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝¹ : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i ↦ ↥(V i)) fun i ↦ (V i).subtypeₗᵢ
i : ι
inst✝ : CompleteSpace ↥(V i)
x : ↥(V i)
⊢ (V i).orthogonalProjectionOnto ↑x = (DFinsupp.single i x) i

pp: case of.inr
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝¹ : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i ↦ ↥(V i)) fun i ↦ (V i).subtypeₗᵢ
i : ι
inst✝ : CompleteSpace ↥(V i)
j : ι
x : ↥(V j)
hij : i ≠ j
⊢ (V i).orthogonalProjectionOnto ↑x = (DFinsupp.single j x) i

Tactic:
·

Goal state after:
case of.inl
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝¹ : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i ↦ ↥(V i)) fun i ↦ (V i).subtypeₗᵢ
i : ι
inst✝ : CompleteSpace ↥(V i)
x : ↥(V i)
⊢ (V i).orthogonalProjectionOnto ↑x = (DFinsupp.single i x) i
Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

Goal state before:
pp: case of.inr
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝¹ : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i ↦ ↥(V i)) fun i ↦ (V i).subtypeₗᵢ
i : ι
inst✝ : CompleteSpace ↥(V i)
j : ι
x : ↥(V j)
hij : i ≠ j
⊢ (V i).orthogonalProjectionOnto ↑x = (DFinsupp.single j x) i

Tactic:
·

Goal state after:
case of.inr
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
ι : Type u_4
inst✝¹ : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : OrthogonalFamily 𝕜 (fun i ↦ ↥(V i)) fun i ↦ (V i).subtypeₗᵢ
i : ι
inst✝ : CompleteSpace ↥(V i)
j : ι
x : ↥(V j)
hij : i ≠ j
⊢ (V i).orthogonalProjectionOnto ↑x = (DFinsupp.single j x) i
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: case inl
α : Type u_2
β : Type u_3
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
hp : Fact (1 ≤ ∞)
x y : WithLp ∞ (α × β)
⊢ edist x.fst y.fst ≤ edist x y ∧ edist x.snd y.snd ≤ edist x y

pp: case inr
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : WithLp p (α × β)
h : 1 ≤ p.toReal
⊢ edist x.fst y.fst ≤ edist x y ∧ edist x.snd y.snd ≤ edist x y

Tactic:
·

Goal state after:
case inl
α : Type u_2
β : Type u_3
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
hp : Fact (1 ≤ ∞)
x y : WithLp ∞ (α × β)
⊢ edist x.fst y.fst ≤ edist x y ∧ edist x.snd y.snd ≤ edist x y
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: case inr
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : WithLp p (α × β)
h : 1 ≤ p.toReal
⊢ edist x.fst y.fst ≤ edist x y ∧ edist x.snd y.snd ≤ edist x y

Tactic:
·

Goal state after:
case inr
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : WithLp p (α × β)
h : 1 ≤ p.toReal
⊢ edist x.fst y.fst ≤ edist x y ∧ edist x.snd y.snd ≤ edist x y
Module: Mathlib.Analysis.Normed.Lp.ProdLp

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

pp: case inr.right
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : WithLp p (α × β)
h : 1 ≤ p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ edist x.snd y.snd ≤ (edist x.fst y.fst ^ p.toReal + edist x.snd y.snd ^ p.toReal) ^ (1 / p.toReal)

Tactic:
·

Goal state after:
case inr.left
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : WithLp p (α × β)
h : 1 ≤ p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ edist x.fst y.fst ≤ (edist x.fst y.fst ^ p.toReal + edist x.snd y.snd ^ p.toReal) ^ (1 / p.toReal)
Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
ι : Type u_4
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
V : ι → Submodule 𝕜 E
inst✝ : ∀ (i : ι), CompleteSpace ↥(V i)
hV : OrthogonalFamily 𝕜 (fun i ↦ ↥(V i)) fun i ↦ (V i).subtypeₗᵢ
h : iSup V = ⊤
x : E
this : (i : ι) → DecidableEq ↥(V i) := fun i ↦ Classical.decEq ↥(V i)
⊢ ∑ i,
      (AddSubmonoidClass.subtype (V i))
        (DFinsupp.equivFunOnFintype (DFinsupp.equivFunOnFintype.symm fun i ↦ (V i).orthogonalProjectionOnto x) i) =
    x

pp: case hf
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
ι : Type u_4
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
V : ι → Submodule 𝕜 E
inst✝ : ∀ (i : ι), CompleteSpace ↥(V i)
hV : OrthogonalFamily 𝕜 (fun i ↦ ↥(V i)) fun i ↦ (V i).subtypeₗᵢ
h : iSup V = ⊤
x : E
this : (i : ι) → DecidableEq ↥(V i) := fun i ↦ Classical.decEq ↥(V i)
⊢ ∀ (i : ι), (AddSubmonoidClass.subtype (V i)) 0 = 0

Tactic:
·

Goal state after:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
ι : Type u_4
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
V : ι → Submodule 𝕜 E
inst✝ : ∀ (i : ι), CompleteSpace ↥(V i)
hV : OrthogonalFamily 𝕜 (fun i ↦ ↥(V i)) fun i ↦ (V i).subtypeₗᵢ
h : iSup V = ⊤
x : E
this : (i : ι) → DecidableEq ↥(V i) := fun i ↦ Classical.decEq ↥(V i)
⊢ ∑ i,
      (AddSubmonoidClass.subtype (V i))
        (DFinsupp.equivFunOnFintype (DFinsupp.equivFunOnFintype.symm fun i ↦ (V i).orthogonalProjectionOnto x) i) =
    x
Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

Goal state before:
pp: case hf
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
ι : Type u_4
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
V : ι → Submodule 𝕜 E
inst✝ : ∀ (i : ι), CompleteSpace ↥(V i)
hV : OrthogonalFamily 𝕜 (fun i ↦ ↥(V i)) fun i ↦ (V i).subtypeₗᵢ
h : iSup V = ⊤
x : E
this : (i : ι) → DecidableEq ↥(V i) := fun i ↦ Classical.decEq ↥(V i)
⊢ ∀ (i : ι), (AddSubmonoidClass.subtype (V i)) 0 = 0

Tactic:
·

Goal state after:
case hf
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
ι : Type u_4
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
V : ι → Submodule 𝕜 E
inst✝ : ∀ (i : ι), CompleteSpace ↥(V i)
hV : OrthogonalFamily 𝕜 (fun i ↦ ↥(V i)) fun i ↦ (V i).subtypeₗᵢ
h : iSup V = ⊤
x : E
this : (i : ι) → DecidableEq ↥(V i) := fun i ↦ Classical.decEq ↥(V i)
⊢ ∀ (i : ι), (AddSubmonoidClass.subtype (V i)) 0 = 0
Module: Mathlib.Analysis.Normed.Lp.ProdLp

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

Tactic:
·

Goal state after:
case inr.right
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : WithLp p (α × β)
h : 1 ≤ p.toReal
cancel : p.toReal * (1 / p.toReal) = 1
⊢ edist x.snd y.snd ≤ (edist x.fst y.fst ^ p.toReal + edist x.snd y.snd ^ p.toReal) ^ (1 / p.toReal)
Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

Goal state before:
pp: case mp
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
⊢ (∀ u ⊇ v, Orthonormal 𝕜 Subtype.val → u = v) → ∀ x ∈ (span 𝕜 v)ᗮ, x = 0

pp: case mpr
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
⊢ (∀ x ∈ (span 𝕜 v)ᗮ, x = 0) → ∀ u ⊇ v, Orthonormal 𝕜 Subtype.val → u = v

Tactic:
·

Goal state after:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
⊢ (∀ u ⊇ v, Orthonormal 𝕜 Subtype.val → u = v) → ∀ x ∈ (span 𝕜 v)ᗮ, x = 0
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: case inl
α : Type u_2
β : Type u_3
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
hp : Fact (1 ≤ ∞)
x y : WithLp ∞ (α × β)
⊢ edist x y ≤ ↑(2 ^ (1 / ∞).toReal) * edist x.ofLp y.ofLp

pp: case inr
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : WithLp p (α × β)
h : 1 ≤ p.toReal
⊢ edist x y ≤ ↑(2 ^ (1 / p).toReal) * edist x.ofLp y.ofLp

Tactic:
·

Goal state after:
case inl
α : Type u_2
β : Type u_3
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
hp : Fact (1 ≤ ∞)
x y : WithLp ∞ (α × β)
⊢ edist x y ≤ ↑(2 ^ (1 / ∞).toReal) * edist x.ofLp y.ofLp
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: case inr
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : WithLp p (α × β)
h : 1 ≤ p.toReal
⊢ edist x y ≤ ↑(2 ^ (1 / p).toReal) * edist x.ofLp y.ofLp

Tactic:
·

Goal state after:
case inr
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x y : WithLp p (α × β)
h : 1 ≤ p.toReal
⊢ edist x y ≤ ↑(2 ^ (1 / p).toReal) * edist x.ofLp y.ofLp
Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

Goal state before:
pp: case mp.refine_1
𝕜 : 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
⊢ ∀ (i : { x // x ∈ insert e v }), ‖↑i‖ = 1

pp: case mp.refine_2
𝕜 : 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
⊢ Pairwise fun i j ↦ ⟪↑i, ↑j⟫_𝕜 = 0

Tactic:
·

Goal state after:
case mp.refine_1
𝕜 : 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
⊢ ∀ (i : { x // x ∈ insert e v }), ‖↑i‖ = 1
Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

Goal state before:
pp: case mp.refine_1.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
a : E
ha' : a ∈ insert e v
ha : a = e
⊢ ‖↑⟨a, ha'⟩‖ = 1

pp: case mp.refine_1.inr
𝕜 : 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
a : E
ha' : a ∈ insert e v
ha : a ∈ v
⊢ ‖↑⟨a, ha'⟩‖ = 1

Tactic:
·

Goal state after:
case mp.refine_1.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
a : E
ha' : a ∈ insert e v
ha : a = e
⊢ ‖↑⟨a, ha'⟩‖ = 1
Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

Goal state before:
pp: case mp.refine_1.inr
𝕜 : 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
a : E
ha' : a ∈ insert e v
ha : a ∈ v
⊢ ‖↑⟨a, ha'⟩‖ = 1

Tactic:
·

Goal state after:
case mp.refine_1.inr
𝕜 : 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
a : E
ha' : a ∈ insert e v
ha : a ∈ v
⊢ ‖↑⟨a, ha'⟩‖ = 1
Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

Goal state before:
pp: case mp.refine_2
𝕜 : 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
⊢ Pairwise fun i j ↦ ⟪↑i, ↑j⟫_𝕜 = 0

Tactic:
·

Goal state after:
case mp.refine_2
𝕜 : 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
⊢ Pairwise fun i j ↦ ⟪↑i, ↑j⟫_𝕜 = 0
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: case inl
𝕜 : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
hp : Fact (1 ≤ ∞)
x y : WithLp ∞ (α × β)
⊢ dist x y = ‖-x + y‖

pp: case inr
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x y : WithLp p (α × β)
h : 1 ≤ p.toReal
⊢ dist x y = ‖-x + y‖

Tactic:
·

Goal state after:
case inl
𝕜 : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
hp : Fact (1 ≤ ∞)
x y : WithLp ∞ (α × β)
⊢ dist x y = ‖-x + y‖
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
⊢ ∀ ⦃j : { x // x ∈ insert e v }⦄, ⟨a, ha'⟩ ≠ j → (fun i j ↦ ⟪↑i, ↑j⟫_𝕜 = 0) ⟨a, ha'⟩ j

pp: case mp.refine_2.inr
𝕜 : 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 ∈ v
⊢ ∀ ⦃j : { x // x ∈ insert e v }⦄, ⟨a, ha'⟩ ≠ j → (fun i j ↦ ⟪↑i, ↑j⟫_𝕜 = 0) ⟨a, ha'⟩ j

Tactic:
·

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
⊢ ∀ ⦃j : { x // x ∈ insert e v }⦄, ⟨a, ha'⟩ ≠ j → (fun i j ↦ ⟪↑i, ↑j⟫_𝕜 = 0) ⟨a, ha'⟩ j
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: case inr
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x y : WithLp p (α × β)
h : 1 ≤ p.toReal
⊢ dist x y = ‖-x + y‖

Tactic:
·

Goal state after:
case inr
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
hp : Fact (1 ≤ p)
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x y : WithLp p (α × β)
h : 1 ≤ p.toReal
⊢ dist x y = ‖-x + y‖
Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

Goal state before:
pp: case mp.refine_2.inr.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 ∈ v
b : E
hb' : b ∈ insert e v
hab' : ⟨a, ha'⟩ ≠ ⟨b, hb'⟩
hb : b = e
⊢ ⟪↑⟨a, ha'⟩, ↑⟨b, hb'⟩⟫_𝕜 = 0

pp: case mp.refine_2.inr.inr
𝕜 : 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 ∈ v
b : E
hb' : b ∈ insert e v
hab' : ⟨a, ha'⟩ ≠ ⟨b, hb'⟩
hb : b ∈ v
⊢ ⟪↑⟨a, ha'⟩, ↑⟨b, hb'⟩⟫_𝕜 = 0

Tactic:
·

Goal state after:
case mp.refine_2.inr.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 ∈ v
b : E
hb' : b ∈ insert e v
hab' : ⟨a, ha'⟩ ≠ ⟨b, hb'⟩
hb : b = e
⊢ ⟪↑⟨a, ha'⟩, ↑⟨b, hb'⟩⟫_𝕜 = 0
Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

Goal state before:
pp: case mpr
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
⊢ (∀ x ∈ (span 𝕜 v)ᗮ, x = 0) → ∀ u ⊇ v, Orthonormal 𝕜 Subtype.val → u = v

Tactic:
·

Goal state after:
case mpr
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
v : Set E
hv : Orthonormal 𝕜 Subtype.val
⊢ (∀ x ∈ (span 𝕜 v)ᗮ, x = 0) → ∀ u ⊇ v, Orthonormal 𝕜 Subtype.val → u = v
Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

Goal state before:
pp: case mp
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
v : Set E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
hv_coe : Set.range Subtype.val = v
⊢ span 𝕜 v = ⊤ → ∃ b, ⇑b = Subtype.val

pp: case mpr
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
v : Set E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
hv_coe : Set.range Subtype.val = v
⊢ (∃ b, ⇑b = Subtype.val) → span 𝕜 v = ⊤

Tactic:
·

Goal state after:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
v : Set E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
hv_coe : Set.range Subtype.val = v
⊢ span 𝕜 v = ⊤ → ∃ b, ⇑b = Subtype.val
Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

Goal state before:
pp: case mpr
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
v : Set E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
hv_coe : Set.range Subtype.val = v
⊢ (∃ b, ⇑b = Subtype.val) → span 𝕜 v = ⊤

Tactic:
·

Goal state after:
case mpr
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
v : Set E
inst✝ : FiniteDimensional 𝕜 E
hv : Orthonormal 𝕜 Subtype.val
hv_coe : Set.range Subtype.val = v
⊢ (∃ b, ⇑b = Subtype.val) → span 𝕜 v = ⊤
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: case inl
𝕜 : Type u_1
α : Type u_2
β : Type u_3
inst✝⁶ : SeminormedAddCommGroup α
inst✝⁵ : SeminormedAddCommGroup β
inst✝⁴ : SeminormedRing 𝕜
inst✝³ : Module 𝕜 α
inst✝² : Module 𝕜 β
inst✝¹ : IsBoundedSMul 𝕜 α
inst✝ : IsBoundedSMul 𝕜 β
c : 𝕜
hp : Fact (1 ≤ ∞)
f : WithLp ∞ (α × β)
⊢ ‖c • f‖₊ ≤ ‖c‖₊ * ‖f‖₊

pp: case inr
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
⊢ ‖c • f‖₊ ≤ ‖c‖₊ * ‖f‖₊

Tactic:
·

Goal state after:
case inl
𝕜 : Type u_1
α : Type u_2
β : Type u_3
inst✝⁶ : SeminormedAddCommGroup α
inst✝⁵ : SeminormedAddCommGroup β
inst✝⁴ : SeminormedRing 𝕜
inst✝³ : Module 𝕜 α
inst✝² : Module 𝕜 β
inst✝¹ : IsBoundedSMul 𝕜 α
inst✝ : IsBoundedSMul 𝕜 β
c : 𝕜
hp : Fact (1 ≤ ∞)
f : WithLp ∞ (α × β)
⊢ ‖c • f‖₊ ≤ ‖c‖₊ * ‖f‖₊
Module: Mathlib.Data.Matrix.Reflection

Goal state before:
pp: case refine_1
α : Type u_1
m n : ℕ
A : Matrix (Fin m) (Fin (n + 1)) α
i : Fin (n + 1)
j : Fin m
⊢ of (vecCons (FinVec.map (fun v ↦ v 0) A) (A.submatrix id Fin.succ)ᵀ) 0 j = Aᵀ 0 j

pp: case refine_2
α : Type u_1
m n : ℕ
A : Matrix (Fin m) (Fin (n + 1)) α
i✝ : Fin (n + 1)
j : Fin m
i : Fin n
⊢ of (vecCons (FinVec.map (fun v ↦ v 0) A) (A.submatrix id Fin.succ)ᵀ) i.succ j = Aᵀ i.succ j

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
m n : ℕ
A : Matrix (Fin m) (Fin (n + 1)) α
i : Fin (n + 1)
j : Fin m
⊢ of (vecCons (FinVec.map (fun v ↦ v 0) A) (A.submatrix id Fin.succ)ᵀ) 0 j = Aᵀ 0 j
Module: Mathlib.Data.Matrix.Reflection

Goal state before:
pp: case refine_2
α : Type u_1
m n : ℕ
A : Matrix (Fin m) (Fin (n + 1)) α
i✝ : Fin (n + 1)
j : Fin m
i : Fin n
⊢ of (vecCons (FinVec.map (fun v ↦ v 0) A) (A.submatrix id Fin.succ)ᵀ) i.succ j = Aᵀ i.succ j

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
m n : ℕ
A : Matrix (Fin m) (Fin (n + 1)) α
i✝ : Fin (n + 1)
j : Fin m
i : Fin n
⊢ of (vecCons (FinVec.map (fun v ↦ v 0) A) (A.submatrix id Fin.succ)ᵀ) i.succ j = Aᵀ i.succ j
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: case inr
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
⊢ ‖c • f‖₊ ≤ ‖c‖₊ * ‖f‖₊

Tactic:
·

Goal state after:
case inr
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
⊢ ‖c • f‖₊ ≤ ‖c‖₊ * ‖f‖₊
Module: Mathlib.LinearAlgebra.UnitaryGroup

Goal state before:
pp: case left
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A : Matrix n n α
hA : A ∈ unitaryGroup n α
⊢ star A.det * A.det = 1

pp: case right
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A : Matrix n n α
hA : A ∈ unitaryGroup n α
⊢ A.det * star A.det = 1

Tactic:
·

Goal state after:
case left
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A : Matrix n n α
hA : A ∈ unitaryGroup n α
⊢ star A.det * A.det = 1
Module: Mathlib.LinearAlgebra.UnitaryGroup

Goal state before:
pp: case right
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A : Matrix n n α
hA : A ∈ unitaryGroup n α
⊢ A.det * star A.det = 1

Tactic:
·

Goal state after:
case right
n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
α : Type v
inst✝¹ : CommRing α
inst✝ : StarRing α
A : Matrix n n α
hA : A ∈ unitaryGroup n α
⊢ A.det * star A.det = 1