mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.MorphismProperty.Comma

Goal state before:
pp: T : Type u_1
inst✝² : Category.{v_1, u_1} T
P Q W : MorphismProperty T
inst✝¹ : Q.IsMultiplicative
inst✝ : W.IsMultiplicative
A B : P.Arrow Q W
f g : A ⟶ B
hl : f.left = g.left
hr : f.right = g.right
⊢ f = g

Tactic:
by

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:
by

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 : A ⟶ B
⊢ f.left ≫ B.hom = A.hom

Tactic:
by

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.Under Q X
f g : A ⟶ B
h : f.right = g.right
⊢ f = g

Tactic:
by

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.Under Q X
f : A ⟶ B
⊢ A.hom ≫ f.right = B.hom

Tactic:
by

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Category.{u_4, u_2} D
P : MorphismProperty D
Q : MorphismProperty C
inst✝ : Q.IsMultiplicative
F : C ⥤ D
X : D
A B : P.CostructuredArrow Q F X
f g : A ⟶ B
h : f.left = g.left
⊢ f = g

Tactic:
by

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝² : Category.{?u.5, u_1} C
inst✝¹ : Category.{?u.8, u_2} D
P : MorphismProperty D
Q : MorphismProperty C
inst✝ : Q.IsMultiplicative
F : C ⥤ D
X : D
A B : P.CostructuredArrow Q F X
f : A.left ≅ B.left
hf : Q f.hom
hf' : Q f.inv
w : F.map f.hom ≫ B.hom = A.hom
⊢ F.map f.inv ≫ A.hom = B.hom

Tactic:
by

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
P : MorphismProperty D
Q : MorphismProperty C
inst✝¹ : Q.IsMultiplicative
F : C ⥤ D
X : D
inst✝ : F.Faithful
⊢ (CostructuredArrow.toOver P F X).Faithful

Tactic:
by

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
P : MorphismProperty D
Q : MorphismProperty C
inst✝¹ : Q.IsMultiplicative
F : C ⥤ D
X : D
inst✝ : F.Full
⊢ (CostructuredArrow.toOver P F X).Full

Tactic:
by

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

Goal state before:
pp: C✝ : Type u_1
D : Type u_2
inst✝⁴ : Category.{?u.5, u_1} C✝
inst✝³ : Category.{?u.8, u_2} D
P : MorphismProperty D
Q : MorphismProperty C✝
inst✝² : Q.IsMultiplicative
F : C✝ ⥤ D
X✝ : D
C : Type u_3
inst✝¹ : Category.{v_1, u_3} C
W₁ W₂ : MorphismProperty C
inst✝ : W₁.HasFactorization W₂
S : C
X Y : Over S
f : X ⟶ Y
⊢ Nonempty (W₁.over.MapFactorizationData W₂.over f)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
x y : F.Elements
h₁ : x.fst = y.fst
h₂ : (ConcreteCategory.hom (F.map (eqToHom h₁))) x.snd = y.snd
⊢ x = y

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
p : F.Elements
⊢ (ConcreteCategory.hom (F.map (𝟙 p.fst))) p.snd = p.snd

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
X Y Z : F.Elements
f : { f // (ConcreteCategory.hom (F.map f)) X.snd = Y.snd }
g : { f // (ConcreteCategory.hom (F.map f)) Y.snd = Z.snd }
⊢ (ConcreteCategory.hom (F.map (↑f ≫ ↑g))) X.snd = Z.snd

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case inr
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✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FinitePresentation R B
inst✝ : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ⇑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker f.toRingHom
RX : Type (max w₁ 0) := MvPolynomial (Fin n) R
AX : Type (max w₂ 0) := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : ↥t → MvPolynomial (Fin n) R
ht' : ∀ (i : ↥t), f (t' i) = (algebraMap A B) ↑i
ht'' : adjoin R (⇑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : ↥t → AX := fun x ↦ MvPolynomial.C ↑x - (MvPolynomial.map (algebraMap R A)) (t' x)
s₀ : Set (MvPolynomial (Fin n) A) := ⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X))
x : A
hx : x ∈ t
⊢ (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X)) (g ⟨x, hx⟩) = 0

Tactic:
· rw [map_sub, MvPolynomial.aeval_map_algebraMap, ← aeval_unique,
          MvPolynomial.aeval_C, ht', Subtype.coe_mk, sub_self]

Goal state after:
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Type w
φ : F ⟶ G
p q : F.Elements
x✝ : p ⟶ q
f : p.fst ⟶ q.fst
h : (ConcreteCategory.hom (F.map f)) p.snd = q.snd
⊢ (ConcreteCategory.hom (G.map f))
      (match p with
        | ⟨X, x⟩ => ⟨X, (ConcreteCategory.hom (φ.app X)) x⟩).snd =
    (match q with
      | ⟨X, x⟩ => ⟨X, (ConcreteCategory.hom (φ.app X)) x⟩).snd

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
x y : F.Elements
e : x.fst ≅ y.fst
he : (ConcreteCategory.hom (F.map e.hom)) x.snd = y.snd
⊢ (ConcreteCategory.hom (F.map e.inv)) y.snd = x.snd

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: 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✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FinitePresentation R B
inst✝ : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ⇑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker f.toRingHom
RX : Type (max w₁ 0) := MvPolynomial (Fin n) R
AX : Type (max w₂ 0) := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : ↥t → MvPolynomial (Fin n) R
ht' : ∀ (i : ↥t), f (t' i) = (algebraMap A B) ↑i
ht'' : adjoin R (⇑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : ↥t → AX := fun x ↦ MvPolynomial.C ↑x - (MvPolynomial.map (algebraMap R A)) (t' x)
s₀ : Set (MvPolynomial (Fin n) A) := ⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X))
⊢ Ideal.span (⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
F : C ⥤ Type w
X : C
snd✝ : F.obj X
Y : C
y : F.obj Y
⊢ Function.Injective fun g ↦ ↑g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
F : C ⥤ Type w
⊢ ∀ (X Y : F.Elements), Small.{w, v} (X ⟶ Y)

Tactic:
by

Goal state after:
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 (Groupoid.inv ↑f))) q.snd =
    (ConcreteCategory.hom (F.map (Groupoid.inv ↑f))) ((ConcreteCategory.hom (F.map ↑f)) p.snd)

Tactic:
by

Goal state after:
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:
by

Goal state after:
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
X✝ Y✝ : F.Elements
x✝ : X✝ ⟶ Y✝
⊢ ⟨Groupoid.inv ↑x✝, ⋯⟩ ≫ x✝ = 𝟙 Y✝

Tactic:
by

Goal state after:
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
X✝ Y✝ : F.Elements
x✝ : X✝ ⟶ Y✝
⊢ x✝ ≫ ⟨Groupoid.inv ↑x✝, ⋯⟩ = 𝟙 X✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
A✝ B✝ : F.Elements
f : A✝ ⟶ B✝
h : IsIso ((π F).map f)
⊢ IsIso f

Tactic:
by

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:
by

Goal state after:
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
X Y : F.Elements
f : X ⟶ Y
⊢ (StructuredArrow.mk (↾fun x ↦ X.snd)).hom ≫ F.map ↑f = (StructuredArrow.mk (↾fun x ↦ Y.snd)).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
X✝ Y✝ : StructuredArrow PUnit.{w + 1} F
f : X✝ ⟶ Y✝
⊢ (ConcreteCategory.hom (F.map (StructuredArrow.Hom.right f)))
      (F.elementsMk X✝.right ((ConcreteCategory.hom X✝.hom) PUnit.unit)).snd =
    (F.elementsMk Y✝.right ((ConcreteCategory.hom Y✝.hom) PUnit.unit)).snd

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
X Y : StructuredArrow PUnit.{w + 1} F
f : X ⟶ Y
⊢ (ConcreteCategory.hom (F.map (StructuredArrow.Hom.right f))) ((fromStructuredArrow F).obj X).snd =
    ((fromStructuredArrow F).obj Y).snd

Tactic:
by

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 : X✝ ⟶ Y✝
⊢ yoneda.map (↑f.unop).unop ≫ (CostructuredArrow.mk (yonedaEquiv.symm (unop Y✝).snd)).hom =
    (CostructuredArrow.mk (yonedaEquiv.symm (unop X✝).snd)).hom

Tactic:
by

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 : (CostructuredArrow yoneda F)ᵒᵖ
f : X ⟶ Y
⊢ (ConcreteCategory.hom (F.map f.unop.left.op)) ⟨op (unop X).left, yonedaEquiv.toFun (unop X).hom⟩.snd =
    ⟨op (unop Y).left, yonedaEquiv.toFun (unop Y).hom⟩.snd

Tactic:
by

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 : F.Elementsᵒᵖ
⊢ (ConcreteCategory.hom (F.map (Iso.refl ((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj X))).fst).hom))
      ((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj X))).snd =
    (unop X).snd

Tactic:
by

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).unop =
    ((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)).unop

Tactic:
by

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 : X ⟶ Y),
    (𝟭 F.Elementsᵒᵖ).map f ≫
        (isoMk ((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj Y))) (unop Y)
              (Iso.refl ((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj Y))).fst) ⋯).op.hom =
      (isoMk ((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj X))) (unop X)
              (Iso.refl ((fromCostructuredArrow F).obj (op ((toCostructuredArrow F).obj X))).fst) ⋯).op.hom ≫
        (toCostructuredArrow F ⋙ (fromCostructuredArrow F).rightOp).map f

Tactic:
by

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:
by

Goal state after:
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : Cᵒᵖ ⥤ Type v
α : F₁ ⟶ F₂
⊢ (map α).op ⋙ toCostructuredArrow F₂ = toCostructuredArrow F₁ ⋙ CostructuredArrow.map α

Tactic:
by

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 (max w v)
X✝ Y✝ : F.Elementsᵒᵖ
f : X✝ ⟶ Y✝
⊢ uliftYoneda.{w, v, u}.map (↑(unop f)).unop ≫ (CostructuredArrow.mk (uliftYonedaEquiv.symm (unop Y✝).snd)).hom =
    (CostructuredArrow.mk (uliftYonedaEquiv.symm (unop X✝).snd)).hom

Tactic:
by

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 (max w v)
X✝ Y✝ : CostructuredArrow uliftYoneda.{w, v, u} F
f : X✝ ⟶ Y✝
⊢ (ConcreteCategory.hom (F.map f.left.op)) (F.elementsMk (op Y✝.left) (uliftYonedaEquiv Y✝.hom)).snd =
    (F.elementsMk (op X✝.left) (uliftYonedaEquiv X✝.hom)).snd

Tactic:
by

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 (max w v)
x : F.Elementsᵒᵖ
⊢ (ConcreteCategory.hom
        (F.map
          (Iso.refl
              (F.elementsMk
                  (op
                    ({ obj := fun x ↦ CostructuredArrow.mk (uliftYonedaEquiv.symm (unop x).snd),
                            map := fun {X Y} f ↦ CostructuredArrow.homMk (↑(unop f)).unop ⋯, map_id := ⋯,
                            map_comp := ⋯ }.obj
                        x).left)
                  (uliftYonedaEquiv
                    ({ obj := fun x ↦ CostructuredArrow.mk (uliftYonedaEquiv.symm (unop x).snd),
                            map := fun {X Y} f ↦ CostructuredArrow.homMk (↑(unop f)).unop ⋯, map_id := ⋯,
                            map_comp := ⋯ }.obj
                        x).hom)).fst).hom))
      (F.elementsMk
          (op
            ({ obj := fun x ↦ CostructuredArrow.mk (uliftYonedaEquiv.symm (unop x).snd),
                    map := fun {X Y} f ↦ CostructuredArrow.homMk (↑(unop f)).unop ⋯, map_id := ⋯, map_comp := ⋯ }.obj
                x).left)
          (uliftYonedaEquiv
            ({ obj := fun x ↦ CostructuredArrow.mk (uliftYonedaEquiv.symm (unop x).snd),
                    map := fun {X Y} f ↦ CostructuredArrow.homMk (↑(unop f)).unop ⋯, map_id := ⋯, map_comp := ⋯ }.obj
                x).hom)).snd =
    (unop x).snd

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type u_1
X : C
h : F.RepresentableBy X
Y : F.Elements
⊢ (ConcreteCategory.hom (F.map (h.homEquiv.symm Y.snd).op)) (initialOfRepresentableBy h).snd = Y.snd

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type u_1
X : C
h : F.RepresentableBy X
Y : F.Elements
m : initialOfRepresentableBy h ⟶ Y
⊢ m = ⟨(h.homEquiv.symm Y.snd).op, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type u_1
X : C
h : F.CorepresentableBy X
Y : F.Elements
⊢ (ConcreteCategory.hom (F.map (h.homEquiv.symm Y.snd))) (initialOfCorepresentableBy h).snd = Y.snd

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type u_1
X : C
h : F.CorepresentableBy X
Y : F.Elements
m : initialOfCorepresentableBy h ⟶ Y
⊢ m = ⟨h.homEquiv.symm Y.snd, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C✝ : Type u
inst✝² : Category.{v, u} C✝
C : Type u
inst✝¹ : Category.{v, u} C
F : C ⥤ Type w
inst✝ : EssentiallySmall.{w, v, u} C
P : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} P
hP : ⊤ ≤ P.isoClosure
y : F.Elements
x✝ : ⊤ y
⊢ ⊤ y.fst

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: C✝ : Type u
inst✝² : Category.{v, u} C✝
C : Type u
inst✝¹ : Category.{v, u} C
F : C ⥤ Type w
inst✝ : EssentiallySmall.{w, v, u} C
⊢ EssentiallySmall.{w, v, max u w} F.Elements

Tactic:
by

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)
⊢ (F.map (𝟙 X)).toFunctor.obj d = d

Tactic:
by

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)
⊢ (Grothendieck.ι F X).obj d = (Grothendieck.ι F X).obj ((F.map (𝟙 X)).toFunctor.obj d)

Tactic:
by

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:
by

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 Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
d : ↑(F.obj X)
⊢ (F.map (f ≫ g)).toFunctor.obj d = (F.map g).toFunctor.obj ((F.map f).toFunctor.obj d)

Tactic:
by

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 Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
d : ↑(F.obj X)
⊢ (Grothendieck.ι F Z).obj ((F.map g).toFunctor.obj ((F.map f).toFunctor.obj d)) =
    (Grothendieck.ι F Z).obj ((F.map (f ≫ g)).toFunctor.obj d)

Tactic:
by

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 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:
by

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)
inst✝ : ∀ (c : C), HasColimitsOfShape (↑(F.obj c)) H
X✝ Y✝ : Grothendieck F ⥤ H
α : X✝ ⟶ Y✝
c₁ c₂ : C
f : c₁ ⟶ c₂
⊢ (fiberwiseColimit X✝).map f ≫ colim.map ((Grothendieck.ι F c₂).whiskerLeft α) =
    colim.map ((Grothendieck.ι F c₁).whiskerLeft α) ≫ (fiberwiseColimit Y✝).map f

Tactic:
by

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✝)
inst✝ : ∀ (c : C), HasColimitsOfShape (↑(F.obj c)) H
G : Grothendieck F ⥤ H
⊢ { app := fun c ↦ colim.map ((Grothendieck.ι F c).whiskerLeft (𝟙 G)), naturality := ⋯ } = 𝟙 (fiberwiseColimit G)

Tactic:
by

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)
inst✝ : ∀ (c : C), HasColimitsOfShape (↑(F.obj c)) H
X✝ Y✝ Z✝ : Grothendieck F ⥤ H
α : X✝ ⟶ Y✝
β : Y✝ ⟶ Z✝
⊢ { app := fun c ↦ colim.map ((Grothendieck.ι F c).whiskerLeft (α ≫ β)), naturality := ⋯ } =
    { app := fun c ↦ colim.map ((Grothendieck.ι F c).whiskerLeft α), naturality := ⋯ } ≫
      { app := fun c ↦ colim.map ((Grothendieck.ι F c).whiskerLeft β), naturality := ⋯ }

Tactic:
by

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
X Y : Grothendieck F
f g : X.Hom Y
w_base : f.base = g.base
⊢ (F.map g.base).toFunctor.obj X.fiber = (F.map f.base).toFunctor.obj X.fiber

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Cat
X Y : Grothendieck F
f g : X.Hom Y
w_base : f.base = g.base
w_fiber : eqToHom ⋯ ≫ f.fiber = g.fiber
⊢ f = g

Tactic:
by

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✝¹ x✝ : Grothendieck F
f : x✝¹ ⟶ x✝
⊢ G.map f ≫ colimit.ι (Grothendieck.ι F x✝.base ⋙ G) x✝.fiber =
    colimit.ι (Grothendieck.ι F x✝¹.base ⋙ G) x✝¹.fiber ≫ (Grothendieck.forget F ⋙ fiberwiseColimit G).map f

Tactic:
by

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
X : Grothendieck F
⊢ (F.map (𝟙 X.base)).toFunctor.obj X.fiber = X.fiber

Tactic:
by

Goal state after: