mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.VectorMeasure.AddContent

Goal state before:
pp: case refine_1
α : 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α
m'' : VectorMeasure α E :=
  { measureOf' := fun s ↦ if MeasurableSet s then ∫ᵛ (x : α), μ[s.indicator 1 | M] x ∂•m' else 0, empty' := ⋯,
    not_measurable' := ⋯, m_iUnion' := ⋯ }
s : Set α
hs : s ∈ C
⊢ m'' s = m s

Tactic:
simp only [coe_mk, h'C s hs, ↓reduceIte, m'']

Goal state after:
case refine_1
α : 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α
m'' : VectorMeasure α E :=
  { measureOf' := fun s ↦ if MeasurableSet s then ∫ᵛ (x : α), μ[s.indicator 1 | M] x ∂•m' else 0, empty' := ⋯,
    not_measurable' := ⋯, m_iUnion' := ⋯ }
s : Set α
hs : s ∈ C
⊢ ∫ᵛ (x : α), μ[s.indicator 1 | M] x ∂•m' = m s
Module: Mathlib.MeasureTheory.VectorMeasure.Variation.SignedMeasure

Goal state before:
pp: case a
X : Type u_1
mX : MeasurableSpace X
μ : SignedMeasure X
r : Set X
hr : MeasurableSet r
⊢ (VectorMeasure.variation μ) r ≤ μ.totalVariation r

Tactic:
· apply VectorMeasure.variation_le_of_forall_enorm_le
    exact fun s _ ↦ enorm_le_totalVariation μ s

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

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
S₁ : Set (Set M)
hS₁ : S₁.Finite
hS₁' : ∀ t ∈ S₁, IsLinearSet t
S₂ : Set (Set M)
hS₂ : S₂.Finite
hS₂' : ∀ t ∈ S₂, IsLinearSet t
⊢ IsSemilinearSet (⋃₀ S₁ + ⋃₀ S₂)

Tactic:
sUnion_add,

Goal state after:
M : Type u_1
inst✝ : AddCommMonoid M
S₁ : Set (Set M)
hS₁ : S₁.Finite
hS₁' : ∀ t ∈ S₁, IsLinearSet t
S₂ : Set (Set M)
hS₂ : S₂.Finite
hS₂' : ∀ t ∈ S₂, IsLinearSet t
⊢ IsSemilinearSet (⋃ s ∈ S₁, s + ⋃₀ S₂)
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
f : X → E
c : ℝ
hG : CompleteSpace G
this✝ : (c • μ).variation = ‖c‖₊ • μ.variation
this : DominatedFinMeasAdditive μ.variation (⇑((c • μ).transpose B)) (‖c‖ * ‖B‖)
⊢ (setToFun (‖c‖₊ • μ.variation) ⇑((c • μ).transpose B) ⋯ fun x ↦ f x) =
    setToFun μ.variation (fun s ↦ c • (μ.transpose B) s) ⋯ fun x ↦ f x

Tactic:
← setToFun_congr_smul_measure' _ this,

Goal state after:
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
f : X → E
c : ℝ
hG : CompleteSpace G
this✝ : (c • μ).variation = ‖c‖₊ • μ.variation
this : DominatedFinMeasAdditive μ.variation (⇑((c • μ).transpose B)) (‖c‖ * ‖B‖)
⊢ (setToFun μ.variation (⇑((c • μ).transpose B)) this fun x ↦ f x) =
    setToFun μ.variation (fun s ↦ c • (μ.transpose B) s) ⋯ fun x ↦ f x
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs

Goal state before:
pp: case pos
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : IsCancelAdd M
a : M
t : Finset M
ih : ∀ m < t.card, ∀ (a : M) (t : Finset M), t.card = m → IsProperSemilinearSet (a +ᵥ ↑(closure ↑t))
t' : Finset M
ht' : t' ⊆ t
f : M → ℕ
i : M
hi : i ∈ t'
hfi : 0 < f i
heq : ∑ x ∈ t', f x • x = ∑ x ∈ t \ t', f x • x
g : M → ℕ
ih' :
  ∀ m < g i,
    ∀ (g : M → ℕ),
      g i = m → a +ᵥ ∑ a ∈ t, g a • a ∈ ⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ ↑(closure ↑(t.erase j))
hfg : ∀ j ∈ t', f j ≤ g j
⊢ a +ᵥ ∑ a ∈ t, g a • a ∈ ⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ ↑(closure ↑(t.erase j))

Tactic:
convert!
        ih' (g i - f i) (Nat.sub_lt_self hfi (hfg i hi))
          (fun j => if j ∈ t' then g j - f j else g j + f j) (by simp [hi]) using 1

Goal state after:
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : IsCancelAdd M
a : M
t : Finset M
ih : ∀ m < t.card, ∀ (a : M) (t : Finset M), t.card = m → IsProperSemilinearSet (a +ᵥ ↑(closure ↑t))
t' : Finset M
ht' : t' ⊆ t
f : M → ℕ
i : M
hi : i ∈ t'
hfi : 0 < f i
heq : ∑ x ∈ t', f x • x = ∑ x ∈ t \ t', f x • x
g : M → ℕ
ih' :
  ∀ m < g i,
    ∀ (g : M → ℕ),
      g i = m → a +ᵥ ∑ a ∈ t, g a • a ∈ ⋃ j ∈ t', ⋃ k ∈ Finset.range (f j), (a + k • j) +ᵥ ↑(closure ↑(t.erase j))
hfg : ∀ j ∈ t', f j ≤ g j
⊢ a +ᵥ ∑ a ∈ t, g a • a = a +ᵥ ∑ a ∈ t, (if a ∈ t' then g a - f a else g a + f a) • 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✝
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 ↦ eLpNorm (F i - f) 1 μ.variation) l (𝓝 0)
s : Set X
⊢ Tendsto (fun i ↦ ∫ᵛ (x : X) in s, F i x ∂[B; μ]) l (𝓝 ∫ᵛ (x : X) in s, f x ∂[B; μ])

Tactic:
refine tendsto_setIntegral_of_L1 f hfi hFi ?_ s

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✝
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 ↦ eLpNorm (F i - f) 1 μ.variation) l (𝓝 0)
s : Set X
⊢ Tendsto (fun i ↦ ∫⁻ (x : X), ‖F i x - f x‖ₑ ∂μ.variation) l (𝓝 0)
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
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
β : Type u_9
inst✝ : MeasurableSpace β
φ : X → β
⊢ ((μ.map φ).transpose B).variation ≤ Measure.map φ (μ.transpose B).variation

Tactic:
transpose_map,

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
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
β : Type u_9
inst✝ : MeasurableSpace β
φ : X → β
⊢ ((μ.transpose B).map φ).variation ≤ Measure.map φ (μ.transpose B).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
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
β : Type u_9
inst✝ : MeasurableSpace β
φ : X → β
hφ : MeasurableEmbedding φ
⊢ ((μ.map φ).transpose B).variation = Measure.map φ (μ.transpose B).variation

Tactic:
transpose_map,

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
μ : VectorMeasure X F
B : E →L[ℝ] F →L[ℝ] G
β : Type u_9
inst✝ : MeasurableSpace β
φ : X → β
hφ : MeasurableEmbedding φ
⊢ ((μ.transpose B).map φ).variation = Measure.map φ (μ.transpose B).variation
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability

Goal state before:
pp: A s : Set ℕ
⊢ A.Definable₁ presburger s ↔ ∃ k, ∃ p > 0, ∀ x ≥ k, x ∈ s ↔ x + p ∈ s

Tactic:
Definable₁,

Goal state after:
A s : Set ℕ
⊢ A.Definable presburger {x | x 0 ∈ s} ↔ ∃ k, ∃ p > 0, ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
Module: Mathlib.ModelTheory.FinitelyGenerated

Goal state before:
pp: L : Language
M : Type u_1
inst✝ : L.Structure M
⊢ CG L M ↔ ∃ S, S.Countable ∧ (closure L).toFun S = ⊤

Tactic:
by
  rw [cg_def, Substructure.cg_def]

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

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
t : Finset (ι → ℕ)
hs : ∀ (f g : (ι → ℕ) → ℕ), ∑ i ∈ t, f i • id i = ∑ i ∈ t, g i • id i → ∀ i ∈ t, f i = g i
f : (ι → ℕ) → ℤ
ht : ↑t ⊆ s
hf : ∀ i ∉ t, f i = 0
heq : ∑ i ∈ t, f i • toRatVec i = 0
i : ι → ℕ
hi : i ∈ t
⊢ ∑ i ∈ t, (Int.toNat ∘ f) i • id i = ∑ i ∈ t, (Int.toNat ∘ (fun x ↦ -x) ∘ f) i • id i

Tactic:
simp_rw [← toRatVec_inj, map_sum]
    rw [← sub_eq_zero, ← Finset.sum_sub_distrib, ← heq]
    refine Finset.sum_congr rfl fun j hj => ?_
    conv_rhs => rw [← (f j).toNat_sub_toNat_neg]
    simp only [sub_smul, map_nsmul, natCast_zsmul, Function.comp_apply, id_eq]

Goal state after:
Module: Mathlib.ModelTheory.Types

Goal state before:
pp: L : Language
T : L.Theory
α : Type w
S : L[[α]].Theory
⊢ {p | S ⊆ ↑p} = ∅ ↔ ¬((L.lhomWithConstants α).onTheory T ∪ S).IsSatisfiable

Tactic:
rw [iff_not_comm, ← not_nonempty_iff_eq_empty, Classical.not_not, Set.Nonempty]
  refine
    ⟨fun h =>
      ⟨⟨L[[α]].completeTheory h.some, (subset_union_left (t := S)).trans completeTheory.subset,
          completeTheory.isMaximal L[[α]] h.some⟩,
        (((L.lhomWithConstants α).onTheory T).subset_union_right).trans completeTheory.subset⟩,
      ?_⟩
  rintro ⟨p, hp⟩
  exact p.isMaximal.1.mono (union_subset p.subset hp)

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

Goal state before:
pp: case h
X : Type u_1
inst✝² : TopologicalSpace X
s : Set X
inst✝¹ : R1Space X
inst✝ : LocallyCompactSpace X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
U : Set X
U_open : IsOpen U
U_nonempty : U.Nonempty
K₀ : PositiveCompacts X
hK₀ : closure ↑K₀ ⊆ U
K_next : ℕ → PositiveCompacts X → PositiveCompacts X
hK_next : ∀ (n : ℕ) (K : PositiveCompacts X), closure ↑(K_next n K) ⊆ f n ∩ interior ↑K
⊢ (∀ (n : ℕ), (fun t ↦ Nat.rec K₀ K_next t) (n + 1) ≤ (fun t ↦ Nat.rec K₀ K_next t) n) ∧
    (∀ (n : ℕ), closure ↑((fun t ↦ Nat.rec K₀ K_next t) (n + 1)) ⊆ f n) ∧ closure ↑((fun t ↦ Nat.rec K₀ K_next t) 0) ⊆ U

Tactic:
refine ⟨fun n ↦ ?_, fun n ↦ (hK_next n _).trans inter_subset_left, hK₀⟩

Goal state after:
case h
X : Type u_1
inst✝² : TopologicalSpace X
s : Set X
inst✝¹ : R1Space X
inst✝ : LocallyCompactSpace X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
U : Set X
U_open : IsOpen U
U_nonempty : U.Nonempty
K₀ : PositiveCompacts X
hK₀ : closure ↑K₀ ⊆ U
K_next : ℕ → PositiveCompacts X → PositiveCompacts X
hK_next : ∀ (n : ℕ) (K : PositiveCompacts X), closure ↑(K_next n K) ⊆ f n ∩ interior ↑K
n : ℕ
⊢ (fun t ↦ Nat.rec K₀ K_next t) (n + 1) ≤ (fun t ↦ Nat.rec K₀ K_next t) n
Module: Mathlib.RingTheory.MvPowerSeries.Derivative

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : Semiring R
i : σ
r : R
n : σ →₀ ℕ
⊢ (coeff n) (pderivFun i (C r)) = (coeff n) 0

Tactic:
rw [coeff_pderivFun, coeff_add_single_C, zero_mul, (coeff n).map_zero]

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

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
f g : MvPowerSeries σ R
n : σ →₀ ℕ
h₁ : n < n + single i 1
h₂ : n + single i 1 < n + single i 1 + single i 1
h₃ : n < n + single i 1 + single i 1
⊢ (coeff (n + single i 1))
        (↑((trunc R (n + single i 1 + single i 1)) f) * ↑((trunc R (n + single i 1 + single i 1)) g)) *
      (↑(n i) + 1) =
    (coeff n)
      (pderivFun i (↑((trunc R (n + single i 1 + single i 1)) f) * ↑((trunc R (n + single i 1 + single i 1)) g)))

Tactic:
coeff_pderivFun

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
f g : MvPowerSeries σ R
n : σ →₀ ℕ
h₁ : n < n + single i 1
h₂ : n + single i 1 < n + single i 1 + single i 1
h₃ : n < n + single i 1 + single i 1
⊢ (coeff (n + single i 1))
        (↑((trunc R (n + single i 1 + single i 1)) f) * ↑((trunc R (n + single i 1 + single i 1)) g)) *
      (↑(n i) + 1) =
    (coeff (n + single i 1))
        (↑((trunc R (n + single i 1 + single i 1)) f) * ↑((trunc R (n + single i 1 + single i 1)) g)) *
      (↑(n i) + 1)
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‖₊ = ‖x‖₊ * ‖y‖₊
⊢ (μ.withDensity f B).variation = (μ.transpose B).variation.withDensity fun x ↦ ‖f x‖ₑ

Tactic:
by
  apply variation_withDensity' hf (fun x y ↦ ?_)
  refine le_antisymm (ContinuousLinearMap.le_opNorm (B.flip y) x) ?_
  rw [hB, mul_comm]
  gcongr
  apply ContinuousLinearMap.opNNNorm_le_bound
  simp [hB, mul_comm]

Goal state after:
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
n m : ℕ
h : n ≤ m
hf_diff : ∀ t ∈ Set.Icc ↑n ↑m, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc ↑n ↑m) volume
⊢ ∑ k ∈ Ioc n m, f ↑k * c k =
    f ↑m * ∑ k ∈ Icc 0 m, c k - f ↑n * ∑ k ∈ Icc 0 n, c k -
      ∫ (t : ℝ) in Set.Ioc ↑n ↑m, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k

Tactic:
convert! sum_mul_eq_sub_sub_integral_mul c n.cast_nonneg (Nat.cast_le.mpr h) hf_diff hf_int

Goal state after:
case e'_2.h.e'_4
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
n m : ℕ
h : n ≤ m
hf_diff : ∀ t ∈ Set.Icc ↑n ↑m, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc ↑n ↑m) volume
⊢ n = ⌊↑n⌋₊

case e'_2.h.e'_5
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
n m : ℕ
h : n ≤ m
hf_diff : ∀ t ∈ Set.Icc ↑n ↑m, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc ↑n ↑m) volume
⊢ m = ⌊↑m⌋₊

case e'_3.e'_5.h
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
n m : ℕ
h : n ≤ m
hf_diff : ∀ t ∈ Set.Icc ↑n ↑m, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc ↑n ↑m) volume
⊢ m = ⌊↑m⌋₊

case e'_3.e'_6.h
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
n m : ℕ
h : n ≤ m
hf_diff : ∀ t ∈ Set.Icc ↑n ↑m, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc ↑n ↑m) volume
⊢ n = ⌊↑n⌋₊
Module: Mathlib.NumberTheory.PrimeCounting

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

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

Goal state after:
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: ⊢ Monotone primesBelow

Tactic:
intros n m _ p
  simp [mem_primesBelow]; grind

Goal state after:
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: n : ℕ
⊢ n ≤ n#

Tactic:
obtain hn | hn := le_or_gt n 2

Goal state after:
case inl
n : ℕ
hn : n ≤ 2
⊢ n ≤ n#

case inr
n : ℕ
hn : 2 < n
⊢ n ≤ n#
Module: Mathlib.NumberTheory.ClassNumber.Finite

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : EuclideanDomain R
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
inst✝² : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
bS : Basis ι R S
h : ∀ (i j k : ι), (Algebra.leftMulMatrix bS) (bS i) j k = 0
⊢ False

Tactic:
obtain ⟨i⟩ := bS.index_nonempty

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : EuclideanDomain R
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
inst✝² : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
bS : Basis ι R S
h : ∀ (i j k : ι), (Algebra.leftMulMatrix bS) (bS i) j k = 0
i : ι
⊢ False
Module: Mathlib.NumberTheory.ClassNumber.Finite

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : EuclideanDomain R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
bS : Basis ι R S
T : Type u_6
inst✝² : Ring T
inst✝¹ : LinearOrder T
inst✝ : IsStrictOrderedRing T
a : S
y : T
hy : ∀ (k : ι), ↑(abv ((bS.repr a) k)) < y
⊢ ↑(abv ((Algebra.norm R) a)) < ↑(normBound abv bS) * y ^ Fintype.card ι

Tactic:
obtain ⟨i⟩ := bS.index_nonempty

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : EuclideanDomain R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
bS : Basis ι R S
T : Type u_6
inst✝² : Ring T
inst✝¹ : LinearOrder T
inst✝ : IsStrictOrderedRing T
a : S
y : T
hy : ∀ (k : ι), ↑(abv ((bS.repr a) k)) < y
i : ι
⊢ ↑(abv ((Algebra.norm R) a)) < ↑(normBound abv bS) * y ^ Fintype.card ι
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 2 ≤ x
N : ℕ
hN : ⌊log x / log 2⌋₊ ≤ N
⊢ 1 ≤ N

Tactic:
apply le_trans _ hN
    rw [le_floor_iff' one_ne_zero, le_div_iff₀ (by positivity), cast_one, one_mul]
    gcongr

Goal state after:
Module: Mathlib.RingTheory.Adjoin.Polynomial.Bivariate

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
B : Type u_3
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : A
y : B
hx : Transcendental R x
p : R[X][Y]
⊢ (aeval ((algebraMap A B) x)) ((aeval (C ⟨y, ⋯⟩)) p) = (aeval y) ((Transcendental.algEquivAdjoin hx) p)

Tactic:
induction p using Polynomial.induction_on' with

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
| IntegrableOn (fun t ↦ θ t / (t * log t ^ 2)) (Set.Icc 2 x) volume

Tactic:
arg 1

Goal state after:
x : ℝ
| fun t ↦ θ t / (t * log t ^ 2)
Module: Mathlib.NumberTheory.ClassNumber.Finite

Goal state before:
pp: R : Type u_1
S : Type u_2
K : Type u_3
L : Type u_4
inst✝¹⁷ : EuclideanDomain R
inst✝¹⁶ : CommRing S
inst✝¹⁵ : IsDomain S
inst✝¹⁴ : Field K
inst✝¹³ : Field L
inst✝¹² : Algebra R K
inst✝¹¹ : IsFractionRing R K
inst✝¹⁰ : Algebra K L
inst✝⁹ : FiniteDimensional K L
inst✝⁸ : Algebra.IsSeparable K L
algRL : Algebra R L
inst✝⁷ : IsScalarTower R K L
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra S L
ist : IsScalarTower R S L
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝² : Infinite R
inst✝¹ : DecidableEq R
inst✝ : IsIntegralClosure S R L
⊢ Fintype (ClassGroup S)

Tactic:
letI := Classical.decEq L

Goal state after:
R : Type u_1
S : Type u_2
K : Type u_3
L : Type u_4
inst✝¹⁷ : EuclideanDomain R
inst✝¹⁶ : CommRing S
inst✝¹⁵ : IsDomain S
inst✝¹⁴ : Field K
inst✝¹³ : Field L
inst✝¹² : Algebra R K
inst✝¹¹ : IsFractionRing R K
inst✝¹⁰ : Algebra K L
inst✝⁹ : FiniteDimensional K L
inst✝⁸ : Algebra.IsSeparable K L
algRL : Algebra R L
inst✝⁷ : IsScalarTower R K L
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra S L
ist : IsScalarTower R S L
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝² : Infinite R
inst✝¹ : DecidableEq R
inst✝ : IsIntegralClosure S R L
this : DecidableEq L := Classical.decEq L
⊢ Fintype (ClassGroup S)
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
hbε : 0 < cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε
A : Fin (n + 1) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (n + 1)} {ε : ℝ},
    ↑(cardPowDegree (A i % b - A j % b)) < ε →
      ↑(cardPowDegree (A j % b - A k % b)) < ε → ↑(cardPowDegree (A i % b - A k % b)) < ε
t' : Fin n → Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
ht' : ∀ (i₀ i₁ : Fin n), t' i₀ = t' i₁ ↔ ↑(cardPowDegree (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < cardPowDegree b • ε
j✝ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
hj✝ : ∀ (i : Fin n), t' i = j✝ → ↑(cardPowDegree (A 0 % b - A i.succ % b)) < cardPowDegree b • ε
j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
hj : ∀ (i : Fin n), t' i = j → ↑(cardPowDegree (A 0 % b - A i.succ % b)) < cardPowDegree b • ε
i : Fin n
hi : t' i = j
i' : Fin n
hi' : ↑(cardPowDegree (A 0 % b - A i'.succ % b)) < cardPowDegree b • ε
⊢ ↑(cardPowDegree (A i.succ % b - A 0 % b)) < cardPowDegree b • ε

Tactic:
rw [AbsoluteValue.map_sub]

Goal state after:
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
hbε : 0 < cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε
A : Fin (n + 1) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (n + 1)} {ε : ℝ},
    ↑(cardPowDegree (A i % b - A j % b)) < ε →
      ↑(cardPowDegree (A j % b - A k % b)) < ε → ↑(cardPowDegree (A i % b - A k % b)) < ε
t' : Fin n → Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
ht' : ∀ (i₀ i₁ : Fin n), t' i₀ = t' i₁ ↔ ↑(cardPowDegree (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < cardPowDegree b • ε
j✝ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
hj✝ : ∀ (i : Fin n), t' i = j✝ → ↑(cardPowDegree (A 0 % b - A i.succ % b)) < cardPowDegree b • ε
j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
hj : ∀ (i : Fin n), t' i = j → ↑(cardPowDegree (A 0 % b - A i.succ % b)) < cardPowDegree b • ε
i : Fin n
hi : t' i = j
i' : Fin n
hi' : ↑(cardPowDegree (A 0 % b - A i'.succ % b)) < cardPowDegree b • ε
⊢ ↑(cardPowDegree (A 0 % b - A i.succ % b)) < cardPowDegree b • ε
Module: Mathlib.NumberTheory.ClassNumber.Finite

Goal state before:
pp: R : Type u_1
S : Type u_2
K : Type u_3
L : Type u_4
inst✝¹⁷ : EuclideanDomain R
inst✝¹⁶ : CommRing S
inst✝¹⁵ : IsDomain S
inst✝¹⁴ : Field K
inst✝¹³ : Field L
inst✝¹² : Algebra R K
inst✝¹¹ : IsFractionRing R K
inst✝¹⁰ : Algebra K L
inst✝⁹ : FiniteDimensional K L
inst✝⁸ : Algebra.IsSeparable K L
algRL : Algebra R L
inst✝⁷ : IsScalarTower R K L
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra S L
ist : IsScalarTower R S L
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝² : Infinite R
inst✝¹ : DecidableEq R
inst✝ : IsIntegralClosure S R L
this✝² : DecidableEq L := Classical.decEq L
this✝¹ : IsFractionRing S L := IsIntegralClosure.isFractionRing_of_finite_extension R K L S
this✝ : IsDedekindDomain S := IsIntegralClosure.isDedekindDomain R K L S
s : Finset L
b✝ : Basis (↥s) K L
hb_int : ∀ (x : ↥s), IsIntegral R (b✝ x)
this : LinearIndependent R ⇑((Algebra.traceForm K L).dualBasis ⋯ b✝)
n : ℕ
b : Basis (Fin n) R ↥(↑R (Algebra.linearMap S L)).range
⊢ (S ⧸ ⊥) ≃ₗ[R] S

Tactic:
exact Submodule.quotEquivOfEqBot _ rfl

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
a✝ : 4 ≤ x
⊢ IntegrableOn (fun x ↦ θ x / (x * log x ^ 2)) (Set.Icc 2 x) volume

Tactic:
exact integrableOn_theta_div_id_mul_log_sq x

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

Goal state before:
pp: case hb
p : ℕ
hp_prime : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
x : ℤ_[p]
⊢ ↑p ^ m ∣ ↑(x.appr n) - ↑(x.appr m)

Tactic:
rcases dvd_appr_sub_appr x m n h with ⟨c, hc⟩

Goal state after:
case hb
p : ℕ
hp_prime : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
x : ℤ_[p]
c : ℕ
hc : x.appr n - x.appr m = p ^ m * c
⊢ ↑p ^ m ∣ ↑(x.appr n) - ↑(x.appr m)