mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.MonoidAlgebra.ToDirectSum

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Semiring M
inst✝ : (m : M) → Decidable (m ≠ 0)
f g : ⨁ (x : ι), M
⊢ (f + g).toAddMonoidAlgebra = f.toAddMonoidAlgebra + g.toAddMonoidAlgebra

Tactic:
ext

Goal state after:
ι : Type u_1
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Semiring M
inst✝ : (m : M) → Decidable (m ≠ 0)
f g : ⨁ (x : ι), M
a✝ : ι
⊢ (f + g).toAddMonoidAlgebra.coeff a✝ = (f.toAddMonoidAlgebra + g.toAddMonoidAlgebra).coeff a✝
Module: Mathlib.Data.List.ToFinsupp

Goal state before:
pp: M : Type u_1
inst✝¹ : Zero M
inst✝ : DecidablePred fun i ↦ [].getD i 0 ≠ 0
⊢ [].toFinsupp = 0

Tactic:
ext

Goal state after:
M : Type u_1
inst✝¹ : Zero M
inst✝ : DecidablePred fun i ↦ [].getD i 0 ≠ 0
a✝ : ℕ
⊢ [].toFinsupp a✝ = 0 a✝
Module: Mathlib.Algebra.MvPolynomial.Coeff

Goal state before:
pp: case h₁.inl
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
s : σ →₀ ℕ
a : σ →₀ R
n : ℕ
hs : (s.sum fun x m ↦ m) = n
hs'' : s.support ⊆ a.support
hs' : ¬a.support.sum ⇑s = n
⊢ False

Tactic:
apply hs'

Goal state after:
case h₁.inl
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
s : σ →₀ ℕ
a : σ →₀ R
n : ℕ
hs : (s.sum fun x m ↦ m) = n
hs'' : s.support ⊆ a.support
hs' : ¬a.support.sum ⇑s = n
⊢ a.support.sum ⇑s = n
Module: Mathlib.Algebra.MvPolynomial.Division

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
r s : R
i j : σ →₀ ℕ
⊢ (monomial i) r ∣ (monomial j) s ↔ (s = 0 ∨ i ≤ j) ∧ r ∣ s

Tactic:
constructor

Goal state after:
case mp
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
r s : R
i j : σ →₀ ℕ
⊢ (monomial i) r ∣ (monomial j) s → (s = 0 ∨ i ≤ j) ∧ r ∣ s

case mpr
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
r s : R
i j : σ →₀ ℕ
⊢ (s = 0 ∨ i ≤ j) ∧ r ∣ s → (monomial i) r ∣ (monomial j) s
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: α : Type u_1
f : α → ℕ
a b : α
inst✝ : DecidableEq α
h : a ≠ b
⊢ (f a + f b + 1).choose (f a + 1) * (f a + 1) = ((f a).succ + f b).choose (f a).succ * (f a).succ

Tactic:
succ_add (f a) (f b)

Goal state after:
α : Type u_1
f : α → ℕ
a b : α
inst✝ : DecidableEq α
h : a ≠ b
⊢ (f a + f b + 1).choose (f a + 1) * (f a + 1) = (f a + f b).succ.choose (f a).succ * (f a).succ
Module: Mathlib.Algebra.MvPolynomial.Division

Goal state before:
pp: case mpr.inr
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
r : R
i j : σ →₀ ℕ
hij : i ≤ j
d : R
⊢ (monomial j) (r * d) = (monomial i) r * (monomial (j - i)) d

Tactic:
rw [monomial_mul, add_tsub_cancel_of_le hij]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Division

Goal state before:
pp: R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsLeftCancelAdd R
σ : Type u_3
i : σ
p q r : MvPolynomial σ R
h : p = X i * q + r
hr : ∀ n ∈ r.support, n i = 0
h' :
  X i * p.divMonomial (Finsupp.single i 1) + p.modMonomial (Finsupp.single i 1) =
    X i * p.divMonomial (Finsupp.single i 1) + r
⊢ r = p.modMonomial (Finsupp.single i 1)

Tactic:
add_right_inj,

Goal state after:
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsLeftCancelAdd R
σ : Type u_3
i : σ
p q r : MvPolynomial σ R
h : p = X i * q + r
hr : ∀ n ∈ r.support, n i = 0
h' : p.modMonomial (Finsupp.single i 1) = r
⊢ r = p.modMonomial (Finsupp.single i 1)
Module: Mathlib.Algebra.MvPolynomial.Division

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
i : σ
p q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
a✝ : Nontrivial R
⊢ X i ∣ p * q ↔ X i ∣ p ∨ X i ∣ q

Tactic:
constructor

Goal state after:
case mp
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
i : σ
p q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
a✝ : Nontrivial R
⊢ X i ∣ p * q → X i ∣ p ∨ X i ∣ q

case mpr
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
i : σ
p q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
a✝ : Nontrivial R
⊢ X i ∣ p ∨ X i ∣ q → X i ∣ p * q
Module: Mathlib.Algebra.MvPolynomial.Division

Goal state before:
pp: case mp
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
i : σ
p q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
a✝ : Nontrivial R
h : X i ∣ p * q
hp : p.modMonomial (Finsupp.single i 1) + X i * p.divMonomial (Finsupp.single i 1) = p
hq : q.modMonomial (Finsupp.single i 1) + X i * q.divMonomial (Finsupp.single i 1) = q
⊢ ∀ n ∈ (p.modMonomial (Finsupp.single i 1) * q.modMonomial (Finsupp.single i 1)).support, n i = 0

pp: case mp
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
i : σ
p q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
a✝ : Nontrivial R
h : X i ∣ p * q
hp : p.modMonomial (Finsupp.single i 1) + X i * p.divMonomial (Finsupp.single i 1) = p
hq : q.modMonomial (Finsupp.single i 1) + X i * q.divMonomial (Finsupp.single i 1) = q
⊢ X i ∣ p * q - p.modMonomial (Finsupp.single i 1) * q.modMonomial (Finsupp.single i 1)

Tactic:
· intro n
      contrapose
      intro hn
      classical
      rw [notMem_support_iff, coeff_mul]
      apply Finset.sum_eq_zero
      intro x hx
      simp only [Finset.mem_antidiagonal] at hx
      simp only [← hx, Finsupp.coe_add, Pi.add_apply, Nat.add_eq_zero_iff, not_and_or] at hn
      rcases hn with hn | hn
      · rw [coeff_modMonomial_of_le, zero_mul]
        simpa [← Nat.one_le_iff_ne_zero] using hn
      · rw [mul_comm, coeff_modMonomial_of_le, zero_mul]
        simpa [← Nat.one_le_iff_ne_zero] using hn

Goal state after:
case mp
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
i : σ
p q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
a✝ : Nontrivial R
h : X i ∣ p * q
hp : p.modMonomial (Finsupp.single i 1) + X i * p.divMonomial (Finsupp.single i 1) = p
hq : q.modMonomial (Finsupp.single i 1) + X i * q.divMonomial (Finsupp.single i 1) = q
⊢ X i ∣ p * q - p.modMonomial (Finsupp.single i 1) * q.modMonomial (Finsupp.single i 1)
Module: Mathlib.Algebra.MvPolynomial.Division

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
i : σ
p q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
⊢ p ∣ X i * q ↔ p ∣ q ∨ X i ∣ p ∧ p.divMonomial (Finsupp.single i 1) ∣ q

Tactic:
constructor

Goal state after:
case mp
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
i : σ
p q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
⊢ p ∣ X i * q → p ∣ q ∨ X i ∣ p ∧ p.divMonomial (Finsupp.single i 1) ∣ q

case mpr
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
i : σ
p q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
⊢ p ∣ q ∨ X i ∣ p ∧ p.divMonomial (Finsupp.single i 1) ∣ q → p ∣ X i * q
Module: Mathlib.Algebra.MvPolynomial.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : ℕ
f : R →+* S
g : σ → S
⊢ (eval₂Hom f g).comp ↑(expand p) = eval₂Hom f (g ^ p)

Tactic:
ext

Goal state after:
case hC
σ : Type u_1
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : ℕ
f : R →+* S
g : σ → S
x✝ : R
⊢ (((eval₂Hom f g).comp ↑(expand p)).comp C) x✝ = ((eval₂Hom f (g ^ p)).comp C) x✝

case hX
σ : Type u_1
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : ℕ
f : R →+* S
g : σ → S
i✝ : σ
⊢ ((eval₂Hom f g).comp ↑(expand p)) (X i✝) = (eval₂Hom f (g ^ p)) (X i✝)
Module: Mathlib.Algebra.MvPolynomial.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝² : CommSemiring R
p : ℕ
A : Type u_5
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
f : σ → A
⊢ (aeval f).comp (expand p) = aeval (f ^ p)

Tactic:
ext

Goal state after:
σ : Type u_1
R : Type u_3
inst✝² : CommSemiring R
p : ℕ
A : Type u_5
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
f : σ → A
i✝ : σ
⊢ ((aeval f).comp (expand p)) (X i✝) = (aeval (f ^ p)) (X i✝)
Module: Mathlib.Order.GameAdd

Goal state before:
pp: α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
x y : α × β
⊢ GameAdd rα rβ x y ↔ rα x.1 y.1 ∧ x.2 = y.2 ∨ rβ x.2 y.2 ∧ x.1 = y.1

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
x y : α × β
⊢ GameAdd rα rβ x y → rα x.1 y.1 ∧ x.2 = y.2 ∨ rβ x.2 y.2 ∧ x.1 = y.1

case mpr
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
x y : α × β
⊢ rα x.1 y.1 ∧ x.2 = y.2 ∨ rβ x.2 y.2 ∧ x.1 = y.1 → GameAdd rα rβ x y
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: case cons.e_a.e_a
m' : Multiset ℕ
x : ℕ
m : Multiset ℕ
hind : (m + m').multinomial = (m + m').sum.choose m.sum * m.multinomial * m'.multinomial
⊢ (x + (m.sum + m'.sum)).choose (x + (m.sum + m'.sum) - x) * (x + (m.sum + m'.sum) - x).choose (x + m.sum - x) =
    (x + (m.sum + m'.sum)).choose (m.sum + m'.sum) * (m.sum + m'.sum).choose m.sum

Tactic:
simp [add_tsub_cancel_left]

Goal state after:
Module: Mathlib.Data.DFinsupp.WellFounded

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → x j = if j ∈ p then x₁ j else x₂ j
hs : s i (x i) (if i ∈ p then x₁ i else x₂ i)
⊢ ∃ a',
    InvImage (GameAdd (DFinsupp.Lex r s) (DFinsupp.Lex r s)) snd a' (p, x₁, x₂) ∧
      (fun x ↦ x.2.1.piecewise x.2.2 x.1) a' = x

Tactic:
split_ifs at hs with hp

Goal state after:
case pos
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → x j = if j ∈ p then x₁ j else x₂ j
hp : i ∈ p
hs : s i (x i) (x₁ i)
⊢ ∃ a',
    InvImage (GameAdd (DFinsupp.Lex r s) (DFinsupp.Lex r s)) snd a' (p, x₁, x₂) ∧
      (fun x ↦ x.2.1.piecewise x.2.2 x.1) a' = x

case neg
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → x j = if j ∈ p then x₁ j else x₂ j
hp : i ∉ p
hs : s i (x i) (x₂ i)
⊢ ∃ a',
    InvImage (GameAdd (DFinsupp.Lex r s) (DFinsupp.Lex r s)) snd a' (p, x₁, x₂) ∧
      (fun x ↦ x.2.1.piecewise x.2.2 x.1) a' = x
Module: Mathlib.Data.Finsupp.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
a : m.syn
⊢ 0 ≤ a

Tactic:
by
    have := m.le_add_right 0 (m.toSyn.symm a)
    simpa [map_add, zero_add]

Goal state after:
Module: Mathlib.Data.DFinsupp.WellFounded

Goal state before:
pp: case insert
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬s i a 0
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (x : α i) → Decidable (x ≠ 0)
b : ι
t : Finset ι
hb : b ∉ t
ih :
  ∀ (x : Π₀ (i : ι), α i), x.support = t → (∀ i ∈ t, Acc (DFinsupp.Lex r s) (single i (x i))) → Acc (DFinsupp.Lex r s) x
⊢ ∀ (x : Π₀ (i : ι), α i),
    x.support = insert b t → (∀ i ∈ insert b t, Acc (DFinsupp.Lex r s) (single i (x i))) → Acc (DFinsupp.Lex r s) x

Tactic:
refine fun x ht h => Lex.acc_of_single_erase b (h b <| t.mem_insert_self b) ?_
      refine ih _ (by rw [support_erase, ht, Finset.erase_insert hb]) fun a ha => ?_
      rw [erase_ne (ha.ne_of_notMem hb)]
      exact h a (Finset.mem_insert_of_mem ha)

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : MvPolynomial σ R
a : R
ha : a ≠ 0
⊢ f ∣ C a ↔ ∃ b, b ∣ a ∧ f = C b

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : MvPolynomial σ R
a : R
ha : a ≠ 0
⊢ f ∣ C a → ∃ b, b ∣ a ∧ f = C b

case mpr
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : MvPolynomial σ R
a : R
ha : a ≠ 0
⊢ (∃ b, b ∣ a ∧ f = C b) → f ∣ C a
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
n : σ →₀ ℕ
a : R
ha : a ≠ 0
m : σ →₀ ℕ
⊢ (∃ r, m ≤ n ∧ r ∣ C a ∧ p = (monomial m) 1 * r) ↔ ∃ b, m ≤ n ∧ b ∣ a ∧ p = (monomial m) b

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
a : R
ha : a ≠ 0
m : σ →₀ ℕ
⊢ (∃ r, m ≤ n ∧ r ∣ C a ∧ p = (monomial m) 1 * r) → ∃ b, m ≤ n ∧ b ∣ a ∧ p = (monomial m) b

case mpr
R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
a : R
ha : a ≠ 0
m : σ →₀ ℕ
⊢ (∃ b, m ≤ n ∧ b ∣ a ∧ p = (monomial m) b) → ∃ r, m ≤ n ∧ r ∣ C a ∧ p = (monomial m) 1 * r
Module: Mathlib.Data.Fin.Tuple.Finset

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_1
S : (i : Fin (n + 1)) → Finset (α i)
P : ((i : Fin n) → α i.succ) → Prop
inst✝ : DecidablePred P
⊢ map (consEquiv α).symm.toEmbedding ({r ∈ piFinset S | P fun i ↦ r i.succ}) =
    S 0 ×ˢ {r ∈ piFinset fun i ↦ S i.succ | P r}

Tactic:
ext

Goal state after:
n : ℕ
α : Fin (n + 1) → Type u_1
S : (i : Fin (n + 1)) → Finset (α i)
P : ((i : Fin n) → α i.succ) → Prop
inst✝ : DecidablePred P
a✝ : α 0 × ((i : Fin n) → α i.succ)
⊢ a✝ ∈ map (consEquiv α).symm.toEmbedding ({r ∈ piFinset S | P fun i ↦ r i.succ}) ↔
    a✝ ∈ S 0 ×ˢ {r ∈ piFinset fun i ↦ S i.succ | P r}
Module: Mathlib.Data.Fin.Tuple.Finset

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_1
S : (i : Fin (n + 1)) → Finset (α i)
P : ((i : Fin n) → α i.castSucc) → Prop
inst✝ : DecidablePred P
⊢ map (snocEquiv α).symm.toEmbedding ({r ∈ piFinset S | P fun i ↦ r i.castSucc}) =
    S (last n) ×ˢ {r ∈ piFinset fun i ↦ S i.castSucc | P r}

Tactic:
ext

Goal state after:
n : ℕ
α : Fin (n + 1) → Type u_1
S : (i : Fin (n + 1)) → Finset (α i)
P : ((i : Fin n) → α i.castSucc) → Prop
inst✝ : DecidablePred P
a✝ : α (last n) × ((i : Fin n) → α i.castSucc)
⊢ a✝ ∈ map (snocEquiv α).symm.toEmbedding ({r ∈ piFinset S | P fun i ↦ r i.castSucc}) ↔
    a✝ ∈ S (last n) ×ˢ {r ∈ piFinset fun i ↦ S i.castSucc | P r}
Module: Mathlib.Data.Fin.Tuple.Finset

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_1
p : Fin (n + 1)
S : (i : Fin (n + 1)) → Finset (α i)
P : ((i : Fin n) → α (p.succAbove i)) → Prop
inst✝ : DecidablePred P
⊢ map (insertNthEquiv α p).symm.toEmbedding ({r ∈ piFinset S | P fun i ↦ r (p.succAbove i)}) =
    S p ×ˢ {r ∈ piFinset fun i ↦ S (p.succAbove i) | P r}

Tactic:
ext

Goal state after:
n : ℕ
α : Fin (n + 1) → Type u_1
p : Fin (n + 1)
S : (i : Fin (n + 1)) → Finset (α i)
P : ((i : Fin n) → α (p.succAbove i)) → Prop
inst✝ : DecidablePred P
a✝ : α p × ((i : Fin n) → α (p.succAbove i))
⊢ a✝ ∈ map (insertNthEquiv α p).symm.toEmbedding ({r ∈ piFinset S | P fun i ↦ r (p.succAbove i)}) ↔
    a✝ ∈ S p ×ˢ {r ∈ piFinset fun i ↦ S (p.succAbove i) | P r}
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 : σ
r : R
hr : r ≠ 0
b : R
⊢ (∃ a ≤ Finsupp.single i 1, b ∣ r ∧ p = (monomial a) b) ↔ b ∣ r ∧ (p = C b ∨ p = b • (monomial (Finsupp.single i 1)) 1)

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p : MvPolynomial σ R
i : σ
r : R
hr : r ≠ 0
b : R
⊢ (∃ a ≤ Finsupp.single i 1, b ∣ r ∧ p = (monomial a) b) → b ∣ r ∧ (p = C b ∨ p = b • (monomial (Finsupp.single i 1)) 1)

case mpr
R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p : MvPolynomial σ R
i : σ
r : R
hr : r ≠ 0
b : R
⊢ b ∣ r ∧ (p = C b ∨ p = b • (monomial (Finsupp.single i 1)) 1) → ∃ a ≤ Finsupp.single i 1, b ∣ r ∧ p = (monomial a) b
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

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

Tactic:
split_ifs with hc <;> simp

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 : MvPolynomial σ R
⊢ m.leadingCoeff f ≠ 0 ↔ f ≠ 0

Tactic:
constructor

Goal state after:
case mp
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
⊢ m.leadingCoeff f ≠ 0 → f ≠ 0

case mpr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
⊢ f ≠ 0 → m.leadingCoeff f ≠ 0
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case a
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ m.degree f ∈ (f + g).support

Tactic:
rw [mem_support_iff, coeff_add, m.coeff_eq_zero_of_lt h, add_zero,
      ← leadingCoeff, leadingCoeff_ne_zero_iff]

Goal state after:
case a
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ f ≠ 0
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n : ℕ
this : n.MinSqFacProp n.minSqFac
⊢ Squarefree n ↔ n.minSqFac = none

Tactic:
constructor

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: n : ℕ
h0 : n ≠ 0
a : ℕ
⊢ (a ∣ n ∧ n ≠ 0) ∧ Squarefree a ↔ ∃ a_1 ∈ (normalizedFactors n).toFinset.powerset, a_1.val.prod = a

Tactic:
constructor

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

case mpr
n : ℕ
h0 : n ≠ 0
a : ℕ
⊢ (∃ a_1 ∈ (normalizedFactors n).toFinset.powerset, a_1.val.prod = a) → (a ∣ n ∧ n ≠ 0) ∧ Squarefree a
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case h
a : ℕ
hsq : (normalizedFactors a).Nodup
b : ℕ
h0✝ : a * b ≠ 0
h0 : a ≠ 0 ∧ b ≠ 0
⊢ normalizedFactors a ⊆ normalizedFactors (a * b) ∧ Associated (normalizedFactors a).prod a

Tactic:
normalizedFactors_mul h0.1 h0.2

Goal state after:
case h
a : ℕ
hsq : (normalizedFactors a).Nodup
b : ℕ
h0✝ : a * b ≠ 0
h0 : a ≠ 0 ∧ b ≠ 0
⊢ normalizedFactors a ⊆ normalizedFactors a + normalizedFactors b ∧ Associated (normalizedFactors a).prod a
Module: Mathlib.Algebra.MvPolynomial.SchwartzZippel

Goal state before:

Tactic:
#{x₀ ∈ S 0 | eval (cons x₀ xₜ) p = 0} ≤ #pₓ.roots.toFinset := by
            gcongr
            simp +contextual [subset_iff, eval_eq_eval_mv_eval', pₓ, hpₓ₀, p']
          _ ≤ Multiset.card pₓ.roots := pₓ.roots.toFinset_card_le
          _ ≤ pₓ.natDegree := pₓ.card_roots'
          _ = k := hpₓdeg
          _ ≤ p.degreeOf 0 := by
            have :
              (ofLex (AddMonoidAlgebra.supDegree toLex p'.leadingCoeff)).cons k ∈ p.support := by
              rwa [← mem_support_coeff_finSuccEquiv, mem_support_iff, ← hp', hk,
                ← Polynomial.leadingCoeff, ← hpₖ, ← leadingCoeff_toLex,
                AddMonoidAlgebra.leadingCoeff_ne_zero toLex.injective]
            simpa using monomial_le_degreeOf 0 this

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

Goal state before:
pp: R : Type u_1
inst✝ : AddGroupWithOne R
f : ArithmeticFunction ℕ
⊢ ↑↑f = ↑f

Tactic:
ext

Goal state after:
R : Type u_1
inst✝ : AddGroupWithOne R
f : ArithmeticFunction ℕ
x✝ : ℕ
⊢ ↑↑f x✝ = ↑f x✝
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ { toFun := fun x ↦ if x = 1 then ↑0 else 0, map_zero' := ⋯ } = 0

Tactic:
ext

Goal state after:
R : Type u_1
inst✝ : AddMonoidWithOne R
x✝ : ℕ
⊢ { toFun := fun x ↦ if x = 1 then ↑0 else 0, map_zero' := ⋯ } x✝ = 0 x✝
Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
f g : ArithmeticFunction R
⊢ f.pmul g = g.pmul f

Tactic:
ext

Goal state after:
R : Type u_1
inst✝ : CommMonoidWithZero R
f g : ArithmeticFunction R
x✝ : ℕ
⊢ (f.pmul g) x✝ = (g.pmul f) x✝
Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta

Goal state before:
pp: R : Type u_1
inst✝ : SemigroupWithZero R
f₁ f₂ f₃ : ArithmeticFunction R
⊢ (f₁.pmul f₂).pmul f₃ = f₁.pmul (f₂.pmul f₃)

Tactic:
ext

Goal state after:
R : Type u_1
inst✝ : SemigroupWithZero R
f₁ f₂ f₃ : ArithmeticFunction R
x✝ : ℕ
⊢ ((f₁.pmul f₂).pmul f₃) x✝ = (f₁.pmul (f₂.pmul f₃)) x✝
Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
⊢ f.ppow 1 = f

Tactic:
ext

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x✝ : ℕ
⊢ (f.ppow 1) x✝ = f x✝
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
⊢ 0 * f = 0

Tactic:
ext

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x✝ : ℕ
⊢ (0 * f) x✝ = 0 x✝
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
⊢ f * 0 = 0

Tactic:
ext

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x✝ : ℕ
⊢ (f * 0) x✝ = 0 x✝
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
a b c : ArithmeticFunction R
⊢ a * (b + c) = a * b + a * c

Tactic:
ext

Goal state after:
R : Type u_1
inst✝ : Semiring R
a b c : ArithmeticFunction R
x✝ : ℕ
⊢ (a * (b + c)) x✝ = (a * b + a * c) x✝
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
a b c : ArithmeticFunction R
⊢ (a + b) * c = a * c + b * c

Tactic:
ext

Goal state after:
R : Type u_1
inst✝ : Semiring R
a b c : ArithmeticFunction R
x✝ : ℕ
⊢ ((a + b) * c) x✝ = (a * c + b * c) x✝
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
⊢ f * g = g * f

Tactic:
ext

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
f g : ArithmeticFunction R
x✝ : ℕ
⊢ (f * g) x✝ = (g * f) x✝
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
r : ArithmeticFunction R
⊢ r • 0 = 0

Tactic:
ext

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : ArithmeticFunction R
x✝ : ℕ
⊢ (r • 0) x✝ = 0 x✝
Module: Mathlib.Data.Nat.Factorization.PrimePow

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

Tactic:
constructor

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

case mpr
n p k : ℕ
⊢ 0 < k ∧ n.factorization = Finsupp.single p k → Nat.Prime p ∧ 0 < k ∧ p ^ k = n
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
r : ArithmeticFunction R
x y : ArithmeticFunction M
⊢ r • (x + y) = r • x + r • y

Tactic:
ext

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : ArithmeticFunction R
x y : ArithmeticFunction M
x✝ : ℕ
⊢ (r • (x + y)) x✝ = (r • x + r • y) x✝
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
r s : ArithmeticFunction R
x : ArithmeticFunction M
⊢ (r + s) • x = r • x + s • x

Tactic:
ext

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r s : ArithmeticFunction R
x : ArithmeticFunction M
x✝ : ℕ
⊢ ((r + s) • x) x✝ = (r • x + s • x) x✝
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
r : ArithmeticFunction M
⊢ 0 • r = 0

Tactic:
ext

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : ArithmeticFunction M
x✝ : ℕ
⊢ (0 • r) x✝ = 0 x✝