mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Module.Basic

Goal state before:
pp: case refine_1
ι : 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)
⊢ ↑(⨆ i, map (LinearMap.single R M i) (s i)) ⊆ Set.univ.pi fun i ↦ ↑(s i)

pp: case refine_2
ι : 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)
⊢ (Set.univ.pi fun i ↦ ↑(s i)) ⊆ closure[Pi.topologicalSpace] ↑(⨆ i, map (LinearMap.single R M i) (s i))

Tactic:
·

Goal state after:
case refine_1
ι : 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)
⊢ ↑(⨆ i, map (LinearMap.single R M i) (s i)) ⊆ Set.univ.pi fun i ↦ ↑(s i)
Module: Mathlib.Topology.Algebra.Module.Basic

Goal state before:
pp: case refine_2
ι : 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)
⊢ (Set.univ.pi fun i ↦ ↑(s i)) ⊆ closure[Pi.topologicalSpace] ↑(⨆ i, map (LinearMap.single R M i) (s i))

Tactic:
·

Goal state after:
case refine_2
ι : 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)
⊢ (Set.univ.pi fun i ↦ ↑(s i)) ⊆ closure[Pi.topologicalSpace] ↑(⨆ i, map (LinearMap.single R M i) (s i))
Module: Mathlib.Topology.Algebra.Module.Basic

Goal state before:
pp: case refine_2.refine_1
ι : 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)
x : (i : ι) → M i
hx : x ∈ Set.univ.pi fun i ↦ ↑(s i)
U : Set ((i : ι) → M i)
hU : IsOpen[Pi.topologicalSpace] U
hxU : x ∈ U
t : Finset ι
V : (a : ι) → Set (M a)
hV : ∀ a ∈ t, IsOpen[inst✝¹ a] (V a) ∧ x a ∈ V a
hVU : (↑t).pi V ⊆ U
⊢ ∑ i ∈ t, Pi.single i (x i) ∈ (↑t).pi V

pp: case refine_2.refine_2
ι : 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)
x : (i : ι) → M i
hx : x ∈ Set.univ.pi fun i ↦ ↑(s i)
U : Set ((i : ι) → M i)
hU : IsOpen[Pi.topologicalSpace] U
hxU : x ∈ U
t : Finset ι
V : (a : ι) → Set (M a)
hV : ∀ a ∈ t, IsOpen[inst✝¹ a] (V a) ∧ x a ∈ V a
hVU : (↑t).pi V ⊆ U
⊢ ∑ i ∈ t, Pi.single i (x i) ∈ ↑(⨆ i, map (LinearMap.single R M i) (s i))

Tactic:
·

Goal state after:
case refine_2.refine_1
ι : 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)
x : (i : ι) → M i
hx : x ∈ Set.univ.pi fun i ↦ ↑(s i)
U : Set ((i : ι) → M i)
hU : IsOpen[Pi.topologicalSpace] U
hxU : x ∈ U
t : Finset ι
V : (a : ι) → Set (M a)
hV : ∀ a ∈ t, IsOpen[inst✝¹ a] (V a) ∧ x a ∈ V a
hVU : (↑t).pi V ⊆ U
⊢ ∑ i ∈ t, Pi.single i (x i) ∈ (↑t).pi V
Module: Mathlib.Topology.Algebra.Module.Basic

Goal state before:
pp: case refine_2.refine_2
ι : 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)
x : (i : ι) → M i
hx : x ∈ Set.univ.pi fun i ↦ ↑(s i)
U : Set ((i : ι) → M i)
hU : IsOpen[Pi.topologicalSpace] U
hxU : x ∈ U
t : Finset ι
V : (a : ι) → Set (M a)
hV : ∀ a ∈ t, IsOpen[inst✝¹ a] (V a) ∧ x a ∈ V a
hVU : (↑t).pi V ⊆ U
⊢ ∑ i ∈ t, Pi.single i (x i) ∈ ↑(⨆ i, map (LinearMap.single R M i) (s i))

Tactic:
·

Goal state after:
case refine_2.refine_2
ι : 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)
x : (i : ι) → M i
hx : x ∈ Set.univ.pi fun i ↦ ↑(s i)
U : Set ((i : ι) → M i)
hU : IsOpen[Pi.topologicalSpace] U
hxU : x ∈ U
t : Finset ι
V : (a : ι) → Set (M a)
hV : ∀ a ∈ t, IsOpen[inst✝¹ a] (V a) ∧ x a ∈ V a
hVU : (↑t).pi V ⊆ U
⊢ ∑ i ∈ t, Pi.single i (x i) ∈ ↑(⨆ i, map (LinearMap.single R M i) (s 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
this : IsCompatible F.obj V sf
s : ToType (F.obj.obj (op U))
s_spec : ∀ (i : ↥U), (ConcreteCategory.hom (F.obj.map (iVU i).op)) s = sf i
⊢ ∃ a, (ConcreteCategory.hom (f.hom.app (op U))) a = t

Tactic:
·

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
this : IsCompatible F.obj V sf
s : ToType (F.obj.obj (op U))
s_spec : ∀ (i : ↥U), (ConcreteCategory.hom (F.obj.map (iVU i).op)) s = sf i
⊢ ∃ a, (ConcreteCategory.hom (f.hom.app (op U))) a = t
Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Goal state before:
pp: case mp
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 := ⋯
x✝ : ↑X
⊢ x✝ ∈ ↑(U ⊔ V) →
    ∃ i,
      x✝ ∈
        ↑(match i with
          | { down := j } => WalkingPair.casesOn j U V)

pp: case mpr
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 := ⋯
x✝ : ↑X
⊢ (∃ i,
      x✝ ∈
        ↑(match i with
          | { down := j } => WalkingPair.casesOn j U V)) →
    x✝ ∈ ↑(U ⊔ V)

Tactic:
·

Goal state after:
case mp
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 := ⋯
x✝ : ↑X
⊢ x✝ ∈ ↑(U ⊔ V) →
    ∃ i,
      x✝ ∈
        ↑(match i with
          | { down := j } => WalkingPair.casesOn j U V)
Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Goal state before:
pp: case mpr
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 := ⋯
x✝ : ↑X
⊢ (∃ i,
      x✝ ∈
        ↑(match i with
          | { down := j } => WalkingPair.casesOn j U V)) →
    x✝ ∈ ↑(U ⊔ V)

Tactic:
·

Goal state after:
case mpr
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 := ⋯
x✝ : ↑X
⊢ (∃ i,
      x✝ ∈
        ↑(match i with
          | { down := j } => WalkingPair.casesOn j U V)) →
    x✝ ∈ ↑(U ⊔ V)
Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Goal state before:
pp: case property.refine_1
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)
⊢ F.interUnionPullbackConeLift U V s ≫ (F.interUnionPullbackCone U V).fst = s.fst

pp: case property.refine_2
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)
⊢ F.interUnionPullbackConeLift U V s ≫ (F.interUnionPullbackCone U V).snd = s.snd

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:
·

Goal state after:
case property.refine_1
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)
⊢ F.interUnionPullbackConeLift U V s ≫ (F.interUnionPullbackCone U V).fst = s.fst
Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Goal state before:
pp: case property.refine_2
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)
⊢ F.interUnionPullbackConeLift U V s ≫ (F.interUnionPullbackCone U V).snd = s.snd

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:
·

Goal state after:
case property.refine_2
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)
⊢ F.interUnionPullbackConeLift U V s ≫ (F.interUnionPullbackCone U V).snd = s.snd
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:
·

Goal state after:
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
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
⊢ ∀ (a : (j : C) × (R ⋙ forget RingCat).obj j) (b₁ b₂ : (j : C) × (M ⋙ forget Ab).obj j),
    (M ⋙ forget Ab).ColimitTypeRel b₁ b₂ →
      (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)

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:
·

Goal state after:
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
⊢ ∀ (a : (j : C) × (R ⋙ forget RingCat).obj j) (b₁ b₂ : (j : C) × (M ⋙ forget Ab).obj j),
    (M ⋙ forget Ab).ColimitTypeRel b₁ b₂ →
      (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)
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:
·

Goal state after:
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)
Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Goal state before:
pp: case property.refine_3.pair.left.e_a
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
h₁ : m ≫ (F.interUnionPullbackCone U V).fst = s.fst
h₂ : m ≫ (F.interUnionPullbackCone U V).snd = s.snd
a✝ : ULift.{w, 0} WalkingPair
⊢ m ≫ F.obj.map ((eqToHom ⋯).op ≫ (homOfLE ⋯).op) =
    F.interUnionPullbackConeLift U V s ≫ F.obj.map ((eqToHom ⋯).op ≫ (homOfLE ⋯).op)

pp: case property.refine_3.pair.right.e_a
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
h₁ : m ≫ (F.interUnionPullbackCone U V).fst = s.fst
h₂ : m ≫ (F.interUnionPullbackCone U V).snd = s.snd
a✝ : ULift.{w, 0} WalkingPair
⊢ m ≫ F.obj.map ((eqToHom ⋯).op ≫ (homOfLE ⋯).op) =
    F.interUnionPullbackConeLift U V s ≫ F.obj.map ((eqToHom ⋯).op ≫ (homOfLE ⋯).op)

Tactic:
·

Goal state after:
case property.refine_3.pair.left.e_a
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
h₁ : m ≫ (F.interUnionPullbackCone U V).fst = s.fst
h₂ : m ≫ (F.interUnionPullbackCone U V).snd = s.snd
a✝ : ULift.{w, 0} WalkingPair
⊢ m ≫ F.obj.map ((eqToHom ⋯).op ≫ (homOfLE ⋯).op) =
    F.interUnionPullbackConeLift U V s ≫ F.obj.map ((eqToHom ⋯).op ≫ (homOfLE ⋯).op)
Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Goal state before:
pp: case property.refine_3.pair.right.e_a
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
h₁ : m ≫ (F.interUnionPullbackCone U V).fst = s.fst
h₂ : m ≫ (F.interUnionPullbackCone U V).snd = s.snd
a✝ : ULift.{w, 0} WalkingPair
⊢ m ≫ F.obj.map ((eqToHom ⋯).op ≫ (homOfLE ⋯).op) =
    F.interUnionPullbackConeLift U V s ≫ F.obj.map ((eqToHom ⋯).op ≫ (homOfLE ⋯).op)

Tactic:
·

Goal state after:
case property.refine_3.pair.right.e_a
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
h₁ : m ≫ (F.interUnionPullbackCone U V).fst = s.fst
h₂ : m ≫ (F.interUnionPullbackCone U V).snd = s.snd
a✝ : ULift.{w, 0} WalkingPair
⊢ m ≫ F.obj.map ((eqToHom ⋯).op ≫ (homOfLE ⋯).op) =
    F.interUnionPullbackConeLift U V s ≫ F.obj.map ((eqToHom ⋯).op ≫ (homOfLE ⋯).op)