ι : Type u_1
ι' : Type ?u.44123
E : Type ?u.44126
F : Type ?u.44129
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
⊢ parallelepiped ↑b = Icc 0 1 ∨ parallelepiped ↑b = Icc (-1) 0
ι : Type u_1
ι' : Type ?u.44123
E : Type ?u.44126
F : Type ?u.44129
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
b : OrthonormalBasis ι ℝ ℝ
⊢ parallelepiped ↑b = Icc 0 1 ∨ parallelepiped ↑b = Icc (-1) 0
have e : ι ≃ Fin 1 := by
  apply Fintype.equivFinOfCardEq
  simp only [← finrank_eq_card_basis b.toBasis, finrank_self]
ι : Type u_1
ι' : Type ?u.44123
E : Type ?u.44126
F : Type ?u.44129
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ↑(OrthonormalBasis.reindex b e) = parallelepiped ↑b
⊢ parallelepiped ↑b = Icc 0 1 ∨ parallelepiped ↑b = Icc (-1) 0
ι : Type u_1
ι' : Type ?u.44123
E : Type ?u.44126
F : Type ?u.44129
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
⊢ parallelepiped ↑b = Icc 0 1 ∨ parallelepiped ↑b = Icc (-1) 0
have B : parallelepiped (b.reindex e) = parallelepiped b := by
  convert parallelepiped_comp_equiv b e.symm
  ext i
  simp only [OrthonormalBasis.coe_reindex]
ι : Type u_1
ι' : Type ?u.44123
E : Type ?u.44126
F : Type ?u.44129
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ↑(OrthonormalBasis.reindex b e) = parallelepiped ↑b
⊢ parallelepiped ↑(OrthonormalBasis.reindex b e) = Icc 0 1 ∨ parallelepiped ↑(OrthonormalBasis.reindex b e) = Icc (-1) 0
ι : Type u_1
ι' : Type ?u.44123
E : Type ?u.44126
F : Type ?u.44129
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ↑(OrthonormalBasis.reindex b e) = parallelepiped ↑b
⊢ parallelepiped ↑b = Icc 0 1 ∨ parallelepiped ↑b = Icc (-1) 0
rw [← B]
ι : Type u_1
ι' : Type ?u.44123
E : Type ?u.44126
F✝ : Type ?u.44129
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F✝
inst✝ : Module ℝ F✝
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ↑(OrthonormalBasis.reindex b e) = parallelepiped ↑b
F : ℝ → Fin 1 → ℝ := fun t _i => t
⊢ parallelepiped ↑(OrthonormalBasis.reindex b e) = Icc 0 1 ∨ parallelepiped ↑(OrthonormalBasis.reindex b e) = Icc (-1) 0
ι : Type u_1
ι' : Type ?u.44123
E : Type ?u.44126
F : Type ?u.44129
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ↑(OrthonormalBasis.reindex b e) = parallelepiped ↑b
⊢ parallelepiped ↑(OrthonormalBasis.reindex b e) = Icc 0 1 ∨ parallelepiped ↑(OrthonormalBasis.reindex b e) = Icc (-1) 0
let F : ℝ → Fin 1 → ℝ := fun t => fun _i => t
case inl
ι : Type u_1
ι' : Type ?u.44123
E : Type ?u.44126
F✝ : Type ?u.44129
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F✝
inst✝ : Module ℝ F✝
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ↑(OrthonormalBasis.reindex b e) = parallelepiped ↑b
F : ℝ → Fin 1 → ℝ := fun t _i => t
A : Icc 0 1 = F '' Icc 0 1
H : ↑(OrthonormalBasis.reindex b e) = fun x => 1
⊢ parallelepiped ↑(OrthonormalBasis.reindex b e) = Icc 0 1 ∨ parallelepiped ↑(OrthonormalBasis.reindex b e) = Icc (-1) 0

