awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
G : Type u_1
inst : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ ((f₁ : (a : G) → CircleDeg1Lift) g) = τ ((f₂ : (a : G) → CircleDeg1Lift) g)
this :
  ∀ (x : ℝ),
    BddAbove (α := ℝ)
      (range fun (g : G) ↦
        (((f₂ : (a : G) → CircleDeg1Lift) g⁻¹ : CircleDeg1Lift) : (a : ℝ) → ℝ)
          ((((f₁ : (a : G) → CircleDeg1Lift) g : CircleDeg1Lift) : (a : ℝ) → ℝ) x : ℝ))
F₁ : G →* ℝ ≃o ℝ := toOrderIso.comp f₁.toHomUnits
F₂ : G →* ℝ ≃o ℝ := toOrderIso.comp f₂.toHomUnits
hF₁ :
  ∀ (g : G),
    Eq (α := (a : ℝ) → ℝ) (⇑((F₁ : (a : G) → ℝ ≃o ℝ) g : ℝ ≃o ℝ) : (a : ℝ) → ℝ)
      (⇑((f₁ : (a : G) → CircleDeg1Lift) g : CircleDeg1Lift) : (a : ℝ) → ℝ)
hF₂ :
  ∀ (g : G),
    Eq (α := (a : ℝ) → ℝ) (⇑((F₂ : (a : G) → ℝ ≃o ℝ) g : ℝ ≃o ℝ) : (a : ℝ) → ℝ)
      (⇑((f₂ : (a : G) → CircleDeg1Lift) g : CircleDeg1Lift) : (a : ℝ) → ℝ)
x : ℝ
⊢ ⨆ (g' : G),
      (((f₂ : (a : G) → CircleDeg1Lift) g'⁻¹ : CircleDeg1Lift) : (a : ℝ) → ℝ)
        ((((f₁ : (a : G) → CircleDeg1Lift) g' : CircleDeg1Lift) : (a : ℝ) → ℝ) (x + 1) : ℝ) =
    HAdd.hAdd (α := ℝ)
      (⨆ (g' : G),
        (((f₂ : (a : G) → CircleDeg1Lift) g'⁻¹ : CircleDeg1Lift) : (a : ℝ) → ℝ)
          ((((f₁ : (a : G) → CircleDeg1Lift) g' : CircleDeg1Lift) : (a : ℝ) → ℝ) x : ℝ))
      1
have refine_2 : ⨆ (g' : G),
    HAdd.hAdd (α := ℝ) (β := ℝ)
      ((((f₂ : (a : G) → CircleDeg1Lift) g'⁻¹ : CircleDeg1Lift) : (a : ℝ) → ℝ)
          ((((f₁ : (a : G) → CircleDeg1Lift) g' : CircleDeg1Lift) : (a : ℝ) → ℝ) x : ℝ) :
        ℝ)
      (1 : ℝ) =
  HAdd.hAdd (α := ℝ)
    (⨆ (g' : G),
      (((f₂ : (a : G) → CircleDeg1Lift) g'⁻¹ : CircleDeg1Lift) : (a : ℝ) → ℝ)
        ((((f₁ : (a : G) → CircleDeg1Lift) g' : CircleDeg1Lift) : (a : ℝ) → ℝ) x : ℝ))
    1
Tactic: simp only [map_add_one]
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
f₁ f₂ : CircleDeg1Lift
h₁ : IsUnit f₁
h₂ : IsUnit f₂
h : τ f₁ = τ f₂
⊢ ∃ (F : CircleDeg1Lift), Semiconj (α := ℝ) (β := ℝ) (⇑F : (a : ℝ) → ℝ) (⇑f₁ : (a : ℝ) → ℝ) (⇑f₂ : (a : ℝ) → ℝ)
have rcases : ∀ (f₁ f₂ : CircleDeg1Liftˣ) (h : τ (↑f₁ : CircleDeg1Lift) = τ (↑f₂ : CircleDeg1Lift)),
  ∃ (F : CircleDeg1Lift),
    Semiconj (α := ℝ) (β := ℝ) (⇑F : (a : ℝ) → ℝ) (⇑(↑f₁ : CircleDeg1Lift) : (a : ℝ) → ℝ)
      (⇑(↑f₂ : CircleDeg1Lift) : (a : ℝ) → ℝ)
Tactic: rcases h₁, h₂ with ⟨⟨f₁, rfl⟩, ⟨f₂, rfl⟩⟩
Cleared hypotheses: f₁, f₂, h₁, h₂, h
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : SMul G α
inst_1 : ErgodicSMul G α μ
s : Set α
hm : NullMeasurableSet s μ
h : ∀ (g : G), (fun (x : α) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s
⊢ EventuallyConst s (ae μ)
have rcases : ∀ (t : Set α) (htm : MeasurableSet t) (hst : s =ᶠ[ae μ] t), EventuallyConst s (ae μ)
Tactic: rcases hm with ⟨t, htm, hst⟩
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : SMul G α
inst_1 : ErgodicSMul G α μ
s : Set α
h : ∀ (g : G), (fun (x : α) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s
t : Set α
htm : MeasurableSet t
hst : s =ᶠ[ae μ] t
⊢ EventuallyConst s (ae μ)
have refine : EventuallyConst t (ae μ)
Tactic: refine .congr ?_ hst.symm
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : SMul G α
inst_1 : ErgodicSMul G α μ
s : Set α
h : ∀ (g : G), (fun (x : α) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s
t : Set α
htm : MeasurableSet t
hst : s =ᶠ[ae μ] t
⊢ EventuallyConst t (ae μ)
have refine : ∀ (g : G), (fun (x : α) ↦ g • x) ⁻¹' t =ᶠ[ae μ] t
Tactic: refine ErgodicSMul.aeconst_of_forall_preimage_smul_ae_eq htm fun g : G ↦ ?_
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.Basic (goal)
Goal:
G : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : SMul G α
inst_1 : ErgodicSMul G α μ
s : Set α
h : ∀ (g : G), (fun (x : α) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s
t : Set α
htm : MeasurableSet t
hst : s =ᶠ[ae μ] t
g : G
⊢ (fun (x : α) ↦ g • x) ⁻¹' t =ᶠ[ae μ] t
have refine : (fun (x : α) ↦ g • x) ⁻¹' t =ᶠ[ae μ] (fun (x : α) ↦ g • x) ⁻¹' s
Tactic: refine .trans (.trans ?_ (h g)) hst
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.Basic (goal)
Goal:
α : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → α
hf : Measurable f
⊢ ErgodicSMul (IterateMulAct f) α μ ↔ Ergodic f μ
have simp : (MeasurePreserving f μ μ ∧
    ∀ {s : Set α},
      MeasurableSet s → (∀ (g : IterateMulAct f), (fun (x : α) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s) → EventuallyConst s (ae μ)) ↔
  Ergodic f μ
Tactic: simp only [ergodicSMul_iff, smulInvariantMeasure_iterateMulAct, hf]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.Basic (goal)
Goal:
α : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → α
hf : Measurable f
⊢ (MeasurePreserving f μ μ ∧
      ∀ {s : Set α},
        MeasurableSet s →
          (∀ (g : IterateMulAct f), (fun (x : α) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s) → EventuallyConst s (ae μ)) ↔
    Ergodic f μ
have refine_1 : (MeasurePreserving f μ μ ∧
    ∀ {s : Set α},
      MeasurableSet s → (∀ (g : IterateMulAct f), (fun (x : α) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s) → EventuallyConst s (ae μ)) →
  ∀ (h₁ : MeasurePreserving f μ μ)
    (h₂ :
      ∀ {s : Set α},
        MeasurableSet s → (∀ (g : IterateMulAct f), (fun (x : α) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s) → EventuallyConst s (ae μ))
    ⦃s : Set α⦄, MeasurableSet s → f ⁻¹' s = s → EventuallyConst s (ae μ)
Tactic: refine ⟨fun ⟨h₁, h₂⟩ ↦ ⟨h₁, ⟨?_⟩⟩, fun h ↦ ⟨h.1, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.Basic (goal)
Goal:
α : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → α
hf : Measurable f
refine_1 :
  (MeasurePreserving f μ μ ∧
      ∀ {s : Set α},
        MeasurableSet s →
          (∀ (g : IterateMulAct f), (fun (x : α) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s) → EventuallyConst s (ae μ)) →
    ∀ (h₁ : MeasurePreserving f μ μ)
      (h₂ :
        ∀ {s : Set α},
          MeasurableSet s →
            (∀ (g : IterateMulAct f), (fun (x : α) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s) → EventuallyConst s (ae μ))
      ⦃s : Set α⦄, MeasurableSet s → f ⁻¹' s = s → EventuallyConst s (ae μ)
⊢ (MeasurePreserving f μ μ ∧
      ∀ {s : Set α},
        MeasurableSet s →
          (∀ (g : IterateMulAct f), (fun (x : α) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s) → EventuallyConst s (ae μ)) ↔
    Ergodic f μ
have refine_2 : ∀ (h : Ergodic f μ) {s : Set α},
  MeasurableSet s → (∀ (g : IterateMulAct f), (fun (x : α) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s) → EventuallyConst s (ae μ)
Tactic: refine ⟨fun ⟨h₁, h₂⟩ ↦ ⟨h₁, ⟨?_⟩⟩, fun h ↦ ⟨h.1, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.Basic (goal)
Goal:
α : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → α
hf : Measurable f
h :
  MeasurePreserving f μ μ ∧
    ∀ {s : Set α},
      MeasurableSet s → (∀ (g : IterateMulAct f), (fun (x : α) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s) → EventuallyConst s (ae μ)
h₁ : MeasurePreserving f μ μ
h₂ :
  ∀ {s : Set α},
    MeasurableSet s → (∀ (g : IterateMulAct f), (fun (x : α) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s) → EventuallyConst s (ae μ)
s : Set α
hm : MeasurableSet s
hs : f ⁻¹' s = s
⊢ EventuallyConst s (ae μ)
have refine_1 : ∀ (n : IterateMulAct f), (fun (x : α) ↦ n • x) ⁻¹' s =ᶠ[ae μ] s
Tactic: refine h₂ hm fun n ↦ ?_
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.Basic (goal)
Goal:
α : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → α
hf : Measurable f
h :
  MeasurePreserving f μ μ ∧
    ∀ {s : Set α},
      MeasurableSet s → (∀ (g : IterateMulAct f), (fun (x : α) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s) → EventuallyConst s (ae μ)
h₁ : MeasurePreserving f μ μ
h₂ :
  ∀ {s : Set α},
    MeasurableSet s → (∀ (g : IterateMulAct f), (fun (x : α) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s) → EventuallyConst s (ae μ)
s : Set α
hm : MeasurableSet s
hs : f ⁻¹' s = s
n : IterateMulAct f
⊢ (fun (x : α) ↦ n • x) ⁻¹' s =ᶠ[ae μ] s
have refine_1 : (fun (x : α) ↦ n • x) ⁻¹' s =ᶠ[ae μ] (fun (x : α) ↦ n • x) ⁻¹' s
Tactic: nth_rewrite 2 [← Function.IsFixedPt.preimage_iterate hs n.val]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.OfMinimal (hypothesis)
Goal:
M : Type u_1
inst : TopologicalSpace M
X : Type u_2
inst_1 : TopologicalSpace X
inst_2 : R1Space X
inst_3 : MeasurableSpace X
inst_4 : BorelSpace X
inst_5 : SMul M X
inst_6 : ContinuousSMul M X
μ : Measure X
inst_7 : IsFiniteMeasure μ
inst_8 : μ.InnerRegular
inst_9 : ErgodicSMul M X μ
s : Set X
hsm : NullMeasurableSet s μ
hd : Dense.{u_1} (X := M) {g : M | (fun (x : X) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s}
⊢ EventuallyConst s (ae μ)
have this : let this := borel M;
BorelSpace M
Tactic: borelize M
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.OfMinimal (goal)
Goal:
M : Type u_1
inst : TopologicalSpace M
X : Type u_2
inst_1 : TopologicalSpace X
inst_2 : R1Space X
inst_3 : MeasurableSpace X
inst_4 : BorelSpace X
inst_5 : SMul M X
inst_6 : ContinuousSMul M X
μ : Measure X
inst_7 : IsFiniteMeasure μ
inst_8 : μ.InnerRegular
inst_9 : ErgodicSMul M X μ
s : Set X
hsm : NullMeasurableSet s μ
hd : Dense.{u_1} (X := M) {g : M | (fun (x : X) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s}
this : MeasurableSpace M := borel M
this_1 : BorelSpace M
⊢ EventuallyConst s (ae μ)
have refine : ∀ (g : M), (fun (x : X) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s
Tactic: refine aeconst_of_forall_preimage_smul_ae_eq M hsm ?_
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.OfMinimal (goal)
Goal:
M : Type u_1
inst : TopologicalSpace M
X : Type u_2
inst_1 : TopologicalSpace X
inst_2 : R1Space X
inst_3 : MeasurableSpace X
inst_4 : BorelSpace X
inst_5 : SMul M X
inst_6 : ContinuousSMul M X
μ : Measure X
inst_7 : IsFiniteMeasure μ
inst_8 : μ.InnerRegular
inst_9 : ErgodicSMul M X μ
s : Set X
hsm : NullMeasurableSet s μ
hd : Dense.{u_1} (X := M) {g : M | (fun (x : X) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s}
this : MeasurableSpace M := borel M
this_1 : BorelSpace M
⊢ ∀ (g : M), (fun (x : X) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s
have rwa : ∀ (hd : Eq.{u_1 + 1} (α := Set M) (closure[inst] {g : M | (fun (x : X) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s}) univ),
  let this := borel M;
  BorelSpace M → IsClosed[inst] {g : M | (fun (x : X) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s}
Tactic: rwa [dense_iff_closure_eq, IsClosed.closure_eq, eq_univ_iff_forall] at hd
Cleared hypotheses: hd, this, this_1
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.OfMinimal (hypothesis)
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : R1Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
M : Type u_3
inst_4 : Monoid M
inst_5 : TopologicalSpace M
inst_6 : MulAction M X
inst_7 : ContinuousSMul M X
g : M
hg : DenseRange.{u_3, 0} (X := M) fun (x : ℕ) ↦ g ^ x
μ : Measure X
inst_8 : IsFiniteMeasure μ
inst_9 : μ.InnerRegular
inst_10 : ErgodicSMul M X μ
⊢ Ergodic (fun (x : X) ↦ g • x) μ
have this : let this := borel M;
BorelSpace M
Tactic: borelize M
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.OfMinimal (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : R1Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
M : Type u_3
inst_4 : Monoid M
inst_5 : TopologicalSpace M
inst_6 : MulAction M X
inst_7 : ContinuousSMul M X
g : M
hg : DenseRange.{u_3, 0} (X := M) fun (x : ℕ) ↦ g ^ x
μ : Measure X
inst_8 : IsFiniteMeasure μ
inst_9 : μ.InnerRegular
inst_10 : ErgodicSMul M X μ
this : MeasurableSpace M := borel M
this_1 : BorelSpace M
⊢ Ergodic (fun (x : X) ↦ g • x) μ
have refine : ∀ (s : Set X) (hsm : MeasurableSet s) (hs : (fun (x : X) ↦ g • x) ⁻¹' s = s), EventuallyConst s (ae μ)
Tactic: refine ⟨measurePreserving_smul _ _, ⟨fun s hsm hs ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.OfMinimal (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : R1Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
M : Type u_3
inst_4 : Monoid M
inst_5 : TopologicalSpace M
inst_6 : MulAction M X
inst_7 : ContinuousSMul M X
g : M
hg : DenseRange.{u_3, 0} (X := M) fun (x : ℕ) ↦ g ^ x
μ : Measure X
inst_8 : IsFiniteMeasure μ
inst_9 : μ.InnerRegular
inst_10 : ErgodicSMul M X μ
this : MeasurableSpace M := borel M
this_1 : BorelSpace M
s : Set X
hsm : MeasurableSet s
hs : (fun (x : X) ↦ g • x) ⁻¹' s = s
⊢ EventuallyConst s (ae μ)
have refine : Subset.{u_3} (α := Set M) (range fun (x : ℕ) ↦ g ^ x) {g : M | (fun (x : X) ↦ g • x) ⁻¹' s = s}
Tactic: refine aeconst_of_dense_setOf_preimage_smul_eq hsm.nullMeasurableSet (hg.mono ?_)
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.OfMinimal (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : R1Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
M : Type u_3
inst_4 : Monoid M
inst_5 : TopologicalSpace M
inst_6 : MulAction M X
inst_7 : ContinuousSMul M X
g : M
hg : DenseRange.{u_3, 0} (X := M) fun (x : ℕ) ↦ g ^ x
μ : Measure X
inst_8 : IsFiniteMeasure μ
inst_9 : μ.InnerRegular
inst_10 : ErgodicSMul M X μ
this : MeasurableSpace M := borel M
this_1 : BorelSpace M
s : Set X
hsm : MeasurableSet s
hs : (fun (x : X) ↦ g • x) ⁻¹' s = s
⊢ Subset.{u_3} (α := Set M) (range fun (x : ℕ) ↦ g ^ x) {g : M | (fun (x : X) ↦ g • x) ⁻¹' s = s}
have refine : ∀ (n : ℕ), Membership.mem (γ := Set M) {g : M | (fun (x : X) ↦ g • x) ⁻¹' s = s} (g ^ n)
Tactic: refine range_subset_iff.2 fun n ↦ ?_
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.OfMinimal (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : R1Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
M : Type u_3
inst_4 : Monoid M
inst_5 : TopologicalSpace M
inst_6 : MulAction M X
inst_7 : ContinuousSMul M X
g : M
hg : DenseRange.{u_3, 0} (X := M) fun (x : ℕ) ↦ g ^ x
μ : Measure X
inst_8 : IsFiniteMeasure μ
inst_9 : μ.InnerRegular
inst_10 : ErgodicSMul M X μ
this : MeasurableSpace M := borel M
this_1 : BorelSpace M
s : Set X
hsm : MeasurableSet s
hs : (fun (x : X) ↦ g • x) ⁻¹' s = s
n : ℕ
⊢ Membership.mem (γ := Set M) {g : M | (fun (x : X) ↦ g • x) ⁻¹' s = s} (g ^ n)
have rw : (fun (x : X) ↦ g ^ n • x) ⁻¹' s = s
Tactic: rw [mem_setOf, ← smul_iterate, preimage_iterate_eq, iterate_fixed hs]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.OfMinimal (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : R1Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
M : Type u_3
inst_4 : Monoid M
inst_5 : TopologicalSpace M
inst_6 : MulAction M X
inst_7 : ContinuousSMul M X
g : M
hg : DenseRange.{u_3, 0} (X := M) fun (x : ℕ) ↦ g ^ x
μ : Measure X
inst_8 : IsFiniteMeasure μ
inst_9 : μ.InnerRegular
inst_10 : ErgodicSMul M X μ
this : MeasurableSpace M := borel M
this_1 : BorelSpace M
s : Set X
hsm : MeasurableSet s
hs : (fun (x : X) ↦ g • x) ⁻¹' s = s
n : ℕ
rw : (fun (x : X) ↦ g ^ n • x) ⁻¹' s = s
⊢ Membership.mem (γ := Set M) {g : M | (fun (x : X) ↦ g • x) ⁻¹' s = s} (g ^ n)
have rw₁ : (fun (x : X) ↦ g • x)^[n] ⁻¹' s = s
Tactic: rw [mem_setOf, ← smul_iterate, preimage_iterate_eq, iterate_fixed hs]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.OfMinimal (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : R1Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
M : Type u_3
inst_4 : Monoid M
inst_5 : TopologicalSpace M
inst_6 : MulAction M X
inst_7 : ContinuousSMul M X
g : M
hg : DenseRange.{u_3, 0} (X := M) fun (x : ℕ) ↦ g ^ x
μ : Measure X
inst_8 : IsFiniteMeasure μ
inst_9 : μ.InnerRegular
inst_10 : ErgodicSMul M X μ
this : MeasurableSpace M := borel M
this_1 : BorelSpace M
s : Set X
hsm : MeasurableSet s
hs : (fun (x : X) ↦ g • x) ⁻¹' s = s
n : ℕ
rw : (fun (x : X) ↦ g ^ n • x) ⁻¹' s = s
rw₁ : (fun (x : X) ↦ g • x)^[n] ⁻¹' s = s
⊢ Membership.mem (γ := Set M) {g : M | (fun (x : X) ↦ g • x) ⁻¹' s = s} (g ^ n)
have rw₂ : (preimage fun (x : X) ↦ g • x)^[n] s = s
Tactic: rw [mem_setOf, ← smul_iterate, preimage_iterate_eq, iterate_fixed hs]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.OfMinimal (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : R1Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
M : Type u_3
inst_4 : Monoid M
inst_5 : TopologicalSpace M
inst_6 : MulAction M X
inst_7 : ContinuousSMul M X
g : M
hg : DenseRange.{u_3, 0} (X := M) fun (x : ℕ) ↦ g ^ x
μ : Measure X
inst_8 : IsFiniteMeasure μ
inst_9 : μ.InnerRegular
inst_10 : ErgodicSMul M X μ
this : MeasurableSpace M := borel M
this_1 : BorelSpace M
s : Set X
hsm : MeasurableSet s
hs : (fun (x : X) ↦ g • x) ⁻¹' s = s
n : ℕ
rw : (fun (x : X) ↦ g ^ n • x) ⁻¹' s = s
rw₁ : (fun (x : X) ↦ g • x)^[n] ⁻¹' s = s
rw₂ : (preimage fun (x : X) ↦ g • x)^[n] s = s
⊢ Membership.mem (γ := Set M) {g : M | (fun (x : X) ↦ g • x) ⁻¹' s = s} (g ^ n)
have rw₃ : s = s
Tactic: rw [mem_setOf, ← smul_iterate, preimage_iterate_eq, iterate_fixed hs]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.OfMinimal (goal)
Goal:
M : Type u_1
X : Type u_2
inst : Monoid M
inst_1 : SMul M X
inst_2 : TopologicalSpace X
inst_3 : R1Space X
inst_4 : MeasurableSpace X
inst_5 : BorelSpace X
μ : Measure X
inst_6 : IsFiniteMeasure μ
inst_7 : μ.InnerRegular
N : Type u_3
inst_8 : MulAction M N
inst_9 : Monoid N
inst_10 : TopologicalSpace N
inst_11 : MulAction.IsMinimal M N
inst_12 : MulAction N X
inst_13 : IsScalarTower M N X
inst_14 : ContinuousSMul N X
inst_15 : ErgodicSMul N X μ
s : Set X
hsm : MeasurableSet s
hs : ∀ (g : M), (fun (x : X) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s
⊢ EventuallyConst s (ae μ)
have refine : Dense.{u_3} (X := N) {g : N | (fun (x : X) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s}
Tactic: refine aeconst_of_dense_setOf_preimage_smul_ae (M := N) hsm.nullMeasurableSet ?_
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.OfMinimal (goal)
Goal:
M : Type u_1
X : Type u_2
inst : Monoid M
inst_1 : SMul M X
inst_2 : TopologicalSpace X
inst_3 : R1Space X
inst_4 : MeasurableSpace X
inst_5 : BorelSpace X
μ : Measure X
inst_6 : IsFiniteMeasure μ
inst_7 : μ.InnerRegular
N : Type u_3
inst_8 : MulAction M N
inst_9 : Monoid N
inst_10 : TopologicalSpace N
inst_11 : MulAction.IsMinimal M N
inst_12 : MulAction N X
inst_13 : IsScalarTower M N X
inst_14 : ContinuousSMul N X
inst_15 : ErgodicSMul N X μ
s : Set X
hsm : MeasurableSet s
hs : ∀ (g : M), (fun (x : X) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s
⊢ Dense.{u_3} (X := N) {g : N | (fun (x : X) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s}
have refine : Subset.{u_3} (α := Set N) (MulAction.orbit M 1) {g : N | (fun (x : X) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s}
Tactic: refine (MulAction.dense_orbit M 1).mono ?_
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.OfMinimal (hypothesis)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : ContinuousInv G
X : Type u_2
inst_3 : TopologicalSpace X
inst_4 : R1Space X
inst_5 : MeasurableSpace X
inst_6 : BorelSpace X
inst_7 : MulAction G X
inst_8 : ContinuousSMul G X
g : G
hg : DenseRange.{u_1, 0} (X := G) fun (x : ℤ) ↦ g ^ x
μ : Measure X
inst_9 : IsFiniteMeasure μ
inst_10 : μ.InnerRegular
inst_11 : ErgodicSMul G X μ
⊢ Ergodic (fun (x : X) ↦ g • x) μ
have this : let this := borel G;
BorelSpace G
Tactic: borelize G
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.OfMinimal (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : ContinuousInv G
X : Type u_2
inst_3 : TopologicalSpace X
inst_4 : R1Space X
inst_5 : MeasurableSpace X
inst_6 : BorelSpace X
inst_7 : MulAction G X
inst_8 : ContinuousSMul G X
g : G
hg : DenseRange.{u_1, 0} (X := G) fun (x : ℤ) ↦ g ^ x
μ : Measure X
inst_9 : IsFiniteMeasure μ
inst_10 : μ.InnerRegular
inst_11 : ErgodicSMul G X μ
this : MeasurableSpace G := borel G
this_1 : BorelSpace G
⊢ Ergodic (fun (x : X) ↦ g • x) μ
have refine : ∀ (s : Set X) (hsm : MeasurableSet s) (hs : (fun (x : X) ↦ g • x) ⁻¹' s = s), EventuallyConst s (ae μ)
Tactic: refine ⟨measurePreserving_smul _ _, ⟨fun s hsm hs ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.OfMinimal (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : ContinuousInv G
X : Type u_2
inst_3 : TopologicalSpace X
inst_4 : R1Space X
inst_5 : MeasurableSpace X
inst_6 : BorelSpace X
inst_7 : MulAction G X
inst_8 : ContinuousSMul G X
g : G
hg : DenseRange.{u_1, 0} (X := G) fun (x : ℤ) ↦ g ^ x
μ : Measure X
inst_9 : IsFiniteMeasure μ
inst_10 : μ.InnerRegular
inst_11 : ErgodicSMul G X μ
this : MeasurableSpace G := borel G
this_1 : BorelSpace G
s : Set X
hsm : MeasurableSet s
hs : (fun (x : X) ↦ g • x) ⁻¹' s = s
⊢ EventuallyConst s (ae μ)
have refine : (range fun (x : ℤ) ↦ g ^ x) ⊆ (↑(MulAction.aestabilizer G μ s) : Set G)
Tactic: refine aeconst_of_dense_aestabilizer_smul hsm.nullMeasurableSet (hg.mono ?_)
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.OfMinimal (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : ContinuousInv G
X : Type u_2
inst_3 : TopologicalSpace X
inst_4 : R1Space X
inst_5 : MeasurableSpace X
inst_6 : BorelSpace X
inst_7 : MulAction G X
inst_8 : ContinuousSMul G X
g : G
hg : DenseRange.{u_1, 0} (X := G) fun (x : ℤ) ↦ g ^ x
μ : Measure X
inst_9 : IsFiniteMeasure μ
inst_10 : μ.InnerRegular
inst_11 : ErgodicSMul G X μ
this : MeasurableSpace G := borel G
this_1 : BorelSpace G
s : Set X
hsm : MeasurableSet s
hs : (fun (x : X) ↦ g • x) ⁻¹' s = s
⊢ (range fun (x : ℤ) ↦ g ^ x) ⊆ (↑(MulAction.aestabilizer G μ s) : Set G)
have rw : (↑(Subgroup.zpowers g) : Set G) ⊆ (↑(MulAction.aestabilizer G μ s) : Set G)
Tactic: rw [← Subgroup.coe_zpowers, SetLike.coe_subset_coe, ← Subgroup.zpowers_inv, Subgroup.zpowers_le,
    MulAction.mem_aestabilizer, ← preimage_smul, hs]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.OfMinimal (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : ContinuousInv G
X : Type u_2
inst_3 : TopologicalSpace X
inst_4 : R1Space X
inst_5 : MeasurableSpace X
inst_6 : BorelSpace X
inst_7 : MulAction G X
inst_8 : ContinuousSMul G X
g : G
hg : DenseRange.{u_1, 0} (X := G) fun (x : ℤ) ↦ g ^ x
μ : Measure X
inst_9 : IsFiniteMeasure μ
inst_10 : μ.InnerRegular
inst_11 : ErgodicSMul G X μ
this : MeasurableSpace G := borel G
this_1 : BorelSpace G
s : Set X
hsm : MeasurableSet s
hs : (fun (x : X) ↦ g • x) ⁻¹' s = s
rw : (↑(Subgroup.zpowers g) : Set G) ⊆ (↑(MulAction.aestabilizer G μ s) : Set G)
⊢ (range fun (x : ℤ) ↦ g ^ x) ⊆ (↑(MulAction.aestabilizer G μ s) : Set G)
have rw₁ : LE.le (α := Subgroup G) (Subgroup.zpowers g) (MulAction.aestabilizer G μ s)
Tactic: rw [← Subgroup.coe_zpowers, SetLike.coe_subset_coe, ← Subgroup.zpowers_inv, Subgroup.zpowers_le,
    MulAction.mem_aestabilizer, ← preimage_smul, hs]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.OfMinimal (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : ContinuousInv G
X : Type u_2
inst_3 : TopologicalSpace X
inst_4 : R1Space X
inst_5 : MeasurableSpace X
inst_6 : BorelSpace X
inst_7 : MulAction G X
inst_8 : ContinuousSMul G X
g : G
hg : DenseRange.{u_1, 0} (X := G) fun (x : ℤ) ↦ g ^ x
μ : Measure X
inst_9 : IsFiniteMeasure μ
inst_10 : μ.InnerRegular
inst_11 : ErgodicSMul G X μ
this : MeasurableSpace G := borel G
this_1 : BorelSpace G
s : Set X
hsm : MeasurableSet s
hs : (fun (x : X) ↦ g • x) ⁻¹' s = s
rw : (↑(Subgroup.zpowers g) : Set G) ⊆ (↑(MulAction.aestabilizer G μ s) : Set G)
rw₁ : LE.le (α := Subgroup G) (Subgroup.zpowers g) (MulAction.aestabilizer G μ s)
⊢ (range fun (x : ℤ) ↦ g ^ x) ⊆ (↑(MulAction.aestabilizer G μ s) : Set G)
have rw₂ : LE.le (α := Subgroup G) (Subgroup.zpowers g⁻¹) (MulAction.aestabilizer G μ s)
Tactic: rw [← Subgroup.coe_zpowers, SetLike.coe_subset_coe, ← Subgroup.zpowers_inv, Subgroup.zpowers_le,
    MulAction.mem_aestabilizer, ← preimage_smul, hs]