awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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
⊢ LE.le (α := ℝ) 0 ((fun (i : ι) ↦ x i / a i) i) ∧ LE.le (α := ℝ) ((fun (i : ι) ↦ x i / a i) i) 1
have h₂ : ∀ (hai : 0 ≤ a i), LE.le (α := ℝ) 0 ((fun (i : ι) ↦ x i / a i) i) ∧ LE.le (α := ℝ) ((fun (i : ι) ↦ x i / a i) i) 1
Tactic: rcases le_total (a i) 0 with hai | hai
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (hypothesis)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
a x : (j : ι) → ℝ
i : ι
h : min 0 (a i) ≤ x i ∧ x i ≤ max 0 (a i)
hai : a i ≤ 0
⊢ LE.le (α := ℝ) 0 ((fun (i : ι) ↦ x i / a i) i) ∧ LE.le (α := ℝ) ((fun (i : ι) ↦ x i / a i) i) 1
have h₁ : a i ≤ x i ∧ x i ≤ 0
Tactic: rw [sup_eq_left.mpr hai, inf_eq_right.mpr hai] at h
Cleared hypotheses: h, hai
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (hypothesis)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
a x : (j : ι) → ℝ
i : ι
h : min 0 (a i) ≤ x i ∧ x i ≤ max 0 (a i)
hai : 0 ≤ a i
⊢ LE.le (α := ℝ) 0 ((fun (i : ι) ↦ x i / a i) i) ∧ LE.le (α := ℝ) ((fun (i : ι) ↦ x i / a i) i) 1
have h₁ : 0 ≤ x i ∧ x i ≤ a i
Tactic: rw [sup_eq_right.mpr hai, inf_eq_left.mpr hai] at h
Cleared hypotheses: h, hai
-- 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 : ι
⊢ x i = HSMul.hSMul (α := (i : ι) → ℝ) (fun (i : ι) ↦ x i / a i) a i
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)
⊢ x i = x i / a i * a i
have h₁ : ∀ (hai : a i = 0), x i = x i / a i * a i
Tactic: rcases eq_or_ne (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 x : (j : ι) → ℝ
i : ι
h : min 0 (a i) ≤ x i ∧ x i ≤ max 0 (a i)
h₁ : ∀ (hai : a i = 0), x i = x i / a i * a i
⊢ x i = x i / a i * a i
have h₂ : ∀ (hai : a i ≠ 0), x i = x i / a i * a i
Tactic: rcases eq_or_ne (a i) 0 with hai | hai
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (hypothesis)
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
a x : (j : ι) → ℝ
i : ι
h : min 0 (a i) ≤ x i ∧ x i ≤ max 0 (a i)
hai : a i = 0
⊢ x i = x i / a i * a i
have h₁ : 0 = x i
Tactic: rw [hai, inf_idem, sup_idem, ← le_antisymm_iff] at h
Cleared hypotheses: h, hai
-- 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 : 0 = x i
hai : a i = 0
⊢ x i = x i / a i * a i
have h₁ : x i = x i / 0 * 0
Tactic: rw [hai, ← h, zero_div, zero_mul]
-- 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 : 0 = x i
hai : a i = 0
h₁ : x i = x i / 0 * 0
⊢ x i = x i / a i * a i
have h₂ : 0 = 0 / 0 * 0
Tactic: rw [hai, ← h, zero_div, zero_mul]
-- 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 : 0 = x i
hai : a i = 0
h₁ : x i = x i / 0 * 0
h₂ : 0 = 0 / 0 * 0
⊢ x i = x i / a i * a i
have h₃ : 0 = HMul.hMul (α := ℝ) 0 0
Tactic: rw [hai, ← h, zero_div, zero_mul]
-- 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 : 0 = x i
hai : a i = 0
h₁ : x i = x i / 0 * 0
h₂ : 0 = 0 / 0 * 0
h₃ : 0 = HMul.hMul (α := ℝ) 0 0
⊢ x i = x i / a i * a i
have h₄ : Eq (α := ℝ) 0 0
Tactic: rw [hai, ← h, zero_div, zero_mul]
-- 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)
hai : a i ≠ 0
⊢ x i = x i / a i * a i
have h₁ : x i = x i
Tactic: rw [div_mul_cancel₀ _ hai]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst : Fintype ι
inst_1 : Fintype ι'
inst_2 : NormedAddCommGroup E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace ℝ E
inst_5 : NormedSpace ℝ F
b : Basis ι ℝ E
H :
  Set.Nonempty.{u_3} (α := E)
    (interior
      (image.{u_1, u_3} (α := ι → ℝ)
        (⇑(ContinuousLinearEquiv.toHomeomorph (ContinuousLinearEquiv.symm b.equivFunL)) : (a : ι → ℝ) → E) (Icc 0 1)))
⊢ Set.Nonempty.{u_3} (α := E)
    (interior ((fun (t : ι → ℝ) ↦ ∑ i : ι, HSMul.hSMul (β := E) (t i) ((b : (a : ι) → E) i : E)) '' Icc 0 1))
have h : ∀ (a : ι → ℝ),
  Membership.mem (γ := Set (ι → ℝ)) (Icc 0 1) a →
    Eq.{u_3 + 1} (α := E) (∑ i : ι, HSMul.hSMul (β := E) (a i) ((b : (a : ι) → E) i : E) : E)
      ((ContinuousLinearEquiv.toHomeomorph (ContinuousLinearEquiv.symm b.equivFunL) : (a : ι → ℝ) → E) a : E)
Tactic: convert! H
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (goal)
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_3} (α := E) (interior (_root_.parallelepiped.{u_1, u_3} (ι := ι) (⇑b : (a : ι) → E)))
have suffices : Set.Nonempty.{u_3} (α := E)
  (interior
    (image.{u_1, u_3} (α := ι → ℝ)
      (⇑(ContinuousLinearEquiv.toHomeomorph (ContinuousLinearEquiv.symm b.equivFunL)) : (a : ι → ℝ) → E) (Icc 0 1)))
Tactic: suffices H : Set.Nonempty (interior (b.equivFunL.symm.toHomeomorph '' Icc 0 1)) by
      dsimp only [_root_.parallelepiped]
      convert! H
      exact (b.equivFun_symm_apply _).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (goal)
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))
have rw : Set.Nonempty.{u_1} (α := ι → ℝ) (pi (α := fun (i : ι) ↦ ℝ) univ fun (i : ι) ↦ interior (Icc (0 i) (1 i)))
Tactic: rw [← pi_univ_Icc, interior_pi_set (@finite_univ ι _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (hypothesis)
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_3} (α := E)
    (interior
      (image.{u_1, u_3} (α := ι → ℝ)
        (⇑(ContinuousLinearEquiv.toHomeomorph (ContinuousLinearEquiv.symm b.equivFunL)) : (a : ι → ℝ) → E) (Icc 0 1)))
have A : 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (goal)
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))
⊢ Set.Nonempty.{u_3} (α := E)
    (interior
      (image.{u_1, u_3} (α := ι → ℝ)
        (⇑(ContinuousLinearEquiv.toHomeomorph (ContinuousLinearEquiv.symm b.equivFunL)) : (a : ι → ℝ) → E) (Icc 0 1)))
have rwa : Set.Nonempty.{u_3} (α := E)
  (image.{u_1, u_3} (α := ι → ℝ)
    (⇑(ContinuousLinearEquiv.toHomeomorph (ContinuousLinearEquiv.symm b.equivFunL)) : (a : ι → ℝ) → E)
    (interior (Icc 0 1)))
Tactic: rwa [← Homeomorph.image_interior, image_nonempty]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (goal)
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
⊢ (v.prod w).parallelepiped (ι := ι ⊕ ι') = v.parallelepiped ×ˢ w.parallelepiped
have h : ∀ (x : E × F),
  x ∈ (↑((v.prod w).parallelepiped (ι := ι ⊕ ι')) : Set (E × F)) ↔
    x ∈ (↑(v.parallelepiped ×ˢ w.parallelepiped) : Set (E × F))
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
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
⊢ x ∈ (↑((v.prod w).parallelepiped (ι := ι ⊕ ι')) : Set (E × F)) ↔
    x ∈ (↑(v.parallelepiped ×ˢ w.parallelepiped) : Set (E × F))
have 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)
Tactic: simp only [Basis.coe_parallelepiped, TopologicalSpace.PositiveCompacts.coe_prod, Set.mem_prod,
    mem_parallelepiped_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (goal)
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 : ι ⊕ ι' → ℝ),
      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)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (goal)
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)
⊢ (∃ (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)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (goal)
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)
have 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)
Tactic: rcases h with ⟨t, ht1, ht2⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (goal)
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)
⊢ (∃ (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)
have h : ∃ (t : ι → ℝ),
  Membership.mem (γ := Set (ι → ℝ)) (Icc 0 1) t ∧ x.1 = ∑ i : ι, HSMul.hSMul (β := E) (t i) ((v : (a : ι) → E) i : E)
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (goal)
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)
⊢ (∃ (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)
have h₁ : ∃ (t : ι' → ℝ),
  Membership.mem (γ := Set (ι' → ℝ)) (Icc 0 1) t ∧ x.2 = ∑ i : ι', HSMul.hSMul (β := F) (t i) ((w : (a : ι') → F) i : F)
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (goal)
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)
⊢ ∃ (t : ι → ℝ),
    Membership.mem (γ := Set (ι → ℝ)) (Icc 0 1) t ∧ x.1 = ∑ i : ι, HSMul.hSMul (β := E) (t i) ((v : (a : ι) → E) i : E)
have 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)
Tactic: use t ∘ Sum.inl
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (goal)
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) ∧
    x.1 = ∑ i : ι, HSMul.hSMul (β := E) ((t ∘ Sum.inl) i) ((v : (a : ι) → E) i : E)
have h : Membership.mem (γ := Set (ι → ℝ)) (Icc 0 1) (t ∘ Sum.inl)
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (goal)
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)
⊢ Membership.mem (γ := Set (ι → ℝ)) (Icc 0 1) (t ∘ Sum.inl) ∧
    x.1 = ∑ i : ι, HSMul.hSMul (β := E) ((t ∘ Sum.inl) i) ((v : (a : ι) → E) i : E)
have h₁ : x.1 = ∑ i : ι, HSMul.hSMul (β := E) ((t ∘ Sum.inl) i) ((v : (a : ι) → E) i : E)
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (goal)
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)
⊢ ∃ (t : ι' → ℝ),
    Membership.mem (γ := Set (ι' → ℝ)) (Icc 0 1) t ∧
      x.2 = ∑ i : ι', HSMul.hSMul (β := F) (t i) ((w : (a : ι') → F) i : F)
have 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)
Tactic: use t ∘ Sum.inr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (goal)
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) ∧
    x.2 = ∑ i : ι', HSMul.hSMul (β := F) ((t ∘ Sum.inr) i) ((w : (a : ι') → F) i : F)
have h : Membership.mem (γ := Set (ι' → ℝ)) (Icc 0 1) (t ∘ Sum.inr)
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (goal)
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)
⊢ Membership.mem (γ := Set (ι' → ℝ)) (Icc 0 1) (t ∘ Sum.inr) ∧
    x.2 = ∑ i : ι', HSMul.hSMul (β := F) ((t ∘ Sum.inr) i) ((w : (a : ι') → F) i : F)
have h₁ : x.2 = ∑ i : ι', HSMul.hSMul (β := F) ((t ∘ Sum.inr) i) ((w : (a : ι') → F) i : F)
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (goal)
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)
⊢ ∃ (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)
have 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)
Tactic: rcases h with ⟨⟨t, ht1, ht2⟩, ⟨s, hs1, hs2⟩⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (goal)
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)
⊢ ∃ (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)
have 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)
Tactic: use Sum.elim t s