mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Goal state before:
pp: R : Type u1
inst✝³ : CommRing R
M : Type u2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
m n : ℕ
I : Type u_1
inst✝ : LinearOrder I
v : I → M
s : ↑(powersetCard I m)
t : ↑(powersetCard I n)
h : Disjoint ↑s ↑t
⊢ ιMulti_family R m v s * ιMulti_family R n v t =
    Equiv.Perm.sign (permOfDisjoint h) • ιMulti_family R (m + n) v (disjUnion h)

Tactic:
simp only [ιMulti_family, ιMulti_mul_ιMulti]
  rw [← AlternatingMap.map_perm, permOfDisjoint]
  congr
  ext i
  let e := powersetCard.orderIsoOfFin (powersetCard.disjUnion h)
  change _ = v (e (e.symm _))
  by_cases! hi : i < m
  · rw [← Fin.castAdd_castLT n i hi, Fin.append_left, OrderIso.apply_symm_apply,
      finSumFinEquiv_symm_apply_castAdd]
    aesop
  · rw [← Fin.natAdd_subNat_cast hi, Fin.append_right, OrderIso.apply_symm_apply,
      finSumFinEquiv_symm_apply_natAdd]
    aesop

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X : C
n : ℕ
inst✝ : Injective X
⊢ HasInjectiveDimensionLT X 1

Tactic:
by
  let := HasExt.standard C
  rw [hasInjectiveDimensionLT_iff]
  intro i hi Y e
  obtain _ | i := i
  · simp at hi
  · exact e.eq_zero_of_injective

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

Goal state before:
pp: case succ
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
hS : S.ShortExact
n : ℕ
h₁ : HasInjectiveDimensionLT S.X₃ n
h₂ : HasInjectiveDimensionLT S.X₂ (n + 1)
this : HasExt C := HasExt.standard C
i : ℕ
hi : n + 1 ≤ i + 1
Y : C
x₁ : Ext Y S.X₃ i
⊢ x₁.comp hS.extClass ⋯ = 0

Tactic:
rw [x₁.eq_zero_of_hasInjectiveDimensionLT n (by lia), Ext.zero_comp]

Goal state after:
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: case a
R : Type u
inst✝³ : CommRing R
n : ℕ
M : Type u_1
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Type u_4
inst✝ : LinearOrder I
v : I → M
hv : Submodule.span R (Set.range v) = ⊤
y✝ : ↑(Set.powersetCard I n)
⊢ ExteriorAlgebra.ιMulti_family R n v y✝ ∈ ↑(⋀[R]^n M)

Tactic:
rw [SetLike.mem_coe, ιMulti_family_eq_coe_comp, comp_apply]

Goal state after:
case a
R : Type u
inst✝³ : CommRing R
n : ℕ
M : Type u_1
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Type u_4
inst✝ : LinearOrder I
v : I → M
hv : Submodule.span R (Set.range v) = ⊤
y✝ : ↑(Set.powersetCard I n)
⊢ ↑(ιMulti_family R n v y✝) ∈ ⋀[R]^n M
Module: Mathlib.Algebra.Category.ModuleCat.Monoidal.Adjunction

Goal state before:
pp: R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
this : Algebra R S := f.toAlgebra
M : ModuleCat R
⊢ (ρ_ ((extendScalars f).obj M)).inv =
    (extendScalars f).map (ρ_ M).inv ≫
      (AlgebraTensorModule.distribBaseChange R S ↑M ↑(𝟙_ (ModuleCat R))).symm.toModuleIso.inv ≫
        (extendScalars f).obj M ◁ (AlgebraTensorModule.rid R S S).symm.toModuleIso.inv

Tactic:
by
        ext m
        dsimp
        rw [MonoidalCategory.rightUnitor_inv_apply]
        erw [AlgebraTensorModule.distribBaseChange_tmul,
          MonoidalCategory.whiskerLeft_apply,
          AlgebraTensorModule.rid_tmul]
        rw [one_smul]
        rfl

Goal state after:
Module: Mathlib.CategoryTheory.Products.Bifunctor

Goal state before:
pp: C : Type u₁
D : Type u₂
E : Type u₃
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Category.{v₃, u₃} E
F : C × D ⥤ E
W : C
X Y Z : D
f : X ⟶ Y
g : Y ⟶ Z
⊢ F.map (𝟙 W ×ₘ f ≫ g) = F.map ((𝟙 W ×ₘ f) ≫ (𝟙 W ×ₘ g))

Tactic:
prod_comp,

Goal state after:
C : Type u₁
D : Type u₂
E : Type u₃
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Category.{v₃, u₃} E
F : C × D ⥤ E
W : C
X Y Z : D
f : X ⟶ Y
g : Y ⟶ Z
⊢ F.map (𝟙 W ×ₘ f ≫ g) = F.map ((𝟙 W ×ₘ f).1 ≫ (𝟙 W ×ₘ g).1 ×ₘ (𝟙 W ×ₘ f).2 ≫ (𝟙 W ×ₘ g).2)
Module: Mathlib.CategoryTheory.Products.Bifunctor

Goal state before:
pp: C : Type u₁
D : Type u₂
E : Type u₃
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Category.{v₃, u₃} E
F : C × D ⥤ E
X Y Z : C
W : D
f : X ⟶ Y
g : Y ⟶ Z
⊢ F.map (f ≫ g ×ₘ 𝟙 W) = F.map ((f ×ₘ 𝟙 W) ≫ (g ×ₘ 𝟙 W))

Tactic:
prod_comp,

Goal state after:
C : Type u₁
D : Type u₂
E : Type u₃
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Category.{v₃, u₃} E
F : C × D ⥤ E
X Y Z : C
W : D
f : X ⟶ Y
g : Y ⟶ Z
⊢ F.map (f ≫ g ×ₘ 𝟙 W) = F.map ((f ×ₘ 𝟙 W).1 ≫ (g ×ₘ 𝟙 W).1 ×ₘ (f ×ₘ 𝟙 W).2 ≫ (g ×ₘ 𝟙 W).2)
Module: Mathlib.CategoryTheory.Products.Bifunctor

Goal state before:
pp: C : Type u₁
D : Type u₂
E : Type u₃
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Category.{v₃, u₃} E
F : C × D ⥤ E
X X' : C
f : X ⟶ X'
Y Y' : D
g : Y ⟶ Y'
⊢ F.map ((𝟙 X ×ₘ g) ≫ (f ×ₘ 𝟙 Y')) = F.map (f ×ₘ g)

Tactic:
prod_comp,

Goal state after:
C : Type u₁
D : Type u₂
E : Type u₃
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Category.{v₃, u₃} E
F : C × D ⥤ E
X X' : C
f : X ⟶ X'
Y Y' : D
g : Y ⟶ Y'
⊢ F.map ((𝟙 X ×ₘ g).1 ≫ (f ×ₘ 𝟙 Y').1 ×ₘ (𝟙 X ×ₘ g).2 ≫ (f ×ₘ 𝟙 Y').2) = F.map (f ×ₘ g)
Module: Mathlib.CategoryTheory.Products.Bifunctor

Goal state before:
pp: C : Type u₁
D : Type u₂
E : Type u₃
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Category.{v₃, u₃} E
F : C × D ⥤ E
X X' : C
f : X ⟶ X'
Y Y' : D
g : Y ⟶ Y'
⊢ F.map ((f ×ₘ 𝟙 Y) ≫ (𝟙 X' ×ₘ g)) = F.map (f ×ₘ g)

Tactic:
prod_comp,

Goal state after:
C : Type u₁
D : Type u₂
E : Type u₃
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Category.{v₃, u₃} E
F : C × D ⥤ E
X X' : C
f : X ⟶ X'
Y Y' : D
g : Y ⟶ Y'
⊢ F.map ((f ×ₘ 𝟙 Y).1 ≫ (𝟙 X' ×ₘ g).1 ×ₘ (f ×ₘ 𝟙 Y).2 ≫ (𝟙 X' ×ₘ g).2) = F.map (f ×ₘ g)
Module: Mathlib.CategoryTheory.Limits.IsConnected

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
c d : (j : C) × F.obj j
h : Relation.EqvGen F.ColimitTypeRel c d
⊢ Zigzag c.fst d.fst

Tactic:
induction h with
  | rel _ _ h => exact Zigzag.of_hom <| Exists.choose h
  | refl _ => exact Zigzag.refl _
  | symm _ _ _ ih => exact ih.symm
  | trans _ _ _ _ _ ih₁ ih₂ => exact ih₁.trans ih₂

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

Goal state before:
pp: case h.left
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsSifted C
c₁ c₂ : C
X : StructuredArrow (c₁, c₂) (Functor.diag C)
⊢ List.IsChain Zag [c₁, X.right, c₂]

pp: case h.right
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsSifted C
c₁ c₂ : C
X : StructuredArrow (c₁, c₂) (Functor.diag C)
⊢ [c₁, X.right, c₂].getLast ⋯ = c₂

Tactic:
· constructor
          · exact Zag.of_hom X.hom.fst
          · simpa using Zag.of_inv X.hom.snd

Goal state after:
case h.right
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsSifted C
c₁ c₂ : C
X : StructuredArrow (c₁, c₂) (Functor.diag C)
⊢ [c₁, X.right, c₂].getLast ⋯ = c₂
Module: Mathlib.CategoryTheory.Limits.Sifted

Goal state before:
pp: C : Type u
inst✝¹ : SmallCategory C
inst✝ : PreservesLimitsOfShape (Discrete (Fin 0)) colim
⊢ Nonempty C

Tactic:
suffices connected : IsConnected C by infer_instance
  rw [Types.isConnected_iff_colimit_constPUnitFunctor_iso_pUnit]
  constructor
  haveI : PreservesLimitsOfShape (Discrete PEmpty) (colim : (C ⥤ _) ⥤ Type u) :=
    preservesLimitsOfShape_of_equiv (Discrete.equivalence finZeroEquiv') _
  apply HasColimit.isoOfNatIso (_ : Types.constPUnitFunctor C ≅ (⊤_ (C ⥤ Type u))) |>.trans
  · apply PreservesTerminal.iso colim |>.trans
    exact Types.terminalIso
  · apply_rules [IsTerminal.uniqueUpToIso _ terminalIsTerminal, evaluationJointlyReflectsLimits]
    intro _
    exact isLimitChangeEmptyCone _ Types.isTerminalPUnit _ <| Iso.refl _

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsCofilteredOrEmpty C
h₁ : ∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)
h₂ : ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d), ∃ c' t, F.map t ≫ s = F.map t ≫ s'
⊢ F.Initial

Tactic:
by
  suffices ∀ d, IsCofiltered (CostructuredArrow F d) from
    initial_of_isCofiltered_costructuredArrow F
  exact fun d => isCofiltered_costructuredArrow_of_isCofiltered_of_exists F d (h₁ d) h₂

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
R : Cᵒᵖ ⥤ RingCat
⊢ (freeYoneda R).IsSeparating

Tactic:
by
  intro M N f₁ f₂ h
  ext ⟨X⟩ m
  obtain ⟨g, rfl⟩ := freeYonedaEquiv.surjective m
  exact congr_arg freeYonedaEquiv (h _ ⟨X⟩ g)

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.PartialAdjoint

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ C
X X' : F.PartialLeftAdjointSource
Y : D
f : X'.obj ⟶ F.obj Y
g : X ⟶ X'
⊢ F.partialLeftAdjointMap g ≫ F.partialLeftAdjointHomEquiv.symm f = F.partialLeftAdjointHomEquiv.symm (g.hom ≫ f)

Tactic:
rw [Equiv.eq_symm_apply, partialLeftAdjointHomEquiv_comp, partialLeftAdjointHomEquiv_map,
    assoc, ← partialLeftAdjointHomEquiv_comp, id_comp, Equiv.apply_symm_apply]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
ι : Type u_1
σ : Type u_2
Y : ι → C
f : (i : ι) → Y i ⟶ X
a : σ → ι
⊢ (ofArrows (Y ∘ a) fun i ↦ f (a i)) ≤ ofArrows Y f

Tactic:
by
  rintro - - ⟨i⟩
  use a i

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
R : Presieve X
⊢ generate R = ⊥ ↔ R = ⊥

Tactic:
by
  simp [giGenerate.gc.l_eq_bot]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
S : C
R : Sieve S
⊢ generate R.arrows = R

Tactic:
generate_sieve

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
S : C
R : Sieve S
⊢ R = R
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
S : Sieve X
f : Y ⟶ X
⊢ S.arrows f ↔ pullback f S = ⊤

Tactic:
rw [← id_mem_iff_eq_top, pullback_apply, id_comp]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : Y ⟶ X
S R : Sieve X
f : Y ⟶ X
inst✝ : IsSplitEpi f
⊢ ∀ (b : Sieve X), b ≤ pushforward f (pullback f b)

Tactic:
intro S Z g hg

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z✝ : C
f✝ : Y ⟶ X
S✝ R : Sieve X
f : Y ⟶ X
inst✝ : IsSplitEpi f
S : Sieve X
Z : C
g : Z ⟶ X
hg : S.arrows g
⊢ (pushforward f (pullback f S)).arrows g
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.Full
X Y : C
R : Sieve X
f : F.obj Y ⟶ F.obj X
x✝ : ∃ g, F.map g = f ∧ R.arrows g
g : Y ⟶ X
hcomp : F.map g = f
hg : R.arrows g
⊢ Presieve.functorPushforward F R.arrows f

Tactic:
use Y, g, 𝟙 _, hg
    simp [hcomp]

Goal state after:
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 : Y ⟶ X
inst✝ : IsIso f
ι : Type (max u₁ v₁)
Z : ι → C
g : (i : ι) → Z i ⟶ X
this : Sieve.pullback f (Sieve.ofArrows Z g) = Sieve.ofArrows Z fun i ↦ g i ≫ inv f
s : Subtype (Arrows.Compatible P fun i ↦ g i ≫ inv f)
i₁ i₂ : ι
W : C
g₁ : W ⟶ Z i₁
g₂ : W ⟶ Z i₂
h : g₁ ≫ g i₁ = g₂ ≫ g i₂
⊢ (ConcreteCategory.hom (P.map g₁.op)) ((fun i ↦ ↑s i) i₁) = (ConcreteCategory.hom (P.map g₂.op)) ((fun i ↦ ↑s i) i₂)

Tactic:
by
        replace h := h =≫ inv f
        simp only [Category.assoc] at h
        exact s.property _ _ _ _ _ h

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

Goal state before:
pp: case mp
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A' : Type u₂
inst✝² : Category.{max v₁ u₁, u₂} A'
J : GrothendieckTopology C
P' : Cᵒᵖ ⥤ A'
inst✝¹ : HasProducts A'
inst✝ : HasPullbacks C
h : IsSheaf J P'
U : C
R : Presieve U
hR : generate R ∈ J U
⊢ Nonempty (IsLimit (Fork.ofι (forkMap R P') ⋯))

Tactic:
refine ⟨?_⟩

Goal state after:
case mp
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A' : Type u₂
inst✝² : Category.{max v₁ u₁, u₂} A'
J : GrothendieckTopology C
P' : Cᵒᵖ ⥤ A'
inst✝¹ : HasProducts A'
inst✝ : HasPullbacks C
h : IsSheaf J P'
U : C
R : Presieve U
hR : generate R ∈ J U
⊢ IsLimit (Fork.ofι (forkMap R P') ⋯)
Module: Mathlib.CategoryTheory.Sites.Sheaf

Goal state before:
pp: case mpr
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A' : Type u₂
inst✝² : Category.{max v₁ u₁, u₂} A'
J : GrothendieckTopology C
P' : Cᵒᵖ ⥤ A'
inst✝¹ : HasProducts A'
inst✝ : HasPullbacks C
h : IsSheaf' J P'
U : A'
X : C
S : Sieve X
hS : S ∈ J X
⊢ Nonempty (IsLimit (Fork.ofι (Equalizer.forkMap (P' ⋙ coyoneda.obj (op U)) S.arrows) ⋯))

Tactic:
refine ⟨?_⟩

Goal state after:
case mpr
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A' : Type u₂
inst✝² : Category.{max v₁ u₁, u₂} A'
J : GrothendieckTopology C
P' : Cᵒᵖ ⥤ A'
inst✝¹ : HasProducts A'
inst✝ : HasPullbacks C
h : IsSheaf' J P'
U : A'
X : C
S : Sieve X
hS : S ∈ J X
⊢ IsLimit (Fork.ofι (Equalizer.forkMap (P' ⋙ coyoneda.obj (op U)) S.arrows) ⋯)
Module: Mathlib.CategoryTheory.Sites.Whiskering

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
A : Type u₂
inst✝⁵ : Category.{v₂, u₂} A
B : Type u₃
inst✝⁴ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U : C
R : Presieve U
F G H : A ⥤ B
η : F ⟶ G
γ : G ⟶ H
inst✝³ : J.HasSheafCompose F
inst✝² : J.HasSheafCompose G
inst✝¹ : J.HasSheafCompose H
inst✝ : F.ReflectsIsomorphisms
G₁ G₂ : Sheaf J A
f : G₁ ⟶ G₂
x✝ : IsIso ((sheafCompose J F).map f)
⊢ IsIso (((whiskeringRight Cᵒᵖ A B).obj F).map ((sheafToPresheaf J A).map f))

Tactic:
change IsIso ((sheafToPresheaf _ _).map ((sheafCompose J F).map f))

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
A : Type u₂
inst✝⁵ : Category.{v₂, u₂} A
B : Type u₃
inst✝⁴ : Category.{v₃, u₃} B
J : GrothendieckTopology C
U : C
R : Presieve U
F G H : A ⥤ B
η : F ⟶ G
γ : G ⟶ H
inst✝³ : J.HasSheafCompose F
inst✝² : J.HasSheafCompose G
inst✝¹ : J.HasSheafCompose H
inst✝ : F.ReflectsIsomorphisms
G₁ G₂ : Sheaf J A
f : G₁ ⟶ G₂
x✝ : IsIso ((sheafCompose J F).map f)
⊢ IsIso ((sheafToPresheaf J B).map ((sheafCompose J F).map f))
Module: Mathlib.CategoryTheory.Sites.CompatiblePlus

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝⁷ : Category.{v_1, u_1} D
E : Type u_2
inst✝⁶ : Category.{v_2, u_2} E
F : D ⥤ E
inst✝⁵ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁴ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝³ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ (J.plusObj P ⋙ F).map f ≫
      ((isColimitOfPreserves F (colimit.isColimit (J.diagram P (unop Y)))).coconePointUniqueUpToIso
            (colimit.isColimit (J.diagram P (unop Y) ⋙ F)) ≪≫
          HasColimit.isoOfNatIso (J.diagramCompIso F P (unop Y))).hom =
    ((isColimitOfPreserves F (colimit.isColimit (J.diagram P (unop X)))).coconePointUniqueUpToIso
            (colimit.isColimit (J.diagram P (unop X) ⋙ F)) ≪≫
          HasColimit.isoOfNatIso (J.diagramCompIso F P (unop X))).hom ≫
      (J.plusObj (P ⋙ F)).map f

Tactic:
apply (isColimitOfPreserves F (colimit.isColimit (J.diagram P X.unop))).hom_ext

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝⁷ : Category.{v_1, u_1} D
E : Type u_2
inst✝⁶ : Category.{v_2, u_2} E
F : D ⥤ E
inst✝⁵ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁴ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝³ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ ∀ (j : (J.Cover (unop X))ᵒᵖ),
    (F.mapCocone (colimit.cocone (J.diagram P (unop X)))).ι.app j ≫
        (J.plusObj P ⋙ F).map f ≫
          ((isColimitOfPreserves F (colimit.isColimit (J.diagram P (unop Y)))).coconePointUniqueUpToIso
                (colimit.isColimit (J.diagram P (unop Y) ⋙ F)) ≪≫
              HasColimit.isoOfNatIso (J.diagramCompIso F P (unop Y))).hom =
      (F.mapCocone (colimit.cocone (J.diagram P (unop X)))).ι.app j ≫
        ((isColimitOfPreserves F (colimit.isColimit (J.diagram P (unop X)))).coconePointUniqueUpToIso
                (colimit.isColimit (J.diagram P (unop X) ⋙ F)) ≪≫
              HasColimit.isoOfNatIso (J.diagramCompIso F P (unop X))).hom ≫
          (J.plusObj (P ⋙ F)).map f
Module: Mathlib.CategoryTheory.Sites.CompatiblePlus

Goal state before:
pp: C : Type u
inst✝¹⁰ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝⁹ : Category.{v_1, u_1} D
E : Type u_2
inst✝⁸ : Category.{v_2, u_2} E
inst✝⁷ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁶ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝⁵ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝⁴ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
F G : D ⥤ E
η : F ⟶ G
P : Cᵒᵖ ⥤ D
inst✝³ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst✝² : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
inst✝¹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ G
inst✝ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan G
X : Cᵒᵖ
⊢ ((J.plusObj P).whiskerLeft η ≫ (J.plusCompIso G P).hom).app X =
    ((J.plusCompIso F P).hom ≫ J.plusMap (P.whiskerLeft η)).app X

Tactic:
apply (isColimitOfPreserves F (colimit.isColimit (J.diagram P X.unop))).hom_ext

Goal state after:
C : Type u
inst✝¹⁰ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝⁹ : Category.{v_1, u_1} D
E : Type u_2
inst✝⁸ : Category.{v_2, u_2} E
inst✝⁷ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁶ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝⁵ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝⁴ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
F G : D ⥤ E
η : F ⟶ G
P : Cᵒᵖ ⥤ D
inst✝³ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
inst✝² : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
inst✝¹ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ G
inst✝ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan G
X : Cᵒᵖ
⊢ ∀ (j : (J.Cover (unop X))ᵒᵖ),
    (F.mapCocone (colimit.cocone (J.diagram P (unop X)))).ι.app j ≫
        ((J.plusObj P).whiskerLeft η ≫ (J.plusCompIso G P).hom).app X =
      (F.mapCocone (colimit.cocone (J.diagram P (unop X)))).ι.app j ≫
        ((J.plusCompIso F P).hom ≫ J.plusMap (P.whiskerLeft η)).app X
Module: Mathlib.CategoryTheory.Sites.CompatiblePlus

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝⁷ : Category.{v_1, u_1} D
E : Type u_2
inst✝⁶ : Category.{v_2, u_2} E
F : D ⥤ E
inst✝⁵ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁴ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝³ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
X : Cᵒᵖ
⊢ (whiskerRight (J.plusMap η) F ≫ (J.plusCompIso F Q).hom).app X =
    ((J.plusCompIso F P).hom ≫ J.plusMap (whiskerRight η F)).app X

Tactic:
apply (isColimitOfPreserves F (colimit.isColimit (J.diagram P X.unop))).hom_ext

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝⁷ : Category.{v_1, u_1} D
E : Type u_2
inst✝⁶ : Category.{v_2, u_2} E
F : D ⥤ E
inst✝⁵ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁴ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝³ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
X : Cᵒᵖ
⊢ ∀ (j : (J.Cover (unop X))ᵒᵖ),
    (F.mapCocone (colimit.cocone (J.diagram P (unop X)))).ι.app j ≫
        (whiskerRight (J.plusMap η) F ≫ (J.plusCompIso F Q).hom).app X =
      (F.mapCocone (colimit.cocone (J.diagram P (unop X)))).ι.app j ≫
        ((J.plusCompIso F P).hom ≫ J.plusMap (whiskerRight η F)).app X
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c✝ c : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hc : IsLimit c
⊢ IsLimit (coneOfConeForget c)

Tactic:
refine IsLimit.ofFaithful forget (ht := hc)
    (fun s ↦ ofHom (ContinuousMap.mk (hc.lift ((forget).mapCone s)) ?_)) (fun _ ↦ rfl)
  rw [continuous_iff_coinduced_le]
  dsimp [topologicalSpaceConePtOfConeForget]
  rw [le_iInf_iff]
  intro j
  rw [coinduced_le_iff_le_induced, induced_compose]
  convert! continuous_iff_le_induced.1 (s.π.app j).hom.continuous
  ext x
  exact ConcreteCategory.hom_ext_iff.mp (hc.fac ((forget).mapCone s) j) x

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

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cocone F
hc : IsColimit c
X : Set ↑c.pt
⊢ TopologicalSpace.IsOpen X ↔ ∀ (j : J), IsOpen (⇑(ConcreteCategory.hom (c.ι.app j)) ⁻¹' X)

Tactic:
simp only [← isOpen_coinduced]

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cocone F
hc : IsColimit c
X : Set ↑c.pt
⊢ TopologicalSpace.IsOpen X ↔ ∀ (j : J), IsOpen X
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: case mp
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✝ ∈ Set.range ⇑(ConcreteCategory.hom (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)) →
    x✝ ∈
      ⇑(ConcreteCategory.hom (pullback.fst g₁ g₂)) ⁻¹' Set.range ⇑(ConcreteCategory.hom i₁) ∩
        ⇑(ConcreteCategory.hom (pullback.snd g₁ g₂)) ⁻¹' Set.range ⇑(ConcreteCategory.hom i₂)

pp: case mpr
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✝ ∈
      ⇑(ConcreteCategory.hom (pullback.fst g₁ g₂)) ⁻¹' Set.range ⇑(ConcreteCategory.hom i₁) ∩
        ⇑(ConcreteCategory.hom (pullback.snd g₁ g₂)) ⁻¹' Set.range ⇑(ConcreteCategory.hom i₂) →
    x✝ ∈ Set.range ⇑(ConcreteCategory.hom (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂))

Tactic:
· rintro ⟨y, rfl⟩
    simp only [Set.mem_inter_iff, Set.mem_preimage, Set.mem_range]
    rw [← ConcreteCategory.comp_apply, ← ConcreteCategory.comp_apply]
    simp only [limit.lift_π, PullbackCone.mk_π_app]
    exact ⟨exists_apply_eq_apply _ _, exists_apply_eq_apply _ _⟩

Goal state after:
case mpr
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✝ ∈
      ⇑(ConcreteCategory.hom (pullback.fst g₁ g₂)) ⁻¹' Set.range ⇑(ConcreteCategory.hom i₁) ∩
        ⇑(ConcreteCategory.hom (pullback.snd g₁ g₂)) ⁻¹' Set.range ⇑(ConcreteCategory.hom i₂) →
    x✝ ∈ Set.range ⇑(ConcreteCategory.hom (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂))