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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
M₁ : Type u_5
M₂ : Type u_6
inst✝²⁰ : Semiring R
inst✝¹⁹ : TopologicalSpace M
inst✝¹⁸ : TopologicalSpace N
inst✝¹⁷ : TopologicalSpace M₁
inst✝¹⁶ : TopologicalSpace M₂
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : Module R M
inst✝¹³ : ContinuousAdd M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : Module R N
inst✝¹⁰ : ContinuousAdd N
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : Module R M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R M₂
inst✝⁵ : ContinuousAdd M₁
inst✝⁴ : ContinuousAdd M₂
inst✝³ : Semiring S
inst✝² : Module S M
inst✝¹ : ContinuousConstSMul S M
inst✝ : SMulCommClass R S M
f : (M₁ →L[R] M) × (M₂ →L[R] M)
⊢ (fun f ↦ (f ∘SL inl R M₁ M₂, f ∘SL inr R M₁ M₂)) ((fun f ↦ f.1.coprod f.2) f) = f

Tactic:
by simp

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

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
p : Submodule R M
x : ↥p
⊢ p.subtypeL x = ↑x

Tactic:
by simp

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

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
inst✝⁸ : Semiring R₁
inst✝⁷ : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
M₂ : Type u_5
inst✝⁶ : TopologicalSpace M₁
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : Module R₁ M₁
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₂ M₂
inst✝ : RingHomSurjective σ₁₂
f : M₁ →SL[σ₁₂] M₂
⊢ ↑f.rangeRestrict = (↑f).rangeRestrict

Tactic:
by simp

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

Goal state before:
pp: R : Type u_6
A : Type u_7
B : Type u_8
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Semiring B
inst✝⁴ : TopologicalSpace R
inst✝³ : TopologicalSpace A
inst✝² : IsModuleTopology R A
inst✝¹ : TopologicalSpace B
inst✝ : IsTopologicalSemiring B
φ : A →+* B
hφ : Continuous ⇑(φ.comp (algebraMap R A))
inst : Module R B := Module.compHom B (φ.comp (algebraMap R A))
φ' : A →ₗ[R] B := { toAddHom := ↑φ, map_smul' := ⋯ }
this : ContinuousSMul R B
⊢ Continuous ⇑φ

Tactic:
exact continuous_of_linearMap φ'

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

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
σ₁₂ : R₁ →+* 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₂
f : M₁ →SL[σ₁₂] M₂
⊢ Set.range ⇑↑f = Set.range ⇑f

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

Tactic:
suffices ∃ h, h ≫ G.map f = Projective.π (G.obj Y) from epi_of_epi_fac this.choose_spec

Goal state after:
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
⊢ ∃ h, h ≫ G.map f = Projective.π (G.obj Y)
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)) ≫
      G.map f =
    Projective.π (G.obj Y)

Tactic:
rw [Category.assoc, ← Functor.map_comp]

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

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

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

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

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

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

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

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

Goal state before:
pp: case a
J : Type v
inst✝ : Category.{u, v} J
F : J ⥤ MonCat
s : Cocone F
⊢ ∀ (a b : Prequotient F), (colimitSetoid F) a b → descFunLift F s a = descFunLift F s b

Tactic:
intro x y r
    induction r with
    | refl x => rfl
    | symm x y _ h => exact h.symm
    | trans x y z _ _ h₁ h₂ => exact h₁.trans h₂
    | map j j' f x => exact s.w_apply f x
    | mul j x y => exact map_mul (s.ι.app j).hom x y
    | one j => exact map_one (s.ι.app j).hom
    | mul_1 x x' y _ h => exact congr_arg (· * _) h
    | mul_2 x y y' _ h => exact congr_arg (_ * ·) h
    | mul_assoc x y z => exact mul_assoc _ _ _
    | one_mul x => exact one_mul _
    | mul_one x => exact mul_one _

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

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✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : ContinuousNeg M
x : M
⊢ (neg R) x = -x

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

Goal state after:
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
j j' : J
φ : j ⟶ j'
i : J := IsCofiltered.min i₀ j
α : i ⟶ i₀ := minToLeft i₀ j
β : i ⟶ j := minToRight i₀ j
⊢ h.coneπApp j' = h.coneπApp j ≫ F.map φ

Tactic:
h.coneπApp_eq j _ α β,

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.IsEventuallyConstantTo i₀
inst✝ : IsCofiltered J
j j' : J
φ : j ⟶ j'
i : J := IsCofiltered.min i₀ j
α : i ⟶ i₀ := minToLeft i₀ j
β : i ⟶ j := minToRight i₀ j
⊢ h.coneπApp j' = ((h.isoMap α ⋯).inv ≫ F.map β) ≫ F.map φ
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
c : Cone F
inst✝ : IsIso (c.π.app i₀)
j : J
i : J := IsCofiltered.min i₀ j
α : i ⟶ i₀ := minToLeft i₀ j
β : i ⟶ j := minToRight i₀ j
⊢ (c.π.app i ≫ F.map α) ≫ h.coneπApp j = c.π.app i ≫ F.map β

Tactic:
h.coneπApp_eq j _ α β,

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.IsEventuallyConstantTo i₀
inst✝¹ : IsCofiltered J
c : Cone F
inst✝ : IsIso (c.π.app i₀)
j : J
i : J := IsCofiltered.min i₀ j
α : i ⟶ i₀ := minToLeft i₀ j
β : i ⟶ j := minToRight i₀ j
⊢ (c.π.app i ≫ F.map α) ≫ (h.isoMap α ⋯).inv ≫ F.map β = c.π.app i ≫ F.map β
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Basic

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

Tactic:
exact congr($(H j).hom y)

Goal state after:
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:
rw [h.coconeιApp_eq i₀ i₀ (𝟙 _) (𝟙 _), h.isoMap_hom_inv_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) → M ⟶ (X i).toModuleCat
J : Type u_2
inst✝ : Category.{v_1, u_2} J
F : J ⥤ TopModuleCat R
c : Cone (F ⋙ forget₂ (TopModuleCat R) (ModuleCat R))
hc : IsLimit c
s : Cone F
m : s.pt ⟶ (ofCone c).pt
H : ∀ (j : J), m ≫ (ofCone c).π.app j = s.π.app j
x : ↑s.pt.toModuleCat
j : J
y : ↑((forget₂ (TopModuleCat R) (ModuleCat R)).mapCone s).pt
⊢ (ModuleCat.Hom.hom ((forget₂ (TopModuleCat R) (ModuleCat R)).map m ≫ c.π.app j)) y =
    (ModuleCat.Hom.hom (((forget₂ (TopModuleCat R) (ModuleCat R)).mapCone s).π.app j)) y

Tactic:
exact congr($(H j).hom y)

Goal state after:
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✝ : C ⥤ D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : IsAccessible.{w, v₁, v₂, u₁, u₂} F
inst✝ : IsAccessible.{w, v₂, v₃, u₂, u₃} G
κF : Cardinal.{w}
w✝¹ : Fact κF.IsRegular
h✝¹ : F.IsCardinalAccessible κF
κG : Cardinal.{w}
w✝ : Fact κG.IsRegular
h✝ : G.IsCardinalAccessible κG
this : Fact (max κF κG).IsRegular
⊢ κF ≤ max κF κG

Tactic:
by simp

Goal state after:
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✝ : C ⥤ D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
F : C ⥤ D
G : D ⥤ E
inst✝¹ : IsAccessible.{w, v₁, v₂, u₁, u₂} F
inst✝ : IsAccessible.{w, v₂, v₃, u₂, u₃} G
κF : Cardinal.{w}
w✝¹ : Fact κF.IsRegular
h✝¹ : F.IsCardinalAccessible κF
κG : Cardinal.{w}
w✝ : Fact κG.IsRegular
h✝ : G.IsCardinalAccessible κG
this✝ : Fact (max κF κG).IsRegular
this : F.IsCardinalAccessible (max κF κG)
⊢ κG ≤ max κF κG

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

Goal state before:
pp: J : Type u
inst✝² : Category.{v, u} J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
j₀ : J
A : Type w
x✝ : SmallCategory A
F : A ⥤ Under j₀
hA : HasCardinalLT (Arrow A) κ
⊢ Cocone F

Tactic:
by
    have := isFiltered_of_isCardinalFiltered J κ
    let c := cocone (F ⋙ Under.forget j₀) hA
    let x (a : A) : j₀ ⟶ IsFiltered.max j₀ c.pt := (F.obj a).hom ≫ c.ι.app a ≫
      IsFiltered.rightToMax j₀ c.pt
    have hκ' : HasCardinalLT A κ := hasCardinalLT_of_hasCardinalLT_arrow hA
    exact
      { pt := Under.mk (toCoeq x hκ')
        ι :=
          { app a := Under.homMk (c.ι.app a ≫ IsFiltered.rightToMax j₀ c.pt ≫ coeqHom x hκ')
              (by simpa [x] using coeq_condition x hκ' a)
            naturality a b f := by
              ext
              have := c.w f
              dsimp at this ⊢
              simp only [reassoc_of% this, Category.comp_id] } }

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

Goal state before:
pp: R A B C : CommRingCat
inst✝ : TopologicalSpace ↑R
f : A ≅ B
x✝ : B ⟶ R
⊢ (fun φ ↦ f.inv ≫ φ) ((fun φ ↦ f.hom ≫ φ) x✝) = x✝

Tactic:
by simp

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

Goal state before:
pp: R A B C : CommRingCat
inst✝ : TopologicalSpace ↑R
f : A ≅ B
x✝ : A ⟶ R
⊢ (fun φ ↦ f.hom ≫ φ) ((fun φ ↦ f.inv ≫ φ) x✝) = x✝

Tactic:
by simp

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.IsCardinalFiltered

Goal state before:
pp: J₁ : Type u
inst✝⁴ : Category.{v, u} J₁
J₂ : Type u'
inst✝³ : Category.{v', u'} J₂
F : J₁ ⥤ J₂
inst✝² : F.Final
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J₁ κ
this : IsFiltered J₁
h₁ : ∀ (d : J₂), ∃ c, Nonempty (d ⟶ F.obj c)
h₂ : ∀ {d : J₂} {c : J₁} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t
ι : Type w
j k : J₂
f : ι → (j ⟶ k)
hι : HasCardinalLT ι κ
h : IsEmpty ι
j' : J₁
a : j ⟶ F.obj j'
k' : J₁
b : k ⟶ F.obj k'
⊢ ∀ (i : ι), f i ≫ b ≫ F.map (IsFiltered.rightToMax j' k') = a ≫ F.map (IsFiltered.leftToMax j' k')

Tactic:
by simp

Goal state after: