mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case refine_2.hd₁
C : Type u
inst✝² : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i ↦ f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsVanKampenColimit c₁
t₂ : IsVanKampenColimit c₂
inst✝¹ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
inst✝ : HasFiniteCoproducts C
j : Fin (n + 1)
F' : Fin (n + 1) → C
c : Cocone (Discrete.functor F')
α : Discrete.functor F' ⟶ Discrete.functor f
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ (const (Discrete (Fin (n + 1)))).map i
hα : NatTrans.Equifibered α
Hc : IsColimit c
T : C
f₁ : F' 0 ⟶ T
f₂ : (∐ fun j ↦ (Discrete.functor F').obj { as := j.succ }) ⟶ T
⊢ (BinaryCofan.mk (c.ι.app { as := 0 }) (Sigma.desc fun b ↦ c.ι.app { as := b.succ })).inl ≫
      Hc.desc
        (Cofan.mk T fun i ↦
          Fin.cases f₁ (fun i ↦ Sigma.ι (fun j ↦ (Discrete.functor F').obj { as := j.succ }) i ≫ f₂) i) =
    f₁

Tactic:
simp only [Discrete.functor_obj, pair_obj_left, BinaryCofan.mk_pt, Functor.const_obj_obj,
        BinaryCofan.mk_inl, IsColimit.fac, Cofan.mk_pt, Cofan.mk_ι_app,
        Fin.cases_zero]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
this : HasExt C := HasExt.standard C
⊢ Projective X ↔ HasProjectiveDimensionLT X 1

Tactic:
exact ⟨fun _ ↦ inferInstance, fun _ ↦ projective_iff_subsingleton_ext_one.2
    (HasProjectiveDimensionLT.subsingleton X 1 1 (by rfl))⟩

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X Y : C
h : Retract X Y
n : ℕ
inst✝ : HasProjectiveDimensionLT Y n
this : HasExt C := HasExt.standard C
i : ℕ
hi : n ≤ i
T : C
x : Ext X T i
⊢ (Ext.mk₀ (𝟙 X)).comp x ⋯ = 0

Tactic:
← h.retract,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X Y : C
h : Retract X Y
n : ℕ
inst✝ : HasProjectiveDimensionLT Y n
this : HasExt C := HasExt.standard C
i : ℕ
hi : n ≤ i
T : C
x : Ext X T i
⊢ (Ext.mk₀ (h.i ≫ h.r)).comp x ⋯ = 0
Module: Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension

Goal state before:
pp: case succ
R : Type u
inst✝⁴ : Ring R
inst✝³ : Small.{v, u} R
R' : Type u'
inst✝² : Ring R'
inst✝¹ : Small.{v', u'} R'
e : R ≃+* R'
n : ℕ
ih :
  ∀ {M : ModuleCat R} {N : ModuleCat R'} (e' : ↑M ≃ₛₗ[↑e] ↑N) [HasProjectiveDimensionLE M n],
    HasProjectiveDimensionLE N n
M : ModuleCat R
N : ModuleCat R'
e' : ↑M ≃ₛₗ[↑e] ↑N
inst✝ : HasProjectiveDimensionLE M (n + 1)
S : ShortComplex (ModuleCat R) := M.projectiveShortComplex
S' : ShortComplex (ModuleCat R') := N.projectiveShortComplex
S_exact : M.projectiveShortComplex.ShortExact
S'_exact : N.projectiveShortComplex.ShortExact
eR : Shrink.{v, u} R ≃ₛₗ[↑e] Shrink.{v', u'} R' :=
  ((Shrink.linearEquiv R R).trans e.toSemilinearEquiv).trans (Shrink.linearEquiv R' R').symm
e2 : ↑S.X₂ ≃ₛₗ[↑e] ↑S'.X₂ :=
  (Finsupp.mapDomain.linearEquiv (Shrink.{v, u} R) R ↑e').trans (Finsupp.mapRange.linearEquiv eR)
⊢ HasProjectiveDimensionLE N (n + 1)

Tactic:
have comm : S'.g.hom.comp e2.toLinearMap = e'.toLinearMap.comp S.g.hom := by
      ext m r
      simp [S, S', e2, eR, Basis.constr_apply, map_smulₛₗ]

Goal state after:
case succ
R : Type u
inst✝⁴ : Ring R
inst✝³ : Small.{v, u} R
R' : Type u'
inst✝² : Ring R'
inst✝¹ : Small.{v', u'} R'
e : R ≃+* R'
n : ℕ
ih :
  ∀ {M : ModuleCat R} {N : ModuleCat R'} (e' : ↑M ≃ₛₗ[↑e] ↑N) [HasProjectiveDimensionLE M n],
    HasProjectiveDimensionLE N n
M : ModuleCat R
N : ModuleCat R'
e' : ↑M ≃ₛₗ[↑e] ↑N
inst✝ : HasProjectiveDimensionLE M (n + 1)
S : ShortComplex (ModuleCat R) := M.projectiveShortComplex
S' : ShortComplex (ModuleCat R') := N.projectiveShortComplex
S_exact : M.projectiveShortComplex.ShortExact
S'_exact : N.projectiveShortComplex.ShortExact
eR : Shrink.{v, u} R ≃ₛₗ[↑e] Shrink.{v', u'} R' :=
  ((Shrink.linearEquiv R R).trans e.toSemilinearEquiv).trans (Shrink.linearEquiv R' R').symm
e2 : ↑S.X₂ ≃ₛₗ[↑e] ↑S'.X₂ :=
  (Finsupp.mapDomain.linearEquiv (Shrink.{v, u} R) R ↑e').trans (Finsupp.mapRange.linearEquiv eR)
comm : Hom.hom S'.g ∘ₛₗ ↑e2 = ↑e' ∘ₛₗ Hom.hom S.g
⊢ HasProjectiveDimensionLE N (n + 1)
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Colimits

Goal state before:
pp: C : Type u'
inst✝⁴ : Category.{v', u'} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝³ : HasWeakSheafify J AddCommGrpCat
inst✝² : J.WEqualsLocallyBijective AddCommGrpCat
K : Type w
inst✝¹ : Category.{w', w} K
inst✝ : HasColimitsOfShape K (PresheafOfModules R.obj)
F : K ⥤ SheafOfModules R
e : F ≅ (F ⋙ forget R) ⋙ PresheafOfModules.sheafification (𝟙 R.obj) :=
  F.isoWhiskerLeft (asIso (PresheafOfModules.sheafificationAdjunction (𝟙 R.obj)).counit).symm
⊢ HasColimit F

Tactic:
exact hasColimit_of_iso e

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

Goal state before:
pp: case mpr.transitive.refine_1
C : Type u_3
inst✝ : Category.{u_2, u_3} C
J : Precoverage C
P : Cᵒᵖ ⥤ Type u_1
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
hS : J.Saturate X R
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → J.Saturate Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X Y : C} {f : Y ⟶ X},
    ∀ R ∈ J.coverings X,
      Presieve.IsSeparatedFor P (Sieve.pullback f (Sieve.generate R)).arrows ∧
        ∀ (x : Presieve.FamilyOfElements P (Sieve.pullback f (Sieve.generate R)).arrows),
          x.Compatible → ∃ t, x.IsAmalgamation t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : Presieve.FamilyOfElements P (Sieve.pullback f R).arrows),
    x.Compatible → ∃ t, x.IsAmalgamation t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), Presieve.IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : Presieve.FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        x.Compatible → ∃ t, x.IsAmalgamation t
⊢ Presieve.IsSeparatedFor P (Sieve.pullback f S).arrows

Tactic:
intro x t₁ t₂ h₁ h₂

Goal state after:
case mpr.transitive.refine_1
C : Type u_3
inst✝ : Category.{u_2, u_3} C
J : Precoverage C
P : Cᵒᵖ ⥤ Type u_1
X✝ : C
S✝ : Sieve X✝
X : C
R S : Sieve X
hS : J.Saturate X R
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → J.Saturate Y (Sieve.pullback f S)
Y : C
f : Y ⟶ X
H :
  ∀ {X Y : C} {f : Y ⟶ X},
    ∀ R ∈ J.coverings X,
      Presieve.IsSeparatedFor P (Sieve.pullback f (Sieve.generate R)).arrows ∧
        ∀ (x : Presieve.FamilyOfElements P (Sieve.pullback f (Sieve.generate R)).arrows),
          x.Compatible → ∃ t, x.IsAmalgamation t
H1 : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSeparatedFor P (Sieve.pullback f R).arrows
H1' :
  ∀ ⦃Y : C⦄ (f : Y ⟶ X) (x : Presieve.FamilyOfElements P (Sieve.pullback f R).arrows),
    x.Compatible → ∃ t, x.IsAmalgamation t
H2 :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f → ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y), Presieve.IsSeparatedFor P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows
H2' :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    R.arrows f →
      ∀ ⦃Y_1 : C⦄ (f_1 : Y_1 ⟶ Y) (x : Presieve.FamilyOfElements P (Sieve.pullback f_1 (Sieve.pullback f S)).arrows),
        x.Compatible → ∃ t, x.IsAmalgamation t
x : Presieve.FamilyOfElements P (Sieve.pullback f S).arrows
t₁ t₂ : P.obj (Opposite.op Y)
h₁ : x.IsAmalgamation t₁
h₂ : x.IsAmalgamation t₂
⊢ t₁ = t₂
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
J : Precoverage C
inst✝¹ : J.HasPullbacks
inst✝ : J.IsStableUnderBaseChange
⊢ J.toCoverage.toGrothendieck = J.toGrothendieck

Tactic:
grind [toGrothendieck_eq_sInf, Coverage.toGrothendieck_eq_sInf,
    Precoverage.toCoverage_le_toCoverage]

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

Goal state before:
pp: C : Type u_2
inst✝ : Category.{v_1, u_2} C
K L : Coverage C
P : Cᵒᵖ ⥤ Type u_1
h : (∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R) ∧ IsSheaf L.toGrothendieck P
⊢ IsSheaf (K ⊔ L).toGrothendieck P

Tactic:
isSheaf_coverage

Goal state after:
C : Type u_2
inst✝ : Category.{v_1, u_2} C
K L : Coverage C
P : Cᵒᵖ ⥤ Type u_1
h : (∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R) ∧ ∀ {X : C}, ∀ R ∈ L.coverings X, IsSheafFor P R
⊢ IsSheaf (K ⊔ L).toGrothendieck P
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: C : Type u_2
inst✝ : Category.{v_1, u_2} C
K L : Coverage C
P : Cᵒᵖ ⥤ Type u_1
h : (∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R) ∧ ∀ {X : C}, ∀ R ∈ L.coverings X, IsSheafFor P R
⊢ IsSheaf (K ⊔ L).toGrothendieck P

Tactic:
isSheaf_coverage

Goal state after:
C : Type u_2
inst✝ : Category.{v_1, u_2} C
K L : Coverage C
P : Cᵒᵖ ⥤ Type u_1
h : (∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R) ∧ ∀ {X : C}, ∀ R ∈ L.coverings X, IsSheafFor P R
⊢ ∀ {X : C}, ∀ R ∈ (K ⊔ L).coverings X, IsSheafFor P R
Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck

Goal state before:
pp: C : Type u_3
inst✝ : Category.{u_2, u_3} C
F : Cᵒᵖ ⥤ Type u_1
S : C
𝒰 𝒱 : PreZeroHypercover S
e : 𝒰 ≅ 𝒱
⊢ Presieve.IsSheafFor F (Sieve.generate 𝒰.presieve₀).arrows ↔ Presieve.IsSheafFor F 𝒱.presieve₀

Tactic:
← Sieve.ofArrows,

Goal state after:
C : Type u_3
inst✝ : Category.{u_2, u_3} C
F : Cᵒᵖ ⥤ Type u_1
S : C
𝒰 𝒱 : PreZeroHypercover S
e : 𝒰 ≅ 𝒱
⊢ Presieve.IsSheafFor F (Sieve.ofArrows 𝒰.X 𝒰.f).arrows ↔ Presieve.IsSheafFor F 𝒱.presieve₀
Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck

Goal state before:
pp: C : Type u_3
inst✝¹ : Category.{u_2, u_3} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
J : GrothendieckTopology C
ι : Type (max u_3 u_2)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ J.toPrecoverage.coverings S
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
⊢ Sieve.generate (Presieve.ofArrows P p₁) ∈ J Y

Tactic:
← Sieve.ofArrows,

Goal state after:
C : Type u_3
inst✝¹ : Category.{u_2, u_3} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
J : GrothendieckTopology C
ι : Type (max u_3 u_2)
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hf : Presieve.ofArrows X f ∈ J.toPrecoverage.coverings S
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
⊢ Sieve.ofArrows P p₁ ∈ J Y
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S : C
E : PreOneHypercover S
c : Cofan E.X
hc : IsColimit c
d : Cofan E.Y'
hd : IsColimit d
F : Cᵒᵖ ⥤ A
⊢ F.map (Cofan.IsColimit.desc hc E.f).op ≫ F.map (Cofan.IsColimit.desc hd fun x ↦ E.p₁ x.snd ≫ c.inj x.fst.1).op =
    F.map (Cofan.IsColimit.desc hc E.f).op ≫ F.map (Cofan.IsColimit.desc hd fun x ↦ E.p₂ x.snd ≫ c.inj x.fst.2).op

Tactic:
simp_rw [← Functor.map_comp, ← op_comp]
    congr 2
    exact Cofan.IsColimit.hom_ext hd _ _ (by simp [E.w])

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
A : Type u_1
inst✝² : Category.{v_1, u_1} A
S : C
E : PreOneHypercover S
c : Cofan E.X
hc : IsColimit c
d : Cofan E.Y'
hd : IsColimit d
F : Cᵒᵖ ⥤ A
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (E.X i)) F
inst✝ : PreservesLimit (Discrete.functor fun i ↦ op (E.Y' i)) F
c' : Fan (E.multicospanIndex F).left := Fan.mk (F.obj (op c.pt)) fun i ↦ F.map (c.inj i).op
hc' : IsLimit c' := isLimitFanMkObjOfIsLimit F (fun i ↦ op (E.X i)) (fun i ↦ (c.inj i).op) (Cofan.IsColimit.op hc)
⊢ IsLimit (E.multifork F) ≃ IsLimit (E.forkOfIsColimit hc hd F)

Tactic:
letI d' : Fan (E.multicospanIndex F).right := Fan.mk _ fun i ↦ F.map (d.inj i).op

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
A : Type u_1
inst✝² : Category.{v_1, u_1} A
S : C
E : PreOneHypercover S
c : Cofan E.X
hc : IsColimit c
d : Cofan E.Y'
hd : IsColimit d
F : Cᵒᵖ ⥤ A
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (E.X i)) F
inst✝ : PreservesLimit (Discrete.functor fun i ↦ op (E.Y' i)) F
c' : Fan (E.multicospanIndex F).left := Fan.mk (F.obj (op c.pt)) fun i ↦ F.map (c.inj i).op
hc' : IsLimit c' := isLimitFanMkObjOfIsLimit F (fun i ↦ op (E.X i)) (fun i ↦ (c.inj i).op) (Cofan.IsColimit.op hc)
d' : Fan (E.multicospanIndex F).right := Fan.mk (F.obj (op d.pt)) fun i ↦ F.map (d.inj i).op
⊢ IsLimit (E.multifork F) ≃ IsLimit (E.forkOfIsColimit hc hd F)
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: case refine_2.refine_1
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
i j : E.I₀ × F.I₀
W : C
p₁ : W ⟶ pullback (E.f i.1) (F.f i.2)
p₂ : W ⟶ pullback (E.f j.1) (F.f j.2)
w : p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) ≫ E.f i.1 = p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) ≫ E.f j.1
Y : C
p : W ⟶ pullback ((E.inter F).f i) ((E.inter F).f j) := pullback.lift p₁ p₂ w
Z : C
a : Y ⟶ Z
b : Z ⟶ W
k : E.I₁ i.1 j.1
e : Z ⟶ E.Y k
h₁ : b ≫ p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) = e ≫ E.p₁ k
h₂ : b ≫ p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) = e ≫ E.p₂ k
l : F.I₁ i.2 j.2
u : Y ⟶ F.Y l
u₁ : (a ≫ b) ≫ p₁ ≫ pullback.snd (E.f i.1) (F.f i.2) = u ≫ F.p₁ l
u₂ : (a ≫ b) ≫ p₂ ≫ pullback.snd (E.f j.1) (F.f j.2) = u ≫ F.p₂ l
x✝ :
  (Sieve.bind (E.sieve₁ (p₁ ≫ pullback.fst (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.fst (E.f j.1) (F.f j.2))).arrows
        fun x f x_1 ↦
        Sieve.pullback f
          (F.sieve₁ (p₁ ≫ pullback.snd (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.snd (E.f j.1) (F.f j.2)))).arrows
    (a ≫ b)
⊢ (a ≫ e) ≫ E.p₁ (k, l).1 ≫ E.f i.1 = u ≫ F.p₁ (k, l).2 ≫ F.f i.2

Tactic:
simp only [Category.assoc] at u₁

Goal state after:
case refine_2.refine_1
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
i j : E.I₀ × F.I₀
W : C
p₁ : W ⟶ pullback (E.f i.1) (F.f i.2)
p₂ : W ⟶ pullback (E.f j.1) (F.f j.2)
w : p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) ≫ E.f i.1 = p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) ≫ E.f j.1
Y : C
p : W ⟶ pullback ((E.inter F).f i) ((E.inter F).f j) := pullback.lift p₁ p₂ w
Z : C
a : Y ⟶ Z
b : Z ⟶ W
k : E.I₁ i.1 j.1
e : Z ⟶ E.Y k
h₁ : b ≫ p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) = e ≫ E.p₁ k
h₂ : b ≫ p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) = e ≫ E.p₂ k
l : F.I₁ i.2 j.2
u : Y ⟶ F.Y l
u₂ : (a ≫ b) ≫ p₂ ≫ pullback.snd (E.f j.1) (F.f j.2) = u ≫ F.p₂ l
x✝ :
  (Sieve.bind (E.sieve₁ (p₁ ≫ pullback.fst (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.fst (E.f j.1) (F.f j.2))).arrows
        fun x f x_1 ↦
        Sieve.pullback f
          (F.sieve₁ (p₁ ≫ pullback.snd (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.snd (E.f j.1) (F.f j.2)))).arrows
    (a ≫ b)
u₁ : a ≫ b ≫ p₁ ≫ pullback.snd (E.f i.1) (F.f i.2) = u ≫ F.p₁ l
⊢ (a ≫ e) ≫ E.p₁ (k, l).1 ≫ E.f i.1 = u ≫ F.p₁ (k, l).2 ≫ F.f i.2
Module: Mathlib.CategoryTheory.Sites.Canonical

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
inst✝ : P.IsRepresentable
⊢ Presieve.IsSheaf (canonicalTopology C) P

Tactic:
← Presieve.isSheaf_comp_uliftFunctor_iff

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
inst✝ : P.IsRepresentable
⊢ Presieve.IsSheaf (canonicalTopology C) (P ⋙ uliftFunctor.{?u.32, w})
Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
inst✝² : HasLimitsOfShape J C
inst✝¹ : HasColimitsOfShape K C
inst✝ : PreservesLimitsOfShape J colim
F : J ⥤ K ⥤ C
a : K
b : J
⊢ colimit.ι (limit F) a ≫ (colimitLimitIso F).hom ≫ limit.π (colimit F.flip) b =
    (limit.π F b).app a ≫ (colimit.ι F.flip a).app b

Tactic:
by
  simp [colimitLimitIso]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Final.Type

Goal state before:
pp: case refine_2.refine_2
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
P : D ⥤ Type w
inst✝ : F.Initial
t : ↑(F ⋙ P).sections
val : (Y : D) → P.obj Y
hval : ∀ (Y : D) (j : CostructuredArrow F Y), (ConcreteCategory.hom (P.map j.hom)) (↑t j.left) = val Y
X : C
⊢ ↑(F.sectionsPrecomp ⟨val, ⋯⟩) X = ↑t X

Tactic:
simpa using (hval (F.obj X) (CostructuredArrow.mk (𝟙 _))).symm

Goal state after:
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X Y : C
inst✝ : Simple Y
f : X ⟶ Y
w : f ≠ 0
⊢ cokernel.π f = 0

Tactic:
by
  by_contra h
  have := isIso_of_epi_of_nonzero h
  exact w (eq_zero_of_mono_cokernel f)

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Opens

Goal state before:
pp: case mp
X : TopCat
U : Opens ↑X
x : ↑X
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom U.inclusion') → x ∈ ↑U

Tactic:
rintro ⟨x, rfl⟩
    exact x.2

Goal state after:
Module: Mathlib.Topology.Sheaves.SheafCondition.Sites

Goal state before:
pp: case mp
X : TopCat
ι : Type u_1
inst✝ : Category.{v_1, u_1} ι
B : ι ⥤ Opens ↑X
⊢ B.IsCoverDense (Opens.grothendieckTopology ↑X) →
    ∀ {U : Opens ↑X} {x : ↑X}, x ∈ U → ∃ U' ∈ Set.range B.obj, x ∈ U' ∧ U' ≤ U

Tactic:
intro hd

Goal state after:
case mp
X : TopCat
ι : Type u_1
inst✝ : Category.{v_1, u_1} ι
B : ι ⥤ Opens ↑X
hd : B.IsCoverDense (Opens.grothendieckTopology ↑X)
⊢ ∀ {U : Opens ↑X} {x : ↑X}, x ∈ U → ∃ U' ∈ Set.range B.obj, x ∈ U' ∧ U' ≤ U
Module: Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Presheaf C X
ι : Type u_2
U : ι → Opens ↑X
h : F.IsSheaf
⊢ Nonempty (IsLimit (Functor.mapCone F (opensLeCoverCocone U).op))

Tactic:
rw [(isLimitOpensLeEquivGenerate₁ F U rfl).nonempty_congr]

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Presheaf C X
ι : Type u_2
U : ι → Opens ↑X
h : F.IsSheaf
⊢ Nonempty (IsLimit (Functor.mapCone F (Sieve.generate (presieveOfCoveringAux U (iSup U))).arrows.cocone.op))
Module: Mathlib.Topology.Sheaves.Stalks

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
F : Presheaf C X
x : ↑X
⊢ IsIso (stalkPushforward C f F x)

Tactic:
have := Functor.initial_of_adjunction (hf.adjunctionNhds x)

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
F : Presheaf C X
x : ↑X
this : (OpenNhds.map f x).Initial
⊢ IsIso (stalkPushforward C f F x)
Module: Mathlib.Topology.Algebra.Module.Basic

Goal state before:
pp: case intro
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁷ : Finite ι
inst✝⁶ : Semiring R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : TopologicalSpace M
inst✝¹ : ContinuousAdd M
inst✝ : ContinuousSMul R M
f : (ι → R) →ₗ[R] M
val✝ : Fintype ι
⊢ Continuous[Pi.topologicalSpace, inst✝²] ⇑f

Tactic:
have : (f : (ι → R) → M) = fun x => ∑ i : ι, x i • f fun j => if i = j then 1 else 0 := by
      ext x
      exact f.pi_apply_eq_sum_univ x

Goal state after:
case intro
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁷ : Finite ι
inst✝⁶ : Semiring R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : TopologicalSpace M
inst✝¹ : ContinuousAdd M
inst✝ : ContinuousSMul R M
f : (ι → R) →ₗ[R] M
val✝ : Fintype ι
this : ⇑f = fun x ↦ ∑ i, x i • f fun j ↦ if i = j then 1 else 0
⊢ Continuous[Pi.topologicalSpace, inst✝²] ⇑f
Module: Mathlib.Topology.Sheaves.Stalks

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝⁴ : PreservesFilteredColimits (forget C)
inst✝³ : HasLimits C
inst✝² : PreservesLimits (forget C)
inst✝¹ : (forget C).ReflectsIsomorphisms
F G : Sheaf C X
f : F ⟶ G
inst✝ : ∀ (x : ↑X), IsIso ((stalkFunctor C x).map f.hom)
this : IsIso ((Sheaf.forget C X).map f)
⊢ IsIso f

Tactic:
by exact isIso_of_fully_faithful (Sheaf.forget C X) f

Goal state after:
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝¹² : Semiring R₁
inst✝¹¹ : Semiring R₂
inst✝¹⁰ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst✝⁹ : TopologicalSpace M₁
inst✝⁸ : AddCommMonoid M₁
M₂ : Type u_6
inst✝⁷ : TopologicalSpace M₂
inst✝⁶ : AddCommMonoid M₂
M₃ : Type u_7
inst✝⁵ : TopologicalSpace M₃
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R₁ M₁
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
g : M₂ →SL[σ₂₃] M₃
f₁ f₂ : M₁ →SL[σ₁₂] M₂
hg : Function.Injective ⇑g
h : g ∘SL f₁ = g ∘SL f₂
x : M₁
⊢ f₁ x = f₂ x

Tactic:
exact hg congr($h x)

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Adjunctions

Goal state before:
pp: X'✝ X✝ : Semigrp
Y✝ : MonCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget₂ MonCat Semigrp).obj Y✝
⊢ (ConcreteCategory.homEquiv.trans (WithOne.lift.symm.trans ConcreteCategory.homEquiv.symm)).symm (f✝ ≫ g✝) =
    adjoinOne.map f✝ ≫
      (ConcreteCategory.homEquiv.trans (WithOne.lift.symm.trans ConcreteCategory.homEquiv.symm)).symm g✝

Tactic:
ext ⟨_ | _⟩ <;> simp <;> rfl

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : TopologicalSpace M
x y : (M →L[R] M)ˣ
⊢ ofUnit (x * y) = ofUnit x * ofUnit y

Tactic:
by
    ext
    rfl

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight

Goal state before:
pp: case h
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : Ring S
inst✝ : Algebra R S
g : S →ₐ[R] R
s : S
hs : (TensorProduct.includeLeftSubRight R S) s = 0
⊢ g s ⊗ₜ[R] 1 = 1 ⊗ₜ[R] s

Tactic:
← AlgHom.id_apply (R := R) (1 : S),

Goal state after:
case h
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : Ring S
inst✝ : Algebra R S
g : S →ₐ[R] R
s : S
hs : (TensorProduct.includeLeftSubRight R S) s = 0
⊢ g s ⊗ₜ[R] (AlgHom.id R S) 1 = 1 ⊗ₜ[R] s
Module: Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight

Goal state before:
pp: case h
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : Ring S
inst✝ : Algebra R S
g : S →ₐ[R] R
s : S
hs : (TensorProduct.includeLeftSubRight R S) s = 0
⊢ (TensorProduct.lid R S).symm ((Algebra.linearMap R S) (g s)) = (TensorProduct.lid R S).symm s

Tactic:
rw [TensorProduct.lid_symm_apply, TensorProduct.lid_symm_apply,
    ← mul_one ((Algebra.linearMap R S) _), Algebra.coe_linearMap, ← Algebra.smul_def,
    ← TensorProduct.smul_tmul, smul_eq_mul, mul_one, ← AlgHom.id_apply (R := R) (1 : S),
    ← TensorProduct.map_tmul,
    sub_eq_zero.mp ((TensorProduct.includeLeftSubRight_apply s).symm.trans hs),
    TensorProduct.map_tmul, map_one, AlgHom.id_apply]

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
g : M₂ →L[R] M₃
f : M →L[R] M₂
hg : g.IsInvertible
⊢ (g ∘SL f).inverse = f.inverse ∘SL g.inverse

Tactic:
by
  rcases hg with ⟨N, rfl⟩
  simp

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight

Goal state before:
pp: R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
hf : IsEffective R S
⊢ Function.Surjective ⇑(codRestrictEqLocusPushoutCocone R S)

Tactic:
by
  intro ⟨s, hs⟩
  obtain ⟨t, rfl⟩ := Set.mem_range.mp <|
    Algebra.IsEffective.eqLocus_includeLeft_includeRight hf ▸ SetLike.mem_coe.mpr hs
  exact ⟨t, rfl⟩

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : C
J : Type u_3
hJ : Category.{u_2, u_3} J
hJ' : IsCofiltered J
F : J ⥤ Over X
c : Cone F
hc : IsLimit c
s : Cone (F ⋙ Over.forget X)
i : J
s' : Cone F :=
  { pt := Over.mk (s.π.app i ≫ (F.obj i).hom), π := { app := fun j ↦ Over.homMk (s.π.app j) ⋯, naturality := ⋯ } }
f : s.pt ⟶ ((Over.forget X).mapCone c).pt
hf : ∀ (j : J), f ≫ Over.Hom.left (c.π.app j) = s.π.app j
⊢ f ≫ c.pt.hom = s'.pt.hom

Tactic:
simp [s', ← hf]

Goal state after: