mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: case hr
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
⊢ (lTensor (A × B) counit ∘ₗ TensorProduct.map (inr R A B) (inr R A B)) ∘ₗ comul =
    (TensorProduct.mk R (A × B) R).flip 1 ∘ₗ inr R A B

Tactic:
lTensor_comp_map,

Goal state after:
case hr
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.map (inr R A B) (counit ∘ₗ inr R A B) ∘ₗ comul = (TensorProduct.mk R (A × B) R).flip 1 ∘ₗ inr R A B
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 =
    (lTensor (Π₀ (i : ι), A i) comul ∘ₗ TensorProduct.map (lsingle i) (lsingle i)) ∘ₗ comul

Tactic:
lTensor_comp_map,

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) (comul ∘ₗ 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✝ : ι
⊢ (lTensor (Π₀ (i : ι), A i) counit ∘ₗ TensorProduct.map (lsingle i✝) (lsingle i✝)) ∘ₗ comul =
    (TensorProduct.mk R (Π₀ (i : ι), A i) R).flip 1 ∘ₗ lsingle i✝

Tactic:
lTensor_comp_map,

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.map (lsingle i✝) (counit ∘ₗ 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) ∘ₗ
        TensorProduct.map (lsingle i) (lsingle i)) ∘ₗ
      comul =
    (lTensor (ι →₀ A) comul ∘ₗ TensorProduct.map (lsingle i) (lsingle i)) ∘ₗ comul

Tactic:
lTensor_comp_map,

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) (comul ∘ₗ 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
a✝ : ι
⊢ (lTensor (ι →₀ A) counit ∘ₗ TensorProduct.map (lsingle a✝) (lsingle a✝)) ∘ₗ comul =
    (TensorProduct.mk R (ι →₀ A) R).flip 1 ∘ₗ lsingle a✝

Tactic:
lTensor_comp_map,

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✝ : ι
⊢ TensorProduct.map (lsingle a✝) (counit ∘ₗ lsingle a✝) ∘ₗ comul = (TensorProduct.mk R (ι →₀ A) R).flip 1 ∘ₗ lsingle a✝
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
A : n → Type u_3
inst✝² : (i : n) → AddCommMonoid (A i)
inst✝¹ : (i : n) → Module R (A i)
inst✝ : (i : n) → Coalgebra R (A i)
i✝ : n
⊢ ((↑(TensorProduct.assoc R ((i : n) → A i) ((i : n) → A i) ((i : n) → A i)) ∘ₗ rTensor ((i : n) → A i) comul) ∘ₗ
        map (LinearMap.single R A i✝) (LinearMap.single R A i✝)) ∘ₗ
      comul =
    (lTensor ((i : n) → A i) comul ∘ₗ map (LinearMap.single R A i✝) (LinearMap.single R A i✝)) ∘ₗ comul

Tactic:
lTensor_comp_map,

Goal state after:
R : Type u_1
n : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
A : n → Type u_3
inst✝² : (i : n) → AddCommMonoid (A i)
inst✝¹ : (i : n) → Module R (A i)
inst✝ : (i : n) → Coalgebra R (A i)
i✝ : n
⊢ ((↑(TensorProduct.assoc R ((i : n) → A i) ((i : n) → A i) ((i : n) → A i)) ∘ₗ rTensor ((i : n) → A i) comul) ∘ₗ
        map (LinearMap.single R A i✝) (LinearMap.single R A i✝)) ∘ₗ
      comul =
    map (LinearMap.single R A i✝) (comul ∘ₗ LinearMap.single R A i✝) ∘ₗ comul
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
A : n → Type u_3
inst✝² : (i : n) → AddCommMonoid (A i)
inst✝¹ : (i : n) → Module R (A i)
inst✝ : (i : n) → Coalgebra R (A i)
i✝ : n
⊢ (lTensor ((i : n) → A i) counit ∘ₗ map (LinearMap.single R A i✝) (LinearMap.single R A i✝)) ∘ₗ comul =
    (TensorProduct.mk R ((i : n) → A i) R).flip 1 ∘ₗ LinearMap.single R A i✝

Tactic:
lTensor_comp_map,

Goal state after:
R : Type u_1
n : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
A : n → Type u_3
inst✝² : (i : n) → AddCommMonoid (A i)
inst✝¹ : (i : n) → Module R (A i)
inst✝ : (i : n) → Coalgebra R (A i)
i✝ : n
⊢ map (LinearMap.single R A i✝) (counit ∘ₗ LinearMap.single R A i✝) ∘ₗ comul =
    (TensorProduct.mk R ((i : n) → A i) R).flip 1 ∘ₗ LinearMap.single R A i✝
Module: Mathlib.Algebra.Ring.BooleanRing

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : BooleanRing α
inst✝¹ : BooleanRing β
inst✝ : BooleanRing γ
f : α →+* β
a b : AsBoolAlg α
⊢ (⇑toBoolAlg ∘ ⇑f ∘ ⇑ofBoolAlg) (a ⊔ b) = (⇑toBoolAlg ∘ ⇑f ∘ ⇑ofBoolAlg) a ⊔ (⇑toBoolAlg ∘ ⇑f ∘ ⇑ofBoolAlg) b

Tactic:
dsimp
    simp_rw [map_add f, map_mul f, toBoolAlg_add_add_mul]

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

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

Tactic:
simp only [← LinearMap.comp_assoc]

Goal state after:
R : Type u_1
M : Type u_3
N : Type u_4
M' : Type u_6
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Coalgebra R M
f : M →ₗ[R] M'
g : N →ₗ[R] M
⊢ ((α ∘ₗ δ ⊗ₘ f) ∘ₗ δ) ∘ₗ g = ((LinearMap.id ⊗ₘ (LinearMap.id ⊗ₘ f) ∘ₗ LinearMap.id ⊗ₘ δ) ∘ₗ δ) ∘ₗ g
Module: Mathlib.RingTheory.Coalgebra.CoassocSimps

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

Tactic:
simp only [← LinearMap.comp_assoc]

Goal state after:
R : Type u_1
M : Type u_3
N : Type u_4
M' : Type u_6
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Coalgebra R M
f : M →ₗ[R] M'
g : N →ₗ[R] M
⊢ ((α⁻¹ ∘ₗ f ⊗ₘ δ) ∘ₗ δ) ∘ₗ g = (((f ⊗ₘ LinearMap.id) ⊗ₘ LinearMap.id ∘ₗ δ ⊗ₘ LinearMap.id) ∘ₗ δ) ∘ₗ g
Module: Mathlib.RingTheory.Coalgebra.CoassocSimps

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : Coalgebra R M
f : M →ₗ[R] N
⊢ α ∘ₗ (β ⊗ₘ f ∘ₗ LinearMap.rTensor M δ) ∘ₗ δ =
    LinearMap.lTensor M (LinearMap.lTensor M (f ∘ₗ LinearMap.id) ∘ₗ β) ∘ₗ α ∘ₗ β ∘ₗ α ∘ₗ LinearMap.rTensor M δ ∘ₗ δ

Tactic:
simp only [← LinearMap.comp_assoc]

Goal state after:
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : Coalgebra R M
f : M →ₗ[R] N
⊢ ((α ∘ₗ β ⊗ₘ f) ∘ₗ LinearMap.rTensor M δ) ∘ₗ δ =
    ((((LinearMap.lTensor M (LinearMap.lTensor M (f ∘ₗ LinearMap.id) ∘ₗ β) ∘ₗ α) ∘ₗ β) ∘ₗ α) ∘ₗ
        LinearMap.rTensor M δ) ∘ₗ
      δ
Module: Mathlib.Algebra.Category.Ring.Adjunctions

Goal state before:
pp: R : CommRingCat
X✝ Y✝ Z✝ : CommMonCat
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ Hom.hom (Under.Hom.right (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom (f ≫ g)))) ⋯)) =
    Hom.hom
      (Under.Hom.right
        (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom f))) ⋯ ≫
          Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom g))) ⋯))

Tactic:
apply MonoidAlgebra.ringHom_ext

Goal state after:
case h₁
R : CommRingCat
X✝ Y✝ Z✝ : CommMonCat
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ∀ (r : ↑R),
    (Hom.hom
          (Under.Hom.right (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom (f ≫ g)))) ⋯)))
        (MonoidAlgebra.single 1 r) =
      (Hom.hom
          (Under.Hom.right
            (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom f))) ⋯ ≫
              Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom g))) ⋯)))
        (MonoidAlgebra.single 1 r)

case h_of
R : CommRingCat
X✝ Y✝ Z✝ : CommMonCat
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ∀ (m : ↑X✝),
    (Hom.hom
          (Under.Hom.right (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom (f ≫ g)))) ⋯)))
        (MonoidAlgebra.single m 1) =
      (Hom.hom
          (Under.Hom.right
            (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom f))) ⋯ ≫
              Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom g))) ⋯)))
        (MonoidAlgebra.single m 1)
Module: Mathlib.Algebra.Category.Ring.Adjunctions

Goal state before:
pp: R : CommRingCat
X✝ Y✝ Z✝ : CommMonCat
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ Hom.hom (Under.Hom.right (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom (f ≫ g)))) ⋯)) =
    Hom.hom
      (Under.Hom.right
        (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom f))) ⋯ ≫
          Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom g))) ⋯))

Tactic:
apply MonoidAlgebra.ringHom_ext <;> intro

Goal state after:
case h₁
R : CommRingCat
X✝ Y✝ Z✝ : CommMonCat
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
r✝ : ↑R
⊢ (Hom.hom (Under.Hom.right (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom (f ≫ g)))) ⋯)))
      (MonoidAlgebra.single 1 r✝) =
    (Hom.hom
        (Under.Hom.right
          (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom f))) ⋯ ≫
            Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom g))) ⋯)))
      (MonoidAlgebra.single 1 r✝)

case h_of
R : CommRingCat
X✝ Y✝ Z✝ : CommMonCat
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
m✝ : ↑X✝
⊢ (Hom.hom (Under.Hom.right (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom (f ≫ g)))) ⋯)))
      (MonoidAlgebra.single m✝ 1) =
    (Hom.hom
        (Under.Hom.right
          (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom f))) ⋯ ≫
            Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R) (CommMonCat.Hom.hom g))) ⋯)))
      (MonoidAlgebra.single m✝ 1)
Module: Mathlib.Algebra.Category.Ring.Adjunctions

Goal state before:
pp: R : CommRingCat
S T : Under R
f : S ⟶ T
⊢ Hom.hom
      (Under.Hom.right
        (((Under.forget R ⋙ forget₂ CommRingCat CommMonCat) ⋙ R.monoidAlgebra).map f ≫
          Under.homMk
            (ofHom
              (MonoidAlgebra.liftNCRingHom (Hom.hom T.hom)
                (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj T)) ⋯))
            ⋯)) =
    Hom.hom
      (Under.Hom.right
        (Under.homMk
            (ofHom
              (MonoidAlgebra.liftNCRingHom (Hom.hom S.hom)
                (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S)) ⋯))
            ⋯ ≫
          (𝟭 (Under R)).map f))

Tactic:
apply MonoidAlgebra.ringHom_ext

Goal state after:
case h₁
R : CommRingCat
S T : Under R
f : S ⟶ T
⊢ ∀ (r : ↑R),
    (Hom.hom
          (Under.Hom.right
            (((Under.forget R ⋙ forget₂ CommRingCat CommMonCat) ⋙ R.monoidAlgebra).map f ≫
              Under.homMk
                (ofHom
                  (MonoidAlgebra.liftNCRingHom (Hom.hom T.hom)
                    (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj T)) ⋯))
                ⋯)))
        (MonoidAlgebra.single 1 r) =
      (Hom.hom
          (Under.Hom.right
            (Under.homMk
                (ofHom
                  (MonoidAlgebra.liftNCRingHom (Hom.hom S.hom)
                    (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S)) ⋯))
                ⋯ ≫
              (𝟭 (Under R)).map f)))
        (MonoidAlgebra.single 1 r)

case h_of
R : CommRingCat
S T : Under R
f : S ⟶ T
⊢ ∀ (m : ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S)),
    (Hom.hom
          (Under.Hom.right
            (((Under.forget R ⋙ forget₂ CommRingCat CommMonCat) ⋙ R.monoidAlgebra).map f ≫
              Under.homMk
                (ofHom
                  (MonoidAlgebra.liftNCRingHom (Hom.hom T.hom)
                    (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj T)) ⋯))
                ⋯)))
        (MonoidAlgebra.single m 1) =
      (Hom.hom
          (Under.Hom.right
            (Under.homMk
                (ofHom
                  (MonoidAlgebra.liftNCRingHom (Hom.hom S.hom)
                    (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S)) ⋯))
                ⋯ ≫
              (𝟭 (Under R)).map f)))
        (MonoidAlgebra.single m 1)
Module: Mathlib.Algebra.Category.Ring.Adjunctions

Goal state before:
pp: R : CommRingCat
G : CommMonCat
⊢ Hom.hom
      (Under.Hom.right
        (R.monoidAlgebra.map ({ app := fun G ↦ CommMonCat.ofHom (MonoidAlgebra.of ↑R ↑G), naturality := ⋯ }.app G) ≫
          {
                app := fun S ↦
                  Under.homMk
                    (ofHom
                      (MonoidAlgebra.liftNCRingHom (Hom.hom S.hom)
                        (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S)) ⋯))
                    ⋯,
                naturality := ⋯ }.app
            (R.monoidAlgebra.obj G))) =
    Hom.hom (Under.Hom.right (𝟙 (R.monoidAlgebra.obj G)))

Tactic:
apply MonoidAlgebra.ringHom_ext

Goal state after:
case h₁
R : CommRingCat
G : CommMonCat
⊢ ∀ (r : ↑R),
    (Hom.hom
          (Under.Hom.right
            (R.monoidAlgebra.map ({ app := fun G ↦ CommMonCat.ofHom (MonoidAlgebra.of ↑R ↑G), naturality := ⋯ }.app G) ≫
              {
                    app := fun S ↦
                      Under.homMk
                        (ofHom
                          (MonoidAlgebra.liftNCRingHom (Hom.hom S.hom)
                            (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S)) ⋯))
                        ⋯,
                    naturality := ⋯ }.app
                (R.monoidAlgebra.obj G))))
        (MonoidAlgebra.single 1 r) =
      (Hom.hom (Under.Hom.right (𝟙 (R.monoidAlgebra.obj G)))) (MonoidAlgebra.single 1 r)

case h_of
R : CommRingCat
G : CommMonCat
⊢ ∀ (m : ↑G),
    (Hom.hom
          (Under.Hom.right
            (R.monoidAlgebra.map ({ app := fun G ↦ CommMonCat.ofHom (MonoidAlgebra.of ↑R ↑G), naturality := ⋯ }.app G) ≫
              {
                    app := fun S ↦
                      Under.homMk
                        (ofHom
                          (MonoidAlgebra.liftNCRingHom (Hom.hom S.hom)
                            (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S)) ⋯))
                        ⋯,
                    naturality := ⋯ }.app
                (R.monoidAlgebra.obj G))))
        (MonoidAlgebra.single m 1) =
      (Hom.hom (Under.Hom.right (𝟙 (R.monoidAlgebra.obj G)))) (MonoidAlgebra.single m 1)
Module: Mathlib.Algebra.Category.Ring.Adjunctions

Goal state before:
pp: R : CommRingCat
G : CommMonCat
⊢ Hom.hom
      (Under.Hom.right
        (R.monoidAlgebra.map ({ app := fun G ↦ CommMonCat.ofHom (MonoidAlgebra.of ↑R ↑G), naturality := ⋯ }.app G) ≫
          {
                app := fun S ↦
                  Under.homMk
                    (ofHom
                      (MonoidAlgebra.liftNCRingHom (Hom.hom S.hom)
                        (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S)) ⋯))
                    ⋯,
                naturality := ⋯ }.app
            (R.monoidAlgebra.obj G))) =
    Hom.hom (Under.Hom.right (𝟙 (R.monoidAlgebra.obj G)))

Tactic:
apply MonoidAlgebra.ringHom_ext <;> intro

Goal state after:
case h₁
R : CommRingCat
G : CommMonCat
r✝ : ↑R
⊢ (Hom.hom
        (Under.Hom.right
          (R.monoidAlgebra.map ({ app := fun G ↦ CommMonCat.ofHom (MonoidAlgebra.of ↑R ↑G), naturality := ⋯ }.app G) ≫
            {
                  app := fun S ↦
                    Under.homMk
                      (ofHom
                        (MonoidAlgebra.liftNCRingHom (Hom.hom S.hom)
                          (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S)) ⋯))
                      ⋯,
                  naturality := ⋯ }.app
              (R.monoidAlgebra.obj G))))
      (MonoidAlgebra.single 1 r✝) =
    (Hom.hom (Under.Hom.right (𝟙 (R.monoidAlgebra.obj G)))) (MonoidAlgebra.single 1 r✝)

case h_of
R : CommRingCat
G : CommMonCat
m✝ : ↑G
⊢ (Hom.hom
        (Under.Hom.right
          (R.monoidAlgebra.map ({ app := fun G ↦ CommMonCat.ofHom (MonoidAlgebra.of ↑R ↑G), naturality := ⋯ }.app G) ≫
            {
                  app := fun S ↦
                    Under.homMk
                      (ofHom
                        (MonoidAlgebra.liftNCRingHom (Hom.hom S.hom)
                          (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S)) ⋯))
                      ⋯,
                  naturality := ⋯ }.app
              (R.monoidAlgebra.obj G))))
      (MonoidAlgebra.single m✝ 1) =
    (Hom.hom (Under.Hom.right (𝟙 (R.monoidAlgebra.obj G)))) (MonoidAlgebra.single m✝ 1)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity

Goal state before:
pp: R : Type u_2
inst✝³ : CommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
α : Type u_3
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : Subsingleton Rˣ
f : α → M
g : α → R
hgi : Function.Injective g
hg : ∀ (s : α), Irreducible (g s)
r : R
hr : r ≠ 0
⊢ Function.HasFiniteMulSupport fun s ↦ f s ^ Multiset.count (g s) (normalizedFactors r)

Tactic:
fun_prop

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
r r' : R
h : Associated r r'
inst✝ : Away r S
⊢ Away r' S

Tactic:
by
  obtain ⟨u, rfl⟩ := h
  refine mk _ ?_ (fun s ↦ ?_) (fun a b hab ↦ ?_)
  · simp [algebraMap_isUnit r, IsUnit.map _ u.isUnit]
  · obtain ⟨n, a, hn⟩ := surj r s
    use n, a * u ^ n
    simp [mul_pow, ← mul_assoc, hn]
  · obtain ⟨n, hn⟩ := exists_of_eq r hab
    use n
    rw [mul_pow, mul_comm (r ^ n), mul_assoc, mul_assoc, hn]

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

Goal state before:
pp: case h
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
z : T
m : ℕ
p : S
hpq : z * (algebraMap S T) ((algebraMap R S) y) ^ m = (algebraMap S T) p
n : ℕ
a : R
hab : p * (algebraMap R S) x ^ n = (algebraMap R S) a
⊢ z * (algebraMap R T) (y * x) ^ (m + n) = (algebraMap R T) (a * x ^ m * y ^ n)

Tactic:
simp only [mul_pow, pow_add, map_pow, map_mul, ← mul_assoc, hpq,
      IsScalarTower.algebraMap_apply R S T, ← hab]

Goal state after:
case h
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
z : T
m : ℕ
p : S
hpq : z * (algebraMap S T) ((algebraMap R S) y) ^ m = (algebraMap S T) p
n : ℕ
a : R
hab : p * (algebraMap R S) x ^ n = (algebraMap R S) a
⊢ (algebraMap S T) p * (algebraMap S T) ((algebraMap R S) x) ^ m * (algebraMap S T) ((algebraMap R S) y) ^ n *
      (algebraMap S T) ((algebraMap R S) x) ^ n =
    (algebraMap S T) p * (algebraMap S T) ((algebraMap R S) x) ^ n * (algebraMap S T) ((algebraMap R S) x) ^ m *
      (algebraMap S T) ((algebraMap R S) y) ^ n
Module: Mathlib.RingTheory.Localization.Away.Basic

Goal state before:
pp: S : Type u_2
inst✝¹ : CommSemiring S
R : Type u_4
inst✝ : CommRing R
f : R →+* S
a : R
H : ∀ (a_1 : R), f a_1 = 0 → ∃ n, a ^ n * a_1 = 0
b x : R
hx : f x = 0
n : ℕ
hn : a ^ n * x = 0
⊢ (a * b) ^ n * x = 0

Tactic:
by simp [mul_pow, mul_assoc, mul_left_comm (a ^ n), hn]

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
f : R →+* S
a b : R
H : ∀ (a_1 : S), ∃ b_1 m, f b_1 = f (a * b) ^ m * a_1
this : ∀ (s : S) (n : ℕ), ∃ c l m k, f (a ^ (k + n) * c) = f (a ^ (k + l) * b ^ m) * s
⊢ ∀ (a_1 : Away (f a)), ∃ b_1 m, (awayMap f a) b_1 = (awayMap f a) ((algebraMap R (Away a)) b) ^ m * a_1

Tactic:
simpa [Function.Surjective, (IsLocalization.mk'_surjective (.powers (f a))).forall, ← map_pow,
      (IsLocalization.mk'_surjective (.powers a)).exists, Submonoid.mem_powers_iff, pow_add,
      Localization.awayMap, IsLocalization.Away.map, IsLocalization.map_mk', ← mul_assoc,
      IsLocalization.mk'_eq_iff_eq, ← map_mul, IsLocalization.eq_iff_exists (.powers (f a)),
      IsLocalization.mul_mk'_eq_mk'_of_mul]

Goal state after:
Module: Mathlib.RingTheory.Jacobson.Ideal

Goal state before:
pp: case mp
R : Type u
inst✝ : CommRing R
I : Ideal R
hf : Function.Surjective ⇑(Quotient.mk I)
h : map (Quotient.mk I) I.jacobson = map (Quotient.mk I) I
⊢ ⊥.jacobson = ⊥

Tactic:
rw [map_jacobson_of_surjective hf (le_of_eq mk_ker)] at h

Goal state after:
case mp
R : Type u
inst✝ : CommRing R
I : Ideal R
hf : Function.Surjective ⇑(Quotient.mk I)
h : (map (Quotient.mk I) I).jacobson = map (Quotient.mk I) I
⊢ ⊥.jacobson = ⊥
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: R : Type u_1
inst✝¹⁷ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝¹⁶ : AddCommMonoid M
inst✝¹⁵ : AddCommMonoid M'
inst✝¹⁴ : Module R M
inst✝¹³ : Module R M'
f : M →ₗ[R] M'
inst✝¹² : IsLocalizedModule S f
N : Type ?u.31
N' : Type ?u.33
inst✝¹¹ : AddCommMonoid N
inst✝¹⁰ : AddCommMonoid N'
inst✝⁹ : Module R N
inst✝⁸ : Module R N'
g : N →ₗ[R] N'
inst✝⁷ : IsLocalizedModule S g
Rₛ : Type ?u.52
inst✝⁶ : CommSemiring Rₛ
inst✝⁵ : Algebra R Rₛ
inst✝⁴ : Module Rₛ M'
inst✝³ : Module Rₛ N'
inst✝² : IsScalarTower R Rₛ M'
inst✝¹ : IsScalarTower R Rₛ N'
inst✝ : IsLocalization S Rₛ
e : M ≃ₗ[R] N
⊢ (mapExtendScalars S f g Rₛ) ↑e ∘ₗ (mapExtendScalars S g f Rₛ) ↑e.symm = LinearMap.id

Tactic:
by
      apply LinearMap.restrictScalars_injective R
      apply IsLocalizedModule.linearMap_ext S g g
      ext; simp

Goal state after: