mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Vector.MapLemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
σ₁ : Type u_6
σ₂ : Type u_7
n : ℕ
xs : Vector α n
f₁ : α → β → σ₁ → σ₁ × γ
f₂ : α → β → σ₂ → σ₂ × γ
R : σ₁ → σ₂ → Prop
hR : ∀ {s : σ₁} {q : σ₂} (a : α) (b : β), R s q → R (f₁ a b s).1 (f₂ a b q).1 ∧ (f₁ a b s).2 = (f₂ a b q).2
s₁ : σ₁
s₂ : σ₂
h₀ : R s₁ s₂
⊢ R (mapAccumr₂ f₁ nil nil s₁).1 (mapAccumr₂ f₂ nil nil s₂).1 ∧
    (mapAccumr₂ f₁ nil nil s₁).2 = (mapAccumr₂ f₂ nil nil s₂).2

Tactic:
exact ⟨h₀, rfl⟩

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 t : Set α
h : s =ᵐ[μ] t
⊢ aestabilizer G μ s = aestabilizer G μ t

Tactic:
ext g
  rw [mem_aestabilizer, mem_aestabilizer, h.congr_right, ((smul_set_ae_eq g).2 h).congr_left]

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

Goal state before:
pp: f : CircleDeg1Lift
x : ℝ
⊢ f (1 + x) = 1 + f x

Tactic:
rw [add_comm, map_add_one, add_comm 1]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (f₁ g) = τ (f₂ g)
x : ℝ
g : G
this : τ (f₂ g⁻¹) = -τ (f₂ g)
⊢ (f₂ g⁻¹) (x + τ (f₂ g) + 1) = (f₂ g⁻¹) (x + τ (f₂ g)) + 1

Tactic:
map_add_one

Goal state after:
G : Type u_1
inst✝ : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ (f₁ g) = τ (f₂ g)
x : ℝ
g : G
this : τ (f₂ g⁻¹) = -τ (f₂ g)
⊢ (f₂ g⁻¹) (x + τ (f₂ g)) + 1 = (f₂ g⁻¹) (x + τ (f₂ g)) + 1
Module: Mathlib.Dynamics.Ergodic.Conservative

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
h0 : μ s ≠ 0
t : ℕ → Set α := fun n ↦ s ∩ f^[n] ⁻¹' s
H : ¬∃ᶠ (m : ℕ) in atTop, μ (s ∩ f^[m] ⁻¹' s) ≠ 0
N : ℕ
hN : μ (t N) ≠ 0
hmax : ∀ n > N, μ (t n) = 0
htm : ∀ {n : ℕ}, NullMeasurableSet (t n) μ
T : Set α := t N \ ⋃ n, ⋃ (_ : n > N), t n
hT : T = t N \ ⋃ n, ⋃ (_ : n > N), t n
hμT : μ T ≠ 0
hTm : NullMeasurableSet T μ
x : α
hxt : x ∈ T
m : ℕ
hm₀ : m ≠ 0
hmt : f^[m] x ∈ T
⊢ N + m > N

pp: case refine_2
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
h0 : μ s ≠ 0
t : ℕ → Set α := fun n ↦ s ∩ f^[n] ⁻¹' s
H : ¬∃ᶠ (m : ℕ) in atTop, μ (s ∩ f^[m] ⁻¹' s) ≠ 0
N : ℕ
hN : μ (t N) ≠ 0
hmax : ∀ n > N, μ (t n) = 0
htm : ∀ {n : ℕ}, NullMeasurableSet (t n) μ
T : Set α := t N \ ⋃ n, ⋃ (_ : n > N), t n
hT : T = t N \ ⋃ n, ⋃ (_ : n > N), t n
hμT : μ T ≠ 0
hTm : NullMeasurableSet T μ
x : α
hxt : x ∈ T
m : ℕ
hm₀ : m ≠ 0
hmt : f^[m] x ∈ T
⊢ x ∈ f^[N + m] ⁻¹' s

Tactic:
· simpa [pos_iff_ne_zero]

Goal state after:
case refine_2
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
h0 : μ s ≠ 0
t : ℕ → Set α := fun n ↦ s ∩ f^[n] ⁻¹' s
H : ¬∃ᶠ (m : ℕ) in atTop, μ (s ∩ f^[m] ⁻¹' s) ≠ 0
N : ℕ
hN : μ (t N) ≠ 0
hmax : ∀ n > N, μ (t n) = 0
htm : ∀ {n : ℕ}, NullMeasurableSet (t n) μ
T : Set α := t N \ ⋃ n, ⋃ (_ : n > N), t n
hT : T = t N \ ⋃ n, ⋃ (_ : n > N), t n
hμT : μ T ≠ 0
hTm : NullMeasurableSet T μ
x : α
hxt : x ∈ T
m : ℕ
hm₀ : m ≠ 0
hmt : f^[m] x ∈ T
⊢ x ∈ f^[N + m] ⁻¹' s
Module: Mathlib.Dynamics.Ergodic.AddCircle

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

Tactic:
replace h : n - 1 ≠ 0 := by
    rw [← abs_one] at h; rw [sub_ne_zero]; exact ne_of_apply_ne _ (ne_of_gt h)

Goal state after:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
f : AddCircle T → AddCircle T := fun y ↦ n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving (⇑e) volume volume
h : n - 1 ≠ 0
⊢ ⇑e ∘ f ∘ ⇑e.symm = fun y ↦ n • y
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)
⊢ μ.rnDeriv (ν.withDensity f) =ᵐ[ν.withDensity f] fun x ↦ (f x)⁻¹ * μ.rnDeriv ν x

Tactic:
refine (Measure.eq_rnDeriv₀ (ν := ν.withDensity f) ?_ Measure.MutuallySingular.zero_left ?_).symm

Goal state after:
case refine_1
α : 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)
⊢ AEMeasurable (fun x ↦ (f x)⁻¹ * μ.rnDeriv ν x) (ν.withDensity f)

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)
⊢ μ = 0 + (ν.withDensity f).withDensity fun x ↦ (f x)⁻¹ * μ.rnDeriv ν x
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
hx : x ∈ mulForbidden F
p : Pattern A G
hp : p ∈ F
⊢ ∀ (g : G), ¬p.mulOccursInAt (mulShift h x) g

Tactic:
g

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
p : Pattern A G
hp : p ∈ F
g : G
⊢ ¬p.mulOccursInAt (mulShift h x) g
Module: Mathlib.Dynamics.OmegaLimit

Goal state before:
pp: case mp
τ : Type u_1
α : Type u_2
β : Type u_3
inst✝ : TopologicalSpace β
f : Filter τ
ϕ : τ → α → β
s : Set α
y : β
h : ∀ i ∈ f, ∀ t ∈ 𝓝 y, (t ∩ image2 ϕ i s).Nonempty
n✝ : Set β
hn : n✝ ∈ 𝓝 y
U✝ : Set τ
hu : U✝ ∈ f
w✝¹ : τ
ht : w✝¹ ∈ U✝
w✝ : α
hx : w✝ ∈ s
left✝ : ϕ w✝¹ w✝ ∈ n✝
⊢ ∃ x ∈ U✝, (s ∩ ϕ x ⁻¹' n✝).Nonempty

Tactic:
exact ⟨_, ht, _, hx, by rwa [mem_preimage]⟩

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_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᵐ[ν + ν']
    (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')
h₂ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᵐ[ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
h₃ : (μ.singularPart ν').rnDeriv (ν + ν') =ᵐ[ν] (μ.singularPart ν').rnDeriv ν
h₄ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᵐ[ν] 0
h₅ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᵐ[ν] 0
x : α
hx₃ : (μ.singularPart ν').rnDeriv (ν + ν') x = (μ.singularPart ν').rnDeriv ν x
hx₄ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') x = 0 x
hx₅ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν x = 0 x
⊢ ((μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')) x =
    ((μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν) x

Tactic:
Pi.add_apply,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᵐ[ν + ν']
    (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')
h₂ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᵐ[ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
h₃ : (μ.singularPart ν').rnDeriv (ν + ν') =ᵐ[ν] (μ.singularPart ν').rnDeriv ν
h₄ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᵐ[ν] 0
h₅ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᵐ[ν] 0
x : α
hx₃ : (μ.singularPart ν').rnDeriv (ν + ν') x = (μ.singularPart ν').rnDeriv ν x
hx₄ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') x = 0 x
hx₅ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν x = 0 x
⊢ (μ.singularPart ν').rnDeriv (ν + ν') x + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') x =
    ((μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν) x
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᵐ[ν + ν']
    (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')
h₂ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᵐ[ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
h₃ : (μ.singularPart ν').rnDeriv (ν + ν') =ᵐ[ν] (μ.singularPart ν').rnDeriv ν
h₄ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᵐ[ν] 0
h₅ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᵐ[ν] 0
x : α
hx₃ : (μ.singularPart ν').rnDeriv (ν + ν') x = (μ.singularPart ν').rnDeriv ν x
hx₄ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') x = 0 x
hx₅ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν x = 0 x
⊢ (μ.singularPart ν').rnDeriv (ν + ν') x + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') x =
    ((μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν) x

Tactic:
Pi.add_apply,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᵐ[ν + ν']
    (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')
h₂ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᵐ[ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
h₃ : (μ.singularPart ν').rnDeriv (ν + ν') =ᵐ[ν] (μ.singularPart ν').rnDeriv ν
h₄ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᵐ[ν] 0
h₅ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᵐ[ν] 0
x : α
hx₃ : (μ.singularPart ν').rnDeriv (ν + ν') x = (μ.singularPart ν').rnDeriv ν x
hx₄ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') x = 0 x
hx₅ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν x = 0 x
⊢ (μ.singularPart ν').rnDeriv (ν + ν') x + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') x =
    (μ.singularPart ν').rnDeriv ν x + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν x
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

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

Tactic:
filter_upwards [this] with x hx h_absurd using absurd hx h_absurd

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

Goal state before:
pp: X : Type u_1
U : SetRel X X
T : X → X
F : Set X
inst✝¹ : U.IsRefl
inst✝ : U.IsSymm
n : ℕ
h✝ : netMaxcard T F U n < ⊤
s : Finset X
s_net : IsDynNetIn T F U n ↑s
s_card : ↑s.card = netMaxcard T F U n
h : ¬F ⊆ ⋃ y ∈ ↑s, ball y (dynEntourage T (U ○ U) n)
x : X
x_F : x ∈ F
x_uncov : ∀ x_1 ∈ s, x ∉ ball x_1 (dynEntourage T (U ○ U) n)
⊢ IsDynNetIn T F U n (insert x ↑s)

Tactic:
refine ⟨insert_subset x_F s_net.1, pairwiseDisjoint_insert.2 ⟨s_net.2, ?_⟩⟩

Goal state after:
X : Type u_1
U : SetRel X X
T : X → X
F : Set X
inst✝¹ : U.IsRefl
inst✝ : U.IsSymm
n : ℕ
h✝ : netMaxcard T F U n < ⊤
s : Finset X
s_net : IsDynNetIn T F U n ↑s
s_card : ↑s.card = netMaxcard T F U n
h : ¬F ⊆ ⋃ y ∈ ↑s, ball y (dynEntourage T (U ○ U) n)
x : X
x_F : x ∈ F
x_uncov : ∀ x_1 ∈ s, x ∉ ball x_1 (dynEntourage T (U ○ U) n)
⊢ ∀ j ∈ ↑s, x ≠ j → Disjoint (ball x (dynEntourage T U n)) (ball j (dynEntourage T U n))
Module: Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Goal state before:
pp: X : Type u_1
T : X → X
F : Set X
h : F.Nonempty
⊢ netEntropyInfEntourage T F univ = 0

Tactic:
rw [← expGrowthInf_const one_ne_zero one_ne_top, netEntropyInfEntourage]
  simp only [netMaxcard_univ T h, ENat.toENNReal_one]

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_meas : Measurable (μ.rnDeriv ν)
h_sing : μ.singularPart ν ⟂ₘ ν
hμν : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
x : α
hx1 :
  (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x =
    ((μ.singularPart ν).rnDeriv κ + (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ) x
hx2 : (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x = μ.rnDeriv ν x * ν.rnDeriv κ x
hx3 : (μ.singularPart ν).rnDeriv κ x = 0 x
⊢ (μ.rnDeriv ν * ν.rnDeriv κ) x = ((μ.singularPart ν).rnDeriv κ + (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ) x

Tactic:
Pi.add_apply,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν κ : Measure α
inst✝² : SigmaFinite μ
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite κ
hνκ : ν ≪ κ
h_meas : Measurable (μ.rnDeriv ν)
h_sing : μ.singularPart ν ⟂ₘ ν
hμν : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
x : α
hx1 :
  (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x =
    ((μ.singularPart ν).rnDeriv κ + (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ) x
hx2 : (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x = μ.rnDeriv ν x * ν.rnDeriv κ x
hx3 : (μ.singularPart ν).rnDeriv κ x = 0 x
⊢ (μ.rnDeriv ν * ν.rnDeriv κ) x = (μ.singularPart ν).rnDeriv κ x + (ν.withDensity (μ.rnDeriv ν)).rnDeriv κ x
Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hν_ac : μ ≪ ν + μ
a : α
h1 : (ν + μ).rnDeriv μ a = (ν.rnDeriv μ + μ.rnDeriv μ) a
h2 : μ.rnDeriv μ a = 1
h3 : (μ.rnDeriv (ν + μ) a)⁻¹ = (ν.rnDeriv μ + μ.rnDeriv μ) a
⊢ μ.rnDeriv (ν + μ) a = (ν.rnDeriv μ a + 1)⁻¹

Tactic:
Pi.add_apply,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hν_ac : μ ≪ ν + μ
a : α
h1 : (ν + μ).rnDeriv μ a = (ν.rnDeriv μ + μ.rnDeriv μ) a
h2 : μ.rnDeriv μ a = 1
h3 : (μ.rnDeriv (ν + μ) a)⁻¹ = ν.rnDeriv μ a + μ.rnDeriv μ a
⊢ μ.rnDeriv (ν + μ) a = (ν.rnDeriv μ a + 1)⁻¹
Module: Mathlib.Dynamics.TopologicalEntropy.Subset

Goal state before:
pp: X : Type u_1
T : X → X
F G : Set X
U : SetRel X X
n : ℕ
⊢ ↑(coverMincard T (F ∪ G) U n) ≤ ((fun n ↦ ↑(coverMincard T F U n)) + fun n ↦ ↑(coverMincard T G U n)) n

Tactic:
Pi.add_apply,

Goal state after:
X : Type u_1
T : X → X
F G : Set X
U : SetRel X X
n : ℕ
⊢ ↑(coverMincard T (F ∪ G) U n) ≤ ↑(coverMincard T F U n) + ↑(coverMincard T G U n)
Module: Mathlib.FieldTheory.AbelRuffini

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

Tactic:
C_0,

Goal state after:
case pos
F : Type u_1
inst✝ : Field F
n : ℕ
a : F
h : (map (RingHom.id F) (X ^ n - 1)).Splits
ha : a = 0
⊢ Group.IsSolvable (X ^ n - 0).Gal
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝² : L.Structure M
inst✝¹ : L.Structure N
P : Type u_1
inst✝ : L.Structure P
h : N ↪[L] P
f : M ↪[L] N
⊢ ∀ ⦃a₂ : M ↪[L] N⦄, h.comp f = h.comp a₂ → f = a₂

Tactic:
g

Goal state after:
L : Language
M : Type w
N : Type w'
inst✝² : L.Structure M
inst✝¹ : L.Structure N
P : Type u_1
inst✝ : L.Structure P
h : N ↪[L] P
f g : M ↪[L] N
⊢ h.comp f = h.comp g → f = g
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝² : L.Structure M
inst✝¹ : L.Structure N
P : Type u_1
inst✝ : L.Structure P
h : N ↪[L] P
f : M →[L] N
⊢ ∀ ⦃a₂ : M →[L] N⦄, h.toHom.comp f = h.toHom.comp a₂ → f = a₂

Tactic:
g

Goal state after:
L : Language
M : Type w
N : Type w'
inst✝² : L.Structure M
inst✝¹ : L.Structure N
P : Type u_1
inst✝ : L.Structure P
h : N ↪[L] P
f g : M →[L] N
⊢ h.toHom.comp f = h.toHom.comp g → f = g
Module: Mathlib.ModelTheory.LanguageMap

Goal state before:
pp: case refine_1
L : Language
L' : Language
M : Type w
inst✝² : L.Structure M
α : Type u_1
inst✝¹ : (constantsOn α).Structure M
A B : Set M
h : A ⊆ B
N : Type w'
inst✝ : L.Structure N
f : M ↪[L] N
n : ℕ
⊢ ∀ (f_1 : L[[↑A]].Functions n) (x : Fin n → M), f.toFun (funMap f_1 x) = funMap f_1 (f.toFun ∘ x)

Tactic:
g

Goal state after:
case refine_1
L : Language
L' : Language
M : Type w
inst✝² : L.Structure M
α : Type u_1
inst✝¹ : (constantsOn α).Structure M
A B : Set M
h : A ⊆ B
N : Type w'
inst✝ : L.Structure N
f : M ↪[L] N
n : ℕ
g : L[[↑A]].Functions n
⊢ ∀ (x : Fin n → M), f.toFun (funMap g x) = funMap g (f.toFun ∘ x)
Module: Mathlib.FieldTheory.AbelRuffini

Goal state before:
pp: case pos
F : Type u_1
inst✝ : Field F
n : ℕ
x : F
hx : x = 0
⊢ Group.IsSolvable (X ^ n - C 0).Gal

Tactic:
C_0,

Goal state after:
case pos
F : Type u_1
inst✝ : Field F
n : ℕ
x : F
hx : x = 0
⊢ Group.IsSolvable (X ^ n - 0).Gal
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝² : L.Structure M
inst✝¹ : L.Structure N
P : Type u_1
inst✝ : L.Structure P
h : N ≃[L] P
f : M ≃[L] N
⊢ ∀ ⦃a₂ : M ≃[L] N⦄, h.comp f = h.comp a₂ → f = a₂

Tactic:
g

Goal state after:
L : Language
M : Type w
N : Type w'
inst✝² : L.Structure M
inst✝¹ : L.Structure N
P : Type u_1
inst✝ : L.Structure P
h : N ≃[L] P
f g : M ≃[L] N
⊢ h.comp f = h.comp g → f = g
Module: Mathlib.ModelTheory.Basic

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝² : L.Structure M
inst✝¹ : L.Structure N
P : Type u_1
inst✝ : L.Structure P
h : M ≃[L] N
f : N ≃[L] P
⊢ ∀ ⦃a₂ : N ≃[L] P⦄, (fun f ↦ f.comp h) f = (fun f ↦ f.comp h) a₂ → f = a₂

Tactic:
g

Goal state after:
L : Language
M : Type w
N : Type w'
inst✝² : L.Structure M
inst✝¹ : L.Structure N
P : Type u_1
inst✝ : L.Structure P
h : M ≃[L] N
f g : N ≃[L] P
⊢ (fun f ↦ f.comp h) f = (fun f ↦ f.comp h) g → f = g
Module: Mathlib.ModelTheory.Syntax

Goal state before:
pp: L : Language
L' : Language
M : Type w
α : Type u'
β : Type v'
γ : Type u_1
t : L[[γ]].Term α
⊢ t.constantsToVars.varsToConstants = t

Tactic:
induction t with
    | var => rfl
    | @func n f _ ih =>
      cases n
      · cases f
        · simp [constantsToVars, varsToConstants, ih]
        · simp [constantsToVars, varsToConstants, Constants.term, eq_iff_true_of_subsingleton]
      · obtain - | f := f
        · simp [constantsToVars, varsToConstants, ih]
        · exact isEmptyElim f

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
x : E
hx : x ∈ solvableByRad F E
q : F[X]
q_irred : Irreducible q
q_aeval : (aeval x) q = 0
⊢ Group.IsSolvable (q * C q.leadingCoeff⁻¹).Gal

Tactic:
minpoly.eq_of_irreducible q_irred q_aeval

Goal state after:
F : Type u_1
E : Type u_2
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
x : E
hx : x ∈ solvableByRad F E
q : F[X]
q_irred : Irreducible q
q_aeval : (aeval x) q = 0
⊢ Group.IsSolvable (minpoly F x).Gal
Module: Mathlib.ModelTheory.Ultraproducts

Goal state before:
pp: case equal
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → L.Structure (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
n : ℕ
x : β → (a : α) → M a
n✝ : ℕ
t₁✝ t₂✝ : L.Term (β ⊕ Fin n✝)
v : Fin n✝ → (a : α) → M a
h2 : ∀ (a : α), (Sum.elim (fun i ↦ x i a) fun i ↦ v i a) = fun i ↦ Sum.elim x v i a
⊢ ((Quotient.mk' fun a ↦ Term.realize (fun i ↦ Sum.elim x v i a) t₁✝) =
      Quotient.mk' fun a ↦ Term.realize (fun i ↦ Sum.elim x v i a) t₂✝) ↔
    ∀ᶠ (a : α) in ↑u, Term.realize (fun i ↦ Sum.elim x v i a) t₁✝ = Term.realize (fun i ↦ Sum.elim x v i a) t₂✝

Tactic:
exact Quotient.eq''

Goal state after:
Module: Mathlib.ModelTheory.Encoding

Goal state before:
pp: L : Language
α : Type u'
h1 : Countable α
h2 : Countable ((l : ℕ) × L.Functions l)
⊢ #α ≤ ℵ₀ ∧ #((i : ℕ) × L.Functions i) ≤ ℵ₀

Tactic:
exact ⟨Cardinal.mk_le_aleph0, Cardinal.mk_le_aleph0⟩

Goal state after:
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
inst✝ : IsEmpty L.Constants
x : M
⊢ ∀ {n : ℕ} (f : L.Functions n), ClosedUnder f ∅

Tactic:
intro n f

Goal state after:
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
⊢ ClosedUnder f ∅
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
⊢ (∃ i,
      Realize φ (Sum.elim v i) default ∧
        ∀ (i_1 : γ → M),
          Realize φ (fun x ↦ Sum.elim (Sum.elim v i) i_1 (Sum.elim (fun x ↦ Sum.inl (Sum.inl x)) Sum.inr x)) default →
            ∀ (b : γ), i_1 b = i b) ↔
    ∃ x, Realize φ (Sum.elim v x) default ∧ ∀ (y : γ → M), Realize φ (Sum.elim v y) default → ∀ (x_1 : γ), y x_1 = x x_1

Tactic:
refine exists_congr (fun i => and_congr_right' (forall_congr' (fun y => ?_)))

Goal state after:
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
γ : Type u_3
inst✝ : Finite γ
φ : L.Formula (α ⊕ γ)
v : α → M
i y : γ → M
⊢ (Realize φ (fun x ↦ Sum.elim (Sum.elim v i) y (Sum.elim (fun x ↦ Sum.inl (Sum.inl x)) Sum.inr x)) default →
      ∀ (b : γ), y b = i b) ↔
    Realize φ (Sum.elim v y) default → ∀ (x : γ), y x = i x
Module: Mathlib.ModelTheory.Skolem

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
κ : Cardinal.{w'}
h1 : ℵ₀ ≤ κ
h2 : lift.{w', w} #↑s ≤ lift.{w, w'} κ
h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ
h4 : lift.{w, w'} κ ≤ lift.{w', w} #M
s' : Set (ULift.{w', w} M)
hs' : #↑s' = lift.{w, w'} κ
⊢ ∃ S, s ⊆ ↑S ∧ lift.{w', w} #↥S = lift.{w, w'} κ

Tactic:
rw [← aleph0_le_lift.{_, w}] at h1

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
s : Set M
κ : Cardinal.{w'}
h1 : ℵ₀ ≤ lift.{w, w'} κ
h2 : lift.{w', w} #↑s ≤ lift.{w, w'} κ
h3 : lift.{w', max u v} L.card ≤ lift.{max u v, w'} κ
h4 : lift.{w, w'} κ ≤ lift.{w', w} #M
s' : Set (ULift.{w', w} M)
hs' : #↑s' = lift.{w, w'} κ
⊢ ∃ S, s ⊆ ↑S ∧ lift.{w', w} #↥S = lift.{w, w'} κ
Module: Mathlib.ModelTheory.Semantics

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
n : ℕ
⊢ M ⊨ Sentence.cardGe L n ↔ lift.{w, 0} #(Fin n) ≤ #M

Tactic:
← lift_le.{0},

Goal state after:
L : Language
M : Type w
inst✝ : L.Structure M
n : ℕ
⊢ M ⊨ Sentence.cardGe L n ↔ lift.{0, w} (lift.{w, 0} #(Fin n)) ≤ lift.{0, w} #M
Module: Mathlib.ModelTheory.Satisfiability

Goal state before:
pp: L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst✝² : Nonempty M
inst✝¹ : L.Structure M
inst✝ : M ⊨ T
h : Nonempty (↑s ↪ M)
this✝ : Inhabited M
this : (constantsOn α).Structure M := constantsOn.structure (Function.extend Subtype.val (⇑h.some) default)
⊢ Set.InjOn (fun i ↦ ↑(L.con i)) s

Tactic:
intro a as b bs ab

Goal state after:
L : Language
α : Type w
T : L.Theory
s : Set α
M : Type w'
inst✝² : Nonempty M
inst✝¹ : L.Structure M
inst✝ : M ⊨ T
h : Nonempty (↑s ↪ M)
this✝ : Inhabited M
this : (constantsOn α).Structure M := constantsOn.structure (Function.extend Subtype.val (⇑h.some) default)
a : α
as : a ∈ s
b : α
bs : b ∈ s
ab : (fun i ↦ ↑(L.con i)) a = (fun i ↦ ↑(L.con i)) b
⊢ a = b