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

Goal state before:
pp: case ac
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : IsSetAlgebra 𝒜
S : μ.FiniteSpanningSetsIn 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ∞
ε : ℝ
ε_pos : 0 < ε
T : ℕ → Set X := ⋯
T_mem : ∀ (n : ℕ), T n ∈ 𝒜
T_finite : ∀ (n : ℕ), μ (T n) < ∞
T_spanning : ⋃ n, T n = univ
mono : Monotone fun n ↦ T n ∩ s
this✝ : Filter.Tendsto (fun n ↦ ((⇑μ ∘ fun n ↦ T n ∩ s) n).toReal) Filter.atTop (nhds (μ (⋃ n, T n ∩ s)).toReal)
N : ℕ
hN : ∀ n ≥ N, dist ((⇑μ ∘ fun n ↦ T n ∩ s) n).toReal (μ (⋃ n, T n ∩ s)).toReal < ε / 2
this : Fact (μ (T N) < ∞)
t : Set X
t_mem : t ∈ 𝒜
ht : (μ.restrict (T N)) (s ∆ t) < ENNReal.ofReal (ε / 2)
⊢ μ (s \ (s ∩ T N)) < ENNReal.ofReal (ε / 2)

Tactic:
rw [measure_sdiff
                    (inter_subset_left ..)
                    (ms.inter (hgen ▸ measurableSet_generateFrom (T_mem N))).nullMeasurableSet
                    (ne_top_of_le_ne_top hμs (measure_mono (inter_subset_left ..))),
                  lt_ofReal_iff_toReal_lt (sub_ne_top hμs),
                  toReal_sub_of_le (measure_mono (inter_subset_left ..)) hμs]

Goal state after:
case ac
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : IsSetAlgebra 𝒜
S : μ.FiniteSpanningSetsIn 𝒜
hgen : m = MeasurableSpace.generateFrom 𝒜
s : Set X
ms : MeasurableSet s
hμs : μ s ≠ ∞
ε : ℝ
ε_pos : 0 < ε
T : ℕ → Set X := accumulate S.set
T_mem : ∀ (n : ℕ), T n ∈ 𝒜
T_finite : ∀ (n : ℕ), μ (T n) < ∞
T_spanning : ⋃ n, T n = univ
mono : Monotone fun n ↦ T n ∩ s
this✝ : Filter.Tendsto (fun n ↦ ((⇑μ ∘ fun n ↦ T n ∩ s) n).toReal) Filter.atTop (nhds (μ (⋃ n, T n ∩ s)).toReal)
N : ℕ
hN : ∀ n ≥ N, dist ((⇑μ ∘ fun n ↦ T n ∩ s) n).toReal (μ (⋃ n, T n ∩ s)).toReal < ε / 2
this : Fact (μ (T N) < ∞)
t : Set X
t_mem : t ∈ 𝒜
ht : (μ.restrict (T N)) (s ∆ t) < ENNReal.ofReal (ε / 2)
⊢ (μ s).toReal - (μ (s ∩ T N)).toReal < ε / 2
Module: Mathlib.MeasureTheory.Order.UpperLower

Goal state before:
pp: case neg
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs : IsUpperSet s
x : ι → ℝ
hx : x ∈ frontier s
h : x ∉ closure s
⊢ ¬Tendsto (fun r ↦ volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0) (𝓝 0)

Tactic:
exact aux₀ fun _ ↦ hs.exists_subset_ball <| frontier_subset_closure hx

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

Goal state before:
pp: case neg
ι : Type u_1
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs : IsLowerSet s
x : ι → ℝ
hx : x ∈ frontier s
h : x ∉ closure s
⊢ ¬Tendsto (fun r ↦ volume (closure s ∩ closedBall x r) / volume (closedBall x r)) (𝓝[>] 0) (𝓝 0)

Tactic:
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 : s.OrdConnected
⊢ volume (frontier s) = 0

Tactic:
by
  rw [← hs.upperClosure_inter_lowerClosure]
  exact measure_mono_null (frontier_inter_subset _ _) <| measure_union_null
    (measure_inter_null_of_null_left _ (UpperSet.upper _).null_frontier)
    (measure_inter_null_of_null_right _ (LowerSet.lower _).null_frontier)

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

Goal state before:
pp: case pos
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst✝² : TopologicalSpace V
inst✝¹ : ENormedAddCommMonoid V
inst✝ : T2Space V
μ : VectorMeasure X V
s : Set X
hs : MeasurableSet s
⊢ (μ.restrict s).variation ≤ μ.variation.restrict s

Tactic:
simp [variation_restrict hs]

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

Goal state before:
pp: case pos
α : 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 : α
hf : BoundedVariationOn f univ
ha : IsBot a
h : ∃ x, IsBot x
⊢ hf.vectorMeasure {a} = Function.rightLim f a - Function.leftLim f a

Tactic:
have heqa : h.choose = a := subsingleton_isBot _ h.choose_spec ha

Goal state after:
case pos
α : 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 : α
hf : BoundedVariationOn f univ
ha : IsBot a
h : ∃ x, IsBot x
heqa : h.choose = a
⊢ hf.vectorMeasure {a} = Function.rightLim f a - Function.leftLim f a
Module: Mathlib.MeasureTheory.VectorMeasure.SetIntegral

Goal state before:
pp: X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
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
inst✝ : CompleteSpace G
a : X
hf : StronglyMeasurable f
⊢ ∫ᵛ (a : X) in {a}, f a ∂[B; μ] = (B (f a)) (μ {a})

Tactic:
simp only [restrict_singleton, integral_dirac' hf]

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

Goal state before:
pp: X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
μ : VectorMeasure X F
f : X → E
s t : Set X
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
hs : MeasurableSet s
ht : MeasurableSet t
ht_eq : ∀ᵐ (x : X) ∂μ.variation.restrict t, f x = 0
⊢ (s ∪ t).indicator f =ᵐ[μ.variation] s.indicator f

Tactic:
ae_restrict_iff' ht

Goal state after:
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
s t : Set X
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
hs : MeasurableSet s
ht : MeasurableSet t
ht_eq : ∀ᵐ (x : X) ∂μ.variation, x ∈ t → f x = 0
⊢ (s ∪ t).indicator f =ᵐ[μ.variation] s.indicator f
Module: Mathlib.MeasureTheory.VectorMeasure.SetIntegral

Goal state before:
pp: X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
μ : VectorMeasure X F
f : X → E
s t : Set X
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
hs : MeasurableSet s
ht : MeasurableSet t
ht_eq : ∀ x ∈ t, f x = 0
⊢ ∀ᵐ (x : X) ∂μ.variation.restrict t, f x = 0

Tactic:
ae_restrict_iff' ht

Goal state after:
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
s t : Set X
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
hs : MeasurableSet s
ht : MeasurableSet t
ht_eq : ∀ x ∈ t, f x = 0
⊢ ∀ᵐ (x : X) ∂μ.variation, x ∈ t → f x = 0
Module: Mathlib.MeasureTheory.VectorMeasure.SetIntegral

Goal state before:
pp: case pos
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
s : Set X
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
C : ℝ
h : IsFiniteMeasure (μ.restrict s).variation
hC : ∀ᵐ (x : X) ∂(μ.restrict s).variation, ‖f x‖ ≤ C
hs : MeasurableSet s
⊢ C * ‖B‖ * (μ.restrict s).variation.real univ = C * ‖B‖ * μ.variation.real s

Tactic:
simp [variation_restrict hs]

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

Goal state before:
pp: case inr
S : Finset (Set ℕ)
hS : ∀ t ∈ S, IsProperLinearSet t
a b : ℕ
ht : LinearIndepOn ℕ id ↑{b}
hb : b ≠ 0
⊢ ∃ k, ∃ p > 0, ∀ x ≥ k, x ∈ a +ᵥ ↑(closure ↑{b}) ↔ x + p ∈ a +ᵥ ↑(closure ↑{b})

Tactic:
rw [Nat.ne_zero_iff_zero_lt] at hb

Goal state after:
case inr
S : Finset (Set ℕ)
hS : ∀ t ∈ S, IsProperLinearSet t
a b : ℕ
ht : LinearIndepOn ℕ id ↑{b}
hb : 0 < b
⊢ ∃ k, ∃ p > 0, ∀ x ≥ k, x ∈ a +ᵥ ↑(closure ↑{b}) ↔ x + p ∈ a +ᵥ ↑(closure ↑{b})
Module: Mathlib.MeasureTheory.VectorMeasure.SetIntegral

Goal state before:
pp: case refine_3
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✝
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F✝
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F✝ →L[ℝ] G
ι : Type u_7
f : X → E
hfi : AEStronglyMeasurable f μ.variation
F : ι → X → E
l : Filter ι
hFi : ∀ᶠ (i : ι) in l, μ.Integrable (F i)
hF : Tendsto (fun i ↦ ∫⁻ (x : X), ‖F i x - f x‖ₑ ∂μ.variation) l (𝓝 0)
s : Set X
⊢ Tendsto (fun i ↦ ∫⁻ (x : X), ‖F i x - f x‖ₑ ∂(μ.restrict s).variation) l (𝓝 0)

Tactic:
· simp_rw [← eLpNorm_one_eq_lintegral_enorm] at hF ⊢
    apply tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds hF (fun _ ↦ zero_le)
      (fun i ↦ ?_)
    apply eLpNorm_mono_measure
    grw [variation_restrict_le]
    apply Measure.restrict_le_self

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 : X → E
μ ν : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
h₁ : μ.Integrable f
h₂ : ν.Integrable f
⊢ ↑(nndist ∫ᵛ (x : X), f x ∂[B; μ] ∫ᵛ (x : X), f x ∂[B; μ + ν]) ≤ ‖B‖ₑ * ∫⁻ (x : X), ‖f x‖ₑ ∂ν.variation

Tactic:
integral_add_vectorMeasure h₁ h₂,

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
h₁ : μ.Integrable f
h₂ : ν.Integrable f
⊢ ↑(nndist ∫ᵛ (x : X), f x ∂[B; μ] (∫ᵛ (x : X), f x ∂[B; μ] + ∫ᵛ (x : X), f x ∂[B; ν])) ≤
    ‖B‖ₑ * ∫⁻ (x : X), ‖f x‖ₑ ∂ν.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
h₁ : μ.Integrable f
h₂ : ν.Integrable f
⊢ ↑(nndist (∫ᵛ (x : X), f x ∂[B; μ] + ∫ᵛ (x : X), f x ∂[B; ν]) ∫ᵛ (x : X), f x ∂[B; μ]) ≤
    ‖B‖ₑ * ∫⁻ (x : X), ‖f x‖ₑ ∂ν.variation

Tactic:
nndist_eq_nnnorm,

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
h₁ : μ.Integrable f
h₂ : ν.Integrable f
⊢ ↑‖∫ᵛ (x : X), f x ∂[B; μ] + ∫ᵛ (x : X), f x ∂[B; ν] - ∫ᵛ (x : X), f x ∂[B; μ]‖₊ ≤
    ‖B‖ₑ * ∫⁻ (x : X), ‖f x‖ₑ ∂ν.variation
Module: Mathlib.MeasureTheory.VectorMeasure.Integral

Goal state before:
pp: case pos
X : Type u_2
E : Type u_4
F : Type u_5
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
μ : VectorMeasure X F
β : Type u_10
inst✝ : MeasurableSpace β
φ : X → β
f : β → E
hfm : AEStronglyMeasurable f (Measure.map φ μ.variation)
h : Integrable (f ∘ φ) μ.variation
hφ : Measurable φ
⊢ Integrable f (μ.map φ).variation

Tactic:
apply ((integrable_map_measure hfm hφ.aemeasurable).2 h).mono_measure

Goal state after:
case pos
X : Type u_2
E : Type u_4
F : Type u_5
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
μ : VectorMeasure X F
β : Type u_10
inst✝ : MeasurableSpace β
φ : X → β
f : β → E
hfm : AEStronglyMeasurable f (Measure.map φ μ.variation)
h : Integrable (f ∘ φ) μ.variation
hφ : Measurable φ
⊢ (μ.map φ).variation ≤ Measure.map φ μ.variation
Module: Mathlib.ModelTheory.Equivalence

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

Tactic:
simp only [BoundedFormula.realize_imp, BoundedFormula.realize_inf]
  exact fun h => ⟨h₁ M v xs h, h₂ M v xs h⟩

Goal state after:
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: L : Language
M : Type u_1
inst✝ : L.Structure M
S : L.Substructure M
⊢ S.FG ↔ Structure.FG L ↥S

Tactic:
Structure.fg_def

Goal state after:
L : Language
M : Type u_1
inst✝ : L.Structure M
S : L.Substructure M
⊢ S.FG ↔ ⊤.FG
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 : ℕ
F : L.Functions 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
⊢ Structure.Sigma.mk f i (funMap F (unify f x i hi)) ≈ Structure.Sigma.mk f j (funMap F (unify f x j hj))

Tactic:
refine ⟨k, ik, jk, ?_⟩

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 : ℕ
F : L.Functions 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
⊢ (f i k ik) (funMap F (unify f x i hi)) = (f j k jk) (funMap F (unify f x j hj))
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case mp.refine_1
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
y : ι → ℕ
hy : y ∈ closure hs.periods
⊢ hs.fract hs.base = hs.base

pp: case mp.refine_1
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
y : ι → ℕ
hy : y ∈ closure hs.periods
⊢ y ∈ closure hs.basisSet

Tactic:
hs.fract_base

Goal state after:
case mp.refine_1
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
y : ι → ℕ
hy : y ∈ closure hs.periods
⊢ hs.base = hs.base

case mp.refine_1
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
y : ι → ℕ
hy : y ∈ closure hs.periods
⊢ y ∈ closure hs.basisSet
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case mpr.refine_1
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
i : ↑hs.basisSet
y : ι → ℕ
hy : y ∈ closure {↑i}
z : ι → ℕ
hz : z ∈ closure (hs.basisSet \ {↑i})
z' : ι → ℕ
hz' : z' ∈ closure (hs.basisSet \ {↑i})
heq : hs.fract x = hs.fract hs.base
⊢ hs.fract x = hs.base

Tactic:
hs.fract_base

Goal state after:
case mpr.refine_1
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
i : ↑hs.basisSet
y : ι → ℕ
hy : y ∈ closure {↑i}
z : ι → ℕ
hz : z ∈ closure (hs.basisSet \ {↑i})
z' : ι → ℕ
hz' : z' ∈ closure (hs.basisSet \ {↑i})
heq : hs.fract x = hs.base
⊢ hs.fract x = hs.base
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case mpr.refine_1
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
i : ↑hs.basisSet
hi : ↑i ∉ hs.periods
y : ι → ℕ
hy : y ∈ closure {↑i}
z : ι → ℕ
hz : z ∈ closure (hs.basisSet \ {↑i})
z' : ι → ℕ
hz' : z' ∈ closure (hs.basisSet \ {↑i})
heq : hs.fract x = hs.fract hs.base
⊢ hs.fract x = hs.base

Tactic:
hs.fract_base

Goal state after:
case mpr.refine_1
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
i : ↑hs.basisSet
hi : ↑i ∉ hs.periods
y : ι → ℕ
hy : y ∈ closure {↑i}
z : ι → ℕ
hz : z ∈ closure (hs.basisSet \ {↑i})
z' : ι → ℕ
hz' : z' ∈ closure (hs.basisSet \ {↑i})
heq : hs.fract x = hs.base
⊢ hs.fract x = hs.base
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: case mpr.refine_1
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
i : ↑hs.basisSet
hi : ↑i ∉ hs.periods
y : ι → ℕ
hy : y ∈ closure {↑i}
z : ι → ℕ
hz : z ∈ closure (hs.basisSet \ {↑i})
z' : ι → ℕ
hz' : z' ∈ closure (hs.basisSet \ {↑i})
heq : x + z' = hs.base + ↑i + y + z
⊢ hs.fract x = hs.base

pp: case mpr.refine_2
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
i : ↑hs.basisSet
hi : ↑i ∉ hs.periods
y : ι → ℕ
hy : y ∈ closure {↑i}
z : ι → ℕ
hz : z ∈ closure (hs.basisSet \ {↑i})
z' : ι → ℕ
hz' : z' ∈ closure (hs.basisSet \ {↑i})
heq : x + z' = hs.base + ↑i + y + z
⊢ 0 < hs.floor x i

Tactic:
· apply congr_arg hs.fract at heq
        rwa [hs.fract_add_of_mem_closure (closure_mono sdiff_subset hz'),
          hs.fract_add_of_mem_closure (closure_mono sdiff_subset hz),
          hs.fract_add_of_mem_closure (closure_mono (singleton_subset_iff.2 i.2) hy),
          hs.fract_add_of_mem_closure (mem_closure_of_mem i.2), hs.fract_base] at heq

Goal state after:
case mpr.refine_2
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
i : ↑hs.basisSet
hi : ↑i ∉ hs.periods
y : ι → ℕ
hy : y ∈ closure {↑i}
z : ι → ℕ
hz : z ∈ closure (hs.basisSet \ {↑i})
z' : ι → ℕ
hz' : z' ∈ closure (hs.basisSet \ {↑i})
heq : x + z' = hs.base + ↑i + y + z
⊢ 0 < hs.floor x i
Module: Mathlib.ModelTheory.Topology.Types

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

Tactic:
intro φ
      simp only [mem_ofPred_eq, typesWith_not]
      exact Ultrafilter.mem_or_compl_mem F (T.typesWith φ)

Goal state after:
Module: Mathlib.Topology.Order.IsLocallyClosed

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
a b : X
inst✝¹ : LinearOrder X
inst✝ : ClosedIciTopology X
⊢ IsLocallyClosed (Set.Iio b ∩ Set.Ici a)

Tactic:
exact isLocallyClosed_Iio.inter isLocallyClosed_Ici

Goal state after:
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: p q r : ℕ+
hs : [p, q, r].SortedLE
x✝ : [p, q, r].length = 3
H : 1 < sumInv ↑[p, q, r]
⊢ (p ≤ q ∧ p ≤ r) ∧ q ≤ r

Tactic:
simpa using hs.pairwise

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 * x) ^ i * ↑(p.choose i) = (u * x) ^ (2 + (i - 2)) * ↑(p.choose i)

Tactic:
by rw [Nat.add_sub_of_le hi']

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

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

pp: p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
a : ℤ
ha : ¬↑p ∣ a
n : ℕ
⊢ 1 + 2 ≤ p * 1

Tactic:
· rw [pow_one]

Goal state after:
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
a : ℤ
ha : ¬↑p ∣ a
n : ℕ
⊢ 1 + 2 ≤ p * 1
Module: Mathlib.RingTheory.PowerSeries.Derivative

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : R⟦X⟧
n : ℕ
⊢ (trunc n) ((d⁄dX R) f) = Polynomial.derivative ((trunc (n + 1)) f)

Tactic:
by
  ext d
  rw [coeff_trunc]
  split_ifs with h
  · have : d + 1 < n + 1 := succ_lt_succ_iff.2 h
    rw [coeff_derivative, Polynomial.coeff_derivative, coeff_trunc, if_pos this]
  · have : ¬d + 1 < n + 1 := by rwa [succ_lt_succ_iff]
    rw [Polynomial.coeff_derivative, coeff_trunc, if_neg this, zero_mul]

Goal state after:
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: n p : ℕ
⊢ p ∈ n.primesBelow ↔ p ∈ filter Prime (Ico 1 n)

Tactic:
simp +contextual [primesBelow_eq_filter_range, Nat.Prime.one_le]

Goal state after:
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: n : ℕ
⊢ ∑ k ∈ range (n + 1), ↑((n + 1).choose k) • bernoulli k = (monomial n) (↑n + 1)

Tactic:
by
  simp_rw [bernoulli_def, Finset.smul_sum, Finset.range_eq_Ico, ← Finset.sum_Ico_Ico_comm,
    Finset.sum_Ico_eq_sum_range]
  simp only [add_tsub_cancel_left, zero_add, map_add]
  simp_rw [smul_monomial, mul_comm (_root_.bernoulli _) _, smul_eq_mul, ← mul_assoc]
  conv_lhs =>
    apply_congr
    · skip
    · conv =>
      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]
  simp_rw [← sum_smul, Nat.sub_zero]
  rw [sum_range_succ_comm]
  simp only [add_eq_left, mul_one, cast_one, cast_add, add_tsub_cancel_left,
    choose_succ_self_right, one_smul, _root_.bernoulli_zero, sum_singleton, zero_add,
    map_add, range_one, mul_one]
  refine sum_eq_zero ?_
  intro x hx
  have hx1 : n + 1 - x ≠ 1 := by grind
  simp [_root_.sum_bernoulli, hx1]

Goal state after:
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: case h.succ.inr
n : ℕ
ihn : ∀ m < n + 1, m ≠ 0 → m# < 4 ^ m
hn : n + 1 ≠ 0
ho : Odd n
⊢ (n + 1)# < 4 ^ (n + 1)

Tactic:
rcases Decidable.eq_or_ne n 1 with rfl | hn
    · decide
    · calc
        (n + 1)# = n# := primorial_succ hn ho
        _ < 4 ^ n := ihn n n.lt_succ_self (by grind)
        _ ≤ 4 ^ (n + 1) := Nat.pow_le_pow_right four_pos n.le_succ

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: p M N : ℕ
inst✝ : Fact (Nat.Prime p)
hM : M ≠ 0
e : ℕ := M.factorization p
hv : e ≤ N
M' : ℕ := M / p ^ e
hM'_cop : M'.Coprime p
hp_ne : ↑p ≠ 0
hdecomp : p ^ e * M' = M
hM_eq : ↑M = ↑(p ^ e) * ↑M'
⊢ ↑p ^ N / (↑p ^ e * ↑M') = ↑p ^ (N - e) / ↑M'

Tactic:
div_mul_eq_div_div

Goal state after:
p M N : ℕ
inst✝ : Fact (Nat.Prime p)
hM : M ≠ 0
e : ℕ := M.factorization p
hv : e ≤ N
M' : ℕ := M / p ^ e
hM'_cop : M'.Coprime p
hp_ne : ↑p ≠ 0
hdecomp : p ^ e * M' = M
hM_eq : ↑M = ↑(p ^ e) * ↑M'
⊢ ↑p ^ N / ↑p ^ e / ↑M' = ↑p ^ (N - e) / ↑M'
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: p M N : ℕ
inst✝ : Fact (Nat.Prime p)
hM : M ≠ 0
e : ℕ := M.factorization p
hv : e ≤ N
M' : ℕ := M / p ^ e
hM'_cop : M'.Coprime p
hp_ne : ↑p ≠ 0
hdecomp : p ^ e * M' = M
hM_eq : ↑M = ↑(p ^ e) * ↑M'
hrw : ↑p ^ N / ↑M = ↑p ^ (N - e) / ↑M'
hM'_eq : ↑p ^ (N - e) / ↑M' = Rat.divInt (↑p ^ (N - e)) ↑M'
⊢ (↑p ^ (N - e) / ↑M').den ∣ M'

Tactic:
rw [hM'_eq]; exact Int.natCast_dvd_natCast.mp (Rat.den_dvd _ _)

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: k m : ℕ
x : ℚ
hm_lt : m < k
⊢ ↑((2 * k + 1).choose (2 * m)) * x * (2 * ↑k - 2 * ↑m + 1) = ↑((2 * k).choose (2 * m)) * x * (2 * ↑k + 1)

Tactic:
mul_right_comm _ x,

Goal state after:
k m : ℕ
x : ℚ
hm_lt : m < k
⊢ ↑((2 * k + 1).choose (2 * m)) * (2 * ↑k - 2 * ↑m + 1) * x = ↑((2 * k).choose (2 * m)) * x * (2 * ↑k + 1)
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: n : ℕ
⊢ ∑ p ∈ Icc 1 n with Nat.Prime p, ∑ q ∈ image (fun k ↦ p ^ k) (Icc 1 (Nat.log p n)), Λ q =
    ∑ p ∈ n.primesLE, ∑ k ∈ Icc 1 (Nat.log p n), Λ (p ^ k)

Tactic:
refine sum_congr (primesLE_eq_filter_Icc_one n).symm fun p hp ↦ ?_
      exact sum_image fun a _ b _ hab ↦ Nat.pow_right_injective (two_le_of_mem_primesLE hp) hab

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
⊢ ∑ k ∈ Icc 1 N, ∑ p ∈ Ioc 0 ⌊x ^ (1 / ↑k)⌋₊ with Nat.Prime p, log ↑(p ^ k).minFac = ∑ n ∈ Icc 1 N, θ (x ^ (1 / ↑n))

Tactic:
apply sum_congr rfl fun _ hk ↦ sum_congr rfl fun _ _ ↦ ?_

Goal state after:
x : ℝ
hx : 0 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
x✝² : ℕ
hk : x✝² ∈ Icc 1 N
x✝¹ : ℕ
x✝ : x✝¹ ∈ {p ∈ Ioc 0 ⌊x ^ (1 / ↑x✝²)⌋₊ | Nat.Prime p}
⊢ log ↑(x✝¹ ^ x✝²).minFac = log ↑x✝¹