-- Mathlib/MeasureTheory/Measure/Haar/OfBasis.lean
theorem parallelepiped_eq_sum_segment (v : ι → E) : parallelepiped v = ∑ i, segment ℝ 0 (v i)

Proof state:
ι : Type u_1
E : Type u_3
inst✝² : Fintype ι
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
v : ι → E
⊢ parallelepiped v = ∑ i : ι, segment ℝ 0 (v i)

Tactic:
ext

Result:
case h
ι : Type u_1
E : Type u_3
inst✝² : Fintype ι
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
v : ι → E
x✝ : E
⊢ x✝ ∈ parallelepiped v ↔ x✝ ∈ ∑ i : ι, segment ℝ 0 (v i)

Proof state:
ι : Type u_1
E : Type u_3
inst✝² : Fintype ι
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
v : ι → E
t : ι → ℝ
ht : ∀ (i : ι), t i ∈ Icc (0 i) (1 i)
i : ι
⊢ (fun a => a • v i) (t i) = (t • v) i

Tactic:
simp

Result:
no goals

Proof state:
case h.mpr.intro.intro
ι : Type u_1
E : Type u_3
inst✝² : Fintype ι
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
v g : ι → E
hg : ∀ {i : ι}, g i ∈ (fun a => a • v i) '' Icc 0 1
⊢ ∃ t, (∀ (i : ι), t i ∈ Icc (0 i) (1 i)) ∧ ∑ i : ι, g i = ∑ i : ι, t i • v i

Tactic:
choose t ht hg using @hg

Result:
case h.mpr.intro.intro
ι : Type u_1
E : Type u_3
inst✝² : Fintype ι
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
v g : ι → E
t : {i : ι} → ℝ
ht : ∀ {i : ι}, t ∈ Icc 0 1
hg : ∀ {i : ι}, (fun a => a • v i) t = g i
⊢ ∃ t, (∀ (i : ι), t i ∈ Icc (0 i) (1 i)) ∧ ∑ i : ι, g i = ∑ i : ι, t i • v i

Proof state:
case h.mpr.intro.intro
ι : Type u_1
E : Type u_3
inst✝² : Fintype ι
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
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

Tactic:
simp_rw [hg]

Result:
no goals

Proof state:
case h.mpr
ι : Type u_1
E : Type u_3
inst✝² : Fintype ι
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
v : ι → E
x✝ : E
⊢ (∃ g, ∃ (_ : ∀ {i : ι}, g i ∈ (fun a => a • v i) '' Icc 0 1), ∑ i : ι, g i = x✝) →
    ∃ t, (∀ (i : ι), t i ∈ Icc (0 i) (1 i)) ∧ x✝ = ∑ i : ι, t i • v i

Tactic:
rintro ⟨g, hg, rfl⟩

Result:
case h.mpr.intro.intro
ι : Type u_1
E : Type u_3
inst✝² : Fintype ι
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
v g : ι → E
hg : ∀ {i : ι}, g i ∈ (fun a => a • v i) '' Icc 0 1
⊢ ∃ t, (∀ (i : ι), t i ∈ Icc (0 i) (1 i)) ∧ ∑ i : ι, g i = ∑ i : ι, t i • v i

Proof state:
case h.mp.intro.intro
ι : Type u_1
E : Type u_3
inst✝² : Fintype ι
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
v : ι → E
t : ι → ℝ
ht : ∀ (i : ι), t i ∈ Icc (0 i) (1 i)
⊢ ∃ g, ∃ (_ : ∀ {i : ι}, g i ∈ (fun a => a • v i) '' Icc 0 1), ∑ i : ι, g i = ∑ i : ι, t i • v i

Tactic:
exact ⟨t • v, fun {i} => ⟨t i, ht _, by simp⟩, rfl⟩

Result:
no goals

Proof state:
case h.mp
ι : Type u_1
E : Type u_3
inst✝² : Fintype ι
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
v : ι → E
x✝ : E
⊢ (∃ t, (∀ (i : ι), t i ∈ Icc (0 i) (1 i)) ∧ x✝ = ∑ i : ι, t i • v i) →
    ∃ g, ∃ (_ : ∀ {i : ι}, g i ∈ (fun a => a • v i) '' Icc 0 1), ∑ i : ι, g i = x✝

Tactic:
rintro ⟨t, ht, rfl⟩

Result:
case h.mp.intro.intro
ι : Type u_1
E : Type u_3
inst✝² : Fintype ι
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
v : ι → E
t : ι → ℝ
ht : ∀ (i : ι), t i ∈ Icc (0 i) (1 i)
⊢ ∃ g, ∃ (_ : ∀ {i : ι}, g i ∈ (fun a => a • v i) '' Icc 0 1), ∑ i : ι, g i = ∑ i : ι, t i • v i

Proof state:
case h.mpr.intro.intro
ι : Type u_1
E : Type u_3
inst✝² : Fintype ι
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
v g : ι → E
t : {i : ι} → ℝ
ht : ∀ {i : ι}, t ∈ Icc 0 1
hg : ∀ {i : ι}, (fun a => a • v i) t = g i
⊢ ∃ t, (∀ (i : ι), t i ∈ Icc (0 i) (1 i)) ∧ ∑ i : ι, g i = ∑ i : ι, t i • v i

Tactic:
refine ⟨@t, @ht, ?_⟩

Result:
case h.mpr.intro.intro
ι : Type u_1
E : Type u_3
inst✝² : Fintype ι
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
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

Proof state:
case h
ι : Type u_1
E : Type u_3
inst✝² : Fintype ι
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
v : ι → E
x✝ : E
⊢ (∃ t, (∀ (i : ι), t i ∈ Icc (0 i) (1 i)) ∧ x✝ = ∑ i : ι, t i • v i) ↔
    ∃ g, ∃ (_ : ∀ {i : ι}, g i ∈ (fun a => a • v i) '' Icc 0 1), ∑ i : ι, g i = x✝

Tactic:
constructor

Result:
case h.mp
ι : Type u_1
E : Type u_3
inst✝² : Fintype ι
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
v : ι → E
x✝ : E
⊢ (∃ t, (∀ (i : ι), t i ∈ Icc (0 i) (1 i)) ∧ x✝ = ∑ i : ι, t i • v i) →
    ∃ g, ∃ (_ : ∀ {i : ι}, g i ∈ (fun a => a • v i) '' Icc 0 1), ∑ i : ι, g i = x✝

case h.mpr
ι : Type u_1
E : Type u_3
inst✝² : Fintype ι
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
v : ι → E
x✝ : E
⊢ (∃ g, ∃ (_ : ∀ {i : ι}, g i ∈ (fun a => a • v i) '' Icc 0 1), ∑ i : ι, g i = x✝) →
    ∃ t, (∀ (i : ι), t i ∈ Icc (0 i) (1 i)) ∧ x✝ = ∑ i : ι, t i • v i

Proof state:
case h
ι : Type u_1
E : Type u_3
inst✝² : Fintype ι
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
v : ι → E
x✝ : E
⊢ x✝ ∈ parallelepiped v ↔ x✝ ∈ ∑ i : ι, segment ℝ 0 (v i)

Tactic:
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]

Result:
case h
ι : Type u_1
E : Type u_3
inst✝² : Fintype ι
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
v : ι → E
x✝ : E
⊢ (∃ t, (∀ (i : ι), t i ∈ Icc (0 i) (1 i)) ∧ x✝ = ∑ i : ι, t i • v i) ↔
    ∃ g, ∃ (_ : ∀ {i : ι}, g i ∈ (fun a => a • v i) '' Icc 0 1), ∑ i : ι, g i = x✝