mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: 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 := ⋯
F : PreZeroHypercover S := ⋯
e : E ≅ F := ⋯
hER : E.presieve₀ = R
hFT : F.presieve₀ = T
⊢ E.presieve₀ ∈ J.coverings S

Tactic:
hER

Goal state after:
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 }
e : E ≅ F :=
  PreZeroHypercover.isoMk (Equiv.refl E.I₀)
    (fun i ↦
      match i with
      | Sum.inl i => id (eR (↑i).snd ⋯).symm
      | Sum.inr i => id (eT (↑i).snd ⋯))
    ⋯
hER : E.presieve₀ = R
hFT : F.presieve₀ = T
⊢ R ∈ J.coverings S
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
X Y : C
f : Y ⟶ X
S : Sieve X
h : K.Saturate X S
⊢ K.Saturate Y (Sieve.pullback f S)

Tactic:
induction h with
  | of X S hS =>
    obtain ⟨R, hR1, hR2⟩ := K.pullback f S hS
    suffices Sieve.generate R ≤ (Sieve.generate S).pullback f from
      saturate_of_superset _ this (Saturate.of _ _ hR1)
    intro Z g ⟨W, i, e, h1, h2⟩
    obtain ⟨WW, ii, ee, hh1, hh2⟩ := hR2 h1
    refine ⟨WW, i ≫ ii, ee, hh1, ?_⟩
    simp [hh2, reassoc_of% h2]
  | top X => exact .top _
  | transitive X R S _ hS H1 _ =>
    refine (H1 f).transitive _ _ _ fun Z g hg ↦ ?_
    rw [← Sieve.pullback_comp]
    exact hS hg

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

Goal state before:
pp: case a
C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
⊢ ∀ b ∈ {J | K ≤ J.toCoverage}, K.toGrothendieck ≤ b

Tactic:
intro J hJ X S hS

Goal state after:
case a
C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
J : GrothendieckTopology C
hJ : J ∈ {J | K ≤ J.toCoverage}
X : C
S : Sieve X
hS : S ∈ K.toGrothendieck X
⊢ S ∈ J X
Module: Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf

Goal state before:
pp: 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
hP : ∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (IsLimit (E.multifork P))
X : C
S : Sieve X
E : J.OneHypercover X
hE : H E
le : E.sieve₀ ≤ S
inst✝ : H.IsGenerating
F : Multifork (Cover.index ⟨S, ⋯⟩ P)
m : F.pt ⟶ (Cover.multifork ⟨S, ⋯⟩ P).pt
hm : ∀ (i : (Cover.shape ⟨S, ⋯⟩).L), m ≫ (Cover.multifork ⟨S, ⋯⟩ P).ι i = F.ι i
⊢ ∀ ⦃Y : C⦄ (f : Y ⟶ X), S.arrows f → m ≫ P.map f.op = lift hP hE le F ≫ P.map f.op

Tactic:
intro Y f hf

Goal state after:
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
hP : ∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (IsLimit (E.multifork P))
X : C
S : Sieve X
E : J.OneHypercover X
hE : H E
le : E.sieve₀ ≤ S
inst✝ : H.IsGenerating
F : Multifork (Cover.index ⟨S, ⋯⟩ P)
m : F.pt ⟶ (Cover.multifork ⟨S, ⋯⟩ P).pt
hm : ∀ (i : (Cover.shape ⟨S, ⋯⟩).L), m ≫ (Cover.multifork ⟨S, ⋯⟩ P).ι i = F.ι i
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ m ≫ P.map f.op = lift hP hE le F ≫ P.map f.op
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.PreservesPointwiseRightKanExtension F L
inst✝ : L.HasPointwiseRightKanExtension F
a : A
⊢ (G.pointwiseRightKanExtensionCompIsoOfPreserves F L).inv.app (L.obj a) ≫
      G.map ((L.pointwiseRightKanExtensionCounit F).app a) =
    (L.pointwiseRightKanExtensionCounit (F ⋙ G)).app a

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

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : RepresentablyFlat G
ℱ : Sheaf K (Type u_1)
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.obj) T
hx : x.Compatible
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
e : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
c : Cone (cospan g₁ g₂ ⋙ G) :=
  (Cone.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)
c' : Cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G) :=
  IsCofiltered.cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G)
eq₁ : f₁ = (c'.pt.hom ≫ G.map (StructuredArrow.Hom.right (c'.π.app left))) ≫ eqToHom ⋯
eq₂ : f₂ = (c'.pt.hom ≫ G.map (StructuredArrow.Hom.right (c'.π.app right))) ≫ eqToHom ⋯
⊢ (ConcreteCategory.hom (ℱ.obj.map c'.pt.hom.op))
      ((ConcreteCategory.hom (ℱ.obj.map (G.map (StructuredArrow.Hom.right (c'.π.app left))).op))
        ((ConcreteCategory.hom (eqToHom ⋯)) (x g₁ hg₁))) =
    (ConcreteCategory.hom (ℱ.obj.map c'.pt.hom.op))
      ((ConcreteCategory.hom (ℱ.obj.map (G.map (StructuredArrow.Hom.right (c'.π.app right))).op))
        ((ConcreteCategory.hom (eqToHom ⋯)) (x g₂ hg₂)))

Tactic:
apply congr_arg

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : RepresentablyFlat G
ℱ : Sheaf K (Type u_1)
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.obj) T
hx : x.Compatible
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
e : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
c : Cone (cospan g₁ g₂ ⋙ G) := ⋯
c' : Cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G) := ⋯
eq₁ : f₁ = (c'.pt.hom ≫ G.map (StructuredArrow.Hom.right (c'.π.app left))) ≫ eqToHom ⋯
eq₂ : f₂ = (c'.pt.hom ≫ G.map (StructuredArrow.Hom.right (c'.π.app right))) ≫ eqToHom ⋯
⊢ (ConcreteCategory.hom (ℱ.obj.map (G.map (StructuredArrow.Hom.right (c'.π.app left))).op))
      ((ConcreteCategory.hom (eqToHom ⋯)) (x g₁ hg₁)) =
    (ConcreteCategory.hom (ℱ.obj.map (G.map (StructuredArrow.Hom.right (c'.π.app right))).op))
      ((ConcreteCategory.hom (eqToHom ⋯)) (x g₂ hg₂))
Module: Mathlib.CategoryTheory.Sites.CoverPreserving

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
K : GrothendieckTopology D
F : C ⥤ D
inst✝¹ : F.Full
inst✝ : F.Faithful
hF : {c : C} → {d : D} → (d ⟶ F.obj c) → (c' : C) × (F.obj c' ≅ d)
ℱ : Sheaf K (Type u_1)
Z : C
T : Presieve Z
x : FamilyOfElements (F.op ⋙ ℱ.obj) T
hx : x.Compatible
Y₁ Y₂ : C
X : D
f₁ : X ⟶ F.obj Y₁
f₂ : X ⟶ F.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
he : f₁ ≫ F.map g₁ = f₂ ≫ F.map g₂
X' : C
e : F.obj X' ≅ X
⊢ (ConcreteCategory.hom (ℱ.obj.map (f₁.op ≫ e.hom.op))) (x g₁ hg₁) =
    (ConcreteCategory.hom (ℱ.obj.map (f₂.op ≫ e.hom.op))) (x g₂ hg₂)

Tactic:
simpa using!
    hx (F.preimage <| e.hom ≫ f₁) (F.preimage <| e.hom ≫ f₂) hg₁ hg₂
      (F.map_injective <| by simpa using! he)

Goal state after:
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

Goal state before:
pp: case h
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
D : Type u_2
inst✝³ : Category.{v_2, u_2} D
K : GrothendieckTopology D
A : Type u_4
inst✝² : Category.{v_4, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj
X : Cᵒᵖ
U : Aᵒᵖ
x✝ : (yoneda.obj ((G.op ⋙ ℱ).obj X)).obj U
⊢ (pushforwardFamily (homOver α (unop U)) x✝).IsAmalgamation
    (have this := (ConcreteCategory.hom ((yoneda.map (α.app X)).app U)) x✝;
    this)

Tactic:
intro Y f hf

Goal state after:
case h
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
D : Type u_2
inst✝³ : Category.{v_2, u_2} D
K : GrothendieckTopology D
A : Type u_4
inst✝² : Category.{v_4, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj
X : Cᵒᵖ
U : Aᵒᵖ
x✝ : (yoneda.obj ((G.op ⋙ ℱ).obj X)).obj U
Y : D
f : Y ⟶ G.obj (unop X)
hf : (Sieve.coverByImage G (G.obj (unop X))).arrows f
⊢ (ConcreteCategory.hom ((ℱ'.obj ⋙ coyoneda.obj (op (unop U))).map f.op))
      (have this := (ConcreteCategory.hom ((yoneda.map (α.app X)).app U)) x✝;
      this) =
    pushforwardFamily (homOver α (unop U)) x✝ f hf
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv

Goal state before:
pp: case left
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type w
inst✝² : Category.{w', w} A
inst✝¹ : ∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A
inst✝ : IsDenseSubsite J K G
Y : Sheaf J A
U : C
X : A
f₁ f₂ : (yoneda.obj (((G.op.ran ⋙ (whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj Y.obj).obj (op U))).obj (op X)
e :
  (ConcreteCategory.hom ((yoneda.map ((G.op.ranCounit.app Y.obj).app (op U))).app (op X))) f₁ =
    (ConcreteCategory.hom ((yoneda.map ((G.op.ranCounit.app Y.obj).app (op U))).app (op X))) f₂
W : C
g : G.obj W ⟶ G.obj U
⊢ f₁ ≫
      ((RightExtension.mk (G.op.ran.obj Y.obj) (G.op.ranCounit.app Y.obj)).coneAt (op (G.obj U))).π.app
        (StructuredArrow.mk (op g)) =
    f₂ ≫
      ((RightExtension.mk (G.op.ran.obj Y.obj) (G.op.ranCounit.app Y.obj)).coneAt (op (G.obj U))).π.app
        (StructuredArrow.mk (op g))

Tactic:
refine (Y.2 X _ (IsDenseSubsite.imageSieve_mem J K G g)).isSeparatedFor.ext
      (fun V iVW ⟨iVU, h⟩ ↦ ?_)

Goal state after:
case left
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
A : Type w
inst✝² : Category.{w', w} A
inst✝¹ : ∀ (X : Dᵒᵖ), Limits.HasLimitsOfShape (StructuredArrow X G.op) A
inst✝ : IsDenseSubsite J K G
Y : Sheaf J A
U : C
X : A
f₁ f₂ : (yoneda.obj (((G.op.ran ⋙ (whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj Y.obj).obj (op U))).obj (op X)
e :
  (ConcreteCategory.hom ((yoneda.map ((G.op.ranCounit.app Y.obj).app (op U))).app (op X))) f₁ =
    (ConcreteCategory.hom ((yoneda.map ((G.op.ranCounit.app Y.obj).app (op U))).app (op X))) f₂
W : C
g : G.obj W ⟶ G.obj U
V : C
iVW : V ⟶ W
x✝ : (G.imageSieve g).arrows iVW
iVU : V ⟶ U
h : G.map iVU = G.map iVW ≫ g
⊢ (ConcreteCategory.hom ((Y.obj ⋙ coyoneda.obj (op X)).map iVW.op))
      (f₁ ≫
        ((RightExtension.mk (G.op.ran.obj Y.obj) (G.op.ranCounit.app Y.obj)).coneAt (op (G.obj U))).π.app
          (StructuredArrow.mk (op g))) =
    (ConcreteCategory.hom ((Y.obj ⋙ coyoneda.obj (op X)).map iVW.op))
      (f₂ ≫
        ((RightExtension.mk (G.op.ran.obj Y.obj) (G.op.ranCounit.app Y.obj)).coneAt (op (G.obj U))).π.app
          (StructuredArrow.mk (op g)))
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

Goal state before:
pp: case h
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
D : Type u_2
inst✝³ : Category.{v_2, u_2} D
K : GrothendieckTopology D
A : Type u_4
inst✝² : Category.{v_4, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : ℱ ⟶ ℱ'.obj
X : Dᵒᵖ
U : Aᵒᵖ
x✝ : (yoneda.obj (ℱ.obj X)).obj U
⊢ (pushforwardFamily (homOver (G.op.whiskerLeft α) (unop U)) x✝).IsAmalgamation
    (have this := (ConcreteCategory.hom ((yoneda.map (α.app X)).app U)) x✝;
    this)

Tactic:
intro Y f hf

Goal state after:
case h
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
D : Type u_2
inst✝³ : Category.{v_2, u_2} D
K : GrothendieckTopology D
A : Type u_4
inst✝² : Category.{v_4, u_4} A
G : C ⥤ D
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
ℱ : Dᵒᵖ ⥤ A
ℱ' : Sheaf K A
α : ℱ ⟶ ℱ'.obj
X : Dᵒᵖ
U : Aᵒᵖ
x✝ : (yoneda.obj (ℱ.obj X)).obj U
Y : D
f : Y ⟶ unop X
hf : (Sieve.coverByImage G (unop X)).arrows f
⊢ (ConcreteCategory.hom ((ℱ'.obj ⋙ coyoneda.obj (op (unop U))).map f.op))
      (have this := (ConcreteCategory.hom ((yoneda.map (α.app X)).app U)) x✝;
      this) =
    pushforwardFamily (homOver (G.op.whiskerLeft α) (unop U)) x✝ f hf
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁵ : Category.{v_2, u_2} D
E : Type u_3
inst✝⁴ : Category.{v_3, u_3} E
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology E
G : C ⥤ D
A : Type u_4
inst✝³ : Category.{v_4, u_4} A
inst✝² : IsDenseSubsite J K G
F : Sheaf J A
inst✝¹ : (G.sheafPushforwardContinuous A J K).IsEquivalence
inst✝ : HasWeakSheafify J A
P₁ P₂ : Dᵒᵖ ⥤ A
Q : Sheaf K A
f : P₁ ⟶ P₂
g : P₂ ⟶ (sheafToPresheaf K A).obj Q
⊢ (sheafifyHomEquivOfIsEquivalence J K G) ((sheafifyHomEquivOfIsEquivalence J K G).symm (f ≫ g)) =
    (sheafifyHomEquivOfIsEquivalence J K G)
      ((sheafifyOfIsEquivalence J K G A).map f ≫ (sheafifyHomEquivOfIsEquivalence J K G).symm g)

Tactic:
simp [sheafifyHomEquivOfIsEquivalence_naturality_left _ _ _ f]

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

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
P✝ : Cᵒᵖ ⥤ Type w
X✝ : C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
X : C
S : Sieve X
hS : S ∈ {S | ∀ (Y : C) (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f S).arrows}
R : Sieve X
hR :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f → Sieve.pullback f R ∈ {S | ∀ (Y_1 : C) (f : Y_1 ⟶ Y), Presieve.IsSheafFor P (Sieve.pullback f S).arrows}
Z : C
g : Z ⟶ X
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ Z⦄,
    (Sieve.pullback g S).arrows f → Presieve.IsSheafFor P (Sieve.pullback f (Sieve.pullback g R)).arrows

Tactic:
intro Y f hf

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
P✝ : Cᵒᵖ ⥤ Type w
X✝ : C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
X : C
S : Sieve X
hS : S ∈ {S | ∀ (Y : C) (f : Y ⟶ X), Presieve.IsSheafFor P (Sieve.pullback f S).arrows}
R : Sieve X
hR :
  ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄,
    S.arrows f → Sieve.pullback f R ∈ {S | ∀ (Y_1 : C) (f : Y_1 ⟶ Y), Presieve.IsSheafFor P (Sieve.pullback f S).arrows}
Z : C
g : Z ⟶ X
Y : C
f : Y ⟶ Z
hf : (Sieve.pullback g S).arrows f
⊢ Presieve.IsSheafFor P (Sieve.pullback f (Sieve.pullback g R)).arrows
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✝¹ E✝ : PreOneHypercover S✝
F✝ : PreOneHypercover S✝
G : PreOneHypercover S✝
S : C
E F : PreOneHypercover S
s₀ : E.I₀ ≃ F.I₀
h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i)
s₁ : ⦃i j : E.I₀⦄ → E.I₁ i j ≃ F.I₁ (s₀ i) (s₀ j)
h₁ : ⦃i j : E.I₀⦄ → (k : E.I₁ i j) → E.Y k ≅ F.Y (s₁ k)
w₀ : ∀ (i : E.I₀), (h₀ i).hom ≫ F.f (s₀ i) = E.f i
w₁₁ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), (h₁ k).hom ≫ F.p₁ (s₁ k) = E.p₁ k ≫ (h₀ i).hom
w₁₂ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), (h₁ k).hom ≫ F.p₂ (s₁ k) = E.p₂ k ≫ (h₀ j).hom
⊢ ∀ (i : E.I₀),
    ((let __Hom := (PreZeroHypercover.isoMk s₀ h₀ w₀).hom;
            { toHom := __Hom, s₁ := fun {i j} k ↦ s₁ k, h₁ := fun {i j} k ↦ (h₁ k).hom, w₁₁ := ⋯, w₁₂ := ⋯ }) ≫
            let __Hom := (PreZeroHypercover.isoMk s₀ h₀ w₀).inv;
            { toHom := __Hom, s₁ := fun {i j} k ↦ s₁.symm ((congrIndexOneOfEq ⋯ ⋯) k),
              h₁ := fun {i j} k ↦
                (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫ eqToHom ⋯ ≫ (h₁ (s₁.symm ((congrIndexOneOfEq ⋯ ⋯) k))).inv,
              w₁₁ := ⋯, w₁₂ := ⋯ }).h₀
        i =
      (𝟙 E).h₀ i ≫ eqToHom ⋯

Tactic:
intro i; simp

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✝¹ E✝ : PreOneHypercover S✝
F✝ : PreOneHypercover S✝
G : PreOneHypercover S✝
S : C
E F : PreOneHypercover S
s₀ : E.I₀ ≃ F.I₀
h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i)
s₁ : ⦃i j : E.I₀⦄ → E.I₁ i j ≃ F.I₁ (s₀ i) (s₀ j)
h₁ : ⦃i j : E.I₀⦄ → (k : E.I₁ i j) → E.Y k ≅ F.Y (s₁ k)
w₀ : ∀ (i : E.I₀), (h₀ i).hom ≫ F.f (s₀ i) = E.f i
w₁₁ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), (h₁ k).hom ≫ F.p₁ (s₁ k) = E.p₁ k ≫ (h₀ i).hom
w₁₂ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), (h₁ k).hom ≫ F.p₂ (s₁ k) = E.p₂ k ≫ (h₀ j).hom
⊢ ∀ (i : F.I₀),
    ((let __Hom := (PreZeroHypercover.isoMk s₀ h₀ w₀).inv;
            { toHom := __Hom, s₁ := fun {i j} k ↦ s₁.symm ((congrIndexOneOfEq ⋯ ⋯) k),
              h₁ := fun {i j} k ↦
                (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫ eqToHom ⋯ ≫ (h₁ (s₁.symm ((congrIndexOneOfEq ⋯ ⋯) k))).inv,
              w₁₁ := ⋯, w₁₂ := ⋯ }) ≫
            let __Hom := (PreZeroHypercover.isoMk s₀ h₀ w₀).hom;
            { toHom := __Hom, s₁ := fun {i j} k ↦ s₁ k, h₁ := fun {i j} k ↦ (h₁ k).hom, w₁₁ := ⋯, w₁₂ := ⋯ }).h₀
        i =
      (𝟙 F).h₀ i ≫ eqToHom ⋯

Tactic:
intro i; simp

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
G : D ⥤ C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
inst✝³ : G.IsCoverDense J
inst✝² : G.Full
inst✝¹ : G.IsContinuous K J
inst✝ : (G.sheafPushforwardContinuous A K J).EssSurj
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
⊢ (ObjectProperty.isoClosure fun x ↦ x ∈ Set.range (sheafToPresheaf K A).obj).isLocal =
    (ObjectProperty.isoClosure fun x ↦
        x ∈ Set.range (sheafToPresheaf J A ⋙ (whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).obj).isLocal

Tactic:
apply congr_arg

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
inst✝³ : G.IsCoverDense J
inst✝² : G.Full
inst✝¹ : G.IsContinuous K J
inst✝ : (G.sheafPushforwardContinuous A K J).EssSurj
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
⊢ (ObjectProperty.isoClosure fun x ↦ x ∈ Set.range (sheafToPresheaf K A).obj) =
    ObjectProperty.isoClosure fun x ↦ x ∈ Set.range (sheafToPresheaf J A ⋙ (whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).obj
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators

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 P : SheafOfModules R
e : M ≅ N
σ : M.GeneratingSections
⊢ (fun σ ↦ σ.ofEpi e.inv) ((fun σ ↦ σ.ofEpi e.hom) σ) = σ

Tactic:
dsimp
    simp only [← opEpi_comp, e.hom_inv_id, opEpi_id]

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

Goal state before:
pp: case refine_1
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
⊢ Function.Injective (F.colimitTypePrecomp P)

Tactic:
have h (Y : D) : ∃ (a : P.obj Y → (F ⋙ P).ColimitType), ∀ (j : StructuredArrow Y F),
        (F ⋙ P).ιColimitType j.right ∘ P.map j.hom = a := by
      apply constant_of_preserves_morphisms'
      intro Z₁ Z₂ f
      ext x
      dsimp
      rw [← (F ⋙ P).ιColimitType_map f.right, comp_map]
      simp [← comp_apply, ← Functor.map_comp]
    choose φ hφ using h
    let c : P.CoconeTypes :=
      { pt := (F ⋙ P).ColimitType
        ι Y := φ Y
        ι_naturality {Y₁ Y₂} f := by
          ext
          have X : StructuredArrow Y₂ F := Classical.arbitrary _
          rw [← hφ Y₂ X, ← hφ Y₁ ((StructuredArrow.map f).obj X)]
          simp }
    refine Function.RightInverse.injective (g := (P.descColimitType c)) (fun x ↦ ?_)
    obtain ⟨X, x, rfl⟩ := (F ⋙ P).ιColimitType_jointly_surjective x
    simp [c, ← hφ (F.obj X) (StructuredArrow.mk (𝟙 _))]

Goal state after:
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
⊢ ∀ {Y : C} (f : Y ⟶ X) [Mono f], IsIso f ↔ f ≠ 0

Tactic:
intro Y f hf

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
Y : C
f : Y ⟶ X
hf : Mono f
⊢ IsIso f ↔ f ≠ 0
Module: Mathlib.CategoryTheory.Limits.Lattice

Goal state before:
pp: α : Type u
J✝ : Type w
inst✝³ : SmallCategory J✝
inst✝² : FinCategory J✝
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
J : Type
𝒥₁ : SmallCategory J
𝒥₂ : FinCategory J
⊢ HasLimitsOfShape J α

Tactic:
exact { has_limit := fun F => HasLimit.mk (finiteLimitCone F) }

Goal state after:
Module: Mathlib.Topology.Sheaves.Presheaf

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
H₁ : X ≅ Y
ℱ : Presheaf C Y
𝒢 : Presheaf C X
H₂ : ℱ ⟶ (pushforward C H₁.hom).obj 𝒢
U : (Opens ↑X)ᵒᵖ
⊢ (pushforwardToOfIso H₁ H₂).app U = H₂.app (op ((Opens.map H₁.inv).obj (unop U))) ≫ 𝒢.map (eqToHom ⋯)

Tactic:
by
  simp [pushforwardToOfIso, Equivalence.toAdjunction, Adjunction.homEquiv_counit]

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

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
inst✝¹⁰ : Ring R
inst✝⁹ : TopologicalSpace R
inst✝⁸ : TopologicalSpace M
inst✝⁷ : AddCommGroup M
inst✝⁶ : ContinuousAdd M
inst✝⁵ : Module R M
inst✝⁴ : ContinuousSMul R M
inst✝³ : IsDomain R
inst✝² : Nontrivial M
inst✝¹ : (𝓝[≠] 0).NeBot
inst✝ : IsTorsionFree R M
x y : M
hy : y ≠ 0
⊢ Tendsto (fun c ↦ x + c • y) (𝓝 0) (𝓝 x)

Tactic:
convert! tendsto_const_nhds.add ((@tendsto_id R _).zero_smul_const y)

Goal state after:
case e'_5
R : Type u_1
M : Type u_2
inst✝¹⁰ : Ring R
inst✝⁹ : TopologicalSpace R
inst✝⁸ : TopologicalSpace M
inst✝⁷ : AddCommGroup M
inst✝⁶ : ContinuousAdd M
inst✝⁵ : Module R M
inst✝⁴ : ContinuousSMul R M
inst✝³ : IsDomain R
inst✝² : Nontrivial M
inst✝¹ : (𝓝[≠] 0).NeBot
inst✝ : IsTorsionFree R M
x y : M
hy : y ≠ 0
⊢ x = x + 0
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
    rw [this]
    fun_prop

Goal state after:
Module: Mathlib.Data.FunLike.Ring

Goal state before:
pp: F : Type u_1
α : Type u_2
inst✝⁸ : FunLike F α α
inst✝⁷ : Zero F
inst✝⁶ : One F
inst✝⁵ : Mul F
inst✝⁴ : Zero α
inst✝³ : IsZeroApply F α α
inst✝² : IsOneApplyEqSelf F α
inst✝¹ : IsMulApplyEqComp F α
inst✝ : ZeroHomClass F α α
x✝² x✝¹ x✝ : F
⊢ x✝² * x✝¹ * x✝ = x✝² * (x✝¹ * x✝)

Tactic:
by apply DFunLike.ext; simp

Goal state after:
Module: Mathlib.Data.FunLike.Ring

Goal state before:
pp: F : Type u_1
α : Type u_2
inst✝⁸ : FunLike F α α
inst✝⁷ : Zero F
inst✝⁶ : One F
inst✝⁵ : Mul F
inst✝⁴ : Zero α
inst✝³ : IsZeroApply F α α
inst✝² : IsOneApplyEqSelf F α
inst✝¹ : IsMulApplyEqComp F α
inst✝ : ZeroHomClass F α α
x✝ : F
⊢ 1 * x✝ = x✝

Tactic:
by apply DFunLike.ext; simp

Goal state after:
Module: Mathlib.Data.FunLike.Ring

Goal state before:
pp: F : Type u_1
α : Type u_2
inst✝⁸ : FunLike F α α
inst✝⁷ : Zero F
inst✝⁶ : One F
inst✝⁵ : Mul F
inst✝⁴ : Zero α
inst✝³ : IsZeroApply F α α
inst✝² : IsOneApplyEqSelf F α
inst✝¹ : IsMulApplyEqComp F α
inst✝ : ZeroHomClass F α α
x✝ : F
⊢ x✝ * 1 = x✝

Tactic:
by apply DFunLike.ext; simp

Goal state after: