mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case cons
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
α : Type u_3
f : α → MvPolynomial σ R
a : α
s : Finset α
haA : a ∉ s
h : m.toWithBotSyn (m.withBotDegree (∑ x ∈ s, f x)) ≤ s.sup fun x ↦ m.toWithBotSyn (m.withBotDegree (f x))
⊢ m.toWithBotSyn (m.withBotDegree (f a + ∑ x ∈ s, f x)) ≤
    max (m.toWithBotSyn (m.withBotDegree (f a))) (s.sup fun x ↦ m.toWithBotSyn (m.withBotDegree (f x)))

Tactic:
]

Goal state after:
case cons
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
α : Type u_3
f : α → MvPolynomial σ R
a : α
s : Finset α
haA : a ∉ s
h : m.toWithBotSyn (m.withBotDegree (∑ x ∈ s, f x)) ≤ s.sup fun x ↦ m.toWithBotSyn (m.withBotDegree (f x))
⊢ m.toWithBotSyn (m.withBotDegree (f a + ∑ x ∈ s, f x)) ≤
    max (m.toWithBotSyn (m.withBotDegree (f a))) (s.sup fun x ↦ m.toWithBotSyn (m.withBotDegree (f x)))
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ⊆ (normalizedFactors n).toFinset
y : Finset ℕ
hy : y ⊆ (normalizedFactors n).toFinset
h : x.val.prod = y.val.prod
z : ℕ
hz : z ∈ x.val
⊢ z ∈ (normalizedFactors ?m.423).toFinset

Tactic:
]

Goal state after:
n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ⊆ (normalizedFactors n).toFinset
y : Finset ℕ
hy : y ⊆ (normalizedFactors n).toFinset
h : x.val.prod = y.val.prod
z : ℕ
hz : z ∈ x.val
⊢ z ∈ (normalizedFactors ?m.423).toFinset
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : f.support ⊆ g.support
hg : ¬g = 0
⊢ m.toSyn (m.degree f) ≤ m.toSyn (m.degree g)

Tactic:
]

Goal state after:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : f.support ⊆ g.support
hg : ¬g = 0
⊢ m.toSyn (m.degree f) ≤ m.toSyn (m.degree g)
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ⊆ (normalizedFactors n).toFinset
y : Finset ℕ
hy : y ⊆ (normalizedFactors n).toFinset
h : x.val.prod = y.val.prod
z : ℕ
hz : z ∈ y.val
⊢ z ∈ (normalizedFactors ?m.439).toFinset

Tactic:
]

Goal state after:
n : ℕ
h0 : n ≠ 0
x : Finset ℕ
hx : x ⊆ (normalizedFactors n).toFinset
y : Finset ℕ
hy : y ⊆ (normalizedFactors n).toFinset
h : x.val.prod = y.val.prod
z : ℕ
hz : z ∈ y.val
⊢ z ∈ (normalizedFactors ?m.439).toFinset
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
this : ∀ (f g : MvPolynomial σ R), m.degree g - m.degree f = m.degree f ⊔ m.degree g - m.degree f
⊢ (monomial (m.degree g ⊔ m.degree f - m.degree f)) (m.leadingCoeff g) * f -
      (monomial (m.degree g ⊔ m.degree f - m.degree g)) (m.leadingCoeff f) * g =
    (monomial (m.degree g ⊔ m.degree f - m.degree f)) (m.leadingCoeff g) * f -
      (monomial (m.degree g ⊔ m.degree f - m.degree g)) (m.leadingCoeff f) * g

Tactic:
]

Goal state after:
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n : ℕ
h0 : n ≠ 0
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ → α
⊢ (Multiset.map (f ∘ fun x ↦ x.val.prod) (normalizedFactors n).toFinset.powerset.val).sum =
    (Multiset.map (fun i ↦ f i.val.prod) (normalizedFactors n).toFinset.powerset.val).sum

Tactic:
]

Goal state after:
n : ℕ
h0 : n ≠ 0
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ → α
⊢ (Multiset.map (f ∘ fun x ↦ x.val.prod) (normalizedFactors n).toFinset.powerset.val).sum =
    (Multiset.map (fun i ↦ f i.val.prod) (normalizedFactors n).toFinset.powerset.val).sum
Module: Mathlib.Algebra.MvPolynomial.SchwartzZippel

Goal state before:
pp: case inr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ≠ 0
S : Finset R
hs : S.Nonempty
⊢ (p.support.sup fun s ↦ ∑ i, ↑(s i) / ↑(#S)) = p.support.sup fun i ↦ ↑(i.sum fun x e ↦ e) / ↑(#S)

Tactic:
]

Goal state after:
case inr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ≠ 0
S : Finset R
hs : S.Nonempty
⊢ (p.support.sup fun s ↦ ∑ i, ↑(s i) / ↑(#S)) = p.support.sup fun i ↦ ↑(i.sum fun x e ↦ e) / ↑(#S)
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n : ℕ
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ x, s = x ^ 2}
hSne : S.Nonempty
s : ℕ := S.max' hSne
a : ℕ
hn : 0 < s * a
hsa : n = s * a
b : ℕ
hsb : s = b ^ 2
⊢ ∃ a b, 0 < a ∧ 0 < b ∧ b ^ 2 * a = n ∧ Squarefree a

Tactic:
]

Goal state after:
n : ℕ
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ x, s = x ^ 2}
hSne : S.Nonempty
s : ℕ := S.max' hSne
a : ℕ
hn : 0 < s * a
hsa : n = s * a
b : ℕ
hsb : s = b ^ 2
⊢ ∃ a b, 0 < a ∧ 0 < b ∧ b ^ 2 * a = n ∧ Squarefree a
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
h : m.degree f = 0
⊢ C (m.leadingCoeff f) = C (m.leadingCoeff f)

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
⊢ m.toSyn.symm ((-f).support.sup ⇑m.toSyn) = m.toSyn.symm (f.support.sup ⇑m.toSyn)

Tactic:
support_neg

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
⊢ m.toSyn.symm (f.support.sup ⇑m.toSyn) = m.toSyn.symm (f.support.sup ⇑m.toSyn)
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
⊢ m.toSyn.symm (f.support.sup ⇑m.toSyn) = m.toSyn.symm (f.support.sup ⇑m.toSyn)

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
⊢ m.toSyn (m.degree (f + -g)) ≤ max (m.toSyn (m.degree f)) (m.toSyn (m.degree g))

Tactic:
]

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
⊢ m.toSyn (m.degree (f + -g)) ≤ max (m.toSyn (m.degree f)) (m.toSyn (m.degree g))
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n : ℕ
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ x, s = x ^ 2}
hSne : S.Nonempty
s : ℕ := S.max' hSne
a b : ℕ
hn : 0 < b ^ 2 * a
hsa : n = b ^ 2 * a
hsb : s = b ^ 2
hlts : 0 < b ^ 2
hlta : 0 < a
⊢ ∃ a b, 0 < a ∧ 0 < b ∧ b ^ 2 * a = n ∧ Squarefree a

Tactic:
]

Goal state after:
n : ℕ
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ x, s = x ^ 2}
hSne : S.Nonempty
s : ℕ := S.max' hSne
a b : ℕ
hn : 0 < b ^ 2 * a
hsa : n = b ^ 2 * a
hsb : s = b ^ 2
hlts : 0 < b ^ 2
hlta : 0 < a
⊢ ∃ a b, 0 < a ∧ 0 < b ∧ b ^ 2 * a = n ∧ Squarefree a
Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : MulAction R M
f : ArithmeticFunction M
x : ℕ
⊢ ∑ x ∈ x.divisorsAntidiagonal, ↑ζ x.1 • f x.2 = ∑ i ∈ x.divisors, f i

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : MulAction R M
f : ArithmeticFunction M
x : ℕ
⊢ ∑ x ∈ x.divisorsAntidiagonal, ↑ζ x.1 • f x.2 = ∑ i ∈ x.divisors, f i
Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : MulAction R M
f : ArithmeticFunction M
i : ℕ × ℕ
hi : i ∈ (i.1 * i.2).divisorsAntidiagonal
h : i.1 * i.2 ≠ 0
⊢ f i.2 = f i.2

Tactic:
]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : MulAction R M
f : ArithmeticFunction M
x : ℕ
⊢ ∑ x_1 ∈ x.divisors, f (x / x_1, x_1).2 = ∑ i ∈ x.divisors, f i

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
⊢ max (m.toSyn (m.degree f)) (m.toSyn (m.degree g)) = max (m.toSyn (m.degree f)) (m.toSyn (m.degree g))

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
h : m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ m.degree (f + -g) = m.degree f

Tactic:
]

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
h : m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ m.degree (f + -g) = m.degree f
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n : ℕ
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ x, s = x ^ 2}
hSne : S.Nonempty
s : ℕ := S.max' hSne
a b : ℕ
hn : 0 < b ^ 2 * a
hsa : n = b ^ 2 * a
hsb : s = b ^ 2
hlts : 0 < b ^ 2
hlta : 0 < a
x y : ℕ
hy : a = x * x * y
⊢ x = 1

Tactic:
]

Goal state after:
n : ℕ
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ x, s = x ^ 2}
hSne : S.Nonempty
s : ℕ := S.max' hSne
a b : ℕ
hn : 0 < b ^ 2 * a
hsa : n = b ^ 2 * a
hsb : s = b ^ 2
hlts : 0 < b ^ 2
hlta : 0 < a
x y : ℕ
hy : a = x * x * y
⊢ x = 1
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
h : m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ m.leadingCoeff (f + -g) = m.leadingCoeff f

Tactic:
]

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
h : m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ m.leadingCoeff (f + -g) = m.leadingCoeff f
Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
n : ℕ
⊢ ∑ i ∈ n.divisors, f (n / i) * ↑(ζ i) = ∑ i ∈ n.divisors, f (n / i) * ↑(ζ i)

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x : ℕ
⊢ ∑ i ∈ x.divisors, f i = ∑ i ∈ x.divisors, f i

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
h : m.degree f ≠ 0
h' : m.degree (f - m.leadingTerm f) = m.degree f
hl : coeff (m.degree f) (f - m.leadingTerm f) ≠ 0
⊢ False

Tactic:
]

Goal state after:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
h : m.degree f ≠ 0
h' : m.degree (f - m.leadingTerm f) = m.degree f
hl : coeff (m.degree f) (f - m.leadingTerm f) ≠ 0
⊢ False
Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta

Goal state before:
pp: f : ArithmeticFunction ℕ
x : ℕ
⊢ ∑ i ∈ x.divisors, f i = ∑ i ∈ x.divisors, f i

Tactic:
]

Goal state after:
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case e'_4
n : ℕ
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ x, s = x ^ 2}
hSne : S.Nonempty
s : ℕ := S.max' hSne
a b : ℕ
hn : 0 < b ^ 2 * a
hsa : n = b ^ 2 * a
hsb : s = b ^ 2
hlts : 0 < b ^ 2
hlta : 0 < a
x y : ℕ
hy : a = x * x * y
hx : ¬x = 1
⊢ b ^ 2 * x ^ 2 = b ^ 2 * x ^ 2

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: f : ArithmeticFunction ℕ
⊢ f * ↑ζ = f * ↑ζ

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
⊢ ↑ζ = ↑ζ

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
k x : ℕ
kpos : 0 < k
⊢ f x ^ k = f x ^ k

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
k x : ℕ
⊢ f x * f x ^ k = (f.pmul (f.ppow k)) x

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
k x : ℕ
⊢ f x * f x ^ k = (f.pmul (f.ppow k)) x
Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
k : ℕ
kpos : 0 < k
x : ℕ
⊢ f x ^ k * f x = ((f.ppow k).pmul f) x

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
k : ℕ
kpos : 0 < k
x : ℕ
⊢ f x ^ k * f x = ((f.ppow k).pmul f) x
Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta

Goal state before:
pp: case succ
R : Type u_1
inst✝ : CommSemiring R
f : ArithmeticFunction R
hf : f.IsMultiplicative
k : ℕ
hi : (f.ppow k).IsMultiplicative
⊢ (f.pmul (f.ppow k)).IsMultiplicative

Tactic:
]

Goal state after:
case succ
R : Type u_1
inst✝ : CommSemiring R
f : ArithmeticFunction R
hf : f.IsMultiplicative
k : ℕ
hi : (f.ppow k).IsMultiplicative
⊢ (f.pmul (f.ppow k)).IsMultiplicative
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
x✝ : ℕ
⊢ ∑ x ∈ x✝.divisorsAntidiagonal, f ((Equiv.prodComm ℕ ℕ).toEmbedding x).1 * g ((Equiv.prodComm ℕ ℕ).toEmbedding x).2 =
    (g * f) x✝

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
x✝ : ℕ
⊢ ∑ x ∈ x✝.divisorsAntidiagonal, f ((Equiv.prodComm ℕ ℕ).toEmbedding x).1 * g ((Equiv.prodComm ℕ ℕ).toEmbedding x).2 =
    (g * f) x✝
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
⊢ coeff (m.degree f ⊔ m.degree g) ((monomial (m.degree f ⊔ m.degree g - m.degree f)) (m.leadingCoeff g) * f) -
      coeff (m.degree f ⊔ m.degree g) ((monomial (m.degree f ⊔ m.degree g - m.degree g)) (m.leadingCoeff f) * g) =
    0

Tactic:
]

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
⊢ coeff (m.degree f ⊔ m.degree g) ((monomial (m.degree f ⊔ m.degree g - m.degree f)) (m.leadingCoeff g) * f) -
      coeff (m.degree f ⊔ m.degree g) ((monomial (m.degree f ⊔ m.degree g - m.degree g)) (m.leadingCoeff f) * g) =
    0
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: p k : ℕ
hp : Nat.Prime p
hk : 0 < k
⊢ (p ^ k).minFac ^ (p ^ k).factorization (p ^ k).minFac = p ^ k

Tactic:
]

Goal state after:
p k : ℕ
hp : Nat.Prime p
hk : 0 < k
⊢ (p ^ k).minFac ^ (p ^ k).factorization (p ^ k).minFac = p ^ k
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: p k : ℕ
hp : Nat.Prime p
hk : 0 < k
⊢ p ^ k = p ^ k

Tactic:
]

Goal state after:
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: n : ℕ
⊢ (∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n) ↔ ∃ p k, 0 < k ∧ n.factorization = Finsupp.single p k

Tactic:
]

Goal state after:
n : ℕ
⊢ (∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n) ↔ ∃ p k, 0 < k ∧ n.factorization = Finsupp.single p k
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: n p k : ℕ
hp : Nat.Prime p
hk : 0 < k
hn : p ^ k = n
⊢ Finsupp.single p k = Finsupp.single p k

Tactic:
]

Goal state after:
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: case mpr
n p k : ℕ
hk : 0 < k
hn : n.factorization = Finsupp.single p k
hn0 : n ≠ 0
⊢ Nat.Prime p ∧ 0 < k ∧ p ^ k = p ^ k

Tactic:
]

Goal state after:
case mpr
n p k : ℕ
hk : 0 < k
hn : n.factorization = Finsupp.single p k
hn0 : n ≠ 0
⊢ Nat.Prime p ∧ 0 < k ∧ p ^ k = p ^ k
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
f : ℕ → R
hf : Invertible (f 1)
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: n : ℕ
hn : 2 ≤ n
⊢ ¬n.primeFactors.card = 1 ↔ 1 < n.primeFactors.card

Tactic:
]

Goal state after:
n : ℕ
hn : 2 ≤ n
⊢ ¬n.primeFactors.card = 1 ↔ 1 < n.primeFactors.card
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
f : ℕ → R
hf : Invertible (f 1)
⊢ ⅟(f 1) = ⅟(f 1)

Tactic:
]

Goal state after:
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case h
n : ℕ
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ x, s = x ^ 2}
hSne : S.Nonempty
s : ℕ := S.max' hSne
a b : ℕ
hn : 0 < b ^ 2 * a
hsa : n = b ^ 2 * a
hsb : s = b ^ 2
hlts : 0 < b ^ 2
hlta : 0 < a
x y : ℕ
hy : a = x * x * y
hx : ¬x = 1
⊢ b ^ 2 * (x * x * y) = (b * x) ^ 2 * y

Tactic:
]

Goal state after:
case h
n : ℕ
S : Finset ℕ := {s ∈ range (n + 1) | s ∣ n ∧ ∃ x, s = x ^ 2}
hSne : S.Nonempty
s : ℕ := S.max' hSne
a b : ℕ
hn : 0 < b ^ 2 * a
hsa : n = b ^ 2 * a
hsb : s = b ^ 2
hlts : 0 < b ^ 2
hlta : 0 < a
x y : ℕ
hy : a = x * x * y
hx : ¬x = 1
⊢ b ^ 2 * (x * x * y) = (b * x) ^ 2 * y
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
f : ℕ → R
hf : Invertible (f 1)
n : ℕ
hn0 : n ≠ 0
hn1 : n ≠ 1
⊢ (-⅟(f 1) *
      ∑ d,
        have this := ⋯;
        f (n / ↑d) * dirichletInverseFun f hf ↑d) =
    -⅟(f 1) * ∑ d ∈ n.properDivisors, f (n / d) * dirichletInverseFun f hf d

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : Ring R
f : ℕ → R
hf : Invertible (f 1)
n : ℕ
hn0 : n ≠ 0
hn1 : n ≠ 1
⊢ (-⅟(f 1) *
      ∑ d,
        have this := ⋯;
        f (n / ↑d) * dirichletInverseFun f hf ↑d) =
    -⅟(f 1) * ∑ d ∈ n.properDivisors, f (n / d) * dirichletInverseFun f hf d
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: case inr.inr
n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : n.factorization = Finsupp.single p k
pp : Nat.Prime p
q : ℕ
⊢ (Finsupp.erase p (Finsupp.single p k)) q = (Nat.factorization 1) q

Tactic:
]

Goal state after:
case inr.inr
n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : n.factorization = Finsupp.single p k
pp : Nat.Prime p
q : ℕ
⊢ (Finsupp.erase p (Finsupp.single p k)) q = (Nat.factorization 1) q
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: n : ℕ
hn : n ≠ 1
p : ℕ
pp : Nat.Prime p
h : n / p ^ n.factorization p = 1
⊢ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n

Tactic:
]

Goal state after:
n : ℕ
hn : n ≠ 1
p : ℕ
pp : Nat.Prime p
h : n / p ^ n.factorization p = 1
⊢ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: n p : ℕ
hn : p ^ n.factorization p ≠ 1
pp : Nat.Prime p
h : n / p ^ n.factorization p = 1
⊢ ∃ p_1 k, Nat.Prime p_1 ∧ 0 < k ∧ p_1 ^ k = p ^ n.factorization p

Tactic:
]

Goal state after:
n p : ℕ
hn : p ^ n.factorization p ≠ 1
pp : Nat.Prime p
h : n / p ^ n.factorization p = 1
⊢ ∃ p_1 k, Nat.Prime p_1 ∧ 0 < k ∧ p_1 ^ k = p ^ n.factorization p
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: n : ℕ
⊢ (∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n) ↔ ∃! p, Nat.Prime p ∧ p ∣ n

Tactic:
]

Goal state after:
n : ℕ
⊢ (∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n) ↔ ∃! p, Nat.Prime p ∧ p ∣ n
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
hf : ¬(m.degree f = 0 ∧ m.degree g = 0)
⊢ ¬m.sPolynomial f g = 0 → m.toSyn (m.degree (m.sPolynomial f g)) < m.toSyn (m.degree f ⊔ m.degree g)

Tactic:
]

Goal state after:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
hf : ¬(m.degree f = 0 ∧ m.degree g = 0)
⊢ ¬m.sPolynomial f g = 0 → m.toSyn (m.degree (m.sPolynomial f g)) < m.toSyn (m.degree f ⊔ m.degree g)
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case zero
⊢ ∃ a b, b ^ 2 * a = 0 ∧ Squarefree a

pp: case succ
n : ℕ
⊢ ∃ a b, b ^ 2 * a = n + 1 ∧ Squarefree a

Tactic:
· exact ⟨1, 0, by simp, squarefree_one⟩

Goal state after:
case succ
n : ℕ
⊢ ∃ a b, b ^ 2 * a = n + 1 ∧ Squarefree a
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: m n : ℕ
⊢ IsRelPrime m n ∧ Squarefree m ∧ Squarefree n ↔ IsRelPrime m n ∧ Squarefree m ∧ Squarefree n

Tactic:
]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Ring R
f : ArithmeticFunction R
hf : Invertible (f 1)
n : ℕ
hn0 : ¬n = 0
hn1 : ¬n = 1
⊢ ∑ i ∈ cons n n.properDivisors ⋯, f (n / i) * dirichletInverseFun (⇑f) hf i = 1 n

Tactic:
]

Goal state after:
case neg
R : Type u_1
inst✝ : Ring R
f : ArithmeticFunction R
hf : Invertible (f 1)
n : ℕ
hn0 : ¬n = 0
hn1 : ¬n = 1
⊢ ∑ i ∈ cons n n.properDivisors ⋯, f (n / i) * dirichletInverseFun (⇑f) hf i = 1 n
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n : ℕ
hn : Squarefree n
⊢ n = n

Tactic:
]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : ArithmeticFunction R
hf : Invertible (f 1)
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: s : Finset ℕ
hs : ∀ p ∈ s, Prime p
hn : ∏ p ∈ s, p ≠ 0
p : ℕ
⊢ (Prime p ∧ ∃ a ∈ s, p ∣ a) ↔ p ∈ s

Tactic:
]

Goal state after:
s : Finset ℕ
hs : ∀ p ∈ s, Prime p
hn : ∏ p ∈ s, p ≠ 0
p : ℕ
⊢ (Prime p ∧ ∃ a ∈ s, p ∣ a) ↔ p ∈ s
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: case mp.refine_1
R : Type u_1
inst✝ : CommRing R
f : (ArithmeticFunction R)ˣ
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: case mpr.inr
n p : ℕ
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
hq : ∀ (y : ℕ), Nat.Prime y → y ∣ n → y = p
⊢ ∀ x ∈ n.primeFactorsList, List.count x n.primeFactorsList ≤ List.count x (List.replicate (n.factorization p) p)

Tactic:
]

Goal state after:
case mpr.inr
n p : ℕ
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
hq : ∀ (y : ℕ), Nat.Prime y → y ∣ n → y = p
⊢ ∀ x ∈ n.primeFactorsList, List.count x n.primeFactorsList ≤ List.count x (List.replicate (n.factorization p) p)
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: s : Finset ℕ
hs : ∀ p ∈ s, Prime p
hn : ∏ p ∈ s, p ≠ 0
p : ℕ
hp : Prime p
q : ℕ
hq : q ∈ s
hpq : p ∣ q
⊢ q ∈ s

Tactic:
]

Goal state after:
s : Finset ℕ
hs : ∀ p ∈ s, Prime p
hn : ∏ p ∈ s, p ≠ 0
p : ℕ
hp : Prime p
q : ℕ
hq : q ∈ s
hpq : p ∣ q
⊢ q ∈ s
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: case mp.refine_2
R : Type u_1
inst✝ : CommRing R
f : (ArithmeticFunction R)ˣ
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: case mpr.inr
n p : ℕ
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
hq : ∀ (y : ℕ), Nat.Prime y → y ∣ n → y = p
q : ℕ
hq' : Nat.Prime q ∧ q ∣ n
⊢ List.count q n.primeFactorsList ≤ List.count q (List.replicate (n.factorization p) p)

Tactic:
]

Goal state after:
case mpr.inr
n p : ℕ
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
hq : ∀ (y : ℕ), Nat.Prime y → y ∣ n → y = p
q : ℕ
hq' : Nat.Prime q ∧ q ∣ n
⊢ List.count q n.primeFactorsList ≤ List.count q (List.replicate (n.factorization p) p)
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case refine_1
n k : ℕ
hk : k ≠ 0
h : ∏ p ∈ n.primeFactors, p ∣ k
⊢ n.primeFactors ⊆ n.primeFactors

Tactic:
]

Goal state after:
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case refine_2
n k : ℕ
hk : k ≠ 0
h : n.primeFactors ⊆ k.primeFactors
⊢ ∏ i ∈ k.primeFactors, i ∣ ∏ p ∈ k.primeFactors, p

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
hf : ¬(m.degree f = 0 ∧ m.degree g = 0)
hs : m.degree (m.sPolynomial f g) = m.degree f ⊔ m.degree g
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: m n : ℕ
hm : Squarefree m
hn : n ≠ 0
p : ℕ
this : m / m.gcd n ≠ 0
hp : (Prime p ∧ p ∣ m) ∧ (Prime p → ¬p ∣ n)
⊢ ¬p ∣ m.gcd n

Tactic:
]

Goal state after:
m n : ℕ
hm : Squarefree m
hn : n ≠ 0
p : ℕ
this : m / m.gcd n ≠ 0
hp : (Prime p ∧ p ∣ m) ∧ (Prime p → ¬p ∣ n)
⊢ ¬p ∣ m.gcd n
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n : ℕ
hn : Squarefree n
t : Finset ℕ
ht : t ⊆ n.primeFactors
⊢ n = n

Tactic:
]

Goal state after: