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

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
M : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : ContinuousNeg M
x : M
⊢ (neg R) x = -x

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝¹¹ : Ring R
R₂ : Type u_2
inst✝¹⁰ : Ring R₂
M : Type u_3
inst✝⁹ : TopologicalSpace M
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
M₂ : Type u_4
inst✝⁶ : TopologicalSpace M₂
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R₂ M₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst✝³ : RingHomInvPair σ₁₂ σ₂₁
inst✝² : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : Module R M₂
inst✝ : IsTopologicalAddGroup M
f₁ : M →L[R] M₂
f₂ : M₂ →L[R] M
h : Function.RightInverse ⇑f₂ ⇑f₁
x : M
⊢ (f₂.coprod (↑f₁).ker.subtypeL) ((f₁.prod (f₁.projKerOfRightInverse f₂ h)) x) = x

Tactic:
simp

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

Goal state before:
pp: 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₂
x✝ : IsInvertible 0
e : M ≃L[R] M₂
he : ↑e = 0
⊢ Subsingleton M

Tactic:
refine ⟨fun x y ↦ e.injective ?_⟩

Goal state after:
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₂
x✝ : IsInvertible 0
e : M ≃L[R] M₂
he : ↑e = 0
x y : M
⊢ e x = e y
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: 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₂
x : M✝
y : M₂
M : M✝ ≃L[R] M₂
⊢ M.symm y = x ↔ y = M x

Tactic:
exact ContinuousLinearEquiv.symm_apply_eq M

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

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
e : M₂ ≃L[R] M₃
f : M →L[R] M₂
A : M ≃L[R] M₃
hA : ↑A = ↑e ∘SL f
x✝ : M
⊢ f x✝ = (↑e.symm ∘SL ↑e ∘SL f) x✝

Tactic:
simp

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

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
e : M₂ ≃L[R] M₃
f : M →L[R] M₂
A : M ≃L[R] M₃
hA : ↑A = ↑e ∘SL f
this : f = ↑e.symm ∘SL ↑e ∘SL f
⊢ (↑e.symm ∘SL ↑A).IsInvertible

Tactic:
simp

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

Goal state before:
pp: case mpr
R : Type u_1
M✝ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁹ : TopologicalSpace M✝
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M✝
inst✝⁴ : Module R M✝
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
e : M₂ ≃L[R] M₃
M : M✝ ≃L[R] M₂
⊢ (↑e ∘SL ↑M).IsInvertible

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
e : M₃ ≃L[R] M
f : M →L[R] M₂
A : M₃ ≃L[R] M₂
hA : ↑A = f ∘SL ↑e
x✝ : M
⊢ f x✝ = ((f ∘SL ↑e) ∘SL ↑e.symm) x✝

Tactic:
simp

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

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
e : M₃ ≃L[R] M
f : M →L[R] M₂
A : M₃ ≃L[R] M₂
hA : ↑A = f ∘SL ↑e
this : f = (f ∘SL ↑e) ∘SL ↑e.symm
⊢ (↑A ∘SL ↑e.symm).IsInvertible

Tactic:
simp

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

Goal state before:
pp: case mpr
R : Type u_1
M✝ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁹ : TopologicalSpace M✝
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M✝
inst✝⁴ : Module R M✝
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
e : M₃ ≃L[R] M✝
M : M✝ ≃L[R] M₂
⊢ (↑M ∘SL ↑e).IsInvertible

Tactic:
simp

Goal state after:
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
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra R T
⊢ ↑(LinearEquiv.restrictScalars R (TensorProduct.AlgebraTensorModule.distribBaseChange R T S S)) ∘ₗ
      LinearMap.lTensor T (includeLeftSubRight R S) =
    ↑R (includeLeftSubRight T (T ⊗[R] S))

Tactic:
ext
  simp [TensorProduct.tmul_sub, TensorProduct.one_def, tmul_one_tmul_one_tmul]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
f : M →L[R] M₂
N : M₂ ≃L[R] M₃
⊢ (↑N ∘SL f).inverse = f.inverse ∘SL (↑N).inverse

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight

Goal state before:
pp: case refine_2
R : Type u_3
inst✝⁵ : CommRing R
S : Type u_4
T : Type u_5
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Ring S
inst✝¹ : Algebra R S
inst✝ : Module.FaithfullyFlat R T
h : IsEffective T (T ⊗[R] S)
x✝ : T ⊗[R] S
⊢ ((↑(TensorProduct.includeLeftSubRight T (T ⊗[R] S))).comp (AddMonoidHom.id (T ⊗[R] S))) x✝ =
    ((↑(TensorProduct.AlgebraTensorModule.distribBaseChange R T S S)).toAddMonoidHom.comp
        ↑(LinearMap.lTensor T (TensorProduct.includeLeftSubRight R S)))
      x✝

Tactic:
simp

Goal state after:
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✝
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ ∀ (x : R),
    (algebraMap R S) x ∈
      (CommRingCat.Hom.hom (CommRingCat.pushoutCocone R S S).inl).eqLocus
        (CommRingCat.Hom.hom (CommRingCat.pushoutCocone R S S).inr)

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
M✝ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁹ : TopologicalSpace M✝
inst✝⁸ : TopologicalSpace M₂
inst✝⁷ : TopologicalSpace M₃
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M✝
inst✝⁴ : Module R M✝
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
g : M₂ →L[R] M₃
M : M✝ ≃L[R] M₂
⊢ (g ∘SL ↑M).inverse = (↑M).inverse ∘SL g.inverse

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
e : M ≃L[R] M
⊢ (↑((ContinuousLinearEquiv.unitsEquiv R M).symm e))⁻¹ʳ = (↑e).inverse

Tactic:
simp

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
e : M ≃L[R] M
⊢ ↑((ContinuousLinearEquiv.unitsEquiv R M).symm e)⁻¹ = ↑e.symm
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₂
e : M ≃L[R] M₂
f : M →L[R] M₂
e' : M ≃L[R] M₂
he' : ↑e' = f
x✝ : M₂
⊢ (↑e').inverse x✝ = ((↑(e'.trans e.symm))⁻¹ʳ ∘SL ↑e.symm) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Over

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : C
J : Type u_3
hJ : Category.{u_2, u_3} J
hJ' : IsCofiltered J
F : J ⥤ Over X
c : Cone F
hc : IsLimit c
s : Cone (F ⋙ Over.forget X)
i j k : J
hik : k ⟶ i
hjk : k ⟶ j
⊢ (s.π.app k ≫ (F ⋙ Over.forget X).map hjk) ≫ (F.obj j).hom = (s.π.app k ≫ (F ⋙ Over.forget X).map hik) ≫ (F.obj i).hom

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Over

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : C
J : Type u_3
hJ : Category.{u_2, u_3} J
hJ' : IsFiltered J
F : J ⥤ Under X
c : Cocone F
hc : IsColimit c
s : Cocone (F ⋙ Under.forget X)
i j k : J
hik : i ⟶ k
hjk : j ⟶ k
⊢ (F.obj j).hom ≫ (F ⋙ Under.forget X).map hjk ≫ s.ι.app k = (F.obj i).hom ≫ (F ⋙ Under.forget X).map hik ≫ s.ι.app k

Tactic:
simp

Goal state after:
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.L
⊢ Hom.id (left a) ∈ if e : a = a then {eqToHom ⋯} else ∅

Tactic:
simp

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

Goal state before:
pp: case h
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₂
e : M ≃L[R] M₂
f : M →L[R] M₂
F : (M →L[R] M)ˣ
hF : ↑F = ↑e.symm ∘SL f
x✝ : M
⊢ e ((↑e.symm ∘SL f) x✝) = f x✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer

Goal state before:
pp: case pos
J : MulticospanShape
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 b = a
h₂ : J.snd b = a
f : (left a ⟶ right b) → Prop :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ True ≠ False

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer

Goal state before:
pp: case neg
J : MulticospanShape
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 b = a
h₂ : ¬J.snd b = a
⊢ ({eqToHom ⋯ ≫ Hom.fst b} + 0).Nodup

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer

Goal state before:
pp: case pos
J : MulticospanShape
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 b = a
h✝ : J.snd b = a
⊢ (0 + {eqToHom ⋯ ≫ Hom.snd b}).Nodup

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer

Goal state before:
pp: case neg
J : MulticospanShape
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 b = a
h✝ : ¬J.snd b = a
⊢ (0 + 0).Nodup

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer

Goal state before:
pp: case fst
J : MulticospanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
b : J.R
⊢ Hom.fst b ∈
    {
      val :=
        (if e : J.fst b = J.fst b then {eqToHom ⋯ ≫ Hom.fst b} else 0) +
          if e : J.snd b = J.fst b then {eqToHom ⋯ ≫ Hom.snd b} else 0,
      nodup := ⋯ }

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer

Goal state before:
pp: case snd
J : MulticospanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
b : J.R
⊢ Hom.snd b ∈
    {
      val :=
        (if e : J.fst b = J.snd b then {eqToHom ⋯ ≫ Hom.fst b} else 0) +
          if e : J.snd b = J.snd b then {eqToHom ⋯ ≫ Hom.snd b} else 0,
      nodup := ⋯ }

Tactic:
simp

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

Goal state before:
pp: 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₂
e : M ≃L[R] M₂
⊢ ↑e ∘SL (↑e).inverse = ContinuousLinearMap.id R M₂

Tactic:
simp

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

Goal state before:
pp: 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₂
y : M₂
e : M ≃L[R] M₂
⊢ ↑e ((↑e).inverse y) = y

Tactic:
simp

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

Goal state before:
pp: 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₂
e : M ≃L[R] M₂
⊢ (↑e).inverse ∘SL ↑e = ContinuousLinearMap.id R M

Tactic:
simp

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

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

Goal state before:
pp: 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₂
y : M
e : M ≃L[R] M₂
⊢ (↑e).inverse (↑e y) = y

Tactic:
simp

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

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

Goal state before:
pp: 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₂
e : M ≃L[R] M₂
⊢ (↑e).inverse.IsInvertible

Tactic:
simp

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

Goal state before:
pp: 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₂
e : M ≃L[R] M₂
⊢ (↑e).inverse.inverse = ↑e

Tactic:
simp

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

Goal state before:
pp: case hl
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝¹⁰ : TopologicalSpace M
inst✝⁹ : TopologicalSpace M₂
inst✝⁸ : TopologicalSpace M₃
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₂
inst✝² : AddCommMonoid M₃
inst✝¹ : Module R M₃
inst✝ : ContinuousAdd M
f : M₂ →L[R] M
g : M₃ →L[R] M
x✝ : M₃
⊢ ((f.coprod g ∘SL ↑(ContinuousLinearEquiv.prodComm R M₃ M₂)) ∘SL inl R M₃ M₂) x✝ = (g.coprod f ∘SL inl R M₃ M₂) x✝

Tactic:
simp

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

Goal state before:
pp: case hr
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝¹⁰ : TopologicalSpace M
inst✝⁹ : TopologicalSpace M₂
inst✝⁸ : TopologicalSpace M₃
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₂
inst✝² : AddCommMonoid M₃
inst✝¹ : Module R M₃
inst✝ : ContinuousAdd M
f : M₂ →L[R] M
g : M₃ →L[R] M
x✝ : M₂
⊢ ((f.coprod g ∘SL ↑(ContinuousLinearEquiv.prodComm R M₃ M₂)) ∘SL inr R M₃ M₂) x✝ = (g.coprod f ∘SL inr R M₃ M₂) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer

Goal state before:
pp: case pos
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)
⊢ True ≠ False

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer

Goal state before:
pp: case neg
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
⊢ ({Hom.fst a ≫ eqToHom ⋯} + 0).Nodup

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer

Goal state before:
pp: case pos
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
⊢ (0 + {Hom.snd a ≫ eqToHom ⋯}).Nodup

Tactic:
simp

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

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer

Goal state before:
pp: case neg
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
⊢ (0 + 0).Nodup

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer

Goal state before:
pp: case fst
J : MultispanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a : J.L
⊢ Hom.fst a ∈
    {
      val :=
        (if e : J.fst a = J.fst a then {Hom.fst a ≫ eqToHom ⋯} else 0) +
          if e : J.snd a = J.fst a then {Hom.snd a ≫ eqToHom ⋯} else 0,
      nodup := ⋯ }

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer

Goal state before:
pp: case snd
J : MultispanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
a : J.L
⊢ Hom.snd a ∈
    {
      val :=
        (if e : J.fst a = J.snd a then {Hom.fst a ≫ eqToHom ⋯} else 0) +
          if e : J.snd a = J.snd a then {Hom.snd a ≫ eqToHom ⋯} else 0,
      nodup := ⋯ }

Tactic:
simp

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

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

Goal state after:
Module: Mathlib.CategoryTheory.Comma.CardinalArrow

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
x✝ : Arrow (ShrinkHoms.{u} C)
⊢ (ShrinkHoms.equivalence C).functor.mapArrow.obj ((ShrinkHoms.equivalence C).inverse.mapArrow.obj x✝) = x✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.CardinalArrow

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
x✝ : Arrow C
⊢ (ShrinkHoms.equivalence C).inverse.mapArrow.obj ((ShrinkHoms.equivalence C).functor.mapArrow.obj x✝) = x✝

Tactic:
simp

Goal state after:
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).functor.mapArrow.obj ((Shrink.equivalence C).inverse.mapArrow.obj x✝)).hom =
    eqToHom ⋯ ≫ x✝.hom ≫ eqToHom ⋯

Tactic:
simp

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) → 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
⊢ Continuous (ModuleCat.Hom.hom (hc.lift ((forget₂ (TopModuleCat R) (ModuleCat R)).mapCone s))).toFun

Tactic:
rw [continuous_iff_coinduced_le]

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
⊢ TopologicalSpace.coinduced (ModuleCat.Hom.hom (hc.lift ((forget₂ (TopModuleCat R) (ModuleCat R)).mapCone s))).toFun
      s.1.topologicalSpace ≤
    instTopologicalSpaceCarrier R (ofCone c).pt
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
⊢ h.coconeιApp i₀ = 𝟙 (F.obj i₀)

Tactic:
h.coconeιApp_eq i₀ i₀ (𝟙 _) (𝟙 _),

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
i₀ : J
h : F.IsEventuallyConstantFrom i₀
inst✝ : IsFiltered J
⊢ F.map (𝟙 i₀) ≫ (h.isoMap (𝟙 i₀) ⋯).inv = 𝟙 (F.obj i₀)
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 := ⊤
⊢ Continuous fun p ↦ p.1 + p.2

Tactic:
rw [continuous_iff_coinduced_le]

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
⊢ Continuous fun p ↦ p.1 • p.2

Tactic:
rw [continuous_iff_coinduced_le]

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✝