mathlib-initiative/mathlib-tactics huggingface dataset:
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)
⊢ IsIso f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd

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₂
M₃ : Type u_4
inst✝² : TopologicalSpace M₃
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
L : M₁ × M₂ →L[R] M₃
v : M₁ × M₂
⊢ (L ∘SL inl R M₁ M₂) v.1 + (L ∘SL inr R M₁ M₂) v.2 = L v

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd

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₂
M₃ : Type u_4
inst✝² : TopologicalSpace M₃
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
f : M₁ →L[R] M₂
g : M₁ →L[R] M₃
⊢ (↑(f.prod g)).ker = (↑f).ker ⊓ (↑g).ker

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd

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
ι : Type u_4
φ : ι → Type u_5
inst✝² : (i : ι) → TopologicalSpace (φ i)
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
f : (i : ι) → M →L[R] φ i
⊢ pi f = 0 ↔ ∀ (i : ι), f i = 0

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd

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)
α : Type u_6
f : α → ι
⊢ ∀ (x y : (i : ι) → φ i), (fun i ↦ (x + y) (f i)) = (fun i ↦ x (f i)) + fun i ↦ y (f i)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd

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)
α : Type u_6
f : α → ι
⊢ ∀ (m : R) (x : (i : ι) → φ i), (fun i ↦ (m • x) (f i)) = (RingHom.id R) m • fun i ↦ x (f i)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd

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
ι : Type u_4
φ : ι → Type u_5
inst✝⁴ : (i : ι) → TopologicalSpace (φ i)
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
L : ((i : ι) → φ i) →L[R] M
v : (i : ι) → φ i
⊢ ∑ i, (L ∘SL single R φ i) (v i) = L v

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd

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₂
M₃ : Type u_4
inst✝² : TopologicalSpace M₃
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
f g : M × M₂ →L[R] M₃
⊢ f = g ↔ f ∘SL inl R M M₂ = g ∘SL inl R M M₂ ∧ f ∘SL inr R M M₂ = g ∘SL inr R M M₂

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd

Goal state before:
pp: R : Type u_1
M : Type u_3
M₁ : Type u_5
M₂ : Type u_6
inst✝¹⁰ : Semiring R
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₁
inst✝⁷ : TopologicalSpace M₂
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : ContinuousAdd M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f₁ g₁ : M₁ →L[R] M
f₂ g₂ : M₂ →L[R] M
⊢ (f₁ + g₁).coprod (f₂ + g₂) = f₁.coprod f₂ + g₁.coprod g₂

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd

Goal state before:
pp: R : Type u_1
M : Type u_3
M₁ : Type u_5
M₂ : Type u_6
inst✝¹² : Semiring R
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : TopologicalSpace M₁
inst✝⁹ : TopologicalSpace M₂
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : ContinuousAdd M
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : Module R M₁
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : ContinuousAdd M₁
inst✝ : ContinuousAdd M₂
f : M × M₁ →L[R] M₂
⊢ (f ∘SL inl R M M₁).coprod (f ∘SL inr R M M₁) = f

Tactic:
by

Goal state after:
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:
by

Goal state after:
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
f : (M₁ →L[R] M) × (M₂ →L[R] M)
⊢ (fun f ↦ (f ∘SL inl R M₁ M₂, f ∘SL inr R M₁ M₂)) ((fun f ↦ f.1.coprod f.2) f) = f

Tactic:
by

Goal state after:
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
f : M₁ × M₂ →L[R] M
⊢ (fun f ↦ f.1.coprod f.2) ((fun f ↦ (f ∘SL inl R M₁ M₂, f ∘SL inr R M₁ M₂)) f) = f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict

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
p : Submodule R M
x : ↥p
⊢ p.subtypeL x = ↑x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
inst✝⁸ : Semiring R₁
inst✝⁷ : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M₁
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : Module R₁ M₁
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₂ M₂
inst✝ : RingHomSurjective σ₁₂
f : M₁ →SL[σ₁₂] M₂
⊢ ↑f.rangeRestrict = (↑f).rangeRestrict

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝⁹ : Ring R₁
inst✝⁸ : Ring R₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst✝⁷ : RingHomInvPair σ₁₂ σ₂₁
M₁ : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M₁
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : Module R₁ M₁
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
inst✝ : IsTopologicalAddGroup M₁
f₁ : M₁ →SL[σ₁₂] M₂
f₂ : M₂ →SL[σ₂₁] M₁
h : Function.RightInverse ⇑f₂ ⇑f₁
x : M₁
⊢ (ContinuousLinearMap.id R₁ M₁ - f₂ ∘SL f₁) x ∈ (↑f₁).ker

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
inst✝⁹ : Ring R₁
inst✝⁸ : Ring R₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst✝⁷ : RingHomInvPair σ₁₂ σ₂₁
M₁ : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M₁
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : Module R₁ M₁
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
inst✝ : IsTopologicalAddGroup M₁
f₁ : M₁ →SL[σ₁₂] M₂
f₂ : M₂ →SL[σ₂₁] M₁
h : Function.RightInverse ⇑f₂ ⇑f₁
x : ↥(↑f₁).ker
⊢ (f₁.projKerOfRightInverse f₂ h) ↑x = x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
inst✝⁹ : Ring R₁
inst✝⁸ : Ring R₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst✝⁷ : RingHomInvPair σ₁₂ σ₂₁
M₁ : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M₁
inst✝⁵ : AddCommGroup M₁
inst✝⁴ : Module R₁ M₁
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
inst✝ : IsTopologicalAddGroup M₁
f₁ : M₁ →SL[σ₁₂] M₂
f₂ : M₂ →SL[σ₂₁] M₁
h : Function.RightInverse ⇑f₂ ⇑f₁
y : M₂
⊢ ↑((f₁.projKerOfRightInverse f₂ h) (f₂ y)) = ↑0

Tactic:
by

Goal state after:
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)
m n : ↑(AddCommGrpCat.FilteredColimits.colimit M)
⊢ ∀ (a : (j : C) × (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j)
    (b c : (j : C) × (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).obj j),
    Quot.mk (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel a •
        (Quot.mk
            (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).ColimitTypeRel
            b +
          Quot.mk
            (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).ColimitTypeRel
            c) =
      Quot.mk (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel a •
          Quot.mk
            (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).ColimitTypeRel
            b +
        Quot.mk (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel a •
          Quot.mk
            (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).ColimitTypeRel c

Tactic:
by

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

Goal state before:
pp: case property.refine_3
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s✝ : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
ι : ULift.{w, 0} WalkingPair → Opens ↑X :=
  fun x ↦
    match x with
    | { down := j } => WalkingPair.casesOn j U V
hι : U ⊔ V = iSup ι
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
⊢ ∀ {m : s.pt ⟶ (F.interUnionPullbackCone U V).pt},
    m ≫ (F.interUnionPullbackCone U V).fst = s.fst →
      m ≫ (F.interUnionPullbackCone U V).snd = s.snd → m = F.interUnionPullbackConeLift U V s

Tactic:
· intro m h₁ h₂
    rw [← cancel_mono (F.1.map (eqToHom hι.symm).op)]
    apply (F.presheaf.isSheaf_iff_isSheafPairwiseIntersections.mp F.2 ι).some.hom_ext
    rintro ((_ | _) | (_ | _)) <;>
    rw [Category.assoc, Category.assoc, Functor.mapCone_π_app, ← F.1.map_comp]
    · convert! h₁
      apply interUnionPullbackConeLift_left
    · convert! h₂
      apply interUnionPullbackConeLift_right
    all_goals
      dsimp only [Functor.op, Pairwise.cocone_ι_app, Functor.mapCone_π_app, Cocone.op,
        Pairwise.coconeιApp, unop_op, op_comp, NatTrans.op]
      simp_rw [F.1.map_comp, ← Category.assoc]
      congr 1
      simp_rw [Category.assoc, ← F.1.map_comp]
    · convert! h₁
      apply interUnionPullbackConeLift_left
    · convert! h₂
      apply interUnionPullbackConeLift_right

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
F : Sheaf C X
U V : Opens ↑X
s : PullbackCone (F.obj.map (homOfLE ⋯).op) (F.obj.map (homOfLE ⋯).op)
⊢ IsLimit (F.interUnionPullbackCone U V)

Tactic:
by

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'
⊢ τB' = moduleTopology S B'

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
τR : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
⊢ IsModuleTopology R R

Tactic:
by

Goal state after:
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 s : ↑(RingCat.FilteredColimits.colimit R)
m : ↑(AddCommGrpCat.FilteredColimits.colimit M)
⊢ ∀ (a b : (j : C) × (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j)
    (c : (j : C) × (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).obj j),
    (Quot.mk (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel a +
          Quot.mk (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel b) •
        Quot.mk
          (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).ColimitTypeRel c =
      Quot.mk (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel a •
          Quot.mk
            (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).ColimitTypeRel
            c +
        Quot.mk (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).ColimitTypeRel b •
          Quot.mk
            (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).ColimitTypeRel c

Tactic:
by

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
A : Type u_3
inst✝⁶ : AddCommMonoid A
inst✝⁵ : Module R A
aA : TopologicalSpace A
inst✝⁴ : IsModuleTopology R A
B' : Type u_5
inst✝³ : AddCommMonoid B'
inst✝² : Module S B'
aB' : TopologicalSpace B'
inst✝¹ : ContinuousAdd B'
inst✝ : ContinuousSMul S B'
σ : R →* S
hσ : Continuous ⇑σ
φ : A →ₑ+[σ] B'
⊢ Continuous ⇑φ

Tactic:
by

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

Goal state before:
pp: R : Type u_6
A : Type u_7
B : Type u_8
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Semiring B
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalSpace A
inst✝² : IsModuleTopology R A
inst✝¹ : TopologicalSpace B
inst✝ : IsTopologicalSemiring B
φ : A →+* B
hφ : Continuous ⇑(φ.comp (algebraMap R A))
inst : Module R B := Module.compHom B (φ.comp (algebraMap R A))
r : R
m : A
⊢ (↑φ).toFun (r • m) = (RingHom.id R) r • (↑φ).toFun m

Tactic:
by

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

Goal state before:
pp: R : Type u_6
A : Type u_7
B : Type u_8
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Semiring B
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalSpace A
inst✝² : IsModuleTopology R A
inst✝¹ : TopologicalSpace B
inst✝ : IsTopologicalSemiring B
φ : A →+* B
hφ : Continuous ⇑(φ.comp (algebraMap R A))
⊢ Continuous ⇑φ

Tactic:
by

Goal state after:
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)
⊢ ∀ (a : (j : C) × (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).obj j),
    0 •
        Quot.mk
          (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).ColimitTypeRel a =
      0

Tactic:
by

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✝⁷ : 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
⊢ (fun p ↦ p.1 • p.2) ∘ Prod.map ⇑σ ⇑φ = ⇑φ ∘ fun p ↦ p.1 • p.2

Tactic:
by

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✝⁷ : 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
⊢ (fun p ↦ p.1 + p.2) ∘ Prod.map ⇑φ ⇑φ = ⇑φ ∘ fun p ↦ p.1 + p.2

Tactic:
by

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✝⁸ : 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'
τB : TopologicalSpace B'
inst✝ : IsModuleTopology S B'
σ : R →+* S
hσ : IsOpenQuotientMap ⇑σ
φ : A →ₛₗ[σ] B'
hφ : Function.Surjective ⇑φ
⊢ τB = TopologicalSpace.coinduced (⇑φ) inst✝⁴

Tactic:
by

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✝¹⁰ : Ring R
inst✝⁹ : Ring S
A : Type u_3
inst✝⁸ : AddCommGroup A
inst✝⁷ : Module R A
inst✝⁶ : TopologicalSpace A
B' : Type u_5
inst✝⁵ : AddCommGroup B'
inst✝⁴ : Module S B'
inst✝³ : TopologicalSpace B'
inst✝² : IsModuleTopology S B'
inst✝¹ : ContinuousAdd A
inst✝ : ContinuousSMul R A
σ : R →+* S
hσ : IsOpenQuotientMap ⇑σ
φ : A →ₛₗ[σ] B'
hφ : Function.Surjective ⇑φ
⊢ IsOpenMap ⇑φ

Tactic:
by

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✝⁷ : 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 ⇑φ
⊢ moduleTopology S B' = TopologicalSpace.coinduced (⇑φ) inferInstance

Tactic:
by

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✝⁹ : 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_4
inst✝³ : AddCommGroup B
inst✝² : Module R B
B' : Type u_5
inst✝¹ : AddCommGroup B'
inst✝ : Module S✝ B'
S : Submodule R A
⊢ IsModuleTopology R (A ⧸ S)

Tactic:
by

Goal state after:
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)
⊢ (ConcreteCategory.hom (cM.ι.app i)) (r • m) =
    (ConcreteCategory.hom (cR.ι.app i)) r • (ConcreteCategory.hom (cM.ι.app i)) m

Tactic:
by

Goal state after:
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
⊢ IsModuleTopology R (M × N)

Tactic:
by

Goal state after:
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:
by

Goal state after:
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:
by

Goal state after: