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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
N : Submodule R M
⊢ (lTensor Q N.mkQ).ker = (lTensor Q N.subtype).range

Tactic:
rw [← exact_iff]
  exact lTensor_exact Q (LinearMap.exact_subtype_mkQ N) (Submodule.mkQ_surjective N)

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

Goal state before:
pp: R : Type u_4
inst✝⁶ : CommRing R
A : Type u_6
C : Type u_8
D : Type u_9
inst✝⁵ : Ring A
inst✝⁴ : Ring C
inst✝³ : Ring D
inst✝² : Algebra R A
inst✝¹ : Algebra R C
inst✝ : Algebra R D
g : C →ₐ[R] D
hg : Function.Surjective ⇑g
this : Submodule.restrictScalars R (RingHom.ker (map (AlgHom.id R A) g)) = (LinearMap.lTensor A g.toLinearMap).ker
⊢ Submodule.restrictScalars R (RingHom.ker (map (AlgHom.id R A) g)) =
    Submodule.restrictScalars R (Ideal.map includeRight (RingHom.ker g))

Tactic:
rw [this, Ideal.map_includeRight_eq]

Goal state after:
R : Type u_4
inst✝⁶ : CommRing R
A : Type u_6
C : Type u_8
D : Type u_9
inst✝⁵ : Ring A
inst✝⁴ : Ring C
inst✝³ : Ring D
inst✝² : Algebra R A
inst✝¹ : Algebra R C
inst✝ : Algebra R D
g : C →ₐ[R] D
hg : Function.Surjective ⇑g
this : Submodule.restrictScalars R (RingHom.ker (map (AlgHom.id R A) g)) = (LinearMap.lTensor A g.toLinearMap).ker
⊢ (LinearMap.lTensor A g.toLinearMap).ker =
    (LinearMap.lTensor A (Submodule.restrictScalars R (RingHom.ker g)).subtype).range
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 : ι) → Monoid (G i)
inst✝² : Monoid C
inst✝¹ : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)
inst✝ : ∀ (i : ι), MonoidHomClass (H i) (G i) C
n : ℕ
i : ι
x✝ : G i
⊢ ⟦⟨i, x✝⟩⟧ ^ (n + 1) = ⟦⟨i, x✝⟩⟧ ^ n * ⟦⟨i, x✝⟩⟧

Tactic:
simp_rw [HPow.hPow, Pow.pow]
    simp_rw [map_def, pow_succ, mul_def]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Gaps

Goal state before:
pp: case neg
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j✝ : ℕ
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj✝ : j < k + 1
hj : ¬j = 0
this :
  a ≤ ((fun j ↦ ((F.intervalGapsWithin h a b ↑j).2, (F.intervalGapsWithin h a b ↑j.succ).1)) (j - 1)).1 ∧
    ((fun j ↦ ((F.intervalGapsWithin h a b ↑j).2, (F.intervalGapsWithin h a b ↑j.succ).1)) (j - 1)).1 ≤
        ((fun j ↦ ((F.intervalGapsWithin h a b ↑j).2, (F.intervalGapsWithin h a b ↑j.succ).1)) (j - 1)).2 ∧
      ((fun j ↦ ((F.intervalGapsWithin h a b ↑j).2, (F.intervalGapsWithin h a b ↑j.succ).1)) (j - 1)).2 ≤ b
⊢ a ≤ (F.intervalGapsWithin h a b ↑j).1

Tactic:
have hj₀ : j - 1 + 1 = j := by lia

Goal state after:
case neg
α : Type u_1
inst✝ : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j✝ : ℕ
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj✝ : j < k + 1
hj : ¬j = 0
this :
  a ≤ ((fun j ↦ ((F.intervalGapsWithin h a b ↑j).2, (F.intervalGapsWithin h a b ↑j.succ).1)) (j - 1)).1 ∧
    ((fun j ↦ ((F.intervalGapsWithin h a b ↑j).2, (F.intervalGapsWithin h a b ↑j.succ).1)) (j - 1)).1 ≤
        ((fun j ↦ ((F.intervalGapsWithin h a b ↑j).2, (F.intervalGapsWithin h a b ↑j.succ).1)) (j - 1)).2 ∧
      ((fun j ↦ ((F.intervalGapsWithin h a b ↑j).2, (F.intervalGapsWithin h a b ↑j.succ).1)) (j - 1)).2 ≤ b
hj₀ : j - 1 + 1 = j
⊢ a ≤ (F.intervalGapsWithin h a b ↑j).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:
← 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.Data.Int.Interval

Goal state before:
pp: a b : ℤ
h : a ≤ b
⊢ ↑(#(Ico a b)) = b - a

Tactic:
card_Ico,

Goal state after:
a b : ℤ
h : a ≤ b
⊢ ↑(b - a).toNat = b - a
Module: Mathlib.Data.List.Sym

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

Tactic:
rw [Sym2.eq_iff] at h

Goal state after:
case cons.inr.inl
α : Type u_1
a b x : α
xs : List α
ih : s(a, b) ∈ xs.sym2 → a ∈ xs
c : α
hc : c ∈ xs
h : a = x ∧ b = c ∨ a = c ∧ b = x
⊢ a = x ∨ a ∈ xs
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: case succ.refine_1
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n✝ n : ℕ
ih : ∀ {m : Sym α n}, m ∈ s.sym n ↔ ∀ a ∈ m, a ∈ s
a : α
ha : a ∈ s
b : α
m : Sym α n
he : m ∈ s.sym n
hb : b ∈ a ::ₛ m
⊢ b ∈ s

Tactic:
Sym.mem_cons

Goal state after:
case succ.refine_1
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
n✝ n : ℕ
ih : ∀ {m : Sym α n}, m ∈ s.sym n ↔ ∀ a ∈ m, a ∈ s
a : α
ha : a ∈ s
b : α
m : Sym α n
he : m ∈ s.sym n
hb : b = a ∨ b ∈ m
⊢ b ∈ s
Module: Mathlib.Data.List.Sym

Goal state before:
pp: case hl
α : Type u_1
n✝ : ℕ
xs ys : List α
h✝ : xs <+ ys
n : ℕ
l₁✝ l₂✝ : List α
a : α
h : l₁✝ <+ l₂✝
⊢ map (fun p ↦ a ::ₛ p) (List.sym n (a :: l₁✝)) <+ map (fun p ↦ a ::ₛ p) (List.sym n (a :: l₂✝))

pp: case hr
α : Type u_1
n✝ : ℕ
xs ys : List α
h✝ : xs <+ ys
n : ℕ
l₁✝ l₂✝ : List α
a : α
h : l₁✝ <+ l₂✝
⊢ List.sym (n + 1) l₁✝ <+ List.sym (n + 1) l₂✝

Tactic:
· exact ((cons_cons a h).sym n).map _

Goal state after:
case hr
α : Type u_1
n✝ : ℕ
xs ys : List α
h✝ : xs <+ ys
n : ℕ
l₁✝ l₂✝ : List α
a : α
h : l₁✝ <+ l₂✝
⊢ List.sym (n + 1) l₁✝ <+ List.sym (n + 1) l₂✝
Module: Mathlib.Data.List.Sym

Goal state before:
pp: case inl
α : Type u_1
n✝ : ℕ
xs✝ : List α
a : α
n : ℕ
x : α
xs : List α
z : Sym α n
hz : z ∈ List.sym n (x :: xs)
ha : a ∈ x ::ₛ z
⊢ a ∈ x :: xs

Tactic:
Sym.mem_cons

Goal state after:
case inl
α : Type u_1
n✝ : ℕ
xs✝ : List α
a : α
n : ℕ
x : α
xs : List α
z : Sym α n
hz : z ∈ List.sym n (x :: xs)
ha : a = x ∨ a ∈ z
⊢ a ∈ x :: xs
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Sym2 α → Sym2 β → Prop
i : Sym2 α
j : Sym2 β
hf : ∀ (a₁ a₂ : α) (b₁ b₂ : β), f s(a₁, a₂) s(b₁, b₂)
⊢ ∀ (a : α × α) (b : β × β), f (Quot.mk (Rel α) a) (Quot.mk (Rel β) b)

Tactic:
intro ⟨a₁, a₂⟩

Goal state after:
α : Type u_1
β : Type u_2
f : Sym2 α → Sym2 β → Prop
i : Sym2 α
j : Sym2 β
hf : ∀ (a₁ a₂ : α) (b₁ b₂ : β), f s(a₁, a₂) s(b₁, b₂)
a₁ a₂ : α
⊢ ∀ (b : β × β), f (Quot.mk (Rel α) (a₁, a₂)) (Quot.mk (Rel β) b)
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
⊢ map id = id

Tactic:
by
  ext ⟨⟨x, y⟩⟩
  rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
g : β → γ
f : α → β
⊢ map (g ∘ f) = map g ∘ map f

Tactic:
by
  ext ⟨⟨x, y⟩⟩
  rfl

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

Goal state before:
pp: α : Type u_1
a b c : α
⊢ a = b ∨ a = c → Sym2.Mem a s(b, c)

Tactic:
by
      rintro (rfl | rfl)
      · exact ⟨_, rfl⟩
      rw [eq_swap]
      exact ⟨_, rfl⟩

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

Goal state before:
pp: ι : Type u_1
M₀ : Type u_3
inst✝³ : CommMonoidWithZero M₀
inst✝² : NoZeroDivisors M₀
inst✝¹ : Nontrivial M₀
inst✝ : DecidableEq M₀
s : Finset ι
f : ι → WithTop M₀
i : ι
hi : i ∈ s
hi' : f i = ⊤
h : ∀ j ∈ s, f j ≠ 0
⊢ ∏ j ∈ s, f j = ⊤

Tactic:
← prod_erase_mul _ _ hi

Goal state after:
ι : Type u_1
M₀ : Type u_3
inst✝³ : CommMonoidWithZero M₀
inst✝² : NoZeroDivisors M₀
inst✝¹ : Nontrivial M₀
inst✝ : DecidableEq M₀
s : Finset ι
f : ι → WithTop M₀
i : ι
hi : i ∈ s
hi' : f i = ⊤
h : ∀ j ∈ s, f j ≠ 0
⊢ (∏ x ∈ s.erase i, f x) * f i = ⊤
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)
Q : Type (max v₂ u_5 u_4)
inst✝³ : AddCommMonoid Q
inst✝² : Module S Q
inst✝¹ : Module T Q
inst✝ : IsScalarTower S T Q
r : N →ₗ[S] Q
this : Module R Q := Module.restrictScalars R S Q
⊢ ∃! g', ↑S g' ∘ₗ h = r

Tactic:
have : IsScalarTower R S Q := .restrictScalars R S Q

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
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)
Q : Type (max v₂ u_5 u_4)
inst✝³ : AddCommMonoid Q
inst✝² : Module S Q
inst✝¹ : Module T Q
inst✝ : IsScalarTower S T Q
r : N →ₗ[S] Q
this✝ : Module R Q := Module.restrictScalars R S Q
this : IsScalarTower R S Q
⊢ ∃! g', ↑S g' ∘ₗ h = r
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
r r₁ r₂ : α → α → Prop
s : Set (Sym2 α)
⊢ (fun r ↦ fromRel ⋯) ((fun s ↦ ⟨ToRel s, ⋯⟩) s) = s

Tactic:
simp [fromRel_toRel]

Goal state after:
Module: Mathlib.CategoryTheory.Iso

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

Tactic:
rw [← symm_inv, inv_eq_inv α.symm β, eq_comm]
  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
G H : C ⥤ D
α : G ⟶ H
F : D ⥤ E
X Y : C
f : X ⟶ Y
⊢ F.map (G.map f) ≫ F.map (α.app Y) = F.map (α.app X) ≫ F.map (H.map f)

Tactic:
← F.map_comp,

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

Tactic:
← F.map_comp,

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
G H : C ⥤ D
α : G ⟶ H
F : D ⥤ E
X Y : C
f : X ⟶ Y
⊢ F.map (G.map f ≫ α.app Y) = F.map (α.app X ≫ H.map f)
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
inst✝ : IsIso α
⊢ F.whiskerLeft (inv α) ≫ F.whiskerLeft α = 𝟙 (F ⋙ H)

Tactic:
simp [← whiskerLeft_comp]

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

Goal state before:
pp: I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
X Y : (i : I) → C i
f : X ≅ Y
i : I
⊢ f.inv i ≫ f.hom i = 𝟙 (Y i)

Tactic:
by rw [← comp_apply, Iso.inv_hom_id, id_apply]

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

Goal state before:
pp: I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝¹ : (i : I) → Category.{v₁, u₁} (C i)
C' : Option J → Type u₁
inst✝ : (i : Option J) → Category.{v₁, u₁} (C' i)
⊢ (pi' fun i ↦
        match i with
        | none => Prod.fst (C' none) ((j : J) → C' (some j))
        | some i => Prod.snd (C' none) ((j : J) → C' (some j)) ⋙ eval (fun j ↦ C' (some j)) i) ⋙
      (eval C' none).prod' (pi' fun i ↦ eval C' (some i)) ≅
    𝟭 (C' none × ((j : J) → C' (some j)))

Tactic:
exact Iso.refl _

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

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
W : Set (MorphismProperty C)
Q : MorphismProperty C
h : ∀ W' ∈ W, W'.RespectsRight Q
X✝ Y✝ Z✝ : C
x✝¹ : Y✝ ⟶ Z✝
hi : Q x✝¹
x✝ : X✝ ⟶ Y✝
hf : InfSet.sInf W x✝
⊢ InfSet.sInf W (x✝ ≫ x✝¹)

Tactic:
rw [sInf_iff] at hf ⊢
    exact fun _ hW' ↦ (h _ hW').postcomp _ hi _ (hf _ hW')

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
L : A ⥤ T
R : B ⥤ T
X Y : Comma L R
e : X ⟶ Y
inst✝ : IsIso e
⊢ (inv e).left = inv e.left

Tactic:
by
  apply IsIso.eq_inv_of_hom_inv_id
  rw [← Comma.comp_left, IsIso.hom_inv_id, id_left]

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

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

Tactic:
intro Z W f

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z W : C
f : yoneda.obj Z ⟶ yoneda.obj W
⊢ yoneda.map ((ConcreteCategory.hom (f.app (op Z))) (𝟙 (unop (op Z)))) = f
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
⊢ ∀ {X Y : Cᵒᵖ} (f : coyoneda.obj X ⟶ coyoneda.obj Y),
    coyoneda.map (Quiver.Hom.op ((ConcreteCategory.hom (f.app (unop X))) (𝟙 (unop X)))) = f

Tactic:
intro Z W f

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z W : Cᵒᵖ
f : coyoneda.obj Z ⟶ coyoneda.obj W
⊢ coyoneda.map (Quiver.Hom.op ((ConcreteCategory.hom (f.app (unop Z))) (𝟙 (unop Z)))) = f
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
f : a ⟶ b
g : b ⟶ c
h k : c ⟶ d
η : h ≅ k
⊢ f ◁ g ◁ η.hom ≫ f ◁ g ◁ η.inv = 𝟙 (f ≫ g ≫ h)

Tactic:
simp [← whiskerLeft_comp]

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
f : a ⟶ b
g : b ⟶ c
h k : c ⟶ d
η : h ≅ k
⊢ f ◁ g ◁ η.inv ≫ f ◁ g ◁ η.hom = 𝟙 (f ≫ g ≫ k)

Tactic:
simp [← whiskerLeft_comp]

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
f : a ⟶ b
g h : b ⟶ c
η : g ≅ h
k : c ⟶ d
⊢ f ◁ η.hom ▷ k ≫ f ◁ η.inv ▷ k = 𝟙 (f ≫ g ≫ k)

Tactic:
simp [← whiskerLeft_comp]

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

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c d : B
f : a ⟶ b
g h : b ⟶ c
η : g ≅ h
k : c ⟶ d
⊢ f ◁ η.inv ▷ k ≫ f ◁ η.hom ▷ k = 𝟙 (f ≫ h ≫ k)

Tactic:
simp [← whiskerLeft_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ IsIso f ↔ ∀ (c : C), IsIso ((coyoneda.map f.op).app c)

Tactic:
by
  rw [isIso_iff_coyoneda_map_bijective]
  exact forall_congr' fun _ ↦ bijective_iff_isIso_ofHom _

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 : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X Y : C
f : X ⟶ Y
hf : Epi f
Z : D
g h : F.obj Y ⟶ Z
H : F.map f ≫ g = F.map f ≫ h
⊢ g = h

Tactic:
replace H := congr_arg (adj.homEquiv X Z) 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
adj : F ⊣ G
X Y : C
f : X ⟶ Y
hf : Epi f
Z : D
g h : F.obj Y ⟶ Z
H : (adj.homEquiv X Z) (F.map f ≫ g) = (adj.homEquiv X Z) (F.map f ≫ h)
⊢ g = h
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
inst✝ : F.Faithful
X Y : C
f : X ⟶ Y
x✝ : Mono (F.map f)
Z : C
g h : Z ⟶ X
hgh : g ≫ f = h ≫ f
⊢ F.map g ≫ F.map f = F.map h ≫ F.map f

Tactic:
← F.map_comp,

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
inst✝ : F.Faithful
X Y : C
f : X ⟶ Y
x✝ : Mono (F.map f)
Z : C
g h : Z ⟶ X
hgh : g ≫ f = h ≫ f
⊢ F.map (g ≫ f) = F.map h ≫ 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
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F : C ⥤ D
inst✝ : F.Faithful
X Y : C
f : X ⟶ Y
x✝ : Mono (F.map f)
Z : C
g h : Z ⟶ X
hgh : g ≫ f = h ≫ f
⊢ F.map g ≫ F.map f = F.map h ≫ F.map f

Tactic:
by rw [← F.map_comp, hgh, F.map_comp]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty.{w + 1} ⥤ C
F₂ : Discrete PEmpty.{w' + 1} ⥤ C
c₁ : Cocone F₁
hl : IsColimit c₁
c₂ : Cocone F₂
hi : c₁.pt ≅ c₂.pt
c : Cocone F₂
f : c₂.pt ⟶ c.pt
x✝ : ∀ (j : Discrete PEmpty.{w' + 1}), c₂.ι.app j ≫ f = c.ι.app j
⊢ f = hi.inv ≫ hl.desc { pt := c.pt, ι := { app := fun X_1 ↦ ⋯.elim, naturality := ⋯ } }

Tactic:
← hl.uniq _ (hi.hom ≫ f) _

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty.{w + 1} ⥤ C
F₂ : Discrete PEmpty.{w' + 1} ⥤ C
c₁ : Cocone F₁
hl : IsColimit c₁
c₂ : Cocone F₂
hi : c₁.pt ≅ c₂.pt
c : Cocone F₂
f : c₂.pt ⟶ c.pt
x✝ : ∀ (j : Discrete PEmpty.{w' + 1}), c₂.ι.app j ≫ f = c.ι.app j
⊢ f = hi.inv ≫ hi.hom ≫ f

C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
F₁ : Discrete PEmpty.{w + 1} ⥤ C
F₂ : Discrete PEmpty.{w' + 1} ⥤ C
c₁ : Cocone F₁
hl : IsColimit c₁
c₂ : Cocone F₂
hi : c₁.pt ≅ c₂.pt
c : Cocone F₂
f : c₂.pt ⟶ c.pt
x✝ : ∀ (j : Discrete PEmpty.{w' + 1}), c₂.ι.app j ≫ f = c.ι.app j
⊢ ∀ (j : Discrete PEmpty.{w + 1}),
    c₁.ι.app j ≫ hi.hom ≫ f = { pt := c.pt, ι := { app := fun X_1 ↦ ⋯.elim, naturality := ⋯ } }.ι.app j
Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u
inst✝ : Category.{v, u} J
X : J
tX : IsInitial X
F : J ⥤ C
j j' : J
k : j ⟶ j'
⊢ 𝟙 (F.obj X) ≫ F.map (tX.to j') = F.map (tX.to j) ≫ F.map k

Tactic:
← F.map_comp,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u
inst✝ : Category.{v, u} J
X : J
tX : IsInitial X
F : J ⥤ C
j j' : J
k : j ⟶ j'
⊢ 𝟙 (F.obj X) ≫ F.map (tX.to j') = F.map (tX.to j ≫ k)
Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u
inst✝ : Category.{v, u} J
X : J
tX : IsTerminal X
F : J ⥤ C
j j' : J
k : j ⟶ j'
⊢ F.map k ≫ F.map (tX.from j') = F.map (tX.from j) ≫ 𝟙 (F.obj X)

Tactic:
← F.map_comp,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u
inst✝ : Category.{v, u} J
X : J
tX : IsTerminal X
F : J ⥤ C
j j' : J
k : j ⟶ j'
⊢ F.map (k ≫ tX.from j') = F.map (tX.from j) ≫ 𝟙 (F.obj X)
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s : WidePullbackCone f
lift : (t : WidePullbackCone f) → t.pt ⟶ s.pt
facbase : ∀ (t : WidePullbackCone f), lift t ≫ s.base = t.base
facπ : ∀ (t : WidePullbackCone f) (i : ι), lift t ≫ s.π i = t.π i
uniq : ∀ (t : WidePullbackCone f) (m : t.pt ⟶ s.pt), m ≫ s.base = t.base → (∀ (i : ι), m ≫ s.π i = t.π i) → m = lift t
t : Cone (WidePullbackShape.wideCospan X Y f)
j : WidePullbackShape ι
⊢ lift t ≫ s.π.app j = t.π.app j

Tactic:
cases j
    · exact facbase t
    · exact facπ t _

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u₂
inst✝⁴ : Category.{w, u₂} D
F : C ⥤ D
A A' B B' : C
inst✝³ : HasBinaryProduct A B
inst✝² : HasBinaryProduct A' B'
inst✝¹ : HasBinaryProduct (F.obj A) (F.obj B)
inst✝ : HasBinaryProduct (F.obj A') (F.obj B')
f : A ⟶ A'
g : B ⟶ B'
⊢ F.map (prod.map f g) ≫ prod.lift (F.map prod.fst) (F.map prod.snd) =
    prod.lift (F.map prod.fst ≫ F.map f) (F.map prod.snd ≫ F.map g)

Tactic:
← F.map_comp,

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u₂
inst✝⁴ : Category.{w, u₂} D
F : C ⥤ D
A A' B B' : C
inst✝³ : HasBinaryProduct A B
inst✝² : HasBinaryProduct A' B'
inst✝¹ : HasBinaryProduct (F.obj A) (F.obj B)
inst✝ : HasBinaryProduct (F.obj A') (F.obj B')
f : A ⟶ A'
g : B ⟶ B'
⊢ F.map (prod.map f g) ≫ prod.lift (F.map prod.fst) (F.map prod.snd) =
    prod.lift (F.map (prod.fst ≫ f)) (F.map prod.snd ≫ F.map g)
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u₂
inst✝⁴ : Category.{w, u₂} D
F : C ⥤ D
A A' B B' : C
inst✝³ : HasBinaryProduct A B
inst✝² : HasBinaryProduct A' B'
inst✝¹ : HasBinaryProduct (F.obj A) (F.obj B)
inst✝ : HasBinaryProduct (F.obj A') (F.obj B')
f : A ⟶ A'
g : B ⟶ B'
⊢ F.map (prod.map f g) ≫ prod.lift (F.map prod.fst) (F.map prod.snd) =
    prod.lift (F.map (prod.fst ≫ f)) (F.map prod.snd ≫ F.map g)

Tactic:
← F.map_comp,

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u₂
inst✝⁴ : Category.{w, u₂} D
F : C ⥤ D
A A' B B' : C
inst✝³ : HasBinaryProduct A B
inst✝² : HasBinaryProduct A' B'
inst✝¹ : HasBinaryProduct (F.obj A) (F.obj B)
inst✝ : HasBinaryProduct (F.obj A') (F.obj B')
f : A ⟶ A'
g : B ⟶ B'
⊢ F.map (prod.map f g) ≫ prod.lift (F.map prod.fst) (F.map prod.snd) =
    prod.lift (F.map (prod.fst ≫ f)) (F.map (prod.snd ≫ g))
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

Goal state before:
pp: case none
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (cospan f g ⋙ F).obj none ≅ (cospan (F.map f) (F.map g)).obj none

Tactic:
exact Iso.refl _

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

Goal state before:
pp: case some.left
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (cospan f g ⋙ F).obj (some WalkingPair.left) ≅ (cospan (F.map f) (F.map g)).obj (some WalkingPair.left)

Tactic:
exact Iso.refl _

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

Goal state before:
pp: case some.right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ (cospan f g ⋙ F).obj (some WalkingPair.right) ≅ (cospan (F.map f) (F.map g)).obj (some WalkingPair.right)

Tactic:
exact Iso.refl _

Goal state after: