awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
E : Type u_3
inst : Fintype ι
inst_1 : Fintype ι'
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
v : ι → E
e : ι' ≃ ι
K : Equiv.{u_2 + 1, u_1 + 1} (ι' → ℝ) (ι → ℝ) := Equiv.piCongrLeft' (fun (_a : ι') ↦ ℝ) e
this_1 :
  Eq.{u_1 + 1} (α := Set (ι → ℝ)) (Icc 0 1) (image.{u_2, u_1} (α := ι' → ℝ) (⇑K : (a : ι' → ℝ) → ι → ℝ) (Icc 0 1))
x : E
this :
  ∀ (z : ι' → ℝ),
    Eq.{u_3 + 1} (α := E) (∑ x : ι, z ((e.symm : (a : ι) → ι') x) • v x) (∑ i : ι', z i • v ((e : (a : ι') → ι) i))
h :
  Membership.mem (γ := Set E) ((fun (a : ι' → ℝ) ↦ ∑ x : ι', a x • v ((e : (a : ι') → ι) x)) '' Icc 0 1) x ↔
    Membership.mem (γ := Set E)
      ((fun (a : ι' → ℝ) ↦ ∑ i : ι, HSMul.hSMul (α := ℝ) ((K : (a : ι' → ℝ) → ι → ℝ) a i : ℝ) (v i)) '' Icc 0 1) x
h₁ :
  (∃ (x_1 : ι' → ℝ),
      Membership.mem (γ := Set (ι' → ℝ)) (Icc 0 1) x_1 ∧ ∑ x : ι', x_1 x • v ((e : (a : ι') → ι) x) = x) ↔
    ∃ (x_1 : ι' → ℝ),
      Membership.mem (γ := Set (ι' → ℝ)) (Icc 0 1) x_1 ∧
        ∑ i : ι, HSMul.hSMul (α := ℝ) ((K : (a : ι' → ℝ) → ι → ℝ) x_1 i : ℝ) (v i) = x
h₂ :
  (∃ (x_1 : ι' → ℝ), (0 ≤ x_1 ∧ x_1 ≤ 1) ∧ ∑ x : ι', x_1 x • v ((e : (a : ι') → ι) x) = x) ↔
    ∃ (x_1 : ι' → ℝ),
      (0 ≤ x_1 ∧ x_1 ≤ 1) ∧ ∑ i : ι, HSMul.hSMul (α := ℝ) ((K : (a : ι' → ℝ) → ι → ℝ) x_1 i : ℝ) (v i) = x
h₃ :
  (∃ (x_1 : ι' → ℝ), (0 ≤ x_1 ∧ x_1 ≤ 1) ∧ ∑ x : ι', x_1 x • v ((e : (a : ι') → ι) x) = x) ↔
    ∃ (x_1 : ι' → ℝ),
      (0 ≤ x_1 ∧ x_1 ≤ 1) ∧
        ∑ x : ι,
            HSMul.hSMul (α := ℝ) ((Equiv.piCongrLeft' (fun (_a : ι') ↦ ℝ) e : (a : ι' → ℝ) → ι → ℝ) x_1 x : ℝ) (v x) =
          x
⊢ Membership.mem (γ := Set E) ((fun (t : ι' → ℝ) ↦ ∑ i : ι', t i • (v ∘ (⇑e : (a : ι') → ι)) i) '' Icc 0 1) x ↔
    Membership.mem (γ := Set E)
      (image.{u_2, u_3} (α := ι' → ℝ) ((fun (t : ι → ℝ) ↦ ∑ i : ι, t i • v i) ∘ (⇑K : (a : ι' → ℝ) → ι → ℝ)) (Icc 0 1))
      x
have h₄ : (∃ (x_1 : ι' → ℝ), (0 ≤ x_1 ∧ x_1 ≤ 1) ∧ ∑ x : ι', x_1 x • v ((e : (a : ι') → ι) x) = x) ↔
  ∃ (x_1 : ι' → ℝ), (0 ≤ x_1 ∧ x_1 ≤ 1) ∧ ∑ x : ι, x_1 ((e.symm : (a : ι) → ι') x) • v x = x
Tactic: simp_rw [Function.comp_apply, mem_image, mem_Icc, K, Equiv.piCongrLeft'_apply, this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (goal)
Goal:
ι : Type u_1
inst : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
⊢ ι ≃ Fin 1
have h : Fintype.card ι = 1
Tactic: apply Fintype.equivFinOfCardEq
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (goal)
Goal:
ι : Type u_1
inst : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
⊢ Eq (α := Set ℝ) (parallelepiped (ι := ι) (⇑b : (a : ι) → ℝ)) (Icc 0 1) ∨
    Eq (α := Set ℝ) (parallelepiped (ι := ι) (⇑b : (a : ι) → ℝ)) (Icc (-1) 0)
have have : ∀ (e : ι ≃ Fin 1),
  Eq (α := Set ℝ) (parallelepiped (ι := ι) (⇑b : (a : ι) → ℝ)) (Icc 0 1) ∨
    Eq (α := Set ℝ) (parallelepiped (ι := ι) (⇑b : (a : ι) → ℝ)) (Icc (-1) 0)
Tactic: have e : ι ≃ Fin 1 := by
    apply Fintype.equivFinOfCardEq
    simp only [← finrank_eq_card_basis b.toBasis, finrank_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (goal)
Goal:
ι : Type u_1
inst : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
⊢ Eq (α := Set ℝ) (parallelepiped (ι := Fin 1) (⇑(b.reindex e) : (a : Fin 1) → ℝ))
    (parallelepiped (ι := ι) (⇑b : (a : ι) → ℝ))
have h : Eq (α := Fin 1 → ℝ) (⇑(b.reindex e) : (a : Fin 1) → ℝ)
  (Function.comp (β := ι) (⇑b : (a : ι) → ℝ) (⇑e.symm : (a : Fin 1) → ι))
Tactic: convert! parallelepiped_comp_equiv b e.symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (goal)
Goal:
ι : Type u_1
inst : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
⊢ Eq (α := Fin 1 → ℝ) (⇑(b.reindex e) : (a : Fin 1) → ℝ)
    (Function.comp (β := ι) (⇑b : (a : ι) → ℝ) (⇑e.symm : (a : Fin 1) → ι))
have h : ∀ (i : Fin 1),
  Eq (α := ℝ) ((b.reindex e : (a : Fin 1) → ℝ) i : ℝ)
    (Function.comp (β := ι) (⇑b : (a : ι) → ℝ) (⇑e.symm : (a : Fin 1) → ι) i : ℝ)
Tactic: ext i
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (hypothesis)
Goal:
ι : Type u_1
inst : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
⊢ Eq (α := Set ℝ) (parallelepiped (ι := ι) (⇑b : (a : ι) → ℝ)) (Icc 0 1) ∨
    Eq (α := Set ℝ) (parallelepiped (ι := ι) (⇑b : (a : ι) → ℝ)) (Icc (-1) 0)
have B : Eq (α := Set ℝ) (parallelepiped (ι := Fin 1) (⇑(b.reindex e) : (a : Fin 1) → ℝ))
  (parallelepiped (ι := ι) (⇑b : (a : ι) → ℝ))
Tactic: have B : parallelepiped (b.reindex e) = parallelepiped b := by
    convert! parallelepiped_comp_equiv b e.symm
    ext i
    simp only [OrthonormalBasis.coe_reindex]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (goal)
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 : ι) → ℝ))
⊢ Eq (α := Set ℝ) (parallelepiped (ι := ι) (⇑b : (a : ι) → ℝ)) (Icc 0 1) ∨
    Eq (α := Set ℝ) (parallelepiped (ι := ι) (⇑b : (a : ι) → ℝ)) (Icc (-1) 0)
have rw : 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: rw [← B]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (goal)
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
⊢ Icc 0 1 = F '' Icc 0 1
have h₁ : Icc 0 1 ⊆ F '' Icc 0 1
Tactic: apply Subset.antisymm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (goal)
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
h₁ : Icc 0 1 ⊆ F '' Icc 0 1
⊢ Icc 0 1 = F '' Icc 0 1
have h₂ : F '' Icc 0 1 ⊆ Icc 0 1
Tactic: apply Subset.antisymm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (goal)
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
x : Fin 1 → ℝ
hx : Membership.mem (γ := Set (Fin 1 → ℝ)) (Icc 0 1) x
⊢ x ∈ F '' Icc 0 1
have h₁ : F (x 0) = x
Tactic: refine ⟨x 0, ⟨hx.1 0, hx.2 0⟩, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (goal)
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
x : Fin 1 → ℝ
hx : Membership.mem (γ := Set (Fin 1 → ℝ)) (Icc 0 1) x
⊢ F (x 0) = x
have h₁ : ∀ (j : Fin 1), F (x 0) j = x j
Tactic: ext j
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (hypothesis)
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
⊢ 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)
have A : Icc 0 1 = F '' Icc 0 1
Tactic: 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 [F, Subsingleton.elim j 0]
    · rintro x ⟨y, hy, rfl⟩
      exact ⟨fun _j => hy.1, fun _j => hy.2⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (goal)
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
⊢ 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)
have inl : ∀ (H : Eq (α := (a : Fin 1) → ℝ) (⇑(b.reindex e) : (a : Fin 1) → ℝ) fun (x : Fin 1) ↦ 1),
  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: rcases orthonormalBasis_one_dim (b.reindex e) with (H | H)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (goal)
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
inl :
  ∀ (H : Eq (α := (a : Fin 1) → ℝ) (⇑(b.reindex e) : (a : Fin 1) → ℝ) fun (x : Fin 1) ↦ 1),
    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)
⊢ 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)
have inr : ∀ (H : Eq (α := (a : Fin 1) → ℝ) (⇑(b.reindex e) : (a : Fin 1) → ℝ) fun (x : Fin 1) ↦ -1),
  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: rcases orthonormalBasis_one_dim (b.reindex e) with (H | H)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (goal)
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 ℝ) (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)
have inl : Eq (α := Set ℝ) (parallelepiped (ι := Fin 1) (⇑(b.reindex e) : (a : Fin 1) → ℝ)) (Icc 0 1)
Tactic: left
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (goal)
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 ℝ) (parallelepiped (ι := Fin 1) (⇑(b.reindex e) : (a : Fin 1) → ℝ)) (Icc 0 1)
have inl : Eq (α := Set ℝ) ((fun (a : Fin 1 → ℝ) ↦ ∑ x : Fin 1, a x) '' F '' Icc 0 1) (Icc 0 1)
Tactic: simp_rw [parallelepiped, H, A, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (goal)
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 ℝ) (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)
have inr : Eq (α := Set ℝ) (parallelepiped (ι := Fin 1) (⇑(b.reindex e) : (a : Fin 1) → ℝ)) (Icc (-1) 0)
Tactic: right
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (goal)
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 ℝ) (parallelepiped (ι := Fin 1) (⇑(b.reindex e) : (a : Fin 1) → ℝ)) (Icc (-1) 0)
have inr : Eq (α := Set ℝ) ((fun (a : Fin 1 → ℝ) ↦ ∑ x : Fin 1, a x * -1) '' F '' Icc 0 1) (Icc (-1) 0)
Tactic: simp_rw [H, parallelepiped, smul_eq_mul, A]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (goal)
Goal:
ι : Type u_1
E : Type u_3
inst : Fintype ι
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
v : ι → E
⊢ parallelepiped v = ∑ i : ι, segment ℝ 0 (v i)
have h : ∀ (x : E), x ∈ parallelepiped v ↔ Membership.mem (γ := Set E) (∑ i : ι, segment ℝ 0 (v i)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (goal)
Goal:
ι : Type u_1
E : Type u_3
inst : Fintype ι
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
v : ι → E
x : E
⊢ x ∈ parallelepiped v ↔ Membership.mem (γ := Set E) (∑ i : ι, segment ℝ 0 (v i)) x
have 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
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (goal)
Goal:
ι : Type u_1
E : Type u_3
inst : Fintype ι
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
v : ι → E
x : E
⊢ (∃ (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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (goal)
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
⊢ (∃ (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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (goal)
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)
⊢ ∃ (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)
have 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)
Tactic: choose t ht hg using @hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (goal)
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)
have h : Eq.{u_3 + 1} (α := E) (∑ i : ι, g i) (∑ i : ι, t (i := i) • v i)
Tactic: refine ⟨@t, @ht, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (goal)
Goal:
ι : Type u_1
E : Type u_3
inst : Fintype ι
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
v : ι → E
⊢ Convex ℝ (parallelepiped v)
have rw : Convex.{0, u_3} ℝ (E := E) (∑ i : ι, segment ℝ 0 (v i))
Tactic: rw [parallelepiped_eq_sum_segment]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (goal)
Goal:
ι : Type u_1
E : Type u_3
inst : Fintype ι
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
v : ι → E
⊢ parallelepiped v = (convexHull ℝ : (a : Set E) → Set E) (∑ i : ι, {0, v i})
have simp_rw : parallelepiped v = ∑ i : ι, (convexHull ℝ : (a : Set E) → Set E) {0, v i}
Tactic: simp_rw [convexHull_sum, convexHull_pair, parallelepiped_eq_sum_segment]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (goal)
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}
⊢ parallelepiped v = (convexHull ℝ : (a : Set E) → Set E) (∑ i : ι, {0, v i})
have simp_rw₁ : parallelepiped v = ∑ x : ι, segment ℝ 0 (v x)
Tactic: simp_rw [convexHull_sum, convexHull_pair, parallelepiped_eq_sum_segment]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
a : ι → ℝ
⊢ (parallelepiped fun (i : ι) ↦ Pi.single (M := fun (i : ι) ↦ ℝ) i (a i)) = uIcc 0 a
have h : ∀ (x : (j : ι) → ℝ),
  Membership.mem (γ := Set ((j : ι) → ℝ)) (parallelepiped fun (i : ι) ↦ Pi.single (M := fun (i : ι) ↦ ℝ) i (a i)) x ↔
    x ∈ uIcc 0 a
Tactic: ext x
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
a x : (j : ι) → ℝ
⊢ Membership.mem (γ := Set ((j : ι) → ℝ)) (parallelepiped fun (i : ι) ↦ Pi.single (M := fun (i : ι) ↦ ℝ) i (a i)) x ↔
    x ∈ uIcc 0 a
have 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)
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 (_ : ι → ℝ)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
a x : (j : ι) → ℝ
⊢ (∃ (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)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (goal)
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)
⊢ (∃ (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)
have 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: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (hypothesis)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
a t : ι → ℝ
ht : ∀ (x : ι), 0 ≤ t x ∧ t x ≤ 1
i : ι
⊢ min 0 (a i) ≤ (t • a) i ∧ (t • a) i ≤ max 0 (a i)
have ht₁ : 0 ≤ t i ∧ t i ≤ 1
Tactic: specialize ht i
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
a t : ι → ℝ
i : ι
ht : 0 ≤ t i ∧ t i ≤ 1
⊢ min 0 (a i) ≤ t i * a i ∧ t i * a i ≤ max 0 (a i)
have h : ∀ (hai : a i ≤ 0), 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (goal)
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)
⊢ min 0 (a i) ≤ t i * a i ∧ t i * a i ≤ max 0 (a i)
have h₁ : ∀ (hai : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
a t : ι → ℝ
i : ι
ht : 0 ≤ t i ∧ t i ≤ 1
hai : a i ≤ 0
⊢ min 0 (a i) ≤ t i * a i ∧ t i * a i ≤ max 0 (a i)
have h : a i ≤ t i * a i ∧ t i * a i ≤ 0
Tactic: rw [sup_eq_left.mpr hai, inf_eq_right.mpr hai]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (goal)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
a t : ι → ℝ
i : ι
ht : 0 ≤ t i ∧ t i ≤ 1
hai : 0 ≤ a i
⊢ min 0 (a i) ≤ t i * a i ∧ t i * a i ≤ max 0 (a i)
have h : 0 ≤ t i * a i ∧ t i * a i ≤ a i
Tactic: rw [sup_eq_right.mpr hai, inf_eq_left.mpr hai]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (goal)
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
have h₁ : ∀ (i : ι), LE.le (α := ℝ) 0 ((fun (i : ι) ↦ x i / a i) i) ∧ LE.le (α := ℝ) ((fun (i : ι) ↦ x i / a i) i) 1
Tactic: refine ⟨fun i => x i / a i, fun i => ?_, funext fun i => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (goal)
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
⊢ ∃ (t : ι → ℝ), (∀ (x : ι), 0 ≤ t x ∧ t x ≤ 1) ∧ x = t • a
have h₂ : ∀ (i : ι), x i = HSMul.hSMul (α := (i : ι) → ℝ) (fun (i : ι) ↦ x i / a i) a i
Tactic: refine ⟨fun i => x i / a i, fun i => ?_, funext fun i => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (hypothesis)
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 : ι
⊢ LE.le (α := ℝ) 0 ((fun (i : ι) ↦ x i / a i) i) ∧ LE.le (α := ℝ) ((fun (i : ι) ↦ x i / a i) i) 1
have h₁ : min 0 (a i) ≤ x i ∧ x i ≤ max 0 (a i)
Tactic: specialize h i
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (goal)
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)
⊢ LE.le (α := ℝ) 0 ((fun (i : ι) ↦ x i / a i) i) ∧ LE.le (α := ℝ) ((fun (i : ι) ↦ x i / a i) i) 1
have 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
Tactic: rcases le_total (a i) 0 with hai | hai