mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv

Goal state before:
pp: case mp.refine_2
n : Type u_1
inst✝⁶ : Fintype n
A : Type u_4
K : Type u_5
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this : (∃ v, v ≠ 0 ∧ (algebraMap A K).mapMatrix M *ᵥ v = 0) ↔ M.det = 0
v : n → A
hv : v ≠ 0
mul_eq : M *ᵥ v = 0
i : n
⊢ (algebraMap A K) ((M *ᵥ v) i) = 0 i

Tactic:
mul_eq,

Goal state after:
case mp.refine_2
n : Type u_1
inst✝⁶ : Fintype n
A : Type u_4
K : Type u_5
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this : (∃ v, v ≠ 0 ∧ (algebraMap A K).mapMatrix M *ᵥ v = 0) ↔ M.det = 0
v : n → A
hv : v ≠ 0
mul_eq : M *ᵥ v = 0
i : n
⊢ (algebraMap A K) (0 i) = 0 i
Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv

Goal state before:
pp: case mpr.refine_2.calc_2
n : Type u_1
inst✝⁶ : Fintype n
A : Type u_4
K : Type u_5
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this✝ : (∃ v, v ≠ 0 ∧ (algebraMap A K).mapMatrix M *ᵥ v = 0) ↔ M.det = 0
v : n → K
hv : v ≠ 0
mul_eq : (algebraMap A K).mapMatrix M *ᵥ v = 0
this : DecidableEq K := Classical.decEq K
b : A
hb : b ∈ nonZeroDivisors A
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf : ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ), (algebraMap A K) (f a a_1) = ↑⟨b, hb⟩ • a
i : n
⊢ ((algebraMap A K) b • (algebraMap A K).mapMatrix M *ᵥ v) i = 0

Tactic:
mul_eq,

Goal state after:
case mpr.refine_2.calc_2
n : Type u_1
inst✝⁶ : Fintype n
A : Type u_4
K : Type u_5
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this✝ : (∃ v, v ≠ 0 ∧ (algebraMap A K).mapMatrix M *ᵥ v = 0) ↔ M.det = 0
v : n → K
hv : v ≠ 0
mul_eq : (algebraMap A K).mapMatrix M *ᵥ v = 0
this : DecidableEq K := Classical.decEq K
b : A
hb : b ∈ nonZeroDivisors A
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf : ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ), (algebraMap A K) (f a a_1) = ↑⟨b, hb⟩ • a
i : n
⊢ ((algebraMap A K) b • 0) i = 0
Module: Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup

Goal state before:
pp: ι : Type u_1
F : Type u_2
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : CommRing F
i j : ι
hij : i ≠ j
b : F
⊢ transvection hij (-b) * transvection hij b = transvection hij (-b) * transvection hij (- -b)

Tactic:
neg_neg

Goal state after:
ι : Type u_1
F : Type u_2
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : CommRing F
i j : ι
hij : i ≠ j
b : F
⊢ transvection hij (-b) * transvection hij b = transvection hij (-b) * transvection hij b
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
⊢ x ∈ Algebra.adjoin R (Set.range ⇑(ι Q))

Tactic:
induction x using induction with

Goal state after:
Module: Mathlib.Algebra.DirectSum.Ring

Goal state before:
pp: case nil
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
α : Type u_3
fι : α → ι
fA : (a : α) → A (fι a)
⊢ (of A ([].dProdIndex fι)) ([].dProd fι fA) = (List.map (fun a ↦ (of A (fι a)) (fA a)) []).prod

Tactic:
simp only [List.map_nil, List.prod_nil, List.dProd_nil]

Goal state after:
case nil
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
α : Type u_3
fι : α → ι
fA : (a : α) → A (fι a)
⊢ (of A ([].dProdIndex fι)) GradedMonoid.GOne.one = 1
Module: Mathlib.LinearAlgebra.CliffordAlgebra.Fold

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N
v_mul : M →ₗ[R] Module.End R (CliffordAlgebra Q)
l : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] CliffordAlgebra Q
⊢ M →ₗ[R] Module.End R (CliffordAlgebra Q × N)

Tactic:
exact
    { toFun := fun m => (l m).prod (f m)
      map_add' := fun v₂ v₂ =>
        LinearMap.ext fun x =>
          Prod.ext (LinearMap.congr_fun (l.map_add _ _) x) (LinearMap.congr_fun (f.map_add _ _) x)
      map_smul' := fun c v =>
        LinearMap.ext fun x =>
          Prod.ext (LinearMap.congr_fun (l.map_smul _ _) x)
            (LinearMap.congr_fun (f.map_smul _ _) x) }

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: case refine_1
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
r : R
h : (ι R) x = (algebraMap R (ExteriorAlgebra R M)) r
⊢ x = 0 ∧ r = 0

Tactic:
let : Module Rᵐᵒᵖ M := Module.compHom _ ((RingHom.id R).fromOpposite mul_comm)

Goal state after:
case refine_1
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
r : R
h : (ι R) x = (algebraMap R (ExteriorAlgebra R M)) r
this : Module Rᵐᵒᵖ M := Module.compHom M ((RingHom.id R).fromOpposite ⋯)
⊢ x = 0 ∧ r = 0
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: case neg
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
f : Fin (n + 1) → M
i : Fin (n + 1)
h : ¬i = 0
hn : (ι R) (f 0) * (ι R) (f i) * (List.ofFn fun i ↦ (ι R) (f i.succ)).prod = 0
⊢ ((ι R) (f 0) * (ι R) (f i) + (ι R) (f i) * (ι R) (f 0)) * (List.ofFn fun i ↦ (ι R) (f i.succ)).prod = 0

Tactic:
ι_add_mul_swap,

Goal state after:
case neg
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
f : Fin (n + 1) → M
i : Fin (n + 1)
h : ¬i = 0
hn : (ι R) (f 0) * (ι R) (f i) * (List.ofFn fun i ↦ (ι R) (f i.succ)).prod = 0
⊢ 0 * (List.ofFn fun i ↦ (ι R) (f i.succ)).prod = 0
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u4
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
⊢ ιInv ∘ₗ (map f).toLinearMap = f ∘ₗ ιInv

Tactic:
let : Module Rᵐᵒᵖ M := Module.compHom _ ((RingHom.id R).fromOpposite mul_comm)

Goal state after:
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u4
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
this : Module Rᵐᵒᵖ M := Module.compHom M ((RingHom.id R).fromOpposite ⋯)
⊢ ιInv ∘ₗ (map f).toLinearMap = f ∘ₗ ιInv
Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits

Goal state before:
pp: R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
x : ↑(M F)
⊢ 1 • x = x

Tactic:
obtain ⟨j, x, rfl⟩ := M.mk_surjective F x
    simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.FilteredColimits

Goal state before:
pp: R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
r : R
i : J
x : ↑(F.obj i)
j : J
y : ↑(F.obj j)
⊢ M.mk F
      ⟨⟨IsFiltered.max i j,
            (hom (F.map (IsFiltered.leftToMax i j))) ⟨i, x⟩.snd +
              (hom (F.map (IsFiltered.rightToMax i j))) ⟨j, y⟩.snd⟩.fst,
        r • (hom (F.map (IsFiltered.leftToMax i j))) ⟨i, x⟩.snd +
          r • (hom (F.map (IsFiltered.rightToMax i j))) ⟨j, y⟩.snd⟩ =
    M.mk F
      ⟨IsFiltered.max i j,
        r • (hom (F.map (IsFiltered.leftToMax i j))) ⟨i, x⟩.snd +
          (hom (F.map (IsFiltered.rightToMax i j))) ⟨j, r • ⟨j, y⟩.snd⟩.snd⟩

Tactic:
map_smul

Goal state after:
R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ ModuleCat R
r : R
i : J
x : ↑(F.obj i)
j : J
y : ↑(F.obj j)
⊢ M.mk F
      ⟨⟨IsFiltered.max i j,
            (hom (F.map (IsFiltered.leftToMax i j))) ⟨i, x⟩.snd +
              (hom (F.map (IsFiltered.rightToMax i j))) ⟨j, y⟩.snd⟩.fst,
        r • (hom (F.map (IsFiltered.leftToMax i j))) ⟨i, x⟩.snd +
          r • (hom (F.map (IsFiltered.rightToMax i j))) ⟨j, y⟩.snd⟩ =
    M.mk F
      ⟨IsFiltered.max i j,
        r • (hom (F.map (IsFiltered.leftToMax i j))) ⟨i, x⟩.snd +
          r • (hom (F.map (IsFiltered.rightToMax i j))) ⟨j, y⟩.snd⟩
Module: Mathlib.Algebra.Category.ModuleCat.Images

Goal state before:
pp: case a
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
c : R
x : ↥(Hom.hom f).range
⊢ (ConcreteCategory.hom F'.m)
      ((ConcreteCategory.hom F'.e) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑(c • x)) ⋯)) =
    (ConcreteCategory.hom F'.m)
      ((RingHom.id R) c •
        (ConcreteCategory.hom F'.e) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑x) ⋯))

Tactic:
map_smul

Goal state after:
case a
R : Type u
inst✝ : Ring R
G H : ModuleCat R
f : G ⟶ H
F' : MonoFactorisation f
c : R
x : ↥(Hom.hom f).range
⊢ (ConcreteCategory.hom F'.m)
      ((ConcreteCategory.hom F'.e) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑(c • x)) ⋯)) =
    (RingHom.id R) c •
      (ConcreteCategory.hom F'.m)
        ((ConcreteCategory.hom F'.e) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑x) ⋯))
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 : A
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasZeroMorphisms C
inst✝ : Abelian A
n : ℕ
this :
  ι.map
      (ι.preimage
        (Λ.π.app (limit (parallelPair (ι.map ((Λ.chainComplex X).d (n + 1) n)) 0)) ≫
          kernel.ι (ι.map ((Λ.chainComplex X).d (n + 1) n)))) =
    Λ.π.app (limit (parallelPair (ι.map ((Λ.chainComplex X).d (n + 1) n)) 0)) ≫
      kernel.ι (ι.map ((Λ.chainComplex X).d (n + 1) n))
⊢ (Λ.chainComplex X).d (n + 2) (n + 1) =
    (Λ.chainComplexXIso X n).hom ≫
      ι.preimage
        (Λ.π.app (limit (parallelPair (ι.map ((Λ.chainComplex X).d (n + 1) n)) 0)) ≫
          kernel.ι (ι.map ((Λ.chainComplex X).d (n + 1) n)))

Tactic:
apply ChainComplex.mk'_d

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

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 : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections
c : Cone F
hc : (X : Cᵒᵖ) → IsLimit ((evaluation R X).mapCone c)
s : Cone F
X Y : Cᵒᵖ
f : X ⟶ Y
j : J
⊢ (s.pt.map f ≫
        (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((hc Y).lift ((evaluation R Y).mapCone s))) ≫
      ((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).mapCone ((evaluation R Y).mapCone c)).π.app j =
    ((hc X).lift ((evaluation R X).mapCone s) ≫ c.pt.map f) ≫
      ((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).mapCone ((evaluation R Y).mapCone c)).π.app j

Tactic:
have h₁ := (c.π.app j).naturality f

Goal state after:
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 : Cᵒᵖ), Small.{v, max u₂ v} ↑((F ⋙ evaluation R X) ⋙ forget (ModuleCat ↑(R.obj X))).sections
c : Cone F
hc : (X : Cᵒᵖ) → IsLimit ((evaluation R X).mapCone c)
s : Cone F
X Y : Cᵒᵖ
f : X ⟶ Y
j : J
h₁ :
  (((Functor.const J).obj c.pt).obj j).map f ≫
      (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((c.π.app j).app Y) =
    (c.π.app j).app X ≫ (F.obj j).map f
⊢ (s.pt.map f ≫
        (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((hc Y).lift ((evaluation R Y).mapCone s))) ≫
      ((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).mapCone ((evaluation R Y).mapCone c)).π.app j =
    ((hc X).lift ((evaluation R X).mapCone s) ≫ c.pt.map f) ≫
      ((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).mapCone ((evaluation R Y).mapCone c)).π.app j
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)))
c : Cocone F
hc : (X : Cᵒᵖ) → IsColimit ((evaluation R X).mapCocone c)
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
⊢ m = { app := fun X ↦ (hc X).desc ((evaluation R X).mapCocone s), naturality := ⋯ }

Tactic:
ext1 X
    apply (hc X).uniq ((evaluation R X).mapCocone s)
    intro j
    dsimp
    rw [← hm]
    rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Bifunctor

Goal state before:
pp: J₁ : Type u_1
J₂ : Type u_2
inst✝⁷ : Category.{v_1, u_1} J₁
inst✝⁶ : Category.{v_2, u_2} J₂
C₁ : Type u_3
C₂ : Type u_4
C : Type u_5
inst✝⁵ : Category.{v_3, u_3} C₁
inst✝⁴ : Category.{v_4, u_4} C₂
inst✝³ : Category.{v_5, u_5} C
K₁ : J₁ ⥤ C₁
K₂ : J₂ ⥤ C₂
G : C₁ ⥤ C₂ ⥤ C
inst✝² : PreservesColimit₂ K₁ K₂ G
inst✝¹ : ∀ (x : C₂), PreservesColimit K₁ (G.flip.obj x)
inst✝ : ∀ (x : C₁), PreservesColimit K₂ (G.obj x)
c₁ : Cocone K₁
hc₁ : IsColimit c₁
c₂ : Cocone K₂
hc₂ : IsColimit c₂
Q₀ : DiagramOfCocones ((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G) :=
  { obj := fun j₁ ↦ (G.obj (K₁.obj j₁)).mapCocone c₂,
    map := fun {j j'} f ↦ { hom := (G.map (K₁.map f)).app c₂.pt, w := ⋯ }, id := ⋯, comp := ⋯ }
P : (j₁ : J₁) → IsColimit (Q₀.obj j₁) := fun j ↦ isColimitOfPreserves (G.obj (K₁.obj j)) hc₂
E₀ : Q₀.coconePoints ≅ K₁ ⋙ G.flip.obj c₂.pt := NatIso.ofComponents (fun x ↦ Iso.refl (Q₀.coconePoints.obj x)) ⋯
j₁ : J₁
⊢ ((Cocone.precompose E₀.hom).obj (coconeOfCoconeUncurry P (G.mapCocone₂ c₁ c₂))).ι.app j₁ ≫
      (Iso.refl ((Cocone.precompose E₀.hom).obj (coconeOfCoconeUncurry P (G.mapCocone₂ c₁ c₂))).pt).hom =
    ((G.flip.obj c₂.pt).mapCocone c₁).ι.app j₁

Tactic:
by
          dsimp [E₀, Q₀]
          simp only [id_comp, comp_id]
          let s : Cocone (whiskeringLeft₂ C |>.obj K₁ |>.obj K₂ |>.obj G |>.obj j₁) := ?_
          change (P j₁).desc s = _
          symm
          apply (P j₁).hom_ext
          intro j₂
          have := (P j₁).fac s j₂
          simp only [Functor.mapCocone_pt, Functor.mapCocone_ι_app, Q₀, s] at this
          simp only [Functor.mapCocone_pt,
            Functor.mapCocone_ι_app, NatTrans.naturality, this, Q₀, s]

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
r₁ r₂ : ↑cR.pt
m : ModuleColimit hcR hcM
⊢ ∃ U a₁ a₂ x, (ιR cR) a₁ = r₁ ∧ (ιR cR) a₂ = r₂ ∧ ιM x = m

Tactic:
obtain ⟨U, ⟨a₁, a₂, x⟩, h⟩ := Types.jointly_surjective_of_isColimit
    ((isColimitOfPreserves (forget RingCat) hcR).tensor
      ((isColimitOfPreserves (forget RingCat) hcR).tensor
        (isColimitOfPreserves (forget AddCommGrpCat) hcM))) ⟨r₁, r₂, m⟩
  rw [Prod.ext_iff, Prod.ext_iff] at h
  obtain ⟨rfl, rfl, rfl⟩ := h
  exact ⟨U, a₁, a₂, x, rfl, rfl, rfl⟩

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''
N : ModuleCat ↑cR.pt
ψ : M ⟶ (constFunctor cR).obj N
φ : ModuleColimit hcR hcM →+ N.1
hφ : (homEquiv' hcR hcM) φ = (toPresheaf R).map ψ
U : Cᵒᵖ
r : ↑(R.obj U)
m : ↑(M.obj U)
⊢ (ConcreteCategory.hom (ψ.app U)) (r • m) =
    (ConcreteCategory.hom (cR.ι.app U)) r • (ConcreteCategory.hom (((toPresheaf R).map ψ).app U)) m

Tactic:
map_smul

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''
N : ModuleCat ↑cR.pt
ψ : M ⟶ (constFunctor cR).obj N
φ : ModuleColimit hcR hcM →+ N.1
hφ : (homEquiv' hcR hcM) φ = (toPresheaf R).map ψ
U : Cᵒᵖ
r : ↑(R.obj U)
m : ↑(M.obj U)
⊢ r • (ConcreteCategory.hom (ψ.app U)) m =
    (ConcreteCategory.hom (cR.ι.app U)) r • (ConcreteCategory.hom (((toPresheaf R).map ψ).app U)) m
Module: Mathlib.CategoryTheory.Adjunction.CompositionIso

Goal state before:
pp: C₀ : Type u_1
C₁ : Type u_2
C₂ : Type u_3
inst✝² : Category.{v_1, u_1} C₀
inst✝¹ : Category.{v_2, u_2} C₁
inst✝ : Category.{v_3, u_3} C₂
F₀₁ : C₀ ⥤ C₁
F₁₂ : C₁ ⥤ C₂
F₀₂ : C₀ ⥤ C₂
G₁₀ : C₁ ⥤ C₀
G₂₁ : C₂ ⥤ C₁
G₂₀ : C₂ ⥤ C₀
adj₀₁ : F₀₁ ⊣ G₁₀
adj₁₂ : F₁₂ ⊣ G₂₁
adj₀₂ : F₀₂ ⊣ G₂₀
e₀₁₂ : G₂₁ ⋙ G₁₀ ≅ G₂₀
⊢ (conjugateEquiv (adj₀₁.comp adj₁₂) adj₀₂) (adj₀₁.leftAdjointCompIso adj₁₂ adj₀₂ e₀₁₂).inv = e₀₁₂.hom

Tactic:
dsimp only [leftAdjointCompIso]
  simp

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
X₁✝ Y₁✝ X₂✝ Y₂✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
x✝¹ : X₁✝ ⟶ Y₁✝
x✝ : X₂✝ ⟶ Y₂✝
X✝ : Cᵒᵖ
⊢ (x✝¹ ⊗ₘ x✝).app X✝ = (x✝¹ ▷ X₂✝ ≫ Y₁✝ ◁ x✝).app X✝

Tactic:
apply tensorHom_def

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
x✝¹ x✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X✝ : Cᵒᵖ
⊢ (𝟙 x✝¹ ⊗ₘ 𝟙 x✝).app X✝ = (𝟙 (x✝¹ ⊗ x✝)).app X✝

Tactic:
apply id_tensorHom_id

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Grothendieck

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
S✝ R : Sieve X
J : GrothendieckTopology C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
S : J.Cover X
P : Cᵒᵖ ⥤ D
inst✝ : Limits.HasMultiequalizer (S.index P)
⊢ ∀ (b : S.shape.R), P.map (S.shape.fst b).f.op ≫ (S.index P).fst b = P.map (S.shape.snd b).f.op ≫ (S.index P).snd b

Tactic:
intro I
      dsimp only [shape, index, Relation.fst, Relation.snd]
      simp only [← P.map_comp, ← op_comp, I.r.w]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
u : Y ⟶ X
⊢ (singleton u).uncurry = {⟨Y, u⟩}

Tactic:
by
  ext ⟨Z, v⟩; constructor
  · rintro ⟨⟩; rfl
  · intro h
    rw [Set.mem_singleton_iff, Sigma.ext_iff] at h
    obtain ⟨rfl, h⟩ := h; subst h; constructor

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
s : Presieve X
t : ⦃Y : C⦄ → (f : Y ⟶ X) → s f → Presieve Y
Z : C
v : Z ⟶ X
⊢ ⟨Z, v⟩ ∈ (s.bind t).uncurry →
    ∃ i, ∃ (h : i ∈ s.uncurry), ∃ x ∈ (t i.snd ⋯).uncurry, Sigma.map id (fun Z g ↦ g ≫ i.snd) x = ⟨Z, v⟩

pp: case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
s : Presieve X
t : ⦃Y : C⦄ → (f : Y ⟶ X) → s f → Presieve Y
Z : C
v : Z ⟶ X
⊢ (∃ i, ∃ (h : i ∈ s.uncurry), ∃ x ∈ (t i.snd ⋯).uncurry, Sigma.map id (fun Z g ↦ g ≫ i.snd) x = ⟨Z, v⟩) →
    ⟨Z, v⟩ ∈ (s.bind t).uncurry

Tactic:
· rintro ⟨Y, g, f, hf, ht, hv⟩
    exact ⟨⟨_, f⟩, hf, ⟨_, g⟩, ht, Sigma.ext rfl (heq_of_eq hv)⟩

Goal state after:
case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
s : Presieve X
t : ⦃Y : C⦄ → (f : Y ⟶ X) → s f → Presieve Y
Z : C
v : Z ⟶ X
⊢ (∃ i, ∃ (h : i ∈ s.uncurry), ∃ x ∈ (t i.snd ⋯).uncurry, Sigma.map id (fun Z g ↦ g ≫ i.snd) x = ⟨Z, v⟩) →
    ⟨Z, v⟩ ∈ (s.bind t).uncurry
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
R : Presieve X
inst✝ : R.HasPullbacks f
⊢ generate (Presieve.pullbackArrows f R) = pullback f (generate R)

Tactic:
ext W g

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
R : Presieve X
inst✝ : R.HasPullbacks f
W : C
g : W ⟶ Y
⊢ (generate (Presieve.pullbackArrows f R)).arrows g ↔ (pullback f (generate R)).arrows g
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
t : P.obj (op X)
ht : x.IsAmalgamation t
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : R f₁
h₂ : R f₂
comm : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ (ConcreteCategory.hom (P.map g₁.op)) (x f₁ h₁) = (ConcreteCategory.hom (P.map g₂.op)) (x f₂ h₂)

Tactic:
← ht _ h₁,

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
t : P.obj (op X)
ht : x.IsAmalgamation t
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : R f₁
h₂ : R f₂
comm : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ (ConcreteCategory.hom (P.map g₁.op)) ((ConcreteCategory.hom (P.map f₁.op)) t) =
    (ConcreteCategory.hom (P.map g₂.op)) (x f₂ h₂)
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
s : Presieve X
Y✝ : D
f✝ : Y✝ ⟶ F.obj X
⊢ Presieve.functorPushforward F s f✝ ↔ (functorPushforward F (generate s)).arrows f✝

Tactic:
simp [functorPushforward_extend_eq]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case mpr.a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
h : IsSeparatedFor P (generate R).arrows
x : FamilyOfElements P R
t₁ t₂ : P.obj (op X)
ht₁ : x.IsAmalgamation t₁
ht₂ : x.IsAmalgamation t₂
⊢ x.sieveExtend.IsAmalgamation t₂

Tactic:
· exact isAmalgamation_sieveExtend x t₂ ht₂

Goal state after:
Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Goal state before:
pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type t
inst✝¹ : Small.{w, t} I
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).HasPairwisePullbacks
x : (i : I) → P.obj (op (X i))
b✝ : Arrows.Compatible P π x
t : P.obj (op B)
⊢ (equivShrink ((j : I) → P.obj (op (X j)))).symm
        ((Types.Small.productIso fun i ↦ P.obj (op (X i))).toEquiv ((ConcreteCategory.hom (forkMap P X π)) t)) =
      x →
    ∀ (i : I), (ConcreteCategory.hom (P.map (π i).op)) t = x i

Tactic:
intro q i
    rw [← q]
    simp [Iso.toEquiv, forkMap]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁴ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝² : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
Y X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : Meq P S
f : Y ⟶ X
i : (S.pullback f).Arrow
⊢ (ConcreteCategory.hom (Multiequalizer.ι (S.index P) i.base)) ((Meq.equiv P S).symm x) =
    ↑x { Y := i.Y, f := i.f ≫ f, hf := ⋯ }

Tactic:
dsimp% Meq.equiv_symm_eq_apply x i.base

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁴ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝³ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝² : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
Y X : C
P : Cᵒᵖ ⥤ D
S : J.Cover X
x : Meq P S
f : Y ⟶ X
i : (S.pullback f).Arrow
⊢ ↑x i.base = ↑x { Y := i.Y, f := i.f ≫ f, hf := ⋯ }