awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
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 y : ℝ
hxy : x ≤ y
⊢ LE.le (α := ℝ)
    (⨆ (g' : G),
      (((f₂ : (a : G) → CircleDeg1Lift) g'⁻¹ : CircleDeg1Lift) : (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 : ℝ) → ℝ) y : ℝ))

Tactic:
exact ciSup_mono (this y) fun g => mono _ (mono _ hxy)

Premises used: CircleDeg1Lift.mono, Inv.inv, DFunLike.coe, ciSup_mono
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
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 : ℝ
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
⊢ ⨆ (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

Tactic:
simp only [map_add_one]

Premises used: CircleDeg1Lift.map_add_one
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
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 : ℝ
⊢ ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ id x + 1)
    (⨆ (g : G),
      (((f₂ : (a : G) → CircleDeg1Lift) g⁻¹ : CircleDeg1Lift) : (a : ℝ) → ℝ)
        ((((f₁ : (a : G) → CircleDeg1Lift) g : CircleDeg1Lift) : (a : ℝ) → ℝ) x : ℝ))

Tactic:
fun_prop
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
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),
      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:
exact (Monotone.map_ciSup_of_continuousAt (by fun_prop)
      (monotone_id.add_const (1 : ℝ)) (this x)).symm

Premises used: monotone_id, Monotone.add_const, Monotone.map_ciSup_of_continuousAt, OfNat.ofNat, Eq.symm
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
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 : ℝ
⊢ BddAbove (α := ℝ)
    (range fun (g : G) ↦
      (((f₂ : (a : G) → CircleDeg1Lift) g⁻¹ : CircleDeg1Lift) : (a : ℝ) → ℝ)
        ((((f₁ : (a : G) → CircleDeg1Lift) g : CircleDeg1Lift) : (a : ℝ) → ℝ) x : ℝ))

Tactic:
this x
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
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 : ℝ
⊢ BddAbove (α := ℝ)
    (range fun (g : G) ↦
      (((f₂ : (a : G) → CircleDeg1Lift) g⁻¹ : CircleDeg1Lift) : (a : ℝ) → ℝ)
        ((((f₁ : (a : G) → CircleDeg1Lift) g : CircleDeg1Lift) : (a : ℝ) → ℝ) x : ℝ))

Tactic:
exact this x
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f₁ f₂ : CircleDeg1Liftˣ
h : τ (↑f₁ : CircleDeg1Lift) = τ (↑f₂ : CircleDeg1Lift)
n : Multiplicative ℤ
⊢ τ
      ((MonoidHom.comp (Units.coeHom CircleDeg1Lift)
            ((zpowersHom CircleDeg1Liftˣ : (a : CircleDeg1Liftˣ) → Multiplicative ℤ →* CircleDeg1Liftˣ) f₁) :
          (a : Multiplicative ℤ) → CircleDeg1Lift)
        n) =
    τ
      ((MonoidHom.comp (Units.coeHom CircleDeg1Lift)
            ((zpowersHom CircleDeg1Liftˣ : (a : CircleDeg1Liftˣ) → Multiplicative ℤ →* CircleDeg1Liftˣ) f₂) :
          (a : Multiplicative ℤ) → CircleDeg1Lift)
        n)

Tactic:
simp [h]
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f₁ f₂ : CircleDeg1Liftˣ
h : τ (↑f₁ : CircleDeg1Lift) = τ (↑f₂ : CircleDeg1Lift)
this :
  ∀ (n : Multiplicative ℤ),
    τ
        ((MonoidHom.comp (Units.coeHom CircleDeg1Lift)
              ((zpowersHom CircleDeg1Liftˣ : (a : CircleDeg1Liftˣ) → Multiplicative ℤ →* CircleDeg1Liftˣ) f₁) :
            (a : Multiplicative ℤ) → CircleDeg1Lift)
          n) =
      τ
        ((MonoidHom.comp (Units.coeHom CircleDeg1Lift)
              ((zpowersHom CircleDeg1Liftˣ : (a : CircleDeg1Liftˣ) → Multiplicative ℤ →* CircleDeg1Liftˣ) f₂) :
            (a : Multiplicative ℤ) → CircleDeg1Lift)
          n)
F : CircleDeg1Lift
hF :
  ∀ (g : Multiplicative ℤ),
    Semiconj (α := ℝ) (β := ℝ) (⇑F : (a : ℝ) → ℝ)
      (⇑((MonoidHom.comp (Units.coeHom CircleDeg1Lift)
                  ((zpowersHom CircleDeg1Liftˣ : (a : CircleDeg1Liftˣ) → Multiplicative ℤ →* CircleDeg1Liftˣ) f₁) :
                (a : Multiplicative ℤ) → CircleDeg1Lift)
              g :
            CircleDeg1Lift) :
        (a : ℝ) → ℝ)
      (⇑((MonoidHom.comp (Units.coeHom CircleDeg1Lift)
                  ((zpowersHom CircleDeg1Liftˣ : (a : CircleDeg1Liftˣ) → Multiplicative ℤ →* CircleDeg1Liftˣ) f₂) :
                (a : Multiplicative ℤ) → CircleDeg1Lift)
              g :
            CircleDeg1Lift) :
        (a : ℝ) → ℝ)
⊢ Semiconj (α := ℝ) (β := ℝ) (⇑F : (a : ℝ) → ℝ) (⇑(↑f₁ : CircleDeg1Lift) : (a : ℝ) → ℝ)
    (⇑(↑f₂ : CircleDeg1Lift) : (a : ℝ) → ℝ)

Tactic:
simpa using hF (Multiplicative.ofAdd 1)

Premises used: Multiplicative.ofAdd, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f₁ f₂ : CircleDeg1Lift
h₁ : IsUnit f₁
h₂ : IsUnit f₂
h : τ f₁ = τ f₂
rcases :
  ∀ (f₁ f₂ : CircleDeg1Liftˣ) (h : τ (↑f₁ : CircleDeg1Lift) = τ (↑f₂ : CircleDeg1Lift)),
    ∃ (F : CircleDeg1Lift),
      Semiconj (α := ℝ) (β := ℝ) (⇑F : (a : ℝ) → ℝ) (⇑(↑f₁ : CircleDeg1Lift) : (a : ℝ) → ℝ)
        (⇑(↑f₂ : CircleDeg1Lift) : (a : ℝ) → ℝ)
⊢ ∃ (F : CircleDeg1Lift), Semiconj (α := ℝ) (β := ℝ) (⇑F : (a : ℝ) → ℝ) (⇑f₁ : (a : ℝ) → ℝ) (⇑f₂ : (a : ℝ) → ℝ)

Tactic:
rcases h₁, h₂ with ⟨⟨f₁, rfl⟩, ⟨f₂, rfl⟩⟩

Premises used: rfl
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f₁ f₂ : CircleDeg1Liftˣ
h : τ (↑f₁ : CircleDeg1Lift) = τ (↑f₂ : CircleDeg1Lift)
⊢ ∃ (F : CircleDeg1Lift),
    Semiconj (α := ℝ) (β := ℝ) (⇑F : (a : ℝ) → ℝ) (⇑(↑f₁ : CircleDeg1Lift) : (a : ℝ) → ℝ)
      (⇑(↑f₂ : CircleDeg1Lift) : (a : ℝ) → ℝ)

Tactic:
units_semiconj_of_translationNumber_eq h

Premises used: CircleDeg1Lift.units_semiconj_of_translationNumber_eq
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f₁ f₂ : CircleDeg1Liftˣ
h : τ (↑f₁ : CircleDeg1Lift) = τ (↑f₂ : CircleDeg1Lift)
⊢ ∃ (F : CircleDeg1Lift),
    Semiconj (α := ℝ) (β := ℝ) (⇑F : (a : ℝ) → ℝ) (⇑(↑f₁ : CircleDeg1Lift) : (a : ℝ) → ℝ)
      (⇑(↑f₂ : CircleDeg1Lift) : (a : ℝ) → ℝ)

Tactic:
exact units_semiconj_of_translationNumber_eq h

Premises used: CircleDeg1Lift.units_semiconj_of_translationNumber_eq
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f₁ f₂ : CircleDeg1Lift
h₁ : Bijective (α := ℝ) (β := ℝ) (⇑f₁ : (a : ℝ) → ℝ)
h₂ : Bijective (α := ℝ) (β := ℝ) (⇑f₂ : (a : ℝ) → ℝ)
h : τ f₁ = τ f₂
⊢ ∃ (F : CircleDeg1Lift), Semiconj (α := ℝ) (β := ℝ) (⇑F : (a : ℝ) → ℝ) (⇑f₁ : (a : ℝ) → ℝ) (⇑f₂ : (a : ℝ) → ℝ)

Tactic:
semiconj_of_isUnit_of_translationNumber_eq (isUnit_iff_bijective.2 h₁) (isUnit_iff_bijective.2 h₂)
    h

Premises used: Iff.mpr, CircleDeg1Lift.isUnit_iff_bijective, CircleDeg1Lift.semiconj_of_isUnit_of_translationNumber_eq
-- Module: Mathlib.Dynamics.Ergodic.Action.Basic
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
rcases : ∀ (t : Set α) (htm : MeasurableSet t) (hst : s =ᶠ[ae μ] t), EventuallyConst s (ae μ)
⊢ EventuallyConst s (ae μ)

Tactic:
rcases hm with ⟨t, htm, hst⟩
-- Module: Mathlib.Dynamics.Ergodic.Action.Basic
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 μ)

Tactic:
.congr ?_ hst.symm

Premises used: Filter.EventuallyConst.congr, Filter.EventuallyEq.symm
-- Module: Mathlib.Dynamics.Ergodic.Action.Basic
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
refine : EventuallyConst t (ae μ)
⊢ EventuallyConst s (ae μ)

Tactic:
refine .congr ?_ hst.symm
-- Module: Mathlib.Dynamics.Ergodic.Action.Basic
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 μ)

Tactic:
ErgodicSMul.aeconst_of_forall_preimage_smul_ae_eq htm fun g : G ↦ ?_

Premises used: ErgodicSMul.aeconst_of_forall_preimage_smul_ae_eq
-- Module: Mathlib.Dynamics.Ergodic.Action.Basic
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
refine : ∀ (g : G), (fun (x : α) ↦ g • x) ⁻¹' t =ᶠ[ae μ] t
⊢ EventuallyConst t (ae μ)

Tactic:
refine ErgodicSMul.aeconst_of_forall_preimage_smul_ae_eq htm fun g : G ↦ ?_

Premises used: ErgodicSMul.aeconst_of_forall_preimage_smul_ae_eq
-- Module: Mathlib.Dynamics.Ergodic.Action.Basic
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

Tactic:
.trans (.trans ?_ (h g)) hst

Premises used: Filter.EventuallyEq.trans
-- Module: Mathlib.Dynamics.Ergodic.Action.Basic
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
refine : (fun (x : α) ↦ g • x) ⁻¹' t =ᶠ[ae μ] (fun (x : α) ↦ g • x) ⁻¹' s
⊢ (fun (x : α) ↦ g • x) ⁻¹' t =ᶠ[ae μ] t

Tactic:
refine .trans (.trans ?_ (h g)) hst
-- Module: Mathlib.Dynamics.Ergodic.Action.Basic
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 μ] (fun (x : α) ↦ g • x) ⁻¹' s

Tactic:
tendsto_smul_ae _ _ hst.symm

Premises used: Set.Mem, Filter.Eventually, setOf, Filter.EventuallyEq, MeasureTheory.tendsto_smul_ae, Set.preimage, Filter.EventuallyEq.symm
-- Module: Mathlib.Dynamics.Ergodic.Action.Basic
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 μ] (fun (x : α) ↦ g • x) ⁻¹' s

Tactic:
exact tendsto_smul_ae _ _ hst.symm

Premises used: MeasureTheory.tendsto_smul_ae, Filter.EventuallyEq.symm
-- Module: Mathlib.Dynamics.Ergodic.Action.Basic
Goal:
G : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Group G
inst_1 : MulAction G α
inst_2 : ErgodicSMul G α μ
s : Set α
hm : NullMeasurableSet s μ
h : ∀ (g : G), g • s =ᶠ[ae μ] s
g : G
⊢ (fun (x : α) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s

Tactic:
simpa only [preimage_smul] using h g⁻¹

Premises used: Set.preimage_smul, Inv.inv
-- Module: Mathlib.Dynamics.Ergodic.Action.Basic
Goal:
G : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Group G
inst_1 : MulAction G α
inst_2 : ErgodicSMul G α μ
s : Set α
hm : NullMeasurableSet s μ
h : Eq (α := Subgroup G) (aestabilizer G μ s) ⊤
⊢ EventuallyConst s (ae μ)

Tactic:
aeconst_of_forall_smul_ae_eq G hm <| (Subgroup.eq_top_iff' _).1 h

Premises used: Subgroup.eq_top_iff', MeasureTheory.aeconst_of_forall_smul_ae_eq, Iff.mp
-- Module: Mathlib.Dynamics.Ergodic.Action.Basic
Goal:
G : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : Group G
inst_1 : MulAction G α
inst_2 : SMulInvariantMeasure G α μ
h : ∀ (s : Set α), MeasurableSet s → Eq (α := Subgroup G) (aestabilizer G μ s) ⊤ → EventuallyConst s (ae μ)
s : Set α
hm : MeasurableSet s
hs : ∀ (g : G), (fun (x : α) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s
g : G
⊢ Membership.mem (γ := Subgroup G) (aestabilizer G μ s) g

Tactic:
simpa only [preimage_smul_inv] using hs g⁻¹

Premises used: Set.preimage_smul_inv, Inv.inv
-- Module: Mathlib.Dynamics.Ergodic.Action.Basic
Goal:
α : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → α
hf : Measurable f
simp :
  (MeasurePreserving f μ μ ∧
      ∀ {s : Set α},
        MeasurableSet s →
          (∀ (g : IterateMulAct f), (fun (x : α) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s) → EventuallyConst s (ae μ)) ↔
    Ergodic f μ
⊢ ErgodicSMul (IterateMulAct f) α μ ↔ Ergodic f μ

Tactic:
simp only [ergodicSMul_iff, smulInvariantMeasure_iterateMulAct, hf]

Premises used: MeasureTheory.smulInvariantMeasure_iterateMulAct, ergodicSMul_iff
-- Module: Mathlib.Dynamics.Ergodic.Action.Basic
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 μ

Tactic:
⟨fun ⟨h₁, h₂⟩ ↦ ⟨h₁, ⟨?_⟩⟩, fun h ↦ ⟨h.1, ?_⟩⟩

Premises used: Ergodic, Ergodic.mk, Ergodic.toMeasurePreserving, PreErgodic.mk, And.intro, Iff.intro, _private.0.MeasureTheory.ergodicSMul_iterateMulAct.match_2
-- Module: Mathlib.Dynamics.Ergodic.Action.Basic
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 μ)
refine_2 :
  ∀ (h : Ergodic f μ) {s : Set α},
    MeasurableSet s → (∀ (g : IterateMulAct f), (fun (x : α) ↦ g • x) ⁻¹' s =ᶠ[ae μ] 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 μ

Tactic:
refine ⟨fun ⟨h₁, h₂⟩ ↦ ⟨h₁, ⟨?_⟩⟩, fun h ↦ ⟨h.1, ?_⟩⟩
-- Module: Mathlib.Dynamics.Ergodic.Action.Basic
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 μ)

Tactic:
h₂ hm fun n ↦ ?_
-- Module: Mathlib.Dynamics.Ergodic.Action.Basic
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
refine_1 : ∀ (n : IterateMulAct f), (fun (x : α) ↦ n • x) ⁻¹' s =ᶠ[ae μ] s
⊢ EventuallyConst s (ae μ)

Tactic:
refine h₂ hm fun n ↦ ?_
-- Module: Mathlib.Dynamics.Ergodic.Action.Basic
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
refine_1 : (fun (x : α) ↦ n • x) ⁻¹' s =ᶠ[ae μ] (fun (x : α) ↦ n • x) ⁻¹' s
⊢ (fun (x : α) ↦ n • x) ⁻¹' s =ᶠ[ae μ] s

Tactic:
nth_rewrite 2 [← Function.IsFixedPt.preimage_iterate hs n.val]

Premises used: Function.IsFixedPt.preimage_iterate, IterateMulAct.val
-- Module: Mathlib.Dynamics.Ergodic.Action.Basic
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 μ] (fun (x : α) ↦ n • x) ⁻¹' s

Tactic:
rfl
-- Module: Mathlib.Dynamics.Ergodic.Action.Basic
Goal:
α : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → α
hf : Measurable f
h : Ergodic f μ
s : Set α
hm : MeasurableSet s
hs : ∀ (g : IterateMulAct f), (fun (x : α) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s
⊢ EventuallyConst s (ae μ)

Tactic:
h.quasiErgodic.aeconst_set₀ hm.nullMeasurableSet <| hs (.mk 1)

Premises used: MeasurableSet.nullMeasurableSet, IterateMulAct.mk, QuasiErgodic.aeconst_set₀, Ergodic.quasiErgodic, OfNat.ofNat
-- Module: Mathlib.Dynamics.Ergodic.Action.Basic
Goal:
α : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → α
hf : Measurable f
h : Ergodic f μ
s : Set α
hm : MeasurableSet s
hs : ∀ (g : IterateMulAct f), (fun (x : α) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s
⊢ EventuallyConst s (ae μ)

Tactic:
exact h.quasiErgodic.aeconst_set₀ hm.nullMeasurableSet <| hs (.mk 1)

Premises used: MeasurableSet.nullMeasurableSet, IterateMulAct.mk, QuasiErgodic.aeconst_set₀, Ergodic.quasiErgodic, OfNat.ofNat
-- Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal
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}
⊢ let this := borel M;
  BorelSpace M

Tactic:
borelize M