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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
α : X ≅ Y
Z : C
β : Y ≅ Z
f : Aut X
⊢ (α ≪≫ β).conjAut f = β.conjAut (α.conjAut f)

Tactic:
by
  simp only [conjAut_apply, Iso.trans_symm, Iso.trans_assoc]

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

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
r t : Cone F
P : IsLimit r
i : IsIso (P.lift t)
⊢ r ≅ t

Tactic:
haveI : IsIso (P.liftConeMorphism t).hom := i

Goal state after:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
r t : Cone F
P : IsLimit r
i : IsIso (P.lift t)
this : IsIso (P.liftConeMorphism t).hom
⊢ r ≅ t
Module: Mathlib.CategoryTheory.Adjunction.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
X Y : C
f : X ⟶ Y
Z : D
⊢ Function.Bijective (⇑(adj.homEquiv X Z) ∘ fun g ↦ F.map f ≫ g) ↔ Function.Bijective fun g ↦ f ≫ g

Tactic:
← Function.Bijective.of_comp_iff _ (adj.homEquiv _ _).symm.bijective

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
X Y : C
f : X ⟶ Y
Z : D
⊢ Function.Bijective ((⇑(adj.homEquiv X Z) ∘ fun g ↦ F.map f ≫ g) ∘ ⇑(adj.homEquiv Y Z).symm) ↔
    Function.Bijective fun g ↦ f ≫ g
Module: Mathlib.CategoryTheory.Adjunction.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
X Y : D
g : X ⟶ Y
Z : C
⊢ (Function.Bijective fun f ↦ f ≫ G.map g) ↔ Function.Bijective (⇑(adj.homEquiv Z Y) ∘ fun f ↦ f ≫ g)

Tactic:
← Function.Bijective.of_comp_iff _ (adj.homEquiv _ _).symm.bijective

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
X Y : D
g : X ⟶ Y
Z : C
⊢ (Function.Bijective fun f ↦ f ≫ G.map g) ↔
    Function.Bijective ((⇑(adj.homEquiv Z Y) ∘ fun f ↦ f ≫ g) ∘ ⇑(adj.homEquiv Z X).symm)
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type v
X : C
e e' : F.CorepresentableBy X
h : e.homEquiv (𝟙 X) = e'.homEquiv (𝟙 X)
⊢ e = e'

Tactic:
have : ∀ {Y : C} (f : X ⟶ Y), e.homEquiv f = e'.homEquiv f := fun {X} f ↦ by
    rw [e.homEquiv_eq, e'.homEquiv_eq, h]
  obtain ⟨e, he⟩ := e
  obtain ⟨e', he'⟩ := e'
  obtain rfl : @e = @e' := by ext; apply this
  rfl

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

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u₃
inst✝² : Category.{v₃, u₃} C
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
E : Type u₅
inst✝ : Category.{v₅, u₅} E
F : J ⥤ C
G : C ⥤ D
A : Cone F
⊢ ∀ ⦃X Y : J⦄ (f : X ⟶ Y), ((const J).obj (G.obj A.pt)).map f ≫ G.map (A.π.app Y) = G.map (A.π.app X) ≫ (F ⋙ G).map f

Tactic:
simp [← G.map_comp]

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

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u₃
inst✝² : Category.{v₃, u₃} C
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
E : Type u₅
inst✝ : Category.{v₅, u₅} E
F : J ⥤ C
G : C ⥤ D
A : Cone F
⊢ ∀ ⦃X Y : J⦄ (f : X ⟶ Y), ((const J).obj (G.obj A.pt)).map f ≫ G.map (A.π.app Y) = G.map (A.π.app X) ≫ (F ⋙ G).map f

Tactic:
by simp [← G.map_comp]

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

Goal state before:
pp: β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝¹ : Category.{v, u} C
X : Discrete α ⥤ C
inst✝ : HasProduct fun j ↦ X.obj { as := j }
s : Cone X
m : s.pt ⟶ (Pi.cone X).pt
hm : ∀ (j : Discrete α), m ≫ (Pi.cone X).π.app j = s.π.app j
⊢ m = Pi.lift fun j ↦ s.π.app { as := j }

Tactic:
by
    dsimp
    ext
    simp only [limit.lift_π, Fan.mk_pt, Fan.mk_π_app]
    apply hm

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

Goal state before:
pp: case uniq
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryFan X Y
f : X ⟶ X'
inst✝ : IsIso f
h : IsLimit c
⊢ ∀ (s : BinaryFan X' ((pair X Y).obj { as := right }))
    (m : s.pt ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }),
    m ≫ c.fst ≫ f = s.fst → m ≫ c.snd = s.snd → m = IsLimit.lift h (s.fst ≫ inv f) s.snd

Tactic:
intro s m e₁ e₂

Goal state after:
case uniq
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryFan X Y
f : X ⟶ X'
inst✝ : IsIso f
h : IsLimit c
s : BinaryFan X' ((pair X Y).obj { as := right })
m : s.pt ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }
e₁ : m ≫ c.fst ≫ f = s.fst
e₂ : m ≫ c.snd = s.snd
⊢ m = IsLimit.lift h (s.fst ≫ inv f) s.snd
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: case uniq
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryCofan X Y
f : X' ⟶ X
inst✝ : IsIso f
h : IsColimit c
⊢ ∀ (s : BinaryCofan X' ((pair X Y).obj { as := right }))
    (m : ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left } ⟶ s.pt),
    (f ≫ c.inl) ≫ m = s.inl → c.inr ≫ m = s.inr → m = IsColimit.desc h (inv f ≫ s.inl) s.inr

Tactic:
intro s m e₁ e₂

Goal state after:
case uniq
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryCofan X Y
f : X' ⟶ X
inst✝ : IsIso f
h : IsColimit c
s : BinaryCofan X' ((pair X Y).obj { as := right })
m : ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left } ⟶ s.pt
e₁ : (f ≫ c.inl) ≫ m = s.inl
e₂ : c.inr ≫ m = s.inr
⊢ m = IsColimit.desc h (inv f ≫ s.inl) s.inr
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: case h₁
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u₂
inst✝⁵ : Category.{w, u₂} D
E : Type u₃
inst✝⁴ : Category.{w', u₃} E
F : C ⥤ D
G : D ⥤ E
A B : C
inst✝³ : HasBinaryProduct A B
inst✝² : HasBinaryProduct (F.obj A) (F.obj B)
inst✝¹ : HasBinaryProduct (G.obj (F.obj A)) (G.obj (F.obj B))
inst✝ : HasBinaryProduct ((F ⋙ G).obj A) ((F ⋙ G).obj B)
⊢ prod.lift ((F ⋙ G).map prod.fst) ((F ⋙ G).map prod.snd) ≫ prod.fst =
    (G.map (prod.lift (F.map prod.fst) (F.map prod.snd)) ≫ prod.lift (G.map prod.fst) (G.map prod.snd)) ≫ prod.fst

Tactic:
simp [← G.map_comp]

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

Goal state before:
pp: case h₂
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u₂
inst✝⁵ : Category.{w, u₂} D
E : Type u₃
inst✝⁴ : Category.{w', u₃} E
F : C ⥤ D
G : D ⥤ E
A B : C
inst✝³ : HasBinaryProduct A B
inst✝² : HasBinaryProduct (F.obj A) (F.obj B)
inst✝¹ : HasBinaryProduct (G.obj (F.obj A)) (G.obj (F.obj B))
inst✝ : HasBinaryProduct ((F ⋙ G).obj A) ((F ⋙ G).obj B)
⊢ prod.lift ((F ⋙ G).map prod.fst) ((F ⋙ G).map prod.snd) ≫ prod.snd =
    (G.map (prod.lift (F.map prod.fst) (F.map prod.snd)) ≫ prod.lift (G.map prod.fst) (G.map prod.snd)) ≫ prod.snd

Tactic:
simp [← G.map_comp]

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S S' S'' : D
Y Y' Y'' : C
T T' : C ⥤ D
A : Type u₃
inst✝¹ : Category.{v₃, u₃} A
B : Type u₄
inst✝ : Category.{v₄, u₄} B
L : D
R : C ⥤ D
L' : B
R' : A ⥤ B
F : C ⥤ A
G : D ⥤ B
β : R ⋙ G ⟶ F ⋙ R'
F' : C ⥤ A
G' : D ⥤ B
e₁ : F ≅ F'
e₂ : G ≅ G'
α' : L' ⟶ G'.obj L
β' : R ⋙ G' ⟶ F' ⋙ R'
hβ : β ≫ Functor.whiskerRight e₁.hom R' = R.whiskerLeft e₂.hom ≫ β'
X : StructuredArrow L R
⊢ ((map₂ (α' ≫ e₂.inv.app L) β).obj X).hom ≫ R'.map (e₁.app X.right).hom = ((map₂ α' β').obj X).hom

Tactic:
simp [dsimp% congr($(hβ).app X.right)]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: case h₀
C : Type u
inst✝³ : Category.{v, u} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback (G.map f) (G.map g)
W : C
h : W ⟶ X
k : W ⟶ Y
w : h ≫ f = k ≫ g
⊢ (G.map (pullback.lift h k w) ≫ pullbackComparison G f g) ≫ pullback.fst (G.map f) (G.map g) =
    pullback.lift (G.map h) (G.map k) ⋯ ≫ pullback.fst (G.map f) (G.map g)

Tactic:
simp [← G.map_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: case h₁
C : Type u
inst✝³ : Category.{v, u} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback (G.map f) (G.map g)
W : C
h : W ⟶ X
k : W ⟶ Y
w : h ≫ f = k ≫ g
⊢ (G.map (pullback.lift h k w) ≫ pullbackComparison G f g) ≫ pullback.snd (G.map f) (G.map g) =
    pullback.lift (G.map h) (G.map k) ⋯ ≫ pullback.snd (G.map f) (G.map g)

Tactic:
simp [← G.map_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: case h₀
C : Type u
inst✝³ : Category.{v, u} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasPushout f g
inst✝ : HasPushout (G.map f) (G.map g)
W : C
h : Y ⟶ W
k : Z ⟶ W
w : f ≫ h = g ≫ k
⊢ pushout.inl (G.map f) (G.map g) ≫ pushoutComparison G f g ≫ G.map (pushout.desc h k w) =
    pushout.inl (G.map f) (G.map g) ≫ pushout.desc (G.map h) (G.map k) ⋯

Tactic:
simp [← G.map_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

Goal state before:
pp: case h₁
C : Type u
inst✝³ : Category.{v, u} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasPushout f g
inst✝ : HasPushout (G.map f) (G.map g)
W : C
h : Y ⟶ W
k : Z ⟶ W
w : f ≫ h = g ≫ k
⊢ pushout.inr (G.map f) (G.map g) ≫ pushoutComparison G f g ≫ G.map (pushout.desc h k w) =
    pushout.inr (G.map f) (G.map g) ≫ pushout.desc (G.map h) (G.map k) ⋯

Tactic:
simp [← G.map_comp]

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
T T' T'' : D
Y Y' Y'' : C
S✝ S' : C ⥤ D
A : Type u₃
inst✝¹ : Category.{v₃, u₃} A
B : Type u₄
inst✝ : Category.{v₄, u₄} B
F : B ⥤ C
G : C ⥤ D
S : C
X✝ Y✝ : CostructuredArrow F S
f : X✝ ⟶ Y✝
⊢ (F ⋙ G).map f.left ≫ (mk (G.map Y✝.hom)).hom = (mk (G.map X✝.hom)).hom

Tactic:
simp [← G.map_comp]

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
T T' T'' : D
Y Y' Y'' : C
S✝ S' : C ⥤ D
A : Type u₃
inst✝¹ : Category.{v₃, u₃} A
B : Type u₄
inst✝ : Category.{v₄, u₄} B
F : B ⥤ C
G : C ⥤ D
S : C
X✝ Y✝ : CostructuredArrow F S
f : X✝ ⟶ Y✝
⊢ (F ⋙ G).map f.left ≫ (mk (G.map Y✝.hom)).hom = (mk (G.map X✝.hom)).hom

Tactic:
by simp [← G.map_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Z
g : Y ⟶ Z
f : X ⟶ Y
inst✝ : Mono f
s : PullbackCone f f
m : s.pt ⟶ X
m₁ : m ≫ 𝟙 X = s.fst
x✝ : m ≫ 𝟙 X = s.snd
⊢ m = s.fst

Tactic:
by
    simpa using m₁

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Y
g : X ⟶ Z
f : X ⟶ Y
inst✝ : Epi f
s : PushoutCocone f f
m : Y ⟶ s.pt
m₁ : 𝟙 Y ≫ m = s.inl
x✝ : 𝟙 Y ≫ m = s.inr
⊢ m = s.inl

Tactic:
by
    simpa using m₁

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

Goal state before:
pp: j : WalkingParallelPairᵒᵖ
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j = (𝟭 WalkingParallelPairᵒᵖ).obj j

Tactic:
by
            induction j with | _ X
            cases X <;> rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Goal state before:
pp: case h₀
C✝ : Type u
inst✝³ : Category.{v, u} C✝
W✝ X✝ Y✝ Z✝ : C✝
C : Type u_1
inst✝² : Category.{v_1, u_1} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasPushout f g
inst✝ : HasBinaryCoproduct Y Z
W : C
i₁ i₂ : pushout f g ⟶ W
h : coprod.desc (pushout.inl f g) (pushout.inr f g) ≫ i₁ = coprod.desc (pushout.inl f g) (pushout.inr f g) ≫ i₂
⊢ pushout.inl f g ≫ i₁ = pushout.inl f g ≫ i₂

Tactic:
simpa using congrArg (fun f => coprod.inl ≫ f) h

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝¹ : HasImage f
W : C
g h : image f ⟶ W
inst✝ : HasLimit (parallelPair g h)
w : factorThruImage f ≫ g = factorThruImage f ≫ h
q : equalizer g h ⟶ image f := equalizer.ι g h
e' : X ⟶ equalizer g h := equalizer.lift (factorThruImage f) w
F' : MonoFactorisation f := { I := equalizer g h, m := q ≫ ι f, m_mono := ⋯, e := e', fac := ⋯ }
v : image f ⟶ F'.I := lift F'
t₀ : v ≫ q ≫ ι f = ι f
t : v ≫ q = 𝟙 (image f)
⊢ g = 𝟙 (image f) ≫ g

Tactic:
by rw [Category.id_comp]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝¹ : HasImage f
W : C
g h : image f ⟶ W
inst✝ : HasLimit (parallelPair g h)
w : factorThruImage f ≫ g = factorThruImage f ≫ h
q : equalizer g h ⟶ image f := equalizer.ι g h
e' : X ⟶ equalizer g h := equalizer.lift (factorThruImage f) w
F' : MonoFactorisation f := { I := equalizer g h, m := q ≫ ι f, m_mono := ⋯, e := e', fac := ⋯ }
v : image f ⟶ F'.I := lift F'
t₀ : v ≫ q ≫ ι f = ι f
t : v ≫ q = 𝟙 (image f)
⊢ 𝟙 (image f) ≫ h = h

Tactic:
by rw [Category.id_comp]

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

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
F : C ⥤ D
inst✝ : F.IsEquivalence
h : HasStrongEpiMonoFactorisations C
X Y : D
f : X ⟶ Y
em : StrongEpiMonoFactorisation (F.inv.map f) := ⋯.some
this✝ : Mono (F.map em.m ≫ F.asEquivalence.counitIso.hom.app Y)
this : StrongEpi (F.asEquivalence.counitIso.inv.app X ≫ F.map em.e)
⊢ (F.asEquivalence.counitIso.inv.app X ≫ F.map em.e) ≫ F.map em.m ≫ F.asEquivalence.counitIso.hom.app Y = f

Tactic:
simp only [Category.assoc, ← F.map_comp_assoc,
              MonoFactorisation.fac, fun_inv_map, id_obj, Iso.inv_hom_id_app, Category.comp_id,
              Iso.inv_hom_id_app_assoc]

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

Goal state before:
pp: C : Type u
X Y : C
inst✝³ : Category.{v, u} C
f g : X ⟶ Y
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasEqualizer f g
inst✝ : HasEqualizer (G.map f) (G.map g)
Z : C
h : Z ⟶ X
w : h ≫ f = h ≫ g
⊢ (G.map (equalizer.lift h w) ≫ equalizerComparison f g G) ≫ equalizer.ι (G.map f) (G.map g) =
    equalizer.lift (G.map h) ⋯ ≫ equalizer.ι (G.map f) (G.map g)

Tactic:
simp [← G.map_comp]

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

Goal state before:
pp: C : Type u
X Y : C
inst✝³ : Category.{v, u} C
f g : X ⟶ Y
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasCoequalizer f g
inst✝ : HasCoequalizer (G.map f) (G.map g)
Z : C
h : Y ⟶ Z
w : f ≫ h = g ≫ h
⊢ coequalizer.π (G.map f) (G.map g) ≫ coequalizerComparison f g G ≫ G.map (coequalizer.desc h w) =
    coequalizer.π (G.map f) (G.map g) ≫ coequalizer.desc (G.map h) ⋯

Tactic:
simp [← G.map_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
J : Type w
inst✝³ : Category.{w', w} J
F : J ⥤ C
G : C ⥤ D
inst✝² : G.ReflectsIsomorphisms
inst✝¹ : HasLimit F
inst✝ : PreservesLimit F G
c : Cone F
t : IsLimit (G.mapCone c)
this : IsIso ((Cone.functoriality F G).map ((limit.isLimit F).liftConeMorphism c))
⊢ IsIso ((limit.isLimit F).liftConeMorphism c)

Tactic:
apply isIso_of_reflects_iso _ (Cone.functoriality F G)

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

Goal state before:
pp: case refine_2
J : Type w
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
D : Type uD
inst✝¹ : Category.{uD', uD} D
inst✝ : HasZeroMorphisms D
F : J → C
K : Type w'
f : J → C
c : Bicone f
g : K ≃ J
hc : (c.whisker g).IsBilimit
⊢ IsColimit c.toCocone

Tactic:
let := IsColimit.ofIsoColimit hc.isColimit (Bicone.whiskerToCocone c g)
    let := (IsColimit.precomposeHomEquiv (Discrete.functorComp f g) _) this
    exact IsColimit.ofWhiskerEquivalence (Discrete.equivalence g) this

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms D
G : C ⥤ D
inst✝² : G.PreservesZeroMorphisms
inst✝¹ : HasKernel f
inst✝ : HasKernel (G.map f)
Z : C
h : Z ⟶ X
w : h ≫ f = 0
⊢ (G.map (kernel.lift f h w) ≫ kernelComparison f G) ≫ equalizer.ι (G.map f) 0 =
    kernel.lift (G.map f) (G.map h) ⋯ ≫ equalizer.ι (G.map f) 0

Tactic:
simp [← G.map_comp]

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms D
G : C ⥤ D
inst✝² : G.PreservesZeroMorphisms
inst✝¹ : HasCokernel f
inst✝ : HasCokernel (G.map f)
Z : C
h : Y ⟶ Z
w : f ≫ h = 0
⊢ coequalizer.π (G.map f) 0 ≫ cokernelComparison f G ≫ G.map (cokernel.desc f h w) =
    coequalizer.π (G.map f) 0 ≫ cokernel.desc (G.map f) (G.map h) ⋯

Tactic:
simp [← G.map_comp]

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

Goal state before:
pp: J : Type w
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
inst✝¹ : HasBiproduct f
p : J → Prop
inst✝ : HasBiproduct (Subtype.restrict p f)
j : Subtype p
⊢ (fromSubtype f p ≫ toSubtype f p) ≫ π (Subtype.restrict p f) j =
    𝟙 (⨁ Subtype.restrict p f) ≫ π (Subtype.restrict p f) j

Tactic:
rw [Category.assoc, biproduct.toSubtype_π, biproduct.fromSubtype_π_subtype, Category.id_comp]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
t : BinaryBicone X Y
ht : IsLimit t.toCone
⊢ t.inl = BinaryFan.IsLimit.lift ht (𝟙 X) 0

Tactic:
apply ht.uniq (BinaryFan.mk (𝟙 X) 0)

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
t : BinaryBicone X Y
ht : IsLimit t.toCone
⊢ ∀ (j : Discrete WalkingPair), t.inl ≫ t.toCone.π.app j = (BinaryFan.mk (𝟙 X) 0).π.app j
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: case h₁.h₀
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ (inr ≫ map f g) ≫ fst = (inr ≫ map' f g) ≫ fst

Tactic:
simp only [mapPair_right, IsColimit.ι_map, IsLimit.map_π,
      Category.assoc, ← BinaryBicone.toCone_π_app_left, ←
      BinaryBicone.toCocone_ι_app_right]

Goal state after:
case h₁.h₀
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ (BinaryBiproduct.bicone W X).toCocone.ι.app { as := WalkingPair.right } ≫
      (BinaryBiproduct.bicone W X).toCone.π.app { as := WalkingPair.left } ≫
        (mapPair f g).app { as := WalkingPair.left } =
    g ≫
      (BinaryBiproduct.bicone Y Z).toCocone.ι.app { as := WalkingPair.right } ≫
        (BinaryBiproduct.bicone Y Z).toCone.π.app { as := WalkingPair.left }
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: case neg
ι : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq (ι → ℕ)
s : Finset ι
m n : ℕ
hn : n ≠ 0
f : ι → ℕ
hfsum : s.sum f = n * m
hfsup : ∀ (i : ι), f i ≠ 0 → i ∈ s
hfdvd : ∀ i ∈ s, n ∣ f i
i : ι
hi : i ∉ s
⊢ n ∣ f i

Tactic:
rw [not_imp_comm.1 (hfsup _) hi]
      exact dvd_zero _

Goal state after:
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
h : f (f x) ≠ x
hx : ¬f x = x
z : α
hzx : z = x
⊢ z ∈ (swap x (f x) * f).support ↔ z ∈ f.support \ {x}

pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
h : f (f x) ≠ x
hx : ¬f x = x
z : α
hzx : ¬z = x
⊢ z ∈ (swap x (f x) * f).support ↔ z ∈ f.support \ {x}

Tactic:
· simp [hzx]

Goal state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
x : α
h : f (f x) ≠ x
hx : ¬f x = x
z : α
hzx : ¬z = x
⊢ z ∈ (swap x (f x) * f).support ↔ z ∈ f.support \ {x}
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case cons.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f hd : Perm α
tl : List (Perm α)
IH : f ∈ tl → List.Pairwise Disjoint tl → ∀ x ∈ f.support, f x = tl.prod x
hl : (∀ a' ∈ tl, hd.Disjoint a') ∧ List.Pairwise Disjoint tl
x : α
hx : x ∈ f.support
h : f ∈ tl
⊢ f x = (hd :: tl).prod x

Tactic:
rw [List.prod_cons, mul_apply, ← IH h hl.right _ hx, eq_comm, ← notMem_support]

Goal state after:
case cons.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f hd : Perm α
tl : List (Perm α)
IH : f ∈ tl → List.Pairwise Disjoint tl → ∀ x ∈ f.support, f x = tl.prod x
hl : (∀ a' ∈ tl, hd.Disjoint a') ∧ List.Pairwise Disjoint tl
x : α
hx : x ∈ f.support
h : f ∈ tl
⊢ f x ∉ hd.support
Module: Mathlib.GroupTheory.Perm.Finite

Goal state before:
pp: α : Type u
β : Type v
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
σ τ : Perm α
h : σ.Disjoint τ
⊢ (σ.extendDomain f).Disjoint (τ.extendDomain f)

Tactic:
by
  intro b
  by_cases pb : p b
  · refine (h (f.symm ⟨b, pb⟩)).imp ?_ ?_ <;>
      · intro h
        rw [extendDomain_apply_subtype _ _ pb, h, apply_symm_apply, Subtype.coe_mk]
  · left
    rw [extendDomain_apply_not_subtype _ _ pb]

Goal state after:
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: case h.h
α : Type u_1
inst✝ : DecidableEq α
x y x' y' : α
l l' : List α
hd : (x :: y :: l).Nodup
hd' : (x' :: y' :: l').Nodup
h : ∀ (x_1 : α), (x :: y :: l).formPerm x_1 = (x' :: y' :: l').formPerm x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < (x :: y :: l).length
hx' : (x :: y :: l).get ⟨n, hn⟩ = x'
hl : (x :: y :: l).length = (x' :: y' :: l').length
⊢ ∀ (i : ℕ) (h₁ : i < ((x :: y :: l).rotate n).length) (h₂ : i < (x' :: y' :: l').length),
    ((x :: y :: l).rotate n)[i] = (x' :: y' :: l')[i]

Tactic:
intro k hk hk'

Goal state after:
case h.h
α : Type u_1
inst✝ : DecidableEq α
x y x' y' : α
l l' : List α
hd : (x :: y :: l).Nodup
hd' : (x' :: y' :: l').Nodup
h : ∀ (x_1 : α), (x :: y :: l).formPerm x_1 = (x' :: y' :: l').formPerm x_1
hx : x' ∈ x :: y :: l
n : ℕ
hn : n < (x :: y :: l).length
hx' : (x :: y :: l).get ⟨n, hn⟩ = x'
hl : (x :: y :: l).length = (x' :: y' :: l').length
k : ℕ
hk : k < ((x :: y :: l).rotate n).length
hk' : k < (x' :: y' :: l').length
⊢ ((x :: y :: l).rotate n)[k] = (x' :: y' :: l')[k]
Module: Mathlib.GroupTheory.Perm.Cycle.Basic

Goal state before:
pp: α : Type u_2
f : Perm α
x y : α
n : ℤ
⊢ f.SameCycle x ((f ^ n) y) ↔ f.SameCycle x y

Tactic:
by
  rw [sameCycle_comm, sameCycle_zpow_left, sameCycle_comm]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: n : ℕ
x✝ : (_ : Fin (n + 2)) × Fin (n + 2)
x₁ x₂ : Fin (n + 2)
⊢ ⟨x₁, x₂⟩ ∈ {⟨1, 0⟩} → ⟨x₁, x₂⟩ ∈ finPairsLT (n + 2)

Tactic:
by
      simp +contextual [mem_finPairsLT]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Sign

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
hy : ∀ (y : α), (swap x (f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(((e.symm.trans (Equiv.trans f (swap x (f x)))).trans e) x✝) =
    ↑((swap (e x) (e (f x)) * (e.symm.trans f).trans e) x✝)

Tactic:
mul_def

Goal state after:
α : Type u
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = f x
hy : ∀ (y : α), (swap x (f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(((e.symm.trans (Equiv.trans f (swap x (f x)))).trans e) x✝) =
    ↑((((e.symm.trans f).trans e).trans (swap (e x) (e (f x)))) x✝)