mathlib-initiative/mathlib-tactics huggingface dataset:
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''
A : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Module A M'
inst✝⁴ : IsLocalization S A
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
inst✝ : IsScalarTower R A M'
f : M →ₗ[R] M'
g : M →ₗ[R] M''
e : M' ≃ₗ[R] M''
hf : IsLocalizedModule S f
x : M''
p : M × ↥S
h : p.2 • e.symm x = f p.1
⊢ p.2 • x = (↑e ∘ₗ f) p.1

Tactic:
LinearMap.coe_comp,

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''
A : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Module A M'
inst✝⁴ : IsLocalization S A
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
inst✝ : IsScalarTower R A M'
f : M →ₗ[R] M'
g : M →ₗ[R] M''
e : M' ≃ₗ[R] M''
hf : IsLocalizedModule S f
x : M''
p : M × ↥S
h : p.2 • e.symm x = f p.1
⊢ p.2 • x = (⇑↑e ∘ ⇑f) p.1
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''
A : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Module A M'
inst✝⁴ : IsLocalization S A
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
inst✝ : IsScalarTower R A M'
f : M →ₗ[R] M'
g : M →ₗ[R] M''
e : M' ≃ₗ[R] M''
hf : IsLocalizedModule S f
x₁✝ x₂✝ : M
h : (↑e ∘ₗ f) x₁✝ = (↑e ∘ₗ f) x₂✝
⊢ ∃ c, c • x₁✝ = c • x₂✝

Tactic:
LinearMap.coe_comp,

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''
A : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Module A M'
inst✝⁴ : IsLocalization S A
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
inst✝ : IsScalarTower R A M'
f : M →ₗ[R] M'
g : M →ₗ[R] M''
e : M' ≃ₗ[R] M''
hf : IsLocalizedModule S f
x₁✝ x₂✝ : M
h : (⇑↑e ∘ ⇑f) x₁✝ = (⇑↑e ∘ ⇑f) x₂✝
⊢ ∃ c, c • x₁✝ = c • 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''
A : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Module A M'
inst✝⁴ : IsLocalization S A
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
inst✝ : IsScalarTower R A M'
f : M →ₗ[R] M'
g : M →ₗ[R] M''
e : M'' ≃ₗ[R] M
hf : IsLocalizedModule S f
x₁✝ x₂✝ : M''
h : (f ∘ₗ ↑e) x₁✝ = (f ∘ₗ ↑e) x₂✝
⊢ ∃ c, c • x₁✝ = c • x₂✝

Tactic:
LinearMap.coe_comp,

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''
A : Type u_5
inst✝⁷ : CommSemiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Module A M'
inst✝⁴ : IsLocalization S A
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
inst✝ : IsScalarTower R A M'
f : M →ₗ[R] M'
g : M →ₗ[R] M''
e : M'' ≃ₗ[R] M
hf : IsLocalizedModule S f
x₁✝ x₂✝ : M''
h : (⇑f ∘ ⇑↑e) x₁✝ = (⇑f ∘ ⇑↑e) x₂✝
⊢ ∃ c, c • x₁✝ = c • x₂✝
Module: Mathlib.Algebra.Module.LocalizedModule.Basic

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

Tactic:
LinearMap.coe_comp,

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_6
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
S T : Submonoid R
h : S ≤ T
h' : ∀ (x : ↥T), ∃ m, m * ↑x ∈ S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule S f
y : N
⊢ ∃ x, x.2 • y = f x.1

Tactic:
by
    obtain ⟨⟨x, t⟩, e⟩ := IsLocalizedModule.surj S f y
    exact ⟨⟨x, ⟨t, h t.2⟩⟩, e⟩

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
s : PushoutCocone (ofHom (algebraMap R A)) (ofHom (algebraMap R B))
⊢ { l //
    (pushoutCocone R A B).inl ≫ l = s.inl ∧
      (pushoutCocone R A B).inr ≫ l = s.inr ∧
        ∀ {m : (pushoutCocone R A B).pt ⟶ s.pt},
          (pushoutCocone R A B).inl ≫ m = s.inl → (pushoutCocone R A B).inr ≫ m = s.inr → m = l }

Tactic:
letI := RingHom.toAlgebra (s.inl.hom.comp (algebraMap R A))

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
⊢ { l //
    (pushoutCocone R A B).inl ≫ l = s.inl ∧
      (pushoutCocone R A B).inr ≫ l = s.inr ∧
        ∀ {m : (pushoutCocone R A B).pt ⟶ s.pt},
          (pushoutCocone R A B).inl ≫ m = s.inl → (pushoutCocone R A B).inr ≫ m = s.inr → m = l }
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)
⊢ (LocalizedModule.lift S g h ∘ₗ ↑(iso S f).symm) ∘ₗ f = g

Tactic:
LinearMap.comp_assoc,

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)
⊢ LocalizedModule.lift S g h ∘ₗ ↑(iso S f).symm ∘ₗ f = g
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)) ∘ₗ ↑(iso S f).symm = l

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 = g

Tactic:
LinearMap.comp_assoc,

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
⊢ l ∘ₗ ↑(iso S f) ∘ₗ ↑(iso S f).symm = l

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 = g
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 = g

Tactic:
LinearMap.comp_assoc,

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
⊢ l ∘ₗ ↑(iso S f) ∘ₗ LocalizedModule.mkLinearMap S M = g
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: J : Type u'
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
c : Cone F
hc : IsLimit c
r : ↑c.pt
inv : (j : J) → ↑(F.obj j)
h_inv : ∀ (j : J), (ConcreteCategory.hom (c.π.app j)) r * inv j = 1
map_inv : ∀ {j k : J} (f : j ⟶ k), (ConcreteCategory.hom (F.map f)) (inv j) = inv k
inv_r : Cone F :=
  { pt := of (FreeCommRing PUnit.{u + 1}),
    π := { app := fun j ↦ ConcreteCategory.ofHom (FreeCommRing.lift fun x ↦ inv j), naturality := ⋯ } }
j : J
⊢ (ConcreteCategory.hom (hc.lift inv_r ≫ c.π.app j)) (FreeCommRing.of PUnit.unit) = inv j

Tactic:
rw [IsLimit.fac]

Goal state after:
J : Type u'
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
c : Cone F
hc : IsLimit c
r : ↑c.pt
inv : (j : J) → ↑(F.obj j)
h_inv : ∀ (j : J), (ConcreteCategory.hom (c.π.app j)) r * inv j = 1
map_inv : ∀ {j k : J} (f : j ⟶ k), (ConcreteCategory.hom (F.map f)) (inv j) = inv k
inv_r : Cone F :=
  { pt := of (FreeCommRing PUnit.{u + 1}),
    π := { app := fun j ↦ ConcreteCategory.ofHom (FreeCommRing.lift fun x ↦ inv j), naturality := ⋯ } }
j : J
⊢ (ConcreteCategory.hom (inv_r.π.app j)) (FreeCommRing.of PUnit.unit) = inv j
Module: Mathlib.CategoryTheory.ObjectProperty.Opposite

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
P Q : ObjectProperty Cᵒᵖ
h : P.unop = Q.unop
⊢ P = Q

Tactic:
rw [← P.op_unop, ← Q.op_unop, h]

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

Goal state before:
pp: case refine_1
X : Type u
⊢ binaryProductFunctor.obj X ≅ prod.functor.obj X

Tactic:
refine NatIso.ofComponents (fun Y => ?_) (fun _ => ?_)
    · exact ((limit.isLimit _).conePointUniqueUpToIso (binaryProductLimit X Y)).symm
    · apply Limits.prod.hom_ext <;> simp <;> rfl

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.Small

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q
hQ : P ≤ Q.isoClosure
P' : ObjectProperty C := Q ⊓ P.isoClosure
h : ∀ (X' : Subtype P'), ∃ X, Nonempty (↑X' ≅ ↑X)
⊢ ∃ Q, ∃ (_ : ObjectProperty.Small.{w, v, u} Q), Q ≤ P ∧ P ≤ Q.isoClosure

Tactic:
choose φ hφ using h

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q
hQ : P ≤ Q.isoClosure
P' : ObjectProperty C := Q ⊓ P.isoClosure
φ : Subtype P' → Subtype P
hφ : ∀ (X' : Subtype P'), Nonempty (↑X' ≅ ↑(φ X'))
⊢ ∃ Q, ∃ (_ : ObjectProperty.Small.{w, v, u} Q), Q ≤ P ∧ P ≤ Q.isoClosure
Module: Mathlib.CategoryTheory.ObjectProperty.Small

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q
hQ : P ≤ Q.isoClosure
P' : ObjectProperty C := Q ⊓ P.isoClosure
φ : Subtype P' → Subtype P
hφ : ∀ (X' : Subtype P'), Nonempty (↑X' ≅ ↑(φ X'))
Y : C
hY : P' Y
⊢ P ↑(φ ⟨Y, hY⟩)

Tactic:
exact (φ ⟨Y, hY⟩).2

Goal state after:
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F F₁ F₂ : C ⥤ Type w
α : F₁ ⟶ F₂
t₁ t₂ : F₁.Elements
k : t₁ ⟶ t₂
⊢ (ConcreteCategory.hom (F₂.map ↑k)) ⟨t₁.fst, (ConcreteCategory.hom (α.app t₁.fst)) t₁.snd⟩.snd =
    ⟨t₂.fst, (ConcreteCategory.hom (α.app t₂.fst)) t₂.snd⟩.snd

Tactic:
simpa [map_snd] using (NatTrans.naturality_apply α k.1 t₁.2).symm

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 : CostructuredArrow yoneda F
⊢ yoneda.map (Iso.refl (((fromCostructuredArrow F).rightOp ⋙ toCostructuredArrow F).obj X).left).hom ≫
      ((𝟭 (CostructuredArrow yoneda F)).obj X).hom =
    (((fromCostructuredArrow F).rightOp ⋙ toCostructuredArrow F).obj X).hom

Tactic:
dsimp
    simpa only [Functor.map_id, Category.id_comp] using!
      (yonedaEquiv.symm_apply_apply X.hom).symm

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
d : ↑(F.obj X)
⊢ G.map { base := 𝟙 X, fiber := 𝟙 ((F.map (𝟙 X)).toFunctor.obj d) } ≫
      colimit.ι (Grothendieck.ι F X ⋙ G) ((F.map (𝟙 X)).toFunctor.obj d) =
    eqToHom ⋯ ≫ colimit.ι (Grothendieck.ι F X ⋙ G) ((F.map (𝟙 X)).toFunctor.obj d)

Tactic:
← eqToHom_map G (by simp),

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝¹ : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
X : C
d : ↑(F.obj X)
⊢ G.map { base := 𝟙 X, fiber := 𝟙 ((F.map (𝟙 X)).toFunctor.obj d) } ≫
      colimit.ι (Grothendieck.ι F X ⋙ G) ((F.map (𝟙 X)).toFunctor.obj d) =
    G.map (eqToHom ⋯) ≫ colimit.ι (Grothendieck.ι F X ⋙ G) ((F.map (𝟙 X)).toFunctor.obj d)
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) } ≫
            { base := g,
              fiber := 𝟙 ((F.map g).toFunctor.obj ((Grothendieck.ι F Y).obj ((F.map f).toFunctor.obj d)).fiber) }) ≫
        eqToHom ⋯) ≫
      colimit.ι (Grothendieck.ι F Z ⋙ G) ((F.map (f ≫ g)).toFunctor.obj d)

Tactic:
← eqToHom_map G (by simp),

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝¹ : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
X 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) }) ≫
        G.map (eqToHom ⋯)) ≫
      colimit.ι (Grothendieck.ι F Z ⋙ G) ((F.map (f ≫ g)).toFunctor.obj d)
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: case h_obj
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
⊢ ∀ (X : Grothendieck F), (map (𝟙 F)).obj X = (𝟭 (Grothendieck F)).obj X

pp: case h_map
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
⊢ autoParam
    (∀ (X Y : Grothendieck F) (f : X ⟶ Y), (map (𝟙 F)).map f = eqToHom ⋯ ≫ (𝟭 (Grothendieck F)).map f ≫ eqToHom ⋯)
    ext._auto_1

Tactic:
· intro X
    rfl

Goal state after:
case h_map
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
⊢ autoParam
    (∀ (X Y : Grothendieck F) (f : X ⟶ Y), (map (𝟙 F)).map f = eqToHom ⋯ ≫ (𝟭 (Grothendieck F)).map f ≫ eqToHom ⋯)
    ext._auto_1
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: case h_obj
C : Type u
inst✝ : Category.{v, u} C
F G H : C ⥤ Cat
α : F ⟶ G
β : G ⟶ H
⊢ ∀ (X : Grothendieck F), (map (α ≫ β)).obj X = (map α ⋙ map β).obj X

pp: case h_map
C : Type u
inst✝ : Category.{v, u} C
F G H : C ⥤ Cat
α : F ⟶ G
β : G ⟶ H
⊢ autoParam (∀ (X Y : Grothendieck F) (f : X ⟶ Y), (map (α ≫ β)).map f = eqToHom ⋯ ≫ (map α ⋙ map β).map f ≫ eqToHom ⋯)
    ext._auto_1

Tactic:
· intro X
    rfl

Goal state after:
case h_map
C : Type u
inst✝ : Category.{v, u} C
F G H : C ⥤ Cat
α : F ⟶ G
β : G ⟶ H
⊢ autoParam (∀ (X Y : Grothendieck F) (f : X ⟶ Y), (map (α ≫ β)).map f = eqToHom ⋯ ≫ (map α ⋙ map β).map f ≫ eqToHom ⋯)
    ext._auto_1
Module: Mathlib.CategoryTheory.Limits.Connected

Goal state before:
pp: case h.zero
p : Set WalkingParallelPair
a✝ : ?j₀ ∈ p
t : ∀ {j₁ j₂ : WalkingParallelPair} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
⊢ WalkingParallelPair.zero ∈ p

Tactic:
rwa [t WalkingParallelPairHom.left]

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
d : D
Z : (X : C) → (F.obj X ⟶ d) → Sort u_1
h₁ : (X₁ X₂ : C) → (k₁ : F.obj X₁ ⟶ d) → (k₂ : F.obj X₂ ⟶ d) → (f : X₁ ⟶ X₂) → F.map f ≫ k₂ = k₁ → Z X₁ k₁ → Z X₂ k₂
h₂ : (X₁ X₂ : C) → (k₁ : F.obj X₁ ⟶ d) → (k₂ : F.obj X₂ ⟶ d) → (f : X₁ ⟶ X₂) → F.map f ≫ k₂ = k₁ → Z X₂ k₂ → Z X₁ k₁
X₀ : C
k₀ : F.obj X₀ ⟶ d
z : Z X₀ k₀
j₁ j₂ : CostructuredArrow F d
f : j₁ ⟶ j₂
a : Z j₁.left j₁.hom
⊢ Z j₂.left j₂.hom

Tactic:
fapply h₁ _ _ _ _ f.left _ a

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
d : D
Z : (X : C) → (F.obj X ⟶ d) → Sort u_1
h₁ : (X₁ X₂ : C) → (k₁ : F.obj X₁ ⟶ d) → (k₂ : F.obj X₂ ⟶ d) → (f : X₁ ⟶ X₂) → F.map f ≫ k₂ = k₁ → Z X₁ k₁ → Z X₂ k₂
h₂ : (X₁ X₂ : C) → (k₁ : F.obj X₁ ⟶ d) → (k₂ : F.obj X₂ ⟶ d) → (f : X₁ ⟶ X₂) → F.map f ≫ k₂ = k₁ → Z X₂ k₂ → Z X₁ k₁
X₀ : C
k₀ : F.obj X₀ ⟶ d
z : Z X₀ k₀
j₁ j₂ : CostructuredArrow F d
f : j₁ ⟶ j₂
a : Z j₁.left j₁.hom
⊢ F.map f.left ≫ j₂.hom = j₁.hom
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 : D ⥤ Cat
G : C ⥤ D
hG : G.Final
d : D
f : ↑(F.obj d)
u : Discrete PUnit.{1}
c : C
g : (fromPUnit d).obj u ⟶ G.obj c
this : Nonempty (StructuredArrow { base := d, fiber := f } (pre F G)) := ⋯
bi : C
fi : ↑(F.obj (G.obj bi))
gbi : d ⟶ G.obj bi
gfi : (F.map gbi).toFunctor.obj f ⟶ fi
bj : C
fj : ↑(F.obj (G.obj bj))
gbj : d ⟶ G.obj bj
gfj : (F.map gbj).toFunctor.obj f ⟶ fj
⊢ Zigzag (StructuredArrow.mk { base := gbi, fiber := 𝟙 ((F.map gbi).toFunctor.obj { base := d, fiber := f }.fiber) })
    { left := { as := PUnit.unit }, right := { base := bj, fiber := fj }, hom := { base := gbj, fiber := gfj } }

Tactic:
refine Zigzag.trans (j₂ := StructuredArrow.mk (Y := ⟨bj, ((F.map gbj).toFunctor.obj f)⟩)
      (Grothendieck.Hom.mk gbj (𝟙 _))) ?_
    (.of_zag (.inl ⟨StructuredArrow.homMk (Grothendieck.Hom.mk (by dsimp; exact 𝟙 _)
      (eqToHom (by simp) ≫ gfj)) (by apply Grothendieck.ext <;> simp)⟩))

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ Cat
G : C ⥤ D
hG : G.Final
d : D
f : ↑(F.obj d)
u : Discrete PUnit.{1}
c : C
g : (fromPUnit d).obj u ⟶ G.obj c
this : Nonempty (StructuredArrow { base := d, fiber := f } (pre F G)) :=
  Nonempty.intro
    { left := u, right := { base := c, fiber := (F.map g).toFunctor.obj f },
      hom := { base := g, fiber := 𝟙 ((F.map g).toFunctor.obj ((fromPUnit { base := d, fiber := f }).obj u).fiber) } }
bi : C
fi : ↑(F.obj (G.obj bi))
gbi : d ⟶ G.obj bi
gfi : (F.map gbi).toFunctor.obj f ⟶ fi
bj : C
fj : ↑(F.obj (G.obj bj))
gbj : d ⟶ G.obj bj
gfj : (F.map gbj).toFunctor.obj f ⟶ fj
⊢ Zigzag (StructuredArrow.mk { base := gbi, fiber := 𝟙 ((F.map gbi).toFunctor.obj { base := d, fiber := f }.fiber) })
    (StructuredArrow.mk { base := gbj, fiber := 𝟙 ((F.map gbj).toFunctor.obj { base := d, fiber := f }.fiber) })
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ P.IsStableUnderBaseChange → P.pullbacks ≤ P

Tactic:
intro h _ _ _ ⟨_, _, _, _, _, h₁, h₂⟩

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.IsStableUnderBaseChange
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
w✝⁴ w✝³ : C
w✝² : w✝⁴ ⟶ w✝³
w✝¹ : X✝ ⟶ w✝⁴
w✝ : Y✝ ⟶ w✝³
h₁ : P w✝²
h₂ : IsPullback w✝¹ f✝ w✝² w✝
⊢ P f✝
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ P.IsStableUnderCobaseChange → P.pushouts ≤ P

Tactic:
intro h _ _ _ ⟨_, _, _, _, _, h₁, h₂⟩

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.IsStableUnderCobaseChange
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
w✝⁴ w✝³ : C
w✝² : w✝⁴ ⟶ w✝³
w✝¹ : w✝⁴ ⟶ X✝
w✝ : w✝³ ⟶ Y✝
h₁ : P w✝²
h₂ : IsPushout w✝¹ w✝² f✝ w✝
⊢ P f✝
Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape

Goal state before:
pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : ObjectProperty C
J : Type u'
inst✝ : Category.{v', u'} J
X : C
x✝ : (P.op.colimitsOfShape Jᵒᵖ).unop X
h : P.op.ColimitOfShape Jᵒᵖ (Opposite.op X)
⊢ P.LimitOfShape J X

Tactic:
exact
      { diag := h.diag.unop
        π := NatTrans.unop h.ι
        isLimit := isLimitOfOp h.isColimit
        prop_diag_obj _ := h.prop_diag_obj _ }

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
f₁ f₂ f₃ : X ⟶ M
⊢ lift (lift f₁ f₂ ≫ μ) f₃ ≫ μ = lift (lift f₁ f₂) f₃ ≫ μ ▷ M ≫ μ

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
f₁ f₂ f₃ : X ⟶ M
⊢ lift (lift f₁ f₂) f₃ ≫ μ ▷ M ≫ μ = lift f₁ (lift f₂ f₃ ≫ μ) ≫ μ

Tactic:
· rw [← tensorHom_id, lift_map_assoc, Category.comp_id]

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
f₁ f₂ f₃ : X ⟶ M
⊢ lift (lift f₁ f₂) f₃ ≫ μ ▷ M ≫ μ = lift f₁ (lift f₂ f₃ ≫ μ) ≫ μ