mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous

Goal state before:
pp: C✝ : Type u₁
inst✝⁸ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝⁷ : Category.{v₂, u₂} D✝
D' : Type u₃
inst✝⁶ : Category.{v₃, u₃} D'
D'' : Type u₄
inst✝⁵ : Category.{v₄, u₄} D''
J✝ : GrothendieckTopology C✝
K✝ : GrothendieckTopology D✝
F✝ : C✝ ⥤ D✝
S✝ : Sheaf J✝ RingCat
R✝ : Sheaf K✝ RingCat
inst✝⁴ : F✝.IsContinuous J✝ K✝
φ✝ : S✝ ⟶ (F✝.sheafPushforwardContinuous RingCat J✝ K✝).obj R✝
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
G : D ⥤ C
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝¹ : F.IsContinuous J K
inst✝ : G.IsContinuous K J
adj : F ⊣ G
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
ψ : R ⟶ (G.sheafPushforwardContinuous RingCat K J).obj S
H₁ : whiskerRight (NatTrans.op adj.counit) R.obj = ψ.hom ≫ G.op.whiskerLeft φ.hom
H₂ : φ.hom ≫ F.op.whiskerLeft ψ.hom ≫ whiskerRight (NatTrans.op adj.unit) S.obj = 𝟙 S.obj
X : SheafOfModules S
U : Dᵒᵖ
x : ↑(((pushforward ψ).obj X).val.obj U)
⊢ (ConcreteCategory.hom
        (X.val.presheaf.map (adj.unit.app (G.obj (Opposite.unop U)) ≫ G.map (adj.counit.app (Opposite.unop U))).op))
      x =
    (ModuleCat.Hom.hom ((𝟙 ((pushforward ψ).obj X)).val.app U)) x

Tactic:
adj.right_triangle_components

Goal state after:
C✝ : Type u₁
inst✝⁸ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝⁷ : Category.{v₂, u₂} D✝
D' : Type u₃
inst✝⁶ : Category.{v₃, u₃} D'
D'' : Type u₄
inst✝⁵ : Category.{v₄, u₄} D''
J✝ : GrothendieckTopology C✝
K✝ : GrothendieckTopology D✝
F✝ : C✝ ⥤ D✝
S✝ : Sheaf J✝ RingCat
R✝ : Sheaf K✝ RingCat
inst✝⁴ : F✝.IsContinuous J✝ K✝
φ✝ : S✝ ⟶ (F✝.sheafPushforwardContinuous RingCat J✝ K✝).obj R✝
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
G : D ⥤ C
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝¹ : F.IsContinuous J K
inst✝ : G.IsContinuous K J
adj : F ⊣ G
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
ψ : R ⟶ (G.sheafPushforwardContinuous RingCat K J).obj S
H₁ : whiskerRight (NatTrans.op adj.counit) R.obj = ψ.hom ≫ G.op.whiskerLeft φ.hom
H₂ : φ.hom ≫ F.op.whiskerLeft ψ.hom ≫ whiskerRight (NatTrans.op adj.unit) S.obj = 𝟙 S.obj
X : SheafOfModules S
U : Dᵒᵖ
x : ↑(((pushforward ψ).obj X).val.obj U)
⊢ (ConcreteCategory.hom (X.val.presheaf.map (𝟙 (G.obj (Opposite.unop U))).op)) x =
    (ModuleCat.Hom.hom ((𝟙 ((pushforward ψ).obj X)).val.app U)) x
Module: Mathlib.Topology.Sheaves.Presheaf

Goal state before:
pp: X : TopCat
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
F G : Presheaf C X
e : F ⟶ G
U V : Opens ↑X
h : U ≤ V
x : ToType (F.obj (op V))
⊢ (ConcreteCategory.hom (e.app (op U))) ((x |_ U) h) = ((ConcreteCategory.hom (e.app (op V))) x |_ U) h

Tactic:
delta restrictOpen restrict
  rw [← ConcreteCategory.comp_apply, NatTrans.naturality, ConcreteCategory.comp_apply]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous

Goal state before:
pp: C✝ : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝¹⁰ : Category.{v₂, u₂} D✝
D' : Type u₃
inst✝⁹ : Category.{v₃, u₃} D'
D'' : Type u₄
inst✝⁸ : Category.{v₄, u₄} D''
J✝ : GrothendieckTopology C✝
K✝ : GrothendieckTopology D✝
F✝ : C✝ ⥤ D✝
S✝ : Sheaf J✝ RingCat
R✝ : Sheaf K✝ RingCat
inst✝⁷ : F✝.IsContinuous J✝ K✝
φ✝ : S✝ ⟶ (F✝.sheafPushforwardContinuous RingCat J✝ K✝).obj R✝
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
G : D ⥤ C
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝⁴ : F.IsContinuous J K
inst✝³ : G.IsContinuous K J
adj : F ⊣ G
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
ψ : R ⟶ (G.sheafPushforwardContinuous RingCat K J).obj S
H₁ : whiskerRight (NatTrans.op adj.counit) R.obj = ψ.hom ≫ G.op.whiskerLeft φ.hom
H₂ : φ.hom ≫ F.op.whiskerLeft ψ.hom ≫ whiskerRight (NatTrans.op adj.unit) S.obj = 𝟙 S.obj
inst✝² : F.IsCocontinuous J K
inst✝¹ : IsIso φ
inst✝ : F.IsLeftAdjoint
⊢ (pushforward φ).IsLeftAdjoint

Tactic:
let adj := Adjunction.ofIsLeftAdjoint F

Goal state after:
C✝ : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝¹⁰ : Category.{v₂, u₂} D✝
D' : Type u₃
inst✝⁹ : Category.{v₃, u₃} D'
D'' : Type u₄
inst✝⁸ : Category.{v₄, u₄} D''
J✝ : GrothendieckTopology C✝
K✝ : GrothendieckTopology D✝
F✝ : C✝ ⥤ D✝
S✝ : Sheaf J✝ RingCat
R✝ : Sheaf K✝ RingCat
inst✝⁷ : F✝.IsContinuous J✝ K✝
φ✝ : S✝ ⟶ (F✝.sheafPushforwardContinuous RingCat J✝ K✝).obj R✝
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
J : GrothendieckTopology C
K : GrothendieckTopology D
F : C ⥤ D
G : D ⥤ C
S : Sheaf J RingCat
R : Sheaf K RingCat
inst✝⁴ : F.IsContinuous J K
inst✝³ : G.IsContinuous K J
adj✝ : F ⊣ G
φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R
ψ : R ⟶ (G.sheafPushforwardContinuous RingCat K J).obj S
H₁ : whiskerRight (NatTrans.op adj✝.counit) R.obj = ψ.hom ≫ G.op.whiskerLeft φ.hom
H₂ : φ.hom ≫ F.op.whiskerLeft ψ.hom ≫ whiskerRight (NatTrans.op adj✝.unit) S.obj = 𝟙 S.obj
inst✝² : F.IsCocontinuous J K
inst✝¹ : IsIso φ
inst✝ : F.IsLeftAdjoint
adj : F ⊣ F.rightAdjoint := Adjunction.ofIsLeftAdjoint F
⊢ (pushforward φ).IsLeftAdjoint
Module: Mathlib.Topology.Sheaves.SheafCondition.Sites

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : TopCat
f : X ⟶ Y
F : Presheaf C Y
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
hF : F.IsSheaf
⊢ IsSheaf (h.functor.op ⋙ F)

Tactic:
by
  have := h.functor_isContinuous
  exact Functor.op_comp_isSheaf _ _ _ ⟨_, hF⟩

Goal state after:
Module: Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Presheaf C X
h : F.IsSheafOpensLeCover
Y : Opens ↑X
S : Sieve Y
hS : Sieve.generate S.arrows ∈ (Opens.grothendieckTopology ↑X) Y
⊢ Nonempty (IsLimit (Functor.mapCone F (Sieve.generate S.arrows).arrows.cocone.op))

Tactic:
rw [← (isLimitOpensLeEquivGenerate₂ F S.1 hS).nonempty_congr]

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Presheaf C X
h : F.IsSheafOpensLeCover
Y : Opens ↑X
S : Sieve Y
hS : Sieve.generate S.arrows ∈ (Opens.grothendieckTopology ↑X) Y
⊢ Nonempty (IsLimit (Functor.mapCone F (opensLeCoverCocone (coveringOfPresieve Y S.arrows)).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
s t : ToType (F.obj.obj (op (iSup U)))
h :
  ∀ (i : ι), (ConcreteCategory.hom (F.obj.map (leSupr U i).op)) s = (ConcreteCategory.hom (F.obj.map (leSupr U i).op)) t
sf : (i : ι) → ToType (F.obj.obj (op (U i))) := fun i ↦ (ConcreteCategory.hom (F.obj.map (leSupr U i).op)) s
sf_compatible : IsCompatible F.obj U sf
gl : ToType (F.obj.obj (op (iSup U)))
gl_uniq : ∀ (y : ToType (F.obj.obj (op (iSup U)))), (fun s ↦ IsGluing F.obj U sf s) y → y = gl
i : ι
⊢ (ConcreteCategory.hom (F.obj.map (leSupr U i).op)) t = sf i

Tactic:
← 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
s t : ToType (F.obj.obj (op (iSup U)))
h :
  ∀ (i : ι), (ConcreteCategory.hom (F.obj.map (leSupr U i).op)) s = (ConcreteCategory.hom (F.obj.map (leSupr U i).op)) t
sf : (i : ι) → ToType (F.obj.obj (op (U i))) := fun i ↦ (ConcreteCategory.hom (F.obj.map (leSupr U i).op)) s
sf_compatible : IsCompatible F.obj U sf
gl : ToType (F.obj.obj (op (iSup U)))
gl_uniq : ∀ (y : ToType (F.obj.obj (op (iSup U)))), (fun s ↦ IsGluing F.obj U sf s) y → y = gl
i : ι
⊢ (ConcreteCategory.hom (F.obj.map (leSupr U i).op)) s = sf i
Module: Mathlib.Topology.Algebra.Module.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : ι → Type u_3
inst✝⁴ : Semiring R
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : (i : ι) → TopologicalSpace (M i)
inst✝ : DecidableEq ι
s : (i : ι) → Submodule R (M i)
⊢ closure[Pi.topologicalSpace] ↑(⨆ i, map (LinearMap.single R M i) (s i)) = Set.univ.pi fun i ↦ closure[inst✝¹ i] ↑(s i)

Tactic:
by
  rw [← closure_pi_set]
  refine (closure_mono ?_).antisymm <| closure_minimal ?_ isClosed_closure
  · exact SetLike.coe_mono <| iSup_map_single_le
  · simp only [Set.subset_def, mem_closure_iff]
    intro x hx U hU hxU
    rcases isOpen_pi_iff.mp hU x hxU with ⟨t, V, hV, hVU⟩
    refine ⟨∑ i ∈ t, Pi.single i (x i), hVU ?_, ?_⟩
    · simp_all [Finset.sum_pi_single]
    · exact sum_mem fun i hi ↦ mem_iSup_of_mem i <| mem_map_of_mem <| hx _ <| Set.mem_univ _

Goal state after:
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 y : ↥U
⊢ ∀ (x_1 : ↑X) (hx : x_1 ∈ V x ⊓ V y),
    (ConcreteCategory.hom (F.presheaf.germ (V x ⊓ V y) x_1 hx))
        ((ConcreteCategory.hom (F.obj.map ((V x).infLELeft (V y)).op)) (sf x)) =
      (ConcreteCategory.hom (F.presheaf.germ (V x ⊓ V y) x_1 hx))
        ((ConcreteCategory.hom (F.obj.map ((V x).infLERight (V y)).op)) (sf y))

Tactic:
intro z

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
z : ↑X
⊢ ∀ (hx : z ∈ V x ⊓ V y),
    (ConcreteCategory.hom (F.presheaf.germ (V x ⊓ V y) z hx))
        ((ConcreteCategory.hom (F.obj.map ((V x).infLELeft (V y)).op)) (sf x)) =
      (ConcreteCategory.hom (F.presheaf.germ (V x ⊓ V y) z hx))
        ((ConcreteCategory.hom (F.obj.map ((V x).infLERight (V y)).op)) (sf y))
Module: Mathlib.Algebra.Category.ModuleCat.Stalk

Goal state before:
pp: case refine_1
C : Type u_1
inst✝² : SmallCategory C
inst✝¹ : IsFiltered C
R : C ⥤ RingCat
M : C ⥤ Ab
inst✝ : (i : C) → Module ↑(R.obj i) ↑(M.obj i)
H :
  ∀ {i j : C} (f : i ⟶ j) (r : ↑(R.obj i)) (m : ↑(M.obj i)),
    (ConcreteCategory.hom (M.map f)) (r • m) = (ConcreteCategory.hom (R.map f)) r • (ConcreteCategory.hom (M.map f)) m
r : (R ⋙ forget RingCat).ColimitType
m : (M ⋙ forget Ab).ColimitType
U : C
a : (R ⋙ forget RingCat).obj U
V₁ : C
b₁ : (M ⋙ forget Ab).obj V₁
V₂ : C
f : V₁ ⟶ V₂
s : C
α : IsFiltered.max U V₁ ⟶ s
β : IsFiltered.max U V₂ ⟶ s
h₁ : leftToMax U V₁ ≫ α = leftToMax U V₂ ≫ β
h₂ : rightToMax U V₁ ≫ α = (f ≫ rightToMax U V₂) ≫ β
⊢ (ConcreteCategory.hom ((M ⋙ forget Ab).map α))
      ((ConcreteCategory.hom (R.map (leftToMax ⟨U, a⟩.fst ⟨V₁, b₁⟩.fst))) ⟨U, a⟩.snd •
        (ConcreteCategory.hom (M.map (rightToMax ⟨U, a⟩.fst ⟨V₁, b₁⟩.fst))) ⟨V₁, b₁⟩.snd) =
    (ConcreteCategory.hom ((M ⋙ forget Ab).map β))
      ((ConcreteCategory.hom (R.map (leftToMax ⟨U, a⟩.fst ⟨V₂, (ConcreteCategory.hom (M.map f)) b₁⟩.fst))) ⟨U, a⟩.snd •
        (ConcreteCategory.hom (M.map (rightToMax ⟨U, a⟩.fst ⟨V₂, (ConcreteCategory.hom (M.map f)) b₁⟩.fst)))
          ⟨V₂, (ConcreteCategory.hom (M.map f)) b₁⟩.snd)

Tactic:
simp [*, ← R.map_comp_apply, ← M.map_comp_apply, -Functor.map_comp]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Stalk

Goal state before:
pp: case refine_2
C : Type u_1
inst✝² : SmallCategory C
inst✝¹ : IsFiltered C
R : C ⥤ RingCat
M : C ⥤ Ab
inst✝ : (i : C) → Module ↑(R.obj i) ↑(M.obj i)
H :
  ∀ {i j : C} (f : i ⟶ j) (r : ↑(R.obj i)) (m : ↑(M.obj i)),
    (ConcreteCategory.hom (M.map f)) (r • m) = (ConcreteCategory.hom (R.map f)) r • (ConcreteCategory.hom (M.map f)) m
r : (R ⋙ forget RingCat).ColimitType
m : (M ⋙ forget Ab).ColimitType
U₁ : C
a₁ : (R ⋙ forget RingCat).obj U₁
U₂ V : C
b : (M ⋙ forget Ab).obj V
f : U₁ ⟶ U₂
s : C
α : IsFiltered.max U₁ V ⟶ s
β : IsFiltered.max U₂ V ⟶ s
h₁ : leftToMax U₁ V ≫ α = (f ≫ leftToMax U₂ V) ≫ β
h₂ : rightToMax U₁ V ≫ α = rightToMax U₂ V ≫ β
⊢ (ConcreteCategory.hom ((M ⋙ forget Ab).map α))
      ((ConcreteCategory.hom (R.map (leftToMax ⟨U₁, a₁⟩.fst ⟨V, b⟩.fst))) ⟨U₁, a₁⟩.snd •
        (ConcreteCategory.hom (M.map (rightToMax ⟨U₁, a₁⟩.fst ⟨V, b⟩.fst))) ⟨V, b⟩.snd) =
    (ConcreteCategory.hom ((M ⋙ forget Ab).map β))
      ((ConcreteCategory.hom (R.map (leftToMax ⟨U₂, (ConcreteCategory.hom (R.map f)) a₁⟩.fst ⟨V, b⟩.fst)))
          ⟨U₂, (ConcreteCategory.hom (R.map f)) a₁⟩.snd •
        (ConcreteCategory.hom (M.map (rightToMax ⟨U₂, (ConcreteCategory.hom (R.map f)) a₁⟩.fst ⟨V, b⟩.fst))) ⟨V, b⟩.snd)

Tactic:
simp [*, ← R.map_comp_apply, ← M.map_comp_apply, -Functor.map_comp]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Stalk

Goal state before:
pp: case refine_2
C : Type u_1
inst✝² : SmallCategory C
inst✝¹ : IsFiltered C
R : C ⥤ RingCat
M : C ⥤ Ab
inst✝ : (i : C) → Module ↑(R.obj i) ↑(M.obj i)
H :
  ∀ {i j : C} (f : i ⟶ j) (r : ↑(R.obj i)) (m : ↑(M.obj i)),
    (ConcreteCategory.hom (M.map f)) (r • m) = (ConcreteCategory.hom (R.map f)) r • (ConcreteCategory.hom (M.map f)) m
r : (R ⋙ forget RingCat).ColimitType
m : (M ⋙ forget Ab).ColimitType
⊢ ∀ (a₁ a₂ : (j : C) × (R ⋙ forget RingCat).obj j) (b : (j : C) × (M ⋙ forget Ab).obj j),
    (R ⋙ forget RingCat).ColimitTypeRel a₁ a₂ →
      (M ⋙ forget Ab).ιColimitType (IsFiltered.max a₁.fst b.fst)
          ((ConcreteCategory.hom (R.map (leftToMax a₁.fst b.fst))) a₁.snd •
            (ConcreteCategory.hom (M.map (rightToMax a₁.fst b.fst))) b.snd) =
        (M ⋙ forget Ab).ιColimitType (IsFiltered.max a₂.fst b.fst)
          ((ConcreteCategory.hom (R.map (leftToMax a₂.fst b.fst))) a₂.snd •
            (ConcreteCategory.hom (M.map (rightToMax a₂.fst b.fst))) b.snd)

Tactic:
rintro ⟨U₁, a₁⟩ ⟨U₂, a₂⟩ ⟨V, b⟩ ⟨f : U₁ ⟶ U₂, rfl : a₂ = R.map _ a₁⟩
    obtain ⟨s, α, β, h₁, h₂⟩ :=
      bowtie (leftToMax U₁ V) (f ≫ leftToMax U₂ V)
        (rightToMax U₁ V) (rightToMax U₂ V)
    refine Functor.ιColimitType_eq_of_map_eq_map _ _ _ α β ?_
    simp [*, ← R.map_comp_apply, ← M.map_comp_apply, -Functor.map_comp]

Goal state after:
Module: Mathlib.Topology.Algebra.Module.ModuleTopology

Goal state before:
pp: R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
σ : R →+* S
σ' : S →+* R
inst✝⁶ : RingHomInvPair σ σ'
inst✝⁵ : RingHomInvPair σ' σ
A : Type u_3
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R A
τA : TopologicalSpace A
inst✝² : IsModuleTopology R A
B' : Type u_5
inst✝¹ : AddCommMonoid B'
inst✝ : Module S B'
τB' : TopologicalSpace B'
hσ : Continuous ⇑σ
hσ' : Continuous ⇑σ'
e : A ≃SL[σ] B'
g : A →ₛₗ[σ] B' := ↑↑e
g' : B' →ₛₗ[σ'] A := ↑↑e.symm
⊢ τB' = moduleTopology S B'

Tactic:
let h : A →+ B' := e

Goal state after:
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
σ : R →+* S
σ' : S →+* R
inst✝⁶ : RingHomInvPair σ σ'
inst✝⁵ : RingHomInvPair σ' σ
A : Type u_3
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R A
τA : TopologicalSpace A
inst✝² : IsModuleTopology R A
B' : Type u_5
inst✝¹ : AddCommMonoid B'
inst✝ : Module S B'
τB' : TopologicalSpace B'
hσ : Continuous ⇑σ
hσ' : Continuous ⇑σ'
e : A ≃SL[σ] B'
g : A →ₛₗ[σ] B' := ↑↑e
g' : B' →ₛₗ[σ'] A := ↑↑e.symm
h : A →+ B' := ↑e
⊢ τB' = moduleTopology S B'
Module: Mathlib.Topology.Algebra.Module.ModuleTopology

Goal state before:
pp: R : Type u_1
inst✝⁹ : TopologicalSpace R
inst✝⁸ : Semiring R
M : Type u_2
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : TopologicalSpace M
inst✝⁴ : IsModuleTopology R M
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : TopologicalSpace N
inst✝ : IsModuleTopology R N
this✝² : ContinuousAdd M
this✝¹ : ContinuousAdd N
P : Type (max u_2 u_3) := M × N
τP : TopologicalSpace P := moduleTopology R P
this✝ : IsModuleTopology R P
this : ContinuousAdd P
i : M × N → P := id
i₁ : M →ₗ[R] P := LinearMap.inl R M N
i₂ : N →ₗ[R] P := LinearMap.inr R M N
⊢ Continuous i

Tactic:
rw [show (i : M × N → P) =
       (fun abcd ↦ abcd.1 + abcd.2 : P × P → P) ∘
       (fun ab ↦ (i₁ ab.1, i₂ ab.2)) by
       ext ⟨a, b⟩ <;> aesop]

Goal state after:
R : Type u_1
inst✝⁹ : TopologicalSpace R
inst✝⁸ : Semiring R
M : Type u_2
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : TopologicalSpace M
inst✝⁴ : IsModuleTopology R M
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : TopologicalSpace N
inst✝ : IsModuleTopology R N
this✝² : ContinuousAdd M
this✝¹ : ContinuousAdd N
P : Type (max u_2 u_3) := M × N
τP : TopologicalSpace P := moduleTopology R P
this✝ : IsModuleTopology R P
this : ContinuousAdd P
i : M × N → P := id
i₁ : M →ₗ[R] P := LinearMap.inl R M N
i₂ : N →ₗ[R] P := LinearMap.inr R M N
⊢ Continuous ((fun abcd ↦ abcd.1 + abcd.2) ∘ fun ab ↦ (i₁ ab.1, i₂ ab.2))
Module: Mathlib.Algebra.Category.MonCat.Colimits

Goal state before:
pp: case h
J : Type v
inst✝ : Category.{u, v} J
F : J ⥤ MonCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
x : Prequotient F
⊢ (Hom.hom m) (Quot.mk (⇑(colimitSetoid F)) x) = (Hom.hom (descMorphism F s)) (Quot.mk (⇑(colimitSetoid F)) x)

Tactic:
| h x =>

Goal state after:
case h
J : Type v
inst✝ : Category.{u, v} J
F : J ⥤ MonCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
x : Prequotient F
⊢ (Hom.hom m) (Quot.mk (⇑(colimitSetoid F)) x) = (Hom.hom (descMorphism F s)) (Quot.mk (⇑(colimitSetoid F)) x)
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
g : M₂ →L[R] M₃
f : M →L[R] M₂
hf : f.IsInvertible
⊢ (g ∘SL f).inverse = f.inverse ∘SL g.inverse

Tactic:
rcases hf with ⟨M, rfl⟩
  simp

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

Goal state before:
pp: C : Type u
inst✝¹ : SmallCategory C
inst✝ : FinCategory C
⊢ Finite (Arrow C)

Tactic:
rw [Arrow.finite_iff]

Goal state after:
C : Type u
inst✝¹ : SmallCategory C
inst✝ : FinCategory C
⊢ Nonempty (FinCategory C)
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) → M ⟶ (X i).toModuleCat
J : Type u_2
inst✝ : Category.{v_1, u_2} J
F : J ⥤ TopModuleCat R
c : Cone (F ⋙ forget₂ (TopModuleCat R) (ModuleCat R))
hc : IsLimit c
s : Cone F
m : s.pt ⟶ (ofCone c).pt
H : ∀ (j : J), m ≫ (ofCone c).π.app j = s.π.app j
⊢ m =
    ofHom { toLinearMap := ModuleCat.Hom.hom (hc.lift ((forget₂ (TopModuleCat R) (ModuleCat R)).mapCone s)), cont := ⋯ }

Tactic:
by
    ext x
    refine congr($(hc.uniq ((forget₂ _ _).mapCone s) ((forget₂ _ _).map m) fun j ↦ ?_).hom x)
    ext y
    exact congr($(H j).hom y)

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X Y : TopCat
f : X ⟶ Y
τ : TopologicalSpace (↑Y →₀ R)
x✝ :
  τ ∈
    {t |
      ContinuousSMul R (↑Y →₀ R) ∧
        ContinuousAdd (↑Y →₀ R) ∧ TopologicalSpace.coinduced (fun x ↦ Finsupp.single x 1) Y.str ≤ t}
hτ₁ : ContinuousSMul R (↑Y →₀ R)
hτ₂ : ContinuousAdd (↑Y →₀ R)
hτ₃ : TopologicalSpace.coinduced (fun x ↦ Finsupp.single x 1) Y.str ≤ τ
⊢ TopologicalSpace.coinduced (Finsupp.lmapDomain R R ⇑(TopCat.Hom.hom f)).toFun (freeObj R X).topologicalSpace ≤ τ

Tactic:
rw [coinduced_le_iff_le_induced]

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X Y : TopCat
f : X ⟶ Y
τ : TopologicalSpace (↑Y →₀ R)
x✝ :
  τ ∈
    {t |
      ContinuousSMul R (↑Y →₀ R) ∧
        ContinuousAdd (↑Y →₀ R) ∧ TopologicalSpace.coinduced (fun x ↦ Finsupp.single x 1) Y.str ≤ t}
hτ₁ : ContinuousSMul R (↑Y →₀ R)
hτ₂ : ContinuousAdd (↑Y →₀ R)
hτ₃ : TopologicalSpace.coinduced (fun x ↦ Finsupp.single x 1) Y.str ≤ τ
⊢ (freeObj R X).topologicalSpace ≤ TopologicalSpace.induced (Finsupp.lmapDomain R R ⇑(TopCat.Hom.hom f)).toFun τ
Module: Mathlib.CategoryTheory.Presentable.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F✝ G : C ⥤ D
e : F✝ ≅ G
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
A : C
J : Type w
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
F : J ⥤ C
c : Cocone F
hc : IsColimit c
h : IsFiltered J
this : ∀ (j : J), IsIso ((((const C).obj A).mapCocone c).ι.app j)
⊢ IsColimit (((const C).obj A).mapCocone c)

Tactic:
exact Functor.IsEventuallyConstantFrom.isColimitOfIsIso
              (i₀ := h.nonempty.some) (fun _ _ ↦ by dsimp; infer_instance) _

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u_1
inst✝¹ : Category.{v_1, u_1} J
D : J ⥤ C
c : Cone D
hc : IsLimit c
X : C
inst✝ : PreservesColimit D.op (yoneda.obj X)
f : c.pt ⟶ X
⊢ ∃ j p, c.π.app j ≫ p = f

Tactic:
obtain ⟨j, p, hp⟩ := Types.jointly_surjective_of_isColimit
    (isColimitOfPreserves (yoneda.obj X) hc.op) f
  exact ⟨j.unop, p, hp⟩

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Small

Goal state before:
pp: case inr
P Q : ObjectProperty CommRingCat
inst✝ : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q
hPQ : ∀ (S : CommRingCat), P S → ∃ s, Ideal.span s = ⊤ ∧ ∀ f ∈ s, Q (of (Localization.Away f))
Q' : ObjectProperty CommRingCat
w✝ : ObjectProperty.Small.{u, u, u + 1} Q'
hQ'Q : Q' ≤ Q
hQQ' : Q ≤ Q'.isoClosure
f : (n : ℕ) × (R : Fin n → Subtype Q') × Subring ((i : Fin n) → ↑↑(R i)) → CommRingCat := fun S ↦ of ↥S.snd.snd
S : CommRingCat
hS : P S
s : Set ↑S
hs : Ideal.span s = ⊤
H : ∀ f ∈ s, Q (of (Localization.Away f))
this :
  ∀ (s : Set ↑S),
    Ideal.span s = ⊤ → (∀ f ∈ s, Q (of (Localization.Away f))) → s.Finite → (ObjectProperty.ofObj f).isoClosure S
hs'✝ : ¬s.Finite
s' : Finset ↑S
hs's : ↑s' ⊆ s
hs' : Ideal.span ↑s' = ⊤
⊢ (ObjectProperty.ofObj f).isoClosure S

Tactic:
exact this s' hs' (fun f hf ↦ H f (hs's hf)) s'.finite_toSet

Goal state after: