mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness

Goal state before:
pp: case add
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x y : M ⊗[R] N
hx : ∃ S, x = S.sum fun m n ↦ m ⊗ₜ[R] n
hy : ∃ S, y = S.sum fun m n ↦ m ⊗ₜ[R] n
⊢ ∃ S, x + y = S.sum fun m n ↦ m ⊗ₜ[R] n

Tactic:
obtain ⟨Sx, hx⟩ := hx

Goal state after:
case add
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x y : M ⊗[R] N
hy : ∃ S, y = S.sum fun m n ↦ m ⊗ₜ[R] n
Sx : M →₀ N
hx : x = Sx.sum fun m n ↦ m ⊗ₜ[R] n
⊢ ∃ S, x + y = S.sum fun m n ↦ m ⊗ₜ[R] n
Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x : M ⊗[R] N
S : N →₀ M
h : (TensorProduct.comm R M N) x = S.sum fun m n ↦ m ⊗ₜ[R] n
⊢ (TensorProduct.comm R M N) x = (TensorProduct.comm R M N) (S.sum fun n m ↦ m ⊗ₜ[R] n)

Tactic:
simp_rw [h, Finsupp.sum, map_sum, comm_tmul]

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: case a.refine_3
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal A
x : A ⊗[R] B
hx : x ∈ ↑(Submodule.restrictScalars R (Submodule.span (A ⊗[R] B) (⇑includeLeft '' ↑I)))
⊢ ∀ (x y : A ⊗[R] B),
    x ∈ Submodule.span (A ⊗[R] B) (⇑includeLeft '' ↑I) →
      y ∈ Submodule.span (A ⊗[R] B) (⇑includeLeft '' ↑I) →
        (∃ y, (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y = x) →
          (∃ y_1, (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y_1 = y) →
            ∃ y_1, (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) y_1 = x + y

Tactic:
rintro x y - - ⟨x, hx, rfl⟩ ⟨y, hy, rfl⟩
      use x + y
      simp only [map_add]

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: case a.zero
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal A
⊢ (LinearMap.rTensor B (Submodule.restrictScalars R I).subtype) 0 ∈ ↑(Submodule.restrictScalars R (map includeLeft I))

Tactic:
rw [map_zero]
        apply zero_mem

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: case a.refine_3
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal B
x : A ⊗[R] B
hx : x ∈ ↑(Submodule.restrictScalars R (Submodule.span (A ⊗[R] B) (⇑includeRight '' ↑I)))
⊢ ∀ (x y : A ⊗[R] B),
    x ∈ Submodule.span (A ⊗[R] B) (⇑includeRight '' ↑I) →
      y ∈ Submodule.span (A ⊗[R] B) (⇑includeRight '' ↑I) →
        (∃ y, (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) y = x) →
          (∃ y_1, (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) y_1 = y) →
            ∃ y_1, (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) y_1 = x + y

Tactic:
rintro x y - - ⟨x, hx, rfl⟩ ⟨y, hy, rfl⟩
      use x + y
      simp only [map_add]

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Finiteness

Goal state before:
pp: case insert.refine_3
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
s✝ : Set (M ⊗[R] N)
a : M ⊗[R] N
s : Set (M ⊗[R] N)
a✝ : a ∉ s
hs✝ : s.Finite
M' : Submodule R M
N' : Submodule R N
hM' : M'.FG
hN' : N'.FG
h : s ⊆ ↑(mapIncl M' N').range
x y : M ⊗[R] N
M₁' : Submodule R M
N₁' : Submodule R N
hM₁' : M₁'.FG
hN₁' : N₁'.FG
h₁ : insert x s ⊆ ↑(mapIncl M₁' N₁').range
M₂' : Submodule R M
N₂' : Submodule R N
hM₂' : M₂'.FG
hN₂' : N₂'.FG
h₂ : insert y s ⊆ ↑(mapIncl M₂' N₂').range
⊢ ∃ M' N', M'.FG ∧ N'.FG ∧ insert (x + y) s ⊆ ↑(mapIncl M' N').range

Tactic:
refine ⟨_, _, hM₁'.sup hM₂', hN₁'.sup hN₂', Set.insert_subset (add_mem ?_ ?_) fun z hz ↦ ?_⟩

Goal state after:
case insert.refine_3.refine_1
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
s✝ : Set (M ⊗[R] N)
a : M ⊗[R] N
s : Set (M ⊗[R] N)
a✝ : a ∉ s
hs✝ : s.Finite
M' : Submodule R M
N' : Submodule R N
hM' : M'.FG
hN' : N'.FG
h : s ⊆ ↑(mapIncl M' N').range
x y : M ⊗[R] N
M₁' : Submodule R M
N₁' : Submodule R N
hM₁' : M₁'.FG
hN₁' : N₁'.FG
h₁ : insert x s ⊆ ↑(mapIncl M₁' N₁').range
M₂' : Submodule R M
N₂' : Submodule R N
hM₂' : M₂'.FG
hN₂' : N₂'.FG
h₂ : insert y s ⊆ ↑(mapIncl M₂' N₂').range
⊢ x ∈ (mapIncl (M₁' ⊔ M₂') (N₁' ⊔ N₂')).range

case insert.refine_3.refine_2
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
s✝ : Set (M ⊗[R] N)
a : M ⊗[R] N
s : Set (M ⊗[R] N)
a✝ : a ∉ s
hs✝ : s.Finite
M' : Submodule R M
N' : Submodule R N
hM' : M'.FG
hN' : N'.FG
h : s ⊆ ↑(mapIncl M' N').range
x y : M ⊗[R] N
M₁' : Submodule R M
N₁' : Submodule R N
hM₁' : M₁'.FG
hN₁' : N₁'.FG
h₁ : insert x s ⊆ ↑(mapIncl M₁' N₁').range
M₂' : Submodule R M
N₂' : Submodule R N
hM₂' : M₂'.FG
hN₂' : N₂'.FG
h₂ : insert y s ⊆ ↑(mapIncl M₂' N₂').range
⊢ y ∈ (mapIncl (M₁' ⊔ M₂') (N₁' ⊔ N₂')).range

case insert.refine_3.refine_3
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
s✝ : Set (M ⊗[R] N)
a : M ⊗[R] N
s : Set (M ⊗[R] N)
a✝ : a ∉ s
hs✝ : s.Finite
M' : Submodule R M
N' : Submodule R N
hM' : M'.FG
hN' : N'.FG
h : s ⊆ ↑(mapIncl M' N').range
x y : M ⊗[R] N
M₁' : Submodule R M
N₁' : Submodule R N
hM₁' : M₁'.FG
hN₁' : N₁'.FG
h₁ : insert x s ⊆ ↑(mapIncl M₁' N₁').range
M₂' : Submodule R M
N₂' : Submodule R N
hM₂' : M₂'.FG
hN₂' : N₂'.FG
h₂ : insert y s ⊆ ↑(mapIncl M₂' N₂').range
z : M ⊗[R] N
hz : z ∈ s
⊢ z ∈ ↑(mapIncl (M₁' ⊔ M₂') (N₁' ⊔ N₂')).range
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: case a.zero
R : Type u_1
inst✝⁴ : CommSemiring R
A : Type u_2
B : Type u_3
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal B
⊢ (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) 0 ∈ ↑(Submodule.restrictScalars R (map includeRight I))

Tactic:
rw [map_zero]
        apply zero_mem

Goal state after:
Module: Mathlib.RingTheory.Flat.Basic

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : ∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P), Injective ⇑(rTensor M N.subtype)
i : N →ₗ[R] M
r : M →ₗ[R] N
h : r ∘ₗ i = LinearMap.id
P : Type u
x✝¹ : AddCommMonoid P
x✝ : Module R P
Q : Submodule R P
⊢ Injective (⇑(lTensor P i) ∘ ⇑(rTensor N Q.subtype))

Tactic:
rw [← coe_comp, lTensor_comp_rTensor, ← rTensor_comp_lTensor, coe_comp]

Goal state after:
R : Type u
M : Type v
N : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : ∀ ⦃P : Type u⦄ [inst : AddCommMonoid P] [inst_1 : Module R P] (N : Submodule R P), Injective ⇑(rTensor M N.subtype)
i : N →ₗ[R] M
r : M →ₗ[R] N
h : r ∘ₗ i = LinearMap.id
P : Type u
x✝¹ : AddCommMonoid P
x✝ : Module R P
Q : Submodule R P
⊢ Injective (⇑(rTensor M Q.subtype) ∘ ⇑(lTensor (↥Q) i))
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝⁹ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝⁸ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁷ : (i : ι) → FunLike (H i) (G i) C
inst✝⁶ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁵ : IsDirectedOrder ι
inst✝⁴ : Nonempty ι
inst✝³ : (i : ι) → GroupWithZero (G i)
inst✝² : GroupWithZero C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MonoidWithZeroHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), MonoidWithZeroHomClass (H i) (G i) C
⊢ ⟦⟨⟨Classical.arbitrary ι, (fun x ↦ 0) (Classical.arbitrary ι)⟩.fst,
        (fun x x_1 ↦ x_1⁻¹) ⟨Classical.arbitrary ι, (fun x ↦ 0) (Classical.arbitrary ι)⟩.fst
          ⟨Classical.arbitrary ι, (fun x ↦ 0) (Classical.arbitrary ι)⟩.snd⟩⟧ =
    ⟦⟨Classical.arbitrary ι, (fun x ↦ 0) (Classical.arbitrary ι)⟩⟧

