mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Dynamics.Ergodic.Ergodic

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
s : Set α
f : α → α
μ : Measure α
inst✝ : IsProbabilityMeasure μ
hf : PreErgodic f μ
hs : MeasurableSet s
hs' : f ⁻¹' s = s
⊢ μ s = 0 ∨ μ s = 1

Tactic:
simpa using

Goal state after:
α : Type u_1
m : MeasurableSpace α
s : Set α
f : α → α
μ : Measure α
inst✝ : IsProbabilityMeasure μ
hf : PreErgodic f μ
hs : MeasurableSet s
hs' : f ⁻¹' s = s
⊢ μ s = 0 ∨ μ s = 1
Module: Mathlib.Dynamics.Ergodic.Action.Regular

Goal state before:
pp: G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulLeftInvariant
s : Set G
hsm : MeasurableSet s
hs : ∀ (g : G), (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] 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 using

Goal state after:
G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulLeftInvariant
s : Set G
hsm : MeasurableSet s
hs : ∀ (g : G), (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s
hμs : ∃ᵐ (x : G) ∂μ, x ∈ s
a : G
has : a ∈ s
ha : ∀ᵐ (b : G) ∂μ, b * a ∈ s ↔ a ∈ s
⊢ s ∈ ae μ
Module: Mathlib.Dynamics.Ergodic.Action.Regular

Goal state before:
pp: G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulRightInvariant
s : Set G
hsm : MeasurableSet s
hs : ∀ (g : Gᵐᵒᵖ), (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] 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 using

Goal state after:
G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulRightInvariant
s : Set G
hsm : MeasurableSet s
hs : ∀ (g : Gᵐᵒᵖ), (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s
hμs : ∃ᵐ (x : G) ∂μ, x ∈ s
a : G
has : a ∈ s
ha : ∀ᵐ (b : G) ∂μ, a * b ∈ s ↔ a ∈ s
⊢ s ∈ ae μ
Module: Mathlib.Dynamics.Ergodic.Action.Basic

Goal state before:
pp: G : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : ErgodicSMul G α μ
s : Set α
hm : NullMeasurableSet s μ
h : ∀ (g : G), g • s =ᵐ[μ] s
g : G
⊢ (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s

Tactic:
simpa using

Goal state after:
G : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : ErgodicSMul G α μ
s : Set α
hm : NullMeasurableSet s μ
h : ∀ (g : G), g • s =ᵐ[μ] s
g : G
⊢ g⁻¹ • s =ᵐ[μ] s
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f✝ g : CircleDeg1Lift
f : CircleDeg1Liftˣ
a✝ b✝ : ℝ
h :
  { toFun := ⇑↑f, invFun := ⇑↑f⁻¹, left_inv := ⋯, right_inv := ⋯ } a✝ ≤
    { toFun := ⇑↑f, invFun := ⇑↑f⁻¹, left_inv := ⋯, right_inv := ⋯ } b✝
⊢ a✝ ≤ b✝

Tactic:
simpa using

Goal state after:
f✝ g : CircleDeg1Lift
f : CircleDeg1Liftˣ
a✝ b✝ : ℝ
h :
  { toFun := ⇑↑f, invFun := ⇑↑f⁻¹, left_inv := ⋯, right_inv := ⋯ } a✝ ≤
    { toFun := ⇑↑f, invFun := ⇑↑f⁻¹, left_inv := ⋯, right_inv := ⋯ } b✝
⊢ a✝ ≤ b✝
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f : CircleDeg1Lift
n : ℕ
⊢ Function.Commute ⇑f fun x ↦ ↑n + x

Tactic:
simpa using

Goal state after:
f : CircleDeg1Lift
n : ℕ
⊢ Function.Commute ⇑f fun x ↦ ↑n + x
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f : CircleDeg1Lift
n : ℕ
⊢ Function.Commute ⇑f fun x ↦ x + ↑-[n+1]

Tactic:
simpa using

Goal state after:
f : CircleDeg1Lift
n : ℕ
⊢ Function.Commute ⇑f fun x ↦ x + (-1 + -↑n)
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f : CircleDeg1Lift
n : ℤ
⊢ Function.Commute ⇑f fun x ↦ ↑n + x

Tactic:
simpa using

Goal state after:
f : CircleDeg1Lift
n : ℤ
⊢ Function.Commute ⇑f fun x ↦ ↑n + x
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f : CircleDeg1Lift
⊢ Tendsto (fun x ↦ x - 1) atTop atTop

Tactic:
simpa using

Goal state after:
f : CircleDeg1Lift
⊢ Tendsto (fun x ↦ x + -1) atTop atTop
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f : CircleDeg1Lift
x : ℝ
m : ℤ
h : f x ≤ x + ↑m
n : ℕ
⊢ (⇑f)^[n] x ≤ x + ↑n * ↑m

Tactic:
simpa using

Goal state after:
f : CircleDeg1Lift
x : ℝ
m : ℤ
h : f x ≤ x + ↑m
n : ℕ
⊢ (⇑f)^[n] x ≤ x + ↑n * ↑m
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f : CircleDeg1Lift
x : ℝ
m : ℤ
h : x + ↑m ≤ f x
n : ℕ
⊢ x + ↑n * ↑m ≤ (⇑f)^[n] x

Tactic:
simpa using

Goal state after:
f : CircleDeg1Lift
x : ℝ
m : ℤ
h : x + ↑m ≤ f x
n : ℕ
⊢ x + ↑n * ↑m ≤ (⇑f)^[n] x
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f : CircleDeg1Lift
x : ℝ
m : ℤ
h : f x = x + ↑m
n : ℕ
⊢ (⇑f)^[n] x = x + ↑n * ↑m

Tactic:
simpa using

Goal state after:
f : CircleDeg1Lift
x : ℝ
m : ℤ
h : f x = x + ↑m
n : ℕ
⊢ (⇑f)^[n] x = x + ↑n * ↑m
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f : CircleDeg1Lift
x : ℝ
m : ℤ
n : ℕ
hn : 0 < n
⊢ (⇑f)^[n] x ≤ x + ↑n * ↑m ↔ f x ≤ x + ↑m

Tactic:
simpa using

Goal state after:
f : CircleDeg1Lift
x : ℝ
m : ℤ
n : ℕ
hn : 0 < n
⊢ (⇑f)^[n] x ≤ x + ↑n * ↑m ↔ f x ≤ x + ↑m
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f : CircleDeg1Lift
x : ℝ
m : ℤ
n : ℕ
hn : 0 < n
⊢ (⇑f)^[n] x < x + ↑n * ↑m ↔ f x < x + ↑m

Tactic:
simpa using

Goal state after:
f : CircleDeg1Lift
x : ℝ
m : ℤ
n : ℕ
hn : 0 < n
⊢ (⇑f)^[n] x < x + ↑n * ↑m ↔ f x < x + ↑m
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f : CircleDeg1Lift
x : ℝ
m : ℤ
n : ℕ
hn : 0 < n
⊢ (⇑f)^[n] x = x + ↑n * ↑m ↔ f x = x + ↑m

Tactic:
simpa using

Goal state after:
f : CircleDeg1Lift
x : ℝ
m : ℤ
n : ℕ
hn : 0 < n
⊢ (⇑f)^[n] x = x + ↑n * ↑m ↔ f x = x + ↑m
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f : CircleDeg1Lift
x : ℝ
m : ℤ
n : ℕ
hn : 0 < n
⊢ x + ↑n * ↑m ≤ (⇑f)^[n] x ↔ x + ↑m ≤ f x

Tactic:
simpa using

Goal state after:
f : CircleDeg1Lift
x : ℝ
m : ℤ
n : ℕ
hn : 0 < n
⊢ x + ↑n * ↑m ≤ (⇑f)^[n] x ↔ x + ↑m ≤ f x
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f : CircleDeg1Lift
x : ℝ
m : ℤ
n : ℕ
hn : 0 < n
⊢ x + ↑n * ↑m < (⇑f)^[n] x ↔ x + ↑m < f x

Tactic:
simpa using

Goal state after:
f : CircleDeg1Lift
x : ℝ
m : ℤ
n : ℕ
hn : 0 < n
⊢ x + ↑n * ↑m < (⇑f)^[n] x ↔ x + ↑m < f x
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f : CircleDeg1Lift
τ' : ℝ
h : Tendsto (fun n ↦ (⇑f)^[n] 0 / ↑n) atTop (𝓝 τ')
⊢ Tendsto f.transnumAuxSeq atTop (𝓝 τ')

Tactic:
simpa using

Goal state after:
f : CircleDeg1Lift
τ' : ℝ
h : Tendsto (fun n ↦ (⇑f)^[n] 0 / ↑n) atTop (𝓝 τ')
⊢ Tendsto (fun n ↦ (⇑f)^[2 ^ n] 0 / 2 ^ n) atTop (𝓝 τ')
Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal

Goal state before:
pp: M : Type u_1
X : Type u_2
inst✝¹⁵ : Monoid M
inst✝¹⁴ : SMul M X
inst✝¹³ : TopologicalSpace X
inst✝¹² : R1Space X
inst✝¹¹ : MeasurableSpace X
inst✝¹⁰ : BorelSpace X
μ : Measure X
inst✝⁹ : IsFiniteMeasure μ
inst✝⁸ : μ.InnerRegular
N : Type u_3
inst✝⁷ : MulAction M N
inst✝⁶ : Monoid N
inst✝⁵ : TopologicalSpace N
inst✝⁴ : MulAction.IsMinimal M N
inst✝³ : MulAction N X
inst✝² : IsScalarTower M N X
inst✝¹ : ContinuousSMul N X
inst✝ : ErgodicSMul N X μ
c : M
s : Set X
hsm : MeasurableSet s
⊢ μ ((fun x ↦ c • x) ⁻¹' s) = μ s

Tactic:
simpa using

Goal state after:
M : Type u_1
X : Type u_2
inst✝¹⁵ : Monoid M
inst✝¹⁴ : SMul M X
inst✝¹³ : TopologicalSpace X
inst✝¹² : R1Space X
inst✝¹¹ : MeasurableSpace X
inst✝¹⁰ : BorelSpace X
μ : Measure X
inst✝⁹ : IsFiniteMeasure μ
inst✝⁸ : μ.InnerRegular
N : Type u_3
inst✝⁷ : MulAction M N
inst✝⁶ : Monoid N
inst✝⁵ : TopologicalSpace N
inst✝⁴ : MulAction.IsMinimal M N
inst✝³ : MulAction N X
inst✝² : IsScalarTower M N X
inst✝¹ : ContinuousSMul N X
inst✝ : ErgodicSMul N X μ
c : M
s : Set X
hsm : MeasurableSet s
⊢ μ ((fun x ↦ c • x) ⁻¹' s) = μ s
Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal

Goal state before:
pp: M : Type u_1
X : Type u_2
inst✝¹⁵ : Monoid M
inst✝¹⁴ : SMul M X
inst✝¹³ : TopologicalSpace X
inst✝¹² : R1Space X
inst✝¹¹ : MeasurableSpace X
inst✝¹⁰ : BorelSpace X
μ : Measure X
inst✝⁹ : IsFiniteMeasure μ
inst✝⁸ : μ.InnerRegular
N : Type u_3
inst✝⁷ : MulAction M N
inst✝⁶ : Monoid N
inst✝⁵ : TopologicalSpace N
inst✝⁴ : MulAction.IsMinimal M N
inst✝³ : MulAction N X
inst✝² : IsScalarTower M N X
inst✝¹ : ContinuousSMul N X
inst✝ : ErgodicSMul N X μ
s : Set X
hsm : MeasurableSet s
hs : ∀ (g : M), (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s
g : M
⊢ (fun m ↦ m • 1) g ∈ {g | (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s}

Tactic:
simpa using

Goal state after:
M : Type u_1
X : Type u_2
inst✝¹⁵ : Monoid M
inst✝¹⁴ : SMul M X
inst✝¹³ : TopologicalSpace X
inst✝¹² : R1Space X
inst✝¹¹ : MeasurableSpace X
inst✝¹⁰ : BorelSpace X
μ : Measure X
inst✝⁹ : IsFiniteMeasure μ
inst✝⁸ : μ.InnerRegular
N : Type u_3
inst✝⁷ : MulAction M N
inst✝⁶ : Monoid N
inst✝⁵ : TopologicalSpace N
inst✝⁴ : MulAction.IsMinimal M N
inst✝³ : MulAction N X
inst✝² : IsScalarTower M N X
inst✝¹ : ContinuousSMul N X
inst✝ : ErgodicSMul N X μ
s : Set X
hsm : MeasurableSet s
hs : ∀ (g : M), (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s
g : M
⊢ (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s
Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal

Goal state before:
pp: M : Type u_1
X : Type u_2
inst✝¹⁵ : Monoid M
inst✝¹⁴ : SMul M X
inst✝¹³ : TopologicalSpace X
inst✝¹² : R1Space X
inst✝¹¹ : MeasurableSpace X
inst✝¹⁰ : BorelSpace X
μ : Measure X
inst✝⁹ : IsFiniteMeasure μ
inst✝⁸ : μ.InnerRegular
N : Type u_3
inst✝⁷ : MulAction M N
inst✝⁶ : Monoid N
inst✝⁵ : TopologicalSpace N
inst✝⁴ : MulAction.IsMinimal M N
inst✝³ : MulAction N X
inst✝² : IsScalarTower M N X
inst✝¹ : ContinuousSMul N X
inst✝ : ErgodicSMul N X μ
s : Set X
hsm : MeasurableSet s
hs : ∀ (g : M), (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s
⊢ EventuallyConst s (ae μ)

Tactic:
refine aeconst_of_dense_setOfPred_preimage_smul_ae (M := N) hsm.nullMeasurableSet ?_
    refine (MulAction.dense_orbit M 1).mono ?_
    rintro _ ⟨g, rfl⟩
    simpa using hs g

Goal state after:
Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal

Goal state before:
pp: G : Type u_1
inst✝¹¹ : Group G
inst✝¹⁰ : TopologicalSpace G
inst✝⁹ : ContinuousInv G
X : Type u_2
inst✝⁸ : TopologicalSpace X
inst✝⁷ : R1Space X
inst✝⁶ : MeasurableSpace X
inst✝⁵ : BorelSpace X
inst✝⁴ : MulAction G X
inst✝³ : ContinuousSMul G X
g : G
hg : DenseRange fun x ↦ g ^ x
μ : Measure X
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : ErgodicSMul G X μ
⊢ Ergodic (fun x ↦ g • x) μ

Tactic:
borelize G
  refine ⟨measurePreserving_smul _ _, ⟨fun s hsm hs ↦ ?_⟩⟩
  refine aeconst_of_dense_aestabilizer_smul hsm.nullMeasurableSet (hg.mono ?_)
  rw [← Subgroup.coe_zpowers, SetLike.coe_subset_coe, ← Subgroup.zpowers_inv, Subgroup.zpowers_le,
    MulAction.mem_aestabilizer, ← preimage_smul, hs]

Goal state after:
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f₁ f₂ : CircleDeg1Liftˣ
h : τ ↑f₁ = τ ↑f₂
this :
  ∀ (n : Multiplicative ℤ),
    τ (((Units.coeHom CircleDeg1Lift).comp ((zpowersHom CircleDeg1Liftˣ) f₁)) n) =
      τ (((Units.coeHom CircleDeg1Lift).comp ((zpowersHom CircleDeg1Liftˣ) f₂)) n)
F : CircleDeg1Lift
hF :
  ∀ (g : Multiplicative ℤ),
    Semiconj ⇑F ⇑(((Units.coeHom CircleDeg1Lift).comp ((zpowersHom CircleDeg1Liftˣ) f₁)) g)
      ⇑(((Units.coeHom CircleDeg1Lift).comp ((zpowersHom CircleDeg1Liftˣ) f₂)) g)
⊢ Semiconj ⇑F ⇑↑f₁ ⇑↑f₂

Tactic:
simpa using

Goal state after:
f₁ f₂ : CircleDeg1Liftˣ
h : τ ↑f₁ = τ ↑f₂
this :
  ∀ (n : Multiplicative ℤ),
    τ (((Units.coeHom CircleDeg1Lift).comp ((zpowersHom CircleDeg1Liftˣ) f₁)) n) =
      τ (((Units.coeHom CircleDeg1Lift).comp ((zpowersHom CircleDeg1Liftˣ) f₂)) n)
F : CircleDeg1Lift
hF :
  ∀ (g : Multiplicative ℤ),
    Semiconj ⇑F ⇑(((Units.coeHom CircleDeg1Lift).comp ((zpowersHom CircleDeg1Liftˣ) f₁)) g)
      ⇑(((Units.coeHom CircleDeg1Lift).comp ((zpowersHom CircleDeg1Liftˣ) f₂)) g)
⊢ Semiconj ⇑F ⇑↑f₁ ⇑↑f₂
Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal

Goal state before:
pp: G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : MeasurableSpace G
inst✝¹ : OpensMeasurableSpace G
μ : Measure G
inst✝ : μ.IsOpenPosMeasure
g : G
hg : Ergodic (fun x ↦ g * x) μ
a : G
h : (range fun x ↦ g ^ x)ᶜ ∈ 𝓝 a
this :
  Tendsto
    (fun x ↦
      match x with
      | (x, y) => a * x / y)
    (𝓝 1.1 ×ˢ 𝓝 1.2) (𝓝 a)
⊢ ∃ V, 1 ∈ V ∧ IsOpen[inst✝⁴] V ∧ ∀ x ∈ V, ∀ y ∈ V, ∀ (m : ℤ), g ^ m ≠ a * x / y

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : MeasurableSpace G
inst✝¹ : OpensMeasurableSpace G
μ : Measure G
inst✝ : μ.IsOpenPosMeasure
g : G
hg : Ergodic (fun x ↦ g * x) μ
a : G
h : (range fun x ↦ g ^ x)ᶜ ∈ 𝓝 a
this :
  Tendsto
    (fun x ↦
      match x with
      | (x, y) => a * x / y)
    (𝓝 1.1 ×ˢ 𝓝 1.2) (𝓝 a)
⊢ ∃ V, 1 ∈ V ∧ IsOpen[inst✝⁴] V ∧ ∀ x ∈ V, ∀ y ∈ V, ∀ (m : ℤ), ¬g ^ m = a * x / y
Module: Mathlib.MeasureTheory.Group.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hI : I =ᵐ[volume] B
hn : 1 ≤ ↑n
g : AddCircle T
hg : g ∈ G
hg' : ⟨g, hg⟩ ≠ 0
⊢ g ≠ 0

Tactic:
simpa using

Goal state after:
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hI : I =ᵐ[volume] B
hn : 1 ≤ ↑n
g : AddCircle T
hg : g ∈ G
hg' : ⟨g, hg⟩ ≠ 0
⊢ ¬g = 0
Module: Mathlib.Topology.Order.CountableSeparating

Goal state before:
pp: case refine_3.inr
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : LinearOrder X
inst✝¹ : OrderTopology X
inst✝ : SecondCountableTopology X
s✝ s : Set X
hsc : s.Countable
hsd : Dense s
t : Set X := s ∪ {x | ∃ y, y ⋖ x}
x y : X
h : ∀ s ∈ Iio '' t, x ∈ s ↔ y ∈ s
hne : x ≠ y
this : ∀ (x y : X), (∀ s ∈ Iio '' t, x ∈ s ↔ y ∈ s) → x ≠ y → x < y → False
hlt : ¬x < y
⊢ ∀ s ∈ Iio '' t, y ∈ s ↔ x ∈ s

Tactic:
simpa using

Goal state after:
case refine_3.inr
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : LinearOrder X
inst✝¹ : OrderTopology X
inst✝ : SecondCountableTopology X
s✝ s : Set X
hsc : s.Countable
hsd : Dense s
t : Set X := s ∪ {x | ∃ y, y ⋖ x}
x y : X
h : ∀ s ∈ Iio '' t, x ∈ s ↔ y ∈ s
hne : x ≠ y
this : ∀ (x y : X), (∀ s ∈ Iio '' t, x ∈ s ↔ y ∈ s) → x ≠ y → x < y → False
hlt : ¬x < y
⊢ ∀ s ∈ Iio '' t, x ∈ s ↔ y ∈ s
Module: Mathlib.Topology.Order.CountableSeparating

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : LinearOrder X
inst✝¹ : OrderTopology X
inst✝ : SecondCountableTopology X
s✝ s : Set X
hsc : s.Countable
hsd : Dense s
t : Set X := s ∪ {x | ∃ y, y ⋖ x}
x y : X
h : ∀ s ∈ Iio '' t, x ∈ s ↔ y ∈ s
hne : x ≠ y
hlt : x < y
he : Ioo x y = ∅
⊢ ∀ ⦃c : X⦄, x < c → ¬c < y

Tactic:
simpa using

Goal state after:
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : LinearOrder X
inst✝¹ : OrderTopology X
inst✝ : SecondCountableTopology X
s✝ s : Set X
hsc : s.Countable
hsd : Dense s
t : Set X := s ∪ {x | ∃ y, y ⋖ x}
x y : X
h : ∀ s ∈ Iio '' t, x ∈ s ↔ y ∈ s
hne : x ≠ y
hlt : x < y
he : Ioo x y = ∅
⊢ ∀ ⦃c : X⦄, x < c → y ≤ c
Module: Mathlib.Topology.Order.CountableSeparating

Goal state before:
pp: case inr
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : LinearOrder X
inst✝¹ : OrderTopology X
inst✝ : SecondCountableTopology X
s✝ s : Set X
hsc : s.Countable
hsd : Dense s
t : Set X := s ∪ {x | ∃ y, y ⋖ x}
x y : X
h : ∀ s ∈ Iio '' t, x ∈ s ↔ y ∈ s
hne✝ : x ≠ y
hlt : x < y
hne : (Ioo x y).Nonempty
z : X
hzs : z ∈ s
hxz : x < z
hzy : z < y
⊢ False

Tactic:
simpa using

Goal state after:
case inr
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : LinearOrder X
inst✝¹ : OrderTopology X
inst✝ : SecondCountableTopology X
s✝ s : Set X
hsc : s.Countable
hsd : Dense s
t : Set X := s ∪ {x | ∃ y, y ⋖ x}
x y : X
h : ∀ s ∈ Iio '' t, x ∈ s ↔ y ∈ s
hne✝ : x ≠ y
hlt : x < y
hne : (Ioo x y).Nonempty
z : X
hzs : z ∈ s
hxz : x < z
hzy : z < y
⊢ False
Module: Mathlib.Topology.Order.CountableSeparating

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : LinearOrder X
inst✝¹ : OrderTopology X
inst✝ : SecondCountableTopology X
s : Set X
t : Set (Set X)
htc : t.Countable
ht_sub : ∀ s ∈ t, s ∈ range Ioi
ht : ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ t, x ∈ s ↔ y ∈ s) → x = y
⊢ ∀ s ∈ compl '' t, s ∈ range Iic

Tactic:
simpa using

Goal state after:
X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : LinearOrder X
inst✝¹ : OrderTopology X
inst✝ : SecondCountableTopology X
s : Set X
t : Set (Set X)
htc : t.Countable
ht_sub : ∀ s ∈ t, s ∈ range Ioi
ht : ∀ x ∈ s, ∀ y ∈ s, (∀ s ∈ t, x ∈ s ↔ y ∈ s) → x = y
⊢ ∀ a ∈ t, ∃ y, Iic y = aᶜ
Module: Mathlib.Dynamics.Ergodic.Extreme

Goal state before:
pp: case inr
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
c : ℝ≥0∞
hc : c ≠ ∞
hf : MeasurePreserving f μ μ
hc₀ : c ≠ 0
this✝ : IsFiniteMeasure μ
S : Set (Measure X) := {ν | MeasurePreserving f ν ν ∧ ν univ = c}
h : μ ∈ extremePoints ℝ≥0∞ S
this : ∀ {s : Set X}, MeasurableSet s → f ⁻¹' s = s → μ s ≠ 0 → c • μ[|s] ∈ S
s : Set X
hsm : MeasurableSet s
hfs : f ⁻¹' s = s
H : ¬EventuallyConst s (ae μ)
⊢ False

Tactic:
obtain ⟨hs, hs'⟩ : μ s ≠ 0 ∧ μ sᶜ ≠ 0 := by
      simpa [eventuallyConst_set, ae_iff, and_comm] using! H

Goal state after:
case inr
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
c : ℝ≥0∞
hc : c ≠ ∞
hf : MeasurePreserving f μ μ
hc₀ : c ≠ 0
this✝ : IsFiniteMeasure μ
S : Set (Measure X) := {ν | MeasurePreserving f ν ν ∧ ν univ = c}
h : μ ∈ extremePoints ℝ≥0∞ S
this : ∀ {s : Set X}, MeasurableSet s → f ⁻¹' s = s → μ s ≠ 0 → c • μ[|s] ∈ S
s : Set X
hsm : MeasurableSet s
hfs : f ⁻¹' s = s
H : ¬EventuallyConst s (ae μ)
hs : μ s ≠ 0
hs' : μ sᶜ ≠ 0
⊢ False
Module: Mathlib.Dynamics.FixedPoints.Support

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
f : X → X
⊢ HasCompactFixedSupport f ↔ ∃ K, IsClosed K ∧ IsCompact K ∧ (fixedPoints f)ᶜ ⊆ K

Tactic:
refine ⟨fun hf ↦ ?_, fun ⟨K, hK₁, hK₂, hf⟩ ↦ ?_⟩

Goal state after:
case refine_1
X : Type u_1
inst✝ : TopologicalSpace X
f : X → X
hf : HasCompactFixedSupport f
⊢ ∃ K, IsClosed K ∧ IsCompact K ∧ (fixedPoints f)ᶜ ⊆ K

case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
f : X → X
x✝ : ∃ K, IsClosed K ∧ IsCompact K ∧ (fixedPoints f)ᶜ ⊆ K
K : Set X
hK₁ : IsClosed K
hK₂ : IsCompact K
hf : (fixedPoints f)ᶜ ⊆ K
⊢ HasCompactFixedSupport f
Module: Mathlib.Dynamics.Ergodic.Extreme

Goal state before:
pp: X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
h : μ ∈ extremePoints ℝ≥0∞ {ν | MeasurePreserving f ν ν ∧ IsProbabilityMeasure ν}
⊢ μ ∈ extremePoints ℝ≥0∞ {ν | MeasurePreserving f ν ν ∧ ν univ = 1}

Tactic:
simpa using

Goal state after:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
h : μ ∈ extremePoints ℝ≥0∞ {ν | MeasurePreserving f ν ν ∧ IsProbabilityMeasure ν}
⊢ μ ∈ extremePoints ℝ≥0∞ {ν | MeasurePreserving f ν ν ∧ ν univ = 1}
Module: Mathlib.Dynamics.Ergodic.Extreme

Goal state before:
pp: X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
inst✝ : IsProbabilityMeasure μ
hμ : Ergodic f μ
⊢ μ ∈ extremePoints ℝ≥0∞ {ν | MeasurePreserving f ν ν ∧ IsProbabilityMeasure ν}

Tactic:
simpa using

Goal state after:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
inst✝ : IsProbabilityMeasure μ
hμ : Ergodic f μ
⊢ μ ∈ extremePoints ℝ≥0∞ {ν | MeasurePreserving f ν ν ∧ ν univ = 1}
Module: Mathlib.Dynamics.SymbolicDynamics.Basic

Goal state before:
pp: A : Type u_1
G : Type u_2
inst✝¹ : TopologicalSpace A
inst✝ : DiscreteTopology A
U : Finset G
x : G → A
⊢ IsOpen[Pi.topologicalSpace] (cylinder U x)

Tactic:
simpa using

Goal state after:
A : Type u_1
G : Type u_2
inst✝¹ : TopologicalSpace A
inst✝ : DiscreteTopology A
U : Finset G
x : G → A
⊢ IsOpen[Pi.topologicalSpace] ((↑U).pi fun i ↦ {x i})
Module: Mathlib.Dynamics.SymbolicDynamics.Basic

Goal state before:
pp: A : Type u_1
G : Type u_2
inst✝¹ : TopologicalSpace A
inst✝ : T1Space A
U : Finset G
x : G → A
⊢ IsClosed[Pi.topologicalSpace] (cylinder U x)

Tactic:
simpa using

Goal state after:
A : Type u_1
G : Type u_2
inst✝¹ : TopologicalSpace A
inst✝ : T1Space A
U : Finset G
x : G → A
⊢ IsClosed[Pi.topologicalSpace] ((↑U).pi fun i ↦ {x i})
Module: Mathlib.Dynamics.SymbolicDynamics.Basic

Goal state before:
pp: A : Type u_1
inst✝² : Inhabited A
G : Type u_2
inst✝¹ : Monoid G
inst✝ : IsLeftCancelMul G
p : Pattern A G
v h : G
hmem : h ∈ Finset.image (fun x ↦ v * x) p.support
⊢ ∃ w ∈ p.support, v * w = h

Tactic:
simpa using

Goal state after:
A : Type u_1
inst✝² : Inhabited A
G : Type u_2
inst✝¹ : Monoid G
inst✝ : IsLeftCancelMul G
p : Pattern A G
v h : G
hmem : h ∈ Finset.image (fun x ↦ v * x) p.support
⊢ ∃ w ∈ p.support, v * w = h
Module: Mathlib.Dynamics.SymbolicDynamics.Basic

Goal state before:
pp: A : Type u_1
inst✝² : Inhabited A
G : Type u_2
inst✝¹ : Monoid G
inst✝ : IsLeftCancelMul G
p : Pattern A G
v : G
⊢ G → A

Tactic:
intro h
  if hmem : h ∈ p.support.image (v * ·) then
    -- package existence of a preimage under (v * ·)
    let ex : ∃ w, w ∈ p.support ∧ v * w = h := by
      simpa [Finset.mem_image] using hmem
    exact p.config (Classical.choose ex)
  else
    exact default

Goal state after:
Module: Mathlib.Dynamics.SymbolicDynamics.Basic

Goal state before:
pp: A : Type u_1
inst✝² : Inhabited A
G : Type u_2
inst✝¹ : Monoid G
inst✝ : IsLeftCancelMul G
p : Pattern A G
v w : G
hw : w ∈ p.support
hmem : v * w ∈ Finset.image (fun x ↦ v * x) p.support
⊢ ∃ w' ∈ p.support, v * w' = v * w

Tactic:
simpa using

Goal state after:
A : Type u_1
inst✝² : Inhabited A
G : Type u_2
inst✝¹ : Monoid G
inst✝ : IsLeftCancelMul G
p : Pattern A G
v w : G
hw : w ∈ p.support
hmem : v * w ∈ Finset.image (fun x ↦ v * x) p.support
⊢ w ∈ p.support
Module: Mathlib.Dynamics.SymbolicDynamics.Basic

Goal state before:
pp: A : Type u_3
G : Type u_4
inst✝¹ : Inhabited A
inst✝ : Monoid G
F : Set (Pattern A G)
h : G
x : G → A
p : Pattern A G
hp : p ∈ F
g : G
hx : p.mulOccursInAt (mulShift h x) g
⊢ p.mulOccursInAt x (h * g)

Tactic:
simpa using

Goal state after:
A : Type u_3
G : Type u_4
inst✝¹ : Inhabited A
inst✝ : Monoid G
F : Set (Pattern A G)
h : G
x : G → A
p : Pattern A G
hp : p ∈ F
g : G
hx : p.mulOccursInAt (mulShift h x) g
⊢ p.mulOccursInAt x (h * g)
Module: Mathlib.Dynamics.SymbolicDynamics.Basic

Goal state before:
pp: case mp
A : Type u_1
inst✝² : Inhabited A
G : Type u_2
inst✝¹ : Monoid G
inst✝ : IsLeftCancelMul G
p : Pattern A G
g : G
x : G → A
H : x ∈ {x | p.mulOccursInAt x g}
w : G
hw : w ∈ p.support
hu : g * w ∈ Finset.image (fun x ↦ g * x) p.support
hx : x (g * w) = p.config w
⊢ x (g * w) = p.mulShift g (g * w)

Tactic:
simpa using

Goal state after:
case mp
A : Type u_1
inst✝² : Inhabited A
G : Type u_2
inst✝¹ : Monoid G
inst✝ : IsLeftCancelMul G
p : Pattern A G
g : G
x : G → A
H : x ∈ {x | p.mulOccursInAt x g}
w : G
hw : w ∈ p.support
hu : g * w ∈ Finset.image (fun x ↦ g * x) p.support
hx : x (g * w) = p.config w
⊢ x (g * w) = p.config w
Module: Mathlib.Dynamics.SymbolicDynamics.Basic

Goal state before:
pp: case mpr
A : Type u_1
inst✝² : Inhabited A
G : Type u_2
inst✝¹ : Monoid G
inst✝ : IsLeftCancelMul G
p : Pattern A G
g : G
x : G → A
H : x ∈ cylinder (Finset.image (fun x ↦ g * x) p.support) (p.mulShift g)
u : G
hu : u ∈ p.support
hx : x (g * u) = p.mulShift g (g * u)
⊢ x (g * u) = p.config u

Tactic:
simpa using

Goal state after:
case mpr
A : Type u_1
inst✝² : Inhabited A
G : Type u_2
inst✝¹ : Monoid G
inst✝ : IsLeftCancelMul G
p : Pattern A G
g : G
x : G → A
H : x ∈ cylinder (Finset.image (fun x ↦ g * x) p.support) (p.mulShift g)
u : G
hu : u ∈ p.support
hx : x (g * u) = p.mulShift g (g * u)
⊢ x (g * u) = p.config u