mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated

Goal state before:
pp: case mpr
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
T : Triangle Cᵒᵖ
⊢ (∃ T',
      ∃ (_ : T' ∈ Pretriangulated.distinguishedTriangles),
        Nonempty (T ≅ (triangleOpEquivalence C).functor.obj (Opposite.op T'))) →
    Opposite.unop ((triangleOpEquivalence C).inverse.obj T) ∈ Pretriangulated.distinguishedTriangles

Tactic:
rintro ⟨T', hT', ⟨e⟩⟩

Goal state after:
case mpr
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
T : Triangle Cᵒᵖ
T' : Triangle C
hT' : T' ∈ Pretriangulated.distinguishedTriangles
e : T ≅ (triangleOpEquivalence C).functor.obj (Opposite.op T')
⊢ Opposite.unop ((triangleOpEquivalence C).inverse.obj T) ∈ Pretriangulated.distinguishedTriangles
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Triangle

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
T : (Triangle C)ᵒᵖ
⊢ ((Triangle.mk ((functor C).obj T).mor₂.unop ((functor C).obj T).mor₁.unop
            (((opShiftFunctorEquivalence C 1).unitIso.inv.app ((functor C).obj T).obj₁).unop ≫
              (shiftFunctor C 1).map ((functor C).obj T).mor₃.unop)).mor₃ ≫
        (shiftFunctor C 1).map
          (Iso.refl
              (Triangle.mk ((functor C).obj T).mor₂.unop ((functor C).obj T).mor₁.unop
                  (((opShiftFunctorEquivalence C 1).unitIso.inv.app ((functor C).obj T).obj₁).unop ≫
                    (shiftFunctor C 1).map ((functor C).obj T).mor₃.unop)).obj₁).hom).op =
    ((Iso.refl
            (Triangle.mk ((functor C).obj T).mor₂.unop ((functor C).obj T).mor₁.unop
                (((opShiftFunctorEquivalence C 1).unitIso.inv.app ((functor C).obj T).obj₁).unop ≫
                  (shiftFunctor C 1).map ((functor C).obj T).mor₃.unop)).obj₃).hom ≫
        (Opposite.unop T).mor₃).op

Tactic:
by simp [shift_unop_opShiftFunctorEquivalence_counitIso_inv_app]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
X Y : Cᵒᵖ
f : X ⟶ Y
Z : C
g : Z ⟶ Opposite.unop Y
h : Opposite.unop X ⟶ (shiftFunctor C 1).obj Z
H : Triangle.mk g f.unop h ∈ Pretriangulated.distinguishedTriangles
⊢ ((Opposite.unop
            ((triangleOpEquivalence C).inverse.obj
              (Triangle.mk f g.op
                ((opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op Z) ≫
                  (shiftFunctor Cᵒᵖ 1).map h.op)))).mor₃ ≫
        (shiftFunctor C 1).map
          (Iso.refl
              (Opposite.unop
                  ((triangleOpEquivalence C).inverse.obj
                    (Triangle.mk f g.op
                      ((opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op Z) ≫
                        (shiftFunctor Cᵒᵖ 1).map h.op)))).obj₁).hom).op =
    ((Iso.refl
            (Opposite.unop
                ((triangleOpEquivalence C).inverse.obj
                  (Triangle.mk f g.op
                    ((opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op Z) ≫
                      (shiftFunctor Cᵒᵖ 1).map h.op)))).obj₃).hom ≫
        (Triangle.mk g f.unop h).mor₃).op

Tactic:
by simp [shift_unop_opShiftFunctorEquivalence_counitIso_inv_app]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Linear

Goal state before:
pp: case mp
C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹¹ : Category.{v₂, u₂} D
inst✝¹⁰ : Preadditive C
inst✝⁹ : Preadditive D
E : Type u_1
inst✝⁸ : Category.{v_1, u_1} E
L : C ⥤ D
W : MorphismProperty C
inst✝⁷ : L.IsLocalization W
inst✝⁶ : Preadditive E
R : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Linear R C
inst✝³ : Linear R D
inst✝² : Linear R E
inst✝¹ : Functor.Linear R L
F : C ⥤ E
G : D ⥤ E
inst✝ : Lifting L W F G
a✝ : Functor.Linear R F
this✝ : Functor.Linear R (L ⋙ G)
this : L.EssSurj
⊢ Functor.Linear R G

Tactic:
Functor.linear_iff

Goal state after:
case mp
C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹¹ : Category.{v₂, u₂} D
inst✝¹⁰ : Preadditive C
inst✝⁹ : Preadditive D
E : Type u_1
inst✝⁸ : Category.{v_1, u_1} E
L : C ⥤ D
W : MorphismProperty C
inst✝⁷ : L.IsLocalization W
inst✝⁶ : Preadditive E
R : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Linear R C
inst✝³ : Linear R D
inst✝² : Linear R E
inst✝¹ : Functor.Linear R L
F : C ⥤ E
G : D ⥤ E
inst✝ : Lifting L W F G
a✝ : Functor.Linear R F
this✝ : Functor.Linear R (L ⋙ G)
this : L.EssSurj
⊢ ∀ (X : D) (r : R), G.map (r • 𝟙 X) = r • 𝟙 (G.obj X)
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : HasDerivedCategory C
P : C
inst✝¹ : Projective P
L : CochainComplex C ℤ
i : ℤ
φ : Q.obj ((CochainComplex.singleFunctor C i).obj P) ⟶ Q.obj L
n : ℤ
hn : n < i
inst✝ : L.IsStrictlyLE n
⊢ φ = 0

Tactic:
by
  obtain ⟨K, _, π, h, g, rfl⟩ := right_fac_of_isStrictlyLE φ i
  have hπ : IsSplitEpi π := by
    rw [isIso_Q_map_iff_quasiIso] at h
    exact CochainComplex.isSplitEpi_to_singleFunctor_obj_of_projective π
  have h₁ : inv (Q.map π) = Q.map (section_ π) := by
    rw [← cancel_mono (Q.map π), IsIso.inv_hom_id, ← Q.map_comp, IsSplitEpi.id, Q.map_id]
  have h₂ : section_ π ≫ g = 0 := by
    apply HomologicalComplex.from_single_hom_ext
    apply (L.isZero_of_isStrictlyLE n i hn).eq_of_tgt
  rw [h₁, ← Q.map_comp, h₂, Q.map_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.SesquilinearForm.Orthogonal

Goal state before:
pp: K : Type u_7
K₁ : Type u_8
V₁ : Type u_10
V₂ : Type u_11
inst✝⁵ : Field K
inst✝⁴ : Field K₁
inst✝³ : AddCommGroup V₁
inst✝² : Module K₁ V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
J₁ J₁' : K₁ →+* K
B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] V₂
x : V₁
hx : (B x) x ≠ 0
μ : V₁ → K₁
h : (B x) (∑ a ∈ {x}, μ a • a) = 0
⊢ ∑ a ∈ {x}, μ a • a ∈ ⊥

Tactic:
Finset.sum_singleton

Goal state after:
K : Type u_7
K₁ : Type u_8
V₁ : Type u_10
V₂ : Type u_11
inst✝⁵ : Field K
inst✝⁴ : Field K₁
inst✝³ : AddCommGroup V₁
inst✝² : Module K₁ V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
J₁ J₁' : K₁ →+* K
B : V₁ →ₛₗ[J₁] V₁ →ₛₗ[J₁'] V₂
x : V₁
hx : (B x) x ≠ 0
μ : V₁ → K₁
h : (B x) (μ x • x) = 0
⊢ μ x • x ∈ ⊥
Module: Mathlib.RingTheory.RootsOfUnity.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝⁵ : CommMonoid M
inst✝⁴ : CommMonoid N
inst✝³ : DivisionCommMonoid G
k l : ℕ
inst✝² : NeZero k
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : { x // x ∈ nthRoots k 1 }
⊢ ↥(rootsOfUnity k R)

Tactic:
refine ⟨⟨x, ↑x ^ (k - 1 : ℕ), ?_, ?_⟩, ?_⟩

Goal state after:
case refine_1
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝⁵ : CommMonoid M
inst✝⁴ : CommMonoid N
inst✝³ : DivisionCommMonoid G
k l : ℕ
inst✝² : NeZero k
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : { x // x ∈ nthRoots k 1 }
⊢ ↑x * ↑x ^ (k - 1) = 1

case refine_2
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝⁵ : CommMonoid M
inst✝⁴ : CommMonoid N
inst✝³ : DivisionCommMonoid G
k l : ℕ
inst✝² : NeZero k
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : { x // x ∈ nthRoots k 1 }
⊢ ↑x ^ (k - 1) * ↑x = 1

case refine_3
M : Type u_1
N : Type u_2
G : Type u_3
R : Type u_4
S : Type u_5
F : Type u_6
inst✝⁵ : CommMonoid M
inst✝⁴ : CommMonoid N
inst✝³ : DivisionCommMonoid G
k l : ℕ
inst✝² : NeZero k
inst✝¹ : CommRing R
inst✝ : IsDomain R
x : { x // x ∈ nthRoots k 1 }
⊢ { val := ↑x, inv := ↑x ^ (k - 1), val_inv := ?refine_1, inv_val := ?refine_2 } ∈ rootsOfUnity k R
Module: Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv

Goal state before:
pp: case e'_5
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
N : Type u_9
inst✝³ : Field K
inst✝² : Invertible 2
inst✝¹ : AddCommGroup V
inst✝ : Module K V
Q : QuadraticForm K V
v : Basis (Fin (finrank K V)) K V
hv₁ : LinearMap.IsOrthoᵢ (associated Q) ⇑v
iso : IsometryEquiv Q (basisRepr Q v) := isometryEquivBasisRepr Q v
m : V
⊢ (weightedSumSquares K fun i ↦ Q (v i)) = basisRepr Q v

Tactic:
basisRepr_eq_of_iIsOrtho _ _ hv₁

Goal state after:
case e'_5
ι : Type u_1
R : Type u_2
K : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
N : Type u_9
inst✝³ : Field K
inst✝² : Invertible 2
inst✝¹ : AddCommGroup V
inst✝ : Module K V
Q : QuadraticForm K V
v : Basis (Fin (finrank K V)) K V
hv₁ : LinearMap.IsOrthoᵢ (associated Q) ⇑v
iso : IsometryEquiv Q (basisRepr Q v) := isometryEquivBasisRepr Q v
m : V
⊢ (weightedSumSquares K fun i ↦ Q (v i)) = weightedSumSquares K fun i ↦ Q (v i)
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: n : Type u
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type v
inst✝¹ : CommRing R
S : Type u_1
inst✝ : CommRing S
i : n
a : ↥(rootsOfUnity (Fintype.card n) R)
⊢ (fun A ↦ rootsOfUnity.mkOfPowEq (↑↑A i i) ⋯) ((fun a ↦ ⟨⟨a • 1, ⋯⟩, ⋯⟩) a) = a

Tactic:
by
    obtain ⟨⟨a, _⟩, ha⟩ := a
    exact SetCoe.ext <| Units.ext <| by simp

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: R : Type v
inst✝ : CommRing R
P : SL(2, R) → Prop
h : ∀ (a b c d : R) (hdet : a * d - b * c = 1), P ⟨!![a, b; c, d], ⋯⟩
m : Matrix (Fin 2) (Fin 2) R
hm : m.det = 1
⊢ m 0 0 * m 1 1 - m 0 1 * m 1 0 = 1

Tactic:
det_fin_two

Goal state after:
R : Type v
inst✝ : CommRing R
P : SL(2, R) → Prop
h : ∀ (a b c d : R) (hdet : a * d - b * c = 1), P ⟨!![a, b; c, d], ⋯⟩
m : Matrix (Fin 2) (Fin 2) R
hm : m 0 0 * m 1 1 - m 0 1 * m 1 0 = 1
⊢ m 0 0 * m 1 1 - m 0 1 * m 1 0 = 1
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R
j : Fin 2
u v : R
h : u * a + v * b = 1
⊢ ∃ g, ↑g 0 j = a ∧ ↑g 1 j = b

Tactic:
refine match j with
  | 0 => ⟨⟨!![a, -v; b, u], ?_⟩, rfl, rfl⟩
  | 1 => ⟨⟨!![v, a; -u, b], ?_⟩, rfl, rfl⟩ <;>
  · rw [Matrix.det_fin_two_of, ← h]
    ring

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
b c : F
hc : c = b * (a ^ 2 - 1)
⊢ ⁅diag2 a ha, SpecialLinearGroup.transvection ⋯ b⁆ = SpecialLinearGroup.transvection ⋯ c

Tactic:
rw [commutatorElement_def, diag2_inv a ha, SpecialLinearGroup.transvection_inv zero_ne_one b]

Goal state after:
F : Type u_1
inst✝ : Field F
a : F
ha : a ≠ 0
b c : F
hc : c = b * (a ^ 2 - 1)
⊢ diag2 a ha * SpecialLinearGroup.transvection ⋯ b * diag2 a⁻¹ ⋯ * SpecialLinearGroup.transvection ⋯ (-b) =
    SpecialLinearGroup.transvection ⋯ c
Module: Mathlib.Algebra.DirectSum.Internal

Goal state before:
pp: case succ
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁴ : Zero ι
inst✝³ : AddMonoidWithOne R
inst✝² : SetLike σ R
inst✝¹ : AddSubmonoidClass σ R
A : ι → σ
inst✝ : GradedOne A
n✝ : ℕ
n_ih : ↑n✝ ∈ A 0
⊢ ↑(n✝ + 1) ∈ A 0

Tactic:
Nat.cast_succ

Goal state after:
case succ
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝⁴ : Zero ι
inst✝³ : AddMonoidWithOne R
inst✝² : SetLike σ R
inst✝¹ : AddSubmonoidClass σ R
A : ι → σ
inst✝ : GradedOne A
n✝ : ℕ
n_ih : ↑n✝ ∈ A 0
⊢ ↑n✝ + 1 ∈ A 0
Module: Mathlib.LinearAlgebra.Matrix.SesquilinearForm

Goal state before:
pp: R : Type u_1
n : Type u_11
m : Type u_12
inst✝⁴ : CommRing R
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix m n R
⊢ ((toLinearMap₂' R) M).SeparatingRight ↔ M.SeparatingRight

Tactic:
refine ⟨fun h ↦ separatingRight_def.mpr ?_, SeparatingRight.toLinearMap₂'⟩

Goal state after:
R : Type u_1
n : Type u_11
m : Type u_12
inst✝⁴ : CommRing R
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix m n R
h : ((toLinearMap₂' R) M).SeparatingRight
⊢ ∀ (w : n → R), (∀ (v : m → R), v ⬝ᵥ M *ᵥ w = 0) → w = 0
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold

Goal state before:
pp: case mem.add
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
P : CliffordAlgebra Q → Prop
algebraMap : ∀ (r : R), P ((Algebra.algebraMap R (CliffordAlgebra Q)) r)
add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
mul_ι : ∀ (m : M) (x : CliffordAlgebra Q), P x → P (x * (ι Q) m)
x✝ : CliffordAlgebra Q
i : ℕ
x _x _y : CliffordAlgebra Q
_i : ℕ
hx✝ : _x ∈ (ι Q).range ^ _i
hy✝ : _y ∈ (ι Q).range ^ _i
ihx : P _x
ihy : P _y
⊢ P (_x + _y)

Tactic:
| add _x _y _i _ _ ihx ihy =>

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₁ : HasInjectiveDimensionLT S.X₁ n
h₃ : HasInjectiveDimensionLT S.X₃ n
this : HasExt C := HasExt.standard C
i : ℕ
hi : n ≤ i
Y : C
x₃ : Ext Y S.X₁ i
⊢ x₃.comp (Ext.mk₀ S.f) ⋯ = 0

Tactic:
x₃.eq_zero_of_hasInjectiveDimensionLT n hi,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₁ : HasInjectiveDimensionLT S.X₁ n
h₃ : HasInjectiveDimensionLT S.X₃ n
this : HasExt C := HasExt.standard C
i : ℕ
hi : n ≤ i
Y : C
x₃ : Ext Y S.X₁ i
⊢ Ext.comp 0 (Ext.mk₀ S.f) ⋯ = 0
Module: Mathlib.Algebra.Homology.LeftResolution.Basic

Goal state before:
pp: A : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasZeroMorphisms C
inst✝ : Abelian A
n : ℕ
⊢ ι.map ((Λ.chainComplex X).d (n + 1) n ≫ (Λ.chainComplexMap f).f n) =
    ι.map ((Λ.chainComplexMap f).f (n + 1) ≫ (Λ.chainComplex Y).d (n + 1) n)

Tactic:
HomologicalComplex.Hom.comm

Goal state after:
A : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasZeroMorphisms C
inst✝ : Abelian A
n : ℕ
⊢ ι.map ((Λ.chainComplex X).d (n + 1) n ≫ (Λ.chainComplexMap f).f n) =
    ι.map ((Λ.chainComplex X).d (n + 1) n ≫ (Λ.chainComplexMap f).f n)
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
J : Type u₂
inst✝² : Category.{v₂, u₂} J
F : J ⥤ PresheafOfModules R
inst✝¹ :
  ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
inst✝ : ∀ (X : Cᵒᵖ), HasColimit (F ⋙ evaluation R X)
X : Cᵒᵖ
j : J
⊢ colimit.ι (F ⋙ evaluation R X) j ≫
      colimMap (F.whiskerLeft (restriction R (𝟙 X))) ≫
        (preservesColimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 X)))) (F ⋙ evaluation R X)).inv =
    colimit.ι (F ⋙ evaluation R X) j ≫
      (ModuleCat.restrictScalarsId' (RingCat.Hom.hom (R.map (𝟙 X))) ⋯).inv.app (colimit (F ⋙ evaluation R X))

Tactic:
by
    dsimp
    rw [ι_colimMap_assoc, Functor.whiskerLeft_app, restriction_app]
    -- Here we should rewrite using `Functor.assoc` but that gives a "motive is type-incorrect"
    erw [ι_preservesColimitIso_inv (G := ModuleCat.restrictScalars (R.map (𝟙 X)).hom)]
    rw [ModuleCat.restrictScalarsId'App_inv_naturality, map_id]
    dsimp

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case h₁
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsCofilteredOrEmpty C
d : D
h₁ : ∃ c, Nonempty (F.obj c ⟶ d)
h₂ : ∀ {c : C} (s s' : F.obj c ⟶ d), ∃ c' t, F.map t ≫ s = F.map t ≫ s'
⊢ ∃ c, Nonempty (op d ⟶ F.op.obj c)

Tactic:
obtain ⟨c, ⟨t⟩⟩ := h₁
    exact ⟨op c, ⟨Quiver.Hom.op t⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: C : Type v₁
inst✝³ : Category.{v₁, v₁} C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
F : C ⥤ D
inst✝¹ : IsFilteredOrEmpty C
inst✝ : F.Final
d : D
c : C
s s' : d ⟶ F.obj c
this :
  (ConcreteCategory.hom (colimit.ι (F ⋙ coyoneda.obj (op d)) c)) s =
    (ConcreteCategory.hom (colimit.ι (F ⋙ coyoneda.obj (op d)) c)) s'
c' : C
t₁ t₂ : c ⟶ c'
h :
  (ConcreteCategory.hom ((F ⋙ coyoneda.obj (op d)).map t₁)) s =
    (ConcreteCategory.hom ((F ⋙ coyoneda.obj (op d)).map t₂)) s'
⊢ ∃ c' t, s ≫ F.map t = s' ≫ F.map t

Tactic:
refine ⟨IsFiltered.coeq t₁ t₂, t₁ ≫ IsFiltered.coeqHom t₁ t₂, ?_⟩

Goal state after:
C : Type v₁
inst✝³ : Category.{v₁, v₁} C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
F : C ⥤ D
inst✝¹ : IsFilteredOrEmpty C
inst✝ : F.Final
d : D
c : C
s s' : d ⟶ F.obj c
this :
  (ConcreteCategory.hom (colimit.ι (F ⋙ coyoneda.obj (op d)) c)) s =
    (ConcreteCategory.hom (colimit.ι (F ⋙ coyoneda.obj (op d)) c)) s'
c' : C
t₁ t₂ : c ⟶ c'
h :
  (ConcreteCategory.hom ((F ⋙ coyoneda.obj (op d)).map t₁)) s =
    (ConcreteCategory.hom ((F ⋙ coyoneda.obj (op d)).map t₂)) s'
⊢ s ≫ F.map (t₁ ≫ IsFiltered.coeqHom t₁ t₂) = s' ≫ F.map (t₁ ≫ IsFiltered.coeqHom t₁ t₂)
Module: Mathlib.CategoryTheory.Monoidal.Limits.Colimits

Goal state before:
pp: case refine_1
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : MonoidalCategory C
J : Type u_2
J₁ : Type u_3
J₂ : Type u_4
inst✝⁴ : Category.{v_2, u_2} J
inst✝³ : Category.{v_3, u_3} J₁
inst✝² : Category.{v_4, u_4} J₂
F₁ F₂ : J ⥤ C
c₁ : Cocone F₁
c₂ : Cocone F₂
inst✝¹ : PreservesColimit₂ F₁ F₂ (curriedTensor C)
inst✝ : IsSifted J
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
⊢ Functor.diag J ⋙ externalProduct F₁ F₂ ≅ F₁ ⊗ F₂

Tactic:
exact NatIso.ofComponents (fun _ ↦ Iso.refl _) (fun _ ↦ by simp)

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
M' : PresheafOfModules R
cM' : Cocone M'.presheaf
hcM' : IsColimit cM'
M'' : PresheafOfModules R
cM'' : Cocone M''.presheaf
hcM'' : IsColimit cM''
m : ModuleColimit hcR hcM
m' : ModuleColimit hcR hcM'
m'' : ModuleColimit hcR hcM''
U : Cᵒᵖ
x : (M.presheaf ⋙ forget AddCommGrpCat).obj U
x' : (M'.presheaf ⋙ forget AddCommGrpCat).obj U
x'' : (M''.presheaf ⋙ forget AddCommGrpCat).obj U
h :
  ((ConcreteCategory.hom
            ((((forget AddCommGrpCat).mapCocone cM).tensor
                    (((forget AddCommGrpCat).mapCocone cM').tensor ((forget AddCommGrpCat).mapCocone cM''))).ι.app
              U))
          (x, x', x'')).1 =
      (m, m', m'').1 ∧
    ((ConcreteCategory.hom
                ((((forget AddCommGrpCat).mapCocone cM).tensor
                        (((forget AddCommGrpCat).mapCocone cM').tensor ((forget AddCommGrpCat).mapCocone cM''))).ι.app
                  U))
              (x, x', x'')).2.1 =
        (m, m', m'').2.1 ∧
      ((ConcreteCategory.hom
                ((((forget AddCommGrpCat).mapCocone cM).tensor
                        (((forget AddCommGrpCat).mapCocone cM').tensor ((forget AddCommGrpCat).mapCocone cM''))).ι.app
                  U))
              (x, x', x'')).2.2 =
        (m, m', m'').2.2
⊢ ∃ U x x' x'', ιM x = m ∧ ιM x' = m' ∧ ιM x'' = m''

Tactic:
obtain ⟨rfl, rfl, rfl⟩ := h

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
M' : PresheafOfModules R
cM' : Cocone M'.presheaf
hcM' : IsColimit cM'
M'' : PresheafOfModules R
cM'' : Cocone M''.presheaf
hcM'' : IsColimit cM''
U : Cᵒᵖ
x : (M.presheaf ⋙ forget AddCommGrpCat).obj U
x' : (M'.presheaf ⋙ forget AddCommGrpCat).obj U
x'' : (M''.presheaf ⋙ forget AddCommGrpCat).obj U
⊢ ∃ U_1 x_1 x'_1 x''_1,
    ιM x_1 =
        ((ConcreteCategory.hom
              ((((forget AddCommGrpCat).mapCocone cM).tensor
                      (((forget AddCommGrpCat).mapCocone cM').tensor ((forget AddCommGrpCat).mapCocone cM''))).ι.app
                U))
            (x, x', x'')).1 ∧
      ιM x'_1 =
          ((ConcreteCategory.hom
                  ((((forget AddCommGrpCat).mapCocone cM).tensor
                          (((forget AddCommGrpCat).mapCocone cM').tensor ((forget AddCommGrpCat).mapCocone cM''))).ι.app
                    U))
                (x, x', x'')).2.1 ∧
        ιM x''_1 =
          ((ConcreteCategory.hom
                  ((((forget AddCommGrpCat).mapCocone cM).tensor
                          (((forget AddCommGrpCat).mapCocone cM').tensor ((forget AddCommGrpCat).mapCocone cM''))).ι.app
                    U))
                (x, x', x'')).2.2
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
r₁ r₂ : ↑cR.pt
m : ModuleColimit hcR hcM
U : Cᵒᵖ
a₁ a₂ : (R ⋙ forget RingCat).obj U
x : (M.presheaf ⋙ forget AddCommGrpCat).obj U
h :
  ((ConcreteCategory.hom
            ((((forget RingCat).mapCocone cR).tensor
                    (((forget RingCat).mapCocone cR).tensor ((forget AddCommGrpCat).mapCocone cM))).ι.app
              U))
          (a₁, a₂, x)).1 =
      (r₁, r₂, m).1 ∧
    ((ConcreteCategory.hom
                ((((forget RingCat).mapCocone cR).tensor
                        (((forget RingCat).mapCocone cR).tensor ((forget AddCommGrpCat).mapCocone cM))).ι.app
                  U))
              (a₁, a₂, x)).2.1 =
        (r₁, r₂, m).2.1 ∧
      ((ConcreteCategory.hom
                ((((forget RingCat).mapCocone cR).tensor
                        (((forget RingCat).mapCocone cR).tensor ((forget AddCommGrpCat).mapCocone cM))).ι.app
                  U))
              (a₁, a₂, x)).2.2 =
        (r₁, r₂, m).2.2
⊢ ∃ U a₁ a₂ x, (ιR cR) a₁ = r₁ ∧ (ιR cR) a₂ = r₂ ∧ ιM x = m

Tactic:
obtain ⟨rfl, rfl, rfl⟩ := h

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
U : Cᵒᵖ
a₁ a₂ : (R ⋙ forget RingCat).obj U
x : (M.presheaf ⋙ forget AddCommGrpCat).obj U
⊢ ∃ U_1 a₁_1 a₂_1 x_1,
    (ιR cR) a₁_1 =
        ((ConcreteCategory.hom
              ((((forget RingCat).mapCocone cR).tensor
                      (((forget RingCat).mapCocone cR).tensor ((forget AddCommGrpCat).mapCocone cM))).ι.app
                U))
            (a₁, a₂, x)).1 ∧
      (ιR cR) a₂_1 =
          ((ConcreteCategory.hom
                  ((((forget RingCat).mapCocone cR).tensor
                          (((forget RingCat).mapCocone cR).tensor ((forget AddCommGrpCat).mapCocone cM))).ι.app
                    U))
                (a₁, a₂, x)).2.1 ∧
        ιM x_1 =
          ((ConcreteCategory.hom
                  ((((forget RingCat).mapCocone cR).tensor
                          (((forget RingCat).mapCocone cR).tensor ((forget AddCommGrpCat).mapCocone cM))).ι.app
                    U))
                (a₁, a₂, x)).2.2