mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case zero
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
F : S →ₗ[R] M →ₗ[R] Q := ↑R ((Algebra.linearMap S (Module.End S (M →ₗ[R] Q))).flip g)
hF : ∀ (s : S) (m : M), (IsTensorProduct.lift h F) (s • f m) = s • g m
⊢ (IsTensorProduct.lift h F) 0 = r • (IsTensorProduct.lift h F) 0

Tactic:
map_zero,

Goal state after:
case zero
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
F : S →ₗ[R] M →ₗ[R] Q := ↑R ((Algebra.linearMap S (Module.End S (M →ₗ[R] Q))).flip g)
hF : ∀ (s : S) (m : M), (IsTensorProduct.lift h F) (s • f m) = s • g m
⊢ 0 = r • 0
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case refine_1
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
Q : Type u_3
inst✝¹ : AddCommMonoid Q
inst✝ : Module S Q
g₁ g₂ : N →ₗ[S] Q
e : ∀ (x : M), g₁ (f x) = g₂ (f x)
x : N
⊢ g₁ 0 = g₂ 0

Tactic:
map_zero,

Goal state after:
case refine_1
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
Q : Type u_3
inst✝¹ : AddCommMonoid Q
inst✝ : Module S Q
g₁ g₂ : N →ₗ[S] Q
e : ∀ (x : M), g₁ (f x) = g₂ (f x)
x : N
⊢ 0 = g₂ 0
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case refine_1
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
r : S
x : S ⊗[R] M
⊢ (IsTensorProduct.equiv h) 0 = r • (IsTensorProduct.equiv h) 0

Tactic:
map_zero,

Goal state after:
case refine_1
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
r : S
x : S ⊗[R] M
⊢ 0 = r • 0
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case refine_3
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
r : S
x✝ x y : S ⊗[R] M
hx : (IsTensorProduct.equiv h) (r • x) = r • (IsTensorProduct.equiv h) x
hy : (IsTensorProduct.equiv h) (r • y) = r • (IsTensorProduct.equiv h) y
⊢ (IsTensorProduct.equiv h) (r • (x + y)) = r • (IsTensorProduct.equiv h) (x + y)

Tactic:
rw [map_add, smul_add, map_add, smul_add, hx, hy]

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:
rw [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.List.Sym

Goal state before:
pp: α : Type u_1
xs : List α
h : xs.Nodup
⊢ xs.sym2.Nodup

Tactic:
by
  induction xs with
  | nil => simp only [List.sym2, nodup_nil]
  | cons x xs ih =>
    rw [List.sym2]
    specialize ih h.of_cons
    rw [nodup_cons] at h
    refine Nodup.append (Nodup.cons ?notmem (h.2.map ?inj)) ih ?disj
    case disj =>
      intro z hz hz'
      simp only [mem_cons, mem_map] at hz
      obtain ⟨_, (rfl | _), rfl⟩ := hz
        <;> simp [left_mem_of_mk_mem_sym2 hz'] at h
    case notmem =>
      intro h'
      simp only [h.1, mem_map, Sym2.eq_iff, true_and, or_self, exists_eq_right] at h'
    case inj =>
      intro a b
      simp only [Sym2.eq_iff, true_and]
      rintro (rfl | ⟨rfl, rfl⟩) <;> rfl

Goal state after:
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case refine_1
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)
hg : ↑R g ∘ₗ f = ↑ULift.moduleEquiv.symm ∘ₗ (mk R S M) 1
f' : S ⊗[R] M →ₗ[R] N := TensorProduct.lift (↑R ((Algebra.ofId S (Module.End S (M →ₗ[R] N))).toLinearMap.flip f))
s : S
x : S ⊗[R] M
⊢ f' (s • 0) = s • f' 0

Tactic:
map_zero,

Goal state after:
case refine_1
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)
hg : ↑R g ∘ₗ f = ↑ULift.moduleEquiv.symm ∘ₗ (mk R S M) 1
f' : S ⊗[R] M →ₗ[R] N := TensorProduct.lift (↑R ((Algebra.ofId S (Module.End S (M →ₗ[R] N))).toLinearMap.flip f))
s : S
x : S ⊗[R] M
⊢ f' (s • 0) = s • 0
Module: Mathlib.RingTheory.IsTensorProduct

Goal state before:
pp: case refine_1
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)
hg : ↑R g ∘ₗ f = ↑ULift.moduleEquiv.symm ∘ₗ (mk R S M) 1
f' : S ⊗[R] M →ₗ[R] N := TensorProduct.lift (↑R ((Algebra.ofId S (Module.End S (M →ₗ[R] N))).toLinearMap.flip f))
s : S
x : S ⊗[R] M
⊢ f' 0 = s • 0

Tactic:
map_zero,

Goal state after:
case refine_1
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)
hg : ↑R g ∘ₗ f = ↑ULift.moduleEquiv.symm ∘ₗ (mk R S M) 1
f' : S ⊗[R] M →ₗ[R] N := TensorProduct.lift (↑R ((Algebra.ofId S (Module.End S (M →ₗ[R] N))).toLinearMap.flip f))
s : S
x : S ⊗[R] M
⊢ 0 = s • 0
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
n : ℕ
k : Sym α n
s : Finset α
hk : k ∈ s.sym n
x : α
hx : x ∈ k
⊢ x ∈ s

Tactic:
simp only [Finset.mem_sym_iff] at hk

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
n : ℕ
k : Sym α n
s : Finset α
x : α
hx : x ∈ k
hk : ∀ a ∈ k, a ∈ s
⊢ x ∈ s
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
β : Type u_3
f : α → β
n : ℕ
xs x✝ : List α
⊢ List.sym 0 (map f x✝) = map (Sym.map f) (List.sym 0 x✝)

Tactic:
simp only [List.sym]; rfl

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid M
s : Finset ι
p : Sym2 ι → M
⊢ ∑ i ∈ s.sym2 with ¬i.IsDiag, p i = ∑ i ∈ s.offDiag with i.1 ≤ i.2, p s(i.1, i.2)

Tactic:
conv_rhs => rw [← Finset.sum_subtype_eq_sum_filter]

Goal state after:
ι : Type u_1
M : Type u_2
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid M
s : Finset ι
p : Sym2 ι → M
⊢ ∑ i ∈ s.sym2 with ¬i.IsDiag, p i = ∑ x ∈ Finset.subtype (fun i ↦ i.1 ≤ i.2) s.offDiag, p s((↑x).1, (↑x).2)
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case cons.cons.nil.cons.cons.nil.inl
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
head✝¹ head✝ : α
hx hy : [head✝¹, head✝].length = 2
h : (Vector.Perm.isSetoid α 2) ⟨[head✝¹, head✝], hx⟩ ⟨[head✝¹, head✝], hy⟩
⊢ Rel α (fromVector ⟨[head✝¹, head✝], hx⟩) (fromVector ⟨[head✝¹, head✝], hy⟩)

pp: case cons.cons.nil.cons.cons.nil.inr
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
head✝¹ head✝ : α
hx : [head✝¹, head✝].length = 2
hy : [head✝, head✝¹].length = 2
h : (Vector.Perm.isSetoid α 2) ⟨[head✝¹, head✝], hx⟩ ⟨[head✝, head✝¹], hy⟩
⊢ Rel α (fromVector ⟨[head✝¹, head✝], hx⟩) (fromVector ⟨[head✝, head✝¹], hy⟩)

Tactic:
· constructor

Goal state after:
case cons.cons.nil.cons.cons.nil.inr
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
head✝¹ head✝ : α
hx : [head✝¹, head✝].length = 2
hy : [head✝, head✝¹].length = 2
h : (Vector.Perm.isSetoid α 2) ⟨[head✝¹, head✝], hx⟩ ⟨[head✝, head✝¹], hy⟩
⊢ Rel α (fromVector ⟨[head✝¹, head✝], hx⟩) (fromVector ⟨[head✝, head✝¹], hy⟩)
Module: Mathlib.Combinatorics.Quiver.Push

Goal state before:
pp: case h_obj
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 : V), (of σ ⋙q lift σ φ τ h).obj X = φ.obj X

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)
⊢ ∀ (X Y : V) (f : X ⟶ Y), (of σ ⋙q lift σ φ τ h).map f = Eq.recOn ⋯ (Eq.recOn ⋯ (φ.map f))

Tactic:
· rintro X
    simp only [Prefunctor.comp_obj]
    apply Eq.symm
    exact h X

Goal state after:
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)
⊢ ∀ (X Y : V) (f : X ⟶ Y), (of σ ⋙q lift σ φ τ h).map f = Eq.recOn ⋯ (Eq.recOn ⋯ (φ.map f))
Module: Mathlib.CategoryTheory.EssentialImage

Goal state before:
pp: case refine_2
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
Y : D
⊢ F.essImage Y → ⊤.map F Y

Tactic:
· rintro ⟨X, ⟨e⟩⟩
    exact ⟨X, by simp, ⟨e⟩⟩

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

Goal state before:
pp: α : Type u_1
p : Discrete α → Prop
⊢ (∀ (a : Discrete α), p a) ↔ ∀ (a' : α), p { as := a' }

Tactic:
iff_iff_eq,

Goal state after:
α : Type u_1
p : Discrete α → Prop
⊢ (∀ (a : Discrete α), p a) = ∀ (a' : α), p { as := a' }
Module: Mathlib.CategoryTheory.Discrete.Basic

Goal state before:
pp: α : Type u_1
p : Discrete α → Prop
⊢ (∃ a, p a) ↔ ∃ a', p { as := a' }

Tactic:
iff_iff_eq,

Goal state after:
α : Type u_1
p : Discrete α → Prop
⊢ (∃ a, p a) = ∃ a', p { as := a' }
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F G : C ⥤ Dᵒᵖ
e : F ≅ G
X : C
⊢ (e.inv.app X).unop ≫ (e.hom.app X).unop = 𝟙 (Opposite.unop (F.obj X))

Tactic:
rw [← unop_comp, hom_inv_id_app, unop_id]

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 : Type u_1
inst✝² : Category.{v_1, u_1} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : G.IsEquivalence
inst✝ : (F ⋙ G).IsEquivalence
⊢ F.IsEquivalence

Tactic:
rw [isEquivalence_iff_of_iso (F.rightUnitor.symm ≪≫ isoWhiskerLeft F (G.asEquivalence.unitIso))]

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u_1
inst✝² : Category.{v_1, u_1} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : G.IsEquivalence
inst✝ : (F ⋙ G).IsEquivalence
⊢ (F ⋙ G.asEquivalence.functor ⋙ G.asEquivalence.inverse).IsEquivalence
Module: Mathlib.CategoryTheory.MorphismProperty.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y : C
f : X ⟶ Y
hf : P f
X' Y' : C
f' : X' ⟶ Y'
hX : X = X'
hY : Y = Y'
h : f' = eqToHom ⋯ ≫ f ≫ eqToHom hY
⊢ P f'

Tactic:
rw [← P.arrow_mk_mem_toSet_iff] at hf ⊢
  rwa [(Arrow.mk_eq_mk_iff f' f).2 ⟨hX.symm, hY.symm, h⟩]

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

Goal state before:
pp: case a
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
P : MorphismProperty D
inst✝ : P.RespectsIso
E : C ≌ D
X Y : D
f : X ⟶ Y
hf : P f
⊢ (P.inverseImage E.functor).inverseImage E.inverse f

Tactic:
exact (P.arrow_mk_iso_iff
      (((Functor.mapArrowFunctor _ _).mapIso E.counitIso).app (Arrow.mk f))).2 hf

Goal state after:
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.cones.RepresentableBy X
Y : C
f : Y ⟶ X
⊢ coneOfHom h f = (limitCone h).extend f

Tactic:
dsimp [coneOfHom, limitCone, Cone.extend]

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.cones.RepresentableBy X
Y : C
f : Y ⟶ X
⊢ { pt := Y, π := h.homEquiv f } = { pt := Y, π := (const J).map f ≫ h.homEquiv (𝟙 X) }
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 : C} {Y Y' : D} (f : F.obj X ⟶ Y) (g : Y ⟶ Y'), (e X Y') (f ≫ g) = (e X Y) f ≫ (rightAdjointOfEquiv e he).map g

Tactic:
intro X Y Y' g h

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 : C
Y Y' : D
g : F.obj X ⟶ Y
h : Y ⟶ Y'
⊢ (e X Y') (g ≫ h) = (e X Y) g ≫ (rightAdjointOfEquiv e he).map h
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝¹ : Bicategory B
a b c : B
f : a ⟶ b
g h : b ⟶ c
η : g ⟶ h
inst✝ : IsIso η
⊢ inv (f ◁ η) = f ◁ inv η

Tactic:
apply IsIso.inv_eq_of_hom_inv_id

Goal state after:
B : Type u
inst✝¹ : Bicategory B
a b c : B
f : a ⟶ b
g h : b ⟶ c
η : g ⟶ h
inst✝ : IsIso η
⊢ f ◁ η ≫ f ◁ inv η = 𝟙 (f ≫ g)
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝¹ : Bicategory B
a b c : B
f g : a ⟶ b
η : f ⟶ g
h : b ⟶ c
inst✝ : IsIso η
⊢ inv (η ▷ h) = inv η ▷ h

Tactic:
apply IsIso.inv_eq_of_hom_inv_id

Goal state after:
B : Type u
inst✝¹ : Bicategory B
a b c : B
f g : a ⟶ b
η : f ⟶ g
h : b ⟶ c
inst✝ : IsIso η
⊢ η ▷ h ≫ inv η ▷ h = 𝟙 (f ≫ h)
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝¹ : Bicategory B
a b c : B
f g : a ⟶ b
η : f ⟶ g
h : b ⟶ c
inst✝ : IsIso η
⊢ inv (η ▷ h) = inv η ▷ h

Tactic:
apply IsIso.inv_eq_of_hom_inv_id
  simp only [← comp_whiskerRight, id_whiskerRight, IsIso.hom_inv_id]

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 : yoneda.obj Y ≅ F
X X' : C
f : X ⟶ X'
g : X' ⟶ Y
⊢ (e.app (op X)).toEquiv (f ≫ g) = (ConcreteCategory.hom (F.map f.op)) ((e.app (op X')).toEquiv g)

Tactic:
apply e.hom.naturality_apply

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 : coyoneda.obj (op X✝) ≅ F
X X' : C
f : X ⟶ X'
g : X✝ ⟶ X
⊢ (e.app X').toEquiv (g ≫ f) = (ConcreteCategory.hom (F.map f)) ((e.app X).toEquiv g)

Tactic:
apply e.hom.naturality_apply

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
F : C ⥤ Type v₁
f : coyoneda.obj (op X) ⟶ F
g : X ⟶ Y
⊢ (ConcreteCategory.hom (f.app X ≫ F.map g)) (𝟙 X) = (ConcreteCategory.hom (f.app Y)) (g ≫ 𝟙 Y)

Tactic:
rw [← f.naturality]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
F : C ⥤ Type v₁
f : coyoneda.obj (op X) ⟶ F
g : X ⟶ Y
⊢ (ConcreteCategory.hom ((coyoneda.obj (op X)).map g ≫ f.app Y)) (𝟙 X) = (ConcreteCategory.hom (f.app Y)) (g ≫ 𝟙 Y)
Module: Mathlib.CategoryTheory.Category.Cat

Goal state before:
pp: X : Type u
⊢ (Discrete.functor (Discrete.mk ∘ ⇑(ConcreteCategory.hom (𝟙 X)))).toCatHom = 𝟙 (Cat.of (Discrete X))

Tactic:
ext
    simp only [Cat.of_α, toCatHom_toFunctor, Cat.Hom.id_toFunctor]
    fapply Functor.ext
    · simp
    · intro X Y f
      cases f
      apply ULift.ext
      cat_disch

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

Goal state before:
pp: 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✝
j j' : WidePullbackShape J
f : j ⟶ j'
⊢ (((Functor.const (WidePullbackShape J)).obj X).map f ≫
      match j' with
      | none => f✝
      | some j => π j) =
    (match j with
      | none => f✝
      | some j => π j) ≫
      F.map f

Tactic:
cases j <;> cases j' <;> 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)

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✝)

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
C : Type u
inst✝ : Category.{v, u} C
F : WidePushoutShape J ⥤ C
X : C
f✝ : F.obj none ⟶ X
ι : (j : J) → F.obj (some j) ⟶ X
w : ∀ (j : J), F.map (Hom.init j) ≫ ι j = f✝
j j' : WidePushoutShape J
f : j ⟶ j'
⊢ (F.map f ≫
      match j' with
      | none => f✝
      | some j => ι j) =
    (match j with
      | none => f✝
      | some j => ι j) ≫
      ((Functor.const (WidePushoutShape J)).obj X).map f

Tactic:
cases j <;> cases j' <;> cases f

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

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

case some.some.id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
F : WidePushoutShape J ⥤ C
X : C
f : F.obj none ⟶ X
ι : (j : J) → F.obj (some j) ⟶ X
w : ∀ (j : J), F.map (Hom.init j) ≫ ι j = f
val✝ : J
⊢ (F.map (Hom.id (some val✝)) ≫
      match some val✝ with
      | none => f
      | some j => ι j) =
    (match some val✝ with
      | none => f
      | some j => ι j) ≫
      ((Functor.const (WidePushoutShape J)).obj X).map (Hom.id (some val✝))
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) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
j : J
⊢ π arrows j ≫ arrows j = base arrows

Tactic:
apply limit.w (WidePullbackShape.wideCospan _ _ _) (WidePullbackShape.Hom.term 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
X : α → C
c : Cofan X
hc : IsColimit c
β : α → Type u_1
Y : (a : α) → β a → C
π : (a : α) → (b : β a) → Y a b ⟶ X a
hs : (a : α) → IsColimit (mk (X a) (π a))
⊢ IsColimit
    (mk c.pt fun x ↦
      match x with
      | ⟨a, b⟩ => π a b ≫ c.inj a)

Tactic:
by
  refine Cofan.IsColimit.mk _ ?_ ?_ ?_
  · exact fun t ↦ hc.desc (Cofan.mk _ fun a ↦ (hs a).desc (Cofan.mk t.pt (fun b ↦ t.inj ⟨a, b⟩)))
  · intro t ⟨a, b⟩
    simp only [mk_pt, cofan_mk_inj, Category.assoc]
    erw [hc.fac, (hs a).fac]
    rfl
  · intro t m h
    refine hc.hom_ext fun ⟨a⟩ ↦ (hs a).hom_ext fun ⟨b⟩ ↦ ?_
    erw [hc.fac, (hs a).fac]
    simpa using! h ⟨a, b⟩

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
X : Discrete α ⥤ C
inst✝ : HasCoproduct fun j ↦ X.obj { as := j }
s : Cocone X
m : (Sigma.cocone X).pt ⟶ s.pt
hm : ∀ (j : Discrete α), (Sigma.cocone X).ι.app j ≫ m = s.ι.app j
⊢ m = Sigma.desc fun j ↦ s.ι.app { as := j }

Tactic:
dsimp
    ext
    simp only [colimit.ι_desc, Cofan.mk_pt, Cofan.mk_ι_app]
    apply hm

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

Goal state before:
pp: case h_map
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
U V : Under Z
⊢ ∀ (f_1 : U ⟶ V), (map (f ≫ g)).map f_1 = eqToHom ⋯ ≫ (map g ⋙ map f).map f_1 ≫ eqToHom ⋯

Tactic:
k

Goal state after:
case h_map
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
U V : Under Z
k : U ⟶ V
⊢ (map (f ≫ g)).map k = eqToHom ⋯ ≫ (map g ⋙ map f).map k ≫ eqToHom ⋯