awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
rw : Set.Nonempty.{u_1} (α := ι → ℝ) (pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ interior (Icc (0 i) (1 i)))
⊢ Set.Nonempty.{u_1} (α := ι → ℝ) (interior (Icc 0 1))

Tactic:
rw [← pi_univ_Icc, interior_pi_set (@finite_univ ι _)]

Premises used: Set.finite_univ, interior_pi_set, Set.pi_univ_Icc
-- 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
⊢ Set.Nonempty.{u_1} (α := ι → ℝ) (pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ interior (Icc (0 i) (1 i)))

Tactic:
simp only [univ_pi_nonempty_iff, Pi.zero_apply, Pi.one_apply, interior_Icc, nonempty_Ioo,
        zero_lt_one, imp_true_iff]

Premises used: Pi.one_apply, interior_Icc, Pi.zero_apply, Set.univ_pi_nonempty_iff, Set.nonempty_Ioo, imp_true_iff, zero_lt_one
-- 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
⊢ Set.Nonempty.{u_1} (α := ι → ℝ) (interior (Icc 0 1))

Tactic:
have A : Set.Nonempty (interior (Icc (0 : ι → ℝ) 1)) := by
      rw [← pi_univ_Icc, interior_pi_set (@finite_univ ι _)]
      simp only [univ_pi_nonempty_iff, Pi.zero_apply, Pi.one_apply, interior_Icc, nonempty_Ioo,
        zero_lt_one, imp_true_iff]
-- 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
A : Set.Nonempty.{u_1} (α := ι → ℝ) (interior (Icc 0 1))
rwa :
  Set.Nonempty.{u_3} (α := E)
    (image.{u_1, u_3} (α := ι → ℝ)
      (⇑(ContinuousLinearEquiv.toHomeomorph (ContinuousLinearEquiv.symm b.equivFunL)) : (a : ι → ℝ) → E)
      (interior (Icc 0 1)))
rwa₁ rwa₂ rwa₃ rwa₄ : Set.Nonempty.{u_1} (α := ι → ℝ) (interior (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:
rwa [← Homeomorph.image_interior, image_nonempty]

Premises used: Set.image_nonempty, Homeomorph.image_interior
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
E : Type u_3
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
b : Basis ι ℝ E
⊢ (↑b.parallelepiped : Set E) = _root_.parallelepiped.{u_1, u_3} (ι := ι) (⇑b : (a : ι) → E)

Tactic:
rfl

Premises used: setOf, Set.image, parallelepiped, rfl
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
ι' : Type u_2
E : Type u_3
inst : Fintype ι
inst_1 : Fintype ι'
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
b : Basis ι ℝ E
e : ι ≃ ι'
⊢ (b.reindex e).parallelepiped = b.parallelepiped

Tactic:
PositiveCompacts.ext <|
    (congr_arg _root_.parallelepiped (b.coe_reindex e)).trans (parallelepiped_comp_equiv b e.symm)

Premises used: Module.Basis.coe_reindex, congr_arg, parallelepiped_comp_equiv, parallelepiped, Equiv.symm, DFunLike.coe, TopologicalSpace.PositiveCompacts.ext, Eq.trans
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
E : Type u_3
F : Type u_4
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ E
inst_4 : NormedSpace ℝ F
b : Basis ι ℝ E
e : E ≃ₗ[ℝ] F
⊢ (b.map e).parallelepiped = PositiveCompacts.map (⇑e : (a : E) → F) ⋯ ⋯ b.parallelepiped

Tactic:
PositiveCompacts.ext (image_parallelepiped e.toLinearMap _).symm

Premises used: LinearEquiv.toLinearMap, image_parallelepiped, Eq.symm, TopologicalSpace.PositiveCompacts.ext
-- 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
v : Basis ι ℝ E
w : Basis ι' ℝ F
h :
  ∀ (x : E × F),
    x ∈ (↑((v.prod w).parallelepiped (ι := ι ⊕ ι')) : Set (E × F)) ↔
      x ∈ (↑(v.parallelepiped ×ˢ w.parallelepiped) : Set (E × F))
⊢ (v.prod w).parallelepiped (ι := ι ⊕ ι') = v.parallelepiped ×ˢ w.parallelepiped

Tactic:
ext x
-- 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
v : Basis ι ℝ E
w : Basis ι' ℝ F
x : E × F
h :
  (∃ (t : ι ⊕ ι' → ℝ),
      Membership.mem (γ := Set (ι ⊕ ι' → ℝ)) (Icc 0 1) t ∧
        x = ∑ i : ι ⊕ ι', HSMul.hSMul (β := E × F) (t i) ((v.prod w : (a : ι ⊕ ι') → E × F) i : E × F)) ↔
    (∃ (t : ι → ℝ),
        Membership.mem (γ := Set (ι → ℝ)) (Icc 0 1) t ∧
          x.1 = ∑ i : ι, HSMul.hSMul (β := E) (t i) ((v : (a : ι) → E) i : E)) ∧
      ∃ (t : ι' → ℝ),
        Membership.mem (γ := Set (ι' → ℝ)) (Icc 0 1) t ∧
          x.2 = ∑ i : ι', HSMul.hSMul (β := F) (t i) ((w : (a : ι') → F) i : F)
⊢ x ∈ (↑((v.prod w).parallelepiped (ι := ι ⊕ ι')) : Set (E × F)) ↔
    x ∈ (↑(v.parallelepiped ×ˢ w.parallelepiped) : Set (E × F))

Tactic:
simp only [Basis.coe_parallelepiped, TopologicalSpace.PositiveCompacts.coe_prod, Set.mem_prod,
    mem_parallelepiped_iff]

Premises used: mem_parallelepiped_iff, Module.Basis.coe_parallelepiped, Set.mem_prod, TopologicalSpace.PositiveCompacts.coe_prod
-- 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
v : Basis ι ℝ E
w : Basis ι' ℝ F
x : E × F
h :
  (∃ (t : ι ⊕ ι' → ℝ),
      Membership.mem (γ := Set (ι ⊕ ι' → ℝ)) (Icc 0 1) t ∧
        x = ∑ i : ι ⊕ ι', HSMul.hSMul (β := E × F) (t i) ((v.prod w : (a : ι ⊕ ι') → E × F) i : E × F)) →
    (∃ (t : ι → ℝ),
        Membership.mem (γ := Set (ι → ℝ)) (Icc 0 1) t ∧
          x.1 = ∑ i : ι, HSMul.hSMul (β := E) (t i) ((v : (a : ι) → E) i : E)) ∧
      ∃ (t : ι' → ℝ),
        Membership.mem (γ := Set (ι' → ℝ)) (Icc 0 1) t ∧
          x.2 = ∑ i : ι', HSMul.hSMul (β := F) (t i) ((w : (a : ι') → F) i : F)
h₁ :
  ((∃ (t : ι → ℝ),
        Membership.mem (γ := Set (ι → ℝ)) (Icc 0 1) t ∧
          x.1 = ∑ i : ι, HSMul.hSMul (β := E) (t i) ((v : (a : ι) → E) i : E)) ∧
      ∃ (t : ι' → ℝ),
        Membership.mem (γ := Set (ι' → ℝ)) (Icc 0 1) t ∧
          x.2 = ∑ i : ι', HSMul.hSMul (β := F) (t i) ((w : (a : ι') → F) i : F)) →
    ∃ (t : ι ⊕ ι' → ℝ),
      Membership.mem (γ := Set (ι ⊕ ι' → ℝ)) (Icc 0 1) t ∧
        x = ∑ i : ι ⊕ ι', HSMul.hSMul (β := E × F) (t i) ((v.prod w : (a : ι ⊕ ι') → E × F) i : E × F)
⊢ (∃ (t : ι ⊕ ι' → ℝ),
      Membership.mem (γ := Set (ι ⊕ ι' → ℝ)) (Icc 0 1) t ∧
        x = ∑ i : ι ⊕ ι', HSMul.hSMul (β := E × F) (t i) ((v.prod w : (a : ι ⊕ ι') → E × F) i : E × F)) ↔
    (∃ (t : ι → ℝ),
        Membership.mem (γ := Set (ι → ℝ)) (Icc 0 1) t ∧
          x.1 = ∑ i : ι, HSMul.hSMul (β := E) (t i) ((v : (a : ι) → E) i : E)) ∧
      ∃ (t : ι' → ℝ),
        Membership.mem (γ := Set (ι' → ℝ)) (Icc 0 1) t ∧
          x.2 = ∑ i : ι', HSMul.hSMul (β := F) (t i) ((w : (a : ι') → F) i : F)

Tactic:
constructor
-- 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
v : Basis ι ℝ E
w : Basis ι' ℝ F
x : E × F
h :
  ∃ (t : ι ⊕ ι' → ℝ),
    Membership.mem (γ := Set (ι ⊕ ι' → ℝ)) (Icc 0 1) t ∧
      x = ∑ i : ι ⊕ ι', HSMul.hSMul (β := E × F) (t i) ((v.prod w : (a : ι ⊕ ι') → E × F) i : E × F)
h₁ :
  ∀ (t : ι ⊕ ι' → ℝ) (ht1 : Membership.mem (γ := Set (ι ⊕ ι' → ℝ)) (Icc 0 1) t)
    (ht2 : x = ∑ i : ι ⊕ ι', HSMul.hSMul (β := E × F) (t i) ((v.prod w : (a : ι ⊕ ι') → E × F) i : E × F)),
    (∃ (t : ι → ℝ),
        Membership.mem (γ := Set (ι → ℝ)) (Icc 0 1) t ∧
          x.1 = ∑ i : ι, HSMul.hSMul (β := E) (t i) ((v : (a : ι) → E) i : E)) ∧
      ∃ (t : ι' → ℝ),
        Membership.mem (γ := Set (ι' → ℝ)) (Icc 0 1) t ∧
          x.2 = ∑ i : ι', HSMul.hSMul (β := F) (t i) ((w : (a : ι') → F) i : F)
⊢ (∃ (t : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) (Icc 0 1) t ∧
        x.1 = ∑ i : ι, HSMul.hSMul (β := E) (t i) ((v : (a : ι) → E) i : E)) ∧
    ∃ (t : ι' → ℝ),
      Membership.mem (γ := Set (ι' → ℝ)) (Icc 0 1) t ∧
        x.2 = ∑ i : ι', HSMul.hSMul (β := F) (t i) ((w : (a : ι') → F) i : F)

Tactic:
rcases h with ⟨t, ht1, ht2⟩
-- 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
v : Basis ι ℝ E
w : Basis ι' ℝ F
x : E × F
t : ι ⊕ ι' → ℝ
ht1 : Membership.mem (γ := Set (ι ⊕ ι' → ℝ)) (Icc 0 1) t
ht2 : x = ∑ i : ι ⊕ ι', HSMul.hSMul (β := E × F) (t i) ((v.prod w : (a : ι ⊕ ι') → E × F) i : E × F)
h :
  ∃ (t : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) (Icc 0 1) t ∧ x.1 = ∑ i : ι, HSMul.hSMul (β := E) (t i) ((v : (a : ι) → E) i : E)
h₁ :
  ∃ (t : ι' → ℝ),
    Membership.mem (γ := Set (ι' → ℝ)) (Icc 0 1) t ∧
      x.2 = ∑ i : ι', HSMul.hSMul (β := F) (t i) ((w : (a : ι') → F) i : F)
⊢ (∃ (t : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) (Icc 0 1) t ∧
        x.1 = ∑ i : ι, HSMul.hSMul (β := E) (t i) ((v : (a : ι) → E) i : E)) ∧
    ∃ (t : ι' → ℝ),
      Membership.mem (γ := Set (ι' → ℝ)) (Icc 0 1) t ∧
        x.2 = ∑ i : ι', HSMul.hSMul (β := F) (t i) ((w : (a : ι') → F) i : F)

Tactic:
constructor
-- 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
v : Basis ι ℝ E
w : Basis ι' ℝ F
x : E × F
t : ι ⊕ ι' → ℝ
ht1 : Membership.mem (γ := Set (ι ⊕ ι' → ℝ)) (Icc 0 1) t
ht2 : x = ∑ i : ι ⊕ ι', HSMul.hSMul (β := E × F) (t i) ((v.prod w : (a : ι ⊕ ι') → E × F) i : E × F)
h :
  Membership.mem (γ := Set (ι → ℝ)) (Icc 0 1) (t ∘ Sum.inl) ∧
    x.1 = ∑ i : ι, HSMul.hSMul (β := E) ((t ∘ Sum.inl) i) ((v : (a : ι) → E) i : E)
⊢ ∃ (t : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) (Icc 0 1) t ∧ x.1 = ∑ i : ι, HSMul.hSMul (β := E) (t i) ((v : (a : ι) → E) i : E)

Tactic:
use t ∘ Sum.inl

Premises used: Sum.inl
-- 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
v : Basis ι ℝ E
w : Basis ι' ℝ F
x : E × F
t : ι ⊕ ι' → ℝ
ht1 : Membership.mem (γ := Set (ι ⊕ ι' → ℝ)) (Icc 0 1) t
ht2 : x = ∑ i : ι ⊕ ι', HSMul.hSMul (β := E × F) (t i) ((v.prod w : (a : ι ⊕ ι') → E × F) i : E × F)
h : Membership.mem (γ := Set (ι → ℝ)) (Icc 0 1) (t ∘ Sum.inl)
h₁ : x.1 = ∑ i : ι, HSMul.hSMul (β := E) ((t ∘ Sum.inl) i) ((v : (a : ι) → E) i : E)
⊢ Membership.mem (γ := Set (ι → ℝ)) (Icc 0 1) (t ∘ Sum.inl) ∧
    x.1 = ∑ i : ι, HSMul.hSMul (β := E) ((t ∘ Sum.inl) i) ((v : (a : ι) → E) i : E)

Tactic:
constructor
-- 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
v : Basis ι ℝ E
w : Basis ι' ℝ F
x : E × F
t : ι ⊕ ι' → ℝ
ht1 : Membership.mem (γ := Set (ι ⊕ ι' → ℝ)) (Icc 0 1) t
ht2 : x = ∑ i : ι ⊕ ι', HSMul.hSMul (β := E × F) (t i) ((v.prod w : (a : ι ⊕ ι') → E × F) i : E × F)
⊢ Membership.mem (γ := Set (ι → ℝ)) (Icc 0 1) (t ∘ Sum.inl)

Tactic:
⟨(ht1.1 <| Sum.inl ·), (ht1.2 <| Sum.inl ·)⟩

Premises used: Set.Mem, setOf, Sum.inl, Set.Icc, And.right, And.left, And.intro
-- 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
v : Basis ι ℝ E
w : Basis ι' ℝ F
x : E × F
t : ι ⊕ ι' → ℝ
ht1 : Membership.mem (γ := Set (ι ⊕ ι' → ℝ)) (Icc 0 1) t
ht2 : x = ∑ i : ι ⊕ ι', HSMul.hSMul (β := E × F) (t i) ((v.prod w : (a : ι ⊕ ι') → E × F) i : E × F)
⊢ Membership.mem (γ := Set (ι → ℝ)) (Icc 0 1) (t ∘ Sum.inl)

Tactic:
exact ⟨(ht1.1 <| Sum.inl ·), (ht1.2 <| Sum.inl ·)⟩
-- 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
v : Basis ι ℝ E
w : Basis ι' ℝ F
x : E × F
t : ι ⊕ ι' → ℝ
ht1 : Membership.mem (γ := Set (ι ⊕ ι' → ℝ)) (Icc 0 1) t
ht2 : x = ∑ i : ι ⊕ ι', HSMul.hSMul (β := E × F) (t i) ((v.prod w : (a : ι ⊕ ι') → E × F) i : E × F)
⊢ x.1 = ∑ i : ι, HSMul.hSMul (β := E) ((t ∘ Sum.inl) i) ((v : (a : ι) → E) i : E)

Tactic:
simp [ht2, Prod.fst_sum]

Premises used: Prod.fst_sum
-- 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
v : Basis ι ℝ E
w : Basis ι' ℝ F
x : E × F
t : ι ⊕ ι' → ℝ
ht1 : Membership.mem (γ := Set (ι ⊕ ι' → ℝ)) (Icc 0 1) t
ht2 : x = ∑ i : ι ⊕ ι', HSMul.hSMul (β := E × F) (t i) ((v.prod w : (a : ι ⊕ ι') → E × F) i : E × F)
h :
  Membership.mem (γ := Set (ι' → ℝ)) (Icc 0 1) (t ∘ Sum.inr) ∧
    x.2 = ∑ i : ι', HSMul.hSMul (β := F) ((t ∘ Sum.inr) i) ((w : (a : ι') → F) i : F)
⊢ ∃ (t : ι' → ℝ),
    Membership.mem (γ := Set (ι' → ℝ)) (Icc 0 1) t ∧
      x.2 = ∑ i : ι', HSMul.hSMul (β := F) (t i) ((w : (a : ι') → F) i : F)

Tactic:
use t ∘ Sum.inr

Premises used: Sum.inr
-- 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
v : Basis ι ℝ E
w : Basis ι' ℝ F
x : E × F
t : ι ⊕ ι' → ℝ
ht1 : Membership.mem (γ := Set (ι ⊕ ι' → ℝ)) (Icc 0 1) t
ht2 : x = ∑ i : ι ⊕ ι', HSMul.hSMul (β := E × F) (t i) ((v.prod w : (a : ι ⊕ ι') → E × F) i : E × F)
h : Membership.mem (γ := Set (ι' → ℝ)) (Icc 0 1) (t ∘ Sum.inr)
h₁ : x.2 = ∑ i : ι', HSMul.hSMul (β := F) ((t ∘ Sum.inr) i) ((w : (a : ι') → F) i : F)
⊢ Membership.mem (γ := Set (ι' → ℝ)) (Icc 0 1) (t ∘ Sum.inr) ∧
    x.2 = ∑ i : ι', HSMul.hSMul (β := F) ((t ∘ Sum.inr) i) ((w : (a : ι') → F) i : F)

Tactic:
constructor
-- 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
v : Basis ι ℝ E
w : Basis ι' ℝ F
x : E × F
t : ι ⊕ ι' → ℝ
ht1 : Membership.mem (γ := Set (ι ⊕ ι' → ℝ)) (Icc 0 1) t
ht2 : x = ∑ i : ι ⊕ ι', HSMul.hSMul (β := E × F) (t i) ((v.prod w : (a : ι ⊕ ι') → E × F) i : E × F)
⊢ Membership.mem (γ := Set (ι' → ℝ)) (Icc 0 1) (t ∘ Sum.inr)

Tactic:
⟨(ht1.1 <| Sum.inr ·), (ht1.2 <| Sum.inr ·)⟩

Premises used: Set.Mem, setOf, Set.Icc, And.right, And.left, Sum.inr, And.intro
-- 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
v : Basis ι ℝ E
w : Basis ι' ℝ F
x : E × F
t : ι ⊕ ι' → ℝ
ht1 : Membership.mem (γ := Set (ι ⊕ ι' → ℝ)) (Icc 0 1) t
ht2 : x = ∑ i : ι ⊕ ι', HSMul.hSMul (β := E × F) (t i) ((v.prod w : (a : ι ⊕ ι') → E × F) i : E × F)
⊢ Membership.mem (γ := Set (ι' → ℝ)) (Icc 0 1) (t ∘ Sum.inr)

Tactic:
exact ⟨(ht1.1 <| Sum.inr ·), (ht1.2 <| Sum.inr ·)⟩
-- 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
v : Basis ι ℝ E
w : Basis ι' ℝ F
x : E × F
t : ι ⊕ ι' → ℝ
ht1 : Membership.mem (γ := Set (ι ⊕ ι' → ℝ)) (Icc 0 1) t
ht2 : x = ∑ i : ι ⊕ ι', HSMul.hSMul (β := E × F) (t i) ((v.prod w : (a : ι ⊕ ι') → E × F) i : E × F)
⊢ x.2 = ∑ i : ι', HSMul.hSMul (β := F) ((t ∘ Sum.inr) i) ((w : (a : ι') → F) i : F)

Tactic:
simp [ht2, Prod.snd_sum]

Premises used: Prod.snd_sum
-- 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
v : Basis ι ℝ E
w : Basis ι' ℝ F
x : E × F
h :
  (∃ (t : ι → ℝ),
      Membership.mem (γ := Set (ι → ℝ)) (Icc 0 1) t ∧
        x.1 = ∑ i : ι, HSMul.hSMul (β := E) (t i) ((v : (a : ι) → E) i : E)) ∧
    ∃ (t : ι' → ℝ),
      Membership.mem (γ := Set (ι' → ℝ)) (Icc 0 1) t ∧
        x.2 = ∑ i : ι', HSMul.hSMul (β := F) (t i) ((w : (a : ι') → F) i : F)
h₁ :
  ∀ (t : ι → ℝ) (ht1 : Membership.mem (γ := Set (ι → ℝ)) (Icc 0 1) t)
    (ht2 : x.1 = ∑ i : ι, HSMul.hSMul (β := E) (t i) ((v : (a : ι) → E) i : E)) (s : ι' → ℝ)
    (hs1 : Membership.mem (γ := Set (ι' → ℝ)) (Icc 0 1) s)
    (hs2 : x.2 = ∑ i : ι', HSMul.hSMul (β := F) (s i) ((w : (a : ι') → F) i : F)),
    ∃ (t : ι ⊕ ι' → ℝ),
      Membership.mem (γ := Set (ι ⊕ ι' → ℝ)) (Icc 0 1) t ∧
        x = ∑ i : ι ⊕ ι', HSMul.hSMul (β := E × F) (t i) ((v.prod w : (a : ι ⊕ ι') → E × F) i : E × F)
⊢ ∃ (t : ι ⊕ ι' → ℝ),
    Membership.mem (γ := Set (ι ⊕ ι' → ℝ)) (Icc 0 1) t ∧
      x = ∑ i : ι ⊕ ι', HSMul.hSMul (β := E × F) (t i) ((v.prod w : (a : ι ⊕ ι') → E × F) i : E × F)

Tactic:
rcases h with ⟨⟨t, ht1, ht2⟩, ⟨s, hs1, hs2⟩⟩
-- 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
v : Basis ι ℝ E
w : Basis ι' ℝ F
x : E × F
t : ι → ℝ
ht1 : Membership.mem (γ := Set (ι → ℝ)) (Icc 0 1) t
ht2 : x.1 = ∑ i : ι, HSMul.hSMul (β := E) (t i) ((v : (a : ι) → E) i : E)
s : ι' → ℝ
hs1 : Membership.mem (γ := Set (ι' → ℝ)) (Icc 0 1) s
hs2 : x.2 = ∑ i : ι', HSMul.hSMul (β := F) (s i) ((w : (a : ι') → F) i : F)
h :
  Membership.mem (γ := Set (ι ⊕ ι' → ℝ)) (Icc 0 1) (Sum.elim t s) ∧
    x = ∑ i : ι ⊕ ι', HSMul.hSMul (β := E × F) (Sum.elim t s i) ((v.prod w : (a : ι ⊕ ι') → E × F) i : E × F)
⊢ ∃ (t : ι ⊕ ι' → ℝ),
    Membership.mem (γ := Set (ι ⊕ ι' → ℝ)) (Icc 0 1) t ∧
      x = ∑ i : ι ⊕ ι', HSMul.hSMul (β := E × F) (t i) ((v.prod w : (a : ι ⊕ ι') → E × F) i : E × F)

Tactic:
use Sum.elim t s

Premises used: Sum.elim
-- 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
v : Basis ι ℝ E
w : Basis ι' ℝ F
x : E × F
t : ι → ℝ
ht1 : Membership.mem (γ := Set (ι → ℝ)) (Icc 0 1) t
ht2 : x.1 = ∑ i : ι, HSMul.hSMul (β := E) (t i) ((v : (a : ι) → E) i : E)
s : ι' → ℝ
hs1 : Membership.mem (γ := Set (ι' → ℝ)) (Icc 0 1) s
hs2 : x.2 = ∑ i : ι', HSMul.hSMul (β := F) (s i) ((w : (a : ι') → F) i : F)
h : Membership.mem (γ := Set (ι ⊕ ι' → ℝ)) (Icc 0 1) (Sum.elim t s)
h₁ : x = ∑ i : ι ⊕ ι', HSMul.hSMul (β := E × F) (Sum.elim t s i) ((v.prod w : (a : ι ⊕ ι') → E × F) i : E × F)
⊢ Membership.mem (γ := Set (ι ⊕ ι' → ℝ)) (Icc 0 1) (Sum.elim t s) ∧
    x = ∑ i : ι ⊕ ι', HSMul.hSMul (β := E × F) (Sum.elim t s i) ((v.prod w : (a : ι ⊕ ι') → E × F) i : E × F)

Tactic:
constructor
-- 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
v : Basis ι ℝ E
w : Basis ι' ℝ F
x : E × F
t : ι → ℝ
ht1 : Membership.mem (γ := Set (ι → ℝ)) (Icc 0 1) t
ht2 : x.1 = ∑ i : ι, HSMul.hSMul (β := E) (t i) ((v : (a : ι) → E) i : E)
s : ι' → ℝ
hs1 : Membership.mem (γ := Set (ι' → ℝ)) (Icc 0 1) s
hs2 : x.2 = ∑ i : ι', HSMul.hSMul (β := F) (s i) ((w : (a : ι') → F) i : F)
h : 0 ≤ Sum.elim t s
h₁ : Sum.elim t s ≤ 1
⊢ Membership.mem (γ := Set (ι ⊕ ι' → ℝ)) (Icc 0 1) (Sum.elim t s)

Tactic:
constructor
-- 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
v : Basis ι ℝ E
w : Basis ι' ℝ F
x : E × F
t : ι → ℝ
ht1 : Membership.mem (γ := Set (ι → ℝ)) (Icc 0 1) t
ht2 : x.1 = ∑ i : ι, HSMul.hSMul (β := E) (t i) ((v : (a : ι) → E) i : E)
s : ι' → ℝ
hs1 : Membership.mem (γ := Set (ι' → ℝ)) (Icc 0 1) s
hs2 : x.2 = ∑ i : ι', HSMul.hSMul (β := F) (s i) ((w : (a : ι') → F) i : F)
⊢ ∀ (x : ι ⊕ ι'), 0 ≤ Sum.elim t s x

Tactic:
aesop
-- 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
v : Basis ι ℝ E
w : Basis ι' ℝ F
x : E × F
t : ι → ℝ
ht1 : Membership.mem (γ := Set (ι → ℝ)) (Icc 0 1) t
ht2 : x.1 = ∑ i : ι, HSMul.hSMul (β := E) (t i) ((v : (a : ι) → E) i : E)
s : ι' → ℝ
hs1 : Membership.mem (γ := Set (ι' → ℝ)) (Icc 0 1) s
hs2 : x.2 = ∑ i : ι', HSMul.hSMul (β := F) (s i) ((w : (a : ι') → F) i : F)
⊢ ∀ (x : ι ⊕ ι'), Sum.elim t s x ≤ 1

Tactic:
aesop
-- 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
v : Basis ι ℝ E
w : Basis ι' ℝ F
x : E × F
t : ι → ℝ
ht1 : Membership.mem (γ := Set (ι → ℝ)) (Icc 0 1) t
ht2 : x.1 = ∑ i : ι, HSMul.hSMul (β := E) (t i) ((v : (a : ι) → E) i : E)
s : ι' → ℝ
hs1 : Membership.mem (γ := Set (ι' → ℝ)) (Icc 0 1) s
hs2 : x.2 = ∑ i : ι', HSMul.hSMul (β := F) (s i) ((w : (a : ι') → F) i : F)
h : x.1 = (∑ i : ι ⊕ ι', HSMul.hSMul (β := E × F) (Sum.elim t s i) ((v.prod w : (a : ι ⊕ ι') → E × F) i : E × F)).1
h₁ : x.2 = (∑ i : ι ⊕ ι', HSMul.hSMul (β := E × F) (Sum.elim t s i) ((v.prod w : (a : ι ⊕ ι') → E × F) i : E × F)).2
⊢ x = ∑ i : ι ⊕ ι', HSMul.hSMul (β := E × F) (Sum.elim t s i) ((v.prod w : (a : ι ⊕ ι') → E × F) i : E × F)

Tactic:
ext
-- 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
v : Basis ι ℝ E
w : Basis ι' ℝ F
x : E × F
t : ι → ℝ
ht1 : Membership.mem (γ := Set (ι → ℝ)) (Icc 0 1) t
ht2 : x.1 = ∑ i : ι, HSMul.hSMul (β := E) (t i) ((v : (a : ι) → E) i : E)
s : ι' → ℝ
hs1 : Membership.mem (γ := Set (ι' → ℝ)) (Icc 0 1) s
hs2 : x.2 = ∑ i : ι', HSMul.hSMul (β := F) (s i) ((w : (a : ι') → F) i : F)
⊢ x.1 = (∑ i : ι ⊕ ι', HSMul.hSMul (β := E × F) (Sum.elim t s i) ((v.prod w : (a : ι ⊕ ι') → E × F) i : E × F)).1

Tactic:
simp [ht2, Prod.fst_sum]

Premises used: Prod.fst_sum