mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.BigOperators.Expect

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝³ : CommSemiring M
inst✝² : Module ℚ≥0 M
inst✝¹ : IsScalarTower ℚ≥0 M M
inst✝ : SMulCommClass ℚ≥0 M M
s : Finset ι
f : ι → M
n : ℕ
⊢ (↑(#s))⁻¹ ^ n • ∑ p ∈ Fintype.piFinset fun _i ↦ s, ∏ i, f (p i) =
    (↑(#s ^ n))⁻¹ • ∑ i ∈ Fintype.piFinset fun x ↦ s, ∏ i_1, f (i i_1)

Tactic:
inv_pow,

Goal state after:
ι : Type u_1
M : Type u_4
inst✝³ : CommSemiring M
inst✝² : Module ℚ≥0 M
inst✝¹ : IsScalarTower ℚ≥0 M M
inst✝ : SMulCommClass ℚ≥0 M M
s : Finset ι
f : ι → M
n : ℕ
⊢ (↑(#s) ^ n)⁻¹ • ∑ p ∈ Fintype.piFinset fun _i ↦ s, ∏ i, f (p i) =
    (↑(#s ^ n))⁻¹ • ∑ i ∈ Fintype.piFinset fun x ↦ s, ∏ i_1, f (i i_1)
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j : ℕ
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
⊢ (F.intervalGapsWithin h a b ↑j).2 ≤ b

Tactic:
wlog hj : j < k + 1 generalizing j
  · grind [cast_val_eq_self]
  by_cases hj : j = k
  · simp [hj]
  · have := hFab (F.intervalGapsWithin_mapsTo h a b (x := j) (by grind))
    grind

Goal state after:
Module: Mathlib.Algebra.BigOperators.ModEq

Goal state before:
pp: α : Type u_1
n : ℕ
l : List α
f g : α → ℕ
h : ∀ x ∈ l, f x ≡ g x [MOD n]
⊢ (List.map f l).sum ≡ (List.map g l).sum [MOD n]

Tactic:
induction l <;> aesop (add unsafe ModEq.add)

Goal state after:
Module: Mathlib.Algebra.BigOperators.ModEq

Goal state before:
pp: α : Type u_1
n : ℤ
l : List α
f g : α → ℤ
h : ∀ x ∈ l, f x ≡ g x [ZMOD n]
⊢ (List.map f l).sum ≡ (List.map g l).sum [ZMOD n]

Tactic:
induction l <;> aesop (add unsafe ModEq.add)

Goal state after:
Module: Mathlib.Algebra.BigOperators.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ : ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range i, g i = ∑ i ∈ Ico m (n - 1), f (i + 1) • ∑ i ∈ range (i + 1), g i
h₂ :
  ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range (i + 1), g i =
    ∑ i ∈ Ico m (n - 1), f i • ∑ i ∈ range (i + 1), g i + f (n - 1) • ∑ i ∈ range n, g i -
      f m • ∑ i ∈ range (m + 1), g i
⊢ f m • g m + ∑ k ∈ Ico (m + 1) n, f k • (∑ i ∈ range (k + 1), g i - ∑ i ∈ range k, g i) =
    f (n - 1) • ∑ i ∈ range n, g i - f m • ∑ i ∈ range m, g i -
      ∑ i ∈ Ico m (n - 1), (f (i + 1) - f i) • ∑ i ∈ range (i + 1), g i

Tactic:
simp_rw [smul_sub, sum_sub_distrib, h₂, h₁]

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
m n : ℕ
hmn : m < n
h₁ : ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range i, g i = ∑ i ∈ Ico m (n - 1), f (i + 1) • ∑ i ∈ range (i + 1), g i
h₂ :
  ∑ i ∈ Ico (m + 1) n, f i • ∑ i ∈ range (i + 1), g i =
    ∑ i ∈ Ico m (n - 1), f i • ∑ i ∈ range (i + 1), g i + f (n - 1) • ∑ i ∈ range n, g i -
      f m • ∑ i ∈ range (m + 1), g i
⊢ f m • g m +
      (∑ x ∈ Ico m (n - 1), f x • ∑ i ∈ range (x + 1), g i + f (n - 1) • ∑ i ∈ range n, g i -
          f m • ∑ i ∈ range (m + 1), g i -
        ∑ i ∈ Ico m (n - 1), f (i + 1) • ∑ i ∈ range (i + 1), g i) =
    f (n - 1) • ∑ i ∈ range n, g i - f m • ∑ i ∈ range m, g i -
      ∑ i ∈ Ico m (n - 1), (f (i + 1) - f i) • ∑ i ∈ range (i + 1), g i
Module: Mathlib.Algebra.BigOperators.Ring.Nat

Goal state before:
pp: case refine_1
ι : Type u_1
M : Type u_2
f : ι → M
s : Finset M
hb : ∀ b ∈ s, {a | f a = b}.Finite
t : Finset M := ⋯.toFinset
ht : (f ⁻¹' ↑t).Finite
⊢ image f ht.toFinset = t

pp: case refine_2
ι : Type u_1
M : Type u_2
f : ι → M
s : Finset M
hb : ∀ b ∈ s, {a | f a = b}.Finite
t : Finset M := ⋯.toFinset
ht : (f ⁻¹' ↑t).Finite
m : M
hm : m ∈ t
⊢ #({a ∈ ht.toFinset | f a = m}) = Nat.card ↑{a | f a = m}

Tactic:
· simpa [← Finset.coe_inj, t] using Set.image_preimage_eq_inter_range

Goal state after:
case refine_2
ι : Type u_1
M : Type u_2
f : ι → M
s : Finset M
hb : ∀ b ∈ s, {a | f a = b}.Finite
t : Finset M := ⋯.toFinset
ht : (f ⁻¹' ↑t).Finite
m : M
hm : m ∈ t
⊢ #({a ∈ ht.toFinset | f a = m}) = Nat.card ↑{a | f a = m}
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
a b a' b' : α
h : Rel α (a, b) (a', b')
hx : a' = b'
⊢ Eq.ndrec (motive := fun x ↦ x.IsDiag → α) (fun x ↦ a) ⋯ hx = a'

Tactic:
cases hx

Goal state after:
case refl
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
a b a' : α
h : Rel α (a, b) (a', a')
⊢ Eq.ndrec (motive := fun x ↦ x.IsDiag → α) (fun x ↦ a) ⋯ ⋯ = a'
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
z✝ : Sym2 α
f✝ : α → β
r r₁ r₂ : α → α → Prop
sym : Std.Symm r
f : α → β
hf : r ≤ ⇑(Setoid.ker f)
z : ↑(fromRel sym)
⊢ (fun z ↦ ⟨map Subtype.val ↑z.snd, ⋯⟩)
      ((fun z ↦ fromRelNdrec ↑z ⋯ (fun a₁ a₂ h ↦ ⟨f a₁, ⟨s(⟨a₁, ⋯⟩, ⟨a₂, ⋯⟩), h⟩⟩) ⋯) z) =
    z

Tactic:
by
    rcases z with ⟨⟨a₁, a₂⟩, h⟩
    rfl

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Prefunctor

Goal state before:
pp: V W : Type u
inst✝¹ : Quiver V
inst✝ : Quiver W
F G : Prefunctor V W
h_obj : ∀ (X : V), F.obj X = G.obj X
h_map : ∀ (X Y : V) (f : X ⟶ Y), F.map f = Quiver.homOfEq (G.map f) ⋯ ⋯
⊢ F = G

Tactic:
obtain ⟨Fobj, Fmap⟩ := F

Goal state after:
V W : Type u
inst✝¹ : Quiver V
inst✝ : Quiver W
G : Prefunctor V W
Fobj : V → W
Fmap : {X Y : V} → (X ⟶ Y) → (Fobj X ⟶ Fobj Y)
h_obj : ∀ (X : V), { obj := Fobj, map := Fmap }.obj X = G.obj X
h_map : ∀ (X Y : V) (f : X ⟶ Y), { obj := Fobj, map := Fmap }.map f = Quiver.homOfEq (G.map f) ⋯ ⋯
⊢ { obj := Fobj, map := Fmap } = G
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
S : Type v₃
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Algebra R S
R' : Type u_6
S' : Type u_7
inst✝⁸ : CommSemiring R'
inst✝⁷ : CommSemiring S'
inst✝⁶ : Algebra R R'
inst✝⁵ : Algebra S S'
inst✝⁴ : Algebra R' S'
inst✝³ : Algebra R S'
inst✝² : IsScalarTower R R' S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsPushout R S R' S'
a : S
⊢ (algebraMap S S') a = (algebraMap S S') a * 1

Tactic:
mul_one

Goal state after:
R : Type u_1
S : Type v₃
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Algebra R S
R' : Type u_6
S' : Type u_7
inst✝⁸ : CommSemiring R'
inst✝⁷ : CommSemiring S'
inst✝⁶ : Algebra R R'
inst✝⁵ : Algebra S S'
inst✝⁴ : Algebra R' S'
inst✝³ : Algebra R S'
inst✝² : IsScalarTower R R' S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsPushout R S R' S'
a : S
⊢ (algebraMap S S') a = (algebraMap S S') a
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case add
R : Type u_1
M✝ : Type v₁
N : Type v₂
S : Type v₃
inst✝⁴⁶ : AddCommMonoid M✝
inst✝⁴⁵ : AddCommMonoid N
inst✝⁴⁴ : CommSemiring R
inst✝⁴³ : CommSemiring S
inst✝⁴² : Algebra R S
inst✝⁴¹ : Module R M✝
inst✝⁴⁰ : Module R N
inst✝³⁹ : Module S N
inst✝³⁸ : IsScalarTower R S N
f : M✝ →ₗ[R] N
h : IsBaseChange S f
P : Type u_2
Q : Type u_3
inst✝³⁷ : AddCommMonoid P
inst✝³⁶ : Module R P
inst✝³⁵ : AddCommMonoid Q
inst✝³⁴ : Module S Q
inst✝³³ : Module R Q
inst✝³² : IsScalarTower R S Q
f' : P →ₗ[R] Q
T : Type u_4
O : Type u_5
inst✝³¹ : CommSemiring T
inst✝³⁰ : Algebra R T
inst✝²⁹ : Algebra S T
inst✝²⁸ : IsScalarTower R S T
inst✝²⁷ : AddCommMonoid O
inst✝²⁶ : Module R O
inst✝²⁵ : Module S O
inst✝²⁴ : Module T O
inst✝²³ : IsScalarTower S T O
inst✝²² : IsScalarTower R S O
inst✝²¹ : IsScalarTower R T O
R' : Type u_6
S' : Type u_7
inst✝²⁰ : CommSemiring R'
inst✝¹⁹ : CommSemiring S'
inst✝¹⁸ : Algebra R R'
inst✝¹⁷ : Algebra S S'
inst✝¹⁶ : Algebra R' S'
inst✝¹⁵ : Algebra R S'
inst✝¹⁴ : IsScalarTower R R' S'
inst✝¹³ : IsScalarTower R S S'
A : Type u_8
B : Type u_9
inst✝¹² : CommRing A
inst✝¹¹ : CommRing B
inst✝¹⁰ : Algebra R A
inst✝⁹ : Algebra R B
inst✝⁸ : Algebra A B
inst✝⁷ : Algebra S B
inst✝⁶ : IsScalarTower R A B
inst✝⁵ : IsScalarTower R S B
inst✝⁴ : IsPushout R S A B
M : Type u_10
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
s : S
x y : S ⊗[R] M
hx : ↑(cancelBaseChangeAux R S A B M).symm (s • x) = s • ↑(cancelBaseChangeAux R S A B M).symm x
hy : ↑(cancelBaseChangeAux R S A B M).symm (s • y) = s • ↑(cancelBaseChangeAux R S A B M).symm y
⊢ ↑(cancelBaseChangeAux R S A B M).symm (s • (x + y)) = s • ↑(cancelBaseChangeAux R S A B M).symm (x + y)

Tactic:
simp only [smul_add, map_add, hx, hy]

Goal state after:
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
α : X ≅ Y
β : Y ≅ X
⊢ α.symm.inv = β.inv ↔ β.hom = α.inv

Tactic:
inv_eq_inv α.symm β,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
α : X ≅ Y
β : Y ≅ X
⊢ α.symm.hom = β.hom ↔ β.hom = α.inv
Module: Mathlib.CategoryTheory.Equivalence

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
e : C ≌ D
G : D ⥤ C
iso : e.inverse ≅ G
X : C
⊢ e.functor.map (e.unitIso.hom.app X ≫ iso.hom.app (e.functor.obj X)) ≫
      e.functor.map (iso.inv.app (e.functor.obj X)) ≫ e.counitIso.hom.app (e.functor.obj X) =
    𝟙 (e.functor.obj X)

Tactic:
rw [← map_comp_assoc, assoc, iso.hom_inv_id_app, comp_id, functor_unit_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Groupoid

Goal state before:
pp: case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
⊢ IsGroupoid C → isomorphisms C = ⊤

Tactic:
rw [eq_top_iff]
    intro _ _
    simp only [isomorphisms.iff, top_apply]
    infer_instance

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

Goal state before:
pp: T : Type u
inst✝¹ : Category.{v, u} T
f g : Arrow T
sq : f ⟶ g
inst✝ : Mono sq
Z : T
φ ψ : Z ⟶ f.left
h : φ ≫ Hom.left sq = ψ ≫ Hom.left sq
⊢ φ = ψ

Tactic:
let aux : (Z ⟶ f.left) → (Arrow.mk (𝟙 Z) ⟶ f) := fun φ =>
      { left := φ
        right := φ ≫ f.hom }
    have : ∀ g, (aux g).right = g ≫ f.hom := fun g => rfl
    change (aux φ).left = (aux ψ).left
    congr 1
    rw [← cancel_mono sq]
    ext
    · exact h
    · simp [this, ← Arrow.w_mk_right, reassoc_of% h]

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

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : Q.RespectsIso
⊢ P ≤ Q → P.isoClosure ≤ Q

Tactic:
intro h
    exact (monotone_isoClosure h).trans (by rw [Q.isoClosure_eq_self])

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

Goal state before:
pp: case hprecomp
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
⊢ MorphismProperty.monomorphisms C f → MorphismProperty.monomorphisms C (e.hom ≫ f)

Tactic:
simp only [monomorphisms.iff]

Goal state after:
case hprecomp
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
⊢ Mono f → Mono (e.hom ≫ f)
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: case hpostcomp
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
⊢ MorphismProperty.monomorphisms C f → MorphismProperty.monomorphisms C (f ≫ e.hom)

Tactic:
simp only [monomorphisms.iff]

Goal state after:
case hpostcomp
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
⊢ Mono f → Mono (f ≫ e.hom)
Module: Mathlib.CategoryTheory.HomCongr

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
f : X ⟶ Y
⊢ α.hom ≫ α.inv ≫ f ≫ 𝟙 Y = f

Tactic:
α.hom_inv_id_assoc,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y X₁ Y₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
f : X ⟶ Y
⊢ f ≫ 𝟙 Y = f
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
t : Cone F
lift : (s : Cone F) → s ⟶ t
uniq : ∀ (s : Cone F) (m : s ⟶ t), m = lift s
s : Cone F
m : s.pt ⟶ t.pt
w : ∀ (j : J), m ≫ t.π.app j = s.π.app j
⊢ { hom := m, w := w } = lift s

Tactic:
by apply uniq

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
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquiv F G
X : C
Y : D
f : F.obj X ⟶ Y
⊢ (adj.homEquiv X Y) f = { app := fun X ↦ (adj.homEquiv X (F.obj X)) (𝟙 (F.obj X)), naturality := ⋯ }.app X ≫ G.map f

Tactic:
by simp [← adj.homEquiv_naturality_right]

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
t : Cocone F
X : C
h : F.cocones.CorepresentableBy X
s : Cocone F
m : (colimitCocone h).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone h).ι.app j ≫ m = s.ι.app j
⊢ m = homOfCocone h s

Tactic:
by
    rw [← homOfCocone_coconeOfHom h m]
    congr
    rw [coconeOfHom_fac]
    dsimp [Cocone.extend]; cases s; congr with j; exact w j

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
⊢ ∀ {X_1 Y : C ⥤ Type (max w v₁)} (f : X_1 ⟶ Y),
    ((uliftCoyoneda.{w, v₁, u₁}.rightOp ⋙ coyoneda).obj X).map f ≫
        (uliftCoyonedaEquiv.trans Equiv.ulift.symm).toIso.hom =
      (uliftCoyonedaEquiv.trans Equiv.ulift.symm).toIso.hom ≫
        ((evaluation C (Type (max v₁ w)) ⋙
                  (whiskeringRight (C ⥤ Type (max v₁ w)) (Type (max v₁ w)) (Type (max (max w u₁) v₁))).obj
                    uliftFunctor.{u₁, max v₁ w}).obj
              X).map
          f

Tactic:
by
        intros Y Z f
        ext g
        rw [← ULift.down_inj]
        simpa using uliftCoyonedaEquiv_comp _ _

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

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
inst✝² : HasColimit F
E : K ⥤ J
inst✝¹ : HasColimit (E ⋙ F)
L : Type u₃
inst✝ : Category.{v₃, u₃} L
D : L ⥤ K
h : HasColimit (D ⋙ E ⋙ F)
j : L
⊢ ι (E ⋙ F) (D.obj j) ≫ pre F E = ι (D ⋙ E ⋙ F) j ≫ pre F (D ⋙ E)

Tactic:
colimit.ι_pre

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
inst✝² : HasColimit F
E : K ⥤ J
inst✝¹ : HasColimit (E ⋙ F)
L : Type u₃
inst✝ : Category.{v₃, u₃} L
D : L ⥤ K
h : HasColimit (D ⋙ E ⋙ F)
j : L
⊢ ι F (E.obj (D.obj j)) = ι (D ⋙ E ⋙ F) j ≫ pre F (D ⋙ E)
Module: Mathlib.CategoryTheory.Limits.HasLimits

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
inst✝¹ : HasColimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
inst✝ : HasColimitsOfShape K C
E : K ⥤ J
j✝ : K
⊢ α.app (E.obj j✝) ≫ ι G (E.obj j✝) = (E.whiskerLeft α).app j✝ ≫ ι (E ⋙ G) j✝ ≫ pre G E

Tactic:
colimit.ι_pre

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
inst✝¹ : HasColimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
inst✝ : HasColimitsOfShape K C
E : K ⥤ J
j✝ : K
⊢ α.app (E.obj j✝) ≫ ι G (E.obj j✝) = (E.whiskerLeft α).app j✝ ≫ ι G (E.obj j✝)
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
inst✝² : HasColimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasColimitsOfShape J D
H : C ⥤ D
j✝ : J
⊢ ι (F ⋙ H) j✝ ≫ post F H ≫ H.map (colim.map α) = ι (F ⋙ H) j✝ ≫ colim.map (whiskerRight α H) ≫ post G H

Tactic:
rw [← assoc, colimit.ι_post, ← H.map_comp, colimit.ι_map, H.map_comp]

Goal state after:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
inst✝² : HasColimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasColimitsOfShape J D
H : C ⥤ D
j✝ : J
⊢ H.map (α.app j✝) ≫ H.map (ι G j✝) = ι (F ⋙ H) j✝ ≫ colim.map (whiskerRight α H) ≫ post G H
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
X✝ Y✝ Z✝ : WidePushoutShape J
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ Hom.casesOn (motive := fun a a_1 x ↦
      X✝ = a → Z✝ = a_1 → f ≫ g ≍ x → (Option.casesOn X✝ B objs ⟶ Option.casesOn Z✝ B objs)) (f ≫ g)
      (fun X h ↦
        Eq.ndrec (motive := fun X ↦ Z✝ = X → f ≫ g ≍ Hom.id X → (Option.casesOn X✝ B objs ⟶ Option.casesOn Z✝ B objs))
          (fun h ↦
            Eq.ndrec (motive := fun {Y} ↦
              (f : X✝ ⟶ Y) → f ≍ Hom.id X✝ → (Option.casesOn X✝ B objs ⟶ Option.casesOn Y B objs))
              (fun f h ↦ 𝟙 (Option.casesOn X✝ B objs)) ⋯ (f ≫ g))
          h)
      (fun j h ↦
        Eq.ndrec (motive := fun {X} ↦
          (f : X ⟶ Z✝) → Z✝ = some j → f ≍ Hom.init j → (Option.casesOn X B objs ⟶ Option.casesOn Z✝ B objs))
          (fun f h ↦
            Eq.ndrec (motive := fun {Y} ↦
              (f : none ⟶ Y) → f ≍ Hom.init j → (Option.casesOn none B objs ⟶ Option.casesOn Y B objs))
              (fun f h ↦ arrows j) ⋯ f)
          ⋯ (f ≫ g))
      ⋯ ⋯ ⋯ =
    Hom.casesOn (motive := fun a a_1 x ↦
        X✝ = a → Y✝ = a_1 → f ≍ x → (Option.casesOn X✝ B objs ⟶ Option.casesOn Y✝ B objs)) f
        (fun X h ↦
          Eq.ndrec (motive := fun X ↦ Y✝ = X → f ≍ Hom.id X → (Option.casesOn X✝ B objs ⟶ Option.casesOn Y✝ B objs))
            (fun h ↦
              Eq.ndrec (motive := fun {Y} ↦
                (f : X✝ ⟶ Y) → f ≍ Hom.id X✝ → (Option.casesOn X✝ B objs ⟶ Option.casesOn Y B objs))
                (fun f h ↦ 𝟙 (Option.casesOn X✝ B objs)) ⋯ f)
            h)
        (fun j h ↦
          Eq.ndrec (motive := fun {X} ↦
            (f : X ⟶ Y✝) → Y✝ = some j → f ≍ Hom.init j → (Option.casesOn X B objs ⟶ Option.casesOn Y✝ B objs))
            (fun f h ↦
              Eq.ndrec (motive := fun {Y} ↦
                (f : none ⟶ Y) → f ≍ Hom.init j → (Option.casesOn none B objs ⟶ Option.casesOn Y B objs))
                (fun f h ↦ arrows j) ⋯ f)
            ⋯ f)
        ⋯ ⋯ ⋯ ≫
      Hom.casesOn (motive := fun a a_1 x ↦
        Y✝ = a → Z✝ = a_1 → g ≍ x → (Option.casesOn Y✝ B objs ⟶ Option.casesOn Z✝ B objs)) g
        (fun X h ↦
          Eq.ndrec (motive := fun X ↦ Z✝ = X → g ≍ Hom.id X → (Option.casesOn Y✝ B objs ⟶ Option.casesOn Z✝ B objs))
            (fun h ↦
              Eq.ndrec (motive := fun {Y} ↦
                (f : Y✝ ⟶ Y) → f ≍ Hom.id Y✝ → (Option.casesOn Y✝ B objs ⟶ Option.casesOn Y B objs))
                (fun f h ↦ 𝟙 (Option.casesOn Y✝ B objs)) ⋯ g)
            h)
        (fun j h ↦
          Eq.ndrec (motive := fun {X} ↦
            (f : X ⟶ Z✝) → Z✝ = some j → f ≍ Hom.init j → (Option.casesOn X B objs ⟶ Option.casesOn Z✝ B objs))
            (fun f h ↦
              Eq.ndrec (motive := fun {Y} ↦
                (f : none ⟶ Y) → f ≍ Hom.init j → (Option.casesOn none B objs ⟶ Option.casesOn Y B objs))
                (fun f h ↦ arrows j) ⋯ f)
            ⋯ g)
        ⋯ ⋯ ⋯

Tactic:
cases f
    · simp only [hom_id, Category.id_comp]; congr
    · cases g
      simp only [hom_id, Category.comp_id]; congr

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
P : C
⊢ desc (initial.to P) (𝟙 P) ≫ inr = 𝟙 ((⊥_ C) ⨿ P)

Tactic:
by apply coprod.hom_ext <;> simp [eq_iff_true_of_subsingleton]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasInitial C
P : C
⊢ desc (𝟙 P) (initial.to P) ≫ inl = 𝟙 (P ⨿ ⊥_ C)

Tactic:
by apply coprod.hom_ext <;> simp [eq_iff_true_of_subsingleton]

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 : 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)
⊢ G.map (pullback.fst f g) ≫ G.map f = G.map (pullback.snd f g) ≫ G.map g

Tactic:
by simp only [← G.map_comp, pullback.condition]

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasInitial C
inst✝ : HasInitial D
i : IsIso (initialComparison G)
⊢ IsColimit (G.mapCocone (asEmptyCocone (⊥_ C)))

Tactic:
apply (isColimitMapCoconeEmptyCoconeEquiv _ _).symm _

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasInitial C
inst✝ : HasInitial D
i : IsIso (initialComparison G)
⊢ IsInitial (G.obj (⊥_ C))
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✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : F.PreservesZeroMorphisms
X : C
hX : 𝟙 X = 0
⊢ F.map 0 = 0

Tactic:
F.map_zero

Goal state after:
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
X : C
hX : 𝟙 X = 0
⊢ 0 = 0
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero

Goal state before:
pp: case calc_2
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
inst✝¹ : HasZeroMorphisms E
G : C ⥤ D
inst✝ : G.IsRightAdjoint
X Y : C
adj : G.leftAdjoint ⊣ G := Adjunction.ofIsRightAdjoint G
⊢ adj.unit.app (G.obj X) ≫ G.map (adj.counit.app X) ≫ G.map 0 =
    adj.unit.app (G.obj X) ≫ G.map (G.leftAdjoint.map 0) ≫ G.map 0

pp: case calc_3
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
inst✝¹ : HasZeroMorphisms E
G : C ⥤ D
inst✝ : G.IsRightAdjoint
X Y : C
adj : G.leftAdjoint ⊣ G := Adjunction.ofIsRightAdjoint G
⊢ adj.unit.app (G.obj X) ≫ G.map (G.leftAdjoint.map 0) ≫ G.map 0 = 0

Tactic:
· simp only [← G.map_comp, comp_zero]

Goal state after:
case calc_3
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
inst✝¹ : HasZeroMorphisms E
G : C ⥤ D
inst✝ : G.IsRightAdjoint
X Y : C
adj : G.leftAdjoint ⊣ G := Adjunction.ofIsRightAdjoint G
⊢ adj.unit.app (G.obj X) ≫ G.map (G.leftAdjoint.map 0) ≫ G.map 0 = 0
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:
dsimp [exactFunctor]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
⊢ (leftExactFunctor C D ⊓ rightExactFunctor C D).IsClosedUnderIsomorphisms
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 0 = 0

Tactic:
F.map_zero

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'
⊢ 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
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
A : Bicone F
i j : J
⊢ G.map (A.ι i ≫ A.π j) = if h : i = j then eqToHom ⋯ else 0

Tactic:
A.ι_π

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
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
A : Bicone F
i j : J
⊢ G.map (if h : i = j then eqToHom ⋯ else 0) = if h : i = j then eqToHom ⋯ else 0