mathlib-initiative/mathlib-tactics huggingface dataset:
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
inst✝ : F.IsContinuous J K
G : Dᵒᵖ ⥤ Type (max w u₁ v₁ u₂ v₂)
hG : Presieve.IsSheaf K G
H : (Cᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)) ⥤ Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂) := F.op.lan
adj : H ⊣ (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))).obj F.op := F.op.lanAdjunction (Type (max u₁ v₁ u₂ v₂))
H' : (Cᵒᵖ ⥤ Type (max w u₁ v₁ u₂ v₂)) ⥤ Dᵒᵖ ⥤ Type (max w u₁ v₁ u₂ v₂) := F.op.lan
adj' : H' ⊣ (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max w u₁ v₁ u₂ v₂))).obj F.op :=
  F.op.lanAdjunction (Type (max w u₁ v₁ u₂ v₂))
⊢ Presieve.IsSheaf J (F.op ⋙ G)

Tactic:
refine Presieve.IsSheaf.comp_of_W_map_of_adjunction _ adj' ?_ _ hG

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
inst✝ : F.IsContinuous J K
G : Dᵒᵖ ⥤ Type (max w u₁ v₁ u₂ v₂)
hG : Presieve.IsSheaf K G
H : (Cᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)) ⥤ Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂) := F.op.lan
adj : H ⊣ (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))).obj F.op := F.op.lanAdjunction (Type (max u₁ v₁ u₂ v₂))
H' : (Cᵒᵖ ⥤ Type (max w u₁ v₁ u₂ v₂)) ⥤ Dᵒᵖ ⥤ Type (max w u₁ v₁ u₂ v₂) := F.op.lan
adj' : H' ⊣ (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max w u₁ v₁ u₂ v₂))).obj F.op :=
  F.op.lanAdjunction (Type (max w u₁ v₁ u₂ v₂))
⊢ ∀ ⦃X : C⦄ ⦃S : Sieve X⦄,
    S ∈ J X → K.W (H'.map (Sieve.shrinkFunctor.{max (max (max (max u₁ u₂) v₁) v₂) w, v₁, u₁} S).ι)
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},
    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₂),
        f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂ →
          (ConcreteCategory.hom (ℱ.obj.map f₁.op)) (x g₁ hg₁) = (ConcreteCategory.hom (ℱ.obj.map f₂.op)) (x g₂ hg₂)

Tactic:
intro ℱ

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},
    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₂),
        f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂ →
          (ConcreteCategory.hom (ℱ.obj.map f₁.op)) (x g₁ hg₁) = (ConcreteCategory.hom (ℱ.obj.map f₂.op)) (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
F : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝ : RepresentablyFlat F
⊢ F.IsContinuous J K ↔ CoverPreserving J K F

Tactic:
refine ⟨fun h ↦ .of_isContinuous _ _ _, fun h ↦ ?_⟩
  apply Functor.isContinuous_of_coverPreserving (compatiblePreservingOfFlat _ _) h

Goal state after:
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
K : GrothendieckTopology D
G : C ⥤ D
inst✝² : G.IsCoverDense K
inst✝¹ : G.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
⊢ ∀ (ℱ : Sheaf K (Type u_5)) {Z : C} {T : Presieve Z} {x : FamilyOfElements (G.op ⋙ ℱ.obj) T},
    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₂),
        f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂ →
          (ConcreteCategory.hom (ℱ.obj.map f₁.op)) (x g₁ hg₁) = (ConcreteCategory.hom (ℱ.obj.map f₂.op)) (x g₂ hg₂)

Tactic:
intro ℱ

Goal state after:
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
G : C ⥤ D
inst✝² : G.IsCoverDense K
inst✝¹ : G.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
ℱ : Sheaf K (Type u_5)
⊢ ∀ {Z : C} {T : Presieve Z} {x : FamilyOfElements (G.op ⋙ ℱ.obj) T},
    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₂),
        f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂ →
          (ConcreteCategory.hom (ℱ.obj.map f₁.op)) (x g₁ hg₁) = (ConcreteCategory.hom (ℱ.obj.map f₂.op)) (x g₂ hg₂)
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv

Goal state before:
pp: case refine_2
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 : (yoneda.obj (((𝟭 (Cᵒᵖ ⥤ A)).obj Y.obj).obj (op U))).obj (op X)
l : (X Y Z : C) → (f : X ⟶ Y) → (g : G.obj Y ⟶ G.obj Z) → (G.imageSieve g).arrows f → (X ⟶ Z)
hl :
  ∀ (X Y Z : C) (f : X ⟶ Y) (g : G.obj Y ⟶ G.obj Z) (hf : (G.imageSieve g).arrows f),
    G.map (l X Y Z f g hf) = G.map f ≫ g
W₁ : C
g₁ : unop (G.op.obj (op W₁)) ⟶ unop (op (G.obj U))
W₂ : C
g₂ : unop (G.op.obj (op W₂)) ⟶ unop (op (G.obj U))
i : unop (StructuredArrow.mk (op g₂)).right ⟶ unop (StructuredArrow.mk (op g₁)).right
hi✝ : (StructuredArrow.mk (op g₁)).hom ≫ G.op.map (op i) = (StructuredArrow.mk (op g₂)).hom
hi : (G.op.map (op i)).unop ≫ (StructuredArrow.mk (op g₁)).hom.unop = g₂
⊢ ((const (StructuredArrow (op (G.obj U)) G.op)).obj X).map (StructuredArrow.homMk (op i) hi✝) ≫
      ⋯.amalgamate ⟨G.imageSieve (StructuredArrow.mk (op g₂)).hom.unop, ⋯⟩
        (fun I ↦
          f ≫ Y.obj.map (l I.Y (unop (StructuredArrow.mk (op g₂)).2) U I.f (StructuredArrow.mk (op g₂)).hom.unop ⋯).op)
        ⋯ =
    ⋯.amalgamate ⟨G.imageSieve (StructuredArrow.mk (op g₁)).hom.unop, ⋯⟩
        (fun I ↦
          f ≫ Y.obj.map (l I.Y (unop (StructuredArrow.mk (op g₁)).2) U I.f (StructuredArrow.mk (op g₁)).hom.unop ⋯).op)
        ⋯ ≫
      (StructuredArrow.proj (op (G.obj U)) G.op ⋙ Y.obj).map (StructuredArrow.homMk (op i) hi✝)

Tactic:
dsimp at g₁ g₂ i hi ⊢

Goal state after:
case refine_2
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 : (yoneda.obj (((𝟭 (Cᵒᵖ ⥤ A)).obj Y.obj).obj (op U))).obj (op X)
l : (X Y Z : C) → (f : X ⟶ Y) → (g : G.obj Y ⟶ G.obj Z) → (G.imageSieve g).arrows f → (X ⟶ Z)
hl :
  ∀ (X Y Z : C) (f : X ⟶ Y) (g : G.obj Y ⟶ G.obj Z) (hf : (G.imageSieve g).arrows f),
    G.map (l X Y Z f g hf) = G.map f ≫ g
W₁ : C
g₁ : G.obj W₁ ⟶ G.obj U
W₂ : C
g₂ : G.obj W₂ ⟶ G.obj U
i : W₂ ⟶ W₁
hi✝ : (StructuredArrow.mk (op g₁)).hom ≫ G.op.map (op i) = (StructuredArrow.mk (op g₂)).hom
hi : G.map i ≫ g₁ = g₂
⊢ 𝟙 X ≫ ⋯.amalgamate ⟨G.imageSieve g₂, ⋯⟩ (fun I ↦ f ≫ Y.obj.map (l I.Y W₂ U I.f g₂ ⋯).op) ⋯ =
    ⋯.amalgamate ⟨G.imageSieve g₁, ⋯⟩ (fun I ↦ f ≫ Y.obj.map (l I.Y W₁ U I.f g₁ ⋯).op) ⋯ ≫ Y.obj.map (op i)
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
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
inst✝ : G.IsContinuous J K
⊢ ∀ {X Y : Sheaf K A}, Function.Injective (G.sheafPushforwardContinuous A J K).map

Tactic:
intro ℱ

Goal state after:
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
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
inst✝ : G.IsContinuous J K
ℱ : Sheaf K A
⊢ ∀ {Y : Sheaf K A}, Function.Injective (G.sheafPushforwardContinuous A J K).map
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 : E.I₀
k : E.I₁ i j
⊢ (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫ E.p₁ ((congrIndexOneOfEq ⋯ ⋯) k) ≫ eqToHom ⋯ = E.p₁ k ≫ eqToHom ⋯

pp: case w
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 : E.I₀
k : E.I₁ i j
⊢ (congrIndexOneOfEq ⋯ ⋯) k = s₁.symm ((congrIndexOneOfEq ⋯ ⋯) (s₁ k))

Tactic:
eqToHom_refl,

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

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

pp: case w
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 : E.I₀
k : E.I₁ i j
⊢ (congrIndexOneOfEq ⋯ ⋯) k = s₁.symm ((congrIndexOneOfEq ⋯ ⋯) (s₁ k))

Tactic:
eqToHom_refl,

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 : E.I₀
k : E.I₁ i j
⊢ (congrIndexOneOfEqIso ⋯ ⋯ k).inv ≫ E.p₂ ((congrIndexOneOfEq ⋯ ⋯) k) ≫ 𝟙 (E.X (s₀.symm (s₀ j))) = E.p₂ k ≫ eqToHom ⋯

case w
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 : E.I₀
k : E.I₁ i j
⊢ (congrIndexOneOfEq ⋯ ⋯) k = s₁.symm ((congrIndexOneOfEq ⋯ ⋯) (s₁ k))
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: case h
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
e : E ≅ F
i : E.I₀
⊢ eqToHom ⋯ = 𝟙 (E.X i) ∧ (e.inv.h₀ (e.hom.s₀ i) ≫ eqToHom ⋯) ≫ e.hom.h₀ i = 𝟙 (F.X (e.hom.s₀ i))

Tactic:
eqToHom_refl,

Goal state after:
case h
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
e : E ≅ F
i : E.I₀
⊢ 𝟙 (E.X i) = 𝟙 (E.X i) ∧ (e.inv.h₀ (e.hom.s₀ i) ≫ eqToHom ⋯) ≫ e.hom.h₀ i = 𝟙 (F.X (e.hom.s₀ i))
Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Connected

Goal state before:
pp: J : Type u'
inst✝³ : Category.{v', u'} J
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
K✝ : C ⥤ D
X : C
inst✝ : IsConnected J
B : D
F : J ⥤ CostructuredArrow K✝ B
c : Cone (F ⋙ proj K✝ B)
t : IsLimit c
s : Cone F
m : s.pt ⟶ (raiseCone c).pt
K : ∀ (j : J), m ≫ (raiseCone c).π.app j = s.π.app j
⊢ m = homMk (t.lift ((proj K✝ B).mapCone s)) ⋯

Tactic:
by
    ext1
    apply t.hom_ext
    intro j
    simp [← K j]

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
⊢ K.W (G.op.whiskerLeft f) ↔ J.W f

Tactic:
rw [← W_inverseImage_whiskeringLeft J K G]

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
⊢ K.W (G.op.whiskerLeft f) ↔ K.W.inverseImage ((whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op) f
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous

Goal state before:
pp: C✝¹ : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C✝¹
D✝ : Type u₂
inst✝¹⁰ : Category.{v₂, u₂} D✝
D' : Type u₃
inst✝⁹ : Category.{v₃, u₃} D'
D'' : Type u₄
inst✝⁸ : Category.{v₄, u₄} D''
J✝¹ : GrothendieckTopology C✝¹
K✝ : GrothendieckTopology D✝
F✝ : C✝¹ ⥤ D✝
S✝ : Sheaf J✝¹ RingCat
R✝¹ : Sheaf K✝ RingCat
inst✝⁷ : F✝.IsContinuous J✝¹ K✝
φ✝ : S✝ ⟶ (F✝.sheafPushforwardContinuous RingCat J✝¹ K✝).obj R✝¹
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
G : D ⥤ C✝
S : Sheaf J✝ RingCat
R✝ : Sheaf K RingCat
inst✝⁴ : F.IsContinuous J✝ K
inst✝³ : G.IsContinuous K J✝
adj : F ⊣ G
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J✝ K).obj R✝
ψ : R✝ ⟶ (G.sheafPushforwardContinuous RingCat K J✝).obj S
H₁ : whiskerRight (NatTrans.op adj.counit) R✝.obj = ψ.hom ≫ G.op.whiskerLeft φ.hom
H₂ : φ.hom ≫ F.op.whiskerLeft ψ.hom ≫ whiskerRight (NatTrans.op adj.unit) S.obj = 𝟙 S.obj
C : Type u'
inst✝² : Category.{v', u'} C
inst✝¹ : HasBinaryProducts C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝ : HasPullbacks C
X Y : C
f : X ⟶ Y
⊢ overMap R f ⊣ overPullback R f

Tactic:
by
  refine pushforwardPushforwardAdj (Over.mapPullbackAdj f) _ _ ?_ ?_
  · ext
    simp [Sheaf.pushforwardOverMapIso]
  · ext
    simp [← Functor.map_comp, ← op_comp, Sheaf.pushforwardOverMapIso]

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

Goal state before:
pp: case e'_2
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
iUV : (i : ι) → U i ⟶ V
hcover : V ≤ iSup U
s t : ToType (F.obj.obj (op V))
h : ∀ (i : ι), (ConcreteCategory.hom (F.obj.map (iUV i).op)) s = (ConcreteCategory.hom (F.obj.map (iUV i).op)) t
V_eq_supr_U : V = iSup U
this : (ConcreteCategory.hom (F.obj.map (eqToHom ⋯).op)) s = (ConcreteCategory.hom (F.obj.map (eqToHom ⋯).op)) t
⊢ s = (ConcreteCategory.hom (F.obj.map (eqToHom ⋯))) s

Tactic:
eqToHom_refl,

Goal state after:
case e'_2
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
iUV : (i : ι) → U i ⟶ V
hcover : V ≤ iSup U
s t : ToType (F.obj.obj (op V))
h : ∀ (i : ι), (ConcreteCategory.hom (F.obj.map (iUV i).op)) s = (ConcreteCategory.hom (F.obj.map (iUV i).op)) t
V_eq_supr_U : V = iSup U
this : (ConcreteCategory.hom (F.obj.map (eqToHom ⋯).op)) s = (ConcreteCategory.hom (F.obj.map (eqToHom ⋯).op)) t
⊢ s = (ConcreteCategory.hom (F.obj.map (𝟙 (op V)))) s
Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing

Goal state before:
pp: case e'_3
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
iUV : (i : ι) → U i ⟶ V
hcover : V ≤ iSup U
s t : ToType (F.obj.obj (op V))
h : ∀ (i : ι), (ConcreteCategory.hom (F.obj.map (iUV i).op)) s = (ConcreteCategory.hom (F.obj.map (iUV i).op)) t
V_eq_supr_U : V = iSup U
this : (ConcreteCategory.hom (F.obj.map (eqToHom ⋯).op)) s = (ConcreteCategory.hom (F.obj.map (eqToHom ⋯).op)) t
⊢ t = (ConcreteCategory.hom (F.obj.map (eqToHom ⋯))) t

Tactic:
eqToHom_refl,

Goal state after:
case e'_3
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
iUV : (i : ι) → U i ⟶ V
hcover : V ≤ iSup U
s t : ToType (F.obj.obj (op V))
h : ∀ (i : ι), (ConcreteCategory.hom (F.obj.map (iUV i).op)) s = (ConcreteCategory.hom (F.obj.map (iUV i).op)) t
V_eq_supr_U : V = iSup U
this : (ConcreteCategory.hom (F.obj.map (eqToHom ⋯).op)) s = (ConcreteCategory.hom (F.obj.map (eqToHom ⋯).op)) t
⊢ t = (ConcreteCategory.hom (F.obj.map (𝟙 (op V)))) t
Module: Mathlib.Topology.Algebra.Module.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : ContinuousConstSMul R M
inst✝ : ContinuousAdd M
s : Submodule R M
hs : IsCoatom s
⊢ IsClosed[inst✝⁴] ↑s ∨ Dense ↑s

Tactic:
refine (hs.le_iff.mp s.le_topologicalClosure).symm.imp ?_ dense_iff_topologicalClosure_eq_top.mpr
  exact fun h ↦ h ▸ isClosed_closure

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

Goal state before:
pp: case property.refine_3.pair.left
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s✝ : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X :=
  fun x ↦
    match x with
    | { down := j } => WalkingPair.casesOn j U V
hι : U ⊔ V = iSup ι
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
m : s.pt ⟶ (F.interUnionPullbackCone U V).pt
h₁ : m ≫ (F.interUnionPullbackCone U V).fst = s.fst
h₂ : m ≫ (F.interUnionPullbackCone U V).snd = s.snd
a✝ : ULift.{w, 0} WalkingPair
⊢ m ≫ F.obj.map ((eqToHom ⋯).op ≫ (homOfLE ⋯).op ≫ (homOfLE ⋯).op) =
    F.interUnionPullbackConeLift U V s ≫ F.obj.map ((eqToHom ⋯).op ≫ (homOfLE ⋯).op ≫ (homOfLE ⋯).op)

Tactic:
F.1.map_comp,

Goal state after:
case property.refine_3.pair.left
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s✝ : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X :=
  fun x ↦
    match x with
    | { down := j } => WalkingPair.casesOn j U V
hι : U ⊔ V = iSup ι
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
m : s.pt ⟶ (F.interUnionPullbackCone U V).pt
h₁ : m ≫ (F.interUnionPullbackCone U V).fst = s.fst
h₂ : m ≫ (F.interUnionPullbackCone U V).snd = s.snd
a✝ : ULift.{w, 0} WalkingPair
⊢ m ≫ F.obj.map (eqToHom ⋯).op ≫ F.obj.map (homOfLE ⋯).op ≫ F.obj.map (homOfLE ⋯).op =
    F.interUnionPullbackConeLift U V s ≫ F.obj.map (eqToHom ⋯).op ≫ F.obj.map (homOfLE ⋯).op ≫ F.obj.map (homOfLE ⋯).op
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
inst✝⁹ : Ring R₁
inst✝⁸ : Ring R₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst✝⁷ : RingHomInvPair σ₁₂ σ₂₁
M₁ : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M₁
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : Module R₁ M₁
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
inst✝ : IsTopologicalAddGroup M₁
f₁ : M₁ →SL[σ₁₂] M₂
f₂ : M₂ →SL[σ₂₁] M₁
h : Function.RightInverse ⇑f₂ ⇑f₁
x : ↥(↑f₁).ker
⊢ (f₁.projKerOfRightInverse f₂ h) ↑x = x

Tactic:
by
  ext1
  simp

Goal state after: