mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst✝ : HasPushout f g
⊢ pushout.inl f g ≫ h.isoPushout.inv = inl

Tactic:
dsimp [isoPushout, cocone, CommSq.cocone]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst✝ : HasPushout f g
⊢ pushout.inl f g ≫ (colimit.isoColimitCocone { cocone := PushoutCocone.mk inl inr ⋯, isColimit := h.isColimit }).hom =
    inl
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst✝ : HasPushout f g
⊢ pushout.inr f g ≫ h.isoPushout.inv = inr

Tactic:
dsimp [isoPushout, cocone, CommSq.cocone]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst✝ : HasPushout f g
⊢ pushout.inr f g ≫ (colimit.isoColimitCocone { cocone := PushoutCocone.mk inl inr ⋯, isColimit := h.isColimit }).hom =
    inr
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 R
inst✝ : IsLocalization M A
s : S
x : R
y : ↥M
⊢ s ⊗ₜ[R] (algebraMap R A) x = ((algebraMap R S) x * s) ⊗ₜ[R] 1

Tactic:
← Algebra.smul_def,

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 R
inst✝ : IsLocalization M A
s : S
x : R
y : ↥M
⊢ s ⊗ₜ[R] (algebraMap R A) x = (x • s) ⊗ₜ[R] 1
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case uniq.h₀
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
s : Fork g g'
m : s.pt ⟶ (Fork.ofι f ⋯).pt
e : m ≫ (Fork.ofι f ⋯).ι = s.ι
⊢ m ≫ H.cone.fst = H.isLimit.lift (PullbackCone.mk s.ι s.ι ⋯) ≫ H.cone.fst

Tactic:
refine e.trans ?_

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 : IsPullback f f g g'
s : Fork g g'
m : s.pt ⟶ (Fork.ofι f ⋯).pt
e : m ≫ (Fork.ofι f ⋯).ι = s.ι
⊢ s.ι = H.isLimit.lift (PullbackCone.mk s.ι s.ι ⋯) ≫ H.cone.fst
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: case uniq.h₁
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
s : Fork g g'
m : s.pt ⟶ (Fork.ofι f ⋯).pt
e : m ≫ (Fork.ofι f ⋯).ι = s.ι
⊢ m ≫ H.cone.snd = H.isLimit.lift (PullbackCone.mk s.ι s.ι ⋯) ≫ H.cone.snd

Tactic:
refine e.trans ?_

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 : IsPullback f f g g'
s : Fork g g'
m : s.pt ⟶ (Fork.ofι f ⋯).pt
e : m ≫ (Fork.ofι f ⋯).ι = s.ι
⊢ s.ι = H.isLimit.lift (PullbackCone.mk s.ι s.ι ⋯) ≫ H.cone.snd
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: 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.π ⋯)

Tactic:
refine e.trans ?_

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.π
⊢ s.π = H.cocone.inl ≫ H.isColimit.desc (PushoutCocone.mk s.π s.π ⋯)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic

Goal state before:
pp: 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.π ⋯)

Tactic:
refine e.trans ?_

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.π
⊢ s.π = H.cocone.inr ≫ H.isColimit.desc (PushoutCocone.mk s.π s.π ⋯)
Module: Mathlib.RingTheory.FreeCommRing

Goal state before:
pp: α : Type u
R : Type v
inst✝ : CommRing R
f : FreeCommRing α →+* R
x✝ x y : FreeCommRing α
ihx : (lift (⇑f ∘ of)) x = f x
ihy : (lift (⇑f ∘ of)) y = f y
⊢ (lift (⇑f ∘ of)) x * (lift (⇑f ∘ of)) y = f (x * y)

Tactic:
f.map_mul,

Goal state after:
α : Type u
R : Type v
inst✝ : CommRing R
f : FreeCommRing α →+* R
x✝ x y : FreeCommRing α
ihx : (lift (⇑f ∘ of)) x = f x
ihy : (lift (⇑f ∘ of)) y = f y
⊢ (lift (⇑f ∘ of)) x * (lift (⇑f ∘ of)) y = f x * f y
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
r : R
m : M
s s' c : ↥S
hc :
  ↑c * (↑s * (IsLocalization.sec S (IsLocalization.mk' T r s)).1) =
    ↑c * (↑(IsLocalization.sec S (IsLocalization.mk' T r s)).2 * r)
⊢ ∃ u,
    u • (s * s') • (IsLocalization.sec S (IsLocalization.mk' T r s)).1 • m =
      u • ((IsLocalization.sec S (IsLocalization.mk' T r s)).2 * s') • r • m

Tactic:
use c

Goal state after:
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
r : R
m : M
s s' c : ↥S
hc :
  ↑c * (↑s * (IsLocalization.sec S (IsLocalization.mk' T r s)).1) =
    ↑c * (↑(IsLocalization.sec S (IsLocalization.mk' T r s)).2 * r)
⊢ c • (s * s') • (IsLocalization.sec S (IsLocalization.mk' T r s)).1 • m =
    c • ((IsLocalization.sec S (IsLocalization.mk' T r s)).2 * s') • r • m
Module: Mathlib.Algebra.Group.Submonoid.Units

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
N : Type u_2
inst✝ : Monoid N
f g : M →* N
r : M
hr : f r = g r
h : IsUnit r
s : M
hs : r * s = 1 ∧ s * r = 1
this : ∃ a, r * a = 1 ∧ f a = g a ∧ a * r = 1
⊢ IsUnit ⟨r, hr⟩

Tactic:
simpa [isUnit_iff_exists, ← Subtype.val_inj]

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

Goal state before:
pp: 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
⊢ (L.map (h₁.lift ((fst L R).mapCone s)) ≫ c.pt.hom) ≫ (R.mapCone ((snd L R).mapCone c)).π.app j =
    (s.pt.hom ≫ R.map (h₂.lift ((snd L R).mapCone s))) ≫ (R.mapCone ((snd L R).mapCone c)).π.app j

Tactic:
simp [← Functor.map_comp, ← Functor.map_comp_assoc, ← CommaMorphism.w,
          dsimp% h₂.fac ((snd _ _).mapCone s) j,
          dsimp% h₁.fac ((fst _ _).mapCone s) j]

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 : 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
j : J
⊢ (c.ι.app j ≫ { left := h₁.desc ((fst L R).mapCocone s), right := h₂.desc ((snd L R).mapCocone s), w := ⋯ }).left =
    (s.ι.app j).left

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
j : J
⊢ (c.ι.app j ≫ { left := h₁.desc ((fst L R).mapCocone s), right := h₂.desc ((snd L R).mapCocone s), w := ⋯ }).right =
    (s.ι.app j).right

Tactic:
· exact h₁.fac ((fst _ _).mapCocone s) j

Goal state after:
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
j : J
⊢ (c.ι.app j ≫ { left := h₁.desc ((fst L R).mapCocone s), right := h₂.desc ((snd L R).mapCocone s), w := ⋯ }).right =
    (s.ι.app j).right
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✝ : B ⥤ᵖ C
F : B ⥤ᵒᵖᴸ C
F' : F.PseudoCore
a✝ b✝ c✝ : B
f✝ g✝ : a✝ ⟶ b✝
η : f✝ ⟶ g✝
h : b✝ ⟶ c✝
⊢ F.map₂ (η ▷ h) = F.mapComp f✝ h ≫ F.map₂ η ▷ F.map h ≫ (F'.mapCompIso g✝ h).inv

Tactic:
← F.mapComp_naturality_left_assoc,

Goal state after:
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
D : Type u₃
inst✝ : Bicategory D
F✝ : B ⥤ᵖ C
F : B ⥤ᵒᵖᴸ C
F' : F.PseudoCore
a✝ b✝ c✝ : B
f✝ g✝ : a✝ ⟶ b✝
η : f✝ ⟶ g✝
h : b✝ ⟶ c✝
⊢ F.map₂ (η ▷ h) = F.map₂ (η ▷ h) ≫ F.mapComp g✝ h ≫ (F'.mapCompIso g✝ h).inv
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
inst✝ : IsPreconnected J
α : Type u₂
F : J ⥤ Discrete α
j j' : J
⊢ (F.obj j).as = (F.obj j').as

Tactic:
exact ((isoConstant F j').hom.app j).down.1

Goal state after:
Module: Mathlib.CategoryTheory.IsConnected

Goal state before:
pp: case tail.inl
J : Type u₁
inst✝ : Category.{v₁, u₁} J
α : Type u₁
F : J → α
hF : ∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), F j₁ = F j₂
j j' b✝ c✝ : J
a✝ : Relation.ReflTransGen Zag j b✝
ih : F j = F b✝
hj : b✝ ⟶ c✝
⊢ F b✝ = F c✝

pp: case tail.inr
J : Type u₁
inst✝ : Category.{v₁, u₁} J
α : Type u₁
F : J → α
hF : ∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), F j₁ = F j₂
j j' b✝ c✝ : J
a✝ : Relation.ReflTransGen Zag j b✝
ih : F j = F b✝
hj : c✝ ⟶ b✝
⊢ F b✝ = F c✝

Tactic:
exacts [hF hj, (hF hj).symm]

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case h.right
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FinitePresentation R A
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG
⊢ (RingHom.ker ((↑e).comp f).toRingHom).FG

Tactic:
suffices (RingHom.ker (AlgHom.comp (e : A →ₐ[R] B) f).toRingHom) = RingHom.ker f.toRingHom by
    rw [this]
    exact hf.2

Goal state after:
case h.right
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FinitePresentation R A
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG
⊢ RingHom.ker ((↑e).comp f).toRingHom = RingHom.ker f.toRingHom
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
X Y : Grothendieck F
f : X.Hom Y
⊢ comp f Y.id = f

Tactic:
ext
    · simp [comp, id]
    · dsimp [comp, id]
      rw [← NatIso.naturality_2 ((Cat.Hom.toNatIso <| eqToIso (F.map_id Y.base)) ≪≫
        (eqToIso Cat.Hom.id_toFunctor)) f.fiber]
      simp

Goal state after:
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
G : D ≌ C
⊢ 𝟭 (Grothendieck (G.functor ⋙ F)) =
    map (G.functor.whiskerLeft (whiskerRight G.counitInv F)) ⋙ map (whiskerRight G.unitInv (G.functor ⋙ F))

Tactic:
calc
      _ = map (𝟙 _) := map_id_eq.symm
      _ = map _ := ?_
      _ = map _ ⋙ map _ := map_comp_eq _ _

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
G✝ : C ⥤ Type w
G : D ≌ C
⊢ map (𝟙 (G.functor ⋙ F)) =
    map (G.functor.whiskerLeft (whiskerRight G.counitInv F) ≫ whiskerRight G.unitInv (G.functor ⋙ F))
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.Final
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : CreatesColimit G H
c : Cocone ((F ⋙ G) ⋙ H)
hc : IsColimit c
i : H.mapCocone (liftColimit ((isColimitExtendCoconeEquiv F c).symm hc)) ≅ extendCocone.obj c :=
  liftedColimitMapsToOriginal ((isColimitExtendCoconeEquiv F c).symm hc)
⊢ H.mapCocone (Cocone.whisker F (liftColimit ((isColimitExtendCoconeEquiv F c).symm hc))) ≅ c

Tactic:
exact (Cocone.whiskering F).mapIso i ≪≫ ((coconesEquiv F (G ⋙ H)).unitIso.app _).symm

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Initial
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cone (F ⋙ G)
X : C
Y : D
f : F.obj X ⟶ Y
⊢ ∀ (X₁ X₂ : C) (k₁ : F.obj X₁ ⟶ Y) (k₂ : F.obj X₂ ⟶ Y) (f_1 : X₁ ⟶ X₂),
    F.map f_1 ≫ k₂ = k₁ → c.π.app X₂ ≫ G.map k₂ = c.π.app X ≫ G.map f → c.π.app X₁ ≫ G.map k₁ = c.π.app X ≫ G.map f

Tactic:
· intro _ _ _ _ _ h₁ h₂
    simp [← h₁, ← Functor.comp_map, h₂]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.Initial
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : ReflectsLimit (F ⋙ G) H
c : Cone G
hc : IsLimit (H.mapCone c)
⊢ Nonempty (IsLimit c)

Tactic:
refine ⟨isLimitWhiskerEquiv F _ (isLimitOfReflects H ?_)⟩

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.Initial
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : ReflectsLimit (F ⋙ G) H
c : Cone G
hc : IsLimit (H.mapCone c)
⊢ IsLimit (H.mapCone (Cone.whisker F c))
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst✝³ : HasPullback f₁ f₂
inst✝² : HasPullback f₃ f₄
inst✝¹ : HasPullback (pullback.snd f₁ f₂ ≫ f₃) f₄
inst✝ : HasPullback f₁ (pullback.fst f₃ f₄ ≫ f₂)
⊢ (pullbackAssoc f₁ f₂ f₃ f₄).hom ≫ pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.snd f₃ f₄ =
    pullback.snd (pullback.snd f₁ f₂ ≫ f₃) f₄

Tactic:
by
  trans l₂ ≫ pullback.snd _ _
  · rw [← Category.assoc]
    congr 1
    exact IsLimit.conePointUniqueUpToIso_hom_comp _ _ WalkingCospan.right
  · exact pullback.lift_snd _ _ _

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst✝² : HasPushout g₁ g₂
inst✝¹ : HasPushout g₃ g₄
inst✝ : HasPushout g₁ (g₂ ≫ pushout.inl g₃ g₄)
⊢ (g₃ ≫ pushout.inr g₁ g₂) ≫
      pushout.desc (pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄))
        (pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)) ⋯ =
    g₄ ≫ pushout.inr g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)

Tactic:
rw [Category.assoc, pushout.inr_desc, pushout.condition_assoc]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.RespectsIso
hP₂ : ∀ (X Y S : C) (f : X ⟶ S) (g : Y ⟶ S) [inst : HasPullback f g], P g → P (pullback.fst f g)
X Y Y' S : C
f : X ⟶ S
g : Y ⟶ S
f' : Y' ⟶ Y
g' : Y' ⟶ X
sq : IsPullback f' g' g f
hg : P g
this : HasPullback f g
⊢ P g'

Tactic:
let e := sq.flip.isoPullback

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.RespectsIso
hP₂ : ∀ (X Y S : C) (f : X ⟶ S) (g : Y ⟶ S) [inst : HasPullback f g], P g → P (pullback.fst f g)
X Y Y' S : C
f : X ⟶ S
g : Y ⟶ S
f' : Y' ⟶ Y
g' : Y' ⟶ X
sq : IsPullback f' g' g f
hg : P g
this : HasPullback f g
e : Y' ≅ pullback f g := ⋯.isoPullback
⊢ P g'
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
⊢ (toMorphismProperty fun {R S} [CommRing R] [CommRing S] ↦ P).IsStableUnderCobaseChange ↔
    IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] ↦ P

Tactic:
refine ⟨fun h R S R' S' _ _ _ _ _ _ _ _ _ _ _ hsq hRS ↦ ?_,
      fun h ↦ ⟨fun {R} S R' S' f g f' g' hsq hf ↦ ?_⟩⟩
  · rw [← CommRingCat.isPushout_iff_isPushout] at hsq
    exact h.1 (f := CommRingCat.ofHom (algebraMap R S)) hsq.flip hRS
  · algebraize [f.hom, g.hom, f'.hom, g'.hom, f'.hom.comp g.hom]
    have : IsScalarTower R S S' := .of_algebraMap_eq fun x ↦ congr($(hsq.1.1).hom x)
    have : Algebra.IsPushout R S R' S' := (CommRingCat.isPushout_iff_isPushout.mp hsq).symm
    exact h (R := R) (S := S) _ _ hf

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y Z : C
e : X ≅ Y
f : Y ⟶ Z
hf : P.universally f
X' Z' : C
i₁ : X' ⟶ X
i₂ : Z' ⟶ Z
f' : X' ⟶ Z'
H : IsPullback f' i₁ i₂ (e.hom ≫ f)
⊢ 𝟙 X' ≫ i₁ = (i₁ ≫ e.hom) ≫ e.inv

Tactic:
by rw [Category.id_comp, Category.assoc, e.hom_inv_id, Category.comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M✝ N✝ O X Y : C
inst✝² : MonObj M✝
inst✝¹ : MonObj N✝
inst✝ : MonObj O
M N : Mon C
α : yonedaMonObj M.X ⟶ yonedaMonObj N.X
⊢ (MonCat.Hom.hom (α.app (op (M.X ⊗ M.X)))) (fst M.X M.X) * (MonCat.Hom.hom (α.app (op (M.X ⊗ M.X)))) (snd M.X M.X) =
    ((ConcreteCategory.hom (α.app (op M.X))) (𝟙 M.X) ⊗ₘ (ConcreteCategory.hom (α.app (op M.X))) (𝟙 M.X)) ≫ μ

Tactic:
change lift _ _ ≫ μ[N.X] = _

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M✝ N✝ O X Y : C
inst✝² : MonObj M✝
inst✝¹ : MonObj N✝
inst✝ : MonObj O
M N : Mon C
α : yonedaMonObj M.X ⟶ yonedaMonObj N.X
⊢ lift ((MonCat.Hom.hom (α.app (op (M.X ⊗ M.X)))) (fst M.X M.X))
        ((MonCat.Hom.hom (α.app (op (M.X ⊗ M.X)))) (snd M.X M.X)) ≫
      μ =
    ((ConcreteCategory.hom (α.app (op M.X))) (𝟙 M.X) ⊗ₘ (ConcreteCategory.hom (α.app (op M.X))) (𝟙 M.X)) ≫ μ
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : CartesianMonoidalCategory D
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X Y : C
⊢ F.map (X ◁ toUnit Y) ≫ δ F X (𝟙_ C) ≫ fst (F.obj X) (F.obj (𝟙_ C)) = F.map (X ◁ toUnit Y) ≫ F.map (ρ_ X).hom

Tactic:
simp [← OplaxMonoidal.right_unitality_hom, rightUnitor_hom (F.obj X)]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : CartesianMonoidalCategory D
F : C ⥤ D
inst✝ : F.OplaxMonoidal
X Y : C
⊢ F.map (X ◁ toUnit Y) ≫ F.map (ρ_ X).hom = F.map (fst X Y)

Tactic:
· simp [← Functor.map_comp, rightUnitor_hom]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : MonoidalCategory C
A₁ A₂ A₃ : C
inst✝² : Closed A₁
inst✝¹ : Closed A₂
inst✝ : Closed A₃
f : A₁ ⟶ A₂
g : A₂ ⟶ A₃
⊢ pre (f ≫ g) = pre g ≫ pre f

Tactic:
by
  rw [pre, pre, pre, conjugateEquiv_comp, (tensoringLeft C).map_comp]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Subfield

Goal state before:
pp: α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ ∀ {x : ↥(closure s)},
    x ∈ Set.range (WType.elim (↥(closure s)) (operate s)) → -x ∈ Set.range (WType.elim (↥(closure s)) (operate s))

Tactic:
rintro _ ⟨x, rfl⟩

Goal state after:
α : Type u
s : Set α
inst✝ : DivisionRing α
x : WType (Operands s)
⊢ -WType.elim (↥(closure s)) (operate s) x ∈ Set.range (WType.elim (↥(closure s)) (operate s))
Module: Mathlib.SetTheory.Cardinal.Subfield

Goal state before:
pp: α : Type u
s : Set α
inst✝ : DivisionRing α
⊢ ∀ x ∈ Set.range (WType.elim (↥(closure s)) (operate s)), x⁻¹ ∈ Set.range (WType.elim (↥(closure s)) (operate s))

Tactic:
rintro _ ⟨x, rfl⟩

Goal state after:
α : Type u
s : Set α
inst✝ : DivisionRing α
x : WType (Operands s)
⊢ (WType.elim (↥(closure s)) (operate s) x)⁻¹ ∈ Set.range (WType.elim (↥(closure s)) (operate s))
Module: Mathlib.LinearAlgebra.Dual.Basis

Goal state before:
pp: R : Type uR
M : Type uM
ι : Type uι
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
m : M
a : b.toDual m = 0
⊢ b.toDual m = b.toDual 0

Tactic:
rwa [map_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.RankNullity

Goal state before:
pp: R : Type u_1
M : Type u
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : HasRankNullity.{u, u_1} R
inst✝ : StrongRankCondition R
s : Set M
hs : LinearIndepOn R _root_.id s
⊢ ∃ t, s ⊆ t ∧ #↑t = Module.rank R M ∧ LinearIndepOn R _root_.id t

Tactic:
obtain ⟨t, ht, ht'⟩ := exists_set_linearIndependent R (M ⧸ Submodule.span R s)

Goal state after:
R : Type u_1
M : Type u
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : HasRankNullity.{u, u_1} R
inst✝ : StrongRankCondition R
s : Set M
hs : LinearIndepOn R _root_.id s
t : Set (M ⧸ span R s)
ht : #↑t = Module.rank R (M ⧸ span R s)
ht' : LinearIndependent (ι := ↑t) R Subtype.val
⊢ ∃ t, s ⊆ t ∧ #↑t = Module.rank R M ∧ LinearIndepOn R _root_.id t
Module: Mathlib.LinearAlgebra.Dimension.RankNullity

Goal state before:
pp: R : Type u_1
M : Type u
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : HasRankNullity.{u, u_1} R
inst✝ : StrongRankCondition R
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
h : ↑n < Module.rank R M
t : Set M
h₁ : Set.range v ⊆ t
h₂ : #↑t = Module.rank R M
h₃ : LinearIndepOn R _root_.id t
this : Set.range v ≠ t
x : M
hx : x ∈ t
hx' : x ∉ Set.range v
⊢ ∃ x, LinearIndependent R (Fin.cons x v)

Tactic:
exact ⟨x, (linearIndepOn_id_range_iff (Fin.cons_injective_iff.mpr ⟨hx', hv.injective⟩)).mp
    (h₃.mono (Fin.range_cons x v ▸ insert_subset hx h₁))⟩

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.Finite.Matrix

Goal state before:
pp: R : Type u
S : Type u'
M : Type v
N : Type w
inst✝¹² : Ring R
inst✝¹¹ : Ring S
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
inst✝⁸ : Free R M
inst✝⁷ : Module.Finite R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
inst✝⁴ : Module S N
inst✝³ : SMulCommClass R S N
inst✝² : StrongRankCondition R
inst✝¹ : StrongRankCondition S
inst✝ : Free S N
⊢ finrank S (M →ₗ[R] N) = finrank R M * finrank S N

Tactic:
simp_rw [finrank, rank_linearMap, toNat_mul, toNat_lift]

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
hp : p < ⊤
hp' : Projective R (M ⧸ p)
⊢ ∃ x, x ∉ p

Tactic:
by rw [lt_top_iff_ne_top] at hp; contrapose! hp; ext; simp [hp]

Goal state after: