case h
ι : Type u_2
ι' : Type ?u.72644
E : Type u_1
F : Type ?u.72650
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)
ι : Type u_2
ι' : Type ?u.72644
E : Type u_1
F : Type ?u.72650
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)
ext
case h
ι : Type u_2
ι' : Type ?u.72644
E : Type u_1
F : Type ?u.72650
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✝
case h
ι : Type u_2
ι' : Type ?u.72644
E : Type u_1
F : Type ?u.72650
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)
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]
case h.mp
ι : Type u_2
ι' : Type ?u.72644
E : Type u_1
F : Type ?u.72650
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✝

case h.mpr
ι : Type u_2
ι' : Type ?u.72644
E : Type u_1
F : Type ?u.72650
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
case h
ι : Type u_2
ι' : Type ?u.72644
E : Type u_1
F : Type ?u.72650
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✝
constructor
case h.mpr.intro.intro
ι : Type u_2
ι' : Type ?u.72644
E : Type u_1
F : Type ?u.72650
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
case h.mpr
ι : Type u_2
ι' : Type ?u.72644
E : Type u_1
F : Type ?u.72650
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
rintro ⟨g, hg, rfl⟩
case h.mpr.intro.intro
ι : Type u_2
ι' : Type ?u.72644
E : Type u_1
F : Type ?u.72650
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
case h.mpr.intro.intro
ι : Type u_2
ι' : Type ?u.72644
E : Type u_1
F : Type ?u.72650
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
choose t ht hg using @hg
case h.mpr.intro.intro
ι : Type u_2
ι' : Type ?u.72644
E : Type u_1
F : Type ?u.72650
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
case h.mpr.intro.intro
ι : Type u_2
ι' : Type ?u.72644
E : Type u_1
F : Type ?u.72650
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
refine ⟨@t, @ht, ?_⟩
no goals
case h.mpr.intro.intro
ι : Type u_2
ι' : Type ?u.72644
E : Type u_1
F : Type ?u.72650
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
simp_rw [hg]
case h.mp.intro.intro
ι : Type u_2
ι' : Type ?u.72644
E : Type u_1
F : Type ?u.72650
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
case h.mp
ι : Type u_2
ι' : Type ?u.72644
E : Type u_1
F : Type ?u.72650
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✝
rintro ⟨t, ht, rfl⟩
no goals
case h.mp.intro.intro
ι : Type u_2
ι' : Type ?u.72644
E : Type u_1
F : Type ?u.72650
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
exact ⟨t • v, fun {i} => ⟨t i, ht _, by simp⟩, rfl⟩
no goals
ι : Type u_2
ι' : Type ?u.72644
E : Type u_1
F : Type ?u.72650
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
simp