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

Goal state before:
pp: case refine_2
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : NullMeasurableSet s volume
hs₂ : volume s ≠ ⊤
x✝¹ x✝ : ι → ℤ
h : x✝¹ ≠ x✝
⊢ Function.onFun (AEDisjoint volume) (fun ν ↦ ↑(box n ν) ∩ s) x✝¹ x✝

Tactic:
exact ((Disjoint.inter_right _ (disjoint.mp h)).inter_left _).aedisjoint

Goal state after:
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: case refine_2
ι : Type u_1
s : Set (ι → ℝ)
inst✝ : Finite ι
hs₁ : IsBounded s
hs₄ : ∀ ⦃x y : ℝ⦄, 0 < x → x ≤ y → x • s ⊆ y • s
x y : ℝ
hx : 0 < x
hy : x ≤ y
this : Fintype ι
⊢ x • s ∩ ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))) ⊆ y • s ∩ ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))

Tactic:
exact Set.inter_subset_inter_left _ <| hs₄ hx hy

Goal state after:
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
inst✝ : Fintype ι
I : Box ι
l : IntegrationParams
f₁ f₂ : (ι → ℝ) → E
vol₁ vol₂ : ι →ᵇᵃ[⊤] E →L[ℝ] F
hf : EqOn f₁ f₂ (Box.Icc I)
hvol : EqOn (⇑vol₁) (⇑vol₂) (Set.Iic I)
y : F
⊢ HasIntegral I l f₁ vol₁ y ↔ HasIntegral I l f₂ vol₂ y

Tactic:
by
  unfold HasIntegral
  refine Filter.tendsto_congr (fun π ↦ integralSum_congr hf (hvol.mono ?_))
  intro J hJ
  simp [π.le_of_mem' J hJ]

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.ProdL2

Goal state before:
pp: 𝕜 : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
E : Type u_4
F : Type u_5
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
x✝ : E
x y z : E ⧸ K
⊢ ⟪K.quotientEquivOrthogonal (x + y), K.quotientEquivOrthogonal z⟫_𝕜 =
    ⟪K.quotientEquivOrthogonal x, K.quotientEquivOrthogonal z⟫_𝕜 +
      ⟪K.quotientEquivOrthogonal y, K.quotientEquivOrthogonal z⟫_𝕜

Tactic:
rw [map_add, inner_add_left]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace

Goal state before:
pp: ι : Type u_1
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional ℝ F
n : ℕ
_i : Fact (finrank ℝ F = n)
o : Orientation ℝ F (Fin n)
b : OrthonormalBasis ι ℝ F
e : ι ≃ Fin n
⊢ ⇑b = ⇑(b.reindex e) ∘ ⇑e

Tactic:
ext x

Goal state after:
ι : Type u_1
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
inst✝³ : MeasurableSpace F
inst✝² : BorelSpace F
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional ℝ F
n : ℕ
_i : Fact (finrank ℝ F = n)
o : Orientation ℝ F (Fin n)
b : OrthonormalBasis ι ℝ F
e : ι ≃ Fin n
x : ι
⊢ b x = (⇑(b.reindex e) ∘ ⇑e) x
Module: Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace

Goal state before:
pp: case e'_5
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : FiniteDimensional ℝ E
h : finrank ℝ E = 1
v : E
hv : v ≠ 0
hv' : ℝ ∙ ‖v‖⁻¹ • v = ⊤
f : ℝ ≃ₗᵢ[ℝ] E :=
  (LinearIsometryEquiv.toSpanUnitSingleton (‖v‖⁻¹ • v) ⋯).trans (LinearIsometryEquiv.ofTop E (ℝ ∙ ‖v‖⁻¹ • v) hv')
⊢ ((fun x ↦ x • v) ∘ fun x ↦ ‖v‖⁻¹ • x) = ⇑f

Tactic:
ext x

Goal state after:
case e'_5
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : FiniteDimensional ℝ E
h : finrank ℝ E = 1
v : E
hv : v ≠ 0
hv' : ℝ ∙ ‖v‖⁻¹ • v = ⊤
f : ℝ ≃ₗᵢ[ℝ] E :=
  (LinearIsometryEquiv.toSpanUnitSingleton (‖v‖⁻¹ • v) ⋯).trans (LinearIsometryEquiv.ofTop E (ℝ ∙ ‖v‖⁻¹ • v) hv')
x : ℝ
⊢ ((fun x ↦ x • v) ∘ fun x ↦ ‖v‖⁻¹ • x) x = f x
Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝¹ : NormedField 𝕜
inst✝ : Norm E
a : 𝕜
f : 𝕜 → E
h : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝[≠] a) (norm ∘ f)
⊢ f =o[𝓝[≠] a] fun x ↦ (x - a)⁻¹

Tactic:
refine (h.isBigO_const (one_ne_zero' ℝ)).trans_isLittleO (isLittleO_const_left.2 <| Or.inr ?_)

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝¹ : NormedField 𝕜
inst✝ : Norm E
a : 𝕜
f : 𝕜 → E
h : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝[≠] a) (norm ∘ f)
⊢ Tendsto (norm ∘ fun x ↦ (x - a)⁻¹) (𝓝[≠] a) atTop
Module: Mathlib.Algebra.Module.ZLattice.Covolume

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
ι : Type u_2
inst✝ : Fintype ι
X : Set E
hX : ∀ ⦃x : E⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
F : E → ℝ
hF₁ : ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ card ι * F x
c : ℝ
hc : 0 < c
⊢ c • {x | x ∈ X ∧ F x ≤ 1} = {x | x ∈ X ∧ F x ≤ c ^ card ι}

Tactic:
ext x

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
ι : Type u_2
inst✝ : Fintype ι
X : Set E
hX : ∀ ⦃x : E⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X
F : E → ℝ
hF₁ : ∀ (x : E) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ card ι * F x
c : ℝ
hc : 0 < c
x : E
⊢ x ∈ c • {x | x ∈ X ∧ F x ≤ 1} ↔ x ∈ {x | x ∈ X ∧ F x ≤ c ^ card ι}
Module: Mathlib.Algebra.Module.ZLattice.Summable

Goal state before:
pp: case inl
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
h✝ : Subsingleton ↥L
⊢ ∃ A > 0,
    ∀ r < -↑(finrank ℤ ↥L), ∀ (s : Finset ↥L), ∑ z ∈ s, ‖z‖ ^ r ≤ A ^ r * ∑' (k : ℕ), ↑k ^ (↑(finrank ℤ ↥L) - 1 + r)

Tactic:
refine ⟨1, zero_lt_one, fun r hr s ↦ ?_⟩

Goal state after:
case inl
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
h✝ : Subsingleton ↥L
r : ℝ
hr : r < -↑(finrank ℤ ↥L)
s : Finset ↥L
⊢ ∑ z ∈ s, ‖z‖ ^ r ≤ 1 ^ r * ∑' (k : ℕ), ↑k ^ (↑(finrank ℤ ↥L) - 1 + r)
Module: Mathlib.Algebra.MvPolynomial.Division

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
j : σ →₀ ℕ
r : R
⊢ (r = 0 ∨ Finsupp.single i 1 ≤ j) ∧ True ↔ r = 0 ∨ j i ≠ 0

Tactic:
and_true,

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
i : σ
j : σ →₀ ℕ
r : R
⊢ r = 0 ∨ Finsupp.single i 1 ≤ j ↔ r = 0 ∨ j i ≠ 0
Module: Mathlib.Algebra.MvPolynomial.Nilpotent

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommRing R
P : MvPolynomial σ R
x✝ : IsUnit (coeff 0 P) ∧ ∀ (i : σ →₀ ℕ), i ≠ 0 → IsNilpotent (coeff i P)
h₁ : IsUnit (coeff 0 P)
h₂ : ∀ (i : σ →₀ ℕ), i ≠ 0 → IsNilpotent (coeff i P)
⊢ IsNilpotent (P - C (coeff 0 P))

Tactic:
simp +contextual [isNilpotent_iff, apply_ite, eq_comm, h₂]

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

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

Tactic:
simp [hp]

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

Goal state before:
pp: case mul_X
R : Type u_1
S : Type u_2
σ : Type u_3
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
x : S
f : R →+* Polynomial S
g : σ → Polynomial S
p✝ p : MvPolynomial σ R
n : σ
hp : Polynomial.eval x (eval₂ f g p) = eval₂ ((Polynomial.evalRingHom x).comp f) (fun s ↦ Polynomial.eval x (g s)) p
⊢ Polynomial.eval x (eval₂ f g (p * X n)) =
    eval₂ ((Polynomial.evalRingHom x).comp f) (fun s ↦ Polynomial.eval x (g s)) (p * X n)

Tactic:
simp [hp]

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

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝ : LinearOrder α
a b c : DegLex (α →₀ ℕ)
hab : degree (ofDegLex a) = degree (ofDegLex b) ∧ toLex (ofDegLex a) < toLex (ofDegLex b)
hbc : degree (ofDegLex b) = degree (ofDegLex c) ∧ toLex (ofDegLex b) < toLex (ofDegLex c)
⊢ degree (ofDegLex a) = degree (ofDegLex c) ∧ toLex (ofDegLex a) < toLex (ofDegLex c)

Tactic:
exact ⟨Eq.trans hab.1 hbc.1, lt_trans hab.2 hbc.2⟩

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

Goal state before:
pp: case pos
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:
simp [hp]

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : DegLex (α →₀ ℕ)
h : a ≤ b
c : DegLex (α →₀ ℕ)
⊢ a + c ≤ b + c

Tactic:
le_iff

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b : DegLex (α →₀ ℕ)
h :
  degree (ofDegLex a) < degree (ofDegLex b) ∨
    degree (ofDegLex a) = degree (ofDegLex b) ∧ toLex (ofDegLex a) ≤ toLex (ofDegLex b)
c : DegLex (α →₀ ℕ)
⊢ degree (ofDegLex (a + c)) < degree (ofDegLex (b + c)) ∨
    degree (ofDegLex (a + c)) = degree (ofDegLex (b + c)) ∧ toLex (ofDegLex (a + c)) ≤ toLex (ofDegLex (b + c))
Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : DegLex (α →₀ ℕ)
h : a + b ≤ a + c
⊢ b ≤ c

Tactic:
le_iff

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b c : DegLex (α →₀ ℕ)
h :
  degree (ofDegLex (a + b)) < degree (ofDegLex (a + c)) ∨
    degree (ofDegLex (a + b)) = degree (ofDegLex (a + c)) ∧ toLex (ofDegLex (a + b)) ≤ toLex (ofDegLex (a + c))
⊢ degree (ofDegLex b) < degree (ofDegLex c) ∨
    degree (ofDegLex b) = degree (ofDegLex c) ∧ toLex (ofDegLex b) ≤ toLex (ofDegLex c)
Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
x y : DegLex (α →₀ ℕ)
⊢ x ≤ y → (fun x ↦ degree (ofDegLex x)) x ≤ (fun x ↦ degree (ofDegLex x)) y

Tactic:
le_iff

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
x y : DegLex (α →₀ ℕ)
⊢ degree (ofDegLex x) < degree (ofDegLex y) ∨
      degree (ofDegLex x) = degree (ofDegLex y) ∧ toLex (ofDegLex x) ≤ toLex (ofDegLex y) →
    (fun x ↦ degree (ofDegLex x)) x ≤ (fun x ↦ degree (ofDegLex x)) y
Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex

Goal state before:
pp: case neg
α : Type u_1
σ : Type u_2
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
a b : σ →₀ ℕ
h : a ≤ b
ha : degree b ≤ degree a
⊢ degree a ≤ degree b

Tactic:
rw [← add_tsub_cancel_of_le h, map_add]

Goal state after:
case neg
α : Type u_1
σ : Type u_2
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
a b : σ →₀ ℕ
h : a ≤ b
ha : degree b ≤ degree a
⊢ degree a ≤ degree a + degree (b - a)
Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex

Goal state before:
pp: α : Type u_1
⊢ degLex.toSyn (single 1 1) < degLex.toSyn (single 0 1)

Tactic:
degLex_lt_iff,

Goal state after:
α : Type u_1
⊢ toDegLex (single 1 1) < toDegLex (single 0 1)
Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex

Goal state before:
pp: α : Type u_1
⊢ degLex.toSyn (single 0 1 + single 1 1) < degLex.toSyn (single 0 2)

Tactic:
degLex_lt_iff,

Goal state after:
α : Type u_1
⊢ toDegLex (single 0 1 + single 1 1) < toDegLex (single 0 2)
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
h : m.toSyn (m.degree f) < m.toSyn (m.degree g)
⊢ m.degree (f + g) = m.degree g

Tactic:
by
  rw [add_comm]
  exact degree_add_of_lt h

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

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : IsReduced R
f : MvPolynomial σ R
n : ℕ
⊢ m.leadingCoeff (f ^ n) = m.leadingCoeff f ^ n

Tactic:
by
  rw [leadingCoeff, degree_pow, coeff_pow_nsmul_degree]

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

Goal state before:
pp: n p : ℕ
hn : Squarefree n
⊢ n.factorization p ≤ 1

Tactic:
by
  rcases eq_or_ne n 0 with (rfl | hn')
  · simp
  rw [squarefree_iff_emultiplicity_le_one] at hn
  by_cases hp : p.Prime
  · have := hn p
    rw [← multiplicity_eq_factorization hp hn']
    simp only [Nat.isUnit_iff, hp.ne_one, or_false] at this
    exact multiplicity_le_of_emultiplicity_le this
  · rw [factorization_eq_zero_of_not_prime _ hp]
    exact zero_le_one

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

Goal state before:
pp: n k : ℕ
hn : n ≠ 1
hk : k ≠ 0
h : Squarefree (n ^ k)
h₁ : ¬k = 1
this : 2 ≤ k
⊢ n * n ∣ n ^ k

Tactic:
rw [← sq]

Goal state after:
n k : ℕ
hn : n ≠ 1
hk : k ≠ 0
h : Squarefree (n ^ k)
h₁ : ¬k = 1
this : 2 ≤ k
⊢ n ^ 2 ∣ n ^ k
Module: Mathlib.Data.Nat.Squarefree

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

Tactic:
Finset.mem_powerset,

Goal state after:
case mpr
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s ⊆ (normalizedFactors n).toFinset
⊢ (s.val.prod ∣ n ∧ n ≠ 0) ∧ Squarefree s.val.prod
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case mpr
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ (normalizedFactors n).dedup
hs0 : s.val.prod ≠ 0
h : Multiset.Rel Associated (normalizedFactors s.val.prod) s.val
⊢ Squarefree s.val.prod

Tactic:
rw [associated_eq_eq, Multiset.rel_eq] at h

Goal state after:
case mpr
n : ℕ
h0 : n ≠ 0
s : Finset ℕ
hs : s.val ≤ (normalizedFactors n).dedup
hs0 : s.val.prod ≠ 0
h : normalizedFactors s.val.prod = s.val
⊢ Squarefree s.val.prod
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:
simp_rw [h]
    revert f g
    simp [m.withBotDegree_eq, m.degree_zero]

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

Goal state before:
pp: case neg.inr
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
h : g = 0
⊢ m.withBotDegree f = m.withBotDegree g ↔ m.degree f = m.degree g ∧ (f = 0 ↔ g = 0)

Tactic:
simp_rw [h]
    revert f g
    simp [m.withBotDegree_eq, m.degree_zero]

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

Goal state before:
pp: n : ℕ
h0 : n ≠ 0
α : Type u_1
inst✝ : AddCommMonoid α
f : ℕ → α
⊢ ∑ d ∈ n.divisors with Squarefree d, f d = ∑ i ∈ (normalizedFactors n).toFinset.powerset, f i.val.prod

Tactic:
by
  rw [Finset.sum_eq_multiset_sum, divisors_filter_squarefree h0, Multiset.map_map,
    Finset.sum_eq_multiset_sum]
  rfl

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

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

Tactic:
ext x

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✝ : NonAssocSemiring R
f : ArithmeticFunction R
⊢ f.pmul ↑ζ = f

Tactic:
ext x

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

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

Tactic:
ext x

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

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

Tactic:
ext x

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

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

Tactic:
ext x

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
⊢ 1 • b = b

Tactic:
ext x

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : ArithmeticFunction M
x : ℕ
⊢ (1 • b) x = b x
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

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

Tactic:
ext x

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

Goal state before:
pp: case insert
R : Type u_1
ι : Type u_2
inst✝ : CommMonoidWithZero R
g : ι → ℕ
f : ArithmeticFunction R
hf : f.IsMultiplicative
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
ih : (↑s✝).Pairwise (Coprime on g) → f (∏ i ∈ s✝, g i) = ∏ i ∈ s✝, f (g i)
hs : (insert a✝ ↑s✝).Pairwise (Coprime on g)
⊢ f (∏ i ∈ insert a✝ s✝, g i) = ∏ i ∈ insert a✝ s✝, f (g i)

Tactic:
Set.pairwise_insert_of_symm

Goal state after:
case insert
R : Type u_1
ι : Type u_2
inst✝ : CommMonoidWithZero R
g : ι → ℕ
f : ArithmeticFunction R
hf : f.IsMultiplicative
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
ih : (↑s✝).Pairwise (Coprime on g) → f (∏ i ∈ s✝, g i) = ∏ i ∈ s✝, f (g i)
hs : (↑s✝).Pairwise (Coprime on g) ∧ ∀ b ∈ ↑s✝, a✝ ≠ b → (Coprime on g) a✝ b
⊢ f (∏ i ∈ insert a✝ s✝, g i) = ∏ i ∈ insert a✝ s✝, f (g i)
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: R : Type u_1
inst✝ : CommMonoidWithZero R
f : ℕ → R
x y : ℕ
hx : ¬x = 0
hy : ¬y = 0
hxy : x.Coprime y
hxy₀ : x * y ≠ 0
⊢ ∏ p ∈ (x * y).primeFactors, f p = (∏ p ∈ x.primeFactors, f p) * (ArithmeticFunction.prodPrimeFactors f) y

Tactic:
prodPrimeFactors_apply hy,

Goal state after:
R : Type u_1
inst✝ : CommMonoidWithZero R
f : ℕ → R
x y : ℕ
hx : ¬x = 0
hy : ¬y = 0
hxy : x.Coprime y
hxy₀ : x * y ≠ 0
⊢ ∏ p ∈ (x * y).primeFactors, f p = (∏ p ∈ x.primeFactors, f p) * ∏ p ∈ y.primeFactors, f p
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: k n : ℕ
⊢ (σ k) n = 0 ↔ n = 0

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Goal state after:
case inl
k : ℕ
⊢ (σ k) 0 = 0 ↔ 0 = 0

case inr
k n : ℕ
hn : n ≠ 0
⊢ (σ k) n = 0 ↔ n = 0
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: divisorsAntidiagonal : ℕ+ → Finset (ℕ+ × ℕ+) :=
  fun n ↦ map { toFun := fun x ↦ (⟨(↑x).1, ⋯⟩, ⟨(↑x).2, ⋯⟩), inj' := ⋯ } (↑n).divisorsAntidiagonal.attach
n : ℕ+
x : ℕ+ × ℕ+
⊢ (∃ a, True ∧ (⟨(↑a).1, ⋯⟩, ⟨(↑a).2, ⋯⟩) = x) ↔ x.1 * x.2 = n

Tactic:
Prod.ext_iff,

Goal state after:
divisorsAntidiagonal : ℕ+ → Finset (ℕ+ × ℕ+) :=
  fun n ↦ map { toFun := fun x ↦ (⟨(↑x).1, ⋯⟩, ⟨(↑x).2, ⋯⟩), inj' := ⋯ } (↑n).divisorsAntidiagonal.attach
n : ℕ+
x : ℕ+ × ℕ+
⊢ (∃ a, True ∧ ⟨(↑a).1, ⋯⟩ = x.1 ∧ ⟨(↑a).2, ⋯⟩ = x.2) ↔ x.1 * x.2 = n
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: n : ℕ
⊢ #n.divisors = 1 ↔ n = 1

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Goal state after:
case inl
⊢ #(divisors 0) = 1 ↔ 0 = 1

case inr
n : ℕ
hn : n ≠ 0
⊢ #n.divisors = 1 ↔ n = 1
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

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

Tactic:
simp at h

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

Goal state before:
pp: n : ℕ
⊢ image (⇑(piFinTwoEquiv fun x ↦ ℕ)) (finMulAntidiag 2 n) = n.divisorsAntidiagonal

Tactic:
ext x

Goal state after:
n : ℕ
x : ℕ × ℕ
⊢ x ∈ image (⇑(piFinTwoEquiv fun x ↦ ℕ)) (finMulAntidiag 2 n) ↔ x ∈ n.divisorsAntidiagonal
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ✝ : Type u_1
m✝ : MonomialOrder σ✝
R✝ : Type u_2
inst✝² : CommRing R✝
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p₁ p₂ : MvPolynomial σ R
d₁ d₂ : σ →₀ ℕ
c₁ c₂ : R
hc1 : c₁ ≠ 0
hc2 : c₂ ≠ 0
hp1 : p₁ ≠ 0
hp2 : p₂ ≠ 0
hm1 : ¬(monomial d₁) c₁ = 0
hm2 : ¬(monomial d₂) c₂ = 0
⊢ (monomial
            (((if c₁ = 0 then 0 else d₁) + m.degree p₁) ⊔ ((if c₂ = 0 then 0 else d₂) + m.degree p₂) -
                ((if c₁ = 0 then 0 else d₁) + m.degree p₁) +
              d₁))
          (c₂ * m.leadingCoeff p₂ * c₁) *
        p₁ -
      (monomial
            (((if c₁ = 0 then 0 else d₁) + m.degree p₁) ⊔ ((if c₂ = 0 then 0 else d₂) + m.degree p₂) -
                ((if c₂ = 0 then 0 else d₂) + m.degree p₂) +
              d₂))
          (c₁ * m.leadingCoeff p₁ * c₂) *
        p₂ =
    (monomial
            ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - m.degree p₁ ⊔ m.degree p₂ +
              (m.degree p₁ ⊔ m.degree p₂ - m.degree p₁)))
          (c₁ * c₂ * m.leadingCoeff p₂) *
        p₁ -
      (monomial
            ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - m.degree p₁ ⊔ m.degree p₂ +
              (m.degree p₁ ⊔ m.degree p₂ - m.degree p₂)))
          (c₁ * c₂ * m.leadingCoeff p₁) *
        p₂

Tactic:
hc1,

Goal state after:
σ✝ : Type u_1
m✝ : MonomialOrder σ✝
R✝ : Type u_2
inst✝² : CommRing R✝
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p₁ p₂ : MvPolynomial σ R
d₁ d₂ : σ →₀ ℕ
c₁ c₂ : R
hc1 : c₁ ≠ 0
hc2 : c₂ ≠ 0
hp1 : p₁ ≠ 0
hp2 : p₂ ≠ 0
hm1 : ¬(monomial d₁) c₁ = 0
hm2 : ¬(monomial d₂) c₂ = 0
⊢ (monomial
            (((if False then 0 else d₁) + m.degree p₁) ⊔ ((if c₂ = 0 then 0 else d₂) + m.degree p₂) -
                ((if False then 0 else d₁) + m.degree p₁) +
              d₁))
          (c₂ * m.leadingCoeff p₂ * c₁) *
        p₁ -
      (monomial
            (((if False then 0 else d₁) + m.degree p₁) ⊔ ((if c₂ = 0 then 0 else d₂) + m.degree p₂) -
                ((if c₂ = 0 then 0 else d₂) + m.degree p₂) +
              d₂))
          (c₁ * m.leadingCoeff p₁ * c₂) *
        p₂ =
    (monomial
            ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - m.degree p₁ ⊔ m.degree p₂ +
              (m.degree p₁ ⊔ m.degree p₂ - m.degree p₁)))
          (c₁ * c₂ * m.leadingCoeff p₂) *
        p₁ -
      (monomial
            ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - m.degree p₁ ⊔ m.degree p₂ +
              (m.degree p₁ ⊔ m.degree p₂ - m.degree p₂)))
          (c₁ * c₂ * m.leadingCoeff p₁) *
        p₂
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 * a 2 = b 0 * b 2
hprods : a 0 * a 1 * a 2 = a 0 * a 1 * b 2
hab2 : a 2 = b 2
hab0 : a 0 = b 0
⊢ a 1 = b 1

Tactic:
rw [hab0] at hfab1

Goal state after:
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 : b 0 * a 1 = b 0 * b 1
hfab2 : a 0 * a 2 = b 0 * b 2
hprods : a 0 * a 1 * a 2 = a 0 * a 1 * b 2
hab2 : a 2 = b 2
hab0 : a 0 = b 0
⊢ a 1 = b 1
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p₁ p₂ : MvPolynomial σ R
d₁ d₂ : σ →₀ ℕ
c₁ c₂ : R
⊢ m.sPolynomial ((monomial d₁) c₁ * p₁) ((monomial d₂) c₂ * p₂) =
    (monomial ((d₁ + m.degree p₁) ⊔ (d₂ + m.degree p₂) - m.degree p₁ ⊔ m.degree p₂)) (c₁ * c₂) * m.sPolynomial p₁ p₂

Tactic:
classical
  simp only [sPolynomial_def]
  wlog! +distrib H : c₁ ≠ 0 ∧ c₂ ≠ 0 ∧ p₁ ≠ 0 ∧ p₂ ≠ 0
  · (obtain rfl | rfl | rfl | rfl := H) <;> simp
  rcases H with ⟨hc1, hc2, hp1, hp2⟩
  have hm1 := (monomial_eq_zero (s := d₁)).not.mpr hc1
  have hm2 := (monomial_eq_zero (s := d₂)).not.mpr hc2
  simp_rw [m.degree_mul hm1 hp1, m.degree_mul hm2 hp2,
    mul_sub, ← mul_assoc _ _ p₁, ← mul_assoc _ _ p₂, monomial_mul,
    m.leadingCoeff_mul, m.leadingCoeff_monomial,
    degree_monomial, hc1, hc2, reduceIte, mul_right_comm, mul_comm c₂ c₁]
  rw [tsub_add_tsub_cancel (sup_le_sup (self_le_add_left _ _) (self_le_add_left _ _)) (by simp),
    tsub_add_tsub_cancel (sup_le_sup (self_le_add_left _ _) (self_le_add_left _ _)) (by simp),
    tsub_add_eq_add_tsub le_sup_left, tsub_add_eq_add_tsub le_sup_right,
    add_comm d₁, add_comm d₂, add_tsub_add_eq_tsub_right, add_tsub_add_eq_tsub_right]

Goal state after: