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

Goal state before:
pp: ι : 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
⊢ dist (integralSum g μ.toBoxAdditive.toSMul π) (∑ J ∈ π.boxes, μ.real ↑J • (f (Nx (π.tag J))) (π.tag J)) +
        dist (∑ J ∈ π.boxes, μ.real ↑J • (f (Nx (π.tag J))) (π.tag J))
          (∑ J ∈ π.boxes, ∫ (x : ι → ℝ) in ↑J, (f (Nx (π.tag J))) x ∂μ) +
      dist (∑ J ∈ π.boxes, ∫ (x : ι → ℝ) in ↑J, (f (Nx (π.tag J))) x ∂μ) (∫ (a : ι → ℝ) in ↑I, g a ∂μ) ≤
    (μ.real ↑I + 1 + 1) * ↑ε

Tactic:
rw [add_mul, add_mul, one_mul]

Goal state after:
ι : 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
⊢ dist (integralSum g μ.toBoxAdditive.toSMul π) (∑ J ∈ π.boxes, μ.real ↑J • (f (Nx (π.tag J))) (π.tag J)) +
        dist (∑ J ∈ π.boxes, μ.real ↑J • (f (Nx (π.tag J))) (π.tag J))
          (∑ J ∈ π.boxes, ∫ (x : ι → ℝ) in ↑J, (f (Nx (π.tag J))) x ∂μ) +
      dist (∑ J ∈ π.boxes, ∫ (x : ι → ℝ) in ↑J, (f (Nx (π.tag J))) x ∂μ) (∫ (a : ι → ℝ) in ↑I, g a ∂μ) ≤
    μ.real ↑I * ↑ε + ↑ε + ↑ε
Module: Mathlib.Analysis.BoxIntegral.Basic

Goal state before:
pp: ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
h : Integrable I l f vol
π₀ : Prepartition I
⊢ Filter.map (fun p ↦ (integralSum f vol p.1, integralSum f vol p.2))
      (l.toFilter I ×ˢ l.toFilter I ⊓ 𝓟 ({π | π.iUnion = π₀.iUnion} ×ˢ {π | π.iUnion = π₀.iUnion})) ≤
    𝓤 F

Tactic:
exact h.tendsto_integralSum_toFilter_prod_self_inf_iUnion_eq_uniformity.mono_left
    (inf_le_inf_left _ <| principal_mono.2 fun π h => h.1.trans h.2.symm)

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
y : E ⧸ K
⊢ ‖y‖ ^ 2 = RCLike.re ⟪K.quotientEquivOrthogonal y, K.quotientEquivOrthogonal y⟫_𝕜

Tactic:
rw [inner_self_eq_norm_sq, LinearIsometryEquiv.norm_map]

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
x : ι
⊢ b x = (⇑(b.reindex e) ∘ ⇑e) x

Tactic:
simp only [OrthonormalBasis.coe_reindex, Function.comp_apply, Equiv.symm_apply_apply]

Goal state after:
Module: Mathlib.Analysis.SumOverResidueClass

Goal state before:
pp: R : Type u_1
inst✝² : AddCommGroup R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalAddGroup R
m : ℕ
hm : NeZero m
k : ℕ
f : ℕ → R
g : ℕ → ℕ := fun n ↦ m * n + k
hg : Function.Injective g
hg' : ∀ n ∉ range g, {n | ↑n = ↑k ∧ k ≤ n}.indicator f n = 0
x✝ : ℕ
⊢ f (m * x✝ + k) = ({n | ↑n = ↑k ∧ k ≤ n}.indicator f ∘ g) x✝

Tactic:
simp only [Function.comp_apply, mem_ofPred_eq, Nat.cast_add, Nat.cast_mul, CharP.cast_eq_zero,
      zero_mul, zero_add, le_add_iff_nonneg_left, zero_le, and_self, indicator_of_mem, g]

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

Goal state before:
pp: case left
ι : Type u
E : Type v
inst✝⁴ : Fintype ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
hb : ∃ C, ∀ x ∈ Box.Icc I, ‖f x‖ ≤ C
hc : ∀ᵐ (x : ι → ℝ) ∂μ, ContinuousAt f x
l : IntegrationParams
y : E
hy : HasIntegral I l f μ.toBoxAdditive.toSMul y
v : Set (ι → ℝ) := {x | ContinuousAt f x}
this : AEStronglyMeasurable f (μ.restrict v)
s : Set (ι → ℝ)
hs : MeasurableSet s
⊢ μ (s ∩ vᶜ) = 0

Tactic:
← nonpos_iff_eq_zero

Goal state after:
case left
ι : Type u
E : Type v
inst✝⁴ : Fintype ι
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : (ι → ℝ) → E
μ : Measure (ι → ℝ)
inst✝ : IsLocallyFiniteMeasure μ
I : Box ι
hb : ∃ C, ∀ x ∈ Box.Icc I, ‖f x‖ ≤ C
hc : ∀ᵐ (x : ι → ℝ) ∂μ, ContinuousAt f x
l : IntegrationParams
y : E
hy : HasIntegral I l f μ.toBoxAdditive.toSMul y
v : Set (ι → ℝ) := {x | ContinuousAt f x}
this : AEStronglyMeasurable f (μ.restrict v)
s : Set (ι → ℝ)
hs : MeasurableSet s
⊢ μ (s ∩ vᶜ) ≤ 0
Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics

Goal state before:
pp: α : Type u_1
inst✝ : NormedAddCommGroup α
f : ℕ → α
g : ℕ → ℝ
h : f =o[atTop] g
hg : 0 ≤ g
h'g : Tendsto (fun n ↦ ∑ i ∈ Finset.range n, g i) atTop atTop
A : ∀ (i : ℕ), ‖g i‖ = g i
B : ∀ (n : ℕ), ‖∑ i ∈ Finset.range n, g i‖ = ∑ i ∈ Finset.range n, g i
ε : ℝ
εpos : 0 < ε
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ‖f b‖ ≤ ε / 2 * g b
this : (fun x ↦ ∑ i ∈ Finset.range N, f i) =o[atTop] fun n ↦ ∑ i ∈ Finset.range n, g i
n : ℕ
hn : ‖∑ i ∈ Finset.range N, f i‖ ≤ ε / 2 * ‖∑ i ∈ Finset.range n, g i‖
Nn : n ∈ Set.Ici N
⊢ ‖∑ i ∈ Finset.range n, f i‖ = ‖∑ i ∈ Finset.range N, f i + ∑ i ∈ Finset.Ico N n, f i‖

Tactic:
by
      rw [sum_range_add_sum_Ico _ Nn]

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: p : ℝ
⊢ (Summable fun n ↦ (↑n ^ p)⁻¹) ↔ 1 < p

Tactic:
by
  rcases le_or_gt 0 p with hp | hp
  /- Cauchy condensation test applies only to antitone sequences, so we consider the
    cases `0 ≤ p` and `p < 0` separately. -/
  · rw [← summable_condensed_iff_of_nonneg]
    · simp_rw [Nat.cast_pow, Nat.cast_two, ← rpow_natCast, ← rpow_mul zero_lt_two.le, mul_comm _ p,
        rpow_mul zero_lt_two.le, rpow_natCast, ← inv_pow, ← mul_pow,
        summable_geometric_iff_norm_lt_one]
      nth_rw 1 [← rpow_one 2]
      rw [← division_def, ← rpow_sub zero_lt_two, norm_eq_abs,
        abs_of_pos (rpow_pos_of_pos zero_lt_two _), rpow_lt_one_iff zero_lt_two.le]
      simp
    · intro n
      positivity
    · intro m n hm hmn
      gcongr
  -- If `p < 0`, then `1 / n ^ p` tends to infinity, thus the series diverges.
  · suffices ¬Summable (fun n => ((n : ℝ) ^ p)⁻¹ : ℕ → ℝ) by
      have : ¬1 < p := fun hp₁ => hp.not_ge (zero_le_one.trans hp₁.le)
      simpa only [this, iff_false]
    intro h
    obtain ⟨k : ℕ, hk₁ : ((k : ℝ) ^ p)⁻¹ < 1, hk₀ : k ≠ 0⟩ :=
      ((h.tendsto_cofinite_zero.eventually (gt_mem_nhds zero_lt_one)).and
          (eventually_cofinite_ne 0)).exists
    apply hk₀
    rw [← pos_iff_ne_zero, ← @Nat.cast_pos ℝ] at hk₀
    simpa [inv_lt_one₀ (rpow_pos_of_pos hk₀ _), one_lt_rpow_iff_of_pos hk₀, hp,
      hp.not_gt, hk₀] using hk₁

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: m : ℕ
hm : m ≠ 0
k : ZMod m
this : NeZero m
h : ∀ (n : ℕ), {n | ↑n = k - 1}.indicator (fun n ↦ 1 / ↑(n + 1)) n = if ↑n = k - 1 then 1 / (↑n + 1) else 0
⊢ ¬Summable fun n ↦ 1 / ↑(n + 1)

Tactic:
exact mt (summable_nat_add_iff (f := fun n : ℕ ↦ 1 / (n : ℝ)) 1).mp not_summable_one_div_natCast

Goal state after:
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:
by
        gcongr
        refine Summable.sum_le_tsum _ (fun _ _ ↦ by positivity) (Real.summable_nat_rpow.mpr ?_)
        linarith

Goal state after:
Module: Mathlib.Data.List.GetD

Goal state before:
pp: α : Type u
β : Type v
l : List α
d : α
n : ℕ
f : α → β
⊢ (map f l).getD n (f d) = f (l.getD n d)

Tactic:
by
  simp only [getD_eq_getElem?_getD, getElem?_map, Option.getD_map]

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

Goal state before:
pp: case pos
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
⊢ ↑(Nat.multinomial a.support ⇑s) * ∏ x ∈ a.support, a x ^ s x = ↑s.multinomial * ∏ x ∈ a.support, a x ^ s x

Tactic:
Finsupp.multinomial_of_support_subset hs'

Goal state after:
case pos
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
⊢ ↑s.multinomial * ∏ x ∈ a.support, a x ^ s x = ↑s.multinomial * ∏ x ∈ a.support, a x ^ s x
Module: Mathlib.Algebra.MvPolynomial.Division

Goal state before:
pp: case mpr.inl
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
i : σ
p q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
a✝ : Nontrivial R
h : X i ∣ p
⊢ X i ∣ p * q

pp: case mpr.inr
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
i : σ
p q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
a✝ : Nontrivial R
h : X i ∣ q
⊢ X i ∣ p * q

Tactic:
· exact dvd_mul_of_dvd_left h q

Goal state after:
case mpr.inr
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
i : σ
p q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
a✝ : Nontrivial R
h : X i ∣ q
⊢ X i ∣ p * q
Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
i : σ
p : MvPolynomial σ R
n : ℕ
hp : p ≠ 0
⊢ degreeOf i (p ^ n) = n * degreeOf i p

Tactic:
pow_eq_prod_const,

Goal state after:
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
i : σ
p : MvPolynomial σ R
n : ℕ
hp : p ≠ 0
⊢ degreeOf i (∏ _k ∈ range n, p) = n * degreeOf i p
Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors

Goal state before:
pp: case mpr
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : MvPolynomial σ R
a : R
ha : a ≠ 0
⊢ (∃ b, b ∣ a ∧ f = C b) → f ∣ C a

Tactic:
rintro ⟨b, hab, rfl⟩

Goal state after:
case mpr
R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
a : R
ha : a ≠ 0
b : R
hab : b ∣ a
⊢ C b ∣ C a
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
c : σ →₀ ℕ
hc : m.toSyn (m.degree f + m.degree g) < m.toSyn c
d e : σ →₀ ℕ
hde : d + e = c
hd : ¬m.toSyn (m.degree f) < m.toSyn d
⊢ m.toSyn (m.degree g) < m.toSyn e

Tactic:
simp only [not_lt] at hd

Goal state after:
case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
f g : MvPolynomial σ R
c : σ →₀ ℕ
hc : m.toSyn (m.degree f + m.degree g) < m.toSyn c
d e : σ →₀ ℕ
hde : d + e = c
hd : m.toSyn d ≤ m.toSyn (m.degree f)
⊢ m.toSyn (m.degree g) < m.toSyn e
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, m.Monic (P i)
⊢ m.leadingCoeff (∏ i ∈ s, P i) = 1

Tactic:
leadingCoeff_prod_of_regular

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, m.Monic (P i)
⊢ ∏ i ∈ s, m.leadingCoeff (P i) = 1

σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
ι : Type u_3
P : ι → MvPolynomial σ R
s : Finset ι
H : ∀ i ∈ s, m.Monic (P i)
⊢ ∀ i ∈ s, IsRegular (m.leadingCoeff (P i))
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 ↦ S i | (eval (tail x)) pₖ ≠ 0 ∧ (eval x) p = 0}) =
    #({xₜ ∈ piFinset fun i ↦ tail S i | (eval xₜ) pₖ ≠ 0}.biUnion fun xₜ ↦
        image (fun x₀ ↦ (x₀, xₜ)) ({x₀ ∈ S 0 | (eval (Fin.cons x₀ xₜ)) p = 0}))

Tactic:
← filter_filter,

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 ∈ {x ∈ piFinset fun i ↦ S i | (eval (tail x)) pₖ ≠ 0} | (eval x) p = 0}) =
    #({xₜ ∈ piFinset fun i ↦ tail S i | (eval xₜ) pₖ ≠ 0}.biUnion fun xₜ ↦
        image (fun x₀ ↦ (x₀, xₜ)) ({x₀ ∈ S 0 | (eval (Fin.cons x₀ xₜ)) 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.Data.Nat.Squarefree

Goal state before:
pp: n : ℕ
hn : Squarefree n
⊢ ∏ p ∈ n.primeFactors, p = n

Tactic:
rw [← toFinset_factors, List.prod_toFinset _ hn.nodup_primeFactorsList,
    List.map_id', Nat.prod_primeFactorsList hn.ne_zero]

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

Goal state before:
pp: n : ℕ
hn : Squarefree n
t : Finset ℕ
ht : t ⊆ n.primeFactors
⊢ n = (∏ a ∈ n.primeFactors \ t, a) * ∏ a ∈ t, a

Tactic:
Finset.prod_sdiff ht,

Goal state after:
n : ℕ
hn : Squarefree n
t : Finset ℕ
ht : t ⊆ n.primeFactors
⊢ n = ∏ x ∈ n.primeFactors, x
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

Goal state before:
pp: case mp
n : ℕ
h0 : n ≠ 0
h : n.primeFactorsList.dedup.length = Ω n
⊢ n.primeFactorsList.Nodup

Tactic:
rw [← n.primeFactorsList.dedup_sublist.eq_of_length h]

Goal state after:
case mp
n : ℕ
h0 : n ≠ 0
h : n.primeFactorsList.dedup.length = Ω n
⊢ n.primeFactorsList.dedup.Nodup
Module: Mathlib.NumberTheory.ArithmeticFunction.Misc

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

Tactic:
induction s using cons_induction_on with

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

Goal state before:
pp: d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiag n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (fun i ↦ p ∣ t i) (f p hp)
hf_unique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors) (y : Fin d), (fun i ↦ p ∣ t i) y → y = f p hp
i : Fin d
this : t i ∣ n
⊢ ∏ a ∈ n.primeFactors with a ∣ t i, a = t i

Tactic:
rw [primeFactors_filter_dvd_of_dvd hn.ne_zero this]

Goal state after:
d n : ℕ
hn : Squarefree n
t : Fin d → ℕ
ht : t ∈ d.finMulAntidiag n
f : (p : ℕ) → p ∈ n.primeFactors → Fin d
hf : ∀ (p : ℕ) (hp : p ∈ n.primeFactors), (fun i ↦ p ∣ t i) (f p hp)
hf_unique : ∀ (p : ℕ) (hp : p ∈ n.primeFactors) (y : Fin d), (fun i ↦ p ∣ t i) y → y = f p hp
i : Fin d
this : t i ∣ n
⊢ ∏ a ∈ (t i).primeFactors, a = t i
Module: Mathlib.Algebra.Order.Antidiag.Nat

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

Tactic:
use a 0

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

Goal state before:
pp: case mk
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a✝ b a : M
⊢ mk a ≤ mk 1

Tactic:
mk_le_mk

Goal state after:
case mk
M : Type u_1
inst✝² : CommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedMonoid M
a✝ b a : M
⊢ ∃ n, |1|ₘ ≤ |a|ₘ ^ n
Module: Mathlib.Algebra.Order.Group.Ideal

Goal state before:
pp: M : Type u_1
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : WellQuasiOrderedLE M
inst✝ : CanonicallyOrderedMul M
f : ℕ →o SemigroupIdeal M
s : Finset M
hI : ⨆ i, f i = closure ↑s
g : M → ℕ
hg : ∀ x ∈ s, x ∈ f (g x)
n : ℕ
hn : s.sup g ≤ n
x : M
hx : x ∈ closure ↑s
⊢ x ∈ f (s.sup g)

Tactic:
mem_closure''

Goal state after:
M : Type u_1
inst✝³ : CommMonoid M
inst✝² : PartialOrder M
inst✝¹ : WellQuasiOrderedLE M
inst✝ : CanonicallyOrderedMul M
f : ℕ →o SemigroupIdeal M
s : Finset M
hI : ⨆ i, f i = closure ↑s
g : M → ℕ
hg : ∀ x ∈ s, x ∈ f (g x)
n : ℕ
hn : s.sup g ≤ n
x : M
hx : ∃ y, ∃ z ∈ ↑s, y * z = x
⊢ x ∈ f (s.sup g)
Module: Mathlib.Algebra.Order.GroupWithZero.Lex

Goal state before:
pp: case coe.coe
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero α
inst✝ : LinearOrderedCommGroupWithZero β
a✝¹ a✝ : Lex (αˣ × βˣ)
⊢ ↑a✝¹ ≤ ↑a✝ →
    (↑((MonoidWithZeroHom.fst α β).comp (WithZero.map' (toLexMulEquiv (αˣ × βˣ)).symm.toMonoidHom))).toFun ↑a✝¹ ≤
      (↑((MonoidWithZeroHom.fst α β).comp (WithZero.map' (toLexMulEquiv (αˣ × βˣ)).symm.toMonoidHom))).toFun ↑a✝

Tactic:
· simpa using Prod.Lex.monotone_fst _ _

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Basic

Goal state before:
pp: case none.none
ι : Type u_1
α : Type u_2
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
s t : Interval α
⊢ none / none = none * none⁻¹

Tactic:
first | rfl | exact congr_arg WithBot.some (div_eq_mul_inv _ _)

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Basic

Goal state before:
pp: case none.some
ι : Type u_1
α : Type u_2
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
s t✝ : Interval α
t : NonemptyInterval α
⊢ none / some t = none * (some t)⁻¹

Tactic:
first | rfl | exact congr_arg WithBot.some (div_eq_mul_inv _ _)

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Basic

Goal state before:
pp: case some.none
ι : Type u_1
α : Type u_2
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
s✝ t : Interval α
s : NonemptyInterval α
⊢ some s / none = some s * none⁻¹

Tactic:
first | rfl | exact congr_arg WithBot.some (div_eq_mul_inv _ _)

Goal state after:
Module: Mathlib.Algebra.Order.Interval.Basic

Goal state before:
pp: case some.some
ι : Type u_1
α : Type u_2
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
s✝ t✝ : Interval α
s t : NonemptyInterval α
⊢ some s / some t = some s * (some t)⁻¹

Tactic:
first | rfl | exact congr_arg WithBot.some (div_eq_mul_inv _ _)

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Basic

Goal state before:
pp: case pos
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : R⟦Γ⟧
hx : 0 < x.order
h : x = 0
⊢ 0 < x.orderTop

pp: case neg
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : R⟦Γ⟧
hx : 0 < x.order
h : ¬x = 0
⊢ 0 < x.orderTop

Tactic:
· simp_all only [order_zero, lt_self_iff_false]

Goal state after:
case neg
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
inst✝ : Zero Γ
x : R⟦Γ⟧
hx : 0 < x.order
h : ¬x = 0
⊢ 0 < x.orderTop
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝² : Zero Γ
inst✝¹ : PartialOrder Γ
inst✝ : MulZeroOneClass R
⊢ order 1 = 0

Tactic:
by
  cases subsingleton_or_nontrivial R
  · rw [Subsingleton.elim (1 : R⟦Γ⟧) 0, order_zero]
  · exact order_single one_ne_zero

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: case neg
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
h : x.leadingCoeff * y.leadingCoeff ≠ 0
hx : ¬x = 0
hy : ¬y = 0
this : (x * y).coeff (x.order + y.order) ≠ 0
hxy : x * y ≠ 0
⊢ x.order + y.order ≤ (x * y).order

Tactic:
rw [HahnSeries.order_of_ne hx, HahnSeries.order_of_ne hy, HahnSeries.order_of_ne hxy,
    ← Set.IsWF.min_add]

Goal state after:
case neg
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
h : x.leadingCoeff * y.leadingCoeff ≠ 0
hx : ¬x = 0
hy : ¬y = 0
this : (x * y).coeff (x.order + y.order) ≠ 0
hxy : x * y ≠ 0
⊢ ⋯.min ⋯ ≤ ⋯.min ⋯
Module: Mathlib.RingTheory.HahnSeries.Multiplication

Goal state before:
pp: Γ✝ : Type u_1
Γ' : Type u_2
R✝ : Type u_3
S : Type u_4
V : Type u_5
Γ : Type ?u.9
R : Type ?u.15
inst✝³ : LinearOrder Γ
inst✝² : AddCommMonoid Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
y : R⟦Γ⟧ˣ
h : y ∈ {x | 0 < (↑x - 1).orderTop}
h✝ : Nontrivial R
this : (↑y).orderTop = 0 ∧ (↑y).leadingCoeff = 1
⊢ (↑y).leadingCoeff * y.inv.leadingCoeff ≠ 0

Tactic:
this.2,

Goal state after:
Γ✝ : Type u_1
Γ' : Type u_2
R✝ : Type u_3
S : Type u_4
V : Type u_5
Γ : Type ?u.9
R : Type ?u.15
inst✝³ : LinearOrder Γ
inst✝² : AddCommMonoid Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
y : R⟦Γ⟧ˣ
h : y ∈ {x | 0 < (↑x - 1).orderTop}
h✝ : Nontrivial R
this : (↑y).orderTop = 0 ∧ (↑y).leadingCoeff = 1
⊢ 1 * y.inv.leadingCoeff ≠ 0
Module: Mathlib.Order.Quotient

Goal state before:
pp: case h.h
α : Type u_1
s : Setoid α
inst✝¹ : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
inst✝ : DecidableRel fun x1 x2 ↦ x1 ≈ x2
x y : α
h₁ : ⟦x⟧ ≤ ⟦y⟧
h₂ : ⟦y⟧ ≤ ⟦x⟧
⊢ ⟦x⟧ = ⟦y⟧

Tactic:
mk_le_mk

Goal state after:
case h.h
α : Type u_1
s : Setoid α
inst✝¹ : LinearOrder α
H : ∀ (x : Quotient s), (Quotient.mk s ⁻¹' {x}).OrdConnected
inst✝ : DecidableRel fun x1 x2 ↦ x1 ≈ x2
x y : α
h₁ : x ≤ y ∨ x ≈ y
h₂ : y ≤ x ∨ y ≈ x
⊢ ⟦x⟧ = ⟦y⟧