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

Goal state before:
pp: n : ℕ
x : ↑(Ioi 0)
hr₀ : 0 ≤ ↑x
⊢ ∫⁻ (x : ℝ) in Ioo 0 ↑x, ENNReal.ofReal (x ^ n) ∂volume = ENNReal.ofReal (↑x ^ (n + 1) / (↑n + 1))

Tactic:
restrict_congr_set Ioo_ae_eq_Ioc,

Goal state after:
n : ℕ
x : ↑(Ioi 0)
hr₀ : 0 ≤ ↑x
⊢ ∫⁻ (x : ℝ) in Ioc 0 ↑x, ENNReal.ofReal (x ^ n) ∂volume = ENNReal.ofReal (↑x ^ (n + 1) / (↑n + 1))
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
⊢ ¬((1 / 2).den = 1 ∧ Rat.den 0 = 1)

Tactic:
by norm_num

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

Goal state before:
pp: L : PeriodPair
⊢ ¬(Rat.den 0 = 1 ∧ (1 / 2).den = 1)

Tactic:
by norm_num

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

Goal state before:
pp: E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
hx : ‖x‖ = 1
ε : ℝ
hε : 0 < ε
hε2 : ε ≤ 2
y : E
hy : dist y ((1 - ε / 4) • x) < ε / 4
habs : |1 - ε / 4| = 1 - ε / 4
hy₀ : y ≠ 0
⊢ y ∈ Ioo 0 1 • (ball x ε ∩ sphere 0 1)

Tactic:
have hy₁ : ‖y‖ < 1 := calc
    ‖y‖ ≤ dist y ((1 - ε / 4) • x) + ‖(1 - ε / 4) • x‖ := by
      simpa using dist_triangle y ((1 - ε / 4) • x) 0
    _ < ε / 4 + ‖(1 - ε / 4) • x‖ := by gcongr
    _ = 1 := by simp [norm_smul, habs, hx]

Goal state after:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
hx : ‖x‖ = 1
ε : ℝ
hε : 0 < ε
hε2 : ε ≤ 2
y : E
hy : dist y ((1 - ε / 4) • x) < ε / 4
habs : |1 - ε / 4| = 1 - ε / 4
hy₀ : y ≠ 0
hy₁ : ‖y‖ < 1
⊢ y ∈ Ioo 0 1 • (ball x ε ∩ sphere 0 1)
Module: Mathlib.Analysis.SpecialFunctions.Sigmoid

Goal state before:
pp: ⊢ 1 + 0 ≠ 0

Tactic:
by norm_num

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

Goal state before:
pp: case e'_9
h : 1 ≠ -1
⊢ 1 / √(1 - 1 ^ 2) = 0

Tactic:
simp +contextual [arcsin_of_one_le]

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

Goal state before:
pp: case inl.convert_3
h : 1 ≠ -1
⊢ ∀ x ∈ Ici 1, arcsin x = π / 2

Tactic:
simp +contextual [arcsin_of_one_le]

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

Goal state before:
pp: case inl.convert_4
h : 1 ≠ -1
⊢ arcsin 1 = π / 2

Tactic:
simp +contextual [arcsin_of_one_le]

Goal state after:
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff

Goal state before:
pp: case inr.hint
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
h'ab : a < b
this : ContinuousOn (derivWithin f (Icc a b)) (Icc a b)
⊢ derivWithin f (Icc a b) =ᵐ[volume.restrict (Ioc a b)] deriv f

Tactic:
← restrict_Ioo_eq_restrict_Ioc

Goal state after:
case inr.hint
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
h'ab : a < b
this : ContinuousOn (derivWithin f (Icc a b)) (Icc a b)
⊢ derivWithin f (Icc a b) =ᵐ[volume.restrict (Ioo a b)] deriv f
Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff

Goal state before:
pp: E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
⊢ derivWithin f (Icc a b) =ᵐ[volume.restrict (Ioc a b)] deriv f

Tactic:
← restrict_Ioo_eq_restrict_Ioc

Goal state after:
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inst✝ : CompleteSpace E
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
⊢ derivWithin f (Icc a b) =ᵐ[volume.restrict (Ioo a b)] deriv f
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality

Goal state before:
pp: f : ℝ → ℝ
⊢ -1 ≤ 1

Tactic:
by norm_num

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

Goal state before:
pp: f : ℝ → ℝ
hf : ContinuousOn f (Set.Icc (-1) 1)
⊢ -1 < 1

Tactic:
by norm_num

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

Goal state before:
pp: f : ℝ → ℝ
hf : ContinuousOn f (Set.uIcc (-1) 1)
this : IntegrableOn (fun x ↦ f x * √(1 - x ^ 2)⁻¹) (Set.uIoc (-1) 1) volume
⊢ -1 ≤ 1

Tactic:
by norm_num

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

Goal state before:
pp: a : ℝ
hane : a ≠ 0
ha : Tendsto stirlingSeq atTop (𝓝 a)
⊢ Tendsto Wallis.W atTop (𝓝 (a ^ 2 / 2))

Tactic:
by
  refine Tendsto.congr' (eventually_atTop.mpr ⟨1, fun n hn =>
    stirlingSeq_pow_four_div_stirlingSeq_pow_two_eq n (one_le_iff_ne_zero.mp hn)⟩) ?_
  have h : a ^ 2 / 2 = a ^ 4 / a ^ 2 * (1 / 2) := by
    rw [mul_one_div, ← mul_one_div (a ^ 4) (a ^ 2), one_div, ← pow_sub_of_lt a]
    simp
  rw [h]
  exact ((ha.pow 4).div ((ha.comp (tendsto_id.const_mul_atTop' two_pos)).pow 2)
    (pow_ne_zero 2 hane)).mul tendsto_self_div_two_mul_self_add_one

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ (log (2 * π) + log ↑n) / 2 + ↑n * (log ↑n - 1) = log √(2 * π * ↑n) + log ((↑n / rexp 1) ^ n)

pp: case hx
n : ℕ
hn : n ≠ 0
⊢ √(2 * π * ↑n) ≠ 0

pp: case hy
n : ℕ
hn : n ≠ 0
⊢ (↑n / rexp 1) ^ n ≠ 0

Tactic:
log_sqrt,

Goal state after:
n : ℕ
hn : n ≠ 0
⊢ (log (2 * π) + log ↑n) / 2 + ↑n * (log ↑n - 1) = log (2 * π * ↑n) / 2 + log ((↑n / rexp 1) ^ n)

n : ℕ
hn : n ≠ 0
⊢ 0 ≤ 2 * π * ↑n

case hx
n : ℕ
hn : n ≠ 0
⊢ √(2 * π * ↑n) ≠ 0

case hy
n : ℕ
hn : n ≠ 0
⊢ (↑n / rexp 1) ^ n ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: case inr
n i : ℕ
hi : i ≤ n
hn : n ≠ 0
h₁ : 0 < (-1) ^ i * ∏ x ∈ Finset.range i, (node n i - node n x)
⊢ 0 < (-1) ^ i * ∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j)

Tactic:
have h₂ : 0 < ∏ j ∈ Finset.Ioc i n, (node n i - node n j) :=
    Finset.prod_pos (fun j hj => sub_pos.mpr <|
      node_lt (Finset.mem_Ioc.mp hj).2 (Finset.mem_Ioc.mp hj).1)

Goal state after:
case inr
n i : ℕ
hi : i ≤ n
hn : n ≠ 0
h₁ : 0 < (-1) ^ i * ∏ x ∈ Finset.range i, (node n i - node n x)
h₂ : 0 < ∏ j ∈ Finset.Ioc i n, (node n i - node n j)
⊢ 0 < (-1) ^ i * ∏ j ∈ (Finset.range (n + 1)).erase i, (node n i - node n j)
Module: Mathlib.NumberTheory.Niven

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : DivisionRing α
inst✝ : CharZero α
q : ℚ
h₁ : IsIntegral ℤ q
k✝ : ℤ
h : (algebraMap ℤ ℚ) k✝ = q
⊢ ↑q = ↑k✝

Tactic:
simp [← h]

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

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

Tactic:
by norm_num

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

Goal state before:
pp: case eval_fg
n : ℕ
c : ℕ → ℝ
hcpos : ∀ i ≤ n, 0 < (-1) ^ i * c i
P : ℝ[X]
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
h : ∑ i ≤ n, eval (node n i) (T ℝ ↑n) * c i ≤ ∑ i ≤ n, eval (node n i) P * c i
⊢ ∀ x ∈ Finset.image (fun x ↦ node n x) (Finset.range (n + 1)), eval x P = eval x (T ℝ ↑n)

Tactic:
contrapose! h

Goal state after:
case eval_fg
n : ℕ
c : ℕ → ℝ
hcpos : ∀ i ≤ n, 0 < (-1) ^ i * c i
P : ℝ[X]
hPdeg : P.degree ≤ ↑n
hPbnd : ∀ x ∈ Set.Icc (-1) 1, |eval x P| ≤ 1
h : ∃ x ∈ Finset.image (fun x ↦ node n x) (Finset.range (n + 1)), eval x P ≠ eval x (T ℝ ↑n)
⊢ ∑ i ≤ n, eval (node n i) P * c i < ∑ i ≤ n, eval (node n i) (T ℝ ↑n) * c i
Module: Mathlib.Order.Interval.Finset.Box

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹⁰ : Ring α
inst✝⁹ : PartialOrder α
inst✝⁸ : IsOrderedRing α
inst✝⁷ : Ring β
inst✝⁶ : PartialOrder β
inst✝⁵ : IsOrderedRing β
inst✝⁴ : LocallyFiniteOrder α
inst✝³ : LocallyFiniteOrder β
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableLE (α × β)
n : ℕ
⊢ #(Icc (-1.1 + -(↑n).1) ((↑n).1 + 1.1)) * #(Icc (-1 + -↑n).2 (↑n + 1).2) -
      #(Icc (-(↑n).1) (↑n).1) * #(Icc (-↑n).2 (↑n).2) =
    #(Icc (-1 + -↑n) (↑n + 1)) * #(Icc (-1 + -↑n) (↑n + 1)) - #(Icc (-↑n) ↑n) * #(Icc (-↑n) ↑n)

Tactic:
fst_one,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹⁰ : Ring α
inst✝⁹ : PartialOrder α
inst✝⁸ : IsOrderedRing α
inst✝⁷ : Ring β
inst✝⁶ : PartialOrder β
inst✝⁵ : IsOrderedRing β
inst✝⁴ : LocallyFiniteOrder α
inst✝³ : LocallyFiniteOrder β
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : DecidableLE (α × β)
n : ℕ
⊢ #(Icc (-1 + -(↑n).1) ((↑n).1 + 1)) * #(Icc (-1 + -↑n).2 (↑n + 1).2) -
      #(Icc (-(↑n).1) (↑n).1) * #(Icc (-↑n).2 (↑n).2) =
    #(Icc (-1 + -↑n) (↑n + 1)) * #(Icc (-1 + -↑n) (↑n + 1)) - #(Icc (-↑n) ↑n) * #(Icc (-↑n) ↑n)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable

Goal state before:
pp: case hab
z : ℍ
A B : ℝ
h : 0 < B
hz : z ∈ verticalStrip A B
⊢ |z.re| ≤ { coe := { re := A, im := B }, coe_im_pos := h }.re

pp: case hab
z : ℍ
A B : ℝ
h : 0 < B
hz : z ∈ verticalStrip A B
⊢ { coe := { re := A, im := B }, coe_im_pos := h }.im ≤ z.im

Tactic:
exacts [hz.1, hz.2]

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

Goal state before:
pp: n k i : ℕ
hi : i ≤ n
x : ℝ
hx : 1 ≤ x
t : Finset ℕ
a : ℕ
x✝ : a ∈ t
⊢ 0 ≤ x - node n a

Tactic:
grind [show node n a ≤ 1 from cos_le_one _]

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

Goal state before:
pp: case inr
n : ℤ
hn : n ≠ 0
x : ℝ
hx : 1 < |x|
this : ∀ {n : ℤ}, n ≠ 0 → ∀ {x : ℝ}, 1 < |x| → 0 ≤ x → 1 < |eval x (T ℝ n)|
h : x < 0
⊢ 1 < |eval x (T ℝ n)|

pp: n : ℤ
hn : n ≠ 0
x : ℝ
hx : 1 < |x|
h : 0 ≤ x
⊢ 1 < |eval x (T ℝ n)|

Tactic:
· simpa [T_eval_neg, abs_mul, abs_unit_intCast] using @this n hn (-x) (by grind) (by grind)

Goal state after:
n : ℤ
hn : n ≠ 0
x : ℝ
hx : 1 < |x|
h : 0 ≤ x
⊢ 1 < |eval x (T ℝ n)|
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
t : Finset ℕ
x✝¹ : t ∈ Finset.powersetCard (n - k) ((Finset.range (n + 1)).erase i)
a : ℕ
x✝ : a ∈ t
⊢ 0 ≤ x - node n a

Tactic:
grind [show node n a ≤ 1 from cos_le_one _]

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

Goal state before:
pp: x : ℂ
hx : x ∈ ℂ_ℤ
⊢ Tendsto (fun n ↦ ∑ j ∈ Finset.range n, cotTerm x j) atTop (𝓝 (↑π * (↑π * x).cot - 1 / x))

Tactic:
simp_rw [← logDeriv_sin_div_eq_cot hx, ← logDeriv_prod_sineTerm_eq_sum_cotTerm hx]

Goal state after:
x : ℂ
hx : x ∈ ℂ_ℤ
⊢ Tendsto (fun n ↦ logDeriv (fun z ↦ ∏ j ∈ Finset.range n, (1 + sineTerm z j)) x) atTop
    (𝓝 (logDeriv (fun t ↦ Complex.sin (↑π * t) / (↑π * t)) x))
Module: Mathlib.Tactic.NormNum.Prime

Goal state before:
pp: n k : ℕ
h1 : MinFacHelper n k
h2 : 0 = n % k
⊢ IsNat n.minFac k

Tactic:
by
    rw [eq_comm, ← Nat.dvd_iff_mod_eq_zero] at h2
    exact ⟨le_antisymm (minFac_le_of_dvd h1.1.le h2) h1.2.2⟩

Goal state after:
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: ⊢ φ * 1 < φ * φ

Tactic:
simp [← sq, zero_lt_one]

Goal state after:
Module: Mathlib.NumberTheory.Real.GoldenRatio

Goal state before:
pp: ⊢ (1 + 3) / 2 = 2

Tactic:
by norm_num

Goal state after:
Module: Mathlib.Analysis.Subadditive

Goal state before:
pp: u : ℕ → ℝ
h : Subadditive u
k n r : ℕ
⊢ u (k * n + r) ≤ ↑k * u n + u r

Tactic:
induction k with

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

Goal state before:
pp: case hg
k : ℕ
z : ℂ
hz : z ∈ ℍₒ
⊢ ContDiffWithinAt ℂ (↑k) (fun x ↦ -(1 / x)) ℍₒ z

Tactic:
simp only [one_div]
    apply ContDiffWithinAt.neg
    exact ContDiffWithinAt.inv (by fun_prop) (ne_zero ⟨z, hz⟩)

Goal state after:
Module: Mathlib.CategoryTheory.Generator.Abelian

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasLimits C
inst✝ : EnoughInjectives C
G : C
hG : IsSeparator G
this✝ : WellPowered.{v, v, u} C
this : HasProductsOfShape (Subobject (op G)) C
T : C := Injective.under (∏ᶜ fun P ↦ unop (Subobject.underlying.obj P))
⊢ ∃ G, Injective G ∧ IsCoseparator G

Tactic:
refine ⟨T, inferInstance, (Preadditive.isCoseparator_iff _).2 fun X Y f hf => ?_⟩

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasLimits C
inst✝ : EnoughInjectives C
G : C
hG : IsSeparator G
this✝ : WellPowered.{v, v, u} C
this : HasProductsOfShape (Subobject (op G)) C
T : C := Injective.under (∏ᶜ fun P ↦ unop (Subobject.underlying.obj P))
X Y : C
f : X ⟶ Y
hf : ∀ (h : Y ⟶ T), f ≫ h = 0
⊢ f = 0
Module: Mathlib.CategoryTheory.Abelian.Yoneda

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
G : C
inst✝¹ : Projective G
hG : IsSeparator G
X : C
p : G ⟶ X
inst✝ : Epi p
Y : C
cm : ShortComplex C := { X₁ := kernel p, X₂ := G, X₃ := X, f := kernel.ι p, g := p, zero := ⋯ }
exact : cm.Exact
⊢ Epi (AddCommGrpCat.ofHom (preadditiveCoyonedaObj G).mapAddHom)

Tactic:
have mono : Mono cm.op.f := by dsimp [cm]; infer_instance

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
G : C
inst✝¹ : Projective G
hG : IsSeparator G
X : C
p : G ⟶ X
inst✝ : Epi p
Y : C
cm : ShortComplex C := { X₁ := kernel p, X₂ := G, X₃ := X, f := kernel.ι p, g := p, zero := ⋯ }
exact : cm.Exact
mono : Mono cm.op.f
⊢ Epi (AddCommGrpCat.ofHom (preadditiveCoyonedaObj G).mapAddHom)
Module: Mathlib.Analysis.SumIntegralComparisons

Goal state before:
pp: f : ℝ → ℝ
anti : AntitoneOn f (Ici 0)
integrable : IntegrableOn f (Ioi 0) volume
nonneg : ∀ t ∈ Ioi 0, 0 ≤ f t
⊢ ∑' (n : ℕ), f ↑n ≤ f 0 + ∫ (x : ℝ) in Ioi 0, f x

Tactic:
grind [(anti.summable_of_integrableOn_Ioi_zero integrable nonneg).tsum_eq_zero_add,
    anti.tsum_add_one_le_integral integrable nonneg]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type v
inst✝² : SmallCategory D
F : D ⥤ Cᵒᵖ
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
⊢ PreservesFiniteLimits (preadditiveCoyonedaObj (generator F))

Tactic:
apply preservesFiniteLimits_of_preservesFiniteLimitsOfSize

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
D : Type v
inst✝² : SmallCategory D
F : D ⥤ Cᵒᵖ
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
⊢ ∀ (J : Type ?u.34) {𝒥 : SmallCategory J} (x : FinCategory J),
    PreservesLimitsOfShape J (preadditiveCoyonedaObj (generator F))
Module: Mathlib.CategoryTheory.Limits.Indization.FilteredColimits

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
I : Type v
inst✝⁴ : SmallCategory I
F : I ⥤ Cᵒᵖ ⥤ Type v
J : Type v
inst✝³ : SmallCategory J
inst✝² : FinCategory J
G : J ⥤ CostructuredArrow yoneda (colimit F)
K : Type v
inst✝¹ : SmallCategory K
H : K ⥤ Over (colimit F)
inst✝ : IsFiltered K
c : Cocone H
hc : IsColimit c
T : Over (colimit F)
hT : c.pt ≅ T
h : Nonempty (limit ((G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op) ⋙ yoneda.obj T))
⊢ ∃ k, Nonempty (limit ((G.op ⋙ (CostructuredArrow.toOver yoneda (colimit F)).op) ⋙ yoneda.obj (H.obj k)))

Tactic:
by
  refine exists_nonempty_limit_obj_of_colimit F G H ?_
  suffices T ≅ colimit H from Nonempty.map (lim.map (whiskerLeft 𝒢 (yoneda.map this.hom))) h
  refine hT.symm ≪≫ IsColimit.coconePointUniqueUpToIso hc (colimit.isColimit _)

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)
⊢ Nonempty (IsColimit (coconePointwiseProduct fun i ↦ colimit.cocone (F i)))

Tactic:
obtain ⟨_, h⟩ := H J F

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)
w✝ : HasColimit (pointwiseProduct F)
h : IsIso (colimitPointwiseProductToProductColimit F)
⊢ Nonempty (IsColimit (coconePointwiseProduct fun i ↦ colimit.cocone (F i)))
Module: Mathlib.CategoryTheory.Abelian.Injective.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
J : C
hJ : Injective J
⊢ (preadditiveYonedaObj J).PreservesHomology

Tactic:
let := (injective_iff_preservesEpimorphisms_preadditive_yoneda_obj' J).mp hJ
  apply Functor.preservesHomology_of_preservesEpis_and_kernels

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Extend

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : Preadditive C
X : C
R : InjectiveResolution X
⊢ R.cochainComplex.IsStrictlyGE 0

Tactic:
by
  dsimp [cochainComplex]
  infer_instance

Goal state after:
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
M : ModuleCat (End G)ᵐᵒᵖ
g : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ A)
hg : Mono g
f : M ⟶ ModuleCat.of (End G)ᵐᵒᵖ (G ⟶ B)
F : Finset (Discrete ↑M)
⊢ pullback.snd ((finiteSubcoproductsCocone fun x ↦ G).ι.app F) (kernel.ι (d g)) ≫ kernel.ι (d g) ≫ d f = 0

Tactic:
classical
  rw [finiteSubcoproductsCocone_ι_app_eq_sum, ← pullback.condition_assoc]
  refine (Preadditive.isSeparator_iff G).1 hG _ (fun h => ?_)
  rw [Preadditive.comp_sum_assoc, Preadditive.comp_sum_assoc, Preadditive.sum_comp]
  simp only [Category.assoc, ι_d]
  let r (x : F) : (End G)ᵐᵒᵖ := MulOpposite.op (h ≫ pullback.fst _ _ ≫ Sigma.π _ x)
  suffices ∑ x ∈ F.attach, r x • f.hom x.1.as = 0 by simpa [End.smul_left, r] using this
  simp only [← map_smul, ← map_sum]
  suffices ∑ x ∈ F.attach, r x • x.1.as = 0 by simp [this]
  simp only [← g.hom.map_eq_zero_iff ((ModuleCat.mono_iff_injective _).1 hg), map_sum, map_smul]
  simp only [← ι_d g, End.smul_left, MulOpposite.unop_op, Category.assoc, r]
  simp [← Preadditive.comp_sum, ← Preadditive.sum_comp', pullback.condition_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Extend

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : Preadditive C
X : C
R : ProjectiveResolution X
⊢ R.cochainComplex.IsStrictlyLE 0

Tactic:
by
  dsimp [cochainComplex]
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Pseudoelements

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P : C
a : Over P
⊢ Quot.mk (PseudoEqual P) a = 0 ↔ a.hom = 0

Tactic:
← pseudoZero_aux P a

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P : C
a : Over P
⊢ Quot.mk (PseudoEqual P) a = 0 ↔ a ≈ Over.mk 0
Module: Mathlib.GroupTheory.SemidirectProduct

Goal state before:
pp: N : Type u_1
G : Type u_2
inst✝¹ : Group N
inst✝ : Group G
φ : G →* MulAut N
g : G
n : N
⊢ inl ((φ g)⁻¹ n) = inr g⁻¹ * inl n * inr g

Tactic:
← map_inv,

Goal state after:
N : Type u_1
G : Type u_2
inst✝¹ : Group N
inst✝ : Group G
φ : G →* MulAut N
g : G
n : N
⊢ inl ((φ g⁻¹) n) = inr g⁻¹ * inl n * inr g
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: case refine_1
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Abelian C
D : Type u'
inst✝⁶ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝⁵ : P.IsSerreClass
E : Type u''
inst✝⁴ : Category.{v'', u''} E
inst✝³ : Abelian E
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
F : C ⥤ₑ E
⊢ (whiskeringLeft L P E).essImage F → P.isoModSerre.IsInvertedBy F.obj

pp: case refine_2
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Abelian C
D : Type u'
inst✝⁶ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝⁵ : P.IsSerreClass
E : Type u''
inst✝⁴ : Category.{v'', u''} E
inst✝³ : Abelian E
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
F : C ⥤ₑ E
hF : P.isoModSerre.IsInvertedBy F.obj
⊢ (whiskeringLeft L P E).essImage F

Tactic:
· rintro ⟨G, ⟨e⟩⟩
    rw [← MorphismProperty.IsInvertedBy.iff_of_iso _
      (show L ⋙ G.obj ≅ F.obj from (ObjectProperty.ι _).mapIso e)]
    exact MorphismProperty.IsInvertedBy.of_comp _ _ (Localization.inverts L _) _

Goal state after:
case refine_2
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Abelian C
D : Type u'
inst✝⁶ : Category.{v', u'} D
L : C ⥤ D
P : ObjectProperty C
inst✝⁵ : P.IsSerreClass
E : Type u''
inst✝⁴ : Category.{v'', u''} E
inst✝³ : Abelian E
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
F : C ⥤ₑ E
hF : P.isoModSerre.IsInvertedBy F.obj
⊢ (whiskeringLeft L P E).essImage F
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Left

Goal state before:
pp: case refine_3
A : Type u₁
B : Type u₂
C : Type u₃
inst✝² : Category.{v₁, u₁} A
inst✝¹ : Category.{v₂, u₂} B
inst✝ : Category.{v₃, u₃} C
U : B ⥤ C
F : C ⥤ B
R : A ⥤ B
F' : C ⥤ A
adj₁ : F ⊣ U
adj₂ : F' ⊣ R ⋙ U
h : (X : B) → RegularEpi (adj₁.counit.app X)
X : B
s : Cofork (F.map (U.map (adj₁.counit.app X))) (adj₁.counit.app ((U ⋙ F).obj X))
this : ∀ (Y : B), Epi (adj₁.counit.app Y)
⊢ ∀ {m : (Cofork.ofπ (adj₁.counit.app X) ⋯).pt ⟶ s.pt},
    (Cofork.ofπ (adj₁.counit.app X) ⋯).π ≫ m = s.π → m = ↑((h X).desc' s.π ⋯)

Tactic:
· intro m hm
      rw [← cancel_epi (adj₁.counit.app X)]
      apply hm.trans ((h _).desc' s.π _).2.symm

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Evaluation

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : ∀ (a b : C), HasCoproductsOfShape (a ⟶ b) D
c : C
d : D
F : C ⥤ D
⊢ Function.LeftInverse (fun f ↦ { app := fun x ↦ Sigma.desc fun h ↦ f ≫ F.map h, naturality := ⋯ }) fun f ↦
    Sigma.ι (fun x ↦ d) (𝟙 c) ≫ f.app c

Tactic:
by
            intro f
            ext x
            dsimp
            ext g
            simp only [colimit.ι_desc, Cofan.mk_ι_app, Category.assoc, ← f.naturality,
              evaluationLeftAdjoint_obj_map, colimit.ι_desc_assoc,
              Discrete.functor_obj, Cofan.mk_pt, Category.id_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Lifting.Right

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
F : B ⥤ A
inst✝² : ComonadicLeftAdjoint F
L : C ⥤ B
inst✝¹ : HasCoreflexiveEqualizers C
inst✝ : (L ⋙ F).IsLeftAdjoint
L' : C ⥤ (comonadicAdjunction F).toComonad.Coalgebra := L ⋙ Comonad.comparison (comonadicAdjunction F)
this : (L' ⋙ (comonadicAdjunction F).toComonad.forget).IsLeftAdjoint :=
  Adjunction.isLeftAdjoint
    ((Adjunction.ofIsLeftAdjoint (L ⋙ F)).ofNatIsoLeft
      (L.isoWhiskerLeft (Comonad.comparisonForget (comonadicAdjunction F)).symm))
⊢ (X : (comonadicAdjunction F).toComonad.Coalgebra) → RegularMono ((comonadicAdjunction F).toComonad.adj.unit.app X)

Tactic:
by
    intro X
    simp only [Comonad.adj_unit]
    exact ⟨_, _, _, _, Comonad.beckCoalgebraEqualizer X⟩

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Triple

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
inst✝¹ : F.Full
inst✝ : F.Faithful
X : C
⊢ Mono (t.leftToRight.app X) ↔ Mono (t.leftToRight.app X ≫ H.map (t.adj₁.unit.app X))

Tactic:
mono_comp_iff_of_mono

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
H : C ⥤ D
t : Triple F G H
inst✝¹ : F.Full
inst✝ : F.Faithful
X : C
⊢ Mono (t.leftToRight.app X) ↔ Mono (t.leftToRight.app X)