[GOAL]
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
v : ι → E
x : E
⊢ x ∈ parallelepiped v ↔ ∃ t _ht, x = ∑ i : ι, t i • v i
[PROOFSTEP]
simp [parallelepiped, eq_comm]
[GOAL]
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
f : E →ₗ[ℝ] F
v : ι → E
⊢ ↑f '' parallelepiped v = parallelepiped (↑f ∘ v)
[PROOFSTEP]
simp only [parallelepiped, ← image_comp]
[GOAL]
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
f : E →ₗ[ℝ] F
v : ι → E
⊢ ((fun a => ↑f a) ∘ fun t => ∑ i : ι, t i • v i) '' Icc 0 1 = (fun a => ∑ x : ι, a x • (↑f ∘ v) x) '' Icc 0 1
[PROOFSTEP]
congr 1 with t
[GOAL]
case h
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
f : E →ₗ[ℝ] F
v : ι → E
t : F
⊢ t ∈ ((fun a => ↑f a) ∘ fun t => ∑ i : ι, t i • v i) '' Icc 0 1 ↔ t ∈ (fun a => ∑ x : ι, a x • (↑f ∘ v) x) '' Icc 0 1
[PROOFSTEP]
simp only [Function.comp_apply, LinearMap.map_sum, LinearMap.map_smulₛₗ, RingHom.id_apply]
[GOAL]
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
v : ι → E
e : ι' ≃ ι
⊢ parallelepiped (v ∘ ↑e) = parallelepiped v
[PROOFSTEP]
simp only [parallelepiped]
[GOAL]
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
v : ι → E
e : ι' ≃ ι
⊢ (fun a => ∑ x : ι', a x • (v ∘ ↑e) x) '' Icc 0 1 = (fun t => ∑ i : ι, t i • v i) '' Icc 0 1
[PROOFSTEP]
let K : (ι' → ℝ) ≃ (ι → ℝ) := Equiv.piCongrLeft' (fun _a : ι' => ℝ) e
[GOAL]
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
v : ι → E
e : ι' ≃ ι
K : (ι' → ℝ) ≃ (ι → ℝ) := Equiv.piCongrLeft' (fun _a => ℝ) e
⊢ (fun a => ∑ x : ι', a x • (v ∘ ↑e) x) '' Icc 0 1 = (fun t => ∑ i : ι, t i • v i) '' Icc 0 1
[PROOFSTEP]
have : Icc (0 : ι → ℝ) 1 = K '' Icc (0 : ι' → ℝ) 1 :=
  by
  rw [← Equiv.preimage_eq_iff_eq_image]
  ext x
  simp only [mem_preimage, mem_Icc, Pi.le_def, Pi.zero_apply, Equiv.piCongrLeft'_apply, Pi.one_apply]
  refine' ⟨fun h => ⟨fun i => _, fun i => _⟩, fun h => ⟨fun i => h.1 (e.symm i), fun i => h.2 (e.symm i)⟩⟩
  · simpa only [Equiv.symm_apply_apply] using h.1 (e i)
  · simpa only [Equiv.symm_apply_apply] using h.2 (e i)
[GOAL]
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
v : ι → E
e : ι' ≃ ι
K : (ι' → ℝ) ≃ (ι → ℝ) := Equiv.piCongrLeft' (fun _a => ℝ) e
⊢ Icc 0 1 = ↑K '' Icc 0 1
[PROOFSTEP]
rw [← Equiv.preimage_eq_iff_eq_image]
[GOAL]
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
v : ι → E
e : ι' ≃ ι
K : (ι' → ℝ) ≃ (ι → ℝ) := Equiv.piCongrLeft' (fun _a => ℝ) e
⊢ ↑K ⁻¹' Icc 0 1 = Icc 0 1
[PROOFSTEP]
ext x
[GOAL]
case h
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
v : ι → E
e : ι' ≃ ι
K : (ι' → ℝ) ≃ (ι → ℝ) := Equiv.piCongrLeft' (fun _a => ℝ) e
x : ι' → ℝ
⊢ x ∈ ↑K ⁻¹' Icc 0 1 ↔ x ∈ Icc 0 1
[PROOFSTEP]
simp only [mem_preimage, mem_Icc, Pi.le_def, Pi.zero_apply, Equiv.piCongrLeft'_apply, Pi.one_apply]
[GOAL]
case h
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
v : ι → E
e : ι' ≃ ι
K : (ι' → ℝ) ≃ (ι → ℝ) := Equiv.piCongrLeft' (fun _a => ℝ) e
x : ι' → ℝ
⊢ ((∀ (i : ι), 0 ≤ x (↑e.symm i)) ∧ ∀ (i : ι), x (↑e.symm i) ≤ 1) ↔ (∀ (i : ι'), 0 ≤ x i) ∧ ∀ (i : ι'), x i ≤ 1
[PROOFSTEP]
refine' ⟨fun h => ⟨fun i => _, fun i => _⟩, fun h => ⟨fun i => h.1 (e.symm i), fun i => h.2 (e.symm i)⟩⟩
[GOAL]
case h.refine'_1
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
v : ι → E
e : ι' ≃ ι
K : (ι' → ℝ) ≃ (ι → ℝ) := Equiv.piCongrLeft' (fun _a => ℝ) e
x : ι' → ℝ
h : (∀ (i : ι), 0 ≤ x (↑e.symm i)) ∧ ∀ (i : ι), x (↑e.symm i) ≤ 1
i : ι'
⊢ 0 ≤ x i
[PROOFSTEP]
simpa only [Equiv.symm_apply_apply] using h.1 (e i)
[GOAL]
case h.refine'_2
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
v : ι → E
e : ι' ≃ ι
K : (ι' → ℝ) ≃ (ι → ℝ) := Equiv.piCongrLeft' (fun _a => ℝ) e
x : ι' → ℝ
h : (∀ (i : ι), 0 ≤ x (↑e.symm i)) ∧ ∀ (i : ι), x (↑e.symm i) ≤ 1
i : ι'
⊢ x i ≤ 1
[PROOFSTEP]
simpa only [Equiv.symm_apply_apply] using h.2 (e i)
[GOAL]
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
v : ι → E
e : ι' ≃ ι
K : (ι' → ℝ) ≃ (ι → ℝ) := Equiv.piCongrLeft' (fun _a => ℝ) e
this : Icc 0 1 = ↑K '' Icc 0 1
⊢ (fun a => ∑ x : ι', a x • (v ∘ ↑e) x) '' Icc 0 1 = (fun t => ∑ i : ι, t i • v i) '' Icc 0 1
[PROOFSTEP]
rw [this, ← image_comp]
[GOAL]
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
v : ι → E
e : ι' ≃ ι
K : (ι' → ℝ) ≃ (ι → ℝ) := Equiv.piCongrLeft' (fun _a => ℝ) e
this : Icc 0 1 = ↑K '' Icc 0 1
⊢ (fun a => ∑ x : ι', a x • (v ∘ ↑e) x) '' Icc 0 1 = (fun t => ∑ i : ι, t i • v i) ∘ ↑K '' Icc 0 1
[PROOFSTEP]
congr 1 with x
[GOAL]
case h
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
v : ι → E
e : ι' ≃ ι
K : (ι' → ℝ) ≃ (ι → ℝ) := Equiv.piCongrLeft' (fun _a => ℝ) e
this : Icc 0 1 = ↑K '' Icc 0 1
x : E
⊢ x ∈ (fun a => ∑ x : ι', a x • (v ∘ ↑e) x) '' Icc 0 1 ↔ x ∈ (fun t => ∑ i : ι, t i • v i) ∘ ↑K '' Icc 0 1
[PROOFSTEP]
have := fun z : ι' → ℝ => e.symm.sum_comp fun i => z i • v (e i)
[GOAL]
case h
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
v : ι → E
e : ι' ≃ ι
K : (ι' → ℝ) ≃ (ι → ℝ) := Equiv.piCongrLeft' (fun _a => ℝ) e
this✝ : Icc 0 1 = ↑K '' Icc 0 1
x : E
this : ∀ (z : ι' → ℝ), ∑ i : ι, z (↑e.symm i) • v (↑e (↑e.symm i)) = ∑ i : ι', z i • v (↑e i)
⊢ x ∈ (fun a => ∑ x : ι', a x • (v ∘ ↑e) x) '' Icc 0 1 ↔ x ∈ (fun t => ∑ i : ι, t i • v i) ∘ ↑K '' Icc 0 1
[PROOFSTEP]
simp_rw [Equiv.apply_symm_apply] at this 
[GOAL]
case h
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
v : ι → E
e : ι' ≃ ι
K : (ι' → ℝ) ≃ (ι → ℝ) := Equiv.piCongrLeft' (fun _a => ℝ) e
this✝ : Icc 0 1 = ↑K '' Icc 0 1
x : E
this : ∀ (z : ι' → ℝ), ∑ x : ι, z (↑e.symm x) • v x = ∑ x : ι', z x • v (↑e x)
⊢ x ∈ (fun a => ∑ x : ι', a x • (v ∘ ↑e) x) '' Icc 0 1 ↔ x ∈ (fun t => ∑ i : ι, t i • v i) ∘ ↑K '' Icc 0 1
[PROOFSTEP]
simp_rw [Function.comp_apply, mem_image, mem_Icc, Equiv.piCongrLeft'_apply, this]
[GOAL]
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
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
[PROOFSTEP]
have e : ι ≃ Fin 1 := by
  apply Fintype.equivFinOfCardEq
  simp only [← finrank_eq_card_basis b.toBasis, finrank_self]
[GOAL]
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
b : OrthonormalBasis ι ℝ ℝ
⊢ ι ≃ Fin 1
[PROOFSTEP]
apply Fintype.equivFinOfCardEq
[GOAL]
case h
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
b : OrthonormalBasis ι ℝ ℝ
⊢ Fintype.card ι = 1
[PROOFSTEP]
simp only [← finrank_eq_card_basis b.toBasis, finrank_self]
[GOAL]
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
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
[PROOFSTEP]
have B : parallelepiped (b.reindex e) = parallelepiped b :=
  by
  convert parallelepiped_comp_equiv b e.symm
  ext i
  simp only [OrthonormalBasis.coe_reindex]
[GOAL]
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
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
[PROOFSTEP]
convert parallelepiped_comp_equiv b e.symm
[GOAL]
case h.e'_2.h.e'_6
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
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
[PROOFSTEP]
ext i
[GOAL]
case h.e'_2.h.e'_6.h
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
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
[PROOFSTEP]
simp only [OrthonormalBasis.coe_reindex]
[GOAL]
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
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
[PROOFSTEP]
rw [← B]
[GOAL]
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
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
[PROOFSTEP]
let F : ℝ → Fin 1 → ℝ := fun t => fun _i => t
[GOAL]
ι : Type u_1
ι' : Type u_2
E : Type u_3
F✝ : Type u_4
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
[PROOFSTEP]
have A : Icc (0 : Fin 1 → ℝ) 1 = F '' Icc (0 : ℝ) 1 :=
  by
  apply Subset.antisymm
  · intro x hx
    refine' ⟨x 0, ⟨hx.1 0, hx.2 0⟩, _⟩
    ext j
    simp only [Subsingleton.elim j 0]
  · rintro x ⟨y, hy, rfl⟩
    exact ⟨fun _j => hy.1, fun _j => hy.2⟩
[GOAL]
ι : Type u_1
ι' : Type u_2
E : Type u_3
F✝ : Type u_4
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
[PROOFSTEP]
apply Subset.antisymm
[GOAL]
case h₁
ι : Type u_1
ι' : Type u_2
E : Type u_3
F✝ : Type u_4
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
[PROOFSTEP]
intro x hx
[GOAL]
case h₁
ι : Type u_1
ι' : Type u_2
E : Type u_3
F✝ : Type u_4
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
[PROOFSTEP]
refine' ⟨x 0, ⟨hx.1 0, hx.2 0⟩, _⟩
[GOAL]
case h₁
ι : Type u_1
ι' : Type u_2
E : Type u_3
F✝ : Type u_4
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
[PROOFSTEP]
ext j
[GOAL]
case h₁.h
ι : Type u_1
ι' : Type u_2
E : Type u_3
F✝ : Type u_4
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
[PROOFSTEP]
simp only [Subsingleton.elim j 0]
[GOAL]
case h₂
ι : Type u_1
ι' : Type u_2
E : Type u_3
F✝ : Type u_4
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
[PROOFSTEP]
rintro x ⟨y, hy, rfl⟩
[GOAL]
case h₂.intro.intro
ι : Type u_1
ι' : Type u_2
E : Type u_3
F✝ : Type u_4
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
[PROOFSTEP]
exact ⟨fun _j => hy.1, fun _j => hy.2⟩
[GOAL]
ι : Type u_1
ι' : Type u_2
E : Type u_3
F✝ : Type u_4
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
[PROOFSTEP]
rcases orthonormalBasis_one_dim (b.reindex e) with (H | H)
[GOAL]
case inl
ι : Type u_1
ι' : Type u_2
E : Type u_3
F✝ : Type u_4
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
[PROOFSTEP]
left
[GOAL]
case inl.h
ι : Type u_1
ι' : Type u_2
E : Type u_3
F✝ : Type u_4
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
[PROOFSTEP]
simp_rw [parallelepiped, H, A, Algebra.id.smul_eq_mul, mul_one]
[GOAL]
case inl.h
ι : Type u_1
ι' : Type u_2
E : Type u_3
F✝ : Type u_4
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
[PROOFSTEP]
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]
[GOAL]
case inr
ι : Type u_1
ι' : Type u_2
E : Type u_3
F✝ : Type u_4
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
[PROOFSTEP]
right
[GOAL]
case inr.h
ι : Type u_1
ι' : Type u_2
E : Type u_3
F✝ : Type u_4
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
[PROOFSTEP]
simp_rw [H, parallelepiped, Algebra.id.smul_eq_mul, A]
[GOAL]
case inr.h
ι : Type u_1
ι' : Type u_2
E : Type u_3
F✝ : Type u_4
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
[PROOFSTEP]
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]
[GOAL]
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
v : ι → E
⊢ parallelepiped v = ∑ i : ι, segment ℝ 0 (v i)
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
v : ι → E
x✝ : E
⊢ x✝ ∈ parallelepiped v ↔ x✝ ∈ ∑ i : ι, segment ℝ 0 (v i)
[PROOFSTEP]
simp only [mem_parallelepiped_iff, Set.mem_finset_sum, Finset.mem_univ, forall_true_left, segment_eq_image, smul_zero,
  zero_add, ← Set.pi_univ_Icc, Set.mem_univ_pi]
[GOAL]
case h
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
v : ι → E
x✝ : E
⊢ (∃ t h, x✝ = ∑ i : ι, t i • v i) ↔ ∃ g h, ∑ i : ι, g i = x✝
[PROOFSTEP]
constructor
[GOAL]
case h.mp
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
v : ι → E
x✝ : E
⊢ (∃ t h, x✝ = ∑ i : ι, t i • v i) → ∃ g h, ∑ i : ι, g i = x✝
[PROOFSTEP]
rintro ⟨t, ht, rfl⟩
[GOAL]
case h.mp.intro.intro
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
v : ι → E
t : ι → ℝ
ht : ∀ (i : ι), t i ∈ Icc (OfNat.ofNat 0 i) (OfNat.ofNat 1 i)
⊢ ∃ g h, ∑ i : ι, g i = ∑ i : ι, t i • v i
[PROOFSTEP]
exact ⟨t • v, fun {i} => ⟨t i, ht _, by simp⟩, rfl⟩
[GOAL]
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
v : ι → E
t : ι → ℝ
ht : ∀ (i : ι), t i ∈ Icc (OfNat.ofNat 0 i) (OfNat.ofNat 1 i)
i : ι
⊢ (fun a => a • v i) (t i) = (t • v) i
[PROOFSTEP]
simp
[GOAL]
case h.mpr
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
v : ι → E
x✝ : E
⊢ (∃ g h, ∑ i : ι, g i = x✝) → ∃ t h, x✝ = ∑ i : ι, t i • v i
[PROOFSTEP]
rintro ⟨g, hg, rfl⟩
[GOAL]
case h.mpr.intro.intro
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
v g : ι → E
hg : ∀ {i : ι}, g i ∈ (fun a => a • v i) '' Icc 0 1
⊢ ∃ t h, ∑ i : ι, g i = ∑ i : ι, t i • v i
[PROOFSTEP]
choose t ht hg using @hg
[GOAL]
case h.mpr.intro.intro
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
v g : ι → E
t : {i : ι} → ℝ
ht : ∀ {i : ι}, t ∈ Icc 0 1
hg : ∀ {i : ι}, (fun a => a • v i) t = g i
⊢ ∃ t h, ∑ i : ι, g i = ∑ i : ι, t i • v i
[PROOFSTEP]
refine ⟨@t, @ht, ?_⟩
[GOAL]
case h.mpr.intro.intro
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
v g : ι → E
t : {i : ι} → ℝ
ht : ∀ {i : ι}, t ∈ Icc 0 1
hg : ∀ {i : ι}, (fun a => a • v i) t = g i
⊢ ∑ i : ι, g i = ∑ i : ι, t • v i
[PROOFSTEP]
simp_rw [hg]
[GOAL]
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
v : ι → E
⊢ Convex ℝ (parallelepiped v)
[PROOFSTEP]
rw [parallelepiped_eq_sum_segment]
[GOAL]
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
v : ι → E
⊢ Convex ℝ (∑ i : ι, segment ℝ 0 (v i))
[PROOFSTEP]
exact convex_sum _ fun _i _hi => convex_segment _ _
[GOAL]
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
v : ι → E
⊢ parallelepiped v = ↑(convexHull ℝ) (∑ i : ι, {0, v i})
[PROOFSTEP]
simp_rw [convexHull_sum, convexHull_pair, parallelepiped_eq_sum_segment]
[GOAL]
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype ι'
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : AddCommGroup F
inst✝¹ : Module ℝ F
inst✝ : DecidableEq ι
a : ι → ℝ
⊢ (parallelepiped fun i => Pi.single i (a i)) = uIcc 0 a
[PROOFSTEP]
ext x
[GOAL]
case h
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype ι'
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : AddCommGroup F
inst✝¹ : Module ℝ F
inst✝ : DecidableEq ι
a x : ι → ℝ
⊢ (x ∈ parallelepiped fun i => Pi.single i (a i)) ↔ x ∈ uIcc 0 a
[PROOFSTEP]
simp_rw [Set.uIcc, mem_parallelepiped_iff, Set.mem_Icc, Pi.le_def, ← forall_and, Pi.inf_apply, Pi.sup_apply, ←
  Pi.single_smul', Pi.one_apply, Pi.zero_apply, ← Pi.smul_apply', Finset.univ_sum_single (_ : ι → ℝ)]
[GOAL]
case h
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype ι'
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : AddCommGroup F
inst✝¹ : Module ℝ F
inst✝ : DecidableEq ι
a x : ι → ℝ
⊢ (∃ t h, x = fun i => (t • a) i) ↔ ∀ (x_1 : ι), 0 ⊓ a x_1 ≤ x x_1 ∧ x x_1 ≤ 0 ⊔ a x_1
[PROOFSTEP]
constructor
[GOAL]
case h.mp
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype ι'
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : AddCommGroup F
inst✝¹ : Module ℝ F
inst✝ : DecidableEq ι
a x : ι → ℝ
⊢ (∃ t h, x = fun i => (t • a) i) → ∀ (x_1 : ι), 0 ⊓ a x_1 ≤ x x_1 ∧ x x_1 ≤ 0 ⊔ a x_1
[PROOFSTEP]
rintro ⟨t, ht, rfl⟩ i
[GOAL]
case h.mp.intro.intro
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype ι'
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : AddCommGroup F
inst✝¹ : Module ℝ F
inst✝ : DecidableEq ι
a t : ι → ℝ
ht : ∀ (x : ι), 0 ≤ t x ∧ t x ≤ 1
i : ι
⊢ 0 ⊓ a i ≤ (fun i => (t • a) i) i ∧ (fun i => (t • a) i) i ≤ 0 ⊔ a i
[PROOFSTEP]
specialize ht i
[GOAL]
case h.mp.intro.intro
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype ι'
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : AddCommGroup F
inst✝¹ : Module ℝ F
inst✝ : DecidableEq ι
a t : ι → ℝ
i : ι
ht : 0 ≤ t i ∧ t i ≤ 1
⊢ 0 ⊓ a i ≤ (fun i => (t • a) i) i ∧ (fun i => (t • a) i) i ≤ 0 ⊔ a i
[PROOFSTEP]
simp_rw [smul_eq_mul, Pi.mul_apply]
[GOAL]
case h.mp.intro.intro
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype ι'
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : AddCommGroup F
inst✝¹ : Module ℝ F
inst✝ : DecidableEq ι
a t : ι → ℝ
i : ι
ht : 0 ≤ t i ∧ t i ≤ 1
⊢ 0 ⊓ a i ≤ t i * a i ∧ t i * a i ≤ 0 ⊔ a i
[PROOFSTEP]
cases' le_total (a i) 0 with hai hai
[GOAL]
case h.mp.intro.intro.inl
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype ι'
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : AddCommGroup F
inst✝¹ : Module ℝ F
inst✝ : DecidableEq ι
a t : ι → ℝ
i : ι
ht : 0 ≤ t i ∧ t i ≤ 1
hai : a i ≤ 0
⊢ 0 ⊓ a i ≤ t i * a i ∧ t i * a i ≤ 0 ⊔ a i
[PROOFSTEP]
rw [sup_eq_left.mpr hai, inf_eq_right.mpr hai]
[GOAL]
case h.mp.intro.intro.inl
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype ι'
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : AddCommGroup F
inst✝¹ : Module ℝ F
inst✝ : DecidableEq ι
a t : ι → ℝ
i : ι
ht : 0 ≤ t i ∧ t i ≤ 1
hai : a i ≤ 0
⊢ a i ≤ t i * a i ∧ t i * a i ≤ 0
[PROOFSTEP]
exact ⟨le_mul_of_le_one_left hai ht.2, mul_nonpos_of_nonneg_of_nonpos ht.1 hai⟩
[GOAL]
case h.mp.intro.intro.inr
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype ι'
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : AddCommGroup F
inst✝¹ : Module ℝ F
inst✝ : DecidableEq ι
a t : ι → ℝ
i : ι
ht : 0 ≤ t i ∧ t i ≤ 1
hai : 0 ≤ a i
⊢ 0 ⊓ a i ≤ t i * a i ∧ t i * a i ≤ 0 ⊔ a i
[PROOFSTEP]
rw [sup_eq_right.mpr hai, inf_eq_left.mpr hai]
[GOAL]
case h.mp.intro.intro.inr
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype ι'
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : AddCommGroup F
inst✝¹ : Module ℝ F
inst✝ : DecidableEq ι
a t : ι → ℝ
i : ι
ht : 0 ≤ t i ∧ t i ≤ 1
hai : 0 ≤ a i
⊢ 0 ≤ t i * a i ∧ t i * a i ≤ a i
[PROOFSTEP]
exact ⟨mul_nonneg ht.1 hai, mul_le_of_le_one_left hai ht.2⟩
[GOAL]
case h.mpr
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype ι'
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : AddCommGroup F
inst✝¹ : Module ℝ F
inst✝ : DecidableEq ι
a x : ι → ℝ
⊢ (∀ (x_1 : ι), 0 ⊓ a x_1 ≤ x x_1 ∧ x x_1 ≤ 0 ⊔ a x_1) → ∃ t h, x = fun i => (t • a) i
[PROOFSTEP]
intro h
[GOAL]
case h.mpr
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype ι'
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : AddCommGroup F
inst✝¹ : Module ℝ F
inst✝ : DecidableEq ι
a x : ι → ℝ
h : ∀ (x_1 : ι), 0 ⊓ a x_1 ≤ x x_1 ∧ x x_1 ≤ 0 ⊔ a x_1
⊢ ∃ t h, x = fun i => (t • a) i
[PROOFSTEP]
refine' ⟨fun i => x i / a i, fun i => _, funext fun i => _⟩
[GOAL]
case h.mpr.refine'_1
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype ι'
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : AddCommGroup F
inst✝¹ : Module ℝ F
inst✝ : DecidableEq ι
a x : ι → ℝ
h : ∀ (x_1 : ι), 0 ⊓ a x_1 ≤ x x_1 ∧ x x_1 ≤ 0 ⊔ a x_1
i : ι
⊢ 0 ≤ (fun i => x i / a i) i ∧ (fun i => x i / a i) i ≤ 1
[PROOFSTEP]
specialize h i
[GOAL]
case h.mpr.refine'_1
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype ι'
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : AddCommGroup F
inst✝¹ : Module ℝ F
inst✝ : DecidableEq ι
a x : ι → ℝ
i : ι
h : 0 ⊓ a i ≤ x i ∧ x i ≤ 0 ⊔ a i
⊢ 0 ≤ (fun i => x i / a i) i ∧ (fun i => x i / a i) i ≤ 1
[PROOFSTEP]
cases' le_total (a i) 0 with hai hai
[GOAL]
case h.mpr.refine'_1.inl
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype ι'
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : AddCommGroup F
inst✝¹ : Module ℝ F
inst✝ : DecidableEq ι
a x : ι → ℝ
i : ι
h : 0 ⊓ a i ≤ x i ∧ x i ≤ 0 ⊔ a i
hai : a i ≤ 0
⊢ 0 ≤ (fun i => x i / a i) i ∧ (fun i => x i / a i) i ≤ 1
[PROOFSTEP]
rw [sup_eq_left.mpr hai, inf_eq_right.mpr hai] at h 
[GOAL]
case h.mpr.refine'_1.inl
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype ι'
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : AddCommGroup F
inst✝¹ : Module ℝ F
inst✝ : DecidableEq ι
a x : ι → ℝ
i : ι
h : a i ≤ x i ∧ x i ≤ 0
hai : a i ≤ 0
⊢ 0 ≤ (fun i => x i / a i) i ∧ (fun i => x i / a i) i ≤ 1
[PROOFSTEP]
exact ⟨div_nonneg_of_nonpos h.2 hai, div_le_one_of_ge h.1 hai⟩
[GOAL]
case h.mpr.refine'_1.inr
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype ι'
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : AddCommGroup F
inst✝¹ : Module ℝ F
inst✝ : DecidableEq ι
a x : ι → ℝ
i : ι
h : 0 ⊓ a i ≤ x i ∧ x i ≤ 0 ⊔ a i
hai : 0 ≤ a i
⊢ 0 ≤ (fun i => x i / a i) i ∧ (fun i => x i / a i) i ≤ 1
[PROOFSTEP]
rw [sup_eq_right.mpr hai, inf_eq_left.mpr hai] at h 
[GOAL]
case h.mpr.refine'_1.inr
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype ι'
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : AddCommGroup F
inst✝¹ : Module ℝ F
inst✝ : DecidableEq ι
a x : ι → ℝ
i : ι
h : 0 ≤ x i ∧ x i ≤ a i
hai : 0 ≤ a i
⊢ 0 ≤ (fun i => x i / a i) i ∧ (fun i => x i / a i) i ≤ 1
[PROOFSTEP]
exact ⟨div_nonneg h.1 hai, div_le_one_of_le h.2 hai⟩
[GOAL]
case h.mpr.refine'_2
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype ι'
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : AddCommGroup F
inst✝¹ : Module ℝ F
inst✝ : DecidableEq ι
a x : ι → ℝ
h : ∀ (x_1 : ι), 0 ⊓ a x_1 ≤ x x_1 ∧ x x_1 ≤ 0 ⊔ a x_1
i : ι
⊢ x i = ((fun i => x i / a i) • a) i
[PROOFSTEP]
specialize h i
[GOAL]
case h.mpr.refine'_2
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype ι'
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : AddCommGroup F
inst✝¹ : Module ℝ F
inst✝ : DecidableEq ι
a x : ι → ℝ
i : ι
h : 0 ⊓ a i ≤ x i ∧ x i ≤ 0 ⊔ a i
⊢ x i = ((fun i => x i / a i) • a) i
[PROOFSTEP]
simp only [smul_eq_mul, Pi.mul_apply]
[GOAL]
case h.mpr.refine'_2
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype ι'
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : AddCommGroup F
inst✝¹ : Module ℝ F
inst✝ : DecidableEq ι
a x : ι → ℝ
i : ι
h : 0 ⊓ a i ≤ x i ∧ x i ≤ 0 ⊔ a i
⊢ x i = x i / a i * a i
[PROOFSTEP]
cases' eq_or_ne (a i) 0 with hai hai
[GOAL]
case h.mpr.refine'_2.inl
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype ι'
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : AddCommGroup F
inst✝¹ : Module ℝ F
inst✝ : DecidableEq ι
a x : ι → ℝ
i : ι
h : 0 ⊓ a i ≤ x i ∧ x i ≤ 0 ⊔ a i
hai : a i = 0
⊢ x i = x i / a i * a i
[PROOFSTEP]
rw [hai, inf_idem, sup_idem, ← le_antisymm_iff] at h 
[GOAL]
case h.mpr.refine'_2.inl
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype ι'
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : AddCommGroup F
inst✝¹ : Module ℝ F
inst✝ : DecidableEq ι
a x : ι → ℝ
i : ι
h : 0 = x i
hai : a i = 0
⊢ x i = x i / a i * a i
[PROOFSTEP]
rw [hai, ← h, zero_div, zero_mul]
[GOAL]
case h.mpr.refine'_2.inr
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype ι'
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : AddCommGroup F
inst✝¹ : Module ℝ F
inst✝ : DecidableEq ι
a x : ι → ℝ
i : ι
h : 0 ⊓ a i ≤ x i ∧ x i ≤ 0 ⊔ a i
hai : a i ≠ 0
⊢ x i = x i / a i * a i
[PROOFSTEP]
rw [div_mul_cancel _ hai]
[GOAL]
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
b : Basis ι ℝ E
⊢ Set.Nonempty
    (interior
      { carrier := _root_.parallelepiped ↑b,
          isCompact' := (_ : IsCompact ((fun t => ∑ i : ι, t i • ↑b i) '' Icc 0 1)) }.carrier)
[PROOFSTEP]
suffices H : Set.Nonempty (interior (b.equivFunL.symm.toHomeomorph '' Icc 0 1))
[GOAL]
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
b : Basis ι ℝ E
H :
  Set.Nonempty (interior (↑(ContinuousLinearEquiv.toHomeomorph (ContinuousLinearEquiv.symm (equivFunL b))) '' Icc 0 1))
⊢ Set.Nonempty
    (interior
      { carrier := _root_.parallelepiped ↑b,
          isCompact' := (_ : IsCompact ((fun t => ∑ i : ι, t i • ↑b i) '' Icc 0 1)) }.carrier)
[PROOFSTEP]
dsimp only [_root_.parallelepiped]
[GOAL]
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
b : Basis ι ℝ E
H :
  Set.Nonempty (interior (↑(ContinuousLinearEquiv.toHomeomorph (ContinuousLinearEquiv.symm (equivFunL b))) '' Icc 0 1))
⊢ Set.Nonempty (interior ((fun t => ∑ i : ι, t i • ↑b i) '' Icc 0 1))
[PROOFSTEP]
convert H
[GOAL]
case h.e'_2.h.e'_3.h
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
b : Basis ι ℝ E
H :
  Set.Nonempty (interior (↑(ContinuousLinearEquiv.toHomeomorph (ContinuousLinearEquiv.symm (equivFunL b))) '' Icc 0 1))
a✝¹ : ι → ℝ
a✝ : a✝¹ ∈ Icc 0 1
⊢ ∑ i : ι, a✝¹ i • ↑b i = ↑(ContinuousLinearEquiv.toHomeomorph (ContinuousLinearEquiv.symm (equivFunL b))) a✝¹
[PROOFSTEP]
exact (b.equivFun_symm_apply _).symm
[GOAL]
case H
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
b : Basis ι ℝ E
⊢ Set.Nonempty (interior (↑(ContinuousLinearEquiv.toHomeomorph (ContinuousLinearEquiv.symm (equivFunL b))) '' Icc 0 1))
[PROOFSTEP]
have A : Set.Nonempty (interior (Icc (0 : ι → ℝ) 1)) :=
  by
  rw [← pi_univ_Icc, interior_pi_set (@finite_univ ι _)]
  simp only [univ_pi_nonempty_iff, Pi.zero_apply, Pi.one_apply, interior_Icc, nonempty_Ioo, zero_lt_one, imp_true_iff]
[GOAL]
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
b : Basis ι ℝ E
⊢ Set.Nonempty (interior (Icc 0 1))
[PROOFSTEP]
rw [← pi_univ_Icc, interior_pi_set (@finite_univ ι _)]
[GOAL]
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
b : Basis ι ℝ E
⊢ Set.Nonempty (pi univ fun i => interior (Icc (OfNat.ofNat 0 i) (OfNat.ofNat 1 i)))
[PROOFSTEP]
simp only [univ_pi_nonempty_iff, Pi.zero_apply, Pi.one_apply, interior_Icc, nonempty_Ioo, zero_lt_one, imp_true_iff]
[GOAL]
case H
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
b : Basis ι ℝ E
A : Set.Nonempty (interior (Icc 0 1))
⊢ Set.Nonempty (interior (↑(ContinuousLinearEquiv.toHomeomorph (ContinuousLinearEquiv.symm (equivFunL b))) '' Icc 0 1))
[PROOFSTEP]
rwa [← Homeomorph.image_interior, nonempty_image_iff]
[GOAL]
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁷ : Fintype ι
inst✝⁶ : Fintype ι'
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ F
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
b : Basis ι ℝ E
⊢ IsAddHaarMeasure (Basis.addHaar b)
[PROOFSTEP]
rw [Basis.addHaar]
[GOAL]
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁷ : Fintype ι
inst✝⁶ : Fintype ι'
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ F
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
b : Basis ι ℝ E
⊢ IsAddHaarMeasure (addHaarMeasure (Basis.parallelepiped b))
[PROOFSTEP]
exact Measure.isAddHaarMeasure_addHaarMeasure _
[GOAL]
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁷ : Fintype ι
inst✝⁶ : Fintype ι'
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ F
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
b : Basis ι ℝ E
⊢ ↑↑(addHaar b) (_root_.parallelepiped ↑b) = 1
[PROOFSTEP]
rw [Basis.addHaar]
[GOAL]
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁷ : Fintype ι
inst✝⁶ : Fintype ι'
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ F
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
b : Basis ι ℝ E
⊢ ↑↑(addHaarMeasure (parallelepiped b)) (_root_.parallelepiped ↑b) = 1
[PROOFSTEP]
exact addHaarMeasure_self
[GOAL]
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Fintype ι
inst✝ : Fintype ι'
⊢ MeasureSpace ℝ
[PROOFSTEP]
infer_instance
