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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R✝ : Sheaf J RingCat
inst✝³ : ∀ (X : C), HasSheafify (J.over X) AddCommGrpCat
inst✝² : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat
inst✝¹ : ∀ (X : C) (Y : Over X), HasSheafify ((J.over X).over Y) AddCommGrpCat
inst✝ : ∀ (X : C) (Y : Over X), ((J.over X).over Y).WEqualsLocallyBijective AddCommGrpCat
R : Sheaf J RingCat
M : SheafOfModules R
I : Type u
X : I → C
hX : J.CoversTop X
D : (i : I) → (M.over (X i)).QuasicoherentData
i : (i : I) × (D i).I
x✝ : (Over ((D i.fst).X i.snd))ᵒᵖ
⊢ ((𝟙 ((R.over (X i.fst)).over ((D i.fst).X i.snd))).hom ≫
          ((D i.fst).X i.snd).iteratedSliceEquiv.functor.op.whiskerLeft (𝟙 (R.over ((D i.fst).X i.snd).left)).hom ≫
            Functor.whiskerRight (NatTrans.op ((D i.fst).X i.snd).iteratedSliceEquiv.unit)
              ((R.over (X i.fst)).over ((D i.fst).X i.snd)).obj).app
      x✝ =
    (𝟙 ((R.over (X i.fst)).over ((D i.fst).X i.snd)).obj).app x✝

Tactic:
;

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
R✝ : Sheaf J RingCat
inst✝³ : ∀ (X : C), HasSheafify (J.over X) AddCommGrpCat
inst✝² : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat
inst✝¹ : ∀ (X : C) (Y : Over X), HasSheafify ((J.over X).over Y) AddCommGrpCat
inst✝ : ∀ (X : C) (Y : Over X), ((J.over X).over Y).WEqualsLocallyBijective AddCommGrpCat
R : Sheaf J RingCat
M : SheafOfModules R
I : Type u
X : I → C
hX : J.CoversTop X
D : (i : I) → (M.over (X i)).QuasicoherentData
i : (i : I) × (D i).I
x✝ : (Over ((D i.fst).X i.snd))ᵒᵖ
⊢ ((𝟙 ((R.over (X i.fst)).over ((D i.fst).X i.snd))).hom ≫
          ((D i.fst).X i.snd).iteratedSliceEquiv.functor.op.whiskerLeft (𝟙 (R.over ((D i.fst).X i.snd).left)).hom ≫
            Functor.whiskerRight (NatTrans.op ((D i.fst).X i.snd).iteratedSliceEquiv.unit)
              ((R.over (X i.fst)).over ((D i.fst).X i.snd)).obj).app
      x✝ =
    (𝟙 ((R.over (X i.fst)).over ((D i.fst).X i.snd)).obj).app x✝
Module: Mathlib.Topology.Sheaves.Stalks

Goal state before:
pp: case op
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X : TopCat
F : Presheaf C X
x : ↑X
Y : C
f₁ f₂ : F.stalk x ⟶ Y
ih : ∀ (U : Opens ↑X) (hxU : x ∈ U), F.germ U x hxU ≫ f₁ = F.germ U x hxU ≫ f₂
U : Opens ↑X
hxU : x ∈ U
⊢ colimit.ι (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj F) (op ⟨U, hxU⟩) ≫ f₁ =
    colimit.ι (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj F) (op ⟨U, hxU⟩) ≫ f₂

Tactic:
;

Goal state after:
case op
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X : TopCat
F : Presheaf C X
x : ↑X
Y : C
f₁ f₂ : F.stalk x ⟶ Y
ih : ∀ (U : Opens ↑X) (hxU : x ∈ U), F.germ U x hxU ≫ f₁ = F.germ U x hxU ≫ f₂
U : Opens ↑X
hxU : x ∈ U
⊢ colimit.ι (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj F) (op ⟨U, hxU⟩) ≫ f₁ =
    colimit.ι (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj F) (op ⟨U, hxU⟩) ≫ f₂
Module: Mathlib.Data.FunLike.Ring

Goal state before:
pp: F : Type u_1
α : Type u_2
inst✝⁸ : FunLike F α α
inst✝⁷ : Zero F
inst✝⁶ : One F
inst✝⁵ : Mul F
inst✝⁴ : Zero α
inst✝³ : IsZeroApply F α α
inst✝² : IsOneApplyEqSelf F α
inst✝¹ : IsMulApplyEqComp F α
inst✝ : ZeroHomClass F α α
x✝² x✝¹ x✝ : F
⊢ ∀ (x : α), (x✝² * x✝¹ * x✝) x = (x✝² * (x✝¹ * x✝)) x

Tactic:
;

Goal state after:
F : Type u_1
α : Type u_2
inst✝⁸ : FunLike F α α
inst✝⁷ : Zero F
inst✝⁶ : One F
inst✝⁵ : Mul F
inst✝⁴ : Zero α
inst✝³ : IsZeroApply F α α
inst✝² : IsOneApplyEqSelf F α
inst✝¹ : IsMulApplyEqComp F α
inst✝ : ZeroHomClass F α α
x✝² x✝¹ x✝ : F
⊢ ∀ (x : α), (x✝² * x✝¹ * x✝) x = (x✝² * (x✝¹ * x✝)) x
Module: Mathlib.Data.FunLike.Ring

Goal state before:
pp: F : Type u_1
α : Type u_2
inst✝⁸ : FunLike F α α
inst✝⁷ : Zero F
inst✝⁶ : One F
inst✝⁵ : Mul F
inst✝⁴ : Zero α
inst✝³ : IsZeroApply F α α
inst✝² : IsOneApplyEqSelf F α
inst✝¹ : IsMulApplyEqComp F α
inst✝ : ZeroHomClass F α α
x✝ : F
⊢ ∀ (x : α), (1 * x✝) x = x✝ x

Tactic:
;

Goal state after:
F : Type u_1
α : Type u_2
inst✝⁸ : FunLike F α α
inst✝⁷ : Zero F
inst✝⁶ : One F
inst✝⁵ : Mul F
inst✝⁴ : Zero α
inst✝³ : IsZeroApply F α α
inst✝² : IsOneApplyEqSelf F α
inst✝¹ : IsMulApplyEqComp F α
inst✝ : ZeroHomClass F α α
x✝ : F
⊢ ∀ (x : α), (1 * x✝) x = x✝ x
Module: Mathlib.Data.FunLike.Ring

Goal state before:
pp: F : Type u_1
α : Type u_2
inst✝⁸ : FunLike F α α
inst✝⁷ : Zero F
inst✝⁶ : One F
inst✝⁵ : Mul F
inst✝⁴ : Zero α
inst✝³ : IsZeroApply F α α
inst✝² : IsOneApplyEqSelf F α
inst✝¹ : IsMulApplyEqComp F α
inst✝ : ZeroHomClass F α α
x✝ : F
⊢ ∀ (x : α), (x✝ * 1) x = x✝ x

Tactic:
;

Goal state after:
F : Type u_1
α : Type u_2
inst✝⁸ : FunLike F α α
inst✝⁷ : Zero F
inst✝⁶ : One F
inst✝⁵ : Mul F
inst✝⁴ : Zero α
inst✝³ : IsZeroApply F α α
inst✝² : IsOneApplyEqSelf F α
inst✝¹ : IsMulApplyEqComp F α
inst✝ : ZeroHomClass F α α
x✝ : F
⊢ ∀ (x : α), (x✝ * 1) x = x✝ x
Module: Mathlib.Data.FunLike.Ring

Goal state before:
pp: F : Type u_1
α : Type u_2
inst✝⁸ : FunLike F α α
inst✝⁷ : Zero F
inst✝⁶ : One F
inst✝⁵ : Mul F
inst✝⁴ : Zero α
inst✝³ : IsZeroApply F α α
inst✝² : IsOneApplyEqSelf F α
inst✝¹ : IsMulApplyEqComp F α
inst✝ : ZeroHomClass F α α
x✝ : F
⊢ ∀ (x : α), (0 * x✝) x = 0 x

Tactic:
;

Goal state after:
F : Type u_1
α : Type u_2
inst✝⁸ : FunLike F α α
inst✝⁷ : Zero F
inst✝⁶ : One F
inst✝⁵ : Mul F
inst✝⁴ : Zero α
inst✝³ : IsZeroApply F α α
inst✝² : IsOneApplyEqSelf F α
inst✝¹ : IsMulApplyEqComp F α
inst✝ : ZeroHomClass F α α
x✝ : F
⊢ ∀ (x : α), (0 * x✝) x = 0 x
Module: Mathlib.Data.FunLike.Ring

Goal state before:
pp: F : Type u_1
α : Type u_2
inst✝⁸ : FunLike F α α
inst✝⁷ : Zero F
inst✝⁶ : One F
inst✝⁵ : Mul F
inst✝⁴ : Zero α
inst✝³ : IsZeroApply F α α
inst✝² : IsOneApplyEqSelf F α
inst✝¹ : IsMulApplyEqComp F α
inst✝ : ZeroHomClass F α α
f : F
⊢ ∀ (x : α), (f * 0) x = 0 x

Tactic:
;

Goal state after:
F : Type u_1
α : Type u_2
inst✝⁸ : FunLike F α α
inst✝⁷ : Zero F
inst✝⁶ : One F
inst✝⁵ : Mul F
inst✝⁴ : Zero α
inst✝³ : IsZeroApply F α α
inst✝² : IsOneApplyEqSelf F α
inst✝¹ : IsMulApplyEqComp F α
inst✝ : ZeroHomClass F α α
f : F
⊢ ∀ (x : α), (f * 0) x = 0 x
Module: Mathlib.Data.FunLike.Ring

Goal state before:
pp: F : Type u_1
α : Type u_2
inst✝¹⁴ : FunLike F α α
inst✝¹³ : Zero F
inst✝¹² : One F
inst✝¹¹ : Mul F
inst✝¹⁰ : Add F
inst✝⁹ : AddCommMonoid α
inst✝⁸ : IsZeroApply F α α
inst✝⁷ : IsAddApply F α α
inst✝⁶ : IsOneApplyEqSelf F α
inst✝⁵ : IsMulApplyEqComp F α
inst✝⁴ : SMul ℕ F
inst✝³ : IsSMulApply ℕ F α α
inst✝² : AddMonoidHomClass F α α
inst✝¹ : NatCast F
inst✝ : IsNatCastApply F α
f g h : F
⊢ ∀ (x : α), (f * (g + h)) x = (f * g + f * h) x

Tactic:
;

Goal state after:
F : Type u_1
α : Type u_2
inst✝¹⁴ : FunLike F α α
inst✝¹³ : Zero F
inst✝¹² : One F
inst✝¹¹ : Mul F
inst✝¹⁰ : Add F
inst✝⁹ : AddCommMonoid α
inst✝⁸ : IsZeroApply F α α
inst✝⁷ : IsAddApply F α α
inst✝⁶ : IsOneApplyEqSelf F α
inst✝⁵ : IsMulApplyEqComp F α
inst✝⁴ : SMul ℕ F
inst✝³ : IsSMulApply ℕ F α α
inst✝² : AddMonoidHomClass F α α
inst✝¹ : NatCast F
inst✝ : IsNatCastApply F α
f g h : F
⊢ ∀ (x : α), (f * (g + h)) x = (f * g + f * h) x
Module: Mathlib.Data.FunLike.Ring

Goal state before:
pp: F : Type u_1
α : Type u_2
inst✝¹⁴ : FunLike F α α
inst✝¹³ : Zero F
inst✝¹² : One F
inst✝¹¹ : Mul F
inst✝¹⁰ : Add F
inst✝⁹ : AddCommMonoid α
inst✝⁸ : IsZeroApply F α α
inst✝⁷ : IsAddApply F α α
inst✝⁶ : IsOneApplyEqSelf F α
inst✝⁵ : IsMulApplyEqComp F α
inst✝⁴ : SMul ℕ F
inst✝³ : IsSMulApply ℕ F α α
inst✝² : AddMonoidHomClass F α α
inst✝¹ : NatCast F
inst✝ : IsNatCastApply F α
x✝² x✝¹ x✝ : F
⊢ ∀ (x : α), ((x✝² + x✝¹) * x✝) x = (x✝² * x✝ + x✝¹ * x✝) x

Tactic:
;

Goal state after:
F : Type u_1
α : Type u_2
inst✝¹⁴ : FunLike F α α
inst✝¹³ : Zero F
inst✝¹² : One F
inst✝¹¹ : Mul F
inst✝¹⁰ : Add F
inst✝⁹ : AddCommMonoid α
inst✝⁸ : IsZeroApply F α α
inst✝⁷ : IsAddApply F α α
inst✝⁶ : IsOneApplyEqSelf F α
inst✝⁵ : IsMulApplyEqComp F α
inst✝⁴ : SMul ℕ F
inst✝³ : IsSMulApply ℕ F α α
inst✝² : AddMonoidHomClass F α α
inst✝¹ : NatCast F
inst✝ : IsNatCastApply F α
x✝² x✝¹ x✝ : F
⊢ ∀ (x : α), ((x✝² + x✝¹) * x✝) x = (x✝² * x✝ + x✝¹ * x✝) x
Module: Mathlib.Data.FunLike.Ring

Goal state before:
pp: F : Type u_1
α : Type u_2
inst✝¹⁴ : FunLike F α α
inst✝¹³ : Zero F
inst✝¹² : One F
inst✝¹¹ : Mul F
inst✝¹⁰ : Add F
inst✝⁹ : AddCommMonoid α
inst✝⁸ : IsZeroApply F α α
inst✝⁷ : IsAddApply F α α
inst✝⁶ : IsOneApplyEqSelf F α
inst✝⁵ : IsMulApplyEqComp F α
inst✝⁴ : SMul ℕ F
inst✝³ : IsSMulApply ℕ F α α
inst✝² : AddMonoidHomClass F α α
inst✝¹ : NatCast F
inst✝ : IsNatCastApply F α
⊢ ∀ (x : α), ↑0 x = 0 x

Tactic:
;

Goal state after:
F : Type u_1
α : Type u_2
inst✝¹⁴ : FunLike F α α
inst✝¹³ : Zero F
inst✝¹² : One F
inst✝¹¹ : Mul F
inst✝¹⁰ : Add F
inst✝⁹ : AddCommMonoid α
inst✝⁸ : IsZeroApply F α α
inst✝⁷ : IsAddApply F α α
inst✝⁶ : IsOneApplyEqSelf F α
inst✝⁵ : IsMulApplyEqComp F α
inst✝⁴ : SMul ℕ F
inst✝³ : IsSMulApply ℕ F α α
inst✝² : AddMonoidHomClass F α α
inst✝¹ : NatCast F
inst✝ : IsNatCastApply F α
⊢ ∀ (x : α), ↑0 x = 0 x
Module: Mathlib.Data.FunLike.Ring

Goal state before:
pp: F : Type u_1
α : Type u_2
inst✝¹⁴ : FunLike F α α
inst✝¹³ : Zero F
inst✝¹² : One F
inst✝¹¹ : Mul F
inst✝¹⁰ : Add F
inst✝⁹ : AddCommMonoid α
inst✝⁸ : IsZeroApply F α α
inst✝⁷ : IsAddApply F α α
inst✝⁶ : IsOneApplyEqSelf F α
inst✝⁵ : IsMulApplyEqComp F α
inst✝⁴ : SMul ℕ F
inst✝³ : IsSMulApply ℕ F α α
inst✝² : AddMonoidHomClass F α α
inst✝¹ : NatCast F
inst✝ : IsNatCastApply F α
n : ℕ
⊢ ∀ (x : α), ↑(n + 1) x = (↑n + 1) x

Tactic:
;

Goal state after:
F : Type u_1
α : Type u_2
inst✝¹⁴ : FunLike F α α
inst✝¹³ : Zero F
inst✝¹² : One F
inst✝¹¹ : Mul F
inst✝¹⁰ : Add F
inst✝⁹ : AddCommMonoid α
inst✝⁸ : IsZeroApply F α α
inst✝⁷ : IsAddApply F α α
inst✝⁶ : IsOneApplyEqSelf F α
inst✝⁵ : IsMulApplyEqComp F α
inst✝⁴ : SMul ℕ F
inst✝³ : IsSMulApply ℕ F α α
inst✝² : AddMonoidHomClass F α α
inst✝¹ : NatCast F
inst✝ : IsNatCastApply F α
n : ℕ
⊢ ∀ (x : α), ↑(n + 1) x = (↑n + 1) x
Module: Mathlib.Data.FunLike.Ring

Goal state before:
pp: F : Type u_1
α : Type u_2
inst✝²² : FunLike F α α
inst✝²¹ : Zero F
inst✝²⁰ : One F
inst✝¹⁹ : Mul F
inst✝¹⁸ : Add F
inst✝¹⁷ : Neg F
inst✝¹⁶ : Sub F
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : IsZeroApply F α α
inst✝¹³ : IsAddApply F α α
inst✝¹² : IsOneApplyEqSelf F α
inst✝¹¹ : IsMulApplyEqComp F α
inst✝¹⁰ : IsNegApply F α α
inst✝⁹ : IsSubApply F α α
inst✝⁸ : SMul ℕ F
inst✝⁷ : IsSMulApply ℕ F α α
inst✝⁶ : SMul ℤ F
inst✝⁵ : IsSMulApply ℤ F α α
inst✝⁴ : AddMonoidHomClass F α α
inst✝³ : NatCast F
inst✝² : IsNatCastApply F α
inst✝¹ : IntCast F
inst✝ : IsIntCastApply F α
x✝ : ℕ
⊢ ∀ (x : α), (IntCast.intCast ↑x✝) x = ↑x✝ x

Tactic:
;

Goal state after:
F : Type u_1
α : Type u_2
inst✝²² : FunLike F α α
inst✝²¹ : Zero F
inst✝²⁰ : One F
inst✝¹⁹ : Mul F
inst✝¹⁸ : Add F
inst✝¹⁷ : Neg F
inst✝¹⁶ : Sub F
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : IsZeroApply F α α
inst✝¹³ : IsAddApply F α α
inst✝¹² : IsOneApplyEqSelf F α
inst✝¹¹ : IsMulApplyEqComp F α
inst✝¹⁰ : IsNegApply F α α
inst✝⁹ : IsSubApply F α α
inst✝⁸ : SMul ℕ F
inst✝⁷ : IsSMulApply ℕ F α α
inst✝⁶ : SMul ℤ F
inst✝⁵ : IsSMulApply ℤ F α α
inst✝⁴ : AddMonoidHomClass F α α
inst✝³ : NatCast F
inst✝² : IsNatCastApply F α
inst✝¹ : IntCast F
inst✝ : IsIntCastApply F α
x✝ : ℕ
⊢ ∀ (x : α), (IntCast.intCast ↑x✝) x = ↑x✝ x
Module: Mathlib.Data.FunLike.Ring

Goal state before:
pp: F : Type u_1
α : Type u_2
inst✝²² : FunLike F α α
inst✝²¹ : Zero F
inst✝²⁰ : One F
inst✝¹⁹ : Mul F
inst✝¹⁸ : Add F
inst✝¹⁷ : Neg F
inst✝¹⁶ : Sub F
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : IsZeroApply F α α
inst✝¹³ : IsAddApply F α α
inst✝¹² : IsOneApplyEqSelf F α
inst✝¹¹ : IsMulApplyEqComp F α
inst✝¹⁰ : IsNegApply F α α
inst✝⁹ : IsSubApply F α α
inst✝⁸ : SMul ℕ F
inst✝⁷ : IsSMulApply ℕ F α α
inst✝⁶ : SMul ℤ F
inst✝⁵ : IsSMulApply ℤ F α α
inst✝⁴ : AddMonoidHomClass F α α
inst✝³ : NatCast F
inst✝² : IsNatCastApply F α
inst✝¹ : IntCast F
inst✝ : IsIntCastApply F α
n : ℕ
⊢ ∀ (x : α), (IntCast.intCast (Int.negSucc n)) x = (-↑(n + 1)) x

Tactic:
;

Goal state after:
F : Type u_1
α : Type u_2
inst✝²² : FunLike F α α
inst✝²¹ : Zero F
inst✝²⁰ : One F
inst✝¹⁹ : Mul F
inst✝¹⁸ : Add F
inst✝¹⁷ : Neg F
inst✝¹⁶ : Sub F
inst✝¹⁵ : AddCommGroup α
inst✝¹⁴ : IsZeroApply F α α
inst✝¹³ : IsAddApply F α α
inst✝¹² : IsOneApplyEqSelf F α
inst✝¹¹ : IsMulApplyEqComp F α
inst✝¹⁰ : IsNegApply F α α
inst✝⁹ : IsSubApply F α α
inst✝⁸ : SMul ℕ F
inst✝⁷ : IsSMulApply ℕ F α α
inst✝⁶ : SMul ℤ F
inst✝⁵ : IsSMulApply ℤ F α α
inst✝⁴ : AddMonoidHomClass F α α
inst✝³ : NatCast F
inst✝² : IsNatCastApply F α
inst✝¹ : IntCast F
inst✝ : IsIntCastApply F α
n : ℕ
⊢ ∀ (x : α), (IntCast.intCast (Int.negSucc n)) x = (-↑(n + 1)) x
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:
;

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
inst✝ : ∀ (x : ↑X), IsIso ((stalkFunctor C x).map f.hom)
U : (Opens ↑X)ᵒᵖ
⊢ IsIso (f.hom.app U)
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:
;

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

Tactic:
;

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

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

Tactic:
;

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)
α : Type u_6
f : α → ι
m✝ : R
x✝¹ : (i : ι) → φ i
x✝ : α
⊢ (m✝ • x✝¹) (f x✝) = ((RingHom.id R) m✝ • fun i ↦ x✝¹ (f i)) x✝
Module: Mathlib.Topology.Algebra.Module.ModuleTopology

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
τR : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
x✝ : R
⊢ id x✝ = ((fun rs ↦ rs.1 • rs.2) ∘ fun r ↦ (r, 1)) x✝

Tactic:
;

Goal state after:
R : Type u_1
inst✝¹ : Semiring R
τR : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
x✝ : R
⊢ id x✝ = ((fun rs ↦ rs.1 • rs.2) ∘ fun r ↦ (r, 1)) x✝
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
⊢ φ ((algebraMap R A) r) * φ m = r • φ m

Tactic:
;

Goal state after:
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
⊢ φ ((algebraMap R A) r) * φ m = r • φ m
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
x✝ : R × A
⊢ ((fun p ↦ p.1 • p.2) ∘ Prod.map ⇑σ ⇑φ) x✝ = (⇑φ ∘ fun p ↦ p.1 • p.2) x✝

Tactic:
;

Goal state after:
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
x✝ : R × A
⊢ ((fun p ↦ p.1 • p.2) ∘ Prod.map ⇑σ ⇑φ) x✝ = (⇑φ ∘ fun p ↦ p.1 • p.2) x✝
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
x✝ : A × A
⊢ ((fun p ↦ p.1 + p.2) ∘ Prod.map ⇑φ ⇑φ) x✝ = (⇑φ ∘ fun p ↦ p.1 + p.2) x✝

Tactic:
;

Goal state after:
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
x✝ : A × A
⊢ ((fun p ↦ p.1 + p.2) ∘ Prod.map ⇑φ ⇑φ) x✝ = (⇑φ ∘ fun p ↦ p.1 + p.2) x✝
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 ↑(R.obj (op ((OpenNhds.inclusion x).obj (unop i)))) ↑(M.obj (op ((OpenNhds.inclusion x).obj (unop i))))

Tactic:
;

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 ↑(R.obj (op ((OpenNhds.inclusion x).obj (unop i)))) ↑(M.obj (op ((OpenNhds.inclusion x).obj (unop i))))

Tactic:
;

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 ↑(R.obj (op ((OpenNhds.inclusion x).obj (unop i)))) ↑(M.obj (op ((OpenNhds.inclusion x).obj (unop i))))

Tactic:
;

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))))