awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
inst : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B :
  Eq (α := Set ℝ) (parallelepiped (ι := Fin 1) (⇑(b.reindex e) : (a : Fin 1) → ℝ))
    (parallelepiped (ι := ι) (⇑b : (a : ι) → ℝ))
F : ℝ → Fin 1 → ℝ := fun (t : ℝ) (_i : Fin 1) ↦ t
A : Icc 0 1 = F '' Icc 0 1
H : Eq (α := (a : Fin 1) → ℝ) (⇑(b.reindex e) : (a : Fin 1) → ℝ) fun (x : Fin 1) ↦ -1
inr : Eq (α := Set ℝ) (parallelepiped (ι := Fin 1) (⇑(b.reindex e) : (a : Fin 1) → ℝ)) (Icc (-1) 0)
⊢ Eq (α := Set ℝ) (parallelepiped (ι := Fin 1) (⇑(b.reindex e) : (a : Fin 1) → ℝ)) (Icc 0 1) ∨
    Eq (α := Set ℝ) (parallelepiped (ι := Fin 1) (⇑(b.reindex e) : (a : Fin 1) → ℝ)) (Icc (-1) 0)

Tactic:
right
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
inst : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B :
  Eq (α := Set ℝ) (parallelepiped (ι := Fin 1) (⇑(b.reindex e) : (a : Fin 1) → ℝ))
    (parallelepiped (ι := ι) (⇑b : (a : ι) → ℝ))
F : ℝ → Fin 1 → ℝ := fun (t : ℝ) (_i : Fin 1) ↦ t
A : Icc 0 1 = F '' Icc 0 1
H : Eq (α := (a : Fin 1) → ℝ) (⇑(b.reindex e) : (a : Fin 1) → ℝ) fun (x : Fin 1) ↦ -1
inr : Eq (α := Set ℝ) ((fun (a : Fin 1 → ℝ) ↦ ∑ x : Fin 1, a x * -1) '' F '' Icc 0 1) (Icc (-1) 0)
⊢ Eq (α := Set ℝ) (parallelepiped (ι := Fin 1) (⇑(b.reindex e) : (a : Fin 1) → ℝ)) (Icc (-1) 0)

Tactic:
simp_rw [H, parallelepiped, smul_eq_mul, A]

Premises used: smul_eq_mul, parallelepiped
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
inst : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
B :
  Eq (α := Set ℝ) (parallelepiped (ι := Fin 1) (⇑(b.reindex e) : (a : Fin 1) → ℝ))
    (parallelepiped (ι := ι) (⇑b : (a : ι) → ℝ))
F : ℝ → Fin 1 → ℝ := fun (t : ℝ) (_i : Fin 1) ↦ t
A : Icc 0 1 = F '' Icc 0 1
H : Eq (α := (a : Fin 1) → ℝ) (⇑(b.reindex e) : (a : Fin 1) → ℝ) fun (x : Fin 1) ↦ -1
⊢ Eq (α := Set ℝ) ((fun (a : Fin 1 → ℝ) ↦ ∑ 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]

Premises used: Set.neg_Icc, Set.image_neg_eq_neg, Function.comp, Finset.univ_unique, Finset.sum_singleton, Set.image_comp, Fin.default_eq_zero, mul_one, Finset.sum_neg_distrib, neg_zero, mul_neg
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
E : Type u_3
inst : Fintype ι
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
v : ι → E
h : ∀ (x : E), x ∈ parallelepiped v ↔ Membership.mem (γ := Set E) (∑ i : ι, segment ℝ 0 (v i)) x
⊢ parallelepiped v = ∑ i : ι, segment ℝ 0 (v i)

Tactic:
ext
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
E : Type u_3
inst : Fintype ι
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
v : ι → E
x : E
h :
  (∃ (t : ι → ℝ), (∀ (i : ι), Membership.mem (γ := Set ℝ) (Icc (0 i) (1 i)) (t i)) ∧ x = ∑ i : ι, t i • v i) ↔
    ∃ (g : ι → E) (_ : ∀ {i : ι}, Membership.mem (γ := Set E) ((fun (a : ℝ) ↦ a • v i) '' Icc 0 1) (g i)),
      ∑ i : ι, g i = x
⊢ x ∈ parallelepiped v ↔ Membership.mem (γ := Set E) (∑ i : ι, segment ℝ 0 (v i)) x

Tactic:
simp only [mem_parallelepiped_iff, Set.mem_finsetSum, Finset.mem_univ, forall_true_left,
    segment_eq_image, smul_zero, zero_add, ← Set.pi_univ_Icc, Set.mem_univ_pi]

Premises used: Finset.mem_univ, forall_true_left, smul_zero, segment_eq_image, zero_add, mem_parallelepiped_iff, Set.mem_finsetSum, Set.mem_univ_pi, Set.pi_univ_Icc
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
E : Type u_3
inst : Fintype ι
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
v : ι → E
x : E
h :
  (∃ (t : ι → ℝ), (∀ (i : ι), Membership.mem (γ := Set ℝ) (Icc (0 i) (1 i)) (t i)) ∧ x = ∑ i : ι, t i • v i) →
    ∃ (g : ι → E) (_ : ∀ {i : ι}, Membership.mem (γ := Set E) ((fun (a : ℝ) ↦ a • v i) '' Icc 0 1) (g i)),
      ∑ i : ι, g i = x
h₁ :
  (∃ (g : ι → E) (_ : ∀ {i : ι}, Membership.mem (γ := Set E) ((fun (a : ℝ) ↦ a • v i) '' Icc 0 1) (g i)),
      ∑ i : ι, g i = x) →
    ∃ (t : ι → ℝ), (∀ (i : ι), Membership.mem (γ := Set ℝ) (Icc (0 i) (1 i)) (t i)) ∧ x = ∑ i : ι, t i • v i
⊢ (∃ (t : ι → ℝ), (∀ (i : ι), Membership.mem (γ := Set ℝ) (Icc (0 i) (1 i)) (t i)) ∧ x = ∑ i : ι, t i • v i) ↔
    ∃ (g : ι → E) (_ : ∀ {i : ι}, Membership.mem (γ := Set E) ((fun (a : ℝ) ↦ a • v i) '' Icc 0 1) (g i)),
      ∑ i : ι, g i = x

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
E : Type u_3
inst : Fintype ι
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
v : ι → E
t : ι → ℝ
ht : ∀ (i : ι), Membership.mem (γ := Set ℝ) (Icc (0 i) (1 i)) (t i)
i : ι
⊢ (fun (a : ℝ) ↦ a • v i) (t i) = (t • v) i

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
E : Type u_3
inst : Fintype ι
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
v : ι → E
t : ι → ℝ
ht : ∀ (i : ι), Membership.mem (γ := Set ℝ) (Icc (0 i) (1 i)) (t i)
⊢ ∃ (g : ι → E) (_ : ∀ {i : ι}, Membership.mem (γ := Set E) ((fun (a : ℝ) ↦ a • v i) '' Icc 0 1) (g i)),
    Eq.{u_3 + 1} (α := E) (∑ i : ι, g i) (∑ i : ι, t i • v i)

Tactic:
exact ⟨t • v, fun {i} => ⟨t i, ht _, by simp⟩, rfl⟩
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
E : Type u_3
inst : Fintype ι
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
v g : ι → E
hg : ∀ {i : ι}, Membership.mem (γ := Set E) ((fun (a : ℝ) ↦ a • v i) '' Icc 0 1) (g i)
h :
  ∀ (t : {i : ι} → ℝ) (ht : ∀ {i : ι}, Membership.mem (γ := Set ℝ) (Icc 0 1) (t (i := i)))
    (hg : ∀ {i : ι}, (fun (a : ℝ) ↦ a • v i) (t (i := i)) = g i),
    ∃ (t : ι → ℝ),
      (∀ (i : ι), Membership.mem (γ := Set ℝ) (Icc (0 i) (1 i)) (t i)) ∧
        Eq.{u_3 + 1} (α := E) (∑ i : ι, g i) (∑ i : ι, t i • v i)
⊢ ∃ (t : ι → ℝ),
    (∀ (i : ι), Membership.mem (γ := Set ℝ) (Icc (0 i) (1 i)) (t i)) ∧
      Eq.{u_3 + 1} (α := E) (∑ i : ι, g i) (∑ i : ι, t i • v i)

Tactic:
choose t ht hg using @hg
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
E : Type u_3
inst : Fintype ι
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
v g : ι → E
t : {i : ι} → ℝ
ht : ∀ {i : ι}, Membership.mem (γ := Set ℝ) (Icc 0 1) (t (i := i))
hg : ∀ {i : ι}, (fun (a : ℝ) ↦ a • v i) (t (i := i)) = g i
⊢ ∃ (t : ι → ℝ),
    (∀ (i : ι), Membership.mem (γ := Set ℝ) (Icc (0 i) (1 i)) (t i)) ∧
      Eq.{u_3 + 1} (α := E) (∑ i : ι, g i) (∑ i : ι, t i • v i)

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

Premises used: And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
E : Type u_3
inst : Fintype ι
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
v g : ι → E
t : {i : ι} → ℝ
ht : ∀ {i : ι}, Membership.mem (γ := Set ℝ) (Icc 0 1) (t (i := i))
hg : ∀ {i : ι}, (fun (a : ℝ) ↦ a • v i) (t (i := i)) = g i
h : Eq.{u_3 + 1} (α := E) (∑ i : ι, g i) (∑ i : ι, t (i := i) • v i)
⊢ ∃ (t : ι → ℝ),
    (∀ (i : ι), Membership.mem (γ := Set ℝ) (Icc (0 i) (1 i)) (t i)) ∧
      Eq.{u_3 + 1} (α := E) (∑ i : ι, g i) (∑ i : ι, t i • v i)

Tactic:
refine ⟨@t, @ht, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
E : Type u_3
inst : Fintype ι
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
v g : ι → E
t : {i : ι} → ℝ
ht : ∀ {i : ι}, Membership.mem (γ := Set ℝ) (Icc 0 1) (t (i := i))
hg : ∀ {i : ι}, (fun (a : ℝ) ↦ a • v i) (t (i := i)) = g i
⊢ Eq.{u_3 + 1} (α := E) (∑ i : ι, g i) (∑ i : ι, t (i := i) • v i)

Tactic:
simp_rw [hg]
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
E : Type u_3
inst : Fintype ι
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
v : ι → E
rw : Convex.{0, u_3} ℝ (E := E) (∑ i : ι, segment ℝ 0 (v i))
⊢ Convex ℝ (parallelepiped v)

Tactic:
rw [parallelepiped_eq_sum_segment]

Premises used: parallelepiped_eq_sum_segment
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
E : Type u_3
inst : Fintype ι
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
v : ι → E
⊢ Convex.{0, u_3} ℝ (E := E) (∑ i : ι, segment ℝ 0 (v i))

Tactic:
convex_sum _ fun _i _hi => convex_segment _ _

Premises used: convex_sum, OfNat.ofNat, convex_segment
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
E : Type u_3
inst : Fintype ι
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
v : ι → E
⊢ Convex.{0, u_3} ℝ (E := E) (∑ i : ι, segment ℝ 0 (v i))

Tactic:
exact convex_sum _ fun _i _hi => convex_segment _ _

Premises used: convex_sum, convex_segment
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
E : Type u_3
inst : Fintype ι
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
v : ι → E
simp_rw : parallelepiped v = ∑ i : ι, (convexHull ℝ : (a : Set E) → Set E) {0, v i}
simp_rw₁ : parallelepiped v = ∑ x : ι, segment ℝ 0 (v x)
⊢ parallelepiped v = (convexHull ℝ : (a : Set E) → Set E) (∑ i : ι, {0, v i})

Tactic:
simp_rw [convexHull_sum, convexHull_pair, parallelepiped_eq_sum_segment]

Premises used: convexHull_pair, convexHull_sum, parallelepiped_eq_sum_segment
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
a : ι → ℝ
h :
  ∀ (x : (j : ι) → ℝ),
    Membership.mem (γ := Set ((j : ι) → ℝ)) (parallelepiped fun (i : ι) ↦ Pi.single (M := fun (i : ι) ↦ ℝ) i (a i)) x ↔
      x ∈ uIcc 0 a
⊢ (parallelepiped fun (i : ι) ↦ Pi.single (M := fun (i : ι) ↦ ℝ) i (a i)) = uIcc 0 a

Tactic:
ext x
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
a x : (j : ι) → ℝ
h :
  (∃ (t : ι → ℝ), (∀ (x : ι), 0 ≤ t x ∧ t x ≤ 1) ∧ x = t • a) ↔
    ∀ (x_1 : ι), min 0 (a x_1) ≤ x x_1 ∧ x x_1 ≤ max 0 (a x_1)
⊢ Membership.mem (γ := Set ((j : ι) → ℝ)) (parallelepiped fun (i : ι) ↦ Pi.single (M := fun (i : ι) ↦ ℝ) i (a i)) x ↔
    x ∈ uIcc 0 a

Tactic:
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 (_ : ι → ℝ)]

Premises used: Finset.univ_sum_single, Pi.one_apply, Pi.smul_apply', Pi.zero_apply, mem_parallelepiped_iff, Pi.sup_apply, Set.mem_Icc, Pi.single_smul', Pi.le_def, Pi.inf_apply, Set.uIcc, forall_and
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
a x : (j : ι) → ℝ
h :
  (∃ (t : ι → ℝ), (∀ (x : ι), 0 ≤ t x ∧ t x ≤ 1) ∧ x = t • a) →
    ∀ (x_1 : ι), min 0 (a x_1) ≤ x x_1 ∧ x x_1 ≤ max 0 (a x_1)
h₁ :
  (∀ (x_1 : ι), min 0 (a x_1) ≤ x x_1 ∧ x x_1 ≤ max 0 (a x_1)) →
    ∃ (t : ι → ℝ), (∀ (x : ι), 0 ≤ t x ∧ t x ≤ 1) ∧ x = t • a
⊢ (∃ (t : ι → ℝ), (∀ (x : ι), 0 ≤ t x ∧ t x ≤ 1) ∧ x = t • a) ↔
    ∀ (x_1 : ι), min 0 (a x_1) ≤ x x_1 ∧ x x_1 ≤ max 0 (a x_1)

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
a t : ι → ℝ
ht : ∀ (x : ι), 0 ≤ t x ∧ t x ≤ 1
i : ι
⊢ 0 ≤ t i ∧ t i ≤ 1

Tactic:
specialize ht i
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
a t : ι → ℝ
i : ι
ht : 0 ≤ t i ∧ t i ≤ 1
h : ∀ (hai : a i ≤ 0), min 0 (a i) ≤ t i * a i ∧ t i * a i ≤ max 0 (a i)
h₁ : ∀ (hai : 0 ≤ a i), min 0 (a i) ≤ t i * a i ∧ t i * a i ≤ max 0 (a i)
⊢ min 0 (a i) ≤ t i * a i ∧ t i * a i ≤ max 0 (a i)

Tactic:
rcases le_total (a i) 0 with hai | hai

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
a t : ι → ℝ
i : ι
ht : 0 ≤ t i ∧ t i ≤ 1
hai : a i ≤ 0
h : a i ≤ t i * a i ∧ t i * a i ≤ 0
⊢ min 0 (a i) ≤ t i * a i ∧ t i * a i ≤ max 0 (a i)

Tactic:
rw [sup_eq_left.mpr hai, inf_eq_right.mpr hai]

Premises used: Iff.mpr, sup_eq_left, inf_eq_right
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : 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

Tactic:
⟨le_mul_of_le_one_left hai ht.2, mul_nonpos_of_nonneg_of_nonpos ht.1 hai⟩

Premises used: And.right, And.left, And.intro, mul_nonpos_of_nonneg_of_nonpos, le_mul_of_le_one_left
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : 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

Tactic:
exact ⟨le_mul_of_le_one_left hai ht.2, mul_nonpos_of_nonneg_of_nonpos ht.1 hai⟩
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
a t : ι → ℝ
i : ι
ht : 0 ≤ t i ∧ t i ≤ 1
hai : 0 ≤ a i
h : 0 ≤ t i * a i ∧ t i * a i ≤ a i
⊢ min 0 (a i) ≤ t i * a i ∧ t i * a i ≤ max 0 (a i)

Tactic:
rw [sup_eq_right.mpr hai, inf_eq_left.mpr hai]

Premises used: Iff.mpr, sup_eq_right, inf_eq_left
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : 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

Tactic:
⟨mul_nonneg ht.1 hai, mul_le_of_le_one_left hai ht.2⟩

Premises used: mul_nonneg, mul_le_of_le_one_left, And.right, And.left, And.intro
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : 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

Tactic:
exact ⟨mul_nonneg ht.1 hai, mul_le_of_le_one_left hai ht.2⟩
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
a x : (j : ι) → ℝ
h : ∀ (x_1 : ι), min 0 (a x_1) ≤ x x_1 ∧ x x_1 ≤ max 0 (a x_1)
⊢ ∃ (t : ι → ℝ), (∀ (x : ι), 0 ≤ t x ∧ t x ≤ 1) ∧ x = t • a

Tactic:
⟨fun i => x i / a i, fun i => ?_, funext fun i => ?_⟩

Premises used: HDiv.hDiv, funext, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
a x : (j : ι) → ℝ
h : ∀ (x_1 : ι), min 0 (a x_1) ≤ x x_1 ∧ x x_1 ≤ max 0 (a x_1)
h₁ : ∀ (i : ι), LE.le (α := ℝ) 0 ((fun (i : ι) ↦ x i / a i) i) ∧ LE.le (α := ℝ) ((fun (i : ι) ↦ x i / a i) i) 1
h₂ : ∀ (i : ι), x i = HSMul.hSMul (α := (i : ι) → ℝ) (fun (i : ι) ↦ x i / a i) a i
⊢ ∃ (t : ι → ℝ), (∀ (x : ι), 0 ≤ t x ∧ t x ≤ 1) ∧ x = t • a

Tactic:
refine ⟨fun i => x i / a i, fun i => ?_, funext fun i => ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
a x : (j : ι) → ℝ
h : ∀ (x_1 : ι), min 0 (a x_1) ≤ x x_1 ∧ x x_1 ≤ max 0 (a x_1)
i : ι
⊢ min 0 (a i) ≤ x i ∧ x i ≤ max 0 (a i)

Tactic:
specialize h i
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
a x : (j : ι) → ℝ
i : ι
h : min 0 (a i) ≤ x i ∧ x i ≤ max 0 (a i)
h₁ : ∀ (hai : a i ≤ 0), LE.le (α := ℝ) 0 ((fun (i : ι) ↦ x i / a i) i) ∧ LE.le (α := ℝ) ((fun (i : ι) ↦ x i / a i) i) 1
h₂ : ∀ (hai : 0 ≤ a i), LE.le (α := ℝ) 0 ((fun (i : ι) ↦ x i / a i) i) ∧ LE.le (α := ℝ) ((fun (i : ι) ↦ x i / a i) i) 1
⊢ LE.le (α := ℝ) 0 ((fun (i : ι) ↦ x i / a i) i) ∧ LE.le (α := ℝ) ((fun (i : ι) ↦ x i / a i) i) 1

Tactic:
rcases le_total (a i) 0 with hai | hai

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
a x : (j : ι) → ℝ
i : ι
h : min 0 (a i) ≤ x i ∧ x i ≤ max 0 (a i)
hai : a i ≤ 0
⊢ a i ≤ x i ∧ x i ≤ 0

Tactic:
rw [sup_eq_left.mpr hai, inf_eq_right.mpr hai] at h

Premises used: Iff.mpr, sup_eq_left, inf_eq_right
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
a x : (j : ι) → ℝ
i : ι
h : min 0 (a i) ≤ x i ∧ x i ≤ max 0 (a i)
hai : a i ≤ 0
h₁ : a i ≤ x i ∧ x i ≤ 0
⊢ a i ≤ 0

Tactic:
rw [sup_eq_left.mpr hai, inf_eq_right.mpr hai] at h

Premises used: Iff.mpr, sup_eq_left, inf_eq_right
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
a x : (j : ι) → ℝ
i : ι
h : a i ≤ x i ∧ x i ≤ 0
hai : a i ≤ 0
⊢ LE.le (α := ℝ) 0 ((fun (i : ι) ↦ x i / a i) i) ∧ LE.le (α := ℝ) ((fun (i : ι) ↦ x i / a i) i) 1

Tactic:
⟨div_nonneg_of_nonpos h.2 hai, div_le_one_of_ge h.1 hai⟩

Premises used: div_nonneg_of_nonpos, div_le_one_of_ge, And.right, And.left, And.intro
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
a x : (j : ι) → ℝ
i : ι
h : a i ≤ x i ∧ x i ≤ 0
hai : a i ≤ 0
⊢ LE.le (α := ℝ) 0 ((fun (i : ι) ↦ x i / a i) i) ∧ LE.le (α := ℝ) ((fun (i : ι) ↦ x i / a i) i) 1

Tactic:
exact ⟨div_nonneg_of_nonpos h.2 hai, div_le_one_of_ge h.1 hai⟩
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
a x : (j : ι) → ℝ
i : ι
h : min 0 (a i) ≤ x i ∧ x i ≤ max 0 (a i)
hai : 0 ≤ a i
⊢ 0 ≤ x i ∧ x i ≤ a i

Tactic:
rw [sup_eq_right.mpr hai, inf_eq_left.mpr hai] at h

Premises used: Iff.mpr, sup_eq_right, inf_eq_left
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
a x : (j : ι) → ℝ
i : ι
h : min 0 (a i) ≤ x i ∧ x i ≤ max 0 (a i)
hai : 0 ≤ a i
h₁ : 0 ≤ x i ∧ x i ≤ a i
⊢ 0 ≤ a i

Tactic:
rw [sup_eq_right.mpr hai, inf_eq_left.mpr hai] at h

Premises used: Iff.mpr, sup_eq_right, inf_eq_left
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
a x : (j : ι) → ℝ
i : ι
h : 0 ≤ x i ∧ x i ≤ a i
hai : 0 ≤ a i
⊢ LE.le (α := ℝ) 0 ((fun (i : ι) ↦ x i / a i) i) ∧ LE.le (α := ℝ) ((fun (i : ι) ↦ x i / a i) i) 1

Tactic:
⟨div_nonneg h.1 hai, div_le_one_of_le₀ h.2 hai⟩

Premises used: div_le_one_of_le₀, And.right, And.left, And.intro, div_nonneg
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
a x : (j : ι) → ℝ
i : ι
h : 0 ≤ x i ∧ x i ≤ a i
hai : 0 ≤ a i
⊢ LE.le (α := ℝ) 0 ((fun (i : ι) ↦ x i / a i) i) ∧ LE.le (α := ℝ) ((fun (i : ι) ↦ x i / a i) i) 1

Tactic:
exact ⟨div_nonneg h.1 hai, div_le_one_of_le₀ h.2 hai⟩
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
a x : (j : ι) → ℝ
i : ι
h : min 0 (a i) ≤ x i ∧ x i ≤ max 0 (a i)
h₁ : ∀ (hai : a i = 0), x i = x i / a i * a i
h₂ : ∀ (hai : a i ≠ 0), x i = x i / a i * a i
⊢ x i = x i / a i * a i

Tactic:
rcases eq_or_ne (a i) 0 with hai | hai

Premises used: eq_or_ne, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
a x : (j : ι) → ℝ
i : ι
h : min 0 (a i) ≤ x i ∧ x i ≤ max 0 (a i)
hai : a i = 0
⊢ 0 = x i

Tactic:
rw [hai, inf_idem, sup_idem, ← le_antisymm_iff] at h

Premises used: sup_idem, le_antisymm_iff, inf_idem
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
a x : (j : ι) → ℝ
i : ι
h : min 0 (a i) ≤ x i ∧ x i ≤ max 0 (a i)
hai : a i = 0
h₁ : 0 = x i
⊢ a i = 0

Tactic:
rw [hai, inf_idem, sup_idem, ← le_antisymm_iff] at h

Premises used: sup_idem, le_antisymm_iff, inf_idem
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
a x : (j : ι) → ℝ
i : ι
h : 0 = x i
hai : a i = 0
h₁ : x i = x i / 0 * 0
h₂ : 0 = 0 / 0 * 0
h₃ : 0 = HMul.hMul (α := ℝ) 0 0
h₄ h₅ : Eq (α := ℝ) 0 0
⊢ x i = x i / a i * a i

Tactic:
rw [hai, ← h, zero_div, zero_mul]

Premises used: MulZeroClass.zero_mul, zero_div
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
a x : (j : ι) → ℝ
i : ι
h : min 0 (a i) ≤ x i ∧ x i ≤ max 0 (a i)
hai : a i ≠ 0
h₁ h₂ : x i = x i
⊢ x i = x i / a i * a i

Tactic:
rw [div_mul_cancel₀ _ hai]

Premises used: div_mul_cancel₀
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst : Fintype ι
inst_1 : Fintype ι'
inst_2 : NormedAddCommGroup E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ E
inst_5 : NormedSpace ℝ F
b : Basis ι ℝ E
i : ι
_H : Membership.mem (γ := Finset ι) Finset.univ i
⊢ Continuous.{u_1, u_3} (Y := E) fun (t : ι → ℝ) ↦ HSMul.hSMul (β := E) (t i) ((b : (a : ι) → E) i : E)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst : Fintype ι
inst_1 : Fintype ι'
inst_2 : NormedAddCommGroup E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ E
inst_5 : NormedSpace ℝ F
b : Basis ι ℝ E
H :
  Set.Nonempty.{u_3} (α := E)
    (interior
      (image.{u_1, u_3} (α := ι → ℝ)
        (⇑(ContinuousLinearEquiv.toHomeomorph (ContinuousLinearEquiv.symm b.equivFunL)) : (a : ι → ℝ) → E) (Icc 0 1)))
⊢ Set.Nonempty.{u_3} (α := E)
    (interior
      (image.{u_1, u_3} (α := ι → ℝ)
        (⇑(ContinuousLinearEquiv.toHomeomorph (ContinuousLinearEquiv.symm b.equivFunL)) : (a : ι → ℝ) → E) (Icc 0 1)))

Tactic:
H
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst : Fintype ι
inst_1 : Fintype ι'
inst_2 : NormedAddCommGroup E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ E
inst_5 : NormedSpace ℝ F
b : Basis ι ℝ E
H :
  Set.Nonempty.{u_3} (α := E)
    (interior
      (image.{u_1, u_3} (α := ι → ℝ)
        (⇑(ContinuousLinearEquiv.toHomeomorph (ContinuousLinearEquiv.symm b.equivFunL)) : (a : ι → ℝ) → E) (Icc 0 1)))
h :
  ∀ (a : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) (Icc 0 1) a →
      Eq.{u_3 + 1} (α := E) (∑ i : ι, HSMul.hSMul (β := E) (a i) ((b : (a : ι) → E) i : E) : E)
        ((ContinuousLinearEquiv.toHomeomorph (ContinuousLinearEquiv.symm b.equivFunL) : (a : ι → ℝ) → E) a : E)
⊢ Set.Nonempty.{u_3} (α := E)
    (interior ((fun (t : ι → ℝ) ↦ ∑ i : ι, HSMul.hSMul (β := E) (t i) ((b : (a : ι) → E) i : E)) '' Icc 0 1))

Tactic:
convert! H
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst : Fintype ι
inst_1 : Fintype ι'
inst_2 : NormedAddCommGroup E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ E
inst_5 : NormedSpace ℝ F
b : Basis ι ℝ E
H :
  Set.Nonempty.{u_3} (α := E)
    (interior
      (image.{u_1, u_3} (α := ι → ℝ)
        (⇑(ContinuousLinearEquiv.toHomeomorph (ContinuousLinearEquiv.symm b.equivFunL)) : (a : ι → ℝ) → E) (Icc 0 1)))
a : ι → ℝ
h : Membership.mem (γ := Set (ι → ℝ)) (Icc 0 1) a
⊢ Eq.{u_3 + 1} (α := E) (∑ i : ι, HSMul.hSMul (β := E) (a i) ((b : (a : ι) → E) i : E) : E)
    ((ContinuousLinearEquiv.toHomeomorph (ContinuousLinearEquiv.symm b.equivFunL) : (a : ι → ℝ) → E) a : E)

Tactic:
(b.equivFun_symm_apply _).symm

Premises used: Module.Basis.equivFun_symm_apply, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst : Fintype ι
inst_1 : Fintype ι'
inst_2 : NormedAddCommGroup E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ E
inst_5 : NormedSpace ℝ F
b : Basis ι ℝ E
H :
  Set.Nonempty.{u_3} (α := E)
    (interior
      (image.{u_1, u_3} (α := ι → ℝ)
        (⇑(ContinuousLinearEquiv.toHomeomorph (ContinuousLinearEquiv.symm b.equivFunL)) : (a : ι → ℝ) → E) (Icc 0 1)))
a : ι → ℝ
h : Membership.mem (γ := Set (ι → ℝ)) (Icc 0 1) a
⊢ Eq.{u_3 + 1} (α := E) (∑ i : ι, HSMul.hSMul (β := E) (a i) ((b : (a : ι) → E) i : E) : E)
    ((ContinuousLinearEquiv.toHomeomorph (ContinuousLinearEquiv.symm b.equivFunL) : (a : ι → ℝ) → E) a : E)

Tactic:
exact (b.equivFun_symm_apply _).symm

Premises used: Module.Basis.equivFun_symm_apply, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst : Fintype ι
inst_1 : Fintype ι'
inst_2 : NormedAddCommGroup E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ E
inst_5 : NormedSpace ℝ F
b : Basis ι ℝ E
suffices :
  Set.Nonempty.{u_3} (α := E)
    (interior
      (image.{u_1, u_3} (α := ι → ℝ)
        (⇑(ContinuousLinearEquiv.toHomeomorph (ContinuousLinearEquiv.symm b.equivFunL)) : (a : ι → ℝ) → E) (Icc 0 1)))
⊢ Set.Nonempty.{u_3} (α := E) (interior (_root_.parallelepiped.{u_1, u_3} (ι := ι) (⇑b : (a : ι) → E)))

Tactic:
suffices H : Set.Nonempty (interior (b.equivFunL.symm.toHomeomorph '' Icc 0 1)) by
      dsimp only [_root_.parallelepiped]
      convert! H
      exact (b.equivFun_symm_apply _).symm