mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
x✝ : ↑(pullback g₁ g₂)
x₁ : ↑W
hx₁ : (ConcreteCategory.hom i₁) x₁ = (ConcreteCategory.hom (pullback.fst g₁ g₂)) x✝
x₂ : ↑X
hx₂ : (ConcreteCategory.hom i₂) x₂ = (ConcreteCategory.hom (pullback.snd g₁ g₂)) x✝
⊢ (ConcreteCategory.hom g₁) ((ConcreteCategory.hom (pullback.fst g₁ g₂)) x✝) =
    (ConcreteCategory.hom g₂) ((ConcreteCategory.hom i₂) x₂)

Tactic:
hx₂,

Goal state after:
W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
x✝ : ↑(pullback g₁ g₂)
x₁ : ↑W
hx₁ : (ConcreteCategory.hom i₁) x₁ = (ConcreteCategory.hom (pullback.fst g₁ g₂)) x✝
x₂ : ↑X
hx₂ : (ConcreteCategory.hom i₂) x₂ = (ConcreteCategory.hom (pullback.snd g₁ g₂)) x✝
⊢ (ConcreteCategory.hom g₁) ((ConcreteCategory.hom (pullback.fst g₁ g₂)) x✝) =
    (ConcreteCategory.hom g₂) ((ConcreteCategory.hom (pullback.snd g₁ g₂)) x✝)
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : H✝.IsVanKampen
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
this : F'.map WalkingSpan.Hom.fst ≫ c'.ι.app WalkingSpan.left = F'.map WalkingSpan.Hom.snd ≫ c'.ι.app WalkingSpan.right
⊢ ∀ (j : WalkingSpan),
    ((Cocone.precompose (diagramIsoSpan F').inv).obj c').ι.app j ≫ (Iso.refl c'.pt).hom =
      (PushoutCocone.mk (c'.ι.app WalkingSpan.left) (c'.ι.app WalkingSpan.right) this).ι.app j

Tactic:
rintro (_ | _ | _) <;> dsimp

Goal state after:
case none
C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : H✝.IsVanKampen
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
this : F'.map WalkingSpan.Hom.fst ≫ c'.ι.app WalkingSpan.left = F'.map WalkingSpan.Hom.snd ≫ c'.ι.app WalkingSpan.right
⊢ (𝟙 (F'.obj none) ≫ c'.ι.app none) ≫ 𝟙 c'.pt = F'.map WalkingSpan.Hom.fst ≫ c'.ι.app WalkingSpan.left

case some.left
C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : H✝.IsVanKampen
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
this : F'.map WalkingSpan.Hom.fst ≫ c'.ι.app WalkingSpan.left = F'.map WalkingSpan.Hom.snd ≫ c'.ι.app WalkingSpan.right
⊢ (𝟙 (F'.obj (some WalkingPair.left)) ≫ c'.ι.app (some WalkingPair.left)) ≫ 𝟙 c'.pt = c'.ι.app WalkingSpan.left

case some.right
C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : H✝.IsVanKampen
F' : WalkingSpan ⥤ C
c' : Cocone F'
α : F' ⟶ span f g
fα : c'.pt ⟶ (PushoutCocone.mk h i ⋯).pt
eα : α ≫ (PushoutCocone.mk h i ⋯).ι = c'.ι ≫ (Functor.const WalkingSpan).map fα
hα : NatTrans.Equifibered α
this : F'.map WalkingSpan.Hom.fst ≫ c'.ι.app WalkingSpan.left = F'.map WalkingSpan.Hom.snd ≫ c'.ι.app WalkingSpan.right
⊢ (𝟙 (F'.obj (some WalkingPair.right)) ≫ c'.ι.app (some WalkingPair.right)) ≫ 𝟙 c'.pt = c'.ι.app WalkingSpan.right
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: case mpr.refine_4
C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i ⋯)
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
⊢ { app := fun X_1 ↦ Option.casesOn X_1 αW fun val ↦ WalkingPair.casesOn val αX αY, naturality := ⋯ }.Equifibered

pp: case mpr.refine_5
C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i ⋯)
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
⊢ (∀ (j : WalkingSpan),
      IsPullback (w.cocone.ι.app j)
        ({ app := fun X_1 ↦ Option.casesOn X_1 αW fun val ↦ WalkingPair.casesOn val αX αY, naturality := ⋯ }.app j) αZ
        ((PushoutCocone.mk h i ⋯).ι.app j)) ↔
    IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i

pp: case mpr.refine_1
C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i ⋯)
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
⊢ IsPushout f' g' h' i' ↔ Nonempty (IsColimit w.cocone)

Tactic:
· rintro i _ (_ | _ | _)
      · dsimp; simp_rw [Functor.map_id]
        exact IsPullback.of_horiz_isIso ⟨by rw [Category.comp_id, Category.id_comp]⟩
      exacts [hf, hg]

Goal state after:
case mpr.refine_5
C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i ⋯)
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
⊢ (∀ (j : WalkingSpan),
      IsPullback (w.cocone.ι.app j)
        ({ app := fun X_1 ↦ Option.casesOn X_1 αW fun val ↦ WalkingPair.casesOn val αX αY, naturality := ⋯ }.app j) αZ
        ((PushoutCocone.mk h i ⋯).ι.app j)) ↔
    IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i

case mpr.refine_1
C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H✝ : IsPushout f g h i
H : IsVanKampenColimit (PushoutCocone.mk h i ⋯)
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
⊢ IsPushout f' g' h' i' ↔ Nonempty (IsColimit w.cocone)
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f c.inl h i
hc₁ : IsColimit (BinaryCofan.mk (c.inr ≫ i) h)
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY c.inl
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' (pullback.fst αY c.inr))
hc₃ :
  IsPullback (BinaryCofan.mk ((BinaryCofan.mk g' (pullback.fst αY c.inr)).inr ≫ i') h').inl (pullback.snd αY c.inr) αZ
    (BinaryCofan.mk (c.inr ≫ i) h).inl
hc₄ :
  IsPullback (BinaryCofan.mk ((BinaryCofan.mk g' (pullback.fst αY c.inr)).inr ≫ i') h').inr αX αZ
    (BinaryCofan.mk (c.inr ≫ i) h).inr
Y'' : C := pullback αZ i
cmp : Y' ⟶ Y'' := pullback.lift i' αY ⋯
e₁ : (g' ≫ cmp) ≫ pullback.snd αZ i = αW ≫ c.inl
⊢ pullback.fst αY c.inr ≫ αY = pullback.snd αY c.inr ≫ c.inr

Tactic:
pullback.condition

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f c.inl h i
hc₁ : IsColimit (BinaryCofan.mk (c.inr ≫ i) h)
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY c.inl
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' (pullback.fst αY c.inr))
hc₃ :
  IsPullback (BinaryCofan.mk ((BinaryCofan.mk g' (pullback.fst αY c.inr)).inr ≫ i') h').inl (pullback.snd αY c.inr) αZ
    (BinaryCofan.mk (c.inr ≫ i) h).inl
hc₄ :
  IsPullback (BinaryCofan.mk ((BinaryCofan.mk g' (pullback.fst αY c.inr)).inr ≫ i') h').inr αX αZ
    (BinaryCofan.mk (c.inr ≫ i) h).inr
Y'' : C := pullback αZ i
cmp : Y' ⟶ Y'' := pullback.lift i' αY ⋯
e₁ : (g' ≫ cmp) ≫ pullback.snd αZ i = αW ≫ c.inl
⊢ pullback.snd αY c.inr ≫ c.inr = pullback.snd αY c.inr ≫ c.inr
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : FinitaryPreExtensive C
n : ℕ
F : Discrete (Fin n) ⥤ C
c : Cocone F
hc : IsColimit c
⊢ IsUniversalColimit c

Tactic:
let f : Fin n → C := F.obj ∘ Discrete.mk
  have : F = Discrete.functor f :=
    Functor.hext (fun _ ↦ rfl) (by rintro ⟨i⟩ ⟨j⟩ ⟨⟨rfl : i = j⟩⟩; simp [f])
  clear_value f
  subst this
  induction n with
  | zero => exact (isVanKampenColimit_of_isEmpty _ hc).isUniversal
  | succ n IH =>
    refine IsUniversalColimit.of_iso (@isUniversalColimit_extendCofan _ _ _ _ _ _
      (IH _ (coproductIsCoproduct _)) (FinitaryPreExtensive.universal' _ (coprodIsCoprod _ _)) ?_)
      ((extendCofanIsColimit f (coproductIsCoproduct _) (coprodIsCoprod _ _)).uniqueUpToIso hc)
    · dsimp
      infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: J : Type v'
inst✝⁴ : Category.{u', v'} J
C : Type u
inst✝³ : Category.{v, u} C
W X Y Z✝ : C
f✝ : W ⟶ X
g✝ : W ⟶ Y
h : X ⟶ Z✝
i : Y ⟶ Z✝
inst✝² : Adhesive C
Z A B : C
a : A ⟶ Z
b : B ⟶ Z
inst✝¹ : Mono a
inst✝ : Mono b
K : C
f g : K ⟶ pushout (fst a b) (snd a b)
w : f ≫ pushout.desc a b ⋯ = g ≫ pushout.desc a b ⋯
u : A ⟶ pushout (fst a b) (snd a b) := inl (fst a b) (snd a b)
v : B ⟶ pushout (fst a b) (snd a b) := inr (fst a b) (snd a b)
this✝ : Mono u := mono_of_isPushout_of_mono_right (of_hasPushout (fst a b) (snd a b))
this : Mono v := mono_of_isPushout_of_mono_left (of_hasPushout (fst a b) (snd a b))
sq_f_u : IsPullback (fst f u) (snd f u) f u := of_hasPullback f u
sq_f_v : IsPullback (fst f v) (snd f v) f v := of_hasPullback f v
sq_g_u : IsPullback (fst g u) (snd g u) g u := of_hasPullback g u
sq_g_v : IsPullback (fst g v) (snd g v) g v := of_hasPullback g v
l₁ : pullback f u ⟶ K := fst f u
f₁ : pullback f u ⟶ A := snd f u
l₂ : pullback f v ⟶ K := fst f v
f₂ : pullback f v ⟶ B := snd f v
m₁ : pullback g u ⟶ K := fst g u
g₁ : pullback g u ⟶ A := snd g u
m₂ : pullback g v ⟶ K := fst g v
⊢ f = g

Tactic:
let g₂ := pullback.snd g v

Goal state after:
J : Type v'
inst✝⁴ : Category.{u', v'} J
C : Type u
inst✝³ : Category.{v, u} C
W X Y Z✝ : C
f✝ : W ⟶ X
g✝ : W ⟶ Y
h : X ⟶ Z✝
i : Y ⟶ Z✝
inst✝² : Adhesive C
Z A B : C
a : A ⟶ Z
b : B ⟶ Z
inst✝¹ : Mono a
inst✝ : Mono b
K : C
f g : K ⟶ pushout (fst a b) (snd a b)
w : f ≫ pushout.desc a b ⋯ = g ≫ pushout.desc a b ⋯
u : A ⟶ pushout (fst a b) (snd a b) := inl (fst a b) (snd a b)
v : B ⟶ pushout (fst a b) (snd a b) := inr (fst a b) (snd a b)
this✝ : Mono u := mono_of_isPushout_of_mono_right (of_hasPushout (fst a b) (snd a b))
this : Mono v := mono_of_isPushout_of_mono_left (of_hasPushout (fst a b) (snd a b))
sq_f_u : IsPullback (fst f u) (snd f u) f u := of_hasPullback f u
sq_f_v : IsPullback (fst f v) (snd f v) f v := of_hasPullback f v
sq_g_u : IsPullback (fst g u) (snd g u) g u := of_hasPullback g u
sq_g_v : IsPullback (fst g v) (snd g v) g v := of_hasPullback g v
l₁ : pullback f u ⟶ K := fst f u
f₁ : pullback f u ⟶ A := snd f u
l₂ : pullback f v ⟶ K := fst f v
f₂ : pullback f v ⟶ B := snd f v
m₁ : pullback g u ⟶ K := fst g u
g₁ : pullback g u ⟶ A := snd g u
m₂ : pullback g v ⟶ K := fst g v
g₂ : pullback g v ⟶ B := snd g v
⊢ f = g
Module: Mathlib.CategoryTheory.Sites.LeftExact

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{t, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
X : C
inst✝ : HasLimitsOfSize.{max t u v, max t u v, t, w} D
⊢ PreservesLimits (J.diagramFunctor D X)

Tactic:
constructor
  intro _ _
  apply preservesLimitsOfShape_diagramFunctor.{max t u v}

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

Goal state before:
pp: C : Type u
inst✝¹² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹¹ : Category.{t, w} D
inst✝¹⁰ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝⁹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁸ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁷ : ConcreteCategory D FD
inst✝⁶ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝⁵ : ∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ
K : Type t
inst✝⁴ : SmallCategory K
inst✝³ : FinCategory K
inst✝² : HasLimitsOfShape K D
inst✝¹ : PreservesLimitsOfShape K (forget D)
inst✝ : ReflectsLimitsOfShape K (forget D)
F : K ⥤ Cᵒᵖ ⥤ D
⊢ PreservesLimit F (J.plusFunctor D)

Tactic:
apply preservesLimit_of_evaluation

Goal state after:
C : Type u
inst✝¹² : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝¹¹ : Category.{t, w} D
inst✝¹⁰ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝⁹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁸ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁷ : ConcreteCategory D FD
inst✝⁶ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝⁵ : ∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ
K : Type t
inst✝⁴ : SmallCategory K
inst✝³ : FinCategory K
inst✝² : HasLimitsOfShape K D
inst✝¹ : PreservesLimitsOfShape K (forget D)
inst✝ : ReflectsLimitsOfShape K (forget D)
F : K ⥤ Cᵒᵖ ⥤ D
⊢ ∀ (k : Cᵒᵖ), PreservesLimit F (J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj k)
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
F : C ⥤ D
G : D ⥤ C
adj : G ⊣ F
inst✝¹ : G.Full
inst✝ : G.Faithful
⊢ F.IsLocalization (isColocal fun x ↦ x ∈ Set.range G.obj)

Tactic:
rw [isColocal_eq_inverseImage_isomorphisms adj]

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
F : C ⥤ D
G : D ⥤ C
adj : G ⊣ F
inst✝¹ : G.Full
inst✝ : G.Faithful
⊢ F.IsLocalization ((MorphismProperty.isomorphisms D).inverseImage F)
Module: Mathlib.CategoryTheory.Sites.PreservesSheafification

Goal state before:
pp: 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
inst✝¹ : J.PreservesSheafification F
inst✝ : HasWeakSheafify J B
⊢ J.W.IsInvertedBy ((whiskeringRight Cᵒᵖ A B).obj F ⋙ presheafToSheaf J B)

Tactic:
intro P₁ P₂ f hf
  dsimp
  rw [← W_iff]
  exact J.W_of_preservesSheafification F _ hf

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
f : F ⟶ G
h₁ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom (f.hom.app X))
right✝ : IsLocallySurjective f
X : Cᵒᵖ
s : G.obj.obj X
H : Presieve.IsSheafFor F.obj (Presheaf.imageSieve f.hom s).arrows
t : Presieve.FamilyOfElements F.obj (Presheaf.imageSieve f.hom s).arrows :=
  fun Y g hg ↦ Presheaf.localPreimage f.hom s g hg
Y₁ Y₂ W : C
g₁ : W ⟶ Y₁
g₂ : W ⟶ Y₂
f₁ : Y₁ ⟶ Opposite.unop X
f₂ : Y₂ ⟶ Opposite.unop X
hf₁ : (Presheaf.imageSieve f.hom s).arrows f₁
hf₂ : (Presheaf.imageSieve f.hom s).arrows f₂
w : g₁ ≫ f₁ = g₂ ≫ f₂
eq₁ :
  (ConcreteCategory.hom (f.hom.app (Opposite.op W))) ((ConcreteCategory.hom (F.obj.map g₁.op)) (t f₁ hf₁)) =
    (ConcreteCategory.hom (G.obj.map g₁.op)) ((ConcreteCategory.hom (f.hom.app (Opposite.op Y₁))) (t f₁ hf₁))
eq₂ :
  (ConcreteCategory.hom (f.hom.app (Opposite.op W))) ((ConcreteCategory.hom (F.obj.map g₂.op)) (t f₂ hf₂)) =
    (ConcreteCategory.hom (G.obj.map g₂.op)) ((ConcreteCategory.hom (f.hom.app (Opposite.op Y₂))) (t f₂ hf₂))
⊢ (ConcreteCategory.hom (f.hom.app (Opposite.op W))) ((ConcreteCategory.hom (F.obj.map g₁.op)) (t f₁ hf₁)) =
    (ConcreteCategory.hom (f.hom.app (Opposite.op W))) ((ConcreteCategory.hom (F.obj.map g₂.op)) (t f₂ hf₂))

Tactic:
have eq₃ := congr_arg (G.obj.map g₁.op) (Presheaf.app_localPreimage f.hom s _ hf₁)

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
f : F ⟶ G
h₁ : ∀ (X : Cᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom (f.hom.app X))
right✝ : IsLocallySurjective f
X : Cᵒᵖ
s : G.obj.obj X
H : Presieve.IsSheafFor F.obj (Presheaf.imageSieve f.hom s).arrows
t : Presieve.FamilyOfElements F.obj (Presheaf.imageSieve f.hom s).arrows :=
  fun Y g hg ↦ Presheaf.localPreimage f.hom s g hg
Y₁ Y₂ W : C
g₁ : W ⟶ Y₁
g₂ : W ⟶ Y₂
f₁ : Y₁ ⟶ Opposite.unop X
f₂ : Y₂ ⟶ Opposite.unop X
hf₁ : (Presheaf.imageSieve f.hom s).arrows f₁
hf₂ : (Presheaf.imageSieve f.hom s).arrows f₂
w : g₁ ≫ f₁ = g₂ ≫ f₂
eq₁ :
  (ConcreteCategory.hom (f.hom.app (Opposite.op W))) ((ConcreteCategory.hom (F.obj.map g₁.op)) (t f₁ hf₁)) =
    (ConcreteCategory.hom (G.obj.map g₁.op)) ((ConcreteCategory.hom (f.hom.app (Opposite.op Y₁))) (t f₁ hf₁))
eq₂ :
  (ConcreteCategory.hom (f.hom.app (Opposite.op W))) ((ConcreteCategory.hom (F.obj.map g₂.op)) (t f₂ hf₂)) =
    (ConcreteCategory.hom (G.obj.map g₂.op)) ((ConcreteCategory.hom (f.hom.app (Opposite.op Y₂))) (t f₂ hf₂))
eq₃ :
  (ConcreteCategory.hom (G.obj.map g₁.op))
      ((ConcreteCategory.hom (f.hom.app (Opposite.op Y₁))) (Presheaf.localPreimage f.hom s f₁ hf₁)) =
    (ConcreteCategory.hom (G.obj.map g₁.op)) ((ConcreteCategory.hom (G.obj.map f₁.op)) s)
⊢ (ConcreteCategory.hom (f.hom.app (Opposite.op W))) ((ConcreteCategory.hom (F.obj.map g₁.op)) (t f₁ hf₁)) =
    (ConcreteCategory.hom (f.hom.app (Opposite.op W))) ((ConcreteCategory.hom (F.obj.map g₂.op)) (t f₂ hf₂))
Module: Mathlib.CategoryTheory.Sites.LocallyBijective

Goal state before:
pp: case mp
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 : Sheaf J A
f : F ⟶ G
inst✝¹ : (forget A).ReflectsIsomorphisms
inst✝ : J.HasSheafCompose (forget A)
⊢ IsLocallyInjective f ∧ IsLocallySurjective f → IsIso f

Tactic:
rintro ⟨_, _⟩
    rw [← isIso_iff_of_reflects_iso f (sheafCompose J (forget A)),
      ← isLocallyBijective_iff_isIso']
    constructor <;> infer_instance

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

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
inst✝¹ : HasWeakSheafify J A
inst✝ : J.WEqualsLocallyBijective A
P Q : Cᵒᵖ ⥤ A
φ : P ⟶ Q
⊢ Sheaf.IsLocallySurjective ((presheafToSheaf J A).map φ) ↔ IsLocallySurjective J φ

Tactic:
rw [← Sheaf.isLocallySurjective_sheafToPresheaf_map_iff,
    ← isLocallySurjective_comp_iff J _ (toSheafify J Q),
    ← comp_isLocallySurjective_iff J (toSheafify J P),
    toSheafify_naturality, ObjectProperty.ι_map]

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₂ : Cᵒᵖ ⥤ Type w
f : F₁ ⟶ F₂
X : C
s : F₂.obj (op X)
hs : s ∈ (Subfunctor.sheafify J (Subfunctor.range f)).obj (op X)
Y : C
g : Y ⟶ X
t : F₁.obj (op Y)
ht : (ConcreteCategory.hom (f.app (op Y))) t = (ConcreteCategory.hom (F₂.map g.op)) s
⊢ (imageSieve (Subfunctor.toRangeSheafify J f) ⟨s, hs⟩).arrows g

Tactic:
exact ⟨t, Subtype.ext ht⟩

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

Goal state before:
pp: case refine_3
C : Type u
inst✝¹ : Category.{v, u} C
ι : Type u_3
S B : C
X : ι → C
a : Cofan X
hau : IsUniversalColimit a
f : (i : ι) → X i ⟶ S
u : a.pt ⟶ S
v : B ⟶ S
P : ι → C
q₁ : (i : ι) → P i ⟶ B
q₂ : (i : ι) → P i ⟶ X i
hP : ∀ (i : ι), IsPullback (q₁ i) (q₂ i) v (f i)
d : Cofan P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
inst✝ : HasPullback v u
c : Cofan P := Cofan.mk (pullback v u) fun i ↦ pullback.lift (q₁ i) (q₂ i ≫ a.inj i) ⋯
hc : IsColimit c
⊢ pullback.snd v u ≫ (Iso.refl a.pt).hom =
    (hc.coconePointUniqueUpToIso hd).hom ≫ Cofan.IsColimit.desc hd fun x ↦ q₂ x ≫ a.inj x

Tactic:
· refine Cofan.IsColimit.hom_ext hc _ _ fun i ↦ ?_
    simpa [Cofan.inj, Cofan.IsColimit.desc] using! pullback.lift_snd _ _ _

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

Goal state before:
pp: case refine_3
C : Type u
inst✝¹ : Category.{v, u} C
ι : Type u_3
S B : C
X : ι → C
a : Cofan X
hau : IsUniversalColimit a
f : (i : ι) → X i ⟶ S
u : a.pt ⟶ S
v : B ⟶ S
P : ι → C
q₁ : (i : ι) → P i ⟶ X i
q₂ : (i : ι) → P i ⟶ B
hP : ∀ (i : ι), IsPullback (q₁ i) (q₂ i) (f i) v
d : Cofan P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
inst✝ : HasPullback u v
c : Cofan P := Cofan.mk (pullback u v) fun i ↦ pullback.lift (q₁ i ≫ a.inj i) (q₂ i) ⋯
hc : IsColimit c
⊢ pullback.snd u v ≫ (Iso.refl B).hom = (hc.coconePointUniqueUpToIso hd).hom ≫ Cofan.IsColimit.desc hd q₂

Tactic:
· refine Cofan.IsColimit.hom_ext hc _ _ fun i ↦ ?_
    simpa [Cofan.inj, Cofan.IsColimit.desc] using! pullback.lift_snd _ _ _

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

Goal state before:
pp: case refine_3
C : Type u
inst✝² : Category.{v, u} C
ι : Type u_3
ι' : Type u_4
S : C
X : ι → C
a : Cofan X
hau : IsUniversalColimit a
Y : ι' → C
b : Cofan Y
hbu : IsUniversalColimit b
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
u : a.pt ⟶ S
v : b.pt ⟶ S
inst✝¹ : ∀ (i : ι), HasPullback (f i) v
inst✝ : HasPullback u v
P : ι × ι' → C
q₁ : (i : ι) → (j : ι') → P (i, j) ⟶ X i
q₂ : (i : ι) → (j : ι') → P (i, j) ⟶ Y j
hP : ∀ (i : ι) (j : ι'), IsPullback (q₁ i j) (q₂ i j) (f i) (g j)
d : Cofan P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
hv : ∀ (i : ι'), b.inj i ≫ v = g i
c : Cofan P := Cofan.mk (pullback u v) fun p ↦ pullback.lift (q₁ p.1 p.2 ≫ a.inj p.1) (q₂ p.1 p.2 ≫ b.inj p.2) ⋯
hc : IsColimit c
⊢ pullback.snd u v ≫ (Iso.refl b.pt).hom =
    (hc.coconePointUniqueUpToIso hd).hom ≫ Cofan.IsColimit.desc hd fun p ↦ q₂ p.1 p.2 ≫ b.inj p.2

Tactic:
· refine Cofan.IsColimit.hom_ext hc _ _ fun i ↦ ?_
    simpa [Cofan.inj, Cofan.IsColimit.desc] using! pullback.lift_snd _ _ _

Goal state after: