mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsCofilteredOrEmpty C
c x✝ : C
x : Over c
s s' : (forget c).obj x ⟶ x✝
⊢ IsCofiltered.eqHom s s' ≫ s = IsCofiltered.eqHom s s' ≫ s'

Tactic:
IsCofiltered.eq_condition

Goal state after:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsCofilteredOrEmpty C
c x✝ : C
x : Over c
s s' : (forget c).obj x ⟶ x✝
⊢ IsCofiltered.eqHom s s' ≫ s' = IsCofiltered.eqHom s s' ≫ s'
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Free

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
F : Cᵒᵖ ⥤ Type u
⊢ ∀ (X : Cᵒᵖ),
    ModuleCat.freeDesc (↾fun x ↦ ModuleCat.freeMk ((ConcreteCategory.hom (F.map (𝟙 X))) x)) =
      (ModuleCat.restrictScalarsId' (RingCat.Hom.hom (R.map (𝟙 X))) ⋯).inv.app
        ((ModuleCat.free ↑(R.obj X)).obj (F.obj X))

Tactic:
by aesop

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

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
R : Dᵒᵖ ⥤ CommRingCat
x✝² x✝¹ x✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
⊢ (isoMk (fun x ↦ Iso.refl (((pushforward₀OfCommRingCat F R).obj x✝² ⊗ (pushforward₀OfCommRingCat F R).obj x✝¹).obj x))
            ⋯).hom ▷
        (pushforward₀OfCommRingCat F R).obj x✝ ≫
      (isoMk
            (fun x ↦
              Iso.refl
                (((pushforward₀OfCommRingCat F R).obj (x✝² ⊗ x✝¹) ⊗ (pushforward₀OfCommRingCat F R).obj x✝).obj x))
            ⋯).hom ≫
        (pushforward₀OfCommRingCat F R).map (α_ x✝² x✝¹ x✝).hom =
    (α_ ((pushforward₀OfCommRingCat F R).obj x✝²) ((pushforward₀OfCommRingCat F R).obj x✝¹)
          ((pushforward₀OfCommRingCat F R).obj x✝)).hom ≫
      (pushforward₀OfCommRingCat F R).obj x✝² ◁
          (isoMk
              (fun x ↦
                Iso.refl (((pushforward₀OfCommRingCat F R).obj x✝¹ ⊗ (pushforward₀OfCommRingCat F R).obj x✝).obj x))
              ⋯).hom ≫
        (isoMk
            (fun x ↦
              Iso.refl
                (((pushforward₀OfCommRingCat F R).obj x✝² ⊗ (pushforward₀OfCommRingCat F R).obj (x✝¹ ⊗ x✝)).obj x))
            ⋯).hom

Tactic:
by
        ext1
        exact tensor_ext₃' fun m₁ m₂ m₃ ↦ rfl

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F F' F'' : C ⥤ Type w
G G' : Subfunctor F
x✝⁴ : Set (Subfunctor F)
x✝³ : Subfunctor F
x✝² : x✝³ ∈ x✝⁴
x✝¹ : C
x✝ : F.obj x✝¹
⊢ x✝ ∈ x✝³.obj x✝¹ → x✝ ∈ { obj := fun U ↦ sSup ((fun T ↦ T.obj U) '' x✝⁴), map := ⋯ }.obj x✝¹

Tactic:
by aesop

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F F' F'' : C ⥤ Type w
G G' : Subfunctor F
x✝³ : Set (Subfunctor F)
x✝² : Subfunctor F
x✝¹ : x✝² ∈ upperBounds x✝³
x✝ : C
⊢ { obj := fun U ↦ sSup ((fun T ↦ T.obj U) '' x✝³), map := ⋯ }.obj x✝ ⊆ x✝².obj x✝

Tactic:
by aesop

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F F' F'' : C ⥤ Type w
G G' : Subfunctor F
x✝⁴ : Set (Subfunctor F)
x✝³ : Subfunctor F
x✝² : x✝³ ∈ x✝⁴
x✝¹ : C
x✝ : F.obj x✝¹
⊢ x✝ ∈ { obj := fun U ↦ sInf ((fun T ↦ T.obj U) '' x✝⁴), map := ⋯ }.obj x✝¹ → x✝ ∈ x✝³.obj x✝¹

Tactic:
by aesop

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F F' F'' : C ⥤ Type w
G G' : Subfunctor F
x✝³ : Set (Subfunctor F)
x✝² : Subfunctor F
x✝¹ : x✝² ∈ lowerBounds x✝³
x✝ : C
⊢ x✝².obj x✝ ⊆ { obj := fun U ↦ sInf ((fun T ↦ T.obj U) '' x✝³), map := ⋯ }.obj x✝

Tactic:
by aesop

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
J : GrothendieckTopology C
f : Y ⟶ X
S : Sieve X
hf : S.arrows f
⊢ J.Covers S f

Tactic:
rw [Covers, (Sieve.mem_iff_pullback_eq_top f).1 hf]
  apply J.top_mem

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Equalizers

Goal state before:
pp: X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : ∀ (y : Y), (hom g) y = (hom h) y → ∃! x, (hom f) x = y
s : Fork g h
⊢ { l // l ≫ (Fork.ofι f w).ι = s.ι ∧ ∀ {m : s.pt ⟶ (Fork.ofι f w).pt}, m ≫ (Fork.ofι f w).ι = s.ι → m = l }

Tactic:
refine ⟨↾fun i => ?_, ?_, ?_⟩
    · apply Classical.choose (t (s.ι i) _)
      apply congr_hom s.condition i
    · ext i
      exact (Classical.choose_spec (t (s.ι i) (congr_hom s.condition i))).1
    · intro m hm
      ext i
      exact (Classical.choose_spec (t (s.ι i) (congr_hom s.condition i))).2 _ (congr_hom hm i)

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
inst✝ : ∀ (i : ι), HasPullback (g i) f
⊢ (ofArrows (fun i ↦ pullback (g i) f) fun x ↦ pullback.snd (g x) f) = pullbackArrows f (ofArrows Z g)

Tactic:
by
  funext T
  ext h
  constructor
  · rintro ⟨hk⟩
    exact pullbackArrows.mk _ _ (ofArrows.mk hk)
  · rintro ⟨W, k, ⟨_⟩⟩
    apply ofArrows.mk

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
R : Presieve X
⊢ pushforward (𝟙 X) R = R

Tactic:
funext
  simp [pushforward]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f : Y ⟶ X
R : Presieve Y
g : X ⟶ Z
⊢ pushforward (f ≫ g) R = pushforward g (pushforward f R)

Tactic:
funext
  simp [pushforward]

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

Goal state before:
pp: case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
ι : Type u_1
Y : ι → C
f : (i : ι) → Y i ⟶ X
i : ι
v : Y i ⟶ X
h : f i ≍ v
⊢ ⟨Y i, v⟩ ∈ (ofArrows Y f).uncurry

Tactic:
← eq_of_heq h

Goal state after:
case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
ι : Type u_1
Y : ι → C
f : (i : ι) → Y i ⟶ X
i : ι
v : Y i ⟶ X
h : f i ≍ v
⊢ ⟨Y i, f i⟩ ∈ (ofArrows Y f).uncurry
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
f : Y ⟶ X
x : FamilyOfElements P S.arrows
h : x.Compatible
⊢ (FamilyOfElements.pullback f x).Compatible

Tactic:
simp only [compatible_iff_sieveCompatible] at h ⊢

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y : C
S : Sieve X
f : Y ⟶ X
x : FamilyOfElements P S.arrows
h : x.SieveCompatible
⊢ (FamilyOfElements.pullback f x).SieveCompatible
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
S : Sieve Y
⊢ pushforward f S = ⊥ ↔ S = ⊥

Tactic:
by
  simp [(galoisConnection f).l_eq_bot]

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
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
X : C
S : Sieve X
R : Presieve X
E : Aᵒᵖ
x : { x // x.SieveCompatible }
f f' : S.arrows.categoryᵒᵖ
g : f ⟶ f'
this : ↑x (Over.Hom.left g.unop.hom ≫ (unop f).obj.hom) ⋯ = ↑x (unop f).obj.hom ⋯ ≫ P.map (Over.Hom.left g.unop.hom).op
⊢ 𝟙 (unop E) ≫ ↑x (unop f').obj.hom ⋯ = ↑x (unop f).obj.hom ⋯ ≫ P.map (Over.Hom.left g.unop.hom).op

Tactic:
rw [id_comp, ← this]

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
X : C
S : Sieve X
R : Presieve X
E : Aᵒᵖ
x : { x // x.SieveCompatible }
f f' : S.arrows.categoryᵒᵖ
g : f ⟶ f'
this : ↑x (Over.Hom.left g.unop.hom ≫ (unop f).obj.hom) ⋯ = ↑x (unop f).obj.hom ⋯ ≫ P.map (Over.Hom.left g.unop.hom).op
⊢ ↑x (unop f').obj.hom ⋯ = ↑x (Over.Hom.left g.unop.hom ≫ (unop f).obj.hom) ⋯
Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type w
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).HasPairwisePullbacks
x : FirstObj P X
⊢ Arrows.Compatible P π ((ConcreteCategory.hom (Types.productIso fun i ↦ P.obj (op (X i))).hom) x) ↔
    (ConcreteCategory.hom (firstMap P X π)) x = (ConcreteCategory.hom (secondMap P X π)) x

Tactic:
rw [Arrows.pullbackCompatible_iff]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type w
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).HasPairwisePullbacks
x : FirstObj P X
⊢ Arrows.PullbackCompatible P π ((ConcreteCategory.hom (Types.productIso fun i ↦ P.obj (op (X i))).hom) x) ↔
    (ConcreteCategory.hom (firstMap P X π)) x = (ConcreteCategory.hom (secondMap P X π)) x
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
F : C ⥤ D
inst✝¹ : F.Full
inst✝ : F.Faithful
X Y : C
R : Sieve X
f : Y ⟶ X
⊢ Presieve.functorPushforward F R.arrows (F.map f) ↔ R.arrows f

Tactic:
rw [Sieve.mem_functorPushforward_iff_of_full]
  refine ⟨fun ⟨g, hcomp, hg⟩ ↦ ?_, fun hf ↦ ⟨f, rfl, hf⟩⟩
  rwa [← F.map_injective hcomp]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type t
inst✝¹ : Small.{w, t} I
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).HasPairwisePullbacks
x : FirstObj P X
⊢ Arrows.Compatible P π
      ((equivShrink ((i : I) → P.obj (op (X i)))).symm
        ((ConcreteCategory.hom (Types.Small.productIso fun i ↦ P.obj (op (X i))).hom) x)) ↔
    (ConcreteCategory.hom (firstMap P X π)) x = (ConcreteCategory.hom (secondMap P X π)) x

Tactic:
rw [Arrows.pullbackCompatible_iff]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type t
inst✝¹ : Small.{w, t} I
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).HasPairwisePullbacks
x : FirstObj P X
⊢ Arrows.PullbackCompatible P π
      ((equivShrink ((i : I) → P.obj (op (X i)))).symm
        ((ConcreteCategory.hom (Types.Small.productIso fun i ↦ P.obj (op (X i))).hom) x)) ↔
    (ConcreteCategory.hom (firstMap P X π)) x = (ConcreteCategory.hom (secondMap P X π)) x
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P₁ : Cᵒᵖ ⥤ Type w
P₂ : Cᵒᵖ ⥤ Type w'
e : ⦃X : C⦄ → P₁.obj (op X) ≃ P₂.obj (op X)
he :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₁.obj (op Y)),
    e ((ConcreteCategory.hom (P₁.map f.op)) x) = (ConcreteCategory.hom (P₂.map f.op)) (e x)
X✝ : C
R : Presieve X✝
h : IsSheafFor P₂ R
X Y : C
f : X ⟶ Y
x : P₂.obj (op Y)
⊢ e.symm ((ConcreteCategory.hom (P₂.map f.op)) x) = (ConcreteCategory.hom (P₁.map f.op)) (e.symm x)

Tactic:
obtain ⟨y, rfl⟩ := e.surjective x

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P₁ : Cᵒᵖ ⥤ Type w
P₂ : Cᵒᵖ ⥤ Type w'
e : ⦃X : C⦄ → P₁.obj (op X) ≃ P₂.obj (op X)
he :
  ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : P₁.obj (op Y)),
    e ((ConcreteCategory.hom (P₁.map f.op)) x) = (ConcreteCategory.hom (P₂.map f.op)) (e x)
X✝ : C
R : Presieve X✝
h : IsSheafFor P₂ R
X Y : C
f : X ⟶ Y
y : P₁.obj (op Y)
⊢ e.symm ((ConcreteCategory.hom (P₂.map f.op)) (e y)) = (ConcreteCategory.hom (P₁.map f.op)) (e.symm (e y))
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
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
⊢ ∀ ⦃X Y : Cᵒᵖ⦄ (f : X ⟶ Y),
    (J.plusObj P).map f ≫ colimMap (J.diagramNatTrans η (unop Y)) =
      colimMap (J.diagramNatTrans η (unop X)) ≫ (J.plusObj Q).map f

Tactic:
intro X Y f

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
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ (J.plusObj P).map f ≫ colimMap (J.diagramNatTrans η (unop Y)) =
    colimMap (J.diagramNatTrans η (unop X)) ≫ (J.plusObj Q).map f
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 : Cᵒᵖ⦄ (f : X ⟶ Y),
    P.map f ≫ ⊤.toMultiequalizer P ≫ colimit.ι (J.diagram P (unop Y)) (op ⊤) =
      (⊤.toMultiequalizer P ≫ colimit.ι (J.diagram P (unop X)) (op ⊤)) ≫ (J.plusObj P).map f

Tactic:
intro X Y f

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 : Cᵒᵖ
f : X ⟶ Y
⊢ P.map f ≫ ⊤.toMultiequalizer P ≫ colimit.ι (J.diagram P (unop Y)) (op ⊤) =
    (⊤.toMultiequalizer P ≫ colimit.ι (J.diagram P (unop X)) (op ⊤)) ≫ (J.plusObj P).map f
Module: Mathlib.CategoryTheory.Subfunctor.Image

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
⊢ range (𝟙 F) = ⊤

Tactic:
by aesop

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Image

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
G : Subfunctor F
⊢ range G.ι = G

Tactic:
by aesop

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Image

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F F' : C ⥤ Type w
p : F' ⟶ F
i : C
x : F.obj i
hx : x ∈ Set.range ⇑(ConcreteCategory.hom (p.app i))
⊢ ⟨x, hx⟩ ∈ Set.range ⇑(ConcreteCategory.hom ((toRange p).app i)) ↔ ⟨x, hx⟩ ∈ Set.univ

Tactic:
simp only [Set.mem_range, Set.mem_univ, iff_true]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F F' : C ⥤ Type w
p : F' ⟶ F
i : C
x : F.obj i
hx : x ∈ Set.range ⇑(ConcreteCategory.hom (p.app i))
⊢ ∃ y, (ConcreteCategory.hom ((toRange p).app i)) y = ⟨x, hx⟩
Module: Mathlib.CategoryTheory.Subfunctor.Image

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F F' F'' : C ⥤ Type w
f : F ⟶ F'
g : F' ⟶ F''
x✝² : C
x✝¹ : F''.obj x✝²
x✝ : x✝¹ ∈ (range (f ≫ g)).obj x✝²
⊢ x✝¹ ∈ (range g).obj x✝²

Tactic:
by aesop

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Image

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F F' : C ⥤ Type w
f : F ⟶ F'
⊢ ⊤.image f = range f

Tactic:
by aesop

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Image

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F F' : C ⥤ Type w
ι : Type u_1
G : ι → Subfunctor F
f : F ⟶ F'
⊢ (⨆ i, G i).image f = ⨆ i, (G i).image f

Tactic:
by aesop

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Image

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F F' F'' : C ⥤ Type w
G : Subfunctor F
f : F ⟶ F'
g : F' ⟶ F''
⊢ G.image (f ≫ g) = (G.image f).image g

Tactic:
by aesop

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Image

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F F' F'' : C ⥤ Type w
f : F ⟶ F'
g : F' ⟶ F''
⊢ range (f ≫ g) = (range f).image g

Tactic:
by aesop

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Image

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
G : Subfunctor F
⊢ G.preimage (𝟙 F) = G

Tactic:
by aesop

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Image

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F F' F'' : C ⥤ Type w
G : Subfunctor F
f : F'' ⟶ F'
g : F' ⟶ F
⊢ G.preimage (f ≫ g) = (G.preimage g).preimage f

Tactic:
by aesop

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subfunctor F
f : G.toFunctor ⟶ F'
h : Presieve.IsSheaf J F'
⊢ ∀ ⦃X Y : Cᵒᵖ⦄ (f_1 : X ⟶ Y),
    ((sheafify J G).toFunctor.map f_1 ≫ ↾fun s ↦ ⋯.amalgamate ((G.familyOfElementsOfSection ↑s).map f) ⋯) =
      (↾fun s ↦ ⋯.amalgamate ((G.familyOfElementsOfSection ↑s).map f) ⋯) ≫ F'.map f_1

Tactic:
intro U V i

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subfunctor F
f : G.toFunctor ⟶ F'
h : Presieve.IsSheaf J F'
U V : Cᵒᵖ
i : U ⟶ V
⊢ ((sheafify J G).toFunctor.map i ≫ ↾fun s ↦ ⋯.amalgamate ((G.familyOfElementsOfSection ↑s).map f) ⋯) =
    (↾fun s ↦ ⋯.amalgamate ((G.familyOfElementsOfSection ↑s).map f) ⋯) ≫ F'.map i
Module: Mathlib.CategoryTheory.Sites.Subsheaf

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' : Cᵒᵖ ⥤ Type w
G : Subfunctor F
f : G.toFunctor ⟶ F'
h : Presieve.IsSheaf J F'
U : Cᵒᵖ
s : G.toFunctor.obj U
V : C
i : V ⟶ unop U
hi : (G.sieveOfSection ↑((ConcreteCategory.hom ((homOfLe ⋯).app U)) s)).arrows i
⊢ (ConcreteCategory.hom (F'.map i.op)) ((ConcreteCategory.hom ((homOfLe ⋯ ≫ G.sheafifyLift f h).app U)).toFun s) =
    (ConcreteCategory.hom (F'.map i.op)) ((ConcreteCategory.hom (f.app U)).toFun s)

Tactic:
have := elementwise_of% f.naturality

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' : Cᵒᵖ ⥤ Type w
G : Subfunctor F
f : G.toFunctor ⟶ F'
h : Presieve.IsSheaf J F'
U : Cᵒᵖ
s : G.toFunctor.obj U
V : C
i : V ⟶ unop U
hi : (G.sieveOfSection ↑((ConcreteCategory.hom ((homOfLe ⋯).app U)) s)).arrows i
this :
  ∀ ⦃X Y : Cᵒᵖ⦄ (f_1 : X ⟶ Y) (x : G.toFunctor.obj X),
    (ConcreteCategory.hom (f.app Y)) ((ConcreteCategory.hom (G.toFunctor.map f_1)) x) =
      (ConcreteCategory.hom (F'.map f_1)) ((ConcreteCategory.hom (f.app X)) x)
⊢ (ConcreteCategory.hom (F'.map i.op)) ((ConcreteCategory.hom ((homOfLe ⋯ ≫ G.sheafifyLift f h).app U)).toFun s) =
    (ConcreteCategory.hom (F'.map i.op)) ((ConcreteCategory.hom (f.app U)).toFun s)
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁵ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁴ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝³ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : J.Cover X) (x y : ToType (P.obj (op X))),
    (∀ (I : S.Arrow), (ConcreteCategory.hom (P.map I.f.op)) x = (ConcreteCategory.hom (P.map I.f.op)) y) → x = y
X : C
S : J.Cover X
s : Meq (J.plusObj P) S
T : (I : S.Arrow) → J.Cover I.Y
t : (I : S.Arrow) → Meq P (T I)
ht : ∀ (I : S.Arrow), ↑s I = mk (t I)
II : (S.bind T).Relation
⊢ (ConcreteCategory.hom ((J.plusObj P).map II.r.g₁.op))
      ((ConcreteCategory.hom ((J.toPlus P).app (op II.fst.Y))) ((fun I ↦ ↑(t I.fromMiddle) I.toMiddle) II.fst)) =
    (ConcreteCategory.hom ((J.plusObj P).map II.r.g₂.op))
      ((ConcreteCategory.hom ((J.toPlus P).app (op II.snd.Y))) ((fun I ↦ ↑(t I.fromMiddle) I.toMiddle) II.snd))

Tactic:
erw [toPlus_apply (T II.fst.fromMiddle) (t II.fst.fromMiddle) II.fst.toMiddle,
      toPlus_apply (T II.snd.fromMiddle) (t II.snd.fromMiddle) II.snd.toMiddle]

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁵ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁴ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝³ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
P : Cᵒᵖ ⥤ D
hsep :
  ∀ (X : C) (S : J.Cover X) (x y : ToType (P.obj (op X))),
    (∀ (I : S.Arrow), (ConcreteCategory.hom (P.map I.f.op)) x = (ConcreteCategory.hom (P.map I.f.op)) y) → x = y
X : C
S : J.Cover X
s : Meq (J.plusObj P) S
T : (I : S.Arrow) → J.Cover I.Y
t : (I : S.Arrow) → Meq P (T I)
ht : ∀ (I : S.Arrow), ↑s I = mk (t I)
II : (S.bind T).Relation
⊢ (ConcreteCategory.hom ((J.plusObj P).map II.r.g₁.op))
      ((ConcreteCategory.hom ((J.plusObj P).map II.fst.toMiddle.f.op)) (mk (t II.fst.fromMiddle))) =
    (ConcreteCategory.hom ((J.plusObj P).map II.r.g₂.op))
      ((ConcreteCategory.hom ((J.plusObj P).map II.snd.toMiddle.f.op)) (mk (t II.snd.fromMiddle)))
Module: Mathlib.CategoryTheory.Sites.Subsheaf

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G G' : Subfunctor F
h : G ≤ G'
hF : Presieve.IsSheaf J F
hG' : Presieve.IsSheaf J G'.toFunctor
U : Cᵒᵖ
x : F.obj U
hx : x ∈ (sheafify J G).obj U
V : C
i : V ⟶ unop U
hi : (G.sieveOfSection x).arrows i
this :
  ↑((ConcreteCategory.hom ((homOfLe ⋯ ≫ G.sheafifyLift (homOfLe h) hG').app (op V)))
        ⟨(ConcreteCategory.hom (F.map i.op)) x, hi⟩) =
    ↑((ConcreteCategory.hom ((homOfLe h).app (op V))) ⟨(ConcreteCategory.hom (F.map i.op)) x, hi⟩)
⊢ (ConcreteCategory.hom (F.map i.op)) x =
    (ConcreteCategory.hom (F.map i.op)) ↑((ConcreteCategory.hom ((G.sheafifyLift (homOfLe h) hG').app U)) ⟨x, hx⟩)

Tactic:
convert! this.symm

Goal state after:
case e'_3
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G G' : Subfunctor F
h : G ≤ G'
hF : Presieve.IsSheaf J F
hG' : Presieve.IsSheaf J G'.toFunctor
U : Cᵒᵖ
x : F.obj U
hx : x ∈ (sheafify J G).obj U
V : C
i : V ⟶ unop U
hi : (G.sieveOfSection x).arrows i
this :
  ↑((ConcreteCategory.hom ((homOfLe ⋯ ≫ G.sheafifyLift (homOfLe h) hG').app (op V)))
        ⟨(ConcreteCategory.hom (F.map i.op)) x, hi⟩) =
    ↑((ConcreteCategory.hom ((homOfLe h).app (op V))) ⟨(ConcreteCategory.hom (F.map i.op)) x, hi⟩)
⊢ (ConcreteCategory.hom (F.map i.op)) ↑((ConcreteCategory.hom ((G.sheafifyLift (homOfLe h) hG').app U)) ⟨x, hx⟩) =
    ↑((ConcreteCategory.hom ((homOfLe ⋯ ≫ G.sheafifyLift (homOfLe h) hG').app (op V)))
        ⟨(ConcreteCategory.hom (F.map i.op)) x, hi⟩)