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

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
D : Type u''
inst✝⁷ : Category.{v'', u''} D
F : C ⥤ D
inst✝⁶ : FinitaryExtensive D
inst✝⁵ : HasFiniteCoproducts C
inst✝⁴ : HasPullbacksOfInclusions C
inst✝³ : PreservesPullbacksOfInclusions F
inst✝² : ReflectsLimitsOfShape WalkingCospan F
inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) F
inst✝ : ReflectsColimitsOfShape (Discrete WalkingPair) F
X Y : C
⊢ ∀ (c : BinaryCofan X Y) (a : IsColimit c), IsVanKampenColimit c

Tactic:
c

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
D : Type u''
inst✝⁷ : Category.{v'', u''} D
F : C ⥤ D
inst✝⁶ : FinitaryExtensive D
inst✝⁵ : HasFiniteCoproducts C
inst✝⁴ : HasPullbacksOfInclusions C
inst✝³ : PreservesPullbacksOfInclusions F
inst✝² : ReflectsLimitsOfShape WalkingCospan F
inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) F
inst✝ : ReflectsColimitsOfShape (Discrete WalkingPair) F
X Y : C
c : BinaryCofan X Y
⊢ ∀ (a : IsColimit c), IsVanKampenColimit c
Module: Mathlib.CategoryTheory.Localization.Bousfield

Goal state before:
pp: case mpr.left
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
Y Z : C
g : Y ⟶ Z
hg : P.isColocal g
X X' : C
hX' : P X'
e : X ≅ X'
f₁ f₂ : X ⟶ Y
eq : (fun f ↦ f ≫ g) f₁ = (fun f ↦ f ≫ g) f₂
⊢ e.inv ≫ f₁ = e.inv ≫ f₂

Tactic:
apply (hg _ hX').1

Goal state after:
case mpr.left
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
Y Z : C
g : Y ⟶ Z
hg : P.isColocal g
X X' : C
hX' : P X'
e : X ≅ X'
f₁ f₂ : X ⟶ Y
eq : (fun f ↦ f ≫ g) f₁ = (fun f ↦ f ≫ g) f₂
⊢ (fun f ↦ f ≫ g) (e.inv ≫ f₁) = (fun f ↦ f ≫ g) (e.inv ≫ f₂)
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: 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) (f_1 : c'.pt ⟶ (extendCofan c₁ c₂).pt),
    α ≫ (extendCofan c₁ c₂).ι = c'.ι ≫ (const (Discrete (Fin (n + 1)))).map f_1 →
      NatTrans.Equifibered α →
        (∀ (j : Discrete (Fin (n + 1))), IsPullback (c'.ι.app j) (α.app j) f_1 ((extendCofan c₁ c₂).ι.app j)) →
          Nonempty (IsColimit c')

Tactic:
c

Goal state after:
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) (f_1 : c.pt ⟶ (extendCofan c₁ c₂).pt),
    α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ (const (Discrete (Fin (n + 1)))).map f_1 →
      NatTrans.Equifibered α →
        (∀ (j : Discrete (Fin (n + 1))), IsPullback (c.ι.app j) (α.app j) f_1 ((extendCofan c₁ c₂).ι.app j)) →
          Nonempty (IsColimit c)
Module: Mathlib.CategoryTheory.Sites.PreservesSheafification

Goal state before:
pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u_1
B : Type u_2
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Category.{v_2, u_2} B
F : A ⥤ B
G₁ : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : (Cᵒᵖ ⥤ B) ⥤ Sheaf J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
h : ∀ (P : Cᵒᵖ ⥤ A), J.W (whiskerRight (adj₁.unit.app P) F)
P₁ P₂ : Cᵒᵖ ⥤ A
f : P₁ ⟶ P₂
hf : IsIso (G₁.map f)
⊢ J.W.inverseImage ((whiskeringRight Cᵒᵖ A B).obj F) f

Tactic:
dsimp [MorphismProperty.inverseImage]

Goal state after:
case mpr
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u_1
B : Type u_2
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Category.{v_2, u_2} B
F : A ⥤ B
G₁ : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : (Cᵒᵖ ⥤ B) ⥤ Sheaf J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
h : ∀ (P : Cᵒᵖ ⥤ A), J.W (whiskerRight (adj₁.unit.app P) F)
P₁ P₂ : Cᵒᵖ ⥤ A
f : P₁ ⟶ P₂
hf : IsIso (G₁.map f)
⊢ J.W (whiskerRight f F)
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₁ F₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst✝ : IsLocallySurjective J (f₁ ≫ f₂)
X : C
x : ToType (F₃.obj (op X))
⊢ imageSieve (f₁ ≫ f₂) x ≤ imageSieve f₂ x

Tactic:
intro Y g hg

Goal state after:
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₃
inst✝ : IsLocallySurjective J (f₁ ≫ f₂)
X : C
x : ToType (F₃.obj (op X))
Y : C
g : Y ⟶ X
hg : (imageSieve (f₁ ≫ f₂) x).arrows g
⊢ (imageSieve f₂ x).arrows g
Module: Mathlib.CategoryTheory.Sites.LocallyBijective

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
f : F ⟶ G
h₁ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom (f.hom.app X))
right✝ : IsLocallySurjective f
X : Cᵒᵖ
s : G.obj.obj X
H : Presieve.IsSheafFor F.obj (Presheaf.imageSieve f.hom s).arrows
t : Presieve.FamilyOfElements F.obj (Presheaf.imageSieve f.hom s).arrows := ⋯
ht : t.Compatible
⊢ ∀ ⦃Y : C⦄ ⦃f_1 : Y ⟶ Opposite.unop X⦄,
    (Presheaf.imageSieve f.hom s).arrows f_1 →
      (ConcreteCategory.hom (G.obj.map f_1.op)) ((ConcreteCategory.hom (f.hom.app X)) (H.amalgamate t ht)) =
        (ConcreteCategory.hom (G.obj.map f_1.op)) s

Tactic:
intro Y g hg

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
f : F ⟶ G
h₁ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom (f.hom.app X))
right✝ : IsLocallySurjective f
X : Cᵒᵖ
s : G.obj.obj X
H : Presieve.IsSheafFor F.obj (Presheaf.imageSieve f.hom s).arrows
t : Presieve.FamilyOfElements F.obj (Presheaf.imageSieve f.hom s).arrows :=
  fun Y g hg ↦ Presheaf.localPreimage f.hom s g hg
ht : t.Compatible
Y : C
g : Y ⟶ Opposite.unop X
hg : (Presheaf.imageSieve f.hom s).arrows g
⊢ (ConcreteCategory.hom (G.obj.map g.op)) ((ConcreteCategory.hom (f.hom.app X)) (H.amalgamate t ht)) =
    (ConcreteCategory.hom (G.obj.map g.op)) s
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: 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
F : Discrete (Fin (n + 1)) ⥤ C
⊢ ∀ (c' : Cocone F) (α : F ⟶ Discrete.functor f) (f_1 : c'.pt ⟶ (extendCofan c₁ c₂).pt),
    α ≫ (extendCofan c₁ c₂).ι = c'.ι ≫ (const (Discrete (Fin (n + 1)))).map f_1 →
      NatTrans.Equifibered α →
        (Nonempty (IsColimit c') ↔
          ∀ (j : Discrete (Fin (n + 1))), IsPullback (c'.ι.app j) (α.app j) f_1 ((extendCofan c₁ c₂).ι.app j))

Tactic:
c

Goal state after:
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
F : Discrete (Fin (n + 1)) ⥤ C
c : Cocone F
⊢ ∀ (α : F ⟶ Discrete.functor f) (f_1 : c.pt ⟶ (extendCofan c₁ c₂).pt),
    α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ (const (Discrete (Fin (n + 1)))).map f_1 →
      NatTrans.Equifibered α →
        (Nonempty (IsColimit c) ↔
          ∀ (j : Discrete (Fin (n + 1))), IsPullback (c.ι.app j) (α.app j) f_1 ((extendCofan c₁ c₂).ι.app j))
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify

Goal state before:
pp: case hm₀
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ R : Cᵒᵖ ⥤ RingCat
α : R₀ ⟶ R
inst✝¹ : Presheaf.IsLocallyInjective J α
M₀ : PresheafOfModules R₀
A : Cᵒᵖ ⥤ AddCommGrpCat
φ : M₀.presheaf ⟶ A
inst✝ : Presheaf.IsLocallyInjective J φ
hA : Presheaf.IsSeparated J A
X : C
r : ↑(R.obj (Opposite.op X))
m : ↑(A.obj (Opposite.op X))
Y Z : C
f : Y ⟶ X
g : Z ⟶ Y
r₀ : ↑(R₀.obj (Opposite.op Y))
r₀' : ↑(R₀.obj (Opposite.op Z))
m₀ : ↑(M₀.obj (Opposite.op Y))
m₀' : ↑(M₀.obj (Opposite.op Z))
hr₀ : (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀ = (ConcreteCategory.hom (R.map f.op)) r
hr₀' : (ConcreteCategory.hom (α.app (Opposite.op Z))) r₀' = (ConcreteCategory.hom (R.map (f.op ≫ g.op))) r
hm₀ : (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀ = (ConcreteCategory.hom (A.map f.op)) m
hm₀' : (ConcreteCategory.hom (φ.app (Opposite.op Z))) m₀' = (ConcreteCategory.hom (A.map (f.op ≫ g.op))) m
⊢ (ConcreteCategory.hom (φ.app (Opposite.op Z))) ((ConcreteCategory.hom (M₀.map g.op)) m₀) =
    (ConcreteCategory.hom (φ.app (Opposite.op Z))) m₀'

Tactic:
rw [hm₀', A.map_comp, AddCommGrpCat.coe_comp, Function.comp_apply, ← hm₀]

Goal state after:
case hm₀
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ R : Cᵒᵖ ⥤ RingCat
α : R₀ ⟶ R
inst✝¹ : Presheaf.IsLocallyInjective J α
M₀ : PresheafOfModules R₀
A : Cᵒᵖ ⥤ AddCommGrpCat
φ : M₀.presheaf ⟶ A
inst✝ : Presheaf.IsLocallyInjective J φ
hA : Presheaf.IsSeparated J A
X : C
r : ↑(R.obj (Opposite.op X))
m : ↑(A.obj (Opposite.op X))
Y Z : C
f : Y ⟶ X
g : Z ⟶ Y
r₀ : ↑(R₀.obj (Opposite.op Y))
r₀' : ↑(R₀.obj (Opposite.op Z))
m₀ : ↑(M₀.obj (Opposite.op Y))
m₀' : ↑(M₀.obj (Opposite.op Z))
hr₀ : (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀ = (ConcreteCategory.hom (R.map f.op)) r
hr₀' : (ConcreteCategory.hom (α.app (Opposite.op Z))) r₀' = (ConcreteCategory.hom (R.map (f.op ≫ g.op))) r
hm₀ : (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀ = (ConcreteCategory.hom (A.map f.op)) m
hm₀' : (ConcreteCategory.hom (φ.app (Opposite.op Z))) m₀' = (ConcreteCategory.hom (A.map (f.op ≫ g.op))) m
⊢ (ConcreteCategory.hom (φ.app (Opposite.op Z))) ((ConcreteCategory.hom (M₀.map g.op)) m₀) =
    (ConcreteCategory.hom (A.map g.op)) ((ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀)
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
n : ℕ
h : HasProjectiveDimensionLT X (n + 1)
i : ℕ
hi : ↑n < ↑i
⊢ n + 1 ≤ i

Tactic:
by simpa using hi

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasCoproducts C
R : C
J : Type u'
x✝ : Category.{v', u'} J
K : J ⥤ Type w
c : Cocone K
hc : (K.coconeTypesEquiv.symm c).IsColimit
⊢ IsColimit ((sigmaConst.obj R).mapCocone c)

Tactic:
let coconeTypes (s : Cocone (K ⋙ sigmaConst.obj R)) : K.CoconeTypes :=
      { pt := R ⟶ s.pt
        ι j k := Sigma.ι (fun _ ↦ R) k ≫ s.ι.app j
        ι_naturality g := by ext; simp [← s.w g] }

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasCoproducts C
R : C
J : Type u'
x✝ : Category.{v', u'} J
K : J ⥤ Type w
c : Cocone K
hc : (K.coconeTypesEquiv.symm c).IsColimit
coconeTypes : Cocone (K ⋙ sigmaConst.obj R) → K.CoconeTypes :=
  fun s ↦ { pt := R ⟶ s.pt, ι := fun j k ↦ Sigma.ι (fun x ↦ R) k ≫ s.ι.app j, ι_naturality := ⋯ }
⊢ IsColimit ((sigmaConst.obj R).mapCocone c)
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case diagram
J : Type v₁
inst✝¹ : SmallCategory J
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : J ⥤ C
c₁ c₂ : Cone F
j✝ k✝ : J
f : j✝ ⟶ k✝
⊢ (Bicone.casesOn (Bicone.diagram j✝) c₁.pt c₂.pt fun j ↦ F.obj j) ⟶
    Bicone.casesOn (Bicone.diagram k✝) c₁.pt c₂.pt fun j ↦ F.obj j

Tactic:
exact F.map f

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

Goal state before:
pp: case a
C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreZeroHypercover S
F : PreZeroHypercover S
⊢ Presieve.ofArrows (E.sum F).X (E.sum F).f ≤ Presieve.ofArrows E.X E.f ⊔ Presieve.ofArrows F.X F.f

Tactic:
intro Z g ⟨i⟩

Goal state after:
case a
C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreZeroHypercover S
F : PreZeroHypercover S
Z : C
g : Z ⟶ S
i : (E.sum F).I₀
⊢ (Presieve.ofArrows E.X E.f ⊔ Presieve.ofArrows F.X F.f) ((E.sum F).f i)
Module: Mathlib.CategoryTheory.Sites.Closed

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
⊢ J₁ = J₂ ↔ ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P

Tactic:
by
  constructor
  · rintro rfl
    intro P
    rfl
  · intro h
    apply le_antisymm
    · apply le_topology_of_closedSieves_isSheaf
      rw [h]
      apply classifier_isSheaf
    · apply le_topology_of_closedSieves_isSheaf
      rw [← h]
      apply classifier_isSheaf

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
X : C
S T : Sieve X
h : S ≤ T
hS : K.Saturate X S
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → K.Saturate Y (Sieve.pullback f T)

Tactic:
intro Y g hg

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
X : C
S T : Sieve X
h : S ≤ T
hS : K.Saturate X S
Y : C
g : Y ⟶ X
hg : S.arrows g
⊢ K.Saturate Y (Sieve.pullback g T)
Module: Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf

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
H : J.OneHypercoverFamily
P : Cᵒᵖ ⥤ A
inst✝ : H.IsGenerating
⊢ Presheaf.IsSheaf J P → ∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (IsLimit (E.multifork P))

pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
H : J.OneHypercoverFamily
P : Cᵒᵖ ⥤ A
inst✝ : H.IsGenerating
⊢ (∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (IsLimit (E.multifork P))) → Presheaf.IsSheaf J P

Tactic:
· intro hP X E _
    exact ⟨E.isLimitMultifork ⟨_, hP⟩⟩

Goal state after:
case mpr
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
H : J.OneHypercoverFamily
P : Cᵒᵖ ⥤ A
inst✝ : H.IsGenerating
⊢ (∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (IsLimit (E.multifork P))) → Presheaf.IsSheaf J P
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.PreservesRightKanExtensions L
inst✝¹ : ∀ (F : A ⥤ B), L.HasRightKanExtension F
inst✝ : ∀ (F : A ⥤ D), L.HasRightKanExtension F
F F' : A ⥤ B
η : F ⟶ F'
⊢ (L.ran ⋙ (whiskeringRight C B D).obj G).map η ≫ (G.rightKanExtensionCompIsoOfPreserves F' L).hom =
    (G.rightKanExtensionCompIsoOfPreserves F L).hom ≫ ((whiskeringRight A B D).obj G ⋙ L.ran).map η

Tactic:
apply hom_ext_of_isRightKanExtension
        (L.rightKanExtension <| F' ⋙ G)
        (L.rightKanExtensionCounit <| F' ⋙ G)
      dsimp [ran]
      ext
      simp only [comp_obj, Category.assoc, rightKanExtensionCompIsoOfPreserves_hom_fac,
        NatTrans.comp_app, whiskerLeft_app, whiskerRight_app, associator_inv_app, Category.id_comp,
        liftOfIsRightKanExtension_fac, rightKanExtensionCompIsoOfPreserves_hom_fac_assoc,
        ← G.map_comp]
      simp

Goal state after:
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
S✝ T✝ : C
f : S✝ ⟶ T✝
hf : IsIso f
⊢ Presieve.singleton f ∈ J.toPrecoverage.coverings T✝

Tactic:
simp [mem_toPrecoverage_iff]

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
F : C ⥤ D
J : Precoverage C
K : Precoverage D
inst✝⁴ : J.IsStableUnderBaseChange
inst✝³ : J.HasPullbacks
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.HasPullbacks
inst✝ : J.PullbacksPreservedBy F
h : J ≤ Precoverage.comap F K
x✝ : Sheaf K.toGrothendieck (Type (max u₁ v₁ u₂ v₂))
G : Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
H✝ : Presheaf.IsSheaf K.toGrothendieck G
H : Presieve.IsSheaf K.toGrothendieck G
⊢ Presieve.IsSheaf J.toGrothendieck (F.op ⋙ { obj := G, property := H✝ }.obj)

Tactic:
rw [← Precoverage.toGrothendieck_toCoverage, Presieve.isSheaf_coverage] at H ⊢

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
F : C ⥤ D
J : Precoverage C
K : Precoverage D
inst✝⁴ : J.IsStableUnderBaseChange
inst✝³ : J.HasPullbacks
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.HasPullbacks
inst✝ : J.PullbacksPreservedBy F
h : J ≤ Precoverage.comap F K
x✝ : Sheaf K.toGrothendieck (Type (max u₁ v₁ u₂ v₂))
G : Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
H✝ : Presheaf.IsSheaf K.toGrothendieck G
H : ∀ {X : D}, ∀ R ∈ K.toCoverage.coverings X, Presieve.IsSheafFor G R
⊢ ∀ {X : C}, ∀ R ∈ J.toCoverage.coverings X, Presieve.IsSheafFor (F.op ⋙ { obj := G, property := H✝ }.obj) R
Module: Mathlib.CategoryTheory.Sites.CoverLifting

Goal state before:
pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
h : CoverPreserving K J G
⊢ ∀ {U : C} {S : Sieve (F.obj U)}, S ∈ K (F.obj U) → Sieve.functorPullback F S ∈ J U

Tactic:
intro U S hS
    refine J.superset_covering ?_ (J.pullback_stable (adj.unit.app U) <| h.cover_preserve hS)
    intro X f ⟨Y, g, u, hg, heq⟩
    suffices F.map f = (adj.homEquiv _ _).symm u ≫ g by
      simp [this, S.downward_closed hg]
    simp [← Adjunction.homEquiv_naturality_right_symm, ← heq,
      Adjunction.homEquiv_naturality_left_symm]

Goal state after:
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 ⋙ uliftFunctor.{?u.32, w})

Tactic:
refine Presieve.isSheaf_iso (canonicalTopology C) (P ⋙ uliftFunctor.{v}).uliftYonedaReprXIso ?_

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

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
h : ∀ {Z : C} (f : X ⟶ Z) [Epi f], IsIso f ↔ f ≠ 0
Y : C
f : Y ⟶ X
I : Mono f
⊢ f ≠ 0 → IsIso f

Tactic:
· intro hf
      suffices Epi f by exact isIso_of_mono_of_epi _
      apply Preadditive.epi_of_cokernel_zero
      by_contra h'
      exact cokernel_not_iso_of_nonzero hf ((h _).mpr h')

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

Goal state before:
pp: C : Type u
inst✝¹ : Preorder C
J : Type u'
inst✝ : Category.{v, u'} J
F : J ⥤ C
c : Cone F
⊢ c.pt ∈ lowerBounds (Set.range F.obj)

Tactic:
intro x ⟨i, p⟩; rw [← p]; exact (c.π.app i).le

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

Goal state before:
pp: C : Type u
inst✝ : CompleteLattice C
ι : Type u_1
X : ι → C
⊢ IsLUB (Set.range (Discrete.functor X).obj) (Cofan.mk (⨆ i, X i) fun i ↦ homOfLE ⋯).pt

Tactic:
simp [isLUB_iSup]

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

Goal state before:
pp: X Y Z : TopCat
U V W : Opens ↑X
⊢ Function.Injective fun f ↦ Set.inclusion ⋯

Tactic:
by rintro ⟨⟨_⟩⟩ _ _; congr!

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

Goal state before:
pp: X Y : TopCat
f : X ⟶ Y
x : ↑X
U V W : OpenNhds x
⊢ Function.Injective fun f ↦ Set.inclusion ⋯

Tactic:
by rintro ⟨⟨_⟩⟩ _ _; congr!

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

Goal state before:
pp: X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ⇑(ConcreteCategory.hom f)
U : Opens ↑X
S : Sieve U
hU : S ∈ (Opens.grothendieckTopology ↑X) U
x : ↑X
hx : x ∈ ↑U
V : Opens ↑X
i : V ⟶ U
hV : S.arrows i
hxV : x ∈ V
⊢ ∃ U_1 f_1, (Sieve.functorPushforward hf.functor S).arrows f_1 ∧ (ConcreteCategory.hom f) x ∈ U_1

Tactic:
exact ⟨_, hf.functor.map i, ⟨_, i, 𝟙 _, hV, rfl⟩, Set.mem_image_of_mem f hxV⟩

Goal state after:
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
F : Presheaf C Y
U : Opens ↑X
x : ↑X
hx : x ∈ U
⊢ germToPullbackStalk C f F U x hx ≫ stalkPullbackHom C f F x = ((pullback C f).obj F).germ U x hx

Tactic:
by
  ext V hV
  dsimp
  simp only [pullbackPushforwardAdjunction_unit_pullback_map_germToPullbackStalk_assoc,
    germ_stalkPullbackHom, germ_res]

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasLimitsOfSize.{x, x, v_1, u_1} C
inst✝¹ : (CategoryTheory.forget C).ReflectsIsomorphisms
inst✝ : PreservesLimitsOfSize.{x, x, v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget C)
X : TopCat
F : Sheaf C X
ι : Type u_4
U : ι → Opens ↑X
V : Opens ↑X
G : Sheaf C X
f : F ⟶ G
s : ToType (F.obj.obj (op (iSup U)))
t : ToType (G.obj.obj (op V))
sf : (i : ι) → ToType (F.obj.obj (op (U i)))
h : IsGluing F.obj U sf s
hV : ∀ (i : ι), U i ≤ V
ht :
  ∀ (i : ι), (ConcreteCategory.hom (f.hom.app (op (U i)))) (sf i) = (ConcreteCategory.hom (G.obj.map (homOfLE ⋯).op)) t
⊢ iSup U ≤ V

Tactic:
aesop_cat

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

Goal state before:
pp: ι : 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 ι
x : ι → R
⊢ f x = ∑ i, x i • f fun j ↦ if i = j then 1 else 0

Tactic:
exact f.pi_apply_eq_sum_univ x

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

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
inst✝⁹ : Semiring R₁
inst✝⁸ : Semiring R₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst✝⁷ : RingHomInvPair σ₁₂ σ₂₁
inst✝⁶ : RingHomInvPair σ₂₁ σ₁₂
M₁ : Type u_4
inst✝⁵ : TopologicalSpace M₁
inst✝⁴ : AddCommMonoid M₁
M₂ : Type u_5
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₁ M₁
inst✝ : Module R₂ M₂
e : M₁ ≃SL[σ₁₂] M₂
⊢ ⇑e ∘ ⇑e.symm = id

Tactic:
by
  ext x
  exact apply_symm_apply e x

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantTo i₀
inst✝ : IsCofiltered J
j j' : J
α : j' ⟶ i₀
β : j' ⟶ j
s : J
γ : s ⟶ IsCofiltered.min i₀ j
δ : s ⟶ j'
h₁ : γ ≫ minToRight i₀ j = δ ≫ β
h₂ : γ ≫ minToLeft i₀ j = δ ≫ α
⊢ F.map δ ≫ F.map α ≫ (h.isoMap (minToLeft i₀ j) ⋯).inv ≫ F.map (minToRight i₀ j) = F.map δ ≫ F.map β

Tactic:
← F.map_comp δ β,

Goal state after:
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantTo i₀
inst✝ : IsCofiltered J
j j' : J
α : j' ⟶ i₀
β : j' ⟶ j
s : J
γ : s ⟶ IsCofiltered.min i₀ j
δ : s ⟶ j'
h₁ : γ ≫ minToRight i₀ j = δ ≫ β
h₂ : γ ≫ minToLeft i₀ j = δ ≫ α
⊢ F.map δ ≫ F.map α ≫ (h.isoMap (minToLeft i₀ j) ⋯).inv ≫ F.map (minToRight i₀ j) = F.map (δ ≫ β)
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X : TopModuleCat R
⊢ Continuous ((Finsupp.lift (↑((𝟭 (TopModuleCat R)).obj X).toModuleCat) R ↑X.toModuleCat) id).toFun

Tactic:
by
      rw [continuous_iff_le_induced]
      refine sInf_le ⟨continuousSMul_induced (Finsupp.lift _ R X id),
        continuousAdd_induced (Finsupp.lift _ R X id), ?_⟩
      rw [coinduced_le_iff_le_induced, induced_compose]
      convert! induced_id.symm.le
      ext
      simp [coe_freeObj]

Goal state after: