mathlib-initiative/mathlib-tactics huggingface dataset:
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)
H :
  ∀ {Z : C} (p₁ p₂ : Z ⟶ X),
    p₁ ≫ f = p₂ ≫ f → (ConcreteCategory.hom (P.map p₁.op)) (x f ⋯) = (ConcreteCategory.hom (P.map p₂.op)) (x f ⋯)
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ Y
f₂ : Y₂ ⟶ Y
⊢ ∀ (h₁ : singleton f f₁) (h₂ : singleton f f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ → (ConcreteCategory.hom (P.map g₁.op)) (x f₁ h₁) = (ConcreteCategory.hom (P.map g₂.op)) (x f₂ h₂)

Tactic:
rintro ⟨rfl⟩ ⟨rfl⟩ h

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X Y✝¹ : C
f : X ⟶ Y✝¹
x : FamilyOfElements P (singleton f)
H :
  ∀ {Z : C} (p₁ p₂ : Z ⟶ X),
    p₁ ≫ f = p₂ ≫ f → (ConcreteCategory.hom (P.map p₁.op)) (x f ⋯) = (ConcreteCategory.hom (P.map p₂.op)) (x f ⋯)
Z Y✝ : C
g₁ : Z ⟶ X
Y : C
g₂ : Z ⟶ X
h : g₁ ≫ f = g₂ ≫ f
⊢ (ConcreteCategory.hom (P.map g₁.op)) (x f ⋯) = (ConcreteCategory.hom (P.map g₂.op)) (x f ⋯)
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
S : Presieve X
R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → Sieve Y
f : Y ⟶ X
h : S f
⊢ R h ≤ pullback f (bind S R)

Tactic:
rw [← galoisConnection f]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
S : Presieve X
R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → Sieve Y
f : Y ⟶ X
h : S f
⊢ pushforward f (R h) ≤ bind S R
Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.HasPairwisePullbacks
a : Presieve.FamilyOfElements P R
| (ConcreteCategory.hom (firstObjEqFamily P R).hom) ((firstObjEqFamily P R).toEquiv.symm a)

Tactic:
← Iso.toEquiv_apply

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
inst✝ : R.HasPairwisePullbacks
a : Presieve.FamilyOfElements P R
| (firstObjEqFamily P R).toEquiv ((firstObjEqFamily P R).toEquiv.symm a)
Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Goal state before:
pp: case mp
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type w
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).HasPairwisePullbacks
x : FirstObj P X
⊢ Arrows.PullbackCompatible P π ((ConcreteCategory.hom (Types.productIso fun i ↦ P.obj (op (X i))).hom) x) →
    (ConcreteCategory.hom (firstMap P X π)) x = (ConcreteCategory.hom (secondMap P X π)) x

pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type w
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).HasPairwisePullbacks
x : FirstObj P X
⊢ (ConcreteCategory.hom (firstMap P X π)) x = (ConcreteCategory.hom (secondMap P X π)) x →
    Arrows.PullbackCompatible P π ((ConcreteCategory.hom (Types.productIso fun i ↦ P.obj (op (X i))).hom) x)

Tactic:
· intro t
    ext ij
    simpa [firstMap, secondMap] using t ij.1 ij.2

Goal state after:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type w
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).HasPairwisePullbacks
x : FirstObj P X
⊢ (ConcreteCategory.hom (firstMap P X π)) x = (ConcreteCategory.hom (secondMap P X π)) x →
    Arrows.PullbackCompatible P π ((ConcreteCategory.hom (Types.productIso fun i ↦ P.obj (op (X i))).hom) x)
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₂
inst✝ : Category.{v₂, u₂} A
E : A
X : C
P : Cᵒᵖ ⥤ A
hP : IsSheaf J P
S : J.Cover X
x : (I : S.Arrow) → E ⟶ P.obj (op I.Y)
hx : ∀ ⦃I₁ I₂ : S.Arrow⦄ (r : I₁.Relation I₂), x I₁ ≫ P.map r.g₁.op = x I₂ ≫ P.map r.g₂.op
I : S.Arrow
⊢ hP.amalgamate S x hx ≫ P.map I.f.op = x I

Tactic:
apply (hP _ _ S.condition).valid_glue

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

Goal state before:
pp: case left
C : Type u
inst✝¹ : Category.{v, u} C
F F' F'' : C ⥤ Type w
p : F' ⟶ F
inst✝ : Mono p
this : Mono (toRange p)
i : C
⊢ Function.Injective ⇑(ConcreteCategory.hom ((toRange p).app i))

Tactic:
rw [← mono_iff_injective]
    infer_instance

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ J U
x : Presieve.FamilyOfElements (sheafify J G).toFunctor S.arrows
hx : x.Compatible
S' : Sieve U := Sieve.bind S.arrows fun Y f hf ↦ G.sieveOfSection ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i),
    (ConcreteCategory.hom (F.map (i₁ V i hi).op)) ↑(x (i₂ V i hi) ⋯) ∈ G.obj (op V)
h₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi ↦ (ConcreteCategory.hom (F.map (i₁ V i hi).op)) ↑(x (i₂ V i hi) ⋯)
s : (sheafify J G).toFunctor.obj (op U)
H : x''.IsAmalgamation ↑s
V : C
i : V ⟶ U
hi : S.arrows i
V' : C
⊢ ∀ ⦃f : V' ⟶ unop (op V)⦄,
    (G.sieveOfSection ↑(x i hi)).arrows f →
      (ConcreteCategory.hom (F.map f.op)) ↑((ConcreteCategory.hom ((sheafify J G).toFunctor.map i.op)) s) =
        (ConcreteCategory.hom (F.map f.op)) ↑(x i hi)

Tactic:
i'

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ J U
x : Presieve.FamilyOfElements (sheafify J G).toFunctor S.arrows
hx : x.Compatible
S' : Sieve U := Sieve.bind S.arrows fun Y f hf ↦ G.sieveOfSection ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i),
    (ConcreteCategory.hom (F.map (i₁ V i hi).op)) ↑(x (i₂ V i hi) ⋯) ∈ G.obj (op V)
h₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi ↦ (ConcreteCategory.hom (F.map (i₁ V i hi).op)) ↑(x (i₂ V i hi) ⋯)
s : (sheafify J G).toFunctor.obj (op U)
H : x''.IsAmalgamation ↑s
V : C
i : V ⟶ U
hi : S.arrows i
V' : C
i' : V' ⟶ unop (op V)
⊢ (G.sieveOfSection ↑(x i hi)).arrows i' →
    (ConcreteCategory.hom (F.map i'.op)) ↑((ConcreteCategory.hom ((sheafify J G).toFunctor.map i.op)) s) =
      (ConcreteCategory.hom (F.map i'.op)) ↑(x i hi)
Module: Mathlib.CategoryTheory.Sites.Subsheaf

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subfunctor F
hF : Presieve.IsSheaf J F
U : C
S : Sieve U
hS : S ∈ J U
x : Presieve.FamilyOfElements (sheafify J G).toFunctor S.arrows
hx : x.Compatible
S' : Sieve U := Sieve.bind S.arrows fun Y f hf ↦ G.sieveOfSection ↑(x f hf)
W : (V : C) → (i : V ⟶ U) → S'.arrows i → C
i₁ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → V ⟶ W V i hi
i₂ : (V : C) → (i : V ⟶ U) → (hi : S'.arrows i) → W V i hi ⟶ U
hi₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), S.arrows (i₂ V i hi)
h₁ :
  ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i),
    (ConcreteCategory.hom (F.map (i₁ V i hi).op)) ↑(x (i₂ V i hi) ⋯) ∈ G.obj (op V)
h₂ : ∀ (V : C) (i : V ⟶ U) (hi : S'.arrows i), i₁ V i hi ≫ i₂ V i hi = i
x'' : Presieve.FamilyOfElements F S'.arrows :=
  fun V i hi ↦ (ConcreteCategory.hom (F.map (i₁ V i hi).op)) ↑(x (i₂ V i hi) ⋯)
s : (sheafify J G).toFunctor.obj (op U)
H : x''.IsAmalgamation ↑s
V : C
i : V ⟶ U
hi : S.arrows i
V' : C
i' : V' ⟶ unop (op V)
hi' : (G.sieveOfSection ↑(x i hi)).arrows i'
hi'' : S'.arrows (i' ≫ i)
this : (ConcreteCategory.hom (F.map i.op ≫ F.map i'.op)) ↑s = x'' (i' ≫ i) hi''
⊢ (ConcreteCategory.hom (F.map i'.op)) ↑((ConcreteCategory.hom ((sheafify J G).toFunctor.map i.op)) s) =
    (ConcreteCategory.hom (F.map i'.op)) ↑(x i hi)

Tactic:
exact this.trans (congr_arg Subtype.val (hx _ _ (hi₂ _ _ hi'') hi (h₂ _ _ hi'')))

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

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F F' F'' : Cᵒᵖ ⥤ Type w
G G' : Subfunctor F
f : G.toFunctor ⟶ F'
h : Presieve.IsSheaf J F'
U V : Cᵒᵖ
i : U ⟶ V
s : (sheafify J G).toFunctor.obj U
W : C
j : W ⟶ unop V
hj : (G.sieveOfSection ↑((ConcreteCategory.hom ((sheafify J G).toFunctor.map i)) s)).arrows j
⊢ (ConcreteCategory.hom (f.app (op W)))
      (G.familyOfElementsOfSection (↑({ toFun := fun x ↦ ⟨(ConcreteCategory.hom (F.map i)) ↑x, ⋯⟩ } s)) j hj) =
    (G.familyOfElementsOfSection ↑s).map f (j ≫ i.unop) ?refine_2

Tactic:
simp [Presieve.FamilyOfElements.map, Subfunctor.familyOfElementsOfSection]
      rfl

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type u_1
R S : Sieve X
hR : IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun Y f x ↦ Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : S.arrows f
⊢ Sieve.pullback f (Sieve.bind R.arrows fun T k x ↦ Sieve.pullback k S) = Sieve.pullback f R

Tactic:
ext Z g

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
P : Cᵒᵖ ⥤ Type u_1
R S : Sieve X
hR : IsSheafFor P R.arrows
hR' : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → IsSeparatedFor P (Sieve.pullback f R).arrows
hS : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R.arrows f → IsSheafFor P (Sieve.pullback f S).arrows
this : (Sieve.bind R.arrows fun Y f x ↦ Sieve.pullback f S).arrows ≤ S.arrows
Y : C
f : Y ⟶ X
hf : S.arrows f
Z : C
g : Z ⟶ Y
⊢ (Sieve.pullback f (Sieve.bind R.arrows fun T k x ↦ Sieve.pullback k S)).arrows g ↔ (Sieve.pullback f R).arrows g
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
S : Cone F
m : S.pt ⟶ (limitCone F).pt
h : ∀ (j : J), m ≫ (limitCone F).π.app j = S.π.app j
⊢ m = ofHom { toFun := fun x ↦ ⟨fun x_1 ↦ (ConcreteCategory.hom (S.π.app x_1)) x, ⋯⟩, continuous_toFun := ⋯ }

Tactic:
by
    ext a
    simp [← h]
    rfl

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

Goal state before:
pp: X Y S : TopCat
f : X ⟶ S
H : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
g : Y ⟶ S
⊢ IsOpenEmbedding ⇑(ConcreteCategory.hom (pullback.snd f g))

Tactic:
convert!
    (homeoOfIso (asIso (pullback.snd (𝟙 S) g))).isOpenEmbedding.comp
      (pullback_map_isOpenEmbedding (i₂ := 𝟙 Y) f g (𝟙 _) g H
        (homeoOfIso (Iso.refl _)).isOpenEmbedding (𝟙 _) rfl (by simp))

Goal state after:
X Y S : TopCat
f : X ⟶ S
H : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
g : Y ⟶ S
⊢ ⇑(ConcreteCategory.hom (pullback.snd f g)) =
    ⇑(homeoOfIso (asIso (pullback.snd (𝟙 S) g))) ∘ ⇑(ConcreteCategory.hom (pullback.map f g (𝟙 S) g f (𝟙 Y) (𝟙 S) ⋯ ⋯))
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
hg : IsEmbedding ⇑(ConcreteCategory.hom g)
H : Set.range ⇑(ConcreteCategory.hom f) ⊆ Set.range ⇑(ConcreteCategory.hom g)
⊢ IsIso (pullback.fst f g)

Tactic:
by
  let esto : (pullback f g : TopCat) ≃ₜ X :=
    (fst_isEmbedding_of_right f hg).toHomeomorph.trans
      { toFun := Subtype.val
        invFun := fun x =>
          ⟨x, by
            rw [pullback_fst_range]
            exact ⟨_, (H (Set.mem_range_self x)).choose_spec.symm⟩⟩ }
  convert! (isoOfHomeo esto).isIso_hom

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : MonoCoprod C
I : Type u_2
J : Type u_3
X : I → C
ι : J → I
hι : Function.Injective ι
c : Cofan X
c₁ : Cofan (X ∘ ι)
hc : IsColimit c
hc₁ : IsColimit c₁
c₂ : Cofan fun k ↦ X ↑k
hc₂ : IsColimit c₂
⊢ Mono (Cofan.IsColimit.desc hc₁ fun i ↦ c.inj (ι i))

Tactic:
classical
  let e := ((Equiv.ofInjective ι hι).sumCongr (Equiv.refl _)).trans (Equiv.Set.sumCompl _)
  refine mono_binaryCofanSum_inl' (Cofan.mk c.pt (fun i' => c.inj (e i'))) _ _ ?_
    hc₁ hc₂ _ (by simp [e])
  exact IsColimit.ofIsoColimit ((IsColimit.ofCoconeEquiv (Cocone.equivalenceOfReindexing
    (Discrete.equivalence e) (Iso.refl _))).symm hc) (Cocone.ext (Iso.refl _))

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

Goal state before:
pp: case mpr
X Y : TopCat
c : BinaryCofan X Y
⊢ IsOpenEmbedding ⇑(ConcreteCategory.hom c.inl) ∧
      IsOpenEmbedding ⇑(ConcreteCategory.hom c.inr) ∧
        IsCompl (range ⇑(ConcreteCategory.hom c.inl)) (range ⇑(ConcreteCategory.hom c.inr)) →
    Nonempty (IsColimit c)

Tactic:
· rintro ⟨h₁, h₂, h₃⟩
      have : ∀ x, x ∈ Set.range c.inl ∨ x ∈ Set.range c.inr := by
        rw [eq_compl_iff_isCompl.mpr h₃.symm]
        exact fun _ => or_not
      refine ⟨BinaryCofan.IsColimit.mk _ ?_ ?_ ?_ ?_⟩
      · intro T f g
        refine ofHom (ContinuousMap.mk ?_ ?_)
        · exact fun x =>
            if h : x ∈ Set.range c.inl then f ((Equiv.ofInjective _ h₁.injective).symm ⟨x, h⟩)
            else g ((Equiv.ofInjective _ h₂.injective).symm ⟨x, (this x).resolve_left h⟩)
        rw [continuous_iff_continuousAt]
        intro x
        by_cases h : x ∈ Set.range c.inl
        · revert h x
          apply (IsOpen.continuousOn_iff _).mp
          · rw [continuousOn_iff_continuous_domRestrict]
            convert_to Continuous (f ∘ h₁.isEmbedding.toHomeomorph.symm)
            · ext ⟨x, hx⟩
              exact dif_pos hx
            fun_prop
          · exact h₁.isOpen_range
        · revert h x
          simp only [← mem_compl_iff]
          apply (IsOpen.continuousOn_iff _).mp
          · rw [continuousOn_iff_continuous_domRestrict]
            have : ∀ a, a ∉ Set.range c.inl → a ∈ Set.range c.inr := by
              rintro a (h : a ∈ (Set.range c.inl)ᶜ)
              rwa [eq_compl_iff_isCompl.mpr h₃.symm]
            convert_to! Continuous
                (g ∘ h₂.isEmbedding.toHomeomorph.symm ∘ Subtype.map _ this)
            · ext ⟨x, hx⟩
              exact dif_neg hx
            apply Continuous.comp
            · exact g.hom.continuous_toFun
            · apply Continuous.comp (by fun_prop)
              rw [IsEmbedding.subtypeVal.isInducing.continuous_iff]
              exact continuous_subtype_val
          · change IsOpen (Set.range c.inl)ᶜ
            rw [← eq_compl_iff_isCompl.mpr h₃.symm]
            exact h₂.isOpen_range
      · intro T f g
        ext x
        simp
      · intro T f g
        ext x
        dsimp
        rw [dif_neg]
        · exact congr_arg g (Equiv.ofInjective_symm_apply _ _)
        · rintro ⟨y, e⟩
          have : c.inr x ∈ Set.range c.inl ⊓ Set.range c.inr := ⟨⟨_, e⟩, ⟨_, rfl⟩⟩
          rwa [disjoint_iff.mp h₃.1] at this
      · rintro T _ _ m rfl rfl
        ext x
        change m x = dite _ _ _
        split_ifs <;> exact congr_arg _ (Equiv.apply_ofInjective_symm _ ⟨_, _⟩).symm

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

Goal state before:
pp: case mp
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
X' Y' Z' : C
h' : X' ⟶ Z'
⊢ ∀ (i' : Y' ⟶ Z') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (αZ : Z' ⟶ Z),
    CommSq h' αX αZ h →
      CommSq i' αY αZ i →
        ∀ [HasPullback αX f],
          IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i ↔
            ∃ W' f' g' αW, IsPullback f' αW αX f ∧ IsPullback g' αW αY g ∧ IsPushout f' g' h' i'

Tactic:
i'

Goal state after:
case mp
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
X' Y' Z' : C
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
⊢ ∀ (αX : X' ⟶ X) (αY : Y' ⟶ Y) (αZ : Z' ⟶ Z),
    CommSq h' αX αZ h →
      CommSq i' αY αZ i →
        ∀ [HasPullback αX f],
          IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i ↔
            ∃ W' f' g' αW, IsPullback f' αW αX f ∧ IsPullback g' αW αY g ∧ IsPushout f' g' h' i'
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: case mpr
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' :
  ∀ ⦃X' Y' Z' : C⦄ (h' : X' ⟶ Z') (i' : Y' ⟶ Z') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (αZ : Z' ⟶ Z),
    CommSq h' αX αZ h →
      CommSq i' αY αZ i →
        ∀ [HasPullback αX f],
          IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i ↔
            ∃ W' f' g' αW, IsPullback f' αW αX f ∧ IsPullback g' αW αY g ∧ IsPushout f' g' 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),
    IsPullback f' αW αX f →
      IsPullback g' αW αY g →
        CommSq h' αX αZ h →
          CommSq i' αY αZ i →
            CommSq f' g' h' i' → (IsPushout f' g' h' i' ↔ IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i)

Tactic:
i'

Goal state after:
case mpr
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' :
  ∀ ⦃X' Y' Z' : C⦄ (h' : X' ⟶ Z') (i' : Y' ⟶ Z') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (αZ : Z' ⟶ Z),
    CommSq h' αX αZ h →
      CommSq i' αY αZ i →
        ∀ [HasPullback αX f],
          IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i ↔
            ∃ W' f' g' αW, IsPullback f' αW αX f ∧ IsPullback g' αW αY g ∧ IsPushout f' g' 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),
    IsPullback f' αW αX f →
      IsPullback g' αW αY g →
        CommSq h' αX αZ h →
          CommSq i' αY αZ i →
            CommSq f' g' h' i' → (IsPushout f' g' h' i' ↔ IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i)
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: case refine_2.convert_6
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.{v, v, 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'
hr : IsColimit (Gl.mapCocone (colimit.cocone (F' ⋙ Gr))) := isColimitOfPreserves Gl (colimit.isColimit (F' ⋙ Gr))
this✝¹ : α.app j = β.inv.app j ≫ Gl.map (Gr.map (α'.app j))
this✝ :
  f =
    (hl.coconePointUniqueUpToIso hr).hom ≫ Gl.map (colimit.desc (F' ⋙ Gr) { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι })
this :
  IsPullback (Gl.map ((colimit.cocone (F' ⋙ Gr)).ι.app j)) (Gl.map ((whiskerRight α' Gr).app j))
    (Gl.map (colimit.desc (F' ⋙ Gr) { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι })) (Gl.map (c.ι.app j))
⊢ (β.hom.app j ≫ c'.ι.app j) ≫ (hl.coconePointUniqueUpToIso hr).hom = Gl.map ((colimit.cocone (F' ⋙ Gr)).ι.app j)

Tactic:
exact IsColimit.comp_coconePointUniqueUpToIso_hom hl hr _

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

Goal state before:
pp: case left
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
H : IsUniversalColimit (BinaryCofan.mk (𝟙 (⊥_ C)) (𝟙 (⊥_ C)))
A : C
f : A ⟶ ⊥_ C
⊢ IsPullback (𝟙 A) f f (𝟙 (⊥_ C))

Tactic:
exact IsPullback.of_horiz_isIso ⟨(Category.id_comp _).trans (Category.comp_id _).symm⟩

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

Goal state before:
pp: case right
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasInitial C
H : IsUniversalColimit (BinaryCofan.mk (𝟙 (⊥_ C)) (𝟙 (⊥_ C)))
A : C
f : A ⟶ ⊥_ C
⊢ IsPullback (𝟙 A) f f (𝟙 (⊥_ C))

Tactic:
exact IsPullback.of_horiz_isIso ⟨(Category.id_comp _).trans (Category.comp_id _).symm⟩

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

Goal state before:
pp: case mp
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
a✝ : J.PreservesSheafification F
P : Cᵒᵖ ⥤ A
⊢ J.W (adj₁.unit.app P)

Tactic:
rw [J.W_iff_isIso_map_of_adjunction adj₁]

Goal state after:
case mp
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
a✝ : J.PreservesSheafification F
P : Cᵒᵖ ⥤ A
⊢ IsIso (G₁.map (adj₁.unit.app P))
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₃
inst✝¹ : IsLocallyInjective J φ
inst✝ : IsLocallyInjective J ψ
X : Cᵒᵖ
x y : ToType (F₁.obj X)
h : (ConcreteCategory.hom ((φ ≫ ψ).app X)) x = (ConcreteCategory.hom ((φ ≫ ψ).app X)) y
⊢ (ConcreteCategory.hom (ψ.app X)) ((ConcreteCategory.hom (φ.app X)) x) =
    (ConcreteCategory.hom (ψ.app X)) ((ConcreteCategory.hom (φ.app X)) y)

Tactic:
by simpa using 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 : Cᵒᵖ ⥤ Type (max u v)
⊢ (Subfunctor.sheafify J (Subfunctor.range (J.toSheafify F))).ι ≫
      J.sheafifyLift (Subfunctor.toRangeSheafify J (J.toSheafify F)) ⋯ =
    𝟙 (Subfunctor.sheafify J (Subfunctor.range (J.toSheafify F))).toFunctor

Tactic:
rw [← cancel_mono (Subfunctor.ι _), Category.id_comp, Category.assoc]

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 : Cᵒᵖ ⥤ Type (max u v)
⊢ (Subfunctor.sheafify J (Subfunctor.range (J.toSheafify F))).ι ≫
      J.sheafifyLift (Subfunctor.toRangeSheafify J (J.toSheafify F)) ⋯ ≫
        (Subfunctor.sheafify J (Subfunctor.range (J.toSheafify F))).ι =
    (Subfunctor.sheafify J (Subfunctor.range (J.toSheafify F))).ι