mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
r : α → α → Prop
hr : Std.Symm r
⊢ fromRel hr ⊆ diagSetᶜ ↔ Std.Irrefl r

Tactic:
simp [Set.subset_compl_iff_disjoint_left]

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
z : Sym2 α
h : a ∈ z
⊢ Mem.other h = Mem.other' h

Tactic:
← congr_right,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
z : Sym2 α
h : a ∈ z
⊢ s(?m.14, Mem.other h) = s(?m.14, Mem.other' h)

α : Type u_1
inst✝ : DecidableEq α
a : α
z : Sym2 α
h : a ∈ z
⊢ α
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_4
R : Type u_5
N : Type u_6
inst✝ : SMul R N
f : { f // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }
g : { g // ∀ (a₁ a₂ : α), g a₁ a₂ = g a₂ a₁ }
⊢ lift f • lift g = lift ⟨↑f • ↑g, ⋯⟩

Tactic:
ext ⟨i, j⟩

Goal state after:
case mk
α : Type u_4
R : Type u_5
N : Type u_6
inst✝ : SMul R N
f : { f // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }
g : { g // ∀ (a₁ a₂ : α), g a₁ a₂ = g a₂ a₁ }
x✝ : Sym2 α
i j : α
⊢ (lift f • lift g) (Quot.mk (Rel α) (i, j)) = lift ⟨↑f • ↑g, ⋯⟩ (Quot.mk (Rel α) (i, j))
Module: Mathlib.CategoryTheory.Functor.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
h : F.toPrefunctor = G.toPrefunctor
⊢ F = G

Tactic:
obtain ⟨obj, map, _, _⟩ := F

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
obj : C → D
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
map_id✝ : ∀ (X : C), map (𝟙 X) = 𝟙 (obj X)
map_comp✝ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = map f ≫ map g
h : { obj := obj, map := map, map_id := map_id✝, map_comp := map_comp✝ }.toPrefunctor = G.toPrefunctor
⊢ { obj := obj, map := map, map_id := map_id✝, map_comp := map_comp✝ } = G
Module: Mathlib.Logic.Lemmas

Goal state before:
pp: case pos
f : Prop → Prop
h₁ : f True
h₀ : f False
p : Prop
hp : p
⊢ f True

Tactic:
assumption

Goal state after:
Module: Mathlib.Logic.Lemmas

Goal state before:
pp: case neg
f : Prop → Prop
h₁ : f True
h₀ : f False
p : Prop
hp : ¬p
⊢ f False

Tactic:
assumption

Goal state after:
Module: Mathlib.CategoryTheory.Whiskering

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
X✝ Y✝ : C ⥤ D
τ : X✝ ⟶ Y✝
H : D ⥤ E
X Y : C
f : X ⟶ Y
⊢ ({ obj := fun G ↦ X✝ ⋙ G, map := fun {X Y} α ↦ X✝.whiskerLeft α, map_id := ⋯, map_comp := ⋯ }.obj H).map f ≫
      H.map (τ.app Y) =
    H.map (τ.app X) ≫
      ({ obj := fun G ↦ Y✝ ⋙ G, map := fun {X Y} α ↦ Y✝.whiskerLeft α, map_id := ⋯, map_comp := ⋯ }.obj H).map f

Tactic:
by dsimp; rw [← H.map_comp, ← H.map_comp, ← τ.naturality]

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

Goal state before:
pp: J : Type u₂
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Discrete J ⥤ C
⊢ ∀ {X Y : Discrete J} (f : X ⟶ Y),
    (({ obj := fun F j ↦ F.obj { as := j }, map := fun {X Y} f j ↦ f.app { as := j }, map_id := ⋯, map_comp := ⋯ } ⋙
                  { obj := fun F ↦ Discrete.functor F, map := fun {X Y} f ↦ Discrete.natTrans fun j ↦ f j.as,
                    map_id := ⋯, map_comp := ⋯ }).obj
              F).map
          f ≫
        (Iso.refl
            ((({ obj := fun F j ↦ F.obj { as := j }, map := fun {X Y} f j ↦ f.app { as := j }, map_id := ⋯,
                        map_comp := ⋯ } ⋙
                      { obj := fun F ↦ Discrete.functor F, map := fun {X Y} f ↦ Discrete.natTrans fun j ↦ f j.as,
                        map_id := ⋯, map_comp := ⋯ }).obj
                  F).obj
              Y)).hom =
      (Iso.refl
            ((({ obj := fun F j ↦ F.obj { as := j }, map := fun {X Y} f j ↦ f.app { as := j }, map_id := ⋯,
                        map_comp := ⋯ } ⋙
                      { obj := fun F ↦ Discrete.functor F, map := fun {X Y} f ↦ Discrete.natTrans fun j ↦ f j.as,
                        map_id := ⋯, map_comp := ⋯ }).obj
                  F).obj
              X)).hom ≫
        ((𝟭 (Discrete J ⥤ C)).obj F).map f

Tactic:
rintro ⟨x⟩ ⟨y⟩ f
      obtain rfl : x = y := Discrete.eq_of_hom f
      obtain rfl : f = 𝟙 _ := rfl
      simp

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

Goal state before:
pp: A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
X Y : Comma L R
e : X ⟶ Y
inst✝ : IsIso e
⊢ (e ≫ inv e).left = 𝟙 X.left

Tactic:
IsIso.hom_inv_id,

Goal state after:
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
X Y : Comma L R
e : X ⟶ Y
inst✝ : IsIso e
⊢ (𝟙 X).left = 𝟙 X.left
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
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (F.map f ≫ g) = f ≫ (e X Y) g
Y Y' Y'' : D
g : Y ⟶ Y'
g' : Y' ⟶ Y''
⊢ (e (G_obj Y) Y'') ((e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g ≫ g') =
    (e (G_obj Y) Y') ((e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g) ≫
      (e (G_obj Y') Y'') ((e (G_obj Y') Y').symm (𝟙 (G_obj Y')) ≫ g')

Tactic:
← Equiv.eq_symm_apply,

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
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (F.map f ≫ g) = f ≫ (e X Y) g
Y Y' Y'' : D
g : Y ⟶ Y'
g' : Y' ⟶ Y''
⊢ (e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g ≫ g' =
    (e (G_obj Y) Y'').symm
      ((e (G_obj Y) Y') ((e (G_obj Y) Y).symm (𝟙 (G_obj Y)) ≫ g) ≫
        (e (G_obj Y') Y'') ((e (G_obj Y') Y').symm (𝟙 (G_obj Y')) ≫ g'))
Module: Mathlib.CategoryTheory.Skeletal

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
x✝¹ x✝ : ThinSkeleton C
⊢ ∀ (a b : x✝¹ ⟶ x✝), a = b

Tactic:
rintro ⟨⟨f₁⟩⟩ ⟨⟨_⟩⟩
    rfl

Goal state after:
Module: Mathlib.CategoryTheory.EssentiallySmall

Goal state before:
pp: case mp.left
C : Type u
inst✝ : Category.{v, u} C
S : Type w
𝒮 : SmallCategory S
e : C ≌ S
⊢ Skeleton C ≃ Skeleton S

Tactic:
exact e.skeletonEquiv

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

Goal state before:
pp: case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
⊢ HasLiftingProperty i p → ∀ (φ : mk i ⟶ mk p), Nonempty (LiftStruct φ)

Tactic:
intro _ φ
    have sq : CommSq φ.left i p φ.right := CommSq.mk φ.w
    exact ⟨{ l := sq.lift }⟩

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

Goal state before:
pp: j : WalkingPair
⊢ (fun x ↦
        match x with
        | left => right
        | right => left)
      ((fun x ↦
          match x with
          | left => right
          | right => left)
        j) =
    j

Tactic:
cases j <;> rfl

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

Goal state before:
pp: j : WalkingPair
⊢ (fun b ↦ Bool.recOn b right left)
      ((fun x ↦
          match x with
          | left => true
          | right => false)
        j) =
    j

Tactic:
cases j <;> rfl

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

Goal state before:
pp: case left
C : Type u
inst✝ : Category.{v, u} C
A B : C
c c' : BinaryFan A B
e : c.pt ≅ c'.pt
h₁ : c.fst = e.hom ≫ c'.fst
h₂ : c.snd = e.hom ≫ c'.snd
⊢ c.π.app { as := left } = e.hom ≫ c'.π.app { as := left }

Tactic:
assumption

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

Goal state before:
pp: case right
C : Type u
inst✝ : Category.{v, u} C
A B : C
c c' : BinaryFan A B
e : c.pt ≅ c'.pt
h₁ : c.fst = e.hom ≫ c'.fst
h₂ : c.snd = e.hom ≫ c'.snd
⊢ c.π.app { as := right } = e.hom ≫ c'.π.app { as := right }

Tactic:
assumption

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

Goal state before:
pp: case left
C : Type u
inst✝ : Category.{v, u} C
A B : C
c c' : BinaryCofan A B
e : c.pt ≅ c'.pt
h₁ : c.inl ≫ e.hom = c'.inl
h₂ : c.inr ≫ e.hom = c'.inr
⊢ c.ι.app { as := left } ≫ e.hom = c'.ι.app { as := left }

Tactic:
assumption

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

Goal state before:
pp: case right
C : Type u
inst✝ : Category.{v, u} C
A B : C
c c' : BinaryCofan A B
e : c.pt ≅ c'.pt
h₁ : c.inl ≫ e.hom = c'.inl
h₂ : c.inr ≫ e.hom = c'.inr
⊢ c.ι.app { as := right } ≫ e.hom = c'.ι.app { as := right }

Tactic:
assumption

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

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsTerminal Y
c : BinaryFan X Y
⊢ IsIso c.fst → Nonempty (IsLimit c)

Tactic:
intro
    exact
      ⟨BinaryFan.IsLimit.mk _ (fun f _ => f ≫ inv c.fst) (fun _ _ => by simp)
          (fun _ _ => h.hom_ext _ _) fun _ _ _ e _ => by simp [← e]⟩

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
W X✝ Y✝ Z✝ X Y Z X' Y' Z' X'' Y'' Z'' : C
f : X ⟶ Z
g : Y ⟶ Z
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
f'' : X'' ⟶ Z''
g'' : Y'' ⟶ Z''
i₁ : X ⟶ X'
j₁ : X' ⟶ X''
i₂ : Y ⟶ Y'
j₂ : Y' ⟶ Y''
i₃ : Z ⟶ Z'
j₃ : Z' ⟶ Z''
inst✝² : HasPullback f g
inst✝¹ : HasPullback f' g'
inst✝ : HasPullback f'' g''
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
e₃ : f' ≫ j₃ = j₁ ≫ f''
e₄ : g' ≫ j₃ = j₂ ≫ g''
⊢ g ≫ i₃ ≫ j₃ = (i₂ ≫ j₂) ≫ g''

Tactic:
by rw [reassoc_of% e₂, e₄, Category.assoc]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
W X✝ Y✝ Z✝ X Y Z X' Y' Z' X'' Y'' Z'' : C
f : X ⟶ Y
g : X ⟶ Z
f' : X' ⟶ Y'
g' : X' ⟶ Z'
f'' : X'' ⟶ Y''
g'' : X'' ⟶ Z''
i₁ : X ⟶ X'
j₁ : X' ⟶ X''
i₂ : Y ⟶ Y'
j₂ : Y' ⟶ Y''
i₃ : Z ⟶ Z'
j₃ : Z' ⟶ Z''
inst✝² : HasPushout f g
inst✝¹ : HasPushout f' g'
inst✝ : HasPushout f'' g''
e₁ : f ≫ i₂ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₁ ≫ g'
e₃ : f' ≫ j₂ = j₁ ≫ f''
e₄ : g' ≫ j₃ = j₁ ≫ g''
⊢ g ≫ i₃ ≫ j₃ = (i₁ ≫ j₁) ≫ g''

Tactic:
by rw [reassoc_of% e₂, e₄, Category.assoc]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : IsIso f
⊢ pullback.fst f g = pullback.fst f g ≫ f ≫ inv f

Tactic:
IsIso.hom_inv_id,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : IsIso f
⊢ pullback.fst f g = pullback.fst f g ≫ 𝟙 X
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : IsIso g
⊢ pullback.snd f g = pullback.snd f g ≫ g ≫ inv g

Tactic:
IsIso.hom_inv_id,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : IsIso g
⊢ pullback.snd f g = pullback.snd f g ≫ 𝟙 Y
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : IsIso f
⊢ g ≫ pushout.inr f g ≫ inv (pushout.inr f g) = g

Tactic:
IsIso.hom_inv_id,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : IsIso f
⊢ g ≫ 𝟙 Z = g
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : IsIso g
⊢ f ≫ pushout.inl f g ≫ inv (pushout.inl f g) = f

Tactic:
IsIso.hom_inv_id,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : IsIso g
⊢ f ≫ 𝟙 Y = f
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 ⟶ W
g : Y ⟶ W
i : W ⟶ Z
inst✝ : Mono i
s : PullbackCone f g
H : IsLimit s
⊢ IsLimit (mk s.fst s.snd ⋯)

Tactic:
apply PullbackCone.isLimitAux'
  intro s
  rcases PullbackCone.IsLimit.lift' H s.fst s.snd
      ((cancel_mono i).mp (by simpa using s.condition)) with
    ⟨l, h₁, h₂⟩
  refine ⟨l, h₁, h₂, ?_⟩
  intro m hm₁ hm₂
  exact (PullbackCone.IsLimit.hom_ext H (hm₁.trans h₁.symm) (hm₂.trans h₂.symm) :)

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

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

Tactic:
cases j <;> rfl

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

Goal state before:
pp: case op.op
i j : WalkingParallelPair
f : op i ⟶ op j
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map f ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPairᵒᵖ).map f

Tactic:
let g := f.unop

Goal state after:
case op.op
i j : WalkingParallelPair
f : op i ⟶ op j
g : unop (op j) ⟶ unop (op i) := f.unop
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map f ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPairᵒᵖ).map f
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: j : WalkingParallelPair
⊢ walkingParallelPairOp.map ((NatIso.ofComponents (fun j ↦ eqToIso ⋯) @walkingParallelPairOpEquiv._proof_2).hom.app j) ≫
      (NatIso.ofComponents (fun j ↦ eqToIso ⋯) ⋯).hom.app (walkingParallelPairOp.obj j) =
    𝟙 (walkingParallelPairOp.obj j)

Tactic:
cases j <;> rfl

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : WalkingParallelPair ⥤ C
j : WalkingParallelPair
⊢ (parallelPair (F.map left) (F.map right)).obj j = F.obj j

Tactic:
cases j <;> rfl

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 : WalkingParallelPair ⥤ C
j : WalkingParallelPair
⊢ F.obj j = (parallelPair (F.map left) (F.map right)).obj j

Tactic:
cases j <;> rfl

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 : WalkingParallelPair ⥤ C
p : F.obj zero ⟶ G.obj zero
q : F.obj one ⟶ G.obj one
hl : F.map left ≫ q = p ≫ G.map left
hr : F.map right ≫ q = p ≫ G.map right
⊢ (X : WalkingParallelPair) → F.obj X ⟶ G.obj X

Tactic:
by rintro (_ | _); exacts [p, q]

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 : WalkingParallelPair ⥤ C
p : F.obj zero ≅ G.obj zero
q : F.obj one ≅ G.obj one
hl : F.map left ≫ q.hom = p.hom ≫ G.map left
hr : F.map right ≫ q.hom = p.hom ≫ G.map right
⊢ (X : WalkingParallelPair) → F.obj X ≅ G.obj X

Tactic:
by rintro (_ | _); exacts [p, q]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
f g : Arrow C
inst✝² : HasImage f.hom
inst✝¹ : HasImage g.hom
sq : f ⟶ g
inst✝ : IsIso sq
⊢ image.ι f.hom = image.ι f.hom ≫ (sq ≫ inv sq).right

Tactic:
IsIso.hom_inv_id,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
f g : Arrow C
inst✝² : HasImage f.hom
inst✝¹ : HasImage g.hom
sq : f ⟶ g
inst✝ : IsIso sq
⊢ image.ι f.hom = image.ι f.hom ≫ (𝟙 f).right
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
i : IsZero Y
⊢ IsZero X

Tactic:
by
  obtain rfl := i.eq_zero_of_tgt f
  exact IsZero.of_mono_zero X Y

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
J' : Type w₂
inst✝¹ : Category.{w₂', w₂} J'
e : J ≌ J'
F : C ⥤ D
inst✝ : PreservesColimitsOfShape J F
K : J' ⥤ C
c : Cocone K
t : IsColimit c
⊢ IsColimit (F.mapCocone c)

Tactic:
by
        let equ := e.invFunIdAssoc (K ⋙ F)
        have := (isColimitOfPreserves F (t.whiskerEquivalence e)).whiskerEquivalence e.symm
        apply ((IsColimit.precomposeInvEquiv equ _).symm this).ofIsoColimit
        refine Cocone.ext (Iso.refl _) fun j => ?_
        simp [equ, ← Functor.map_comp]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type w
inst✝¹ : Semiring R
inst✝ : Linear R C
D : Type u'
F : D → C
x✝⁵ x✝⁴ x✝³ : InducedCategory C F
x✝² : x✝⁵ ⟶ x✝⁴
x✝¹ : R
x✝ : x✝⁴ ⟶ x✝³
⊢ x✝² ≫ (x✝¹ • x✝) = x✝¹ • x✝² ≫ x✝

Tactic:
ext; apply comp_smul

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

Goal state before:
pp: case left
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : PreservesFiniteLimits F
inst✝ : PreservesFiniteColimits F
⊢ PreservesFiniteLimits F

Tactic:
assumption

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

Goal state before:
pp: case right
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : PreservesFiniteLimits F
inst✝ : PreservesFiniteColimits F
⊢ PreservesFiniteColimits F

Tactic:
assumption

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
Z : C
l : Z ⟶ X
s : KernelFork f
hs : IsLimit s
i : Z ≅ s.pt
h : i.hom ≫ Fork.ι s = l
j : WalkingParallelPair
⊢ s.π.app j = i.symm.hom ≫ (KernelFork.ofι l ⋯).π.app j

Tactic:
cases j
      · exact (Iso.eq_inv_comp i).2 h
      · dsimp; rw [← h]; simp

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
t : CokernelCofork f
desc : (s : CokernelCofork f) → t.pt ⟶ s.pt
fac : ∀ (s : CokernelCofork f), Cofork.π t ≫ desc s = Cofork.π s
uniq : ∀ (s : CokernelCofork f) (m : t.pt ⟶ s.pt), Cofork.π t ≫ m = Cofork.π s → m = desc s
s : Cocone (parallelPair f 0)
j : WalkingParallelPair
⊢ t.ι.app j ≫ desc s = s.ι.app j

Tactic:
cases j
      · simp
      · exact fac s

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

Goal state before:
pp: J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
⊢ (whiskerEquiv e w).hom = lift fun k ↦ π f (e.symm k) ≫ (w (e.symm k)).inv ≫ eqToHom ⋯

Tactic:
simp only [whiskerEquiv_hom]
  ext k j
  by_cases h : k = e j
  · subst h
    simp
  · simp only [ι_desc_assoc, Category.assoc, lift_π]
    rw [biproduct.ι_π_ne, biproduct.ι_π_ne_assoc]
    · simp
    · rintro rfl
      simp at h
    · exact Ne.symm h

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: case mpr
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCancelCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
i : ι
s : Finset ι
hi : i ∉ s
n : μ
f : ι → μ
⊢ (∃ a b,
      a + b = n ∧
        ∃ a_1,
          (s.sum a_1 = b ∧ ∀ (i : ι), ¬a_1 i = 0 → i ∈ s) ∧
            (addRightEmbedding fun t ↦ if t = i then a else 0) a_1 = f) →
    f i + ∑ x ∈ s, f x = n ∧ ∀ (i_1 : ι), ¬f i_1 = 0 → i_1 = i ∨ i_1 ∈ s

Tactic:
· rintro ⟨a, _, hn, g, ⟨rfl, hg⟩, rfl⟩
    have := hg i
    aesop (add simp [sum_add_distrib])

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Partition.Basic

Goal state before:
pp: n : ℕ
p q : n.Partition
h :
  (fun p ↦ { support := p.parts.toFinset, toFun := fun m ↦ count m p.parts * m, mem_support_toFun := ⋯ }) p =
    (fun p ↦ { support := p.parts.toFinset, toFun := fun m ↦ count m p.parts * m, mem_support_toFun := ⋯ }) q
⊢ p = q

Tactic:
Finsupp.mk.injEq

Goal state after:
n : ℕ
p q : n.Partition
h : p.parts.toFinset = q.parts.toFinset ∧ (fun m ↦ count m p.parts * m) = fun m ↦ count m q.parts * m
⊢ p = q
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
f : Perm α
x : α
hffx : f (f x) = x
n : ℕ
⊢ (f ^ (n + 1 + 1)) x = x ∨ (f ^ (n + 1 + 1)) x = f x

Tactic:
exact pow_apply_eq_of_apply_apply_eq_self hffx _

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

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Preadditive C
D : Type u'
inst✝⁶ : Category.{v', u'} D
inst✝⁵ : Preadditive D
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
J : Type u_1
inst✝³ : Finite J
f : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct (F.obj ∘ f)
inst✝ : Mono (F.biproductComparison f)
⊢ PreservesBiproduct f F

Tactic:
have : HasProduct fun b => F.obj (f b) := by
    change HasProduct (F.obj ∘ f)
    infer_instance
  have that : piComparison F f =
      (F.mapIso (biproduct.isoProduct f)).inv ≫
        biproductComparison F f ≫ (biproduct.isoProduct _).hom := by
    ext j
    convert! piComparison_comp_π F f j; simp [← Function.comp_def, ← Functor.map_comp]
  have : IsIso (biproductComparison F f) := isIso_of_mono_of_isSplitEpi _
  have : IsIso (piComparison F f) := by
    rw [that]
    infer_instance
  have := PreservesProduct.of_iso_comparison F f
  apply preservesBiproduct_of_preservesProduct

Goal state after:
Module: Mathlib.Logic.Equiv.Fintype

Goal state before:
pp: α : Type u_1
p q : α → Prop
inst✝² : DecidablePred p
inst✝¹ : DecidablePred q
inst✝ : Finite ↑{x | p x}
e : { x // p x } ≃ { x // q x }
x : α
hx : p x
⊢ e.extendSubtype x = ↑(e ⟨x, hx⟩)

Tactic:
simp [extendSubtype, subtypeCongr, sumCompl_symm_apply_of_pos hx]

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

Goal state before:
pp: case neg
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
f : { x // x ∈ ↑σ.support } ≃ { x // x ∈ ↑τ.support }
hf : ∀ (x : α) (hx : x ∈ ↑σ.support), ↑(f ⟨σ x, ⋯⟩) = τ ↑(f ⟨x, hx⟩)
x : α
hx : x ∉ σ.support
⊢ f.extendSubtype (σ x) = τ (f.extendSubtype x)

Tactic:
Classical.not_not.1 ((not_congr mem_support).1 (Equiv.extendSubtype_not_mem f _ _)),

Goal state after:
case neg
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
f : { x // x ∈ ↑σ.support } ≃ { x // x ∈ ↑τ.support }
hf : ∀ (x : α) (hx : x ∈ ↑σ.support), ↑(f ⟨σ x, ⋯⟩) = τ ↑(f ⟨x, hx⟩)
x : α
hx : x ∉ σ.support
⊢ f.extendSubtype (σ x) = f.extendSubtype x

α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
f : { x // x ∈ ↑σ.support } ≃ { x // x ∈ ↑τ.support }
hf : ∀ (x : α) (hx : x ∈ ↑σ.support), ↑(f ⟨σ x, ⋯⟩) = τ ↑(f ⟨x, hx⟩)
x : α
hx : x ∉ σ.support
⊢ x ∉ ↑σ.support
Module: Mathlib.GroupTheory.Perm.List

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l : List α
x : α
h : l.formPerm x ≠ x
⊢ x ∈ l

Tactic:
simpa [or_iff_left_of_imp mem_of_mem_tail] using mem_or_mem_of_zipWith_swap_prod_ne h

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

Goal state before:
pp: case cons
α : Type u_1
inst✝ : DecidableEq α
i : ℕ
x : α
xs : List α
w : (x :: xs).Nodup
h : i < (x :: xs).length
⊢ (x :: xs).formPerm (x :: xs)[i] = (x :: xs)[(i + 1) % (x :: xs).length]

Tactic:
· have : i ≤ xs.length := by
      refine Nat.le_of_lt_succ ?_
      simpa using h
    rcases this.eq_or_lt with (rfl | hn')
    · simp
    · rw [formPerm_apply_lt_getElem (x :: xs) w _ (Nat.succ_lt_succ hn')]
      congr
      rw [Nat.mod_eq_of_lt]; simpa [Nat.succ_eq_add_one]

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

Goal state before:
pp: case a.inl
α : Type u_1
inst✝ : DecidableEq α
l : List α
h' : ∀ (x : α), l ≠ [x]
n : ℕ
hn : n < l.length
h : ⟨(n + 1) % l.length, ⋯⟩ = ⟨n, hn⟩
hx : l[n] ∈ l
H : l[(n + 1) % l.length] = l[n]
hn' : n.succ = l.length
⊢ False

Tactic:
simp only [← hn', Nat.mod_self] at h
      refine not_exists.mpr h' ?_
      rw [← length_eq_one_iff, ← hn', (Fin.mk.inj_iff.mp h).symm]

Goal state after:
Module: Mathlib.Data.Int.Order.Units

Goal state before:
pp: u : ℤˣ
⊢ u ^ 2 = 1

Tactic:
rw [Units.ext_iff, Units.val_pow_eq_pow_val, Units.val_one, isUnit_sq u.isUnit]

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

Goal state before:
pp: n : ℕ
i j : Fin (n + 1)
ne : i ≠ j
lt : i < j
⊢ swap i j ∈ ↑(Submonoid.closure (Set.range fun i ↦ swap i.castSucc i.succ))

Tactic:
induction j using Fin.induction with

Goal state after: