mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ x ∈ {x | p.mulOccursInAt x g} → x ∈ cylinder (Finset.image (fun x ↦ g * x) p.support) (p.mulShift g)

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
⊢ x ∈ cylinder (Finset.image (fun x ↦ g * x) p.support) (p.mulShift g) → x ∈ {x | p.mulOccursInAt x g}

Tactic:
·

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
⊢ x ∈ {x | p.mulOccursInAt x g} → x ∈ cylinder (Finset.image (fun x ↦ g * x) p.support) (p.mulShift g)
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: case mp
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
y : β
⊢ (∀ i ∈ f, ∀ t ∈ 𝓝 y, (t ∩ image2 ϕ i s).Nonempty) →
    ∀ n ∈ 𝓝 y, ∀ {U : Set τ}, U ∈ f → ∃ x ∈ U, (s ∩ ϕ x ⁻¹' n).Nonempty

pp: case mpr
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
y : β
⊢ (∀ n ∈ 𝓝 y, ∀ {U : Set τ}, U ∈ f → ∃ x ∈ U, (s ∩ ϕ x ⁻¹' n).Nonempty) →
    ∀ i ∈ f, ∀ t ∈ 𝓝 y, (t ∩ image2 ϕ i s).Nonempty

Tactic:
·

Goal state after:
case mp
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
y : β
⊢ (∀ i ∈ f, ∀ t ∈ 𝓝 y, (t ∩ image2 ϕ i s).Nonempty) →
    ∀ n ∈ 𝓝 y, ∀ {U : Set τ}, U ∈ f → ∃ x ∈ U, (s ∩ ϕ x ⁻¹' n).Nonempty
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
⊢ x ∈ cylinder (Finset.image (fun x ↦ g * x) p.support) (p.mulShift g) → x ∈ {x | p.mulOccursInAt x g}

Tactic:
·

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
⊢ x ∈ cylinder (Finset.image (fun x ↦ g * x) p.support) (p.mulShift g) → x ∈ {x | p.mulOccursInAt x g}
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
this : SigmaFinite (ν.withDensity f)
s : Set α
hs : MeasurableSet s
⊢ ∀ᵐ (x : α) ∂ν.restrict s, f x < ∞

pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
this : SigmaFinite (ν.withDensity f)
s : Set α
hs : MeasurableSet s
⊢ AEMeasurable f (ν.restrict s)

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
this : SigmaFinite (ν.withDensity f)
s : Set α
hs : MeasurableSet s
⊢ ∀ᵐ (x : α) ∂ν.restrict s, f x < ∞
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
this : SigmaFinite (ν.withDensity f)
s : Set α
hs : MeasurableSet s
⊢ AEMeasurable f (ν.restrict s)

Tactic:
·

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
this : SigmaFinite (ν.withDensity f)
s : Set α
hs : MeasurableSet s
⊢ AEMeasurable f (ν.restrict s)
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: case mpr
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
y : β
⊢ (∀ n ∈ 𝓝 y, ∀ {U : Set τ}, U ∈ f → ∃ x ∈ U, (s ∩ ϕ x ⁻¹' n).Nonempty) →
    ∀ i ∈ f, ∀ t ∈ 𝓝 y, (t ∩ image2 ϕ i s).Nonempty

Tactic:
·

Goal state after:
case mpr
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
y : β
⊢ (∀ n ∈ 𝓝 y, ∀ {U : Set τ}, U ∈ f → ∃ x ∈ U, (s ∩ ϕ x ⁻¹' n).Nonempty) →
    ∀ i ∈ f, ∀ t ∈ 𝓝 y, (t ∩ image2 ϕ i s).Nonempty
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: case mp
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s₁ s₂ : Set α
y : β
⊢ y ∈ ω f ϕ (s₁ ∪ s₂) → y ∈ ω f ϕ s₁ ∪ ω f ϕ s₂

pp: case mpr
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s₁ s₂ : Set α
y : β
⊢ y ∈ ω f ϕ s₁ ∪ ω f ϕ s₂ → y ∈ ω f ϕ (s₁ ∪ s₂)

Tactic:
·

Goal state after:
case mp
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s₁ s₂ : Set α
y : β
⊢ y ∈ ω f ϕ (s₁ ∪ s₂) → y ∈ ω f ϕ s₁ ∪ ω f ϕ s₂
Module: Mathlib.Dynamics.SymbolicDynamics.Basic

Goal state before:
pp: case pos
A : Type u_3
G : Type u_4
inst✝¹ : Finite A
inst✝ : Inhabited A
val✝ : Fintype A
cfg : G → A
dom : Finset G
cond : ∀ g ∉ dom, cfg g = default
g : G
hg : g ∈ dom
⊢ (if h : g ∈ dom then cfg g else default) = cfg g

pp: case neg
A : Type u_3
G : Type u_4
inst✝¹ : Finite A
inst✝ : Inhabited A
val✝ : Fintype A
cfg : G → A
dom : Finset G
cond : ∀ g ∉ dom, cfg g = default
g : G
hg : g ∉ dom
⊢ (if h : g ∈ dom then cfg g else default) = cfg g

Tactic:
·

Goal state after:
case pos
A : Type u_3
G : Type u_4
inst✝¹ : Finite A
inst✝ : Inhabited A
val✝ : Fintype A
cfg : G → A
dom : Finset G
cond : ∀ g ∉ dom, cfg g = default
g : G
hg : g ∈ dom
⊢ (if h : g ∈ dom then cfg g else default) = cfg g
Module: Mathlib.Dynamics.SymbolicDynamics.Basic

Goal state before:
pp: case neg
A : Type u_3
G : Type u_4
inst✝¹ : Finite A
inst✝ : Inhabited A
val✝ : Fintype A
cfg : G → A
dom : Finset G
cond : ∀ g ∉ dom, cfg g = default
g : G
hg : g ∉ dom
⊢ (if h : g ∈ dom then cfg g else default) = cfg g

Tactic:
·

Goal state after:
case neg
A : Type u_3
G : Type u_4
inst✝¹ : Finite A
inst✝ : Inhabited A
val✝ : Fintype A
cfg : G → A
dom : Finset G
cond : ∀ g ∉ dom, cfg g = default
g : G
hg : g ∉ dom
⊢ (if h : g ∈ dom then cfg g else default) = cfg g
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: case mp
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s₁ s₂ : Set α
y : β
n₁ : Set β
hn₁ : n₁ ∈ 𝓝 y
h₁ : ∀ᶠ (x : τ) in f, s₁ ∩ ϕ x ⁻¹' n₁ ⊆ ∅
n₂ : Set β
hn₂ : n₂ ∈ 𝓝 y
h₂ : ∀ᶠ (x : τ) in f, s₂ ∩ ϕ x ⁻¹' n₂ ⊆ ∅
⊢ ∃ n ∈ 𝓝 y, (∀ᶠ (x : τ) in f, s₁ ∩ ϕ x ⁻¹' n ⊆ ∅) ∧ ∀ᶠ (x : τ) in f, s₂ ∩ ϕ x ⁻¹' n ⊆ ∅

Tactic:
refine ⟨n₁ ∩ n₂, inter_mem hn₁ hn₂, h₁.mono fun t ↦ ?_, h₂.mono fun t ↦ ?_⟩

Goal state after:
case mp.refine_1
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s₁ s₂ : Set α
y : β
n₁ : Set β
hn₁ : n₁ ∈ 𝓝 y
h₁ : ∀ᶠ (x : τ) in f, s₁ ∩ ϕ x ⁻¹' n₁ ⊆ ∅
n₂ : Set β
hn₂ : n₂ ∈ 𝓝 y
h₂ : ∀ᶠ (x : τ) in f, s₂ ∩ ϕ x ⁻¹' n₂ ⊆ ∅
t : τ
⊢ s₁ ∩ ϕ t ⁻¹' n₁ ⊆ ∅ → s₁ ∩ ϕ t ⁻¹' (n₁ ∩ n₂) ⊆ ∅

case mp.refine_2
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s₁ s₂ : Set α
y : β
n₁ : Set β
hn₁ : n₁ ∈ 𝓝 y
h₁ : ∀ᶠ (x : τ) in f, s₁ ∩ ϕ x ⁻¹' n₁ ⊆ ∅
n₂ : Set β
hn₂ : n₂ ∈ 𝓝 y
h₂ : ∀ᶠ (x : τ) in f, s₂ ∩ ϕ x ⁻¹' n₂ ⊆ ∅
t : τ
⊢ s₂ ∩ ϕ t ⁻¹' n₂ ⊆ ∅ → s₂ ∩ ϕ t ⁻¹' (n₁ ∩ n₂) ⊆ ∅
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: case mpr
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s₁ s₂ : Set α
y : β
⊢ y ∈ ω f ϕ s₁ ∪ ω f ϕ s₂ → y ∈ ω f ϕ (s₁ ∪ s₂)

Tactic:
·

Goal state after:
case mpr
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s₁ s₂ : Set α
y : β
⊢ y ∈ ω f ϕ s₁ ∪ ω f ϕ s₂ → y ∈ ω f ϕ (s₁ ∪ s₂)
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: case inl
X : Type u_1
T : X → X
U : SetRel X X
m : ℕ
inst✝ : U.IsSymm
n : ℕ
s : Finset X
F_inv : MapsTo T ∅ ∅
h : IsDynCoverOf T ∅ U m ↑s
⊢ ∃ t, IsDynCoverOf T ∅ (U ○ U) (m * n) ↑t ∧ #t ≤ #s ^ n

pp: case inr
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
m : ℕ
F_inv : MapsTo T F F
inst✝ : U.IsSymm
n : ℕ
s : Finset X
h : IsDynCoverOf T F U m ↑s
F_nemp : F.Nonempty
⊢ ∃ t, IsDynCoverOf T F (U ○ U) (m * n) ↑t ∧ #t ≤ #s ^ n

Tactic:
·

Goal state after:
case inl
X : Type u_1
T : X → X
U : SetRel X X
m : ℕ
inst✝ : U.IsSymm
n : ℕ
s : Finset X
F_inv : MapsTo T ∅ ∅
h : IsDynCoverOf T ∅ U m ↑s
⊢ ∃ t, IsDynCoverOf T ∅ (U ○ U) (m * n) ↑t ∧ #t ≤ #s ^ n
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: case inr.inl
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
F_inv : MapsTo T F F
inst✝ : U.IsSymm
n : ℕ
s : Finset X
x✝ : Nonempty X
s_nemp : (↑s).Nonempty
x : X
x_F : x ∈ F
h : IsDynCoverOf T F U 0 ↑s
⊢ ∃ t, IsDynCoverOf T F (U ○ U) (0 * n) ↑t ∧ #t ≤ #s ^ n

pp: case inr.inr
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
m : ℕ
F_inv : MapsTo T F F
inst✝ : U.IsSymm
n : ℕ
s : Finset X
h : IsDynCoverOf T F U m ↑s
x✝ : Nonempty X
s_nemp : (↑s).Nonempty
x : X
x_F : x ∈ F
m_pos : m > 0
⊢ ∃ t, IsDynCoverOf T F (U ○ U) (m * n) ↑t ∧ #t ≤ #s ^ n

Tactic:
·

Goal state after:
case inr.inl
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
F_inv : MapsTo T F F
inst✝ : U.IsSymm
n : ℕ
s : Finset X
x✝ : Nonempty X
s_nemp : (↑s).Nonempty
x : X
x_F : x ∈ F
h : IsDynCoverOf T F U 0 ↑s
⊢ ∃ t, IsDynCoverOf T F (U ○ U) (0 * n) ↑t ∧ #t ≤ #s ^ n
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: case inl
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
m : ℕ
F_inv : MapsTo T F F
inst✝ : U.IsSymm
n : ℕ
s : Finset X
h : IsDynCoverOf T F U m ↑s
x✝ : Nonempty X
s_nemp : (↑s).Nonempty
x : X
x_F : x ∈ F
m_pos : m > 0
t : Fin n → ↥s
inter_empt : ⋂ k, T^[m * ↑k] ⁻¹' ball (↑(t k)) (dynEntourage T U m) = ∅
⊢ ∃ y, ⋂ k, T^[m * ↑k] ⁻¹' ball (↑(t k)) (dynEntourage T U m) ⊆ ball y (dynEntourage T (U ○ U) (m * n))

pp: case inr
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
m : ℕ
F_inv : MapsTo T F F
inst✝ : U.IsSymm
n : ℕ
s : Finset X
h : IsDynCoverOf T F U m ↑s
x✝ : Nonempty X
s_nemp : (↑s).Nonempty
x : X
x_F : x ∈ F
m_pos : m > 0
t : Fin n → ↥s
inter_nemp : (⋂ k, T^[m * ↑k] ⁻¹' ball (↑(t k)) (dynEntourage T U m)).Nonempty
⊢ ∃ y, ⋂ k, T^[m * ↑k] ⁻¹' ball (↑(t k)) (dynEntourage T U m) ⊆ ball y (dynEntourage T (U ○ U) (m * n))

Tactic:
·

Goal state after:
case inl
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
m : ℕ
F_inv : MapsTo T F F
inst✝ : U.IsSymm
n : ℕ
s : Finset X
h : IsDynCoverOf T F U m ↑s
x✝ : Nonempty X
s_nemp : (↑s).Nonempty
x : X
x_F : x ∈ F
m_pos : m > 0
t : Fin n → ↥s
inter_empt : ⋂ k, T^[m * ↑k] ⁻¹' ball (↑(t k)) (dynEntourage T U m) = ∅
⊢ ∃ y, ⋂ k, T^[m * ↑k] ⁻¹' ball (↑(t k)) (dynEntourage T U m) ⊆ ball y (dynEntourage T (U ○ U) (m * n))
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: case inr
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
m : ℕ
F_inv : MapsTo T F F
inst✝ : U.IsSymm
n : ℕ
s : Finset X
h : IsDynCoverOf T F U m ↑s
x✝ : Nonempty X
s_nemp : (↑s).Nonempty
x : X
x_F : x ∈ F
m_pos : m > 0
t : Fin n → ↥s
inter_nemp : (⋂ k, T^[m * ↑k] ⁻¹' ball (↑(t k)) (dynEntourage T U m)).Nonempty
⊢ ∃ y, ⋂ k, T^[m * ↑k] ⁻¹' ball (↑(t k)) (dynEntourage T U m) ⊆ ball y (dynEntourage T (U ○ U) (m * n))

Tactic:
·

Goal state after:
case inr
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
m : ℕ
F_inv : MapsTo T F F
inst✝ : U.IsSymm
n : ℕ
s : Finset X
h : IsDynCoverOf T F U m ↑s
x✝ : Nonempty X
s_nemp : (↑s).Nonempty
x : X
x_F : x ∈ F
m_pos : m > 0
t : Fin n → ↥s
inter_nemp : (⋂ k, T^[m * ↑k] ⁻¹' ball (↑(t k)) (dynEntourage T U m)).Nonempty
⊢ ∃ y, ⋂ k, T^[m * ↑k] ⁻¹' ball (↑(t k)) (dynEntourage T U m) ⊆ ball y (dynEntourage T (U ○ U) (m * n))
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: case inr.inr.refine_1
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
m : ℕ
F_inv : MapsTo T F F
inst✝ : U.IsSymm
n : ℕ
s : Finset X
h : IsDynCoverOf T F U m ↑s
x✝ : Nonempty X
s_nemp : (↑s).Nonempty
x : X
x_F : x ∈ F
m_pos : m > 0
dyncover : (Fin n → ↥s) → X
h_dyncover :
  ∀ (t : Fin n → ↥s),
    ⋂ k, T^[m * ↑k] ⁻¹' ball (↑(t k)) (dynEntourage T U m) ⊆ ball (dyncover t) (dynEntourage T (U ○ U) (m * n))
sn : Set X := range dyncover
⊢ IsDynCoverOf T F (U ○ U) (m * n) ↑sn.toFinset

pp: case inr.inr.refine_2
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
m : ℕ
F_inv : MapsTo T F F
inst✝ : U.IsSymm
n : ℕ
s : Finset X
h : IsDynCoverOf T F U m ↑s
x✝ : Nonempty X
s_nemp : (↑s).Nonempty
x : X
x_F : x ∈ F
m_pos : m > 0
dyncover : (Fin n → ↥s) → X
h_dyncover :
  ∀ (t : Fin n → ↥s),
    ⋂ k, T^[m * ↑k] ⁻¹' ball (↑(t k)) (dynEntourage T U m) ⊆ ball (dyncover t) (dynEntourage T (U ○ U) (m * n))
sn : Set X := range dyncover
⊢ #sn.toFinset ≤ #s ^ n

Tactic:
·

Goal state after:
case inr.inr.refine_1
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
m : ℕ
F_inv : MapsTo T F F
inst✝ : U.IsSymm
n : ℕ
s : Finset X
h : IsDynCoverOf T F U m ↑s
x✝ : Nonempty X
s_nemp : (↑s).Nonempty
x : X
x_F : x ∈ F
m_pos : m > 0
dyncover : (Fin n → ↥s) → X
h_dyncover :
  ∀ (t : Fin n → ↥s),
    ⋂ k, T^[m * ↑k] ⁻¹' ball (↑(t k)) (dynEntourage T U m) ⊆ ball (dyncover t) (dynEntourage T (U ○ U) (m * n))
sn : Set X := range dyncover
⊢ IsDynCoverOf T F (U ○ U) (m * n) ↑sn.toFinset
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: case htd
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : f.NeBot
c : Set β
hc₁ : IsCompact c
hs : s.Nonempty
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst✝¹] (image2 ϕ v s) ⊆ c
⊢ Directed (fun x1 x2 ↦ x1 ⊇ x2) fun i ↦ closure[inst✝¹] (image2 ϕ (↑i ∩ v) s)

pp: case htn
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : f.NeBot
c : Set β
hc₁ : IsCompact c
hs : s.Nonempty
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst✝¹] (image2 ϕ v s) ⊆ c
⊢ ∀ (i : ↑f.sets), (closure[inst✝¹] (image2 ϕ (↑i ∩ v) s)).Nonempty

pp: case htc
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : f.NeBot
c : Set β
hc₁ : IsCompact c
hs : s.Nonempty
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst✝¹] (image2 ϕ v s) ⊆ c
⊢ ∀ (i : ↑f.sets), IsCompact (closure[inst✝¹] (image2 ϕ (↑i ∩ v) s))

pp: case htcl
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : f.NeBot
c : Set β
hc₁ : IsCompact c
hs : s.Nonempty
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst✝¹] (image2 ϕ v s) ⊆ c
⊢ ∀ (i : ↑f.sets), IsClosed[inst✝¹] (closure[inst✝¹] (image2 ϕ (↑i ∩ v) s))

Tactic:
·

Goal state after:
case htd
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : f.NeBot
c : Set β
hc₁ : IsCompact c
hs : s.Nonempty
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst✝¹] (image2 ϕ v s) ⊆ c
⊢ Directed (fun x1 x2 ↦ x1 ⊇ x2) fun i ↦ closure[inst✝¹] (image2 ϕ (↑i ∩ v) s)
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
pp: case mp
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : netMaxcard T F U n < ⊤
⊢ ∃ s, IsDynNetIn T F U n ↑s ∧ ↑s.card = netMaxcard T F U n

pp: case mpr
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : ∃ s, IsDynNetIn T F U n ↑s ∧ ↑s.card = netMaxcard T F U n
⊢ netMaxcard T F U n < ⊤

Tactic:
·

Goal state after:
case mp
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : netMaxcard T F U n < ⊤
⊢ ∃ s, IsDynNetIn T F U n ↑s ∧ ↑s.card = netMaxcard T F U n
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: case refine_2
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᵐ[ν + ν']
    (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')
h₂ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᵐ[ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
h₃ : (μ.singularPart ν').rnDeriv (ν + ν') =ᵐ[ν] (μ.singularPart ν').rnDeriv ν
⊢ (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᵐ[ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν

pp: case refine_1
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᵐ[ν + ν']
    (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')
h₂ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᵐ[ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
⊢ μ.singularPart ν' ⟂ₘ ν'

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᵐ[ν + ν']
    (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')
h₂ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᵐ[ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
h₃ : (μ.singularPart ν').rnDeriv (ν + ν') =ᵐ[ν] (μ.singularPart ν').rnDeriv ν
⊢ (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᵐ[ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: case inr.inr.refine_2
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
m : ℕ
F_inv : MapsTo T F F
inst✝ : U.IsSymm
n : ℕ
s : Finset X
h : IsDynCoverOf T F U m ↑s
x✝ : Nonempty X
s_nemp : (↑s).Nonempty
x : X
x_F : x ∈ F
m_pos : m > 0
dyncover : (Fin n → ↥s) → X
h_dyncover :
  ∀ (t : Fin n → ↥s),
    ⋂ k, T^[m * ↑k] ⁻¹' ball (↑(t k)) (dynEntourage T U m) ⊆ ball (dyncover t) (dynEntourage T (U ○ U) (m * n))
sn : Set X := range dyncover
⊢ #sn.toFinset ≤ #s ^ n

Tactic:
·

Goal state after:
case inr.inr.refine_2
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
m : ℕ
F_inv : MapsTo T F F
inst✝ : U.IsSymm
n : ℕ
s : Finset X
h : IsDynCoverOf T F U m ↑s
x✝ : Nonempty X
s_nemp : (↑s).Nonempty
x : X
x_F : x ∈ F
m_pos : m > 0
dyncover : (Fin n → ↥s) → X
h_dyncover :
  ∀ (t : Fin n → ↥s),
    ⋂ k, T^[m * ↑k] ⁻¹' ball (↑(t k)) (dynEntourage T U m) ⊆ ball (dyncover t) (dynEntourage T (U ○ U) (m * n))
sn : Set X := range dyncover
⊢ #sn.toFinset ≤ #s ^ n
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: case htn
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : f.NeBot
c : Set β
hc₁ : IsCompact c
hs : s.Nonempty
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst✝¹] (image2 ϕ v s) ⊆ c
⊢ ∀ (i : ↑f.sets), (closure[inst✝¹] (image2 ϕ (↑i ∩ v) s)).Nonempty

pp: case htc
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : f.NeBot
c : Set β
hc₁ : IsCompact c
hs : s.Nonempty
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst✝¹] (image2 ϕ v s) ⊆ c
⊢ ∀ (i : ↑f.sets), IsCompact (closure[inst✝¹] (image2 ϕ (↑i ∩ v) s))

pp: case htcl
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : f.NeBot
c : Set β
hc₁ : IsCompact c
hs : s.Nonempty
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst✝¹] (image2 ϕ v s) ⊆ c
⊢ ∀ (i : ↑f.sets), IsClosed[inst✝¹] (closure[inst✝¹] (image2 ϕ (↑i ∩ v) s))

Tactic:
·

Goal state after:
case htn
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : f.NeBot
c : Set β
hc₁ : IsCompact c
hs : s.Nonempty
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst✝¹] (image2 ϕ v s) ⊆ c
⊢ ∀ (i : ↑f.sets), (closure[inst✝¹] (image2 ϕ (↑i ∩ v) s)).Nonempty
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
pp: X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : netMaxcard T F U n < ⊤
k : ℕ
k_max : ↑k = sSup (WithTop.some '' Finset.card '' {s | IsDynNetIn T F U n ↑s})
this : netMaxcard T F U n = sSup (WithTop.some '' Finset.card '' {s | IsDynNetIn T F U n ↑s})
⊢ ∀ (a : Finset X), IsDynNetIn T F U n ↑a → a.card ≤ k

Tactic:
intro s h

Goal state after:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h✝ : netMaxcard T F U n < ⊤
k : ℕ
k_max : ↑k = sSup (WithTop.some '' Finset.card '' {s | IsDynNetIn T F U n ↑s})
this : netMaxcard T F U n = sSup (WithTop.some '' Finset.card '' {s | IsDynNetIn T F U n ↑s})
s : Finset X
h : IsDynNetIn T F U n ↑s
⊢ s.card ≤ k
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: case htc
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : f.NeBot
c : Set β
hc₁ : IsCompact c
hs : s.Nonempty
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst✝¹] (image2 ϕ v s) ⊆ c
⊢ ∀ (i : ↑f.sets), IsCompact (closure[inst✝¹] (image2 ϕ (↑i ∩ v) s))

pp: case htcl
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : f.NeBot
c : Set β
hc₁ : IsCompact c
hs : s.Nonempty
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst✝¹] (image2 ϕ v s) ⊆ c
⊢ ∀ (i : ↑f.sets), IsClosed[inst✝¹] (closure[inst✝¹] (image2 ϕ (↑i ∩ v) s))

Tactic:
·

Goal state after:
case htc
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : f.NeBot
c : Set β
hc₁ : IsCompact c
hs : s.Nonempty
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst✝¹] (image2 ϕ v s) ⊆ c
⊢ ∀ (i : ↑f.sets), IsCompact (closure[inst✝¹] (image2 ϕ (↑i ∩ v) s))
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: case htcl
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : f.NeBot
c : Set β
hc₁ : IsCompact c
hs : s.Nonempty
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst✝¹] (image2 ϕ v s) ⊆ c
⊢ ∀ (i : ↑f.sets), IsClosed[inst✝¹] (closure[inst✝¹] (image2 ϕ (↑i ∩ v) s))

Tactic:
·

Goal state after:
case htcl
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
inst✝ : f.NeBot
c : Set β
hc₁ : IsCompact c
hs : s.Nonempty
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst✝¹] (image2 ϕ v s) ⊆ c
⊢ ∀ (i : ↑f.sets), IsClosed[inst✝¹] (closure[inst✝¹] (image2 ϕ (↑i ∩ v) s))
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
pp: case mpr
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : ∃ s, IsDynNetIn T F U n ↑s ∧ ↑s.card = netMaxcard T F U n
⊢ netMaxcard T F U n < ⊤

Tactic:
·

Goal state after:
case mpr
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h : ∃ s, IsDynNetIn T F U n ↑s ∧ ↑s.card = netMaxcard T F U n
⊢ netMaxcard T F U n < ⊤
Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj

Goal state before:
pp: case inl
X : Type u_1
Y : Type u_2
F : Set X
V : SetRel Y Y
S : X → X
T : Y → Y
φ : X → Y
n : ℕ
h : Semiconj φ S T
inst✝ : V.IsSymm
t : Finset Y
h' : IsDynCoverOf T (φ '' F) V n ↑t
h✝ : IsEmpty X
⊢ ∃ s, IsDynCoverOf S F (map φ φ ⁻¹' (V ○ V)) n ↑s ∧ s.card ≤ t.card

pp: case inr
X : Type u_1
Y : Type u_2
F : Set X
V : SetRel Y Y
S : X → X
T : Y → Y
φ : X → Y
n : ℕ
h : Semiconj φ S T
inst✝ : V.IsSymm
t : Finset Y
h' : IsDynCoverOf T (φ '' F) V n ↑t
h✝ : Nonempty X
⊢ ∃ s, IsDynCoverOf S F (map φ φ ⁻¹' (V ○ V)) n ↑s ∧ s.card ≤ t.card

Tactic:
·

Goal state after:
case inl
X : Type u_1
Y : Type u_2
F : Set X
V : SetRel Y Y
S : X → X
T : Y → Y
φ : X → Y
n : ℕ
h : Semiconj φ S T
inst✝ : V.IsSymm
t : Finset Y
h' : IsDynCoverOf T (φ '' F) V n ↑t
h✝ : IsEmpty X
⊢ ∃ s, IsDynCoverOf S F (map φ φ ⁻¹' (V ○ V)) n ↑s ∧ s.card ≤ t.card