mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p : MvPolynomial σ R
i : σ
a✝ : Nontrivial R
⊢ p ∣ 1 • X i ↔ ∃ r, IsUnit r ∧ (p = C r ∨ p = r • 1 • X i)

Tactic:
dvd_smul_X_iff_exists (one_ne_zero' R)

Goal state after:
R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p : MvPolynomial σ R
i : σ
a✝ : Nontrivial R
⊢ (∃ s, s ∣ 1 ∧ (p = C s ∨ p = s • X i)) ↔ ∃ r, IsUnit r ∧ (p = C r ∨ p = r • 1 • X i)
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
d : σ →₀ ℕ
c : R
inst✝ : Decidable (c = 0)
hc : c = 0
⊢ m.toSyn.symm (∅.sup ⇑m.toSyn) = 0

pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
d : σ →₀ ℕ
c : R
inst✝ : Decidable (c = 0)
hc : ¬c = 0
⊢ m.toSyn.symm ({d}.sup ⇑m.toSyn) = d

Tactic:
<;>

Goal state after:
case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
d : σ →₀ ℕ
c : R
inst✝ : Decidable (c = 0)
hc : c = 0
⊢ m.toSyn.symm (∅.sup ⇑m.toSyn) = 0

case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
d : σ →₀ ℕ
c : R
inst✝ : Decidable (c = 0)
hc : ¬c = 0
⊢ m.toSyn.symm ({d}.sup ⇑m.toSyn) = d
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
d : σ →₀ ℕ
c : R
hc : c = 0
⊢ coeff 0 ((monomial d) c) = c

pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
d : σ →₀ ℕ
c : R
hc : ¬c = 0
⊢ coeff d ((monomial d) c) = c

Tactic:
<;>

Goal state after:
case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
d : σ →₀ ℕ
c : R
hc : c = 0
⊢ coeff 0 ((monomial d) c) = c

case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
d : σ →₀ ℕ
c : R
hc : ¬c = 0
⊢ coeff d ((monomial d) c) = c
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.toSyn (m.degree (∑ x ∈ s, f x)) ≤ s.sup fun x ↦ m.toSyn (m.degree (f x))
⊢ m.toSyn (m.degree (f a + ∑ x ∈ s, f x)) ≤ (Finset.cons a s haA).sup fun x ↦ m.toSyn (m.degree (f x))

Tactic:
Finset.sup_cons

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.toSyn (m.degree (∑ x ∈ s, f x)) ≤ s.sup fun x ↦ m.toSyn (m.degree (f x))
⊢ m.toSyn (m.degree (f a + ∑ x ∈ s, f x)) ≤ max (m.toSyn (m.degree (f a))) (s.sup fun x ↦ m.toSyn (m.degree (f x)))
Module: Mathlib.Data.Sym.Card

Goal state before:
pp: n k : ℕ
⊢ Fintype.card (Sym (Fin (n + 2)) (k + 1)) = (n + 2).multichoose (k + 1)

Tactic:
multichoose_succ_succ,

Goal state after:
n k : ℕ
⊢ Fintype.card (Sym (Fin (n + 2)) (k + 1)) = (n + 1).multichoose (k + 1) + (n + 1 + 1).multichoose k
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case pos.inl
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f g : MvPolynomial σ R
h✝ : f = 0
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

pp: case pos.inr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f g : MvPolynomial σ R
h✝ : g = 0
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

Tactic:
<;>

Goal state after:
case pos.inl
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f g : MvPolynomial σ R
h✝ : f = 0
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

case pos.inr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f g : MvPolynomial σ R
h✝ : g = 0
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g
Module: Mathlib.Algebra.MvPolynomial.SchwartzZippel

Goal state before:
pp: 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
⊢ ↑(#({x ∈ piFinset fun i ↦ S i | (eval x) p = 0})) / ∏ i, ↑(#(S i)) =
    ↑(#({x ∈ piFinset fun i ↦ S i | (eval x) p = 0 ∧ (eval (tail x)) pₖ = 0}) +
          #({x ∈ piFinset fun i ↦ S i | (eval x) p = 0 ∧ (eval (tail x)) pₖ ≠ 0})) /
      ∏ i, ↑(#(S i))

Tactic:
← card_union_add_card_inter,

Goal state after:
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
⊢ ↑(#({x ∈ piFinset fun i ↦ S i | (eval x) p = 0})) / ∏ i, ↑(#(S i)) =
    ↑(#({x ∈ piFinset fun i ↦ S i | (eval x) p = 0 ∧ (eval (tail x)) pₖ = 0} ∪
              {x ∈ piFinset fun i ↦ S i | (eval x) p = 0 ∧ (eval (tail x)) pₖ ≠ 0}) +
          #({x ∈ piFinset fun i ↦ S i | (eval x) p = 0 ∧ (eval (tail x)) pₖ = 0} ∩
              {x ∈ piFinset fun i ↦ S i | (eval x) p = 0 ∧ (eval (tail x)) pₖ ≠ 0})) /
      ∏ i, ↑(#(S i))
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case insert
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
a : ι
s : Finset ι
has : a ∉ s
hrec : m.toSyn (m.degree (∏ i ∈ s, P i)) ≤ m.toSyn (∑ i ∈ s, m.degree (P i))
⊢ m.toSyn (m.degree (P a * ∏ x ∈ s, P x)) ≤ m.toSyn (m.degree (P a) + ∑ x ∈ s, m.degree (P x))

Tactic:
apply le_trans degree_mul_le

Goal state after:
case insert
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
a : ι
s : Finset ι
has : a ∉ s
hrec : m.toSyn (m.degree (∏ i ∈ s, P i)) ≤ m.toSyn (∑ i ∈ s, m.degree (P i))
⊢ m.toSyn (m.degree (P a) + m.degree (∏ x ∈ s, P x)) ≤ m.toSyn (m.degree (P a) + ∑ x ∈ s, m.degree (P x))
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, P i ≠ 0
⊢ m.degree (∏ i ∈ s, P i) = ∑ i ∈ s, m.degree (P i)

Tactic:
cases subsingleton_or_nontrivial R with
  | inl _ => simp [Subsingleton.elim _ (0 : MvPolynomial σ R)]
  | inr _ =>
    apply m.toSyn.injective
    refine le_antisymm degree_prod_le (m.le_degree ?_)
    simpa [m.coeff_prod_sum_degree, Finset.prod_eq_zero_iff]

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

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
h : f = 0
⊢ m.leadingTerm (m.leadingTerm f) = m.leadingTerm f

pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
h : ¬f = 0
⊢ m.leadingTerm (m.leadingTerm f) = m.leadingTerm f

Tactic:
<;>

Goal state after:
case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
h : f = 0
⊢ m.leadingTerm (m.leadingTerm f) = m.leadingTerm f

case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
h : ¬f = 0
⊢ m.leadingTerm (m.leadingTerm f) = m.leadingTerm f
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
s : σ →₀ ℕ
c : R
h : c = 0
⊢ m.leadingTerm ((monomial s) c) = (monomial s) c

pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
s : σ →₀ ℕ
c : R
h : ¬c = 0
⊢ m.leadingTerm ((monomial s) c) = (monomial s) c

Tactic:
<;>

Goal state after:
case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
s : σ →₀ ℕ
c : R
h : c = 0
⊢ m.leadingTerm ((monomial s) c) = (monomial s) c

case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
s : σ →₀ ℕ
c : R
h : ¬c = 0
⊢ m.leadingTerm ((monomial s) c) = (monomial s) c
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case inr.inl
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
q : MvPolynomial σ R
this :
  ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] [NoZeroDivisors R]
    (p q : MvPolynomial σ R), p ≠ 0 ∧ q ≠ 0 → m.degree (m.leadingTerm p * q) = m.degree (p * q)
⊢ m.degree (m.leadingTerm 0 * q) = m.degree (0 * q)

pp: case inr.inr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : MvPolynomial σ R
this :
  ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] [NoZeroDivisors R]
    (p q : MvPolynomial σ R), p ≠ 0 ∧ q ≠ 0 → m.degree (m.leadingTerm p * q) = m.degree (p * q)
⊢ m.degree (m.leadingTerm p * 0) = m.degree (p * 0)

Tactic:
<;>

Goal state after:
case inr.inl
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
q : MvPolynomial σ R
this :
  ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] [NoZeroDivisors R]
    (p q : MvPolynomial σ R), p ≠ 0 ∧ q ≠ 0 → m.degree (m.leadingTerm p * q) = m.degree (p * q)
⊢ m.degree (m.leadingTerm 0 * q) = m.degree (0 * q)

case inr.inr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : MvPolynomial σ R
this :
  ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] [NoZeroDivisors R]
    (p q : MvPolynomial σ R), p ≠ 0 ∧ q ≠ 0 → m.degree (m.leadingTerm p * q) = m.degree (p * q)
⊢ m.degree (m.leadingTerm p * 0) = m.degree (p * 0)
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case pos
n p : ℕ
hn : ∀ (x : ℕ), emultiplicity x n ≤ 1 ∨ IsUnit x
hn' : n ≠ 0
hp : Prime p
⊢ n.factorization p ≤ 1

Tactic:
have := hn p
    rw [← multiplicity_eq_factorization hp hn']
    simp only [Nat.isUnit_iff, hp.ne_one, or_false] at this
    exact multiplicity_le_of_emultiplicity_le this

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

Goal state before:
pp: case pos
n m : ℕ
hn : Squarefree n
hm : Squarefree m
h : ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ m)
p : ℕ
hp : Prime p
⊢ n.factorization p = m.factorization p

Tactic:
have h₁ := h _ hp
    rw [← not_iff_not, hp.dvd_iff_one_le_factorization hn.ne_zero, not_le, lt_one_iff,
      hp.dvd_iff_one_le_factorization hm.ne_zero, not_le, lt_one_iff] at h₁
    have h₂ := hn.natFactorization_le_one p
    have h₃ := hm.natFactorization_le_one p
    lia

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

Goal state before:
pp: case pos
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : n < k * k
⊢ n.MinSqFacProp
    (if h : n < k * k then none
    else
      have this := ⋯;
      if k ∣ n then
        let n' := n / k;
        have this := ⋯;
        if k ∣ n' then some k else n'.minSqFacAux (k + 2)
      else n.minSqFacAux (k + 2))

pp: case neg
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
⊢ n.MinSqFacProp
    (if h : n < k * k then none
    else
      have this := ⋯;
      if k ∣ n then
        let n' := n / k;
        have this := ⋯;
        if k ∣ n' then some k else n'.minSqFacAux (k + 2)
      else n.minSqFacAux (k + 2))

Tactic:
<;>

Goal state after:
case pos
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : n < k * k
⊢ n.MinSqFacProp
    (if h : n < k * k then none
    else
      have this := ⋯;
      if k ∣ n then
        let n' := n / k;
        have this := ⋯;
        if k ∣ n' then some k else n'.minSqFacAux (k + 2)
      else n.minSqFacAux (k + 2))

case neg
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
⊢ n.MinSqFacProp
    (if h : n < k * k then none
    else
      have this := ⋯;
      if k ∣ n then
        let n' := n / k;
        have this := ⋯;
        if k ∣ n' then some k else n'.minSqFacAux (k + 2)
      else n.minSqFacAux (k + 2))
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
⊢ n'.MinSqFacProp (n'.minSqFacAux (k + 2))

Tactic:
have hn' := le_of_dvd n0 nd'

Goal state after:
n k : ℕ
n0 : 0 < n
i : ℕ
e : k = 2 * i + 3
ih : ∀ (m : ℕ), Prime m → m ∣ n → k ≤ m
h : ¬n < k * k
k2 : 2 ≤ k
k0 : 0 < k
n' : ℕ
nd' : n' ∣ n
nk : ¬k ∣ n'
hn' : n' ≤ n
⊢ n'.MinSqFacProp (n'.minSqFacAux (k + 2))
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

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

pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
h : ¬f = 0
⊢ m.degree f = WithBot.unbotD 0 (m.withBotDegree f)

Tactic:
<;>

Goal state after:
case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
h : f = 0
⊢ m.degree f = WithBot.unbotD 0 (m.withBotDegree f)

case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
h : ¬f = 0
⊢ m.degree f = WithBot.unbotD 0 (m.withBotDegree f)
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
d : σ →₀ ℕ
c : R
inst✝ : Decidable (c = 0)
h✝ : c = 0
⊢ m.withBotDegree ((monomial d) c) = ⊥

pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
d : σ →₀ ℕ
c : R
inst✝ : Decidable (c = 0)
h✝ : ¬c = 0
⊢ m.withBotDegree ((monomial d) c) = ↑d

Tactic:
<;>

Goal state after:
case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
d : σ →₀ ℕ
c : R
inst✝ : Decidable (c = 0)
h✝ : c = 0
⊢ m.withBotDegree ((monomial d) c) = ⊥

case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
d : σ →₀ ℕ
c : R
inst✝ : Decidable (c = 0)
h✝ : ¬c = 0
⊢ m.withBotDegree ((monomial d) c) = ↑d
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case pos.inl
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hf : m.leadingCoeff f ∈ R⁰
h0 : f = 0
⊢ m.withBotDegree (f * g) = m.withBotDegree f + m.withBotDegree g

pp: case pos.inr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hf : m.leadingCoeff f ∈ R⁰
h0 : g = 0
⊢ m.withBotDegree (f * g) = m.withBotDegree f + m.withBotDegree g

Tactic:
<;>

Goal state after:
case pos.inl
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hf : m.leadingCoeff f ∈ R⁰
h0 : f = 0
⊢ m.withBotDegree (f * g) = m.withBotDegree f + m.withBotDegree g

case pos.inr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hf : m.leadingCoeff f ∈ R⁰
h0 : g = 0
⊢ m.withBotDegree (f * g) = m.withBotDegree f + m.withBotDegree g
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case neg
n : ℕ
d2 : ¬2 ∣ n
⊢ n.MinSqFacProp (n.minSqFacAux 3)

Tactic:
rcases Nat.eq_zero_or_pos n with rfl | n0
    · cases d2 (by decide)
    refine minSqFacAux_has_prop _ n0 0 rfl ?_
    refine fun p pp dp => succ_le_of_lt (lt_of_le_of_ne pp.two_le ?_)
    rintro rfl
    contradiction

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

Goal state before:
pp: case mp
n : ℕ
this : n.MinSqFacProp n.minSqFac
⊢ Squarefree n → n.minSqFac = none

pp: case mpr
n : ℕ
this : n.MinSqFacProp n.minSqFac
⊢ n.minSqFac = none → Squarefree n

Tactic:
<;>

Goal state after:
case mp
n : ℕ
this : n.MinSqFacProp n.minSqFac
⊢ Squarefree n → n.minSqFac = none

case mpr
n : ℕ
this : n.MinSqFacProp n.minSqFac
⊢ n.minSqFac = none → Squarefree n
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: ⊢ (primeFactorsList 2).Nodup

pp: ⊢ 2 ≠ 0

Tactic:
<;>

Goal state after:
⊢ (primeFactorsList 2).Nodup

⊢ 2 ≠ 0
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case mp
n : ℕ
h0 : n ≠ 0
a : ℕ
⊢ (a ∣ n ∧ n ≠ 0) ∧ Squarefree a → ∃ a_2 ∈ (normalizedFactors n).toFinset.powerset, a_2.val.prod = a

Tactic:
rintro ⟨⟨an, h0⟩, hsq⟩
      use (UniqueFactorizationMonoid.normalizedFactors a).toFinset
      simp only [Finset.mem_powerset]
      rcases an with ⟨b, rfl⟩
      rw [mul_ne_zero_iff] at h0
      rw [UniqueFactorizationMonoid.squarefree_iff_nodup_normalizedFactors h0.1] at hsq
      rw [Multiset.toFinset_subset, Multiset.toFinset_val, hsq.dedup, ← associated_iff_eq,
        normalizedFactors_mul h0.1 h0.2]
      exact ⟨Multiset.subset_of_le (Multiset.le_add_right _ _), prod_normalizedFactors h0.1⟩

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

Goal state before:
pp: σ : 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)

Tactic:
by
  simp [withBotDegree_le_withBotDegree_iff, hg]

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

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

pp: case pos.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 + g)) ≤
    max (m.toWithBotSyn (m.withBotDegree f)) (m.toWithBotSyn (m.withBotDegree g))

Tactic:
<;>

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

case pos.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 + g)) ≤
    max (m.toWithBotSyn (m.withBotDegree f)) (m.toWithBotSyn (m.withBotDegree g))
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)) ≤
    (Finset.cons a s haA).sup fun x ↦ m.toWithBotSyn (m.withBotDegree (f x))

Tactic:
Finset.sup_cons

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.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case inl
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f✝ g✝ f g : MvPolynomial σ R
a : σ
h : (m.degree f) a ≤ (m.degree g) a
⊢ (m.degree g - m.degree f) a = (m.degree f ⊔ m.degree g - m.degree f) a

pp: case inr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f✝ g✝ f g : MvPolynomial σ R
a : σ
h : (m.degree g) a ≤ (m.degree f) a
⊢ (m.degree g - m.degree f) a = (m.degree f ⊔ m.degree g - m.degree f) a

Tactic:
<;>

Goal state after:
case inl
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f✝ g✝ f g : MvPolynomial σ R
a : σ
h : (m.degree f) a ≤ (m.degree g) a
⊢ (m.degree g - m.degree f) a = (m.degree f ⊔ m.degree g - m.degree f) a

case inr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f✝ g✝ f g : MvPolynomial σ R
a : σ
h : (m.degree g) a ≤ (m.degree f) a
⊢ (m.degree g - m.degree f) a = (m.degree f ⊔ m.degree g - m.degree f) a
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: case pos
R : Type u_1
inst✝ : AddMonoidWithOne R
n x : ℕ
h : x = 1
⊢ { toFun := fun x ↦ if x = 1 then ↑(n + 1) else 0, map_zero' := ⋯ } x =
    ({ toFun := fun x ↦ if x = 1 then ↑n else 0, map_zero' := ⋯ } + 1) x

pp: case neg
R : Type u_1
inst✝ : AddMonoidWithOne R
n x : ℕ
h : ¬x = 1
⊢ { toFun := fun x ↦ if x = 1 then ↑(n + 1) else 0, map_zero' := ⋯ } x =
    ({ toFun := fun x ↦ if x = 1 then ↑n else 0, map_zero' := ⋯ } + 1) x

Tactic:
<;>

Goal state after:
case pos
R : Type u_1
inst✝ : AddMonoidWithOne R
n x : ℕ
h : x = 1
⊢ { toFun := fun x ↦ if x = 1 then ↑(n + 1) else 0, map_zero' := ⋯ } x =
    ({ toFun := fun x ↦ if x = 1 then ↑n else 0, map_zero' := ⋯ } + 1) x

case neg
R : Type u_1
inst✝ : AddMonoidWithOne R
n x : ℕ
h : ¬x = 1
⊢ { toFun := fun x ↦ if x = 1 then ↑(n + 1) else 0, map_zero' := ⋯ } x =
    ({ toFun := fun x ↦ if x = 1 then ↑n else 0, map_zero' := ⋯ } + 1) x
Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta

Goal state before:
pp: case zero
R : Type u_1
inst✝ : NonAssocSemiring R
f : ArithmeticFunction R
⊢ (f.pmul ↑ζ) 0 = f 0

pp: case succ
R : Type u_1
inst✝ : NonAssocSemiring R
f : ArithmeticFunction R
n✝ : ℕ
⊢ (f.pmul ↑ζ) (n✝ + 1) = f (n✝ + 1)

Tactic:
<;>

Goal state after:
case zero
R : Type u_1
inst✝ : NonAssocSemiring R
f : ArithmeticFunction R
⊢ (f.pmul ↑ζ) 0 = f 0

case succ
R : Type u_1
inst✝ : NonAssocSemiring R
f : ArithmeticFunction R
n✝ : ℕ
⊢ (f.pmul ↑ζ) (n✝ + 1) = f (n✝ + 1)
Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta

Goal state before:
pp: case zero
R : Type u_1
inst✝ : NonAssocSemiring R
f : ArithmeticFunction R
⊢ ((↑ζ).pmul f) 0 = f 0

pp: case succ
R : Type u_1
inst✝ : NonAssocSemiring R
f : ArithmeticFunction R
n✝ : ℕ
⊢ ((↑ζ).pmul f) (n✝ + 1) = f (n✝ + 1)

Tactic:
<;>

Goal state after:
case zero
R : Type u_1
inst✝ : NonAssocSemiring R
f : ArithmeticFunction R
⊢ ((↑ζ).pmul f) 0 = f 0

case succ
R : Type u_1
inst✝ : NonAssocSemiring R
f : ArithmeticFunction R
n✝ : ℕ
⊢ ((↑ζ).pmul f) (n✝ + 1) = f (n✝ + 1)
Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta

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

pp: case succ
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x n✝ : ℕ
a✝ : f x * f x ^ n✝ = (f.pmul (f.ppow n✝)) x
⊢ f x * f x ^ (n✝ + 1) = (f.pmul (f.ppow (n✝ + 1))) x

Tactic:
<;>

Goal state after:
case zero
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x : ℕ
⊢ f x * f x ^ 0 = (f.pmul (f.ppow 0)) x

case succ
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x n✝ : ℕ
a✝ : f x * f x ^ n✝ = (f.pmul (f.ppow n✝)) x
⊢ f x * f x ^ (n✝ + 1) = (f.pmul (f.ppow (n✝ + 1))) x