mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.ModuleCat.Stalk

Goal state before:
pp: X : TopCat
R : TopCat.Presheaf CommRingCat X
M : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
x : ↑X
U : Opens ↑X
hx : x ∈ U
r : ↑(R.obj (op U))
m : ↑(M.obj (op U))
i : (OpenNhds x)ᵒᵖ
⊢ Module ↑(R.obj (op ((OpenNhds.inclusion x).obj (unop i)))) ↑(M.obj (op ((OpenNhds.inclusion x).obj (unop i))))

Tactic:
;

Goal state after:
X : TopCat
R : TopCat.Presheaf CommRingCat X
M : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
x : ↑X
U : Opens ↑X
hx : x ∈ U
r : ↑(R.obj (op U))
m : ↑(M.obj (op U))
i : (OpenNhds x)ᵒᵖ
⊢ Module ↑(R.obj (op ((OpenNhds.inclusion x).obj (unop i)))) ↑(M.obj (op ((OpenNhds.inclusion x).obj (unop i))))
Module: Mathlib.Topology.Algebra.Module.ModuleTopology

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : TopologicalSpace R
inst✝⁹ : CommSemiring R
B : Type u_2
inst✝⁸ : AddCommMonoid B
inst✝⁷ : Module R B
inst✝⁶ : TopologicalSpace B
inst✝⁵ : IsModuleTopology R B
C : Type u_3
inst✝⁴ : AddCommMonoid C
inst✝³ : Module R C
inst✝² : TopologicalSpace C
inst✝¹ : IsModuleTopology R C
ι : Type u_4
inst✝ : Finite ι
bil : (ι → R) →ₗ[R] B →ₗ[R] C
val✝ : Fintype ι
f : ι → R
b : B
x : ι
x✝ : x ∈ Finset.univ
⊢ (bil ⇑(Finsupp.single x (f x))) b = f x • (bil ⇑(Finsupp.single x 1)) b

Tactic:
← Finsupp.smul_single_one

Goal state after:
R : Type u_1
inst✝¹⁰ : TopologicalSpace R
inst✝⁹ : CommSemiring R
B : Type u_2
inst✝⁸ : AddCommMonoid B
inst✝⁷ : Module R B
inst✝⁶ : TopologicalSpace B
inst✝⁵ : IsModuleTopology R B
C : Type u_3
inst✝⁴ : AddCommMonoid C
inst✝³ : Module R C
inst✝² : TopologicalSpace C
inst✝¹ : IsModuleTopology R C
ι : Type u_4
inst✝ : Finite ι
bil : (ι → R) →ₗ[R] B →ₗ[R] C
val✝ : Fintype ι
f : ι → R
b : B
x : ι
x✝ : x ∈ Finset.univ
⊢ (bil ⇑(f x • Finsupp.single x 1)) b = f x • (bil ⇑(Finsupp.single x 1)) b
Module: Mathlib.Topology.Algebra.Module.ModuleTopology

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : TopologicalSpace R
inst✝⁹ : CommSemiring R
B : Type u_2
inst✝⁸ : AddCommMonoid B
inst✝⁷ : Module R B
inst✝⁶ : TopologicalSpace B
inst✝⁵ : IsModuleTopology R B
C : Type u_3
inst✝⁴ : AddCommMonoid C
inst✝³ : Module R C
inst✝² : TopologicalSpace C
inst✝¹ : IsModuleTopology R C
ι : Type u_4
inst✝ : Finite ι
bil : (ι → R) →ₗ[R] B →ₗ[R] C
val✝ : Fintype ι
f : ι → R
b : B
x : ι
x✝ : x ∈ Finset.univ
⊢ (bil ⇑(Finsupp.single x (f x))) b = f x • (bil ⇑(Finsupp.single x 1)) b

Tactic:
rw [← Finsupp.smul_single_one]

Goal state after:
R : Type u_1
inst✝¹⁰ : TopologicalSpace R
inst✝⁹ : CommSemiring R
B : Type u_2
inst✝⁸ : AddCommMonoid B
inst✝⁷ : Module R B
inst✝⁶ : TopologicalSpace B
inst✝⁵ : IsModuleTopology R B
C : Type u_3
inst✝⁴ : AddCommMonoid C
inst✝³ : Module R C
inst✝² : TopologicalSpace C
inst✝¹ : IsModuleTopology R C
ι : Type u_4
inst✝ : Finite ι
bil : (ι → R) →ₗ[R] B →ₗ[R] C
val✝ : Fintype ι
f : ι → R
b : B
x : ι
x✝ : x ∈ Finset.univ
⊢ (bil ⇑(f x • Finsupp.single x 1)) b = f x • (bil ⇑(Finsupp.single x 1)) b
Module: Mathlib.Topology.Algebra.Module.ModuleTopology

Goal state before:
pp: R : Type u_1
inst✝¹² : TopologicalSpace R
inst✝¹¹ : CommRing R
inst✝¹⁰ : IsTopologicalRing R
A : Type u_2
inst✝⁹ : AddCommGroup A
inst✝⁸ : Module R A
aA : TopologicalSpace A
inst✝⁷ : IsModuleTopology R A
B : Type u_3
inst✝⁶ : AddCommGroup B
inst✝⁵ : Module R B
aB : TopologicalSpace B
inst✝⁴ : IsModuleTopology R B
C : Type u_4
inst✝³ : AddCommGroup C
inst✝² : Module R C
aC : TopologicalSpace C
inst✝¹ : IsModuleTopology R C
inst✝ : Module.Finite R A
bil : A →ₗ[R] B →ₗ[R] C
⊢ Continuous fun ab ↦ (bil ab.1) ab.2

Tactic:
obtain ⟨m, f, hf⟩ := Module.Finite.exists_fin' R A
  -- The induced linear map `φ : Rⁿ × B → A × B` is surjective
  let bil' : (Fin m → R) →ₗ[R] B →ₗ[R] C := bil.comp f
  let φ := f.prodMap (LinearMap.id : B →ₗ[R] B)
  have hφ : Function.Surjective φ := Function.Surjective.prodMap hf fun b ↦ ⟨b, rfl⟩
  -- ... and thus a quotient map, so it suffices to prove that the composite `Rⁿ × B → C` is
  -- continuous.
  rw [Topology.IsQuotientMap.continuous_iff (isQuotientMap_of_surjective hφ)]
  -- But this follows from an earlier result.
  exact continuous_bilinear_of_pi_fintype (Fin m) bil'

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

Goal state before:
pp: R : Type u_1
inst✝¹² : TopologicalSpace R
inst✝¹¹ : CommRing R
inst✝¹⁰ : IsTopologicalRing R
A : Type u_2
inst✝⁹ : AddCommGroup A
inst✝⁸ : Module R A
aA : TopologicalSpace A
inst✝⁷ : IsModuleTopology R A
B : Type u_3
inst✝⁶ : AddCommGroup B
inst✝⁵ : Module R B
aB : TopologicalSpace B
inst✝⁴ : IsModuleTopology R B
C : Type u_4
inst✝³ : AddCommGroup C
inst✝² : Module R C
aC : TopologicalSpace C
inst✝¹ : IsModuleTopology R C
inst✝ : Module.Finite R B
bil : A →ₗ[R] B →ₗ[R] C
x✝ : A × B
⊢ (bil x✝.1) x✝.2 = ((fun ba ↦ (bil.flip ba.1) ba.2) ∘ Prod.swap) x✝

Tactic:
;

Goal state after:
R : Type u_1
inst✝¹² : TopologicalSpace R
inst✝¹¹ : CommRing R
inst✝¹⁰ : IsTopologicalRing R
A : Type u_2
inst✝⁹ : AddCommGroup A
inst✝⁸ : Module R A
aA : TopologicalSpace A
inst✝⁷ : IsModuleTopology R A
B : Type u_3
inst✝⁶ : AddCommGroup B
inst✝⁵ : Module R B
aB : TopologicalSpace B
inst✝⁴ : IsModuleTopology R B
C : Type u_4
inst✝³ : AddCommGroup C
inst✝² : Module R C
aC : TopologicalSpace C
inst✝¹ : IsModuleTopology R C
inst✝ : Module.Finite R B
bil : A →ₗ[R] B →ₗ[R] C
x✝ : A × B
⊢ (bil x✝.1) x✝.2 = ((fun ba ↦ (bil.flip ba.1) ba.2) ∘ Prod.swap) x✝
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:
;

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

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

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

Goal state after:
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
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
val✝ : ↑M.toModuleCat
hm : val✝ ∈ (↑(Hom.hom φ)).ker
⊢ (ConcreteCategory.hom (kerι φ ≫ φ)) ⟨val✝, hm⟩ = (ConcreteCategory.hom 0) ⟨val✝, hm⟩

Tactic:
;

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
M N : TopModuleCat R
φ : M ⟶ N
val✝ : ↑M.toModuleCat
hm : val✝ ∈ (↑(Hom.hom φ)).ker
⊢ (ConcreteCategory.hom (kerι φ ≫ φ)) ⟨val✝, hm⟩ = (ConcreteCategory.hom 0) ⟨val✝, hm⟩
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:
;

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

Goal state after:
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✝
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 ≫ kerι φ = Fork.ι s
⊢ m = ofHom ((Hom.hom (Fork.ι s)).codRestrict (↑(Hom.hom φ)).ker ⋯)

Tactic:
;

Goal state after:
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 ≫ kerι φ = Fork.ι s
⊢ m = ofHom ((Hom.hom (Fork.ι s)).codRestrict (↑(Hom.hom φ)).ker ⋯)
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:
;

Goal state after:
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
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 ≫ kerι φ = Fork.ι s
⊢ Fork.ι s = ofHom ((Hom.hom (Fork.ι s)).codRestrict (↑(Hom.hom φ)).ker ⋯) ≫ kerι φ

Tactic:
;

Goal state after:
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 ≫ kerι φ = Fork.ι s
⊢ Fork.ι s = ofHom ((Hom.hom (Fork.ι s)).codRestrict (↑(Hom.hom φ)).ker ⋯) ≫ kerι φ
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 : cokerπ φ ≫ m = Cofork.π s
⊢ m = ofHom { toLinearMap := (↑(Hom.hom φ)).range.liftQ ↑(Hom.hom (Cofork.π s)) ⋯, cont := ⋯ }

Tactic:
;

Goal state after:
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 : cokerπ φ ≫ m = Cofork.π s
⊢ m = ofHom { toLinearMap := (↑(Hom.hom φ)).range.liftQ ↑(Hom.hom (Cofork.π s)) ⋯, cont := ⋯ }
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 : cokerπ φ ≫ m = Cofork.π s
⊢ Cofork.π s = cokerπ φ ≫ ofHom { toLinearMap := (↑(Hom.hom φ)).range.liftQ ↑(Hom.hom (Cofork.π s)) ⋯, cont := ⋯ }

Tactic:
;

Goal state after:
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 : cokerπ φ ≫ m = Cofork.π s
⊢ Cofork.π s = cokerπ φ ≫ ofHom { toLinearMap := (↑(Hom.hom φ)).range.liftQ ↑(Hom.hom (Cofork.π s)) ⋯, cont := ⋯ }
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:
;

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

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

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

Goal state after:
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✝
Module: Mathlib.Algebra.Category.MonCat.Adjunctions

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

Tactic:
;

Goal state after:
M N : AddCommMonCat
f : M ⟶ N
⊢ Hom.hom ((forget AddCommMonCat ⋙ free).map f ≫ ofHom (Finsupp.liftAddHom ⇑(multiplesHom ↑N))) =
    Hom.hom (ofHom (Finsupp.liftAddHom ⇑(multiplesHom ↑M)) ≫ (𝟭 AddCommMonCat).map f)
Module: Mathlib.Algebra.Category.MonCat.Adjunctions

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

Tactic:
;

Goal state after:
M N : AddCommMonCat
f : M ⟶ N
⊢ Finsupp.liftAddHom.symm
      (Hom.hom ((forget AddCommMonCat ⋙ free).map f ≫ ofHom (Finsupp.liftAddHom ⇑(multiplesHom ↑N)))) =
    Finsupp.liftAddHom.symm (Hom.hom (ofHom (Finsupp.liftAddHom ⇑(multiplesHom ↑M)) ≫ (𝟭 AddCommMonCat).map f))
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))
r : ↑(of R)
⊢ (Hom.hom (ofHom (algebraMap R S) ≫ ofHom Algebra.TensorProduct.includeLeftRingHom)) r =
    (Hom.hom (ofHom (algebraMap R S) ≫ ofHom Algebra.TensorProduct.includeRight.toRingHom)) r

Tactic:
;

Goal state after:
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
H : Epi (ofHom (algebraMap R S))
r : ↑(of R)
⊢ (Hom.hom (ofHom (algebraMap R S) ≫ ofHom Algebra.TensorProduct.includeLeftRingHom)) r =
    (Hom.hom (ofHom (algebraMap R S) ≫ ofHom Algebra.TensorProduct.includeRight.toRingHom)) r
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))
r : ↑(of R)
⊢ (algebraMap R S) r ⊗ₜ[R] 1 = 1 ⊗ₜ[R] (algebraMap R S) r

Tactic:
;

Goal state after:
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
H : Epi (ofHom (algebraMap R S))
r : ↑(of R)
⊢ (algebraMap R S) r ⊗ₜ[R] 1 = 1 ⊗ₜ[R] (algebraMap R S) r
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
⊢ e.symm 1 * e 1 = 1

Tactic:
by
      rw [← smul_eq_mul, ← map_smul, smul_eq_mul, mul_one, apply_symm_apply]

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

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

Goal state after:
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✝
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
e : j ⟶ k
⊢ Over.Hom.left (((Functor.const J).obj (Over.mk (s.π.app i ≫ (F.obj i).hom))).map e ≫ Over.homMk (s.π.app k) ⋯) =
    Over.Hom.left (Over.homMk (s.π.app j) ⋯ ≫ F.map e)

Tactic:
;

Goal state after:
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
e : j ⟶ k
⊢ Over.Hom.left (((Functor.const J).obj (Over.mk (s.π.app i ≫ (F.obj i).hom))).map e ≫ Over.homMk (s.π.app k) ⋯) =
    Over.Hom.left (Over.homMk (s.π.app j) ⋯ ≫ F.map e)
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:
;

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

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

Tactic:
;

Goal state after:
J : MulticospanShape
inst✝³ : Fintype J.L
inst✝² : Fintype J.R
inst✝¹ : DecidableEq J.L
inst✝ : DecidableEq J.R
b : J.R
h₂ : J.snd b = J.fst b
f : (left (J.fst b) ⟶ right b) → Prop :=
  failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ f (eqToHom ⋯ ≫ Hom.fst b) = ?m.540 (J.fst b) ⋯ h₂
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
e : j ⟶ k
⊢ Under.Hom.right (F.map e ≫ Under.homMk (s.ι.app k) ⋯) =
    Under.Hom.right (Under.homMk (s.ι.app j) ⋯ ≫ ((Functor.const J).obj (Under.mk ((F.obj i).hom ≫ s.ι.app i))).map e)

Tactic:
;

Goal state after:
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
e : j ⟶ k
⊢ Under.Hom.right (F.map e ≫ Under.homMk (s.ι.app k) ⋯) =
    Under.Hom.right (Under.homMk (s.ι.app j) ⋯ ≫ ((Functor.const J).obj (Under.mk ((F.obj i).hom ≫ s.ι.app i))).map e)
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer

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

Tactic:
;

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