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

Goal state before:
pp: J : Type v₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
F : Discrete J ⥤ C
j : Discrete J
f : j ⟶ j
⊢ F.map f = 𝟙 (F.obj j)

Tactic:
by
  have h : f = 𝟙 j := by cat_disch
  rw [h]
  simp

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

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
W : Set (MorphismProperty C)
Q : MorphismProperty C
h : ∀ W' ∈ W, W'.RespectsLeft Q
X✝ Y✝ Z✝ : C
x✝¹ : X✝ ⟶ Y✝
hi : Q x✝¹
x✝ : Y✝ ⟶ Z✝
hf : InfSet.sInf W x✝
⊢ InfSet.sInf W (x✝¹ ≫ x✝)

Tactic:
rw [sInf_iff] at hf ⊢
    exact fun _ hW' ↦ (h _ hW').precomp _ hi _ (hf _ hW')

Goal state after:
Module: Mathlib.CategoryTheory.ConcreteCategory.Forget

Goal state before:
pp: C : Type u_1
inst✝¹⁰ : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type w
inst✝⁹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁸ : ConcreteCategory C FC
D : Type u_3
inst✝⁷ : Category.{v_2, u_3} D
FD : D → D → Type u_4
CD : D → Type w
inst✝⁶ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁵ : ConcreteCategory D FD
E : Type u_5
inst✝⁴ : Category.{v_3, u_5} E
FE : E → E → Type u_6
CE : E → Type w
inst✝³ : (X Y : E) → FunLike (FE X Y) (CE X) (CE Y)
inst✝² : ConcreteCategory E FE
inst✝¹ : HasForget₂ C D
inst✝ : HasForget₂ D E
⊢ (CategoryTheory.forget₂ C D ⋙ CategoryTheory.forget₂ D E) ⋙ forget E = forget C

Tactic:
by
    change (CategoryTheory.forget₂ _ D) ⋙ (CategoryTheory.forget₂ D E ⋙ CategoryTheory.forget E) = _
    simp only [HasForget₂.forget_comp]

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
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
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
X Y : Comma L₁ R₁
l : X.left ≅ Y.left
r : X.right ≅ Y.right
h : L₁.map l.hom ≫ Y.hom = X.hom ≫ R₁.map r.hom
⊢ (L₁.mapIso l).inv ≫ X.hom = Y.hom ≫ R₁.map r.inv

Tactic:
Iso.inv_comp_eq,

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
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
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
X Y : Comma L₁ R₁
l : X.left ≅ Y.left
r : X.right ≅ Y.right
h : L₁.map l.hom ≫ Y.hom = X.hom ≫ R₁.map r.hom
⊢ X.hom = (L₁.mapIso l).hom ≫ Y.hom ≫ R₁.map r.inv
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
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
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
L' : A' ⥤ T'
R' : B' ⥤ T'
F₁ : A ⥤ A'
F₂ : B ⥤ B'
F : T ⥤ T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
inst✝⁴ : F.Faithful
inst✝³ : F₁.Full
inst✝² : F₂.Full
inst✝¹ : IsIso α
inst✝ : IsIso β
X Y : Comma L R
φ : (map α β).obj X ⟶ (map α β).obj Y
⊢ F.map (L.map (F₁.preimage φ.left) ≫ Y.hom) = F.map (X.hom ≫ R.map (F₂.preimage φ.right))

Tactic:
← cancel_mono (β.app _),

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
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
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
L' : A' ⥤ T'
R' : B' ⥤ T'
F₁ : A ⥤ A'
F₂ : B ⥤ B'
F : T ⥤ T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
inst✝⁴ : F.Faithful
inst✝³ : F₁.Full
inst✝² : F₂.Full
inst✝¹ : IsIso α
inst✝ : IsIso β
X Y : Comma L R
φ : (map α β).obj X ⟶ (map α β).obj Y
⊢ F.map (L.map (F₁.preimage φ.left) ≫ Y.hom) ≫ β.app Y.right =
    F.map (X.hom ≫ R.map (F₂.preimage φ.right)) ≫ β.app Y.right
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' X : C
Y Y' : D
f : X' ⟶ X
g : X ⟶ G.obj Y'
h : X' ⟶ G.obj Y
k : Y ⟶ Y'
w : f ≫ g = h ≫ G.map k
⊢ F.map f ≫ (adj.homEquiv X Y').symm g = (adj.homEquiv X' Y).symm h ≫ k

Tactic:
by
  rw [← homEquiv_naturality_left_symm, ← homEquiv_naturality_right_symm, w]

Goal state after:
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
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝ : F.IsEquivalence
⊢ (F ⋙ G).IsLeftAdjoint ↔ G.IsLeftAdjoint

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ inferInstance⟩
  let iso : G ≅ F.asEquivalence.inverse ⋙ F ⋙ G :=
    (Functor.leftUnitor _).symm ≪≫ Functor.isoWhiskerRight (F.asEquivalence.counitIso).symm _ ≪≫
      Functor.associator _ _ _
  exact isLeftAdjoint_of_iso iso.symm

Goal state after:
Module: Mathlib.CategoryTheory.Functor.EpiMono

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F G : C ⥤ D
inst✝ : F.ReflectsMonomorphisms
α : F ≅ G
X Y : C
f : X ⟶ Y
h : Mono (G.map f)
⊢ Mono f

Tactic:
apply F.mono_of_mono_map

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F G : C ⥤ D
inst✝ : F.ReflectsMonomorphisms
α : F ≅ G
X Y : C
f : X ⟶ Y
h : Mono (G.map f)
⊢ Mono (F.map f)
Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty.{w + 1} ⥤ C
F₂ : Discrete PEmpty.{w' + 1} ⥤ C
c₁ : Cone F₁
c₂ : Cone F₂
h : c₁.pt ≅ c₂.pt
⊢ Function.RightInverse (fun hl ↦ isLimitChangeEmptyCone C hl c₁ h.symm) fun hl ↦ isLimitChangeEmptyCone C hl c₂ h

Tactic:
dsimp [Function.LeftInverse, Function.RightInverse]; intro
    simp only [eq_iff_true_of_subsingleton]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty.{w + 1} ⥤ C
F₂ : Discrete PEmpty.{w' + 1} ⥤ C
c₁ : Cocone F₁
c₂ : Cocone F₂
h : c₁.pt ≅ c₂.pt
⊢ Function.RightInverse (fun hl ↦ isColimitChangeEmptyCocone C hl c₁ h.symm) fun hl ↦
    isColimitChangeEmptyCocone C hl c₂ h

Tactic:
dsimp [Function.LeftInverse, Function.RightInverse]; intro
    simp only [eq_iff_true_of_subsingleton]

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 : 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

Tactic:
apply BinaryCofan.IsColimit.hom_ext h

Goal state after:
case uniq.h₁
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
⊢ c.inl ≫ m = c.inl ≫ IsColimit.desc h (inv f ≫ s.inl) s.inr

case uniq.h₂
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
⊢ c.inr ≫ m = c.inr ≫ IsColimit.desc h (inv f ≫ s.inl) s.inr
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasTerminal C
inst✝ : HasBinaryProducts C
f : X ⟶ Y
⊢ (leftUnitor X).inv ≫ map (𝟙 (⊤_ C)) f = f ≫ (leftUnitor Y).inv

Tactic:
Iso.inv_comp_eq,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasTerminal C
inst✝ : HasBinaryProducts C
f : X ⟶ Y
⊢ map (𝟙 (⊤_ C)) f = (leftUnitor X).hom ≫ f ≫ (leftUnitor Y).inv
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasTerminal C
inst✝ : HasBinaryProducts C
f : X ⟶ Y
⊢ (prod.rightUnitor X).inv ≫ prod.map f (𝟙 (⊤_ C)) = f ≫ (prod.rightUnitor Y).inv

Tactic:
Iso.inv_comp_eq,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasTerminal C
inst✝ : HasBinaryProducts C
f : X ⟶ Y
⊢ prod.map f (𝟙 (⊤_ C)) = (prod.rightUnitor X).hom ≫ f ≫ (prod.rightUnitor Y).inv
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: X✝ Y✝ : WalkingParallelPair
f : X✝ ⟶ Y✝
⊢ op
      (match X✝ with
      | zero => one
      | one => zero) ⟶
    op
      (match Y✝ with
      | zero => one
      | one => zero)

Tactic:
cases f <;> apply Quiver.Hom.op
    exacts [left, right, WalkingParallelPairHom.id _]

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

Goal state before:
pp: case h_map
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
⊢ autoParam
    (∀ (X_1 Y_1 : Under Z) (f_1 : X_1 ⟶ Y_1), (map (f ≫ g)).map f_1 = eqToHom ⋯ ≫ (map g ⋙ map f).map f_1 ≫ eqToHom ⋯)
    Functor.ext._auto_1

Tactic:
· intro U V k
    ext
    simp

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 ⟶ W
g : Y ⟶ W
i : W ⟶ Z
inst✝ : Mono i
s✝ : PullbackCone f g
H : IsLimit s✝
s : PullbackCone (f ≫ i) (g ≫ i)
l : s.pt ⟶ s✝.pt
h₁ : l ≫ s✝.fst = s.fst
h₂ : l ≫ s✝.snd = s.snd
m : s.pt ⟶ (mk s✝.fst s✝.snd ⋯).pt
hm₁ : m ≫ (mk s✝.fst s✝.snd ⋯).fst = s.fst
⊢ m ≫ (mk s✝.fst s✝.snd ⋯).snd = s.snd → m = l

Tactic:
hm₂

Goal state after:
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✝
s : PullbackCone (f ≫ i) (g ≫ i)
l : s.pt ⟶ s✝.pt
h₁ : l ≫ s✝.fst = s.fst
h₂ : l ≫ s✝.snd = s.snd
m : s.pt ⟶ (mk s✝.fst s✝.snd ⋯).pt
hm₁ : m ≫ (mk s✝.fst s✝.snd ⋯).fst = s.fst
hm₂ : m ≫ (mk s✝.fst s✝.snd ⋯).snd = s.snd
⊢ m = l
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
g : X ⟶ Z
h : W ⟶ X
inst✝ : Epi h
s✝ : PushoutCocone f g
H : IsColimit s✝
s : PushoutCocone (h ≫ f) (h ≫ g)
l : s✝.pt ⟶ s.pt
h₁ : s✝.inl ≫ l = s.inl
h₂ : s✝.inr ≫ l = s.inr
m : (mk s✝.inl s✝.inr ⋯).pt ⟶ s.pt
hm₁ : (mk s✝.inl s✝.inr ⋯).inl ≫ m = s.inl
⊢ (mk s✝.inl s✝.inr ⋯).inr ≫ m = s.inr → m = l

Tactic:
hm₂

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Y
g✝ : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : W ⟶ X
inst✝ : Epi h
s✝ : PushoutCocone f g
H : IsColimit s✝
s : PushoutCocone (h ≫ f) (h ≫ g)
l : s✝.pt ⟶ s.pt
h₁ : s✝.inl ≫ l = s.inl
h₂ : s✝.inr ≫ l = s.inr
m : (mk s✝.inl s✝.inr ⋯).pt ⟶ s.pt
hm₁ : (mk s✝.inl s✝.inr ⋯).inl ≫ m = s.inl
hm₂ : (mk s✝.inl s✝.inr ⋯).inr ≫ m = s.inr
⊢ m = l
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: case one
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
s t : Fork f g
k : s.pt ⟶ t.pt
w : k ≫ t.ι = s.ι
⊢ k ≫ t.π.app one = s.π.app one

Tactic:
· simp only [Fork.app_one_eq_ι_comp_left, ← Category.assoc]
      congr

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroObject C
inst✝² : HasZeroObject D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroMorphisms D
F : C ⥤ D
i : F.obj 0 ≅ 0
X Y : C
⊢ F.map 0 = F.map 0 ≫ F.map 0

Tactic:
by rw [← Functor.map_comp, comp_zero]

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✝
K✝ : J✝ ⥤ C
F : C ⥤ D
inst✝¹ : F.Full
inst✝ : F.Faithful
J : Type w'
𝒥₁ : Category.{w, w'} J
K : J ⥤ C
c : Cocone K
t : IsColimit (F.mapCocone c)
⊢ ∀ (s : Cocone K) (m : c ⟶ s),
    m = (Cocone.functoriality K F).preimage (t.descCoconeMorphism ((Cocone.functoriality K F).obj s))

Tactic:
apply fun s m => (Cocone.functoriality K F).map_injective _

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J✝ : Type w
inst✝² : Category.{w', w} J✝
K✝ : J✝ ⥤ C
F : C ⥤ D
inst✝¹ : F.Full
inst✝ : F.Faithful
J : Type w'
𝒥₁ : Category.{w, w'} J
K : J ⥤ C
c : Cocone K
t : IsColimit (F.mapCocone c)
⊢ ∀ (s : Cocone K) (m : c ⟶ s),
    (Cocone.functoriality K F).map m =
      (Cocone.functoriality K F).map
        ((Cocone.functoriality K F).preimage (t.descCoconeMorphism ((Cocone.functoriality K F).obj s)))
Module: Mathlib.CategoryTheory.Preadditive.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
P✝ Q✝ R : C
f✝ f' : P✝ ⟶ Q✝
g✝ g'✝ : Q✝ ⟶ R
P Q : C
f : P ⟶ Q
inst✝ : Epi f
Z✝ : C
g g' : Q ⟶ Z✝
H : (-f) ≫ g = (-f) ≫ g'
⊢ g = g'

Tactic:
by rwa [neg_comp, neg_comp, ← comp_neg, ← comp_neg, cancel_epi, neg_inj] at H

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
c : CokernelCofork (f - g)
⊢ f ≫ Cofork.π c = g ≫ Cofork.π c

Tactic:
rw [← sub_eq_zero, ← sub_comp, c.condition]

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
α : Sort u_1
P : α → ObjectProperty C
X Y : C
e : X ≅ Y
a : α
hY : P a Y
⊢ ∃ a, (P a).isoClosure X

Tactic:
exact ⟨a, _, hY, ⟨e⟩⟩

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

Tactic:
cases j
      · exact fac s
      · simp

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
⊢ (exactFunctor C D).IsClosedUnderIsomorphisms

Tactic:
by
  dsimp [exactFunctor]
  infer_instance

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
W : C
g : Y ⟶ W
h : X ⟶ W
c : KernelFork h
i : IsLimit c
hf : Fork.ι c ≫ f = 0
hfg : f ≫ g = h
s : Fork f 0
⊢ i.lift (KernelFork.ofι s.ι ⋯) ≫ Fork.ι (KernelFork.ofι (Fork.ι c) hf) = s.ι

Tactic:
simp only [KernelFork.ι_ofι, Fork.IsLimit.lift_ι]

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

Goal state before:
pp: case neg
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : F.PreservesZeroMorphisms
J : Type w₁
f : J → C
b : Bicone f
j j' : J
h : ¬j = j'
⊢ F.map (b.ι j ≫ b.π j') = 0

Tactic:
bicone_ι_π_ne _ h,

Goal state after:
case neg
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : F.PreservesZeroMorphisms
J : Type w₁
f : J → C
b : Bicone f
j j' : J
h : ¬j = j'
⊢ F.map 0 = 0
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: J : Type w
C : Type uC
inst✝¹ : Category.{uC', uC} C
inst✝ : HasZeroMorphisms C
F : J → C
B : Bicone F
j : J
⊢ B.ι j ≫ B.π j = 𝟙 (F j)

Tactic:
simpa using B.ι_π j j

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
⊢ ι f ↑j ≫ toSubtype f p = ι (Subtype.restrict p f) j

Tactic:
ext
  rw [biproduct.toSubtype, Category.assoc, biproduct.lift_π, biproduct.ι_π, biproduct.ι_π]
  split_ifs with h₁ h₂ h₂
  exacts [rfl, False.elim (h₂ (Subtype.ext h₁)), False.elim (h₁ (congr_arg Subtype.val h₂)), rfl]

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
b : BinaryBicone X Y
total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.pt
s : Cone (pair X Y)
m : s.pt ⟶ b.toCone.pt
h : ∀ (j : Discrete WalkingPair), m ≫ b.toCone.π.app j = s.π.app j
hₗ : m ≫ b.toCone.π.app { as := WalkingPair.left } = s.π.app { as := WalkingPair.left }
hᵣ : m ≫ b.toCone.π.app { as := WalkingPair.right } = s.π.app { as := WalkingPair.right }
⊢ m = BinaryFan.fst s ≫ b.inl + BinaryFan.snd s ≫ b.inr

Tactic:
dsimp at hₗ hᵣ

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
b : BinaryBicone X Y
total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.pt
s : Cone (pair X Y)
m : s.pt ⟶ b.toCone.pt
h : ∀ (j : Discrete WalkingPair), m ≫ b.toCone.π.app j = s.π.app j
hₗ : m ≫ b.fst = s.π.app { as := WalkingPair.left }
hᵣ : m ≫ b.snd = s.π.app { as := WalkingPair.right }
⊢ m = BinaryFan.fst s ≫ b.inl + BinaryFan.snd s ≫ b.inr
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: 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✝
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
i : J
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct (Subtype.restrict (fun j ↦ j ≠ i) f)
s : Fork (π f i) 0
⊢ ∀ {m : s.pt ⟶ (KernelFork.ofι (fromSubtype f fun j ↦ j ≠ i) ⋯).pt},
    m ≫ Fork.ι (KernelFork.ofι (fromSubtype f fun j ↦ j ≠ i) ⋯) = s.ι → m = s.ι ≫ toSubtype f fun j ↦ j ≠ i

Tactic:
intro m hm
      rw [← hm, KernelFork.ι_ofι, Category.assoc, biproduct.fromSubtype_toSubtype]
      exact (Category.comp_id _).symm

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
b : BinaryBicone X Y
total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.pt
s : Cocone (pair X Y)
m : b.toCocone.pt ⟶ s.pt
h : ∀ (j : Discrete WalkingPair), b.toCocone.ι.app j ≫ m = s.ι.app j
hₗ : b.toCocone.ι.app { as := WalkingPair.left } ≫ m = s.ι.app { as := WalkingPair.left }
hᵣ : b.toCocone.ι.app { as := WalkingPair.right } ≫ m = s.ι.app { as := WalkingPair.right }
⊢ m = b.fst ≫ BinaryCofan.inl s + b.snd ≫ BinaryCofan.inr s

Tactic:
dsimp at hₗ hᵣ

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
b : BinaryBicone X Y
total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.pt
s : Cocone (pair X Y)
m : b.toCocone.pt ⟶ s.pt
h : ∀ (j : Discrete WalkingPair), b.toCocone.ι.app j ≫ m = s.ι.app j
hₗ : b.inl ≫ m = s.ι.app { as := WalkingPair.left }
hᵣ : b.inr ≫ m = s.ι.app { as := WalkingPair.right }
⊢ m = b.fst ≫ BinaryCofan.inl s + b.snd ≫ BinaryCofan.inr s
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C✝ : Type u
inst✝⁴ : Category.{v, u} C✝
inst✝³ : Preadditive C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
a b : Preadditive C
X Y : C
f g : X ⟶ Y
h₁ : f + g = biprod.lift (𝟙 X) (𝟙 X) ≫ biprod.desc f g
h₂ : f + g = biprod.lift (𝟙 X) (𝟙 X) ≫ biprod.desc f g
⊢ f + g = f + g

Tactic:
refine h₁.trans (Eq.trans ?_ h₂.symm)

Goal state after:
C✝ : Type u
inst✝⁴ : Category.{v, u} C✝
inst✝³ : Preadditive C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
a b : Preadditive C
X Y : C
f g : X ⟶ Y
h₁ : f + g = biprod.lift (𝟙 X) (𝟙 X) ≫ biprod.desc f g
h₂ : f + g = biprod.lift (𝟙 X) (𝟙 X) ≫ biprod.desc f g
⊢ biprod.lift (𝟙 X) (𝟙 X) ≫ biprod.desc f g = biprod.lift (𝟙 X) (𝟙 X) ≫ biprod.desc f g
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: case mpr
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
f : ι → ℕ
hf : ∀ (i : ι), ¬f i = 0 → i ∈ s
⊢ ∃ s_1, (∀ a ∈ s_1, a ∈ s) ∧ s_1.card = s.sum f ∧ ∀ (x : ι), Multiset.count x s_1 = f x

Tactic:
refine ⟨∑ a ∈ s, f a • {a}, ?_, ?_⟩

Goal state after:
case mpr.refine_1
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
f : ι → ℕ
hf : ∀ (i : ι), ¬f i = 0 → i ∈ s
⊢ ∀ a ∈ ∑ a ∈ s, f a • {a}, a ∈ s

case mpr.refine_2
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
f : ι → ℕ
hf : ∀ (i : ι), ¬f i = 0 → i ∈ s
⊢ (∑ a ∈ s, f a • {a}).card = s.sum f ∧ ∀ (x : ι), Multiset.count x (∑ a ∈ s, f a • {a}) = f x
Module: Mathlib.Combinatorics.Enumerative.Partition.Basic

Goal state before:
pp: n : ℕ
p : n.Partition
m : ℕ
h : m ∈ p.parts
⊢ m ≤ n

Tactic:
by
  simpa [p.parts_sum] using Multiset.le_sum_of_mem h

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

Goal state before:
pp: n : ℕ
σ : Type u_1
s : Sym σ n
inst✝ : DecidableEq σ
⊢ ∑ a ∈ (↑s).toFinset, count a ↑s = n

Tactic:
rw [toFinset_sum_count_eq]

Goal state after:
n : ℕ
σ : Type u_1
s : Sym σ n
inst✝ : DecidableEq σ
⊢ (↑s).card = n
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: c c' : (n : ℕ) × Composition n
H : c.snd.blocks = c'.snd.blocks
⊢ c = c'

Tactic:
rcases c with ⟨n, c⟩

Goal state after:
c' : (n : ℕ) × Composition n
n : ℕ
c : Composition n
H : ⟨n, c⟩.snd.blocks = c'.snd.blocks
⊢ ⟨n, c⟩ = c'
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
⊢ ∀ (a : α), True

Tactic:
imp_true_iff

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g c : Perm α
s : Finset α
hg : ∀ (x : α), g x ∈ s ↔ x ∈ s
⊢ ofSubtype (g.subtypePerm hg) = c ↔
    c.support ⊆ s ∧ ∀ (hc' : ∀ (x : α), c x ∈ s ↔ x ∈ s), c.subtypePerm hc' = g.subtypePerm hg

Tactic:
simp only [Equiv.ext_iff, subtypePerm_apply, Subtype.mk.injEq, Subtype.forall]
  constructor
  · intro h
    constructor
    · intro a ha
      by_contra ha'
      rw [mem_support, ← h a, ofSubtype_apply_of_not_mem (p := (· ∈ s)) _ ha'] at ha
      exact ha rfl
    · intro _ a ha
      rw [← h a, ofSubtype_apply_of_mem (p := (· ∈ s)) _ ha, subtypePerm_apply]
  · rintro ⟨hc, h⟩ a
    specialize h (isInvariant_of_support_le hc)
    by_cases ha : a ∈ s
    · rw [h a ha, ofSubtype_apply_of_mem (p := (· ∈ s)) _ ha, subtypePerm_apply]
    · rw [ofSubtype_apply_of_not_mem (p := (· ∈ s)) _ ha, eq_comm, ← notMem_support]
      exact Finset.notMem_mono hc ha

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq β
inst✝ : Fintype β
s : Finset α
f : α → Perm β
comm : (↑s).Pairwise (Commute on f)
x : β
hx : ∀ a ∈ s, x ∉ (f a).support
⊢ x ∉ (s.noncommProd f comm).support

Tactic:
revert hx comm s

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : α → Perm β
x : β
⊢ ∀ {s : Finset α} {comm : (↑s).Pairwise (Commute on f)},
    (∀ a ∈ s, x ∉ (f a).support) → x ∉ (s.noncommProd f comm).support
Module: Mathlib.GroupTheory.Perm.Support

Goal state before:
pp: case neg
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
pb : ¬p b
⊢ ¬(g.extendDomain f) b = b ↔ ∃ a, ¬g a = a ∧ f.asEmbedding a = b

Tactic:
extendDomain_apply_not_subtype _ _ pb

Goal state after:
case neg
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
β : Type u_2
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g : Perm α
b : β
pb : ¬p b
⊢ ¬b = b ↔ ∃ a, ¬g a = a ∧ f.asEmbedding a = b