mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case refine_1
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
⊢ Surjective ⇑(MvPolynomial.aeval (⇑f ∘ MvPolynomial.X))

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
⊢ (RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X)).toRingHom).FG

Tactic:
·

Goal state after:
case refine_1
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
⊢ Surjective ⇑(MvPolynomial.aeval (⇑f ∘ MvPolynomial.X))
Module: Mathlib.CategoryTheory.ObjectProperty.Small

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
inst✝ : LocallySmall.{w', v, u} C
x✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
⊢ ∃ J x, Nonempty (P.FullSubcategory ≌ J)

Tactic:
·

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
inst✝ : LocallySmall.{w', v, u} C
x✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
⊢ ∃ J x, Nonempty (P.FullSubcategory ≌ J)
Module: Mathlib.CategoryTheory.MorphismProperty.Comma

Goal state before:
pp: A : Type u_1
inst✝⁶ : Category.{v_1, u_1} A
B : Type u_2
inst✝⁵ : Category.{v_2, u_2} B
T : Type u_3
inst✝⁴ : Category.{v_3, u_3} T
L : A ⥤ T
R : B ⥤ T
P : MorphismProperty T
Q : MorphismProperty A
W : MorphismProperty B
inst✝³ : Q.IsMultiplicative
inst✝² : W.IsMultiplicative
inst✝¹ : Q.RespectsIso
inst✝ : W.RespectsIso
A✝ B✝ : MorphismProperty.Comma L R P Q W
f : A✝ ⟶ B✝
hf : IsIso (Hom.hom f)
⊢ IsIso f

Tactic:
← hom_homFromCommaOfIsIso f

Goal state after:
A : Type u_1
inst✝⁶ : Category.{v_1, u_1} A
B : Type u_2
inst✝⁵ : Category.{v_2, u_2} B
T : Type u_3
inst✝⁴ : Category.{v_3, u_3} T
L : A ⥤ T
R : B ⥤ T
P : MorphismProperty T
Q : MorphismProperty A
W : MorphismProperty B
inst✝³ : Q.IsMultiplicative
inst✝² : W.IsMultiplicative
inst✝¹ : Q.RespectsIso
inst✝ : W.RespectsIso
A✝ B✝ : MorphismProperty.Comma L R P Q W
f : A✝ ⟶ B✝
hf : IsIso (Hom.hom f)
⊢ IsIso (homFromCommaOfIsIso (Hom.hom f))
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
⊢ (RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X)).toRingHom).FG

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
⊢ (RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X)).toRingHom).FG
Module: Mathlib.CategoryTheory.ObjectProperty.Small

Goal state before:
pp: case inr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
this :
  ∀ {C : Type u_1} [inst : Category.{v_1, u_1} C],
    LocallySmall.{w, v_1, u_1} C →
      (EssentiallySmall.{w, v_1, u_1} C ↔
        LocallySmall.{w, v_1, u_1} C ∧ ObjectProperty.EssentiallySmall.{w, v_1, u_1} ⊤)
hC : ¬LocallySmall.{w, v_1, u_1} C
⊢ EssentiallySmall.{w, v_1, u_1} C ↔ LocallySmall.{w, v_1, u_1} C ∧ ObjectProperty.EssentiallySmall.{w, v_1, u_1} ⊤

pp: C✝ : Type u_1
inst✝¹ : Category.{v_1, u_1} C✝
C : Type u_1
inst✝ : Category.{v_1, u_1} C
hC : LocallySmall.{w, v_1, u_1} C
⊢ EssentiallySmall.{w, v_1, u_1} C ↔ LocallySmall.{w, v_1, u_1} C ∧ ObjectProperty.EssentiallySmall.{w, v_1, u_1} ⊤

Tactic:
·

Goal state after:
case inr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
this :
  ∀ {C : Type u_1} [inst : Category.{v_1, u_1} C],
    LocallySmall.{w, v_1, u_1} C →
      (EssentiallySmall.{w, v_1, u_1} C ↔
        LocallySmall.{w, v_1, u_1} C ∧ ObjectProperty.EssentiallySmall.{w, v_1, u_1} ⊤)
hC : ¬LocallySmall.{w, v_1, u_1} C
⊢ EssentiallySmall.{w, v_1, u_1} C ↔ LocallySmall.{w, v_1, u_1} C ∧ ObjectProperty.EssentiallySmall.{w, v_1, u_1} ⊤
Module: Mathlib.CategoryTheory.MorphismProperty.Comma

Goal state before:
pp: case h₁
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
⊢ (Comma.Hom.hom f).left = (Comma.Hom.hom g).left

pp: case h₂
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
⊢ (Comma.Hom.hom f).right = (Comma.Hom.hom g).right

Tactic:
·

Goal state after:
case h₁
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
⊢ (Comma.Hom.hom f).left = (Comma.Hom.hom g).left
Module: Mathlib.CategoryTheory.MorphismProperty.Comma

Goal state before:
pp: case h₂
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
⊢ (Comma.Hom.hom f).right = (Comma.Hom.hom g).right

Tactic:
·

Goal state after:
case h₂
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
⊢ (Comma.Hom.hom f).right = (Comma.Hom.hom g).right
Module: Mathlib.CategoryTheory.MorphismProperty.Comma

Goal state before:
pp: case h₁
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
⊢ (Comma.Hom.hom f).left = (Comma.Hom.hom g).left

pp: case h₂
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
⊢ (Comma.Hom.hom f).right = (Comma.Hom.hom g).right

Tactic:
·

Goal state after:
case h₁
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
⊢ (Comma.Hom.hom f).left = (Comma.Hom.hom g).left
Module: Mathlib.CategoryTheory.MorphismProperty.Comma

Goal state before:
pp: case h₂
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
⊢ (Comma.Hom.hom f).right = (Comma.Hom.hom g).right

Tactic:
·

Goal state after:
case h₂
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
⊢ (Comma.Hom.hom f).right = (Comma.Hom.hom g).right
Module: Mathlib.CategoryTheory.MorphismProperty.Comma

Goal state before:
pp: case h₁
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
⊢ (Comma.Hom.hom f).left = (Comma.Hom.hom g).left

pp: case h₂
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
⊢ (Comma.Hom.hom f).right = (Comma.Hom.hom g).right

Tactic:
·

Goal state after:
case h₁
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
⊢ (Comma.Hom.hom f).left = (Comma.Hom.hom g).left
Module: Mathlib.CategoryTheory.MorphismProperty.Comma

Goal state before:
pp: case h₂
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
⊢ (Comma.Hom.hom f).right = (Comma.Hom.hom g).right

Tactic:
·

Goal state after:
case h₂
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
⊢ (Comma.Hom.hom f).right = (Comma.Hom.hom g).right
Module: Mathlib.CategoryTheory.MorphismProperty.Comma

Goal state before:
pp: case refine_1
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
A B : P.CostructuredArrow ⊤ F X
f : (CostructuredArrow.toOver P F X).obj A ⟶ (CostructuredArrow.toOver P F X).obj B
⊢ F.map (F.preimage f.left) ≫ B.hom = A.hom

pp: case refine_2
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
A B : P.CostructuredArrow ⊤ F X
f : (CostructuredArrow.toOver P F X).obj A ⟶ (CostructuredArrow.toOver P F X).obj B
⊢ (CostructuredArrow.toOver P F X).map (CostructuredArrow.homMk (F.preimage f.left) trivial ?refine_1) = f

Tactic:
·

Goal state after:
case refine_1
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
A B : P.CostructuredArrow ⊤ F X
f : (CostructuredArrow.toOver P F X).obj A ⟶ (CostructuredArrow.toOver P F X).obj B
⊢ F.map (F.preimage f.left) ≫ B.hom = A.hom
Module: Mathlib.CategoryTheory.MorphismProperty.Comma

Goal state before:
pp: case refine_2
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
A B : P.CostructuredArrow ⊤ F X
f : (CostructuredArrow.toOver P F X).obj A ⟶ (CostructuredArrow.toOver P F X).obj B
⊢ (CostructuredArrow.toOver P F X).map (CostructuredArrow.homMk (F.preimage f.left) trivial ⋯) = f

Tactic:
·

Goal state after:
case refine_2
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
A B : P.CostructuredArrow ⊤ F X
f : (CostructuredArrow.toOver P F X).obj A ⟶ (CostructuredArrow.toOver P F X).obj B
⊢ (CostructuredArrow.toOver P F X).map (CostructuredArrow.homMk (F.preimage f.left) trivial ⋯) = f
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.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
  cases x
  cases y
  cases h₁
  simp_all

Goal state after:
Module: Mathlib.CategoryTheory.Elements

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

pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
A✝ B✝ : F.Elements
f : A✝ ⟶ B✝
h : IsIso ((π F).map f)
⊢ f ≫ ⟨inv ((π F).map f), ?refine_1⟩ = 𝟙 A✝

pp: case refine_3
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
A✝ B✝ : F.Elements
f : A✝ ⟶ B✝
h : IsIso ((π F).map f)
⊢ ⟨inv ((π F).map f), ?refine_1⟩ ≫ f = 𝟙 B✝

Tactic:
·

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
A✝ B✝ : F.Elements
f : A✝ ⟶ B✝
h : IsIso ((π F).map f)
⊢ (ConcreteCategory.hom (F.map (inv ((π F).map f)))) B✝.snd = A✝.snd
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
A✝ B✝ : F.Elements
f : A✝ ⟶ B✝
h : IsIso ((π F).map f)
⊢ f ≫ ⟨inv ((π F).map f), ⋯⟩ = 𝟙 A✝

pp: case refine_3
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
A✝ B✝ : F.Elements
f : A✝ ⟶ B✝
h : IsIso ((π F).map f)
⊢ ⟨inv ((π F).map f), ⋯⟩ ≫ f = 𝟙 B✝

Tactic:
·

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
A✝ B✝ : F.Elements
f : A✝ ⟶ B✝
h : IsIso ((π F).map f)
⊢ f ≫ ⟨inv ((π F).map f), ⋯⟩ = 𝟙 A✝
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: case refine_3
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
A✝ B✝ : F.Elements
f : A✝ ⟶ B✝
h : IsIso ((π F).map f)
⊢ ⟨inv ((π F).map f), ⋯⟩ ≫ f = 𝟙 B✝

Tactic:
·

Goal state after:
case refine_3
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
A✝ B✝ : F.Elements
f : A✝ ⟶ B✝
h : IsIso ((π F).map f)
⊢ ⟨inv ((π F).map f), ⋯⟩ ≫ f = 𝟙 B✝
Module: Mathlib.CategoryTheory.Elements

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

pp: case h_map
C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : Cᵒᵖ ⥤ Type v
α : F₁ ⟶ F₂
⊢ autoParam
    (∀ (X Y : F₁.Elementsᵒᵖ) (f : X ⟶ Y),
      ((map α).op ⋙ toCostructuredArrow F₂).map f =
        eqToHom ⋯ ≫ (toCostructuredArrow F₁ ⋙ CostructuredArrow.map α).map f ≫ eqToHom ⋯)
    Functor.ext._auto_1

Tactic:
·

Goal state after:
case h_obj
C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : Cᵒᵖ ⥤ Type v
α : F₁ ⟶ F₂
⊢ ∀ (X : F₁.Elementsᵒᵖ),
    ((map α).op ⋙ toCostructuredArrow F₂).obj X = (toCostructuredArrow F₁ ⋙ CostructuredArrow.map α).obj X
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: case h_map
C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : Cᵒᵖ ⥤ Type v
α : F₁ ⟶ F₂
⊢ autoParam
    (∀ (X Y : F₁.Elementsᵒᵖ) (f : X ⟶ Y),
      ((map α).op ⋙ toCostructuredArrow F₂).map f =
        eqToHom ⋯ ≫ (toCostructuredArrow F₁ ⋙ CostructuredArrow.map α).map f ≫ eqToHom ⋯)
    Functor.ext._auto_1

Tactic:
·

Goal state after:
case h_map
C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : Cᵒᵖ ⥤ Type v
α : F₁ ⟶ F₂
⊢ autoParam
    (∀ (X Y : F₁.Elementsᵒᵖ) (f : X ⟶ Y),
      ((map α).op ⋙ toCostructuredArrow F₂).map f =
        eqToHom ⋯ ≫ (toCostructuredArrow F₁ ⋙ CostructuredArrow.map α).map f ≫ eqToHom ⋯)
    Functor.ext._auto_1
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case hy
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) := ⋯
AX : Type (max w₂ 0) := ⋯
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 := ⋯
s₀✝ : Set (MvPolynomial (Fin n) A) := ⋯
I : Ideal (MvPolynomial (Fin n) A) := ⋯
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) := ⋯
this : x✝ ∈ adjoin R (⇑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
x : A
hx : x ∈ ↑t
⊢ MvPolynomial.C x - (MvPolynomial.map (algebraMap R A)) (t' ⟨x, hx⟩) ∈ (Ideal.span s₀).toAddSubmonoid

Tactic:
·

Goal state after:
case hy
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) := ⋯
AX : Type (max w₂ 0) := ⋯
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 := ⋯
s₀✝ : Set (MvPolynomial (Fin n) A) := ⋯
I : Ideal (MvPolynomial (Fin n) A) := ⋯
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) := ⋯
this : x✝ ∈ adjoin R (⇑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X)
x : A
hx : x ∈ ↑t
⊢ MvPolynomial.C x - (MvPolynomial.map (algebraMap R A)) (t' ⟨x, hx⟩) ∈ (Ideal.span s₀).toAddSubmonoid
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: case refine_1
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
⊢ ObjectProperty.Small.{w, v, max u w} fun x ↦ P x.fst

pp: case refine_2
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
⊢ ObjectProperty.isoClosure (fun x ↦ P x.fst) y

Tactic:
·

Goal state after:
case refine_1
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
⊢ ObjectProperty.Small.{w, v, max u w} fun x ↦ P x.fst
Module: Mathlib.CategoryTheory.Elements

Goal state before:
pp: case refine_2
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
⊢ ObjectProperty.isoClosure (fun x ↦ P x.fst) y

Tactic:
·

Goal state after:
case refine_2
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
⊢ ObjectProperty.isoClosure (fun x ↦ P x.fst) y