mathlib-initiative/mathlib-tactics huggingface dataset:
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 : PreOneHypercover S
c : Cofan E.X
hc : IsColimit c
d : Cofan E.Y'
hd : IsColimit d
F : Cᵒᵖ ⥤ A
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (E.X i)) F
inst✝ : PreservesLimit (Discrete.functor fun i ↦ op (E.Y' i)) F
⊢ IsLimit (E.multifork F) ≃ IsLimit (E.forkOfIsColimit hc hd F)

Tactic:
by
  letI c' : Fan (E.multicospanIndex F).left := Fan.mk _ fun i ↦ F.map (c.inj i).op
  letI hc' : IsLimit c' := isLimitFanMkObjOfIsLimit _ _ (fun i : E.I₀ ↦ _) (Cofan.IsColimit.op hc)
  letI d' : Fan (E.multicospanIndex F).right := Fan.mk _ fun i ↦ F.map (d.inj i).op
  letI hd' : IsLimit d' := isLimitFanMkObjOfIsLimit _ _ (fun i : E.I₁' ↦ _) (Cofan.IsColimit.op hd)
  refine (IsLimit.ofConeEquiv <|
    (E.multicospanIndex F).multiforkEquivPiForkOfIsLimit hc' hd').symm.trans ?_
  refine Fork.isLimitEquivOfIsos _ _ (Iso.refl _) (Iso.refl _) (Iso.refl _) ?_ ?_ ?_
  · refine Fan.IsLimit.hom_ext hd' _ _ fun i ↦ ?_
    simp only [multicospanShape_L, multicospanIndex_right, multicospanShape_R, Iso.refl_hom,
      Y'_apply, id_comp, comp_id]
    rw [MulticospanIndex.fstPiMapOfIsLimit_proj]
    simp [c', d', ← F.map_comp, ← op_comp]
  · refine Fan.IsLimit.hom_ext hd' _ _ fun i ↦ ?_
    simp only [multicospanShape_L, multicospanIndex_right, multicospanShape_R, Iso.refl_hom,
      Y'_apply, id_comp, comp_id]
    rw [MulticospanIndex.sndPiMapOfIsLimit_proj]
    simp [c', d', ← F.map_comp, ← op_comp]
  · refine Fan.IsLimit.hom_ext hc' _ _ fun i ↦ ?_
    simp
    simp [c']

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

Goal state before:
pp: C : Type uC
inst✝¹ : Category.{vC, uC} C
D : Type uD
inst✝ : Category.{vD, uD} D
G : C ⥤ D
J : GrothendieckTopology C
K : GrothendieckTopology D
U V : C
f : G.obj U ⟶ G.obj V
⊢ ∀ {Y Z : C} {f_1 : Y ⟶ U}, (∃ l, G.map l = G.map f_1 ≫ f) → ∀ (g : Z ⟶ Y), ∃ l, G.map l = G.map (g ≫ f_1) ≫ f

Tactic:
by
    rintro Y₁ Y₂ i₁ ⟨l, hl⟩ i₂
    exact ⟨i₂ ≫ l, by simp [hl]⟩

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

Goal state before:
pp: C : Type uC
inst✝² : Category.{vC, uC} C
D : Type uD
inst✝¹ : Category.{vD, uD} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : G.IsLocallyFull K
ℱ : Sheaf K (Type u_2)
X Y : C
i : G.obj X ⟶ G.obj Y
s t : ℱ.obj.obj (op (G.obj X))
h :
  ∀ ⦃Z : C⦄ (j : Z ⟶ X) (f : Z ⟶ Y),
    G.map f = G.map j ≫ i →
      (ConcreteCategory.hom (ℱ.obj.map (G.map j).op)) s = (ConcreteCategory.hom (ℱ.obj.map (G.map j).op)) t
Z : D
W : C
iWX : W ⟶ X
iZW : Z ⟶ G.obj W
iWY : W ⟶ Y
e : G.map iWY = G.map iWX ≫ i
⊢ (ConcreteCategory.hom (ℱ.obj.map (iZW ≫ G.map iWX).op)) s = (ConcreteCategory.hom (ℱ.obj.map (iZW ≫ G.map iWX).op)) t

Tactic:
simp [h iWX iWY e]

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
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : Sheaf K (Type v)
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
X : D
x : ℱ.obj (op X)
⊢ (pushforwardFamily α x).Compatible

Tactic:
suffices ∀ {Z W₁ W₂} (iWX₁ : G.obj W₁ ⟶ X) (iWX₂ : G.obj W₂ ⟶ X) (iZW₁ : Z ⟶ G.obj W₁)
      (iZW₂ : Z ⟶ G.obj W₂), iZW₁ ≫ iWX₁ = iZW₂ ≫ iWX₂ →
      ℱ'.1.map iZW₁.op (α.app _ (ℱ.map iWX₁.op x)) = ℱ'.1.map iZW₂.op (α.app _ (ℱ.map iWX₂.op x)) by
    rintro Y₁ Y₂ Z iZY₁ iZY₂ f₁ f₂ h₁ h₂ e
    simp only [pushforwardFamily, ← Functor.map_comp_apply, ← op_comp]
    generalize Nonempty.some h₁ = l₁
    generalize Nonempty.some h₂ = l₂
    obtain ⟨W₁, iYW₁, iWX₁, rfl⟩ := l₁
    obtain ⟨W₂, iYW₂, iWX₂, rfl⟩ := l₂
    exact this _ _ _ _ (by simpa only [Category.assoc] using e)

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
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : Sheaf K (Type v)
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
X : D
x : ℱ.obj (op X)
⊢ ∀ {Z : D} {W₁ W₂ : C} (iWX₁ : G.obj W₁ ⟶ X) (iWX₂ : G.obj W₂ ⟶ X) (iZW₁ : Z ⟶ G.obj W₁) (iZW₂ : Z ⟶ G.obj W₂),
    iZW₁ ≫ iWX₁ = iZW₂ ≫ iWX₂ →
      (ConcreteCategory.hom (ℱ'.obj.map iZW₁.op))
          ((ConcreteCategory.hom (α.app (op W₁))) ((ConcreteCategory.hom (ℱ.map iWX₁.op)) x)) =
        (ConcreteCategory.hom (ℱ'.obj.map iZW₂.op))
          ((ConcreteCategory.hom (α.app (op W₂))) ((ConcreteCategory.hom (ℱ.map iWX₂.op)) x))
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
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : Sheaf K (Type v)
α✝ : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj
X Y : Dᵒᵖ
f : X ⟶ Y
x : ℱ.obj X
Y' : C
f' : G.obj Y' ⟶ unop Y
⊢ (ConcreteCategory.hom (ℱ'.obj.map f'.op))
      ((ConcreteCategory.hom (appHom α (unop Y))) ((ConcreteCategory.hom (ℱ.map f)) x)) =
    (ConcreteCategory.hom (ℱ'.obj.map (f ≫ f'.op))) ((ConcreteCategory.hom (appHom α (unop X))) x)

Tactic:
appHom_restrict,

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
ℱ : Dᵒᵖ ⥤ Type v
ℱ' : Sheaf K (Type v)
α✝ : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj
inst✝¹ : G.IsCoverDense K
inst✝ : G.IsLocallyFull K
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj
X Y : Dᵒᵖ
f : X ⟶ Y
x : ℱ.obj X
Y' : C
f' : G.obj Y' ⟶ unop Y
⊢ (ConcreteCategory.hom (α.app (op Y'))) ((ConcreteCategory.hom (ℱ.map f'.op)) ((ConcreteCategory.hom (ℱ.map f)) x)) =
    (ConcreteCategory.hom (ℱ'.obj.map (f ≫ f'.op))) ((ConcreteCategory.hom (appHom α (unop X))) x)
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₁ : (yoneda.obj (((G.op.ran ⋙ (whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj Y.obj).obj (op U))).obj (op X)
⊢ ∀
    ⦃a₂ :
      (fun X ↦ X) ((yoneda.obj (((G.op.ran ⋙ (whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj Y.obj).obj (op U))).obj (op X))⦄,
    (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))) a₂ →
      f₁ = a₂

Tactic:
f₂

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)
⊢ (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₂ →
    f₁ = f₂
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: case refine_1.refine_3
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
i j : E.I₀ × F.I₀
W : C
p₁ : W ⟶ pullback (E.f i.1) (F.f i.2)
p₂ : W ⟶ pullback (E.f j.1) (F.f j.2)
w : p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) ≫ E.f i.1 = p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) ≫ E.f j.1
Y : C
f : Y ⟶ W
p : W ⟶ pullback ((E.inter F).f i) ((E.inter F).f j) := pullback.lift p₁ p₂ w
x✝ : ((E.inter F).sieve₁ p₁ p₂).arrows f
k : (E.inter F).I₁ i j
a : Y ⟶ (E.inter F).Y k
h₁ : f ≫ p₁ = a ≫ (E.inter F).p₁ k
h₂ : f ≫ p₂ = a ≫ (E.inter F).p₂ k
⊢ (fun x x_1 h ↦
      ((fun x f x_2 ↦
            Sieve.pullback f (F.sieve₁ (p₁ ≫ pullback.snd (E.f i.1) (F.f i.2)) (p₂ ≫ pullback.snd (E.f j.1) (F.f j.2))))
          x x_1 h).arrows)
    (pullback p ((E.inter F).toPullback k)) (pullback.fst p ((E.inter F).toPullback k)) ⋯ (pullback.lift f a ⋯)

pp: case refine_1.refine_4
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
i j : E.I₀ × F.I₀
W : C
p₁ : W ⟶ pullback (E.f i.1) (F.f i.2)
p₂ : W ⟶ pullback (E.f j.1) (F.f j.2)
w : p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) ≫ E.f i.1 = p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) ≫ E.f j.1
Y : C
f : Y ⟶ W
p : W ⟶ pullback ((E.inter F).f i) ((E.inter F).f j) := pullback.lift p₁ p₂ w
x✝ : ((E.inter F).sieve₁ p₁ p₂).arrows f
k : (E.inter F).I₁ i j
a : Y ⟶ (E.inter F).Y k
h₁ : f ≫ p₁ = a ≫ (E.inter F).p₁ k
h₂ : f ≫ p₂ = a ≫ (E.inter F).p₂ k
⊢ pullback.lift f a ⋯ ≫ pullback.fst p ((E.inter F).toPullback k) = f

Tactic:
· exact ⟨k.2, a ≫ pullback.snd _ _, by simp [reassoc_of% h₁], by simp [reassoc_of% h₂]⟩

Goal state after:
case refine_1.refine_4
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
i j : E.I₀ × F.I₀
W : C
p₁ : W ⟶ pullback (E.f i.1) (F.f i.2)
p₂ : W ⟶ pullback (E.f j.1) (F.f j.2)
w : p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) ≫ E.f i.1 = p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) ≫ E.f j.1
Y : C
f : Y ⟶ W
p : W ⟶ pullback ((E.inter F).f i) ((E.inter F).f j) := pullback.lift p₁ p₂ w
x✝ : ((E.inter F).sieve₁ p₁ p₂).arrows f
k : (E.inter F).I₁ i j
a : Y ⟶ (E.inter F).Y k
h₁ : f ≫ p₁ = a ≫ (E.inter F).p₁ k
h₂ : f ≫ p₂ = a ≫ (E.inter F).p₂ k
⊢ pullback.lift f a ⋯ ≫ pullback.fst p ((E.inter F).toPullback k) = f
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
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₂),
    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:
f₂

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
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₂),
    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.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
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
A : Type u_4
inst✝³ : Category.{v_4, u_4} A
inst✝² : IsDenseSubsite J K G
inst✝¹ : (G.sheafPushforwardContinuous A J K).IsEquivalence
inst✝ : HasWeakSheafify J A
P₁ P₂ : Dᵒᵖ ⥤ A
f : P₁ ⟶ P₂
Q : Sheaf K A
g : (sheafifyOfIsEquivalence J K G A).obj P₂ ⟶ Q
this✝ : G.IsLocallyFull K
this : G.IsCoverDense K
adj₁ : (G.sheafPushforwardContinuous A J K).asEquivalence.symm.functor ⊣
  (G.sheafPushforwardContinuous A J K).asEquivalence.symm.inverse :=
  (G.sheafPushforwardContinuous A J K).asEquivalence.symm.toAdjunction
adj₂ : presheafToSheaf J A ⊣ sheafToPresheaf J A := sheafificationAdjunction J A
⊢ IsCoverDense.restrictHomEquivHom
      ((adj₂.homEquiv (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj P₁)
          ((G.sheafPushforwardContinuous A J K).asEquivalence.symm.inverse.obj Q))
        ((adj₁.homEquiv ((presheafToSheaf J A).obj (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj P₁)) Q)
          ((sheafifyOfIsEquivalence J K G A).map f ≫ g))) =
    f ≫
      IsCoverDense.restrictHomEquivHom
        ((adj₂.homEquiv (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj P₂)
            ((G.sheafPushforwardContinuous A J K).asEquivalence.symm.inverse.obj Q))
          ((adj₁.homEquiv ((presheafToSheaf J A).obj (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj P₂)) Q) g))

Tactic:
← IsCoverDense.restrictHomEquivHom_naturality_left

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
J : GrothendieckTopology C
K : GrothendieckTopology D
G : C ⥤ D
A : Type u_4
inst✝³ : Category.{v_4, u_4} A
inst✝² : IsDenseSubsite J K G
inst✝¹ : (G.sheafPushforwardContinuous A J K).IsEquivalence
inst✝ : HasWeakSheafify J A
P₁ P₂ : Dᵒᵖ ⥤ A
f : P₁ ⟶ P₂
Q : Sheaf K A
g : (sheafifyOfIsEquivalence J K G A).obj P₂ ⟶ Q
this✝ : G.IsLocallyFull K
this : G.IsCoverDense K
adj₁ : (G.sheafPushforwardContinuous A J K).asEquivalence.symm.functor ⊣
  (G.sheafPushforwardContinuous A J K).asEquivalence.symm.inverse :=
  (G.sheafPushforwardContinuous A J K).asEquivalence.symm.toAdjunction
adj₂ : presheafToSheaf J A ⊣ sheafToPresheaf J A := sheafificationAdjunction J A
⊢ IsCoverDense.restrictHomEquivHom
      ((adj₂.homEquiv (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj P₁)
          ((G.sheafPushforwardContinuous A J K).asEquivalence.symm.inverse.obj Q))
        ((adj₁.homEquiv ((presheafToSheaf J A).obj (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj P₁)) Q)
          ((sheafifyOfIsEquivalence J K G A).map f ≫ g))) =
    IsCoverDense.restrictHomEquivHom
      (G.op.whiskerLeft f ≫
        (adj₂.homEquiv (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj P₂)
            ((G.sheafPushforwardContinuous A J K).asEquivalence.symm.inverse.obj Q))
          ((adj₁.homEquiv ((presheafToSheaf J A).obj (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).obj P₂)) Q) g))
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S : C
E F : PreOneHypercover S
e : E ≅ F
i : E.I₀
hs : (e.hom ≫ e.inv).s₀ = (𝟙 E).s₀
hh : ∀ (i : E.I₀), (e.hom ≫ e.inv).h₀ i = (𝟙 E).h₀ i ≫ eqToHom ⋯
h✝ :
  ∃ (hs₁ : ∀ (i j : E.I₀) (k : E.I₁ i j), (e.hom ≫ e.inv).s₁ k = (congrIndexOneOfEq ⋯ ⋯) ((𝟙 E).s₁ k)),
    ∀ (i j : E.I₀) (k : E.I₁ i j),
      (e.hom ≫ e.inv).h₁ k = (𝟙 E).h₁ k ≫ (congrIndexOneOfEqIso ⋯ ⋯ ((𝟙 E).s₁ k)).inv ≫ eqToHom ⋯
⊢ e.hom.h₀ i ≫ e.inv.h₀ (e.hom.s₀ i) = eqToHom ⋯

Tactic:
simpa using hh i

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S : C
E F : PreOneHypercover S
e : E ≅ F
i : F.I₀
hs : (e.inv ≫ e.hom).s₀ = (𝟙 F).s₀
hh : ∀ (i : F.I₀), (e.inv ≫ e.hom).h₀ i = (𝟙 F).h₀ i ≫ eqToHom ⋯
h✝ :
  ∃ (hs₁ : ∀ (i j : F.I₀) (k : F.I₁ i j), (e.inv ≫ e.hom).s₁ k = (congrIndexOneOfEq ⋯ ⋯) ((𝟙 F).s₁ k)),
    ∀ (i j : F.I₀) (k : F.I₁ i j),
      (e.inv ≫ e.hom).h₁ k = (𝟙 F).h₁ k ≫ (congrIndexOneOfEqIso ⋯ ⋯ ((𝟙 F).s₁ k)).inv ≫ eqToHom ⋯
⊢ e.inv.h₀ i ≫ e.hom.h₀ (e.inv.s₀ i) = eqToHom ⋯

Tactic:
simpa using hh i

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 F : PreOneHypercover S
f : E ≅ F
c : WalkingMulticospan E.multicospanShape
⊢ (Hom.mapMulticospan f.hom).map ((eqToIso ⋯).hom.app c) ≫ (eqToIso ⋯).hom.app ((Hom.mapMulticospan f.hom).obj c) =
    𝟙 ((Hom.mapMulticospan f.hom).obj c)

Tactic:
by
    cases c <;> rw [eqToIso.hom, eqToHom_app, eqToHom_map] <;> simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
hX : IsTerminal X
I : Type u_1
Y : I → C
⊢ J.CoversTop Y ↔ Sieve.ofObjects Y X ∈ J X

Tactic:
by
  constructor
  · tauto
  · intro h W
    apply J.superset_covering _ (J.pullback_stable (hX.from W) h)
    rintro T a ⟨i, ⟨b⟩⟩
    exact ⟨i, ⟨b⟩⟩

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
X Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
⊢ ∀ ⦃f₂ : Y₂ ⟶ X⦄ (h₁ : (Sieve.ofObjects Y X).arrows f₁) (h₂ : (Sieve.ofObjects Y X).arrows f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      (ConcreteCategory.hom (F.map g₁.op)) (x.familyOfElements X f₁ h₁) =
        (ConcreteCategory.hom (F.map g₂.op)) (x.familyOfElements X f₂ h₂)

Tactic:
f₂

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
I : Type u_1
Y : I → C
x : FamilyOfElementsOnObjects F Y
hx : x.IsCompatible
X Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
⊢ ∀ (h₁ : (Sieve.ofObjects Y X).arrows f₁) (h₂ : (Sieve.ofObjects Y X).arrows f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      (ConcreteCategory.hom (F.map g₁.op)) (x.familyOfElements X f₁ h₁) =
        (ConcreteCategory.hom (F.map g₂.op)) (x.familyOfElements X f₂ h₂)
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackFree

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
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝² : F.IsContinuous J K
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
inst✝¹ : (pushforward φ).IsRightAdjoint
inst✝ : F.Final
M : SheafOfModules R
f : unit R ⟶ M
⊢ ((pullbackPushforwardAdjunction φ).homEquiv (unit S) (unit R)) (pullbackObjUnitToUnit φ) ≫ (pushforward φ).map f =
    unitToPushforwardObjUnit φ ≫ (pushforward φ).map f

Tactic:
pullbackPushforwardAdjunction_homEquiv_pullbackObjUnitToUnit

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
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝² : F.IsContinuous J K
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
inst✝¹ : (pushforward φ).IsRightAdjoint
inst✝ : F.Final
M : SheafOfModules R
f : unit R ⟶ M
⊢ unitToPushforwardObjUnit φ ≫ (pushforward φ).map f = unitToPushforwardObjUnit φ ≫ (pushforward φ).map f
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
D : Type u_1
inst✝³ : Category.{v_1, u_1} D
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : F.IsEquivalence
X : C
inst✝ : Simple X
⊢ Simple (F.obj X)

Tactic:
rw [← F.asEquivalence_functor]

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
D : Type u_1
inst✝³ : Category.{v_1, u_1} D
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : F.IsEquivalence
X : C
inst✝ : Simple X
⊢ Simple (F.asEquivalence.functor.obj X)
Module: Mathlib.Algebra.Category.ModuleCat.Simple

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ IsSimpleOrder (Submodule R ↑(of R M)) ↔ IsSimpleModule R M

Tactic:
isSimpleModule_iff

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ IsSimpleOrder (Submodule R ↑(of R M)) ↔ IsSimpleOrder (Submodule R M)
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
X Y : C
inst✝¹ : Simple X
f : X ⟶ Y
inst✝ : Epi f
w : IsIso f → False
⊢ f = 0

Tactic:
by
  by_contra h
  exact w (isIso_of_epi_of_nonzero h)

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

Goal state before:
pp: 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✝ : (𝓝[{x | IsUnit x}] 0).NeBot
s : Submodule R M
y : M
hy : ↑s ∈ 𝓝 y
x : M
this : Tendsto (fun c ↦ y + c • x) (𝓝[{x | IsUnit x}] 0) (𝓝 (y + 0))
⊢ x ∈ s

Tactic:
rw [add_zero] at this

Goal state after:
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✝ : (𝓝[{x | IsUnit x}] 0).NeBot
s : Submodule R M
y : M
hy : ↑s ∈ 𝓝 y
x : M
this : Tendsto (fun c ↦ y + c • x) (𝓝[{x | IsUnit x}] 0) (𝓝 y)
⊢ x ∈ s
Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Goal state before:
pp: case property.refine_1
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)
⊢ F.interUnionPullbackConeLift U V s ≫ (F.interUnionPullbackCone U V).fst = s.fst

pp: case property.refine_2
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)
⊢ F.interUnionPullbackConeLift U V s ≫ (F.interUnionPullbackCone U V).snd = s.snd

pp: case property.refine_3
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},
    m ≫ (F.interUnionPullbackCone U V).fst = s.fst →
      m ≫ (F.interUnionPullbackCone U V).snd = s.snd → m = F.interUnionPullbackConeLift U V s

Tactic:
· apply interUnionPullbackConeLift_left

Goal state after:
case property.refine_2
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)
⊢ F.interUnionPullbackConeLift U V s ≫ (F.interUnionPullbackCone U V).snd = s.snd

case property.refine_3
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},
    m ≫ (F.interUnionPullbackCone U V).fst = s.fst →
      m ≫ (F.interUnionPullbackCone U V).snd = s.snd → m = F.interUnionPullbackConeLift U V s