mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
μ' : Measure α := ν.withDensity (μ.rnDeriv ν)
h₁ : μ'.rnDeriv (ν.withDensity f) =ᵐ[ν] μ.rnDeriv (ν.withDensity f)
h₂ : μ.rnDeriv ν =ᵐ[ν] μ'.rnDeriv ν
hμ' :
  (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) =ᵐ[ν] fun x ↦
    (f x)⁻¹ * (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν x
x : α
hx₁ : μ'.rnDeriv (ν.withDensity f) x = μ.rnDeriv (ν.withDensity f) x
hx₂ : μ.rnDeriv ν x = μ'.rnDeriv ν x
hx_eq : (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) x = (f x)⁻¹ * (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν x
⊢ (f x)⁻¹ * (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν x = (f x)⁻¹ * μ'.rnDeriv ν x

Tactic:
]

Goal state after:
Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage

Goal state before:
pp: X : Type u_1
U : SetRel X X
inst✝ : TopologicalSpace X
T : X → X
T_cont : Continuous[inst✝, inst✝] T
U_open : IsOpen[instTopologicalSpaceProd] U
n : ℕ
⊢ IsOpen[instTopologicalSpaceProd] (⋂ k, (map T T)^[↑k] ⁻¹' U)

Tactic:
]

Goal state after:
X : Type u_1
U : SetRel X X
inst✝ : TopologicalSpace X
T : X → X
T_cont : Continuous[inst✝, inst✝] T
U_open : IsOpen[instTopologicalSpaceProd] U
n : ℕ
⊢ IsOpen[instTopologicalSpaceProd] (⋂ k, (map T T)^[↑k] ⁻¹' U)
Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage

Goal state before:
pp: X : Type u_1
T : X → X
n : ℕ
U : SetRel X X
inst✝ : U.IsSymm
x y z : X
z_Bx : x ∈ ball z (dynEntourage T U n)
z_By : z ∈ ball y (dynEntourage T U n)
⊢ x ∈ ball y (dynEntourage T (U ○ U) n)

Tactic:
]

Goal state after:
X : Type u_1
T : X → X
n : ℕ
U : SetRel X X
inst✝ : U.IsSymm
x y z : X
z_Bx : x ∈ ball z (dynEntourage T U n)
z_By : z ∈ ball y (dynEntourage T U n)
⊢ x ∈ ball y (dynEntourage T (U ○ U) n)
Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage

Goal state before:
pp: X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Function.Semiconj φ S T
U : Set (Y × Y)
n : ℕ
⊢ ⋂ i, ⋂ (_ : i < n), map φ φ ⁻¹' (map T T)^[i] ⁻¹' U = dynEntourage S (map φ φ ⁻¹' U) n

Tactic:
]

Goal state after:
X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Function.Semiconj φ S T
U : Set (Y × Y)
n : ℕ
⊢ ⋂ i, ⋂ (_ : i < n), map φ φ ⁻¹' (map T T)^[i] ⁻¹' U = dynEntourage S (map φ φ ⁻¹' U) n
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
p : ι → Set α
⊢ ∀ (i : ι), ω f ϕ (p i) ⊆ ω f ϕ (⋃ i, p i)

Tactic:
]

Goal state after:
τ : Type u_1
α : Type u_2
β : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
p : ι → Set α
⊢ ∀ (i : ι), ω f ϕ (p i) ⊆ ω f ϕ (⋃ i, p i)
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν'
inst✝ : SigmaFinite ν'
h✝ : μ ⟂ₘ ν
hνν' : ν ≪ ν'
t : Set α := h✝.nullSet
ht : MeasurableSet t
h : (μ.restrict t).rnDeriv ν' =ᵐ[ν] t.indicator (μ.rnDeriv ν')
⊢ ∀ᵐ (x : α) ∂ν, x ∈ t → μ.rnDeriv ν' x = (μ.restrict t).rnDeriv ν' x

Tactic:
]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν'
inst✝ : SigmaFinite ν'
h✝ : μ ⟂ₘ ν
hνν' : ν ≪ ν'
t : Set α := h✝.nullSet
ht : MeasurableSet t
h : (μ.restrict t).rnDeriv ν' =ᵐ[ν] t.indicator (μ.rnDeriv ν')
⊢ ∀ᵐ (x : α) ∂ν, x ∈ t → μ.rnDeriv ν' x = (μ.restrict t).rnDeriv ν' x
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
v : Set τ
hv : v ∈ f
⊢ ⋂ u ∈ f, closure[inst✝] (image2 ϕ (u ∩ v) s) = ⋂ u, closure[inst✝] (image2 ϕ (↑u ∩ v) s)

Tactic:
]

Goal state after:
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
v : Set τ
hv : v ∈ f
⊢ ⋂ u ∈ f, closure[inst✝] (image2 ϕ (u ∩ v) s) = ⋂ u, closure[inst✝] (image2 ϕ (↑u ∩ v) s)
Module: Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage

Goal state before:
pp: X : Type u_1
Y : Type u_2
S : X → X
T : Y → Y
φ : X → Y
h : Function.Semiconj φ S T
U : Set (Y × Y)
n k : ℕ
x✝ : k < n
⊢ map (T^[k] ∘ φ) (T^[k] ∘ φ) ⁻¹' U = map (T^[k] ∘ φ) (T^[k] ∘ φ) ⁻¹' U

Tactic:
]

Goal state after:
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
u : Set τ
hu : u ∈ f
⊢ ⋂ u, closure[inst✝] (image2 ϕ (↑u) s) ⊆ closure[inst✝] (image2 ϕ u s)

Tactic:
]

Goal state after:
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
u : Set τ
hu : u ∈ f
⊢ ⋂ u, closure[inst✝] (image2 ϕ (↑u) s) ⊆ closure[inst✝] (image2 ϕ u s)
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν'
inst✝ : SigmaFinite ν'
h✝ : μ ⟂ₘ ν
hνν' : ν ≪ ν'
t : Set α := h✝.nullSet
ht : MeasurableSet t
h : (μ.restrict t).rnDeriv ν' =ᵐ[ν] t.indicator (μ.rnDeriv ν')
x : α
hx : (μ.restrict t).rnDeriv ν' x = t.indicator (μ.rnDeriv ν') x
hxt : x ∈ t
⊢ μ.rnDeriv ν' x = μ.rnDeriv ν' x

Tactic:
]

Goal state after:
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
u : Set τ
hu : u ∈ f
a✝ : β
hx : ∀ (i : ↑f.sets), a✝ ∈ closure[inst✝] (image2 ϕ (↑i) s)
⊢ a✝ ∈ closure[inst✝] (image2 ϕ u s)

Tactic:
]

Goal state after:
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
u : Set τ
hu : u ∈ f
a✝ : β
hx : ∀ (i : ↑f.sets), a✝ ∈ closure[inst✝] (image2 ϕ (↑i) s)
⊢ a✝ ∈ closure[inst✝] (image2 ϕ u s)
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝² : μ.HaveLebesgueDecomposition ν
inst✝¹ : μ.HaveLebesgueDecomposition (ν + ν')
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hνν' : ν ⟂ₘ ν'
t : Set α := hνν'.nullSet
ht : MeasurableSet t
⊢ (ν.restrict tᶜ).withDensity (μ.rnDeriv (ν + ν')) = (ν.restrict tᶜ).withDensity (μ.rnDeriv ν)

Tactic:
]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝² : μ.HaveLebesgueDecomposition ν
inst✝¹ : μ.HaveLebesgueDecomposition (ν + ν')
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hνν' : ν ⟂ₘ ν'
t : Set α := hνν'.nullSet
ht : MeasurableSet t
⊢ (ν.restrict tᶜ).withDensity (μ.rnDeriv (ν + ν')) = (ν.restrict tᶜ).withDensity (μ.rnDeriv ν)
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen[inst✝] n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst✝] (image2 ϕ v s) ⊆ c
k : Set β := closure[inst✝] (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u ↦ (closure[inst✝] (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ u ∈ f, IsOpen[inst✝] (j u)
this : ⋃ u ∈ f, j u = ⋃ u, j ↑u
⊢ ⋂ i, k \ j ↑i ⊆ n

Tactic:
]

Goal state after:
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen[inst✝] n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst✝] (image2 ϕ v s) ⊆ c
k : Set β := closure[inst✝] (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u ↦ (closure[inst✝] (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ u ∈ f, IsOpen[inst✝] (j u)
this : ⋃ u ∈ f, j u = ⋃ u, j ↑u
⊢ ⋂ i, k \ j ↑i ⊆ n
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen[inst✝] n
v : Set τ
hn₂ : ⋂ u, closure[inst✝] (image2 ϕ (↑u ∩ v) s) ⊆ n
hv₁ : v ∈ f
hv₂ : closure[inst✝] (image2 ϕ v s) ⊆ c
k : Set β := closure[inst✝] (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u ↦ (closure[inst✝] (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ u ∈ f, IsOpen[inst✝] (j u)
this : ⋃ u ∈ f, j u = ⋃ u, j ↑u
⊢ ⋂ i, k \ j ↑i ⊆ n

Tactic:
]

Goal state after:
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen[inst✝] n
v : Set τ
hn₂ : ⋂ u, closure[inst✝] (image2 ϕ (↑u ∩ v) s) ⊆ n
hv₁ : v ∈ f
hv₂ : closure[inst✝] (image2 ϕ v s) ⊆ c
k : Set β := closure[inst✝] (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u ↦ (closure[inst✝] (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ u ∈ f, IsOpen[inst✝] (j u)
this : ⋃ u ∈ f, j u = ⋃ u, j ↑u
⊢ ⋂ i, k \ j ↑i ⊆ n
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝² : μ.HaveLebesgueDecomposition ν
inst✝¹ : μ.HaveLebesgueDecomposition (ν + ν')
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hνν' : ν ⟂ₘ ν'
t : Set α := hνν'.nullSet
ht : MeasurableSet t
this : (ν.restrict tᶜ).withDensity (μ.rnDeriv (ν + ν')) = ((ν + ν').restrict tᶜ).withDensity (μ.rnDeriv (ν + ν'))
⊢ μ.restrict tᶜ = μ.restrict tᶜ

Tactic:
]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

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

Tactic:
]

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

Goal state before:
pp: τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen[inst✝] n
v : Set τ
hn₂ : ⋂ u, closure[inst✝] (image2 ϕ (↑u ∩ v) s) ⊆ n
hv₁ : v ∈ f
hv₂ : closure[inst✝] (image2 ϕ v s) ⊆ c
k : Set β := closure[inst✝] (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u ↦ (closure[inst✝] (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ u ∈ f, IsOpen[inst✝] (j u)
this : ⋃ u ∈ f, j u = ⋃ u, j ↑u
⊢ k ∩ ⋂ i, closure[inst✝] (image2 ϕ (↑i ∩ v) s) ⊆ n

Tactic:
]

Goal state after:
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen[inst✝] n
v : Set τ
hn₂ : ⋂ u, closure[inst✝] (image2 ϕ (↑u ∩ v) s) ⊆ n
hv₁ : v ∈ f
hv₂ : closure[inst✝] (image2 ϕ v s) ⊆ c
k : Set β := closure[inst✝] (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u ↦ (closure[inst✝] (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ u ∈ f, IsOpen[inst✝] (j u)
this : ⋃ u ∈ f, j u = ⋃ u, j ↑u
⊢ k ∩ ⋂ i, closure[inst✝] (image2 ϕ (↑i ∩ v) s) ⊆ 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
y z : X
k : ℕ
k_mn : k / m < n
y_int : (T^[k % m] ↑(t ⟨k / m, k_mn⟩), T^[k] y) ∈ U
z_int : (T^[k % m] ↑(t ⟨k / m, k_mn⟩), T^[k] z) ∈ U
⊢ ∃ b, (T^[k] y, b) ∈ U ∧ (b, T^[k] z) ∈ U

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
y z : X
k : ℕ
k_mn : k / m < n
y_int : (T^[k % m] ↑(t ⟨k / m, k_mn⟩), T^[k] y) ∈ U
z_int : (T^[k % m] ↑(t ⟨k / m, k_mn⟩), T^[k] z) ∈ U
⊢ ∃ b, (T^[k] y, b) ∈ U ∧ (b, T^[k] z) ∈ U
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
c : Set β
hc₁ : IsCompact c
n : Set β
hn₁ : IsOpen[inst✝] n
hn₂ : ω f ϕ s ⊆ n
v : Set τ
hv₁ : v ∈ f
hv₂ : closure[inst✝] (image2 ϕ v s) ⊆ c
k : Set β := closure[inst✝] (image2 ϕ v s)
hk : IsCompact (k \ n)
j : Set τ → Set β := fun u ↦ (closure[inst✝] (image2 ϕ (u ∩ v) s))ᶜ
hj₁ : ∀ u ∈ f, IsOpen[inst✝] (j u)
hj₂ : k \ n ⊆ ⋃ u ∈ f, j u
g : Set (Set τ)
hg₁ : ∀ u ∈ g, u ∈ f
hg₂ : g.Finite
hg₃ : k \ n ⊆ ⋃ i ∈ g, j i
w : Set τ := (⋂ u ∈ g, u) ∩ v
hw₂ : w ∈ f
hw₃ : k \ n ⊆ (closure[inst✝] (image2 ϕ w s))ᶜ
hw₄ : kᶜ ⊆ (closure[inst✝] (image2 ϕ w s))ᶜ
⊢ k ∩ nᶜ ⊆ k ∩ nᶜ

Tactic:
]

Goal state after:
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: τ : 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
⊢ (⋂ u, closure[inst✝¹] (image2 ϕ (↑u ∩ v) s)).Nonempty

Tactic:
]

Goal state after:
τ : 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
⊢ (⋂ u, closure[inst✝¹] (image2 ϕ (↑u ∩ v) s)).Nonempty
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

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

Tactic:
]

Goal state after:
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

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.MeasureTheory.Measure.Decomposition.RadonNikodym

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

Tactic:
]

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
⊢ (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᵐ[ν]
    (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
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 < ⊤
k : ℕ
k_max : ↑k = netMaxcard T F U n
⊢ ∃ s, IsDynNetIn T F U n ↑s ∧ ↑s.card = ↑k

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 < ⊤
k : ℕ
k_max : ↑k = netMaxcard T F U n
⊢ ∃ s, IsDynNetIn T F U n ↑s ∧ ↑s.card = ↑k
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 = netMaxcard T F U n
⊢ ⨆ s, ⨆ (_ : IsDynNetIn T F U n ↑s), ↑s.card = ⨆ a ∈ {s | IsDynNetIn T F U n ↑s}, (WithTop.some ∘ Finset.card) a

Tactic:
]

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 = netMaxcard T F U n
⊢ ⨆ s, ⨆ (_ : IsDynNetIn T F U n ↑s), ↑s.card = ⨆ a ∈ {s | IsDynNetIn T F U n ↑s}, (WithTop.some ∘ Finset.card) a
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
⊢ Fintype.card ↑sn ≤ #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
⊢ Fintype.card ↑sn ≤ #s ^ n
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 < ⊤
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, IsDynNetIn T F U n ↑s ∧ s.card = k

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 < ⊤
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, IsDynNetIn T F U n ↑s ∧ s.card = k
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : 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 ν
h₄ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᵐ[ν] 0
⊢ ν'.withDensity (μ.rnDeriv ν') ⟂ₘ ν

Tactic:
]

Goal state after:
α : 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 ν
h₄ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᵐ[ν] 0
⊢ ν'.withDensity (μ.rnDeriv ν') ⟂ₘ ν
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})
s : Finset X
h : IsDynNetIn T F U n ↑s
⊢ ↑s.card ≤ sSup (WithTop.some '' Finset.card '' {s | IsDynNetIn T F U n ↑s})

Tactic:
]

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 ≤ sSup (WithTop.some '' Finset.card '' {s | IsDynNetIn T F U n ↑s})
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
⊢ c ⊆ c

Tactic:
]

Goal state after:
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: X : Type u_1
T : X → X
U : SetRel X X
F : Set X
inst✝ : UniformSpace X
F_comp : IsCompact F
F_inv : MapsTo T F F
U_uni : U ∈ 𝓤 X
n : ℕ
V : SetRel X X
V_uni : V ∈ 𝓤 X
V_symm : V.IsSymm
V_U : V ○ V ⊆ U
s : Finset X
left✝ : ∀ x ∈ s, x ∈ F
s_cover : F ⊆ ⋃ x ∈ s, ball x V
this : IsDynCoverOf T F V 1 ↑s
t : Finset X
t_dyncover : IsDynCoverOf T F (V ○ V) n ↑t
t_card : #t ≤ #s ^ n
⊢ ∃ s, IsDynCoverOf T F U n ↑s

Tactic:
]

Goal state after:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
inst✝ : UniformSpace X
F_comp : IsCompact F
F_inv : MapsTo T F F
U_uni : U ∈ 𝓤 X
n : ℕ
V : SetRel X X
V_uni : V ∈ 𝓤 X
V_symm : V.IsSymm
V_U : V ○ V ⊆ U
s : Finset X
left✝ : ∀ x ∈ s, x ∈ F
s_cover : F ⊆ ⋃ x ∈ s, ball x V
this : IsDynCoverOf T F V 1 ↑s
t : Finset X
t_dyncover : IsDynCoverOf T F (V ○ V) n ↑t
t_card : #t ≤ #s ^ n
⊢ ∃ s, IsDynCoverOf T F U n ↑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 < ⊤
k : ℕ
k_max : ↑k = ↑(sSup (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})
h_bdda : BddAbove (Finset.card '' {s | IsDynNetIn T F U n ↑s})
h_nemp : (Finset.card '' {s | IsDynNetIn T F U n ↑s}).Nonempty
⊢ ∃ s, IsDynNetIn T F U n ↑s ∧ s.card = k

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 < ⊤
k : ℕ
k_max : ↑k = ↑(sSup (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})
h_bdda : BddAbove (Finset.card '' {s | IsDynNetIn T F U n ↑s})
h_nemp : (Finset.card '' {s | IsDynNetIn T F U n ↑s}).Nonempty
⊢ ∃ s, IsDynNetIn T F U n ↑s ∧ s.card = k
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h_fin : coverMincard T F U n < ⊤
k : ℕ
k_min : ↑k = coverMincard T F U n
⊢ ∃ s, IsDynCoverOf T F U n ↑s ∧ ↑(#s) = ↑k

Tactic:
]

Goal state after:
X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
h_fin : coverMincard T F U n < ⊤
k : ℕ
k_min : ↑k = coverMincard T F U n
⊢ ∃ s, IsDynCoverOf T F U n ↑s ∧ ↑(#s) = ↑k