case inr
ι : Type u_1
ι' : Type ?u.44123
E : Type ?u.44126
F✝ : Type ?u.44129
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F✝
inst✝ : Module ℝ F✝
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ↑(OrthonormalBasis.reindex b e) = parallelepiped ↑b
F : ℝ → Fin 1 → ℝ := fun t _i => t
A : Icc 0 1 = F '' Icc 0 1
H : ↑(OrthonormalBasis.reindex b e) = fun x => -1
⊢ parallelepiped ↑(OrthonormalBasis.reindex b e) = Icc 0 1 ∨ parallelepiped ↑(OrthonormalBasis.reindex b e) = Icc (-1) 0
ι : Type u_1
ι' : Type ?u.44123
E : Type ?u.44126
F✝ : Type ?u.44129
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F✝
inst✝ : Module ℝ F✝
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ↑(OrthonormalBasis.reindex b e) = parallelepiped ↑b
F : ℝ → Fin 1 → ℝ := fun t _i => t
A : Icc 0 1 = F '' Icc 0 1
⊢ parallelepiped ↑(OrthonormalBasis.reindex b e) = Icc 0 1 ∨ parallelepiped ↑(OrthonormalBasis.reindex b e) = Icc (-1) 0
rcases orthonormalBasis_one_dim (b.reindex e) with (H | H)
case h
ι : Type u_1
ι' : Type ?u.44123
E : Type ?u.44126
F : Type ?u.44129
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
b : OrthonormalBasis ι ℝ ℝ
⊢ Fintype.card ι = 1
ι : Type u_1
ι' : Type ?u.44123
E : Type ?u.44126
F : Type ?u.44129
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
b : OrthonormalBasis ι ℝ ℝ
⊢ ι ≃ Fin 1
apply Fintype.equivFinOfCardEq
no goals
case h
ι : Type u_1
ι' : Type ?u.44123
E : Type ?u.44126
F : Type ?u.44129
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
b : OrthonormalBasis ι ℝ ℝ
⊢ Fintype.card ι = 1
simp only [← finrank_eq_card_basis b.toBasis, finrank_self]
case h.e'_2.h.e'_6
ι : Type u_1
ι' : Type ?u.44123
E : Type ?u.44126
F : Type ?u.44129
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
⊢ ↑(OrthonormalBasis.reindex b e) = ↑b ∘ ↑e.symm
ι : Type u_1
ι' : Type ?u.44123
E : Type ?u.44126
F : Type ?u.44129
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
⊢ parallelepiped ↑(OrthonormalBasis.reindex b e) = parallelepiped ↑b
convert parallelepiped_comp_equiv b e.symm
case h.e'_2.h.e'_6.h
ι : Type u_1
ι' : Type ?u.44123
E : Type ?u.44126
F : Type ?u.44129
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
i : Fin 1
⊢ ↑(OrthonormalBasis.reindex b e) i = (↑b ∘ ↑e.symm) i
case h.e'_2.h.e'_6
ι : Type u_1
ι' : Type ?u.44123
E : Type ?u.44126
F : Type ?u.44129
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
⊢ ↑(OrthonormalBasis.reindex b e) = ↑b ∘ ↑e.symm
ext i
no goals
case h.e'_2.h.e'_6.h
ι : Type u_1
ι' : Type ?u.44123
E : Type ?u.44126
F : Type ?u.44129
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
i : Fin 1
⊢ ↑(OrthonormalBasis.reindex b e) i = (↑b ∘ ↑e.symm) i
simp only [OrthonormalBasis.coe_reindex]
case h₁
ι : Type u_1
ι' : Type ?u.44123
E : Type ?u.44126
F✝ : Type ?u.44129
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F✝
inst✝ : Module ℝ F✝
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ↑(OrthonormalBasis.reindex b e) = parallelepiped ↑b
F : ℝ → Fin 1 → ℝ := fun t _i => t
⊢ Icc 0 1 ⊆ F '' Icc 0 1

case h₂
ι : Type u_1
ι' : Type ?u.44123
E : Type ?u.44126
F✝ : Type ?u.44129
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F✝
inst✝ : Module ℝ F✝
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ↑(OrthonormalBasis.reindex b e) = parallelepiped ↑b
F : ℝ → Fin 1 → ℝ := fun t _i => t
⊢ F '' Icc 0 1 ⊆ Icc 0 1
ι : Type u_1
ι' : Type ?u.44123
E : Type ?u.44126
F✝ : Type ?u.44129
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F✝
inst✝ : Module ℝ F✝
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ↑(OrthonormalBasis.reindex b e) = parallelepiped ↑b
F : ℝ → Fin 1 → ℝ := fun t _i => t
⊢ Icc 0 1 = F '' Icc 0 1
apply Subset.antisymm
case h₁
ι : Type u_1
ι' : Type ?u.44123
E : Type ?u.44126
F✝ : Type ?u.44129
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F✝
inst✝ : Module ℝ F✝
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ↑(OrthonormalBasis.reindex b e) = parallelepiped ↑b
F : ℝ → Fin 1 → ℝ := fun t _i => t
x : Fin 1 → ℝ
hx : x ∈ Icc 0 1
⊢ x ∈ F '' Icc 0 1
case h₁
ι : Type u_1
ι' : Type ?u.44123
E : Type ?u.44126
F✝ : Type ?u.44129
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F✝
inst✝ : Module ℝ F✝
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ↑(OrthonormalBasis.reindex b e) = parallelepiped ↑b
F : ℝ → Fin 1 → ℝ := fun t _i => t
⊢ Icc 0 1 ⊆ F '' Icc 0 1
intro x hx
case h₁
ι : Type u_1
ι' : Type ?u.44123
E : Type ?u.44126
F✝ : Type ?u.44129
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F✝
inst✝ : Module ℝ F✝
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ↑(OrthonormalBasis.reindex b e) = parallelepiped ↑b
F : ℝ → Fin 1 → ℝ := fun t _i => t
x : Fin 1 → ℝ
hx : x ∈ Icc 0 1
⊢ F (x 0) = x
case h₁
ι : Type u_1
ι' : Type ?u.44123
E : Type ?u.44126
F✝ : Type ?u.44129
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F✝
inst✝ : Module ℝ F✝
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ↑(OrthonormalBasis.reindex b e) = parallelepiped ↑b
F : ℝ → Fin 1 → ℝ := fun t _i => t
x : Fin 1 → ℝ
hx : x ∈ Icc 0 1
⊢ x ∈ F '' Icc 0 1
refine' ⟨x 0, ⟨hx.1 0, hx.2 0⟩, _⟩
case h₁.h
ι : Type u_1
ι' : Type ?u.44123
E : Type ?u.44126
F✝ : Type ?u.44129
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F✝
inst✝ : Module ℝ F✝
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ↑(OrthonormalBasis.reindex b e) = parallelepiped ↑b
F : ℝ → Fin 1 → ℝ := fun t _i => t
x : Fin 1 → ℝ
hx : x ∈ Icc 0 1
j : Fin 1
⊢ F (x 0) j = x j
case h₁
ι : Type u_1
ι' : Type ?u.44123
E : Type ?u.44126
F✝ : Type ?u.44129
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F✝
inst✝ : Module ℝ F✝
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ↑(OrthonormalBasis.reindex b e) = parallelepiped ↑b
F : ℝ → Fin 1 → ℝ := fun t _i => t
x : Fin 1 → ℝ
hx : x ∈ Icc 0 1
⊢ F (x 0) = x
ext j
no goals
case h₁.h
ι : Type u_1
ι' : Type ?u.44123
E : Type ?u.44126
F✝ : Type ?u.44129
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F✝
inst✝ : Module ℝ F✝
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ↑(OrthonormalBasis.reindex b e) = parallelepiped ↑b
F : ℝ → Fin 1 → ℝ := fun t _i => t
x : Fin 1 → ℝ
hx : x ∈ Icc 0 1
j : Fin 1
⊢ F (x 0) j = x j
simp only [Subsingleton.elim j 0]
case h₂.intro.intro
ι : Type u_1
ι' : Type ?u.44123
E : Type ?u.44126
F✝ : Type ?u.44129
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F✝
inst✝ : Module ℝ F✝
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ↑(OrthonormalBasis.reindex b e) = parallelepiped ↑b
F : ℝ → Fin 1 → ℝ := fun t _i => t
y : ℝ
hy : y ∈ Icc 0 1
⊢ F y ∈ Icc 0 1
case h₂
ι : Type u_1
ι' : Type ?u.44123
E : Type ?u.44126
F✝ : Type ?u.44129
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F✝
inst✝ : Module ℝ F✝
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ↑(OrthonormalBasis.reindex b e) = parallelepiped ↑b
F : ℝ → Fin 1 → ℝ := fun t _i => t
⊢ F '' Icc 0 1 ⊆ Icc 0 1
rintro x ⟨y, hy, rfl⟩
no goals
case h₂.intro.intro
ι : Type u_1
ι' : Type ?u.44123
E : Type ?u.44126
F✝ : Type ?u.44129
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F✝
inst✝ : Module ℝ F✝
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ↑(OrthonormalBasis.reindex b e) = parallelepiped ↑b
F : ℝ → Fin 1 → ℝ := fun t _i => t
y : ℝ
hy : y ∈ Icc 0 1
⊢ F y ∈ Icc 0 1
exact ⟨fun _j => hy.1, fun _j => hy.2⟩
case inl.h
ι : Type u_1
ι' : Type ?u.44123
E : Type ?u.44126
F✝ : Type ?u.44129
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F✝
inst✝ : Module ℝ F✝
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ↑(OrthonormalBasis.reindex b e) = parallelepiped ↑b
F : ℝ → Fin 1 → ℝ := fun t _i => t
A : Icc 0 1 = F '' Icc 0 1
H : ↑(OrthonormalBasis.reindex b e) = fun x => 1
⊢ parallelepiped ↑(OrthonormalBasis.reindex b e) = Icc 0 1
case inl
ι : Type u_1
ι' : Type ?u.44123
E : Type ?u.44126
F✝ : Type ?u.44129
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F✝
inst✝ : Module ℝ F✝
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ↑(OrthonormalBasis.reindex b e) = parallelepiped ↑b
F : ℝ → Fin 1 → ℝ := fun t _i => t
A : Icc 0 1 = F '' Icc 0 1
H : ↑(OrthonormalBasis.reindex b e) = fun x => 1
⊢ parallelepiped ↑(OrthonormalBasis.reindex b e) = Icc 0 1 ∨ parallelepiped ↑(OrthonormalBasis.reindex b e) = Icc (-1) 0
left
case inl.h
ι : Type u_1
ι' : Type ?u.44123
E : Type ?u.44126
F✝ : Type ?u.44129
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F✝
inst✝ : Module ℝ F✝
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ↑(OrthonormalBasis.reindex b e) = parallelepiped ↑b
F : ℝ → Fin 1 → ℝ := fun t _i => t
A : Icc 0 1 = F '' Icc 0 1
H : ↑(OrthonormalBasis.reindex b e) = fun x => 1
⊢ (fun a => ∑ x : Fin 1, a x) '' ((fun a _i => a) '' Icc 0 1) = Icc 0 1
case inl.h
ι : Type u_1
ι' : Type ?u.44123
E : Type ?u.44126
F✝ : Type ?u.44129
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F✝
inst✝ : Module ℝ F✝
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ↑(OrthonormalBasis.reindex b e) = parallelepiped ↑b
F : ℝ → Fin 1 → ℝ := fun t _i => t
A : Icc 0 1 = F '' Icc 0 1
H : ↑(OrthonormalBasis.reindex b e) = fun x => 1
⊢ parallelepiped ↑(OrthonormalBasis.reindex b e) = Icc 0 1
simp_rw [parallelepiped, H, A, Algebra.id.smul_eq_mul, mul_one]
no goals
case inl.h
ι : Type u_1
ι' : Type ?u.44123
E : Type ?u.44126
F✝ : Type ?u.44129
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F✝
inst✝ : Module ℝ F✝
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ↑(OrthonormalBasis.reindex b e) = parallelepiped ↑b
F : ℝ → Fin 1 → ℝ := fun t _i => t
A : Icc 0 1 = F '' Icc 0 1
H : ↑(OrthonormalBasis.reindex b e) = fun x => 1
⊢ (fun a => ∑ x : Fin 1, a x) '' ((fun a _i => a) '' Icc 0 1) = Icc 0 1
simp only [Finset.univ_unique, Fin.default_eq_zero, smul_eq_mul, mul_one, Finset.sum_singleton,
  ← image_comp, Function.comp_apply, image_id', ge_iff_le, zero_le_one, not_true, gt_iff_lt]
case inr.h
ι : Type u_1
ι' : Type ?u.44123
E : Type ?u.44126
F✝ : Type ?u.44129
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F✝
inst✝ : Module ℝ F✝
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ↑(OrthonormalBasis.reindex b e) = parallelepiped ↑b
F : ℝ → Fin 1 → ℝ := fun t _i => t
A : Icc 0 1 = F '' Icc 0 1
H : ↑(OrthonormalBasis.reindex b e) = fun x => -1
⊢ parallelepiped ↑(OrthonormalBasis.reindex b e) = Icc (-1) 0
case inr
ι : Type u_1
ι' : Type ?u.44123
E : Type ?u.44126
F✝ : Type ?u.44129
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F✝
inst✝ : Module ℝ F✝
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ↑(OrthonormalBasis.reindex b e) = parallelepiped ↑b
F : ℝ → Fin 1 → ℝ := fun t _i => t
A : Icc 0 1 = F '' Icc 0 1
H : ↑(OrthonormalBasis.reindex b e) = fun x => -1
⊢ parallelepiped ↑(OrthonormalBasis.reindex b e) = Icc 0 1 ∨ parallelepiped ↑(OrthonormalBasis.reindex b e) = Icc (-1) 0
right
case inr.h
ι : Type u_1
ι' : Type ?u.44123
E : Type ?u.44126
F✝ : Type ?u.44129
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F✝
inst✝ : Module ℝ F✝
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ↑(OrthonormalBasis.reindex b e) = parallelepiped ↑b
F : ℝ → Fin 1 → ℝ := fun t _i => t
A : Icc 0 1 = F '' Icc 0 1
H : ↑(OrthonormalBasis.reindex b e) = fun x => -1
⊢ (fun a => ∑ x : Fin 1, a x * -1) '' ((fun a _i => a) '' Icc 0 1) = Icc (-1) 0
case inr.h
ι : Type u_1
ι' : Type ?u.44123
E : Type ?u.44126
F✝ : Type ?u.44129
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F✝
inst✝ : Module ℝ F✝
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ↑(OrthonormalBasis.reindex b e) = parallelepiped ↑b
F : ℝ → Fin 1 → ℝ := fun t _i => t
A : Icc 0 1 = F '' Icc 0 1
H : ↑(OrthonormalBasis.reindex b e) = fun x => -1
⊢ parallelepiped ↑(OrthonormalBasis.reindex b e) = Icc (-1) 0
simp_rw [H, parallelepiped, Algebra.id.smul_eq_mul, mul_one, A]
no goals
case inr.h
ι : Type u_1
ι' : Type ?u.44123
E : Type ?u.44126
F✝ : Type ?u.44129
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F✝
inst✝ : Module ℝ F✝
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ↑(OrthonormalBasis.reindex b e) = parallelepiped ↑b
F : ℝ → Fin 1 → ℝ := fun t _i => t
A : Icc 0 1 = F '' Icc 0 1
H : ↑(OrthonormalBasis.reindex b e) = fun x => -1
⊢ (fun a => ∑ x : Fin 1, a x * -1) '' ((fun a _i => a) '' Icc 0 1) = Icc (-1) 0
simp only [Finset.univ_unique, Fin.default_eq_zero, mul_neg, mul_one, Finset.sum_neg_distrib,
  Finset.sum_singleton, ← image_comp, Function.comp, image_neg, preimage_neg_Icc, neg_zero]