mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Normed.Lp.ProdLp

Goal state before:
pp: case inr.inr
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
α' : Type u_5
β' : Type u_6
hp✝ : Fact (1 ≤ p)
inst✝⁵ : PseudoEMetricSpace α
inst✝⁴ : PseudoEMetricSpace β
inst✝³ : PseudoEMetricSpace γ
inst✝² : PseudoEMetricSpace α'
inst✝¹ : PseudoEMetricSpace β'
inst✝ : Unique β
x y : WithLp p (α × β)
hp : 0 < p.toReal
⊢ edist x.fst y.fst = (edist x.fst y.fst ^ p.toReal + 0) ^ (1 / p.toReal)

Tactic:
add_zero,

Goal state after:
case inr.inr
p : ℝ≥0∞
𝕜 : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
α' : Type u_5
β' : Type u_6
hp✝ : Fact (1 ≤ p)
inst✝⁵ : PseudoEMetricSpace α
inst✝⁴ : PseudoEMetricSpace β
inst✝³ : PseudoEMetricSpace γ
inst✝² : PseudoEMetricSpace α'
inst✝¹ : PseudoEMetricSpace β'
inst✝ : Unique β
x y : WithLp p (α × β)
hp : 0 < p.toReal
⊢ edist x.fst y.fst = (edist x.fst y.fst ^ p.toReal) ^ (1 / p.toReal)
Module: Mathlib.MeasureTheory.Measure.Haar.OfBasis

Goal state before:
pp: case h.left.left
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
v : Basis ι ℝ E
w : Basis ι' ℝ F
x : E × F
t : ι → ℝ
ht1 : t ∈ Icc 0 1
ht2 : x.1 = ∑ i, t i • v i
s : ι' → ℝ
hs1 : s ∈ Icc 0 1
hs2 : x.2 = ∑ i, s i • w i
⊢ 0 ≤ Sum.elim t s

Tactic:
change ∀ x : ι ⊕ ι', 0 ≤ Sum.elim t s x

Goal state after:
case h.left.left
ι : Type u_1
ι' : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
v : Basis ι ℝ E
w : Basis ι' ℝ F
x : E × F
t : ι → ℝ
ht1 : t ∈ Icc 0 1
ht2 : x.1 = ∑ i, t i • v i
s : ι' → ℝ
hs1 : s ∈ Icc 0 1
hs2 : x.2 = ∑ i, s i • w i
⊢ ∀ (x : ι ⊕ ι'), 0 ≤ Sum.elim t s x
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 : Submodule ℝ E
hs : s ≠ ⊤
x : E
hx : x ∉ s
c : ℝ
cpos : 0 < c
cone : c < 1
A : Bornology.IsBounded (range fun n ↦ c ^ n • x)
⊢ Pairwise (Disjoint on fun n ↦ {c ^ n • x} + ↑s)

Tactic:
intro m

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 : Submodule ℝ E
hs : s ≠ ⊤
x : E
hx : x ∉ s
c : ℝ
cpos : 0 < c
cone : c < 1
A : Bornology.IsBounded (range fun n ↦ c ^ n • x)
m : ℕ
⊢ ∀ ⦃j : ℕ⦄, m ≠ j → (Disjoint on fun n ↦ {c ^ n • x} + ↑s) m j
Module: Mathlib.Algebra.Module.ZLattice.Basic

Goal state before:
pp: ι : Type u_2
inst✝ : Fintype ι
⊢ fundamentalDomain (Pi.basisFun ℝ ι) = Set.univ.pi fun x ↦ Set.Ico 0 1

Tactic:
by
  ext; simp

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
r : ℝ
hr : 0 ≤ r
s : Set E
⊢ ENNReal.ofReal (|r| ^ finrank ℝ E) * μ s = ENNReal.ofReal (r ^ finrank ℝ E) * μ s

Tactic:
abs_of_nonneg hr

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
r : ℝ
hr : 0 ≤ r
s : Set E
⊢ ENNReal.ofReal (r ^ finrank ℝ E) * μ s = ENNReal.ofReal (r ^ finrank ℝ E) * μ s
Module: Mathlib.Analysis.BoxIntegral.Box.Basic

Goal state before:
pp: ι : Type u_1
I J : Box ι
⊢ [I ≤ J, ↑I ⊆ ↑J, Icc I.lower I.upper ⊆ Icc J.lower J.upper, J.lower ≤ I.lower ∧ I.upper ≤ J.upper].TFAE

Tactic:
tfae_have 1 ↔ 2 := Iff.rfl

Goal state after:
ι : Type u_1
I J : Box ι
tfae_1_iff_2 : I ≤ J ↔ ↑I ⊆ ↑J
⊢ [I ≤ J, ↑I ⊆ ↑J, Icc I.lower I.upper ⊆ Icc J.lower J.upper, J.lower ≤ I.lower ∧ I.upper ≤ J.upper].TFAE
Module: Mathlib.Analysis.InnerProductSpace.PiL2

Goal state before:
pp: n : Type u_7
inst✝ : Fintype n
r : ℝ
hr : 0 ≤ r
⊢ Metric.ball 0 r = {x | ∑ i, x.ofLp i ^ 2 < r ^ 2}

Tactic:
by
  ext x
  have : (0 : ℝ) ≤ ∑ i, x i ^ 2 := Finset.sum_nonneg fun _ _ => sq_nonneg _
  simp_rw [mem_ofPred, mem_ball_zero_iff, norm_eq, norm_eq_abs, sq_abs, sqrt_lt this hr]

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

Goal state before:
pp: ι : Type u_1
I : Box ι
π : TaggedPrepartition I
inst✝ : Fintype ι
h : π.IsHenstock
x : ι → ℝ
⊢ #({J ∈ π.boxes | π.tag J = x}) ≤ #({J ∈ π.boxes | x ∈ Box.Icc J})

Tactic:
refine Finset.card_le_card fun J hJ => ?_

Goal state after:
ι : Type u_1
I : Box ι
π : TaggedPrepartition I
inst✝ : Fintype ι
h : π.IsHenstock
x : ι → ℝ
J : Box ι
hJ : J ∈ {J ∈ π.boxes | π.tag J = x}
⊢ J ∈ {J ∈ π.boxes | x ∈ Box.Icc J}
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, 0 < n ∧ μ (t \ closedBall 0 ↑n) < ε / 2 * μ t

Tactic:
have A :
      Tendsto (fun n : ℕ => μ (t \ closedBall 0 n)) atTop
        (𝓝 (μ (⋂ n : ℕ, t \ closedBall 0 n))) := by
      have N : ∃ n : ℕ, μ (t \ closedBall 0 n) ≠ ∞ :=
        ⟨0, ((measure_mono sdiff_subset).trans_lt h''t.lt_top).ne⟩
      refine tendsto_measure_iInter_atTop
        (fun n ↦ (ht.diff measurableSet_closedBall).nullMeasurableSet) (fun m n hmn ↦ ?_) N
      exact sdiff_subset_sdiff Subset.rfl (by gcongr)
    have : ⋂ n : ℕ, t \ closedBall 0 n = ∅ := by
      simp_rw [sdiff_eq, ← inter_iInter, iInter_eq_compl_iUnion_compl, compl_compl,
        iUnion_closedBall_nat, compl_univ, inter_empty]
    simp only [this, measure_empty] at A
    have I : 0 < ε / 2 * μ t := ENNReal.mul_pos (ENNReal.half_pos εpos.ne').ne' h't
    exact (Eventually.and (Ioi_mem_atTop 0) ((tendsto_order.1 A).2 _ I)).exists

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

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
p : Box ι → Prop
I : Box ι
H_ind : ∀ J ≤ I, (∀ J' ∈ splitCenter J, p J') → p J
H_nhds :
  ∀ 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) → p J
J : Box ι
hle : J ≤ I
hs : ∀ (s : Set ι), p (J.splitCenterBox s)
J' : Box ι
h' : J' ∈ splitCenter J
⊢ p J'

Tactic:
rcases mem_splitCenter.1 h' with ⟨s, rfl⟩

Goal state after:
ι : Type u_1
inst✝ : Fintype ι
p : Box ι → Prop
I : Box ι
H_ind : ∀ J ≤ I, (∀ J' ∈ splitCenter J, p J') → p J
H_nhds :
  ∀ 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) → p J
J : Box ι
hle : J ≤ I
hs : ∀ (s : Set ι), p (J.splitCenterBox s)
s : Set ι
h' : J.splitCenterBox s ∈ splitCenter J
⊢ p (J.splitCenterBox s)
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 ι
U : Submodule 𝕜 E
inst✝ : U.HasOrthogonalProjection
b : OrthonormalBasis ι 𝕜 ↥U
⊢ U.starProjection = ∑ i, ((InnerProductSpace.rankOne 𝕜) ↑(b i)) ↑(b i)

Tactic:
by
  ext; simp [starProjection, b.orthogonalProjectionOnto_eq_sum_rankOne]

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

Goal state before:
pp: ι : Type u_7
𝕜 : Type u_8
inst✝¹ : Unique ι
inst✝ : RCLike 𝕜
⊢ ⇑(OrthonormalBasis.singleton ι 𝕜) = 1

Tactic:
by
  ext; simp

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

Goal state before:
pp: case refine_2
ι : Type u_1
I J Js : Box ι
s : Finset (ι × ℝ)
HJs : Js ∈ splitMany I s
Hn : ¬Disjoint ↑J ↑Js
H : ∀ (i : ι), (i, J.lower i) ∈ s ∧ (i, J.upper i) ∈ s
x : ι → ℝ
hx : x ∈ ↑J
hxs : x ∈ ↑Js
y : ι → ℝ
hy : y ∈ Js
i : ι
Jl : Box ι
Hmem : Jl ∈ split I i (J.upper i)
Hle : Js ≤ Jl
this : x ∈ Jl
⊢ y i ≤ J.upper i

Tactic:
rw [← Box.coe_subset_coe, coe_eq_of_mem_split_of_mem_le Hmem this (hx i).2] at Hle

Goal state after:
case refine_2
ι : Type u_1
I J Js : Box ι
s : Finset (ι × ℝ)
HJs : Js ∈ splitMany I s
Hn : ¬Disjoint ↑J ↑Js
H : ∀ (i : ι), (i, J.lower i) ∈ s ∧ (i, J.upper i) ∈ s
x : ι → ℝ
hx : x ∈ ↑J
hxs : x ∈ ↑Js
y : ι → ℝ
hy : y ∈ Js
i : ι
Jl : Box ι
Hmem : Jl ∈ split I i (J.upper i)
Hle : ↑Js ⊆ ↑I ∩ {y | y i ≤ J.upper i}
this : x ∈ Jl
⊢ y i ≤ J.upper i
Module: Mathlib.Analysis.BoxIntegral.Partition.Split

Goal state before:
pp: case intro
ι : Type u_1
inst✝ : Finite ι
s : Finset (Box ι)
val✝ : Fintype ι
⊢ ∀ᶠ (t : Finset (ι × ℝ)) in atTop, ∀ (I J : Box ι), J ∈ s → ∀ J' ∈ splitMany I t, ¬Disjoint ↑J ↑J' → J' ≤ J

Tactic:
refine eventually_atTop.2
    ⟨s.biUnion fun J => Finset.univ.biUnion fun i => {(i, J.lower i), (i, J.upper i)},
      fun t ht I J hJ J' hJ' => not_disjoint_imp_le_of_subset_of_mem_splitMany (fun i => ?_) hJ'⟩

Goal state after:
case intro
ι : Type u_1
inst✝ : Finite ι
s : Finset (Box ι)
val✝ : Fintype ι
t : Finset (ι × ℝ)
ht : (s.biUnion fun J ↦ Finset.univ.biUnion fun i ↦ {(i, J.lower i), (i, J.upper i)}) ⊆ t
I J : Box ι
hJ : J ∈ s
J' : Box ι
hJ' : J' ∈ splitMany I t
i : ι
⊢ {(i, J.lower i), (i, J.upper i)} ⊆ t
Module: Mathlib.Analysis.BoxIntegral.Partition.Filter

Goal state before:
pp: ι : Type u_2
l : IntegrationParams
hl : l.bRiemann = false
r : (ι → ℝ) → ↑(Set.Ioi 0)
⊢ l.RCond r

Tactic:
by
  simp [RCond, hl]

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

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
r : (ι → ℝ) → ↑(Set.Ioi 0)
π : Prepartition I
πi : (J : Box ι) → TaggedPrepartition J
h : ∀ J ∈ π, l.MemBaseSet J c r (πi J)
hp : ∀ J ∈ π, (πi J).IsPartition
hc : l.bDistortion = true → π.compl.distortion ≤ c
⊢ l.MemBaseSet I c r (π.biUnionTagged πi)

