mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.Transport

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategoryStruct D
F : D ⥤ C
inst✝ : F.Faithful
fData : InducingFunctorData F
this : MonoidalCategory D := induced F fData
X✝ Y✝ : D
x✝ : X✝ ⟶ Y✝
⊢ ∀ (X' : D), F.map x✝ ▷ F.obj X' ≫ (fData.μIso Y✝ X').hom = (fData.μIso X✝ X').hom ≫ F.map (x✝ ▷ X')

Tactic:
by simp [fData.whiskerRight_eq]

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.Rat

Goal state before:
pp: M : Type u_1
M₂ : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module ℚ M
inst✝¹ : AddCommGroup M₂
inst✝ : Module ℚ M₂
f g : M →+ M₂
h : f.toRatLinearMap = g.toRatLinearMap
⊢ f = g

Tactic:
ext x

Goal state after:
M : Type u_1
M₂ : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module ℚ M
inst✝¹ : AddCommGroup M₂
inst✝ : Module ℚ M₂
f g : M →+ M₂
h : f.toRatLinearMap = g.toRatLinearMap
x : M
⊢ f x = g x
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
inst✝¹ : MonoidalCategory E
C' : Type u₁'
inst✝ : Category.{v₁', u₁'} C'
F : C ⥤ D
h : F.CoreMonoidal
X Y Z : C
⊢ (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom =
    (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom ≫ F.obj X ◁ (h.μIso Y Z).hom ≫ F.obj X ◁ (h.μIso Y Z).inv

Tactic:
whiskerLeft_hom_inv,

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
inst✝¹ : MonoidalCategory E
C' : Type u₁'
inst✝ : Category.{v₁', u₁'} C'
F : C ⥤ D
h : F.CoreMonoidal
X Y Z : C
⊢ (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom = (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom ≫ 𝟙 (F.obj X ⊗ F.obj Y ⊗ F.obj Z)
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X Y : D
f : X ⟶ Y
X' : D
⊢ G.map f ▷ G.obj X' ≫
      (adj.homEquiv (G.obj Y ⊗ G.obj X') (Y ⊗ X'))
        (δ F (G.obj Y) (G.obj X') ≫ (adj.counit.app Y ⊗ₘ adj.counit.app X')) =
    (adj.homEquiv (G.obj X ⊗ G.obj X') (X ⊗ X')) (δ F (G.obj X) (G.obj X') ≫ (adj.counit.app X ⊗ₘ adj.counit.app X')) ≫
      G.map (f ▷ X')

Tactic:
by
    simp only [Adjunction.homEquiv_apply, ← adj.unit_naturality_assoc, ← G.map_comp, assoc,
      ← δ_natural_left_assoc F]
    suffices F.map (G.map f) ▷ F.obj (G.obj X') ≫ _ =
      (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ _ by rw [this]
    simpa using NatTrans.whiskerRight_app_tensor_app adj.counit adj.counit (f := f) X'

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Concrete

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
f g : Arrow (Type u)
φ : f ⟶ g
⊢ (Arrow.leftFunc.map φ ≫ ↾fun x ↦ ⟨(hom g.hom) x, ⋯⟩) =
    (↾fun x ↦ ⟨(hom f.hom) x, ⋯⟩) ≫
      { obj := fun f ↦ ↑(Set.range ⇑(TypeCat.Hom.hom f.hom)),
            map := fun {X Y} φ ↦ ↾fun y ↦ ⟨(hom (Arrow.Hom.right φ)) ↑y, ⋯⟩,
            map_id := functorialSurjectiveInjectiveFactorizationData._proof_2,
            map_comp := @functorialSurjectiveInjectiveFactorizationData._proof_3 }.map
        φ

Tactic:
ext x

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type u_2
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
f g : Arrow (Type u)
φ : f ⟶ g
x : Arrow.leftFunc.obj f
⊢ ↑((hom (Arrow.leftFunc.map φ ≫ ↾fun x ↦ ⟨(hom g.hom) x, ⋯⟩)).toFun x) =
    ↑((hom
            ((↾fun x ↦ ⟨(hom f.hom) x, ⋯⟩) ≫
              { obj := fun f ↦ ↑(Set.range ⇑(TypeCat.Hom.hom f.hom)),
                    map := fun {X Y} φ ↦ ↾fun y ↦ ⟨(hom (Arrow.Hom.right φ)) ↑y, ⋯⟩,
                    map_id := functorialSurjectiveInjectiveFactorizationData._proof_2,
                    map_comp := @functorialSurjectiveInjectiveFactorizationData._proof_3 }.map
                φ)).toFun
        x)
Module: Mathlib.Algebra.Category.ModuleCat.EpiMono

Goal state before:
pp: R : Type u
inst✝ : Ring R
X Y : ModuleCat R
f : X ⟶ Y
⊢ Mono f ↔ Function.Injective ⇑(ConcreteCategory.hom f)

Tactic:
rw [mono_iff_ker_eq_bot, LinearMap.ker_eq_bot]

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
h : Function.Bijective ⇑(Quot.desc F c)
s : Cocone F
j : J
⊢ c.ι.app j ≫ ofHom ((Quot.desc F s).comp (AddEquiv.ofBijective (Quot.desc F c) h).symm.toAddMonoidHom) = s.ι.app j

Tactic:
ext x

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
h : Function.Bijective ⇑(Quot.desc F c)
s : Cocone F
j : J
x : ↑(F.obj j)
⊢ (Hom.hom (c.ι.app j ≫ ofHom ((Quot.desc F s).comp (AddEquiv.ofBijective (Quot.desc F c) h).symm.toAddMonoidHom))) x =
    (Hom.hom (s.ι.app j)) x
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
h : Function.Bijective ⇑(Quot.desc F c)
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
⊢ m = ofHom ((Quot.desc F s).comp (AddEquiv.ofBijective (Quot.desc F c) h).symm.toAddMonoidHom)

Tactic:
ext x

Goal state after:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
h : Function.Bijective ⇑(Quot.desc F c)
s : Cocone F
m : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ m = s.ι.app j
x : ↑c.pt
⊢ (Hom.hom m) x =
    (Hom.hom (ofHom ((Quot.desc F s).comp (AddEquiv.ofBijective (Quot.desc F c) h).symm.toAddMonoidHom))) x
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: G H : AddCommGrpCat
f : G ⟶ H
⊢ f ≫ ofHom (mk' (Hom.hom f).range) = 0

Tactic:
ext x

Goal state after:
G H : AddCommGrpCat
f : G ⟶ H
x : ↑G
⊢ (Hom.hom (f ≫ ofHom (mk' (Hom.hom f).range))) x = (Hom.hom 0) x
Module: Mathlib.Algebra.Category.Grp.Colimits

Goal state before:
pp: G H : AddCommGrpCat
f : G ⟶ H
⊢ ofHom (lift (Hom.hom f).range (Hom.hom (cokernel.π f)) ⋯) ≫ cokernel.desc f (ofHom (mk' (Hom.hom f).range)) ⋯ =
    𝟙 (of (↑H ⧸ (Hom.hom f).range))

Tactic:
ext x

Goal state after:
G H : AddCommGrpCat
f : G ⟶ H
x : ↑H
⊢ ((Hom.hom
            (ofHom (lift (Hom.hom f).range (Hom.hom (cokernel.π f)) ⋯) ≫
              cokernel.desc f (ofHom (mk' (Hom.hom f).range)) ⋯)).comp
        (mk' (Hom.hom f).range))
      x =
    ((Hom.hom (𝟙 (of (↑H ⧸ (Hom.hom f).range)))).comp (mk' (Hom.hom f).range)) x
Module: Mathlib.RingTheory.Congruence.Hom

Goal state before:
pp: case mk.mk
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : NonAssocSemiring M
inst✝¹ : NonAssocSemiring N
inst✝ : NonAssocSemiring P
c✝ d✝ c : RingCon M
d : RingCon N
e : M ≃+* N
h : c = d.comap e
x✝ : c.Quotient
x : M
y✝ : c.Quotient
y : M
⊢ (Quotient.congr ↑e ⋯).toFun (Quot.mk (⇑c.toSetoid) x * Quot.mk (⇑c.toSetoid) y) =
    (Quotient.congr ↑e ⋯).toFun (Quot.mk (⇑c.toSetoid) x) * (Quotient.congr ↑e ⋯).toFun (Quot.mk (⇑c.toSetoid) y)

Tactic:
exact congrArg toQuotient (e.map_mul x y)

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : NonAssocSemiring M
inst✝ : NonAssocSemiring N
c : RingCon M
f : M →+* N
h : ker f ≤ c
hf : Surjective ⇑f
x y : M
x✝ : ∃ a b, c a b ∧ f a = f x ∧ f b = f y
a b : M
h₁ : c a b
h₂ : f a = f x
h₃ : f b = f y
⊢ c x y

Tactic:
exact c.trans (h h₂.symm) <| c.trans h₁ <| h h₃

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : NonAssocSemiring M
inst✝ : NonAssocSemiring N
c : RingCon M
f : M →+* N
h : ker f ≤ c
hf : Surjective ⇑f
x y : M
⊢ (mapGen ⇑f) (f x) (f y) ↔ c x y

Tactic:
rw [mapGen_eq_map_of_surjective f h hf, Relation.map_apply]
  refine ⟨fun ⟨a, b, h₁, h₂, h₃⟩ ↦ ?_, by grind⟩
  exact c.trans (h h₂.symm) <| c.trans h₁ <| h h₃

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

Goal state before:
pp: M : Type u_1
P : Type u_3
inst✝¹ : NonAssocSemiring M
inst✝ : NonAssocSemiring P
c : RingCon M
f : c.Quotient →+* P
⊢ c.lift (f.comp c.mk') ⋯ = f

Tactic:
ext x

Goal state after:
M : Type u_1
P : Type u_3
inst✝¹ : NonAssocSemiring M
inst✝ : NonAssocSemiring P
c : RingCon M
f : c.Quotient →+* P
x : c.Quotient
⊢ (c.lift (f.comp c.mk') ⋯) x = f x
Module: Mathlib.RingTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : NonAssocSemiring M
inst✝¹ : NonAssocSemiring N
inst✝ : NonAssocSemiring P
c✝ : RingCon M
f : M →+* P
c d : RingCon M
h : c ≤ d
x y : (ker (c.map d h)).Quotient
w z : c.Quotient
a b : M
⊢ (c.quotientQuotientEquivQuotient d.toSetoid h).toFun (↑↑a * ↑↑b) = d.mk' a * d.mk' b

Tactic:
rw [← d.mk'.map_mul]; rfl

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n : ℕ
h : x.snd <• x.fst = x.fst •> x.snd
⊢ [].sum = 0

Tactic:
List.sum_nil

Goal state after:
R : Type u
M : Type v
inst✝⁴ : Monoid R
inst✝³ : AddMonoid M
inst✝² : DistribMulAction R M
inst✝¹ : DistribMulAction Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
n : ℕ
h : x.snd <• x.fst = x.fst •> x.snd
⊢ 0 = 0
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : AddCommGroup M
inst✝³ : Semiring R
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
r : R
⊢ IsUnit (inl r) ↔ IsUnit r

Tactic:
by
  rw [isUnit_iff_isUnit_fst, fst_inl]

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₂ : B ⥤ C
R₁ R₂ : C ⥤ B
L : A ⥤ B
R : B ⥤ A
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj : L ⊣ R
τ : L₂ ⟶ L₁
X : C
h₁ :
  (R₂ ⋙ R).map (L₂.map (adj.counit.app (R₁.obj X)) ≫ τ.app ((𝟭 B).obj (R₁.obj X))) =
    (R₂ ⋙ R).map (τ.app ((R ⋙ L).obj (R₁.obj X)) ≫ L₁.map (adj.counit.app (R₁.obj X)))
⊢ ((conjugateEquiv (adj.comp adj₁) (adj.comp adj₂)) (L.whiskerLeft τ)).app X =
    (whiskerRight ((conjugateEquiv adj₁ adj₂) τ) R).app X

Tactic:
have h₂ := congr_map R (adj₂.unit_naturality (adj.counit.app (R₁.obj X)))

Goal state after:
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₂ : B ⥤ C
R₁ R₂ : C ⥤ B
L : A ⥤ B
R : B ⥤ A
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj : L ⊣ R
τ : L₂ ⟶ L₁
X : C
h₁ :
  (R₂ ⋙ R).map (L₂.map (adj.counit.app (R₁.obj X)) ≫ τ.app ((𝟭 B).obj (R₁.obj X))) =
    (R₂ ⋙ R).map (τ.app ((R ⋙ L).obj (R₁.obj X)) ≫ L₁.map (adj.counit.app (R₁.obj X)))
h₂ :
  R.map (adj₂.unit.app ((R ⋙ L).obj (R₁.obj X)) ≫ R₂.map (L₂.map (adj.counit.app (R₁.obj X)))) =
    R.map (adj.counit.app (R₁.obj X) ≫ adj₂.unit.app ((𝟭 B).obj (R₁.obj X)))
⊢ ((conjugateEquiv (adj.comp adj₁) (adj.comp adj₂)) (L.whiskerLeft τ)).app X =
    (whiskerRight ((conjugateEquiv adj₁ adj₂) τ) R).app X
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : DivisionSemiring R
inst✝³ : AddCommGroup M
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
⊢ IsUnit x.fst⁻¹ ↔ IsUnit x.fst

Tactic:
isUnit_iff_ne_zero,

Goal state after:
R : Type u
M : Type v
inst✝⁴ : DivisionSemiring R
inst✝³ : AddCommGroup M
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
⊢ x.fst⁻¹ ≠ 0 ↔ x.fst ≠ 0
Module: Mathlib.RingTheory.Coalgebra.Equiv

Goal state before:
pp: case e_f
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : Module R A
inst✝³ : Coalgebra R A
inst✝² : AddCommMonoid B
inst✝¹ : Module R B
inst✝ : CoalgebraStruct R B
f : A ≃ₗc[R] B
⊢ ((↑(TensorProduct.assoc R B B B) ∘ₗ
          LinearMap.rTensor B ((TensorProduct.map f.toLinearMap f.toLinearMap ∘ₗ comul) ∘ₗ ↑f.toLinearEquiv.symm)) ∘ₗ
        TensorProduct.map f.toLinearMap f.toLinearMap) ∘ₗ
      comul =
    (LinearMap.lTensor B ((TensorProduct.map f.toLinearMap f.toLinearMap ∘ₗ comul) ∘ₗ ↑f.toLinearEquiv.symm) ∘ₗ
        TensorProduct.map f.toLinearMap f.toLinearMap) ∘ₗ
      comul

Tactic:
ext x

Goal state after:
case e_f
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : Module R A
inst✝³ : Coalgebra R A
inst✝² : AddCommMonoid B
inst✝¹ : Module R B
inst✝ : CoalgebraStruct R B
f : A ≃ₗc[R] B
x : A
⊢ (((↑(TensorProduct.assoc R B B B) ∘ₗ
            LinearMap.rTensor B ((TensorProduct.map f.toLinearMap f.toLinearMap ∘ₗ comul) ∘ₗ ↑f.toLinearEquiv.symm)) ∘ₗ
          TensorProduct.map f.toLinearMap f.toLinearMap) ∘ₗ
        comul)
      x =
    ((LinearMap.lTensor B ((TensorProduct.map f.toLinearMap f.toLinearMap ∘ₗ comul) ∘ₗ ↑f.toLinearEquiv.symm) ∘ₗ
          TensorProduct.map f.toLinearMap f.toLinearMap) ∘ₗ
        comul)
      x
Module: Mathlib.RingTheory.Coalgebra.Equiv

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : Module R A
inst✝³ : Coalgebra R A
inst✝² : AddCommMonoid B
inst✝¹ : Module R B
inst✝ : CoalgebraStruct R B
f : A ≃ₗc[R] B
⊢ (LinearMap.rTensor B (counit ∘ₗ ↑f.toLinearEquiv.symm) ∘ₗ TensorProduct.map f.toLinearMap f.toLinearMap) ∘ₗ comul =
    (TensorProduct.mk R R B) 1 ∘ₗ f.toLinearMap

Tactic:
ext x

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : Module R A
inst✝³ : Coalgebra R A
inst✝² : AddCommMonoid B
inst✝¹ : Module R B
inst✝ : CoalgebraStruct R B
f : A ≃ₗc[R] B
x : A
⊢ ((LinearMap.rTensor B (counit ∘ₗ ↑f.toLinearEquiv.symm) ∘ₗ TensorProduct.map f.toLinearMap f.toLinearMap) ∘ₗ comul)
      x =
    ((TensorProduct.mk R R B) 1 ∘ₗ f.toLinearMap) x
Module: Mathlib.RingTheory.Coalgebra.Equiv

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : Module R A
inst✝³ : Coalgebra R A
inst✝² : AddCommMonoid B
inst✝¹ : Module R B
inst✝ : CoalgebraStruct R B
f : A ≃ₗc[R] B
⊢ (LinearMap.lTensor B (counit ∘ₗ ↑f.toLinearEquiv.symm) ∘ₗ TensorProduct.map f.toLinearMap f.toLinearMap) ∘ₗ comul =
    (TensorProduct.mk R B R).flip 1 ∘ₗ f.toLinearMap

Tactic:
ext x

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : Module R A
inst✝³ : Coalgebra R A
inst✝² : AddCommMonoid B
inst✝¹ : Module R B
inst✝ : CoalgebraStruct R B
f : A ≃ₗc[R] B
x : A
⊢ ((LinearMap.lTensor B (counit ∘ₗ ↑f.toLinearEquiv.symm) ∘ₗ TensorProduct.map f.toLinearMap f.toLinearMap) ∘ₗ comul)
      x =
    ((TensorProduct.mk R B R).flip 1 ∘ₗ f.toLinearMap) x
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
X✝ Y✝ : ModuleCat S
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : (restrictScalars f).map a₁✝ = (restrictScalars f).map a₂✝
⊢ a₁✝ = a₂✝

Tactic:
ext x

Goal state after:
R : Type u₁
S : Type u₂
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
X✝ Y✝ : ModuleCat S
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : (restrictScalars f).map a₁✝ = (restrictScalars f).map a₂✝
x : ↑X✝
⊢ (Hom.hom a₁✝) x = (Hom.hom a₂✝) x
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
M₁ M₂ M₃ : ModuleCat R
l₁₂ : M₁ ⟶ M₂
l₂₃ : M₂ ⟶ M₃
⊢ map' f (l₁₂ ≫ l₂₃) = map' f l₁₂ ≫ map' f l₂₃

Tactic:
ext x

Goal state after:
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M₁ M₂ M₃ : ModuleCat R
l₁₂ : M₁ ⟶ M₂
l₂₃ : M₂ ⟶ M₃
x : ↑(obj' f M₁)
⊢ (Hom.hom (map' f (l₁₂ ≫ l₂₃))) x = (Hom.hom (map' f l₁₂ ≫ map' f l₂₃)) x
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: case add
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M₁ M₂ M₃ : ModuleCat R
l₁₂ : M₁ ⟶ M₂
l₂₃ : M₂ ⟶ M₃
x✝ y✝ : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑M₁
ihx : (Hom.hom (map' f (l₁₂ ≫ l₂₃))) x✝ = (Hom.hom (map' f l₁₂ ≫ map' f l₂₃)) x✝
ihy : (Hom.hom (map' f (l₁₂ ≫ l₂₃))) y✝ = (Hom.hom (map' f l₁₂ ≫ map' f l₂₃)) y✝
⊢ (Hom.hom (map' f (l₁₂ ≫ l₂₃))) (x✝ + y✝) = (Hom.hom (map' f l₁₂ ≫ map' f l₂₃)) (x✝ + y✝)

Tactic:
erw [LinearMap.map_add, LinearMap.map_add]

Goal state after:
case add
R : Type u₁
S : Type u₂
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M₁ M₂ M₃ : ModuleCat R
l₁₂ : M₁ ⟶ M₂
l₂₃ : M₂ ⟶ M₃
x✝ y✝ : ↑((restrictScalars f).obj (of S S)) ⊗[R] ↑M₁
ihx : (Hom.hom (map' f (l₁₂ ≫ l₂₃))) x✝ = (Hom.hom (map' f l₁₂ ≫ map' f l₂₃)) x✝
ihy : (Hom.hom (map' f (l₁₂ ≫ l₂₃))) y✝ = (Hom.hom (map' f l₁₂ ≫ map' f l₂₃)) y✝
⊢ (Hom.hom (map' f (l₁₂ ≫ l₂₃))) x✝ + (Hom.hom (map' f (l₁₂ ≫ l₂₃))) y✝ =
    (Hom.hom (map' f l₁₂ ≫ map' f l₂₃)) x✝ + (Hom.hom (map' f l₁₂ ≫ map' f l₂₃)) y✝
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:
ext x

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
x : ↑X
⊢ (evalAt f (r • s) g) x = ((RingHom.id R) r • evalAt f s g) x
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
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
⊢ HomEquiv.toRestrictScalars f (HomEquiv.fromExtendScalars f g) = g

Tactic:
ext x

Goal state after:
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 : ↑X
⊢ (Hom.hom (HomEquiv.toRestrictScalars f (HomEquiv.fromExtendScalars f g))) x = (Hom.hom g) x
Module: Mathlib.RingTheory.Coalgebra.TensorProduct

Goal state before:
pp: case e'_2.tmul.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
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
x₁ x₂ : A
y₁ y₂ : B
x₁₁ x₁₂ : A
⊢ (TensorProduct.assoc S (A ⊗[R] B) (A ⊗[R] B) (A ⊗[R] B))
      ((AlgebraTensorModule.tensorTensorTensorComm R S R S A A B B) (x₁₁ ⊗ₜ[S] x₁₂ ⊗ₜ[R] comul y₁) ⊗ₜ[S]
        (x₂ ⊗ₜ[R] y₂)) =
    F ((TensorProduct.assoc S A A A) (x₁₁ ⊗ₜ[S] x₁₂ ⊗ₜ[S] x₂) ⊗ₜ[R] (TensorProduct.assoc R B B B) (comul y₁ ⊗ₜ[R] y₂))

Tactic:
hopf_tensor_induction comul (R := R) y₁ with y₁₁ y₁₂

Goal state after:
case e'_2.tmul.tmul.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
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
x₁ x₂ : A
y₁ y₂ : B
x₁₁ x₁₂ : A
y₁₁ y₁₂ : B
⊢ (TensorProduct.assoc S (A ⊗[R] B) (A ⊗[R] B) (A ⊗[R] B))
      ((AlgebraTensorModule.tensorTensorTensorComm R S R S A A B B) (x₁₁ ⊗ₜ[S] x₁₂ ⊗ₜ[R] (y₁₁ ⊗ₜ[R] y₁₂)) ⊗ₜ[S]
        (x₂ ⊗ₜ[R] y₂)) =
    F
      ((TensorProduct.assoc S A A A) (x₁₁ ⊗ₜ[S] x₁₂ ⊗ₜ[S] x₂) ⊗ₜ[R]
        (TensorProduct.assoc R B B B) (y₁₁ ⊗ₜ[R] y₁₂ ⊗ₜ[R] y₂))
Module: Mathlib.RingTheory.Coalgebra.TensorProduct

Goal state before:
pp: 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
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : CommSemiring S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : AddCommMonoid N
inst✝¹³ : AddCommMonoid P
inst✝¹² : AddCommMonoid Q
inst✝¹¹ : Module R M
inst✝¹⁰ : Module R N
inst✝⁹ : Module R P
inst✝⁸ : Module R Q
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower R S M
inst✝⁵ : Coalgebra S M
inst✝⁴ : Module S N
inst✝³ : IsScalarTower R S N
inst✝² : Coalgebra S N
inst✝¹ : Coalgebra R P
inst✝ : Coalgebra R Q
⊢ _root_.TensorProduct.map ↑(_root_.TensorProduct.lid R P) ↑(_root_.TensorProduct.lid R P) ∘ₗ comul =
    comul ∘ₗ ↑(_root_.TensorProduct.lid R P)

Tactic:
ext x

Goal state after:
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
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : CommSemiring S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : AddCommMonoid N
inst✝¹³ : AddCommMonoid P
inst✝¹² : AddCommMonoid Q
inst✝¹¹ : Module R M
inst✝¹⁰ : Module R N
inst✝⁹ : Module R P
inst✝⁸ : Module R Q
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower R S M
inst✝⁵ : Coalgebra S M
inst✝⁴ : Module S N
inst✝³ : IsScalarTower R S N
inst✝² : Coalgebra S N
inst✝¹ : Coalgebra R P
inst✝ : Coalgebra R Q
x : P
⊢ ((AlgebraTensorModule.curry
          (_root_.TensorProduct.map ↑(_root_.TensorProduct.lid R P) ↑(_root_.TensorProduct.lid R P) ∘ₗ comul))
        1)
      x =
    ((AlgebraTensorModule.curry (comul ∘ₗ ↑(_root_.TensorProduct.lid R P))) 1) x