mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.BoxIntegral.Basic

Goal state before:
pp: ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
hl : l.bRiemann = false
B : ι →ᵇᵃ[↑I] ℝ
hB0 : ∀ (J : Box ι), 0 ≤ B J
g : ι →ᵇᵃ[↑I] F
s : Set (ι → ℝ)
hs : s.Countable
hlH : s.Nonempty → l.bHenstock = true
H₁ :
  ∀ (c : ℝ≥0),
    ∀ x ∈ Box.Icc I ∩ s,
      ∀ ε > 0,
        ∃ δ > 0,
          ∀ J ≤ I,
            Box.Icc J ⊆ Metric.closedBall x δ →
              x ∈ Box.Icc J → (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε
H₂ :
  ∀ (c : ℝ≥0),
    ∀ x ∈ Box.Icc I \ s,
      ∀ ε > 0,
        ∃ δ > 0,
          ∀ J ≤ I,
            Box.Icc J ⊆ Metric.closedBall x δ →
              (l.bHenstock = true → x ∈ Box.Icc J) →
                (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε * B J
ε : ℝ
⊢ 0 < ε →
    ∃ ia,
      (∀ (c : ℝ≥0), l.RCond (ia c)) ∧
        ∀ x ∈ {π | ∃ c, l.MemBaseSet I c (ia c) π ∧ π.IsPartition}, integralSum f vol x ∈ Metric.closedBall (g I) ε

Tactic:
ε0

Goal state after:
ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
hl : l.bRiemann = false
B : ι →ᵇᵃ[↑I] ℝ
hB0 : ∀ (J : Box ι), 0 ≤ B J
g : ι →ᵇᵃ[↑I] F
s : Set (ι → ℝ)
hs : s.Countable
hlH : s.Nonempty → l.bHenstock = true
H₁ :
  ∀ (c : ℝ≥0),
    ∀ x ∈ Box.Icc I ∩ s,
      ∀ ε > 0,
        ∃ δ > 0,
          ∀ J ≤ I,
            Box.Icc J ⊆ Metric.closedBall x δ →
              x ∈ Box.Icc J → (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε
H₂ :
  ∀ (c : ℝ≥0),
    ∀ x ∈ Box.Icc I \ s,
      ∀ ε > 0,
        ∃ δ > 0,
          ∀ J ≤ I,
            Box.Icc J ⊆ Metric.closedBall x δ →
              (l.bHenstock = true → x ∈ Box.Icc J) →
                (l.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε * B J
ε : ℝ
ε0 : 0 < ε
⊢ ∃ ia,
    (∀ (c : ℝ≥0), l.RCond (ia c)) ∧
      ∀ x ∈ {π | ∃ c, l.MemBaseSet I c (ia c) π ∧ π.IsPartition}, integralSum f vol x ∈ Metric.closedBall (g I) ε
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
hi : X i ∣ p
hq : p.divMonomial (Finsupp.single i 1) ∣ q
this : p = X i * p.divMonomial (Finsupp.single i 1)
⊢ p ∣ X i * q

Tactic:
this

Goal state after:
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
i : σ
p q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
hi : X i ∣ p
hq : p.divMonomial (Finsupp.single i 1) ∣ q
this : p = X i * p.divMonomial (Finsupp.single i 1)
⊢ X i * p.divMonomial (Finsupp.single i 1) ∣ X i * q
Module: Mathlib.Algebra.MvPolynomial.Nilpotent

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
P : MvPolynomial σ R
inst✝ : IsReduced R
⊢ IsUnit P ↔ IsUnit (coeff 0 P) ∧ P.totalDegree = 0

Tactic:
convert! isUnit_iff (P := P)

Goal state after:
σ : Type u_1
R : Type u_2
inst✝¹ : CommRing R
P : MvPolynomial σ R
inst✝ : IsReduced R
⊢ P.totalDegree = 0 ↔ ∀ (i : σ →₀ ℕ), i ≠ 0 → IsNilpotent (coeff i P)
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: case insert
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
x : α → R
a : α
s : Finset α
ha : a ∉ s
hc : (↑(insert a s)).Pairwise (Commute on x)
ih : ∀ (n : ℕ), s.sum x ^ n = ∑ k, ↑(↑↑k).countPerms * (Multiset.map x ↑↑k).noncommProd ⋯
n : ℕ
⊢ ∑ i, x a ^ ↑i * (∑ i ∈ s, x i) ^ (n - ↑i) * ↑(n.choose ↑i) =
    ∑ k, ↑(↑↑k).countPerms * (Multiset.map x ↑↑k).noncommProd ⋯

Tactic:
[

Goal state after:
case insert
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
x : α → R
a : α
s : Finset α
ha : a ∉ s
hc : (↑(insert a s)).Pairwise (Commute on x)
ih : ∀ (n : ℕ), s.sum x ^ n = ∑ k, ↑(↑↑k).countPerms * (Multiset.map x ↑↑k).noncommProd ⋯
n : ℕ
⊢ ∑ i, x a ^ ↑i * (∑ i ∈ s, x i) ^ (n - ↑i) * ↑(n.choose ↑i) =
    ∑ k, ↑(↑↑k).countPerms * (Multiset.map x ↑↑k).noncommProd ⋯
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: case insert
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
x : α → R
a : α
s : Finset α
ha : a ∉ s
hc : (↑(insert a s)).Pairwise (Commute on x)
ih : ∀ (n : ℕ), s.sum x ^ n = ∑ k, ↑(↑↑k).countPerms * (Multiset.map x ↑↑k).noncommProd ⋯
n : ℕ
⊢ ∑ x_1, (∑ i, x a ^ ↑x_1 * (↑(↑↑i).countPerms * (Multiset.map x ↑↑i).noncommProd ⋯)) * ↑(n.choose ↑x_1) =
    ∑ k, ↑(↑↑k).countPerms * (Multiset.map x ↑↑k).noncommProd ⋯

Tactic:
sum_mul,

Goal state after:
case insert
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
x : α → R
a : α
s : Finset α
ha : a ∉ s
hc : (↑(insert a s)).Pairwise (Commute on x)
ih : ∀ (n : ℕ), s.sum x ^ n = ∑ k, ↑(↑↑k).countPerms * (Multiset.map x ↑↑k).noncommProd ⋯
n : ℕ
⊢ ∑ x_1, ∑ i, x a ^ ↑x_1 * (↑(↑↑i).countPerms * (Multiset.map x ↑↑i).noncommProd ⋯) * ↑(n.choose ↑x_1) =
    ∑ k, ↑(↑↑k).countPerms * (Multiset.map x ↑↑k).noncommProd ⋯
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: case insert
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
x : α → R
a : α
s : Finset α
ha : a ∉ s
hc : (↑(insert a s)).Pairwise (Commute on x)
ih : ∀ (n : ℕ), s.sum x ^ n = ∑ k, ↑(↑↑k).countPerms * (Multiset.map x ↑↑k).noncommProd ⋯
n : ℕ
m : ↥((insert a s).sym n)
⊢ ↑((↑↑m).card.choose (Multiset.count a ↑↑m) * (Multiset.filter (fun x ↦ a ≠ x) ↑↑m).countPerms) *
      (Multiset.map x (Multiset.filter (fun x ↦ a = x) ↑↑m) +
            Multiset.map x (Multiset.filter (fun a_1 ↦ ¬a = a_1) ↑↑m)).noncommProd
        ⋯ =
    x a ^ ↑((symInsertEquiv ha) m).fst *
        (↑(↑↑((symInsertEquiv ha) m).snd).countPerms * (Multiset.map x ↑↑((symInsertEquiv ha) m).snd).noncommProd ⋯) *
      ↑(n.choose ↑((symInsertEquiv ha) m).fst)

Tactic:
[

Goal state after:
case insert
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
x : α → R
a : α
s : Finset α
ha : a ∉ s
hc : (↑(insert a s)).Pairwise (Commute on x)
ih : ∀ (n : ℕ), s.sum x ^ n = ∑ k, ↑(↑↑k).countPerms * (Multiset.map x ↑↑k).noncommProd ⋯
n : ℕ
m : ↥((insert a s).sym n)
⊢ ↑((↑↑m).card.choose (Multiset.count a ↑↑m) * (Multiset.filter (fun x ↦ a ≠ x) ↑↑m).countPerms) *
      (Multiset.map x (Multiset.filter (fun x ↦ a = x) ↑↑m) +
            Multiset.map x (Multiset.filter (fun a_1 ↦ ¬a = a_1) ↑↑m)).noncommProd
        ⋯ =
    x a ^ ↑((symInsertEquiv ha) m).fst *
        (↑(↑↑((symInsertEquiv ha) m).snd).countPerms * (Multiset.map x ↑↑((symInsertEquiv ha) m).snd).noncommProd ⋯) *
      ↑(n.choose ↑((symInsertEquiv ha) m).fst)
Module: Mathlib.Algebra.MvPolynomial.Expand

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
p : ℕ
f : MvPolynomial σ R
hp : p > 0
hf : ¬f = 0
⊢ ((expand p) f).totalDegree = f.totalDegree * p

Tactic:
[

Goal state after:
case neg
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
p : ℕ
f : MvPolynomial σ R
hp : p > 0
hf : ¬f = 0
⊢ ((expand p) f).totalDegree = f.totalDegree * p
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: case insert.e_a
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
x : α → R
a : α
s : Finset α
ha : a ∉ s
hc : (↑(insert a s)).Pairwise (Commute on x)
ih : ∀ (n : ℕ), s.sum x ^ n = ∑ k, ↑(↑↑k).countPerms * (Multiset.map x ↑↑k).noncommProd ⋯
n : ℕ
m : ↥((insert a s).sym n)
⊢ ↑(Multiset.filter (fun x ↦ a ≠ x) ↑↑m).countPerms *
      (x a ^ Multiset.count a ↑↑m * (Multiset.map x (Multiset.filter (fun a_1 ↦ ¬a = a_1) ↑↑m)).noncommProd ⋯) =
    x a ^ ↑((symInsertEquiv ha) m).fst *
      (↑(↑↑((symInsertEquiv ha) m).snd).countPerms * (Multiset.map x ↑↑((symInsertEquiv ha) m).snd).noncommProd ⋯)

Tactic:
[

Goal state after:
case insert.e_a
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
x : α → R
a : α
s : Finset α
ha : a ∉ s
hc : (↑(insert a s)).Pairwise (Commute on x)
ih : ∀ (n : ℕ), s.sum x ^ n = ∑ k, ↑(↑↑k).countPerms * (Multiset.map x ↑↑k).noncommProd ⋯
n : ℕ
m : ↥((insert a s).sym n)
⊢ ↑(Multiset.filter (fun x ↦ a ≠ x) ↑↑m).countPerms *
      (x a ^ Multiset.count a ↑↑m * (Multiset.map x (Multiset.filter (fun a_1 ↦ ¬a = a_1) ↑↑m)).noncommProd ⋯) =
    x a ^ ↑((symInsertEquiv ha) m).fst *
      (↑(↑↑((symInsertEquiv ha) m).snd).countPerms * (Multiset.map x ↑↑((symInsertEquiv ha) m).snd).noncommProd ⋯)
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring R
s : Finset α
f : α → R
n : ℕ
⊢ (∑ i ∈ s, f i) ^ n = ∑ k ∈ s.piAntidiag n, ↑(multinomial s k) * ∏ i ∈ s, f i ^ k i

Tactic:
[

Goal state after:
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring R
s : Finset α
f : α → R
n : ℕ
⊢ (∑ i ∈ s, f i) ^ n = ∑ k ∈ s.piAntidiag n, ↑(multinomial s k) * ∏ i ∈ s, f i ^ k i
Module: Mathlib.Algebra.MvPolynomial.Funext

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
σ : Type u_2
p q : MvPolynomial σ R
s : σ → Set R
hs : ∀ (i : σ), (s i).Infinite
h : ∀ x ∈ Set.univ.pi s, (eval x) p = (eval x) q
this : ∀ (p : MvPolynomial σ R), (∀ x ∈ Set.univ.pi s, (eval x) p = 0) → p = 0
x : σ → R
hx : x ∈ Set.univ.pi s
⊢ (eval x) (p - q) = 0

Tactic:
[

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
σ : Type u_2
p q : MvPolynomial σ R
s : σ → Set R
hs : ∀ (i : σ), (s i).Infinite
h : ∀ x ∈ Set.univ.pi s, (eval x) p = (eval x) q
this : ∀ (p : MvPolynomial σ R), (∀ x ∈ Set.univ.pi s, (eval x) p = 0) → p = 0
x : σ → R
hx : x ∈ Set.univ.pi s
⊢ (eval x) (p - q) = 0
Module: Mathlib.Algebra.MvPolynomial.Funext

Goal state before:
pp: case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
σ : Type u_2
p✝ q : MvPolynomial σ R
s : σ → Set R
hs : ∀ (i : σ), (s i).Infinite
h✝ : ∀ x ∈ Set.univ.pi s, (eval x) p✝ = (eval x) q
n : ℕ
f : Fin n → σ
hf : Function.Injective f
p : MvPolynomial (Fin n) R
h : ∀ x ∈ Set.univ.pi s, (eval x) ((rename f) p) = 0
x : Fin n → R
hx : x ∈ Set.univ.pi (s ∘ f)
g : σ → R
hg : ∀ (i : σ), g i ∈ s i
i : σ
x✝ : i ∈ Set.univ
nex : ¬∃ x, f x = i
⊢ Function.extend f x g i ∈ s i

Tactic:
[

Goal state after:
case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
σ : Type u_2
p✝ q : MvPolynomial σ R
s : σ → Set R
hs : ∀ (i : σ), (s i).Infinite
h✝ : ∀ x ∈ Set.univ.pi s, (eval x) p✝ = (eval x) q
n : ℕ
f : Fin n → σ
hf : Function.Injective f
p : MvPolynomial (Fin n) R
h : ∀ x ∈ Set.univ.pi s, (eval x) ((rename f) p) = 0
x : Fin n → R
hx : x ∈ Set.univ.pi (s ∘ f)
g : σ → R
hg : ∀ (i : σ), g i ∈ s i
i : σ
x✝ : i ∈ Set.univ
nex : ¬∃ x, f x = i
⊢ Function.extend f x g i ∈ s i
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 = (x₁.piecewise x₂ p) j
hs : s i (x i) ((x₁.piecewise x₂ p) 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:
[

Goal state after:
ι : 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 = (x₁.piecewise x₂ p) j
hs : s i (x i) ((x₁.piecewise x₂ p) 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.DFinsupp.WellFounded

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), WellFoundedLT (α i)
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬a < 0
β : ι → Type u_2 := fun i ↦ Antisymmetrization (α i) fun x1 x2 ↦ x1 ≤ x2
e : (i : ι) → α i → β i := fun i ↦ toAntisymmetrization fun x1 x2 ↦ x1 ≤ x2
x✝¹ : (i : ι) → Zero (β i) := fun i ↦ { zero := e i 0 }
this : WellFounded (DFinsupp.Lex (Function.swap WellOrderingRel) fun x x1 x2 ↦ x1 < x2)
x✝ y✝ : Π₀ (i : ι), α i
h : x✝ < y✝
⊢ InvImage (DFinsupp.Lex (Function.swap WellOrderingRel) fun x x1 x2 ↦ x1 < x2) (mapRange e ⋯) x✝ y✝

Tactic:
obtain ⟨i, he, hl⟩ := lex_lt_of_lt_of_preorder (Function.swap WellOrderingRel) h

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : (i : ι) → Preorder (α i)
inst✝ : ∀ (i : ι), WellFoundedLT (α i)
hbot : ∀ ⦃i : ι⦄ ⦃a : α i⦄, ¬a < 0
β : ι → Type u_2 := fun i ↦ Antisymmetrization (α i) fun x1 x2 ↦ x1 ≤ x2
e : (i : ι) → α i → β i := fun i ↦ toAntisymmetrization fun x1 x2 ↦ x1 ≤ x2
x✝¹ : (i : ι) → Zero (β i) := fun i ↦ { zero := e i 0 }
this : WellFounded (DFinsupp.Lex (Function.swap WellOrderingRel) fun x x1 x2 ↦ x1 < x2)
x✝ y✝ : Π₀ (i : ι), α i
h : x✝ < y✝
i : ι
he : ∀ (j : ι), Function.swap WellOrderingRel j i → x✝ j ≤ y✝ j ∧ y✝ j ≤ x✝ j
hl : x✝ i < y✝ i
⊢ InvImage (DFinsupp.Lex (Function.swap WellOrderingRel) fun x x1 x2 ↦ x1 < x2) (mapRange e ⋯) x✝ y✝
Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors

Goal state before:
pp: R : Type u_1
σ : Type u_2
n : σ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : NoZeroDivisors R
hp : p ≠ 0
hq : q ≠ 0
⊢ degreeOf n (p * q) = degreeOf n p + degreeOf n q

Tactic:
[

Goal state after:
R : Type u_1
σ : Type u_2
n : σ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : NoZeroDivisors R
hp : p ≠ 0
hq : q ≠ 0
⊢ degreeOf n (p * q) = degreeOf n p + degreeOf n q
Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : NoZeroDivisors R
hp : p ≠ 0
hq : q ≠ 0
s : σ
⊢ Multiset.count s (p * q).degrees = Multiset.count s (p.degrees + q.degrees)

Tactic:
[

Goal state after:
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : NoZeroDivisors R
hp : p ≠ 0
hq : q ≠ 0
s : σ
⊢ Multiset.count s (p * q).degrees = Multiset.count s (p.degrees + q.degrees)
Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors

Goal state before:
pp: case neg
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
j : σ
c : R
hc : c ∈ R⁰
hp : ¬p = 0
⊢ degreeOf j (C c * p) = degreeOf j p

Tactic:
[

Goal state after:
case neg
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
j : σ
c : R
hc : c ∈ R⁰
hp : ¬p = 0
⊢ degreeOf j (C c * p) = degreeOf j p
Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors

Goal state before:
pp: case neg
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
j : σ
c : R
hc : c ∈ R⁰
hp : ¬p = 0
hp' : ((optionEquivLeft R { b // b ≠ j }) ((rename ⇑(optionSubtypeNe j).symm) p)).leadingCoeff ≠ 0
⊢ ((optionEquivLeft R { b // b ≠ j }) ((renameEquiv R (optionSubtypeNe j).symm) (C c))).leadingCoeff *
      ((optionEquivLeft R { b // b ≠ j }) ((renameEquiv R (optionSubtypeNe j).symm) p)).leadingCoeff ≠
    0

Tactic:
[

Goal state after:
case neg
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
j : σ
c : R
hc : c ∈ R⁰
hp : ¬p = 0
hp' : ((optionEquivLeft R { b // b ≠ j }) ((rename ⇑(optionSubtypeNe j).symm) p)).leadingCoeff ≠ 0
⊢ ((optionEquivLeft R { b // b ≠ j }) ((renameEquiv R (optionSubtypeNe j).symm) (C c))).leadingCoeff *
      ((optionEquivLeft R { b // b ≠ j }) ((renameEquiv R (optionSubtypeNe j).symm) p)).leadingCoeff ≠
    0
Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
⊢ StrictAnti fun a ↦ toDegLex (single a 1)

Tactic:
by
  intro _ _ h
  simp only [lt_iff, ofDegLex_toDegLex, degree_single, lt_self_iff_false, Lex.single_lt_iff, h,
    and_self, or_true]

Goal state after:
Module: Mathlib.Data.Fin.Tuple.Finset

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_1
x_zero : α 0
x_tail : (i : Fin n) → α i.succ
s_zero : Finset (α 0)
s_tail : (i : Fin n) → Finset (α i.succ)
⊢ cons x_zero x_tail ∈ piFinset (cons s_zero s_tail) ↔ x_zero ∈ s_zero ∧ x_tail ∈ piFinset s_tail

Tactic:
[

Goal state after:
n : ℕ
α : Fin (n + 1) → Type u_1
x_zero : α 0
x_tail : (i : Fin n) → α i.succ
s_zero : Finset (α 0)
s_tail : (i : Fin n) → Finset (α i.succ)
⊢ cons x_zero x_tail ∈ piFinset (cons s_zero s_tail) ↔ x_zero ∈ s_zero ∧ x_tail ∈ piFinset s_tail
Module: Mathlib.Data.Fin.Tuple.Finset

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_1
x_last : α (last n)
x_init : (i : Fin n) → α i.castSucc
s_last : Finset (α (last n))
s_init : (i : Fin n) → Finset (α i.castSucc)
⊢ snoc x_init x_last ∈ piFinset (snoc s_init s_last) ↔ x_last ∈ s_last ∧ x_init ∈ piFinset s_init

Tactic:
[

Goal state after:
n : ℕ
α : Fin (n + 1) → Type u_1
x_last : α (last n)
x_init : (i : Fin n) → α i.castSucc
s_last : Finset (α (last n))
s_init : (i : Fin n) → Finset (α i.castSucc)
⊢ snoc x_init x_last ∈ piFinset (snoc s_init s_last) ↔ x_last ∈ s_last ∧ x_init ∈ piFinset s_init
Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors

Goal state before:
pp: case inr
R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
hR : Nontrivial R
m : σ →₀ ℕ
⊢ (∃ b, m ≤ n ∧ b ∣ 1 ∧ p = (monomial m) b) ↔ ∃ u, m ≤ n ∧ IsUnit u ∧ p = (monomial m) u

Tactic:
[

Goal state after:
case inr
R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
hR : Nontrivial R
m : σ →₀ ℕ
⊢ (∃ b, m ≤ n ∧ b ∣ 1 ∧ p = (monomial m) b) ↔ ∃ u, m ≤ n ∧ IsUnit u ∧ p = (monomial m) u
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
f : MvPolynomial σ R
hf : m.Monic f
⊢ f ≠ 0

Tactic:
rintro rfl
  simp [Monic, leadingCoeff_zero] at hf

Goal state after:
Module: Mathlib.Data.Sym.Card

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ 2 * #(image (uncurry Sym2.mk) s.offDiag) = #s.offDiag

Tactic:
by
  rw [card_eq_sum_card_image (Sym2.mk.uncurry : α × α → _), sum_const_nat (Sym2.ind _), mul_comm]
  -- FIXME: Would be cool for the final `aesop` call not to require this `a ≠ b ∨ b ≠ a` trick.
  have (a b : α) (ha : a ∈ s) (hb : b ∈ s) (hab : a ≠ b ∨ b ≠ a) :
      {z ∈ s.offDiag | Sym2.mk.uncurry z = s(a, b)} = .cons (a, b) {(b, a)}
        (by simpa [eq_comm] using hab) := by aesop
  aesop

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
hf : m.Monic f
hg : m.Monic g
a✝ : Nontrivial R
this : m.leadingCoeff f * m.leadingCoeff g = 1
⊢ m.leadingCoeff f * m.leadingCoeff g = 1

pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hf : m.Monic f
hg : m.Monic g
a✝ : Nontrivial R
this : m.leadingCoeff f * m.leadingCoeff g = 1
⊢ m.leadingCoeff f * m.leadingCoeff g ≠ 0

Tactic:
this

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hf : m.Monic f
hg : m.Monic g
a✝ : Nontrivial R
this : m.leadingCoeff f * m.leadingCoeff g = 1
⊢ 1 = 1

σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hf : m.Monic f
hg : m.Monic g
a✝ : Nontrivial R
this : m.leadingCoeff f * m.leadingCoeff g = 1
⊢ m.leadingCoeff f * m.leadingCoeff g ≠ 0
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
hf : m.Monic f
hg : m.Monic g
a✝ : Nontrivial R
this : m.leadingCoeff f * m.leadingCoeff g = 1
⊢ m.leadingCoeff f * m.leadingCoeff g ≠ 0

Tactic:
this

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hf : m.Monic f
hg : m.Monic g
a✝ : Nontrivial R
this : m.leadingCoeff f * m.leadingCoeff g = 1
⊢ 1 ≠ 0
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsReduced R
f : MvPolynomial σ R
n : ℕ
hf : f = 0
hn : ¬n = 0
⊢ m.degree (0 ^ n) = 0

Tactic:
rw [zero_pow hn, degree_zero]

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

Goal state before:
pp: case empty
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
⊢ m.toSyn (m.degree (C 1)) ≤ m.toSyn 0

Tactic:
m.degree_C,

Goal state after:
case empty
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
⊢ m.toSyn 0 ≤ m.toSyn 0
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 ∧ (eval (tail x)) pₖ ≠ 0}) =
    #({x ∈ piFinset fun i ↦ S i | (eval (tail x)) pₖ ≠ 0 ∧ (eval x) p = 0})

Tactic:
[

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 ∧ (eval (tail x)) pₖ ≠ 0}) =
    #({x ∈ piFinset fun i ↦ S i | (eval (tail x)) pₖ ≠ 0 ∧ (eval x) p = 0})
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: p k : ℕ
hp : Prime p
hk : 0 < k
h : Squarefree p ∧ k = 1
⊢ Prime (p ^ k)

Tactic:
h.2,

Goal state after:
p k : ℕ
hp : Prime p
hk : 0 < k
h : Squarefree p ∧ k = 1
⊢ Prime (p ^ 1)
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : p.support ⊆ q.support
⊢ m.toSyn (m.degree p) ≤ m.toSyn (m.degree q)

Tactic:
[

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : p.support ⊆ q.support
⊢ m.toSyn (m.degree p) ≤ m.toSyn (m.degree q)
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case mpr
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s ⊆ (normalizedFactors n).toFinset
⊢ (s.val.prod ∣ n ∧ n ≠ 0) ∧ Squarefree s.val.prod

Tactic:
← Finset.val_le_iff,

Goal state after:
case mpr
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ (normalizedFactors n).toFinset.val
⊢ (s.val.prod ∣ n ∧ n ≠ 0) ∧ Squarefree s.val.prod
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

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 neg.inl
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : f = 0
⊢ m.withBotDegree f = m.withBotDegree g ↔ m.degree f = m.degree g ∧ (f = 0 ↔ g = 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.withBotDegree f = m.withBotDegree g ↔ m.degree f = m.degree g ∧ (f = 0 ↔ g = 0)