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

Goal state before:
pp: case h₃
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
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
⊢ m.τ₃ =
    { τ₁ := h₁.desc (π₁.mapCocone s), τ₂ := h₂.desc (π₂.mapCocone s), τ₃ := h₃.desc (π₃.mapCocone s), comm₁₂ := ⋯,
        comm₂₃ := ⋯ }.τ₃

Tactic:
exact h₃.uniq (π₃.mapCocone s) _ (fun j => π₃.congr_map (hm j))

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

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
inst✝⁸ : HasZeroMorphisms C
inst✝⁷ : HasZeroMorphisms D
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁶ : F.PreservesZeroMorphisms
inst✝⁵ : S₁.HasHomology
inst✝⁴ : S₂.HasHomology
inst✝³ : (S₁.map F).HasHomology
inst✝² : (S₂.map F).HasHomology
inst✝¹ : F.PreservesLeftHomologyOf S₁
inst✝ : F.PreservesLeftHomologyOf S₂
⊢ leftHomologyMap' (F.mapShortComplex.map φ) (S₁.map F).homologyData.left (S₂.map F).homologyData.left ≫
      leftHomologyMap' (𝟙 (S₂.map F)) (S₂.map F).homologyData.left (S₂.map F).leftHomologyData ≫
        leftHomologyMap' (𝟙 (S₂.map F)) (S₂.map F).leftHomologyData (S₂.homologyData.left.map F) =
    (leftHomologyMap' (𝟙 (S₁.map F)) (S₁.map F).homologyData.left (S₁.map F).leftHomologyData ≫
        leftHomologyMap' (𝟙 (S₁.map F)) (S₁.map F).leftHomologyData (S₁.homologyData.left.map F)) ≫
      F.map (leftHomologyMap' φ S₁.homologyData.left S₂.homologyData.left)

Tactic:
simp only [LeftHomologyData.map_leftHomologyMap', ← leftHomologyMap'_comp, comp_id, id_comp]

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
β : Type v
c : β → C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasBiproduct c
inst✝ : ∀ (b : β), Injective (c b)
X✝ Y✝ : C
g : X✝ ⟶ ⨁ c
f : X✝ ⟶ Y✝
mono : Mono f
j✝ : β
⊢ (f ≫ biproduct.lift fun b ↦ factorThru (g ≫ biproduct.π c b) f) ≫ biproduct.π c j✝ = g ≫ biproduct.π c j✝

Tactic:
simp only [Category.assoc, biproduct.lift_π, comp_factorThru]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
J : C
⊢ Injective J ↔ (yoneda.obj J).PreservesEpimorphisms

Tactic:
rw [injective_iff_projective_op, Projective.projective_iff_preservesEpimorphisms_coyoneda_obj]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
J : C
⊢ (coyoneda.obj (op (op J))).PreservesEpimorphisms ↔ (yoneda.obj J).PreservesEpimorphisms
Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
h : S.HomologyData
this✝ : Epi h.left.f'
this : Mono h.right.g'
S' : ShortComplex C := { X₁ := h.left.K, X₂ := S.X₂, X₃ := S.X₃, f := h.left.i, g := S.g, zero := ⋯ }
S'' : ShortComplex C := { X₁ := h.left.K, X₂ := S.X₂, X₃ := h.right.Q, f := h.left.i, g := h.right.p, zero := ⋯ }
a : S ⟶ S' := { τ₁ := h.left.f', τ₂ := 𝟙 S.X₂, τ₃ := 𝟙 S.X₃, comm₁₂ := ⋯, comm₂₃ := ⋯ }
b : S'' ⟶ S' := { τ₁ := 𝟙 S''.X₁, τ₂ := 𝟙 S''.X₂, τ₃ := h.right.g', comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ { X₁ := h.left.K, X₂ := S.X₂, X₃ := h.right.Q, f := h.left.i, g := h.right.p, zero := ⋯ }.Exact

Tactic:
rwa [ShortComplex.exact_iff_of_epi_of_isIso_of_mono b,
      ← ShortComplex.exact_iff_of_epi_of_isIso_of_mono a]

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.LeftExact

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Preadditive C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Preadditive D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
X Y Z : C
π₁ : Z ⟶ X
π₂ : Z ⟶ Y
inst✝ : PreservesLimit (parallelPair π₂ 0) F
i : IsLimit (BinaryFan.mk π₁ π₂)
⊢ IsLimit (F.mapCone (BinaryFan.mk π₁ π₂))

Tactic:
let bc := BinaryBicone.ofLimitCone i

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Preadditive C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Preadditive D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
X Y Z : C
π₁ : Z ⟶ X
π₂ : Z ⟶ Y
inst✝ : PreservesLimit (parallelPair π₂ 0) F
i : IsLimit (BinaryFan.mk π₁ π₂)
bc : BinaryBicone X Y := BinaryBicone.ofLimitCone i
⊢ IsLimit (F.mapCone (BinaryFan.mk π₁ π₂))
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₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
⊢ S₁.Exact ↔ S₂.Exact

Tactic:
by
  constructor
  · rintro ⟨h₁, z₁⟩
    exact ⟨HomologyData.ofEpiOfIsIsoOfMono φ h₁, z₁⟩
  · rintro ⟨h₂, z₂⟩
    exact ⟨HomologyData.ofEpiOfIsIsoOfMono' φ h₂, z₂⟩

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
⊢ S.Exact ↔ h.left.i ≫ h.right.p = 0

Tactic:
have := HasHomology.mk' h
  rw [h.left.exact_iff, ← h.comm]
  constructor
  · intro z
    rw [IsZero.eq_of_src z h.iso.hom 0, zero_comp, comp_zero]
  · 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✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
hf : S.f = 0
this✝¹ : S.HasHomology
this✝ : Epi S.toCycles
this : S.iCycles = 0
A : C
x₂ : A ⟶ S.X₂
hx₂ : x₂ ≫ S.g = 0
⊢ S.liftCycles x₂ hx₂ ≫ S.iCycles = 0

Tactic:
this,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
hf : S.f = 0
this✝¹ : S.HasHomology
this✝ : Epi S.toCycles
this : S.iCycles = 0
A : C
x₂ : A ⟶ S.X₂
hx₂ : x₂ ≫ S.g = 0
⊢ S.liftCycles x₂ hx₂ ≫ 0 = 0
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
hg : S.g = 0
this✝¹ : S.HasHomology
this✝ : Mono S.fromOpcycles
this : S.pOpcycles = 0
A : C
x₂ : S.X₂ ⟶ A
hx₂ : S.f ≫ x₂ = 0
⊢ S.pOpcycles ≫ S.descOpcycles x₂ hx₂ = 0

Tactic:
this,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
hg : S.g = 0
this✝¹ : S.HasHomology
this✝ : Mono S.fromOpcycles
this : S.pOpcycles = 0
A : C
x₂ : S.X₂ ⟶ A
hx₂ : S.f ≫ x₂ = 0
⊢ 0 ≫ S.descOpcycles x₂ hx₂ = 0
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : Balanced C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.Exact
inst✝³ : Mono S₁.f
inst✝² : Mono S₂.f
inst✝¹ : Mono φ.τ₁
inst✝ : Mono φ.τ₃
A : C
x₂ : A ⟶ S₁.X₂
hx₂ : x₂ ≫ φ.τ₂ = 0
x₁ : A ⟶ S₁.X₁
hx₁ : x₁ ≫ S₁.f = x₂
this : x₁ = 0
⊢ x₁ ≫ S₁.f = 0

Tactic:
this,

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : Balanced C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.Exact
inst✝³ : Mono S₁.f
inst✝² : Mono S₂.f
inst✝¹ : Mono φ.τ₁
inst✝ : Mono φ.τ₃
A : C
x₂ : A ⟶ S₁.X₂
hx₂ : x₂ ≫ φ.τ₂ = 0
x₁ : A ⟶ S₁.X₁
hx₁ : x₁ ≫ S₁.f = x₂
this : x₁ = 0
⊢ 0 ≫ S₁.f = 0
Module: Mathlib.CategoryTheory.Subobject.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
x : Subobject X
⊢ (map (𝟙 X)).obj x = x

Tactic:
induction x using Quotient.inductionOn' with | _ f
  exact Quotient.sound ⟨(MonoOver.mapId _).app f⟩

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
cg : KernelFork S.g
hg : IsLimit cg
cf : CokernelCofork S.f
hf : IsColimit cf
e₁ : (Fork.ofι (kernel.ι S.g) ⋯).pt ≅ cg.pt := (kernelIsKernel S.g).conePointUniqueUpToIso hg
e₂ : (Cofork.ofπ (cokernel.π S.f) ⋯).pt ≅ cf.pt := (cokernelIsCokernel S.f).coconePointUniqueUpToIso hf
this : Fork.ι cg ≫ Cofork.π cf = e₁.inv ≫ kernel.ι S.g ≫ cokernel.π S.f ≫ e₂.hom
⊢ kernel.ι S.g ≫ cokernel.π S.f = 0 ↔ Fork.ι cg ≫ Cofork.π cf = 0

Tactic:
this,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
cg : KernelFork S.g
hg : IsLimit cg
cf : CokernelCofork S.f
hf : IsColimit cf
e₁ : (Fork.ofι (kernel.ι S.g) ⋯).pt ≅ cg.pt := (kernelIsKernel S.g).conePointUniqueUpToIso hg
e₂ : (Cofork.ofπ (cokernel.π S.f) ⋯).pt ≅ cf.pt := (cokernelIsCokernel S.f).coconePointUniqueUpToIso hf
this : Fork.ι cg ≫ Cofork.π cf = e₁.inv ≫ kernel.ι S.g ≫ cokernel.π S.f ≫ e₂.hom
⊢ kernel.ι S.g ≫ cokernel.π S.f = 0 ↔ e₁.inv ≫ kernel.ι S.g ≫ cokernel.π S.f ≫ e₂.hom = 0
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_3, u_3} D'
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
E E' : L.RightExtension F
Y : D
g₁ g₂ : StructuredArrow Y L
φ : g₁ ⟶ g₂
⊢ (CostructuredArrow.left E).map g₂.hom ≫ (CostructuredArrow.hom E).app g₂.right =
    (CostructuredArrow.left E).map g₁.hom ≫ (CostructuredArrow.hom E).app g₁.right ≫ F.map φ.right

Tactic:
← StructuredArrow.w φ,

Goal state after:
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_3, u_3} D'
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
E E' : L.RightExtension F
Y : D
g₁ g₂ : StructuredArrow Y L
φ : g₁ ⟶ g₂
⊢ (CostructuredArrow.left E).map (g₁.hom ≫ L.map (StructuredArrow.Hom.right φ)) ≫
      (CostructuredArrow.hom E).app g₂.right =
    (CostructuredArrow.left E).map g₁.hom ≫ (CostructuredArrow.hom E).app g₁.right ≫ F.map φ.right
Module: Mathlib.CategoryTheory.Limits.Shapes.Countable

Goal state before:
pp: J : Type u_2
inst✝² : Countable J
inst✝¹ : Preorder J
inst✝ : IsCofiltered J
d : J
n : ℕ
g : (sequentialFunctor J).obj (op n) ≤ d
this : Nonempty (CostructuredArrow (sequentialFunctor J) d)
i j : CostructuredArrow (sequentialFunctor J) d
⊢ Nonempty (i ⟶ j) ∨ Nonempty (j ⟶ i)

Tactic:
wlog! h : (unop i.left) ≤ (unop j.left)

Goal state after:
case inr
J : Type u_2
inst✝² : Countable J
inst✝¹ : Preorder J
inst✝ : IsCofiltered J
d : J
n : ℕ
g : (sequentialFunctor J).obj (op n) ≤ d
this✝ : Nonempty (CostructuredArrow (sequentialFunctor J) d)
i j : CostructuredArrow (sequentialFunctor J) d
this :
  ∀ (J : Type u_2) [inst : Countable J] [inst_1 : Preorder J] [inst_2 : IsCofiltered J] (d : J) (n : ℕ),
    (sequentialFunctor J).obj (op n) ≤ d →
      Nonempty (CostructuredArrow (sequentialFunctor J) d) →
        ∀ (i j : CostructuredArrow (sequentialFunctor J) d),
          unop i.left ≤ unop j.left → Nonempty (i ⟶ j) ∨ Nonempty (j ⟶ i)
h : unop j.left < unop i.left
⊢ Nonempty (i ⟶ j) ∨ Nonempty (j ⟶ i)

J✝ : Type u_2
inst✝⁵ : Countable J✝
inst✝⁴ : Preorder J✝
inst✝³ : IsCofiltered J✝
J : Type u_2
inst✝² : Countable J
inst✝¹ : Preorder J
inst✝ : IsCofiltered J
d : J
n : ℕ
g : (sequentialFunctor J).obj (op n) ≤ d
this : Nonempty (CostructuredArrow (sequentialFunctor J) d)
i j : CostructuredArrow (sequentialFunctor J) d
h : unop i.left ≤ unop j.left
⊢ Nonempty (i ⟶ j) ∨ Nonempty (j ⟶ i)
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} C'
inst✝³ : Category.{v_3, u_3} H
inst✝² : Category.{v_4, u_4} D
inst✝¹ : Category.{v_5, u_5} D'
F' : D ⥤ H
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
inst✝ : F'.IsLeftKanExtension α
c : Cocone F
hc : IsColimit c
s : Cocone F'
m : (F'.coconeOfIsLeftKanExtension α c).pt ⟶ s.pt
hm : ∀ (j : D), (F'.coconeOfIsLeftKanExtension α c).ι.app j ≫ m = s.ι.app j
j : C
this : (F'.descOfIsLeftKanExtension α ((const D).obj c.pt) c.ι).app (L.obj j) ≫ m = s.ι.app (L.obj j)
⊢ α.app j ≫ (F'.descOfIsLeftKanExtension α ((const D).obj c.pt) c.ι).app (L.obj j) ≫ m =
    c.ι.app j ≫ hc.desc { pt := s.1, ι := α ≫ L.whiskerLeft s.ι }

Tactic:
this,

Goal state after:
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} C'
inst✝³ : Category.{v_3, u_3} H
inst✝² : Category.{v_4, u_4} D
inst✝¹ : Category.{v_5, u_5} D'
F' : D ⥤ H
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
inst✝ : F'.IsLeftKanExtension α
c : Cocone F
hc : IsColimit c
s : Cocone F'
m : (F'.coconeOfIsLeftKanExtension α c).pt ⟶ s.pt
hm : ∀ (j : D), (F'.coconeOfIsLeftKanExtension α c).ι.app j ≫ m = s.ι.app j
j : C
this : (F'.descOfIsLeftKanExtension α ((const D).obj c.pt) c.ι).app (L.obj j) ≫ m = s.ι.app (L.obj j)
⊢ α.app j ≫ s.ι.app (L.obj j) = c.ι.app j ≫ hc.desc { pt := s.1, ι := α ≫ L.whiskerLeft s.ι }
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} C'
inst✝³ : Category.{v_3, u_3} H
inst✝² : Category.{v_4, u_4} D
inst✝¹ : Category.{v_5, u_5} D'
F' : D ⥤ H
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
inst✝ : F'.IsRightKanExtension α
c : Cone F
hc : IsLimit c
s : Cone F'
⊢ ∀ (j : D), hc.lift { pt := s.1, π := L.whiskerLeft s.π ≫ α } ≫ (F'.coneOfIsRightKanExtension α c).π.app j = s.π.app j

Tactic:
by
    have : (Functor.const _).map (hc.lift (Cone.mk _ (whiskerLeft L s.π ≫ α))) ≫
        F'.liftOfIsRightKanExtension α ((const D).obj c.pt) c.π = s.π :=
      F'.hom_ext_of_isRightKanExtension α _ _ (by cat_disch)
    exact congr_app this

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

Goal state before:
pp: C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} C'
inst✝³ : Category.{v_3, u_3} H
inst✝² : Category.{v_4, u_4} D
inst✝¹ : Category.{v_5, u_5} D'
F' : D ⥤ H
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
inst✝ : F'.IsRightKanExtension α
c : Cone F
hc : IsLimit c
s : Cone F'
m : s.pt ⟶ (F'.coneOfIsRightKanExtension α c).pt
hm : ∀ (j : D), m ≫ (F'.coneOfIsRightKanExtension α c).π.app j = s.π.app j
j : C
this : m ≫ (F'.liftOfIsRightKanExtension α ((const D).obj c.pt) c.π).app (L.obj j) = s.π.app (L.obj j)
⊢ (m ≫ (F'.liftOfIsRightKanExtension α ((const D).obj c.pt) c.π).app (L.obj j)) ≫ α.app j =
    hc.lift { pt := s.1, π := L.whiskerLeft s.π ≫ α } ≫ c.π.app j

Tactic:
this,

Goal state after:
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} C'
inst✝³ : Category.{v_3, u_3} H
inst✝² : Category.{v_4, u_4} D
inst✝¹ : Category.{v_5, u_5} D'
F' : D ⥤ H
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
inst✝ : F'.IsRightKanExtension α
c : Cone F
hc : IsLimit c
s : Cone F'
m : s.pt ⟶ (F'.coneOfIsRightKanExtension α c).pt
hm : ∀ (j : D), m ≫ (F'.coneOfIsRightKanExtension α c).π.app j = s.π.app j
j : C
this : m ≫ (F'.liftOfIsRightKanExtension α ((const D).obj c.pt) c.π).app (L.obj j) = s.π.app (L.obj j)
⊢ s.π.app (L.obj j) ≫ α.app j = hc.lift { pt := s.1, π := L.whiskerLeft s.π ≫ α } ≫ c.π.app j
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 ⥤ ℰ
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
E : ℰ
g : P ⟶ (restrictedULiftYoneda A).obj E
⊢ (fun f ↦
        { app := fun x ↦ ↾fun x_1 ↦ { down := f.app (CostructuredArrow.mk (uliftYonedaEquiv.symm x_1)) },
          naturality := ⋯ })
      ((fun g ↦ { app := fun y ↦ (uliftYonedaEquiv (y.hom ≫ g)).down, naturality := ⋯ }) g) =
    g

Tactic:
by
    ext X x
    apply ULift.down_injective
    simp [uliftYonedaEquiv]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ Dᵒᵖ ⥤ Type (max w v₁ v₂)
φ : F ⋙ uliftYoneda.{max w v₁, v₂, u₂} ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ G
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
X : C
x : P.obj (op X)
⊢ uliftYonedaEquiv
      ({
              pt :=
                { obj := fun X ↦ (G.obj P).obj (F.op.obj X), map := fun {X Y} f ↦ (G.obj P).map (F.op.map f),
                  map_id := ⋯, map_comp := ⋯ },
              ι := { app := fun x ↦ coconeApp φ (unop x), naturality := ⋯ } }.ι.app
        (op (P.elementsMk (op X) x))) =
    (hom ((G.map (uliftYonedaEquiv.symm x)).app (op (F.obj X))))
      ((hom ((φ.app X).app (op (F.obj X)))) { down := 𝟙 (unop (op (F.obj X))) })

Tactic:
dsimp only [coconeApp]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ Dᵒᵖ ⥤ Type (max w v₁ v₂)
φ : F ⋙ uliftYoneda.{max w v₁, v₂, u₂} ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ G
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
X : C
x : P.obj (op X)
⊢ uliftYonedaEquiv
      (uliftYonedaEquiv.symm
        ((hom ((G.map (uliftYonedaEquiv.symm x)).app (F.op.obj (op X))))
          ((hom ((φ.app X).app (F.op.obj (op X)))) { down := 𝟙 (unop (F.op.obj (op X))) }))) =
    (hom ((G.map (uliftYonedaEquiv.symm x)).app (op (F.obj X))))
      ((hom ((φ.app X).app (op (F.obj X)))) { down := 𝟙 (F.obj X) })
Module: Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic

Goal state before:
pp: case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Abelian C
inst✝¹ : Abelian D
inst✝ : IsGrothendieckAbelian.{w, v, u} C
α : C ≌ D
hasFilteredColimits : HasFilteredColimitsOfSize.{w, w, v₂, u₂} D
⊢ LocallySmall.{w, v₂, u₂} D

pp: case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Abelian C
inst✝¹ : Abelian D
inst✝ : IsGrothendieckAbelian.{w, v, u} C
α : C ≌ D
hasFilteredColimits : HasFilteredColimitsOfSize.{w, w, v₂, u₂} D
⊢ AB5OfSize.{w, w, v₂, u₂} D

pp: case refine_3
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Abelian C
inst✝¹ : Abelian D
inst✝ : IsGrothendieckAbelian.{w, v, u} C
α : C ≌ D
hasFilteredColimits : HasFilteredColimitsOfSize.{w, w, v₂, u₂} D
⊢ HasSeparator D

Tactic:
· exact locallySmall_of_faithful α.inverse

Goal state after:
case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Abelian C
inst✝¹ : Abelian D
inst✝ : IsGrothendieckAbelian.{w, v, u} C
α : C ≌ D
hasFilteredColimits : HasFilteredColimitsOfSize.{w, w, v₂, u₂} D
⊢ AB5OfSize.{w, w, v₂, u₂} D

case refine_3
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Abelian C
inst✝¹ : Abelian D
inst✝ : IsGrothendieckAbelian.{w, v, u} C
α : C ≌ D
hasFilteredColimits : HasFilteredColimitsOfSize.{w, w, v₂, u₂} D
⊢ HasSeparator D
Module: Mathlib.Algebra.Category.Grp.Zero

Goal state before:
pp: case refine_1
G : GrpCat
inst✝ : Subsingleton ↑G
X : GrpCat
f : G ⟶ X
x : ↑G
this : x = 1
⊢ (Hom.hom f) x = (Hom.hom default) x

Tactic:
this,

Goal state after:
case refine_1
G : GrpCat
inst✝ : Subsingleton ↑G
X : GrpCat
f : G ⟶ X
x : ↑G
this : x = 1
⊢ (Hom.hom f) 1 = (Hom.hom default) 1
Module: Mathlib.Algebra.Category.Grp.Zero

Goal state before:
pp: case refine_1
G : CommGrpCat
inst✝ : Subsingleton ↑G
X : CommGrpCat
f : G ⟶ X
x : ↑G
this : x = 1
⊢ (Hom.hom f) x = (Hom.hom default) x

Tactic:
this,

Goal state after:
case refine_1
G : CommGrpCat
inst✝ : Subsingleton ↑G
X : CommGrpCat
f : G ⟶ X
x : ↑G
this : x = 1
⊢ (Hom.hom f) 1 = (Hom.hom default) 1
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : AddGroup α
inst✝ : InvolutiveNeg β
h : Antiperiodic f c
n : ℤ
⊢ Antiperiodic f ((2 * n + 1) • c)

Tactic:
by
  intro x
  rw [add_zsmul, one_zsmul, ← add_assoc, h, h.even_zsmul_periodic]

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

Goal state before:
pp: R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ⇑i)
h : Baer R Q
y : N
r : R
a : ↥(supExtensionOfMaxSingleton i f y)
⊢ ExtensionOfMaxAdjoin.extensionToFun i f h (r • a) = (RingHom.id R) r • ExtensionOfMaxAdjoin.extensionToFun i f h a

Tactic:
by
        dsimp
        have eq1 :
          r • (a : N) =
            ↑(r • ExtensionOfMaxAdjoin.fst i a) + (r • ExtensionOfMaxAdjoin.snd i a) • y := by
          rw [ExtensionOfMaxAdjoin.eqn, smul_add, smul_eq_mul, mul_smul]
          rfl
        rw [ExtensionOfMaxAdjoin.extensionToFun_wd i f h (r • a :) _ _ eq1, map_smul,
          LinearPMap.map_smul, ← smul_add]
        congr

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

Goal state before:
pp: n : ℕ
⊢ ∑ m ∈ range n.succ with m ∣ n, φ m = n

Tactic:
convert! sum_totient _ using 1

Goal state after:
case e'_2
n : ℕ
⊢ ∑ m ∈ range n.succ with m ∣ n, φ m = n.divisors.sum φ
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case zero
⊢ Odd (φ 0) ↔ 0 = 1 ∨ 0 = 2

Tactic:
simp [Nat.totient_even]

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

Goal state before:
pp: case succ.zero
⊢ Odd (φ (0 + 1)) ↔ 0 + 1 = 1 ∨ 0 + 1 = 2

Tactic:
simp [Nat.totient_even]

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

Goal state before:
pp: case succ.succ.zero
⊢ Odd (φ (0 + 1 + 1)) ↔ 0 + 1 + 1 = 1 ∨ 0 + 1 + 1 = 2

Tactic:
simp [Nat.totient_even]

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

Goal state before:
pp: case succ.succ.succ
n✝ : ℕ
⊢ Odd (φ (n✝ + 1 + 1 + 1)) ↔ n✝ + 1 + 1 + 1 = 1 ∨ n✝ + 1 + 1 + 1 = 2

Tactic:
simp [Nat.totient_even]

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoDiv hp a (-b) = -(toIocDiv hp (-a) b + 1)

Tactic:
suffices toIcoDiv hp a (-b) = -toIocDiv hp (-(a + p)) b by
    rwa [neg_add, ← sub_eq_add_neg, toIocDiv_sub_eq_toIocDiv_add', toIocDiv_add_right] at this

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoDiv hp a (-b) = -toIocDiv hp (-(a + p)) b
Module: Mathlib.Order.Filter.Lift

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝ : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
s : Set β
t : Set α
ht✝ : t ∈ iInf f
i✝ : ι
s₁✝ s₂✝ : Set α
hs : s₁✝ ∈ f i✝
ht : ⨅ i, (f i).lift g ≤ g s₂✝
⊢ ⨅ i, (f i).lift g ≤ g (s₁✝ ∩ s₂✝)

Tactic:
rw [hg]
      exact le_inf (iInf₂_le_of_le _ _ <| iInf_le _ hs) ht

Goal state after:
Module: Mathlib.Topology.Basic

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set (Set X)
⊢ (∀ t ∈ s, IsClosed[inst✝] t) → IsClosed[inst✝] (⋂₀ s)

Tactic:
by
  simpa only [← isOpen_compl_iff, compl_sInter, sUnion_image] using isOpen_biUnion

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
h : toIocMod hp a b = toIocMod hp a c
| c - b

Tactic:
← toIocMod_add_toIocDiv_zsmul hp a b,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
h : toIocMod hp a b = toIocMod hp a c
| c - (toIocMod hp a b + toIocDiv hp a b • p)
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
h : Disjoint (closure s) (closure t)
⊢ interior (s ∪ t) = interior s ∪ interior t

Tactic:
have full : interior sᶜ ∪ interior tᶜ = univ := by simpa [disjoint_iff, ← compl_inter] using h

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
h : Disjoint (closure s) (closure t)
full : interior sᶜ ∪ interior tᶜ = univ
⊢ interior (s ∪ t) = interior s ∪ interior t