mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
⊢ Set.range ⇑(ConcreteCategory.hom (pullback.snd f g)) =
    {y | ∃ x, (ConcreteCategory.hom f) x = (ConcreteCategory.hom g) y}

Tactic:
by
  ext y
  constructor
  · rintro ⟨x, rfl⟩
    use pullback.fst f g x
    exact CategoryTheory.congr_fun pullback.condition x
  · rintro ⟨x, eq⟩
    use (TopCat.pullbackIsoProdSubtype f g).inv ⟨⟨x, y⟩, eq⟩
    rw [pullbackIsoProdSubtype_inv_snd_apply]

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H₁ : IsEmbedding ⇑(ConcreteCategory.hom f)
H₂ : IsEmbedding ⇑(ConcreteCategory.hom g)
⊢ IsEmbedding ⇑(ConcreteCategory.hom (limit.π (cospan f g) WalkingCospan.one))

Tactic:
by
  convert! H₂.comp (snd_isEmbedding_of_left H₁ g)
  rw [← coe_comp, ← limit.w _ WalkingCospan.Hom.inr]
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: case h.refine_1
C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H : IsPushout f g h i
H' : H.IsVanKampen
X' Y' Z' : C
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
inst✝ : HasPullback αX f
hh : IsPullback h' αX αZ h
hi : IsPullback i' αY αZ i
l : pullback αX f ⟶ Y' := hi.lift (pullback.fst αX f ≫ h') (pullback.snd αX f ≫ g) ⋯
⊢ IsPullback l (pullback.snd αX f) αY g

Tactic:
refine IsPullback.of_right' ?_ hi
    rw [← H.w]
    exact IsPullback.paste_horiz (IsPullback.of_hasPullback αX f) hh

Goal state after:
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : H✝.IsVanKampen
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
this : F'.map WalkingSpan.Hom.fst ≫ c'.ι.app WalkingSpan.left = F'.map WalkingSpan.Hom.snd ≫ c'.ι.app WalkingSpan.right
⊢ ∀ (j : WalkingSpan),
    ((Cocone.precompose (diagramIsoSpan F').inv).obj c').ι.app j ≫ (Iso.refl c'.pt).hom =
      (PushoutCocone.mk (c'.ι.app WalkingSpan.left) (c'.ι.app WalkingSpan.right) this).ι.app j

Tactic:
rintro (_ | _ | _) <;> dsimp <;>
          simp only [c'.w, Category.id_comp, Category.comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: case mp.refine_2.h₁
C : Type u
inst✝ : Category.{v, u} C
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H : CommSq f c.inl iY fE
h : IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)
s : PushoutCocone f c.inl
m : (PushoutCocone.mk iY fE ⋯).pt ⟶ s.pt
e₁ : iY ≫ m = s.inl
e₂ : fE ≫ m = s.inr
⊢ c.inr ≫ fE ≫ m = (c.inr ≫ fE) ≫ BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl

Tactic:
e₂,

Goal state after:
case mp.refine_2.h₁
C : Type u
inst✝ : Category.{v, u} C
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H : CommSq f c.inl iY fE
h : IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)
s : PushoutCocone f c.inl
m : (PushoutCocone.mk iY fE ⋯).pt ⟶ s.pt
e₁ : iY ≫ m = s.inl
e₂ : fE ≫ m = s.inr
⊢ c.inr ≫ s.inr = (c.inr ≫ fE) ≫ BinaryCofan.IsColimit.desc h (c.inr ≫ s.inr) s.inl
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case refine_4.refine_1.right
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₁ : IsUniversalColimit c₁
t₂ : IsUniversalColimit c₂
inst✝ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
F : Discrete (Fin (n + 1)) ⥤ C
c : Cocone F
α : 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 α
H : ∀ (j : Discrete (Fin (n + 1))), IsPullback (c.ι.app j) (α.app j) i ((extendCofan c₁ c₂).ι.app j)
F' : Fin (n + 1) → C := F.obj ∘ Discrete.mk
this : F = Discrete.functor F'
H₁ :
  IsColimit
    (Cofan.mk (pullback c₂.inr i) fun j ↦
      pullback.lift (α.app { as := j.succ } ≫ c₁.inj j) (c.ι.app { as := j.succ }) ⋯)
⊢ (mapPair (α.app { as := 0 }) (pullback.fst c₂.inr i) ≫ c₂.ι).app { as := WalkingPair.right } =
    ((BinaryCofan.mk (c.ι.app { as := 0 }) (pullback.snd c₂.inr i)).ι ≫ (const (Discrete WalkingPair)).map i).app
      { as := WalkingPair.right }

Tactic:
simpa using! pullback.condition

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝¹ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝ : ConcreteCategory A FA
F : Cᵒᵖ ⥤ Type (max u v)
⊢ (Subfunctor.sheafify J (Subfunctor.range (J.toSheafify F))).ι ≫
      J.sheafifyLift (Subfunctor.toRangeSheafify J (J.toSheafify F)) ⋯ =
    𝟙 (Subfunctor.sheafify J (Subfunctor.range (J.toSheafify F))).toFunctor

Tactic:
by
    rw [← cancel_mono (Subfunctor.ι _), Category.id_comp, Category.assoc]
    refine Eq.trans ?_ (Category.comp_id _)
    congr 1
    exact J.sheafify_hom_ext _ _ (J.sheafify_isSheaf _) (by simp [Subfunctor.toRangeSheafify])

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

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : LocallySmall.{w, v, u} C
S : C
ι : Type u_2
inst✝ : Small.{w, u_2} ι
X : ι → C
f : (i : ι) → X i ⟶ S
c : Cofan fun i ↦ shrinkYoneda.{w, v, u}.obj (X i)
hc : IsColimit c
U : C
u : unop (op U) ⟶ S
hf : Sieve.pullback u (Sieve.ofArrows X f) ∈ J (unop (op U))
⊢ Presheaf.imageSieve (Cofan.IsColimit.desc hc fun i ↦ shrinkYoneda.{w, v, u}.map (f i))
      (shrinkYonedaObjObjEquiv.symm u) ∈
    J U

Tactic:
← Presheaf.imageSieve_cofanIsColimitDesc_shrinkYoneda_map f hc u

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : LocallySmall.{w, v, u} C
S : C
ι : Type u_2
inst✝ : Small.{w, u_2} ι
X : ι → C
f : (i : ι) → X i ⟶ S
c : Cofan fun i ↦ shrinkYoneda.{w, v, u}.obj (X i)
hc : IsColimit c
U : C
u : unop (op U) ⟶ S
hf :
  Presheaf.imageSieve (Cofan.IsColimit.desc hc fun i ↦ shrinkYoneda.{w, v, u}.map (f i))
      (shrinkYonedaObjObjEquiv.symm u) ∈
    J (unop (op U))
⊢ Presheaf.imageSieve (Cofan.IsColimit.desc hc fun i ↦ shrinkYoneda.{w, v, u}.map (f i))
      (shrinkYonedaObjObjEquiv.symm u) ∈
    J U
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: case succ
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₁ : HasProjectiveDimensionLT S.X₁ n
h₂ : HasProjectiveDimensionLT S.X₂ (n + 1)
this : HasExt C := HasExt.standard C
i : ℕ
hi : n + 1 ≤ i + 1
Y : C
x₃ : Ext S.X₃ Y (i + 1)
⊢ x₃ = 0

Tactic:
obtain ⟨x₁, rfl⟩ := Ext.contravariant_sequence_exact₃ hS _ x₃
      (Ext.eq_zero_of_hasProjectiveDimensionLT _ (n + 1) hi) (add_comm _ _)
    rw [x₁.eq_zero_of_hasProjectiveDimensionLT n (by lia), Ext.comp_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
inst✝¹ : HasExt C
inst✝ : EnoughInjectives C
X : C
n : ℕ
hX : ∀ (Y : C), Subsingleton (Ext X Y n)
d : ℕ
Y : C
e : Ext X Y d
k : ℕ
hd : d = n + k
⊢ e = 0

Tactic:
induction k generalizing d Y with

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
R : C
α : Type u_1
β : Type u_2
f : α → β
inst✝² : HasCoproduct fun x ↦ R
inst✝¹ : HasCoproduct fun x ↦ R
inst✝ : HasCoproduct fun x ↦ R
b : β
hb : b ∉ Set.range f
⊢ Sigma.ι (fun x ↦ R) b ≫ Cofork.π (sigmaConstCokernelCofork R f) = Sigma.ι (fun x ↦ R) ⟨b, hb⟩

Tactic:
dsimp [sigmaConstCokernelCofork]
  rw [Sigma.ι_desc]
  apply dif_pos

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Free

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
M N : SheafOfModules R
I : Type u
s : I → M.sections
p : M ⟶ N
⊢ N.freeHomEquiv (M.freeHomEquiv.symm s ≫ p) = N.freeHomEquiv (N.freeHomEquiv.symm fun i ↦ sectionsMap p (s i))

Tactic:
by ext; simp [freeHomEquiv_comp_apply]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Free

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
I J : Type u
f : I → J
⊢ (free J).freeHomEquiv.symm ((free J).freeHomEquiv (freeMap f)) = (free J).freeHomEquiv.symm (freeSection ∘ f)

Tactic:
simp; rfl

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreZeroHypercover S
c : Cofan E.X
hc : IsColimit c
i : E.I₀
r : PUnit.{w + 1}
⊢ c.inj i ≫ (E.sigmaOfIsColimit hc).f r = E.f i

Tactic:
by
  simp [PreZeroHypercover.sigmaOfIsColimit]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
K : Precoverage C
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasIsos
X : C
E F : PreZeroHypercover X
e : E ≅ F
hE : E.presieve₀ ∈ K.coverings X
⊢ F.presieve₀ ∈ K.coverings X

Tactic:
by
  have : F.presieve₀ =
      Presieve.ofArrows (fun (i : Σ (_ : F.I₀), Unit) ↦ _) (fun i ↦ e.inv.h₀ i.1 ≫ E.f _) := by
    simp only [Hom.w₀]
    refine le_antisymm ?_ ?_
    · rw [Presieve.ofArrows_le_iff]
      intro i
      exact .mk (⟨i, ⟨⟩⟩ : Σ (_ : F.I₀), Unit)
    · simp [Presieve.ofArrows_le_iff]
  rw [this]
  refine K.comp_mem_coverings (fun i ↦ E.f (e.inv.s₀ i)) ?_ (fun i (k : Unit) ↦ e.inv.h₀ i) ?_
  · rwa [← E.presieve₀_reindex (PreZeroHypercover.equivOfIso e.symm)] at hE
  · intro i
    rw [Presieve.ofArrows_pUnit]
    exact K.mem_coverings_of_isIso _

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
S T : C
inst✝ : J.IsStableUnderSup
E : J.ZeroHypercover S
F : J.ZeroHypercover S
⊢ (E.sum F.toPreZeroHypercover).presieve₀ ∈ J.coverings S

Tactic:
rw [PreZeroHypercover.presieve₀_sum]
    exact J.sup_mem_coverings E.mem₀ F.mem₀

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

Goal state before:
pp: case inl
C : Type ?u.2
D : Type ?u.4
inst✝¹ : Category.{v_1, ?u.2} C
inst✝ : Category.{v_2, ?u.4} D
x y : Coverage C
X Y : C
f : Y ⟶ X
S : Presieve X
hx : S ∈ x.coverings X
T : Presieve Y
hT : T ∈ x.coverings Y ∧ T.FactorsThruAlong S f
⊢ ∃ T ∈ x.coverings Y ∪ y.coverings Y, T.FactorsThruAlong S f

Tactic:
exact ⟨T, Or.inl hT.1, hT.2⟩

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

Goal state before:
pp: C : Type u_2
inst✝² : Category.{v_1, u_2} C
J : Precoverage C
inst✝¹ : J.HasPullbacks
inst✝ : J.IsStableUnderBaseChange
P : Cᵒᵖ ⥤ Type u_1
⊢ Presieve.IsSheaf J.toGrothendieck P ↔ ∀ ⦃X : C⦄, ∀ R ∈ J.coverings X, Presieve.IsSheafFor P R

Tactic:
rw [← J.toCoverage_toPrecoverage, Coverage.toGrothendieck_toPrecoverage,
    Presieve.isSheaf_coverage]

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Preserves

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst✝⁵ : Category.{v_1, u_1} A
inst✝⁴ : Category.{v_2, u_2} B
inst✝³ : Category.{v_3, u_3} C
inst✝² : Category.{v_4, u_4} D
G : B ⥤ D
F : A ⥤ B
L : A ⥤ C
inst✝¹ : G.PreservesLeftKanExtension F L
inst✝ : L.HasLeftKanExtension F
a : A
⊢ G.map ((L.leftKanExtensionUnit F).app a) ≫ (G.leftKanExtensionCompIsoOfPreserves F L).hom.app (L.obj a) =
    (L.leftKanExtensionUnit (F ⋙ G)).app a

Tactic:
simpa [-leftKanExtensionCompIsoOfPreserves_hom_fac] using
    NatTrans.congr_app (leftKanExtensionCompIsoOfPreserves_hom_fac G F L) a

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
F F' : C ⥤ D
τ : F ⟶ F'
e : F ≅ F'
G : D ⥤ E
F'' : C ⥤ C
eF'' : F'' ≅ 𝟭 C
FG : C ⥤ E
eFG : F ⋙ G ≅ FG
A : Type u
inst✝² : Category.{t, u} A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
inst✝¹ : F.IsContinuous J K
inst✝ : F'.IsContinuous J K
x✝¹ : Sheaf K A
x✝ : Cᵒᵖ
⊢ ((sheafPushforwardContinuousNatTrans e.inv A J K ≫ sheafPushforwardContinuousNatTrans e.hom A J K).app x✝¹).hom.app
      x✝ =
    ((𝟙 (F.sheafPushforwardContinuous A J K)).app x✝¹).hom.app x✝

Tactic:
simp [← Functor.map_comp, ← op_comp]

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
F F' : C ⥤ D
τ : F ⟶ F'
e : F ≅ F'
G : D ⥤ E
F'' : C ⥤ C
eF'' : F'' ≅ 𝟭 C
FG : C ⥤ E
eFG : F ⋙ G ≅ FG
A : Type u
inst✝² : Category.{t, u} A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
inst✝¹ : F.IsContinuous J K
inst✝ : F'.IsContinuous J K
x✝¹ : Sheaf K A
x✝ : Cᵒᵖ
⊢ ((sheafPushforwardContinuousNatTrans e.hom A J K ≫ sheafPushforwardContinuousNatTrans e.inv A J K).app x✝¹).hom.app
      x✝ =
    ((𝟙 (F'.sheafPushforwardContinuous A J K)).app x✝¹).hom.app x✝

Tactic:
simp [← Functor.map_comp, ← op_comp]

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

Goal state before:
pp: C : Type uC
inst✝³ : Category.{vC, uC} C
D : Type uD
inst✝² : Category.{vD, uD} D
G✝ : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type u_1
inst✝¹ : Category.{v_1, u_1} A
G : C ⥤ D
inst✝ : G.Full
U✝ V✝ : C
f : G.obj U✝ ⟶ G.obj V✝
⊢ Sieve.functorPushforward G (G.imageSieve (G.map (G.preimage f))) ∈ K (G.obj U✝)

Tactic:
simp only [Functor.imageSieve_map, Sieve.functorPushforward_top, GrothendieckTopology.top_mem]

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
K : GrothendieckTopology D
e : C ≌ D
G : D ⥤ C
A : Type u₃
inst✝¹ : Category.{v₃, u₃} A
inst✝ : IsDenseSubsite K J e.inverse
X : Sheaf J A
x✝ : Dᵒᵖ
⊢ ((sheafCongr.functor J K e A).map ((sheafCongr.unitIso J K e A).hom.app X) ≫
            (sheafCongr.counitIso J K e A).hom.app ((sheafCongr.functor J K e A).obj X)).hom.app
      x✝ =
    (𝟙 ((sheafCongr.functor J K e A).obj X)).hom.app x✝

Tactic:
simp [← Functor.map_comp, ← op_comp]

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

Goal state before:
pp: case refine_2.left
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S : C
E✝¹ E✝ : PreOneHypercover S
F✝ : PreOneHypercover S
G✝ : PreOneHypercover S
E F : PreOneHypercover S
f : E ≅ F
G : Cᵒᵖ ⥤ A
a✝ : E.multicospanShape.L
⊢ ((Cone.postcompose
                (WalkingMulticospan.functorExt (fun i ↦ G.mapIso (asIso (f.hom.h₀ i)).symm.op)
                    (fun i ↦ G.mapIso (asIso (f.hom.h₁ i.snd)).symm.op) ⋯ ⋯).hom).obj
            (E.multifork G)).π.app
      (WalkingMulticospan.left a✝) =
    (Iso.refl
          ((Cone.postcompose
                  (WalkingMulticospan.functorExt (fun i ↦ G.mapIso (asIso (f.hom.h₀ i)).symm.op)
                      (fun i ↦ G.mapIso (asIso (f.hom.h₁ i.snd)).symm.op) ⋯ ⋯).hom).obj
              (E.multifork G)).pt).hom ≫
      (Cone.whisker (equivalenceMulticospanOfIso f).functor (F.multifork G)).π.app (WalkingMulticospan.left a✝)

Tactic:
simp [← Functor.map_comp, ← op_comp]

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

Goal state before:
pp: C : Type u'
inst✝⁴ : Category.{v', u'} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
inst✝¹ : J.WEqualsLocallyBijective AddCommGrpCat
inst✝ : HasWeakSheafify J AddCommGrpCat
⊢ J.W.inverseImage (toPresheaf R₀) = (isomorphisms (SheafOfModules R)).inverseImage (sheafification α)

Tactic:
J.W_eq_inverseImage_isomorphisms

Goal state after:
C : Type u'
inst✝⁴ : Category.{v', u'} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
inst✝¹ : J.WEqualsLocallyBijective AddCommGrpCat
inst✝ : HasWeakSheafify J AddCommGrpCat
⊢ ((isomorphisms (Sheaf J Ab)).inverseImage (presheafToSheaf J Ab)).inverseImage (toPresheaf R₀) =
    (isomorphisms (SheafOfModules R)).inverseImage (sheafification α)
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : Limits.HasPullbacks C
F : Sheaf J A
X Y : C
f : X ⟶ Y
⊢ ∀ ⦃X_1 Y_1 : (Over Y)ᵒᵖ⦄ (f_1 : X_1 ⟶ Y_1),
    (F.over Y).obj.map f_1 ≫ F.obj.map (Limits.pullback.fst (Opposite.unop Y_1).hom f).op =
      F.obj.map (Limits.pullback.fst (Opposite.unop X_1).hom f).op ≫
        (((Over.pullback f).sheafPushforwardContinuous A (J.over Y) (J.over X)).obj (F.over X)).obj.map f_1

Tactic:
simp [← Functor.map_comp, ← op_comp]

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

Goal state before:
pp: 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.Final
φ : (Y : D) → P.obj Y → (F ⋙ P).ColimitType
hφ : ∀ (Y : D) (j : StructuredArrow Y F), (F ⋙ P).ιColimitType j.right ∘ ⇑(ConcreteCategory.hom (P.map j.hom)) = φ Y
Y₁ Y₂ : D
f : Y₁ ⟶ Y₂
x✝ : (fun X ↦ X) (P.obj Y₁)
X : StructuredArrow Y₂ F
⊢ (φ Y₂ ∘ ⇑(ConcreteCategory.hom (P.map f))) x✝ = φ Y₁ x✝

Tactic:
← hφ Y₂ X,

Goal state after:
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.Final
φ : (Y : D) → P.obj Y → (F ⋙ P).ColimitType
hφ : ∀ (Y : D) (j : StructuredArrow Y F), (F ⋙ P).ιColimitType j.right ∘ ⇑(ConcreteCategory.hom (P.map j.hom)) = φ Y
Y₁ Y₂ : D
f : Y₁ ⟶ Y₂
x✝ : (fun X ↦ X) (P.obj Y₁)
X : StructuredArrow Y₂ F
⊢ (((F ⋙ P).ιColimitType X.right ∘ ⇑(ConcreteCategory.hom (P.map X.hom))) ∘ ⇑(ConcreteCategory.hom (P.map f))) x✝ =
    φ Y₁ x✝
Module: Mathlib.CategoryTheory.Limits.Lattice

Goal state before:
pp: α : Type u
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
x y : α
⊢ colimit (pair x y) = Finset.univ.sup (pair x y).obj

Tactic:
by rw [finite_colimit_eq_finset_univ_sup (pair x y)]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous

Goal state before:
pp: C✝ : Type u₁
inst✝⁹ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝⁸ : Category.{v₂, u₂} D✝
D' : Type u₃
inst✝⁷ : Category.{v₃, u₃} D'
D'' : Type u₄
inst✝⁶ : Category.{v₄, u₄} D''
J✝ : GrothendieckTopology C✝
K✝ : GrothendieckTopology D✝
F✝ : C✝ ⥤ D✝
S✝ : Sheaf J✝ RingCat
R : Sheaf K✝ RingCat
inst✝⁵ : F✝.IsContinuous J✝ K✝
φ✝ : S✝ ⟶ (F✝.sheafPushforwardContinuous RingCat J✝ K✝).obj R
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F G H : C ⥤ D
T : Sheaf J RingCat
S : Sheaf K RingCat
inst✝² : F.IsContinuous J K
inst✝¹ : G.IsContinuous J K
inst✝ : H.IsContinuous J K
φ : T ⟶ (G.sheafPushforwardContinuous RingCat J K).obj S
α : F ⟶ G
X Y : SheafOfModules S
f : X ⟶ Y
⊢ (pushforward φ).map f ≫
      {
        val :=
          {
            app := fun U ↦
              (ModuleCat.restrictScalars (RingCat.Hom.hom (φ.hom.app U))).map (Y.val.map (α.app (Opposite.unop U)).op),
            naturality := ⋯ } } =
    {
        val :=
          {
            app := fun U ↦
              (ModuleCat.restrictScalars (RingCat.Hom.hom (φ.hom.app U))).map (X.val.map (α.app (Opposite.unop U)).op),
            naturality := ⋯ } } ≫
      (pushforward (φ ≫ (sheafPushforwardContinuousNatTrans α RingCat J K).app S)).map f

Tactic:
ext U x
    exact congr($(f.val.naturality (α.app U.unop).op) x).symm

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous

Goal state before:
pp: C✝ : Type u₁
inst✝⁹ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝⁸ : Category.{v₂, u₂} D✝
D' : Type u₃
inst✝⁷ : Category.{v₃, u₃} D'
D'' : Type u₄
inst✝⁶ : Category.{v₄, u₄} D''
J✝ : GrothendieckTopology C✝
K✝ : GrothendieckTopology D✝
F✝ : C✝ ⥤ D✝
S✝ : Sheaf J✝ RingCat
R : Sheaf K✝ RingCat
inst✝⁵ : F✝.IsContinuous J✝ K✝
φ✝ : S✝ ⟶ (F✝.sheafPushforwardContinuous RingCat J✝ K✝).obj R
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F G H : C ⥤ D
T : Sheaf J RingCat
S : Sheaf K RingCat
inst✝² : F.IsContinuous J K
inst✝¹ : G.IsContinuous J K
inst✝ : H.IsContinuous J K
φ : T ⟶ (G.sheafPushforwardContinuous RingCat J K).obj S
α : F ≅ G
x✝ : Cᵒᵖ
⊢ ((φ ≫ (sheafPushforwardContinuousNatTrans α.hom RingCat J K).app S) ≫
            (sheafPushforwardContinuousNatTrans α.inv RingCat J K).app S).hom.app
      x✝ =
    φ.hom.app x✝

Tactic:
simp [← Functor.map_comp, ← op_comp]

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

Goal state before:
pp: T : Type u
inst✝ : TopologicalSpace T
ι : Type u_1
U : ι → Opens T
⊢ Sieve.ofObjects U ⊤ ∈
      { sieves := fun X ↦ {S | ∀ x ∈ X, ∃ U, (∃ x, S.arrows x) ∧ x ∈ U}, top_mem' := ⋯, pullback_stable' := ⋯,
          transitive' := ⋯ }
        ⊤ ↔
    ∀ ⦃x : T⦄, ∃ i, x ∈ U i

Tactic:
refine ⟨fun h x ↦ ?_, fun hU x hx ↦ ?_⟩

Goal state after:
case refine_1
T : Type u
inst✝ : TopologicalSpace T
ι : Type u_1
U : ι → Opens T
h :
  Sieve.ofObjects U ⊤ ∈
    { sieves := fun X ↦ {S | ∀ x ∈ X, ∃ U, (∃ x, S.arrows x) ∧ x ∈ U}, top_mem' := ⋯, pullback_stable' := ⋯,
        transitive' := ⋯ }
      ⊤
x : T
⊢ ∃ i, x ∈ U i

case refine_2
T : Type u
inst✝ : TopologicalSpace T
ι : Type u_1
U : ι → Opens T
hU : ∀ ⦃x : T⦄, ∃ i, x ∈ U i
x : T
hx : x ∈ ⊤
⊢ ∃ U_1, (∃ x, (Sieve.ofObjects U ⊤).arrows x) ∧ x ∈ U_1
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous

Goal state before:
pp: C✝ : Type u₁
inst✝⁹ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝⁸ : Category.{v₂, u₂} D✝
D' : Type u₃
inst✝⁷ : Category.{v₃, u₃} D'
D'' : Type u₄
inst✝⁶ : Category.{v₄, u₄} D''
J✝ : GrothendieckTopology C✝
K✝ : GrothendieckTopology D✝
F✝ : C✝ ⥤ D✝
S✝ : Sheaf J✝ RingCat
R : Sheaf K✝ RingCat
inst✝⁵ : F✝.IsContinuous J✝ K✝
φ✝ : S✝ ⟶ (F✝.sheafPushforwardContinuous RingCat J✝ K✝).obj R
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F G H : C ⥤ D
T : Sheaf J RingCat
S : Sheaf K RingCat
inst✝² : F.IsContinuous J K
inst✝¹ : G.IsContinuous J K
inst✝ : H.IsContinuous J K
φ : T ⟶ (G.sheafPushforwardContinuous RingCat J K).obj S
α : F ≅ G
⊢ (pushforwardNatTrans (φ ≫ (sheafPushforwardContinuousNatTrans α.hom RingCat J K).app S) α.inv ≫
        (pushforwardCongr ⋯).hom) ≫
      pushforwardNatTrans φ α.hom =
    𝟙 (pushforward (φ ≫ (sheafPushforwardContinuousNatTrans α.hom RingCat J K).app S))

Tactic:
ext X U x
    suffices X.val.presheaf.map (α.inv.app U.unop).op ≫
      X.val.presheaf.map (α.hom.app U.unop).op = 𝟙 _ from congr($this x)
    simp only [← Functor.map_comp, ← op_comp,
      Iso.hom_inv_id_app, op_id, CategoryTheory.Functor.map_id]

Goal state after: