mathlib-initiative/mathlib-tactics huggingface dataset:
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₃
⊢ (s.fst ≫ g₁) ≫ g₂ = s.snd ≫ i₃

Tactic:
← s.condition,

Goal state after:
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₃
⊢ (s.fst ≫ g₁) ≫ g₂ = s.fst ≫ g₁ ≫ g₂
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'
inst✝ : IsLocalizedModule S f
Q : Type (max u_3 u_4 u_2)
x✝³ : AddCommMonoid Q
x✝² : Module R Q
x✝¹ : Module A Q
x✝ : IsScalarTower R A Q
ℓ : M' →ₗ[R] Q
h₂ : ∀ (y : M' →ₗ[R] Q), (fun l ↦ l ∘ₗ f = ℓ ∘ₗ f) y → y = ℓ
g'' : M' →ₗ[A] Q
h : (fun g' ↦ ↑R g' ∘ₗ f = ℓ ∘ₗ f) g''
⊢ g'' = LinearMap.extendScalarsOfIsLocalization S A ℓ

Tactic:
cases h₂ (LinearMap.restrictScalars R g'') h

Goal state after:
case refl
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'
inst✝ : IsLocalizedModule S f
Q : Type (max u_3 u_4 u_2)
x✝³ : AddCommMonoid Q
x✝² : Module R Q
x✝¹ : Module A Q
x✝ : IsScalarTower R A Q
g'' : M' →ₗ[A] Q
h₂ : ∀ (y : M' →ₗ[R] Q), (fun l ↦ l ∘ₗ f = ↑R g'' ∘ₗ f) y → y = ↑R g''
h : ↑R g'' ∘ₗ f = ↑R g'' ∘ₗ f
⊢ g'' = LinearMap.extendScalarsOfIsLocalization S A (↑R g'')
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 ⟶ Y
g : X ⟶ Z
g' : Z ⟶ W
inst✝¹ : HasPushout f g
inst✝ : HasPushout (pushout.inr f g) g'
⊢ pushout.inr f g ≫ pushout.inl (pushout.inr f g) g' =
    g' ≫ pushout.inr f (g ≫ g') ≫ (pushoutLeftPushoutInrIso f g g').inv

Tactic:
inr_pushoutLeftPushoutInrIso_inv,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
g' : Z ⟶ W
inst✝¹ : HasPushout f g
inst✝ : HasPushout (pushout.inr f g) g'
⊢ pushout.inr f g ≫ pushout.inl (pushout.inr f g) g' = g' ≫ pushout.inr (pushout.inr f g) g'
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
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
x : S
a : A
⊢ (tensorProductEquivOfMapIncludeRight R S M B C) (x ⊗ₜ[R] (algebraMap A B) a) = (algebraMap (S ⊗[R] A) C) (x ⊗ₜ[R] a)

Tactic:
by
  let : Algebra (S ⊗[R] A) (S ⊗[R] B) :=
    (Algebra.TensorProduct.map (AlgHom.id R S) (IsScalarTower.toAlgHom R _ _)).toAlgebra
  have heq : x ⊗ₜ[R] (algebraMap A B) a = algebraMap _ _ (x ⊗ₜ[R] a) := rfl
  simp [heq, IsLocalization.tensorProductEquivOfMapIncludeRight]

Goal state after:
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 + y) = f (x + y)

Tactic:
by rw [map_add, f.map_add, ihx, ihy]

Goal state after:
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
r : R
m : M
s t : ↥S
⊢ r • m /ₒ (t * s) = mk (r • m) (s * t)

Tactic:
rw [mul_comm]

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
⊢ (∀ ⦃a₁ a₂ : M⦄, f a₁ = f a₂ → a₁ = a₂) ↔ ∀ (c : ↥S) ⦃a₁ a₂ : M⦄, c • a₁ = c • a₂ → a₁ = a₂

Tactic:
eq_iff_exists S,

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
⊢ (∀ ⦃a₁ a₂ : M⦄, (∃ c, c • a₁ = c • a₂) → a₁ = a₂) ↔ ∀ (c : ↥S) ⦃a₁ a₂ : M⦄, c • a₁ = c • a₂ → a₁ = a₂
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
M : Type u_2
inst✝⁹ : AddCommMonoid M
A : Type u_5
inst✝⁸ : CommSemiring A
inst✝⁷ : Algebra R A
inst✝⁶ : Module R M
S : Submonoid R
inst✝⁵ : Module A M
N : Type u_6
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
inst✝² : Module A N
inst✝¹ : IsScalarTower R A M
inst✝ : IsScalarTower R A N
f : M →ₗ[A] N
h : IsLocalizedModule (Algebra.algebraMapSubmonoid A S) f
x₁ x₂ : M
e : (↑R f) x₁ = (↑R f) x₂
r : R
hr : r ∈ ↑S
hc : ⟨(algebraMap R A) r, ⋯⟩ • x₁ = ⟨(algebraMap R A) r, ⋯⟩ • x₂
⊢ ∃ c, c • x₁ = c • x₂

Tactic:
exact ⟨⟨r, hr⟩, by simpa [Submonoid.smul_def] using hc⟩

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
G : D ⥤ C
F : C ⥤ D
h : F ⊣ G
A : D
s : Cone (Functor.empty (CostructuredArrow F A))
m : s.pt ⟶ (asEmptyCone (CostructuredArrow.mk (h.counit.app A))).pt
x✝ : ∀ (j : Discrete PEmpty.{1}), m ≫ (asEmptyCone (CostructuredArrow.mk (h.counit.app A))).π.app j = s.π.app j
⊢ m = CostructuredArrow.homMk ((h.homEquiv s.pt.left A) s.pt.hom) ⋯

Tactic:
by
    apply CostructuredArrow.ext
    simp [← CostructuredArrow.w m]

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_6
M' : Type u_7
inst✝⁴ : NonUnitalNonAssocSemiring M
inst✝³ : Semiring M'
inst✝² : Module R M
inst✝¹ : Algebra R M'
f : M →ₗ[R] M'
hf : ∀ (m₁ m₂ : M), f (m₁ * m₂) = f m₁ * f m₂
inst✝ : IsLocalizedModule S f
m₁ m₂ : M
s₁ s₂ : ↥S
⊢ f (m₁ • m₂) = (↑s₁ • ↑s₂) • mk' f m₁ s₁ • mk' f m₂ s₂

Tactic:
smul_smul_smul_comm,

Goal state after:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_6
M' : Type u_7
inst✝⁴ : NonUnitalNonAssocSemiring M
inst✝³ : Semiring M'
inst✝² : Module R M
inst✝¹ : Algebra R M'
f : M →ₗ[R] M'
hf : ∀ (m₁ m₂ : M), f (m₁ * m₂) = f m₁ * f m₂
inst✝ : IsLocalizedModule S f
m₁ m₂ : M
s₁ s₂ : ↥S
⊢ f (m₁ • m₂) = (↑s₁ • mk' f m₁ s₁) • ↑s₂ • mk' f m₂ s₂
Module: Mathlib.Algebra.Category.Ring.Constructions

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

pp: case property.right
A B : CommRingCat
f g : A ⟶ B
s : Fork f g
⊢ ∀ {m : s.pt ⟶ (equalizerFork f g).pt},
    m ≫ (equalizerFork f g).ι = s.ι → m = ofHom ((Hom.hom s.ι).codRestrict ((Hom.hom f).eqLocus (Hom.hom g)) ⋯)

Tactic:
· ext
    rfl

Goal state after:
case property.right
A B : CommRingCat
f g : A ⟶ B
s : Fork f g
⊢ ∀ {m : s.pt ⟶ (equalizerFork f g).pt},
    m ≫ (equalizerFork f g).ι = s.ι → m = ofHom ((Hom.hom s.ι).codRestrict ((Hom.hom f).eqLocus (Hom.hom g)) ⋯)
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
inst✝¹ : ∀ (a : B), IsIso (F.mapId a)
inst✝ : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), IsIso (F.mapComp f g)
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 ≫ inv (F.mapComp g✝ h)

Tactic:
rw [← assoc, IsIso.eq_comp_inv, F.mapComp_naturality_left]

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

Goal state before:
pp: case singleton
R : Type u_3
inst✝ : CommSemiring R
I J : Ideal R
x : R
n : ℕ
hn : x ^ n ∈ J
⊢ ∃ n, (R ∙ x) ^ n ≤ J

Tactic:
refine ⟨n, by simpa [span_singleton_pow, span_le]⟩

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

Goal state before:
pp: T : Type u_1
inst✝¹ : Category.{v_1, u_1} T
P Q : MorphismProperty T
X : T
inst✝ : Q.IsMultiplicative
A B : P.Over Q X
f g : A ⟶ B
h : f.left = g.left
⊢ f = g

Tactic:
ext
  · exact h
  · simp

Goal state after:
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
x y : F.Elements
f : y ⟶ x
⊢ (𝟭 F.Elementsᵒᵖ).map (op f) ≫
      (isoMk ((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj (op y)))) (unop (op y))
            (Iso.refl ((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj (op y)))).fst) ⋯).op.hom =
    (isoMk ((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj (op x)))) (unop (op x))
            (Iso.refl ((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj (op x)))).fst) ⋯).op.hom ≫
      (toCostructuredArrow F ⋙ (fromCostructuredArrow F).rightOp).map (op f)

Tactic:
exact Quiver.Hom.unop_inj (by ext; simp)

Goal state after:
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
⊢ colimMap
        (whiskerRight (Grothendieck.ιNatTrans (𝟙 X)) G ≫
          ((F.map (𝟙 X)).toFunctor.associator (Grothendieck.ι F X) G).hom) ≫
      colimit.pre (Grothendieck.ι F X ⋙ G) (F.map (𝟙 X)).toFunctor =
    𝟙 (colimit (Grothendieck.ι F X ⋙ G))

Tactic:
ext d

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)
⊢ colimit.ι (Grothendieck.ι F X ⋙ G) d ≫
      colimMap
          (whiskerRight (Grothendieck.ιNatTrans (𝟙 X)) G ≫
            ((F.map (𝟙 X)).toFunctor.associator (Grothendieck.ι F X) G).hom) ≫
        colimit.pre (Grothendieck.ι F X ⋙ G) (F.map (𝟙 X)).toFunctor =
    colimit.ι (Grothendieck.ι F X ⋙ G) d ≫ 𝟙 (colimit (Grothendieck.ι F X ⋙ G))
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 Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ colimMap
        (whiskerRight (Grothendieck.ιNatTrans (f ≫ g)) G ≫
          ((F.map (f ≫ g)).toFunctor.associator (Grothendieck.ι F Z) G).hom) ≫
      colimit.pre (Grothendieck.ι F Z ⋙ G) (F.map (f ≫ g)).toFunctor =
    (colimMap
          (whiskerRight (Grothendieck.ιNatTrans f) G ≫ ((F.map f).toFunctor.associator (Grothendieck.ι F Y) G).hom) ≫
        colimit.pre (Grothendieck.ι F Y ⋙ G) (F.map f).toFunctor) ≫
      colimMap
          (whiskerRight (Grothendieck.ιNatTrans g) G ≫ ((F.map g).toFunctor.associator (Grothendieck.ι F Z) G).hom) ≫
        colimit.pre (Grothendieck.ι F Z ⋙ G) (F.map g).toFunctor

Tactic:
ext d

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 Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
d : ↑(F.obj X)
⊢ colimit.ι (Grothendieck.ι F X ⋙ G) d ≫
      colimMap
          (whiskerRight (Grothendieck.ιNatTrans (f ≫ g)) G ≫
            ((F.map (f ≫ g)).toFunctor.associator (Grothendieck.ι F Z) G).hom) ≫
        colimit.pre (Grothendieck.ι F Z ⋙ G) (F.map (f ≫ g)).toFunctor =
    colimit.ι (Grothendieck.ι F X ⋙ G) d ≫
      (colimMap
            (whiskerRight (Grothendieck.ιNatTrans f) G ≫ ((F.map f).toFunctor.associator (Grothendieck.ι F Y) G).hom) ≫
          colimit.pre (Grothendieck.ι F Y ⋙ G) (F.map f).toFunctor) ≫
        colimMap
            (whiskerRight (Grothendieck.ιNatTrans g) G ≫ ((F.map g).toFunctor.associator (Grothendieck.ι F Z) G).hom) ≫
          colimit.pre (Grothendieck.ι F Z ⋙ G) (F.map g).toFunctor
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 Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
d : ↑(F.obj X)
⊢ G.map { base := f ≫ g, fiber := 𝟙 ((F.map (f ≫ g)).toFunctor.obj ((Grothendieck.ι F X).obj d).fiber) } ≫
      colimit.ι (Grothendieck.ι F Z ⋙ G) ((F.map (f ≫ g)).toFunctor.obj d) =
    (G.map { base := f, fiber := 𝟙 ((F.map f).toFunctor.obj ((Grothendieck.ι F X).obj d).fiber) } ≫
        G.map
          { base := g,
            fiber := 𝟙 ((F.map g).toFunctor.obj ((Grothendieck.ι F Y).obj ((F.map f).toFunctor.obj d)).fiber) }) ≫
      colimit.ι (Grothendieck.ι F Z ⋙ G) ((F.map g).toFunctor.obj ((F.map f).toFunctor.obj d))

Tactic:
← G.map_comp

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 Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
d : ↑(F.obj X)
⊢ G.map { base := f ≫ g, fiber := 𝟙 ((F.map (f ≫ g)).toFunctor.obj ((Grothendieck.ι F X).obj d).fiber) } ≫
      colimit.ι (Grothendieck.ι F Z ⋙ G) ((F.map (f ≫ g)).toFunctor.obj d) =
    G.map
        ({ base := f, fiber := 𝟙 ((F.map f).toFunctor.obj ((Grothendieck.ι F X).obj d).fiber) } ≫
          { base := g,
            fiber := 𝟙 ((F.map g).toFunctor.obj ((Grothendieck.ι F Y).obj ((F.map f).toFunctor.obj d)).fiber) }) ≫
      colimit.ι (Grothendieck.ι F Z ⋙ G) ((F.map g).toFunctor.obj ((F.map f).toFunctor.obj d))
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: case w_fiber
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
⊢ eqToHom ⋯ ≫ (comp f Y.id).fiber = f.fiber

Tactic:
dsimp [comp, id]

Goal state after:
case w_fiber
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
⊢ eqToHom ⋯ ≫ eqToHom ⋯ ≫ (F.map (𝟙 Y.base)).toFunctor.map f.fiber ≫ eqToHom ⋯ = f.fiber
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)
c : Cocone (fiberwiseColimit G)
X Y : Grothendieck F
x✝ : X ⟶ Y
f : X.base ⟶ Y.base
g : (F.map f).toFunctor.obj X.fiber ⟶ Y.fiber
⊢ (G.map { base := f, fiber := g } ≫ colimit.ι (Grothendieck.ι F Y.base ⋙ G) Y.fiber) ≫ c.ι.app Y.base =
    ((G.map ((Grothendieck.ιNatTrans f).app X.fiber) ≫ G.map ((Grothendieck.ι F Y.base).map g)) ≫
        colimit.ι (Grothendieck.ι F Y.base ⋙ G) Y.fiber) ≫
      c.ι.app Y.base

Tactic:
← G.map_comp

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)
c : Cocone (fiberwiseColimit G)
X Y : Grothendieck F
x✝ : X ⟶ Y
f : X.base ⟶ Y.base
g : (F.map f).toFunctor.obj X.fiber ⟶ Y.fiber
⊢ (G.map { base := f, fiber := g } ≫ colimit.ι (Grothendieck.ι F Y.base ⋙ G) Y.fiber) ≫ c.ι.app Y.base =
    (G.map ((Grothendieck.ιNatTrans f).app X.fiber ≫ (Grothendieck.ι F Y.base).map g) ≫
        colimit.ι (Grothendieck.ι F Y.base ⋙ G) Y.fiber) ≫
      c.ι.app Y.base
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)
c : Cocone (fiberwiseColimit G)
hc : IsColimit c
s : Cocone G
m : (coconeOfCoconeFiberwiseColimit c).pt ⟶ s.pt
X : C
hm : ∀ (j : Grothendieck F), colimit.ι (Grothendieck.ι F j.base ⋙ G) j.fiber ≫ c.ι.app j.base ≫ m = s.ι.app j
⊢ c.ι.app X ≫ m = colimit.desc (Grothendieck.ι F X ⋙ G) (Cocone.whisker (Grothendieck.ι F X) s)

Tactic:
ext d

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)
c : Cocone (fiberwiseColimit G)
hc : IsColimit c
s : Cocone G
m : (coconeOfCoconeFiberwiseColimit c).pt ⟶ s.pt
X : C
hm : ∀ (j : Grothendieck F), colimit.ι (Grothendieck.ι F j.base ⋙ G) j.fiber ≫ c.ι.app j.base ≫ m = s.ι.app j
d : ↑(F.obj X)
⊢ colimit.ι (Grothendieck.ι F X ⋙ G) d ≫ c.ι.app X ≫ m =
    colimit.ι (Grothendieck.ι F X ⋙ G) d ≫ colimit.desc (Grothendieck.ι F X ⋙ G) (Cocone.whisker (Grothendieck.ι F X) s)
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case inr
R : Type w₁
A : Type w₂
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f
inst✝ : FinitePresentation R A
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ⇑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker f'.toRingHom
RXn : Type (max w₁ 0) := MvPolynomial (Fin n) R
RXm : Type (max w₁ 0) := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), f' (g i) = f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), f (h i) = f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i ↦ MvPolynomial.X i - aeval_h (g i)
hh' : ∀ (x : RXm), f (aeval_h x) = f' x
s' : Set RXn := Set.range g' ∪ ⇑aeval_h '' ↑s
x : RXm
hx : x ∈ ↑s
⊢ f' x = 0

Tactic:
change x ∈ RingHom.ker f'.toRingHom

Goal state after:
case inr
R : Type w₁
A : Type w₂
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f
inst✝ : FinitePresentation R A
m : ℕ
f' : MvPolynomial (Fin m) R →ₐ[R] A
hf' : Surjective ⇑f'
s : Finset (MvPolynomial (Fin m) R)
hs : Ideal.span ↑s = RingHom.ker f'.toRingHom
RXn : Type (max w₁ 0) := MvPolynomial (Fin n) R
RXm : Type (max w₁ 0) := MvPolynomial (Fin m) R
g : Fin n → MvPolynomial (Fin m) R
hg : ∀ (i : Fin n), f' (g i) = f (MvPolynomial.X i)
h : Fin m → MvPolynomial (Fin n) R
hh : ∀ (i : Fin m), f (h i) = f' (MvPolynomial.X i)
aeval_h : RXm →ₐ[R] RXn := MvPolynomial.aeval h
g' : Fin n → RXn := fun i ↦ MvPolynomial.X i - aeval_h (g i)
hh' : ∀ (x : RXm), f (aeval_h x) = f' x
s' : Set RXn := Set.range g' ∪ ⇑aeval_h '' ↑s
x : RXm
hx : x ∈ ↑s
⊢ x ∈ RingHom.ker f'.toRingHom
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✝ : PreservesLimit G H
c : Cone (F ⋙ G)
hc : IsLimit c
⊢ IsLimit (extendCone.obj (H.mapCone c))

Tactic:
let hc' := isLimitOfPreserves H ((isLimitExtendConeEquiv F c).symm hc)

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✝ : PreservesLimit G H
c : Cone (F ⋙ G)
hc : IsLimit c
hc' : IsLimit (H.mapCone (extendCone.obj c)) := isLimitOfPreserves H ((isLimitExtendConeEquiv F c).symm hc)
⊢ IsLimit (extendCone.obj (H.mapCone c))
Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hr : RegularMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
⊢ g ≫ k ≫ hr.left = g ≫ k ≫ hr.right

Tactic:
rw [← Category.assoc, ← eq_whisker comm]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hr : RegularMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
⊢ (f ≫ h) ≫ hr.left = g ≫ k ≫ hr.right
Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hr : RegularMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
⊢ (f ≫ h) ≫ hr.left = g ≫ k ≫ hr.right

Tactic:
rw [← Category.assoc, ← eq_whisker comm]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hr : RegularMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
⊢ (f ≫ h) ≫ hr.left = (f ≫ h) ≫ hr.right
Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hr : RegularMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
⊢ (f ≫ h) ≫ hr.left = (f ≫ h) ≫ hr.right

Tactic:
rw [← Category.assoc, ← eq_whisker comm]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hr : RegularMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
⊢ (f ≫ h) ≫ hr.left = (f ≫ h) ≫ hr.right
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
inst✝ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
⊢ snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      fst (i₁ ≫ snd f i) (i₂ ≫ snd f i) ≫ i₁ ≫ fst f i =
    fst (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫ 𝟙 X

Tactic:
← diagonal_fst f,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
inst✝ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
⊢ snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      fst (i₁ ≫ snd f i) (i₂ ≫ snd f i) ≫ i₁ ≫ fst f i =
    fst (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫ diagonal f ≫ fst f f
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : IsStableUnderBaseChange P
hP' : RespectsIso P
R S T : CommRingCat
f : R ⟶ S
g : R ⟶ T
H : P (CommRingCat.Hom.hom g)
this✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom f).toAlgebra
this : Algebra ↑R ↑T := (CommRingCat.Hom.hom g).toAlgebra
⊢ P (CommRingCat.Hom.hom (pushout.inl f g))

Tactic:
rw [← show _ = pushout.inl f g from
      colimit.isoColimitCocone_ι_inv ⟨_, CommRingCat.pushoutCoconeIsColimit R S T⟩ WalkingSpan.left,
    CommRingCat.hom_comp, hP'.cancel_right_isIso]

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : IsStableUnderBaseChange P
hP' : RespectsIso P
R S T : CommRingCat
f : R ⟶ S
g : R ⟶ T
H : P (CommRingCat.Hom.hom g)
this✝ : Algebra ↑R ↑S := (CommRingCat.Hom.hom f).toAlgebra
this : Algebra ↑R ↑T := (CommRingCat.Hom.hom g).toAlgebra
⊢ P
    (CommRingCat.Hom.hom
      ({ cocone := CommRingCat.pushoutCocone ↑R ↑S ↑T,
                isColimit := CommRingCat.pushoutCoconeIsColimit ↑R ↑S ↑T }.cocone.ι.app
        WalkingSpan.left))