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

Goal state before:
pp: C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : TwoSquare G L₁ L₂ H
⊢ (fun β ↦
        TwoSquare.mk G L₁ L₂ H
          ((G ⋙ L₂).leftUnitor.inv ≫
            whiskerRight adj₁.unit (G ⋙ L₂) ≫
              ((L₁ ⋙ R₁).associator G L₂).inv ≫
                whiskerRight (L₁.associator R₁ G).hom L₂ ≫
                  whiskerRight (L₁.whiskerLeft β.natTrans) L₂ ≫
                    whiskerRight (L₁.associator H R₂).inv L₂ ≫
                      ((L₁ ⋙ H).associator R₂ L₂).hom ≫ (L₁ ⋙ H).whiskerLeft adj₂.counit ≫ (L₁ ⋙ H).rightUnitor.hom))
      ((fun α ↦
          TwoSquare.mk R₁ H G R₂
            ((R₁ ⋙ G).rightUnitor.inv ≫
              (R₁ ⋙ G).whiskerLeft adj₂.unit ≫
                (R₁.associator G (L₂ ⋙ R₂)).hom ≫
                  R₁.whiskerLeft (G.associator L₂ R₂).inv ≫
                    R₁.whiskerLeft (whiskerRight α.natTrans R₂) ≫
                      R₁.whiskerLeft (L₁.associator H R₂).hom ≫
                        (R₁.associator L₁ (H ⋙ R₂)).inv ≫ whiskerRight adj₁.counit (H ⋙ R₂) ≫ (H ⋙ R₂).leftUnitor.hom))
        α) =
    α

Tactic:
ext

Goal state after:
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : TwoSquare G L₁ L₂ H
X✝ : C
⊢ ((fun β ↦
              TwoSquare.mk G L₁ L₂ H
                ((G ⋙ L₂).leftUnitor.inv ≫
                  whiskerRight adj₁.unit (G ⋙ L₂) ≫
                    ((L₁ ⋙ R₁).associator G L₂).inv ≫
                      whiskerRight (L₁.associator R₁ G).hom L₂ ≫
                        whiskerRight (L₁.whiskerLeft β.natTrans) L₂ ≫
                          whiskerRight (L₁.associator H R₂).inv L₂ ≫
                            ((L₁ ⋙ H).associator R₂ L₂).hom ≫
                              (L₁ ⋙ H).whiskerLeft adj₂.counit ≫ (L₁ ⋙ H).rightUnitor.hom))
            ((fun α ↦
                TwoSquare.mk R₁ H G R₂
                  ((R₁ ⋙ G).rightUnitor.inv ≫
                    (R₁ ⋙ G).whiskerLeft adj₂.unit ≫
                      (R₁.associator G (L₂ ⋙ R₂)).hom ≫
                        R₁.whiskerLeft (G.associator L₂ R₂).inv ≫
                          R₁.whiskerLeft (whiskerRight α.natTrans R₂) ≫
                            R₁.whiskerLeft (L₁.associator H R₂).hom ≫
                              (R₁.associator L₁ (H ⋙ R₂)).inv ≫
                                whiskerRight adj₁.counit (H ⋙ R₂) ≫ (H ⋙ R₂).leftUnitor.hom))
              α)).natTrans.app
      X✝ =
    α.natTrans.app X✝
Module: Mathlib.CategoryTheory.Adjunction.Mates

Goal state before:
pp: C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
β : TwoSquare R₁ H G R₂
⊢ (fun α ↦
        TwoSquare.mk R₁ H G R₂
          ((R₁ ⋙ G).rightUnitor.inv ≫
            (R₁ ⋙ G).whiskerLeft adj₂.unit ≫
              (R₁.associator G (L₂ ⋙ R₂)).hom ≫
                R₁.whiskerLeft (G.associator L₂ R₂).inv ≫
                  R₁.whiskerLeft (whiskerRight α.natTrans R₂) ≫
                    R₁.whiskerLeft (L₁.associator H R₂).hom ≫
                      (R₁.associator L₁ (H ⋙ R₂)).inv ≫ whiskerRight adj₁.counit (H ⋙ R₂) ≫ (H ⋙ R₂).leftUnitor.hom))
      ((fun β ↦
          TwoSquare.mk G L₁ L₂ H
            ((G ⋙ L₂).leftUnitor.inv ≫
              whiskerRight adj₁.unit (G ⋙ L₂) ≫
                ((L₁ ⋙ R₁).associator G L₂).inv ≫
                  whiskerRight (L₁.associator R₁ G).hom L₂ ≫
                    whiskerRight (L₁.whiskerLeft β.natTrans) L₂ ≫
                      whiskerRight (L₁.associator H R₂).inv L₂ ≫
                        ((L₁ ⋙ H).associator R₂ L₂).hom ≫ (L₁ ⋙ H).whiskerLeft adj₂.counit ≫ (L₁ ⋙ H).rightUnitor.hom))
        β) =
    β

Tactic:
ext

Goal state after:
C : Type u₁
D : Type u₂
E : Type u₃
F : Type u₄
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} E
inst✝ : Category.{v₄, u₄} F
G : C ⥤ E
H : D ⥤ F
L₁ : C ⥤ D
R₁ : D ⥤ C
L₂ : E ⥤ F
R₂ : F ⥤ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
β : TwoSquare R₁ H G R₂
X✝ : D
⊢ ((fun α ↦
              TwoSquare.mk R₁ H G R₂
                ((R₁ ⋙ G).rightUnitor.inv ≫
                  (R₁ ⋙ G).whiskerLeft adj₂.unit ≫
                    (R₁.associator G (L₂ ⋙ R₂)).hom ≫
                      R₁.whiskerLeft (G.associator L₂ R₂).inv ≫
                        R₁.whiskerLeft (whiskerRight α.natTrans R₂) ≫
                          R₁.whiskerLeft (L₁.associator H R₂).hom ≫
                            (R₁.associator L₁ (H ⋙ R₂)).inv ≫
                              whiskerRight adj₁.counit (H ⋙ R₂) ≫ (H ⋙ R₂).leftUnitor.hom))
            ((fun β ↦
                TwoSquare.mk G L₁ L₂ H
                  ((G ⋙ L₂).leftUnitor.inv ≫
                    whiskerRight adj₁.unit (G ⋙ L₂) ≫
                      ((L₁ ⋙ R₁).associator G L₂).inv ≫
                        whiskerRight (L₁.associator R₁ G).hom L₂ ≫
                          whiskerRight (L₁.whiskerLeft β.natTrans) L₂ ≫
                            whiskerRight (L₁.associator H R₂).inv L₂ ≫
                              ((L₁ ⋙ H).associator R₂ L₂).hom ≫
                                (L₁ ⋙ H).whiskerLeft adj₂.counit ≫ (L₁ ⋙ H).rightUnitor.hom))
              β)).natTrans.app
      X✝ =
    β.natTrans.app 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
inst✝ : Small.{w, max w u} (Quot F)
x✝² x✝¹ : J
x✝ : x✝² ⟶ x✝¹
⊢ F.map x✝ ≫ ofHom (Shrink.addEquiv.symm.toAddMonoidHom.comp (Quot.ι F x✝¹)) =
    ofHom (Shrink.addEquiv.symm.toAddMonoidHom.comp (Quot.ι F x✝²)) ≫
      ((Functor.const J).obj (of (Shrink.{w, max u w} (Quot F)))).map x✝

Tactic:
ext

Goal state after:
J : Type u
inst✝² : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝¹ : DecidableEq J
inst✝ : Small.{w, max w u} (Quot F)
x✝³ x✝² : J
x✝¹ : x✝³ ⟶ x✝²
x✝ : ↑(F.obj x✝³)
⊢ (Hom.hom (F.map x✝¹ ≫ ofHom (Shrink.addEquiv.symm.toAddMonoidHom.comp (Quot.ι F x✝²)))) x✝ =
    (Hom.hom
        (ofHom (Shrink.addEquiv.symm.toAddMonoidHom.comp (Quot.ι F x✝³)) ≫
          ((Functor.const J).obj (of (Shrink.{w, max u w} (Quot F)))).map x✝¹))
      x✝
Module: Mathlib.RingTheory.Congruence.Hom

Goal state before:
pp: case refl
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 : N
⊢ Relation.Map (⇑c) (⇑f) (⇑f) x x

Tactic:
exact this.refl x

Goal state after:
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✝ d✝ c : RingCon M
d : ↑(Set.Ici c)
⊢ (fun d ↦ ⟨d.comap c.mk', ⋯⟩) ((fun d ↦ mapGen ⇑c.mk') d) = d

Tactic:
ext

Goal state after:
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 : ↑(Set.Ici c)
x✝ y✝ : M
⊢ ↑((fun d ↦ ⟨d.comap c.mk', ⋯⟩) ((fun d ↦ mapGen ⇑c.mk') d)) x✝ y✝ ↔ ↑d x✝ y✝
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
C : TensorAlgebra R M → Prop
algebraMap : ∀ (r : R), C ((Algebra.algebraMap R (TensorAlgebra R M)) r)
ι : ∀ (x : M), C ((TensorAlgebra.ι R) x)
mul : ∀ (a b : TensorAlgebra R M), C a → C b → C (a * b)
add : ∀ (a b : TensorAlgebra R M), C a → C b → C (a + b)
a : TensorAlgebra R M
s : Subalgebra R (TensorAlgebra R M) :=
  { carrier := {a | C a}, mul_mem' := mul, one_mem' := ⋯, add_mem' := add, zero_mem' := ⋯,
    algebraMap_mem' := algebraMap }
of : M →ₗ[R] ↥s := LinearMap.codRestrict (Subalgebra.toSubmodule s) (TensorAlgebra.ι R) ι
of_apply : ∀ {x : M}, ↑(of x) = (TensorAlgebra.ι R) x
⊢ AlgHom.id R (TensorAlgebra R M) = s.val.comp ((lift R) of)

Tactic:
ext

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
C : TensorAlgebra R M → Prop
algebraMap : ∀ (r : R), C ((Algebra.algebraMap R (TensorAlgebra R M)) r)
ι : ∀ (x : M), C ((TensorAlgebra.ι R) x)
mul : ∀ (a b : TensorAlgebra R M), C a → C b → C (a * b)
add : ∀ (a b : TensorAlgebra R M), C a → C b → C (a + b)
a : TensorAlgebra R M
s : Subalgebra R (TensorAlgebra R M) :=
  { carrier := {a | C a}, mul_mem' := mul, one_mem' := ⋯, add_mem' := add, zero_mem' := ⋯,
    algebraMap_mem' := algebraMap }
of : M →ₗ[R] ↥s := LinearMap.codRestrict (Subalgebra.toSubmodule s) (TensorAlgebra.ι R) ι
of_apply : ∀ {x : M}, ↑(of x) = (TensorAlgebra.ι R) x
x✝ : M
⊢ ((AlgHom.id R (TensorAlgebra R M)).toLinearMap ∘ₗ TensorAlgebra.ι R) x✝ =
    ((s.val.comp ((lift R) of)).toLinearMap ∘ₗ TensorAlgebra.ι R) x✝
Module: Mathlib.Algebra.Category.AlgCat.TensorAlgebra

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝² x✝¹ : AlgCat R
x✝ : x✝² ⟶ x✝¹
⊢ (Hom.hom
          ((forget₂ (AlgCat R) (ModuleCat R) ⋙ tensorAlgebra R).map x✝ ≫
            ofHom ((TensorAlgebra.lift R) LinearMap.id))).toLinearMap ∘ₗ
      TensorAlgebra.ι R =
    (Hom.hom (ofHom ((TensorAlgebra.lift R) LinearMap.id) ≫ (𝟭 (AlgCat R)).map x✝)).toLinearMap ∘ₗ TensorAlgebra.ι R

Tactic:
ext

Goal state after:
R : Type u
inst✝ : CommRing R
x✝³ x✝² : AlgCat R
x✝¹ : x✝³ ⟶ x✝²
x✝ : ↑((forget₂ (AlgCat R) (ModuleCat R)).obj x✝³)
⊢ ((Hom.hom
            ((forget₂ (AlgCat R) (ModuleCat R) ⋙ tensorAlgebra R).map x✝¹ ≫
              ofHom ((TensorAlgebra.lift R) LinearMap.id))).toLinearMap ∘ₗ
        TensorAlgebra.ι R)
      x✝ =
    ((Hom.hom (ofHom ((TensorAlgebra.lift R) LinearMap.id) ≫ (𝟭 (AlgCat R)).map x✝¹)).toLinearMap ∘ₗ TensorAlgebra.ι R)
      x✝
Module: Mathlib.Algebra.Category.AlgCat.TensorAlgebra

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝² x✝¹ : AlgCat R
x✝ : x✝² ⟶ x✝¹
⊢ (forget₂ (AlgCat R) (ModuleCat R) ⋙ tensorAlgebra R).map x✝ ≫ ofHom ((TensorAlgebra.lift R) LinearMap.id) =
    ofHom ((TensorAlgebra.lift R) LinearMap.id) ≫ (𝟭 (AlgCat R)).map x✝

Tactic:
by
    ext : 1
    apply TensorAlgebra.hom_ext
    ext
    simp

Goal state after:
Module: Mathlib.Algebra.Category.AlgCat.TensorAlgebra

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x✝ : ModuleCat R
⊢ ((TensorAlgebra.lift R) LinearMap.id).comp ((TensorAlgebra.lift R) (TensorAlgebra.ι R ∘ₗ TensorAlgebra.ι R)) =
    AlgHom.id R (TensorAlgebra R ↑x✝)

Tactic:
ext

Goal state after:
R : Type u
inst✝ : CommRing R
x✝¹ : ModuleCat R
x✝ : ↑x✝¹
⊢ ((((TensorAlgebra.lift R) LinearMap.id).comp
            ((TensorAlgebra.lift R) (TensorAlgebra.ι R ∘ₗ TensorAlgebra.ι R))).toLinearMap ∘ₗ
        TensorAlgebra.ι R)
      x✝ =
    ((AlgHom.id R (TensorAlgebra R ↑x✝¹)).toLinearMap ∘ₗ TensorAlgebra.ι R) x✝
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝¹ : AddMonoidWithOne R
inst✝ : AddMonoid M
x✝ : ℕ
⊢ inl ↑(x✝ + 1) = inl ↑x✝ + 1

Tactic:
ext

Goal state after:
case h1
R : Type u
M : Type v
inst✝¹ : AddMonoidWithOne R
inst✝ : AddMonoid M
x✝ : ℕ
⊢ (inl ↑(x✝ + 1)).fst = (inl ↑x✝ + 1).fst

case h2
R : Type u
M : Type v
inst✝¹ : AddMonoidWithOne R
inst✝ : AddMonoid M
x✝ : ℕ
⊢ (inl ↑(x✝ + 1)).snd = (inl ↑x✝ + 1).snd
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: case succ
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
n : ℕ
ih : x.snd <• x.fst ^ n = x.fst ^ n •> x.snd
⊢ x.snd <• x.fst ^ (n + 1) = x.fst ^ (n + 1) •> x.snd

Tactic:
rw [pow_succ, op_mul, mul_smul, mul_smul, ← h, smul_comm (_ : R) (op x.fst) x.snd, ih]

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₁ : C ⥤ D
R₁ : D ⥤ C
adj₁ : L₁ ⊣ R₁
⊢ (conjugateEquiv adj₁ adj₁) (𝟙 L₁) = 𝟙 R₁

Tactic:
ext

Goal state after:
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
L₁ : C ⥤ D
R₁ : D ⥤ C
adj₁ : L₁ ⊣ R₁
x✝ : D
⊢ ((conjugateEquiv adj₁ adj₁) (𝟙 L₁)).app x✝ = (𝟙 R₁).app x✝
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
r : R
x : tsze R M
h : r * x.fst = 1
⊢ (inl r + inr (-(r •> x.snd <• r))) * x = 1

Tactic:
ext

Goal state after:
case h1
R : Type u
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Semiring R
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
r : R
x : tsze R M
h : r * x.fst = 1
⊢ ((inl r + inr (-(r •> x.snd <• r))) * x).fst = fst 1

case h2
R : Type u
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Semiring R
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
r : R
x : tsze R M
h : r * x.fst = 1
⊢ ((inl r + inr (-(r •> x.snd <• r))) * x).snd = snd 1
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
x : tsze R M
r : R
h : x.fst * r = 1
⊢ x * (inl r + inr (-(r •> (x.snd <• r)))) = 1

Tactic:
ext

Goal state after:
case h1
R : Type u
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Semiring R
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
x : tsze R M
r : R
h : x.fst * r = 1
⊢ (x * (inl r + inr (-(r •> (x.snd <• r))))).fst = fst 1

case h2
R : Type u
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Semiring R
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
x : tsze R M
r : R
h : x.fst * r = 1
⊢ (x * (inl r + inr (-(r •> (x.snd <• r))))).snd = snd 1
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
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
inst✝ : Invertible x.fst
⊢ (⅟x.fst, -(⅟x.fst •> x.snd <• ⅟x.fst)) = inl ⅟x.fst + inr (-(⅟x.fst •> x.snd <• ⅟x.fst))

Tactic:
ext

Goal state after:
case h1
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
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
inst✝ : Invertible x.fst
⊢ fst (⅟x.fst, -(⅟x.fst •> x.snd <• ⅟x.fst)) = (inl ⅟x.fst + inr (-(⅟x.fst •> x.snd <• ⅟x.fst))).fst

case h2
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
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
inst✝ : Invertible x.fst
⊢ snd (⅟x.fst, -(⅟x.fst •> x.snd <• ⅟x.fst)) = (inl ⅟x.fst + inr (-(⅟x.fst •> x.snd <• ⅟x.fst))).snd
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
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
inst✝ : Invertible x.fst
⊢ (⅟x.fst, -(⅟x.fst •> x.snd <• ⅟x.fst)) = inl ⅟x.fst + inr (-(⅟x.fst •> (x.snd <• ⅟x.fst)))

Tactic:
ext

Goal state after:
case h1
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
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
inst✝ : Invertible x.fst
⊢ fst (⅟x.fst, -(⅟x.fst •> x.snd <• ⅟x.fst)) = (inl ⅟x.fst + inr (-(⅟x.fst •> (x.snd <• ⅟x.fst)))).fst

case h2
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
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
inst✝ : Invertible x.fst
⊢ snd (⅟x.fst, -(⅟x.fst •> x.snd <• ⅟x.fst)) = (inl ⅟x.fst + inr (-(⅟x.fst •> (x.snd <• ⅟x.fst)))).snd
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
x : tsze R M
⊢ IsUnit x ↔ IsUnit x.fst

Tactic:
simp only [← nonempty_invertible_iff_isUnit, (invertibleEquivInvertibleFst x).nonempty_congr]

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

Goal state before:
pp: R : Type u
A : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
this :
  TensorProduct.lift (LinearMap.lsmul R A ∘ₗ counit) ∘ₗ comul =
    TensorProduct.lift (LinearMap.lsmul R A) ∘ₗ (TensorProduct.mk R R A) 1
⊢ TensorProduct.lift (LinearMap.lsmul R A ∘ₗ counit) ∘ₗ comul = LinearMap.id

Tactic:
ext

Goal state after:
R : Type u
A : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
this :
  TensorProduct.lift (LinearMap.lsmul R A ∘ₗ counit) ∘ₗ comul =
    TensorProduct.lift (LinearMap.lsmul R A) ∘ₗ (TensorProduct.mk R R A) 1
x✝ : A
⊢ (TensorProduct.lift (LinearMap.lsmul R A ∘ₗ counit) ∘ₗ comul) x✝ = LinearMap.id 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
r : R
⊢ (inl r)⁻¹ = inl r⁻¹

Tactic:
ext

Goal state after:
case h1
R : Type u
M : Type v
inst✝³ : DivisionSemiring R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
r : R
⊢ (inl r)⁻¹.fst = (inl r⁻¹).fst

case h2
R : Type u
M : Type v
inst✝³ : DivisionSemiring R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
r : R
⊢ (inl r)⁻¹.snd = (inl r⁻¹).snd
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ LinearMap.rTensor R LinearMap.id ∘ₗ (TensorProduct.mk R R R) 1 = (TensorProduct.mk R R R) 1

Tactic:
ext

Goal state after:
R : Type u
inst✝ : CommSemiring R
⊢ (LinearMap.rTensor R LinearMap.id ∘ₗ (TensorProduct.mk R R R) 1) 1 = ((TensorProduct.mk R R R) 1) 1
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ LinearMap.lTensor R LinearMap.id ∘ₗ (TensorProduct.mk R R R) 1 = (TensorProduct.mk R R R).flip 1

Tactic:
ext

Goal state after:
R : Type u
inst✝ : CommSemiring R
⊢ (LinearMap.lTensor R LinearMap.id ∘ₗ (TensorProduct.mk R R R) 1) 1 = ((TensorProduct.mk R R R).flip 1) 1
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ ↑(TensorProduct.comm R R R) ∘ₗ comul = comul

Tactic:
ext

Goal state after:
R : Type u
inst✝ : CommSemiring R
⊢ (↑(TensorProduct.comm R R R) ∘ₗ comul) 1 = comul 1
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
⊢ comul ∘ₗ inl R A B = TensorProduct.map (inl R A B) (inl R A B) ∘ₗ comul

Tactic:
ext

Goal state after:
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✝
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
m : M
⊢ (inr m)⁻¹ = 0

Tactic:
ext

Goal state after:
case h1
R : Type u
M : Type v
inst✝³ : DivisionSemiring R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
m : M
⊢ (inr m)⁻¹.fst = fst 0

case h2
R : Type u
M : Type v
inst✝³ : DivisionSemiring R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
m : M
⊢ (inr m)⁻¹.snd = snd 0
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₁
⊢ (mateEquiv adj₁ adj₂).symm ((mateEquiv adj₄ adj₃).symm α) =
    ((conjugateEquiv (adj₁.comp adj₄) (adj₃.comp adj₂)).symm.trans (equivNatTrans F₁ L₁ L₂ F₂).symm) α

Tactic:
ext

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
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✝
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
⊢ comul ∘ₗ inr R A B = TensorProduct.map (inr R A B) (inr R A B) ∘ₗ comul

Tactic:
ext

Goal state after:
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✝
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
x : tsze R M
hx : x.fst ≠ 0
⊢ x⁻¹ = inl x.fst⁻¹ + inr (-(x.fst⁻¹ •> x.snd <• x.fst⁻¹))

Tactic:
ext

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

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
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
inst✝ : Invertible x
this : Invertible x.fst := x.invertibleFstOfInvertible
⊢ ⅟x = x⁻¹

Tactic:
ext

Goal state after:
case h1
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
inst✝ : Invertible x
this : Invertible x.fst := ⋯
⊢ (⅟x).fst = x⁻¹.fst

case h2
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
inst✝ : Invertible x
this : Invertible x.fst := ⋯
⊢ (⅟x).snd = x⁻¹.snd