awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : SecondCountableTopology G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
μ : Measure G
inst_6 : IsFiniteMeasure μ
inst_7 : μ.InnerRegular
inst_8 : μ.IsMulLeftInvariant
f : G →* G
hf : Dense.{u_1} (X := G) (⋃ (n : ℕ), (⇑f : (a : G) → G)^[n] ⁻¹' 1)
s : Set G
hsm : MeasurableSet s
hs : (⇑f : (a : G) → G) ⁻¹' s = s
n : ℕ
x : G
hx : (⇑f : (a : G) → G)^[n] x = 1
hsn : (⇑f : (a : G) → G)^[n] ⁻¹' s = s
h :
  ∀ (y : G),
    Membership.mem (γ := Set G) ((fun (x_1 : G) ↦ x • x_1) ⁻¹' (⇑f : (a : G) → G)^[n] ⁻¹' s) y ↔
      y ∈ (⇑f : (a : G) → G)^[n] ⁻¹' s
⊢ (fun (x_1 : G) ↦ x • x_1) ⁻¹' (⇑f : (a : G) → G)^[n] ⁻¹' s = (⇑f : (a : G) → G)^[n] ⁻¹' s

Tactic:
ext y
-- Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : SecondCountableTopology G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
μ : Measure G
inst_6 : IsFiniteMeasure μ
inst_7 : μ.InnerRegular
inst_8 : μ.IsMulLeftInvariant
f : G →* G
hf : Dense.{u_1} (X := G) (⋃ (n : ℕ), (⇑f : (a : G) → G)^[n] ⁻¹' 1)
s : Set G
hsm : MeasurableSet s
hs : (⇑f : (a : G) → G) ⁻¹' s = s
n : ℕ
x : G
hx : (⇑f : (a : G) → G)^[n] x = 1
hsn : (⇑f : (a : G) → G)^[n] ⁻¹' s = s
y : G
⊢ Membership.mem (γ := Set G) ((fun (x_1 : G) ↦ x • x_1) ⁻¹' (⇑f : (a : G) → G)^[n] ⁻¹' s) y ↔
    y ∈ (⇑f : (a : G) → G)^[n] ⁻¹' s

Tactic:
simp [hx]
-- Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : SecondCountableTopology G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
inst_6 : CompactSpace G
μ : Measure G
inst_7 : μ.IsHaarMeasure
f : G →* G
hf : Dense.{u_1} (X := G) (⋃ (n : ℕ), (⇑f : (a : G) → G)^[n] ⁻¹' 1)
hcont : Continuous[inst_1, inst_1] (⇑f : (a : G) → G)
hsurj : Surjective (α := G) (β := G) (⇑f : (a : G) → G)
⊢ Ergodic (⇑f : (a : G) → G) μ

Tactic:
⟨f.measurePreserving hcont hsurj rfl, f.preErgodic_of_dense_iUnion_preimage_one hf⟩

Premises used: Ergodic.mk, MonoidHom.preErgodic_of_dense_iUnion_preimage_one, MonoidHom.measurePreserving, rfl
-- Module: Mathlib.Dynamics.Ergodic.Action.Regular
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : MeasurableMul₂ G
inst_3 : MeasurableInv G
μ : Measure G
inst_4 : SFinite μ
inst_5 : μ.IsMulLeftInvariant
⊢ ErgodicSMul G G μ

Tactic:
⟨fun {s} hsm hs ↦ ?_⟩

Premises used: ErgodicSMul.mk
-- Module: Mathlib.Dynamics.Ergodic.Action.Regular
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : MeasurableMul₂ G
inst_3 : MeasurableInv G
μ : Measure G
inst_4 : SFinite μ
inst_5 : μ.IsMulLeftInvariant
refine :
  ∀ {s : Set G} (hsm : MeasurableSet s) (hs : ∀ (g : G), (fun (x : G) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s),
    EventuallyConst s (ae μ)
⊢ ErgodicSMul G G μ

Tactic:
refine ⟨fun {s} hsm hs ↦ ?_⟩
-- Module: Mathlib.Dynamics.Ergodic.Action.Regular
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : MeasurableMul₂ G
inst_3 : MeasurableInv G
μ : Measure G
inst_4 : SFinite μ
inst_5 : μ.IsMulLeftInvariant
s : Set G
hsm : MeasurableSet s
hs : ∀ (g : G), (fun (x : G) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s
this : (∃ᵐ (x : G) ∂μ, x ∈ s) → ∀ᵐ (x : G) ∂μ, x ∈ s
simp : (∀ᵐ (x : G) ∂μ, x ∈ s) ∨ ¬∃ᵐ (x : G) ∂μ, x ∈ s
⊢ EventuallyConst s (ae μ)

Tactic:
simp only [eventuallyConst_set, ← not_frequently]

Premises used: Filter.eventuallyConst_set, Filter.not_frequently
-- Module: Mathlib.Dynamics.Ergodic.Action.Regular
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : MeasurableMul₂ G
inst_3 : MeasurableInv G
μ : Measure G
inst_4 : SFinite μ
inst_5 : μ.IsMulLeftInvariant
s : Set G
hsm : MeasurableSet s
hs : ∀ (g : G), (fun (x : G) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s
this : (∃ᵐ (x : G) ∂μ, x ∈ s) → ∀ᵐ (x : G) ∂μ, x ∈ s
⊢ (∀ᵐ (x : G) ∂μ, x ∈ s) ∨ ¬∃ᵐ (x : G) ∂μ, x ∈ s

Tactic:
or_not_of_imp this

Premises used: or_not_of_imp
-- Module: Mathlib.Dynamics.Ergodic.Action.Regular
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : MeasurableMul₂ G
inst_3 : MeasurableInv G
μ : Measure G
inst_4 : SFinite μ
inst_5 : μ.IsMulLeftInvariant
s : Set G
hsm : MeasurableSet s
hs : ∀ (g : G), (fun (x : G) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s
this : (∃ᵐ (x : G) ∂μ, x ∈ s) → ∀ᵐ (x : G) ∂μ, x ∈ s
⊢ (∀ᵐ (x : G) ∂μ, x ∈ s) ∨ ¬∃ᵐ (x : G) ∂μ, x ∈ s

Tactic:
exact or_not_of_imp this

Premises used: or_not_of_imp
-- Module: Mathlib.Dynamics.Ergodic.Action.Regular
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : MeasurableMul₂ G
inst_3 : MeasurableInv G
μ : Measure G
inst_4 : SFinite μ
inst_5 : μ.IsMulLeftInvariant
s : Set G
hsm : MeasurableSet s
hs : ∀ (g : G), (fun (x : G) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s
suffices : (∃ᵐ (x : G) ∂μ, x ∈ s) → ∀ᵐ (x : G) ∂μ, x ∈ s
⊢ EventuallyConst s (ae μ)

Tactic:
suffices (∃ᵐ x ∂μ, x ∈ s) → ∀ᵐ x ∂μ, x ∈ s by
    simp only [eventuallyConst_set, ← not_frequently]
    exact or_not_of_imp this
-- Module: Mathlib.Dynamics.Ergodic.Action.Regular
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : MeasurableMul₂ G
inst_3 : MeasurableInv G
μ : Measure G
inst_4 : SFinite μ
inst_5 : μ.IsMulLeftInvariant
s : Set G
hsm : MeasurableSet s
hs : ∀ (g : G), (fun (x : G) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s
hμs : ∃ᵐ (x : G) ∂μ, x ∈ s
⊢ ∃ a ∈ s, ∀ᵐ (b : G) ∂μ, b * a ∈ s ↔ a ∈ s

Tactic:
(hμs.and_eventually ?_).exists

Premises used: Filter.Frequently.and_eventually, Filter.Frequently.exists
-- Module: Mathlib.Dynamics.Ergodic.Action.Regular
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : MeasurableMul₂ G
inst_3 : MeasurableInv G
μ : Measure G
inst_4 : SFinite μ
inst_5 : μ.IsMulLeftInvariant
s : Set G
hsm : MeasurableSet s
hs : ∀ (g : G), (fun (x : G) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s
hμs : ∃ᵐ (x : G) ∂μ, x ∈ s
refine : ∀ᵐ (x : G) (b : G) ∂μ, b * x ∈ s ↔ x ∈ s
⊢ ∃ a ∈ s, ∀ᵐ (b : G) ∂μ, b * a ∈ s ↔ a ∈ s

Tactic:
refine (hμs.and_eventually ?_).exists

Premises used: Filter.Frequently.and_eventually, Filter.Frequently.exists
-- Module: Mathlib.Dynamics.Ergodic.Action.Regular
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : MeasurableMul₂ G
inst_3 : MeasurableInv G
μ : Measure G
inst_4 : SFinite μ
inst_5 : μ.IsMulLeftInvariant
s : Set G
hsm : MeasurableSet s
hs : ∀ (g : G), (fun (x : G) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s
hμs : ∃ᵐ (x : G) ∂μ, x ∈ s
rw : ∀ᵐ (y : G) (x : G) ∂μ, y * x ∈ s ↔ x ∈ s
rw₁ : MeasurableSet.{u_1} (α := G × G) {x : G × G | x.2 * x.1 ∈ s ↔ x.1 ∈ s}
⊢ ∀ᵐ (x : G) (b : G) ∂μ, b * x ∈ s ↔ x ∈ s

Tactic:
rw [ae_ae_comm]

Premises used: MeasureTheory.Measure.ae_ae_comm
-- Module: Mathlib.Dynamics.Ergodic.Action.Regular
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : MeasurableMul₂ G
inst_3 : MeasurableInv G
μ : Measure G
inst_4 : SFinite μ
inst_5 : μ.IsMulLeftInvariant
s : Set G
hsm : MeasurableSet s
hs : ∀ (g : G), (fun (x : G) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s
hμs : ∃ᵐ (x : G) ∂μ, x ∈ s
⊢ ∀ᵐ (y : G) (x : G) ∂μ, y * x ∈ s ↔ x ∈ s

Tactic:
ae_of_all _ fun b ↦ (hs b).mem_iff

Premises used: Filter.EventuallyEq.mem_iff, MeasureTheory.ae_of_all
-- Module: Mathlib.Dynamics.Ergodic.Action.Regular
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : MeasurableMul₂ G
inst_3 : MeasurableInv G
μ : Measure G
inst_4 : SFinite μ
inst_5 : μ.IsMulLeftInvariant
s : Set G
hsm : MeasurableSet s
hs : ∀ (g : G), (fun (x : G) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s
hμs : ∃ᵐ (x : G) ∂μ, x ∈ s
⊢ ∀ᵐ (y : G) (x : G) ∂μ, y * x ∈ s ↔ x ∈ s

Tactic:
exact ae_of_all _ fun b ↦ (hs b).mem_iff

Premises used: Filter.EventuallyEq.mem_iff, MeasureTheory.ae_of_all
-- Module: Mathlib.Dynamics.Ergodic.Action.Regular
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : MeasurableMul₂ G
inst_3 : MeasurableInv G
μ : Measure G
inst_4 : SFinite μ
inst_5 : μ.IsMulLeftInvariant
s : Set G
hsm : MeasurableSet s
hs : ∀ (g : G), (fun (x : G) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s
hμs : ∃ᵐ (x : G) ∂μ, x ∈ s
⊢ MeasurableSet.{u_1} (α := G × G) {x : G × G | x.2 * x.1 ∈ s ↔ x.1 ∈ s}

Tactic:
((hsm.preimage <| measurable_snd.mul measurable_fst).mem.iff
        (hsm.preimage measurable_fst).mem).setOf

Premises used: MeasurableSet.mem, MeasurableSet.preimage, Measurable.mul, Set.Mem, setOf, Measurable.setOf, Set.preimage, measurable_snd, Measurable.iff, measurable_fst
-- Module: Mathlib.Dynamics.Ergodic.Action.Regular
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : MeasurableMul₂ G
inst_3 : MeasurableInv G
μ : Measure G
inst_4 : SFinite μ
inst_5 : μ.IsMulLeftInvariant
s : Set G
hsm : MeasurableSet s
hs : ∀ (g : G), (fun (x : G) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s
hμs : ∃ᵐ (x : G) ∂μ, x ∈ s
⊢ MeasurableSet.{u_1} (α := G × G) {x : G × G | x.2 * x.1 ∈ s ↔ x.1 ∈ s}

Tactic:
exact ((hsm.preimage <| measurable_snd.mul measurable_fst).mem.iff
        (hsm.preimage measurable_fst).mem).setOf

Premises used: MeasurableSet.mem, MeasurableSet.preimage, Measurable.mul, Measurable.setOf, measurable_snd, Measurable.iff, measurable_fst
-- Module: Mathlib.Dynamics.Ergodic.Action.Regular
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : MeasurableMul₂ G
inst_3 : MeasurableInv G
μ : Measure G
inst_4 : SFinite μ
inst_5 : μ.IsMulLeftInvariant
s : Set G
hsm : MeasurableSet s
hs : ∀ (g : G), (fun (x : G) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s
hμs : ∃ᵐ (x : G) ∂μ, x ∈ s
obtain : ∀ (a : G) (has : a ∈ s) (ha : ∀ᵐ (b : G) ∂μ, b * a ∈ s ↔ a ∈ s), ∀ᵐ (x : G) ∂μ, x ∈ s
⊢ ∀ᵐ (x : G) ∂μ, x ∈ s

Tactic:
obtain ⟨a, has, ha⟩ : ∃ a ∈ s, ∀ᵐ b ∂μ, (b * a ∈ s ↔ a ∈ s) := by
    refine (hμs.and_eventually ?_).exists
    rw [ae_ae_comm]
    · exact ae_of_all _ fun b ↦ (hs b).mem_iff
    · exact ((hsm.preimage <| measurable_snd.mul measurable_fst).mem.iff
        (hsm.preimage measurable_fst).mem).setOf
-- Module: Mathlib.Dynamics.Ergodic.Action.Regular
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : MeasurableMul₂ G
inst_3 : MeasurableInv G
μ : Measure G
inst_4 : SFinite μ
inst_5 : μ.IsMulLeftInvariant
s : Set G
hsm : MeasurableSet s
hs : ∀ (g : G), (fun (x : G) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s
hμs : ∃ᵐ (x : G) ∂μ, x ∈ s
a : G
has : a ∈ s
ha : ∀ᵐ (b : G) ∂μ, b * a ∈ s ↔ a ∈ s
⊢ ∀ᵐ (x : G) ∂μ, x ∈ s

Tactic:
simpa [has] using (MeasureTheory.quasiMeasurePreserving_mul_right μ a⁻¹).ae ha

Premises used: MeasureTheory.Measure.QuasiMeasurePreserving.ae, Inv.inv, MeasureTheory.quasiMeasurePreserving_mul_right
-- Module: Mathlib.Dynamics.Ergodic.Action.Regular
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : MeasurableMul₂ G
inst_3 : MeasurableInv G
μ : Measure G
inst_4 : SFinite μ
inst_5 : μ.IsMulRightInvariant
⊢ ErgodicSMul Gᵐᵒᵖ G μ

Tactic:
⟨fun {s} hsm hs ↦ ?_⟩

Premises used: ErgodicSMul.mk
-- Module: Mathlib.Dynamics.Ergodic.Action.Regular
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : MeasurableMul₂ G
inst_3 : MeasurableInv G
μ : Measure G
inst_4 : SFinite μ
inst_5 : μ.IsMulRightInvariant
refine :
  ∀ {s : Set G} (hsm : MeasurableSet s) (hs : ∀ (g : Gᵐᵒᵖ), (fun (x : G) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s),
    EventuallyConst s (ae μ)
⊢ ErgodicSMul Gᵐᵒᵖ G μ

Tactic:
refine ⟨fun {s} hsm hs ↦ ?_⟩
-- Module: Mathlib.Dynamics.Ergodic.Action.Regular
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : MeasurableMul₂ G
inst_3 : MeasurableInv G
μ : Measure G
inst_4 : SFinite μ
inst_5 : μ.IsMulRightInvariant
s : Set G
hsm : MeasurableSet s
hs : ∀ (g : Gᵐᵒᵖ), (fun (x : G) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s
this : (∃ᵐ (x : G) ∂μ, x ∈ s) → ∀ᵐ (x : G) ∂μ, x ∈ s
simp : (∀ᵐ (x : G) ∂μ, x ∈ s) ∨ ¬∃ᵐ (x : G) ∂μ, x ∈ s
⊢ EventuallyConst s (ae μ)

Tactic:
simp only [eventuallyConst_set, ← not_frequently]

Premises used: Filter.eventuallyConst_set, Filter.not_frequently
-- Module: Mathlib.Dynamics.Ergodic.Action.Regular
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : MeasurableMul₂ G
inst_3 : MeasurableInv G
μ : Measure G
inst_4 : SFinite μ
inst_5 : μ.IsMulRightInvariant
s : Set G
hsm : MeasurableSet s
hs : ∀ (g : Gᵐᵒᵖ), (fun (x : G) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s
this : (∃ᵐ (x : G) ∂μ, x ∈ s) → ∀ᵐ (x : G) ∂μ, x ∈ s
⊢ (∀ᵐ (x : G) ∂μ, x ∈ s) ∨ ¬∃ᵐ (x : G) ∂μ, x ∈ s

Tactic:
or_not_of_imp this

Premises used: or_not_of_imp
-- Module: Mathlib.Dynamics.Ergodic.Action.Regular
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : MeasurableMul₂ G
inst_3 : MeasurableInv G
μ : Measure G
inst_4 : SFinite μ
inst_5 : μ.IsMulRightInvariant
s : Set G
hsm : MeasurableSet s
hs : ∀ (g : Gᵐᵒᵖ), (fun (x : G) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s
this : (∃ᵐ (x : G) ∂μ, x ∈ s) → ∀ᵐ (x : G) ∂μ, x ∈ s
⊢ (∀ᵐ (x : G) ∂μ, x ∈ s) ∨ ¬∃ᵐ (x : G) ∂μ, x ∈ s

Tactic:
exact or_not_of_imp this

Premises used: or_not_of_imp
-- Module: Mathlib.Dynamics.Ergodic.Action.Regular
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : MeasurableMul₂ G
inst_3 : MeasurableInv G
μ : Measure G
inst_4 : SFinite μ
inst_5 : μ.IsMulRightInvariant
s : Set G
hsm : MeasurableSet s
hs : ∀ (g : Gᵐᵒᵖ), (fun (x : G) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s
suffices : (∃ᵐ (x : G) ∂μ, x ∈ s) → ∀ᵐ (x : G) ∂μ, x ∈ s
⊢ EventuallyConst s (ae μ)

Tactic:
suffices (∃ᵐ x ∂μ, x ∈ s) → ∀ᵐ x ∂μ, x ∈ s by
    simp only [eventuallyConst_set, ← not_frequently]
    exact or_not_of_imp this
-- Module: Mathlib.Dynamics.Ergodic.Action.Regular
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : MeasurableMul₂ G
inst_3 : MeasurableInv G
μ : Measure G
inst_4 : SFinite μ
inst_5 : μ.IsMulRightInvariant
s : Set G
hsm : MeasurableSet s
hs : ∀ (g : Gᵐᵒᵖ), (fun (x : G) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s
hμs : ∃ᵐ (x : G) ∂μ, x ∈ s
⊢ ∃ a ∈ s, ∀ᵐ (b : G) ∂μ, a * b ∈ s ↔ a ∈ s

Tactic:
(hμs.and_eventually ?_).exists

Premises used: Filter.Frequently.and_eventually, Filter.Frequently.exists
-- Module: Mathlib.Dynamics.Ergodic.Action.Regular
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : MeasurableMul₂ G
inst_3 : MeasurableInv G
μ : Measure G
inst_4 : SFinite μ
inst_5 : μ.IsMulRightInvariant
s : Set G
hsm : MeasurableSet s
hs : ∀ (g : Gᵐᵒᵖ), (fun (x : G) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s
hμs : ∃ᵐ (x : G) ∂μ, x ∈ s
refine : ∀ᵐ (x : G) (b : G) ∂μ, x * b ∈ s ↔ x ∈ s
⊢ ∃ a ∈ s, ∀ᵐ (b : G) ∂μ, a * b ∈ s ↔ a ∈ s

Tactic:
refine (hμs.and_eventually ?_).exists

Premises used: Filter.Frequently.and_eventually, Filter.Frequently.exists
-- Module: Mathlib.Dynamics.Ergodic.Action.Regular
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : MeasurableMul₂ G
inst_3 : MeasurableInv G
μ : Measure G
inst_4 : SFinite μ
inst_5 : μ.IsMulRightInvariant
s : Set G
hsm : MeasurableSet s
hs : ∀ (g : Gᵐᵒᵖ), (fun (x : G) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s
hμs : ∃ᵐ (x : G) ∂μ, x ∈ s
rw : ∀ᵐ (y : G) (x : G) ∂μ, x * y ∈ s ↔ x ∈ s
rw₁ : MeasurableSet.{u_1} (α := G × G) {x : G × G | x.1 * x.2 ∈ s ↔ x.1 ∈ s}
⊢ ∀ᵐ (x : G) (b : G) ∂μ, x * b ∈ s ↔ x ∈ s

Tactic:
rw [ae_ae_comm]

Premises used: MeasureTheory.Measure.ae_ae_comm
-- Module: Mathlib.Dynamics.Ergodic.Action.Regular
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : MeasurableMul₂ G
inst_3 : MeasurableInv G
μ : Measure G
inst_4 : SFinite μ
inst_5 : μ.IsMulRightInvariant
s : Set G
hsm : MeasurableSet s
hs : ∀ (g : Gᵐᵒᵖ), (fun (x : G) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s
hμs : ∃ᵐ (x : G) ∂μ, x ∈ s
⊢ ∀ᵐ (y : G) (x : G) ∂μ, x * y ∈ s ↔ x ∈ s

Tactic:
ae_of_all _ fun b ↦ (hs ⟨b⟩).mem_iff

Premises used: Filter.EventuallyEq.mem_iff, MeasureTheory.ae_of_all, PreOpposite.op'
-- Module: Mathlib.Dynamics.Ergodic.Action.Regular
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : MeasurableMul₂ G
inst_3 : MeasurableInv G
μ : Measure G
inst_4 : SFinite μ
inst_5 : μ.IsMulRightInvariant
s : Set G
hsm : MeasurableSet s
hs : ∀ (g : Gᵐᵒᵖ), (fun (x : G) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s
hμs : ∃ᵐ (x : G) ∂μ, x ∈ s
⊢ ∀ᵐ (y : G) (x : G) ∂μ, x * y ∈ s ↔ x ∈ s

Tactic:
exact ae_of_all _ fun b ↦ (hs ⟨b⟩).mem_iff

Premises used: Filter.EventuallyEq.mem_iff, MeasureTheory.ae_of_all, PreOpposite.op'
-- Module: Mathlib.Dynamics.Ergodic.Action.Regular
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : MeasurableMul₂ G
inst_3 : MeasurableInv G
μ : Measure G
inst_4 : SFinite μ
inst_5 : μ.IsMulRightInvariant
s : Set G
hsm : MeasurableSet s
hs : ∀ (g : Gᵐᵒᵖ), (fun (x : G) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s
hμs : ∃ᵐ (x : G) ∂μ, x ∈ s
⊢ MeasurableSet.{u_1} (α := G × G) {x : G × G | x.1 * x.2 ∈ s ↔ x.1 ∈ s}

Tactic:
((hsm.preimage <| measurable_fst.mul measurable_snd).mem.iff
        (hsm.preimage measurable_fst).mem).setOf

Premises used: MeasurableSet.mem, MeasurableSet.preimage, Measurable.mul, Set.Mem, setOf, Measurable.setOf, Set.preimage, measurable_snd, Measurable.iff, measurable_fst
-- Module: Mathlib.Dynamics.Ergodic.Action.Regular
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : MeasurableMul₂ G
inst_3 : MeasurableInv G
μ : Measure G
inst_4 : SFinite μ
inst_5 : μ.IsMulRightInvariant
s : Set G
hsm : MeasurableSet s
hs : ∀ (g : Gᵐᵒᵖ), (fun (x : G) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s
hμs : ∃ᵐ (x : G) ∂μ, x ∈ s
⊢ MeasurableSet.{u_1} (α := G × G) {x : G × G | x.1 * x.2 ∈ s ↔ x.1 ∈ s}

Tactic:
exact ((hsm.preimage <| measurable_fst.mul measurable_snd).mem.iff
        (hsm.preimage measurable_fst).mem).setOf

Premises used: MeasurableSet.mem, MeasurableSet.preimage, Measurable.mul, Measurable.setOf, measurable_snd, Measurable.iff, measurable_fst
-- Module: Mathlib.Dynamics.Ergodic.Action.Regular
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : MeasurableMul₂ G
inst_3 : MeasurableInv G
μ : Measure G
inst_4 : SFinite μ
inst_5 : μ.IsMulRightInvariant
s : Set G
hsm : MeasurableSet s
hs : ∀ (g : Gᵐᵒᵖ), (fun (x : G) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s
hμs : ∃ᵐ (x : G) ∂μ, x ∈ s
obtain : ∀ (a : G) (has : a ∈ s) (ha : ∀ᵐ (b : G) ∂μ, a * b ∈ s ↔ a ∈ s), ∀ᵐ (x : G) ∂μ, x ∈ s
⊢ ∀ᵐ (x : G) ∂μ, x ∈ s

Tactic:
obtain ⟨a, has, ha⟩ : ∃ a ∈ s, ∀ᵐ b ∂μ, (a * b ∈ s ↔ a ∈ s) := by
    refine (hμs.and_eventually ?_).exists
    rw [ae_ae_comm]
    · exact ae_of_all _ fun b ↦ (hs ⟨b⟩).mem_iff
    · exact ((hsm.preimage <| measurable_fst.mul measurable_snd).mem.iff
        (hsm.preimage measurable_fst).mem).setOf
-- Module: Mathlib.Dynamics.Ergodic.Action.Regular
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : MeasurableMul₂ G
inst_3 : MeasurableInv G
μ : Measure G
inst_4 : SFinite μ
inst_5 : μ.IsMulRightInvariant
s : Set G
hsm : MeasurableSet s
hs : ∀ (g : Gᵐᵒᵖ), (fun (x : G) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s
hμs : ∃ᵐ (x : G) ∂μ, x ∈ s
a : G
has : a ∈ s
ha : ∀ᵐ (b : G) ∂μ, a * b ∈ s ↔ a ∈ s
⊢ ∀ᵐ (x : G) ∂μ, x ∈ s

Tactic:
simpa [has] using (quasiMeasurePreserving_mul_left μ a⁻¹).ae ha

Premises used: MeasureTheory.Measure.QuasiMeasurePreserving.ae, MeasureTheory.quasiMeasurePreserving_mul_left, Inv.inv
-- Module: Mathlib.Dynamics.Ergodic.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
hs : NullMeasurableSet s volume
ι : Type u_1
l : Filter ι
inst : l.NeBot
u : ι → AddCircle T
hu₁ : ∀ (i : ι), u i +ᵥ s =ᶠ[ae (F := Measure (AddCircle T)) volume] s
hu₂ : Tendsto (addOrderOf ∘ u) l atTop
set :
  let μ : Measure (AddCircle T) := volume;
  ∀ (hs : NullMeasurableSet s μ) (hu₁ : ∀ (i : ι), u i +ᵥ s =ᶠ[ae μ] s), s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ
⊢ s =ᶠ[ae (F := Measure (AddCircle T)) volume] ∅ ∨ s =ᶠ[ae (F := Measure (AddCircle T)) volume] univ

Tactic:
set μ := (volume : Measure <| AddCircle T)

Premises used: MeasureTheory.MeasureSpace.volume
-- Module: Mathlib.Dynamics.Ergodic.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst : l.NeBot
u : ι → AddCircle T
hu₂ : Tendsto (addOrderOf ∘ u) l atTop
μ : Measure (AddCircle T) := volume
hs : NullMeasurableSet s μ
hu₁ : ∀ (i : ι), u i +ᵥ s =ᶠ[ae μ] s
⊢ let n := addOrderOf ∘ u;
  Tendsto n l atTop

Tactic:
set n : ι → ℕ := addOrderOf ∘ u

Premises used: addOrderOf
-- Module: Mathlib.Dynamics.Ergodic.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst : l.NeBot
u : ι → AddCircle T
μ : Measure (AddCircle T) := volume
hs : NullMeasurableSet s μ
hu₁ : ∀ (i : ι), u i +ᵥ s =ᶠ[ae μ] s
n : ι → ℕ := addOrderOf ∘ u
hu₂ : Tendsto n l atTop
⊢ 0 < T

Tactic:
have hT₀ : 0 < T := hT.out
-- Module: Mathlib.Dynamics.Ergodic.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst : l.NeBot
u : ι → AddCircle T
μ : Measure (AddCircle T) := volume
hs : NullMeasurableSet s μ
hu₁ : ∀ (i : ι), u i +ᵥ s =ᶠ[ae μ] s
n : ι → ℕ := addOrderOf ∘ u
hu₂ : Tendsto n l atTop
hT₀ : 0 < T
⊢ ENNReal.ofReal T ≠ 0

Tactic:
simpa
-- Module: Mathlib.Dynamics.Ergodic.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst : l.NeBot
u : ι → AddCircle T
μ : Measure (AddCircle T) := volume
hs : NullMeasurableSet s μ
hu₁ : ∀ (i : ι), u i +ᵥ s =ᶠ[ae μ] s
n : ι → ℕ := addOrderOf ∘ u
hu₂ : Tendsto n l atTop
hT₀ : 0 < T
⊢ ENNReal.ofReal T ≠ 0

Tactic:
have hT₁ : ENNReal.ofReal T ≠ 0 := by simpa
-- Module: Mathlib.Dynamics.Ergodic.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst : l.NeBot
u : ι → AddCircle T
μ : Measure (AddCircle T) := volume
hs : NullMeasurableSet s μ
hu₁ : ∀ (i : ι), u i +ᵥ s =ᶠ[ae μ] s
n : ι → ℕ := addOrderOf ∘ u
hu₂ : Tendsto n l atTop
hT₀ : 0 < T
hT₁ : ENNReal.ofReal T ≠ 0
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∨
    (μ : (a : Set (AddCircle T)) → ℝ≥0∞) s = ENNReal.ofReal T
⊢ s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ

Tactic:
rw [ae_eq_empty, ae_eq_univ_iff_measure_eq hs, AddCircle.measure_univ]

Premises used: AddCircle.measure_univ, MeasureTheory.ae_eq_empty, MeasureTheory.ae_eq_univ_iff_measure_eq
-- Module: Mathlib.Dynamics.Ergodic.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst : l.NeBot
u : ι → AddCircle T
μ : Measure (AddCircle T) := volume
hs : NullMeasurableSet s μ
hu₁ : ∀ (i : ι), u i +ᵥ s =ᶠ[ae μ] s
n : ι → ℕ := addOrderOf ∘ u
hu₂ : Tendsto n l atTop
hT₀ : 0 < T
hT₁ : ENNReal.ofReal T ≠ 0
inl :
  ∀ (h : Eq (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∨
      (μ : (a : Set (AddCircle T)) → ℝ≥0∞) s = ENNReal.ofReal T
inr :
  ∀ (h : Ne (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∨
      (μ : (a : Set (AddCircle T)) → ℝ≥0∞) s = ENNReal.ofReal T
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∨
    (μ : (a : Set (AddCircle T)) → ℝ≥0∞) s = ENNReal.ofReal T

Tactic:
rcases eq_or_ne (μ s) 0 with h | h

Premises used: eq_or_ne, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Dynamics.Ergodic.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst : l.NeBot
u : ι → AddCircle T
μ : Measure (AddCircle T) := volume
hs : NullMeasurableSet s μ
hu₁ : ∀ (i : ι), u i +ᵥ s =ᶠ[ae μ] s
n : ι → ℕ := addOrderOf ∘ u
hu₂ : Tendsto n l atTop
hT₀ : 0 < T
hT₁ : ENNReal.ofReal T ≠ 0
h : Eq (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∨
    (μ : (a : Set (AddCircle T)) → ℝ≥0∞) s = ENNReal.ofReal T

Tactic:
Or.inl h

Premises used: Or.inl
-- Module: Mathlib.Dynamics.Ergodic.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst : l.NeBot
u : ι → AddCircle T
μ : Measure (AddCircle T) := volume
hs : NullMeasurableSet s μ
hu₁ : ∀ (i : ι), u i +ᵥ s =ᶠ[ae μ] s
n : ι → ℕ := addOrderOf ∘ u
hu₂ : Tendsto n l atTop
hT₀ : 0 < T
hT₁ : ENNReal.ofReal T ≠ 0
h : Eq (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∨
    (μ : (a : Set (AddCircle T)) → ℝ≥0∞) s = ENNReal.ofReal T

Tactic:
exact Or.inl h

Premises used: Or.inl