mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.ObjectProperty.Small

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
ι : Type u_1
X : ι → C
inst✝ : Small.{w, u_1} ι
i : ι
⊢ ofObj X (X i)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
ι : Type u_1
X : ι → C
inst✝ : Small.{w, u_1} ι
⊢ Function.Surjective fun i ↦ ⟨X i, ⋯⟩

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
X Y : C
⊢ ObjectProperty.Small.{w, v, u} (pair X Y)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
P Q : ObjectProperty C
inst✝¹ : ObjectProperty.Small.{w, v, u} P
inst✝ : ObjectProperty.Small.{w, v, u} Q
⊢ Function.Surjective fun x ↦
    match x with
    | Sum.inl x => ⟨↑x, ⋯⟩
    | Sum.inr x => ⟨↑x, ⋯⟩

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
α : Type u_1
P : α → ObjectProperty C
inst✝¹ : ∀ (a : α), ObjectProperty.Small.{w, v, u} (P a)
inst✝ : Small.{w, u_1} α
x : (a : α) × Subtype (P a)
⊢ (⨆ a, P a) ↑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✝ : FinitePresentation R A
e : A ≃ₐ[R] B
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG
⊢ ((↑e).comp f).toRingHom = (↑e.toRingEquiv).comp f.toRingHom

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
α : Type u_1
P : α → ObjectProperty C
inst✝¹ : ∀ (a : α), ObjectProperty.Small.{w, v, u} (P a)
inst✝ : Small.{w, u_1} α
x✝ : Subtype (⨆ a, P a)
x : C
hx : (⨆ a, P a) x
⊢ ∃ a, (fun x ↦ ⟨↑x.snd, ⋯⟩) a = ⟨x, hx⟩

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty Cᵒᵖ
⊢ ObjectProperty.Small.{w, v, u} P.unop ↔ ObjectProperty.Small.{w, v, u} P

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v, u} P
⊢ ObjectProperty.Small.{w, v, u} P.op

Tactic:
by

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
φ : Subtype P' → Subtype P
hφ : ∀ (X' : Subtype P'), Nonempty (↑X' ≅ ↑(φ X'))
X : Subtype P'
⊢ ↑(φ X) ∈ Set.range (Subtype.val ∘ φ)

Tactic:
by

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
φ : Subtype P' → Subtype P
hφ : ∀ (X' : Subtype P'), Nonempty (↑X' ≅ ↑(φ X'))
⊢ Function.Surjective fun X ↦ ⟨↑(φ X), ⋯⟩

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✝ : FinitePresentation R A
e : A ≃ₐ[R] B
⊢ FinitePresentation R B

Tactic:
by

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.Small.{w, v, u} Q), Q ≤ P ∧ P ≤ Q.isoClosure

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: R : Type w₁
inst✝¹ : CommRing R
ι : Type u_1
inst✝ : Finite ι
⊢ ∃ n f, Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
P : ObjectProperty C
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q
left✝ : Q ≤ P
right✝ : P ≤ Q.isoClosure
⊢ P.isoClosure ≤ Q.isoClosure

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
P : ObjectProperty C
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
⊢ ∃ Q, ∃ (_ : ObjectProperty.Small.{w, v, u} Q), P.isoClosure ≤ Q.isoClosure

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderIsomorphisms
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q
hQ₁ : Q ≤ P
hQ₂ : P ≤ Q.isoClosure
⊢ Q.isoClosure ≤ P

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderIsomorphisms
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
⊢ ∃ P₀, ∃ (_ : ObjectProperty.Small.{w, v, u} P₀), P = P₀.isoClosure

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P Q : ObjectProperty C
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} Q
h : P ≤ Q
⊢ ∃ Q, ∃ (_ : ObjectProperty.Small.{w, v, u} Q), P ≤ Q.isoClosure

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
P Q : ObjectProperty C
inst✝¹ : ObjectProperty.EssentiallySmall.{w, v, u} P
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} Q
⊢ ObjectProperty.EssentiallySmall.{w, v, u} (P ⊔ Q)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: R : Type w₁
A : Type w₂
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
I : Ideal A
h : I.FG
inst✝ : FinitePresentation R A
⊢ ∃ n f, Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
α : Type u_1
P : α → ObjectProperty C
inst✝¹ : ∀ (a : α), ObjectProperty.EssentiallySmall.{w, v, u} (P a)
inst✝ : Small.{w, u_1} α
⊢ ∃ Q, ∃ (_ : ObjectProperty.Small.{w, v, u} Q), ⨆ a, P a ≤ Q.isoClosure

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
x✝ : ObjectProperty.EssentiallySmall.{w, v, u} P.op
Q : ObjectProperty Cᵒᵖ
h₁ : ObjectProperty.Small.{w, v, u} Q
left✝ : Q ≤ P.op
h₂ : P.op ≤ Q.isoClosure
⊢ P ≤ Q.unop.isoClosure

Tactic:
by

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

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
x✝ : ObjectProperty.EssentiallySmall.{w, v, u} P.op
⊢ ObjectProperty.EssentiallySmall.{w, v, u} P

pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
x✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
⊢ ObjectProperty.EssentiallySmall.{w, v, u} P.op

Tactic:
· obtain ⟨Q, h₁, _, h₂⟩ := EssentiallySmall.exists_small_le P.op
    exact ⟨Q.unop, inferInstance, by rwa [← unop_isoClosure, ← op_monotone_iff, op_unop]⟩

Goal state after:
case refine_2
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
x✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
⊢ ObjectProperty.EssentiallySmall.{w, v, u} P.op
Module: Mathlib.CategoryTheory.ObjectProperty.Small

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
x✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
Q : ObjectProperty C
h₁ : ObjectProperty.Small.{w, v, u} Q
left✝ : Q ≤ P
h₂ : P ≤ Q.isoClosure
⊢ P.op ≤ Q.op.isoClosure

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
⊢ ObjectProperty.EssentiallySmall.{w, v, u} P.op ↔ ObjectProperty.EssentiallySmall.{w, v, u} P

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty Cᵒᵖ
⊢ ObjectProperty.EssentiallySmall.{w, v, u} P.unop ↔ ObjectProperty.EssentiallySmall.{w, v, u} P

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: R : Type w₁
A : Type w₂
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ FinitePresentation R A ↔ ∃ n I x, I.FG

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
P : ObjectProperty C
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
⊢ ObjectProperty.EssentiallySmall.{w, v, u} P.op

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
P : ObjectProperty Cᵒᵖ
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
⊢ ObjectProperty.EssentiallySmall.{w, v, u} P.unop

Tactic:
by

Goal state after:
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
W : MorphismProperty T
X✝ : T
inst✝ : W.RespectsIso
X Y : Comma L R
e : X ≅ Y
h : commaObj L R W X
⊢ commaObj L R W Y

Tactic:
commaObj_iff,

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
W : MorphismProperty T
X✝ : T
inst✝ : W.RespectsIso
X Y : Comma L R
e : X ≅ Y
h : commaObj L R W X
⊢ W Y.hom
Module: Mathlib.CategoryTheory.ObjectProperty.Small

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
P : ObjectProperty C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
⊢ EssentiallySmall.{w, v, u} P.FullSubcategory

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v, u} P
F : C ⥤ D
⊢ Function.Surjective fun X ↦ ⟨F.obj ↑X, ⋯⟩

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
P : ObjectProperty C
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
F : C ⥤ D
Q : ObjectProperty C
w✝ : ObjectProperty.Small.{w, v, u} Q
h₁ : Q ≤ P
h₂ : P ≤ Q.isoClosure
⊢ Q.isoClosure.map F ≤ (Q.strictMap F).isoClosure

Tactic:
by

Goal state after:
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
W : MorphismProperty T
X✝ : T
inst✝ : W.RespectsIso
X Y : Comma L R
e : X ≅ Y
h : commaObj L R W X
⊢ commaObj L R W Y

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
P : ObjectProperty C
inst✝ : ObjectProperty.EssentiallySmall.{w, v, u} P
F : C ⥤ D
⊢ ObjectProperty.EssentiallySmall.{w, v', u'} (P.map F)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : EssentiallySmall.{w, v, u} C
F : C ⥤ D
⊢ ObjectProperty.EssentiallySmall.{w, v', u'} F.essImage

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: R : Type w₁
A : Type w₂
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ FinitePresentation R A ↔ ∃ ι x f, Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: R : Type w₁
A : Type w₂
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FinitePresentation R A
ι : Type v
inst✝ : Finite ι
ι' : Type v
w✝ : Fintype ι'
f : MvPolynomial ι' R →ₐ[R] A
hf_surj : Surjective ⇑f
hf_ker : (RingHom.ker f.toRingHom).FG
g : MvPolynomial (ι ⊕ ι') R →ₐ[R] MvPolynomial ι A := (MvPolynomial.mapAlgHom f).comp ↑(MvPolynomial.sumAlgEquiv R ι ι')
val✝ : Fintype (ι ⊕ ι')
⊢ Fintype (ι ⊕ ι')

Tactic:
by

Goal state after:
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
X Y : MorphismProperty.Comma L R P Q W
i : X.toComma ⟶ Y.toComma
inst✝ : IsIso i
⊢ IsIso (homFromCommaOfIsIso i)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
P : ObjectProperty C
F : C ⥤ D
H₁ : ObjectProperty.EssentiallySmall.{w, v', u'} (P.map F)
H₂ : ∀ (Y : D), ObjectProperty.EssentiallySmall.{w, v, u} (P ⊓ fun x ↦ Nonempty (F.obj x ≅ Y))
⊢ ObjectProperty.EssentiallySmall.{w, v, u} P

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: R : Type w₁
A : Type w₂
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FinitePresentation R A
ι : Type v
inst✝ : Finite ι
⊢ FinitePresentation R (MvPolynomial ι A)

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 A
inst✝ : FinitePresentation A B
⊢ FinitePresentation R B

Tactic:
by

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

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

Tactic:
by

Goal state after:
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
X Y : MorphismProperty.Comma L R P Q W
f : X ⟶ Y
inst✝ : IsIso f
⊢ Hom.hom (inv f) = inv (Hom.hom f)

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : LocallySmall.{w', v_1, u_1} C
⊢ (∃ J x, Nonempty (C ≌ J)) ↔ ObjectProperty.EssentiallySmall.{w, v_1, u_1} ⊤

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
⊢ EssentiallySmall.{w, v, u} C ↔ ObjectProperty.EssentiallySmall.{w, v, u} ⊤

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{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:
by

Goal state after:
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 ((forget L R P Q W).map f)
⊢ IsIso f

Tactic:
by

Goal state after:
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
X Y : MorphismProperty.Comma L R P Q W
h : X = Y
⊢ X.left = Y.left

Tactic:
by

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
F : C ⥤ D
inst✝ : LocallySmall.{w, v_1, u_1} C
H₁ : ObjectProperty.EssentiallySmall.{w, v_2, u_2} F.essImage
H₂ : ∀ (Y : D), ObjectProperty.EssentiallySmall.{w, v_1, u_1} fun x ↦ Nonempty (F.obj x ≅ Y)
Y : D
⊢ ⊤.map F Y ≤ F.essImage Y

Tactic:
by

Goal state after:
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
X Y : MorphismProperty.Comma L R P Q W
h : X = Y
⊢ (eqToHom h).left = eqToHom ⋯

Tactic:
by

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
F : C ⥤ D
inst✝ : LocallySmall.{w, v_1, u_1} C
H₁ : ObjectProperty.EssentiallySmall.{w, v_2, u_2} F.essImage
H₂ : ∀ (Y : D), ObjectProperty.EssentiallySmall.{w, v_1, u_1} fun x ↦ Nonempty (F.obj x ≅ Y)
⊢ ∀ (Y : D), ObjectProperty.EssentiallySmall.{w, v_1, u_1} (⊤ ⊓ fun x ↦ Nonempty (F.obj x ≅ Y))

Tactic:
by

Goal state after:
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
X Y : MorphismProperty.Comma L R P Q W
h : X = Y
⊢ X.right = Y.right

Tactic:
by

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
F : C ⥤ D
inst✝ : LocallySmall.{w, v_1, u_1} C
H₁ : ObjectProperty.EssentiallySmall.{w, v_2, u_2} F.essImage
H₂ : ∀ (Y : D), ObjectProperty.EssentiallySmall.{w, v_1, u_1} fun x ↦ Nonempty (F.obj x ≅ Y)
⊢ EssentiallySmall.{w, v_1, u_1} C

Tactic:
by

Goal state after:
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
X Y : MorphismProperty.Comma L R P Q W
h : X = Y
⊢ (eqToHom h).right = eqToHom ⋯

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
⊢ adjoin R (⇑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤

Tactic:
by

Goal state after:
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
P P' : MorphismProperty T
Q Q' : MorphismProperty A
W W' : MorphismProperty B
hP : P ≤ P'
hQ : Q ≤ Q'
hW : W ≤ W'
inst✝³ : Q.IsMultiplicative
inst✝² : Q'.IsMultiplicative
inst✝¹ : W.IsMultiplicative
inst✝ : W'.IsMultiplicative
X Y : MorphismProperty.Comma L R P Q W
f g : X ⟶ Y
h : (changeProp L R hP hQ hW).map f = (changeProp L R hP hQ hW).map g
⊢ f = g

Tactic:
by

Goal state after:
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
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
inst✝¹ : Q.RespectsIso
inst✝ : W.RespectsIso
X : MorphismProperty.Comma L R P Q W
⊢ P ((𝟙 L).app X.left ≫ X.hom)

Tactic:
by

Goal state after:
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
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
inst✝² : P.RespectsIso
inst✝¹ : Q.RespectsIso
inst✝ : W.RespectsIso
e : L₁ ≅ L₂
X : MorphismProperty.Comma L₁ R P Q W
⊢ P ((𝟙 L₁).app X.left ≫ X.hom)

Tactic:
by

Goal state after:
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
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
inst✝¹ : Q.RespectsIso
inst✝ : W.RespectsIso
X : MorphismProperty.Comma L R P Q W
⊢ P (X.hom ≫ (𝟙 R).app X.right)

Tactic:
by

Goal state after:
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
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
inst✝² : P.RespectsIso
inst✝¹ : Q.RespectsIso
inst✝ : W.RespectsIso
e : R₁ ≅ R₂
X : MorphismProperty.Comma L R₁ P Q W
⊢ P (X.hom ≫ (𝟙 R₁).app X.right)

Tactic:
by

Goal state after: