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

Goal state before:
pp: case pos.h_add
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
H : Type u_6
mX : MeasurableSpace X
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedAddCommGroup H
μ : VectorMeasure X F
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedSpace ℝ G
inst✝ : NormedSpace ℝ H
B : E →L[ℝ] F →L[ℝ] G
f✝ : X → H
C : H →L[ℝ] E
hf✝ : Integrable f✝ μ.variation
hG : CompleteSpace G
f g : X → H
a✝ : Disjoint (support f) (support g)
f_int : Integrable f μ.variation
g_int : Integrable g μ.variation
hf : ∫ᵛ (y : X), C (f y) ∂[B; μ] = ∫ᵛ (y : X), f y ∂[B ∘SL C; μ]
hg : ∫ᵛ (y : X), C (g y) ∂[B; μ] = ∫ᵛ (y : X), g y ∂[B ∘SL C; μ]
⊢ ∫ᵛ (y : X), f y ∂[B ∘SL C; μ] + ∫ᵛ (y : X), g y ∂[B ∘SL C; μ] = ∫ᵛ (y : X), f y + g y ∂[B ∘SL C; μ]

Tactic:
integral_fun_add f_int g_int

Goal state after:
case pos.h_add
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
H : Type u_6
mX : MeasurableSpace X
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedAddCommGroup H
μ : VectorMeasure X F
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedSpace ℝ G
inst✝ : NormedSpace ℝ H
B : E →L[ℝ] F →L[ℝ] G
f✝ : X → H
C : H →L[ℝ] E
hf✝ : Integrable f✝ μ.variation
hG : CompleteSpace G
f g : X → H
a✝ : Disjoint (support f) (support g)
f_int : Integrable f μ.variation
g_int : Integrable g μ.variation
hf : ∫ᵛ (y : X), C (f y) ∂[B; μ] = ∫ᵛ (y : X), f y ∂[B ∘SL C; μ]
hg : ∫ᵛ (y : X), C (g y) ∂[B; μ] = ∫ᵛ (y : X), g y ∂[B ∘SL C; μ]
⊢ ∫ᵛ (y : X), f y ∂[B ∘SL C; μ] + ∫ᵛ (y : X), g y ∂[B ∘SL C; μ] =
    ∫ᵛ (x : X), f x ∂[B ∘SL C; μ] + ∫ᵛ (x : X), g x ∂[B ∘SL C; μ]
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs

Goal state before:
pp: M : Type u_1
N : Type u_2
F : Type u_5
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : FunLike F M N
inst✝ : AddMonoidHomClass F M N
f : F
S : Set (Set M)
hS : S.Finite
hS' : ∀ t ∈ S, IsLinearSet t
⊢ IsSemilinearSet (⇑f '' ⋃₀ S)

Tactic:
simp_rw [sUnion_eq_biUnion, image_iUnion]

Goal state after:
M : Type u_1
N : Type u_2
F : Type u_5
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : FunLike F M N
inst✝ : AddMonoidHomClass F M N
f : F
S : Set (Set M)
hS : S.Finite
hS' : ∀ t ∈ S, IsLinearSet t
⊢ IsSemilinearSet (⋃ i ∈ S, ⇑f '' i)
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 μ.variation (⇑((c • μ).transpose B)) this fun x ↦ f x) =
    setToFun μ.variation (fun s ↦ c • (μ.transpose B) s) ⋯ fun x ↦ f x

Tactic:
transpose_smul

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) ⋯ fun x ↦ f x) =
    setToFun μ.variation (fun s ↦ c • (μ.transpose B) s) ⋯ fun x ↦ f x
Module: Mathlib.MeasureTheory.VectorMeasure.Integral

Goal state before:
pp: case neg
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
le_ae : ∀ᵐ (a : X) ∂μ.variation, 0 ≤ ‖f a‖
h : ¬AEStronglyMeasurable f μ.variation
⊢ ‖∫ᵛ (a : X), f a ∂[B; μ]‖ ≤ ‖B‖ * ∫ (a : X), ‖f a‖ ∂μ.variation

Tactic:
rw [integral_non_aestronglyMeasurable h, norm_zero]
    positivity

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

Goal state before:
pp: M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : IsCancelAdd M
S : Set (Set M)
hS : S.Finite
hS' : ∀ t ∈ S, IsLinearSet t
⊢ IsProperSemilinearSet (⋃₀ S)

Tactic:
sUnion_eq_biUnion

Goal state after:
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : IsCancelAdd M
S : Set (Set M)
hS : S.Finite
hS' : ∀ t ∈ S, IsLinearSet t
⊢ IsProperSemilinearSet (⋃ i ∈ S, i)
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability

Goal state before:
pp: case func.inr.zero
α : Type u_1
A : Set ℕ
inst✝ : Fintype α
ts : Fin 0 → presburger[[↑A]].Term α
ih : ∀ (a : Fin 0), ∃ k u, ∀ (v : α → ℕ), Term.realize v (ts a) = k + u ⬝ᵥ v
f : (constantsOn ↑A).Functions 0
v : α → ℕ
⊢ ↑(presburger.con f) = ↑f + 0 ⬝ᵥ v

Tactic:
zero_dotProduct,

Goal state after:
case func.inr.zero
α : Type u_1
A : Set ℕ
inst✝ : Fintype α
ts : Fin 0 → presburger[[↑A]].Term α
ih : ∀ (a : Fin 0), ∃ k u, ∀ (v : α → ℕ), Term.realize v (ts a) = k + u ⬝ᵥ v
f : (constantsOn ↑A).Functions 0
v : α → ℕ
⊢ ↑(presburger.con f) = ↑f + 0
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability

Goal state before:
pp: case pos
A : Set ℕ
hmul : A.Definable presburger {v | v 0 = v 1 * v 2}
k p : ℕ
hp : p > 0
x : ℕ
h₁ : x * x = max k p * max k p + p
h₂ : x ≤ max k p
⊢ False

Tactic:
apply Nat.mul_self_le_mul_self at h₂

Goal state after:
case pos
A : Set ℕ
hmul : A.Definable presburger {v | v 0 = v 1 * v 2}
k p : ℕ
hp : p > 0
x : ℕ
h₁ : x * x = max k p * max k p + p
h₂ : x * x ≤ max k p * max k p
⊢ False
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Definability

Goal state before:
pp: case neg
A : Set ℕ
hmul : A.Definable presburger {v | v 0 = v 1 * v 2}
k p : ℕ
hp : p > 0
x : ℕ
h₁ : x * x = max k p * max k p + p
h₂ : max k p + 1 ≤ x
⊢ False

Tactic:
apply Nat.mul_self_le_mul_self at h₂

Goal state after:
case neg
A : Set ℕ
hmul : A.Definable presburger {v | v 0 = v 1 * v 2}
k p : ℕ
hp : p > 0
x : ℕ
h₁ : x * x = max k p * max k p + p
h₂ : (max k p + 1) * (max k p + 1) ≤ x * x
⊢ False
Module: Mathlib.ModelTheory.Complexity

Goal state before:
pp: L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α (n + 1)
con : (∀' φ).IsAtomic
⊢ False

Tactic:
cases con

Goal state after:
Module: Mathlib.ModelTheory.Complexity

Goal state before:
pp: L : Language
α : Type u'
n : ℕ
φ : L.BoundedFormula α (n + 1)
con : (∃' φ).IsAtomic
⊢ False

Tactic:
cases con

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 ι
S : L.Substructure (DirectLimit G f)
S_fg : S.FG
A : Finset (DirectLimit G f)
A_closure : (Substructure.closure L).toFun ↑A = S
⊢ ∃ i T, Substructure.map (of L ι G f i).toHom T = S

Tactic:
let ⟨i, y, eq_y⟩ := exists_quotient_mk'_sigma_mk'_eq G _ (fun a : A ↦ a.1)

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 ι
S : L.Substructure (DirectLimit G f)
S_fg : S.FG
A : Finset (DirectLimit G f)
A_closure : (Substructure.closure L).toFun ↑A = S
i : ι
y : ↥A → G i
eq_y : (fun a ↦ ↑a) = fun a ↦ ⟦Structure.Sigma.mk f i (y a)⟧
⊢ ∃ i T, Substructure.map (of L ι G f i).toHom T = S
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: case mp
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
⊢ f = g →
    ∃ (h_dom : f.dom = g.dom),
      ∀ (x : M) (h : x ∈ f.dom), f.cod.subtype (f.toEquiv ⟨x, h⟩) = g.cod.subtype (g.toEquiv ⟨x, ⋯⟩)

pp: case mpr
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
⊢ (∃ (h_dom : f.dom = g.dom),
      ∀ (x : M) (h : x ∈ f.dom), f.cod.subtype (f.toEquiv ⟨x, h⟩) = g.cod.subtype (g.toEquiv ⟨x, ⋯⟩)) →
    f = g

Tactic:
· intro h_eq
    rcases f with ⟨dom_f, cod_f, equiv_f⟩
    cases h_eq
    exact ⟨rfl, fun _ _ ↦ rfl⟩

Goal state after:
case mpr
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
⊢ (∃ (h_dom : f.dom = g.dom),
      ∀ (x : M) (h : x ∈ f.dom), f.cod.subtype (f.toEquiv ⟨x, h⟩) = g.cod.subtype (g.toEquiv ⟨x, ⋯⟩)) →
    f = g
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: ι : Type u_3
inst✝ : Finite ι
S : Set (Set (ι → ℕ))
hS : S.Finite
hS' : ∀ t ∈ S, IsProperLinearSet t
hs : IsSemilinearSet (⋃₀ S)
⊢ IsSemilinearSet (⋃₀ S)ᶜ

Tactic:
simp_rw [sUnion_eq_biUnion, compl_iUnion]

Goal state after:
ι : Type u_3
inst✝ : Finite ι
S : Set (Set (ι → ℕ))
hS : S.Finite
hS' : ∀ t ∈ S, IsProperLinearSet t
hs : IsSemilinearSet (⋃₀ S)
⊢ IsSemilinearSet (⋂ i ∈ S, iᶜ)
Module: Mathlib.Topology.Baire.LocallyCompactRegular

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
s : Set X
inst✝¹ : R1Space X
inst✝ : LocallyCompactSpace X
f : ℕ → Set X
ho : ∀ (n : ℕ), IsOpen (f n)
hd : ∀ (n : ℕ), Dense (f n)
U : Set X
U_open : IsOpen U
⊢ U.Nonempty → (U ∩ ⋂ n, f n).Nonempty

Tactic:
U_nonempty

Goal state after:
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
⊢ (U ∩ ⋂ n, f n).Nonempty
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

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

Tactic:
by ring_nf

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
x a : R
ha : u = v * a
b : R
hb : u ^ p = ↑p * u * v * b
⊢ ↑p * u * v * b * x ^ p = ↑p * u * (v * (b * x ^ p))

Tactic:
by ring_nf

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

Goal state before:
pp: ⊢ ↑μ * log = Λ

Tactic:
by
  rw [mul_comm]; simp

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

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

Tactic:
cast_ne_zero

Goal state after:
n m : ℕ
mn : m ∣ n
hn : ¬n = 0
⊢ m ≠ 0
Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt

Goal state before:
pp: n : ℕ
⊢ Λ (n + 1) ≤ Real.log ↑(n + 1)

Tactic:
by
    rw [← vonMangoldt_sum]
    exact single_le_sum (by exact fun _ _ => vonMangoldt_nonneg)
      (mem_divisors_self _ n.succ_ne_zero)

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

Goal state before:
pp: case refine_1
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)
⊢ ↑p * ↑p ^ m * ↑p ∣ (↑p ^ m) ^ p

Tactic:
rw [← pow_succ', ← pow_succ, ← pow_mul, mul_comm]
      exact pow_dvd_pow _ hpm

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

Goal state before:
pp: case zero
A : Type u_3
inst✝² : CommRing A
inst✝¹ : Algebra ℚ A
inst✝ : IsAddTorsionFree A
f : A⟦X⟧
hd : (d⁄dX A) f = f
hc : constantCoeff f = 1
⊢ constantCoeff f = constantCoeff (exp A)

Tactic:
hc,

Goal state after:
case zero
A : Type u_3
inst✝² : CommRing A
inst✝¹ : Algebra ℚ A
inst✝ : IsAddTorsionFree A
f : A⟦X⟧
hd : (d⁄dX A) f = f
hc : constantCoeff f = 1
⊢ 1 = constantCoeff (exp A)
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: a k : ℕ
h0 : a ≠ 0
h1 : a ≤ k
n : ℕ
⊢ π' (k + n + 1) ≤ π k + φ a * (n / a + 1)

Tactic:
convert! primeCounting'_add_le h0 (Order.lt_add_one_iff.mpr h1) n using 2

Goal state after:
case e'_3
a k : ℕ
h0 : a ≠ 0
h1 : a ≤ k
n : ℕ
⊢ k + n + 1 = k + 1 + n
Module: Mathlib.NumberTheory.BernoulliPolynomials

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

Tactic:
refine Nat.strong_induction_on n fun d hd => ?_

Goal state after:
n d : ℕ
hd : ∀ m < d, (bernoulli m).comp (1 + X) = bernoulli m + m • X ^ (m - 1)
⊢ (bernoulli d).comp (1 + X) = bernoulli d + d • X ^ (d - 1)
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: case succ
n d : ℕ
hd : ∀ m < d + 1, (bernoulli m).comp (1 + X) = bernoulli m + m • X ^ (m - 1)
⊢ ((d + 2) • X ^ (d + 1)).comp (1 + X) -
      (∑ x ∈ range (d + 1), (d + 2).choose x • bernoulli x + ∑ x ∈ range (d + 1), (d + 2).choose x • x • X ^ (x - 1)) =
    (d + 2) • X ^ (d + 1) -
      (∑ x ∈ range (d + 1), (d + 2).choose x • bernoulli x - ((d + 2) * (d + 1)) • X ^ (d + 1 - 1))

Tactic:
sub_add_eq_sub_sub_swap,

Goal state after:
case succ
n d : ℕ
hd : ∀ m < d + 1, (bernoulli m).comp (1 + X) = bernoulli m + m • X ^ (m - 1)
⊢ ((d + 2) • X ^ (d + 1)).comp (1 + X) - ∑ x ∈ range (d + 1), (d + 2).choose x • x • X ^ (x - 1) -
      ∑ x ∈ range (d + 1), (d + 2).choose x • bernoulli x =
    (d + 2) • X ^ (d + 1) -
      (∑ x ∈ range (d + 1), (d + 2).choose x • bernoulli x - ((d + 2) * (d + 1)) • X ^ (d + 1 - 1))
Module: Mathlib.NumberTheory.AbelSummation

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

Tactic:
hc,

Goal state after:
case inl
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
b : ℝ
hf_diff : ∀ t ∈ Set.Icc 1 b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc 1 b) volume
hb : 1 ≤ b
this : 1 ≤ ⌊b⌋₊
⊢ f ↑0 * 0 +
      (f 1 * c 1 +
        (f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f 1 * (0 + c 1) - ∫ (t : ℝ) in Set.Ioc 1 b, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k)) =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - ∫ (t : ℝ) in Set.Ioc 1 b, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: case inr
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
b : ℝ
hf_diff : ∀ t ∈ Set.Icc 1 b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc 1 b) volume
hb : b < 1
⊢ f 0 * c 0 = f b * c 0 - ∫ (t : ℝ) in Set.Ioc 1 b, deriv f t * ∑ x ∈ Icc 0 ⌊t⌋₊, c x

Tactic:
hc,

Goal state after:
case inr
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
b : ℝ
hf_diff : ∀ t ∈ Set.Icc 1 b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc 1 b) volume
hb : b < 1
⊢ f 0 * 0 = f b * 0 - ∫ (t : ℝ) in Set.Ioc 1 b, deriv f t * ∑ x ∈ Icc 0 ⌊t⌋₊, c x
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
r : ℚ
⊢ r * (↑p + 1 + 1) * ↑n ^ p.succ / (↑p + 1 + 1) = r * ↑n ^ p.succ

Tactic:
mul_div_right_comm,

Goal state after:
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
r : ℚ
⊢ r * (↑p + 1 + 1) / (↑p + 1 + 1) * ↑n ^ p.succ = r * ↑n ^ p.succ
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: case h₁
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 ℕ := ⋯
f : ℕ → ℕ := ⋯
this : ∏ x ∈ S, f x = ∏ x ∈ Finset.range (2 * n / 3 + 1), f x
⊢ ∏ x ∈ S with x ≤ (2 * n).sqrt, f x ≤ (2 * n) ^ (2 * n).sqrt

pp: case h₂
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 ℕ := ⋯
f : ℕ → ℕ := ⋯
this : ∏ x ∈ S, f x = ∏ x ∈ Finset.range (2 * n / 3 + 1), f x
⊢ ∏ x ∈ S with ¬x ≤ (2 * n).sqrt, f x ≤ 4 ^ (2 * n / 3)

Tactic:
· refine (Finset.prod_le_prod' fun p _ => (?_ : f p ≤ 2 * n)).trans ?_
    · exact pow_factorization_choose_le (mul_pos two_pos n_pos)
    have : (Finset.Icc 1 (sqrt (2 * n))).card = sqrt (2 * n) := by rw [card_Icc, Nat.add_sub_cancel]
    rw [Finset.prod_const]
    refine pow_right_mono₀ n2_pos ((Finset.card_le_card fun x hx => ?_).trans this.le)
    obtain ⟨h1, h2⟩ := Finset.mem_filter.1 hx
    exact Finset.mem_Icc.mpr ⟨(Finset.mem_filter.1 h1).2.one_lt.le, h2⟩

Goal state after:
case h₂
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 ℕ := ⋯
f : ℕ → ℕ := ⋯
this : ∏ x ∈ S, f x = ∏ x ∈ Finset.range (2 * n / 3 + 1), f x
⊢ ∏ x ∈ S with ¬x ≤ (2 * n).sqrt, f x ≤ 4 ^ (2 * n / 3)
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : x < 2
⊢ θ x = 0

Tactic:
by
  apply sum_eq_zero fun n hn ↦ ?_
  convert! log_one
  simp only [mem_filter, mem_Ioc] at hn
  have := lt_of_le_of_lt (le_floor_iff' hn.1.1.ne' |>.mp hn.1.2) hx
  norm_cast at ⊢ this
  linarith

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

Goal state before:
pp: case pos
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)
le_b : b.natDegree ≤ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊
i₀ i₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ
i_ne : i₀ ≠ i₁
mod_eq : A i₁ % b = A i₀ % b
⊢ ↑0 < cardPowDegree b • ε

Tactic:
Int.cast_zero

Goal state after:
case pos
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)
le_b : b.natDegree ≤ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊
i₀ i₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ
i_ne : i₀ ≠ i₁
mod_eq : A i₁ % b = A i₀ % b
⊢ 0 < cardPowDegree b • ε
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: case pos
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)
le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < b.natDegree
i₀ i₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ
i_ne : i₀ ≠ i₁
deg_lt : (A i₁ % b - A i₀ % b).degree < ↑(b.natDegree - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
h : A i₁ % b = A i₀ % b
⊢ ↑0 < cardPowDegree b • ε

Tactic:
Int.cast_zero

Goal state after:
case pos
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)
le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < b.natDegree
i₀ i₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ
i_ne : i₀ ≠ i₁
deg_lt : (A i₁ % b - A i₀ % b).degree < ↑(b.natDegree - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
h : A i₁ % b = A i₀ % b
⊢ 0 < cardPowDegree b • ε
Module: Mathlib.NumberTheory.ClassNumber.Finite

Goal state before:
pp: case c0
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 : ι
him : (Finset.image (fun k ↦ abv ((bS.repr a) k)) Finset.univ).Nonempty
y' : ℤ := ⋯
y'_def : y' = (Finset.image (fun k ↦ abv ((bS.repr a) k)) Finset.univ).max' him
hy' : ∀ (k : ι), abv ((bS.repr a) k) ≤ y'
this : ↑y' < y
y'_nonneg : 0 ≤ y'
⊢ 0 ≤ ↑y' ^ Fintype.card ι

pp: case b0
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 : ι
him : (Finset.image (fun k ↦ abv ((bS.repr a) k)) Finset.univ).Nonempty
y' : ℤ := ⋯
y'_def : y' = (Finset.image (fun k ↦ abv ((bS.repr a) k)) Finset.univ).max' him
hy' : ∀ (k : ι), abv ((bS.repr a) k) ≤ y'
this : ↑y' < y
y'_nonneg : 0 ≤ y'
⊢ 0 < ↑(normBound abv bS)

Tactic:
· positivity

Goal state after:
case b0
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 : ι
him : (Finset.image (fun k ↦ abv ((bS.repr a) k)) Finset.univ).Nonempty
y' : ℤ := ⋯
y'_def : y' = (Finset.image (fun k ↦ abv ((bS.repr a) k)) Finset.univ).max' him
hy' : ∀ (k : ι), abv ((bS.repr a) k) ≤ y'
this : ↑y' < y
y'_nonneg : 0 ≤ y'
⊢ 0 < ↑(normBound abv bS)
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case succ.succ
k p : ℕ
hk : k > 0
inst✝ : Fact (Nat.Prime p)
ih : ∀ (m : ℕ), 0 < m → m < k → pIntegral p (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / ↑p)
i : ℕ
hi : i + 1 + 1 < 2 * k
⊢ (Rat.padicValuation p)
      (bernoulli (i + 1 + 1) * ↑((2 * k + 1).choose (i + 1 + 1)) * ↑p ^ (2 * k - (i + 1 + 1)) / (2 * ↑k + 1)) ≤
    1

Tactic:
· rcases Nat.even_or_odd (i + 2) with ⟨m, hm⟩ | hodd
    · have ⟨hm_pos, hm_lt, hi_eq⟩ : 0 < m ∧ m < k ∧ i + 2 = 2 * m := by lia
      simp only [hi_eq]
      exact pIntegral_bernoulli_even_term hm_lt (ih m hm_pos hm_lt)
    · simp [bernoulli_eq_zero_of_odd hodd (by lia)]

Goal state after:
Module: Mathlib.NumberTheory.FunctionField

Goal state before:
pp: case mpr
F : Type u_1
K : Type u_2
inst✝⁹ : Field F
inst✝⁸ : Field K
Ft : Type u_3
inst✝⁷ : Field Ft
inst✝⁶ : Algebra F[X] Ft
inst✝⁵ : IsFractionRing F[X] Ft
inst✝⁴ : Algebra F⟮X⟯ K
inst✝³ : Algebra Ft K
inst✝² : Algebra F[X] K
inst✝¹ : IsScalarTower F[X] Ft K
inst✝ : IsScalarTower F[X] F⟮X⟯ K
e : F⟮X⟯ ≃ₐ[F[X]] Ft := IsLocalization.algEquiv F[X]⁰ F⟮X⟯ Ft
this : ∀ (c : F⟮X⟯) (x : K), e c • x = c • x
h : FiniteDimensional Ft K
⊢ FunctionField F K

Tactic:
· let b := Module.finBasis Ft K
    refine (b.mapCoeffs e.symm ?_).finiteDimensional_of_finite
    intro c x; convert! (this (e.symm c) x).symm; simp only [e.apply_symm_apply]

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

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

Tactic:
by ring_nf

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

Goal state before:
pp: case neg
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(x.appr n)
x : ℤ_[p]
h : ¬x - ↑(x.appr n) = 0
⊢ ↑p ^ (n + 1) ∣
    x - (↑(x.appr n) + ↑p ^ n * ↑(toZMod (↑(unitCoeff h) * ↑p ^ (↑(x - ↑(x.appr n)).valuation - ↑n).natAbs)).val)

Tactic:
rw [sub_add_eq_sub_sub]

Goal state after:
case neg
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), ↑p ^ n ∣ x - ↑(x.appr n)
x : ℤ_[p]
h : ¬x - ↑(x.appr n) = 0
⊢ ↑p ^ (n + 1) ∣
    x - ↑(x.appr n) - ↑p ^ n * ↑(toZMod (↑(unitCoeff h) * ↑p ^ (↑(x - ↑(x.appr n)).valuation - ↑n).natAbs)).val