mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S : C
E✝¹ E✝ : PreOneHypercover S
F✝ : PreOneHypercover S
G✝ : PreOneHypercover S
E F : PreOneHypercover S
f : E ≅ F
G : Cᵒᵖ ⥤ A
⊢ (E.multicospanIndex G).multicospan ≅ (equivalenceMulticospanOfIso f).functor ⋙ (F.multicospanIndex G).multicospan

Tactic:
refine WalkingMulticospan.functorExt ?_ ?_ ?_ ?_

Goal state after:
case refine_1.refine_1
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S : C
E✝¹ E✝ : PreOneHypercover S
F✝ : PreOneHypercover S
G✝ : PreOneHypercover S
E F : PreOneHypercover S
f : E ≅ F
G : Cᵒᵖ ⥤ A
⊢ (i : E.multicospanShape.L) →
    (E.multicospanIndex G).multicospan.obj (WalkingMulticospan.left i) ≅
      ((equivalenceMulticospanOfIso f).functor ⋙ (F.multicospanIndex G).multicospan).obj (WalkingMulticospan.left i)

case refine_1.refine_2
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S : C
E✝¹ E✝ : PreOneHypercover S
F✝ : PreOneHypercover S
G✝ : PreOneHypercover S
E F : PreOneHypercover S
f : E ≅ F
G : Cᵒᵖ ⥤ A
⊢ (i : E.multicospanShape.R) →
    (E.multicospanIndex G).multicospan.obj (WalkingMulticospan.right i) ≅
      ((equivalenceMulticospanOfIso f).functor ⋙ (F.multicospanIndex G).multicospan).obj (WalkingMulticospan.right i)

case refine_1.refine_3
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S : C
E✝¹ E✝ : PreOneHypercover S
F✝ : PreOneHypercover S
G✝ : PreOneHypercover S
E F : PreOneHypercover S
f : E ≅ F
G : Cᵒᵖ ⥤ A
⊢ ∀ (i : E.multicospanShape.R),
    (E.multicospanIndex G).multicospan.map (WalkingMulticospan.Hom.fst i) ≫ Iso.hom (?refine_1.refine_2 i) =
      Iso.hom (?refine_1.refine_1 (E.multicospanShape.fst i)) ≫
        ((equivalenceMulticospanOfIso f).functor ⋙ (F.multicospanIndex G).multicospan).map
          (WalkingMulticospan.Hom.fst i)

case refine_1.refine_4
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u_1
inst✝ : Category.{v_1, u_1} A
S : C
E✝¹ E✝ : PreOneHypercover S
F✝ : PreOneHypercover S
G✝ : PreOneHypercover S
E F : PreOneHypercover S
f : E ≅ F
G : Cᵒᵖ ⥤ A
⊢ ∀ (i : E.multicospanShape.R),
    (E.multicospanIndex G).multicospan.map (WalkingMulticospan.Hom.snd i) ≫ Iso.hom (?refine_1.refine_2 i) =
      Iso.hom (?refine_1.refine_1 (E.multicospanShape.snd i)) ≫
        ((equivalenceMulticospanOfIso f).functor ⋙ (F.multicospanIndex G).multicospan).map
          (WalkingMulticospan.Hom.snd i)
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators

Goal state before:
pp: C : Type u'
inst✝² : Category.{v', u'} C
J : GrothendieckTopology C
R : Sheaf J RingCat
inst✝¹ : HasWeakSheafify J AddCommGrpCat
inst✝ : J.WEqualsLocallyBijective AddCommGrpCat
M N P : SheafOfModules R
e : M ≅ N
σ : N.GeneratingSections
⊢ (fun σ ↦ σ.ofEpi e.hom) ((fun σ ↦ σ.ofEpi e.inv) σ) = σ

Tactic:
by
    dsimp
    simp only [← opEpi_comp, e.inv_hom_id, opEpi_id]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.One

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X : C
E : PreZeroHypercover X
inst✝ : E.HasPullbacks
F : (i j : E.I₀) → PreZeroHypercover (pullback (E.f i) (E.f j))
i j : E.I₀
⊢ (Sieve.ofArrows (E.refineOneHypercover F).Y fun j_1 ↦ (E.refineOneHypercover F).toPullback j_1) = (F i j).sieve₀

Tactic:
congr

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X : C
E : PreZeroHypercover X
inst✝ : E.HasPullbacks
F : (i j : E.I₀) → PreZeroHypercover (pullback (E.f i) (E.f j))
i j : E.I₀
⊢ (fun j_1 ↦ (E.refineOneHypercover F).toPullback j_1) = (F i j).f
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J✝ J : GrothendieckTopology C
X : C
Y : Over X
E : (J.over X).OneHypercover Y
⊢ E.IsPreservedBy (Over.forget X) J

Tactic:
refine ⟨?_, ?_⟩

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
J✝ J : GrothendieckTopology C
X : C
Y : Over X
E : (J.over X).OneHypercover Y
⊢ (E.map (Over.forget X)).sieve₀ ∈ J ((Over.forget X).obj Y)

case refine_2
C : Type u
inst✝ : Category.{v, u} C
J✝ J : GrothendieckTopology C
X : C
Y : Over X
E : (J.over X).OneHypercover Y
⊢ ∀ (i₁ i₂ : E.I₀) ⦃W : C⦄ (p₁ : W ⟶ (Over.forget X).obj (E.X i₁)) (p₂ : W ⟶ (Over.forget X).obj (E.X i₂)),
    p₁ ≫ (Over.forget X).map (E.f i₁) = p₂ ≫ (Over.forget X).map (E.f i₂) → (E.map (Over.forget X)).sieve₁ p₁ p₂ ∈ J W
Module: Mathlib.CategoryTheory.Sites.Over

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
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
X : C
inst✝ : F.PreservesOneHypercovers J K
Y : Over X
E : (J.over X).OneHypercover Y
E' : K.OneHypercover (F.obj ((Over.forget X).obj Y)) := (E.map (Over.forget X) J).map F K
⊢ E.IsPreservedBy (Over.post F) (K.over (F.obj X))

Tactic:
refine ⟨?_, ?_⟩

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
J✝ : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
X : C
inst✝ : F.PreservesOneHypercovers J K
Y : Over X
E : (J.over X).OneHypercover Y
E' : K.OneHypercover (F.obj ((Over.forget X).obj Y)) := (E.map (Over.forget X) J).map F K
⊢ (E.map (Over.post F)).sieve₀ ∈ (K.over (F.obj X)) ((Over.post F).obj Y)

case refine_2
C : Type u
inst✝² : Category.{v, u} C
J✝ : GrothendieckTopology C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
X : C
inst✝ : F.PreservesOneHypercovers J K
Y : Over X
E : (J.over X).OneHypercover Y
E' : K.OneHypercover (F.obj ((Over.forget X).obj Y)) := (E.map (Over.forget X) J).map F K
⊢ ∀ (i₁ i₂ : E.I₀) ⦃W : Over (F.obj X)⦄ (p₁ : W ⟶ (Over.post F).obj (E.X i₁)) (p₂ : W ⟶ (Over.post F).obj (E.X i₂)),
    p₁ ≫ (Over.post F).map (E.f i₁) = p₂ ≫ (Over.post F).map (E.f i₂) →
      (E.map (Over.post F)).sieve₁ p₁ p₂ ∈ (K.over (F.obj X)) W
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
X Y : C
f : X ⟶ Y
x✝¹ : Sheaf (J.over Y) A
x✝ : (Over X)ᵒᵖ
⊢ x✝¹.obj.map
      ((Over.mapId Y).inv.app ((Over.map f).obj (Opposite.unop x✝)) ≫
          (Over.mapComp f (𝟙 Y)).inv.app (Opposite.unop x✝)).op =
    x✝¹.obj.map ((Over.mapCongr (f ≫ 𝟙 Y) f ⋯).inv.app (Opposite.unop x✝)).op

Tactic:
congr

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
X Y : C
f : X ⟶ Y
x✝¹ : Sheaf (J.over Y) A
x✝ : (Over X)ᵒᵖ
⊢ (Over.mapId Y).inv.app ((Over.map f).obj (Opposite.unop x✝)) ≫ (Over.mapComp f (𝟙 Y)).inv.app (Opposite.unop x✝) =
    (Over.mapCongr (f ≫ 𝟙 Y) f ⋯).inv.app (Opposite.unop x✝)
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
X Y : C
f : X ⟶ Y
x✝¹ : Sheaf (J.over Y) A
x✝ : (Over X)ᵒᵖ
⊢ x✝¹.obj.map
      ((Over.map f).map ((Over.mapId X).inv.app (Opposite.unop x✝)) ≫
          (Over.mapComp (𝟙 X) f).inv.app (Opposite.unop x✝)).op =
    x✝¹.obj.map ((Over.mapCongr (𝟙 X ≫ f) f ⋯).inv.app (Opposite.unop x✝)).op

Tactic:
congr

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
X Y : C
f : X ⟶ Y
x✝¹ : Sheaf (J.over Y) A
x✝ : (Over X)ᵒᵖ
⊢ (Over.map f).map ((Over.mapId X).inv.app (Opposite.unop x✝)) ≫ (Over.mapComp (𝟙 X) f).inv.app (Opposite.unop x✝) =
    (Over.mapCongr (𝟙 X ≫ f) f ⋯).inv.app (Opposite.unop x✝)
Module: Mathlib.CategoryTheory.Sites.Over

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
X Y Z T : C
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ T
x✝¹ : Sheaf (J.over T) A
x✝ : (Over X)ᵒᵖ
⊢ x✝¹.obj.map
      ((Over.mapComp (f ≫ g) h).hom.app (Opposite.unop x✝) ≫
          (Over.map h).map ((Over.mapComp f g).hom.app (Opposite.unop x✝)) ≫
            (Over.mapComp g h).inv.app ((Over.map f).obj (Opposite.unop x✝)) ≫
              (Over.mapComp f (g ≫ h)).inv.app (Opposite.unop x✝)).op =
    x✝¹.obj.map ((Over.mapCongr (f ≫ g ≫ h) ((f ≫ g) ≫ h) ⋯).inv.app (Opposite.unop x✝)).op

Tactic:
congr

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
X Y Z T : C
f : X ⟶ Y
g : Y ⟶ Z
h : Z ⟶ T
x✝¹ : Sheaf (J.over T) A
x✝ : (Over X)ᵒᵖ
⊢ (Over.mapComp (f ≫ g) h).hom.app (Opposite.unop x✝) ≫
      (Over.map h).map ((Over.mapComp f g).hom.app (Opposite.unop x✝)) ≫
        (Over.mapComp g h).inv.app ((Over.map f).obj (Opposite.unop x✝)) ≫
          (Over.mapComp f (g ≫ h)).inv.app (Opposite.unop x✝) =
    (Over.mapCongr (f ≫ g ≫ h) ((f ≫ g) ≫ h) ⋯).inv.app (Opposite.unop x✝)
Module: Mathlib.Topology.Sheaves.Presheaf

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U V : Opens ↑X
HU : IsOpen (⇑(ConcreteCategory.hom f) '' ↑U)
HV : IsOpen (⇑(ConcreteCategory.hom f) '' ↑V)
le : U ≤ V
⊢ ((pullback C f).obj ℱ).map (homOfLE le).op ≫
      (IsColimit.coconePointUniqueUpToIso ((Opens.map f).op.isPointwiseLeftKanExtensionLeftKanExtensionUnit ℱ (op U))
          (colimitOfDiagramTerminal { lift := fun s ↦ CostructuredArrow.homMk (homOfLE ⋯).op ⋯, fac := ⋯, uniq := ⋯ }
            (CostructuredArrow.proj (Opens.map f).op (op U) ⋙ ℱ))).hom =
    (IsColimit.coconePointUniqueUpToIso ((Opens.map f).op.isPointwiseLeftKanExtensionLeftKanExtensionUnit ℱ (op V))
          (colimitOfDiagramTerminal { lift := fun s ↦ CostructuredArrow.homMk (homOfLE ⋯).op ⋯, fac := ⋯, uniq := ⋯ }
            (CostructuredArrow.proj (Opens.map f).op (op V) ⋙ ℱ))).hom ≫
      ℱ.map (IsOpenMap.functorMap HU HV le).op

Tactic:
refine ((Opens.map f).op.isPointwiseLeftKanExtensionLeftKanExtensionUnit ℱ (op V)).hom_ext
    (fun j ↦ ?_)

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
ℱ : Presheaf C Y
U V : Opens ↑X
HU : IsOpen (⇑(ConcreteCategory.hom f) '' ↑U)
HV : IsOpen (⇑(ConcreteCategory.hom f) '' ↑V)
le : U ≤ V
j : CostructuredArrow (Opens.map f).op (op V)
⊢ ((LeftExtension.mk ((Opens.map f).op.leftKanExtension ℱ) ((Opens.map f).op.leftKanExtensionUnit ℱ)).coconeAt
              (op V)).ι.app
        j ≫
      ((pullback C f).obj ℱ).map (homOfLE le).op ≫
        (IsColimit.coconePointUniqueUpToIso ((Opens.map f).op.isPointwiseLeftKanExtensionLeftKanExtensionUnit ℱ (op U))
            (colimitOfDiagramTerminal { lift := fun s ↦ CostructuredArrow.homMk (homOfLE ⋯).op ⋯, fac := ⋯, uniq := ⋯ }
              (CostructuredArrow.proj (Opens.map f).op (op U) ⋙ ℱ))).hom =
    ((LeftExtension.mk ((Opens.map f).op.leftKanExtension ℱ) ((Opens.map f).op.leftKanExtensionUnit ℱ)).coconeAt
              (op V)).ι.app
        j ≫
      (IsColimit.coconePointUniqueUpToIso ((Opens.map f).op.isPointwiseLeftKanExtensionLeftKanExtensionUnit ℱ (op V))
            (colimitOfDiagramTerminal { lift := fun s ↦ CostructuredArrow.homMk (homOfLE ⋯).op ⋯, fac := ⋯, uniq := ⋯ }
              (CostructuredArrow.proj (Opens.map f).op (op V) ⋙ ℱ))).hom ≫
        ℱ.map (IsOpenMap.functorMap HU HV le).op
Module: Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasLimitsOfSize.{x, x, v_1, u_1} C
inst✝¹ : (CategoryTheory.forget C).ReflectsIsomorphisms
inst✝ : PreservesLimitsOfSize.{x, x, v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget C)
X : TopCat
F : Sheaf C X
ι : Type u_4
U : ι → Opens ↑X
V : Opens ↑X
iUV : (i : ι) → U i ⟶ V
hcover : V ≤ iSup U
sf : (i : ι) → ToType (F.obj.obj (op (U i)))
h : IsCompatible F.obj U sf
V_eq_supr_U : V = iSup U
⊢ ∃! s, ∀ (i : ι), (ConcreteCategory.hom (F.obj.map (iUV i).op)) s = sf i

Tactic:
obtain ⟨gl, gl_spec, gl_uniq⟩ := F.existsUnique_gluing U sf h

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasLimitsOfSize.{x, x, v_1, u_1} C
inst✝¹ : (CategoryTheory.forget C).ReflectsIsomorphisms
inst✝ : PreservesLimitsOfSize.{x, x, v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget C)
X : TopCat
F : Sheaf C X
ι : Type u_4
U : ι → Opens ↑X
V : Opens ↑X
iUV : (i : ι) → U i ⟶ V
hcover : V ≤ iSup U
sf : (i : ι) → ToType (F.obj.obj (op (U i)))
h : IsCompatible F.obj U sf
V_eq_supr_U : V = iSup U
gl : ToType (F.obj.obj (op (iSup U)))
gl_spec : IsGluing F.obj U sf gl
gl_uniq : ∀ (y : ToType (F.obj.obj (op (iSup U)))), (fun s ↦ IsGluing F.obj U sf s) y → y = gl
⊢ ∃! s, ∀ (i : ι), (ConcreteCategory.hom (F.obj.map (iUV i).op)) s = sf i
Module: Mathlib.Topology.Sheaves.Stalks

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : (forget C).ReflectsIsomorphisms
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ x ∈ U, Function.Injective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map f.hom))
hsurj :
  ∀ (t : CC (G.obj.obj (op U))) (x : ↥U),
    ∃ V,
      ∃ (_ : ↑x ∈ V), ∃ iVU s, (ConcreteCategory.hom (f.hom.app (op V))) s = (ConcreteCategory.hom (G.obj.map iVU.op)) t
t : CC (G.obj.obj (op U))
V : ↥U → Opens ↑X
mV : ∀ (x : ↥U), ↑x ∈ V x
iVU : (x : ↥U) → V x ⟶ U
sf : (x : ↥U) → ToType (F.obj.obj (op (V x)))
heq : ∀ (x : ↥U), (ConcreteCategory.hom (f.hom.app (op (V x)))) (sf x) = (ConcreteCategory.hom (G.obj.map (iVU x).op)) t
V_cover : U ≤ iSup V
x : ↥U
⊢ ∀ (j : ↥U),
    (ConcreteCategory.hom (F.obj.map ((V x).infLELeft (V j)).op)) (sf x) =
      (ConcreteCategory.hom (F.obj.map ((V x).infLERight (V j)).op)) (sf j)

Tactic:
y

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasColimits C
X : TopCat
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝³ : PreservesFilteredColimits (forget C)
inst✝² : HasLimits C
inst✝¹ : PreservesLimits (forget C)
inst✝ : (forget C).ReflectsIsomorphisms
F G : Sheaf C X
f : F ⟶ G
U : Opens ↑X
hinj : ∀ x ∈ U, Function.Injective ⇑(ConcreteCategory.hom ((stalkFunctor C x).map f.hom))
hsurj :
  ∀ (t : CC (G.obj.obj (op U))) (x : ↥U),
    ∃ V,
      ∃ (_ : ↑x ∈ V), ∃ iVU s, (ConcreteCategory.hom (f.hom.app (op V))) s = (ConcreteCategory.hom (G.obj.map iVU.op)) t
t : CC (G.obj.obj (op U))
V : ↥U → Opens ↑X
mV : ∀ (x : ↥U), ↑x ∈ V x
iVU : (x : ↥U) → V x ⟶ U
sf : (x : ↥U) → ToType (F.obj.obj (op (V x)))
heq : ∀ (x : ↥U), (ConcreteCategory.hom (f.hom.app (op (V x)))) (sf x) = (ConcreteCategory.hom (G.obj.map (iVU x).op)) t
V_cover : U ≤ iSup V
x y : ↥U
⊢ (ConcreteCategory.hom (F.obj.map ((V x).infLELeft (V y)).op)) (sf x) =
    (ConcreteCategory.hom (F.obj.map ((V x).infLERight (V y)).op)) (sf y)
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: case mk.mk
R₁ : Type u_1
R₂ : Type u_2
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst✝⁵ : TopologicalSpace M₁
inst✝⁴ : AddCommMonoid M₁
M₂ : Type u_6
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₁ M₁
inst✝ : Module R₂ M₂
toLinearMap✝¹ : M₁ →ₛₗ[σ₁₂] M₂
cont✝¹ : Continuous[inst✝⁵, inst✝³] toLinearMap✝¹.toFun
toLinearMap✝ : M₁ →ₛₗ[σ₁₂] M₂
cont✝ : Continuous[inst✝⁵, inst✝³] toLinearMap✝.toFun
H : ↑{ toLinearMap := toLinearMap✝¹, cont := cont✝¹ } = ↑{ toLinearMap := toLinearMap✝, cont := cont✝ }
⊢ { toLinearMap := toLinearMap✝¹, cont := cont✝¹ } = { toLinearMap := toLinearMap✝, cont := cont✝ }

Tactic:
congr

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Homology

Goal state before:
pp: case refine_2
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
M N : TopModuleCat R
φ : M ⟶ N
S : ShortComplex (TopModuleCat R)
D₁ : S.LeftHomologyData :=
  { K := ker S.g, H := coker ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)), i := kerι S.g,
    π := cokerπ ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)), wi := ⋯, hi := isLimitKer S.g, wπ := ⋯,
    hπ := isColimitCoker ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)) }
D₂ : S.RightHomologyData :=
  { Q := coker S.f, H := ker ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)), p := cokerπ S.f,
    ι := kerι ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)), wp := ⋯, hp := isColimitCoker S.f, wι := ⋯,
    hι := isLimitKer ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)) }
F : D₁.H ⟶ D₂.H := ShortComplex.leftRightHomologyComparison' D₁ D₂
hF : Function.Bijective ⇑(ConcreteCategory.hom F)
x : ↑S.X₂.toModuleCat
⊢ ∀ (y : (fun X ↦ ↑X.toModuleCat) S.X₂),
    (ConcreteCategory.hom S.g) y = 0 →
      (ConcreteCategory.hom D₂.p) y = (ConcreteCategory.hom D₂.p) x → (ConcreteCategory.hom S.g) x = 0

Tactic:
y

Goal state after:
case refine_2
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
M N : TopModuleCat R
φ : M ⟶ N
S : ShortComplex (TopModuleCat R)
D₁ : S.LeftHomologyData :=
  { K := ker S.g, H := coker ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)), i := kerι S.g,
    π := cokerπ ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)), wi := ⋯, hi := isLimitKer S.g, wπ := ⋯,
    hπ := isColimitCoker ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)) }
D₂ : S.RightHomologyData :=
  { Q := coker S.f, H := ker ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)), p := cokerπ S.f,
    ι := kerι ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)), wp := ⋯, hp := isColimitCoker S.f, wι := ⋯,
    hι := isLimitKer ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)) }
F : D₁.H ⟶ D₂.H := ShortComplex.leftRightHomologyComparison' D₁ D₂
hF : Function.Bijective ⇑(ConcreteCategory.hom F)
x y : ↑S.X₂.toModuleCat
⊢ (ConcreteCategory.hom S.g) y = 0 →
    (ConcreteCategory.hom D₂.p) y = (ConcreteCategory.hom D₂.p) x → (ConcreteCategory.hom S.g) x = 0
Module: Mathlib.Algebra.Category.MonCat.Colimits

Goal state before:
pp: case a
J : Type v
inst✝ : Category.{u, v} J
F : J ⥤ MonCat
s : Cocone F
x : Prequotient F
⊢ ∀ (b : Prequotient F), (colimitSetoid F) x b → descFunLift F s x = descFunLift F s b

Tactic:
y

Goal state after:
case a
J : Type v
inst✝ : Category.{u, v} J
F : J ⥤ MonCat
s : Cocone F
x y : Prequotient F
⊢ (colimitSetoid F) x y → descFunLift F s x = descFunLift F s y
Module: Mathlib.CategoryTheory.Comma.CardinalArrow

Goal state before:
pp: C : Type u
inst✝ : SmallCategory C
a✝ : Finite (Arrow C)
a b : C
f g : a ⟶ b
h : (fun f ↦ mk f) f = (fun f ↦ mk f) g
⊢ (mk f).hom = (mk g).hom

Tactic:
congr

Goal state after:
Module: Mathlib.CategoryTheory.Comma.CardinalArrow

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Small.{w, max u v} (Arrow C)
X Y : C
f g : X ⟶ Y
h : (fun f ↦ Arrow.mk f) f = (fun f ↦ Arrow.mk f) g
⊢ (Arrow.mk f).hom = (Arrow.mk g).hom

Tactic:
congr

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic

Goal state before:
pp: R : Type u
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
M : ModuleCat R
I : Type u_1
X : I → TopModuleCat R
f : (i : I) → (X i).toModuleCat ⟶ M
J : Type u_2
inst✝ : Category.{v_1, u_2} J
F : J ⥤ TopModuleCat R
c : Cocone (F ⋙ forget₂ (TopModuleCat R) (ModuleCat R))
hc : IsColimit c
s : Cocone F
⊢ instTopologicalSpaceCarrier R (ofCocone c).pt ≤
    TopologicalSpace.induced (ModuleCat.Hom.hom (hc.desc ((forget₂ (TopModuleCat R) (ModuleCat R)).mapCocone s))).toFun
      s.1.topologicalSpace

Tactic:
refine sInf_le ⟨continuousSMul_induced (M₂ := s.pt) (hc.desc ((forget₂ _ _).mapCocone s)).hom,
      continuousAdd_induced (N := s.pt) (hc.desc ((forget₂ _ _).mapCocone s)).hom, fun i ↦ ?_⟩

Goal state after:
R : Type u
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
M : ModuleCat R
I : Type u_1
X : I → TopModuleCat R
f : (i : I) → (X i).toModuleCat ⟶ M
J : Type u_2
inst✝ : Category.{v_1, u_2} J
F : J ⥤ TopModuleCat R
c : Cocone (F ⋙ forget₂ (TopModuleCat R) (ModuleCat R))
hc : IsColimit c
s : Cocone F
i : J
⊢ TopologicalSpace.coinduced (⇑(hom (c.ι.app i))) (F.obj i).topologicalSpace ≤
    TopologicalSpace.induced (ModuleCat.Hom.hom (hc.desc ((forget₂ (TopModuleCat R) (ModuleCat R)).mapCocone s))).toFun
      s.1.topologicalSpace
Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

Goal state before:
pp: J : Type u
inst✝² : Category.{v, u} J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
ι : Type v'
j : ι → J
k : J
f₁ f₂ : (i : ι) → j i ⟶ k
hι : HasCardinalLT ι κ
this : IsFiltered J
l : J
a : (i : ι) → IsFiltered.coeq (f₁ i) (f₂ i) ⟶ l
b : k ⟶ l
h : ∀ (i : ι), IsFiltered.coeqHom (f₁ i) (f₂ i) ≫ a i = b
i : ι
⊢ f₁ i ≫ b = f₂ i ≫ b

Tactic:
← h i,

Goal state after:
J : Type u
inst✝² : Category.{v, u} J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
ι : Type v'
j : ι → J
k : J
f₁ f₂ : (i : ι) → j i ⟶ k
hι : HasCardinalLT ι κ
this : IsFiltered J
l : J
a : (i : ι) → IsFiltered.coeq (f₁ i) (f₂ i) ⟶ l
b : k ⟶ l
h : ∀ (i : ι), IsFiltered.coeqHom (f₁ i) (f₂ i) ≫ a i = b
i : ι
⊢ f₁ i ≫ IsFiltered.coeqHom (f₁ i) (f₂ i) ≫ a i = f₂ i ≫ IsFiltered.coeqHom (f₁ i) (f₂ i) ≫ a i
Module: Mathlib.LinearAlgebra.TensorProduct.Pi

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Type u_2
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
N : Type u_3
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : Module S N
inst✝⁴ : IsScalarTower R S N
ι : Type u_4
M : ι → Type u_5
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : N
m : (i : ι) → M i
⊢ x ⊗ₜ[R] ∑ a, Pi.single a (m a) = x ⊗ₜ[R] m

Tactic:
congr

Goal state after:
case e_n
R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Type u_2
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
N : Type u_3
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : Module S N
inst✝⁴ : IsScalarTower R S N
ι : Type u_4
M : ι → Type u_5
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : N
m : (i : ι) → M i
⊢ ∑ a, Pi.single a (m a) = m