mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.ZLattice.Summable

Goal state before:
pp: case a
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝² : DiscreteTopology ↥L
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ ↥L
n : ℕ
r : ℝ
s : ℕ → Finset (ι → ℤ) := fun n ↦ Fintype.piFinset fun i ↦ Icc (-↑n) ↑n
d : ℕ := Fintype.card ι
hr : r < -↑d
hr' : r < 0
hd : 1 ≤ d
hs0 : s 0 = {0}
hs : ∀ {a b : ℕ}, a ≤ b → s a ⊆ s b
this : ∀ (k : ℕ), #(s (k + 1) \ s k) ≤ 2 * d * (2 * k + 3) ^ (d - 1)
ε : ℝ := normBound b
hε : 0 < ε
k : ℕ
hk : k ∈ range n
⊢ 2 * d * (2 * k + 3) ^ (d - 1) ≤ 2 * d * (3 * (k + 1)) ^ (d - 1)

Tactic:
gcongr

Goal state after:
case hab
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝² : DiscreteTopology ↥L
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ ↥L
n : ℕ
r : ℝ
s : ℕ → Finset (ι → ℤ) := ⋯
d : ℕ := ⋯
hr : r < -↑d
hr' : r < 0
hd : 1 ≤ d
hs0 : s 0 = {0}
hs : ∀ {a b : ℕ}, a ≤ b → s a ⊆ s b
this : ∀ (k : ℕ), #(s (k + 1) \ s k) ≤ 2 * d * (2 * k + 3) ^ (d - 1)
ε : ℝ := ⋯
hε : 0 < ε
k : ℕ
hk : k ∈ range n
⊢ 2 * k + 3 ≤ 3 * (k + 1)
Module: Mathlib.Algebra.Module.ZLattice.Summable

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝² : DiscreteTopology ↥L
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ ↥L
n : ℕ
r : ℝ
s : ℕ → Finset (ι → ℤ) := fun n ↦ Fintype.piFinset fun i ↦ Icc (-↑n) ↑n
d : ℕ := Fintype.card ι
hr : r < -↑d
hr' : r < 0
hd : 1 ≤ d
hs0 : s 0 = {0}
hs : ∀ {a b : ℕ}, a ≤ b → s a ⊆ s b
this : ∀ (k : ℕ), #(s (k + 1) \ s k) ≤ 2 * d * (2 * k + 3) ^ (d - 1)
ε : ℝ := normBound b
hε : 0 < ε
⊢ 2 * ↑d * 3 ^ (d - 1) * ε ^ r * ∑ k ∈ range (n + 1), ↑k ^ (↑d - 1 + r) ≤
    2 * ↑d * 3 ^ (d - 1) * ε ^ r * ∑' (k : ℕ), ↑k ^ (↑d - 1 + r)

Tactic:
gcongr

Goal state after:
case hbc
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝² : DiscreteTopology ↥L
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ ↥L
n : ℕ
r : ℝ
s : ℕ → Finset (ι → ℤ) := ⋯
d : ℕ := ⋯
hr : r < -↑d
hr' : r < 0
hd : 1 ≤ d
hs0 : s 0 = {0}
hs : ∀ {a b : ℕ}, a ≤ b → s a ⊆ s b
this : ∀ (k : ℕ), #(s (k + 1) \ s k) ≤ 2 * d * (2 * k + 3) ^ (d - 1)
ε : ℝ := ⋯
hε : 0 < ε
⊢ ∑ k ∈ range (n + 1), ↑k ^ (↑d - 1 + r) ≤ ∑' (k : ℕ), ↑k ^ (↑d - 1 + r)
Module: Mathlib.Analysis.BoxIntegral.Basic

Goal state before:
pp: ι : Type u
E : Type v
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : Fintype ι
l : IntegrationParams
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
hc : ∀ᵐ (x : ι → ℝ) ∂μ.restrict (Box.Icc I), ContinuousWithinAt f (Box.Icc I) x
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
hε₁ : 2 * μ.toBoxAdditive I * ε₁ < ε
C : ℝ
hC : ∀ x ∈ Box.Icc I, ‖f x‖ ≤ C
C0 : 0 ≤ C
ε₂ : ℝ
ε₂0 : 0 < ε₂
hε₂ : 4 * C * ε₂ < ε
ε₂0' : ENNReal.ofReal ε₂ ≠ 0
D : Set (ι → ℝ) := {x | x ∈ Box.Icc I ∧ ¬ContinuousWithinAt f (Box.Icc I) x}
μ' : Measure (ι → ℝ) := μ.restrict (Box.Icc I)
μ'D : μ' D = 0
U : Set (ι → ℝ)
UD : U ⊇ D
Uopen : IsOpen U
hU : μ' U < ENNReal.ofReal ε₂
comp : IsCompact (Box.Icc I \ U)
this : ∀ x ∈ Box.Icc I \ U, oscillationWithin f (Box.Icc I) x < ENNReal.ofReal ε₁
r : ℝ
r0 : r > 0
hr : ∀ x ∈ Box.Icc I \ U, ediam (f '' (eball x (ENNReal.ofReal r) ∩ Box.Icc I)) ≤ ENNReal.ofReal ε₁
c₁ c₂ : ℝ≥0
π₁ π₂ : TaggedPrepartition I
h₁ : l.MemBaseSet I c₁ ((fun x x_1 ↦ ⟨r / 2, ⋯⟩) c₁) π₁
h₁p : π₁.IsPartition
h₂ : l.MemBaseSet I c₂ ((fun x x_1 ↦ ⟨r / 2, ⋯⟩) c₂) π₂
h₂p : π₂.IsPartition
μI : μ ↑I < ∞
t₁ : Box ι → ι → ℝ := fun J ↦ (π₁.infPrepartition π₂.toPrepartition).tag J
t₂ : Box ι → ι → ℝ := fun J ↦ (π₂.infPrepartition π₁.toPrepartition).tag J
B : Finset (Box ι) := (π₁.toPrepartition ⊓ π₂.toPrepartition).boxes
B' : Finset (Box ι) := {J ∈ B | ↑J ⊆ U}
hB' : B' ⊆ B
μJ_ne_top : ∀ J ∈ B, μ ↑J ≠ ∞
un : ∀ S ⊆ B, ⋃ J ∈ S, ↑J ⊆ ↑I
J : Box ι
a✝ : J ∈ B'
⊢ μ.real ↑J * ‖f (t₁ J) - f (t₂ J)‖ ≤ μ.real ↑J * (C + C)

Tactic:
gcongr

Goal state after:
case hbc
ι : Type u
E : Type v
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : Fintype ι
l : IntegrationParams
inst✝¹ : CompleteSpace E
I : Box ι
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
hc : ∀ᵐ (x : ι → ℝ) ∂μ.restrict (Box.Icc I), ContinuousWithinAt f (Box.Icc I) x
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
hε₁ : 2 * μ.toBoxAdditive I * ε₁ < ε
C : ℝ
hC : ∀ x ∈ Box.Icc I, ‖f x‖ ≤ C
C0 : 0 ≤ C
ε₂ : ℝ
ε₂0 : 0 < ε₂
hε₂ : 4 * C * ε₂ < ε
ε₂0' : ENNReal.ofReal ε₂ ≠ 0
D : Set (ι → ℝ) := ⋯
μ' : Measure (ι → ℝ) := ⋯
μ'D : μ' D = 0
U : Set (ι → ℝ)
UD : U ⊇ D
Uopen : IsOpen U
hU : μ' U < ENNReal.ofReal ε₂
comp : IsCompact (Box.Icc I \ U)
this : ∀ x ∈ Box.Icc I \ U, oscillationWithin f (Box.Icc I) x < ENNReal.ofReal ε₁
r : ℝ
r0 : r > 0
hr : ∀ x ∈ Box.Icc I \ U, ediam (f '' (eball x (ENNReal.ofReal r) ∩ Box.Icc I)) ≤ ENNReal.ofReal ε₁
c₁ c₂ : ℝ≥0
π₁ π₂ : TaggedPrepartition I
h₁ : l.MemBaseSet I c₁ ((fun x x_1 ↦ ⟨r / 2, ⋯⟩) c₁) π₁
h₁p : π₁.IsPartition
h₂ : l.MemBaseSet I c₂ ((fun x x_1 ↦ ⟨r / 2, ⋯⟩) c₂) π₂
h₂p : π₂.IsPartition
μI : μ ↑I < ∞
t₁ : Box ι → ι → ℝ := ⋯
t₂ : Box ι → ι → ℝ := ⋯
B : Finset (Box ι) := ⋯
B' : Finset (Box ι) := ⋯
hB' : B' ⊆ B
μJ_ne_top : ∀ J ∈ B, μ ↑J ≠ ∞
un : ∀ S ⊆ B, ⋃ J ∈ S, ↑J ⊆ ↑I
J : Box ι
a✝ : J ∈ B'
⊢ ‖f (t₁ J) - f (t₂ J)‖ ≤ C + C
Module: Mathlib.Algebra.Module.ZLattice.Summable

Goal state before:
pp: case neg
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
h✝ : Nontrivial ↥L
I : Type u_1 := Free.ChooseBasisIndex ℤ ↥L
this : Fintype I
b : Basis I ℤ ↥L := Free.chooseBasis ℤ ↥L
d : ℕ := Fintype.card I
hd : d ≠ 0
ε : ℝ := normBound b
A : ℝ
hA : A > 0
B : ℝ
hB : B > 0
H : ∀ r < -↑d, ∀ (s : Finset ↥L), ∑ z ∈ s, ‖z‖ ^ r ≤ A * B ^ r * ∑' (k : ℕ), ↑k ^ (↑d - 1 + r)
hA' : ¬A ≤ 1
r : ℝ
hr : r < -↑d
s : Finset ↥L
⊢ A * (B ^ r * ∑' (k : ℕ), ↑k ^ (↑d - 1 + r)) ≤ A⁻¹ ^ r * (B ^ r * ∑' (k : ℕ), ↑k ^ (↑d - 1 + r))

Tactic:
gcongr

Goal state after:
case hbc
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
h✝ : Nontrivial ↥L
I : Type u_1 := ⋯
this : Fintype I
b : Basis I ℤ ↥L := ⋯
d : ℕ := ⋯
hd : d ≠ 0
ε : ℝ := ⋯
A : ℝ
hA : A > 0
B : ℝ
hB : B > 0
H : ∀ r < -↑d, ∀ (s : Finset ↥L), ∑ z ∈ s, ‖z‖ ^ r ≤ A * B ^ r * ∑' (k : ℕ), ↑k ^ (↑d - 1 + r)
hA' : ¬A ≤ 1
r : ℝ
hr : r < -↑d
s : Finset ↥L
⊢ A ≤ A⁻¹ ^ r
Module: Mathlib.Algebra.Module.ZLattice.Summable

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
n : ℕ
hn : finrank ℤ ↥L < n
x : E
⊢ -↑n < -↑(finrank ℤ ↥L)

Tactic:
gcongr

Goal state after:
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a✝ : α
m : Multiset α
a : α
h : ¬a✝ ≠ a
⊢ 0 = Function.update (⇑(toFinsupp m)) a 0 a

Tactic:
Function.update_self

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
a✝ : α
m : Multiset α
a : α
h : ¬a✝ ≠ a
⊢ 0 = 0
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ (2 * ∑ i ∈ s, f i)! * ∏ i ∈ s, (f i)! ≤ ((2 * ∑ i ∈ s, f i) ^ ∑ i ∈ s, f i) * (∑ i ∈ s, f i)! * ∏ i ∈ s, (f i)!

Tactic:
gcongr

Goal state after:
case h₁
ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ (2 * ∑ i ∈ s, f i)! ≤ ((2 * ∑ i ∈ s, f i) ^ ∑ i ∈ s, f i) * (∑ i ∈ s, f i)!
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ ((∑ i ∈ s, f i) ^ ∑ i ∈ s, f i) * (∑ i ∈ s, f i)! * ∏ i ∈ s, 2 ^ f i * (f i)! ≤
    ((∑ i ∈ s, f i) ^ ∑ i ∈ s, f i) * (∑ i ∈ s, f i)! * ∏ i ∈ s, (2 * f i)!

Tactic:
gcongr

Goal state after:
case h1
ι : Type u_1
s : Finset ι
f : ι → ℕ
i : ι
a✝ : i ∈ s
⊢ 2 ^ f i * (f i)! ≤ (2 * f i)!
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

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

Tactic:
intro hf
    rw [← support_nonempty] at hf
    rw [leadingCoeff, ← mem_support_iff, degree]
    suffices f.support.sup m.toSyn ∈ m.toSyn '' f.support by
      obtain ⟨d, hd, hd'⟩ := this
      rw [← hd', AddEquiv.symm_apply_apply]
      exact hd
    exact Finset.sup_mem_of_nonempty hf

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

Goal state before:
pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
hf : IsRegular (m.leadingCoeff f)
hg : ¬g = 0
⊢ m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g

Tactic:
· simp only [leadingCoeff, degree_mul_of_isRegular_left hf hg, coeff_mul_of_degree_add]

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 ∈ piFinset fun i ↦ S i | (eval x) p = 0 ∧ (eval (tail x)) pₖ ≠ 0})) / ∏ i, ↑(#(S i)) ≤
    ↑(degreeOf 0 p * ∏ i, #(S i.succ)) / ∏ i, ↑(#(S i))

Tactic:
gcongr

Goal state after:
case a
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 ↦ S i | (eval x) p = 0 ∧ (eval (tail x)) pₖ ≠ 0}) ≤ degreeOf 0 p * ∏ i, #(S i.succ)
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 ↦ tail S i with (eval xₜ) pₖ ≠ 0,
      #(image (fun x₀ ↦ (x₀, xₜ)) ({x₀ ∈ S 0 | (eval (Fin.cons x₀ xₜ)) p = 0})) ≤
    ∑ xₜ ∈ piFinset fun i ↦ tail S i with (eval xₜ) pₖ ≠ 0, #({x₀ ∈ S 0 | (eval (Fin.cons x₀ xₜ)) p = 0})

Tactic:
gcongr

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.Data.Nat.Squarefree

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

Tactic:
gcongr

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: 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 ↦ tail S i with (eval xₜ) pₖ ≠ 0, degreeOf 0 p ≤ ∑ _xₜ ∈ piFinset fun i ↦ tail S i, degreeOf 0 p

Tactic:
gcongr

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 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'.sqrt - k ≤ n.sqrt - k

Tactic:
gcongr

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

Goal state before:
pp: ⊢ Squarefree 2

Tactic:
rw [squarefree_iff_nodup_primeFactorsList]

Goal state after:
⊢ (primeFactorsList 2).Nodup

⊢ 2 ≠ 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ₜ : 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}) ≤ #pₓ.roots.toFinset

Tactic:
gcongr

Goal state after:
case a
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ₜ : Fin n → R
hxₜ : xₜ ∈ {xₜ ∈ piFinset fun i ↦ tail S i | (eval xₜ) pₖ ≠ 0}
pₓ : Polynomial R := ⋯
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} ⊆ pₓ.roots.toFinset
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) ∧ (normalizedFactors a).prod = a

Tactic:
← associated_iff_eq,

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

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

Tactic:
gcongr

Goal state after:
case a
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
i : Fin n →₀ ℕ
hi : i ∈ pₖ.support
⊢ degreeOf 0 p ≤ p'.natDegree
Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta

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

Tactic:
cases x <;> simp

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

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

Tactic:
cases x <;> simp

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
k x : ℕ
⊢ (f.ppow (k + 1)) x = (f.pmul (f.ppow k)) x

Tactic:
rw [ppow_apply (succ_pos k), _root_.pow_succ']

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
k x : ℕ
⊢ f x * f x ^ k = (f.pmul (f.ppow k)) x
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
h₁ : m.degree f = 0
h₂ : m.degree g = 0
this : C (m.leadingCoeff g) * f - C (m.leadingCoeff f) * g = 0
⊢ m.sPolynomial f g = 0

Tactic:
by simp_all [sPolynomial_def]

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

Goal state before:
pp: s : Finset ℕ
hs : ∀ p ∈ s, Prime p
⊢ (∏ p ∈ s, p).primeFactors = s

Tactic:
by
  have hn : ∏ p ∈ s, p ≠ 0 := prod_ne_zero_iff.2 fun p hp ↦ (hs _ hp).ne_zero
  ext p
  rw [mem_primeFactors_of_ne_zero hn, and_congr_right (fun hp ↦ hp.prime.dvd_finsetProd_iff _)]
  refine ⟨?_, fun hp ↦ ⟨hs _ hp, _, hp, dvd_rfl⟩⟩
  rintro ⟨hp, q, hq, hpq⟩
  rwa [← ((hs _ hq).dvd_iff_eq hp.ne_one).1 hpq]

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

Goal state before:
pp: k : ℕ
⊢ ζ * pow k = σ k

Tactic:
by
  ext
  rw [sigma, zeta_mul_apply]
  apply sum_congr rfl
  aesop

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

Goal state before:
pp: case neg.mp
k n : ℕ
hn0 : ¬n = 0
⊢ (σ k) n = 1 → n = 1

pp: case neg.mpr
k n : ℕ
hn0 : ¬n = 0
⊢ n = 1 → (σ k) n = 1

Tactic:
· intro h
    rw [← sigma_zero_eq_one_iff]
    have zero_lt_sigma := sigma_pos 0 n hn0
    have sigma_zero_le_sigma := sigma_mono 0 k n k.zero_le
    lia

Goal state after:
case neg.mpr
k n : ℕ
hn0 : ¬n = 0
⊢ n = 1 → (σ k) n = 1
Module: Mathlib.Algebra.Order.Rearrangement

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁸ : Semiring α
inst✝⁷ : LinearOrder α
inst✝⁶ : IsStrictOrderedRing α
inst✝⁵ : ExistsAddOfLE α
inst✝⁴ : AddCommMonoid β
inst✝³ : LinearOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulMono α β
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : a ∉ s
hamax : ∀ x ∈ s, toLex (g x, f x) ≤ toLex (g a, f a)
hind : ∀ {σ : Perm ι}, MonovaryOn f g ↑s → {x | σ x ≠ x} ⊆ ↑s → ∑ i ∈ s, f i • g (σ i) ≤ ∑ i ∈ s, f i • g i
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := Equiv.trans σ (Equiv.swap a (σ a))
hτ : τ = Equiv.trans σ (Equiv.swap a (σ a))
x : ι
hx : x ∈ {x | τ x ≠ x}
⊢ x ∈ ↑s

Tactic:
simp only [τ, Ne, Set.mem_ofPred_eq, Equiv.swap_comp_apply] at hx

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁸ : Semiring α
inst✝⁷ : LinearOrder α
inst✝⁶ : IsStrictOrderedRing α
inst✝⁵ : ExistsAddOfLE α
inst✝⁴ : AddCommMonoid β
inst✝³ : LinearOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulMono α β
f : ι → α
g : ι → β
a : ι
s : Finset ι
has : a ∉ s
hamax : ∀ x ∈ s, toLex (g x, f x) ≤ toLex (g a, f a)
hind : ∀ {σ : Perm ι}, MonovaryOn f g ↑s → {x | σ x ≠ x} ⊆ ↑s → ∑ i ∈ s, f i • g (σ i) ≤ ∑ i ∈ s, f i • g i
σ : Perm ι
hfg : MonovaryOn f g ↑(insert a s)
hσ : {x | σ x ≠ x} ⊆ ↑(insert a s)
τ : Perm ι := Equiv.trans σ (Equiv.swap a (σ a))
hτ : τ = Equiv.trans σ (Equiv.swap a (σ a))
x : ι
hx : ¬(if σ x = a then σ a else if σ x = σ a then a else σ x) = x
⊢ x ∈ ↑s
Module: Mathlib.Algebra.Order.Chebyshev

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝³ : Semiring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : ExistsAddOfLE α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, 0 ≤ f i
n : ℕ
⊢ (∑ i ∈ s, f i) ^ (n + 1) * ∑ i ∈ s, f i ≤ (↑(#s) ^ n * ∑ i ∈ s, f i ^ (n + 1)) * ∑ i ∈ s, f i

Tactic:
gcongr

Goal state after:
case ha
ι : Type u_1
α : Type u_2
inst✝³ : Semiring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : ExistsAddOfLE α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, 0 ≤ f i
n : ℕ
⊢ 0 ≤ ∑ i ∈ s, f i

case hbc
ι : Type u_1
α : Type u_2
inst✝³ : Semiring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : ExistsAddOfLE α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, 0 ≤ f i
n : ℕ
⊢ (∑ i ∈ s, f i) ^ (n + 1) ≤ ↑(#s) ^ n * ∑ i ∈ s, f i ^ (n + 1)
Module: Mathlib.Algebra.Order.Chebyshev

Goal state before:
pp: case inr
ι : Type u_1
α : Type u_2
inst✝³ : Semifield α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : ExistsAddOfLE α
s : Finset ι
f : ι → α
hs : s.Nonempty
⊢ (∑ i ∈ s, f i) ^ 2 * ↑(#s) ≤ (↑(#s) * ∑ i ∈ s, f i ^ 2) * ↑(#s)

Tactic:
gcongr

Goal state after:
case hbc
ι : Type u_1
α : Type u_2
inst✝³ : Semifield α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : ExistsAddOfLE α
s : Finset ι
f : ι → α
hs : s.Nonempty
⊢ (∑ i ∈ s, f i) ^ 2 ≤ ↑(#s) * ∑ i ∈ s, f i ^ 2
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a b : M
⊢ mk (a / b) = mk (b / a)

Tactic:
rw [← mk_inv, inv_div]

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Semifield

Goal state before:
pp: K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a b : K
hb₀ : 0 < b
hb : b < 1
hba : ↑⌈b / (1 - b)⌉₊ ≤ a
⊢ b * a < b * (↑⌊a⌋₊ + 1)

Tactic:
gcongr

Goal state after:
case hbc
K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a b : K
hb₀ : 0 < b
hb : b < 1
hba : ↑⌈b / (1 - b)⌉₊ ≤ a
⊢ a < ↑⌊a⌋₊ + 1
Module: Mathlib.Algebra.Order.Floor.Semifield

Goal state before:
pp: K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a b : K
hb : 1 < b
hba : ↑⌈(b - 1)⁻¹⌉₊ / b < a
hab : a ≤ (b - 1)⁻¹
⊢ ↑⌈a⌉₊ ≤ ↑⌈(b - 1)⁻¹⌉₊

Tactic:
gcongr

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Semifield

Goal state before:
pp: K : Type u_2
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsOrderedRing K
inst✝ : FloorSemiring K
a b : K
hb : 0 < b - 1
hba✝ : ↑⌈(b - 1)⁻¹⌉₊ / b < a
hba : (b - 1)⁻¹ ≤ a
⊢ a + (b - 1) * (b - 1)⁻¹ ≤ a + (b - 1) * a

Tactic:
gcongr

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: r : ℝ≥0
n : ℕ
⊢ ⌊↑r + ↑n⌋ₑ = ↑(⌊r⌋₊ + n)

Tactic:
← ENNReal.ofNNReal_add_natCast

Goal state after:
r : ℝ≥0
n : ℕ
⊢ ⌊↑(r + ↑n)⌋ₑ = ↑(⌊r⌋₊ + n)
Module: Mathlib.Algebra.Order.Floor.Extended

Goal state before:
pp: r : ℝ≥0
n : ℕ
⊢ ⌈↑r + ↑n⌉ₑ = ↑(⌈r⌉₊ + n)

Tactic:
← ENNReal.ofNNReal_add_natCast

Goal state after:
r : ℝ≥0
n : ℕ
⊢ ⌈↑(r + ↑n)⌉ₑ = ↑(⌈r⌉₊ + n)
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
r : Finset ℤ := Ioc (c - ↑(#s)) c
⊢ ∑ x ∈ s ∩ r, x + ∑ x ∈ s \ r, x ≤ ∑ x ∈ s ∩ r, x + #(s \ r) • (c - ↑(#s))

Tactic:
gcongr

Goal state after:
case h₂
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
r : Finset ℤ := ⋯
⊢ ∑ x ∈ s \ r, x ≤ #(s \ r) • (c - ↑(#s))
Module: Mathlib.Algebra.Order.Group.Int.Sum

Goal state before:
pp: s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
r : Finset ℤ := Ioc (c - ↑(#s)) c
⊢ ∑ x ∈ r ∩ s, x + #(r \ s) • (c - ↑(#s)) ≤ ∑ x ∈ r ∩ s, x + ∑ x ∈ r \ s, x

Tactic:
gcongr

Goal state after:
case h₂
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, x ≤ c
r : Finset ℤ := ⋯
⊢ #(r \ s) • (c - ↑(#s)) ≤ ∑ x ∈ r \ s, x
Module: Mathlib.Data.Finset.MulAntidiagonal

Goal state before:
pp: case mpr
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedCancelMonoid α
s t : Set α
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
a b : α
⊢ a = hs.min hns ∧ b = ht.min hnt → a ∈ s ∧ b ∈ t ∧ a * b = hs.min hns * ht.min hnt

Tactic:
rintro ⟨rfl, rfl⟩
    exact ⟨hs.min_mem _, ht.min_mem _, rfl⟩

Goal state after: