mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Localization.Bousfield

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
P : ObjectProperty C
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hg : P.isLocal g
hfg : P.isLocal (f ≫ g)
Z : C
hZ : P Z
⊢ Function.Bijective fun g ↦ f ≫ g

Tactic:
← Function.Bijective.of_comp_iff _ (hg Z hZ)

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
P : ObjectProperty C
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hg : P.isLocal g
hfg : P.isLocal (f ≫ g)
Z : C
hZ : P Z
⊢ Function.Bijective ((fun g ↦ f ≫ g) ∘ fun g_1 ↦ g ≫ g_1)
Module: Mathlib.CategoryTheory.Localization.Bousfield

Goal state before:
pp: case mpr.left
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
Y Z : C
g : Y ⟶ Z
hg : P.isColocal g
X X' : C
hX' : P X'
e : X ≅ X'
f₁ f₂ : X ⟶ Y
eq : (fun f ↦ f ≫ g) f₁ = (fun f ↦ f ≫ g) f₂
⊢ f₁ = f₂

Tactic:
rw [← cancel_epi e.inv]

Goal state after:
case mpr.left
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
Y Z : C
g : Y ⟶ Z
hg : P.isColocal g
X X' : C
hX' : P X'
e : X ≅ X'
f₁ f₂ : X ⟶ Y
eq : (fun f ↦ f ≫ g) f₁ = (fun f ↦ f ≫ g) f₂
⊢ e.inv ≫ f₁ = e.inv ≫ f₂
Module: Mathlib.CategoryTheory.Sites.LocallyInjective

Goal state before:
pp: case mp
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst✝¹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝ : ConcreteCategory D FD
F : Cᵒᵖ ⥤ D
X : Cᵒᵖ
x y : ToType (F.obj X)
⊢ equalizerSieve x y = ⊤ → x = y

Tactic:
intro h

Goal state after:
case mp
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst✝¹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝ : ConcreteCategory D FD
F : Cᵒᵖ ⥤ D
X : Cᵒᵖ
x y : ToType (F.obj X)
h : equalizerSieve x y = ⊤
⊢ x = y
Module: Mathlib.CategoryTheory.Sites.PreservesSheafification

Goal state before:
pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u_1
B : Type u_2
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Category.{v_2, u_2} B
F : A ⥤ B
G₁ : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : (Cᵒᵖ ⥤ B) ⥤ Sheaf J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
⊢ (∀ (P : Cᵒᵖ ⥤ A), J.W (whiskerRight (adj₁.unit.app P) F)) → J.PreservesSheafification F

Tactic:
intro h

Goal state after:
case mpr
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u_1
B : Type u_2
inst✝¹ : Category.{v_1, u_1} A
inst✝ : Category.{v_2, u_2} B
F : A ⥤ B
G₁ : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A
adj₁ : G₁ ⊣ sheafToPresheaf J A
G₂ : (Cᵒᵖ ⥤ B) ⥤ Sheaf J B
adj₂ : G₂ ⊣ sheafToPresheaf J B
h : ∀ (P : Cᵒᵖ ⥤ A), J.W (whiskerRight (adj₁.unit.app P) F)
⊢ J.PreservesSheafification F
Module: Mathlib.CategoryTheory.Sites.LocallyInjective

Goal state before:
pp: case mp
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst✝¹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝ : ConcreteCategory D FD
J : GrothendieckTopology C
F₁ F₂ : Cᵒᵖ ⥤ D
φ : F₁ ⟶ F₂
hsep : Presieve.IsSeparated J (F₁ ⋙ forget D)
⊢ IsLocallyInjective J φ → ∀ (X : Cᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom (φ.app X))

pp: case mpr
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst✝¹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝ : ConcreteCategory D FD
J : GrothendieckTopology C
F₁ F₂ : Cᵒᵖ ⥤ D
φ : F₁ ⟶ F₂
hsep : Presieve.IsSeparated J (F₁ ⋙ forget D)
⊢ (∀ (X : Cᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom (φ.app X))) → IsLocallyInjective J φ

Tactic:
· intro _ X x y h
    exact (hsep _ (equalizerSieve_mem J φ x y h)).ext (fun _ _ hf => hf)

Goal state after:
case mpr
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst✝¹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝ : ConcreteCategory D FD
J : GrothendieckTopology C
F₁ F₂ : Cᵒᵖ ⥤ D
φ : F₁ ⟶ F₂
hsep : Presieve.IsSeparated J (F₁ ⋙ forget D)
⊢ (∀ (X : Cᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom (φ.app X))) → IsLocallyInjective J φ
Module: Mathlib.CategoryTheory.Sites.LocallySurjective

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝¹ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝ : ConcreteCategory A FA
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
⊢ IsLocallySurjective J f ↔ Subfunctor.sheafify J (Subfunctor.range (whiskerRight f (forget A))) = ⊤

Tactic:
simp only [Subfunctor.ext_iff, funext_iff, Set.ext_iff, Subfunctor.top_obj,
    Set.top_eq_univ, Set.mem_univ, iff_true]
  exact ⟨fun H _ => H.imageSieve_mem, fun H => ⟨H _⟩⟩

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁴ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
F₁ F₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst✝¹ : IsLocallySurjective J (f₁ ≫ f₂)
inst✝ : IsLocallyInjective J f₂
X : C
x : ToType (F₂.obj (op X))
S : Sieve X := imageSieve (f₁ ≫ f₂) ((ConcreteCategory.hom (f₂.app (op X))) x)
T : ⦃Y : C⦄ → (f : Y ⟶ X) → S.arrows f → Sieve Y :=
  fun Y f hf ↦
    equalizerSieve
      ((ConcreteCategory.hom (f₁.app (op Y))) (localPreimage (f₁ ≫ f₂) ((ConcreteCategory.hom (f₂.app (op X))) x) f hf))
      ((ConcreteCategory.hom (F₂.map f.op)) x)
Y Z : C
a : Y ⟶ Z
g : Z ⟶ unop (op X)
hg : S.arrows g
ha : (T g hg).arrows a
⊢ (ConcreteCategory.hom (f₁.app (op Y)))
      ((ConcreteCategory.hom (F₁.map a.op)) (localPreimage (f₁ ≫ f₂) ((ConcreteCategory.hom (f₂.app (op X))) x) g hg)) =
    (ConcreteCategory.hom (F₂.map (a ≫ g).op)) x

Tactic:
by simpa using! ha

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Dimension

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
h : HasProjectiveDimensionLT X 0
⊢ ⊥ < ↑0

Tactic:
by decide

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.SigmaConst

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
R : C
α : Type u_1
β : Type u_2
f : α → β
inst✝² : HasCoproduct fun x ↦ R
inst✝¹ : HasCoproduct fun x ↦ R
inst✝ : HasCoproduct fun x ↦ R
a : α
⊢ Sigma.ι (fun x ↦ R) (f a) ≫ Cofork.π (sigmaConstCokernelCofork R f) = 0

Tactic:
by
  dsimp [sigmaConstCokernelCofork]
  rw [Sigma.ι_desc]
  exact dif_neg (by simp)

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

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

Tactic:
intro h

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

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
⊢ (∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P) → J₁ = J₂

Tactic:
intro h

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
J₁ J₂ : GrothendieckTopology C
h : ∀ (P : Cᵒᵖ ⥤ Type (max v u)), Presieve.IsSheaf J₁ P ↔ Presieve.IsSheaf J₂ P
⊢ J₁ = J₂
Module: Mathlib.CategoryTheory.Sites.Coverage

Goal state before:
pp: case refine_2
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) ⋯)
hy : y.Compatible
left✝ : IsSeparatedFor P S
h2' : ∀ (x : FamilyOfElements P S), x.Compatible → ∃ t, x.IsAmalgamation t
z : P.obj (Opposite.op X)
hz : y.IsAmalgamation z
Y : C
g : Y ⟶ X
hg : T g
⊢ (ConcreteCategory.hom (P.map g.op)) z = x g hg

Tactic:
obtain ⟨R, hR1, hR2⟩ := h hg

Goal state after:
case refine_2
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) ⋯)
hy : y.Compatible
left✝ : IsSeparatedFor P S
h2' : ∀ (x : FamilyOfElements P S), x.Compatible → ∃ t, x.IsAmalgamation t
z : P.obj (Opposite.op X)
hz : y.IsAmalgamation z
Y : C
g : Y ⟶ X
hg : T g
R : Presieve Y
hR1 : IsSeparatedFor P R
hR2 : R.FactorsThruAlong S g
⊢ (ConcreteCategory.hom (P.map g.op)) z = x g hg
Module: Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
H : J.OneHypercoverFamily
P : Cᵒᵖ ⥤ A
hP : ∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (IsLimit (E.multifork P))
X : C
S : Sieve X
E : J.OneHypercover X
hE : H E
le : E.sieve₀ ≤ S
inst✝ : H.IsGenerating
F : Multifork (Cover.index ⟨S, ⋯⟩ P)
m : F.pt ⟶ (Cover.multifork ⟨S, ⋯⟩ P).pt
hm : ∀ (i : (Cover.shape ⟨S, ⋯⟩).L), m ≫ (Cover.multifork ⟨S, ⋯⟩ P).ι i = F.ι i
⊢ m = lift hP hE le F

Tactic:
apply hom_ext H P hP S (J.superset_covering le E.mem₀)
      intro Y f hf
      rw [fac _ _ _ _ _ hf]
      exact hm ⟨_, _, hf⟩

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

Goal state before:
pp: case refine_2.refine_1
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
X : C
E : PreOneHypercover X
F : C ⥤ D
i₁ i₂ : E.I₀
inst✝¹ : HasPullback (E.f i₁) (E.f i₂)
inst✝ : PreservesLimit (cospan (E.f i₁) (E.f i₂)) F
this : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
W : D
f : W ⟶ F.obj (pullback (E.f i₁) (E.f i₂))
Y : D
k : (E.map F).I₁ i₁ i₂
u : W ⟶ (E.map F).Y k
h :
  u ≫ (E.map F).toPullback k =
    f ≫ pullback.lift (F.map (pullback.fst (E.f i₁) (E.f i₂))) (F.map (pullback.snd (E.f i₁) (E.f i₂))) ⋯
⊢ (E.sieve₁' i₁ i₂).arrows (pullback.lift (E.p₁ k) (E.p₂ k) ⋯)

Tactic:
use E.Y k, 𝟙 _, pullback.lift (E.p₁ k) (E.p₂ k) (E.w _), ⟨k⟩

Goal state after:
case right
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
X : C
E : PreOneHypercover X
F : C ⥤ D
i₁ i₂ : E.I₀
inst✝¹ : HasPullback (E.f i₁) (E.f i₂)
inst✝ : PreservesLimit (cospan (E.f i₁) (E.f i₂)) F
this : HasPullback ((E.map F).f i₁) ((E.map F).f i₂)
W : D
f : W ⟶ F.obj (pullback (E.f i₁) (E.f i₂))
Y : D
k : (E.map F).I₁ i₁ i₂
u : W ⟶ (E.map F).Y k
h :
  u ≫ (E.map F).toPullback k =
    f ≫ pullback.lift (F.map (pullback.fst (E.f i₁) (E.f i₂))) (F.map (pullback.snd (E.f i₁) (E.f i₂))) ⋯
⊢ 𝟙 (E.Y k) ≫ pullback.lift (E.p₁ k) (E.p₂ k) ⋯ = pullback.lift (E.p₁ k) (E.p₂ k) ⋯
Module: Mathlib.CategoryTheory.Sites.Continuous

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
inst✝ : F.IsContinuous J K
G : Dᵒᵖ ⥤ Type (max w u₁ v₁ u₂ v₂)
hG : Presieve.IsSheaf K G
H : (Cᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂)) ⥤ Dᵒᵖ ⥤ Type (max u₁ v₁ u₂ v₂) := F.op.lan
adj : H ⊣ (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max u₁ v₁ u₂ v₂))).obj F.op := F.op.lanAdjunction (Type (max u₁ v₁ u₂ v₂))
H' : (Cᵒᵖ ⥤ Type (max w u₁ v₁ u₂ v₂)) ⥤ Dᵒᵖ ⥤ Type (max w u₁ v₁ u₂ v₂) := F.op.lan
adj' : H' ⊣ (whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max w u₁ v₁ u₂ v₂))).obj F.op :=
  F.op.lanAdjunction (Type (max w u₁ v₁ u₂ v₂))
X : C
S : Sieve X
hS : S ∈ J X
hWS : J.W (Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂, v₁, u₁} S).ι
this : K.W (H.map (Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂, v₁, u₁} S).ι)
e : H ⋙
    (whiskeringRight Dᵒᵖ (Type (max u₁ v₁ u₂ v₂)) (Type (max (max (max (max u₁ u₂) v₁) v₂) w))).obj
      uliftFunctor.{w, max (max (max u₁ u₂) v₁) v₂} ≅
  (whiskeringRight Cᵒᵖ (Type (max u₁ v₁ u₂ v₂)) (Type (max (max (max (max u₁ u₂) v₁) v₂) w))).obj
      uliftFunctor.{w, max (max (max u₁ u₂) v₁) v₂} ⋙
    H' :=
  uliftFunctor.{w, max (max (max u₁ u₂) v₁) v₂}.lanCompIsoOfPreserves F.op
⊢ (H'.mapIso S.shrinkFunctorUliftFunctorIso.symm ≪≫
          (e.app (Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂, v₁, u₁} S).toFunctor).symm).hom ≫
      whiskerRight (H.map (Sieve.shrinkFunctor.{max u₁ v₁ u₂ v₂, v₁, u₁} S).ι)
        uliftFunctor.{w, max (max (max u₁ u₂) v₁) v₂} =
    H'.map (Sieve.shrinkFunctor.{max w u₁ v₁ u₂ v₂, v₁, u₁} S).ι ≫
      (H'.mapIso (shrinkYonedaUliftFunctorIso.app X).symm ≪≫
          (e.app (shrinkYoneda.{max u₁ v₁ u₂ v₂, v₁, u₁}.obj X)).symm).hom

Tactic:
simp only [Functor.mapIso_symm, Functor.comp_obj, Functor.whiskeringRight_obj_obj,
          Iso.trans_hom, Iso.symm_hom, Functor.mapIso_inv, Iso.app_inv, Category.assoc]
        rw [← Functor.map_comp_assoc, ← dsimp% e.inv.naturality, ← Functor.map_comp_assoc,
          Sieve.shrinkFunctorUliftFunctorIso_inv_ι]

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

Goal state before:
pp: case refine_2
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
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
h : CoverPreserving K J G
U : C
S : Sieve (F.obj U)
hS : S ∈ K (F.obj U)
⊢ Sieve.functorPullback F S ∈ J U

Tactic:
refine J.superset_covering ?_ (J.pullback_stable (adj.unit.app U) <| h.cover_preserve hS)

Goal state after:
case refine_2
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
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
h : CoverPreserving K J G
U : C
S : Sieve (F.obj U)
hS : S ∈ K (F.obj U)
⊢ Sieve.pullback (adj.unit.app U) (Sieve.functorPushforward G S) ≤ Sieve.functorPullback F S
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)
this :
  ∀ {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))
Y₁ Y₂ Z : D
iZY₁ : Z ⟶ Y₁
iZY₂ : Z ⟶ Y₂
W₁ : C
iYW₁ : Y₁ ⟶ G.obj W₁
iWX₁ : G.obj W₁ ⟶ X
h₁ : coverByImage G X (iYW₁ ≫ iWX₁)
W₂ : C
iYW₂ : Y₂ ⟶ G.obj W₂
iWX₂ : G.obj W₂ ⟶ X
h₂ : coverByImage G X (iYW₂ ≫ iWX₂)
e : iZY₁ ≫ iYW₁ ≫ iWX₁ = iZY₂ ≫ iYW₂ ≫ iWX₂
⊢ (ConcreteCategory.hom (ℱ'.obj.map (iZY₁ ≫ { obj := W₁, lift := iYW₁, map := iWX₁, fac := ⋯ }.lift).op))
      ((ConcreteCategory.hom (α.app (op { obj := W₁, lift := iYW₁, map := iWX₁, fac := ⋯ }.1)))
        ((ConcreteCategory.hom (ℱ.map { obj := W₁, lift := iYW₁, map := iWX₁, fac := ⋯ }.map.op)) x)) =
    (ConcreteCategory.hom (ℱ'.obj.map (iZY₂ ≫ { obj := W₂, lift := iYW₂, map := iWX₂, fac := ⋯ }.lift).op))
      ((ConcreteCategory.hom (α.app (op { obj := W₂, lift := iYW₂, map := iWX₂, fac := ⋯ }.1)))
        ((ConcreteCategory.hom (ℱ.map { obj := W₂, lift := iYW₂, map := iWX₂, fac := ⋯ }.map.op)) x))

Tactic:
exact this _ _ _ _ (by simpa only [Category.assoc] using e)

Goal state after:
Module: Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology

Goal state before:
pp: case transitive
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.IsLocallyFull K
inst✝ : G.IsLocallyFaithful K
U✝ : C
S✝ : Sieve U✝
X : C
S R : Sieve X
a✝¹ : (Precoverage.comap G K.toPrecoverage).Saturate X S
a✝ : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → (Precoverage.comap G K.toPrecoverage).Saturate Y (Sieve.pullback f R)
hS : Sieve.functorPushforward G S ∈ K (G.obj X)
H' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → Sieve.functorPushforward G (Sieve.pullback f R) ∈ K (G.obj Y)
⊢ Sieve.functorPushforward G R ∈ K (G.obj X)

Tactic:
| transitive X S R _ _ hS H' =>

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

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
inst✝³ : G.IsCoverDense J
inst✝² : G.Full
inst✝¹ : G.IsContinuous K J
inst✝ : (G.sheafPushforwardContinuous A K J).EssSurj
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
h₁ : K.W = ObjectProperty.isLocal fun x ↦ x ∈ Set.range (sheafToPresheaf J A ⋙ (whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).obj
R : Sheaf J A
⊢ (Function.Bijective fun g ↦ G.op.whiskerLeft f ≫ g) ↔ Function.Bijective fun g ↦ f ≫ g

Tactic:
← Function.Bijective.of_comp_iff _
      (Functor.whiskerLeft_obj_map_bijective_of_isCoverDense J G Q R.obj R.property)

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
A : Type u₃
inst✝⁴ : Category.{v₃, u₃} A
inst✝³ : G.IsCoverDense J
inst✝² : G.Full
inst✝¹ : G.IsContinuous K J
inst✝ : (G.sheafPushforwardContinuous A K J).EssSurj
P Q : Cᵒᵖ ⥤ A
f : P ⟶ Q
h₁ : K.W = ObjectProperty.isLocal fun x ↦ x ∈ Set.range (sheafToPresheaf J A ⋙ (whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).obj
R : Sheaf J A
⊢ Function.Bijective ((fun g ↦ G.op.whiskerLeft f ≫ g) ∘ ((whiskeringLeft Dᵒᵖ Cᵒᵖ A).obj G.op).map) ↔
    Function.Bijective fun g ↦ f ≫ g
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

Goal state after:
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
h : Sieve.ofObjects Y X ∈ J X
⊢ J.CoversTop Y
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 : PreOneHypercover S
inst✝ : E.HasPullbacks
mem₀ : E.sieve₀ ∈ J S
mem₁' : ∀ (i₁ i₂ : E.I₀), E.sieve₁' i₁ i₂ ∈ J (Limits.pullback (E.f i₁) (E.f i₂))
i₁ i₂ : E.I₀
W : C
p₁ : W ⟶ E.X i₁
p₂ : W ⟶ E.X i₂
w : p₁ ≫ E.f i₁ = p₂ ≫ E.f i₂
⊢ E.sieve₁ p₁ p₂ ∈ J W

Tactic:
rw [E.sieve₁_eq_pullback_sieve₁' _ _ w]
    exact J.pullback_stable' _ (mem₁' i₁ i₂)

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

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
S : J.Cover X
Y✝ Y : C
g : S.preOneHypercover.I₀
w✝ : Y✝ ⟶ S.preOneHypercover.X g
⊢ (↑S).arrows (w✝ ≫ S.preOneHypercover.f g)

Tactic:
exact S.1.downward_closed g.hf _

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
J : GrothendieckTopology C
X : C
S : J.Cover X
f₁ f₂ : S.preOneHypercover.I₀
x✝ : C
p₁ : x✝ ⟶ S.preOneHypercover.X f₁
p₂ : x✝ ⟶ S.preOneHypercover.X f₂
w : p₁ ≫ S.preOneHypercover.f f₁ = p₂ ≫ S.preOneHypercover.f f₂
⊢ S.preOneHypercover.sieve₁ p₁ p₂ ∈ J x✝

Tactic:
by simp [S.preOneHypercover_sieve₁ f₁ f₂ p₁ p₂ w]

Goal state after:
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
⊢ IsIso f → f ≠ 0

Tactic:
intro h

Goal state after:
case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
h : IsIso f
⊢ f ≠ 0
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
⊢ f ≠ 0 → IsIso f

Tactic:
intro h

Goal state after:
case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
h : f ≠ 0
⊢ IsIso f
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X Y : C
⊢ biprod.snd ≫ biprod.inr = 0 → IsZero Y

Tactic:
intro h

Goal state after:
case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X Y : C
h : biprod.snd ≫ biprod.inr = 0
⊢ IsZero Y
Module: Mathlib.CategoryTheory.Simple

Goal state before:
pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X Y : C
⊢ IsZero Y → biprod.snd ≫ biprod.inr = 0

Tactic:
intro h

Goal state after:
case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X Y : C
h : IsZero Y
⊢ biprod.snd ≫ biprod.inr = 0
Module: Mathlib.CategoryTheory.Simple

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

Tactic:
intro h

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
h : Simple X
⊢ IsSimpleOrder (Subobject X)
Module: Mathlib.CategoryTheory.Simple

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

Tactic:
intro h

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
h : IsSimpleOrder (Subobject X)
⊢ Simple X
Module: Mathlib.Topology.Category.TopCat.OpenNhds

Goal state before:
pp: X Y : TopCat
f : X ⟶ Y
x✝¹ : ↑X
U V W : OpenNhds x✝¹
x✝ : ↑X
x : OpenNhds x✝
⊢ x ≤ ⟨⊤, trivial⟩

Tactic:
cases x

Goal state after:
case mk
X Y : TopCat
f : X ⟶ Y
x✝ : ↑X
U V W : OpenNhds x✝
x : ↑X
val✝ : Opens ↑X
property✝ : x ∈ val✝
⊢ ⟨val✝, property✝⟩ ≤ ⟨⊤, trivial⟩
Module: Mathlib.Topology.Category.TopCat.Opens

Goal state before:
pp: case mpr
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
V : Opens ↑Y
t : Set ↑Y
ht : IsOpen t
hU : IsOpen (⇑(ConcreteCategory.hom f) ⁻¹' t)
⊢ (Opens.map f).obj V ≤ { carrier := ⇑(ConcreteCategory.hom f) ⁻¹' t, is_open' := hU } →
    V ≤ hf.functorObj { carrier := ⇑(ConcreteCategory.hom f) ⁻¹' t, is_open' := hU }

Tactic:
intro h

Goal state after:
case mpr
X Y : TopCat
f : X ⟶ Y
hf : IsInducing ⇑(ConcreteCategory.hom f)
V : Opens ↑Y
t : Set ↑Y
ht : IsOpen t
hU : IsOpen (⇑(ConcreteCategory.hom f) ⁻¹' t)
h : (Opens.map f).obj V ≤ { carrier := ⇑(ConcreteCategory.hom f) ⁻¹' t, is_open' := hU }
⊢ V ≤ hf.functorObj { carrier := ⇑(ConcreteCategory.hom f) ⁻¹' t, is_open' := hU }
Module: Mathlib.Topology.Category.TopCat.Opens

Goal state before:
pp: case mpr
X : TopCat
U : Opens ↑X
x : ↑X
⊢ x ∈ ↑U → x ∈ Set.range ⇑(ConcreteCategory.hom U.inclusion')

Tactic:
intro h

Goal state after:
case mpr
X : TopCat
U : Opens ↑X
x : ↑X
h : x ∈ ↑U
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom U.inclusion')
Module: Mathlib.Topology.Category.TopCat.Opens

Goal state before:
pp: X : TopCat
U : Opens ↑X
V : Opens ↥U
⊢ (map U.inclusion' ⋙ ⋯.functor).obj (⋯.functor.obj V) = (𝟭 (Opens ↑X)).obj (⋯.functor.obj V)

Tactic:
by dsimp; rw [map_functor_eq V]

Goal state after: