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

Goal state before:
pp: case refine_3
ι : Type u
E : Type v
inst✝⁴ : Fintype ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
g : (ι → ℝ) → E
hg : StronglyMeasurable g
this : SeparableSpace ↑(Set.range g ∪ {0})
hgi✝ : IntegrableOn g (↑I) μ
f : ℕ → SimpleFunc (ι → ℝ) E := SimpleFunc.approxOn g ⋯ (Set.range g ∪ {0}) 0 ⋯
hfi✝ : ∀ (n : ℕ), IntegrableOn (⇑(f n)) (↑I) μ
hfi' : ∀ (n : ℕ), BoxIntegral.Integrable I l (⇑(f n)) μ.toBoxAdditive.toSMul
hfg_mono : ∀ (x : ι → ℝ) {m n : ℕ}, m ≤ n → ‖(f n) x - g x‖ ≤ ‖(f m) x - g x‖
ε : ℝ≥0
ε0 : 0 < ε
ε0' : 0 < ↑ε
N₀ : ℕ
hN₀ : ∫ (x : ι → ℝ) in ↑I, ‖(f N₀) x - g x‖ ∂μ ≤ ↑ε
Nx : (ι → ℝ) → ℕ
hNx : ∀ (x : ι → ℝ), N₀ ≤ Nx x
hNxε : ∀ (x : ι → ℝ), dist ((f (Nx x)) x) (g x) ≤ ↑ε
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c✝ : ℝ≥0
hδc : HasSum δ c✝
hcε : c✝ < ε
r : ℝ≥0 → (ι → ℝ) → ↑(Set.Ioi 0) := fun c x ↦ ⋯.convergenceR (↑(δ (Nx x))) c x
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c (r c) π
hπp : π.IsPartition
hfi : ∀ (n : ℕ), ∀ J ∈ π, IntegrableOn (⇑(f n)) (↑J) μ
hgi : ∀ J ∈ π, IntegrableOn g (↑J) μ
hfgi : ∀ (n : ℕ), ∀ J ∈ π, IntegrableOn (fun x ↦ ‖(f n) x - g x‖) (↑J) μ
J : Box ι
hJ : J ∈ π.boxes
⊢ ‖∫ (a : ι → ℝ) in ↑J, (f (Nx (π.tag J))) a - g a ∂μ‖ ≤ ∫ (x : ι → ℝ) in ↑J, ‖(f N₀) x - g x‖ ∂μ

Tactic:
refine norm_integral_le_of_norm_le (hfgi _ J hJ) (Eventually.of_forall fun x => ?_)

Goal state after:
case refine_3
ι : Type u
E : Type v
inst✝⁴ : Fintype ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
l : IntegrationParams
hl : l.bRiemann = false
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
g : (ι → ℝ) → E
hg : StronglyMeasurable g
this : SeparableSpace ↑(Set.range g ∪ {0})
hgi✝ : IntegrableOn g (↑I) μ
f : ℕ → SimpleFunc (ι → ℝ) E := SimpleFunc.approxOn g ⋯ (Set.range g ∪ {0}) 0 ⋯
hfi✝ : ∀ (n : ℕ), IntegrableOn (⇑(f n)) (↑I) μ
hfi' : ∀ (n : ℕ), BoxIntegral.Integrable I l (⇑(f n)) μ.toBoxAdditive.toSMul
hfg_mono : ∀ (x : ι → ℝ) {m n : ℕ}, m ≤ n → ‖(f n) x - g x‖ ≤ ‖(f m) x - g x‖
ε : ℝ≥0
ε0 : 0 < ε
ε0' : 0 < ↑ε
N₀ : ℕ
hN₀ : ∫ (x : ι → ℝ) in ↑I, ‖(f N₀) x - g x‖ ∂μ ≤ ↑ε
Nx : (ι → ℝ) → ℕ
hNx : ∀ (x : ι → ℝ), N₀ ≤ Nx x
hNxε : ∀ (x : ι → ℝ), dist ((f (Nx x)) x) (g x) ≤ ↑ε
δ : ℕ → ℝ≥0
δ0 : ∀ (i : ℕ), 0 < δ i
c✝ : ℝ≥0
hδc : HasSum δ c✝
hcε : c✝ < ε
r : ℝ≥0 → (ι → ℝ) → ↑(Set.Ioi 0) := fun c x ↦ ⋯.convergenceR (↑(δ (Nx x))) c x
c : ℝ≥0
π : TaggedPrepartition I
hπ : l.MemBaseSet I c (r c) π
hπp : π.IsPartition
hfi : ∀ (n : ℕ), ∀ J ∈ π, IntegrableOn (⇑(f n)) (↑J) μ
hgi : ∀ J ∈ π, IntegrableOn g (↑J) μ
hfgi : ∀ (n : ℕ), ∀ J ∈ π, IntegrableOn (fun x ↦ ‖(f n) x - g x‖) (↑J) μ
J : Box ι
hJ : J ∈ π.boxes
x : ι → ℝ
⊢ ‖(f (Nx (π.tag J))) x - g x‖ ≤ ‖(f N₀) x - g x‖
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: case zero
M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedAddMonoid M
f : ℕ → M
u : ℕ → ℕ
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : Monotone u
⊢ ∑ k ∈ Ico (u 0) (u 0), f k ≤ ∑ k ∈ range 0, (u (k + 1) - u k) • f (u k)

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: case zero
M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedAddMonoid M
f : ℕ → M
u : ℕ → ℕ
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : Monotone u
⊢ ∑ k ∈ range 0, (u (k + 1) - u k) • f (u (k + 1)) ≤ ∑ k ∈ Ico (u 0 + 1) (u 0 + 1), f k

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Covolume

Goal state before:
pp: case e_a
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
L : Submodule ℤ E
inst✝⁵ : DiscreteTopology ↥L
inst✝⁴ : IsZLattice ℝ L
ι : Type u_2
inst✝³ : Fintype ι
b : Basis ι ℤ ↥L
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s : Set E
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier (⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' s)) = 0
n : ℕ
hn : 0 < n
x : E
⊢ x ∈ s →
    (↑n • x ∈ span ℤ (Set.range ⇑(Basis.ofZLatticeBasis ℝ L b)) ↔
      ⇑((Basis.ofZLatticeBasis ℝ L b).repr (↑n • x)) ∈ span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))

Tactic:
Basis.mem_span_iff_repr_mem,

Goal state after:
case e_a
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
L : Submodule ℤ E
inst✝⁵ : DiscreteTopology ↥L
inst✝⁴ : IsZLattice ℝ L
ι : Type u_2
inst✝³ : Fintype ι
b : Basis ι ℤ ↥L
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
s : Set E
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier (⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' s)) = 0
n : ℕ
hn : 0 < n
x : E
⊢ x ∈ s →
    ((∀ (i : ι), ((Basis.ofZLatticeBasis ℝ L b).repr (↑n • x)) i ∈ Set.range ⇑(algebraMap ℤ ℝ)) ↔
      ∀ (i : ι),
        ((Pi.basisFun ℝ ι).repr ⇑((Basis.ofZLatticeBasis ℝ L b).repr (↑n • x))) i ∈ Set.range ⇑(algebraMap ℤ ℝ))
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: case e'_2
f : ℕ → ℝ
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → 0 b ≤ f b
m : ℕ
hm : ∀ (b : ℕ), m ≤ b → f (b + 1) ≤ f b
⊢ Summable f ↔ Summable fun k ↦ f (max k (n + m))

Tactic:
rw [summable_congr_atTop]
    filter_upwards [Filter.eventually_ge_atTop (n + m)] with _ hk using by simp [max_eq_left hk]

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: case convert_2
f : ℕ → ℝ
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → 0 b ≤ f b
m : ℕ
hm : ∀ (b : ℕ), m ≤ b → f (b + 1) ≤ f b
⊢ ∀ ⦃m_1 n_1 : ℕ⦄, 0 < m_1 → m_1 ≤ n_1 → f (max n_1 (n + m)) ≤ f (max m_1 (n + m))

Tactic:
intro _ _ _ _

Goal state after:
case convert_2
f : ℕ → ℝ
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → 0 b ≤ f b
m : ℕ
hm : ∀ (b : ℕ), m ≤ b → f (b + 1) ≤ f b
m✝ n✝ : ℕ
a✝¹ : 0 < m✝
a✝ : m✝ ≤ n✝
⊢ f (max n✝ (n + m)) ≤ f (max m✝ (n + m))
Module: Mathlib.Algebra.Module.ZLattice.Covolume

Goal state before:
pp: case e_a
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
L : Submodule ℤ E
inst✝⁶ : DiscreteTopology ↥L
inst✝⁵ : IsZLattice ℝ L
ι : Type u_2
inst✝⁴ : Fintype ι
b : Basis ι ℤ ↥L
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : Nonempty ι
X : Set E
hX : ∀ ⦃x : E⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
F : E → ℝ
h₁ : ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ card ι * F x
h₂ : Bornology.IsBounded {x | x ∈ X ∧ F x ≤ 1}
h₃ : MeasurableSet {x | x ∈ X ∧ F x ≤ 1}
h₄ : volume (frontier (⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' {x | x ∈ X ∧ F x ≤ 1})) = 0
c : ℝ
hc : 0 < c
aux₁ : ↑(card ι) ≠ 0
aux₂ : 0 < c ^ (↑(card ι))⁻¹
aux₃ : (c ^ (↑(card ι))⁻¹)⁻¹ ≠ 0
aux₄ : c ^ (-(↑(card ι))⁻¹) ≠ 0
hc₁ : 0 ≤ c
hc₂ : 0 ≠ c
x✝ : E
⊢ x✝ ∈ {x | x ∈ X ∧ F x ≤ c} →
    (x✝ ∈ span ℤ (Set.range ⇑(Basis.ofZLatticeBasis ℝ L b)) ↔
      (Basis.ofZLatticeBasis ℝ L b).equivFun x✝ ∈ span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))

Tactic:
Basis.mem_span_iff_repr_mem,

Goal state after:
case e_a
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
L : Submodule ℤ E
inst✝⁶ : DiscreteTopology ↥L
inst✝⁵ : IsZLattice ℝ L
ι : Type u_2
inst✝⁴ : Fintype ι
b : Basis ι ℤ ↥L
inst✝³ : FiniteDimensional ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : Nonempty ι
X : Set E
hX : ∀ ⦃x : E⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
F : E → ℝ
h₁ : ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ card ι * F x
h₂ : Bornology.IsBounded {x | x ∈ X ∧ F x ≤ 1}
h₃ : MeasurableSet {x | x ∈ X ∧ F x ≤ 1}
h₄ : volume (frontier (⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' {x | x ∈ X ∧ F x ≤ 1})) = 0
c : ℝ
hc : 0 < c
aux₁ : ↑(card ι) ≠ 0
aux₂ : 0 < c ^ (↑(card ι))⁻¹
aux₃ : (c ^ (↑(card ι))⁻¹)⁻¹ ≠ 0
aux₄ : c ^ (-(↑(card ι))⁻¹) ≠ 0
hc₁ : 0 ≤ c
hc₂ : 0 ≠ c
x✝ : E
⊢ x✝ ∈ {x | x ∈ X ∧ F x ≤ c} →
    ((∀ (i : ι), ((Basis.ofZLatticeBasis ℝ L b).repr x✝) i ∈ Set.range ⇑(algebraMap ℤ ℝ)) ↔
      ∀ (i : ι), ((Pi.basisFun ℝ ι).repr ((Basis.ofZLatticeBasis ℝ L b).equivFun x✝)) i ∈ Set.range ⇑(algebraMap ℤ ℝ))
Module: Mathlib.Data.Nat.Factorial.DoubleFactorial

Goal state before:
pp: k : ℕ
⊢ (k + 1 + 1)! = (k + 2) * k‼ * (k + 1)‼

Tactic:
factorial,

Goal state after:
k : ℕ
⊢ (k + 1).succ * (k + 1)! = (k + 2) * k‼ * (k + 1)‼
Module: Mathlib.Data.Nat.Factorial.DoubleFactorial

Goal state before:
pp: n : ℕ
⊢ (2 * n + 2) * (2 * n)‼ = 2 ^ (n + 1) * (n + 1)!

Tactic:
factorial,

Goal state after:
n : ℕ
⊢ (2 * n + 2) * (2 * n)‼ = 2 ^ (n + 1) * (n.succ * n !)
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
⊢ a.support.sum ⇑s = n

Tactic:
← 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 = s.sum fun x m ↦ m
Module: Mathlib.Algebra.MvPolynomial.Division

Goal state before:
pp: case inr.zero
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
n : σ →₀ ℕ
hR : Nontrivial R
⊢ ∀ (n : σ →₀ ℕ),
    Finsupp.degree n = 0 →
      ∀ (p q : MvPolynomial σ R), p ∣ (monomial n) 1 * q ↔ ∃ m r, m ≤ n ∧ r ∣ q ∧ p = (monomial m) 1 * r

Tactic:
| zero =>

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

Goal state before:
pp: case refine_1
σ : Type u_1
R : Type u_2
inst✝ : CommRing R
P : MvPolynomial σ R
H✝ : IsUnit P
n : σ →₀ ℕ
hn : n ≠ 0
i : σ
hi : n i ≠ 0
e : Polynomial (MvPolynomial { b // b ≠ i } R) ≃ₐ[R] MvPolynomial σ R :=
  (optionEquivLeft R { b // b ≠ i }).symm.trans (renameEquiv R (Equiv.optionSubtypeNe i))
H : IsNilpotent ((e.symm P).coeff (n i))
⊢ IsNilpotent (coeff n P)

Tactic:
simp only [ne_eq, isNilpotent_iff] at H

Goal state after:
case refine_1
σ : Type u_1
R : Type u_2
inst✝ : CommRing R
P : MvPolynomial σ R
H✝ : IsUnit P
n : σ →₀ ℕ
hn : n ≠ 0
i : σ
hi : n i ≠ 0
e : Polynomial (MvPolynomial { b // b ≠ i } R) ≃ₐ[R] MvPolynomial σ R :=
  (optionEquivLeft R { b // b ≠ i }).symm.trans (renameEquiv R (Equiv.optionSubtypeNe i))
H : ∀ (i_1 : { b // ¬b = i } →₀ ℕ), IsNilpotent (coeff i_1 ((e.symm P).coeff (n i)))
⊢ IsNilpotent (coeff n P)
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 ↔ ∃ r, IsUnit r ∧ P = C r

Tactic:
rw [isUnit_iff_totalDegree_of_isReduced, totalDegree_eq_zero_iff_eq_C]
  refine ⟨fun H ↦ ⟨_, H⟩, ?_⟩
  rintro ⟨r, hr, rfl⟩
  simpa

Goal state after:
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).support.sup fun m ↦ (Finsupp.toMultiset m).card) =
    (f.support.sup fun m ↦ (Finsupp.toMultiset m).card) * p

Tactic:
support_expand _ (p.ne_zero_iff_zero_lt.mpr hp)

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
⊢ ((Finset.image (fun x ↦ p • x) f.support).sup fun m ↦ (Finsupp.toMultiset m).card) =
    (f.support.sup fun m ↦ (Finsupp.toMultiset m).card) * p
Module: Mathlib.Algebra.MvPolynomial.Funext

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : MvPolynomial (Fin 0) R
s : Fin 0 → Set R
hs : ∀ (i : Fin 0), (s i).Infinite
h : ∀ x ∈ Set.univ.pi s, (eval x) p = 0
⊢ p = 0

Tactic:
| zero =>

Goal state after:
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:
simp_rw [map_sub, h x hx, sub_self]

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

Goal state before:
pp: case zero
m : Multiset ℕ
⊢ (0 • m).multinomial = (Nat.multinomial (Finset.range 0) fun x ↦ m.sum) * m.multinomial ^ 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
⊢ ∀ (a b c : DegLex (α →₀ ℕ)), a < b → b < c → a < c

Tactic:
intro a

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a : DegLex (α →₀ ℕ)
⊢ ∀ (b c : DegLex (α →₀ ℕ)), a < b → b < c → a < c
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
⊢ m.degree 0 = 0

Tactic:
simp [degree]

Goal state after:
Module: Mathlib.Algebra.NonAssoc.LieAdmissible.Defs

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝¹ : CommRing R
inst✝ : LieAdmissibleRing L
x y z : L
⊢ ⁅x + y, z⁆ = ⁅x, z⁆ + ⁅y, z⁆

Tactic:
by
    simp only [Ring.lie_def, mul_add, add_mul]
    abel

Goal state after:
Module: Mathlib.Algebra.NonAssoc.LieAdmissible.Defs

Goal state before:
pp: R : Type u_1
L : Type u_2
inst✝¹ : CommRing R
inst✝ : LieAdmissibleRing L
x y z : L
⊢ ⁅x, y + z⁆ = ⁅x, y⁆ + ⁅x, z⁆

Tactic:
by
    simp only [Ring.lie_def, mul_add, add_mul]
    abel

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Nat

Goal state before:
pp: ⊢ ∀ {a b : ℕ}, DvdNotUnit a b → (if a = 0 then ⊤ else ↑a) < if b = 0 then ⊤ else ↑b

Tactic:
intro a

Goal state after:
a : ℕ
⊢ ∀ {b : ℕ}, DvdNotUnit a b → (if a = 0 then ⊤ else ↑a) < if b = 0 then ⊤ else ↑b
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case zero
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
⊢ m.toSyn (m.degree (f ^ 0)) ≤ m.toSyn (0 • m.degree f)

Tactic:
| zero =>

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

Goal state before:
pp: case zero
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
⊢ coeff (0 • m.degree f) (f ^ 0) = m.leadingCoeff f ^ 0

Tactic:
| zero =>

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
hn' : ∀ (p : ℕ), n.factorization p ≤ 1
⊢ ∀ (a : ℕ), List.count a n.primeFactorsList ≤ 1

Tactic:
intro a

Goal state after:
n : ℕ
hn : n ≠ 0
hn' : ∀ (p : ℕ), n.factorization p ≤ 1
a : ℕ
⊢ List.count a n.primeFactorsList ≤ 1
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

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

pp: σ✝ : Type u_1
m✝ : MonomialOrder σ✝
R✝ : Type u_2
inst✝² : CommSemiring R✝
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p p' q : MvPolynomial σ R
hp : p ≠ 0
h : m.toSyn (m.degree (p * q)) < m.toSyn (m.degree (p' * q))
hq : q ≠ 0
⊢ m.toSyn (m.degree p) < m.toSyn (m.degree p')

Tactic:
· simp [hq] at h

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

Goal state before:
pp: n : ℕ
h0 : n ≠ 0
⊢ ∀ (a : ℕ),
    a ∈ {d ∈ n.divisors | Squarefree d}.val ↔
      a ∈ Multiset.map (fun x ↦ x.val.prod) (normalizedFactors n).toFinset.powerset.val

Tactic:
intro a

Goal state after:
n : ℕ
h0 : n ≠ 0
a : ℕ
⊢ a ∈ {d ∈ n.divisors | Squarefree d}.val ↔
    a ∈ Multiset.map (fun x ↦ x.val.prod) (normalizedFactors n).toFinset.powerset.val
Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta

Goal state before:
pp: x : ℕ
⊢ ζ x = 0 ↔ x = 0

Tactic:
by simp [zeta]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : MulAction R M
f : ArithmeticFunction M
x : ℕ
⊢ (↑ζ • f) x = ∑ i ∈ x.divisors, f i

Tactic:
rw [smul_apply]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : MulAction R M
f : ArithmeticFunction M
x : ℕ
⊢ ∑ x ∈ x.divisorsAntidiagonal, ↑ζ x.1 • f x.2 = ∑ i ∈ x.divisors, f i
Module: Mathlib.NumberTheory.ArithmeticFunction.Zeta

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommSemiring R
f : ArithmeticFunction R
hf : f.IsMultiplicative
⊢ (f.ppow 0).IsMultiplicative

Tactic:
| zero =>

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

Goal state before:
pp: case mp
n : ℕ
⊢ (∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n) → ∃! p, Nat.Prime p ∧ p ∣ n

pp: case mpr
n : ℕ
⊢ (∃! p, Nat.Prime p ∧ p ∣ n) → ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n

Tactic:
· rintro ⟨p, k, hp, hk, rfl⟩
    refine ⟨p, ⟨hp, dvd_pow_self _ hk.ne'⟩, ?_⟩
    rintro q ⟨hq, hq'⟩
    exact (Nat.prime_dvd_prime_iff_eq hq hp).1 (hq.dvd_of_dvd_pow hq')

Goal state after:
case mpr
n : ℕ
⊢ (∃! p, Nat.Prime p ∧ p ∣ n) → ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: case zero
h : Ω 0 = 1
⊢ Nat.Prime 0

Tactic:
| zero =>

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

Goal state before:
pp: case neg.zero
m : ℕ
hm : ¬m = 0
⊢ Ω (m ^ 0) = 0 * Ω m

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: case e'_3
d n : ℕ
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : f ∈ n.primeFactors.pi fun x ↦ univ
g : (p : ℕ) → p ∈ n.primeFactors → Fin d
hg : g ∈ n.primeFactors.pi fun x ↦ univ
p : ℕ
hp : p ∈ n.primeFactors
hfg : f p hp ≠ g p hp
⊢ p = if f ↑⟨p, hp⟩ ⋯ = f p hp then ↑⟨p, hp⟩ else 1

Tactic:
rw [if_pos rfl]

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: n : ℕ
a : Fin 3 → ℕ
ha : a ∈ finMulAntidiag 3 n
b : Fin 3 → ℕ
hb : b ∈ finMulAntidiag 3 n
hfab : f a ha = f b hb
hfab1 : a 0 * a 1 = b 0 * b 1
hfab2 : a 0 * b 2 = b 0 * b 2
hprods : a 0 * a 1 * a 2 = a 0 * a 1 * b 2
hab2 : a 2 = b 2
⊢ a 0 = b 0

Tactic:
exact (mul_left_inj' <| ne_zero_of_mem_finMulAntidiag hb 2).mp hfab2

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

Goal state before:
pp: case e_a
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
g : ι → MvPolynomial σ R
b : ι
B : Finset ι
hb : b ∉ B
hb0 : ¬g b = 0
isunit_gb : IsUnit (m.leadingCoeff (g b))
hfd : m.toSyn (m.degree (g b + ∑ b ∈ B, g b)) < m.toSyn (m.degree (g b))
h :
  (∀ b_1 ∈ B, m.degree (g b_1) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g b_1)) ∨ g b_1 = 0) →
    m.toSyn (m.degree (∑ b ∈ B, g b)) < m.toSyn (m.degree (g b)) →
      ∃ c, ∑ b ∈ B, g b = ∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂)
hd : ∀ a ∈ B, m.degree (g a) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g a)) ∨ g a = 0
b' : ι
⊢ b' ∈ B → coeff (m.degree (g b')) (g b') = coeff (m.degree (g b)) (g b')

Tactic:
hb'

Goal state after:
case e_a
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
g : ι → MvPolynomial σ R
b : ι
B : Finset ι
hb : b ∉ B
hb0 : ¬g b = 0
isunit_gb : IsUnit (m.leadingCoeff (g b))
hfd : m.toSyn (m.degree (g b + ∑ b ∈ B, g b)) < m.toSyn (m.degree (g b))
h :
  (∀ b_1 ∈ B, m.degree (g b_1) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g b_1)) ∨ g b_1 = 0) →
    m.toSyn (m.degree (∑ b ∈ B, g b)) < m.toSyn (m.degree (g b)) →
      ∃ c, ∑ b ∈ B, g b = ∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂)
hd : ∀ a ∈ B, m.degree (g a) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g a)) ∨ g a = 0
b' : ι
hb' : b' ∈ B
⊢ coeff (m.degree (g b')) (g b') = coeff (m.degree (g b)) (g b')
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
g : ι → MvPolynomial σ R
b : ι
B : Finset ι
hb : b ∉ B
hb0 : ¬g b = 0
isunit_gb : IsUnit (m.leadingCoeff (g b))
hfd : m.toSyn (m.degree (g b + ∑ b ∈ B, g b)) < m.toSyn (m.degree (g b))
h :
  (∀ b_1 ∈ B, m.degree (g b_1) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g b_1)) ∨ g b_1 = 0) →
    m.toSyn (m.degree (∑ b ∈ B, g b)) < m.toSyn (m.degree (g b)) →
      ∃ c, ∑ b ∈ B, g b = ∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂)
hd : ∀ a ∈ B, m.degree (g a) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g a)) ∨ g a = 0
b' : ι
⊢ b' ∈ B → g b' - (m.leadingCoeff (g b') * ↑isunit_gb.unit⁻¹) • g b = ↑isunit_gb.unit⁻¹ • m.sPolynomial (g b') (g b)

Tactic:
hb'

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
g : ι → MvPolynomial σ R
b : ι
B : Finset ι
hb : b ∉ B
hb0 : ¬g b = 0
isunit_gb : IsUnit (m.leadingCoeff (g b))
hfd : m.toSyn (m.degree (g b + ∑ b ∈ B, g b)) < m.toSyn (m.degree (g b))
h :
  (∀ b_1 ∈ B, m.degree (g b_1) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g b_1)) ∨ g b_1 = 0) →
    m.toSyn (m.degree (∑ b ∈ B, g b)) < m.toSyn (m.degree (g b)) →
      ∃ c, ∑ b ∈ B, g b = ∑ b₁ ∈ B, ∑ b₂ ∈ B, c b₁ b₂ • m.sPolynomial (g b₁) (g b₂)
hd : ∀ a ∈ B, m.degree (g a) = m.degree (g b) ∧ IsUnit (m.leadingCoeff (g a)) ∨ g a = 0
b' : ι
hb' : b' ∈ B
⊢ g b' - (m.leadingCoeff (g b') * ↑isunit_gb.unit⁻¹) • g b = ↑isunit_gb.unit⁻¹ • m.sPolynomial (g b') (g b)
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
⊢ AntitoneOn mk (Set.Ici 1)

Tactic:
intro a

Goal state after:
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a : M
⊢ a ∈ Set.Ici 1 → ∀ ⦃b : M⦄, b ∈ Set.Ici 1 → a ≤ b → mk b ≤ mk a
Module: Mathlib.Algebra.Order.Archimedean.Class

Goal state before:
pp: M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
⊢ MonotoneOn mk (Set.Iic 1)

Tactic:
intro a

Goal state after:
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a : M
⊢ a ∈ Set.Iic 1 → ∀ ⦃b : M⦄, b ∈ Set.Iic 1 → a ≤ b → mk a ≤ mk b
Module: Mathlib.Algebra.Order.Disjointed

Goal state before:
pp: case neg
α : Type u_1
ι : Type u_2
inst✝⁵ : GeneralizedBooleanAlgebra α
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrderBot ι
inst✝² : Add ι
inst✝¹ : One ι
inst✝ : SuccAddOrder ι
f : ι → α
i : ι
hi : ¬IsMax i
⊢ (partialSups f) (succ i) = (partialSups f) i ⊔ disjointed f (succ i)

Tactic:
disjointed_succ _ hi

Goal state after:
case neg
α : Type u_1
ι : Type u_2
inst✝⁵ : GeneralizedBooleanAlgebra α
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrderBot ι
inst✝² : Add ι
inst✝¹ : One ι
inst✝ : SuccAddOrder ι
f : ι → α
i : ι
hi : ¬IsMax i
⊢ (partialSups f) (succ i) = (partialSups f) i ⊔ f (succ i) \ (partialSups f) i
Module: Mathlib.Algebra.Order.Disjointed

Goal state before:
pp: case zero
α : Type u_1
ι : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
f : ℕ → α
p : α → Sort u_3
hdiff : ⦃t : α⦄ → ⦃i : ℕ⦄ → p t → p (t \ f i)
n : ℕ
h : p (f (n + 1))
⊢ p (f (n + 1) \ (partialSups f) 0)

Tactic:
| zero =>

Goal state after:
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 α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | σ x ≠ x} ⊆ ↑s
⊢ ∑ i ∈ s, f (σ i) • g i ≤ ∑ i ∈ s, f i • g i

Tactic:
by
  convert!
    hfg.sum_smul_comp_perm_le_sum_smul
      (show {x | σ⁻¹ x ≠ x} ⊆ s by simp [set_support_symm_eq, hσ]) using 1
  exact σ.sum_comp' s (fun i j ↦ f i • g j) hσ

Goal state after: