mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.ModelTheory.Equivalence

Goal state before:
pp: L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α (n + 1)
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
⊢ (∃' φ ⇔ ∼(∀' ∼φ)).Realize v xs

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
⊢ N.FG ↔ ∃ n s, (closure L).toFun (range s) = N

Tactic:
rw [fg_def]

Goal state after:
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
⊢ (∃ S, S.Finite ∧ (closure L).toFun S = N) ↔ ∃ n s, (closure L).toFun (range s) = N
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
t : Finset N
h : (closure L).toFun ↑t = Substructure.map f.toHom s
⊢ s.FG

Tactic:
rw [fg_def]

Goal state after:
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
t : Finset N
h : (closure L).toFun ↑t = Substructure.map f.toHom s
⊢ ∃ S, S.Finite ∧ (closure L).toFun S = s
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_1
inst✝ : Finite ι
s : Set (ι → ℕ)
hs : IsSlice s
h : ∀ (a : ι → ℕ) (t : Finset ι), (∀ x ∈ s, ∀ i ∉ t, x i = a i) → IsSemilinearSet s
this : Fintype ι
⊢ ∀ x ∈ s, ∀ i ∉ Finset.univ, x i = 0 i

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Complexity

Goal state before:
pp: case ex
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
n : ℕ
inst✝ : Nonempty M
φ : L.BoundedFormula α n
v : α → M
n✝ : ℕ
φ✝ : L.BoundedFormula α (n✝ + 1)
h✝ : φ✝.IsPrenex
ih :
  ∀ {xs : Fin (n✝ + 1) → M} {ψ : L.BoundedFormula α (n✝ + 1)},
    ψ.IsPrenex → ((φ✝.toPrenexImp ψ).Realize v xs ↔ (φ✝ ⟹ ψ).Realize v xs)
xs : Fin n✝ → M
ψ : L.BoundedFormula α n✝
hψ : ψ.IsPrenex
⊢ (∀ (a : M), (φ✝ ⟹ liftAt 1 n✝ ψ).Realize v (snoc xs a)) ↔ (∃' φ✝ ⟹ ψ).Realize v xs

Tactic:
simp

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
δ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, g x ∂[B; μ.restrict s]‖ₑ =
    ∑ i ∈ g.range.sigma P, ‖∫ᵛ (x : X) in i.snd, g x - f x + f x ∂[B; μ.restrict s]‖ₑ

Tactic:
simp

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

Goal state before:
pp: case empty
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : AddMonoid.FG M
S : Set (Set M)
hS' : ∀ s ∈ ∅, IsSemilinearSet s
⊢ IsSemilinearSet (⋂₀ ∅)

Tactic:
simp

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

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

Tactic:
simp

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 g : M ≃ₚ[L] N
h : f ≤ g
⊢ g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion ⋯)) = f.cod.subtype.comp f.toEquiv.toEmbedding

Tactic:
let ⟨_, eq⟩ := h; exact eq

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 g : M ≃ₚ[L] N
h : f ≤ g
x✝ : ↥f.dom
⊢ (f.cod.subtype.comp f.toEquiv.toEmbedding) x✝ = (g.cod.subtype.comp ((inclusion ⋯).comp f.toEquiv.toEmbedding)) x✝

Tactic:
simp

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

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : LinearIndepOn ℕ id s
t : Finset (ι → ℕ)
f : (ι → ℕ) → ℤ
ht : ↑t ⊆ s
⊢ (∀ i ∉ t, f i = 0) → ∑ i ∈ t, f i • toRatVec i = 0 → ∀ i ∈ t, f i = 0

Tactic:
hf

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : LinearIndepOn ℕ id s
t : Finset (ι → ℕ)
f : (ι → ℕ) → ℤ
ht : ↑t ⊆ s
hf : ∀ i ∉ t, f i = 0
⊢ ∑ i ∈ t, f i • toRatVec i = 0 → ∀ i ∈ t, f i = 0
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 g : M ≃ₚ[L] N
h : f ≤ g
x : ↥f.dom
⊢ (f.cod.subtype.comp f.toEquiv.toEmbedding) x = g.cod.subtype ((inclusion ⋯) (f.toEquiv x))

Tactic:
simp

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 g h : M ≃ₚ[L] N
le_fg : f.dom ≤ g.dom
eq_fg : g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion le_fg)) = f.cod.subtype.comp f.toEquiv.toEmbedding
le_gh : g.dom ≤ h.dom
eq_gh : h.cod.subtype.comp (h.toEquiv.toEmbedding.comp (inclusion le_gh)) = g.cod.subtype.comp g.toEquiv.toEmbedding
x✝ : ↥f.dom
⊢ (h.cod.subtype.comp (h.toEquiv.toEmbedding.comp (inclusion ⋯))) x✝ =
    ((h.cod.subtype.comp (h.toEquiv.toEmbedding.comp (inclusion le_gh))).comp (inclusion le_fg)) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: L : Language
ι : Type v
inst✝⁴ : Preorder ι
G : ι → Type w
inst✝³ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝² : IsDirectedOrder ι
inst✝¹ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝ : Nonempty ι
z : DirectLimit G f
⊢ (of L ι G f (Quotient.out z).fst) (Quotient.out z).snd = z

Tactic:
simp

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

Goal state before:
pp: case zero
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x y : ι → ℕ
i : ↑hs.basisSet
t : Set (ι → ℕ)
ht : t ⊆ hs.basisSet
hi : ↑i ∉ t
⊢ (hs.basis.repr (toRatVec 0)) i = 0

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: L : Language
ι : Type v
inst✝⁵ : Preorder ι
G : ι → Type w
inst✝⁴ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝³ : IsDirectedOrder ι
inst✝² : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝¹ : Nonempty ι
P : Type u₁
inst✝ : L.Structure P
g : (i : ι) → G i ↪[L] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x
i : ι
x : G i
⊢ (lift L ι G f g Hg) ⟦Structure.Sigma.mk f i x⟧ = (g i) x

Tactic:
change (lift L ι G f g Hg).toFun ⟦.mk f i x⟧ = _
  simp only [lift, Quotient.lift_mk]

Goal state after:
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: L : Language
ι : Type v
inst✝⁵ : Preorder ι
G : ι → Type w
inst✝⁴ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝³ : IsDirectedOrder ι
inst✝² : DirectedSystem G fun i j h ↦ ⇑(f i j h)
inst✝¹ : Nonempty ι
P : Type u₁
inst✝ : L.Structure P
g : (i : ι) → G i ↪[L] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x
i : ι
x : G i
⊢ (lift L ι G f g Hg) ((of L ι G f i) x) = (g i) x

Tactic:
simp

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
⊢ L.IsExtensionPair M N ↔
    ∀ (S : L.Substructure M), S.FG → ∀ (f : ↥S ↪[L] N) (m : M), ∃ g, f = g.comp (Substructure.inclusion ⋯)

Tactic:
by
  refine ⟨fun h S S_FG f m => ?_, fun h ⟨f, f_FG⟩ m => ?_⟩
  · obtain ⟨⟨f', hf'⟩, mf', ff'1, ff'2⟩ := h ⟨⟨S, _, f.equivRange⟩, S_FG⟩ m
    refine ⟨f'.toEmbedding.comp (Substructure.inclusion ?_), ?_⟩
    · simp only [sup_le_iff, ff'1, closure_le, singleton_subset_iff, SetLike.mem_coe, mf',
        and_self]
    · 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]
  · obtain ⟨f', eq_f'⟩ := h f.dom f_FG f.toEmbedding m
    refine ⟨⟨⟨closure L {m} ⊔ f.dom, f'.toHom.range, f'.equivRange⟩,
      (fg_closure_singleton _).sup f_FG⟩,
      subset_closure.trans (le_sup_left : (closure L) {m} ≤ _) (mem_singleton m),
      ⟨le_sup_right, Embedding.ext (fun _ => ?_)⟩⟩
    rw [PartialEquiv.toEmbedding] at eq_f'
    simp only [Embedding.comp_apply, Substructure.coe_inclusion, Equiv.coe_toEmbedding, coe_subtype,
      Embedding.equivRange_apply, eq_f']

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 : ι → ℕ
hx : x ∈ hs.fundamentalDomain
⊢ toRatVec hs.base + (toRatVec x - toRatVec hs.base) = toRatVec x

Tactic:
simp

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

Goal state before:
pp: case pos
ι : 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)
i : ↑hs.basisSet
a✝ : i ∈ Finset.univ
hi : ↑i ∈ hs.periods
⊢ (hs.floor x i).toNat • ↑i = (hs.floor x i).toNat • ↑i

Tactic:
simp

Goal state after:
Module: Mathlib.Order.CountableDenseLinearOrder

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : Finset (α × β)
hf : ∀ p ∈ f, ∀ q ∈ f, cmp p.1 q.1 = cmp p.2 q.2
p : β × α
hp : p ∈ Finset.image (⇑(Equiv.prodComm α β)) f
q : β × α
hq : q ∈ Finset.image (⇑(Equiv.prodComm α β)) f
⊢ (Equiv.prodComm α β).symm q ∈ f

Tactic:
rw [← Finset.mem_coe, Finset.coe_image, Equiv.image_eq_preimage_symm] at hq

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : Finset (α × β)
hf : ∀ p ∈ f, ∀ q ∈ f, cmp p.1 q.1 = cmp p.2 q.2
p : β × α
hp : p ∈ Finset.image (⇑(Equiv.prodComm α β)) f
q : β × α
hq : q ∈ ⇑(Equiv.prodComm α β).symm ⁻¹' ↑f
⊢ (Equiv.prodComm α β).symm q ∈ f
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
h : L.IsUltrahomogeneous M
N P Q : Bundled L.Structure
NP : ↑N ↪[L] ↑P
NQ : ↑N ↪[L] ↑Q
Nfg : Structure.FG L ↑N
Pfg : Structure.FG L ↑P
PM : ↑P ↪[L] M
Qfg : Structure.FG L ↑Q
QM : ↑Q ↪[L] M
g : M ≃[L] M
hg : (QM.comp NQ).comp (PM.comp NP).equivRange.symm.toEmbedding = g.toEmbedding.comp (PM.comp NP).toHom.range.subtype
s : L.Substructure M := (g.toHom.comp PM.toHom).range ⊔ QM.toHom.range
n : ↑N
hgn : QM (NQ n) = g (PM (NP n))
⊢ (g.toEmbedding.comp PM) (NP n) = g (PM (NP n))

Tactic:
simp

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₁' s₂' : Set ↥P
hs₁' : IsSemilinearSet s₁'
hs₁ : IsSemilinearSet (Subtype.val '' s₁')
hs₂' : IsSemilinearSet s₂'
hs₂ : IsSemilinearSet (Subtype.val '' s₂')
n : ℕ
f : (Fin n → ℕ) →+ ↥P
hf : Function.Surjective ⇑f
⊢ IsSemilinearSet (⇑f '' ⇑f ⁻¹' (s₁' \ s₂'))

Tactic:
preimage_sdiff

Goal state after:
M : Type u_1
inst✝ : AddCommMonoid M
P : AddSubmonoid M
s₁' s₂' : Set ↥P
hs₁' : IsSemilinearSet s₁'
hs₁ : IsSemilinearSet (Subtype.val '' s₁')
hs₂' : IsSemilinearSet s₂'
hs₂ : IsSemilinearSet (Subtype.val '' s₂')
n : ℕ
f : (Fin n → ℕ) →+ ↥P
hf : Function.Surjective ⇑f
⊢ IsSemilinearSet (⇑f '' (⇑f ⁻¹' s₁' \ ⇑f ⁻¹' s₂'))
Module: Mathlib.ModelTheory.Types

Goal state before:
pp: L : Language
T : L.Theory
α : Type w
φ : L[[α]].Sentence
⊢ {p | Formula.not φ ∈ p} = ∅ ↔ {p | {Formula.not φ} ⊆ ↑p} = ∅

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: M : Type u_1
inst✝² : Countable M
inst✝¹ : Infinite M
inst✝ : Language.empty.Structure M
S : Bundled Language.empty.Structure
hS : Finite ↑S
⊢ Nonempty (↑S ↪[Language.empty] M)

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Types

Goal state before:
pp: L : Language
T : L.Theory
α : Type w
⊢ {p | ∅ ⊆ ↑p} = ∅ ↔ Set.univ = ∅

Tactic:
simp

Goal state after:
Module: Mathlib.ModelTheory.Types

Goal state before:
pp: L : Language
T : L.Theory
α : Type w
M : Type w'
inst✝² : L.Structure M
inst✝¹ : Nonempty M
inst✝ : M ⊨ T
v : α → M
φ : L.Formula α
⊢ Formula.equivSentence φ ∈ T.typeOf v ↔ φ.Realize v

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
hvu : v ∣ u
hpuv : ↑p * u * v ∣ u ^ p
x : R
⊢ 0 ∈ Finset.range (p + 1)

Tactic:
simp

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

Goal state before:
pp: case zero
⊢ λ 0 ∣ φ 0

Tactic:
simp

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

Goal state before:
pp: case zero
a : ℕ
h : a ∣ 0
⊢ λ a ∣ λ 0

Tactic:
simp

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

Goal state before:
pp: n : ℕ
hn : 3 ≤ n
⊢ 2 * λ (2 ^ n) = φ (2 ^ n)

Tactic:
rw [carmichael_two_pow_of_ne_two, ← pow_succ', totient_prime_pow prime_two] <;>
  · #adaptation_note /-- After https://github.com/leanprover/lean4/pull/13593
    we need to re-enable model-based theory combination in `lia` for this to go through. -/
    lia +mbtc

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

Goal state before:
pp: ⊢ (if 0 = 0 then 0 else (-1) ^ cardFactors 0) = 0

Tactic:
simp

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

Goal state before:
pp: ⊢ Real.log ↑0 = 0

Tactic:
simp

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

Goal state before:
pp: case refine_1
n : ℕ
⊢ ∑ i ∈ divisors 0, Λ i = Real.log ↑0

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : ℕ
u v : R
hp : Nat.Prime p
hvu : v ∣ u
hpuv : ↑p * u * v ∣ u ^ p
x : R
m : ℕ
⊢ (1 + u * x) ^ p ^ 0 = 1 + ↑p ^ 0 * u * (x + v * 0)

Tactic:
simp

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

Goal state before:
pp: ⊢ Λ * ↑ζ = log

Tactic:
simp

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

Goal state before:
pp: ⊢ log * ↑μ = Λ

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: p : ℕ
hp : Nat.Prime p
m : ℕ
hm0 : m ≠ 0
hpm : m + 2 ≤ p * m
a : ℤ
ha : ¬↑p ∣ a
n : ℕ
⊢ orderOf (1 + 0 * ↑a) = p ^ 0

Tactic:
simp

Goal state after:
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: 𝕜 : 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⌋₊
t₁ t₂ : ℝ
n : ℕ
h✝ : t₁ ≤ t₂
h₁ : ↑n ≤ t₁
h₂ : t₂ ≤ ↑n + 1
h₃ : a ≤ t₁
h₄ : t₂ ≤ b
t : ℝ
h : t ∈ Set.Icc (↑n) (↑n + 1) → ∑ k ∈ Icc ?m.346 ⌊t⌋₊, c k = ∑ k ∈ Icc ?m.346 n, c k
ht : t ∈ Set.Icc (↑n) (↑n + 1)
⊢ g t * ?m.294 = g t * ∑ k ∈ Icc m ⌊t⌋₊, c k

Tactic:
by rw [h ht]

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

Goal state before:
pp: ⊢ Λ 0 ≤ Real.log ↑0

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case hfin
p : ℕ
hp : Nat.Prime p
m : ℕ
hm0 : m ≠ 0
hpm : m + 2 ≤ p * m
a : ℤ
ha : ¬↑p ∣ a
n✝ n : ℕ
this✝ : Fact (Nat.Prime p)
this : ∀ (m_1 : ℕ), ∃ y, (1 + ↑p ^ m * ↑a) ^ p ^ m_1 = 1 + ↑p ^ m_1 * ↑p ^ m * (↑a + ↑p * y)
y : ZMod (p ^ (n + 1 + m))
hy : (1 + ↑p ^ m * ↑a) ^ p ^ (n + 1) = 1 + ↑p ^ (n + 1) * ↑p ^ m * (↑a + ↑p * y)
⊢ 1 + ↑(p ^ (n + 1 + m)) * (↑a + ↑p * y) = 1

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
n : ℕ
⊢ ↑p = ↑p * ↑1

Tactic:
simp

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
f g : MvPolynomial σ R
⊢ ↑((pderiv i) (f * g)) = ↑f * ↑((pderiv i) g) + ↑g * ↑((pderiv i) f)

Tactic:
pderiv_mul,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
f g : MvPolynomial σ R
⊢ ↑((pderiv i) f * g + f * (pderiv i) g) = ↑f * ↑((pderiv i) g) + ↑g * ↑((pderiv i) f)
Module: Mathlib.RingTheory.MvPowerSeries.Derivative

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
f g : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ n i < (n + single i 1) i

Tactic:
simp

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
f g : MvPowerSeries σ R
n : σ →₀ ℕ
h₁ : n < n + single i 1
⊢ (n + single i 1) i < (n + single i 1 + single i 1) i

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case h
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
this✝¹ : Fact (Nat.Prime p)
n : ℕ
a : ZMod (p ^ (n + 1)) := 1 + ↑p
ha_def : a = 1 + ↑p
ha : IsUnit a
ha' : orderOf ha.unit = p ^ n
b : (ZMod (p ^ (n + 1)))ˣ
hc : orderOf ((unitsMap ⋯) b) = p - 1
this✝ : p - 1 ∣ orderOf b
k : ℕ := orderOf b / (p - 1)
this : orderOf (b ^ k) = p - 1
⊢ p.Coprime (Nat.succ 0)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: n : ℕ
⊢ Odd 1

Tactic:
simp

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
δ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‖ₑ + ↑δ
I4 :
  ∑ 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]‖ₑ + ↑δ
I5 : ∑ i ∈ g.range.sigma P, ‖∫ᵛ (x : X) in i.snd, f x ∂[B; μ.restrict s]‖ₑ ≤ (μ.withDensity f B).variation s
⊢ 3 ≠ 0

Tactic:
simp

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
δ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‖ₑ + ↑δ
I4 :
  ∑ 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]‖ₑ + ↑δ
I5 : ∑ i ∈ g.range.sigma P, ‖∫ᵛ (x : X) in i.snd, f x ∂[B; μ.restrict s]‖ₑ ≤ (μ.withDensity f B).variation s
⊢ 3 ≠ ∞

Tactic:
simp

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommSemiring R
f : R⟦X⟧
k : ℕ
⊢ (coeff k) ((⇑(d⁄dX R))^[0] f) = ↑((k + 1).ascFactorial 0) * (coeff (k + 0)) f

Tactic:
simp

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

Goal state before:
pp: X : Type u_1
E : Type u_2
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure X
f : X → E
hf : Integrable f μ
hE : Nontrivial E
this : IsFiniteMeasure (μ.withDensity fun x ↦ ‖f x‖ₑ)
I : VectorMeasure.Integrable (μ.withDensity fun x ↦ ‖f x‖ₑ).toSignedMeasure fun x ↦ ‖f x‖⁻¹ • f x
s : Set X
hs : MeasurableSet s
⊢ (μ.withDensityᵥ f) s =
    (withDensity (μ.withDensity fun x ↦ ‖f x‖ₑ).toSignedMeasure (fun x ↦ ‖f x‖⁻¹ • f x)
        (ContinuousLinearMap.lsmul ℝ ℝ).flip)
      s

Tactic:
withDensityᵥ_apply hf hs,

Goal state after:
X : Type u_1
E : Type u_2
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure X
f : X → E
hf : Integrable f μ
hE : Nontrivial E
this : IsFiniteMeasure (μ.withDensity fun x ↦ ‖f x‖ₑ)
I : VectorMeasure.Integrable (μ.withDensity fun x ↦ ‖f x‖ₑ).toSignedMeasure fun x ↦ ‖f x‖⁻¹ • f x
s : Set X
hs : MeasurableSet s
⊢ ∫ (x : X) in s, f x ∂μ =
    (withDensity (μ.withDensity fun x ↦ ‖f x‖ₑ).toSignedMeasure (fun x ↦ ‖f x‖⁻¹ • f x)
        (ContinuousLinearMap.lsmul ℝ ℝ).flip)
      s
Module: Mathlib.RingTheory.PowerSeries.Exp

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : Algebra ℚ A
⊢ (algebraMap ℚ A) (1 / ↑0!) = 1

Tactic:
simp

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

Goal state before:
pp: A : Type u_1
A' : Type u_2
inst✝³ : Ring A
inst✝² : Ring A'
inst✝¹ : Algebra ℚ A
inst✝ : Algebra ℚ A'
f : A →+* A'
n✝ : ℕ
⊢ (coeff n✝) ((map f) (exp A)) = (coeff n✝) (exp A')

Tactic:
simp

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

Goal state before:
pp: X : Type u_1
E : Type u_2
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure X
f : X → E
hf : Integrable f μ
hE : Nontrivial E
this : IsFiniteMeasure (μ.withDensity fun x ↦ ‖f x‖ₑ)
I : VectorMeasure.Integrable (μ.withDensity fun x ↦ ‖f x‖ₑ).toSignedMeasure fun x ↦ ‖f x‖⁻¹ • f x
s : Set X
hs : MeasurableSet s
x : X
⊢ ‖f x‖ₑ < ∞

Tactic:
simp

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

Goal state before:
pp: A : Type u_4
inst✝¹ : Ring A
inst✝ : Algebra ℚ A
⊢ IsUnit (constantCoeff (exp A))

Tactic:
simp

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

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

Tactic:
simp

Goal state after: