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

Goal state before:
pp: case h₁.left
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u''
inst✝ : Category.{v'', u''} D
X Y : C
X' Y' : TopCat
αX : X' ⟶ TopCat.of PUnit.{u + 1}
αY : Y' ⟶ TopCat.of PUnit.{u + 1}
f : (X'.binaryCofan Y').pt ⟶ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).pt
hαX : αX ≫ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl = (X'.binaryCofan Y').inl ≫ f
hαY : αY ≫ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr = (X'.binaryCofan Y').inr ≫ f
s : PullbackCone f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl
l : ↑s.pt → ↑X'
hl : ∀ (x : ↑s.pt), (fun y ↦ (ConcreteCategory.hom s.fst) x = Sum.inl y) (l x)
hl' : ∀ (x : ↑s.pt) (y : ↑X'), (fun y ↦ (ConcreteCategory.hom s.fst) x = Sum.inl y) y → y = l x
⊢ Continuous (Sum.inl ∘ l)

Tactic:
convert! s.fst.hom.2 using 1

Goal state after:
case e'_5
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u''
inst✝ : Category.{v'', u''} D
X Y : C
X' Y' : TopCat
αX : X' ⟶ TopCat.of PUnit.{u + 1}
αY : Y' ⟶ TopCat.of PUnit.{u + 1}
f : (X'.binaryCofan Y').pt ⟶ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).pt
hαX : αX ≫ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl = (X'.binaryCofan Y').inl ≫ f
hαY : αY ≫ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr = (X'.binaryCofan Y').inr ≫ f
s : PullbackCone f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl
l : ↑s.pt → ↑X'
hl : ∀ (x : ↑s.pt), (fun y ↦ (ConcreteCategory.hom s.fst) x = Sum.inl y) (l x)
hl' : ∀ (x : ↑s.pt) (y : ↑X'), (fun y ↦ (ConcreteCategory.hom s.fst) x = Sum.inl y) y → y = l x
e_2✝ :
  (↑X' ⊕ ↑Y') = ↑(((Functor.const (Discrete WalkingPair)).obj (X'.binaryCofan Y').pt).obj { as := WalkingPair.left })
⊢ Sum.inl ∘ l = (TopCat.Hom.hom s.fst).toFun
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case h₁.right
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u''
inst✝ : Category.{v'', u''} D
X Y : C
X' Y' : TopCat
αX : X' ⟶ TopCat.of PUnit.{u + 1}
αY : Y' ⟶ TopCat.of PUnit.{u + 1}
f : (X'.binaryCofan Y').pt ⟶ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).pt
hαX : αX ≫ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl = (X'.binaryCofan Y').inl ≫ f
hαY : αY ≫ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr = (X'.binaryCofan Y').inr ≫ f
s : PullbackCone f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr
l : ↑s.pt → ↑Y'
hl : ∀ (x : ↑s.pt), (fun y ↦ (ConcreteCategory.hom s.fst) x = Sum.inr y) (l x)
hl' : ∀ (x : ↑s.pt) (y : ↑Y'), (fun y ↦ (ConcreteCategory.hom s.fst) x = Sum.inr y) y → y = l x
⊢ { l //
    l ≫ (PullbackCone.mk (X'.binaryCofan Y').inr αY ⋯).fst = s.fst ∧
      l ≫ (PullbackCone.mk (X'.binaryCofan Y').inr αY ⋯).snd = s.snd ∧
        ∀ {m : s.pt ⟶ (PullbackCone.mk (X'.binaryCofan Y').inr αY ⋯).pt},
          m ≫ (PullbackCone.mk (X'.binaryCofan Y').inr αY ⋯).fst = s.fst →
            m ≫ (PullbackCone.mk (X'.binaryCofan Y').inr αY ⋯).snd = s.snd → m = l }

Tactic:
refine ⟨TopCat.ofHom ⟨l, ?_⟩, TopCat.ext fun a => (hl a).symm,
        TopCat.isTerminalPUnit.hom_ext _ _,
        fun {l'} h₁ _ =>
          TopCat.ext fun x => hl' x (l' x) (ConcreteCategory.congr_hom h₁ x).symm⟩

Goal state after:
case h₁.right
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u''
inst✝ : Category.{v'', u''} D
X Y : C
X' Y' : TopCat
αX : X' ⟶ TopCat.of PUnit.{u + 1}
αY : Y' ⟶ TopCat.of PUnit.{u + 1}
f : (X'.binaryCofan Y').pt ⟶ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).pt
hαX : αX ≫ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl = (X'.binaryCofan Y').inl ≫ f
hαY : αY ≫ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr = (X'.binaryCofan Y').inr ≫ f
s : PullbackCone f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr
l : ↑s.pt → ↑Y'
hl : ∀ (x : ↑s.pt), (fun y ↦ (ConcreteCategory.hom s.fst) x = Sum.inr y) (l x)
hl' : ∀ (x : ↑s.pt) (y : ↑Y'), (fun y ↦ (ConcreteCategory.hom s.fst) x = Sum.inr y) y → y = l x
⊢ Continuous l
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case h₁.right
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u''
inst✝ : Category.{v'', u''} D
X Y : C
X' Y' : TopCat
αX : X' ⟶ TopCat.of PUnit.{u + 1}
αY : Y' ⟶ TopCat.of PUnit.{u + 1}
f : (X'.binaryCofan Y').pt ⟶ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).pt
hαX : αX ≫ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl = (X'.binaryCofan Y').inl ≫ f
hαY : αY ≫ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr = (X'.binaryCofan Y').inr ≫ f
s : PullbackCone f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr
l : ↑s.pt → ↑Y'
hl : ∀ (x : ↑s.pt), (fun y ↦ (ConcreteCategory.hom s.fst) x = Sum.inr y) (l x)
hl' : ∀ (x : ↑s.pt) (y : ↑Y'), (fun y ↦ (ConcreteCategory.hom s.fst) x = Sum.inr y) y → y = l x
⊢ Continuous (Sum.inr ∘ l)

Tactic:
convert! s.fst.hom.2 using 1

Goal state after:
case e'_5
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u''
inst✝ : Category.{v'', u''} D
X Y : C
X' Y' : TopCat
αX : X' ⟶ TopCat.of PUnit.{u + 1}
αY : Y' ⟶ TopCat.of PUnit.{u + 1}
f : (X'.binaryCofan Y').pt ⟶ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).pt
hαX : αX ≫ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl = (X'.binaryCofan Y').inl ≫ f
hαY : αY ≫ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr = (X'.binaryCofan Y').inr ≫ f
s : PullbackCone f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr
l : ↑s.pt → ↑Y'
hl : ∀ (x : ↑s.pt), (fun y ↦ (ConcreteCategory.hom s.fst) x = Sum.inr y) (l x)
hl' : ∀ (x : ↑s.pt) (y : ↑Y'), (fun y ↦ (ConcreteCategory.hom s.fst) x = Sum.inr y) y → y = l x
e_2✝ :
  (↑X' ⊕ ↑Y') = ↑(((Functor.const (Discrete WalkingPair)).obj (X'.binaryCofan Y').pt).obj { as := WalkingPair.right })
⊢ Sum.inr ∘ l = (TopCat.Hom.hom s.fst).toFun
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: case left
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 := ⋯
cmp : Y' ⟶ Y'' := ⋯
e₁ : (g' ≫ cmp) ≫ pullback.snd αZ i = αW ≫ c.inl
e₂ : (pullback.fst αY c.inr ≫ cmp) ≫ pullback.snd αZ i = pullback.snd αY c.inr ≫ c.inr
⊢ IsPullback (BinaryCofan.mk (g' ≫ cmp) (pullback.fst αY c.inr ≫ cmp)).inl αW (pullback.snd αZ i) c.inl

Tactic:
apply IsPullback.of_right _ e₁ (IsPullback.of_hasPullback _ _)
          rw [Category.assoc, pullback.lift_fst, ← H.w, ← w.w]; exact hf.paste_horiz hc₄

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)
X : C
K : Type s
inst✝¹ : SmallCategory K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Cᵒᵖ ⥤ D
W : (J.Cover X)ᵒᵖ
⊢ ∀ (s : Cone (F ⋙ J.diagramFunctor D X ⋙ (evaluation (J.Cover X)ᵒᵖ D).obj W))
    (m : s.pt ⟶ ((J.diagramFunctor D X ⋙ (evaluation (J.Cover X)ᵒᵖ D).obj W).mapCone (limit.cone F)).pt),
    (∀ (j : K),
        m ≫ ((J.diagramFunctor D X ⋙ (evaluation (J.Cover X)ᵒᵖ D).obj W).mapCone (limit.cone F)).π.app j = s.π.app j) →
      m = liftToDiagramLimitObj F s

Tactic:
intro E m hm
          refine Multiequalizer.hom_ext _ _ _ (fun a => limit_obj_ext (fun j => ?_))
          dsimp [liftToDiagramLimitObj]
          rw [Multiequalizer.lift_ι, Category.assoc, liftToDiagramLimitObjAux_fac, ← hm,
            Category.assoc]
          dsimp
          rw [limit.lift_π]
          dsimp

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Bousfield

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
Z : C
x✝ : P Z
⊢ Function.Bijective fun f_1 ↦ f_1 ≫ f

Tactic:
by
  constructor
  · intro g₁ g₂ _
    simpa only [← cancel_mono f]
  · intro g
    exact ⟨g ≫ inv f, by simp⟩

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

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ c.inl = (cofans X' Y').inl ≫ f →
      αY ≫ c.inr = (cofans X' Y').inr ≫ f →
        IsPullback (cofans X' Y').inl αX f c.inl ∧ IsPullback (cofans X' Y').inr αY f c.inr
h₂ : {Z : C} → (f : Z ⟶ c.pt) → IsColimit (BinaryCofan.mk (cones f c.inl).fst (cones f c.inr).fst)
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ c.inl = c'.inl ≫ f
hY : αY ≫ c.inr = c'.inr ≫ f
H₁ : IsPullback c'.inl αX f c.inl
H₂ : IsPullback c'.inr αY f c.inr
e₁ : X' ≅ (cones f c.inl).pt := H₁.isLimit.conePointUniqueUpToIso (limits f c.inl)
e₂ : Y' ≅ (cones f c.inr).pt := H₂.isLimit.conePointUniqueUpToIso (limits f c.inr)
he₁ : c'.inl = e₁.hom ≫ (cones f c.inl).fst
he₂ : c'.inr = e₂.hom ≫ (cones f c.inr).fst
⊢ IsColimit (BinaryCofan.mk c'.inl c'.inr)

Tactic:
he₁,

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
cofans : (X Y : C) → BinaryCofan X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ c.inl = (cofans X' Y').inl ≫ f →
      αY ≫ c.inr = (cofans X' Y').inr ≫ f →
        IsPullback (cofans X' Y').inl αX f c.inl ∧ IsPullback (cofans X' Y').inr αY f c.inr
h₂ : {Z : C} → (f : Z ⟶ c.pt) → IsColimit (BinaryCofan.mk (cones f c.inl).fst (cones f c.inr).fst)
X' Y' : C
c' : BinaryCofan X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ c.inl = c'.inl ≫ f
hY : αY ≫ c.inr = c'.inr ≫ f
H₁ : IsPullback c'.inl αX f c.inl
H₂ : IsPullback c'.inr αY f c.inr
e₁ : X' ≅ (cones f c.inl).pt := H₁.isLimit.conePointUniqueUpToIso (limits f c.inl)
e₂ : Y' ≅ (cones f c.inr).pt := H₂.isLimit.conePointUniqueUpToIso (limits f c.inr)
he₁ : c'.inl = e₁.hom ≫ (cones f c.inl).fst
he₂ : c'.inr = e₂.hom ≫ (cones f c.inr).fst
⊢ IsColimit (BinaryCofan.mk (e₁.hom ≫ (cones f c.inl).fst) c'.inr)
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u''
inst✝⁸ : Category.{v'', u''} D
inst✝⁷ : HasPullbacks D
inst✝⁶ : Adhesive C
inst✝⁵ : HasPullbacks C
inst✝⁴ : HasPushouts C
H₂ : ∀ {X Y S : D} (f : S ⟶ X) (g : S ⟶ Y) [Mono f], HasPushout f g
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝³ : Gr.Full
inst✝² : Gr.Faithful
inst✝¹ : PreservesLimitsOfShape WalkingCospan Gl
this✝ : PreservesColimitsOfSize.{?u.95, ?u.94, v, v'', u, u''} Gl
this : PreservesLimitsOfSize.{?u.102, ?u.101, v'', v, u'', u} Gr
W X Y Z : D
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : Mono f
H : IsPushout f g h i
⊢ H.IsVanKampen

Tactic:
have := Adhesive.van_kampen (IsPushout.of_hasPushout (Gr.map f) (Gr.map g))

Goal state after:
C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u''
inst✝⁸ : Category.{v'', u''} D
inst✝⁷ : HasPullbacks D
inst✝⁶ : Adhesive C
inst✝⁵ : HasPullbacks C
inst✝⁴ : HasPushouts C
H₂ : ∀ {X Y S : D} (f : S ⟶ X) (g : S ⟶ Y) [Mono f], HasPushout f g
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝³ : Gr.Full
inst✝² : Gr.Faithful
inst✝¹ : PreservesLimitsOfShape WalkingCospan Gl
this✝¹ : PreservesColimitsOfSize.{?u.95, ?u.94, v, v'', u, u''} Gl
this✝ : PreservesLimitsOfSize.{v, v, v'', v, u'', u} Gr
W X Y Z : D
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : Mono f
H : IsPushout f g h i
this : ⋯.IsVanKampen
⊢ H.IsVanKampen
Module: Mathlib.CategoryTheory.Sites.LocallyInjective

Goal state before:
pp: 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₂ F₃ : Cᵒᵖ ⥤ D
φ : F₁ ⟶ F₂
ψ : F₂ ⟶ F₃
P : Cᵒᵖ ⥤ Type (max u v)
X : Cᵒᵖ
x y : ToType (P.obj X)
h : (ConcreteCategory.hom ((J.toPlus P).app X)) x = (ConcreteCategory.hom ((J.toPlus P).app X)) y
⊢ equalizerSieve x y ∈ J (unop X)

Tactic:
toPlus_eq_mk,

Goal state after:
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₂ F₃ : Cᵒᵖ ⥤ D
φ : F₁ ⟶ F₂
ψ : F₂ ⟶ F₃
P : Cᵒᵖ ⥤ Type (max u v)
X : Cᵒᵖ
x y : ToType (P.obj X)
h : mk (Meq.mk ⊤ x) = (ConcreteCategory.hom ((J.toPlus P).app X)) y
⊢ equalizerSieve x y ∈ J (unop X)
Module: Mathlib.CategoryTheory.Sites.LocallyInjective

Goal state before:
pp: 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₂ F₃ : Cᵒᵖ ⥤ D
φ : F₁ ⟶ F₂
ψ : F₂ ⟶ F₃
P : Cᵒᵖ ⥤ Type (max u v)
X : Cᵒᵖ
x y : ToType (P.obj X)
h : mk (Meq.mk ⊤ x) = (ConcreteCategory.hom ((J.toPlus P).app X)) y
⊢ equalizerSieve x y ∈ J (unop X)

Tactic:
toPlus_eq_mk,

Goal state after:
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₂ F₃ : Cᵒᵖ ⥤ D
φ : F₁ ⟶ F₂
ψ : F₂ ⟶ F₃
P : Cᵒᵖ ⥤ Type (max u v)
X : Cᵒᵖ
x y : ToType (P.obj X)
h : mk (Meq.mk ⊤ x) = mk (Meq.mk ⊤ y)
⊢ equalizerSieve x y ∈ J (unop X)
Module: Mathlib.CategoryTheory.Sites.LocallyInjective

Goal state before:
pp: 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₂ : Sheaf J D
φ : F₁ ⟶ F₂
inst✝¹ : J.HasSheafCompose (forget D)
inst✝ : IsLocallyInjective φ
⊢ ∀ (X : Cᵒᵖ), Function.Injective ⇑(ConcreteCategory.hom (φ.hom.app X))

Tactic:
rw [← isLocallyInjective_iff_injective]

Goal state after:
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₂ : Sheaf J D
φ : F₁ ⟶ F₂
inst✝¹ : J.HasSheafCompose (forget D)
inst✝ : IsLocallyInjective φ
⊢ IsLocallyInjective φ
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R✝ : Sheaf J RingCat
R : Cᵒᵖ ⥤ RingCat
M₁ M₂ : PresheafOfModules R
f : M₁ ⟶ M₂
N : PresheafOfModules R
hN : Presheaf.IsSheaf J N.presheaf
inst✝² : J.WEqualsLocallyBijective AddCommGrpCat
inst✝¹ : IsLocallySurjective J f
inst✝ : IsLocallyInjective J f
ψ : M₁ ⟶ N
φ : (toPresheaf R).obj M₂ ⟶ N.presheaf
hφ :
  ∀ (Z : Cᵒᵖ) (x : ↑(M₁.obj Z)),
    (ConcreteCategory.hom (φ.app Z)) ((ConcreteCategory.hom (f.app Z)) x) = (ConcreteCategory.hom (ψ.app Z)) x
X : Cᵒᵖ
r : ↑(R.obj X)
y : ↑(M₂.obj X)
Y : C
p : Y ⟶ Opposite.unop X
x : ↑(M₁.obj (Opposite.op Y))
hx : (ConcreteCategory.hom (f.app (Opposite.op Y))) x = (ConcreteCategory.hom (M₂.map p.op)) y
hφ' :
  ∀ (z : ↑(M₂.obj X)),
    (ConcreteCategory.hom (φ.app (Opposite.op Y))) ((ConcreteCategory.hom (M₂.map p.op)) z) =
      (ConcreteCategory.hom (N.map p.op)) ((ConcreteCategory.hom (φ.app (Opposite.op (Opposite.unop X)))) z)
⊢ (ConcreteCategory.hom (N.map p.op)) ((ConcreteCategory.hom (φ.app X)) (r • y)) =
    (ConcreteCategory.hom (N.map p.op)) (r • (ConcreteCategory.hom (φ.app X)) y)

Tactic:
← hφ',

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R✝ : Sheaf J RingCat
R : Cᵒᵖ ⥤ RingCat
M₁ M₂ : PresheafOfModules R
f : M₁ ⟶ M₂
N : PresheafOfModules R
hN : Presheaf.IsSheaf J N.presheaf
inst✝² : J.WEqualsLocallyBijective AddCommGrpCat
inst✝¹ : IsLocallySurjective J f
inst✝ : IsLocallyInjective J f
ψ : M₁ ⟶ N
φ : (toPresheaf R).obj M₂ ⟶ N.presheaf
hφ :
  ∀ (Z : Cᵒᵖ) (x : ↑(M₁.obj Z)),
    (ConcreteCategory.hom (φ.app Z)) ((ConcreteCategory.hom (f.app Z)) x) = (ConcreteCategory.hom (ψ.app Z)) x
X : Cᵒᵖ
r : ↑(R.obj X)
y : ↑(M₂.obj X)
Y : C
p : Y ⟶ Opposite.unop X
x : ↑(M₁.obj (Opposite.op Y))
hx : (ConcreteCategory.hom (f.app (Opposite.op Y))) x = (ConcreteCategory.hom (M₂.map p.op)) y
hφ' :
  ∀ (z : ↑(M₂.obj X)),
    (ConcreteCategory.hom (φ.app (Opposite.op Y))) ((ConcreteCategory.hom (M₂.map p.op)) z) =
      (ConcreteCategory.hom (N.map p.op)) ((ConcreteCategory.hom (φ.app (Opposite.op (Opposite.unop X)))) z)
⊢ (ConcreteCategory.hom (φ.app (Opposite.op Y))) ((ConcreteCategory.hom (M₂.map p.op)) (r • y)) =
    (ConcreteCategory.hom (N.map p.op)) (r • (ConcreteCategory.hom (φ.app X)) y)
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
P : Cᵒᵖ ⥤ Type (max u v)
U✝ : C
S : J.Cover U✝
x : Meq P S
Y : C
f : Y ⟶ U✝
hf : (↑S).arrows f
⊢ (ConcreteCategory.hom ((J.toPlus P).app (op Y))) (↑x { Y := Y, f := f, hf := hf }) =
    (ConcreteCategory.hom ((J.plusObj P).map f.op)) (Plus.mk x)

Tactic:
toPlus_eq_mk,

Goal state after:
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
P : Cᵒᵖ ⥤ Type (max u v)
U✝ : C
S : J.Cover U✝
x : Meq P S
Y : C
f : Y ⟶ U✝
hf : (↑S).arrows f
⊢ Plus.mk (Meq.mk ⊤ (↑x { Y := Y, f := f, hf := hf })) = (ConcreteCategory.hom ((J.plusObj P).map f.op)) (Plus.mk x)
Module: Mathlib.CategoryTheory.Sites.LocallySurjective

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
f : F ⟶ G
⊢ Presheaf.IsLocallySurjective J f.hom ↔ IsIso (imageι f)

Tactic:
rw [Sheaf.imageι, Presheaf.isLocallySurjective_iff_range_sheafify_eq_top',
    Subfunctor.eq_top_iff_isIso]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type w)
f : F ⟶ G
⊢ IsIso (Subfunctor.sheafify J (Subfunctor.range f.hom)).ι ↔
    IsIso { hom := (Subfunctor.sheafify J (Subfunctor.range f.hom)).ι }
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrpCat
φ : M₀.presheaf ⟶ A.obj
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
X Y : Cᵒᵖ
π : X ⟶ Y
r r' : ↑(R.obj.obj X)
m m' x₁ : ↑(A.obj.obj X)
h₁ :
  ∀ ⦃Y : Cᵒᵖ⦄ (f : X ⟶ Y) (r₀ : ↑(R₀.obj Y)),
    (ConcreteCategory.hom (α.app Y)) r₀ = (ConcreteCategory.hom (R.obj.map f)) r →
      ∀ (m₀ : ↑(M₀.obj Y)),
        (ConcreteCategory.hom (φ.app Y)) m₀ = (ConcreteCategory.hom (A.obj.map f)) m →
          (ConcreteCategory.hom (A.obj.map f)) x₁ = (ConcreteCategory.hom (φ.app Y)) (r₀ • m₀)
x₂ : ↑(A.obj.obj X)
h₂ :
  ∀ ⦃Y : Cᵒᵖ⦄ (f : X ⟶ Y) (r₀ : ↑(R₀.obj Y)),
    (ConcreteCategory.hom (α.app Y)) r₀ = (ConcreteCategory.hom (R.obj.map f)) r →
      ∀ (m₀ : ↑(M₀.obj Y)),
        (ConcreteCategory.hom (φ.app Y)) m₀ = (ConcreteCategory.hom (A.obj.map f)) m →
          (ConcreteCategory.hom (A.obj.map f)) x₂ = (ConcreteCategory.hom (φ.app Y)) (r₀ • m₀)
S : Sieve (Opposite.unop X) := ⋯
hS : S ∈ J (Opposite.unop X)
⊢ ∀ (Y : C) (f : Y ⟶ Opposite.unop X),
    S.arrows f → (ConcreteCategory.hom (A.obj.map f.op)) x₁ = (ConcreteCategory.hom (A.obj.map f.op)) x₂

Tactic:
intro Y f ⟨⟨r₀, hr₀⟩, ⟨m₀, hm₀⟩⟩

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R₀ : Cᵒᵖ ⥤ RingCat
R : Sheaf J RingCat
α : R₀ ⟶ R.obj
inst✝³ : Presheaf.IsLocallyInjective J α
inst✝² : Presheaf.IsLocallySurjective J α
M₀ : PresheafOfModules R₀
A : Sheaf J AddCommGrpCat
φ : M₀.presheaf ⟶ A.obj
inst✝¹ : Presheaf.IsLocallyInjective J φ
inst✝ : Presheaf.IsLocallySurjective J φ
X Y✝ : Cᵒᵖ
π : X ⟶ Y✝
r r' : ↑(R.obj.obj X)
m m' x₁ : ↑(A.obj.obj X)
h₁ :
  ∀ ⦃Y : Cᵒᵖ⦄ (f : X ⟶ Y) (r₀ : ↑(R₀.obj Y)),
    (ConcreteCategory.hom (α.app Y)) r₀ = (ConcreteCategory.hom (R.obj.map f)) r →
      ∀ (m₀ : ↑(M₀.obj Y)),
        (ConcreteCategory.hom (φ.app Y)) m₀ = (ConcreteCategory.hom (A.obj.map f)) m →
          (ConcreteCategory.hom (A.obj.map f)) x₁ = (ConcreteCategory.hom (φ.app Y)) (r₀ • m₀)
x₂ : ↑(A.obj.obj X)
h₂ :
  ∀ ⦃Y : Cᵒᵖ⦄ (f : X ⟶ Y) (r₀ : ↑(R₀.obj Y)),
    (ConcreteCategory.hom (α.app Y)) r₀ = (ConcreteCategory.hom (R.obj.map f)) r →
      ∀ (m₀ : ↑(M₀.obj Y)),
        (ConcreteCategory.hom (φ.app Y)) m₀ = (ConcreteCategory.hom (A.obj.map f)) m →
          (ConcreteCategory.hom (A.obj.map f)) x₂ = (ConcreteCategory.hom (φ.app Y)) (r₀ • m₀)
S : Sieve (Opposite.unop X) := Presheaf.imageSieve α r ⊓ Presheaf.imageSieve φ m
hS : S ∈ J (Opposite.unop X)
Y : C
f : Y ⟶ Opposite.unop X
r₀ : ToType (R₀.obj (Opposite.op Y))
hr₀ : (ConcreteCategory.hom (α.app (Opposite.op Y))) r₀ = (ConcreteCategory.hom (R.obj.map f.op)) r
m₀ : ToType (M₀.presheaf.obj (Opposite.op Y))
hm₀ : (ConcreteCategory.hom (φ.app (Opposite.op Y))) m₀ = (ConcreteCategory.hom (A.obj.map f.op)) m
⊢ (ConcreteCategory.hom (A.obj.map f.op)) x₁ = (ConcreteCategory.hom (A.obj.map f.op)) x₂
Module: Mathlib.CategoryTheory.Limits.Bicones

Goal state before:
pp: J : Type u₁
inst✝ : Category.{v₁, u₁} J
X✝ Y✝ Z✝ : Bicone J
f : BiconeHom J X✝ Y✝
g : BiconeHom J Y✝ Z✝
⊢ BiconeHom J X✝ Z✝

Tactic:
rcases f with (_ | _ | _ | _ | f)

Goal state after:
case left_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
g : BiconeHom J Bicone.left Z✝
⊢ BiconeHom J Bicone.left Z✝

case right_id
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
g : BiconeHom J Bicone.right Z✝
⊢ BiconeHom J Bicone.right Z✝

case left
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ : J
g : BiconeHom J (Bicone.diagram j✝) Z✝
⊢ BiconeHom J Bicone.left Z✝

case right
J : Type u₁
inst✝ : Category.{v₁, u₁} J
Z✝ : Bicone J
j✝ : J
g : BiconeHom J (Bicone.diagram j✝) Z✝
⊢ BiconeHom J Bicone.right Z✝

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✝