mathlib-initiative/mathlib-tactics huggingface dataset:
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:
ext

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

Tactic:
constructor

Goal state after:
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
M N : TopModuleCat R
φ : M ⟶ N
⊢ ∀ (S : ShortComplex (TopModuleCat R)), S.HasHomology
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
  induction x <;> rfl

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

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
⊢ (MagmaCat.Hom.hom i.hom).comp (MagmaCat.Hom.hom i.inv) = MulHom.id ↑Y

Tactic:
ext

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
⊢ (Semigrp.Hom.hom i.inv).comp (Semigrp.Hom.hom i.hom) = MulHom.id ↑X

Tactic:
ext

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
⊢ (Semigrp.Hom.hom i.hom).comp (Semigrp.Hom.hom i.inv) = MulHom.id ↑Y

Tactic:
ext

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.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:
ext

Goal state after:
J : Type v
inst✝ : Category.{u, v} J
F : J ⥤ MonCat
j j' : J
f : j ⟶ j'
x✝ : ↑(F.obj j)
⊢ (Hom.hom (F.map f ≫ coconeMorphism F j')) x✝ = (Hom.hom (coconeMorphism F j)) x✝
Module: Mathlib.Algebra.Category.Ring.Epi

Goal state before:
pp: R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Epi (ofHom (algebraMap R S)) ↔ ∀ (a : S), a ⊗ₜ[R] 1 = 1 ⊗ₜ[R] a

Tactic:
constructor

Goal state after:
case mp
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Epi (ofHom (algebraMap R S)) → ∀ (a : S), a ⊗ₜ[R] 1 = 1 ⊗ₜ[R] a

case mpr
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (∀ (a : S), a ⊗ₜ[R] 1 = 1 ⊗ₜ[R] a) → Epi (ofHom (algebraMap R S))
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₃
inst✝² : Module R₁ M₁
inst✝¹ : Module R₂ M₂
inst✝ : Module R₃ M₃
e₁ : M₁ ≃SL[σ₁₂] M₂
e₂ : M₂ ≃SL[σ₂₃] M₃
⊢ ↑(e₁.trans e₂) = (↑e₁).trans ↑e₂

Tactic:
ext

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₃
inst✝² : Module R₁ M₁
inst✝¹ : Module R₂ M₂
inst✝ : Module R₃ M₃
e₁ : M₁ ≃SL[σ₁₂] M₂
e₂ : M₂ ≃SL[σ₂₃] M₃
x✝ : M₁
⊢ ↑(e₁.trans e₂) x✝ = ((↑e₁).trans ↑e₂) x✝
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
⊢ ↑f * ↑f.symm = 1

Tactic:
ext

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
⊢ (↑f * ↑f.symm) x✝ = 1 x✝
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
⊢ ↑f.symm * ↑f = 1

Tactic:
ext

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
⊢ (↑f.symm * ↑f) x✝ = 1 x✝
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
x y : (M →L[R] M)ˣ
⊢ ofUnit (x * y) = ofUnit x * ofUnit y

Tactic:
ext

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : TopologicalSpace M
x y : (M →L[R] M)ˣ
x✝ : M
⊢ (ofUnit (x * y)) x✝ = (ofUnit x * ofUnit y) 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₂
⊢ (↑e ∘SL f).IsInvertible ↔ f.IsInvertible

Tactic:
constructor

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₂
⊢ (↑e ∘SL f).IsInvertible → f.IsInvertible

case mpr
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₂
⊢ f.IsInvertible → (↑e ∘SL f).IsInvertible
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
⊢ f = ↑e.symm ∘SL ↑e ∘SL f

Tactic:
ext

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₂
⊢ (f ∘SL ↑e).IsInvertible ↔ f.IsInvertible

Tactic:
constructor

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₂
⊢ (f ∘SL ↑e).IsInvertible → f.IsInvertible

case mpr
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₂
⊢ f.IsInvertible → (f ∘SL ↑e).IsInvertible
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
⊢ f = (f ∘SL ↑e) ∘SL ↑e.symm

Tactic:
ext

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.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
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra R T
⊢ ↑(LinearEquiv.restrictScalars R (TensorProduct.AlgebraTensorModule.distribBaseChange R T S S)) ∘ₗ
      LinearMap.lTensor T (includeLeftSubRight R S) =
    ↑R (includeLeftSubRight T (T ⊗[R] S))

Tactic:
ext

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : Ring S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommRing T
inst✝ : Algebra R T
x✝¹ : T
x✝ : S
⊢ ((TensorProduct.AlgebraTensorModule.curry
          (↑(LinearEquiv.restrictScalars R (TensorProduct.AlgebraTensorModule.distribBaseChange R T S S)) ∘ₗ
            LinearMap.lTensor T (includeLeftSubRight R S)))
        x✝¹)
      x✝ =
    ((TensorProduct.AlgebraTensorModule.curry (↑R (includeLeftSubRight T (T ⊗[R] S)))) x✝¹) x✝
Module: Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight

Goal state before:
pp: case refine_1
R : Type u_3
inst✝⁵ : CommRing R
S : Type u_4
T : Type u_5
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Ring S
inst✝¹ : Algebra R S
inst✝ : Module.FaithfullyFlat R T
h : IsEffective T (T ⊗[R] S)
⊢ (↑(Algebra.linearMap T (T ⊗[R] S))).comp (TensorProduct.rid R R T).toAddEquiv.toAddMonoidHom =
    (AddMonoidHom.id (T ⊗[R] S)).comp ↑(LinearMap.lTensor T (Algebra.linearMap R S))

Tactic:
ext

Goal state after:
case refine_1
R : Type u_3
inst✝⁵ : CommRing R
S : Type u_4
T : Type u_5
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Ring S
inst✝¹ : Algebra R S
inst✝ : Module.FaithfullyFlat R T
h : IsEffective T (T ⊗[R] S)
x✝ : T ⊗[R] R
⊢ ((↑(Algebra.linearMap T (T ⊗[R] S))).comp (TensorProduct.rid R R T).toAddEquiv.toAddMonoidHom) x✝ =
    ((AddMonoidHom.id (T ⊗[R] S)).comp ↑(LinearMap.lTensor T (Algebra.linearMap R S))) x✝
Module: Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight

Goal state before:
pp: case refine_2
R : Type u_3
inst✝⁵ : CommRing R
S : Type u_4
T : Type u_5
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Ring S
inst✝¹ : Algebra R S
inst✝ : Module.FaithfullyFlat R T
h : IsEffective T (T ⊗[R] S)
⊢ (↑(TensorProduct.includeLeftSubRight T (T ⊗[R] S))).comp (AddMonoidHom.id (T ⊗[R] S)) =
    (↑(TensorProduct.AlgebraTensorModule.distribBaseChange R T S S)).toAddMonoidHom.comp
      ↑(LinearMap.lTensor T (TensorProduct.includeLeftSubRight R S))

Tactic:
ext

Goal state after:
case refine_2
R : Type u_3
inst✝⁵ : CommRing R
S : Type u_4
T : Type u_5
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Ring S
inst✝¹ : Algebra R S
inst✝ : Module.FaithfullyFlat R T
h : IsEffective T (T ⊗[R] S)
x✝ : T ⊗[R] S
⊢ ((↑(TensorProduct.includeLeftSubRight T (T ⊗[R] S))).comp (AddMonoidHom.id (T ⊗[R] S))) x✝ =
    ((↑(TensorProduct.AlgebraTensorModule.distribBaseChange R T S S)).toAddMonoidHom.comp
        ↑(LinearMap.lTensor T (TensorProduct.includeLeftSubRight R S)))
      x✝
Module: Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight

Goal state before:
pp: R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.FaithfullyFlat R S
⊢ Function.Bijective ⇑(codRestrictEqLocusPushoutCocone R S)

Tactic:
constructor

Goal state after:
case left
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.FaithfullyFlat R S
⊢ Function.Injective ⇑(codRestrictEqLocusPushoutCocone R S)

case right
R S : Type u
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Module.FaithfullyFlat R S
⊢ Function.Surjective ⇑(codRestrictEqLocusPushoutCocone R S)
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'.trans e.symm))⁻¹ʳ ∘SL ↑e.symm

Tactic:
ext

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
x✝ : M₂
⊢ (↑e').inverse x✝ = ((↑(e'.trans e.symm))⁻¹ʳ ∘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
⊢ ((Functor.const J).obj (Over.mk (s.π.app i ≫ (F.obj i).hom))).map e ≫ Over.homMk (s.π.app k) ⋯ =
    Over.homMk (s.π.app j) ⋯ ≫ F.map e

Tactic:
ext

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.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
⊢ ↑(((ContinuousLinearEquiv.unitsEquiv R M) F).trans e) = f

Tactic:
ext

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
⊢ ↑(((ContinuousLinearEquiv.unitsEquiv R M) F).trans e) x✝ = f 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' : 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
⊢ F.map e ≫ Under.homMk (s.ι.app k) ⋯ =
    Under.homMk (s.ι.app j) ⋯ ≫ ((Functor.const J).obj (Under.mk ((F.obj i).hom ≫ s.ι.app i))).map e

Tactic:
ext

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.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
s' : Cocone F :=
  { pt := Under.mk ((F.obj i).hom ≫ s.ι.app i), ι := { app := fun j ↦ Under.homMk (s.ι.app j) ⋯, naturality := ⋯ } }
⊢ ∃! l, ∀ (j : J), ((Under.forget X).mapCocone c).ι.app j ≫ l = s.ι.app j

Tactic:
refine ⟨(hc.desc s').right, fun j ↦ congr($(hc.fac s' j).right), fun f hf ↦ ?_⟩

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
s' : Cocone F :=
  { pt := Under.mk ((F.obj i).hom ≫ s.ι.app i), ι := { app := fun j ↦ Under.homMk (s.ι.app j) ⋯, naturality := ⋯ } }
f : ((Under.forget X).mapCocone c).pt ⟶ s.pt
hf : (fun l ↦ ∀ (j : J), ((Under.forget X).mapCocone c).ι.app j ≫ l = s.ι.app j) f
⊢ f = Under.Hom.right (hc.desc s')
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
⊢ Ring.inverse = inverse

Tactic:
ext

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝¹ : M →L[R] M
x✝ : M
⊢ x✝¹⁻¹ʳ x✝ = x✝¹.inverse 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₃
inst✝ : ContinuousAdd M
f : M₂ →L[R] M
g : M₃ →L[R] M
⊢ f.coprod g ∘SL ↑(ContinuousLinearEquiv.prodComm R M₃ M₂) = g.coprod f

Tactic:
ext

Goal state after:
case hl
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₃
inst✝ : ContinuousAdd M
f : M₂ →L[R] M
g : M₃ →L[R] M
x✝ : M₃
⊢ ((f.coprod g ∘SL ↑(ContinuousLinearEquiv.prodComm R M₃ M₂)) ∘SL inl R M₃ M₂) x✝ = (g.coprod f ∘SL inl R M₃ M₂) x✝

case hr
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₃
inst✝ : ContinuousAdd M
f : M₂ →L[R] M
g : M₃ →L[R] M
x✝ : M₂
⊢ ((f.coprod g ∘SL ↑(ContinuousLinearEquiv.prodComm R M₃ M₂)) ∘SL inr R M₃ M₂) x✝ = (g.coprod f ∘SL inr R M₃ M₂) x✝
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: S : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
G : Type u_5
inst✝²² : Semiring R
inst✝²¹ : Semiring S
inst✝²⁰ : AddCommMonoid V
inst✝¹⁹ : Module R V
inst✝¹⁸ : TopologicalSpace V
inst✝¹⁷ : Module S V
inst✝¹⁶ : ContinuousConstSMul S V
inst✝¹⁵ : AddCommMonoid W
inst✝¹⁴ : Module R W
inst✝¹³ : TopologicalSpace W
inst✝¹² : Module S W
inst✝¹¹ : ContinuousConstSMul S W
inst✝¹⁰ : AddCommMonoid G
inst✝⁹ : Module R G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Module S G
inst✝⁶ : ContinuousConstSMul S G
inst✝⁵ : SMulCommClass R S W
inst✝⁴ : SMul S R
inst✝³ : IsScalarTower S R V
inst✝² : IsScalarTower S R W
inst✝¹ : SMulCommClass R S V
inst✝ : IsScalarTower S R G
α : Sˣ
e : G ≃L[R] V
f : V ≃L[R] W
⊢ (α • e).trans f = α • e.trans f

Tactic:
ext

Goal state after:
S : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
G : Type u_5
inst✝²² : Semiring R
inst✝²¹ : Semiring S
inst✝²⁰ : AddCommMonoid V
inst✝¹⁹ : Module R V
inst✝¹⁸ : TopologicalSpace V
inst✝¹⁷ : Module S V
inst✝¹⁶ : ContinuousConstSMul S V
inst✝¹⁵ : AddCommMonoid W
inst✝¹⁴ : Module R W
inst✝¹³ : TopologicalSpace W
inst✝¹² : Module S W
inst✝¹¹ : ContinuousConstSMul S W
inst✝¹⁰ : AddCommMonoid G
inst✝⁹ : Module R G
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Module S G
inst✝⁶ : ContinuousConstSMul S G
inst✝⁵ : SMulCommClass R S W
inst✝⁴ : SMul S R
inst✝³ : IsScalarTower S R V
inst✝² : IsScalarTower S R W
inst✝¹ : SMulCommClass R S V
inst✝ : IsScalarTower S R G
α : Sˣ
e : G ≃L[R] V
f : V ≃L[R] W
x✝ : G
⊢ ((α • e).trans f) x✝ = (α • e.trans f) x✝
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: S : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
G : Type u_5
inst✝²¹ : Semiring R
inst✝²⁰ : Semiring S
inst✝¹⁹ : AddCommMonoid V
inst✝¹⁸ : Module R V
inst✝¹⁷ : TopologicalSpace V
inst✝¹⁶ : Module S V
inst✝¹⁵ : ContinuousConstSMul S V
inst✝¹⁴ : AddCommMonoid W
inst✝¹³ : Module R W
inst✝¹² : TopologicalSpace W
inst✝¹¹ : Module S W
inst✝¹⁰ : ContinuousConstSMul S W
inst✝⁹ : AddCommMonoid G
inst✝⁸ : Module R G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Module S G
inst✝⁵ : ContinuousConstSMul S G
inst✝⁴ : SMulCommClass R S W
inst✝³ : SMul S R
inst✝² : IsScalarTower S R V
inst✝¹ : IsScalarTower S R W
inst✝ : IsScalarTower S R G
α : Sˣ
e : G ≃L[R] V
f : V ≃L[R] W
⊢ e.trans (α • f) = α • e.trans f

Tactic:
ext

Goal state after:
S : Type u_1
R : Type u_2
V : Type u_3
W : Type u_4
G : Type u_5
inst✝²¹ : Semiring R
inst✝²⁰ : Semiring S
inst✝¹⁹ : AddCommMonoid V
inst✝¹⁸ : Module R V
inst✝¹⁷ : TopologicalSpace V
inst✝¹⁶ : Module S V
inst✝¹⁵ : ContinuousConstSMul S V
inst✝¹⁴ : AddCommMonoid W
inst✝¹³ : Module R W
inst✝¹² : TopologicalSpace W
inst✝¹¹ : Module S W
inst✝¹⁰ : ContinuousConstSMul S W
inst✝⁹ : AddCommMonoid G
inst✝⁸ : Module R G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Module S G
inst✝⁵ : ContinuousConstSMul S G
inst✝⁴ : SMulCommClass R S W
inst✝³ : SMul S R
inst✝² : IsScalarTower S R V
inst✝¹ : IsScalarTower S R W
inst✝ : IsScalarTower S R G
α : Sˣ
e : G ≃L[R] V
f : V ≃L[R] W
x✝ : G
⊢ (e.trans (α • f)) x✝ = (α • e.trans f) x✝