mathlib-initiative/mathlib-tactics huggingface dataset:
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:
]

Goal state after:
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
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case inl
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 : MvPolynomial (Fin n) R
hx : x ∈ ↑s
⊢ f x = 0

Tactic:
]

Goal state after:
case inl
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 : MvPolynomial (Fin n) R
hx : x ∈ ↑s
⊢ f x = 0
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case inl
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 : MvPolynomial (Fin n) R
hx : x ∈ ↑s
this : x ∈ ↑(RingHom.ker f.toRingHom)
⊢ f x = 0

Tactic:
]

Goal state after:
case inl
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 : MvPolynomial (Fin n) R
hx : x ∈ ↑s
this : x ∈ ↑(RingHom.ker f.toRingHom)
⊢ f x = 0
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
⊢ 0 = 0

Tactic:
]

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
⊢ x.snd = x.snd

Tactic:
]

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))) q.snd

Tactic:
]

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 ≫ Groupoid.inv ↑f))) p.snd = p.snd

Tactic:
]

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

Goal state before:
pp: case refine_2
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))
leI :
  Ideal.span (⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) A
hx : (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X)) x = 0
⊢ x ∈ Ideal.span (⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g)

Tactic:
]

Goal state after:
case refine_2
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))
leI :
  Ideal.span (⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) A
hx : (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X)) x = 0
⊢ x ∈ Ideal.span (⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g)
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))
leI :
  Ideal.span (⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) A
hx : (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X)) x = 0
s₀ : Set (MvPolynomial (Fin n) A) := ⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
this : x ∈ adjoin R (⇑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
⊢ x ∈ (MvPolynomial.map (algebraMap R A)).range.toAddSubmonoid ⊔ (Ideal.span s₀).toAddSubmonoid

Tactic:
]

Goal state after:
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))
leI :
  Ideal.span (⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X))
x : MvPolynomial (Fin n) A
hx : (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X)) x = 0
s₀ : Set (MvPolynomial (Fin n) A) := ⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
this : x ∈ adjoin R (⇑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
⊢ x ∈ (MvPolynomial.map (algebraMap R A)).range.toAddSubmonoid ⊔ (Ideal.span s₀).toAddSubmonoid
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✝
⊢ uliftYonedaEquiv.symm (unop X✝).snd = uliftYonedaEquiv.symm (unop X✝).snd

Tactic:
]

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✝
⊢ uliftYonedaEquiv (uliftYoneda.{w, v, u}.map f.left ≫ Y✝.hom) =
    uliftYonedaEquiv (uliftYoneda.{w, v, u}.map f.left ≫ Y✝.hom)

Tactic:
]

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
⊢ ObjectProperty.EssentiallySmall.{w, v, max u w} ⊤

Tactic:
]

Goal state after:
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
⊢ ObjectProperty.EssentiallySmall.{w, v, max u w} ⊤
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) =
    G.map { base := eqToHom ⋯, fiber := eqToHom ⋯ } ≫ colimit.ι (Grothendieck.ι F X ⋙ G) ((F.map (𝟙 X)).toFunctor.obj d)

Tactic:
]

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

Tactic:
]

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

Tactic:
]

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) }) ≫
          { base := eqToHom ⋯, fiber := eqToHom ⋯ }) ≫
      colimit.ι (Grothendieck.ι F Z ⋙ G) ((F.map (f ≫ g)).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✝¹ x✝ : Grothendieck F
f : x✝¹ ⟶ x✝
⊢ G.map f ≫ colimit.ι (Grothendieck.ι F x✝.base ⋙ G) x✝.fiber =
    G.map ((Grothendieck.ιNatTrans f.base).app x✝¹.fiber) ≫
      (Grothendieck.ι F x✝.base ⋙ G).map f.fiber ≫ colimit.ι (Grothendieck.ι F x✝.base ⋙ G) x✝.fiber

Tactic:
]

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✝¹ x✝ : Grothendieck F
f : x✝¹ ⟶ x✝
⊢ G.map f ≫ colimit.ι (Grothendieck.ι F x✝.base ⋙ G) x✝.fiber =
    G.map ((Grothendieck.ιNatTrans f.base).app x✝¹.fiber) ≫
      (Grothendieck.ι F x✝.base ⋙ G).map f.fiber ≫ colimit.ι (Grothendieck.ι F x✝.base ⋙ G) x✝.fiber
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 g.base).toFunctor.obj X.fiber

Tactic:
]

Goal state after:
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 ⋯ ≫
      eqToHom ⋯ ≫
        ((Cat.Hom.toNatIso (eqToIso ⋯) ≪≫ eqToIso ⋯).hom.app ((F.map f.base).toFunctor.obj X.fiber) ≫
            (𝟭 ↑(F.obj Y.base)).map f.fiber ≫ (Cat.Hom.toNatIso (eqToIso ⋯) ≪≫ eqToIso ⋯).inv.app Y.fiber) ≫
          eqToHom ⋯ =
    f.fiber

Tactic:
]

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 ⋯ ≫
        ((Cat.Hom.toNatIso (eqToIso ⋯) ≪≫ eqToIso ⋯).hom.app ((F.map f.base).toFunctor.obj X.fiber) ≫
            (𝟭 ↑(F.obj Y.base)).map f.fiber ≫ (Cat.Hom.toNatIso (eqToIso ⋯) ≪≫ eqToIso ⋯).inv.app Y.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 =
    (colimit.ι (Grothendieck.ι F X.base ⋙ G) X.fiber ≫ (fiberwiseColimit G).map f) ≫ c.ι.app Y.base

Tactic:
]

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 =
    (colimit.ι (Grothendieck.ι F X.base ⋙ G) X.fiber ≫ (fiberwiseColimit G).map f) ≫ c.ι.app Y.base