mathlib-initiative/mathlib-tactics huggingface dataset:
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₁.HasRightHomology
inst✝² : S₂.HasRightHomology
inst✝¹ : F.PreservesRightHomologyOf S₁
inst✝ : F.PreservesRightHomologyOf S₂
⊢ rightHomologyMap (F.mapShortComplex.map φ) ≫ 𝟙 (F.mapShortComplex.obj S₂).rightHomology =
    (S₁.mapRightHomologyIso F).hom ≫ (S₁.mapRightHomologyIso F).inv ≫ rightHomologyMap (F.mapShortComplex.map φ)

Tactic:
comp_id,

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Category.{v_2, u_2} D
inst✝⁶ : HasZeroMorphisms C
inst✝⁵ : HasZeroMorphisms D
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : S₁.HasRightHomology
inst✝² : S₂.HasRightHomology
inst✝¹ : F.PreservesRightHomologyOf S₁
inst✝ : F.PreservesRightHomologyOf S₂
⊢ rightHomologyMap (F.mapShortComplex.map φ) =
    (S₁.mapRightHomologyIso F).hom ≫ (S₁.mapRightHomologyIso F).inv ≫ rightHomologyMap (F.mapShortComplex.map φ)
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₂
⊢ homologyMap (F.mapShortComplex.map φ) ≫ 𝟙 (S₂.map F).homology =
    (S₁.mapHomologyIso F).hom ≫ (S₁.mapHomologyIso F).inv ≫ homologyMap (F.mapShortComplex.map φ)

Tactic:
comp_id,

Goal state after:
C : Type u_1
D : Type u_2
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
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₂
⊢ homologyMap (F.mapShortComplex.map φ) =
    (S₁.mapHomologyIso F).hom ≫ (S₁.mapHomologyIso F).inv ≫ homologyMap (F.mapShortComplex.map φ)
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.PreservesRightHomologyOf S₁
inst✝ : F.PreservesRightHomologyOf S₂
⊢ homologyMap (F.mapShortComplex.map φ) ≫ 𝟙 (S₂.map F).homology =
    (S₁.mapHomologyIso' F).hom ≫ (S₁.mapHomologyIso' F).inv ≫ homologyMap (F.mapShortComplex.map φ)

Tactic:
comp_id,

Goal state after:
C : Type u_1
D : Type u_2
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
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.PreservesRightHomologyOf S₁
inst✝ : F.PreservesRightHomologyOf S₂
⊢ homologyMap (F.mapShortComplex.map φ) =
    (S₁.mapHomologyIso' F).hom ≫ (S₁.mapHomologyIso' F).inv ≫ homologyMap (F.mapShortComplex.map φ)
Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic

Goal state before:
pp: case pos
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : Type u₁
inst✝ : Nonempty X
X✝ Y✝ : Type u₁
g : X✝ ⟶ X
f : X✝ ⟶ Y✝
mono : Mono f
y : X✝
h : (ConcreteCategory.hom f) y ∈ Set.range ⇑(ConcreteCategory.hom f)
⊢ (ConcreteCategory.hom g) (Classical.choose h) = (ConcreteCategory.hom g).toFun y

pp: case neg
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : Type u₁
inst✝ : Nonempty X
X✝ Y✝ : Type u₁
g : X✝ ⟶ X
f : X✝ ⟶ Y✝
mono : Mono f
y : X✝
h : (ConcreteCategory.hom f) y ∉ Set.range ⇑(ConcreteCategory.hom f)
⊢ ⋯.some = (ConcreteCategory.hom g).toFun y

Tactic:
· rw [mono_iff_injective] at mono
        simp [mono (Classical.choose_spec h)]

Goal state after:
case neg
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : Type u₁
inst✝ : Nonempty X
X✝ Y✝ : Type u₁
g : X✝ ⟶ X
f : X✝ ⟶ Y✝
mono : Mono f
y : X✝
h : (ConcreteCategory.hom f) y ∉ Set.range ⇑(ConcreteCategory.hom f)
⊢ ⋯.some = (ConcreteCategory.hom g).toFun y
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
F G : C ⥤ D
τ : F ⟶ G
S : ShortComplex C
inst✝⁶ : S.HasHomology
inst✝⁵ : F.PreservesZeroMorphisms
inst✝⁴ : G.PreservesZeroMorphisms
inst✝³ : F.PreservesLeftHomologyOf S
inst✝² : G.PreservesLeftHomologyOf S
inst✝¹ : F.PreservesRightHomologyOf S
inst✝ : G.PreservesRightHomologyOf S
⊢ τ.app S.homology = (S.mapHomologyIso F).inv ≫ (S.mapHomologyIso F).hom ≫ τ.app S.homology ≫ 𝟙 (G.obj S.homology)

Tactic:
comp_id,

Goal state after:
C : Type u_1
D : Type u_2
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : HasZeroMorphisms C
inst✝⁷ : HasZeroMorphisms D
F G : C ⥤ D
τ : F ⟶ G
S : ShortComplex C
inst✝⁶ : S.HasHomology
inst✝⁵ : F.PreservesZeroMorphisms
inst✝⁴ : G.PreservesZeroMorphisms
inst✝³ : F.PreservesLeftHomologyOf S
inst✝² : G.PreservesLeftHomologyOf S
inst✝¹ : F.PreservesRightHomologyOf S
inst✝ : G.PreservesRightHomologyOf S
⊢ τ.app S.homology = (S.mapHomologyIso F).inv ≫ (S.mapHomologyIso F).hom ≫ τ.app S.homology
Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact

Goal state before:
pp: case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
e : S₁ ≅ S₂
⊢ S₂.ShortExact → S₁.ShortExact

Tactic:
· exact shortExact_of_iso e.symm

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

Goal state before:
pp: S : ShortComplex Ab
x : ↑S.X₁
⊢ ∃ x_1,
    S.abToCycles x_1 = (AddCommGrpCat.Hom.hom ((AddCommGrpCat.kernelIsLimit S.g).lift (Limits.KernelFork.ofι S.f ⋯))) x

Tactic:
apply exists_apply_eq_apply

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

Goal state before:
pp: S : ShortComplex Ab
x : ↥(AddCommGrpCat.Hom.hom S.g).ker
⊢ (ConcreteCategory.hom S.iCycles) ((ConcreteCategory.hom S.abCyclesIso.inv) x) = ↑x

Tactic:
dsimp only [abCyclesIso]

Goal state after:
S : ShortComplex Ab
x : ↥(AddCommGrpCat.Hom.hom S.g).ker
⊢ (ConcreteCategory.hom S.iCycles) ((ConcreteCategory.hom S.abLeftHomologyData.cyclesIso.inv) x) = ↑x
Module: Mathlib.CategoryTheory.Adjunction.Reflective

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
i : D ⥤ C
inst✝ : Reflective i
A : C
h : i.essImage A
⊢ IsIso ((reflectorAdjunction i).unit.app A)

Tactic:
by
  rwa [isIso_unit_app_iff_mem_essImage]

Goal state after:
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
f : X ⟶ Y
inst✝ : Mono f
g h : MonoOver X
e : (map f).obj g ⟶ (map f).obj h
⊢ ∃ a, (map f).map a = e

Tactic:
refine ⟨homMk e.hom.left ?_, rfl⟩
    · rw [← cancel_mono f, assoc]
      apply w e

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : X ≅ Y
g : Subobject X
⊢ (map e.inv).obj ((map e.hom).obj g) = g

Tactic:
by simp_rw [← map_comp, e.hom_inv_id, map_id]

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

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✝¹ : Preadditive C
inst✝ : Balanced C
S : ShortComplex C
hS : S.Exact
s : S.X₃ ⟶ S.X₂
s_g : s ≫ S.g = 𝟙 S.X₃
hf : Mono S.f
⊢ S.f ≫ 𝟙 S.X₂ - S.f ≫ S.g ≫ s = 𝟙 S.X₁ ≫ S.f

Tactic:
comp_id,

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preadditive C
inst✝ : Balanced C
S : ShortComplex C
hS : S.Exact
s : S.X₃ ⟶ S.X₂
s_g : s ≫ S.g = 𝟙 S.X₃
hf : Mono S.f
⊢ S.f - S.f ≫ S.g ≫ s = 𝟙 S.X₁ ≫ S.f
Module: Mathlib.CategoryTheory.Abelian.Exact

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
⊢ Arrow.mk (imageToKernel' S.f S.g ⋯) ≅ Arrow.mk (imageToKernel S.f S.g ⋯)

Tactic:
exact Arrow.isoMk (imageSubobjectIso S.f).symm (kernelSubobjectIso S.g).symm

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✝⁶ : Preadditive C
inst✝⁵ : Preadditive D
F : C ⥤ D
inst✝⁴ : F.Additive
inst✝³ : F.PreservesHomology
inst✝² : HasZeroObject C
inst✝¹ : HasFiniteProducts C
inst✝ : HasKernels C
this✝ : ∀ {X Y : C} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
this : HasBinaryBiproducts C
⊢ PreservesFiniteLimits F

Tactic:
have : HasEqualizers C := Preadditive.hasEqualizers_of_hasKernels

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Category.{v_2, u_2} D
inst✝⁶ : Preadditive C
inst✝⁵ : Preadditive D
F : C ⥤ D
inst✝⁴ : F.Additive
inst✝³ : F.PreservesHomology
inst✝² : HasZeroObject C
inst✝¹ : HasFiniteProducts C
inst✝ : HasKernels C
this✝¹ : ∀ {X Y : C} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
this✝ : HasBinaryBiproducts C
this : HasEqualizers C
⊢ PreservesFiniteLimits F
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
hF : ∀ (S : ShortComplex C), S.ShortExact → (S.map F).Exact ∧ Mono (F.map S.f)
S : ShortComplex C
hS : S.Exact
hf : Mono S.f
this : F.PreservesMonomorphisms
T : ShortComplex C :=
  { X₁ := S.X₁, X₂ := S.X₂, X₃ := Abelian.coimage S.g, f := S.f, g := Abelian.coimage.π S.g, zero := ⋯ }
⊢ (S.map F).Exact

Tactic:
let φ : T.map F ⟶ S.map F :=
      { τ₁ := 𝟙 _
        τ₂ := 𝟙 _
        τ₃ := F.map <| Abelian.factorThruCoimage S.g
        comm₂₃ := show 𝟙 _ ≫ F.map _ = F.map (cokernel.π _) ≫ _ by
          rw [Category.id_comp, ← F.map_comp, cokernel.π_desc] }

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Abelian C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
hF : ∀ (S : ShortComplex C), S.ShortExact → (S.map F).Exact ∧ Mono (F.map S.f)
S : ShortComplex C
hS : S.Exact
hf : Mono S.f
this : F.PreservesMonomorphisms
T : ShortComplex C :=
  { X₁ := S.X₁, X₂ := S.X₂, X₃ := Abelian.coimage S.g, f := S.f, g := Abelian.coimage.π S.g, zero := ⋯ }
φ : T.map F ⟶ S.map F :=
  { τ₁ := 𝟙 (T.map F).X₁, τ₂ := 𝟙 (T.map F).X₂, τ₃ := F.map (Abelian.factorThruCoimage S.g), comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ (S.map F).Exact
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
e : (Discrete.functor fun x ↦ Opposite.op (Z x)) ≅ (Discrete.opposite α).inverse ⋙ (Discrete.functor Z).op :=
  Discrete.natIso fun x ↦ Iso.refl ((Discrete.functor fun x ↦ Opposite.op (Z x)).obj x)
⊢ IsLimit c.op

Tactic:
refine IsLimit.ofIsoLimit ((IsLimit.postcomposeInvEquiv e _).2
    (IsLimit.whiskerEquivalence hc.op (Discrete.opposite α).symm))
    (Cone.ext (Iso.refl _) (fun ⟨a⟩ ↦ ?_))

Goal state after:
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
e : (Discrete.functor fun x ↦ Opposite.op (Z x)) ≅ (Discrete.opposite α).inverse ⋙ (Discrete.functor Z).op :=
  Discrete.natIso fun x ↦ Iso.refl ((Discrete.functor fun x ↦ Opposite.op (Z x)).obj x)
x✝ : Discrete α
a : α
⊢ ((Cone.postcompose e.inv).obj (Cone.whisker (Discrete.opposite α).symm.functor (Cocone.op c))).π.app { as := a } =
    (Iso.refl ((Cone.postcompose e.inv).obj (Cone.whisker (Discrete.opposite α).symm.functor (Cocone.op c))).pt).hom ≫
      c.op.π.app { as := a }
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
f f' : Fan Z
c : Cofan fun x ↦ op (Z x)
hf : IsLimit f
hf' : IsLimit f'
hc : IsColimit c
⊢ (opProductIsoCoproduct' hf hc).hom ≫ (opProductIsoCoproduct' hf' hc).inv = (hf.conePointUniqueUpToIso hf').op.inv

Tactic:
by
  apply Quiver.Hom.unop_inj
  apply hf.hom_ext
  intro ⟨j⟩
  change _ ≫ f.proj _ = _
  simp only [unop_op, unop_comp, Category.assoc, Discrete.functor_obj, Iso.op_inv,
    Quiver.Hom.unop_op, IsLimit.conePointUniqueUpToIso_inv_comp]
  apply Quiver.Hom.op_inj
  simp only [op_comp, op_unop, Quiver.Hom.op_unop, proj_comp_opProductIsoCoproduct'_hom]
  rw [← proj_comp_opProductIsoCoproduct'_hom hf' hc]
  simp only [Category.assoc, Iso.hom_inv_id, Category.comp_id]
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Functor

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T : C ⥤ D
d : D
⊢ (map (𝟙 d)).toCatHom.toFunctor = (𝟙 (Cat.of (CostructuredArrow T d))).toFunctor

Tactic:
exact Functor.ext (fun ⟨_, _, _⟩ => by simp [CostructuredArrow.map, Comma.mapRight])

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

Goal state before:
pp: C : Type u_1
H : Type u_3
D : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_3, u_3} H
inst✝ : Category.{v_4, u_4} D
F' F'' : D ⥤ H
e : F' ≅ F''
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
α' : L ⋙ F'' ⟶ F
comm : L.whiskerLeft e.hom ≫ α' = α
⊢ F'.IsRightKanExtension α ↔ F''.IsRightKanExtension α'

Tactic:
by
  constructor
  · intro
    exact isRightKanExtension_of_iso e α α' comm
  · intro
    refine isRightKanExtension_of_iso e.symm α' α ?_
    rw [← comm, ← whiskerLeft_comp_assoc, Iso.symm_hom, e.inv_hom_id, whiskerLeft_id', id_comp]

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
X : D
j : StructuredArrow X L
⊢ j = StructuredArrow.mk (j.hom ≫ 𝟙 (L.obj j.right))

Tactic:
comp_id,

Goal state after:
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
X : D
j : StructuredArrow X L
⊢ j = StructuredArrow.mk j.hom
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
y y' : CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P
f : y ⟶ y'
⊢ A.map f.left ≫ (uliftYonedaEquiv (y'.hom ≫ g)).down = (uliftYonedaEquiv (y.hom ≫ g)).down ≫ 𝟙 E

Tactic:
comp_id,

Goal state after:
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
y y' : CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P
f : y ⟶ y'
⊢ A.map f.left ≫ (uliftYonedaEquiv (y'.hom ≫ g)).down = (uliftYonedaEquiv (y.hom ≫ g)).down
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₁)
x₁ x₂ : P.Elementsᵒᵖ
f : x₁ ⟶ x₂
⊢ uliftYoneda.{w, v₁, u₁}.map (↑f.unop).unop ≫ uliftYonedaEquiv.symm (unop x₂).snd =
    uliftYonedaEquiv.symm (unop x₁).snd ≫ 𝟙 P

Tactic:
comp_id,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝ : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type (max w v₁)
x₁ x₂ : P.Elementsᵒᵖ
f : x₁ ⟶ x₂
⊢ uliftYoneda.{w, v₁, u₁}.map (↑f.unop).unop ≫ uliftYonedaEquiv.symm (unop x₂).snd = uliftYonedaEquiv.symm (unop x₁).snd
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasLimitsOfSize.{w, w, v₁, u₁} C
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v₁, u₁} P
hP : P.IsCoseparating
this✝⁴ : HasFiniteLimits C
this✝³ : HasProductsOfShape (Subtype P) C
this✝² : ∀ (A : C), HasProductsOfShape (StructuredArrow A P.ι) C
this✝¹ : CompleteLattice (Subobject (∏ᶜ Subtype.val)) :=
  completeLatticeOfCompleteSemilatticeInf (Subobject (∏ᶜ Subtype.val))
this✝ : ∀ (X : C) [inst : HasProduct (P.productToFamily X)], Mono (P.productTo X)
A : C
f : Subobject.underlying.obj ⊥ ⟶ A
this : ∀ (g : Subobject.underlying.obj ⊥ ⟶ A), f = g
⊢ f = default

Tactic:
apply this

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : NonAssocRing α
inst✝ : InvolutiveNeg β
h : Antiperiodic f c
n : ℤ
x : α
⊢ f (x + (↑n * (2 * c) + c)) = -f x

Tactic:
rw [← add_assoc, h, h.int_even_mul_periodic]

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Induction

Goal state before:
pp: case convert_1
a b m n✝ p✝ : ℕ
motive : ℕ → Sort u_1
zero : motive 0
one : motive 1
prime_pow_mul : (a p n : ℕ) → Prime p → ¬p ∣ a → 0 < n → motive a → motive (p ^ n * a)
n k : ℕ
hk : (m : ℕ) → m < k + 2 → motive m
p : ℕ := (k + 2).minFac
hp : Prime p
t : ℕ := (k + 2).factorization p
hpt : p ^ t ∣ k + 2
htp : 0 < t
⊢ ¬p ∣ (k + 2) / p ^ t

Tactic:
rw [Nat.dvd_div_iff_mul_dvd hpt, ← Nat.pow_succ]

Goal state after:
case convert_1
a b m n✝ p✝ : ℕ
motive : ℕ → Sort u_1
zero : motive 0
one : motive 1
prime_pow_mul : (a p n : ℕ) → Prime p → ¬p ∣ a → 0 < n → motive a → motive (p ^ n * a)
n k : ℕ
hk : (m : ℕ) → m < k + 2 → motive m
p : ℕ := (k + 2).minFac
hp : Prime p
t : ℕ := (k + 2).factorization p
hpt : p ^ t ∣ k + 2
htp : 0 < t
⊢ ¬p ^ t.succ ∣ k + 2
Module: Mathlib.Data.Nat.Factorization.Induction

Goal state before:
pp: case pos
a✝ b m n✝ p✝ : ℕ
motive : ℕ → Sort u_1
prime_pow : (p n : ℕ) → Prime p → 0 < n → motive (p ^ n)
zero : motive 0
one : motive 1
coprime : (a b : ℕ) → 1 < a → 1 < b → a.Coprime b → motive a → motive b → motive (a * b)
a p n : ℕ
hp' : Prime p
hpa : ¬p ∣ a
hn : 0 < n
hPa : motive a
ha1 : a = 1
⊢ motive (p ^ n * a)

Tactic:
rw [ha1, mul_one]
      exact prime_pow p n hp' hn

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:
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 : ℕ
hn : 2 < n
this✝ : Fact (1 < n)
this : NeZero n
⊢ 2 = orderOf (-1)

Tactic:
rw [← orderOf_units, Units.coe_neg_one, orderOf_neg_one, ringChar.eq (ZMod n) n, if_neg hn.ne']

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

Goal state before:
pp: ι : Type u_3
l : Filter ι
p : ι → Prop
inst✝ : l.IsCountablyGenerated
⊢ (∃ᶠ (n : ι) in l, p n) ↔ ∃ x, Tendsto x atTop l ∧ ∃ᶠ (n : ℕ) in atTop, p (x n)

Tactic:
simp only [Filter.Frequently, eventually_iff_seq_eventually (l := l)]

Goal state after:
ι : Type u_3
l : Filter ι
p : ι → Prop
inst✝ : l.IsCountablyGenerated
⊢ (¬∀ (x : ℕ → ι), Tendsto x atTop l → ∀ᶠ (n : ℕ) in atTop, ¬p (x n)) ↔
    ∃ x, Tendsto x atTop l ∧ ¬∀ᶠ (x_1 : ℕ) in atTop, ¬p (x x_1)
Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated

Goal state before:
pp: ι : Type u_3
l : Filter ι
p : ι → Prop
inst✝ : l.IsCountablyGenerated
h : ∃ x, Tendsto x atTop l ∧ ∃ᶠ (n : ℕ) in atTop, p (x n)
⊢ ∃ ns, Tendsto ns atTop l ∧ ∀ (n : ℕ), p (ns n)

Tactic:
obtain ⟨x, hx_tendsto, hx_freq⟩ := h

Goal state after:
ι : Type u_3
l : Filter ι
p : ι → Prop
inst✝ : l.IsCountablyGenerated
x : ℕ → ι
hx_tendsto : Tendsto x atTop l
hx_freq : ∃ᶠ (n : ℕ) in atTop, p (x n)
⊢ ∃ ns, Tendsto ns atTop l ∧ ∀ (n : ℕ), p (ns n)
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case H
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ (∏ p ∈ a.primeFactors, p) * ∏ p ∈ b.primeFactors, p ∣ a * b

Tactic:
exact mul_dvd_mul (prod_primeFactors_dvd a) (prod_primeFactors_dvd b)

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

Goal state before:
pp: case pos
a b : ℕ
h : a ∣ b
h' : a = 0
ha : ¬a = 0
hb : b = 0
⊢ a = b ∨ 2 * a = b

Tactic:
exact False.elim (ha h')

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

Tactic:
toIocDiv_add_zsmul,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIocDiv hp a b + m = m + toIocDiv hp a b
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 : ℤ
⊢ toIocDiv hp a (b + -m • p) = toIocDiv hp a b - m

Tactic:
toIocDiv_add_zsmul,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIocDiv hp a b + -m = toIocDiv hp a b - m
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 : ℤ
⊢ b + m • p - toIocDiv hp a (b + m • p) • p = toIocMod hp a b

Tactic:
toIocDiv_add_zsmul,

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
S : Set (Set X)
hS : S.Finite
⊢ closure (⋃ i ∈ S, i) = ⋃ s ∈ S, closure s

Tactic:
hS.closure_biUnion

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
S : Set (Set X)
hS : S.Finite
⊢ ⋃ i ∈ S, closure i = ⋃ s ∈ S, closure s
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 : α
⊢ toIcoMod hp a b ≤ toIocMod hp a b

Tactic:
rw [toIcoMod, toIocMod, sub_le_sub_iff_left]

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocDiv hp a b • p ≤ toIcoDiv hp a b • p