awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.NormedSpace (goal)
Goal:
F : Type u_1
inst : NormedAddCommGroup F
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
μ : Measure E
inst_6 : μ.IsAddHaarMeasure
f : E → F
R : ℝ
hR : R ≠ 0
this : ∀ {g : E → F}, Integrable g μ → ∀ {S : ℝ}, S ≠ 0 → Integrable.{u_1, u_2} (ε := F) (fun (x : E) ↦ g (S • x)) μ
hf : Integrable.{u_1, u_2} (ε := F) (fun (x : E) ↦ f (R • x)) μ
x : E
⊢ x = R • R⁻¹ • x
have h : x = (R * R⁻¹) • x
Tactic: rw [← mul_smul, mul_inv_cancel₀ hR, one_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.NormedSpace (goal)
Goal:
F : Type u_1
inst : NormedAddCommGroup F
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
μ : Measure E
inst_6 : μ.IsAddHaarMeasure
f : E → F
R : ℝ
hR : R ≠ 0
this : ∀ {g : E → F}, Integrable g μ → ∀ {S : ℝ}, S ≠ 0 → Integrable.{u_1, u_2} (ε := F) (fun (x : E) ↦ g (S • x)) μ
hf : Integrable.{u_1, u_2} (ε := F) (fun (x : E) ↦ f (R • x)) μ
x : E
h : x = (R * R⁻¹) • x
⊢ x = R • R⁻¹ • x
have h₁ : x = HSMul.hSMul (α := ℝ) 1 x
Tactic: rw [← mul_smul, mul_inv_cancel₀ hR, one_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.NormedSpace (goal)
Goal:
F : Type u_1
inst : NormedAddCommGroup F
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
μ : Measure E
inst_6 : μ.IsAddHaarMeasure
f : E → F
R : ℝ
hR : R ≠ 0
this : ∀ {g : E → F}, Integrable g μ → ∀ {S : ℝ}, S ≠ 0 → Integrable.{u_1, u_2} (ε := F) (fun (x : E) ↦ g (S • x)) μ
hf : Integrable.{u_1, u_2} (ε := F) (fun (x : E) ↦ f (R • x)) μ
x : E
h : x = (R * R⁻¹) • x
h₁ : x = HSMul.hSMul (α := ℝ) 1 x
⊢ x = R • R⁻¹ • x
have h₂ : x = x
Tactic: rw [← mul_smul, mul_inv_cancel₀ hR, one_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.NormedSpace (goal)
Goal:
F : Type u_1
inst : NormedAddCommGroup F
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
μ : Measure E
inst_6 : μ.IsAddHaarMeasure
f : E → F
R : ℝ
hR : R ≠ 0
⊢ Integrable.{u_1, u_2} (ε := F) (fun (x : E) ↦ f (R • x)) μ ↔ Integrable f μ
have E₁ : ∀ {g : E → F}, Integrable g μ → ∀ {S : ℝ}, S ≠ 0 → Integrable.{u_1, u_2} (ε := F) (fun (x : E) ↦ g (S • x)) μ
Tactic: suffices
    ∀ {g : E → F} (_ : Integrable g μ) {S : ℝ} (_ : S ≠ 0), Integrable (fun x => g (S • x)) μ by
    refine ⟨fun hf => ?_, fun hf => this hf hR⟩
    convert! this hf (inv_ne_zero hR)
    rw [← mul_smul, mul_inv_cancel₀ hR, one_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.NormedSpace (goal)
Goal:
F : Type u_1
inst : NormedAddCommGroup F
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
μ : Measure E
inst_6 : μ.IsAddHaarMeasure
f : E → F
R : ℝ
hR : R ≠ 0
g : E → F
hg : Integrable g μ
S : ℝ
hS : S ≠ 0
t : E ≃ᵐ E := Homeomorph.toMeasurableEquiv (Homeomorph.smul ⋯.unit)
⊢ Integrable.{u_1, u_2} (ε := F) (fun (x : E) ↦ g (S • x)) μ
have refine : @Integrable _ _ _ _ inst_3 g (Measure.map (fun (x : E) ↦ S • x) μ)
Tactic: refine (integrable_map_equiv t g).mp (?_ : Integrable g (map (S • ·) μ))
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.NormedSpace (goal)
Goal:
F : Type u_1
inst : NormedAddCommGroup F
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : FiniteDimensional ℝ E
μ : Measure E
inst_6 : μ.IsAddHaarMeasure
f : E → F
R : ℝ
hR : R ≠ 0
g : E → F
hg : Integrable g μ
S : ℝ
hS : S ≠ 0
t : E ≃ᵐ E := Homeomorph.toMeasurableEquiv (Homeomorph.smul ⋯.unit)
⊢ @Integrable _ _ _ _ inst_3 g (Measure.map (fun (x : E) ↦ S • x) μ)
have rwa : ENNReal.ofReal |(S ^ finrank ℝ E)⁻¹| ≠ 0
Tactic: rwa [map_addHaar_smul μ hS, integrable_smul_measure _ ENNReal.ofReal_ne_top]
-- 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
b : Basis ι ℝ E
⊢ Eq.{u_3 + 1} (α := Set E) (parallelepiped.{u_1, u_3} (ι := ι) (⇑b : (a : ι) → E))
    {x : E |
      ∀ (i : ι),
        Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ)}
have h : ∀ (x : E),
  Membership.mem (γ := Set E) (parallelepiped.{u_1, u_3} (ι := ι) (⇑b : (a : ι) → E)) x ↔
    Membership.mem (γ := Set E)
      {x : E |
        ∀ (i : ι),
          Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1)
            ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ)}
      x
Tactic: ext x
-- 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
b : Basis ι ℝ E
x : E
⊢ Membership.mem (γ := Set E) (parallelepiped.{u_1, u_3} (ι := ι) (⇑b : (a : ι) → E)) x ↔
    Membership.mem (γ := Set E)
      {x : E |
        ∀ (i : ι),
          Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1)
            ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ)}
      x
have h : (∃ (t : ι → ℝ),
    ∀ (x_1 : ι), (0 ≤ t x_1 ∧ t x_1 ≤ 1) ∧ (((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) x_1 = t x_1) ↔
  ∀ (i : ι),
    LE.le (α := ℝ) (0 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ) ∧
      LE.le (α := ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ) (1 : ℝ)
Tactic: simp_rw [mem_parallelepiped_iff, mem_setOf_eq, b.ext_elem_iff, _root_.map_sum,
    map_smul, Finset.sum_apply', Basis.repr_self, Finsupp.smul_single, smul_eq_mul,
    mul_one, Finsupp.single_apply, Finset.sum_ite_eq', Finset.mem_univ, ite_true, mem_Icc,
    Pi.le_def, Pi.zero_apply, Pi.one_apply, ← forall_and]
-- 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
b : Basis ι ℝ E
⊢ Eq.{u_3 + 1} (α := Set E) (parallelepiped.{u_1, u_3} (ι := ι) (⇑b : (a : ι) → E))
    {x : E |
      ∀ (i : ι),
        Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ)}
have h : ∀ (x : E),
  Membership.mem (γ := Set E) (parallelepiped.{u_1, u_3} (ι := ι) (⇑b : (a : ι) → E)) x ↔
    Membership.mem (γ := Set E)
      {x : E |
        ∀ (i : ι),
          Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1)
            ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ)}
      x
Tactic: classical
  ext x
  simp_rw [mem_parallelepiped_iff, mem_setOf_eq, b.ext_elem_iff, _root_.map_sum,
    map_smul, Finset.sum_apply', Basis.repr_self, Finsupp.smul_single, smul_eq_mul,
    mul_one, Finsupp.single_apply, Finset.sum_ite_eq', Finset.mem_univ, ite_true, mem_Icc,
    Pi.le_def, Pi.zero_apply, Pi.one_apply, ← forall_and]
  aesop
-- 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
b : Basis ι ℝ E
h :
  ∀ (x : E),
    Membership.mem (γ := Set E) (parallelepiped.{u_1, u_3} (ι := ι) (⇑b : (a : ι) → E)) x ↔
      Membership.mem (γ := Set E)
        {x : E |
          ∀ (i : ι),
            Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1)
              ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ)}
        x
⊢ Eq.{u_3 + 1} (α := Set E) (parallelepiped.{u_1, u_3} (ι := ι) (⇑b : (a : ι) → E))
    {x : E |
      ∀ (i : ι),
        Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ)}
have h₁ : ∀ (x : E),
  (∃ (t : ι → ℝ),
      ∀ (x_1 : ι), (0 ≤ t x_1 ∧ t x_1 ≤ 1) ∧ (((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) x_1 = t x_1) ↔
    ∀ (i : ι),
      LE.le (α := ℝ) (0 : ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ) ∧
        LE.le (α := ℝ) ((((b.repr : (a : E) → ι →₀ ℝ) x : ι →₀ ℝ) : (a : ι) → ℝ) i : ℝ) (1 : ℝ)
Tactic: classical
  ext x
  simp_rw [mem_parallelepiped_iff, mem_setOf_eq, b.ext_elem_iff, _root_.map_sum,
    map_smul, Finset.sum_apply', Basis.repr_self, Finsupp.smul_single, smul_eq_mul,
    mul_one, Finsupp.single_apply, Finset.sum_ite_eq', Finset.mem_univ, ite_true, mem_Icc,
    Pi.le_def, Pi.zero_apply, Pi.one_apply, ← forall_and]
  aesop
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (goal)
Goal:
ι : Type u_1
E : Type u_3
F : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
inst_3 : AddCommGroup F
inst_4 : Module ℝ F
f : E →ₗ[ℝ] F
v : ι → E
⊢ Eq.{u_4 + 1} (α := Set F) ((⇑f : (a : E) → F) '' parallelepiped v) (parallelepiped ((⇑f : (a : E) → F) ∘ v))
have simp : Eq.{u_4 + 1} (α := Set F)
  (image.{u_1, u_4} (α := ι → ℝ)
    (Function.comp.{u_1 + 1, u_3 + 1, u_4 + 1} (β := E) (⇑f : (a : E) → F) fun (t : ι → ℝ) ↦ ∑ i : ι, t i • v i)
    (Icc 0 1))
  ((fun (t : ι → ℝ) ↦ ∑ i : ι, HSMul.hSMul (β := F) (t i) (((⇑f : (a : E) → F) ∘ v) i)) '' Icc 0 1)
Tactic: simp only [parallelepiped, ← image_comp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (goal)
Goal:
ι : Type u_1
E : Type u_3
F : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
inst_3 : AddCommGroup F
inst_4 : Module ℝ F
f : E →ₗ[ℝ] F
v : ι → E
⊢ Eq.{u_4 + 1} (α := Set F)
    (image.{u_1, u_4} (α := ι → ℝ)
      (Function.comp.{u_1 + 1, u_3 + 1, u_4 + 1} (β := E) (⇑f : (a : E) → F) fun (t : ι → ℝ) ↦ ∑ i : ι, t i • v i)
      (Icc 0 1))
    ((fun (t : ι → ℝ) ↦ ∑ i : ι, HSMul.hSMul (β := F) (t i) (((⇑f : (a : E) → F) ∘ v) i)) '' Icc 0 1)
have e_f : ∀ (t : ι → ℝ),
  Eq.{u_4 + 1} (α := F)
    (Function.comp.{u_1 + 1, u_3 + 1, u_4 + 1} (β := E) (⇑f : (a : E) → F) (fun (t : ι → ℝ) ↦ ∑ i : ι, t i • v i) t)
    (∑ i : ι, HSMul.hSMul (β := F) (t i) (((⇑f : (a : E) → F) ∘ v) i))
Tactic: congr 1 with t
-- 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
⊢ Eq.{u_1 + 1} (α := Set (ι → ℝ)) (Icc 0 1) (image.{u_2, u_1} (α := ι' → ℝ) (⇑K : (a : ι' → ℝ) → ι → ℝ) (Icc 0 1))
have rw : Eq.{u_2 + 1} (α := Set (ι' → ℝ)) (preimage.{u_2, u_1} (β := ι → ℝ) (⇑K : (a : ι' → ℝ) → ι → ℝ) (Icc 0 1)) (Icc 0 1)
Tactic: rw [← Equiv.preimage_eq_iff_eq_image]
-- 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
⊢ Eq.{u_2 + 1} (α := Set (ι' → ℝ)) (preimage.{u_2, u_1} (β := ι → ℝ) (⇑K : (a : ι' → ℝ) → ι → ℝ) (Icc 0 1)) (Icc 0 1)
have h : ∀ (x : ι' → ℝ),
  Membership.mem (γ := Set (ι' → ℝ)) (preimage.{u_2, u_1} (β := ι → ℝ) (⇑K : (a : ι' → ℝ) → ι → ℝ) (Icc 0 1)) x ↔
    Membership.mem (γ := Set (ι' → ℝ)) (Icc 0 1) x
Tactic: ext x
-- 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
x : ι' → ℝ
⊢ Membership.mem (γ := Set (ι' → ℝ)) (preimage.{u_2, u_1} (β := ι → ℝ) (⇑K : (a : ι' → ℝ) → ι → ℝ) (Icc 0 1)) x ↔
    Membership.mem (γ := Set (ι' → ℝ)) (Icc 0 1) x
have h : ((∀ (i : ι), 0 ≤ x ((e.symm : (a : ι) → ι') i)) ∧ ∀ (i : ι), x ((e.symm : (a : ι) → ι') i) ≤ 1) ↔
  (∀ (i : ι'), 0 ≤ x i) ∧ ∀ (i : ι'), x i ≤ 1
Tactic: simp only [K, mem_preimage, mem_Icc, Pi.le_def, Pi.zero_apply, Equiv.piCongrLeft'_apply,
      Pi.one_apply]
-- 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
x : ι' → ℝ
⊢ ((∀ (i : ι), 0 ≤ x ((e.symm : (a : ι) → ι') i)) ∧ ∀ (i : ι), x ((e.symm : (a : ι) → ι') i) ≤ 1) ↔
    (∀ (i : ι'), 0 ≤ x i) ∧ ∀ (i : ι'), x i ≤ 1
have h : ∀ (h : (∀ (i : ι), 0 ≤ x ((e.symm : (a : ι) → ι') i)) ∧ ∀ (i : ι), x ((e.symm : (a : ι) → ι') i) ≤ 1) (i : ι'), 0 ≤ x i
Tactic: refine
      ⟨fun h => ⟨fun i => ?_, fun i => ?_⟩, fun h =>
        ⟨fun i => h.1 (e.symm i), fun i => h.2 (e.symm i)⟩⟩
-- 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
x : ι' → ℝ
h :
  ∀ (h : (∀ (i : ι), 0 ≤ x ((e.symm : (a : ι) → ι') i)) ∧ ∀ (i : ι), x ((e.symm : (a : ι) → ι') i) ≤ 1) (i : ι'),
    0 ≤ x i
⊢ ((∀ (i : ι), 0 ≤ x ((e.symm : (a : ι) → ι') i)) ∧ ∀ (i : ι), x ((e.symm : (a : ι) → ι') i) ≤ 1) ↔
    (∀ (i : ι'), 0 ≤ x i) ∧ ∀ (i : ι'), x i ≤ 1
have h₁ : ∀ (h : (∀ (i : ι), 0 ≤ x ((e.symm : (a : ι) → ι') i)) ∧ ∀ (i : ι), x ((e.symm : (a : ι) → ι') i) ≤ 1) (i : ι'), x i ≤ 1
Tactic: refine
      ⟨fun h => ⟨fun i => ?_, fun i => ?_⟩, fun h =>
        ⟨fun i => h.1 (e.symm i), fun i => h.2 (e.symm i)⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (hypothesis)
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
⊢ Eq.{u_3 + 1} (α := Set E) ((fun (t : ι' → ℝ) ↦ ∑ i : ι', t i • (v ∘ (⇑e : (a : ι') → ι)) i) '' Icc 0 1)
    ((fun (t : ι → ℝ) ↦ ∑ i : ι, t i • v i) '' Icc 0 1)
have this : Eq.{u_1 + 1} (α := Set (ι → ℝ)) (Icc 0 1) (image.{u_2, u_1} (α := ι' → ℝ) (⇑K : (a : ι' → ℝ) → ι → ℝ) (Icc 0 1))
Tactic: have : Icc (0 : ι → ℝ) 1 = K '' Icc (0 : ι' → ℝ) 1 := by
    rw [← Equiv.preimage_eq_iff_eq_image]
    ext x
    simp only [K, 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)
-- 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 : Eq.{u_1 + 1} (α := Set (ι → ℝ)) (Icc 0 1) (image.{u_2, u_1} (α := ι' → ℝ) (⇑K : (a : ι' → ℝ) → ι → ℝ) (Icc 0 1))
⊢ Eq.{u_3 + 1} (α := Set E) ((fun (t : ι' → ℝ) ↦ ∑ i : ι', t i • (v ∘ (⇑e : (a : ι') → ι)) i) '' Icc 0 1)
    ((fun (t : ι → ℝ) ↦ ∑ i : ι, t i • v i) '' Icc 0 1)
have rw : Eq.{u_3 + 1} (α := Set E) ((fun (t : ι' → ℝ) ↦ ∑ i : ι', t i • (v ∘ (⇑e : (a : ι') → ι)) i) '' Icc 0 1)
  (image.{u_2, u_3} (α := ι' → ℝ) ((fun (t : ι → ℝ) ↦ ∑ i : ι, t i • v i) ∘ (⇑K : (a : ι' → ℝ) → ι → ℝ)) (Icc 0 1))
Tactic: rw [this, ← image_comp]
-- 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 : Eq.{u_1 + 1} (α := Set (ι → ℝ)) (Icc 0 1) (image.{u_2, u_1} (α := ι' → ℝ) (⇑K : (a : ι' → ℝ) → ι → ℝ) (Icc 0 1))
⊢ Eq.{u_3 + 1} (α := Set E) ((fun (t : ι' → ℝ) ↦ ∑ i : ι', t i • (v ∘ (⇑e : (a : ι') → ι)) i) '' Icc 0 1)
    (image.{u_2, u_3} (α := ι' → ℝ) ((fun (t : ι → ℝ) ↦ ∑ i : ι, t i • v i) ∘ (⇑K : (a : ι' → ℝ) → ι → ℝ)) (Icc 0 1))
have h : ∀ (x : E),
  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
Tactic: ext x
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (hypothesis)
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 : Eq.{u_1 + 1} (α := Set (ι → ℝ)) (Icc 0 1) (image.{u_2, u_1} (α := ι' → ℝ) (⇑K : (a : ι' → ℝ) → ι → ℝ) (Icc 0 1))
x : E
⊢ 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 this₁ : ∀ (z : ι' → ℝ),
  Eq.{u_3 + 1} (α := E)
    (∑ i : ι, z ((e.symm : (a : ι) → ι') i) • v ((e : (a : ι') → ι) ((e.symm : (a : ι) → ι') i : ι')))
    (∑ i : ι', z i • v ((e : (a : ι') → ι) i))
Tactic: have := fun z : ι' → ℝ => e.symm.sum_comp fun i => z i • v (e i)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (hypothesis)
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)
      (∑ i : ι, z ((e.symm : (a : ι) → ι') i) • v ((e : (a : ι') → ι) ((e.symm : (a : ι) → ι') i : ι')))
      (∑ i : ι', z i • v ((e : (a : ι') → ι) i))
⊢ 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 this₁ : ∀ (z : ι' → ℝ),
  Eq.{u_3 + 1} (α := E) (∑ x : ι, z ((e.symm : (a : ι) → ι') x) • v x) (∑ i : ι', z i • v ((e : (a : ι') → ι) i))
Tactic: simp_rw [Equiv.apply_symm_apply] at this
Cleared hypotheses: this
-- 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))
⊢ 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 : 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
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
ι' : 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
⊢ 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 : ι' → ℝ), 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
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
ι' : 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
⊢ 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) ∧ ∑ i : ι, HSMul.hSMul (α := ℝ) ((K : (a : ι' → ℝ) → ι → ℝ) x_1 i : ℝ) (v i) = x
Tactic: simp_rw [Function.comp_apply, mem_image, mem_Icc, K, Equiv.piCongrLeft'_apply, this]