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

Goal state before:
pp: case inr
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
S : Type u_2
inst✝² : CommRing S
inst✝¹ : LinearOrder S
inst✝ : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun i j ↦ A i j < 0
h2 : ∀ (j : n), 0 < ∑ i, A i j
h✝ : Nonempty n
⊢ A.det ≠ 0

Tactic:
contrapose! h2

Goal state after:
case inr
n : Type u_1
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
S : Type u_2
inst✝² : CommRing S
inst✝¹ : LinearOrder S
inst✝ : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun i j ↦ A i j < 0
h✝ : Nonempty n
h2 : A.det = 0
⊢ ∃ j, ∑ i, A i j ≤ 0
Module: Mathlib.Algebra.Ring.Associator

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
h : mulLeft₃ = mulRight₃
x y z : R
⊢ ((mulLeft₃ x) y) z = x * (y * z)

Tactic:
← mulRight₃_apply,

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocSemiring R
h : mulLeft₃ = mulRight₃
x y z : R
⊢ ((mulLeft₃ x) y) z = ((mulRight₃ x) y) z
Module: Mathlib.Algebra.DirectSum.Algebra

Goal state before:
pp: ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : ι) → AddCommMonoid (A i)
inst✝⁶ : (i : ι) → Module R (A i)
inst✝⁵ : AddMonoid ι
inst✝⁴ : GSemiring A
inst✝³ : Semiring B
inst✝² : GAlgebra R A
inst✝¹ : Algebra R B
inst✝ : DecidableEq ι
f : (i : ι) → A i →ₗ[R] B
hone : (f 0) GradedMonoid.GOne.one = 1
hmul : ∀ {i j : ι} (ai : A i) (aj : A j), (f (i + j)) (GradedMonoid.GMul.mul ai aj) = (f i) ai * (f j) aj
r : R
⊢ (toModule R ι B f) ((algebraMap R (⨁ (i : ι), A i)) r) = (algebraMap R B) r

Tactic:
Algebra.algebraMap_eq_smul_one,

Goal state after:
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : ι) → AddCommMonoid (A i)
inst✝⁶ : (i : ι) → Module R (A i)
inst✝⁵ : AddMonoid ι
inst✝⁴ : GSemiring A
inst✝³ : Semiring B
inst✝² : GAlgebra R A
inst✝¹ : Algebra R B
inst✝ : DecidableEq ι
f : (i : ι) → A i →ₗ[R] B
hone : (f 0) GradedMonoid.GOne.one = 1
hmul : ∀ {i j : ι} (ai : A i) (aj : A j), (f (i + j)) (GradedMonoid.GMul.mul ai aj) = (f i) ai * (f j) aj
r : R
⊢ (toModule R ι B f) (r • 1) = (algebraMap R B) r
Module: Mathlib.Algebra.DirectSum.Algebra

Goal state before:
pp: ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : ι) → AddCommMonoid (A i)
inst✝⁶ : (i : ι) → Module R (A i)
inst✝⁵ : AddMonoid ι
inst✝⁴ : GSemiring A
inst✝³ : Semiring B
inst✝² : GAlgebra R A
inst✝¹ : Algebra R B
inst✝ : DecidableEq ι
f : (i : ι) → A i →ₗ[R] B
hone : (f 0) GradedMonoid.GOne.one = 1
hmul : ∀ {i j : ι} (ai : A i) (aj : A j), (f (i + j)) (GradedMonoid.GMul.mul ai aj) = (f i) ai * (f j) aj
r : R
⊢ (toModule R ι B f) (r • 1) = (algebraMap R B) r

Tactic:
Algebra.algebraMap_eq_smul_one,

Goal state after:
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst✝⁸ : CommSemiring R
inst✝⁷ : (i : ι) → AddCommMonoid (A i)
inst✝⁶ : (i : ι) → Module R (A i)
inst✝⁵ : AddMonoid ι
inst✝⁴ : GSemiring A
inst✝³ : Semiring B
inst✝² : GAlgebra R A
inst✝¹ : Algebra R B
inst✝ : DecidableEq ι
f : (i : ι) → A i →ₗ[R] B
hone : (f 0) GradedMonoid.GOne.one = 1
hmul : ∀ {i j : ι} (ai : A i) (aj : A j), (f (i + j)) (GradedMonoid.GMul.mul ai aj) = (f i) ai * (f j) aj
r : R
⊢ (toModule R ι B f) (r • 1) = r • 1
Module: Mathlib.Algebra.DirectSum.Ring

Goal state before:
pp: ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddCommMonoid ι
inst✝ : GCommSemiring A
a b : ⨁ (i : ι), A i
⊢ a * b = b * a

Tactic:
by
  suffices mulHom A = (mulHom A).flip by
    rw [← mulHom_apply, this, AddMonoidHom.flip_apply, mulHom_apply]
  apply addHom_ext; intro ai ax; apply addHom_ext; intro bi bx
  rw [AddMonoidHom.flip_apply, mulHom_of_of, mulHom_of_of]
  exact of_eq_of_gradedMonoid_eq (GCommSemiring.mul_comm ⟨ai, ax⟩ ⟨bi, bx⟩)

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

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
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
m : M
⊢ (liftAlternating f) ((ι R) m) = (f 1) ![m]

Tactic:
dsimp [liftAlternating]
  rw [foldl_ι, LinearMap.mk₂_apply, AlternatingMap.curryLeft_apply_apply]
  congr!

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

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
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
r : R
⊢ (liftAlternating f) ((algebraMap R (ExteriorAlgebra R M)) r) = r • (f 0) 0

Tactic:
Algebra.algebraMap_eq_smul_one,

Goal state after:
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
f : (i : ℕ) → M [⋀^Fin i]→ₗ[R] N
r : R
⊢ (liftAlternating f) (r • 1) = r • (f 0) 0
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: case a.refine_2
R : Type u
inst✝² : CommRing R
n : ℕ
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
hs : span R s = ⊤
f : Fin n → ↑(⇑(ExteriorAlgebra.ι R) '' s)
hx : (List.ofFn fun i ↦ ↑(f i)).prod ∈ (⇑(ExteriorAlgebra.ι R) '' s) ^ n
⊢ (List.ofFn fun i ↦ (ExteriorAlgebra.ι R) ((⇑ExteriorAlgebra.ιInv ∘ Subtype.val ∘ f) i)).prod =
    (List.ofFn fun i ↦ ↑(f i)).prod

Tactic:
apply congrArg (List.prod ∘ List.ofFn)

Goal state after:
case a.refine_2
R : Type u
inst✝² : CommRing R
n : ℕ
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
hs : span R s = ⊤
f : Fin n → ↑(⇑(ExteriorAlgebra.ι R) '' s)
hx : (List.ofFn fun i ↦ ↑(f i)).prod ∈ (⇑(ExteriorAlgebra.ι R) '' s) ^ n
⊢ (fun i ↦ (ExteriorAlgebra.ι R) ((⇑ExteriorAlgebra.ιInv ∘ Subtype.val ∘ f) i)) = fun i ↦ ↑(f i)
Module: Mathlib.CategoryTheory.Abelian.Injective.Dimension

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
n : ℕ
h : injectiveDimension X < ↑n
this : injectiveDimension X ∈ {n | ∀ (i : ℕ), n < ↑i → HasInjectiveDimensionLT X i}
⊢ HasInjectiveDimensionLT X n

Tactic:
simp only [Set.mem_ofPred_eq] at this

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
n : ℕ
h : injectiveDimension X < ↑n
this : ∀ (i : ℕ), injectiveDimension X < ↑i → HasInjectiveDimensionLT X i
⊢ HasInjectiveDimensionLT X n
Module: Mathlib.Algebra.Category.ModuleCat.LeftResolution

Goal state before:
pp: R : Type u
inst✝ : Ring R
X : Type u
M N : ModuleCat R
f : (free R).obj X ⟶ N
p : M ⟶ N
hp : Epi p
⊢ ∃ f', f' ≫ p = f

Tactic:
epi_iff_surjective

Goal state after:
R : Type u
inst✝ : Ring R
X : Type u
M N : ModuleCat R
f : (free R).obj X ⟶ N
p : M ⟶ N
hp : Function.Surjective ⇑(ConcreteCategory.hom p)
⊢ ∃ f', f' ≫ p = f
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
N' : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
r : R
⊢ Fin 0 → M

Tactic:
rintro ⟨i, hi⟩

Goal state after:
R : Type u
inst✝⁶ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
N' : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
r : R
i : ℕ
hi : i < 0
⊢ M
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
j j' : J
f : j ⟶ j'
⊢ ((Functor.const J).obj (limitPresheafOfModules F)).map f ≫
      { app := fun X ↦ limit.π (F ⋙ evaluation R X) j', naturality := ⋯ } =
    { app := fun X ↦ limit.π (F ⋙ evaluation R X) j, naturality := ⋯ } ≫ F.map f

Tactic:
ext1 X
        simpa using (limit.w (F ⋙ evaluation R X) f).symm

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

Goal state before:
pp: R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M₁ M₂ : ModuleCat S
m₁ : ↑M₁
m₂ : ↑M₂
⊢ (ConcreteCategory.hom (μ (restrictScalars f) M₁ M₂)) (m₁ ⊗ₜ[R] m₂) = m₁ ⊗ₜ[S] m₂

Tactic:
by
  dsimp [Adjunction.rightAdjointLaxMonoidal_μ]
  rw [extendRestrictScalarsAdj_homEquiv_apply]
  dsimp
  rw [extendScalars_δ_tmul, tensorHom_tmul,
    extendRestrictScalarsAdj_counit_app_apply_one_tmul,
    extendRestrictScalarsAdj_counit_app_apply_one_tmul]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimit (constPUnitFunctor C)
⊢ IsConnected C ↔ Nonempty (colimit (constPUnitFunctor C) ≅ PUnit.{w + 1})

Tactic:
refine ⟨fun _ => ⟨colimitConstPUnitIsoPUnit.{w} C⟩, fun ⟨h⟩ => ?_⟩

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimit (constPUnitFunctor C)
x✝ : Nonempty (colimit (constPUnitFunctor C) ≅ PUnit.{w + 1})
h : colimit (constPUnitFunctor C) ≅ PUnit.{w + 1}
⊢ IsConnected C
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M₁ M₂ : PresheafOfModules R
f : M₁ ⟶ M₂
inst✝ : Mono f
X : Cᵒᵖ
⊢ Function.Injective ⇑(ConcreteCategory.hom (f.app X))

Tactic:
by
  rw [← ModuleCat.mono_iff_injective]
  infer_instance

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
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (uncurry.obj F)
P : IsColimit c
s : Cocone D.coconePoints
j : J
k : K
j' : J
k' : K
fj : (j, k).1 ⟶ (j', k').1
fk : (j, k).2 ⟶ (j', k').2
w : (D.obj j).ι.app k ≫ (D.map fj).hom = (F.map fj).app k ≫ (D.obj j').ι.app k
n : (D.map fj).hom ≫ s.ι.app j' = s.ι.app j
⊢ (((D.obj j).ι.app k ≫ (D.map fj).hom) ≫ 𝟙 (D.obj j').pt) ≫ s.ι.app j' = (D.obj j).ι.app k ≫ s.ι.app j ≫ 𝟙 s.pt

Tactic:
rw [← n]

Goal state after:
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
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (uncurry.obj F)
P : IsColimit c
s : Cocone D.coconePoints
j : J
k : K
j' : J
k' : K
fj : (j, k).1 ⟶ (j', k').1
fk : (j, k).2 ⟶ (j', k').2
w : (D.obj j).ι.app k ≫ (D.map fj).hom = (F.map fj).app k ≫ (D.obj j').ι.app k
n : (D.map fj).hom ≫ s.ι.app j' = s.ι.app j
⊢ (((D.obj j).ι.app k ≫ (D.map fj).hom) ≫ 𝟙 (D.obj j').pt) ≫ s.ι.app j' =
    (D.obj j).ι.app k ≫ ((D.map fj).hom ≫ s.ι.app j') ≫ 𝟙 s.pt
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'
N : ModuleCat ↑cR.pt
f : M ⟶ M'
g : M' ⟶ (constFunctor cR).obj N
⊢ (homEquiv hcR hcM) ((homEquiv hcR hcM).symm (f ≫ g)) =
    (homEquiv hcR hcM) (ModuleCat.ofHom (map hcR hcM hcM' f) ≫ (homEquiv hcR hcM').symm g)

Tactic:
obtain ⟨g, rfl⟩ := (homEquiv hcR hcM').surjective g

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'
N : ModuleCat ↑cR.pt
f : M ⟶ M'
g : ModuleCat.of (↑cR.pt) (ModuleColimit hcR hcM') ⟶ N
⊢ (homEquiv hcR hcM) ((homEquiv hcR hcM).symm (f ≫ (homEquiv hcR hcM') g)) =
    (homEquiv hcR hcM) (ModuleCat.ofHom (map hcR hcM hcM' f) ≫ (homEquiv hcR hcM').symm ((homEquiv hcR hcM') g))
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
F : PresheafOfModules R
G : ModuleCat ↑cR.pt
β : F ⟶ (constFunctor cR).obj G
X : Cᵒᵖ
m : ↑(F.obj X)
⊢ (ConcreteCategory.hom (((colimitAdjunction hcR).homEquiv F G).symm β)) (ιM m) = (ConcreteCategory.hom (β.app X)) m

Tactic:
rw [colimitAdjunction_homEquiv]
  apply homEquiv_symm_apply

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.CompositionIso

Goal state before:
pp: C₀ : Type u_1
C₁ : Type u_2
C₂ : Type u_3
C₃ : Type u_4
inst✝³ : Category.{v_1, u_1} C₀
inst✝² : Category.{v_2, u_2} C₁
inst✝¹ : Category.{v_3, u_3} C₂
inst✝ : Category.{v_4, u_4} C₃
F₀₁ : C₀ ⥤ C₁
F₁₂ : C₁ ⥤ C₂
F₂₃ : C₂ ⥤ C₃
F₀₂ : C₀ ⥤ C₂
F₁₃ : C₁ ⥤ C₃
F₀₃ : C₀ ⥤ C₃
G₁₀ : C₁ ⥤ C₀
G₂₁ : C₂ ⥤ C₁
G₃₂ : C₃ ⥤ C₂
G₂₀ : C₂ ⥤ C₀
G₃₁ : C₃ ⥤ C₁
G₃₀ : C₃ ⥤ C₀
adj₀₁ : F₀₁ ⊣ G₁₀
adj₁₂ : F₁₂ ⊣ G₂₁
adj₂₃ : F₂₃ ⊣ G₃₂
adj₀₂ : F₀₂ ⊣ G₂₀
adj₁₃ : F₁₃ ⊣ G₃₁
adj₀₃ : F₀₃ ⊣ G₃₀
e₀₁₂ : G₂₁ ⋙ G₁₀ ≅ G₂₀
e₁₂₃ : G₃₂ ⋙ G₂₁ ≅ G₃₁
e₀₁₃ : G₃₁ ⋙ G₁₀ ≅ G₃₀
e₀₂₃ : G₃₂ ⋙ G₂₀ ≅ G₃₀
h : G₃₂.isoWhiskerLeft e₀₁₂ ≪≫ e₀₂₃ = (G₃₂.associator G₂₁ G₁₀).symm ≪≫ isoWhiskerRight e₁₂₃ G₁₀ ≪≫ e₀₁₃
⊢ F₀₁.isoWhiskerLeft (adj₁₂.leftAdjointCompIso adj₂₃ adj₁₃ e₁₂₃) ≪≫ adj₀₁.leftAdjointCompIso adj₁₃ adj₀₃ e₀₁₃ =
    (F₀₁.associator F₁₂ F₂₃).symm ≪≫
      isoWhiskerRight (adj₀₁.leftAdjointCompIso adj₁₂ adj₀₂ e₀₁₂) F₂₃ ≪≫ adj₀₂.leftAdjointCompIso adj₂₃ adj₀₃ e₀₂₃

Tactic:
by
  ext : 1
  exact leftAdjointCompNatTrans_assoc _ _ _ _ _ _ _ _ _ _
    (by simpa using congr_arg Iso.inv h)

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
J : GrothendieckTopology C
X : C
S : Presieve X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → S f → Presieve Y
hS : S ∈ {R | Sieve.generate R ∈ J X}
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : S f), Ti f H ∈ {R | Sieve.generate R ∈ J Y}
Y Z : C
g : Y ⟶ Z
f : Z ⟶ X
hf : S f
⊢ Sieve.pullback (g ≫ f) (Sieve.generate (S.bind Ti)) ∈ J Y

Tactic:
rw [Sieve.pullback_comp]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
J : GrothendieckTopology C
X : C
S : Presieve X
Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → S f → Presieve Y
hS : S ∈ {R | Sieve.generate R ∈ J X}
hTi : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : S f), Ti f H ∈ {R | Sieve.generate R ∈ J Y}
Y Z : C
g : Y ⟶ Z
f : Z ⟶ X
hf : S f
⊢ Sieve.pullback g (Sieve.pullback f (Sieve.generate (S.bind Ti))) ∈ J Y
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
⊢ ∀ (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

Goal state after:
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
I : S.shape.R
⊢ P.map (S.shape.fst I).f.op ≫ (S.index P).fst I = P.map (S.shape.snd I).f.op ≫ (S.index P).snd I
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

Goal state after:
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)
I : S.shape.R
⊢ P.map (S.shape.fst I).f.op ≫ (S.index P).fst I = P.map (S.shape.snd I).f.op ≫ (S.index P).snd I
Module: Mathlib.CategoryTheory.Sites.SheafOfTypes

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
H : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
⊢ ∀ (s : Cocone S.arrows.diagram) (j : S.arrows.category), S.arrows.cocone.ι.app j ≫ Exists.choose ⋯ = s.ι.app j

Tactic:
intro s

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
H : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
s : Cocone S.arrows.diagram
⊢ ∀ (j : S.arrows.category), S.arrows.cocone.ι.app j ≫ Exists.choose ⋯ = s.ι.app j
Module: Mathlib.CategoryTheory.Sites.SheafOfTypes

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
H : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
⊢ ∀ (s : Cocone S.arrows.diagram) (m : S.arrows.cocone.pt ⟶ s.pt),
    (∀ (j : S.arrows.category), S.arrows.cocone.ι.app j ≫ m = s.ι.app j) → m = Exists.choose ⋯

Tactic:
intro s

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : C
S : Sieve X
H : ∀ (W : C), IsSheafFor (yoneda.obj W) S.arrows
s : Cocone S.arrows.diagram
⊢ ∀ (m : S.arrows.cocone.pt ⟶ s.pt),
    (∀ (j : S.arrows.category), S.arrows.cocone.ι.app j ≫ m = s.ι.app j) → m = Exists.choose ⋯
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
S : C
R : Presieve S
⊢ R ≤ ofArrows (fun f ↦ f.obj.left) fun f ↦ f.obj.hom

Tactic:
rintro X g hg

Goal state after:
case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
S : C
R : Presieve S
X : C
g : X ⟶ S
hg : R g
⊢ ofArrows (fun f ↦ f.obj.left) (fun f ↦ f.obj.hom) g
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
R : Presieve X
x : FamilyOfElements P R
t : x.Compatible
f : Y ⟶ X
hf : R f
h : ∃ h g, R g ∧ h ≫ g = f
⊢ x.sieveExtend f ⋯ = x f hf

Tactic:
unfold FamilyOfElements.sieveExtend

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
R : Presieve X
x : FamilyOfElements P R
t : x.Compatible
f : Y ⟶ X
hf : R f
h : ∃ h g, R g ∧ h ≫ g = f
⊢ (ConcreteCategory.hom (P.map ⋯.choose.op)) (x ⋯.choose ⋯) = x f hf
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X✝ : C
R : Sieve X✝
S : Sieve (F.obj X✝)
hle : R ≤ functorPullback F S
Y : D
X : C
g : X ⟶ X✝
h : Y ⟶ F.obj X
hg : R.arrows g
⊢ S.arrows (F.map g)

Tactic:
exact hle g hg

Goal state after:
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
X : C
S : Sieve X
e : C ≌ D
Y : D
iYX : Y ⟶ e.functor.obj X
H : (functorPullback e.inverse (pullback (e.unitInv.app X) S)).arrows iYX
⊢ S.arrows (e.inverse.map iYX ≫ e.unitInv.app X)

Tactic:
by simpa using H

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))ᵒᵖ
⊢ colimit.ι (J.diagram P (unop X)) S ≫
      colimMap (J.diagramPullback P (g.unop ≫ f.unop)) ≫
        colimit.pre (J.diagram P (unop Z)) (J.pullback (g.unop ≫ f.unop)).op =
    colimit.ι (J.diagram P (unop X)) S ≫
      (colimMap (J.diagramPullback P f.unop) ≫ colimit.pre (J.diagram P (unop Y)) (J.pullback f.unop).op) ≫
        colimMap (J.diagramPullback P g.unop) ≫ colimit.pre (J.diagram P (unop Z)) (J.pullback g.unop).op

Tactic:
simp only [diagramPullback_app, colimit.ι_pre_assoc, colimit.ι_pre, ι_colimMap_assoc,
      Category.assoc]

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))ᵒᵖ
⊢ Multiequalizer.lift ((unop ((J.pullback (g.unop ≫ f.unop)).op.obj S)).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)) ((J.pullback (g.unop ≫ f.unop)).op.obj S) =
    Multiequalizer.lift ((unop ((J.pullback f.unop).op.obj S)).index P) ((J.diagram P (unop X)).obj S)
        (fun I ↦ Multiequalizer.ι ((unop S).index P) (Cover.Arrow.base I)) ⋯ ≫
      Multiequalizer.lift ((unop ((J.pullback g.unop).op.obj ((J.pullback f.unop).op.obj S))).index P)
          ((J.diagram P (unop Y)).obj ((J.pullback f.unop).op.obj S))
          (fun I ↦ Multiequalizer.ι ((unop ((J.pullback f.unop).op.obj S)).index P) (Cover.Arrow.base I)) ⋯ ≫
        colimit.ι (J.diagram P (unop Z)) ((J.pullback g.unop).op.obj ((J.pullback f.unop).op.obj S))
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
P' : Cᵒᵖ ⥤ Type w
i : P ≅ P'
hP : IsSeparatedFor P R
x : FamilyOfElements P' R
t₁ t₂ : P'.obj (op X)
ht₁ : x.IsAmalgamation t₁
ht₂ : x.IsAmalgamation t₂
⊢ t₁ = t₂

Tactic:
simpa using congrArg (i.hom.app _) <| hP (x.map i.inv) _ _ (ht₁.map i.inv) (ht₂.map i.inv)

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
A' : Type u₂
inst✝¹ : Category.{max v₁ u₁, u₂} A'
B : Type u₃
inst✝ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
P' : Cᵒᵖ ⥤ A'
X : C
S : J.Cover X
hP : IsSheaf J P
E : Multifork (S.index P)
m : E.pt ⟶ (S.multifork P).pt
hm : ∀ (j : WalkingMulticospan S.shape), m ≫ (S.multifork P).π.app j = E.π.app j
⊢ ∀ (I : S.Arrow), m ≫ P.map I.f.op = hP.amalgamate S (fun x ↦ E.ι x) ⋯ ≫ P.map I.f.op

Tactic:
intro I

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
A' : Type u₂
inst✝¹ : Category.{max v₁ u₁, u₂} A'
B : Type u₃
inst✝ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U : C
R : Presieve U
P : Cᵒᵖ ⥤ A
P' : Cᵒᵖ ⥤ A'
X : C
S : J.Cover X
hP : IsSheaf J P
E : Multifork (S.index P)
m : E.pt ⟶ (S.multifork P).pt
hm : ∀ (j : WalkingMulticospan S.shape), m ≫ (S.multifork P).π.app j = E.π.app j
I : S.Arrow
⊢ m ≫ P.map I.f.op = hP.amalgamate S (fun x ↦ E.ι x) ⋯ ≫ P.map I.f.op
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : Type u₂
inst✝¹ : Category.{v₂, u₂} A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
inst✝ : ∀ (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
⊢ IsSheaf J P ↔ ∀ (X : C) (S : J.Cover X), IsIso (S.toMultiequalizer P)

Tactic:
isSheaf_iff_multifork

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
A : Type u₂
inst✝¹ : Category.{v₂, u₂} A
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
inst✝ : ∀ (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
⊢ (∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork P))) ↔
    ∀ (X : C) (S : J.Cover X), IsIso (S.toMultiequalizer P)