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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : RepresentablyFlat F
J : Type ?u.26
𝒥✝ : SmallCategory J
x✝ : FinCategory J
K : J ⥤ C
⊢ ∀ {c : Cone K} (hc : IsLimit c), Nonempty (IsLimit (F.mapCone c))

Tactic:
intro c

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : RepresentablyFlat F
J : Type ?u.26
𝒥✝ : SmallCategory J
x✝ : FinCategory J
K : J ⥤ C
c : Cone K
⊢ ∀ (hc : IsLimit c), Nonempty (IsLimit (F.mapCone c))
Module: Mathlib.CategoryTheory.Sites.Closed

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
S : Sieve X
H : Presieve.IsSheafFor (Functor.closedSieves J).toFunctor S.arrows
this✝ : J.IsClosed ⊤
this : ⟨J.close S, ⋯⟩ = ⟨⊤, this✝⟩
⊢ J.close S = ⊤

Tactic:
rw [Subtype.ext_iff] at this

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
S : Sieve X
H : Presieve.IsSheafFor (Functor.closedSieves J).toFunctor S.arrows
this✝ : J.IsClosed ⊤
this : ↑⟨J.close S, ⋯⟩ = ↑⟨⊤, this✝⟩
⊢ J.close S = ⊤
Module: Mathlib.CategoryTheory.Sites.Hypercover.Zero

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
S : C
R : Presieve S
⊢ R.preZeroHypercover.presieve₀ = R

Tactic:
by
  refine le_antisymm ?_ ?_
  · rintro - - ⟨i⟩
    exact i.2
  · intro Y f h
    let i : R.uncurry := ⟨⟨Y, f⟩, h⟩
    exact .mk i

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

Goal state before:
pp: C : Type u_2
inst✝ : Category.{v_1, u_2} C
X : C
S T : Presieve X
P : Cᵒᵖ ⥤ Type u_1
h : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ R, IsSeparatedFor P R ∧ R.FactorsThruAlong S f
hS : IsSeparatedFor P S ∧ ∀ (x : FamilyOfElements P S), x.Compatible → ∃ t, x.IsAmalgamation t
W : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → S g → C
i : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → Z ⟶ W a
e : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → W a ⟶ X
h1 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), T (e a)
h2 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), i a ≫ e a = g
x : FamilyOfElements P T
hx : x.Compatible
y : FamilyOfElements P S := fun Y g hg ↦ (ConcreteCategory.hom (P.map (i hg).op)) (x (e hg) ⋯)
⊢ y.Compatible

Tactic:
intro Y₁ Y₂ Z g₁ g₂ f₁ f₂ h₁ h₂ h

Goal state after:
C : Type u_2
inst✝ : Category.{v_1, u_2} C
X : C
S T : Presieve X
P : Cᵒᵖ ⥤ Type u_1
h✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, T f → ∃ R, IsSeparatedFor P R ∧ R.FactorsThruAlong S f
hS : IsSeparatedFor P S ∧ ∀ (x : FamilyOfElements P S), x.Compatible → ∃ t, x.IsAmalgamation t
W : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → S g → C
i : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → Z ⟶ W a
e : ⦃Z : C⦄ → ⦃g : Z ⟶ X⦄ → (a : S g) → W a ⟶ X
h1 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), T (e a)
h2 : ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄ (a : S g), i a ≫ e a = g
x : FamilyOfElements P T
hx : x.Compatible
y : FamilyOfElements P S := fun Y g hg ↦ (ConcreteCategory.hom (P.map (i hg).op)) (x (e hg) ⋯)
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : S f₁
h₂ : S f₂
h : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ (ConcreteCategory.hom (P.map g₁.op)) (y f₁ h₁) = (ConcreteCategory.hom (P.map g₂.op)) (y f₂ h₂)
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
J : Precoverage C
inst✝¹ : J.HasPullbacks
inst✝ : J.IsStableUnderBaseChange
X Y : C
f : Y ⟶ X
S : Presieve X
hS : S ∈ J.coverings X
⊢ ∃ T ∈ J.coverings Y, T.FactorsThruAlong S f

Tactic:
have : S.HasPullbacks f := J.hasPullbacks_of_mem _ hS

Goal state after:
C : Type ?u.2
D : Type ?u.4
inst✝³ : Category.{v_1, ?u.2} C
inst✝² : Category.{v_2, ?u.4} D
J : Precoverage C
inst✝¹ : J.HasPullbacks
inst✝ : J.IsStableUnderBaseChange
X Y : C
f : Y ⟶ X
S : Presieve X
hS : S ∈ J.coverings X
this : S.HasPullbacks f
⊢ ∃ T ∈ J.coverings Y, T.FactorsThruAlong S f
Module: Mathlib.CategoryTheory.Functor.KanExtension.Preserves

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst✝⁵ : Category.{v_1, u_1} A
inst✝⁴ : Category.{v_2, u_2} B
inst✝³ : Category.{v_3, u_3} C
inst✝² : Category.{v_4, u_4} D
G : B ⥤ D
F : A ⥤ B
L : A ⥤ C
inst✝¹ : G.PreservesPointwiseRightKanExtension F L
inst✝ : L.HasPointwiseRightKanExtension F
a : A
⊢ (G.pointwiseRightKanExtensionCompIsoOfPreserves F L).hom.app (L.obj a) ≫
      (L.pointwiseRightKanExtensionCounit (F ⋙ G)).app a =
    G.map ((L.pointwiseRightKanExtensionCounit F).app a)

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

Goal state after:
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
X : C
E : PreOneHypercover X
F : C ⥤ D
⊢ Sieve.generate (E.map F).presieve₀ = Sieve.functorPushforward F E.sieve₀

Tactic:
PreOneHypercover.map_toPreZeroHypercover,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
E : PreOneHypercover X
F : C ⥤ D
⊢ Sieve.generate (PreZeroHypercover.map F E.toPreZeroHypercover).presieve₀ = Sieve.functorPushforward F E.sieve₀
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
X : C
E : PreOneHypercover X
F : C ⥤ D
W : C
i₁ i₂ : E.I₀
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
Y : C
f : Y ⟶ W
k : E.I₁ i₁ i₂
u : Y ⟶ E.Y k
hf₁ : f ≫ p₁ = u ≫ E.p₁ k
hf₂ : f ≫ p₂ = u ≫ E.p₂ k
⊢ (Sieve.functorPullback F ((E.map F).sieve₁ (F.map p₁) (F.map p₂))).arrows f

Tactic:
exact ⟨k, F.map u, by simp [← Functor.map_comp, hf₁], by simp [← Functor.map_comp, hf₂]⟩

Goal state after:
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
X : C
E : PreOneHypercover X
F : C ⥤ D
W : C
i₁ i₂ : E.I₀
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
h : p₁ ≫ E.f i₁ = p₂ ≫ E.f i₂
inst✝¹ : HasPullbacks C
inst✝ : PreservesLimitsOfShape WalkingCospan F
this : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
T : D
f : T ⟶ F.obj W
k : (E.map F).I₁ i₁ i₂
u : T ⟶ (E.map F).Y k
hf₁ : f ≫ F.map p₁ = u ≫ (E.map F).p₁ k
hf₂ : f ≫ F.map p₂ = u ≫ (E.map F).p₂ k
l : W ⟶ pullback (E.f i₁) (E.f i₂) := pullback.lift p₁ p₂ h
⊢ (Sieve.functorPushforward F (E.sieve₁ p₁ p₂)).arrows f

Tactic:
have hl₁ : l ≫ pullback.fst _ _ = p₁ := by simp [l]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
X : C
E : PreOneHypercover X
F : C ⥤ D
W : C
i₁ i₂ : E.I₀
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
h : p₁ ≫ E.f i₁ = p₂ ≫ E.f i₂
inst✝¹ : HasPullbacks C
inst✝ : PreservesLimitsOfShape WalkingCospan F
this : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
T : D
f : T ⟶ F.obj W
k : (E.map F).I₁ i₁ i₂
u : T ⟶ (E.map F).Y k
hf₁ : f ≫ F.map p₁ = u ≫ (E.map F).p₁ k
hf₂ : f ≫ F.map p₂ = u ≫ (E.map F).p₂ k
l : W ⟶ pullback (E.f i₁) (E.f i₂) := pullback.lift p₁ p₂ h
hl₁ : l ≫ pullback.fst (E.f i₁) (E.f i₂) = p₁
⊢ (Sieve.functorPushforward F (E.sieve₁ p₁ p₂)).arrows f
Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck

Goal state before:
pp: C : Type u_3
inst✝ : Category.{u_2, u_3} C
J : Precoverage C
P : Cᵒᵖ ⥤ Type u_1
h : IsSheaf J.toGrothendieck P
S : C
R : Presieve S
hR : R ∈ J.coverings S
⊢ IsSheafFor P R

Tactic:
rw [J.isSheaf_toGrothendieck_iff] at h

Goal state after:
C : Type u_3
inst✝ : Category.{u_2, u_3} C
J : Precoverage C
P : Cᵒᵖ ⥤ Type u_1
h : ∀ {X Y : C} {f : Y ⟶ X}, ∀ R ∈ J.coverings X, IsSheafFor P (Sieve.pullback f (Sieve.generate R)).arrows
S : C
R : Presieve S
hR : R ∈ J.coverings S
⊢ IsSheafFor P R
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 J (F.op ⋙ G.obj)

Tactic:
← Presieve.isSheaf_comp_uliftFunctor_iff.{t, max u₁ v₁ u₂ v₂},

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)
⊢ Presieve.IsSheaf J ((F.op ⋙ G.obj) ⋙ uliftFunctor.{max u₁ v₁ u₂ v₂, t})
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
i₁ i₂ : E.I₀
inst✝ : HasPullback (E.f i₁) (E.f i₂)
W : C
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
w : p₁ ≫ E.f i₁ = p₂ ≫ E.f i₂
Z : C
g : Z ⟶ W
⊢ (Sieve.pullback (pullback.lift p₁ p₂ w) (E.sieve₁' i₁ i₂)).arrows g → (E.sieve₁ p₁ p₂).arrows g

Tactic:
rintro ⟨_, h, w, ⟨j⟩, fac⟩
    exact ⟨j, h, by simpa using fac.symm =≫ pullback.fst _ _,
      by simpa using fac.symm =≫ pullback.snd _ _⟩

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
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
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj
X Y : Aᵒᵖ
f : X ⟶ Y
⊢ (coyoneda ⋙ (whiskeringLeft Dᵒᵖ A (Type v_4)).obj ℱ).map f ≫ presheafHom (homOver α (unop Y)) =
    presheafHom (homOver α (unop X)) ≫ (coyoneda ⋙ (whiskeringLeft Dᵒᵖ A (Type v_4)).obj ℱ'.obj).map f

Tactic:
ext U x

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
α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.obj
X Y : Aᵒᵖ
f : X ⟶ Y
U : Dᵒᵖ
x : ((coyoneda ⋙ (whiskeringLeft Dᵒᵖ A (Type v_4)).obj ℱ).obj X).obj U
⊢ (ConcreteCategory.hom
          (((coyoneda ⋙ (whiskeringLeft Dᵒᵖ A (Type v_4)).obj ℱ).map f ≫ presheafHom (homOver α (unop Y))).app U)).toFun
      x =
    (ConcreteCategory.hom
          ((presheafHom (homOver α (unop X)) ≫ (coyoneda ⋙ (whiskeringLeft Dᵒᵖ A (Type v_4)).obj ℱ'.obj).map f).app
            U)).toFun
      x
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: case refine_1.refine_2.refine_1
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.fst p ((E.inter F).toPullback k) ≫ p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) =
    (pullback.snd p ((E.inter F).toPullback k) ≫ pullback.fst (E.p₁ k.1 ≫ E.f i.1) (F.p₁ k.2 ≫ F.f i.2)) ≫ E.p₁ k.1

pp: case refine_1.refine_2.refine_2
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.fst p ((E.inter F).toPullback k) ≫ p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) =
    (pullback.snd p ((E.inter F).toPullback k) ≫ pullback.fst (E.p₁ k.1 ≫ E.f i.1) (F.p₁ k.2 ≫ F.f i.2)) ≫ E.p₂ k.1

Tactic:
· have : p₁ ≫ pullback.fst (E.f i.1) (F.f i.2) = p ≫ pullback.fst _ _ ≫ pullback.fst _ _ := by
          simp [p]
        simp [this, pullback.condition_assoc, toPullback]

Goal state after:
case refine_1.refine_2.refine_2
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.fst p ((E.inter F).toPullback k) ≫ p₂ ≫ pullback.fst (E.f j.1) (F.f j.2) =
    (pullback.snd p ((E.inter F).toPullback k) ≫ pullback.fst (E.p₁ k.1 ≫ E.f i.1) (F.p₁ k.2 ≫ F.f i.2)) ≫ E.p₂ k.1
Module: Mathlib.CategoryTheory.Sites.Equivalence

Goal state before:
pp: case mp
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
K : GrothendieckTopology D
e : C ≌ D
inst✝¹ : e.functor.IsCocontinuous J K
inst✝ : e.inverse.IsCocontinuous K J
X : C
S : Sieve X
⊢ Sieve.functorPushforward e.functor S ∈ K (e.functor.obj X) → S ∈ J X

pp: case mpr
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
K : GrothendieckTopology D
e : C ≌ D
inst✝¹ : e.functor.IsCocontinuous J K
inst✝ : e.inverse.IsCocontinuous K J
X : C
S : Sieve X
⊢ S ∈ J X → Sieve.functorPushforward e.functor S ∈ K (e.functor.obj X)

Tactic:
· intro H
      refine J.superset_covering ?_ (e.functor.cover_lift J K H)
      rw [(Sieve.fullyFaithfulFunctorGaloisCoinsertion e.functor X).u_l_eq S]

Goal state after:
case mpr
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
K : GrothendieckTopology D
e : C ≌ D
inst✝¹ : e.functor.IsCocontinuous J K
inst✝ : e.inverse.IsCocontinuous K J
X : C
S : Sieve X
⊢ S ∈ J X → Sieve.functorPushforward e.functor S ∈ K (e.functor.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
J : GrothendieckTopology C
S : C
E : J.OneHypercover S
F : Sheaf J A
⊢ ∀ (E_1 : Multifork (E.multicospanIndex F.obj)) (m : E_1.pt ⟶ (E.multifork F.obj).pt),
    (∀ (i : E.multicospanShape.L), m ≫ (E.multifork F.obj).ι i = E_1.ι i) → m = multiforkLift E_1

Tactic:
intro c

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
J : GrothendieckTopology C
S : C
E : J.OneHypercover S
F : Sheaf J A
c : Multifork (E.multicospanIndex F.obj)
⊢ ∀ (m : c.pt ⟶ (E.multifork F.obj).pt),
    (∀ (i : E.multicospanShape.L), m ≫ (E.multifork F.obj).ι i = c.ι i) → m = multiforkLift c
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
⊢ Simple X

Tactic:
constructor; intro Y f hf; constructor
  · intro i
    rw [Subobject.isIso_iff_mk_eq_top] at i
    intro w
    rw [← Subobject.mk_eq_bot_iff_zero] at w
    exact IsSimpleOrder.bot_ne_top (w.symm.trans i)
  · intro i
    rcases IsSimpleOrder.eq_bot_or_eq_top (Subobject.mk f) with (h | h)
    · rw [Subobject.mk_eq_bot_iff_zero] at h
      exact False.elim (i h)
    · exact (Subobject.isIso_iff_mk_eq_top _).mpr 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 G H : C ⥤ D
T : Sheaf J RingCat
S : Sheaf K RingCat
inst✝² : F.IsContinuous J K
inst✝¹ : G.IsContinuous J K
inst✝ : H.IsContinuous J K
φ : T ⟶ (G.sheafPushforwardContinuous RingCat J K).obj S
α : F ⟶ G
X : SheafOfModules S
U V : Cᵒᵖ
i : U ⟶ V
x : ↑(((pushforward φ).obj X).val.obj U)
⊢ (ConcreteCategory.hom (X.val.presheaf.map (G.map i.unop).op ≫ X.val.presheaf.map (α.app (Opposite.unop V)).op)) x =
    (ConcreteCategory.hom (X.val.presheaf.map (α.app (Opposite.unop U)).op ≫ X.val.presheaf.map (F.map i.unop).op)) x

Tactic:
simp only [← CategoryTheory.Functor.map_comp, ← op_comp, α.naturality]

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 G H : C ⥤ D
T : Sheaf J RingCat
S : Sheaf K RingCat
inst✝² : F.IsContinuous J K
inst✝¹ : G.IsContinuous J K
inst✝ : H.IsContinuous J K
φ : T ⟶ (G.sheafPushforwardContinuous RingCat J K).obj S
α : F ⟶ G
X Y : SheafOfModules S
f : X ⟶ Y
⊢ (pushforward φ).map f ≫
      {
        val :=
          {
            app := fun U ↦
              (ModuleCat.restrictScalars (RingCat.Hom.hom (φ.hom.app U))).map (Y.val.map (α.app (Opposite.unop U)).op),
            naturality := ⋯ } } =
    {
        val :=
          {
            app := fun U ↦
              (ModuleCat.restrictScalars (RingCat.Hom.hom (φ.hom.app U))).map (X.val.map (α.app (Opposite.unop U)).op),
            naturality := ⋯ } } ≫
      (pushforward (φ ≫ (sheafPushforwardContinuousNatTrans α RingCat J K).app S)).map f

Tactic:
ext U x

Goal state after:
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 G H : C ⥤ D
T : Sheaf J RingCat
S : Sheaf K RingCat
inst✝² : F.IsContinuous J K
inst✝¹ : G.IsContinuous J K
inst✝ : H.IsContinuous J K
φ : T ⟶ (G.sheafPushforwardContinuous RingCat J K).obj S
α : F ⟶ G
X Y : SheafOfModules S
f : X ⟶ Y
U : Cᵒᵖ
x : ↑(((pushforward φ).obj X).val.obj U)
⊢ (ModuleCat.Hom.hom
        (((pushforward φ).map f ≫
                {
                  val :=
                    {
                      app := fun U ↦
                        (ModuleCat.restrictScalars (RingCat.Hom.hom (φ.hom.app U))).map
                          (Y.val.map (α.app (Opposite.unop U)).op),
                      naturality := ⋯ } }).val.app
          U))
      x =
    (ModuleCat.Hom.hom
        (({
                  val :=
                    {
                      app := fun U ↦
                        (ModuleCat.restrictScalars (RingCat.Hom.hom (φ.hom.app U))).map
                          (X.val.map (α.app (Opposite.unop U)).op),
                      naturality := ⋯ } } ≫
                (pushforward (φ ≫ (sheafPushforwardContinuousNatTrans α RingCat J K).app S)).map f).val.app
          U))
      x
Module: Mathlib.Topology.Sheaves.SheafCondition.Sites

Goal state before:
pp: X : TopCat
ι : Type v
U : ι → Opens ↑X
x : ↑X
hx : x ∈ iSup U
i : ι
hxi : x ∈ U i
⊢ ∃ U_1 f, (Sieve.generate (presieveOfCovering U)).arrows f ∧ x ∈ U_1

Tactic:
exact ⟨U i, Opens.leSupr U i, ⟨U i, 𝟙 _, Opens.leSupr U i, ⟨i, rfl⟩, Category.id_comp _⟩, hxi⟩

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous

Goal state before:
pp: case refine_1.refine_1
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
X : Cᵒᵖ
hX : IsInitial X
hX' : IsInitial (F.op.obj X)
M : SheafOfModules R
U : Cᵒᵖ
⊢ (RingCat.Hom.hom (R.obj.map (hX'.to (Opposite.op (F.obj (Opposite.unop U)))))).comp (RingCat.Hom.hom (φ.hom.app X)) =
    (RingCat.Hom.hom (R.obj.map (F.map (hX.to U).unop).op)).comp (RingCat.Hom.hom (φ.hom.app X))

Tactic:
rw [hX'.hom_ext (hX'.to (Opposite.op (F.obj (Opposite.unop U)))) _]

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
s t : ToType (F.obj.obj (op (iSup U)))
h :
  ∀ (i : ι), (ConcreteCategory.hom (F.obj.map (leSupr U i).op)) s = (ConcreteCategory.hom (F.obj.map (leSupr U i).op)) t
sf : (i : ι) → ToType (F.obj.obj (op (U i))) := fun i ↦ (ConcreteCategory.hom (F.obj.map (leSupr U i).op)) s
i j : ι
⊢ (ConcreteCategory.hom (F.obj.map ((U i).infLELeft (U j)).op)) (sf i) =
    (ConcreteCategory.hom (F.obj.map ((U i).infLERight (U j)).op)) (sf j)

Tactic:
simp_rw [sf, ← ConcreteCategory.comp_apply, ← F.1.map_comp]

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
s t : ToType (F.obj.obj (op (iSup U)))
h :
  ∀ (i : ι), (ConcreteCategory.hom (F.obj.map (leSupr U i).op)) s = (ConcreteCategory.hom (F.obj.map (leSupr U i).op)) t
sf : (i : ι) → ToType (F.obj.obj (op (U i))) := fun i ↦ (ConcreteCategory.hom (F.obj.map (leSupr U i).op)) s
i j : ι
⊢ (ConcreteCategory.hom (F.obj.map ((leSupr U i).op ≫ ((U i).infLELeft (U j)).op))) s =
    (ConcreteCategory.hom (F.obj.map ((leSupr U j).op ≫ ((U i).infLERight (U j)).op))) s
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent

Goal state before:
pp: C✝ : Type u₁
inst✝⁶ : Category.{v₁, u₁} C✝
J✝ : GrothendieckTopology C✝
R✝ : Sheaf J✝ RingCat
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : HasBinaryProducts C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝³ : HasSheafify J AddCommGrpCat
inst✝² : J.WEqualsLocallyBijective AddCommGrpCat
inst✝¹ : ∀ (X : C), HasSheafify (J.over X) AddCommGrpCat
inst✝ : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat
M : SheafOfModules R
P : M.Presentation
x Y✝ : C
f : Y✝ ⟶ x
⊢ (Sieve.ofObjects id x).arrows f ↔ ⊤.arrows f

Tactic:
simp [Sieve.top_apply]

Goal state after: