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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
hfg : Exact ⇑f ⇑g
h : P → N
hgh : RightInverse h ⇑g
⊢ ∀ (x : N ⊗[R] Q), (inverse_of_rightInverse Q hfg hgh ∘ₗ rTensor Q g) x = (rTensor Q f).range.mkQ x

Tactic:
intro y

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
hfg : Exact ⇑f ⇑g
h : P → N
hgh : RightInverse h ⇑g
y : N ⊗[R] Q
⊢ (inverse_of_rightInverse Q hfg hgh ∘ₗ rTensor Q g) y = (rTensor Q f).range.mkQ y
Module: Mathlib.LinearAlgebra.TensorProduct.RightExactness

Goal state before:
pp: case h
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)))
a : A
b : B
x : A
y : ↥(Submodule.restrictScalars R I)
⊢ (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) ((a * x) ⊗ₜ[R] (b • y)) =
    a ⊗ₜ[R] b • (LinearMap.lTensor A (Submodule.restrictScalars R I).subtype) (x ⊗ₜ[R] y)

Tactic:
simp only [LinearMap.lTensor_tmul, Submodule.coe_subtype, smul_eq_mul, tmul_mul_tmul]

Goal state after:
case h
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)))
a : A
b : B
x : A
y : ↥(Submodule.restrictScalars R I)
⊢ (a * x) ⊗ₜ[R] ↑(b • y) = (a * x) ⊗ₜ[R] (b * ↑y)
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 ⇑(rTensor M Q.subtype ∘ₗ lTensor (↥Q) i)

Tactic:
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.RingTheory.Flat.Basic

Goal state before:
pp: R : Type u
M : Type v
N : Type u_1
P✝ : Type u_2
Q : Type u_3
inst✝¹⁴ : CommSemiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : Module R N
inst✝⁹ : AddCommMonoid P✝
inst✝⁸ : Module R P✝
inst✝⁷ : AddCommMonoid Q
inst✝⁶ : Module R Q
S : Type u_4
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : Flat S M
inst✝ : Flat R N
P : Type u_4
x✝¹ : AddCommMonoid P
x✝ : Module S P
I : Submodule S P
⊢ Injective ⇑(rTensor (M ⊗[R] N) I.subtype)

Tactic:
let := RestrictScalars.moduleOrig R S P

Goal state after:
R : Type u
M : Type v
N : Type u_1
P✝ : Type u_2
Q : Type u_3
inst✝¹⁴ : CommSemiring R
inst✝¹³ : AddCommMonoid M
inst✝¹² : Module R M
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : Module R N
inst✝⁹ : AddCommMonoid P✝
inst✝⁸ : Module R P✝
inst✝⁷ : AddCommMonoid Q
inst✝⁶ : Module R Q
S : Type u_4
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : Flat S M
inst✝ : Flat R N
P : Type u_4
x✝¹ : AddCommMonoid P
x✝ : Module S P
I : Submodule S P
this : Module S (RestrictScalars R S P) := RestrictScalars.moduleOrig R S P
⊢ Injective ⇑(rTensor (M ⊗[R] N) I.subtype)
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.Even g
⊢ Function.Odd (f * g)

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

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝² : AddCommGroup β
inst✝¹ : IsAddTorsionFree β
f : α → β
inst✝ : NegZeroClass α
hf : Function.Odd f
⊢ f 0 = 0

Tactic:
by simp [← neg_eq_self, ← hf 0]

Goal state after:
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:
rw [← h.equiv.right_inv m]

Goal state after:
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 ((↑h.equiv).toFun (h.equiv.invFun m))
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case tmul
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)
x✝ : M₁
y✝ : M₂
⊢ motive ((TensorProduct.lift f) (x✝ ⊗ₜ[R] y✝))

Tactic:
TensorProduct.lift.tmul

Goal state after:
case tmul
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)
x✝ : M₁
y✝ : M₂
⊢ motive ((f x✝) y✝)
Module: Mathlib.Data.Int.Interval

Goal state before:
pp: case inr.mpr.inl.refine_2
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ i + a * (n / a + 1) < n + a

pp: case inr.mpr.inl.refine_3
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ (i + a * (n / a + 1)) % a = i

Tactic:
· calc
        i + a * (n / a + 1) < n % a + a * (n / a + 1) := by gcongr
        _ = n + a := by rw [mul_add, mul_one, ← add_assoc, hn]

Goal state after:
case inr.mpr.inl.refine_3
n a : ℤ
h : 0 ≤ a
ha : 0 < a
i : ℤ
hi₀ : 0 ≤ i
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ (i + a * (n / a + 1)) % a = i
Module: Mathlib.Data.Multiset.Sym

Goal state before:
pp: α : Type u_1
β : Type u_2
m : Multiset α
x✝¹ x✝ : List α
h : x✝¹ ≈ x✝
⊢ ↑x✝¹.sym2 = ↑x✝.sym2

Tactic:
coe_eq_coe

Goal state after:
α : Type u_1
β : Type u_2
m : Multiset α
x✝¹ x✝ : List α
h : x✝¹ ≈ x✝
⊢ x✝¹.sym2.Perm x✝.sym2
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: case inl
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
ha : a ∈ s
⊢ (insert a s).sym2 = image (fun b ↦ s(a, b)) (insert a s) ∪ s.sym2

pp: case inr
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
ha : a ∉ s
⊢ (insert a s).sym2 = image (fun b ↦ s(a, b)) (insert a s) ∪ s.sym2

Tactic:
· simp only [insert_eq_of_mem ha, right_eq_union, image_subset_iff]
    simp_all

Goal state after:
case inr
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
ha : a ∉ s
⊢ (insert a s).sym2 = image (fun b ↦ s(a, b)) (insert a s) ∪ s.sym2
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
⊢ (insert a s).sym2 = image (fun b ↦ s(a, b)) (insert a s) ∪ s.sym2

Tactic:
by
  obtain ha | ha := Decidable.em (a ∈ s)
  · simp only [insert_eq_of_mem ha, right_eq_union, image_subset_iff]
    simp_all
  · simpa [map_eq_image] using! sym2_cons a s ha

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

Goal state before:
pp: α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n : ℕ
h : s.sym n = ∅
⊢ s = ∅

Tactic:
by
  contrapose! h; exact h.sym _

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

Goal state before:
pp: case nil
α : Type u_1
xs : List α
⊢ map ⇑(Sym2.equivSym α) [].sym2 = List.sym 2 []

Tactic:
simp only [List.sym, map_eq_nil_iff, sym2_eq_nil_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
motive : Sym2 α → Sort u_4
f : (a b : α) → motive s(a, b)
h : ∀ (a b : α), f a b ≍ f b a
z : Sym2 α
⊢ ∀ (a b : α × α),
    Rel α a b →
      (match a with
        | (a, b) => f a b) ≍
        match b with
        | (a, b) => f a b

Tactic:
simp only [rel_iff']
    rintro _ _ (rfl | rfl)
    exacts [HEq.rfl, h _ _]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f g : X ⟶ Y
w : ∀ {Z : C} (h : Y ⟶ Z), f ≫ h = g ≫ h
⊢ f = g

Tactic:
convert! w (𝟙 Y)

Goal state after:
case e'_2
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f g : X ⟶ Y
w : ∀ {Z : C} (h : Y ⟶ Z), f ≫ h = g ≫ h
⊢ f = f ≫ 𝟙 Y

case e'_3
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f g : X ⟶ Y
w : ∀ {Z : C} (h : Y ⟶ Z), f ≫ h = g ≫ h
⊢ g = g ≫ 𝟙 Y
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
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
f : M →ₗ[R] N
hf : IsBaseChange S f
h : N →ₗ[S] O
hc : IsBaseChange T (↑R h ∘ₗ f)
⊢ IsBaseChange T h

Tactic:
apply IsBaseChange.of_lift_unique
  intro Q _ _ _ _ r
  let : Module R Q := .restrictScalars R S Q
  have : IsScalarTower R S Q := .restrictScalars R S Q
  have : IsScalarTower R T Q := IsScalarTower.of_algebraMap_smul fun r x ↦ by
    simp [IsScalarTower.algebraMap_apply R S T]
  let r' : M →ₗ[R] Q := r ∘ₗ f
  let q : O →ₗ[T] Q := hc.lift r'
  refine ⟨q, ?_, ?_⟩
  · apply hf.algHom_ext'
    simp [r', q, LinearMap.comp_assoc, hc.lift_comp]
  · intro q' hq'
    apply hc.algHom_ext'
    apply_fun LinearMap.restrictScalars R at hq'
    rw [← LinearMap.comp_assoc]
    rw [show q'.restrictScalars R ∘ₗ h.restrictScalars R = _ from hq', hc.lift_comp]

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

Goal state before:
pp: case mpr
C : Type u
inst✝ : CategoryStruct.{v, u} C
X Y Z : C
⊢ X = Z ∨ Y = Z → pair X Y Z

Tactic:
rintro (rfl | rfl); exacts [⟨Sum.inl .unit⟩, ⟨Sum.inr .unit⟩]

Goal state after:
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
inst✝ : ∀ (X : C), Epi (α.app X)
Z✝ : C ⥤ D
g h : G ⟶ Z✝
eq : α ≫ g = α ≫ h
X : C
⊢ α.app X ≫ g.app X = α.app X ≫ h.app X

Tactic:
← comp_app,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ⟶ G
inst✝ : ∀ (X : C), Epi (α.app X)
Z✝ : C ⥤ D
g h : G ⟶ Z✝
eq : α ≫ g = α ≫ h
X : C
⊢ (α ≫ g).app X = α.app X ≫ h.app X
Module: Mathlib.CategoryTheory.NatIso

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
⊢ ∀ {F₁ F₂ : C ⥤ D} (e : F₁ ≅ F₂), IsIso (F₁.map f) ↔ IsIso (F₂.map f)

Tactic:
suffices ∀ {F₁ F₂ : C ⥤ D} (_ : F₁ ≅ F₂) (_ : IsIso (F₁.map f)), IsIso (F₂.map f) from
    fun F₁ F₂ e => ⟨this e, this e.symm⟩

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
⊢ ∀ {F₁ F₂ : C ⥤ D} (x : F₁ ≅ F₂), IsIso (F₁.map f) → IsIso (F₂.map f)
Module: Mathlib.Logic.Lemmas

Goal state before:
pp: f : Prop → Prop
⊢ f True ∨ f False → ∃ p, f p

Tactic:
by rintro (h | h) <;> exact ⟨_, h⟩

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

Goal state before:
pp: case h_map
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)
Φ : Push σ ⥤q W'
Φ₀ : Φ.obj = τ
Φcomp : of σ ⋙q Φ = φ
⊢ ∀ (X Y : Push σ) (f : X ⟶ Y),
    Φ.map f =
      Eq.recOn ⋯
        (Eq.recOn ⋯
          ({ obj := τ,
                map := @PushQuiver.rec V inst✝¹ W σ (fun X Y x ↦ τ X ⟶ τ Y) fun X Y f ↦ ⋯.mpr (⋯.mpr (φ.map f)) }.map
            f))

Tactic:
· rintro _ _ ⟨⟩
    subst_vars
    simp only [Prefunctor.comp_map]
    rfl

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

Goal state before:
pp: case nil
V : Type u
inst✝ : Quiver V
a b : V
n : ℕ
hp : nil.length = n + 1
⊢ ∃ c f q x, nil = f.toPath.comp q

Tactic:
simp at hp

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

Goal state before:
pp: 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))

Tactic:
· simp only [reverse_reverse]
    rfl

Goal state after:
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 : C ⥤ D
G H : D ⥤ E
α : G ⟶ H
X Y : C
f : X ⟶ Y
⊢ (F ⋙ G).map f ≫ α.app (F.obj Y) = α.app (F.obj X) ≫ (F ⋙ H).map f

Tactic:
rw [Functor.comp_map, Functor.comp_map, α.naturality]

Goal state after:
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
W✝ X✝ Y✝ Z✝ : Cᵒᵖ
f : W✝ ⟶ X✝
g : X✝ ⟶ Y✝
h : Y✝ ⟶ Z✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h

Tactic:
by simp only [← op_comp_unop, Quiver.Hom.unop_op, assoc]

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

Tactic:
simp only [comp_id, assoc, map_comp]

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
A B X Y : C
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
l : sq.LiftStruct
⊢ p.op ≫ l.l.op = g.op

Tactic:
by rw [← op_comp, l.fac_right]

Goal state after:
Module: Mathlib.CategoryTheory.EpiMono

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
se : SplitEpi f
Z✝ : C
g h : Y ⟶ Z✝
w : f ≫ g = f ≫ h
⊢ g = h

Tactic:
replace w := se.section_ ≫= w; simpa using w

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

Goal state before:
pp: A : Type u₁
inst✝⁶ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁵ : Category.{v₂, u₂} B
T : Type u₃
inst✝⁴ : Category.{v₃, u₃} T
A' : Type u₄
inst✝³ : Category.{v₄, u₄} A'
B' : Type u₅
inst✝² : Category.{v₅, u₅} B'
T' : Type u₆
inst✝¹ : Category.{v₆, u₆} T'
L✝ : A ⥤ T
R✝ : B ⥤ T
C : Type u₄
inst✝ : Category.{v₄, u₄} C
F : C ⥤ A
L : A ⥤ T
R : B ⥤ T
X✝ Y✝ : Comma (F ⋙ L) R
f : X✝ ⟶ Y✝
⊢ L.map (F.map f.left) ≫ { left := F.obj Y✝.left, right := Y✝.right, hom := Y✝.hom }.hom =
    { left := F.obj X✝.left, right := X✝.right, hom := X✝.hom }.hom ≫ R.map f.right

Tactic:
by simpa using! f.w

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X : C
Y : D
f : F.obj X ⟶ Y
⊢ F.map (adj.unit.app X) ≫ adj.counit.app (F.obj X) ≫ (𝟭 D).map f = f

Tactic:
← assoc

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 : D
f : F.obj X ⟶ Y
⊢ (F.map (adj.unit.app X) ≫ adj.counit.app (F.obj X)) ≫ (𝟭 D).map f = f
Module: Mathlib.CategoryTheory.Adjunction.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y Y' : D
f : X' ⟶ X
g : F.obj X ⟶ Y'
h : F.obj X' ⟶ Y
k : Y ⟶ Y'
w : f ≫ (adj.homEquiv X Y') g = (adj.homEquiv X' Y) h ≫ G.map k
⊢ F.map f ≫ g = h ≫ k

Tactic:
simpa only [Equiv.symm_apply_apply]
      using homEquiv_naturality_right_square adj _ _ _ _ w

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)
X : C
f : X ⟶ Y
⊢ e.homEquiv f = e'.homEquiv f

Tactic:
by
    rw [e.homEquiv_eq, e'.homEquiv_eq, h]

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type v
X✝ : C
e e' : F.CorepresentableBy X✝
h : e.homEquiv (𝟙 X✝) = e'.homEquiv (𝟙 X✝)
X : C
f : X✝ ⟶ X
⊢ e.homEquiv f = e'.homEquiv f

Tactic:
by
    rw [e.homEquiv_eq, e'.homEquiv_eq, h]

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

Goal state before:
pp: X✝ Y✝ Z✝ : Type u
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (Discrete.functor (Discrete.mk ∘ ⇑(ConcreteCategory.hom (f ≫ g)))).toCatHom.toFunctor =
    ((Discrete.functor (Discrete.mk ∘ ⇑(ConcreteCategory.hom f))).toCatHom ≫
        (Discrete.functor (Discrete.mk ∘ ⇑(ConcreteCategory.hom g))).toCatHom).toFunctor

Tactic:
simp only [Cat.of_α, toCatHom_toFunctor, Cat.Hom.comp_toFunctor]

Goal state after:
X✝ Y✝ Z✝ : Type u
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ Discrete.functor (Discrete.mk ∘ ⇑(ConcreteCategory.hom (f ≫ g))) =
    Discrete.functor (Discrete.mk ∘ ⇑(ConcreteCategory.hom f)) ⋙
      Discrete.functor (Discrete.mk ∘ ⇑(ConcreteCategory.hom g))
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Y Z : C
f : Y ⟶ Z
F : C ⥤ Type (max w v₁)
g : ((uliftCoyoneda.{w, v₁, u₁}.rightOp ⋙ coyoneda).obj Y).obj F
⊢ ((ConcreteCategory.hom
            (((uliftCoyoneda.{w, v₁, u₁}.rightOp ⋙ coyoneda).map f ≫
                  (NatIso.ofComponents (fun x ↦ (uliftCoyonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom).app
              F)).toFun
        g).down =
    ((ConcreteCategory.hom
            (((NatIso.ofComponents (fun x ↦ (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}).map
                    f).app
              F)).toFun
        g).down

Tactic:
simpa using (uliftCoyonedaEquiv_naturality _ _).symm

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F G : C ⥤ D
inst✝¹ : F.PreservesMonomorphisms
f : G ⟶ F
inst✝ : ∀ (X : C), Mono (f.app X)
X Y : C
π : X ⟶ Y
hπ : Mono π
⊢ Mono (G.map π ≫ f.app Y)

Tactic:
f.naturality π

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F G : C ⥤ D
inst✝¹ : F.PreservesMonomorphisms
f : G ⟶ F
inst✝ : ∀ (X : C), Mono (f.app X)
X Y : C
π : X ⟶ Y
hπ : Mono π
⊢ Mono (f.app X ≫ F.map π)
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: case term
J : Type w
C : Type u
inst✝ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → objs j ⟶ B
j : J
⊢ Option.casesOn (some j) B objs ⟶ Option.casesOn none B objs

Tactic:
exact arrows j

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

Tactic:
← assoc

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
D : Type u'
inst✝³ : Category.{v', u'} D
E : K ⥤ J
F : J ⥤ C
G : C ⥤ D
inst✝² : HasColimit F
inst✝¹ : HasColimit (E ⋙ F)
inst✝ : HasColimit (F ⋙ G)
h : HasColimit ((E ⋙ F) ⋙ G)
j : K
⊢ G.map (ι F (E.obj j)) = (ι ((E ⋙ F) ⋙ G) j ≫ pre (F ⋙ G) E) ≫ post F G
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: case init
J : Type w
C : Type u
inst✝ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
j : J
⊢ Option.casesOn none B objs ⟶ Option.casesOn (some j) B objs

Tactic:
exact arrows j

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

Goal state before:
pp: β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝² : Category.{v, u} C
ι : Type u_1
f : ι → Type u_2
g : (i : ι) → f i → C
inst✝¹ : ∀ (i : ι), HasProduct (g i)
inst✝ : HasProduct fun i ↦ ∏ᶜ g i
s : Fan fun p ↦ g p.fst p.snd
m : s.pt ⟶ ∏ᶜ fun i ↦ ∏ᶜ g i
w :
  ∀ (j : (i : ι) × f i),
    m ≫ (Fan.mk (∏ᶜ fun i ↦ ∏ᶜ g i) fun X ↦ Pi.π (fun i ↦ ∏ᶜ g i) X.fst ≫ Pi.π (g X.fst) X.snd).proj j = s.proj j
⊢ m = Pi.lift fun b ↦ Pi.lift fun c ↦ s.proj ⟨b, c⟩

Tactic:
aesop (add norm simp Sigma.forall)

Goal state after: