mathlib-initiative/mathlib-tactics huggingface dataset:
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 α
⊢ α ≫ inv α = 𝟙 L₂

Tactic:
by

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₂
inst✝ : IsIso α
⊢ inv α ≫ α = 𝟙 R₂

Tactic:
by

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₂
inst✝ : IsIso α
⊢ α ≫ inv α = 𝟙 R₁

Tactic:
by

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

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₂
α : L₂ ⟶ L₁
inst✝ : IsIso ((conjugateEquiv adj₁ adj₂) α)
this : IsIso ((conjugateEquiv adj₁ adj₂).symm ((conjugateEquiv adj₁ adj₂) α))
⊢ IsIso α

Tactic:
by

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₂
α : L₂ ⟶ L₁
inst✝ : IsIso ((conjugateEquiv adj₁ adj₂) α)
⊢ IsIso α

Tactic:
by

Goal state after:
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
m : M
⊢ IsUnit (inr m) ↔ Subsingleton R

Tactic:
by

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₂
inst✝ : IsIso ((conjugateEquiv adj₁ adj₂).symm α)
this : IsIso ((conjugateEquiv adj₁ adj₂) ((conjugateEquiv adj₁ adj₂).symm α))
⊢ IsIso α

Tactic:
by

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₂
inst✝ : IsIso ((conjugateEquiv adj₁ adj₂).symm α)
⊢ IsIso α

Tactic:
by

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
⊢ TensorProduct.lift (LinearMap.lsmul R A ∘ₗ counit) ∘ₗ comul = LinearMap.id

Tactic:
by

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₂
⊢ Function.LeftInverse
    (fun β ↦
      { hom := (conjugateEquiv adj₁ adj₂).symm β.hom, inv := (conjugateEquiv adj₂ adj₁).symm β.inv, hom_inv_id := ⋯,
        inv_hom_id := ⋯ })
    fun α ↦
    { hom := (conjugateEquiv adj₁ adj₂) α.hom, inv := (conjugateEquiv adj₂ adj₁) α.inv, hom_inv_id := ⋯,
      inv_hom_id := ⋯ }

Tactic:
by

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

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₂
⊢ Function.RightInverse
    (fun β ↦
      { hom := (conjugateEquiv adj₁ adj₂).symm β.hom, inv := (conjugateEquiv adj₂ adj₁).symm β.inv, hom_inv_id := ⋯,
        inv_hom_id := ⋯ })
    fun α ↦
    { hom := (conjugateEquiv adj₁ adj₂) α.hom, inv := (conjugateEquiv adj₂ adj₁) α.inv, hom_inv_id := ⋯,
      inv_hom_id := ⋯ }

Tactic:
by

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

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

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

Tactic:
by

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 F₁ L₁ L₂ F₂
⊢ ((mateEquiv adj₄ adj₃) ((mateEquiv adj₁ adj₂) α)).natTrans = (conjugateEquiv (adj₁.comp adj₄) (adj₃.comp adj₂)) α

Tactic:
by

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

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

Tactic:
by

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₁
⊢ (mateEquiv adj₁ adj₂).symm ((mateEquiv adj₄ adj₃).symm α) =
    ((conjugateEquiv (adj₁.comp adj₄) (adj₃.comp adj₂)).symm.trans (equivNatTrans F₁ L₁ L₂ F₂).symm) α

Tactic:
by

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

Tactic:
by

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

Goal state after:
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
⊢ 0⁻¹ = 0

Tactic:
by

Goal state after:
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
⊢ 1⁻¹ = 1

Tactic:
by

Goal state after:
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⁻¹ * x = 1

Tactic:
by

Goal state after:
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
⊢ ⅟x = x⁻¹

Tactic:
by

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:
by

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

Tactic:
by

Goal state after:
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
hx : x.fst ≠ 0
⊢ x * x⁻¹ = 1

Tactic:
by

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

Tactic:
by

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
⊢ counit ∘ₗ inr R A B = counit

Tactic:
by

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
⊢ counit ∘ₗ inl R A B = counit

Tactic:
by

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:
by

Goal state after:
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
a b : tsze R M
⊢ (a * b)⁻¹ = b⁻¹ * a⁻¹

Tactic:
by

Goal state after:
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
hx : x.fst ≠ 0
⊢ x⁻¹⁻¹ = 1 * x⁻¹⁻¹

Tactic:
by

Goal state after:
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
hx : x.fst ≠ 0
⊢ 1 * x⁻¹⁻¹ = x * x⁻¹ * x⁻¹⁻¹

Tactic:
by

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₃₂
⊢ (conjugateEquiv (adj₀₁.comp (adj₁₂.comp adj₂₃)) ((adj₀₁.comp adj₁₂).comp adj₂₃)) (L₀₁.associator L₁₂ L₂₃).hom =
    (R₃₂.associator R₂₁ R₁₀).hom

Tactic:
by

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

Goal state before:
pp: A : Type u₁
B : Type u₂
inst✝¹ : Category.{v₁, u₁} A
inst✝ : Category.{v₂, u₂} B
L : A ⥤ B
R : B ⥤ A
adj : L ⊣ R
⊢ (conjugateEquiv adj (Adjunction.id.comp adj)) L.leftUnitor.hom = R.rightUnitor.inv

Tactic:
by

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

Goal state before:
pp: A : Type u₁
B : Type u₂
inst✝¹ : Category.{v₁, u₁} A
inst✝ : Category.{v₂, u₂} B
L : A ⥤ B
R : B ⥤ A
adj : L ⊣ R
⊢ (conjugateEquiv adj (adj.comp Adjunction.id)) L.rightUnitor.hom = R.leftUnitor.inv

Tactic:
by

Goal state after:
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
hx : x.fst ≠ 0
⊢ x * x⁻¹ * x⁻¹⁻¹ = x

Tactic:
by

Goal state after:
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⁻¹ ↔ IsUnit x

Tactic:
by

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

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : DivisionRing R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
x : tsze R M
⊢ (-x)⁻¹ = -x⁻¹

Tactic:
by

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₁
⊢ (conjugateEquiv (adj.comp adj₁) (adj.comp adj₂)) (L.whiskerLeft τ) = whiskerRight ((conjugateEquiv adj₁ adj₂) τ) R

Tactic:
by

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₁
⊢ (conjugateEquiv (adj₁.comp adj) (adj₂.comp adj)) (whiskerRight τ L) = R.whiskerLeft ((conjugateEquiv adj₁ adj₂) τ)

Tactic:
by

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
f g : A →ₗc[R] B
h : (fun f ↦ f.toFun) f = (fun f ↦ f.toFun) g
⊢ f = g

Tactic:
by

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : CoalgebraStruct R A
f g : R →ₗc[R] A
h : f 1 = g 1
⊢ (fun x ↦ ↑x) f = (fun x ↦ ↑x) g

Tactic:
by

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
f : A →ₗc[R] B
f' : A → B
h : f' = ⇑f
⊢ counit ∘ₗ (↑f).copy f' h = counit

Tactic:
by

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
f : A →ₗc[R] B
f' : A → B
h : f' = ⇑f
⊢ map ((↑f).copy f' h) ((↑f).copy f' h) ∘ₗ comul = comul ∘ₗ (↑f).copy f' h

Tactic:
by

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
⊢ counit ∘ₗ LinearMap.id = counit

Tactic:
by

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
⊢ map LinearMap.id LinearMap.id ∘ₗ comul = comul ∘ₗ LinearMap.id

Tactic:
by

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
⊢ counit ∘ₗ ↑φ₁ ∘ₗ ↑φ₂ = counit

Tactic:
by

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
⊢ map (↑φ₁ ∘ₗ ↑φ₂) (↑φ₁ ∘ₗ ↑φ₂) ∘ₗ comul = comul ∘ₗ ↑φ₁ ∘ₗ ↑φ₂

Tactic:
by

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
⊢ counit ∘ₗ counit = counit

Tactic:
by

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
⊢ map counit counit ∘ₗ comul = comul ∘ₗ counit

Tactic:
by

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
f g : A →ₗc[R] R
x : A
⊢ f x = g x

Tactic:
by

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

Goal state before:
pp: S : Type u_1
R R' : Type u
M : Type v
inst✝¹⁶ : CommSemiring S
inst✝¹⁵ : Semiring R
inst✝¹⁴ : CommSemiring R'
inst✝¹³ : AddCommMonoid M
inst✝¹² : Algebra S R
inst✝¹¹ : Module S M
inst✝¹⁰ : Module R M
inst✝⁹ : Module Rᵐᵒᵖ M
inst✝⁸ : SMulCommClass R Rᵐᵒᵖ M
inst✝⁷ : IsScalarTower S R M
inst✝⁶ : IsScalarTower S Rᵐᵒᵖ M
inst✝⁵ : Module R' M
inst✝⁴ : Module R'ᵐᵒᵖ M
inst✝³ : IsCentralScalar R' M
A : Type u_2
inst✝² : Semiring A
inst✝¹ : Algebra S A
inst✝ : Algebra R' A
f : R →ₐ[S] A
g : M →ₗ[S] A
hg : ∀ (x y : M), g x * g y = 0
hfg : ∀ (r : R) (x : M), g (r •> x) = f r * g x
hgf : ∀ (r : R) (x : M), g (x <• r) = g x * f r
r₁ : R
m₁ : M
r₂ : R
m₂ : M
⊢ ((f.comp (fstHom S R M)).toLinearMap + g ∘ₗ ↑S (sndHom R M)) ((inl r₁ + inr m₁) * (inl r₂ + inr m₂)) =
    ((f.comp (fstHom S R M)).toLinearMap + g ∘ₗ ↑S (sndHom R M)) (inl r₁ + inr m₁) *
      ((f.comp (fstHom S R M)).toLinearMap + g ∘ₗ ↑S (sndHom R M)) (inl r₂ + inr m₂)

Tactic:
by

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
a : A
repr : Repr R a ι
F : Type u_2
inst✝¹ : FunLike F A B
inst✝ : CoalgHomClass F R A B
φ : F
⊢ (map ↑φ ↑φ ∘ₗ comul) a = ∑ i ∈ repr.index, (⇑φ ∘ repr.left) i ⊗ₜ[R] (⇑φ ∘ repr.right) i

Tactic:
by

Goal state after:
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✝⁷ : AddCommMonoid B
inst✝⁶ : AddCommMonoid C
inst✝⁵ : Module R A
inst✝⁴ : Module R B
inst✝³ : Module R C
inst✝² : CoalgebraStruct R A
inst✝¹ : CoalgebraStruct R B
inst✝ : CoalgebraStruct R C
e✝ e' e : A ≃ₗc[R] B
⊢ TensorProduct.map ↑e.toLinearEquiv.symm ↑e.toLinearEquiv.symm ∘ₗ comul = comul ∘ₗ ↑e.toLinearEquiv.symm

Tactic:
by

Goal state after:
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
⊢ ↑(TensorProduct.assoc R B B B) ∘ₗ LinearMap.rTensor B comul ∘ₗ comul = LinearMap.lTensor B comul ∘ₗ comul

Tactic:
by

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
⊢ ↑(TensorProduct.assoc R (A × B) (A × B) (A × B)) ∘ₗ rTensor (A × B) comul ∘ₗ comul = lTensor (A × B) comul ∘ₗ comul

Tactic:
by

Goal state after:
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 ∘ₗ comul = (TensorProduct.mk R R B) 1

Tactic:
by

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

Goal state before:
pp: S : Type u_1
R : Type u
M : Type v
inst✝⁹ : CommSemiring S
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Algebra S R
inst✝⁵ : Module S M
inst✝⁴ : Module R M
inst✝³ : Module Rᵐᵒᵖ M
inst✝² : SMulCommClass R Rᵐᵒᵖ M
inst✝¹ : IsScalarTower S R M
inst✝ : IsScalarTower S Rᵐᵒᵖ M
⊢ (inlAlgHom S R M).range ⊔ Algebra.adjoin S (Set.range inr) = ⊤

Tactic:
by

Goal state after:
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 ∘ₗ comul = (TensorProduct.mk R B R).flip 1

Tactic:
by

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
⊢ rTensor (A × B) counit ∘ₗ comul = (TensorProduct.mk R R (A × B)) 1

Tactic:
by

Goal state after: