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

Goal state before:
pp: case neg.inl
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : f = 0
⊢ m.toWithBotSyn (m.withBotDegree f) ≤ m.toWithBotSyn (m.withBotDegree g) ↔
    m.toSyn (m.degree f) ≤ m.toSyn (m.degree g) ∧ (g = 0 → f = 0)

pp: case neg.inr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h✝ : g = 0
⊢ m.toWithBotSyn (m.withBotDegree f) ≤ m.toWithBotSyn (m.withBotDegree g) ↔
    m.toSyn (m.degree f) ≤ m.toSyn (m.degree g) ∧ (g = 0 → f = 0)

Tactic:
·

Goal state after:
case neg.inl
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : f = 0
⊢ m.toWithBotSyn (m.withBotDegree f) ≤ m.toWithBotSyn (m.withBotDegree g) ↔
    m.toSyn (m.degree f) ≤ m.toSyn (m.degree g) ∧ (g = 0 → f = 0)
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case neg.inr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h✝ : g = 0
⊢ m.toWithBotSyn (m.withBotDegree f) ≤ m.toWithBotSyn (m.withBotDegree g) ↔
    m.toSyn (m.degree f) ≤ m.toSyn (m.degree g) ∧ (g = 0 → f = 0)

Tactic:
·

Goal state after:
case neg.inr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h✝ : g = 0
⊢ m.toWithBotSyn (m.withBotDegree f) ≤ m.toWithBotSyn (m.withBotDegree g) ↔
    m.toSyn (m.degree f) ≤ m.toSyn (m.degree g) ∧ (g = 0 → f = 0)
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hg : g = 0
⊢ m.toWithBotSyn (m.withBotDegree f) < m.toWithBotSyn (m.withBotDegree g) ↔
    m.toSyn (m.degree f) < m.toSyn (m.degree g) ∨ f = 0 ∧ g ≠ 0

pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hg : g ≠ 0
⊢ m.toWithBotSyn (m.withBotDegree f) < m.toWithBotSyn (m.withBotDegree g) ↔
    m.toSyn (m.degree f) < m.toSyn (m.degree g) ∨ f = 0 ∧ g ≠ 0

Tactic:
·

Goal state after:
case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hg : g = 0
⊢ m.toWithBotSyn (m.withBotDegree f) < m.toWithBotSyn (m.withBotDegree g) ↔
    m.toSyn (m.degree f) < m.toSyn (m.degree g) ∨ f = 0 ∧ g ≠ 0
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hg : g ≠ 0
hf : f = 0
⊢ m.toWithBotSyn (m.withBotDegree f) < m.toWithBotSyn (m.withBotDegree g) ↔
    m.toSyn (m.degree f) < m.toSyn (m.degree g) ∨ f = 0 ∧ g ≠ 0

pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hg : g ≠ 0
hf : f ≠ 0
⊢ m.toWithBotSyn (m.withBotDegree f) < m.toWithBotSyn (m.withBotDegree g) ↔
    m.toSyn (m.degree f) < m.toSyn (m.degree g) ∨ f = 0 ∧ g ≠ 0

Tactic:
·

Goal state after:
case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hg : g ≠ 0
hf : f = 0
⊢ m.toWithBotSyn (m.withBotDegree f) < m.toWithBotSyn (m.withBotDegree g) ↔
    m.toSyn (m.degree f) < m.toSyn (m.degree g) ∨ f = 0 ∧ g ≠ 0
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : f ≠ 0 ∧ g ≠ 0
⊢ m.withBotDegree f = m.withBotDegree g ↔ m.degree f = m.degree g ∧ (f = 0 ↔ g = 0)

pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : f = 0 ∨ g = 0
⊢ m.withBotDegree f = m.withBotDegree g ↔ m.degree f = m.degree g ∧ (f = 0 ↔ g = 0)

Tactic:
·

Goal state after:
case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : f ≠ 0 ∧ g ≠ 0
⊢ m.withBotDegree f = m.withBotDegree g ↔ m.degree f = m.degree g ∧ (f = 0 ↔ g = 0)
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n : ℕ
h0 : n ≠ 0
⊢ ∀ x ∈ (normalizedFactors n).toFinset.powerset.val,
    ∀ y ∈ (normalizedFactors n).toFinset.powerset.val, x.val.prod = y.val.prod → x = y

Tactic:
·

Goal state after:
n : ℕ
h0 : n ≠ 0
⊢ ∀ x ∈ (normalizedFactors n).toFinset.powerset.val,
    ∀ y ∈ (normalizedFactors n).toFinset.powerset.val, x.val.prod = y.val.prod → x = y
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : f = 0 ∨ g = 0
⊢ m.toWithBotSyn (m.withBotDegree (f + g)) ≤
    max (m.toWithBotSyn (m.withBotDegree f)) (m.toWithBotSyn (m.withBotDegree g))

pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : f ≠ 0 ∧ g ≠ 0
⊢ m.toWithBotSyn (m.withBotDegree (f + g)) ≤
    max (m.toWithBotSyn (m.withBotDegree f)) (m.toWithBotSyn (m.withBotDegree g))

Tactic:
·

Goal state after:
case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : f = 0 ∨ g = 0
⊢ m.toWithBotSyn (m.withBotDegree (f + g)) ≤
    max (m.toWithBotSyn (m.withBotDegree f)) (m.toWithBotSyn (m.withBotDegree g))
Module: Mathlib.Algebra.MvPolynomial.SchwartzZippel

Goal state before:
pp: case calc_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
hp : p ≠ 0
S : Fin (n + 1) → Finset R
p' : Polynomial (MvPolynomial (Fin n) R) := (finSuccEquiv R n) p
hp' : p' = (finSuccEquiv R n) p
k : ℕ := p'.natDegree
hk : k = p'.natDegree
pₖ : MvPolynomial (Fin n) R := p'.leadingCoeff
hpₖ : pₖ = p'.leadingCoeff
hp'₀ : p' ≠ 0
hpₖ₀ : pₖ ≠ 0
⊢ (pₖ.support.sup fun s ↦ ∑ i, ↑(s i) / ↑(#(S i.succ))) + ↑(degreeOf 0 p) / ↑(#(S 0)) ≤
    p.support.sup fun s ↦ ∑ i, ↑(s i) / ↑(#(S i))

Tactic:
·

Goal state after:
case calc_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
hp : p ≠ 0
S : Fin (n + 1) → Finset R
p' : Polynomial (MvPolynomial (Fin n) R) := (finSuccEquiv R n) p
hp' : p' = (finSuccEquiv R n) p
k : ℕ := p'.natDegree
hk : k = p'.natDegree
pₖ : MvPolynomial (Fin n) R := p'.leadingCoeff
hpₖ : pₖ = p'.leadingCoeff
hp'₀ : p' ≠ 0
hpₖ₀ : pₖ ≠ 0
⊢ (pₖ.support.sup fun s ↦ ∑ i, ↑(s i) / ↑(#(S i.succ))) + ↑(degreeOf 0 p) / ↑(#(S 0)) ≤
    p.support.sup fun s ↦ ∑ i, ↑(s i) / ↑(#(S i))
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : m.toWithBotSyn (m.withBotDegree g) < m.toWithBotSyn (m.withBotDegree f)
hg : g = 0
⊢ m.withBotDegree (f + g) = m.withBotDegree f

pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : m.toWithBotSyn (m.withBotDegree g) < m.toWithBotSyn (m.withBotDegree f)
hg : ¬g = 0
⊢ m.withBotDegree (f + g) = m.withBotDegree f

Tactic:
·

Goal state after:
case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : m.toWithBotSyn (m.withBotDegree g) < m.toWithBotSyn (m.withBotDegree f)
hg : g = 0
⊢ m.withBotDegree (f + g) = m.withBotDegree f
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
⊢ ∀ x_1 ∈ x.val, Irreducible x_1

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
⊢ ∀ x ∈ y.val, Irreducible x

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
⊢ ∀ x_1 ∈ x.val, Irreducible x_1
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

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
⊢ ℕ

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
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
⊢ ∀ x ∈ y.val, Irreducible x

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
⊢ ∀ x ∈ y.val, Irreducible x
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case pos
σ : 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.toWithBotSyn (m.withBotDegree f) ≤ m.toWithBotSyn (m.withBotDegree g)

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.toWithBotSyn (m.withBotDegree f) ≤ m.toWithBotSyn (m.withBotDegree g)

Tactic:
·

Goal state after:
case pos
σ : 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.toWithBotSyn (m.withBotDegree f) ≤ m.toWithBotSyn (m.withBotDegree 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

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
⊢ ℕ

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
Module: Mathlib.Algebra.MvPolynomial.SchwartzZippel

Goal state before:
pp: case inl
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ≠ 0
⊢ (p.support.sup fun s ↦ ∑ i, ↑(s i) / ↑(#∅)) = ↑p.totalDegree / ↑(#∅)

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.totalDegree / ↑(#S)

Tactic:
·

Goal state after:
case inl
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ≠ 0
⊢ (p.support.sup fun s ↦ ∑ i, ↑(s i) / ↑(#∅)) = ↑p.totalDegree / ↑(#∅)
Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta

Goal state before:
pp: x : ℕ
⊢ 0 < ζ x ↔ 0 < x

Tactic:
simp [pos_iff_ne_zero]

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 ∈ x.divisorsAntidiagonal, ↑ζ x.1 • f x.2 = ∑ i ∈ x.divisorsAntidiagonal, f i.2

pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : MulAction R M
f : ArithmeticFunction M
x : ℕ
⊢ ∑ i ∈ x.divisorsAntidiagonal, f i.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.divisorsAntidiagonal, f i.2
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 : ℕ
⊢ ∑ i ∈ x.divisorsAntidiagonal, f i.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 : ℕ
⊢ ∑ i ∈ x.divisorsAntidiagonal, f i.2 = ∑ i ∈ x.divisors, f i
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ ↑1 = 1

Tactic:
by
  ext n
  simp [one_apply]

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

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

pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
h : m.degree f ≠ 0
hl : ¬f - m.leadingTerm f = 0
⊢ m.toSyn (m.degree (f - m.leadingTerm f)) < m.toSyn (m.degree f)

Tactic:
·

Goal state after:
case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
h : m.degree f ≠ 0
hl : f - m.leadingTerm f = 0
⊢ m.toSyn (m.degree (f - m.leadingTerm f)) < m.toSyn (m.degree f)
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : AddGroupWithOne R
⊢ ↑1 = 1

Tactic:
by
  ext n
  simp [one_apply]

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
hl : ¬f - m.leadingTerm f = 0
⊢ m.toSyn (m.degree (f - m.leadingTerm f)) < m.toSyn (m.degree f)

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
hl : ¬f - m.leadingTerm f = 0
⊢ m.toSyn (m.degree (f - m.leadingTerm f)) < m.toSyn (m.degree f)
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case refine_1
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
⊢ S.max' ⋯ < (b * x) ^ 2

pp: case refine_2
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 * x) ^ 2 ∈ S

Tactic:
·

Goal state after:
case refine_1
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
⊢ S.max' ⋯ < (b * x) ^ 2
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case inr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
this :
  ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommRing R] (f g : MvPolynomial σ R),
    f ≠ 0 ∧ g ≠ 0 → m.toSyn (m.degree (m.sPolynomial f g)) ≤ m.toSyn (m.degree f ⊔ m.degree g)
h0 : f = 0 ∨ g = 0
⊢ m.toSyn (m.degree (m.sPolynomial f g)) ≤ m.toSyn (m.degree f ⊔ m.degree g)

pp: σ✝ : Type u_1
m✝ : MonomialOrder σ✝
R✝ : Type u_2
inst✝¹ : CommRing R✝
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
h0 : f ≠ 0 ∧ g ≠ 0
⊢ m.toSyn (m.degree (m.sPolynomial f g)) ≤ m.toSyn (m.degree f ⊔ m.degree g)

Tactic:
·

Goal state after:
case inr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
this :
  ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommRing R] (f g : MvPolynomial σ R),
    f ≠ 0 ∧ g ≠ 0 → m.toSyn (m.degree (m.sPolynomial f g)) ≤ m.toSyn (m.degree f ⊔ m.degree g)
h0 : f = 0 ∨ 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 refine_2
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 * x) ^ 2 ∈ S

Tactic:
·

Goal state after:
case refine_2
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 * x) ^ 2 ∈ S
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : ArithmeticFunction R
h : ArithmeticFunction M
⊢ (f * g) • h = f • g • h

Tactic:
ext n
  simp only [mul_apply, smul_apply, sum_smul, mul_smul, smul_sum, sum_sigma']
  apply sum_nbij' (fun ⟨⟨_i, j⟩, ⟨k, l⟩⟩ ↦ ⟨(k, l * j), (l, j)⟩)
    (fun ⟨⟨i, _j⟩, ⟨k, l⟩⟩ ↦ ⟨(i * k, l), (i, k)⟩) <;> aesop (add simp mul_assoc)

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

Goal state before:
pp: case inl
h : Nat.minFac 0 ^ (Nat.factorization 0) (Nat.minFac 0) = 0
hn : 0 ≠ 1
⊢ IsPrimePow 0

pp: case inr
n : ℕ
h : n.minFac ^ n.factorization n.minFac = n
hn : n ≠ 1
hn' : n ≠ 0
⊢ IsPrimePow n

Tactic:
·

Goal state after:
case inl
h : Nat.minFac 0 ^ (Nat.factorization 0) (Nat.minFac 0) = 0
hn : 0 ≠ 1
⊢ IsPrimePow 0
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: case mp
n p k : ℕ
⊢ Nat.Prime p ∧ 0 < k ∧ p ^ k = n → 0 < k ∧ n.factorization = Finsupp.single p k

pp: case mpr
n p k : ℕ
⊢ 0 < k ∧ n.factorization = Finsupp.single p k → Nat.Prime p ∧ 0 < k ∧ p ^ k = n

Tactic:
·

Goal state after:
case mp
n p k : ℕ
⊢ Nat.Prime p ∧ 0 < k ∧ p ^ k = n → 0 < k ∧ n.factorization = Finsupp.single p k
Module: Mathlib.Data.Nat.Factorization.PrimePow

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

Tactic:
·

Goal state after:
case mpr
n p k : ℕ
⊢ 0 < k ∧ n.factorization = Finsupp.single p k → Nat.Prime p ∧ 0 < k ∧ p ^ k = n
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: case inl
h : IsPrimePow 0
⊢ ∃ p, Nat.Prime p ∧ 0 / p ^ (Nat.factorization 0) p = 1

pp: case inr
n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
⊢ ∃ p, Nat.Prime p ∧ n / p ^ n.factorization p = 1

Tactic:
·

Goal state after:
case inl
h : IsPrimePow 0
⊢ ∃ p, Nat.Prime p ∧ 0 / p ^ (Nat.factorization 0) p = 1
Module: Mathlib.Data.Nat.Factorization.PrimePow

Goal state before:
pp: case inr.inl
n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : n.factorization = Finsupp.single p k
pp : ¬Nat.Prime p
⊢ ∃ p, Nat.Prime p ∧ n / p ^ n.factorization p = 1

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
⊢ ∃ p, Nat.Prime p ∧ n / p ^ n.factorization p = 1

Tactic:
·

Goal state after:
case inr.inl
n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
p k : ℕ
hk0 : 0 < k
h1 : n.factorization = Finsupp.single p k
pp : ¬Nat.Prime p
⊢ ∃ p, Nat.Prime p ∧ n / p ^ n.factorization p = 1
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case pos
σ : 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.toSyn (m.degree (m.sPolynomial f g)) < m.toSyn (m.degree f ⊔ m.degree g) ∨ m.sPolynomial f g = 0

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.toSyn (m.degree (m.sPolynomial f g)) < m.toSyn (m.degree f ⊔ m.degree g) ∨ m.sPolynomial f g = 0

Tactic:
·

Goal state after:
case pos
σ : 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.toSyn (m.degree (m.sPolynomial f g)) < m.toSyn (m.degree f ⊔ m.degree g) ∨ m.sPolynomial f g = 0
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Ring R
f : ArithmeticFunction R
hf : Invertible (f 1)
n : ℕ
hn0 : n = 0
⊢ (f * dirichletInverse (⇑f) hf) n = 1 n

pp: case neg
R : Type u_1
inst✝ : Ring R
f : ArithmeticFunction R
hf : Invertible (f 1)
n : ℕ
hn0 : ¬n = 0
⊢ (f * dirichletInverse (⇑f) hf) n = 1 n

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝ : Ring R
f : ArithmeticFunction R
hf : Invertible (f 1)
n : ℕ
hn0 : n = 0
⊢ (f * dirichletInverse (⇑f) hf) n = 1 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.toSyn (m.degree (m.sPolynomial f g)) < m.toSyn (m.degree f ⊔ m.degree g) ∨ m.sPolynomial f g = 0

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.toSyn (m.degree (m.sPolynomial f g)) < m.toSyn (m.degree f ⊔ m.degree g) ∨ m.sPolynomial f g = 0
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Ring R
f : ArithmeticFunction R
hf : Invertible (f 1)
n : ℕ
hn0 : ¬n = 0
hn1 : n = 1
⊢ (f * dirichletInverse (⇑f) hf) n = 1 n

pp: case neg
R : Type u_1
inst✝ : Ring R
f : ArithmeticFunction R
hf : Invertible (f 1)
n : ℕ
hn0 : ¬n = 0
hn1 : ¬n = 1
⊢ (f * dirichletInverse (⇑f) hf) n = 1 n

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝ : Ring R
f : ArithmeticFunction R
hf : Invertible (f 1)
n : ℕ
hn0 : ¬n = 0
hn1 : n = 1
⊢ (f * dirichletInverse (⇑f) hf) n = 1 n
Module: Mathlib.Data.Nat.Factorization.PrimePow

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

pp: case mpr
n : ℕ
⊢ (∃! p, Nat.Prime p ∧ p ∣ n) → ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n

Tactic:
·

Goal state after:
case mp
n : ℕ
⊢ (∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n) → ∃! p, Nat.Prime p ∧ p ∣ n
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:
·

Goal state after:
case zero
⊢ ∃ a b, b ^ 2 * a = 0 ∧ Squarefree a
Module: Mathlib.Data.Nat.Squarefree

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

Tactic:
·

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

Goal state before:
pp: case mpr.inl
p : ℕ
hp : Nat.Prime p
hq : ∀ (y : ℕ), (fun p ↦ Nat.Prime p ∧ p ∣ 0) y → y = p
hn : p ∣ 0
⊢ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = 0

pp: case mpr.inr
n p : ℕ
hq : ∀ (y : ℕ), (fun p ↦ Nat.Prime p ∧ p ∣ n) y → y = p
hp : Nat.Prime p
hn : p ∣ n
hn₀ : n ≠ 0
⊢ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n

Tactic:
·

Goal state after:
case mpr.inl
p : ℕ
hp : Nat.Prime p
hq : ∀ (y : ℕ), (fun p ↦ Nat.Prime p ∧ p ∣ 0) y → y = p
hn : p ∣ 0
⊢ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = 0
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: case mp
R : Type u_1
inst✝ : CommRing R
f : ArithmeticFunction R
⊢ IsUnit f → IsUnit (f 1)

pp: case mpr
R : Type u_1
inst✝ : CommRing R
f : ArithmeticFunction R
⊢ IsUnit (f 1) → IsUnit f

Tactic:
·

Goal state after:
case mp
R : Type u_1
inst✝ : CommRing R
f : ArithmeticFunction R
⊢ IsUnit f → IsUnit (f 1)
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

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

pp: case mp.refine_2
R : Type u_1
inst✝ : CommRing R
f : (ArithmeticFunction R)ˣ
⊢ ↑f⁻¹ 1 * ↑f 1 = 1

Tactic:
·

Goal state after:
case mp.refine_1
R : Type u_1
inst✝ : CommRing R
f : (ArithmeticFunction R)ˣ
⊢ ↑f 1 * ↑f⁻¹ 1 = 1