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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁷ : Finite ι
inst✝⁶ : Semiring R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : TopologicalSpace M
inst✝¹ : ContinuousAdd M
inst✝ : ContinuousSMul R M
f : (ι → R) →ₗ[R] M
val✝ : Fintype ι
⊢ ⇑f = fun x ↦ ∑ i, x i • f fun j ↦ if i = j then 1 else 0

Tactic:
ext x

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁷ : Finite ι
inst✝⁶ : Semiring R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : TopologicalSpace M
inst✝¹ : ContinuousAdd M
inst✝ : ContinuousSMul R M
f : (ι → R) →ₗ[R] M
val✝ : Fintype ι
x : ι → R
⊢ f x = ∑ i, x i • f fun j ↦ if i = j then 1 else 0
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
  let ι : ULift.{w} WalkingPair → Opens X := fun ⟨j⟩ => WalkingPair.casesOn j U V
  have hι : U ⊔ V = iSup ι := by
    ext
    rw [Opens.coe_iSup, Set.mem_iUnion]
    constructor
    · rintro (h | h)
      exacts [⟨⟨WalkingPair.left⟩, h⟩, ⟨⟨WalkingPair.right⟩, h⟩]
    · rintro ⟨⟨_ | _⟩, h⟩
      exacts [Or.inl h, Or.inr h]
  apply PullbackCone.isLimitAux'
  intro s
  use interUnionPullbackConeLift F U V s
  refine ⟨?_, ?_, ?_⟩
  · apply interUnionPullbackConeLift_left
  · apply interUnionPullbackConeLift_right
  · 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.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₃
f₁ f₂ : M₁ →SL[σ₁₂] M₂
hg : Function.Injective ⇑g
h : g ∘SL f₁ = g ∘SL f₂
⊢ f₁ = f₂

Tactic:
ext x

Goal state after:
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₃
f₁ f₂ : M₁ →SL[σ₁₂] M₂
hg : Function.Injective ⇑g
h : g ∘SL f₁ = g ∘SL f₂
x : M₁
⊢ f₁ x = f₂ x
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

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

Tactic:
ext x

Goal state after:
R : Type u_1
inst✝¹⁴ : Ring R
R₂ : Type u_2
inst✝¹³ : Ring R₂
R₃ : Type u_3
inst✝¹² : Ring R₃
M : Type u_4
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : AddCommGroup M
M₂ : Type u_5
inst✝⁹ : TopologicalSpace M₂
inst✝⁸ : AddCommGroup M₂
M₃ : Type u_6
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : Module R M
inst✝⁴ : Module R₂ M₂
inst✝³ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : IsTopologicalAddGroup M₂
inst✝ : IsTopologicalAddGroup M₃
g : M₂ →SL[σ₂₃] M₃
f : M →SL[σ₁₂] M₂
x : M
⊢ (g ∘SL (-f)) x = (-g ∘SL f) x
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: R : Type u_1
S : Type u_4
inst✝¹⁷ : Semiring R
inst✝¹⁶ : Monoid S
M : Type u_6
inst✝¹⁵ : TopologicalSpace M
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R M
N₂ : Type u_9
inst✝¹² : TopologicalSpace N₂
inst✝¹¹ : AddCommMonoid N₂
inst✝¹⁰ : Module R N₂
N₃ : Type u_10
inst✝⁹ : TopologicalSpace N₃
inst✝⁸ : AddCommMonoid N₃
inst✝⁷ : Module R N₃
inst✝⁶ : DistribMulAction S N₃
inst✝⁵ : SMulCommClass R S N₃
inst✝⁴ : ContinuousConstSMul S N₃
inst✝³ : DistribMulAction S N₂
inst✝² : ContinuousConstSMul S N₂
inst✝¹ : SMulCommClass R S N₂
inst✝ : LinearMap.CompatibleSMul N₂ N₃ S R
hₗ : N₂ →L[R] N₃
c : S
fₗ : M →L[R] N₂
⊢ hₗ ∘SL (c • fₗ) = c • hₗ ∘SL fₗ

Tactic:
ext x

Goal state after:
R : Type u_1
S : Type u_4
inst✝¹⁷ : Semiring R
inst✝¹⁶ : Monoid S
M : Type u_6
inst✝¹⁵ : TopologicalSpace M
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R M
N₂ : Type u_9
inst✝¹² : TopologicalSpace N₂
inst✝¹¹ : AddCommMonoid N₂
inst✝¹⁰ : Module R N₂
N₃ : Type u_10
inst✝⁹ : TopologicalSpace N₃
inst✝⁸ : AddCommMonoid N₃
inst✝⁷ : Module R N₃
inst✝⁶ : DistribMulAction S N₃
inst✝⁵ : SMulCommClass R S N₃
inst✝⁴ : ContinuousConstSMul S N₃
inst✝³ : DistribMulAction S N₂
inst✝² : ContinuousConstSMul S N₂
inst✝¹ : SMulCommClass R S N₂
inst✝ : LinearMap.CompatibleSMul N₂ N₃ S R
hₗ : N₂ →L[R] N₃
c : S
fₗ : M →L[R] N₂
x : M
⊢ (hₗ ∘SL (c • fₗ)) x = (c • hₗ ∘SL fₗ) x
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₃
M : Type u_6
inst✝¹³ : TopologicalSpace M
inst✝¹² : AddCommMonoid M
inst✝¹¹ : Module R M
M₂ : Type u_7
inst✝¹⁰ : TopologicalSpace M₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
M₃ : Type u_8
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝⁴ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝³ : SMulCommClass R₂ R₂ M₂
inst✝² : SMulCommClass R₃ R₃ M₃
inst✝¹ : ContinuousConstSMul R₂ M₂
inst✝ : ContinuousConstSMul R₃ M₃
h : M₂ →SL[σ₂₃] M₃
c : R₂
f : M →SL[σ₁₂] M₂
⊢ h ∘SL (c • f) = σ₂₃ c • h ∘SL f

Tactic:
ext x

Goal state after:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝¹⁶ : Semiring R
inst✝¹⁵ : Semiring R₂
inst✝¹⁴ : Semiring R₃
M : Type u_6
inst✝¹³ : TopologicalSpace M
inst✝¹² : AddCommMonoid M
inst✝¹¹ : Module R M
M₂ : Type u_7
inst✝¹⁰ : TopologicalSpace M₂
inst✝⁹ : AddCommMonoid M₂
inst✝⁸ : Module R₂ M₂
M₃ : Type u_8
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
inst✝⁴ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝³ : SMulCommClass R₂ R₂ M₂
inst✝² : SMulCommClass R₃ R₃ M₃
inst✝¹ : ContinuousConstSMul R₂ M₂
inst✝ : ContinuousConstSMul R₃ M₃
h : M₂ →SL[σ₂₃] M₃
c : R₂
f : M →SL[σ₁₂] M₂
x : M
⊢ (h ∘SL (c • f)) x = (σ₂₃ c • h ∘SL f) x
Module: Mathlib.Algebra.Group.WithOne.Basic

Goal state before:
pp: α : Type u
inst✝ : Mul α
⊢ mapMulHom (MulHom.id α) = MonoidHom.id (WithOne α)

Tactic:
ext x

Goal state after:
α : Type u
inst✝ : Mul α
x : WithOne α
⊢ (mapMulHom (MulHom.id α)) x = (MonoidHom.id (WithOne α)) x
Module: Mathlib.Algebra.Category.MonCat.Colimits

Goal state before:
pp: J : Type v
inst✝ : Category.{u, v} J
F : J ⥤ MonCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
⊢ m = descMorphism F s

Tactic:
ext x

Goal state after:
J : Type v
inst✝ : Category.{u, v} J
F : J ⥤ MonCat
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
x : ↑(colimitCocone F).pt
⊢ (Hom.hom m) x = (Hom.hom (descMorphism F s)) x
Module: Mathlib.Algebra.Category.MonCat.Shrink

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
F G : C ⥤ MonCat
τ : F ⟶ G
inst✝¹ : ∀ (X : C), Small.{w, w'} ↑(F.obj X)
inst✝ : ∀ (X : C), Small.{w, w'} ↑(G.obj X)
X Y : C
f : X ⟶ Y
⊢ (shrinkFunctor.{w, w', v, u} F).map f ≫
      ofHom ((Shrink.mulEquiv.symm.toMonoidHom.comp (Hom.hom (τ.app Y))).comp Shrink.mulEquiv.toMonoidHom) =
    ofHom ((Shrink.mulEquiv.symm.toMonoidHom.comp (Hom.hom (τ.app X))).comp Shrink.mulEquiv.toMonoidHom) ≫
      (shrinkFunctor.{w, w', v, u} G).map f

Tactic:
ext x

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
F G : C ⥤ MonCat
τ : F ⟶ G
inst✝¹ : ∀ (X : C), Small.{w, w'} ↑(F.obj X)
inst✝ : ∀ (X : C), Small.{w, w'} ↑(G.obj X)
X Y : C
f : X ⟶ Y
x : ↑((shrinkFunctor.{w, w', v, u} F).obj X)
⊢ (Hom.hom
        ((shrinkFunctor.{w, w', v, u} F).map f ≫
          ofHom ((Shrink.mulEquiv.symm.toMonoidHom.comp (Hom.hom (τ.app Y))).comp Shrink.mulEquiv.toMonoidHom)))
      x =
    (Hom.hom
        (ofHom ((Shrink.mulEquiv.symm.toMonoidHom.comp (Hom.hom (τ.app X))).comp Shrink.mulEquiv.toMonoidHom) ≫
          (shrinkFunctor.{w, w', v, u} G).map f))
      x
Module: Mathlib.Algebra.Category.Ring.Epi

Goal state before:
pp: R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Epi (ofHom (algebraMap R S)) ↔ Algebra.IsEpi R S

Tactic:
Algebra.isEpi_iff_forall_one_tmul_eq,

Goal state after:
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Epi (ofHom (algebraMap R S)) ↔ ∀ (a : S), 1 ⊗ₜ[R] a = a ⊗ₜ[R] 1
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
inst✝⁹ : Semiring R₁
inst✝⁸ : Semiring R₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst✝⁷ : RingHomInvPair σ₁₂ σ₂₁
inst✝⁶ : RingHomInvPair σ₂₁ σ₁₂
M₁ : Type u_4
inst✝⁵ : TopologicalSpace M₁
inst✝⁴ : AddCommMonoid M₁
M₂ : Type u_5
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₁ M₁
inst✝ : Module R₂ M₂
e : M₁ ≃SL[σ₁₂] M₂
⊢ ⇑e.symm ∘ ⇑e = id

Tactic:
ext x

Goal state after:
R₁ : Type u_1
R₂ : Type u_2
inst✝⁹ : Semiring R₁
inst✝⁸ : Semiring R₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst✝⁷ : RingHomInvPair σ₁₂ σ₂₁
inst✝⁶ : RingHomInvPair σ₂₁ σ₁₂
M₁ : Type u_4
inst✝⁵ : TopologicalSpace M₁
inst✝⁴ : AddCommMonoid M₁
M₂ : Type u_5
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₁ M₁
inst✝ : Module R₂ M₂
e : M₁ ≃SL[σ₁₂] M₂
x : M₁
⊢ (⇑e.symm ∘ ⇑e) x = id x
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
inst✝⁹ : Semiring R₁
inst✝⁸ : Semiring R₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst✝⁷ : RingHomInvPair σ₁₂ σ₂₁
inst✝⁶ : RingHomInvPair σ₂₁ σ₁₂
M₁ : Type u_4
inst✝⁵ : TopologicalSpace M₁
inst✝⁴ : AddCommMonoid M₁
M₂ : Type u_5
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₁ M₁
inst✝ : Module R₂ M₂
e : M₁ ≃SL[σ₁₂] M₂
⊢ ⇑e ∘ ⇑e.symm = id

Tactic:
ext x

Goal state after:
R₁ : Type u_1
R₂ : Type u_2
inst✝⁹ : Semiring R₁
inst✝⁸ : Semiring R₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst✝⁷ : RingHomInvPair σ₁₂ σ₂₁
inst✝⁶ : RingHomInvPair σ₂₁ σ₁₂
M₁ : Type u_4
inst✝⁵ : TopologicalSpace M₁
inst✝⁴ : AddCommMonoid M₁
M₂ : Type u_5
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₁ M₁
inst✝ : Module R₂ M₂
e : M₁ ≃SL[σ₁₂] M₂
x : M₂
⊢ (⇑e ∘ ⇑e.symm) x = id x
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
hM : Subsingleton M
hM₂ : Subsingleton M₂
e : M ≃L[R] M₂ :=
  { toFun := 0, map_add' := ⋯, map_smul' := ⋯, invFun := 0, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯,
    continuous_invFun := ⋯ }
⊢ ↑e = 0

Tactic:
ext x

Goal state after:
case refine_2
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
hM : Subsingleton M
hM₂ : Subsingleton M₂
e : M ≃L[R] M₂ :=
  { toFun := 0, map_add' := ⋯, map_smul' := ⋯, invFun := 0, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯,
    continuous_invFun := ⋯ }
x : M
⊢ ↑e x = 0 x
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: case pos
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
h : IsInvertible 0
hM : Subsingleton M
hM₂ : Subsingleton M₂
⊢ inverse 0 = 0

Tactic:
ext x

Goal state after:
case pos
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
h : IsInvertible 0
hM : Subsingleton M
hM₂ : Subsingleton M₂
x : M₂
⊢ (inverse 0) x = 0 x
Module: Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : Ring S
inst✝ : Algebra R S
s : S
hs : s ∈ Set.range ⇑(algebraMap R S)
w✝ : R
hr : (algebraMap R S) w✝ = s
⊢ (includeLeftSubRight R S) s = 0

Tactic:
simp [← hr, algebraMap_eq_smul_one]

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

Goal state before:
pp: R : Type u
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
M : ModuleCat R
I : Type u_1
X✝ : I → TopModuleCat R
f✝ : (i : I) → (X✝ i).toModuleCat ⟶ M
J : Type u_2
inst✝ : Category.{v_1, u_2} J
F : J ⥤ TopModuleCat R
c : Cocone (F ⋙ forget₂ (TopModuleCat R) (ModuleCat R))
X Y : J
f : X ⟶ Y
⊢ F.map f ≫ toCoinduced c.ι.app Y = toCoinduced c.ι.app X ≫ ((Functor.const J).obj (coinduced c.ι.app)).map f

Tactic:
ext x

Goal state after:
R : Type u
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
M : ModuleCat R
I : Type u_1
X✝ : I → TopModuleCat R
f✝ : (i : I) → (X✝ i).toModuleCat ⟶ M
J : Type u_2
inst✝ : Category.{v_1, u_2} J
F : J ⥤ TopModuleCat R
c : Cocone (F ⋙ forget₂ (TopModuleCat R) (ModuleCat R))
X Y : J
f : X ⟶ Y
x : ↑(F.obj X).toModuleCat
⊢ (hom (F.map f ≫ toCoinduced c.ι.app Y)) x =
    (hom (toCoinduced c.ι.app X ≫ ((Functor.const J).obj (coinduced c.ι.app)).map f)) x
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic

Goal state before:
pp: R : Type u
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
M : ModuleCat R
I : Type u_1
X : I → TopModuleCat R
f : (i : I) → (X i).toModuleCat ⟶ M
J : Type u_2
inst✝ : Category.{v_1, u_2} J
F : J ⥤ TopModuleCat R
c : Cocone (F ⋙ forget₂ (TopModuleCat R) (ModuleCat R))
hc : IsColimit c
s : Cocone F
i : J
⊢ (ofCocone c).ι.app i ≫
      ofHom
        { toLinearMap := ModuleCat.Hom.hom (hc.desc ((forget₂ (TopModuleCat R) (ModuleCat R)).mapCocone s)),
          cont := ⋯ } =
    s.ι.app i

Tactic:
ext x

Goal state after:
R : Type u
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
M : ModuleCat R
I : Type u_1
X : I → TopModuleCat R
f : (i : I) → (X i).toModuleCat ⟶ M
J : Type u_2
inst✝ : Category.{v_1, u_2} J
F : J ⥤ TopModuleCat R
c : Cocone (F ⋙ forget₂ (TopModuleCat R) (ModuleCat R))
hc : IsColimit c
s : Cocone F
i : J
x : ↑(F.obj i).toModuleCat
⊢ (hom
        ((ofCocone c).ι.app i ≫
          ofHom
            { toLinearMap := ModuleCat.Hom.hom (hc.desc ((forget₂ (TopModuleCat R) (ModuleCat R)).mapCocone s)),
              cont := ⋯ }))
      x =
    (hom (s.ι.app i)) x
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic

Goal state before:
pp: R : Type u
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
M : ModuleCat R
I : Type u_1
X : I → TopModuleCat R
f : (i : I) → (X i).toModuleCat ⟶ M
J : Type u_2
inst✝ : Category.{v_1, u_2} J
F : J ⥤ TopModuleCat R
c : Cocone (F ⋙ forget₂ (TopModuleCat R) (ModuleCat R))
hc : IsColimit c
s : Cocone F
m : (ofCocone c).pt ⟶ s.pt
H : ∀ (j : J), (ofCocone c).ι.app j ≫ m = s.ι.app j
⊢ m =
    ofHom
      { toLinearMap := ModuleCat.Hom.hom (hc.desc ((forget₂ (TopModuleCat R) (ModuleCat R)).mapCocone s)), cont := ⋯ }

Tactic:
ext x

Goal state after:
R : Type u
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
M : ModuleCat R
I : Type u_1
X : I → TopModuleCat R
f : (i : I) → (X i).toModuleCat ⟶ M
J : Type u_2
inst✝ : Category.{v_1, u_2} J
F : J ⥤ TopModuleCat R
c : Cocone (F ⋙ forget₂ (TopModuleCat R) (ModuleCat R))
hc : IsColimit c
s : Cocone F
m : (ofCocone c).pt ⟶ s.pt
H : ∀ (j : J), (ofCocone c).ι.app j ≫ m = s.ι.app j
x : ↑(ofCocone c).pt.toModuleCat
⊢ (hom m) x =
    (hom
        (ofHom
          { toLinearMap := ModuleCat.Hom.hom (hc.desc ((forget₂ (TopModuleCat R) (ModuleCat R)).mapCocone s)),
            cont := ⋯ }))
      x
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic

Goal state before:
pp: R : Type u
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
M : ModuleCat R
I : Type u_1
X✝ : I → TopModuleCat R
f✝ : (i : I) → M ⟶ (X✝ i).toModuleCat
J : Type u_2
inst✝ : Category.{v_1, u_2} J
F : J ⥤ TopModuleCat R
c : Cone (F ⋙ forget₂ (TopModuleCat R) (ModuleCat R))
X Y : J
f : X ⟶ Y
⊢ ((Functor.const J).obj (induced c.π.app)).map f ≫ fromInduced c.π.app Y = fromInduced c.π.app X ≫ F.map f

Tactic:
ext x

Goal state after:
R : Type u
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
M : ModuleCat R
I : Type u_1
X✝ : I → TopModuleCat R
f✝ : (i : I) → M ⟶ (X✝ i).toModuleCat
J : Type u_2
inst✝ : Category.{v_1, u_2} J
F : J ⥤ TopModuleCat R
c : Cone (F ⋙ forget₂ (TopModuleCat R) (ModuleCat R))
X Y : J
f : X ⟶ Y
x : ↑(((Functor.const J).obj (induced c.π.app)).obj X).toModuleCat
⊢ (hom (((Functor.const J).obj (induced c.π.app)).map f ≫ fromInduced c.π.app Y)) x =
    (hom (fromInduced c.π.app X ≫ F.map f)) x
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic

Goal state before:
pp: R : Type u
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
M : ModuleCat R
I : Type u_1
X✝ : I → TopModuleCat R
f✝ : (i : I) → M ⟶ (X✝ i).toModuleCat
J : Type u_2
inst✝ : Category.{v_1, u_2} J
F : J ⥤ TopModuleCat R
c : Cone (F ⋙ forget₂ (TopModuleCat R) (ModuleCat R))
X Y : J
f : X ⟶ Y
⊢ ((Functor.const J).obj (induced c.π.app)).map f ≫ fromInduced c.π.app Y = fromInduced c.π.app X ≫ F.map f

Tactic:
ext x; exact congr($(c.π.naturality f).hom x)

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

Goal state before:
pp: R : Type u
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
M : ModuleCat R
I : Type u_1
X : I → TopModuleCat R
f : (i : I) → M ⟶ (X i).toModuleCat
J : Type u_2
inst✝ : Category.{v_1, u_2} J
F : J ⥤ TopModuleCat R
c : Cone (F ⋙ forget₂ (TopModuleCat R) (ModuleCat R))
hc : IsLimit c
s : Cone F
i : J
⊢ ofHom { toLinearMap := ModuleCat.Hom.hom (hc.lift ((forget₂ (TopModuleCat R) (ModuleCat R)).mapCone s)), cont := ⋯ } ≫
      (ofCone c).π.app i =
    s.π.app i

Tactic:
ext x

Goal state after:
R : Type u
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
M : ModuleCat R
I : Type u_1
X : I → TopModuleCat R
f : (i : I) → M ⟶ (X i).toModuleCat
J : Type u_2
inst✝ : Category.{v_1, u_2} J
F : J ⥤ TopModuleCat R
c : Cone (F ⋙ forget₂ (TopModuleCat R) (ModuleCat R))
hc : IsLimit c
s : Cone F
i : J
x : ↑s.pt.toModuleCat
⊢ (hom
        (ofHom
            { toLinearMap := ModuleCat.Hom.hom (hc.lift ((forget₂ (TopModuleCat R) (ModuleCat R)).mapCone s)),
              cont := ⋯ } ≫
          (ofCone c).π.app i))
      x =
    (hom (s.π.app i)) x
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic

Goal state before:
pp: R : Type u
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
M : ModuleCat R
I : Type u_1
X : I → TopModuleCat R
f : (i : I) → M ⟶ (X i).toModuleCat
J : Type u_2
inst✝ : Category.{v_1, u_2} J
F : J ⥤ TopModuleCat R
c : Cone (F ⋙ forget₂ (TopModuleCat R) (ModuleCat R))
hc : IsLimit c
s : Cone F
m : s.pt ⟶ (ofCone c).pt
H : ∀ (j : J), m ≫ (ofCone c).π.app j = s.π.app j
⊢ m =
    ofHom { toLinearMap := ModuleCat.Hom.hom (hc.lift ((forget₂ (TopModuleCat R) (ModuleCat R)).mapCone s)), cont := ⋯ }

Tactic:
ext x

Goal state after:
R : Type u
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
M : ModuleCat R
I : Type u_1
X : I → TopModuleCat R
f : (i : I) → M ⟶ (X i).toModuleCat
J : Type u_2
inst✝ : Category.{v_1, u_2} J
F : J ⥤ TopModuleCat R
c : Cone (F ⋙ forget₂ (TopModuleCat R) (ModuleCat R))
hc : IsLimit c
s : Cone F
m : s.pt ⟶ (ofCone c).pt
H : ∀ (j : J), m ≫ (ofCone c).π.app j = s.π.app j
x : ↑s.pt.toModuleCat
⊢ (hom m) x =
    (hom
        (ofHom
          { toLinearMap := ModuleCat.Hom.hom (hc.lift ((forget₂ (TopModuleCat R) (ModuleCat R)).mapCone s)),
            cont := ⋯ }))
      x
Module: Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
F : J ⥤ C
hF : IsEventuallyConstant F
inst✝ : IsCofiltered J
⊢ HasLimit F

Tactic:
obtain ⟨j, h⟩ := hF.exists_isEventuallyConstantTo

Goal state after:
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
F : J ⥤ C
hF : IsEventuallyConstant F
inst✝ : IsCofiltered J
j : J
h : F.IsEventuallyConstantTo j
⊢ HasLimit F
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic

Goal state before:
pp: case hxy
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X Y : TopCat
f : X ⟶ Y
τ : TopologicalSpace (↑Y →₀ R)
x✝ :
  τ ∈
    {t |
      ContinuousSMul R (↑Y →₀ R) ∧
        ContinuousAdd (↑Y →₀ R) ∧ TopologicalSpace.coinduced (fun x ↦ Finsupp.single x 1) Y.str ≤ t}
hτ₁ : ContinuousSMul R (↑Y →₀ R)
hτ₂ : ContinuousAdd (↑Y →₀ R)
hτ₃ : TopologicalSpace.coinduced (fun x ↦ Finsupp.single x 1) Y.str ≤ τ
⊢ ((Finsupp.lmapDomain R R ⇑(TopCat.Hom.hom f)).toFun ∘ fun x ↦ Finsupp.single x 1) =
    (fun x ↦ Finsupp.single x 1) ∘ (TopCat.Hom.hom f).toFun

Tactic:
ext x

Goal state after:
case hxy
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X Y : TopCat
f : X ⟶ Y
τ : TopologicalSpace (↑Y →₀ R)
x✝ :
  τ ∈
    {t |
      ContinuousSMul R (↑Y →₀ R) ∧
        ContinuousAdd (↑Y →₀ R) ∧ TopologicalSpace.coinduced (fun x ↦ Finsupp.single x 1) Y.str ≤ t}
hτ₁ : ContinuousSMul R (↑Y →₀ R)
hτ₂ : ContinuousAdd (↑Y →₀ R)
hτ₃ : TopologicalSpace.coinduced (fun x ↦ Finsupp.single x 1) Y.str ≤ τ
x : ↑X
⊢ ((Finsupp.lmapDomain R R ⇑(TopCat.Hom.hom f)).toFun ∘ fun x ↦ Finsupp.single x 1) x =
    ((fun x ↦ Finsupp.single x 1) ∘ (TopCat.Hom.hom f).toFun) x
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
M : TopCat
⊢ freeMap R (𝟙 M) = 𝟙 (freeObj R M)

Tactic:
ext x

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
M : TopCat
x : ↑(freeObj R M).toModuleCat
⊢ (hom (freeMap R (𝟙 M))) x = (hom (𝟙 (freeObj R M))) x
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X Y : TopCat
f : X ⟶ Y
⊢ (𝟭 TopCat).map f ≫ TopCat.ofHom { toFun := fun x ↦ Finsupp.single x 1, continuous_toFun := ⋯ } =
    TopCat.ofHom { toFun := fun x ↦ Finsupp.single x 1, continuous_toFun := ⋯ } ≫
      (free R ⋙ forget₂ (TopModuleCat R) TopCat).map f

Tactic:
ext x

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X Y : TopCat
f : X ⟶ Y
x : ↑((𝟭 TopCat).obj X)
⊢ (hom ((𝟭 TopCat).map f ≫ TopCat.ofHom { toFun := fun x ↦ Finsupp.single x 1, continuous_toFun := ⋯ })) x =
    (hom
        (TopCat.ofHom { toFun := fun x ↦ Finsupp.single x 1, continuous_toFun := ⋯ } ≫
          (free R ⋙ forget₂ (TopModuleCat R) TopCat).map f))
      x