mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer

Goal state before:
pp: case id
J : MulticospanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a : J.R
⊢ Hom.id (right a) ∈ if e : a = a then {eqToHom ⋯} else ∅

Tactic:
;

Goal state after:
case id
J : MulticospanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a : J.R
⊢ Hom.id (right a) ∈ if e : a = a then {eqToHom ⋯} else ∅
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer

Goal state before:
pp: case id
J : MultispanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a : J.L
⊢ Hom.id (left a) ∈ if e : a = a then {eqToHom ⋯} else ∅

Tactic:
;

Goal state after:
case id
J : MultispanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a : J.L
⊢ Hom.id (left a) ∈ if e : a = a then {eqToHom ⋯} else ∅
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer

Goal state before:
pp: J : MultispanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a : J.L
h₂ : J.snd a = J.fst a
f : (left a ⟶ right (J.fst a)) → Prop :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ f (Hom.fst a ≫ eqToHom ⋯) = ?m.532 (J.fst a) ⋯ h₂

Tactic:
;

Goal state after:
J : MultispanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a : J.L
h₂ : J.snd a = J.fst a
f : (left a ⟶ right (J.fst a)) → Prop :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ f (Hom.fst a ≫ eqToHom ⋯) = ?m.532 (J.fst a) ⋯ h₂
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer

Goal state before:
pp: J : MultispanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a : J.L
b : J.R
h₁ : J.fst a = b
h₂ : J.snd a = b
f : (left a ⟶ right b) → Prop :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
| f (Hom.fst a ≫ eqToHom ⋯)

Tactic:
tactic => subst h₁; simp only [eqToHom_refl, f]

Goal state after:
J : MultispanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a : J.L
h₂ : J.snd a = J.fst a
f : (left a ⟶ right (J.fst a)) → Prop :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
| failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer

Goal state before:
pp: J : MultispanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a : J.L
h₁ : J.fst a = J.snd a
f : (left a ⟶ right (J.snd a)) → Prop :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ f (Hom.snd a ≫ eqToHom ⋯) = ?m.563 (J.snd a) ⋯ h₁

Tactic:
;

Goal state after:
J : MultispanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a : J.L
h₁ : J.fst a = J.snd a
f : (left a ⟶ right (J.snd a)) → Prop :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ f (Hom.snd a ≫ eqToHom ⋯) = ?m.563 (J.snd a) ⋯ h₁
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: S : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
G : Type u_5
inst✝²² : Semiring R
inst✝²¹ : Semiring S
inst✝²⁰ : AddCommMonoid V
inst✝¹⁹ : Module R V
inst✝¹⁸ : TopologicalSpace V
inst✝¹⁷ : Module S V
inst✝¹⁶ : ContinuousConstSMul S V
inst✝¹⁵ : AddCommMonoid W
inst✝¹⁴ : Module R W
inst✝¹³ : TopologicalSpace W
inst✝¹² : Module S W
inst✝¹¹ : ContinuousConstSMul S W
inst✝¹⁰ : AddCommMonoid G
inst✝⁹ : Module R G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Module S G
inst✝⁶ : ContinuousConstSMul S G
inst✝⁵ : SMulCommClass R S W
inst✝⁴ : SMul S R
inst✝³ : IsScalarTower S R V
inst✝² : IsScalarTower S R W
inst✝¹ : SMulCommClass R S V
inst✝ : IsScalarTower S R G
α : Sˣ
e : G ≃L[R] V
f : V ≃L[R] W
x✝ : G
⊢ ((α • e).trans f) x✝ = (α • e.trans f) x✝

Tactic:
;

Goal state after:
S : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
G : Type u_5
inst✝²² : Semiring R
inst✝²¹ : Semiring S
inst✝²⁰ : AddCommMonoid V
inst✝¹⁹ : Module R V
inst✝¹⁸ : TopologicalSpace V
inst✝¹⁷ : Module S V
inst✝¹⁶ : ContinuousConstSMul S V
inst✝¹⁵ : AddCommMonoid W
inst✝¹⁴ : Module R W
inst✝¹³ : TopologicalSpace W
inst✝¹² : Module S W
inst✝¹¹ : ContinuousConstSMul S W
inst✝¹⁰ : AddCommMonoid G
inst✝⁹ : Module R G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Module S G
inst✝⁶ : ContinuousConstSMul S G
inst✝⁵ : SMulCommClass R S W
inst✝⁴ : SMul S R
inst✝³ : IsScalarTower S R V
inst✝² : IsScalarTower S R W
inst✝¹ : SMulCommClass R S V
inst✝ : IsScalarTower S R G
α : Sˣ
e : G ≃L[R] V
f : V ≃L[R] W
x✝ : G
⊢ ((α • e).trans f) x✝ = (α • e.trans f) x✝
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: S : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
G : Type u_5
inst✝²¹ : Semiring R
inst✝²⁰ : Semiring S
inst✝¹⁹ : AddCommMonoid V
inst✝¹⁸ : Module R V
inst✝¹⁷ : TopologicalSpace V
inst✝¹⁶ : Module S V
inst✝¹⁵ : ContinuousConstSMul S V
inst✝¹⁴ : AddCommMonoid W
inst✝¹³ : Module R W
inst✝¹² : TopologicalSpace W
inst✝¹¹ : Module S W
inst✝¹⁰ : ContinuousConstSMul S W
inst✝⁹ : AddCommMonoid G
inst✝⁸ : Module R G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Module S G
inst✝⁵ : ContinuousConstSMul S G
inst✝⁴ : SMulCommClass R S W
inst✝³ : SMul S R
inst✝² : IsScalarTower S R V
inst✝¹ : IsScalarTower S R W
inst✝ : IsScalarTower S R G
α : Sˣ
e : G ≃L[R] V
f : V ≃L[R] W
x✝ : G
⊢ (e.trans (α • f)) x✝ = (α • e.trans f) x✝

Tactic:
;

Goal state after:
S : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
G : Type u_5
inst✝²¹ : Semiring R
inst✝²⁰ : Semiring S
inst✝¹⁹ : AddCommMonoid V
inst✝¹⁸ : Module R V
inst✝¹⁷ : TopologicalSpace V
inst✝¹⁶ : Module S V
inst✝¹⁵ : ContinuousConstSMul S V
inst✝¹⁴ : AddCommMonoid W
inst✝¹³ : Module R W
inst✝¹² : TopologicalSpace W
inst✝¹¹ : Module S W
inst✝¹⁰ : ContinuousConstSMul S W
inst✝⁹ : AddCommMonoid G
inst✝⁸ : Module R G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Module S G
inst✝⁵ : ContinuousConstSMul S G
inst✝⁴ : SMulCommClass R S W
inst✝³ : SMul S R
inst✝² : IsScalarTower S R V
inst✝¹ : IsScalarTower S R W
inst✝ : IsScalarTower S R G
α : Sˣ
e : G ≃L[R] V
f : V ≃L[R] W
x✝ : G
⊢ (e.trans (α • f)) x✝ = (α • e.trans f) x✝
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
inst✝⁵ : TopologicalSpace R
M : Type v
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : TopologicalSpace M
inst✝¹ : ContinuousAdd M
inst✝ : ContinuousSMul R M
x✝ : M
⊢ Neg.neg = HSMul.hSMul (-1)

Tactic:
;

Goal state after:
R : Type u
inst✝⁶ : Ring R
inst✝⁵ : TopologicalSpace R
M : Type v
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : TopologicalSpace M
inst✝¹ : ContinuousAdd M
inst✝ : ContinuousSMul R M
x✝ : M
⊢ Neg.neg = HSMul.hSMul (-1)
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
inst✝⁵ : TopologicalSpace R
M : Type v
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : TopologicalSpace M
inst✝¹ : ContinuousAdd M
inst✝ : ContinuousSMul R M
x✝¹ x✝ : M
⊢ -x✝ = -1 • x✝

Tactic:
;

Goal state after:
R : Type u
inst✝⁶ : Ring R
inst✝⁵ : TopologicalSpace R
M : Type v
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : TopologicalSpace M
inst✝¹ : ContinuousAdd M
inst✝ : ContinuousSMul R M
x✝¹ x✝ : M
⊢ -x✝ = -1 • x✝
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer

Goal state before:
pp: case id
J : MultispanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a : J.R
⊢ Hom.id (right a) ∈ if e : a = a then {eqToHom ⋯} else ∅

Tactic:
;

Goal state after:
case id
J : MultispanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a : J.R
⊢ Hom.id (right a) ∈ if e : a = a then {eqToHom ⋯} else ∅
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X Y : TopModuleCat R
e : ↑X.toModuleCat ≃L[R] ↑Y.toModuleCat
x✝ : ↑X.toModuleCat
⊢ (hom (ofHom ↑e ≫ ofHom ↑e.symm)) x✝ = (hom (𝟙 X)) x✝

Tactic:
;

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X Y : TopModuleCat R
e : ↑X.toModuleCat ≃L[R] ↑Y.toModuleCat
x✝ : ↑X.toModuleCat
⊢ (hom (ofHom ↑e ≫ ofHom ↑e.symm)) x✝ = (hom (𝟙 X)) x✝
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X Y : TopModuleCat R
e : ↑X.toModuleCat ≃L[R] ↑Y.toModuleCat
x✝ : ↑Y.toModuleCat
⊢ (hom (ofHom ↑e.symm ≫ ofHom ↑e)) x✝ = (hom (𝟙 Y)) x✝

Tactic:
;

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X Y : TopModuleCat R
e : ↑X.toModuleCat ≃L[R] ↑Y.toModuleCat
x✝ : ↑Y.toModuleCat
⊢ (hom (ofHom ↑e.symm ≫ ofHom ↑e)) x✝ = (hom (𝟙 Y)) x✝
Module: Mathlib.CategoryTheory.Comma.CardinalArrow

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Small.{w, u} C
x✝ : Arrow (Shrink.{w, u} C)
⊢ (Shrink.equivalence C).counit.app x✝.left ≫ x✝.hom ≫ (Shrink.equivalence C).counitInv.app x✝.right =
    eqToHom ⋯ ≫ x✝.hom ≫ eqToHom ⋯

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Small.{w, u} C
x✝ : Arrow (Shrink.{w, u} C)
⊢ (Shrink.equivalence C).counit.app x✝.left ≫ x✝.hom ≫ (Shrink.equivalence C).counitInv.app x✝.right =
    eqToHom ⋯ ≫ x✝.hom ≫ eqToHom ⋯
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
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

Tactic:
;

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.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
i₀ : J
h : F.IsEventuallyConstantTo i₀
inst✝ : IsCofiltered J
s : Cone F
m : s.pt ⟶ h.cone.pt
hm : ∀ (j : J), m ≫ h.cone.π.app j = s.π.app j
⊢ m = s.π.app i₀

Tactic:
by simp only [← hm i₀, cone_π_app, coneπApp_eq_id, cone_pt, comp_id]

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

Tactic:
;

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

Tactic:
;

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

Tactic:
;

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
X : ModuleCat R
this : TopologicalSpace ↑X := ⊤
⊢ TopologicalSpace.coinduced (fun p ↦ p.1 + p.2) instTopologicalSpaceProd ≤ this

Tactic:
;

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X : ModuleCat R
this : TopologicalSpace ↑X := ⊤
⊢ TopologicalSpace.coinduced (fun p ↦ p.1 + p.2) instTopologicalSpaceProd ≤ this
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X : ModuleCat R
this✝ : TopologicalSpace ↑X := ⊤
this : ContinuousAdd ↑X
⊢ TopologicalSpace.coinduced (fun p ↦ p.1 • p.2) instTopologicalSpaceProd ≤ this✝

Tactic:
;

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X : ModuleCat R
this✝ : TopologicalSpace ↑X := ⊤
this : ContinuousAdd ↑X
⊢ TopologicalSpace.coinduced (fun p ↦ p.1 • p.2) instTopologicalSpaceProd ≤ this✝
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X Y : ModuleCat R
f : X ⟶ Y
this✝ : TopologicalSpace ↑X := ⊤
this : TopologicalSpace ↑Y := ⊤
⊢ TopologicalSpace.coinduced (ModuleCat.Hom.hom f).toFun (of R ↑X).topologicalSpace ≤ (of R ↑Y).topologicalSpace

Tactic:
;

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X Y : ModuleCat R
f : X ⟶ Y
this✝ : TopologicalSpace ↑X := ⊤
this : TopologicalSpace ↑Y := ⊤
⊢ TopologicalSpace.coinduced (ModuleCat.Hom.hom f).toFun (of R ↑X).topologicalSpace ≤ (of R ↑Y).topologicalSpace
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
i₀ : J
h : F.IsEventuallyConstantFrom i₀
inst✝ : IsFiltered J
c : Cocone F
hc : IsColimit c
⊢ IsIso (c.ι.app i₀)

Tactic:
simp only [← IsColimit.comp_coconePointUniqueUpToIso_inv hc h.isColimitCocone i₀,
    cocone_ι_app, coconeιApp_eq_id, id_comp]
  infer_instance

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X : TopModuleCat R
⊢ TopologicalSpace.coinduced LinearMap.id.toFun ((𝟭 (TopModuleCat R)).obj X).topologicalSpace ≤
    ((forget₂ (TopModuleCat R) (ModuleCat R) ⋙ indiscrete R).obj X).topologicalSpace

Tactic:
;

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X : TopModuleCat R
⊢ TopologicalSpace.coinduced LinearMap.id.toFun ((𝟭 (TopModuleCat R)).obj X).topologicalSpace ≤
    ((forget₂ (TopModuleCat R) (ModuleCat R) ⋙ indiscrete R).obj X).topologicalSpace
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic

Goal state before:
pp: 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

Tactic:
;

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✝ Z✝ : TopCat
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
x✝ : ↑(freeObj R X✝).toModuleCat
⊢ (hom (freeMap R (f ≫ g))) x✝ = (hom (freeMap R f ≫ freeMap R g)) x✝

Tactic:
;

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
X✝ Y✝ Z✝ : TopCat
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
x✝ : ↑(freeObj R X✝).toModuleCat
⊢ (hom (freeMap R (f ≫ g))) x✝ = (hom (freeMap R f ≫ freeMap R g)) 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
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

Tactic:
;

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
Module: Mathlib.CategoryTheory.Presentable.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F✝ G : C ⥤ D
e : F✝ ≅ G
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
A : C
J : Type w
x✝³ : SmallCategory J
x✝² : IsCardinalFiltered J κ
F : J ⥤ C
c : Cocone F
hc : IsColimit c
h : IsFiltered J
this : ∀ (j : J), IsIso ((((const C).obj A).mapCocone c).ι.app j)
x✝¹ : J
x✝ : ⋯.some ⟶ x✝¹
⊢ IsIso (𝟙 A)

Tactic:
;

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F✝ G : C ⥤ D
e : F✝ ≅ G
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
A : C
J : Type w
x✝³ : SmallCategory J
x✝² : IsCardinalFiltered J κ
F : J ⥤ C
c : Cocone F
hc : IsColimit c
h : IsFiltered J
this : ∀ (j : J), IsIso ((((const C).obj A).mapCocone c).ι.app j)
x✝¹ : J
x✝ : ⋯.some ⟶ x✝¹
⊢ IsIso (𝟙 A)
Module: Mathlib.LinearAlgebra.TensorProduct.Pi

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Type u_2
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
N : Type u_3
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : Module S N
inst✝⁴ : IsScalarTower R S N
ι : Type u_4
M : ι → Type u_5
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
x : N
m : M i
j : ι
⊢ ((AlgebraTensorModule.curry ((piRightHom R S N M ∘ₗ piRightInv R S N M) ∘ₗ single S (fun i ↦ N ⊗[R] M i) i)) x) m j =
    ((AlgebraTensorModule.curry (LinearMap.id ∘ₗ single S (fun i ↦ N ⊗[R] M i) i)) x) m j

Tactic:
;

Goal state after:
R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Type u_2
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
N : Type u_3
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : Module S N
inst✝⁴ : IsScalarTower R S N
ι : Type u_4
M : ι → Type u_5
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
x : N
m : M i
j : ι
⊢ ((AlgebraTensorModule.curry ((piRightHom R S N M ∘ₗ piRightInv R S N M) ∘ₗ single S (fun i ↦ N ⊗[R] M i) i)) x) m j =
    ((AlgebraTensorModule.curry (LinearMap.id ∘ₗ single S (fun i ↦ N ⊗[R] M i) i)) x) m j
Module: Mathlib.LinearAlgebra.TensorProduct.Pi

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Type u_2
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
N : Type u_3
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : Module S N
inst✝⁴ : IsScalarTower R S N
ι : Type u_4
M : ι → Type u_5
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : N
j : ι
m : M j
⊢ ((AlgebraTensorModule.curry (piRightInv R S N M ∘ₗ piRightHom R S N M)) x ∘ₗ single R M j) m =
    ((AlgebraTensorModule.curry LinearMap.id) x ∘ₗ single R M j) m

Tactic:
;

Goal state after:
R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Type u_2
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra R S
N : Type u_3
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : Module S N
inst✝⁴ : IsScalarTower R S N
ι : Type u_4
M : ι → Type u_5
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : N
j : ι
m : M j
⊢ ((AlgebraTensorModule.curry (piRightInv R S N M ∘ₗ piRightHom R S N M)) x ∘ₗ single R M j) m =
    ((AlgebraTensorModule.curry LinearMap.id) x ∘ₗ single R M j) m
Module: Mathlib.Algebra.Category.Ring.Topology

Goal state before:
pp: R A : CommRingCat
inst✝ : TopologicalSpace ↑R
x✝² x✝¹ : A ⟶ R
e : ⇑(Hom.hom x✝²) = ⇑(Hom.hom x✝¹)
x✝ : ↑A
⊢ (Hom.hom x✝²) x✝ = (Hom.hom x✝¹) x✝

Tactic:
;

Goal state after:
R A : CommRingCat
inst✝ : TopologicalSpace ↑R
x✝² x✝¹ : A ⟶ R
e : ⇑(Hom.hom x✝²) = ⇑(Hom.hom x✝¹)
x✝ : ↑A
⊢ (Hom.hom x✝²) x✝ = (Hom.hom x✝¹) x✝
Module: Mathlib.Algebra.Category.Ring.Topology

Goal state before:
pp: R A B : CommRingCat
inst✝ : TopologicalSpace ↑R
f✝ : A ⟶ B
hf : Function.Surjective ⇑(ConcreteCategory.hom f✝)
this : IsEmbedding fun x ↦ x ∘ ⇑(Hom.hom f✝)
f g : B ⟶ R
e : (↑↑f.hom').1 = (↑↑g.hom').1
a : ↑B
⊢ (Hom.hom f) a = (Hom.hom g) a

Tactic:
;

Goal state after:
R A B : CommRingCat
inst✝ : TopologicalSpace ↑R
f✝ : A ⟶ B
hf : Function.Surjective ⇑(ConcreteCategory.hom f✝)
this : IsEmbedding fun x ↦ x ∘ ⇑(Hom.hom f✝)
f g : B ⟶ R
e : (↑↑f.hom').1 = (↑↑g.hom').1
a : ↑B
⊢ (Hom.hom f) a = (Hom.hom g) a
Module: Mathlib.Algebra.Category.Ring.Topology

Goal state before:
pp: case mp
R A B : CommRingCat
inst✝¹ : TopologicalSpace ↑R
inst✝ : T1Space ↑R
f : A ⟶ B
hf : Function.Surjective ⇑(ConcreteCategory.hom f)
this : IsClosed[instTopologicalSpaceHom] (⋂ i, {f_1 | (ConcreteCategory.hom f_1) ↑i = 0})
g : B ⟶ R
a : ↑A
ha : (Hom.hom f) a = 0
⊢ (ConcreteCategory.hom (f ≫ g)) a = 0

Tactic:
;

Goal state after:
case mp
R A B : CommRingCat
inst✝¹ : TopologicalSpace ↑R
inst✝ : T1Space ↑R
f : A ⟶ B
hf : Function.Surjective ⇑(ConcreteCategory.hom f)
this : IsClosed[instTopologicalSpaceHom] (⋂ i, {f_1 | (ConcreteCategory.hom f_1) ↑i = 0})
g : B ⟶ R
a : ↑A
ha : (Hom.hom f) a = 0
⊢ (ConcreteCategory.hom (f ≫ g)) a = 0