mathlib-initiative/mathlib-tactics huggingface dataset:
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‖₊ = ‖B.flip y‖₊ * ‖x‖₊
s : Set X
hs : MeasurableSet s
ε : NNReal
εpos : 0 < ε
δ : NNReal := ε / 3
δpos : 0 < δ
g : X →ₛ E
hg : eLpNorm (f - ⇑g) 1 (μ.transpose B).variation ≤ ↑δ
gmem : MemLp (⇑g) 1 μ.variation
I1 : ∫⁻ (a : X) in s, ‖f a‖ₑ ∂(μ.transpose B).variation ≤ ∫⁻ (a : X) in s, ‖g a‖ₑ ∂(μ.transpose B).variation + ↑δ
I2 :
  ∫⁻ (a : X) in s, ‖g a‖ₑ ∂(μ.transpose B).variation =
    ∑ i ∈ g.range, ‖i‖ₑ * ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i})
ρ : ℝ≥0∞
ρpos : ρ > 0
hρ : ∑ i ∈ g.range, ‖i‖ₑ * ρ ≤ ↑δ
P : E → Finset (Set X)
Pg : ∀ (i : E), ∀ t ∈ P i, t ⊆ ⇑g ⁻¹' {i}
Pdisj : ∀ (i : E), (↑(P i)).PairwiseDisjoint id
Pmeas : ∀ (i : E), ∀ t ∈ P i, MeasurableSet t
hP :
  ∀ (i : E),
    ‖i‖ₑ * ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i}) ≤
      ‖i‖ₑ * (∑ p ∈ P i, ‖((μ.transpose B).restrict s) p‖ₑ + ρ)
I3 :
  ∑ i ∈ g.range, ‖i‖ₑ * ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i}) ≤
    ∑ i ∈ g.range.sigma P, ‖i.fst‖ₑ * ‖((μ.transpose B).restrict s) i.snd‖ₑ + ↑δ
⊢ ∑ i ∈ g.range.sigma P, ‖∫ᵛ (x : X) in i.snd, i.fst ∂[B; μ.restrict s]‖ₑ =
    ∑ i ∈ g.range.sigma P, ‖∫ᵛ (x : X) in i.snd, g x ∂[B; μ.restrict s]‖ₑ

Tactic:
congr! 2 with ⟨i, p⟩ hi

Goal state after:
case a
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‖₊ = ‖B.flip y‖₊ * ‖x‖₊
s : Set X
hs : MeasurableSet s
ε : NNReal
εpos : 0 < ε
δ : NNReal := ε / 3
δpos : 0 < δ
g : X →ₛ E
hg : eLpNorm (f - ⇑g) 1 (μ.transpose B).variation ≤ ↑δ
gmem : MemLp (⇑g) 1 μ.variation
I1 : ∫⁻ (a : X) in s, ‖f a‖ₑ ∂(μ.transpose B).variation ≤ ∫⁻ (a : X) in s, ‖g a‖ₑ ∂(μ.transpose B).variation + ↑δ
I2 :
  ∫⁻ (a : X) in s, ‖g a‖ₑ ∂(μ.transpose B).variation =
    ∑ i ∈ g.range, ‖i‖ₑ * ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i})
ρ : ℝ≥0∞
ρpos : ρ > 0
hρ : ∑ i ∈ g.range, ‖i‖ₑ * ρ ≤ ↑δ
P : E → Finset (Set X)
Pg : ∀ (i : E), ∀ t ∈ P i, t ⊆ ⇑g ⁻¹' {i}
Pdisj : ∀ (i : E), (↑(P i)).PairwiseDisjoint id
Pmeas : ∀ (i : E), ∀ t ∈ P i, MeasurableSet t
hP :
  ∀ (i : E),
    ‖i‖ₑ * ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i}) ≤
      ‖i‖ₑ * (∑ p ∈ P i, ‖((μ.transpose B).restrict s) p‖ₑ + ρ)
I3 :
  ∑ i ∈ g.range, ‖i‖ₑ * ((μ.transpose B).restrict s).variation (⇑g ⁻¹' {i}) ≤
    ∑ i ∈ g.range.sigma P, ‖i.fst‖ₑ * ‖((μ.transpose B).restrict s) i.snd‖ₑ + ↑δ
i : E
p : Set X
hi : ⟨i, p⟩ ∈ g.range.sigma P
⊢ ∫ᵛ (x : X) in ⟨i, p⟩.snd, ⟨i, p⟩.fst ∂[B; μ.restrict s] = ∫ᵛ (x : X) in ⟨i, p⟩.snd, g x ∂[B; μ.restrict s]
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

Goal state before:
pp: M : Type u_1
ι : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : AddMonoid.FG M
s : Set ι
t : ι → Set M
hs : s.Finite
ht : ∀ i ∈ s, IsSemilinearSet (t i)
⊢ IsSemilinearSet (⋂₀ (t '' s))

Tactic:
apply sInter (hs.image t)

Goal state after:
M : Type u_1
ι : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : AddMonoid.FG M
s : Set ι
t : ι → Set M
hs : s.Finite
ht : ∀ i ∈ s, IsSemilinearSet (t i)
⊢ ∀ s_1 ∈ t '' s, IsSemilinearSet s_1
Module: Mathlib.ModelTheory.DirectLimit

Goal state before:
pp: case refine_2
L : Language
ι : Type u_1
inst✝⁵ : Countable ι
inst✝⁴ : Preorder ι
inst✝³ : IsDirectedOrder ι
inst✝² : Nonempty ι
G : ι → Type w
inst✝¹ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
h : ∀ (i : ι), CG L (G i)
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
⊢ ⊤ ≤ ⨆ i, (Substructure.closure L).toFun ((fun a ↦ (of L ι G f i).toHom a) '' Classical.choose ⋯)

Tactic:
Substructure.closure_image

Goal state after:
case refine_2
L : Language
ι : Type u_1
inst✝⁵ : Countable ι
inst✝⁴ : Preorder ι
inst✝³ : IsDirectedOrder ι
inst✝² : Nonempty ι
G : ι → Type w
inst✝¹ : (i : ι) → L.Structure (G i)
f : (i j : ι) → i ≤ j → G i ↪[L] G j
h : ∀ (i : ι), CG L (G i)
inst✝ : DirectedSystem G fun i j h ↦ ⇑(f i j h)
⊢ ⊤ ≤ ⨆ i, Substructure.map (of L ι G f i).toHom ((Substructure.closure L).toFun (Classical.choose ⋯))
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: case mpr
L : Language
M : Type w
inst✝ : L.Structure M
h : Countable M
N P : Bundled L.Structure
hP2 : Quotient.mk' P = ⟦N⟧
s : Finset ↑P
hs : (closure L).toFun ↑s = ⊤
PM : ↑P ↪[L] M
⊢ ∃ y, equivSetoid { α := ↥((closure L).toFun ↑y), str := inferInstance } N

Tactic:
refine ⟨s.image PM, Setoid.trans (b := P) ?_ <| Quotient.exact hP2⟩

Goal state after:
case mpr
L : Language
M : Type w
inst✝ : L.Structure M
h : Countable M
N P : Bundled L.Structure
hP2 : Quotient.mk' P = ⟦N⟧
s : Finset ↑P
hs : (closure L).toFun ↑s = ⊤
PM : ↑P ↪[L] M
⊢ { α := ↥((closure L).toFun ↑(Finset.image (⇑PM) s)), str := inferInstance } ≈ P
Module: Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic

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

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

Goal state after:
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
i : ↑hs.basisSet
⊢ IsSemilinearSet
    {a |
      ∃ z ∈ closure (hs.basisSet \ {↑i}),
        ∃ z' ∈ closure (hs.basisSet \ {↑i}), a ∘ Sum.inl + ↑i + a ∘ Sum.inr + z' = hs.base + z}
Module: Mathlib.Order.CountableDenseLinearOrder

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : LinearOrder β
inst✝³ : DenselyOrdered α
inst✝² : NoMinOrder α
inst✝¹ : NoMaxOrder α
inst✝ : Nonempty α
b : β
f : PartialIso α β
f' : PartialIso β α
hl : f.comm ≤ f'
a : α
ha : (b, a) ∈ ↑f'
⊢ ↑f ⊆ Finset.image ⇑(Equiv.prodComm β α) ↑f'

Tactic:
rwa [← Finset.coe_subset, Finset.coe_image, ← Equiv.symm_image_subset, ← Finset.coe_image,
        Finset.coe_subset]

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

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

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

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

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

Tactic:
convert!
      Nat.isSemilinearSet_setOfPred_mulVec_eq (κ := ((ι ⊕ ι) ⊕ ι) ⊕ ι) 0 (hs.base + i.1)
        (Matrix.fromCols (Matrix.fromCols (Matrix.fromCols 1 0) 0) 1)
        (Matrix.fromCols (Matrix.fromCols (Matrix.fromCols 0 1) 1) 0) using 4

Goal state after:
case e'_2
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
i : ↑hs.basisSet
hi : i ∈ {i | ↑i ∉ hs.periods}
this : Fintype ι
x✝ : ((ι ⊕ ι) ⊕ ι) ⊕ ι → ℕ
⊢ ((x✝ ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inl + x✝ ∘ Sum.inr = 0 + ((fromCols 1 0).fromCols 0).fromCols 1 *ᵥ x✝

case e'_3
ι : Type u_3
s : Set (ι → ℕ)
hs : IsProperLinearSet s
inst✝ : Finite ι
i : ↑hs.basisSet
hi : i ∈ {i | ↑i ∉ hs.periods}
this : Fintype ι
x✝ : ((ι ⊕ ι) ⊕ ι) ⊕ ι → ℕ
⊢ hs.base + ↑i + ((x✝ ∘ Sum.inl) ∘ Sum.inl) ∘ Sum.inr + (x✝ ∘ Sum.inl) ∘ Sum.inr =
    hs.base + ↑i + ((fromCols 0 1).fromCols 1).fromCols 0 *ᵥ x✝
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: M : Type w'
inst✝¹ : Language.order.Structure M
Mdlo : M ⊨ Language.order.dlo
inst✝ : Nonempty M
⊢ Language.order.age M = {M | Finite ↑M ∧ ↑M ⊨ Language.order.linearOrderTheory}

Tactic:
by
  classical
  rw [age]
  ext N
  refine ⟨fun ⟨hF, h⟩ => ⟨hF.finite, Theory.IsUniversal.models_of_embedding h.some⟩,
    fun ⟨hF, h⟩ => ⟨FG.of_finite, ?_⟩⟩
  let := Language.order.linearOrderOfModels M
  let := Language.order.linearOrderOfModels N
  exact ⟨StrongHomClass.toEmbedding (nonempty_orderEmbedding_of_finite_infinite N M).some⟩

Goal state after:
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
hG : IsGδ s
⊢ BaireSpace ↑s

Tactic:
by
  have : LocallyCompactSpace (closure s) := isClosed_closure.locallyCompactSpace
  have : BaireSpace (closure s) := .of_t2Space_locallyCompactSpace
  have : BaireSpace ((↑) ⁻¹' s : Set (closure s)) :=
    (hG.preimage continuous_subtype_val).baireSpace_of_dense
    (by simp [Subtype.dense_iff, inter_eq_right.mpr subset_closure])
  have h_homeo : Homeomorph ((↑) ⁻¹' s : Set (closure s)) s := ⟨⟨fun x => ⟨x, x.2⟩,
    fun x => ⟨⟨x, subset_closure x.2⟩, x.2⟩, by grind, by grind⟩, by fun_prop, by fun_prop⟩
  exact h_homeo.baireSpace

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

Goal state before:
pp: case refine_3
n a b : ℕ
ha' : 1 < a
hb' : 1 < b
hab : a.Coprime b
ha : ∑ a ∈ a.divisors with IsPrimePow a, Real.log ↑a.minFac = Real.log ↑a
hb : ∑ a ∈ b.divisors with IsPrimePow a, Real.log ↑a.minFac = Real.log ↑b
⊢ ∑ a ∈ (a * b).divisors with IsPrimePow a, Real.log ↑a.minFac = Real.log ↑(a * b)

Tactic:
mul_divisors_filter_prime_pow hab,

Goal state after:
case refine_3
n a b : ℕ
ha' : 1 < a
hb' : 1 < b
hab : a.Coprime b
ha : ∑ a ∈ a.divisors with IsPrimePow a, Real.log ↑a.minFac = Real.log ↑a
hb : ∑ a ∈ b.divisors with IsPrimePow a, Real.log ↑a.minFac = Real.log ↑b
⊢ ∑ a ∈ a.divisors ∪ b.divisors with IsPrimePow a, Real.log ↑a.minFac = Real.log ↑(a * b)
Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt

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

Tactic:
rw [sum_divisorsAntidiagonal fun i j => (μ i : ℝ) * -Real.log j]

Goal state after:
n : ℕ
⊢ ∑ d ∈ n.divisors, ↑(μ d) * Real.log ↑d = ∑ i ∈ n.divisors, ↑(μ i) * -Real.log ↑(n / i)
Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt

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

Tactic:
apply sum_congr rfl

Goal state after:
n : ℕ
⊢ ∀ x ∈ n.divisors, ↑(μ x) * -Real.log ↑(n / x) = ↑(μ x) * Real.log ↑x - ↑(μ x) * Real.log ↑n
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case h
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
this✝¹ : Fact (Nat.Prime p)
n : ℕ
a : ZMod (p ^ (n + 1)) := 1 + ↑p
ha_def : a = 1 + ↑p
ha : IsUnit a
ha' : orderOf ha.unit = p ^ n
b : (ZMod (p ^ (n + 1)))ˣ
hc : orderOf ((unitsMap ⋯) b) = p - 1
this✝ : p - 1 ∣ orderOf b
k : ℕ := orderOf b / (p - 1)
this : orderOf (b ^ k) = p - 1
⊢ (p ^ n).Coprime (p - 1)

Tactic:
apply Nat.Coprime.pow_left

Goal state after:
case h
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
this✝¹ : Fact (Nat.Prime p)
n : ℕ
a : ZMod (p ^ (n + 1)) := ⋯
ha_def : a = 1 + ↑p
ha : IsUnit a
ha' : orderOf ha.unit = p ^ n
b : (ZMod (p ^ (n + 1)))ˣ
hc : orderOf ((unitsMap ⋯) b) = p - 1
this✝ : p - 1 ∣ orderOf b
k : ℕ := ⋯
this : orderOf (b ^ k) = p - 1
⊢ p.Coprime (p - 1)
Module: Mathlib.RingTheory.PowerSeries.Exp

Goal state before:
pp: case succ
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
n : ℕ
ih : (coeff n) f = (coeff n) (exp A)
eq1 : (coeff (n + 1)) f * (↑n + 1) = (coeff n) (exp A)
eq2 : (coeff (n + 1)) (exp A) * (↑n + 1) = (coeff n) (exp A)
h : (coeff (n + 1)) f * (↑n + 1) = (coeff (n + 1)) (exp A) * (↑n + 1)
⊢ (coeff (n + 1)) f = (coeff (n + 1)) (exp A)

Tactic:
rw [← Nat.cast_succ, mul_comm, ← nsmul_eq_mul, mul_comm, ← nsmul_eq_mul] at h

Goal state after:
case succ
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
n : ℕ
ih : (coeff n) f = (coeff n) (exp A)
eq1 : (coeff (n + 1)) f * (↑n + 1) = (coeff n) (exp A)
eq2 : (coeff (n + 1)) (exp A) * (↑n + 1) = (coeff n) (exp A)
h : n.succ • (coeff (n + 1)) f = n.succ • (coeff (n + 1)) (exp A)
⊢ (coeff (n + 1)) f = (coeff (n + 1)) (exp A)
Module: Mathlib.RingTheory.PowerSeries.Exp

Goal state before:
pp: A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n : ℕ
⊢ ∑ x ∈ Finset.range n.succ, a ^ x * (algebraMap ℚ A) (1 / ↑x !) * (b ^ (n - x) * (algebraMap ℚ A) (1 / ↑(n - x)!)) =
    ∑ x ∈ Finset.range (n + 1), a ^ x * b ^ (n - x) * ↑(n.choose x) * (algebraMap ℚ A) (1 / ↑n !)

Tactic:
apply sum_congr rfl

Goal state after:
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n : ℕ
⊢ ∀ x ∈ Finset.range n.succ,
    a ^ x * (algebraMap ℚ A) (1 / ↑x !) * (b ^ (n - x) * (algebraMap ℚ A) (1 / ↑(n - x)!)) =
      a ^ x * b ^ (n - x) * ↑(n.choose x) * (algebraMap ℚ A) (1 / ↑n !)
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: n : ℕ
⊢ ∑ i ∈ range (n + 1), (monomial (n - i)) (_root_.bernoulli i * ↑(n.choose i)) =
    ∑ j ∈ range (n + 1), (monomial (n - j)) (_root_.bernoulli (n - (n - j)) * ↑(n.choose (n - j)))

Tactic:
apply sum_congr rfl

Goal state after:
n : ℕ
⊢ ∀ x ∈ range (n + 1),
    (monomial (n - x)) (_root_.bernoulli x * ↑(n.choose x)) =
      (monomial (n - x)) (_root_.bernoulli (n - (n - x)) * ↑(n.choose (n - x)))
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: case pos
n i : ℕ
h : i ≤ n
⊢ (∑ x ∈ range (n + 1), if n - x = i then _root_.bernoulli x * ↑(n.choose x) else 0) =
    _root_.bernoulli (n - i) * ↑(n.choose i)

pp: case neg
n i : ℕ
h : ¬i ≤ n
⊢ (∑ x ∈ range (n + 1), if n - x = i then _root_.bernoulli x * ↑(n.choose x) else 0) = 0

Tactic:
· convert! sum_ite_eq_of_mem (range (n + 1)) (n - i) _ (by grind) using 3 <;> grind [choose_symm]

Goal state after:
case neg
n i : ℕ
h : ¬i ≤ n
⊢ (∑ x ∈ range (n + 1), if n - x = i then _root_.bernoulli x * ↑(n.choose x) else 0) = 0
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: n : ℕ
⊢ n ≤ nth Prime 0 ↔ n ≤ 2

Tactic:
Nat.nth_prime_zero_eq_two

Goal state after:
n : ℕ
⊢ n ≤ 2 ↔ n ≤ 2
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: n : ℕ
⊢ π n = 0 ↔ n ≤ 1

Tactic:
simp [primeCounting, -Order.add_one_le_iff]

Goal state after:
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: n : ℕ
⊢ n.primesBelow = filter Prime (Ico 0 n)

Tactic:
by
  ext p
  simp [primesBelow_eq_filter_range]

Goal state after:
Module: Mathlib.NumberTheory.Primorial

Goal state before:
pp: n : ℕ
hn1 : n ≠ 1
hn : Odd n
⊢ (n + 1)# = n#

Tactic:
by
  refine prod_congr ?_ fun _ _ ↦ rfl
  rw [range_add_one, filter_insert, if_neg fun h ↦ not_even_iff_odd.2 hn _]
  exact fun h ↦ h.even_sub_one <| mt succ.inj hn1

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ∑ i ∈ antidiagonal n, bernoulli' i.1 / ↑i.1! * ((↑i.2 + 1) * ↑i.2!)⁻¹ * ↑n ! =
    ∑ k ∈ antidiagonal n, ↑((k.1 + k.2).choose k.2) / (↑k.2 + 1) * bernoulli' k.1

Tactic:
apply sum_congr rfl

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
⊢ ∀ x ∈ antidiagonal n,
    bernoulli' x.1 / ↑x.1! * ((↑x.2 + 1) * ↑x.2!)⁻¹ * ↑n ! = ↑((x.1 + x.2).choose x.2) / (↑x.2 + 1) * bernoulli' x.1
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case inl
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun n ↦ bernoulli' n / ↑n !
this : (B - evalNegHom B) * (exp ℚ - 1) = X * (exp ℚ - 1)
h : ∀ (n : ℕ), (coeff n) (B - (rescale (-1)) B) = if n = 1 then 1 else 0
⊢ bernoulli' n = 0

pp: case inr
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun n ↦ bernoulli' n / ↑n !
this : (B - evalNegHom B) * (exp ℚ - 1) = X * (exp ℚ - 1)
h : ∀ (n : ℕ), (coeff n) (exp ℚ - 1) = (coeff n) 0
⊢ bernoulli' n = 0

Tactic:
· apply eq_zero_of_neg_eq
      specialize h n
      split_ifs at h <;> simp_all [B, h_odd.neg_one_pow, factorial_ne_zero]

Goal state after:
case inr
n : ℕ
h_odd : Odd n
hlt : 1 < n
B : ℚ⟦X⟧ := PowerSeries.mk fun n ↦ bernoulli' n / ↑n !
this : (B - evalNegHom B) * (exp ℚ - 1) = X * (exp ℚ - 1)
h : ∀ (n : ℕ), (coeff n) (exp ℚ - 1) = (coeff n) 0
⊢ bernoulli' n = 0
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: case succ
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
t : A
n : ℕ
⊢ (PowerSeries.coeff (n + 1)) ((PowerSeries.mk fun n ↦ (aeval t) ((1 / ↑n !) • bernoulli n)) * (exp A - 1)) =
    (PowerSeries.coeff (n + 1)) (PowerSeries.X * (rescale t) (exp A))

Tactic:
rw [coeff_succ_X_mul, coeff_rescale, coeff_exp, PowerSeries.coeff_mul,
    Nat.sum_antidiagonal_eq_sum_range_succ_mk, sum_range_succ]
  -- last term is zero so kill with `add_zero`
  simp only [map_sub, tsub_self, constantCoeff_one, constantCoeff_exp,
    coeff_zero_eq_constantCoeff, mul_zero, sub_self, add_zero]
  -- Let's multiply both sides by (n+1)! (OK because it's a unit)
  have hnp1 : IsUnit ((n + 1)! : ℚ) := IsUnit.mk0 _ (mod_cast factorial_ne_zero (n + 1))
  rw [← (hnp1.map (algebraMap ℚ A)).mul_right_inj]
  -- do trivial rearrangements to make RHS (n+1)*t^n
  rw [mul_left_comm, ← map_mul]
  change _ = t ^ n * algebraMap ℚ A (((n + 1) * n ! : ℕ) * (1 / n !))
  rw [cast_mul, mul_assoc,
    mul_one_div_cancel (show (n ! : ℚ) ≠ 0 from cast_ne_zero.2 (factorial_ne_zero n)), mul_one,
    mul_comm (t ^ n), ← aeval_monomial, cast_add, cast_one]
  -- But this is the RHS of `Polynomial.sum_bernoulli`
  rw [← sum_bernoulli, Finset.mul_sum, map_sum]
  -- and now we have to prove a sum is a sum, but all the terms are equal.
  apply Finset.sum_congr rfl
  -- The rest is just trivialities, hampered by the fact that we're coercing
  -- factorials and binomial coefficients between ℕ and ℚ and A.
  intro i hi
  -- deal with coefficients of e^X-1
  simp only [Nat.cast_choose ℚ (mem_range_le hi), coeff_mk, if_neg (mem_range_sub_ne_zero hi),
    PowerSeries.coeff_one, coeff_exp, sub_zero, Algebra.smul_def,
    mul_right_comm _ ((aeval t) _), ← mul_assoc, ← map_mul, ← Polynomial.C_eq_algebraMap,
    Polynomial.aeval_mul, Polynomial.aeval_C]
  -- finally cancel the Bernoulli polynomial and the algebra_map
  field_simp

Goal state after:
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
q : ℕ
f : ℕ → ℕ → ℚ := fun a b ↦ bernoulli a / ↑a ! * (coeff (b + 1)) (exp ℚ ^ n)
⊢ ∑ x ∈ range q.succ, bernoulli x / ↑x ! * (coeff (q - x + 1)) (exp ℚ ^ n) =
    ∑ i ∈ range (q + 1), bernoulli i * ↑((q + 1).choose i) * ↑n ^ (q + 1 - i) / ↑(q + 1)!

Tactic:
apply sum_congr rfl

Goal state after:
n p : ℕ
hne : ∀ (m : ℕ), ↑m ! ≠ 0
q : ℕ
f : ℕ → ℕ → ℚ := ⋯
⊢ ∀ x ∈ range q.succ,
    bernoulli x / ↑x ! * (coeff (q - x + 1)) (exp ℚ ^ n) =
      bernoulli x * ↑((q + 1).choose x) * ↑n ^ (q + 1 - x) / ↑(q + 1)!
Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree

Goal state before:
pp: case pos
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
hb : b ≠ 0
f : Fin m.succ → Fin d → Fq := fun i j ↦ (A i).coeff (b.natDegree - ↑j.succ)
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hj : b.natDegree - d ≤ j
hbj✝ : ↑j < ↑b.natDegree
hbj : j < b.natDegree
hd : b.natDegree < d
⊢ b.natDegree - j.succ < d

Tactic:
exact lt_of_le_of_lt tsub_le_self hd

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 ℤ
I : ↥(Ideal S)⁰
b : S
b_mem : b ∈ ↑I
b_ne_zero : b ≠ 0
min : ∀ (z : ℤ), (∃ b ∈ ↑I, b ≠ 0 ∧ abv ((Algebra.norm R) b) = z) → abv ((Algebra.norm R) b) ≤ z
⊢ ∃ b ∈ ↑I, b ≠ 0 ∧ ∀ c ∈ ↑I, abv ((Algebra.norm R) c) < abv ((Algebra.norm R) b) → c = 0

Tactic:
refine ⟨b, b_mem, b_ne_zero, ?_⟩

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 ℤ
I : ↥(Ideal S)⁰
b : S
b_mem : b ∈ ↑I
b_ne_zero : b ≠ 0
min : ∀ (z : ℤ), (∃ b ∈ ↑I, b ≠ 0 ∧ abv ((Algebra.norm R) b) = z) → abv ((Algebra.norm R) b) ≤ z
⊢ ∀ c ∈ ↑I, abv ((Algebra.norm R) c) < abv ((Algebra.norm R) b) → c = 0
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case inr
k : ℕ
hk : k > 0
h : ¬(bernoulli (2 * k) + ∑ p ∈ range (2 * k + 2) with Nat.Prime p ∧ p - 1 ∣ 2 * k, 1 / ↑p).den = 1
⊢ False

Tactic:
obtain ⟨p, hp, hdvd⟩ := ne_one_iff_exists_prime_dvd.mp h

Goal state after:
case inr
k : ℕ
hk : k > 0
h : ¬(bernoulli (2 * k) + ∑ p ∈ range (2 * k + 2) with Nat.Prime p ∧ p - 1 ∣ 2 * k, 1 / ↑p).den = 1
p : ℕ
hp : Nat.Prime p
hdvd : p ∣ (bernoulli (2 * k) + ∑ p ∈ range (2 * k + 2) with Nat.Prime p ∧ p - 1 ∣ 2 * k, 1 / ↑p).den
⊢ False
Module: Mathlib.NumberTheory.ClassNumber.Finite

Goal state before:
pp: case refine_2
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
inst✝¹ : IsDedekindDomain S
inst✝ : Algebra.IsAlgebraic R S
I : ↥(Ideal S)⁰
M : R := ∏ m ∈ finsetApprox bS adm, m
hM : (algebraMap R S) M ≠ 0
b : S
b_mem : b ∈ ↑I
b_ne_zero : b ≠ 0
b_min : ∀ c ∈ ↑I, abv ((Algebra.norm R) c) < abv ((Algebra.norm R) b) → c = 0
J : Ideal S
hJ : Ideal.span {(algebraMap R S) M} * ↑I = Ideal.span {b} * J
⊢ mk0 I = mk0 ⟨J, ⋯⟩

Tactic:
ClassGroup.mk0_eq_mk0_iff

Goal state after:
case refine_2
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
inst✝¹ : IsDedekindDomain S
inst✝ : Algebra.IsAlgebraic R S
I : ↥(Ideal S)⁰
M : R := ∏ m ∈ finsetApprox bS adm, m
hM : (algebraMap R S) M ≠ 0
b : S
b_mem : b ∈ ↑I
b_ne_zero : b ≠ 0
b_min : ∀ c ∈ ↑I, abv ((Algebra.norm R) c) < abv ((Algebra.norm R) b) → c = 0
J : Ideal S
hJ : Ideal.span {(algebraMap R S) M} * ↑I = Ideal.span {b} * J
⊢ ∃ x y, ∃ (_ : x ≠ 0) (_ : y ≠ 0), Ideal.span {x} * ↑I = Ideal.span {y} * ↑⟨J, ⋯⟩