Tactic:
simp_rw [inv_zero]

Goal state after:
Module: Mathlib.Algebra.Group.EvenFunction

Goal state before:
pp: α : Type u_1
inst✝¹ : Neg α
R : Type u_3
inst✝ : Mul R
f g : α → R
hf : Function.Even f
hg : Function.Even g
⊢ Function.Even (f * g)

Tactic:
by
  intro a
  simp only [Pi.mul_apply, hf a, hg a]

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

Goal state before:
pp: m n : ℕ
a✝ : ℤ
⊢ a✝ ∈ Ioo (-(↑m + 1)) (↑n + 1) ↔ a✝ ∈ Ioo (-↑m) ↑n ∪ {-↑m, ↑n}

Tactic:
simp only [mem_Ioo, union_insert, union_singleton, mem_insert]

Goal state after:
m n : ℕ
a✝ : ℤ
⊢ -(↑m + 1) < a✝ ∧ a✝ < ↑n + 1 ↔ a✝ = -↑m ∨ a✝ = ↑n ∨ -↑m < a✝ ∧ a✝ < ↑n
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
M' : Type u_5
inst✝⁴¹ : AddCommMonoid M₁✝
inst✝⁴⁰ : AddCommMonoid M₂✝
inst✝³⁹ : AddCommMonoid M
inst✝³⁸ : AddCommMonoid M'
inst✝³⁷ : Module R✝ M₁✝
inst✝³⁶ : Module R✝ M₂✝
inst✝³⁵ : Module R✝ M
inst✝³⁴ : Module R✝ M'
f✝¹ : M₁✝ →ₗ[R✝] M₂✝ →ₗ[R✝] M
N₁ : Type u_6
N₂ : Type u_7
N : Type u_8
inst✝³³ : AddCommMonoid N₁
inst✝³² : AddCommMonoid N₂
inst✝³¹ : AddCommMonoid N
inst✝³⁰ : Module R✝ N₁
inst✝²⁹ : Module R✝ N₂
inst✝²⁸ : Module R✝ N
g✝¹ : N₁ →ₗ[R✝] N₂ →ₗ[R✝] N
R : Type u_9
S : Type u_10
inst✝²⁷ : CommSemiring R
inst✝²⁶ : CommSemiring S
inst✝²⁵ : Algebra R S
M₁ : Type u_11
M₂ : Type u_12
M₃ : Type u_13
M₁₂ : Type u_14
M₂₃ : Type u_15
inst✝²⁴ : AddCommMonoid M₁
inst✝²³ : AddCommMonoid M₂
inst✝²² : AddCommMonoid M₃
inst✝²¹ : AddCommMonoid M₁₂
inst✝²⁰ : AddCommMonoid M₂₃
inst✝¹⁹ : Module R M₁
inst✝¹⁸ : Module R M₂
inst✝¹⁷ : Module S M₂
inst✝¹⁶ : IsScalarTower R S M₂
inst✝¹⁵ : Module R M₃
inst✝¹⁴ : Module S M₃
inst✝¹³ : IsScalarTower R S M₃
inst✝¹² : Module R M₁₂
inst✝¹¹ : Module S M₁₂
inst✝¹⁰ : IsScalarTower R S M₁₂
inst✝⁹ : Module R M₂₃
inst✝⁸ : Module S M₂₃
inst✝⁷ : IsScalarTower R S M₂₃
f✝ : M₁ →ₗ[R] M₂ →ₗ[S] M₁₂
hf✝ : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f✝)
g✝ : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg✝ : IsTensorProduct g✝
T : Type u_16
inst✝⁶ : CommSemiring T
inst✝⁵ : Algebra R T
inst✝⁴ : Module T M₁
inst✝³ : IsScalarTower R T M₁
inst✝² : Module T M₁₂
inst✝¹ : SMulCommClass S T M₁₂
inst✝ : IsScalarTower R T M₁₂
f : M₁ →ₗ[T] M₂ →ₗ[S] M₁₂
hf : IsTensorProduct (LinearMap.restrictScalars₁₂ R R f)
g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃
hg : IsTensorProduct g
t : T
x : M₁₂ ⊗[S] M₃
⊢ (↑(assocAux (LinearMap.restrictScalars₁₂ R S f) hf g hg)).toFun (t • x) =
    (RingHom.id T) t • (↑(assocAux (LinearMap.restrictScalars₁₂ R S f) hf g hg)).toFun x

Tactic:
by
    induction x with
    | zero => simp
    | add x y _ _ => simp_all
    | tmul x y =>
    obtain ⟨x, rfl⟩ := hf.equiv.surjective x
    induction x with
    | zero => simp
    | add x y _ _ => simp_all [add_tmul]
    | tmul x z =>
      have : t • (f x) z = f (t • x) z := by simp
      dsimp
      rw [smul_tmul', this, ← f.restrictScalars₁₂_apply_apply R S,
        ← f.restrictScalars₁₂_apply_apply R S, IsTensorProduct.assocAux_tmul,
        IsTensorProduct.assocAux_tmul, TensorProduct.smul_tmul']

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

Goal state before:
pp: α : Type u_1
⊢ diagSet = fromRel ⋯

Tactic:
ext ⟨a, b⟩; simp

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

Goal state before:
pp: α : Type u_1
⊢ diagSetᶜ = fromRel ⋯

Tactic:
ext ⟨a, b⟩; simp

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

Goal state before:
pp: V W : Type u
inst✝¹ : Quiver V
inst✝ : Quiver W
Fobj : V → W
Fmap : {X Y : V} → (X ⟶ Y) → (Fobj X ⟶ Fobj Y)
Gobj : V → W
Gmap : {X Y : V} → (X ⟶ Y) → (Gobj X ⟶ Gobj Y)
h_obj : ∀ (X : V), { obj := Fobj, map := Fmap }.obj X = { obj := Gobj, map := Gmap }.obj X
h_map :
  ∀ (X Y : V) (f : X ⟶ Y), { obj := Fobj, map := Fmap }.map f = Quiver.homOfEq ({ obj := Gobj, map := Gmap }.map f) ⋯ ⋯
⊢ { obj := Fobj, map := Fmap } = { obj := Gobj, map := Gmap }

Tactic:
obtain rfl : Fobj = Gobj := funext h_obj

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ⟶ G
X Y : C
f : X ⟶ Y
inst✝¹ : IsIso (α.app X)
inst✝ : IsIso (α.app Y)
⊢ inv (α.app X) ≫ F.map f = G.map f ≫ inv (α.app Y)

Tactic:
rw [IsIso.inv_comp_eq, ← Category.assoc, IsIso.eq_comp_inv]
  exact α.naturality f

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y Z : C
f : X ⟶ Y
h : Y = Z
⊢ f ≫ eqToHom h ≍ f

Tactic:
rw [← conj_eqToHom_iff_heq' _ _ rfl h, eqToHom_refl, Category.id_comp]

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
h_obj : ∀ (X : C), F.obj X = G.obj X
h_map : ∀ (X Y : C) (f : X ⟶ Y), F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯
⊢ F = G

Tactic:
match F, G with
  | mk F_obj _ _ _, mk G_obj _ _ _ =>
    obtain rfl : F_obj = G_obj := by
      ext X
      apply h_obj
    congr
    funext X Y f
    simpa using h_map X Y f

Goal state after:
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 : C ≌ D
Y : D
⊢ e.unit.app (e.inverse.obj Y) ≫ e.inverse.map (e.counit.app Y) = 𝟙 (e.inverse.obj Y)

Tactic:
← id_comp (e.inverse.map _),

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ e.unit.app (e.inverse.obj Y) ≫ 𝟙 (e.inverse.obj (e.functor.obj (e.inverse.obj Y))) ≫ e.inverse.map (e.counit.app Y) =
    𝟙 (e.inverse.obj Y)
Module: Mathlib.CategoryTheory.Whiskering

Goal state before:
pp: C✝ : Type u₁
inst✝³ : Category.{v₁, u₁} C✝
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F : D ⥤ E
hF : F.FullyFaithful
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X✝ Y✝ : C ⥤ D
f : ((Functor.whiskeringRight C D E).obj F).obj X✝ ⟶ ((Functor.whiskeringRight C D E).obj F).obj Y✝
x✝¹ x✝ : C
g : x✝¹ ⟶ x✝
⊢ X✝.map g ≫ hF.preimage (f.app x✝) = hF.preimage (f.app x✝¹) ≫ Y✝.map g

Tactic:
by
        apply hF.map_injective
        simp only [map_comp, map_preimage]
        apply f.naturality

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : IsDiscrete C
⊢ ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y), X = Y

Tactic:
by
    rintro ⟨_⟩ ⟨_⟩ ⟨f⟩
    obtain rfl := obj_ext_of_isDiscrete f
    rfl

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 : F ⊣ G
X : C
Y Y' : D
f : X ⟶ G.obj Y
g : Y ⟶ Y'
⊢ (adj.homEquiv X Y').symm (f ≫ G.map g) = (adj.homEquiv X Y).symm f ≫ g

Tactic:
rw [Equiv.symm_apply_eq]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X : C
Y Y' : D
f : X ⟶ G.obj Y
g : Y ⟶ Y'
⊢ f ≫ G.map g = (adj.homEquiv X Y') ((adj.homEquiv X Y).symm f ≫ g)
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 Y' : D
f : X ⟶ G.obj Y
g : Y ⟶ Y'
⊢ (adj.homEquiv X Y').symm (f ≫ G.map g) = (adj.homEquiv X Y).symm f ≫ g

Tactic:
rw [Equiv.symm_apply_eq]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquiv F G
X : C
Y Y' : D
f : X ⟶ G.obj Y
g : Y ⟶ Y'
⊢ f ≫ G.map g = (adj.homEquiv X Y') ((adj.homEquiv X Y).symm f ≫ g)
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
h : IsColimit t
W : C
ι : F ⟶ (const J).obj W
j j' : J
f : j ⟶ j'
⊢ F.map f ≫ (fun j ↦ ι.app j) j' = (fun j ↦ ι.app j) j

Tactic:
convert! ← ι.naturality f; apply comp_id

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

Tactic:
rw [Equiv.symm_apply_eq]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
G_obj : D → C
e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y)
he : ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y), (e X' Y) (F.map f ≫ g) = f ≫ (e X Y) g
X X' : C
Y : D
f : X ⟶ X'
g : X' ⟶ (rightAdjointOfEquiv e he).obj Y
⊢ f ≫ g = (e X Y) (F.map f ≫ (e X' Y).symm g)
Module: Mathlib.CategoryTheory.Limits.IsLimit

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : F.cocones.CorepresentableBy X
s : Cocone F
| (colimitCocone h).extend (homOfCocone h (coconeOfHom h (homOfCocone h s)))

Tactic:
simp only [homOfCocone_coconeOfHom]

Goal state after:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : F.cocones.CorepresentableBy X
s : Cocone F
| (colimitCocone h).extend (homOfCocone h s)
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (ρ_ f).inv ▷ g ≫ (α_ f (𝟙 b) g).hom = f ◁ (λ_ g).inv

Tactic:
simp [← cancel_mono (f ◁ (λ_ g).hom)]

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type v
Y : C
e e' : F.RepresentableBy Y
h : e.homEquiv (𝟙 Y) = e'.homEquiv (𝟙 Y)
⊢ e = e'

Tactic:
by
  have : ∀ {X : C} (f : X ⟶ Y), e.homEquiv f = e'.homEquiv f := fun {X} f ↦ by
    rw [e.homEquiv_eq, e'.homEquiv_eq, h]
  obtain ⟨e, he⟩ := e
  obtain ⟨e', he'⟩ := e'
  obtain rfl : @e = @e' := by ext; apply this
  rfl

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (f ◁ (ρ_ g).hom) ▷ 𝟙 c = (α_ f g (𝟙 c)).inv ▷ 𝟙 c ≫ (ρ_ (f ≫ g)).hom ▷ 𝟙 c

Tactic:
← cancel_epi (α_ _ _ _).inv,

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (α_ f (g ≫ 𝟙 c) (𝟙 c)).inv ≫ (f ◁ (ρ_ g).hom) ▷ 𝟙 c =
    (α_ f (g ≫ 𝟙 c) (𝟙 c)).inv ≫ (α_ f g (𝟙 c)).inv ▷ 𝟙 c ≫ (ρ_ (f ≫ g)).hom ▷ 𝟙 c
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : SmallCategory C
⊢ ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    (yoneda.op ⋙ coyoneda).map f ≫ (NatIso.ofComponents (fun x ↦ yonedaEquiv.toIso) ⋯).hom =
      (NatIso.ofComponents (fun x ↦ yonedaEquiv.toIso) ⋯).hom ≫ (evaluation Cᵒᵖ (Type u₁)).map f

Tactic:
intro X Y f
    ext a b
    simp [yonedaEquiv, ← NatTrans.naturality_apply]

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

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
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
⊢ ⋯.HasLift ↔ sq.HasLift

Tactic:
simp only [HasLift.iff]
  exact Equiv.nonempty_congr (sq.rightAdjointLiftStructEquiv adj).symm

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

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
F G : WidePullbackShape ι ⥤ C
base : F.obj none ≅ G.obj none
comp : (i : ι) → F.obj (some i) ≅ G.obj (some i)
w : ∀ (i : ι), F.map (Hom.term i) ≫ base.hom = (comp i).hom ≫ G.map (Hom.term i)
X✝ Y✝ : WidePullbackShape ι
f : X✝ ⟶ Y✝
⊢ F.map f ≫
      (match Y✝ with
        | none => base
        | some i => comp i).hom =
    (match X✝ with
        | none => base
        | some i => comp i).hom ≫
      G.map f

Tactic:
rcases f

Goal state after:
case id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
F G : WidePullbackShape ι ⥤ C
base : F.obj none ≅ G.obj none
comp : (i : ι) → F.obj (some i) ≅ G.obj (some i)
w : ∀ (i : ι), F.map (Hom.term i) ≫ base.hom = (comp i).hom ≫ G.map (Hom.term i)
X✝ : WidePullbackShape ι
⊢ F.map (Hom.id X✝) ≫
      (match X✝ with
        | none => base
        | some i => comp i).hom =
    (match X✝ with
        | none => base
        | some i => comp i).hom ≫
      G.map (Hom.id X✝)

case term
J : Type w
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
F G : WidePullbackShape ι ⥤ C
base : F.obj none ≅ G.obj none
comp : (i : ι) → F.obj (some i) ≅ G.obj (some i)
w : ∀ (i : ι), F.map (Hom.term i) ≫ base.hom = (comp i).hom ≫ G.map (Hom.term i)
j✝ : ι
⊢ F.map (Hom.term j✝) ≫
      (match none with
        | none => base
        | some i => comp i).hom =
    (match some j✝ with
        | none => base
        | some i => comp i).hom ≫
      G.map (Hom.term j✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
W X Y Z : C
inst✝¹ : HasBinaryProduct W Y
inst✝ : HasBinaryProduct X Z
g : W ⟶ X
g' : Y ⟶ Z
⊢ lift (fst ≫ g) (snd ≫ g') = map g g'

Tactic:
rw [← prod.lift_map]
  simp

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

Goal state before:
pp: T : Type u₁
inst✝³ : Category.{v₁, u₁} T
D : Type u₂
inst✝² : Category.{v₂, u₂} D
X : T
f g : Under X
φ : f ⟶ g
F : T ⥤ D
inst✝¹ : F.Full
inst✝ : F.EssSurj
B : Under (F.obj X)
⊢ (post F).essImage B

Tactic:
by
    obtain ⟨B', ⟨e⟩⟩ := Functor.EssSurj.mem_essImage (F := F) B.right
    obtain ⟨f, hf⟩ := F.map_surjective (B.hom ≫ e.inv)
    exact ⟨Under.mk f, ⟨Under.isoMk e⟩⟩

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝¹ inst✝ : HasImage f
⊢ (image.eqToHom ⋯ ≫ image.eqToHom ⋯) ≫ image.ι f = 𝟙 (image f) ≫ image.ι f

Tactic:
simp [image.eqToHom]

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
F : WalkingParallelPair ⥤ C
t : Fork (F.map left) (F.map right)
⊢ ∀ ⦃X Y : WalkingParallelPair⦄ (f : X ⟶ Y),
    ((Functor.const WalkingParallelPair).obj t.pt).map f ≫ t.π.app Y ≫ eqToHom ⋯ = (t.π.app X ≫ eqToHom ⋯) ≫ F.map f

Tactic:
rintro _ _ (_ | _ | _) <;> simp [t.condition]

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
F : WalkingParallelPair ⥤ C
t : Cofork (F.map left) (F.map right)
⊢ ∀ ⦃X Y : WalkingParallelPair⦄ (f : X ⟶ Y),
    F.map f ≫ eqToHom ⋯ ≫ t.ι.app Y = (eqToHom ⋯ ≫ t.ι.app X) ≫ ((Functor.const WalkingParallelPair).obj t.pt).map f

Tactic:
rintro _ _ (_ | _ | _) <;> simp [t.condition]

Goal state after: