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

Goal state before:
pp: case refine_1.refine_1
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
X : E
inst✝¹ : RepresentablyFlat F
inst✝ : IsCofiltered (StructuredArrow X G)
T : StructuredArrow X (F ⋙ G) ⥤ StructuredArrow X G := StructuredArrow.pre X F G
Y : StructuredArrow X G
A✝ : StructuredArrow Y.right F
this : Nonempty (StructuredArrow X (F ⋙ G))
A B : StructuredArrow X (F ⋙ G)
U : StructuredArrow X G := IsCofiltered.min (T.obj A) (T.obj B)
A' : StructuredArrow U.right F :=
  StructuredArrow.mk (StructuredArrow.Hom.right (IsCofiltered.minToLeft (T.obj A) (T.obj B)))
B' : StructuredArrow U.right F :=
  StructuredArrow.mk (StructuredArrow.Hom.right (IsCofiltered.minToRight (T.obj A) (T.obj B)))
⊢ (StructuredArrow.mk (U.hom ≫ G.map (IsCofiltered.min A' B').hom)).hom ≫
      (F ⋙ G).map (StructuredArrow.Hom.right (IsCofiltered.minToLeft A' B')) =
    A.hom

pp: case refine_1.refine_2
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
X : E
inst✝¹ : RepresentablyFlat F
inst✝ : IsCofiltered (StructuredArrow X G)
T : StructuredArrow X (F ⋙ G) ⥤ StructuredArrow X G := StructuredArrow.pre X F G
Y : StructuredArrow X G
A✝ : StructuredArrow Y.right F
this : Nonempty (StructuredArrow X (F ⋙ G))
A B : StructuredArrow X (F ⋙ G)
U : StructuredArrow X G := IsCofiltered.min (T.obj A) (T.obj B)
A' : StructuredArrow U.right F :=
  StructuredArrow.mk (StructuredArrow.Hom.right (IsCofiltered.minToLeft (T.obj A) (T.obj B)))
B' : StructuredArrow U.right F :=
  StructuredArrow.mk (StructuredArrow.Hom.right (IsCofiltered.minToRight (T.obj A) (T.obj B)))
⊢ (StructuredArrow.mk (U.hom ≫ G.map (IsCofiltered.min A' B').hom)).hom ≫
      (F ⋙ G).map (StructuredArrow.Hom.right (IsCofiltered.minToRight A' B')) =
    B.hom

Tactic:
· simp [← Functor.map_comp, A', T]

Goal state after:
case refine_1.refine_2
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
X : E
inst✝¹ : RepresentablyFlat F
inst✝ : IsCofiltered (StructuredArrow X G)
T : StructuredArrow X (F ⋙ G) ⥤ StructuredArrow X G := StructuredArrow.pre X F G
Y : StructuredArrow X G
A✝ : StructuredArrow Y.right F
this : Nonempty (StructuredArrow X (F ⋙ G))
A B : StructuredArrow X (F ⋙ G)
U : StructuredArrow X G := IsCofiltered.min (T.obj A) (T.obj B)
A' : StructuredArrow U.right F :=
  StructuredArrow.mk (StructuredArrow.Hom.right (IsCofiltered.minToLeft (T.obj A) (T.obj B)))
B' : StructuredArrow U.right F :=
  StructuredArrow.mk (StructuredArrow.Hom.right (IsCofiltered.minToRight (T.obj A) (T.obj B)))
⊢ (StructuredArrow.mk (U.hom ≫ G.map (IsCofiltered.min A' B').hom)).hom ≫
      (F ⋙ G).map (StructuredArrow.Hom.right (IsCofiltered.minToRight A' B')) =
    B.hom
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: C : Type ?u.2
D : Type ?u.4
inst✝¹ : Category.{v_1, ?u.2} C
inst✝ : Category.{v_2, ?u.4} D
x y : Coverage C
⊢ ∀ ⦃X Y : C⦄ (f : Y ⟶ X),
    ∀ S ∈ x.coverings X ∪ y.coverings X, ∃ T ∈ x.coverings Y ∪ y.coverings Y, T.FactorsThruAlong S f

Tactic:
rintro X Y f S (hx | hy)

Goal state after:
case inl
C : Type ?u.2
D : Type ?u.4
inst✝¹ : Category.{v_1, ?u.2} C
inst✝ : Category.{v_2, ?u.4} D
x y : Coverage C
X Y : C
f : Y ⟶ X
S : Presieve X
hx : S ∈ x.coverings X
⊢ ∃ T ∈ x.coverings Y ∪ y.coverings Y, T.FactorsThruAlong S f

case inr
C : Type ?u.2
D : Type ?u.4
inst✝¹ : Category.{v_1, ?u.2} C
inst✝ : Category.{v_2, ?u.4} D
x y : Coverage C
X Y : C
f : Y ⟶ X
S : Presieve X
hy : S ∈ y.coverings X
⊢ ∃ T ∈ x.coverings Y ∪ y.coverings Y, T.FactorsThruAlong S f
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
⊢ (Cofan.IsColimit.desc hd fun x ↦ E.p₁ x.snd ≫ c.inj x.fst.1) ≫ Cofan.IsColimit.desc hc E.f =
    (Cofan.IsColimit.desc hd fun x ↦ E.p₂ x.snd ≫ c.inj x.fst.2) ≫ Cofan.IsColimit.desc hc E.f

Tactic:
exact Cofan.IsColimit.hom_ext hd _ _ (by simp [E.w])

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 : 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:
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.DenseSubsite.SheafEquiv

Goal state before:
pp: case right
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)
⊢ ∃ a, (ConcreteCategory.hom ((yoneda.map ((G.op.ranCounit.app Y.obj).app (op U))).app (op X))) a = f

Tactic:
have (X Y Z) (f : X ⟶ Y) (g : G.obj Y ⟶ G.obj Z) (hf : G.imageSieve g f) : Exists _ := hf

Goal state after:
case right
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)
this : ∀ (X Y Z : C) (f : X ⟶ Y) (g : G.obj Y ⟶ G.obj Z), (G.imageSieve g).arrows f → ∃ l, G.map l = G.map f ≫ g
⊢ ∃ a, (ConcreteCategory.hom ((yoneda.map ((G.op.ranCounit.app Y.obj).app (op U))).app (op X))) a = f
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv

Goal state before:
pp: 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
g : StructuredArrow (op (G.obj U)) G.op
I₁ I₂ : GrothendieckTopology.Cover.Arrow ⟨G.imageSieve g.hom.unop, ⋯⟩
r : I₁.Relation I₂
⊢ G.map (r.g₁ ≫ I₁.f) ≫ g.hom.unop = G.map r.g₂ ≫ G.map I₂.f ≫ g.hom.unop

Tactic:
r.w,

Goal state after:
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
g : StructuredArrow (op (G.obj U)) G.op
I₁ I₂ : GrothendieckTopology.Cover.Arrow ⟨G.imageSieve g.hom.unop, ⋯⟩
r : I₁.Relation I₂
⊢ G.map (r.g₂ ≫ I₂.f) ≫ g.hom.unop = G.map r.g₂ ≫ G.map I₂.f ≫ g.hom.unop
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
      have := hR hf _ (𝟙 _)
      rw [pullback_id, pullback_comp] at this
      apply this

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
toHomf : E.Hom F.toPreZeroHypercover
fs₁ : {i j : E.I₀} → E.I₁ i j → F.I₁ (toHomf.s₀ i) (toHomf.s₀ j)
fh₁ : {i j : E.I₀} → (k : E.I₁ i j) → E.Y k ⟶ F.Y (fs₁ k)
w₁₁✝¹ : ∀ {i j : E.I₀} (k : E.I₁ i j), fh₁ k ≫ F.p₁ (fs₁ k) = E.p₁ k ≫ toHomf.h₀ i
w₁₂✝¹ : ∀ {i j : E.I₀} (k : E.I₁ i j), fh₁ k ≫ F.p₂ (fs₁ k) = E.p₂ k ≫ toHomf.h₀ j
gh₁ : {i j : E.I₀} → (k : E.I₁ i j) → E.Y k ⟶ F.Y (fs₁ k)
w₁₁✝ : ∀ {i j : E.I₀} (k : E.I₁ i j), gh₁ k ≫ F.p₁ (fs₁ k) = E.p₁ k ≫ toHomf.h₀ i
w₁₂✝ : ∀ {i j : E.I₀} (k : E.I₁ i j), gh₁ k ≫ F.p₂ (fs₁ k) = E.p₂ k ≫ toHomf.h₀ j
hs₀ :
  { toHom := toHomf, s₁ := fs₁, h₁ := fh₁, w₁₁ := w₁₁✝¹, w₁₂ := w₁₂✝¹ }.s₀ =
    { toHom := toHomf, s₁ := fs₁, h₁ := gh₁, w₁₁ := w₁₁✝, w₁₂ := w₁₂✝ }.s₀
hh₀ :
  ∀ (i : E.I₀),
    { toHom := toHomf, s₁ := fs₁, h₁ := fh₁, w₁₁ := w₁₁✝¹, w₁₂ := w₁₂✝¹ }.h₀ i =
      { toHom := toHomf, s₁ := fs₁, h₁ := gh₁, w₁₁ := w₁₁✝, w₁₂ := w₁₂✝ }.h₀ i ≫ eqToHom ⋯
hs₁ :
  ∀ (i j : E.I₀) (k : E.I₁ i j),
    { toHom := toHomf, s₁ := fs₁, h₁ := fh₁, w₁₁ := w₁₁✝¹, w₁₂ := w₁₂✝¹ }.s₁ k =
      (congrIndexOneOfEq ⋯ ⋯) ({ toHom := toHomf, s₁ := fs₁, h₁ := gh₁, w₁₁ := w₁₁✝, w₁₂ := w₁₂✝ }.s₁ k)
hh₁ :
  ∀ (i j : E.I₀) (k : E.I₁ i j),
    { toHom := toHomf, s₁ := fs₁, h₁ := fh₁, w₁₁ := w₁₁✝¹, w₁₂ := w₁₂✝¹ }.h₁ k =
      { toHom := toHomf, s₁ := fs₁, h₁ := gh₁, w₁₁ := w₁₁✝, w₁₂ := w₁₂✝ }.h₁ k ≫
        (congrIndexOneOfEqIso ⋯ ⋯ ({ toHom := toHomf, s₁ := fs₁, h₁ := gh₁, w₁₁ := w₁₁✝, w₁₂ := w₁₂✝ }.s₁ k)).inv ≫
          eqToHom ⋯
⊢ { toHom := toHomf, s₁ := fs₁, h₁ := fh₁, w₁₁ := w₁₁✝¹, w₁₂ := w₁₂✝¹ } =
    { toHom := toHomf, s₁ := fs₁, h₁ := gh₁, w₁₁ := w₁₁✝, w₁₂ := w₁₂✝ }

Tactic:
simp_all only [eqToHom_refl, Category.comp_id, implies_true, congrIndexOneOfEqIso_refl,
    Iso.refl_inv, mk.injEq, heq_eq_eq, true_and]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
toHomf : E.Hom F.toPreZeroHypercover
fs₁ : {i j : E.I₀} → E.I₁ i j → F.I₁ (toHomf.s₀ i) (toHomf.s₀ j)
fh₁ : {i j : E.I₀} → (k : E.I₁ i j) → E.Y k ⟶ F.Y (fs₁ k)
w₁₁✝¹ : ∀ {i j : E.I₀} (k : E.I₁ i j), fh₁ k ≫ F.p₁ (fs₁ k) = E.p₁ k ≫ toHomf.h₀ i
w₁₂✝¹ : ∀ {i j : E.I₀} (k : E.I₁ i j), fh₁ k ≫ F.p₂ (fs₁ k) = E.p₂ k ≫ toHomf.h₀ j
gh₁ : {i j : E.I₀} → (k : E.I₁ i j) → E.Y k ⟶ F.Y (fs₁ k)
w₁₁✝ : ∀ {i j : E.I₀} (k : E.I₁ i j), gh₁ k ≫ F.p₁ (fs₁ k) = E.p₁ k ≫ toHomf.h₀ i
w₁₂✝ : ∀ {i j : E.I₀} (k : E.I₁ i j), gh₁ k ≫ F.p₂ (fs₁ k) = E.p₂ k ≫ toHomf.h₀ j
hs₀ :
  { toHom := toHomf, s₁ := fs₁, h₁ := fh₁, w₁₁ := w₁₁✝¹, w₁₂ := w₁₂✝¹ }.s₀ =
    { toHom := toHomf, s₁ := fs₁, h₁ := gh₁, w₁₁ := w₁₁✝, w₁₂ := w₁₂✝ }.s₀
hs₁ :
  ∀ (i j : E.I₀) (k : E.I₁ i j),
    { toHom := toHomf, s₁ := fs₁, h₁ := fh₁, w₁₁ := w₁₁✝¹, w₁₂ := w₁₂✝¹ }.s₁ k =
      (congrIndexOneOfEq ⋯ ⋯) ({ toHom := toHomf, s₁ := fs₁, h₁ := gh₁, w₁₁ := w₁₁✝, w₁₂ := w₁₂✝ }.s₁ k)
hh₁ : ∀ (i j : E.I₀) (k : E.I₁ i j), fh₁ k = gh₁ k ≫ 𝟙 (F.Y ((congrIndexOneOfEq ⋯ ⋯) (fs₁ k)))
⊢ fh₁ = gh₁
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology

Goal state before:
pp: C : Type u_3
D : Type u_4
inst✝⁵ : Category.{v_3, u_3} C
inst✝⁴ : Category.{v_4, u_4} D
F : C ⥤ D
K : Precoverage D
inst✝³ : K.HasIsos
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasPullbacks
H : ∀ {S : C} {R : Presieve (F.obj S)}, R ∈ K.coverings (F.obj S) → map F (functorPullback F R) ∈ K.coverings (F.obj S)
U : C
x✝ : ↑(K.toGrothendieck (F.obj U))
T : Sieve (F.obj U)
hT : T ∈ K.toGrothendieck (F.obj U)
⊢ Sieve.functorPushforward F (Sieve.functorPullback F ↑⟨T, hT⟩) ∈ K.toGrothendieck (F.obj U)

Tactic:
rw [Precoverage.mem_toGrothendieck_iff_of_isStableUnderComposition] at hT ⊢

Goal state after:
C : Type u_3
D : Type u_4
inst✝⁵ : Category.{v_3, u_3} C
inst✝⁴ : Category.{v_4, u_4} D
F : C ⥤ D
K : Precoverage D
inst✝³ : K.HasIsos
inst✝² : K.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderComposition
inst✝ : K.HasPullbacks
H : ∀ {S : C} {R : Presieve (F.obj S)}, R ∈ K.coverings (F.obj S) → map F (functorPullback F R) ∈ K.coverings (F.obj S)
U : C
x✝ : ↑(K.toGrothendieck (F.obj U))
T : Sieve (F.obj U)
hT✝ : T ∈ K.toGrothendieck (F.obj U)
hT : ∃ R ∈ K.coverings (F.obj U), R ≤ T.arrows
⊢ ∃ R ∈ K.coverings (F.obj U), R ≤ (Sieve.functorPushforward F (Sieve.functorPullback F ↑⟨T, hT✝⟩)).arrows
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: case refine_1.refine_3
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.fst i) ≫
        (G.mapIso (asIso (f.hom.h₁ i.snd)).symm.op).hom =
      (G.mapIso (asIso (f.hom.h₀ (E.multicospanShape.fst i))).symm.op).hom ≫
        ((equivalenceMulticospanOfIso f).functor ⋙ (F.multicospanIndex G).multicospan).map
          (WalkingMulticospan.Hom.fst 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.left
⊢ (functorPushforward (Over.forget X) (functorPullback (Over.forget X) S)).arrows = S.arrows

Tactic:
simp [← arrows_generate_map_eq_functorPushforward]

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

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

Tactic:
· 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.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_contra h
  exact w (isIso_of_epi_of_nonzero h)

Goal state after:
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
inst✝² : F.IsCocontinuous J K
inst✝¹ : IsIso φ
inst✝ : F.IsLeftAdjoint
⊢ (pushforward φ).IsLeftAdjoint

Tactic:
let adj := Adjunction.ofIsLeftAdjoint F
  let shAdj := adj.sheafPushforwardContinuous (E := RingCat.{u}) J K
  let ψ : R ⟶ (F.rightAdjoint.sheafPushforwardContinuous RingCat.{u} K J).obj S :=
    shAdj.unit.app R ≫ (F.rightAdjoint.sheafPushforwardContinuous _ _ _).map (inv φ)
  refine (SheafOfModules.pushforwardPushforwardAdj adj φ ψ ?_ ?_).isLeftAdjoint
  · ext U : 2
    simp [ψ, shAdj]
  · ext U : 2
    have := (inv φ).hom.naturality
    dsimp at this
    simp only [ObjectProperty.hom_inv, NatIso.isIso_inv_app, sheafPushforwardContinuous_obj_obj_obj,
      IsIso.eq_inv_comp] at this
    simp [ψ, shAdj, ← this, ← Functor.map_comp_assoc, ← op_comp]

Goal state after:
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
x : C
⊢ pushforward (𝟙 (R.over x)) ⊣ pushforward (pushforwardOver x)

Tactic:
by
  refine pushforwardPushforwardAdj (Over.forgetAdjStar x) (𝟙 (R.over x)) _ ?_ ?_
  · ext y : 2
    simp [pushforwardOver]
  · ext y : 2
    simp [pushforwardOver, ← Functor.map_comp, ← op_comp]

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

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

Tactic:
have V_eq_supr_U : V = iSup U := le_antisymm hcover (iSup_le fun i => (iUV i).le)

Goal state after:
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
sf : (i : ι) → ToType (F.obj.obj (op (U i)))
h : IsCompatible F.obj U sf
V_eq_supr_U : V = iSup U
⊢ ∃! s, ∀ (i : ι), (ConcreteCategory.hom (F.obj.map (iUV i).op)) s = sf i
Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasLimitsOfSize.{x, x, v_1, u_1} C
inst✝¹ : (CategoryTheory.forget C).ReflectsIsomorphisms
inst✝ : PreservesLimitsOfSize.{x, x, v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget C)
X : TopCat
F : Sheaf C X
ι : Type u_4
U : ι → Opens ↑X
V : Opens ↑X
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
⊢ s = t

Tactic:
have V_eq_supr_U : V = iSup U := le_antisymm hcover (iSup_le fun i => (iUV i).le)

Goal state after:
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
⊢ s = t
Module: Mathlib.Topology.Algebra.Module.ModuleTopology

Goal state before:
pp: R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
σ : R →+* S
σ' : S →+* R
inst✝⁶ : RingHomInvPair σ σ'
inst✝⁵ : RingHomInvPair σ' σ
A : Type u_3
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R A
τA : TopologicalSpace A
inst✝² : IsModuleTopology R A
B' : Type u_5
inst✝¹ : AddCommMonoid B'
inst✝ : Module S B'
τB' : TopologicalSpace B'
hσ : Continuous ⇑σ
hσ' : Continuous ⇑σ'
e : A ≃SL[σ] B'
g : A →ₛₗ[σ] B' := ↑↑e
g' : B' →ₛₗ[σ'] A := ↑↑e.symm
h : A →+ B' := ↑e
h' : B' →+ A := ↑e.symm
⊢ τB' = moduleTopology S B'

Tactic:
e.toHomeomorph.symm.isInducing.1,

Goal state after:
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
σ : R →+* S
σ' : S →+* R
inst✝⁶ : RingHomInvPair σ σ'
inst✝⁵ : RingHomInvPair σ' σ
A : Type u_3
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R A
τA : TopologicalSpace A
inst✝² : IsModuleTopology R A
B' : Type u_5
inst✝¹ : AddCommMonoid B'
inst✝ : Module S B'
τB' : TopologicalSpace B'
hσ : Continuous ⇑σ
hσ' : Continuous ⇑σ'
e : A ≃SL[σ] B'
g : A →ₛₗ[σ] B' := ↑↑e
g' : B' →ₛₗ[σ'] A := ↑↑e.symm
h : A →+ B' := ↑e
h' : B' →+ A := ↑e.symm
⊢ TopologicalSpace.induced (⇑e.toHomeomorph.symm) τA = moduleTopology S B'
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer

Goal state before:
pp: J : MulticospanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
b : J.R
h₂ : J.snd b = J.fst b
f : (left (J.fst b) ⟶ right b) → Prop :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ f (eqToHom ⋯ ≫ Hom.fst b) = ?m.540 (J.fst b) ⋯ h₂

Tactic:
simp only [eqToHom_refl, Category.id_comp, f]

Goal state after:
J : MulticospanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
b : J.R
h₂ : J.snd b = J.fst b
f : (left (J.fst b) ⟶ right b) → Prop :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ True = ?m.540 (J.fst b) ⋯ h₂