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

Goal state before:

Tactic:
‖μ s‖ₑ
  _ = ‖(μ.mapRange (ℓ : E →+ ℝ) ℓ.continuous) s‖ₑ := by simp [← ofReal_norm, hℓ]
  _ ≤ (μ.mapRange (ℓ : E →+ ℝ) ℓ.continuous).variation s := enorm_measure_le_variation _ _
  _ ≤ μ.semivariation s := by apply le_biSup _ h'ℓ

Goal state after:
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
lip : LipschitzWith 1 m₀
m₁ : MeasuredSets μ → E := C'_dense.extend m₀
m₁_lip : LipschitzWith 1 m₁
hBound : ∀ (s : MeasuredSets μ), ‖m₁ s‖ₑ ≤ μ ↑s
hAddit : ∀ (s t : MeasuredSets μ), Disjoint ↑s ↑t → m₁ ⟨↑s ∪ ↑t, ⋯⟩ = m₁ s + m₁ t
m' : Set α → E := fun s ↦ if hs : MeasurableSet s then m₁ ⟨s, hs⟩ else 0
⊢ ∃ m', (∀ s ∈ C, m' s = m s) ∧ ∀ (s : Set α), ‖m' s‖ₑ ≤ μ s

Tactic:
let m'' : VectorMeasure α E := by
    apply VectorMeasure.of_additive_of_le_measure m' (μ := μ)
    · intro s
      by_cases hs : MeasurableSet s
      · simpa [hs, m'] using! hBound _
      · simp [hs, m']
    · intro s t hs ht hst
      simp only [hs, ht, MeasurableSet.union, ↓reduceDIte, m']
      exact hAddit ⟨s, hs⟩ ⟨t, ht⟩ hst
    · intro s hs
      simp [m', hs]

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
lip : LipschitzWith 1 m₀
m₁ : MeasuredSets μ → E := C'_dense.extend m₀
m₁_lip : LipschitzWith 1 m₁
hBound : ∀ (s : MeasuredSets μ), ‖m₁ s‖ₑ ≤ μ ↑s
hAddit : ∀ (s t : MeasuredSets μ), Disjoint ↑s ↑t → m₁ ⟨↑s ∪ ↑t, ⋯⟩ = m₁ s + m₁ t
m' : Set α → E := fun s ↦ if hs : MeasurableSet s then m₁ ⟨s, hs⟩ else 0
m'' : VectorMeasure α E := of_additive_of_le_measure m' ⋯ ⋯ ⋯
⊢ ∃ m', (∀ s ∈ C, m' s = m s) ∧ ∀ (s : Set α), ‖m' s‖ₑ ≤ μ s
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
H : Type u_6
mX : MeasurableSpace X
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedAddCommGroup H
μ : VectorMeasure X F
f : X → E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedSpace ℝ F
inst✝³ : NormedSpace ℝ G
inst✝² : NormedSpace ℝ H
B : E →L[ℝ] F →L[ℝ] G
inst✝¹ : CompleteSpace G
inst✝ : CompleteSpace H
C : G →L[ℝ] H
hf : Integrable f μ.variation
⊢ C ∫ᵛ (y : X), f y ∂[B; μ] = ∫ᵛ (y : X), f y ∂[(compL ℝ F G H) C ∘SL B; μ]

Tactic:
apply hf.induction (P := fun f ↦ C (∫ᵛ y, f y ∂[B; μ]) = ∫ᵛ y, f y ∂[((compL ℝ F G H C) ∘L B); μ])
  · intro c s hs hc
    have : IsFiniteMeasure (μ.variation.restrict s) := ⟨by simpa⟩
    simp [integral_indicator_const _ hs]
  · intro f g _ f_int g_int hf hg
    simp only [Pi.add_apply]
    simp [integral_fun_add, f_int, g_int, hf, hg]
  · apply isClosed_eq
    · apply C.continuous.comp continuous_integral
    · exact continuous_integral
  · intro f g hfg _ hf
    rw [← integral_congr_ae hfg, ← integral_congr_ae hfg, hf]

Goal state after:
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 : IsSetSemiring C
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : hα = generateFrom C
M : ∀ s ∈ C, MeasurableSet s
D : Set (Set α)
DC : D ⊆ C
D_count : D.Countable
hD : ∀ s ∈ C, s ≤ᵐ[μ] ⋃₀ D
MD : MeasurableSet (⋃₀ D)
μ' : Measure α := μ.restrict (⋃₀ D)
⊢ μ' (⋃₀ D)ᶜ = 0

Tactic:
simp [μ', Measure.restrict_apply' MD]

Goal state after:
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 : IsSetSemiring C
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : hα = generateFrom C
M : ∀ s ∈ C, MeasurableSet s
D : Set (Set α)
DC : D ⊆ C
D_count : D.Countable
hD : ∀ s ∈ C, s ≤ᵐ[μ] ⋃₀ D
MD : MeasurableSet (⋃₀ D)
μ' : Measure α := μ.restrict (⋃₀ D)
⊢ ∃ D, D.Countable ∧ D ⊆ C ∧ μ' (⋃₀ D)ᶜ = 0

Tactic:
exact ⟨D, D_count, DC, by simp [μ', Measure.restrict_apply' MD]⟩

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

Goal state before:
pp: ι : Type u_1
X : Type u_2
Y : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
H : Type u_7
I : Type u_8
J : Type u_9
mX : MeasurableSpace X
mY : MeasurableSpace Y
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
inst✝⁶ : NormedAddCommGroup H
inst✝⁵ : NormedSpace ℝ H
inst✝⁴ : NormedAddCommGroup I
inst✝³ : NormedSpace ℝ I
inst✝² : NormedAddCommGroup J
inst✝¹ : NormedSpace ℝ J
μ✝ : VectorMeasure X E
ν✝ : VectorMeasure Y F
B✝ : E →L[ℝ] F →L[ℝ] G
μ : VectorMeasure X E
ν : VectorMeasure Y F
B : E →L[ℝ] F →L[ℝ] G
inst✝ : IsFiniteMeasure μ.variation
f : ℕ → Set (X × Y)
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Disjoint on f)
a : Finset ℕ
⊢ ∑ y ∈ a, ∫ᵛ (x : X), ν (Prod.mk x ⁻¹' f y) ∂[B.flip; μ] = ∫ᵛ (x : X), ∑ y ∈ a, ν (Prod.mk x ⁻¹' f y) ∂[B.flip; μ]

Tactic:
rw [integral_finsetSum _ (fun i hi ↦ integrable_vectorMeasure_prodMk_left (f_meas i))]

Goal state after:
Module: Mathlib.MeasureTheory.VectorMeasure.Variation.SignedMeasure

Goal state before:
pp: case pos
X : Type u_1
mX : MeasurableSpace X
s : SignedMeasure X
i : Set X
hi : MeasurableSet i
⊢ ‖s i‖ ≤ s.totalVariation.real i

Tactic:
s.apply_eq_posPart_real_sub_negPart_real hi,

Goal state after:
case pos
X : Type u_1
mX : MeasurableSpace X
s : SignedMeasure X
i : Set X
hi : MeasurableSet i
⊢ ‖s.toJordanDecomposition.posPart.real i - s.toJordanDecomposition.negPart.real i‖ ≤ s.totalVariation.real i
Module: Mathlib.MeasureTheory.VectorMeasure.Integral

Goal state before:
pp: case pos
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
hμ : μ.variation = 0
⊢ ‖B‖ * (∫⁻ (a : X), ENNReal.ofReal C ∂μ.variation).toReal = ‖B‖ * (C * μ.variation.real univ)

pp: case neg
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
hμ : ¬μ.variation = 0
⊢ ‖B‖ * (∫⁻ (a : X), ENNReal.ofReal C ∂μ.variation).toReal = ‖B‖ * (C * μ.variation.real univ)

Tactic:
· simp [hμ]

Goal state after:
case neg
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
hμ : ¬μ.variation = 0
⊢ ‖B‖ * (∫⁻ (a : X), ENNReal.ofReal C ∂μ.variation).toReal = ‖B‖ * (C * μ.variation.real univ)
Module: Mathlib.ModelTheory.Complexity

Goal state before:
pp: L : Language
α : Type u'
n : ℕ
M : Type u_1
inst✝⁴ : L.Structure M
N : Type u_2
inst✝³ : L.Structure N
F : Type u_3
inst✝² : FunLike F M N
inst✝¹ : EmbeddingLike F M N
inst✝ : L.StrongHomClass F M N
φ : L.BoundedFormula α n
hQF : φ.IsQF
f : F
v : α → M
xs : Fin n → M
⊢ φ.Realize (⇑f ∘ v) (⇑f ∘ xs) ↔ φ.Realize v xs

Tactic:
by
  induction hQF with
  | falsum => rfl
  | of_isAtomic hA => induction hA with
    | equal t₁ t₂ => simp only [realize_bdEqual, ← Sum.comp_elim, HomClass.realize_term,
        (EmbeddingLike.injective f).eq_iff]
    | rel R ts =>
      simp only [realize_rel, ← Sum.comp_elim, HomClass.realize_term]
      exact StrongHomClass.map_rel f R (fun i => Term.realize (Sum.elim v xs) (ts i))
  | imp _ _ ihφ ihψ => simp only [realize_imp, ihφ, ihψ]

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

Goal state before:
pp: M : Type u_1
ι : Type u_3
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Finite ι
F : Type u_5
G : Type u_6
inst✝³ : FunLike F (ι → ℕ) M
inst✝² : AddMonoidHomClass F (ι → ℕ) M
inst✝¹ : FunLike G (ι → ℕ) M
inst✝ : AddMonoidHomClass G (ι → ℕ) M
a b : M
f : F
g : G
⊢ IsSemilinearSet {x | a + f x = b + g x}

Tactic:
by
  apply isSemilinearSet_of_isSlice
  intro x hx y z hy hz
  simp only [mem_ofPred, map_add, ← add_assoc] at *
  conv_lhs => rw [hy, ← hx, add_right_comm _ (g y) (f z), hz, add_right_comm _ (g z)]

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

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
P₁ : AddSubmonoid M
s₁' : Set ↥P₁
hP₁ : P₁.FG
hs₁' : IsSemilinearSet s₁'
hs₁ : IsSemilinearSet (Subtype.val '' s₁')
P₂ : AddSubmonoid M
s₂' : Set ↥P₂
hP₂ : P₂.FG
hs₂' : IsSemilinearSet s₂'
hs₂ : IsSemilinearSet (Subtype.val '' s₂')
⊢ ∃ P s₁'_1 s₂'_1,
    P.FG ∧
      IsSemilinearSet s₁'_1 ∧
        Subtype.val '' s₁' = Subtype.val '' s₁'_1 ∧ IsSemilinearSet s₂'_1 ∧ Subtype.val '' s₂' = Subtype.val '' s₂'_1

Tactic:
refine ⟨P₁ ⊔ P₂, (AddSubmonoid.inclusion le_sup_left) '' s₁',
    (AddSubmonoid.inclusion le_sup_right) '' s₂', hP₁.sup hP₂, hs₁'.image _, ?_, hs₂'.image _, ?_⟩

Goal state after:
case refine_1
M : Type u_1
inst✝ : AddCommMonoid M
P₁ : AddSubmonoid M
s₁' : Set ↥P₁
hP₁ : P₁.FG
hs₁' : IsSemilinearSet s₁'
hs₁ : IsSemilinearSet (Subtype.val '' s₁')
P₂ : AddSubmonoid M
s₂' : Set ↥P₂
hP₂ : P₂.FG
hs₂' : IsSemilinearSet s₂'
hs₂ : IsSemilinearSet (Subtype.val '' s₂')
⊢ Subtype.val '' s₁' = Subtype.val '' ⇑(AddSubmonoid.inclusion ⋯) '' s₁'

case refine_2
M : Type u_1
inst✝ : AddCommMonoid M
P₁ : AddSubmonoid M
s₁' : Set ↥P₁
hP₁ : P₁.FG
hs₁' : IsSemilinearSet s₁'
hs₁ : IsSemilinearSet (Subtype.val '' s₁')
P₂ : AddSubmonoid M
s₂' : Set ↥P₂
hP₂ : P₂.FG
hs₂' : IsSemilinearSet s₂'
hs₂ : IsSemilinearSet (Subtype.val '' s₂')
⊢ Subtype.val '' s₂' = Subtype.val '' ⇑(AddSubmonoid.inclusion ⋯) '' s₂'
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
s₁ s₂ : Set M
hs₁ : IsSemilinearSet s₁
hs₂ : IsSemilinearSet s₂
⊢ IsSemilinearSet (s₁ ∩ s₂)

Tactic:
rcases hs₁.exists_fg_eq_subtypeVal₂ hs₂ with ⟨P, s₁', s₂', hP, hs₁', rfl, hs₂', rfl⟩
  rw [← image_inter Subtype.val_injective]
  apply image (f := P.subtype)
  rw [← AddMonoid.fg_iff_addSubmonoid_fg, AddMonoid.fg_def, fg_iff_exists_fin_addMonoidHom] at hP
  rcases hP with ⟨n, f, hf⟩
  rw [AddMonoidHom.mrange_eq_top] at hf
  rw [← image_preimage_eq (s₁' ∩ s₂') hf, preimage_inter]
  apply image
  apply Nat.isSemilinearSet_inter <;> apply Nat.isSemilinearSet_preimage <;> assumption

Goal state after:
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:
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: 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'

Tactic:
apply PartialEquiv.ext (by rfl)

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) := ⋯
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'
⊢ ∀ (x : M) (h : x ∈ (↑⟨{ dom := (↑f').1, cod := cod_f, toEquiv := equiv_f }, f_fin⟩).dom),
    (↑⟨{ dom := (↑f').1, cod := cod_f, toEquiv := equiv_f }, f_fin⟩).cod.subtype
        ((↑⟨{ dom := (↑f').1, cod := cod_f, toEquiv := equiv_f }, f_fin⟩).toEquiv ⟨x, h⟩) =
      (↑f').cod.subtype ((↑f').toEquiv ⟨x, ⋯⟩)
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:
by
  classical
  rw [mem_closure_iff_of_fintype] at hy
  rcases hy with ⟨f, t, ht, hf, rfl⟩
  rw [← toRatVec_inj, hs.toRatVec_fract_eq, hs.toRatVec_fract_eq]
  congr! 3
  rw [map_add, ← sub_add_eq_add_sub]
  simp [-nsmul_eq_mul, ← hs.basis_apply, Finsupp.single_apply]

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

Goal state before:
pp: case mpr
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
⊢ (hs.fract x = hs.base ∧ ∀ (i : ↑hs.basisSet), 0 ≤ hs.floor x i ∧ (↑i ∉ hs.periods → hs.floor x i = 0)) →
    ∃ y ∈ closure hs.periods, hs.base + y = x

Tactic:
intro ⟨hx₁, hx₂⟩

Goal state after:
case mpr
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
hx₁ : hs.fract x = hs.base
hx₂ : ∀ (i : ↑hs.basisSet), 0 ≤ hs.floor x i ∧ (↑i ∉ hs.periods → hs.floor x i = 0)
⊢ ∃ y ∈ closure hs.periods, hs.base + y = x
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 ∈ g.range.sigma P, ‖∫ᵛ (x : X) in i.snd, f x ∂[B; μ.restrict s]‖ₑ +
      ∫⁻ (x : X), ‖g x - f x‖ₑ ∂(μ.transpose B).variation ≤
    ∑ i ∈ g.range.sigma P, ‖∫ᵛ (x : X) in i.snd, f x ∂[B; μ.restrict s]‖ₑ + ↑δ

Tactic:
gcongr
      simp_rw [enorm_sub_rev, ← eLpNorm_one_eq_lintegral_enorm]
      exact hg

Goal state after:
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: case refine_2
L : Language
K : Set (Bundled L.Structure)
hn : K.Nonempty
hc : (Quotient.mk' '' K).Countable
fg : ∀ M ∈ K, Structure.FG L ↑M
hp : Hereditary K
jep : JointEmbedding K
F : ℕ → Quotient equivSetoid
hF : ∀ (a : Bundled L.Structure), (∃ x ∈ K, (Quotient.mk' x).out ≈ a) ↔ ∃ y, (F y).out ≈ a
hF' : ∀ (n : ℕ), (F n).out ∈ K
P : ↑K → ℕ → Bundled L.Structure
hPK : ∀ (N : ↑K) (n : ℕ), P N n ∈ K
hP : ∀ (N : ↑K) (n : ℕ), (fun M N ↦ Nonempty (↑M ↪[L] ↑N)) (↑N) (P N n)
hFP : ∀ (N : ↑K) (n : ℕ), (fun M N ↦ Nonempty (↑M ↪[L] ↑N)) (F (n + 1)).out (P N n)
G : ℕ → ↑K := Nat.rec ⟨(F 0).out, ⋯⟩ fun n N ↦ ⟨P N n, ⋯⟩
f : (i j : ℕ) → i ≤ j → ↑↑(G i) ↪[L] ↑↑(G j) := DirectedSystem.natLERec fun n ↦ Nonempty.some ⋯
N : Bundled L.Structure
KN : N ∈ K
this : (Quotient.mk' N).out ≈ N
⊢ N ∈ ⋃ i, L.age ↑↑(G i)

Tactic:
obtain ⟨n, ⟨e⟩⟩ := (hF N).1 ⟨N, KN, this⟩

Goal state after:
case refine_2
L : Language
K : Set (Bundled L.Structure)
hn : K.Nonempty
hc : (Quotient.mk' '' K).Countable
fg : ∀ M ∈ K, Structure.FG L ↑M
hp : Hereditary K
jep : JointEmbedding K
F : ℕ → Quotient equivSetoid
hF : ∀ (a : Bundled L.Structure), (∃ x ∈ K, (Quotient.mk' x).out ≈ a) ↔ ∃ y, (F y).out ≈ a
hF' : ∀ (n : ℕ), (F n).out ∈ K
P : ↑K → ℕ → Bundled L.Structure
hPK : ∀ (N : ↑K) (n : ℕ), P N n ∈ K
hP : ∀ (N : ↑K) (n : ℕ), (fun M N ↦ Nonempty (↑M ↪[L] ↑N)) (↑N) (P N n)
hFP : ∀ (N : ↑K) (n : ℕ), (fun M N ↦ Nonempty (↑M ↪[L] ↑N)) (F (n + 1)).out (P N n)
G : ℕ → ↑K := Nat.rec ⟨(F 0).out, ⋯⟩ fun n N ↦ ⟨P N n, ⋯⟩
f : (i j : ℕ) → i ≤ j → ↑↑(G i) ↪[L] ↑↑(G j) := DirectedSystem.natLERec fun n ↦ Nonempty.some ⋯
N : Bundled L.Structure
KN : N ∈ K
this : (Quotient.mk' N).out ≈ N
n : ℕ
e : ↑(F n).out ≃[L] ↑N
⊢ N ∈ ⋃ i, L.age ↑↑(G i)
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: α β : Type w'
inst✝¹¹ : LinearOrder α
inst✝¹⁰ : LinearOrder β
inst✝⁹ : Countable α
inst✝⁸ : DenselyOrdered α
inst✝⁷ : NoMinOrder α
inst✝⁶ : NoMaxOrder α
inst✝⁵ : Nonempty α
inst✝⁴ : Countable β
inst✝³ : DenselyOrdered β
inst✝² : NoMinOrder β
inst✝¹ : NoMaxOrder β
inst✝ : Nonempty β
⊢ Nonempty (α ≃o β)

Tactic:
let := orderStructure α
  let := orderStructure β
  let := StrongHomClass.toOrderIsoClass Language.order α β (α ≃[Language.order] β)
  exact ⟨(IsFraisseLimit.nonempty_equiv (isFraisseLimit_of_countable_nonempty_dlo α)
    (isFraisseLimit_of_countable_nonempty_dlo β)).some⟩

Goal state after:
Module: Mathlib.ModelTheory.Topology.Types

Goal state before:
pp: case inl
L : Language
T : L.Theory
α : Type u_1
p q : T.CompleteType α
φ : L[[α]].Sentence
hφ : φ ∉ p ↔ φ ∈ q
h : φ ∈ p
⊢ ¬φ ∉ p

Tactic:
not_not

Goal state after:
case inl
L : Language
T : L.Theory
α : Type u_1
p q : T.CompleteType α
φ : L[[α]].Sentence
hφ : φ ∉ p ↔ φ ∈ q
h : φ ∈ p
⊢ φ ∈ p
Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt

Goal state before:
pp: case refine_2
n p k : ℕ
⊢ Nat.Prime p → ∑ i ∈ (p ^ k).divisors, Λ i = Real.log ↑(p ^ k)

Tactic:
hp

Goal state after:
case refine_2
n p k : ℕ
hp : Nat.Prime p
⊢ ∑ i ∈ (p ^ k).divisors, Λ i = Real.log ↑(p ^ k)
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: case inl.inl
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn g (Set.Icc a b) volume
hab : a ≤ b
hb : ⌊a⌋₊ = ⌊b⌋₊
⊢ IntegrableOn (fun t ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) (Set.Icc a b) volume

Tactic:
have : ∀ᵐ t, t ∈ Set.Icc a b → ∑ k ∈ Icc m ⌊a⌋₊, c k = ∑ k ∈ Icc m ⌊t⌋₊, c k := by
        filter_upwards [sumlocc c ⌊a⌋₊] with t ht₁ ht₂
        rw [ht₁ ⟨(Nat.floor_le ha).trans ht₂.1, hb ▸ ht₂.2.trans (Nat.lt_floor_add_one b).le⟩]

Goal state after:
case inl.inl
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn g (Set.Icc a b) volume
hab : a ≤ b
hb : ⌊a⌋₊ = ⌊b⌋₊
this : ∀ᵐ (t : ℝ), t ∈ Set.Icc a b → ∑ k ∈ Icc m ⌊a⌋₊, c k = ∑ k ∈ Icc m ⌊t⌋₊, c k
⊢ IntegrableOn (fun t ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) (Set.Icc a b) volume
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
ha : 0 ≤ a
hab : a ≤ b
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc a b) volume
aux1 : ↑⌊a⌋₊ ≤ a
aux2 : b ≤ ↑⌊b⌋₊ + 1
hb : ⌊a⌋₊ < ⌊b⌋₊
aux3 : a ≤ ↑⌊a⌋₊ + 1
aux4 : ↑⌊a⌋₊ + 1 ≤ b
aux5 : ↑⌊b⌋₊ ≤ b
⊢ ∑ k ∈ Ioc ⌊a⌋₊ ⌊b⌋₊, f ↑k * c k =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f a * ∑ k ∈ Icc 0 ⌊a⌋₊, c k - ∫ (x : ℝ) in a..b, deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k

Tactic:
have aux6 : a ≤ ⌊b⌋₊ := Nat.floor_lt ha |>.mp hb |>.le

Goal state after:
case inr
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
ha : 0 ≤ a
hab : a ≤ b
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc a b) volume
aux1 : ↑⌊a⌋₊ ≤ a
aux2 : b ≤ ↑⌊b⌋₊ + 1
hb : ⌊a⌋₊ < ⌊b⌋₊
aux3 : a ≤ ↑⌊a⌋₊ + 1
aux4 : ↑⌊a⌋₊ + 1 ≤ b
aux5 : ↑⌊b⌋₊ ≤ b
aux6 : a ≤ ↑⌊b⌋₊
⊢ ∑ k ∈ Ioc ⌊a⌋₊ ⌊b⌋₊, f ↑k * c k =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f a * ∑ k ∈ Icc 0 ⌊a⌋₊, c k - ∫ (x : ℝ) in a..b, deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k
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 : (coeff (n - single i 1)) ((pderiv R i) f) = (coeff (n - single i 1)) ((pderiv R i) g)
⊢ (coeff n) f = (coeff n) g

Tactic:
rwa [coeff_pderiv, coeff_pderiv, tsub_add_cancel_of_le this, coe_tsub, Pi.sub_apply,
    single_eq_same, Nat.cast_sub (Nat.one_le_iff_ne_zero.mpr hi), Nat.cast_one, sub_add_cancel,
    mul_comm, ← nsmul_eq_mul, mul_comm, ← nsmul_eq_mul, smul_right_inj hi] at e

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.Exp

Goal state before:
pp: case succ
A : Type u_3
inst✝² : CommRing A
inst✝¹ : Algebra ℚ A
inst✝ : IsAddTorsionFree A
f : A⟦X⟧
hd : (d⁄dX A) f = f
hc : constantCoeff f = 1
n : ℕ
ih : (coeff n) f = (coeff n) (exp A)
eq1 : (coeff (n + 1)) f * (↑n + 1) = (coeff n) (exp A)
eq2 : (coeff (n + 1)) (exp A) * (↑n + 1) = (coeff n) (exp A)
h : (coeff (n + 1)) f * (↑n + 1) = (coeff (n + 1)) (exp A) * (↑n + 1)
⊢ (coeff (n + 1)) f = (coeff (n + 1)) (exp A)

Tactic:
← Nat.cast_succ,

Goal state after:
case succ
A : Type u_3
inst✝² : CommRing A
inst✝¹ : Algebra ℚ A
inst✝ : IsAddTorsionFree A
f : A⟦X⟧
hd : (d⁄dX A) f = f
hc : constantCoeff f = 1
n : ℕ
ih : (coeff n) f = (coeff n) (exp A)
eq1 : (coeff (n + 1)) f * (↑n + 1) = (coeff n) (exp A)
eq2 : (coeff (n + 1)) (exp A) * (↑n + 1) = (coeff n) (exp A)
h : (coeff (n + 1)) f * ↑n.succ = (coeff (n + 1)) (exp A) * ↑n.succ
⊢ (coeff (n + 1)) f = (coeff (n + 1)) (exp A)
Module: Mathlib.RingTheory.PowerSeries.Exp

Goal state before:
pp: A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ exp A * evalNegHom (exp A) = 1

Tactic:
convert! exp_mul_exp_eq_exp_add (1 : A) (-1)

Goal state after:
case e'_2.e'_5
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ exp A = (rescale 1) (exp A)

case e'_3
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ 1 = (rescale (1 + -1)) (exp A)
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: n : ℕ
⊢ eval 0 (bernoulli n) = _root_.bernoulli n

Tactic:
← coeff_zero_eq_eval_zero,

Goal state after:
n : ℕ
⊢ (bernoulli n).coeff 0 = _root_.bernoulli n
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: n : ℕ
⊢ ∑ x ∈ range (n + 1 - 0),
      (∑ i ∈ range (n + 1 - x), ↑((n + 1 - x).choose i) * _root_.bernoulli i) • (monomial x) ↑((n + 1).choose x) =
    (monomial n) ↑n + (monomial n) 1

Tactic:
Nat.sub_zero

Goal state after:
n : ℕ
⊢ ∑ x ∈ range (n + 1),
      (∑ i ∈ range (n + 1 - x), ↑((n + 1 - x).choose i) * _root_.bernoulli i) • (monomial x) ↑((n + 1).choose x) =
    (monomial n) ↑n + (monomial n) 1