mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monad.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Comonad C
X : C
inst✝ : IsIso T.δ
x✝ : IsSplitEpi (T.ε.app X)
⊢ T.ε.app X ≫ section_ (T.ε.app X) = T.map (section_ (T.ε.app X)) ≫ T.ε.app (T.obj X)

Tactic:
T.counit_naturality

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Comonad C
X : C
inst✝ : IsIso T.δ
x✝ : IsSplitEpi (T.ε.app X)
⊢ T.ε.app X ≫ section_ (T.ε.app X) = T.ε.app X ≫ section_ (T.ε.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)
⊢ lift S g h ∘ₗ mkLinearMap S M = g

Tactic:
ext x

Goal state after:
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 : M
⊢ (lift S g h ∘ₗ mkLinearMap S M) x = g 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)
l : LocalizedModule S M →ₗ[R] M''
hl : l ∘ₗ mkLinearMap S M = g
⊢ lift S g h = l

Tactic:
ext x

Goal state after:
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
x : LocalizedModule S M
⊢ (lift S g h) x = l x
Module: Mathlib.Algebra.Category.Ring.Under.Basic

Goal state before:
pp: R : CommRingCat
A : Type u
inst✝¹ : CommRing A
inst✝ : Algebra (↑R) A
B : Under R
f g : R.mkUnder A ⟶ B
h : ∀ (a : A), (ConcreteCategory.hom (Under.Hom.right f)) a = (ConcreteCategory.hom (Under.Hom.right g)) a
⊢ f = g

Tactic:
ext x

Goal state after:
R : CommRingCat
A : Type u
inst✝¹ : CommRing A
inst✝ : Algebra (↑R) A
B : Under R
f g : R.mkUnder A ⟶ B
h : ∀ (a : A), (ConcreteCategory.hom (Under.Hom.right f)) a = (ConcreteCategory.hom (Under.Hom.right g)) a
x : ↑(R.mkUnder A).right
⊢ (Hom.hom (Under.Hom.right f)) x = (Hom.hom (Under.Hom.right g)) x
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case property.left
R A B : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : PushoutCocone (ofHom (algebraMap R A)) (ofHom (algebraMap R B))
this✝ : Algebra R ↑s.pt := ⋯
f' : A →ₐ[R] ↑s.pt := ⋯
g' : B →ₐ[R] ↑s.pt := ⋯
this : Algebra R ↑(pushoutCocone R A B).pt := ⋯
⊢ ofHom Algebra.TensorProduct.includeLeftRingHom ≫ ofHom (Algebra.TensorProduct.productMap f' g').toRingHom = s.inl

Tactic:
ext x

Goal state after:
case property.left
R A B : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : PushoutCocone (ofHom (algebraMap R A)) (ofHom (algebraMap R B))
this✝ : Algebra R ↑s.pt := ((Hom.hom s.inl).comp (algebraMap R A)).toAlgebra
f' : A →ₐ[R] ↑s.pt :=
  let __src := Hom.hom s.inl;
  { toRingHom := __src, commutes' := ⋯ }
g' : B →ₐ[R] ↑s.pt :=
  let __src := Hom.hom s.inr;
  { toRingHom := __src, commutes' := ⋯ }
this : Algebra R ↑(pushoutCocone R A B).pt :=
  have this := inferInstance;
  this
x : ↑(of A)
⊢ (Hom.hom (ofHom Algebra.TensorProduct.includeLeftRingHom ≫ ofHom (Algebra.TensorProduct.productMap f' g').toRingHom))
      x =
    (Hom.hom s.inl) x
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case property.right.left
R A B : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : PushoutCocone (ofHom (algebraMap R A)) (ofHom (algebraMap R B))
this✝ : Algebra R ↑s.pt := ⋯
f' : A →ₐ[R] ↑s.pt := ⋯
g' : B →ₐ[R] ↑s.pt := ⋯
this : Algebra R ↑(pushoutCocone R A B).pt := ⋯
⊢ ofHom Algebra.TensorProduct.includeRight.toRingHom ≫ ofHom (Algebra.TensorProduct.productMap f' g').toRingHom = s.inr

Tactic:
ext x

Goal state after:
case property.right.left
R A B : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : PushoutCocone (ofHom (algebraMap R A)) (ofHom (algebraMap R B))
this✝ : Algebra R ↑s.pt := ((Hom.hom s.inl).comp (algebraMap R A)).toAlgebra
f' : A →ₐ[R] ↑s.pt :=
  let __src := Hom.hom s.inl;
  { toRingHom := __src, commutes' := ⋯ }
g' : B →ₐ[R] ↑s.pt :=
  let __src := Hom.hom s.inr;
  { toRingHom := __src, commutes' := ⋯ }
this : Algebra R ↑(pushoutCocone R A B).pt :=
  have this := inferInstance;
  this
x : ↑(of B)
⊢ (Hom.hom
        (ofHom Algebra.TensorProduct.includeRight.toRingHom ≫ ofHom (Algebra.TensorProduct.productMap f' g').toRingHom))
      x =
    (Hom.hom s.inr) x
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: R A B : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : PushoutCocone (ofHom (algebraMap R A)) (ofHom (algebraMap R B))
this✝¹ : Algebra R ↑s.pt := ((Hom.hom s.inl).comp (algebraMap R A)).toAlgebra
f' : A →ₐ[R] ↑s.pt :=
  let __src := Hom.hom s.inl;
  { toRingHom := __src, commutes' := ⋯ }
g' : B →ₐ[R] ↑s.pt :=
  let __src := Hom.hom s.inr;
  { toRingHom := __src, commutes' := ⋯ }
this✝ : Algebra R ↑(pushoutCocone R A B).pt :=
  have this := inferInstance;
  this
h : (pushoutCocone R A B).pt ⟶ s.pt
eq1 : ofHom Algebra.TensorProduct.includeLeftRingHom ≫ h = s.inl
eq2 : ofHom Algebra.TensorProduct.includeRight.toRingHom ≫ h = s.inr
h' : A ⊗[R] B →ₐ[R] ↑s.pt :=
  let __src := Hom.hom h;
  { toRingHom := __src, commutes' := ⋯ }
this : h' = Algebra.TensorProduct.productMap f' g'
⊢ h = ofHom (Algebra.TensorProduct.productMap f' g').toRingHom

Tactic:
ext x

Goal state after:
R A B : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : PushoutCocone (ofHom (algebraMap R A)) (ofHom (algebraMap R B))
this✝¹ : Algebra R ↑s.pt := ((Hom.hom s.inl).comp (algebraMap R A)).toAlgebra
f' : A →ₐ[R] ↑s.pt :=
  let __src := Hom.hom s.inl;
  { toRingHom := __src, commutes' := ⋯ }
g' : B →ₐ[R] ↑s.pt :=
  let __src := Hom.hom s.inr;
  { toRingHom := __src, commutes' := ⋯ }
this✝ : Algebra R ↑(pushoutCocone R A B).pt :=
  have this := inferInstance;
  this
h : (pushoutCocone R A B).pt ⟶ s.pt
eq1 : ofHom Algebra.TensorProduct.includeLeftRingHom ≫ h = s.inl
eq2 : ofHom Algebra.TensorProduct.includeRight.toRingHom ≫ h = s.inr
h' : A ⊗[R] B →ₐ[R] ↑s.pt :=
  let __src := Hom.hom h;
  { toRingHom := __src, commutes' := ⋯ }
this : h' = Algebra.TensorProduct.productMap f' g'
x : ↑(pushoutCocone R A B).pt
⊢ (Hom.hom h) x = (Hom.hom (ofHom (Algebra.TensorProduct.productMap f' g').toRingHom)) x
Module: Mathlib.Algebra.Category.Ring.Under.Basic

Goal state before:
pp: case h₀
R S : CommRingCat
inst✝ : Algebra ↑R ↑S
A B : Under R
f : A ⟶ B
⊢ (pushout.inl A.hom (ofHom (algebraMap ↑R ↑S)) ≫
        Under.Hom.right
          ((tensorProdObjIsoPushoutObj S A).inv ≫ (R.tensorProd S).map f ≫ (tensorProdObjIsoPushoutObj S B).hom)) ≫
      Under.Hom.right (tensorProdObjIsoPushoutObj S B).inv =
    (pushout.inl A.hom (ofHom (algebraMap ↑R ↑S)) ≫
        Under.Hom.right
          ((tensorProdObjIsoPushoutObj S A).inv ≫
            (tensorProdObjIsoPushoutObj S A).hom ≫
              Under.homMk
                (pushout.desc (Under.Hom.right f ≫ pushout.inl B.hom (ofHom (algebraMap ↑R ↑S)))
                  (pushout.inr B.hom (ofHom (algebraMap ↑R ↑S))) ⋯)
                ⋯)) ≫
      Under.Hom.right (tensorProdObjIsoPushoutObj S B).inv

Tactic:
ext x

Goal state after:
case h₀
R S : CommRingCat
inst✝ : Algebra ↑R ↑S
A B : Under R
f : A ⟶ B
x : ↑A.right
⊢ (Hom.hom
        ((pushout.inl A.hom (ofHom (algebraMap ↑R ↑S)) ≫
            Under.Hom.right
              ((tensorProdObjIsoPushoutObj S A).inv ≫ (R.tensorProd S).map f ≫ (tensorProdObjIsoPushoutObj S B).hom)) ≫
          Under.Hom.right (tensorProdObjIsoPushoutObj S B).inv))
      x =
    (Hom.hom
        ((pushout.inl A.hom (ofHom (algebraMap ↑R ↑S)) ≫
            Under.Hom.right
              ((tensorProdObjIsoPushoutObj S A).inv ≫
                (tensorProdObjIsoPushoutObj S A).hom ≫
                  Under.homMk
                    (pushout.desc (Under.Hom.right f ≫ pushout.inl B.hom (ofHom (algebraMap ↑R ↑S)))
                      (pushout.inr B.hom (ofHom (algebraMap ↑R ↑S))) ⋯)
                    ⋯)) ≫
          Under.Hom.right (tensorProdObjIsoPushoutObj S B).inv))
      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_3
M'' : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
l : M' →ₗ[R] M''
hl : l ∘ₗ f = g
⊢ l ∘ₗ ↑(iso S f) ∘ₗ LocalizedModule.mkLinearMap S M = l ∘ₗ f

Tactic:
ext x

Goal state after:
R : Type u_1
inst✝⁷ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (End R M'')) ↑x)
l : M' →ₗ[R] M''
hl : l ∘ₗ f = g
x : M
⊢ (l ∘ₗ ↑(iso S f) ∘ₗ LocalizedModule.mkLinearMap S M) x = (l ∘ₗ f) x
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case refine_2
X : CommRingCat
f : of PUnit.{u + 1} ⟶ X
⊢ ofHom { toMonoidHom := 1, map_zero' := ⋯, map_add' := ⋯ } ≫ f = 𝟙 X

Tactic:
ext x

Goal state after:
case refine_2
X : CommRingCat
f : of PUnit.{u + 1} ⟶ X
x : ↑X
⊢ (Hom.hom (ofHom { toMonoidHom := 1, map_zero' := ⋯, map_add' := ⋯ } ≫ f)) x = (Hom.hom (𝟙 X)) x
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: A B : CommRingCat
s : Cone (pair A B)
m : s.pt ⟶ (A.prodFan B).pt
h : ∀ (j : Discrete WalkingPair), m ≫ (A.prodFan B).π.app j = s.π.app j
⊢ m = ofHom ((Hom.hom (s.π.app { as := WalkingPair.left })).prod (Hom.hom (s.π.app { as := WalkingPair.right })))

Tactic:
ext x

Goal state after:
A B : CommRingCat
s : Cone (pair A B)
m : s.pt ⟶ (A.prodFan B).pt
h : ∀ (j : Discrete WalkingPair), m ≫ (A.prodFan B).π.app j = s.π.app j
x : ↑s.pt
⊢ (Hom.hom m) x =
    (Hom.hom
        (ofHom ((Hom.hom (s.π.app { as := WalkingPair.left })).prod (Hom.hom (s.π.app { as := WalkingPair.right })))))
      x
Module: Mathlib.CategoryTheory.Limits.Comma

Goal state before:
pp: case h₂
J : Type w
inst✝⁴ : Category.{w', w} J
A : Type u₁
inst✝³ : Category.{v₁, u₁} A
B : Type u₂
inst✝² : Category.{v₂, u₂} B
T : Type u₃
inst✝¹ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
F✝ F : J ⥤ Comma L R
c : Cocone F
inst✝ : PreservesColimit (F ⋙ fst L R) L
h₁ : IsColimit ((fst L R).mapCocone c)
h₂ : IsColimit ((snd L R).mapCocone c)
s : Cocone F
x✝ : c.pt ⟶ s.pt
hm : ∀ (j : J), c.ι.app j ≫ x✝ = s.ι.app j
⊢ x✝.right = { left := h₁.desc ((fst L R).mapCocone s), right := h₂.desc ((snd L R).mapCocone s), w := ⋯ }.right

Tactic:
exact h₂.uniq ((snd _ _).mapCocone s) _ (by simp [← hm])

Goal state after:
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
⊢ (map S f f) LinearMap.id = LinearMap.id

Tactic:
ext x

Goal state after:
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 : M'
⊢ ((map S f f) LinearMap.id) x = LinearMap.id x
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Submonoid R
M₀ : Type u_6
M₀' : Type u_9
inst✝⁹ : AddCommMonoid M₀
inst✝⁸ : AddCommMonoid M₀'
inst✝⁷ : Module R M₀
inst✝⁶ : Module R M₀'
f₀ : M₀ →ₗ[R] M₀'
inst✝⁵ : IsLocalizedModule S f₀
M₁ : Type u_7
M₁' : Type u_8
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₁'
inst✝² : Module R M₁
inst✝¹ : Module R M₁'
f₁ : M₁ →ₗ[R] M₁'
inst✝ : IsLocalizedModule S f₁
g : M₀ →ₗ[R] M₁
⊢ (map S f₀ f₁) g ∘ₗ ↑(iso S f₀) = ↑(iso S f₁) ∘ₗ (map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g

Tactic:
ext x

Goal state after:
R : Type u_1
inst✝¹⁰ : CommSemiring R
S : Submonoid R
M₀ : Type u_6
M₀' : Type u_9
inst✝⁹ : AddCommMonoid M₀
inst✝⁸ : AddCommMonoid M₀'
inst✝⁷ : Module R M₀
inst✝⁶ : Module R M₀'
f₀ : M₀ →ₗ[R] M₀'
inst✝⁵ : IsLocalizedModule S f₀
M₁ : Type u_7
M₁' : Type u_8
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₁'
inst✝² : Module R M₁
inst✝¹ : Module R M₁'
f₁ : M₁ →ₗ[R] M₁'
inst✝ : IsLocalizedModule S f₁
g : M₀ →ₗ[R] M₁
x : LocalizedModule S M₀
⊢ ((map S f₀ f₁) g ∘ₗ ↑(iso S f₀)) x = (↑(iso S f₁) ∘ₗ (map S (mkLinearMap S M₀) (mkLinearMap S M₁)) g) x
Module: Mathlib.CategoryTheory.Bicategory.Functor.Prelax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : PrelaxFunctor B C
x y : B
f g : x ⟶ y
hfg : f = g
⊢ F.map₂ (eqToHom hfg) = eqToHom ⋯

Tactic:
subst hfg

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : PrelaxFunctor B C
x y : B
f : x ⟶ y
⊢ F.map₂ (eqToHom ⋯) = eqToHom ⋯
Module: Mathlib.CategoryTheory.Bicategory.Functor.Prelax

Goal state before:
pp: B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : PrelaxFunctor B C
x y : B
f g : x ⟶ y
hfg : f = g
⊢ F.map₂Iso (eqToIso hfg) = eqToIso ⋯

Tactic:
subst hfg

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : PrelaxFunctor B C
x y : B
f : x ⟶ y
⊢ F.map₂Iso (eqToIso ⋯) = eqToIso ⋯
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case property.right
A B : CommRingCat
f g : A ⟶ B
s : Fork f g
m : s.pt ⟶ (equalizerFork f g).pt
hm : m ≫ (equalizerFork f g).ι = s.ι
⊢ m = ofHom ((Hom.hom s.ι).codRestrict ((Hom.hom f).eqLocus (Hom.hom g)) ⋯)

Tactic:
ext x

Goal state after:
case property.right
A B : CommRingCat
f g : A ⟶ B
s : Fork f g
m : s.pt ⟶ (equalizerFork f g).pt
hm : m ≫ (equalizerFork f g).ι = s.ι
x : ↑s.pt
⊢ (Hom.hom m) x = (Hom.hom (ofHom ((Hom.hom s.ι).codRestrict ((Hom.hom f).eqLocus (Hom.hom g)) ⋯))) x
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝¹⁵ : CommSemiring R
S : Submonoid R
M₀ : Type u_6
M₀' : Type u_9
inst✝¹⁴ : AddCommMonoid M₀
inst✝¹³ : AddCommMonoid M₀'
inst✝¹² : Module R M₀
inst✝¹¹ : Module R M₀'
f₀ : M₀ →ₗ[R] M₀'
inst✝¹⁰ : IsLocalizedModule S f₀
M₁ : Type u_7
M₁' : Type u_11
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : AddCommMonoid M₁'
inst✝⁷ : Module R M₁
inst✝⁶ : Module R M₁'
f₁ : M₁ →ₗ[R] M₁'
inst✝⁵ : IsLocalizedModule S f₁
M₂ : Type u_8
M₂' : Type u_10
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₂'
inst✝² : Module R M₂
inst✝¹ : Module R M₂'
f₂ : M₂ →ₗ[R] M₂'
inst✝ : IsLocalizedModule S f₂
g : M₀ →ₗ[R] M₁
h : M₁ →ₗ[R] M₂
⊢ (map S f₀ f₂) (h ∘ₗ g) = (map S f₁ f₂) h ∘ₗ (map S f₀ f₁) g

Tactic:
ext x

Goal state after:
R : Type u_1
inst✝¹⁵ : CommSemiring R
S : Submonoid R
M₀ : Type u_6
M₀' : Type u_9
inst✝¹⁴ : AddCommMonoid M₀
inst✝¹³ : AddCommMonoid M₀'
inst✝¹² : Module R M₀
inst✝¹¹ : Module R M₀'
f₀ : M₀ →ₗ[R] M₀'
inst✝¹⁰ : IsLocalizedModule S f₀
M₁ : Type u_7
M₁' : Type u_11
inst✝⁹ : AddCommMonoid M₁
inst✝⁸ : AddCommMonoid M₁'
inst✝⁷ : Module R M₁
inst✝⁶ : Module R M₁'
f₁ : M₁ →ₗ[R] M₁'
inst✝⁵ : IsLocalizedModule S f₁
M₂ : Type u_8
M₂' : Type u_10
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₂'
inst✝² : Module R M₂
inst✝¹ : Module R M₂'
f₂ : M₂ →ₗ[R] M₂'
inst✝ : IsLocalizedModule S f₂
g : M₀ →ₗ[R] M₁
h : M₁ →ₗ[R] M₂
x : M₀'
⊢ ((map S f₀ f₂) (h ∘ₗ g)) x = ((map S f₁ f₂) h ∘ₗ (map S f₀ f₁) g) x
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_6
S : Type u_7
S' : Type u_8
inst✝⁴ : CommSemiring R
inst✝³ : Ring S
inst✝² : Ring S'
inst✝¹ : Algebra R S
inst✝ : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit ((algebraMap R S') x)
h₂ : ∀ (y : S'), ∃ x, x.2 • y = f x.1
h₃ : ∀ (x : S), f x = 0 → ∃ m, m • x = 0
⊢ IsLocalizedModule M f.toLinearMap

Tactic:
replace h₃ := fun x =>
    Iff.intro (h₃ x) fun ⟨⟨m, hm⟩, e⟩ =>
      (h₁ m hm).mul_left_cancel <| by
        rw [← Algebra.smul_def]
        simpa [Submonoid.smul_def] using f.congr_arg e

Goal state after:
R : Type u_6
S : Type u_7
S' : Type u_8
inst✝⁴ : CommSemiring R
inst✝³ : Ring S
inst✝² : Ring S'
inst✝¹ : Algebra R S
inst✝ : Algebra R S'
M : Submonoid R
f : S →ₐ[R] S'
h₁ : ∀ x ∈ M, IsUnit ((algebraMap R S') x)
h₂ : ∀ (y : S'), ∃ x, x.2 • y = f x.1
h₃ : ∀ (x : S), f x = 0 ↔ ∃ m, m • x = 0
⊢ IsLocalizedModule M f.toLinearMap
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case fac_left
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
s : PullbackCone f g
⊢ ofHom
        (((Hom.hom s.fst).prod (Hom.hom s.snd)).codRestrict
          (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))) ⋯) ≫
      ofHom
        ((RingHom.fst ↑A ↑B).comp
          (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype) =
    s.fst

Tactic:
ext x

Goal state after:
case fac_left
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
s : PullbackCone f g
x : ↑s.pt
⊢ (Hom.hom
        (ofHom
            (((Hom.hom s.fst).prod (Hom.hom s.snd)).codRestrict
              (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))) ⋯) ≫
          ofHom
            ((RingHom.fst ↑A ↑B).comp
              (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype)))
      x =
    (Hom.hom s.fst) x
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: case fac_right
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
s : PullbackCone f g
⊢ ofHom
        (((Hom.hom s.fst).prod (Hom.hom s.snd)).codRestrict
          (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))) ⋯) ≫
      ofHom
        ((RingHom.snd ↑A ↑B).comp
          (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype) =
    s.snd

Tactic:
ext x

Goal state after:
case fac_right
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
s : PullbackCone f g
x : ↑s.pt
⊢ (Hom.hom
        (ofHom
            (((Hom.hom s.fst).prod (Hom.hom s.snd)).codRestrict
              (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))) ⋯) ≫
          ofHom
            ((RingHom.snd ↑A ↑B).comp
              (((Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus ((Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype)))
      x =
    (Hom.hom s.snd) x
Module: Mathlib.CategoryTheory.Bicategory.Functor.Oplax

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᵒᵖᴸ C
b₀ b₁ b₂ : B
f : b₀ ⟶ b₁
g : b₁ ⟶ b₂
fg : b₀ ⟶ b₂
h : f ≫ g = fg
⊢ fg = f ≫ g

Tactic:
by rw [h]

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
a b c d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
⊢ F.mapComp f g ▷ F.map h ≫ F.mapComp (f ≫ g) h =
    F.mapComp f g ▷ F.map h ≫ F.mapComp (f ≫ g) h ≫ F.map₂ (α_ f g h).hom ≫ F.map₂ (α_ f g h).inv

Tactic:
← F.map₂_comp

Goal state after:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : B ⥤ᴸ C
a b c d : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
⊢ F.mapComp f g ▷ F.map h ≫ F.mapComp (f ≫ g) h =
    F.mapComp f g ▷ F.map h ≫ F.mapComp (f ≫ g) h ≫ F.map₂ ((α_ f g h).hom ≫ (α_ f g h).inv)
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
b₀ b₁ b₂ : B
f : b₀ ⟶ b₁
g : b₁ ⟶ b₂
fg : b₀ ⟶ b₂
h : f ≫ g = fg
⊢ f ≫ g = fg

Tactic:
by rw [h]

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

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ F : B ⥤ᵖ C
a b b₀ b₁ b₂ : B
f : b₀ ⟶ b₁
g : b₁ ⟶ b₂
fg : b₀ ⟶ b₂
h : f ≫ g = fg
⊢ fg = f ≫ g

Tactic:
by rw [h]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Products

Goal state before:
pp: X Y : Type u
x✝¹ : Cone (pair X Y)
x✝ : x✝¹.pt ⟶ (binaryProductCone X Y).pt
w : ∀ (j : Discrete WalkingPair), x✝ ≫ (binaryProductCone X Y).π.app j = x✝¹.π.app j
⊢ x✝ = ↾fun x ↦ ((ConcreteCategory.hom (BinaryFan.fst x✝¹)) x, (ConcreteCategory.hom (BinaryFan.snd x✝¹)) x)

Tactic:
ext x

Goal state after:
X Y : Type u
x✝¹ : Cone (pair X Y)
x✝ : x✝¹.pt ⟶ (binaryProductCone X Y).pt
w : ∀ (j : Discrete WalkingPair), x✝ ≫ (binaryProductCone X Y).π.app j = x✝¹.π.app j
x : x✝¹.pt
⊢ (ConcreteCategory.hom x✝).toFun x =
    (ConcreteCategory.hom
          (↾fun x ↦ ((ConcreteCategory.hom (BinaryFan.fst x✝¹)) x, (ConcreteCategory.hom (BinaryFan.snd x✝¹)) x))).toFun
      x
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: R : Type w₁
A : Type w₂
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FinitePresentation R A
ι : Type v
inst✝ : Finite ι
⊢ FinitePresentation R (MvPolynomial ι A)

Tactic:
have hfp : FinitePresentation R A := inferInstance

Goal state after:
R : Type w₁
A : Type w₂
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FinitePresentation R A
ι : Type v
inst✝ : Finite ι
hfp : FinitePresentation R A
⊢ FinitePresentation R (MvPolynomial ι A)
Module: Mathlib.CategoryTheory.MorphismProperty.Comma

Goal state before:
pp: A : Type u_1
inst✝⁴ : Category.{v_1, u_1} A
B : Type u_2
inst✝³ : Category.{v_2, u_2} B
T : Type u_3
inst✝² : Category.{v_3, u_3} T
L : A ⥤ T
R : B ⥤ T
P : MorphismProperty T
Q : MorphismProperty A
W : MorphismProperty B
inst✝¹ : Q.IsMultiplicative
inst✝ : W.IsMultiplicative
X Y : MorphismProperty.Comma L R P Q W
h : X = Y
⊢ X.left = Y.left

Tactic:
by rw [h]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Comma

Goal state before:
pp: A : Type u_1
inst✝⁴ : Category.{v_1, u_1} A
B : Type u_2
inst✝³ : Category.{v_2, u_2} B
T : Type u_3
inst✝² : Category.{v_3, u_3} T
L : A ⥤ T
R : B ⥤ T
P : MorphismProperty T
Q : MorphismProperty A
W : MorphismProperty B
inst✝¹ : Q.IsMultiplicative
inst✝ : W.IsMultiplicative
X Y : MorphismProperty.Comma L R P Q W
h : X = Y
⊢ X.right = Y.right

Tactic:
by rw [h]

Goal state after: