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

Goal state before:
pp: 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
m : ↑(AddCommGrpCat.FilteredColimits.colimit M)
V : C
b : (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).obj V
⊢ (ConcreteCategory.hom ((M ⋙ forget Ab).map (𝟙 (IsFiltered.max ⟨⟨⋯.some, 1⟩.fst, ⟨⋯.some, 1⟩.snd⟩.fst ⟨V, b⟩.fst))))
      ((ConcreteCategory.hom (R.map (leftToMax ⟨⟨⋯.some, 1⟩.fst, ⟨⋯.some, 1⟩.snd⟩.fst ⟨V, b⟩.fst)))
          ⟨⟨⋯.some, 1⟩.fst, ⟨⋯.some, 1⟩.snd⟩.snd •
        (ConcreteCategory.hom (M.map (rightToMax ⟨⟨⋯.some, 1⟩.fst, ⟨⋯.some, 1⟩.snd⟩.fst ⟨V, b⟩.fst))) ⟨V, b⟩.snd) =
    (ConcreteCategory.hom ((M ⋙ forget Ab).map (rightToMax ⟨⟨⋯.some, 1⟩.fst, ⟨⋯.some, 1⟩.snd⟩.fst V))) b

Tactic:
dsimp

Goal state after:
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
m : ↑(AddCommGrpCat.FilteredColimits.colimit M)
V : C
b : (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).obj V
⊢ (ConcreteCategory.hom (M.map (𝟙 (IsFiltered.max ⋯.some V))))
      ((ConcreteCategory.hom (R.map (leftToMax ⋯.some V))) 1 • (ConcreteCategory.hom (M.map (rightToMax ⋯.some V))) b) =
    (ConcreteCategory.hom (M.map (rightToMax ⋯.some V))) b
Module: Mathlib.Algebra.Category.ModuleCat.Stalk

Goal state before:
pp: 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 : ↑(RingCat.FilteredColimits.colimit R)
U : C
a : (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj U
⊢ (ConcreteCategory.hom ((M ⋙ forget Ab).map (𝟙 (IsFiltered.max ⟨U, a⟩.fst ⟨⟨⋯.some, 0⟩.fst, ⟨⋯.some, 0⟩.snd⟩.fst))))
      ((ConcreteCategory.hom (R.map (leftToMax ⟨U, a⟩.fst ⟨⟨⋯.some, 0⟩.fst, ⟨⋯.some, 0⟩.snd⟩.fst))) ⟨U, a⟩.snd •
        (ConcreteCategory.hom (M.map (rightToMax ⟨U, a⟩.fst ⟨⟨⋯.some, 0⟩.fst, ⟨⋯.some, 0⟩.snd⟩.fst)))
          ⟨⟨⋯.some, 0⟩.fst, ⟨⋯.some, 0⟩.snd⟩.snd) =
    (ConcreteCategory.hom ((M ⋙ forget Ab).map (rightToMax ⟨U, a⟩.fst ⟨⋯.some, 0⟩.fst))) ⟨⋯.some, 0⟩.snd

Tactic:
dsimp

Goal state after:
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 : ↑(RingCat.FilteredColimits.colimit R)
U : C
a : (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj U
⊢ (ConcreteCategory.hom (M.map (𝟙 (IsFiltered.max U ⋯.some))))
      ((ConcreteCategory.hom (R.map (leftToMax U ⋯.some))) a • (ConcreteCategory.hom (M.map (rightToMax U ⋯.some))) 0) =
    (ConcreteCategory.hom (M.map (rightToMax U ⋯.some))) 0
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
inst✝ : ∀ (x : ↑X), IsIso ((stalkFunctor C x).map f.hom)
U : (Opens ↑X)ᵒᵖ
⊢ IsIso (f.hom.app U)

Tactic:
induction U

Goal state after:
case op
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
inst✝ : ∀ (x : ↑X), IsIso ((stalkFunctor C x).map f.hom)
unop✝ : Opens ↑X
⊢ IsIso (f.hom.app (op unop✝))
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
M₁ : Type u_5
M₂ : Type u_6
inst✝²⁰ : Semiring R
inst✝¹⁹ : TopologicalSpace M
inst✝¹⁸ : TopologicalSpace N
inst✝¹⁷ : TopologicalSpace M₁
inst✝¹⁶ : TopologicalSpace M₂
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
inst✝¹³ : ContinuousAdd M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : Module R N
inst✝¹⁰ : ContinuousAdd N
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : Module R M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₂
inst✝⁵ : ContinuousAdd M₁
inst✝⁴ : ContinuousAdd M₂
inst✝³ : Semiring S
inst✝² : Module S M
inst✝¹ : ContinuousConstSMul S M
inst✝ : SMulCommClass R S M
r : S
a : (M₁ →L[R] M) × (M₂ →L[R] M)
⊢ (r • a).1.coprod (r • a).2 = (RingHom.id S) r • a.1.coprod a.2

Tactic:
dsimp

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
M₁ : Type u_5
M₂ : Type u_6
inst✝²⁰ : Semiring R
inst✝¹⁹ : TopologicalSpace M
inst✝¹⁸ : TopologicalSpace N
inst✝¹⁷ : TopologicalSpace M₁
inst✝¹⁶ : TopologicalSpace M₂
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
inst✝¹³ : ContinuousAdd M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : Module R N
inst✝¹⁰ : ContinuousAdd N
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : Module R M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₂
inst✝⁵ : ContinuousAdd M₁
inst✝⁴ : ContinuousAdd M₂
inst✝³ : Semiring S
inst✝² : Module S M
inst✝¹ : ContinuousConstSMul S M
inst✝ : SMulCommClass R S M
r : S
a : (M₁ →L[R] M) × (M₂ →L[R] M)
⊢ (r • a.1).coprod (r • a.2) = r • a.1.coprod a.2
Module: Mathlib.Algebra.Category.ModuleCat.Stalk

Goal state before:
pp: 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
m : ↑(AddCommGrpCat.FilteredColimits.colimit M)
V : C
b : (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).obj V
⊢ (ConcreteCategory.hom ((M ⋙ forget Ab).map (𝟙 (IsFiltered.max ⟨⟨⋯.some, 0⟩.fst, ⟨⋯.some, 0⟩.snd⟩.fst ⟨V, b⟩.fst))))
      ((ConcreteCategory.hom (R.map (leftToMax ⟨⟨⋯.some, 0⟩.fst, ⟨⋯.some, 0⟩.snd⟩.fst ⟨V, b⟩.fst)))
          ⟨⟨⋯.some, 0⟩.fst, ⟨⋯.some, 0⟩.snd⟩.snd •
        (ConcreteCategory.hom (M.map (rightToMax ⟨⟨⋯.some, 0⟩.fst, ⟨⋯.some, 0⟩.snd⟩.fst ⟨V, b⟩.fst))) ⟨V, b⟩.snd) =
    (ConcreteCategory.hom ((M ⋙ forget Ab).map (leftToMax ⟨⋯.some, 0⟩.fst ⟨V, b⟩.fst))) ⟨⋯.some, 0⟩.snd

Tactic:
dsimp

Goal state after:
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
m : ↑(AddCommGrpCat.FilteredColimits.colimit M)
V : C
b : (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).obj V
⊢ (ConcreteCategory.hom (M.map (𝟙 (IsFiltered.max ⋯.some V))))
      ((ConcreteCategory.hom (R.map (leftToMax ⋯.some V))) 0 • (ConcreteCategory.hom (M.map (rightToMax ⋯.some V))) b) =
    (ConcreteCategory.hom (M.map (leftToMax ⋯.some V))) 0
Module: Mathlib.Topology.Algebra.Module.ModuleTopology

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst✝⁷ : Ring R
inst✝⁶ : Ring S
A : Type u_3
inst✝⁵ : AddCommGroup A
inst✝⁴ : Module R A
inst✝³ : TopologicalSpace A
inst✝² : IsModuleTopology R A
B' : Type u_5
inst✝¹ : AddCommGroup B'
inst✝ : Module S B'
σ : R →+* S
hσ : IsOpenQuotientMap ⇑σ
φ : A →ₛₗ[σ] B'
hφ : Function.Surjective ⇑φ
this✝ : ContinuousAdd A
this : TopologicalSpace B' := TopologicalSpace.coinduced (⇑φ) inferInstance
hφo : IsOpenQuotientMap ⇑φ
hA : Continuous[instTopologicalSpaceProd, inst✝³] fun p ↦ p.1 + p.2
hφ2 : (fun p ↦ p.1 + p.2) ∘ Prod.map ⇑φ ⇑φ = ⇑φ ∘ fun p ↦ p.1 + p.2
⊢ Continuous[instTopologicalSpaceProd, TopologicalSpace.coinduced (⇑φ) inst✝³] fun p ↦ p.1 + p.2

Tactic:
rw [← (IsOpenQuotientMap.prodMap hφo hφo).continuous_comp_iff, hφ2]

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst✝⁷ : Ring R
inst✝⁶ : Ring S
A : Type u_3
inst✝⁵ : AddCommGroup A
inst✝⁴ : Module R A
inst✝³ : TopologicalSpace A
inst✝² : IsModuleTopology R A
B' : Type u_5
inst✝¹ : AddCommGroup B'
inst✝ : Module S B'
σ : R →+* S
hσ : IsOpenQuotientMap ⇑σ
φ : A →ₛₗ[σ] B'
hφ : Function.Surjective ⇑φ
this✝ : ContinuousAdd A
this : TopologicalSpace B' := TopologicalSpace.coinduced (⇑φ) inferInstance
hφo : IsOpenQuotientMap ⇑φ
hA : Continuous[instTopologicalSpaceProd, inst✝³] fun p ↦ p.1 + p.2
hφ2 : (fun p ↦ p.1 + p.2) ∘ Prod.map ⇑φ ⇑φ = ⇑φ ∘ fun p ↦ p.1 + p.2
⊢ Continuous[instTopologicalSpaceProd, TopologicalSpace.coinduced (⇑φ) inst✝³] (⇑φ ∘ fun p ↦ p.1 + p.2)
Module: Mathlib.Algebra.Category.ModuleCat.Stalk

Goal state before:
pp: 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
cR : Cocone R
hcR : IsColimit cR
cM : Cocone M
hcM : IsColimit cM
i : C
r : ↑(R.obj i)
m : ↑(M.obj i)
this : Module ↑(RingCat.FilteredColimits.colimit R) ↑(AddCommGrpCat.FilteredColimits.colimit M) :=
  filteredColimitsModule R M ⋯
α✝ : cM.pt ≅ (AddCommGrpCat.FilteredColimits.colimitCocone M).pt :=
  hcM.coconePointUniqueUpToIso (AddCommGrpCat.FilteredColimits.colimitCoconeIsColimit M)
β : cR.pt ≅ (RingCat.FilteredColimits.colimitCocone R).pt :=
  hcR.coconePointUniqueUpToIso (RingCat.FilteredColimits.colimitCoconeIsColimit R)
s : C
α : IsFiltered.max i i ⟶ s
H : leftToMax i i ≫ α = rightToMax i i ≫ α
⊢ (ConcreteCategory.hom
        ((((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).map
          (leftToMax i i ≫ α)))
      (r • m) =
    (ConcreteCategory.hom
        ((((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).map α))
      ((ConcreteCategory.hom (R.map (leftToMax ⟨i, r⟩.fst ⟨i, m⟩.fst))) ⟨i, r⟩.snd •
        (ConcreteCategory.hom (M.map (rightToMax ⟨i, r⟩.fst ⟨i, m⟩.fst))) ⟨i, m⟩.snd)

Tactic:
dsimp

Goal state after:
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
cR : Cocone R
hcR : IsColimit cR
cM : Cocone M
hcM : IsColimit cM
i : C
r : ↑(R.obj i)
m : ↑(M.obj i)
this : Module ↑(RingCat.FilteredColimits.colimit R) ↑(AddCommGrpCat.FilteredColimits.colimit M) :=
  filteredColimitsModule R M ⋯
α✝ : cM.pt ≅ (AddCommGrpCat.FilteredColimits.colimitCocone M).pt :=
  hcM.coconePointUniqueUpToIso (AddCommGrpCat.FilteredColimits.colimitCoconeIsColimit M)
β : cR.pt ≅ (RingCat.FilteredColimits.colimitCocone R).pt :=
  hcR.coconePointUniqueUpToIso (RingCat.FilteredColimits.colimitCoconeIsColimit R)
s : C
α : IsFiltered.max i i ⟶ s
H : leftToMax i i ≫ α = rightToMax i i ≫ α
⊢ (ConcreteCategory.hom (M.map (leftToMax i i ≫ α))) (r • m) =
    (ConcreteCategory.hom (M.map α))
      ((ConcreteCategory.hom (R.map (leftToMax i i))) r • (ConcreteCategory.hom (M.map (rightToMax i i))) m)
Module: Mathlib.Algebra.Category.ModuleCat.Stalk

Goal state before:
pp: X : TopCat
R : TopCat.Presheaf RingCat X
M : PresheafOfModules R
x : ↑X
i : (OpenNhds x)ᵒᵖ
⊢ Module ↑(((OpenNhds.inclusion x).op ⋙ R).obj i) ↑(((OpenNhds.inclusion x).op ⋙ M.presheaf).obj i)

Tactic:
dsimp

Goal state after:
X : TopCat
R : TopCat.Presheaf RingCat X
M : PresheafOfModules R
x : ↑X
i : (OpenNhds x)ᵒᵖ
⊢ Module ↑(R.obj (op ((OpenNhds.inclusion x).obj (unop i)))) ↑(M.obj (op ((OpenNhds.inclusion x).obj (unop i))))
Module: Mathlib.Algebra.Category.ModuleCat.Stalk

Goal state before:
pp: X : TopCat
R : TopCat.Presheaf RingCat X
M : PresheafOfModules R
x : ↑X
U : Opens ↑X
hx : x ∈ U
r : ↑(R.obj (op U))
m : ↑(M.obj (op U))
i : (OpenNhds x)ᵒᵖ
⊢ Module ↑(((OpenNhds.inclusion x).op ⋙ R).obj i) ↑(((OpenNhds.inclusion x).op ⋙ M.presheaf).obj i)

Tactic:
dsimp

Goal state after:
X : TopCat
R : TopCat.Presheaf RingCat X
M : PresheafOfModules R
x : ↑X
U : Opens ↑X
hx : x ∈ U
r : ↑(R.obj (op U))
m : ↑(M.obj (op U))
i : (OpenNhds x)ᵒᵖ
⊢ Module ↑(R.obj (op ((OpenNhds.inclusion x).obj (unop i)))) ↑(M.obj (op ((OpenNhds.inclusion x).obj (unop i))))
Module: Mathlib.Algebra.Category.ModuleCat.Stalk

Goal state before:
pp: X✝ : TopCat
R✝ : TopCat.Presheaf RingCat X✝
M✝ : PresheafOfModules R✝
x✝ : ↑X✝
X : TopCat
R : TopCat.Presheaf CommRingCat X
M : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
x : ↑X
i : (OpenNhds x)ᵒᵖ
⊢ Module ↑(((OpenNhds.inclusion x).op ⋙ R ⋙ forget₂ CommRingCat RingCat).obj i)
    ↑(((OpenNhds.inclusion x).op ⋙ M.presheaf).obj i)

Tactic:
dsimp

Goal state after:
X✝ : TopCat
R✝ : TopCat.Presheaf RingCat X✝
M✝ : PresheafOfModules R✝
x✝ : ↑X✝
X : TopCat
R : TopCat.Presheaf CommRingCat X
M : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
x : ↑X
i : (OpenNhds x)ᵒᵖ
⊢ Module ↑(R.obj (op ((OpenNhds.inclusion x).obj (unop i)))) ↑(M.obj (op ((OpenNhds.inclusion x).obj (unop i))))
Module: Mathlib.Algebra.Category.ModuleCat.Stalk

Goal state before:
pp: X : TopCat
R : TopCat.Presheaf CommRingCat X
M : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
x : ↑X
U : Opens ↑X
hx : x ∈ U
r : ↑(R.obj (op U))
m : ↑(M.obj (op U))
i : (OpenNhds x)ᵒᵖ
⊢ Module ↑(((OpenNhds.inclusion x).op ⋙ R ⋙ forget₂ CommRingCat RingCat).obj i)
    ↑(((OpenNhds.inclusion x).op ⋙ M.presheaf).obj i)

Tactic:
dsimp

Goal state after:
X : TopCat
R : TopCat.Presheaf CommRingCat X
M : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
x : ↑X
U : Opens ↑X
hx : x ∈ U
r : ↑(R.obj (op U))
m : ↑(M.obj (op U))
i : (OpenNhds x)ᵒᵖ
⊢ Module ↑(R.obj (op ((OpenNhds.inclusion x).obj (unop i)))) ↑(M.obj (op ((OpenNhds.inclusion x).obj (unop i))))
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝¹⁸ : Semiring R
inst✝¹⁷ : Semiring S
inst✝¹⁶ : Semiring T
inst✝¹⁵ : Module R S
inst✝¹⁴ : AddCommMonoid M₂
inst✝¹³ : Module R M₂
inst✝¹² : Module S M₂
inst✝¹¹ : IsScalarTower R S M₂
inst✝¹⁰ : TopologicalSpace S
inst✝⁹ : TopologicalSpace M₂
inst✝⁸ : ContinuousSMul S M₂
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : ContinuousAdd M₂
inst✝³ : Module T M₂
inst✝² : ContinuousConstSMul T M₂
inst✝¹ : SMulCommClass R T M₂
inst✝ : SMulCommClass S T M₂
c : M →L[R] S
a : T
x : M₂
e : M
⊢ (c.smulRight (a • x)) e = ((RingHom.id T) a • c.smulRight x) e

Tactic:
dsimp

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝¹⁸ : Semiring R
inst✝¹⁷ : Semiring S
inst✝¹⁶ : Semiring T
inst✝¹⁵ : Module R S
inst✝¹⁴ : AddCommMonoid M₂
inst✝¹³ : Module R M₂
inst✝¹² : Module S M₂
inst✝¹¹ : IsScalarTower R S M₂
inst✝¹⁰ : TopologicalSpace S
inst✝⁹ : TopologicalSpace M₂
inst✝⁸ : ContinuousSMul S M₂
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : ContinuousAdd M₂
inst✝³ : Module T M₂
inst✝² : ContinuousConstSMul T M₂
inst✝¹ : SMulCommClass R T M₂
inst✝ : SMulCommClass S T M₂
c : M →L[R] S
a : T
x : M₂
e : M
⊢ c e • a • x = (a • c.smulRight x) e
Module: Mathlib.Algebra.Category.ModuleCat.Ulift

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : Small.{v, u} R
M : ModuleCat R
proj : Projective M
this : Small.{max v v', u} R
⊢ Projective ((uliftFunctor.{v', v, u} R).obj M)

Tactic:
dsimp

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : Small.{v, u} R
M : ModuleCat R
proj : Projective M
this : Small.{max v v', u} R
⊢ Projective (of R (ULift.{v', v} ↑M))
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Homology

Goal state before:
pp: 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)
hF' : Topology.IsEmbedding ⇑(ConcreteCategory.hom F)
⊢ IsIso F

Tactic:
rw [← isIso_iff_of_reflects_iso _ (forget₂ (TopModuleCat R) TopCat),
    TopCat.isIso_iff_isHomeomorph, isHomeomorph_iff_isEmbedding_surjective]

Goal state after:
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)
hF' : Topology.IsEmbedding ⇑(ConcreteCategory.hom F)
⊢ Topology.IsEmbedding ⇑(ConcreteCategory.hom ((forget₂ (TopModuleCat R) TopCat).map F)) ∧
    Function.Surjective ⇑(ConcreteCategory.hom ((forget₂ (TopModuleCat R) TopCat).map F))
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : Semiring R
M : Type u_2
inst✝⁹ : TopologicalSpace M
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M₂
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
ι : Type u_4
φ : ι → Type u_5
inst✝³ : (i : ι) → TopologicalSpace (φ i)
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
I J : Set ι
inst✝ : DecidablePred fun i ↦ i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
i : ι
⊢ Continuous[Pi.topologicalSpace, inst✝³ i] fun a ↦
    (LinearMap.pi fun i ↦ if h : i ∈ I then LinearMap.proj ⟨i, h⟩ else 0) a i

Tactic:
dsimp

Goal state after:
R : Type u_1
inst✝¹⁰ : Semiring R
M : Type u_2
inst✝⁹ : TopologicalSpace M
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M₂
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
ι : Type u_4
φ : ι → Type u_5
inst✝³ : (i : ι) → TopologicalSpace (φ i)
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
I J : Set ι
inst✝ : DecidablePred fun i ↦ i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
i : ι
⊢ Continuous[Pi.topologicalSpace, inst✝³ i] fun a ↦ (if h : i ∈ I then LinearMap.proj ⟨i, h⟩ else 0) a
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: case h
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
F : (M →L[R] M)ˣ
hF : ↑F = ↑e.symm ∘SL f
x✝ : M
⊢ ↑(((ContinuousLinearEquiv.unitsEquiv R M) F).trans e) x✝ = f x✝

Tactic:
dsimp

Goal state after:
case h
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
F : (M →L[R] M)ˣ
hF : ↑F = ↑e.symm ∘SL f
x✝ : M
⊢ e (↑F x✝) = f x✝
Module: Mathlib.CategoryTheory.Limits.Preserves.Over

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : C
J : Type u_3
hJ : Category.{u_2, u_3} J
hJ' : IsFiltered J
F : J ⥤ Under X
c : Cocone F
hc : IsColimit c
s : Cocone (F ⋙ Under.forget X)
i j k : J
e : j ⟶ k
⊢ Under.Hom.right (F.map e ≫ Under.homMk (s.ι.app k) ⋯) =
    Under.Hom.right (Under.homMk (s.ι.app j) ⋯ ≫ ((Functor.const J).obj (Under.mk ((F.obj i).hom ≫ s.ι.app i))).map e)

Tactic:
simpa using s.w e

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantTo i₀
inst✝ : IsCofiltered J
j j' : J
φ : j ⟶ j'
⊢ ((const J).obj (F.obj i₀)).map φ ≫ h.coneπApp j' = h.coneπApp j ≫ F.map φ

Tactic:
dsimp

Goal state after:
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantTo i₀
inst✝ : IsCofiltered J
j j' : J
φ : j ⟶ j'
⊢ 𝟙 (F.obj i₀) ≫ h.coneπApp j' = h.coneπApp j ≫ F.map φ
Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝³ : Category.{v_1, u_1} J
inst✝² : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantTo i₀
inst✝¹ : IsCofiltered J
c : Cone F
inst✝ : IsIso (c.π.app i₀)
j : J
i : J := IsCofiltered.min i₀ j
α : i ⟶ i₀ := minToLeft i₀ j
β : i ⟶ j := minToRight i₀ j
⊢ h.cone.π.app j = (asIso (c.π.app i₀)).symm.hom ≫ c.π.app j

Tactic:
dsimp

Goal state after:
J : Type u_1
C : Type u_2
inst✝³ : Category.{v_1, u_1} J
inst✝² : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantTo i₀
inst✝¹ : IsCofiltered J
c : Cone F
inst✝ : IsIso (c.π.app i₀)
j : J
i : J := IsCofiltered.min i₀ j
α : i ⟶ i₀ := minToLeft i₀ j
β : i ⟶ j := minToRight i₀ j
⊢ h.coneπApp j = CategoryTheory.inv (c.π.app i₀) ≫ c.π.app j
Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
inst✝ : IsFiltered J
j j' : J
φ : j ⟶ j'
⊢ F.map φ ≫ h.coconeιApp j' = h.coconeιApp j ≫ ((const J).obj (F.obj i₀)).map φ

Tactic:
dsimp

Goal state after:
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
inst✝ : IsFiltered J
j j' : J
φ : j ⟶ j'
⊢ F.map φ ≫ h.coconeιApp j' = h.coconeιApp j ≫ 𝟙 (F.obj i₀)
Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝³ : Category.{v_1, u_1} J
inst✝² : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
inst✝¹ : IsFiltered J
c : Cocone F
inst✝ : IsIso (c.ι.app i₀)
j : J
i : J := IsFiltered.max i₀ j
α : i₀ ⟶ i := leftToMax i₀ j
β : j ⟶ i := rightToMax i₀ j
⊢ h.cocone.ι.app j ≫ (asIso (c.ι.app i₀)).hom = c.ι.app j

Tactic:
dsimp

Goal state after:
J : Type u_1
C : Type u_2
inst✝³ : Category.{v_1, u_1} J
inst✝² : Category.{v_2, u_2} C
F : J ⥤ C
i₀ : J
h : F.IsEventuallyConstantFrom i₀
inst✝¹ : IsFiltered J
c : Cocone F
inst✝ : IsIso (c.ι.app i₀)
j : J
i : J := IsFiltered.max i₀ j
α : i₀ ⟶ i := leftToMax i₀ j
β : j ⟶ i := rightToMax i₀ j
⊢ h.coconeιApp j ≫ c.ι.app i₀ = c.ι.app j