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

Goal state before:
pp: case neg
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 (μ.variation.restrict s)
hC : ∀ᵐ (x : X) ∂μ.variation.restrict s, ‖f x‖ ≤ C
hs : ¬MeasurableSet s
h's : ¬μ.variation s = 0
this : (ae (μ.variation.restrict s)).NeBot
x : X
hx : ‖f x‖ ≤ C
⊢ 0 ≤ C * ‖B‖ * μ.variation.real s

Tactic:
have : 0 ≤ C := le_trans (norm_nonneg _) hx

Goal state after:
case neg
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 (μ.variation.restrict s)
hC : ∀ᵐ (x : X) ∂μ.variation.restrict s, ‖f x‖ ≤ C
hs : ¬MeasurableSet s
h's : ¬μ.variation s = 0
this✝ : (ae (μ.variation.restrict s)).NeBot
x : X
hx : ‖f x‖ ≤ C
this : 0 ≤ C
⊢ 0 ≤ C * ‖B‖ * μ.variation.real s
Module: Mathlib.MeasureTheory.VectorMeasure.AddContent

Goal state before:
pp: case pos
α : 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 : MeasurableSet s
⊢ ∫⁻ (a : α), ‖μ[s.indicator 1 | M] a‖ₑ ∂μ.trim Mle ≤ μ s

Tactic:
lintegral_trim _ (by fun_prop),

Goal state after:
case pos
α : 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 : MeasurableSet s
⊢ ∫⁻ (a : α), ‖μ[s.indicator 1 | M] a‖ₑ ∂μ ≤ μ s
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensityVec

Goal state before:
pp: case pos
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
s : Set X
hf : μ.Integrable f
hs : MeasurableSet s
t : Set X
ht : MeasurableSet t
⊢ (μ.withDensity f B) (t ∩ s) = ((μ.restrict s).withDensity f B) t

Tactic:
withDensity_apply hf,

Goal state after:
case pos
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
s : Set X
hf : μ.Integrable f
hs : MeasurableSet s
t : Set X
ht : MeasurableSet t
⊢ ∫ᵛ (x : X) in t ∩ s, f x ∂[B; μ] = ((μ.restrict s).withDensity f B) t
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
hf : μ.Integrable f
s : Set X
hs : MeasurableSet s
⊢ ‖(μ.withDensity f B) s‖ₑ ≤ ((μ.transpose B).variation.withDensity fun x ↦ ‖f x‖ₑ) s

Tactic:
withDensity_apply hf,

Goal state after:
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
hf : μ.Integrable f
s : Set X
hs : MeasurableSet s
⊢ ‖∫ᵛ (x : X) in s, f x ∂[B; μ]‖ₑ ≤ ((μ.transpose B).variation.withDensity fun x ↦ ‖f x‖ₑ) s
Module: Mathlib.ModelTheory.Complexity

Goal state before:
pp: L : Language
α : Type u'
β : Type v'
n m : ℕ
φ : L.BoundedFormula α m
h✝ : φ.IsPrenex
f : α → β ⊕ Fin n
n✝ : ℕ
φ✝ : L.BoundedFormula α (n✝ + 1)
x✝ : φ✝.IsPrenex
h : (BoundedFormula.relabel f φ✝).IsPrenex
⊢ (BoundedFormula.relabel f (∃' φ✝)).IsPrenex

Tactic:
simp [h.ex]

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

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : LinearIndepOn ℕ id s
⊢ LinearIndepOn ℚ (⇑toRatVec) s

Tactic:
rw [LinearIndepOn, ← LinearIndependent.iff_fractionRing ℤ ℚ, ← LinearIndepOn, linearIndepOn_iff'']

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : LinearIndepOn ℕ id s
⊢ ∀ (t : Finset (ι → ℕ)) (g : (ι → ℕ) → ℤ),
    ↑t ⊆ s → (∀ i ∉ t, g i = 0) → ∑ i ∈ t, g i • toRatVec i = 0 → ∀ i ∈ t, g i = 0
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
h : f ≤ g
x : ↥f.dom
⊢ g.cod.subtype.toFun ((inclusion ⋯) (f.toEquiv x)) = g.cod.subtype.toFun (g.toEquiv ((inclusion ⋯) x))

Tactic:
toEquiv_inclusion_apply

Goal state after:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
h : f ≤ g
x : ↥f.dom
⊢ g.cod.subtype.toFun ((inclusion ⋯) (f.toEquiv x)) = g.cod.subtype.toFun ((inclusion ⋯) (f.toEquiv x))

case h
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
h : f ≤ g
x : ↥f.dom
⊢ f ≤ g
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝⁴ : L.Structure M
inst✝³ : L.Structure N
ι : Type u_1
inst✝² : Preorder ι
inst✝¹ : Nonempty ι
inst✝ : IsDirectedOrder ι
S : ι →o M ≃ₚ[L] N
i : ι
⊢ (partialEquivLimit S).cod.subtype.comp ((partialEquivLimit S).toEquiv.toEmbedding.comp (inclusion ⋯)) =
    (S i).cod.subtype.comp (S i).toEquiv.toEmbedding

Tactic:
by
    #adaptation_note /-- https://github.com/leanprover/lean4/pull/5020
    these two `simp` calls cannot be combined. -/
    simp only [partialEquivLimit_comp_inclusion]
    simp only [cod_partialEquivLimit, ← Embedding.comp_assoc,
      subtype_comp_inclusion]

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

Goal state before:
pp: ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
⊢ toRatVec x - ∑ x_1, (hs.floor x x_1).toNat • toRatVec ↑x_1 + ∑ x_1, (-hs.floor x x_1).toNat • toRatVec ↑x_1 =
    toRatVec hs.base + ∑ i, Int.fract ((hs.basis.repr (toRatVec x - toRatVec hs.base)) i) • toRatVec ↑i

Tactic:
sub_add,

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
⊢ toRatVec x - (∑ x_1, (hs.floor x x_1).toNat • toRatVec ↑x_1 - ∑ x_1, (-hs.floor x x_1).toNat • toRatVec ↑x_1) =
    toRatVec hs.base + ∑ i, Int.fract ((hs.basis.repr (toRatVec x - toRatVec hs.base)) i) • toRatVec ↑i
Module: Mathlib.ModelTheory.PartialEquiv

Goal state before:
pp: L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
g : L.FGEquiv M N
H : L.IsExtensionPair M N
X : Set M
left✝ : X.Countable
X_gen : (closure L).toFun X = ⊤
x✝² : Countable ↑X
x✝¹ : Encodable ↑X
D : ↑X → Order.Cofinal (L.FGEquiv M N) := fun x ↦ H.definedAtLeft ↑x
S : ℕ →o M ≃ₚ[L] N := { toFun := Subtype.val ∘ Order.sequenceOfCofinals g D, monotone' := ⋯ }
F : M ≃ₚ[L] N := partialEquivLimit S
x✝ : X ⊆ ↑F.dom
isTop : F.dom = ⊤
⊢ ↑g ≤ (toEmbeddingOfEqTop isTop).toPartialEquiv

Tactic:
by convert! (le_partialEquivLimit S 0); apply Embedding.toPartialEquiv_toEmbedding

Goal state after:
Module: Mathlib.Order.CountableDenseLinearOrder

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : LinearOrder β
inst✝² : DenselyOrdered β
inst✝¹ : NoMinOrder β
inst✝ : NoMaxOrder β
nonem : Nonempty β
S : Finset α
f : ↥S ↪o β
a : α
Slt : Finset β := Finset.image (⇑f) ({x ∈ S.attach | ↑x < a})
Sgt : Finset β := Finset.image (⇑f) ({x ∈ S.attach | a < ↑x})
x : β
hx : x ∈ Slt
y : β
hy : y ∈ Sgt
⊢ x < y

Tactic:
by
    simp only [Finset.mem_image, Finset.mem_filter, Finset.mem_attach, true_and, Subtype.exists,
      exists_and_left, Slt, Sgt] at hx hy
    obtain ⟨_, hx, _, rfl⟩ := hx
    obtain ⟨_, hy, _, rfl⟩ := hy
    exact f.strictMono (hx.trans hy)

Goal state after:
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: L : Language
K : Set (Bundled L.Structure)
inst✝ : Countable ((l : ℕ) × L.Functions l)
⊢ (∃ M, Countable ↑M ∧ L.age ↑M = K) ↔
    K.Nonempty ∧
      (∀ (M N : Bundled L.Structure), Nonempty (↑M ≃[L] ↑N) → (M ∈ K ↔ N ∈ K)) ∧
        (Quotient.mk' '' K).Countable ∧ (∀ M ∈ K, Structure.FG L ↑M) ∧ Hereditary K ∧ JointEmbedding K

Tactic:
constructor
  · rintro ⟨M, h1, h2, rfl⟩
    refine ⟨age.nonempty M, age.is_equiv_invariant L M, age.countable_quotient M, fun N hN => hN.1,
      age.hereditary M, age.jointEmbedding M⟩
  · rintro ⟨Kn, _, cq, hfg, hp, jep⟩
    obtain ⟨M, hM, rfl⟩ := exists_cg_is_age_of Kn cq hfg hp jep
    exact ⟨M, Structure.cg_iff_countable.1 hM, rfl⟩

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

Goal state before:
pp: case mp
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
⊢ (hs.fract x = hs.base ∧ ∃ i, ↑i ∉ hs.periods ∧ 0 < hs.floor x i) →
    ∃ i,
      ↑i ∉ hs.periods ∧
        ∃ y ∈ closure {↑i},
          ∃ z ∈ closure (hs.basisSet \ {↑i}), ∃ z' ∈ closure (hs.basisSet \ {↑i}), x + z' = hs.base + ↑i + y + z

Tactic:
intro ⟨hx, i, hi, hi'⟩

Goal state after:
case mp
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
x : ι → ℕ
hx : hs.fract x = hs.base
i : ↑hs.basisSet
hi : ↑i ∉ hs.periods
hi' : 0 < hs.floor x i
⊢ ∃ i,
    ↑i ∉ hs.periods ∧
      ∃ y ∈ closure {↑i},
        ∃ z ∈ closure (hs.basisSet \ {↑i}), ∃ z' ∈ closure (hs.basisSet \ {↑i}), x + z' = hs.base + ↑i + y + z
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: M : Type u_1
inst✝² : Countable M
inst✝¹ : Infinite M
inst✝ : Language.empty.Structure M
S : Language.empty.Substructure M
hS : S.FG
f : ↥S ↪[Language.empty] M
this✝² : Finite ↥S
this✝¹ : Infinite { x // x ∉ S }
this✝ : Finite ↥f.toHom.range
this : Infinite { x // x ∉ f.toHom.range }
⊢ ∃ g, f = g.toEmbedding.comp S.subtype

Tactic:
refine ⟨StrongHomClass.toEquiv (f.equivRange.subtypeCongr nonempty_equiv_of_countable.some), ?_⟩

Goal state after:
M : Type u_1
inst✝² : Countable M
inst✝¹ : Infinite M
inst✝ : Language.empty.Structure M
S : Language.empty.Substructure M
hS : S.FG
f : ↥S ↪[Language.empty] M
this✝² : Finite ↥S
this✝¹ : Infinite { x // x ∉ S }
this✝ : Finite ↥f.toHom.range
this : Infinite { x // x ∉ f.toHom.range }
⊢ f = (StrongHomClass.toEquiv (f.equivRange.subtypeCongr ⋯.some)).toEmbedding.comp S.subtype
Module: Mathlib.ModelTheory.Topology.Types

Goal state before:
pp: L : Language
T : L.Theory
α : Type u_1
p q : T.CompleteType α
φ : L[[α]].Sentence
hφ : φ ∉ p ↔ φ ∈ q
x✝ : φ ∈ p ∨ Formula.not φ ∈ p
⊢ ∃ U, IsClopen U ∧ p ∈ U ∧ q ∈ Uᶜ

Tactic:
cases mem_or_not_mem p φ with

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

Goal state before:
pp: n : ℕ
this : ∑ i ∈ n.divisors, ↑(μ i) * -Real.log ↑(n / i) = ∑ i ∈ n.divisors, (↑(μ i) * Real.log ↑i - ↑(μ i) * Real.log ↑n)
⊢ ∑ d ∈ n.divisors, ↑(μ d) * Real.log ↑d =
    ∑ x ∈ n.divisors, ↑(μ x) * Real.log ↑x - ∑ x ∈ n.divisors, ↑(μ x) * Real.log ↑n

Tactic:
← sum_mul,

Goal state after:
n : ℕ
this : ∑ i ∈ n.divisors, ↑(μ i) * -Real.log ↑(n / i) = ∑ i ∈ n.divisors, (↑(μ i) * Real.log ↑i - ↑(μ i) * Real.log ↑n)
⊢ ∑ d ∈ n.divisors, ↑(μ d) * Real.log ↑d =
    ∑ x ∈ n.divisors, ↑(μ x) * Real.log ↑x - (∑ i ∈ n.divisors, ↑(μ i)) * Real.log ↑n
Module: Mathlib.MeasureTheory.VectorMeasure.WithDensityVec

Goal state before:
pp: case inr.e_f.inr
X : Type u_1
E : Type u_2
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure X
f : X → E
hf : Integrable f μ
hE : Nontrivial E
this✝ : IsFiniteMeasure (μ.withDensity fun x ↦ ‖f x‖ₑ)
I : VectorMeasure.Integrable (μ.withDensity fun x ↦ ‖f x‖ₑ).toSignedMeasure fun x ↦ ‖f x‖⁻¹ • f x
this :
  μ.withDensityᵥ f =
    withDensity (μ.withDensity fun x ↦ ‖f x‖ₑ).toSignedMeasure (fun x ↦ ‖f x‖⁻¹ • f x)
      (ContinuousLinearMap.lsmul ℝ ℝ).flip
x : X
hx : f x ≠ 0
h'x : ‖f x‖ ≠ 0
⊢ ((fun x ↦ ‖f x‖ₑ) * fun x ↦ ‖‖f x‖⁻¹ • f x‖ₑ) x = ‖f x‖ₑ

Tactic:
simp only [enorm_smul, Pi.mul_apply, ne_eq, h'x, not_false_eq_true, enorm_inv, enorm_norm]

Goal state after:
case inr.e_f.inr
X : Type u_1
E : Type u_2
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
μ : Measure X
f : X → E
hf : Integrable f μ
hE : Nontrivial E
this✝ : IsFiniteMeasure (μ.withDensity fun x ↦ ‖f x‖ₑ)
I : VectorMeasure.Integrable (μ.withDensity fun x ↦ ‖f x‖ₑ).toSignedMeasure fun x ↦ ‖f x‖⁻¹ • f x
this :
  μ.withDensityᵥ f =
    withDensity (μ.withDensity fun x ↦ ‖f x‖ₑ).toSignedMeasure (fun x ↦ ‖f x‖⁻¹ • f x)
      (ContinuousLinearMap.lsmul ℝ ℝ).flip
x : X
hx : f x ≠ 0
h'x : ‖f x‖ ≠ 0
⊢ ‖f x‖ₑ * (‖f x‖ₑ⁻¹ * ‖f x‖ₑ) = ‖f x‖ₑ
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n : ℕ
⊢ 1 - ∑ k ∈ range n, ↑(n.choose k) / (↑n - ↑k + 1) * bernoulli' k +
      ∑ x ∈ range n, ↑(n.choose (n - x)) / (↑n - ↑x + 1) * bernoulli' x =
    1

Tactic:
sub_add,

Goal state after:
n : ℕ
⊢ 1 -
      (∑ k ∈ range n, ↑(n.choose k) / (↑n - ↑k + 1) * bernoulli' k -
        ∑ x ∈ range n, ↑(n.choose (n - x)) / (↑n - ↑x + 1) * bernoulli' x) =
    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,

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 • 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))
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: case pos
n i : ℕ
h : i ≤ n + 1
h' : i = n + 1 - 1
⊢ _root_.bernoulli (n + 1 - i) * ↑((n + 1).choose i) * (-1) ^ i =
    (-1) ^ (n + 1) • (_root_.bernoulli (n + 1 - i) * ↑((n + 1).choose i) + (n + 1) • 1)

Tactic:
subst h'
    simp
    grind

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case succ.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
hfact : ∀ (m : ℕ), ↑m ! ≠ 0
hite2 : (if n.succ = 0 then 1 else 0) = 0
⊢ (algebraMap ℚ A) (∑ x ∈ antidiagonal (n + 1), bernoulli x.1 / ↑x.1! * ((↑x.2 + 1) * ↑x.2!)⁻¹) =
    (algebraMap ℚ A) ((∑ k ∈ antidiagonal n.succ, ↑((k.1 + k.2).choose k.2) / (↑k.2 + 1) * bernoulli k.1) / ↑n.succ !)

Tactic:
sum_div

Goal state after:
case succ.succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
hfact : ∀ (m : ℕ), ↑m ! ≠ 0
hite2 : (if n.succ = 0 then 1 else 0) = 0
⊢ (algebraMap ℚ A) (∑ x ∈ antidiagonal (n + 1), bernoulli x.1 / ↑x.1! * ((↑x.2 + 1) * ↑x.2!)⁻¹) =
    (algebraMap ℚ A) (∑ i ∈ antidiagonal n.succ, ↑((i.1 + i.2).choose i.2) / (↑i.2 + 1) * bernoulli i.1 / ↑n.succ !)
Module: Mathlib.NumberTheory.Bernoulli

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

Tactic:
rw [show (2 * (k : ℚ) - 2 * (m : ℚ) + 1) = (↑(2 * k + 1 - 2 * m) : ℚ) by norm_cast; lia]

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

Goal state before:
pp: case refine_1
n q : ℕ
hq : q ∈ (filter Nat.Prime (Icc 1 n)).biUnion fun p ↦ image (fun x ↦ p ^ x) (Icc 1 (Nat.log p n))
⊢ q ∈ Icc 1 n

Tactic:
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⟩

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case hy
k m p : ℕ
hm_lt : m < k
inst✝ : Fact (Nat.Prime p)
ih : pIntegral p (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / ↑p)
hp_ne : ↑p ≠ 0
P : ℚ := ⋯
hpow : ↑p ^ (2 * k - 2 * m) = P * ↑p
hdecomp :
  bernoulli (2 * m) * ↑((2 * k + 1).choose (2 * m)) * ↑p ^ (2 * k - 2 * m) / (2 * ↑k + 1) =
    (bernoulli (2 * m) + vonStaudtIndicator (2 * m) p / ↑p) * ↑((2 * k + 1).choose (2 * m)) * ↑p ^ (2 * k - 2 * m) /
        (2 * ↑k + 1) -
      vonStaudtIndicator (2 * m) p * ↑((2 * k + 1).choose (2 * m)) * P / (2 * ↑k + 1)
hcmp : pIntegral p (↑((2 * k).choose (2 * m)) * ↑p ^ (2 * k - 2 * m - 1) / (2 * ↑k - 2 * ↑m + 1))
H : ∀ (x : ℚ), ↑((2 * k + 1).choose (2 * m)) * x / (2 * ↑k + 1) = ↑((2 * k).choose (2 * m)) * x / (2 * ↑k - 2 * ↑m + 1)
⊢ (Rat.padicValuation p) (vonStaudtIndicator (2 * m) p * ↑((2 * k + 1).choose (2 * m)) * P / (2 * ↑k + 1)) ≤ 1

Tactic:
· unfold vonStaudtIndicator
    split_ifs
    · grind
    · simp

Goal state after:
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
adm : abv.IsAdmissible
inst✝¹ : Infinite R
inst✝ : DecidableEq R
a : S
b : R
hb : b ≠ 0
dim_pos : 0 < Fintype.card ι
ε : ℝ := ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
ε_eq : ε = ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
hε : 0 < ε
ε_le : ↑(normBound abv bS) * (abv b • ε) ^ ↑(Fintype.card ι) ≤ ↑(abv b) ^ ↑(Fintype.card ι)
μ : Fin (cardM bS adm).succ ↪ R := distinctElems bS adm
s : ι →₀ R := bS.repr a
s_eq : ∀ (i : ι), s i = (bS.repr a) i
qs : Fin (cardM bS adm).succ → ι → R := fun j i ↦ μ j * s i / b
⊢ ∃ q, ∃ r ∈ finsetApprox bS adm, abv ((Algebra.norm R) (r • a - b • q)) < abv ((Algebra.norm R) ((algebraMap R S) b))

Tactic:
let rs : Fin (cardM bS adm).succ → ι → R := fun j i => μ j * s i % b

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
adm : abv.IsAdmissible
inst✝¹ : Infinite R
inst✝ : DecidableEq R
a : S
b : R
hb : b ≠ 0
dim_pos : 0 < Fintype.card ι
ε : ℝ := ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
ε_eq : ε = ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
hε : 0 < ε
ε_le : ↑(normBound abv bS) * (abv b • ε) ^ ↑(Fintype.card ι) ≤ ↑(abv b) ^ ↑(Fintype.card ι)
μ : Fin (cardM bS adm).succ ↪ R := distinctElems bS adm
s : ι →₀ R := bS.repr a
s_eq : ∀ (i : ι), s i = (bS.repr a) i
qs : Fin (cardM bS adm).succ → ι → R := fun j i ↦ μ j * s i / b
rs : Fin (cardM bS adm).succ → ι → R := fun j i ↦ μ j * s i % b
⊢ ∃ q, ∃ r ∈ finsetApprox bS adm, abv ((Algebra.norm R) (r • a - b • q)) < abv ((Algebra.norm R) ((algebraMap R S) b))
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
adm : abv.IsAdmissible
inst✝¹ : Infinite R
inst✝ : DecidableEq R
a : S
b : R
hb : b ≠ 0
dim_pos : 0 < Fintype.card ι
ε : ℝ := ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
ε_eq : ε = ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
hε : 0 < ε
ε_le : ↑(normBound abv bS) * (abv b • ε) ^ ↑(Fintype.card ι) ≤ ↑(abv b) ^ ↑(Fintype.card ι)
μ : Fin (cardM bS adm).succ ↪ R := distinctElems bS adm
s : ι →₀ R := bS.repr a
s_eq : ∀ (i : ι), s i = (bS.repr a) i
qs : Fin (cardM bS adm).succ → ι → R := fun j i ↦ μ j * s i / b
rs : Fin (cardM bS adm).succ → ι → R := fun j i ↦ μ j * s i % b
r_eq : ∀ (j : Fin (cardM bS adm).succ) (i : ι), rs j i = μ j * s i % b
μ_eq : ∀ (i : ι) (j : Fin (cardM bS adm).succ), μ j * s i = b * qs j i + rs j i
μ_mul_a_eq : ∀ (j : Fin (cardM bS adm).succ), μ j • a = b • ∑ i, qs j i • bS i + ∑ i, rs j i • bS i
⊢ ∃ q, ∃ r ∈ finsetApprox bS adm, abv ((Algebra.norm R) (r • a - b • q)) < abv ((Algebra.norm R) ((algebraMap R S) b))

Tactic:
obtain ⟨j, k, j_ne_k, hjk⟩ := adm.exists_approx hε hb fun j i => μ j * s i

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
adm : abv.IsAdmissible
inst✝¹ : Infinite R
inst✝ : DecidableEq R
a : S
b : R
hb : b ≠ 0
dim_pos : 0 < Fintype.card ι
ε : ℝ := ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
ε_eq : ε = ↑(normBound abv bS) ^ (-1 / ↑(Fintype.card ι))
hε : 0 < ε
ε_le : ↑(normBound abv bS) * (abv b • ε) ^ ↑(Fintype.card ι) ≤ ↑(abv b) ^ ↑(Fintype.card ι)
μ : Fin (cardM bS adm).succ ↪ R := distinctElems bS adm
s : ι →₀ R := bS.repr a
s_eq : ∀ (i : ι), s i = (bS.repr a) i
qs : Fin (cardM bS adm).succ → ι → R := fun j i ↦ μ j * s i / b
rs : Fin (cardM bS adm).succ → ι → R := fun j i ↦ μ j * s i % b
r_eq : ∀ (j : Fin (cardM bS adm).succ) (i : ι), rs j i = μ j * s i % b
μ_eq : ∀ (i : ι) (j : Fin (cardM bS adm).succ), μ j * s i = b * qs j i + rs j i
μ_mul_a_eq : ∀ (j : Fin (cardM bS adm).succ), μ j • a = b • ∑ i, qs j i • bS i + ∑ i, rs j i • bS i
j k : Fin (adm.card ε ^ Fintype.card ι).succ
j_ne_k : j ≠ k
hjk : ∀ (k_1 : ι), ↑(abv (μ k * s k_1 % b - μ j * s k_1 % b)) < abv b • ε
⊢ ∃ q, ∃ r ∈ finsetApprox bS adm, abv ((Algebra.norm R) (r • a - b • q)) < abv ((Algebra.norm R) ((algebraMap R S) b))
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), x - ↑(f x) ∈ Ideal.span {↑v}
f_congr : ∀ (x : ℤ_[p]) (a b : ℕ), x - ↑a ∈ Ideal.span {↑v} → x - ↑b ∈ Ideal.span {↑v} → ↑a = ↑b
x y : ℤ_[p]
⊢ ↑(f (x + y)) = ↑(f x) + ↑(f y)

Tactic:
f_congr (x + y) _ (f x + f y),

Goal state after:
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), x - ↑(f x) ∈ Ideal.span {↑v}
f_congr : ∀ (x : ℤ_[p]) (a b : ℕ), x - ↑a ∈ Ideal.span {↑v} → x - ↑b ∈ Ideal.span {↑v} → ↑a = ↑b
x y : ℤ_[p]
⊢ ↑(f x + f y) = ↑(f x) + ↑(f y)

case a
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), x - ↑(f x) ∈ Ideal.span {↑v}
f_congr : ∀ (x : ℤ_[p]) (a b : ℕ), x - ↑a ∈ Ideal.span {↑v} → x - ↑b ∈ Ideal.span {↑v} → ↑a = ↑b
x y : ℤ_[p]
⊢ x + y - ↑(f (x + y)) ∈ Ideal.span {↑v}

case a
p : ℕ
hp_prime : Fact (Nat.Prime p)
r : ℚ
x✝ : ℤ_[p]
v : ℕ
f : ℤ_[p] → ℕ
f_spec : ∀ (x : ℤ_[p]), x - ↑(f x) ∈ Ideal.span {↑v}
f_congr : ∀ (x : ℤ_[p]) (a b : ℕ), x - ↑a ∈ Ideal.span {↑v} → x - ↑b ∈ Ideal.span {↑v} → ↑a = ↑b
x y : ℤ_[p]
⊢ x + y - ↑(f x + f y) ∈ Ideal.span {↑v}