mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.VectorMeasure.AddContent

Goal state before:
pp: α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetRing C
hCmeas : ∀ s ∈ C, MeasurableSet s
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : ∀ (t : Set α) (ε : ℝ≥0∞), MeasurableSet t → 0 < ε → ∃ s ∈ C, μ (s ∆ t) < ε
C' : Set (MeasuredSets μ) := {s | ∃ c ∈ C, ↑s = c}
C'C : ∀ s ∈ C', ↑s ∈ C
C'_dense : Dense C'
m₀ : ↑C' → E := fun x ↦ m ↑↑x
s t : ↑C'
this : edist s t = edist ↑s ↑t
Is : ↑↑s ∩ ↑↑t ∪ ↑↑s \ ↑↑t = ↑↑s
It : ↑↑t ∩ ↑↑s ∪ ↑↑t \ ↑↑s = ↑↑t
⊢ ‖m (↑↑t ∩ ↑↑s) + m (↑↑s \ ↑↑t) - (m (↑↑t ∩ ↑↑s) + m (↑↑t \ ↑↑s))‖ₑ ≤ μ (↑↑s \ ↑↑t) + μ (↑↑t \ ↑↑s)

Tactic:
simp only [add_sub_add_left_eq_sub, ge_iff_le]

Goal state after:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetRing C
hCmeas : ∀ s ∈ C, MeasurableSet s
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : ∀ (t : Set α) (ε : ℝ≥0∞), MeasurableSet t → 0 < ε → ∃ s ∈ C, μ (s ∆ t) < ε
C' : Set (MeasuredSets μ) := {s | ∃ c ∈ C, ↑s = c}
C'C : ∀ s ∈ C', ↑s ∈ C
C'_dense : Dense C'
m₀ : ↑C' → E := fun x ↦ m ↑↑x
s t : ↑C'
this : edist s t = edist ↑s ↑t
Is : ↑↑s ∩ ↑↑t ∪ ↑↑s \ ↑↑t = ↑↑s
It : ↑↑t ∩ ↑↑s ∪ ↑↑t \ ↑↑s = ↑↑t
⊢ ‖m (↑↑s \ ↑↑t) - m (↑↑t \ ↑↑s)‖ₑ ≤ μ (↑↑s \ ↑↑t) + μ (↑↑t \ ↑↑s)
Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation

Goal state before:
pp: case pos
α : Type u_1
inst✝⁸ : LinearOrder α
inst✝⁷ : DenselyOrdered α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : SecondCountableTopology α
inst✝³ : CompactIccSpace α
hα : MeasurableSpace α
inst✝² : BorelSpace α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : α → E
a b : α
hf : BoundedVariationOn f univ
h : a ≤ b
A : ⋯.choose (Ioc a b) = Function.rightLim f b - Function.rightLim f a
hx : ∃ x, IsBot x
⊢ (VectorMeasure.dirac ⋯.choose (Function.rightLim f ⋯.choose - f ⋯.choose)) (Ioc a b) = 0

Tactic:
rw [VectorMeasure.dirac_apply_of_notMem]

Goal state after:
case pos
α : Type u_1
inst✝⁸ : LinearOrder α
inst✝⁷ : DenselyOrdered α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : SecondCountableTopology α
inst✝³ : CompactIccSpace α
hα : MeasurableSpace α
inst✝² : BorelSpace α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : α → E
a b : α
hf : BoundedVariationOn f univ
h : a ≤ b
A : ⋯.choose (Ioc a b) = Function.rightLim f b - Function.rightLim f a
hx : ∃ x, IsBot x
⊢ ⋯.choose ∉ Ioc a b
Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ ν : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
s : Set X
hs : IsHahnDecomposition μ ν s
hsc : IsHahnDecomposition ν μ sᶜ
h₁ :
  ((ν - μ).restrict s).toSignedMeasure =
    VectorMeasure.restrict ν.toSignedMeasure s - VectorMeasure.restrict μ.toSignedMeasure s
h₂ :
  ((μ - ν).restrict sᶜ).toSignedMeasure =
    VectorMeasure.restrict μ.toSignedMeasure sᶜ - VectorMeasure.restrict ν.toSignedMeasure sᶜ
h₁' : ((μ - ν).restrict s).toSignedMeasure = toSignedMeasure 0
h₂' : ((ν - μ).restrict sᶜ).toSignedMeasure = toSignedMeasure 0
partition₁ :
  toSignedMeasure 0 + (VectorMeasure.restrict μ.toSignedMeasure sᶜ - VectorMeasure.restrict ν.toSignedMeasure sᶜ) =
    (μ - ν).toSignedMeasure
partition₂ :
  VectorMeasure.restrict ν.toSignedMeasure s - VectorMeasure.restrict μ.toSignedMeasure s + toSignedMeasure 0 =
    (ν - μ).toSignedMeasure
⊢ μ.toSignedMeasure - ν.toSignedMeasure = (μ - ν).toSignedMeasure - (ν - μ).toSignedMeasure

Tactic:
simp only [toSignedMeasure_zero, zero_add] at partition₁ partition₂

Goal state after:
X : Type u_1
mX : MeasurableSpace X
μ ν : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
s : Set X
hs : IsHahnDecomposition μ ν s
hsc : IsHahnDecomposition ν μ sᶜ
h₁ :
  ((ν - μ).restrict s).toSignedMeasure =
    VectorMeasure.restrict ν.toSignedMeasure s - VectorMeasure.restrict μ.toSignedMeasure s
h₂ :
  ((μ - ν).restrict sᶜ).toSignedMeasure =
    VectorMeasure.restrict μ.toSignedMeasure sᶜ - VectorMeasure.restrict ν.toSignedMeasure sᶜ
h₁' : ((μ - ν).restrict s).toSignedMeasure = toSignedMeasure 0
h₂' : ((ν - μ).restrict sᶜ).toSignedMeasure = toSignedMeasure 0
partition₁ :
  VectorMeasure.restrict μ.toSignedMeasure sᶜ - VectorMeasure.restrict ν.toSignedMeasure sᶜ = (μ - ν).toSignedMeasure
partition₂ :
  VectorMeasure.restrict ν.toSignedMeasure s - VectorMeasure.restrict μ.toSignedMeasure s + 0 = (ν - μ).toSignedMeasure
⊢ μ.toSignedMeasure - ν.toSignedMeasure = (μ - ν).toSignedMeasure - (ν - μ).toSignedMeasure
Module: Mathlib.MeasureTheory.VectorMeasure.Prod

Goal state before:
pp: X : Type u_2
Y : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
mX : MeasurableSpace X
mY : MeasurableSpace Y
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
μ : VectorMeasure X E
ν : VectorMeasure Y F
B : E →L[ℝ] F →L[ℝ] G
inst✝¹ : CompleteSpace G
inst✝ : IsFiniteMeasure μ.variation
s : Set (X × Y)
hs : MeasurableSet s
⊢ μ.prod ν B = μ.prodOfIsFiniteMeasureLeft ν B

Tactic:
apply prod_eq_of_forall_apply_prod (fun s t hs ht ↦ ?_)
    simp [prodOfIsFiniteMeasureLeft, hs.prod ht, ↓reduceIte, mk_preimage_prod_right_eq_if,
      of_if, integral_indicator hs, ContinuousLinearMap.flip_apply, restrict_apply, hs]

Goal state after:
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs

Goal state before:
pp: case mp.mem
M : Type u_1
inst✝ : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
x✝ x : M
hx : x ∈ a +ᵥ ↑(closure t)
⊢ x = 0 ∨ ∃ y ∈ closure (insert a t), a + y = x

Tactic:
rcases hx with ⟨x, hx, rfl⟩
      exact Or.inr ⟨x, closure_mono (subset_insert _ _) hx, rfl⟩

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensityVec

Goal state before:
pp: X : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
mX : MeasurableSpace X
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
μ : VectorMeasure X F
f : X → E
B : E →L[ℝ] F →L[ℝ] G
inst✝ : CompleteSpace G
hf : μ.Integrable f
hB : ∀ (x : E) (y : F), ‖(B x) y‖₊ = ‖B.flip y‖₊ * ‖x‖₊
s : Set X
hs : MeasurableSet s
ε : NNReal
εpos : 0 < ε
δ : NNReal := ε / 3
⊢ 0 < 3

Tactic:
by norm_num

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Integral

Goal state before:
pp: X : Type u_2
E : Type u_4
F : Type u_5
G : Type u_6
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
f : X → E
B : E →L[ℝ] F →L[ℝ] G
inst✝¹ : MeasurableSpace X
inst✝ : CompleteSpace G
a : X
v : F
hfm : StronglyMeasurable f
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : IsFiniteMeasure ((dirac a v).transpose B).variation
⊢ f =ᵐ[‖v‖ₑ • Measure.dirac a] fun x ↦ f a

Tactic:
exact Measure.ae_smul_measure (ae_eq_dirac' hfm.measurable) _

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.SetIntegral

Goal state before:
pp: X : Type u_2
E : Type u_3
F✝ : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F✝
inst✝³ : NormedAddCommGroup G
μ : VectorMeasure X F✝
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F✝
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F✝ →L[ℝ] G
ι : Type u_7
f : X → E
hfi : AEStronglyMeasurable f μ.variation
F : ι → X → E
l : Filter ι
hFi : ∀ᶠ (i : ι) in l, μ.Integrable (F i)
s : Set X
hF : Tendsto (fun i ↦ eLpNorm (fun x ↦ F i x - f x) 1 μ.variation) l (𝓝 0)
i : ι
⊢ μ.variation.restrict s ≤ μ.variation

Tactic:
apply Measure.restrict_le_self

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Integral

Goal state before:
pp: case hbc.hb
X : Type u_2
E : Type u_4
F : Type u_5
G : Type u_6
mX : MeasurableSpace X
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
f : X → E
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
inst✝ : IsFiniteMeasure μ.variation
C : ℝ
h : ∀ᵐ (x : X) ∂μ.variation, ‖f x‖ ≤ C
⊢ ∫⁻ (a : X), ENNReal.ofReal C ∂μ.variation ≠ ∞

Tactic:
simp only [lintegral_const, ne_eq]

Goal state after:
case hbc.hb
X : Type u_2
E : Type u_4
F : Type u_5
G : Type u_6
mX : MeasurableSpace X
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
f : X → E
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
inst✝ : IsFiniteMeasure μ.variation
C : ℝ
h : ∀ᵐ (x : X) ∂μ.variation, ‖f x‖ ≤ C
⊢ ¬ENNReal.ofReal C * μ.variation univ = ∞
Module: Mathlib.MeasureTheory.VectorMeasure.Integral

Goal state before:
pp: case neg
X : Type u_2
E : Type u_4
F : Type u_5
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
μ : VectorMeasure X F
β : Type u_10
inst✝ : MeasurableSpace β
φ : X → β
f : β → E
hfm : AEStronglyMeasurable f (Measure.map φ μ.variation)
h : μ.Integrable (f ∘ φ)
hφ : ¬Measurable φ
⊢ (μ.map φ).Integrable f

Tactic:
simp [VectorMeasure.map, hφ]

Goal state after:
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability

Goal state before:
pp: case func.inr
α : Type u_1
A : Set ℕ
inst✝ : Fintype α
l : ℕ
ts : Fin l → presburger[[↑A]].Term α
ih : ∀ (a : Fin l), ∃ k u, ∀ (v : α → ℕ), Term.realize v (ts a) = k + u ⬝ᵥ v
f : (constantsOn ↑A).Functions l
⊢ ∃ k u, ∀ (v : α → ℕ), (Structure.funMap (Sum.inr f) fun i ↦ Term.realize v (ts i)) = k + u ⬝ᵥ v

Tactic:
cases l with

Goal state after:
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability

Goal state before:
pp: A : Set ℕ
⊢ ¬A.Definable presburger {v | v 0 = v 1 * v 2}

Tactic:
intro hmul
  have hsqr : A.Definable₁ presburger {x * x | x : ℕ} := by
    rw [Definable₁]
    convert! (hmul.preimage_comp (β := Fin 2) ![0, 1, 1]).image_comp ![0]
    ext
    simpa [funext_iff, Fin.exists_fin_succ_pi] using exists_congr fun _ => Eq.comm
  rw [definable₁_iff_ultimately_periodic] at hsqr
  rcases hsqr with ⟨k, p, hp, h⟩
  specialize h ((max k p) * (max k p)) ((Nat.le_mul_self _).trans' (le_max_left _ _))
  simp only [mem_ofPred_eq, exists_apply_eq_apply, true_iff] at h
  rcases h with ⟨x, h₁⟩
  by_cases h₂ : x ≤ max k p
  · apply Nat.mul_self_le_mul_self at h₂
    grind
  · simp only [not_le, Nat.lt_iff_add_one_le] at h₂
    apply Nat.mul_self_le_mul_self at h₂
    grind

Goal state after:
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: L : Language
M : Type u_1
inst✝¹ : L.Structure M
N : Type u_2
inst✝ : L.Structure N
f : M ↪[L] N
s : L.Substructure M
hs : (Substructure.map f.toHom s).CG
⊢ s.CG

Tactic:
by
  rcases hs with ⟨t, h1, h2⟩
  rw [cg_def]
  refine ⟨f ⁻¹' t, h1.preimage f.injective, ?_⟩
  have hf : Function.Injective f.toHom := f.injective
  refine map_injective_of_injective hf ?_
  rw [← h2, map_closure, Embedding.coe_toHom, image_preimage_eq_of_subset]
  intro x hx
  have h' := subset_closure (L := L) hx
  rw [h2] at h'
  exact Hom.map_le_range h'

Goal state after:
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case refine_1
M : Type u_1
inst✝ : AddCommMonoid M
s : Set M
a : M
x✝ : ∃ P, (∃ n f, AddMonoidHom.mrange f = P) ∧ s = a +ᵥ ↑P
P : AddSubmonoid M
n : ℕ
f : (Fin n → ℕ) →+ M
hf : AddMonoidHom.mrange f = P
hs : s = a +ᵥ ↑P
⊢ s = a +ᵥ ↑(AddMonoidHom.mrange f)

pp: case refine_2
M : Type u_1
inst✝ : AddCommMonoid M
s : Set M
a : M
x✝ : ∃ n f, s = a +ᵥ ↑(AddMonoidHom.mrange f)
n : ℕ
f : (Fin n → ℕ) →+ M
hs : s = a +ᵥ ↑(AddMonoidHom.mrange f)
⊢ s = a +ᵥ ↑(AddMonoidHom.mrange f)

Tactic:
· rw [hf, hs]

Goal state after:
case refine_2
M : Type u_1
inst✝ : AddCommMonoid M
s : Set M
a : M
x✝ : ∃ n f, s = a +ᵥ ↑(AddMonoidHom.mrange f)
n : ℕ
f : (Fin n → ℕ) →+ M
hs : s = a +ᵥ ↑(AddMonoidHom.mrange f)
⊢ s = a +ᵥ ↑(AddMonoidHom.mrange f)
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: L : Language
G' : ℕ → Type w
inst✝ : (i : ℕ) → L.Structure (G' i)
f' : (n : ℕ) → G' n ↪[L] G' (n + 1)
m k : ℕ
h : m ≤ m + k
x : G' m
⊢ (natLERec f' m (m + k) h) x = Nat.leRecOn h (fun k ↦ ⇑(f' k)) x

Tactic:
induction k with

Goal state after:
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
x : ι → ℕ
⊢ 0 ≤ toRatVec x

Tactic:
rw [← map_zero toRatVec, toRatVec_mono]
  simp

Goal state after:
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x y : ι → ℕ
i : ↑hs.basisSet
hy : y ∈ closure hs.basisSet
⊢ 0 ≤ (hs.basis.repr (toRatVec y)) i

Tactic:
mem_closure_iff_of_fintype

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x y : ι → ℕ
i : ↑hs.basisSet
hy : ∃ a, y = ∑ i, a i • ↑i
⊢ 0 ≤ (hs.basis.repr (toRatVec y)) i
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M ≃ₚ[L] N
A : L.Substructure M
h : A ≤ f.dom
⊢ M ≃ₚ[L] N

Tactic:
by
  let g := (subtype _).comp (f.toEquiv.toEmbedding.comp (A.inclusion h))
  exact {
    dom := A
    cod := g.toHom.range
    toEquiv := g.equivRange
  }

Goal state after:
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: L : Language
M : Type w
inst✝¹ : L.Structure M
inst✝ : Countable M
g : L.FGEquiv M M → (U : { S // S.FG }) × (↥↑U →[L] M) :=
  fun f ↦ ⟨⟨(↑f).dom, ⋯⟩, (↑f).cod.subtype.toHom.comp (↑f).toEquiv.toHom⟩
f f' : L.FGEquiv M M
dom_f cod_f : L.Substructure M
equiv_f : ↥dom_f ≃[L] ↥cod_f
f_fin : { dom := dom_f, cod := cod_f, toEquiv := equiv_f }.dom.FG
h : g ⟨{ dom := dom_f, cod := cod_f, toEquiv := equiv_f }, f_fin⟩ = g f'
⊢ ↑⟨{ dom := dom_f, cod := cod_f, toEquiv := equiv_f }, f_fin⟩ = ↑f'

Tactic:
cases congr_arg (·.1) h

Goal state after:
case refl
L : Language
M : Type w
inst✝¹ : L.Structure M
inst✝ : Countable M
g : L.FGEquiv M M → (U : { S // S.FG }) × (↥↑U →[L] M) :=
  fun f ↦ ⟨⟨(↑f).dom, ⋯⟩, (↑f).cod.subtype.toHom.comp (↑f).toEquiv.toHom⟩
f f' : L.FGEquiv M M
cod_f : L.Substructure M
equiv_f : ↥(↑f').1 ≃[L] ↥cod_f
f_fin : { dom := (↑f').1, cod := cod_f, toEquiv := equiv_f }.dom.FG
h : g ⟨{ dom := (↑f').1, cod := cod_f, toEquiv := equiv_f }, f_fin⟩ = g f'
⊢ ↑⟨{ dom := (↑f').1, cod := cod_f, toEquiv := equiv_f }, f_fin⟩ = ↑f'
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensityVec

Goal state before:
pp: X : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
mX : MeasurableSpace X
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
μ : VectorMeasure X F
f : X → E
B : E →L[ℝ] F →L[ℝ] G
inst✝ : CompleteSpace G
hf : μ.Integrable f
hB : ∀ (x : E) (y : F), ‖(B x) y‖₊ = ‖B.flip y‖₊ * ‖x‖₊
s : Set X
hs : MeasurableSet s
ε : NNReal
εpos : 0 < ε
δ : NNReal := ε / 3
δpos : 0 < δ
g : X →ₛ E
hg : eLpNorm (f - ⇑g) 1 (μ.transpose B).variation ≤ ↑δ
gmem : MemLp (⇑g) 1 μ.variation
I1 : ∫⁻ (a : X) in s, ‖f a‖ₑ ∂(μ.transpose B).variation ≤ ∫⁻ (a : X) in s, ‖g a‖ₑ ∂(μ.transpose B).variation + ↑δ
I2 :
  ∫⁻ (a : X) in s, ‖g a‖ₑ ∂(μ.transpose B).variation =
    ∑ i ∈ g.range, ‖i‖ₑ * ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i})
ρ : ℝ≥0∞
ρpos : ρ > 0
hρ : ∑ i ∈ g.range, ‖i‖ₑ * ρ ≤ ↑δ
P : E → Finset (Set X)
Pg : ∀ (i : E), ∀ t ∈ P i, t ⊆ ⇑g ⁻¹' {i}
Pdisj : ∀ (i : E), (↑(P i)).PairwiseDisjoint id
Pmeas : ∀ (i : E), ∀ t ∈ P i, MeasurableSet t
hP :
  ∀ (i : E),
    ‖i‖ₑ * ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i}) ≤
      ‖i‖ₑ * (∑ p ∈ P i, ‖((μ.transpose B).restrict s) p‖ₑ + ρ)
I3 :
  ∑ i ∈ g.range, ‖i‖ₑ * ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i}) ≤
    ∑ i ∈ g.range.sigma P, ‖i.fst‖ₑ * ‖((μ.transpose B).restrict s) i.snd‖ₑ + ↑δ
i : (_ : E) × Set X
hi : i ∈ g.range.sigma P
⊢ (μ.transpose B).variation.restrict s ≤ (μ.transpose B).variation

Tactic:
apply Measure.restrict_le_self

Goal state after:
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: case refine_1.refine_2
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
h : L.IsExtensionPair M N
S : L.Substructure M
S_FG : S.FG
f : ↥S ↪[L] N
m : M
f' : M ≃ₚ[L] N
hf' : f'.dom.FG
mf' : m ∈ (↑⟨f', hf'⟩).dom
ff'1 : (↑⟨{ dom := S, cod := f.toHom.range, toEquiv := f.equivRange }, S_FG⟩).dom ≤ (↑⟨f', hf'⟩).dom
ff'2 :
  (↑⟨f', hf'⟩).cod.subtype.comp ((↑⟨f', hf'⟩).toEquiv.toEmbedding.comp (Substructure.inclusion ff'1)) =
    (↑⟨{ dom := S, cod := f.toHom.range, toEquiv := f.equivRange }, S_FG⟩).cod.subtype.comp
      (↑⟨{ dom := S, cod := f.toHom.range, toEquiv := f.equivRange }, S_FG⟩).toEquiv.toEmbedding
⊢ f = (f'.toEmbedding.comp (Substructure.inclusion ⋯)).comp (Substructure.inclusion ⋯)

Tactic:
· ext ⟨x, hx⟩
      rw [Embedding.subtype_equivRange] at ff'2
      simp only [← ff'2, Embedding.comp_apply, Substructure.coe_inclusion,
        Equiv.coe_toEmbedding, coe_subtype, PartialEquiv.toEmbedding_apply]

Goal state after:
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x y : ι → ℕ
hy : y ∈ closure hs.basisSet
⊢ hs.fract (x + y) = hs.fract x

Tactic:
mem_closure_iff_of_fintype

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x y : ι → ℕ
hy : ∃ a, y = ∑ i, a i • ↑i
⊢ hs.fract (x + y) = hs.fract x
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensityVec

Goal state before:
pp: case h2
X : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
mX : MeasurableSpace X
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
μ : VectorMeasure X F
f : X → E
B : E →L[ℝ] F →L[ℝ] G
inst✝ : CompleteSpace G
hf : μ.Integrable f
hB : ∀ (x : E) (y : F), ‖(B x) y‖₊ = ‖B.flip y‖₊ * ‖x‖₊
s : Set X
hs : MeasurableSet s
ε : NNReal
εpos : 0 < ε
δ : NNReal := ⋯
δpos : 0 < δ
g : X →ₛ E
hg : eLpNorm (f - ⇑g) 1 (μ.transpose B).variation ≤ ↑δ
gmem : MemLp (⇑g) 1 μ.variation
I1 : ∫⁻ (a : X) in s, ‖f a‖ₑ ∂(μ.transpose B).variation ≤ ∫⁻ (a : X) in s, ‖g a‖ₑ ∂(μ.transpose B).variation + ↑δ
I2 :
  ∫⁻ (a : X) in s, ‖g a‖ₑ ∂(μ.transpose B).variation =
    ∑ i ∈ g.range, ‖i‖ₑ * ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i})
ρ : ℝ≥0∞
ρpos : ρ > 0
hρ : ∑ i ∈ g.range, ‖i‖ₑ * ρ ≤ ↑δ
P : E → Finset (Set X)
Pg : ∀ (i : E), ∀ t ∈ P i, t ⊆ ⇑g ⁻¹' {i}
Pdisj : ∀ (i : E), (↑(P i)).PairwiseDisjoint id
Pmeas : ∀ (i : E), ∀ t ∈ P i, MeasurableSet t
hP :
  ∀ (i : E),
    ‖i‖ₑ * ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i}) ≤
      ‖i‖ₑ * (∑ p ∈ P i, ‖((μ.transpose B).restrict s) p‖ₑ + ρ)
I3 :
  ∑ i ∈ g.range, ‖i‖ₑ * ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i}) ≤
    ∑ i ∈ g.range.sigma P, ‖i.fst‖ₑ * ‖((μ.transpose B).restrict s) i.snd‖ₑ + ↑δ
⊢ (μ.transpose B).variation.restrict (⋃ i ∈ g.range.sigma P, i.snd) ≤ (μ.transpose B).variation

Tactic:
apply Measure.restrict_le_self

Goal state after:
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: case mpr
L : Language
inst✝ : Countable ((l : ℕ) × L.Functions l)
M : Bundled L.Structure
hM : Structure.CG L ↑M
Kn : (L.age ↑M).Nonempty
left✝ : ∀ (M_1 N : Bundled L.Structure), Nonempty (↑M_1 ≃[L] ↑N) → (M_1 ∈ L.age ↑M ↔ N ∈ L.age ↑M)
cq : (Quotient.mk' '' L.age ↑M).Countable
hfg : ∀ M_1 ∈ L.age ↑M, Structure.FG L ↑M_1
hp : Hereditary (L.age ↑M)
jep : JointEmbedding (L.age ↑M)
⊢ ∃ M_1, Countable ↑M_1 ∧ L.age ↑M_1 = L.age ↑M

Tactic:
exact ⟨M, Structure.cg_iff_countable.1 hM, rfl⟩

Goal state after:
Module: Mathlib.Topology.Order.IsLocallyClosed

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
a b : X
inst✝¹ : LinearOrder X
inst✝ : ClosedIicTopology X
⊢ IsLocallyClosed (Set.Ioc a b)

Tactic:
rw [← Set.Iic_inter_Ioi]
  exact isLocallyClosed_Iic.inter isLocallyClosed_Ioi

Goal state after:
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 3 ≤ p
h3q : 3 ≤ q
h3r : 3 ≤ r
hp : (↑↑p)⁻¹ ≤ 3⁻¹
hq : (↑↑q)⁻¹ ≤ 3⁻¹
hr : (↑↑r)⁻¹ ≤ 3⁻¹
⊢ 3⁻¹ + 3⁻¹ + 3⁻¹ = 1

Tactic:
by norm_num

Goal state after:
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: q r : ℕ+
hqr : q ≤ r
H : 4 ≤ q
h4r : 4 ≤ r
hq : (↑↑q)⁻¹ ≤ 4⁻¹
hr : (↑↑r)⁻¹ ≤ 4⁻¹
⊢ 2⁻¹ + 4⁻¹ + 4⁻¹ = 1

Tactic:
by norm_num

Goal state after:
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: r : ℕ+
H : 6 ≤ r
hr : (↑↑r)⁻¹ ≤ 6⁻¹
⊢ 2⁻¹ + 3⁻¹ + 6⁻¹ = 1

Tactic:
by norm_num

Goal state after:
Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael

Goal state before:
pp: case neg.refine_1
n : ℕ
hn : n ≠ 2
hn' : ¬n ≤ 2
hcard : Nat.card (ZMod (2 ^ n))ˣ = 2 ^ (n - 1)
⊢ exponent (ZMod (2 ^ n))ˣ ∣ 2 ^ (n - 2)

Tactic:
have ⟨k, hk, h⟩ := dvd_prime_pow prime_two |>.mp <| hcard ▸ Group.exponent_dvd_nat_card

Goal state after:
case neg.refine_1
n : ℕ
hn : n ≠ 2
hn' : ¬n ≤ 2
hcard : Nat.card (ZMod (2 ^ n))ˣ = 2 ^ (n - 1)
k : ℕ
hk : k ≤ n - 1
h : exponent (ZMod (2 ^ n))ˣ = 2 ^ k
⊢ exponent (ZMod (2 ^ n))ˣ ∣ 2 ^ (n - 2)
Module: Mathlib.NumberTheory.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
p : ℕ
a b : R
h : ↑p ∣ a - b
k : ℕ
⊢ ↑p ^ (k + 1) ∣ a ^ p ^ k - b ^ p ^ k

Tactic:
induction k with

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Derivative

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
r : R
f : MvPowerSeries σ R
⊢ pderivFun i (C r * f) = C r * pderivFun i f

Tactic:
pderivFun_mul,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
r : R
f : MvPowerSeries σ R
⊢ C r • pderivFun i f + f • pderivFun i (C r) = C r * pderivFun i f
Module: Mathlib.RingTheory.MvPowerSeries.Derivative

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsAddTorsionFree R
f g : MvPowerSeries σ R
hD : ∀ (i : σ), (pderiv R i) f = (pderiv R i) g
hc : constantCoeff f = constantCoeff g
n : σ →₀ ℕ
h : ¬n = 0
i : σ
hi : n i ≠ 0
this : single i 1 ≤ n
e : n i • (coeff n) f = n i • (coeff n) g
⊢ (coeff n) f = (coeff n) g

Tactic:
smul_right_inj hi

Goal state after:
case neg
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsAddTorsionFree R
f g : MvPowerSeries σ R
hD : ∀ (i : σ), (pderiv R i) f = (pderiv R i) g
hc : constantCoeff f = constantCoeff g
n : σ →₀ ℕ
h : ¬n = 0
i : σ
hi : n i ≠ 0
this : single i 1 ≤ n
e : (coeff n) f = (coeff n) g
⊢ (coeff n) f = (coeff n) g
Module: Mathlib.RingTheory.PowerSeries.Exp

Goal state before:
pp: case e_a
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
⊢ ↑(n ! / (x ! * (n - x)!)) = ↑n ! / ↑(x ! * (n - x)!)

Tactic:
cast_div_charZero

Goal state after:
case e_a
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
⊢ ↑n ! / ↑(x ! * (n - x)!) = ↑n ! / ↑(x ! * (n - x)!)

case e_a
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
⊢ x ! * (n - x)! ∣ n !
Module: Mathlib.RingTheory.PowerSeries.Exp

Goal state before:
pp: A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
k : ℕ
⊢ exp A ^ k = (rescale ↑k) (exp A)

Tactic:
induction k with

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: n : ℕ
⊢ eval 1 (bernoulli n) = bernoulli' n

Tactic:
simp only [bernoulli, eval_finsetSum]
  simp only [← succ_eq_add_one, sum_range_succ, mul_one, cast_one, choose_self,
    (_root_.bernoulli _).mul_comm, sum_bernoulli, one_pow, mul_one, eval_monomial, one_mul]
  by_cases h : n = 1
  · norm_num [h]
  · simp [h, bernoulli_eq_bernoulli'_of_ne_one h]

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: case a
n d : ℕ
hd : ∀ m < d + 1, (bernoulli m).comp (1 + X) = bernoulli m + m • X ^ (m - 1)
| ∑ i ∈ range (d + 1), ((d + 2).choose i • bernoulli i).comp (1 + X)

Tactic:
apply_congr
      · skip
      · rw [smul_comp, hd _ (mem_range.1 (by assumption))]

Goal state after: