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✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetSemiring C
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : ∀ s ∈ C, MeasurableSet s
M : MeasurableSpace α := generateFrom C
Mle : M ≤ hα
μ' : Measure α := μ.trim Mle
hμ' : μ' = μ.trim Mle
⊢ ∃ m', (∀ s ∈ C, m' s = m s) ∧ ∀ (s : Set α), ‖m' s‖ₑ ≤ μ' s

Tactic:
by
    apply exists_extension_of_isSetSemiring_of_le_measure_of_generateFrom hC (fun s hs ↦ ?_) rfl
    apply (hm s hs).trans_eq
    exact (MeasureTheory.trim_measurableSet_eq Mle (measurableSet_generateFrom hs)).symm

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✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetSemiring C
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : ∀ s ∈ C, MeasurableSet s
M : MeasurableSpace α := generateFrom C
Mle : M ≤ hα
μ' : Measure α := μ.trim Mle
hμ' : μ' = μ.trim Mle
m' : VectorMeasure α E
m'C : ∀ s ∈ C, m' s = m s
hm' : ∀ (s : Set α), ‖m' s‖ₑ ≤ μ' s
m'_le : m'.variation ≤ μ'
this✝ : MeasurableSpace α := hα
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf : Pairwise (Function.onFun Disjoint f)
this :
  ∫ᵛ (x : α), μ[fun x ↦ ∑' (d : ℕ), (f d).indicator 1 x | M] x ∂•m' =
    ∫ᵛ (x : α), ∑' (d : ℕ), μ[(f d).indicator 1 | M] x ∂•m'
I : ∑' (i : ℕ), ∫⁻ (a : α), ‖μ[(f i).indicator 1 | M] a‖ₑ ∂μ < ∞
⊢ HasSum (fun i ↦ ∫ᵛ (x : α), μ[(f i).indicator 1 | M] x ∂•m') (∫ᵛ (x : α), ∑' (d : ℕ), μ[(f d).indicator 1 | M] x ∂•m')

Tactic:
rw [integral_tsum (by fun_prop)]

Goal state after:
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetSemiring C
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : ∀ s ∈ C, MeasurableSet s
M : MeasurableSpace α := generateFrom C
Mle : M ≤ hα
μ' : Measure α := μ.trim Mle
hμ' : μ' = μ.trim Mle
m' : VectorMeasure α E
m'C : ∀ s ∈ C, m' s = m s
hm' : ∀ (s : Set α), ‖m' s‖ₑ ≤ μ' s
m'_le : m'.variation ≤ μ'
this✝ : MeasurableSpace α := hα
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf : Pairwise (Function.onFun Disjoint f)
this :
  ∫ᵛ (x : α), μ[fun x ↦ ∑' (d : ℕ), (f d).indicator 1 x | M] x ∂•m' =
    ∫ᵛ (x : α), ∑' (d : ℕ), μ[(f d).indicator 1 | M] x ∂•m'
I : ∑' (i : ℕ), ∫⁻ (a : α), ‖μ[(f i).indicator 1 | M] a‖ₑ ∂μ < ∞
⊢ HasSum (fun i ↦ ∫ᵛ (x : α), μ[(f i).indicator 1 | M] x ∂•m') (∑' (i : ℕ), ∫ᵛ (a : α), μ[(f i).indicator 1 | M] a ∂•m')

α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : CompleteSpace E
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetSemiring C
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : ∀ s ∈ C, MeasurableSet s
M : MeasurableSpace α := generateFrom C
Mle : M ≤ hα
μ' : Measure α := μ.trim Mle
hμ' : μ' = μ.trim Mle
m' : VectorMeasure α E
m'C : ∀ s ∈ C, m' s = m s
hm' : ∀ (s : Set α), ‖m' s‖ₑ ≤ μ' s
m'_le : m'.variation ≤ μ'
this✝ : MeasurableSpace α := hα
f : ℕ → Set α
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
hf : Pairwise (Function.onFun Disjoint f)
this :
  ∫ᵛ (x : α), μ[fun x ↦ ∑' (d : ℕ), (f d).indicator 1 x | M] x ∂•m' =
    ∫ᵛ (x : α), ∑' (d : ℕ), μ[(f d).indicator 1 | M] x ∂•m'
I : ∑' (i : ℕ), ∫⁻ (a : α), ‖μ[(f i).indicator 1 | M] a‖ₑ ∂μ < ∞
⊢ ∑' (i : ℕ), ∫⁻ (a : α), ‖μ[(f i).indicator 1 | M] a‖ₑ ∂m'.variation ≠ ∞
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.toJordanDecomposition.posPart.real i - s.toJordanDecomposition.negPart.real i‖ ≤
    (s.toJordanDecomposition.posPart + s.toJordanDecomposition.negPart).real i

Tactic:
measureReal_add_apply

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.toJordanDecomposition.posPart.real i + s.toJordanDecomposition.negPart.real i
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs

Goal state before:
pp: case mp
M : Type u_1
ι : Type u_3
κ : Type u_4
inst✝ : AddCommMonoid M
s : Set (ι ⊕ κ → M)
hs : IsSemilinearSet s
x : ι → M
⊢ x ∈ {x | ∃ y, Sum.elim x y ∈ s} → x ∈ ⇑(LinearMap.funLeft ℕ M Sum.inl) '' s

Tactic:
intro ⟨y, hy⟩

Goal state after:
case mp
M : Type u_1
ι : Type u_3
κ : Type u_4
inst✝ : AddCommMonoid M
s : Set (ι ⊕ κ → M)
hs : IsSemilinearSet s
x : ι → M
y : κ → M
hy : Sum.elim x y ∈ s
⊢ x ∈ ⇑(LinearMap.funLeft ℕ M Sum.inl) '' s
Module: Mathlib.MeasureTheory.VectorMeasure.Integral

Goal state before:
pp: X : Type u_2
F : Type u_5
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
μ : VectorMeasure X F
⊢ (μ.transpose (lsmul ℝ ℝ)).variation = μ.variation

Tactic:
apply variation_transpose_eq
  simp [nnnorm_smul, mul_comm]

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

Goal state before:
pp: X : Type u_2
E : Type u_4
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
μ : SignedMeasure X
⊢ (transpose μ (lsmul ℝ ℝ).flip).variation = variation μ

Tactic:
apply variation_transpose_eq
  simp [nnnorm_smul, mul_comm]

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
a : X
⊢ f a = f a - g a + g a

Tactic:
abel

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
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
f g : X → E
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
hf : μ.Integrable f
hg : μ.Integrable g
⊢ dist ∫ᵛ (a : X), f a ∂[B; μ] ∫ᵛ (a : X), g a ∂[B; μ] ≤ (‖B‖ₑ * ∫⁻ (a : X), edist (f a) (g a) ∂μ.variation).toReal

Tactic:
dist_integral_le_lintegral_edist hf hg,

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 g : X → E
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
hf : μ.Integrable f
hg : μ.Integrable g
⊢ ‖B‖ * (∫⁻ (a : X), edist (f a) (g a) ∂μ.variation).toReal ≤ (‖B‖ₑ * ∫⁻ (a : X), edist (f a) (g a) ∂μ.variation).toReal
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case pos
M : Type u_1
inst✝⁴ : AddCommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelAddMonoid M
inst✝ : CanonicallyOrderedAdd M
s : Set M
hs : IsSlice s
hs' : s.Nonempty
f : M → AddSubmonoid M :=
  fun x ↦ if hx : x ∈ s then { carrier := {y | x + y ∈ s}, add_mem' := ⋯, zero_mem' := ⋯ } else ⊥
hf : ∀ x ∈ s, ∀ (y : M), y ∈ f x ↔ x + y ∈ s
g : M → AddSemigroupIdeal M := fun x ↦ AddSemigroupIdeal.closure (↑(f x) \ {0})
hg : ∀ x ∈ s, ∀ y ∈ s, x ≤ y → g x ≤ g y
a : M
ha : MaximalFor (fun x ↦ x ∈ s) g a
x : M
hx : a + x ∈ s
w : M
ih : ∀ y < w, ∀ u ∈ f a, u ≠ 0 → a + x + (y + u) ∈ s → y + u ∈ f a
u : M
hu₁ : u ∈ f a
hu₂ : u ≠ 0
hxy : a + x + (w + u) ∈ s
hw₁ : w = 0
⊢ w + u ∈ f a

Tactic:
simpa [hw₁]

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

Goal state before:
pp: α : Type u_1
A : Set ℕ
inst✝ : Finite α
φ : presburger[[↑A]].Formula α
e : α ⊕ Fin 0 ≃ α := Equiv.sumEmpty α (Fin 0)
x : α → ℕ
⊢ φ.Realize x ↔
    ∃ x_1, BoundedFormula.Realize φ (x_1 ∘ Sum.inl) (x_1 ∘ Sum.inr) ∧ (LinearMap.funLeft ℕ ℕ ⇑e.symm) x_1 = x

Tactic:
rw [(e.arrowCongr (.refl ℕ)).exists_congr_left]

Goal state after:
α : Type u_1
A : Set ℕ
inst✝ : Finite α
φ : presburger[[↑A]].Formula α
e : α ⊕ Fin 0 ≃ α := Equiv.sumEmpty α (Fin 0)
x : α → ℕ
⊢ φ.Realize x ↔
    ∃ b,
      BoundedFormula.Realize φ ((e.arrowCongr (_root_.Equiv.refl ℕ)).symm b ∘ Sum.inl)
          ((e.arrowCongr (_root_.Equiv.refl ℕ)).symm b ∘ Sum.inr) ∧
        (LinearMap.funLeft ℕ ℕ ⇑e.symm) ((e.arrowCongr (_root_.Equiv.refl ℕ)).symm b) = x
Module: Mathlib.ModelTheory.Complexity

Goal state before:
pp: case ex.refine_1
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 :
  ∀ {φ : L.BoundedFormula α (n✝ + 1)},
    φ.IsQF → ∀ {xs : Fin (n✝ + 1) → M}, (φ.toPrenexImpRight φ✝).Realize v xs ↔ (φ ⟹ φ✝).Realize v xs
φ : L.BoundedFormula α n✝
hφ : φ.IsQF
xs : Fin n✝ → M
⊢ (∃ a, φ.Realize v xs → φ✝.Realize v (snoc xs a)) → φ.Realize v xs → ∃ a, φ✝.Realize v (snoc xs a)

pp: case ex.refine_2
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 :
  ∀ {φ : L.BoundedFormula α (n✝ + 1)},
    φ.IsQF → ∀ {xs : Fin (n✝ + 1) → M}, (φ.toPrenexImpRight φ✝).Realize v xs ↔ (φ ⟹ φ✝).Realize v xs
φ : L.BoundedFormula α n✝
hφ : φ.IsQF
xs : Fin n✝ → M
h' : φ.Realize v xs → ∃ a, φ✝.Realize v (snoc xs a)
⊢ ∃ a, φ.Realize v xs → φ✝.Realize v (snoc xs a)

Tactic:
· rintro ⟨a, ha⟩ h
      exact ⟨a, ha h⟩

Goal state after:
case ex.refine_2
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 :
  ∀ {φ : L.BoundedFormula α (n✝ + 1)},
    φ.IsQF → ∀ {xs : Fin (n✝ + 1) → M}, (φ.toPrenexImpRight φ✝).Realize v xs ↔ (φ ⟹ φ✝).Realize v xs
φ : L.BoundedFormula α n✝
hφ : φ.IsQF
xs : Fin n✝ → M
h' : φ.Realize v xs → ∃ a, φ✝.Realize v (snoc xs a)
⊢ ∃ a, φ.Realize v xs → φ✝.Realize v (snoc xs a)
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: case mp.inr
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
S : Set M
Scount : S.Countable
hS : (closure L).toFun S = N
h : (↑N).Nonempty
f : ℕ → M
h' : S ∪ {h.some} = range f
⊢ (closure L).toFun (range f) = N

Tactic:
← h',

Goal state after:
case mp.inr
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
S : Set M
Scount : S.Countable
hS : (closure L).toFun S = N
h : (↑N).Nonempty
f : ℕ → M
h' : S ∪ {h.some} = range f
⊢ (closure L).toFun (S ∪ {h.some}) = N
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: L : Language
M : Type w
inst✝¹ : L.Structure M
inst✝ : Countable M
⊢ Countable (L.FGEquiv M M)

Tactic:
let g : L.FGEquiv M M →
      Σ U : { S : L.Substructure M // S.FG }, U.val →[L] M :=
    fun f ↦ ⟨⟨f.val.dom, f.prop⟩, (subtype _).toHom.comp f.val.toEquiv.toHom⟩

Goal state after:
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⟩
⊢ Countable (L.FGEquiv M M)
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: L : Language
ι : Type u_1
inst✝⁵ : Countable ι
inst✝⁴ : Preorder ι
inst✝³ : IsDirectedOrder ι
inst✝² : Nonempty ι
G : ι → Type w
inst✝¹ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
h : ∀ (i : ι), CG L (G i)
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
⊢ CG L (DirectLimit G f)

Tactic:
refine ⟨⟨⋃ i, DirectLimit.of L ι G f i '' Classical.choose (h i).out, ?_, ?_⟩⟩

Goal state after:
case refine_1
L : Language
ι : Type u_1
inst✝⁵ : Countable ι
inst✝⁴ : Preorder ι
inst✝³ : IsDirectedOrder ι
inst✝² : Nonempty ι
G : ι → Type w
inst✝¹ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
h : ∀ (i : ι), CG L (G i)
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
⊢ (⋃ i, ⇑(of L ι G f i) '' Classical.choose ⋯).Countable

case refine_2
L : Language
ι : Type u_1
inst✝⁵ : Countable ι
inst✝⁴ : Preorder ι
inst✝³ : IsDirectedOrder ι
inst✝² : Nonempty ι
G : ι → Type w
inst✝¹ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
h : ∀ (i : ι), CG L (G i)
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
⊢ (Substructure.closure L).toFun (⋃ i, ⇑(of L ι G f i) '' Classical.choose ⋯) = ⊤
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: L : Language
M : Type w
inst✝ : L.Structure M
h : L.IsUltrahomogeneous M
⊢ Amalgamation (L.age M)

Tactic:
by
  rintro N P Q NP NQ ⟨Nfg, ⟨-⟩⟩ ⟨Pfg, ⟨PM⟩⟩ ⟨Qfg, ⟨QM⟩⟩
  obtain ⟨g, hg⟩ := h (PM.comp NP).toHom.range (Nfg.range _)
    ((QM.comp NQ).comp (PM.comp NP).equivRange.symm.toEmbedding)
  let s := (g.toHom.comp PM.toHom).range ⊔ QM.toHom.range
  refine ⟨Bundled.of s,
    Embedding.comp (Substructure.inclusion le_sup_left)
      (g.toEmbedding.comp PM).equivRange.toEmbedding,
    Embedding.comp (Substructure.inclusion le_sup_right) QM.equivRange.toEmbedding,
    ⟨(fg_iff_structure_fg _).1 (FG.sup (Pfg.range _) (Qfg.range _)), ⟨Substructure.subtype _⟩⟩, ?_⟩
  ext n
  apply Subtype.ext
  have hgn := (Embedding.ext_iff.1 hg) ((PM.comp NP).equivRange n)
  simp only [Embedding.comp_apply, Equiv.coe_toEmbedding, Equiv.symm_apply_apply,
    Substructure.coe_subtype, Embedding.equivRange_apply] at hgn
  simp only [Embedding.comp_apply, Equiv.coe_toEmbedding]
  erw [Substructure.coe_inclusion, Substructure.coe_inclusion]
  simp only [Embedding.equivRange_apply, hgn]
  -- This used to be `simp only [...]` before https://github.com/leanprover/lean4/pull/2644
  erw [Embedding.comp_apply, Equiv.coe_toEmbedding,
    Embedding.equivRange_apply]
  simp

Goal state after:
Module: Mathlib.ModelTheory.Types

Goal state before:
pp: L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
t : Finset L[[α]].Sentence
⊢ List.foldr (fun x1 x2 ↦ x1 ⊓ x2) ⊤ t.toList ∈ p ↔ ↑t ⊆ ↑p

Tactic:
subset_def,

Goal state after:
L : Language
T : L.Theory
α : Type w
p : T.CompleteType α
t : Finset L[[α]].Sentence
⊢ List.foldr (fun x1 x2 ↦ x1 ⊓ x2) ⊤ t.toList ∈ p ↔ ∀ x ∈ ↑t, x ∈ ↑p
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:
by
  rw [← Set.Iic_inter_Ioi]
  exact isLocallyClosed_Iic.inter isLocallyClosed_Ioi

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

Goal state before:
pp: ⊢ ¬IsCyclic (ZMod 8)ˣ

Tactic:
by
  rw [IsCyclic.iff_exponent_eq_card, Nat.card_eq_fintype_card, card_units_eq_totient]
  have h : Monoid.exponent (ZMod 8)ˣ ∣ 2 := Monoid.exponent_dvd_of_forall_pow_eq_one (by decide)
  intro (h' : Monoid.exponent (ZMod 8)ˣ = 4)
  simp [h'] at h

Goal state after:
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: a b : ℝ
k : ℕ
hk : k ∈ Ico (⌊a⌋₊ + 1) ⌊b⌋₊
⊢ k ∈ Set.Ico (⌊a⌋₊ + 1) ⌊b⌋₊

Tactic:
← Finset.coe_Ico

Goal state after:
a b : ℝ
k : ℕ
hk : k ∈ Ico (⌊a⌋₊ + 1) ⌊b⌋₊
⊢ k ∈ ↑(Ico (⌊a⌋₊ + 1) ⌊b⌋₊)
Module: Mathlib.NumberTheory.AbelSummation

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

Tactic:
exact integrableOn_empty

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

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

Tactic:
induction n generalizing k with

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n : ℕ
h_odd : Odd n
hlt : 1 < n
⊢ bernoulli' n = 0

Tactic:
by
  let B := mk fun n => bernoulli' n / (n ! : ℚ)
  suffices (B - evalNegHom B) * (exp ℚ - 1) = X * (exp ℚ - 1) by
    rcases mul_eq_mul_right_iff.mp this with h | h <;>
      simp only [PowerSeries.ext_iff, evalNegHom, coeff_X] at h
    · apply eq_zero_of_neg_eq
      specialize h n
      split_ifs at h <;> simp_all [B, h_odd.neg_one_pow, factorial_ne_zero]
    · simpa +decide [Nat.factorial] using h 1
  have h : B * (exp ℚ - 1) = X * exp ℚ := by
    simpa [bernoulli'PowerSeries] using bernoulli'PowerSeries_mul_exp_sub_one ℚ
  rw [sub_mul, h, mul_sub X, sub_right_inj, ← neg_sub, mul_neg, neg_eq_iff_eq_neg]
  suffices evalNegHom (B * (exp ℚ - 1)) * exp ℚ = evalNegHom (X * exp ℚ) * exp ℚ by
    simpa [mul_assoc, sub_mul, mul_comm (evalNegHom (exp ℚ)), exp_mul_exp_neg_eq_one]
  congr

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
⊢ x * (2 * x) ^ √(2 * x) * 4 ^ (2 * x / 3) / 4 ^ x ≤ 1

Tactic:
← div_div_eq_mul_div,

Goal state after:
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
⊢ x * (2 * x) ^ √(2 * x) / (4 ^ x / 4 ^ (2 * x / 3)) ≤ 1
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
a : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg : LocallyIntegrableOn g (Set.Ici a) volume
K : Set ℝ
hK₁ : K ⊆ Set.Ici a
hK₂ : IsCompact K
hK₃ : ¬K.Nonempty
⊢ IntegrableOn (fun t ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) ∅ volume

Tactic:
exact integrableOn_empty

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n p : ℕ
f : ℕ → ℚ := fun i ↦ bernoulli i * ↑(p.succ.succ.choose i) * ↑n ^ (p.succ.succ - i) / ↑p.succ.succ
f' : ℕ → ℚ := fun i ↦ bernoulli' i * ↑(p.succ.succ.choose i) * ↑n ^ (p.succ.succ - i) / ↑p.succ.succ
hle : 1 ≤ n + 1
hne : ↑p + 1 + 1 ≠ 0
h1 : ∀ (r : ℚ), r * (↑p + 1 + 1) * ↑n ^ p.succ / (↑p + 1 + 1) = r * ↑n ^ p.succ
h2 : f 1 + ↑n ^ p.succ = 1 / 2 * ↑n ^ p.succ
this :
  ∑ i ∈ range p, bernoulli (i + 2) * ↑((p + 2).choose (i + 2)) * ↑n ^ (p - i) / ↑(p + 2) =
    ∑ i ∈ range p, bernoulli' (i + 2) * ↑((p + 2).choose (i + 2)) * ↑n ^ (p - i) / ↑(p + 2)
⊢ ∑ i ∈ range p.succ.succ, f i + ↑n ^ p.succ = ∑ i ∈ range p, f i.succ.succ + f 1 + f 0 + ↑n ^ p.succ

Tactic:
sum_range_succ'

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n p : ℕ
f : ℕ → ℚ := fun i ↦ bernoulli i * ↑(p.succ.succ.choose i) * ↑n ^ (p.succ.succ - i) / ↑p.succ.succ
f' : ℕ → ℚ := fun i ↦ bernoulli' i * ↑(p.succ.succ.choose i) * ↑n ^ (p.succ.succ - i) / ↑p.succ.succ
hle : 1 ≤ n + 1
hne : ↑p + 1 + 1 ≠ 0
h1 : ∀ (r : ℚ), r * (↑p + 1 + 1) * ↑n ^ p.succ / (↑p + 1 + 1) = r * ↑n ^ p.succ
h2 : f 1 + ↑n ^ p.succ = 1 / 2 * ↑n ^ p.succ
this :
  ∑ i ∈ range p, bernoulli (i + 2) * ↑((p + 2).choose (i + 2)) * ↑n ^ (p - i) / ↑(p + 2) =
    ∑ i ∈ range p, bernoulli' (i + 2) * ↑((p + 2).choose (i + 2)) * ↑n ^ (p - i) / ↑(p + 2)
⊢ ∑ i ∈ range p, f' i.succ.succ + f' 1 + f' 0 = ∑ i ∈ range p.succ.succ, f' i

Tactic:
sum_range_succ'

Goal state after:
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
A : Fin m.succ → Fq[X]
hA : (A 0).degree < degree 0
⊢ False

Tactic:
rw [degree_zero] at hA

Goal state after:
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
A : Fin m.succ → Fq[X]
hA : (A 0).degree < ⊥
⊢ False
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ → Fq[X]
hbε : 0 < cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε

Tactic:
have q_pos' : (0 : ℝ) < Fintype.card Fq := by assumption_mod_cast

Goal state after:
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ → Fq[X]
hbε : 0 < cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
p k : ℕ
hp : _root_.Prime p
hk₀ : 0 < k
a✝ : 0 < p ^ k
hbx : ↑p ^ k ≤ x
⊢ 2 ^ k ≤ ↑p ^ k

Tactic:
exact pow_le_pow_left₀ (by norm_num) (mod_cast hp.nat_prime.two_le) _

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: case refine_3.refine_1
R : Type u_1
inst✝ : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
p k : ℕ
hp : _root_.Prime p
hk₀ : 0 < k
a✝ : 0 < p ^ k
hbx : ↑p ^ k ≤ x
⊢ ↑k ≤ log x / log 2

Tactic:
rw [le_div_iff₀ (log_pos (by norm_num)), ← Real.log_pow]
        gcongr
        apply (LE.le.trans ?_ hbx)
        exact pow_le_pow_left₀ (by norm_num) (mod_cast hp.nat_prime.two_le) _

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx✝ : 1 ≤ x
hx : 2 ≤ x
⊢ log x / log 2 * (log 4 * √x) = log 4 / log 2 * √x * log x

Tactic:
by field

Goal state after: