mathlib-initiative/mathlib-tactics huggingface dataset:
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
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}

Tactic:
;

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:
;

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

Tactic:
;

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:
;

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

Tactic:
;

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.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 ι
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
B : ι →ᵇᵃ[↑I] ℝ
hB0 : ∀ (J : Box ι), 0 ≤ B J
g : ι →ᵇᵃ[↑I] F
H :
  ∀ (x : ℝ≥0),
    ∀ x ∈ Box.Icc I, ∀ ε > 0, ∃ δ > 0, ∀ J ≤ I, Box.Icc J ⊆ Metric.closedBall x δ → dist ((vol J) (f x)) (g J) ≤ ε * B J
⊢ ∀ (c : ℝ≥0),
    ∀ x ∈ Box.Icc I \ ∅,
      ∀ ε > 0,
        ∃ δ > 0,
          ∀ J ≤ I,
            Box.Icc J ⊆ Metric.closedBall x δ →
              (McShane.bHenstock = true → x ∈ Box.Icc J) →
                (McShane.bDistortion = true → J.distortion ≤ c) → dist ((vol J) (f x)) (g J) ≤ ε * B J

Tactic:
by
    simpa only [McShane, Bool.coe_sort_false, false_imp_iff, true_imp_iff, sdiff_empty] using H

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

Goal state before:
pp: case neg
R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
i : σ
r : R
hr : r ≠ 0
b : R
m : σ →₀ ℕ
hmn : m ≤ Finsupp.single i 1
hb : b ∣ r
hm : ¬m i = 0
j : σ
hj : ¬j = i
⊢ (Finsupp.single i 1) j ≤ m j

Tactic:
· simp [Finsupp.single_eq_of_ne hj]

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

Goal state before:
pp: case h
R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p : MvPolynomial σ R
i : σ
r : R
hr : r ≠ 0
b : R
hb : b ∣ r
hp : p = C b
⊢ 0 ≤ Finsupp.single i 1 ∧ b ∣ r ∧ p = (monomial 0) b

Tactic:
;

Goal state after:
case h
R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p : MvPolynomial σ R
i : σ
r : R
hr : r ≠ 0
b : R
hb : b ∣ r
hp : p = C b
⊢ 0 ≤ Finsupp.single i 1 ∧ b ∣ r ∧ p = (monomial 0) b
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
⊢ ∀ (a : R), a ∣ 1 ∧ (p = C a ∨ p = a • X i) ↔ IsUnit a ∧ (p = C a ∨ p = a • 1 • X i)

Tactic:
intro r

Goal state after:
R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p : MvPolynomial σ R
i : σ
a✝ : Nontrivial R
r : R
⊢ r ∣ 1 ∧ (p = C r ∨ p = r • X i) ↔ 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
f g : MvPolynomial σ R
b : σ →₀ ℕ
hb : b ∈ (f + g).support
hf : b ∈ f.support
⊢ m.toSyn b ≤ m.toSyn (m.degree f) ∨ m.toSyn b ≤ m.toSyn (m.degree g)

pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
b : σ →₀ ℕ
hb : b ∈ (f + g).support
hf : b ∉ f.support
⊢ m.toSyn b ≤ m.toSyn (m.degree f) ∨ m.toSyn b ≤ m.toSyn (m.degree g)

Tactic:
· left
    exact m.le_degree hf

Goal state after:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
b : σ →₀ ℕ
hb : b ∈ (f + g).support
hf : b ∉ f.support
⊢ m.toSyn b ≤ m.toSyn (m.degree f) ∨ m.toSyn b ≤ m.toSyn (m.degree g)
Module: Mathlib.Data.Sym.Card

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

Tactic:
;

Goal state after:
k : ℕ
⊢ Fintype.card (Sym (Fin 0) (k + 1)) = 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
⊢ m.leadingCoeff f * m.leadingCoeff g = 1

Tactic:
rw [hf.leadingCoeff_eq_one, hg.leadingCoeff_eq_one, one_mul]

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

Goal state before:
pp: case h
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 : Fin (n + 1) → R
a✝ : x ∈ piFinset fun i ↦ S i
⊢ (eval x) p = 0 ∧ (eval (tail x)) pₖ = 0 → (eval (tail x)) pₖ = 0

Tactic:
;

Goal state after:
case h
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 : Fin (n + 1) → R
a✝ : x ∈ piFinset fun i ↦ S i
⊢ (eval x) p = 0 ∧ (eval (tail x)) pₖ = 0 → (eval (tail x)) pₖ = 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
⊢ ↑(degreeOf 0 p * ∏ i, #(S i.succ)) / ↑(∏ i, #(S i)) =
    ↑(degreeOf 0 p * ∏ i, #(S i.succ)) / ↑(#(S 0) * ∏ i, #(S i.succ))

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
⊢ ↑(degreeOf 0 p * ∏ i, #(S i.succ)) / ↑(∏ i, #(S i)) =
    ↑(degreeOf 0 p * ∏ i, #(S i.succ)) / ↑(#(S 0) * ∏ i, #(S i.succ))
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n : ℕ
hn hm : Squarefree n
⊢ ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ n)

Tactic:
;

Goal state after:
n : ℕ
hn hm : Squarefree n
⊢ ∀ (p : ℕ), Prime p → (p ∣ n ↔ p ∣ n)
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p p' q : MvPolynomial σ R
hp : p ≠ 0
hq : q ≠ 0
h : p' = 0
⊢ m.toSyn (m.degree p') ≤ m.toSyn (m.degree p)

Tactic:
;

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p p' q : MvPolynomial σ R
hp : p ≠ 0
hq : q ≠ 0
h : p' = 0
⊢ m.toSyn (m.degree p') ≤ m.toSyn (m.degree p)
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n : ℕ
hn✝ : n ≠ 1
hn : Squarefree n
hk : 1 ≠ 0
⊢ Squarefree (n ^ 1)

Tactic:
;

Goal state after:
n : ℕ
hn✝ : n ≠ 1
hn : Squarefree n
hk : 1 ≠ 0
⊢ Squarefree (n ^ 1)
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case h
s : Finset ℕ
m n✝ p n k : ℕ
h : ¬n < k * k
this : n.sqrt - k < n.sqrt + 2 - k
n' : ℕ := ⋯
⊢ n' ≤ n

Tactic:
;

Goal state after:
case h
s : Finset ℕ
m n✝ p n k : ℕ
h : ¬n < k * k
this : n.sqrt - k < n.sqrt + 2 - k
n' : ℕ := ⋯
⊢ n' ≤ n
Module: Mathlib.Algebra.MvPolynomial.SchwartzZippel

Goal state before:
pp: case h
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ₜ : Fin n → R
a✝ : xₜ ∈ {xₜ ∈ piFinset fun i ↦ tail S i | (eval xₜ) pₖ ≠ 0}
⊢ #(image (fun x₀ ↦ (x₀, xₜ)) ({x₀ ∈ S 0 | (eval (Fin.cons x₀ xₜ)) p = 0})) ≤
    #({x₀ ∈ S 0 | (eval (Fin.cons x₀ xₜ)) p = 0})

Tactic:
;

Goal state after:
case h
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ₜ : Fin n → R
a✝ : xₜ ∈ {xₜ ∈ piFinset fun i ↦ tail S i | (eval xₜ) pₖ ≠ 0}
⊢ #(image (fun x₀ ↦ (x₀, xₜ)) ({x₀ ∈ S 0 | (eval (Fin.cons x₀ xₜ)) p = 0})) ≤
    #({x₀ ∈ S 0 | (eval (Fin.cons x₀ xₜ)) p = 0})
Module: Mathlib.Algebra.MvPolynomial.SchwartzZippel

Goal state before:
pp: case h
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) := ⋯
hp' : p' = (finSuccEquiv R n) p
k : ℕ := ⋯
hk : k = p'.natDegree
pₖ : MvPolynomial (Fin n) R := ⋯
hpₖ : pₖ = p'.leadingCoeff
hp'₀ : p' ≠ 0
hpₖ₀ : pₖ ≠ 0
⊢ {xₜ ∈ piFinset fun i ↦ tail S i | (eval xₜ) pₖ ≠ 0} ⊆ piFinset fun i ↦ tail S i

Tactic:
;

Goal state after:
case h
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) := ⋯
hp' : p' = (finSuccEquiv R n) p
k : ℕ := ⋯
hk : k = p'.natDegree
pₖ : MvPolynomial (Fin n) R := ⋯
hpₖ : pₖ = p'.leadingCoeff
hp'₀ : p' ≠ 0
hpₖ₀ : pₖ ≠ 0
⊢ {xₜ ∈ piFinset fun i ↦ tail S i | (eval xₜ) pₖ ≠ 0} ⊆ piFinset fun i ↦ tail S i
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n : ℕ
⊢ n.MinSqFacProp (if 2 ∣ n then if 2 ∣ n / 2 then some 2 else (n / 2).minSqFacAux 3 else n.minSqFacAux 3)

Tactic:
;

Goal state after:
n : ℕ
⊢ n.MinSqFacProp (if 2 ∣ n then if 2 ∣ n / 2 then some 2 else (n / 2).minSqFacAux 3 else n.minSqFacAux 3)
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n d : ℕ
h : n.minSqFac = some d
m : ℕ
m2 : 2 ≤ m
md : m * m ∣ n
this : n.MinSqFacProp n.minSqFac
⊢ d ≤ m

Tactic:
;

Goal state after:
n d : ℕ
h : n.minSqFac = some d
m : ℕ
m2 : 2 ≤ m
md : m * m ∣ n
this : n.MinSqFacProp n.minSqFac
⊢ d ≤ m
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n d : ℕ
h : n.minSqFac = some d
m : ℕ
m2 : 2 ≤ m
md : m * m ∣ n
⊢ d ≤ m

Tactic:
by
  have := minSqFac_has_prop n; rw [h] at this
  have fd := minFac_dvd m
  exact
    le_trans (this.2.2 _ (minFac_prime <| ne_of_gt m2) (dvd_trans (mul_dvd_mul fd fd) md))
      (minFac_le <| lt_of_lt_of_le (by decide) m2)

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

Goal state before:
pp: case h
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ₜ : Fin n → R
hxₜ : xₜ ∈ {xₜ ∈ piFinset fun i ↦ tail S i | (eval xₜ) pₖ ≠ 0}
pₓ : Polynomial R := Polynomial.map (eval xₜ) p'
hpₓ : pₓ = Polynomial.map (eval xₜ) p'
hpₓdeg : pₓ.natDegree = k
⊢ #({x₀ ∈ S 0 | (eval (Fin.cons x₀ xₜ)) p = 0}) ≤ degreeOf 0 p

Tactic:
have hpₓ₀ : pₓ ≠ 0 := fun h ↦ (mem_filter.1 hxₜ).2 <| by
          rw [hpₖ, Polynomial.leadingCoeff, ← hk, ← hpₓdeg, h, Polynomial.natDegree_zero,
            ← Polynomial.coeff_map, ← hpₓ, h, Polynomial.coeff_zero]

Goal state after:
case h
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ₜ : Fin n → R
hxₜ : xₜ ∈ {xₜ ∈ piFinset fun i ↦ tail S i | (eval xₜ) pₖ ≠ 0}
pₓ : Polynomial R := Polynomial.map (eval xₜ) p'
hpₓ : pₓ = Polynomial.map (eval xₜ) p'
hpₓdeg : pₓ.natDegree = k
hpₓ₀ : pₓ ≠ 0
⊢ #({x₀ ∈ S 0 | (eval (Fin.cons x₀ xₜ)) p = 0}) ≤ degreeOf 0 p
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
h : f = 0
⊢ ¬m.toSyn (m.degree g) < m.toSyn (m.degree f)

Tactic:
;

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hg : ¬g = 0
h : f = 0
⊢ ¬m.toSyn (m.degree g) < m.toSyn (m.degree f)
Module: Mathlib.Algebra.MvPolynomial.SchwartzZippel

Goal state before:
pp: case a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ≠ 0
S : Fin n → Finset R
s : Fin n →₀ ℕ
hs : s ∈ p.support
i : Fin n
a✝ : i ∈ univ
⊢ s i ≤ degreeOf i p

Tactic:
;

Goal state after:
case a
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ≠ 0
S : Fin n → Finset R
s : Fin n →₀ ℕ
hs : s ∈ p.support
i : Fin n
a✝ : i ∈ univ
⊢ s i ≤ degreeOf i p
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
inst✝ : Zero R
f : ArithmeticFunction R
⊢ ⇑f ∈ {f | f 0 = 0}

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : Zero R
f : ArithmeticFunction R
⊢ ⇑f ∈ {f | f 0 = 0}
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

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

Tactic:
;

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.Defs

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
n x : ℕ
⊢ { 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:
R : Type u_1
inst✝ : AddMonoidWithOne R
n x : ℕ
⊢ { 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: R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
x✝ : ℕ
⊢ (f.ppow 1) x✝ = f x✝

Tactic:
;

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
x✝ : ℕ
⊢ (0 * f) x✝ = 0 x✝

Tactic:
;

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
x✝ : ℕ
⊢ (f * 0) x✝ = 0 x✝

Tactic:
;

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
x✝ : ℕ
⊢ (a * (b + c)) x✝ = (a * b + a * c) x✝

Tactic:
;

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.Zeta

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

Tactic:
;

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

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

Tactic:
;

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:
by
    ext
    rw [mul_apply, ← map_swap_divisorsAntidiagonal, sum_map]
    simp [mul_comm]

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

Goal state before:
pp: n : ℕ
hn : IsPrimePow n
⊢ n.minFac ^ n.factorization n.minFac = n

Tactic:
obtain ⟨p, k, hp, hk, rfl⟩ := hn

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

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

case inr
n : ℕ
h : IsPrimePow n
hn0 : n ≠ 0
⊢ ∃ p, Nat.Prime p ∧ n / p ^ n.factorization p = 1
Module: Mathlib.Data.Nat.Factorization.PrimePow

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

Tactic:
apply existsUnique_congr

Goal state after:
n k : ℕ
hk : k ≠ 0
⊢ ∀ (a : ℕ), Nat.Prime a ∧ a ∣ n ^ k ↔ Nat.Prime a ∧ a ∣ n
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

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

Tactic:
by simpa using Nonempty.map this

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

Goal state before:
pp: m n : ℕ
m0 : m ≠ 0
n0 : n ≠ 0
⊢ (↑m.primeFactorsList + ↑n.primeFactorsList).card = m.primeFactorsList.length + n.primeFactorsList.length

Tactic:
Multiset.card_add,

Goal state after:
m n : ℕ
m0 : m ≠ 0
n0 : n ≠ 0
⊢ (↑m.primeFactorsList).card + (↑n.primeFactorsList).card = m.primeFactorsList.length + n.primeFactorsList.length
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: case cons
ι : Type u_2
f : ι → ℕ
a : ι
s : Finset ι
ha : a ∉ s
ih : (↑s).Pairwise (Coprime on f) → ω (∏ i ∈ s, f i) = ∑ i ∈ s, ω (f i)
h : (↑(cons a s ha)).Pairwise (Coprime on f)
⊢ ω (∏ i ∈ cons a s ha, f i) = ∑ i ∈ cons a s ha, ω (f i)

Tactic:
prod_cons,

Goal state after:
case cons
ι : Type u_2
f : ι → ℕ
a : ι
s : Finset ι
ha : a ∉ s
ih : (↑s).Pairwise (Coprime on f) → ω (∏ i ∈ s, f i) = ∑ i ∈ s, ω (f i)
h : (↑(cons a s ha)).Pairwise (Coprime on f)
⊢ ω (f a * ∏ x ∈ s, f x) = ∑ i ∈ cons a s ha, ω (f i)
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: N a✝ : ℕ
⊢ a✝ ∈ {x ∈ Ioc 0 N | ¬x = 0} ↔ a✝ ∈ Ioc 0 N

Tactic:
;

Goal state after:
N a✝ : ℕ
⊢ a✝ ∈ {x ∈ Ioc 0 N | ¬x = 0} ↔ a✝ ∈ Ioc 0 N
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: N a✝ : ℕ
⊢ 0 < a✝ → a✝ ≤ N → ¬a✝ = 0

Tactic:
;

Goal state after:
N a✝ : ℕ
⊢ 0 < a✝ → a✝ ≤ N → ¬a✝ = 0
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: case h
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
⊢ a 0 * a 1 * a 2 = (a 0 * a 1, a 0 * a 2).2 * a 1

Tactic:
;

Goal state after:
case h
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
⊢ a 0 * a 1 * a 2 = (a 0 * a 1, a 0 * a 2).2 * a 1
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: case h
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
⊢ n = a 1 * a 2 * a 0

Tactic:
;

Goal state after:
case h
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
⊢ n = a 1 * a 2 * a 0
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: case h
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
⊢ a 0 * a 1 * a 2 = a 1 * a 2 * a 0

Tactic:
;

Goal state after:
case h
n : ℕ
hn : Squarefree n
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
⊢ a 0 * a 1 * a 2 = a 1 * a 2 * a 0
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:

Tactic:
;

Goal state after: