mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.WSeq.Defs

Goal state before:
pp: α : Type u
s✝ : WSeq α
s1 s2 : Computation ℕ
l : List α
s : WSeq α
h :
  s1 =
      Computation.corec
        (fun x ↦
          match x with
          | (n, s) =>
            match Seq.destruct s with
            | none => Sum.inl n
            | some (none, s') => Sum.inr (n, s')
            | some (some val, s') => Sum.inr (n + 1, s'))
        (l.length, s.think) ∧
    s2 =
      Computation.map List.length
        (Computation.corec
          (fun x ↦
            match x with
            | (l, s) =>
              match Seq.destruct s with
              | none => Sum.inl l.reverse
              | some (none, s') => Sum.inr (l, s')
              | some (some a, s') => Sum.inr (a :: l, s'))
          (l, s.think))
⊢ Computation.corec
      (fun x ↦
        match Seq.destruct x.2 with
        | none => Sum.inl x.1
        | some (none, s') => Sum.inr (x.1, s')
        | some (some val, s') => Sum.inr (x.1 + 1, s'))
      (l.length, s) =
    Computation.corec
      (fun x ↦
        match Seq.destruct x.2 with
        | none => Sum.inl x.1
        | some (none, s') => Sum.inr (x.1, s')
        | some (some val, s') => Sum.inr (x.1 + 1, s'))
      (l.length, s)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.WSeq.Defs

Goal state before:
pp: α : Type u
s✝ : WSeq α
s1 s2 : Computation ℕ
l : List α
s : WSeq α
h :
  s1 =
      Computation.corec
        (fun x ↦
          match x with
          | (n, s) =>
            match Seq.destruct s with
            | none => Sum.inl n
            | some (none, s') => Sum.inr (n, s')
            | some (some val, s') => Sum.inr (n + 1, s'))
        (l.length, s.think) ∧
    s2 =
      Computation.map List.length
        (Computation.corec
          (fun x ↦
            match x with
            | (l, s) =>
              match Seq.destruct s with
              | none => Sum.inl l.reverse
              | some (none, s') => Sum.inr (l, s')
              | some (some a, s') => Sum.inr (a :: l, s'))
          (l, s.think))
⊢ Computation.map List.length
      (Computation.corec
        (fun x ↦
          match Seq.destruct x.2 with
          | none => Sum.inl x.1.reverse
          | some (none, s') => Sum.inr (x.1, s')
          | some (some a, s') => Sum.inr (a :: x.1, s'))
        (l, s)) =
    Computation.map List.length
      (Computation.corec
        (fun x ↦
          match Seq.destruct x.2 with
          | none => Sum.inl x.1.reverse
          | some (none, s') => Sum.inr (x.1, s')
          | some (some a, s') => Sum.inr (a :: x.1, s'))
        (l, s))

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
f : α → α
x✝² : Set α
x✝¹ : MeasurableSet x✝²
x✝ : f ⁻¹' x✝² = x✝²
⊢ EventuallyConst x✝² (ae 0)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
f : α → α
hf : Measurable f
⊢ Measure.map f 0 ≪ 0

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
f : α → α
hf : Measurable f
⊢ Measure.map f 0 = 0

Tactic:
simp

Goal state after:
Module: Mathlib.MeasureTheory.Group.AEStabilizer

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
s : Set α
⊢ 1 ∈ {g | g • s =ᵐ[μ] s}

Tactic:
simp

Goal state after:
Module: Mathlib.MeasureTheory.Group.AEStabilizer

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
x✝² : MeasurableSpace α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
x✝¹ : G
x✝ : x✝¹ ∈ ⊤
⊢ x✝¹ ∈ aestabilizer G μ ∅

Tactic:
simp

Goal state after:
Module: Mathlib.MeasureTheory.Group.AEStabilizer

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
x✝² : MeasurableSpace α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
x✝¹ : G
x✝ : x✝¹ ∈ ⊤
⊢ x✝¹ ∈ aestabilizer G μ univ

Tactic:
simp

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

Goal state before:
pp: ⊢ Tendsto (fun n ↦ (⇑1)^[n] 0 / ↑n) atTop (𝓝 0)

Tactic:
simp

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

Goal state before:
pp: f : CircleDeg1Lift
⊢ τ (f ^ 0) = ↑0 * τ f

Tactic:
simp

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

Goal state before:
pp: f : CircleDeg1Liftˣ
n : ℕ
⊢ τ ↑(f ^ -[n+1]) = ↑-[n+1] * τ ↑f

Tactic:
simp

Goal state after:
f : CircleDeg1Liftˣ
n : ℕ
⊢ -((↑n + 1) * τ ↑f) = (-1 + -↑n) * τ ↑f
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)
s : Set Y
hfg : Tendsto f l (𝓝 g)
hf : ∀ᶠ (a : α) in l, MeasurePreserving (⇑(f a)) μ ν
hg : MeasurePreserving (⇑g) μ ν
hs : NullMeasurableSet s ν
hνs : ν s ≠ ∞
this✝ : ν.InnerRegularCompactLTTop
ε : ℝ≥0∞
hε : ε > 0
this :
  ∀ {s : Set Y},
    NullMeasurableSet s ν → ν s ≠ ∞ → ∀ ε > 0, IsOpen[inst✝⁵] s → ∀ᶠ (x : α) in l, μ ((⇑(f x) ⁻¹' s) ∆ (⇑g ⁻¹' s)) ≤ ε
hso : ¬IsOpen[inst✝⁵] s
H : 0 < ε / 3
U : Set Y
hUo : IsOpen[inst✝⁵] U
hU : ν U < ∞
hmU : NullMeasurableSet U ν
hUs : ν (U ∆ s) ≤ ε / 3
a : α
hfa : MeasurePreserving (⇑(f a)) μ ν
ha : μ ((⇑(f a) ⁻¹' U) ∆ (⇑g ⁻¹' U)) ≤ ε / 3
⊢ ε / 3 + ε / 3 + ε / 3 = ε

Tactic:
simp

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✝² : 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
⊢ (match 1 with
    | (x, y) => a * x / y) =
    a

Tactic:
simp

Goal state after:
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
⊢ μ ((⇑(f w) ⁻¹' t) ∆ (⇑(f z) ⁻¹' t)) < μ ((⇑(f z) ⁻¹' t) ∆ s) → w ∈ {z | ⇑(f z) ⁻¹' t =ᵐ[μ] s}ᶜ

Tactic:
hw

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 w) ⁻¹' t) ∆ (⇑(f z) ⁻¹' t)) < μ ((⇑(f z) ⁻¹' t) ∆ s)
⊢ w ∈ {z | ⇑(f z) ⁻¹' t =ᵐ[μ] 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))
hI : I =ᵐ[volume] B
hn : 1 ≤ ↑n
g : AddCircle T
hg : g ∈ G
hg' : g ≠ 0
⊢ g +ᵥ B = ball (g + x) (T / (2 * ↑n))

Tactic:
add_comm g x,

Goal state after:
T : ℝ
hT : Fact (0 < T)
I : Set (AddCircle T)
u x : AddCircle T
hu : IsOfFinAddOrder u
G : AddSubgroup (AddCircle T) := AddSubgroup.zmultiples u
n : ℕ := addOrderOf u
B : Set (AddCircle T) := ball x (T / (2 * ↑n))
hI : I =ᵐ[volume] B
hn : 1 ≤ ↑n
g : AddCircle T
hg : g ∈ G
hg' : g ≠ 0
⊢ g +ᵥ B = ball (x + g) (T / (2 * ↑n))
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 : ℕ
⊢ ∀ (a : α), ¬(a ∈ s ∧ ∀ m ≥ n, f^[m] a ∉ s) → a ∈ s → ∃ b, n ≤ b ∧ f^[b] a ∈ s

Tactic:
simp

Goal state after:
Module: Mathlib.Dynamics.Ergodic.Extreme

Goal state before:
pp: X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
f : X → X
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμ : Ergodic f μ
hfν : MeasurePreserving f ν ν
hνμ : ν ≪ μ
this : ν.rnDeriv μ ∘ f =ᵐ[μ] ν.rnDeriv μ
c : ℝ≥0∞
hc : ν.rnDeriv μ =ᵐ[μ] const X c
s : Set X
hs : MeasurableSet s
⊢ ∫⁻ (x : X) in s, c ∂μ = (c • μ) s

Tactic:
simp

Goal state after:
Module: Mathlib.Dynamics.Ergodic.Extreme

Goal state before:
pp: case inl
X : Type u_1
m : MeasurableSpace X
f : X → X
c : ℝ≥0∞
inst✝¹ : IsFiniteMeasure 0
hμ : Ergodic f 0
inst✝ : IsFiniteMeasure (c • 0)
hfν : MeasurePreserving f (c • 0) (c • 0)
hνμ : c • 0 ≪ 0
huniv : (c • 0) univ = 0 univ
⊢ c • 0 = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Dynamics.Ergodic.Extreme

Goal state before:
pp: X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
f : X → X
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
hμ : Ergodic f μ
hfν : MeasurePreserving f ν ν
hνμ : ν ≪ μ
⊢ ν univ = μ univ

Tactic:
simp

Goal state after:
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
this : IsFiniteMeasure ν₁
⊢ ν₁ ≪ a • ν₁

Tactic:
apply absolutelyContinuous_smul ha.ne'

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

Goal state before:
pp: A : Type u_1
G : Type u_2
inst✝¹ : TopologicalSpace A
inst✝ : DiscreteTopology A
U : Finset G
x : G → A
⊢ ∀ a ∈ ↑U, IsOpen[inst✝¹] {x a}

Tactic:
simp

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

Goal state before:
pp: A : Type u_1
G : Type u_2
inst✝¹ : TopologicalSpace A
inst✝ : T1Space A
U : Finset G
x : G → A
⊢ ∀ a ∈ ↑U, IsClosed[inst✝¹] {x a}

Tactic:
simp

Goal state after:
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
this : (fun a ↦ f a * ((f a)⁻¹ * μ.rnDeriv ν a)) =ᵐ[ν] μ.rnDeriv ν
⊢ ∫⁻ (a : α) in s, μ.rnDeriv ν a ∂ν = ∫⁻ (a : α) in s, f a * ((f a)⁻¹ * μ.rnDeriv ν a) ∂ν

Tactic:
lintegral_congr_ae (ae_restrict_of_ae this)

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
this : (fun a ↦ f a * ((f a)⁻¹ * μ.rnDeriv ν a)) =ᵐ[ν] μ.rnDeriv ν
⊢ ∫⁻ (a : α) in s, μ.rnDeriv ν a ∂ν = ∫⁻ (a : α) in s, μ.rnDeriv ν a ∂ν
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:
simp

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

Goal state before:
pp: case zero
X : Type u_1
T : X → X
U : SetRel X X
inst✝ : UniformSpace X
h : UniformContinuous T
U_uni : U ∈ 𝓤 X
⊢ ⋂ k, (map T T)^[↑k] ⁻¹' U ∈ 𝓤 X

Tactic:
simp

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

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

Goal state before:
pp: 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
⊢ IsDynCoverOf T ∅ (U ○ U) (m * n) ↑∅ ∧ #∅ ≤ #s ^ n

Tactic:
simp

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₁ : Set τ
hu₁ : u₁ ∈ f.sets
u₂ : Set τ
hu₂ : u₂ ∈ f.sets
⊢ ↑⟨u₁ ∩ u₂, ⋯⟩ ⊆ ↑⟨u₁, hu₁⟩

Tactic:
simp

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₁ : Set τ
hu₁ : u₁ ∈ f.sets
u₂ : Set τ
hu₂ : u₂ ∈ f.sets
⊢ ↑⟨u₁ ∩ u₂, ⋯⟩ ⊆ ↑⟨u₂, hu₂⟩

Tactic:
simp

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
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
x✝ : Nonempty ↥s
y : X
y_F : y ∈ F
t : Fin n → ↥s
ht : ∀ (k : Fin n), y ∈ T^[m * ↑k] ⁻¹' ball (↑(t k)) (dynEntourage T U m)
⊢ y ∈ ⋂ k, T^[m * ↑k] ⁻¹' ball (↑(t k)) (dynEntourage T U m)

Tactic:
simpa using ht

Goal state after:
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 = ⨅ x, ↑(#↑x)
this : Nonempty { s // IsDynCoverOf T F U n ↑s }
key : ∃ y, ↑(#↑y) = ↑k
⊢ ∃ s, IsDynCoverOf T F U n ↑s ∧ #s = k

Tactic:
Subtype.exists

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 = ⨅ x, ↑(#↑x)
this : Nonempty { s // IsDynCoverOf T F U n ↑s }
key : ∃ a, ∃ (b : IsDynCoverOf T F U n ↑a), ↑(#↑⟨a, b⟩) = ↑k
⊢ ∃ s, IsDynCoverOf T F U n ↑s ∧ #s = k
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: case inl
X : Type u_1
T : X → X
U : SetRel X X
inst✝ : U.IsSymm
m n : ℕ
F_inv : MapsTo T ∅ ∅
⊢ coverMincard T ∅ (U ○ U) (m * n) ≤ coverMincard T ∅ U m ^ n

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
s : Set α
hs : MeasurableSet s
⊢ (ν.withDensity (μ.rnDeriv ν)) s = (ν.withDensity (μ.rnDeriv ν)) s ∨
    (ν.withDensity (μ.rnDeriv ν)) s = 0 ∧ (ν.withDensity (μ.rnDeriv ν)) s = ∞ ∨
      (ν.withDensity (μ.rnDeriv ν)) s = ∞ ∧ (ν.withDensity (μ.rnDeriv ν)) s = 0

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SFinite ν
s : Set α
⊢ (ν.withDensity (μ.rnDeriv ν)) s = (ν.withDensity (μ.rnDeriv ν)) s ∨
    (ν.withDensity (μ.rnDeriv ν)) s = 0 ∧ (ν.withDensity (μ.rnDeriv ν)) s = ∞ ∨
      (ν.withDensity (μ.rnDeriv ν)) s = ∞ ∧ (ν.withDensity (μ.rnDeriv ν)) s = 0

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
s : Set α
hμs : μ s ≠ ∞
t : Set α := toMeasurable μ s
ht : t = toMeasurable μ s
ht_m : MeasurableSet t
hμt : μ t ≠ ∞
⊢ ∀ (a : α), 0 a ≤ (fun x ↦ (μ.rnDeriv ν x).toReal) a

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
h_add : (μ + ν).rnDeriv (μ + ν) =ᵐ[ν] μ.rnDeriv (μ + ν) + ν.rnDeriv (μ + ν)
h_one_add : ∀ᵐ (x : α) ∂ν, (μ + ν).rnDeriv (μ + ν) x = (fun x ↦ 1) x
a : α
h4 : 1 = μ.rnDeriv (μ + ν) a + ν.rnDeriv (μ + ν) a
h5 : (μ + ν).rnDeriv (μ + ν) a = 1
h6 : ν.rnDeriv (μ + ν) a = (μ.rnDeriv ν a + 1)⁻¹
⊢ μ.rnDeriv (μ + ν) a = μ.rnDeriv (μ + ν) a + (μ.rnDeriv ν a + 1)⁻¹ - (μ.rnDeriv ν a + 1)⁻¹

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
h_add : (μ + ν).rnDeriv (μ + ν) =ᵐ[ν] μ.rnDeriv (μ + ν) + ν.rnDeriv (μ + ν)
h_one_add : ∀ᵐ (x : α) ∂ν, (μ + ν).rnDeriv (μ + ν) x = (fun x ↦ 1) x
this : μ.rnDeriv (μ + ν) =ᵐ[ν] fun x ↦ 1 - (μ.rnDeriv ν x + 1)⁻¹
a : α
ha : μ.rnDeriv (μ + ν) a = 1 - (μ.rnDeriv ν a + 1)⁻¹
ha_lt_top : μ.rnDeriv ν a < ∞
⊢ (μ.rnDeriv ν a + 1)⁻¹ ≠ ∞

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
h_add : (μ + ν).rnDeriv (μ + ν) =ᵐ[ν] μ.rnDeriv (μ + ν) + ν.rnDeriv (μ + ν)
h_one_add : ∀ᵐ (x : α) ∂ν, (μ + ν).rnDeriv (μ + ν) x = (fun x ↦ 1) x
this : μ.rnDeriv (μ + ν) =ᵐ[ν] fun x ↦ 1 - (μ.rnDeriv ν x + 1)⁻¹
a : α
ha : μ.rnDeriv (μ + ν) a = 1 - (μ.rnDeriv ν a + 1)⁻¹
ha_lt_top : μ.rnDeriv ν a < ∞
h : (μ.rnDeriv ν a + 1) * (μ.rnDeriv ν a + 1)⁻¹ = μ.rnDeriv ν a * (μ.rnDeriv ν a + 1)⁻¹ + 1 * (μ.rnDeriv ν a + 1)⁻¹
⊢ μ.rnDeriv ν a + 1 ≠ 0

Tactic:
simp

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

Goal state before:
pp: case refine_1
X : Type u_1
T : X → X
F G : Set X
U : SetRel X X
⊢ coverEntropyEntourage T (F ∪ G) U ≤ max (coverEntropyEntourage T F U) (coverEntropyEntourage T G U)

pp: case refine_2
X : Type u_1
T : X → X
F G : Set X
U : SetRel X X
⊢ max (coverEntropyEntourage T F U) (coverEntropyEntourage T G U) ≤ coverEntropyEntourage T (F ∪ G) U

Tactic:
· apply le_of_le_of_eq (expGrowthSup_monotone fun n ↦ ?_) expGrowthSup_add
    rw [Pi.add_apply, ← ENat.toENNReal_add]
    exact ENat.toENNReal_mono (coverMincard_union_le T F G U n)

Goal state after:
case refine_2
X : Type u_1
T : X → X
F G : Set X
U : SetRel X X
⊢ max (coverEntropyEntourage T F U) (coverEntropyEntourage T G U) ≤ coverEntropyEntourage T (F ∪ G) U
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: case h0
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
a : α
ha1 : ν.rnDeriv (μ + ν) a = (μ.rnDeriv ν a + 1)⁻¹
ha2 : μ.rnDeriv (μ + ν) a = μ.rnDeriv ν a / (μ.rnDeriv ν a + 1)
ha_lt_top : μ.rnDeriv ν a < ∞
⊢ μ.rnDeriv ν a + 1 ≠ 0

Tactic:
simp

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

Goal state before:
pp: α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite μ
f : α → E
hμν : μ ≪ ν
⊢ ∫ (x : α), (μ.rnDeriv ν x).toReal • f x ∂ν = ∫ (x : α), f x ∂μ

Tactic:
by
  rw [← integral_withDensity_eq_integral_toReal_smul (measurable_rnDeriv _ _) (rnDeriv_lt_top _ _),
    withDensity_rnDeriv_eq _ _ hμν]

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

Goal state before:
pp: G : Type u_3
inst✝⁶ : Group G
mG : MeasurableSpace G
inst✝⁵ : MeasurableMul₂ G
inst✝⁴ : MeasurableInv G
μ : Measure G
inst✝³ : μ.IsMulLeftInvariant
inst✝² : SFinite μ
ν₁ ν₂ : Measure G
inst✝¹ : ν₁.HaveLebesgueDecomposition μ
inst✝ : ν₂.HaveLebesgueDecomposition μ
hν₁ : ν₁ ≪ μ
hν₂ : ν₂ ≪ μ
⊢ (0, ν₁.rnDeriv μ ⋆ₘₗ[μ] ν₂.rnDeriv μ).1 ⟂ₘ μ

Tactic:
simp

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
⊢ max (max (lift.{v, u} (max #R ℵ₀)) ℵ₀) ℵ₀ = max (lift.{v, u} #R) ℵ₀

Tactic:
simp

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

Goal state after:
Module: Mathlib.FieldTheory.IsAlgClosed.Classification

Goal state before:
pp: case refine_2
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.symm).comp (MvPolynomial.rename ⇑e)) (MvPolynomial.X i✝)) =
    MvPolynomial.coeff m✝ ((AlgHom.id R (MvPolynomial ι R)) (MvPolynomial.X i✝))

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.IsAlgClosed.Classification

Goal state before:
pp: R : Type u
K : Type v
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsAlgClosed K
ι : Type w
v : ι → K
hv : IsTranscendenceBasis R v
⊢ Cardinal.lift.{v, max u w} (max (max (max (Cardinal.lift.{w, u} #R) (Cardinal.lift.{u, w} #ι)) ℵ₀) ℵ₀) =
    max (max (Cardinal.lift.{max v w, u} #R) (Cardinal.lift.{max u v, w} #ι)) ℵ₀

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case neg
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : (map i (X ^ n - C a)).Splits
ha' : i a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : (X ^ n - C a).degree ≠ 0
b : E
hb : b ^ n - eval₂ i b (C a) = 0
⊢ (map i (X ^ n - 1)).Splits

Tactic:
eval₂_C,

Goal state after:
case neg
F : Type u_3
inst✝¹ : Field F
E : Type u_4
inst✝ : Field E
i : F →+* E
n : ℕ
a : F
ha : a ≠ 0
h : (map i (X ^ n - C a)).Splits
ha' : i a ≠ 0
hn : ¬n = 0
hn' : 0 < n
hn'' : (X ^ n - C a).degree ≠ 0
b : E
hb : b ^ n - i a = 0
⊢ (map i (X ^ n - 1)).Splits