[GOAL]
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalAddGroup E
inst✝³ : T2Space E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
r : ℝ
⊢ closedBall x r = ↑(ContinuousLinearEquiv.symm toEuclidean) '' Metric.closedBall (↑toEuclidean x) r
[PROOFSTEP]
rw [toEuclidean.image_symm_eq_preimage, closedBall_eq_preimage]
[GOAL]
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalAddGroup E
inst✝³ : T2Space E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
r : ℝ
⊢ IsCompact (closedBall x r)
[PROOFSTEP]
rw [closedBall_eq_image]
[GOAL]
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalAddGroup E
inst✝³ : T2Space E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
r : ℝ
⊢ IsCompact (↑(ContinuousLinearEquiv.symm toEuclidean) '' Metric.closedBall (↑toEuclidean x) r)
[PROOFSTEP]
exact (isCompact_closedBall _ _).image toEuclidean.symm.continuous
[GOAL]
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalAddGroup E
inst✝³ : T2Space E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
r : ℝ
h : r ≠ 0
⊢ closure (ball x r) = closedBall x r
[PROOFSTEP]
rw [ball_eq_preimage, ← toEuclidean.preimage_closure, closure_ball (toEuclidean x) h, closedBall_eq_preimage]
[GOAL]
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalAddGroup E
inst✝³ : T2Space E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : FiniteDimensional ℝ E
R : ℝ
s : Set E
x : E
hR : 0 < R
hs : IsClosed s
h : s ⊆ ball x R
⊢ ∃ r, r ∈ Ioo 0 R ∧ s ⊆ ball x r
[PROOFSTEP]
rw [ball_eq_preimage, ← image_subset_iff] at h
[GOAL]
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalAddGroup E
inst✝³ : T2Space E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : FiniteDimensional ℝ E
R : ℝ
s : Set E
x : E
hR : 0 < R
hs : IsClosed s
h : ↑toEuclidean '' s ⊆ Metric.ball (↑toEuclidean x) R
⊢ ∃ r, r ∈ Ioo 0 R ∧ s ⊆ ball x r
[PROOFSTEP]
rcases exists_pos_lt_subset_ball hR (toEuclidean.isClosed_image.2 hs) h with ⟨r, hr, hsr⟩
[GOAL]
case intro.intro
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalAddGroup E
inst✝³ : T2Space E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : FiniteDimensional ℝ E
R : ℝ
s : Set E
x : E
hR : 0 < R
hs : IsClosed s
h : ↑toEuclidean '' s ⊆ Metric.ball (↑toEuclidean x) R
r : ℝ
hr : r ∈ Ioo 0 R
hsr : ↑toEuclidean '' s ⊆ Metric.ball (↑toEuclidean x) r
⊢ ∃ r, r ∈ Ioo 0 R ∧ s ⊆ ball x r
[PROOFSTEP]
exact ⟨r, hr, image_subset_iff.1 hsr⟩
[GOAL]
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalAddGroup E
inst✝³ : T2Space E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
⊢ Filter.HasBasis (𝓝 x) (fun r => 0 < r) (closedBall x)
[PROOFSTEP]
rw [toEuclidean.toHomeomorph.nhds_eq_comap x]
[GOAL]
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalAddGroup E
inst✝³ : T2Space E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
⊢ Filter.HasBasis
    (Filter.comap (↑(ContinuousLinearEquiv.toHomeomorph toEuclidean))
      (𝓝 (↑(ContinuousLinearEquiv.toHomeomorph toEuclidean) x)))
    (fun r => 0 < r) (closedBall x)
[PROOFSTEP]
exact Metric.nhds_basis_closedBall.comap _
[GOAL]
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalAddGroup E
inst✝³ : T2Space E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
⊢ Filter.HasBasis (𝓝 x) (fun r => 0 < r) (ball x)
[PROOFSTEP]
rw [toEuclidean.toHomeomorph.nhds_eq_comap x]
[GOAL]
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalAddGroup E
inst✝³ : T2Space E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : FiniteDimensional ℝ E
x : E
⊢ Filter.HasBasis
    (Filter.comap (↑(ContinuousLinearEquiv.toHomeomorph toEuclidean))
      (𝓝 (↑(ContinuousLinearEquiv.toHomeomorph toEuclidean) x)))
    (fun r => 0 < r) (ball x)
[PROOFSTEP]
exact Metric.nhds_basis_ball.comap _
[GOAL]
E : Type u_1
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : TopologicalAddGroup E
inst✝⁸ : T2Space E
inst✝⁷ : Module ℝ E
inst✝⁶ : ContinuousSMul ℝ E
inst✝⁵ : FiniteDimensional ℝ E
F : Type u_2
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
inst✝ : FiniteDimensional ℝ G
f g : F → G
n : ℕ∞
hf : ContDiff ℝ n f
hg : ContDiff ℝ n g
h : ∀ (x : F), f x ≠ g x
⊢ ContDiff ℝ n fun x => Euclidean.dist (f x) (g x)
[PROOFSTEP]
simp only [Euclidean.dist]
[GOAL]
E : Type u_1
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : TopologicalAddGroup E
inst✝⁸ : T2Space E
inst✝⁷ : Module ℝ E
inst✝⁶ : ContinuousSMul ℝ E
inst✝⁵ : FiniteDimensional ℝ E
F : Type u_2
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
inst✝ : FiniteDimensional ℝ G
f g : F → G
n : ℕ∞
hf : ContDiff ℝ n f
hg : ContDiff ℝ n g
h : ∀ (x : F), f x ≠ g x
⊢ ContDiff ℝ n fun x => Dist.dist (↑toEuclidean (f x)) (↑toEuclidean (g x))
[PROOFSTEP]
apply @ContDiff.dist ℝ
[GOAL]
case hf
E : Type u_1
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : TopologicalAddGroup E
inst✝⁸ : T2Space E
inst✝⁷ : Module ℝ E
inst✝⁶ : ContinuousSMul ℝ E
inst✝⁵ : FiniteDimensional ℝ E
F : Type u_2
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
inst✝ : FiniteDimensional ℝ G
f g : F → G
n : ℕ∞
hf : ContDiff ℝ n f
hg : ContDiff ℝ n g
h : ∀ (x : F), f x ≠ g x
⊢ ContDiff ℝ n fun y => ↑toEuclidean (f y)
case hg
E : Type u_1
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : TopologicalAddGroup E
inst✝⁸ : T2Space E
inst✝⁷ : Module ℝ E
inst✝⁶ : ContinuousSMul ℝ E
inst✝⁵ : FiniteDimensional ℝ E
F : Type u_2
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
inst✝ : FiniteDimensional ℝ G
f g : F → G
n : ℕ∞
hf : ContDiff ℝ n f
hg : ContDiff ℝ n g
h : ∀ (x : F), f x ≠ g x
⊢ ContDiff ℝ n fun y => ↑toEuclidean (g y)
case hne
E : Type u_1
inst✝¹¹ : AddCommGroup E
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : TopologicalAddGroup E
inst✝⁸ : T2Space E
inst✝⁷ : Module ℝ E
inst✝⁶ : ContinuousSMul ℝ E
inst✝⁵ : FiniteDimensional ℝ E
F : Type u_2
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
G : Type u_3
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
inst✝ : FiniteDimensional ℝ G
f g : F → G
n : ℕ∞
hf : ContDiff ℝ n f
hg : ContDiff ℝ n g
h : ∀ (x : F), f x ≠ g x
⊢ ∀ (x : F), ↑toEuclidean (f x) ≠ ↑toEuclidean (g x)
[PROOFSTEP]
exacts [(@toEuclidean G _ _ _ _ _ _ _).contDiff.comp hf, (@toEuclidean G _ _ _ _ _ _ _).contDiff.comp hg, fun x =>
  toEuclidean.injective.ne (h x)]


