mathlib-initiative/mathlib-tactics huggingface dataset:
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✝ : G.LaxMonoidal
X Y Z : C
| adj.unit.app X ▷ Y ▷ Z ≫
    (α_ (G.obj (F.obj X)) Y Z).hom ≫
      G.obj (F.obj X) ◁ adj.unit.app (Y ⊗ Z) ≫
        G.obj (F.obj X) ◁
            (G.map (F.map (adj.unit.app Y ⊗ₘ adj.unit.app Z)) ≫
              G.map (F.map (μ G (F.obj Y) (F.obj Z)) ≫ adj.counit.app (F.obj Y ⊗ F.obj Z))) ≫
          μ G (F.obj X) (F.obj Y ⊗ F.obj Z)

Tactic:
rw [← MonoidalCategory.whiskerLeft_comp_assoc, map_comp,
        unit_naturality_assoc, MonoidalCategory.whiskerLeft_comp,
        unit_naturality_assoc, right_triangle_components, comp_id, assoc,
        tensorHom_def, MonoidalCategory.whiskerLeft_comp_assoc,
        ← associator_naturality_middle_assoc, ← associator_naturality_right_assoc,
        ← associativity G, ← comp_whiskerRight_assoc, ← tensorHom_def,
        ← whisker_exchange_assoc, ← comp_whiskerRight_assoc]

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
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.LaxMonoidal
X Y Z : C
| (X ⊗ Y) ◁ adj.unit.app Z ≫
    ((adj.unit.app X ⊗ₘ adj.unit.app Y) ≫ μ G (F.obj X) (F.obj Y)) ▷ G.obj (F.obj Z) ≫
      μ G (F.obj X ⊗ F.obj Y) (F.obj Z) ≫ G.map (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom
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 : C ≌ D
inst✝² : e.functor.Monoidal
inst✝¹ : e.inverse.Monoidal
inst✝ : e.IsMonoidal
⊢ e.counitIso.inv.app (𝟙_ D) ≫ e.functor.map (η e.inverse) = ε e.functor

Tactic:
by
  rw [← cancel_epi (η e.functor), Monoidal.η_ε, ← functor_map_ε_inverse_comp_counitIso_hom_app,
    Category.assoc, Iso.hom_inv_id_app_assoc, Monoidal.map_ε_η]

Goal state after:
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 : C ≌ D
inst✝² : e.functor.Monoidal
inst✝¹ : e.inverse.Monoidal
inst✝ : e.IsMonoidal
⊢ e.counitInv.app (𝟙_ D) ≫ e.functor.map (η e.inverse) = ε e.functor

Tactic:
by
  rw [← cancel_epi (η e.functor), Monoidal.η_ε, ← functor_map_ε_inverse_comp_counitIso_hom_app,
    Category.assoc, Iso.hom_inv_id_app_assoc, Monoidal.map_ε_η]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : Ring M
inst✝ : Ring N
c : RingCon M
f : N →+* M
d : RingCon N
hcd : d = c.comap f
x : N
⊢ (c.comapQuotientEquivRange f hcd).symm ⟨↑(f x), ⋯⟩ = ↑x

Tactic:
by
  simp [RingEquiv.symm_apply_eq, ← Subtype.coe_inj]

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
⊢ Rel R M ≤ ⇑(RingCon.ker ((FreeAlgebra.lift R) ⇑f).toRingHom)

Tactic:
intro x

Goal state after:
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 : FreeAlgebra R M
⊢ Rel R M x ≤ (RingCon.ker ((FreeAlgebra.lift R) ⇑f).toRingHom) x
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
⊢ ∀ (n : ℕ), x.snd <• x.fst ^ n = x.fst ^ n •> x.snd

Tactic:
intro n
    induction n with
    | zero => simp
    | succ n ih =>
      rw [pow_succ, op_mul, mul_smul, mul_smul, ← h, smul_comm (_ : R) (op x.fst) x.snd, ih]

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

Goal state before:
pp: R : Type u
ι : Type v
A : ι → Type w
inst✝⁴ : DecidableEq ι
inst✝³ : CommSemiring R
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : (i : ι) → Module R (A i)
inst✝ : (i : ι) → Coalgebra R (A i)
i : ι
⊢ ↑(TensorProduct.assoc R (Π₀ (i : ι), A i) (Π₀ (i : ι), A i) (Π₀ (i : ι), A i)) ∘ₗ
      rTensor (Π₀ (i : ι), A i) comul ∘ₗ comul ∘ₗ lsingle i =
    lTensor (Π₀ (i : ι), A i) comul ∘ₗ comul ∘ₗ lsingle i

Tactic:
comul_comp_lsingle,

Goal state after:
R : Type u
ι : Type v
A : ι → Type w
inst✝⁴ : DecidableEq ι
inst✝³ : CommSemiring R
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : (i : ι) → Module R (A i)
inst✝ : (i : ι) → Coalgebra R (A i)
i : ι
⊢ ↑(TensorProduct.assoc R (Π₀ (i : ι), A i) (Π₀ (i : ι), A i) (Π₀ (i : ι), A i)) ∘ₗ
      rTensor (Π₀ (i : ι), A i) comul ∘ₗ TensorProduct.map (lsingle i) (lsingle i) ∘ₗ comul =
    lTensor (Π₀ (i : ι), A i) comul ∘ₗ TensorProduct.map (lsingle i) (lsingle i) ∘ₗ comul
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
ι : Type v
A : ι → Type w
inst✝⁴ : DecidableEq ι
inst✝³ : CommSemiring R
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : (i : ι) → Module R (A i)
inst✝ : (i : ι) → Coalgebra R (A i)
i : ι
⊢ ((↑(TensorProduct.assoc R (Π₀ (i : ι), A i) (Π₀ (i : ι), A i) (Π₀ (i : ι), A i)) ∘ₗ
          rTensor (Π₀ (i : ι), A i) comul) ∘ₗ
        TensorProduct.map (lsingle i) (lsingle i)) ∘ₗ
      comul =
    TensorProduct.map (lsingle i) (comul ∘ₗ lsingle i) ∘ₗ comul

Tactic:
comul_comp_lsingle,

Goal state after:
R : Type u
ι : Type v
A : ι → Type w
inst✝⁴ : DecidableEq ι
inst✝³ : CommSemiring R
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : (i : ι) → Module R (A i)
inst✝ : (i : ι) → Coalgebra R (A i)
i : ι
⊢ ((↑(TensorProduct.assoc R (Π₀ (i : ι), A i) (Π₀ (i : ι), A i) (Π₀ (i : ι), A i)) ∘ₗ
          rTensor (Π₀ (i : ι), A i) comul) ∘ₗ
        TensorProduct.map (lsingle i) (lsingle i)) ∘ₗ
      comul =
    TensorProduct.map (lsingle i) (TensorProduct.map (lsingle i) (lsingle i) ∘ₗ comul) ∘ₗ comul
Module: Mathlib.RingTheory.Coalgebra.Basic

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

Tactic:
comul_comp_lsingle,

Goal state after:
R : Type u
ι : Type v
A : ι → Type w
inst✝⁴ : DecidableEq ι
inst✝³ : CommSemiring R
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : (i : ι) → Module R (A i)
inst✝ : (i : ι) → Coalgebra R (A i)
i : ι
⊢ (↑(TensorProduct.assoc R (Π₀ (i : ι), A i) (Π₀ (i : ι), A i) (Π₀ (i : ι), A i)) ∘ₗ
        TensorProduct.map (TensorProduct.map (lsingle i) (lsingle i) ∘ₗ comul) (lsingle i)) ∘ₗ
      comul =
    TensorProduct.map (lsingle i) (TensorProduct.map (lsingle i) (lsingle i) ∘ₗ comul) ∘ₗ comul
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
ι : Type v
A : ι → Type w
inst✝⁴ : DecidableEq ι
inst✝³ : CommSemiring R
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : (i : ι) → Module R (A i)
inst✝ : (i : ι) → Coalgebra R (A i)
i✝ : ι
⊢ rTensor (Π₀ (i : ι), A i) counit ∘ₗ comul ∘ₗ lsingle i✝ = (TensorProduct.mk R R (Π₀ (i : ι), A i)) 1 ∘ₗ lsingle i✝

Tactic:
comul_comp_lsingle,

Goal state after:
R : Type u
ι : Type v
A : ι → Type w
inst✝⁴ : DecidableEq ι
inst✝³ : CommSemiring R
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : (i : ι) → Module R (A i)
inst✝ : (i : ι) → Coalgebra R (A i)
i✝ : ι
⊢ rTensor (Π₀ (i : ι), A i) counit ∘ₗ TensorProduct.map (lsingle i✝) (lsingle i✝) ∘ₗ comul =
    (TensorProduct.mk R R (Π₀ (i : ι), A i)) 1 ∘ₗ lsingle i✝
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
ι : Type v
A : ι → Type w
inst✝⁴ : DecidableEq ι
inst✝³ : CommSemiring R
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : (i : ι) → Module R (A i)
inst✝ : (i : ι) → Coalgebra R (A i)
i✝ : ι
⊢ lTensor (Π₀ (i : ι), A i) counit ∘ₗ comul ∘ₗ lsingle i✝ =
    (TensorProduct.mk R (Π₀ (i : ι), A i) R).flip 1 ∘ₗ lsingle i✝

Tactic:
comul_comp_lsingle,

Goal state after:
R : Type u
ι : Type v
A : ι → Type w
inst✝⁴ : DecidableEq ι
inst✝³ : CommSemiring R
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : (i : ι) → Module R (A i)
inst✝ : (i : ι) → Coalgebra R (A i)
i✝ : ι
⊢ lTensor (Π₀ (i : ι), A i) counit ∘ₗ TensorProduct.map (lsingle i✝) (lsingle i✝) ∘ₗ comul =
    (TensorProduct.mk R (Π₀ (i : ι), A i) R).flip 1 ∘ₗ lsingle i✝
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
ι : Type v
A : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
i : ι
⊢ ↑(TensorProduct.assoc R (ι →₀ A) (ι →₀ A) (ι →₀ A)) ∘ₗ rTensor (ι →₀ A) comul ∘ₗ comul ∘ₗ lsingle i =
    lTensor (ι →₀ A) comul ∘ₗ comul ∘ₗ lsingle i

Tactic:
comul_comp_lsingle,

Goal state after:
R : Type u
ι : Type v
A : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
i : ι
⊢ ↑(TensorProduct.assoc R (ι →₀ A) (ι →₀ A) (ι →₀ A)) ∘ₗ
      rTensor (ι →₀ A) comul ∘ₗ TensorProduct.map (lsingle i) (lsingle i) ∘ₗ comul =
    lTensor (ι →₀ A) comul ∘ₗ TensorProduct.map (lsingle i) (lsingle i) ∘ₗ comul
Module: Mathlib.RingTheory.Coalgebra.Basic

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

Tactic:
comul_comp_lsingle,

Goal state after:
R : Type u
ι : Type v
A : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
i : ι
⊢ ((↑(TensorProduct.assoc R (ι →₀ A) (ι →₀ A) (ι →₀ A)) ∘ₗ rTensor (ι →₀ A) comul) ∘ₗ
        TensorProduct.map (lsingle i) (lsingle i)) ∘ₗ
      comul =
    TensorProduct.map (lsingle i) (TensorProduct.map (lsingle i) (lsingle i) ∘ₗ comul) ∘ₗ comul
Module: Mathlib.RingTheory.Coalgebra.Basic

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

Tactic:
comul_comp_lsingle,

Goal state after:
R : Type u
ι : Type v
A : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
i : ι
⊢ (↑(TensorProduct.assoc R (ι →₀ A) (ι →₀ A) (ι →₀ A)) ∘ₗ
        TensorProduct.map (TensorProduct.map (lsingle i) (lsingle i) ∘ₗ comul) (lsingle i)) ∘ₗ
      comul =
    TensorProduct.map (lsingle i) (TensorProduct.map (lsingle i) (lsingle i) ∘ₗ comul) ∘ₗ comul
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
ι : Type v
A : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
a✝ : ι
⊢ rTensor (ι →₀ A) counit ∘ₗ comul ∘ₗ lsingle a✝ = (TensorProduct.mk R R (ι →₀ A)) 1 ∘ₗ lsingle a✝

Tactic:
comul_comp_lsingle,

Goal state after:
R : Type u
ι : Type v
A : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
a✝ : ι
⊢ rTensor (ι →₀ A) counit ∘ₗ TensorProduct.map (lsingle a✝) (lsingle a✝) ∘ₗ comul =
    (TensorProduct.mk R R (ι →₀ A)) 1 ∘ₗ lsingle a✝
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u
ι : Type v
A : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
a✝ : ι
⊢ lTensor (ι →₀ A) counit ∘ₗ comul ∘ₗ lsingle a✝ = (TensorProduct.mk R (ι →₀ A) R).flip 1 ∘ₗ lsingle a✝

Tactic:
comul_comp_lsingle,

Goal state after:
R : Type u
ι : Type v
A : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
a✝ : ι
⊢ lTensor (ι →₀ A) counit ∘ₗ TensorProduct.map (lsingle a✝) (lsingle a✝) ∘ₗ comul =
    (TensorProduct.mk R (ι →₀ A) R).flip 1 ∘ₗ lsingle a✝
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R₁ R₂ R₃ R₄ : Type u₁
inst✝³ : CommRing R₁
inst✝² : CommRing R₂
inst✝¹ : CommRing R₃
inst✝ : CommRing R₄
f₁₂ : R₁ →+* R₂
f₂₃ : R₂ →+* R₃
f₃₄ : R₃ →+* R₄
M : ModuleCat R₁
m : ↑M
h₁ : (ConcreteCategory.hom ((extendScalarsComp (f₂₃.comp f₁₂) f₃₄).hom.app M)) (1 ⊗ₜ[R₁] m) = 1 ⊗ₜ[R₃] (1 ⊗ₜ[R₁] m)
h₂ : (ConcreteCategory.hom ((extendScalarsComp f₁₂ (f₃₄.comp f₂₃)).hom.app M)) (1 ⊗ₜ[R₁] m) = 1 ⊗ₜ[R₂] (1 ⊗ₜ[R₁] m)
h₃ :
  ∀ (M : ModuleCat R₂) (m : ↑M),
    (ConcreteCategory.hom ((extendScalarsComp f₂₃ f₃₄).hom.app M)) (1 ⊗ₜ[R₂] m) = 1 ⊗ₜ[R₃] (1 ⊗ₜ[R₂] m)
⊢ (ConcreteCategory.hom
        (((extendScalarsComp (f₂₃.comp f₁₂) f₃₄).hom ≫
              Functor.whiskerRight (extendScalarsComp f₁₂ f₂₃).hom (extendScalars f₃₄)).app
          M))
      (1 ⊗ₜ[R₁] m) =
    (ConcreteCategory.hom
        (((extendScalarsComp f₁₂ (f₃₄.comp f₂₃)).hom ≫
              (extendScalars f₁₂).whiskerLeft (extendScalarsComp f₂₃ f₃₄).hom ≫
                ((extendScalars f₁₂).associator (extendScalars f₂₃) (extendScalars f₃₄)).inv).app
          M))
      (1 ⊗ₜ[R₁] m)

Tactic:
have h₄ := extendScalarsComp_hom_app_one_tmul f₁₂ f₂₃ M m

Goal state after:
R₁ R₂ R₃ R₄ : Type u₁
inst✝³ : CommRing R₁
inst✝² : CommRing R₂
inst✝¹ : CommRing R₃
inst✝ : CommRing R₄
f₁₂ : R₁ →+* R₂
f₂₃ : R₂ →+* R₃
f₃₄ : R₃ →+* R₄
M : ModuleCat R₁
m : ↑M
h₁ : (ConcreteCategory.hom ((extendScalarsComp (f₂₃.comp f₁₂) f₃₄).hom.app M)) (1 ⊗ₜ[R₁] m) = 1 ⊗ₜ[R₃] (1 ⊗ₜ[R₁] m)
h₂ : (ConcreteCategory.hom ((extendScalarsComp f₁₂ (f₃₄.comp f₂₃)).hom.app M)) (1 ⊗ₜ[R₁] m) = 1 ⊗ₜ[R₂] (1 ⊗ₜ[R₁] m)
h₃ :
  ∀ (M : ModuleCat R₂) (m : ↑M),
    (ConcreteCategory.hom ((extendScalarsComp f₂₃ f₃₄).hom.app M)) (1 ⊗ₜ[R₂] m) = 1 ⊗ₜ[R₃] (1 ⊗ₜ[R₂] m)
h₄ : (ConcreteCategory.hom ((extendScalarsComp f₁₂ f₂₃).hom.app M)) (1 ⊗ₜ[R₁] m) = 1 ⊗ₜ[R₂] (1 ⊗ₜ[R₁] m)
⊢ (ConcreteCategory.hom
        (((extendScalarsComp (f₂₃.comp f₁₂) f₃₄).hom ≫
              Functor.whiskerRight (extendScalarsComp f₁₂ f₂₃).hom (extendScalars f₃₄)).app
          M))
      (1 ⊗ₜ[R₁] m) =
    (ConcreteCategory.hom
        (((extendScalarsComp f₁₂ (f₃₄.comp f₂₃)).hom ≫
              (extendScalars f₁₂).whiskerLeft (extendScalarsComp f₂₃ f₃₄).hom ≫
                ((extendScalars f₁₂).associator (extendScalars f₂₃) (extendScalars f₃₄)).inv).app
          M))
      (1 ⊗ₜ[R₁] m)
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Goal state before:
pp: R₁ R₂ R₃ R₄ : Type u₁
inst✝³ : CommRing R₁
inst✝² : CommRing R₂
inst✝¹ : CommRing R₃
inst✝ : CommRing R₄
f₁₂ : R₁ →+* R₂
f₂₃ : R₂ →+* R₃
f₃₄ : R₃ →+* R₄
⊢ (extendScalarsComp f₁₂ (f₃₄.comp f₂₃)).hom ≫
      (extendScalars f₁₂).whiskerLeft (extendScalarsComp f₂₃ f₃₄).hom ≫
        ((extendScalars f₁₂).associator (extendScalars f₂₃) (extendScalars f₃₄)).inv ≫
          ((extendScalars f₁₂).associator (extendScalars f₂₃) (extendScalars f₃₄)).hom ≫
            (extendScalars f₁₂).whiskerLeft (extendScalarsComp f₂₃ f₃₄).inv ≫
              (extendScalarsComp f₁₂ (f₃₄.comp f₂₃)).inv =
    𝟙 (extendScalars (f₃₄.comp (f₂₃.comp f₁₂)))

Tactic:
simp only [Iso.inv_hom_id_assoc, ← Functor.whiskerLeft_comp_assoc, Iso.hom_inv_id,
    Functor.whiskerLeft_id', Category.id_comp]

Goal state after:
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
inst✝³ : Coalgebra R B
inst✝² : Coalgebra S A
inst✝¹ : IsCocomm S A
inst✝ : IsCocomm R B
⊢ ↑(TensorProduct.comm S (A ⊗[R] B) (A ⊗[R] B)) ∘ₗ comul = comul

Tactic:
ext x y
    dsimp
    conv_rhs => rw [← comm_comul _ x, ← comm_comul _ y]
    hopf_tensor_induction comul (R := S) x with x₁ x₂
    hopf_tensor_induction comul (R := R) y with y₁ y₂
    simp

Goal state after:
Module: Mathlib.CategoryTheory.Category.Bipointed

Goal state before:
pp: X Y Z : Bipointed
f : X.Hom Y
g : Y.Hom Z
⊢ (g.toFun ∘ f.toFun) X.toProd.1 = Z.toProd.1

Tactic:
rw [Function.comp_apply, f.map_fst, g.map_fst]

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

Goal state before:
pp: R : Type u_1
M : Type u_3
P : Type u_5
M' : Type u_6
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R P
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Coalgebra R M
f : M →ₗ[R] M'
g : P →ₗ[R] M
⊢ (ε ⊗ₘ f ∘ₗ δ) ∘ₗ g = (LinearMap.id ⊗ₘ f ∘ₗ λ⁻¹) ∘ₗ g

Tactic:
map_counit_comp_comul_left

Goal state after:
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
T : Type u_5
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra S T
inst✝³ : Algebra R T
inst✝² : IsScalarTower R S T
x y : R
inst✝¹ : Away x S
inst✝ : Away ((algebraMap R S) y) T
⊢ IsUnit ((algebraMap S T) ((algebraMap R S) y)) ∧ IsUnit ((algebraMap S T) ((algebraMap R S) x))

Tactic:
exact ⟨algebraMap_isUnit _, IsUnit.map _ (algebraMap_isUnit x)⟩

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s : Set R
⊢ s ⊆ ↑(span s)

Tactic:
intro x

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s : Set R
x : R
⊢ x ∈ s → x ∈ ↑(span s)
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s : Set R
x : R
h : x ∈ { ringCon := sInf {s_1 | ∀ (x y : R), x - y ∈ s → s_1 x y} }
I : TwoSidedIdeal R
hI : s ⊆ ↑I
⊢ I.ringCon ∈ {s_1 | ∀ (x y : R), x - y ∈ s → s_1 x y}

Tactic:
intro x

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s : Set R
x✝ : R
h : x✝ ∈ { ringCon := sInf {s_1 | ∀ (x y : R), x - y ∈ s → s_1 x y} }
I : TwoSidedIdeal R
hI : s ⊆ ↑I
x : R
⊢ ∀ (y : R), x - y ∈ s → I.ringCon x y
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s t : Set R
h : s ⊆ t
⊢ span s ≤ span t

Tactic:
intro x

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
s t : Set R
h : s ⊆ t
x : R
⊢ x ∈ span s → x ∈ span t
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
F : Type u_3
inst✝¹ : FunLike F R S
f : F
inst✝ : NonUnitalRingHomClass F R S
I J : TwoSidedIdeal S
h : ↑I ⊆ ↑J
⊢ (fun I ↦ { ringCon := I.ringCon.comap f }) I ≤ (fun I ↦ { ringCon := I.ringCon.comap f }) J

Tactic:
intro x

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocRing S
F : Type u_3
inst✝¹ : FunLike F R S
f : F
inst✝ : NonUnitalRingHomClass F R S
I J : TwoSidedIdeal S
h : ↑I ⊆ ↑J
x : R
⊢ x ∈ (fun I ↦ { ringCon := I.ringCon.comap f }) I → x ∈ (fun I ↦ { ringCon := I.ringCon.comap f }) J
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommSemiring R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
x z : R
y : S
inst✝⁵ : Away x S
T : Type u_4
inst✝⁴ : CommRing T
inst✝³ : Algebra S T
inst✝² : Algebra R T
inst✝¹ : IsScalarTower R S T
inst✝ : Away y T
h : Associated ((algebraMap R S) z) y
this : Away ((algebraMap R S) z) T
⊢ Away (x * z) T

Tactic:
exact .mul' S _ _ _

Goal state after:
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
e : R
he : IsIdempotentElem e
inst✝ : Away e S
⊢ Function.Surjective ⇑(algebraMap R S)

Tactic:
intro x

Goal state after:
R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
e : R
he : IsIdempotentElem e
inst✝ : Away e S
x : S
⊢ ∃ a, (algebraMap R S) a = x
Module: Mathlib.RingTheory.TwoSidedIdeal.Operations

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : Ring R
s : Set R
z : R
⊢ ∀ (x y : R), y ∈ univ * s * univ → x * y ∈ univ * s * univ

Tactic:
intro x

Goal state after:
case refine_1
R : Type u_1
inst✝ : Ring R
s : Set R
z x : R
⊢ ∀ y ∈ univ * s * univ, x * y ∈ univ * s * univ
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: R : Type u
inst✝ : Ring R
I : Ideal R
x : R
hx : x ∈ I.jacobson
y : R
hxy : I ⊔ span {y * x + 1} = ⊤
p : R
hpi : p ∈ I
q : R
hq : q ∈ span {y * x + 1}
hpq : p + q = 1
r : R
hr : r * (y * x + 1) = q
⊢ q - (p + q) ∈ I

Tactic:
← neg_sub,

Goal state after:
R : Type u
inst✝ : Ring R
I : Ideal R
x : R
hx : x ∈ I.jacobson
y : R
hxy : I ⊔ span {y * x + 1} = ⊤
p : R
hpi : p ∈ I
q : R
hq : q ∈ span {y * x + 1}
hpq : p + q = 1
r : R
hr : r * (y * x + 1) = q
⊢ -(p + q - q) ∈ I
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I : Ideal R
hi : I.IsLocal
x : R
h : I ⊔ span {x} = ⊤
p : R
hpi : p ∈ I
q : R
hq : q ∈ span {x}
hpq : p + q = 1
r : R
hr : q = x * r
⊢ q - (p + q) ∈ I

Tactic:
← neg_sub,

Goal state after:
R : Type u
inst✝ : CommRing R
I : Ideal R
hi : I.IsLocal
x : R
h : I ⊔ span {x} = ⊤
p : R
hpi : p ∈ I
q : R
hq : q ∈ span {x}
hpq : p + q = 1
r : R
hr : q = x * r
⊢ -(p + q - q) ∈ I
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: R : Type u
inst✝ : Ring R
I : TwoSidedIdeal R
⊢ asIdeal I.jacobson = (asIdeal I).jacobson

Tactic:
by
  ext; simp [jacobson]

Goal state after:
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
s : Finset R
f : (a : ↑↑s) → Away ↑a
h : ∀ (a b : ↑↑s), (Away.awayToAwayRight ↑a ↑b) (f a) = (Away.awayToAwayLeft ↑b ↑a) (f b)
mem : 1 ∈ Ideal.span ↑s
span_eq : Ideal.span ↑s = ⊤
n : ↑↑s → ℕ
r✝¹ : ↑↑s → R
eq✝¹ : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) ↑a ^ n a = (algebraMap R (Away ↑a)) (r✝¹ a)
N✝ : ℕ := s.attach.sup n
r✝ : ↑↑s → R := fun a ↦ ↑a ^ (N✝ - n a) * r✝¹ a
eq✝ : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) (↑a ^ N✝) = (algebraMap R (Away ↑a)) (r✝ a)
N'✝ : ↑↑s → ↑↑s → ℕ
hN' : ∀ (a b : ↑↑s), (↑a * ↑b) ^ N'✝ a b * (r✝ a * ↑b ^ N✝) = (↑a * ↑b) ^ N'✝ a b * (r✝ b * ↑a ^ N✝)
N' : ℕ := (s ×ˢ s).attach.sup fun a ↦ N'✝ ⟨(↑a).1, ⋯⟩ ⟨(↑a).2, ⋯⟩
eq2 : ∀ (a b : ↑↑s), (↑a * ↑b) ^ N' * (r✝ a * ↑b ^ N✝) = (↑a * ↑b) ^ N' * (r✝ b * ↑a ^ N✝)
N : ℕ := N' + N✝
r : ↑↑s → R := fun a ↦ ↑a ^ N' * r✝ a
eq : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) (↑a ^ N) = (algebraMap R (Away ↑a)) (r a)
a b : ↑↑s
⊢ r a * (↑b ^ N' * ↑b ^ N✝) = r b * ↑a ^ N

Tactic:
mul_mul_mul_comm,

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
s : Finset R
f : (a : ↑↑s) → Away ↑a
h : ∀ (a b : ↑↑s), (Away.awayToAwayRight ↑a ↑b) (f a) = (Away.awayToAwayLeft ↑b ↑a) (f b)
mem : 1 ∈ Ideal.span ↑s
span_eq : Ideal.span ↑s = ⊤
n : ↑↑s → ℕ
r✝¹ : ↑↑s → R
eq✝¹ : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) ↑a ^ n a = (algebraMap R (Away ↑a)) (r✝¹ a)
N✝ : ℕ := s.attach.sup n
r✝ : ↑↑s → R := fun a ↦ ↑a ^ (N✝ - n a) * r✝¹ a
eq✝ : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) (↑a ^ N✝) = (algebraMap R (Away ↑a)) (r✝ a)
N'✝ : ↑↑s → ↑↑s → ℕ
hN' : ∀ (a b : ↑↑s), (↑a * ↑b) ^ N'✝ a b * (r✝ a * ↑b ^ N✝) = (↑a * ↑b) ^ N'✝ a b * (r✝ b * ↑a ^ N✝)
N' : ℕ := (s ×ˢ s).attach.sup fun a ↦ N'✝ ⟨(↑a).1, ⋯⟩ ⟨(↑a).2, ⋯⟩
eq2 : ∀ (a b : ↑↑s), (↑a * ↑b) ^ N' * (r✝ a * ↑b ^ N✝) = (↑a * ↑b) ^ N' * (r✝ b * ↑a ^ N✝)
N : ℕ := N' + N✝
r : ↑↑s → R := fun a ↦ ↑a ^ N' * r✝ a
eq : ∀ (a : ↑↑s), f a * (algebraMap R (Away ↑a)) (↑a ^ N) = (algebraMap R (Away ↑a)) (r a)
a b : ↑↑s
⊢ ↑a ^ N' * ↑b ^ N' * (r✝ a * ↑b ^ N✝) = r b * ↑a ^ N