awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.Ring.Topology
Goal:
R A B : CommRingCat
inst : TopologicalSpace (↑R : Type u)
f : A ⟶ B
inst_1 : IsIso f
⊢ IsHomeomorph (Y := A ⟶ R) fun (x : B ⟶ R) ↦ f ≫ x

Tactic:
(precompHomeomorph (asIso f)).isHomeomorph

Premises used: CommRingCat.HomTopology.precompHomeomorph, Homeomorph.isHomeomorph, CategoryTheory.asIso
-- Module: Mathlib.Algebra.Category.Ring.Topology
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

Tactic:
IsEmbedding.of_comp (continuous_precomp _) (IsInducing.induced _).continuous ?_

Premises used: CommRingCat.HomTopology.continuous_precomp, Topology.IsEmbedding.of_comp, Topology.IsInducing.continuous, Topology.IsInducing.induced
-- Module: Mathlib.Algebra.Category.Ring.Topology
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))
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)
⊢ IsEmbedding (Y := A ⟶ R) fun (x : B ⟶ R) ↦ f ≫ x

Tactic:
refine IsEmbedding.of_comp (continuous_precomp _) (IsInducing.induced _).continuous ?_

Premises used: CommRingCat.HomTopology.continuous_precomp, Topology.IsEmbedding.of_comp, Topology.IsInducing.continuous, Topology.IsInducing.induced
-- Module: Mathlib.Algebra.Category.Ring.Topology
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
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))
⊢ f = g

Tactic:
ext a
-- Module: Mathlib.Algebra.Category.Ring.Topology
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
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:
congr($e a)

Premises used: id, congrFun
-- Module: Mathlib.Algebra.Category.Ring.Topology
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
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:
exact congr($e a)
-- Module: Mathlib.Algebra.Category.Ring.Topology
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))
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))
⊢ 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:
suffices IsEmbedding ((· ∘ f.hom) : (B → R) → (A → R)) from
    this.comp (.induced (fun f g e ↦ by ext a; exact congr($e a)))
-- Module: Mathlib.Algebra.Category.Ring.Topology
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 : 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:
Function.Surjective.isEmbedding_comp _ hf

Premises used: Function.Surjective.isEmbedding_comp
-- Module: Mathlib.Algebra.Category.Ring.Topology
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 : 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:
exact Function.Surjective.isEmbedding_comp _ hf

Premises used: Function.Surjective.isEmbedding_comp
-- Module: Mathlib.Algebra.Category.Ring.Topology
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

Tactic:
⟨isEmbedding_precomp_of_surjective f hf, ?_⟩

Premises used: CommRingCat.HomTopology.isEmbedding_precomp_of_surjective, Topology.IsClosedEmbedding.mk
-- Module: Mathlib.Algebra.Category.Ring.Topology
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))
refine : IsClosed[instTopologicalSpaceHom] (Set.range fun (x : B ⟶ R) ↦ f ≫ x)
⊢ IsClosedEmbedding (Y := A ⟶ R) fun (x : B ⟶ R) ↦ f ≫ x

Tactic:
refine ⟨isEmbedding_precomp_of_surjective f hf, ?_⟩
-- Module: Mathlib.Algebra.Category.Ring.Topology
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]
    (⋂ (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)
-- Module: Mathlib.Algebra.Category.Ring.Topology
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]
    (⋂ (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:
this
-- Module: Mathlib.Algebra.Category.Ring.Topology
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))})
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))})
⊢ IsClosed[instTopologicalSpaceHom] (Set.range fun (x : B ⟶ R) ↦ f ≫ x)

Tactic:
convert! this
-- Module: Mathlib.Algebra.Category.Ring.Topology
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))})
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
⊢ 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:
ext x
-- Module: Mathlib.Algebra.Category.Ring.Topology
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))})
x : A ⟶ R
h :
  (∃ (y : B ⟶ R), f ≫ y = x) ↔
    ∀ (a : (↑A : Type u))
      (b :
        Eq (α := (↑B : Type u)) ((Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) a : (↑B : Type u))
          (0 : (↑B : Type u))),
      Eq (α := (↑R : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) x :
              (a : (↑A : Type u)) → (↑R : Type u))
            a :
          (↑R : Type u))
        (0 : (↑R : Type u))
⊢ 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:
simp only [Set.mem_range, Set.mem_iInter, Set.mem_setOf_eq, Subtype.forall, RingHom.mem_ker]

Premises used: Set.mem_range, RingHom.mem_ker, Subtype.forall, Set.mem_setOf_eq, Set.mem_iInter
-- Module: Mathlib.Algebra.Category.Ring.Topology
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))})
x : A ⟶ R
h :
  (∃ (y : B ⟶ R), f ≫ y = x) →
    ∀ (a : (↑A : Type u))
      (b :
        Eq (α := (↑B : Type u)) ((Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) a : (↑B : Type u))
          (0 : (↑B : Type u))),
      Eq (α := (↑R : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) x :
              (a : (↑A : Type u)) → (↑R : Type u))
            a :
          (↑R : Type u))
        (0 : (↑R : Type u))
h₁ :
  (∀ (a : (↑A : Type u))
      (b :
        Eq (α := (↑B : Type u)) ((Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) a : (↑B : Type u))
          (0 : (↑B : Type u))),
      Eq (α := (↑R : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) x :
              (a : (↑A : Type u)) → (↑R : Type u))
            a :
          (↑R : Type u))
        (0 : (↑R : Type u))) →
    ∃ (y : B ⟶ R), f ≫ y = x
⊢ (∃ (y : B ⟶ R), f ≫ y = x) ↔
    ∀ (a : (↑A : Type u))
      (b :
        Eq (α := (↑B : Type u)) ((Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) a : (↑B : Type u))
          (0 : (↑B : Type u))),
      Eq (α := (↑R : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) x :
              (a : (↑A : Type u)) → (↑R : Type u))
            a :
          (↑R : Type u))
        (0 : (↑R : Type u))

Tactic:
constructor
-- Module: Mathlib.Algebra.Category.Ring.Topology
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))})
g : B ⟶ R
a : (↑A : Type u)
ha : Eq (α := (↑B : Type u)) ((Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) a : (↑B : Type u)) (0 : (↑B : Type u))
⊢ Eq (α := (↑R : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
            (f ≫ g) :
          (a : (↑A : Type u)) → (↑R : Type u))
        a :
      (↑R : Type u))
    (0 : (↑R : Type u))

Tactic:
simp [ha]
-- Module: Mathlib.Algebra.Category.Ring.Topology
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))})
x : A ⟶ R
H :
  ∀ (a : (↑A : Type u))
    (b :
      Eq (α := (↑B : Type u)) ((Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) a : (↑B : Type u))
        (0 : (↑B : Type u))),
    Eq (α := (↑R : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) x :
            (a : (↑A : Type u)) → (↑R : Type u))
          a :
        (↑R : Type u))
      (0 : (↑R : Type u))
hf₁ :
  ∀ (x_1 : (↑A : Type u)),
    Eq (α := (↑R : Type u))
      ((Hom.hom
              (f ≫
                ofHom
                  (((Hom.hom f).liftOfSurjective hf :
                      (a : { g : (↑A : Type u) →+* (↑R : Type u) // RingHom.ker (Hom.hom f) ≤ RingHom.ker g }) →
                        (↑B : Type u) →+* (↑R : Type u))
                    (Subtype.mk (p := fun (g : (↑A : Type u) →+* (↑R : Type u)) ↦
                      LE.le (α := Ideal (↑A : Type u)) (RingHom.ker (Hom.hom f)) (RingHom.ker g)) (Hom.hom x) H))) :
            (a : (↑A : Type u)) → (↑R : Type u))
          x_1 :
        (↑R : Type u))
      ((Hom.hom x : (a : (↑A : Type u)) → (↑R : Type u)) x_1 : (↑R : Type u))
⊢ f ≫
      ofHom
        (((Hom.hom f).liftOfSurjective hf :
            (a : { g : (↑A : Type u) →+* (↑R : Type u) // RingHom.ker (Hom.hom f) ≤ RingHom.ker g }) →
              (↑B : Type u) →+* (↑R : Type u))
          (Subtype.mk (p := fun (g : (↑A : Type u) →+* (↑R : Type u)) ↦
            LE.le (α := Ideal (↑A : Type u)) (RingHom.ker (Hom.hom f)) (RingHom.ker g)) (Hom.hom x) H)) =
    x

Tactic:
ext
-- Module: Mathlib.Algebra.Category.Ring.Topology
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))})
x : A ⟶ R
H :
  ∀ (a : (↑A : Type u))
    (b :
      Eq (α := (↑B : Type u)) ((Hom.hom f : (a : (↑A : Type u)) → (↑B : Type u)) a : (↑B : Type u))
        (0 : (↑B : Type u))),
    Eq (α := (↑R : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) x :
            (a : (↑A : Type u)) → (↑R : Type u))
          a :
        (↑R : Type u))
      (0 : (↑R : Type u))
x_1 : (↑A : Type u)
⊢ Eq (α := (↑R : Type u))
    ((Hom.hom
            (f ≫
              ofHom
                (((Hom.hom f).liftOfSurjective hf :
                    (a : { g : (↑A : Type u) →+* (↑R : Type u) // RingHom.ker (Hom.hom f) ≤ RingHom.ker g }) →
                      (↑B : Type u) →+* (↑R : Type u))
                  (Subtype.mk (p := fun (g : (↑A : Type u) →+* (↑R : Type u)) ↦
                    LE.le (α := Ideal (↑A : Type u)) (RingHom.ker (Hom.hom f)) (RingHom.ker g)) (Hom.hom x) H))) :
          (a : (↑A : Type u)) → (↑R : Type u))
        x_1 :
      (↑R : Type u))
    ((Hom.hom x : (a : (↑A : Type u)) → (↑R : Type u)) x_1 : (↑R : Type u))

Tactic:
simp [RingHom.liftOfRightInverse_comp_apply]

Premises used: RingHom.liftOfRightInverse_comp_apply