mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X : C
⊢ cokernel.π (diag X) ≫ (asIso (r X)).symm.hom = σ

Tactic:
by rw [Iso.symm_hom, asIso_inv]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteCoproducts C
inst✝¹ : HasCokernels C
inst✝ : IsNormalEpiCategory C
X Y : C
f g : X ⟶ Y
huv : pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g) = pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g)
hvu :
  f ≫ pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g) =
    g ≫ pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g)
huu :
  f ≫ pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g) =
    g ≫ pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g)
s : Cofork f g
⊢ (Cofork.ofπ (pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g)) huu).π ≫ pushout.desc s.π s.π ⋯ = s.π

Tactic:
by simp only [pushout.inl_desc, Cofork.π_ofπ]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Category.{v_3, u_3} E
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
inst✝ : HasZeroMorphisms E
S S₁✝ S₂✝ S₃ : ShortComplex C
S₁ S₂ : ShortComplex Cᵒᵖ
φ : S₁ ⟶ S₂
⊢ φ.τ₂.unop ≫ S₁.unop.g = S₂.unop.g ≫ φ.τ₁.unop

Tactic:
by
    dsimp
    simp only [← unop_comp, φ.comm₁₂]

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

Goal state before:
pp: A B : GrpCat
f✝ : A ⟶ B
X✝ Y✝ : GrpCat
f : X✝ ⟶ Y✝
e : Mono f
⊢ Mono ((forget GrpCat).map f)

Tactic:
rwa [mono_iff_injective, ← CategoryTheory.ofHom_mono_iff_injective] at e

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

Goal state before:
pp: A B : CommGrpCat
f✝ : A ⟶ B
X✝ Y✝ : CommGrpCat
f : X✝ ⟶ Y✝
e : Mono f
⊢ Mono ((forget CommGrpCat).map f)

Tactic:
rwa [mono_iff_injective, ← CategoryTheory.ofHom_mono_iff_injective] at e

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.RightHomologyData
hf : S.f = 0
⊢ S.f ≫ 𝟙 S.X₂ = 0

Tactic:
rw [hf, comp_id]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
hf : S.f = 0
c : KernelFork S.g
hc : IsLimit c
T : C
φ : S.X₂ ⟶ T
⊢ (ofIsLimitKernelFork S hf c hc).descQ φ ⋯ = φ

Tactic:
rw [← cancel_epi (ofIsLimitKernelFork S hf c hc).p, p_descQ]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
hf : S.f = 0
c : KernelFork S.g
hc : IsLimit c
T : C
φ : S.X₂ ⟶ T
⊢ φ = (ofIsLimitKernelFork S hf c hc).p ≫ φ
Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ (rightHomologyMap' φ h₁ h₂).op = leftHomologyMap' (opMap φ) h₂.op h₁.op

Tactic:
let γ : RightHomologyMapData φ h₁ h₂ := rightHomologyMapData φ h₁ h₂

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂ := rightHomologyMapData φ h₁ h₂
⊢ (rightHomologyMap' φ h₁ h₂).op = leftHomologyMap' (opMap φ) h₂.op h₁.op
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 : ShortComplex C
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
hₗ : S.LeftHomologyData
hᵣ : S.RightHomologyData
inst✝¹ : hₗ.IsPreservedBy F
inst✝ : hᵣ.IsPreservedBy F
⊢ (Cofork.π (CokernelCofork.ofπ (hₗ.map F).π ⋯) ≫ F.map (leftRightHomologyComparison' hₗ hᵣ)) ≫
      Fork.ι (KernelFork.ofι (hᵣ.map F).ι ⋯) =
    F.map (hₗ.i ≫ hᵣ.p)

Tactic:
simp [← Functor.map_comp]

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.f = (F.obj j).f ≫ (c.ι.app j).τ₂
eq₁₂' : ∀ (j : J), (s.ι.app j).τ₁ ≫ s.pt.f = (F.obj j).f ≫ (s.ι.app j).τ₂
⊢ (F.obj j).f ≫ (s.ι.app j).τ₂ = (F.obj j).f ≫ (c.ι.app j).τ₂ ≫ h₂.desc (π₂.mapCocone s)

Tactic:
eq₂

Goal state after:
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.f = (F.obj j).f ≫ (c.ι.app j).τ₂
eq₁₂' : ∀ (j : J), (s.ι.app j).τ₁ ≫ s.pt.f = (F.obj j).f ≫ (s.ι.app j).τ₂
⊢ (F.obj j).f ≫ (s.ι.app j).τ₂ = (F.obj j).f ≫ (s.ι.app j).τ₂
Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : C
i : P ≅ Q
hP : Injective P
X✝ Y✝ : C
g : X✝ ⟶ Q
f : X✝ ⟶ Y✝
mono : Mono f
h : Y✝ ⟶ P
h_eq : f ≫ h = g ≫ i.inv
⊢ ∃ h, f ≫ h = g

Tactic:
refine ⟨h ≫ i.hom, ?_⟩

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : C
i : P ≅ Q
hP : Injective P
X✝ Y✝ : C
g : X✝ ⟶ Q
f : X✝ ⟶ Y✝
mono : Mono f
h : Y✝ ⟶ P
h_eq : f ≫ h = g ≫ i.inv
⊢ f ≫ h ≫ i.hom = g
Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic

Goal state before:
pp: case h.h₁
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
P Q : C
inst✝² : HasBinaryProduct P Q
inst✝¹ : Injective P
inst✝ : Injective Q
X✝ Y✝ : C
g : X✝ ⟶ P ⨯ Q
f : X✝ ⟶ Y✝
mono : Mono f
⊢ prod.lift (g ≫ prod.fst) (g ≫ prod.snd) ≫ prod.fst = g ≫ prod.fst

pp: case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
P Q : C
inst✝² : HasBinaryProduct P Q
inst✝¹ : Injective P
inst✝ : Injective Q
X✝ Y✝ : C
g : X✝ ⟶ P ⨯ Q
f : X✝ ⟶ Y✝
mono : Mono f
⊢ prod.lift (g ≫ prod.fst) (g ≫ prod.snd) ≫ prod.snd = g ≫ prod.snd

Tactic:
· simp only [prod.lift_fst]

Goal state after:
case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
P Q : C
inst✝² : HasBinaryProduct P Q
inst✝¹ : Injective P
inst✝ : Injective Q
X✝ Y✝ : C
g : X✝ ⟶ P ⨯ Q
f : X✝ ⟶ Y✝
mono : Mono f
⊢ prod.lift (g ≫ prod.fst) (g ≫ prod.snd) ≫ prod.snd = g ≫ prod.snd
Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
e : S₁ ≅ S₂
h : S₁.ShortExact
this : Epi (e.hom.τ₂ ≫ S₂.g)
⊢ Epi S₂.g

Tactic:
by
      exact epi_of_epi e.hom.τ₂ _

Goal state after:
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.ShortExact
inst✝ : Balanced C
⊢ IsIso S.f ↔ IsZero S.X₃

Tactic:
by
  have := hS.exact.hasZeroObject
  have := hS.mono_f
  have := hS.epi_g
  constructor
  · intro hf
    simp only [IsZero.iff_id_eq_zero, ← cancel_epi S.g, ← cancel_epi S.f,
      S.zero_assoc, zero_comp]
  · intro hX₃
    have : Epi S.f := (S.exact_iff_epi (hX₃.eq_of_tgt _ _)).1 hS.exact
    apply isIso_of_mono_of_epi

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.Exact
X Y : C
a : X ⟶ S.X₂
ha : a ≫ S.g = 0
b : S.X₂ ⟶ Y
hb : S.f ≫ b = 0
⊢ a ≫ b = 0

Tactic:
have := h.hasHomology
  have eq := h
  rw [exact_iff_iCycles_pOpcycles_zero] at eq
  rw [← S.liftCycles_i a ha, ← S.p_descOpcycles b hb, assoc, reassoc_of% eq,
    zero_comp, comp_zero]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
f g : MonoOver X
Y : C
h : Y ⟶ X
e : f ≅ g
x✝ : f.Factors h
u : Y ⟶ f.obj.left
hu : u ≫ f.arrow = h
⊢ (u ≫ Over.Hom.left ((forget X).map e.hom)) ≫ g.arrow = h

Tactic:
by simp [hu]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
f g : MonoOver X
Y : C
h : Y ⟶ X
e : f ≅ g
x✝ : g.Factors h
u : Y ⟶ g.obj.left
hu : u ≫ g.arrow = h
⊢ (u ≫ Over.Hom.left ((forget X).map e.inv)) ≫ f.arrow = h

Tactic:
by simp [hu]

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
B A₁ A₂ : C
f : A₁ ⟶ B
g : A₂ ⟶ B
inst✝¹ : Mono f
inst✝ : Mono g
h : mk f ≤ mk g
⊢ Mono (ofMkLEMk f g h)

Tactic:
dsimp only [ofMkLEMk]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
B A₁ A₂ : C
f : A₁ ⟶ B
g : A₂ ⟶ B
inst✝¹ : Mono f
inst✝ : Mono g
h : mk f ≤ mk g
⊢ Mono ((underlyingIso f).inv ≫ (mk f).ofLE (mk g) h ≫ (underlyingIso g).hom)
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
B A₁ A₂ : C
f : A₁ ⟶ B
g : A₂ ⟶ B
inst✝¹ : Mono f
inst✝ : Mono g
h : mk f ≤ mk g
⊢ Mono (ofMkLEMk f g h)

Tactic:
dsimp only [ofMkLEMk]
  infer_instance

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y✝ Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
Y : C
⊢ IsIso ⊤.arrow

Tactic:
rw [isIso_arrow_iff_eq_top]

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y : C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
f : X ⟶ Y
inst✝ : Mono f
h : mk f = ⊥
⊢ f = 0

Tactic:
by simpa [h, bot_factors_iff_zero] using mk_factors_self f

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
tfae_1_to_2 :
  (∀ (S : ShortComplex C), S.ShortExact → (S.map F).Exact ∧ Epi (F.map S.g)) →
    ∀ (S : ShortComplex C), S.Exact ∧ Epi S.g → (S.map F).Exact ∧ Epi (F.map S.g)
hF : ∀ (S : ShortComplex C), S.Exact ∧ Epi S.g → (S.map F).Exact ∧ Epi (F.map S.g)
X Y : C
f : X ⟶ Y
S : ShortComplex C := { X₁ := X, X₂ := Y, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }
⊢ IsColimit (CokernelCofork.map (Cofork.ofπ (cokernel.π f) ⋯) F)

Tactic:
let hS := hF S ⟨exact_cokernel f, inferInstance⟩

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
tfae_1_to_2 :
  (∀ (S : ShortComplex C), S.ShortExact → (S.map F).Exact ∧ Epi (F.map S.g)) →
    ∀ (S : ShortComplex C), S.Exact ∧ Epi S.g → (S.map F).Exact ∧ Epi (F.map S.g)
hF : ∀ (S : ShortComplex C), S.Exact ∧ Epi S.g → (S.map F).Exact ∧ Epi (F.map S.g)
X Y : C
f : X ⟶ Y
S : ShortComplex C := { X₁ := X, X₂ := Y, X₃ := cokernel f, f := f, g := cokernel.π f, zero := ⋯ }
hS : (S.map F).Exact ∧ Epi (F.map S.g) := hF S ⟨exact_cokernel f, inferInstance⟩
⊢ IsColimit (CokernelCofork.map (Cofork.ofπ (cokernel.π f) ⋯) F)
Module: Mathlib.CategoryTheory.Abelian.Exact

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
Z : C
tfae_2_to_1 : kernel.ι f = 0 → Mono f
⊢ [Mono f, kernel.ι f = 0, { X₁ := Z, X₂ := X, X₃ := Y, f := 0, g := f, zero := ⋯ }.Exact].TFAE

Tactic:
tfae_have 1 → 2
  | _ => by rw [← cancel_mono f, kernel.condition, zero_comp]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
Z : C
tfae_2_to_1 : kernel.ι f = 0 → Mono f
tfae_1_to_2 : Mono f → kernel.ι f = 0
⊢ [Mono f, kernel.ι f = 0, { X₁ := Z, X₂ := X, X₃ := Y, f := 0, g := f, zero := ⋯ }.Exact].TFAE
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: case mpr
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 : D ≌ D'
eL : L ⋙ E.functor ≅ L'
Y : D
Y' : D'
e : E.functor.obj Y ≅ Y'
a✝ : L'.HasPointwiseLeftKanExtensionAt F Y'
⊢ L.HasPointwiseLeftKanExtensionAt F Y

Tactic:
exact hasPointwiseLeftKanExtensionAt_of_equivalence L' L F E.symm
      (isoWhiskerRight eL.symm _ ≪≫ Functor.associator _ _ _ ≪≫
        isoWhiskerLeft L E.unitIso.symm ≪≫ L.rightUnitor) Y' Y
      (E.inverse.mapIso e.symm ≪≫ E.unitIso.symm.app Y)

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

Goal state before:
pp: case mpr
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
φ : F'' ⟶ F'
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
α' : L ⋙ F'' ⟶ F
comm : L.whiskerLeft φ ≫ α = α'
inst✝ : F'.IsRightKanExtension α
⊢ IsIso φ → F''.IsRightKanExtension α'

Tactic:
intro
    rw [isRightKanExtension_iff_of_iso (asIso φ) α' α comm]
    infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Countable

Goal state before:
pp: case inr
J : Type u_2
inst✝² : Countable J
inst✝¹ : Preorder J
inst✝ : IsFiltered J
d : J
n : ℕ
g : d ≤ (sequentialFunctor J).obj n
this✝ : Nonempty (StructuredArrow d (sequentialFunctor J))
i j : StructuredArrow d (sequentialFunctor J)
this :
  ∀ (J : Type u_2) [inst : Countable J] [inst_1 : Preorder J] [inst_2 : IsFiltered J] (d : J) (n : ℕ),
    d ≤ (sequentialFunctor J).obj n →
      Nonempty (StructuredArrow d (sequentialFunctor J)) →
        ∀ (i j : StructuredArrow d (sequentialFunctor J)), j.right ≤ i.right → Nonempty (i ⟶ j) ∨ Nonempty (j ⟶ i)
h : i.right < j.right
⊢ Nonempty (i ⟶ j) ∨ Nonempty (j ⟶ i)

Tactic:
exact or_comm.1 (this J d n g inferInstance j i (le_of_lt h))

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Countable

Goal state before:
pp: 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)

Tactic:
exact or_comm.1 (this J d n g inferInstance j i (le_of_lt h))

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u₁
inst✝² : Category.{v₁, u₁} D
G : D ⥤ C
inst✝¹ : HasLimits D
inst✝ : PreservesLimitsOfSize.{v₁, v₁, v₁, v, u₁, u} G
A : C
hG : ∃ ι B f, ∀ (X : D) (h : A ⟶ G.obj X), ∃ i g, f i ≫ G.map g = h
⊢ HasInitial (StructuredArrow A G)

Tactic:
choose ι B f g using hG

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u₁
inst✝² : Category.{v₁, u₁} D
G : D ⥤ C
inst✝¹ : HasLimits D
inst✝ : PreservesLimitsOfSize.{v₁, v₁, v₁, v, u₁, u} G
A : C
ι : Type v₁
B : ι → D
f : (i : ι) → A ⟶ G.obj (B i)
g : ∀ (X : D) (h : A ⟶ G.obj X), ∃ i g, f i ≫ G.map g = h
⊢ HasInitial (StructuredArrow A G)
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
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
X : C
⊢ (natTrans φ).app (uliftYoneda.{max w v₂, v₁, u₁}.obj X) = (compULiftYonedaIsoULiftYonedaCompLan F).inv.app X ≫ φ.app X

Tactic:
dsimp [natTrans]

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
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
X : C
⊢ (F.op.lan.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj X)).descOfIsLeftKanExtension
      (F.op.lanUnit.app (uliftYoneda.{max w v₂, v₁, u₁}.obj X)) (G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj X))
      (presheafHom φ (uliftYoneda.{max w v₂, v₁, u₁}.obj X)) =
    (compULiftYonedaIsoULiftYonedaCompLan F).inv.app X ≫ φ.app X
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), HasProduct fun x ↦ G
h : ∀ (A : C), Mono (Pi.lift fun f ↦ f)
X Y : C
f g : X ⟶ Y
hh : ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
⊢ f = g

Tactic:
have := h Y
    refine (cancel_mono (Pi.lift fun f : Y ⟶ G => f)).1 (limit.hom_ext fun j => ?_)
    simpa using hh j.as

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: X : Type u
⊢ Nonempty (IsInitial X) ↔ IsEmpty X

Tactic:
constructor
  · intro ⟨h⟩
    exact Function.isEmpty (IsInitial.to h PEmpty)
  · intro h
    exact ⟨IsInitial.ofIso Types.isInitialPEmpty <| Equiv.toIso <| Equiv.equivOfIsEmpty PEmpty X⟩

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
c : Set (ExtensionOf i f)
hchain : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
a : ExtensionOf i f
a_mem : a ∈ c
b : ExtensionOf i f
b_mem : b ∈ c
ne : (fun x ↦ x.toLinearPMap) a ≠ (fun x ↦ x.toLinearPMap) b
⊢ (fun x1 x2 ↦ x1 ≤ x2) ((fun x ↦ x.toLinearPMap) a) ((fun x ↦ x.toLinearPMap) b) ∨
    (fun x1 x2 ↦ x1 ≤ x2) ((fun x ↦ x.toLinearPMap) b) ((fun x ↦ x.toLinearPMap) a)

Tactic:
exact hchain a_mem b_mem (ne_of_apply_ne _ ne)

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)
y : N
x : ↥(supExtensionOfMaxSingleton i f y)
⊢ ∃ a b, ↑x = ↑a + b • y

Tactic:
by
  have mem1 : x.1 ∈ (_ : Set _) := x.2
  rw [Submodule.coe_sup] at mem1
  rcases mem1 with ⟨a, a_mem, b, b_mem : b ∈ (Submodule.span R _ : Submodule R N), eq1⟩
  rw [Submodule.mem_span_singleton] at b_mem
  rcases b_mem with ⟨z, eq2⟩
  exact ⟨⟨a, a_mem⟩, z, by rw [← eq1, ← eq2]⟩

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' : R
eq1 : r • y = r' • y
⊢ (extendIdealTo i f h y) (r - r') = 0

Tactic:
convert! ExtensionOfMaxAdjoin.extendIdealTo_wd' i f h (r - r') _

Goal state after:
case convert_2
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' : R
eq1 : r • y = r' • y
⊢ (r - r') • y = 0
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
a b : ↥(supExtensionOfMaxSingleton i f y)
⊢ ExtensionOfMaxAdjoin.extensionToFun i f h (a + b) =
    ExtensionOfMaxAdjoin.extensionToFun i f h a + ExtensionOfMaxAdjoin.extensionToFun i f h b

Tactic:
have eq1 :
          ↑a + ↑b =
            ↑(ExtensionOfMaxAdjoin.fst i a + ExtensionOfMaxAdjoin.fst i b) +
              (ExtensionOfMaxAdjoin.snd i a + ExtensionOfMaxAdjoin.snd i b) • y := by
          rw [ExtensionOfMaxAdjoin.eqn, ExtensionOfMaxAdjoin.eqn, add_smul, Submodule.coe_add]
          ac_rfl
        rw [ExtensionOfMaxAdjoin.extensionToFun_wd (y := y) i f h (a + b) _ _ eq1,
          LinearPMap.map_add, map_add]
        unfold ExtensionOfMaxAdjoin.extensionToFun
        abel

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)
eq1 : r • ↑a = ↑(r • ExtensionOfMaxAdjoin.fst i a) + (r • ExtensionOfMaxAdjoin.snd i a) • y
⊢ ↑(extensionOfMax i f).toLinearPMap (r • ExtensionOfMaxAdjoin.fst i a) +
      r • (ExtensionOfMaxAdjoin.extendIdealTo i f h y) (ExtensionOfMaxAdjoin.snd i a) =
    r • ExtensionOfMaxAdjoin.extensionToFun i f h a

Tactic:
LinearPMap.map_smul,

Goal state after:
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)
eq1 : r • ↑a = ↑(r • ExtensionOfMaxAdjoin.fst i a) + (r • ExtensionOfMaxAdjoin.snd i a) • y
⊢ r • ↑(extensionOfMax i f).toLinearPMap (ExtensionOfMaxAdjoin.fst i a) +
      r • (ExtensionOfMaxAdjoin.extendIdealTo i f h y) (ExtensionOfMaxAdjoin.snd i a) =
    r • ExtensionOfMaxAdjoin.extensionToFun i f h a
Module: Mathlib.Order.Filter.AtTopBot.Prod

Goal state before:
pp: α : Type u_3
inst✝ : Preorder α
⊢ Tendsto (fun a ↦ (a, a)) atTop atTop

Tactic:
rw [← prod_atTop_atTop_eq]
  exact tendsto_id.prodMk tendsto_id

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 : α
⊢ toIocMod hp a a = a + p

Tactic:
rw [toIocMod_eq_iff hp, Set.right_mem_Ioc]
  exact ⟨lt_add_of_pos_right _ hp, -1, by simp⟩

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 (p + b) = toIcoDiv hp a b + 1

Tactic:
rw [add_comm, toIcoDiv_add_right]

Goal state after:
Module: Mathlib.Order.Filter.Lift

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
h : Set α → Set β
m : γ → β
⊢ comap m (f.lift' h) = f.lift' (preimage m ∘ h)

Tactic:
by
  simp only [Filter.lift', comap_lift_eq, comp_def, comap_principal]

Goal state after: