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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
⊢ (factorThruImage f ≫ image.lift (imageStrongEpiMonoFactorisation f).toMonoFactorisation) ≫
      equalizer.ι (cokernel.π f) 0 =
    (factorThruImage f ≫ kernel.lift (cokernel.π f) (Limits.image.ι f) ⋯) ≫ equalizer.ι (cokernel.π f) 0

Tactic:
Limits.image.fac_lift,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
⊢ (imageStrongEpiMonoFactorisation f).e ≫ equalizer.ι (cokernel.π f) 0 =
    (factorThruImage f ≫ kernel.lift (cokernel.π f) (Limits.image.ι f) ⋯) ≫ equalizer.ι (cokernel.π f) 0
Module: Mathlib.Algebra.Category.Grp.EpiMono

Goal state before:
pp: A B : GrpCat
f : A ⟶ B
β : ↑B
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (β * β⁻¹) • x = x

Tactic:
mul_inv_cancel,

Goal state after:
A B : GrpCat
f : A ⟶ B
β : ↑B
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ 1 • x = x
Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
h : S.LeftHomologyData
inst✝ : S.HasLeftHomology
⊢ S.leftHomologyπ ≫ h.leftHomologyIso.hom = h.cyclesIso.hom ≫ h.π

Tactic:
dsimp only [leftHomologyπ, leftHomologyIso, cyclesIso, leftHomologyMapIso',
    cyclesMapIso', Iso.refl]
  rw [← leftHomologyπ_naturality']

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

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

Tactic:
simp only [Fork.ι_ofι] at eq

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h : S₁.LeftHomologyData
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
i : h.K ⟶ S₂.X₂ := h.i ≫ φ.τ₂
wi : i ≫ S₂.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₂.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₂.f ⋯)
eq : hi.lift (KernelFork.ofι S₂.f ⋯) ≫ i = S₂.f
⊢ φ.τ₁ ≫ f' = h.f'
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₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ leftRightHomologyComparison' S₁.leftHomologyData h₁ ≫ rightHomologyMap' φ h₁ h₂ =
    leftRightHomologyComparison' S₁.leftHomologyData h₁ ≫ h₁.homologyIso.inv ≫ homologyMap φ ≫ h₂.homologyIso.hom

Tactic:
← leftRightHomologyComparison'_naturality φ S₁.leftHomologyData h₁ S₂.leftHomologyData h₂,

Goal state after:
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₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ leftHomologyMap' φ S₁.leftHomologyData S₂.leftHomologyData ≫ leftRightHomologyComparison' S₂.leftHomologyData h₂ =
    leftRightHomologyComparison' S₁.leftHomologyData h₁ ≫ h₁.homologyIso.inv ≫ homologyMap φ ≫ h₂.homologyIso.hom
Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology

Goal state before:
pp: case refine_3
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₂✝ : IsIso φ.τ₂
h₃ : Mono φ.τ₃
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ h₁.liftK (h₂.i ≫ inv φ.τ₂) ⋯ ≫ cyclesMap' φ h₁ h₂ = 𝟙 h₂.K

Tactic:
simp only [← cancel_mono h₂.i, assoc, cyclesMap'_i, h₁.liftK_i_assoc,
      IsIso.inv_hom_id, comp_id, id_comp]

Goal state after:
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 : Cone F
h₁ : IsLimit (π₁.mapCone c)
h₂ : IsLimit (π₂.mapCone c)
h₃ : IsLimit (π₃.mapCone c)
s : Cone F
m : s.pt ⟶ c.pt
hm : ∀ (j : J), m ≫ c.π.app j = s.π.app j
⊢ m.τ₁ =
    { τ₁ := h₁.lift (π₁.mapCone s), τ₂ := h₂.lift (π₂.mapCone s), τ₃ := h₃.lift (π₃.mapCone s), comm₁₂ := ⋯,
        comm₂₃ := ⋯ }.τ₁

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

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₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
h' : Homotopy φ₃ φ₄
⊢ S₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f + φ₂.τ₂ - (S₁.g ≫ h'.h₂ + h'.h₁ ≫ S₂.f + φ₄.τ₂) =
    S₁.g ≫ h.h₂ - S₁.g ≫ h'.h₂ + (h.h₁ - h'.h₁) ≫ S₂.f + (φ₂.τ₂ - φ₄.τ₂)

Tactic:
sub_comp

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
h' : Homotopy φ₃ φ₄
⊢ S₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f + φ₂.τ₂ - (S₁.g ≫ h'.h₂ + h'.h₁ ≫ S₂.f + φ₄.τ₂) =
    S₁.g ≫ h.h₂ - S₁.g ≫ h'.h₂ + (h.h₁ ≫ S₂.f - h'.h₁ ≫ S₂.f) + (φ₂.τ₂ - φ₄.τ₂)
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₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
h' : Homotopy φ₃ φ₄
⊢ h.h₃ + h.h₂ ≫ S₂.g + φ₂.τ₃ - (h'.h₃ + h'.h₂ ≫ S₂.g + φ₄.τ₃) = h.h₃ - h'.h₃ + (h.h₂ - h'.h₂) ≫ S₂.g + (φ₂.τ₃ - φ₄.τ₃)

Tactic:
sub_comp

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
h' : Homotopy φ₃ φ₄
⊢ h.h₃ + h.h₂ ≫ S₂.g + φ₂.τ₃ - (h'.h₃ + h'.h₂ ≫ S₂.g + φ₄.τ₃) =
    h.h₃ - h'.h₃ + (h.h₂ ≫ S₂.g - h'.h₂ ≫ S₂.g) + (φ₂.τ₃ - φ₄.τ₃)
Module: Mathlib.CategoryTheory.Preadditive.Projective.Basic

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

Tactic:
rcases hP.factors (adj.unit.app P ≫ G.map f) (G.map g) with ⟨f', hf'⟩

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.PreservesEpimorphisms
P : C
hP : Projective P
E✝ X✝ : D
f : F.obj P ⟶ X✝
g : E✝ ⟶ X✝
x✝ : Epi g
f' : P ⟶ G.obj E✝
hf' : f' ≫ G.map g = adj.unit.app P ≫ G.map f
⊢ ∃ f', f' ≫ g = f
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₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
H₁ : S₁.LeftHomologyData
H₂ : S₂.LeftHomologyData
h₀ : S₁.X₁ ⟶ S₂.X₁
h₀_f : h₀ ≫ S₂.f = 0
h₁ : S₁.X₂ ⟶ S₂.X₁
h₂ : S₁.X₃ ⟶ S₂.X₂
h₃ : S₁.X₃ ⟶ S₂.X₃
g_h₃ : S₁.g ≫ h₃ = 0
⊢ H₁.f' ≫ H₂.liftK (H₁.i ≫ h₁ ≫ S₂.f) ⋯ = (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ ≫ H₂.f'

Tactic:
← cancel_mono H₂.i,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
H₁ : S₁.LeftHomologyData
H₂ : S₂.LeftHomologyData
h₀ : S₁.X₁ ⟶ S₂.X₁
h₀_f : h₀ ≫ S₂.f = 0
h₁ : S₁.X₂ ⟶ S₂.X₁
h₂ : S₁.X₃ ⟶ S₂.X₂
h₃ : S₁.X₃ ⟶ S₂.X₃
g_h₃ : S₁.g ≫ h₃ = 0
⊢ (H₁.f' ≫ H₂.liftK (H₁.i ≫ h₁ ≫ S₂.f) ⋯) ≫ H₂.i = ((S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ ≫ H₂.f') ≫ H₂.i
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: case mp
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
S : ShortComplex C
inst✝¹ : S.HasHomology
inst✝ : HasZeroObject C
⊢ IsZero S.homology → Nonempty (S.homology ≅ 0)

pp: case mpr
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
S : ShortComplex C
inst✝¹ : S.HasHomology
inst✝ : HasZeroObject C
⊢ Nonempty (S.homology ≅ 0) → IsZero S.homology

Tactic:
· intro h
    exact ⟨h.isoZero⟩

Goal state after:
case mpr
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
S : ShortComplex C
inst✝¹ : S.HasHomology
inst✝ : HasZeroObject C
⊢ Nonempty (S.homology ≅ 0) → IsZero S.homology
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✝¹ : Preadditive D
S : ShortComplex C
s : S.Splitting
F : C ⥤ D
inst✝ : F.Additive
⊢ (S.map F).f ≫ F.map s.r = 𝟙 (S.map F).X₁

Tactic:
dsimp [ShortComplex.map]

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
S : ShortComplex C
s : S.Splitting
F : C ⥤ D
inst✝ : F.Additive
⊢ F.map S.f ≫ F.map s.r = 𝟙 (F.obj S.X₁)
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✝¹ : Preadditive D
S : ShortComplex C
s : S.Splitting
F : C ⥤ D
inst✝ : F.Additive
⊢ F.map s.s ≫ (S.map F).g = 𝟙 (S.map F).X₃

Tactic:
dsimp [ShortComplex.map]

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
S : ShortComplex C
s : S.Splitting
F : C ⥤ D
inst✝ : F.Additive
⊢ F.map s.s ≫ F.map S.g = 𝟙 (F.obj S.X₃)
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✝¹ : Preadditive D
S : ShortComplex C
s : S.Splitting
F : C ⥤ D
inst✝ : F.Additive
⊢ F.map s.r ≫ (S.map F).f + (S.map F).g ≫ F.map s.s = 𝟙 (S.map F).X₂

Tactic:
dsimp [ShortComplex.map]

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
S : ShortComplex C
s : S.Splitting
F : C ⥤ D
inst✝ : F.Additive
⊢ F.map s.r ≫ F.map S.f + F.map S.g ≫ F.map s.s = 𝟙 (F.obj S.X₂)
Module: Mathlib.CategoryTheory.Subobject.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
inst✝ : HasPullbacks C
f : X ⟶ Y
y : Subobject Y
⊢ ∃ φ, IsPullback φ ((pullback f).obj y).arrow y.arrow f

Tactic:
obtain ⟨A, i, ⟨_, rfl⟩⟩ := mk_surjective y
  rw [pullback_obj]
  exists (underlyingIso (pullback.snd (mk i).arrow f)).hom ≫ pullback.fst (mk i).arrow f
  exact IsPullback.of_iso (IsPullback.of_hasPullback (mk i).arrow f)
        (underlyingIso (pullback.snd (mk i).arrow f)).symm (Iso.refl _) (Iso.refl _) (Iso.refl _)
        (by simp) (by simp) (by simp) (by simp)

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
⊢ S.Exact ↔ IsIso (imageToKernel S.f S.g ⋯)

Tactic:
rw [S.exact_iff_epi_imageToKernel]
  constructor
  · intro
    apply isIso_of_mono_of_epi
  · intro
    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
inst✝ : HasPullbacks C
x✝ : Cᵒᵖ
⊢ ↾(pullback (𝟙 x✝).unop).obj = 𝟙 (Subobject (Opposite.unop x✝))

Tactic:
ext : 3; simp [pullback_id]

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
h : kernel.ι S.g ≫ cokernel.π S.f = 0
Z'✝ : C
u : S.X₂ ⟶ Z'✝
hu : S.f ≫ u = 0
⊢ kernel.ι S.g ≫ u = 0

Tactic:
by rw [← cokernel.π_desc S.f u hu, ← Category.assoc, h, zero_comp]

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

Goal state before:
pp: A : Type u₁
B : Type u₂
inst✝⁴ : Category.{v₁, u₁} A
inst✝³ : Category.{v₂, u₂} B
inst✝² : Abelian A
inst✝¹ : Abelian B
L : A ⥤ B
inst✝ : L.PreservesZeroMorphisms
hL : ∀ (S : ShortComplex A), S.Exact → (S.map L).Exact
X✝ Y✝ : A
f : X✝ ⟶ Y✝
hf : Mono f
⊢ Mono (L.map f)

Tactic:
apply ((Abelian.tfae_mono (L.map f) (L.obj 0)).out 2 0).mp
    refine ShortComplex.exact_of_iso ?_ (hL _ (((tfae_mono f 0).out 0 2).mp hf))
    exact ShortComplex.isoMk (Iso.refl _) (Iso.refl _) (Iso.refl _)

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

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

Tactic:
exact prod.lift (inf_le_left _ _).hom (inf_le_right _ _).hom

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

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

Tactic:
intro ⟨j⟩

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
c c' : Cofan Z
f : Fan fun x ↦ op (Z x)
hc : IsColimit c
hc' : IsColimit c'
hf : IsLimit f
j : α
⊢ c'.ι.app { as := j } ≫ ((opCoproductIsoProduct' hc hf).hom ≫ (opCoproductIsoProduct' hc' hf).inv).unop =
    c'.ι.app { as := j } ≫ (hc.coconePointUniqueUpToIso hc').op.inv.unop
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
⊢ ∀ (j : Discrete α),
    ((opProductIsoCoproduct' hf hc).hom ≫ (opProductIsoCoproduct' hf' hc).inv).unop ≫ f.π.app j =
      (hf.conePointUniqueUpToIso hf').op.inv.unop ≫ f.π.app j

Tactic:
intro ⟨j⟩

Goal state after:
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
j : α
⊢ ((opProductIsoCoproduct' hf hc).hom ≫ (opProductIsoCoproduct' hf' hc).inv).unop ≫ f.π.app { as := j } =
    (hf.conePointUniqueUpToIso hf').op.inv.unop ≫ f.π.app { as := j }
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 = prod.fst.op

Tactic:
rw [Iso.comp_inv_eq, fst_opProdIsoCoprod_hom]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
H : Type u_3
inst✝¹ : Category.{v_3, u_3} H
inst✝ : ∀ (F : C ⥤ H), L.HasLeftKanExtension F
F₁ F₂ : C ⥤ H
G : D ⥤ H
f : F₁ ⟶ F₂
α : F₂ ⟶ ((whiskeringLeft C D H).obj L).obj G
X : C
⊢ (L.lanUnit.app F₁).app X ≫ ((L.lan.obj F₁).descOfIsLeftKanExtension (L.lanUnit.app F₁) G (f ≫ α)).app (L.obj X) =
    (L.lanUnit.app F₁).app X ≫
      (L.lan.map f).app (L.obj X) ≫ ((L.lan.obj F₂).descOfIsLeftKanExtension (L.lanUnit.app F₂) G α).app (L.obj X)

Tactic:
descOfIsLeftKanExtension_fac_app,

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
L : C ⥤ D
H : Type u_3
inst✝¹ : Category.{v_3, u_3} H
inst✝ : ∀ (F : C ⥤ H), L.HasLeftKanExtension F
F₁ F₂ : C ⥤ H
G : D ⥤ H
f : F₁ ⟶ F₂
α : F₂ ⟶ ((whiskeringLeft C D H).obj L).obj G
X : C
⊢ (f ≫ α).app X =
    (L.lanUnit.app F₁).app X ≫
      (L.lan.map f).app (L.obj X) ≫ ((L.lan.obj F₂).descOfIsLeftKanExtension (L.lanUnit.app F₂) G α).app (L.obj X)
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
E' : ?m.13
h : E.IsPointwiseLeftKanExtension
G : L.LeftExtension F
Y₁ Y₂ : D
φ : Y₁ ⟶ Y₂
X : CostructuredArrow L Y₁
⊢ (E.coconeAt Y₁).ι.app X ≫ (StructuredArrow.right E).map φ ≫ (h Y₂).desc (G.coconeAt Y₂) =
    (E.coconeAt Y₁).ι.app X ≫ (h Y₁).desc (G.coconeAt Y₁) ≫ (StructuredArrow.right G).map φ

Tactic:
rw [(h Y₁).fac_assoc (coconeAt G Y₁) X]
        simpa using (h Y₂).fac (coconeAt G Y₂) ((CostructuredArrow.map φ).obj X)

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
H : Type u_3
inst✝¹ : Category.{v_3, u_3} H
inst✝ : ∀ (F : C ⥤ H), L.HasRightKanExtension F
F₁ F₂ : D ⥤ H
G : C ⥤ H
β : F₁ ⟶ F₂
f : F₂ ⟶ L.ran.obj G
⊢ ((L.ran.obj G).homEquivOfIsRightKanExtension (L.ranCounit.app G) F₁).symm.symm (β ≫ f) =
    ((whiskeringLeft C D H).obj L).map β ≫
      ((L.ran.obj G).homEquivOfIsRightKanExtension (L.ranCounit.app G) F₂).symm.symm f

Tactic:
dsimp [homEquivOfIsRightKanExtension]
        rw [assoc]

Goal state after:
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
h : E.IsPointwiseRightKanExtension
G : L.RightExtension F
⊢ ((whiskeringLeft C D H).obj L).map { app := fun Y ↦ (h Y).lift (G.coneAt Y), naturality := ⋯ } ≫
      CostructuredArrow.hom E =
    CostructuredArrow.hom G

Tactic:
by
      ext X
      simpa using (h (L.obj X)).fac (RightExtension.coneAt G _) (StructuredArrow.mk (𝟙 _))

Goal state after:
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
inst✝ : L.HasPointwiseLeftKanExtension F
X : D
j : CostructuredArrow L X
⊢ (colimit.cocone (CostructuredArrow.proj L X ⋙ F)).ι.app j ≫
      (Iso.refl (colimit.cocone (CostructuredArrow.proj L X ⋙ F)).pt).hom =
    ((LeftExtension.mk (L.pointwiseLeftKanExtension F) (L.pointwiseLeftKanExtensionUnit F)).coconeAt X).ι.app j

Tactic:
by
    dsimp
    simp only [comp_id, colimit.ι_desc, CostructuredArrow.map_mk]
    congr 1
    rw [id_comp, ← CostructuredArrow.eq_mk]

Goal state after:
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 : ℰ
f :
  CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A ⟶
    (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)).obj E
X : CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P
Y : Cᵒᵖ
x :
  (uliftYoneda.{max w v₂, v₁, u₁}.obj
        (CostructuredArrow.mk (uliftYonedaEquiv.symm ((hom (X.hom.app (op X.left))) { down := 𝟙 X.left }))).left).obj
    Y
⊢ (hom (X.hom.app Y)) { down := x.down ≫ 𝟙 X.left } =
    (hom (P.map x.down.op)) ((hom (X.hom.app (op X.left))) { down := 𝟙 X.left })

Tactic:
simp [← NatTrans.naturality_apply]

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝² : Category.{v₂, u₂} ℰ
A✝ A : C ⥤ ℰ
inst✝¹ : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
D : Type u₂
inst✝ : Category.{v₁, u₂} D
F : C ⥤ D
X : C
Y : F.op.LeftExtension (yoneda.obj X)
φ : Functor.LeftExtension.mk (yoneda.obj (F.obj X)) (yonedaMap F X) ⟶ Y
⊢ yonedaEquiv (StructuredArrow.Hom.right φ) =
    yonedaEquiv
      (StructuredArrow.Hom.right (StructuredArrow.homMk (yonedaEquiv.symm (yonedaEquiv (StructuredArrow.hom Y))) ⋯))

Tactic:
simp [← StructuredArrow.w φ, yonedaEquiv, yonedaMap]

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

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
j : WalkingParallelFamily J
⊢ F.obj j = (parallelFamily fun j ↦ F.map (line j)).obj j

Tactic:
by cases j <;> cat_disch

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

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Trident fun j ↦ F.map (line j)
j : WalkingParallelFamily J
⊢ (parallelFamily fun j ↦ F.map (line j)).obj j = F.obj j

Tactic:
by cases j <;> cat_disch

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

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cotrident fun j ↦ F.map (line j)
j : WalkingParallelFamily J
⊢ F.obj j = (parallelFamily fun j ↦ F.map (line j)).obj j

Tactic:
by cases j <;> cat_disch

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

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cone F
j : WalkingParallelFamily J
⊢ F.obj j = (parallelFamily fun j ↦ F.map (line j)).obj j

Tactic:
by cases j <;> cat_disch

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

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cocone F
j : WalkingParallelFamily J
⊢ (parallelFamily fun j ↦ F.map (line j)).obj j = F.obj j

Tactic:
by cases j <;> cat_disch

Goal state after:
Module: Mathlib.Data.Int.SuccPred

Goal state before:
pp: a b : ℕ
⊢ ↑a ⋖ ↑b ↔ a ⋖ b

Tactic:
by
  rw [Order.covBy_iff_add_one_eq, Order.covBy_iff_add_one_eq]
  exact Int.natCast_inj

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddMonoid α
h : Periodic f c
n : ℕ
⊢ Periodic f (n • c)

Tactic:
induction n <;> simp_all [add_nsmul, ← add_assoc]

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : AddGroup α
inst✝ : SubtractionMonoid β
h : Antiperiodic f c
k : ℤ
⊢ f (x + (2 * k) • c) = ↑(2 * k).negOnePow • f x

Tactic:
h.even_zsmul_periodic,

Goal state after:
case inl
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : AddGroup α
inst✝ : SubtractionMonoid β
h : Antiperiodic f c
k : ℤ
⊢ f x = ↑(2 * k).negOnePow • f x
Module: Mathlib.Algebra.Order.Interval.Set.Group

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
⊢ Pairwise (Disjoint on fun n ↦ Ioc (a * b ^ n) (a * b ^ (n + 1)))

Tactic:
simp +unfoldPartialApp only [Function.onFun]

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
⊢ Pairwise fun x y ↦ Disjoint (Ioc (a * b ^ x) (a * b ^ (x + 1))) (Ioc (a * b ^ y) (a * b ^ (y + 1)))
Module: Mathlib.Algebra.Order.Interval.Set.Group

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
⊢ Pairwise (Disjoint on fun n ↦ Ico (a * b ^ n) (a * b ^ (n + 1)))

Tactic:
simp +unfoldPartialApp only [Function.onFun]

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
⊢ Pairwise fun x y ↦ Disjoint (Ico (a * b ^ x) (a * b ^ (x + 1))) (Ico (a * b ^ y) (a * b ^ (y + 1)))