awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (goal)
Goal:
ι : Type u_1
ι' : Type u_2
E : Type u_3
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)
⊢ 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)
have h : Membership.mem (γ := Set (ι ⊕ ι' → ℝ)) (Icc 0 1) (Sum.elim t s)
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.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)
⊢ 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)
have h₁ : x = ∑ i : ι ⊕ ι', HSMul.hSMul (β := E × F) (Sum.elim t s 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
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)
⊢ Membership.mem (γ := Set (ι ⊕ ι' → ℝ)) (Icc 0 1) (Sum.elim t s)
have h : 0 ≤ Sum.elim t s
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.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
⊢ Membership.mem (γ := Set (ι ⊕ ι' → ℝ)) (Icc 0 1) (Sum.elim t s)
have h₁ : Sum.elim t s ≤ 1
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.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 = ∑ i : ι ⊕ ι', HSMul.hSMul (β := E × F) (Sum.elim t s i) ((v.prod w : (a : ι ⊕ ι') → E × F) i : E × F)
have h : x.1 = (∑ i : ι ⊕ ι', HSMul.hSMul (β := E × F) (Sum.elim t s i) ((v.prod w : (a : ι ⊕ ι') → E × F) i : E × F)).1
Tactic: ext
-- 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)
h : x.1 = (∑ i : ι ⊕ ι', HSMul.hSMul (β := E × F) (Sum.elim t s i) ((v.prod w : (a : ι ⊕ ι') → E × F) i : E × F)).1
⊢ x = ∑ i : ι ⊕ ι', HSMul.hSMul (β := E × F) (Sum.elim t s i) ((v.prod w : (a : ι ⊕ ι') → E × F) i : E × F)
have h₁ : x.2 = (∑ i : ι ⊕ ι', HSMul.hSMul (β := E × F) (Sum.elim t s i) ((v.prod w : (a : ι ⊕ ι') → E × F) i : E × F)).2
Tactic: ext
-- 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
inst_6 : MeasurableSpace E
inst_7 : BorelSpace E
b : Basis ι ℝ E
⊢ IsAddHaarMeasure b.addHaar
have rw : IsAddHaarMeasure (addHaarMeasure b.parallelepiped)
Tactic: rw [Basis.addHaar]
-- 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
inst_6 : MeasurableSpace E
inst_7 : BorelSpace E
b : Basis ι ℝ E
⊢ SigmaFinite (m0 := inst_6) b.addHaar
have this : FiniteDimensional ℝ E
Tactic: have : FiniteDimensional ℝ E := b.finiteDimensional_of_finite
-- 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
inst_6 : MeasurableSpace E
inst_7 : BorelSpace E
b : Basis ι ℝ E
this : FiniteDimensional ℝ E
⊢ SigmaFinite (m0 := inst_6) b.addHaar
have rw : SigmaFinite (m0 := inst_6) (addHaarMeasure b.parallelepiped)
Tactic: rw [Basis.addHaar_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (goal)
Goal:
ι : Type u_1
E : Type u_3
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
inst_5 : SecondCountableTopology E
b : Basis ι ℝ E
μ : Measure E
inst_6 : SigmaFinite μ
inst_7 : μ.IsAddLeftInvariant
⊢ b.addHaar = μ ↔ Eq (α := ENNReal) ((μ : (a : Set E) → ENNReal) (↑b.parallelepiped : Set E) : ENNReal) (1 : ENNReal)
have rw : addHaarMeasure b.parallelepiped = μ ↔
  Eq (α := ENNReal) ((μ : (a : Set E) → ENNReal) (↑b.parallelepiped : Set E) : ENNReal) (1 : ENNReal)
Tactic: rw [Basis.addHaar_def]
-- 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 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
b : Basis ι ℝ E
e : ι ≃ ι'
⊢ Eq (α := Measure E) (b.reindex e).addHaar b.addHaar
have rw : Eq (α := Measure E) (addHaarMeasure (b.reindex e).parallelepiped) b.addHaar
Tactic: rw [Basis.addHaar, b.parallelepiped_reindex e, ← Basis.addHaar]
-- 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 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
b : Basis ι ℝ E
e : ι ≃ ι'
rw : Eq (α := Measure E) (addHaarMeasure (b.reindex e).parallelepiped) b.addHaar
⊢ Eq (α := Measure E) (b.reindex e).addHaar b.addHaar
have rw₁ : Eq (α := Measure E) (addHaarMeasure b.parallelepiped) b.addHaar
Tactic: rw [Basis.addHaar, b.parallelepiped_reindex e, ← Basis.addHaar]
-- 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 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
b : Basis ι ℝ E
e : ι ≃ ι'
rw : Eq (α := Measure E) (addHaarMeasure (b.reindex e).parallelepiped) b.addHaar
rw₁ : Eq (α := Measure E) (addHaarMeasure b.parallelepiped) b.addHaar
⊢ Eq (α := Measure E) (b.reindex e).addHaar b.addHaar
have rw₂ : Eq (α := Measure E) b.addHaar b.addHaar
Tactic: rw [Basis.addHaar, b.parallelepiped_reindex e, ← Basis.addHaar]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.OfBasis (goal)
Goal:
ι : Type u_1
E : Type u_3
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
b : Basis ι ℝ E
⊢ Eq (α := ENNReal)
    (((b.addHaar : Measure E) : (a : Set E) → ENNReal) (_root_.parallelepiped.{u_1, u_3} (ι := ι) (⇑b : (a : ι) → E)) :
      ENNReal)
    (1 : ENNReal)
have rw : Eq (α := ENNReal)
  (((addHaarMeasure b.parallelepiped : Measure E) : (a : Set E) → ENNReal)
      (_root_.parallelepiped.{u_1, u_3} (ι := ι) (⇑b : (a : ι) → E)) :
    ENNReal)
  (1 : ENNReal)
Tactic: rw [Basis.addHaar]
-- 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
inst_6 : MeasurableSpace E
inst_7 : BorelSpace E
inst_8 : MeasurableSpace F
inst_9 : BorelSpace F
inst_10 : SecondCountableTopologyEither E F
v : Basis ι ℝ E
w : Basis ι' ℝ F
⊢ Eq (α := Measure (E × F)) ((v.prod w).addHaar (ι := ι ⊕ ι')) (Measure.prod v.addHaar w.addHaar)
have this : FiniteDimensional ℝ E
Tactic: have : FiniteDimensional ℝ E := v.finiteDimensional_of_finite
-- 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
inst_6 : MeasurableSpace E
inst_7 : BorelSpace E
inst_8 : MeasurableSpace F
inst_9 : BorelSpace F
inst_10 : SecondCountableTopologyEither E F
v : Basis ι ℝ E
w : Basis ι' ℝ F
this : FiniteDimensional ℝ E
⊢ Eq (α := Measure (E × F)) ((v.prod w).addHaar (ι := ι ⊕ ι')) (Measure.prod v.addHaar w.addHaar)
have this₁ : FiniteDimensional ℝ F
Tactic: have : FiniteDimensional ℝ F := w.finiteDimensional_of_finite
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Quotient (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
ν : Measure G
Γ : Subgroup G
μ : Measure (G ⧸ Γ)
inst_2 : QuotientMeasureEqMeasurePreimage ν μ
inst_3 : TopologicalSpace G
inst_4 : IsTopologicalGroup G
inst_5 : BorelSpace G
inst_6 : PolishSpace G
inst_7 : T2Space.{u_1} (G ⧸ Γ)
inst_8 : SecondCountableTopology.{u_1} (G ⧸ Γ)
inst_9 : ν.IsMulLeftInvariant
hasFun : HasFundamentalDomain (↥Γ.op) G ν
g : G
A : Set (G ⧸ Γ)
hA : MeasurableSet A
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) ((fun (x : G ⧸ Γ) ↦ g • x) ⁻¹' A) : ℝ≥0∞)
    ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) A : ℝ≥0∞)
have meas_π : Measurable.{u_1, u_1} (α := G) (β := G ⧸ Γ) QuotientGroup.mk
Tactic: have meas_π : Measurable π := continuous_quotient_mk'.measurable
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Quotient (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
ν : Measure G
Γ : Subgroup G
μ : Measure (G ⧸ Γ)
inst_2 : QuotientMeasureEqMeasurePreimage ν μ
inst_3 : TopologicalSpace G
inst_4 : IsTopologicalGroup G
inst_5 : BorelSpace G
inst_6 : PolishSpace G
inst_7 : T2Space.{u_1} (G ⧸ Γ)
inst_8 : SecondCountableTopology.{u_1} (G ⧸ Γ)
inst_9 : ν.IsMulLeftInvariant
hasFun : HasFundamentalDomain (↥Γ.op) G ν
g : G
A : Set (G ⧸ Γ)
hA : MeasurableSet A
meas_π : Measurable.{u_1, u_1} (α := G) (β := G ⧸ Γ) QuotientGroup.mk
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) ((fun (x : G ⧸ Γ) ↦ g • x) ⁻¹' A) : ℝ≥0∞)
    ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) A : ℝ≥0∞)
have obtain : ∀ (𝓕 : Set G) (h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν),
  Eq (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) ((fun (x : G ⧸ Γ) ↦ g • x) ⁻¹' A) : ℝ≥0∞)
    ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) A : ℝ≥0∞)
Tactic: obtain ⟨𝓕, h𝓕⟩ := hasFun.ExistsIsFundamentalDomain
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Quotient (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
ν : Measure G
Γ : Subgroup G
μ : Measure (G ⧸ Γ)
inst_2 : QuotientMeasureEqMeasurePreimage ν μ
inst_3 : TopologicalSpace G
inst_4 : IsTopologicalGroup G
inst_5 : BorelSpace G
inst_6 : PolishSpace G
inst_7 : T2Space.{u_1} (G ⧸ Γ)
inst_8 : SecondCountableTopology.{u_1} (G ⧸ Γ)
inst_9 : ν.IsMulLeftInvariant
hasFun : HasFundamentalDomain (↥Γ.op) G ν
g : G
A : Set (G ⧸ Γ)
hA : MeasurableSet A
meas_π : Measurable.{u_1, u_1} (α := G) (β := G ⧸ Γ) QuotientGroup.mk
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) ((fun (x : G ⧸ Γ) ↦ g • x) ⁻¹' A) : ℝ≥0∞)
    ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) A : ℝ≥0∞)
have h𝓕_translate_fundom : IsFundamentalDomain (↥Γ.op) (g • 𝓕) ν
Tactic: have h𝓕_translate_fundom : IsFundamentalDomain Γ.op (g • 𝓕) ν := h𝓕.smul_of_comm g
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Quotient (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
ν : Measure G
Γ : Subgroup G
μ : Measure (G ⧸ Γ)
inst_2 : QuotientMeasureEqMeasurePreimage ν μ
inst_3 : TopologicalSpace G
inst_4 : IsTopologicalGroup G
inst_5 : BorelSpace G
inst_6 : PolishSpace G
inst_7 : T2Space.{u_1} (G ⧸ Γ)
inst_8 : SecondCountableTopology.{u_1} (G ⧸ Γ)
inst_9 : ν.IsMulLeftInvariant
hasFun : HasFundamentalDomain (↥Γ.op) G ν
g : G
A : Set (G ⧸ Γ)
hA : MeasurableSet A
meas_π : Measurable.{u_1, u_1} (α := G) (β := G ⧸ Γ) QuotientGroup.mk
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
h𝓕_translate_fundom : IsFundamentalDomain (↥Γ.op) (g • 𝓕) ν
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) ((fun (x : G ⧸ Γ) ↦ g • x) ⁻¹' A) : ℝ≥0∞)
    ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) A : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞)
  ((ν : (a : Set G) → ℝ≥0∞) (Quotient.mk (MulAction.orbitRel (↥Γ.op) G) ⁻¹' (fun (x : G ⧸ Γ) ↦ g • x) ⁻¹' A ∩ 𝓕) : ℝ≥0∞)
  ((ν : (a : Set G) → ℝ≥0∞) (Quotient.mk (MulAction.orbitRel (↥Γ.op) G) ⁻¹' A ∩ g • 𝓕) : ℝ≥0∞)
Tactic: rw [h𝓕.projection_respects_measure_apply (μ := μ)
      (meas_π (measurableSet_preimage (measurable_const_smul g) hA)),
      h𝓕_translate_fundom.projection_respects_measure_apply (μ := μ) hA]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Quotient (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
ν : Measure G
Γ : Subgroup G
μ : Measure (G ⧸ Γ)
inst_2 : QuotientMeasureEqMeasurePreimage ν μ
inst_3 : TopologicalSpace G
inst_4 : IsTopologicalGroup G
inst_5 : BorelSpace G
inst_6 : PolishSpace G
inst_7 : T2Space.{u_1} (G ⧸ Γ)
inst_8 : SecondCountableTopology.{u_1} (G ⧸ Γ)
inst_9 : ν.IsMulLeftInvariant
hasFun : HasFundamentalDomain (↥Γ.op) G ν
g : G
A : Set (G ⧸ Γ)
hA : MeasurableSet A
meas_π : Measurable.{u_1, u_1} (α := G) (β := G ⧸ Γ) QuotientGroup.mk
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
h𝓕_translate_fundom : IsFundamentalDomain (↥Γ.op) (g • 𝓕) ν
⊢ Eq (α := ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (Quotient.mk (MulAction.orbitRel (↥Γ.op) G) ⁻¹' (fun (x : G ⧸ Γ) ↦ g • x) ⁻¹' A ∩ 𝓕) :
      ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (Quotient.mk (MulAction.orbitRel (↥Γ.op) G) ⁻¹' A ∩ g • 𝓕) : ℝ≥0∞)
have change : Eq (α := ℝ≥0∞)
  ((ν : (a : Set G) → ℝ≥0∞) (preimage (β := G ⧸ Γ) QuotientGroup.mk ((fun (x : G ⧸ Γ) ↦ g • x) ⁻¹' A) ∩ 𝓕) : ℝ≥0∞)
  ((ν : (a : Set G) → ℝ≥0∞) (QuotientGroup.mk ⁻¹' A ∩ g • 𝓕) : ℝ≥0∞)
Tactic: change ν ((π ⁻¹' _) ∩ _) = ν ((π ⁻¹' _) ∩ _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Quotient (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
ν : Measure G
Γ : Subgroup G
μ : Measure (G ⧸ Γ)
inst_2 : QuotientMeasureEqMeasurePreimage ν μ
inst_3 : TopologicalSpace G
inst_4 : IsTopologicalGroup G
inst_5 : BorelSpace G
inst_6 : PolishSpace G
inst_7 : T2Space.{u_1} (G ⧸ Γ)
inst_8 : SecondCountableTopology.{u_1} (G ⧸ Γ)
inst_9 : ν.IsMulLeftInvariant
hasFun : HasFundamentalDomain (↥Γ.op) G ν
g : G
A : Set (G ⧸ Γ)
hA : MeasurableSet A
meas_π : Measurable.{u_1, u_1} (α := G) (β := G ⧸ Γ) QuotientGroup.mk
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
h𝓕_translate_fundom : IsFundamentalDomain (↥Γ.op) (g • 𝓕) ν
π_preA : Set G := QuotientGroup.mk ⁻¹' A
⊢ Eq (α := Set G) (preimage (β := G ⧸ Γ) QuotientGroup.mk ((fun (x : G ⧸ Γ) ↦ g • x) ⁻¹' A))
    ((fun (x : G) ↦ g * x) ⁻¹' π_preA)
have h : ∀ (x : G),
  Membership.mem (γ := Set G) (preimage (β := G ⧸ Γ) QuotientGroup.mk ((fun (x : G ⧸ Γ) ↦ g • x) ⁻¹' A)) x ↔
    Membership.mem (γ := Set G) ((fun (x : G) ↦ g * x) ⁻¹' π_preA) x
Tactic: ext1
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Quotient (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
ν : Measure G
Γ : Subgroup G
μ : Measure (G ⧸ Γ)
inst_2 : QuotientMeasureEqMeasurePreimage ν μ
inst_3 : TopologicalSpace G
inst_4 : IsTopologicalGroup G
inst_5 : BorelSpace G
inst_6 : PolishSpace G
inst_7 : T2Space.{u_1} (G ⧸ Γ)
inst_8 : SecondCountableTopology.{u_1} (G ⧸ Γ)
inst_9 : ν.IsMulLeftInvariant
hasFun : HasFundamentalDomain (↥Γ.op) G ν
g : G
A : Set (G ⧸ Γ)
hA : MeasurableSet A
meas_π : Measurable.{u_1, u_1} (α := G) (β := G ⧸ Γ) QuotientGroup.mk
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
h𝓕_translate_fundom : IsFundamentalDomain (↥Γ.op) (g • 𝓕) ν
π_preA : Set G := QuotientGroup.mk ⁻¹' A
⊢ Eq (α := ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (preimage (β := G ⧸ Γ) QuotientGroup.mk ((fun (x : G ⧸ Γ) ↦ g • x) ⁻¹' A) ∩ 𝓕) : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (π_preA ∩ g • 𝓕) : ℝ≥0∞)
have this : Eq (α := Set G) (preimage (β := G ⧸ Γ) QuotientGroup.mk ((fun (x : G ⧸ Γ) ↦ g • x) ⁻¹' A))
  ((fun (x : G) ↦ g * x) ⁻¹' π_preA)
Tactic: have : π ⁻¹' ((fun x : G ⧸ Γ => g • x) ⁻¹' A) = (g * ·) ⁻¹' π_preA := by ext1; simp [π_preA]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Quotient (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
ν : Measure G
Γ : Subgroup G
μ : Measure (G ⧸ Γ)
inst_2 : QuotientMeasureEqMeasurePreimage ν μ
inst_3 : TopologicalSpace G
inst_4 : IsTopologicalGroup G
inst_5 : BorelSpace G
inst_6 : PolishSpace G
inst_7 : T2Space.{u_1} (G ⧸ Γ)
inst_8 : SecondCountableTopology.{u_1} (G ⧸ Γ)
inst_9 : ν.IsMulLeftInvariant
hasFun : HasFundamentalDomain (↥Γ.op) G ν
g : G
A : Set (G ⧸ Γ)
hA : MeasurableSet A
meas_π : Measurable.{u_1, u_1} (α := G) (β := G ⧸ Γ) QuotientGroup.mk
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
h𝓕_translate_fundom : IsFundamentalDomain (↥Γ.op) (g • 𝓕) ν
π_preA : Set G := QuotientGroup.mk ⁻¹' A
this :
  Eq (α := Set G) (preimage (β := G ⧸ Γ) QuotientGroup.mk ((fun (x : G ⧸ Γ) ↦ g • x) ⁻¹' A))
    ((fun (x : G) ↦ g * x) ⁻¹' π_preA)
⊢ Eq (α := ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (preimage (β := G ⧸ Γ) QuotientGroup.mk ((fun (x : G ⧸ Γ) ↦ g • x) ⁻¹' A) ∩ 𝓕) : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (π_preA ∩ g • 𝓕) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ g * x) ⁻¹' π_preA ∩ 𝓕) : ℝ≥0∞)
  ((ν : (a : Set G) → ℝ≥0∞) (π_preA ∩ g • 𝓕) : ℝ≥0∞)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Quotient (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
ν : Measure G
Γ : Subgroup G
μ : Measure (G ⧸ Γ)
inst_2 : QuotientMeasureEqMeasurePreimage ν μ
inst_3 : TopologicalSpace G
inst_4 : IsTopologicalGroup G
inst_5 : BorelSpace G
inst_6 : PolishSpace G
inst_7 : T2Space.{u_1} (G ⧸ Γ)
inst_8 : SecondCountableTopology.{u_1} (G ⧸ Γ)
inst_9 : ν.IsMulLeftInvariant
hasFun : HasFundamentalDomain (↥Γ.op) G ν
g : G
A : Set (G ⧸ Γ)
hA : MeasurableSet A
meas_π : Measurable.{u_1, u_1} (α := G) (β := G ⧸ Γ) QuotientGroup.mk
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
h𝓕_translate_fundom : IsFundamentalDomain (↥Γ.op) (g • 𝓕) ν
π_preA : Set G := QuotientGroup.mk ⁻¹' A
this :
  Eq (α := Set G) (preimage (β := G ⧸ Γ) QuotientGroup.mk ((fun (x : G ⧸ Γ) ↦ g • x) ⁻¹' A))
    ((fun (x : G) ↦ g * x) ⁻¹' π_preA)
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ g * x) ⁻¹' π_preA ∩ 𝓕) : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (π_preA ∩ (fun (x : G) ↦ g⁻¹ * x) ⁻¹' 𝓕) : ℝ≥0∞)
have trans : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ g * x) ⁻¹' π_preA ∩ 𝓕) : ℝ≥0∞)
  ((ν : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ g * x) ⁻¹' (π_preA ∩ (fun (x : G) ↦ g⁻¹ * x) ⁻¹' 𝓕)) : ℝ≥0∞)
Tactic: trans ν ((g * ·) ⁻¹' (π_preA ∩ (g⁻¹ * ·) ⁻¹' 𝓕))
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Quotient (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
ν : Measure G
Γ : Subgroup G
μ : Measure (G ⧸ Γ)
inst_2 : QuotientMeasureEqMeasurePreimage ν μ
inst_3 : TopologicalSpace G
inst_4 : IsTopologicalGroup G
inst_5 : BorelSpace G
inst_6 : PolishSpace G
inst_7 : T2Space.{u_1} (G ⧸ Γ)
inst_8 : SecondCountableTopology.{u_1} (G ⧸ Γ)
inst_9 : ν.IsMulLeftInvariant
hasFun : HasFundamentalDomain (↥Γ.op) G ν
g : G
A : Set (G ⧸ Γ)
hA : MeasurableSet A
meas_π : Measurable.{u_1, u_1} (α := G) (β := G ⧸ Γ) QuotientGroup.mk
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
h𝓕_translate_fundom : IsFundamentalDomain (↥Γ.op) (g • 𝓕) ν
π_preA : Set G := QuotientGroup.mk ⁻¹' A
this :
  Eq (α := Set G) (preimage (β := G ⧸ Γ) QuotientGroup.mk ((fun (x : G ⧸ Γ) ↦ g • x) ⁻¹' A))
    ((fun (x : G) ↦ g * x) ⁻¹' π_preA)
trans :
  Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ g * x) ⁻¹' π_preA ∩ 𝓕) : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ g * x) ⁻¹' (π_preA ∩ (fun (x : G) ↦ g⁻¹ * x) ⁻¹' 𝓕)) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ g * x) ⁻¹' π_preA ∩ 𝓕) : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (π_preA ∩ (fun (x : G) ↦ g⁻¹ * x) ⁻¹' 𝓕) : ℝ≥0∞)
have trans₁ : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ g * x) ⁻¹' (π_preA ∩ (fun (x : G) ↦ g⁻¹ * x) ⁻¹' 𝓕)) : ℝ≥0∞)
  ((ν : (a : Set G) → ℝ≥0∞) (π_preA ∩ (fun (x : G) ↦ g⁻¹ * x) ⁻¹' 𝓕) : ℝ≥0∞)
Tactic: trans ν ((g * ·) ⁻¹' (π_preA ∩ (g⁻¹ * ·) ⁻¹' 𝓕))
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Quotient (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
ν : Measure G
Γ : Subgroup G
μ : Measure (G ⧸ Γ)
inst_2 : QuotientMeasureEqMeasurePreimage ν μ
inst_3 : TopologicalSpace G
inst_4 : IsTopologicalGroup G
inst_5 : BorelSpace G
inst_6 : PolishSpace G
inst_7 : T2Space.{u_1} (G ⧸ Γ)
inst_8 : SecondCountableTopology.{u_1} (G ⧸ Γ)
inst_9 : ν.IsMulLeftInvariant
hasFun : HasFundamentalDomain (↥Γ.op) G ν
g : G
A : Set (G ⧸ Γ)
hA : MeasurableSet A
meas_π : Measurable.{u_1, u_1} (α := G) (β := G ⧸ Γ) QuotientGroup.mk
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
h𝓕_translate_fundom : IsFundamentalDomain (↥Γ.op) (g • 𝓕) ν
π_preA : Set G := QuotientGroup.mk ⁻¹' A
this :
  Eq (α := Set G) (preimage (β := G ⧸ Γ) QuotientGroup.mk ((fun (x : G ⧸ Γ) ↦ g • x) ⁻¹' A))
    ((fun (x : G) ↦ g * x) ⁻¹' π_preA)
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ g * x) ⁻¹' π_preA ∩ 𝓕) : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ g * x) ⁻¹' (π_preA ∩ (fun (x : G) ↦ g⁻¹ * x) ⁻¹' 𝓕)) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ g * x) ⁻¹' π_preA ∩ 𝓕) : ℝ≥0∞)
  ((ν : (a : Set G) → ℝ≥0∞)
      ((fun (x : G) ↦ g * x) ⁻¹' π_preA ∩ preimage (β := G) (fun (x : G) ↦ g * x) ((fun (x : G) ↦ g⁻¹ * x) ⁻¹' 𝓕)) :
    ℝ≥0∞)
Tactic: rw [preimage_inter]