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

Goal state before:
pp: case e'_2
E : Type u_1
ι : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : MeasurableSpace E
μ : Measure E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
b₀ : Basis ι ℝ E
this : FiniteDimensional ℝ E
⊢ fundamentalDomain b = ⇑(b.equiv b₀ (Equiv.refl ι)) ⁻¹' fundamentalDomain b₀

Tactic:
Set.eq_preimage_iff_image_eq (LinearEquiv.bijective _),

Goal state after:
case e'_2
E : Type u_1
ι : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : MeasurableSpace E
μ : Measure E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
b₀ : Basis ι ℝ E
this : FiniteDimensional ℝ E
⊢ ⇑(b.equiv b₀ (Equiv.refl ι)) '' fundamentalDomain b = fundamentalDomain b₀
Module: Mathlib.Analysis.BoxIntegral.Partition.Basic

Goal state before:
pp: ι : Type u_1
I : Box ι
M : Type u_2
inst✝ : AddCommMonoid M
π : Prepartition I
πi : (J : Box ι) → Prepartition J
f : Box ι → M
⊢ ∑ J ∈ π.boxes.biUnion fun J ↦ (πi J).boxes, f J = ∑ J ∈ π.boxes, ∑ J' ∈ (πi J).boxes, f J'

Tactic:
refine Finset.sum_biUnion fun J₁ h₁ J₂ h₂ hne => Finset.disjoint_left.2 fun J' h₁' h₂' => ?_
  exact hne (π.eq_of_le_of_le h₁ h₂ ((πi J₁).le_of_mem h₁') ((πi J₂).le_of_mem h₂'))

Goal state after:
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
F : Type u_5
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type u_6
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : IsInternal V
hV' : OrthogonalFamily 𝕜 (fun i ↦ ↥(V i)) fun i ↦ (V i).subtypeₗᵢ
e₁ : (⨁ (i : ι), ↥(V i)) ≃ₗ[𝕜] (i : ι) → ↥(V i) := linearEquivFunOnFintype 𝕜 ι fun i ↦ ↥(V i)
e₂ : (⨁ (i : ι), ↥(V i)) ≃ₗ[𝕜] E := LinearEquiv.ofBijective (coeLinearMap V) hV
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
v₀ : E
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
w₀

Goal state after:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst✝⁸ : RCLike 𝕜
E : Type u_4
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace 𝕜 E
F : Type u_5
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : InnerProductSpace ℝ F
F' : Type u_6
inst✝³ : NormedAddCommGroup F'
inst✝² : InnerProductSpace ℝ F'
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : IsInternal V
hV' : OrthogonalFamily 𝕜 (fun i ↦ ↥(V i)) fun i ↦ (V i).subtypeₗᵢ
e₁ : (⨁ (i : ι), ↥(V i)) ≃ₗ[𝕜] (i : ι) → ↥(V i) := linearEquivFunOnFintype 𝕜 ι fun i ↦ ↥(V i)
e₂ : (⨁ (i : ι), ↥(V i)) ≃ₗ[𝕜] E := LinearEquiv.ofBijective (coeLinearMap V) hV
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
v₀ w₀ : E
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
I✝ J I : Box ι
⊢ (↑(Finset.map I.splitCenterBoxEmb Finset.univ)).Pairwise (Function.onFun Disjoint Box.toSet)

Tactic:
rw [Finset.coe_map, Finset.coe_univ, image_univ]

Goal state after:
ι : Type u_1
inst✝ : Fintype ι
I✝ J I : Box ι
⊢ (range ⇑I.splitCenterBoxEmb).Pairwise (Function.onFun Disjoint Box.toSet)
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 ι
inst✝ : Fintype ι'
b : OrthonormalBasis ι 𝕜 E
e : ι ≃ ι'
i' : ι'
⊢ (b.reindex e) i' = b (e.symm i')

Tactic:
by
  classical
    dsimp [reindex]
    rw [coe_ofRepr]
    dsimp
    rw [← b.repr_symm_single, LinearIsometryEquiv.piLpCongrLeft_symm,
      EuclideanSpace.piLpCongrLeft_single]

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

Goal state before:
pp: case refine_2
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
π : TaggedPrepartition I
r : (ι → ℝ) → ↑(Set.Ioi 0)
hπ : l.MemBaseSet I c r π
p : Box ι → Prop
hD : l.bDistortion = true
π₁ : Prepartition I
hπ₁U : π₁.iUnion = ↑I \ π.iUnion
hc : π₁.distortion ≤ c
π₂ : TaggedPrepartition I := π.filter fun J ↦ ¬p J
this✝ : Disjoint π₁.iUnion π₂.iUnion
this : (π.filter fun J ↦ ¬p J).distortion ≤ c
⊢ (π₁.disjUnion π₂.toPrepartition this✝).distortion ≤ c

Tactic:
simpa [hc]

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

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
I : Box ι
c : ℝ≥0
l : IntegrationParams
π : TaggedPrepartition I
r : (ι → ℝ) → ↑(Set.Ioi 0)
hπ : l.MemBaseSet I c r π
p : Box ι → Prop
⊢ l.MemBaseSet I c r (π.filter p)

Tactic:
refine ⟨fun J hJ => hπ.1 J (π.mem_filter.1 hJ).1, fun hH J hJ => hπ.2 hH J (π.mem_filter.1 hJ).1,
    fun hD => (distortion_filter_le _ _).trans (hπ.3 hD), fun hD => ?_⟩
  rcases hπ.4 hD with ⟨π₁, hπ₁U, hc⟩
  set π₂ := π.filter fun J => ¬p J
  have : Disjoint π₁.iUnion π₂.iUnion := by
    simpa [π₂, hπ₁U] using disjoint_sdiff_self_left.mono_right sdiff_le
  refine ⟨π₁.disjUnion π₂.toPrepartition this, ?_, ?_⟩
  · suffices ↑I \ π.iUnion ∪ π.iUnion \ (π.filter p).iUnion = ↑I \ (π.filter p).iUnion by
      simp [π₂, *]
    have h : (π.filter p).iUnion ⊆ π.iUnion :=
      biUnion_subset_biUnion_left (Finset.filter_subset _ _)
    ext x
    fconstructor
    · rintro (⟨hxI, hxπ⟩ | ⟨hxπ, hxp⟩)
      exacts [⟨hxI, mt (@h x) hxπ⟩, ⟨π.iUnion_subset hxπ, hxp⟩]
    · rintro ⟨hxI, hxp⟩
      by_cases hxπ : x ∈ π.iUnion
      exacts [Or.inr ⟨hxπ, hxp⟩, Or.inl ⟨hxI, hxπ⟩]
  · have : (π.filter fun J => ¬p J).distortion ≤ c := (distortion_filter_le _ _).trans (hπ.3 hD)
    simpa [hc]

Goal state after:
Module: Mathlib.Analysis.Oscillation

Goal state before:
pp: case right
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₁
T : Set ℝ
Tb : T ⊆ Real.lt✝ 0
Tfin : T.Finite
hT : K ⊆ ⋃ i ∈ T, S i
T_nonempty : T.Nonempty
x : E
hx : x ∈ K
⊢ x ∈ S (⋯.min T_nonempty)

Tactic:
obtain ⟨r, hr⟩ := mem_iUnion.1 (hT hx)

Goal state after:
case right
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₁
T : Set ℝ
Tb : T ⊆ Real.lt✝ 0
Tfin : T.Finite
hT : K ⊆ ⋃ i ∈ T, S i
T_nonempty : T.Nonempty
x : E
hx : x ∈ K
r : ℝ
hr : x ∈ ⋃ (_ : r ∈ T), S r
⊢ x ∈ S (⋯.min T_nonempty)
Module: Mathlib.Analysis.BoxIntegral.UnitPartition

Goal state before:
pp: ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
ν : ι → ℤ
i : ι
⊢ ENNReal.ofReal (1 / ↑n) ≤ ENNReal.ofReal (1 / ↑n)

Tactic:
le_rfl

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

Goal state before:
pp: ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
n : ι
i : ↥(Iio n)
⊢ ↑i < n

Tactic:
exact mem_Iio.1 i.2

Goal state after:
Module: Mathlib.LinearAlgebra.Orientation

Goal state before:
pp: case h
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : IsEmpty ι
x : M [⋀^ι]→ₗ[R] R
hx : x ≠ 0
⊢ ¬LinearIndependent R ![x, AlternatingMap.constLinearEquivOfIsEmpty 1]

Tactic:
intro h

Goal state after:
case h
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : LinearOrder R
inst✝³ : IsStrictOrderedRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : IsEmpty ι
x : M [⋀^ι]→ₗ[R] R
hx : x ≠ 0
h : LinearIndependent R ![x, AlternatingMap.constLinearEquivOfIsEmpty 1]
⊢ False
Module: Mathlib.Analysis.InnerProductSpace.Orientation

Goal state before:
pp: case mp
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e f : OrthonormalBasis ι ℝ E
⊢ e.toBasis.det = f.toBasis.det → e.toBasis.orientation = f.toBasis.orientation

Tactic:
intro h

Goal state after:
case mp
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e f : OrthonormalBasis ι ℝ E
h : e.toBasis.det = f.toBasis.det
⊢ e.toBasis.orientation = f.toBasis.orientation
Module: Mathlib.Analysis.InnerProductSpace.Orientation

Goal state before:
pp: case mpr
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e f : OrthonormalBasis ι ℝ E
⊢ e.toBasis.orientation = f.toBasis.orientation → e.toBasis.det = f.toBasis.det

Tactic:
intro h

Goal state after:
case mpr
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e f : OrthonormalBasis ι ℝ E
h : e.toBasis.orientation = f.toBasis.orientation
⊢ e.toBasis.det = f.toBasis.det
Module: Mathlib.Analysis.InnerProductSpace.Orientation

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
⊢ ¬SameRay ℝ (AlternatingMap.constLinearEquivOfIsEmpty 1) (-AlternatingMap.constLinearEquivOfIsEmpty 1)

Tactic:
intro h

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
h : SameRay ℝ (AlternatingMap.constLinearEquivOfIsEmpty 1) (-AlternatingMap.constLinearEquivOfIsEmpty 1)
⊢ False
Module: Mathlib.Analysis.InnerProductSpace.Orientation

Goal state before:
pp: case zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
b : OrthonormalBasis (Fin 0) ℝ E
v : Fin 0 → E
⊢ |o.volumeForm v| = |b.toBasis.det v|

Tactic:
refine o.eq_or_eq_neg_of_isEmpty.elim ?_ ?_ <;> rintro rfl <;> simp

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

Goal state before:
pp: case zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
v : Fin 0 → E
⊢ |o.volumeForm v| ≤ ∏ i, ‖v i‖

Tactic:
refine o.eq_or_eq_neg_of_isEmpty.elim ?_ ?_ <;> rintro rfl <;> simp

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

Goal state before:
pp: case zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
v : Fin 0 → E
hv : Pairwise fun i j ↦ ⟪v i, v j⟫ = 0
⊢ |o.volumeForm v| = ∏ i, ‖v i‖

Tactic:
refine o.eq_or_eq_neg_of_isEmpty.elim ?_ ?_ <;> rintro rfl <;> simp

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

Goal state before:
pp: case zero
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
φ : E ≃ₗᵢ[ℝ] F
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
inst✝ : Fact (finrank ℝ F = 0)
x : Fin 0 → F
⊢ ((map (Fin 0) φ.toLinearEquiv) o).volumeForm x = o.volumeForm (⇑φ.symm ∘ x)

Tactic:
refine o.eq_or_eq_neg_of_isEmpty.elim ?_ ?_ <;> rintro rfl <;> simp

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

Goal state before:
pp: case zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
φ : E ≃ₗᵢ[ℝ] E
hφ : 0 < LinearMap.det ↑φ.toLinearEquiv
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
x : Fin 0 → E
⊢ o.volumeForm (⇑φ ∘ x) = o.volumeForm x

Tactic:
refine o.eq_or_eq_neg_of_isEmpty.elim ?_ ?_ <;> rintro rfl <;> simp

Goal state after:
Module: Mathlib.Analysis.SumOverResidueClass

Goal state before:
pp: f : ℕ → ℝ
hf : Antitone f
n : ℕ
hn : f n < 0
hs : Summable f
this : ∀ ε > 0, ∃ N, ∀ n ≥ N, |f n| < ε
N : ℕ
H : f (max n N) ≤ f n
⊢ -f n ≤ -f (max n N)

Tactic:
neg_le_neg_iff

Goal state after:
f : ℕ → ℝ
hf : Antitone f
n : ℕ
hn : f n < 0
hs : Summable f
this : ∀ ε > 0, ∃ N, ∀ n ≥ N, |f n| < ε
N : ℕ
H : f (max n N) ≤ f n
⊢ f (max n N) ≤ f n
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: case succ
M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedAddMonoid M
f : ℕ → M
u : ℕ → ℕ
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : Monotone u
n : ℕ
ihn : ∑ k ∈ Ico (u 0) (u n), f k ≤ ∑ k ∈ range n, (u (k + 1) - u k) • f (u k)
this : ∀ k ∈ Ico (u n) (u (n + 1)), f k ≤ f (u n)
⊢ ∑ k ∈ Ico (u n) (u (n + 1)), f k ≤ (u (n + 1) - u n) • f (u n)

Tactic:
convert! sum_le_sum this

Goal state after:
M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedAddMonoid M
f : ℕ → M
u : ℕ → ℕ
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : Monotone u
n : ℕ
ihn : ∑ k ∈ Ico (u 0) (u n), f k ≤ ∑ k ∈ range n, (u (k + 1) - u k) • f (u k)
this : ∀ k ∈ Ico (u n) (u (n + 1)), f k ≤ f (u n)
⊢ (u (n + 1) - u n) • f (u n) = ∑ i ∈ Ico (u n) (u (n + 1)), f (u n)
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: case succ
M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedAddMonoid M
f : ℕ → M
u : ℕ → ℕ
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : Monotone u
n : ℕ
ihn : ∑ k ∈ range n, (u (k + 1) - u k) • f (u (k + 1)) ≤ ∑ k ∈ Ico (u 0 + 1) (u n + 1), f k
this : ∀ k ∈ Ico (u n + 1) (u (n + 1) + 1), f (u (n + 1)) ≤ f k
⊢ (u (n + 1) - u n) • f (u (n + 1)) ≤ ∑ k ∈ Ico (u n + 1) (u (n + 1) + 1), f k

Tactic:
convert! sum_le_sum this

Goal state after:
M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedAddMonoid M
f : ℕ → M
u : ℕ → ℕ
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : Monotone u
n : ℕ
ihn : ∑ k ∈ range n, (u (k + 1) - u k) • f (u (k + 1)) ≤ ∑ k ∈ Ico (u 0 + 1) (u n + 1), f k
this : ∀ k ∈ Ico (u n + 1) (u (n + 1) + 1), f (u (n + 1)) ≤ f k
⊢ (u (n + 1) - u n) • f (u (n + 1)) = ∑ i ∈ Ico (u n + 1) (u (n + 1) + 1), f (u (n + 1))
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: case h₂
M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedAddMonoid M
f : ℕ → M
u : ℕ → ℕ
C : ℕ
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
h_nonneg : ∀ (n : ℕ), 0 ≤ f n
hu : Monotone u
h_succ_diff : SuccDiffBounded C u
n : ℕ
this : ∀ k ∈ range n, (u (k + 2) - u (k + 1)) • f (u (k + 1)) ≤ C • (u (k + 1) - u k) • f (u (k + 1))
⊢ ∑ k ∈ range n, (u (k + 2) - u (k + 1)) • f (u (k + 1)) ≤ C • ∑ k ∈ range n, (u (k + 1) - u k) • f (u (k + 1))

Tactic:
convert! sum_le_sum this

Goal state after:
M : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : PartialOrder M
inst✝ : IsOrderedAddMonoid M
f : ℕ → M
u : ℕ → ℕ
C : ℕ
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
h_nonneg : ∀ (n : ℕ), 0 ≤ f n
hu : Monotone u
h_succ_diff : SuccDiffBounded C u
n : ℕ
this : ∀ k ∈ range n, (u (k + 2) - u (k + 1)) • f (u (k + 1)) ≤ C • (u (k + 1) - u k) • f (u (k + 1))
⊢ C • ∑ k ∈ range n, (u (k + 1) - u k) • f (u (k + 1)) = ∑ i ∈ range n, C • (u (i + 1) - u i) • f (u (i + 1))
Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics

Goal state before:
pp: case mp
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
D : Type u_2
inst✝ : TopologicalSpace D
f : D → E
hf : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
⊢ Bornology.IsBounded (range f) → f =O[cocompact D] 1

Tactic:
intro h

Goal state after:
case mp
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
D : Type u_2
inst✝ : TopologicalSpace D
f : D → E
hf : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h : Bornology.IsBounded (range f)
⊢ f =O[cocompact D] 1
Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics

Goal state before:
pp: case mpr
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
D : Type u_2
inst✝ : TopologicalSpace D
f : D → E
hf : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
⊢ f =O[cocompact D] 1 → Bornology.IsBounded (range f)

Tactic:
intro h

Goal state after:
case mpr
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
D : Type u_2
inst✝ : TopologicalSpace D
f : D → E
hf : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h : f =O[cocompact D] 1
⊢ Bornology.IsBounded (range f)
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: case mp
C : ℕ
u : ℕ → ℕ
f : ℕ → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu_strict : StrictMono u
hC_nonzero : C ≠ 0
h_succ_diff : SuccDiffBounded C u
⊢ ∑' (b : ℕ), ↑(↑(u (b + 1)) - ↑(u b)) * ↑(f (u b)) = ∞ → ∑' (b : ℕ), ↑(f b) = ∞

Tactic:
intro h

Goal state after:
case mp
C : ℕ
u : ℕ → ℕ
f : ℕ → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu_strict : StrictMono u
hC_nonzero : C ≠ 0
h_succ_diff : SuccDiffBounded C u
h : ∑' (b : ℕ), ↑(↑(u (b + 1)) - ↑(u b)) * ↑(f (u b)) = ∞
⊢ ∑' (b : ℕ), ↑(f b) = ∞
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: case mpr
C : ℕ
u : ℕ → ℕ
f : ℕ → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu_strict : StrictMono u
hC_nonzero : C ≠ 0
h_succ_diff : SuccDiffBounded C u
⊢ ∑' (b : ℕ), ↑(f b) = ∞ → ∑' (b : ℕ), ↑(↑(u (b + 1)) - ↑(u b)) * ↑(f (u b)) = ∞

Tactic:
intro h

Goal state after:
case mpr
C : ℕ
u : ℕ → ℕ
f : ℕ → ℝ≥0
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu_strict : StrictMono u
hC_nonzero : C ≠ 0
h_succ_diff : SuccDiffBounded C u
h : ∑' (b : ℕ), ↑(f b) = ∞
⊢ ∑' (b : ℕ), ↑(↑(u (b + 1)) - ↑(u b)) * ↑(f (u b)) = ∞
Module: Mathlib.Analysis.Asymptotics.SpecificAsymptotics

Goal state before:
pp: case mpr.hs
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}
⊢ Bornology.IsBounded (f '' t)

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}
⊢ Bornology.IsBounded (f '' tᶜ)

Tactic:
· apply (IsCompact.image hcompact hf).isBounded

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}
⊢ Bornology.IsBounded (f '' tᶜ)
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: case inr
p : ℝ
hp : p < 0
⊢ ¬Summable fun n ↦ (↑n ^ p)⁻¹

Tactic:
intro h

Goal state after:
case inr
p : ℝ
hp : p < 0
h : Summable fun n ↦ (↑n ^ p)⁻¹
⊢ False
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: p : ℕ
⊢ (Summable fun n ↦ 1 / ↑n ^ p) ↔ 1 < p

Tactic:
by
  simp only [one_div, Real.summable_nat_pow_inv]

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: case refine_2
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
k n : ℕ
hk : k ≠ 0
h : k ≤ n
⊢ ∀ (n : ℕ),
    k ≤ n → ∑ i ∈ Ioc k n, (↑i ^ 2)⁻¹ ≤ (↑k)⁻¹ - (↑n)⁻¹ → ∑ i ∈ Ioc k (n + 1), (↑i ^ 2)⁻¹ ≤ (↑k)⁻¹ - (↑(n + 1))⁻¹

Tactic:
intro n hn IH

Goal state after:
case refine_2
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
k n✝ : ℕ
hk : k ≠ 0
h : k ≤ n✝
n : ℕ
hn : k ≤ n
IH : ∑ i ∈ Ioc k n, (↑i ^ 2)⁻¹ ≤ (↑k)⁻¹ - (↑n)⁻¹
⊢ ∑ i ∈ Ioc k (n + 1), (↑i ^ 2)⁻¹ ≤ (↑k)⁻¹ - (↑(n + 1))⁻¹
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
k n : ℕ
⊢ (↑(k + 1) ^ 2)⁻¹ + ∑ k ∈ Ico (k + 1 + 1) (max (k + 1) n + 1), (↑k ^ 2)⁻¹ ≤
    ((↑k + 1) ^ 2)⁻¹ + ∑ i ∈ Ioc k.succ (max (k + 1) n), (↑i ^ 2)⁻¹

Tactic:
Ico_add_one_right_eq_Icc,

Goal state after:
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
k n : ℕ
⊢ (↑(k + 1) ^ 2)⁻¹ + ∑ k ∈ Icc (k + 1 + 1) (max (k + 1) n), (↑k ^ 2)⁻¹ ≤
    ((↑k + 1) ^ 2)⁻¹ + ∑ i ∈ Ioc k.succ (max (k + 1) n), (↑i ^ 2)⁻¹
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: a s : ℝ
hnorm : Tendsto (fun n ↦ ‖↑n‖) atTop atTop
h_abs : (fun n ↦ |↑n + a|) ~[atTop] fun x ↦ ↑x
⊢ (Summable fun n ↦ 1 / |↑n + a| ^ s) ↔ Summable fun n ↦ 1 / ↑n ^ s

Tactic:
Asymptotics.IsEquivalent.summable_iff_nat

Goal state after:
a s : ℝ
hnorm : Tendsto (fun n ↦ ‖↑n‖) atTop atTop
h_abs : (fun n ↦ |↑n + a|) ~[atTop] fun x ↦ ↑x
⊢ Summable ?m.154 ↔ Summable fun n ↦ 1 / ↑n ^ s

a s : ℝ
hnorm : Tendsto (fun n ↦ ‖↑n‖) atTop atTop
h_abs : (fun n ↦ |↑n + a|) ~[atTop] fun x ↦ ↑x
⊢ (fun n ↦ 1 / |↑n + a| ^ s) ~[atTop] ?m.154

a s : ℝ
hnorm : Tendsto (fun n ↦ ‖↑n‖) atTop atTop
h_abs : (fun n ↦ |↑n + a|) ~[atTop] fun x ↦ ↑x
⊢ ℕ → ℝ
Module: Mathlib.Algebra.MonoidAlgebra.Ideal

Goal state before:
pp: case mp
k : Type u_1
A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : Semiring k
s : Set A
x : k[A]
RHS : Ideal k[A] :=
  { carrier := {p | ∀ m ∈ p.coeff.support, ∃ m' ∈ s, ∃ d, m = d + m'}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
i : A
hi : i ∈ s
m : A
hm : m ∈ (of' k A i).coeff.support
⊢ ∃ m' ∈ s, ∃ d, m = d + m'

Tactic:
refine ⟨_, hi, 0, ?_⟩

Goal state after:
case mp
k : Type u_1
A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : Semiring k
s : Set A
x : k[A]
RHS : Ideal k[A] :=
  { carrier := {p | ∀ m ∈ p.coeff.support, ∃ m' ∈ s, ∃ d, m = d + m'}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
i : A
hi : i ∈ s
m : A
hm : m ∈ (of' k A i).coeff.support
⊢ m = 0 + i
Module: Mathlib.Data.Set.SMulAntidiagonal

Goal state before:
pp: G : Type u_1
P : Type u_2
s : Set G
t : Set P
a : P
inst✝¹ : SMul G P
x y : ↑(s.smulAntidiagonal t a)
inst✝ : IsLeftCancelSMul G P
h : (↑x).1 = (↑y).1
⊢ a = (↑y).1 • (↑x).2

Tactic:
by rw [← h]; exact x.2.2.2.symm

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.PointwiseSMul

Goal state before:
pp: G : Type u_1
P : Type u_2
R : Type u_3
V : Type u_4
inst✝⁴ : Group G
inst✝³ : MulAction G P
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : SMulWithZero R V
f : R[G]
x : P → V
p : P
hp : ((↑f.coeff.support).smulAntidiagonal (Function.support x) p).Finite
s : Set (G × P) := ↑(Finset.SMulAntidiagonal p hp)
x✝¹ : G × P
h₁ : x✝¹ ∈ Finset.SMulAntidiagonal p hp
x✝ : G × P
h₂ : x✝ ∈ Finset.SMulAntidiagonal p hp
h : x✝¹.1 = x✝.1
⊢ x✝¹ = x✝

Tactic:
mem_smulAntidiagonal_of_group

Goal state after:
G : Type u_1
P : Type u_2
R : Type u_3
V : Type u_4
inst✝⁴ : Group G
inst✝³ : MulAction G P
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : SMulWithZero R V
f : R[G]
x : P → V
p : P
hp : ((↑f.coeff.support).smulAntidiagonal (Function.support x) p).Finite
s : Set (G × P) := ↑(Finset.SMulAntidiagonal p hp)
x✝¹ : G × P
h₁ : f.coeff x✝¹.1 ≠ 0 ∧ x x✝¹.2 ≠ 0 ∧ x✝¹.2 = x✝¹.1⁻¹ • p
x✝ : G × P
h₂ : f.coeff x✝.1 ≠ 0 ∧ x x✝.2 ≠ 0 ∧ x✝.2 = x✝.1⁻¹ • p
h : x✝¹.1 = x✝.1
⊢ x✝¹ = x✝