case h
ι : Type u_1
ι' : Type ?u.104527
E : Type ?u.104530
F : Type ?u.104533
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
ι : Type u_1
ι' : Type ?u.104527
E : Type ?u.104530
F : Type ?u.104533
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
ext x
case h
ι : Type u_1
ι' : Type ?u.104527
E : Type ?u.104530
F : Type ?u.104533
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
case h
ι : Type u_1
ι' : Type ?u.104527
E : Type ?u.104530
F : Type ?u.104533
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
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 (_ : ι → ℝ)]
case h.mp
ι : Type u_1
ι' : Type ?u.104527
E : Type ?u.104530
F : Type ?u.104533
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

case h.mpr
ι : Type u_1
ι' : Type ?u.104527
E : Type ?u.104530
F : Type ?u.104533
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
case h
ι : Type u_1
ι' : Type ?u.104527
E : Type ?u.104530
F : Type ?u.104533
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
constructor
case h.mp.intro.intro
ι : Type u_1
ι' : Type ?u.104527
E : Type ?u.104530
F : Type ?u.104533
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
case h.mp
ι : Type u_1
ι' : Type ?u.104527
E : Type ?u.104530
F : Type ?u.104533
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
rintro ⟨t, ht, rfl⟩ i
case h.mp.intro.intro
ι : Type u_1
ι' : Type ?u.104527
E : Type ?u.104530
F : Type ?u.104533
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
case h.mp.intro.intro
ι : Type u_1
ι' : Type ?u.104527
E : Type ?u.104530
F : Type ?u.104533
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
specialize ht i
case h.mp.intro.intro
ι : Type u_1
ι' : Type ?u.104527
E : Type ?u.104530
F : Type ?u.104533
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
case h.mp.intro.intro
ι : Type u_1
ι' : Type ?u.104527
E : Type ?u.104530
F : Type ?u.104533
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
simp_rw [smul_eq_mul, Pi.mul_apply]
case h.mp.intro.intro.inl
ι : Type u_1
ι' : Type ?u.104527
E : Type ?u.104530
F : Type ?u.104533
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

case h.mp.intro.intro.inr
ι : Type u_1
ι' : Type ?u.104527
E : Type ?u.104530
F : Type ?u.104533
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
case h.mp.intro.intro
ι : Type u_1
ι' : Type ?u.104527
E : Type ?u.104530
F : Type ?u.104533
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
cases' le_total (a i) 0 with hai hai
case h.mp.intro.intro.inl
ι : Type u_1
ι' : Type ?u.104527
E : Type ?u.104530
F : Type ?u.104533
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
case h.mp.intro.intro.inl
ι : Type u_1
ι' : Type ?u.104527
E : Type ?u.104530
F : Type ?u.104533
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
rw [sup_eq_left.mpr hai, inf_eq_right.mpr hai]
no goals
case h.mp.intro.intro.inl
ι : Type u_1
ι' : Type ?u.104527
E : Type ?u.104530
F : Type ?u.104533
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
exact ⟨le_mul_of_le_one_left hai ht.2, mul_nonpos_of_nonneg_of_nonpos ht.1 hai⟩
case h.mp.intro.intro.inr
ι : Type u_1
ι' : Type ?u.104527
E : Type ?u.104530
F : Type ?u.104533
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
case h.mp.intro.intro.inr
ι : Type u_1
ι' : Type ?u.104527
E : Type ?u.104530
F : Type ?u.104533
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
rw [sup_eq_right.mpr hai, inf_eq_left.mpr hai]
no goals
case h.mp.intro.intro.inr
ι : Type u_1
ι' : Type ?u.104527
E : Type ?u.104530
F : Type ?u.104533
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
exact ⟨mul_nonneg ht.1 hai, mul_le_of_le_one_left hai ht.2⟩
case h.mpr
ι : Type u_1
ι' : Type ?u.104527
E : Type ?u.104530
F : Type ?u.104533
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
case h.mpr
ι : Type u_1
ι' : Type ?u.104527
E : Type ?u.104530
F : Type ?u.104533
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
intro h
case h.mpr.refine'_1
ι : Type u_1
ι' : Type ?u.104527
E : Type ?u.104530
F : Type ?u.104533
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

case h.mpr.refine'_2
ι : Type u_1
ι' : Type ?u.104527
E : Type ?u.104530
F : Type ?u.104533
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
case h.mpr
ι : Type u_1
ι' : Type ?u.104527
E : Type ?u.104530
F : Type ?u.104533
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
refine' ⟨fun i => x i / a i, fun i => _, funext fun i => _⟩
case h.mpr.refine'_1
ι : Type u_1
ι' : Type ?u.104527
E : Type ?u.104530
F : Type ?u.104533
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
case h.mpr.refine'_1
ι : Type u_1
ι' : Type ?u.104527
E : Type ?u.104530
F : Type ?u.104533
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
specialize h i
case h.mpr.refine'_1.inl
ι : Type u_1
ι' : Type ?u.104527
E : Type ?u.104530
F : Type ?u.104533
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

case h.mpr.refine'_1.inr
ι : Type u_1
ι' : Type ?u.104527
E : Type ?u.104530
F : Type ?u.104533
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
case h.mpr.refine'_1
ι : Type u_1
ι' : Type ?u.104527
E : Type ?u.104530
F : Type ?u.104533
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
cases' le_total (a i) 0 with hai hai
case h.mpr.refine'_1.inl
ι : Type u_1
ι' : Type ?u.104527
E : Type ?u.104530
F : Type ?u.104533
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
case h.mpr.refine'_1.inl
ι : Type u_1
ι' : Type ?u.104527
E : Type ?u.104530
F : Type ?u.104533
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
rw [sup_eq_left.mpr hai, inf_eq_right.mpr hai] at h
no goals
case h.mpr.refine'_1.inl
ι : Type u_1
ι' : Type ?u.104527
E : Type ?u.104530
F : Type ?u.104533
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
exact ⟨div_nonneg_of_nonpos h.2 hai, div_le_one_of_ge h.1 hai⟩
case h.mpr.refine'_1.inr
ι : Type u_1
ι' : Type ?u.104527
E : Type ?u.104530
F : Type ?u.104533
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
case h.mpr.refine'_1.inr
ι : Type u_1
ι' : Type ?u.104527
E : Type ?u.104530
F : Type ?u.104533
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
rw [sup_eq_right.mpr hai, inf_eq_left.mpr hai] at h
no goals
case h.mpr.refine'_1.inr
ι : Type u_1
ι' : Type ?u.104527
E : Type ?u.104530
F : Type ?u.104533
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
exact ⟨div_nonneg h.1 hai, div_le_one_of_le h.2 hai⟩
case h.mpr.refine'_2
ι : Type u_1
ι' : Type ?u.104527
E : Type ?u.104530
F : Type ?u.104533
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
case h.mpr.refine'_2
ι : Type u_1
ι' : Type ?u.104527
E : Type ?u.104530
F : Type ?u.104533
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
specialize h i
case h.mpr.refine'_2
ι : Type u_1
ι' : Type ?u.104527
E : Type ?u.104530
F : Type ?u.104533
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
case h.mpr.refine'_2
ι : Type u_1
ι' : Type ?u.104527
E : Type ?u.104530
F : Type ?u.104533
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
simp only [smul_eq_mul, Pi.mul_apply]
case h.mpr.refine'_2.inl
ι : Type u_1
ι' : Type ?u.104527
E : Type ?u.104530
F : Type ?u.104533
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

case h.mpr.refine'_2.inr
ι : Type u_1
ι' : Type ?u.104527
E : Type ?u.104530
F : Type ?u.104533
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
case h.mpr.refine'_2
ι : Type u_1
ι' : Type ?u.104527
E : Type ?u.104530
F : Type ?u.104533
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
cases' eq_or_ne (a i) 0 with hai hai
case h.mpr.refine'_2.inl
ι : Type u_1
ι' : Type ?u.104527
E : Type ?u.104530
F : Type ?u.104533
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
case h.mpr.refine'_2.inl
ι : Type u_1
ι' : Type ?u.104527
E : Type ?u.104530
F : Type ?u.104533
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
rw [hai, inf_idem, sup_idem, ← le_antisymm_iff] at h
no goals
case h.mpr.refine'_2.inl
ι : Type u_1
ι' : Type ?u.104527
E : Type ?u.104530
F : Type ?u.104533
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
rw [hai, ← h, zero_div, MulZeroClass.zero_mul]
no goals
case h.mpr.refine'_2.inr
ι : Type u_1
ι' : Type ?u.104527
E : Type ?u.104530
F : Type ?u.104533
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
rw [div_mul_cancel _ hai]