mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
inst✝ : Category.{v₄, u₄} D
F₁ : A ⥤ C
U₁ : C ⥤ A
F₂ : B ⥤ D
U₂ : D ⥤ B
L₁ : A ⥤ B
R₁ : B ⥤ A
L₂ : C ⥤ D
R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : F₁ ⊣ U₁
adj₄ : F₂ ⊣ U₂
α : TwoSquare F₁ L₁ L₂ F₂
d : D
⊢ ((mateEquiv adj₄ adj₃) ((mateEquiv adj₁ adj₂) α)).natTrans.app d =
    ((conjugateEquiv (adj₁.comp adj₄) (adj₃.comp adj₂)) α).app d

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
x✝ : A
⊢ (comul ∘ₗ inl R A B) x✝ = (TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
inst✝ : Category.{v₄, u₄} D
F₁ : A ⥤ C
U₁ : C ⥤ A
F₂ : B ⥤ D
U₂ : D ⥤ B
L₁ : A ⥤ B
R₁ : B ⥤ A
L₂ : C ⥤ D
R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : F₁ ⊣ U₁
adj₄ : F₂ ⊣ U₂
α : TwoSquare U₂ R₂ R₁ U₁
X✝ : A
⊢ ((mateEquiv adj₁ adj₂).symm ((mateEquiv adj₄ adj₃).symm α)).natTrans.app X✝ =
    (((conjugateEquiv (adj₁.comp adj₄) (adj₃.comp adj₂)).symm.trans (equivNatTrans F₁ L₁ L₂ F₂).symm) α).natTrans.app X✝

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
x✝ : B
⊢ (comul ∘ₗ inr R A B) x✝ = (TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
inst✝ : Category.{v₄, u₄} D
G : A ⥤ C
H : B ⥤ D
L₁ : A ⥤ B
R₁ : B ⥤ A
L₂ : C ⥤ D
R₂ : D ⥤ C
L₃ : C ⥤ D
R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : TwoSquare G L₁ L₂ H
β : L₃ ⟶ L₂
⊢ (mateEquiv adj₁ adj₃) (α.whiskerRight β) = ((mateEquiv adj₁ adj₂) α).whiskerBottom ((conjugateEquiv adj₂ adj₃) β)

Tactic:
ext b

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
inst✝ : Category.{v₄, u₄} D
G : A ⥤ C
H : B ⥤ D
L₁ : A ⥤ B
R₁ : B ⥤ A
L₂ : C ⥤ D
R₂ : D ⥤ C
L₃ : C ⥤ D
R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : TwoSquare G L₁ L₂ H
β : L₃ ⟶ L₂
b : B
⊢ ((mateEquiv adj₁ adj₃) (α.whiskerRight β)).natTrans.app b =
    (((mateEquiv adj₁ adj₂) α).whiskerBottom ((conjugateEquiv adj₂ adj₃) β)).natTrans.app b
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: case h1
R : Type u
M : Type v
inst✝³ : DivisionSemiring R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
x : tsze R M
hx : x.fst ≠ 0
⊢ x⁻¹.fst = (inl x.fst⁻¹ + inr (-(x.fst⁻¹ •> x.snd <• x.fst⁻¹))).fst

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: case h2
R : Type u
M : Type v
inst✝³ : DivisionSemiring R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
x : tsze R M
hx : x.fst ≠ 0
⊢ x⁻¹.snd = (inl x.fst⁻¹ + inr (-(x.fst⁻¹ •> x.snd <• x.fst⁻¹))).snd

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
inst✝ : Category.{v₄, u₄} D
G : A ⥤ C
H : B ⥤ D
L₁ : A ⥤ B
R₁ : B ⥤ A
L₂ : A ⥤ B
R₂ : B ⥤ A
L₃ : C ⥤ D
R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : L₂ ⟶ L₁
β : TwoSquare G L₂ L₃ H
⊢ (mateEquiv adj₁ adj₃) (β.whiskerLeft α) = ((mateEquiv adj₂ adj₃) β).whiskerTop ((conjugateEquiv adj₁ adj₂) α)

Tactic:
ext b

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
inst✝ : Category.{v₄, u₄} D
G : A ⥤ C
H : B ⥤ D
L₁ : A ⥤ B
R₁ : B ⥤ A
L₂ : A ⥤ B
R₂ : B ⥤ A
L₃ : C ⥤ D
R₃ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : L₂ ⟶ L₁
β : TwoSquare G L₂ L₃ H
b : B
⊢ ((mateEquiv adj₁ adj₃) (β.whiskerLeft α)).natTrans.app b =
    (((mateEquiv adj₂ adj₃) β).whiskerTop ((conjugateEquiv adj₁ adj₂) α)).natTrans.app b
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
x✝ : B
⊢ (counit ∘ₗ inr R A B) x✝ = counit x✝

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
x✝ : A
⊢ (counit ∘ₗ inl R A B) x✝ = counit x✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
inst✝ : Category.{v₄, u₄} D
L₀₁ : A ⥤ B
R₁₀ : B ⥤ A
L₁₂ : B ⥤ C
R₂₁ : C ⥤ B
L₂₃ : C ⥤ D
R₃₂ : D ⥤ C
adj₀₁ : L₀₁ ⊣ R₁₀
adj₁₂ : L₁₂ ⊣ R₂₁
adj₂₃ : L₂₃ ⊣ R₃₂
X : D
⊢ adj₀₁.unit.app (R₁₀.obj (R₂₁.obj (R₃₂.obj X))) ≫
      R₁₀.map
        (adj₁₂.unit.app (L₀₁.obj (R₁₀.obj (R₂₁.obj (R₃₂.obj X)))) ≫
          R₂₁.map
            (adj₂₃.unit.app (L₁₂.obj (L₀₁.obj (R₁₀.obj (R₂₁.obj (R₃₂.obj X))))) ≫
              R₃₂.map
                (L₂₃.map (L₁₂.map (adj₀₁.counit.app (R₂₁.obj (R₃₂.obj X)))) ≫
                  L₂₃.map (adj₁₂.counit.app (R₃₂.obj X)) ≫ adj₂₃.counit.app X))) =
    𝟙 (R₁₀.obj (R₂₁.obj (R₃₂.obj X)))

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝² : Category.{v₁, u₁} A
inst✝¹ : Category.{v₂, u₂} B
inst✝ : Category.{v₃, u₃} C
L₁ L₂ : A ⥤ B
R₁ R₂ : B ⥤ A
L : B ⥤ C
R : C ⥤ B
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj : L ⊣ R
τ : L₂ ⟶ L₁
X : C
⊢ adj₂.unit.app (R₁.obj (R.obj X)) ≫
      R₂.map
        (adj.unit.app (L₂.obj (R₁.obj (R.obj X))) ≫
          R.map (L.map (τ.app (R₁.obj (R.obj X))) ≫ L.map (adj₁.counit.app (R.obj X)) ≫ adj.counit.app X)) =
    adj₂.unit.app (R₁.obj (R.obj X)) ≫ R₂.map (τ.app (R₁.obj (R.obj X)) ≫ adj₁.counit.app (R.obj X))

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.Hom

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝¹² : CommSemiring R
inst✝¹¹ : AddCommMonoid A
inst✝¹⁰ : Module R A
inst✝⁹ : AddCommMonoid B
inst✝⁸ : Module R B
inst✝⁷ : AddCommMonoid C
inst✝⁶ : Module R C
inst✝⁵ : AddCommMonoid D
inst✝⁴ : Module R D
inst✝³ : CoalgebraStruct R A
inst✝² : CoalgebraStruct R B
inst✝¹ : CoalgebraStruct R C
inst✝ : CoalgebraStruct R D
φ₁ : B →ₗc[R] C
φ₂ : A →ₗc[R] B
x✝ : A
⊢ (counit ∘ₗ ↑φ₁ ∘ₗ ↑φ₂) x✝ = counit x✝

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.Hom

Goal state before:
pp: R : Type u
A : Type v
B : Type w
ι : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : Module R A
inst✝² : Module R B
inst✝¹ : Coalgebra R A
inst✝ : Coalgebra R B
x✝ : A
⊢ (counit ∘ₗ counit) x✝ = counit x✝

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ (((LinearMap.mul R R).compr₂ CoalgebraStruct.counit) 1) 1 =
    (((LinearMap.mul R R).compl₁₂ CoalgebraStruct.counit CoalgebraStruct.counit) 1) 1

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ (((LinearMap.mul R R).compr₂ CoalgebraStruct.comul) 1) 1 =
    (((LinearMap.mul R (R ⊗[R] R)).compl₁₂ CoalgebraStruct.comul CoalgebraStruct.comul) 1) 1

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
ι : Type v
A : ι → Type w
inst✝⁴ : DecidableEq ι
inst✝³ : CommSemiring R
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : (i : ι) → Module R (A i)
inst✝ : (i : ι) → CoalgebraStruct R (A i)
i : ι
x✝ : A i
⊢ (comul ∘ₗ lsingle i) x✝ = (TensorProduct.map (lsingle i) (lsingle i) ∘ₗ comul) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
ι : Type v
A : ι → Type w
inst✝⁴ : DecidableEq ι
inst✝³ : CommSemiring R
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : (i : ι) → Module R (A i)
inst✝ : (i : ι) → CoalgebraStruct R (A i)
i : ι
x✝ : A i
⊢ (counit ∘ₗ lsingle i) x✝ = counit x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R' : Type u
M : Type v
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R' M
inst✝⁵ : Module R'ᵐᵒᵖ M
inst✝⁴ : IsCentralScalar R' M
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R' N
inst✝¹ : Module R'ᵐᵒᵖ N
inst✝ : IsCentralScalar R' N
f : M →ₗ[R'] N
x : tsze R' M
⊢ ((map f) x).fst = x.fst

Tactic:
by
  simp [map, lift_def, Algebra.ofId_apply, algebraMap_eq_inl]

Goal state after:
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R' : Type u
M : Type v
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R' M
inst✝⁵ : Module R'ᵐᵒᵖ M
inst✝⁴ : IsCentralScalar R' M
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R' N
inst✝¹ : Module R'ᵐᵒᵖ N
inst✝ : IsCentralScalar R' N
f : M →ₗ[R'] N
x : tsze R' M
⊢ ((map f) x).snd = f x.snd

Tactic:
by
  simp [map, lift_def, Algebra.ofId_apply, algebraMap_eq_inl]

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
ι : Type v
A : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : CoalgebraStruct R A
i : ι
x✝ : A
⊢ (comul ∘ₗ lsingle i) x✝ = (TensorProduct.map (lsingle i) (lsingle i) ∘ₗ comul) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
ι : Type v
A : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : CoalgebraStruct R A
i : ι
x✝ : A
⊢ (counit ∘ₗ lsingle i) x✝ = counit x✝

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
A : n → Type u_3
inst✝² : (i : n) → AddCommMonoid (A i)
inst✝¹ : (i : n) → Module R (A i)
inst✝ : (i : n) → CoalgebraStruct R (A i)
i : n
x✝ : A i
⊢ (comul ∘ₗ LinearMap.single R A i) x✝ = (map (LinearMap.single R A i) (LinearMap.single R A i) ∘ₗ comul) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
A : n → Type u_3
inst✝² : (i : n) → AddCommMonoid (A i)
inst✝¹ : (i : n) → Module R (A i)
inst✝ : (i : n) → CoalgebraStruct R (A i)
i : n
x✝ : A i
⊢ (counit ∘ₗ LinearMap.single R A i) x✝ = counit x✝

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.Hom

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A
inst✝¹⁰ : Semiring B
inst✝⁹ : Semiring C
inst✝⁸ : Semiring D
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra R C
inst✝⁴ : Algebra R D
inst✝³ : CoalgebraStruct R A
inst✝² : CoalgebraStruct R B
inst✝¹ : CoalgebraStruct R C
inst✝ : CoalgebraStruct R D
f g : A →ₐc[R] B
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
rcases f with ⟨_, _⟩

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
D : Type u_5
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A
inst✝¹⁰ : Semiring B
inst✝⁹ : Semiring C
inst✝⁸ : Semiring D
inst✝⁷ : Algebra R A
inst✝⁶ : Algebra R B
inst✝⁵ : Algebra R C
inst✝⁴ : Algebra R D
inst✝³ : CoalgebraStruct R A
inst✝² : CoalgebraStruct R B
inst✝¹ : CoalgebraStruct R C
inst✝ : CoalgebraStruct R D
g : A →ₐc[R] B
toCoalgHom✝ : A →ₗc[R] B
map_one'✝ : toCoalgHom✝.toFun 1 = 1
map_mul'✝ : ∀ (x y : A), toCoalgHom✝.toFun (x * y) = toCoalgHom✝.toFun x * toCoalgHom✝.toFun y
h : (fun f ↦ f.toFun) { toCoalgHom := toCoalgHom✝, map_one' := map_one'✝, map_mul' := map_mul'✝ } = (fun f ↦ f.toFun) g
⊢ { toCoalgHom := toCoalgHom✝, map_one' := map_one'✝, map_mul' := map_mul'✝ } = g
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
M : ModuleCat R
N : ModuleCat S
g : ↑M →ₛₗ[f] ↑N
⊢ ∀ (x y : ↑M), g (x + y) = g x + g y

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
M : ModuleCat R
N : ModuleCat S
g : ↑M →ₛₗ[f] ↑N
⊢ ∀ (m : R) (x : ↑M), g (m • x) = (RingHom.id R) m • g x

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
M : ModuleCat R
N : ModuleCat S
g : M ⟶ (restrictScalars f).obj N
⊢ ∀ (x y : ↑M), (ConcreteCategory.hom g) (x + y) = (ConcreteCategory.hom g) x + (ConcreteCategory.hom g) y

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.Equiv

Goal state before:
pp: R : Type u
A : Type v
B : Type w
C : Type u₁
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Bialgebra R A
inst✝ : Bialgebra R B
f : A →ₐc[R] B
hf : Bijective ⇑f
x✝ : A
⊢ ((counitAlgHom R B).comp ↑(AlgEquiv.ofBijective (↑f) hf)) x✝ = (counitAlgHom R A) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.Bialgebra.Equiv

Goal state before:
pp: R : Type u
A : Type v
B : Type w
C : Type u₁
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Bialgebra R A
inst✝ : Bialgebra R B
f : A →ₐc[R] B
hf : Bijective ⇑f
x✝ : A
⊢ ((Algebra.TensorProduct.map ↑(AlgEquiv.ofBijective (↑f) hf) ↑(AlgEquiv.ofBijective (↑f) hf)).comp (comulAlgHom R A))
      x✝ =
    ((comulAlgHom R B).comp ↑(AlgEquiv.ofBijective (↑f) hf)) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝⁵ : CommRing R✝
inst✝⁴ : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝³ : Ring R
inst✝² : Ring S
f : R →+* S
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
g : ↑((restrictScalars f).obj (of S S)) →ₗ[R] M
s : S
⊢ (1 • g) s = g s

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝⁵ : CommRing R✝
inst✝⁴ : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝³ : Ring R
inst✝² : Ring S
f : R →+* S
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝¹ x✝ : S
⊢ (x✝¹ • 0) x✝ = 0 x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝⁵ : CommRing R✝
inst✝⁴ : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝³ : Ring R
inst✝² : Ring S
f : R →+* S
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : S
g h : ↑((restrictScalars f).obj (of S S)) →ₗ[R] M
x✝ : S
⊢ (s • (g + h)) x✝ = (s • g + s • h) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
M✝ : ModuleCat R
M M' : ModuleCat R
g : M ⟶ M'
s : S
h : ↑((restrictScalars f).obj (of S S)) →ₗ[R] ↑M
x✝ : ↑((restrictScalars f).obj (of S S))
⊢ (Hom.hom g ∘ₗ (s • h)) x✝ = ((RingHom.id S) s • Hom.hom g ∘ₗ h) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : (restrictScalars f).obj Y ⟶ X
y1 y2 : ↑Y
s : S
⊢ ((CoextendScalars.equiv f X)
        ((CoextendScalars.equiv f X).symm
          { toFun := fun s ↦ (ConcreteCategory.hom g) (s • (y1 + y2)), map_add' := ⋯, map_smul' := ⋯ }))
      s =
    ((CoextendScalars.equiv f X)
        ((CoextendScalars.equiv f X).symm
            { toFun := fun s ↦ (ConcreteCategory.hom g) (s • y1), map_add' := ⋯, map_smul' := ⋯ } +
          (CoextendScalars.equiv f X).symm
            { toFun := fun s ↦ (ConcreteCategory.hom g) (s • y2), map_add' := ⋯, map_smul' := ⋯ }))
      s

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
X : ModuleCat R
Y : ModuleCat S
g : Y ⟶ (coextendScalars f).obj X
x y : ↑((restrictScalars f).obj Y)
⊢ ((CoextendScalars.equiv f X) ((ConcreteCategory.hom g) (x + y))) 1 =
    ((CoextendScalars.equiv f X) ((ConcreteCategory.hom g) x)) 1 +
      ((CoextendScalars.equiv f X) ((ConcreteCategory.hom g) y)) 1

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
X : ModuleCat R
x1 x2 : ↑((restrictScalars f).obj ((coextendScalars f).obj X))
⊢ ((CoextendScalars.equiv f X) (x1 + x2)) 1 = ((CoextendScalars.equiv f X) x1) 1 + ((CoextendScalars.equiv f X) x2) 1

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: case e_6
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
X : ModuleCat R
r : R
g : ↑((restrictScalars f).obj ((coextendScalars f).obj X))
⊢ f r = r • 1

Tactic:
change f r = f r • (1 : S)

Goal state after:
case e_6
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
X : ModuleCat R
r : R
g : ↑((restrictScalars f).obj ((coextendScalars f).obj X))
⊢ f r = f r • 1
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: case e_6
R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
X : ModuleCat R
r : R
g : ↑((restrictScalars f).obj ((coextendScalars f).obj X))
⊢ f r = f r • 1

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
X : ModuleCat S
Y : ModuleCat R
g : (restrictScalars f).obj X ⟶ Y
x✝ : ↑((restrictScalars f).obj X)
⊢ (Hom.hom
        (RestrictionCoextensionAdj.HomEquiv.toRestriction f (RestrictionCoextensionAdj.HomEquiv.fromRestriction f g)))
      x✝ =
    (Hom.hom g) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R✝ : Type u₁
S✝ : Type u₂
inst✝³ : CommRing R✝
inst✝² : CommRing S✝
f✝ : R✝ →+* S✝
R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
X : ModuleCat S
Y : ModuleCat R
g : X ⟶ (coextendScalars f).obj Y
x✝¹ : ↑X
x✝ : ↑((restrictScalars f).obj (of S S))
⊢ ((CoextendScalars.equiv f Y)
        ((Hom.hom
            (RestrictionCoextensionAdj.HomEquiv.fromRestriction f
              (RestrictionCoextensionAdj.HomEquiv.toRestriction f g)))
          x✝¹))
      x✝ =
    ((CoextendScalars.equiv f Y) ((Hom.hom g) x✝¹)) x✝

Tactic:
simp

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

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: 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
x x' : ↑X
⊢ 1 ⊗ₜ[R] (x + x') = 1 ⊗ₜ[R] x + 1 ⊗ₜ[R] x'

Tactic:
by dsimp; rw [TensorProduct.tmul_add]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
Y : ModuleCat S
y : ↑Y
⊢ 1 • y = y

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R : Type u₁
inst✝ : CommRing R
M : ModuleCat R
m : ↑M
⊢ (ConcreteCategory.hom ((extendScalarsId R).inv.app M ≫ (extendScalarsId R).hom.app M)) m =
    (Hom.hom ((restrictScalarsId R).inv.app M)) m

Tactic:
simp

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

Goal state before:
pp: case e'_2.tmul.tmul
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
x₁ x₂ : A
y₁ y₂ : B
⊢ (counit y₁ • counit x₁) • x₂ ⊗ₜ[R] y₂ = 1 • (counit x₁ • x₂) ⊗ₜ[R] (counit y₁ • y₂)

Tactic:
rw [tmul_smul, smul_assoc, one_smul, smul_tmul']

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

Goal state before:
pp: case e'_2.tmul.tmul
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
x₁ x₂ : A
y₁ y₂ : B
⊢ (counit y₂ • counit x₂) • x₁ ⊗ₜ[R] y₁ = 1 • (counit x₂ • x₁) ⊗ₜ[R] (counit y₂ • y₁)

Tactic:
rw [tmul_smul, smul_assoc, one_smul, smul_tmul']

Goal state after: