mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: case inr.inl
pqr : Multiset ℕ+
n : ℕ+
H : D' n = pqr
⊢ 1 < (↑↑2)⁻¹ + (↑↑2)⁻¹ + (↑↑n)⁻¹

Tactic:
]

Goal state after:
case inr.inl
pqr : Multiset ℕ+
n : ℕ+
H : D' n = pqr
⊢ 1 < (↑↑2)⁻¹ + (↑↑2)⁻¹ + (↑↑n)⁻¹
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: case inr.inr.inl
pqr : Multiset ℕ+
H : E' 3 = pqr
⊢ 1 < (↑↑2)⁻¹ + (↑↑3)⁻¹ + (↑↑3)⁻¹

Tactic:
]

Goal state after:
case inr.inr.inl
pqr : Multiset ℕ+
H : E' 3 = pqr
⊢ 1 < (↑↑2)⁻¹ + (↑↑3)⁻¹ + (↑↑3)⁻¹
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: case inr.inr.inr.inl
pqr : Multiset ℕ+
H : E' 4 = pqr
⊢ 1 < (↑↑2)⁻¹ + (↑↑3)⁻¹ + (↑↑4)⁻¹

Tactic:
]

Goal state after:
case inr.inr.inr.inl
pqr : Multiset ℕ+
H : E' 4 = pqr
⊢ 1 < (↑↑2)⁻¹ + (↑↑3)⁻¹ + (↑↑4)⁻¹
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: case inr.inr.inr.inr
pqr : Multiset ℕ+
H : E' 5 = pqr
⊢ 1 < (↑↑2)⁻¹ + (↑↑3)⁻¹ + (↑↑5)⁻¹

Tactic:
]

Goal state after:
case inr.inr.inr.inr
pqr : Multiset ℕ+
H : E' 5 = pqr
⊢ 1 < (↑↑2)⁻¹ + (↑↑3)⁻¹ + (↑↑5)⁻¹
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 3 ≤ p
⊢ (↑↑p)⁻¹ + (↑↑q)⁻¹ + (↑↑r)⁻¹ ≤ 1

Tactic:
]

Goal state after:
p q r : ℕ+
hpq : p ≤ q
hqr : q ≤ r
H : 3 ≤ p
⊢ (↑↑p)⁻¹ + (↑↑q)⁻¹ + (↑↑r)⁻¹ ≤ 1
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: q r : ℕ+
hqr : q ≤ r
H : 4 ≤ q
⊢ (↑↑2)⁻¹ + (↑↑q)⁻¹ + (↑↑r)⁻¹ ≤ 1

Tactic:
]

Goal state after:
q r : ℕ+
hqr : q ≤ r
H : 4 ≤ q
⊢ (↑↑2)⁻¹ + (↑↑q)⁻¹ + (↑↑r)⁻¹ ≤ 1
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: r : ℕ+
H : 6 ≤ r
⊢ (↑↑2)⁻¹ + (↑↑3)⁻¹ + (↑↑r)⁻¹ ≤ 1

Tactic:
]

Goal state after:
r : ℕ+
H : 6 ≤ r
⊢ (↑↑2)⁻¹ + (↑↑3)⁻¹ + (↑↑r)⁻¹ ≤ 1
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: p q r : ℕ+
H : 1 < sumInv {p, q, r}
S : List ℕ+ := {p, q, r}.sort fun a b ↦ a ≤ b
hS : S.SortedLE
hpqr : {p, q, r} = ↑S
⊢ (∃ q r, A' q r = ↑S) ∨ (∃ r, D' r = ↑S) ∨ E' 3 = ↑S ∨ E' 4 = ↑S ∨ E' 5 = ↑S

Tactic:
]

Goal state after:
p q r : ℕ+
H : 1 < sumInv {p, q, r}
S : List ℕ+ := {p, q, r}.sort fun a b ↦ a ≤ b
hS : S.SortedLE
hpqr : {p, q, r} = ↑S
⊢ (∃ q r, A' q r = ↑S) ∨ (∃ r, D' r = ↑S) ∨ E' 3 = ↑S ∨ E' 4 = ↑S ∨ E' 5 = ↑S
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: ⊢ ¬Monoid.exponent (ZMod 8)ˣ = φ 8

Tactic:
]

Goal state after:
⊢ ¬Monoid.exponent (ZMod 8)ˣ = φ 8
Module: Mathlib.NumberTheory.ADEInequality

Goal state before:
pp: p q r : ℕ+
S : List ℕ+ := {p, q, r}.sort fun a b ↦ a ≤ b
H : 1 < sumInv ↑S
hS : S.SortedLE
hpqr : {p, q, r} = ↑S
⊢ (∃ q r, A' q r = ↑S) ∨ (∃ r, D' r = ↑S) ∨ E' 3 = ↑S ∨ E' 4 = ↑S ∨ E' 5 = ↑S

Tactic:
]

Goal state after:
p q r : ℕ+
S : List ℕ+ := {p, q, r}.sort fun a b ↦ a ≤ b
H : 1 < sumInv ↑S
hS : S.SortedLE
hpqr : {p, q, r} = ↑S
⊢ (∃ q r, A' q r = ↑S) ∨ (∃ r, D' r = ↑S) ∨ E' 3 = ↑S ∨ E' 4 = ↑S ∨ E' 5 = ↑S
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
hvu : v ∣ u
hpuv : ↑p * u * v ∣ u ^ p
x : R
⊢ ∃ y, ∑ m ∈ Finset.range (p + 1), (u * x) ^ m * 1 ^ (p - m) * ↑(p.choose m) = 1 + ↑p * u * (x + v * y)

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
hvu : v ∣ u
hpuv : ↑p * u * v ∣ u ^ p
x : R
⊢ ∃ y, ∑ m ∈ Finset.range (p + 1), (u * x) ^ m * 1 ^ (p - m) * ↑(p.choose m) = 1 + ↑p * u * (x + v * y)
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
hvu : v ∣ u
hpuv : ↑p * u * v ∣ u ^ p
x : R
⊢ ∃ y,
    (u * x) ^ 0 * 1 ^ (p - 0) * ↑(p.choose 0) +
        ∑ x_1 ∈ (Finset.range (p + 1)).erase 0, (u * x) ^ x_1 * 1 ^ (p - x_1) * ↑(p.choose x_1) =
      1 + ↑p * u * (x + v * y)

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
hvu : v ∣ u
hpuv : ↑p * u * v ∣ u ^ p
x : R
⊢ ∃ y,
    (u * x) ^ 0 * 1 ^ (p - 0) * ↑(p.choose 0) +
        ∑ x_1 ∈ (Finset.range (p + 1)).erase 0, (u * x) ^ x_1 * 1 ^ (p - x_1) * ↑(p.choose x_1) =
      1 + ↑p * u * (x + v * y)
Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael

Goal state before:
pp: case succ
n : ℕ
hn : n + 1 ≠ 0
⊢ Nat.find ⋯ = exponent (ZMod (n + 1))ˣ

Tactic:
grind [exponent, ExponentExists.of_finite]

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

Goal state before:
pp: case zero
a : (ZMod 0)ˣ
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: case succ
n✝ : ℕ
a : (ZMod (n✝ + 1))ˣ
⊢ a ^ exponent (ZMod (n✝ + 1))ˣ = 1

Tactic:
]

Goal state after:
case succ
n✝ : ℕ
a : (ZMod (n✝ + 1))ˣ
⊢ a ^ exponent (ZMod (n✝ + 1))ˣ = 1
Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael

Goal state before:
pp: case succ
n✝ : ℕ
⊢ exponent (ZMod (n✝ + 1))ˣ ∣ Fintype.card (ZMod (n✝ + 1))ˣ

Tactic:
]

Goal state after:
case succ
n✝ : ℕ
⊢ exponent (ZMod (n✝ + 1))ˣ ∣ Fintype.card (ZMod (n✝ + 1))ˣ
Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael

Goal state before:
pp: case succ
a n✝ : ℕ
h : a ∣ n✝ + 1
⊢ exponent (ZMod a)ˣ ∣ exponent (ZMod (n✝ + 1))ˣ

Tactic:
]

Goal state after:
case succ
a n✝ : ℕ
h : a ∣ n✝ + 1
⊢ exponent (ZMod a)ˣ ∣ exponent (ZMod (n✝ + 1))ˣ
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 × ZMod b)ˣ

Tactic:
]

Goal state after:
case neg.a
a b : ℕ
h₀ : a ≠ 0 ∧ b ≠ 0
⊢ exponent (ZMod (a.lcm b))ˣ ∣ exponent (ZMod a × ZMod b)ˣ
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
hvu : v ∣ u
hpuv : ↑p * u * v ∣ u ^ p
x : R
⊢ ∃ y,
    1 +
        ((u * x) ^ 1 * ↑(p.choose 1) +
          ∑ x_1 ∈ ((Finset.range (p + 1)).erase 0).erase 1, (u * x) ^ x_1 * ↑(p.choose x_1)) =
      1 + ↑p * u * (x + v * y)

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
hvu : v ∣ u
hpuv : ↑p * u * v ∣ u ^ p
x : R
⊢ ∃ y,
    1 +
        ((u * x) ^ 1 * ↑(p.choose 1) +
          ∑ x_1 ∈ ((Finset.range (p + 1)).erase 0).erase 1, (u * x) ^ x_1 * ↑(p.choose x_1)) =
      1 + ↑p * u * (x + v * y)
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
m n : ℕ
t : ℝ
h : Set.Ico (↑n) (↑n + 1) t = Set.Icc (↑n) (↑n + 1) t
ht : t ∈ Set.Icc (↑n) (↑n + 1)
⊢ ∑ k ∈ Icc m n, c k = ∑ k ∈ Icc m n, c k

Tactic:
]

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
hvu : v ∣ u
hpuv : ↑p * u * v ∣ u ^ p
x : R
⊢ 2 ≤ p ∧ p ∈ Finset.range (p + 1)

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
hvu : v ∣ u
hpuv : ↑p * u * v ∣ u ^ p
x : R
⊢ 2 ≤ p ∧ p ∈ Finset.range (p + 1)
Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael

Goal state before:
pp: case refine_2
α : Type u_2
s✝ : Finset α
f : α → ℕ
a : α
s : Finset α
ha : a ∉ s
ih : λ (s.lcm f) = s.lcm (⇑λ ∘ f)
⊢ λ (GCDMonoid.lcm (f a) (s.lcm f)) = GCDMonoid.lcm ((⇑λ ∘ f) a) (λ (s.lcm f))

Tactic:
]

Goal state after:
case refine_2
α : Type u_2
s✝ : Finset α
f : α → ℕ
a : α
s : Finset α
ha : a ∉ s
ih : λ (s.lcm f) = s.lcm (⇑λ ∘ f)
⊢ λ (GCDMonoid.lcm (f a) (s.lcm f)) = GCDMonoid.lcm ((⇑λ ∘ f) a) (λ (s.lcm f))
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
hvu : v ∣ u
hpuv : ↑p * u * v ∣ u ^ p
x : R
⊢ ∃ y,
    1 +
        ((u * x) ^ 1 * ↑(p.choose 1) +
          (∑ x_1 ∈ (((Finset.range (p + 1)).erase 0).erase 1).erase p, (u * x) ^ x_1 * ↑(p.choose x_1) +
            (u * x) ^ p * ↑(p.choose p))) =
      1 + ↑p * u * (x + v * y)

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
u v : R
p : ℕ
hp : Nat.Prime p
hvu : v ∣ u
hpuv : ↑p * u * v ∣ u ^ p
x : R
⊢ ∃ y,
    1 +
        ((u * x) ^ 1 * ↑(p.choose 1) +
          (∑ x_1 ∈ (((Finset.range (p + 1)).erase 0).erase 1).erase p, (u * x) ^ x_1 * ↑(p.choose x_1) +
            (u * x) ^ p * ↑(p.choose p))) =
      1 + ↑p * u * (x + v * y)
Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ λ (n.factorization.prod fun x1 x2 ↦ x1 ^ x2) = n.primeFactors.lcm fun p ↦ λ (p ^ n.factorization p)

Tactic:
]

Goal state after:
n : ℕ
inst✝ : NeZero n
⊢ λ (n.factorization.prod fun x1 x2 ↦ x1 ^ x2) = n.primeFactors.lcm fun p ↦ λ (p ^ n.factorization p)
Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael

Goal state before:
pp: n : ℕ
hn : n ≤ 2
⊢ exponent (ZMod (2 ^ n))ˣ = Nat.card (ZMod (2 ^ n))ˣ

Tactic:
]

Goal state after:
n : ℕ
hn : n ≤ 2
⊢ exponent (ZMod (2 ^ n))ˣ = Nat.card (ZMod (2 ^ n))ˣ
Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael

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

Tactic:
]

Goal state after:
n : ℕ
hn : n ≤ 2
⊢ φ (2 ^ n) = 2 ^ (n - 1)
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc a b) volume
t₁ t₂ : ℝ
n : ℕ
h : t₁ ≤ t₂
h₁ : ↑n ≤ t₁
h₂ : t₂ ≤ ↑n + 1
h₃ : a ≤ t₁
h₄ : t₂ ≤ b
h_inc₁ : Ι t₁ t₂ ⊆ Set.Icc (↑n) (↑n + 1)
h_inc₂ : [[t₁, t₂]] ⊆ Set.Icc a b
⊢ ∫ (t : ℝ) in t₁..t₂, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k = ∫ (x : ℝ) in t₁..t₂, deriv f x * ∑ k ∈ Icc 0 n, c k

pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc a b) volume
t₁ t₂ : ℝ
n : ℕ
h : t₁ ≤ t₂
h₁ : ↑n ≤ t₁
h₂ : t₂ ≤ ↑n + 1
h₃ : a ≤ t₁
h₄ : t₂ ≤ b
h_inc₁ : Ι t₁ t₂ ⊆ Set.Icc (↑n) (↑n + 1)
h_inc₂ : [[t₁, t₂]] ⊆ Set.Icc a b
⊢ IntervalIntegrable (deriv f) volume t₁ t₂

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc a b) volume
t₁ t₂ : ℝ
n : ℕ
h : t₁ ≤ t₂
h₁ : ↑n ≤ t₁
h₂ : t₂ ≤ ↑n + 1
h₃ : a ≤ t₁
h₄ : t₂ ≤ b
h_inc₁ : Ι t₁ t₂ ⊆ Set.Icc (↑n) (↑n + 1)
h_inc₂ : [[t₁, t₂]] ⊆ Set.Icc a b
⊢ ∫ (t : ℝ) in t₁..t₂, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k = ∫ (x : ℝ) in t₁..t₂, deriv f x * ∑ k ∈ Icc 0 n, c k

𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc a b) volume
t₁ t₂ : ℝ
n : ℕ
h : t₁ ≤ t₂
h₁ : ↑n ≤ t₁
h₂ : t₂ ≤ ↑n + 1
h₃ : a ≤ t₁
h₄ : t₂ ≤ b
h_inc₁ : Ι t₁ t₂ ⊆ Set.Icc (↑n) (↑n + 1)
h_inc₂ : [[t₁, t₂]] ⊆ Set.Icc a b
⊢ IntervalIntegrable (deriv f) volume t₁ t₂
Module: Mathlib.NumberTheory.ArithmeticFunction.Carmichael

Goal state before:
pp: n : ℕ
hn : n ≠ 2
hn' : ¬n ≤ 2
⊢ 2 ^ (n - 1) = 2 ^ (n - 1)

Tactic:
]

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

Goal state before:
pp: case h
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
⊢ 1 +
      ((u * x) ^ 1 * ↑(p.choose 1) +
        (∑ x_1 ∈ (((Finset.range (p + 1)).erase 0).erase 1).erase p, (u * x) ^ x_1 * ↑(p.choose x_1) +
          (u * x) ^ p * ↑(p.choose p))) =
    1 +
      (↑p * u * x +
        ↑p * u *
          (v *
            (a * x ^ 2 *
                ∑ i ∈ (((Finset.range (p + 1)).erase 0).erase 1).erase p, (u * x) ^ (i - 2) * ↑(p.choose i / p) +
              b * x ^ p)))

Tactic:
]

Goal state after:
case h
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
⊢ 1 +
      ((u * x) ^ 1 * ↑(p.choose 1) +
        (∑ x_1 ∈ (((Finset.range (p + 1)).erase 0).erase 1).erase p, (u * x) ^ x_1 * ↑(p.choose x_1) +
          (u * x) ^ p * ↑(p.choose p))) =
    1 +
      (↑p * u * x +
        ↑p * u *
          (v *
            (a * x ^ 2 *
                ∑ i ∈ (((Finset.range (p + 1)).erase 0).erase 1).erase p, (u * x) ^ (i - 2) * ↑(p.choose i / p) +
              b * x ^ p)))
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc a b) volume
t₁ t₂ : ℝ
n : ℕ
h✝ : t₁ ≤ t₂
h₁ : ↑n ≤ t₁
h₂ : t₂ ≤ ↑n + 1
h₃ : a ≤ t₁
h₄ : t₂ ≤ b
h_inc₁ : Ι t₁ t₂ ⊆ Set.Icc (↑n) (↑n + 1)
h_inc₂ : [[t₁, t₂]] ⊆ Set.Icc a b
t : ℝ
h : t ∈ Set.Icc (↑n) (↑n + 1) → ∑ k ∈ Icc 0 ⌊t⌋₊, c k = ∑ k ∈ Icc 0 n, c k
h' : t ∈ Ι t₁ t₂
⊢ deriv f t * ∑ k ∈ Icc 0 n, c k = deriv f t * ∑ k ∈ Icc 0 n, c k

Tactic:
]

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

Goal state before:
pp: case neg.refine_2
n : ℕ
hn : n ≠ 2
hn' : ¬n ≤ 2
five : (ZMod (2 ^ n))ˣ := ZMod.unitOfCoprime 5 ⋯
⊢ orderOf five ∣ exponent (ZMod (2 ^ n))ˣ

Tactic:
]

Goal state after:
case neg.refine_2
n : ℕ
hn : n ≠ 2
hn' : ¬n ≤ 2
five : (ZMod (2 ^ n))ˣ := ZMod.unitOfCoprime 5 ⋯
⊢ orderOf five ∣ exponent (ZMod (2 ^ n))ˣ
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.Carmichael

Goal state before:
pp: p n : ℕ
hp : Nat.Prime p
hp₂ : p ≠ 2
this : NeZero p
⊢ exponent (ZMod (p ^ n))ˣ = Nat.card (ZMod (p ^ n))ˣ

Tactic:
]

Goal state after:
p n : ℕ
hp : Nat.Prime p
hp₂ : p ≠ 2
this : NeZero p
⊢ exponent (ZMod (p ^ n))ˣ = Nat.card (ZMod (p ^ n))ˣ
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case h.e_a.e_a
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
⊢ (u * x) ^ 1 * ↑p = ↑p * u * x

Tactic:
]

Goal state after:
case h.e_a.e_a
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
⊢ (u * x) ^ 1 * ↑p = ↑p * u * x
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc a b) volume
t₁ t₂ : ℝ
n : ℕ
h : t₁ ≤ t₂
h₁ : ↑n ≤ t₁
h₂ : t₂ ≤ ↑n + 1
h₃ : a ≤ t₁
h₄ : t₂ ≤ b
h_inc₁ : Ι t₁ t₂ ⊆ Set.Icc (↑n) (↑n + 1)
h_inc₂ : [[t₁, t₂]] ⊆ Set.Icc a b
⊢ [[t₁, t₂]] ⊆ Set.Icc a b

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (deriv f) (Set.Icc a b) volume
t₁ t₂ : ℝ
n : ℕ
h : t₁ ≤ t₂
h₁ : ↑n ≤ t₁
h₂ : t₂ ≤ ↑n + 1
h₃ : a ≤ t₁
h₄ : t₂ ≤ b
h_inc₁ : Ι t₁ t₂ ⊆ Set.Icc (↑n) (↑n + 1)
h_inc₂ : [[t₁, t₂]] ⊆ Set.Icc a b
⊢ [[t₁, t₂]] ⊆ Set.Icc a b
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: case right
a b : ℝ
k : ℕ
hk : k ∈ Set.Ico (⌊a⌋₊ + 1) ⌊b⌋₊
⊢ k.succ ≤ ⌊b⌋₊

Tactic:
]

Goal state after:
case right
a b : ℝ
k : ℕ
hk : k ∈ Set.Ico (⌊a⌋₊ + 1) ⌊b⌋₊
⊢ k.succ ≤ ⌊b⌋₊
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) ^ i * ↑(p.choose i) = (u * x) ^ i * ↑(p.choose i)

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: a b : ℝ
k : ℕ
hk : k ∈ Ico (⌊a⌋₊ + 1) ⌊b⌋₊
⊢ k ∈ ↑(Ico (⌊a⌋₊ + 1) ⌊b⌋₊)

Tactic:
]

Goal state after:
a b : ℝ
k : ℕ
hk : k ∈ Ico (⌊a⌋₊ + 1) ⌊b⌋₊
⊢ k ∈ ↑(Ico (⌊a⌋₊ + 1) ⌊b⌋₊)
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 ^ 2 * x ^ 2 * (u * x) ^ (i - 2) * ↑(p.choose i) = u ^ 2 * x ^ 2 * (u * x) ^ (i - 2) * ↑(p.choose i)

Tactic:
]

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

Goal state before:
pp: m n : ℕ
⊢ liouville (m * n) = liouville m * liouville n

Tactic:
by
  by_cases hm : m = 0
  · simp [hm]
  by_cases hn : n = 0
  · simp [hn]
  simp [liouville_apply, cardFactors_mul, hm, hn, pow_add]

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
i : ℕ
hi : ¬i = p ∧ ¬i = 1 ∧ ¬i = 0 ∧ i < p + 1
hi' : 2 ≤ i
⊢ (v * a) ^ 2 * x ^ 2 * (v * a * x) ^ (i - 2) * ↑p * ↑(p.choose i / p) =
    ↑p * (v * a) * (v * (a * x ^ 2 * ((v * a * x) ^ (i - 2) * ↑(p.choose i / p))))

Tactic:
]

Goal state after:
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
⊢ (v * a) ^ 2 * x ^ 2 * (v * a * x) ^ (i - 2) * ↑p * ↑(p.choose i / p) =
    ↑p * (v * a) * (v * (a * x ^ 2 * ((v * a * x) ^ (i - 2) * ↑(p.choose i / p))))
Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt

Goal state before:
pp: n : ℕ
⊢ 0 ≤ if IsPrimePow n then Real.log ↑n.minFac else 0

Tactic:
]

Goal state after:
n : ℕ
⊢ 0 ≤ if IsPrimePow n then Real.log ↑n.minFac else 0
Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt

Goal state before:
pp: p : ℕ
hp : Nat.Prime p
⊢ Real.log ↑p = Real.log ↑p

Tactic:
]

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:
]

Goal state after:
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn g (Set.Icc a b) volume
hab : a ≤ b
hb : ⌊a⌋₊ = ⌊b⌋₊
t : ℝ
ht₁ : t ∈ Set.Icc (↑⌊a⌋₊) (↑⌊a⌋₊ + 1) → ∑ k ∈ Icc m ⌊t⌋₊, c k = ∑ k ∈ Icc m ⌊a⌋₊, c k
ht₂ : t ∈ Set.Icc a b
⊢ ∑ k ∈ Icc m ⌊a⌋₊, c k = ∑ k ∈ Icc m ⌊a⌋₊, c k

Tactic:
]

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

Goal state before:
pp: case refine_2
n p k : ℕ
hp : Nat.Prime p
⊢ ∑ k ∈ range k, Λ (p ^ (k + 1)) + 0 = ↑k * Real.log ↑p

Tactic:
]

Goal state after:
case refine_2
n p k : ℕ
hp : Nat.Prime p
⊢ ∑ k ∈ range k, Λ (p ^ (k + 1)) + 0 = ↑k * Real.log ↑p
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : ℕ
u v : R
hp : Nat.Prime p
hvu : v ∣ u
hpuv : ↑p * u * v ∣ u ^ p
x : R
m✝ m : ℕ
⊢ ∃ y, ((1 + u * x) ^ p) ^ p ^ m = 1 + ↑p ^ (m + 1) * u * (x + v * y)

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
u v : R
hp : Nat.Prime p
hvu : v ∣ u
hpuv : ↑p * u * v ∣ u ^ p
x : R
m✝ m : ℕ
⊢ ∃ y, ((1 + u * x) ^ p) ^ p ^ m = 1 + ↑p ^ (m + 1) * u * (x + v * y)
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : ℕ
u v : R
hp : Nat.Prime p
hvu : v ∣ u
hpuv : ↑p * u * v ∣ u ^ p
x : R
m✝ m : ℕ
y : R
hy : (1 + u * x) ^ p = 1 + ↑p * u * (x + v * y)
⊢ ∃ y_1, (1 + ↑p * u * (x + v * y)) ^ p ^ m = 1 + ↑p ^ (m + 1) * u * (x + v * y_1)

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
u v : R
hp : Nat.Prime p
hvu : v ∣ u
hpuv : ↑p * u * v ∣ u ^ p
x : R
m✝ m : ℕ
y : R
hy : (1 + u * x) ^ p = 1 + ↑p * u * (x + v * y)
⊢ ∃ y_1, (1 + ↑p * u * (x + v * y)) ^ p ^ m = 1 + ↑p ^ (m + 1) * u * (x + v * y_1)
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : ℕ
u v : R
hp : Nat.Prime p
hvu : v ∣ u
hpuv : ↑p * u * v ∣ u ^ p
x : R
m✝ m : ℕ
y : R
hy : (1 + u * x) ^ p = 1 + ↑p * u * (x + v * y)
⊢ ↑p * (↑p * u) * (↑p * v) ∣ ↑p ^ p * u ^ p

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
u v : R
hp : Nat.Prime p
hvu : v ∣ u
hpuv : ↑p * u * v ∣ u ^ p
x : R
m✝ m : ℕ
y : R
hy : (1 + u * x) ^ p = 1 + ↑p * u * (x + v * y)
⊢ ↑p * (↑p * u) * (↑p * v) ∣ ↑p ^ p * u ^ p
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : ℕ
u v : R
hp : Nat.Prime p
hvu : v ∣ u
hpuv : ↑p * u * v ∣ u ^ p
x : R
m✝ m : ℕ
y : R
hy : (1 + u * x) ^ p = 1 + ↑p * u * (x + v * y)
⊢ ↑p * ↑p * (↑p * u * v) ∣ ↑p ^ p * u ^ p

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
u v : R
hp : Nat.Prime p
hvu : v ∣ u
hpuv : ↑p * u * v ∣ u ^ p
x : R
m✝ m : ℕ
y : R
hy : (1 + u * x) ^ p = 1 + ↑p * u * (x + v * y)
⊢ ↑p * ↑p * (↑p * u * v) ∣ ↑p ^ p * u ^ p
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: case inl.inl
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn g (Set.Icc a b) volume
hab : a ≤ b
hb : ⌊a⌋₊ = ⌊b⌋₊
this : ∀ᵐ (x : ℝ) ∂volume.restrict (Set.Icc a b), ∑ k ∈ Icc m ⌊a⌋₊, c k = ∑ k ∈ Icc m ⌊x⌋₊, c k
⊢ IntegrableOn (fun t ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) (Set.Icc a b) volume

Tactic:
]

Goal state after:
case inl.inl
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn g (Set.Icc a b) volume
hab : a ≤ b
hb : ⌊a⌋₊ = ⌊b⌋₊
this : ∀ᵐ (x : ℝ) ∂volume.restrict (Set.Icc a b), ∑ k ∈ Icc m ⌊a⌋₊, c k = ∑ k ∈ Icc m ⌊x⌋₊, c k
⊢ IntegrableOn (fun t ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) (Set.Icc a b) volume
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : ℕ
u v : R
hp : Nat.Prime p
hvu : v ∣ u
hpuv : ↑p * u * v ∣ u ^ p
x : R
m✝ m : ℕ
y : R
hy : (1 + u * x) ^ p = 1 + ↑p * u * (x + v * y)
⊢ ↑p ^ 2 ∣ ↑p ^ p

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
u v : R
hp : Nat.Prime p
hvu : v ∣ u
hpuv : ↑p * u * v ∣ u ^ p
x : R
m✝ m : ℕ
y : R
hy : (1 + u * x) ^ p = 1 + ↑p * u * (x + v * y)
⊢ ↑p ^ 2 ∣ ↑p ^ p
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case h
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
u v : R
hp : Nat.Prime p
hvu : v ∣ u
hpuv : ↑p * u * v ∣ u ^ p
x : R
m✝ m : ℕ
y : R
hy : (1 + u * x) ^ p = 1 + ↑p * u * (x + v * y)
z : R
hz : (1 + ↑p * u * (x + v * y)) ^ p ^ m = 1 + ↑p ^ m * (↑p * u) * (x + v * y + ↑p * v * z)
⊢ 1 + ↑p ^ m * (↑p * u) * (x + v * y + ↑p * v * z) = 1 + ↑p ^ (m + 1) * u * (x + v * (y + ↑p * z))

Tactic:
]

Goal state after:
case h
R : Type u_1
inst✝ : CommSemiring R
p : ℕ
u v : R
hp : Nat.Prime p
hvu : v ∣ u
hpuv : ↑p * u * v ∣ u ^ p
x : R
m✝ m : ℕ
y : R
hy : (1 + u * x) ^ p = 1 + ↑p * u * (x + v * y)
z : R
hz : (1 + ↑p * u * (x + v * y)) ^ p ^ m = 1 + ↑p ^ m * (↑p * u) * (x + v * y + ↑p * v * z)
⊢ 1 + ↑p ^ m * (↑p * u) * (x + v * y + ↑p * v * z) = 1 + ↑p ^ (m + 1) * u * (x + v * (y + ↑p * z))
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn g (Set.Icc a b) volume
hab : a ≤ b
hb : ⌊a⌋₊ < ⌊b⌋₊
t₁ t₂ : ℝ
n : ℕ
h : t₁ ≤ t₂
h₁ : ↑n ≤ t₁
h₂ : t₂ ≤ ↑n + 1
h₃ : a ≤ t₁
h₄ : t₂ ≤ b
⊢ IntegrableOn (fun t ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) (Set.Icc t₁ t₂) volume

Tactic:
]

Goal state after:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn g (Set.Icc a b) volume
hab : a ≤ b
hb : ⌊a⌋₊ < ⌊b⌋₊
t₁ t₂ : ℝ
n : ℕ
h : t₁ ≤ t₂
h₁ : ↑n ≤ t₁
h₂ : t₂ ≤ ↑n + 1
h₃ : a ≤ t₁
h₄ : t₂ ≤ b
⊢ IntegrableOn (fun t ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) (Set.Icc t₁ t₂) volume
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
⊢ Real.log ↑a + Real.log ↑b = Real.log ↑a + Real.log ↑b

Tactic:
]

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

Goal state before:
pp: n : ℕ
⊢ Real.log ↑n = log n

Tactic:
]

Goal state after:
n : ℕ
⊢ Real.log ↑n = log n
Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt

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

Tactic:
]

Goal state after:
⊢ Λ * ↑ζ = log
Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt

Goal state before:
pp: ⊢ Λ = Λ

Tactic:
]

Goal state after: