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

Goal state before:
pp: case refine_1
n : ℕ
⊢ ∑ i ∈ divisors 0, Λ i = Real.log ↑0

pp: case refine_2
n : ℕ
⊢ ∀ (p n : ℕ), Nat.Prime p → ∑ i ∈ (p ^ n).divisors, Λ i = Real.log ↑(p ^ n)

pp: case refine_3
n : ℕ
⊢ ∀ (a b : ℕ),
    1 < a →
      1 < b →
        a.Coprime b →
          ∑ i ∈ a.divisors, Λ i = Real.log ↑a →
            ∑ i ∈ b.divisors, Λ i = Real.log ↑b → ∑ i ∈ (a * b).divisors, Λ i = Real.log ↑(a * b)

Tactic:
·

Goal state after:
case refine_1
n : ℕ
⊢ ∑ i ∈ divisors 0, Λ i = Real.log ↑0
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

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

Tactic:
·

Goal state after:
case h.e_a.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) ^ p * ↑(p.choose p) = ↑p * u * (v * (b * x ^ p))
Module: Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt

Goal state before:
pp: case refine_2
n : ℕ
⊢ ∀ (p n : ℕ), Nat.Prime p → ∑ i ∈ (p ^ n).divisors, Λ i = Real.log ↑(p ^ n)

pp: case refine_3
n : ℕ
⊢ ∀ (a b : ℕ),
    1 < a →
      1 < b →
        a.Coprime b →
          ∑ i ∈ a.divisors, Λ i = Real.log ↑a →
            ∑ i ∈ b.divisors, Λ i = Real.log ↑b → ∑ i ∈ (a * b).divisors, Λ i = Real.log ↑(a * b)

Tactic:
·

Goal state after:
case refine_2
n : ℕ
⊢ ∀ (p n : ℕ), Nat.Prime p → ∑ i ∈ (p ^ n).divisors, Λ i = Real.log ↑(p ^ n)
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: case inl.inr
𝕜 : 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⌋₊
⊢ IntegrableOn (fun t ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) (Set.Icc a b) volume

Tactic:
·

Goal state after:
case inl.inr
𝕜 : 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⌋₊
⊢ 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: case refine_2
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)
⊢ orderOf (1 + ↑p ^ m * ↑a) = p ^ (n + 1)

pp: case refine_1
p : ℕ
hp : Nat.Prime p
m : ℕ
hm0 : m ≠ 0
hpm : m + 2 ≤ p * m
a : ℤ
ha : ¬↑p ∣ a
n✝ n : ℕ
this : Fact (Nat.Prime p)
⊢ ↑p * ↑p ^ m * ↑p ∣ (↑p ^ m) ^ p

Tactic:
·

Goal state after:
case refine_2
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)
⊢ orderOf (1 + ↑p ^ m * ↑a) = p ^ (n + 1)
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

pp: case hfin
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) = 1

Tactic:
·

Goal state after:
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
Module: Mathlib.NumberTheory.AbelSummation

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

Tactic:
·

Goal state after:
case inr
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn g (Set.Icc a b) volume
hab : b < a
⊢ 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: case hfin
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) = 1

Tactic:
·

Goal state after:
case hfin
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) = 1
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: case inl
𝕜 : 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⌋₊
⊢ ∑ k ∈ Ioc ⌊a⌋₊ ⌊b⌋₊, f ↑k * c k =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f a * ∑ k ∈ Icc 0 ⌊a⌋₊, c k - ∫ (x : ℝ) in a..b, deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k

pp: case inr
𝕜 : 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⌋₊
⊢ ∑ k ∈ Ioc ⌊a⌋₊ ⌊b⌋₊, f ↑k * c k =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f a * ∑ k ∈ Icc 0 ⌊a⌋₊, c k - ∫ (x : ℝ) in a..b, deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k

Tactic:
·

Goal state after:
case inl
𝕜 : 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⌋₊
⊢ ∑ k ∈ Ioc ⌊a⌋₊ ⌊b⌋₊, f ↑k * c k =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f a * ∑ k ∈ Icc 0 ⌊a⌋₊, c k - ∫ (x : ℝ) in a..b, deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case refine_1
p : ℕ
hp : Nat.Prime p
m : ℕ
hm0 : m ≠ 0
hpm : m + 2 ≤ p * m
a : ℤ
ha : ¬↑p ∣ a
n✝ n : ℕ
this : Fact (Nat.Prime p)
⊢ ↑p * ↑p ^ m * ↑p ∣ (↑p ^ m) ^ p

Tactic:
·

Goal state after:
case refine_1
p : ℕ
hp : Nat.Prime p
m : ℕ
hm0 : m ≠ 0
hpm : m + 2 ≤ p * m
a : ℤ
ha : ¬↑p ∣ a
n✝ n : ℕ
this : Fact (Nat.Prime p)
⊢ ↑p * ↑p ^ m * ↑p ∣ (↑p ^ m) ^ p
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
a : ℤ
ha : ¬↑p ∣ a
n : ℕ
⊢ orderOf (1 + ↑p * ↑a) = orderOf (1 + ↑p ^ 1 * ↑a)

pp: p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
a : ℤ
ha : ¬↑p ∣ a
n : ℕ
⊢ 1 + 2 ≤ p * 1

Tactic:
·

Goal state after:
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
a : ℤ
ha : ¬↑p ∣ a
n : ℕ
⊢ orderOf (1 + ↑p * ↑a) = orderOf (1 + ↑p ^ 1 * ↑a)
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
a : ℤ
ha : ¬↑p ∣ a
n : ℕ
⊢ 1 + 2 ≤ p * 1

Tactic:
·

Goal state after:
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
a : ℤ
ha : ¬↑p ∣ a
n : ℕ
⊢ 1 + 2 ≤ p * 1
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
n : ℕ
⊢ ↑p = ↑p * ↑1

pp: p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
n : ℕ
⊢ ¬↑p ∣ 1

Tactic:
·

Goal state after:
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
n : ℕ
⊢ ↑p = ↑p * ↑1
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
n : ℕ
⊢ ¬↑p ∣ 1

Tactic:
·

Goal state after:
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
n : ℕ
⊢ ¬↑p ∣ 1
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case zero
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
this : Fact (Nat.Prime p)
⊢ IsCyclic (ZMod (p ^ 0))ˣ

pp: case succ
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
this : Fact (Nat.Prime p)
n : ℕ
⊢ IsCyclic (ZMod (p ^ (n + 1)))ˣ

Tactic:
·

Goal state after:
case zero
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
this : Fact (Nat.Prime p)
⊢ IsCyclic (ZMod (p ^ 0))ˣ
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case succ
p : ℕ
hp : Nat.Prime p
hp2 : p ≠ 2
this : Fact (Nat.Prime p)
n : ℕ
⊢ IsCyclic (ZMod (p ^ (n + 1)))ˣ

Tactic:
set a := (1 + p : ZMod (p ^ (n + 1))) with ha_def

Goal state after:
case succ
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
⊢ IsCyclic (ZMod (p ^ (n + 1)))ˣ
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case succ
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
⊢ IsCyclic (ZMod (p ^ (n + 1)))ˣ

Tactic:
have : p - 1 ∣ orderOf b := hc ▸ orderOf_map_dvd _ b

Goal state after:
case succ
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
⊢ IsCyclic (ZMod (p ^ (n + 1)))ˣ
Module: Mathlib.NumberTheory.AbelSummation

Goal state before:
pp: 𝕜 : 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⌋₊
⊢ 1 ≤ ⌊b⌋₊

Tactic:
by lia

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Derivative

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
i : σ
f : MvPowerSeries σ R
n m✝ : σ →₀ ℕ
h : m✝ < n
⊢ (coeff m✝) (pderivFun i f) = MvPolynomial.coeff m✝ ((pderiv i) ((trunc R (n + single i 1)) f))

pp: case neg
σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
i : σ
f : MvPowerSeries σ R
n m✝ : σ →₀ ℕ
h : ¬m✝ < n
⊢ 0 = MvPolynomial.coeff m✝ ((pderiv i) ((trunc R (n + single i 1)) f))

Tactic:
·

Goal state after:
case pos
σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
i : σ
f : MvPowerSeries σ R
n m✝ : σ →₀ ℕ
h : m✝ < n
⊢ (coeff m✝) (pderivFun i f) = MvPolynomial.coeff m✝ ((pderiv i) ((trunc R (n + single i 1)) f))
Module: Mathlib.RingTheory.MvPowerSeries.Derivative

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
i : σ
f : MvPowerSeries σ R
n m✝ : σ →₀ ℕ
h : ¬m✝ < n
⊢ 0 = MvPolynomial.coeff m✝ ((pderiv i) ((trunc R (n + single i 1)) f))

Tactic:
·

Goal state after:
case neg
σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
i : σ
f : MvPowerSeries σ R
n m✝ : σ →₀ ℕ
h : ¬m✝ < n
⊢ 0 = MvPolynomial.coeff m✝ ((pderiv i) ((trunc R (n + single i 1)) f))
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: n✝ n : ℕ
H : IsCyclic (ZMod (2 ^ (n + 3)))ˣ
⊢ 3 ≤ n + 3

Tactic:
by lia

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

Goal state before:
pp: a : ℤ
ha : Odd a
n : ℕ
⊢ orderOf (1 + 4 * ↑a) = orderOf (1 + ↑2 ^ 2 * ↑a)

pp: a : ℤ
ha : Odd a
n : ℕ
⊢ ¬↑2 ∣ a

Tactic:
·

Goal state after:
a : ℤ
ha : Odd a
n : ℕ
⊢ orderOf (1 + 4 * ↑a) = orderOf (1 + ↑2 ^ 2 * ↑a)
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: a : ℤ
ha : Odd a
n : ℕ
⊢ ¬↑2 ∣ a

Tactic:
·

Goal state after:
a : ℤ
ha : Odd a
n : ℕ
⊢ ¬↑2 ∣ a
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case inl
⊢ IsCyclic (ZMod (4 * 0))ˣ ↔ 0 = 0 ∨ 0 = 1

pp: case inr
n : ℕ
hn0 : n ≠ 0
⊢ IsCyclic (ZMod (4 * n))ˣ ↔ n = 0 ∨ n = 1

Tactic:
·

Goal state after:
case inl
⊢ IsCyclic (ZMod (4 * 0))ˣ ↔ 0 = 0 ∨ 0 = 1
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case inr.inl
hn0 : 1 ≠ 0
⊢ IsCyclic (ZMod (4 * 1))ˣ ↔ 1 = 0 ∨ 1 = 1

pp: case inr.inr
n : ℕ
hn0 : n ≠ 0
hn1 : n ≠ 1
⊢ IsCyclic (ZMod (4 * n))ˣ ↔ n = 0 ∨ n = 1

Tactic:
·

Goal state after:
case inr.inl
hn0 : 1 ≠ 0
⊢ IsCyclic (ZMod (4 * 1))ˣ ↔ 1 = 0 ∨ 1 = 1
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:
·

Goal state after:
case inr.inr.inl
n : ℕ
hn0 : 2 * n ≠ 0
hn1 : 2 * n ≠ 1
⊢ ¬IsCyclic (ZMod (4 * (2 * 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))ˣ

Tactic:
have : NeZero n := ⟨by simpa using hn0⟩

Goal state after:
case inr.inr.inl
n : ℕ
hn0 : 2 * n ≠ 0
hn1 : 2 * n ≠ 1
this : NeZero n
⊢ ¬IsCyclic (ZMod (4 * 2 * 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)))ˣ

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:
Module: Mathlib.RingTheory.MvPowerSeries.Derivative

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
⊢ (pderiv R i) (X i) = 1

Tactic:
classical
  ext n
  simp only [coeff_pderiv, coeff_X, boole_mul, add_eq_right, coeff_one]
  split_ifs <;> simp_all

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.Derivative

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
i j : σ
h : i = j
⊢ (pderiv R i) (X j) = Pi.single i 1 j

pp: case neg
σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
i j : σ
h : ¬i = j
⊢ (pderiv R i) (X j) = Pi.single i 1 j

Tactic:
·

Goal state after:
case pos
σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
i j : σ
h : i = j
⊢ (pderiv R i) (X j) = Pi.single i 1 j
Module: Mathlib.RingTheory.MvPowerSeries.Derivative

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
i j : σ
h : ¬i = j
⊢ (pderiv R i) (X j) = Pi.single i 1 j

Tactic:
·

Goal state after:
case neg
σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
i j : σ
h : ¬i = j
⊢ (pderiv R i) (X j) = Pi.single i 1 j
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
⊢ (coeff n) f = (coeff n) g

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
⊢ (coeff n) f = (coeff n) g

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
⊢ (coeff n) f = (coeff n) g
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case inl
n : ℕ
hn : Odd n
hn1 : n ≠ 1
x✝¹ : NeZero n
hm : Odd 2
hm1 : 2 ≠ 1
hmn : Nat.Coprime 2 n
x✝ : NeZero 2
e : (ZMod (2 * n))ˣ ≃* (ZMod 2)ˣ × (ZMod n)ˣ :=
  (Units.mapEquiv (chineseRemainder hmn).toMulEquiv).trans MulEquiv.prodUnits
⊢ False

pp: case inr
m : ℕ
hm : Odd m
hm1 : m ≠ 1
x✝¹ : NeZero m
hn : Odd 2
hn1 : 2 ≠ 1
hmn : m.Coprime 2
x✝ : NeZero 2
e : (ZMod (m * 2))ˣ ≃* (ZMod m)ˣ × (ZMod 2)ˣ :=
  (Units.mapEquiv (chineseRemainder hmn).toMulEquiv).trans MulEquiv.prodUnits
⊢ False

Tactic:
·

Goal state after:
case inl
n : ℕ
hn : Odd n
hn1 : n ≠ 1
x✝¹ : NeZero n
hm : Odd 2
hm1 : 2 ≠ 1
hmn : Nat.Coprime 2 n
x✝ : NeZero 2
e : (ZMod (2 * n))ˣ ≃* (ZMod 2)ˣ × (ZMod n)ˣ :=
  (Units.mapEquiv (chineseRemainder hmn).toMulEquiv).trans MulEquiv.prodUnits
⊢ False
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case inr
m : ℕ
hm : Odd m
hm1 : m ≠ 1
x✝¹ : NeZero m
hn : Odd 2
hn1 : 2 ≠ 1
hmn : m.Coprime 2
x✝ : NeZero 2
e : (ZMod (m * 2))ˣ ≃* (ZMod m)ˣ × (ZMod 2)ˣ :=
  (Units.mapEquiv (chineseRemainder hmn).toMulEquiv).trans MulEquiv.prodUnits
⊢ False

Tactic:
·

Goal state after:
case inr
m : ℕ
hm : Odd m
hm1 : m ≠ 1
x✝¹ : NeZero m
hn : Odd 2
hn1 : 2 ≠ 1
hmn : m.Coprime 2
x✝ : NeZero 2
e : (ZMod (m * 2))ˣ ≃* (ZMod m)ˣ × (ZMod 2)ˣ :=
  (Units.mapEquiv (chineseRemainder hmn).toMulEquiv).trans MulEquiv.prodUnits
⊢ False
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:
·

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

Goal state before:
pp: case pos
n : ℕ
hn : Odd n
hn0 : n ≠ 0
h1 : n ≠ 1
p : ℕ
hp : Nat.Prime p
dvd : p ∣ n
odd : Odd p
hnp : n = p ^ n.factorization p
⊢ IsCyclic (ZMod n)ˣ ↔ ∃ p m, Nat.Prime p ∧ Odd p ∧ n = p ^ m

pp: case neg
n : ℕ
hn : Odd n
hn0 : n ≠ 0
h1 : n ≠ 1
p : ℕ
hp : Nat.Prime p
dvd : p ∣ n
odd : Odd p
hnp : ¬n = p ^ n.factorization p
⊢ IsCyclic (ZMod n)ˣ ↔ ∃ p m, Nat.Prime p ∧ Odd p ∧ n = p ^ m

Tactic:
·

Goal state after:
case pos
n : ℕ
hn : Odd n
hn0 : n ≠ 0
h1 : n ≠ 1
p : ℕ
hp : Nat.Prime p
dvd : p ∣ n
odd : Odd p
hnp : n = p ^ n.factorization p
⊢ IsCyclic (ZMod n)ˣ ↔ ∃ p m, Nat.Prime p ∧ Odd p ∧ n = p ^ m
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case neg.refine_1
n : ℕ
hn : Odd n
hn0 : n ≠ 0
h1 : n ≠ 1
p : ℕ
hp : Nat.Prime p
dvd : p ∣ n
odd : Odd p
hnp : ¬n = p ^ n.factorization p
⊢ ¬IsCyclic (ZMod n)ˣ

pp: case neg.refine_2
n : ℕ
hn : Odd n
hn0 : n ≠ 0
h1 : n ≠ 1
p : ℕ
hp : Nat.Prime p
dvd : p ∣ n
odd : Odd p
hnp : ¬n = p ^ n.factorization p
⊢ (∃ p m, Nat.Prime p ∧ Odd p ∧ n = p ^ m) → n = p ^ n.factorization p

Tactic:
·

Goal state after:
case neg.refine_1
n : ℕ
hn : Odd n
hn0 : n ≠ 0
h1 : n ≠ 1
p : ℕ
hp : Nat.Prime p
dvd : p ∣ n
odd : Odd p
hnp : ¬n = p ^ n.factorization p
⊢ ¬IsCyclic (ZMod n)ˣ
Module: Mathlib.RingTheory.MvPowerSeries.Derivative

Goal state before:
pp: case pos
σ : Type u_1
R : Type u_2
i : σ
inst✝ : Field R
f : MvPowerSeries σ R
h : constantCoeff f = 0
⊢ (pderiv R i) f⁻¹ = -f⁻¹ ^ 2 * (pderiv R i) f

pp: case neg
σ : Type u_1
R : Type u_2
i : σ
inst✝ : Field R
f : MvPowerSeries σ R
h : ¬constantCoeff f = 0
⊢ (pderiv R i) f⁻¹ = -f⁻¹ ^ 2 * (pderiv R i) f

Tactic:
·

Goal state after:
case pos
σ : Type u_1
R : Type u_2
i : σ
inst✝ : Field R
f : MvPowerSeries σ R
h : constantCoeff f = 0
⊢ (pderiv R i) f⁻¹ = -f⁻¹ ^ 2 * (pderiv R i) f
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case neg.refine_1.refine_1
n : ℕ
hn : Odd n
hn0 : n ≠ 0
h1 : n ≠ 1
p : ℕ
hp : Nat.Prime p
dvd : p ∣ n
odd : Odd p
hnp : ¬n = p ^ n.factorization p
this : p ^ n.factorization p ∣ n
⊢ p ^ n.factorization p ≠ 1

pp: case neg.refine_1.refine_2
n : ℕ
hn : Odd n
hn0 : n ≠ 0
h1 : n ≠ 1
p : ℕ
hp : Nat.Prime p
dvd : p ∣ n
odd : Odd p
hnp : ¬n = p ^ n.factorization p
this : p ^ n.factorization p ∣ n
⊢ n / p ^ n.factorization p ≠ 1

Tactic:
·

Goal state after:
case neg.refine_1.refine_1
n : ℕ
hn : Odd n
hn0 : n ≠ 0
h1 : n ≠ 1
p : ℕ
hp : Nat.Prime p
dvd : p ∣ n
odd : Odd p
hnp : ¬n = p ^ n.factorization p
this : p ^ n.factorization p ∣ n
⊢ p ^ n.factorization p ≠ 1
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case neg.refine_1.refine_2
n : ℕ
hn : Odd n
hn0 : n ≠ 0
h1 : n ≠ 1
p : ℕ
hp : Nat.Prime p
dvd : p ∣ n
odd : Odd p
hnp : ¬n = p ^ n.factorization p
this : p ^ n.factorization p ∣ n
⊢ n / p ^ n.factorization p ≠ 1

Tactic:
·

Goal state after:
case neg.refine_1.refine_2
n : ℕ
hn : Odd n
hn0 : n ≠ 0
h1 : n ≠ 1
p : ℕ
hp : Nat.Prime p
dvd : p ∣ n
odd : Odd p
hnp : ¬n = p ^ n.factorization p
this : p ^ n.factorization p ∣ n
⊢ n / p ^ n.factorization p ≠ 1
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case pos
n : ℕ
h0 : n = 0
⊢ IsCyclic (ZMod n)ˣ ↔ n = 0 ∨ n = 1 ∨ n = 2 ∨ n = 4 ∨ ∃ p m, Nat.Prime p ∧ Odd p ∧ 1 ≤ m ∧ (n = p ^ m ∨ n = 2 * p ^ m)

pp: case neg
n : ℕ
h0 : ¬n = 0
⊢ IsCyclic (ZMod n)ˣ ↔ n = 0 ∨ n = 1 ∨ n = 2 ∨ n = 4 ∨ ∃ p m, Nat.Prime p ∧ Odd p ∧ 1 ≤ m ∧ (n = p ^ m ∨ n = 2 * p ^ m)

Tactic:
·

Goal state after:
case pos
n : ℕ
h0 : n = 0
⊢ IsCyclic (ZMod n)ˣ ↔ n = 0 ∨ n = 1 ∨ n = 2 ∨ n = 4 ∨ ∃ p m, Nat.Prime p ∧ Odd p ∧ 1 ≤ m ∧ (n = p ^ m ∨ n = 2 * p ^ m)
Module: Mathlib.RingTheory.PowerSeries.Derivative

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommSemiring R
f : R⟦X⟧
n d : ℕ
h : d < n
⊢ (coeff d) ((d⁄dX R) f) = (Polynomial.derivative ((trunc (n + 1)) f)).coeff d

pp: case neg
R : Type u_1
inst✝ : CommSemiring R
f : R⟦X⟧
n d : ℕ
h : ¬d < n
⊢ 0 = (Polynomial.derivative ((trunc (n + 1)) f)).coeff d

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝ : CommSemiring R
f : R⟦X⟧
n d : ℕ
h : d < n
⊢ (coeff d) ((d⁄dX R) f) = (Polynomial.derivative ((trunc (n + 1)) f)).coeff d
Module: Mathlib.RingTheory.PowerSeries.Derivative

Goal state before:
pp: case neg
R : Type u_1
inst✝ : CommSemiring R
f : R⟦X⟧
n d : ℕ
h : ¬d < n
⊢ 0 = (Polynomial.derivative ((trunc (n + 1)) f)).coeff d

Tactic:
·

Goal state after:
case neg
R : Type u_1
inst✝ : CommSemiring R
f : R⟦X⟧
n d : ℕ
h : ¬d < n
⊢ 0 = (Polynomial.derivative ((trunc (n + 1)) f)).coeff d
Module: Mathlib.RingTheory.PowerSeries.Derivative

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : R⟦X⟧
n d : ℕ
h : ¬d < n
⊢ ¬d + 1 < n + 1

Tactic:
rwa [succ_lt_succ_iff]

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

Goal state before:
pp: case pos
n : ℕ
h0 : ¬n = 0
h1 : n = 1
⊢ IsCyclic (ZMod n)ˣ ↔ n = 0 ∨ n = 1 ∨ n = 2 ∨ n = 4 ∨ ∃ p m, Nat.Prime p ∧ Odd p ∧ 1 ≤ m ∧ (n = p ^ m ∨ n = 2 * p ^ m)

pp: case neg
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
⊢ IsCyclic (ZMod n)ˣ ↔ n = 0 ∨ n = 1 ∨ n = 2 ∨ n = 4 ∨ ∃ p m, Nat.Prime p ∧ Odd p ∧ 1 ≤ m ∧ (n = p ^ m ∨ n = 2 * p ^ m)

Tactic:
·

Goal state after:
case pos
n : ℕ
h0 : ¬n = 0
h1 : n = 1
⊢ IsCyclic (ZMod n)ˣ ↔ n = 0 ∨ n = 1 ∨ n = 2 ∨ n = 4 ∨ ∃ p m, Nat.Prime p ∧ Odd p ∧ 1 ≤ m ∧ (n = p ^ m ∨ n = 2 * p ^ m)
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case pos
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : n = 2
⊢ IsCyclic (ZMod n)ˣ ↔ n = 0 ∨ n = 1 ∨ n = 2 ∨ n = 4 ∨ ∃ p m, Nat.Prime p ∧ Odd p ∧ 1 ≤ m ∧ (n = p ^ m ∨ n = 2 * p ^ m)

pp: case neg
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : ¬n = 2
⊢ IsCyclic (ZMod n)ˣ ↔ n = 0 ∨ n = 1 ∨ n = 2 ∨ n = 4 ∨ ∃ p m, Nat.Prime p ∧ Odd p ∧ 1 ≤ m ∧ (n = p ^ m ∨ n = 2 * p ^ m)

Tactic:
·

Goal state after:
case pos
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : n = 2
⊢ IsCyclic (ZMod n)ˣ ↔ n = 0 ∨ n = 1 ∨ n = 2 ∨ n = 4 ∨ ∃ p m, Nat.Prime p ∧ Odd p ∧ 1 ≤ m ∧ (n = p ^ m ∨ n = 2 * p ^ m)
Module: Mathlib.RingTheory.ZMod.UnitsCyclic

Goal state before:
pp: case pos
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : ¬n = 2
h4 : n = 4
⊢ IsCyclic (ZMod n)ˣ ↔ n = 0 ∨ n = 1 ∨ n = 2 ∨ n = 4 ∨ ∃ p m, Nat.Prime p ∧ Odd p ∧ 1 ≤ m ∧ (n = p ^ m ∨ n = 2 * p ^ m)

pp: case neg
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : ¬n = 2
h4 : ¬n = 4
⊢ IsCyclic (ZMod n)ˣ ↔ n = 0 ∨ n = 1 ∨ n = 2 ∨ n = 4 ∨ ∃ p m, Nat.Prime p ∧ Odd p ∧ 1 ≤ m ∧ (n = p ^ m ∨ n = 2 * p ^ m)

Tactic:
·

Goal state after:
case pos
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : ¬n = 2
h4 : n = 4
⊢ IsCyclic (ZMod n)ˣ ↔ n = 0 ∨ n = 1 ∨ n = 2 ∨ n = 4 ∨ ∃ p m, Nat.Prime p ∧ Odd p ∧ 1 ≤ m ∧ (n = p ^ m ∨ n = 2 * p ^ m)