mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : TopCat
ι : Type u_2
U : ι → Opens ↑X
V : OpensLeCover U
i j : ι
a : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (Pairwise.pair i j)
i' j' : ι
b : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (Pairwise.pair i' j')
⊢ ((pairwiseToOpensLeCover U).obj (Pairwise.pair i j)).obj ≤ U i

Tactic:
simp

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
ι : Type u_2
U : ι → Opens ↑X
V : OpensLeCover U
i j : ι
a : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (Pairwise.pair i j)
i' j' : ι
b : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (Pairwise.pair i' j')
⊢ ((pairwiseToOpensLeCover U).obj (Pairwise.pair i' j')).obj ≤ U i'

Tactic:
simp

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
ι : Type u_2
U : ι → Opens ↑X
V : OpensLeCover U
i j : ι
a : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (Pairwise.pair i j)
i' j' : ι
b : (Functor.fromPUnit V).obj { as := PUnit.unit } ⟶ (pairwiseToOpensLeCover U).obj (Pairwise.pair i' j')
⊢ ((pairwiseToOpensLeCover U).obj (Pairwise.pair i' j')).obj ≤ ((pairwiseToOpensLeCover U).obj (single i')).obj

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Sheaves.Stalks

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X : TopCat
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 : (OpenNhds x)ᵒᵖ
⊢ colimit.ι (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj F) U ≫ f₁ =
    colimit.ι (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj F) U ≫ f₂

Tactic:
induction U with | op U => obtain ⟨U, hxU⟩ := U; exact ih U hxU

Goal state after:
Module: Mathlib.Topology.Sheaves.Stalks

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y Z : TopCat
FC : C → C → Type u_1
CC : C → Type u_2
inst✝ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
f : X ⟶ Y
F : Presheaf C Y
U : Opens ↑X
x : ↑X
hx : x ∈ U
x✝¹ x✝ : CostructuredArrow (Opens.map f).op (op U)
i : x✝¹ ⟶ x✝
⊢ (CostructuredArrow.proj (Opens.map f).op (op U) ⋙ F).map i ≫ F.germ (unop x✝.1) ((ConcreteCategory.hom f) x) ⋯ =
    F.germ (unop x✝¹.1) ((ConcreteCategory.hom f) x) ⋯ ≫
      ((Functor.const (CostructuredArrow (Opens.map f).op (op U))).obj (F.stalk ((ConcreteCategory.hom f) x))).map i

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Sheaves.Stalks

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X : TopCat
F : Presheaf C X
x : ↑X
U✝ : Opens ↑X
hxU✝ : x ∈ U✝
⊢ F.germ U✝ x hxU✝ ≫ F.stalkSpecializes ⋯ = F.germ U✝ x hxU✝ ≫ 𝟙 (F.stalk x)

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Sheaves.Stalks

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X : TopCat
F : Presheaf C X
x y z : ↑X
h : x ⤳ y
h' : y ⤳ z
U✝ : Opens ↑X
hxU✝ : z ∈ U✝
⊢ F.germ U✝ z hxU✝ ≫ F.stalkSpecializes h' ≫ F.stalkSpecializes h = F.germ U✝ z hxU✝ ≫ F.stalkSpecializes ⋯

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Sheaves.Stalks

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X : TopCat
F G : Presheaf C X
f : F ⟶ G
x y : ↑X
h : x ⤳ y
U✝ : Opens ↑X
hxU✝ : y ∈ U✝
⊢ F.germ U✝ y hxU✝ ≫ F.stalkSpecializes h ≫ (stalkFunctor C x).map f =
    F.germ U✝ y hxU✝ ≫ (stalkFunctor C y).map f ≫ G.stalkSpecializes h

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Sheaves.Stalks

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X Y : TopCat
f : X ⟶ Y
F : Presheaf C X
x y : ↑X
h : x ⤳ y
U✝ : Opens ↑Y
hxU✝ : (Hom.hom f) y ∈ U✝
⊢ ((pushforward C f).obj F).germ U✝ ((Hom.hom f) y) hxU✝ ≫
      ((pushforward C f).obj F).stalkSpecializes ⋯ ≫ stalkPushforward C f F x =
    ((pushforward C f).obj F).germ U✝ ((Hom.hom f) y) hxU✝ ≫ stalkPushforward C f F y ≫ F.stalkSpecializes h

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Sheaves.Stalks

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y Z : TopCat
FC : C → C → Type u_1
CC : C → Type u_2
inst✝ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
F : Presheaf C X
x y : ↑X
e : Inseparable x y
⊢ F.stalkSpecializes ⋯ ≫ F.stalkSpecializes ⋯ = 𝟙 (F.stalk x)

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Sheaves.Stalks

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimits C
X Y Z : TopCat
FC : C → C → Type u_1
CC : C → Type u_2
inst✝ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
F : Presheaf C X
x y : ↑X
e : Inseparable x y
⊢ F.stalkSpecializes ⋯ ≫ F.stalkSpecializes ⋯ = 𝟙 (F.stalk y)

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
x✝ : R
⊢ (fun φ ↦ (ConcreteCategory.hom (φ.hom.app (ModuleCat.of R R))) 1)
      ((fun r ↦
          ObjectProperty.homMk
            { app := fun M ↦ AddCommGrpCat.ofHom (DistribSMul.toAddMonoidHom (↑M) r), naturality := ⋯ })
        x✝) =
    x✝

Tactic:
simp

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : ContinuousConstSMul R M
inst✝ : ContinuousAdd M
s : Submodule R M
⊢ closure[inst✝⁴] ↑s = Set.univ ↔ ↑s.topologicalClosure = ↑⊤

Tactic:
simp

Goal state after:
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:
simp only [Set.subset_def, mem_closure_iff]
    intro x hx U hU hxU
    rcases isOpen_pi_iff.mp hU x hxU with ⟨t, V, hV, hVU⟩
    refine ⟨∑ i ∈ t, Pi.single i (x i), hVU ?_, ?_⟩
    · simp_all [Finset.sum_pi_single]
    · exact sum_mem fun i hi ↦ mem_iSup_of_mem i <| mem_map_of_mem <| hx _ <| Set.mem_univ _

Goal state after:
Module: Mathlib.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:
simp

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

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

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

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

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

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

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

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

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)
U₁ : C
a₁ : (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj U₁
U₂ : C
a₂ : (((R ⋙ forget₂ RingCat SemiRingCat) ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj U₂
V : C
b : (((M ⋙ forget₂ AddCommGrpCat AddGrpCat) ⋙ forget₂ AddGrpCat AddMonCat) ⋙ forget AddMonCat).obj V
s : C
α : IsFiltered.max (IsFiltered.max U₁ U₂) V ⟶ s
β : IsFiltered.max U₁ (IsFiltered.max U₂ V) ⟶ s
h₁ : (leftToMax U₁ U₂ ≫ leftToMax (IsFiltered.max U₁ U₂) V) ≫ α = leftToMax U₁ (IsFiltered.max U₂ V) ≫ β
h₂ :
  (rightToMax U₁ U₂ ≫ leftToMax (IsFiltered.max U₁ U₂) V) ≫ α =
    (leftToMax U₂ V ≫ rightToMax U₁ (IsFiltered.max U₂ V)) ≫ β
h₃ : rightToMax (IsFiltered.max U₁ U₂) V ≫ α = (rightToMax U₂ V ≫ rightToMax U₁ (IsFiltered.max U₂ V)) ≫ β
⊢ (ConcreteCategory.hom (M.map α))
      ((ConcreteCategory.hom (R.map (leftToMax (IsFiltered.max U₁ U₂) V)))
          ((ConcreteCategory.hom (R.map (leftToMax U₁ U₂))) a₁ * (ConcreteCategory.hom (R.map (rightToMax U₁ U₂))) a₂) •
        (ConcreteCategory.hom (M.map (rightToMax (IsFiltered.max U₁ U₂) V))) b) =
    (ConcreteCategory.hom (M.map β))
      ((ConcreteCategory.hom (R.map (leftToMax U₁ (IsFiltered.max U₂ V)))) a₁ •
        (ConcreteCategory.hom (M.map (rightToMax U₁ (IsFiltered.max U₂ V))))
          ((ConcreteCategory.hom (R.map (leftToMax U₂ V))) a₂ • (ConcreteCategory.hom (M.map (rightToMax U₂ V))) b))

Tactic:
simp only [map_mul, ← ConcreteCategory.comp_apply, ← Functor.map_comp, mul_smul, *]

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

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

Tactic:
simp

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

Tactic:
simp

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

Goal state before:
pp: case hl
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
x✝ : M₁
⊢ ((f₁ + g₁).coprod (f₂ + g₂) ∘SL inl R M₁ M₂) x✝ = ((f₁.coprod f₂ + g₁.coprod g₂) ∘SL inl R M₁ M₂) x✝

Tactic:
simp

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

Goal state before:
pp: case hr
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
x✝ : M₂
⊢ ((f₁ + g₁).coprod (f₂ + g₂) ∘SL inr R M₁ M₂) x✝ = ((f₁.coprod f₂ + g₁.coprod g₂) ∘SL inr R M₁ M₂) x✝

Tactic:
simp

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

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

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

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

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

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

Tactic:
simp

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
x✝ : R
⊢ id x✝ = ((fun rs ↦ rs.1 • rs.2) ∘ fun r ↦ (r, 1)) x✝

Tactic:
simp

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

Tactic:
simp

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

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : TopologicalSpace R
inst✝⁹ : CommSemiring R
B : Type u_2
inst✝⁸ : AddCommMonoid B
inst✝⁷ : Module R B
inst✝⁶ : TopologicalSpace B
inst✝⁵ : IsModuleTopology R B
C : Type u_3
inst✝⁴ : AddCommMonoid C
inst✝³ : Module R C
inst✝² : TopologicalSpace C
inst✝¹ : IsModuleTopology R C
ι : Type u_4
inst✝ : Finite ι
bil : (ι → R) →ₗ[R] B →ₗ[R] C
val✝ : Fintype ι
f : ι → R
b : B
x : ι
x✝ : x ∈ Finset.univ
⊢ (bil (f x • ⇑(Finsupp.single x 1))) b = f x • (bil ⇑(Finsupp.single x 1)) b

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝¹² : TopologicalSpace R
inst✝¹¹ : CommRing R
inst✝¹⁰ : IsTopologicalRing R
A : Type u_2
inst✝⁹ : AddCommGroup A
inst✝⁸ : Module R A
aA : TopologicalSpace A
inst✝⁷ : IsModuleTopology R A
B : Type u_3
inst✝⁶ : AddCommGroup B
inst✝⁵ : Module R B
aB : TopologicalSpace B
inst✝⁴ : IsModuleTopology R B
C : Type u_4
inst✝³ : AddCommGroup C
inst✝² : Module R C
aC : TopologicalSpace C
inst✝¹ : IsModuleTopology R C
inst✝ : Module.Finite R B
bil : A →ₗ[R] B →ₗ[R] C
x✝ : A × B
⊢ (bil x✝.1) x✝.2 = ((fun ba ↦ (bil.flip ba.1) ba.2) ∘ Prod.swap) x✝

Tactic:
simp

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

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst✝⁵ : TopologicalSpace M₁
inst✝⁴ : AddCommMonoid M₁
M₂ : Type u_6
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₁ M₁
inst✝ : Module R₂ M₂
f : M₁ →SL[σ₁₂] M₂
⊢ Set.range ⇑↑f = Set.range ⇑f

Tactic:
simp

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

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝¹² : Semiring R₁
inst✝¹¹ : Semiring R₂
inst✝¹⁰ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst✝⁹ : TopologicalSpace M₁
inst✝⁸ : AddCommMonoid M₁
M₂ : Type u_6
inst✝⁷ : TopologicalSpace M₂
inst✝⁶ : AddCommMonoid M₂
M₃ : Type u_7
inst✝⁵ : TopologicalSpace M₃
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R₁ M₁
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
g : M₂ →SL[σ₂₃] M₃
x✝ : M₁
⊢ (g ∘SL 0) x✝ = 0 x✝

Tactic:
simp

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

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝¹² : Semiring R₁
inst✝¹¹ : Semiring R₂
inst✝¹⁰ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst✝⁹ : TopologicalSpace M₁
inst✝⁸ : AddCommMonoid M₁
M₂ : Type u_6
inst✝⁷ : TopologicalSpace M₂
inst✝⁶ : AddCommMonoid M₂
M₃ : Type u_7
inst✝⁵ : TopologicalSpace M₃
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R₁ M₁
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M₁ →SL[σ₁₂] M₂
x✝ : M₁
⊢ (0 ∘SL f) x✝ = 0 x✝

Tactic:
simp

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

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝¹⁴ : Semiring R₁
inst✝¹³ : Semiring R₂
inst✝¹² : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
M₁ : Type u_4
inst✝¹¹ : TopologicalSpace M₁
inst✝¹⁰ : AddCommMonoid M₁
M₂ : Type u_6
inst✝⁹ : TopologicalSpace M₂
inst✝⁸ : AddCommMonoid M₂
M₃ : Type u_7
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : Module R₁ M₁
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : ContinuousAdd M₂
inst✝ : ContinuousAdd M₃
g : M₂ →SL[σ₂₃] M₃
f₁ f₂ : M₁ →SL[σ₁₂] M₂
x✝ : M₁
⊢ (g ∘SL (f₁ + f₂)) x✝ = (g ∘SL f₁ + g ∘SL f₂) x✝

Tactic:
simp

Goal state after: