mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.QuadraticForm.Basic

Goal state before:
pp: R : Type u_3
N : Type u_5
n : Type w
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
inst✝³ : CommRing R
inst✝² : Invertible 2
inst✝¹ : AddCommGroup N
inst✝ : Module R N
b : Basis n R N
a : R
Q : QuadraticForm R N
⊢ toMatrix b (a • Q) = a • toMatrix b Q

Tactic:
simp [toMatrix]

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

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
htwo : Invertible 2
B : BilinForm R M
hB₁ : B ≠ 0
hB₂ : IsSymm B
⊢ ∃ x, (B x) x ≠ 0

Tactic:
by
  lift B to QuadraticForm R M using hB₂ with Q
  obtain ⟨x, hx⟩ := QuadraticMap.exists_quadraticMap_ne_zero hB₁
  exact ⟨x, fun h => hx (Q.associated_eq_self_apply ℕ x ▸ h)⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.Curry

Goal state before:
pp: case e_6
R : Type uR
M₂ : Type v₂
M' : Type v'
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M'
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M'
inst✝ : Module R M₂
k l n : ℕ
s : Finset (Fin n)
hk : #s = k
hl : #sᶜ = l
f : MultilinearMap R (fun x ↦ M') (MultilinearMap R (fun x ↦ M') M₂)
x y : M'
⊢ (fun i ↦ s.piecewise (fun x_1 ↦ x) (fun x ↦ y) ((finSumEquivOfFinset hk hl) (Sum.inr i))) = fun x ↦ y

Tactic:
· ext
    rw [finSumEquivOfFinset_inr, Finset.piecewise_eq_of_notMem]
    exact Finset.mem_compl.1 (Finset.orderEmbOfFin_mem _ _ _)

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
this✝ : Module Rᵐᵒᵖ M := Module.compHom M ((RingHom.id R).fromOpposite ⋯)
this : IsCentralScalar R M
hf0 : toTrivSqZeroExt ((ι R) x) = (0, x)
⊢ x = 0 ∧ r = 0

Tactic:
rw [h, AlgHom.commutes] at hf0

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 ⋯)
this : IsCentralScalar R M
hf0 : (algebraMap R (TrivSqZeroExt R M)) r = (0, x)
⊢ x = 0 ∧ r = 0
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup N'
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R N'
⊢ M →ₗ[R] ((i : ℕ) → M [⋀^Fin i]→ₗ[R] N) →ₗ[R] (i : ℕ) → M [⋀^Fin i]→ₗ[R] N

Tactic:
refine
      LinearMap.mk₂ R (fun m f i => (f i.succ).curryLeft m) (fun m₁ m₂ f => ?_) (fun c m f => ?_)
        (fun m f₁ f₂ => ?_) fun c m f => ?_

Goal state after:
case refine_1.refine_1
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup N'
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R N'
m₁ m₂ : M
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
⊢ (fun i ↦ (f i.succ).curryLeft (m₁ + m₂)) = (fun i ↦ (f i.succ).curryLeft m₁) + fun i ↦ (f i.succ).curryLeft m₂

case refine_1.refine_2
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup N'
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R N'
c : R
m : M
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
⊢ (fun i ↦ (f i.succ).curryLeft (c • m)) = c • fun i ↦ (f i.succ).curryLeft m

case refine_1.refine_3
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup N'
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R N'
m : M
f₁ f₂ : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
⊢ (fun i ↦ ((f₁ + f₂) i.succ).curryLeft m) = (fun i ↦ (f₁ i.succ).curryLeft m) + fun i ↦ (f₂ i.succ).curryLeft m

case refine_1.refine_4
R : Type u_1
M : Type u_2
N : Type u_3
N' : Type u_4
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup N'
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R N'
c : R
m : M
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
⊢ (fun i ↦ ((c • f) i.succ).curryLeft m) = c • fun i ↦ (f i.succ).curryLeft m
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
x y : ↑(M F)
⊢ r • (x + y) = r • x + r • y

Tactic:
by
    obtain ⟨i, x, rfl⟩ := M.mk_surjective F x
    obtain ⟨j, y, rfl⟩ := M.mk_surjective F y
    rw [colimit_smul_mk_eq, colimit_smul_mk_eq,
      colimit_add_mk_eq _ ⟨i, _⟩ ⟨j, _⟩ (max' i j) (IsFiltered.leftToMax i j)
      (IsFiltered.rightToMax i j), colimit_smul_mk_eq, smul_add,
      colimit_add_mk_eq _ ⟨i, _⟩ ⟨j, _⟩ (max' i j) (IsFiltered.leftToMax i j)
      (IsFiltered.rightToMax i j), map_smul, map_smul]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
n : ℕ
h : HasInjectiveDimensionLT X (n + 1)
⊢ ↑n < ↑(n + 1)

Tactic:
by simp [ENat.WithBot.lt_add_one_iff]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Small.{v, u} R
M : ModuleCat R
S : Submonoid R
⊢ IsLocalizedModule S (M.localizedModuleMkLinearMap S)

Tactic:
dsimp only [localizedModuleMkLinearMap]
  infer_instance

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
j : J
⊢ { app := fun X ↦ (hc X).lift ((evaluation R X).mapCone s), naturality := ⋯ } ≫ c.π.app j = s.π.app j

Tactic:
ext1 X
    exact (hc X).fac ((evaluation R X).mapCone s) j

Goal state after:
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
X Y : Cᵒᵖ
f : X ⟶ Y
j : J
⊢ ((evaluation R X).mapCocone c).ι.app j ≫
      c.pt.map f ≫
        (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((hc Y).desc ((evaluation R Y).mapCocone s)) =
    ((evaluation R X).mapCocone c).ι.app j ≫ (hc X).desc ((evaluation R X).mapCocone s) ≫ s.pt.map f

Tactic:
(hc X).fac_assoc ((evaluation R X).mapCocone s) j

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 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
X Y : Cᵒᵖ
f : X ⟶ Y
j : J
⊢ ((evaluation R X).mapCocone c).ι.app j ≫
      c.pt.map f ≫
        (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map ((hc Y).desc ((evaluation R Y).mapCocone s)) =
    ((evaluation R X).mapCocone s).ι.app j ≫ s.pt.map f
Module: Mathlib.CategoryTheory.Monoidal.Closed.Cartesian

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
X X' Y Y' Z A B : C
inst✝ : Closed A
I : C
t : IsInitial I
⊢ curry (snd A I) = t.to (A ⟹ I)

Tactic:
apply t.hom_ext

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.Cartesian

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : CartesianMonoidalCategory C
X X' Y Y' Z A B : C
inst✝ : Closed A
I : C
t : IsInitial I
this : snd A I = uncurry (t.to (A ⟹ I))
⊢ t.to (A ⟹ I) ≫ (ihom A).map (t.to (A ⊗ I)) = curry (𝟙 (A ⊗ I))

Tactic:
apply t.hom_ext

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.Cartesian

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CartesianMonoidalCategory C
X X' Y Y' Z A B : C
inst✝² : Closed A
inst✝¹ : BraidedCategory C
I : C
t : IsInitial I
inst✝ : MonoidalClosed C
⊢ (mulZero t).inv ≫ I ◁ default ≫ (mulZero t).hom ≫ t.to B = (mulZero t).inv ≫ uncurry (𝟙 (I ⟹ B))

Tactic:
apply t.hom_ext

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Sifted

Goal state before:
pp: C : Type u
inst✝ : SmallCategory C
h : PreservesFiniteProducts colim
⊢ IsSifted C

Tactic:
have := isSiftedOrEmpty_of_colim_preservesFiniteProducts C

Goal state after:
C : Type u
inst✝ : SmallCategory C
h : PreservesFiniteProducts colim
this : IsSiftedOrEmpty C
⊢ IsSifted C
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case refine_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsFilteredOrEmpty C
d : D
h₁ : ∃ c, Nonempty (d ⟶ F.obj c)
h₂ : ∀ {c : C} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t
this : Nonempty (StructuredArrow d F)
f g : StructuredArrow d F
⊢ ∃ Z x x, True

Tactic:
obtain ⟨c, ⟨t, ht⟩⟩ := h₂ (f.hom ≫ F.map (IsFiltered.leftToMax f.right g.right))
        (g.hom ≫ F.map (IsFiltered.rightToMax f.right g.right))
    refine ⟨.mk (f.hom ≫ F.map (IsFiltered.leftToMax f.right g.right ≫ t)), ?_, ?_, trivial⟩
    · exact StructuredArrow.homMk (IsFiltered.leftToMax _ _ ≫ t) rfl
    · exact StructuredArrow.homMk (IsFiltered.rightToMax _ _ ≫ t) (by simpa using ht.symm)

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : IsFilteredOrEmpty C
T : C ⥤ D
inst✝ : T.Final
Y : D
X : C
⊢ IsConnected (StructuredArrow X (proj Y T))

Tactic:
isConnected_iff_of_equivalence (ofStructuredArrowProjEquivalence T Y X)

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : IsFilteredOrEmpty C
T : C ⥤ D
inst✝ : T.Final
Y : D
X : C
⊢ IsConnected (StructuredArrow Y (Under.forget X ⋙ T))
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case mp
J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsCodirectedOrder J₁
f : J₁ → J₂
hf : Monotone f
h : ∀ (d : J₂), ∃ c, Nonempty (hf.functor.obj c ⟶ d)
right✝ : ∀ {d : J₂} {c : J₁} (s s' : hf.functor.obj c ⟶ d), ∃ c' t, hf.functor.map t ≫ s = hf.functor.map t ≫ s'
j₂ : J₂
j₁ : J₁
φ : hf.functor.obj j₁ ⟶ j₂
⊢ ∃ j₂_1, f j₂_1 ≤ j₂

Tactic:
exact ⟨j₁,leOfHom φ⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Fubini

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝⁴ : Category.{v_1, u_1} J
inst✝³ : Category.{v_2, u_2} K
C : Type u_3
inst✝² : Category.{v_3, u_3} C
G : J × K ⥤ C
inst✝¹ : HasColimitsOfShape K C
inst✝ : HasColimit (curry.obj G ⋙ colim)
j : J
k : K
⊢ colimit.ι ((curry.obj G).obj j) k ≫ colimit.ι (curry.obj G ⋙ colim) j ≫ (colimitIsoColimitCurryCompColim G).inv =
    colimit.ι G (j, k)

Tactic:
simp [colimitIsoColimitCurryCompColim, Trans.simple, colimitUncurryIsoColimitCompColim]

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✝² x✝¹ x✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
⊢ (α_ x✝³ x✝² x✝¹).hom ▷ x✝ ≫ (α_ x✝³ (x✝² ⊗ x✝¹) x✝).hom ≫ x✝³ ◁ (α_ x✝² x✝¹ x✝).hom =
    (α_ (x✝³ ⊗ x✝²) x✝¹ x✝).hom ≫ (α_ x✝³ x✝² (x✝¹ ⊗ x✝)).hom

Tactic:
ext1; apply pentagon

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
⊢ ∀ ⦃X Y : C⦄ ⦃S : Sieve X⦄ (f : Y ⟶ X),
    S ∈ {S | ∀ {Y : C} (f : Y ⟶ X), ∃ Z g, S.arrows (g ≫ f)} →
      Sieve.pullback f S ∈ {S | ∀ {Y_1 : C} (f : Y_1 ⟶ Y), ∃ Z g, S.arrows (g ≫ f)}

Tactic:
intro X Y S h H Z f
    rcases H (f ≫ h) with ⟨W, g, H'⟩
    exact ⟨W, g, by simpa⟩

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
X : C
S : J.Cover X
T : (I : S.Arrow) → J.Cover I.Y
Y : C
f : Y ⟶ X
Z : C
e1 : Y ⟶ Z
e2 : Z ⟶ X
h1 : (↑S).arrows e2
left✝ : ((fun Y f hf ↦ ↑(T { Y := Y, f := f, hf := hf })) Z e2 h1).arrows e1
h3 : e1 ≫ e2 = f
⊢ (↑S).arrows (e1 ≫ e2)

Tactic:
apply Sieve.downward_closed

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : C
S✝ R : Sieve X✝
J : GrothendieckTopology C
X : C
S : J.Cover X
T : (I : S.Arrow) → J.Cover I.Y
Y : C
f : Y ⟶ X
Z : C
e1 : Y ⟶ Z
e2 : Z ⟶ X
h1 : (↑S).arrows e2
left✝ : ((fun Y f hf ↦ ↑(T { Y := Y, f := f, hf := hf })) Z e2 h1).arrows e1
h3 : e1 ≫ e2 = f
⊢ (↑S).arrows e2
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
S : Sieve X
x : FamilyOfElements P S.arrows
h : x.Compatible
Y Z : C
f : Y ⟶ X
g : Z ⟶ Y
hf : S.arrows f
⊢ x (g ≫ f) ⋯ = (ConcreteCategory.hom (P.map g.op)) (x f hf)

Tactic:
simpa using h (𝟙 _) g (S.downward_closed hf g) hf (id_comp _)

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
i : X ⟶ Y
f : Y ⟶ Z
inst✝ : IsIso i
S : Sieve Z
⊢ S.arrows (i ≫ f) ↔ S.arrows f

Tactic:
by
  refine ⟨fun H ↦ ?_, fun H ↦ S.downward_closed H _⟩
  convert! S.downward_closed H (inv i)
  simp

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 (max v u)
X : C
S : Sieve X
x : Presieve.FamilyOfElements P S.arrows
b✝ : x.Compatible
t : P.obj (op X)
q : (firstObjEqFamily P S.arrows).toEquiv ((ConcreteCategory.hom (forkMap P S.arrows)) t) = x
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ (ConcreteCategory.hom (P.map f.op)) t = x f hf

Tactic:
rw [← q]

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
S : Sieve X
x : Presieve.FamilyOfElements P S.arrows
b✝ : x.Compatible
t : P.obj (op X)
q : (firstObjEqFamily P S.arrows).toEquiv ((ConcreteCategory.hom (forkMap P S.arrows)) t) = x
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ (ConcreteCategory.hom (P.map f.op)) t =
    (firstObjEqFamily P S.arrows).toEquiv ((ConcreteCategory.hom (forkMap P S.arrows)) t) f hf
Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.HasPairwisePullbacks
x : Presieve.FamilyOfElements P R
b✝ : x.Compatible
t : P.obj (op X)
q : (firstObjEqFamily P R).toEquiv ((ConcreteCategory.hom (forkMap P R)) t) = x
Y : C
f : Y ⟶ X
hf : R f
⊢ (ConcreteCategory.hom (P.map f.op)) t = x f hf

Tactic:
rw [← q]

Goal state after:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.HasPairwisePullbacks
x : Presieve.FamilyOfElements P R
b✝ : x.Compatible
t : P.obj (op X)
q : (firstObjEqFamily P R).toEquiv ((ConcreteCategory.hom (forkMap P R)) t) = x
Y : C
f : Y ⟶ X
hf : R f
⊢ (ConcreteCategory.hom (P.map f.op)) t = (firstObjEqFamily P R).toEquiv ((ConcreteCategory.hom (forkMap P R)) t) f hf
Module: Mathlib.CategoryTheory.Sites.Plus

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
X : Cᵒᵖ
S : (J.Cover (unop X))ᵒᵖ
e : (unop S).pullback (𝟙 (unop X)) ≅ unop S := (unop S).pullbackId
⊢ Multiequalizer.lift (((unop S).pullback (𝟙 (unop X))).index P) ((J.diagram P (unop X)).obj S)
        (fun I ↦ Multiequalizer.ι ((unop S).index P) (Cover.Arrow.base I)) ⋯ ≫
      colimit.ι (J.diagram P (unop X)) (op ((unop S).pullback (𝟙 (unop X)))) =
    colimit.ι (J.diagram P (unop X)) S

Tactic:
← colimit.w _ e.inv.op,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
X : Cᵒᵖ
S : (J.Cover (unop X))ᵒᵖ
e : (unop S).pullback (𝟙 (unop X)) ≅ unop S := (unop S).pullbackId
⊢ Multiequalizer.lift (((unop S).pullback (𝟙 (unop X))).index P) ((J.diagram P (unop X)).obj S)
        (fun I ↦ Multiequalizer.ι ((unop S).index P) (Cover.Arrow.base I)) ⋯ ≫
      (J.diagram P (unop X)).map e.inv.op ≫ colimit.ι (J.diagram P (unop X)) (op (unop S)) =
    colimit.ι (J.diagram P (unop X)) S
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)
q :
  (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:
rw [← q]

Goal state after:
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)
q :
  (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 =
    (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)) i
Module: Mathlib.CategoryTheory.Sites.Plus

Goal state before:
pp: case e'_2
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
X : Cᵒᵖ
S : (J.Cover (unop X))ᵒᵖ
e : (unop S).pullback (𝟙 (unop X)) ≅ unop S := (unop S).pullbackId
e_1✝ :
  (multiequalizer ((unop S).index P) ⟶ colimit (J.diagram P (unop X))) =
    ((J.diagram P (unop X)).obj S ⟶ colimit (J.diagram P (unop X)))
I : (unop (op (unop S))).shape.L
⊢ Multiequalizer.ι ((unop S).index P) { Y := I.Y, f := I.f ≫ 𝟙 (unop X), hf := ⋯ } =
    Multiequalizer.ι ((unop S).index P) I

Tactic:
cases I

Goal state after:
case e'_2.mk
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
X : Cᵒᵖ
S : (J.Cover (unop X))ᵒᵖ
e : (unop S).pullback (𝟙 (unop X)) ≅ unop S := (unop S).pullbackId
e_1✝ :
  (multiequalizer ((unop S).index P) ⟶ colimit (J.diagram P (unop X))) =
    ((J.diagram P (unop X)).obj S ⟶ colimit (J.diagram P (unop X)))
Y✝ : C
f✝ : Y✝ ⟶ unop X
hf✝ : (↑(unop (op (unop S)))).arrows f✝
⊢ Multiequalizer.ι ((unop S).index P)
      { Y := { Y := Y✝, f := f✝, hf := hf✝ }.Y, f := { Y := Y✝, f := f✝, hf := hf✝ }.f ≫ 𝟙 (unop X), hf := ⋯ } =
    Multiequalizer.ι ((unop S).index P) { Y := Y✝, f := f✝, hf := hf✝ }
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type w
x : FamilyOfElements P (singleton (𝟙 X))
a✝ : x.Compatible
⊢ ∀ (y : P.obj (op X)), (fun t ↦ x.IsAmalgamation t) y → y = x (𝟙 X) ⋯

Tactic:
· intro t ht
    simpa using ht _ (Presieve.singleton_self _)

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
S : (J.Cover (unop X))ᵒᵖ
e : (unop S).pullback (g.unop ≫ f.unop) ≅ ((unop S).pullback f.unop).pullback g.unop :=
  (unop S).pullbackComp g.unop f.unop
⊢ Multiequalizer.lift (((unop S).pullback (g.unop ≫ f.unop)).index P) ((J.diagram P (unop X)).obj S)
        (fun I ↦ Multiequalizer.ι ((unop S).index P) (Cover.Arrow.base I)) ⋯ ≫
      colimit.ι (J.diagram P (unop Z)) (op ((unop S).pullback (g.unop ≫ f.unop))) =
    Multiequalizer.lift (((unop S).pullback f.unop).index P) ((J.diagram P (unop X)).obj S)
        (fun I ↦ Multiequalizer.ι ((unop S).index P) (Cover.Arrow.base I)) ⋯ ≫
      Multiequalizer.lift ((((unop S).pullback f.unop).pullback g.unop).index P)
          ((J.diagram P (unop Y)).obj (op ((unop S).pullback f.unop)))
          (fun I ↦ Multiequalizer.ι (((unop S).pullback f.unop).index P) (Cover.Arrow.base I)) ⋯ ≫
        colimit.ι (J.diagram P (unop Z)) (op (((unop S).pullback f.unop).pullback g.unop))

Tactic:
← colimit.w _ e.inv.op,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
P : Cᵒᵖ ⥤ D
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
X Y Z : Cᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
S : (J.Cover (unop X))ᵒᵖ
e : (unop S).pullback (g.unop ≫ f.unop) ≅ ((unop S).pullback f.unop).pullback g.unop :=
  (unop S).pullbackComp g.unop f.unop
⊢ Multiequalizer.lift (((unop S).pullback (g.unop ≫ f.unop)).index P) ((J.diagram P (unop X)).obj S)
        (fun I ↦ Multiequalizer.ι ((unop S).index P) (Cover.Arrow.base I)) ⋯ ≫
      (J.diagram P (unop Z)).map e.inv.op ≫
        colimit.ι (J.diagram P (unop Z)) (op (((unop S).pullback f.unop).pullback g.unop)) =
    Multiequalizer.lift (((unop S).pullback f.unop).index P) ((J.diagram P (unop X)).obj S)
        (fun I ↦ Multiequalizer.ι ((unop S).index P) (Cover.Arrow.base I)) ⋯ ≫
      Multiequalizer.lift ((((unop S).pullback f.unop).pullback g.unop).index P)
          ((J.diagram P (unop Y)).obj (op ((unop S).pullback f.unop)))
          (fun I ↦ Multiequalizer.ι (((unop S).pullback f.unop).index P) (Cover.Arrow.base I)) ⋯ ≫
        colimit.ι (J.diagram P (unop Z)) (op (((unop S).pullback f.unop).pullback g.unop))
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: case mpr.refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
hP : Presieve.IsSheaf J P
X : Type w
Y : C
S : Sieve Y
hS : S ∈ J Y
z : Presieve.FamilyOfElements (P ⋙ coyoneda.obj (op X)) S.arrows
hz : z.Compatible
⊢ (fun t ↦ z.IsAmalgamation t) (↾fun x ↦ ⋯.amalgamate (fun Z f hf ↦ (ConcreteCategory.hom (z f hf)) x) ⋯)

Tactic:
intro Z f hf

Goal state after:
case mpr.refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
hP : Presieve.IsSheaf J P
X : Type w
Y : C
S : Sieve Y
hS : S ∈ J Y
z : Presieve.FamilyOfElements (P ⋙ coyoneda.obj (op X)) S.arrows
hz : z.Compatible
Z : C
f : Z ⟶ Y
hf : S.arrows f
⊢ (ConcreteCategory.hom ((P ⋙ coyoneda.obj (op X)).map f.op))
      (↾fun x ↦ ⋯.amalgamate (fun Z f hf ↦ (ConcreteCategory.hom (z f hf)) x) ⋯) =
    z f hf