mathlib-initiative/mathlib-tactics huggingface dataset:
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 < δ
ρ : NNReal
ρpos : ρ > 0
hδ : ‖B‖₊ * ρ ≤ δ
⊢ ∃ g, eLpNorm (f - ⇑g) 1 (μ.transpose B).variation ≤ ↑δ ∧ MemLp (⇑g) 1 μ.variation

Tactic:
obtain ⟨g, h'g, gmem⟩ : ∃ (g : X →ₛ E), eLpNorm (f - ⇑g) 1 μ.variation < ρ
        ∧ MemLp (⇑g) 1 μ.variation :=
      (memLp_one_iff_integrable.2 hf).exists_simpleFunc_eLpNorm_sub_lt (by simp)
        (by simpa using ρpos.ne')

Goal state after:
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 < δ
ρ : NNReal
ρpos : ρ > 0
hδ : ‖B‖₊ * ρ ≤ δ
g : X →ₛ E
h'g : eLpNorm (f - ⇑g) 1 μ.variation < ↑ρ
gmem : MemLp (⇑g) 1 μ.variation
⊢ ∃ g, eLpNorm (f - ⇑g) 1 (μ.transpose B).variation ≤ ↑δ ∧ MemLp (⇑g) 1 μ.variation
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
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
⊢ ‖∫ᵛ (a : X), f a ∂[B; μ]‖ₑ ≤ ‖B‖ₑ * ∫⁻ (a : X), ‖f a‖ₑ ∂μ.variation

Tactic:
apply (enorm_setToFun_le _ (by simp)).trans

Goal state after:
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
⊢ ↑(NNReal.mk ‖B‖ ⋯) * ∫⁻ (x : X), ‖f x‖ₑ ∂μ.variation ≤ ‖B‖ₑ * ∫⁻ (a : X), ‖f a‖ₑ ∂μ.variation
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
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
β : Type u_9
inst✝ : MeasurableSpace β
φ : X → β
hφ : MeasurableEmbedding φ
f : β → E
hfm : AEStronglyMeasurable f (Measure.map φ μ.variation)
h'fm : μ.Integrable (f ∘ φ)
⊢ ∫ᵛ (y : β), f y ∂[B; μ.map φ] = ∫ᵛ (x : X), f (φ x) ∂[B; μ]

Tactic:
apply integral_map hφ.measurable hfm h'fm

Goal state after:
Module: Mathlib.ModelTheory.Equivalence

Goal state before:
pp: L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ : L.BoundedFormula α n
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
⊢ (φ ⊓ ψ ⟹ φ).Realize v xs

Tactic:
simp only [BoundedFormula.realize_imp, BoundedFormula.realize_inf]
  exact And.left

Goal state after:
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: case mk.mk
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)
i fst✝¹ : ι
snd✝¹ : G fst✝¹
hx : ⟨fst✝¹, snd✝¹⟩.fst ≤ i
fst✝ : ι
snd✝ : G fst✝
hy : ⟨fst✝, snd✝⟩.fst ≤ i
j : ι
w✝¹ : fst✝¹ ≤ j
w✝ : fst✝ ≤ j
h✝ : (f fst✝¹ j w✝¹) snd✝¹ = (f fst✝ j w✝) snd✝
k : ι
ik : i ≤ k
jk : j ≤ k
h : (f j k jk) ((f fst✝¹ j w✝¹) snd✝¹) = (f j k jk) ((f fst✝ j w✝) snd✝)
⊢ (f i k ik) ((f ⟨fst✝¹, snd✝¹⟩.fst i hx) ⟨fst✝¹, snd✝¹⟩.snd) = (f i k ik) ((f ⟨fst✝, snd✝⟩.fst i hy) ⟨fst✝, snd✝⟩.snd)

Tactic:
DirectedSystem.map_map,

Goal state after:
case mk.mk
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)
i fst✝¹ : ι
snd✝¹ : G fst✝¹
hx : ⟨fst✝¹, snd✝¹⟩.fst ≤ i
fst✝ : ι
snd✝ : G fst✝
hy : ⟨fst✝, snd✝⟩.fst ≤ i
j : ι
w✝¹ : fst✝¹ ≤ j
w✝ : fst✝ ≤ j
h✝ : (f fst✝¹ j w✝¹) snd✝¹ = (f fst✝ j w✝) snd✝
k : ι
ik : i ≤ k
jk : j ≤ k
h : (f fst✝¹ k ⋯) snd✝¹ = (f j k jk) ((f fst✝ j w✝) snd✝)
⊢ (f ⟨fst✝¹, snd✝¹⟩.fst k ⋯) ⟨fst✝¹, snd✝¹⟩.snd = (f i k ik) ((f ⟨fst✝, snd✝⟩.fst i hy) ⟨fst✝, snd✝⟩.snd)
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)
n : ℕ
R : L.Relations n
x : Fin n → Σˣ f
i j : ι
hi : i ∈ upperBounds (range (Sigma.fst ∘ x))
hj : j ∈ upperBounds (range (Sigma.fst ∘ x))
k : ι
ik : i ≤ k
jk : j ≤ k
⊢ RelMap R (unify f x k ⋯) = RelMap R (unify f x j hj)

Tactic:
← (f j k jk).map_rel,

Goal state after:
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)
n : ℕ
R : L.Relations n
x : Fin n → Σˣ f
i j : ι
hi : i ∈ upperBounds (range (Sigma.fst ∘ x))
hj : j ∈ upperBounds (range (Sigma.fst ∘ x))
k : ι
ik : i ≤ k
jk : j ≤ k
⊢ RelMap R (unify f x k ⋯) = RelMap R (⇑(f j k jk) ∘ unify f x j hj)
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

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

Tactic:
induction S, hS using Finite.induction_on with

Goal state after:
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: case mpr
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
dom_le_dom : f.dom ≤ g.dom
le_cod : f.cod ≤ g.cod
h_eq : ∀ (x : ↥f.dom), (inclusion le_cod) (f.toEquiv x) = g.toEquiv ((inclusion dom_le_dom) x)
⊢ f ≤ g

Tactic:
rw [le_def]

Goal state after:
case mpr
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
dom_le_dom : f.dom ≤ g.dom
le_cod : f.cod ≤ g.cod
h_eq : ∀ (x : ↥f.dom), (inclusion le_cod) (f.toEquiv x) = g.toEquiv ((inclusion dom_le_dom) x)
⊢ ∃ (h : f.dom ≤ g.dom),
    g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion h)) = f.cod.subtype.comp f.toEquiv.toEmbedding
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: case refl.le_fg
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : M ≃ₚ[L] N
cod_f : L.Substructure N
equiv_f : ↥g.1 ≃[L] ↥cod_f
h :
  ∀ (x : M) (h : x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom),
    { dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod.subtype
        ({ dom := g.1, cod := cod_f, toEquiv := equiv_f }.toEquiv ⟨x, h⟩) =
      g.cod.subtype (g.toEquiv ⟨x, ⋯⟩)
⊢ { dom := g.1, cod := cod_f, toEquiv := equiv_f } ≤ g

Tactic:
rw [le_def]

Goal state after:
case refl.le_fg
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : M ≃ₚ[L] N
cod_f : L.Substructure N
equiv_f : ↥g.1 ≃[L] ↥cod_f
h :
  ∀ (x : M) (h : x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom),
    { dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod.subtype
        ({ dom := g.1, cod := cod_f, toEquiv := equiv_f }.toEquiv ⟨x, h⟩) =
      g.cod.subtype (g.toEquiv ⟨x, ⋯⟩)
⊢ ∃ (h : { dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom ≤ g.dom),
    g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion h)) =
      { dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod.subtype.comp
        { dom := g.1, cod := cod_f, toEquiv := equiv_f }.toEquiv.toEmbedding
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: case refl.le_gf
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : M ≃ₚ[L] N
cod_f : L.Substructure N
equiv_f : ↥g.1 ≃[L] ↥cod_f
h :
  ∀ (x : M) (h : x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom),
    { dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod.subtype
        ({ dom := g.1, cod := cod_f, toEquiv := equiv_f }.toEquiv ⟨x, h⟩) =
      g.cod.subtype (g.toEquiv ⟨x, ⋯⟩)
⊢ g ≤ { dom := g.1, cod := cod_f, toEquiv := equiv_f }

Tactic:
rw [le_def]

Goal state after:
case refl.le_gf
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : M ≃ₚ[L] N
cod_f : L.Substructure N
equiv_f : ↥g.1 ≃[L] ↥cod_f
h :
  ∀ (x : M) (h : x ∈ { dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom),
    { dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod.subtype
        ({ dom := g.1, cod := cod_f, toEquiv := equiv_f }.toEquiv ⟨x, h⟩) =
      g.cod.subtype (g.toEquiv ⟨x, ⋯⟩)
⊢ ∃ (h : g.dom ≤ { dom := g.1, cod := cod_f, toEquiv := equiv_f }.dom),
    { dom := g.1, cod := cod_f, toEquiv := equiv_f }.cod.subtype.comp
        ({ dom := g.1, cod := cod_f, toEquiv := equiv_f }.toEquiv.toEmbedding.comp (inclusion h)) =
      g.cod.subtype.comp g.toEquiv.toEmbedding
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case right
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
i : ↑hs.basisSet
⊢ (hs.basis.repr (toRatVec (hs.fract x) - toRatVec hs.base)) i < 1

Tactic:
· rw [hs.toRatVec_fract_eq, add_sub_cancel_left]
    simp [← hs.basis_apply, Finsupp.single_apply, Int.fract_lt_one]

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

Goal state before:
pp: case e'_3.a
ι : 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
⊢ 0 = (-hs.floor x i).toNat • ↑i

Tactic:
· simp [fun i => Int.toNat_eq_zero.2 (neg_nonpos.2 (hx₂ i).1)]

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 u : ι → ℕ
hu : u ∈ hs.fundamentalDomain
hu' : u ∉ {hs.base}
y : ι → ℕ
hy : y ∈ closure hs.basisSet
y' : ι → ℕ
hy' : y' ∈ closure hs.basisSet
heq : hs.fract x = u
⊢ hs.fract x ≠ hs.base

Tactic:
rwa [heq]

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 p ∈ f

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

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 ∈ ⇑(Equiv.prodComm α β).symm ⁻¹' ↑f
q : β × α
hq : q ∈ Finset.image (⇑(Equiv.prodComm α β)) f
⊢ (Equiv.prodComm α β).symm p ∈ f
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: L : Language
α : Type w
M : Type w'
n : ℕ
inst✝¹ : L.IsOrdered
inst✝ : L.Structure M
h : M ⊨ L.preorderTheory
⊢ leSymb.reflexive ∈ L.preorderTheory

Tactic:
by simp [preorderTheory]

Goal state after:
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: L : Language
α : Type w
M : Type w'
n : ℕ
inst✝¹ : L.IsOrdered
inst✝ : L.Structure M
h : M ⊨ L.preorderTheory
⊢ leSymb.transitive ∈ L.preorderTheory

Tactic:
by simp [preorderTheory]

Goal state after:
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: L : Language
K : Set (Bundled L.Structure)
M : Type w
inst✝⁴ : L.Structure M
N : Type w
inst✝³ : L.Structure N
inst✝² : Countable ((l : ℕ) × L.Functions l)
inst✝¹ : Countable M
inst✝ : Countable N
hM : IsFraisseLimit K M
hN : IsFraisseLimit K N
⊢ L.IsExtensionPair M N

Tactic:
intro ⟨f, f_FG⟩ m
  let S := f.dom ⊔ closure L {m}
  have S_FG : S.FG := f_FG.sup (Substructure.fg_closure_singleton _)
  have S_in_age_N : ⟨S, inferInstance⟩ ∈ L.age N := by
    rw [hN.age, ← hM.age]
    exact ⟨(fg_iff_structure_fg S).1 S_FG, ⟨subtype _⟩⟩
  have nonempty_S_N : Nonempty (S ↪[L] N) := S_in_age_N.2
  let ⟨g, g_eq⟩ := hN.ultrahomogeneous.extend_embedding (f.dom.fg_iff_structure_fg.1 f_FG)
    ((subtype f.cod).comp f.toEquiv.toEmbedding) (inclusion (le_sup_left : _ ≤ S))
  refine ⟨⟨⟨S, g.toHom.range, g.equivRange⟩, S_FG⟩,
    subset_closure.trans (le_sup_right : _ ≤ S) (mem_singleton m), ⟨le_sup_left, ?_⟩⟩
  ext
  simp [S, g_eq]

Goal state after:
Module: Mathlib.Topology.Baire.LocallyCompactRegular

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
s : Set X
inst✝¹ : R1Space X
inst✝ : LocallyCompactSpace X
⊢ BaireSpace X

Tactic:
by
  constructor
  intro f ho hd
  /- To prove that an intersection of open dense subsets is dense, prove that its intersection
    with any open neighbourhood `U` is dense. Define recursively a decreasing sequence `K` of
    compact neighbourhoods: start with some compact neighbourhood inside `U`, then at each step,
    take its interior, intersect with `f n`, then choose a compact neighbourhood inside the
    intersection. -/
  rw [dense_iff_inter_open]
  intro U U_open U_nonempty
  -- Choose an antitone sequence of positive compacts such that `closure (K 0) ⊆ U`
  -- and `closure (K (n + 1)) ⊆ f n` for all `n`
  obtain ⟨K, hK_anti, hKf, hKU⟩ : ∃ K : ℕ → PositiveCompacts X,
      (∀ n, K (n + 1) ≤ K n) ∧ (∀ n, closure ↑(K (n + 1)) ⊆ f n) ∧ closure ↑(K 0) ⊆ U := by
    rcases U_open.exists_positiveCompacts_closure_subset U_nonempty with ⟨K₀, hK₀⟩
    have : ∀ (n) (K : PositiveCompacts X),
        ∃ K' : PositiveCompacts X, closure ↑K' ⊆ f n ∩ interior K := by
      refine fun n K ↦ ((ho n).inter isOpen_interior).exists_positiveCompacts_closure_subset ?_
      rw [inter_comm]
      exact (hd n).inter_open_nonempty _ isOpen_interior K.interior_nonempty
    choose K_next hK_next using this
    -- The next two lines are faster than a single `refine`.
    use Nat.rec K₀ K_next
    refine ⟨fun n ↦ ?_, fun n ↦ (hK_next n _).trans inter_subset_left, hK₀⟩
    exact subset_closure.trans <| (hK_next _ _).trans <|
      inter_subset_right.trans interior_subset
  -- Prove that `⋂ n : ℕ, closure (K n)` is inside `U ∩ ⋂ n : ℕ, f n`.
  have hK_subset : (⋂ n, closure (K n) : Set X) ⊆ U ∩ ⋂ n, f n := fun x hx ↦ by
    simp only [mem_iInter, mem_inter_iff] at hx ⊢
    exact ⟨hKU <| hx 0, fun n ↦ hKf n <| hx (n + 1)⟩
  /- Prove that `⋂ n : ℕ, closure (K n)` is not empty, as an intersection of a decreasing sequence
    of nonempty compact closed subsets. -/
  have hK_nonempty : (⋂ n, closure (K n) : Set X).Nonempty :=
    IsCompact.nonempty_iInter_of_sequence_nonempty_isCompact_isClosed _
      (fun n => closure_mono <| hK_anti n) (fun n => (K n).nonempty.closure)
      (K 0).isCompact.closure fun n => isClosed_closure
  exact hK_nonempty.mono hK_subset

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

Goal state before:
pp: case refine_2
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
a✝ : ↑F ≤ Filter.principal univ
⊢ IsMaximal {φ | T.typesWith φ ∈ F}

Tactic:
Theory.IsMaximal,

Goal state after:
case refine_2
L : Language
T : L.Theory
α : Type u_1
F : Ultrafilter (T.CompleteType α)
a✝ : ↑F ≤ Filter.principal univ
⊢ IsSatisfiable {φ | T.typesWith φ ∈ F} ∧
    ∀ (φ : L[[α]].Sentence), φ ∈ {φ | T.typesWith φ ∈ F} ∨ Formula.not φ ∈ {φ | T.typesWith φ ∈ F}
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: ⊢ Nat.card (ZMod 4)ˣ = 2

Tactic:
simp only [Nat.card_eq_fintype_card, card_units_eq_totient]

Goal state after:
⊢ φ 4 = 2
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: p q r : ℕ+
S : List ℕ+ := {p, q, r}.sort fun a b ↦ a ≤ b
H : 1 < sumInv ↑S
hS : S.SortedLE
hpqr : {p, q, r} = ↑S
⊢ (∃ q r, A' q r = ↑S) ∨ (∃ r, D' r = ↑S) ∨ E' 3 = ↑S ∨ E' 4 = ↑S ∨ E' 5 = ↑S

Tactic:
apply admissible_of_one_lt_sumInv_aux hS _ H

Goal state after:
p q r : ℕ+
S : List ℕ+ := ⋯
H : 1 < sumInv ↑S
hS : S.SortedLE
hpqr : {p, q, r} = ↑S
⊢ S.length = 3
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
x a : R
ha : u = v * a
b : R
hb : u ^ p = ↑p * u * v * b
i : ℕ
hi : ¬i = p ∧ ¬i = 1 ∧ ¬i = 0 ∧ i < p + 1
hi' : 2 ≤ i
⊢ (u * x) ^ (2 + (i - 2)) * ↑(p.choose i) = u ^ 2 * x ^ 2 * (u * x) ^ (i - 2) * ↑(p.choose i)

Tactic:
ring_nf

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
x a : R
ha : u = v * a
b : R
hb : u ^ p = ↑p * u * v * b
i : ℕ
hi : ¬i = p ∧ ¬i = 1 ∧ ¬i = 0 ∧ i < p + 1
hi' : 2 ≤ i
⊢ u ^ 2 * x ^ 2 * (u * x) ^ (i - 2) * (↑p * ↑(p.choose i / p)) =
    u ^ 2 * x ^ 2 * (u * x) ^ (i - 2) * ↑p * ↑(p.choose i / p)

Tactic:
ring_nf

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
x a : R
ha : u = v * a
b : R
hb : u ^ p = ↑p * u * v * b
⊢ ↑p * u * v * b * x ^ p = ↑p * u * (v * (b * x ^ p))

Tactic:
ring_nf

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

Goal state before:
pp: case refine_2
n p k : ℕ
hp : Nat.Prime p
⊢ ∑ x ∈ range (k + 1), Λ (p ^ x) = Real.log ↑(p ^ k)

Tactic:
cast_pow,

Goal state after:
case refine_2
n p k : ℕ
hp : Nat.Prime p
⊢ ∑ x ∈ range (k + 1), Λ (p ^ x) = Real.log (↑p ^ k)
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: n : ℕ
⊢ n.primesLE = filter Prime (Ioc 1 n)

Tactic:
by
  ext p
  simp +contextual [primesLE_eq_filter_range, Nat.Prime.one_lt]

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: n x✝ : ℕ
a✝ : x✝ ∈ range (n + 1 - 0)
| ∑ x ∈ range (n + 1 - x✝), (monomial x✝) (↑((n + 1).choose (x✝ + x)) * ↑((x✝ + x).choose x✝) * _root_.bernoulli x)

Tactic:
apply_congr
      · skip
      · rw [← Nat.cast_mul, choose_mul (le_add_right _ _), Nat.cast_mul, add_tsub_cancel_left,
          mul_assoc, mul_comm, ← smul_eq_mul, ← smul_monomial]

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: ⊢ bernoulli' 4 = -1 / 30

Tactic:
have : Nat.choose 4 2 = 6 := by decide

Goal state after:
this : Nat.choose 4 2 = 6
⊢ bernoulli' 4 = -1 / 30
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
this : ∑ p ∈ antidiagonal n, bernoulli' p.1 / ↑p.1! * ((↑p.2 + 1) * ↑p.2!)⁻¹ = (↑n !)⁻¹
⊢ (coeff (n + 1, 0).1) (PowerSeries.mk fun n ↦ (algebraMap ℚ A) (bernoulli' n / ↑n !)) *
        (coeff (n + 1, 0).2) (exp A - 1) +
      ∑ p ∈ antidiagonal n,
        (coeff (p.1, p.2 + 1).1) (PowerSeries.mk fun n ↦ (algebraMap ℚ A) (bernoulli' n / ↑n !)) *
          (coeff (p.1, p.2 + 1).2) (exp A - 1) =
    (coeff (n + 1)) (exp A * X)

Tactic:
by
    simpa [map_sum, Nat.factorial] using congr_arg (algebraMap ℚ A) this

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: case succ
n i : ℕ
⊢ ((bernoulli (n + 1)).comp (-X)).coeff i = ((-1) ^ (n + 1) • (bernoulli (n + 1) + (n + 1) • X ^ (n + 1 - 1))).coeff i

Tactic:
← neg_one_mul,

Goal state after:
case succ
n i : ℕ
⊢ ((bernoulli (n + 1)).comp (-1 * X)).coeff i =
    ((-1) ^ (n + 1) • (bernoulli (n + 1) + (n + 1) • X ^ (n + 1 - 1))).coeff i
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: ⊢ bernoulli 1 = -1 / 2

Tactic:
norm_num [bernoulli]

Goal state after:
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun x ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3))
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : √(2 * 512) = 32
| 4

Tactic:
equals 2 ^ (2 : ℝ) => rw [rpow_two]; norm_num1

Goal state after:
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: case succ.calc_4
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
m : ℕ
h_bdd : (fun n ↦ ‖f ↑n‖ * ∑ k ∈ Icc 0 n, ‖c k‖) =O[atTop] fun x ↦ 1
hf_int : LocallyIntegrableOn (deriv fun t ↦ ‖f t‖) (Set.Ici ↑m) volume
hf :
  ∀ (n : ℕ),
    ∑ k ∈ Icc 0 n, ‖f ↑k‖ * ‖c k‖ =
      ‖f ↑n‖ * ∑ k ∈ Icc 0 n, ‖c k‖ - ∫ (t : ℝ) in Set.Ioc ↑m ↑n, deriv (fun t ↦ ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖
g : ℝ → ℝ
hg₁ : (fun t ↦ deriv (fun t ↦ ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖) =O[atTop] g
hg₂ : IntegrableAtFilter g atTop volume
C₁ : ℝ
hC₁ : ∀ (n : ℕ), ‖‖f ↑n‖ * ∑ k ∈ Icc 0 n, ‖c k‖‖ ≤ C₁
C₂ : ℝ := ∫ (t : ℝ) in Set.Ioi ↑m, ‖deriv (fun t ↦ ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖‖
n : ℕ
⊢ C₁ + ∫ (t : ℝ) in Set.Ioc ↑m ↑n, ‖deriv (fun t ↦ ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖‖ ≤
    C₁ + ∫ (t : ℝ) in Set.Ioi ↑m, ‖deriv (fun t ↦ ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖‖

Tactic:
grw [setIntegral_mono_set ?_ (.of_forall fun _ ↦ norm_nonneg _)
          Set.Ioc_subset_Ioi_self.eventuallyLE]

Goal state after:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
m : ℕ
h_bdd : (fun n ↦ ‖f ↑n‖ * ∑ k ∈ Icc 0 n, ‖c k‖) =O[atTop] fun x ↦ 1
hf_int : LocallyIntegrableOn (deriv fun t ↦ ‖f t‖) (Set.Ici ↑m) volume
hf :
  ∀ (n : ℕ),
    ∑ k ∈ Icc 0 n, ‖f ↑k‖ * ‖c k‖ =
      ‖f ↑n‖ * ∑ k ∈ Icc 0 n, ‖c k‖ - ∫ (t : ℝ) in Set.Ioc ↑m ↑n, deriv (fun t ↦ ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖
g : ℝ → ℝ
hg₁ : (fun t ↦ deriv (fun t ↦ ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖) =O[atTop] g
hg₂ : IntegrableAtFilter g atTop volume
C₁ : ℝ
hC₁ : ∀ (n : ℕ), ‖‖f ↑n‖ * ∑ k ∈ Icc 0 n, ‖c k‖‖ ≤ C₁
C₂ : ℝ := ∫ (t : ℝ) in Set.Ioi ↑m, ‖deriv (fun t ↦ ‖f t‖) t * ∑ k ∈ Icc 0 ⌊t⌋₊, ‖c k‖‖
n : ℕ
⊢ IntegrableOn (fun x ↦ ‖deriv (fun t ↦ ‖f t‖) x * ∑ k ∈ Icc 0 ⌊x⌋₊, ‖c k‖‖) (Set.Ioi ↑m) volume
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case succ
x : ℝ
N : ℕ
ih :
  ∑ n ∈ Icc 1 (1 + 6 * N), b x n =
    b x 1 + ∑ n ∈ Icc 1 (3 * N), b x (2 * n) + ∑ n ∈ Icc 1 (2 * N), b x (3 * n) + ∑ n ∈ Icc 1 N, c x n
⊢ b x 1 + ∑ n ∈ Icc 1 (3 * N), b x (2 * n) + ∑ n ∈ Icc 1 (2 * N), b x (3 * n) +
                  ∑ n ∈ Icc 1 N, (b x (6 * n - 1) - b x (6 * n) + b x (6 * n + 1)) +
                b x (1 + 6 * N + 1) +
              b x (1 + 6 * N + 1 + 1) +
            b x (1 + 6 * N + 2 + 1) +
          b x (1 + 6 * N + 3 + 1) +
        b x (1 + 6 * N + 4 + 1) +
      b x (1 + 6 * N + 5 + 1) =
    b x 1 +
          (∑ n ∈ Icc 1 (3 * N), b x (2 * n) + b x (2 * (3 * N + 1)) + b x (2 * (3 * N + 1 + 1)) +
            b x (2 * (3 * N + 2 + 1))) +
        (∑ n ∈ Icc 1 (2 * N), b x (3 * n) + b x (3 * (2 * N + 1)) + b x (3 * (2 * N + 1 + 1))) +
      (∑ n ∈ Icc 1 N, (b x (6 * n - 1) - b x (6 * n) + b x (6 * n + 1)) +
        (b x (6 * N + 5) - b x (6 * (N + 1)) + b x (6 * (N + 1) + 1)))

Tactic:
ring_nf

Goal state after:
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
r : ℚ
hr : ‖↑r - ↑x‖ < 1
⊢ ‖↑r‖ = ‖↑r - ↑x + ↑x‖

Tactic:
ring_nf

Goal state after: