-- Mathlib/MeasureTheory/Measure/Haar/OfBasis.lean
theorem parallelepiped_orthonormalBasis_one_dim (b : OrthonormalBasis ι ℝ ℝ) :
    parallelepiped b = Icc 0 1 ∨ parallelepiped b = Icc (-1) 0

Proof state:
case h
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
⊢ Fintype.card ι = 1

Tactic:
simp only [← finrank_eq_card_basis b.toBasis, finrank_self]

Result:
no goals

Proof state:
case inl
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ⇑(b.reindex e) = parallelepiped ⇑b
F : ℝ → Fin 1 → ℝ := fun t _i => t
A : Icc 0 1 = F '' Icc 0 1
H : ⇑(b.reindex e) = fun x => 1
⊢ parallelepiped ⇑(b.reindex e) = Icc 0 1 ∨ parallelepiped ⇑(b.reindex e) = Icc (-1) 0

Tactic:
left

Result:
case inl.h
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ⇑(b.reindex e) = parallelepiped ⇑b
F : ℝ → Fin 1 → ℝ := fun t _i => t
A : Icc 0 1 = F '' Icc 0 1
H : ⇑(b.reindex e) = fun x => 1
⊢ parallelepiped ⇑(b.reindex e) = Icc 0 1

Proof state:
case h.e'_2.h.e'_6.h
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
i : Fin 1
⊢ (b.reindex e) i = (⇑b ∘ ⇑e.symm) i

Tactic:
simp only [OrthonormalBasis.coe_reindex]

Result:
no goals

Proof state:
case inl.h
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ⇑(b.reindex e) = parallelepiped ⇑b
F : ℝ → Fin 1 → ℝ := fun t _i => t
A : Icc 0 1 = F '' Icc 0 1
H : ⇑(b.reindex e) = fun x => 1
⊢ (fun a => ∑ x : Fin 1, a x) '' (F '' Icc 0 1) = Icc 0 1

Tactic:
simp only [F, Finset.univ_unique, Fin.default_eq_zero, Finset.sum_singleton,
  ← image_comp, Function.comp_apply, image_id']

Result:
no goals

Proof state:
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
⊢ parallelepiped ⇑b = Icc 0 1 ∨ parallelepiped ⇑b = Icc (-1) 0

Tactic:
have e : ι ≃ Fin 1 := by
  apply Fintype.equivFinOfCardEq
  simp only [← finrank_eq_card_basis b.toBasis, finrank_self]

Result:
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
⊢ parallelepiped ⇑b = Icc 0 1 ∨ parallelepiped ⇑b = Icc (-1) 0

Proof state:
case h₁.h
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ⇑(b.reindex 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

Tactic:
simp only [F, Subsingleton.elim j 0]

Result:
no goals

Proof state:
case h₂.intro.intro
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ⇑(b.reindex e) = parallelepiped ⇑b
F : ℝ → Fin 1 → ℝ := fun t _i => t
y : ℝ
hy : y ∈ Icc 0 1
⊢ F y ∈ Icc 0 1

Tactic:
exact ⟨fun _j => hy.1, fun _j => hy.2⟩

Result:
no goals

Proof state:
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
⊢ parallelepiped ⇑b = Icc 0 1 ∨ parallelepiped ⇑b = Icc (-1) 0

Tactic:
have B : parallelepiped (b.reindex e) = parallelepiped b := by
  convert parallelepiped_comp_equiv b e.symm
  ext i
  simp only [OrthonormalBasis.coe_reindex]

Result:
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ⇑(b.reindex e) = parallelepiped ⇑b
⊢ parallelepiped ⇑b = Icc 0 1 ∨ parallelepiped ⇑b = Icc (-1) 0

Proof state:
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ⇑(b.reindex e) = parallelepiped ⇑b
⊢ parallelepiped ⇑b = Icc 0 1 ∨ parallelepiped ⇑b = Icc (-1) 0

Tactic:
rw [← B]

Result:
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ⇑(b.reindex e) = parallelepiped ⇑b
⊢ parallelepiped ⇑(b.reindex e) = Icc 0 1 ∨ parallelepiped ⇑(b.reindex e) = Icc (-1) 0

Proof state:
case inr.h
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ⇑(b.reindex e) = parallelepiped ⇑b
F : ℝ → Fin 1 → ℝ := fun t _i => t
A : Icc 0 1 = F '' Icc 0 1
H : ⇑(b.reindex e) = fun x => -1
⊢ parallelepiped ⇑(b.reindex e) = Icc (-1) 0

Tactic:
simp_rw [H, parallelepiped, Algebra.id.smul_eq_mul, A]

Result:
case inr.h
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ⇑(b.reindex e) = parallelepiped ⇑b
F : ℝ → Fin 1 → ℝ := fun t _i => t
A : Icc 0 1 = F '' Icc 0 1
H : ⇑(b.reindex e) = fun x => -1
⊢ (fun a => ∑ x : Fin 1, a x * -1) '' (F '' Icc 0 1) = Icc (-1) 0

Proof state:
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ⇑(b.reindex e) = parallelepiped ⇑b
⊢ parallelepiped ⇑(b.reindex e) = Icc 0 1 ∨ parallelepiped ⇑(b.reindex e) = Icc (-1) 0

Tactic:
let F : ℝ → Fin 1 → ℝ := fun t => fun _i => t

Result:
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ⇑(b.reindex e) = parallelepiped ⇑b
F : ℝ → Fin 1 → ℝ := fun t _i => t
⊢ parallelepiped ⇑(b.reindex e) = Icc 0 1 ∨ parallelepiped ⇑(b.reindex e) = Icc (-1) 0

Proof state:
case inl.h
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ⇑(b.reindex e) = parallelepiped ⇑b
F : ℝ → Fin 1 → ℝ := fun t _i => t
A : Icc 0 1 = F '' Icc 0 1
H : ⇑(b.reindex e) = fun x => 1
⊢ parallelepiped ⇑(b.reindex e) = Icc 0 1

Tactic:
simp_rw [parallelepiped, H, A, Algebra.id.smul_eq_mul, mul_one]

Result:
case inl.h
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ⇑(b.reindex e) = parallelepiped ⇑b
F : ℝ → Fin 1 → ℝ := fun t _i => t
A : Icc 0 1 = F '' Icc 0 1
H : ⇑(b.reindex e) = fun x => 1
⊢ (fun a => ∑ x : Fin 1, a x) '' (F '' Icc 0 1) = Icc 0 1

Proof state:
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
⊢ ι ≃ Fin 1

Tactic:
apply Fintype.equivFinOfCardEq

Result:
case h
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
⊢ Fintype.card ι = 1

Proof state:
case h.e'_2.h.e'_6
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
⊢ ⇑(b.reindex e) = ⇑b ∘ ⇑e.symm

Tactic:
ext i

Result:
case h.e'_2.h.e'_6.h
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
i : Fin 1
⊢ (b.reindex e) i = (⇑b ∘ ⇑e.symm) i

Proof state:
case h₁
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ⇑(b.reindex e) = parallelepiped ⇑b
F : ℝ → Fin 1 → ℝ := fun t _i => t
x : Fin 1 → ℝ
hx : x ∈ Icc 0 1
⊢ x ∈ F '' Icc 0 1

Tactic:
refine ⟨x 0, ⟨hx.1 0, hx.2 0⟩, ?_⟩

Result:
case h₁
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ⇑(b.reindex e) = parallelepiped ⇑b
F : ℝ → Fin 1 → ℝ := fun t _i => t
x : Fin 1 → ℝ
hx : x ∈ Icc 0 1
⊢ F (x 0) = x

Proof state:
case inr.h
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ⇑(b.reindex e) = parallelepiped ⇑b
F : ℝ → Fin 1 → ℝ := fun t _i => t
A : Icc 0 1 = F '' Icc 0 1
H : ⇑(b.reindex e) = fun x => -1
⊢ (fun a => ∑ x : Fin 1, a x * -1) '' (F '' Icc 0 1) = Icc (-1) 0

Tactic:
simp only [F, Finset.univ_unique, Fin.default_eq_zero, mul_neg, mul_one, Finset.sum_neg_distrib,
  Finset.sum_singleton, ← image_comp, Function.comp, image_neg_eq_neg, neg_Icc, neg_zero]

Result:
no goals

Proof state:
case h₁
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ⇑(b.reindex e) = parallelepiped ⇑b
F : ℝ → Fin 1 → ℝ := fun t _i => t
⊢ Icc 0 1 ⊆ F '' Icc 0 1

Tactic:
intro x hx

Result:
case h₁
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ⇑(b.reindex e) = parallelepiped ⇑b
F : ℝ → Fin 1 → ℝ := fun t _i => t
x : Fin 1 → ℝ
hx : x ∈ Icc 0 1
⊢ x ∈ F '' Icc 0 1

Proof state:
case h₂
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ⇑(b.reindex e) = parallelepiped ⇑b
F : ℝ → Fin 1 → ℝ := fun t _i => t
⊢ F '' Icc 0 1 ⊆ Icc 0 1

Tactic:
rintro x ⟨y, hy, rfl⟩

Result:
case h₂.intro.intro
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B : parallelepiped ⇑(b.reindex e) = parallelepiped ⇑b
F : ℝ → Fin 1 → ℝ := fun t _i => t
y : ℝ
hy : y ∈ Icc 0 1
⊢ F y ∈ Icc 0 1