mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

Goal state before:
pp: case none
C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
s t : Cone F
i : s.pt ≅ t.pt
w₁ : s.π.app left = i.hom ≫ t.π.app left
w₂ : s.π.app right = i.hom ≫ t.π.app right
h₁ : ((Functor.const WalkingCospan).obj s.pt).map inl ≫ s.π.app one = s.π.app left ≫ F.map inl
⊢ s.π.app none = i.hom ≫ t.π.app none

Tactic:
dsimp at h₁

Goal state after:
case none
C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
s t : Cone F
i : s.pt ≅ t.pt
w₁ : s.π.app left = i.hom ≫ t.π.app left
w₂ : s.π.app right = i.hom ≫ t.π.app right
h₁ : 𝟙 s.pt ≫ s.π.app one = s.π.app left ≫ F.map inl
⊢ s.π.app none = i.hom ≫ t.π.app none
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

Goal state before:
pp: case none
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
s t : Cocone F
i : s.pt ≅ t.pt
w₁ : s.ι.app WalkingCospan.left ≫ i.hom = t.ι.app WalkingCospan.left
w₂ : s.ι.app WalkingCospan.right ≫ i.hom = t.ι.app WalkingCospan.right
h₁ : F.map fst ≫ s.ι.app left = s.ι.app zero ≫ ((Functor.const WalkingSpan).obj s.pt).map fst
⊢ s.ι.app none ≫ i.hom = t.ι.app none

Tactic:
dsimp at h₁

Goal state after:
case none
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
s t : Cocone F
i : s.pt ≅ t.pt
w₁ : s.ι.app WalkingCospan.left ≫ i.hom = t.ι.app WalkingCospan.left
w₂ : s.ι.app WalkingCospan.right ≫ i.hom = t.ι.app WalkingCospan.right
h₁ : F.map fst ≫ s.ι.app left = s.ι.app zero ≫ 𝟙 s.pt
⊢ s.ι.app none ≫ i.hom = t.ι.app none
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 : D
T : C ⥤ D
f : StructuredArrow S T
h : f.IsUniversal
c : C
η η' : f.right ⟶ c
w : f.hom ≫ T.map η = f.hom ≫ T.map η'
⊢ h.desc (mk (f.hom ≫ T.map η)) = h.desc (mk (f.hom ≫ T.map η'))

Tactic:
w

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : D
T : C ⥤ D
f : StructuredArrow S T
h : f.IsUniversal
c : C
η η' : f.right ⟶ c
w : f.hom ≫ T.map η = f.hom ≫ T.map η'
⊢ h.desc (mk (f.hom ≫ T.map η')) = h.desc (mk (f.hom ≫ T.map η'))
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 : D
S : C ⥤ D
f : CostructuredArrow S T
h : f.IsUniversal
c : C
η η' : c ⟶ f.left
w : S.map η ≫ f.hom = S.map η' ≫ f.hom
⊢ h.lift (mk (S.map η ≫ f.hom)) = h.lift (mk (S.map η' ≫ f.hom))

Tactic:
w

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T : D
S : C ⥤ D
f : CostructuredArrow S T
h : f.IsUniversal
c : C
η η' : c ⟶ f.left
w : S.map η ≫ f.hom = S.map η' ≫ f.hom
⊢ h.lift (mk (S.map η' ≫ f.hom)) = h.lift (mk (S.map η' ≫ f.hom))
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
h : W ⟶ X
inst✝¹ : Epi h
inst✝ : HasPushout f g
⊢ h ≫ f ≫ pushout.inl f g = h ≫ g ≫ pushout.inr f g

Tactic:
rw [cancel_epi]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
h : W ⟶ X
inst✝¹ : Epi h
inst✝ : HasPushout f g
⊢ f ≫ pushout.inl f g = g ≫ pushout.inr f g
Module: Mathlib.CategoryTheory.Limits.Shapes.Images

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
F F' : MonoFactorisation f
hI : F.I = F'.I
hm : F.m = eqToHom hI ≫ F'.m
⊢ F = F'

Tactic:
obtain ⟨_, Fm, _, Ffac⟩ := F; obtain ⟨_, Fm', _, Ffac'⟩ := F'
  cases hI
  replace hm : Fm = Fm' := by simpa using hm
  congr
  apply (cancel_mono Fm).1
  rw [Ffac, hm, Ffac']

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
s : Cofork f g
⊢ s.ι.app zero = f ≫ s.π

Tactic:
← s.app_one_eq_π,

Goal state after:
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
s : Cofork f g
⊢ s.ι.app zero = f ≫ s.ι.app one
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
s : Cofork f g
⊢ s.ι.app zero = g ≫ s.π

Tactic:
← s.app_one_eq_π,

Goal state after:
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
s : Cofork f g
⊢ s.ι.app zero = g ≫ s.ι.app one
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
s : Fork f g
W : C
k l : W ⟶ s.pt
h : k ≫ s.ι = l ≫ s.ι
this : k ≫ s.ι ≫ f = l ≫ s.ι ≫ f
⊢ k ≫ s.π.app one = l ≫ s.π.app one

Tactic:
s.app_one_eq_ι_comp_left,

Goal state after:
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
s : Fork f g
W : C
k l : W ⟶ s.pt
h : k ≫ s.ι = l ≫ s.ι
this : k ≫ s.ι ≫ f = l ≫ s.ι ≫ f
⊢ k ≫ s.ι ≫ f = l ≫ s.ι ≫ f
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: case mk
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
J : Type w
𝒥 : Category.{w', w} J
obj✝ : J → C
map✝ : {X Y : J} → (X ⟶ Y) → (obj✝ X ⟶ obj✝ Y)
map_id✝ : ∀ (X : J), map✝ (𝟙 X) = 𝟙 (obj✝ X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), map✝ (f ≫ g) = map✝ f ≫ map✝ g
pt✝ : C
app✝ :
  (X : J) →
    ((Functor.const J).obj pt✝).obj X ⟶ { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    ((Functor.const J).obj pt✝).map f ≫ app✝ Y =
      app✝ X ≫ { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f
h : IsLimit { pt := pt✝, π := { app := app✝, naturality := naturality✝ } }
s : Cone ({ obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ } ⋙ 𝟭 C)
m : s.pt ⟶ ((𝟭 C).mapCone { pt := pt✝, π := { app := app✝, naturality := naturality✝ } }).pt
⊢ (∀ (j : J), m ≫ ((𝟭 C).mapCone { pt := pt✝, π := { app := app✝, naturality := naturality✝ } }).π.app j = s.π.app j) →
    m = h.lift { pt := s.pt, π := { app := fun j ↦ s.π.app j, naturality := ⋯ } }

Tactic:
w

Goal state after:
case mk
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
J : Type w
𝒥 : Category.{w', w} J
obj✝ : J → C
map✝ : {X Y : J} → (X ⟶ Y) → (obj✝ X ⟶ obj✝ Y)
map_id✝ : ∀ (X : J), map✝ (𝟙 X) = 𝟙 (obj✝ X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), map✝ (f ≫ g) = map✝ f ≫ map✝ g
pt✝ : C
app✝ :
  (X : J) →
    ((Functor.const J).obj pt✝).obj X ⟶ { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    ((Functor.const J).obj pt✝).map f ≫ app✝ Y =
      app✝ X ≫ { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f
h : IsLimit { pt := pt✝, π := { app := app✝, naturality := naturality✝ } }
s : Cone ({ obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ } ⋙ 𝟭 C)
m : s.pt ⟶ ((𝟭 C).mapCone { pt := pt✝, π := { app := app✝, naturality := naturality✝ } }).pt
w : ∀ (j : J), m ≫ ((𝟭 C).mapCone { pt := pt✝, π := { app := app✝, naturality := naturality✝ } }).π.app j = s.π.app j
⊢ m = h.lift { pt := s.pt, π := { app := fun j ↦ s.π.app j, naturality := ⋯ } }
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
⊢ Nonempty (StrongEpiMonoFactorisation f)

Tactic:
have : Mono (F.map em.m ≫ F.asEquivalence.counitIso.hom.app Y) := mono_comp _ _

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
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)
⊢ Nonempty (StrongEpiMonoFactorisation f)
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
s t : Cofork f g
i : s.pt ≅ t.pt
w : s.π ≫ i.hom = t.π
⊢ t.π = s.π ≫ i.hom

Tactic:
w

Goal state after:
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
s t : Cofork f g
i : s.pt ≅ t.pt
w : s.π ≫ i.hom = t.π
⊢ t.π = t.π
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: case mk
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
J : Type w
𝒥 : Category.{w', w} J
obj✝ : J → C
map✝ : {X Y : J} → (X ⟶ Y) → (obj✝ X ⟶ obj✝ Y)
map_id✝ : ∀ (X : J), map✝ (𝟙 X) = 𝟙 (obj✝ X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), map✝ (f ≫ g) = map✝ f ≫ map✝ g
pt✝ : C
app✝ :
  (X : J) →
    { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X ⟶ ((Functor.const J).obj pt✝).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f ≫ app✝ Y =
      app✝ X ≫ ((Functor.const J).obj pt✝).map f
h : IsColimit { pt := pt✝, ι := { app := app✝, naturality := naturality✝ } }
s : Cocone ({ obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ } ⋙ 𝟭 C)
m : ((𝟭 C).mapCocone { pt := pt✝, ι := { app := app✝, naturality := naturality✝ } }).pt ⟶ s.pt
⊢ (∀ (j : J),
      ((𝟭 C).mapCocone { pt := pt✝, ι := { app := app✝, naturality := naturality✝ } }).ι.app j ≫ m = s.ι.app j) →
    m = h.desc { pt := s.pt, ι := { app := fun j ↦ s.ι.app j, naturality := ⋯ } }

Tactic:
w

Goal state after:
case mk
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
J : Type w
𝒥 : Category.{w', w} J
obj✝ : J → C
map✝ : {X Y : J} → (X ⟶ Y) → (obj✝ X ⟶ obj✝ Y)
map_id✝ : ∀ (X : J), map✝ (𝟙 X) = 𝟙 (obj✝ X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), map✝ (f ≫ g) = map✝ f ≫ map✝ g
pt✝ : C
app✝ :
  (X : J) →
    { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X ⟶ ((Functor.const J).obj pt✝).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f ≫ app✝ Y =
      app✝ X ≫ ((Functor.const J).obj pt✝).map f
h : IsColimit { pt := pt✝, ι := { app := app✝, naturality := naturality✝ } }
s : Cocone ({ obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ } ⋙ 𝟭 C)
m : ((𝟭 C).mapCocone { pt := pt✝, ι := { app := app✝, naturality := naturality✝ } }).pt ⟶ s.pt
w : ∀ (j : J), ((𝟭 C).mapCocone { pt := pt✝, ι := { app := app✝, naturality := naturality✝ } }).ι.app j ≫ m = s.ι.app j
⊢ m = h.desc { pt := s.pt, ι := { app := fun j ↦ s.ι.app j, naturality := ⋯ } }
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: case mk
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
J : Type w'
𝒥 : Category.{w, w'} J
obj✝ : J → C
map✝ : {X Y : J} → (X ⟶ Y) → (obj✝ X ⟶ obj✝ Y)
map_id✝ : ∀ (X : J), map✝ (𝟙 X) = 𝟙 (obj✝ X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), map✝ (f ≫ g) = map✝ f ≫ map✝ g
pt✝ : C
app✝ :
  (X : J) →
    ((Functor.const J).obj pt✝).obj X ⟶ { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    ((Functor.const J).obj pt✝).map f ≫ app✝ Y =
      app✝ X ≫ { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f
h : IsLimit ((𝟭 C).mapCone { pt := pt✝, π := { app := app✝, naturality := naturality✝ } })
s : Cone { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }
m : s.pt ⟶ { pt := pt✝, π := { app := app✝, naturality := naturality✝ } }.pt
⊢ (∀ (j : J), m ≫ { pt := pt✝, π := { app := app✝, naturality := naturality✝ } }.π.app j = s.π.app j) →
    m = h.lift { pt := s.pt, π := { app := fun j ↦ s.π.app j, naturality := ⋯ } }

Tactic:
w

Goal state after:
case mk
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
J : Type w'
𝒥 : Category.{w, w'} J
obj✝ : J → C
map✝ : {X Y : J} → (X ⟶ Y) → (obj✝ X ⟶ obj✝ Y)
map_id✝ : ∀ (X : J), map✝ (𝟙 X) = 𝟙 (obj✝ X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), map✝ (f ≫ g) = map✝ f ≫ map✝ g
pt✝ : C
app✝ :
  (X : J) →
    ((Functor.const J).obj pt✝).obj X ⟶ { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    ((Functor.const J).obj pt✝).map f ≫ app✝ Y =
      app✝ X ≫ { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f
h : IsLimit ((𝟭 C).mapCone { pt := pt✝, π := { app := app✝, naturality := naturality✝ } })
s : Cone { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }
m : s.pt ⟶ { pt := pt✝, π := { app := app✝, naturality := naturality✝ } }.pt
w : ∀ (j : J), m ≫ { pt := pt✝, π := { app := app✝, naturality := naturality✝ } }.π.app j = s.π.app j
⊢ m = h.lift { pt := s.pt, π := { app := fun j ↦ s.π.app j, naturality := ⋯ } }
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: case mk
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
J : Type w'
𝒥 : Category.{w, w'} J
obj✝ : J → C
map✝ : {X Y : J} → (X ⟶ Y) → (obj✝ X ⟶ obj✝ Y)
map_id✝ : ∀ (X : J), map✝ (𝟙 X) = 𝟙 (obj✝ X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), map✝ (f ≫ g) = map✝ f ≫ map✝ g
pt✝ : C
app✝ :
  (X : J) →
    { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X ⟶ ((Functor.const J).obj pt✝).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f ≫ app✝ Y =
      app✝ X ≫ ((Functor.const J).obj pt✝).map f
h : IsColimit ((𝟭 C).mapCocone { pt := pt✝, ι := { app := app✝, naturality := naturality✝ } })
s : Cocone { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }
m : { pt := pt✝, ι := { app := app✝, naturality := naturality✝ } }.pt ⟶ s.pt
⊢ (∀ (j : J), { pt := pt✝, ι := { app := app✝, naturality := naturality✝ } }.ι.app j ≫ m = s.ι.app j) →
    m = h.desc { pt := s.pt, ι := { app := fun j ↦ s.ι.app j, naturality := ⋯ } }

Tactic:
w

Goal state after:
case mk
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
J : Type w'
𝒥 : Category.{w, w'} J
obj✝ : J → C
map✝ : {X Y : J} → (X ⟶ Y) → (obj✝ X ⟶ obj✝ Y)
map_id✝ : ∀ (X : J), map✝ (𝟙 X) = 𝟙 (obj✝ X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), map✝ (f ≫ g) = map✝ f ≫ map✝ g
pt✝ : C
app✝ :
  (X : J) →
    { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X ⟶ ((Functor.const J).obj pt✝).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f ≫ app✝ Y =
      app✝ X ≫ ((Functor.const J).obj pt✝).map f
h : IsColimit ((𝟭 C).mapCocone { pt := pt✝, ι := { app := app✝, naturality := naturality✝ } })
s : Cocone { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }
m : { pt := pt✝, ι := { app := app✝, naturality := naturality✝ } }.pt ⟶ s.pt
w : ∀ (j : J), { pt := pt✝, ι := { app := app✝, naturality := naturality✝ } }.ι.app j ≫ m = s.ι.app j
⊢ m = h.desc { pt := s.pt, ι := { app := fun j ↦ s.ι.app j, naturality := ⋯ } }
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
E : Type u₃
ℰ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : PreservesLimit K (F ⋙ G)
inst✝ : ReflectsLimit (K ⋙ F) G
c✝ : Cone K
h : IsLimit c✝
⊢ IsLimit (F.mapCone c✝)

Tactic:
apply isLimitOfReflects G

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
E : Type u₃
ℰ : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : PreservesLimit K (F ⋙ G)
inst✝ : ReflectsLimit (K ⋙ F) G
c✝ : Cone K
h : IsLimit c✝
⊢ IsLimit (G.mapCone (F.mapCone c✝))
Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
⊢ ⊤.map P.ι = P.isoClosure

Tactic:
by
  ext X
  constructor
  · rintro ⟨⟨Y, hY⟩, _, ⟨e⟩⟩
    exact ⟨Y, hY, ⟨e.symm⟩⟩
  · rintro ⟨Y, hY, ⟨e⟩⟩
    exact ⟨⟨Y, hY⟩, by simp, ⟨e.symm⟩⟩

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
P : C
ι ι' : P ⟶ X
w : ι ≫ f = 0
h : ι = ι'
⊢ ι ≫ f = 0

Tactic:
w

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
P : C
ι ι' : P ⟶ X
w : ι ≫ f = 0
h : ι = ι'
⊢ 0 = 0
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
P : C
π π' : Y ⟶ P
w : f ≫ π = 0
h : π = π'
⊢ f ≫ π = 0

Tactic:
w

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
P : C
π π' : Y ⟶ P
w : f ≫ π = 0
h : π = π'
⊢ 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✝
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
K : Type
inst✝¹ : Finite K
inst✝ : HasFiniteBiproducts C
f : K → C
p : K → Prop
W' : C
g' : W' ⟶ ⨁ f
⊢ g' ≫ biproduct.toSubtype f p = 0 → (g' ≫ biproduct.toSubtype f pᶜ) ≫ biproduct.fromSubtype f pᶜ = g'

Tactic:
w

Goal state after:
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
K : Type
inst✝¹ : Finite K
inst✝ : HasFiniteBiproducts C
f : K → C
p : K → Prop
W' : C
g' : W' ⟶ ⨁ f
w : g' ≫ biproduct.toSubtype f p = 0
⊢ (g' ≫ biproduct.toSubtype f pᶜ) ≫ biproduct.fromSubtype f pᶜ = g'
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
K : Type
inst✝¹ : Finite K
inst✝ : HasFiniteBiproducts C
f : K → C
p : K → Prop
W : C
g' : ⨁ f ⟶ W
⊢ biproduct.fromSubtype f p ≫ g' = 0 → biproduct.toSubtype f pᶜ ≫ biproduct.fromSubtype f pᶜ ≫ g' = g'

Tactic:
w

Goal state after:
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
K : Type
inst✝¹ : Finite K
inst✝ : HasFiniteBiproducts C
f : K → C
p : K → Prop
W : C
g' : ⨁ f ⟶ W
w : biproduct.fromSubtype f p ≫ g' = 0
⊢ biproduct.toSubtype f pᶜ ≫ biproduct.fromSubtype f pᶜ ≫ g' = g'
Module: Mathlib.Algebra.Order.Antidiag.Pi

Goal state before:
pp: ι : Type u_1
μ : Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : AddCancelCommMonoid μ
inst✝² : HasAntidiagonal μ
inst✝¹ : DecidableEq μ
i : ι
s : Finset ι
inst✝ : DecidableEq (ι → μ)
hi : i ∉ s
n : μ
⊢ (insert i s).piAntidiag n =
    (antidiagonal n).biUnion fun p ↦ image (fun f j ↦ f j + if j = i then p.1 else 0) (s.piAntidiag p.2)

Tactic:
by
  simpa [map_eq_image, addRightEmbedding] using! piAntidiag_cons hi n

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case mp
n : ℕ
c : Composition n
⊢ c.blocks = [] → n = 0

Tactic:
intro h
    simpa using congr(List.sum $h)

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Composition

Goal state before:
pp: case mpr
c : Composition 0
⊢ c.blocks.length = 0

Tactic:
← nonpos_iff_eq_zero

Goal state after:
case mpr
c : Composition 0
⊢ c.blocks.length ≤ 0
Module: Mathlib.Algebra.Order.Antidiag.Finsupp

Goal state before:
pp: ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
n : μ
f : ι →₀ μ
⊢ (∃ m ∈ antidiagonal n, ∃ g, f = g.update a m.1 ∧ g ∈ s.finsuppAntidiag m.2) ↔
    ∃ a_1 ∈ antidiagonal n, ∃ a_2 ∈ s.finsuppAntidiag a_1.2, a_2.update a a_1.1 = f

Tactic:
and_comm,

Goal state after:
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
a : ι
s : Finset ι
h : a ∉ s
n : μ
f : ι →₀ μ
⊢ (∃ m ∈ antidiagonal n, ∃ g, f = g.update a m.1 ∧ g ∈ s.finsuppAntidiag m.2) ↔
    ∃ a_1 ∈ antidiagonal n, ∃ a_2, a_2.update a a_1.1 = f ∧ a_2 ∈ s.finsuppAntidiag a_1.2
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✝ : Epi (F.biproductComparison' f)
this✝ : Epi (F.splitEpiBiproductComparison f).section_
this : IsIso (F.biproductComparison f)
⊢ PreservesBiproduct f F

Tactic:
apply preservesBiproduct_of_mono_biproductComparison

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

Goal state before:
pp: case left
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid μ
inst✝⁴ : HasAntidiagonal μ
inst✝³ : DecidableEq μ
inst✝² : AddCommMonoid μ'
inst✝¹ : HasAntidiagonal μ'
inst✝ : DecidableEq μ'
e : μ ≃+ μ'
s : Finset ι
n : μ
g : ι →₀ μ
hsum : (g.sum fun x x_1 ↦ x_1) = n
hsupp : g.support ⊆ s
⊢ ((mapRange ⇑e ⋯ g).sum fun x x_1 ↦ x_1) = e n

Tactic:
sum_mapRange_index (fun _ ↦ rfl),

Goal state after:
case left
ι : Type u_1
μ : Type u_2
μ' : Type u_3
inst✝⁶ : DecidableEq ι
inst✝⁵ : AddCommMonoid μ
inst✝⁴ : HasAntidiagonal μ
inst✝³ : DecidableEq μ
inst✝² : AddCommMonoid μ'
inst✝¹ : HasAntidiagonal μ'
inst✝ : DecidableEq μ'
e : μ ≃+ μ'
s : Finset ι
n : μ
g : ι →₀ μ
hsum : (g.sum fun x x_1 ↦ x_1) = n
hsupp : g.support ⊆ s
⊢ (g.sum fun a b ↦ e b) = e n
Module: Mathlib.Logic.Equiv.Fintype

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
e : Perm α
f : α ↪ β
b : β
h : b ∉ Set.range ⇑f
⊢ (e.viaFintypeEmbedding f) b = b

Tactic:
by
  rwa [Equiv.Perm.viaFintypeEmbedding, Equiv.Perm.extendDomain_apply_not_subtype]

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 : x ∈ (s.noncommProd f comm).support
⊢ ∃ a ∈ s, x ∈ (f a).support

Tactic:
by
  contrapose! hx
  classical
  revert hx comm s
  apply Finset.induction
  · simp
  · intro a s ha ih comm hs
    rw [Finset.noncommProd_insert_of_notMem s a f comm ha]
    apply mt (Finset.mem_of_subset (support_mul_le _ _))
    rw [Finset.sup_eq_union, Finset.notMem_union]
    exact ⟨hs a (s.mem_insert_self a), ih (fun a ha ↦ hs a (Finset.mem_insert_of_mem ha))⟩

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
z : α
l : List α
IH : ∀ {x : α} (y : α), x ∈ y :: l → (y :: l).formPerm x ∈ y :: l
x y : α
h : x ∈ y :: z :: l
hx : x ∉ z :: l
⊢ (y :: z :: l).formPerm x ∈ y :: z :: l

Tactic:
replace h : x = y := Or.resolve_right (mem_cons.1 h) hx

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
z : α
l : List α
IH : ∀ {x : α} (y : α), x ∈ y :: l → (y :: l).formPerm x ∈ y :: l
x y : α
hx : x ∉ z :: l
h : x = y
⊢ (y :: z :: l).formPerm x ∈ y :: z :: l