mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.EvenFunction

Goal state before:
pp: α : Type u_1
inst✝² : Neg α
R : Type u_3
inst✝¹ : Mul R
f g : α → R
inst✝ : HasDistribNeg R
hf : Function.Odd f
hg : Function.Odd g
a : α
⊢ (f * g) (-a) = (f * g) a

Tactic:
simp only [Pi.mul_apply, hf a, hg a, mul_neg, neg_mul, neg_neg]

Goal state after:
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: a b : ℤ
⊢ max a b + 1 - min a b = ↑(b - a).natAbs + ↑1

Tactic:
Int.natCast_natAbs,

Goal state after:
a b : ℤ
⊢ max a b + 1 - min a b = |b - a| + ↑1
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M
f : M₁ →ₗ[R] M₂ →ₗ[R] M
h : IsTensorProduct f
motive : M → Prop
m : M
zero : motive 0
tmul : ∀ (x : M₁) (y : M₂), motive ((f x) y)
add : ∀ (x y : M), motive x → motive y → motive (x + y)
⊢ motive m

Tactic:
by
  rw [← h.equiv.right_inv m]
  generalize h.equiv.invFun m = y
  change motive (TensorProduct.lift f y)
  induction y with
  | zero => rwa [map_zero]
  | tmul _ _ =>
    rw [TensorProduct.lift.tmul]
    apply tmul
  | add _ _ _ _ =>
    rw [map_add]
    apply add <;> assumption

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

Goal state before:
pp: α : Type u_1
n : ℕ
f : α → ℕ
s : Finset α
h : ∀ x ∈ s, f x ≡ 1 [MOD n]
⊢ ∏ x ∈ s, f x ≡ 1 [MOD n]

Tactic:
simpa using ModEq.prod h

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

Goal state before:
pp: α : Type u_1
n : ℕ
f : α → ℕ
inst✝ : DecidableEq α
s : Finset α
a : α
hf : ∀ x ∈ s, x ≠ a → f x ≡ 1 [MOD n]
⊢ ∏ x ∈ s, f x ≡ if a ∈ s then f a else 1 [MOD n]

Tactic:
simp only [← ZMod.natCast_eq_natCast_iff, cast_one, cast_prod, apply_ite Nat.cast] at *

Goal state after:
α : Type u_1
n : ℕ
f : α → ℕ
inst✝ : DecidableEq α
s : Finset α
a : α
hf : ∀ x ∈ s, x ≠ a → ↑(f x) = 1
⊢ ∏ i ∈ s, ↑(f i) = if a ∈ s then ↑(f a) else 1
Module: Mathlib.Algebra.BigOperators.ModEq

Goal state before:
pp: α : Type u_1
n : ℤ
f : α → ℤ
s : Finset α
h : ∀ x ∈ s, f x ≡ 1 [ZMOD n]
⊢ ∏ x ∈ s, f x ≡ 1 [ZMOD n]

Tactic:
simpa using ModEq.prod h

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: 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
g : M →ₗ[R] Q
r : S
x : N
⊢ (IsTensorProduct.lift h (↑R ((Algebra.linearMap S (Module.End S (M →ₗ[R] Q))).flip g))).toFun (r • x) =
    (RingHom.id S) r • (IsTensorProduct.lift h (↑R ((Algebra.linearMap S (Module.End S (M →ₗ[R] Q))).flip g))).toFun x

Tactic:
let F := ((Algebra.linearMap S <| Module.End S (M →ₗ[R] Q)).flip g).restrictScalars R

Goal state after:
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
g : M →ₗ[R] Q
r : S
x : N
F : S →ₗ[R] M →ₗ[R] Q := ↑R ((Algebra.linearMap S (Module.End S (M →ₗ[R] Q))).flip g)
⊢ (IsTensorProduct.lift h (↑R ((Algebra.linearMap S (Module.End S (M →ₗ[R] Q))).flip g))).toFun (r • x) =
    (RingHom.id S) r • (IsTensorProduct.lift h (↑R ((Algebra.linearMap S (Module.End S (M →ₗ[R] Q))).flip g))).toFun x
Module: Mathlib.Data.List.Sym

Goal state before:
pp: case cons
α : Type u_1
a b x : α
xs : List α
ih : s(a, b) ∈ xs.sym2 → a ∈ xs
h : s(a, b) ∈ (x :: xs).sym2
⊢ a = x ∨ a ∈ xs

Tactic:
mem_sym2_cons_iff

Goal state after:
case cons
α : Type u_1
a b x : α
xs : List α
ih : s(a, b) ∈ xs.sym2 → a ∈ xs
h : s(a, b) = s(x, x) ∨ (∃ y ∈ xs, s(a, b) = s(x, y)) ∨ s(a, b) ∈ xs.sym2
⊢ a = x ∨ a ∈ xs
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
xs : List α
a b : α
h : s(b, a) ∈ xs.sym2
⊢ b ∈ xs

Tactic:
exact left_mem_of_mk_mem_sym2 h

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

Goal state before:
pp: case cons
α : Type u_1
a b x : α
xs : List α
ih : a ∈ xs → b ∈ xs → s(a, b) ∈ xs.sym2
ha : a ∈ x :: xs
hb : b ∈ x :: xs
⊢ s(a, b) ∈ (x :: xs).sym2

Tactic:
mem_sym2_cons_iff

Goal state after:
case cons
α : Type u_1
a b x : α
xs : List α
ih : a ∈ xs → b ∈ xs → s(a, b) ∈ xs.sym2
ha : a ∈ x :: xs
hb : b ∈ x :: xs
⊢ s(a, b) = s(x, x) ∨ (∃ y ∈ xs, s(a, b) = s(x, y)) ∨ s(a, b) ∈ xs.sym2
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Finset α
⊢ (Multiset.map f s.val).sym2.dedup = (Multiset.map (Sym2.map f) s.val.sym2).dedup

Tactic:
Multiset.sym2_map

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Finset α
⊢ (Multiset.map (Sym2.map f) s.val.sym2).dedup = (Multiset.map (Sym2.map f) s.val.sym2).dedup
Module: Mathlib.Data.List.Sym

Goal state before:
pp: case cons.inr
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : xs.sym2.dedup = xs.dedup.sym2
hm : x ∉ xs
⊢ (map (fun y ↦ s(x, y)) xs).Disjoint xs.sym2

pp: case cons.inr
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : xs.sym2.dedup = xs.dedup.sym2
hm : x ∉ xs
⊢ s(x, x) ∉ map (fun y ↦ s(x, y)) xs ++ xs.sym2

Tactic:
· exact map_mk_disjoint_sym2 x xs hm

Goal state after:
case cons.inr
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
ih : xs.sym2.dedup = xs.dedup.sym2
hm : x ∉ xs
⊢ s(x, x) ∉ map (fun y ↦ s(x, y)) xs ++ xs.sym2
Module: Mathlib.Data.Sym.Sym2.Order

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s t : Sym2 α
⊢ s.inf = t.inf ∧ s.sup = t.sup ↔ s = t

Tactic:
induction s with | _ a b
  induction t with | _ c d
  obtain hab | hba := le_total a b <;> obtain hcd | hdc := le_total c d <;>
    aesop (add unsafe le_antisymm)

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: 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 :
  ∀ (Q : Type (max v₁ v₂ v₃)) [inst : AddCommMonoid Q] [inst_1 : Module R Q] [inst_2 : Module S Q]
    [inst_3 : IsScalarTower R S Q] (g : M →ₗ[R] Q), ∃! g', ↑R g' ∘ₗ f = g
g : N →ₗ[S] ULift.{v₂, max v₁ v₃} (S ⊗[R] M)
f' : S ⊗[R] M →ₗ[R] N := TensorProduct.lift (↑R ((Algebra.ofId S (Module.End S (M →ₗ[R] N))).toLinearMap.flip f))
f'' : S ⊗[R] M →ₗ[S] N := { toAddHom := f'.toAddHom, map_smul' := ⋯ }
hg : ∀ (x : M), (↑R g ∘ₗ f) x = (↑ULift.moduleEquiv.symm ∘ₗ (mk R S M) 1) x
⊢ Function.Bijective ⇑f'

Tactic:
LinearMap.comp_apply,

Goal state after:
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 :
  ∀ (Q : Type (max v₁ v₂ v₃)) [inst : AddCommMonoid Q] [inst_1 : Module R Q] [inst_2 : Module S Q]
    [inst_3 : IsScalarTower R S Q] (g : M →ₗ[R] Q), ∃! g', ↑R g' ∘ₗ f = g
g : N →ₗ[S] ULift.{v₂, max v₁ v₃} (S ⊗[R] M)
f' : S ⊗[R] M →ₗ[R] N := TensorProduct.lift (↑R ((Algebra.ofId S (Module.End S (M →ₗ[R] N))).toLinearMap.flip f))
f'' : S ⊗[R] M →ₗ[S] N := { toAddHom := f'.toAddHom, map_smul' := ⋯ }
hg : ∀ (x : M), (↑R g) (f x) = ↑ULift.moduleEquiv.symm (((mk R S M) 1) x)
⊢ Function.Bijective ⇑f'
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x y : α
⊢ s(x, y).toFinset = {x, y}

Tactic:
ext; simp [← Sym2.mem_toFinset, ← Sym2.mem_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x : Sym' α 2
⊢ Quot.map (fun x ↦ ⟨[x.1, x.2], ⋯⟩) ⋯ (Quot.map fromVector ⋯ x) = x

Tactic:
refine x.recOnSubsingleton fun x => ?_

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
x✝ : Sym' α 2
x : List.Vector α 2
⊢ Quot.map (fun x ↦ ⟨[x.1, x.2], ⋯⟩) ⋯ (Quot.map fromVector ⋯ ⟦x⟧) = ⟦x⟧
Module: Mathlib.CategoryTheory.Functor.FullyFaithful

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
hF : ∀ (X Y : C), Function.Bijective F.map
⊢ Nonempty F.FullyFaithful

Tactic:
have : F.Faithful := ⟨fun h ↦ (hF _ _).injective h⟩

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
hF : ∀ (X Y : C), Function.Bijective F.map
this : F.Faithful
⊢ Nonempty F.FullyFaithful
Module: Mathlib.Combinatorics.Quiver.Push

Goal state before:
pp: V : Type u_1
inst✝¹ : Quiver V
W : Type u_2
σ : V → W
W' : Type u_3
inst✝ : Quiver W'
φ : V ⥤q W'
τ : W → W'
h : ∀ (x : V), φ.obj x = τ (σ x)
X Y : V
f : X ⟶ Y
⊢ φ.obj X ⟶ φ.obj Y

Tactic:
exact φ.map f

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

Goal state before:
pp: V : Type u_2
inst✝¹ : Quiver V
V' : Type u_4
inst✝ : Quiver V'
h : HasInvolutiveReverse V'
φ : V ⥤q V'
X Y : Symmetrify V
f : X ⟶ Y
⊢ (match Sum.swap f with
    | Sum.inl g => φ.map g
    | Sum.inr g => reverse (φ.map g)) =
    reverse
      (match f with
      | Sum.inl g => φ.map g
      | Sum.inr g => reverse (φ.map g))

Tactic:
cases f

Goal state after:
case inl
V : Type u_2
inst✝¹ : Quiver V
V' : Type u_4
inst✝ : Quiver V'
h : HasInvolutiveReverse V'
φ : V ⥤q V'
X Y : Symmetrify V
val✝ : X ⟶ Y
⊢ (match (Sum.inl val✝).swap with
    | Sum.inl g => φ.map g
    | Sum.inr g => reverse (φ.map g)) =
    reverse
      (match Sum.inl val✝ with
      | Sum.inl g => φ.map g
      | Sum.inr g => reverse (φ.map g))

case inr
V : Type u_2
inst✝¹ : Quiver V
V' : Type u_4
inst✝ : Quiver V'
h : HasInvolutiveReverse V'
φ : V ⥤q V'
X Y : Symmetrify V
val✝ : Y ⟶ X
⊢ (match (Sum.inr val✝).swap with
    | Sum.inl g => φ.map g
    | Sum.inr g => reverse (φ.map g)) =
    reverse
      (match Sum.inr val✝ with
      | Sum.inl g => φ.map g
      | Sum.inr g => reverse (φ.map g))
Module: Mathlib.Combinatorics.Quiver.Symmetric

Goal state before:
pp: case h_map
V : Type u_2
inst✝² : Quiver V
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
Φ : Symmetrify V ⥤q V'
hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y), Φ.map (reverse f) = reverse (Φ.map f)
X Y : Symmetrify V
f : X ⟶ Y
⊢ Φ.map f = Eq.recOn ⋯ (Eq.recOn ⋯ ((lift (of ⋙q Φ)).map f))

Tactic:
cases f

Goal state after:
case h_map.inl
V : Type u_2
inst✝² : Quiver V
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
Φ : Symmetrify V ⥤q V'
hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y), Φ.map (reverse f) = reverse (Φ.map f)
X Y : Symmetrify V
val✝ : X ⟶ Y
⊢ Φ.map (Sum.inl val✝) = Eq.recOn ⋯ (Eq.recOn ⋯ ((lift (of ⋙q Φ)).map (Sum.inl val✝)))

case h_map.inr
V : Type u_2
inst✝² : Quiver V
V' : Type u_4
inst✝¹ : Quiver V'
inst✝ : HasReverse V'
Φ : Symmetrify V ⥤q V'
hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y), Φ.map (reverse f) = reverse (Φ.map f)
X Y : Symmetrify V
val✝ : Y ⟶ X
⊢ Φ.map (Sum.inr val✝) = Eq.recOn ⋯ (Eq.recOn ⋯ ((lift (of ⋙q Φ)).map (Sum.inr val✝)))
Module: Mathlib.CategoryTheory.Equivalence

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
η : 𝟭 C ≅ F ⋙ G
ε : G ⋙ F ≅ 𝟭 D
X : C
⊢ F.map ((adjointifyη η ε).hom.app X) ≫ ε.hom.app (F.obj X) = 𝟙 (F.obj X)

Tactic:
by
  dsimp [adjointifyη, Trans.trans]
  simp only [comp_id, assoc, map_comp]
  have := ε.hom.naturality (F.map (η.inv.app X)); dsimp at this; rw [this]; clear this
  rw [← assoc _ _ (F.map _)]
  have := ε.hom.naturality (ε.inv.app <| F.obj X); dsimp at this; rw [this]; clear this
  have := (ε.app <| F.obj X).hom_inv_id; dsimp at this; rw [this]; clear this
  rw [id_comp]; have := (F.mapIso <| η.app X).hom_inv_id; dsimp at this; rw [this]

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

Goal state before:
pp: T : Type u
inst✝ : Category.{v, u} T
f : Arrow T
⊢ mk f.hom = f

Tactic:
cases f

Goal state after:
case mk
T : Type u
inst✝ : Category.{v, u} T
left✝ right✝ : T
hom✝ : (𝟭 T).obj left✝ ⟶ (𝟭 T).obj right✝
⊢ mk (hom { left := left✝, right := right✝, hom := hom✝ }) = { left := left✝, right := right✝, hom := hom✝ }
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
ι : Type u_3
W : ι → MorphismProperty C
⊢ (⨆ i, W i).toSet = ⋃ i, (W i).toSet

Tactic:
by
  ext
  simp [mem_toSet_iff]

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

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : ofHoms P.homFamily f
⊢ P f

Tactic:
ofHoms_iff

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : ∃ i, Arrow.mk f = Arrow.mk (P.homFamily i)
⊢ P f
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.isomorphisms C f → MorphismProperty.isomorphisms C (e.hom ≫ f)

Tactic:
· intro X Y Z e f
      simp only [isomorphisms.iff]
      intro
      exact IsIso.comp_isIso

Goal state after:
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.isomorphisms C f → MorphismProperty.isomorphisms C (f ≫ e.hom)

Tactic:
· intro X Y Z e f
      simp only [isomorphisms.iff]
      intro
      exact IsIso.comp_isIso

Goal state after:
Module: Mathlib.CategoryTheory.Endomorphism

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
f g : (End X)ˣ
⊢ { hom := ↑(f * g), inv := (f * g).inv, hom_inv_id := ⋯, inv_hom_id := ⋯ } =
    { hom := ↑f, inv := f.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ } *
      { hom := ↑g, inv := g.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

Tactic:
cases f

Goal state after:
case mk
C : Type u
inst✝ : Category.{v, u} C
X : C
g : (End X)ˣ
val✝ inv✝ : End X
val_inv✝ : val✝ * inv✝ = 1
inv_val✝ : inv✝ * val✝ = 1
⊢ { hom := ↑({ val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } * g),
      inv := ({ val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ } * g).inv, hom_inv_id := ⋯,
      inv_hom_id := ⋯ } =
    { hom := ↑{ val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ },
        inv := { val := val✝, inv := inv✝, val_inv := val_inv✝, inv_val := inv_val✝ }.inv, hom_inv_id := ⋯,
        inv_hom_id := ⋯ } *
      { hom := ↑g, inv := g.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }
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✝
F : J ⥤ C
s : Cone F
G : K ⥤ C
t : Cone G
P : IsLimit s
Q : IsLimit t
e : J ≌ K
w : e.functor ⋙ G ≅ F
w' : e.inverse ⋙ F ≅ G := (e.inverse.isoWhiskerLeft w).symm ≪≫ e.invFunIdAssoc G
j : J
⊢ s.π.app (e.inverse.obj (e.functor.obj j)) ≫
      w.inv.app (e.inverse.obj (e.functor.obj j)) ≫ G.map (e.counit.app (e.functor.obj j)) ≫ w.hom.app j =
    s.π.app j

Tactic:
counit_app_functor,

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
t✝ : Cone F✝
F : J ⥤ C
s : Cone F
G : K ⥤ C
t : Cone G
P : IsLimit s
Q : IsLimit t
e : J ≌ K
w : e.functor ⋙ G ≅ F
w' : e.inverse ⋙ F ≅ G := (e.inverse.isoWhiskerLeft w).symm ≪≫ e.invFunIdAssoc G
j : J
⊢ s.π.app (e.inverse.obj (e.functor.obj j)) ≫
      w.inv.app (e.inverse.obj (e.functor.obj j)) ≫ G.map (e.functor.map (e.unitInv.app j)) ≫ w.hom.app j =
    s.π.app j
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type v
Y Y' : C
e : F.RepresentableBy Y
e' : F.RepresentableBy Y'
ε : {X : C} → (X ⟶ Y) ≃ (X ⟶ Y') := fun {X} ↦ e.homEquiv.trans e'.homEquiv.symm
⊢ ∀ {Z Z' : C} (f : Z' ⟶ Z) (g : Z ⟶ Y), ε (f ≫ g) = f ≫ ε g

Tactic:
by simp [ε, comp_homEquiv_symm, homEquiv_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Category.Cat

Goal state before:
pp: case h_map
X✝ : Type u
X Y : Discrete X✝
f : X ⟶ Y
⊢ (Discrete.functor (Discrete.mk ∘ ⇑(ConcreteCategory.hom (𝟙 X✝)))).map f =
    eqToHom ⋯ ≫ (𝟭 (Discrete X✝)).map f ≫ eqToHom ⋯

Tactic:
cases f

Goal state after:
case h_map.up
X✝ : Type u
X Y : Discrete X✝
down✝ : PLift (X.as = Y.as)
⊢ (Discrete.functor (Discrete.mk ∘ ⇑(ConcreteCategory.hom (𝟙 X✝)))).map { down := down✝ } =
    eqToHom ⋯ ≫ (𝟭 (Discrete X✝)).map { down := down✝ } ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Limits.Cones

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
c c' : Cone F
f g : c ⟶ c'
w : f.hom = g.hom
⊢ f = g

Tactic:
cases f

Goal state after:
case mk
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
c c' : Cone F
g : c ⟶ c'
hom✝ : c.pt ⟶ c'.pt
w✝ : ∀ (j : J), hom✝ ≫ c'.π.app j = c.π.app j
w : { hom := hom✝, w := w✝ }.hom = g.hom
⊢ { hom := hom✝, w := w✝ } = g
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
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.PreservesMonomorphisms
inst✝ : G.PreservesMonomorphisms
X✝ Y✝ : C
f : X✝ ⟶ Y✝
h : Mono f
⊢ Mono ((F ⋙ G).map f)

Tactic:
comp_map

Goal state after:
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.PreservesMonomorphisms
inst✝ : G.PreservesMonomorphisms
X✝ Y✝ : C
f : X✝ ⟶ Y✝
h : Mono f
⊢ Mono (G.map (F.map f))
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 : C ⥤ D
inst✝¹ : F.IsEquivalence
inst✝ : SplitEpiCategory C
X Y : D
f : X ⟶ Y
⊢ ∀ [Epi f], IsSplitEpi f

Tactic:
by
    intro
    rw [← F.inv.isSplitEpi_iff f]
    apply isSplitEpi_of_epi

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
hX : IsTerminal X
hY : IsTerminal Y
f : X ⟶ Y
⊢ f ≫ hX.from Y = 𝟙 X ∧ hX.from Y ≫ f = 𝟙 Y

Tactic:
simp only [IsTerminal.comp_from, IsTerminal.from_self, true_and]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
hX : IsTerminal X
hY : IsTerminal Y
f : X ⟶ Y
⊢ hX.from Y ≫ f = 𝟙 Y
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: J : Type w
X✝ Y✝ Z✝ : WidePullbackShape J
f : X✝.Hom Y✝
g : Y✝.Hom Z✝
⊢ X✝.Hom Z✝

Tactic:
cases f

Goal state after:
case id
J : Type w
X✝ Z✝ : WidePullbackShape J
g : X✝.Hom Z✝
⊢ X✝.Hom Z✝

case term
J : Type w
Z✝ : WidePullbackShape J
j✝ : J
g : Hom none Z✝
⊢ Hom (some j✝) Z✝
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
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasColimit F
G : C ⥤ D
inst✝ : HasColimit (F ⋙ G)
c : Cocone F
j✝ : J
⊢ ι (F ⋙ G) j✝ ≫ post F G ≫ G.map (desc F c) = ι (F ⋙ G) j✝ ≫ desc (F ⋙ G) (G.mapCocone c)

Tactic:
rw [← assoc, colimit.ι_post, ← G.map_comp, colimit.ι_desc, colimit.ι_desc]

Goal state after:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasColimit F
G : C ⥤ D
inst✝ : HasColimit (F ⋙ G)
c : Cocone F
j✝ : J
⊢ G.map (c.ι.app j✝) = (G.mapCocone c).ι.app j✝
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: case none.none
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePullbackShape J ⥤ C
X : C
f✝ : X ⟶ F.obj none
π : (j : J) → X ⟶ F.obj (some j)
w : ∀ (j : J), π j ≫ F.map (Hom.term j) = f✝
f : none ⟶ none
⊢ (((Functor.const (WidePullbackShape J)).obj X).map f ≫
      match none with
      | none => f✝
      | some j => π j) =
    (match none with
      | none => f✝
      | some j => π j) ≫
      F.map f

Tactic:
cases f

Goal state after:
case none.none.id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePullbackShape J ⥤ C
X : C
f : X ⟶ F.obj none
π : (j : J) → X ⟶ F.obj (some j)
w : ∀ (j : J), π j ≫ F.map (Hom.term j) = f
⊢ (((Functor.const (WidePullbackShape J)).obj X).map (Hom.id none) ≫
      match none with
      | none => f
      | some j => π j) =
    (match none with
      | none => f
      | some j => π j) ≫
      F.map (Hom.id none)
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: case none.some
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePullbackShape J ⥤ C
X : C
f✝ : X ⟶ F.obj none
π : (j : J) → X ⟶ F.obj (some j)
w : ∀ (j : J), π j ≫ F.map (Hom.term j) = f✝
val✝ : J
f : none ⟶ some val✝
⊢ (((Functor.const (WidePullbackShape J)).obj X).map f ≫
      match some val✝ with
      | none => f✝
      | some j => π j) =
    (match none with
      | none => f✝
      | some j => π j) ≫
      F.map f

Tactic:
cases f

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

Goal state before:
pp: case some.none
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePullbackShape J ⥤ C
X : C
f✝ : X ⟶ F.obj none
π : (j : J) → X ⟶ F.obj (some j)
w : ∀ (j : J), π j ≫ F.map (Hom.term j) = f✝
val✝ : J
f : some val✝ ⟶ none
⊢ (((Functor.const (WidePullbackShape J)).obj X).map f ≫
      match none with
      | none => f✝
      | some j => π j) =
    (match some val✝ with
      | none => f✝
      | some j => π j) ≫
      F.map f

Tactic:
cases f

Goal state after:
case some.none.term
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePullbackShape J ⥤ C
X : C
f : X ⟶ F.obj none
π : (j : J) → X ⟶ F.obj (some j)
w : ∀ (j : J), π j ≫ F.map (Hom.term j) = f
val✝ : J
⊢ (((Functor.const (WidePullbackShape J)).obj X).map (Hom.term val✝) ≫
      match none with
      | none => f
      | some j => π j) =
    (match some val✝ with
      | none => f
      | some j => π j) ≫
      F.map (Hom.term val✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: case some.some
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePullbackShape J ⥤ C
X : C
f✝ : X ⟶ F.obj none
π : (j : J) → X ⟶ F.obj (some j)
w : ∀ (j : J), π j ≫ F.map (Hom.term j) = f✝
val✝¹ val✝ : J
f : some val✝¹ ⟶ some val✝
⊢ (((Functor.const (WidePullbackShape J)).obj X).map f ≫
      match some val✝ with
      | none => f✝
      | some j => π j) =
    (match some val✝¹ with
      | none => f✝
      | some j => π j) ≫
      F.map f

Tactic:
cases f

Goal state after:
case some.some.id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePullbackShape J ⥤ C
X : C
f : X ⟶ F.obj none
π : (j : J) → X ⟶ F.obj (some j)
w : ∀ (j : J), π j ≫ F.map (Hom.term j) = f
val✝ : J
⊢ (((Functor.const (WidePullbackShape J)).obj X).map (Hom.id (some val✝)) ≫
      match some val✝ with
      | none => f
      | some j => π j) =
    (match some val✝ with
      | none => f
      | some j => π j) ≫
      F.map (Hom.id (some val✝))
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: J : Type w
X✝ Y✝ Z✝ : WidePushoutShape J
f : X✝.Hom Y✝
g : Y✝.Hom Z✝
⊢ X✝.Hom Z✝

Tactic:
cases f

Goal state after:
case id
J : Type w
X✝ Z✝ : WidePushoutShape J
g : X✝.Hom Z✝
⊢ X✝.Hom Z✝

case init
J : Type w
Z✝ : WidePushoutShape J
j✝ : J
g : Hom (some j✝) Z✝
⊢ Hom none Z✝