mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.ModelTheory.Order

Goal state before:
pp: M : Type w
inst✝⁴ : Language.order.Structure M
inst✝³ : M ⊨ Language.order.linearOrderTheory
N : Type w'
inst✝² : Language.order.Structure N
inst✝¹ : N ⊨ Language.order.dlo
inst✝ : Nonempty N
S : Language.order.Substructure M
S_fg : S.FG
f : ↥S ↪[Language.order] N
m : M
this✝⁵ : LinearOrder M := Language.order.linearOrderOfModels M
this✝⁴ : LinearOrder N := Language.order.linearOrderOfModels N
this✝³ : DenselyOrdered N
this✝² : NoBotOrder N
this✝¹ : NoTopOrder N
this✝ : NoMinOrder N
this : NoMaxOrder N
hS : (↑S).Finite
g : ↥(insert m hS.toFinset) ↪o N
hg :
  ⇑g ∘ Set.inclusion ⋯ =
    ⇑(RelEmbedding.trans (OrderIso.setCongr ↑hS.toFinset ↑S ⋯).toOrderEmbedding (OrderEmbedding.ofStrictMono ⇑f ⋯))
g' : ↥((Substructure.closure Language.order).toFun {m} ⊔ S) ↪o N :=
  RelEmbedding.trans
    (OrderIso.setCongr ↑((Substructure.closure Language.order).toFun {m} ⊔ S) ↑(insert m hS.toFinset)
        ⋯).toOrderEmbedding
    g
⊢ ∃ g, f = g.comp (Substructure.inclusion ⋯)

Tactic:
use StrongHomClass.toEmbedding g'

Goal state after:
case h
M : Type w
inst✝⁴ : Language.order.Structure M
inst✝³ : M ⊨ Language.order.linearOrderTheory
N : Type w'
inst✝² : Language.order.Structure N
inst✝¹ : N ⊨ Language.order.dlo
inst✝ : Nonempty N
S : Language.order.Substructure M
S_fg : S.FG
f : ↥S ↪[Language.order] N
m : M
this✝⁵ : LinearOrder M := ⋯
this✝⁴ : LinearOrder N := ⋯
this✝³ : DenselyOrdered N
this✝² : NoBotOrder N
this✝¹ : NoTopOrder N
this✝ : NoMinOrder N
this : NoMaxOrder N
hS : (↑S).Finite
g : ↥(insert m hS.toFinset) ↪o N
hg :
  ⇑g ∘ Set.inclusion ⋯ =
    ⇑(RelEmbedding.trans (OrderIso.setCongr ↑hS.toFinset ↑S ⋯).toOrderEmbedding (OrderEmbedding.ofStrictMono ⇑f ⋯))
g' : ↥((Substructure.closure Language.order).toFun {m} ⊔ S) ↪o N := ⋯
⊢ f = (StrongHomClass.toEmbedding g').comp (Substructure.inclusion ⋯)
Module: Mathlib.ModelTheory.Fraisse

Goal state before:
pp: L : Language
K : Set (Bundled L.Structure)
M : Type w
inst✝⁴ : L.Structure M
N : Type w
inst✝³ : L.Structure N
inst✝² : Countable ((l : ℕ) × L.Functions l)
inst✝¹ : Countable M
inst✝ : Countable N
hM : IsFraisseLimit K M
hN : IsFraisseLimit K N
S : L.Substructure M := ⊥
⊢ Nonempty (M ≃[L] N)

Tactic:
have S_fg : FG L S := (fg_iff_structure_fg _).1 Substructure.fg_bot

Goal state after:
L : Language
K : Set (Bundled L.Structure)
M : Type w
inst✝⁴ : L.Structure M
N : Type w
inst✝³ : L.Structure N
inst✝² : Countable ((l : ℕ) × L.Functions l)
inst✝¹ : Countable M
inst✝ : Countable N
hM : IsFraisseLimit K M
hN : IsFraisseLimit K N
S : L.Substructure M := ⊥
S_fg : Structure.FG L ↥S
⊢ Nonempty (M ≃[L] N)
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: case inl.ha
pqr : Multiset ℕ+
p' q' : ℕ+
H : A' p' q' = pqr
⊢ 0 < (↑↑p')⁻¹

pp: case hb
pqr : Multiset ℕ+
p' q' : ℕ+
H : A' p' q' = pqr
⊢ 0 < (↑↑q')⁻¹

Tactic:
<;>

Goal state after:
case inl.ha
pqr : Multiset ℕ+
p' q' : ℕ+
H : A' p' q' = pqr
⊢ 0 < (↑↑p')⁻¹

case hb
pqr : Multiset ℕ+
p' q' : ℕ+
H : A' p' q' = pqr
⊢ 0 < (↑↑q')⁻¹
Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ λ n = exponent (ZMod n)ˣ

Tactic:
cases n with | zero => contradiction | succ n =>
  change Nat.find _ = _
  grind [exponent, ExponentExists.of_finite]

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

Goal state before:
pp: case neg.a
a b : ℕ
h₀ : a ≠ 0 ∧ b ≠ 0
⊢ exponent (ZMod (a.lcm b))ˣ ∣ (exponent (ZMod a)ˣ).lcm (exponent (ZMod b)ˣ)

Tactic:
← lcm_eq_nat_lcm <| exponent _,

Goal state after:
case neg.a
a b : ℕ
h₀ : a ≠ 0 ∧ b ≠ 0
⊢ exponent (ZMod (a.lcm b))ˣ ∣ GCDMonoid.lcm (exponent (ZMod a)ˣ) (exponent (ZMod b)ˣ)
Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael

Goal state before:
pp: case «0»
n : ℕ
hn : 0 ≤ 2
⊢ φ (2 ^ 0) = 2 ^ (0 - 1)

pp: case «1»
n : ℕ
hn : 1 ≤ 2
⊢ φ (2 ^ 1) = 2 ^ (1 - 1)

pp: case «2»
n : ℕ
hn : 2 ≤ 2
⊢ φ (2 ^ 2) = 2 ^ (2 - 1)

Tactic:
<;>

Goal state after:
case «0»
n : ℕ
hn : 0 ≤ 2
⊢ φ (2 ^ 0) = 2 ^ (0 - 1)

case «1»
n : ℕ
hn : 1 ≤ 2
⊢ φ (2 ^ 1) = 2 ^ (1 - 1)

case «2»
n : ℕ
hn : 2 ≤ 2
⊢ φ (2 ^ 2) = 2 ^ (2 - 1)
Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael

Goal state before:
pp: n : ℕ
hn : 3 ≤ n
⊢ 2 ^ (n - 2).succ = 2 ^ (n - 1) * (2 - 1)

pp: n : ℕ
hn : 3 ≤ n
⊢ 0 < n

pp: n : ℕ
hn : 3 ≤ n
⊢ n ≠ 2

Tactic:
<;>

Goal state after:
n : ℕ
hn : 3 ≤ n
⊢ 2 ^ (n - 2).succ = 2 ^ (n - 1) * (2 - 1)

n : ℕ
hn : 3 ≤ n
⊢ 0 < n

n : ℕ
hn : 3 ≤ n
⊢ n ≠ 2
Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt

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

pp: case inr
n : ℕ
this : ∑ i ∈ n.divisors, ↑(μ i) * -Real.log ↑(n / i) = ∑ i ∈ n.divisors, (↑(μ i) * Real.log ↑i - ↑(μ i) * Real.log ↑n)
hn : n ≠ 1
⊢ ↑(1 n) * Real.log ↑n = 0

Tactic:
<;>

Goal state after:
case inl
n : ℕ
this : ∑ i ∈ n.divisors, ↑(μ i) * -Real.log ↑(n / i) = ∑ i ∈ n.divisors, (↑(μ i) * Real.log ↑i - ↑(μ i) * Real.log ↑n)
hn : n = 1
⊢ ↑(1 n) * Real.log ↑n = 0

case inr
n : ℕ
this : ∑ i ∈ n.divisors, ↑(μ i) * -Real.log ↑(n / i) = ∑ i ∈ n.divisors, (↑(μ i) * Real.log ↑i - ↑(μ i) * Real.log ↑n)
hn : n ≠ 1
⊢ ↑(1 n) * Real.log ↑n = 0
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case refine_2.hnot
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)
this : ∀ (m_1 : ℕ), ∃ y, (1 + ↑p ^ m * ↑a) ^ p ^ m_1 = 1 + ↑p ^ m_1 * ↑p ^ m * (↑a + ↑p * y)
y : ZMod (p ^ (n + 1 + m))
hy : (1 + ↑p ^ m * ↑a) ^ p ^ n = 1 + ↑p ^ n * ↑p ^ m * (↑a + ↑p * y)
⊢ ¬↑(p ^ (n + m)) * ↑a = 0

Tactic:
rwa [← Int.cast_natCast, ← Int.cast_mul, ZMod.intCast_zmod_eq_zero_iff_dvd, add_right_comm,
          pow_succ, Nat.cast_mul, Int.mul_dvd_mul_iff_left (by simp [hp.ne_zero])]

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

Goal state before:
pp: case refine_2.hnot
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)
this : ∀ (m_1 : ℕ), ∃ y, (1 + ↑p ^ m * ↑a) ^ p ^ m_1 = 1 + ↑p ^ m_1 * ↑p ^ m * (↑a + ↑p * y)
⊢ ¬(1 + ↑p ^ m * ↑a) ^ p ^ n = 1

Tactic:
obtain ⟨y, hy⟩ := this n
        rw [hy, ← pow_add, add_eq_left, mul_add, ← mul_assoc, ← pow_succ]
        simp_rw [add_right_comm n _ 1, ← Nat.cast_pow, ZMod.natCast_self, zero_mul, add_zero]
        rwa [← Int.cast_natCast, ← Int.cast_mul, ZMod.intCast_zmod_eq_zero_iff_dvd, add_right_comm,
          pow_succ, Nat.cast_mul, Int.mul_dvd_mul_iff_left (by simp [hp.ne_zero])]

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

Goal state before:
pp: 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
⊢ orderOf ((Units.coeHom (ZMod (p ^ (n + 1)))) ha.unit) = p ^ n

Tactic:
Units.coeHom_apply,

Goal state after:
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
⊢ orderOf ↑ha.unit = p ^ n
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case inr.inr.inl
n : ℕ
hn0 : 2 * n ≠ 0
hn1 : 2 * n ≠ 1
⊢ ¬IsCyclic (ZMod (4 * (2 * n)))ˣ

pp: case inr.inr.inr
n : ℕ
hn0 : n ≠ 0
hn1 : n ≠ 1
h2n : ¬2 ∣ n
⊢ ¬IsCyclic (ZMod (4 * n))ˣ

Tactic:
· rw [← mul_assoc]
    have : NeZero n := ⟨by simpa using hn0⟩
    refine mt (fun _ ↦ ?_) not_isCyclic_units_eight
    exact isCyclic_of_surjective _ (ZMod.unitsMap_surjective (m := 4 * 2 * n) (dvd_mul_right 8 _))

Goal state after:
case inr.inr.inr
n : ℕ
hn0 : n ≠ 0
hn1 : n ≠ 1
h2n : ¬2 ∣ n
⊢ ¬IsCyclic (ZMod (4 * n))ˣ
Module: Mathlib.RingTheory.MvPowerSeries.Derivative

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
n : σ →₀ ℕ
h✝ : n = 0
⊢ ↑(n i) + 1 = 1

pp: case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
n : σ →₀ ℕ
h✝ : ¬n = 0
⊢ 0 = 0

Tactic:
<;>

Goal state after:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
n : σ →₀ ℕ
h✝ : n = 0
⊢ ↑(n i) + 1 = 1

case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
n : σ →₀ ℕ
h✝ : ¬n = 0
⊢ 0 = 0
Module: Mathlib.RingTheory.MvPowerSeries.Derivative

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsAddTorsionFree R
f g : MvPowerSeries σ R
hD : ∀ (i : σ), (pderiv R i) f = (pderiv R i) g
hc : constantCoeff f = constantCoeff g
n : σ →₀ ℕ
h : ¬n = 0
i : σ
hi : n i ≠ 0
j : σ
hj : j = i
⊢ (single i 1) j ≤ n j

pp: case neg
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsAddTorsionFree R
f g : MvPowerSeries σ R
hD : ∀ (i : σ), (pderiv R i) f = (pderiv R i) g
hc : constantCoeff f = constantCoeff g
n : σ →₀ ℕ
h : ¬n = 0
i : σ
hi : n i ≠ 0
j : σ
hj : ¬j = i
⊢ (single i 1) j ≤ n j

Tactic:
<;>

Goal state after:
case pos
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsAddTorsionFree R
f g : MvPowerSeries σ R
hD : ∀ (i : σ), (pderiv R i) f = (pderiv R i) g
hc : constantCoeff f = constantCoeff g
n : σ →₀ ℕ
h : ¬n = 0
i : σ
hi : n i ≠ 0
j : σ
hj : j = i
⊢ (single i 1) j ≤ n j

case neg
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsAddTorsionFree R
f g : MvPowerSeries σ R
hD : ∀ (i : σ), (pderiv R i) f = (pderiv R i) g
hc : constantCoeff f = constantCoeff g
n : σ →₀ ℕ
h : ¬n = 0
i : σ
hi : n i ≠ 0
j : σ
hj : ¬j = i
⊢ (single i 1) j ≤ n j
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case inl
hn : Odd 1
hn0 : 1 ≠ 0
⊢ IsCyclic (ZMod 1)ˣ ↔ ∃ p m, Nat.Prime p ∧ Odd p ∧ 1 = p ^ m

pp: case inr
n : ℕ
hn : Odd n
hn0 : n ≠ 0
h1 : n ≠ 1
⊢ IsCyclic (ZMod n)ˣ ↔ ∃ p m, Nat.Prime p ∧ Odd p ∧ n = p ^ m

Tactic:
· simp_rw [isCyclic_units_one, true_iff]
    exact ⟨3, 0, Nat.prime_three, by simp [Nat.odd_iff], by rw [pow_zero]⟩

Goal state after:
case inr
n : ℕ
hn : Odd n
hn0 : n ≠ 0
h1 : n ≠ 1
⊢ IsCyclic (ZMod n)ˣ ↔ ∃ p m, Nat.Prime p ∧ Odd p ∧ n = p ^ m
Module: Mathlib.RingTheory.PowerSeries.Derivative

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommSemiring R
f : R⟦X⟧
⊢ (trunc (0 - 1)) ((d⁄dX R) f) = Polynomial.derivative ((trunc 0) f)

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

Tactic:
<;>

Goal state after:
case zero
R : Type u_1
inst✝ : CommSemiring R
f : R⟦X⟧
⊢ (trunc (0 - 1)) ((d⁄dX R) f) = Polynomial.derivative ((trunc 0) f)

case succ
R : Type u_1
inst✝ : CommSemiring R
f : R⟦X⟧
n✝ : ℕ
⊢ (trunc (n✝ + 1 - 1)) ((d⁄dX R) f) = Polynomial.derivative ((trunc (n✝ + 1)) f)
Module: Mathlib.RingTheory.PowerSeries.Derivative

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
f g : R⟦X⟧
hg : HasSubst g
n m : ℕ
hm : ∀ (b : ℕ), m ≤ b → ∀ n' ≤ n + 1, (coeff n') (g ^ b) = 0
this : (coeff (n + 1)) (subst g f) = (coeff (n + 1)) (subst g ↑((trunc (m + 1)) f))
x✝ : ℕ × ℕ
i j : ℕ
hij : (i, j) ∈ Finset.antidiagonal n
d : ℕ
h✝ : d + 1 < m + 1
⊢ ((coeff (d + 1)) f * (↑d + 1)) • (coeff i) (g ^ d) = ((coeff (d + 1)) f * (↑d + 1)) • (coeff i) (g ^ d)

pp: case neg
R : Type u_1
inst✝ : CommRing R
f g : R⟦X⟧
hg : HasSubst g
n m : ℕ
hm : ∀ (b : ℕ), m ≤ b → ∀ n' ≤ n + 1, (coeff n') (g ^ b) = 0
this : (coeff (n + 1)) (subst g f) = (coeff (n + 1)) (subst g ↑((trunc (m + 1)) f))
x✝ : ℕ × ℕ
i j : ℕ
hij : (i, j) ∈ Finset.antidiagonal n
d : ℕ
h✝ : ¬d + 1 < m + 1
⊢ (0 * (↑d + 1)) • (coeff i) (g ^ d) = ((coeff (d + 1)) f * (↑d + 1)) • (coeff i) (g ^ d)

Tactic:
<;>

Goal state after:
case pos
R : Type u_1
inst✝ : CommRing R
f g : R⟦X⟧
hg : HasSubst g
n m : ℕ
hm : ∀ (b : ℕ), m ≤ b → ∀ n' ≤ n + 1, (coeff n') (g ^ b) = 0
this : (coeff (n + 1)) (subst g f) = (coeff (n + 1)) (subst g ↑((trunc (m + 1)) f))
x✝ : ℕ × ℕ
i j : ℕ
hij : (i, j) ∈ Finset.antidiagonal n
d : ℕ
h✝ : d + 1 < m + 1
⊢ ((coeff (d + 1)) f * (↑d + 1)) • (coeff i) (g ^ d) = ((coeff (d + 1)) f * (↑d + 1)) • (coeff i) (g ^ d)

case neg
R : Type u_1
inst✝ : CommRing R
f g : R⟦X⟧
hg : HasSubst g
n m : ℕ
hm : ∀ (b : ℕ), m ≤ b → ∀ n' ≤ n + 1, (coeff n') (g ^ b) = 0
this : (coeff (n + 1)) (subst g f) = (coeff (n + 1)) (subst g ↑((trunc (m + 1)) f))
x✝ : ℕ × ℕ
i j : ℕ
hij : (i, j) ∈ Finset.antidiagonal n
d : ℕ
h✝ : ¬d + 1 < m + 1
⊢ (0 * (↑d + 1)) • (coeff i) (g ^ d) = ((coeff (d + 1)) f * (↑d + 1)) • (coeff i) (g ^ d)
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)
⊢ (coeff (n + 1)) f = (coeff (n + 1)) (exp A)

Tactic:
have eq1 : coeff n (d⁄dX A f) = coeff n f := congrArg (coeff n) hd

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) ((d⁄dX A) f) = (coeff n) f
⊢ (coeff (n + 1)) f = (coeff (n + 1)) (exp A)
Module: Mathlib.RingTheory.PowerSeries.Exp

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

pp: case e'_3
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
this :
  a ^ x * b ^ (n - x) * ((algebraMap ℚ A) (1 / ↑x !) * (algebraMap ℚ A) (1 / ↑(n - x)!)) =
    a ^ x * b ^ (n - x) * (↑(n.choose x) * (algebraMap ℚ A) (1 / ↑n !))
⊢ a ^ x * b ^ (n - x) * ↑(n.choose x) * (algebraMap ℚ A) (1 / ↑n !) =
    a ^ x * b ^ (n - x) * (↑(n.choose x) * (algebraMap ℚ A) (1 / ↑n !))

Tactic:
<;>

Goal state after:
case e'_2
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
this :
  a ^ x * b ^ (n - x) * ((algebraMap ℚ A) (1 / ↑x !) * (algebraMap ℚ A) (1 / ↑(n - x)!)) =
    a ^ x * b ^ (n - x) * (↑(n.choose x) * (algebraMap ℚ A) (1 / ↑n !))
⊢ a ^ x * (algebraMap ℚ A) (1 / ↑x !) * (b ^ (n - x) * (algebraMap ℚ A) (1 / ↑(n - x)!)) =
    a ^ x * b ^ (n - x) * ((algebraMap ℚ A) (1 / ↑x !) * (algebraMap ℚ A) (1 / ↑(n - x)!))

case e'_3
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
a b : A
n x : ℕ
hx : x ∈ Finset.range n.succ
this :
  a ^ x * b ^ (n - x) * ((algebraMap ℚ A) (1 / ↑x !) * (algebraMap ℚ A) (1 / ↑(n - x)!)) =
    a ^ x * b ^ (n - x) * (↑(n.choose x) * (algebraMap ℚ A) (1 / ↑n !))
⊢ a ^ x * b ^ (n - x) * ↑(n.choose x) * (algebraMap ℚ A) (1 / ↑n !) =
    a ^ x * b ^ (n - x) * (↑(n.choose x) * (algebraMap ℚ A) (1 / ↑n !))
Module: Mathlib.RingTheory.PowerSeries.Exp

Goal state before:
pp: case e'_2.e'_5
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ exp A = (rescale 1) (exp A)

pp: case e'_3
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ 1 = (rescale (1 + -1)) (exp A)

Tactic:
<;>

Goal state after:
case e'_2.e'_5
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ exp A = (rescale 1) (exp A)

case e'_3
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
⊢ 1 = (rescale (1 + -1)) (exp A)
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: case e'_2.a.h₁
n i : ℕ
h : i ≤ n
x✝ : ℕ
a✝ : x✝ ∈ range (n + 1)
⊢ n - x✝ = i ↔ n - i = x✝

pp: case e'_3
n i : ℕ
h : i ≤ n
⊢ n.choose i = n.choose (n - i)

Tactic:
<;>

Goal state after:
case e'_2.a.h₁
n i : ℕ
h : i ≤ n
x✝ : ℕ
a✝ : x✝ ∈ range (n + 1)
⊢ n - x✝ = i ↔ n - i = x✝

case e'_3
n i : ℕ
h : i ≤ n
⊢ n.choose i = n.choose (n - i)
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: case inr.hac
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
ha : 0 ≤ a
hab : a ≤ b
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc a b) volume
aux1 : ↑⌊a⌋₊ ≤ a
aux2 : b ≤ ↑⌊b⌋₊ + 1
hb : ⌊a⌋₊ < ⌊b⌋₊
aux3 : a ≤ ↑⌊a⌋₊ + 1
aux4 : ↑⌊a⌋₊ + 1 ≤ b
aux5 : ↑⌊b⌋₊ ≤ b
aux6 : a ≤ ↑⌊b⌋₊
this :
  ∑ k ∈ Ioc ⌊a⌋₊ (⌊b⌋₊ - 1), (f ↑(k + 1) - f ↑k) * ∑ n ∈ Icc 0 k, c n =
    ∑ k ∈ Ico (⌊a⌋₊ + 1) ⌊b⌋₊, ∫ (t : ℝ) in ↑k..↑(k + 1), deriv f t * ∑ n ∈ Icc 0 ⌊t⌋₊, c n
⊢ IntervalIntegrable (fun x ↦ deriv f x * ∑ n ∈ Icc 0 ⌊x⌋₊, c n) volume a (↑⌊a⌋₊ + 1)

Tactic:
rw [intervalIntegrable_iff_integrableOn_Icc_of_le aux3]
    exact (integrableOn_mul_sum_Icc c ha hf_int).mono_set (Set.Icc_subset_Icc_right aux4)

Goal state after:
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: case zero
⊢ π (0 - 1) = π' 0

pp: case succ
n✝ : ℕ
⊢ π (n✝ + 1 - 1) = π' (n✝ + 1)

Tactic:
<;>

Goal state after:
case zero
⊢ π (0 - 1) = π' 0

case succ
n✝ : ℕ
⊢ π (n✝ + 1 - 1) = π' (n✝ + 1)
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: case zero
⊢ primesBelow 0 = (0 - 1).primesLE

pp: case succ
n✝ : ℕ
⊢ (n✝ + 1).primesBelow = (n✝ + 1 - 1).primesLE

Tactic:
<;>

Goal state after:
case zero
⊢ primesBelow 0 = (0 - 1).primesLE

case succ
n✝ : ℕ
⊢ (n✝ + 1).primesBelow = (n✝ + 1 - 1).primesLE
Module: Mathlib.NumberTheory.PrimeCounting

Goal state before:
pp: n : ℕ
⊢ #n.primesBelow = π' n

Tactic:
simp only [primesBelow, primeCounting']

Goal state after:
n : ℕ
⊢ #({p ∈ range n | Prime p}) = count Prime n
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 (0 + 1) +
        (f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f 1 * (c 0 + ∑ x ∈ Ioc 0 (0 + 1), c x) -
          ∫ (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:
Nat.Ioc_succ_singleton,

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 * c 0 +
      (f 1 * c (0 + 1) +
        (f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f 1 * (c 0 + ∑ x ∈ {0 + 1}, c x) -
          ∫ (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.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 : B - evalNegHom B = X
⊢ 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 : exp ℚ - 1 = 0
⊢ bernoulli' n = 0

Tactic:
<;>

Goal state after:
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 : B - evalNegHom B = X
⊢ bernoulli' n = 0

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 : exp ℚ - 1 = 0
⊢ bernoulli' n = 0
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: case pos
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 = 1
h : (coeff n) (B - (rescale (-1)) B) = 1
⊢ -bernoulli' n = bernoulli' n

pp: case neg
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 = 1
h : (coeff n) (B - (rescale (-1)) B) = 0
⊢ -bernoulli' n = bernoulli' n

Tactic:
<;>

Goal state after:
case pos
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 = 1
h : (coeff n) (B - (rescale (-1)) B) = 1
⊢ -bernoulli' n = bernoulli' n

case neg
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 = 1
h : (coeff n) (B - (rescale (-1)) B) = 0
⊢ -bernoulli' n = bernoulli' n
Module: Mathlib.NumberTheory.BernoulliPolynomials

Goal state before:
pp: case neg.inr
n i : ℕ
h✝ : i ≤ n + 1
h' : ¬i = n + 1 - 1
h : Odd (n + 1 - i)
⊢ 0 * ↑((n + 1).choose i) * (-1) ^ i = (-1) ^ (n + 1) • (0 * ↑((n + 1).choose i) + (n + 1) • 0)

pp: case neg.inr.h_odd
n i : ℕ
h✝ : i ≤ n + 1
h' : ¬i = n + 1 - 1
h : Odd (n + 1 - i)
⊢ Odd (n + 1 - i)

pp: case neg.inr.hlt
n i : ℕ
h✝ : i ≤ n + 1
h' : ¬i = n + 1 - 1
h : Odd (n + 1 - i)
⊢ 1 < n + 1 - i

Tactic:
<;>

Goal state after:
case neg.inr
n i : ℕ
h✝ : i ≤ n + 1
h' : ¬i = n + 1 - 1
h : Odd (n + 1 - i)
⊢ 0 * ↑((n + 1).choose i) * (-1) ^ i = (-1) ^ (n + 1) • (0 * ↑((n + 1).choose i) + (n + 1) • 0)

case neg.inr.h_odd
n i : ℕ
h✝ : i ≤ n + 1
h' : ¬i = n + 1 - 1
h : Odd (n + 1 - i)
⊢ Odd (n + 1 - i)

case neg.inr.hlt
n i : ℕ
h✝ : i ≤ n + 1
h' : ¬i = n + 1 - 1
h : Odd (n + 1 - i)
⊢ 1 < n + 1 - i
Module: Mathlib.NumberTheory.Bernoulli

Goal state before:
pp: n : ℕ
h₁ : (1, n) ∈ antidiagonal n.succ
h₃ : (1 + n).choose n = n + 1
H :
  ↑(((1, n).1 + (1, n).2).choose (1, n).2) / (↑(1, n).2 + 1) * bernoulli' (1, n).1 +
      ∑ x ∈ antidiagonal n.succ \ {(1, n)}, ↑((x.1 + x.2).choose x.2) / (↑x.2 + 1) * bernoulli' x.1 =
    1
p : ℕ × ℕ
h : p ∈ antidiagonal n.succ \ {(1, n)}
⊢ p ∈ ?m.256 ∧ p ≠ ?m.258

Tactic:
rwa [mem_sdiff, mem_singleton] at h

Goal state after:
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun x ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3))
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : √(2 * 512) = 32
| 32

Tactic:
← Nat.cast_ofNat

Goal state after:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun x ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3))
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : √(2 * 512) = 32
| ↑32
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: case refine_2
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun x ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3))
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : √(2 * 512) = 32
⊢ 2 ^ (9 + 10 * 32) ≤ (2 ^ 2) ^ (512 / 3)

Tactic:
rw [← rpow_mul, ← rpow_natCast]

Goal state after:
case refine_2
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun x ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3))
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : √(2 * 512) = 32
⊢ 2 ^ ↑(9 + 10 * 32) ≤ 2 ^ (2 * (512 / 3))

case refine_2.hx
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun x ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3))
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : √(2 * 512) = 32
⊢ 0 ≤ 2
Module: Mathlib.NumberTheory.Bertrand

Goal state before:
pp: 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 ℕ := {p ∈ Finset.range (2 * n / 3 + 1) | Nat.Prime p}
⊢ n.centralBinom ≤ (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3)

Tactic:
let f x := x ^ n.centralBinom.factorization x

Goal state after:
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 ℕ := {p ∈ Finset.range (2 * n / 3 + 1) | Nat.Prime p}
f : ℕ → ℕ := fun x ↦ x ^ n.centralBinom.factorization x
⊢ n.centralBinom ≤ (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3)