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

Goal state before:
pp: case refine_1.refine_1
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : X ⟶ (restrictScalars f).obj Y
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
z : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑X
s₁ s₂ : S
⊢ evalAt f (s₁ + s₂) g = evalAt f s₁ g + evalAt f s₂ g

pp: case refine_1.refine_2
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : X ⟶ (restrictScalars f).obj Y
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
z : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑X
r : R
s : S
⊢ evalAt f (r • s) g = (RingHom.id R) r • evalAt f s g

Tactic:
·

Goal state after:
case refine_1.refine_1
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : X ⟶ (restrictScalars f).obj Y
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
z : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑X
s₁ s₂ : S
⊢ evalAt f (s₁ + s₂) g = evalAt f s₁ g + evalAt f s₂ g
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: case refine_1.refine_2
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : X ⟶ (restrictScalars f).obj Y
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
z : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑X
r : R
s : S
⊢ evalAt f (r • s) g = (RingHom.id R) r • evalAt f s g

Tactic:
·

Goal state after:
case refine_1.refine_2
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : X ⟶ (restrictScalars f).obj Y
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
z : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑X
r : R
s : S
⊢ evalAt f (r • s) g = (RingHom.id R) r • evalAt f s g
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: case refine_2
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : X ⟶ (restrictScalars f).obj Y
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
⊢ ∀ (x y : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑X),
    (lift { toFun := fun s ↦ evalAt f s g, map_add' := ⋯, map_smul' := ⋯ }) (x + y) =
      (lift { toFun := fun s ↦ evalAt f s g, map_add' := ⋯, map_smul' := ⋯ }) x +
        (lift { toFun := fun s ↦ evalAt f s g, map_add' := ⋯, map_smul' := ⋯ }) y

pp: case refine_3
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : X ⟶ (restrictScalars f).obj Y
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
⊢ ∀ (m : S) (x : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑X),
    (lift { toFun := fun s ↦ evalAt f s g, map_add' := ⋯, map_smul' := ⋯ }) (m • x) =
      (RingHom.id S) m • (lift { toFun := fun s ↦ evalAt f s g, map_add' := ⋯, map_smul' := ⋯ }) x

Tactic:
·

Goal state after:
case refine_2
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : X ⟶ (restrictScalars f).obj Y
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
⊢ ∀ (x y : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑X),
    (lift { toFun := fun s ↦ evalAt f s g, map_add' := ⋯, map_smul' := ⋯ }) (x + y) =
      (lift { toFun := fun s ↦ evalAt f s g, map_add' := ⋯, map_smul' := ⋯ }) x +
        (lift { toFun := fun s ↦ evalAt f s g, map_add' := ⋯, map_smul' := ⋯ }) y
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: case refine_3
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : X ⟶ (restrictScalars f).obj Y
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
⊢ ∀ (m : S) (x : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑X),
    (lift { toFun := fun s ↦ evalAt f s g, map_add' := ⋯, map_smul' := ⋯ }) (m • x) =
      (RingHom.id S) m • (lift { toFun := fun s ↦ evalAt f s g, map_add' := ⋯, map_smul' := ⋯ }) x

Tactic:
·

Goal state after:
case refine_3
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : X ⟶ (restrictScalars f).obj Y
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
⊢ ∀ (m : S) (x : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑X),
    (lift { toFun := fun s ↦ evalAt f s g, map_add' := ⋯, map_smul' := ⋯ }) (m • x) =
      (RingHom.id S) m • (lift { toFun := fun s ↦ evalAt f s g, map_add' := ⋯, map_smul' := ⋯ }) x
Module: Mathlib.RingTheory.Coalgebra.TensorProduct

Goal state before:
pp: case e'_3
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid A
inst✝⁷ : AddCommMonoid B
inst✝⁶ : Algebra R S
inst✝⁵ : Module R A
inst✝⁴ : Module S A
inst✝³ : Module R B
inst✝² : IsScalarTower R S A
inst✝¹ : Coalgebra R B
inst✝ : Coalgebra S A
x : A
y : B
F : A ⊗[S] (A ⊗[S] A) ⊗[R] (B ⊗[R] (B ⊗[R] B)) ≃ₗ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)) :=
  AlgebraTensorModule.tensorTensorTensorComm R S R S A (A ⊗[S] A) B (B ⊗[R] B) ≪≫ₗ
    AlgebraTensorModule.congr (LinearEquiv.refl S (A ⊗[R] B))
      (AlgebraTensorModule.tensorTensorTensorComm R S R S A A B B)
F' : A ⊗[S] (A ⊗[S] A) ⊗[R] (B ⊗[R] (B ⊗[R] B)) →ₗ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)) :=
  mapOfCompatibleSMul S S S (A ⊗[R] B) (A ⊗[R] B ⊗[S] (A ⊗[R] B)) ∘ₗ
    map LinearMap.id (mapOfCompatibleSMul S S S (A ⊗[R] B) (A ⊗[R] B)) ∘ₗ ↑F
⊢ ((AlgebraTensorModule.curry (LinearMap.lTensor (A ⊗[R] B) comul ∘ₗ comul)) x) y =
    F ((LinearMap.lTensor A comul) (comul x) ⊗ₜ[R] (LinearMap.lTensor B comul) (comul y))

Tactic:
·

Goal state after:
case e'_3
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid A
inst✝⁷ : AddCommMonoid B
inst✝⁶ : Algebra R S
inst✝⁵ : Module R A
inst✝⁴ : Module S A
inst✝³ : Module R B
inst✝² : IsScalarTower R S A
inst✝¹ : Coalgebra R B
inst✝ : Coalgebra S A
x : A
y : B
F : A ⊗[S] (A ⊗[S] A) ⊗[R] (B ⊗[R] (B ⊗[R] B)) ≃ₗ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)) :=
  AlgebraTensorModule.tensorTensorTensorComm R S R S A (A ⊗[S] A) B (B ⊗[R] B) ≪≫ₗ
    AlgebraTensorModule.congr (LinearEquiv.refl S (A ⊗[R] B))
      (AlgebraTensorModule.tensorTensorTensorComm R S R S A A B B)
F' : A ⊗[S] (A ⊗[S] A) ⊗[R] (B ⊗[R] (B ⊗[R] B)) →ₗ[S] A ⊗[R] B ⊗[S] (A ⊗[R] B ⊗[S] (A ⊗[R] B)) :=
  mapOfCompatibleSMul S S S (A ⊗[R] B) (A ⊗[R] B ⊗[S] (A ⊗[R] B)) ∘ₗ
    map LinearMap.id (mapOfCompatibleSMul S S S (A ⊗[R] B) (A ⊗[R] B)) ∘ₗ ↑F
⊢ ((AlgebraTensorModule.curry (LinearMap.lTensor (A ⊗[R] B) comul ∘ₗ comul)) x) y =
    F ((LinearMap.lTensor A comul) (comul x) ⊗ₜ[R] (LinearMap.lTensor B comul) (comul y))
Module: Mathlib.RingTheory.Coalgebra.TensorProduct

Goal state before:
pp: case e'_2
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid A
inst✝⁷ : AddCommMonoid B
inst✝⁶ : Algebra R S
inst✝⁵ : Module R A
inst✝⁴ : Module S A
inst✝³ : Module R B
inst✝² : IsScalarTower R S A
inst✝¹ : Coalgebra R B
inst✝ : Coalgebra S A
x : A
y : B
⊢ ((AlgebraTensorModule.curry (LinearMap.rTensor (A ⊗[R] B) counit ∘ₗ comul)) x) y =
    (TensorProduct.lid S (A ⊗[R] B)).symm
      ((TensorProduct.lid S A) ((LinearMap.rTensor A counit) (comul x)) ⊗ₜ[R]
        (TensorProduct.lid R B) ((LinearMap.rTensor B counit) (comul y)))

pp: case e'_3
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid A
inst✝⁷ : AddCommMonoid B
inst✝⁶ : Algebra R S
inst✝⁵ : Module R A
inst✝⁴ : Module S A
inst✝³ : Module R B
inst✝² : IsScalarTower R S A
inst✝¹ : Coalgebra R B
inst✝ : Coalgebra S A
x : A
y : B
⊢ ((AlgebraTensorModule.curry ((mk S S (A ⊗[R] B)) 1)) x) y =
    (TensorProduct.lid S (A ⊗[R] B)).symm
      ((TensorProduct.lid S A) (1 ⊗ₜ[S] x) ⊗ₜ[R] (TensorProduct.lid R B) (1 ⊗ₜ[R] y))

Tactic:
·

Goal state after:
case e'_2
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid A
inst✝⁷ : AddCommMonoid B
inst✝⁶ : Algebra R S
inst✝⁵ : Module R A
inst✝⁴ : Module S A
inst✝³ : Module R B
inst✝² : IsScalarTower R S A
inst✝¹ : Coalgebra R B
inst✝ : Coalgebra S A
x : A
y : B
⊢ ((AlgebraTensorModule.curry (LinearMap.rTensor (A ⊗[R] B) counit ∘ₗ comul)) x) y =
    (TensorProduct.lid S (A ⊗[R] B)).symm
      ((TensorProduct.lid S A) ((LinearMap.rTensor A counit) (comul x)) ⊗ₜ[R]
        (TensorProduct.lid R B) ((LinearMap.rTensor B counit) (comul y)))
Module: Mathlib.RingTheory.Coalgebra.TensorProduct

Goal state before:
pp: case e'_3
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid A
inst✝⁷ : AddCommMonoid B
inst✝⁶ : Algebra R S
inst✝⁵ : Module R A
inst✝⁴ : Module S A
inst✝³ : Module R B
inst✝² : IsScalarTower R S A
inst✝¹ : Coalgebra R B
inst✝ : Coalgebra S A
x : A
y : B
⊢ ((AlgebraTensorModule.curry ((mk S S (A ⊗[R] B)) 1)) x) y =
    (TensorProduct.lid S (A ⊗[R] B)).symm
      ((TensorProduct.lid S A) (1 ⊗ₜ[S] x) ⊗ₜ[R] (TensorProduct.lid R B) (1 ⊗ₜ[R] y))

Tactic:
·

Goal state after:
case e'_3
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid A
inst✝⁷ : AddCommMonoid B
inst✝⁶ : Algebra R S
inst✝⁵ : Module R A
inst✝⁴ : Module S A
inst✝³ : Module R B
inst✝² : IsScalarTower R S A
inst✝¹ : Coalgebra R B
inst✝ : Coalgebra S A
x : A
y : B
⊢ ((AlgebraTensorModule.curry ((mk S S (A ⊗[R] B)) 1)) x) y =
    (TensorProduct.lid S (A ⊗[R] B)).symm
      ((TensorProduct.lid S A) (1 ⊗ₜ[S] x) ⊗ₜ[R] (TensorProduct.lid R B) (1 ⊗ₜ[R] y))
Module: Mathlib.RingTheory.Coalgebra.TensorProduct

Goal state before:
pp: case e'_2
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid A
inst✝⁷ : AddCommMonoid B
inst✝⁶ : Algebra R S
inst✝⁵ : Module R A
inst✝⁴ : Module S A
inst✝³ : Module R B
inst✝² : IsScalarTower R S A
inst✝¹ : Coalgebra R B
inst✝ : Coalgebra S A
x : A
y : B
⊢ ((AlgebraTensorModule.curry (LinearMap.lTensor (A ⊗[R] B) counit ∘ₗ comul)) x) y =
    (TensorProduct.rid S (A ⊗[R] B)).symm
      ((TensorProduct.rid S A) ((LinearMap.lTensor A counit) (comul x)) ⊗ₜ[R]
        (TensorProduct.rid R B) ((LinearMap.lTensor B counit) (comul y)))

pp: case e'_3
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid A
inst✝⁷ : AddCommMonoid B
inst✝⁶ : Algebra R S
inst✝⁵ : Module R A
inst✝⁴ : Module S A
inst✝³ : Module R B
inst✝² : IsScalarTower R S A
inst✝¹ : Coalgebra R B
inst✝ : Coalgebra S A
x : A
y : B
⊢ ((AlgebraTensorModule.curry ((mk S (A ⊗[R] B) S).flip 1)) x) y =
    (TensorProduct.rid S (A ⊗[R] B)).symm
      ((TensorProduct.rid S A) (x ⊗ₜ[S] 1) ⊗ₜ[R] (TensorProduct.rid R B) (y ⊗ₜ[R] 1))

Tactic:
·

Goal state after:
case e'_2
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid A
inst✝⁷ : AddCommMonoid B
inst✝⁶ : Algebra R S
inst✝⁵ : Module R A
inst✝⁴ : Module S A
inst✝³ : Module R B
inst✝² : IsScalarTower R S A
inst✝¹ : Coalgebra R B
inst✝ : Coalgebra S A
x : A
y : B
⊢ ((AlgebraTensorModule.curry (LinearMap.lTensor (A ⊗[R] B) counit ∘ₗ comul)) x) y =
    (TensorProduct.rid S (A ⊗[R] B)).symm
      ((TensorProduct.rid S A) ((LinearMap.lTensor A counit) (comul x)) ⊗ₜ[R]
        (TensorProduct.rid R B) ((LinearMap.lTensor B counit) (comul y)))
Module: Mathlib.RingTheory.Coalgebra.TensorProduct

Goal state before:
pp: case e'_3
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid A
inst✝⁷ : AddCommMonoid B
inst✝⁶ : Algebra R S
inst✝⁵ : Module R A
inst✝⁴ : Module S A
inst✝³ : Module R B
inst✝² : IsScalarTower R S A
inst✝¹ : Coalgebra R B
inst✝ : Coalgebra S A
x : A
y : B
⊢ ((AlgebraTensorModule.curry ((mk S (A ⊗[R] B) S).flip 1)) x) y =
    (TensorProduct.rid S (A ⊗[R] B)).symm
      ((TensorProduct.rid S A) (x ⊗ₜ[S] 1) ⊗ₜ[R] (TensorProduct.rid R B) (y ⊗ₜ[R] 1))

Tactic:
·

Goal state after:
case e'_3
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommSemiring R
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid A
inst✝⁷ : AddCommMonoid B
inst✝⁶ : Algebra R S
inst✝⁵ : Module R A
inst✝⁴ : Module S A
inst✝³ : Module R B
inst✝² : IsScalarTower R S A
inst✝¹ : Coalgebra R B
inst✝ : Coalgebra S A
x : A
y : B
⊢ ((AlgebraTensorModule.curry ((mk S (A ⊗[R] B) S).flip 1)) x) y =
    (TensorProduct.rid S (A ⊗[R] B)).symm
      ((TensorProduct.rid S A) (x ⊗ₜ[S] 1) ⊗ₜ[R] (TensorProduct.rid R B) (y ⊗ₜ[R] 1))
Module: Mathlib.CategoryTheory.Category.Pointed

Goal state before:
pp: case none
X : Type ?u.36
Y : Pointed
f : typeToPointed.obj X ⟶ Y
⊢ ((fun f ↦ { toFun := fun o ↦ Option.elim o Y.point ⇑(ConcreteCategory.hom f), map_point := ⋯ })
          ((fun f ↦ ↾(f.toFun ∘ some)) f)).toFun
      none =
    f.toFun none

pp: case some
X : Type ?u.36
Y : Pointed
f : typeToPointed.obj X ⟶ Y
val✝ : X
⊢ ((fun f ↦ { toFun := fun o ↦ Option.elim o Y.point ⇑(ConcreteCategory.hom f), map_point := ⋯ })
          ((fun f ↦ ↾(f.toFun ∘ some)) f)).toFun
      (some val✝) =
    f.toFun (some val✝)

Tactic:
·

Goal state after:
case none
X : Type ?u.36
Y : Pointed
f : typeToPointed.obj X ⟶ Y
⊢ ((fun f ↦ { toFun := fun o ↦ Option.elim o Y.point ⇑(ConcreteCategory.hom f), map_point := ⋯ })
          ((fun f ↦ ↾(f.toFun ∘ some)) f)).toFun
      none =
    f.toFun none
Module: Mathlib.CategoryTheory.Category.Pointed

Goal state before:
pp: case some
X : Type ?u.36
Y : Pointed
f : typeToPointed.obj X ⟶ Y
val✝ : X
⊢ ((fun f ↦ { toFun := fun o ↦ Option.elim o Y.point ⇑(ConcreteCategory.hom f), map_point := ⋯ })
          ((fun f ↦ ↾(f.toFun ∘ some)) f)).toFun
      (some val✝) =
    f.toFun (some val✝)

Tactic:
·

Goal state after:
case some
X : Type ?u.36
Y : Pointed
f : typeToPointed.obj X ⟶ Y
val✝ : X
⊢ ((fun f ↦ { toFun := fun o ↦ Option.elim o Y.point ⇑(ConcreteCategory.hom f), map_point := ⋯ })
          ((fun f ↦ ↾(f.toFun ∘ some)) f)).toFun
      (some val✝) =
    f.toFun (some val✝)
Module: Mathlib.RingTheory.Bialgebra.TensorProduct

Goal state before:
pp: case ha
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Bialgebra R A
inst✝ : Bialgebra R B
a : A
⊢ (((Algebra.TensorProduct.map ↑(Algebra.TensorProduct.comm R A B) ↑(Algebra.TensorProduct.comm R A B)).comp
            (comulAlgHom R (A ⊗[R] B))).comp
        Algebra.TensorProduct.includeLeft)
      a =
    (((comulAlgHom R (B ⊗[R] A)).comp ↑(Algebra.TensorProduct.comm R A B)).comp Algebra.TensorProduct.includeLeft) a

Tactic:
·

Goal state after:
case ha
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Bialgebra R A
inst✝ : Bialgebra R B
a : A
⊢ (((Algebra.TensorProduct.map ↑(Algebra.TensorProduct.comm R A B) ↑(Algebra.TensorProduct.comm R A B)).comp
            (comulAlgHom R (A ⊗[R] B))).comp
        Algebra.TensorProduct.includeLeft)
      a =
    (((comulAlgHom R (B ⊗[R] A)).comp ↑(Algebra.TensorProduct.comm R A B)).comp Algebra.TensorProduct.includeLeft) a
Module: Mathlib.CategoryTheory.Category.Bipointed

Goal state before:
pp: case none
X : Pointed
Y : Bipointed
f : pointedToBipointedFst.obj X ⟶ Y
⊢ ((fun f ↦ { toFun := fun o ↦ Option.elim o Y.toProd.2 f.toFun, map_fst := ⋯, map_snd := ⋯ })
          ((fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ }) f)).toFun
      none =
    f.toFun none

pp: case some
X : Pointed
Y : Bipointed
f : pointedToBipointedFst.obj X ⟶ Y
val✝ : X.X
⊢ ((fun f ↦ { toFun := fun o ↦ Option.elim o Y.toProd.2 f.toFun, map_fst := ⋯, map_snd := ⋯ })
          ((fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ }) f)).toFun
      (some val✝) =
    f.toFun (some val✝)

Tactic:
·

Goal state after:
case none
X : Pointed
Y : Bipointed
f : pointedToBipointedFst.obj X ⟶ Y
⊢ ((fun f ↦ { toFun := fun o ↦ Option.elim o Y.toProd.2 f.toFun, map_fst := ⋯, map_snd := ⋯ })
          ((fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ }) f)).toFun
      none =
    f.toFun none
Module: Mathlib.CategoryTheory.Category.Bipointed

Goal state before:
pp: case some
X : Pointed
Y : Bipointed
f : pointedToBipointedFst.obj X ⟶ Y
val✝ : X.X
⊢ ((fun f ↦ { toFun := fun o ↦ Option.elim o Y.toProd.2 f.toFun, map_fst := ⋯, map_snd := ⋯ })
          ((fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ }) f)).toFun
      (some val✝) =
    f.toFun (some val✝)

Tactic:
·

Goal state after:
case some
X : Pointed
Y : Bipointed
f : pointedToBipointedFst.obj X ⟶ Y
val✝ : X.X
⊢ ((fun f ↦ { toFun := fun o ↦ Option.elim o Y.toProd.2 f.toFun, map_fst := ⋯, map_snd := ⋯ })
          ((fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ }) f)).toFun
      (some val✝) =
    f.toFun (some val✝)
Module: Mathlib.RingTheory.Bialgebra.TensorProduct

Goal state before:
pp: case hb
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Bialgebra R A
inst✝ : Bialgebra R B
a : B
⊢ ((AlgHom.restrictScalars R
            ((Algebra.TensorProduct.map ↑(Algebra.TensorProduct.comm R A B) ↑(Algebra.TensorProduct.comm R A B)).comp
              (comulAlgHom R (A ⊗[R] B)))).comp
        Algebra.TensorProduct.includeRight)
      a =
    ((AlgHom.restrictScalars R ((comulAlgHom R (B ⊗[R] A)).comp ↑(Algebra.TensorProduct.comm R A B))).comp
        Algebra.TensorProduct.includeRight)
      a

Tactic:
·

Goal state after:
case hb
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring S
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Bialgebra R A
inst✝ : Bialgebra R B
a : B
⊢ ((AlgHom.restrictScalars R
            ((Algebra.TensorProduct.map ↑(Algebra.TensorProduct.comm R A B) ↑(Algebra.TensorProduct.comm R A B)).comp
              (comulAlgHom R (A ⊗[R] B)))).comp
        Algebra.TensorProduct.includeRight)
      a =
    ((AlgHom.restrictScalars R ((comulAlgHom R (B ⊗[R] A)).comp ↑(Algebra.TensorProduct.comm R A B))).comp
        Algebra.TensorProduct.includeRight)
      a
Module: Mathlib.CategoryTheory.Category.Bipointed

Goal state before:
pp: case none
X : Pointed
Y : Bipointed
f : pointedToBipointedSnd.obj X ⟶ Y
⊢ ((fun f ↦ { toFun := fun o ↦ Option.elim o Y.toProd.1 f.toFun, map_fst := ⋯, map_snd := ⋯ })
          ((fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ }) f)).toFun
      none =
    f.toFun none

pp: case some
X : Pointed
Y : Bipointed
f : pointedToBipointedSnd.obj X ⟶ Y
val✝ : X.X
⊢ ((fun f ↦ { toFun := fun o ↦ Option.elim o Y.toProd.1 f.toFun, map_fst := ⋯, map_snd := ⋯ })
          ((fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ }) f)).toFun
      (some val✝) =
    f.toFun (some val✝)

Tactic:
·

Goal state after:
case none
X : Pointed
Y : Bipointed
f : pointedToBipointedSnd.obj X ⟶ Y
⊢ ((fun f ↦ { toFun := fun o ↦ Option.elim o Y.toProd.1 f.toFun, map_fst := ⋯, map_snd := ⋯ })
          ((fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ }) f)).toFun
      none =
    f.toFun none
Module: Mathlib.CategoryTheory.Category.Bipointed

Goal state before:
pp: case some
X : Pointed
Y : Bipointed
f : pointedToBipointedSnd.obj X ⟶ Y
val✝ : X.X
⊢ ((fun f ↦ { toFun := fun o ↦ Option.elim o Y.toProd.1 f.toFun, map_fst := ⋯, map_snd := ⋯ })
          ((fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ }) f)).toFun
      (some val✝) =
    f.toFun (some val✝)

Tactic:
·

Goal state after:
case some
X : Pointed
Y : Bipointed
f : pointedToBipointedSnd.obj X ⟶ Y
val✝ : X.X
⊢ ((fun f ↦ { toFun := fun o ↦ Option.elim o Y.toProd.1 f.toFun, map_fst := ⋯, map_snd := ⋯ })
          ((fun f ↦ { toFun := f.toFun ∘ some, map_point := ⋯ }) f)).toFun
      (some val✝) =
    f.toFun (some val✝)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: case succ.mp
R : Type u_2
inst✝² : CommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a : R
ha : Irreducible a
n : ℕ
ih : ∀ {b : R}, b ≠ 0 → (a ^ n ∣ b ↔ replicate n (normalize a) ≤ normalizedFactors b)
b : R
hb : b ≠ 0
⊢ a ^ (n + 1) ∣ b → replicate (n + 1) (normalize a) ≤ normalizedFactors b

pp: case succ.mpr
R : Type u_2
inst✝² : CommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a : R
ha : Irreducible a
n : ℕ
ih : ∀ {b : R}, b ≠ 0 → (a ^ n ∣ b ↔ replicate n (normalize a) ≤ normalizedFactors b)
b : R
hb : b ≠ 0
⊢ replicate (n + 1) (normalize a) ≤ normalizedFactors b → a ^ (n + 1) ∣ b

Tactic:
·

Goal state after:
case succ.mp
R : Type u_2
inst✝² : CommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a : R
ha : Irreducible a
n : ℕ
ih : ∀ {b : R}, b ≠ 0 → (a ^ n ∣ b ↔ replicate n (normalize a) ≤ normalizedFactors b)
b : R
hb : b ≠ 0
⊢ a ^ (n + 1) ∣ b → replicate (n + 1) (normalize a) ≤ normalizedFactors b
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: case succ.mpr
R : Type u_2
inst✝² : CommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a : R
ha : Irreducible a
n : ℕ
ih : ∀ {b : R}, b ≠ 0 → (a ^ n ∣ b ↔ replicate n (normalize a) ≤ normalizedFactors b)
b : R
hb : b ≠ 0
⊢ replicate (n + 1) (normalize a) ≤ normalizedFactors b → a ^ (n + 1) ∣ b

Tactic:
·

Goal state after:
case succ.mpr
R : Type u_2
inst✝² : CommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a : R
ha : Irreducible a
n : ℕ
ih : ∀ {b : R}, b ≠ 0 → (a ^ n ∣ b ↔ replicate n (normalize a) ≤ normalizedFactors b)
b : R
hb : b ≠ 0
⊢ replicate (n + 1) (normalize a) ≤ normalizedFactors b → a ^ (n + 1) ∣ b
Module: Mathlib.Algebra.Category.CoalgCat.ComonEquivalence

Goal state before:
pp: R : Type u
inst✝ : CommRing R
X : CoalgCat R
⊢ ModuleCat.Hom.hom
      (ModuleCat.ofHom CoalgebraStruct.comul ≫ ModuleCat.of R ↑X.toModuleCat ◁ ModuleCat.ofHom CoalgebraStruct.comul) =
    ModuleCat.Hom.hom
      (ModuleCat.ofHom CoalgebraStruct.comul ≫
        ModuleCat.ofHom CoalgebraStruct.comul ▷ ModuleCat.of R ↑X.toModuleCat ≫
          (α_ (ModuleCat.of R ↑X.toModuleCat) (ModuleCat.of R ↑X.toModuleCat) (ModuleCat.of R ↑X.toModuleCat)).hom)

Tactic:
simp_rw [ModuleCat.of_coe]; exact Coalgebra.coassoc.symm

Goal state after: