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

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

Tactic:
]

Goal state after:
R : Type u
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
h : S.Exact
⊢ Function.Exact ⇑(ConcreteCategory.hom (S.map (uliftFunctor.{u_1, v, u} R)).f)
    ⇑(ConcreteCategory.hom (S.map (uliftFunctor.{u_1, v, u} R)).g)
Module: Mathlib.Algebra.Category.ModuleCat.Ulift

Goal state before:
pp: R : Type u
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
h : S.Exact
x : ULift.{u_1, v} ↑S.X₂
⊢ ULift.moduleEquiv x ∈ Set.range ⇑(ConcreteCategory.hom S.f) ↔
    ∃ y, (Hom.hom S.f) (ULift.moduleEquiv y) = ULift.moduleEquiv x

Tactic:
]

Goal state after:
R : Type u
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
h : S.Exact
x : ULift.{u_1, v} ↑S.X₂
⊢ ULift.moduleEquiv x ∈ Set.range ⇑(ConcreteCategory.hom S.f) ↔
    ∃ y, (Hom.hom S.f) (ULift.moduleEquiv y) = ULift.moduleEquiv x
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:
have := small_lift.{u, v'} R

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : Small.{v, u} R
M : ModuleCat R
proj : Projective M
this : Small.{max v v', u} R
⊢ Projective ((uliftFunctor.{v', v, u} R).obj M)
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Homology

Goal state before:
pp: case refine_1
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)
⊢ ⇑(Hom.hom (D₁.i ≫ D₂.p)) = ⇑(Hom.hom (D₁.i ≫ D₂.p))

Tactic:
]

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)
hF' : Topology.IsEmbedding ⇑(ConcreteCategory.hom F)
⊢ Topology.IsEmbedding ⇑(ConcreteCategory.hom ((forget₂ (TopModuleCat R) TopCat).map F)) ∧
    Function.Surjective ⇑(ConcreteCategory.hom ((forget₂ (TopModuleCat R) TopCat).map F))

Tactic:
]

Goal state after:
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)
hF' : Topology.IsEmbedding ⇑(ConcreteCategory.hom F)
⊢ Topology.IsEmbedding ⇑(ConcreteCategory.hom ((forget₂ (TopModuleCat R) TopCat).map F)) ∧
    Function.Surjective ⇑(ConcreteCategory.hom ((forget₂ (TopModuleCat R) TopCat).map F))
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 (F.map f ≫ coconeMorphism F j')) x

Tactic:
]

Goal state after:
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 (F.map f ≫ coconeMorphism F j')) x
Module: Mathlib.Algebra.Category.MonCat.Colimits

Goal state before:
pp: case h.of
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
j : J
x✝ : ↑(F.obj j)
⊢ (Hom.hom m) (Quot.mk (⇑(colimitSetoid F)) (Prequotient.of j x✝)) =
    (ConcreteCategory.hom ((colimitCocone F).ι.app j ≫ m)) x✝

Tactic:
]

Goal state after:
case h.of
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
j : J
x✝ : ↑(F.obj j)
⊢ (Hom.hom m) (Quot.mk (⇑(colimitSetoid F)) (Prequotient.of j x✝)) =
    (ConcreteCategory.hom ((colimitCocone F).ι.app j ≫ m)) x✝
Module: Mathlib.Algebra.Category.MonCat.Colimits

Goal state before:
pp: case h.one
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
⊢ 1 = (Hom.hom (descMorphism F s)) 1

Tactic:
]

Goal state after:
case h.one
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
⊢ 1 = (Hom.hom (descMorphism F s)) 1
Module: Mathlib.Algebra.Category.MonCat.Colimits

Goal state before:
pp: case h.mul
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
x y : Prequotient F
hx : (Hom.hom m) (Quot.mk (⇑(colimitSetoid F)) x) = (Hom.hom (descMorphism F s)) (Quot.mk (⇑(colimitSetoid F)) x)
hy : (Hom.hom m) (Quot.mk (⇑(colimitSetoid F)) y) = (Hom.hom (descMorphism F s)) (Quot.mk (⇑(colimitSetoid F)) y)
⊢ (Hom.hom (descMorphism F s)) (Quot.mk (⇑(colimitSetoid F)) x) *
      (Hom.hom (descMorphism F s)) (Quot.mk (⇑(colimitSetoid F)) y) =
    (Hom.hom (descMorphism F s)) (Quot.mk (⇑(colimitSetoid F)) x * Quot.mk (⇑(colimitSetoid F)) y)

Tactic:
]

Goal state after:
case h.mul
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
x y : Prequotient F
hx : (Hom.hom m) (Quot.mk (⇑(colimitSetoid F)) x) = (Hom.hom (descMorphism F s)) (Quot.mk (⇑(colimitSetoid F)) x)
hy : (Hom.hom m) (Quot.mk (⇑(colimitSetoid F)) y) = (Hom.hom (descMorphism F s)) (Quot.mk (⇑(colimitSetoid F)) y)
⊢ (Hom.hom (descMorphism F s)) (Quot.mk (⇑(colimitSetoid F)) x) *
      (Hom.hom (descMorphism F s)) (Quot.mk (⇑(colimitSetoid F)) y) =
    (Hom.hom (descMorphism F s)) (Quot.mk (⇑(colimitSetoid F)) x * Quot.mk (⇑(colimitSetoid F)) y)
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₃
f g : M₁ ≃SL[σ₁₂] M₂
h₁ : (↑↑f).toFun = (↑↑g).toFun
h₂ : (↑f).invFun = (↑g).invFun
⊢ f = g

Tactic:
obtain ⟨f', _⟩ := f

Goal state after:
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₃
g : M₁ ≃SL[σ₁₂] M₂
f' : M₁ ≃ₛₗ[σ₁₂] M₂
continuous_toFun✝ : Continuous[inst✝¹⁰, inst✝⁸] (↑f').toFun
continuous_invFun✝ : Continuous[inst✝⁸, inst✝¹⁰] f'.invFun
h₁ :
  (↑↑{ toLinearEquiv := f', continuous_toFun := continuous_toFun✝, continuous_invFun := continuous_invFun✝ }).toFun =
    (↑↑g).toFun
h₂ :
  (↑{ toLinearEquiv := f', continuous_toFun := continuous_toFun✝, continuous_invFun := continuous_invFun✝ }).invFun =
    (↑g).invFun
⊢ { toLinearEquiv := f', continuous_toFun := continuous_toFun✝, continuous_invFun := continuous_invFun✝ } = g
Module: Mathlib.Topology.Algebra.Module.Equiv

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₁
f g : R₁ ≃L[R₁] M₁
h : f 1 = g 1
x : R₁
⊢ x • g 1 = x • g 1

Tactic:
]

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

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
inst✝⁹ : Semiring R₁
inst✝⁸ : Semiring R₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst✝⁷ : RingHomInvPair σ₁₂ σ₂₁
inst✝⁶ : RingHomInvPair σ₂₁ σ₁₂
M₁ : Type u_4
inst✝⁵ : TopologicalSpace M₁
inst✝⁴ : AddCommMonoid M₁
M₂ : Type u_5
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₁ M₁
inst✝ : Module R₂ M₂
e : M₁ ≃SL[σ₁₂] M₂
s : Set M₂
⊢ ⇑e ⁻¹' s = ⇑e ⁻¹' s

Tactic:
]

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

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
inst✝ : Epi f
h₂ : (CommRingCat.Hom.hom f).Finite
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom f).toAlgebra
algebraizeInst✝ : Module.Finite ↑R ↑S
this : Function.Surjective ⇑(algebraMap ↑R ↑S)
⊢ Function.Surjective ⇑(ConcreteCategory.hom f)

Tactic:
]

Goal state after:
R S : CommRingCat
f : R ⟶ S
inst✝ : Epi f
h₂ : (CommRingCat.Hom.hom f).Finite
algInst✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom f).toAlgebra
algebraizeInst✝ : Module.Finite ↑R ↑S
this : Function.Surjective ⇑(algebraMap ↑R ↑S)
⊢ Function.Surjective ⇑(ConcreteCategory.hom f)
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:
]

Goal state after:
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
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
⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M →L[R] M₂
g : M₂ →L[R] M
hf : f ∘SL g = ContinuousLinearMap.id R M₂
hg : g ∘SL f = ContinuousLinearMap.id R M
this : f = ↑(ContinuousLinearEquiv.equivOfInverse' f g hf hg)
⊢ ↑(ContinuousLinearEquiv.equivOfInverse' f g hf hg).symm = g

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M →L[R] M₂
g : M₂ →L[R] M
hf : f ∘SL g = ContinuousLinearMap.id R M₂
hg : g ∘SL f = ContinuousLinearMap.id R M
this : f = ↑(ContinuousLinearEquiv.equivOfInverse' f g hf hg)
⊢ ↑(ContinuousLinearEquiv.equivOfInverse' f g hf hg).symm = g
Module: Mathlib.Topology.Algebra.Module.Equiv

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

Tactic:
]

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

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

Tactic:
]

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

Goal state before:
pp: case neg
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₂
hf : ¬f.IsInvertible
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case h
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : Ring S
inst✝ : Algebra R S
g : S →ₐ[R] R
s : S
hs : (TensorProduct.includeLeftSubRight R S) s = 0
⊢ 1 ⊗ₜ[R] s = 1 ⊗ₜ[R] s

Tactic:
]

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

Goal state before:
pp: case neg
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₂
hf : ¬f.IsInvertible
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
hf : (Hom.hom f).FaithfullyFlat
algInst✝ : Algebra ↑R ↑S := (Hom.hom f).toAlgebra
algebraizeInst✝ : Module.FaithfullyFlat ↑R ↑S
⊢ ofHom (algebraMap ↑R ↑S) ≫ (pushoutCocone ↑R ↑S ↑S).inr = ofHom (algebraMap ↑R ↑S) ≫ (pushoutCocone ↑R ↑S ↑S).inr

Tactic:
]

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

Goal state before:
pp: case pos
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
e' : M ≃L[R] M₂
he' : ↑e' = f
⊢ (↑e').inverse = (↑e.symm ∘SL ↑e')⁻¹ʳ ∘SL ↑e.symm

Tactic:
]

Goal state after:
case pos
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
e' : M ≃L[R] M₂
he' : ↑e' = f
⊢ (↑e').inverse = (↑e.symm ∘SL ↑e')⁻¹ʳ ∘SL ↑e.symm
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: case h
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
F : (M →L[R] M)ˣ
hF : ↑F = ↑e.symm ∘SL f
x✝ : M
⊢ e ((↑e.symm ∘SL f) x✝) = f x✝

Tactic:
]

Goal state after:
case h
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
e : M ≃L[R] M₂
f : M →L[R] M₂
F : (M →L[R] M)ˣ
hF : ↑F = ↑e.symm ∘SL f
x✝ : M
⊢ e ((↑e.symm ∘SL f) x✝) = f x✝
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ (ContinuousLinearMap.id R M)⁻¹ʳ = ContinuousLinearMap.id R M

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ (ContinuousLinearMap.id R M)⁻¹ʳ = ContinuousLinearMap.id R M
Module: Mathlib.CategoryTheory.Comma.CardinalArrow

Goal state before:
pp: C : Type u
inst✝¹ : SmallCategory C
inst✝ : FinCategory C
⊢ Nonempty (FinCategory C)

Tactic:
]

Goal state after:
C : Type u
inst✝¹ : SmallCategory C
inst✝ : FinCategory C
⊢ Nonempty (FinCategory C)
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' ⟶ i₀
β : j' ⟶ j
s : J
γ : s ⟶ IsCofiltered.min i₀ j
δ : s ⟶ j'
h₁ : γ ≫ minToRight i₀ j = δ ≫ β
h₂ : γ ≫ minToLeft i₀ j = δ ≫ α
⊢ F.map γ ≫ F.map (minToRight i₀ j) = F.map γ ≫ F.map (minToRight i₀ j)

Tactic:
]

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
⊢ 𝟙 (F.obj i₀) = 𝟙 (F.obj i₀)

Tactic:
]

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'
⊢ h.coneπApp j' = h.coneπApp j ≫ F.map φ

Tactic:
]

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'
⊢ h.coneπApp j' = h.coneπApp j ≫ 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
⊢ instTopologicalSpaceCarrier R (ofCocone c).pt ≤
    TopologicalSpace.induced (ModuleCat.Hom.hom (hc.desc ((forget₂ (TopModuleCat R) (ModuleCat R)).mapCocone s))).toFun
      s.1.topologicalSpace

Tactic:
]

Goal state after:
R : Type u
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
M : ModuleCat R
I : Type u_1
X : I → TopModuleCat R
f : (i : I) → (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
⊢ instTopologicalSpaceCarrier R (ofCocone c).pt ≤
    TopologicalSpace.induced (ModuleCat.Hom.hom (hc.desc ((forget₂ (TopModuleCat R) (ModuleCat R)).mapCocone s))).toFun
      s.1.topologicalSpace
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.isoMap α ⋯).inv ≫ F.map β ≫ F.map φ = (h.isoMap α ⋯).inv ≫ F.map β ≫ F.map φ

Tactic:
]

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
s : Cone F
j : J
⊢ s.π.app (IsCofiltered.min i₀ j) ≫ F.map (minToRight i₀ j) = s.π.app (IsCofiltered.min i₀ j) ≫ F.map (minToRight i₀ j)

Tactic:
]

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) → (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
i : J
⊢ Continuous
    ((ModuleCat.Hom.hom (hc.desc ((forget₂ (TopModuleCat R) (ModuleCat R)).mapCocone s))).toFun ∘ ⇑(hom (c.ι.app i)))

Tactic:
]

Goal state after:
R : Type u
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
M : ModuleCat R
I : Type u_1
X : I → TopModuleCat R
f : (i : I) → (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
i : J
⊢ Continuous
    ((ModuleCat.Hom.hom (hc.desc ((forget₂ (TopModuleCat R) (ModuleCat R)).mapCocone s))).toFun ∘ ⇑(hom (c.ι.app i)))