mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral

Goal state before:
pp: case h
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
g : E →ᵇ ℝ
hε : 0 < ε
N : ℕ
hgN : ε * (‖g‖ * ‖g‖) < ↑N
n : ℕ
hn : N ≤ n
⊢ ∀ᵐ (ω : E) ∂P, ‖(g * (1 + (↑n)⁻¹ • -(ε • g * g)) ^ n) ω‖ ≤ ‖g‖

Tactic:
have hnpos : 0 < (n : ℝ) := by
      apply lt_of_lt_of_le (lt_of_le_of_lt _ hgN) (Nat.cast_le.mpr hn)
      exact (mul_nonneg (le_of_lt hε) (mul_self_nonneg (norm g)))

Goal state after:
case h
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
P : Measure E
inst✝ : IsFiniteMeasure P
ε : ℝ
g : E →ᵇ ℝ
hε : 0 < ε
N : ℕ
hgN : ε * (‖g‖ * ‖g‖) < ↑N
n : ℕ
hn : N ≤ n
hnpos : 0 < ↑n
⊢ ∀ᵐ (ω : E) ∂P, ‖(g * (1 + (↑n)⁻¹ • -(ε • g * g)) ^ n) ω‖ ≤ ‖g‖
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
L : PeriodPair
⊢ Submodule.span ℤ (Set.range ![L.ω₁, L.ω₂]) = L.lattice

Tactic:
simp [lattice, Set.pair_comm L.ω₂ L.ω₁]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Pow.Integral

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : FiniteDimensional ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedAddCommGroup F
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hd : 1 ≤ Module.finrank ℝ E
f : E → F
C α r : ℝ
hα : α < ↑(Module.finrank ℝ E)
h_decay : ∀ᵐ (x : E) ∂μ.restrict (ball 0 r), ‖f x‖ ≤ C * ‖x‖ ^ (-α)
h_meas : AEStronglyMeasurable f μ
this : Nontrivial E
hint : IntegrableOn (fun x ↦ C * ‖x‖ ^ (-α)) (ball 0 r) μ
⊢ IntegrableOn f (ball 0 r) μ

Tactic:
exact Integrable.mono' hint h_meas.restrict h_decay

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
F : Type u_2
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : Nontrivial E
μ : Measure E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : μ.IsAddHaarMeasure
f : ℝ → F
⊢ Integrable (fun x ↦ f ‖x‖) μ ↔ IntegrableOn (fun y ↦ y ^ (dim E - 1) • f y) (Ioi 0) volume

Tactic:
have := μ.measurePreserving_homeomorphUnitSphereProd.integrable_comp_emb (g := f ∘ (↑) ∘ Prod.snd)
    (Homeomorph.measurableEmbedding _)
  simp only [comp_def, homeomorphUnitSphereProd_apply_snd_coe] at this
  rw [← restrict_compl_singleton (μ := μ) 0, ← IntegrableOn,
    integrableOn_iff_comap_subtypeVal (by measurability), comp_def, this,
    Integrable.comp_snd_iff (β := Ioi 0) (f := (f <| Subtype.val ·)),
    integrableOn_iff_comap_subtypeVal, comp_def, Measure.volumeIoiPow,
    integrable_withDensity_iff_integrable_smul', integrable_congr]
  · refine .of_forall ?_
    rintro ⟨x, hx : 0 < x⟩
    simp (disch := positivity) [ENNReal.toReal_ofReal]
  · fun_prop
  · simp
  · measurability
  · simp

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
z : ℂ
l : ↥L.lattice
⊢ -∑' (c : ↥L.lattice), 2 / (z + ↑l - ↑((Equiv.addRight l) c)) ^ 3 = -∑' (l : ↥L.lattice), 2 / (z - ↑l) ^ 3

Tactic:
simp only [← tsum_neg, ← div_neg, Equiv.coe_addRight, Submodule.coe_add, add_sub_add_right_eq_sub]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: case succ
n : ℕ
r : ℝ := (1 / (2 * (↑n + 1) + 1)) ^ 2
hr : r = (1 / (2 * (↑n + 1) + 1)) ^ 2
hr1 : r < 1
⊢ HasSum (fun j ↦ r ^ (j + 1) / 3) (1 / (12 * ↑(n + 1) * (↑(n + 1) + 1)))

Tactic:
grind [((hasSum_geometric_of_lt_one (by positivity) hr1).mul_right r).div_const 3]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: α : ℝ
i : ℕ
hα : |α| ≤ 1
⊢ (-1) ^ i * α ≤ 1

Tactic:
by
  apply le_of_abs_le
  rwa [abs_mul, abs_neg_one_pow, one_mul]

Goal state after:
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: r q : ℚ
hq : cos (↑r * π) = ↑q
⊢ ∃ q, cos (↑(Int.fract r) * π) = ↑q

Tactic:
exact ⟨(-1) ^ ⌊r⌋ * q, by rw [Int.fract]; push_cast; rw [sub_mul, cos_sub_int_mul_pi, hq]⟩

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: m n : ℤ
⊢ ↑|n| ≤ ‖![n, m]‖

Tactic:
by
  simp only [EisensteinSeries.norm_eq_max_natAbs, Fin.isValue, Matrix.cons_val_zero,
    Matrix.cons_val_one, Matrix.cons_val_fin_one, Nat.cast_max, le_sup_iff]
  left
  rw [Int.abs_eq_natAbs]
  exact le_refl _

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: case refine_1
x : Fin 2 → ℤ
hx : x ≠ 0
H0 : max (x 0).natAbs (x 1).natAbs = (x 0).natAbs
this : x 0 ≠ 0
⊢ 1 ≤ (↑(x 0) / ‖x‖) ^ 2

Tactic:
simp only [norm_eq_max_natAbs, H0, Nat.cast_natAbs, Int.cast_abs, div_pow, sq_abs, ne_eq,
      OfNat.ofNat_ne_zero, not_false_eq_true, pow_eq_zero_iff, Int.cast_eq_zero, this, div_self,
      le_refl]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: n : ℤ
hn : n ≠ 0
x : ℝ
hx : 1 < x
this : arcosh x ≠ 0
⊢ ↑n * arcosh x ≠ 0

Tactic:
mul_ne_zero_iff

Goal state after:
n : ℤ
hn : n ≠ 0
x : ℝ
hx : 1 < x
this : arcosh x ≠ 0
⊢ ↑n ≠ 0 ∧ arcosh x ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: n k i : ℕ
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
⊢ 0 ≤ (-1) ^ i * iterateDerivativeC n k x i

Tactic:
rw [iterateDerivativeC, ← mul_assoc]

Goal state after:
n k i : ℕ
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
⊢ 0 ≤
    (-1) ^ i * (↑k.factorial * (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹) *
      ∑ t ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase i), ∏ a ∈ t, (x - node n a)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
⊢ 0 < (-1) ^ i * iterateDerivativeC n k x i

Tactic:
rw [iterateDerivativeC, ← mul_assoc]

Goal state after:
n k i : ℕ
hk₁ : 0 < k
hk₂ : k ≤ n
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
⊢ 0 <
    (-1) ^ i * (↑k.factorial * (∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j))⁻¹) *
      ∑ t ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase i), ∏ a ∈ t, (x - node n a)
Module: Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn

Goal state before:
pp: α : Type u_1
β : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : CompleteSpace F
inst✝¹ : TopologicalSpace β
inst✝ : LocallyCompactSpace β
f : α → β → F
s : Set β
hs : IsOpen[inst✝¹] s
hu : ∀ K ⊆ s, IsCompact K → ∃ u, Summable u ∧ ∀ᶠ (n : α) in cofinite, ∀ k ∈ K, ‖f n k‖ ≤ u n
⊢ ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn (fun x1 x2 ↦ ∑ i ∈ x1, f i x2) (fun x ↦ ∑' (n : α), f n x) atTop K

Tactic:
intro K hK hKc

Goal state after:
α : Type u_1
β : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : CompleteSpace F
inst✝¹ : TopologicalSpace β
inst✝ : LocallyCompactSpace β
f : α → β → F
s : Set β
hs : IsOpen[inst✝¹] s
hu : ∀ K ⊆ s, IsCompact K → ∃ u, Summable u ∧ ∀ᶠ (n : α) in cofinite, ∀ k ∈ K, ‖f n k‖ ≤ u n
K : Set β
hK : K ⊆ s
hKc : IsCompact K
⊢ TendstoUniformlyOn (fun x1 x2 ↦ ∑ i ∈ x1, f i x2) (fun x ↦ ∑' (n : α), f n x) atTop K
Module: Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn

Goal state before:
pp: α : Type u_1
β : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : CompleteSpace F
inst✝¹ : TopologicalSpace β
inst✝ : LocallyCompactSpace β
f : α → β → F
s : Set β
hs : IsOpen[inst✝¹] s
hu : ∀ K ⊆ s, IsCompact K → ∃ u, Summable u ∧ ∀ (n : α), ∀ k ∈ K, ‖f n k‖ ≤ u n
⊢ ∀ K ⊆ s, IsCompact K → ∃ u, Summable u ∧ ∀ᶠ (n : α) in cofinite, ∀ k ∈ K, ‖f n k‖ ≤ u n

Tactic:
intro K hK hKc

Goal state after:
α : Type u_1
β : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : CompleteSpace F
inst✝¹ : TopologicalSpace β
inst✝ : LocallyCompactSpace β
f : α → β → F
s : Set β
hs : IsOpen[inst✝¹] s
hu : ∀ K ⊆ s, IsCompact K → ∃ u, Summable u ∧ ∀ (n : α), ∀ k ∈ K, ‖f n k‖ ≤ u n
K : Set β
hK : K ⊆ s
hKc : IsCompact K
⊢ ∃ u, Summable u ∧ ∀ᶠ (n : α) in cofinite, ∀ k ∈ K, ‖f n k‖ ≤ u n
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: z : ℂ
c₁ c₂ : ℤ
⊢ Summable fun n ↦ ((↑c₁ * z + ↑n + 1) * (↑c₂ * z + ↑n))⁻¹

Tactic:
apply summable_inv_of_isBigO_rpow_inv (a := 2) (by norm_cast)
  simpa [pow_two] using (linear_inv_isBigO_right c₂ z).mul
    (linear_inv_isBigO_right_add c₁ 1 z)

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case refine_2
n k : ℕ
hn : n ≠ 0
hk₀ : 0 < k
hk₁ : k < n
hk₂ : Even k
zero_lt : 0 < ↑k * π / ↑n
lt_pi : ↑k * π / ↑n < π
⊢ cos π < cos (↑k * π / ↑n)

Tactic:
exact cos_lt_cos_of_nonneg_of_le_pi (le_of_lt zero_lt) (le_refl π) lt_pi

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: case refine_2
n k : ℕ
hn : n ≠ 0
hk₁ : k < n
hk₂ : Odd k
k_pos : 0 < k
zero_lt : 0 < ↑k * π / ↑n
lt_pi : ↑k * π / ↑n < π
⊢ cos π < cos (↑k * π / ↑n)

Tactic:
exact cos_lt_cos_of_nonneg_of_le_pi (le_of_lt zero_lt) (le_refl π) lt_pi

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Meromorphic

Goal state before:
pp: x : ℂ
⊢ x ∈ Set.univ → MeromorphicNFAt tan x

Tactic:
_

Goal state after:
x : ℂ
a✝ : x ∈ Set.univ
⊢ MeromorphicNFAt tan x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Meromorphic

Goal state before:
pp: x : ℂ
⊢ x ∈ Set.univ → MeromorphicNFAt tanh x

Tactic:
_

Goal state after:
x : ℂ
a✝ : x ∈ Set.univ
⊢ MeromorphicNFAt tanh x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: x : ℂ
h0 : x ≠ 0
⊢ Tendsto (fun n ↦ ∏ i ∈ Finset.range n, (1 + sineTerm x i)) atTop (𝓝 (Complex.sin (↑π * x) / (↑π * x)))

Tactic:
show (sin (π * x) / (π * x)) = sin (π * x) * (1 / (π * x)) by ring

Goal state after:
x : ℂ
h0 : x ≠ 0
⊢ Tendsto (fun n ↦ ∏ i ∈ Finset.range n, (1 + sineTerm x i)) atTop (𝓝 (Complex.sin (↑π * x) * (1 / (↑π * x))))
Module: Mathlib.Analysis.SpecificLimits.ArithmeticGeometric

Goal state before:
pp: R : Type u_1
a b u₀ : R
inst✝³ : Field R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
ha : 1 < a
h0 : b / (1 - a) < u₀
⊢ Tendsto (arithGeom a b u₀) atTop atTop

Tactic:
rw [arithGeom_eq' ha.ne']
  refine tendsto_atTop_add_const_right _ _ ?_
  refine Tendsto.atTop_mul_const (sub_pos.mpr h0) ?_
  exact tendsto_pow_atTop_atTop_of_one_lt ha

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: x : ℂ
hx : x ∈ ℂ_ℤ
n : ℕ
⊢ logDeriv (fun z ↦ ∏ j ∈ Finset.range n, (1 + sineTerm z j)) x = ∑ j ∈ Finset.range n, cotTerm x j

Tactic:
rw [logDeriv_prod]
  · simp_rw [logDeriv_sineTerm_eq_cotTerm hx]
  · exact fun i _ ↦ sineTerm_ne_zero hx i
  · fun_prop

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: A B : ℝ
hB : 0 < B
k : ℕ
hk : 1 ≤ k
| Summable fun i ↦ ‖(↑i + 1) ^ (-1 - ↑k)‖

Tactic:
1,

Goal state after:
A B : ℝ
hB : 0 < B
k : ℕ
hk : 1 ≤ k
| fun i ↦ ‖(↑i + 1) ^ (-1 - ↑k)‖
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: A B : ℝ
hB : 0 < B
k : ℕ
hk : 1 ≤ k
n : ℕ
| ‖((↑n + 1) ^ (1 + k))⁻¹‖

Tactic:
1,

Goal state after:
A B : ℝ
hB : 0 < B
k : ℕ
hk : 1 ≤ k
n : ℕ
| ((↑n + 1) ^ (1 + k))⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: A B : ℝ
hB : 0 < B
k : ℕ
hk : 1 ≤ k
n : ℕ
| ((↑n + 1) ^ (1 + k))⁻¹

Tactic:
1,

Goal state after:
A B : ℝ
hB : 0 < B
k : ℕ
hk : 1 ≤ k
n : ℕ
| (↑n + 1) ^ (1 + k)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: k : ℕ
hk : 1 ≤ k
⊢ ∀ K ⊆ ℍₒ,
    IsCompact K → ∃ u, Summable u ∧ ∀ (n : ℕ), ∀ k_1 ∈ K, ‖iteratedDerivWithin k (fun z ↦ cotTerm z n) ℍₒ k_1‖ ≤ u n

Tactic:
intro K hK hKc

Goal state after:
k : ℕ
hk : 1 ≤ k
K : Set ℂ
hK : K ⊆ ℍₒ
hKc : IsCompact K
⊢ ∃ u, Summable u ∧ ∀ (n : ℕ), ∀ k_1 ∈ K, ‖iteratedDerivWithin k (fun z ↦ cotTerm z n) ℍₒ k_1‖ ≤ u n
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: z : ℂ
k : ℕ
hk : 1 ≤ k
hz : z ∈ ℍₒ
| (-1) ^ k * ↑k ! * z ^ (-1 - ↑k) + ∑' (n : ℕ), iteratedDerivWithin k (fun t ↦ cotTerm t n) ℍₒ z =
    (-1) ^ k * ↑k ! * ∑' (n : ℤ), (z + ↑n) ^ (-1 - ↑k)

Tactic:
1,

Goal state after:
z : ℂ
k : ℕ
hk : 1 ≤ k
hz : z ∈ ℍₒ
| (-1) ^ k * ↑k ! * z ^ (-1 - ↑k) + ∑' (n : ℕ), iteratedDerivWithin k (fun t ↦ cotTerm t n) ℍₒ z
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent

Goal state before:
pp: z : ℂ
k : ℕ
hk : 1 ≤ k
hz : z ∈ ℍₒ
| ∑' (n : ℕ), iteratedDerivWithin k (fun t ↦ cotTerm t n) ℍₒ z

Tactic:
1,

Goal state after:
z : ℂ
k : ℕ
hk : 1 ≤ k
hz : z ∈ ℍₒ
| fun n ↦ iteratedDerivWithin k (fun t ↦ cotTerm t n) ℍₒ z
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc ↑a ↑b)
hg : AntitoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑a
gpos : 0 ≤ g (↑b - 1)
a✝ : ℝ
⊢ a✝ ∈ Icc ↑a ↑b → ∀ ⦃b_1 : ℝ⦄, b_1 ∈ Icc ↑a ↑b → a✝ ≤ b_1 → (fun x ↦ g (x - 1)) b_1 ≤ (fun x ↦ g (x - 1)) a✝

Tactic:
_

Goal state after:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc ↑a ↑b)
hg : AntitoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑a
gpos : 0 ≤ g (↑b - 1)
a✝ : ℝ
x✝ : a✝ ∈ Icc ↑a ↑b
⊢ ∀ ⦃b_1 : ℝ⦄, b_1 ∈ Icc ↑a ↑b → a✝ ≤ b_1 → (fun x ↦ g (x - 1)) b_1 ≤ (fun x ↦ g (x - 1)) a✝
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc ↑a ↑b)
hg : AntitoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑a
gpos : 0 ≤ g (↑b - 1)
a✝ : ℝ
x✝ : a✝ ∈ Icc ↑a ↑b
⊢ ∀ ⦃b_1 : ℝ⦄, b_1 ∈ Icc ↑a ↑b → a✝ ≤ b_1 → (fun x ↦ g (x - 1)) b_1 ≤ (fun x ↦ g (x - 1)) a✝

Tactic:
_

Goal state after:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc ↑a ↑b)
hg : AntitoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑a
gpos : 0 ≤ g (↑b - 1)
a✝ : ℝ
x✝ : a✝ ∈ Icc ↑a ↑b
b✝ : ℝ
⊢ b✝ ∈ Icc ↑a ↑b → a✝ ≤ b✝ → (fun x ↦ g (x - 1)) b✝ ≤ (fun x ↦ g (x - 1)) a✝
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc ↑a ↑b)
hg : AntitoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑a
gpos : 0 ≤ g (↑b - 1)
a✝ : ℝ
x✝ : a✝ ∈ Icc ↑a ↑b
b✝ : ℝ
⊢ b✝ ∈ Icc ↑a ↑b → a✝ ≤ b✝ → (fun x ↦ g (x - 1)) b✝ ≤ (fun x ↦ g (x - 1)) a✝

Tactic:
_

Goal state after:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc ↑a ↑b)
hg : AntitoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑a
gpos : 0 ≤ g (↑b - 1)
a✝ : ℝ
x✝¹ : a✝ ∈ Icc ↑a ↑b
b✝ : ℝ
x✝ : b✝ ∈ Icc ↑a ↑b
⊢ a✝ ≤ b✝ → (fun x ↦ g (x - 1)) b✝ ≤ (fun x ↦ g (x - 1)) a✝
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc ↑a ↑b)
hg : AntitoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑a
gpos : 0 ≤ g (↑b - 1)
a✝ : ℝ
x✝¹ : a✝ ∈ Icc ↑a ↑b
b✝ : ℝ
x✝ : b✝ ∈ Icc ↑a ↑b
⊢ a✝ ≤ b✝ → (fun x ↦ g (x - 1)) b✝ ≤ (fun x ↦ g (x - 1)) a✝

Tactic:
_

Goal state after:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc ↑a ↑b)
hg : AntitoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑a
gpos : 0 ≤ g (↑b - 1)
a✝¹ : ℝ
x✝¹ : a✝¹ ∈ Icc ↑a ↑b
b✝ : ℝ
x✝ : b✝ ∈ Icc ↑a ↑b
a✝ : a✝¹ ≤ b✝
⊢ (fun x ↦ g (x - 1)) b✝ ≤ (fun x ↦ g (x - 1)) a✝¹
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
hg : MonotoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑b
gpos : 0 ≤ g (↑a - 1)
⊢ MemLp (fun x ↦ g (x - 1)) ⊤ (volume.restrict (Icc ↑a ↑b))

Tactic:
apply MonotoneOn.memLp_isCompact isCompact_Icc

Goal state after:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
hg : MonotoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑b
gpos : 0 ≤ g (↑a - 1)
⊢ MonotoneOn (fun x ↦ g (x - 1)) (Icc ↑a ↑b)
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
hg : MonotoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑b
gpos : 0 ≤ g (↑a - 1)
a✝ : ℝ
⊢ a✝ ∈ Icc ↑a ↑b → ∀ ⦃b_1 : ℝ⦄, b_1 ∈ Icc ↑a ↑b → a✝ ≤ b_1 → (fun x ↦ g (x - 1)) a✝ ≤ (fun x ↦ g (x - 1)) b_1

Tactic:
_

Goal state after:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
hg : MonotoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑b
gpos : 0 ≤ g (↑a - 1)
a✝ : ℝ
x✝ : a✝ ∈ Icc ↑a ↑b
⊢ ∀ ⦃b_1 : ℝ⦄, b_1 ∈ Icc ↑a ↑b → a✝ ≤ b_1 → (fun x ↦ g (x - 1)) a✝ ≤ (fun x ↦ g (x - 1)) b_1
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
hg : MonotoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑b
gpos : 0 ≤ g (↑a - 1)
a✝ : ℝ
x✝ : a✝ ∈ Icc ↑a ↑b
⊢ ∀ ⦃b_1 : ℝ⦄, b_1 ∈ Icc ↑a ↑b → a✝ ≤ b_1 → (fun x ↦ g (x - 1)) a✝ ≤ (fun x ↦ g (x - 1)) b_1

Tactic:
_

Goal state after:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
hg : MonotoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑b
gpos : 0 ≤ g (↑a - 1)
a✝ : ℝ
x✝ : a✝ ∈ Icc ↑a ↑b
b✝ : ℝ
⊢ b✝ ∈ Icc ↑a ↑b → a✝ ≤ b✝ → (fun x ↦ g (x - 1)) a✝ ≤ (fun x ↦ g (x - 1)) b✝
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
hg : MonotoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑b
gpos : 0 ≤ g (↑a - 1)
a✝ : ℝ
x✝ : a✝ ∈ Icc ↑a ↑b
b✝ : ℝ
⊢ b✝ ∈ Icc ↑a ↑b → a✝ ≤ b✝ → (fun x ↦ g (x - 1)) a✝ ≤ (fun x ↦ g (x - 1)) b✝

Tactic:
_

Goal state after:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
hg : MonotoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑b
gpos : 0 ≤ g (↑a - 1)
a✝ : ℝ
x✝¹ : a✝ ∈ Icc ↑a ↑b
b✝ : ℝ
x✝ : b✝ ∈ Icc ↑a ↑b
⊢ a✝ ≤ b✝ → (fun x ↦ g (x - 1)) a✝ ≤ (fun x ↦ g (x - 1)) b✝
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
hg : MonotoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑b
gpos : 0 ≤ g (↑a - 1)
a✝ : ℝ
x✝¹ : a✝ ∈ Icc ↑a ↑b
b✝ : ℝ
x✝ : b✝ ∈ Icc ↑a ↑b
⊢ a✝ ≤ b✝ → (fun x ↦ g (x - 1)) a✝ ≤ (fun x ↦ g (x - 1)) b✝

Tactic:
_

Goal state after:
a b : ℕ
f g : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
hg : MonotoneOn g (Icc (↑a - 1) (↑b - 1))
fpos : 0 ≤ f ↑b
gpos : 0 ≤ g (↑a - 1)
a✝¹ : ℝ
x✝¹ : a✝¹ ∈ Icc ↑a ↑b
b✝ : ℝ
x✝ : b✝ ∈ Icc ↑a ↑b
a✝ : a✝¹ ≤ b✝
⊢ (fun x ↦ g (x - 1)) a✝¹ ≤ (fun x ↦ g (x - 1)) b✝
Module: Mathlib.CategoryTheory.Limits.FunctorToTypes

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
F : J ⥤ K ⥤ Type w
k : K
t : Cocone F
h : IsColimit t
x : t.pt.obj k
inst✝ : ∀ (k : K), HasColimit (F.flip.obj k)
hev : IsColimit (((evaluation K (Type w)).obj k).mapCocone t) := isColimitOfPreserves ((evaluation K (Type w)).obj k) h
⊢ ∃ j y, x = (ConcreteCategory.hom ((t.ι.app j).app k)) y

Tactic:
obtain ⟨j, y, rfl⟩ := Types.jointly_surjective _ hev x

Goal state after:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
F : J ⥤ K ⥤ Type w
k : K
t : Cocone F
h : IsColimit t
inst✝ : ∀ (k : K), HasColimit (F.flip.obj k)
hev : IsColimit (((evaluation K (Type w)).obj k).mapCocone t) := isColimitOfPreserves ((evaluation K (Type w)).obj k) h
j : J
y : (F ⋙ (evaluation K (Type w)).obj k).obj j
⊢ ∃ j_1 y_1,
    (ConcreteCategory.hom ((((evaluation K (Type w)).obj k).mapCocone t).ι.app j)) y =
      (ConcreteCategory.hom ((t.ι.app j_1).app k)) y_1
Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
ι : Type u_2
inst✝ : HasProductsOfShape ι C
H :
  ∀ ⦃J : ι → Type w⦄ [inst : (i : ι) → SmallCategory (J i)] [∀ (i : ι), IsFiltered (J i)] (F : (i : ι) → J i ⥤ C)
    [∀ (i : ι), HasColimit (F i)], ∃ c x, Nonempty (IsColimit (coconePointwiseProduct c))
J : ι → Type w
x✝¹ : (i : ι) → SmallCategory (J i)
x✝ : ∀ (i : ι), IsFiltered (J i)
F : (i : ι) → J i ⥤ C
c : (i : ι) → Cocone (F i)
hc : (i : ι) → IsColimit (c i)
this : ∀ (i : ι), HasColimit (F i)
c' : (i : ι) → Cocone (F i)
hc' : (i : ι) → IsColimit (c' i)
h✝ : Nonempty (IsColimit (coconePointwiseProduct c'))
e : coconePointwiseProduct c ≅ coconePointwiseProduct c' :=
  coconePointwiseProductIso F fun i ↦ (hc i).uniqueUpToIso (hc' i)
⊢ Nonempty (IsColimit (coconePointwiseProduct c))

Tactic:
(IsColimit.equivIsoColimit e).nonempty_congr

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
ι : Type u_2
inst✝ : HasProductsOfShape ι C
H :
  ∀ ⦃J : ι → Type w⦄ [inst : (i : ι) → SmallCategory (J i)] [∀ (i : ι), IsFiltered (J i)] (F : (i : ι) → J i ⥤ C)
    [∀ (i : ι), HasColimit (F i)], ∃ c x, Nonempty (IsColimit (coconePointwiseProduct c))
J : ι → Type w
x✝¹ : (i : ι) → SmallCategory (J i)
x✝ : ∀ (i : ι), IsFiltered (J i)
F : (i : ι) → J i ⥤ C
c : (i : ι) → Cocone (F i)
hc : (i : ι) → IsColimit (c i)
this : ∀ (i : ι), HasColimit (F i)
c' : (i : ι) → Cocone (F i)
hc' : (i : ι) → IsColimit (c' i)
h✝ : Nonempty (IsColimit (coconePointwiseProduct c'))
e : coconePointwiseProduct c ≅ coconePointwiseProduct c' :=
  coconePointwiseProductIso F fun i ↦ (hc i).uniqueUpToIso (hc' i)
⊢ Nonempty (IsColimit (coconePointwiseProduct c'))
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator G
A B : C
inst✝ : Injective B
M : ModuleCat (End G)ᵐᵒᵖ
g : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)
hg : Mono g
f : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)
l₁ : image (d g) ⟶ B := epiDesc (factorThruImage (d g)) (d f) ⋯
l₂ : A ⟶ B := Injective.factorThru l₁ (Limits.image.ι (d g))
| d g ≫ Injective.factorThru (epiDesc (factorThruImage (d g)) (d f) ⋯) (Limits.image.ι (d g))

Tactic:
congr; rw [← Limits.image.fac (d g)]

Goal state after:
case a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator G
A B : C
inst✝ : Injective B
M : ModuleCat (End G)ᵐᵒᵖ
g : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)
hg : Mono g
f : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)
l₁ : image (d g) ⟶ B := epiDesc (factorThruImage (d g)) (d f) ⋯
l₂ : A ⟶ B := Injective.factorThru l₁ (Limits.image.ι (d g))
| factorThruImage (d g) ≫ Limits.image.ι (d g)

case a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator G
A B : C
inst✝ : Injective B
M : ModuleCat (End G)ᵐᵒᵖ
g : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)
hg : Mono g
f : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)
l₁ : image (d g) ⟶ B := epiDesc (factorThruImage (d g)) (d f) ⋯
l₂ : A ⟶ B := Injective.factorThru l₁ (Limits.image.ι (d g))
| Injective.factorThru (epiDesc (factorThruImage (d g)) (d f) ⋯) (Limits.image.ι (d g))
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
a b : Over P
x✝ : a ≈ b
R : C
p : R ⟶ a.left
q : R ⟶ b.left
ep : Epi p
Eq : Epi q
comm : p ≫ a.hom = q ≫ b.hom
⊢ p ≫ a.hom ≫ f = q ≫ b.hom ≫ f

Tactic:
rw [reassoc_of% comm]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.OfObjectProperty

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P Q P' : ObjectProperty C
h : P ≤ P'
X✝ : C
⊢ ∀ ⦃Y : C⦄ (f : X✝ ⟶ Y), ofObjectProperty P Q f → ofObjectProperty P' Q f

Tactic:
_

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P Q P' : ObjectProperty C
h : P ≤ P'
X✝ Y✝ : C
⊢ ∀ (f : X✝ ⟶ Y✝), ofObjectProperty P Q f → ofObjectProperty P' Q f
Module: Mathlib.CategoryTheory.MorphismProperty.OfObjectProperty

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P Q P' : ObjectProperty C
h : P ≤ P'
X✝ Y✝ : C
⊢ ∀ (f : X✝ ⟶ Y✝), ofObjectProperty P Q f → ofObjectProperty P' Q f

Tactic:
_

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P Q P' : ObjectProperty C
h : P ≤ P'
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ ofObjectProperty P Q f✝ → ofObjectProperty P' Q f✝
Module: Mathlib.CategoryTheory.MorphismProperty.OfObjectProperty

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P Q Q' : ObjectProperty C
h : Q ≤ Q'
X✝ : C
⊢ ∀ ⦃Y : C⦄ (f : X✝ ⟶ Y), ofObjectProperty P Q f → ofObjectProperty P Q' f

Tactic:
_

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P Q Q' : ObjectProperty C
h : Q ≤ Q'
X✝ Y✝ : C
⊢ ∀ (f : X✝ ⟶ Y✝), ofObjectProperty P Q f → ofObjectProperty P Q' f