mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: 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
T' : Type u_2
inst✝⁴ : CommSemiring T'
inst✝³ : Algebra R T'
inst✝² : IsLocalization S✝ T'
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Submonoid R
m₁ m₂ : LocalizedModule S A
⊢ ∀ (p q p' q' : A × ↥S), p ≈ p' → q ≈ q' → mk (p.1 * q.1) (q.2 * p.2) = mk (p'.1 * q'.1) (q'.2 * p'.2)

Tactic:
rintro ⟨a₁, s₁⟩ ⟨a₂, s₂⟩ ⟨b₁, t₁⟩ ⟨b₂, t₂⟩ ⟨u₁, e₁⟩ ⟨u₂, e₂⟩

Goal state after:
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
T' : Type u_2
inst✝⁴ : CommSemiring T'
inst✝³ : Algebra R T'
inst✝² : IsLocalization S✝ T'
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Submonoid R
m₁ m₂ : LocalizedModule S A
a₁ : A
s₁ : ↥S
a₂ : A
s₂ : ↥S
b₁ : A
t₁ : ↥S
b₂ : A
t₂ u₁ : ↥S
e₁ : u₁ • (b₁, t₁).2 • (a₁, s₁).1 = u₁ • (a₁, s₁).2 • (b₁, t₁).1
u₂ : ↥S
e₂ : u₂ • (b₂, t₂).2 • (a₂, s₂).1 = u₂ • (a₂, s₂).2 • (b₂, t₂).1
⊢ mk ((a₁, s₁).1 * (a₂, s₂).1) ((a₂, s₂).2 * (a₁, s₁).2) = mk ((b₁, t₁).1 * (b₂, t₂).1) ((b₂, t₂).2 * (b₁, t₁).2)
Module: Mathlib.RingTheory.Localization.BaseChange

Goal state before:
pp: R : Type u_7
S : Type u_8
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Algebra R S
A : Type u_9
inst✝⁸ : CommSemiring A
inst✝⁷ : Algebra R A
M : Submonoid A
B : Type u_10
inst✝⁶ : CommSemiring B
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : IsScalarTower R A B
inst✝² : IsLocalization M B
inst✝¹ : Algebra (S ⊗[R] A) (S ⊗[R] B)
inst✝ : IsScalarTower S (S ⊗[R] A) (S ⊗[R] B)
H :
  (algebraMap (S ⊗[R] A) (S ⊗[R] B)).comp Algebra.TensorProduct.includeRight.toRingHom =
    Algebra.TensorProduct.includeRight.comp (algebraMap A B)
this✝ : Algebra A (S ⊗[R] B) := Algebra.compHom (S ⊗[R] B) (algebraMap A B)
this : IsScalarTower A (S ⊗[R] A) (S ⊗[R] B)
⊢ IsLocalization (Algebra.algebraMapSubmonoid (S ⊗[R] A) M) (S ⊗[R] B)

Tactic:
have : IsScalarTower R A (S ⊗[R] B) :=
    .of_algebraMap_eq' <| by
      rw [Algebra.compHom_algebraMap_eq, RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq,
        IsScalarTower.algebraMap_eq R B]

Goal state after:
R : Type u_7
S : Type u_8
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : CommSemiring S
inst✝⁹ : Algebra R S
A : Type u_9
inst✝⁸ : CommSemiring A
inst✝⁷ : Algebra R A
M : Submonoid A
B : Type u_10
inst✝⁶ : CommSemiring B
inst✝⁵ : Algebra R B
inst✝⁴ : Algebra A B
inst✝³ : IsScalarTower R A B
inst✝² : IsLocalization M B
inst✝¹ : Algebra (S ⊗[R] A) (S ⊗[R] B)
inst✝ : IsScalarTower S (S ⊗[R] A) (S ⊗[R] B)
H :
  (algebraMap (S ⊗[R] A) (S ⊗[R] B)).comp Algebra.TensorProduct.includeRight.toRingHom =
    Algebra.TensorProduct.includeRight.comp (algebraMap A B)
this✝¹ : Algebra A (S ⊗[R] B) := Algebra.compHom (S ⊗[R] B) (algebraMap A B)
this✝ : IsScalarTower A (S ⊗[R] A) (S ⊗[R] B)
this : IsScalarTower R A (S ⊗[R] B)
⊢ IsLocalization (Algebra.algebraMapSubmonoid (S ⊗[R] A) M) (S ⊗[R] B)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
f' : W ⟶ X
inst✝¹ : HasPullback f g
inst✝ : HasPullback f' (pullback.fst f g)
⊢ (pullbackRightPullbackFstIso f g f').inv ≫ pullback.snd f' (pullback.fst f g) ≫ pullback.fst f g =
    pullback.fst (f' ≫ f) g ≫ f'

Tactic:
← pullback.condition

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
f' : W ⟶ X
inst✝¹ : HasPullback f g
inst✝ : HasPullback f' (pullback.fst f g)
⊢ (pullbackRightPullbackFstIso f g f').inv ≫ pullback.fst f' (pullback.fst f g) ≫ f' = pullback.fst (f' ≫ f) g ≫ f'
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: case mk.mk.mk
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
T' : Type u_2
inst✝⁴ : CommSemiring T'
inst✝³ : Algebra R T'
inst✝² : IsLocalization S✝ T'
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Submonoid R
a✝ : LocalizedModule S A
a₁ : A
s₁ : ↥S
b✝ : LocalizedModule S A
a₂ : A
s₂ : ↥S
c✝ : LocalizedModule S A
a₃ : A
s₃ : ↥S
⊢ mk (a₁ * (s₃ • a₂ + s₂ • a₃)) (s₁ * (s₂ * s₃)) = mk (a₁ * a₂) (s₁ * s₂) + mk (a₁ * a₃) (s₁ * s₃)

Tactic:
mk_add_mk

Goal state after:
case mk.mk.mk
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
T' : Type u_2
inst✝⁴ : CommSemiring T'
inst✝³ : Algebra R T'
inst✝² : IsLocalization S✝ T'
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Submonoid R
a✝ : LocalizedModule S A
a₁ : A
s₁ : ↥S
b✝ : LocalizedModule S A
a₂ : A
s₂ : ↥S
c✝ : LocalizedModule S A
a₃ : A
s₃ : ↥S
⊢ mk (a₁ * (s₃ • a₂ + s₂ • a₃)) (s₁ * (s₂ * s₃)) =
    mk ((s₁ * s₃) • (a₁ * a₂) + (s₁ * s₂) • (a₁ * a₃)) (s₁ * s₂ * (s₁ * s₃))
Module: Mathlib.RingTheory.Localization.BaseChange

Goal state before:
pp: R✝ : Type u_1
inst✝³² : CommSemiring R✝
S✝ : Submonoid R✝
A✝ : Type u_2
inst✝³¹ : CommSemiring A✝
inst✝³⁰ : Algebra R✝ A✝
inst✝²⁹ : IsLocalization S✝ A✝
M✝ : Type u_3
inst✝²⁸ : AddCommMonoid M✝
inst✝²⁷ : Module R✝ M✝
M'✝ : Type u_4
inst✝²⁶ : AddCommMonoid M'✝
inst✝²⁵ : Module R✝ M'✝
inst✝²⁴ : Module A✝ M'✝
inst✝²³ : IsScalarTower R✝ A✝ M'✝
f : M✝ →ₗ[R✝] M'✝
T : Type u_5
B✝ : Type u_6
inst✝²² : CommSemiring T
inst✝²¹ : CommSemiring B✝
inst✝²⁰ : Algebra R✝ T
inst✝¹⁹ : Algebra T B✝
inst✝¹⁸ : Algebra R✝ B✝
inst✝¹⁷ : Algebra A✝ B✝
inst✝¹⁶ : IsScalarTower R✝ T B✝
inst✝¹⁵ : IsScalarTower R✝ A✝ B✝
R : Type u_7
S : Type u_8
inst✝¹⁴ : CommSemiring R
inst✝¹³ : CommSemiring S
inst✝¹² : Algebra R S
r : R
A : Type u_9
inst✝¹¹ : CommSemiring A
inst✝¹⁰ : Algebra R A
M : Submonoid A
B : Type u_10
inst✝⁹ : CommSemiring B
inst✝⁸ : Algebra R B
inst✝⁷ : Algebra A B
inst✝⁶ : IsScalarTower R A B
inst✝⁵ : IsLocalization M B
C : Type u_11
inst✝⁴ : CommSemiring C
inst✝³ : Algebra S C
inst✝² : Algebra (S ⊗[R] A) C
inst✝¹ : IsScalarTower S (S ⊗[R] A) C
inst✝ : IsLocalization (Submonoid.map Algebra.TensorProduct.includeRight M) C
M' : Submonoid (S ⊗[R] A) := Submonoid.map Algebra.TensorProduct.includeRight M
this : Algebra (S ⊗[R] A) (S ⊗[R] B) :=
  (Algebra.TensorProduct.map (AlgHom.id R S) (IsScalarTower.toAlgHom R A B)).toAlgebra
⊢ ∀ (x : S), (algebraMap S (S ⊗[R] B)) x = (algebraMap (S ⊗[R] A) (S ⊗[R] B)) ((algebraMap S (S ⊗[R] A)) x)

Tactic:
by intro; simp [RingHom.algebraMap_toAlgebra]

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

Goal state before:
pp: case mk.mk.mk
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
T' : Type u_2
inst✝⁴ : CommSemiring T'
inst✝³ : Algebra R T'
inst✝² : IsLocalization S✝ T'
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Submonoid R
a✝ : LocalizedModule S A
a₁ : A
s₁ : ↥S
b✝ : LocalizedModule S A
a₂ : A
s₂ : ↥S
c✝ : LocalizedModule S A
a₃ : A
s₃ : ↥S
⊢ mk ((s₂ • a₁ + s₁ • a₂) * a₃) (s₁ * s₂ * s₃) = mk (a₁ * a₃) (s₁ * s₃) + mk (a₂ * a₃) (s₂ * s₃)

Tactic:
mk_add_mk

Goal state after:
case mk.mk.mk
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
T' : Type u_2
inst✝⁴ : CommSemiring T'
inst✝³ : Algebra R T'
inst✝² : IsLocalization S✝ T'
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Submonoid R
a✝ : LocalizedModule S A
a₁ : A
s₁ : ↥S
b✝ : LocalizedModule S A
a₂ : A
s₂ : ↥S
c✝ : LocalizedModule S A
a₃ : A
s₃ : ↥S
⊢ mk ((s₂ • a₁ + s₁ • a₂) * a₃) (s₁ * s₂ * s₃) =
    mk ((s₂ * s₃) • (a₁ * a₃) + (s₁ * s₃) • (a₂ * a₃)) (s₁ * s₃ * (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
⊢ x • mk (t • m + s • n) (s * t) =
    mk ((IsLocalization.sec S x).1 • m) ((IsLocalization.sec S x).2 * s) +
      mk ((IsLocalization.sec S x).1 • n) ((IsLocalization.sec S x).2 * t)

Tactic:
mk_add_mk

Goal state after:
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
⊢ x • mk (t • m + s • n) (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))
Module: Mathlib.CategoryTheory.Monad.Basic

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

pp: case a.a.a.a.a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Comonad C
i : T.toFunctor ≅ F
X : C
| F.map (T.δ.app X)

pp: case a.a.a.a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Comonad C
i : T.toFunctor ≅ F
X : C
| F.map (i.hom.app (T.obj X))

pp: case a.a.a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Comonad C
i : T.toFunctor ≅ F
X : C
| F.map (F.map (i.hom.app X))

pp: case a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Comonad C
i : T.toFunctor ≅ F
X : C
| T.δ.app X

pp: case a.a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Comonad C
i : T.toFunctor ≅ F
X : C
| i.hom.app (T.obj X)

Tactic:
← F.map_comp

Goal state after:
case a.a.a.a.a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Comonad C
i : T.toFunctor ≅ F
X : C
| F.map (i.hom.app X ≫ i.inv.app X)

case a.a.a.a.a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Comonad C
i : T.toFunctor ≅ F
X : C
| F.map (T.δ.app X)

case a.a.a.a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Comonad C
i : T.toFunctor ≅ F
X : C
| F.map (i.hom.app (T.obj X))

case a.a.a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Comonad C
i : T.toFunctor ≅ F
X : C
| F.map (F.map (i.hom.app X))

case a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Comonad C
i : T.toFunctor ≅ F
X : C
| T.δ.app X

case a.a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Comonad C
i : T.toFunctor ≅ F
X : C
| i.hom.app (T.obj X)
Module: Mathlib.CategoryTheory.Monad.Basic

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

pp: case a.a.a.a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Comonad C
i : T.toFunctor ≅ F
X : C
| F.map (T.ε.app X)

pp: case a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Comonad C
i : T.toFunctor ≅ F
X : C
| i.inv.app X

pp: case a.a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Comonad C
i : T.toFunctor ≅ F
X : C
| T.δ.app X

pp: case a.a.a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Comonad C
i : T.toFunctor ≅ F
X : C
| i.hom.app (T.obj X)

Tactic:
← F.map_comp

Goal state after:
case a.a.a.a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Comonad C
i : T.toFunctor ≅ F
X : C
| F.map (i.hom.app X ≫ i.inv.app X)

case a.a.a.a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Comonad C
i : T.toFunctor ≅ F
X : C
| F.map (T.ε.app X)

case a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Comonad C
i : T.toFunctor ≅ F
X : C
| i.inv.app X

case a.a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Comonad C
i : T.toFunctor ≅ F
X : C
| T.δ.app X

case a.a.a
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T✝ : Monad C
G : Comonad C
F : C ⥤ C
T : Comonad C
i : T.toFunctor ≅ F
X : C
| i.hom.app (T.obj X)
Module: Mathlib.CategoryTheory.Monad.Algebra

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Monad C
X : C
Y : T.Algebra
f : X ⟶ T.forget.obj Y
⊢ T.map (T.map f ≫ Y.a) ≫ Y.a = (T.free.obj X).a ≫ T.map f ≫ Y.a

Tactic:
simp [← Y.assoc, ← T.μ.naturality_assoc]

Goal state after:
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
r : ↑(of R)
⊢ (algebraMap R (A ⊗[R] B)) r =
    (Hom.hom (ofHom (algebraMap R B) ≫ ofHom Algebra.TensorProduct.includeRight.toRingHom)) r

Tactic:
· exact (Algebra.TensorProduct.includeRight.commutes (R := R) r).symm

Goal state after:
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 : Cone F
inst✝ : PreservesLimit (F ⋙ snd L R) R
h₁ : IsLimit ((fst L R).mapCone c)
h₂ : IsLimit ((snd L R).mapCone c)
s : Cone F
j : J
⊢ ({ left := h₁.lift ((fst L R).mapCone s), right := h₂.lift ((snd L R).mapCone s), w := ⋯ } ≫ c.π.app j).right =
    (s.π.app j).right

Tactic:
exact h₂.fac ((snd _ _).mapCone s) j

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
N : Type u_6
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
g : M' →ₗ[R] N
H : ∀ {x y : M}, g (f x) = g (f y) → f x = f y
⊢ Function.Injective ⇑g

Tactic:
intro a b hab

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
N : Type u_6
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
g : M' →ₗ[R] N
H : ∀ {x y : M}, g (f x) = g (f y) → f x = f y
a b : M'
hab : g a = g b
⊢ a = b
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
N : Type u_6
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
g : M' →ₗ[R] N
H : ∀ {x y : M}, g (f x) = g (f y) → f x = f y
a b : M'
hab : g a = g b
x : M
m : ↥S
hxm : m • a = f x
y : M
n : ↥S
hym : n • b = f y
⊢ a = b

Tactic:
suffices h : g (f (n.val • x)) = g (f (m.val • y)) by
    apply H at h
    rw [map_smul, map_smul] at h
    rwa [← IsLocalizedModule.smul_inj f (n * m), mul_smul, mul_comm, mul_smul, hxm, hym]

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
N : Type u_6
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
g : M' →ₗ[R] N
H : ∀ {x y : M}, g (f x) = g (f y) → f x = f y
a b : M'
hab : g a = g b
x : M
m : ↥S
hxm : m • a = f x
y : M
n : ↥S
hym : n • b = f y
⊢ g (f (↑n • x)) = g (f (↑m • y))
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: A B : CommRingCat
f g : A ⟶ B
⊢ IsLimit (equalizerFork f g)

Tactic:
fapply Fork.IsLimit.mk'

Goal state after:
A B : CommRingCat
f g : A ⟶ B
⊢ (s : Fork f g) →
    { l //
      l ≫ (equalizerFork f g).ι = s.ι ∧ ∀ {m : s.pt ⟶ (equalizerFork f g).pt}, m ≫ (equalizerFork f g).ι = s.ι → m = l }
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
inst✝ : IsPreconnected J
p : Set J
j₀ : J
h0 : j₀ ∈ p
h1 : ∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
j : J
aux : ∀ (j₁ j₂ : J) (f : j₁ ⟶ j₂), { down := j₁ ∈ p } = { down := j₂ ∈ p } :=
  fun j₁ j₂ f ↦ congrArg ULift.up (Iff.eq (h1 f))
i : (j ∈ p) = (j₀ ∈ p)
⊢ j ∈ p

Tactic:
i

Goal state after:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
inst✝ : IsPreconnected J
p : Set J
j₀ : J
h0 : j₀ ∈ p
h1 : ∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
j : J
aux : ∀ (j₁ j₂ : J) (f : j₁ ⟶ j₂), { down := j₁ ∈ p } = { down := j₂ ∈ p } :=
  fun j₁ j₂ f ↦ congrArg ULift.up (Iff.eq (h1 f))
i : (j ∈ p) = (j₀ ∈ p)
⊢ j₀ ∈ p
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝ : Category.{v₁, u₁} J
h : ∀ (j₁ j₂ : J), Zigzag j₁ j₂
⊢ IsPreconnected J

Tactic:
apply IsPreconnected.of_constant_of_preserves_morphisms

Goal state after:
J : Type u₁
inst✝ : Category.{v₁, u₁} J
h : ∀ (j₁ j₂ : J), Zigzag j₁ j₂
⊢ ∀ {α : Type u₁} (F : J → α), (∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), F j₁ = F j₂) → ∀ (j j' : J), F j = F j'
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
G : Type u
inst✝ : Groupoid G
F : G ⥤ Type w
p q : F.Elements
f : p ⟶ q
⊢ (ConcreteCategory.hom (F.map ↑f ≫ F.map (Groupoid.inv ↑f))) p.snd = p.snd

Tactic:
← F.map_comp

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
G : Type u
inst✝ : Groupoid G
F : G ⥤ Type w
p q : F.Elements
f : p ⟶ q
⊢ (ConcreteCategory.hom (F.map (↑f ≫ Groupoid.inv ↑f))) p.snd = p.snd
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
F : C ⥤ Cat
G : C ⥤ Type w
E : Type u_1
inst✝ : Category.{v_1, u_1} E
X Y : C
f : X ⟶ Y
x✝² x✝¹ : ↑(F.obj X)
x✝ : x✝² ⟶ x✝¹
⊢ eqToHom ⋯ ≫
      ({ base := 𝟙 X, fiber := eqToHom ⋯ ≫ x✝ } ≫ { base := f, fiber := 𝟙 ((F.map f).toFunctor.obj x✝¹) }).fiber =
    ({ base := f, fiber := 𝟙 ((F.map f).toFunctor.obj x✝²) } ≫
        { base := 𝟙 Y, fiber := eqToHom ⋯ ≫ (F.map f).toFunctor.map x✝ }).fiber

Tactic:
by simp [eqToHom_map]

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : WithTerminal C ⥤ D
x y : C
f : x ⟶ y
⊢ F.map (incl.map f) ≫ F.map (starTerminal.from (of y)) = F.map (starTerminal.from (of x))

Tactic:
← F.map_comp

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : WithTerminal C ⥤ D
x y : C
f : x ⟶ y
⊢ F.map (incl.map f ≫ starTerminal.from (of y)) = F.map (starTerminal.from (of x))
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
I : (d : D) → colimit (F ⋙ coyoneda.obj (op d)) ≅ PUnit.{v + 1}
d : D
this : Nonempty (StructuredArrow d F)
X₁ : C
f₁ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₁
X₂ : C
f₂ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₂
y₁ : (fun X ↦ X) (colimit (F ⋙ coyoneda.obj (op d))) :=
  (ConcreteCategory.hom (colimit.ι (F ⋙ coyoneda.obj (op d)) X₁)) f₁
y₂ : (fun X ↦ X) (colimit (F ⋙ coyoneda.obj (op d))) :=
  (ConcreteCategory.hom (colimit.ι (F ⋙ coyoneda.obj (op d)) X₂)) f₂
⊢ Zigzag { left := { as := PUnit.unit }, right := X₁, hom := f₁ }
    { left := { as := PUnit.unit }, right := X₂, hom := f₂ }

Tactic:
have e : y₁ = y₂ := by
      apply (I d).toEquiv.injective
      ext

Goal state after:
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
I : (d : D) → colimit (F ⋙ coyoneda.obj (op d)) ≅ PUnit.{v + 1}
d : D
this : Nonempty (StructuredArrow d F)
X₁ : C
f₁ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₁
X₂ : C
f₂ : (fromPUnit d).obj { as := PUnit.unit } ⟶ F.obj X₂
y₁ : (fun X ↦ X) (colimit (F ⋙ coyoneda.obj (op d))) :=
  (ConcreteCategory.hom (colimit.ι (F ⋙ coyoneda.obj (op d)) X₁)) f₁
y₂ : (fun X ↦ X) (colimit (F ⋙ coyoneda.obj (op d))) :=
  (ConcreteCategory.hom (colimit.ι (F ⋙ coyoneda.obj (op d)) X₂)) f₂
e : y₁ = y₂
⊢ Zigzag { left := { as := PUnit.unit }, right := X₁, hom := f₁ }
    { left := { as := PUnit.unit }, right := X₂, hom := f₂ }
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y : C
f g : X ⟶ Y
⊢ ∀ {X_1 Y_1 : WalkingParallelPair} (f_1 : X_1 ⟶ Y_1),
    (parallelPair f.op g.op).map f_1 ≫
        (match Y_1 with
          | WalkingParallelPair.zero => Iso.refl ((parallelPair f.op g.op).obj WalkingParallelPair.zero)
          | WalkingParallelPair.one => Iso.refl ((parallelPair f.op g.op).obj WalkingParallelPair.one)).hom =
      (match X_1 with
          | WalkingParallelPair.zero => Iso.refl ((parallelPair f.op g.op).obj WalkingParallelPair.zero)
          | WalkingParallelPair.one => Iso.refl ((parallelPair f.op g.op).obj WalkingParallelPair.one)).hom ≫
        (walkingParallelPairOpEquiv.functor ⋙ (parallelPair f g).op).map f_1

Tactic:
rintro (_ | _ | _) (_ | _ | _) f <;> cases f <;> cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : WithInitial C ⥤ D
x y : C
f : x ⟶ y
⊢ F.map (starInitial.to (of y)) = F.map (starInitial.to (of x)) ≫ F.map (incl.map f)

Tactic:
← F.map_comp

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : WithInitial C ⥤ D
x y : C
f : x ⟶ y
⊢ F.map (starInitial.to (of y)) = F.map (starInitial.to (of x) ≫ incl.map f)
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y P : Cᵒᵖ
f g : X ⟶ Y
ι ι' : P ⟶ X
w : ι ≫ f = ι ≫ g
w' : f.unop ≫ ι'.unop = g.unop ≫ ι'.unop
h : ι = ι'
⊢ (ofι ι w).unop.π ≫ (Iso.refl (ofι ι w).unop.pt).hom = (Cofork.ofπ ι'.unop w').π

Tactic:
by simp [Fork.unop_π, h]

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : WithInitial C ⥤ D
x y : C
f : x ⟶ y
⊢ F.map (starInitial.to (of x)) ≫ F.map (incl.map f) = F.map (starInitial.to (of y))

Tactic:
← F.map_comp

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : WithInitial C ⥤ D
x y : C
f : x ⟶ y
⊢ F.map (starInitial.to (of x) ≫ incl.map f) = F.map (starInitial.to (of y))