[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
T : E →L[𝕜] E
hT : IsPositive T
x : E
⊢ 0 ≤ ↑re (inner x (↑T x))
[PROOFSTEP]
rw [inner_re_symm]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
T : E →L[𝕜] E
hT : IsPositive T
x : E
⊢ 0 ≤ ↑re (inner (↑T x) x)
[PROOFSTEP]
exact hT.inner_nonneg_left x
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
⊢ IsPositive 0
[PROOFSTEP]
refine' ⟨isSelfAdjoint_zero _, fun x => _⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
x : E
⊢ 0 ≤ reApplyInnerSelf 0 x
[PROOFSTEP]
change 0 ≤ re ⟪_, _⟫
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
x : E
⊢ 0 ≤ ↑re (inner (↑0 x) x)
[PROOFSTEP]
rw [zero_apply, inner_zero_left, ZeroHomClass.map_zero]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
T S : E →L[𝕜] E
hT : IsPositive T
hS : IsPositive S
⊢ IsPositive (T + S)
[PROOFSTEP]
refine' ⟨hT.isSelfAdjoint.add hS.isSelfAdjoint, fun x => _⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
T S : E →L[𝕜] E
hT : IsPositive T
hS : IsPositive S
x : E
⊢ 0 ≤ reApplyInnerSelf (T + S) x
[PROOFSTEP]
rw [reApplyInnerSelf, add_apply, inner_add_left, map_add]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
T S : E →L[𝕜] E
hT : IsPositive T
hS : IsPositive S
x : E
⊢ 0 ≤ ↑re (inner (↑T x) x) + ↑re (inner (↑S x) x)
[PROOFSTEP]
exact add_nonneg (hT.inner_nonneg_left x) (hS.inner_nonneg_left x)
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
T : E →L[𝕜] E
hT : IsPositive T
S : E →L[𝕜] F
⊢ IsPositive (comp S (comp T (↑adjoint S)))
[PROOFSTEP]
refine' ⟨hT.isSelfAdjoint.conj_adjoint S, fun x => _⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
T : E →L[𝕜] E
hT : IsPositive T
S : E →L[𝕜] F
x : F
⊢ 0 ≤ reApplyInnerSelf (comp S (comp T (↑adjoint S))) x
[PROOFSTEP]
rw [reApplyInnerSelf, comp_apply, ← adjoint_inner_right]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
T : E →L[𝕜] E
hT : IsPositive T
S : E →L[𝕜] F
x : F
⊢ 0 ≤ ↑re (inner (↑(comp T (↑adjoint S)) x) (↑(↑adjoint S) x))
[PROOFSTEP]
exact hT.inner_nonneg_left _
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
T : E →L[𝕜] E
hT : IsPositive T
S : F →L[𝕜] E
⊢ IsPositive (comp (↑adjoint S) (comp T S))
[PROOFSTEP]
convert hT.conj_adjoint (S†)
[GOAL]
case h.e'_7.h.e'_24.h.e'_24
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
T : E →L[𝕜] E
hT : IsPositive T
S : F →L[𝕜] E
⊢ S = ↑adjoint (↑adjoint S)
[PROOFSTEP]
rw [adjoint_adjoint]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : InnerProductSpace 𝕜 F
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace F
U : Submodule 𝕜 E
T : E →L[𝕜] E
hT : IsPositive T
inst✝ : CompleteSpace { x // x ∈ U }
⊢ IsPositive
    (comp (Submodule.subtypeL U)
      (comp (orthogonalProjection U) (comp T (comp (Submodule.subtypeL U) (orthogonalProjection U)))))
[PROOFSTEP]
have := hT.conj_adjoint (U.subtypeL ∘L orthogonalProjection U)
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : InnerProductSpace 𝕜 F
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace F
U : Submodule 𝕜 E
T : E →L[𝕜] E
hT : IsPositive T
inst✝ : CompleteSpace { x // x ∈ U }
this :
  IsPositive
    (comp (comp (Submodule.subtypeL U) (orthogonalProjection U))
      (comp T (↑adjoint (comp (Submodule.subtypeL U) (orthogonalProjection U)))))
⊢ IsPositive
    (comp (Submodule.subtypeL U)
      (comp (orthogonalProjection U) (comp T (comp (Submodule.subtypeL U) (orthogonalProjection U)))))
[PROOFSTEP]
rwa [(orthogonalProjection_isSelfAdjoint U).adjoint_eq] at this
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : InnerProductSpace 𝕜 F
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace F
T : E →L[𝕜] E
hT : IsPositive T
U : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ U }
⊢ IsPositive (comp (orthogonalProjection U) (comp T (Submodule.subtypeL U)))
[PROOFSTEP]
have := hT.conj_adjoint (orthogonalProjection U : E →L[𝕜] U)
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : InnerProductSpace 𝕜 F
inst✝² : CompleteSpace E
inst✝¹ : CompleteSpace F
T : E →L[𝕜] E
hT : IsPositive T
U : Submodule 𝕜 E
inst✝ : CompleteSpace { x // x ∈ U }
this : IsPositive (comp (orthogonalProjection U) (comp T (↑adjoint (orthogonalProjection U))))
⊢ IsPositive (comp (orthogonalProjection U) (comp T (Submodule.subtypeL U)))
[PROOFSTEP]
rwa [U.adjoint_orthogonalProjection] at this
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : InnerProductSpace 𝕜 F
inst✝⁴ : CompleteSpace E
inst✝³ : CompleteSpace F
E' : Type u_4
inst✝² : NormedAddCommGroup E'
inst✝¹ : InnerProductSpace ℂ E'
inst✝ : CompleteSpace E'
T : E' →L[ℂ] E'
⊢ IsPositive T ↔ ∀ (x : E'), ↑(↑re (inner (↑T x) x)) = inner (↑T x) x ∧ 0 ≤ ↑re (inner (↑T x) x)
[PROOFSTEP]
simp_rw [IsPositive, forall_and, isSelfAdjoint_iff_isSymmetric, LinearMap.isSymmetric_iff_inner_map_self_real,
  conj_eq_iff_re]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace 𝕜 E
inst✝⁵ : InnerProductSpace 𝕜 F
inst✝⁴ : CompleteSpace E
inst✝³ : CompleteSpace F
E' : Type u_4
inst✝² : NormedAddCommGroup E'
inst✝¹ : InnerProductSpace ℂ E'
inst✝ : CompleteSpace E'
T : E' →L[ℂ] E'
⊢ ((∀ (v : E'), ↑(↑re (inner (↑↑T v) v)) = inner (↑↑T v) v) ∧ ∀ (x : E'), 0 ≤ reApplyInnerSelf T x) ↔
    (∀ (x : E'), ↑(↑re (inner (↑T x) x)) = inner (↑T x) x) ∧ ∀ (x : E'), 0 ≤ ↑re (inner (↑T x) x)
[PROOFSTEP]
rfl


[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
ne : Nonempty ι
e f : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
h : Basis.orientation (OrthonormalBasis.toBasis e) = Basis.orientation (OrthonormalBasis.toBasis f)
⊢ ↑(Basis.det (OrthonormalBasis.toBasis e)) ↑f = 1
[PROOFSTEP]
apply (e.det_to_matrix_orthonormalBasis_real f).resolve_right
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
ne : Nonempty ι
e f : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
h : Basis.orientation (OrthonormalBasis.toBasis e) = Basis.orientation (OrthonormalBasis.toBasis f)
⊢ ¬↑(Basis.det (OrthonormalBasis.toBasis e)) ↑f = -1
[PROOFSTEP]
have : 0 < e.toBasis.det f := by
  rw [e.toBasis.orientation_eq_iff_det_pos] at h
  simpa using h
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
ne : Nonempty ι
e f : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
h : Basis.orientation (OrthonormalBasis.toBasis e) = Basis.orientation (OrthonormalBasis.toBasis f)
⊢ 0 < ↑(Basis.det (OrthonormalBasis.toBasis e)) ↑f
[PROOFSTEP]
rw [e.toBasis.orientation_eq_iff_det_pos] at h
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
ne : Nonempty ι
e f : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
h : 0 < ↑(Basis.det (OrthonormalBasis.toBasis e)) ↑(OrthonormalBasis.toBasis f)
⊢ 0 < ↑(Basis.det (OrthonormalBasis.toBasis e)) ↑f
[PROOFSTEP]
simpa using h
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
ne : Nonempty ι
e f : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
h : Basis.orientation (OrthonormalBasis.toBasis e) = Basis.orientation (OrthonormalBasis.toBasis f)
this : 0 < ↑(Basis.det (OrthonormalBasis.toBasis e)) ↑f
⊢ ¬↑(Basis.det (OrthonormalBasis.toBasis e)) ↑f = -1
[PROOFSTEP]
linarith
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
ne : Nonempty ι
e f : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
h : Basis.orientation (OrthonormalBasis.toBasis e) ≠ Basis.orientation (OrthonormalBasis.toBasis f)
⊢ ↑(Basis.det (OrthonormalBasis.toBasis e)) ↑f = -1
[PROOFSTEP]
contrapose! h
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
ne : Nonempty ι
e f : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
h : ↑(Basis.det (OrthonormalBasis.toBasis e)) ↑f ≠ -1
⊢ Basis.orientation (OrthonormalBasis.toBasis e) = Basis.orientation (OrthonormalBasis.toBasis f)
[PROOFSTEP]
simp [e.toBasis.orientation_eq_iff_det_pos, (e.det_to_matrix_orthonormalBasis_real f).resolve_right h]
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
ne : Nonempty ι
e f : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
⊢ Basis.det (OrthonormalBasis.toBasis e) = Basis.det (OrthonormalBasis.toBasis f) ↔
    Basis.orientation (OrthonormalBasis.toBasis e) = Basis.orientation (OrthonormalBasis.toBasis f)
[PROOFSTEP]
constructor
[GOAL]
case mp
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
ne : Nonempty ι
e f : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
⊢ Basis.det (OrthonormalBasis.toBasis e) = Basis.det (OrthonormalBasis.toBasis f) →
    Basis.orientation (OrthonormalBasis.toBasis e) = Basis.orientation (OrthonormalBasis.toBasis f)
[PROOFSTEP]
intro h
[GOAL]
case mp
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
ne : Nonempty ι
e f : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
h : Basis.det (OrthonormalBasis.toBasis e) = Basis.det (OrthonormalBasis.toBasis f)
⊢ Basis.orientation (OrthonormalBasis.toBasis e) = Basis.orientation (OrthonormalBasis.toBasis f)
[PROOFSTEP]
dsimp [Basis.orientation]
[GOAL]
case mp
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
ne : Nonempty ι
e f : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
h : Basis.det (OrthonormalBasis.toBasis e) = Basis.det (OrthonormalBasis.toBasis f)
⊢ rayOfNeZero ℝ (Basis.det (OrthonormalBasis.toBasis e)) (_ : Basis.det (OrthonormalBasis.toBasis e) ≠ 0) =
    rayOfNeZero ℝ (Basis.det (OrthonormalBasis.toBasis f)) (_ : Basis.det (OrthonormalBasis.toBasis f) ≠ 0)
[PROOFSTEP]
congr
[GOAL]
case mpr
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
ne : Nonempty ι
e f : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
⊢ Basis.orientation (OrthonormalBasis.toBasis e) = Basis.orientation (OrthonormalBasis.toBasis f) →
    Basis.det (OrthonormalBasis.toBasis e) = Basis.det (OrthonormalBasis.toBasis f)
[PROOFSTEP]
intro h
[GOAL]
case mpr
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
ne : Nonempty ι
e f : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
h : Basis.orientation (OrthonormalBasis.toBasis e) = Basis.orientation (OrthonormalBasis.toBasis f)
⊢ Basis.det (OrthonormalBasis.toBasis e) = Basis.det (OrthonormalBasis.toBasis f)
[PROOFSTEP]
rw [e.toBasis.det.eq_smul_basis_det f.toBasis]
[GOAL]
case mpr
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
ne : Nonempty ι
e f : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
h : Basis.orientation (OrthonormalBasis.toBasis e) = Basis.orientation (OrthonormalBasis.toBasis f)
⊢ ↑(Basis.det (OrthonormalBasis.toBasis e)) ↑(OrthonormalBasis.toBasis f) • Basis.det (OrthonormalBasis.toBasis f) =
    Basis.det (OrthonormalBasis.toBasis f)
[PROOFSTEP]
simp [e.det_to_matrix_orthonormalBasis_of_same_orientation f h]
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
ne : Nonempty ι
e f : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
h : Basis.orientation (OrthonormalBasis.toBasis e) ≠ Basis.orientation (OrthonormalBasis.toBasis f)
⊢ Basis.det (OrthonormalBasis.toBasis e) = -Basis.det (OrthonormalBasis.toBasis f)
[PROOFSTEP]
rw [e.toBasis.det.eq_smul_basis_det f.toBasis]
  -- Porting note: added `neg_one_smul` with explicit type
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
ne : Nonempty ι
e f : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
h : Basis.orientation (OrthonormalBasis.toBasis e) ≠ Basis.orientation (OrthonormalBasis.toBasis f)
⊢ ↑(Basis.det (OrthonormalBasis.toBasis e)) ↑(OrthonormalBasis.toBasis f) • Basis.det (OrthonormalBasis.toBasis f) =
    -Basis.det (OrthonormalBasis.toBasis f)
[PROOFSTEP]
simp [e.det_to_matrix_orthonormalBasis_of_opposite_orientation f h, neg_one_smul ℝ (M := AlternatingMap ℝ E ℝ ι)]
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
ne : Nonempty ι
e f : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
⊢ Orthonormal ℝ ↑(Basis.adjustToOrientation (OrthonormalBasis.toBasis e) x)
[PROOFSTEP]
apply e.orthonormal.orthonormal_of_forall_eq_or_eq_neg
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
ne : Nonempty ι
e f : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
⊢ ∀ (i : ι),
    ↑(Basis.adjustToOrientation (OrthonormalBasis.toBasis e) x) i = ↑e i ∨
      ↑(Basis.adjustToOrientation (OrthonormalBasis.toBasis e) x) i = -↑e i
[PROOFSTEP]
simpa using e.toBasis.adjustToOrientation_apply_eq_or_eq_neg x
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
ne : Nonempty ι
e f : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
⊢ Basis.orientation (OrthonormalBasis.toBasis (adjustToOrientation e x)) = x
[PROOFSTEP]
rw [e.toBasis_adjustToOrientation]
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
ne : Nonempty ι
e f : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
⊢ Basis.orientation (Basis.adjustToOrientation (OrthonormalBasis.toBasis e) x) = x
[PROOFSTEP]
exact e.toBasis.orientation_adjustToOrientation x
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
ne : Nonempty ι
e f : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
i : ι
⊢ ↑(adjustToOrientation e x) i = ↑e i ∨ ↑(adjustToOrientation e x) i = -↑e i
[PROOFSTEP]
simpa [← e.toBasis_adjustToOrientation] using e.toBasis.adjustToOrientation_apply_eq_or_eq_neg x i
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
ne : Nonempty ι
e f : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
⊢ Basis.det (OrthonormalBasis.toBasis (adjustToOrientation e x)) = Basis.det (OrthonormalBasis.toBasis e) ∨
    Basis.det (OrthonormalBasis.toBasis (adjustToOrientation e x)) = -Basis.det (OrthonormalBasis.toBasis e)
[PROOFSTEP]
simpa using e.toBasis.det_adjustToOrientation x
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
ne : Nonempty ι
e f : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
v : ι → E
⊢ |↑(Basis.det (OrthonormalBasis.toBasis (adjustToOrientation e x))) v| = |↑(Basis.det (OrthonormalBasis.toBasis e)) v|
[PROOFSTEP]
simp [toBasis_adjustToOrientation]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
hn : 0 < n
h : finrank ℝ E = n
x : Orientation ℝ E (Fin n)
⊢ OrthonormalBasis (Fin n) ℝ E
[PROOFSTEP]
haveI := Fin.pos_iff_nonempty.1 hn
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
hn : 0 < n
h : finrank ℝ E = n
x : Orientation ℝ E (Fin n)
this : Nonempty (Fin n)
⊢ OrthonormalBasis (Fin n) ℝ E
[PROOFSTEP]
haveI := finiteDimensional_of_finrank (h.symm ▸ hn : 0 < finrank ℝ E)
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
hn : 0 < n
h : finrank ℝ E = n
x : Orientation ℝ E (Fin n)
this✝ : Nonempty (Fin n)
this : FiniteDimensional ℝ E
⊢ OrthonormalBasis (Fin n) ℝ E
[PROOFSTEP]
exact ((@stdOrthonormalBasis _ _ _ _ _ this).reindex <| finCongr h).adjustToOrientation x
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
hn : 0 < n
h : finrank ℝ E = n
x : Orientation ℝ E (Fin n)
⊢ Basis.orientation (OrthonormalBasis.toBasis (Orientation.finOrthonormalBasis hn h x)) = x
[PROOFSTEP]
haveI := Fin.pos_iff_nonempty.1 hn
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
hn : 0 < n
h : finrank ℝ E = n
x : Orientation ℝ E (Fin n)
this : Nonempty (Fin n)
⊢ Basis.orientation (OrthonormalBasis.toBasis (Orientation.finOrthonormalBasis hn h x)) = x
[PROOFSTEP]
haveI := finiteDimensional_of_finrank (h.symm ▸ hn : 0 < finrank ℝ E)
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
hn : 0 < n
h : finrank ℝ E = n
x : Orientation ℝ E (Fin n)
this✝ : Nonempty (Fin n)
this : FiniteDimensional ℝ E
⊢ Basis.orientation (OrthonormalBasis.toBasis (Orientation.finOrthonormalBasis hn h x)) = x
[PROOFSTEP]
exact ((@stdOrthonormalBasis _ _ _ _ _ this).reindex <| finCongr h).orientation_adjustToOrientation x
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n)
o : Orientation ℝ E (Fin n)
⊢ IsEmpty (Fin Nat.zero)
[PROOFSTEP]
simp only [Nat.zero_eq]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n)
o : Orientation ℝ E (Fin n)
⊢ IsEmpty (Fin 0)
[PROOFSTEP]
infer_instance
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n)
o : Orientation ℝ E (Fin n)
⊢ AlternatingMap ℝ E ℝ (Fin n)
[PROOFSTEP]
classical
cases' n with n
· let opos : AlternatingMap ℝ E ℝ (Fin 0) := AlternatingMap.constOfIsEmpty ℝ E (Fin 0) (1 : ℝ)
  exact o.eq_or_eq_neg_of_isEmpty.by_cases (fun _ => opos) fun _ => -opos
· exact (o.finOrthonormalBasis n.succ_pos _i.out).toBasis.det
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n)
o : Orientation ℝ E (Fin n)
⊢ AlternatingMap ℝ E ℝ (Fin n)
[PROOFSTEP]
cases' n with n
[GOAL]
case zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = Nat.zero)
o : Orientation ℝ E (Fin Nat.zero)
⊢ AlternatingMap ℝ E ℝ (Fin Nat.zero)
[PROOFSTEP]
let opos : AlternatingMap ℝ E ℝ (Fin 0) := AlternatingMap.constOfIsEmpty ℝ E (Fin 0) (1 : ℝ)
[GOAL]
case zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = Nat.zero)
o : Orientation ℝ E (Fin Nat.zero)
opos : AlternatingMap ℝ E ℝ (Fin 0) := AlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1
⊢ AlternatingMap ℝ E ℝ (Fin Nat.zero)
[PROOFSTEP]
exact o.eq_or_eq_neg_of_isEmpty.by_cases (fun _ => opos) fun _ => -opos
[GOAL]
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
⊢ AlternatingMap ℝ E ℝ (Fin (Nat.succ n))
[PROOFSTEP]
exact (o.finOrthonormalBasis n.succ_pos _i.out).toBasis.det
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i✝ : Fact (finrank ℝ E = n)
o : Orientation ℝ E (Fin n)
_i : Fact (finrank ℝ E = 0)
⊢ volumeForm positiveOrientation = ↑AlternatingMap.constLinearEquivOfIsEmpty 1
[PROOFSTEP]
simp [volumeForm, Or.by_cases, if_pos]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i✝ : Fact (finrank ℝ E = n)
o : Orientation ℝ E (Fin n)
_i : Fact (finrank ℝ E = 0)
⊢ volumeForm (-positiveOrientation) = -↑AlternatingMap.constLinearEquivOfIsEmpty 1
[PROOFSTEP]
simp_rw [volumeForm, Or.by_cases, positiveOrientation]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i✝ : Fact (finrank ℝ E = n)
o : Orientation ℝ E (Fin n)
_i : Fact (finrank ℝ E = 0)
⊢ Nat.rec (motive := fun t => 0 = t → AlternatingMap ℝ E ℝ (Fin 0))
      (fun h =>
        if hp :
            -rayOfNeZero ℝ (↑AlternatingMap.constLinearEquivOfIsEmpty 1)
                  (_ :
                    ↑AlternatingMap.constLinearEquivOfIsEmpty 1 ≠
                      ↑AlternatingMap.constLinearEquivOfIsEmpty AddMonoid.toZero.1) =
              rayOfNeZero ℝ (↑AlternatingMap.constLinearEquivOfIsEmpty 1)
                (_ :
                  ↑AlternatingMap.constLinearEquivOfIsEmpty 1 ≠
                    ↑AlternatingMap.constLinearEquivOfIsEmpty AddMonoid.toZero.1) then
          AlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1
        else -AlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1)
      (fun n n_ih h =>
        Eq.rec (motive := fun x x_1 =>
          [_i : Fact (finrank ℝ E = x)] → Orientation ℝ E (Fin x) → AlternatingMap ℝ E ℝ (Fin x))
          (fun [Fact (finrank ℝ E = Nat.succ n)] o =>
            Basis.det
              (OrthonormalBasis.toBasis
                (Orientation.finOrthonormalBasis (_ : 0 < Nat.succ n) (_ : finrank ℝ E = Nat.succ n) o)))
          (_ : Nat.succ n = 0)
          (-rayOfNeZero ℝ (↑AlternatingMap.constLinearEquivOfIsEmpty 1)
              (_ :
                ↑AlternatingMap.constLinearEquivOfIsEmpty 1 ≠
                  ↑AlternatingMap.constLinearEquivOfIsEmpty AddMonoid.toZero.1)))
      0 (_ : 0 = 0) =
    -↑AlternatingMap.constLinearEquivOfIsEmpty 1
[PROOFSTEP]
apply if_neg
[GOAL]
case hnc
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i✝ : Fact (finrank ℝ E = n)
o : Orientation ℝ E (Fin n)
_i : Fact (finrank ℝ E = 0)
⊢ ¬-rayOfNeZero ℝ (↑AlternatingMap.constLinearEquivOfIsEmpty 1)
          (_ :
            ↑AlternatingMap.constLinearEquivOfIsEmpty 1 ≠
              ↑AlternatingMap.constLinearEquivOfIsEmpty AddMonoid.toZero.1) =
      rayOfNeZero ℝ (↑AlternatingMap.constLinearEquivOfIsEmpty 1)
        (_ : ↑AlternatingMap.constLinearEquivOfIsEmpty 1 ≠ ↑AlternatingMap.constLinearEquivOfIsEmpty AddMonoid.toZero.1)
[PROOFSTEP]
simp only [neg_rayOfNeZero]
[GOAL]
case hnc
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i✝ : Fact (finrank ℝ E = n)
o : Orientation ℝ E (Fin n)
_i : Fact (finrank ℝ E = 0)
⊢ ¬rayOfNeZero ℝ (-↑AlternatingMap.constLinearEquivOfIsEmpty 1) (_ : -↑AlternatingMap.constLinearEquivOfIsEmpty 1 ≠ 0) =
      rayOfNeZero ℝ (↑AlternatingMap.constLinearEquivOfIsEmpty 1)
        (_ : ↑AlternatingMap.constLinearEquivOfIsEmpty 1 ≠ ↑AlternatingMap.constLinearEquivOfIsEmpty AddMonoid.toZero.1)
[PROOFSTEP]
rw [ray_eq_iff, SameRay.sameRay_comm]
[GOAL]
case hnc
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i✝ : Fact (finrank ℝ E = n)
o : Orientation ℝ E (Fin n)
_i : Fact (finrank ℝ E = 0)
⊢ ¬SameRay ℝ (↑AlternatingMap.constLinearEquivOfIsEmpty 1) (-↑AlternatingMap.constLinearEquivOfIsEmpty 1)
[PROOFSTEP]
intro h
[GOAL]
case hnc
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i✝ : Fact (finrank ℝ E = n)
o : Orientation ℝ E (Fin n)
_i : Fact (finrank ℝ E = 0)
h : SameRay ℝ (↑AlternatingMap.constLinearEquivOfIsEmpty 1) (-↑AlternatingMap.constLinearEquivOfIsEmpty 1)
⊢ False
[PROOFSTEP]
simpa using congr_arg AlternatingMap.constLinearEquivOfIsEmpty.symm (eq_zero_of_sameRay_self_neg h)
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n)
o : Orientation ℝ E (Fin n)
b : OrthonormalBasis (Fin n) ℝ E
hb : Basis.orientation (OrthonormalBasis.toBasis b) = o
⊢ volumeForm o = Basis.det (OrthonormalBasis.toBasis b)
[PROOFSTEP]
cases n
[GOAL]
case zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = Nat.zero)
o : Orientation ℝ E (Fin Nat.zero)
b : OrthonormalBasis (Fin Nat.zero) ℝ E
hb : Basis.orientation (OrthonormalBasis.toBasis b) = o
⊢ volumeForm o = Basis.det (OrthonormalBasis.toBasis b)
[PROOFSTEP]
classical
have : o = positiveOrientation := hb.symm.trans b.toBasis.orientation_isEmpty
simp_rw [volumeForm, Or.by_cases, dif_pos this, Basis.det_isEmpty]
[GOAL]
case zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = Nat.zero)
o : Orientation ℝ E (Fin Nat.zero)
b : OrthonormalBasis (Fin Nat.zero) ℝ E
hb : Basis.orientation (OrthonormalBasis.toBasis b) = o
⊢ volumeForm o = Basis.det (OrthonormalBasis.toBasis b)
[PROOFSTEP]
have : o = positiveOrientation := hb.symm.trans b.toBasis.orientation_isEmpty
[GOAL]
case zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = Nat.zero)
o : Orientation ℝ E (Fin Nat.zero)
b : OrthonormalBasis (Fin Nat.zero) ℝ E
hb : Basis.orientation (OrthonormalBasis.toBasis b) = o
this : o = positiveOrientation
⊢ volumeForm o = Basis.det (OrthonormalBasis.toBasis b)
[PROOFSTEP]
simp_rw [volumeForm, Or.by_cases, dif_pos this, Basis.det_isEmpty]
[GOAL]
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n✝ : ℕ
_i : Fact (finrank ℝ E = Nat.succ n✝)
o : Orientation ℝ E (Fin (Nat.succ n✝))
b : OrthonormalBasis (Fin (Nat.succ n✝)) ℝ E
hb : Basis.orientation (OrthonormalBasis.toBasis b) = o
⊢ volumeForm o = Basis.det (OrthonormalBasis.toBasis b)
[PROOFSTEP]
simp_rw [volumeForm]
[GOAL]
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n✝ : ℕ
_i : Fact (finrank ℝ E = Nat.succ n✝)
o : Orientation ℝ E (Fin (Nat.succ n✝))
b : OrthonormalBasis (Fin (Nat.succ n✝)) ℝ E
hb : Basis.orientation (OrthonormalBasis.toBasis b) = o
⊢ Basis.det
      (OrthonormalBasis.toBasis
        (Orientation.finOrthonormalBasis (_ : 0 < Nat.succ n✝) (_ : finrank ℝ E = Nat.succ n✝) o)) =
    Basis.det (OrthonormalBasis.toBasis b)
[PROOFSTEP]
rw [same_orientation_iff_det_eq_det, hb]
[GOAL]
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n✝ : ℕ
_i : Fact (finrank ℝ E = Nat.succ n✝)
o : Orientation ℝ E (Fin (Nat.succ n✝))
b : OrthonormalBasis (Fin (Nat.succ n✝)) ℝ E
hb : Basis.orientation (OrthonormalBasis.toBasis b) = o
⊢ Basis.orientation
      (OrthonormalBasis.toBasis
        (Orientation.finOrthonormalBasis (_ : 0 < Nat.succ n✝) (_ : finrank ℝ E = Nat.succ n✝) o)) =
    o
[PROOFSTEP]
exact o.finOrthonormalBasis_orientation _ _
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n)
o : Orientation ℝ E (Fin n)
b : OrthonormalBasis (Fin n) ℝ E
hb : Basis.orientation (OrthonormalBasis.toBasis b) ≠ o
⊢ volumeForm o = -Basis.det (OrthonormalBasis.toBasis b)
[PROOFSTEP]
cases' n with n
[GOAL]
case zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = Nat.zero)
o : Orientation ℝ E (Fin Nat.zero)
b : OrthonormalBasis (Fin Nat.zero) ℝ E
hb : Basis.orientation (OrthonormalBasis.toBasis b) ≠ o
⊢ volumeForm o = -Basis.det (OrthonormalBasis.toBasis b)
[PROOFSTEP]
classical
have : positiveOrientation ≠ o := by rwa [b.toBasis.orientation_isEmpty] at hb
simp_rw [volumeForm, Or.by_cases, dif_neg this.symm, Basis.det_isEmpty]
[GOAL]
case zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = Nat.zero)
o : Orientation ℝ E (Fin Nat.zero)
b : OrthonormalBasis (Fin Nat.zero) ℝ E
hb : Basis.orientation (OrthonormalBasis.toBasis b) ≠ o
⊢ volumeForm o = -Basis.det (OrthonormalBasis.toBasis b)
[PROOFSTEP]
have : positiveOrientation ≠ o := by rwa [b.toBasis.orientation_isEmpty] at hb
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = Nat.zero)
o : Orientation ℝ E (Fin Nat.zero)
b : OrthonormalBasis (Fin Nat.zero) ℝ E
hb : Basis.orientation (OrthonormalBasis.toBasis b) ≠ o
⊢ positiveOrientation ≠ o
[PROOFSTEP]
rwa [b.toBasis.orientation_isEmpty] at hb
[GOAL]
case zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = Nat.zero)
o : Orientation ℝ E (Fin Nat.zero)
b : OrthonormalBasis (Fin Nat.zero) ℝ E
hb : Basis.orientation (OrthonormalBasis.toBasis b) ≠ o
this : positiveOrientation ≠ o
⊢ volumeForm o = -Basis.det (OrthonormalBasis.toBasis b)
[PROOFSTEP]
simp_rw [volumeForm, Or.by_cases, dif_neg this.symm, Basis.det_isEmpty]
[GOAL]
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E
hb : Basis.orientation (OrthonormalBasis.toBasis b) ≠ o
⊢ volumeForm o = -Basis.det (OrthonormalBasis.toBasis b)
[PROOFSTEP]
let e : OrthonormalBasis (Fin n.succ) ℝ E := o.finOrthonormalBasis n.succ_pos Fact.out
[GOAL]
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E
hb : Basis.orientation (OrthonormalBasis.toBasis b) ≠ o
e : OrthonormalBasis (Fin (Nat.succ n)) ℝ E :=
  Orientation.finOrthonormalBasis (_ : 0 < Nat.succ n) (_ : finrank ℝ E = Nat.succ n) o
⊢ volumeForm o = -Basis.det (OrthonormalBasis.toBasis b)
[PROOFSTEP]
simp_rw [volumeForm]
[GOAL]
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E
hb : Basis.orientation (OrthonormalBasis.toBasis b) ≠ o
e : OrthonormalBasis (Fin (Nat.succ n)) ℝ E :=
  Orientation.finOrthonormalBasis (_ : 0 < Nat.succ n) (_ : finrank ℝ E = Nat.succ n) o
⊢ Basis.det
      (OrthonormalBasis.toBasis
        (Orientation.finOrthonormalBasis (_ : 0 < Nat.succ n) (_ : finrank ℝ E = Nat.succ n) o)) =
    -Basis.det (OrthonormalBasis.toBasis b)
[PROOFSTEP]
apply e.det_eq_neg_det_of_opposite_orientation b
[GOAL]
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E
hb : Basis.orientation (OrthonormalBasis.toBasis b) ≠ o
e : OrthonormalBasis (Fin (Nat.succ n)) ℝ E :=
  Orientation.finOrthonormalBasis (_ : 0 < Nat.succ n) (_ : finrank ℝ E = Nat.succ n) o
⊢ Basis.orientation (OrthonormalBasis.toBasis e) ≠ Basis.orientation (OrthonormalBasis.toBasis b)
[PROOFSTEP]
convert hb.symm
[GOAL]
case h.e'_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E
hb : Basis.orientation (OrthonormalBasis.toBasis b) ≠ o
e : OrthonormalBasis (Fin (Nat.succ n)) ℝ E :=
  Orientation.finOrthonormalBasis (_ : 0 < Nat.succ n) (_ : finrank ℝ E = Nat.succ n) o
⊢ Basis.orientation (OrthonormalBasis.toBasis e) = o
[PROOFSTEP]
exact o.finOrthonormalBasis_orientation _ _
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n)
o : Orientation ℝ E (Fin n)
⊢ volumeForm (-o) = -volumeForm o
[PROOFSTEP]
cases' n with n
[GOAL]
case zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = Nat.zero)
o : Orientation ℝ E (Fin Nat.zero)
⊢ volumeForm (-o) = -volumeForm o
[PROOFSTEP]
refine' o.eq_or_eq_neg_of_isEmpty.elim _ _
[GOAL]
case zero.refine'_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = Nat.zero)
o : Orientation ℝ E (Fin Nat.zero)
⊢ o = positiveOrientation → volumeForm (-o) = -volumeForm o
[PROOFSTEP]
rintro rfl
[GOAL]
case zero.refine'_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = Nat.zero)
o : Orientation ℝ E (Fin Nat.zero)
⊢ o = -positiveOrientation → volumeForm (-o) = -volumeForm o
[PROOFSTEP]
rintro rfl
[GOAL]
case zero.refine'_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = Nat.zero)
⊢ volumeForm (-positiveOrientation) = -volumeForm positiveOrientation
[PROOFSTEP]
simp [volumeForm_zero_neg]
[GOAL]
case zero.refine'_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = Nat.zero)
⊢ volumeForm (- -positiveOrientation) = -volumeForm (-positiveOrientation)
[PROOFSTEP]
rw [neg_neg (positiveOrientation (R := ℝ))]
  -- Porting note: added
[GOAL]
case zero.refine'_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = Nat.zero)
⊢ volumeForm positiveOrientation = -volumeForm (-positiveOrientation)
[PROOFSTEP]
simp [volumeForm_zero_neg]
[GOAL]
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
⊢ volumeForm (-o) = -volumeForm o
[PROOFSTEP]
let e : OrthonormalBasis (Fin n.succ) ℝ E := o.finOrthonormalBasis n.succ_pos Fact.out
[GOAL]
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
e : OrthonormalBasis (Fin (Nat.succ n)) ℝ E :=
  Orientation.finOrthonormalBasis (_ : 0 < Nat.succ n) (_ : finrank ℝ E = Nat.succ n) o
⊢ volumeForm (-o) = -volumeForm o
[PROOFSTEP]
have h₁ : e.toBasis.orientation = o := o.finOrthonormalBasis_orientation _ _
[GOAL]
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
e : OrthonormalBasis (Fin (Nat.succ n)) ℝ E :=
  Orientation.finOrthonormalBasis (_ : 0 < Nat.succ n) (_ : finrank ℝ E = Nat.succ n) o
h₁ : Basis.orientation (OrthonormalBasis.toBasis e) = o
⊢ volumeForm (-o) = -volumeForm o
[PROOFSTEP]
have h₂ : e.toBasis.orientation ≠ -o := by
  symm
  rw [e.toBasis.orientation_ne_iff_eq_neg, h₁]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
e : OrthonormalBasis (Fin (Nat.succ n)) ℝ E :=
  Orientation.finOrthonormalBasis (_ : 0 < Nat.succ n) (_ : finrank ℝ E = Nat.succ n) o
h₁ : Basis.orientation (OrthonormalBasis.toBasis e) = o
⊢ Basis.orientation (OrthonormalBasis.toBasis e) ≠ -o
[PROOFSTEP]
symm
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
e : OrthonormalBasis (Fin (Nat.succ n)) ℝ E :=
  Orientation.finOrthonormalBasis (_ : 0 < Nat.succ n) (_ : finrank ℝ E = Nat.succ n) o
h₁ : Basis.orientation (OrthonormalBasis.toBasis e) = o
⊢ -o ≠ Basis.orientation (OrthonormalBasis.toBasis e)
[PROOFSTEP]
rw [e.toBasis.orientation_ne_iff_eq_neg, h₁]
[GOAL]
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
e : OrthonormalBasis (Fin (Nat.succ n)) ℝ E :=
  Orientation.finOrthonormalBasis (_ : 0 < Nat.succ n) (_ : finrank ℝ E = Nat.succ n) o
h₁ : Basis.orientation (OrthonormalBasis.toBasis e) = o
h₂ : Basis.orientation (OrthonormalBasis.toBasis e) ≠ -o
⊢ volumeForm (-o) = -volumeForm o
[PROOFSTEP]
rw [o.volumeForm_robust e h₁, (-o).volumeForm_robust_neg e h₂]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n)
o : Orientation ℝ E (Fin n)
b : OrthonormalBasis (Fin n) ℝ E
v : Fin n → E
⊢ |↑(volumeForm o) v| = |↑(Basis.det (OrthonormalBasis.toBasis b)) v|
[PROOFSTEP]
cases n
[GOAL]
case zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = Nat.zero)
o : Orientation ℝ E (Fin Nat.zero)
b : OrthonormalBasis (Fin Nat.zero) ℝ E
v : Fin Nat.zero → E
⊢ |↑(volumeForm o) v| = |↑(Basis.det (OrthonormalBasis.toBasis b)) v|
[PROOFSTEP]
refine' o.eq_or_eq_neg_of_isEmpty.elim _ _
[GOAL]
case zero.refine'_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = Nat.zero)
o : Orientation ℝ E (Fin Nat.zero)
b : OrthonormalBasis (Fin Nat.zero) ℝ E
v : Fin Nat.zero → E
⊢ o = positiveOrientation → |↑(volumeForm o) v| = |↑(Basis.det (OrthonormalBasis.toBasis b)) v|
[PROOFSTEP]
rintro rfl
[GOAL]
case zero.refine'_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = Nat.zero)
o : Orientation ℝ E (Fin Nat.zero)
b : OrthonormalBasis (Fin Nat.zero) ℝ E
v : Fin Nat.zero → E
⊢ o = -positiveOrientation → |↑(volumeForm o) v| = |↑(Basis.det (OrthonormalBasis.toBasis b)) v|
[PROOFSTEP]
rintro rfl
[GOAL]
case zero.refine'_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = Nat.zero)
b : OrthonormalBasis (Fin Nat.zero) ℝ E
v : Fin Nat.zero → E
⊢ |↑(volumeForm positiveOrientation) v| = |↑(Basis.det (OrthonormalBasis.toBasis b)) v|
[PROOFSTEP]
simp
[GOAL]
case zero.refine'_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = Nat.zero)
b : OrthonormalBasis (Fin Nat.zero) ℝ E
v : Fin Nat.zero → E
⊢ |↑(volumeForm (-positiveOrientation)) v| = |↑(Basis.det (OrthonormalBasis.toBasis b)) v|
[PROOFSTEP]
simp
[GOAL]
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n✝ : ℕ
_i : Fact (finrank ℝ E = Nat.succ n✝)
o : Orientation ℝ E (Fin (Nat.succ n✝))
b : OrthonormalBasis (Fin (Nat.succ n✝)) ℝ E
v : Fin (Nat.succ n✝) → E
⊢ |↑(volumeForm o) v| = |↑(Basis.det (OrthonormalBasis.toBasis b)) v|
[PROOFSTEP]
rw [o.volumeForm_robust (b.adjustToOrientation o) (b.orientation_adjustToOrientation o), b.abs_det_adjustToOrientation]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n)
o : Orientation ℝ E (Fin n)
v : Fin n → E
⊢ |↑(volumeForm o) v| ≤ ∏ i : Fin n, ‖v i‖
[PROOFSTEP]
cases' n with n
[GOAL]
case zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = Nat.zero)
o : Orientation ℝ E (Fin Nat.zero)
v : Fin Nat.zero → E
⊢ |↑(volumeForm o) v| ≤ ∏ i : Fin Nat.zero, ‖v i‖
[PROOFSTEP]
refine' o.eq_or_eq_neg_of_isEmpty.elim _ _
[GOAL]
case zero.refine'_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = Nat.zero)
o : Orientation ℝ E (Fin Nat.zero)
v : Fin Nat.zero → E
⊢ o = positiveOrientation → |↑(volumeForm o) v| ≤ ∏ i : Fin Nat.zero, ‖v i‖
[PROOFSTEP]
rintro rfl
[GOAL]
case zero.refine'_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = Nat.zero)
o : Orientation ℝ E (Fin Nat.zero)
v : Fin Nat.zero → E
⊢ o = -positiveOrientation → |↑(volumeForm o) v| ≤ ∏ i : Fin Nat.zero, ‖v i‖
[PROOFSTEP]
rintro rfl
[GOAL]
case zero.refine'_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = Nat.zero)
v : Fin Nat.zero → E
⊢ |↑(volumeForm positiveOrientation) v| ≤ ∏ i : Fin Nat.zero, ‖v i‖
[PROOFSTEP]
simp
[GOAL]
case zero.refine'_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = Nat.zero)
v : Fin Nat.zero → E
⊢ |↑(volumeForm (-positiveOrientation)) v| ≤ ∏ i : Fin Nat.zero, ‖v i‖
[PROOFSTEP]
simp
[GOAL]
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
v : Fin (Nat.succ n) → E
⊢ |↑(volumeForm o) v| ≤ ∏ i : Fin (Nat.succ n), ‖v i‖
[PROOFSTEP]
haveI : FiniteDimensional ℝ E := fact_finiteDimensional_of_finrank_eq_succ n
[GOAL]
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
v : Fin (Nat.succ n) → E
this : FiniteDimensional ℝ E
⊢ |↑(volumeForm o) v| ≤ ∏ i : Fin (Nat.succ n), ‖v i‖
[PROOFSTEP]
have : finrank ℝ E = Fintype.card (Fin n.succ) := by simpa using _i.out
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
v : Fin (Nat.succ n) → E
this : FiniteDimensional ℝ E
⊢ finrank ℝ E = Fintype.card (Fin (Nat.succ n))
[PROOFSTEP]
simpa using _i.out
[GOAL]
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
v : Fin (Nat.succ n) → E
this✝ : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
⊢ |↑(volumeForm o) v| ≤ ∏ i : Fin (Nat.succ n), ‖v i‖
[PROOFSTEP]
let b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis this v
[GOAL]
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
v : Fin (Nat.succ n) → E
this✝ : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E := gramSchmidtOrthonormalBasis this v
⊢ |↑(volumeForm o) v| ≤ ∏ i : Fin (Nat.succ n), ‖v i‖
[PROOFSTEP]
have hb : b.toBasis.det v = ∏ i, ⟪b i, v i⟫ := gramSchmidtOrthonormalBasis_det this v
[GOAL]
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
v : Fin (Nat.succ n) → E
this✝ : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E := gramSchmidtOrthonormalBasis this v
hb : ↑(Basis.det (OrthonormalBasis.toBasis b)) v = ∏ i : Fin (Nat.succ n), inner (↑b i) (v i)
⊢ |↑(volumeForm o) v| ≤ ∏ i : Fin (Nat.succ n), ‖v i‖
[PROOFSTEP]
rw [o.volumeForm_robust' b, hb, Finset.abs_prod]
[GOAL]
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
v : Fin (Nat.succ n) → E
this✝ : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E := gramSchmidtOrthonormalBasis this v
hb : ↑(Basis.det (OrthonormalBasis.toBasis b)) v = ∏ i : Fin (Nat.succ n), inner (↑b i) (v i)
⊢ ∏ x : Fin (Nat.succ n), |inner (↑b x) (v x)| ≤ ∏ i : Fin (Nat.succ n), ‖v i‖
[PROOFSTEP]
apply Finset.prod_le_prod
[GOAL]
case succ.h0
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
v : Fin (Nat.succ n) → E
this✝ : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E := gramSchmidtOrthonormalBasis this v
hb : ↑(Basis.det (OrthonormalBasis.toBasis b)) v = ∏ i : Fin (Nat.succ n), inner (↑b i) (v i)
⊢ ∀ (i : Fin (Nat.succ n)), i ∈ Finset.univ → 0 ≤ |inner (↑b i) (v i)|
[PROOFSTEP]
intro i _
[GOAL]
case succ.h0
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
v : Fin (Nat.succ n) → E
this✝ : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E := gramSchmidtOrthonormalBasis this v
hb : ↑(Basis.det (OrthonormalBasis.toBasis b)) v = ∏ i : Fin (Nat.succ n), inner (↑b i) (v i)
i : Fin (Nat.succ n)
a✝ : i ∈ Finset.univ
⊢ 0 ≤ |inner (↑b i) (v i)|
[PROOFSTEP]
positivity
[GOAL]
case succ.h1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
v : Fin (Nat.succ n) → E
this✝ : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E := gramSchmidtOrthonormalBasis this v
hb : ↑(Basis.det (OrthonormalBasis.toBasis b)) v = ∏ i : Fin (Nat.succ n), inner (↑b i) (v i)
⊢ ∀ (i : Fin (Nat.succ n)), i ∈ Finset.univ → |inner (↑b i) (v i)| ≤ ‖v i‖
[PROOFSTEP]
intro i _
[GOAL]
case succ.h1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
v : Fin (Nat.succ n) → E
this✝ : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E := gramSchmidtOrthonormalBasis this v
hb : ↑(Basis.det (OrthonormalBasis.toBasis b)) v = ∏ i : Fin (Nat.succ n), inner (↑b i) (v i)
i : Fin (Nat.succ n)
a✝ : i ∈ Finset.univ
⊢ |inner (↑b i) (v i)| ≤ ‖v i‖
[PROOFSTEP]
convert abs_real_inner_le_norm (b i) (v i)
[GOAL]
case h.e'_4
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
v : Fin (Nat.succ n) → E
this✝ : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E := gramSchmidtOrthonormalBasis this v
hb : ↑(Basis.det (OrthonormalBasis.toBasis b)) v = ∏ i : Fin (Nat.succ n), inner (↑b i) (v i)
i : Fin (Nat.succ n)
a✝ : i ∈ Finset.univ
⊢ ‖v i‖ = ‖↑b i‖ * ‖v i‖
[PROOFSTEP]
simp [b.orthonormal.1 i]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n)
o : Orientation ℝ E (Fin n)
v : Fin n → E
hv : Pairwise fun i j => inner (v i) (v j) = 0
⊢ |↑(volumeForm o) v| = ∏ i : Fin n, ‖v i‖
[PROOFSTEP]
cases' n with n
[GOAL]
case zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = Nat.zero)
o : Orientation ℝ E (Fin Nat.zero)
v : Fin Nat.zero → E
hv : Pairwise fun i j => inner (v i) (v j) = 0
⊢ |↑(volumeForm o) v| = ∏ i : Fin Nat.zero, ‖v i‖
[PROOFSTEP]
refine' o.eq_or_eq_neg_of_isEmpty.elim _ _
[GOAL]
case zero.refine'_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = Nat.zero)
o : Orientation ℝ E (Fin Nat.zero)
v : Fin Nat.zero → E
hv : Pairwise fun i j => inner (v i) (v j) = 0
⊢ o = positiveOrientation → |↑(volumeForm o) v| = ∏ i : Fin Nat.zero, ‖v i‖
[PROOFSTEP]
rintro rfl
[GOAL]
case zero.refine'_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = Nat.zero)
o : Orientation ℝ E (Fin Nat.zero)
v : Fin Nat.zero → E
hv : Pairwise fun i j => inner (v i) (v j) = 0
⊢ o = -positiveOrientation → |↑(volumeForm o) v| = ∏ i : Fin Nat.zero, ‖v i‖
[PROOFSTEP]
rintro rfl
[GOAL]
case zero.refine'_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = Nat.zero)
v : Fin Nat.zero → E
hv : Pairwise fun i j => inner (v i) (v j) = 0
⊢ |↑(volumeForm positiveOrientation) v| = ∏ i : Fin Nat.zero, ‖v i‖
[PROOFSTEP]
simp
[GOAL]
case zero.refine'_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = Nat.zero)
v : Fin Nat.zero → E
hv : Pairwise fun i j => inner (v i) (v j) = 0
⊢ |↑(volumeForm (-positiveOrientation)) v| = ∏ i : Fin Nat.zero, ‖v i‖
[PROOFSTEP]
simp
[GOAL]
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
v : Fin (Nat.succ n) → E
hv : Pairwise fun i j => inner (v i) (v j) = 0
⊢ |↑(volumeForm o) v| = ∏ i : Fin (Nat.succ n), ‖v i‖
[PROOFSTEP]
haveI : FiniteDimensional ℝ E := fact_finiteDimensional_of_finrank_eq_succ n
[GOAL]
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
v : Fin (Nat.succ n) → E
hv : Pairwise fun i j => inner (v i) (v j) = 0
this : FiniteDimensional ℝ E
⊢ |↑(volumeForm o) v| = ∏ i : Fin (Nat.succ n), ‖v i‖
[PROOFSTEP]
have hdim : finrank ℝ E = Fintype.card (Fin n.succ) := by simpa using _i.out
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
v : Fin (Nat.succ n) → E
hv : Pairwise fun i j => inner (v i) (v j) = 0
this : FiniteDimensional ℝ E
⊢ finrank ℝ E = Fintype.card (Fin (Nat.succ n))
[PROOFSTEP]
simpa using _i.out
[GOAL]
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
v : Fin (Nat.succ n) → E
hv : Pairwise fun i j => inner (v i) (v j) = 0
this : FiniteDimensional ℝ E
hdim : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
⊢ |↑(volumeForm o) v| = ∏ i : Fin (Nat.succ n), ‖v i‖
[PROOFSTEP]
let b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis hdim v
[GOAL]
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
v : Fin (Nat.succ n) → E
hv : Pairwise fun i j => inner (v i) (v j) = 0
this : FiniteDimensional ℝ E
hdim : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E := gramSchmidtOrthonormalBasis hdim v
⊢ |↑(volumeForm o) v| = ∏ i : Fin (Nat.succ n), ‖v i‖
[PROOFSTEP]
have hb : b.toBasis.det v = ∏ i, ⟪b i, v i⟫ := gramSchmidtOrthonormalBasis_det hdim v
[GOAL]
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
v : Fin (Nat.succ n) → E
hv : Pairwise fun i j => inner (v i) (v j) = 0
this : FiniteDimensional ℝ E
hdim : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E := gramSchmidtOrthonormalBasis hdim v
hb : ↑(Basis.det (OrthonormalBasis.toBasis b)) v = ∏ i : Fin (Nat.succ n), inner (↑b i) (v i)
⊢ |↑(volumeForm o) v| = ∏ i : Fin (Nat.succ n), ‖v i‖
[PROOFSTEP]
rw [o.volumeForm_robust' b, hb, Finset.abs_prod]
[GOAL]
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
v : Fin (Nat.succ n) → E
hv : Pairwise fun i j => inner (v i) (v j) = 0
this : FiniteDimensional ℝ E
hdim : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E := gramSchmidtOrthonormalBasis hdim v
hb : ↑(Basis.det (OrthonormalBasis.toBasis b)) v = ∏ i : Fin (Nat.succ n), inner (↑b i) (v i)
⊢ ∏ x : Fin (Nat.succ n), |inner (↑b x) (v x)| = ∏ i : Fin (Nat.succ n), ‖v i‖
[PROOFSTEP]
by_cases h : ∃ i, v i = 0
[GOAL]
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
v : Fin (Nat.succ n) → E
hv : Pairwise fun i j => inner (v i) (v j) = 0
this : FiniteDimensional ℝ E
hdim : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E := gramSchmidtOrthonormalBasis hdim v
hb : ↑(Basis.det (OrthonormalBasis.toBasis b)) v = ∏ i : Fin (Nat.succ n), inner (↑b i) (v i)
h : ∃ i, v i = 0
⊢ ∏ x : Fin (Nat.succ n), |inner (↑b x) (v x)| = ∏ i : Fin (Nat.succ n), ‖v i‖
case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
v : Fin (Nat.succ n) → E
hv : Pairwise fun i j => inner (v i) (v j) = 0
this : FiniteDimensional ℝ E
hdim : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E := gramSchmidtOrthonormalBasis hdim v
hb : ↑(Basis.det (OrthonormalBasis.toBasis b)) v = ∏ i : Fin (Nat.succ n), inner (↑b i) (v i)
h : ¬∃ i, v i = 0
⊢ ∏ x : Fin (Nat.succ n), |inner (↑b x) (v x)| = ∏ i : Fin (Nat.succ n), ‖v i‖
[PROOFSTEP]
obtain ⟨i, hi⟩ := h
[GOAL]
case pos.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
v : Fin (Nat.succ n) → E
hv : Pairwise fun i j => inner (v i) (v j) = 0
this : FiniteDimensional ℝ E
hdim : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E := gramSchmidtOrthonormalBasis hdim v
hb : ↑(Basis.det (OrthonormalBasis.toBasis b)) v = ∏ i : Fin (Nat.succ n), inner (↑b i) (v i)
i : Fin (Nat.succ n)
hi : v i = 0
⊢ ∏ x : Fin (Nat.succ n), |inner (↑b x) (v x)| = ∏ i : Fin (Nat.succ n), ‖v i‖
[PROOFSTEP]
rw [Finset.prod_eq_zero (Finset.mem_univ i), Finset.prod_eq_zero (Finset.mem_univ i)]
[GOAL]
case pos.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
v : Fin (Nat.succ n) → E
hv : Pairwise fun i j => inner (v i) (v j) = 0
this : FiniteDimensional ℝ E
hdim : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E := gramSchmidtOrthonormalBasis hdim v
hb : ↑(Basis.det (OrthonormalBasis.toBasis b)) v = ∏ i : Fin (Nat.succ n), inner (↑b i) (v i)
i : Fin (Nat.succ n)
hi : v i = 0
⊢ ‖v i‖ = 0
[PROOFSTEP]
simp [hi]
[GOAL]
case pos.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
v : Fin (Nat.succ n) → E
hv : Pairwise fun i j => inner (v i) (v j) = 0
this : FiniteDimensional ℝ E
hdim : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E := gramSchmidtOrthonormalBasis hdim v
hb : ↑(Basis.det (OrthonormalBasis.toBasis b)) v = ∏ i : Fin (Nat.succ n), inner (↑b i) (v i)
i : Fin (Nat.succ n)
hi : v i = 0
⊢ |inner (↑b i) (v i)| = 0
[PROOFSTEP]
simp [hi]
[GOAL]
case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
v : Fin (Nat.succ n) → E
hv : Pairwise fun i j => inner (v i) (v j) = 0
this : FiniteDimensional ℝ E
hdim : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E := gramSchmidtOrthonormalBasis hdim v
hb : ↑(Basis.det (OrthonormalBasis.toBasis b)) v = ∏ i : Fin (Nat.succ n), inner (↑b i) (v i)
h : ¬∃ i, v i = 0
⊢ ∏ x : Fin (Nat.succ n), |inner (↑b x) (v x)| = ∏ i : Fin (Nat.succ n), ‖v i‖
[PROOFSTEP]
push_neg at h
[GOAL]
case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
v : Fin (Nat.succ n) → E
hv : Pairwise fun i j => inner (v i) (v j) = 0
this : FiniteDimensional ℝ E
hdim : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E := gramSchmidtOrthonormalBasis hdim v
hb : ↑(Basis.det (OrthonormalBasis.toBasis b)) v = ∏ i : Fin (Nat.succ n), inner (↑b i) (v i)
h : ∀ (i : Fin (Nat.succ n)), v i ≠ 0
⊢ ∏ x : Fin (Nat.succ n), |inner (↑b x) (v x)| = ∏ i : Fin (Nat.succ n), ‖v i‖
[PROOFSTEP]
congr
[GOAL]
case neg.e_f
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
v : Fin (Nat.succ n) → E
hv : Pairwise fun i j => inner (v i) (v j) = 0
this : FiniteDimensional ℝ E
hdim : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E := gramSchmidtOrthonormalBasis hdim v
hb : ↑(Basis.det (OrthonormalBasis.toBasis b)) v = ∏ i : Fin (Nat.succ n), inner (↑b i) (v i)
h : ∀ (i : Fin (Nat.succ n)), v i ≠ 0
⊢ (fun x => |inner (↑b x) (v x)|) = fun i => ‖v i‖
[PROOFSTEP]
ext i
[GOAL]
case neg.e_f.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
v : Fin (Nat.succ n) → E
hv : Pairwise fun i j => inner (v i) (v j) = 0
this : FiniteDimensional ℝ E
hdim : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E := gramSchmidtOrthonormalBasis hdim v
hb : ↑(Basis.det (OrthonormalBasis.toBasis b)) v = ∏ i : Fin (Nat.succ n), inner (↑b i) (v i)
h : ∀ (i : Fin (Nat.succ n)), v i ≠ 0
i : Fin (Nat.succ n)
⊢ |inner (↑b i) (v i)| = ‖v i‖
[PROOFSTEP]
have hb : b i = ‖v i‖⁻¹ • v i := gramSchmidtOrthonormalBasis_apply_of_orthogonal hdim hv (h i)
[GOAL]
case neg.e_f.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
v : Fin (Nat.succ n) → E
hv : Pairwise fun i j => inner (v i) (v j) = 0
this : FiniteDimensional ℝ E
hdim : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E := gramSchmidtOrthonormalBasis hdim v
hb✝ : ↑(Basis.det (OrthonormalBasis.toBasis b)) v = ∏ i : Fin (Nat.succ n), inner (↑b i) (v i)
h : ∀ (i : Fin (Nat.succ n)), v i ≠ 0
i : Fin (Nat.succ n)
hb : ↑b i = ‖v i‖⁻¹ • v i
⊢ |inner (↑b i) (v i)| = ‖v i‖
[PROOFSTEP]
simp only [hb, inner_smul_left, real_inner_self_eq_norm_mul_norm, IsROrC.conj_to_real]
[GOAL]
case neg.e_f.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
v : Fin (Nat.succ n) → E
hv : Pairwise fun i j => inner (v i) (v j) = 0
this : FiniteDimensional ℝ E
hdim : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E := gramSchmidtOrthonormalBasis hdim v
hb✝ : ↑(Basis.det (OrthonormalBasis.toBasis b)) v = ∏ i : Fin (Nat.succ n), inner (↑b i) (v i)
h : ∀ (i : Fin (Nat.succ n)), v i ≠ 0
i : Fin (Nat.succ n)
hb : ↑b i = ‖v i‖⁻¹ • v i
⊢ |‖v i‖⁻¹ * (‖v i‖ * ‖v i‖)| = ‖v i‖
[PROOFSTEP]
rw [abs_of_nonneg]
[GOAL]
case neg.e_f.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
v : Fin (Nat.succ n) → E
hv : Pairwise fun i j => inner (v i) (v j) = 0
this : FiniteDimensional ℝ E
hdim : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E := gramSchmidtOrthonormalBasis hdim v
hb✝ : ↑(Basis.det (OrthonormalBasis.toBasis b)) v = ∏ i : Fin (Nat.succ n), inner (↑b i) (v i)
h : ∀ (i : Fin (Nat.succ n)), v i ≠ 0
i : Fin (Nat.succ n)
hb : ↑b i = ‖v i‖⁻¹ • v i
⊢ ‖v i‖⁻¹ * (‖v i‖ * ‖v i‖) = ‖v i‖
[PROOFSTEP]
field_simp
[GOAL]
case neg.e_f.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
v : Fin (Nat.succ n) → E
hv : Pairwise fun i j => inner (v i) (v j) = 0
this : FiniteDimensional ℝ E
hdim : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E := gramSchmidtOrthonormalBasis hdim v
hb✝ : ↑(Basis.det (OrthonormalBasis.toBasis b)) v = ∏ i : Fin (Nat.succ n), inner (↑b i) (v i)
h : ∀ (i : Fin (Nat.succ n)), v i ≠ 0
i : Fin (Nat.succ n)
hb : ↑b i = ‖v i‖⁻¹ • v i
⊢ 0 ≤ ‖v i‖⁻¹ * (‖v i‖ * ‖v i‖)
[PROOFSTEP]
positivity
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n)
o : Orientation ℝ E (Fin n)
v : OrthonormalBasis (Fin n) ℝ E
⊢ |↑(volumeForm o) ↑v| = 1
[PROOFSTEP]
simpa [o.volumeForm_robust' v v] using congr_arg abs v.toBasis.det_self
[GOAL]
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n)
o : Orientation ℝ E (Fin n)
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : Fact (finrank ℝ F = n)
φ : E ≃ₗᵢ[ℝ] F
x : Fin n → F
⊢ ↑(volumeForm (↑(map (Fin n) φ.toLinearEquiv) o)) x = ↑(volumeForm o) (↑(LinearIsometryEquiv.symm φ) ∘ x)
[PROOFSTEP]
cases' n with n
[GOAL]
case zero
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
φ : E ≃ₗᵢ[ℝ] F
_i : Fact (finrank ℝ E = Nat.zero)
o : Orientation ℝ E (Fin Nat.zero)
inst✝ : Fact (finrank ℝ F = Nat.zero)
x : Fin Nat.zero → F
⊢ ↑(volumeForm (↑(map (Fin Nat.zero) φ.toLinearEquiv) o)) x = ↑(volumeForm o) (↑(LinearIsometryEquiv.symm φ) ∘ x)
[PROOFSTEP]
refine' o.eq_or_eq_neg_of_isEmpty.elim _ _
[GOAL]
case zero.refine'_1
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
φ : E ≃ₗᵢ[ℝ] F
_i : Fact (finrank ℝ E = Nat.zero)
o : Orientation ℝ E (Fin Nat.zero)
inst✝ : Fact (finrank ℝ F = Nat.zero)
x : Fin Nat.zero → F
⊢ o = positiveOrientation →
    ↑(volumeForm (↑(map (Fin Nat.zero) φ.toLinearEquiv) o)) x = ↑(volumeForm o) (↑(LinearIsometryEquiv.symm φ) ∘ x)
[PROOFSTEP]
rintro rfl
[GOAL]
case zero.refine'_2
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
φ : E ≃ₗᵢ[ℝ] F
_i : Fact (finrank ℝ E = Nat.zero)
o : Orientation ℝ E (Fin Nat.zero)
inst✝ : Fact (finrank ℝ F = Nat.zero)
x : Fin Nat.zero → F
⊢ o = -positiveOrientation →
    ↑(volumeForm (↑(map (Fin Nat.zero) φ.toLinearEquiv) o)) x = ↑(volumeForm o) (↑(LinearIsometryEquiv.symm φ) ∘ x)
[PROOFSTEP]
rintro rfl
[GOAL]
case zero.refine'_1
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
φ : E ≃ₗᵢ[ℝ] F
_i : Fact (finrank ℝ E = Nat.zero)
inst✝ : Fact (finrank ℝ F = Nat.zero)
x : Fin Nat.zero → F
⊢ ↑(volumeForm (↑(map (Fin Nat.zero) φ.toLinearEquiv) positiveOrientation)) x =
    ↑(volumeForm positiveOrientation) (↑(LinearIsometryEquiv.symm φ) ∘ x)
[PROOFSTEP]
simp
[GOAL]
case zero.refine'_2
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
φ : E ≃ₗᵢ[ℝ] F
_i : Fact (finrank ℝ E = Nat.zero)
inst✝ : Fact (finrank ℝ F = Nat.zero)
x : Fin Nat.zero → F
⊢ ↑(volumeForm (↑(map (Fin Nat.zero) φ.toLinearEquiv) (-positiveOrientation))) x =
    ↑(volumeForm (-positiveOrientation)) (↑(LinearIsometryEquiv.symm φ) ∘ x)
[PROOFSTEP]
simp
[GOAL]
case succ
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
φ : E ≃ₗᵢ[ℝ] F
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
inst✝ : Fact (finrank ℝ F = Nat.succ n)
x : Fin (Nat.succ n) → F
⊢ ↑(volumeForm (↑(map (Fin (Nat.succ n)) φ.toLinearEquiv) o)) x = ↑(volumeForm o) (↑(LinearIsometryEquiv.symm φ) ∘ x)
[PROOFSTEP]
let e : OrthonormalBasis (Fin n.succ) ℝ E := o.finOrthonormalBasis n.succ_pos Fact.out
[GOAL]
case succ
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
φ : E ≃ₗᵢ[ℝ] F
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
inst✝ : Fact (finrank ℝ F = Nat.succ n)
x : Fin (Nat.succ n) → F
e : OrthonormalBasis (Fin (Nat.succ n)) ℝ E :=
  Orientation.finOrthonormalBasis (_ : 0 < Nat.succ n) (_ : finrank ℝ E = Nat.succ n) o
⊢ ↑(volumeForm (↑(map (Fin (Nat.succ n)) φ.toLinearEquiv) o)) x = ↑(volumeForm o) (↑(LinearIsometryEquiv.symm φ) ∘ x)
[PROOFSTEP]
have he : e.toBasis.orientation = o := o.finOrthonormalBasis_orientation n.succ_pos Fact.out
[GOAL]
case succ
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
φ : E ≃ₗᵢ[ℝ] F
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
inst✝ : Fact (finrank ℝ F = Nat.succ n)
x : Fin (Nat.succ n) → F
e : OrthonormalBasis (Fin (Nat.succ n)) ℝ E :=
  Orientation.finOrthonormalBasis (_ : 0 < Nat.succ n) (_ : finrank ℝ E = Nat.succ n) o
he : Basis.orientation (OrthonormalBasis.toBasis e) = o
⊢ ↑(volumeForm (↑(map (Fin (Nat.succ n)) φ.toLinearEquiv) o)) x = ↑(volumeForm o) (↑(LinearIsometryEquiv.symm φ) ∘ x)
[PROOFSTEP]
have heφ : (e.map φ).toBasis.orientation = Orientation.map (Fin n.succ) φ.toLinearEquiv o :=
  by
  rw [← he]
  exact e.toBasis.orientation_map φ.toLinearEquiv
[GOAL]
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
φ : E ≃ₗᵢ[ℝ] F
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
inst✝ : Fact (finrank ℝ F = Nat.succ n)
x : Fin (Nat.succ n) → F
e : OrthonormalBasis (Fin (Nat.succ n)) ℝ E :=
  Orientation.finOrthonormalBasis (_ : 0 < Nat.succ n) (_ : finrank ℝ E = Nat.succ n) o
he : Basis.orientation (OrthonormalBasis.toBasis e) = o
⊢ Basis.orientation (OrthonormalBasis.toBasis (OrthonormalBasis.map e φ)) = ↑(map (Fin (Nat.succ n)) φ.toLinearEquiv) o
[PROOFSTEP]
rw [← he]
[GOAL]
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
φ : E ≃ₗᵢ[ℝ] F
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
inst✝ : Fact (finrank ℝ F = Nat.succ n)
x : Fin (Nat.succ n) → F
e : OrthonormalBasis (Fin (Nat.succ n)) ℝ E :=
  Orientation.finOrthonormalBasis (_ : 0 < Nat.succ n) (_ : finrank ℝ E = Nat.succ n) o
he : Basis.orientation (OrthonormalBasis.toBasis e) = o
⊢ Basis.orientation (OrthonormalBasis.toBasis (OrthonormalBasis.map e φ)) =
    ↑(map (Fin (Nat.succ n)) φ.toLinearEquiv) (Basis.orientation (OrthonormalBasis.toBasis e))
[PROOFSTEP]
exact e.toBasis.orientation_map φ.toLinearEquiv
[GOAL]
case succ
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
φ : E ≃ₗᵢ[ℝ] F
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
inst✝ : Fact (finrank ℝ F = Nat.succ n)
x : Fin (Nat.succ n) → F
e : OrthonormalBasis (Fin (Nat.succ n)) ℝ E :=
  Orientation.finOrthonormalBasis (_ : 0 < Nat.succ n) (_ : finrank ℝ E = Nat.succ n) o
he : Basis.orientation (OrthonormalBasis.toBasis e) = o
heφ :
  Basis.orientation (OrthonormalBasis.toBasis (OrthonormalBasis.map e φ)) = ↑(map (Fin (Nat.succ n)) φ.toLinearEquiv) o
⊢ ↑(volumeForm (↑(map (Fin (Nat.succ n)) φ.toLinearEquiv) o)) x = ↑(volumeForm o) (↑(LinearIsometryEquiv.symm φ) ∘ x)
[PROOFSTEP]
rw [(Orientation.map (Fin n.succ) φ.toLinearEquiv o).volumeForm_robust (e.map φ) heφ]
[GOAL]
case succ
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
φ : E ≃ₗᵢ[ℝ] F
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
inst✝ : Fact (finrank ℝ F = Nat.succ n)
x : Fin (Nat.succ n) → F
e : OrthonormalBasis (Fin (Nat.succ n)) ℝ E :=
  Orientation.finOrthonormalBasis (_ : 0 < Nat.succ n) (_ : finrank ℝ E = Nat.succ n) o
he : Basis.orientation (OrthonormalBasis.toBasis e) = o
heφ :
  Basis.orientation (OrthonormalBasis.toBasis (OrthonormalBasis.map e φ)) = ↑(map (Fin (Nat.succ n)) φ.toLinearEquiv) o
⊢ ↑(Basis.det (OrthonormalBasis.toBasis (OrthonormalBasis.map e φ))) x =
    ↑(volumeForm o) (↑(LinearIsometryEquiv.symm φ) ∘ x)
[PROOFSTEP]
rw [o.volumeForm_robust e he]
[GOAL]
case succ
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
φ : E ≃ₗᵢ[ℝ] F
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
inst✝ : Fact (finrank ℝ F = Nat.succ n)
x : Fin (Nat.succ n) → F
e : OrthonormalBasis (Fin (Nat.succ n)) ℝ E :=
  Orientation.finOrthonormalBasis (_ : 0 < Nat.succ n) (_ : finrank ℝ E = Nat.succ n) o
he : Basis.orientation (OrthonormalBasis.toBasis e) = o
heφ :
  Basis.orientation (OrthonormalBasis.toBasis (OrthonormalBasis.map e φ)) = ↑(map (Fin (Nat.succ n)) φ.toLinearEquiv) o
⊢ ↑(Basis.det (OrthonormalBasis.toBasis (OrthonormalBasis.map e φ))) x =
    ↑(Basis.det (OrthonormalBasis.toBasis e)) (↑(LinearIsometryEquiv.symm φ) ∘ x)
[PROOFSTEP]
simp
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n)
o : Orientation ℝ E (Fin n)
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < ↑LinearMap.det ↑φ.toLinearEquiv
x : Fin n → E
⊢ ↑(volumeForm o) (↑φ ∘ x) = ↑(volumeForm o) x
[PROOFSTEP]
cases' n with n
[GOAL]
case zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < ↑LinearMap.det ↑φ.toLinearEquiv
_i : Fact (finrank ℝ E = Nat.zero)
o : Orientation ℝ E (Fin Nat.zero)
x : Fin Nat.zero → E
⊢ ↑(volumeForm o) (↑φ ∘ x) = ↑(volumeForm o) x
[PROOFSTEP]
refine' o.eq_or_eq_neg_of_isEmpty.elim _ _
[GOAL]
case zero.refine'_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < ↑LinearMap.det ↑φ.toLinearEquiv
_i : Fact (finrank ℝ E = Nat.zero)
o : Orientation ℝ E (Fin Nat.zero)
x : Fin Nat.zero → E
⊢ o = positiveOrientation → ↑(volumeForm o) (↑φ ∘ x) = ↑(volumeForm o) x
[PROOFSTEP]
rintro rfl
[GOAL]
case zero.refine'_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < ↑LinearMap.det ↑φ.toLinearEquiv
_i : Fact (finrank ℝ E = Nat.zero)
o : Orientation ℝ E (Fin Nat.zero)
x : Fin Nat.zero → E
⊢ o = -positiveOrientation → ↑(volumeForm o) (↑φ ∘ x) = ↑(volumeForm o) x
[PROOFSTEP]
rintro rfl
[GOAL]
case zero.refine'_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < ↑LinearMap.det ↑φ.toLinearEquiv
_i : Fact (finrank ℝ E = Nat.zero)
x : Fin Nat.zero → E
⊢ ↑(volumeForm positiveOrientation) (↑φ ∘ x) = ↑(volumeForm positiveOrientation) x
[PROOFSTEP]
simp
[GOAL]
case zero.refine'_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < ↑LinearMap.det ↑φ.toLinearEquiv
_i : Fact (finrank ℝ E = Nat.zero)
x : Fin Nat.zero → E
⊢ ↑(volumeForm (-positiveOrientation)) (↑φ ∘ x) = ↑(volumeForm (-positiveOrientation)) x
[PROOFSTEP]
simp
[GOAL]
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < ↑LinearMap.det ↑φ.toLinearEquiv
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
x : Fin (Nat.succ n) → E
⊢ ↑(volumeForm o) (↑φ ∘ x) = ↑(volumeForm o) x
[PROOFSTEP]
haveI : FiniteDimensional ℝ E := fact_finiteDimensional_of_finrank_eq_succ n
[GOAL]
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < ↑LinearMap.det ↑φ.toLinearEquiv
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
x : Fin (Nat.succ n) → E
this : FiniteDimensional ℝ E
⊢ ↑(volumeForm o) (↑φ ∘ x) = ↑(volumeForm o) x
[PROOFSTEP]
convert o.volumeForm_map φ (φ ∘ x)
[GOAL]
case h.e'_2.h.e'_5.h.e'_6
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < ↑LinearMap.det ↑φ.toLinearEquiv
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
x : Fin (Nat.succ n) → E
this : FiniteDimensional ℝ E
⊢ o = ↑(map (Fin (Nat.succ n)) φ.toLinearEquiv) o
[PROOFSTEP]
symm
[GOAL]
case h.e'_2.h.e'_5.h.e'_6
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < ↑LinearMap.det ↑φ.toLinearEquiv
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
x : Fin (Nat.succ n) → E
this : FiniteDimensional ℝ E
⊢ ↑(map (Fin (Nat.succ n)) φ.toLinearEquiv) o = o
[PROOFSTEP]
rwa [← o.map_eq_iff_det_pos φ.toLinearEquiv] at hφ
[GOAL]
case h.e'_2.h.e'_5.h.e'_6
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < ↑LinearMap.det ↑φ.toLinearEquiv
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
x : Fin (Nat.succ n) → E
this : FiniteDimensional ℝ E
⊢ Fintype.card (Fin (Nat.succ n)) = finrank ℝ E
[PROOFSTEP]
rw [_i.out, Fintype.card_fin]
[GOAL]
case h.e'_3.h.e'_6
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < ↑LinearMap.det ↑φ.toLinearEquiv
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
x : Fin (Nat.succ n) → E
this : FiniteDimensional ℝ E
⊢ x = ↑(LinearIsometryEquiv.symm φ) ∘ ↑φ ∘ x
[PROOFSTEP]
ext
[GOAL]
case h.e'_3.h.e'_6.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < ↑LinearMap.det ↑φ.toLinearEquiv
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
x : Fin (Nat.succ n) → E
this : FiniteDimensional ℝ E
x✝ : Fin (Nat.succ n)
⊢ x x✝ = (↑(LinearIsometryEquiv.symm φ) ∘ ↑φ ∘ x) x✝
[PROOFSTEP]
simp