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

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
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
cases' n with n
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
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
haveI : FiniteDimensional ℝ E := fact_finiteDimensional_of_finrank_eq_succ n
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

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
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
convert o.volumeForm_map φ (φ ∘ x)
no goals
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
refine' o.eq_or_eq_neg_of_isEmpty.elim _ _ <;> rintro rfl <;> simp
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
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
symm
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
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
rwa [← o.map_eq_iff_det_pos φ.toLinearEquiv] at hφ
no goals
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
rw [_i.out, Fintype.card_fin]
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✝
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
ext
no goals
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✝
simp