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

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

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

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
⊢ kerι φ ≫ φ = 0

Tactic:
by

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
⊢ lcomp W (x✝¹ + x✝) = lcomp W x✝¹ + lcomp W x✝

Tactic:
by

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 : KernelFork φ
m : ↑s.pt.toModuleCat
⊢ (Hom.hom (Fork.ι s)) m ∈ (↑(Hom.hom φ)).ker

Tactic:
by

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
⊢ lcomp W (x✝¹ • x✝) = (RingHom.id R) x✝¹ • lcomp W x✝

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝¹⁸ : Semiring R
inst✝¹⁷ : Semiring S
inst✝¹⁶ : Semiring T
inst✝¹⁵ : Module R S
inst✝¹⁴ : AddCommMonoid M₂
inst✝¹³ : Module R M₂
inst✝¹² : Module S M₂
inst✝¹¹ : IsScalarTower R S M₂
inst✝¹⁰ : TopologicalSpace S
inst✝⁹ : TopologicalSpace M₂
inst✝⁸ : ContinuousSMul S M₂
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : ContinuousAdd M₂
inst✝³ : Module T M₂
inst✝² : ContinuousConstSMul T M₂
inst✝¹ : SMulCommClass R T M₂
inst✝ : SMulCommClass S T M₂
c : M →L[R] S
x y : M₂
⊢ c.smulRight (x + y) = c.smulRight x + c.smulRight y

Tactic:
by

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 : KernelFork φ
m : s.pt ⟶ (KernelFork.ofι (kerι φ) ⋯).pt
h : m ≫ Fork.ι (KernelFork.ofι (kerι φ) ⋯) = Fork.ι s
⊢ m = ofHom ((Hom.hom (Fork.ι s)).codRestrict (↑(Hom.hom φ)).ker ⋯)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
M : Type u_4
M₂ : Type u_5
inst✝¹⁸ : Semiring R
inst✝¹⁷ : Semiring S
inst✝¹⁶ : Semiring T
inst✝¹⁵ : Module R S
inst✝¹⁴ : AddCommMonoid M₂
inst✝¹³ : Module R M₂
inst✝¹² : Module S M₂
inst✝¹¹ : IsScalarTower R S M₂
inst✝¹⁰ : TopologicalSpace S
inst✝⁹ : TopologicalSpace M₂
inst✝⁸ : ContinuousSMul S M₂
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : ContinuousAdd M₂
inst✝³ : Module T M₂
inst✝² : ContinuousConstSMul T M₂
inst✝¹ : SMulCommClass R T M₂
inst✝ : SMulCommClass S T M₂
c : M →L[R] S
a : T
x : M₂
⊢ c.smulRight (a • x) = (RingHom.id T) a • c.smulRight x

Tactic:
by

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
⊢ Continuous (↑(Hom.hom φ)).range.mkQ.toFun

Tactic:
by

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
⊢ φ ≫ cokerπ φ = 0

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : EnoughInjectives D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.PreservesInjectiveObjects
X Y : C
f : X ⟶ Y
x✝ : Mono f
⊢ F.map f ≫
      F.map (Injective.factorThru (adj.unit.app X ≫ G.map (Injective.ι (F.obj X))) f) ≫
        adj.counit.app (Injective.under (F.obj X)) =
    Injective.ι (F.obj X)

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : EnoughInjectives D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.PreservesInjectiveObjects
X Y : C
f : X ⟶ Y
x✝ : Mono f
⊢ Mono (F.map f)

Tactic:
by

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
⊢ Epi (G.map f)

Tactic:
by

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 : CokernelCofork φ
m : (CokernelCofork.ofπ (cokerπ φ) ⋯).pt ⟶ s.pt
h : Cofork.π (CokernelCofork.ofπ (cokerπ φ) ⋯) ≫ m = Cofork.π s
⊢ m =
    ofHom
      (let __LinearMap := (↑(Hom.hom φ)).range.liftQ ↑(Hom.hom (Cofork.π s)) ⋯;
      { toLinearMap := __LinearMap, cont := ⋯ })

Tactic:
by

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

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

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 ⋯)) }
D₂ : S.RightHomologyData :=
  { Q := coker S.f, H := ker ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)), p := cokerπ S.f,
    ι := kerι ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)), wp := ⋯, hp := isColimitCoker S.f, wι := ⋯,
    hι := isLimitKer ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)) }
F : D₁.H ⟶ D₂.H := ShortComplex.leftRightHomologyComparison' D₁ D₂
⊢ Function.Bijective ⇑(ConcreteCategory.hom F)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
⊢ Limits.PreservesLimitsOfSize.{v, v, v, max v v', max u (v + 1), (max v v') + 1}
    (uliftFunctor.{v', v, u} R ⋙ forget (ModuleCat R))

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
h : S.Exact
⊢ (S.map (uliftFunctor.{u_1, v, u} R)).Exact

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
⊢ Limits.PreservesFiniteColimits (uliftFunctor.{v', v, u} R)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : Small.{v, u} R
M : ModuleCat R
proj : Projective M
⊢ Projective ((uliftFunctor.{v', v, u} R).obj M)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.PEmptyInstances

Goal state before:
pp: x x✝ : PEmpty
⊢ PEmpty

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.PEmptyInstances

Goal state before:
pp: x y z : PEmpty
⊢ x * y * z = x * (y * z)

Tactic:
by

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 ⋯)) }
D₂ : S.RightHomologyData :=
  { Q := coker S.f, H := ker ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)), p := cokerπ S.f,
    ι := kerι ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)), wp := ⋯, hp := isColimitCoker S.f, wι := ⋯,
    hι := isLimitKer ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)) }
F : D₁.H ⟶ D₂.H := ShortComplex.leftRightHomologyComparison' D₁ D₂
hF : Function.Bijective ⇑(ConcreteCategory.hom F)
this :
  ∀ (x y : (fun X ↦ ↑X.toModuleCat) S.X₂),
    (ConcreteCategory.hom S.g) y = 0 →
      (ConcreteCategory.hom D₂.p) y = (ConcreteCategory.hom D₂.p) x → (ConcreteCategory.hom S.g) x = 0
⊢ ⇑(ConcreteCategory.hom D₂.p) ⁻¹' ⇑(ConcreteCategory.hom D₂.p) '' Set.range ⇑(ConcreteCategory.hom D₁.i) ⊆
    Set.range ⇑(ConcreteCategory.hom D₁.i)

Tactic:
by

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 ⋯)) }
D₂ : S.RightHomologyData :=
  { Q := coker S.f, H := ker ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)), p := cokerπ S.f,
    ι := kerι ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)), wp := ⋯, hp := isColimitCoker S.f, wι := ⋯,
    hι := isLimitKer ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)) }
F : D₁.H ⟶ D₂.H := ShortComplex.leftRightHomologyComparison' D₁ D₂
hF : Function.Bijective ⇑(ConcreteCategory.hom F)
⊢ Topology.IsEmbedding ⇑(ConcreteCategory.hom F)

Tactic:
by

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
⊢ CategoryWithHomology (TopModuleCat R)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝ : InvolutiveInv α
a : WithOne α
⊢ Option.map (Inv.inv ∘ Inv.inv) a = a

Tactic:
by

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

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

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Mul α
inst✝ : MulOneClass β
f : WithOne α →* β
hf : Function.Injective ⇑f
x✝¹ x✝ : α
⊢ (lift.symm f) x✝¹ = (lift.symm f) x✝ → x✝¹ = x✝

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Mul α
inst✝ : Mul β
f : α →ₙ* β
hf : Function.Injective ⇑f
a₁ a₂ : α
H : (mapMulHom f) ↑a₁ = (mapMulHom f) ↑a₂
⊢ ↑a₁ = ↑a₂

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Mul α
inst✝ : Mul β
f g : α →ₙ* β
h : mapMulHom f = mapMulHom g
x : α
⊢ ↑(f x) = ↑(g x)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : Mul α
inst✝¹ : Mul β
inst✝ : Mul γ
f : α →ₙ* β
g : β →ₙ* γ
x : WithOne α
⊢ (mapMulHom g) ((mapMulHom f) x) = (mapMulHom (g.comp f)) x

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : Mul α
inst✝¹ : Mul β
inst✝ : Mul γ
e : α ≃* β
x✝ : WithOne α
⊢ (mapMulHom e.symm.toMulHom) ((mapMulHom e.toMulHom) x✝) = x✝

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : Mul α
inst✝¹ : Mul β
inst✝ : Mul γ
e : α ≃* β
x✝ : WithOne β
⊢ (mapMulHom e.toMulHom) ((mapMulHom e.symm.toMulHom) x✝) = x✝

Tactic:
by

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

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

Tactic:
by

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

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

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

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

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

Tactic:
by

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

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

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

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: X✝ Y✝ : Type u
X Y : MagmaCat
f : X ⟶ Y
x✝ : IsIso ((forget MagmaCat).map f)
⊢ IsIso f

Tactic:
by

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

Goal state before:
pp: X✝ Y✝ : Type u
X Y : Semigrp
f : X ⟶ Y
x✝ : IsIso ((forget Semigrp).map f)
⊢ IsIso f

Tactic:
by

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

Goal state before:
pp: J : Type v
inst✝ : Category.{u, v} J
F : J ⥤ MonCat
j j' : J
f : j ⟶ j'
⊢ F.map f ≫ coconeMorphism F j' = coconeMorphism F j

Tactic:
by

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

Goal state before:
pp: J : Type v
inst✝ : Category.{u, v} J
F : J ⥤ MonCat
j j' : J
f : j ⟶ j'
x : ↑(F.obj j)
⊢ (ConcreteCategory.hom (coconeMorphism F j')) ((ConcreteCategory.hom (F.map f)) x) =
    (ConcreteCategory.hom (coconeMorphism F j)) x

Tactic:
by

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

Goal state before:
pp: J : Type v
inst✝ : Category.{u, v} J
F : J ⥤ MonCat
s : Cocone F
⊢ ColimitType F → ↑s.pt

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ {X' X : Semigrp} {Y : MonCat} (f : X' ⟶ X) (g : X ⟶ (forget₂ MonCat Semigrp).obj Y),
    (ConcreteCategory.homEquiv.trans (WithOne.lift.symm.trans ConcreteCategory.homEquiv.symm)).symm (f ≫ g) =
      adjoinOne.map f ≫
        (ConcreteCategory.homEquiv.trans (WithOne.lift.symm.trans ConcreteCategory.homEquiv.symm)).symm g

Tactic:
by

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

Goal state before:
pp: X'✝ X✝ : Type u
Y✝ : MonCat
x✝² : X'✝ ⟶ X✝
x✝¹ : X✝ ⟶ (forget MonCat).obj Y✝
x✝ : X'✝
⊢ (ConcreteCategory.hom
        ((ConcreteCategory.homEquiv.trans (FreeMonoid.lift.symm.trans TypeCat.homEquiv.symm)).symm (x✝² ≫ x✝¹)))
      (FreeMonoid.of x✝) =
    (ConcreteCategory.hom
        (free.map x✝² ≫ (ConcreteCategory.homEquiv.trans (FreeMonoid.lift.symm.trans TypeCat.homEquiv.symm)).symm x✝¹))
      (FreeMonoid.of x✝)

Tactic:
by

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

Goal state before:
pp: J : Type v
inst✝ : Category.{u, v} J
F : J ⥤ MonCat
s : Cocone F
x y : ColimitType F
⊢ descFun F s (x * y) = descFun F s x * descFun F s y

Tactic:
by

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

Goal state before:
pp: M N : AddCommMonCat
f : M ⟶ N
⊢ (forget AddCommMonCat ⋙ free).map f ≫ ofHom (Finsupp.liftAddHom ⇑(multiplesHom ↑N)) =
    ofHom (Finsupp.liftAddHom ⇑(multiplesHom ↑M)) ≫ (𝟭 AddCommMonCat).map f

Tactic:
by

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

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

Goal state after:
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✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M₂
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
ι : Type u_4
φ : ι → Type u_5
inst✝³ : (i : ι) → TopologicalSpace (φ i)
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
I J : Set ι
inst✝ : DecidablePred fun i ↦ i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
i : ι
⊢ Continuous[Pi.topologicalSpace, inst✝³ i] fun a ↦
    (LinearMap.pi fun i ↦ if h : i ∈ I then LinearMap.proj ⟨i, h⟩ else 0) a i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Epi

Goal state before:
pp: R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
H : Epi (ofHom (algebraMap R S))
⊢ ofHom (algebraMap R S) ≫ ofHom Algebra.TensorProduct.includeLeftRingHom =
    ofHom (algebraMap R S) ≫ ofHom Algebra.TensorProduct.includeRight.toRingHom

Tactic:
by

Goal state after: