mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (f₁ g) = τ (f₂ g)
x : ℝ
g : G
this : τ (f₂ g⁻¹) = -τ (f₂ g)
⊢ (f₂ g⁻¹) (x + τ (f₂ g)) + 1 = (f₂ g⁻¹) (x + τ (f₂ g)) + 1

Tactic:
]

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

Goal state before:
pp: M : Type u_1
inst✝⁹ : TopologicalSpace M
X : Type u_2
inst✝⁸ : TopologicalSpace X
inst✝⁷ : R1Space X
inst✝⁶ : MeasurableSpace X
inst✝⁵ : BorelSpace X
inst✝⁴ : SMul M X
inst✝³ : ContinuousSMul M X
μ : Measure X
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : ErgodicSMul M X μ
s : Set X
hsm : NullMeasurableSet s μ
hd : ∀ (x : M), x ∈ {g | (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s}
this✝¹ : MeasurableSpace M := borel M
this✝ : BorelSpace M
⊢ ∀ (g : M), (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s

pp: M : Type u_1
inst✝⁹ : TopologicalSpace M
X : Type u_2
inst✝⁸ : TopologicalSpace X
inst✝⁷ : R1Space X
inst✝⁶ : MeasurableSpace X
inst✝⁵ : BorelSpace X
inst✝⁴ : SMul M X
inst✝³ : ContinuousSMul M X
μ : Measure X
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : ErgodicSMul M X μ
s : Set X
hsm : NullMeasurableSet s μ
hd : closure[inst✝⁹] {g | (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s} = univ
this✝¹ : MeasurableSpace M := borel M
this✝ : BorelSpace M
⊢ IsClosed[inst✝⁹] {g | (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s}

Tactic:
]

Goal state after:
M : Type u_1
inst✝⁹ : TopologicalSpace M
X : Type u_2
inst✝⁸ : TopologicalSpace X
inst✝⁷ : R1Space X
inst✝⁶ : MeasurableSpace X
inst✝⁵ : BorelSpace X
inst✝⁴ : SMul M X
inst✝³ : ContinuousSMul M X
μ : Measure X
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : ErgodicSMul M X μ
s : Set X
hsm : NullMeasurableSet s μ
hd : ∀ (x : M), x ∈ {g | (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s}
this✝¹ : MeasurableSpace M := borel M
this✝ : BorelSpace M
⊢ ∀ (g : M), (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s

M : Type u_1
inst✝⁹ : TopologicalSpace M
X : Type u_2
inst✝⁸ : TopologicalSpace X
inst✝⁷ : R1Space X
inst✝⁶ : MeasurableSpace X
inst✝⁵ : BorelSpace X
inst✝⁴ : SMul M X
inst✝³ : ContinuousSMul M X
μ : Measure X
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : ErgodicSMul M X μ
s : Set X
hsm : NullMeasurableSet s μ
hd : closure[inst✝⁹] {g | (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s} = univ
this✝¹ : MeasurableSpace M := borel M
this✝ : BorelSpace M
⊢ IsClosed[inst✝⁹] {g | (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s}
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (f₁ g) = τ (f₂ g)
x : ℝ
g : G
this : τ (f₂ g⁻¹) = -τ (f₂ g)
⊢ x + τ (f₂ g) + τ (f₂ g⁻¹) + 1 + 1 ≤ x + τ (f₂ g) + τ (f₂ g⁻¹) + 1 + 1

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.ContinuousPreimage

Goal state before:
pp: α : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁹ : TopologicalSpace X
inst✝⁸ : MeasurableSpace X
inst✝⁷ : BorelSpace X
inst✝⁶ : R1Space X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : MeasurableSpace Y
inst✝³ : BorelSpace Y
inst✝² : R1Space Y
μ : Measure X
ν : Measure Y
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : IsLocallyFiniteMeasure ν
l : Filter α
f : α → C(X, Y)
g : C(X, Y)
hfg : Tendsto f l (𝓝 g)
hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a)) μ ν
hg : MeasurePreserving (⇑g) μ ν
this : ν.InnerRegularCompactLTTop
s : Set Y
hs : NullMeasurableSet s ν
hνs : ν s ≠ ∞
ε : ℝ≥0∞
hε : ε > 0
hso : IsOpen[inst✝⁵] s
hνs' : μ (⇑g ⁻¹' s) ≠ ∞
K : Set X
hKg : MapsTo (⇑g) K s
hKco : IsCompact K
hKcl : IsClosed[inst✝⁹] K
hKμ : μ (⇑g ⁻¹' s \ K) < ε / 2
hKm : NullMeasurableSet K μ
a : α
hfa : MeasurePreserving (⇑(f a)) μ ν
ha : MapsTo (⇑(f a)) K s
⊢ μ ((⇑(f a) ⁻¹' s) ∆ (⇑g ⁻¹' s)) ≤ ε / 2 + ε / 2

Tactic:
]

Goal state after:
α : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁹ : TopologicalSpace X
inst✝⁸ : MeasurableSpace X
inst✝⁷ : BorelSpace X
inst✝⁶ : R1Space X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : MeasurableSpace Y
inst✝³ : BorelSpace Y
inst✝² : R1Space Y
μ : Measure X
ν : Measure Y
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : IsLocallyFiniteMeasure ν
l : Filter α
f : α → C(X, Y)
g : C(X, Y)
hfg : Tendsto f l (𝓝 g)
hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a)) μ ν
hg : MeasurePreserving (⇑g) μ ν
this : ν.InnerRegularCompactLTTop
s : Set Y
hs : NullMeasurableSet s ν
hνs : ν s ≠ ∞
ε : ℝ≥0∞
hε : ε > 0
hso : IsOpen[inst✝⁵] s
hνs' : μ (⇑g ⁻¹' s) ≠ ∞
K : Set X
hKg : MapsTo (⇑g) K s
hKco : IsCompact K
hKcl : IsClosed[inst✝⁹] K
hKμ : μ (⇑g ⁻¹' s \ K) < ε / 2
hKm : NullMeasurableSet K μ
a : α
hfa : MeasurePreserving (⇑(f a)) μ ν
ha : MapsTo (⇑(f a)) K s
⊢ μ ((⇑(f a) ⁻¹' s) ∆ (⇑g ⁻¹' s)) ≤ ε / 2 + ε / 2
Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal

Goal state before:
pp: X : Type u_2
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : R1Space X
inst✝⁸ : MeasurableSpace X
inst✝⁷ : BorelSpace X
M : Type u_3
inst✝⁶ : Monoid M
inst✝⁵ : TopologicalSpace M
inst✝⁴ : MulAction M X
inst✝³ : ContinuousSMul M X
g : M
hg : DenseRange fun x ↦ g ^ x
μ : Measure X
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : ErgodicSMul M X μ
this✝¹ : MeasurableSpace M := borel M
this✝ : BorelSpace M
s : Set X
hsm : MeasurableSet s
hs : (fun x ↦ g • x) ⁻¹' s = s
n : ℕ
⊢ s = s

Tactic:
]

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
μ : Measure X
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : ErgodicSMul G X μ
s : Set X
hsm : NullMeasurableSet s μ
hd : Dense ↑(MulAction.aestabilizer G μ s)
g : G
hg : g ∈ Inv.inv ⁻¹' ↑(MulAction.aestabilizer G μ s)
⊢ g ∈ {g | (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s}

Tactic:
simpa only [preimage_smul] using! hg

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 μ
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
s : Set X
hsm : MeasurableSet s
hs : (fun x ↦ g • x) ⁻¹' s = s
⊢ s =ᵐ[μ] s

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.ContinuousPreimage

Goal state before:
pp: α : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁹ : TopologicalSpace X
inst✝⁸ : MeasurableSpace X
inst✝⁷ : BorelSpace X
inst✝⁶ : R1Space X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : MeasurableSpace Y
inst✝³ : BorelSpace Y
inst✝² : R1Space Y
μ : Measure X
ν : Measure Y
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : IsLocallyFiniteMeasure ν
l : Filter α
f : α → C(X, Y)
g : C(X, Y)
hfg : Tendsto f l (𝓝 g)
hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a)) μ ν
hg : MeasurePreserving (⇑g) μ ν
this : ν.InnerRegularCompactLTTop
s : Set Y
hs : NullMeasurableSet s ν
hνs : ν s ≠ ∞
ε : ℝ≥0∞
hε : ε > 0
hso : IsOpen[inst✝⁵] s
hνs' : μ (⇑g ⁻¹' s) ≠ ∞
K : Set X
hKg : MapsTo (⇑g) K s
hKco : IsCompact K
hKcl : IsClosed[inst✝⁹] K
hKμ : μ (⇑g ⁻¹' s \ K) < ε / 2
hKm : NullMeasurableSet K μ
a : α
hfa : MeasurePreserving (⇑(f a)) μ ν
ha : MapsTo (⇑(f a)) K s
⊢ μ (⇑(f a) ⁻¹' s \ K) + μ (⇑g ⁻¹' s \ K) ≤ ε / 2 + ε / 2

Tactic:
]

Goal state after:
α : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁹ : TopologicalSpace X
inst✝⁸ : MeasurableSpace X
inst✝⁷ : BorelSpace X
inst✝⁶ : R1Space X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : MeasurableSpace Y
inst✝³ : BorelSpace Y
inst✝² : R1Space Y
μ : Measure X
ν : Measure Y
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : IsLocallyFiniteMeasure ν
l : Filter α
f : α → C(X, Y)
g : C(X, Y)
hfg : Tendsto f l (𝓝 g)
hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a)) μ ν
hg : MeasurePreserving (⇑g) μ ν
this : ν.InnerRegularCompactLTTop
s : Set Y
hs : NullMeasurableSet s ν
hνs : ν s ≠ ∞
ε : ℝ≥0∞
hε : ε > 0
hso : IsOpen[inst✝⁵] s
hνs' : μ (⇑g ⁻¹' s) ≠ ∞
K : Set X
hKg : MapsTo (⇑g) K s
hKco : IsCompact K
hKcl : IsClosed[inst✝⁹] K
hKμ : μ (⇑g ⁻¹' s \ K) < ε / 2
hKm : NullMeasurableSet K μ
a : α
hfa : MeasurePreserving (⇑(f a)) μ ν
ha : MapsTo (⇑(f a)) K s
⊢ μ (⇑(f a) ⁻¹' s \ K) + μ (⇑g ⁻¹' s \ K) ≤ ε / 2 + ε / 2
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
⊢ ∃ V, 1 ∈ V ∧ IsOpen[inst✝⁴] V ∧ ∀ x ∈ V, ∀ y ∈ V, ∀ (m : ℤ), g ^ m ≠ a * x / y

Tactic:
]

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
⊢ ∃ V, 1 ∈ V ∧ IsOpen[inst✝⁴] V ∧ ∀ x ∈ V, ∀ y ∈ V, ∀ (m : ℤ), g ^ m ≠ a * x / y
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:
]

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.Measure.ContinuousPreimage

Goal state before:
pp: case h₁
α : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁹ : TopologicalSpace X
inst✝⁸ : MeasurableSpace X
inst✝⁷ : BorelSpace X
inst✝⁶ : R1Space X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : MeasurableSpace Y
inst✝³ : BorelSpace Y
inst✝² : R1Space Y
μ : Measure X
ν : Measure Y
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : IsLocallyFiniteMeasure ν
l : Filter α
f : α → C(X, Y)
g : C(X, Y)
hfg : Tendsto f l (𝓝 g)
hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a)) μ ν
hg : MeasurePreserving (⇑g) μ ν
this : ν.InnerRegularCompactLTTop
s : Set Y
hs : NullMeasurableSet s ν
hνs : ν s ≠ ∞
ε : ℝ≥0∞
hε : ε > 0
hso : IsOpen[inst✝⁵] s
hνs' : μ (⇑g ⁻¹' s) ≠ ∞
K : Set X
hKg : MapsTo (⇑g) K s
hKco : IsCompact K
hKcl : IsClosed[inst✝⁹] K
hKμ : μ (⇑g ⁻¹' s \ K) < ε / 2
hKm : NullMeasurableSet K μ
a : α
hfa : MeasurePreserving (⇑(f a)) μ ν
ha : MapsTo (⇑(f a)) K s
hK' : μ K ≠ ∞
⊢ μ (⇑g ⁻¹' s \ K) ≤ ε / 2

Tactic:
]

Goal state after:
case h₁
α : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁹ : TopologicalSpace X
inst✝⁸ : MeasurableSpace X
inst✝⁷ : BorelSpace X
inst✝⁶ : R1Space X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : MeasurableSpace Y
inst✝³ : BorelSpace Y
inst✝² : R1Space Y
μ : Measure X
ν : Measure Y
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : IsLocallyFiniteMeasure ν
l : Filter α
f : α → C(X, Y)
g : C(X, Y)
hfg : Tendsto f l (𝓝 g)
hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a)) μ ν
hg : MeasurePreserving (⇑g) μ ν
this : ν.InnerRegularCompactLTTop
s : Set Y
hs : NullMeasurableSet s ν
hνs : ν s ≠ ∞
ε : ℝ≥0∞
hε : ε > 0
hso : IsOpen[inst✝⁵] s
hνs' : μ (⇑g ⁻¹' s) ≠ ∞
K : Set X
hKg : MapsTo (⇑g) K s
hKco : IsCompact K
hKcl : IsClosed[inst✝⁹] K
hKμ : μ (⇑g ⁻¹' s \ K) < ε / 2
hKm : NullMeasurableSet K μ
a : α
hfa : MeasurePreserving (⇑(f a)) μ ν
ha : MapsTo (⇑(f a)) K s
hK' : μ K ≠ ∞
⊢ μ (⇑g ⁻¹' s \ K) ≤ ε / 2
Module: Mathlib.Dynamics.Ergodic.AddCircle

Goal state before:
pp: 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 =ᵐ[μ] s
n : ι → ℕ := addOrderOf ∘ u
hu₂ : Tendsto n l atTop
hT₀ : 0 < T
hT₁ : ENNReal.ofReal T ≠ 0
⊢ μ s = 0 ∨ μ s = ENNReal.ofReal T

Tactic:
]

Goal state after:
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 =ᵐ[μ] s
n : ι → ℕ := addOrderOf ∘ u
hu₂ : Tendsto n l atTop
hT₀ : 0 < T
hT₁ : ENNReal.ofReal T ≠ 0
⊢ μ s = 0 ∨ μ s = ENNReal.ofReal T
Module: Mathlib.MeasureTheory.Measure.ContinuousPreimage

Goal state before:
pp: X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : MeasurableSpace X
inst✝⁸ : BorelSpace X
inst✝⁷ : R1Space X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : MeasurableSpace Y
inst✝⁴ : BorelSpace Y
inst✝³ : R1Space Y
inst✝² : TopologicalSpace Z
μ : Measure X
ν : Measure Y
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : IsLocallyFiniteMeasure ν
f : Z → C(X, Y)
hf : Continuous[inst✝², _] f
hfm : ∀ (z : Z), MeasurePreserving (⇑(f z)) μ ν
s : Set X
t : Set Y
htm : NullMeasurableSet t ν
ht : ν t ≠ ∞
⊢ ∀ x ∈ {z | ⇑(f z) ⁻¹' t =ᵐ[μ] s}ᶜ, {z | ⇑(f z) ⁻¹' t =ᵐ[μ] s}ᶜ ∈ 𝓝 x

Tactic:
]

Goal state after:
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : MeasurableSpace X
inst✝⁸ : BorelSpace X
inst✝⁷ : R1Space X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : MeasurableSpace Y
inst✝⁴ : BorelSpace Y
inst✝³ : R1Space Y
inst✝² : TopologicalSpace Z
μ : Measure X
ν : Measure Y
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : IsLocallyFiniteMeasure ν
f : Z → C(X, Y)
hf : Continuous[inst✝², _] f
hfm : ∀ (z : Z), MeasurePreserving (⇑(f z)) μ ν
s : Set X
t : Set Y
htm : NullMeasurableSet t ν
ht : ν t ≠ ∞
⊢ ∀ x ∈ {z | ⇑(f z) ⁻¹' t =ᵐ[μ] s}ᶜ, {z | ⇑(f z) ⁻¹' t =ᵐ[μ] s}ᶜ ∈ 𝓝 x
Module: Mathlib.MeasureTheory.Measure.ContinuousPreimage

Goal state before:
pp: X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : MeasurableSpace X
inst✝⁸ : BorelSpace X
inst✝⁷ : R1Space X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : MeasurableSpace Y
inst✝⁴ : BorelSpace Y
inst✝³ : R1Space Y
inst✝² : TopologicalSpace Z
μ : Measure X
ν : Measure Y
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : IsLocallyFiniteMeasure ν
f : Z → C(X, Y)
hf : Continuous[inst✝², _] f
hfm : ∀ (z : Z), MeasurePreserving (⇑(f z)) μ ν
s : Set X
t : Set Y
htm : NullMeasurableSet t ν
ht : ν t ≠ ∞
z : Z
hz : z ∈ {z | ⇑(f z) ⁻¹' t =ᵐ[μ] s}ᶜ
⊢ ¬⇑(f z) ⁻¹' t =ᵐ[μ] s

Tactic:
]

Goal state after:
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : MeasurableSpace X
inst✝⁸ : BorelSpace X
inst✝⁷ : R1Space X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : MeasurableSpace Y
inst✝⁴ : BorelSpace Y
inst✝³ : R1Space Y
inst✝² : TopologicalSpace Z
μ : Measure X
ν : Measure Y
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : IsLocallyFiniteMeasure ν
f : Z → C(X, Y)
hf : Continuous[inst✝², _] f
hfm : ∀ (z : Z), MeasurePreserving (⇑(f z)) μ ν
s : Set X
t : Set Y
htm : NullMeasurableSet t ν
ht : ν t ≠ ∞
z : Z
hz : z ∈ {z | ⇑(f z) ⁻¹' t =ᵐ[μ] s}ᶜ
⊢ ¬⇑(f z) ⁻¹' t =ᵐ[μ] s
Module: Mathlib.MeasureTheory.Group.AddCircle

Goal state before:
pp: case inl
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : ε ≤ 0
⊢ 2 * ε ≤ 0

Tactic:
]

Goal state after:
case inl
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
ε : ℝ
hε : ε ≤ 0
⊢ 2 * ε ≤ 0
Module: Mathlib.MeasureTheory.Measure.ContinuousPreimage

Goal state before:
pp: X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : MeasurableSpace X
inst✝⁸ : BorelSpace X
inst✝⁷ : R1Space X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : MeasurableSpace Y
inst✝⁴ : BorelSpace Y
inst✝³ : R1Space Y
inst✝² : TopologicalSpace Z
μ : Measure X
ν : Measure Y
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : IsLocallyFiniteMeasure ν
f : Z → C(X, Y)
hf : Continuous[inst✝², _] f
hfm : ∀ (z : Z), MeasurePreserving (⇑(f z)) μ ν
s : Set X
t : Set Y
htm : NullMeasurableSet t ν
ht : ν t ≠ ∞
z : Z
hz : ∀ᶠ (ε : ℝ≥0∞) in 𝓝 0, ε < μ ((⇑(f z) ⁻¹' t) ∆ s)
w : Z
hw : μ ((⇑(f z) ⁻¹' t) ∆ s) < μ ((⇑(f z) ⁻¹' t) ∆ s)
hw' : ⇑(f w) ⁻¹' t =ᵐ[μ] s
⊢ False

Tactic:
]

Goal state after:
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : MeasurableSpace X
inst✝⁸ : BorelSpace X
inst✝⁷ : R1Space X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : MeasurableSpace Y
inst✝⁴ : BorelSpace Y
inst✝³ : R1Space Y
inst✝² : TopologicalSpace Z
μ : Measure X
ν : Measure Y
inst✝¹ : μ.InnerRegularCompactLTTop
inst✝ : IsLocallyFiniteMeasure ν
f : Z → C(X, Y)
hf : Continuous[inst✝², _] f
hfm : ∀ (z : Z), MeasurePreserving (⇑(f z)) μ ν
s : Set X
t : Set Y
htm : NullMeasurableSet t ν
ht : ν t ≠ ∞
z : Z
hz : ∀ᶠ (ε : ℝ≥0∞) in 𝓝 0, ε < μ ((⇑(f z) ⁻¹' t) ∆ s)
w : Z
hw : μ ((⇑(f z) ⁻¹' t) ∆ s) < μ ((⇑(f z) ⁻¹' t) ∆ s)
hw' : ⇑(f w) ⁻¹' t =ᵐ[μ] s
⊢ False
Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup

Goal state before:
pp: case inl
a : ℝ
⊢ Dense ↑(AddSubgroup.closure {0, a}) ↔ Irrational (a / 0)

Tactic:
]

Goal state after:
case inl
a : ℝ
⊢ Dense ↑(AddSubgroup.closure {0, a}) ↔ Irrational (a / 0)
Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup

Goal state before:
pp: case inr.mp
a b : ℝ
hb : b ≠ 0
hd : Dense ↑(AddSubgroup.closure {a, b})
r : ℚ
hr : ↑r = a / b
⊢ (a ∈ range fun x ↦ x • (b / ↑r.den)) ∧ b ∈ range fun x ↦ x • (b / ↑r.den)

Tactic:
]

Goal state after:
case inr.mp
a b : ℝ
hb : b ≠ 0
hd : Dense ↑(AddSubgroup.closure {a, b})
r : ℚ
hr : ↑r = a / b
⊢ (a ∈ range fun x ↦ x • (b / ↑r.den)) ∧ b ∈ range fun x ↦ x • (b / ↑r.den)
Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup

Goal state before:
pp: a b : ℝ
hb : b ≠ 0
h : ¬Dense ↑(AddSubgroup.closure {a, b})
c : ℝ
hc : AddSubgroup.closure {a, b} = AddSubgroup.closure {c}
⊢ {a, b} ⊆ ↑(AddSubgroup.closure {a, b})

Tactic:
]

Goal state after:
a b : ℝ
hb : b ≠ 0
h : ¬Dense ↑(AddSubgroup.closure {a, b})
c : ℝ
hc : AddSubgroup.closure {a, b} = AddSubgroup.closure {c}
⊢ {a, b} ⊆ ↑(AddSubgroup.closure {a, b})
Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal

Goal state before:
pp: case inr
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✝ : a ∉ closure[inst✝⁴] (range fun x ↦ g ^ x)
V : Set G
hV₁ : 1 ∈ V
hVo : IsOpen[inst✝⁴] V
hV : ∀ x ∈ V, ∀ y ∈ V, ∀ (m : ℤ), g ^ m ≠ a * x / y
s : Set G := ⋃ m, g ^ m • V
hso : IsOpen[inst✝⁴] s
hsne : s.Nonempty
hd : ∀ ⦃a_1 : G⦄, a_1 ∈ a • V → a_1 ∉ s
hgs : (fun x ↦ g * x) ⁻¹' s = s
h : μ sᶜ = 0
⊢ a • V ⊆ sᶜ

Tactic:
]

Goal state after:
case inr
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✝ : a ∉ closure[inst✝⁴] (range fun x ↦ g ^ x)
V : Set G
hV₁ : 1 ∈ V
hVo : IsOpen[inst✝⁴] V
hV : ∀ x ∈ V, ∀ y ∈ V, ∀ (m : ℤ), g ^ m ≠ a * x / y
s : Set G := ⋃ m, g ^ m • V
hso : IsOpen[inst✝⁴] s
hsne : s.Nonempty
hd : ∀ ⦃a_1 : G⦄, a_1 ∈ a • V → a_1 ∉ s
hgs : (fun x ↦ g * x) ⁻¹' s = s
h : μ sᶜ = 0
⊢ a • V ⊆ sᶜ
Module: Mathlib.Dynamics.Ergodic.AddCircle

Goal state before:
pp: 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 =ᵐ[μ] s
n : ι → ℕ := addOrderOf ∘ u
hu₂ : Tendsto n l atTop
hT₀ : 0 < T
hT₁ : ENNReal.ofReal T ≠ 0
h : μ s ≠ 0
d : AddCircle T
I : ι → Set (AddCircle T) := fun j ↦ closedBall d (T / (2 * ↑(n j)))
this : ∀ᶠ (j : ι) in l, μ (s ∩ I j) / μ (I j) = μ s / ENNReal.ofReal T
hd : μ s = ENNReal.ofReal T
⊢ μ s = ENNReal.ofReal T

Tactic:
]

Goal state after:
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 =ᵐ[μ] s
n : ι → ℕ := addOrderOf ∘ u
hu₂ : Tendsto n l atTop
hT₀ : 0 < T
hT₁ : ENNReal.ofReal T ≠ 0
h : μ s ≠ 0
d : AddCircle T
I : ι → Set (AddCircle T) := fun j ↦ closedBall d (T / (2 * ↑(n j)))
this : ∀ᶠ (j : ι) in l, μ (s ∩ I j) / μ (I j) = μ s / ENNReal.ofReal T
hd : μ s = ENNReal.ofReal T
⊢ μ s = ENNReal.ofReal T
Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal

Goal state before:
pp: G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : SecondCountableTopology G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : μ.IsMulLeftInvariant
f : G →* G
hf : Dense (⋃ n, (⇑f)^[n] ⁻¹' 1)
s : Set G
hsm : MeasurableSet s
hs : ⇑f ⁻¹' s = s
n : ℕ
x : G
hx : x ∈ (⇑f)^[n] ⁻¹' 1
⊢ s = s

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup

Goal state before:
pp: a p : ℝ
⊢ Dense ↑(AddSubgroup.closure ({a} ∪ {p})) ↔ Dense ↑(AddSubgroup.closure ({a} ∪ {p}))

Tactic:
]

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

Goal state before:
pp: G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : SecondCountableTopology G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : μ.IsMulLeftInvariant
f : G →* G
hf : Dense (⋃ n, (⇑f)^[n] ⁻¹' 1)
s : Set G
hsm : MeasurableSet s
hs : ⇑f ⁻¹' s = s
n : ℕ
x : G
hx : (⇑f)^[n] x = 1
hsn : (⇑f)^[n] ⁻¹' s = s
⊢ x ∈ {g | (fun x ↦ g • x) ⁻¹' s = s}

Tactic:
]

Goal state after:
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : SecondCountableTopology G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : μ.IsMulLeftInvariant
f : G →* G
hf : Dense (⋃ n, (⇑f)^[n] ⁻¹' 1)
s : Set G
hsm : MeasurableSet s
hs : ⇑f ⁻¹' s = s
n : ℕ
x : G
hx : (⇑f)^[n] x = 1
hsn : (⇑f)^[n] ⁻¹' s = s
⊢ x ∈ {g | (fun x ↦ g • x) ⁻¹' s = s}
Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal

Goal state before:
pp: G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : SecondCountableTopology G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : μ.IsMulLeftInvariant
f : G →* G
hf : Dense (⋃ n, (⇑f)^[n] ⁻¹' 1)
s : Set G
hsm : MeasurableSet s
hs : ⇑f ⁻¹' s = s
n : ℕ
x : G
hx : (⇑f)^[n] x = 1
hsn : (⇑f)^[n] ⁻¹' s = s
⊢ (fun x_1 ↦ x • x_1) ⁻¹' (⇑f)^[n] ⁻¹' s = (⇑f)^[n] ⁻¹' s

Tactic:
]

Goal state after:
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : SecondCountableTopology G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : μ.IsMulLeftInvariant
f : G →* G
hf : Dense (⋃ n, (⇑f)^[n] ⁻¹' 1)
s : Set G
hsm : MeasurableSet s
hs : ⇑f ⁻¹' s = s
n : ℕ
x : G
hx : (⇑f)^[n] x = 1
hsn : (⇑f)^[n] ⁻¹' s = s
⊢ (fun x_1 ↦ x • x_1) ⁻¹' (⇑f)^[n] ⁻¹' s = (⇑f)^[n] ⁻¹' s
Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup

Goal state before:
pp: case mp
p : ℝ
inst✝ : Fact (0 < p)
a : AddCircle p
ha : addOrderOf a ≠ 0
hd : addOrderOf a = 0
⊢ False

Tactic:
]

Goal state after:
case mp
p : ℝ
inst✝ : Fact (0 < p)
a : AddCircle p
ha : addOrderOf a ≠ 0
hd : addOrderOf a = 0
⊢ False
Module: Mathlib.Topology.Instances.AddCircle.DenseSubgroup

Goal state before:
pp: p : ℝ
inst✝ : Fact (0 < p)
s : AddSubgroup (AddCircle p)
h : ∃ a, AddSubgroup.comap (QuotientAddGroup.mk' (AddSubgroup.zmultiples p)) s = AddSubgroup.zmultiples a
⊢ ∃ a, s = AddSubgroup.zmultiples a

Tactic:
]

Goal state after:
p : ℝ
inst✝ : Fact (0 < p)
s : AddSubgroup (AddCircle p)
h : ∃ a, AddSubgroup.comap (QuotientAddGroup.mk' (AddSubgroup.zmultiples p)) s = AddSubgroup.zmultiples a
⊢ ∃ a, s = AddSubgroup.zmultiples a