mathlib-initiative/mathlib-tactics huggingface dataset:
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
h : (∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R) ∧ ∀ {X : C}, ∀ R ∈ L.coverings X, IsSheafFor P R
X : C
R : Presieve X
hR : R ∈ (K ⊔ L).coverings X
⊢ IsSheafFor P R

Tactic:
rcases hR with hR | hR

Goal state after:
case inl
C : Type u_2
inst✝ : Category.{v_1, u_2} C
K L : Coverage C
P : Cᵒᵖ ⥤ Type u_1
h : (∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R) ∧ ∀ {X : C}, ∀ R ∈ L.coverings X, IsSheafFor P R
X : C
R : Presieve X
hR : R ∈ K.coverings X
⊢ IsSheafFor P R

case inr
C : Type u_2
inst✝ : Category.{v_1, u_2} C
K L : Coverage C
P : Cᵒᵖ ⥤ Type u_1
h : (∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R) ∧ ∀ {X : C}, ∀ R ∈ L.coverings X, IsSheafFor P R
X : C
R : Presieve X
hR : R ∈ L.coverings X
⊢ IsSheafFor P R
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: case h
C : Type u_2
inst✝³ : Category.{v_1, u_2} C
J : Precoverage C
inst✝² : J.IsStableUnderBaseChange
inst✝¹ : J.HasPullbacks
inst✝ : J.Small
P : Cᵒᵖ ⥤ Type u_1
h : ∀ ⦃X : C⦄ (E : J.ZeroHypercover X), Presieve.IsSheafFor P E.presieve₀
X : C
E₀ : PreZeroHypercover X
hR : E₀.presieve₀ ∈ J.coverings X
E : J.ZeroHypercover X := ⋯
⊢ (Sieve.generate E.restrictIndexOfSmall.presieve₀).arrows ≤ (Sieve.generate E₀.presieve₀).arrows

pp: case trans
C : Type u_2
inst✝³ : Category.{v_1, u_2} C
J : Precoverage C
inst✝² : J.IsStableUnderBaseChange
inst✝¹ : J.HasPullbacks
inst✝ : J.Small
P : Cᵒᵖ ⥤ Type u_1
h : ∀ ⦃X : C⦄ (E : J.ZeroHypercover X), Presieve.IsSheafFor P E.presieve₀
X : C
E₀ : PreZeroHypercover X
hR : E₀.presieve₀ ∈ J.coverings X
E : J.ZeroHypercover X := ⋯
⊢ ∀ ⦃Y : C⦄ (f : Y ⟶ X),
    Presieve.IsSheafFor P (Sieve.pullback f (Sieve.generate E.restrictIndexOfSmall.presieve₀)).arrows

Tactic:
· exact Sieve.generate_mono (by simp [E])

Goal state after:
case trans
C : Type u_2
inst✝³ : Category.{v_1, u_2} C
J : Precoverage C
inst✝² : J.IsStableUnderBaseChange
inst✝¹ : J.HasPullbacks
inst✝ : J.Small
P : Cᵒᵖ ⥤ Type u_1
h : ∀ ⦃X : C⦄ (E : J.ZeroHypercover X), Presieve.IsSheafFor P E.presieve₀
X : C
E₀ : PreZeroHypercover X
hR : E₀.presieve₀ ∈ J.coverings X
E : J.ZeroHypercover X := ⋯
⊢ ∀ ⦃Y : C⦄ (f : Y ⟶ X),
    Presieve.IsSheafFor P (Sieve.pullback f (Sieve.generate E.restrictIndexOfSmall.presieve₀)).arrows
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
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
H : (Cᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)) ⥤ Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
adj : H ⊣ (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))).obj F.op
inst✝ : F.IsContinuous J K
G G' : Cᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
f : G ⟶ G'
hf : J.W f
U : Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
hU : Presheaf.IsSheaf K U
⊢ Presheaf.IsSheaf J (((whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))).obj F.op).obj U)

Tactic:
rw [isSheaf_iff_isSheaf_of_type]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
H : (Cᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)) ⥤ Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
adj : H ⊣ (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))).obj F.op
inst✝ : F.IsContinuous J K
G G' : Cᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
f : G ⟶ G'
hf : J.W f
U : Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
hU : Presheaf.IsSheaf K U
⊢ Presieve.IsSheaf J (((whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))).obj F.op).obj U)
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 : GrothendieckTopology C
K : GrothendieckTopology D
inst✝ : F.IsContinuous J K
G : Sheaf K (Type t)
⊢ Presieve.IsSheaf K G.obj

Tactic:
← isSheaf_iff_isSheaf_of_type

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝ : F.IsContinuous J K
G : Sheaf K (Type t)
⊢ Presheaf.IsSheaf K G.obj
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 : GrothendieckTopology C
K : GrothendieckTopology D
inst✝ : F.IsContinuous J K
G : Dᵒᵖ ⥤ Type u_1
h : Presieve.IsSheaf K G
⊢ Presieve.IsSheaf J (F.op ⋙ G)

Tactic:
← isSheaf_iff_isSheaf_of_type

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝ : F.IsContinuous J K
G : Dᵒᵖ ⥤ Type u_1
h : Presheaf.IsSheaf K G
⊢ Presheaf.IsSheaf J (F.op ⋙ G)
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 : GrothendieckTopology C
K : GrothendieckTopology D
inst✝¹ : F.PreservesOneHypercovers J K
inst✝ : J.IsGeneratedByOneHypercovers
P : Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
hP : Presheaf.IsSheaf K P
⊢ Presieve.IsSheaf J (F.op ⋙ { obj := P, property := hP }.obj)

Tactic:
← isSheaf_iff_isSheaf_of_type

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝¹ : F.PreservesOneHypercovers J K
inst✝ : J.IsGeneratedByOneHypercovers
P : Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
hP : Presheaf.IsSheaf K P
⊢ Presheaf.IsSheaf J (F.op ⋙ { obj := P, property := hP }.obj)
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
V : C
iVW : V ⟶ W
x✝ : (G.imageSieve g).arrows iVW
iVU : V ⟶ U
h : G.map iVU = G.map iVW ≫ g
this :
  (ConcreteCategory.hom ((yoneda.map ((G.op.ranCounit.app Y.obj).app (op U))).app (op X))) f₁ ≫ Y.obj.map iVU.op =
    (ConcreteCategory.hom ((yoneda.map ((G.op.ranCounit.app Y.obj).app (op U))).app (op X))) f₂ ≫ Y.obj.map iVU.op
⊢ (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)))

Tactic:
dsimp at this ⊢

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
this :
  (f₁ ≫ (G.op.ranCounit.app Y.obj).app (op U)) ≫ Y.obj.map iVU.op =
    (f₂ ≫ (G.op.ranCounit.app Y.obj).app (op U)) ≫ Y.obj.map iVU.op
⊢ (f₁ ≫ (G.op.ran.obj Y.obj).map (op g) ≫ (G.op.ranCounit.app Y.obj).app (op W)) ≫ Y.obj.map iVW.op =
    (f₂ ≫ (G.op.ran.obj Y.obj).map (op g) ≫ (G.op.ranCounit.app Y.obj).app (op W)) ≫ Y.obj.map iVW.op
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
E : PreOneHypercover S
F : PreOneHypercover S
f g : E.Hom F
hs₀ : f.s₀ = g.s₀
i : E.I₀
⊢ F.X (g.s₀ i) = F.X (f.s₀ i)

Tactic:
simp [hs₀]

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
E : PreOneHypercover S
F : PreOneHypercover S
f g : E.Hom F
hs₀ : f.s₀ = g.s₀
hh₀ : ∀ (i : E.I₀), f.h₀ i = g.h₀ i ≫ eqToHom ⋯
i j : E.I₀
k : E.I₁ i j
⊢ g.s₀ i = f.s₀ i

Tactic:
simp [hs₀]

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
E : PreOneHypercover S
F : PreOneHypercover S
f g : E.Hom F
hs₀ : f.s₀ = g.s₀
hh₀ : ∀ (i : E.I₀), f.h₀ i = g.h₀ i ≫ eqToHom ⋯
i j : E.I₀
k : E.I₁ i j
⊢ g.s₀ j = f.s₀ j

Tactic:
simp [hs₀]

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) (uliftYoneda.{w, v, u}.obj (P ⋙ uliftFunctor.{v, w}).reprX)

Tactic:
← isSheaf_iff_isSheaf_of_type

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
inst✝ : P.IsRepresentable
⊢ Presheaf.IsSheaf (canonicalTopology C) (yoneda.obj (P ⋙ uliftFunctor.{v, w}).reprX)

Tactic:
rw [isSheaf_iff_isSheaf_of_type]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
X✝ : C
J✝ J : GrothendieckTopology C
inst✝ : J.Subcanonical
X : C
⊢ Presheaf.IsSheaf J (CategoryTheory.yoneda.obj X)

Tactic:
rw [isSheaf_iff_isSheaf_of_type]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
X✝ : C
J✝ J : GrothendieckTopology C
inst✝ : J.Subcanonical
X : C
⊢ Presieve.IsSheaf J (CategoryTheory.yoneda.obj X)
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
E : PreOneHypercover S
F : PreOneHypercover S
f g : E.Hom F
hs₀ : f.s₀ = g.s₀
x✝ : ∀ (i : E.I₀), f.h₀ i = g.h₀ i ≫ eqToHom ⋯
i j : E.I₀
k : E.I₁ i j
⊢ g.s₀ i = f.s₀ i

Tactic:
simp [hs₀]

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
E : PreOneHypercover S
F : PreOneHypercover S
f g : E.Hom F
hs₀ : f.s₀ = g.s₀
x✝ : ∀ (i : E.I₀), f.h₀ i = g.h₀ i ≫ eqToHom ⋯
i j : E.I₀
k : E.I₁ i j
⊢ g.s₀ j = f.s₀ j

Tactic:
simp [hs₀]

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 j : F.I₀
k : F.I₁ i j
⊢ ((congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫ eqToHom ⋯ ≫ (h₁ (s₁.symm ((congrIndexOneOfEq ⋯ ⋯) k))).inv) ≫
      E.p₁ (s₁.symm ((congrIndexOneOfEq ⋯ ⋯) k)) =
    F.p₁ k ≫ (PreZeroHypercover.isoMk s₀ h₀ w₀).inv.h₀ i

Tactic:
obtain ⟨i, rfl⟩ := s₀.surjective i
    obtain ⟨j, rfl⟩ := s₀.surjective j
    obtain ⟨k, rfl⟩ := s₁.surjective k
    rw [← cancel_epi (h₁ k).hom, reassoc_of% w₁₁ k]
    simp only [PreZeroHypercover.isoMk_inv_s₀, Category.assoc, PreZeroHypercover.isoMk_inv_h₀,
      Equiv.symm_apply_apply, eqToHom_iso_hom_naturality_assoc, Iso.hom_inv_id,
      Category.comp_id]
    rw [PreOneHypercover.isoMk_aux_assoc, ← eqToHom_naturality, eqToHom_refl, Category.comp_id,
      congrIndexOneOfEqIso_inv_p₁]
    apply PreOneHypercover.congrIndexOneOfEq_equiv

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 j : F.I₀
k : F.I₁ i j
⊢ ((congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫ eqToHom ⋯ ≫ (h₁ (s₁.symm ((congrIndexOneOfEq ⋯ ⋯) k))).inv) ≫
      (h₁ (s₁.symm ((congrIndexOneOfEq ⋯ ⋯) k))).hom =
    𝟙 (F.Y k) ≫ (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫ eqToHom ⋯

Tactic:
simp only [Category.assoc, Iso.inv_hom_id, Category.comp_id]

Goal state after:
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 j : F.I₀
k : F.I₁ i j
⊢ (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫ eqToHom ⋯ = 𝟙 (F.Y k) ≫ (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: case refine_1.refine_4
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S : C
E✝¹ E✝ : PreOneHypercover S
F✝ : PreOneHypercover S
G✝ : PreOneHypercover S
E F : PreOneHypercover S
f : E ≅ F
G : Cᵒᵖ ⥤ A
⊢ ∀ (i : E.multicospanShape.R),
    (E.multicospanIndex G).multicospan.map (WalkingMulticospan.Hom.snd i) ≫
        (G.mapIso (asIso (f.hom.h₁ i.snd)).symm.op).hom =
      (G.mapIso (asIso (f.hom.h₀ (E.multicospanShape.snd i))).symm.op).hom ≫
        ((equivalenceMulticospanOfIso f).functor ⋙ (F.multicospanIndex G).multicospan).map
          (WalkingMulticospan.Hom.snd i)

Tactic:
simp [← Functor.map_comp_assoc, ← Functor.map_comp, ← op_comp, f.hom.w₁₂]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
Y : Over X
S : Sieve Y
⊢ functorPullback (Over.forget X) (functorPushforward (Over.forget X) S) = S

Tactic:
by
  apply arrows_ext
  simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
K : GrothendieckTopology D
F : C ⥤ D
X : C
h : CoverPreserving J K F
U : Over X
S : Sieve U
hS : (Sieve.overEquiv U) S ∈ J U.left
⊢ (Sieve.overEquiv ((Over.post F).obj U)) (Sieve.functorPushforward (Over.post F) S) ∈ K ((Over.post F).obj U).left

Tactic:
Sieve.overEquiv_functorPushforward_post

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
K : GrothendieckTopology D
F : C ⥤ D
X : C
h : CoverPreserving J K F
U : Over X
S : Sieve U
hS : (Sieve.overEquiv U) S ∈ J U.left
⊢ Sieve.functorPushforward F ((Sieve.overEquiv U) S) ∈ K ((Over.post F).obj U).left
Module: Mathlib.CategoryTheory.Limits.Final.Type

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
P : D ⥤ Type w
inst✝ : F.Final
Y : D
Z₁ Z₂ : StructuredArrow Y F
f : Z₁ ⟶ Z₂
x : (fun X ↦ X) (P.obj Y)
⊢ (F ⋙ P).ιColimitType Z₂.right
      ((ConcreteCategory.hom (P.map (F.map (StructuredArrow.Hom.right f)))) ((ConcreteCategory.hom (P.map Z₁.hom)) x)) =
    (F ⋙ P).ιColimitType Z₂.right ((ConcreteCategory.hom (P.map Z₂.hom)) x)

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

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

Goal state before:
pp: case mp
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
V : Opens ↑Y
t : Set ↑Y
ht : IsOpen t
hU : IsOpen (⇑(ConcreteCategory.hom f) ⁻¹' t)
⊢ V ≤ hf.functorObj { carrier := ⇑(ConcreteCategory.hom f) ⁻¹' t, is_open' := hU } →
    (Opens.map f).obj V ≤ { carrier := ⇑(ConcreteCategory.hom f) ⁻¹' t, is_open' := hU }

Tactic:
exact fun i x hx ↦ (hf.mem_functorObj_iff ((Opens.map f).obj ⟨t, ht⟩)).mp (i hx)

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

Goal state before:
pp: case a
T : Type u
inst✝ : TopologicalSpace T
X : Opens T
R : Presieve X
hR : R ∈ (pretopology T).coverings X
x : T
hx : x ∈ X
U : Opens T
f : U ⟶ X
hf : R f
hU : x ∈ U
⊢ ∃ U f, (Sieve.generate R).arrows f ∧ x ∈ U

Tactic:
exact ⟨U, f, Sieve.le_generate R U _ hf, hU⟩

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

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y Z : TopCat
FC : C → C → Type u_1
CC : C → Type u_2
inst✝ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
F : Presheaf C X
x y : ↑X
h : x ⤳ y
⊢ ∀ ⦃X_1 Y : (OpenNhds y)ᵒᵖ⦄ (f : X_1 ⟶ Y),
    (((whiskeringLeft (OpenNhds y)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion y).op).obj F).map f ≫
        colimit.ι ((OpenNhds.inclusion x).op ⋙ F) (op ⟨↑(unop Y), ⋯⟩) =
      colimit.ι ((OpenNhds.inclusion x).op ⋙ F) (op ⟨↑(unop X_1), ⋯⟩) ≫
        ((Functor.const (OpenNhds y)ᵒᵖ).obj ((stalkFunctor C x).1 F)).map f

Tactic:
intro U V i
    dsimp
    rw [Category.comp_id]
    let U' : OpenNhds x := ⟨_, (specializes_iff_forall_open.mp h _ (unop U).1.2 (unop U).2 :)⟩
    let V' : OpenNhds x := ⟨_, (specializes_iff_forall_open.mp h _ (unop V).1.2 (unop V).2 :)⟩
    exact colimit.w ((OpenNhds.inclusion x).op ⋙ F) (show V' ⟶ U' from i.unop).op

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)
B : Set (Opens ↑X)
hB : Opens.IsBasis B
F : Presheaf C X
x : ↑X
t : ToType (F.stalk x)
⊢ ∃ U, ∃ (m : x ∈ U) (_ : U ∈ B), ∃ s, (ConcreteCategory.hom (F.germ U x m)) s = t

Tactic:
obtain ⟨U, hxU, s, rfl⟩ := F.exists_germ_eq t

Goal state after:
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)
B : Set (Opens ↑X)
hB : Opens.IsBasis B
F : Presheaf C X
x : ↑X
U : Opens ↑X
hxU : x ∈ U
s : ToType (F.obj (op U))
⊢ ∃ U_1,
    ∃ (m : x ∈ U_1) (_ : U_1 ∈ B),
      ∃ s_1, (ConcreteCategory.hom (F.germ U_1 x m)) s_1 = (ConcreteCategory.hom (F.germ U x hxU)) s
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 G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ x ∈ U, Function.Injective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map f.hom))
hsurj :
  ∀ (t : CC (G.obj.obj (op U))) (x : ↥U),
    ∃ V,
      ∃ (_ : ↑x ∈ V), ∃ iVU s, (ConcreteCategory.hom (f.hom.app (op V))) s = (ConcreteCategory.hom (G.obj.map iVU.op)) t
t : CC (G.obj.obj (op U))
V : ↥U → Opens ↑X
mV : ∀ (x : ↥U), ↑x ∈ V x
iVU : (x : ↥U) → V x ⟶ U
sf : (x : ↥U) → ToType (F.obj.obj (op (V x)))
heq : ∀ (x : ↥U), (ConcreteCategory.hom (f.hom.app (op (V x)))) (sf x) = (ConcreteCategory.hom (G.obj.map (iVU x).op)) t
V_cover : U ≤ iSup V
this : IsCompatible F.obj V sf
s : ToType (F.obj.obj (op U))
s_spec : ∀ (i : ↥U), (ConcreteCategory.hom (F.obj.map (iVU i).op)) s = sf i
⊢ ∃ a, (ConcreteCategory.hom (f.hom.app (op U))) a = t

Tactic:
use s
      apply G.eq_of_locally_eq' V U iVU V_cover
      intro x
      rw [← ConcreteCategory.comp_apply, ← f.1.naturality, ConcreteCategory.comp_apply, s_spec, heq]

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Colimits

Goal state before:
pp: case h.of
J : Type v
inst✝ : Category.{u, v} J
F : J ⥤ MonCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
j : J
x✝ : ↑(F.obj j)
⊢ (Hom.hom m) (Quot.mk (⇑(colimitSetoid F)) (Prequotient.of j x✝)) =
    (Hom.hom (descMorphism F s)) (Quot.mk (⇑(colimitSetoid F)) (Prequotient.of j x✝))

Tactic:
change _ = s.ι.app j _
      rw [← w j]
      rfl

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₂
⊢ Function.Injective toLinearEquiv

Tactic:
rintro ⟨e, _, _⟩ ⟨e', _, _⟩ rfl

Goal state after:
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₁ ≃ₛₗ[σ₁₂] M₂
continuous_toFun✝¹ : Continuous[inst✝⁵, inst✝³] (↑e).toFun
continuous_invFun✝¹ : Continuous[inst✝³, inst✝⁵] e.invFun
continuous_toFun✝ :
  Continuous[inst✝⁵, inst✝³]
    (↑↑{ toLinearEquiv := e, continuous_toFun := continuous_toFun✝¹, continuous_invFun := continuous_invFun✝¹ }).toFun
continuous_invFun✝ :
  Continuous[inst✝³, inst✝⁵]
    (↑{ toLinearEquiv := e, continuous_toFun := continuous_toFun✝¹, continuous_invFun := continuous_invFun✝¹ }).invFun
⊢ { toLinearEquiv := e, continuous_toFun := continuous_toFun✝¹, continuous_invFun := continuous_invFun✝¹ } =
    {
      toLinearEquiv :=
        ↑{ toLinearEquiv := e, continuous_toFun := continuous_toFun✝¹, continuous_invFun := continuous_invFun✝¹ },
      continuous_toFun := continuous_toFun✝, continuous_invFun := continuous_invFun✝ }
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₂
x : M₁
⊢ (⇑e.symm ∘ ⇑e) x = id x

Tactic:
exact symm_apply_apply e x

Goal state after: