mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: α : Type u
β : Type v
f : α → β
S✝ : WSeq (Computation α)
c1 c2 : Computation β
h : ∃ l S, c1 = map f (corec parallel.aux1 (l, S)) ∧ c2 = corec parallel.aux1 (List.map (map f) l, WSeq.map (map f) S)
l : List (Computation α)
S : WSeq (Computation α)
⊢ BisimO
    (fun c1 c2 ↦
      ∃ l S,
        c1 = map f (corec parallel.aux1 (l, S)) ∧ c2 = corec parallel.aux1 (List.map (map f) l, WSeq.map (map f) S))
    (map f (corec parallel.aux1 (l, S))).destruct
    (corec parallel.aux1 (List.map (map f) l, WSeq.map (map f) S)).destruct

Tactic:
have : parallel.aux2 (l.map (map f))
          = lmap f (rmap (List.map (map f)) (parallel.aux2 l)) := by
        simp only [parallel.aux2, rmap, lmap]
        induction l with
        | nil => grind
        | cons => grind [destruct_map, lmap, rmap]

Goal state after:
α : Type u
β : Type v
f : α → β
S✝ : WSeq (Computation α)
c1 c2 : Computation β
h : ∃ l S, c1 = map f (corec parallel.aux1 (l, S)) ∧ c2 = corec parallel.aux1 (List.map (map f) l, WSeq.map (map f) S)
l : List (Computation α)
S : WSeq (Computation α)
this : parallel.aux2 (List.map (map f) l) = lmap f (rmap (List.map (map f)) (parallel.aux2 l))
⊢ BisimO
    (fun c1 c2 ↦
      ∃ l S,
        c1 = map f (corec parallel.aux1 (l, S)) ∧ c2 = corec parallel.aux1 (List.map (map f) l, WSeq.map (map f) S))
    (map f (corec parallel.aux1 (l, S))).destruct
    (corec parallel.aux1 (List.map (map f) l, WSeq.map (map f) S)).destruct
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
s : σ
xs : Vector α n
ys : Vector β n
f : α → β → σ → σ × γ
f' : β → σ → σ × γ
h : ∀ (a : α) (b : β) (s : σ), f a b s = f' b s
⊢ mapAccumr₂ f xs ys s = mapAccumr f' ys s

Tactic:
induction xs, ys using Vector.revInductionOn₂ generalizing s with

Goal state after:
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
s : σ
xs : Vector α n
ys : Vector β n
f : α → β → σ → σ × γ
f' : α → σ → σ × γ
h : ∀ (a : α) (b : β) (s : σ), f a b s = f' a s
⊢ mapAccumr₂ f xs ys s = mapAccumr f' xs s

Tactic:
induction xs, ys using Vector.revInductionOn₂ generalizing s with

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

Goal state before:
pp: α : Type u
s : WSeq α
inst✝ : s.Productive
n m : ℕ
⊢ ((s.drop n).get? m).Terminates

Tactic:
rw [← get?_add]; infer_instance

Goal state after:
Module: Mathlib.Data.ZMod.Factorial

Goal state before:
pp: n p : ℕ
h : n ≤ p
x : ℕ
⊢ x ∈ range n → ↑(p - 1 - x) = -1 * ↑(x + 1)

Tactic:
hx

Goal state after:
n p : ℕ
h : n ≤ p
x : ℕ
hx : x ∈ range n
⊢ ↑(p - 1 - x) = -1 * ↑(x + 1)
Module: Mathlib.Dynamics.Ergodic.Action.Regular

Goal state before:
pp: G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulLeftInvariant
s : Set G
hsm : MeasurableSet s
hs : ∀ (g : G), (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s
hμs : ∃ᵐ (x : G) ∂μ, x ∈ s
⊢ MeasurableSet {x | x.2 * x.1 ∈ s ↔ x.1 ∈ s}

Tactic:
· exact ((hsm.preimage <| measurable_snd.mul measurable_fst).mem.iff
        (hsm.preimage measurable_fst).mem).setOf

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

Goal state before:
pp: f : CircleDeg1Lift
n : ℕ
⊢ ↑(↑n * ⌊f 0⌋) ≤ (⇑f)^[n] 0

Tactic:
Int.cast_mul,

Goal state after:
f : CircleDeg1Lift
n : ℕ
⊢ ↑↑n * ↑⌊f 0⌋ ≤ (⇑f)^[n] 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 ≠ 0

Tactic:
← abs_one

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.Function

Goal state before:
pp: case _b
α : Type u_1
X : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : Nonempty X
inst✝¹ : MeasurableSpace X
s : Set X
inst✝ : MeasurableSpace.CountablySeparated ↑s
f : α → α
g : α → X
h : QuasiErgodic f μ
hs : ∀ᵐ (x : α) ∂μ, g x ∈ s
hgm : NullMeasurable g μ
hg_eq : g ∘ f =ᵐ[μ] g
U : Set X
hU : MeasurableSet U
x : α
hx : (g ∘ f) x = g x
⊢ (g ∘ f) x ∈ U ↔ g x ∈ U

Tactic:
hx

Goal state after:
case _b
α : Type u_1
X : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : Nonempty X
inst✝¹ : MeasurableSpace X
s : Set X
inst✝ : MeasurableSpace.CountablySeparated ↑s
f : α → α
g : α → X
h : QuasiErgodic f μ
hs : ∀ᵐ (x : α) ∂μ, g x ∈ s
hgm : NullMeasurable g μ
hg_eq : g ∘ f =ᵐ[μ] g
U : Set X
hU : MeasurableSet U
x : α
hx : (g ∘ f) x = g x
⊢ g x ∈ U ↔ g x ∈ U
Module: Mathlib.Dynamics.Ergodic.Function

Goal state before:
pp: α : Type u_1
X : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace X
inst✝¹ : MetrizableSpace X
inst✝ : Nonempty X
f : α → α
g : α → X
h : QuasiErgodic f μ
hgm : AEStronglyMeasurable g μ
hg_eq : g ∘ f =ᵐ[μ] g
⊢ ∃ c, g =ᵐ[μ] const α c

Tactic:
borelize X
  rcases hgm.isSeparable_ae_range with ⟨t, ht, hgt⟩
  have := ht.secondCountableTopology
  exact h.ae_eq_const_of_ae_eq_comp_of_ae_range₀ hgt hgm.aemeasurable.nullMeasurable hg_eq

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : ν.HaveLebesgueDecomposition μ
inst✝ : SigmaFinite μ
hμν : μ ≪ ν
x : α
⊢ 0 < (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ x →
    (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ x = ν.rnDeriv μ x → 0 < ν.rnDeriv μ x

Tactic:
hx

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : ν.HaveLebesgueDecomposition μ
inst✝ : SigmaFinite μ
hμν : μ ≪ ν
x : α
hx : 0 < (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ x
⊢ (μ.withDensity (ν.rnDeriv μ)).rnDeriv μ x = ν.rnDeriv μ x → 0 < ν.rnDeriv μ x
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_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
μ' : Measure α := ν.withDensity (μ.rnDeriv ν)
hμ'ν : μ' ≪ ν
h : (μ'.withDensity f).rnDeriv ν =ᵐ[ν] fun x ↦ f x * μ'.rnDeriv ν x
h1 : μ'.rnDeriv ν =ᵐ[ν] μ.rnDeriv ν
h2 : (μ'.withDensity f).rnDeriv ν =ᵐ[ν] (μ.withDensity f).rnDeriv ν
x : α
⊢ (μ'.withDensity f).rnDeriv ν x = f x * μ'.rnDeriv ν x →
    μ'.rnDeriv ν x = μ.rnDeriv ν x →
      (μ'.withDensity f).rnDeriv ν x = (μ.withDensity f).rnDeriv ν x →
        (μ.withDensity f).rnDeriv ν x = f x * μ.rnDeriv ν x

Tactic:
hx

Goal state after:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hfν : AEMeasurable f ν
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
μ' : Measure α := ν.withDensity (μ.rnDeriv ν)
hμ'ν : μ' ≪ ν
h : (μ'.withDensity f).rnDeriv ν =ᵐ[ν] fun x ↦ f x * μ'.rnDeriv ν x
h1 : μ'.rnDeriv ν =ᵐ[ν] μ.rnDeriv ν
h2 : (μ'.withDensity f).rnDeriv ν =ᵐ[ν] (μ.withDensity f).rnDeriv ν
x : α
hx : (μ'.withDensity f).rnDeriv ν x = f x * μ'.rnDeriv ν x
⊢ μ'.rnDeriv ν x = μ.rnDeriv ν x →
    (μ'.withDensity f).rnDeriv ν x = (μ.withDensity f).rnDeriv ν x → (μ.withDensity f).rnDeriv ν x = f x * μ.rnDeriv ν x
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
ex : ∃ w' ∈ p.support, v * w' = v * w
h1 : p.mulShift v (v * w) = p.config (Classical.choose ex)
⊢ p.mulShift v (v * w) = p.config w

Tactic:
have hwv' : v * Classical.choose ex = v * w := (Classical.choose_spec ex).2

Goal state after:
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
ex : ∃ w' ∈ p.support, v * w' = v * w
h1 : p.mulShift v (v * w) = p.config (Classical.choose ex)
hwv' : v * Classical.choose ex = v * w
⊢ p.mulShift v (v * w) = p.config w
Module: Mathlib.Dynamics.SymbolicDynamics.Basic

Goal state before:
pp: A : Type u_3
G : Type u_4
inst✝¹ : Inhabited A
inst✝ : Monoid G
F : Set (Pattern A G)
h : G
x : G → A
⊢ x ∈ mulForbidden F → mulShift h x ∈ mulForbidden F

Tactic:
hx

Goal state after:
A : Type u_3
G : Type u_4
inst✝¹ : Inhabited A
inst✝ : Monoid G
F : Set (Pattern A G)
h : G
x : G → A
hx : x ∈ mulForbidden F
⊢ mulShift h x ∈ mulForbidden F
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
x : α
⊢ f x ≠ ∞ → f x < ∞

Tactic:
hx

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
x : α
hx : f x ≠ ∞
⊢ f x < ∞
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 : α
⊢ (μ.restrict t).rnDeriv ν' x = t.indicator (μ.rnDeriv ν') x → x ∈ t → μ.rnDeriv ν' x = (μ.restrict t).rnDeriv ν' x

Tactic:
hx

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 : α
hx : (μ.restrict t).rnDeriv ν' x = 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 α
u : Set τ
hu : u ∈ f
a✝ : β
⊢ a✝ ∈ ⋂ u, closure[inst✝] (image2 ϕ (↑u) s) → a✝ ∈ closure[inst✝] (image2 ϕ u s)

Tactic:
hx

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 : a✝ ∈ ⋂ u, closure[inst✝] (image2 ϕ (↑u) s)
⊢ a✝ ∈ closure[inst✝] (image2 ϕ u s)
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

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

Tactic:
refine ⟨sn.toFinset, ?_, ?_⟩

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

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝² : μ.HaveLebesgueDecomposition ν
inst✝¹ : ν.HaveLebesgueDecomposition μ
inst✝ : SigmaFinite μ
hμν : μ ≪ ν
hνμ : ν ≪ μ
x : α
⊢ 0 < μ.rnDeriv ν x → μ.rnDeriv ν x ≠ 0

Tactic:
hx

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝² : μ.HaveLebesgueDecomposition ν
inst✝¹ : ν.HaveLebesgueDecomposition μ
inst✝ : SigmaFinite μ
hμν : μ ≪ ν
hνμ : ν ≪ μ
x : α
hx : 0 < μ.rnDeriv ν x
⊢ μ.rnDeriv ν x ≠ 0
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

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

Tactic:
hx

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

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

Tactic:
hx

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

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
p : α → Prop
h : ∀ᵐ (a : α) ∂μ, p a
this : ∀ᵐ (x : α) ∂ν.singularPart μ, μ.rnDeriv ν x = 0
x : α
⊢ μ.rnDeriv ν x = 0 → μ.rnDeriv ν x ≠ 0 → p x

Tactic:
hx

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
p : α → Prop
h : ∀ᵐ (a : α) ∂μ, p a
this : ∀ᵐ (x : α) ∂ν.singularPart μ, μ.rnDeriv ν x = 0
x : α
hx : μ.rnDeriv ν x = 0
⊢ μ.rnDeriv ν x ≠ 0 → p x
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: X : Type u_1
T : X → X
U : SetRel X X
F : Set X
n : ℕ
inst✝ : U.IsSymm
s : Finset X
h' : ↑(#s) = coverMincard T F U n
x : X
x_s : x ∈ s
ball_empt : F ∩ ball x (dynEntourage T U n) = ∅
y : X
y_F : y ∈ F
z : X
z_s : z ∈ s
hz : (y, x) ∈ dynEntourage T U n
z_x : z = x
⊢ y ∈ F ∩ ball x (dynEntourage T U n)

Tactic:
exact mem_inter y_F <| (dynEntourage T U n).symm hz

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

Goal state before:
pp: case h'
X : Type u_1
F : Set X
T : X → X
h : F.Nonempty
U : SetRel X X
⊢ (fun n ↦ ↑(coverMincard T F U n)) ≠ 0

Tactic:
· rw [ne_eq, funext_iff.not, not_forall]
    use 0
    rw [coverMincard_zero T h U, Pi.zero_apply, ENat.toENNReal_one]
    exact one_ne_zero

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : (map (algebraMap F q.SplittingField) p).Splits
hp : Group.IsSolvable p.Gal
hq : Group.IsSolvable (map (algebraMap F p.SplittingField) q).Gal
K : Type u_1 := p.SplittingField
L : Type u_1 := q.SplittingField
this : Fact (map (algebraMap F L) p).Splits
ϕ : Gal(L/K) ≃* (map (algebraMap F K) q).Gal := (IsSplittingField.algEquiv L (map (algebraMap F K) q)).autCongr
ϕ_inj : Function.Injective ⇑ϕ.toMonoidHom
⊢ Group.IsSolvable q.Gal

Tactic:
have : Group.IsSolvable Gal(K/F) := hp

Goal state after:
F : Type u_1
inst✝ : Field F
p q : F[X]
hpq : (map (algebraMap F q.SplittingField) p).Splits
hp : Group.IsSolvable p.Gal
hq : Group.IsSolvable (map (algebraMap F p.SplittingField) q).Gal
K : Type u_1 := p.SplittingField
L : Type u_1 := q.SplittingField
this✝ : Fact (map (algebraMap F L) p).Splits
ϕ : Gal(L/K) ≃* (map (algebraMap F K) q).Gal := (IsSplittingField.algEquiv L (map (algebraMap F K) q)).autCongr
ϕ_inj : Function.Injective ⇑ϕ.toMonoidHom
this : Group.IsSolvable Gal(K/F)
⊢ Group.IsSolvable q.Gal
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: case refine_3
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
s : Set α
x✝¹ : MeasurableSet s
x✝ : ν s < ∞
hs_eq : s = f ⁻¹' f '' s
this : SigmaFinite (map f ν)
⊢ (map f μ) (f '' s) = μ (f ⁻¹' f '' s)

Tactic:
hf.map_apply

Goal state after:
case refine_3
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
s : Set α
x✝¹ : MeasurableSet s
x✝ : ν s < ∞
hs_eq : s = f ⁻¹' f '' s
this : SigmaFinite (map f ν)
⊢ μ (f ⁻¹' f '' s) = μ (f ⁻¹' f '' s)
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μν : μ ≪ ν
⊢ Integrable (fun x ↦ (μ.rnDeriv ν x).toReal • f x) ν ↔ Integrable f (ν.withDensity (μ.rnDeriv ν))

Tactic:
rw [← integrable_withDensity_iff_integrable_smul' (E := E)
    (measurable_rnDeriv μ ν) (rnDeriv_lt_top μ ν)]

Goal state after:
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
x : M
⊢ (refl L M) x = x

Tactic:
simp [refl]; rfl

Goal state after:
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
motive : (x : E) → x ∈ solvableByRad F E → Prop
mem : ∀ (x : F), motive ((algebraMap F E) x) ⋯
add :
  ∀ (x y : E) (hx : x ∈ solvableByRad F E) (hy : y ∈ solvableByRad F E), motive x hx → motive y hy → motive (x + y) ⋯
mul :
  ∀ (x y : E) (hx : x ∈ solvableByRad F E) (hy : y ∈ solvableByRad F E), motive x hx → motive y hy → motive (x * y) ⋯
rad : ∀ (n : ℕ) (x : E) (hn : n ≠ 0) (hx : x ^ n ∈ solvableByRad F E), motive (x ^ n) hx → motive x ⋯
x : E
hx : x ∈ solvableByRad F E
⊢ motive x hx

Tactic:
let s : Subalgebra F E :=
  { carrier := {x | ∃ hx : x ∈ solvableByRad F E, motive x hx}
    algebraMap_mem' a := ⟨algebraMap_mem _ a, mem a⟩
    add_mem' := fun ⟨ha, ha'⟩ ⟨hb, hb'⟩ ↦ ⟨add_mem ha hb, add _ _ ha hb ha' hb'⟩
    mul_mem' := fun ⟨ha, ha'⟩ ⟨hb, hb'⟩ ↦ ⟨mul_mem ha hb, mul _ _ ha hb ha' hb'⟩ }

Goal state after:
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
motive : (x : E) → x ∈ solvableByRad F E → Prop
mem : ∀ (x : F), motive ((algebraMap F E) x) ⋯
add :
  ∀ (x y : E) (hx : x ∈ solvableByRad F E) (hy : y ∈ solvableByRad F E), motive x hx → motive y hy → motive (x + y) ⋯
mul :
  ∀ (x y : E) (hx : x ∈ solvableByRad F E) (hy : y ∈ solvableByRad F E), motive x hx → motive y hy → motive (x * y) ⋯
rad : ∀ (n : ℕ) (x : E) (hn : n ≠ 0) (hx : x ^ n ∈ solvableByRad F E), motive (x ^ n) hx → motive x ⋯
x : E
hx : x ∈ solvableByRad F E
s : Subalgebra F E :=
  { carrier := {x | ∃ (hx : x ∈ solvableByRad F E), motive x hx}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯,
    zero_mem' := ⋯, algebraMap_mem' := ⋯ }
⊢ motive x hx
Module: Mathlib.ModelTheory.Algebra.Field.Basic

Goal state before:
pp: case leftDistrib
K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
⊢ toProp K leftDistrib

Tactic:
| leftDistrib =>

Goal state after:
Module: Mathlib.ModelTheory.Algebra.Field.CharP

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
⊢ K ⊨ (fun q ↦ ∼(eqZero q)) '' {q | Nat.Prime q} ↔ CharP K 0

Tactic:
simp only [Theory.model_iff, Set.mem_image, Set.mem_ofPred_eq, Sentence.Realize,
      forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, Formula.realize_not,
      realize_eqZero, ← CharZero.charZero_iff_forall_prime_ne_zero]

Goal state after:
case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : CompatibleRing K
⊢ CharZero K ↔ CharP K 0
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: case succ
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝³ : L.Structure M
inst✝² : L.Structure N
inst✝¹ : L.Structure P
S : L.Substructure M
s : Set M
inst✝ : IsEmpty L.Constants
x✝ : M
n✝ : ℕ
f : L.Functions (n✝ + 1)
x : Fin (n✝ + 1) → M
⊢ (∀ (i : Fin (n✝ + 1)), x i ∈ ∅) → funMap f x ∈ ∅

Tactic:
hx

Goal state after:
case succ
L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝³ : L.Structure M
inst✝² : L.Structure N
inst✝¹ : L.Structure P
S : L.Substructure M
s : Set M
inst✝ : IsEmpty L.Constants
x✝ : M
n✝ : ℕ
f : L.Functions (n✝ + 1)
x : Fin (n✝ + 1) → M
hx : ∀ (i : Fin (n✝ + 1)), x i ∈ ∅
⊢ funMap f x ∈ ∅
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
N : Type u_1
P : Type u_2
inst✝² : L.Structure M
inst✝¹ : L.Structure N
inst✝ : L.Structure P
S✝ : L.Substructure M
s : Set M
φ : M →[L] N
S : L.Substructure M
n : ℕ
f : L.Functions n
x : Fin n → N
hx : ∀ (i : Fin n), x i ∈ ⇑φ '' ↑S
⊢ funMap f (⇑φ ∘ fun i ↦ Classical.choose ⋯) = funMap f x

Tactic:
exact congr rfl (funext fun i => (Classical.choose_spec (hx i)).2)

Goal state after:
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
p : (x : M) → x ∈ (closure L).toFun s → Prop
Hs : ∀ (x : M) (h : x ∈ s), p x ⋯
Hfun : ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f {x | ∃ (hx : x ∈ (closure L).toFun s), p x hx}
x : M
hx : x ∈ (closure L).toFun s
⊢ p x hx

Tactic:
refine Exists.elim ?_ fun (hx : x ∈ closure L s) (hc : p x hx) => hc

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
p : (x : M) → x ∈ (closure L).toFun s → Prop
Hs : ∀ (x : M) (h : x ∈ s), p x ⋯
Hfun : ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f {x | ∃ (hx : x ∈ (closure L).toFun s), p x hx}
x : M
hx : x ∈ (closure L).toFun s
⊢ ∃ (x_1 : x ∈ (closure L).toFun s), p x x_1
Module: Mathlib.ModelTheory.ElementarySubstructures

Goal state before:
pp: L : Language
M : Type u_1
inst✝ : L.Structure M
A : Set M
hA : MeetsDefinable A
x : M
⊢ x ∈ range (Term.realize Subtype.val) → x ∈ A

Tactic:
hx

Goal state after:
L : Language
M : Type u_1
inst✝ : L.Structure M
A : Set M
hA : MeetsDefinable A
x : M
hx : x ∈ range (Term.realize Subtype.val)
⊢ x ∈ A
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
B : Set M
s : Set (α → M)
hAs : A.Definable L s
hAB : A ⊆ B
⊢ B.Definable L s

Tactic:
rw [definable_iff_empty_definable_with_params] at *
  exact hAs.map_expansion (L.lhomWithConstantsMap (Set.inclusion hAB))

Goal state after: