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

Goal state before:
pp: case h
J : Type u₁
K : Type u₂
inst✝⁴ : SmallCategory J
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
inst✝¹ : FinCategory J
F : J × K ⥤ Type v
inst✝ : IsFiltered K
x : limit (curry.obj F ⋙ colim)
k : J → K
y : (j : J) → F.obj (j, k j)
e :
  ∀ (j : J),
    (ConcreteCategory.hom (colimit.ι ((curry.obj F).obj j) (k j))) (y j) =
      (ConcreteCategory.hom (limit.π (curry.obj F ⋙ colim) j)) x
k' : K
g : (j : J) → k j ⟶ k'
kf : {j j' : J} → (j ⟶ j') → K
gf hf : {j j' : J} → (f : j ⟶ j') → k' ⟶ kf f
wf :
  ∀ {j j' : J} (f : j ⟶ j'),
    (ConcreteCategory.hom (F.map (𝟙 j' ×ₘ g j' ≫ gf f))) (y j') = (ConcreteCategory.hom (F.map (f ×ₘ g j ≫ hf f))) (y j)
k'' : K
i : {j j' : J} → (f : j ⟶ j') → kf f ⟶ k''
s : ∀ {j₁ j₂ j₃ j₄ : J} (f : j₁ ⟶ j₂) (f' : j₃ ⟶ j₄), gf f ≫ i f = hf f' ≫ i f'
⊢ ∀ (j j' : J) (f : j ⟶ j'),
    (ConcreteCategory.hom (((curry.obj (swap K J ⋙ F)).obj k'').map f))
        ((ConcreteCategory.hom (F.map (𝟙 j ×ₘ g j ≫ gf (𝟙 j) ≫ i (𝟙 j)))) (y j)) =
      (ConcreteCategory.hom (F.map (𝟙 j' ×ₘ g j' ≫ gf (𝟙 j') ≫ i (𝟙 j')))) (y j')

Tactic:
· -- After which it's just a calculation, using `s` and `wf`, to see they are coherent.
        dsimp
        intro j j' f
        simp only [← comp_apply, ← Functor.map_comp, prod_comp, id_comp, comp_id]
        calc
          F.map (f ×ₘ (g j ≫ gf (𝟙 j) ≫ i (𝟙 j))) (y j) =
              F.map (f ×ₘ (g j ≫ hf f ≫ i f)) (y j) := by
            rw [s (𝟙 j) f]
          _ =
              F.map (𝟙 j' ×ₘ i f) (F.map (f ×ₘ (g j ≫ hf f)) (y j)) := by
            rw [← comp_apply, ← Functor.map_comp, prod_comp, comp_id, assoc]
          _ =
              F.map (𝟙 j' ×ₘ i f) (F.map (𝟙 j' ×ₘ (g j' ≫ gf f)) (y j')) := by
            rw [← wf f]
          _ = F.map (𝟙 j' ×ₘ (g j' ≫ gf f ≫ i f)) (y j') := by
            rw [← comp_apply, ← Functor.map_comp, prod_comp, id_comp, assoc]
          _ = F.map (𝟙 j' ×ₘ (g j' ≫ gf (𝟙 j') ≫ i (𝟙 j'))) (y j') := by
            rw [s f (𝟙 j'), ← s (𝟙 j') (𝟙 j')]

Goal state after:
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: J : Type v'
inst✝⁶ : Category.{u', v'} J
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u''
inst✝⁴ : Category.{v'', u''} D
X✝ Y✝ : C
inst✝³ : HasPullbacks C
inst✝² : FinitaryPreExtensive C
ι : Type u_1
ι' : Type u_2
inst✝¹ : Finite ι
inst✝ : Finite ι'
S : C
X : ι → C
Y : ι' → C
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
⊢ IsIso
    (Sigma.desc fun p ↦
      pullback.map (f p.1) (g p.2) (Sigma.desc f) (Sigma.desc g) (Sigma.ι X p.1) (Sigma.ι Y p.2) (𝟙 S) ⋯ ⋯)

Tactic:
let c : Cofan _ := Cofan.mk _ <| fun (p : ι × ι') ↦
      pullback.map (f p.1) (g p.2) (Sigma.desc f) (Sigma.desc g) (Sigma.ι _ p.1)
        (Sigma.ι _ p.2) (𝟙 S) (by simp) (by simp)

Goal state after:
J : Type v'
inst✝⁶ : Category.{u', v'} J
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u''
inst✝⁴ : Category.{v'', u''} D
X✝ Y✝ : C
inst✝³ : HasPullbacks C
inst✝² : FinitaryPreExtensive C
ι : Type u_1
ι' : Type u_2
inst✝¹ : Finite ι
inst✝ : Finite ι'
S : C
X : ι → C
Y : ι' → C
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
c : Cofan fun p ↦ pullback (f p.1) (g p.2) :=
  Cofan.mk (pullback (Sigma.desc f) (Sigma.desc g)) fun p ↦
    pullback.map (f p.1) (g p.2) (Sigma.desc f) (Sigma.desc g) (Sigma.ι X p.1) (Sigma.ι Y p.2) (𝟙 S) ⋯ ⋯
⊢ IsIso
    (Sigma.desc fun p ↦
      pullback.map (f p.1) (g p.2) (Sigma.desc f) (Sigma.desc g) (Sigma.ι X p.1) (Sigma.ι Y p.2) (𝟙 S) ⋯ ⋯)
Module: Mathlib.CategoryTheory.Localization.Adjunction

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D₁
inst✝⁴ : Category.{v_4, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
⊢ 𝟭 D₁ ⟶ G' ⋙ F'

Tactic:
letI : Lifting L₁ W₁ ((G ⋙ F) ⋙ L₁) (G' ⋙ F') :=
    Lifting.mk (CatCommSq.hComp G F L₁ L₂ L₁ G' F').iso.symm
  exact Localization.liftNatTrans L₁ W₁ L₁ ((G ⋙ F) ⋙ L₁) (𝟭 D₁) (G' ⋙ F')
    (whiskerRight adj.unit L₁)

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Bousfield

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : G ⊣ F
inst✝¹ : G.Full
inst✝ : G.Faithful
X : C
⊢ isColocal (fun x ↦ x ∈ Set.range G.obj) (adj.counit.app X)

Tactic:
rintro _ ⟨Y, rfl⟩
  convert!
    ((Functor.FullyFaithful.ofFullyFaithful G).homEquiv.symm.trans
        (adj.homEquiv Y X).symm).bijective using 1
  dsimp [Adjunction.homEquiv]
  cat_disch

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

Goal state before:
pp: case mp
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₁ F₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
f₃ : F₁ ⟶ F₃
fac : f₁ ≫ f₂ = f₃
inst✝ : IsLocallySurjective J f₁
⊢ IsLocallySurjective J f₃ → IsLocallySurjective J f₂

pp: case mpr
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₁ F₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
f₃ : F₁ ⟶ F₃
fac : f₁ ≫ f₂ = f₃
inst✝ : IsLocallySurjective J f₁
⊢ IsLocallySurjective J f₂ → IsLocallySurjective J f₃

Tactic:
· intro
    exact isLocallySurjective_of_isLocallySurjective_fac J fac

Goal state after:
case mpr
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₁ F₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
f₃ : F₁ ⟶ F₃
fac : f₁ ≫ f₂ = f₃
inst✝ : IsLocallySurjective J f₁
⊢ IsLocallySurjective J f₂ → IsLocallySurjective J f₃
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case refine_2.uniq
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
⊢ ∀ (m : (BinaryCofan.mk (c.ι.app { as := 0 }) (Sigma.desc fun b ↦ c.ι.app { as := b.succ })).pt ⟶ T),
    (BinaryCofan.mk (c.ι.app { as := 0 }) (Sigma.desc fun b ↦ c.ι.app { as := b.succ })).inl ≫ m = f₁ →
      (BinaryCofan.mk (c.ι.app { as := 0 }) (Sigma.desc fun b ↦ c.ι.app { as := b.succ })).inr ≫ m = f₂ →
        m =
          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)

Tactic:
f₃

Goal state after:
case refine_2.uniq
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
f₃ : (BinaryCofan.mk (c.ι.app { as := 0 }) (Sigma.desc fun b ↦ c.ι.app { as := b.succ })).pt ⟶ T
⊢ (BinaryCofan.mk (c.ι.app { as := 0 }) (Sigma.desc fun b ↦ c.ι.app { as := b.succ })).inl ≫ f₃ = f₁ →
    (BinaryCofan.mk (c.ι.app { as := 0 }) (Sigma.desc fun b ↦ c.ι.app { as := b.succ })).inr ≫ f₃ = f₂ →
      f₃ =
        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)
Module: Mathlib.CategoryTheory.Sites.LocallySurjective

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
S : C
ι : Type u_2
inst✝¹ : Small.{w, u_2} ι
X : ι → C
f : (i : ι) → X i ⟶ S
inst✝ : LocallySmall.{w, v, u} C
c : Cofan fun i ↦ shrinkYoneda.{w, v, u}.obj (X i)
hc : IsColimit c
U : C
g : U ⟶ S
V : C
v : V ⟶ U
i : ι
a : V ⟶ X i
hw :
  (ConcreteCategory.hom ((Cofan.IsColimit.desc hc fun i ↦ shrinkYoneda.{w, v, u}.map (f i)).app (op V)))
      ((ConcreteCategory.hom ((((evaluation Cᵒᵖ (Type w)).obj (op V)).mapCocone c).ι.app { as := i }))
        (shrinkYonedaObjObjEquiv.symm a)) =
    (ConcreteCategory.hom ((shrinkYoneda.{w, v, u}.obj S).map v.op)) (shrinkYonedaObjObjEquiv.symm g)
⊢ shrinkYonedaObjObjEquiv.symm (a ≫ f i) = shrinkYonedaObjObjEquiv.symm (v ≫ g)

Tactic:
← shrinkYoneda_map_app_shrinkYonedaObjObjEquiv_symm

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
S : C
ι : Type u_2
inst✝¹ : Small.{w, u_2} ι
X : ι → C
f : (i : ι) → X i ⟶ S
inst✝ : LocallySmall.{w, v, u} C
c : Cofan fun i ↦ shrinkYoneda.{w, v, u}.obj (X i)
hc : IsColimit c
U : C
g : U ⟶ S
V : C
v : V ⟶ U
i : ι
a : V ⟶ X i
hw :
  (ConcreteCategory.hom ((Cofan.IsColimit.desc hc fun i ↦ shrinkYoneda.{w, v, u}.map (f i)).app (op V)))
      ((ConcreteCategory.hom ((((evaluation Cᵒᵖ (Type w)).obj (op V)).mapCocone c).ι.app { as := i }))
        (shrinkYonedaObjObjEquiv.symm a)) =
    (ConcreteCategory.hom ((shrinkYoneda.{w, v, u}.obj S).map v.op)) (shrinkYonedaObjObjEquiv.symm g)
⊢ (ConcreteCategory.hom ((shrinkYoneda.{w, v, u}.map (f i)).app (op V))) (shrinkYonedaObjObjEquiv.symm a) =
    shrinkYonedaObjObjEquiv.symm (v ≫ g)
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
⊢ projectiveDimension X = 0 ↔ Projective X ∧ ¬Limits.IsZero X

Tactic:
by
  rw [← projectiveDimension_eq_bot_iff, projective_iff_hasProjectiveDimensionLE_zero,
    ← projectiveDimension_le_iff, ← WithBot.lt_zero_iff_eq_bot, not_lt, Nat.cast_zero,
    le_antisymm_iff]

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
⊢ (if hb : b ∈ (Set.range f)ᶜ then Sigma.ι (fun x ↦ R) ⟨b, hb⟩ else 0) = Sigma.ι (fun x ↦ R) ⟨b, hb⟩

Tactic:
apply dif_pos

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

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 α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrpCat
φ : M₀.presheaf ⟶ A.obj
inst✝⁴ : Presheaf.IsLocallyInjective J φ
inst✝³ : Presheaf.IsLocallySurjective J φ
inst✝² : J.WEqualsLocallyBijective AddCommGrpCat
M₀' : PresheafOfModules R₀
A' : Sheaf J AddCommGrpCat
φ' : M₀'.presheaf ⟶ A'.obj
inst✝¹ : Presheaf.IsLocallyInjective J φ'
inst✝ : Presheaf.IsLocallySurjective J φ'
τ₀ : M₀ ⟶ M₀'
τ : A ⟶ A'
fac : (toPresheaf R₀).map τ₀ ≫ φ' = φ ≫ τ.hom
X : Cᵒᵖ
r : ↑(R.obj.obj X)
m : ↑((sheafify α φ).val.obj X)
f : (sheafify α φ).val ⟶ (sheafify α φ').val := (sheafifyHomEquiv' α φ ⋯).symm (τ₀ ≫ toSheafify α φ')
this : τ.hom = (toPresheaf R.obj).map f
⊢ (ConcreteCategory.hom (τ.hom.app X)) (r • m) = r • (ConcreteCategory.hom (τ.hom.app X)) m

Tactic:
by simpa only [this] using! (f.app X).hom.map_smul r m

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

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.RespectsIso
S : C
R T : Presieve S
hR : R ∈ J.coverings S
YR : ⦃Z : C⦄ → (g : Z ⟶ S) → R g → C
eR : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : R g) → YR g a ≅ Z
hTeg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : R g), T ((eR g a).hom ≫ g)
YT : ⦃Z : C⦄ → (g : Z ⟶ S) → T g → C
eT : ⦃Z : C⦄ → (g : Z ⟶ S) → (a : T g) → YT g a ≅ Z
hReg : ∀ ⦃Z : C⦄ (g : Z ⟶ S) (a : T g), R ((eT g a).hom ≫ g)
E : PreZeroHypercover S :=
  { I₀ := ↑R.uncurry ⊕ ↑T.uncurry, X := fun i ↦ Sum.elim (fun j ↦ (↑j).fst) (fun j ↦ YT (↑j).snd ⋯) i,
    f := fun i ↦
      match i with
      | Sum.inl i => (↑i).snd
      | Sum.inr i => (eT (↑i).snd ⋯).hom ≫ (↑i).snd }
F : PreZeroHypercover S :=
  { I₀ := ↑R.uncurry ⊕ ↑T.uncurry, X := fun i ↦ Sum.elim (fun j ↦ YR (↑j).snd ⋯) (fun j ↦ (↑j).fst) i,
    f := fun i ↦
      match i with
      | Sum.inl i => (eR (↑i).snd ⋯).hom ≫ (↑i).snd
      | Sum.inr i => (↑i).snd }
i : E.I₀
⊢ (match i with
        | Sum.inl i => id (eR (↑i).snd ⋯).symm
        | Sum.inr i => id (eT (↑i).snd ⋯)).hom ≫
      F.f ((Equiv.refl E.I₀) i) =
    E.f i

Tactic:
· cases i <;> simp [E, F]

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

Goal state before:
pp: case mpr
C : Type ?u.2
D : Type ?u.4
inst✝¹ : Category.{v_1, ?u.2} C
inst✝ : Category.{v_2, ?u.4} D
K : Coverage C
J : GrothendieckTopology C
⊢ K ≤ J.toCoverage → K.toGrothendieck ≤ J

Tactic:
· intro H X S hS
      induction hS with
      | of X S hS => exact H _ hS
      | top => apply J.top_mem
      | transitive X R S _ _ H1 H2 => exact J.transitive H1 _ H2

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

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.IsStableUnderBaseChange
S : C
E F : PreZeroHypercover S
e : E ≅ F
h : E.presieve₀ ∈ J.coverings S
⊢ (Presieve.ofArrows (fun i ↦ E.X (e.inv.s₀ i)) fun i ↦ E.f (e.inv.s₀ i)) ∈ J.coverings S

pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.IsStableUnderBaseChange
S : C
E F : PreZeroHypercover S
e : E ≅ F
h : E.presieve₀ ∈ J.coverings S
i : F.I₀
⊢ F.X i ⟶ E.X (e.inv.s₀ i)

pp: case refine_3
C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.IsStableUnderBaseChange
S : C
E F : PreZeroHypercover S
e : E ≅ F
h : E.presieve₀ ∈ J.coverings S
⊢ ∀ (i : F.I₀), IsPullback (F.f i) ?refine_2 (𝟙 S) (E.f (e.inv.s₀ i))

Tactic:
· convert! h
      exact Presieve.ofArrows_comp_eq_of_surjective _ (fun i ↦ ⟨e.hom.s₀ i, by simp⟩)

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.IsStableUnderBaseChange
S : C
E F : PreZeroHypercover S
e : E ≅ F
h : E.presieve₀ ∈ J.coverings S
i : F.I₀
⊢ F.X i ⟶ E.X (e.inv.s₀ i)

case refine_3
C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.IsStableUnderBaseChange
S : C
E F : PreZeroHypercover S
e : E ≅ F
h : E.presieve₀ ∈ J.coverings S
⊢ ∀ (i : F.I₀), IsPullback (F.f i) ?refine_2 (𝟙 S) (E.f (e.inv.s₀ i))
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
⊢ IsSheaf (K ⊔ L).toGrothendieck P ↔ IsSheaf K.toGrothendieck P ∧ IsSheaf L.toGrothendieck P

Tactic:
refine ⟨fun h ↦ ⟨Presieve.isSheaf_of_le _ ((gi C).gc.monotone_l le_sup_left) h,
      Presieve.isSheaf_of_le _ ((gi C).gc.monotone_l le_sup_right) h⟩, fun h ↦ ?_⟩

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

Goal state before:
pp: case refine_2
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
X : C
E : PreOneHypercover X
F : C ⥤ D
i₁ i₂ : E.I₀
inst✝¹ : HasPullback (E.f i₁) (E.f i₂)
inst✝ : PreservesLimit (cospan (E.f i₁) (E.f i₂)) F
this : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
⊢ (E.map F).sieve₁ (F.map (pullback.fst (E.f i₁) (E.f i₂))) (F.map (pullback.snd (E.f i₁) (E.f i₂))) ≤
    Sieve.functorPushforward F (E.sieve₁' i₁ i₂)

Tactic:
PreOneHypercover.sieve₁_eq_pullback_sieve₁' _ _ _
      (by simp [← Functor.map_comp, pullback.condition])

Goal state after:
case refine_2
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
X : C
E : PreOneHypercover X
F : C ⥤ D
i₁ i₂ : E.I₀
inst✝¹ : HasPullback (E.f i₁) (E.f i₂)
inst✝ : PreservesLimit (cospan (E.f i₁) (E.f i₂)) F
this : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
⊢ Sieve.pullback (pullback.lift (F.map (pullback.fst (E.f i₁) (E.f i₂))) (F.map (pullback.snd (E.f i₁) (E.f i₂))) ⋯)
      ((E.map F).sieve₁' i₁ i₂) ≤
    Sieve.functorPushforward F (E.sieve₁' i₁ i₂)
Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck

Goal state before:
pp: C : Type u_4
inst✝³ : Category.{u_3, u_4} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
F : C ⥤ D
P : Dᵒᵖ ⥤ Type u_2
X : C
ι : Type (max u_4 u_3)
Y : ι → C
f : (i : ι) → Y i ⟶ X
inst✝¹ : (ofArrows Y f).HasPairwisePullbacks
inst✝ : F.PreservesPairwisePullbacks (ofArrows Y f)
this : (map F (ofArrows Y f)).HasPairwisePullbacks
⊢ IsSheafFor (F.op ⋙ P) (ofArrows Y f) ↔ IsSheafFor P (map F (ofArrows Y f))

Tactic:
rw [map_ofArrows] at this ⊢

Goal state after:
C : Type u_4
inst✝³ : Category.{u_3, u_4} C
D : Type u_1
inst✝² : Category.{v_1, u_1} D
F : C ⥤ D
P : Dᵒᵖ ⥤ Type u_2
X : C
ι : Type (max u_4 u_3)
Y : ι → C
f : (i : ι) → Y i ⟶ X
inst✝¹ : (ofArrows Y f).HasPairwisePullbacks
inst✝ : F.PreservesPairwisePullbacks (ofArrows Y f)
this : (ofArrows (fun i ↦ F.obj (Y i)) fun i ↦ F.map (f i)).HasPairwisePullbacks
⊢ IsSheafFor (F.op ⋙ P) (ofArrows Y f) ↔ IsSheafFor P (ofArrows (fun i ↦ F.obj (Y i)) fun i ↦ F.map (f i))
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology

Goal state before:
pp: case refine_2
C : Type u_3
D : Type u_4
inst✝⁷ : Category.{v_3, u_3} C
inst✝⁶ : Category.{v_4, u_4} D
F : C ⥤ D
K : Precoverage D
inst✝⁵ : K.HasIsos
inst✝⁴ : K.IsStableUnderBaseChange
inst✝³ : K.IsStableUnderComposition
inst✝² : K.HasPullbacks
inst✝¹ : F.Faithful
inst✝ : F.Full
H : ∀ {S : C} {R : Presieve (F.obj S)}, R ∈ K.coverings (F.obj S) → map F (functorPullback F R) ∈ K.coverings (F.obj S)
this : F.LocallyCoverDense K.toGrothendieck
X : C
T : Sieve X
R : Presieve (F.obj X)
hR : R ∈ K.coverings (F.obj X)
hle : R ≤ (Sieve.functorPushforward F T).arrows
⊢ T ∈ (comap F K).toGrothendieck X

Tactic:
refine GrothendieckTopology.superset_covering
        (S := Sieve.generate (Presieve.functorPullback F R)) _ ?_ ?_

Goal state after:
case refine_2.refine_1
C : Type u_3
D : Type u_4
inst✝⁷ : Category.{v_3, u_3} C
inst✝⁶ : Category.{v_4, u_4} D
F : C ⥤ D
K : Precoverage D
inst✝⁵ : K.HasIsos
inst✝⁴ : K.IsStableUnderBaseChange
inst✝³ : K.IsStableUnderComposition
inst✝² : K.HasPullbacks
inst✝¹ : F.Faithful
inst✝ : F.Full
H : ∀ {S : C} {R : Presieve (F.obj S)}, R ∈ K.coverings (F.obj S) → map F (functorPullback F R) ∈ K.coverings (F.obj S)
this : F.LocallyCoverDense K.toGrothendieck
X : C
T : Sieve X
R : Presieve (F.obj X)
hR : R ∈ K.coverings (F.obj X)
hle : R ≤ (Sieve.functorPushforward F T).arrows
⊢ Sieve.generate (functorPullback F R) ≤ T

case refine_2.refine_2
C : Type u_3
D : Type u_4
inst✝⁷ : Category.{v_3, u_3} C
inst✝⁶ : Category.{v_4, u_4} D
F : C ⥤ D
K : Precoverage D
inst✝⁵ : K.HasIsos
inst✝⁴ : K.IsStableUnderBaseChange
inst✝³ : K.IsStableUnderComposition
inst✝² : K.HasPullbacks
inst✝¹ : F.Faithful
inst✝ : F.Full
H : ∀ {S : C} {R : Presieve (F.obj S)}, R ∈ K.coverings (F.obj S) → map F (functorPullback F R) ∈ K.coverings (F.obj S)
this : F.LocallyCoverDense K.toGrothendieck
X : C
T : Sieve X
R : Presieve (F.obj X)
hR : R ∈ K.coverings (F.obj X)
hle : R ≤ (Sieve.functorPushforward F T).arrows
⊢ Sieve.generate (functorPullback F R) ∈ (comap F K).toGrothendieck X
Module: Mathlib.Topology.Sheaves.SheafCondition.Sites

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf C Y
U : Opens ↑X
⊢ Nonempty (StructuredArrow U (Opens.map f))

Tactic:
exact ⟨StructuredArrow.mk <| show U ⟶ (Opens.map f).obj ⊤ from homOfLE le_top⟩

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : TopCat.Presheaf C Y
⊢ (Opens.map f).IsContinuous (Opens.grothendieckTopology ↑Y) (Opens.grothendieckTopology ↑X)

Tactic:
by
  apply Functor.isContinuous_of_coverPreserving
  · exact compatiblePreserving_opens_map f
  · exact coverPreserving_opens_map f

Goal state after:
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 : Sheaf C X
G : Presheaf C X
f : F.obj ⟶ G
U : Opens ↑X
h : ∀ x ∈ U, Function.Injective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map f))
s t : CC (F.obj.obj (op U))
hst : (ConcreteCategory.hom (f.app (op U))) s = (ConcreteCategory.hom (f.app (op U))) t
x : ↑X
hx : x ∈ U
⊢ (ConcreteCategory.hom ((stalkFunctor C x).map f)) ((ConcreteCategory.hom (F.presheaf.germ U x hx)) s) =
    (ConcreteCategory.hom ((stalkFunctor C x).map f)) ((ConcreteCategory.hom (F.presheaf.germ U x hx)) t)

Tactic:
by rw [stalkFunctor_map_germ_apply, stalkFunctor_map_germ_apply, hst]

Goal state after: