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

Goal state before:
pp: case map_eq
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
s : Set X
hs : MeasurableSet s
⊢ (ν.withDensity (μ.rnDeriv ν)) (f ⁻¹' s) + (μ.singularPart ν) s = (ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν) s

Tactic:
rnDeriv_add_singularPart,

Goal state after:
case map_eq
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
s : Set X
hs : MeasurableSet s
⊢ (ν.withDensity (μ.rnDeriv ν)) (f ⁻¹' s) + (μ.singularPart ν) s = μ s
Module: Mathlib.Dynamics.Ergodic.RadonNikodym

Goal state before:
pp: case map_eq
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
s : Set X
hs : MeasurableSet s
⊢ (ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν) (f ⁻¹' s) = μ s

Tactic:
rnDeriv_add_singularPart,

Goal state after:
case map_eq
X : Type u_1
m : MeasurableSpace X
μ ν : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : SigmaFinite ν
f : X → X
hfμ : MeasurePreserving f μ μ
hfν : MeasurePreserving f ν ν
s : Set X
hs : MeasurableSet s
⊢ μ (f ⁻¹' s) = μ s
Module: Mathlib.Dynamics.Ergodic.Extreme

Goal state before:
pp: case refine_1
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
c : ℝ≥0∞
hc : c ≠ ∞
hf : MeasurePreserving f μ μ
hc₀ : c ≠ 0
this✝ : IsFiniteMeasure μ
S : Set (Measure X) := {ν | MeasurePreserving f ν ν ∧ ν univ = c}
h : μ ∈ extremePoints ℝ≥0∞ S
this : ∀ {s : Set X}, MeasurableSet s → f ⁻¹' s = s → μ s ≠ 0 → c • μ[|s] ∈ S
s : Set X
hsm : MeasurableSet s
hfs : f ⁻¹' s = s
H : ¬EventuallyConst s (ae μ)
hs : μ s ≠ 0
hs' : μ sᶜ ≠ 0
⊢ μ s / c + μ sᶜ / c = 1

pp: case refine_2
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
c : ℝ≥0∞
hc : c ≠ ∞
hf : MeasurePreserving f μ μ
hc₀ : c ≠ 0
this✝ : IsFiniteMeasure μ
S : Set (Measure X) := {ν | MeasurePreserving f ν ν ∧ ν univ = c}
h : μ ∈ extremePoints ℝ≥0∞ S
this : ∀ {s : Set X}, MeasurableSet s → f ⁻¹' s = s → μ s ≠ 0 → c • μ[|s] ∈ S
s : Set X
hsm : MeasurableSet s
hfs : f ⁻¹' s = s
H : ¬EventuallyConst s (ae μ)
hs : μ s ≠ 0
hs' : μ sᶜ ≠ 0
⊢ (μ s / c) • c • μ[|s] + (μ sᶜ / c) • c • μ[|sᶜ] = μ

Tactic:
· rw [← ENNReal.add_div, measure_add_measure_compl hsm, h.1.2, ENNReal.div_self hc₀ hc]

Goal state after:
case refine_2
X : Type u_1
m : MeasurableSpace X
μ : Measure X
f : X → X
c : ℝ≥0∞
hc : c ≠ ∞
hf : MeasurePreserving f μ μ
hc₀ : c ≠ 0
this✝ : IsFiniteMeasure μ
S : Set (Measure X) := {ν | MeasurePreserving f ν ν ∧ ν univ = c}
h : μ ∈ extremePoints ℝ≥0∞ S
this : ∀ {s : Set X}, MeasurableSet s → f ⁻¹' s = s → μ s ≠ 0 → c • μ[|s] ∈ S
s : Set X
hsm : MeasurableSet s
hfs : f ⁻¹' s = s
H : ¬EventuallyConst s (ae μ)
hs : μ s ≠ 0
hs' : μ sᶜ ≠ 0
⊢ (μ s / c) • c • μ[|s] + (μ sᶜ / c) • c • μ[|sᶜ] = μ
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: case refine_1
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
⊢ AEMeasurable (fun x ↦ f x * μ.rnDeriv ν x) ν

pp: case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
⊢ μ.withDensity f = 0 + ν.withDensity fun x ↦ f x * μ.rnDeriv ν x

Tactic:
· exact hf.mul (Measure.measurable_rnDeriv _ _).aemeasurable

Goal state after:
case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : AEMeasurable f ν
⊢ μ.withDensity f = 0 + ν.withDensity fun 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
⊢ p.mulShift v (v * w) = p.config (Classical.choose ex)

Tactic:
simp [Pattern.mulShift, hmem]

Goal state after:
Module: Mathlib.Dynamics.OmegaLimit

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

Tactic:
contrapose!

Goal state after:
case mp
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s₁ s₂ : Set α
y : β
⊢ ((∃ n ∈ 𝓝 y, ∀ᶠ (x : τ) in f, s₁ ∩ ϕ x ⁻¹' n = ∅) ∧ ∃ n ∈ 𝓝 y, ∀ᶠ (x : τ) in f, s₂ ∩ ϕ x ⁻¹' n = ∅) →
    ∃ n ∈ 𝓝 y, (∀ᶠ (x : τ) in f, s₁ ∩ ϕ x ⁻¹' n = ∅) ∧ ∀ᶠ (x : τ) in f, s₂ ∩ ϕ x ⁻¹' n = ∅
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 ν')
⊢ μ.rnDeriv ν' =ᵐ[ν.restrict t] (μ.restrict t).rnDeriv ν'

Tactic:
Filter.EventuallyEq,

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 : α) ∂ν.restrict t, μ.rnDeriv ν' x = (μ.restrict t).rnDeriv ν' x
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: X : Type u_1
T : X → X
F : Set X
U : SetRel X X
n : ℕ
⊢ 1 ≤ coverMincard T F U n ↔ F.Nonempty

Tactic:
by
  rw [Order.one_le_iff_ne_zero, nonempty_iff_ne_empty, not_iff_not]
  exact coverMincard_eq_zero_iff T F U n

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

Goal state before:
pp: X : Type u_1
inst✝ : UniformSpace X
T : X → X
F G : Set X
hF : F ⊆ G
hG : MapsTo T G G
⊢ coverEntropy T (G ∩ F) = coverEntropy T F

Tactic:
inter_eq_right.2 hF

Goal state after:
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F G : Set X
hF : F ⊆ G
hG : MapsTo T G G
⊢ coverEntropy T F = coverEntropy T F
Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj

Goal state before:
pp: X : Type u_1
inst✝ : UniformSpace X
T : X → X
F G : Set X
hF : F ⊆ G
hG : MapsTo T G G
⊢ coverEntropyInf T (G ∩ F) = coverEntropyInf T F

Tactic:
inter_eq_right.2 hF

Goal state after:
X : Type u_1
inst✝ : UniformSpace X
T : X → X
F G : Set X
hF : F ⊆ G
hG : MapsTo T G G
⊢ coverEntropyInf T F = coverEntropyInf T F
Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
inst✝ : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F G : Set X
h' : UniformContinuousOn φ G
hF : F ⊆ G
hG : MapsTo S G G
hφ : Semiconj (G.domRestrict φ) (MapsTo.restrict S G G hG) T
⊢ coverEntropy T (φ '' (G ∩ F)) = coverEntropy T (φ '' F)

Tactic:
inter_eq_right.2 hF

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
inst✝ : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F G : Set X
h' : UniformContinuousOn φ G
hF : F ⊆ G
hG : MapsTo S G G
hφ : Semiconj (G.domRestrict φ) (MapsTo.restrict S G G hG) T
⊢ coverEntropy T (φ '' F) = coverEntropy T (φ '' F)
Module: Mathlib.Dynamics.TopologicalEntropy.Semiconj

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
inst✝ : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F G : Set X
h' : UniformContinuousOn φ G
hF : F ⊆ G
hG : MapsTo S G G
hφ : Semiconj (G.domRestrict φ) (MapsTo.restrict S G G hG) T
⊢ coverEntropyInf T (φ '' (G ∩ F)) = coverEntropyInf T (φ '' F)

Tactic:
inter_eq_right.2 hF

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
inst✝ : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
F G : Set X
h' : UniformContinuousOn φ G
hF : F ⊆ G
hG : MapsTo S G G
hφ : Semiconj (G.domRestrict φ) (MapsTo.restrict S G G hG) T
⊢ coverEntropyInf T (φ '' F) = coverEntropyInf T (φ '' F)
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, (fun x ↦ m • x) ⁻¹' U)

Tactic:
simp only [dense_iff_inter_open, inter_iUnion, nonempty_iUnion, ← image_inter_nonempty_iff]

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

Goal state before:
pp: case inr.inr
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 < ⊤
s : Finset X
s_cover : IsDynCoverOf T F U n ↑s
s_coverMincard : ↑s.card = coverMincard T F U n
t : Finset X
t_cover : IsDynCoverOf T G U n ↑t
t_coverMincard : ↑t.card = coverMincard T G U n
⊢ coverMincard T (F ∪ G) U n ≤ ↑(s.card + t.card)

Tactic:
apply (IsDynCoverOf.coverMincard_le_card _).trans (WithTop.coe_mono (s.card_union_le t))

Goal state after:
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 < ⊤
s : Finset X
s_cover : IsDynCoverOf T F U n ↑s
s_coverMincard : ↑s.card = coverMincard T F U n
t : Finset X
t_cover : IsDynCoverOf T G U n ↑t
t_coverMincard : ↑t.card = coverMincard T G U n
⊢ IsDynCoverOf T (F ∪ G) U n ↑(s ∪ t)
Module: Mathlib.Dynamics.TopologicalEntropy.Subset

Goal state before:
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:
· exact max_le (coverEntropyEntourage_monotone T U subset_union_left)
      (coverEntropyEntourage_monotone T U subset_union_right)

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ν : ν ≪ ξ
h1✝ : μ.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ =ᵐ[ξ] μ.rnDeriv ξ
h2✝ : ν.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ =ᵐ[ξ] ν.rnDeriv ξ
h_ac : μ + ν ≪ ξ
a : α
h1 : (μ.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ) a = μ.rnDeriv ξ a
h2 : (ν.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ) a = ν.rnDeriv ξ a
h_lt_top1 : (μ + ν).rnDeriv ξ a < ∞
h_lt_top2 : ν.rnDeriv (μ + ν) a < ∞
h_pos : 0 < (μ + ν).rnDeriv ξ a
⊢ (μ.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ) a / ν.rnDeriv ξ a = μ.rnDeriv (μ + ν) a / ν.rnDeriv (μ + ν) a

Tactic:
← h2,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite ξ
hμ : μ ≪ ξ
hν : ν ≪ ξ
h1✝ : μ.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ =ᵐ[ξ] μ.rnDeriv ξ
h2✝ : ν.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ =ᵐ[ξ] ν.rnDeriv ξ
h_ac : μ + ν ≪ ξ
a : α
h1 : (μ.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ) a = μ.rnDeriv ξ a
h2 : (ν.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ) a = ν.rnDeriv ξ a
h_lt_top1 : (μ + ν).rnDeriv ξ a < ∞
h_lt_top2 : ν.rnDeriv (μ + ν) a < ∞
h_pos : 0 < (μ + ν).rnDeriv ξ a
⊢ (μ.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ) a / (ν.rnDeriv (μ + ν) * (μ + ν).rnDeriv ξ) a =
    μ.rnDeriv (μ + ν) a / ν.rnDeriv (μ + ν) a
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
this✝¹ : SigmaFinite (map f ν)
this✝ : SigmaFinite (map f (μ.singularPart ν))
this : SigmaFinite (map f (ν.withDensity (μ.rnDeriv ν)))
h_add :
  (map f (μ.singularPart ν) + map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν) =ᵐ[map f ν]
    (map f (μ.singularPart ν)).rnDeriv (map f ν) + (map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν)
⊢ (fun x ↦ (map f (μ.singularPart ν) + map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν) (f x)) =ᵐ[ν]
    (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv ν

Tactic:
Filter.EventuallyEq,

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
this✝¹ : SigmaFinite (map f ν)
this✝ : SigmaFinite (map f (μ.singularPart ν))
this : SigmaFinite (map f (ν.withDensity (μ.rnDeriv ν)))
h_add :
  ∀ᵐ (x : β) ∂map f ν,
    (map f (μ.singularPart ν) + map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν) x =
      ((map f (μ.singularPart ν)).rnDeriv (map f ν) + (map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν)) x
⊢ (fun x ↦ (map f (μ.singularPart ν) + map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν) (f x)) =ᵐ[ν]
    (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
this✝² : SigmaFinite (map f ν)
this✝¹ : SigmaFinite (map f (μ.singularPart ν))
this✝ : SigmaFinite (map f (ν.withDensity (μ.rnDeriv ν)))
h_add :
  (fun x ↦ (map f (μ.singularPart ν) + map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν) (f x)) =ᵐ[ν] fun x ↦
    ((map f (μ.singularPart ν)).rnDeriv (map f ν) + (map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν)) (f x)
this : (fun x ↦ (map f (μ.singularPart ν)).rnDeriv (map f ν) x) =ᵐ[map f ν] 0
⊢ (fun x ↦ (map f (μ.singularPart ν)).rnDeriv (map f ν) (f x)) =ᵐ[ν] 0

Tactic:
Filter.EventuallyEq,

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
this✝² : SigmaFinite (map f ν)
this✝¹ : SigmaFinite (map f (μ.singularPart ν))
this✝ : SigmaFinite (map f (ν.withDensity (μ.rnDeriv ν)))
h_add :
  (fun x ↦ (map f (μ.singularPart ν) + map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν) (f x)) =ᵐ[ν] fun x ↦
    ((map f (μ.singularPart ν)).rnDeriv (map f ν) + (map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν)) (f x)
this : ∀ᵐ (x : β) ∂map f ν, (map f (μ.singularPart ν)).rnDeriv (map f ν) x = 0 x
⊢ (fun x ↦ (map f (μ.singularPart ν)).rnDeriv (map f ν) (f x)) =ᵐ[ν] 0
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
this✝¹ : SigmaFinite (map f ν)
this✝ : SigmaFinite (map f (μ.singularPart ν))
this : SigmaFinite (map f (ν.withDensity (μ.rnDeriv ν)))
h_add :
  (fun x ↦ (map f (μ.singularPart ν) + map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν) (f x)) =ᵐ[ν] fun x ↦
    ((map f (μ.singularPart ν)).rnDeriv (map f ν) + (map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν)) (f x)
⊢ (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν =ᵐ[ν] fun x ↦ (map f (ν.withDensity (μ.rnDeriv ν))).rnDeriv (map f ν) (f x)

Tactic:
exact (hf.rnDeriv_map_aux (withDensity_absolutelyContinuous _ _)).symm

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
⊢ map f (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)) =
    map f (μ.singularPart ν) + (map f ν).withDensity ((map f μ).rnDeriv (map f ν))

Tactic:
Measure.map_add _ _ hf.measurable,

Goal state after:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
⊢ map f (μ.singularPart ν) + map f (ν.withDensity (μ.rnDeriv ν)) =
    map f (μ.singularPart ν) + (map f ν).withDensity ((map f μ).rnDeriv (map f ν))
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
β : Type u_2
m : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
⊢ (map f μ).singularPart (map f ν) = map f (μ.singularPart ν)

Tactic:
have h_add : μ.map f = (μ.singularPart ν).map f
      + (ν.map f).withDensity ((μ.map f).rnDeriv (ν.map f)) := by
    conv_lhs => rw [μ.haveLebesgueDecomposition_add ν]
    rw [Measure.map_add _ _ hf.measurable, ← hf.map_withDensity_rnDeriv μ ν]
  refine (Measure.eq_singularPart (Measure.measurable_rnDeriv _ _) ?_ h_add).symm
  exact hf.mutuallySingular_map (μ.mutuallySingular_singularPart ν)

Goal state after:
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
L' : Language
⊢ IsEmpty Language.empty.Symbols

Tactic:
simp only [Language.Symbols, isEmpty_sum, isEmpty_sigma]

Goal state after:
L : Language
L' : Language
⊢ (∀ (a : ℕ), IsEmpty (Language.empty.Functions a)) ∧ ∀ (a : ℕ), IsEmpty (Language.empty.Relations a)
Module: Mathlib.FieldTheory.IsAlgClosed.Classification

Goal state before:
pp: K : Type u
L : Type v
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : IsAlgClosed K
inst✝³ : IsAlgClosed L
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
this✝ : Algebra (ZMod p) K := ZMod.algebra K p
this : Algebra (ZMod p) L := ZMod.algebra L p
s : Set K
hs : IsTranscendenceBasis (ZMod p) Subtype.val
t : Set L
ht : IsTranscendenceBasis (ZMod p) Subtype.val
hL : ℵ₀ < #L
⊢ Nonempty (K ≃+* L)

Tactic:
have : Cardinal.lift.{v} #s = Cardinal.lift.{u} #t := by
    rw [← lift_injective (cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt _
        hs (le_of_lt (lt_aleph0_of_finite _)) hK),
      ← lift_injective (cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt _
        ht (le_of_lt (lt_aleph0_of_finite _)) hL)]
    exact Cardinal.lift_mk_eq'.2 hKL

Goal state after:
K : Type u
L : Type v
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : IsAlgClosed K
inst✝³ : IsAlgClosed L
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP K p
inst✝ : CharP L p
hK : ℵ₀ < #K
hKL : Nonempty (K ≃ L)
this✝¹ : Algebra (ZMod p) K := ZMod.algebra K p
this✝ : Algebra (ZMod p) L := ZMod.algebra L p
s : Set K
hs : IsTranscendenceBasis (ZMod p) Subtype.val
t : Set L
ht : IsTranscendenceBasis (ZMod p) Subtype.val
hL : ℵ₀ < #L
this : Cardinal.lift.{v, u} #↑s = Cardinal.lift.{u, v} #↑t
⊢ Nonempty (K ≃+* L)
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: case func
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
v : β → M
l✝ : ℕ
f : L.Functions l✝
ts : Fin l✝ → L.Term (α ⊕ β)
ih : ∀ (a : Fin l✝), realize v (ts a).varsToConstants = realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (ts a)
⊢ realize v (func f ts).varsToConstants = realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (func f ts)

Tactic:
simp only [realize, constantsOn, constantsOnFunc, ih, varsToConstants]

Goal state after:
case func
L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
v : β → M
l✝ : ℕ
f : L.Functions l✝
ts : Fin l✝ → L.Term (α ⊕ β)
ih : ∀ (a : Fin l✝), realize v (ts a).varsToConstants = realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (ts a)
⊢ (funMap (Sum.inl f) fun i ↦ realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (ts i)) =
    funMap f fun i ↦ realize (Sum.elim (fun a ↦ ↑(L.con a)) v) (ts i)
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: L : Language
α : Type u'
t : L.Term α
h : listDecode t.listEncode = [t]
⊢ (do
        let a ← (listDecode t.listEncode).head?
        pure (some a)).join =
    some t

Tactic:
simp only [Option.join, h, head?_cons, Option.pure_def, Option.bind_eq_bind, Option.bind_some,
      id_eq]

Goal state after:
Module: Mathlib.ModelTheory.Substructures

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
n : ℕ
f : L.Functions n
x : Fin n → M
hx : ∀ (i : Fin n), ∃ y, Term.realize Subtype.val y = x i
⊢ Term.realize Subtype.val (func f fun i ↦ Classical.choose ⋯) = funMap f x

Tactic:
simp only [Term.realize, fun i => Classical.choose_spec (hx i)]

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
⊢ (Formula.iAlls β φ).Realize v ↔ ∀ (i : β → M), φ.Realize fun a ↦ Sum.elim v i a

Tactic:
let e := Classical.choice (Classical.choose_spec (Finite.exists_equiv_fin β))

Goal state after:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
e : β ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯
⊢ (Formula.iAlls β φ).Realize v ↔ ∀ (i : β → M), φ.Realize fun a ↦ Sum.elim v i a
Module: Mathlib.ModelTheory.ElementaryMaps

Goal state before:
pp: case refine_5.refine_2
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    φ.Realize default (Fin.snoc (⇑f ∘ x) a) → ∃ b, φ.Realize default (Fin.snoc (⇑f ∘ x) (f b))
n✝ : ℕ
φ✝ : L.BoundedFormula Empty n✝
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
ih : ∀ (xs : Fin (n + 1) → M), φ.Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ φ.Realize default xs
xs : Fin n → M
⊢ (∀ (a : M), φ.Realize default (Fin.snoc xs a)) → ∀ (a : N), φ.Realize (⇑f ∘ default) (Fin.snoc (⇑f ∘ xs) a)

Tactic:
contrapose!

Goal state after:
case refine_5.refine_2
L : Language
M : Type u_1
N : Type u_2
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ↪[L] N
htv :
  ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
    φ.Realize default (Fin.snoc (⇑f ∘ x) a) → ∃ b, φ.Realize default (Fin.snoc (⇑f ∘ x) (f b))
n✝ : ℕ
φ✝ : L.BoundedFormula Empty n✝
n : ℕ
φ : L.BoundedFormula Empty (n + 1)
ih : ∀ (xs : Fin (n + 1) → M), φ.Realize (⇑f ∘ default) (⇑f ∘ xs) ↔ φ.Realize default xs
xs : Fin n → M
⊢ (∃ a, ¬φ.Realize (⇑f ∘ default) (Fin.snoc (⇑f ∘ xs) a)) → ∃ a, ¬φ.Realize default (Fin.snoc xs a)
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
hx : x ∈ range (Term.realize Subtype.val)
⊢ x ∈ A

Tactic:
have : A.Definable₁ L {x} := by
    obtain ⟨t, rfl⟩ := hx
    use (Term.var 0).equal (t.relabel Sum.inl).varsToConstants
    simp [Set.ext_iff]

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)
this : A.Definable₁ L {x}
⊢ x ∈ A
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: case mpr
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
⊢ (∃ A0, ↑A0 ⊆ A ∧ (↑A0).Definable L s) → A.Definable L s

Tactic:
· rintro ⟨A0, hA0, hd⟩
    exact Definable.mono hd hA0

Goal state after:
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
⊢ (Formula.iExsUnique γ φ).Realize v ↔ ∃! i, φ.Realize (Sum.elim v i)

Tactic:
Formula.iExsUnique,

Goal state after:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
⊢ (Formula.iExs γ
          (φ ⊓
            Formula.iAlls γ
              ((Formula.relabel (fun a ↦ Sum.elim (Sum.inl ∘ Sum.inl) Sum.inr a) φ).imp
                (iInf fun g ↦ (var (Sum.inr g)).equal (var (Sum.inl (Sum.inr g))))))).Realize
      v ↔
    ∃! i, φ.Realize (Sum.elim v i)