mathlib-initiative/mathlib-tactics huggingface dataset:
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₃
g₁ g₂ : M₂ →SL[σ₂₃] M₃
f : M₁ →SL[σ₁₂] M₂
x✝ : M₁
⊢ ((g₁ + g₂) ∘SL f) x✝ = (g₁ ∘SL f + g₂ ∘SL f) 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 σ₁₂ σ₂₃ σ₁₃
ι : Type u_9
s : Finset ι
inst✝¹ : ContinuousAdd M₂
inst✝ : ContinuousAdd M₃
g : M₂ →SL[σ₂₃] M₃
f : ι → M₁ →SL[σ₁₂] M₂
x✝ : M₁
⊢ (g ∘SL ∑ i ∈ s, f i) x✝ = (∑ i ∈ s, g ∘SL f i) x✝

Tactic:
simp

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

Goal state before:
pp: M₁ : Type u_4
inst✝¹² : TopologicalSpace M₁
inst✝¹¹ : AddCommMonoid M₁
M₂ : Type u_6
inst✝¹⁰ : TopologicalSpace M₂
inst✝⁹ : AddCommMonoid M₂
R : Type u_9
S : Type u_10
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
inst✝⁶ : Module R M₁
inst✝⁵ : Module R M₂
inst✝⁴ : Module R S
inst✝³ : Module S M₂
inst✝² : IsScalarTower R S M₂
inst✝¹ : TopologicalSpace S
inst✝ : ContinuousSMul S M₂
f : M₁ →L[R] S
x✝ : M₁
⊢ (f.smulRight 0) x✝ = 0 x✝

Tactic:
simp

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

Goal state before:
pp: M₁ : Type u_4
inst✝¹² : TopologicalSpace M₁
inst✝¹¹ : AddCommMonoid M₁
M₂ : Type u_6
inst✝¹⁰ : TopologicalSpace M₂
inst✝⁹ : AddCommMonoid M₂
R : Type u_9
S : Type u_10
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
inst✝⁶ : Module R M₁
inst✝⁵ : Module R M₂
inst✝⁴ : Module R S
inst✝³ : Module S M₂
inst✝² : IsScalarTower R S M₂
inst✝¹ : TopologicalSpace S
inst✝ : ContinuousSMul S M₂
x : M₂
x✝ : M₁
⊢ (smulRight 0 x) x✝ = 0 x✝

Tactic:
simp

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

Goal state before:
pp: R₁ : Type u_1
inst✝¹² : Semiring 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₂
inst✝⁵ : TopologicalSpace R₁
inst✝⁴ : ContinuousSMul R₁ M₂
M₃ : Type u_9
inst✝³ : AddCommMonoid M₃
inst✝² : Module R₁ M₃
inst✝¹ : TopologicalSpace M₃
inst✝ : ContinuousSMul R₁ M₃
f : M₃ →L[R₁] R₁
g : M₁ →L[R₁] R₁
x : M₂
y : M₃
x✝ : M₁
⊢ (f.smulRight x ∘SL g.smulRight y) x✝ = (g.smulRight (f y • x)) x✝

Tactic:
simp

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

Goal state before:
pp: R₁ : Type u_1
inst✝⁵ : Semiring R₁
M₁ : Type u_4
inst✝⁴ : TopologicalSpace M₁
inst✝³ : AddCommMonoid M₁
inst✝² : Module R₁ M₁
inst✝¹ : TopologicalSpace R₁
inst✝ : ContinuousSMul R₁ M₁
⊢ (toSpanSingleton R₁ 0) 1 = 0 1

Tactic:
simp

Goal state after:
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₂
x : M
⊢ (g ∘SL (-f)) x = (-g ∘SL f) x

Tactic:
simp

Goal state after:
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₃
g : M₂ →SL[σ₂₃] M₃
f : M →SL[σ₁₂] M₂
x✝ : M
⊢ ((-g) ∘SL f) x✝ = (-g ∘SL f) x✝

Tactic:
simp

Goal state after:
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₁ f₂ : M →SL[σ₁₂] M₂
x✝ : M
⊢ (g ∘SL (f₁ - f₂)) x✝ = (g ∘SL f₁ - g ∘SL f₂) x✝

Tactic:
simp

Goal state after:
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₃
g₁ g₂ : M₂ →SL[σ₂₃] M₃
f : M →SL[σ₁₂] M₂
x✝ : M
⊢ ((g₁ - g₂) ∘SL f) x✝ = (g₁ ∘SL f - g₂ ∘SL f) x✝

Tactic:
simp

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

Goal state before:
pp: case zero
R : Type u_1
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
c : R
⊢ (toSpanSingleton R c ^ 0) 1 = (toSpanSingleton R (c ^ 0)) 1

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁷ : TopologicalSpace R
inst✝⁶ : DivisionRing R
inst✝⁵ : ContinuousSub R
inst✝⁴ : AddCommGroup M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousAdd M
inst✝¹ : Module R M
inst✝ : ContinuousSMul R M
f : StrongDual R M
hf : f ≠ 0
x : M
hx : f x ≠ 0
y : M
⊢ (fun a ↦ y + (a - f y) • (f x)⁻¹ • x) (f y) = y

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

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
U : Type u_2
V : Type u_3
W : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid U
inst✝⁹ : Module R U
inst✝⁸ : TopologicalSpace U
inst✝⁷ : AddCommMonoid V
inst✝⁶ : Module R V
inst✝⁵ : TopologicalSpace V
inst✝⁴ : AddCommMonoid W
inst✝³ : Module R W
inst✝² : TopologicalSpace W
inst✝¹ : ContinuousAdd W
inst✝ : ContinuousConstSMul R W
f : U →L[R] V
x✝¹ x✝ : V →L[R] W
⊢ (x✝¹ + x✝) ∘SL f = x✝¹ ∘SL f + x✝ ∘SL f

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
U : Type u_2
V : Type u_3
W : Type u_4
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : AddCommMonoid U
inst✝⁹ : Module R U
inst✝⁸ : TopologicalSpace U
inst✝⁷ : AddCommMonoid V
inst✝⁶ : Module R V
inst✝⁵ : TopologicalSpace V
inst✝⁴ : AddCommMonoid W
inst✝³ : Module R W
inst✝² : TopologicalSpace W
inst✝¹ : ContinuousAdd W
inst✝ : ContinuousConstSMul R W
f : U →L[R] V
x✝¹ : R
x✝ : V →L[R] W
⊢ (x✝¹ • x✝) ∘SL f = (RingHom.id R) x✝¹ • x✝ ∘SL f

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
U : Type u_2
V : Type u_3
W : Type u_4
inst✝¹³ : CommSemiring R
inst✝¹² : AddCommMonoid U
inst✝¹¹ : Module R U
inst✝¹⁰ : TopologicalSpace U
inst✝⁹ : AddCommMonoid V
inst✝⁸ : Module R V
inst✝⁷ : TopologicalSpace V
inst✝⁶ : ContinuousAdd V
inst✝⁵ : ContinuousConstSMul R V
inst✝⁴ : AddCommMonoid W
inst✝³ : Module R W
inst✝² : TopologicalSpace W
inst✝¹ : ContinuousAdd W
inst✝ : ContinuousConstSMul R W
x✝³ x✝² : U →L[R] V
x✝¹ : V →L[R] W
x✝ : U
⊢ ((lcomp W (x✝³ + x✝²)) x✝¹) x✝ = ((lcomp W x✝³ + lcomp W x✝²) x✝¹) x✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
U : Type u_2
V : Type u_3
W : Type u_4
inst✝¹³ : CommSemiring R
inst✝¹² : AddCommMonoid U
inst✝¹¹ : Module R U
inst✝¹⁰ : TopologicalSpace U
inst✝⁹ : AddCommMonoid V
inst✝⁸ : Module R V
inst✝⁷ : TopologicalSpace V
inst✝⁶ : ContinuousAdd V
inst✝⁵ : ContinuousConstSMul R V
inst✝⁴ : AddCommMonoid W
inst✝³ : Module R W
inst✝² : TopologicalSpace W
inst✝¹ : ContinuousAdd W
inst✝ : ContinuousConstSMul R W
x✝³ : R
x✝² : U →L[R] V
x✝¹ : V →L[R] W
x✝ : U
⊢ ((lcomp W (x✝³ • x✝²)) x✝¹) x✝ = (((RingHom.id R) x✝³ • lcomp W x✝²) x✝¹) x✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹⁰ : Semiring R
inst✝⁹ : Semiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : Module S M
inst✝⁵ : SMulCommClass R S M
inst✝⁴ : TopologicalSpace M
inst✝³ : ContinuousAdd M
inst✝² : ContinuousConstSMul S M
inst✝¹ : TopologicalSpace R
inst✝ : ContinuousSMul R M
x : M
⊢ (fun f ↦ f 1) (toSpanSingleton R x) = x

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
inst✝¹⁰ : Semiring R
inst✝⁹ : Semiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
inst✝⁶ : Module S M
inst✝⁵ : SMulCommClass R S M
inst✝⁴ : TopologicalSpace M
inst✝³ : ContinuousAdd M
inst✝² : ContinuousConstSMul S M
inst✝¹ : TopologicalSpace R
inst✝ : ContinuousSMul R M
f : R →L[R] M
⊢ (toSpanSingleton R ((fun f ↦ f 1) f)) 1 = f 1

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
M N : TopModuleCat R
φ : M ⟶ N
m : ↑M.toModuleCat
⊢ (↑(Hom.hom φ)).range.mkQ ((ConcreteCategory.hom φ) m) = 0

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Projective.Preserves

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : EnoughProjectives C
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.PreservesProjectiveObjects
X Y : D
f : X ⟶ Y
x✝ : Epi f
⊢ adj.unit.app (Projective.over (G.obj Y)) ≫
      G.map (Projective.factorThru (F.map (Projective.π (G.obj Y)) ≫ adj.counit.app Y) f ≫ f) =
    Projective.π (G.obj Y)

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
M N : TopModuleCat R
φ : M ⟶ N
S : ShortComplex (TopModuleCat R)
⊢ (isLimitKer S.g).lift (KernelFork.ofι S.f ⋯) ≫ cokerπ ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)) = 0

Tactic:
simp

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
M N : TopModuleCat R
φ : M ⟶ N
S : ShortComplex (TopModuleCat R)
D₁ : S.LeftHomologyData :=
  { K := ker S.g, H := coker ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)), i := kerι S.g,
    π := cokerπ ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)), wi := ⋯, hi := isLimitKer S.g, wπ := ⋯,
    hπ := isColimitCoker ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)) }
⊢ S.f ≫ cokerπ S.f = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.WithOne.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝¹ : Mul α
inst✝ : MulOneClass β
f : α →ₙ* β
x y : WithOne α
⊢ recOneCoe 1 (⇑f) (1 * y) = recOneCoe 1 (⇑f) 1 * recOneCoe 1 (⇑f) y

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.WithOne.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝¹ : Mul α
inst✝ : MulOneClass β
f : α →ₙ* β
x✝ y : WithOne α
x : α
⊢ recOneCoe 1 (⇑f) (↑x * 1) = recOneCoe 1 ⇑f ↑x * recOneCoe 1 (⇑f) 1

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.Semigrp.Basic

Goal state before:
pp: M : MagmaCat
x : ↑M
⊢ (ConcreteCategory.hom (𝟙 M)) x = x

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.Semigrp.Basic

Goal state before:
pp: M N T : MagmaCat
f : M ⟶ N
g : N ⟶ T
x : ↑M
⊢ (ConcreteCategory.hom (f ≫ g)) x = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) x)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.Semigrp.Basic

Goal state before:
pp: M N : MagmaCat
e : M ≅ N
x : ↑M
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) x) = x

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.Semigrp.Basic

Goal state before:
pp: M N : MagmaCat
e : M ≅ N
s : ↑N
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) s) = s

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.Semigrp.Basic

Goal state before:
pp: X : Semigrp
x : ↑X
⊢ (ConcreteCategory.hom (𝟙 X)) x = x

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.Semigrp.Basic

Goal state before:
pp: X Y T : Semigrp
f : X ⟶ Y
g : Y ⟶ T
x : ↑X
⊢ (ConcreteCategory.hom (f ≫ g)) x = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) x)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.Semigrp.Basic

Goal state before:
pp: X Y : Semigrp
e : X ≅ Y
x : ↑X
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) x) = x

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.Semigrp.Basic

Goal state before:
pp: X Y : Semigrp
e : X ≅ Y
s : ↑Y
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) s) = s

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.Semigrp.Basic

Goal state before:
pp: X✝ Y✝ : Type u
X Y : MagmaCat
i : X ≅ Y
x✝ : ↑X
⊢ ((MagmaCat.Hom.hom i.inv).comp (MagmaCat.Hom.hom i.hom)) x✝ = (MulHom.id ↑X) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.Semigrp.Basic

Goal state before:
pp: X✝ Y✝ : Type u
X Y : MagmaCat
i : X ≅ Y
x✝ : ↑Y
⊢ ((MagmaCat.Hom.hom i.hom).comp (MagmaCat.Hom.hom i.inv)) x✝ = (MulHom.id ↑Y) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.Semigrp.Basic

Goal state before:
pp: X✝ Y✝ : Type u
X Y : Semigrp
i : X ≅ Y
x✝ : ↑X
⊢ ((Semigrp.Hom.hom i.inv).comp (Semigrp.Hom.hom i.hom)) x✝ = (MulHom.id ↑X) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.Semigrp.Basic

Goal state before:
pp: X✝ Y✝ : Type u
X Y : Semigrp
i : X ≅ Y
x✝ : ↑Y
⊢ ((Semigrp.Hom.hom i.hom).comp (Semigrp.Hom.hom i.inv)) x✝ = (MulHom.id ↑Y) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Adjunctions

Goal state before:
pp: case none
X'✝ X✝ : Semigrp
Y✝ : MonCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget₂ MonCat Semigrp).obj Y✝
⊢ (Hom.hom ((ConcreteCategory.homEquiv.trans (WithOne.lift.symm.trans ConcreteCategory.homEquiv.symm)).symm (f✝ ≫ g✝)))
      none =
    (Hom.hom
        (adjoinOne.map f✝ ≫
          (ConcreteCategory.homEquiv.trans (WithOne.lift.symm.trans ConcreteCategory.homEquiv.symm)).symm g✝))
      none

Tactic:
simp

Goal state after:
case none
X'✝ X✝ : Semigrp
Y✝ : MonCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget₂ MonCat Semigrp).obj Y✝
⊢ (Hom.hom ((ConcreteCategory.homEquiv.trans (WithOne.lift.symm.trans ConcreteCategory.homEquiv.symm)).symm (f✝ ≫ g✝)))
      none =
    (Hom.hom
        (ofHom (WithOne.mapMulHom (Semigrp.Hom.hom f✝)) ≫
          (ConcreteCategory.homEquiv.trans (WithOne.lift.symm.trans ConcreteCategory.homEquiv.symm)).symm g✝))
      none
Module: Mathlib.Algebra.Category.MonCat.Adjunctions

Goal state before:
pp: case some
X'✝ X✝ : Semigrp
Y✝ : MonCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget₂ MonCat Semigrp).obj Y✝
val✝ : ↑X'✝
⊢ (Hom.hom ((ConcreteCategory.homEquiv.trans (WithOne.lift.symm.trans ConcreteCategory.homEquiv.symm)).symm (f✝ ≫ g✝)))
      (some val✝) =
    (Hom.hom
        (adjoinOne.map f✝ ≫
          (ConcreteCategory.homEquiv.trans (WithOne.lift.symm.trans ConcreteCategory.homEquiv.symm)).symm g✝))
      (some val✝)

Tactic:
simp

Goal state after:
case some
X'✝ X✝ : Semigrp
Y✝ : MonCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget₂ MonCat Semigrp).obj Y✝
val✝ : ↑X'✝
⊢ (Hom.hom ((ConcreteCategory.homEquiv.trans (WithOne.lift.symm.trans ConcreteCategory.homEquiv.symm)).symm (f✝ ≫ g✝)))
      (some val✝) =
    (Hom.hom
        (ofHom (WithOne.mapMulHom (Semigrp.Hom.hom f✝)) ≫
          (ConcreteCategory.homEquiv.trans (WithOne.lift.symm.trans ConcreteCategory.homEquiv.symm)).symm g✝))
      (some val✝)
Module: Mathlib.Algebra.Category.MonCat.Colimits

Goal state before:
pp: case a.map
J : Type v
inst✝ : Category.{u, v} J
F : J ⥤ MonCat
s : Cocone F
x✝ y : Prequotient F
j j' : J
f : j ⟶ j'
x : ↑(F.obj j)
⊢ descFunLift F s (Prequotient.of j' ((ConcreteCategory.hom (F.map f)) x)) = descFunLift F s (Prequotient.of j x)

Tactic:
exact s.w_apply f x

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

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₁
inst✝³¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝³⁰ : RingHomInvPair σ₂₁ σ₁₂
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
inst✝²⁹ : RingHomInvPair σ₂₃ σ₃₂
inst✝²⁸ : RingHomInvPair σ₃₂ σ₂₃
σ₁₃ : R₁ →+* R₃
σ₃₁ : R₃ →+* R₁
inst✝²⁷ : RingHomInvPair σ₁₃ σ₃₁
inst✝²⁶ : RingHomInvPair σ₃₁ σ₁₃
inst✝²⁵ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝²⁴ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
M₁ : Type u_4
inst✝²³ : TopologicalSpace M₁
inst✝²² : AddCommMonoid M₁
M₂ : Type u_5
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₃
R₄ : Type u_8
inst✝¹² : Semiring R₄
inst✝¹¹ : Module R₄ M₄
σ₃₄ : R₃ →+* R₄
σ₄₃ : R₄ →+* R₃
inst✝¹⁰ : RingHomInvPair σ₃₄ σ₄₃
inst✝⁹ : RingHomInvPair σ₄₃ σ₃₄
σ₂₄ : R₂ →+* R₄
σ₁₄ : R₁ →+* R₄
inst✝⁸ : RingHomCompTriple σ₂₁ σ₁₄ σ₂₄
inst✝⁷ : RingHomCompTriple σ₂₄ σ₄₃ σ₂₃
inst✝⁶ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝⁵ : SMulCommClass R₃ R₃ M₃
inst✝⁴ : SMulCommClass R₄ R₄ M₄
inst✝³ : ContinuousAdd M₃
inst✝² : ContinuousConstSMul R₃ M₃
inst✝¹ : ContinuousAdd M₄
inst✝ : ContinuousConstSMul R₄ M₄
e₁₂ : M₁ ≃SL[σ₁₂] M₂
e₄₃ : M₄ ≃SL[σ₄₃] M₃
⊢ ∀ (x y : M₁ →SL[σ₁₄] M₄),
    (e₁₂.arrowCongrEquiv e₄₃).toFun (x + y) = (e₁₂.arrowCongrEquiv e₄₃).toFun x + (e₁₂.arrowCongrEquiv e₄₃).toFun y

Tactic:
simp

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

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₁
inst✝³¹ : RingHomInvPair σ₁₂ σ₂₁
inst✝³⁰ : RingHomInvPair σ₂₁ σ₁₂
σ₂₃ : R₂ →+* R₃
σ₃₂ : R₃ →+* R₂
inst✝²⁹ : RingHomInvPair σ₂₃ σ₃₂
inst✝²⁸ : RingHomInvPair σ₃₂ σ₂₃
σ₁₃ : R₁ →+* R₃
σ₃₁ : R₃ →+* R₁
inst✝²⁷ : RingHomInvPair σ₁₃ σ₃₁
inst✝²⁶ : RingHomInvPair σ₃₁ σ₁₃
inst✝²⁵ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝²⁴ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
M₁ : Type u_4
inst✝²³ : TopologicalSpace M₁
inst✝²² : AddCommMonoid M₁
M₂ : Type u_5
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₃
R₄ : Type u_8
inst✝¹² : Semiring R₄
inst✝¹¹ : Module R₄ M₄
σ₃₄ : R₃ →+* R₄
σ₄₃ : R₄ →+* R₃
inst✝¹⁰ : RingHomInvPair σ₃₄ σ₄₃
inst✝⁹ : RingHomInvPair σ₄₃ σ₃₄
σ₂₄ : R₂ →+* R₄
σ₁₄ : R₁ →+* R₄
inst✝⁸ : RingHomCompTriple σ₂₁ σ₁₄ σ₂₄
inst✝⁷ : RingHomCompTriple σ₂₄ σ₄₃ σ₂₃
inst✝⁶ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝⁵ : SMulCommClass R₃ R₃ M₃
inst✝⁴ : SMulCommClass R₄ R₄ M₄
inst✝³ : ContinuousAdd M₃
inst✝² : ContinuousConstSMul R₃ M₃
inst✝¹ : ContinuousAdd M₄
inst✝ : ContinuousConstSMul R₄ M₄
e₁₂ : M₁ ≃SL[σ₁₂] M₂
e₄₃ : M₄ ≃SL[σ₄₃] M₃
⊢ ∀ (m : R₄) (x : M₁ →SL[σ₁₄] M₄), (e₁₂.arrowCongrEquiv e₄₃).toFun (m • x) = σ₄₃ m • (e₁₂.arrowCongrEquiv e₄₃).toFun x

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : TopologicalSpace M
f : (M →L[R] M)ˣ
⊢ ∀ (x y : M), ↑f (x + y) = ↑f x + ↑f y

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : TopologicalSpace M
f : (M →L[R] M)ˣ
⊢ ∀ (m : R) (x : M), ↑f (m • x) = (RingHom.id R) m • ↑f x

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : TopologicalSpace M
f : (M →L[R] M)ˣ
x : M
⊢ 1 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
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : TopologicalSpace M
f : M ≃L[R] M
x✝ : M
⊢ (↑f * ↑f.symm) x✝ = 1 x✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : TopologicalSpace M
f : M ≃L[R] M
x✝ : M
⊢ (↑f.symm * ↑f) x✝ = 1 x✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : ContinuousMul R
u : Rˣ
x : R
⊢ (ContinuousLinearMap.smulRight 1 ↑u⁻¹) ((ContinuousLinearMap.smulRight 1 ↑u) x) = x

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : ContinuousMul R
u : Rˣ
x : R
⊢ (ContinuousLinearMap.smulRight 1 ↑u) ((ContinuousLinearMap.smulRight 1 ↑u⁻¹) x) = x

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : ContinuousMul R
u : Rˣ
⊢ ↑((fun e ↦ { val := e 1, inv := e.symm 1, val_inv := ⋯, inv_val := ⋯ })
        ((fun u ↦ equivOfInverse (ContinuousLinearMap.smulRight 1 ↑u) (ContinuousLinearMap.smulRight 1 ↑u⁻¹) ⋯ ⋯) u)) =
    ↑u

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
inst✝¹ : TopologicalSpace R
inst✝ : ContinuousMul R
e : R ≃L[R] R
⊢ ((fun u ↦ equivOfInverse (ContinuousLinearMap.smulRight 1 ↑u) (ContinuousLinearMap.smulRight 1 ↑u⁻¹) ⋯ ⋯)
        ((fun e ↦ { val := e 1, inv := e.symm 1, val_inv := ⋯, inv_val := ⋯ }) e))
      1 =
    e 1

Tactic:
simp

Goal state after: