awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
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
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))
⊢ 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:
congr 1 with t
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
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
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:
simp only [Function.comp_apply, _root_.map_sum, map_smulₛₗ, RingHom.id_apply]

Premises used: RingHom.id_apply, MulActionSemiHomClass.map_smulₛₗ, map_sum, Function.comp_apply
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
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
rw : Eq.{u_2 + 1} (α := Set (ι' → ℝ)) (preimage.{u_2, u_1} (β := ι → ℝ) (⇑K : (a : ι' → ℝ) → ι → ℝ) (Icc 0 1)) (Icc 0 1)
⊢ Eq.{u_1 + 1} (α := Set (ι → ℝ)) (Icc 0 1) (image.{u_2, u_1} (α := ι' → ℝ) (⇑K : (a : ι' → ℝ) → ι → ℝ) (Icc 0 1))

Tactic:
rw [← Equiv.preimage_eq_iff_eq_image]

Premises used: Equiv.preimage_eq_iff_eq_image
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
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
h :
  ∀ (x : ι' → ℝ),
    Membership.mem (γ := Set (ι' → ℝ)) (preimage.{u_2, u_1} (β := ι → ℝ) (⇑K : (a : ι' → ℝ) → ι → ℝ) (Icc 0 1)) x ↔
      Membership.mem (γ := Set (ι' → ℝ)) (Icc 0 1) x
⊢ Eq.{u_2 + 1} (α := Set (ι' → ℝ)) (preimage.{u_2, u_1} (β := ι → ℝ) (⇑K : (a : ι' → ℝ) → ι → ℝ) (Icc 0 1)) (Icc 0 1)

Tactic:
ext x
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
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 :
  ((∀ (i : ι), 0 ≤ x ((e.symm : (a : ι) → ι') i)) ∧ ∀ (i : ι), x ((e.symm : (a : ι) → ι') i) ≤ 1) ↔
    (∀ (i : ι'), 0 ≤ x i) ∧ ∀ (i : ι'), x i ≤ 1
⊢ Membership.mem (γ := Set (ι' → ℝ)) (preimage.{u_2, u_1} (β := ι → ℝ) (⇑K : (a : ι' → ℝ) → ι → ℝ) (Icc 0 1)) x ↔
    Membership.mem (γ := Set (ι' → ℝ)) (Icc 0 1) x

Tactic:
simp only [K, mem_preimage, mem_Icc, Pi.le_def, Pi.zero_apply, Equiv.piCongrLeft'_apply,
      Pi.one_apply]

Premises used: Pi.one_apply, Pi.zero_apply, Set.mem_Icc, Pi.le_def, Set.mem_preimage, Equiv.piCongrLeft'_apply
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
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

Tactic:
⟨fun h => ⟨fun i => ?_, fun i => ?_⟩, fun h =>
        ⟨fun i => h.1 (e.symm i), fun i => h.2 (e.symm i)⟩⟩

Premises used: And.right, And.left, And.intro, Iff.intro, Equiv.symm, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
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
h₁ :
  ∀ (h : (∀ (i : ι), 0 ≤ x ((e.symm : (a : ι) → ι') i)) ∧ ∀ (i : ι), x ((e.symm : (a : ι) → ι') i) ≤ 1) (i : ι'),
    x i ≤ 1
⊢ ((∀ (i : ι), 0 ≤ x ((e.symm : (a : ι) → ι') i)) ∧ ∀ (i : ι), x ((e.symm : (a : ι) → ι') i) ≤ 1) ↔
    (∀ (i : ι'), 0 ≤ x i) ∧ ∀ (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)⟩⟩
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
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 : (∀ (i : ι), 0 ≤ x ((e.symm : (a : ι) → ι') i)) ∧ ∀ (i : ι), x ((e.symm : (a : ι) → ι') i) ≤ 1
i : ι'
⊢ 0 ≤ x i

Tactic:
simpa only [Equiv.symm_apply_apply] using h.1 (e i)

Premises used: Equiv.symm_apply_apply, And.left, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
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 : (∀ (i : ι), 0 ≤ x ((e.symm : (a : ι) → ι') i)) ∧ ∀ (i : ι), x ((e.symm : (a : ι) → ι') i) ≤ 1
i : ι'
⊢ x i ≤ 1

Tactic:
simpa only [Equiv.symm_apply_apply] using h.2 (e i)

Premises used: Equiv.symm_apply_apply, And.right, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
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))

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)
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
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))
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))
⊢ 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)

Tactic:
rw [this, ← image_comp]

Premises used: Set.image_comp
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
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))
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
⊢ 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:
ext x
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
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
⊢ ∀ (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)
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
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))
⊢ ∀ (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

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
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
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
⊢ 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:
simp_rw [Function.comp_apply, mem_image, mem_Icc, K, Equiv.piCongrLeft'_apply, this]

Premises used: Set.mem_image, Set.mem_Icc, Function.comp_apply, Equiv.piCongrLeft'_apply
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
inst : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
h : Fintype.card ι = 1
⊢ ι ≃ Fin 1

Tactic:
apply Fintype.equivFinOfCardEq

Premises used: Fintype.equivFinOfCardEq
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
inst : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
⊢ Fintype.card ι = 1

Tactic:
simp only [← finrank_eq_card_basis b.toBasis, finrank_self]

Premises used: Module.finrank_eq_card_basis, Module.finrank_self, OrthonormalBasis.toBasis
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
inst : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
have :
  ∀ (e : ι ≃ Fin 1),
    Eq (α := Set ℝ) (parallelepiped (ι := ι) (⇑b : (a : ι) → ℝ)) (Icc 0 1) ∨
      Eq (α := Set ℝ) (parallelepiped (ι := ι) (⇑b : (a : ι) → ℝ)) (Icc (-1) 0)
⊢ 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]
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
inst : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
⊢ Eq (α := Set ℝ) (parallelepiped (ι := Fin 1) (Function.comp (β := ι) (⇑b : (a : ι) → ℝ) (⇑e.symm : (a : Fin 1) → ι)))
    (parallelepiped (ι := ι) (⇑b : (a : ι) → ℝ))

Tactic:
parallelepiped_comp_equiv b e.symm

Premises used: parallelepiped_comp_equiv, Equiv.symm, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
inst : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
h :
  Eq (α := Fin 1 → ℝ) (⇑(b.reindex e) : (a : Fin 1) → ℝ)
    (Function.comp (β := ι) (⇑b : (a : ι) → ℝ) (⇑e.symm : (a : Fin 1) → ι))
⊢ Eq (α := Set ℝ) (parallelepiped (ι := Fin 1) (⇑(b.reindex e) : (a : Fin 1) → ℝ))
    (parallelepiped (ι := ι) (⇑b : (a : ι) → ℝ))

Tactic:
convert! parallelepiped_comp_equiv b e.symm

Premises used: parallelepiped_comp_equiv, Equiv.symm, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
inst : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
h :
  ∀ (i : Fin 1),
    Eq (α := ℝ) ((b.reindex e : (a : Fin 1) → ℝ) i : ℝ)
      (Function.comp (β := ι) (⇑b : (a : ι) → ℝ) (⇑e.symm : (a : Fin 1) → ι) i : ℝ)
⊢ Eq (α := Fin 1 → ℝ) (⇑(b.reindex e) : (a : Fin 1) → ℝ)
    (Function.comp (β := ι) (⇑b : (a : ι) → ℝ) (⇑e.symm : (a : Fin 1) → ι))

Tactic:
ext i
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
inst : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
e : ι ≃ Fin 1
i : Fin 1
⊢ Eq (α := ℝ) ((b.reindex e : (a : Fin 1) → ℝ) i : ℝ)
    (Function.comp (β := ι) (⇑b : (a : ι) → ℝ) (⇑e.symm : (a : Fin 1) → ι) i : ℝ)

Tactic:
simp only [OrthonormalBasis.coe_reindex]

Premises used: OrthonormalBasis.coe_reindex
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
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 : ι) → ℝ))

Tactic:
have B : parallelepiped (b.reindex e) = parallelepiped b := by
    convert! parallelepiped_comp_equiv b e.symm
    ext i
    simp only [OrthonormalBasis.coe_reindex]
-- 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 : ι) → ℝ))
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)
⊢ Eq (α := Set ℝ) (parallelepiped (ι := ι) (⇑b : (a : ι) → ℝ)) (Icc 0 1) ∨
    Eq (α := Set ℝ) (parallelepiped (ι := ι) (⇑b : (a : ι) → ℝ)) (Icc (-1) 0)

Tactic:
rw [← B]
-- 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
h₁ : Icc 0 1 ⊆ F '' Icc 0 1
h₂ : F '' Icc 0 1 ⊆ Icc 0 1
⊢ Icc 0 1 = F '' Icc 0 1

Tactic:
apply Subset.antisymm

Premises used: Set.Subset.antisymm
-- 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
x : Fin 1 → ℝ
hx : Membership.mem (γ := Set (Fin 1 → ℝ)) (Icc 0 1) x
⊢ x ∈ F '' Icc 0 1

Tactic:
⟨x 0, ⟨hx.1 0, hx.2 0⟩, ?_⟩

Premises used: Set.Mem, setOf, And.right, And.left, And.intro, Exists.intro, Set.image, OfNat.ofNat
-- 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
x : Fin 1 → ℝ
hx : Membership.mem (γ := Set (Fin 1 → ℝ)) (Icc 0 1) x
h₁ : F (x 0) = x
⊢ x ∈ F '' Icc 0 1

Tactic:
refine ⟨x 0, ⟨hx.1 0, hx.2 0⟩, ?_⟩
-- 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
x : Fin 1 → ℝ
hx : Membership.mem (γ := Set (Fin 1 → ℝ)) (Icc 0 1) x
h₁ : ∀ (j : Fin 1), F (x 0) j = x j
⊢ F (x 0) = x

Tactic:
ext j
-- 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
x : Fin 1 → ℝ
hx : Membership.mem (γ := Set (Fin 1 → ℝ)) (Icc 0 1) x
j : Fin 1
⊢ F (x 0) j = x j

Tactic:
simp only [F, Subsingleton.elim j 0]

Premises used: Subsingleton.elim, OfNat.ofNat
-- 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
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Icc 0 1) y
⊢ Membership.mem (γ := Set (Fin 1 → ℝ)) (Icc 0 1) (F y)

Tactic:
⟨fun _j => hy.1, fun _j => hy.2⟩

Premises used: Set.Mem, setOf, Set.Icc, And.right, And.left, And.intro
-- 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
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Icc 0 1) y
⊢ Membership.mem (γ := Set (Fin 1 → ℝ)) (Icc 0 1) (F y)

Tactic:
exact ⟨fun _j => hy.1, fun _j => hy.2⟩
-- 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
⊢ 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⟩
-- 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
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)
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)
⊢ 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)

Premises used: OrthonormalBasis.reindex, orthonormalBasis_one_dim
-- 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
inl : 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 0 1) ∨
    Eq (α := Set ℝ) (parallelepiped (ι := Fin 1) (⇑(b.reindex e) : (a : Fin 1) → ℝ)) (Icc (-1) 0)

Tactic:
left
-- 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
inl : Eq (α := Set ℝ) ((fun (a : Fin 1 → ℝ) ↦ ∑ x : Fin 1, a x) '' F '' Icc 0 1) (Icc 0 1)
⊢ Eq (α := Set ℝ) (parallelepiped (ι := Fin 1) (⇑(b.reindex e) : (a : Fin 1) → ℝ)) (Icc 0 1)

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

Premises used: smul_eq_mul, parallelepiped, mul_one
-- 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) '' F '' Icc 0 1) (Icc 0 1)

Tactic:
simp only [F, Finset.univ_unique, Fin.default_eq_zero, Finset.sum_singleton,
      ← image_comp, Function.comp_apply, image_id']

Premises used: Set.image_id', Finset.univ_unique, Finset.sum_singleton, Set.image_comp, Function.comp_apply, Fin.default_eq_zero