awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Small (goal)
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
⊢ ObjectProperty.isoClosure (ObjectProperty.ofObj f) S
have 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
Tactic: obtain ⟨T, e, he⟩ := hφ.exists_smallRepr
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Small (goal)
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))
⊢ ObjectProperty.EssentiallySmall.{u, u, u + 1} P
have 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
Tactic: obtain ⟨Q', _, hQ'Q, hQQ'⟩ := ObjectProperty.EssentiallySmall.exists_small_le Q
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Small (goal)
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
have refine : ∀ (S : CommRingCat.{u}) (hS : P S), ObjectProperty.isoClosure (ObjectProperty.ofObj f) S
Tactic: refine ⟨.ofObj f, inferInstance, fun S hS ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Small (goal)
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
⊢ ObjectProperty.isoClosure (ObjectProperty.ofObj f) S
have 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
Tactic: obtain ⟨s, hs, H⟩ := hPQ S hS
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Small (goal)
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))
⊢ ObjectProperty.isoClosure (ObjectProperty.ofObj f) S
have 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
Tactic: wlog hs' : s.Finite generalizing s
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Small (goal)
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
⊢ ObjectProperty.isoClosure (ObjectProperty.ofObj f) S
have 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
Tactic: wlog hs' : s.Finite generalizing s
Cleared hypotheses: s, hs, H
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Small (goal)
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
⊢ ObjectProperty.isoClosure (ObjectProperty.ofObj f) S
have 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
Tactic: obtain ⟨s', hs's, hs'⟩ := (Ideal.span_eq_top_iff_finite _).mp hs
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Small (goal)
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
⊢ ObjectProperty.isoClosure (ObjectProperty.ofObj f) S
have 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
Tactic: choose S' hS' e using fun (f : s) ↦ hQQ' _ (H _ f.2)
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Topology (goal)
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 = x_1
have 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))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Topology (goal)
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)
⊢ 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))
have 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))
Tactic: rw [e]
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Topology (goal)
Goal:
R A B : CommRingCat
inst : TopologicalSpace (↑R : Type u)
f : A ⟶ B
hf :
  Function.Surjective (α := (↑A : Type u)) (β := (↑B : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) f) :
      (a : (↑A : Type u)) → (↑B : Type u))
⊢ IsEmbedding (Y := A ⟶ R) fun (x : B ⟶ R) ↦ f ≫ x
have refine : IsEmbedding.{u, u} (X := B ⟶ R) (Y := (↑A : Type u) → (↑R : Type u))
  ((fun (f : A ⟶ R) ↦ (⇑(Hom.hom f) : (a : (↑A : Type u)) → (↑R : Type u))) ∘ fun (x : B ⟶ R) ↦ f ≫ x)
Tactic: refine IsEmbedding.of_comp (continuous_precomp _) (IsInducing.induced _).continuous ?_
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Topology (goal)
Goal:
R A B : CommRingCat
inst : TopologicalSpace (↑R : Type u)
f_1 : A ⟶ B
hf :
  Function.Surjective (α := (↑A : Type u)) (β := (↑B : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) f_1) :
      (a : (↑A : Type u)) → (↑B : Type u))
this :
  IsEmbedding (Y := (↑A : Type u) → (↑R : Type u)) fun (x : (↑B : Type u) → (↑R : Type u)) ↦
    x ∘ (⇑(Hom.hom f_1) : (a : (↑A : Type u)) → (↑B : Type u))
f g : B ⟶ R
e :
  Eq.{u + 1} (α := (↑B : Type u) → (↑R : Type u))
    (↑(↑f.hom' : (↑B : Type u) →* (↑R : Type u)) : OneHom (↑B : Type u) (↑R : Type u)).1
    (↑(↑g.hom' : (↑B : Type u) →* (↑R : Type u)) : OneHom (↑B : Type u) (↑R : Type u)).1
⊢ f = g
have hf₁ : ∀ (a : (↑B : Type u)),
  Eq (α := (↑R : Type u)) ((Hom.hom f : (a : (↑B : Type u)) → (↑R : Type u)) a : (↑R : Type u))
    ((Hom.hom g : (a : (↑B : Type u)) → (↑R : Type u)) a : (↑R : Type u))
Tactic: ext a
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Topology (goal)
Goal:
R A B : CommRingCat
inst : TopologicalSpace (↑R : Type u)
f : A ⟶ B
hf :
  Function.Surjective (α := (↑A : Type u)) (β := (↑B : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) f) :
      (a : (↑A : Type u)) → (↑B : Type u))
⊢ IsEmbedding.{u, u} (X := B ⟶ R) (Y := (↑A : Type u) → (↑R : Type u))
    ((fun (f : A ⟶ R) ↦ (⇑(Hom.hom f) : (a : (↑A : Type u)) → (↑R : Type u))) ∘ fun (x : B ⟶ R) ↦ f ≫ x)
have suffices : IsEmbedding (Y := (↑A : Type u) → (↑R : Type u)) fun (x : (↑B : Type u) → (↑R : Type u)) ↦
  x ∘ (⇑(Hom.hom f) : (a : (↑A : Type u)) → (↑B : Type u))
Tactic: suffices IsEmbedding ((· ∘ f.hom) : (B → R) → (A → R)) from
    this.comp (.induced (fun f g e ↦ by ext a; exact congr($e a)))
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Topology (goal)
Goal:
R A B : CommRingCat
inst : TopologicalSpace (↑R : Type u)
inst_1 : T1Space.{u} (↑R : Type u)
f : A ⟶ B
hf :
  Function.Surjective (α := (↑A : Type u)) (β := (↑B : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) f) :
      (a : (↑A : Type u)) → (↑B : Type u))
⊢ IsClosedEmbedding (Y := A ⟶ R) fun (x : B ⟶ R) ↦ f ≫ x
have refine : IsClosed[instTopologicalSpaceHom] (Set.range fun (x : B ⟶ R) ↦ f ≫ x)
Tactic: refine ⟨isEmbedding_precomp_of_surjective f hf, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Topology (hypothesis)
Goal:
R A B : CommRingCat
inst : TopologicalSpace (↑R : Type u)
inst_1 : T1Space.{u} (↑R : Type u)
f : A ⟶ B
hf :
  Function.Surjective (α := (↑A : Type u)) (β := (↑B : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) f) :
      (a : (↑A : Type u)) → (↑B : Type u))
⊢ IsClosed[instTopologicalSpaceHom] (Set.range fun (x : B ⟶ R) ↦ f ≫ x)
have this : IsClosed[instTopologicalSpaceHom]
  (⋂ (i : ↥(RingHom.ker (Hom.hom f))),
    {f_1 : A ⟶ R |
      Eq (α := (↑R : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
                f_1 :
              (a : (↑A : Type u)) → (↑R : Type u))
            (↑i : (↑A : Type u)) :
          (↑R : Type u))
        (0 : (↑R : Type u))})
Tactic: have : IsClosed (⋂ i : RingHom.ker f.hom, { f : A ⟶ R | f i = 0 }) :=
    isClosed_iInter fun x ↦ (isClosed_singleton (x := 0)).preimage (continuous_apply (R := R) x.1)
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Topology (goal)
Goal:
R A B : CommRingCat
inst : TopologicalSpace (↑R : Type u)
inst_1 : T1Space.{u} (↑R : Type u)
f : A ⟶ B
hf :
  Function.Surjective (α := (↑A : Type u)) (β := (↑B : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) f) :
      (a : (↑A : Type u)) → (↑B : Type u))
this :
  IsClosed[instTopologicalSpaceHom]
    (⋂ (i : ↥(RingHom.ker (Hom.hom f))),
      {f_1 : A ⟶ R |
        Eq (α := (↑R : Type u))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
                  f_1 :
                (a : (↑A : Type u)) → (↑R : Type u))
              (↑i : (↑A : Type u)) :
            (↑R : Type u))
          (0 : (↑R : Type u))})
⊢ IsClosed[instTopologicalSpaceHom] (Set.range fun (x : B ⟶ R) ↦ f ≫ x)
have h : Eq.{u + 1} (α := Set (A ⟶ R)) (Set.range fun (x : B ⟶ R) ↦ f ≫ x)
  (⋂ (i : ↥(RingHom.ker (Hom.hom f))),
    {f_1 : A ⟶ R |
      Eq (α := (↑R : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
                f_1 :
              (a : (↑A : Type u)) → (↑R : Type u))
            (↑i : (↑A : Type u)) :
          (↑R : Type u))
        (0 : (↑R : Type u))})
Tactic: convert! this
-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Topology (goal)
Goal:
R A B : CommRingCat
inst : TopologicalSpace (↑R : Type u)
inst_1 : T1Space.{u} (↑R : Type u)
f : A ⟶ B
hf :
  Function.Surjective (α := (↑A : Type u)) (β := (↑B : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) f) :
      (a : (↑A : Type u)) → (↑B : Type u))
this :
  IsClosed[instTopologicalSpaceHom]
    (⋂ (i : ↥(RingHom.ker (Hom.hom f))),
      {f_1 : A ⟶ R |
        Eq (α := (↑R : Type u))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
                  f_1 :
                (a : (↑A : Type u)) → (↑R : Type u))
              (↑i : (↑A : Type u)) :
            (↑R : Type u))
          (0 : (↑R : Type u))})
⊢ Eq.{u + 1} (α := Set (A ⟶ R)) (Set.range fun (x : B ⟶ R) ↦ f ≫ x)
    (⋂ (i : ↥(RingHom.ker (Hom.hom f))),
      {f_1 : A ⟶ R |
        Eq (α := (↑R : Type u))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
                  f_1 :
                (a : (↑A : Type u)) → (↑R : Type u))
              (↑i : (↑A : Type u)) :
            (↑R : Type u))
          (0 : (↑R : Type u))})
have h : ∀ (x : A ⟶ R),
  Membership.mem (γ := Set (A ⟶ R)) (Set.range fun (x : B ⟶ R) ↦ f ≫ x) x ↔
    Membership.mem (γ := Set (A ⟶ R))
      (⋂ (i : ↥(RingHom.ker (Hom.hom f))),
        {f_1 : A ⟶ R |
          Eq (α := (↑R : Type u))
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
                    f_1 :
                  (a : (↑A : Type u)) → (↑R : Type u))
                (↑i : (↑A : Type u)) :
              (↑R : Type u))
            (0 : (↑R : Type u))})
      x
Tactic: ext x