mathlib-initiative/mathlib-tactics huggingface dataset:
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:
congr 1

Goal state after:
case e_f
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 ⊗ₘ δ) ∘ₗ δ = ((f ⊗ₘ LinearMap.id) ⊗ₘ LinearMap.id ∘ₗ δ ⊗ₘ LinearMap.id) ∘ₗ δ
Module: Mathlib.RingTheory.Coalgebra.CoassocSimps

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

Tactic:
congr 1

Goal state after:
case e_f
R : Type u_1
M : Type u_3
N : Type u_4
Q : Type u_9
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
inst✝² : AddCommMonoid Q
inst✝¹ : Module R Q
inst✝ : Coalgebra R M
f : M →ₗ[R] N
h : Q →ₗ[R] M
⊢ (α ∘ₗ (β ∘ₗ δ) ⊗ₘ f) ∘ₗ δ = (((LinearMap.id ⊗ₘ (LinearMap.id ⊗ₘ f ∘ₗ β) ∘ₗ α) ∘ₗ δ ⊗ₘ LinearMap.id) ∘ₗ β) ∘ₗ δ
Module: Mathlib.GroupTheory.MonoidLocalization.Away

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
g : M →* P
hg✝ : ∀ (y : ↥S), IsUnit (g ↑y)
x : M
F : AwayMap x N
hg : IsUnit (g x)
y : ↥(powers x)
⊢ IsUnit (g ↑y)

Tactic:
obtain ⟨n, hn⟩ := y.2
      rw [← hn, g.map_pow]
      exact IsUnit.pow n hg

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
⊢ sInf {J | J.IsMaximal} = sInf {m | IsCoatom m}

Tactic:
isMaximal_def

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.StrictInitial

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
I : C
h : ∀ (A : C) (f : I ⟶ A), IsIso f
I' A : C
f : I' ⟶ A
hI' : IsTerminal I'
this : IsIso (hI'.from I ≫ f)
⊢ inv (hI'.from I ≫ f) ≫ hI'.from I ≫ f = 𝟙 A

Tactic:
IsIso.inv_hom_id

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
I : C
h : ∀ (A : C) (f : I ⟶ A), IsIso f
I' A : C
f : I' ⟶ A
hI' : IsTerminal I'
this : IsIso (hI'.from I ≫ f)
⊢ 𝟙 A = 𝟙 A
Module: Mathlib.RingTheory.Localization.Module

Goal state before:
pp: R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommSemiring R
S : Submonoid R
inst✝⁹ : CommSemiring Rₛ
inst✝⁸ : Algebra R Rₛ
inst✝⁷ : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid Mₛ
inst✝³ : Module R Mₛ
inst✝² : Module Rₛ Mₛ
inst✝¹ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
ι : Type u_5
v : ι → M
hv : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
t : Finset ι
⊢ ∀ (f_1 g : ι → Rₛ), ∑ i ∈ t, f_1 i • (⇑f ∘ v) i = ∑ i ∈ t, g i • (⇑f ∘ v) i → ∀ i ∈ t, f_1 i = g i

Tactic:
g₁

Goal state after:
R : Type u_1
Rₛ : Type u_2
inst✝¹⁰ : CommSemiring R
S : Submonoid R
inst✝⁹ : CommSemiring Rₛ
inst✝⁸ : Algebra R Rₛ
inst✝⁷ : IsLocalization S Rₛ
M : Type u_3
Mₛ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid Mₛ
inst✝³ : Module R Mₛ
inst✝² : Module Rₛ Mₛ
inst✝¹ : IsScalarTower R Rₛ Mₛ
f : M →ₗ[R] Mₛ
inst✝ : IsLocalizedModule S f
ι : Type u_5
v : ι → M
hv : ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
t : Finset ι
g₁ : ι → Rₛ
⊢ ∀ (g : ι → Rₛ), ∑ i ∈ t, g₁ i • (⇑f ∘ v) i = ∑ i ∈ t, g i • (⇑f ∘ v) i → ∀ i ∈ t, g₁ i = g i
Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts

Goal state before:
pp: case none
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ : C ⥤ D
F : Discrete WalkingPair ⥤ C
c : Cocone F
X : C
hX : IsInitial X
f : X ⟶ F.obj { as := WalkingPair.left }
g : X ⟶ F.obj { as := WalkingPair.right }
hc : IsColimit (PushoutCocone.mk (c.ι.app { as := WalkingPair.left }) (c.ι.app { as := WalkingPair.right }) ⋯)
s : Cocone F
m : c.pt ⟶ s.pt
J : ∀ (j : Discrete WalkingPair), c.ι.app j ≫ m = s.ι.app j
c' : PushoutCocone f g :=
  PushoutCocone.mk (c.ι.app { as := WalkingPair.left } ≫ m) (c.ι.app { as := WalkingPair.right } ≫ m) ⋯
⊢ f ≫ c.ι.app { as := WalkingPair.left } ≫ m =
    f ≫
      c.ι.app { as := WalkingPair.left } ≫
        hc.desc (PushoutCocone.mk (c.ι.app { as := WalkingPair.left } ≫ m) (c.ι.app { as := WalkingPair.right } ≫ m) ⋯)

Tactic:
congr 1

Goal state after:
case e_a
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ : C ⥤ D
F : Discrete WalkingPair ⥤ C
c : Cocone F
X : C
hX : IsInitial X
f : X ⟶ F.obj { as := WalkingPair.left }
g : X ⟶ F.obj { as := WalkingPair.right }
hc : IsColimit (PushoutCocone.mk (c.ι.app { as := WalkingPair.left }) (c.ι.app { as := WalkingPair.right }) ⋯)
s : Cocone F
m : c.pt ⟶ s.pt
J : ∀ (j : Discrete WalkingPair), c.ι.app j ≫ m = s.ι.app j
c' : PushoutCocone f g :=
  PushoutCocone.mk (c.ι.app { as := WalkingPair.left } ≫ m) (c.ι.app { as := WalkingPair.right } ≫ m) ⋯
⊢ c.ι.app { as := WalkingPair.left } ≫ m =
    c.ι.app { as := WalkingPair.left } ≫
      hc.desc (PushoutCocone.mk (c.ι.app { as := WalkingPair.left } ≫ m) (c.ι.app { as := WalkingPair.right } ≫ m) ⋯)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₃ Y₁ Y₂ Y₃ : C
g₁ : Y₁ ⟶ Y₂
g₂ : Y₂ ⟶ Y₃
i₃ : X₃ ⟶ Y₃
t₂ : PullbackCone g₂ i₃
i₂ : t₂.pt ⟶ Y₂
t₁ : PullbackCone g₁ i₂
hi₂ : i₂ = t₂.fst
H : IsLimit t₂
H' : IsLimit t₁
s : PullbackCone (g₁ ≫ g₂) i₃
l₂ : s.pt ⟶ t₂.pt
hl₂ : l₂ ≫ t₂.fst = s.fst ≫ g₁
hl₂' : l₂ ≫ t₂.snd = s.snd
l₁ : s.pt ⟶ t₁.pt
hl₁ : l₁ ≫ t₁.fst = s.fst
hl₁' : l₁ ≫ t₁.snd = l₂
m : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt
hm₁ : m ≫ (t₂.pasteHoriz t₁ hi₂).fst = s.fst
hm₂ : m ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd
⊢ m ≫ t₁.fst = l₁ ≫ t₁.fst

Tactic:
simpa [hl₁] using hm₁

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Goal state before:
pp: case refine_1.h₀
C : Type u
inst✝ : Category.{v, u} C
X₃ Y₁ Y₂ Y₃ : C
g₁ : Y₁ ⟶ Y₂
g₂ : Y₂ ⟶ Y₃
i₃ : X₃ ⟶ Y₃
t₂ : PullbackCone g₂ i₃
i₂ : t₂.pt ⟶ Y₂
t₁ : PullbackCone g₁ i₂
hi₂ : i₂ = t₂.fst
H : IsLimit t₂
H' : IsLimit (t₂.pasteHoriz t₁ hi₂)
s : PullbackCone g₁ i₂
l : s.pt ⟶ (t₂.pasteHoriz t₁ hi₂).pt
hl : l ≫ (t₂.pasteHoriz t₁ hi₂).fst = s.fst
hl' : l ≫ (t₂.pasteHoriz t₁ hi₂).snd = s.snd ≫ t₂.snd
⊢ (l ≫ t₁.snd) ≫ t₂.fst = s.snd ≫ t₂.fst

Tactic:
simp [← s.condition, ← hl, ← t₁.condition, ← hi₂]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case uniq
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
s : Cofork f f'
m : (Cofork.ofπ g ⋯).pt ⟶ s.pt
e : (Cofork.ofπ g ⋯).π ≫ m = s.π
⊢ m = H.isColimit.desc (PushoutCocone.mk s.π s.π ⋯)

Tactic:
apply PushoutCocone.IsColimit.hom_ext H.isColimit

Goal state after:
case uniq.h₀
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
s : Cofork f f'
m : (Cofork.ofπ g ⋯).pt ⟶ s.pt
e : (Cofork.ofπ g ⋯).π ≫ m = s.π
⊢ H.cocone.inl ≫ m = H.cocone.inl ≫ H.isColimit.desc (PushoutCocone.mk s.π s.π ⋯)

case uniq.h₁
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
s : Cofork f f'
m : (Cofork.ofπ g ⋯).pt ⟶ s.pt
e : (Cofork.ofπ g ⋯).π ≫ m = s.π
⊢ H.cocone.inr ≫ m = H.cocone.inr ≫ H.isColimit.desc (PushoutCocone.mk s.π s.π ⋯)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case h.h
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
x : T
m : M
s : ↥S
n : M
t : ↥S
⊢ mk (((IsLocalization.sec S x).1 * ↑(IsLocalization.sec S x).2) • (t • m + s • n))
      ((IsLocalization.sec S x).2 * (IsLocalization.sec S x).2 * (s * t)) =
    mk
      (((IsLocalization.sec S x).2 * t) • (IsLocalization.sec S x).1 • m +
        ((IsLocalization.sec S x).2 * s) • (IsLocalization.sec S x).1 • n)
      ((IsLocalization.sec S x).2 * s * ((IsLocalization.sec S x).2 * t))

Tactic:
congr 1

Goal state after:
case h.h.e_m
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
x : T
m : M
s : ↥S
n : M
t : ↥S
⊢ ((IsLocalization.sec S x).1 * ↑(IsLocalization.sec S x).2) • (t • m + s • n) =
    ((IsLocalization.sec S x).2 * t) • (IsLocalization.sec S x).1 • m +
      ((IsLocalization.sec S x).2 * s) • (IsLocalization.sec S x).1 • n

case e_s
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
x : T
m : M
s : ↥S
n : M
t : ↥S
⊢ (IsLocalization.sec S x).2 * (IsLocalization.sec S x).2 * (s * t) =
    (IsLocalization.sec S x).2 * s * ((IsLocalization.sec S x).2 * t)
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case h.h.e_m
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
x : T
m : M
s : ↥S
n : M
t : ↥S
⊢ ((IsLocalization.sec S x).1 * ↑(IsLocalization.sec S x).2) • (t • m + s • n) =
    ((IsLocalization.sec S x).2 * t) • (IsLocalization.sec S x).1 • m +
      ((IsLocalization.sec S x).2 * s) • (IsLocalization.sec S x).1 • n

Tactic:
simp only [Submonoid.smul_def, smul_add, ← mul_smul, Submonoid.coe_mul]

Goal state after:
case h.h.e_m
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
x : T
m : M
s : ↥S
n : M
t : ↥S
⊢ ((IsLocalization.sec S x).1 * ↑(IsLocalization.sec S x).2 * ↑t) • m +
      ((IsLocalization.sec S x).1 * ↑(IsLocalization.sec S x).2 * ↑s) • n =
    (↑(IsLocalization.sec S x).2 * ↑t * (IsLocalization.sec S x).1) • m +
      (↑(IsLocalization.sec S x).2 * ↑s * (IsLocalization.sec S x).1) • n
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: case refine_3
α : Type u
x : FreeCommRing α
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
hxs : x.IsSupported s
⊢ ∀ z ∈ of '' s,
    ∀ (n : FreeCommRing α),
      (map Subtype.val) ((restriction s) n) = n → (map Subtype.val) ((restriction s) (z * n)) = z * n

Tactic:
rintro _ ⟨p, hps, rfl⟩ n ih
    rw [map_mul, restriction_of, dif_pos hps, map_mul, map_of, ih]

Goal state after:
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: α : Type u
inst✝ : Subsingleton α
x y : FreeRing α
⊢ x * y = y * x

Tactic:
by
      rw [← (subsingletonEquivFreeCommRing α).symm_apply_apply (y * x),
        (subsingletonEquivFreeCommRing α).map_mul, mul_comm,
        ← (subsingletonEquivFreeCommRing α).map_mul,
        (subsingletonEquivFreeCommRing α).symm_apply_apply]

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

Goal state before:
pp: case h
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
x y : T
m : M
s : ↥S
⊢ mk
      ((((IsLocalization.sec S x).1 * ↑(IsLocalization.sec S y).2 +
            (IsLocalization.sec S y).1 * ↑(IsLocalization.sec S x).2) *
          ↑s) •
        m)
      ((IsLocalization.sec S x).2 * (IsLocalization.sec S y).2 * s * s) =
    mk
      ((((IsLocalization.sec S y).2 * s) • (IsLocalization.sec S x).1 +
          ((IsLocalization.sec S x).2 * s) • (IsLocalization.sec S y).1) •
        m)
      ((IsLocalization.sec S x).2 * s * ((IsLocalization.sec S y).2 * s))

Tactic:
congr 1

Goal state after:
case h.e_m
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
x y : T
m : M
s : ↥S
⊢ (((IsLocalization.sec S x).1 * ↑(IsLocalization.sec S y).2 +
          (IsLocalization.sec S y).1 * ↑(IsLocalization.sec S x).2) *
        ↑s) •
      m =
    (((IsLocalization.sec S y).2 * s) • (IsLocalization.sec S x).1 +
        ((IsLocalization.sec S x).2 * s) • (IsLocalization.sec S y).1) •
      m

case e_s
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type v
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
T : Type u_1
inst✝² : CommSemiring T
inst✝¹ : Algebra R T
inst✝ : IsLocalization S T
x y : T
m : M
s : ↥S
⊢ (IsLocalization.sec S x).2 * (IsLocalization.sec S y).2 * s * s =
    (IsLocalization.sec S x).2 * s * ((IsLocalization.sec S y).2 * s)
Module: Mathlib.Algebra.Group.Submonoid.Units

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H : Subgroup G
x : G
⊢ toUnits x ∈ H.units ↔ x ∈ H

Tactic:
mem_units_iff_val_mem,

Goal state after:
G : Type u_2
inst✝ : Group G
H : Subgroup G
x : G
⊢ ↑(toUnits x) ∈ H ↔ x ∈ H
Module: Mathlib.CategoryTheory.Monad.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Monad C
i : T.toFunctor ≅ F
X : C
⊢ T.map (i.inv.app (F.obj X)) ≫ T.map (T.map (i.inv.app X)) ≫ T.map (T.μ.app X) ≫ T.μ.app X ≫ i.hom.app X =
    T.map (i.inv.app (F.obj X)) ≫ T.μ.app (F.obj X) ≫ T.map (i.inv.app X) ≫ T.μ.app X ≫ i.hom.app X

Tactic:
congr 1

Goal state after:
case e_a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Monad C
i : T.toFunctor ≅ F
X : C
⊢ T.map (T.map (i.inv.app X)) ≫ T.map (T.μ.app X) ≫ T.μ.app X ≫ i.hom.app X =
    T.μ.app (F.obj X) ≫ T.map (i.inv.app X) ≫ T.μ.app X ≫ i.hom.app X
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
M'' : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ g (b' • a) + g (b • a') = ↑⋯.unit⁻¹ (g (↑(b * b') • a)) + ↑⋯.unit⁻¹ (↑(b * b') • g a')

Tactic:
congr 1

Goal state after:
case e_a
R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
M'' : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ g (b' • a) = ↑⋯.unit⁻¹ (g (↑(b * b') • a))

case e_a
R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
M'' : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ g (b • a') = ↑⋯.unit⁻¹ (↑(b * b') • g a')
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case h
R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
M'' : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
l : LocalizedModule S M →ₗ[R] M''
hl : l ∘ₗ mkLinearMap S M = g
m : M
s : ↥S
⊢ l (mk m 1) = l (mk (↑s • m) s)

Tactic:
congr 1

Goal state after:
case h.e_6
R : Type u_1
inst✝⁴ : CommSemiring R
S : Submonoid R
M : Type u_2
M'' : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M''
inst✝¹ : Module R M
inst✝ : Module R M''
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
l : LocalizedModule S M →ₗ[R] M''
hl : l ∘ₗ mkLinearMap S M = g
m : M
s : ↥S
⊢ mk m 1 = mk (↑s • m) s
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

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
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ f (b' • a) + f (b • a') = ↑⋯.unit⁻¹ (f (↑(b * b') • a)) + ↑⋯.unit⁻¹ (↑(b * b') • f a')

Tactic:
congr 1

Goal state after:
case e_a
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
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ f (b' • a) = ↑⋯.unit⁻¹ (f (↑(b * b') • a))

case e_a
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
x y : LocalizedModule S M
a a' : M
b b' : ↥S
⊢ f (b • a') = ↑⋯.unit⁻¹ (↑(b * b') • f a')
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: R S : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
R' S' : Type u
inst✝⁷ : CommRing R'
inst✝⁶ : CommRing S'
inst✝⁵ : Algebra R R'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R' S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : IsScalarTower R S S'
h : IsPushout (ofHom (algebraMap R R')) (ofHom (algebraMap R S)) (ofHom (algebraMap R' S')) (ofHom (algebraMap S S'))
e : R' ⊗[R] S ≃+* S' := (⋯.isoPushout ≪≫ h.isoPushout.symm).commRingCatIsoToRingEquiv
h2 :
  ∀ (r : R'),
    (ConcreteCategory.hom ⋯.isoPushout.hom) (r ⊗ₜ[R] 1) =
      (ConcreteCategory.hom (pushout.inl (ofHom (algebraMap R R')) (ofHom (algebraMap R S)))) r
h3 :
  ∀ (x : R'),
    (Hom.hom h.isoPushout.inv) ((Hom.hom (pushout.inl (ofHom (algebraMap R R')) (ofHom (algebraMap R S)))) x) =
      (algebraMap R' S') x
e' : R' ⊗[R] S ≃ₐ[R'] S' :=
  let __spread.0 := e;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
s : S
h1 :
  (ConcreteCategory.hom ⋯.isoPushout.hom) ((algebraMap S (R' ⊗[R] S)) s) =
    (ConcreteCategory.hom (pushout.inr (ofHom (algebraMap R R')) (ofHom (algebraMap R S)))) s
⊢ (e'.toRingEquiv.toRingHom.comp (algebraMap S (R' ⊗[R] S))) s = (algebraMap S S') s

Tactic:
have h4 (x : S) := congr($(h.inr_isoPushout_inv) x)

Goal state after:
R S : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
R' S' : Type u
inst✝⁷ : CommRing R'
inst✝⁶ : CommRing S'
inst✝⁵ : Algebra R R'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R' S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : IsScalarTower R S S'
h : IsPushout (ofHom (algebraMap R R')) (ofHom (algebraMap R S)) (ofHom (algebraMap R' S')) (ofHom (algebraMap S S'))
e : R' ⊗[R] S ≃+* S' := (⋯.isoPushout ≪≫ h.isoPushout.symm).commRingCatIsoToRingEquiv
h2 :
  ∀ (r : R'),
    (ConcreteCategory.hom ⋯.isoPushout.hom) (r ⊗ₜ[R] 1) =
      (ConcreteCategory.hom (pushout.inl (ofHom (algebraMap R R')) (ofHom (algebraMap R S)))) r
h3 :
  ∀ (x : R'),
    (Hom.hom h.isoPushout.inv) ((Hom.hom (pushout.inl (ofHom (algebraMap R R')) (ofHom (algebraMap R S)))) x) =
      (algebraMap R' S') x
e' : R' ⊗[R] S ≃ₐ[R'] S' :=
  let __spread.0 := e;
  { toEquiv := __spread.0.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
s : S
h1 :
  (ConcreteCategory.hom ⋯.isoPushout.hom) ((algebraMap S (R' ⊗[R] S)) s) =
    (ConcreteCategory.hom (pushout.inr (ofHom (algebraMap R R')) (ofHom (algebraMap R S)))) s
h4 :
  ∀ (x : S),
    (ConcreteCategory.hom (pushout.inr (ofHom (algebraMap R R')) (ofHom (algebraMap R S)) ≫ h.isoPushout.inv)) x =
      (ConcreteCategory.hom (ofHom (algebraMap S S'))) x
⊢ (e'.toRingEquiv.toRingHom.comp (algebraMap S (R' ⊗[R] S))) s = (algebraMap S S') s
Module: Mathlib.CategoryTheory.Bicategory.Functor.Oplax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤ᵒᵖᴸ C
a b : B
f : a ⟶ b
⊢ F.mapComp f (𝟙 b) ≫ F.map f ◁ F.mapId b = F.map₂ (ρ_ f).hom ≫ (ρ_ (F.map f)).inv

Tactic:
by
  rw [Iso.eq_comp_inv]
  simp only [Category.assoc]
  rw [← F.map₂_rightUnitor]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Lax

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
F✝ : B ⥤ᴸ C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᴸ C
G : C ⥤ᴸ D
a✝ b✝ c✝ : B
f✝ f'✝ : a✝ ⟶ b✝
η : f✝ ⟶ f'✝
g : b✝ ⟶ c✝
⊢ (G.mapComp (F.map f✝) (F.map g) ≫ G.map₂ (F.mapComp f✝ g)) ≫ (F.comp G.toPrelaxFunctor).map₂ (η ▷ g) =
    (F.comp G.toPrelaxFunctor).map₂ η ▷ (F.comp G.toPrelaxFunctor).map g ≫
      G.mapComp (F.map f'✝) (F.map g) ≫ G.map₂ (F.mapComp f'✝ g)

Tactic:
dsimp
    rw [assoc, ← G.map₂_comp, mapComp_naturality_left, G.map₂_comp, mapComp_naturality_left_assoc]

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

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal R
hmap : (map f I).FG
hk : (I ⊓ RingHom.ker f).FG
hf : Function.Surjective ⇑f
algInst✝ : Algebra R S := f.toAlgebra
⊢ I.FG

Tactic:
refine Submodule.fg_of_fg_map_of_fg_inf_ker (Module.compHom.toLinearMap f) ?_ hk

Goal state after:
R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal R
hmap : (map f I).FG
hk : (I ⊓ RingHom.ker f).FG
hf : Function.Surjective ⇑f
algInst✝ : Algebra R S := f.toAlgebra
⊢ (Submodule.map (Module.compHom.toLinearMap f) I).FG
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case refine_2
R : Type w₁
A : Type w₂
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
I : Ideal A
h : I.FG
inst✝ : FinitePresentation R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG
⊢ (RingHom.ker ((Ideal.Quotient.mkₐ R I).comp f).toRingHom).FG

Tactic:
refine Ideal.fg_ker_comp _ _ hf.2 ?_ hf.1

Goal state after:
case refine_2
R : Type w₁
A : Type w₂
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
I : Ideal A
h : I.FG
inst✝ : FinitePresentation R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG
⊢ (RingHom.ker (Ideal.Quotient.mkₐ R I).toRingHom).FG
Module: Mathlib.CategoryTheory.ObjectProperty.Small

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
⊢ EssentiallySmall.{w, v, u} C ↔ ObjectProperty.EssentiallySmall.{w, v, u} ⊤

Tactic:
rw [← exists_equivalence_iff_of_locallySmall]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
⊢ EssentiallySmall.{w, v, u} C ↔ ∃ J x, Nonempty (C ≌ J)
Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝¹ : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
X : C
d : ↑(F.obj X)
| colimit.ι (Grothendieck.ι F X ⋙ G) d

Tactic:
← colimit.eqToHom_comp_ι (Grothendieck.ι F X ⋙ G)
      (j := (F.map (𝟙 X)).toFunctor.obj d) (by simp)

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝¹ : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
X : C
d : ↑(F.obj X)
| eqToHom ⋯ ≫ colimit.ι (Grothendieck.ι F X ⋙ G) ((F.map (𝟙 X)).toFunctor.obj d)