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

Goal state before:
pp: ι : Type u_2
K : Type u_3
inst✝⁵ : NormedField K
inst✝⁴ : LinearOrder K
inst✝³ : IsStrictOrderedRing K
inst✝² : FloorRing K
inst✝¹ : Fintype ι
inst✝ : Unique ι
k : K
x✝ : ι
⊢ ((Basis.singleton ι K).repr ↑(floor (Basis.singleton ι K) k)) x✝ = ((Basis.singleton ι K).repr ↑⌊k⌋) x✝

Tactic:
repr_floor_apply,

Goal state after:
ι : Type u_2
K : Type u_3
inst✝⁵ : NormedField K
inst✝⁴ : LinearOrder K
inst✝³ : IsStrictOrderedRing K
inst✝² : FloorRing K
inst✝¹ : Fintype ι
inst✝ : Unique ι
k : K
x✝ : ι
⊢ ↑⌊((Basis.singleton ι K).repr k) x✝⌋ = ((Basis.singleton ι K).repr ↑⌊k⌋) x✝
Module: Mathlib.Analysis.BoxIntegral.Partition.Basic

Goal state before:
pp: ι : Type u_1
I : Box ι
π : Prepartition I
inst✝ : Fintype ι
x : ι → ℝ
⊢ #({J ∈ π.boxes | x ∈ Box.Icc J}) ≤ Fintype.card (Set ι)

Tactic:
refine Finset.card_le_card_of_injOn (fun J : Box ι => { i | J.lower i = x i })
    (fun _ _ => Finset.mem_univ _) ?_

Goal state after:
ι : Type u_1
I : Box ι
π : Prepartition I
inst✝ : Fintype ι
x : ι → ℝ
⊢ InjOn (fun J ↦ {i | J.lower i = x i}) ↑({J ∈ π.boxes | x ∈ Box.Icc J})
Module: Mathlib.Analysis.BoxIntegral.Partition.Basic

Goal state before:
pp: ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
hJ : J ∈ π.biUnion πi
⊢ J ∈ πi (π.biUnionIndex πi J)

Tactic:
convert! (π.mem_biUnion.1 hJ).choose_spec.2

Goal state after:
case e'_2
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
hJ : J ∈ π.biUnion πi
⊢ π.biUnionIndex πi J = ⋯.choose

case e'_3
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
hJ : J ∈ π.biUnion πi
e_2✝ : Prepartition (π.biUnionIndex πi J) = Prepartition ⋯.choose
⊢ π.biUnionIndex πi J = ⋯.choose

case e'_4
ι : Type u_1
I J : Box ι
π : Prepartition I
πi : (J : Box ι) → Prepartition J
hJ : J ∈ π.biUnion πi
e_2✝ : Prepartition (π.biUnionIndex πi J) = Prepartition ⋯.choose
⊢ π.biUnionIndex πi J = ⋯.choose
Module: Mathlib.Analysis.BoxIntegral.Partition.Basic

Goal state before:
pp: ι : Type u_1
I J J₁ : Box ι
π : Prepartition I
⊢ J₁ ∈ π.restrict J ↔ ∃ J' ∈ π, ↑J₁ = ↑J ∩ ↑J'

Tactic:
by
  simp only [mem_restrict, ← Box.withBotCoe_inj, Box.coe_inf, Box.coe_coe]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
x : E
h : Tendsto (fun r ↦ μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)
t : Set E
ht : MeasurableSet t
h''t : μ t ≠ ∞
ε : ℝ≥0∞
εpos : 0 < ε
h't : μ t ≠ 0
n : ℕ
npos : 0 < n
hn : μ (t \ closedBall 0 ↑n) < ε / 2 * μ t
L : Tendsto (fun r ↦ μ (s ∩ ({x} + r • (t ∩ closedBall 0 ↑n))) / μ ({x} + r • t)) (𝓝[>] 0) (𝓝 0)
r : ℝ
hr : μ (s ∩ ({x} + r • (t ∩ closedBall 0 ↑n))) / μ ({x} + r • t) < ε / 2
rpos : 0 < r
I : μ (s ∩ ({x} + r • t)) ≤ μ (s ∩ ({x} + r • (t ∩ closedBall 0 ↑n))) + μ ({x} + r • (t \ closedBall 0 ↑n))
⊢ (μ (s ∩ ({x} + r • (t ∩ closedBall 0 ↑n))) + μ ({x} + r • (t \ closedBall 0 ↑n))) / μ ({x} + r • t) < ε / 2 + ε / 2

Tactic:
ENNReal.add_div

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
x : E
h : Tendsto (fun r ↦ μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 0)
t : Set E
ht : MeasurableSet t
h''t : μ t ≠ ∞
ε : ℝ≥0∞
εpos : 0 < ε
h't : μ t ≠ 0
n : ℕ
npos : 0 < n
hn : μ (t \ closedBall 0 ↑n) < ε / 2 * μ t
L : Tendsto (fun r ↦ μ (s ∩ ({x} + r • (t ∩ closedBall 0 ↑n))) / μ ({x} + r • t)) (𝓝[>] 0) (𝓝 0)
r : ℝ
hr : μ (s ∩ ({x} + r • (t ∩ closedBall 0 ↑n))) / μ ({x} + r • t) < ε / 2
rpos : 0 < r
I : μ (s ∩ ({x} + r • t)) ≤ μ (s ∩ ({x} + r • (t ∩ closedBall 0 ↑n))) + μ ({x} + r • (t \ closedBall 0 ↑n))
⊢ μ (s ∩ ({x} + r • (t ∩ closedBall 0 ↑n))) / μ ({x} + r • t) + μ ({x} + r • (t \ closedBall 0 ↑n)) / μ ({x} + r • t) <
    ε / 2 + ε / 2
Module: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction

Goal state before:
pp: case refine_2
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
r : (ι → ℝ) → ↑(Ioi 0)
z : ι → ℝ
x✝ : z ∈ Box.Icc I
⊢ ∃ U ∈ 𝓝[Box.Icc I] z,
    ∀ J ≤ I,
      ∀ (m : ℕ),
        z ∈ Box.Icc J →
          Box.Icc J ⊆ U →
            (∀ (i : ι), J.upper i - J.lower i = (I.upper i - I.lower i) / 2 ^ m) →
              ∃ π,
                π.IsPartition ∧
                  π.IsHenstock ∧
                    π.IsSubordinate r ∧
                      (∀ J_1 ∈ π, ∃ m, ∀ (i : ι), J_1.upper i - J_1.lower i = (J.upper i - J.lower i) / 2 ^ m) ∧
                        π.distortion = J.distortion

Tactic:
· refine ⟨Box.Icc I ∩ closedBall z (r z),
      inter_mem_nhdsWithin _ (closedBall_mem_nhds _ (r z).coe_prop), ?_⟩
    intro J _ n Hmem HIcc Hsub
    rw [Set.subset_inter_iff] at HIcc
    refine ⟨single _ _ le_rfl _ Hmem, isPartition_single _, isHenstock_single _,
      (isSubordinate_single _ _).2 HIcc.2, ?_, distortion_single _ _⟩
    simp only [TaggedPrepartition.mem_single, forall_eq]
    refine ⟨0, fun i => ?_⟩
    simp

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

Goal state before:
pp: case refine_1
K : Type u_1
inst✝⁹ : NormedField K
inst✝⁸ : LinearOrder K
inst✝⁷ : IsStrictOrderedRing K
inst✝⁶ : HasSolidNorm K
inst✝⁵ : FloorRing K
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace K E
inst✝² : FiniteDimensional K E
inst✝¹ : ProperSpace E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
hs : IsZLattice K L
this✝³ : Module.Finite ℤ ↥L
this✝² : Module ℚ E
this✝¹ : IsAddTorsionFree E
b₀ : Basis (Free.ChooseBasisIndex ℤ ↥L) ℤ ↥L := Free.chooseBasis ℤ ↥L
b : Free.ChooseBasisIndex ℤ ↥L → E := Subtype.val ∘ ⇑b₀
this✝ : LinearIndependent ℤ b
h_spanL : span ℤ (Set.range b) = L
h_spanE : span K (Set.range b) = ⊤
h_card : Fintype.card (Free.ChooseBasisIndex ℤ ↥L) = (Set.range b).toFinset.card
t : Set E
ht_inc : t ⊆ Set.range b
ht_span : span K t = span K (Set.range b)
ht_lin : LinearIndependent K Subtype.val
e : Basis (↑t) K E := Basis.mk ht_lin ⋯
this : Fintype ↑t
h : finrank K E < Fintype.card (Free.ChooseBasisIndex ℤ ↥L)
v : E
hv : v ∈ Set.range b \ Set.range ⇑e
a✝ : LinearIndepOn ℚ id (Set.range ⇑e)
h_mapsto : Set.MapsTo (fun n ↦ fract e (n • v)) Set.univ (Metric.closedBall 0 (∑ i, ‖e i‖) ∩ ↑L)
h_finite : (Metric.closedBall 0 (∑ i, ‖e i‖) ∩ ↑L).Finite
n m : ℤ
h_ne : n ≠ m
h_eq : fract e (n • v) = fract e (m • v)
h_nz : -↑n + ↑m ≠ 0
⊢ (-↑n + ↑m) • v ∈ ↑(span ℤ (Set.range ⇑e))

Tactic:
rwa [add_smul, neg_smul, SetLike.mem_coe, ← fract_eq_fract, Int.cast_smul_eq_zsmul ℚ,
      Int.cast_smul_eq_zsmul ℚ]

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Goal state before:
pp: case h0
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
hs : MeasurableSet s
x : E
h : Tendsto (fun r ↦ μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)
t : Set E
ht : MeasurableSet t
h't : μ t ≠ 0
h''t : μ t ≠ ∞
I : ∀ (u v : Set E), μ u ≠ 0 → μ u ≠ ∞ → MeasurableSet v → μ u / μ u - μ (vᶜ ∩ u) / μ u = μ (v ∩ u) / μ u
r : ℝ
hr : r ∈ Ioi 0
⊢ μ (closedBall x r) ≠ 0

Tactic:
exact (measure_closedBall_pos μ _ hr).ne'

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

Goal state before:
pp: ι : Type u_1
𝕜 : Type u_3
inst✝¹ : RCLike 𝕜
inst✝ : Fintype ι
x : EuclideanSpace 𝕜 ι
i : ι
⊢ ⟪(basisFun ι 𝕜) i, x⟫ = x.ofLp i

Tactic:
simp [← OrthonormalBasis.repr_apply_apply]

Goal state after:
Module: Mathlib.Analysis.BoxIntegral.Partition.Split

Goal state before:
pp: ι : Type u_1
I : Box ι
inst✝ : Finite ι
π : Prepartition I
h : π.IsPartition
⊢ π.compl = ⊥

Tactic:
rw [← iUnion_eq_empty, iUnion_compl, h.iUnion_eq, sdiff_self]

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

Goal state before:
pp: K : Type u_1
inst✝⁴ : NormedField K
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace K F
L : Submodule ℤ E
e : F ≃ₗ[K] E
x✝ : ↥(ZLattice.comap K L ↑e)
x : F
hx : x ∈ ZLattice.comap K L ↑e
⊢ ((↑ℤ ↑e.symm).restrict ⋯) ⟨e x, ⋯⟩ = ⟨x, hx⟩

Tactic:
by simp [Subtype.ext_iff]

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 ι
A : ι → Submodule 𝕜 E
inst✝¹ : DecidableEq ι
h : IsInternal A
α : ι → Type u_7
inst✝ : (i : ι) → Fintype (α i)
hV : OrthogonalFamily 𝕜 (fun i ↦ ↥(A i)) fun i ↦ (A i).subtypeₗᵢ
v : (i : ι) → OrthonormalBasis (α i) 𝕜 ↥(A i)
a : (i : ι) × α i
⊢ (collectedOrthonormalBasis hV h v) a ∈ A a.fst

Tactic:
by
  simp [DirectSum.IsInternal.collectedOrthonormalBasis]

Goal state after:
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)) ≤ ε}
S_open : ∀ r > 0, IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (S r)
x : E
hx : x ∈ K
⊢ x ∈ ⋃ r, ⋃ (_ : r > 0), S r

Tactic:
have : oscillationWithin f D x < ε := hK x hx

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)) ≤ ε}
S_open : ∀ r > 0, IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (S r)
x : E
hx : x ∈ K
this : oscillationWithin f D x < ε
⊢ x ∈ ⋃ r, ⋃ (_ : r > 0), S r
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Finite ι
x : ι → ℝ
hx : x ∈ (↑n)⁻¹ • span ℤ (Set.range ⇑(Pi.basisFun ℝ ι))
⊢ tag n (index n x) = x

Tactic:
rw [mem_smul_span_iff] at hx
  ext i
  obtain ⟨a, ha⟩ : ∃ a : ℤ, a = n * x i := hx i
  rwa [tag_apply, index_apply, Int.cast_sub, Int.cast_one, sub_add_cancel, ← ha, Int.ceil_intCast,
    div_eq_iff (NeZero.ne _), mul_comm]

Goal state after:
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
a : ι
⊢ a ∈ Finset.Iio n → (𝕜 ∙ gramSchmidt 𝕜 f a).starProjection (f n) ∈ span 𝕜 (gramSchmidt 𝕜 f '' Set.Iio n)

Tactic:
ha

Goal state after:
𝕜 : 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
a : ι
ha : a ∈ Finset.Iio n
⊢ (𝕜 ∙ gramSchmidt 𝕜 f a).starProjection (f n) ∈ span 𝕜 (gramSchmidt 𝕜 f '' Set.Iio n)
Module: Mathlib.Analysis.BoxIntegral.Basic

Goal state before:
pp: case insert
ι : 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
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
α : Type u_1
f : α → (ι → ℝ) → E
g : α → F
a : α
s : Finset α
ha : a ∉ s
ihs : (∀ i ∈ s, HasIntegral I l (f i) vol (g i)) → HasIntegral I l (fun x ↦ ∑ i ∈ s, f i x) vol (∑ i ∈ s, g i)
h : ∀ i ∈ insert a s, HasIntegral I l (f i) vol (g i)
⊢ HasIntegral I l (fun x ↦ ∑ i ∈ insert a s, f i x) vol (∑ i ∈ insert a s, g i)

Tactic:
simp only [Finset.sum_insert ha]; rw [Finset.forall_mem_insert] at h
    exact h.1.add (ihs h.2)

Goal state after:
Module: Mathlib.Analysis.SumOverResidueClass

Goal state before:
pp: case neg
m : ℕ
inst✝ : NeZero m
f : ℕ → ℝ
hf : Antitone f
k l : ZMod m
hs : Summable ({n | ↑n = k}.indicator f)
hf₀ : ∃ n, f n < 0
⊢ Summable ({n | ↑n = l}.indicator f)

Tactic:
obtain ⟨n, hn⟩ := hf₀

Goal state after:
case neg
m : ℕ
inst✝ : NeZero m
f : ℕ → ℝ
hf : Antitone f
k l : ZMod m
hs : Summable ({n | ↑n = k}.indicator f)
n : ℕ
hn : f n < 0
⊢ Summable ({n | ↑n = l}.indicator f)
Module: Mathlib.Analysis.SumOverResidueClass

Goal state before:
pp: m : ℕ
inst✝ : NeZero m
f : ℕ → ℝ
hf : Antitone f
k : ZMod m
⊢ Summable ({n | ↑n = k}.indicator f) ↔ Summable f

Tactic:
refine ⟨fun H ↦ ?_, fun H ↦ Summable.indicator H _⟩
  rw [Finset.sum_indicator_mod m f]
  convert!
    summable_sum (s := Finset.univ) fun a _ ↦
      summable_indicator_mod_iff_summable_indicator_mod hf a H
  simp only [Finset.sum_apply]

Goal state after:
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:
by
  refine (h.isBigO_const (one_ne_zero' ℝ)).trans_isLittleO (isLittleO_const_left.2 <| Or.inr ?_)
  simp only [Function.comp_def, norm_inv]
  exact (tendsto_norm_sub_self_nhdsNE a).inv_tendsto_nhdsGT_zero

Goal state after:
Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics

Goal state before:
pp: case h
α : Type u_1
u v : α → ℝ
l : Filter α
hv : 0 ≤ v
h : u ~[l] v
r : ℝ
φ : α → ℝ
hφ : Tendsto φ l (𝓝 1)
huφv : u =ᶠ[l] φ * v
hφr : Tendsto ((fun x ↦ x ^ r) ∘ φ) l (𝓝 1)
⊢ u ^ r =ᶠ[l] fun x ↦ φ x ^ r * v x ^ r

Tactic:
filter_upwards [Tendsto.eventually_const_lt (zero_lt_one) hφ, huφv] with x hφ_pos huv'

Goal state after:
α : Type u_1
u v : α → ℝ
l : Filter α
hv : 0 ≤ v
h : u ~[l] v
r : ℝ
φ : α → ℝ
hφ : Tendsto φ l (𝓝 1)
huφv : u =ᶠ[l] φ * v
hφr : Tendsto ((fun x ↦ x ^ r) ∘ φ) l (𝓝 1)
x : α
hφ_pos : 0 < φ x
huv' : u x = (φ * v) x
⊢ (u ^ r) x = φ x ^ r * v x ^ r
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
n : ℕ
⊢ f 0 + ∑ x ∈ range n, 2 ^ x * f (2 ^ x) ≤ f 0 + ∑' (k : ℕ), 2 ^ k * f (2 ^ k)

Tactic:
ENNReal.sum_le_tsum

Goal state after:
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
n : ℕ
⊢ f 0 + ∑' (x : ℕ), 2 ^ x * f (2 ^ x) ≤ f 0 + ∑' (k : ℕ), 2 ^ k * f (2 ^ k)
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: C : ℕ
u : ℕ → ℕ
h_pos : ∀ (n : ℕ), 0 < u n
hu_strict : StrictMono u
hC_nonzero : C ≠ 0
h_succ_diff : SuccDiffBounded C u
f : ℕ → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → (fun i ↦ ↑(f i)) n ≤ (fun i ↦ ↑(f i)) m
⊢ (Summable fun k ↦ (↑(u (k + 1)) - ↑(u k)) * (fun i ↦ ↑(f i)) (u k)) ↔ Summable fun i ↦ ↑(f i)

Tactic:
simp only [NNReal.coe_le_coe] at *

Goal state after:
C : ℕ
u : ℕ → ℕ
h_pos : ∀ (n : ℕ), 0 < u n
hu_strict : StrictMono u
hC_nonzero : C ≠ 0
h_succ_diff : SuccDiffBounded C u
f : ℕ → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
⊢ (Summable fun k ↦ (↑(u (k + 1)) - ↑(u k)) * ↑(f (u k))) ↔ Summable fun i ↦ ↑(f i)
Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics

Goal state before:
pp: case mpr.ht
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
D : Type u_2
inst✝ : TopologicalSpace D
f : D → E
hf : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
c : ℝ
t : Set D
hcompact : IsCompact t
h : tᶜ ⊆ {x | ‖f x‖ ≤ c}
⊢ ∃ C, ∀ x ∈ f '' tᶜ, ‖x‖ ≤ C

Tactic:
refine ⟨c, fun x hx ↦ ?_⟩

Goal state after:
case mpr.ht
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
D : Type u_2
inst✝ : TopologicalSpace D
f : D → E
hf : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
c : ℝ
t : Set D
hcompact : IsCompact t
h : tᶜ ⊆ {x | ‖f x‖ ≤ c}
x : E
hx : x ∈ f '' tᶜ
⊢ ‖x‖ ≤ c
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: case inl
p : ℝ
hp : 0 ≤ p
⊢ (Summable fun k ↦ 2 ^ ↑k * (2 ^ (↑k * p))⁻¹) ↔ 1 < p

Tactic:
mul_comm _ p,

Goal state after:
case inl
p : ℝ
hp : 0 ≤ p
⊢ (Summable fun k ↦ 2 ^ ↑k * (2 ^ (p * ↑k))⁻¹) ↔ 1 < p
Module: Mathlib.Data.Finset.SMulAntidiagonal

Goal state before:
pp: case mp
G : Type u_1
P : Type u_2
inst✝³ : LinearOrder G
inst✝² : LinearOrder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
s : Set G
t : Set P
hs : s.IsWF
ht : t.IsWF
hns : s.Nonempty
hnt : t.Nonempty
b : P
hat : b ∈ t
has : hs.min hns ∈ s
hst : hs.min hns • b = hs.min hns • ht.min hnt
⊢ hs.min hns = hs.min hns ∧ b = ht.min hnt

Tactic:
exact ⟨rfl, IsCancelSMul.left_cancel _ _ _ hst⟩

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

Goal state before:
pp: σ : Type u
R : Type v
inst✝² : CommSemiring R
inst✝¹ : Nonempty σ
inst✝ : Nontrivial R
⊢ #(MvPolynomial σ R) = max (max (lift.{u, v} #R) (lift.{v, u} #σ)) ℵ₀

Tactic:
simp [sup_assoc]

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

Goal state before:
pp: σ R : Type u
inst✝² : CommSemiring R
inst✝¹ : Nonempty σ
inst✝ : Nontrivial R
⊢ #(MvPolynomial σ R) = max (max #R #σ) ℵ₀

Tactic:
simp [sup_assoc]

Goal state after:
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 : σ
⊢ (g.comp f) (X i) = (aeval fun i ↦ g (X i)) (f (X i))

Tactic:
rw [AlgHom.comp_apply]

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 (f (X i)) = (aeval fun i ↦ g (X i)) (f (X i))
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: case pos
α : Type u_1
a : α
f : α →₀ ℕ
h : a ∈ f.support
⊢ Nat.multinomial f.support ⇑f =
    (f.sum fun x ↦ id).choose (f a) * Nat.multinomial (f.update a 0).support ⇑(f.update a 0)

pp: case neg
α : Type u_1
a : α
f : α →₀ ℕ
h : a ∉ f.support
⊢ Nat.multinomial f.support ⇑f =
    (f.sum fun x ↦ id).choose (f a) * Nat.multinomial (f.update a 0).support ⇑(f.update a 0)

Tactic:
· rw [← Finset.insert_erase h, Nat.multinomial_insert (Finset.notMem_erase a _),
        Finset.add_sum_erase _ f h, support_update_zero]
      congr 1
      exact Nat.multinomial_congr fun _ h ↦ (Function.update_of_ne (mem_erase.1 h).1 0 f).symm

Goal state after:
case neg
α : Type u_1
a : α
f : α →₀ ℕ
h : a ∉ f.support
⊢ Nat.multinomial f.support ⇑f =
    (f.sum fun x ↦ id).choose (f a) * Nat.multinomial (f.update a 0).support ⇑(f.update a 0)
Module: Mathlib.Algebra.MvPolynomial.Nilpotent

Goal state before:
pp: case refine_3
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
P✝ : MvPolynomial σ R
inst✝¹ : Finite σ
this : Fintype σ
α : Type u_1
inst✝ : Fintype α
H : ∀ (x : MvPolynomial α R), IsNilpotent x ↔ ∀ (i : α →₀ ℕ), IsNilpotent (coeff i x)
P : MvPolynomial (Option α) R
⊢ IsNilpotent P ↔ ∀ (i : Option α →₀ ℕ), IsNilpotent (coeff i P)

Tactic:
obtain ⟨P, rfl⟩ := (optionEquivLeft _ _).symm.surjective P

Goal state after:
case refine_3
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
P✝ : MvPolynomial σ R
inst✝¹ : Finite σ
this : Fintype σ
α : Type u_1
inst✝ : Fintype α
H : ∀ (x : MvPolynomial α R), IsNilpotent x ↔ ∀ (i : α →₀ ℕ), IsNilpotent (coeff i x)
P : Polynomial (MvPolynomial α R)
⊢ IsNilpotent ((optionEquivLeft R α).symm P) ↔
    ∀ (i : Option α →₀ ℕ), IsNilpotent (coeff i ((optionEquivLeft R α).symm P))
Module: Mathlib.Algebra.MvPolynomial.Division

Goal state before:
pp: case inl
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
n : σ →₀ ℕ
hR : Subsingleton R
⊢ p ∣ (monomial n) 1 * q ↔ ∃ m r, m ≤ n ∧ r ∣ q ∧ p = (monomial m) 1 * r

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

Tactic:
· simp only [Subsingleton.elim _ p, dvd_refl, and_self, and_true, exists_const, true_iff]
    refine ⟨n, le_refl n⟩

Goal state after:
case inr
σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p q : MvPolynomial σ R
inst✝ : IsCancelMulZero R
n : σ →₀ ℕ
hR : Nontrivial R
⊢ p ∣ (monomial n) 1 * q ↔ ∃ m r, m ≤ n ∧ r ∣ q ∧ p = (monomial m) 1 * r
Module: Mathlib.Algebra.MvPolynomial.Nilpotent

Goal state before:
pp: case neg
σ : Type u_1
R : Type u_2
inst✝ : CommRing R
n : ℕ
P : MvPolynomial (Fin n) R
f : Fin n ↪ σ
H✝ : ∀ (i : Fin n →₀ ℕ), IsNilpotent (coeff i P)
i : σ →₀ ℕ
H : i ∉ Set.range (Finsupp.embDomain f)
⊢ IsNilpotent (coeff i ((rename ⇑f) P))

Tactic:
rw [coeff_rename_eq_zero]

Goal state after:
case neg
σ : Type u_1
R : Type u_2
inst✝ : CommRing R
n : ℕ
P : MvPolynomial (Fin n) R
f : Fin n ↪ σ
H✝ : ∀ (i : Fin n →₀ ℕ), IsNilpotent (coeff i P)
i : σ →₀ ℕ
H : i ∉ Set.range (Finsupp.embDomain f)
⊢ IsNilpotent 0

case neg.h
σ : Type u_1
R : Type u_2
inst✝ : CommRing R
n : ℕ
P : MvPolynomial (Fin n) R
f : Fin n ↪ σ
H✝ : ∀ (i : Fin n →₀ ℕ), IsNilpotent (coeff i P)
i : σ →₀ ℕ
H : i ∉ Set.range (Finsupp.embDomain f)
⊢ ∀ (u : Fin n →₀ ℕ), Finsupp.mapDomain (⇑f) u = i → coeff u P = 0
Module: Mathlib.Algebra.MvPolynomial.Polynomial

Goal state before:
pp: R : Type u_1
n : ℕ
x : Fin n → R
inst✝ : CommSemiring R
f : MvPolynomial (Fin (n + 1)) R
q : MvPolynomial (Fin n) R
| (eval x).comp ((Polynomial.evalRingHom q).comp (Polynomial.C.comp C))

Tactic:
refine @RingHom.ext _ _ _ _ _ (RingHom.id _) fun r => ?_
    simp

Goal state after:
R : Type u_1
n : ℕ
x : Fin n → R
inst✝ : CommSemiring R
f : MvPolynomial (Fin (n + 1)) R
q : MvPolynomial (Fin n) R
r : R
| r
Module: Mathlib.Data.DFinsupp.WellFounded

Goal state before:
pp: case pos
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → x j = if j ∈ p then x₁ j else x₂ j
hp : i ∉ p
hs : s i (x i) (x₂ i)
j : ι
h₁ : ¬(r j i ∧ j ∈ p)
h₂ : r j i
⊢ x₂ j = x j

Tactic:
rw [hr j h₂, if_neg]

Goal state after:
case pos.hnc
ι : Type u_1
α : ι → Type u_2
inst✝¹ : (i : ι) → Zero (α i)
r : ι → ι → Prop
s : (i : ι) → α i → α i → Prop
inst✝ : (i : ι) → (s : Set ι) → Decidable (i ∈ s)
p : Set ι
x₁ x₂ x : Π₀ (i : ι), α i
i : ι
hr : ∀ (j : ι), r j i → x j = if j ∈ p then x₁ j else x₂ j
hp : i ∉ p
hs : s i (x i) (x₂ i)
j : ι
h₁ : ¬(r j i ∧ j ∈ p)
h₂ : r j i
⊢ j ∉ p
Module: Mathlib.Algebra.MvPolynomial.NoZeroDivisors

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f g : MvPolynomial σ R
hf : f ≠ 0
hg : g ≠ 0
⊢ (f * g).totalDegree = f.totalDegree + g.totalDegree

Tactic:
cases exists_wellFoundedGT σ
  simp [← degree_degLexDegree, MonomialOrder.degree_mul hf hg]

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

Goal state before:
pp: case inr
R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
hR : Nontrivial R
⊢ p ∣ (monomial n) 1 ↔ ∃ m u, m ≤ n ∧ IsUnit u ∧ p = (monomial m) u

Tactic:
dvd_monomial_iff_exists (one_ne_zero' R)

Goal state after:
case inr
R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
hR : Nontrivial R
⊢ (∃ m b, m ≤ n ∧ b ∣ 1 ∧ p = (monomial m) b) ↔ ∃ m u, m ≤ n ∧ IsUnit u ∧ p = (monomial m) u
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
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
this : m.toSyn (m.degree g) < m.toSyn e
⊢ coeff d f * coeff e g = 0

Tactic:
rw [m.coeff_eq_zero_of_lt this, mul_zero]

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:
by
  rw [← card_sym_fin_eq_multichoose]
  exact card_congr (equivCongr (equivFin α))

Goal state after: