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

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} K
C : Type u_3
inst✝³ : Category.{v_3, u_3} C
G : J × K ⥤ C
inst✝² : HasColimitsOfShape K C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasColimit (curry.obj G ⋙ colim)
j : J
k : K
⊢ colimit.ι ((curry.obj G).obj j) k ≫
      colimit.ι (curry.obj G ⋙ colim) j ≫ (colimitCurrySwapCompColimIsoColimitCurryCompColim G).inv =
    colimit.ι ((curry.obj (Prod.swap K J ⋙ G)).obj k) j ≫ colimit.ι (curry.obj (Prod.swap K J ⋙ G) ⋙ colim) k

Tactic:
dsimp [colimitCurrySwapCompColimIsoColimitCurryCompColim]
  conv_lhs => slice 1 3
  rw [colimitIsoColimitCurryCompColim_ι_ι_inv, HasColimit.ι_isoOfEquivalence_inv]
  dsimp [Equivalence.counitInv]
  rw [CategoryTheory.Bifunctor.map_id]
  simp

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

Goal state before:
pp: case inl
C : Type u
inst✝ : Category.{v, u} C
F✝ F' F'' : C ⥤ Type w
G✝ G' F G H : Subfunctor F✝
h₁ : F ≤ H
h₂ : G ≤ H
U : C
x : F✝.obj U
h : x ∈ F.obj U
⊢ x ∈ H.obj U

pp: case inr
C : Type u
inst✝ : Category.{v, u} C
F✝ F' F'' : C ⥤ Type w
G✝ G' F G H : Subfunctor F✝
h₁ : F ≤ H
h₂ : G ≤ H
U : C
x : F✝.obj U
h : x ∈ G.obj U
⊢ x ∈ H.obj U

Tactic:
· exact h₁ _ h

Goal state after:
case inr
C : Type u
inst✝ : Category.{v, u} C
F✝ F' F'' : C ⥤ Type w
G✝ G' F G H : Subfunctor F✝
h₁ : F ≤ H
h₂ : G ≤ H
U : C
x : F✝.obj U
h : x ∈ G.obj U
⊢ x ∈ H.obj U
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
R : Presieve X
ι : Type (max 0 u₁ v₁) := ⋯
⊢ R = ofArrows (fun x ↦ (↑x).fst) fun x ↦ (↑x).snd

Tactic:
exact le_antisymm (fun Z g hg ↦ .mk (⟨⟨_, _⟩, hg⟩ : ι)) fun Z g ⟨x⟩ ↦ x.2

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
u : Y ⟶ X
⊢ (singleton u).uncurry = {⟨Y, u⟩}

Tactic:
ext ⟨Z, v⟩

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
u : Y ⟶ X
Z : C
v : Z ⟶ X
⊢ ⟨Z, v⟩ ∈ (singleton u).uncurry ↔ ⟨Z, v⟩ ∈ {⟨Y, u⟩}
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
s : Presieve X
inst✝ : HasPullbacks C
B : C
b : B ⟶ X
⊢ (pullbackArrows b s).uncurry = (fun f ↦ ⟨Limits.pullback f.snd b, pullback.snd f.snd b⟩) '' s.uncurry

Tactic:
ext ⟨Z, v⟩

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X : C
s : Presieve X
inst✝ : HasPullbacks C
B : C
b : B ⟶ X
Z : C
v : Z ⟶ B
⊢ ⟨Z, v⟩ ∈ (pullbackArrows b s).uncurry ↔
    ⟨Z, v⟩ ∈ (fun f ↦ ⟨Limits.pullback f.snd b, pullback.snd f.snd b⟩) '' s.uncurry
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
s : Presieve X
t : ⦃Y : C⦄ → (f : Y ⟶ X) → s f → Presieve Y
⊢ (s.bind t).uncurry = ⋃ i, ⋃ (h : i ∈ s.uncurry), (Sigma.map id fun Z g ↦ g ≫ i.snd) '' (t i.snd h).uncurry

Tactic:
ext ⟨Z, v⟩

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
s : Presieve X
t : ⦃Y : C⦄ → (f : Y ⟶ X) → s f → Presieve Y
Z : C
v : Z ⟶ X
⊢ ⟨Z, v⟩ ∈ (s.bind t).uncurry ↔
    ⟨Z, v⟩ ∈ ⋃ i, ⋃ (h : i ∈ s.uncurry), (Sigma.map id fun Z g ↦ g ≫ i.snd) '' (t i.snd h).uncurry
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
ι : Type u_1
Y : ι → C
f : (i : ι) → Y i ⟶ X
⊢ (ofArrows Y f).uncurry = Set.range fun i ↦ ⟨Y i, f i⟩

Tactic:
ext ⟨Z, v⟩

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
ι : Type u_1
Y : ι → C
f : (i : ι) → Y i ⟶ X
Z : C
v : Z ⟶ X
⊢ ⟨Z, v⟩ ∈ (ofArrows Y f).uncurry ↔ ⟨Z, v⟩ ∈ Set.range fun i ↦ ⟨Y i, f i⟩
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y✝ : C
f : X ⟶ Y✝
x : FamilyOfElements P (singleton f)
y : P.obj (op Y✝)
H : (ConcreteCategory.hom (P.map f.op)) y = x f ⋯
Y : C
⊢ (ConcreteCategory.hom (P.map f.op)) y = x f ⋯

Tactic:
exact H

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type u_1
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
h :
  ∀ (x : F.obj (op X)),
    (∀ {Z : C} (p₁ p₂ : Z ⟶ X),
        p₁ ≫ f = p₂ ≫ f → (ConcreteCategory.hom (F.map p₁.op)) x = (ConcreteCategory.hom (F.map p₂.op)) x) ↔
      (ConcreteCategory.hom (F.map c.fst.op)) x = (ConcreteCategory.hom (F.map c.snd.op)) x
⊢ Presieve.IsSheafFor F (Presieve.singleton f) ↔ Nonempty (IsLimit (Fork.ofι (F.map f.op) ⋯))

Tactic:
rw [Types.type_equalizer_iff_unique, Presieve.isSheafFor_singleton]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type u_1
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
h :
  ∀ (x : F.obj (op X)),
    (∀ {Z : C} (p₁ p₂ : Z ⟶ X),
        p₁ ≫ f = p₂ ≫ f → (ConcreteCategory.hom (F.map p₁.op)) x = (ConcreteCategory.hom (F.map p₂.op)) x) ↔
      (ConcreteCategory.hom (F.map c.fst.op)) x = (ConcreteCategory.hom (F.map c.snd.op)) x
⊢ (∀ (x : F.obj (op X)),
      (∀ {Z : C} (p₁ p₂ : Z ⟶ X),
          p₁ ≫ f = p₂ ≫ f → (ConcreteCategory.hom (F.map p₁.op)) x = (ConcreteCategory.hom (F.map p₂.op)) x) →
        ∃! y, (ConcreteCategory.hom (F.map f.op)) y = x) ↔
    ∀ (y : F.obj (op X)),
      (ConcreteCategory.hom (F.map c.fst.op)) y = (ConcreteCategory.hom (F.map c.snd.op)) y →
        ∃! x, (ConcreteCategory.hom (F.map f.op)) x = y
Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type u_1
X Y : C
f : X ⟶ Y
c : PullbackCone f f
hc : IsLimit c
⊢ Presieve.IsSheafFor F (Presieve.singleton f) ↔ Nonempty (IsLimit (Fork.ofι (F.map f.op) ⋯))

Tactic:
have h (x : F.obj (op X)) : (∀ {Z : C} (p₁ p₂ : Z ⟶ X),
      p₁ ≫ f = p₂ ≫ f → F.map p₁.op x = F.map p₂.op x) ↔ F.map c.fst.op x = F.map c.snd.op x := by
    refine ⟨fun H ↦ H _ _ c.condition, fun H Z p₁ p₂ h ↦ ?_⟩
    rw [← PullbackCone.IsLimit.lift_fst hc _ _ h, op_comp, Functor.map_comp, comp_apply, H]
    simp [← comp_apply, ← Functor.map_comp, ← op_comp]
  rw [Types.type_equalizer_iff_unique, Presieve.isSheafFor_singleton]
  simp_rw [h]

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: case isOpen_range.hs.self
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
H₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom i₁)
H₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom i₂)
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ Continuous ⇑(ConcreteCategory.hom (pullback.fst g₁ g₂))

pp: case isOpen_range.hs.a
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
H₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom i₁)
H₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom i₂)
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ IsOpen (Set.range ⇑(ConcreteCategory.hom i₁))

pp: case ht.self
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
H₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom i₁)
H₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom i₂)
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ Continuous ⇑(ConcreteCategory.hom (pullback.snd g₁ g₂))

pp: case ht.a
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
H₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom i₁)
H₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom i₂)
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ IsOpen (Set.range ⇑(ConcreteCategory.hom i₂))

Tactic:
· apply ContinuousMap.continuous_toFun

Goal state after:
case isOpen_range.hs.a
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
H₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom i₁)
H₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom i₂)
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ IsOpen (Set.range ⇑(ConcreteCategory.hom i₁))

case ht.self
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
H₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom i₁)
H₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom i₂)
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ Continuous ⇑(ConcreteCategory.hom (pullback.snd g₁ g₂))

case ht.a
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
H₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom i₁)
H₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom i₂)
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ IsOpen (Set.range ⇑(ConcreteCategory.hom i₂))
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: case ht.self
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
H₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom i₁)
H₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom i₂)
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ Continuous ⇑(ConcreteCategory.hom (pullback.snd g₁ g₂))

pp: case ht.a
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
H₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom i₁)
H₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom i₂)
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ IsOpen (Set.range ⇑(ConcreteCategory.hom i₂))

Tactic:
· apply ContinuousMap.continuous_toFun

Goal state after:
case ht.a
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
H₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom i₁)
H₂ : IsOpenEmbedding ⇑(ConcreteCategory.hom i₂)
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
⊢ IsOpen (Set.range ⇑(ConcreteCategory.hom i₂))
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: case mpr.zero
X Y : TopCat
f g : X ⟶ Y
c : Cofork f g
hc : IsColimit c
U : Set ↑c.pt
h : IsOpen (⇑(ConcreteCategory.hom c.π) ⁻¹' U)
⊢ IsOpen
    (⇑(ConcreteCategory.hom ((parallelPair f g).map WalkingParallelPairHom.left ≫ c.ι.app WalkingParallelPair.one)) ⁻¹'
      U)

Tactic:
exact Continuous.isOpen_preimage f.hom.continuous (c.π ⁻¹' U) h

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
A : C
inst✝¹ : HasCoproducts C
inst✝ : MonoCoprod C
J I : Type u
ι : J ⟶ I
hι : Mono ι
⊢ Mono ((sigmaConst.obj A).map ι)

Tactic:
rw [mono_iff_injective] at hι

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
A : C
inst✝¹ : HasCoproducts C
inst✝ : MonoCoprod C
J I : Type u
ι : J ⟶ I
hι : Function.Injective ⇑(ConcreteCategory.hom ι)
⊢ Mono ((sigmaConst.obj A).map ι)
Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct

Goal state before:
pp: case h_1
C : Type u
inst✝² : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
hc : IsColimit c
inst✝¹ : Mono c.inl
inst✝ : Mono c.inr
s : PullbackCone c.inl c.inr
hs : IsLimit s
H : IsInitial s.pt
this : ∀ (i : WalkingPair), Mono (Cofan.inj c i)
i✝ j✝ : WalkingPair
hij✝¹ : i✝ ≠ j✝
hij✝ : WalkingPair.left ≠ WalkingPair.right
⊢ IsInitial s.pt

Tactic:
exact H

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct

Goal state before:
pp: case h_2
C : Type u
inst✝² : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
hc : IsColimit c
inst✝¹ : Mono c.inl
inst✝ : Mono c.inr
s : PullbackCone c.inl c.inr
hs : IsLimit s
H : IsInitial s.pt
this : ∀ (i : WalkingPair), Mono (Cofan.inj c i)
i✝ j✝ : WalkingPair
hij✝¹ : i✝ ≠ j✝
hij✝ : WalkingPair.right ≠ WalkingPair.left
⊢ IsInitial s.flip.pt

Tactic:
exact H

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

Goal state before:
pp: case e'_2.mpr
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
K : Type u_3
inst✝ : Category.{v_3, u_3} K
e : J ≌ K
F : K ⥤ C
c : Cocone F
hc : IsVanKampenColimit c
F' : J ⥤ C
c' : Cocone F'
α : F' ⟶ e.functor ⋙ F
f : c'.pt ⟶ (Cocone.whisker e.functor c).pt
e' : α ≫ (Cocone.whisker e.functor c).ι = c'.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
H : ∀ (j : K), IsPullback (c'.ι.app (e.inverse.obj j)) (α.app (e.inverse.obj j) ≫ F.map (e.counit.app j)) f (c.ι.app j)
j : J
this : α.app j = F'.map (e.unit.app j) ≫ α.app ((e.functor ⋙ e.inverse).obj j) ≫ F.map (e.counit.app (e.functor.obj j))
⊢ IsPullback (c'.ι.app j) (α.app j) f (c.ι.app (e.functor.obj j))

Tactic:
rw [← Category.id_comp f, this]

Goal state after:
case e'_2.mpr
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
K : Type u_3
inst✝ : Category.{v_3, u_3} K
e : J ≌ K
F : K ⥤ C
c : Cocone F
hc : IsVanKampenColimit c
F' : J ⥤ C
c' : Cocone F'
α : F' ⟶ e.functor ⋙ F
f : c'.pt ⟶ (Cocone.whisker e.functor c).pt
e' : α ≫ (Cocone.whisker e.functor c).ι = c'.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
H : ∀ (j : K), IsPullback (c'.ι.app (e.inverse.obj j)) (α.app (e.inverse.obj j) ≫ F.map (e.counit.app j)) f (c.ι.app j)
j : J
this : α.app j = F'.map (e.unit.app j) ≫ α.app ((e.functor ⋙ e.inverse).obj j) ≫ F.map (e.counit.app (e.functor.obj j))
⊢ IsPullback (c'.ι.app j)
    (F'.map (e.unit.app j) ≫ α.app ((e.functor ⋙ e.inverse).obj j) ≫ F.map (e.counit.app (e.functor.obj j)))
    (𝟙 c'.pt ≫ f) (c.ι.app (e.functor.obj j))
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
g₂ : pullback g v ⟶ B := snd g v
w✝² : C
f' : w✝² ⟶ pullback f u
w✝¹ : w✝² ⟶ pullback f v
w✝ : w✝² ⟶ pullback a b
p₁ : IsPullback f' w✝ (snd f u) (fst a b)
left✝ : IsPullback w✝¹ w✝ (snd f v) (snd a b)
h₁ : IsPushout f' w✝¹ (fst f u) (fst f v)
⊢ Mono f'

Tactic:
by
      rw [← p₁.isoPullback_hom_fst]
      infer_instance

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

Goal state before:
pp: J : Type v'
inst✝⁸ : Category.{u', v'} J
C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u_2
inst✝⁶ : Category.{v_2, u_2} D
inst✝⁵ : HasColimitsOfShape J C
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝⁴ : Gr.Full
inst✝³ : Gr.Faithful
F : J ⥤ D
c : Cocone (F ⋙ Gr)
H : IsVanKampenColimit c
inst✝² : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)
inst✝¹ : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl
inst✝ : ∀ (X : C) (i : J) (f : X ⟶ c.pt), PreservesLimit (cospan f (c.ι.app i)) Gl
this✝ : PreservesLimitsOfSize.{?u.178, ?u.177, v_2, v, u_2, u} Gr
this : PreservesColimitsOfSize.{u', v', v, v_2, u, u_2} Gl
F' : J ⥤ D
c' : Cocone F'
α : F' ⟶ (F ⋙ Gr) ⋙ Gl
f : c'.pt ⟶ (Gl.mapCocone c).pt
h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
hc' : IsColimit c'
j : J
α' : F' ⟶ F := α ≫ (F.associator Gr Gl).hom ≫ F.whiskerLeft adj.counit ≫ F.rightUnitor.hom
hα' : NatTrans.Equifibered α'
hα'' : ∀ (j : J), Gl.map (Gr.map (α'.app j)) = adj.counit.app (F'.1 j) ≫ α.app j
β : F' ⋙ Gr ⋙ Gl ≅ F' := F'.isoWhiskerLeft (asIso adj.counit) ≪≫ F'.rightUnitor
⊢ IsPullback (c'.ι.app j) (α.app j) f ((Gl.mapCocone c).ι.app j)

Tactic:
let hl := (IsColimit.precomposeHomEquiv β c').symm hc'

Goal state after:
J : Type v'
inst✝⁸ : Category.{u', v'} J
C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u_2
inst✝⁶ : Category.{v_2, u_2} D
inst✝⁵ : HasColimitsOfShape J C
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝⁴ : Gr.Full
inst✝³ : Gr.Faithful
F : J ⥤ D
c : Cocone (F ⋙ Gr)
H : IsVanKampenColimit c
inst✝² : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)
inst✝¹ : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl
inst✝ : ∀ (X : C) (i : J) (f : X ⟶ c.pt), PreservesLimit (cospan f (c.ι.app i)) Gl
this✝ : PreservesLimitsOfSize.{?u.178, ?u.177, v_2, v, u_2, u} Gr
this : PreservesColimitsOfSize.{u', v', v, v_2, u, u_2} Gl
F' : J ⥤ D
c' : Cocone F'
α : F' ⟶ (F ⋙ Gr) ⋙ Gl
f : c'.pt ⟶ (Gl.mapCocone c).pt
h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
hc' : IsColimit c'
j : J
α' : F' ⟶ F := α ≫ (F.associator Gr Gl).hom ≫ F.whiskerLeft adj.counit ≫ F.rightUnitor.hom
hα' : NatTrans.Equifibered α'
hα'' : ∀ (j : J), Gl.map (Gr.map (α'.app j)) = adj.counit.app (F'.1 j) ≫ α.app j
β : F' ⋙ Gr ⋙ Gl ≅ F' := F'.isoWhiskerLeft (asIso adj.counit) ≪≫ F'.rightUnitor
hl : IsColimit ((Cocone.precompose β.hom).obj c') := (IsColimit.precomposeHomEquiv β c').symm hc'
⊢ IsPullback (c'.ι.app j) (α.app j) f ((Gl.mapCocone c).ι.app j)
Module: Mathlib.CategoryTheory.ObjectProperty.Local

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W W' : MorphismProperty C
Z Z' : C
e : Z ≅ Z'
hZ : W.isLocal Z
X Y : C
f : X ⟶ Y
hf : W f
⊢ Function.Bijective fun g ↦ f ≫ g

Tactic:
by
    rw [← Function.Bijective.of_comp_iff _ (Iso.homToEquiv e).bijective]
    convert! (Iso.homToEquiv e).bijective.comp (hZ f hf) using 1
    aesop

Goal state after:
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✝¹ : F.Full
inst✝ : F.Faithful
⊢ (isLocal fun x ↦ x ∈ Set.range F.obj) = (MorphismProperty.isomorphisms C).inverseImage G

Tactic:
ext P₁ P₂ f
  rw [isLocal_iff_isIso_map adj]
  rfl

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

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₁ F₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst✝¹ : IsLocallyInjective J f₂
inst✝ : IsLocallySurjective J f₂
⊢ IsLocallySurjective J (f₁ ≫ f₂) → IsLocallySurjective J f₁

pp: case mpr
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✝¹ : IsLocallyInjective J f₂
inst✝ : IsLocallySurjective J f₂
⊢ IsLocallySurjective J f₁ → IsLocallySurjective J (f₁ ≫ f₂)

Tactic:
· intro
    exact isLocallySurjective_of_isLocallySurjective_of_isLocallyInjective J f₁ f₂

Goal state after:
case mpr
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✝¹ : IsLocallyInjective J f₂
inst✝ : IsLocallySurjective J f₂
⊢ IsLocallySurjective J f₁ → IsLocallySurjective J (f₁ ≫ f₂)
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)
⊢ (ConcreteCategory.hom (φ.app X)) (r • y) = r • (ConcreteCategory.hom (φ.app X)) y

Tactic:
apply hN.isSeparated _ _
          (Presheaf.imageSieve_mem J ((toPresheaf R).map f) y)

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) (f_1 : Y ⟶ Opposite.unop X),
    (Presheaf.imageSieve ((toPresheaf R).map f) y).arrows f_1 →
      (ConcreteCategory.hom (N.presheaf.map f_1.op)) ((ConcreteCategory.hom (φ.app X)) (r • y)) =
        (ConcreteCategory.hom (N.presheaf.map f_1.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
D : Type u_2
inst✝⁵ : Category.{v_1, u_2} D
FD : D → D → Type u_3
CD : D → Type (max u v)
inst✝⁴ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝³ : ConcreteCategory D FD
P : Cᵒᵖ ⥤ D
inst✝² : HasWeakSheafify J D
inst✝¹ : J.HasSheafCompose (forget D)
inst✝ : J.PreservesSheafification (forget D)
⊢ IsLocallySurjective J (toSheafify J P)

Tactic:
rw [isLocallySurjective_iff_whisker_forget,
    ← sheafComposeIso_hom_fac, ← toSheafify_plusPlusIsoSheafify_hom]

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
D : Type u_2
inst✝⁵ : Category.{v_1, u_2} D
FD : D → D → Type u_3
CD : D → Type (max u v)
inst✝⁴ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝³ : ConcreteCategory D FD
P : Cᵒᵖ ⥤ D
inst✝² : HasWeakSheafify J D
inst✝¹ : J.HasSheafCompose (forget D)
inst✝ : J.PreservesSheafification (forget D)
⊢ IsLocallySurjective J
    ((J.toSheafify (P ⋙ forget D) ≫ (plusPlusIsoSheafify J (Type (max u v)) (P ⋙ forget D)).hom) ≫
      (sheafifyComposeIso J (forget D) P).hom)
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₃ : Sheaf J A
φ✝ : F₁✝ ⟶ F₂✝
ψ : F₂✝ ⟶ F₃
inst✝¹ : J.HasSheafCompose (forget A)
F₁ F₂ : Sheaf J (Type w)
φ : F₁ ⟶ F₂
inst✝ : IsLocallySurjective φ
Z : Sheaf J (Type w)
f₁ f₂ : F₂ ⟶ Z
h : φ ≫ f₁ = φ ≫ f₂
X : Cᵒᵖ
x : F₂.obj.obj X
⊢ (ConcreteCategory.hom (f₁.hom.app X)).toFun x = (ConcreteCategory.hom (f₂.hom.app X)).toFun x

Tactic:
apply (((isSheaf_iff_isSheaf_of_type _ _).1 Z.2).isSeparated _
      (Presheaf.imageSieve_mem J φ.hom x)).ext

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
F₁✝ F₂✝ F₃ : Sheaf J A
φ✝ : F₁✝ ⟶ F₂✝
ψ : F₂✝ ⟶ F₃
inst✝¹ : J.HasSheafCompose (forget A)
F₁ F₂ : Sheaf J (Type w)
φ : F₁ ⟶ F₂
inst✝ : IsLocallySurjective φ
Z : Sheaf J (Type w)
f₁ f₂ : F₂ ⟶ Z
h : φ ≫ f₁ = φ ≫ f₂
X : Cᵒᵖ
x : F₂.obj.obj X
⊢ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ unop X⦄,
    (Presheaf.imageSieve φ.hom x).arrows f →
      (ConcreteCategory.hom (Z.obj.map f.op)) ((ConcreteCategory.hom (f₁.hom.app X)).toFun x) =
        (ConcreteCategory.hom (Z.obj.map f.op)) ((ConcreteCategory.hom (f₂.hom.app X)).toFun x)