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

Goal state before:
pp: case inr.inl
α : Type u
S : WSeq (Computation α)
a✝ : α
h✝ : a✝ ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
c : Computation α
l val✝ : List (Computation α)
IH : F l (Sum.inr val✝)
a : α
h : c.destruct = Sum.inl a
⊢ F (c :: l) (rmap (fun c' ↦ c' :: val✝) (Sum.inl a))

Tactic:
simp only [rmap]

Goal state after:
case inr.inl
α : Type u
S : WSeq (Computation α)
a✝ : α
h✝ : a✝ ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
c : Computation α
l val✝ : List (Computation α)
IH : F l (Sum.inr val✝)
a : α
h : c.destruct = Sum.inl a
⊢ F (c :: l) (Sum.inl a)
Module: Mathlib.Data.Seq.Parallel

Goal state before:
pp: case inr.inr
α : Type u
S : WSeq (Computation α)
a : α
h✝ : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
c : Computation α
l val✝ : List (Computation α)
IH : F l (Sum.inr val✝)
c' : Computation α
h : c.destruct = Sum.inr c'
⊢ F (c :: l) (rmap (fun c' ↦ c' :: val✝) (Sum.inr c'))

Tactic:
simp only [rmap]

Goal state after:
case inr.inr
α : Type u
S : WSeq (Computation α)
a : α
h✝ : a ∈ parallel S
F : List (Computation α) → α ⊕ List (Computation α) → Prop :=
  fun l a ↦ Sum.casesOn a (fun a ↦ ∃ c ∈ l, a ∈ c) fun l' ↦ ∀ (a' : α), (∃ c ∈ l', a' ∈ c) → ∃ c ∈ l, a' ∈ c
c : Computation α
l val✝ : List (Computation α)
IH : F l (Sum.inr val✝)
c' : Computation α
h : c.destruct = Sum.inr c'
⊢ F (c :: l) (Sum.inr (c' :: val✝))
Module: Mathlib.Data.Sigma.Order

Goal state before:
pp: case inl
ι : Type u_1
α : ι → Type u_2
inst✝³ : PartialOrder ι
inst✝² : OrderBot ι
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : OrderBot (α ⊥)
x✝ : Σₗ (i : ι), α i
b : α ⊥
⊢ ⟨⊥, ⊥⟩ ≤ ⟨⊥, b⟩

Tactic:
exact Lex.right _ _ bot_le

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : WSeq α
⊢ (map f s).destruct = Computation.map (Option.map (Prod.map f (map f))) s.destruct

Tactic:
apply
    Computation.eq_of_bisim fun c1 c2 =>
      ∃ s,
        c1 = destruct (map f s) ∧
          c2 = Computation.map (Option.map (Prod.map f (map f))) (destruct s)

Goal state after:
case bisim
α : Type u
β : Type v
f : α → β
s : WSeq α
⊢ Computation.IsBisimulation fun c1 c2 ↦
    ∃ s, c1 = (map f s).destruct ∧ c2 = Computation.map (Option.map (Prod.map f (map f))) s.destruct

case r
α : Type u
β : Type v
f : α → β
s : WSeq α
⊢ ∃ s_1,
    (map f s).destruct = (map f s_1).destruct ∧
      Computation.map (Option.map (Prod.map f (map f))) s.destruct =
        Computation.map (Option.map (Prod.map f (map f))) s_1.destruct
Module: Mathlib.Data.WSeq.Basic

Goal state before:
pp: case bisim
α : Type u
β : Type v
f : α → β
S : WSeq (WSeq α)
⊢ Seq.IsBisimulation fun s1 s2 ↦ ∃ s S, s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join

Tactic:
rintro s1 s2 ⟨s, S, rfl, rfl⟩

Goal state after:
case bisim
α : Type u
β : Type v
f : α → β
S✝ : WSeq (WSeq α)
s : WSeq β
S : WSeq (WSeq α)
⊢ Seq.BisimO (fun s1 s2 ↦ ∃ s S, s1 = s.append (map f S.join) ∧ s2 = s.append (map (map f) S).join)
    (Seq.destruct (s.append (map f S.join))) (Seq.destruct (s.append (map (map f) S).join))
Module: Mathlib.Data.WSeq.Relation

Goal state before:
pp: α : Type u
s✝¹ s' s✝ : WSeq α
h : (map ret s✝).join = s'
c1 c2 : Computation (Option (α × WSeq α))
s : WSeq α
this : ∀ (s : WSeq α), ∃ s', (map ret s).join.destruct = (map ret s').join.destruct ∧ s.destruct = s'.destruct
⊢ LiftRelAux (LiftRelO Eq fun s1 s2 ↦ (map ret s2).join = s1)
    (fun c1 c2 ↦ ∃ s, c1 = (map ret s).join.destruct ∧ c2 = s.destruct) (map ret s).join.destruct.destruct
    s.destruct.destruct

Tactic:
induction s using WSeq.recOn <;> simp [ret, this]

Goal state after:
Module: Mathlib.Data.W.Constructions

Goal state before:
pp: f : Natβ Natα.zero → WType Natβ
⊢ ofNat (mk Natα.zero f).toNat = mk Natα.zero f

Tactic:
rw [toNat, ofNat]
    congr
    ext x
    cases x

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

Goal state before:
pp: α : Type u
s t : WSeq α
h : s ~ʷ t
⊢ s.Productive ↔ t.Productive

Tactic:
simp only [productive_iff]; exact forall_congr' fun n => terminates_congr <| get?_congr h _

Goal state after:
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
⊢ (∃ᵐ (x : G) ∂μ, x ∈ s) → ∀ᵐ (x : G) ∂μ, x ∈ s

Tactic:
intro hμs

Goal state after:
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
⊢ ∀ᵐ (x : G) ∂μ, x ∈ s
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✝ : μ.IsMulRightInvariant
s : Set G
hsm : MeasurableSet s
hs : ∀ (g : Gᵐᵒᵖ), (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s
⊢ (∃ᵐ (x : G) ∂μ, x ∈ s) → ∀ᵐ (x : G) ∂μ, x ∈ s

Tactic:
intro hμs

Goal state after:
G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : MeasurableSpace G
inst✝³ : MeasurableMul₂ G
inst✝² : MeasurableInv G
μ : Measure G
inst✝¹ : SFinite μ
inst✝ : μ.IsMulRightInvariant
s : Set G
hsm : MeasurableSet s
hs : ∀ (g : Gᵐᵒᵖ), (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s
hμs : ∃ᵐ (x : G) ∂μ, x ∈ s
⊢ ∀ᵐ (x : G) ∂μ, x ∈ s
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✝ : μ.IsMulRightInvariant
s : Set G
hsm : MeasurableSet s
hs : ∀ (g : Gᵐᵒᵖ), (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s
hμs : ∃ᵐ (x : G) ∂μ, x ∈ s
a : G
has : a ∈ s
ha : ∀ᵐ (b : G) ∂μ, a * b ∈ s ↔ a ∈ s
⊢ ∀ᵐ (x : G) ∂μ, x ∈ s

Tactic:
simpa [has] using (quasiMeasurePreserving_mul_left μ a⁻¹).ae ha

Goal state after:
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 ≠ ∞
⊢ ν.InnerRegularCompactLTTop

Tactic:
← hg.map_eq

Goal state after:
α : 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 ≠ ∞
⊢ (Measure.map (⇑g) μ).InnerRegularCompactLTTop
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 ≠ ∞
⊢ (Measure.map (⇑g) μ).InnerRegularCompactLTTop

Tactic:
exact .map_of_continuous (map_continuous _)

Goal state after:
Module: Mathlib.Dynamics.FixedPoints.Prufer

Goal state before:
pp: G : Type u_1
inst✝ : CommGroup G
n : ℤ
s : Set G
hs : (fun x ↦ x ^ n) ⁻¹' s = s
g : G
j : ℕ
hg : g ^ n ^ j = 1
g' y : G
hy : y ∈ (fun x ↦ x ^ n)^[j] ⁻¹' s
hg' : (⇑(zpowGroupHom n))^[j] g' = 1
⊢ (⇑(zpowGroupHom n))^[j] (g' * y) ∈ s

Tactic:
iterate_map_mul,

Goal state after:
G : Type u_1
inst✝ : CommGroup G
n : ℤ
s : Set G
hs : (fun x ↦ x ^ n) ⁻¹' s = s
g : G
j : ℕ
hg : g ^ n ^ j = 1
g' y : G
hy : y ∈ (fun x ↦ x ^ n)^[j] ⁻¹' s
hg' : (⇑(zpowGroupHom n))^[j] g' = 1
⊢ (⇑(zpowGroupHom n))^[j] g' * (⇑(zpowGroupHom n))^[j] y ∈ s
Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber

Goal state before:
pp: f : CircleDeg1Lift
hf : Continuous ⇑f
m : ℤ
n : ℕ
hn : 0 < n
⊢ τ f = ↑m / ↑n ↔ ∃ x, (f ^ n) x = x + ↑m

Tactic:
rw [eq_div_iff, mul_comm, ← translationNumber_pow]

Goal state after:
f : CircleDeg1Lift
hf : Continuous ⇑f
m : ℤ
n : ℕ
hn : 0 < n
⊢ τ (f ^ n) = ↑m ↔ ∃ x, (f ^ n) x = x + ↑m

f : CircleDeg1Lift
hf : Continuous ⇑f
m : ℤ
n : ℕ
hn : 0 < n
⊢ ↑n ≠ 0
Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal

Goal state before:
pp: G : Type u_1
inst✝¹¹ : Group G
inst✝¹⁰ : TopologicalSpace G
inst✝⁹ : ContinuousInv G
X : Type u_2
inst✝⁸ : TopologicalSpace X
inst✝⁷ : R1Space X
inst✝⁶ : MeasurableSpace X
inst✝⁵ : BorelSpace X
inst✝⁴ : MulAction G X
inst✝³ : ContinuousSMul G X
g : G
hg : DenseRange fun x ↦ g ^ x
μ : Measure X
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : ErgodicSMul G X μ
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
s : Set X
hsm : MeasurableSet s
hs : (fun x ↦ g • x) ⁻¹' s = s
⊢ g⁻¹ • s =ᵐ[μ] s

Tactic:
← preimage_smul,

Goal state after:
G : Type u_1
inst✝¹¹ : Group G
inst✝¹⁰ : TopologicalSpace G
inst✝⁹ : ContinuousInv G
X : Type u_2
inst✝⁸ : TopologicalSpace X
inst✝⁷ : R1Space X
inst✝⁶ : MeasurableSpace X
inst✝⁵ : BorelSpace X
inst✝⁴ : MulAction G X
inst✝³ : ContinuousSMul G X
g : G
hg : DenseRange fun x ↦ g ^ x
μ : Measure X
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : ErgodicSMul G X μ
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
s : Set X
hsm : MeasurableSet s
hs : (fun x ↦ g • x) ⁻¹' s = s
⊢ (fun x ↦ g • x) ⁻¹' s =ᵐ[μ] s
Module: Mathlib.Dynamics.Ergodic.AddCircle

Goal state before:
pp: case inr
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : l.NeBot
u : ι → AddCircle T
μ : Measure (AddCircle T) := volume
hs : NullMeasurableSet s μ
hu₁ : ∀ (i : ι), u i +ᵥ s =ᵐ[μ] s
n : ι → ℕ := addOrderOf ∘ u
hu₂ : Tendsto n l atTop
hT₀ : 0 < T
hT₁ : ENNReal.ofReal T ≠ 0
h : μ s ≠ 0
d : AddCircle T
I : ι → Set (AddCircle T) := fun j ↦ closedBall d (T / (2 * ↑(n j)))
hd : Tendsto (fun j ↦ μ (s ∩ I j) / μ (I j)) l (𝓝 1)
j : ι
hj : 0 < n j
⊢ μ (s ∩ I j) / μ (I j) = μ s / ENNReal.ofReal T

Tactic:
have : addOrderOf (u j) = n j := rfl

Goal state after:
case inr
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst✝ : l.NeBot
u : ι → AddCircle T
μ : Measure (AddCircle T) := volume
hs : NullMeasurableSet s μ
hu₁ : ∀ (i : ι), u i +ᵥ s =ᵐ[μ] s
n : ι → ℕ := addOrderOf ∘ u
hu₂ : Tendsto n l atTop
hT₀ : 0 < T
hT₁ : ENNReal.ofReal T ≠ 0
h : μ s ≠ 0
d : AddCircle T
I : ι → Set (AddCircle T) := fun j ↦ closedBall d (T / (2 * ↑(n j)))
hd : Tendsto (fun j ↦ μ (s ∩ I j) / μ (I j)) l (𝓝 1)
j : ι
hj : 0 < n j
this : addOrderOf (u j) = n j
⊢ μ (s ∩ I j) / μ (I j) = μ s / ENNReal.ofReal T
Module: Mathlib.Dynamics.Ergodic.Extreme

Goal state before:
pp: 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
s : Set X
hsm : MeasurableSet s
hfs : f ⁻¹' s = s
hμs : μ s ≠ 0
⊢ s = f ⁻¹' s

Tactic:
exact hfs.symm

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

Goal state before:
pp: A : Type u_3
G : Type u_4
inst✝¹ : Finite A
inst✝ : Inhabited A
val✝ : Fintype A
cfg : G → A
dom : Finset G
cond : ∀ g ∉ dom, cfg g = default
g : G
⊢ (if h : g ∈ dom then cfg g else default) = cfg g

Tactic:
by_cases hg : g ∈ dom

Goal state after:
case pos
A : Type u_3
G : Type u_4
inst✝¹ : Finite A
inst✝ : Inhabited A
val✝ : Fintype A
cfg : G → A
dom : Finset G
cond : ∀ g ∉ dom, cfg g = default
g : G
hg : g ∈ dom
⊢ (if h : g ∈ dom then cfg g else default) = cfg g

case neg
A : Type u_3
G : Type u_4
inst✝¹ : Finite A
inst✝ : Inhabited A
val✝ : Fintype A
cfg : G → A
dom : Finset G
cond : ∀ g ∉ dom, cfg g = default
g : G
hg : g ∉ dom
⊢ (if h : g ∈ dom then cfg g else default) = cfg g
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: X : Type u_1
T : X → X
U : SetRel X X
F : Set X
n : ℕ
F_inv : MapsTo T F F
inst✝ : U.IsSymm
n_pos : n ≠ 0
cv_mono : Monotone fun m ↦ ↑(coverMincard T F (U ○ U) m)
h :
  (expGrowthSup fun n_1 ↦ ↑(coverMincard T F (U ○ U) (n * n_1))) / ↑n =
    expGrowthSup fun m ↦ ↑(coverMincard T F (U ○ U) m)
⊢ coverEntropyEntourage T F (U ○ U) ≤ (↑(coverMincard T F U n)).log / ↑n

Tactic:
rw [coverEntropyEntourage, ← h]

Goal state after:
X : Type u_1
T : X → X
U : SetRel X X
F : Set X
n : ℕ
F_inv : MapsTo T F F
inst✝ : U.IsSymm
n_pos : n ≠ 0
cv_mono : Monotone fun m ↦ ↑(coverMincard T F (U ○ U) m)
h :
  (expGrowthSup fun n_1 ↦ ↑(coverMincard T F (U ○ U) (n * n_1))) / ↑n =
    expGrowthSup fun m ↦ ↑(coverMincard T F (U ○ U) m)
⊢ (expGrowthSup fun n_1 ↦ ↑(coverMincard T F (U ○ U) (n * n_1))) / ↑n ≤ (↑(coverMincard T F U n)).log / ↑n
Module: Mathlib.Dynamics.TopologicalEntropy.CoverEntropy

Goal state before:
pp: X : Type u_1
inst✝ : UniformSpace X
ι : Sort u_2
p : ι → Prop
s : ι → SetRel X X
h : (𝓤 X).HasBasis p s
T : X → X
F : Set X
U : Set (X × X)
U_uni : U ∈ 𝓤 X
i : ι
h_i : p i
si_U : s i ⊆ U
⊢ coverEntropyEntourage T F U ≤ ⨆ i, ⨆ (_ : p i), coverEntropyEntourage T F (s i)

Tactic:
exact (coverEntropyEntourage_antitone T F si_U).trans
    (le_iSup₂ (f := fun (i : ι) (_ : p i) ↦ coverEntropyEntourage T F (s i)) i h_i)

Goal state after:
Module: Mathlib.Dynamics.Transitive

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : Monoid M
inst✝¹ : MulAction M α
inst✝ : IsMinimal M α
U✝ : Set α
h : IsOpen U✝
hn : U✝.Nonempty
⊢ Dense (⋃ m, (fun x ↦ m • x) ⁻¹' U✝)

Tactic:
simp only [h.iUnion_preimage_smul M hn, dense_univ]

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ ν : Measure α
mβ : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
⊢ Measurable fun x ↦ (map f μ).rnDeriv (map f ν) (f x)

Tactic:
exact (Measure.measurable_rnDeriv _ _).comp hf.measurable

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 μ = map f (μ.singularPart ν) + (map f ν).withDensity ((map f μ).rnDeriv (map f ν))

Tactic:
conv_lhs => rw [μ.haveLebesgueDecomposition_add ν]

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 ν + ν.withDensity (μ.rnDeriv ν)) =
    map f (μ.singularPart ν) + (map f ν).withDensity ((map f μ).rnDeriv (map f ν))
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ν₂ : ν₂ ≪ μ
⊢ ν₁ ∗ₘ ν₂ = ν₁ ∗ₘ μ.withDensity (ν₂.rnDeriv μ)

Tactic:
withDensity_rnDeriv_eq _ _ hν₂

Goal state after:
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ν₂ : ν₂ ≪ μ
⊢ ν₁ ∗ₘ ν₂ = ν₁ ∗ₘ ν₂
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
β : Type v'
inst✝¹ : L[[α]].Structure M
inst✝ : (L.lhomWithConstants α).IsExpansionOn M
t : L[[α]].Term β
v : β → M
⊢ realize (Sum.elim (fun a ↦ ↑(L.con a)) v) t.constantsToVars = realize v t

Tactic:
by
  induction t with
  | var => simp
  | @func n f ts ih =>
    cases n
    · cases f
      · simp only [realize, ih, constantsOn, constantsOnFunc, constantsToVars]
        -- Porting note: below lemma does not work with simp for some reason
        rw [withConstants_funMap_sumInl]
      · simp only [realize, constantsToVars, Sum.elim_inl, funMap_eq_coe_constants]
        rfl
    · obtain - | f := f
      · simp only [realize, ih, constantsOn, constantsOnFunc, constantsToVars]
        -- Porting note: below lemma does not work with simp for some reason
        rw [withConstants_funMap_sumInl]
      · exact isEmptyElim f

Goal state after:
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case cons
L : Language
α : Type u'
l✝ : List (L.Term α)
n : ℕ
f : L.Functions n
ts : Fin n → L.Term α
ih : ∀ (a : Fin n) (l : List (α ⊕ (i : ℕ) × L.Functions i)), listDecode ((ts a).listEncode ++ l) = ts a :: listDecode l
l : List (α ⊕ (i : ℕ) × L.Functions i)
i : Fin n
l' : List (Fin n)
l'ih : listDecode (flatMap (fun i ↦ (ts i).listEncode) l' ++ l) = List.map ts l' ++ listDecode l
⊢ listDecode (flatMap (fun i ↦ (ts i).listEncode) (i :: l') ++ l) = List.map ts (i :: l') ++ listDecode l

Tactic:
| cons i l' l'ih =>

Goal state after:
Module: Mathlib.ModelTheory.ElementaryMaps

Goal state before:
pp: case refine_5.refine_1
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
h : ∀ (a : N), φ.Realize (⇑f ∘ default) (Fin.snoc (⇑f ∘ xs) a)
a : M
⊢ φ.Realize default (Fin.snoc xs a)

Tactic:
rw [← ih, Fin.comp_snoc]

Goal state after:
case refine_5.refine_1
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
h : ∀ (a : N), φ.Realize (⇑f ∘ default) (Fin.snoc (⇑f ∘ xs) a)
a : M
⊢ φ.Realize (⇑f ∘ default) (Fin.snoc (⇑f ∘ xs) (f a))
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: case rel.refine_2
L : Language
α : Type u'
l✝ : List ((n : ℕ) × L.BoundedFormula α n)
n φ_n φ_l : ℕ
φ_R : L.Relations φ_l
ts : Fin φ_l → L.Term (α ⊕ Fin φ_n)
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
h :
  ∀ (i : Fin φ_l),
    (List.map Sum.getLeft? (List.map (fun i ↦ Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l))[i]?.join =
      some ⟨φ_n, ts i⟩
⊢ listDecode (drop φ_l (List.map (fun i ↦ Sum.inl ⟨φ_n, ts i⟩) (finRange φ_l)) ++ l) = listDecode l

Tactic:
drop_eq_nil_of_le,

Goal state after:
case rel.refine_2
L : Language
α : Type u'
l✝ : List ((n : ℕ) × L.BoundedFormula α n)
n φ_n φ_l : ℕ
φ_R : L.Relations φ_l
ts : Fin φ_l → L.Term (α ⊕ Fin φ_n)
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
h :
  ∀ (i : Fin φ_l),
    (List.map Sum.getLeft? (List.map (fun i ↦ Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l))[i]?.join =
      some ⟨φ_n, ts i⟩
⊢ listDecode ([] ++ l) = listDecode l

case rel.refine_2
L : Language
α : Type u'
l✝ : List ((n : ℕ) × L.BoundedFormula α n)
n φ_n φ_l : ℕ
φ_R : L.Relations φ_l
ts : Fin φ_l → L.Term (α ⊕ Fin φ_n)
l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
h :
  ∀ (i : Fin φ_l),
    (List.map Sum.getLeft? (List.map (fun i ↦ Sum.inl ⟨⟨φ_n, rel φ_R ts⟩.fst, ts i⟩) (finRange φ_l) ++ l))[i]?.join =
      some ⟨φ_n, ts i⟩
⊢ (List.map (fun i ↦ Sum.inl ⟨φ_n, ts i⟩) (finRange φ_l)).length ≤ φ_l
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
f g : Set (α → M)
φ : L[[↑A]].Formula α
hφ : f = ofPred φ.Realize
θ : L[[↑A]].Formula α
hθ : g = ofPred θ.Realize
x✝ : α → M
⊢ x✝ ∈ ofPred φ.Realize ∪ ofPred θ.Realize ↔ x✝ ∈ ofPred (φ ⊔ θ).Realize

Tactic:
mem_ofPred_eq,

Goal state after:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
f g : Set (α → M)
φ : L[[↑A]].Formula α
hφ : f = ofPred φ.Realize
θ : L[[↑A]].Formula α
hθ : g = ofPred θ.Realize
x✝ : α → M
⊢ x✝ ∈ ofPred φ.Realize ∪ ofPred θ.Realize ↔ (φ ⊔ θ).Realize x✝
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
f g : Set (α → M)
φ : L[[↑A]].Formula α
hφ : f = ofPred φ.Realize
θ : L[[↑A]].Formula α
hθ : g = ofPred θ.Realize
x✝ : α → M
⊢ x✝ ∈ ofPred φ.Realize ∨ x✝ ∈ ofPred θ.Realize ↔ φ.Realize x✝ ∨ θ.Realize x✝

Tactic:
mem_ofPred_eq,

Goal state after:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
f g : Set (α → M)
φ : L[[↑A]].Formula α
hφ : f = ofPred φ.Realize
θ : L[[↑A]].Formula α
hθ : g = ofPred θ.Realize
x✝ : α → M
⊢ φ.Realize x✝ ∨ x✝ ∈ ofPred θ.Realize ↔ φ.Realize x✝ ∨ θ.Realize x✝
Module: Mathlib.ModelTheory.Definability

Goal state before:
pp: M : Type w
L : Language
inst✝ : L.Structure M
α : Type u₁
f : (α → M) → M
⊢ ∅.TermDefinable L f ↔ ∃ φ, f = fun v ↦ Term.realize v φ

Tactic:
rw [TermDefinable, Equiv.exists_congr_left (LEquiv.addEmptyConstants L (∅ : Set M)).onTerm]

Goal state after:
M : Type w
L : Language
inst✝ : L.Structure M
α : Type u₁
f : (α → M) → M
⊢ (∃ φ, f = fun v ↦ Term.realize v φ) ↔ ∃ b, f = fun v ↦ Term.realize v ((LEquiv.addEmptyConstants L ↑∅).onTerm.symm b)
Module: Mathlib.ModelTheory.Algebra.Field.IsAlgClosed

Goal state before:
pp: p✝ : ℕ
K : Type u_2
inst✝¹ : Field K
inst✝ : CompatibleRing K
h✝ : K ⊨ Theory.ACF p✝
p : K[X]
hpm : p.Monic
hpi : Irreducible p
h : ∀ (φ : Language.ring.Sentence), ∀ x ∈ {n | 0 < n}, genericMonicPolyHasRoot x = φ → K ⊨ φ
⊢ ∃ x, eval x p = 0

Tactic:
have := h _ p.natDegree (natDegree_pos_iff_degree_pos.2
    (degree_pos_of_irreducible hpi)) rfl

Goal state after:
p✝ : ℕ
K : Type u_2
inst✝¹ : Field K
inst✝ : CompatibleRing K
h✝ : K ⊨ Theory.ACF p✝
p : K[X]
hpm : p.Monic
hpi : Irreducible p
h : ∀ (φ : Language.ring.Sentence), ∀ x ∈ {n | 0 < n}, genericMonicPolyHasRoot x = φ → K ⊨ φ
this : K ⊨ genericMonicPolyHasRoot p.natDegree
⊢ ∃ x, eval x p = 0