mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝¹⁰ : Preorder ι
G : ι → Type u_3
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✝⁸ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁷ : IsDirectedOrder ι
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : ι) → NonUnitalNonAssocSemiring (G i)
inst✝⁴ : (i : ι) → DistribMulAction R (G i)
inst✝³ : ∀ (i j : ι) (h : i ≤ j), NonUnitalAlgHomClass (T h) R (G i) (G j)
inst✝² : Nonempty ι
P : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring P
inst✝ : DistribMulAction R P
g₁ g₂ : DirectLimit G f →ₙₐ[R] P
h : ∀ (i : ι), g₁.comp (of G f i) = g₂.comp (of G f i)
x : DirectLimit G f
⊢ g₁ x = g₂ x

Tactic:
induction x using DirectLimit.induction with | _ i x
   =>  _ 

Goal state after:
case ih
R : Type u_1
ι : Type u_2
inst✝¹⁰ : Preorder ι
G : ι → Type u_3
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✝⁸ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁷ : IsDirectedOrder ι
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : ι) → NonUnitalNonAssocSemiring (G i)
inst✝⁴ : (i : ι) → DistribMulAction R (G i)
inst✝³ : ∀ (i j : ι) (h : i ≤ j), NonUnitalAlgHomClass (T h) R (G i) (G j)
inst✝² : Nonempty ι
P : Type u_7
inst✝¹ : NonUnitalNonAssocSemiring P
inst✝ : DistribMulAction R P
g₁ g₂ : DirectLimit G f →ₙₐ[R] P
h : ∀ (i : ι), g₁.comp (of G f i) = g₂.comp (of G f i)
i : ι
x : G i
⊢ g₁ ⟦⟨i, x⟩⟧ = g₂ ⟦⟨i, x⟩⟧
Module: Mathlib.Algebra.BigOperators.Module

Goal state before:
pp: case neg
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
n : ℕ
hn : ¬n = 0
⊢ f (n - 1) • ∑ i ∈ range n, g i - 0 - ∑ i ∈ Ico 0 (n - 1), (f (i + 1) - f i) • ∑ i ∈ range (i + 1), g i =
    f (n - 1) • ∑ x ∈ Ico 0 n, g x - ∑ x ∈ Ico 0 (n - 1), (f (x + 1) - f x) • ∑ x ∈ Ico 0 (x + 1), g x

Tactic:
sub_zero

Goal state after:
case neg
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
n : ℕ
hn : ¬n = 0
⊢ f (n - 1) • ∑ i ∈ range n, g i - ∑ i ∈ Ico 0 (n - 1), (f (i + 1) - f i) • ∑ i ∈ range (i + 1), g i =
    f (n - 1) • ∑ x ∈ Ico 0 n, g x - ∑ x ∈ Ico 0 (n - 1), (f (x + 1) - f x) • ∑ x ∈ Ico 0 (x + 1), g x
Module: Mathlib.Data.List.Sym

Goal state before:
pp: α : Type u_1
x : α
xs : List α
ih : xs.sym2.Nodup
h : x ∉ xs ∧ xs.Nodup
a b : α
⊢ (fun y ↦ s(x, y)) a = (fun y ↦ s(x, y)) b → a = b

Tactic:
simp only [Sym2.eq_iff, true_and]

Goal state after:
α : Type u_1
x : α
xs : List α
ih : xs.sym2.Nodup
h : x ∉ xs ∧ xs.Nodup
a b : α
⊢ a = b ∨ x = b ∧ a = x → a = b
Module: Mathlib.Data.List.Sym

Goal state before:
pp: case cons
α : Type u_1
x x' : α
xs : List α
ih : x ∈ xs → map (fun y ↦ s(x, y)) xs <+ xs.sym2
h : x ∈ x' :: xs
⊢ s(x, x') :: map (fun y ↦ s(x, y)) xs <+ s(x', x') :: (map (fun y ↦ s(x', y)) xs ++ xs.sym2)

Tactic:
cases h with

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

Goal state before:
pp: case h.h
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
⊢ s(a, b).inf = s(c, d).inf ∧ s(a, b).sup = s(c, d).sup ↔ s(a, b) = s(c, d)

Tactic:
obtain hab | hba := le_total a b <;> obtain hcd | hdc := le_total c d

Goal state after:
case h.h.inl.inl
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
⊢ s(a, b).inf = s(c, d).inf ∧ s(a, b).sup = s(c, d).sup ↔ s(a, b) = s(c, d)

case h.h.inl.inr
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hab : a ≤ b
hdc : d ≤ c
⊢ s(a, b).inf = s(c, d).inf ∧ s(a, b).sup = s(c, d).sup ↔ s(a, b) = s(c, d)

case h.h.inr.inl
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hba : b ≤ a
hcd : c ≤ d
⊢ s(a, b).inf = s(c, d).inf ∧ s(a, b).sup = s(c, d).sup ↔ s(a, b) = s(c, d)

case h.h.inr.inr
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hba : b ≤ a
hdc : d ≤ c
⊢ s(a, b).inf = s(c, d).inf ∧ s(a, b).sup = s(c, d).sup ↔ s(a, b) = s(c, d)
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
⊢ ∀ ⦃a b : α × α⦄, Rel α a b → Rel β (Prod.map f f a) (Prod.map f f b)

Tactic:
intro _ _ h; cases h <;> constructor

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

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
f g : α → β
s : Sym2 α
h : ∀ x ∈ s, f x = g x
y : β
⊢ (∃ a ∈ s, f a = y) → ∃ a ∈ s, g a = y

Tactic:
rintro ⟨w, hw, rfl⟩
      exact ⟨w, hw, by simp [hw, h]⟩

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

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
f g : α → β
s : Sym2 α
h : ∀ x ∈ s, f x = g x
y : β
⊢ (∃ a ∈ s, g a = y) → ∃ a ∈ s, f a = y

Tactic:
rintro ⟨w, hw, rfl⟩
      exact ⟨w, hw, by simp [hw, h]⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
P : α → Prop
f : (a : α) → P a → β
s : Sym2 α
g : (p : α × α) → (∀ a ∈ s(p.1, p.2), P a) → Sym2 β := fun p H ↦ s(f p.1 ⋯, f p.2 ⋯)
p q : α × α
hpq✝ : Rel α p q
hpq : p = q ∨ p = q.swap
Hq : ∀ a ∈ Quot.mk (Rel α) q, P a
Hp : ∀ a ∈ s(p.1, p.2), P a
⊢ ∀ {s₂ : Sym2 α} {e : s(p.1, p.2) = s₂} {H : ∀ a ∈ s₂, P a},
    Eq.ndrec (motive := fun s ↦ (∀ a ∈ s, P a) → Sym2 β) (g p) e H = g p Hp

Tactic:
rintro s₂ rfl _

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
P : α → Prop
f : (a : α) → P a → β
s : Sym2 α
g : (p : α × α) → (∀ a ∈ s(p.1, p.2), P a) → Sym2 β := fun p H ↦ s(f p.1 ⋯, f p.2 ⋯)
p q : α × α
hpq✝ : Rel α p q
hpq : p = q ∨ p = q.swap
Hq : ∀ a ∈ Quot.mk (Rel α) q, P a
Hp H✝ : ∀ a ∈ s(p.1, p.2), P a
⊢ Eq.ndrec (motive := fun s ↦ (∀ a ∈ s, P a) → Sym2 β) (g p) ⋯ H✝ = g p Hp
Module: Mathlib.Data.Opposite

Goal state before:
pp: α : Sort u
X : Type v
inst✝ : Small.{u, v} X
⊢ Small.{u, v} Xᵒᵖ

Tactic:
obtain ⟨S, ⟨e⟩⟩ := Small.equiv_small (α := X)
  exact ⟨S, ⟨equivToOpposite.symm.trans e⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Iso

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

Tactic:
← w

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : X ⟶ Z
inst✝ : IsIso f
hh : IsIso (f ≫ g)
w : f ≫ g = h
⊢ IsIso g
Module: Mathlib.CategoryTheory.Functor.FullyFaithful

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

Tactic:
by simp [← NatIso.naturality_1 α]

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
F✝ F' : C ⥤ D
G✝ : D ⥤ E
F : C ⥤ E
G : D ⥤ E
inst✝ : G.Faithful
obj : C → D
h_obj : ∀ (X : C), G.obj (obj X) = F.obj X
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, G.map (map f) ≍ F.map f
X : C
⊢ map (𝟙 X) = 𝟙 (obj X)

Tactic:
apply G.map_injective

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✝ F' : C ⥤ D
G✝ : D ⥤ E
F : C ⥤ E
G : D ⥤ E
inst✝ : G.Faithful
obj : C → D
h_obj : ∀ (X : C), G.obj (obj X) = F.obj X
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, G.map (map f) ≍ F.map f
X : C
⊢ G.map (map (𝟙 X)) = G.map (𝟙 (obj X))
Module: Mathlib.Logic.Lemmas

Goal state before:
pp: case refine_1
f : Prop → Prop
x✝ : ∃ p, f p
p : Prop
h : f p
H : p
⊢ f True

Tactic:
convert! h

Goal state after:
f : Prop → Prop
x✝ : ∃ p, f p
p : Prop
h : f p
H : p
⊢ True ↔ p
Module: Mathlib.Logic.Lemmas

Goal state before:
pp: case refine_2
f : Prop → Prop
x✝ : ∃ p, f p
p : Prop
h : f p
H : ¬p
⊢ f False

Tactic:
convert! h

Goal state after:
f : Prop → Prop
x✝ : ∃ p, f p
p : Prop
h : f p
H : ¬p
⊢ False ↔ p
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: V : Type u
inst✝ : Quiver V
a b c x✝ : V
p : Path a b
q : Path b c
b✝ : V
r : Path c b✝
a✝ : b✝ ⟶ x✝
⊢ ((p.comp q).comp r).cons a✝ = (p.comp (q.comp r)).cons a✝

Tactic:
comp_assoc p q r

Goal state after:
V : Type u
inst✝ : Quiver V
a b c x✝ : V
p : Path a b
q : Path b c
b✝ : V
r : Path c b✝
a✝ : b✝ ⟶ x✝
⊢ (p.comp (q.comp r)).cons a✝ = (p.comp (q.comp r)).cons a✝
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: case nil.cons
V : Type u
inst✝ : Quiver V
a b c : V
p₁ p₂ : Path a b
b✝ : V
q₂ : Path b b✝
f₂ : b✝ ⟶ b
hq : nil.length = (q₂.cons f₂).length
h : p₁.comp nil = p₂.comp (q₂.cons f₂)
⊢ p₁ = p₂ ∧ nil = q₂.cons f₂

Tactic:
cases hq

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

Goal state before:
pp: case cons.nil
V : Type u
inst✝ : Quiver V
a b c : V
p₁ p₂ : Path a b
b✝ : V
q₁ : Path b b✝
ih : ∀ {q₂ : Path b b✝}, q₁.length = q₂.length → p₁.comp q₁ = p₂.comp q₂ → p₁ = p₂ ∧ q₁ = q₂
f₁ : b✝ ⟶ b
hq : (q₁.cons f₁).length = nil.length
h : p₁.comp (q₁.cons f₁) = p₂.comp nil
⊢ p₁ = p₂ ∧ q₁.cons f₁ = nil

Tactic:
cases hq

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
W X Y Z : C
f : W ⟶ X
g : Y ⟶ Z
h : W = Y
h' : X = Z
⊢ f = eqToHom h ≫ g ≫ eqToHom ⋯ ↔ f ≍ g

Tactic:
cases h
  cases h'
  simp

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
p : X = Y
q : Y ⟶ Z
⊢ cast ⋯ q = eqToHom p ≫ q

Tactic:
cases p
  simp

Goal state after:
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
p : X = Y
q : Y ⟶ Z
⊢ ⋯.mpr q = eqToHom p ≫ q

Tactic:
cases p
  simp

Goal state after:
Module: Mathlib.CategoryTheory.CommSq

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
W X X' Y Z Z' : C
f : W ⟶ X
f' : X ⟶ X'
g : W ⟶ Y
h : X ⟶ Z
h' : X' ⟶ Z'
i : Y ⟶ Z
i' : Z ⟶ Z'
hsq₁ : CommSq f g h i
hsq₂ : CommSq f' h h' i'
⊢ (f ≫ f') ≫ h' = g ≫ i ≫ i'

Tactic:
rw [← Category.assoc, Category.assoc, ← hsq₁.w, hsq₂.w, Category.assoc]

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
H : X = Y
⊢ (eqToHom H).left = eqToHom ⋯

Tactic:
by
  cases H
  rfl

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
H : X = Y
⊢ (eqToHom H).right = eqToHom ⋯

Tactic:
by
  cases H
  rfl

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
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
L' : A' ⥤ T'
R' : B' ⥤ T'
F₁ : A ⥤ A'
F₂ : B ⥤ B'
F : T ⥤ T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
inst✝⁴ : F.Faithful
inst✝³ : F₁.Full
inst✝² : F₂.Full
inst✝¹ : IsIso α
inst✝ : IsIso β
X Y : Comma L R
φ : (map α β).obj X ⟶ (map α β).obj Y
⊢ F.map (L.map (F₁.preimage φ.left) ≫ Y.hom) ≫ β.app Y.right =
    F.map (X.hom ≫ R.map (F₂.preimage φ.right)) ≫ β.app Y.right

Tactic:
← cancel_epi (α.app _),

Goal state after:
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
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
L' : A' ⥤ T'
R' : B' ⥤ T'
F₁ : A ⥤ A'
F₂ : B ⥤ B'
F : T ⥤ T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
inst✝⁴ : F.Faithful
inst✝³ : F₁.Full
inst✝² : F₂.Full
inst✝¹ : IsIso α
inst✝ : IsIso β
X Y : Comma L R
φ : (map α β).obj X ⟶ (map α β).obj Y
⊢ α.app X.left ≫ F.map (L.map (F₁.preimage φ.left) ≫ Y.hom) ≫ β.app Y.right =
    α.app X.left ≫ F.map (X.hom ≫ R.map (F₂.preimage φ.right)) ≫ β.app Y.right
Module: Mathlib.CategoryTheory.Conj

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
α : X ≅ Y
f : End X
⊢ (refl X).conj f = f

Tactic:
refl_conj

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
α : X ≅ Y
f : End X
⊢ f = f
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✝ t : Cone F
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
G : C ⥤ D
inst✝ : G.Faithful
ht : IsLimit (G.mapCone t)
lift : (s : Cone F) → s.pt ⟶ t.pt
h : ∀ (s : Cone F), G.map (lift s) = ht.lift (G.mapCone s)
s : Cone F
j : J
⊢ lift s ≫ t.π.app j = s.π.app j

Tactic:
apply G.map_injective

Goal state after:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u₃
inst✝² : Category.{v₃, u₃} C
F : J ⥤ C
t✝ t : Cone F
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
G : C ⥤ D
inst✝ : G.Faithful
ht : IsLimit (G.mapCone t)
lift : (s : Cone F) → s.pt ⟶ t.pt
h : ∀ (s : Cone F), G.map (lift s) = ht.lift (G.mapCone s)
s : Cone F
j : J
⊢ G.map (lift s ≫ t.π.app j) = G.map (s.π.app j)
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✝ t : Cone F
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
G : C ⥤ D
inst✝ : G.Faithful
ht : IsLimit (G.mapCone t)
lift : (s : Cone F) → s.pt ⟶ t.pt
h : ∀ (s : Cone F), G.map (lift s) = ht.lift (G.mapCone s)
s : Cone F
m : s.pt ⟶ t.pt
w : ∀ (j : J), m ≫ t.π.app j = s.π.app j
⊢ m = lift s

Tactic:
apply G.map_injective

Goal state after:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u₃
inst✝² : Category.{v₃, u₃} C
F : J ⥤ C
t✝ t : Cone F
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
G : C ⥤ D
inst✝ : G.Faithful
ht : IsLimit (G.mapCone t)
lift : (s : Cone F) → s.pt ⟶ t.pt
h : ∀ (s : Cone F), G.map (lift s) = ht.lift (G.mapCone s)
s : Cone F
m : s.pt ⟶ t.pt
w : ∀ (j : J), m ≫ t.π.app j = s.π.app j
⊢ G.map m = G.map (lift s)
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ yonedaEquiv (yoneda.map f) = f

Tactic:
rw [yonedaEquiv_apply]
  simp

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
F : Cᵒᵖ ⥤ Type v₁
t : F.obj X
⊢ yonedaEquiv.symm ((ConcreteCategory.hom (F.map f)) t) = yoneda.map f.unop ≫ yonedaEquiv.symm t

Tactic:
by
  obtain ⟨u, rfl⟩ := yonedaEquiv.surjective t
  rw [yonedaEquiv_naturality', Equiv.symm_apply_apply, Equiv.symm_apply_apply]

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : Cᵒᵖ
F : C ⥤ Type (max w v₁)
τ : uliftCoyoneda.{w, v₁, u₁}.obj X ⟶ F
⊢ (fun x ↦ { app := fun Y ↦ ↾fun y ↦ (ConcreteCategory.hom (F.map y.down)) x, naturality := ⋯ })
      ((fun τ ↦ (ConcreteCategory.hom (τ.app (unop X))) { down := 𝟙 (unop X) }) τ) =
    τ

Tactic:
by
    ext Y ⟨x⟩
    simp [← comp_apply, ← τ.naturality]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝ : StrongEpi (f ≫ g)
X Y : C
z : X ⟶ Y
x✝ : Mono z
u : Q ⟶ X
v : R ⟶ Y
⊢ ∀ (sq : CommSq u g z v), sq.HasLift

Tactic:
sq

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst✝ : StrongEpi (f ≫ g)
X Y : C
z : X ⟶ Y
x✝ : Mono z
u : Q ⟶ X
v : R ⟶ Y
sq : CommSq u g z v
⊢ sq.HasLift
Module: Mathlib.CategoryTheory.LiftingProperties.Adjunction

Goal state before:
pp: case mp
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
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
a✝ : HasLiftingProperty (G.map i) p
f : A ⟶ F.obj X
g : B ⟶ F.obj Y
⊢ ∀ (sq : CommSq f i (F.map p) g), sq.HasLift

Tactic:
sq

Goal state after:
case mp
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
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
a✝ : HasLiftingProperty (G.map i) p
f : A ⟶ F.obj X
g : B ⟶ F.obj Y
sq : CommSq f i (F.map p) g
⊢ sq.HasLift
Module: Mathlib.CategoryTheory.LiftingProperties.Adjunction

Goal state before:
pp: case mpr
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
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
a✝ : HasLiftingProperty i (F.map p)
f : G.obj A ⟶ X
g : G.obj B ⟶ Y
⊢ ∀ (sq : CommSq f (G.map i) p g), sq.HasLift

Tactic:
sq

Goal state after:
case mpr
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
adj : G ⊣ F
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
a✝ : HasLiftingProperty i (F.map p)
f : G.obj A ⟶ X
g : G.obj B ⟶ Y
sq : CommSq f (G.map i) p g
⊢ sq.HasLift
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
F : J ⥤ C
t : Cone F
P : IsLimit t
s : Cocone F.op
m : t.op.pt ⟶ s.pt
w : ∀ (j : Jᵒᵖ), t.op.ι.app j ≫ m = s.ι.app j
j : J
⊢ m.unop ≫ t.π.app j = (s.ι.app (Opposite.op j)).unop

Tactic:
← w

Goal state after:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cone F
P : IsLimit t
s : Cocone F.op
m : t.op.pt ⟶ s.pt
w : ∀ (j : Jᵒᵖ), t.op.ι.app j ≫ m = s.ι.app j
j : J
⊢ m.unop ≫ t.π.app j = (t.op.ι.app (Opposite.op j) ≫ m).unop
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
F : J ⥤ C
t : Cocone F
P : IsColimit t
s : Cone F.op
m : s.pt ⟶ t.op.pt
w : ∀ (j : Jᵒᵖ), m ≫ t.op.π.app j = s.π.app j
j : J
⊢ t.ι.app j ≫ m.unop = (s.π.app (Opposite.op j)).unop

Tactic:
← w

Goal state after:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cocone F
P : IsColimit t
s : Cone F.op
m : s.pt ⟶ t.op.pt
w : ∀ (j : Jᵒᵖ), m ≫ t.op.π.app j = s.π.app j
j : J
⊢ t.ι.app j ≫ m.unop = (m ≫ t.op.π.app (Opposite.op j)).unop
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
F : J ⥤ C
t : Cone F.op
P : IsLimit t
s : Cocone F
m : t.unop.pt ⟶ s.pt
w : ∀ (j : J), t.unop.ι.app j ≫ m = s.ι.app j
j : Jᵒᵖ
⊢ m.op ≫ t.π.app j = (s.ι.app (Opposite.unop j)).op

Tactic:
← w

Goal state after:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cone F.op
P : IsLimit t
s : Cocone F
m : t.unop.pt ⟶ s.pt
w : ∀ (j : J), t.unop.ι.app j ≫ m = s.ι.app j
j : Jᵒᵖ
⊢ m.op ≫ t.π.app j = (t.unop.ι.app (Opposite.unop j) ≫ m).op
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
F : J ⥤ C
t : Cocone F.op
P : IsColimit t
s : Cone F
m : s.pt ⟶ t.unop.pt
w : ∀ (j : J), m ≫ t.unop.π.app j = s.π.app j
j : Jᵒᵖ
⊢ t.ι.app j ≫ m.op = (s.π.app (Opposite.unop j)).op

Tactic:
← w

Goal state after:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cocone F.op
P : IsColimit t
s : Cone F
m : s.pt ⟶ t.unop.pt
w : ∀ (j : J), m ≫ t.unop.π.app j = s.π.app j
j : Jᵒᵖ
⊢ t.ι.app j ≫ m.op = (m ≫ t.unop.π.app (Opposite.unop j)).op
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W✝ X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
W : C
fst : W ⟶ X
snd : W ⟶ Y
eq : fst ≫ f = snd ≫ g
⊢ ∀ ⦃X_1 Y_1 : WalkingCospan⦄ (f_1 : X_1 ⟶ Y_1),
    (((Functor.const WalkingCospan).obj W).map f_1 ≫
        Option.casesOn Y_1 (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) =
      (Option.casesOn X_1 (fst ≫ f) fun j' ↦ WalkingPair.casesOn j' fst snd) ≫ (cospan f g).map f_1

Tactic:
by rintro (⟨⟩ | ⟨⟨⟩⟩) (⟨⟩ | ⟨⟨⟩⟩) j <;> cases j <;> simp [eq]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Z
g : Y ⟶ Z
f : X ⟶ Y
inst✝ : Mono f
s : PullbackCone f f
⊢ s.fst ≫ 𝟙 X = s.snd

Tactic:
rw [← cancel_mono f, Category.comp_id, s.condition]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
f : X ⟶ W
g : Y ⟶ W
i : W ⟶ Z
inst✝ : Mono i
s✝ : PullbackCone f g
H : IsLimit s✝
s : PullbackCone (f ≫ i) (g ≫ i)
⊢ (s.fst ≫ f) ≫ i = (s.snd ≫ g) ≫ i

Tactic:
simpa using s.condition

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Y
g✝ : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : W ⟶ X
inst✝ : Epi h
s✝ : PushoutCocone f g
H : IsColimit s✝
s : PushoutCocone (h ≫ f) (h ≫ g)
⊢ h ≫ f ≫ s.inl = h ≫ g ≫ s.inr

Tactic:
simpa using s.condition

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Y
g✝ : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : W ⟶ X
inst✝ : Epi h
s✝ : PushoutCocone f g
H : IsColimit s✝
s : PushoutCocone (h ≫ f) (h ≫ g)
⊢ { l //
    (mk s✝.inl s✝.inr ⋯).inl ≫ l = s.inl ∧
      (mk s✝.inl s✝.inr ⋯).inr ≫ l = s.inr ∧
        ∀ {m : (mk s✝.inl s✝.inr ⋯).pt ⟶ s.pt},
          (mk s✝.inl s✝.inr ⋯).inl ≫ m = s.inl → (mk s✝.inl s✝.inr ⋯).inr ≫ m = s.inr → m = l }

Tactic:
rcases PushoutCocone.IsColimit.desc' H s.inl s.inr
      ((cancel_epi h).mp (by simpa using s.condition)) with
    ⟨l, h₁, h₂⟩

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Y
g✝ : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : W ⟶ X
inst✝ : Epi h
s✝ : PushoutCocone f g
H : IsColimit s✝
s : PushoutCocone (h ≫ f) (h ≫ g)
l : s✝.pt ⟶ s.pt
h₁ : s✝.inl ≫ l = s.inl
h₂ : s✝.inr ≫ l = s.inr
⊢ { l //
    (mk s✝.inl s✝.inr ⋯).inl ≫ l = s.inl ∧
      (mk s✝.inl s✝.inr ⋯).inr ≫ l = s.inr ∧
        ∀ {m : (mk s✝.inl s✝.inr ⋯).pt ⟶ s.pt},
          (mk s✝.inl s✝.inr ⋯).inl ≫ m = s.inl → (mk s✝.inl s✝.inr ⋯).inr ≫ m = s.inr → m = l }
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
h✝ : f = g
s : Fork f g
m : s.pt ⟶ (idFork h✝).pt
h : m ≫ (idFork h✝).ι = s.ι
⊢ m = s.ι

Tactic:
convert! h

Goal state after:
case e'_2
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
h✝ : f = g
s : Fork f g
m : s.pt ⟶ (idFork h✝).pt
h : m ≫ (idFork h✝).ι = s.ι
e_1✝ : (s.pt ⟶ (idFork h✝).pt) = (s.pt ⟶ X)
⊢ m = m ≫ (idFork h✝).ι
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
h✝ : f = g
s : Cofork f g
m : (idCofork h✝).pt ⟶ s.pt
h : (idCofork h✝).π ≫ m = s.π
⊢ m = s.π

Tactic:
convert! h

Goal state after:
case e'_2
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
h✝ : f = g
s : Cofork f g
m : (idCofork h✝).pt ⟶ s.pt
h : (idCofork h✝).π ≫ m = s.π
e_1✝ : ((idCofork h✝).pt ⟶ s.pt) = (Y ⟶ s.pt)
⊢ m = (idCofork h✝).π ≫ m