awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.Ring.Small
Goal:
P Q : ObjectProperty CommRingCat
inst : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q
hPQ : ∀ (S : CommRingCat.{u}), P S → ∃ (R : CommRingCat.{u}), Q R ∧ ∃ (f : R ⟶ S), (Hom.hom f).FiniteType
Q' : ObjectProperty CommRingCat
w : ObjectProperty.Small.{u, u, u + 1} Q'
hQ'Q : Q' ≤ Q
hQQ' : Q ≤ Q'.isoClosure
f : (S : (R : Subtype Q') × FGAlgCatSkeleton (↑(↑R : CommRingCat) : Type u)) → CommRingCat :=
  fun (S : (R : Subtype Q') × FGAlgCatSkeleton (↑(↑R : CommRingCat) : Type u)) ↦
    of
      (↑((FGAlgCatSkeleton.eval
                (↑(↑(S.fst (β := fun (R : Subtype Q') ↦ FGAlgCatSkeleton (↑(↑R : CommRingCat) : Type u))) :
                      CommRingCat) :
                  Type u)
                (S.snd (β := fun (R : Subtype Q') ↦ FGAlgCatSkeleton (↑(↑R : CommRingCat) : Type u)))).obj
            (P :=
            fun
              (A :
                CommAlgCat
                  (↑(↑(S.fst (β := fun (R : Subtype Q') ↦ FGAlgCatSkeleton (↑(↑R : CommRingCat) : Type u))) :
                        CommRingCat) :
                    Type u)) ↦
            Algebra.FiniteType.{u, u}
              (↑(↑(S.fst (β := fun (R : Subtype Q') ↦ FGAlgCatSkeleton (↑(↑R : CommRingCat) : Type u))) : CommRingCat) :
                Type u)
              (↑A : Type u))) :
        Type u)
S : CommRingCat
hS : P S
R : CommRingCat
hR : Q R
φ : R ⟶ S
hφ : (Hom.hom φ).FiniteType
hR' : Q' R
obtain :
  ∀ (T : FGAlgCatSkeleton (↑R : Type u))
    (e :
      (↑((FGAlgCatSkeleton.eval (↑R : Type u) T).obj (P := fun (A : CommAlgCat (↑R : Type u)) ↦
              Algebra.FiniteType.{u, u} (↑R : Type u) (↑A : Type u))) :
          Type u) ≃+*
        (↑S : Type u))
    (he :
      Hom.hom φ =
        e.toRingHom.comp
          (algebraMap (↑R : Type u)
            (↑((FGAlgCatSkeleton.eval (↑R : Type u) T).obj (P := fun (A : CommAlgCat (↑R : Type u)) ↦
                  Algebra.FiniteType.{u, u} (↑R : Type u) (↑A : Type u))) :
              Type u))),
    ObjectProperty.isoClosure (ObjectProperty.ofObj f) S
⊢ ObjectProperty.isoClosure (ObjectProperty.ofObj f) S

Tactic:
obtain ⟨T, e, he⟩ := hφ.exists_smallRepr

Premises used: RingHom.FiniteType.exists_smallRepr
-- Module: Mathlib.Algebra.Category.Ring.Small
Goal:
P Q : ObjectProperty CommRingCat
inst : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q
hPQ : ∀ (S : CommRingCat.{u}), P S → ∃ (R : CommRingCat.{u}), Q R ∧ ∃ (f : R ⟶ S), (Hom.hom f).FiniteType
Q' : ObjectProperty CommRingCat
w : ObjectProperty.Small.{u, u, u + 1} Q'
hQ'Q : Q' ≤ Q
hQQ' : Q ≤ Q'.isoClosure
f : (S : (R : Subtype Q') × FGAlgCatSkeleton (↑(↑R : CommRingCat) : Type u)) → CommRingCat :=
  fun (S : (R : Subtype Q') × FGAlgCatSkeleton (↑(↑R : CommRingCat) : Type u)) ↦
    of
      (↑((FGAlgCatSkeleton.eval
                (↑(↑(S.fst (β := fun (R : Subtype Q') ↦ FGAlgCatSkeleton (↑(↑R : CommRingCat) : Type u))) :
                      CommRingCat) :
                  Type u)
                (S.snd (β := fun (R : Subtype Q') ↦ FGAlgCatSkeleton (↑(↑R : CommRingCat) : Type u)))).obj
            (P :=
            fun
              (A :
                CommAlgCat
                  (↑(↑(S.fst (β := fun (R : Subtype Q') ↦ FGAlgCatSkeleton (↑(↑R : CommRingCat) : Type u))) :
                        CommRingCat) :
                    Type u)) ↦
            Algebra.FiniteType.{u, u}
              (↑(↑(S.fst (β := fun (R : Subtype Q') ↦ FGAlgCatSkeleton (↑(↑R : CommRingCat) : Type u))) : CommRingCat) :
                Type u)
              (↑A : Type u))) :
        Type u)
S : CommRingCat
hS : P S
R : CommRingCat
hR : Q R
φ : R ⟶ S
hφ : (Hom.hom φ).FiniteType
hR' : Q' R
T : FGAlgCatSkeleton (↑R : Type u)
e :
  (↑((FGAlgCatSkeleton.eval (↑R : Type u) T).obj (P := fun (A : CommAlgCat (↑R : Type u)) ↦
          Algebra.FiniteType.{u, u} (↑R : Type u) (↑A : Type u))) :
      Type u) ≃+*
    (↑S : Type u)
he :
  Hom.hom φ =
    e.toRingHom.comp
      (algebraMap (↑R : Type u)
        (↑((FGAlgCatSkeleton.eval (↑R : Type u) T).obj (P := fun (A : CommAlgCat (↑R : Type u)) ↦
              Algebra.FiniteType.{u, u} (↑R : Type u) (↑A : Type u))) :
          Type u))
⊢ ObjectProperty.isoClosure (ObjectProperty.ofObj f) S

Tactic:
⟨_, ⟨⟨_, hR'⟩, T⟩, ⟨RingEquiv.toCommRingCatIso e.symm⟩⟩

Premises used: RingEquiv.toCommRingCatIso, Nonempty.intro, CategoryTheory.ObjectProperty.ofObj.mk, CategoryTheory.ObjectProperty.isoClosure, Exists.intro
-- Module: Mathlib.Algebra.Category.Ring.Small
Goal:
P Q : ObjectProperty CommRingCat
inst : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q
hPQ : ∀ (S : CommRingCat.{u}), P S → ∃ (R : CommRingCat.{u}), Q R ∧ ∃ (f : R ⟶ S), (Hom.hom f).FiniteType
Q' : ObjectProperty CommRingCat
w : ObjectProperty.Small.{u, u, u + 1} Q'
hQ'Q : Q' ≤ Q
hQQ' : Q ≤ Q'.isoClosure
f : (S : (R : Subtype Q') × FGAlgCatSkeleton (↑(↑R : CommRingCat) : Type u)) → CommRingCat :=
  fun (S : (R : Subtype Q') × FGAlgCatSkeleton (↑(↑R : CommRingCat) : Type u)) ↦
    of
      (↑((FGAlgCatSkeleton.eval
                (↑(↑(S.fst (β := fun (R : Subtype Q') ↦ FGAlgCatSkeleton (↑(↑R : CommRingCat) : Type u))) :
                      CommRingCat) :
                  Type u)
                (S.snd (β := fun (R : Subtype Q') ↦ FGAlgCatSkeleton (↑(↑R : CommRingCat) : Type u)))).obj
            (P :=
            fun
              (A :
                CommAlgCat
                  (↑(↑(S.fst (β := fun (R : Subtype Q') ↦ FGAlgCatSkeleton (↑(↑R : CommRingCat) : Type u))) :
                        CommRingCat) :
                    Type u)) ↦
            Algebra.FiniteType.{u, u}
              (↑(↑(S.fst (β := fun (R : Subtype Q') ↦ FGAlgCatSkeleton (↑(↑R : CommRingCat) : Type u))) : CommRingCat) :
                Type u)
              (↑A : Type u))) :
        Type u)
S : CommRingCat
hS : P S
R : CommRingCat
hR : Q R
φ : R ⟶ S
hφ : (Hom.hom φ).FiniteType
hR' : Q' R
T : FGAlgCatSkeleton (↑R : Type u)
e :
  (↑((FGAlgCatSkeleton.eval (↑R : Type u) T).obj (P := fun (A : CommAlgCat (↑R : Type u)) ↦
          Algebra.FiniteType.{u, u} (↑R : Type u) (↑A : Type u))) :
      Type u) ≃+*
    (↑S : Type u)
he :
  Hom.hom φ =
    e.toRingHom.comp
      (algebraMap (↑R : Type u)
        (↑((FGAlgCatSkeleton.eval (↑R : Type u) T).obj (P := fun (A : CommAlgCat (↑R : Type u)) ↦
              Algebra.FiniteType.{u, u} (↑R : Type u) (↑A : Type u))) :
          Type u))
⊢ ObjectProperty.isoClosure (ObjectProperty.ofObj f) S

Tactic:
exact ⟨_, ⟨⟨_, hR'⟩, T⟩, ⟨RingEquiv.toCommRingCatIso e.symm⟩⟩
-- Module: Mathlib.Algebra.Category.Ring.Small
Goal:
P Q : ObjectProperty CommRingCat
inst : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q
hPQ :
  ∀ (S : CommRingCat.{u}),
    P S →
      ∃ (s : Set (↑S : Type u)), Eq (α := Ideal (↑S : Type u)) (Ideal.span s) ⊤ ∧ ∀ f ∈ s, Q (of (Localization.Away f))
obtain :
  ∀ (Q' : ObjectProperty CommRingCat),
    ObjectProperty.Small.{u, u, u + 1} Q' →
      ∀ (hQ'Q : Q' ≤ Q) (hQQ' : Q ≤ Q'.isoClosure), ObjectProperty.EssentiallySmall.{u, u, u + 1} P
⊢ ObjectProperty.EssentiallySmall.{u, u, u + 1} P

Tactic:
obtain ⟨Q', _, hQ'Q, hQQ'⟩ := ObjectProperty.EssentiallySmall.exists_small_le Q

Premises used: CategoryTheory.ObjectProperty.EssentiallySmall.exists_small_le
-- Module: Mathlib.Algebra.Category.Ring.Small
Goal:
P Q : ObjectProperty CommRingCat
inst : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q
hPQ :
  ∀ (S : CommRingCat.{u}),
    P S →
      ∃ (s : Set (↑S : Type u)), Eq (α := Ideal (↑S : Type u)) (Ideal.span s) ⊤ ∧ ∀ f ∈ s, Q (of (Localization.Away f))
Q' : ObjectProperty CommRingCat
w : ObjectProperty.Small.{u, u, u + 1} Q'
hQ'Q : Q' ≤ Q
hQQ' : Q ≤ Q'.isoClosure
f : (S : (n : ℕ) × (R : Fin n → Subtype Q') × Subring ((i : Fin n) → (↑(↑(R i) : CommRingCat) : Type u))) →
  CommRingCat :=
  fun (S : (n : ℕ) × (R : Fin n → Subtype Q') × Subring ((i : Fin n) → (↑(↑(R i) : CommRingCat) : Type u))) ↦
    of
      ↥(S.snd (β := fun (n : ℕ) ↦
              (R : Fin n → Subtype Q') × Subring ((i : Fin n) → (↑(↑(R i) : CommRingCat) : Type u))).snd
          (β :=
          fun
            (R :
              Fin
                  (S.fst (β := fun (n : ℕ) ↦
                    (R : Fin n → Subtype Q') × Subring ((i : Fin n) → (↑(↑(R i) : CommRingCat) : Type u)))) →
                Subtype Q') ↦
          Subring
            ((i :
                Fin
                  (S.fst (β := fun (n : ℕ) ↦
                    (R : Fin n → Subtype Q') × Subring ((i : Fin n) → (↑(↑(R i) : CommRingCat) : Type u))))) →
              (↑(↑(R i) : CommRingCat) : Type u))))
⊢ ObjectProperty.EssentiallySmall.{u, u, u + 1} P

Tactic:
⟨.ofObj f, inferInstance, fun S hS ↦ ?_⟩

Premises used: CategoryTheory.ObjectProperty.ofObj, inferInstance, Exists.intro, CategoryTheory.ObjectProperty.EssentiallySmall.mk
-- Module: Mathlib.Algebra.Category.Ring.Small
Goal:
P Q : ObjectProperty CommRingCat
inst : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q
hPQ :
  ∀ (S : CommRingCat.{u}),
    P S →
      ∃ (s : Set (↑S : Type u)), Eq (α := Ideal (↑S : Type u)) (Ideal.span s) ⊤ ∧ ∀ f ∈ s, Q (of (Localization.Away f))
Q' : ObjectProperty CommRingCat
w : ObjectProperty.Small.{u, u, u + 1} Q'
hQ'Q : Q' ≤ Q
hQQ' : Q ≤ Q'.isoClosure
f : (S : (n : ℕ) × (R : Fin n → Subtype Q') × Subring ((i : Fin n) → (↑(↑(R i) : CommRingCat) : Type u))) →
  CommRingCat :=
  fun (S : (n : ℕ) × (R : Fin n → Subtype Q') × Subring ((i : Fin n) → (↑(↑(R i) : CommRingCat) : Type u))) ↦
    of
      ↥(S.snd (β := fun (n : ℕ) ↦
              (R : Fin n → Subtype Q') × Subring ((i : Fin n) → (↑(↑(R i) : CommRingCat) : Type u))).snd
          (β :=
          fun
            (R :
              Fin
                  (S.fst (β := fun (n : ℕ) ↦
                    (R : Fin n → Subtype Q') × Subring ((i : Fin n) → (↑(↑(R i) : CommRingCat) : Type u)))) →
                Subtype Q') ↦
          Subring
            ((i :
                Fin
                  (S.fst (β := fun (n : ℕ) ↦
                    (R : Fin n → Subtype Q') × Subring ((i : Fin n) → (↑(↑(R i) : CommRingCat) : Type u))))) →
              (↑(↑(R i) : CommRingCat) : Type u))))
refine : ∀ (S : CommRingCat.{u}) (hS : P S), ObjectProperty.isoClosure (ObjectProperty.ofObj f) S
⊢ ObjectProperty.EssentiallySmall.{u, u, u + 1} P

Tactic:
refine ⟨.ofObj f, inferInstance, fun S hS ↦ ?_⟩
-- Module: Mathlib.Algebra.Category.Ring.Small
Goal:
P Q : ObjectProperty CommRingCat
inst : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q
hPQ :
  ∀ (S : CommRingCat.{u}),
    P S →
      ∃ (s : Set (↑S : Type u)), Eq (α := Ideal (↑S : Type u)) (Ideal.span s) ⊤ ∧ ∀ f ∈ s, Q (of (Localization.Away f))
Q' : ObjectProperty CommRingCat
w : ObjectProperty.Small.{u, u, u + 1} Q'
hQ'Q : Q' ≤ Q
hQQ' : Q ≤ Q'.isoClosure
f : (S : (n : ℕ) × (R : Fin n → Subtype Q') × Subring ((i : Fin n) → (↑(↑(R i) : CommRingCat) : Type u))) →
  CommRingCat :=
  fun (S : (n : ℕ) × (R : Fin n → Subtype Q') × Subring ((i : Fin n) → (↑(↑(R i) : CommRingCat) : Type u))) ↦
    of
      ↥(S.snd (β := fun (n : ℕ) ↦
              (R : Fin n → Subtype Q') × Subring ((i : Fin n) → (↑(↑(R i) : CommRingCat) : Type u))).snd
          (β :=
          fun
            (R :
              Fin
                  (S.fst (β := fun (n : ℕ) ↦
                    (R : Fin n → Subtype Q') × Subring ((i : Fin n) → (↑(↑(R i) : CommRingCat) : Type u)))) →
                Subtype Q') ↦
          Subring
            ((i :
                Fin
                  (S.fst (β := fun (n : ℕ) ↦
                    (R : Fin n → Subtype Q') × Subring ((i : Fin n) → (↑(↑(R i) : CommRingCat) : Type u))))) →
              (↑(↑(R i) : CommRingCat) : Type u))))
S : CommRingCat
hS : P S
obtain :
  ∀ (s : Set (↑S : Type u)) (hs : Eq (α := Ideal (↑S : Type u)) (Ideal.span s) ⊤)
    (H : ∀ f ∈ s, Q (of (Localization.Away f))), ObjectProperty.isoClosure (ObjectProperty.ofObj f) S
⊢ ObjectProperty.isoClosure (ObjectProperty.ofObj f) S

Tactic:
obtain ⟨s, hs, H⟩ := hPQ S hS
-- Module: Mathlib.Algebra.Category.Ring.Small
Goal:
P Q : ObjectProperty CommRingCat
inst : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q
hPQ :
  ∀ (S : CommRingCat.{u}),
    P S →
      ∃ (s : Set (↑S : Type u)), Eq (α := Ideal (↑S : Type u)) (Ideal.span s) ⊤ ∧ ∀ f ∈ s, Q (of (Localization.Away f))
Q' : ObjectProperty CommRingCat
w : ObjectProperty.Small.{u, u, u + 1} Q'
hQ'Q : Q' ≤ Q
hQQ' : Q ≤ Q'.isoClosure
f : (S : (n : ℕ) × (R : Fin n → Subtype Q') × Subring ((i : Fin n) → (↑(↑(R i) : CommRingCat) : Type u))) →
  CommRingCat :=
  fun (S : (n : ℕ) × (R : Fin n → Subtype Q') × Subring ((i : Fin n) → (↑(↑(R i) : CommRingCat) : Type u))) ↦
    of
      ↥(S.snd (β := fun (n : ℕ) ↦
              (R : Fin n → Subtype Q') × Subring ((i : Fin n) → (↑(↑(R i) : CommRingCat) : Type u))).snd
          (β :=
          fun
            (R :
              Fin
                  (S.fst (β := fun (n : ℕ) ↦
                    (R : Fin n → Subtype Q') × Subring ((i : Fin n) → (↑(↑(R i) : CommRingCat) : Type u)))) →
                Subtype Q') ↦
          Subring
            ((i :
                Fin
                  (S.fst (β := fun (n : ℕ) ↦
                    (R : Fin n → Subtype Q') × Subring ((i : Fin n) → (↑(↑(R i) : CommRingCat) : Type u))))) →
              (↑(↑(R i) : CommRingCat) : Type u))))
S : CommRingCat
hS : P S
s : Set (↑S : Type u)
hs : Eq (α := Ideal (↑S : Type u)) (Ideal.span s) ⊤
H : ∀ f ∈ s, Q (of (Localization.Away f))
inr :
  ∀
    (this :
      ∀ (s : Set (↑S : Type u)) (hs : Eq (α := Ideal (↑S : Type u)) (Ideal.span s) ⊤)
        (H : ∀ f ∈ s, Q (of (Localization.Away f))) (hs' : s.Finite),
        ObjectProperty.isoClosure (ObjectProperty.ofObj f) S)
    (hs' : ¬s.Finite), ObjectProperty.isoClosure (ObjectProperty.ofObj f) S
wlog :
  ∀ (s : Set (↑S : Type u)) (hs : Eq (α := Ideal (↑S : Type u)) (Ideal.span s) ⊤)
    (H : ∀ f ∈ s, Q (of (Localization.Away f))) (hs' : s.Finite), ObjectProperty.isoClosure (ObjectProperty.ofObj f) S
⊢ ObjectProperty.isoClosure (ObjectProperty.ofObj f) S

Tactic:
wlog hs' : s.Finite generalizing s

Premises used: Set.Finite
-- Module: Mathlib.Algebra.Category.Ring.Small
Goal:
P Q : ObjectProperty CommRingCat
inst : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q
hPQ :
  ∀ (S : CommRingCat.{u}),
    P S →
      ∃ (s : Set (↑S : Type u)), Eq (α := Ideal (↑S : Type u)) (Ideal.span s) ⊤ ∧ ∀ f ∈ s, Q (of (Localization.Away f))
Q' : ObjectProperty CommRingCat
w : ObjectProperty.Small.{u, u, u + 1} Q'
hQ'Q : Q' ≤ Q
hQQ' : Q ≤ Q'.isoClosure
f : (S : (n : ℕ) × (R : Fin n → Subtype Q') × Subring ((i : Fin n) → (↑(↑(R i) : CommRingCat) : Type u))) →
  CommRingCat :=
  fun (S : (n : ℕ) × (R : Fin n → Subtype Q') × Subring ((i : Fin n) → (↑(↑(R i) : CommRingCat) : Type u))) ↦
    of
      ↥(S.snd (β := fun (n : ℕ) ↦
              (R : Fin n → Subtype Q') × Subring ((i : Fin n) → (↑(↑(R i) : CommRingCat) : Type u))).snd
          (β :=
          fun
            (R :
              Fin
                  (S.fst (β := fun (n : ℕ) ↦
                    (R : Fin n → Subtype Q') × Subring ((i : Fin n) → (↑(↑(R i) : CommRingCat) : Type u)))) →
                Subtype Q') ↦
          Subring
            ((i :
                Fin
                  (S.fst (β := fun (n : ℕ) ↦
                    (R : Fin n → Subtype Q') × Subring ((i : Fin n) → (↑(↑(R i) : CommRingCat) : Type u))))) →
              (↑(↑(R i) : CommRingCat) : Type u))))
S : CommRingCat
hS : P S
s : Set (↑S : Type u)
hs : Eq (α := Ideal (↑S : Type u)) (Ideal.span s) ⊤
H : ∀ f ∈ s, Q (of (Localization.Away f))
this :
  ∀ (s : Set (↑S : Type u)) (hs : Eq (α := Ideal (↑S : Type u)) (Ideal.span s) ⊤)
    (H : ∀ f ∈ s, Q (of (Localization.Away f))) (hs' : s.Finite), ObjectProperty.isoClosure (ObjectProperty.ofObj f) S
hs' : ¬s.Finite
inr :
  ∀ (s' : Finset (↑S : Type u)) (hs's : (↑s' : Set (↑S : Type u)) ⊆ s)
    (hs' : Eq (α := Ideal (↑S : Type u)) (Ideal.span (↑s' : Set (↑S : Type u))) ⊤),
    ObjectProperty.isoClosure (ObjectProperty.ofObj f) S
⊢ ObjectProperty.isoClosure (ObjectProperty.ofObj f) S

Tactic:
obtain ⟨s', hs's, hs'⟩ := (Ideal.span_eq_top_iff_finite _).mp hs

Premises used: Ideal.span_eq_top_iff_finite, Iff.mp
-- Module: Mathlib.Algebra.Category.Ring.Small
Goal:
P Q : ObjectProperty CommRingCat
inst : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q
hPQ :
  ∀ (S : CommRingCat.{u}),
    P S →
      ∃ (s : Set (↑S : Type u)), Eq (α := Ideal (↑S : Type u)) (Ideal.span s) ⊤ ∧ ∀ f ∈ s, Q (of (Localization.Away f))
Q' : ObjectProperty CommRingCat
w : ObjectProperty.Small.{u, u, u + 1} Q'
hQ'Q : Q' ≤ Q
hQQ' : Q ≤ Q'.isoClosure
f : (S : (n : ℕ) × (R : Fin n → Subtype Q') × Subring ((i : Fin n) → (↑(↑(R i) : CommRingCat) : Type u))) →
  CommRingCat :=
  fun (S : (n : ℕ) × (R : Fin n → Subtype Q') × Subring ((i : Fin n) → (↑(↑(R i) : CommRingCat) : Type u))) ↦
    of
      ↥(S.snd (β := fun (n : ℕ) ↦
              (R : Fin n → Subtype Q') × Subring ((i : Fin n) → (↑(↑(R i) : CommRingCat) : Type u))).snd
          (β :=
          fun
            (R :
              Fin
                  (S.fst (β := fun (n : ℕ) ↦
                    (R : Fin n → Subtype Q') × Subring ((i : Fin n) → (↑(↑(R i) : CommRingCat) : Type u)))) →
                Subtype Q') ↦
          Subring
            ((i :
                Fin
                  (S.fst (β := fun (n : ℕ) ↦
                    (R : Fin n → Subtype Q') × Subring ((i : Fin n) → (↑(↑(R i) : CommRingCat) : Type u))))) →
              (↑(↑(R i) : CommRingCat) : Type u))))
S : CommRingCat
hS : P S
s : Set (↑S : Type u)
hs : Eq (α := Ideal (↑S : Type u)) (Ideal.span s) ⊤
H : ∀ f ∈ s, Q (of (Localization.Away f))
this :
  ∀ (s : Set (↑S : Type u)) (hs : Eq (α := Ideal (↑S : Type u)) (Ideal.span s) ⊤)
    (H : ∀ f ∈ s, Q (of (Localization.Away f))) (hs' : s.Finite), ObjectProperty.isoClosure (ObjectProperty.ofObj f) S
hs'_1 : ¬s.Finite
s' : Finset (↑S : Type u)
hs's : (↑s' : Set (↑S : Type u)) ⊆ s
hs' : Eq (α := Ideal (↑S : Type u)) (Ideal.span (↑s' : Set (↑S : Type u))) ⊤
⊢ ObjectProperty.isoClosure (ObjectProperty.ofObj f) S

Tactic:
this s' hs' (fun f hf ↦ H f (hs's hf)) s'.finite_toSet

Premises used: SetLike.coe, Finset.finite_toSet
-- Module: Mathlib.Algebra.Category.Ring.Small
Goal:
P Q : ObjectProperty CommRingCat
inst : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q
hPQ :
  ∀ (S : CommRingCat.{u}),
    P S →
      ∃ (s : Set (↑S : Type u)), Eq (α := Ideal (↑S : Type u)) (Ideal.span s) ⊤ ∧ ∀ f ∈ s, Q (of (Localization.Away f))
Q' : ObjectProperty CommRingCat
w : ObjectProperty.Small.{u, u, u + 1} Q'
hQ'Q : Q' ≤ Q
hQQ' : Q ≤ Q'.isoClosure
f : (S : (n : ℕ) × (R : Fin n → Subtype Q') × Subring ((i : Fin n) → (↑(↑(R i) : CommRingCat) : Type u))) →
  CommRingCat :=
  fun (S : (n : ℕ) × (R : Fin n → Subtype Q') × Subring ((i : Fin n) → (↑(↑(R i) : CommRingCat) : Type u))) ↦
    of
      ↥(S.snd (β := fun (n : ℕ) ↦
              (R : Fin n → Subtype Q') × Subring ((i : Fin n) → (↑(↑(R i) : CommRingCat) : Type u))).snd
          (β :=
          fun
            (R :
              Fin
                  (S.fst (β := fun (n : ℕ) ↦
                    (R : Fin n → Subtype Q') × Subring ((i : Fin n) → (↑(↑(R i) : CommRingCat) : Type u)))) →
                Subtype Q') ↦
          Subring
            ((i :
                Fin
                  (S.fst (β := fun (n : ℕ) ↦
                    (R : Fin n → Subtype Q') × Subring ((i : Fin n) → (↑(↑(R i) : CommRingCat) : Type u))))) →
              (↑(↑(R i) : CommRingCat) : Type u))))
S : CommRingCat
hS : P S
s : Set (↑S : Type u)
hs : Eq (α := Ideal (↑S : Type u)) (Ideal.span s) ⊤
H : ∀ f ∈ s, Q (of (Localization.Away f))
this :
  ∀ (s : Set (↑S : Type u)) (hs : Eq (α := Ideal (↑S : Type u)) (Ideal.span s) ⊤)
    (H : ∀ f ∈ s, Q (of (Localization.Away f))) (hs' : s.Finite), ObjectProperty.isoClosure (ObjectProperty.ofObj f) S
hs'_1 : ¬s.Finite
s' : Finset (↑S : Type u)
hs's : (↑s' : Set (↑S : Type u)) ⊆ s
hs' : Eq (α := Ideal (↑S : Type u)) (Ideal.span (↑s' : Set (↑S : Type u))) ⊤
⊢ ObjectProperty.isoClosure (ObjectProperty.ofObj f) S

Tactic:
exact this s' hs' (fun f hf ↦ H f (hs's hf)) s'.finite_toSet

Premises used: SetLike.coe, Finset.finite_toSet
-- Module: Mathlib.Algebra.Category.Ring.Small
Goal:
P Q : ObjectProperty CommRingCat
inst : ObjectProperty.EssentiallySmall.{u, u, u + 1} Q
hPQ :
  ∀ (S : CommRingCat.{u}),
    P S →
      ∃ (s : Set (↑S : Type u)), Eq (α := Ideal (↑S : Type u)) (Ideal.span s) ⊤ ∧ ∀ f ∈ s, Q (of (Localization.Away f))
Q' : ObjectProperty CommRingCat
w : ObjectProperty.Small.{u, u, u + 1} Q'
hQ'Q : Q' ≤ Q
hQQ' : Q ≤ Q'.isoClosure
f : (S : (n : ℕ) × (R : Fin n → Subtype Q') × Subring ((i : Fin n) → (↑(↑(R i) : CommRingCat) : Type u))) →
  CommRingCat :=
  fun (S : (n : ℕ) × (R : Fin n → Subtype Q') × Subring ((i : Fin n) → (↑(↑(R i) : CommRingCat) : Type u))) ↦
    of
      ↥(S.snd (β := fun (n : ℕ) ↦
              (R : Fin n → Subtype Q') × Subring ((i : Fin n) → (↑(↑(R i) : CommRingCat) : Type u))).snd
          (β :=
          fun
            (R :
              Fin
                  (S.fst (β := fun (n : ℕ) ↦
                    (R : Fin n → Subtype Q') × Subring ((i : Fin n) → (↑(↑(R i) : CommRingCat) : Type u)))) →
                Subtype Q') ↦
          Subring
            ((i :
                Fin
                  (S.fst (β := fun (n : ℕ) ↦
                    (R : Fin n → Subtype Q') × Subring ((i : Fin n) → (↑(↑(R i) : CommRingCat) : Type u))))) →
              (↑(↑(R i) : CommRingCat) : Type u))))
S : CommRingCat
hS : P S
s : Set (↑S : Type u)
hs : Eq (α := Ideal (↑S : Type u)) (Ideal.span s) ⊤
H : ∀ f ∈ s, Q (of (Localization.Away f))
hs' : s.Finite
choose :
  ∀ (S' : (f : (↑s : Type u)) → CommRingCat.{u}) (hS' : ∀ (f : (↑s : Type u)), Q' (S' f))
    (e : ∀ (f : (↑s : Type u)), Nonempty.{u + 1} (of (Localization.Away (↑f : (↑S : Type u))) ≅ S' f)),
    ObjectProperty.isoClosure (ObjectProperty.ofObj f) S
⊢ ObjectProperty.isoClosure (ObjectProperty.ofObj f) S

Tactic:
choose S' hS' e using fun (f : s) ↦ hQQ' _ (H _ f.2)

Premises used: Localization.Away, CommRingCat.of, Subtype.val, Subtype.property
-- Module: Mathlib.Algebra.Category.Ring.Topology
Goal:
R A : CommRingCat
inst : TopologicalSpace (↑R : Type u)
x : (↑A : Type u)
⊢ Continuous[instTopologicalSpaceHom, inst] fun (f : A ⟶ R) ↦ (Hom.hom f : (a : (↑A : Type u)) → (↑R : Type u)) x

Tactic:
(continuous_apply x).comp continuous_induced_dom

Premises used: Continuous.comp, continuous_induced_dom, continuous_apply
-- Module: Mathlib.Algebra.Category.Ring.Topology
Goal:
R A : CommRingCat
inst : TopologicalSpace (↑R : Type u)
x x_1 : A ⟶ R
e :
  Eq (α := (a : (↑A : Type u)) → (↑R : Type u)) (⇑(Hom.hom x) : (a : (↑A : Type u)) → (↑R : Type u))
    (⇑(Hom.hom x_1) : (a : (↑A : Type u)) → (↑R : Type u))
hf :
  ∀ (x_2 : (↑A : Type u)),
    Eq (α := (↑R : Type u)) ((Hom.hom x : (a : (↑A : Type u)) → (↑R : Type u)) x_2 : (↑R : Type u))
      ((Hom.hom x_1 : (a : (↑A : Type u)) → (↑R : Type u)) x_2 : (↑R : Type u))
⊢ x = x_1

Tactic:
ext
-- Module: Mathlib.Algebra.Category.Ring.Topology
Goal:
R A : CommRingCat
inst : TopologicalSpace (↑R : Type u)
x x_1 : A ⟶ R
e :
  Eq (α := (a : (↑A : Type u)) → (↑R : Type u)) (⇑(Hom.hom x) : (a : (↑A : Type u)) → (↑R : Type u))
    (⇑(Hom.hom x_1) : (a : (↑A : Type u)) → (↑R : Type u))
x_2 : (↑A : Type u)
hf hf₁ :
  Eq (α := (↑R : Type u)) ((Hom.hom x_1 : (a : (↑A : Type u)) → (↑R : Type u)) x_2 : (↑R : Type u))
    ((Hom.hom x_1 : (a : (↑A : Type u)) → (↑R : Type u)) x_2 : (↑R : Type u))
⊢ Eq (α := (↑R : Type u)) ((Hom.hom x : (a : (↑A : Type u)) → (↑R : Type u)) x_2 : (↑R : Type u))
    ((Hom.hom x_1 : (a : (↑A : Type u)) → (↑R : Type u)) x_2 : (↑R : Type u))

Tactic:
rw [e]
-- Module: Mathlib.Algebra.Category.Ring.Topology
Goal:
R A B : CommRingCat
inst : TopologicalSpace (↑R : Type u)
f : A ⟶ B
⊢ Continuous[instTopologicalSpaceHom, instTopologicalSpaceHom] fun (x : B ⟶ R) ↦ f ≫ x

Tactic:
continuous_induced_rng.mpr ((Pi.continuous_precomp f.hom).comp continuous_induced_dom)

Premises used: Iff.mpr, CommRingCat.Hom.hom, Pi.continuous_precomp, Continuous.comp, continuous_induced_dom, DFunLike.coe, continuous_induced_rng
-- Module: Mathlib.Algebra.Category.Ring.Topology
Goal:
R A B C : CommRingCat
inst : TopologicalSpace (↑R : Type u)
f : A ≅ B
x : B ⟶ R
⊢ (fun (φ : A ⟶ R) ↦ f.inv ≫ φ) ((fun (φ : B ⟶ R) ↦ f.hom ≫ φ) x) = x

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Ring.Topology
Goal:
R A B C : CommRingCat
inst : TopologicalSpace (↑R : Type u)
f : A ≅ B
x : A ⟶ R
⊢ (fun (φ : B ⟶ R) ↦ f.hom ≫ φ) ((fun (φ : A ⟶ R) ↦ f.inv ≫ φ) x) = x

Tactic:
simp