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

Goal state before:
pp: α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
n : ℕ
H : ¬μ {x | x ∈ s ∧ ∀ m ≥ n, f^[m] x ∉ s} = 0
⊢ NullMeasurableSet (s ∩ {x | ∀ m ≥ n, f^[m] x ∉ s}) μ

Tactic:
simp only [ofPred_forall, ← compl_ofPred]

Goal state after:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
n : ℕ
H : ¬μ {x | x ∈ s ∧ ∀ m ≥ n, f^[m] x ∉ s} = 0
⊢ NullMeasurableSet (s ∩ ⋂ i, ⋂ (_ : i ≥ n), {a | f^[i] a ∈ s}ᶜ) μ
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))
hn : 1 ≤ ↑n
hI : I =ᵐ[volume] closedBall x (T / (2 * ↑n))
this : Fintype ↥G
⊢ #Finset.univ = Fintype.card ↥(AddSubgroup.zmultiples u)

Tactic:
;

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))
hn : 1 ≤ ↑n
hI : I =ᵐ[volume] closedBall x (T / (2 * ↑n))
this : Fintype ↥G
⊢ #Finset.univ = Fintype.card ↥(AddSubgroup.zmultiples u)
Module: Mathlib.Dynamics.Ergodic.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
n : ℤ
hn✝ : 1 < |n|
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun y ↦ n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun j ↦ ↑(1 / ↑(n.natAbs ^ j) * T)
hn : 1 < n.natAbs
hu₀ : ∀ (j : ℕ), addOrderOf (u j) = n.natAbs ^ j
hnu : ∀ (j : ℕ), n ^ j • u j = 0
hu₁ : ∀ (j : ℕ), u j +ᵥ s =ᵐ[volume] s
⊢ Tendsto (fun j ↦ n.natAbs ^ j) atTop atTop

Tactic:
;

Goal state after:
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn✝ : 1 < |n|
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun y ↦ n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun j ↦ ↑(1 / ↑(n.natAbs ^ j) * T)
hn : 1 < n.natAbs
hu₀ : ∀ (j : ℕ), addOrderOf (u j) = n.natAbs ^ j
hnu : ∀ (j : ℕ), n ^ j • u j = 0
hu₁ : ∀ (j : ℕ), u j +ᵥ s =ᵐ[volume] s
⊢ Tendsto (fun j ↦ n.natAbs ^ j) atTop atTop
Module: Mathlib.MeasureTheory.Group.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
s I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
hs : u +ᵥ s =ᵐ[volume] s
hI : I =ᵐ[volume] ball x (T / (2 * ↑(addOrderOf u)))
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
this : Fintype ↥G
y : AddCircle T
hy : y ∈ G
⊢ ⟨y, hy⟩ +ᵥ s =ᵐ[volume] s

Tactic:
;

Goal state after:
T : ℝ
hT : Fact (0 < T)
s I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
hs : u +ᵥ s =ᵐ[volume] s
hI : I =ᵐ[volume] ball x (T / (2 * ↑(addOrderOf u)))
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
this : Fintype ↥G
y : AddCircle T
hy : y ∈ G
⊢ ⟨y, hy⟩ +ᵥ s =ᵐ[volume] s
Module: Mathlib.Dynamics.Ergodic.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
h : 1 < |n|
f : AddCircle T → AddCircle T := fun y ↦ n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving (⇑e) volume volume
this : ⇑e ∘ f ∘ ⇑e.symm = fun y ↦ n • y
⊢ Ergodic (fun y ↦ n • y) volume

Tactic:
;

Goal state after:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
h : 1 < |n|
f : AddCircle T → AddCircle T := fun y ↦ n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving (⇑e) volume volume
this : ⇑e ∘ f ∘ ⇑e.symm = fun y ↦ n • y
⊢ Ergodic (fun y ↦ n • y) volume
Module: Mathlib.Dynamics.Ergodic.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
h : |1| < |n|
f : AddCircle T → AddCircle T := fun y ↦ n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving (⇑e) volume volume
⊢ n - 1 ≠ 0

Tactic:
;

Goal state after:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
h : |1| < |n|
f : AddCircle T → AddCircle T := fun y ↦ n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving (⇑e) volume volume
⊢ n - 1 ≠ 0
Module: Mathlib.Dynamics.Ergodic.AddCircle

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
h : |1| < |n|
f : AddCircle T → AddCircle T := fun y ↦ n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving (⇑e) volume volume
⊢ n ≠ 1

Tactic:
;

Goal state after:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
h : |1| < |n|
f : AddCircle T → AddCircle T := fun y ↦ n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving (⇑e) volume volume
⊢ n ≠ 1
Module: Mathlib.Dynamics.Ergodic.AddCircle

Goal state before:
pp: case a
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
f : AddCircle T → AddCircle T := fun y ↦ n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving (⇑e) volume volume
h : n - 1 ≠ 0
| x

pp: case a
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
f : AddCircle T → AddCircle T := fun y ↦ n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving (⇑e) volume volume
h : n - 1 ≠ 0
| DivisibleBy.div x (n - 1)

Tactic:
;

Goal state after:
case a
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
f : AddCircle T → AddCircle T := fun y ↦ n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving (⇑e) volume volume
h : n - 1 ≠ 0
| x

case a
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
f : AddCircle T → AddCircle T := fun y ↦ n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving (⇑e) volume volume
h : n - 1 ≠ 0
| DivisibleBy.div x (n - 1)
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 ≠ ∞
hν_ac : ν ≪ ν.withDensity f
⊢ (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) =ᵐ[ν]
    (ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν).rnDeriv (ν.withDensity f)

Tactic:
refine hν_ac.ae_eq ?_

Goal state after:
α : 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 ≠ ∞
hν_ac : ν ≪ ν.withDensity f
⊢ (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) =ᵐ[ν.withDensity f]
    (ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν).rnDeriv (ν.withDensity f)
Module: Mathlib.Dynamics.Ergodic.Extreme

Goal state before:
pp: X : Type u_1
m : MeasurableSpace X
f : X → X
ν₁ : Measure X
hfν₁ : MeasurePreserving f ν₁ ν₁
ν₂ : Measure X
hfν₂ : MeasurePreserving f ν₂ ν₂
a b : ℝ≥0∞
ha : 0 < a
hb : 0 < b
hab : a + b = 1
inst✝ : IsFiniteMeasure (a • ν₁ + b • ν₂)
hμ : Ergodic f (a • ν₁ + b • ν₂)
hν₁μ : ν₁ univ = (a • ν₁ + b • ν₂) univ
hν₂μ : ν₂ univ = (a • ν₁ + b • ν₂) univ
⊢ (a • ν₁ + b • ν₂) univ < ∞

Tactic:
;

Goal state after:
X : Type u_1
m : MeasurableSpace X
f : X → X
ν₁ : Measure X
hfν₁ : MeasurePreserving f ν₁ ν₁
ν₂ : Measure X
hfν₂ : MeasurePreserving f ν₂ ν₂
a b : ℝ≥0∞
ha : 0 < a
hb : 0 < b
hab : a + b = 1
inst✝ : IsFiniteMeasure (a • ν₁ + b • ν₂)
hμ : Ergodic f (a • ν₁ + b • ν₂)
hν₁μ : ν₁ univ = (a • ν₁ + b • ν₂) univ
hν₂μ : ν₂ univ = (a • ν₁ + b • ν₂) univ
⊢ (a • ν₁ + b • ν₂) univ < ∞
Module: Mathlib.Dynamics.SymbolicDynamics.Basic

Goal state before:
pp: A : Type u_1
G : Type u_2
inst✝ : Monoid G
x : G → A
h : G
⊢ mulShift 1 x h = x h

Tactic:
;

Goal state after:
A : Type u_1
G : Type u_2
inst✝ : Monoid G
x : G → A
h : G
⊢ mulShift 1 x h = x h
Module: Mathlib.Dynamics.SymbolicDynamics.Basic

Goal state before:
pp: A : Type u_1
G : Type u_2
inst✝ : Monoid G
g₁ g₂ : G
x : G → A
h : G
⊢ mulShift (g₁ * g₂) x h = mulShift g₂ (mulShift g₁ x) h

Tactic:
;

Goal state after:
A : Type u_1
G : Type u_2
inst✝ : Monoid G
g₁ g₂ : G
x : G → A
h : G
⊢ mulShift (g₁ * g₂) x h = mulShift g₂ (mulShift g₁ x) h
Module: Mathlib.Dynamics.SymbolicDynamics.Basic

Goal state before:
pp: A : Type u_1
G : Type u_2
U : Finset G
x y : G → A
⊢ y ∈ cylinder U x ↔ y ∈ (↑U).pi fun i ↦ {x i}

Tactic:
;

Goal state after:
A : Type u_1
G : Type u_2
U : Finset G
x y : G → A
⊢ y ∈ cylinder U x ↔ y ∈ (↑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 [Finset.mem_image] using hmem

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 [Finset.mem_image] using hmem

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

Tactic:
;

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

Goal state before:
pp: A : Type u_1
inst✝⁴ : TopologicalSpace A
inst✝³ : Inhabited A
G : Type u_2
inst✝² : Monoid G
inst✝¹ : IsLeftCancelMul G
inst✝ : DiscreteTopology A
F : Set (Pattern A G)
x✝ : G → A
⊢ x✝ ∈ {x | ∀ p ∈ F, ∀ (v : G), ¬p.mulOccursInAt x v} ↔ x✝ ∈ ⋂ p ∈ F, ⋂ v, {x | ¬p.mulOccursInAt x v}

Tactic:
;

Goal state after:
A : Type u_1
inst✝⁴ : TopologicalSpace A
inst✝³ : Inhabited A
G : Type u_2
inst✝² : Monoid G
inst✝¹ : IsLeftCancelMul G
inst✝ : DiscreteTopology A
F : Set (Pattern A G)
x✝ : G → A
⊢ x✝ ∈ {x | ∀ p ∈ F, ∀ (v : G), ¬p.mulOccursInAt x v} ↔ x✝ ∈ ⋂ p ∈ F, ⋂ v, {x | ¬p.mulOccursInAt x v}
Module: Mathlib.Dynamics.SymbolicDynamics.Basic

Goal state before:
pp: A : Type u_1
inst✝⁴ : TopologicalSpace A
inst✝³ : Inhabited A
G : Type u_2
inst✝² : Monoid G
inst✝¹ : IsLeftCancelMul G
inst✝ : DiscreteTopology A
F : Set (Pattern A G)
h_eq : {x | ∀ p ∈ F, ∀ (v : G), ¬p.mulOccursInAt x v} = ⋂ p ∈ F, ⋂ v, {x | ¬p.mulOccursInAt x v}
p : Pattern A G
hp : p ∈ F
v : G
x✝ : G → A
⊢ x✝ ∈ {x | ¬p.mulOccursInAt x v} ↔ x✝ ∈ {x | p.mulOccursInAt x v}ᶜ

Tactic:
;

Goal state after:
A : Type u_1
inst✝⁴ : TopologicalSpace A
inst✝³ : Inhabited A
G : Type u_2
inst✝² : Monoid G
inst✝¹ : IsLeftCancelMul G
inst✝ : DiscreteTopology A
F : Set (Pattern A G)
h_eq : {x | ∀ p ∈ F, ∀ (v : G), ¬p.mulOccursInAt x v} = ⋂ p ∈ F, ⋂ v, {x | ¬p.mulOccursInAt x v}
p : Pattern A G
hp : p ∈ F
v : G
x✝ : G → A
⊢ x✝ ∈ {x | ¬p.mulOccursInAt x v} ↔ x✝ ∈ {x | p.mulOccursInAt x v}ᶜ
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: τ : 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₂

Tactic:
;

Goal state after:
τ : 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: A : Type u_3
G : Type u_4
inst✝¹ : Finite A
inst✝ : Inhabited A
U : Finset G
val✝ : Fintype A
cfg : G → A
dom : Finset G
cond : ∀ g ∉ dom, cfg g = default
hU : dom = U
⊢ (fun f ↦ ⟨{ config := fun g ↦ if h : g ∈ U then f ⟨g, h⟩ else default, support := U, condition := ⋯ }, ⋯⟩)
      ((fun p i ↦ (↑p).config ↑i) ⟨{ config := cfg, support := dom, condition := cond }, hU⟩) =
    ⟨{ config := cfg, support := dom, condition := cond }, hU⟩

Tactic:
;

Goal state after:
A : Type u_3
G : Type u_4
inst✝¹ : Finite A
inst✝ : Inhabited A
U : Finset G
val✝ : Fintype A
cfg : G → A
dom : Finset G
cond : ∀ g ∉ dom, cfg g = default
hU : dom = U
⊢ (fun f ↦ ⟨{ config := fun g ↦ if h : g ∈ U then f ⟨g, h⟩ else default, support := U, condition := ⋯ }, ⋯⟩)
      ((fun p i ↦ (↑p).config ↑i) ⟨{ config := cfg, support := dom, condition := cond }, hU⟩) =
    ⟨{ config := cfg, support := dom, condition := cond }, hU⟩
Module: Mathlib.Dynamics.SymbolicDynamics.Basic

Goal state before:
pp: A : Type u_3
G : Type u_4
inst✝¹ : Finite A
inst✝ : Inhabited A
U : Finset G
val✝ : Fintype A
f : ↥U → A
i : ↥U
⊢ (fun p i ↦ (↑p).config ↑i)
      ((fun f ↦ ⟨{ config := fun g ↦ if h : g ∈ U then f ⟨g, h⟩ else default, support := U, condition := ⋯ }, ⋯⟩) f) i =
    f i

Tactic:
;

Goal state after:
A : Type u_3
G : Type u_4
inst✝¹ : Finite A
inst✝ : Inhabited A
U : Finset G
val✝ : Fintype A
f : ↥U → A
i : ↥U
⊢ (fun p i ↦ (↑p).config ↑i)
      ((fun f ↦ ⟨{ config := fun g ↦ if h : g ∈ U then f ⟨g, h⟩ else default, support := U, condition := ⋯ }, ⋯⟩) f) i =
    f i
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:
· rintro ⟨u₁, hu₁⟩ ⟨u₂, hu₂⟩
    use ⟨u₁ ∩ u₂, inter_mem hu₁ hu₂⟩
    constructor
    all_goals exact closure_mono (image2_subset (inter_subset_inter_left _ (by simp)) Subset.rfl)

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

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))

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: 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})
⊢ ∀ x ∈ Finset.card '' {s | IsDynNetIn T F U n ↑s}, x ≤ k

Tactic:
simp only [mem_image, mem_ofPred_eq, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]

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})
⊢ ∀ (a : Finset X), IsDynNetIn T F U n ↑a → a.card ≤ k
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
x : α
hx : (μ.rnDeriv ν)⁻¹ x = ν.rnDeriv μ x
⊢ (ν.rnDeriv μ)⁻¹ x = μ.rnDeriv ν x

Tactic:
;

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
x : α
hx : (μ.rnDeriv ν)⁻¹ x = ν.rnDeriv μ x
⊢ (ν.rnDeriv μ)⁻¹ x = μ.rnDeriv ν x
Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj

Goal state before:
pp: X : Type u_1
Y : Type u_2
u : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F : Set X
⊢ coverEntropyInf T (φ '' F) = coverEntropyInf S F

Tactic:
let : UniformSpace X := comap φ u
  apply le_antisymm
  · refine iSup₂_le fun V V_uni ↦
      (coverEntropyInfEntourage_antitone _ _ SetRel.symmetrize_subset_self).trans <|
      (coverEntropyInfEntourage_image_le h F _).trans ?_
    apply coverEntropyInfEntourage_le_coverEntropyInf
    rw [uniformity_comap φ, mem_comap]
    exact ⟨_, symmetrize_mem_uniformity V_uni, .rfl⟩
  · refine iSup₂_le fun U U_uni ↦ ?_
    simp only [uniformity_comap φ, mem_comap] at U_uni
    obtain ⟨V, V_uni, V_sub⟩ := U_uni
    obtain ⟨W, W_uni, W_symm, W_V⟩ := comp_symm_mem_uniformity_sets V_uni
    apply (coverEntropyInfEntourage_antitone S F ((preimage_mono W_V).trans V_sub)).trans
    apply (le_coverEntropyInfEntourage_image h F).trans
    exact coverEntropyInfEntourage_le_coverEntropyInf T (φ '' F) W_uni

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

Goal state before:
pp: case inl
X : Type u_1
T : X → X
F G : Set X
U : SetRel X X
n : ℕ
hF : coverMincard T F U n = ⊤
⊢ coverMincard T (F ∪ G) U n ≤ ⊤

Tactic:
;

Goal state after:
case inl
X : Type u_1
T : X → X
F G : Set X
U : SetRel X X
n : ℕ
hF : coverMincard T F U n = ⊤
⊢ coverMincard T (F ∪ G) U n ≤ ⊤
Module: Mathlib.Dynamics.Transitive

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : Monoid M
inst✝ : MulAction M α
⊢ IsTopologicallyTransitive M α ↔ ∀ {U : Set α}, IsOpen U → U.Nonempty → Dense (⋃ m, m • U)

Tactic:
simp only [isTopologicallyTransitive_iff, inter_comm, dense_iff_inter_open, inter_iUnion,
    nonempty_iUnion]

Goal state after:
M : Type u_1
α : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : Monoid M
inst✝ : MulAction M α
⊢ (∀ {U V : Set α}, IsOpen U → U.Nonempty → IsOpen V → V.Nonempty → ∃ m, (V ∩ m • U).Nonempty) ↔
    ∀ {U : Set α}, IsOpen U → U.Nonempty → ∀ (U_1 : Set α), IsOpen U_1 → U_1.Nonempty → ∃ i, (U_1 ∩ i • U).Nonempty
Module: Mathlib.Dynamics.TopologicalEntropy.Subset

Goal state before:
pp: case inr.inl
X : Type u_1
T : X → X
F G : Set X
U : SetRel X X
n : ℕ
hF : coverMincard T F U n < ⊤
hG : coverMincard T G U n = ⊤
⊢ coverMincard T (F ∪ G) U n ≤ ⊤

Tactic:
;

Goal state after:
case inr.inl
X : Type u_1
T : X → X
F G : Set X
U : SetRel X X
n : ℕ
hF : coverMincard T F U n < ⊤
hG : coverMincard T G U n = ⊤
⊢ coverMincard T (F ∪ G) U n ≤ ⊤
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case pos
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : (map (RingHom.id F) (X ^ n - 1)).Splits
ha : ¬a = 0
ha' : (algebraMap F (X ^ n - C a).SplittingField) a ≠ 0
hn : n = 0
⊢ Group.IsSolvable (X ^ n - C a).Gal

Tactic:
rw [hn, pow_zero, ← C_1, ← C_sub]
    exact gal_C_isSolvable (1 - a)

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

Goal state before:
pp: α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
f : α → ℝ≥0∞
hf : AEMeasurable f ν
⊢ ∫⁻ (x : α), μ.rnDeriv ν x * f x ∂ν = ∫⁻ (x : α), f x ∂μ

Tactic:
by
  nth_rw 2 [← withDensity_rnDeriv_eq μ ν hμν]
  rw [lintegral_withDensity_eq_lintegral_mul₀ (measurable_rnDeriv μ ν).aemeasurable hf]
  simp only [Pi.mul_apply]

Goal state after:
Module: Mathlib.RingTheory.Algebraic.Cardinality

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
L : Type v
inst✝⁴ : CommRing L
inst✝³ : IsDomain L
inst✝² : Algebra R L
inst✝¹ : IsTorsionFree R L
inst✝ : Algebra.IsAlgebraic R L
⊢ #((p : R[X]) × { x // x ∈ p.aroots L }) = #((i : R[X]) × ↑{x | x ∈ i.aroots L})

Tactic:
;

Goal state after:
R : Type u
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
L : Type v
inst✝⁴ : CommRing L
inst✝³ : IsDomain L
inst✝² : Algebra R L
inst✝¹ : IsTorsionFree R L
inst✝ : Algebra.IsAlgebraic R L
⊢ #((p : R[X]) × { x // x ∈ p.aroots L }) = #((i : R[X]) × ↑{x | x ∈ i.aroots L})
Module: Mathlib.RingTheory.Algebraic.Cardinality

Goal state before:
pp: case h₁
R : Type u
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
L : Type v
inst✝⁴ : CommRing L
inst✝³ : IsDomain L
inst✝² : Algebra R L
inst✝¹ : IsTorsionFree R L
inst✝ : Algebra.IsAlgebraic R L
⊢ lift.{v, u} #R[X] ≤ lift.{v, u} (max #R ℵ₀)

Tactic:
;

Goal state after:
case h₁
R : Type u
inst✝⁶ : CommRing R
inst✝⁵ : IsDomain R
L : Type v
inst✝⁴ : CommRing L
inst✝³ : IsDomain L
inst✝² : Algebra R L
inst✝¹ : IsTorsionFree R L
inst✝ : Algebra.IsAlgebraic R L
⊢ lift.{v, u} #R[X] ≤ lift.{v, u} (max #R ℵ₀)
Module: Mathlib.FieldTheory.IsAlgClosed.Classification

Goal state before:
pp: case refine_1
R : Type u_1
L : Type u_2
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : Field L
inst✝² : Algebra R L
ι : Type u_4
v : ι → K
κ : Type u_5
w : κ → L
hv✝ : AlgebraicIndependent R v
hw✝ : AlgebraicIndependent R w
inst✝¹ : IsAlgClosed K
inst✝ : IsAlgClosed L
e : ι ≃ κ
hv : IsTranscendenceBasis R v
hw : IsTranscendenceBasis R w
this✝ : IsAlgClosure (↥(Algebra.adjoin R (Set.range v))) K := isAlgClosure_of_transcendence_basis v hv
this : IsAlgClosure (↥(Algebra.adjoin R (Set.range w))) L := isAlgClosure_of_transcendence_basis w hw
i✝ : κ
m✝ : κ →₀ ℕ
⊢ MvPolynomial.coeff m✝ (((MvPolynomial.rename ⇑e).comp (MvPolynomial.rename ⇑e.symm)) (MvPolynomial.X i✝)) =
    MvPolynomial.coeff m✝ ((AlgHom.id R (MvPolynomial κ R)) (MvPolynomial.X i✝))

Tactic:
;

Goal state after:
case refine_1
R : Type u_1
L : Type u_2
K : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : Field L
inst✝² : Algebra R L
ι : Type u_4
v : ι → K
κ : Type u_5
w : κ → L
hv✝ : AlgebraicIndependent R v
hw✝ : AlgebraicIndependent R w
inst✝¹ : IsAlgClosed K
inst✝ : IsAlgClosed L
e : ι ≃ κ
hv : IsTranscendenceBasis R v
hw : IsTranscendenceBasis R w
this✝ : IsAlgClosure (↥(Algebra.adjoin R (Set.range v))) K := isAlgClosure_of_transcendence_basis v hv
this : IsAlgClosure (↥(Algebra.adjoin R (Set.range w))) L := isAlgClosure_of_transcendence_basis w hw
i✝ : κ
m✝ : κ →₀ ℕ
⊢ MvPolynomial.coeff m✝ (((MvPolynomial.rename ⇑e).comp (MvPolynomial.rename ⇑e.symm)) (MvPolynomial.X i✝)) =
    MvPolynomial.coeff m✝ ((AlgHom.id R (MvPolynomial κ R)) (MvPolynomial.X i✝))