mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ R : Cᵒᵖ ⥤ RingCat
α : R₀ ⟶ R
inst✝¹ : Presheaf.IsLocallyInjective J α
M₀ : PresheafOfModules R₀
A : Cᵒᵖ ⥤ AddCommGrpCat
φ : M₀.presheaf ⟶ A
inst✝ : Presheaf.IsLocallyInjective J φ
hA : Presheaf.IsSeparated J A
X : C
r : ↑(R.obj (Opposite.op X))
m : ↑(A.obj (Opposite.op X))
P : Presieve X
r₀ : FamilyOfElements (R₀ ⋙ forget RingCat) P
m₀ : FamilyOfElements (M₀.presheaf ⋙ forget Ab) P
hr₀ : (r₀.map (whiskerRight α (forget RingCat))).IsAmalgamation r
hm₀ : (m₀.map (whiskerRight φ (forget Ab))).IsAmalgamation m
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : P f₁
h₂ : P f₂
fac : g₁ ≫ f₁ = g₂ ≫ f₂
a₁ : (R₀ ⋙ forget RingCat).obj (Opposite.op Y₁) := r₀ f₁ h₁
b₁ : (M₀.presheaf ⋙ forget Ab).obj (Opposite.op Y₁) := m₀ f₁ h₁
a₂ : (R₀ ⋙ forget RingCat).obj (Opposite.op Y₂) := r₀ f₂ h₂
⊢ (ConcreteCategory.hom ((A ⋙ forget Ab).map g₁.op)) ((r₀.smul m₀).map (whiskerRight φ (forget Ab)) f₁ h₁) =
    (ConcreteCategory.hom ((A ⋙ forget Ab).map g₂.op)) ((r₀.smul m₀).map (whiskerRight φ (forget Ab)) f₂ h₂)

Tactic:
let b₂ := m₀ f₂ h₂

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ R : Cᵒᵖ ⥤ RingCat
α : R₀ ⟶ R
inst✝¹ : Presheaf.IsLocallyInjective J α
M₀ : PresheafOfModules R₀
A : Cᵒᵖ ⥤ AddCommGrpCat
φ : M₀.presheaf ⟶ A
inst✝ : Presheaf.IsLocallyInjective J φ
hA : Presheaf.IsSeparated J A
X : C
r : ↑(R.obj (Opposite.op X))
m : ↑(A.obj (Opposite.op X))
P : Presieve X
r₀ : FamilyOfElements (R₀ ⋙ forget RingCat) P
m₀ : FamilyOfElements (M₀.presheaf ⋙ forget Ab) P
hr₀ : (r₀.map (whiskerRight α (forget RingCat))).IsAmalgamation r
hm₀ : (m₀.map (whiskerRight φ (forget Ab))).IsAmalgamation m
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : P f₁
h₂ : P f₂
fac : g₁ ≫ f₁ = g₂ ≫ f₂
a₁ : (R₀ ⋙ forget RingCat).obj (Opposite.op Y₁) := r₀ f₁ h₁
b₁ : (M₀.presheaf ⋙ forget Ab).obj (Opposite.op Y₁) := m₀ f₁ h₁
a₂ : (R₀ ⋙ forget RingCat).obj (Opposite.op Y₂) := r₀ f₂ h₂
b₂ : (M₀.presheaf ⋙ forget Ab).obj (Opposite.op Y₂) := m₀ f₂ h₂
⊢ (ConcreteCategory.hom ((A ⋙ forget Ab).map g₁.op)) ((r₀.smul m₀).map (whiskerRight φ (forget Ab)) f₁ h₁) =
    (ConcreteCategory.hom ((A ⋙ forget Ab).map g₂.op)) ((r₀.smul m₀).map (whiskerRight φ (forget Ab)) f₂ h₂)
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
hX : IsZero X
this : HasExt C := HasExt.standard C
⊢ ∀ (i : ℕ), 0 ≤ i → ∀ ⦃Y : C⦄ (e : Ext X Y i), e = 0

Tactic:
intro i hi Y e

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
hX : IsZero X
this : HasExt C := HasExt.standard C
i : ℕ
hi : 0 ≤ i
Y : C
e : Ext X Y i
⊢ e = 0
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
n m : ℕ
h : n ≤ m
inst✝ : HasProjectiveDimensionLT X n
this : HasExt C := HasExt.standard C
⊢ ∀ (i : ℕ), m ≤ i → ∀ ⦃Y : C⦄ (e : Ext X Y i), e = 0

Tactic:
intro i hi Y e

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
n m : ℕ
h : n ≤ m
inst✝ : HasProjectiveDimensionLT X n
this : HasExt C := HasExt.standard C
i : ℕ
hi : m ≤ i
Y : C
e : Ext X Y i
⊢ e = 0
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
n : ℕ
inst✝ : Projective X
this : HasExt C := HasExt.standard C
⊢ ∀ (i : ℕ), 1 ≤ i → ∀ ⦃Y : C⦄ (e : Ext X Y i), e = 0

Tactic:
intro i hi Y e

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
n : ℕ
inst✝ : Projective X
this : HasExt C := HasExt.standard C
i : ℕ
hi : 1 ≤ i
Y : C
e : Ext X Y i
⊢ e = 0
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: case diagram
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ k✝ : J
f : j✝ ⟶ k✝
g : BiconeHom J (Bicone.diagram k✝) Z✝
⊢ BiconeHom J (Bicone.diagram j✝) Z✝

Tactic:
· rcases g with (_ | _ | _ | _ | g)
      exact BiconeHom.diagram (f ≫ g)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: J : Type u₁
inst✝ : Category.{v₁, u₁} J
W✝ X✝ Y✝ Z✝ : Bicone J
f : W✝ ⟶ X✝
g : X✝ ⟶ Y✝
h : Y✝ ⟶ Z✝
⊢ (f ≫ g) ≫ h = f ≫ g ≫ h

Tactic:
by cases f <;> cases g <;> cases h <;> simp

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

Goal state before:
pp: case a
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X Y : C
f : Y ⟶ X
S : Sieve X
Z : C
g : Z ⟶ Y
⊢ (Sieve.pullback f (J₁.close S)).arrows g → (J₁.close (Sieve.pullback f S)).arrows g

Tactic:
hg

Goal state after:
case a
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X Y : C
f : Y ⟶ X
S : Sieve X
Z : C
g : Z ⟶ Y
hg : (Sieve.pullback f (J₁.close S)).arrows g
⊢ (J₁.close (Sieve.pullback f S)).arrows g
Module: Mathlib.CategoryTheory.Sites.Closed

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
⊢ S ∈ J₁ X → J₁.close S = ⊤

Tactic:
intro hS

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
⊢ J₁.close S = ⊤
Module: Mathlib.CategoryTheory.Sites.Closed

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows
M : (Functor.sieves C).obj (Opposite.op X)
hM : M ∈ (Functor.closedSieves J₁).obj (Opposite.op X)
N : (Functor.sieves C).obj (Opposite.op X)
hN : N ∈ (Functor.closedSieves J₁).obj (Opposite.op X)
hM₂ : x.IsAmalgamation ⟨M, hM⟩
hN₂ : x.IsAmalgamation ⟨N, hN⟩
⊢ ⟨M, hM⟩ = ⟨N, hN⟩

Tactic:
dsimp at S M N ⊢

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
J₁ : GrothendieckTopology C
X : C
S : Sieve X
hS : S ∈ J₁ X
x : Presieve.FamilyOfElements (Functor.closedSieves J₁).toFunctor S.arrows
M : Sieve X
hM : M ∈ (Functor.closedSieves J₁).obj (Opposite.op X)
N : Sieve X
hN : N ∈ (Functor.closedSieves J₁).obj (Opposite.op X)
hM₂ : x.IsAmalgamation ⟨M, hM⟩
hN₂ : x.IsAmalgamation ⟨N, hN⟩
⊢ ⟨M, hM⟩ = ⟨N, hN⟩
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
X : C
S T : Sieve X
h : S ≤ T
hS : K.Saturate X S
Y : C
g : Y ⟶ X
⊢ S.arrows g → K.Saturate Y (Sieve.pullback g T)

Tactic:
hg

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
X : C
S T : Sieve X
h : S ≤ T
hS : K.Saturate X S
Y : C
g : Y ⟶ X
hg : S.arrows g
⊢ K.Saturate Y (Sieve.pullback g T)
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: case hf
C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
X : C
S T : Sieve X
h : S ≤ T
hS : K.Saturate X S
Y : C
g : Y ⟶ X
hg : S.arrows g
⊢ S.arrows g

Tactic:
· assumption

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

Goal state before:
pp: case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
X : C
S : Sieve X
⊢ K.Saturate X S → K.Saturate X S

Tactic:
intro hS

Goal state after:
case mp
C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
X : C
S : Sieve X
hS : K.Saturate X S
⊢ K.Saturate X S
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
X : C
S : Sieve X
⊢ K.Saturate X S → K.Saturate X S

Tactic:
intro hS

Goal state after:
case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
K : Coverage C
X : C
S : Sieve X
hS : K.Saturate X S
⊢ K.Saturate X S
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: case mpr.H
C : Type u_2
inst✝ : Category.{v_1, u_2} C
K : Coverage C
P : Cᵒᵖ ⥤ Type u_1
H : ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R
X Y : C
f : Y ⟶ X
S : Presieve X
hS : S ∈ K.coverings X
T : Presieve Y
hT1 : T ∈ K.coverings Y
hT2 : T.FactorsThruAlong S f
Z : C
g : Z ⟶ Y
⊢ T g → ∃ W i e, (Sieve.pullback f (Sieve.generate S)).arrows e ∧ i ≫ e = g

Tactic:
hg

Goal state after:
case mpr.H
C : Type u_2
inst✝ : Category.{v_1, u_2} C
K : Coverage C
P : Cᵒᵖ ⥤ Type u_1
H : ∀ {X : C}, ∀ R ∈ K.coverings X, IsSheafFor P R
X Y : C
f : Y ⟶ X
S : Presieve X
hS : S ∈ K.coverings X
T : Presieve Y
hT1 : T ∈ K.coverings Y
hT2 : T.FactorsThruAlong S f
Z : C
g : Z ⟶ Y
hg : T g
⊢ ∃ W i e, (Sieve.pullback f (Sieve.generate S)).arrows e ∧ i ≫ e = g
Module: Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck

Goal state before:
pp: case refine_2
C : Type u_2
inst✝⁴ : Category.{u_1, u_2} C
J : Precoverage C
inst✝³ : J.IsStableUnderComposition
inst✝² : J.IsStableUnderBaseChange
inst✝¹ : J.HasPullbacks
inst✝ : J.HasIsos
X : C
S : Sieve X
x✝ : ∃ R ∈ J.coverings X, R ≤ S.arrows
R : Presieve X
hR : R ∈ J.coverings X
hle : Sieve.generate R ≤ S
⊢ S ∈ J.toGrothendieck X

Tactic:
apply GrothendieckTopology.superset_covering _ hle

Goal state after:
case refine_2
C : Type u_2
inst✝⁴ : Category.{u_1, u_2} C
J : Precoverage C
inst✝³ : J.IsStableUnderComposition
inst✝² : J.IsStableUnderBaseChange
inst✝¹ : J.HasPullbacks
inst✝ : J.HasIsos
X : C
S : Sieve X
x✝ : ∃ R ∈ J.coverings X, R ≤ S.arrows
R : Presieve X
hR : R ∈ J.coverings X
hle : Sieve.generate R ≤ S
⊢ Sieve.generate R ∈ J.toGrothendieck X
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

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

Tactic:
refine ⟨k.1, pullback.snd _ _ ≫ pullback.fst _ _, ?_, ?_⟩

Goal state after:
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

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.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
F : Sheaf J A
X Y Z : C
f : G.obj X ⟶ G.obj Y
p : Z ⟶ X
g : Z ⟶ Y
fac : G.map p ≫ f = G.map g
W₀ : C
a : W₀ ⟶ Z
ha : (Sieve.pullback p (G.imageSieve f)).arrows a
⊢ mapPreimage K G F f ≫ F.obj.map (a ≫ p).op = F.obj.map g.op ≫ F.obj.map a.op

Tactic:
mapPreimage

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
F : Sheaf J A
X Y Z : C
f : G.obj X ⟶ G.obj Y
p : Z ⟶ X
g : Z ⟶ Y
fac : G.map p ≫ f = G.map g
W₀ : C
a : W₀ ⟶ Z
ha : (Sieve.pullback p (G.imageSieve f)).arrows a
⊢ ⋯.amalgamate ⟨G.imageSieve f, ⋯⟩
        (fun x ↦
          match x with
          | { Y := W₀, f := a, hf := ha } => F.obj.map (Exists.choose ha).op)
        ⋯ ≫
      F.obj.map (a ≫ p).op =
    F.obj.map g.op ≫ F.obj.map a.op
Module: Mathlib.CategoryTheory.Sites.InducedTopology

Goal state before:
pp: case refine_2
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
K : GrothendieckTopology D
J : GrothendieckTopology C
h : F.IsContinuous J K
⊢ J ≤ F.inducedTopology K

Tactic:
apply Sheaf.le_finestTopology

Goal state after:
case refine_2
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
K : GrothendieckTopology D
J : GrothendieckTopology C
h : F.IsContinuous J K
⊢ ∀ P ∈ Set.range fun G ↦ F.op ⋙ G.obj, Presieve.IsSheaf J P
Module: Mathlib.CategoryTheory.Sites.InducedTopology

Goal state before:
pp: case refine_1
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
K : GrothendieckTopology D
inst✝ : LocallySmall.{max u₁ v₁ u₂ v₂, v₁, u₁} C
X : C
S : Sieve X
G : (Cᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)) ⥤ Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
adj : G ⊣ (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))).obj F.op
⊢ S ∈ (F.inducedTopology K) X →
    ∀ ⦃Y : C⦄ (f : Y ⟶ X), K.W (G.map (Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂, v₁, u₁} (Sieve.pullback f S)).ι)

Tactic:
intro hS

Goal state after:
case refine_1
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
K : GrothendieckTopology D
inst✝ : LocallySmall.{max u₁ v₁ u₂ v₂, v₁, u₁} C
X : C
S : Sieve X
G : (Cᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)) ⥤ Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)
adj : G ⊣ (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))).obj F.op
hS : S ∈ (F.inducedTopology K) X
⊢ ∀ ⦃Y : C⦄ (f : Y ⟶ X), K.W (G.map (Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂, v₁, u₁} (Sieve.pullback f S)).ι)
Module: Mathlib.CategoryTheory.Sites.InducedTopology

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
K : GrothendieckTopology D
X : C
S : Sieve X
hS : Sieve.functorPushforward F S ∈ K (F.obj X)
⊢ Sieve.generate S.arrows ∈ (F.restrictedTopology K) X

Tactic:
apply Precoverage.generate_mem_toGrothendieck

Goal state after:
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
K : GrothendieckTopology D
X : C
S : Sieve X
hS : Sieve.functorPushforward F S ∈ K (F.obj X)
⊢ S.arrows ∈ (Precoverage.comap F K.toPrecoverage).coverings X
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology

Goal state before:
pp: case mp
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
D : Type u_2
inst✝³ : Category.{v_2, u_2} D
G : C ⥤ D
K : GrothendieckTopology D
inst✝² : G.LocallyCoverDense K
inst✝¹ : G.Full
inst✝ : G.Faithful
X : C
S : Sieve X
⊢ Sieve.functorPushforward G S ∈ K (G.obj X) → ∃ T, Sieve.functorPullback G ↑T = S

Tactic:
intro hS

Goal state after:
case mp
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
D : Type u_2
inst✝³ : Category.{v_2, u_2} D
G : C ⥤ D
K : GrothendieckTopology D
inst✝² : G.LocallyCoverDense K
inst✝¹ : G.Full
inst✝ : G.Faithful
X : C
S : Sieve X
hS : Sieve.functorPushforward G S ∈ K (G.obj X)
⊢ ∃ T, Sieve.functorPullback G ↑T = S
Module: Mathlib.CategoryTheory.Sites.PreservesLocallyBijective

Goal state before:
pp: C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : Category.{v_3, u_3} A
J : GrothendieckTopology C
K : GrothendieckTopology D
H : C ⥤ D
F G : Dᵒᵖ ⥤ A
f : F ⟶ G
FA : A → A → Type u_4
CA : A → Type u_5
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
hH : CoverPreserving J K H
inst✝¹ : H.IsCoverDense K
inst✝ : IsLocallyInjective J (H.op.whiskerLeft f)
X : Dᵒᵖ
a b : ToType (F.obj X)
h : (ConcreteCategory.hom (f.app X)) a = (ConcreteCategory.hom (f.app X)) b
Y : D
g : Y ⟶ Opposite.unop X
Z : C
lift : Y ⟶ H.obj Z
m : H.obj Z ⟶ Opposite.unop X
fac : lift ≫ m = g
⊢ Sieve.pullback g (equalizerSieve a b) ∈ K Y

Tactic:
rw [← fac, Sieve.pullback_comp]

Goal state after:
C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : Category.{v_3, u_3} A
J : GrothendieckTopology C
K : GrothendieckTopology D
H : C ⥤ D
F G : Dᵒᵖ ⥤ A
f : F ⟶ G
FA : A → A → Type u_4
CA : A → Type u_5
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
hH : CoverPreserving J K H
inst✝¹ : H.IsCoverDense K
inst✝ : IsLocallyInjective J (H.op.whiskerLeft f)
X : Dᵒᵖ
a b : ToType (F.obj X)
h : (ConcreteCategory.hom (f.app X)) a = (ConcreteCategory.hom (f.app X)) b
Y : D
g : Y ⟶ Opposite.unop X
Z : C
lift : Y ⟶ H.obj Z
m : H.obj Z ⟶ Opposite.unop X
fac : lift ≫ m = g
⊢ Sieve.pullback lift (Sieve.pullback m (equalizerSieve a b)) ∈ K Y
Module: Mathlib.CategoryTheory.Sites.PreservesLocallyBijective

Goal state before:
pp: C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : Category.{v_3, u_3} A
J : GrothendieckTopology C
K : GrothendieckTopology D
H : C ⥤ D
F G : Dᵒᵖ ⥤ A
f : F ⟶ G
FA : A → A → Type u_4
CA : A → Type u_5
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
hH : CoverPreserving J K H
inst✝¹ : H.IsCoverDense K
inst✝ : IsLocallySurjective J (H.op.whiskerLeft f)
X : D
a : ToType (G.obj (Opposite.op X))
Y : D
g : Y ⟶ X
Z : C
lift : Y ⟶ H.obj Z
m : H.obj Z ⟶ X
fac : lift ≫ m = g
⊢ Sieve.pullback g (imageSieve f a) ∈ K Y

Tactic:
rw [← fac, Sieve.pullback_comp]

Goal state after:
C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : Category.{v_3, u_3} A
J : GrothendieckTopology C
K : GrothendieckTopology D
H : C ⥤ D
F G : Dᵒᵖ ⥤ A
f : F ⟶ G
FA : A → A → Type u_4
CA : A → Type u_5
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
hH : CoverPreserving J K H
inst✝¹ : H.IsCoverDense K
inst✝ : IsLocallySurjective J (H.op.whiskerLeft f)
X : D
a : ToType (G.obj (Opposite.op X))
Y : D
g : Y ⟶ X
Z : C
lift : Y ⟶ H.obj Z
m : H.obj Z ⟶ X
fac : lift ≫ m = g
⊢ Sieve.pullback lift (Sieve.pullback m (imageSieve f a)) ∈ K Y
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₀
⊢ e.inv.h₀ i ≫ e.hom.h₀ (e.inv.s₀ i) = eqToHom ⋯

Tactic:
obtain ⟨hs, hh, _⟩ := Hom.ext'_iff.mp e.inv_hom_id
  simpa using hh i

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

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : C ⥤ D
X : C
U : Over X
S : Sieve ((Over.post F).obj U)
Z : C
g : Z ⟶ U.left
⊢ (functorPullback F ((overEquiv ((Over.post F).obj U)) S)).arrows g →
    ((overEquiv U) (functorPullback (Over.post F) S)).arrows g

Tactic:
hg

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : C ⥤ D
X : C
U : Over X
S : Sieve ((Over.post F).obj U)
Z : C
g : Z ⟶ U.left
hg : (functorPullback F ((overEquiv ((Over.post F).obj U)) S)).arrows g
⊢ ((overEquiv U) (functorPullback (Over.post F) S)).arrows g
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
K : Precoverage C
inst✝¹ : K.HasPullbacks
inst✝ : K.IsStableUnderBaseChange
X Y : C
right : Discrete PUnit.{1}
s : Y ⟶ X
R : Sieve { left := Y, right := right, hom := s }
hR : R ∈ (K.toGrothendieck.over X) { left := Y, right := right, hom := s }
⊢ R ∈ (Precoverage.comap (Over.forget X) K).toGrothendieck { left := Y, right := right, hom := s }

Tactic:
obtain ⟨(R : Sieve Y), rfl⟩ := (Sieve.overEquiv _).symm.surjective R

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
K : Precoverage C
inst✝¹ : K.HasPullbacks
inst✝ : K.IsStableUnderBaseChange
X Y : C
right : Discrete PUnit.{1}
s : Y ⟶ X
R : Sieve Y
hR :
  (Sieve.overEquiv { left := Y, right := right, hom := s }).symm R ∈
    (K.toGrothendieck.over X) { left := Y, right := right, hom := s }
⊢ (Sieve.overEquiv { left := Y, right := right, hom := s }).symm R ∈
    (Precoverage.comap (Over.forget X) K).toGrothendieck { left := Y, right := right, hom := s }
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: case mpr
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
Y : C
f : Y ⟶ X
hf : Mono f
⊢ f ≠ 0 → IsIso f

Tactic:
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 : 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
X : SheafOfModules R
⊢ (pushforward φ).map
        (((pushforwardId R).inv ≫
              pushforwardNatTrans (𝟙 (((𝟭 D).sheafPushforwardContinuous RingCat K K).obj R)) adj.counit ≫
                (pushforwardCongr ⋯).hom ≫ (pushforwardComp ψ φ).inv).app
          X) ≫
      ((pushforwardComp φ ψ).hom ≫
            pushforwardNatTrans (φ ≫ (F.sheafPushforwardContinuous RingCat J K).map ψ) adj.unit ≫
              (pushforwardCongr ⋯).hom ≫ (pushforwardId S).hom).app
        ((pushforward φ).obj X) =
    𝟙 ((pushforward φ).obj X)

Tactic:
by
    ext U x
    change (X.val.presheaf.map (adj.counit.app (F.obj U.unop)).op ≫
      X.val.presheaf.map (F.map (adj.unit.app U.unop)).op) _ = _
    dsimp only [id_obj]
    rw [← Functor.map_comp, ← op_comp, adj.left_triangle_components]
    simp

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

Goal state before:
pp: X : TopCat
Y : Opens ↑X
R : Presieve Y
Z : Opens ↑X
f : Z ⟶ Y
x✝ : presieveOfCoveringAux (coveringOfPresieve Y R) Y f
f' : Z ⟶ Y
h : R f'
⊢ R f

Tactic:
rwa [Subsingleton.elim f f']

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

Goal state before:
pp: case hF₂
X Y : TopCat
f : X ⟶ Y
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
⊢ CoverPreserving (Opens.grothendieckTopology ↑X) (Opens.grothendieckTopology ↑Y) h.functor

Tactic:
· exact h.isOpenMap.coverPreserving

Goal state after: