mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
a✝ : Nontrivial E
s : Set ↑(sphere 0 1)
hs : s ∈ {s | MeasurableSet s}
r : ↑(Ioi 0)
this : Ioo 0 ↑r = ↑r • Ioo 0 1
hpos : 0 < dim E
⊢ (comap Subtype.val μ) (⇑(homeomorphUnitSphereProd E) ⁻¹' s ×ˢ Iio r) =
    ↑(dim E) * μ (Ioo 0 1 • Subtype.val '' s) * ENNReal.ofReal (↑r ^ (dim E - 1 + 1) / (↑(dim E - 1) + 1))

Tactic:
comap_subtype_coe_apply (measurableSet_singleton _).compl,

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
a✝ : Nontrivial E
s : Set ↑(sphere 0 1)
hs : s ∈ {s | MeasurableSet s}
r : ↑(Ioi 0)
this : Ioo 0 ↑r = ↑r • Ioo 0 1
hpos : 0 < dim E
⊢ μ (Subtype.val '' ⇑(homeomorphUnitSphereProd E) ⁻¹' s ×ˢ Iio r) =
    ↑(dim E) * μ (Ioo 0 1 • Subtype.val '' s) * ENNReal.ofReal (↑r ^ (dim E - 1 + 1) / (↑(dim E - 1) + 1))
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
f : ↥L.lattice → ℂ → ℂ
u : ℝ → ↥L.lattice → ℝ
hu : ∀ r > 0, Summable (u r)
hf : ∀ r > 0, ∀ᶠ (R : ℝ) in atTop, ∀ (x : ℂ), ‖x‖ < r → ∀ (l : ↥L.lattice), ‖↑l‖ = R → ‖f l x‖ ≤ u r l
x : ℂ
r : ℝ
hr : 0 < r
hr' : 𝓝 x ≤ 𝓟 (Metric.ball 0 r)
R : ℝ
hR : ∀ (b : ℝ), R ≤ b → ∀ (x : ℂ), ‖x‖ < r → ∀ (l : ↥L.lattice), ‖↑l‖ = b → ‖f l x‖ ≤ u r l
⊢ ∀ᶠ (n : ↥L.lattice) in cofinite, ∀ x ∈ Metric.ball 0 r, ‖f n x‖ ≤ u r n

Tactic:
refine (isCompact_iff_finite.mp (isCompact_closedBall (0 : L.lattice) R)).subset ?_

Goal state after:
L : PeriodPair
f : ↥L.lattice → ℂ → ℂ
u : ℝ → ↥L.lattice → ℝ
hu : ∀ r > 0, Summable (u r)
hf : ∀ r > 0, ∀ᶠ (R : ℝ) in atTop, ∀ (x : ℂ), ‖x‖ < r → ∀ (l : ↥L.lattice), ‖↑l‖ = R → ‖f l x‖ ≤ u r l
x : ℂ
r : ℝ
hr : 0 < r
hr' : 𝓝 x ≤ 𝓟 (Metric.ball 0 r)
R : ℝ
hR : ∀ (b : ℝ), R ≤ b → ∀ (x : ℂ), ‖x‖ < r → ∀ (l : ↥L.lattice), ‖↑l‖ = b → ‖f l x‖ ≤ u r l
⊢ {x | (fun n ↦ ∀ x ∈ Metric.ball 0 r, ‖f n x‖ ≤ u r n) x}ᶜ ⊆ Metric.closedBall 0 R
Module: Mathlib.MeasureTheory.Constructions.HaarToSphere

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
x : ↑(sphere 0 1)
this : Nontrivial E
ε : ℝ
hε : 0 < ε
hε₂ : ε ≤ 2
⊢ ↑(toSphereBallBound (dim E) ε) * μ (ball 0 1) ≤ ↑(dim E) * μ (Ioo 0 1 • (ball (↑x) ε ∩ sphere 0 1))

Tactic:
grw [← ball_subset_sector_of_small_epsilon]

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
x : ↑(sphere 0 1)
this : Nontrivial E
ε : ℝ
hε : 0 < ε
hε₂ : ε ≤ 2
⊢ ↑(toSphereBallBound (dim E) ε) * μ (ball 0 1) ≤ ↑(dim E) * μ (ball ((1 - ε / 4) • ↑x) (ε / 4))

case hx
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
x : ↑(sphere 0 1)
this : Nontrivial E
ε : ℝ
hε : 0 < ε
hε₂ : ε ≤ 2
⊢ ‖↑x‖ = 1

case hε
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
x : ↑(sphere 0 1)
this : Nontrivial E
ε : ℝ
hε : 0 < ε
hε₂ : ε ≤ 2
⊢ 0 < ε

case hε2
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
μ : Measure E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : μ.IsAddHaarMeasure
x : ↑(sphere 0 1)
this : Nontrivial E
ε : ℝ
hε : 0 < ε
hε₂ : ε ≤ 2
⊢ ε ≤ 2
Module: Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric

Goal state before:
pp: a b : Multiset ℂ
n : ℕ
hb : ∀ k ∈ b, k ≠ -↑n
⊢ (Multiset.map (fun i ↦ Polynomial.eval i (ascPochhammer ℂ n) * (i + ↑n)) a).prod /
      (↑n ! * (↑n + 1) * (Multiset.map (fun j ↦ Gamma (j + ↑n) * (j + ↑n)) b).prod) =
    regularizedHGFunCoeff a b n *
      ((Multiset.map (fun x ↦ x + ↑n) a).prod / ((Multiset.map (fun x ↦ x + ↑n) b).prod * (↑n + 1)))

Tactic:
unfold regularizedHGFunCoeff
    simp_rw [div_mul_div_comm, Multiset.prod_map_mul]
    ring

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
hα : ¬Countable α
⊢ ¬Countable ↑univ

Tactic:
countable_coe_iff

Goal state after:
case neg
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
hα : ¬Countable α
⊢ ¬univ.Countable
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv

Goal state before:
pp: case neg
x : ℝ
h : ¬(x ≠ -1 ∧ x ≠ 1)
⊢ deriv arcsin x = 1 / √(1 - x ^ 2)

Tactic:
· rw [deriv_zero_of_not_differentiableAt (mt differentiableAt_arcsin.1 h)]
    simp only [not_and_or, Ne, Classical.not_not] at h
    rcases h with (rfl | rfl) <;> simp

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

Goal state before:
pp: case e'_5
m : ℕ
f : ℕ → ℝ := fun k ↦ 1 / (2 * ↑k + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ k
k : ℕ
⊢ 1 / (2 * ↑k + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ k =
    (↑(m + 1) + 1 / 2) * (2 * (1 / (2 * ↑k + 1)) * (1 / (2 * (↑m + 1) + 1)) ^ (2 * k + 1))

Tactic:
rw [← pow_mul, pow_add]

Goal state after:
case e'_5
m : ℕ
f : ℕ → ℝ := fun k ↦ 1 / (2 * ↑k + 1) * ((1 / (2 * ↑(m + 1) + 1)) ^ 2) ^ k
k : ℕ
⊢ 1 / (2 * ↑k + 1) * (1 / (2 * ↑(m + 1) + 1)) ^ (2 * k) =
    (↑(m + 1) + 1 / 2) * (2 * (1 / (2 * ↑k + 1)) * ((1 / (2 * (↑m + 1) + 1)) ^ (2 * k) * (1 / (2 * (↑m + 1) + 1)) ^ 1))
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality

Goal state before:
pp: x : ℝ
hx : x ∈ Set.Ioo (min (-1) 1) (max (-1) 1)
⊢ x ≠ -1

Tactic:
by aesop

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

Goal state before:
pp: x : ℝ
hx : x ∈ Set.Ioo (min (-1) 1) (max (-1) 1)
⊢ x ≠ 1

Tactic:
by aesop

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

Goal state before:
pp: n : ℕ
this : log (stirlingSeq 1) - log (stirlingSeq (n + 1)) ≤ 12⁻¹
⊢ 1 - 12⁻¹ - log 2 / 2 ≤ log (stirlingSeq (n + 1))

Tactic:
rw [stirlingSeq_one, log_div (by positivity), log_exp, log_sqrt] at this <;> grind

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

Goal state before:
pp: f : ℝ → ℝ
x : ℝ
hx : x ∈ uIcc 1 (-1)
⊢ -1 ≤ x

Tactic:
by aesop

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

Goal state before:
pp: f : ℝ → ℝ
x : ℝ
hx : x ∈ uIcc 1 (-1)
⊢ x ≤ 1

Tactic:
by aesop

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

Goal state before:
pp: f : ℝ → ℝ
x : ℝ
hx : x ∈ Ioo (min 1 (-1)) (max 1 (-1))
⊢ x ≠ -1

Tactic:
by aesop

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

Goal state before:
pp: f : ℝ → ℝ
x : ℝ
hx : x ∈ Ioo (min 1 (-1)) (max 1 (-1))
⊢ x ≠ 1

Tactic:
by aesop

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

Goal state before:
pp: n : ℤ
hn : n ≠ 0
hn' : ↑n ≠ 0
this : ∫ (θ : ℝ) in 0..↑n * π, cos θ = 0
⊢ (↑n)⁻¹ ≠ 0

Tactic:
by aesop

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

Goal state before:
pp: n m : ℕ
h : n ≠ m
⊢ ∫ (x : ℝ), eval x (T ℝ ↑n) * eval x (T ℝ ↑m) ∂measureT = 0

Tactic:
rw [integral_eval_T_real_mul_eval_T_real_measureT,
    integral_eval_T_real_measureT_of_ne_zero (by grind),
    integral_eval_T_real_measureT_of_ne_zero (by grind)]
  simp

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

Goal state before:
pp: n : ℕ
k : ℤ
hk : ¬2 * ↑n ∣ k
hn : n ≠ 0
this : ∑ i ∈ range n, 2 * cos (↑k * ((2 * ↑i + 1) / (2 * ↑n) * π)) = 0
⊢ π / ↑n ≠ 0

Tactic:
by aesop

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

Goal state before:
pp: n : ℕ
k : ℤ
hk : ¬2 * ↑n ∣ k
hn : n ≠ 0
this : ∑ i ∈ range n, 2 * Complex.cos (↑k * ((2 * ↑i + 1) / (2 * ↑n) * ↑π)) = 0
⊢ ∑ i ∈ range n, 2 * ↑(cos (↑k * ((2 * ↑i + 1) / (2 * ↑n) * π))) = 0

Tactic:
by aesop

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

Goal state before:
pp: n : ℕ
k : ℤ
hk : ¬2 * ↑n ∣ k
hn : n ≠ 0
this : (-1) ^ (-k) = (-1) ^ k
⊢ ¬2 * ↑n ∣ -k

Tactic:
by aesop

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

Goal state before:
pp: 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)

Tactic:
refine mul_nonneg ?_ (Finset.sum_nonneg' ?_)

Goal state after:
case refine_1
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))⁻¹)

case refine_2
n k i : ℕ
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
⊢ ∀ (i : Finset ℕ), 0 ≤ ∏ a ∈ i, (x - node n a)
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
x : ℂ
r : NNReal
hr0 : 0 < r
hr : Metric.closedBall x ↑r ⊆ (↑L.lattice)ᶜ
⊢ HasFPowerSeriesOnBall ℘[L - L.ω₁ / 2] (L.weierstrassPExceptSeries (L.ω₁ / 2) x) x ↑r

Tactic:
exact L.hasFPowerSeriesOnBall_weierstrassPExcept _ x r hr0
    (hr.trans (Set.compl_subset_compl.mpr Set.sdiff_subset))

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ Set.InjOn (fun k ↦ (2 * ↑k + 1) * π / (2 * ↑n)) ↑(Finset.range n)

Tactic:
by aesop

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

Goal state before:
pp: n : ℕ
hn : 2 ≤ n
x : ℝ
hx : ↑n * eval x (U ℝ (↑n - 1)) = 0
⊢ ↑n ≠ 0

Tactic:
by aesop

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

Goal state before:
pp: Z : Set ℂ
hZ2 : Z ⊆ ℂ_ℤ
hZC : IsCompact Z
x : ℂ
hx : x ∈ Z
⊢ x ∈ ℂ_ℤ

Tactic:
by aesop

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

Goal state before:
pp: x : ℂ
hx : x ∈ ℂ_ℤ
k : ℤ
⊢ x ≠ ↑k

Tactic:
by aesop

Goal state after:
Module: Mathlib.Data.Int.Fib.Basic

Goal state before:
pp: case inl
n : ℕ
hn0 : ¬n + n = 0
this : -↑(n + n) + 1 = -↑(n + n - 1)
⊢ (-1) ^ (n + n) * (-1) ^ 1 * (↑(Nat.fib (n + n)) - ↑(Nat.fib (n + n - 1) + Nat.fib (n + n))) =
    (-1) ^ (n + n - 1 + 1) * ↑(Nat.fib (n + n - 1))

Tactic:
← two_mul,

Goal state after:
case inl
n : ℕ
hn0 : ¬n + n = 0
this : -↑(n + n) + 1 = -↑(n + n - 1)
⊢ (-1) ^ (2 * n) * (-1) ^ 1 * (↑(Nat.fib (2 * n)) - ↑(Nat.fib (2 * n - 1) + Nat.fib (2 * n))) =
    (-1) ^ (2 * n - 1 + 1) * ↑(Nat.fib (2 * n - 1))
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ kernel.map f (f ≫ g) (𝟙 X) g ⋯ ≫ kernel.map (f ≫ g) g f (𝟙 Z) ⋯ = 0

Tactic:
by aesop

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ cokernel.map f (f ≫ g) (𝟙 X) g ⋯ ≫ cokernel.map (f ≫ g) g f (𝟙 Z) ⋯ = 0

Tactic:
by aesop

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ (-kernel.ι g) ≫ (snakeInput f g).L₂.f = (kernel.ι g ≫ biprod.inr) ≫ (snakeInput f g).v₁₂.τ₂

Tactic:
by aesop

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: case refine_2
f : ℝ → ℝ
N : ℕ
anti : AntitoneOn f (Set.Ici ↑N)
integrable : IntegrableOn f (Set.Ioi ↑N) volume
nonneg : ∀ t ∈ Set.Ioi ↑N, 0 ≤ f t
s : Finset ℕ
t : ℕ
ht : s ⊆ Finset.range t
⊢ ∑ i ∈ s, f ↑(i + N + 1) ≤ ∫ (x : ℝ) in Set.Ioi ↑N, f x

Tactic:
calc
      ∑ i ∈ s, f ↑(i + N + 1) ≤ ∑ i ∈ range t, f ↑(i + N + 1) :=
        sum_le_sum_of_subset_of_nonneg ht <| by grind
      _ = ∑ i ∈ Ico N (N + t), f ↑(i + 1) := by rw [Finset.sum_Ico_eq_sum_range]; grind
      _ ≤ ∫ (x : ℝ) in Set.Ioi (N : ℝ), f x :=
        (anti.mono <| by grind).sum_Ico_le_integral integrable nonneg

Goal state after:
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: f : ℝ → ℝ
N : ℕ
anti : AntitoneOn f (Ici ↑N)
summable : Summable fun n ↦ f ↑(n + N)
nonneg : ∀ t ∈ Ioi ↑N, 0 ≤ f t
⊢ IntegrableOn f (Ioi ↑N) volume

Tactic:
refine integrableOn_Ioi_of_intervalIntegral_norm_bounded (∑' (n : ℕ), f (n + N : ℕ)) _ ?_
    (tendsto_atTop_add_const_right atTop (N : ℝ) tendsto_natCast_atTop_atTop) ?_

Goal state after:
case refine_1
f : ℝ → ℝ
N : ℕ
anti : AntitoneOn f (Ici ↑N)
summable : Summable fun n ↦ f ↑(n + N)
nonneg : ∀ t ∈ Ioi ↑N, 0 ≤ f t
⊢ ∀ (i : ℕ), IntegrableOn f (Ioc (↑N) (↑i + ↑N)) volume

case refine_2
f : ℝ → ℝ
N : ℕ
anti : AntitoneOn f (Ici ↑N)
summable : Summable fun n ↦ f ↑(n + N)
nonneg : ∀ t ∈ Ioi ↑N, 0 ≤ f t
⊢ ∀ᶠ (i : ℕ) in atTop, ∫ (x : ℝ) in ↑N..↑i + ↑N, ‖f x‖ ≤ ∑' (n : ℕ), f ↑(n + N)
Module: Mathlib.Analysis.SpecificLimits.FloorPow

Goal state before:
pp: case a
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
B : c ^ 2 * (1 - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹
C : c⁻¹ ^ 2 < 1
⊢ Real.log j / Real.log c * (↑2 * Real.log c) = ↑2 * Real.log j

Tactic:
field [(Real.log_pos hc).ne']

Goal state after:
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)
    [inst_2 : ∀ (i : ι), HasColimit (F i)],
    ∃ (x : HasColimit (pointwiseProduct F)), IsIso (colimitPointwiseProductToProductColimit F)
J : ι → Type w
x✝² : (i : ι) → SmallCategory (J i)
x✝¹ : ∀ (i : ι), IsFiltered (J i)
F : (i : ι) → J i ⥤ C
x✝ : ∀ (i : ι), HasColimit (F i)
⊢ ∃ c x, Nonempty (IsColimit (coconePointwiseProduct c))

Tactic:
refine ⟨fun i ↦ colimit.cocone _, fun i ↦ colimit.isColimit _, ?_⟩

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)
    [inst_2 : ∀ (i : ι), HasColimit (F i)],
    ∃ (x : HasColimit (pointwiseProduct F)), IsIso (colimitPointwiseProductToProductColimit F)
J : ι → Type w
x✝² : (i : ι) → SmallCategory (J i)
x✝¹ : ∀ (i : ι), IsFiltered (J i)
F : (i : ι) → J i ⥤ C
x✝ : ∀ (i : ι), HasColimit (F i)
⊢ Nonempty (IsColimit (coconePointwiseProduct fun i ↦ colimit.cocone (F i)))
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected

Goal state before:
pp: J : Type w
inst✝⁵ : Category.{w', w} J
inst✝⁴ : IsConnected J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasPullbacks C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasExactColimitsOfShape J C
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X : C
f : X ⟶ c.pt
⊢ IsIso (colimMap (pullback.snd c.ι ((Functor.const J).map f)))

Tactic:
have hpull := colim.map_isPullback (IsPullback.of_hasPullback c.ι ((Functor.const J).map f))

Goal state after:
J : Type w
inst✝⁵ : Category.{w', w} J
inst✝⁴ : IsConnected J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasPullbacks C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasExactColimitsOfShape J C
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X : C
f : X ⟶ c.pt
hpull :
  IsPullback (colim.map (pullback.fst c.ι ((Functor.const J).map f)))
    (colim.map (pullback.snd c.ι ((Functor.const J).map f))) (colim.map c.ι) (colim.map ((Functor.const J).map f))
⊢ IsIso (colimMap (pullback.snd c.ι ((Functor.const J).map f)))
Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct

Goal state before:
pp: α : Type u
I : α → Type u
inst✝¹ : (i : α) → SmallCategory (I i)
inst✝ : ∀ (i : α), IsFiltered (I i)
F : (i : α) → I i ⥤ Type u
ky : (i : α) → I i
yk₀ : (pointwiseProduct F).obj ky
ky' : (i : α) → I i
yk₀' : (pointwiseProduct F).obj ky'
k : (i : α) → I i := IsFiltered.max ky ky'
yk : ∏ᶜ (Functor.pi F).obj k := (hom ((pointwiseProduct F).map (IsFiltered.leftToMax ky ky'))) yk₀
yk' : ∏ᶜ (Functor.pi F).obj k := (hom ((pointwiseProduct F).map (IsFiltered.rightToMax ky ky'))) yk₀'
hyk₀ : (hom (colimit.ι (pointwiseProduct F) ky)) yk₀ = (hom (colimit.ι (pointwiseProduct F) k)) yk
hyk₀' : (hom (colimit.ι (pointwiseProduct F) ky')) yk₀' = (hom (colimit.ι (pointwiseProduct F) k)) yk'
hy :
  (hom (colimitPointwiseProductToProductColimit F)) ((hom (colimit.ι (pointwiseProduct F) k)) yk) =
    (hom (colimitPointwiseProductToProductColimit F)) ((hom (colimit.ι (pointwiseProduct F) k)) yk')
s : α
hy₁ :
  (hom (Pi.π (fun s ↦ colimit (F s)) s))
      ((hom (colimitPointwiseProductToProductColimit F)) ((hom (colimit.ι (pointwiseProduct F) k)) yk)) =
    (hom (colimit.ι (F s) (k s))) ((hom (Pi.π ((Functor.pi F).obj k) s)) yk)
i₀ : I s
f₀ g₀ : k s ⟶ i₀
h₀ :
  (hom ((F s).map f₀)) ((hom (Pi.π ((Functor.pi F).obj k) s)) yk) =
    (hom ((F s).map g₀)) ((hom (Pi.π ((Functor.pi F).obj k) s)) yk')
| (hom ((F s).map (f₀ ≫ IsFiltered.coeqHom f₀ g₀))) ((hom (Pi.π (fun s ↦ (F s).obj (k s)) s)) yk')

Tactic:
IsFiltered.coeq_condition

Goal state after:
α : Type u
I : α → Type u
inst✝¹ : (i : α) → SmallCategory (I i)
inst✝ : ∀ (i : α), IsFiltered (I i)
F : (i : α) → I i ⥤ Type u
ky : (i : α) → I i
yk₀ : (pointwiseProduct F).obj ky
ky' : (i : α) → I i
yk₀' : (pointwiseProduct F).obj ky'
k : (i : α) → I i := IsFiltered.max ky ky'
yk : ∏ᶜ (Functor.pi F).obj k := (hom ((pointwiseProduct F).map (IsFiltered.leftToMax ky ky'))) yk₀
yk' : ∏ᶜ (Functor.pi F).obj k := (hom ((pointwiseProduct F).map (IsFiltered.rightToMax ky ky'))) yk₀'
hyk₀ : (hom (colimit.ι (pointwiseProduct F) ky)) yk₀ = (hom (colimit.ι (pointwiseProduct F) k)) yk
hyk₀' : (hom (colimit.ι (pointwiseProduct F) ky')) yk₀' = (hom (colimit.ι (pointwiseProduct F) k)) yk'
hy :
  (hom (colimitPointwiseProductToProductColimit F)) ((hom (colimit.ι (pointwiseProduct F) k)) yk) =
    (hom (colimitPointwiseProductToProductColimit F)) ((hom (colimit.ι (pointwiseProduct F) k)) yk')
s : α
hy₁ :
  (hom (Pi.π (fun s ↦ colimit (F s)) s))
      ((hom (colimitPointwiseProductToProductColimit F)) ((hom (colimit.ι (pointwiseProduct F) k)) yk)) =
    (hom (colimit.ι (F s) (k s))) ((hom (Pi.π ((Functor.pi F).obj k) s)) yk)
i₀ : I s
f₀ g₀ : k s ⟶ i₀
h₀ :
  (hom ((F s).map f₀)) ((hom (Pi.π ((Functor.pi F).obj k) s)) yk) =
    (hom ((F s).map g₀)) ((hom (Pi.π ((Functor.pi F).obj k) s)) yk')
| (hom ((F s).map (g₀ ≫ IsFiltered.coeqHom f₀ g₀))) ((hom (Pi.π (fun s ↦ (F s).obj (k s)) s)) yk')
Module: Mathlib.CategoryTheory.Preadditive.Injective.Resolution

Goal state before:
pp: case succ
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
I : InjectiveResolution Z
n✝ : ℕ
⊢ Mono (I.ι.f (n✝ + 1))

Tactic:
rw [ι_f_succ]

Goal state after:
case succ
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
I : InjectiveResolution Z
n✝ : ℕ
⊢ Mono 0
Module: Mathlib.CategoryTheory.Abelian.Injective.Ext

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
R : InjectiveResolution Y
n : ℕ
f : X ⟶ R.cocomplex.X n
m : ℕ
hm : n + 1 = m
hf : f ≫ R.cocomplex.d n m = 0
p : ℕ
hp : p + 1 = n
⊢ (∃ g,
      g ≫ (R.cochainComplexXIso (↑p) p ⋯).hom ≫ R.cocomplex.d p n ≫ (R.cochainComplexXIso (↑n) n ⋯).inv =
        f ≫ (R.cochainComplexXIso (↑n) n ⋯).inv) ↔
    ∃ g, g ≫ R.cocomplex.d p n = f

Tactic:
exact ⟨fun ⟨g, hg⟩ ↦ ⟨g ≫ (R.cochainComplexXIso p p rfl).hom,
      by simp only [← cancel_mono (R.cochainComplexXIso n n rfl).inv, Category.assoc, hg]⟩,
    fun ⟨g, hg⟩ ↦ ⟨g ≫ (R.cochainComplexXIso p p rfl).inv, by simp [← hg]⟩⟩

Goal state after:
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
x y : Pseudoelement P
a a' : Over P
h : pseudoApply f ⟦a⟧ = pseudoApply f ⟦a'⟧
R : C
p : R ⟶ ((fun g ↦ app f g) a).left
q : R ⟶ ((fun g ↦ app f g) a').left
ep : Epi p
w✝ : Epi q
comm : p ≫ ((fun g ↦ app f g) a).hom = q ≫ ((fun g ↦ app f g) a').hom
a'' : R ⟶ P := p ≫ a.hom - q ≫ a'.hom
Z : C
g : P ⟶ Z
hh : pseudoApply g ⟦a'⟧ = 0
⊢ pseudoApply g (Quot.mk (PseudoEqual P) (Over.mk a'')) = pseudoApply g ⟦a⟧

Tactic:
by
          obtain ⟨X, p', q', ep', _, comm'⟩ := Quotient.exact hh
          have : a'.hom ≫ g = 0 := by
            apply (epi_iff_cancel_zero _).1 ep' _ (a'.hom ≫ g)
            simpa using comm'
          apply Quotient.sound
          -- Can we prevent quotient.sound from giving us this weird `coe_b` thingy?
          change app g (a'' : Over P) ≈ app g a
          exact ⟨R, 𝟙 R, p, inferInstance, ep, by simp [a'', sub_eq_add_neg, this]⟩

Goal state after:
Module: Mathlib.CategoryTheory.Action.Concrete

Goal state before:
pp: X : Type u
⊢ ∀ (x y : Function.End X), ↾(x * y) = ↾x * ↾y

Tactic:
by aesop

Goal state after:
Module: Mathlib.CategoryTheory.Action.Monoidal

Goal state before:
pp: V : Type u_1
inst✝⁵ : Category.{v_1, u_1} V
G : Type u_2
inst✝⁴ : Monoid G
W : Type u_3
inst✝³ : Category.{v_2, u_3} W
inst✝² : MonoidalCategory V
inst✝¹ : MonoidalCategory W
F : V ⥤ W
inst✝ : F.LaxMonoidal
g : G
⊢ 𝟙 (𝟙_ W) ≫ ε F = ε F ≫ F.map (𝟙 (𝟙_ V))

Tactic:
rw [Category.id_comp, F.map_id, Category.comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F G H I : B ⥤ᴸ C
η : F ⟶ G
θ ι : G ⟶ H
Γ : θ ⟶ ι
a b : B
f : a ⟶ b
⊢ F.map f ◁ η.app b ◁ Γ.as.app b ≫ (η ≫ ι).naturality f = (η ≫ θ).naturality f ≫ (η.app a ◁ Γ.as.app a) ▷ H.map f

Tactic:
dsimp only [comp_app, comp_naturality]
      calc
        _ = 𝟙 _ ⊗≫ ((F.map f ≫ η.app b) ◁ Γ.as.app b ≫ η.naturality f ▷ ι.app b) ⊗≫
            η.app a ◁ ι.naturality f ⊗≫ 𝟙 _ := by
          bicategory
        _ = 𝟙 _ ⊗≫ η.naturality f ▷ θ.app b ⊗≫ η.app a ◁ (G.map f ◁ Γ.as.app b ≫
            ι.naturality f) ⊗≫ 𝟙 _ := by
          rw [whisker_exchange]
          bicategory
        _ = _ := by
          rw [Γ.as.naturality]
          bicategory

Goal state after:
Module: Mathlib.CategoryTheory.Category.PartialFun

Goal state before:
pp: X Y Z : Pointed
f : X ⟶ Y
g : Y ⟶ Z
x✝¹ : PartialFun.of { x // x ≠ X.point }
x✝ : PartialFun.of { x // x ≠ Z.point }
a : X.X
ha : a ≠ X.point
c : Z.X
hc : c ≠ Z.point
this : c = g.toFun (f.toFun a) → ¬Y.point = f.toFun a ∧ ¬Z.point = g.toFun (f.toFun a)
⊢ ↑⟨c, hc⟩ = (f ≫ g).toFun ↑⟨a, ha⟩ →
    ∃ a_2 ∈ (PFun.toSubtype (fun x ↦ x ≠ Y.point) f.toFun ∘ Subtype.val) ⟨a, ha⟩,
      ⟨c, hc⟩ ∈ (PFun.toSubtype (fun x ↦ x ≠ Z.point) g.toFun ∘ Subtype.val) a_2

Tactic:
by aesop

Goal state after:
Module: Mathlib.CategoryTheory.Category.RelCat

Goal state before:
pp: X Y : RelCat
r : X ⟶ Y
h : IsIso r
h1 : ∀ (a b : X), (∃ y, (a, y) ∈ r.rel ∧ (y, b) ∈ (inv r).rel) ↔ a = b
h2 : ∀ (a b : Y), (∃ y, (a, y) ∈ (inv r).rel ∧ (y, b) ∈ r.rel) ↔ a = b
f : X → Y
hf : ∀ (x : X), (x, f x) ∈ r.rel ∧ (f x, x) ∈ (inv r).rel
g : Y → X
hg : ∀ (x : Y), (x, g x) ∈ (inv r).rel ∧ (g x, x) ∈ r.rel
hif : IsIso (↾f)
x : graphFunctor.obj X
y : graphFunctor.obj Y
⊢ (x, y) ∈ (graphFunctor.map (asIso (↾f)).hom).rel → (x, y) ∈ r.rel

Tactic:
by aesop

Goal state after: