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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ h₁.homologyIso.hom ≫ leftHomologyMap' φ h₁ h₂ = homologyMap φ ≫ h₂.homologyIso.hom

Tactic:
dsimp [homologyIso, ShortComplex.leftHomologyIso, homologyMap, homologyMap', leftHomologyIso]
  simp only [← leftHomologyMap'_comp, id_comp, comp_id]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ h₁.homologyIso.inv ≫ homologyMap φ = leftHomologyMap' φ h₁ h₂ ≫ h₂.homologyIso.inv

Tactic:
dsimp [homologyIso, ShortComplex.leftHomologyIso, homologyMap, homologyMap', leftHomologyIso]
  simp only [← leftHomologyMap'_comp, id_comp, comp_id]

Goal state after:
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₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ cyclesMap' (-φ) h₁ h₂ = -cyclesMap' φ h₁ h₂

Tactic:
by
  have γ : LeftHomologyMapData φ h₁ h₂ := default
  simp only [γ.cyclesMap'_eq, γ.neg.cyclesMap'_eq, LeftHomologyMapData.neg_φK]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ cokernel.desc f (kernel.ι f.op).unop ⋯ ≫ (kernel.lift f.op (cokernel.π f).op ⋯).unop = 𝟙 (cokernel f)

Tactic:
by
    ext
    simp [← unop_comp]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ (cokernel.desc f.op (kernel.ι f).op ⋯).unop ≫ kernel.lift f (cokernel.π f.op).unop ⋯ = 𝟙 (kernel f)

Tactic:
by
    ext
    simp [← unop_comp]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : EnoughInjectives C
X : C
h : IsZero X
this : Injective X
⊢ IsZero X → IsZero { J := X, injective := ⋯, f := 𝟙 X, mono := ⋯ }.J

Tactic:
by tauto

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : EnoughInjectives C
X : C
h : ¬IsZero X
⊢ IsZero X → IsZero ⋯.some.J

Tactic:
by tauto

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:
by
  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.Ab

Goal state before:
pp: case mp
S : ShortComplex Ab
x₂ : ↑S.X₂
⊢ ((ConcreteCategory.hom S.g) x₂ = 0 → ∃ x₁, (ConcreteCategory.hom S.f) x₁ = x₂) →
    ((ConcreteCategory.hom S.g) x₂ = 0 ↔ x₂ ∈ Set.range ⇑(ConcreteCategory.hom S.f))

pp: case mpr
S : ShortComplex Ab
x₂ : ↑S.X₂
⊢ ((ConcreteCategory.hom S.g) x₂ = 0 ↔ x₂ ∈ Set.range ⇑(ConcreteCategory.hom S.f)) →
    (ConcreteCategory.hom S.g) x₂ = 0 → ∃ x₁, (ConcreteCategory.hom S.f) x₁ = x₂

Tactic:
· intro h
    refine ⟨h, ?_⟩
    rintro ⟨x₁, rfl⟩
    simp only [ab_zero_apply]

Goal state after:
case mpr
S : ShortComplex Ab
x₂ : ↑S.X₂
⊢ ((ConcreteCategory.hom S.g) x₂ = 0 ↔ x₂ ∈ Set.range ⇑(ConcreteCategory.hom S.f)) →
    (ConcreteCategory.hom S.g) x₂ = 0 → ∃ x₁, (ConcreteCategory.hom S.f) x₁ = x₂
Module: Mathlib.CategoryTheory.Subobject.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
A : C
X Y : Subobject A
h : X = Y
⊢ eqToHom ⋯ ≫ Y.arrow = X.arrow

Tactic:
by
  induction h
  simp

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

Goal state before:
pp: case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
inst✝ : HasPullbacks C
f : X ⟶ Y
g : Y ⟶ Z
t : MonoOver Z
⊢ (pullback (f ≫ g)).obj (Quotient.mk'' t) = (pullback f).obj ((pullback g).obj (Quotient.mk'' t))

Tactic:
exact Quotient.sound ⟨(MonoOver.pullbackComp _ _).app t⟩

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X Y : C
inst✝² : HasEqualizers C
f : X ⟶ Y
inst✝¹ : HasImage f
Y' : C
h : Y ⟶ Y'
inst✝ : IsIso h
⊢ (imageSubobjectCompIso f h).hom ≫ (imageSubobject f).arrow = (imageSubobject (f ≫ h)).arrow ≫ inv h

Tactic:
by
  simp [imageSubobjectCompIso]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X Y : C
inst✝² : HasEqualizers C
f : X ⟶ Y
inst✝¹ : HasImage f
Y' : C
h : Y ⟶ Y'
inst✝ : IsIso h
⊢ (imageSubobjectCompIso f h).inv ≫ (imageSubobject (f ≫ h)).arrow = (imageSubobject f).arrow ≫ h

Tactic:
by
  simp [imageSubobjectCompIso]

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

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✝² : Abelian C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
⊢ [∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact, ∀ (S : ShortComplex C), S.Exact → (S.map F).Exact,
      F.PreservesHomology, PreservesFiniteLimits F ∧ PreservesFiniteColimits F].TFAE

Tactic:
by
  tfae_have 1 → 3
  | hF => by
    refine ⟨fun {X Y} f ↦ ?_, fun {X Y} f ↦ ?_⟩
    · have h := (preservesFiniteLimits_tfae F |>.out 0 2 |>.1 fun S hS ↦
        And.intro (hF S hS).exact (hF S hS).mono_f)
      exact h f
    · have h := (preservesFiniteColimits_tfae F |>.out 0 2 |>.1 fun S hS ↦
        And.intro (hF S hS).exact (hF S hS).epi_g)
      exact h f
  tfae_have 2 → 1
  | hF, S, hS => by
    have : Mono (S.map F).f := exact_iff_mono _ (by simp) |>.1 <|
      hF (.mk (0 : 0 ⟶ S.X₁) S.f <| by simp) (exact_iff_mono _ (by simp) |>.2 hS.mono_f)
    have : Epi (S.map F).g := exact_iff_epi _ (by simp) |>.1 <|
      hF (.mk S.g (0 : S.X₃ ⟶ 0) <| by simp) (exact_iff_epi _ (by simp) |>.2 hS.epi_g)
    exact ⟨hF S hS.exact⟩
  tfae_have 3 → 4
  | h => ⟨preservesFiniteLimits_of_preservesHomology F,
      preservesFiniteColimits_of_preservesHomology F⟩
  tfae_have 4 → 2
  | ⟨h1, h2⟩, _, h => h.map F
  tfae_finish

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A B : C
inst✝ : HasBinaryProduct A B
⊢ (coprod.inl ≫ (opProdIsoCoprod A B).inv).unop = prod.fst

Tactic:
inl_opProdIsoCoprod_inv,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A B : C
inst✝ : HasBinaryProduct A B
⊢ prod.fst.op.unop = prod.fst
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 : L.LeftExtension F
Y : D
g₁ g₂ : CostructuredArrow L Y
φ : g₁ ⟶ g₂
⊢ (CostructuredArrow.proj L Y ⋙ F).map φ ≫ (StructuredArrow.hom E).app g₂.left ≫ (StructuredArrow.right E).map g₂.hom =
    ((StructuredArrow.hom E).app g₁.left ≫ (StructuredArrow.right E).map g₁.hom) ≫
      ((const (CostructuredArrow L Y)).obj ((StructuredArrow.right E).obj Y)).map φ

Tactic:
dsimp
        rw [← CostructuredArrow.w φ]
        simp only [NatTrans.naturality_assoc, Functor.comp_map,
          Functor.map_comp, comp_id]

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

Goal state before:
pp: case e_7
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
inst✝ : L.HasPointwiseRightKanExtension F
Y₁ Y₂ Y₃ : D
f : Y₁ ⟶ Y₂
f' : Y₂ ⟶ Y₃
j : StructuredArrow Y₃ L
⊢ (StructuredArrow.map (f ≫ f')).obj j = (StructuredArrow.map f).obj ((StructuredArrow.map f').obj j)

Tactic:
apply StructuredArrow.map_comp

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
inst✝ : L.HasPointwiseRightKanExtension F
G : D ⥤ H
α : L ⋙ G ⟶ F
Y : D
⊢ ((L.pointwiseRightKanExtension F).liftOfIsRightKanExtension (L.pointwiseRightKanExtensionCounit F) G α).app Y =
    limit.lift (StructuredArrow.proj Y L ⋙ F) (L.structuredArrowMapCone F G α Y)

Tactic:
let β : G ⟶ L.pointwiseRightKanExtension F :=
    { app := fun Y ↦ limit.lift _ (structuredArrowMapCone L F G α Y) }

Goal state after:
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
inst✝ : L.HasPointwiseRightKanExtension F
G : D ⥤ H
α : L ⋙ G ⟶ F
Y : D
β : G ⟶ L.pointwiseRightKanExtension F :=
  { app := fun Y ↦ limit.lift (StructuredArrow.proj Y L ⋙ F) (L.structuredArrowMapCone F G α Y), naturality := ⋯ }
⊢ ((L.pointwiseRightKanExtension F).liftOfIsRightKanExtension (L.pointwiseRightKanExtensionCounit F) G α).app Y =
    limit.lift (StructuredArrow.proj Y L ⋙ F) (L.structuredArrowMapCone F G α Y)
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'
L : C ⥤ D
L' : D ⥤ D'
F₀ : C ⥤ H
F₁ : D ⥤ H
F₂ : D' ⥤ H
α : F₀ ⟶ L ⋙ F₁
hα : StructuredArrow.IsUniversal (mk F₁ α)
b : L'.LeftExtension F₁
hb : StructuredArrow.IsUniversal ((precomp₂ L' α).obj b)
y : L'.LeftExtension F₁
u : (precomp₂ L' α).obj b ⟶ (precomp₂ L' α).obj y := IsInitial.to hb ((precomp₂ L' α).obj y)
t : C
this :
  (StructuredArrow.hom ((precomp₂ L' α).obj b) ≫
          ((whiskeringLeft C D' H).obj (L ⋙ L')).map (StructuredArrow.Hom.right u)).app
      t =
    (StructuredArrow.hom ((precomp₂ L' α).obj y)).app t
⊢ (StructuredArrow.hom (mk F₁ α) ≫
          ((whiskeringLeft C D H).obj L).map
            (StructuredArrow.hom b ≫ ((whiskeringLeft D D' H).obj L').map (StructuredArrow.Hom.right u))).app
      t =
    (StructuredArrow.hom (mk F₁ α) ≫ ((whiskeringLeft C D H).obj L).map (StructuredArrow.hom y)).app t

Tactic:
dsimp at 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'
L : C ⥤ D
L' : D ⥤ D'
F₀ : C ⥤ H
F₁ : D ⥤ H
F₂ : D' ⥤ H
α : F₀ ⟶ L ⋙ F₁
hα : StructuredArrow.IsUniversal (mk F₁ α)
b : L'.LeftExtension F₁
hb : StructuredArrow.IsUniversal ((precomp₂ L' α).obj b)
y : L'.LeftExtension F₁
u : (precomp₂ L' α).obj b ⟶ (precomp₂ L' α).obj y := IsInitial.to hb ((precomp₂ L' α).obj y)
t : C
this :
  (StructuredArrow.hom ((precomp₂ L' α).obj b)).app t ≫ (StructuredArrow.Hom.right u).app (L'.obj (L.obj t)) =
    (StructuredArrow.hom ((precomp₂ L' α).obj y)).app t
⊢ (StructuredArrow.hom (mk F₁ α) ≫
          ((whiskeringLeft C D H).obj L).map
            (StructuredArrow.hom b ≫ ((whiskeringLeft D D' H).obj L').map (StructuredArrow.Hom.right u))).app
      t =
    (StructuredArrow.hom (mk F₁ α) ≫ ((whiskeringLeft C D H).obj L).map (StructuredArrow.hom y)).app t
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'
L : C ⥤ D
L' : D ⥤ D'
F₀ : C ⥤ H
F₁ : D ⥤ H
F₂ : D' ⥤ H
α : F₀ ⟶ L ⋙ F₁
hα : StructuredArrow.IsUniversal (mk F₁ α)
b : L'.LeftExtension F₁
hb : StructuredArrow.IsUniversal ((precomp₂ L' α).obj b)
y : L'.LeftExtension F₁
u : (precomp₂ L' α).obj b ⟶ (precomp₂ L' α).obj y := IsInitial.to hb ((precomp₂ L' α).obj y)
a : b ⟶ y
t : C
this :
  (StructuredArrow.hom ((precomp₂ L' α).obj b) ≫
          ((whiskeringLeft C D' H).obj (L ⋙ L')).map (StructuredArrow.Hom.right u)).app
      t =
    (StructuredArrow.hom ((precomp₂ L' α).obj y)).app t
⊢ (StructuredArrow.hom ((precomp₂ L' α).obj b) ≫
          ((whiskeringLeft C D' H).obj (L ⋙ L')).map (StructuredArrow.Hom.right a)).app
      t =
    (StructuredArrow.hom ((precomp₂ L' α).obj b) ≫
          ((whiskeringLeft C D' H).obj (L ⋙ L')).map (StructuredArrow.Hom.right default)).app
      t

Tactic:
dsimp at 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'
L : C ⥤ D
L' : D ⥤ D'
F₀ : C ⥤ H
F₁ : D ⥤ H
F₂ : D' ⥤ H
α : F₀ ⟶ L ⋙ F₁
hα : StructuredArrow.IsUniversal (mk F₁ α)
b : L'.LeftExtension F₁
hb : StructuredArrow.IsUniversal ((precomp₂ L' α).obj b)
y : L'.LeftExtension F₁
u : (precomp₂ L' α).obj b ⟶ (precomp₂ L' α).obj y := IsInitial.to hb ((precomp₂ L' α).obj y)
a : b ⟶ y
t : C
this :
  (StructuredArrow.hom ((precomp₂ L' α).obj b)).app t ≫ (StructuredArrow.Hom.right u).app (L'.obj (L.obj t)) =
    (StructuredArrow.hom ((precomp₂ L' α).obj y)).app t
⊢ (StructuredArrow.hom ((precomp₂ L' α).obj b) ≫
          ((whiskeringLeft C D' H).obj (L ⋙ L')).map (StructuredArrow.Hom.right a)).app
      t =
    (StructuredArrow.hom ((precomp₂ L' α).obj b) ≫
          ((whiskeringLeft C D' H).obj (L ⋙ L')).map (StructuredArrow.Hom.right default)).app
      t
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✝ : ℰᵒᵖ ⥤ Type (max w v₁ v₂)
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₂)
X Y : ℰ
f : L.obj P ⟶ X
g : X ⟶ Y
this :
  ∀ {W W' : ℰ}
    (f :
      CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A ⟶
        (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)).obj W)
    (g : W ⟶ W'),
    (IsColimit.homEquiv (Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension L α P)).symm
        (f ≫ (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)).map g) =
      (IsColimit.homEquiv (Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension L α P)).symm f ≫ g
⊢ (restrictedULiftYonedaHomEquiv L α P Y) (f ≫ g) =
    (restrictedULiftYonedaHomEquiv L α P X) f ≫ (restrictedULiftYoneda A).map g

Tactic:
dsimp at this

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝² : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
P✝ : ℰᵒᵖ ⥤ Type (max w v₁ v₂)
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₂)
X Y : ℰ
f : L.obj P ⟶ X
g : X ⟶ Y
this :
  ∀ {W W' : ℰ}
    (f :
      CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A ⟶
        (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)).obj W)
    (g : W ⟶ W'),
    (IsColimit.homEquiv (Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension L α P)).symm
        (f ≫ (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)).map g) =
      (IsColimit.homEquiv (Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension L α P)).symm f ≫ g
⊢ (restrictedULiftYonedaHomEquiv L α P Y) (f ≫ g) =
    (restrictedULiftYonedaHomEquiv L α P X) f ≫ (restrictedULiftYoneda A).map g
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:
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.Generator.Basic

Goal state before:
pp: case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
G : C
inst✝ : ∀ (A : C), HasCoproduct fun x ↦ G
h : ∀ (A : C), Epi (Sigma.desc fun f ↦ f)
X Y : C
f g : X ⟶ Y
hh : ∀ (h : G ⟶ X), h ≫ f = h ≫ g
this : Epi (Sigma.desc fun f ↦ f)
⊢ f = g

Tactic:
refine (cancel_epi (Sigma.desc fun f : G ⟶ X => f)).1 (colimit.hom_ext fun j => ?_)

Goal state after:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
G : C
inst✝ : ∀ (A : C), HasCoproduct fun x ↦ G
h : ∀ (A : C), Epi (Sigma.desc fun f ↦ f)
X Y : C
f g : X ⟶ Y
hh : ∀ (h : G ⟶ X), h ≫ f = h ≫ g
this : Epi (Sigma.desc fun f ↦ f)
j : Discrete (G ⟶ X)
⊢ colimit.ι (Discrete.functor fun f ↦ G) j ≫ (Sigma.desc fun f ↦ f) ≫ f =
    colimit.ι (Discrete.functor fun f ↦ G) j ≫ (Sigma.desc fun f ↦ f) ≫ g
Module: Mathlib.Algebra.Category.Grp.AB

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
⊢ ∃ G, IsSeparator G

Tactic:
use AddCommGrpCat.of (ULift ℤ)
    intro A B f g h; simp_all only [ObjectProperty.singleton_iff, AddCommGrpCat.ext_iff,
      AddCommGrpCat.hom_comp, AddMonoidHom.coe_comp, Function.comp_apply, forall_eq', ULift.forall]
    (intro x; specialize h (AddCommGrpCat.ofHom
    (AddMonoidHom.mk' (fun y => y • x) fun y z => by simp only [add_smul])) 1; aesop)

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)
⊢ Function.Injective
    (((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)))

Tactic:
have (u : G.ColimitType) (x : F.obj X) (h : G.descColimitType c u = x) :
        G.ιColimitType (op (elementsMk _ _ x))
          (shrinkYonedaObjObjEquiv.symm (𝟙 X)) = u := by
      obtain ⟨⟨u⟩, v, rfl⟩ := Functor.ιColimitType_jointly_surjective _ u
      obtain ⟨v, rfl⟩ := shrinkYonedaObjObjEquiv.symm.surjective v
      dsimp [c] at v h
      simp only [Equiv.apply_symm_apply] at h
      rw [← G.ιColimitType_map (show u ⟶ F.elementsMk _ x from ⟨v, h⟩).op]
      simp [G, shrinkYoneda_obj_map_shrinkYonedaObjObjEquiv_symm.{w}]

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
⊢ Function.Injective
    (((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)))
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: C : Type u
F : C → Type v
c : CofanTypes F
hc : Functor.CoconeTypes.IsColimit c
i : C
⊢ Function.Injective (c.inj i)

Tactic:
intro y₁ y₂ h

Goal state after:
C : Type u
F : C → Type v
c : CofanTypes F
hc : Functor.CoconeTypes.IsColimit c
i : C
y₁ y₂ : F i
h : c.inj i y₁ = c.inj i y₂
⊢ y₁ = y₂
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: case mp
X : Type u
⊢ Nonempty (IsInitial X) → IsEmpty X

pp: case mpr
X : Type u
⊢ IsEmpty X → Nonempty (IsInitial X)

Tactic:
· intro ⟨h⟩
    exact Function.isEmpty (IsInitial.to h PEmpty)

Goal state after:
case mpr
X : Type u
⊢ IsEmpty X → Nonempty (IsInitial X)
Module: Mathlib.Order.Circular

Goal state before:
pp: case inr.inr.inr.inr
α : Type u_1
inst✝ : Preorder α
a b c d : α
hca : c < a
hab : a < b
hcb : c < b
hbd : b < d
⊢ a < d ∧ d < c ∨ d < c ∧ c < a ∨ c < a ∧ a < d

Tactic:
refine .inr <| .inr ?_; constructor <;> order

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

Goal state before:
pp: n : ℕ
m : ↑{m | m < n ∧ n.Coprime m}
⊢ (fun m ↦ ⟨↑m, ⋯⟩) ((fun m ↦ ⟨↑m, ⋯⟩) m) = m

Tactic:
by simp only [Subtype.coe_eta]

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

Goal state before:
pp: n : ℕ
⊢ (1 % (n + 1)).gcd (n + 1) = 1

Tactic:
← gcd_rec,

Goal state after:
n : ℕ
⊢ (n + 1).gcd 1 = 1
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case zero
a k n : ℕ
a_ne_zero : a ≠ 0
⊢ #({x ∈ Ico k (k + n % a) | a.Coprime x}) ≤ #({x ∈ Ico k (k + a) | a.Coprime x})

Tactic:
gcongr

Goal state after:
case h₂
a k n : ℕ
a_ne_zero : a ≠ 0
⊢ n % a ≤ a
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: a k n : ℕ
a_ne_zero : a ≠ 0
i : ℕ
ih : #({x ∈ Ico k (k + n % a + a * i) | a.Coprime x}) ≤ φ a * (i + 1)
⊢ #({x ∈ Ico k (k + n % a + a * i + a) | a.Coprime x}) ≤
    #({x ∈ Ico k (k + n % a + a * i) ∪ Ico (k + n % a + a * i) (k + n % a + a * i + a) | a.Coprime x})

Tactic:
gcongr

Goal state after:
case h
a k n : ℕ
a_ne_zero : a ≠ 0
i : ℕ
ih : #({x ∈ Ico k (k + n % a + a * i) | a.Coprime x}) ≤ φ a * (i + 1)
⊢ Ico k (k + n % a + a * i + a) ⊆ Ico k (k + n % a + a * i) ∪ Ico (k + n % a + a * i) (k + n % a + a * i + a)
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: d : ℕ
hd0 : d > 0
x a : ℕ
ha1 : a < x
ha2 : x.gcd a = 1
⊢ d * a < d * x

Tactic:
gcongr

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

Goal state before:
pp: n : ℕ
⊢ Odd (φ n) ↔ φ n = 1

Tactic:
simp [Nat.odd_totient_iff, Nat.totient_eq_one_iff]

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated

Goal state before:
pp: α : Type u_1
ι : Type u_3
x : ι → α
f : Filter α
l : Filter ι
inst✝ : l.IsCountablyGenerated
hxy : ¬Tendsto x l f
⊢ ∃ s ∈ f, ∃ᶠ (n : ι) in l, x n ∉ s

Tactic:
by
    rwa [not_tendsto_iff_exists_frequently_notMem] at hxy

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 : α
m : ℤ
⊢ toIcoMod hp (a + m • p) b = toIcoMod hp a b + m • p

Tactic:
by
  simp only [toIcoMod, toIcoDiv_add_zsmul', sub_smul, sub_add]

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsOpen s
⊢ s ∩ frontier s = ∅

Tactic:
by
  rw [hs.frontier_eq, inter_sdiff_self]

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
⊢ ∀ i ∈ {s | a ∈ s ∧ IsOpen[generateFrom g] s}, ⨅ s ∈ {s | a ∈ s ∧ s ∈ g}, 𝓟 s ≤ 𝓟 i

Tactic:
rintro s ⟨ha, hs⟩

Goal state after:
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s : Set α
ha : a ∈ s
hs : IsOpen[generateFrom g] s
⊢ ⨅ s ∈ {s | a ∈ s ∧ s ∈ g}, 𝓟 s ≤ 𝓟 s