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
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.2 = (∑ i : ι ⊕ ι', HSMul.hSMul (β := E × F) (Sum.elim t s i) ((v.prod w : (a : ι ⊕ ι') → E × F) i : E × F)).2

Tactic:
simp [hs2, 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
inst_6 : MeasurableSpace E
inst_7 : BorelSpace E
b : Basis ι ℝ E
rw : IsAddHaarMeasure (addHaarMeasure b.parallelepiped)
⊢ IsAddHaarMeasure b.addHaar

Tactic:
rw [Basis.addHaar]

Premises used: Module.Basis.addHaar
-- 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
inst_6 : MeasurableSpace E
inst_7 : BorelSpace E
b : Basis ι ℝ E
⊢ IsAddHaarMeasure (addHaarMeasure b.parallelepiped)

Tactic:
Measure.isAddHaarMeasure_addHaarMeasure _

Premises used: MeasureTheory.Measure.isAddHaarMeasure_addHaarMeasure
-- 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
inst_6 : MeasurableSpace E
inst_7 : BorelSpace E
b : Basis ι ℝ E
⊢ IsAddHaarMeasure (addHaarMeasure b.parallelepiped)

Tactic:
exact Measure.isAddHaarMeasure_addHaarMeasure _

Premises used: MeasureTheory.Measure.isAddHaarMeasure_addHaarMeasure
-- 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
inst_6 : MeasurableSpace E
inst_7 : BorelSpace E
b : Basis ι ℝ E
⊢ FiniteDimensional ℝ E

Tactic:
have : FiniteDimensional ℝ E := b.finiteDimensional_of_finite
-- 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
inst_6 : MeasurableSpace E
inst_7 : BorelSpace E
b : Basis ι ℝ E
this : FiniteDimensional ℝ E
rw : SigmaFinite (m0 := inst_6) (addHaarMeasure b.parallelepiped)
⊢ SigmaFinite (m0 := inst_6) b.addHaar

Tactic:
rw [Basis.addHaar_def]

Premises used: Module.Basis.addHaar_def
-- 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
inst_6 : MeasurableSpace E
inst_7 : BorelSpace E
b : Basis ι ℝ E
this : FiniteDimensional ℝ E
⊢ SigmaFinite (m0 := inst_6) (addHaarMeasure b.parallelepiped)

Tactic:
sigmaFinite_addHaarMeasure

Premises used: MeasureTheory.Measure.sigmaFinite_addHaarMeasure
-- 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
inst_6 : MeasurableSpace E
inst_7 : BorelSpace E
b : Basis ι ℝ E
this : FiniteDimensional ℝ E
⊢ SigmaFinite (m0 := inst_6) (addHaarMeasure b.parallelepiped)

Tactic:
exact sigmaFinite_addHaarMeasure

Premises used: MeasureTheory.Measure.sigmaFinite_addHaarMeasure
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
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
rw :
  addHaarMeasure b.parallelepiped = μ ↔
    Eq (α := ENNReal) ((μ : (a : Set E) → ENNReal) (↑b.parallelepiped : Set E) : ENNReal) (1 : ENNReal)
⊢ b.addHaar = μ ↔ Eq (α := ENNReal) ((μ : (a : Set E) → ENNReal) (↑b.parallelepiped : Set E) : ENNReal) (1 : ENNReal)

Tactic:
rw [Basis.addHaar_def]

Premises used: Module.Basis.addHaar_def
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
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
⊢ addHaarMeasure b.parallelepiped = μ ↔
    Eq (α := ENNReal) ((μ : (a : Set E) → ENNReal) (↑b.parallelepiped : Set E) : ENNReal) (1 : ENNReal)

Tactic:
addHaarMeasure_eq_iff b.parallelepiped μ

Premises used: MeasureTheory.Measure.addHaarMeasure_eq_iff, Module.Basis.parallelepiped
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
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
⊢ addHaarMeasure b.parallelepiped = μ ↔
    Eq (α := ENNReal) ((μ : (a : Set E) → ENNReal) (↑b.parallelepiped : Set E) : ENNReal) (1 : ENNReal)

Tactic:
exact addHaarMeasure_eq_iff b.parallelepiped μ

Premises used: MeasureTheory.Measure.addHaarMeasure_eq_iff, Module.Basis.parallelepiped
-- 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
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
rw₂ rw₃ : Eq (α := Measure E) b.addHaar b.addHaar
⊢ Eq (α := Measure E) (b.reindex e).addHaar b.addHaar

Tactic:
rw [Basis.addHaar, b.parallelepiped_reindex e, ← Basis.addHaar]

Premises used: Module.Basis.parallelepiped_reindex, Module.Basis.addHaar
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
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
rw :
  Eq (α := ENNReal)
    (((addHaarMeasure b.parallelepiped : Measure E) : (a : Set E) → ENNReal)
        (_root_.parallelepiped.{u_1, u_3} (ι := ι) (⇑b : (a : ι) → E)) :
      ENNReal)
    (1 : ENNReal)
⊢ Eq (α := ENNReal)
    (((b.addHaar : Measure E) : (a : Set E) → ENNReal) (_root_.parallelepiped.{u_1, u_3} (ι := ι) (⇑b : (a : ι) → E)) :
      ENNReal)
    (1 : ENNReal)

Tactic:
rw [Basis.addHaar]

Premises used: Module.Basis.addHaar
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
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)
    (((addHaarMeasure b.parallelepiped : Measure E) : (a : Set E) → ENNReal)
        (_root_.parallelepiped.{u_1, u_3} (ι := ι) (⇑b : (a : ι) → E)) :
      ENNReal)
    (1 : ENNReal)

Tactic:
addHaarMeasure_self

Premises used: setOf, MeasureTheory.Measure.addHaarMeasure_self, Set.image, parallelepiped
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
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)
    (((addHaarMeasure b.parallelepiped : Measure E) : (a : Set E) → ENNReal)
        (_root_.parallelepiped.{u_1, u_3} (ι := ι) (⇑b : (a : ι) → E)) :
      ENNReal)
    (1 : ENNReal)

Tactic:
exact addHaarMeasure_self

Premises used: MeasureTheory.Measure.addHaarMeasure_self
-- 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
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
⊢ FiniteDimensional ℝ E

Tactic:
have : FiniteDimensional ℝ E := v.finiteDimensional_of_finite
-- 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
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
⊢ FiniteDimensional ℝ F

Tactic:
have : FiniteDimensional ℝ F := w.finiteDimensional_of_finite
-- 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
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_1 : FiniteDimensional ℝ E
this : FiniteDimensional ℝ F
⊢ Eq (α := Measure (E × F)) ((v.prod w).addHaar (ι := ι ⊕ ι')) (Measure.prod v.addHaar w.addHaar)

Tactic:
simp [(v.prod w).addHaar_eq_iff, Basis.prod_parallelepiped, Basis.addHaar_self]

Premises used: Module.Basis.prod_parallelepiped, Module.Basis.prod, Module.Basis.addHaar_eq_iff, Module.Basis.addHaar_self
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : FiniteDimensional ℝ E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
⊢ IsAddHaarMeasure.{u_3} (G := E) volume

Tactic:
isAddHaarMeasure_basis_addHaar _

Premises used: isAddHaarMeasure_basis_addHaar
-- Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis
Goal:
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
⊢ MeasureSpace ℝ

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
ν : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 ν
μ : Measure (G ⧸ Γ)
inst_2 : QuotientMeasureEqMeasurePreimage ν μ
⊢ MeasurePreserving QuotientGroup.mk (ν.restrict 𝓕) μ

Tactic:
h𝓕.measurePreserving_quotient_mk μ

Premises used: MeasureTheory.IsFundamentalDomain.measurePreserving_quotient_mk
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
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
⊢ Measurable.{u_1, u_1} (α := G) (β := G ⧸ Γ) QuotientGroup.mk

Tactic:
have meas_π : Measurable π := continuous_quotient_mk'.measurable
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
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
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∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) ((fun (x : G ⧸ Γ) ↦ g • x) ⁻¹' A) : ℝ≥0∞)
    ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) A : ℝ≥0∞)

Tactic:
obtain ⟨𝓕, h𝓕⟩ := hasFun.ExistsIsFundamentalDomain

Premises used: MeasureTheory.HasFundamentalDomain.ExistsIsFundamentalDomain
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
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) 𝓕 ν
⊢ IsFundamentalDomain (↥Γ.op) (g • 𝓕) ν

Tactic:
have h𝓕_translate_fundom : IsFundamentalDomain Γ.op (g • 𝓕) ν := h𝓕.smul_of_comm g
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
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 • 𝓕) ν
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∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) ((fun (x : G ⧸ Γ) ↦ g • x) ⁻¹' A) : ℝ≥0∞)
    ((μ : (a : Set (G ⧸ Γ)) → ℝ≥0∞) A : ℝ≥0∞)

Tactic:
rw [h𝓕.projection_respects_measure_apply (μ := μ)
      (meas_π (measurableSet_preimage (measurable_const_smul g) hA)),
      h𝓕_translate_fundom.projection_respects_measure_apply (μ := μ) hA]

Premises used: MeasurableConstSMul.measurable_const_smul, measurableSet_preimage, MeasureTheory.IsFundamentalDomain.projection_respects_measure_apply
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
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 • 𝓕) ν
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∞)
⊢ 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:
change ν ((π ⁻¹' _) ∩ _) = ν ((π ⁻¹' _) ∩ _)
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
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 • 𝓕) ν
set :
  let π_preA := 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∞)
⊢ 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:
set π_preA := π ⁻¹' A
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
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
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
⊢ Eq (α := Set G) (preimage (β := G ⧸ Γ) QuotientGroup.mk ((fun (x : G ⧸ Γ) ↦ g • x) ⁻¹' A))
    ((fun (x : G) ↦ g * x) ⁻¹' π_preA)

Tactic:
ext1
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
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
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:
simp [π_preA]
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
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)

Tactic:
have : π ⁻¹' ((fun x : G ⧸ Γ => g • x) ⁻¹' A) = (g * ·) ⁻¹' π_preA := by ext1; simp [π_preA]
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
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)
rw :
  Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ g * x) ⁻¹' π_preA ∩ 𝓕) : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (π_preA ∩ g • 𝓕) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (preimage (β := G ⧸ Γ) QuotientGroup.mk ((fun (x : G ⧸ Γ) ↦ g • x) ⁻¹' A) ∩ 𝓕) : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (π_preA ∩ g • 𝓕) : ℝ≥0∞)

Tactic:
rw [this]
-- Module: Mathlib.MeasureTheory.Measure.Haar.Quotient
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∞)
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∞)
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set G) → ℝ≥0∞) ((fun (x : G) ↦ g * x) ⁻¹' π_preA ∩ 𝓕) : ℝ≥0∞)
    ((ν : (a : Set G) → ℝ≥0∞) (π_preA ∩ (fun (x : G) ↦ g⁻¹ * x) ⁻¹' 𝓕) : ℝ≥0∞)

Tactic:
trans ν ((g * ·) ⁻¹' (π_preA ∩ (g⁻¹ * ·) ⁻¹' 𝓕))

Premises used: HMul.hMul, Inter.inter, Inv.inv, Set.preimage, DFunLike.coe