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

Goal state before:
pp: case inr
ε : ℝ
E : Type u_2
inst✝⁶ : MeasurableSpace E
inst✝⁵ : PseudoEMetricSpace E
inst✝⁴ : BorelSpace E
inst✝³ : CompleteSpace E
inst✝² : SecondCountableTopology E
P P' : Measure E
inst✝¹ : IsFiniteMeasure P
inst✝ : IsFiniteMeasure P'
f : E →ᵇ ℝ
A : Subalgebra ℝ (E →ᵇ ℝ)
hA : (Subalgebra.map (toContinuousMapₐ ℝ) A).SeparatesPoints
heq : ∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P'
hε : 0 < ε
const : ℝ := max (P.real Set.univ) (P'.real Set.univ)
hP'0 : ¬P' = 0
⊢ 0 < const

Tactic:
· exact lt_max_of_lt_right
        (toReal_pos ((Measure.measure_univ_ne_zero).mpr hP'0) (by finiteness))

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

Goal state before:
pp: case neg.hb
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : 2 * r ≤ ‖↑l‖
h✝ : ¬↑l = l₀
this✝ : s ≠ ↑l
this : l ≠ 0
⊢ 0 < ‖s - ↑l‖ ^ 3

pp: case neg.hd
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : 2 * r ≤ ‖↑l‖
h✝ : ¬↑l = l₀
this✝ : s ≠ ↑l
this : l ≠ 0
⊢ 0 < ‖l‖ ^ 3

Tactic:
· exact pow_pos (by simpa [sub_eq_zero]) _

Goal state after:
case neg.hd
L : PeriodPair
l₀ : ℂ
r : ℝ
hr : r > 0
s : ℂ
hs : ‖s‖ < r
l : ↥L.lattice
h : 2 * r ≤ ‖↑l‖
h✝ : ¬↑l = l₀
this✝ : s ≠ ↑l
this : l ≠ 0
⊢ 0 < ‖l‖ ^ 3
Module: Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
⊢ ∃ f, MeasurableEmbedding f

Tactic:
by
  obtain ⟨s, hs, ⟨e⟩⟩ := exists_subset_real_measurableEquiv α
  exact ⟨(↑) ∘ e, (MeasurableEmbedding.subtype_coe hs).comp e.measurableEmbedding⟩

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

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
hl₀ : l₀ ∈ L.lattice
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
⊢ Set.EqOn (fun x ↦ ℘[L - l₀] (x + ↑l)) (fun x ↦ ℘[L - l₀ - ↑l] x + (1 / l₀ ^ 2 - 1 / (l₀ - ↑l) ^ 2))
    (↑L.lattice \ {l₀ - ↑l})ᶜ

Tactic:
apply IsOpen.eqOn_of_deriv_eq (𝕜 := ℂ) L.isOpen_compl_lattice_sdiff
    ?_ ?_ ?_ ?_ (x := -(l / 2)) ?_ ?_
  · refine (Set.Countable.isConnected_compl_of_one_lt_rank (by simp) ?_).2
    exact .mono sdiff_le (countable_of_Lindelof_of_discrete (X := L.lattice))
  · refine (L.differentiableOn_weierstrassPExcept l₀).comp (f := (· + l.1)) (by fun_prop) ?_
    rintro x h₁ ⟨h₂ : x + l ∈ _, h₃ : x + l ≠ l₀⟩
    exact h₁ ⟨by simpa using sub_mem h₂ l.2, by rintro rfl; simp at h₃⟩
  · refine .add (L.differentiableOn_weierstrassPExcept _) (by simp)
  · intro x hx
    simp only [deriv_add_const', deriv_comp_add_const]
    rw [L.eqOn_deriv_weierstrassPExcept_derivWeierstrassPExcept,
      L.eqOn_deriv_weierstrassPExcept_derivWeierstrassPExcept, L.derivWeierstrassPExcept_add_coe]
    · simpa using hx
    · simp only [Set.mem_compl_iff, Set.mem_sdiff, SetLike.mem_coe, Set.mem_singleton_iff, not_and,
        Decidable.not_not, eq_sub_iff_add_eq] at hx ⊢
      exact fun H ↦ hx (by simpa using sub_mem H l.2)
  · simp [hl]
  · rw [L.weierstrassPExcept_neg, L.weierstrassPExcept_def ⟨l₀, hl₀⟩,
      L.weierstrassPExcept_def ⟨_, neg_mem (sub_mem hl₀ l.2)⟩, add_assoc]
    congr 2 <;> ring

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

Goal state before:
pp: case pos
L : PeriodPair
z : ℂ
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
hl0 : l ≠ 0
hz : z ∈ L.lattice
this : ℘[L - z + ↑l] (z + ↑l) = ℘[L - z + ↑l - ↑l] z + (1 / (z + ↑l) ^ 2 - 1 / (z + ↑l - ↑l) ^ 2)
⊢ ℘[L] (z + ↑l) = ℘[L] z

Tactic:
← L.weierstrassPExcept_add ⟨z + l, add_mem hz l.2⟩,

Goal state after:
case pos
L : PeriodPair
z : ℂ
l : ↥L.lattice
hl : ↑l / 2 ∉ L.lattice
hl0 : l ≠ 0
hz : z ∈ L.lattice
this : ℘[L - z + ↑l] (z + ↑l) = ℘[L - z + ↑l - ↑l] z + (1 / (z + ↑l) ^ 2 - 1 / (z + ↑l - ↑l) ^ 2)
⊢ ℘[L - ↑⟨z + ↑l, ⋯⟩] (z + ↑l) + (1 / (z + ↑l - ↑⟨z + ↑l, ⋯⟩) ^ 2 - 1 / ↑⟨z + ↑l, ⋯⟩ ^ 2) = ℘[L] z
Module: Mathlib.Analysis.SpecialFunctions.Stirling

Goal state before:
pp: ⊢ ∃ a, 0 < a ∧ ∀ (n : ℕ), a ≤ stirlingSeq (n + 1)

Tactic:
let c := 1 - 12⁻¹ - log 2 / 2
  have h := log_stirlingSeq_bounded_by_constant
  refine ⟨exp c, exp_pos _, fun n => ?_⟩
  rw [← le_log_iff_exp_le (stirlingSeq'_pos n)]
  exact h n

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

Goal state before:
pp: n : ℕ
P : ℝ[X]
hP : P.degree ≤ ↑n
⊢ P.degree < ↑(n + 1)

Tactic:
hP

Goal state after:
n : ℕ
P : ℝ[X]
hP : P.degree ≤ ↑n
⊢ ↑n < ↑(n + 1)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal

Goal state before:
pp: n k : ℕ
hk : k ≤ n
x : ℝ
P : ℝ[X]
hP : P.degree ≤ ↑n
⊢ P.degree < ↑(n + 1)

Tactic:
hP

Goal state after:
n k : ℕ
hk : k ≤ n
x : ℝ
P : ℝ[X]
hP : P.degree ≤ ↑n
⊢ ↑n < ↑(n + 1)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema

Goal state before:
pp: k n : ℕ
hn : n ≠ 0
⊢ cos (↑↑n * (↑k * π / ↑n)) = ↑↑(↑k).negOnePow

Tactic:
Int.cast_negOnePow

Goal state after:
k n : ℕ
hn : n ≠ 0
⊢ cos (↑↑n * (↑k * π / ↑n)) = (-1) ^ ↑k
Module: Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass

Goal state before:
pp: L : PeriodPair
l₀ : ℂ
h : l₀ ∈ L.lattice
z : ℂ
hz : z ≠ l₀
this : (z - l₀) ^ 2 ≠ 0
⊢ ℘[L] z = (z - l₀) ^ (-2) • ((z - l₀) ^ 2 * ℘[L - l₀] z + 1 - (z - l₀) ^ 2 / l₀ ^ 2)

Tactic:
simp [← L.ite_eq_one_sub_sq_mul_weierstrassP l₀ h,
        if_neg hz, inv_mul_cancel_left₀ this, zpow_ofNat]

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

Goal state before:
pp: case hab
Z : Set ℂ
hZ : IsCompact Z
s : ℝ
hf : ContinuousOn (fun x ↦ ‖x‖ ^ 2) Z
hs : ∀ a ∈ Z, ‖a‖ ^ 2 ≤ s
n : ℕ
x : ℂ
hx : x ∈ Z
⊢ ‖x‖ ^ 2 ≤ |s|

Tactic:
apply le_trans (hs x hx) (le_abs_self s)

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

Goal state before:
pp: case ofNat
n : ℕ
⊢ ↑(Nat.fib n + Nat.fib (n + 1)) = ↑(Nat.fib n) + ↑(Nat.fib (n + 1))

Tactic:
Nat.cast_add

Goal state after:
case ofNat
n : ℕ
⊢ ↑(Nat.fib n) + ↑(Nat.fib (n + 1)) = ↑(Nat.fib n) + ↑(Nat.fib (n + 1))
Module: Mathlib.Analysis.SpecificLimits.Fibonacci

Goal state before:
pp: h₁ : ∀ (n : ℕ), ↑(fib (n + 1)) / ↑(fib n) = (φ - ψ * (ψ / φ) ^ n) / (1 - (ψ / φ) ^ n)
⊢ |ψ| < |φ|

Tactic:
abs_of_pos goldenRatio_pos,

Goal state after:
h₁ : ∀ (n : ℕ), ↑(fib (n + 1)) / ↑(fib n) = (φ - ψ * (ψ / φ) ^ n) / (1 - (ψ / φ) ^ n)
⊢ |ψ| < φ
Module: Mathlib.Tactic.NormNum.Prime

Goal state before:
pp: case inr
n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
p : ℕ
hp : 2 ≤ p
hpn : p ∣ n
h : 2 < p
⊢ 3 ≤ p

Tactic:
· exact h

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

Goal state before:
pp: α : Type u_1
inst✝ : CommSemiring α
⊢ fibRec.IsSolution fun x ↦ ↑(Nat.fib x)

Tactic:
fibRec

Goal state after:
α : Type u_1
inst✝ : CommSemiring α
⊢ { order := 2, coeffs := ![1, 1] }.IsSolution fun x ↦ ↑(Nat.fib x)
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)
⊢ AntitoneOn (fun x ↦ g (x - 1)) (Icc ↑a ↑b)

Tactic:
intro _

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✝ : ℝ
⊢ 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.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
⊢ ∃ G, Injective G ∧ IsCoseparator G

Tactic:
have : WellPowered.{v} C := wellPowered_of_isDetector G hG.isDetector

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
⊢ ∃ G, Injective G ∧ IsCoseparator G
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)
⊢ MonotoneOn (fun x ↦ g (x - 1)) (Icc ↑a ↑b)

Tactic:
intro _

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✝ : ℝ
⊢ 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.SpecificLimits.FloorPow

Goal state before:
pp: N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
this : c ^ 3 = c ^ 2 * c
⊢ c ^ 2 * c * (c ^ 2)⁻¹ ≤ c ^ 2

Tactic:
rw [mul_assoc, mul_comm c, ← mul_assoc, mul_inv_cancel₀ (sq_pos_of_pos cpos).ne', one_mul]

Goal state after:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < c⁻¹ ^ 2
this : c ^ 3 = c ^ 2 * c
⊢ c ≤ c ^ 2
Module: Mathlib.CategoryTheory.Limits.Indization.ParallelPair

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
A B : Cᵒᵖ ⥤ Type v₁
f g : A ⟶ B
P₁ : IndObjectPresentation A
P₂ : IndObjectPresentation B
⊢ f = (isColimit₁ f g P₁ P₂).map { pt := B, ι := ι₂ f g P₁ P₂ } (whiskerRight (ϕ f g P₁ P₂) yoneda)

Tactic:
by
  refine (isColimit₁ f g P₁ P₂).hom_ext (fun i => ?_)
  rw [IsColimit.ι_map]
  simpa using! i.hom.1.w.symm

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Indization.Category

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ RepresentablyCoflat Ind.yoneda

Tactic:
by
  refine ⟨fun X => ?_⟩
  suffices IsFiltered (CostructuredArrow yoneda ((Ind.inclusion C).obj X)) from
    IsFiltered.of_equivalence
      ((CostructuredArrow.post Ind.yoneda (Ind.inclusion C) X).asEquivalence.trans
      (CostructuredArrow.mapNatIso Ind.yonedaCompInclusion)).symm
  exact ((isIndObject_iff _).1 (Ind.isIndObject_inclusion_obj X)).1

Goal state after:
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 (colimit.ι (pointwiseProduct F) k ≫ colimitPointwiseProductToProductColimit F ≫ Pi.π (fun s ↦ colimit (F s)) s))
      yk =
    (hom (Pi.π ((Functor.pi F).obj k) s ≫ colimit.ι (F s) (k s))) yk
⊢ ∃ i' hi',
    (hom ((F s).map hi')) ((hom (Pi.π (fun s ↦ (F s).obj (k s)) s)) yk) =
      (hom ((F s).map hi')) ((hom (Pi.π (fun s ↦ (F s).obj (k s)) s)) yk')

Tactic:
have hy₂ := congr_hom (ι_colimitPointwiseProductToProductColimit_π F k s) yk'

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 (colimit.ι (pointwiseProduct F) k ≫ colimitPointwiseProductToProductColimit F ≫ Pi.π (fun s ↦ colimit (F s)) s))
      yk =
    (hom (Pi.π ((Functor.pi F).obj k) s ≫ colimit.ι (F s) (k s))) yk
hy₂ :
  (hom (colimit.ι (pointwiseProduct F) k ≫ colimitPointwiseProductToProductColimit F ≫ Pi.π (fun s ↦ colimit (F s)) s))
      yk' =
    (hom (Pi.π ((Functor.pi F).obj k) s ≫ colimit.ι (F s) (k s))) yk'
⊢ ∃ i' hi',
    (hom ((F s).map hi')) ((hom (Pi.π (fun s ↦ (F s).obj (k s)) s)) yk) =
      (hom ((F s).map hi')) ((hom (Pi.π (fun s ↦ (F s).obj (k s)) s)) yk')
Module: Mathlib.CategoryTheory.Preadditive.Injective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
I : InjectiveResolution Z
n : ℕ
⊢ (ComplexShape.up ℕ).next (n + 1) = n + 2

Tactic:
by simp only [CochainComplex.next]; rfl

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:
dsimp only [liftToFinsetObj_obj, Discrete.functor_obj_eq_as, finiteSubcoproductsCocone_pt,
    Functor.const_obj_obj]

Goal state after:
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
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]; 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
B : C
hB : Injective B
M : Ideal (End G)ᵐᵒᵖ
g : ↥M →ₗ[(End G)ᵐᵒᵖ] G ⟶ B
⊢ ∃ g', ∀ (x : (End G)ᵐᵒᵖ) (mem : x ∈ M), g' x = g ⟨x, mem⟩

Tactic:
have h := exists_d_comp_eq_d hG B (ModuleCat.ofHom
      ⟨⟨fun i => i.1.unop, by cat_disch⟩, by cat_disch⟩) ?_ (ModuleCat.ofHom g)

Goal state after:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator G
B : C
hB : Injective B
M : Ideal (End G)ᵐᵒᵖ
g : ↥M →ₗ[(End G)ᵐᵒᵖ] G ⟶ B
h :
  ∃ l,
    d (ModuleCat.ofHom { toFun := fun i ↦ MulOpposite.unop ↑i, map_add' := ⋯, map_smul' := ⋯ }) ≫ l =
      d (ModuleCat.ofHom g)
⊢ ∃ g', ∀ (x : (End G)ᵐᵒᵖ) (mem : x ∈ M), g' x = g ⟨x, mem⟩

case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : IsGrothendieckAbelian.{v, v, u} C
G : C
hG : IsSeparator G
B : C
hB : Injective B
M : Ideal (End G)ᵐᵒᵖ
g : ↥M →ₗ[(End G)ᵐᵒᵖ] G ⟶ B
⊢ Mono (ModuleCat.ofHom { toFun := fun i ↦ MulOpposite.unop ↑i, map_add' := ⋯, map_smul' := ⋯ })
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
inst✝ : Epi f
qbar : Pseudoelement Q
q : Over Q
⊢ 𝟙 (pullback f q.hom) ≫ ((fun g ↦ app f g) (Over.mk (pullback.fst f q.hom))).hom = pullback.snd f q.hom ≫ q.hom

Tactic:
by
          rw [Category.id_comp, ← pullback.condition, app_hom, Over.coe_hom]

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
h : Function.Surjective (pseudoApply f)
pbar : Pseudoelement P
hpbar : pseudoApply f pbar = Quot.mk (PseudoEqual Q) (Over.mk (𝟙 Q))
p : Over P
hp : ⟦p⟧ = pbar
this : ⟦Over.mk (p.hom ≫ f)⟧ = ⟦Over.mk (𝟙 Q)⟧
R : C
x : R ⟶ (Over.mk (p.hom ≫ f)).left
y : R ⟶ (Over.mk (𝟙 Q)).left
w✝ : Epi x
ey : Epi y
comm : x ≫ (Over.mk (p.hom ≫ f)).hom = y ≫ (Over.mk (𝟙 Q)).hom
⊢ Epi f

Tactic:
apply @epi_of_epi_fac _ _ _ _ _ (x ≫ p.hom) f y ey

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
h : Function.Surjective (pseudoApply f)
pbar : Pseudoelement P
hpbar : pseudoApply f pbar = Quot.mk (PseudoEqual Q) (Over.mk (𝟙 Q))
p : Over P
hp : ⟦p⟧ = pbar
this : ⟦Over.mk (p.hom ≫ f)⟧ = ⟦Over.mk (𝟙 Q)⟧
R : C
x : R ⟶ (Over.mk (p.hom ≫ f)).left
y : R ⟶ (Over.mk (𝟙 Q)).left
w✝ : Epi x
ey : Epi y
comm : x ≫ (Over.mk (p.hom ≫ f)).hom = y ≫ (Over.mk (𝟙 Q)).hom
⊢ (x ≫ p.hom) ≫ f = y
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P : ObjectProperty C
inst✝ : P.IsSerreClass
X Y : C
f : X ⟶ Y
hf : P (Abelian.image f)
⊢ ∃ X' s, ∃ (_ : P.epiModSerre s), s ≫ f = 0

Tactic:
· exact ⟨_, kernel.ι f, P.prop_of_iso (Abelian.coimageIsoImage f).symm hf, by simp⟩

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'
⊢ ofObjectProperty P Q ≤ ofObjectProperty P' Q

Tactic:
intro _

Goal state after:
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
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'
⊢ ofObjectProperty P Q ≤ ofObjectProperty P Q'

Tactic:
intro _

Goal state after:
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
Module: Mathlib.CategoryTheory.ObjectProperty.Kernels

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
P : ObjectProperty C
inst✝ : P.IsClosedUnderSubobjects
⊢ (MorphismProperty.ofObjectProperty P P).kernels ≤ P

Tactic:
intro _

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
P : ObjectProperty C
inst✝ : P.IsClosedUnderSubobjects
i✝ : C
⊢ (MorphismProperty.ofObjectProperty P P).kernels i✝ ≤ P i✝
Module: Mathlib.CategoryTheory.ObjectProperty.Kernels

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
P : ObjectProperty C
inst✝ : P.IsClosedUnderQuotients
⊢ (MorphismProperty.ofObjectProperty P P).cokernels ≤ P

Tactic:
intro _

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
P : ObjectProperty C
inst✝ : P.IsClosedUnderQuotients
i✝ : C
⊢ (MorphismProperty.ofObjectProperty P P).cokernels i✝ ≤ P i✝
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
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
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : D
f : X ⟶ Y
this✝ : L.PreservesMonomorphisms
this : L.mapArrow.EssSurj
⊢ (∃ X' Y' f', ∃ (_ : Mono f'), Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk f)) → Mono f

Tactic:
rintro ⟨X', Y', f', _, ⟨e⟩⟩

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
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : D
f : X ⟶ Y
this✝ : L.PreservesMonomorphisms
this : L.mapArrow.EssSurj
X' Y' : C
f' : X' ⟶ Y'
w✝ : Mono f'
e : Arrow.mk (L.map f') ≅ Arrow.mk f
⊢ Mono f
Module: Mathlib.CategoryTheory.Abelian.SerreClass.Localization

Goal state before:
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
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : D
f : X ⟶ Y
this✝ : L.PreservesEpimorphisms
this : L.mapArrow.EssSurj
⊢ (∃ X' Y' f', ∃ (_ : Epi f'), Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk f)) → Epi f

Tactic:
rintro ⟨X', Y', f', _, ⟨e⟩⟩

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
inst✝² : L.IsLocalization P.isoModSerre
inst✝¹ : Preadditive D
inst✝ : L.Additive
X Y : D
f : X ⟶ Y
this✝ : L.PreservesEpimorphisms
this : L.mapArrow.EssSurj
X' Y' : C
f' : X' ⟶ Y'
w✝ : Epi f'
e : Arrow.mk (L.map f') ≅ Arrow.mk f
⊢ Epi f
Module: Mathlib.CategoryTheory.Linear.FunctorCategory

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{v_1, u_2} C
inst✝² : Category.{v_2, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F G : C ⥤ D
r : R
α : F ⟶ G
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ r • F.map f✝ ≫ α.app Y✝ = (r • α.app X✝) ≫ G.map f✝

Tactic:
smul_comp,

Goal state after:
R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{v_1, u_2} C
inst✝² : Category.{v_2, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F G : C ⥤ D
r : R
α : F ⟶ G
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ r • F.map f✝ ≫ α.app Y✝ = r • α.app X✝ ≫ G.map f✝
Module: Mathlib.CategoryTheory.Linear.FunctorCategory

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{v_1, u_2} C
inst✝² : Category.{v_2, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F G : C ⥤ D
r✝ s✝ : R
x✝¹ : F ⟶ G
x✝ : C
⊢ ((r✝ + s✝) • x✝¹).app x✝ = (r✝ • x✝¹ + s✝ • x✝¹).app x✝

Tactic:
apply add_smul

Goal state after:
Module: Mathlib.CategoryTheory.Linear.FunctorCategory

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
C : Type u_2
D : Type u_3
inst✝³ : Category.{v_1, u_2} C
inst✝² : Category.{v_2, u_3} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
⊢ ∀ (X Y Z : C ⥤ D) (f : X ⟶ Y) (r : R) (g : Y ⟶ Z), f ≫ (r • g) = r • f ≫ g

Tactic:
by
    intros
    ext
    apply comp_smul

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

Goal state before:
pp: V : Type u_1
inst✝³ : Category.{v_1, u_1} V
G : Type u_2
inst✝² : Monoid G
C : Type u_3
inst✝¹ : Category.{v_2, u_3} C
F : C ⥤ SingleObj G ⥤ V
J : Type u_4
inst✝ : Category.{v_3, u_4} J
K : J ⥤ C
h : PreservesLimit K (F ⋙ (evaluation (SingleObj G) V).obj (SingleObj.star G))
⊢ ∀ (k : SingleObj G), PreservesLimit K (F ⋙ (evaluation (SingleObj G) V).obj k)

Tactic:
intro _

Goal state after:
V : Type u_1
inst✝³ : Category.{v_1, u_1} V
G : Type u_2
inst✝² : Monoid G
C : Type u_3
inst✝¹ : Category.{v_2, u_3} C
F : C ⥤ SingleObj G ⥤ V
J : Type u_4
inst✝ : Category.{v_3, u_4} J
K : J ⥤ C
h : PreservesLimit K (F ⋙ (evaluation (SingleObj G) V).obj (SingleObj.star G))
k✝ : SingleObj G
⊢ PreservesLimit K (F ⋙ (evaluation (SingleObj G) V).obj k✝)
Module: Mathlib.CategoryTheory.Action.Limits

Goal state before:
pp: V : Type u_1
inst✝³ : Category.{v_1, u_1} V
G : Type u_2
inst✝² : Monoid G
C : Type u_3
inst✝¹ : Category.{v_2, u_3} C
F : C ⥤ SingleObj G ⥤ V
J : Type u_4
inst✝ : Category.{v_3, u_4} J
K : J ⥤ C
h : PreservesColimit K (F ⋙ (evaluation (SingleObj G) V).obj (SingleObj.star G))
⊢ ∀ (k : SingleObj G), PreservesColimit K (F ⋙ (evaluation (SingleObj G) V).obj k)

Tactic:
intro _

Goal state after:
V : Type u_1
inst✝³ : Category.{v_1, u_1} V
G : Type u_2
inst✝² : Monoid G
C : Type u_3
inst✝¹ : Category.{v_2, u_3} C
F : C ⥤ SingleObj G ⥤ V
J : Type u_4
inst✝ : Category.{v_3, u_4} J
K : J ⥤ C
h : PreservesColimit K (F ⋙ (evaluation (SingleObj G) V).obj (SingleObj.star G))
k✝ : SingleObj G
⊢ PreservesColimit K (F ⋙ (evaluation (SingleObj G) V).obj k✝)