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

Goal state before:
pp: ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ (∃ i_1, update I.upper i (min x (I.upper i)) i_1 ≤ I.lower i_1) ↔ x ≤ I.lower i

Tactic:
exists_update_iff I.upper fun j y => y ≤ I.lower j

Goal state after:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ (min x (I.upper i) ≤ I.lower i ∨ ∃ x, x ≠ i ∧ I.upper x ≤ I.lower x) ↔ x ≤ I.lower i
Module: Mathlib.Analysis.BoxIntegral.Partition.Split

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : AddCommMonoid M
I : Box ι
i : ι
x : ℝ
f : Box ι → M
⊢ ∑ J ∈ (split I i x).boxes, f J = Option.elim' 0 f (I.splitLower i x) + Option.elim' 0 f (I.splitUpper i x)

Tactic:
split,

Goal state after:
ι : Type u_1
M : Type u_3
inst✝ : AddCommMonoid M
I : Box ι
i : ι
x : ℝ
f : Box ι → M
⊢ ∑ J ∈ (ofWithBot {I.splitLower i x, I.splitUpper i x} ⋯ ⋯).boxes, f J =
    Option.elim' 0 f (I.splitLower i x) + Option.elim' 0 f (I.splitUpper i x)
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst✝⁶ : RCLike 𝕜
E : Type u_4
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : Fintype ι
E' : Type u_7
inst✝² : Fintype ι'
inst✝¹ : NormedAddCommGroup E'
inst✝ : InnerProductSpace 𝕜 E'
b : OrthonormalBasis ι 𝕜 E
b' : OrthonormalBasis ι' 𝕜 E'
e : ι ≃ ι'
⊢ (b.equiv b' e).symm = b'.equiv b e.symm

Tactic:
apply b'.toBasis.ext_linearIsometryEquiv
  simp [OrthonormalBasis.equiv]

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a b : OrthonormalBasis ι 𝕜 E
this : ↑‖(a.toBasis.toMatrix ⇑b).det‖ ^ 2 = 1
⊢ ‖a.toBasis.det ⇑b‖ = 1

Tactic:
norm_cast at this

Goal state after:
ι : Type u_1
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
a b : OrthonormalBasis ι 𝕜 E
this : ‖(a.toBasis.toMatrix ⇑b).det‖ ^ 2 = 1
⊢ ‖a.toBasis.det ⇑b‖ = 1
Module: Mathlib.Analysis.Oscillation

Goal state before:
pp: E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : PseudoEMetricSpace E
K : Set E
f : E → F
D : Set E
ε : ℝ≥0∞
comp : IsCompact K
hK : ∀ x ∈ K, oscillationWithin f D x < ε
S : ℝ → Set E := fun r ↦ {x | ∃ a > r, ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε}
⊢ ∀ r > 0, IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (S r)

Tactic:
refine fun r _ ↦ EMetric.isOpen_iff.mpr fun x ⟨a, ar, ha⟩ ↦
      ⟨ENNReal.ofReal ((a - r) / 2), by simp [ar], ?_⟩

Goal state after:
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : PseudoEMetricSpace E
K : Set E
f : E → F
D : Set E
ε : ℝ≥0∞
comp : IsCompact K
hK : ∀ x ∈ K, oscillationWithin f D x < ε
S : ℝ → Set E := fun r ↦ {x | ∃ a > r, ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε}
r : ℝ
x✝¹ : r > 0
x : E
x✝ : x ∈ S r
a : ℝ
ar : a > r
ha : ediam (f '' (eball x (ENNReal.ofReal a) ∩ D)) ≤ ε
⊢ eball x (ENNReal.ofReal ((a - r) / 2)) ⊆ S r
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst✝ : Fintype ι
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ⊆ ↑B
this : Fintype ↑(s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))
⊢ ∑ i ∈ (s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))).toFinset, F i / ↑n ^ card ι =
    ∑ x ∈ (prepartition n B).boxes,
      if (prepartition n B).tag x ∈ s then volume.real ↑x • F ((prepartition n B).tag x) else volume.real ↑x • 0

Tactic:
smul_eq_mul,

Goal state after:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
s : Set (ι → ℝ)
F : (ι → ℝ) → ℝ
inst✝ : Fintype ι
B : Box ι
hB : hasIntegralVertices B
hs₀ : s ⊆ ↑B
this : Fintype ↑(s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))))
⊢ ∑ i ∈ (s ∩ (↑n)⁻¹ • ↑(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))).toFinset, F i / ↑n ^ card ι =
    ∑ x ∈ (prepartition n B).boxes,
      if (prepartition n B).tag x ∈ s then volume.real ↑x * F ((prepartition n B).tag x) else volume.real ↑x * 0
Module: Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
n : ι
h₀ : LinearIndependent 𝕜 (f ∘ Subtype.val)
h : gramSchmidt 𝕜 f n = 0
h₁ : f n ∈ span 𝕜 (f '' Set.Iio n)
h₂ : (f ∘ Subtype.val) ⟨n, ⋯⟩ ∈ span 𝕜 (f ∘ Subtype.val '' Set.Iio ⟨n, ⋯⟩)
⊢ ⟨n, ⋯⟩ ∉ Set.Iio ⟨n, ⋯⟩

Tactic:
simp only [Set.mem_Iio, lt_self_iff_false, not_false_iff]

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

Goal state before:
pp: case e'_5
ι : Type u_1
s : Set (ι → ℝ)
inst✝ : Fintype ι
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
⊢ volume.real s = volume.real s • 1

Tactic:
smul_eq_mul,

Goal state after:
case e'_5
ι : Type u_1
s : Set (ι → ℝ)
inst✝ : Fintype ι
hs₁ : Bornology.IsBounded s
hs₂ : MeasurableSet s
hs₃ : volume (frontier s) = 0
⊢ volume.real s = volume.real s * 1
Module: Mathlib.LinearAlgebra.Orientation

Goal state before:
pp: case intro.h
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_4
inst✝ : Finite ι
e : Basis ι R M
f : M ≃ₗ[R] M
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
g : M [⋀^ι]→ₗ[R] R
hg : g ≠ 0
⊢ SameRay R ((g ⇑e • LinearMap.det ↑f.symm) • e.det) (↑(LinearEquiv.det f)⁻¹ • g ⇑e • e.det)

Tactic:
smul_eq_mul,

Goal state after:
case intro.h
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : PartialOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_4
inst✝ : Finite ι
e : Basis ι R M
f : M ≃ₗ[R] M
val✝ : Fintype ι
this : DecidableEq ι := Classical.decEq ι
g : M [⋀^ι]→ₗ[R] R
hg : g ≠ 0
⊢ SameRay R ((g ⇑e * LinearMap.det ↑f.symm) • e.det) (↑(LinearEquiv.det f)⁻¹ • g ⇑e • e.det)
Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
u : ℕ → E
l : E
h : Tendsto u atTop (𝓝 l)
this : (fun n ↦ ∑ i ∈ Finset.range n, (u i - l)) =o[atTop] fun n ↦ ↑n
n : ℕ
npos : n ∈ Set.Ici 1
nposℝ : 0 < ↑n
⊢ (↑n)⁻¹ • ↑n = 1

Tactic:
smul_eq_mul,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
u : ℕ → E
l : E
h : Tendsto u atTop (𝓝 l)
this : (fun n ↦ ∑ i ∈ Finset.range n, (u i - l)) =o[atTop] fun n ↦ ↑n
n : ℕ
npos : n ∈ Set.Ici 1
nposℝ : 0 < ↑n
⊢ (↑n)⁻¹ * ↑n = 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
b : Basis ι ℤ ↥L
x : ↥L
n : ℕ
hxn : ‖x‖ < normBound b * ↑n
i : ι
⊢ (normBound b)⁻¹ * ‖x‖ < ↑↑n

Tactic:
inv_mul_lt_iff₀ (normBound_pos b)

Goal state after:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
ι : Type u_3
b : Basis ι ℤ ↥L
x : ↥L
n : ℕ
hxn : ‖x‖ < normBound b * ↑n
i : ι
⊢ ‖x‖ < normBound b * ↑↑n
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
k : ℕ
⊢ (↑(k + 1) + 1 - -↑(k + 1)).toNat ^ #univ - (↑k + 1 - -↑k).toNat ^ #univ ≤ 2 * d * (2 * k + 3) ^ (d - 1)

Tactic:
grind [abs_pow_sub_pow_le (α := ℤ) (2 * k + 3) (2 * k + 1) d]

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

Goal state before:
pp: case h
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
v : ι → ℤ
hv : v ∈ s (k + 1) \ s k
j : ι
hj : v j ∉ Icc (-↑k) ↑k
⊢ ↑k + 1 ≤ |v j|

Tactic:
by_contra! H

Goal state after:
case h
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
v : ι → ℤ
hv : v ∈ s (k + 1) \ s k
j : ι
hj : v j ∉ Icc (-↑k) ↑k
H : |v j| < ↑k + 1
⊢ False
Module: Mathlib.Algebra.MvPolynomial.Comap

Goal state before:
pp: σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
i : σ
⊢ comap (g.comp f) x i = (aeval x) ((aeval fun i ↦ g (X i)) (f (X i)))

Tactic:
apply eval₂Hom_congr rfl rfl

Goal state after:
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
i : σ
⊢ (g.comp f) (X i) = (aeval fun i ↦ g (X i)) (f (X i))
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: α : Type u_1
s : Finset α
f : α → ℕ
a : α
inst✝ : DecidableEq α
h : a ∉ s
h₁ : f a = 1
⊢ (∑ x ∈ s, f x + 1) * (∑ x ∈ s, f x)! / ∏ x ∈ s, (f x)! = (s.sum f + 1) * ((∑ x ∈ s, f x)! / ∏ x ∈ s, (f x)!)

Tactic:
rw [Nat.mul_div_assoc _ (prod_factorial_dvd_factorial_sum _ _)]

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

Goal state before:
pp: case cons
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
f✝ : α → R
a : α
s : Finset α
has : a ∉ s
ih :
  ∀ (hc : (↑s).Pairwise (Commute on f✝)) (n : ℕ),
    (∑ i ∈ s, f✝ i) ^ n = ∑ k ∈ s.piAntidiag n, ↑(multinomial s k) * s.noncommProd (fun i ↦ f✝ i ^ k i) ⋯
hc : (↑(cons a s has)).Pairwise (Commute on f✝)
n : ℕ
p : ℕ × ℕ
hp : p ∈ antidiagonal n
f : α → ℕ
hf : f ∈ s.piAntidiag p.2
⊢ ↑((f a + p.1 + s.sum f).choose (f a + p.1)) * ↑(multinomial s (f + fun i ↦ if i = a then p.1 else 0)) *
      (f✝ a ^ (f a + p.1) * s.noncommProd (fun i ↦ f✝ i ^ (f i + if i = a then p.1 else 0)) ⋯) =
    ↑(n.choose p.1) * ↑(multinomial s f) * (f✝ a ^ p.1 * s.noncommProd (fun i ↦ f✝ i ^ f i) ⋯)

Tactic:
rw [mem_piAntidiag] at hf

Goal state after:
case cons
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
f✝ : α → R
a : α
s : Finset α
has : a ∉ s
ih :
  ∀ (hc : (↑s).Pairwise (Commute on f✝)) (n : ℕ),
    (∑ i ∈ s, f✝ i) ^ n = ∑ k ∈ s.piAntidiag n, ↑(multinomial s k) * s.noncommProd (fun i ↦ f✝ i ^ k i) ⋯
hc : (↑(cons a s has)).Pairwise (Commute on f✝)
n : ℕ
p : ℕ × ℕ
hp : p ∈ antidiagonal n
f : α → ℕ
hf : s.sum f = p.2 ∧ ∀ (i : α), f i ≠ 0 → i ∈ s
⊢ ↑((f a + p.1 + s.sum f).choose (f a + p.1)) * ↑(multinomial s (f + fun i ↦ if i = a then p.1 else 0)) *
      (f✝ a ^ (f a + p.1) * s.noncommProd (fun i ↦ f✝ i ^ (f i + if i = a then p.1 else 0)) ⋯) =
    ↑(n.choose p.1) * ↑(multinomial s f) * (f✝ a ^ p.1 * s.noncommProd (fun i ↦ f✝ i ^ f i) ⋯)
Module: Mathlib.Algebra.MvPolynomial.Division

Goal state before:
pp: case mp.g
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
i : σ
p q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
r : MvPolynomial σ R
hp : X i * q = p * r
this : X i ∣ p ∨ X i ∣ r
hip : X i ∣ p
⊢ p.divMonomial (Finsupp.single i 1) ∣ q

Tactic:
rw [X_dvd_iff_modMonomial_eq_zero] at hip

Goal state after:
case mp.g
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
i : σ
p q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
r : MvPolynomial σ R
hp : X i * q = p * r
this : X i ∣ p ∨ X i ∣ r
hip : p.modMonomial (Finsupp.single i 1) = 0
⊢ p.divMonomial (Finsupp.single i 1) ∣ q
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: case empty.succ
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
x : α → R
hc : (↑∅).Pairwise (Commute on x)
n : ℕ
⊢ 0 ^ (n + 1) = ∑ k, ↑(↑↑k).countPerms * (Multiset.map x ↑↑k).noncommProd ⋯

Tactic:
rw [_root_.pow_succ, mul_zero]
      have : IsEmpty (Finset.sym (∅ : Finset α) n.succ) := Finset.instIsEmpty
      apply (Fintype.sum_empty _).symm

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

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : MvPolynomial σ R
a : R
ha : a ≠ 0
hf : f ∣ C a
⊢ C a ≠ 0

Tactic:
simp [ha]

Goal state after:
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 : σ
r : R
hr : r ≠ 0
⊢ p ∣ (monomial (Finsupp.single i 1)) (r • 1) ↔ ∃ s, s ∣ r ∧ (p = C s ∨ p = s • (monomial (Finsupp.single i 1)) 1)

Tactic:
smul_eq_mul,

Goal state after:
R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p : MvPolynomial σ R
i : σ
r : R
hr : r ≠ 0
⊢ p ∣ (monomial (Finsupp.single i 1)) (r * 1) ↔ ∃ s, s ∣ r ∧ (p = C s ∨ p = s • (monomial (Finsupp.single i 1)) 1)
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f : MvPolynomial σ R
d : σ →₀ ℕ
hd : d ∈ f.support
⊢ m.toSyn d ≤ m.toSyn (m.toSyn.symm (f.support.sup ⇑m.toSyn))

Tactic:
simp only [AddEquiv.apply_symm_apply, Finset.le_sup hd]

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

Goal state before:
pp: α : Type u_2
k : ℕ
inst✝¹ : Fintype α
inst✝ : Fintype (Sym α k)
⊢ Fintype.card (Sym α k) = (Fintype.card α).multichoose k

Tactic:
← card_sym_fin_eq_multichoose

Goal state after:
α : Type u_2
k : ℕ
inst✝¹ : Fintype α
inst✝ : Fintype (Sym α k)
⊢ Fintype.card (Sym α k) = Fintype.card (Sym (Fin (Fintype.card α)) k)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Nat

Goal state before:
pp: n : ℕ
⊢ Multiset.Rel (fun x1 x2 ↦ Associated x1 x2) (normalizedFactors (n + 1)) ↑(n + 1).primeFactorsList

Tactic:
apply UniqueFactorizationMonoid.factors_unique irreducible_of_normalized_factor _

Goal state after:
n : ℕ
⊢ Associated (normalizedFactors (n + 1)).prod (↑(n + 1).primeFactorsList).prod

n : ℕ
⊢ ∀ x ∈ ↑(n + 1).primeFactorsList, Irreducible x
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: n k : ℕ
pk : Prime k
dk : k ∣ n
dkk : ¬k * k ∣ n
o : Option ℕ
H : (n / k).MinSqFacProp o
this : ∀ (p : ℕ), Prime p → p * p ∣ n → k * (p * p) ∣ n
⊢ n.MinSqFacProp o

Tactic:
rcases o with - | d

Goal state after:
case none
n k : ℕ
pk : Prime k
dk : k ∣ n
dkk : ¬k * k ∣ n
this : ∀ (p : ℕ), Prime p → p * p ∣ n → k * (p * p) ∣ n
H : (n / k).MinSqFacProp none
⊢ n.MinSqFacProp none

case some
n k : ℕ
pk : Prime k
dk : k ∣ n
dkk : ¬k * k ∣ n
this : ∀ (p : ℕ), Prime p → p * p ∣ n → k * (p * p) ∣ n
d : ℕ
H : (n / k).MinSqFacProp (some d)
⊢ n.MinSqFacProp (some d)
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

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

Tactic:
degree,

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : p.support ⊆ q.support
⊢ m.toSyn (m.toSyn.symm (p.support.sup ⇑m.toSyn)) ≤ m.toSyn (m.toSyn.symm (q.support.sup ⇑m.toSyn))
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' : ℕ
⊢ n' ∣ n → ¬k ∣ n' → n'.MinSqFacProp (n'.minSqFacAux (k + 2))

Tactic:
nd'

Goal state after:
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
⊢ ¬k ∣ n' → n'.MinSqFacProp (n'.minSqFacAux (k + 2))
Module: Mathlib.Data.Nat.Squarefree

Goal state before:
pp: case h
n : ℕ
h0✝ : n ≠ 0
a : ℕ
hsq : Squarefree a
an : a ∣ n
h0 : n ≠ 0
⊢ (normalizedFactors a).toFinset ⊆ (normalizedFactors n).toFinset ∧ (normalizedFactors a).toFinset.val.prod = a

Tactic:
rcases an with ⟨b, rfl⟩

Goal state after:
case h
a : ℕ
hsq : Squarefree a
b : ℕ
h0✝ h0 : a * b ≠ 0
⊢ (normalizedFactors a).toFinset ⊆ (normalizedFactors (a * b)).toFinset ∧ (normalizedFactors a).toFinset.val.prod = a
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
⊢ coeff (ofLex (AddMonoidAlgebra.supDegree (⇑toLex) p'.leadingCoeff)) p'.leadingCoeff ≠ 0

Tactic:
← hpₖ,

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
hp : p ≠ 0
S : Fin (n + 1) → Finset R
p' : Polynomial (MvPolynomial (Fin n) R) := (finSuccEquiv R n) p
hp' : p' = (finSuccEquiv R n) p
k : ℕ := p'.natDegree
hk : k = p'.natDegree
pₖ : MvPolynomial (Fin n) R := p'.leadingCoeff
hpₖ : pₖ = p'.leadingCoeff
hp'₀ : p' ≠ 0
hpₖ₀ : pₖ ≠ 0
xₜ : 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
⊢ coeff (ofLex (AddMonoidAlgebra.supDegree (⇑toLex) pₖ)) pₖ ≠ 0
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
⊢ (pₖ.support.sup fun s ↦ ∑ i, ↑(s i) / ↑(#(S i.succ))) + ↑(degreeOf 0 p) / ↑(#(S 0)) ≤
    p.support.sup fun s ↦ ∑ i, ↑(s i) / ↑(#(S i))

Tactic:
· rw [Finset.sup_add (support_nonempty.mpr hpₖ₀)]
      apply Finset.sup_le
      rintro i hi
      refine le_sup_of_le (mem_support_coeff_finSuccEquiv.mp hi) ?_
      rw [Fin.sum_univ_succ, add_comm]
      dsimp
      gcongr
      simp [natDegree_finSuccEquiv, p']

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

Goal state before:
pp: R : Type u_1
inst✝ : CommGroupWithZero R
f g : ArithmeticFunction R
hf : f.IsMultiplicative
hg : g.IsMultiplicative
m✝ n✝ : ℕ
cop : m✝.Coprime n✝
⊢ (f.pdiv g) (m✝ * n✝) = (f.pdiv g) m✝ * (f.pdiv g) n✝

Tactic:
by
    simp only [pdiv_apply, map_mul_of_coprime hf cop, map_mul_of_coprime hg cop, div_eq_mul_inv,
      mul_inv]
    apply mul_mul_mul_comm

Goal state after:
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
r : ArithmeticFunction R
x y : ArithmeticFunction M
x✝ : ℕ
⊢ (r • (x + y)) x✝ = (r • x + r • y) x✝

Tactic:
simp only [sum_add_distrib, smul_add, smul_apply, add_apply]

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
f : ℕ → R
hf : Invertible (f 1)
n : ℕ
hn0 : n ≠ 0
hn1 : n ≠ 1
| -⅟(f 1) * ∑ d ∈ n.properDivisors, f (n / d) * dirichletInverseFun f hf d

Tactic:
rw [← Finset.sum_attach, Finset.attach_eq_univ]

Goal state after:
R : Type u_1
inst✝ : Ring R
f : ℕ → R
hf : Invertible (f 1)
n : ℕ
hn0 : n ≠ 0
hn1 : n ≠ 1
| -⅟(f 1) * ∑ x, f (n / ↑x) * dirichletInverseFun f hf ↑x
Module: Mathlib.NumberTheory.ArithmeticFunction.Defs

Goal state before:
pp: R : Type u_1
f : ArithmeticFunction ℕ
inst✝ : Semiring R
h : f.IsMultiplicative
m✝ n✝ : ℕ
cop : m✝.Coprime n✝
⊢ ↑f (m✝ * n✝) = ↑f m✝ * ↑f n✝

Tactic:
simp [h.2 cop]

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

Goal state before:
pp: R : Type u_1
f : ArithmeticFunction ℤ
inst✝ : Ring R
h : f.IsMultiplicative
m✝ n✝ : ℕ
cop : m✝.Coprime n✝
⊢ ↑f (m✝ * n✝) = ↑f m✝ * ↑f n✝

Tactic:
simp [h.2 cop]

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

Goal state before:
pp: d : ℕ
⊢ d.finMulAntidiag 1 = {fun x ↦ 1}

Tactic:
ext
  simp only [mem_finMulAntidiag, prod_eq_one_iff, mem_univ, forall_const, ne_eq, one_ne_zero,
    not_false_eq_true, and_true, mem_singleton]
  grind

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

Goal state before:
pp: case h.h
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 ∈ n.primeFactors.attach with f ↑p ⋯ = f p hp, ↑p ∈ {x | p ∣ x}

Tactic:
simp_rw [Set.mem_ofPred_eq]

Goal state after:
case h.h
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 ∣ ∏ p ∈ n.primeFactors.attach with f ↑p ⋯ = f p hp, ↑p
Module: Mathlib.Algebra.Order.Antidiag.Nat

Goal state before:
pp: case h.a
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 ∈ n.primeFactors.attach with g ↑p ⋯ = f p hp, ↑p ∉ {x | p ∣ x}

Tactic:
simp_rw [Set.mem_ofPred_eq]

Goal state after:
case h.a
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 ∣ ∏ p ∈ n.primeFactors.attach with g ↑p ⋯ = f p hp, ↑p
Module: Mathlib.Algebra.Order.Archimedean.IndicatorCard

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : AddCommMonoid α
a : α
s : Set ℕ
hs : s.Finite
key : ∀ x ∈ hs.toFinset, s.indicator (fun x ↦ a) x = a
m : ℕ
hm : m ∈ upperBounds s
n : ℕ
n_m : m + 1 ≤ n
x : ℕ
⊢ x ∈ s → x ∈ Finset.range n

pp: case refine_2
α : Type u_1
inst✝ : AddCommMonoid α
a : α
s : Set ℕ
hs : s.Finite
key : ∀ x ∈ hs.toFinset, s.indicator (fun x ↦ a) x = a
m : ℕ
hm : m ∈ upperBounds s
n : ℕ
n_m : m + 1 ≤ n
x : ℕ
⊢ x ∈ Finset.range n → x ∉ s → s.indicator (fun x ↦ a) x = 0

Tactic:
· rw [Finset.mem_range]
    exact fun x_s ↦ ((mem_upperBounds.1 hm) x x_s).trans_lt (Nat.lt_of_succ_le n_m)

Goal state after:
case refine_2
α : Type u_1
inst✝ : AddCommMonoid α
a : α
s : Set ℕ
hs : s.Finite
key : ∀ x ∈ hs.toFinset, s.indicator (fun x ↦ a) x = a
m : ℕ
hm : m ∈ upperBounds s
n : ℕ
n_m : m + 1 ≤ n
x : ℕ
⊢ x ∈ Finset.range n → x ∉ s → s.indicator (fun x ↦ a) x = 0
Module: Mathlib.Algebra.Order.CompleteField

Goal state before:
pp: case refine_2
α : Type u_2
β : Type u_3
inst✝⁶ : Field α
inst✝⁵ : LinearOrder α
inst✝⁴ : IsStrictOrderedRing α
inst✝³ : Field β
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : Archimedean α
q : ℚ
w : β
h : w < ↑q
⊢ ∃ a ∈ cutMap β ↑q, w < a

Tactic:
· obtain ⟨q', hwq, hq⟩ := exists_rat_btwn h
    rw [cutMap_coe]
    exact ⟨q', ⟨_, hq, rfl⟩, hwq⟩

Goal state after: