[GOAL]
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
ν : Measure α
hν : ν ≪ μ
s : Set α
f : α → Set (Set α)
h : ∀ (x : α), x ∈ s → f x ⊆ setsAt v x
h' : ∀ (x : α), x ∈ s → ∀ (ε : ℝ), ε > 0 → ∃ a, a ∈ f x ∧ a ⊆ closedBall x ε
⊢ ∃ t,
    (∀ (p : α × Set α), p ∈ t → p.fst ∈ s) ∧
      (PairwiseDisjoint t fun p => p.snd) ∧
        (∀ (p : α × Set α), p ∈ t → p.snd ∈ f p.fst) ∧ ↑↑ν (s \ ⋃ (p : α × Set α) (_ : p ∈ t), p.snd) = 0
[PROOFSTEP]
rcases v.covering s f h h' with ⟨t, ts, disj, mem_f, hμ⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
ν : Measure α
hν : ν ≪ μ
s : Set α
f : α → Set (Set α)
h : ∀ (x : α), x ∈ s → f x ⊆ setsAt v x
h' : ∀ (x : α), x ∈ s → ∀ (ε : ℝ), ε > 0 → ∃ a, a ∈ f x ∧ a ⊆ closedBall x ε
t : Set (α × Set α)
ts : ∀ (p : α × Set α), p ∈ t → p.fst ∈ s
disj : PairwiseDisjoint t fun p => p.snd
mem_f : ∀ (p : α × Set α), p ∈ t → p.snd ∈ f p.fst
hμ : ↑↑μ (s \ ⋃ (p : α × Set α) (_ : p ∈ t), p.snd) = 0
⊢ ∃ t,
    (∀ (p : α × Set α), p ∈ t → p.fst ∈ s) ∧
      (PairwiseDisjoint t fun p => p.snd) ∧
        (∀ (p : α × Set α), p ∈ t → p.snd ∈ f p.fst) ∧ ↑↑ν (s \ ⋃ (p : α × Set α) (_ : p ∈ t), p.snd) = 0
[PROOFSTEP]
exact ⟨t, ts, disj, mem_f, hν hμ⟩
[GOAL]
α : Type u_1
inst✝¹ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
f : α → Set (Set α)
s : Set α
h : FineSubfamilyOn v f s
inst✝ : SecondCountableTopology α
ρ : Measure α
hρ : ρ ≪ μ
⊢ s ⊆
    (s \ ⋃ (p : α × Set α) (_ : p ∈ FineSubfamilyOn.index h), FineSubfamilyOn.covering h p) ∪
      ⋃ (p : α × Set α) (_ : p ∈ FineSubfamilyOn.index h), FineSubfamilyOn.covering h p
[PROOFSTEP]
simp only [subset_union_left, diff_union_self]
[GOAL]
α : Type u_1
inst✝¹ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
f : α → Set (Set α)
s : Set α
h : FineSubfamilyOn v f s
inst✝ : SecondCountableTopology α
ρ : Measure α
hρ : ρ ≪ μ
⊢ ↑↑ρ (s \ ⋃ (p : α × Set α) (_ : p ∈ FineSubfamilyOn.index h), FineSubfamilyOn.covering h p) +
      ↑↑ρ (⋃ (p : α × Set α) (_ : p ∈ FineSubfamilyOn.index h), FineSubfamilyOn.covering h p) =
    ∑' (p : ↑(FineSubfamilyOn.index h)), ↑↑ρ (FineSubfamilyOn.covering h ↑p)
[PROOFSTEP]
rw [hρ h.measure_diff_biUnion, zero_add,
  measure_biUnion h.index_countable h.covering_disjoint fun x hx => h.measurableSet_u hx]
[GOAL]
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
x : α
a : Set α
ha : a ∈ (fun x => setsAt v x ∪ {a | MeasurableSet a ∧ Set.Nonempty (interior a) ∧ ¬a ⊆ closedBall x δ}) x
⊢ MeasurableSet a
[PROOFSTEP]
cases' ha with ha ha
[GOAL]
case inl
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
x : α
a : Set α
ha : a ∈ setsAt v x
⊢ MeasurableSet a
case inr
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
x : α
a : Set α
ha : a ∈ {a | MeasurableSet a ∧ Set.Nonempty (interior a) ∧ ¬a ⊆ closedBall x δ}
⊢ MeasurableSet a
[PROOFSTEP]
exacts [v.MeasurableSet' _ _ ha, ha.1]
[GOAL]
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
x : α
a : Set α
ha : a ∈ (fun x => setsAt v x ∪ {a | MeasurableSet a ∧ Set.Nonempty (interior a) ∧ ¬a ⊆ closedBall x δ}) x
⊢ Set.Nonempty (interior a)
[PROOFSTEP]
cases' ha with ha ha
[GOAL]
case inl
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
x : α
a : Set α
ha : a ∈ setsAt v x
⊢ Set.Nonempty (interior a)
case inr
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
x : α
a : Set α
ha : a ∈ {a | MeasurableSet a ∧ Set.Nonempty (interior a) ∧ ¬a ⊆ closedBall x δ}
⊢ Set.Nonempty (interior a)
[PROOFSTEP]
exacts [v.nonempty_interior _ _ ha, ha.2.1]
[GOAL]
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
⊢ ∀ (x : α) (ε : ℝ),
    ε > 0 →
      ∃ y,
        y ∈ (fun x => setsAt v x ∪ {a | MeasurableSet a ∧ Set.Nonempty (interior a) ∧ ¬a ⊆ closedBall x δ}) x ∧
          y ⊆ closedBall x ε
[PROOFSTEP]
intro x ε εpos
[GOAL]
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
x : α
ε : ℝ
εpos : ε > 0
⊢ ∃ y,
    y ∈ (fun x => setsAt v x ∪ {a | MeasurableSet a ∧ Set.Nonempty (interior a) ∧ ¬a ⊆ closedBall x δ}) x ∧
      y ⊆ closedBall x ε
[PROOFSTEP]
rcases v.Nontrivial x ε εpos with ⟨a, ha, h'a⟩
[GOAL]
case intro.intro
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
x : α
ε : ℝ
εpos : ε > 0
a : Set α
ha : a ∈ setsAt v x
h'a : a ⊆ closedBall x ε
⊢ ∃ y,
    y ∈ (fun x => setsAt v x ∪ {a | MeasurableSet a ∧ Set.Nonempty (interior a) ∧ ¬a ⊆ closedBall x δ}) x ∧
      y ⊆ closedBall x ε
[PROOFSTEP]
exact ⟨a, mem_union_left _ ha, h'a⟩
[GOAL]
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
⊢ ∀ (s : Set α) (f : α → Set (Set α)),
    (∀ (x : α),
        x ∈ s →
          f x ⊆ (fun x => setsAt v x ∪ {a | MeasurableSet a ∧ Set.Nonempty (interior a) ∧ ¬a ⊆ closedBall x δ}) x) →
      (∀ (x : α), x ∈ s → ∀ (ε : ℝ), ε > 0 → ∃ a, a ∈ f x ∧ a ⊆ closedBall x ε) →
        ∃ t,
          (∀ (p : α × Set α), p ∈ t → p.fst ∈ s) ∧
            (PairwiseDisjoint t fun p => p.snd) ∧
              (∀ (p : α × Set α), p ∈ t → p.snd ∈ f p.fst) ∧ ↑↑μ (s \ ⋃ (p : α × Set α) (_ : p ∈ t), p.snd) = 0
[PROOFSTEP]
intro s f fset ffine
[GOAL]
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
s : Set α
f : α → Set (Set α)
fset :
  ∀ (x : α),
    x ∈ s → f x ⊆ (fun x => setsAt v x ∪ {a | MeasurableSet a ∧ Set.Nonempty (interior a) ∧ ¬a ⊆ closedBall x δ}) x
ffine : ∀ (x : α), x ∈ s → ∀ (ε : ℝ), ε > 0 → ∃ a, a ∈ f x ∧ a ⊆ closedBall x ε
⊢ ∃ t,
    (∀ (p : α × Set α), p ∈ t → p.fst ∈ s) ∧
      (PairwiseDisjoint t fun p => p.snd) ∧
        (∀ (p : α × Set α), p ∈ t → p.snd ∈ f p.fst) ∧ ↑↑μ (s \ ⋃ (p : α × Set α) (_ : p ∈ t), p.snd) = 0
[PROOFSTEP]
let g : α → Set (Set α) := fun x => f x ∩ v.setsAt x
[GOAL]
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
s : Set α
f : α → Set (Set α)
fset :
  ∀ (x : α),
    x ∈ s → f x ⊆ (fun x => setsAt v x ∪ {a | MeasurableSet a ∧ Set.Nonempty (interior a) ∧ ¬a ⊆ closedBall x δ}) x
ffine : ∀ (x : α), x ∈ s → ∀ (ε : ℝ), ε > 0 → ∃ a, a ∈ f x ∧ a ⊆ closedBall x ε
g : α → Set (Set α) := fun x => f x ∩ setsAt v x
⊢ ∃ t,
    (∀ (p : α × Set α), p ∈ t → p.fst ∈ s) ∧
      (PairwiseDisjoint t fun p => p.snd) ∧
        (∀ (p : α × Set α), p ∈ t → p.snd ∈ f p.fst) ∧ ↑↑μ (s \ ⋃ (p : α × Set α) (_ : p ∈ t), p.snd) = 0
[PROOFSTEP]
have : ∀ x ∈ s, ∀ ε : ℝ, ε > 0 → ∃ (a : Set α), a ∈ g x ∧ a ⊆ closedBall x ε :=
  by
  intro x hx ε εpos
  obtain ⟨a, af, ha⟩ : ∃ a ∈ f x, a ⊆ closedBall x (min ε δ)
  exact ffine x hx (min ε δ) (lt_min εpos δpos)
  rcases fset x hx af with (h'a | h'a)
  · exact ⟨a, ⟨af, h'a⟩, ha.trans (closedBall_subset_closedBall (min_le_left _ _))⟩
  · refine' False.elim (h'a.2.2 _)
    exact ha.trans (closedBall_subset_closedBall (min_le_right _ _))
[GOAL]
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
s : Set α
f : α → Set (Set α)
fset :
  ∀ (x : α),
    x ∈ s → f x ⊆ (fun x => setsAt v x ∪ {a | MeasurableSet a ∧ Set.Nonempty (interior a) ∧ ¬a ⊆ closedBall x δ}) x
ffine : ∀ (x : α), x ∈ s → ∀ (ε : ℝ), ε > 0 → ∃ a, a ∈ f x ∧ a ⊆ closedBall x ε
g : α → Set (Set α) := fun x => f x ∩ setsAt v x
⊢ ∀ (x : α), x ∈ s → ∀ (ε : ℝ), ε > 0 → ∃ a, a ∈ g x ∧ a ⊆ closedBall x ε
[PROOFSTEP]
intro x hx ε εpos
[GOAL]
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
s : Set α
f : α → Set (Set α)
fset :
  ∀ (x : α),
    x ∈ s → f x ⊆ (fun x => setsAt v x ∪ {a | MeasurableSet a ∧ Set.Nonempty (interior a) ∧ ¬a ⊆ closedBall x δ}) x
ffine : ∀ (x : α), x ∈ s → ∀ (ε : ℝ), ε > 0 → ∃ a, a ∈ f x ∧ a ⊆ closedBall x ε
g : α → Set (Set α) := fun x => f x ∩ setsAt v x
x : α
hx : x ∈ s
ε : ℝ
εpos : ε > 0
⊢ ∃ a, a ∈ g x ∧ a ⊆ closedBall x ε
[PROOFSTEP]
obtain ⟨a, af, ha⟩ : ∃ a ∈ f x, a ⊆ closedBall x (min ε δ)
[GOAL]
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
s : Set α
f : α → Set (Set α)
fset :
  ∀ (x : α),
    x ∈ s → f x ⊆ (fun x => setsAt v x ∪ {a | MeasurableSet a ∧ Set.Nonempty (interior a) ∧ ¬a ⊆ closedBall x δ}) x
ffine : ∀ (x : α), x ∈ s → ∀ (ε : ℝ), ε > 0 → ∃ a, a ∈ f x ∧ a ⊆ closedBall x ε
g : α → Set (Set α) := fun x => f x ∩ setsAt v x
x : α
hx : x ∈ s
ε : ℝ
εpos : ε > 0
⊢ ∃ a, a ∈ f x ∧ a ⊆ closedBall x (min ε δ)
case intro.intro
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
s : Set α
f : α → Set (Set α)
fset :
  ∀ (x : α),
    x ∈ s → f x ⊆ (fun x => setsAt v x ∪ {a | MeasurableSet a ∧ Set.Nonempty (interior a) ∧ ¬a ⊆ closedBall x δ}) x
ffine : ∀ (x : α), x ∈ s → ∀ (ε : ℝ), ε > 0 → ∃ a, a ∈ f x ∧ a ⊆ closedBall x ε
g : α → Set (Set α) := fun x => f x ∩ setsAt v x
x : α
hx : x ∈ s
ε : ℝ
εpos : ε > 0
a : Set α
af : a ∈ f x
ha : a ⊆ closedBall x (min ε δ)
⊢ ∃ a, a ∈ g x ∧ a ⊆ closedBall x ε
[PROOFSTEP]
exact ffine x hx (min ε δ) (lt_min εpos δpos)
[GOAL]
case intro.intro
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
s : Set α
f : α → Set (Set α)
fset :
  ∀ (x : α),
    x ∈ s → f x ⊆ (fun x => setsAt v x ∪ {a | MeasurableSet a ∧ Set.Nonempty (interior a) ∧ ¬a ⊆ closedBall x δ}) x
ffine : ∀ (x : α), x ∈ s → ∀ (ε : ℝ), ε > 0 → ∃ a, a ∈ f x ∧ a ⊆ closedBall x ε
g : α → Set (Set α) := fun x => f x ∩ setsAt v x
x : α
hx : x ∈ s
ε : ℝ
εpos : ε > 0
a : Set α
af : a ∈ f x
ha : a ⊆ closedBall x (min ε δ)
⊢ ∃ a, a ∈ g x ∧ a ⊆ closedBall x ε
[PROOFSTEP]
rcases fset x hx af with (h'a | h'a)
[GOAL]
case intro.intro.inl
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
s : Set α
f : α → Set (Set α)
fset :
  ∀ (x : α),
    x ∈ s → f x ⊆ (fun x => setsAt v x ∪ {a | MeasurableSet a ∧ Set.Nonempty (interior a) ∧ ¬a ⊆ closedBall x δ}) x
ffine : ∀ (x : α), x ∈ s → ∀ (ε : ℝ), ε > 0 → ∃ a, a ∈ f x ∧ a ⊆ closedBall x ε
g : α → Set (Set α) := fun x => f x ∩ setsAt v x
x : α
hx : x ∈ s
ε : ℝ
εpos : ε > 0
a : Set α
af : a ∈ f x
ha : a ⊆ closedBall x (min ε δ)
h'a : a ∈ setsAt v x
⊢ ∃ a, a ∈ g x ∧ a ⊆ closedBall x ε
[PROOFSTEP]
exact ⟨a, ⟨af, h'a⟩, ha.trans (closedBall_subset_closedBall (min_le_left _ _))⟩
[GOAL]
case intro.intro.inr
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
s : Set α
f : α → Set (Set α)
fset :
  ∀ (x : α),
    x ∈ s → f x ⊆ (fun x => setsAt v x ∪ {a | MeasurableSet a ∧ Set.Nonempty (interior a) ∧ ¬a ⊆ closedBall x δ}) x
ffine : ∀ (x : α), x ∈ s → ∀ (ε : ℝ), ε > 0 → ∃ a, a ∈ f x ∧ a ⊆ closedBall x ε
g : α → Set (Set α) := fun x => f x ∩ setsAt v x
x : α
hx : x ∈ s
ε : ℝ
εpos : ε > 0
a : Set α
af : a ∈ f x
ha : a ⊆ closedBall x (min ε δ)
h'a : a ∈ {a | MeasurableSet a ∧ Set.Nonempty (interior a) ∧ ¬a ⊆ closedBall x δ}
⊢ ∃ a, a ∈ g x ∧ a ⊆ closedBall x ε
[PROOFSTEP]
refine' False.elim (h'a.2.2 _)
[GOAL]
case intro.intro.inr
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
s : Set α
f : α → Set (Set α)
fset :
  ∀ (x : α),
    x ∈ s → f x ⊆ (fun x => setsAt v x ∪ {a | MeasurableSet a ∧ Set.Nonempty (interior a) ∧ ¬a ⊆ closedBall x δ}) x
ffine : ∀ (x : α), x ∈ s → ∀ (ε : ℝ), ε > 0 → ∃ a, a ∈ f x ∧ a ⊆ closedBall x ε
g : α → Set (Set α) := fun x => f x ∩ setsAt v x
x : α
hx : x ∈ s
ε : ℝ
εpos : ε > 0
a : Set α
af : a ∈ f x
ha : a ⊆ closedBall x (min ε δ)
h'a : a ∈ {a | MeasurableSet a ∧ Set.Nonempty (interior a) ∧ ¬a ⊆ closedBall x δ}
⊢ a ⊆ closedBall x δ
[PROOFSTEP]
exact ha.trans (closedBall_subset_closedBall (min_le_right _ _))
[GOAL]
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
s : Set α
f : α → Set (Set α)
fset :
  ∀ (x : α),
    x ∈ s → f x ⊆ (fun x => setsAt v x ∪ {a | MeasurableSet a ∧ Set.Nonempty (interior a) ∧ ¬a ⊆ closedBall x δ}) x
ffine : ∀ (x : α), x ∈ s → ∀ (ε : ℝ), ε > 0 → ∃ a, a ∈ f x ∧ a ⊆ closedBall x ε
g : α → Set (Set α) := fun x => f x ∩ setsAt v x
this : ∀ (x : α), x ∈ s → ∀ (ε : ℝ), ε > 0 → ∃ a, a ∈ g x ∧ a ⊆ closedBall x ε
⊢ ∃ t,
    (∀ (p : α × Set α), p ∈ t → p.fst ∈ s) ∧
      (PairwiseDisjoint t fun p => p.snd) ∧
        (∀ (p : α × Set α), p ∈ t → p.snd ∈ f p.fst) ∧ ↑↑μ (s \ ⋃ (p : α × Set α) (_ : p ∈ t), p.snd) = 0
[PROOFSTEP]
rcases v.covering s g (fun x _ => inter_subset_right _ _) this with ⟨t, ts, tdisj, tg, μt⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
s : Set α
f : α → Set (Set α)
fset :
  ∀ (x : α),
    x ∈ s → f x ⊆ (fun x => setsAt v x ∪ {a | MeasurableSet a ∧ Set.Nonempty (interior a) ∧ ¬a ⊆ closedBall x δ}) x
ffine : ∀ (x : α), x ∈ s → ∀ (ε : ℝ), ε > 0 → ∃ a, a ∈ f x ∧ a ⊆ closedBall x ε
g : α → Set (Set α) := fun x => f x ∩ setsAt v x
this : ∀ (x : α), x ∈ s → ∀ (ε : ℝ), ε > 0 → ∃ a, a ∈ g x ∧ a ⊆ closedBall x ε
t : Set (α × Set α)
ts : ∀ (p : α × Set α), p ∈ t → p.fst ∈ s
tdisj : PairwiseDisjoint t fun p => p.snd
tg : ∀ (p : α × Set α), p ∈ t → p.snd ∈ g p.fst
μt : ↑↑μ (s \ ⋃ (p : α × Set α) (_ : p ∈ t), p.snd) = 0
⊢ ∃ t,
    (∀ (p : α × Set α), p ∈ t → p.fst ∈ s) ∧
      (PairwiseDisjoint t fun p => p.snd) ∧
        (∀ (p : α × Set α), p ∈ t → p.snd ∈ f p.fst) ∧ ↑↑μ (s \ ⋃ (p : α × Set α) (_ : p ∈ t), p.snd) = 0
[PROOFSTEP]
exact ⟨t, ts, tdisj, fun p hp => (tg p hp).1, μt⟩
[GOAL]
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
x : α
s : Set (Set α)
⊢ s ∈ filterAt v x ↔ ∃ ε, ε > 0 ∧ ∀ (a : Set α), a ∈ setsAt v x → a ⊆ closedBall x ε → a ∈ s
[PROOFSTEP]
simp only [filterAt, exists_prop, gt_iff_lt]
[GOAL]
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
x : α
s : Set (Set α)
⊢ s ∈ ⨅ (ε : ℝ) (_ : ε ∈ Ioi 0), 𝓟 {a | a ∈ setsAt v x ∧ a ⊆ closedBall x ε} ↔
    ∃ ε, 0 < ε ∧ ∀ (a : Set α), a ∈ setsAt v x → a ⊆ closedBall x ε → a ∈ s
[PROOFSTEP]
rw [mem_biInf_of_directed]
[GOAL]
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
x : α
s : Set (Set α)
⊢ (∃ i, i ∈ Ioi 0 ∧ s ∈ 𝓟 {a | a ∈ setsAt v x ∧ a ⊆ closedBall x i}) ↔
    ∃ ε, 0 < ε ∧ ∀ (a : Set α), a ∈ setsAt v x → a ⊆ closedBall x ε → a ∈ s
[PROOFSTEP]
simp only [subset_def, and_imp, exists_prop, mem_sep_iff, mem_Ioi, mem_principal]
[GOAL]
case h
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
x : α
s : Set (Set α)
⊢ DirectedOn ((fun ε => 𝓟 {a | a ∈ setsAt v x ∧ a ⊆ closedBall x ε}) ⁻¹'o fun x x_1 => x ≥ x_1) (Ioi 0)
[PROOFSTEP]
simp only [DirectedOn, exists_prop, ge_iff_le, le_principal_iff, mem_Ioi, Order.Preimage, mem_principal]
[GOAL]
case h
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
x : α
s : Set (Set α)
⊢ ∀ (x_1 : ℝ),
    0 < x_1 →
      ∀ (y : ℝ),
        0 < y →
          ∃ z,
            0 < z ∧
              {a | a ∈ setsAt v x ∧ a ⊆ closedBall x z} ⊆ {a | a ∈ setsAt v x ∧ a ⊆ closedBall x x_1} ∧
                {a | a ∈ setsAt v x ∧ a ⊆ closedBall x z} ⊆ {a | a ∈ setsAt v x ∧ a ⊆ closedBall x y}
[PROOFSTEP]
intro x hx y hy
[GOAL]
case h
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
x✝ : α
s : Set (Set α)
x : ℝ
hx : 0 < x
y : ℝ
hy : 0 < y
⊢ ∃ z,
    0 < z ∧
      {a | a ∈ setsAt v x✝ ∧ a ⊆ closedBall x✝ z} ⊆ {a | a ∈ setsAt v x✝ ∧ a ⊆ closedBall x✝ x} ∧
        {a | a ∈ setsAt v x✝ ∧ a ⊆ closedBall x✝ z} ⊆ {a | a ∈ setsAt v x✝ ∧ a ⊆ closedBall x✝ y}
[PROOFSTEP]
refine'
  ⟨min x y, lt_min hx hy, fun a ha => ⟨ha.1, ha.2.trans (closedBall_subset_closedBall (min_le_left _ _))⟩, fun a ha =>
    ⟨ha.1, ha.2.trans (closedBall_subset_closedBall (min_le_right _ _))⟩⟩
[GOAL]
case ne
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
x : α
s : Set (Set α)
⊢ Set.Nonempty (Ioi 0)
[PROOFSTEP]
exact ⟨(1 : ℝ), mem_Ioi.2 zero_lt_one⟩
[GOAL]
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
x : α
⊢ NeBot (filterAt v x)
[PROOFSTEP]
simp only [neBot_iff, ← empty_mem_iff_bot, mem_filterAt_iff, not_exists, exists_prop, mem_empty_iff_false, and_true_iff,
  gt_iff_lt, not_and, Ne.def, not_false_iff, not_forall]
[GOAL]
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
x : α
⊢ ∀ (x_1 : ℝ), 0 < x_1 → ∃ x_2, x_2 ∈ setsAt v x ∧ x_2 ⊆ closedBall x x_1
[PROOFSTEP]
intro ε εpos
[GOAL]
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
x : α
ε : ℝ
εpos : 0 < ε
⊢ ∃ x_1, x_1 ∈ setsAt v x ∧ x_1 ⊆ closedBall x ε
[PROOFSTEP]
obtain ⟨w, w_sets, hw⟩ : ∃ w ∈ v.setsAt x, w ⊆ closedBall x ε := v.Nontrivial x ε εpos
[GOAL]
case intro.intro
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
x : α
ε : ℝ
εpos : 0 < ε
w : Set α
w_sets : w ∈ setsAt v x
hw : w ⊆ closedBall x ε
⊢ ∃ x_1, x_1 ∈ setsAt v x ∧ x_1 ⊆ closedBall x ε
[PROOFSTEP]
exact ⟨w, w_sets, hw⟩
[GOAL]
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
x : α
⊢ ∀ᶠ (a : Set α) in filterAt v x, a ∈ setsAt v x
[PROOFSTEP]
simp (config := { contextual := true }) only [eventually_filterAt_iff, exists_prop, and_true_iff, gt_iff_lt,
  imp_true_iff]
[GOAL]
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
x : α
⊢ ∃ ε, 0 < ε
[PROOFSTEP]
exact ⟨1, zero_lt_one⟩
[GOAL]
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
x : α
ε : ℝ
hε : 0 < ε
⊢ ∀ᶠ (a : Set α) in filterAt v x, a ⊆ closedBall x ε
[PROOFSTEP]
simp only [v.eventually_filterAt_iff]
[GOAL]
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
x : α
ε : ℝ
hε : 0 < ε
⊢ ∃ ε_1, ε_1 > 0 ∧ ∀ (a : Set α), a ∈ setsAt v x → a ⊆ closedBall x ε_1 → a ⊆ closedBall x ε
[PROOFSTEP]
exact ⟨ε, hε, fun a _ ha' => ha'⟩
[GOAL]
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
ι : Type u_2
l : Filter ι
f : ι → Set α
x : α
⊢ Tendsto f l (filterAt v x) ↔
    (∀ᶠ (i : ι) in l, f i ∈ setsAt v x) ∧ ∀ (ε : ℝ), ε > 0 → ∀ᶠ (i : ι) in l, f i ⊆ closedBall x ε
[PROOFSTEP]
refine'
  ⟨fun H =>
    ⟨H.eventually <| v.eventually_filterAt_mem_sets x, fun ε hε =>
      H.eventually <| v.eventually_filterAt_subset_closedBall x hε⟩,
    fun H s hs => (_ : ∀ᶠ i in l, f i ∈ s)⟩
[GOAL]
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
ι : Type u_2
l : Filter ι
f : ι → Set α
x : α
H : (∀ᶠ (i : ι) in l, f i ∈ setsAt v x) ∧ ∀ (ε : ℝ), ε > 0 → ∀ᶠ (i : ι) in l, f i ⊆ closedBall x ε
s : Set (Set α)
hs : s ∈ filterAt v x
⊢ ∀ᶠ (i : ι) in l, f i ∈ s
[PROOFSTEP]
obtain ⟨ε, εpos, hε⟩ := v.mem_filterAt_iff.mp hs
[GOAL]
case intro.intro
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
ι : Type u_2
l : Filter ι
f : ι → Set α
x : α
H : (∀ᶠ (i : ι) in l, f i ∈ setsAt v x) ∧ ∀ (ε : ℝ), ε > 0 → ∀ᶠ (i : ι) in l, f i ⊆ closedBall x ε
s : Set (Set α)
hs : s ∈ filterAt v x
ε : ℝ
εpos : ε > 0
hε : ∀ (a : Set α), a ∈ setsAt v x → a ⊆ closedBall x ε → a ∈ s
⊢ ∀ᶠ (i : ι) in l, f i ∈ s
[PROOFSTEP]
filter_upwards [H.1, H.2 ε εpos] with i hi hiε using hε _ hi hiε
[GOAL]
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
x : α
⊢ ∀ᶠ (a : Set α) in filterAt v x, MeasurableSet a
[PROOFSTEP]
filter_upwards [v.eventually_filterAt_mem_sets x] with _ ha using v.MeasurableSet' _ _ ha
[GOAL]
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
x : α
P : Set α → Prop
⊢ (∃ᶠ (a : Set α) in filterAt v x, P a) ↔ ∀ (ε : ℝ), ε > 0 → ∃ a, a ∈ setsAt v x ∧ a ⊆ closedBall x ε ∧ P a
[PROOFSTEP]
simp only [Filter.Frequently, eventually_filterAt_iff, not_exists, exists_prop, not_and, Classical.not_not, not_forall]
[GOAL]
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
x : α
o : Set α
hx : o ∈ 𝓝 x
⊢ ∀ᶠ (a : Set α) in filterAt v x, a ⊆ o
[PROOFSTEP]
rw [eventually_filterAt_iff]
[GOAL]
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
x : α
o : Set α
hx : o ∈ 𝓝 x
⊢ ∃ ε, ε > 0 ∧ ∀ (a : Set α), a ∈ setsAt v x → a ⊆ closedBall x ε → a ⊆ o
[PROOFSTEP]
rcases Metric.mem_nhds_iff.1 hx with ⟨ε, εpos, hε⟩
[GOAL]
case intro.intro
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
x : α
o : Set α
hx : o ∈ 𝓝 x
ε : ℝ
εpos : ε > 0
hε : ball x ε ⊆ o
⊢ ∃ ε, ε > 0 ∧ ∀ (a : Set α), a ∈ setsAt v x → a ⊆ closedBall x ε → a ⊆ o
[PROOFSTEP]
exact ⟨ε / 2, half_pos εpos, fun a _ ha => ha.trans ((closedBall_subset_ball (half_lt_self εpos)).trans hε)⟩
[GOAL]
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v✝ v : VitaliFamily μ
f : α → Set (Set α)
s : Set α
h : ∀ (x : α), x ∈ s → ∃ᶠ (a : Set α) in filterAt v x, a ∈ f x
⊢ FineSubfamilyOn v f s
[PROOFSTEP]
intro x hx ε εpos
[GOAL]
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v✝ v : VitaliFamily μ
f : α → Set (Set α)
s : Set α
h : ∀ (x : α), x ∈ s → ∃ᶠ (a : Set α) in filterAt v x, a ∈ f x
x : α
hx : x ∈ s
ε : ℝ
εpos : ε > 0
⊢ ∃ a, a ∈ setsAt v x ∩ f x ∧ a ⊆ closedBall x ε
[PROOFSTEP]
obtain ⟨a, av, ha, af⟩ : ∃ (a : Set α), a ∈ v.setsAt x ∧ a ⊆ closedBall x ε ∧ a ∈ f x :=
  v.frequently_filterAt_iff.1 (h x hx) ε εpos
[GOAL]
case intro.intro.intro
α : Type u_1
inst✝ : MetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v✝ v : VitaliFamily μ
f : α → Set (Set α)
s : Set α
h : ∀ (x : α), x ∈ s → ∃ᶠ (a : Set α) in filterAt v x, a ∈ f x
x : α
hx : x ∈ s
ε : ℝ
εpos : ε > 0
a : Set α
av : a ∈ setsAt v x
ha : a ⊆ closedBall x ε
af : a ∈ f x
⊢ ∃ a, a ∈ setsAt v x ∩ f x ∧ a ⊆ closedBall x ε
[PROOFSTEP]
exact ⟨a, ⟨av, af⟩, ha⟩


[GOAL]
x y : ℝ
hxy : x < y
⊢ Icc x y ∈ VitaliFamily.setsAt (vitaliFamily volume 1) x
[PROOFSTEP]
rw [Icc_eq_closedBall]
[GOAL]
x y : ℝ
hxy : x < y
⊢ Metric.closedBall ((x + y) / 2) ((y - x) / 2) ∈ VitaliFamily.setsAt (vitaliFamily volume 1) x
[PROOFSTEP]
refine' closedBall_mem_vitaliFamily_of_dist_le_mul _ _ (by linarith)
[GOAL]
x y : ℝ
hxy : x < y
⊢ 0 < (y - x) / 2
[PROOFSTEP]
linarith
[GOAL]
x y : ℝ
hxy : x < y
⊢ dist x ((x + y) / 2) ≤ 1 * ((y - x) / 2)
[PROOFSTEP]
rw [dist_comm, Real.dist_eq, abs_of_nonneg]
[GOAL]
x y : ℝ
hxy : x < y
⊢ (x + y) / 2 - x ≤ 1 * ((y - x) / 2)
[PROOFSTEP]
linarith
[GOAL]
x y : ℝ
hxy : x < y
⊢ 0 ≤ (x + y) / 2 - x
[PROOFSTEP]
linarith
[GOAL]
x : ℝ
⊢ Tendsto (fun y => Icc x y) (𝓝[Ioi x] x) (VitaliFamily.filterAt (vitaliFamily volume 1) x)
[PROOFSTEP]
refine' (VitaliFamily.tendsto_filterAt_iff _).2 ⟨_, _⟩
[GOAL]
case refine'_1
x : ℝ
⊢ ∀ᶠ (i : ℝ) in 𝓝[Ioi x] x, Icc x i ∈ VitaliFamily.setsAt (vitaliFamily volume 1) x
[PROOFSTEP]
filter_upwards [self_mem_nhdsWithin] with y hy using Icc_mem_vitaliFamily_at_right hy
[GOAL]
case refine'_2
x : ℝ
⊢ ∀ (ε : ℝ), ε > 0 → ∀ᶠ (i : ℝ) in 𝓝[Ioi x] x, Icc x i ⊆ Metric.closedBall x ε
[PROOFSTEP]
intro ε εpos
[GOAL]
case refine'_2
x ε : ℝ
εpos : ε > 0
⊢ ∀ᶠ (i : ℝ) in 𝓝[Ioi x] x, Icc x i ⊆ Metric.closedBall x ε
[PROOFSTEP]
have : x ∈ Ico x (x + ε) := ⟨le_refl _, by linarith⟩
[GOAL]
x ε : ℝ
εpos : ε > 0
⊢ x < x + ε
[PROOFSTEP]
linarith
[GOAL]
case refine'_2
x ε : ℝ
εpos : ε > 0
this : x ∈ Ico x (x + ε)
⊢ ∀ᶠ (i : ℝ) in 𝓝[Ioi x] x, Icc x i ⊆ Metric.closedBall x ε
[PROOFSTEP]
filter_upwards [Icc_mem_nhdsWithin_Ioi this] with y hy
[GOAL]
case h
x ε : ℝ
εpos : ε > 0
this : x ∈ Ico x (x + ε)
y : ℝ
hy : y ∈ Icc x (x + ε)
⊢ Icc x y ⊆ Metric.closedBall x ε
[PROOFSTEP]
rw [closedBall_eq_Icc]
[GOAL]
case h
x ε : ℝ
εpos : ε > 0
this : x ∈ Ico x (x + ε)
y : ℝ
hy : y ∈ Icc x (x + ε)
⊢ Icc x y ⊆ Icc (x - ε) (x + ε)
[PROOFSTEP]
exact Icc_subset_Icc (by linarith) hy.2
[GOAL]
x ε : ℝ
εpos : ε > 0
this : x ∈ Ico x (x + ε)
y : ℝ
hy : y ∈ Icc x (x + ε)
⊢ x - ε ≤ x
[PROOFSTEP]
linarith
[GOAL]
x y : ℝ
hxy : x < y
⊢ Icc x y ∈ VitaliFamily.setsAt (vitaliFamily volume 1) y
[PROOFSTEP]
rw [Icc_eq_closedBall]
[GOAL]
x y : ℝ
hxy : x < y
⊢ Metric.closedBall ((x + y) / 2) ((y - x) / 2) ∈ VitaliFamily.setsAt (vitaliFamily volume 1) y
[PROOFSTEP]
refine' closedBall_mem_vitaliFamily_of_dist_le_mul _ _ (by linarith)
[GOAL]
x y : ℝ
hxy : x < y
⊢ 0 < (y - x) / 2
[PROOFSTEP]
linarith
[GOAL]
x y : ℝ
hxy : x < y
⊢ dist y ((x + y) / 2) ≤ 1 * ((y - x) / 2)
[PROOFSTEP]
rw [Real.dist_eq, abs_of_nonneg]
[GOAL]
x y : ℝ
hxy : x < y
⊢ y - (x + y) / 2 ≤ 1 * ((y - x) / 2)
[PROOFSTEP]
linarith
[GOAL]
x y : ℝ
hxy : x < y
⊢ 0 ≤ y - (x + y) / 2
[PROOFSTEP]
linarith
[GOAL]
x : ℝ
⊢ Tendsto (fun y => Icc y x) (𝓝[Iio x] x) (VitaliFamily.filterAt (vitaliFamily volume 1) x)
[PROOFSTEP]
refine' (VitaliFamily.tendsto_filterAt_iff _).2 ⟨_, _⟩
[GOAL]
case refine'_1
x : ℝ
⊢ ∀ᶠ (i : ℝ) in 𝓝[Iio x] x, Icc i x ∈ VitaliFamily.setsAt (vitaliFamily volume 1) x
[PROOFSTEP]
filter_upwards [self_mem_nhdsWithin] with y hy using Icc_mem_vitaliFamily_at_left hy
[GOAL]
case refine'_2
x : ℝ
⊢ ∀ (ε : ℝ), ε > 0 → ∀ᶠ (i : ℝ) in 𝓝[Iio x] x, Icc i x ⊆ Metric.closedBall x ε
[PROOFSTEP]
intro ε εpos
[GOAL]
case refine'_2
x ε : ℝ
εpos : ε > 0
⊢ ∀ᶠ (i : ℝ) in 𝓝[Iio x] x, Icc i x ⊆ Metric.closedBall x ε
[PROOFSTEP]
have : x ∈ Ioc (x - ε) x := ⟨by linarith, le_refl _⟩
[GOAL]
x ε : ℝ
εpos : ε > 0
⊢ x - ε < x
[PROOFSTEP]
linarith
[GOAL]
case refine'_2
x ε : ℝ
εpos : ε > 0
this : x ∈ Ioc (x - ε) x
⊢ ∀ᶠ (i : ℝ) in 𝓝[Iio x] x, Icc i x ⊆ Metric.closedBall x ε
[PROOFSTEP]
filter_upwards [Icc_mem_nhdsWithin_Iio this] with y hy
[GOAL]
case h
x ε : ℝ
εpos : ε > 0
this : x ∈ Ioc (x - ε) x
y : ℝ
hy : y ∈ Icc (x - ε) x
⊢ Icc y x ⊆ Metric.closedBall x ε
[PROOFSTEP]
rw [closedBall_eq_Icc]
[GOAL]
case h
x ε : ℝ
εpos : ε > 0
this : x ∈ Ioc (x - ε) x
y : ℝ
hy : y ∈ Icc (x - ε) x
⊢ Icc y x ⊆ Icc (x - ε) (x + ε)
[PROOFSTEP]
exact Icc_subset_Icc hy.1 (by linarith)
[GOAL]
x ε : ℝ
εpos : ε > 0
this : x ∈ Ioc (x - ε) x
y : ℝ
hy : y ∈ Icc (x - ε) x
⊢ x ≤ x + ε
[PROOFSTEP]
linarith


[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