mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : IsIso f
hfg : IsIso (f ≫ g)
⊢ isomorphisms C g

Tactic:
simpa using

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : IsIso f
hfg : IsIso (f ≫ g)
⊢ IsIso g
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
W✝ : MorphismProperty C
F : C ⥤ D
W : MorphismProperty D
inst✝ : W.HasTwoOutOfThreeProperty
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hg : W.inverseImage F g
hfg : W.inverseImage F (f ≫ g)
⊢ W (F.map f ≫ F.map g)

Tactic:
simpa using

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
W✝ : MorphismProperty C
F : C ⥤ D
W : MorphismProperty D
inst✝ : W.HasTwoOutOfThreeProperty
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hg : W.inverseImage F g
hfg : W.inverseImage F (f ≫ g)
⊢ W (F.map f ≫ F.map g)
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
W✝ : MorphismProperty C
F : C ⥤ D
W : MorphismProperty D
inst✝ : W.HasTwoOutOfThreeProperty
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : W.inverseImage F f
hfg : W.inverseImage F (f ≫ g)
⊢ W (F.map f ≫ F.map g)

Tactic:
simpa using

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
W✝ : MorphismProperty C
F : C ⥤ D
W : MorphismProperty D
inst✝ : W.HasTwoOutOfThreeProperty
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : W.inverseImage F f
hfg : W.inverseImage F (f ≫ g)
⊢ W (F.map f ≫ F.map g)
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
X : C
⊢ MorphismProperty.injective C (𝟙 X)

Tactic:
by
    delta MorphismProperty.injective
    convert! injective_id
    aesop

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ HasPushout f.op g.op ↔ HasPullback f g

Tactic:
HasPushout,

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ HasColimit (span f.op g.op) ↔ HasPullback f g
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : Cᵒᵖ
f : X ⟶ Z
g : Y ⟶ Z
⊢ HasPushout f.unop g.unop ↔ HasPullback f g

Tactic:
HasPushout,

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : Cᵒᵖ
f : X ⟶ Z
g : Y ⟶ Z
⊢ HasColimit (span f.unop g.unop) ↔ HasPullback f g
Module: Mathlib.Algebra.Category.ModuleCat.Colimits

Goal state before:
pp: R : Type w
inst✝² : Ring R
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ ModuleCat R
inst✝ : HasColimit (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat)
⊢ ∀ (j : J),
    colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j ≫
        colimMap { app := fun j ↦ (F.obj j).smul 1, naturality := ⋯ } =
      colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j ≫ 1

Tactic:
simp +instances

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

Goal state before:
pp: R : Type w
inst✝² : Ring R
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ ModuleCat R
inst✝ : HasColimit (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat)
r s : R
j : J
⊢ colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j ≫
      colimMap { app := fun j ↦ (F.obj j).smul (r * s), naturality := ⋯ } =
    colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j ≫
      (colimMap { app := fun j ↦ (F.obj j).smul r, naturality := ⋯ } *
        colimMap { app := fun j ↦ (F.obj j).smul s, naturality := ⋯ })

Tactic:
simp +instances

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

Goal state before:
pp: R : Type w
inst✝² : Ring R
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ ModuleCat R
inst✝ : HasColimit (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat)
⊢ ∀ (j : J),
    colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j ≫
        colimMap { app := fun j ↦ (F.obj j).smul 0, naturality := ⋯ } =
      colimit.ι (F ⋙ forget₂ (ModuleCat R) AddCommGrpCat) j ≫ 0

Tactic:
simp +instances

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
j : J
x : ↑(F.obj j)
⊢ (desc F c) ((ι F j) x) = (ConcreteCategory.hom (c.ι.app j)) x

Tactic:
dsimp [desc, ι]
  erw [QuotientAddGroup.lift_mk']
  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₄
E : Type u₅
F : Type u₆
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
inst✝² : Category.{v₄, u₄} D
inst✝¹ : Category.{v₅, u₅} E
inst✝ : Category.{v₆, u₆} F
G₁ : A ⥤ C
G₂ : C ⥤ E
H₁ : B ⥤ D
H₂ : D ⥤ F
L₁ : A ⥤ B
R₁ : B ⥤ A
L₂ : C ⥤ D
R₂ : D ⥤ C
L₃ : E ⥤ F
R₃ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : TwoSquare G₁ L₁ L₂ H₁
β : TwoSquare G₂ L₂ L₃ H₂
b : B
⊢ adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
      R₃.map (β.natTrans.app (G₁.obj (R₁.obj b))) ≫
        R₃.map (H₂.map (α.natTrans.app (R₁.obj b))) ≫ R₃.map (H₂.map (H₁.map (adj₁.counit.app b))) =
    ((adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
          R₃.map
            (L₃.map
              ((G₂.map (adj₂.unit.app (G₁.obj (R₁.obj b))) ≫ G₂.map (R₂.map (α.natTrans.app (R₁.obj b)))) ≫
                G₂.map (R₂.map (H₁.map (adj₁.counit.app b)))))) ≫
        R₃.map (β.natTrans.app (R₂.obj (H₁.obj b)))) ≫
      R₃.map (H₂.map (adj₂.counit.app (H₁.obj b)))

Tactic:
L₃.map_comp,

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
D : Type u₄
E : Type u₅
F : Type u₆
inst✝⁵ : Category.{v₁, u₁} A
inst✝⁴ : Category.{v₂, u₂} B
inst✝³ : Category.{v₃, u₃} C
inst✝² : Category.{v₄, u₄} D
inst✝¹ : Category.{v₅, u₅} E
inst✝ : Category.{v₆, u₆} F
G₁ : A ⥤ C
G₂ : C ⥤ E
H₁ : B ⥤ D
H₂ : D ⥤ F
L₁ : A ⥤ B
R₁ : B ⥤ A
L₂ : C ⥤ D
R₂ : D ⥤ C
L₃ : E ⥤ F
R₃ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
adj₃ : L₃ ⊣ R₃
α : TwoSquare G₁ L₁ L₂ H₁
β : TwoSquare G₂ L₂ L₃ H₂
b : B
⊢ adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
      R₃.map (β.natTrans.app (G₁.obj (R₁.obj b))) ≫
        R₃.map (H₂.map (α.natTrans.app (R₁.obj b))) ≫ R₃.map (H₂.map (H₁.map (adj₁.counit.app b))) =
    ((adj₃.unit.app (G₂.obj (G₁.obj (R₁.obj b))) ≫
          R₃.map
            (L₃.map (G₂.map (adj₂.unit.app (G₁.obj (R₁.obj b))) ≫ G₂.map (R₂.map (α.natTrans.app (R₁.obj b)))) ≫
              L₃.map (G₂.map (R₂.map (H₁.map (adj₁.counit.app b)))))) ≫
        R₃.map (β.natTrans.app (R₂.obj (H₁.obj b)))) ≫
      R₃.map (H₂.map (adj₂.counit.app (H₁.obj b)))
Module: Mathlib.RingTheory.Congruence.Hom

Goal state before:
pp: case symm
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
this : Equivalence (Relation.Map ⇑c.toSetoid ⇑f ⇑f)
i✝¹ i✝ x✝ y✝ : N
a✝ : RingConGen.Rel (Relation.Map ⇑c ⇑f ⇑f) x✝ y✝
h : Relation.Map (⇑c) (⇑f) (⇑f) x✝ y✝
⊢ Relation.Map (⇑c) (⇑f) (⇑f) y✝ x✝

Tactic:
exact this.symm h

Goal state after:
Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
x : M
⊢ ((ringCon R M).liftₐ ((FreeAlgebra.lift R) ⇑f) ⋯) ↑(FreeAlgebra.ι R x) = f x

Tactic:
exact (RingCon.liftₐ_mk _ _ _ _).trans (FreeAlgebra.lift_ι_apply f x)

Goal state after:
Module: Mathlib.LinearAlgebra.TensorAlgebra.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : R
⊢ algebraMapInv ((algebraMap R (TensorAlgebra R M)) x) = x

Tactic:
simp [algebraMapInv]

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : R₁ ⟶ R₂
c : C
⊢ adj₁.unit.app c ≫ ((conjugateEquiv adj₁ adj₂).toFun ((conjugateEquiv adj₁ adj₂).invFun α)).app (L₁.obj c) =
    adj₂.unit.app c ≫ R₂.map (((conjugateEquiv adj₁ adj₂).symm α).app c)

Tactic:
exact (unit_conjugateEquiv adj₁ adj₂ ((conjugateEquiv adj₁ adj₂).symm α) c)

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

Goal state before:
pp: R : Type u
A : Type v
ι : Type u_1
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
a : A
repr : Repr R a ι
⊢ ∑ i ∈ repr.index, counit (repr.left i) ⊗ₜ[R] repr.right i = 1 ⊗ₜ[R] a

Tactic:
simpa using

Goal state after:
R : Type u
A : Type v
ι : Type u_1
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
a : A
repr : Repr R a ι
⊢ ∑ i ∈ repr.index, counit (repr.left i) ⊗ₜ[R] repr.right i = 1 ⊗ₜ[R] a
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
ι : Type u_1
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
a : A
repr : Repr R a ι
⊢ ∑ i ∈ repr.index, repr.left i ⊗ₜ[R] counit (repr.right i) = a ⊗ₜ[R] 1

Tactic:
simpa using

Goal state after:
R : Type u
A : Type v
ι : Type u_1
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
a : A
repr : Repr R a ι
⊢ ∑ i ∈ repr.index, repr.left i ⊗ₜ[R] counit (repr.right i) = a ⊗ₜ[R] 1
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
ι : Type u_1
κ : ι → Type u_2
Λ : ι → Type u_3
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
a : A
repr : Repr R a ι
a₁ : (i : ι) → Repr R (repr.left i) (κ i)
a₂ : (i : ι) → Repr R (repr.right i) (Λ i)
⊢ ∑ i ∈ repr.index, ∑ j ∈ (a₁ i).index, (a₁ i).left j ⊗ₜ[R] ((a₁ i).right j ⊗ₜ[R] repr.right i) =
    ∑ i ∈ repr.index, ∑ j ∈ (a₂ i).index, repr.left i ⊗ₜ[R] ((a₂ i).left j ⊗ₜ[R] (a₂ i).right j)

Tactic:
simpa using

Goal state after:
R : Type u
A : Type v
ι : Type u_1
κ : ι → Type u_2
Λ : ι → Type u_3
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
a : A
repr : Repr R a ι
a₁ : (i : ι) → Repr R (repr.left i) (κ i)
a₂ : (i : ι) → Repr R (repr.right i) (Λ i)
⊢ ∑ i ∈ repr.index, ∑ j ∈ (a₁ i).index, (a₁ i).left j ⊗ₜ[R] ((a₁ i).right j ⊗ₜ[R] repr.right i) =
    ∑ x ∈ repr.index, repr.left x ⊗ₜ[R] comul (repr.right x)
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
ι : Type u_1
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
a : A
𝓡 : Repr R a ι
⊢ ∑ x ∈ 𝓡.index, counit (𝓡.left x) • 𝓡.right x = a

Tactic:
simpa using

Goal state after:
R : Type u
A : Type v
ι : Type u_1
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
a : A
𝓡 : Repr R a ι
⊢ ∑ x ∈ 𝓡.index, counit (𝓡.left x) • 𝓡.right x = a
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : L₂ ⟶ L₁
inst✝ : IsIso ((conjugateEquiv adj₁ adj₂) α)
this : IsIso ((conjugateEquiv adj₁ adj₂).symm ((conjugateEquiv adj₁ adj₂) α))
⊢ IsIso α

Tactic:
simpa using

Goal state after:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : L₂ ⟶ L₁
inst✝ : IsIso ((conjugateEquiv adj₁ adj₂) α)
this : IsIso ((conjugateEquiv adj₁ adj₂).symm ((conjugateEquiv adj₁ adj₂) α))
⊢ IsIso α
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : R₁ ⟶ R₂
inst✝ : IsIso ((conjugateEquiv adj₁ adj₂).symm α)
this : IsIso ((conjugateEquiv adj₁ adj₂) ((conjugateEquiv adj₁ adj₂).symm α))
⊢ IsIso α

Tactic:
simpa using

Goal state after:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : R₁ ⟶ R₂
inst✝ : IsIso ((conjugateEquiv adj₁ adj₂).symm α)
this : IsIso ((conjugateEquiv adj₁ adj₂) ((conjugateEquiv adj₁ adj₂).symm α))
⊢ IsIso α
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
  have vcomp := mateEquiv_vcomp adj₁ adj₂ adj₃ α (L₃.leftUnitor.hom ≫ β ≫ L₂.rightUnitor.inv)
  unfold vComp hComp at vcomp
  have vcompb := congr_app vcomp b
  simp only [comp_obj, id_obj, whiskerLeft_comp, assoc, mateEquiv_apply, whiskerLeft_twice,
    Iso.hom_inv_id_assoc, whiskerRight_comp, comp_app, Functor.whiskerLeft_app,
    Functor.whiskerRight_app, associator_hom_app, map_id, associator_inv_app, leftUnitor_hom_app,
    rightUnitor_inv_app, Functor.id_map, Functor.comp_map, id_comp, whiskerRight_twice,
    comp_id] at vcompb
  simpa [mateEquiv]

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

Tactic:
simpa using

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
⊢ ∑ x_1 ∈ (ℛ R x).index,
      ∑ x_2 ∈ (ℛ R ((ℛ R x).left x_1)).index,
        f ((ℛ R ((ℛ R x).left x_1)).left x_2) ⊗ₜ[R]
          (f ((ℛ R ((ℛ R x).left x_1)).right x_2) ⊗ₜ[R] f ((ℛ R x).right x_1)) =
    ∑ x_1 ∈ (ℛ R x).index,
      ∑ a ∈ (ℛ R ((ℛ R x).right x_1)).index,
        f ((ℛ R x).left x_1) ⊗ₜ[R] (f ((ℛ R ((ℛ R x).right x_1)).left a) ⊗ₜ[R] f ((ℛ R ((ℛ R x).right x_1)).right a))
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: case tmul
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 : (extendScalars f).obj X ⟶ Y
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
x : ↑((restrictScalars f).obj (of S S))
s : ↑X
⊢ (Hom.hom (HomEquiv.fromExtendScalars f (HomEquiv.toRestrictScalars f g))) (x ⊗ₜ[R] s) = (Hom.hom g) (x ⊗ₜ[R] s)

Tactic:
erw [TensorProduct.lift.tmul]

Goal state after:
case tmul
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 : (extendScalars f).obj X ⟶ Y
m1 : Module R S := Module.compHom S f
m2 : Module R ↑Y := Module.compHom (↑Y) f
x : ↑((restrictScalars f).obj (of S S))
s : ↑X
⊢ ({ toFun := fun s ↦ HomEquiv.evalAt f s (HomEquiv.toRestrictScalars f g), map_add' := ⋯, map_smul' := ⋯ } x) s =
    (Hom.hom g) (x ⊗ₜ[R] s)
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 : ModuleCat S
m : ↑M
⊢ (ConcreteCategory.hom ((extendRestrictScalarsAdj f).counit.app M)) (1 ⊗ₜ[R] m) = m

Tactic:
apply ExtendRestrictScalarsAdj.Counit.map_apply_one_tmul

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : D
⊢ F.map (adj2.unit.app (G.obj x)) ≫ adj1.counit.app (F'.obj (G.obj x)) ≫ adj2.counit.app x = adj1.counit.app x

Tactic:
rw [← adj1.counit_naturality, ← Category.assoc, ← F.map_comp]

Goal state after:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : D
⊢ F.map (adj2.unit.app (G.obj x) ≫ G.map (adj2.counit.app x)) ≫ adj1.counit.app x = adj1.counit.app x
Module: Mathlib.Order.Heyting.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : FunLike F α β
inst✝¹ : HeytingAlgebra α
x✝ : HeytingAlgebra β
inst✝ : HeytingHomClass F α β
f : F
⊢ f ⊤ = ⊤

Tactic:
by rw [← @himp_self α _ ⊥, ← himp_self, map_himp]

Goal state after:
Module: Mathlib.Order.Heyting.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝² : FunLike F α β
inst✝¹ : BiheytingAlgebra α
x✝ : BiheytingAlgebra β
inst✝ : BiheytingHomClass F α β
f : F
⊢ f ⊤ = ⊤

Tactic:
by rw [← @himp_self α _ ⊥, ← himp_self, map_himp]

Goal state after:
Module: Mathlib.Order.Heyting.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : HeytingAlgebra α
inst✝² : HeytingAlgebra β
inst✝¹ : HeytingAlgebra γ
inst✝ : HeytingAlgebra δ
f : HeytingHom α β
f' : α → β
h : f' = ⇑f
⊢ ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b

Tactic:
simpa using

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : HeytingAlgebra α
inst✝² : HeytingAlgebra β
inst✝¹ : HeytingAlgebra γ
inst✝ : HeytingAlgebra δ
f : HeytingHom α β
f' : α → β
h : f' = ⇑f
⊢ ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
Module: Mathlib.Order.Heyting.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : HeytingAlgebra α
inst✝² : HeytingAlgebra β
inst✝¹ : HeytingAlgebra γ
inst✝ : HeytingAlgebra δ
f : HeytingHom α β
f' : α → β
h : f' = ⇑f
⊢ ∀ (a b : α), f' (a ⊓ b) = f' a ⊓ f' b

Tactic:
simpa using

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : HeytingAlgebra α
inst✝² : HeytingAlgebra β
inst✝¹ : HeytingAlgebra γ
inst✝ : HeytingAlgebra δ
f : HeytingHom α β
f' : α → β
h : f' = ⇑f
⊢ ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
Module: Mathlib.Order.Heyting.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : HeytingAlgebra α
inst✝² : HeytingAlgebra β
inst✝¹ : HeytingAlgebra γ
inst✝ : HeytingAlgebra δ
f : HeytingHom α β
f' : α → β
h : f' = ⇑f
⊢ f' ⊥ = ⊥

Tactic:
simpa using

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : HeytingAlgebra α
inst✝² : HeytingAlgebra β
inst✝¹ : HeytingAlgebra γ
inst✝ : HeytingAlgebra δ
f : HeytingHom α β
f' : α → β
h : f' = ⇑f
⊢ f ⊥ = ⊥
Module: Mathlib.Order.Heyting.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : HeytingAlgebra α
inst✝² : HeytingAlgebra β
inst✝¹ : HeytingAlgebra γ
inst✝ : HeytingAlgebra δ
f : HeytingHom α β
f' : α → β
h : f' = ⇑f
⊢ ∀ (a b : α), f' (a ⇨ b) = f' a ⇨ f' b

Tactic:
simpa using

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : HeytingAlgebra α
inst✝² : HeytingAlgebra β
inst✝¹ : HeytingAlgebra γ
inst✝ : HeytingAlgebra δ
f : HeytingHom α β
f' : α → β
h : f' = ⇑f
⊢ ∀ (a b : α), f (a ⇨ b) = f a ⇨ f b
Module: Mathlib.Order.Heyting.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : CoheytingAlgebra α
inst✝² : CoheytingAlgebra β
inst✝¹ : CoheytingAlgebra γ
inst✝ : CoheytingAlgebra δ
f : CoheytingHom α β
f' : α → β
h : f' = ⇑f
⊢ ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b

Tactic:
simpa using

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : CoheytingAlgebra α
inst✝² : CoheytingAlgebra β
inst✝¹ : CoheytingAlgebra γ
inst✝ : CoheytingAlgebra δ
f : CoheytingHom α β
f' : α → β
h : f' = ⇑f
⊢ ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
Module: Mathlib.Order.Heyting.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : CoheytingAlgebra α
inst✝² : CoheytingAlgebra β
inst✝¹ : CoheytingAlgebra γ
inst✝ : CoheytingAlgebra δ
f : CoheytingHom α β
f' : α → β
h : f' = ⇑f
⊢ ∀ (a b : α), f' (a ⊓ b) = f' a ⊓ f' b

Tactic:
simpa using

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : CoheytingAlgebra α
inst✝² : CoheytingAlgebra β
inst✝¹ : CoheytingAlgebra γ
inst✝ : CoheytingAlgebra δ
f : CoheytingHom α β
f' : α → β
h : f' = ⇑f
⊢ ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
Module: Mathlib.Order.Heyting.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : CoheytingAlgebra α
inst✝² : CoheytingAlgebra β
inst✝¹ : CoheytingAlgebra γ
inst✝ : CoheytingAlgebra δ
f : CoheytingHom α β
f' : α → β
h : f' = ⇑f
⊢ f' ⊤ = ⊤

Tactic:
simpa using

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : CoheytingAlgebra α
inst✝² : CoheytingAlgebra β
inst✝¹ : CoheytingAlgebra γ
inst✝ : CoheytingAlgebra δ
f : CoheytingHom α β
f' : α → β
h : f' = ⇑f
⊢ f ⊤ = ⊤
Module: Mathlib.Order.Heyting.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : CoheytingAlgebra α
inst✝² : CoheytingAlgebra β
inst✝¹ : CoheytingAlgebra γ
inst✝ : CoheytingAlgebra δ
f : CoheytingHom α β
f' : α → β
h : f' = ⇑f
⊢ ∀ (a b : α), f' (a \ b) = f' a \ f' b

Tactic:
simpa using

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : CoheytingAlgebra α
inst✝² : CoheytingAlgebra β
inst✝¹ : CoheytingAlgebra γ
inst✝ : CoheytingAlgebra δ
f : CoheytingHom α β
f' : α → β
h : f' = ⇑f
⊢ ∀ (a b : α), f (a \ b) = f a \ f b
Module: Mathlib.Order.Heyting.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : BiheytingAlgebra α
inst✝² : BiheytingAlgebra β
inst✝¹ : BiheytingAlgebra γ
inst✝ : BiheytingAlgebra δ
f : BiheytingHom α β
f' : α → β
h : f' = ⇑f
⊢ ∀ (a b : α), f' (a ⊔ b) = f' a ⊔ f' b

Tactic:
simpa using

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : BiheytingAlgebra α
inst✝² : BiheytingAlgebra β
inst✝¹ : BiheytingAlgebra γ
inst✝ : BiheytingAlgebra δ
f : BiheytingHom α β
f' : α → β
h : f' = ⇑f
⊢ ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
Module: Mathlib.Order.Heyting.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : BiheytingAlgebra α
inst✝² : BiheytingAlgebra β
inst✝¹ : BiheytingAlgebra γ
inst✝ : BiheytingAlgebra δ
f : BiheytingHom α β
f' : α → β
h : f' = ⇑f
⊢ ∀ (a b : α), f' (a ⊓ b) = f' a ⊓ f' b

Tactic:
simpa using

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : FunLike F α β
inst✝³ : BiheytingAlgebra α
inst✝² : BiheytingAlgebra β
inst✝¹ : BiheytingAlgebra γ
inst✝ : BiheytingAlgebra δ
f : BiheytingHom α β
f' : α → β
h : f' = ⇑f
⊢ ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b