mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
wi : i ≫ S₁.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₁.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₁.f ⋯)
hf' : f' ≫ i = S₁.f
hf'' : f' = φ.τ₁ ≫ h.f'
wπ : f' ≫ h.π = 0
Z'✝ : C
x : h.K ⟶ Z'✝
hx✝ : f' ≫ x = 0
b : h.H ⟶ Z'✝
hx : h.π ≫ b = x
⊢ h.π ≫ b = x

Tactic:
hx

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
wi : i ≫ S₁.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₁.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₁.f ⋯)
hf' : f' ≫ i = S₁.f
hf'' : f' = φ.τ₁ ≫ h.f'
wπ : f' ≫ h.π = 0
Z'✝ : C
x : h.K ⟶ Z'✝
hx✝ : f' ≫ x = 0
b : h.H ⟶ Z'✝
hx : h.π ≫ b = x
⊢ x = x
Module: Mathlib.Algebra.Homology.ShortComplex.Homology

Goal state before:
pp: case refine_2
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
h₁ : IsIso (cyclesMap φ)
h₂ : Epi φ.τ₁
h : S₂.toCycles ≫ inv (cyclesMap φ) ≫ S₁.homologyπ = 0
z : (CokernelCofork.ofπ S₂.homologyπ ⋯).pt ⟶ S₁.homology
hz : S₂.homologyπ ≫ z = inv (cyclesMap φ) ≫ S₁.homologyπ
⊢ inv (cyclesMap φ) ≫ cyclesMap φ ≫ S₂.homologyπ = S₂.homologyπ ≫ 𝟙 S₂.homology

Tactic:
IsIso.inv_hom_id_assoc,

Goal state after:
case refine_2
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
h₁ : IsIso (cyclesMap φ)
h₂ : Epi φ.τ₁
h : S₂.toCycles ≫ inv (cyclesMap φ) ≫ S₁.homologyπ = 0
z : (CokernelCofork.ofπ S₂.homologyπ ⋯).pt ⟶ S₁.homology
hz : S₂.homologyπ ≫ z = inv (cyclesMap φ) ≫ S₁.homologyπ
⊢ S₂.homologyπ = S₂.homologyπ ≫ 𝟙 S₂.homology
Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ φ' : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
γ' : RightHomologyMapData φ' h₁ h₂
⊢ opcyclesMap' (φ + φ') h₁ h₂ = opcyclesMap' φ h₁ h₂ + opcyclesMap' φ' h₁ h₂

Tactic:
simp only [γ.opcyclesMap'_eq, γ'.opcyclesMap'_eq,
    (γ.add γ').opcyclesMap'_eq, RightHomologyMapData.add_φQ]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Limits

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cocone F
h₁ : IsColimit (π₁.mapCocone c)
h₂ : IsColimit (π₂.mapCocone c)
h₃ : IsColimit (π₃.mapCocone c)
s : Cocone F
j : J
eq₂ : ∀ (j : J), (c.ι.app j).τ₂ ≫ h₂.desc (π₂.mapCocone s) = (s.ι.app j).τ₂
eq₃ : ∀ (j : J), (c.ι.app j).τ₃ ≫ h₃.desc (π₃.mapCocone s) = (s.ι.app j).τ₃
eq₂₃ : ∀ (j : J), (c.ι.app j).τ₂ ≫ c.pt.g = (F.obj j).g ≫ (c.ι.app j).τ₃
eq₂₃' : ∀ (j : J), (s.ι.app j).τ₂ ≫ s.pt.g = (F.obj j).g ≫ (s.ι.app j).τ₃
⊢ (c.ι.app j).τ₂ ≫ h₂.desc (π₂.mapCocone s) ≫ s.pt.g = (c.ι.app j).τ₂ ≫ c.pt.g ≫ h₃.desc (π₃.mapCocone s)

Tactic:
rw [reassoc_of% (eq₂ j), eq₂₃', reassoc_of% eq₂₃, eq₃]

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Projective.Basic

Goal state before:
pp: case h
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.PreservesEpimorphisms
P : C
hP : Projective P
E✝ X✝ : D
f : F.obj P ⟶ X✝
g : E✝ ⟶ X✝
x✝ : Epi g
f' : P ⟶ G.obj E✝
hf' : f' ≫ G.map g = adj.unit.app P ≫ G.map f
⊢ (F.map f' ≫ adj.counit.app E✝) ≫ g = f

Tactic:
rw [Category.assoc, ← Adjunction.counit_naturality, ← Category.assoc, ← F.map_comp, hf']

Goal state after:
case h
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.PreservesEpimorphisms
P : C
hP : Projective P
E✝ X✝ : D
f : F.obj P ⟶ X✝
g : E✝ ⟶ X✝
x✝ : Epi g
f' : P ⟶ G.obj E✝
hf' : f' ≫ G.map g = adj.unit.app P ≫ G.map f
⊢ F.map (adj.unit.app P ≫ G.map f) ≫ adj.counit.app X✝ = f
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.HomologyData
this : S.HasHomology
⊢ h.left.π ≫ h.iso.hom ≫ h.right.ι = 0 → IsZero h.left.H

Tactic:
· intro eq
    simp only [IsZero.iff_id_eq_zero, ← cancel_mono h.iso.hom, id_comp, ← cancel_mono h.right.ι,
      ← cancel_epi h.left.π, eq, zero_comp, comp_zero]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.HomologyData
z : IsZero h.left.H
⊢ S.op.Exact

Tactic:
exact ⟨⟨h.op, (IsZero.of_iso z h.iso.symm).op⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
X A₁ A₂ : C
i₁ : A₁ ⟶ X
i₂ : A₂ ⟶ X
inst✝¹ : Mono i₁
inst✝ : Mono i₂
f : A₁ ⟶ A₂
fac : f ≫ i₂ = i₁
hf : ¬IsIso f
h : mk i₁ = mk i₂
⊢ f ≫ i₂ = ofMkLEMk i₁ i₂ ⋯ ≫ i₂

Tactic:
ofMkLEMk_comp,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X A₁ A₂ : C
i₁ : A₁ ⟶ X
i₂ : A₂ ⟶ X
inst✝¹ : Mono i₁
inst✝ : Mono i₂
f : A₁ ⟶ A₂
fac : f ≫ i₂ = i₁
hf : ¬IsIso f
h : mk i₁ = mk i₂
⊢ f ≫ i₂ = i₁
Module: Mathlib.CategoryTheory.Subobject.MonoOver

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasImages C
f g : Over X
k : f ⟶ g
⊢ image.lift
        { I := Limits.image g.hom, m := image.ι g.hom, m_mono := ⋯, e := Over.Hom.left k ≫ factorThruImage g.hom,
          fac := ⋯ } ≫
      ((forget X).obj (imageMonoOver g.hom)).hom =
    ((forget X).obj (imageMonoOver f.hom)).hom

Tactic:
apply image.lift_fac

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
X Y Z✝ : C
inst✝³ : HasZeroMorphisms C
f✝ : X ⟶ Y
inst✝² : HasKernel f✝
f : X ⟶ Y
inst✝¹ : HasKernel f
Z : C
h : Y ⟶ Z
inst✝ : Mono h
⊢ IsIso ((underlyingIso (kernel.ι f)).hom ≫ (kernelCompMono f h).inv ≫ (underlyingIso (kernel.ι (f ≫ h))).inv)

pp: C : Type u
inst✝⁴ : Category.{v, u} C
X Y Z✝ : C
inst✝³ : HasZeroMorphisms C
f✝ : X ⟶ Y
inst✝² : HasKernel f✝
f : X ⟶ Y
inst✝¹ : HasKernel f
Z : C
h : Y ⟶ Z
inst✝ : Mono h
⊢ (kernelCompMono f h).inv ≫ kernel.ι (f ≫ h) = kernel.ι f

Tactic:
· infer_instance

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
X Y Z✝ : C
inst✝³ : HasZeroMorphisms C
f✝ : X ⟶ Y
inst✝² : HasKernel f✝
f : X ⟶ Y
inst✝¹ : HasKernel f
Z : C
h : Y ⟶ Z
inst✝ : Mono h
⊢ (kernelCompMono f h).inv ≫ kernel.ι (f ≫ h) = kernel.ι f
Module: Mathlib.Algebra.Homology.ImageToKernel

Goal state before:
pp: V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝¹ : HasKernels V
inst✝ : HasImages V
w : f ≫ g = 0
⊢ (imageSubobjectIso f).hom ≫ imageToKernel' f g w = imageToKernel f g w ≫ (kernelSubobjectIso g).hom

Tactic:
ext
  simp [imageToKernel']

Goal state after:
Module: Mathlib.Algebra.Homology.ImageToKernel

Goal state before:
pp: V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝¹ : HasKernels V
inst✝ : HasImages V
w : f ≫ g = 0
⊢ imageToKernel' f g w ≫ (kernelSubobjectIso g).inv = (imageSubobjectIso f).inv ≫ imageToKernel f g w

Tactic:
ext
  simp [imageToKernel']

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
X Y Z : C
f✝ : X ⟶ Y
inst✝⁴ : HasImage f✝
inst✝³ : HasEqualizers C
X' : C
h : X' ⟶ X
inst✝² : Epi h
f : X ⟶ Y
inst✝¹ : HasImage f
inst✝ : HasImage (h ≫ f)
⊢ Epi ((underlyingIso (image.ι (h ≫ f))).hom ≫ image.preComp h f ≫ (underlyingIso (image.ι f)).inv)

pp: C : Type u
inst✝⁵ : Category.{v, u} C
X Y Z : C
f✝ : X ⟶ Y
inst✝⁴ : HasImage f✝
inst✝³ : HasEqualizers C
X' : C
h : X' ⟶ X
inst✝² : Epi h
f : X ⟶ Y
inst✝¹ : HasImage f
inst✝ : HasImage (h ≫ f)
⊢ image.preComp h f ≫ image.ι f = image.ι (h ≫ f)

Tactic:
· infer_instance

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
X Y Z : C
f✝ : X ⟶ Y
inst✝⁴ : HasImage f✝
inst✝³ : HasEqualizers C
X' : C
h : X' ⟶ X
inst✝² : Epi h
f : X ⟶ Y
inst✝¹ : HasImage f
inst✝ : HasImage (h ≫ f)
⊢ image.preComp h f ≫ image.ι f = image.ι (h ≫ f)
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: case refine_2
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasImages C
inst✝ : HasBinaryCoproducts C
A : C
f g h : MonoOver A
k₁ : f ⟶ h
k₂ : g ⟶ h
⊢ image.lift
        { I := h.obj.left, m := h.arrow, m_mono := ⋯, e := coprod.desc (Over.Hom.left k₁.hom) (Over.Hom.left k₂.hom),
          fac := ⋯ } ≫
      h.arrow =
    ((sup.obj f).obj g).arrow

Tactic:
apply image.lift_fac

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasPullbacks C
A : C
f₁ f₂ : Subobject A
inst✝ : HasBinaryProduct f₁ f₂
⊢ f₁ ⊓ f₂ ≤ (f₁ ⨯ f₂)

Tactic:
apply leOfHom

Goal state after:
case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasPullbacks C
A : C
f₁ f₂ : Subobject A
inst✝ : HasBinaryProduct f₁ f₂
⊢ f₁ ⊓ f₂ ⟶ f₁ ⨯ f₂
Module: Mathlib.CategoryTheory.Limits.Filtered

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ IsFiltered C ↔
    ∀ {J : Type v} [inst : SmallCategory J] [FinCategory J] (F : J ⥤ C), ∃ X, Nonempty (limit (F.op ⋙ yoneda.obj X))

Tactic:
rw [IsFiltered.iff_cocone_nonempty.{v}]
  refine ⟨fun h J _ _ F => ?_, fun h J _ _ F => ?_⟩
  · obtain ⟨c⟩ := h F
    exact ⟨c.pt, ⟨(limitCompYonedaIsoCocone F c.pt).inv c.ι⟩⟩
  · obtain ⟨pt, ⟨ι⟩⟩ := h F
    exact ⟨⟨pt, (limitCompYonedaIsoCocone F pt).hom ι⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X : Type v₂
α : Type u_1
Z : α → C
inst✝ : HasCoproduct Z
c : Cofan Z
hc : IsColimit c
⊢ IsLimit c.op

Tactic:
by
  let e : Discrete.functor (Opposite.op <| Z ·) ≅ (Discrete.opposite α).inverse ⋙
    (Discrete.functor Z).op := Discrete.natIso (fun _ ↦ Iso.refl _)
  refine IsLimit.ofIsoLimit ((IsLimit.postcomposeInvEquiv e _).2
    (IsLimit.whiskerEquivalence hc.op (Discrete.opposite α).symm))
    (Cone.ext (Iso.refl _) (fun ⟨a⟩ ↦ ?_))
  simp [e, Cofan.inj]

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Adjunction

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
L : C ⥤ D
H : Type u_3
inst✝¹ : Category.{v_3, u_3} H
inst✝ : ∀ (F : C ⥤ H), L.HasLeftKanExtension F
⊢ (L.lanAdjunction H).unit = L.lanUnit

Tactic:
ext F : 2
  dsimp [lanAdjunction, homEquivOfIsLeftKanExtension]
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_4, u_4} H
L : C ⥤ D
F : C ⥤ H
E : L.RightExtension F
Y : D
h : E.IsPointwiseRightKanExtensionAt Y
inst✝ : HasLimit (StructuredArrow.proj Y L ⋙ F)
g : StructuredArrow Y L
⊢ h.isoLimit.inv ≫ (CostructuredArrow.left E).map g.hom ≫ (CostructuredArrow.hom E).app g.right =
    limit.π (StructuredArrow.proj Y L ⋙ F) g

Tactic:
by
  simpa using! h.conePointUniqueUpToIso_inv_comp (limit.isLimit _) g

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic

Goal state before:
pp: case pos
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasCountableCoproducts C
inst✝³ : HasFiniteLimits C
inst✝² : ∀ (J : Type) [inst : Finite J], HasExactColimitsOfShape (Discrete J) C
inst✝¹ : HasExactColimitsOfShape (Discrete ℕ) C
J : Type
inst✝ : Countable J
h : Finite J
⊢ HasExactColimitsOfShape (Discrete J) C

pp: case neg
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasCountableCoproducts C
inst✝³ : HasFiniteLimits C
inst✝² : ∀ (J : Type) [inst : Finite J], HasExactColimitsOfShape (Discrete J) C
inst✝¹ : HasExactColimitsOfShape (Discrete ℕ) C
J : Type
inst✝ : Countable J
h : ¬Finite J
⊢ HasExactColimitsOfShape (Discrete J) C

Tactic:
· infer_instance

Goal state after:
case neg
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasCountableCoproducts C
inst✝³ : HasFiniteLimits C
inst✝² : ∀ (J : Type) [inst : Finite J], HasExactColimitsOfShape (Discrete J) C
inst✝¹ : HasExactColimitsOfShape (Discrete ℕ) C
J : Type
inst✝ : Countable J
h : ¬Finite J
⊢ HasExactColimitsOfShape (Discrete J) C
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic

Goal state before:
pp: case pos
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasCountableProducts C
inst✝³ : HasFiniteColimits C
inst✝² : ∀ (J : Type) [inst : Finite J], HasExactLimitsOfShape (Discrete J) C
inst✝¹ : HasExactLimitsOfShape (Discrete ℕ) C
J : Type
inst✝ : Countable J
h : Finite J
⊢ HasExactLimitsOfShape (Discrete J) C

pp: case neg
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasCountableProducts C
inst✝³ : HasFiniteColimits C
inst✝² : ∀ (J : Type) [inst : Finite J], HasExactLimitsOfShape (Discrete J) C
inst✝¹ : HasExactLimitsOfShape (Discrete ℕ) C
J : Type
inst✝ : Countable J
h : ¬Finite J
⊢ HasExactLimitsOfShape (Discrete J) C

Tactic:
· infer_instance

Goal state after:
case neg
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasCountableProducts C
inst✝³ : HasFiniteColimits C
inst✝² : ∀ (J : Type) [inst : Finite J], HasExactLimitsOfShape (Discrete J) C
inst✝¹ : HasExactLimitsOfShape (Discrete ℕ) C
J : Type
inst✝ : Countable J
h : ¬Finite J
⊢ HasExactLimitsOfShape (Discrete J) C
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝² : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
inst✝¹ : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
L : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ ℰ
α : A ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ L
inst✝ : L.IsLeftKanExtension α
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
Z : Cᵒᵖ
z : P.obj Z
⊢ (hom (((uliftYonedaAdjunction L α).unit.app P).app Z)) z =
    { down := α.app (unop Z) ≫ L.map (uliftYonedaEquiv.symm z) }

Tactic:
by
  have h₁ := (uliftYonedaAdjunction.{w} L α).homEquiv_unit P _ (𝟙 _)
  simp only [Functor.comp_obj, Functor.map_id, comp_id] at h₁
  simp [← h₁]

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

Goal state before:
pp: case mp
C : Type u₁
inst✝² : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝¹ : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
inst✝ : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
L : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ ℰ
α : A ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ L
⊢ L.IsLeftKanExtension α →
    IsIso α ∧
      PreservesColimitsOfSize.{v₁, max w u₁ v₁ v₂, max (max (max u₁ v₁) v₂) w, v₂,
          max (max (max u₁ (v₁ + 1)) (v₂ + 1)) (w + 1), u₂}
        L

pp: case mpr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝¹ : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
inst✝ : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
L : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ ℰ
α : A ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ L
⊢ IsIso α ∧
      PreservesColimitsOfSize.{v₁, max w u₁ v₁ v₂, max (max (max u₁ v₁) v₂) w, v₂,
          max (max (max u₁ (v₁ + 1)) (v₂ + 1)) (w + 1), u₂}
        L →
    L.IsLeftKanExtension α

Tactic:
· intro
    exact ⟨inferInstance, preservesColimits_of_natIso (Functor.leftKanExtensionUnique _
      (uliftYoneda.{max w v₂}.leftKanExtensionUnit A) _ α)⟩

Goal state after:
case mpr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝¹ : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
inst✝ : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
L : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ ℰ
α : A ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ L
⊢ IsIso α ∧
      PreservesColimitsOfSize.{v₁, max w u₁ v₁ v₂, max (max (max u₁ v₁) v₂) w, v₂,
          max (max (max u₁ (v₁ + 1)) (v₂ + 1)) (w + 1), u₂}
        L →
    L.IsLeftKanExtension α
Module: Mathlib.CategoryTheory.Subobject.Comma

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasFiniteColimits C
inst✝ : PreservesFiniteColimits S
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
hf : Mono f
hg : Mono g
i : P ≅ Q
hi : i.hom ≫ g = f
⊢ Subobject.mk f.unop.left.op = Subobject.mk g.unop.left.op

Tactic:
refine Subobject.mk_eq_mk_of_comm _ _ ((proj S T).mapIso i.unop).op (Quiver.Hom.unop_inj ?_)

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasFiniteColimits C
inst✝ : PreservesFiniteColimits S
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
hf : Mono f
hg : Mono g
i : P ≅ Q
hi : i.hom ≫ g = f
⊢ (((proj S T).mapIso i.unop).op.hom ≫ g.unop.left.op).unop = f.unop.left.op.unop
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
j₁ j₂ : J
t : Cotrident f
⊢ t.ι.app zero = f j₂ ≫ t.π

Tactic:
t.app_one

Goal state after:
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
j₁ j₂ : J
t : Cotrident f
⊢ t.ι.app zero = t.ι.app zero
Module: Mathlib.CategoryTheory.Subobject.Comma

Goal state before:
pp: case refine_3
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasFiniteColimits C
inst✝ : PreservesFiniteColimits S
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
this : (Subobject.ofMkLEMk f g h ≫ g).unop = f.unop
⊢ ((Subobject.ofMkLEMk f g h).unop.left.op ≫ (MonoOver.mk g).arrow.unop.left.op).unop =
    (MonoOver.mk f).arrow.unop.left.op.unop

Tactic:
simpa only [unop_op, Functor.id_obj, Functor.const_obj_obj, MonoOver.mk_obj, Over.mk_left,
        MonoOver.mk_arrow, unop_comp, Quiver.Hom.unop_op, comp_left]
          using congr_arg CommaMorphism.left this

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

Goal state before:
pp: case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
X : C
G : F.Elementsᵒᵖ ⥤ Type w := (CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X
c : G.CoconeTypes := G.coconeTypesEquiv.symm (coconeπOpCompShrinkYonedaObj F X)
this :
  ∀ (u : G.ColimitType) (x : F.obj X),
    G.descColimitType c u = x → G.ιColimitType (op (F.elementsMk X x)) (shrinkYonedaObjObjEquiv.symm (𝟙 X)) = u
u₁ u₂ : ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).ColimitType
hu :
  ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).descColimitType
      (((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).coconeTypesEquiv.symm
        (coconeπOpCompShrinkYonedaObj F X))
      u₁ =
    ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).descColimitType
      (((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).coconeTypesEquiv.symm
        (coconeπOpCompShrinkYonedaObj F X))
      u₂
x : c.pt
hx₁ : G.descColimitType c u₁ = x
hx₂ : G.descColimitType c u₂ = x
⊢ u₁ = u₂

Tactic:
← this _ _ hx₁,

Goal state after:
case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
X : C
G : F.Elementsᵒᵖ ⥤ Type w := (CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X
c : G.CoconeTypes := G.coconeTypesEquiv.symm (coconeπOpCompShrinkYonedaObj F X)
this :
  ∀ (u : G.ColimitType) (x : F.obj X),
    G.descColimitType c u = x → G.ιColimitType (op (F.elementsMk X x)) (shrinkYonedaObjObjEquiv.symm (𝟙 X)) = u
u₁ u₂ : ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).ColimitType
hu :
  ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).descColimitType
      (((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).coconeTypesEquiv.symm
        (coconeπOpCompShrinkYonedaObj F X))
      u₁ =
    ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).descColimitType
      (((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).coconeTypesEquiv.symm
        (coconeπOpCompShrinkYonedaObj F X))
      u₂
x : c.pt
hx₁ : G.descColimitType c u₁ = x
hx₂ : G.descColimitType c u₂ = x
⊢ G.ιColimitType (op (F.elementsMk X x)) (shrinkYonedaObjObjEquiv.symm (𝟙 X)) = u₂
Module: Mathlib.Algebra.Category.Grp.Adjunctions

Goal state before:
pp: ⊢ ∀ {X : CommGrpCat} {Y : CommMonCat} {f : (forget₂ CommGrpCat CommMonCat).obj X ⟶ Y},
    { toFun := fun f ↦ ofHom (CommMonCat.Hom.hom f).toHomUnits,
          invFun := fun f ↦ CommMonCat.ofHom ((Units.coeHom ↑Y).comp (Hom.hom f)), left_inv := ⋯, right_inv := ⋯ }
        f =
      { app := fun X ↦ ofHom toUnits.toMonoidHom, naturality := ⋯ }.app X ≫ CommMonCat.units.map f

Tactic:
by intros; rfl

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Adjunctions

Goal state before:
pp: ⊢ ∀ {X : CommGrpCat} {Y : CommMonCat} {g : X ⟶ CommMonCat.units.obj Y},
    { toFun := fun f ↦ ofHom (CommMonCat.Hom.hom f).toHomUnits,
            invFun := fun f ↦ CommMonCat.ofHom ((Units.coeHom ↑Y).comp (Hom.hom f)), left_inv := ⋯,
            right_inv := ⋯ }.symm
        g =
      (forget₂ CommGrpCat CommMonCat).map g ≫
        { app := fun X ↦ CommMonCat.ofHom (Units.coeHom ↑X), naturality := ⋯ }.app Y

Tactic:
by intros; rfl

Goal state after:
Module: Mathlib.Algebra.Ring.NegOnePow

Goal state before:
pp: n : ℤ
⊢ (n + 1).negOnePow = -n.negOnePow

Tactic:
rw [negOnePow_add, negOnePow_one, mul_neg, mul_one]

Goal state after:
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: case h
M : Type u_1
inst✝² : AddCommGroup M
R : Type u
inst✝¹ : CommRing R
inst✝ : Module R M
h : ∀ (I : Ideal R), Function.Surjective ⇑(LinearMap.lcomp R M (Submodule.subtype I))
I : Ideal R
g : ↥I →ₗ[R] M
g' : R →ₗ[R] M
hg' : (LinearMap.lcomp R M (Submodule.subtype I)) g' = g
x : R
⊢ ∀ (mem : x ∈ I), g' x = g ⟨x, mem⟩

Tactic:
hx

Goal state after:
case h
M : Type u_1
inst✝² : AddCommGroup M
R : Type u
inst✝¹ : CommRing R
inst✝ : Module R M
h : ∀ (I : Ideal R), Function.Surjective ⇑(LinearMap.lcomp R M (Submodule.subtype I))
I : Ideal R
g : ↥I →ₗ[R] M
g' : R →ₗ[R] M
hg' : (LinearMap.lcomp R M (Submodule.subtype I)) g' = g
x : R
hx : x ∈ I
⊢ g' x = g ⟨x, hx⟩
Module: Mathlib.Algebra.Order.Interval.Set.Group

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
⊢ x ∈ Ioc (a * b ^ m) (a * b ^ (m + 1)) ∩ Ioc (a * b ^ n) (a * b ^ (n + 1)) → x ∈ ∅

Tactic:
hx

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ioc (a * b ^ m) (a * b ^ (m + 1)) ∩ Ioc (a * b ^ n) (a * b ^ (n + 1))
⊢ x ∈ ∅
Module: Mathlib.Algebra.Order.Interval.Set.Group

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
⊢ x ∈ Ico (a * b ^ m) (a * b ^ (m + 1)) ∩ Ico (a * b ^ n) (a * b ^ (n + 1)) → x ∈ ∅

Tactic:
hx

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ico (a * b ^ m) (a * b ^ (m + 1)) ∩ Ico (a * b ^ n) (a * b ^ (n + 1))
⊢ x ∈ ∅
Module: Mathlib.Data.Nat.Count

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ count p (n + 1) = count p n + if p n then 1 else 0

Tactic:
grind [count, List.range_succ]

Goal state after:
Module: Mathlib.Data.Nat.Count

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
a k : ℕ
h : count p a < count p (a + k + 1)
⊢ ∃ x ∈ Set.Ico a (a + k + 1), p x

Tactic:
rw [add_assoc, count_add, Nat.lt_add_right_iff_pos] at h

Goal state after:
p : ℕ → Prop
inst✝ : DecidablePred p
a k : ℕ
h : 0 < count (fun k ↦ p (a + k)) (k + 1)
⊢ ∃ x ∈ Set.Ico a (a + k + 1), p x