Tactic:
by
  refine ⟨TaggedPrepartition.isSubordinate_biUnionTagged.2 fun J hJ => (h J hJ).1,
    fun hH => TaggedPrepartition.isHenstock_biUnionTagged.2 fun J hJ => (h J hJ).2 hH,
    fun hD => ?_, fun hD => ?_⟩
  · rw [Prepartition.distortion_biUnionTagged, Finset.sup_le_iff]
    exact fun J hJ => (h J hJ).3 hD
  · refine ⟨_, ?_, hc hD⟩
    rw [π.iUnion_compl, ← π.iUnion_biUnion_partition hp]
    rfl

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

Goal state before:
pp: ι : Type u_1
M✝ : Type u_2
n : ℕ
N : Type u_3
inst✝² : AddCommMonoid M✝
inst✝¹ : AddCommMonoid N
I₀ : WithTop (Box ι)
I✝ : Box ι
i : ι
M : Type u_4
inst✝ : AddCommGroup M
f : ι →ᵇᵃ[I₀] M
I : Box ι
hI : ↑I ≤ I₀
π : Prepartition I
hπ : π.IsPartition
⊢ ∑ Ji ∈ π.boxes, (-⇑f) Ji = (-⇑f) I

Tactic:
by
      simp only [Pi.neg_apply, Finset.sum_neg_distrib, sum_partition_boxes _ hI hπ]

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)
S_cover : K ⊆ ⋃ r, ⋃ (_ : r > 0), S r
S_antitone : ∀ (r₁ r₂ : ℝ), r₁ ≤ r₂ → S r₂ ⊆ S r₁
⊢ ∃ r > 0, K ⊆ S r

Tactic:
by
    obtain ⟨T, Tb, Tfin, hT⟩ := comp.elim_finite_subcover_image S_open S_cover
    by_cases T_nonempty : T.Nonempty
    · use Tfin.isWF.min T_nonempty, Tb (Tfin.isWF.min_mem T_nonempty)
      intro x hx
      obtain ⟨r, hr⟩ := mem_iUnion.1 (hT hx)
      simp only [mem_iUnion, exists_prop] at hr
      exact (S_antitone _ r (IsWF.min_le Tfin.isWF T_nonempty hr.1)) hr.2
    · rw [not_nonempty_iff_eq_empty] at T_nonempty
      use 1, one_pos, subset_trans hT (by simp [T_nonempty])

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

Goal state before:
pp: case refine_1
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
s : Set (ι → ℝ)
hs₁ : NullMeasurableSet s volume
hs₂ : volume s ≠ ⊤
ν : ι → ℤ
⊢ NullMeasurableSet (↑(box n ν)) volume

Tactic:
exact (box n ν).measurableSet_coe.nullMeasurableSet

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
I : Box ι
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
π₁ π₂ : TaggedPrepartition I
h : Disjoint π₁.iUnion π₂.iUnion
⊢ integralSum f vol (π₁.disjUnion π₂ h) = integralSum f vol π₁ + integralSum f vol π₂

Tactic:
by
  refine (Prepartition.sum_disj_union_boxes h _).trans
      (congr_arg₂ (· + ·) (sum_congr rfl fun J hJ => ?_) (sum_congr rfl fun J hJ => ?_))
  · rw [disjUnion_tag_of_mem_left _ hJ]
  · rw [disjUnion_tag_of_mem_right _ hJ]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
⊢ ↑↑K.orthogonalDecomposition =
    ↑(WithLp.prodContinuousLinearEquiv 2 𝕜 ↥K ↥Kᗮ).symm ∘SL K.orthogonalProjectionOnto.prod Kᗮ.orthogonalProjectionOnto

Tactic:
by
  ext; simp

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
⊢ WithLp.fstL 2 𝕜 ↥K ↥Kᗮ ∘SL ↑↑K.orthogonalDecomposition = K.orthogonalProjectionOnto

Tactic:
by
  ext; simp

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_4
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : K.HasOrthogonalProjection
⊢ WithLp.sndL 2 𝕜 ↥K ↥Kᗮ ∘SL ↑↑K.orthogonalDecomposition = Kᗮ.orthogonalProjectionOnto

Tactic:
by
  ext; simp

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

Goal state before:
pp: ι : Type u_4
inst✝ : Fintype ι
⊢ volume = map (⇑(MeasurableEquiv.toLp 2 (ι → ℝ))) (addHaarMeasure (Pi.basisFun ℝ ι).parallelepiped)

Tactic:
← Basis.addHaar_def,

Goal state after:
ι : Type u_4
inst✝ : Fintype ι
⊢ volume = map (⇑(MeasurableEquiv.toLp 2 (ι → ℝ))) (Pi.basisFun ℝ ι).addHaar
Module: Mathlib.Analysis.SumOverResidueClass

Goal state before:
pp: case pos
m : ℕ
inst✝ : NeZero m
f : ℕ → ℝ
hf : Antitone f
k l : ZMod m
hs : Summable fun n ↦ f (m * n + k.val)
hf₀ : ∀ (n : ℕ), 0 ≤ f n
hl : ↑l.val + ↑m = l
⊢ Summable fun n ↦ f (m * n + (l.val + m))

Tactic:
exact hs.of_nonneg_of_le (fun _ ↦ hf₀ _)
      fun _ ↦ hf <| Nat.add_le_add Nat.le.refl (k.val_lt.trans_le <| m.le_add_left l.val).le

Goal state after:
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
n : ℕ
⊢ ‖∑ i ∈ Finset.range n, g i‖ = ∑ i ∈ Finset.range n, g i

Tactic:
by
    rwa [Real.norm_eq_abs, abs_sum_of_nonneg']

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: case inl.h_mono
p : ℝ
hp : 0 ≤ p
⊢ ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → (↑n ^ p)⁻¹ ≤ (↑m ^ p)⁻¹

Tactic:
intro m

Goal state after:
case inl.h_mono
p : ℝ
hp : 0 ≤ p
m : ℕ
⊢ ∀ ⦃n : ℕ⦄, 0 < m → m ≤ n → (↑n ^ p)⁻¹ ≤ (↑m ^ p)⁻¹
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
k n : ℕ
⊢ 1 ≤ ↑k + 1

Tactic:
simp only [le_add_iff_nonneg_left, Nat.cast_nonneg]

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: a s : ℝ
⊢ ((Summable fun n ↦ 1 / |↑↑n + a| ^ s) ∧ Summable fun n ↦ 1 / |↑(-↑n) + a| ^ s) ↔ 1 < s

Tactic:
← abs_neg (↑(-_ : ℤ) + a),

Goal state after:
a s : ℝ
⊢ ((Summable fun n ↦ 1 / |↑↑n + a| ^ s) ∧ Summable fun n ↦ 1 / |(-(↑(-↑n) + a))| ^ s) ↔ 1 < s
Module: Mathlib.Data.List.ToFinsupp

Goal state before:
pp: R : Type u_2
inst✝² : AddZeroClass R
x : R
xs : List R
inst✝¹ : DecidablePred fun x_1 ↦ (x :: xs).getD x_1 0 ≠ 0
inst✝ : DecidablePred fun x ↦ xs.getD x 0 ≠ 0
⊢ (x :: xs).toFinsupp = Finsupp.single 0 x + Finsupp.embDomain (addRightEmbedding 1) xs.toFinsupp

Tactic:
convert! toFinsupp_append [x] xs using 3

Goal state after:
case e'_3.e'_5
R : Type u_2
inst✝² : AddZeroClass R
x : R
xs : List R
inst✝¹ : DecidablePred fun x_1 ↦ (x :: xs).getD x_1 0 ≠ 0
inst✝ : DecidablePred fun x ↦ xs.getD x 0 ≠ 0
⊢ Finsupp.single 0 x = [x].toFinsupp

case e'_3.e'_6
R : Type u_2
inst✝² : AddZeroClass R
x : R
xs : List R
inst✝¹ : DecidablePred fun x_1 ↦ (x :: xs).getD x_1 0 ≠ 0
inst✝ : DecidablePred fun x ↦ xs.getD x 0 ≠ 0
⊢ addRightEmbedding 1 = addLeftEmbedding [x].length
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
ha : a ∉ s
f : α → ℕ
⊢ multinomial (cons a s ha) f = (f a + ∑ i ∈ s, f i).choose (f a) * multinomial s f

Tactic:
multinomial,

Goal state after:
α : Type u_1
s : Finset α
a : α
ha : a ∉ s
f : α → ℕ
⊢ (∑ i ∈ cons a s ha, f i)! / ∏ i ∈ cons a s ha, (f i)! = (f a + ∑ i ∈ s, f i).choose (f a) * multinomial s f
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: α : Type u_1
s : Finset α
a : α
ha : a ∉ s
f : α → ℕ
⊢ (∑ i ∈ cons a s ha, f i)! = (f a + ∑ i ∈ s, f i).choose (f a) * multinomial s f * ((f a)! * ∏ x ∈ s, (f x)!)

pp: α : Type u_1
s : Finset α
a : α
ha : a ∉ s
f : α → ℕ
⊢ 0 < ∏ i ∈ cons a s ha, (f i)!

Tactic:
multinomial,

Goal state after:
α : Type u_1
s : Finset α
a : α
ha : a ∉ s
f : α → ℕ
⊢ (∑ i ∈ cons a s ha, f i)! =
    (f a + ∑ i ∈ s, f i).choose (f a) * ((∑ i ∈ s, f i)! / ∏ i ∈ s, (f i)!) * ((f a)! * ∏ x ∈ s, (f x)!)

α : Type u_1
s : Finset α
a : α
ha : a ∉ s
f : α → ℕ
⊢ 0 < ∏ i ∈ cons a s ha, (f i)!
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: a b : ℕ
⊢ multinomial univ ![a, b] = (a + b)! / (a ! * b !)

Tactic:
multinomial,

Goal state after:
a b : ℕ
⊢ (∑ i, ![a, b] i)! / ∏ i, (![a, b] i)! = (a + b)! / (a ! * b !)
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: a b c : ℕ
⊢ multinomial univ ![a, b, c] = (a + b + c)! / (a ! * b ! * c !)

Tactic:
multinomial,

Goal state after:
a b c : ℕ
⊢ (∑ i, ![a, b, c] i)! / ∏ i, (![a, b, c] i)! = (a + b + c)! / (a ! * b ! * c !)
Module: Mathlib.Algebra.MvPolynomial.Nilpotent

Goal state before:
pp: case refine_1
σ : Type u_1
R : Type u_2
inst✝ : CommRing R
P : MvPolynomial σ R
H : IsUnit P
⊢ ∀ (i : σ →₀ ℕ), i ≠ 0 → IsNilpotent (coeff i P)

pp: case refine_2
σ : 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)
⊢ IsUnit P

Tactic:
· intro n hn
    obtain ⟨i, hi⟩ : ∃ i, n i ≠ 0 := by simpa [Finsupp.ext_iff] using hn
    let e := (optionEquivLeft _ _).symm.trans (renameEquiv R (Equiv.optionSubtypeNe i))
    have H := (Polynomial.coeff_isUnit_isNilpotent_of_isUnit (H.map e.symm)).2 (n i) hi
    simp only [ne_eq, isNilpotent_iff] at H
    convert! ← H (n.equivMapDomain (Equiv.optionSubtypeNe i).symm).some
    refine (optionEquivLeft_coeff_some_coeff_none _ _ _ _).trans ?_
    simp [Finsupp.equivMapDomain_eq_mapDomain,
      coeff_rename_mapDomain _ (Equiv.optionSubtypeNe i).symm.injective]

Goal state after:
case refine_2
σ : 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)
⊢ IsUnit P
Module: Mathlib.Algebra.MvPolynomial.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝² : CommSemiring R
p : ℕ
A : Type u_5
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
f : σ → A
⊢ (aeval f).comp (expand p) = aeval (f ^ p)

Tactic:
by
  ext; simp

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

Goal state before:
pp: ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ (multinomial s fun i ↦ 2 * f i) ≤ ((∑ i ∈ s, f i) ^ ∑ i ∈ s, f i) * multinomial s f

Tactic:
multinomial,

Goal state after:
ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ (∑ i ∈ s, 2 * f i)! / ∏ i ∈ s, (2 * f i)! ≤ ((∑ i ∈ s, f i) ^ ∑ i ∈ s, f i) * multinomial s f
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ (∑ i ∈ s, 2 * f i)! / ∏ i ∈ s, (2 * f i)! ≤ ((∑ i ∈ s, f i) ^ ∑ i ∈ s, f i) * multinomial s f

Tactic:
multinomial,

Goal state after:
ι : Type u_1
s : Finset ι
f : ι → ℕ
⊢ (∑ i ∈ s, 2 * f i)! / ∏ i ∈ s, (2 * f i)! ≤ ((∑ i ∈ s, f i) ^ ∑ i ∈ s, f i) * ((∑ i ∈ s, f i)! / ∏ i ∈ s, (f i)!)
Module: Mathlib.Order.GameAdd

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
x y : α × β
⊢ GameAdd rα rβ x y → rα x.1 y.1 ∧ x.2 = y.2 ∨ rβ x.2 y.2 ∧ x.1 = y.1

pp: case mpr
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
x y : α × β
⊢ rα x.1 y.1 ∧ x.2 = y.2 ∨ rβ x.2 y.2 ∧ x.1 = y.1 → GameAdd rα rβ x y

Tactic:
· rintro (@⟨a₁, a₂, b, h⟩ | @⟨a, b₁, b₂, h⟩)
    exacts [Or.inl ⟨h, rfl⟩, Or.inr ⟨h, rfl⟩]

Goal state after:
case mpr
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
x y : α × β
⊢ rα x.1 y.1 ∧ x.2 = y.2 ∨ rβ x.2 y.2 ∧ x.1 = y.1 → GameAdd rα rβ x y
Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex

Goal state before:
pp: case pos
α : Type u_1
inst✝ : LinearOrder α
x y : DegLex (α →₀ ℕ)
h : ¬x = y
k : degree (ofDegLex x) < degree (ofDegLex y)
⊢ x = y ∨
      degree (ofDegLex x) < degree (ofDegLex y) ∨
        degree (ofDegLex x) = degree (ofDegLex y) ∧ toLex (ofDegLex x) < toLex (ofDegLex y) ↔
    degree (ofDegLex x) < degree (ofDegLex y) ∨
      degree (ofDegLex x) = degree (ofDegLex y) ∧ (x = y ∨ toLex (ofDegLex x) < toLex (ofDegLex y))

Tactic:
simp [k]

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
n : σ →₀ ℕ
a : R
ha : a ≠ 0
⊢ ∀ (a_1 : σ →₀ ℕ), (∃ r, a_1 ≤ n ∧ r ∣ C a ∧ p = (monomial a_1) 1 * r) ↔ ∃ b, a_1 ≤ n ∧ b ∣ a ∧ p = (monomial a_1) b

Tactic:
intro m

Goal state after:
R : Type u_1
σ : Type u_2
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
p : MvPolynomial σ R
n : σ →₀ ℕ
a : R
ha : a ≠ 0
m : σ →₀ ℕ
⊢ (∃ r, m ≤ n ∧ r ∣ C a ∧ p = (monomial m) 1 * r) ↔ ∃ b, m ≤ n ∧ b ∣ a ∧ p = (monomial m) b
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
⊢ ∀ (a : σ →₀ ℕ), (∃ b, a ≤ n ∧ b ∣ 1 ∧ p = (monomial a) b) ↔ ∃ u, a ≤ n ∧ IsUnit u ∧ p = (monomial a) u

Tactic:
intro m

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) ↔ ∃ u, m ≤ n ∧ IsUnit u ∧ p = (monomial m) u
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case cons
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
α : Type u_3
f : α → MvPolynomial σ R
a : α
s : Finset α
haA : a ∉ s
h : m.toSyn (m.degree (∑ x ∈ s, f x)) ≤ s.sup fun x ↦ m.toSyn (m.degree (f x))
⊢ m.toSyn (m.degree (∑ x ∈ Finset.cons a s haA, f x)) ≤ (Finset.cons a s haA).sup fun x ↦ m.toSyn (m.degree (f x))

Tactic:
rw [Finset.sum_cons, Finset.sup_cons]
    exact le_trans m.degree_add_le (max_le_max le_rfl h)

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

Goal state before:
pp: case cons
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
α : Type u_3
f : α → MvPolynomial σ R
a : α
s : Finset α
haA : a ∉ s
h : m.toSyn (m.degree (∑ x ∈ s, f x)) ≤ s.sup fun x ↦ m.toSyn (m.degree (f x))
⊢ m.toSyn (m.degree (∑ x ∈ Finset.cons a s haA, f x)) ≤ (Finset.cons a s haA).sup fun x ↦ m.toSyn (m.degree (f x))

Tactic:
| cons a s haA h =>

Goal state after: