mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Measure.SeparableMeasure

Goal state before:
pp: X : Type u_1
E : Type u_2
m : MeasurableSpace X
inst✝² : NormedAddCommGroup E
μ : Measure X
p : ℝ≥0∞
one_le_p : Fact (1 ≤ p)
p_ne_top : Fact (p ≠ ∞)
𝒜✝ : Set (Set X)
inst✝¹ : IsSeparable μ
inst✝ : SeparableSpace E
𝒜 : Set (Set X)
count_𝒜 : 𝒜.Countable
h𝒜 : μ.MeasureDense 𝒜
𝒜₀ : Set (Set X) := {s | s ∈ 𝒜 ∧ μ s ≠ ∞}
h𝒜₀ : μ.MeasureDense 𝒜₀
count_𝒜₀ : 𝒜₀.Countable
p_ne_zero : p ≠ 0
u : Set E
countable_u : u.Countable
dense_u : Dense u
⊢ SeparableSpace ↥(Lp E p μ)

Tactic:
let key (n : ℕ) (d : Fin n → u) (s : Fin n → 𝒜₀) : (Lp E p μ) :=
    ∑ i, indicatorConstLp p (h𝒜₀.measurable (s i) (Subtype.mem (s i))) (s i).2.2 (d i : E)

Goal state after:
X : Type u_1
E : Type u_2
m : MeasurableSpace X
inst✝² : NormedAddCommGroup E
μ : Measure X
p : ℝ≥0∞
one_le_p : Fact (1 ≤ p)
p_ne_top : Fact (p ≠ ∞)
𝒜✝ : Set (Set X)
inst✝¹ : IsSeparable μ
inst✝ : SeparableSpace E
𝒜 : Set (Set X)
count_𝒜 : 𝒜.Countable
h𝒜 : μ.MeasureDense 𝒜
𝒜₀ : Set (Set X) := {s | s ∈ 𝒜 ∧ μ s ≠ ∞}
h𝒜₀ : μ.MeasureDense 𝒜₀
count_𝒜₀ : 𝒜₀.Countable
p_ne_zero : p ≠ 0
u : Set E
countable_u : u.Countable
dense_u : Dense u
key : (n : ℕ) → (Fin n → ↑u) → (Fin n → ↑𝒜₀) → ↥(Lp E p μ) := fun n d s ↦ ∑ i, indicatorConstLp p ⋯ ⋯ ↑(d i)
⊢ SeparableSpace ↥(Lp E p μ)
Module: Mathlib.MeasureTheory.Order.UpperLower

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs : IsUpperSet s
⊢ volume (frontier s) = 0

Tactic:
refine measure_mono_null (fun x hx ↦ ?_)
    (Besicovitch.ae_tendsto_measure_inter_div_of_measurableSet _
      (isClosed_closure (s := s)).measurableSet)
  by_cases h : x ∈ closure s <;>
    simp only [mem_compl_iff, mem_ofPred, h, not_false_eq_true, indicator_of_notMem,
      indicator_of_mem, Pi.one_apply]
  · refine aux₁ fun _ ↦ hs.compl.exists_subset_ball <| frontier_subset_closure ?_
    rwa [frontier_compl]
  · exact aux₀ fun _ ↦ hs.exists_subset_ball <| frontier_subset_closure hx

Goal state after:
Module: Mathlib.MeasureTheory.Order.UpperLower

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs : IsLowerSet s
⊢ volume (frontier s) = 0

Tactic:
refine measure_mono_null (fun x hx ↦ ?_)
    (Besicovitch.ae_tendsto_measure_inter_div_of_measurableSet _
      (isClosed_closure (s := s)).measurableSet)
  by_cases h : x ∈ closure s <;>
    simp only [mem_compl_iff, mem_ofPred, h, not_false_eq_true, indicator_of_notMem,
      indicator_of_mem, Pi.one_apply]
  · refine aux₁ fun _ ↦ hs.compl.exists_subset_ball <| frontier_subset_closure ?_
    rwa [frontier_compl]
  · exact aux₀ fun _ ↦ hs.exists_subset_ball <| frontier_subset_closure hx

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

Goal state before:
pp: α : Type u_1
inst✝⁸ : LinearOrder α
inst✝⁷ : DenselyOrdered α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : SecondCountableTopology α
inst✝³ : CompactIccSpace α
hα : MeasurableSpace α
inst✝² : BorelSpace α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : α → E
a b : α
hf : BoundedVariationOn f univ
h : a ≤ b
⊢ Function.rightLim f a - Function.leftLim f a + hf.vectorMeasure (Ioc a b) =
    Function.rightLim f b - Function.leftLim f a

Tactic:
hf.vectorMeasure_Ioc h

Goal state after:
α : Type u_1
inst✝⁸ : LinearOrder α
inst✝⁷ : DenselyOrdered α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : SecondCountableTopology α
inst✝³ : CompactIccSpace α
hα : MeasurableSpace α
inst✝² : BorelSpace α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : α → E
a b : α
hf : BoundedVariationOn f univ
h : a ≤ b
⊢ Function.rightLim f a - Function.leftLim f a + (Function.rightLim f b - Function.rightLim f a) =
    Function.rightLim f b - Function.leftLim f a
Module: Mathlib.MeasureTheory.VectorMeasure.Prod

Goal state before:
pp: case iUnion
X : Type u_2
Y : Type u_3
F : Type u_5
mX : MeasurableSpace X
mY : MeasurableSpace Y
inst✝ : NormedAddCommGroup F
ν : VectorMeasure Y F
s : Set (X × Y)
f : ℕ → Set (X × Y)
hfd : Pairwise (Disjoint on f)
hfm : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ (i : ℕ), StronglyMeasurable fun x ↦ ν (Prod.mk x ⁻¹' f i)
⊢ StronglyMeasurable fun x ↦ ν (Prod.mk x ⁻¹' ⋃ i, f i)

Tactic:
have (a : X) : HasSum (fun i ↦ ν (Prod.mk a ⁻¹' f i)) (ν (Prod.mk a ⁻¹' ⋃ i, f i)) := by
      rw [preimage_iUnion]
      apply hasSum_of_disjoint_iUnion
      exacts [fun i ↦ measurable_prodMk_left (hfm i), hfd.mono fun _ _ ↦ .preimage _]

Goal state after:
case iUnion
X : Type u_2
Y : Type u_3
F : Type u_5
mX : MeasurableSpace X
mY : MeasurableSpace Y
inst✝ : NormedAddCommGroup F
ν : VectorMeasure Y F
s : Set (X × Y)
f : ℕ → Set (X × Y)
hfd : Pairwise (Disjoint on f)
hfm : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ (i : ℕ), StronglyMeasurable fun x ↦ ν (Prod.mk x ⁻¹' f i)
this : ∀ (a : X), HasSum (fun i ↦ ν (Prod.mk a ⁻¹' f i)) (ν (Prod.mk a ⁻¹' ⋃ i, f i))
⊢ StronglyMeasurable fun x ↦ ν (Prod.mk x ⁻¹' ⋃ i, f i)
Module: Mathlib.MeasureTheory.VectorMeasure.Integral

Goal state before:
pp: case hbc
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
s : Set X
hs : MeasurableSet s
hsf : μ.variation s < ∞
⊢ ‖μ s‖ ≤ μ.variation.real s

Tactic:
exact norm_measure_le_variation hsf.ne

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

Goal state before:
pp: case hst
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
μ : VectorMeasure X F
f : X → E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
s : ℕ → Set X
hm : ∀ (i : ℕ), MeasurableSet (s i)
hd : Pairwise (Disjoint on s)
hfi : μ.IntegrableOn f (⋃ i, s i)
hG : CompleteSpace G
I : ∑' (i : ℕ), ‖B‖ₑ * ∫⁻ (x : X) in s i, ‖f x‖ₑ ∂μ.variation < ∞
this✝ : Summable fun n ↦ ∫ᵛ (x : X) in s n, f x ∂[B; μ]
N : ℕ
this : ⋃ n, s n = (⋃ n ∈ Finset.range N, s n) ∪ ⋃ n, s (n + N)
⊢ Disjoint (⋃ n ∈ Finset.range N, s n) (⋃ n, s (n + N))

Tactic:
simp only [Finset.mem_range, disjoint_iUnion_right, disjoint_iUnion_left]

Goal state after:
case hst
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
μ : VectorMeasure X F
f : X → E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
s : ℕ → Set X
hm : ∀ (i : ℕ), MeasurableSet (s i)
hd : Pairwise (Disjoint on s)
hfi : μ.IntegrableOn f (⋃ i, s i)
hG : CompleteSpace G
I : ∑' (i : ℕ), ‖B‖ₑ * ∫⁻ (x : X) in s i, ‖f x‖ₑ ∂μ.variation < ∞
this✝ : Summable fun n ↦ ∫ᵛ (x : X) in s n, f x ∂[B; μ]
N : ℕ
this : ⋃ n, s n = (⋃ n ∈ Finset.range N, s n) ∪ ⋃ n, s (n + N)
⊢ ∀ (i i_1 : ℕ), i_1 < N → Disjoint (s i_1) (s (i + N))
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs

Goal state before:
pp: case mpr.inr
M : Type u_1
inst✝ : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
x : M
hx : x ∈ closure (insert a t)
⊢ a + x ∈ closure (a +ᵥ ↑(closure t))

Tactic:
simp_rw [insert_eq, closure_union, mem_sup, mem_closure_singleton] at hx

Goal state after:
case mpr.inr
M : Type u_1
inst✝ : AddCommMonoid M
a : M
t : Set M
ht : t.Finite
x : M
hx : ∃ y, (∃ n, n • a = y) ∧ ∃ z ∈ closure t, y + z = x
⊢ a + x ∈ closure (a +ᵥ ↑(closure t))
Module: Mathlib.MeasureTheory.VectorMeasure.Integral

Goal state before:
pp: X : Type u_2
E : Type u_4
F : Type u_5
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
f : X → E
μ ν : VectorMeasure X F
hμ : μ.Integrable f
hν : ν.Integrable f
⊢ (μ + ν).Integrable f

Tactic:
apply Integrable.mono_measure (integrable_add_measure.2 ⟨hμ, hν⟩)
  grw [variation_add_le]

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
x y : DirectLimit G f
xy : (g (Quotient.out x).fst) (Quotient.out x).snd = (g (Quotient.out y).fst) (Quotient.out y).snd
i : ι
hx : (Quotient.out x).fst ≤ i
hy : (Quotient.out y).fst ≤ i
⊢ x = y

Tactic:
← Hg x.out.1 i hx,

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)
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
x y : DirectLimit G f
i : ι
hx : (Quotient.out x).fst ≤ i
xy : (g i) ((f (Quotient.out x).fst i hx) (Quotient.out x).snd) = (g (Quotient.out y).fst) (Quotient.out y).snd
hy : (Quotient.out y).fst ≤ i
⊢ x = y
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: case refine_1
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
h : L.IsExtensionPair M N
S : L.Substructure M
S_FG : S.FG
f : ↥S ↪[L] N
m : M
⊢ ∃ g, f = g.comp (Substructure.inclusion ⋯)

pp: case refine_2
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
h : ∀ (S : L.Substructure M), S.FG → ∀ (f : ↥S ↪[L] N) (m : M), ∃ g, f = g.comp (Substructure.inclusion ⋯)
x✝ : L.FGEquiv M N
m : M
f : M ≃ₚ[L] N
f_FG : f.dom.FG
⊢ ∃ g, m ∈ (↑g).dom ∧ ⟨f, f_FG⟩ ≤ g

Tactic:
· 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]

Goal state after:
case refine_2
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
h : ∀ (S : L.Substructure M), S.FG → ∀ (f : ↥S ↪[L] N) (m : M), ∃ g, f = g.comp (Substructure.inclusion ⋯)
x✝ : L.FGEquiv M N
m : M
f : M ≃ₚ[L] N
f_FG : f.dom.FG
⊢ ∃ g, m ∈ (↑g).dom ∧ ⟨f, f_FG⟩ ≤ g
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : 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)
| x + 0

Tactic:
← Finset.sum_const_zero (ι := hs.basisSet) (s := Finset.univ)

Goal state after:
ι : 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)
| x + ∑ _x, 0
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: L : Language
ι : Type v
inst✝³ : Preorder ι
inst✝² : Nonempty ι
inst✝¹ : IsDirectedOrder ι
M : Type u_1
inst✝ : L.Structure M
S : ι →o L.Substructure M
⊢ (liftInclusion S).toHom.range = ⨆ i, S i

Tactic:
simp_rw [liftInclusion, range_lift, Substructure.range_subtype]

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

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
i : ι → ℕ
hi : i ∈ hs.fundamentalDomain \ {hs.base}
⊢ IsSemilinearSet
    ({a | a ∘ Sum.inr ∈ closure hs.basisSet} ∩ {a | ∃ y' ∈ closure hs.basisSet, a ∘ Sum.inl + y' = i + a ∘ Sum.inr})

Tactic:
apply Nat.isSemilinearSet_inter <| Nat.isSemilinearSet_preimage
      (.closure_of_finite hs.finite_basisSet) (LinearMap.funLeft ℕ ℕ Sum.inr)

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
i : ι → ℕ
hi : i ∈ hs.fundamentalDomain \ {hs.base}
⊢ IsSemilinearSet {a | ∃ y' ∈ closure hs.basisSet, a ∘ Sum.inl + y' = i + a ∘ Sum.inr}
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
i : ι → ℕ
hi : i ∈ hs.fundamentalDomain \ {hs.base}
⊢ IsSemilinearSet
    ({a | a ∘ Sum.inr ∈ closure hs.basisSet} ∩
      {a | (a ∘ Sum.inl) ∘ Sum.inl + a ∘ Sum.inr = i + (a ∘ Sum.inl) ∘ Sum.inr})

Tactic:
apply Nat.isSemilinearSet_inter <| Nat.isSemilinearSet_preimage
      (.closure_of_finite hs.finite_basisSet) (LinearMap.funLeft ℕ ℕ Sum.inr)

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
i : ι → ℕ
hi : i ∈ hs.fundamentalDomain \ {hs.base}
⊢ IsSemilinearSet {a | (a ∘ Sum.inl) ∘ Sum.inl + a ∘ Sum.inr = i + (a ∘ Sum.inl) ∘ Sum.inr}
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: case mp
L : Language
ι : Type w
inst✝⁴ : Preorder ι
inst✝³ : IsDirectedOrder ι
inst✝² : Nonempty ι
G : ι → Type (max w w')
inst✝¹ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
M : Bundled L.Structure
Mfg : Structure.FG L ↑M
e : ↑M ↪[L] DirectLimit G f
s : Finset (DirectLimit G f)
hs : (closure L).toFun ↑s = e.toHom.range
out : Quotient (DirectLimit.setoid G f) → Structure.Sigma f := Quotient.out
i : ι
hi : ∀ i_1 ∈ Finset.image (Sigma.fst ∘ out) s, i_1 ≤ i
e' : ↥(DirectLimit.of L ι G f i).toHom.range ↪[L] G i
⊢ ∃ i, M ∈ L.age (G i)

Tactic:
refine ⟨i, Mfg, ⟨e'.comp ((Substructure.inclusion ?_).comp e.equivRange.toEmbedding)⟩⟩

Goal state after:
case mp
L : Language
ι : Type w
inst✝⁴ : Preorder ι
inst✝³ : IsDirectedOrder ι
inst✝² : Nonempty ι
G : ι → Type (max w w')
inst✝¹ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
M : Bundled L.Structure
Mfg : Structure.FG L ↑M
e : ↑M ↪[L] DirectLimit G f
s : Finset (DirectLimit G f)
hs : (closure L).toFun ↑s = e.toHom.range
out : Quotient (DirectLimit.setoid G f) → Structure.Sigma f := Quotient.out
i : ι
hi : ∀ i_1 ∈ Finset.image (Sigma.fst ∘ out) s, i_1 ≤ i
e' : ↥(DirectLimit.of L ι G f i).toHom.range ↪[L] G i
⊢ e.toHom.range ≤ (DirectLimit.of L ι G f i).toHom.range
Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael

Goal state before:
pp: n : ℕ
hn : n ≤ 2
⊢ λ (2 ^ n) = 2 ^ (n - 1)

Tactic:
carmichael_two_pow_of_le_two_eq_totient hn

Goal state after:
n : ℕ
hn : n ≤ 2
⊢ φ (2 ^ n) = 2 ^ (n - 1)
Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt

Goal state before:
pp: n : ℕ
hn : ¬n = 0
mn : 0 ∣ n
⊢ n = 0

Tactic:
simpa using mn

Goal state after:
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: case inl.inr
𝕜 : 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⌋₊
h_locint :
  ∀ {t₁ t₂ : ℝ} {n : ℕ},
    t₁ ≤ t₂ →
      ↑n ≤ t₁ → t₂ ≤ ↑n + 1 → a ≤ t₁ → t₂ ≤ b → IntervalIntegrable (fun t ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume t₁ t₂
aux1 : 0 ≤ b
aux2 : ↑⌊a⌋₊ + 1 ≤ b
⊢ IntegrableOn (fun t ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) (Set.Icc a b) volume

Tactic:
have aux3 : a ≤ ⌊a⌋₊ + 1 := (Nat.lt_floor_add_one _).le

Goal state after:
case inl.inr
𝕜 : 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⌋₊
h_locint :
  ∀ {t₁ t₂ : ℝ} {n : ℕ},
    t₁ ≤ t₂ →
      ↑n ≤ t₁ → t₂ ≤ ↑n + 1 → a ≤ t₁ → t₂ ≤ b → IntervalIntegrable (fun t ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume t₁ t₂
aux1 : 0 ≤ b
aux2 : ↑⌊a⌋₊ + 1 ≤ b
aux3 : a ≤ ↑⌊a⌋₊ + 1
⊢ IntegrableOn (fun t ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) (Set.Icc a b) volume
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)
⊢ (1 + ↑p ^ m * ↑a) ^ p ^ (n + 1) = 1

Tactic:
obtain ⟨y, hy⟩ := this (n + 1)

Goal state after:
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 ^ m * ↑a) ^ p ^ (n + 1) = 1
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⌋₊
⊢ ∑ 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 aux3 : a ≤ ⌊a⌋₊ + 1 := (Nat.lt_floor_add_one _).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
⊢ ∑ 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.ZMod.UnitsCyclic

Goal state before:
pp: p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
n : ℕ
⊢ IsCyclic (ZMod (p ^ n))ˣ

Tactic:
by
  have := Fact.mk hp
  rcases n with _ | n
  · rw [pow_zero]; infer_instance
  -- We first consider the element `1 + p` of order `p ^ n`
  set a := (1 + p : ZMod (p ^ (n + 1))) with ha_def
  have ha : IsUnit a := by
    rw [ha_def, ← Nat.cast_one (R := ZMod _), ← Nat.cast_add, ZMod.isUnit_iff_coprime]
    apply Nat.Coprime.pow_right
    simp only [Nat.coprime_add_self_left, Nat.coprime_one_left_eq_true]
  have ha' : orderOf ha.unit = p ^ n := by
    rw [← orderOf_injective _ Units.coeHom_injective ha.unit, Units.coeHom_apply, IsUnit.unit_spec]
    exact orderOf_one_add_prime hp hp2 n
  -- We lift a primitive root of unity mod `p`, an adequate power of which has order `p - 1`.
  obtain ⟨c, hc⟩ := isCyclic_iff_exists_orderOf_eq_natCard.mp (isCyclic_units_prime hp)
  rw [Nat.card_eq_fintype_card, ZMod.card_units] at hc
  obtain ⟨(b : (ZMod (p ^ (n + 1)))ˣ), rfl⟩ :=
    ZMod.unitsMap_surjective (Dvd.intro_left (p ^ n) rfl) c
  have : p - 1 ∣ orderOf b := hc ▸ orderOf_map_dvd _ b
  let k := orderOf b / (p - 1)
  have : orderOf (b ^ k) = p - 1 := orderOf_pow_orderOf_div (orderOf_pos b).ne' this
  rw [isCyclic_iff_exists_orderOf_eq_natCard]
  -- The product of `ha.unit` and `b ^ k` has the required order
  use ha.unit * b ^ k
  rw [(Commute.all _ _).orderOf_mul_eq_mul_orderOf_of_coprime, this, Nat.card_eq_fintype_card,
    ZMod.card_units_eq_totient, Nat.totient_prime_pow_succ hp, ← ha']
  rw [ha', this]
  apply Nat.Coprime.pow_left
  rw [Nat.coprime_self_sub_right hp.pos]
  simp

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

Goal state before:
pp: n : ℕ
hn0 : n ≠ 0
hn1 : n ≠ 1
⊢ ¬(n = 0 ∨ n = 1)

Tactic:
by simp [hn0, hn1]

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

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_2
i : σ
inst✝ : Field R
f : MvPowerSeries σ R
h : ¬constantCoeff f = 0
⊢ (pderiv R i) f⁻¹ = -f⁻¹ ^ 2 * (pderiv R i) f

Tactic:
apply Derivation.leibniz_of_mul_eq_one

Goal state after:
case neg
σ : Type u_1
R : Type u_2
i : σ
inst✝ : Field R
f : MvPowerSeries σ R
h : ¬constantCoeff f = 0
⊢ f⁻¹ * f = 1
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case pos
n : ℕ
h0 : ¬n = 0
h1 : n = 1
⊢ IsCyclic (ZMod n)ˣ ↔ n = 0 ∨ n = 1 ∨ n = 2 ∨ n = 4 ∨ ∃ p m, Nat.Prime p ∧ Odd p ∧ 1 ≤ m ∧ (n = p ^ m ∨ n = 2 * p ^ m)

pp: case neg
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
⊢ IsCyclic (ZMod n)ˣ ↔ n = 0 ∨ n = 1 ∨ n = 2 ∨ n = 4 ∨ ∃ p m, Nat.Prime p ∧ Odd p ∧ 1 ≤ m ∧ (n = p ^ m ∨ n = 2 * p ^ m)

Tactic:
· rw [h1]; simp [isCyclic_units_one]

Goal state after:
case neg
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
⊢ IsCyclic (ZMod n)ˣ ↔ n = 0 ∨ n = 1 ∨ n = 2 ∨ n = 4 ∨ ∃ p m, Nat.Prime p ∧ Odd p ∧ 1 ≤ m ∧ (n = p ^ m ∨ n = 2 * p ^ m)
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case neg.inl
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : ¬n = 2
h4 : ¬n = 4
hn : Odd n
⊢ (∃ p m, Nat.Prime p ∧ Odd p ∧ n = p ^ m) ↔ ∃ x x_1, Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ n = x ^ x_1

Tactic:
congr! with p m

Goal state after:
case neg.inl
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : ¬n = 2
h4 : ¬n = 4
hn : Odd n
p m : ℕ
⊢ n = p ^ m ↔ 1 ≤ m ∧ n = p ^ m
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case neg.inr.inl
n : ℕ
h0 : ¬2 * n = 0
h1 : ¬2 * n = 1
h2 : ¬2 * n = 2
h4 : ¬2 * n = 4
hn✝ : Even (2 * n)
hn : Odd n
⊢ (∃ p m, Nat.Prime p ∧ Odd p ∧ n = p ^ m) ↔ ∃ x x_1, Nat.Prime x ∧ Odd x ∧ 1 ≤ x_1 ∧ 2 * n = 2 * x ^ x_1

Tactic:
congr! with p m

Goal state after:
case neg.inr.inl
n : ℕ
h0 : ¬2 * n = 0
h1 : ¬2 * n = 1
h2 : ¬2 * n = 2
h4 : ¬2 * n = 4
hn✝ : Even (2 * n)
hn : Odd n
p m : ℕ
⊢ n = p ^ m ↔ 1 ≤ m ∧ 2 * n = 2 * p ^ m
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
n_pos : 0 < n
n2_pos : 1 ≤ 2 * n
S : Finset ℕ := {p ∈ Finset.range (2 * n / 3 + 1) | Nat.Prime p}
f : ℕ → ℕ := fun x ↦ x ^ n.centralBinom.factorization x
p : ℕ
x✝ : p ∈ Finset.range (2 * n / 3 + 1)
h : ¬Nat.Prime p
⊢ f p = 1

Tactic:
dsimp only [f]

Goal state after:
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
n_pos : 0 < n
n2_pos : 1 ≤ 2 * n
S : Finset ℕ := {p ∈ Finset.range (2 * n / 3 + 1) | Nat.Prime p}
f : ℕ → ℕ := fun x ↦ x ^ n.centralBinom.factorization x
p : ℕ
x✝ : p ∈ Finset.range (2 * n / 3 + 1)
h : ¬Nat.Prime p
⊢ p ^ n.centralBinom.factorization p = 1
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case neg
k p : ℕ
hk : k > 0
inst✝ : Fact (Nat.Prime p)
hdvd : ¬p - 1 ∣ 2 * k
⊢ ∑ q ∈ vonStaudtPrimes k, 1 / ↑q = vonStaudtIndicator (2 * k) p / ↑p + ∑ q ∈ (vonStaudtPrimes k).erase p, 1 / ↑q

Tactic:
· rw [Finset.erase_eq_of_notMem fun h ↦ hdvd (Finset.mem_filter.mp h).2.2]
    simp [vonStaudtIndicator, hdvd]

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: p d : ℕ
inst✝ : Fact (Nat.Prime p)
hd : d ≥ 2
hcase : ¬(p = 2 ∧ d = 2)
hp2 : 2 ≤ p
n m : ℕ
hm : Nat.le 2 m
IH : ¬(p = 2 ∧ m = 2) → m + 1 ≤ p ^ (m - 1)
hne' : ¬(p = 2 ∧ m.succ = 2)
hm2 : ¬(p = 2 ∧ m = 2)
⊢ m + 1 + 1 ≤ p ^ (m - 1) + 1

Tactic:
linarith [IH hm2]

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hy : 2 ≤ x
⊢ 0 < θ x

Tactic:
by
  refine sum_pos (fun n hn ↦ log_pos ?_) ⟨2, ?_⟩
  · simp only [mem_filter] at hn; exact_mod_cast hn.2.one_lt
  · have : 0 ≤ x := by grind
    simpa using ⟨(le_floor_iff this).2 hy, prime_two⟩

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n : ℕ
⊢ ∑ m ∈ Icc 1 n, Λ m =
    ∑ m ∈ (filter Nat.Prime (Icc 1 n)).biUnion fun p ↦ image (fun x ↦ p ^ x) (Icc 1 (Nat.log p n)), Λ m

Tactic:
by
    refine (sum_subset (fun q hq ↦ ?_) fun x hx ↦ ?_).symm
    · simp only [mem_biUnion, mem_filter, mem_Icc, mem_image] at hq ⊢
      obtain ⟨p, _, k, ⟨_, hk⟩, rfl⟩ := hq
      exact ⟨by grind, pow_le_of_le_log (by linarith) hk⟩
    · simp only [mem_biUnion, mem_filter, mem_Icc, mem_image, not_exists, not_and, and_imp,
        vonMangoldt_eq_zero_iff, isPrimePow_nat_iff]
      contrapose!
      rintro ⟨p, k, hp, hk, rfl⟩
      simp only [mem_Icc] at hx
      have hpn : p ≤ n := (le_of_dvd (by lia) (dvd_pow_self p hk.ne')).trans hx.2
      exact ⟨p, ⟨hp.one_le, hpn, hp, ⟨k, ⟨by lia, le_log_of_pow_le hp.one_lt hx.2, rfl⟩⟩⟩⟩

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

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
a b : ℤ
ha : x - ↑a ∈ Ideal.span {↑p ^ n}
hb : x - ↑b ∈ Ideal.span {↑p ^ n}
⊢ ↑a = ↑b

Tactic:
rw [Ideal.mem_span_singleton] at ha hb

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
a b : ℤ
ha : ↑p ^ n ∣ x - ↑a
hb : ↑p ^ n ∣ x - ↑b
⊢ ↑a = ↑b