awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Conductor
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
I : Ideal R
hx : comap (F := R →+* S) (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective (α := ↥R[x]) (β := S) (⇑(algebraMap (↥R[x]) S) : (a : ↥R[x]) → S)
z : S
hz : Membership.mem (γ := Subalgebra R S) R[x] z
hy :
  Membership.mem (γ := Submodule ↥R[x] ↥R[x])
    (comap (F := ↥R[x] →+* S) (algebraMap (↥R[x]) S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
    (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) z hz)
p : R
hp : Membership.mem (γ := Submodule R R) (comap (F := R →+* S) (algebraMap R S) (conductor R x)) p
q : R
hq : q ∈ I
hpq : p + q = 1
temp :
  HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p : S) z +
      HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) q : S) z =
    z
h :
  Membership.mem (γ := Set S)
    ((⇑(algebraMap (↥R[x]) S) : (a : ↥R[x]) → S) ''
      (↑(Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) : Set ↥R[x]))
    z
x₁ : ↥R[x]
hx₁ : x₁ ∈ (↑(Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) : Set ↥R[x])
hx₂ : (algebraMap (↥R[x]) S : (a : ↥R[x]) → S) x₁ = z
a : z = HSMul.hSMul (β := S) z 1
a₁ : z = z * 1
a₂ a₃ : z = z
⊢ z = HSMul.hSMul (β := S) (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) z hz) 1

Tactic:
rw [Submonoid.mk_smul, smul_eq_mul, mul_one]

Premises used: Submonoid.mk_smul, smul_eq_mul, mul_one
-- Module: Mathlib.RingTheory.Conductor
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
I : Ideal R
hx : comap (F := R →+* S) (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective (α := ↥R[x]) (β := S) (⇑(algebraMap (↥R[x]) S) : (a : ↥R[x]) → S)
z : S
hz : Membership.mem (γ := Subalgebra R S) R[x] z
hy :
  Membership.mem (γ := Submodule ↥R[x] ↥R[x])
    (comap (F := ↥R[x] →+* S) (algebraMap (↥R[x]) S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
    (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) z hz)
p : R
hp : Membership.mem (γ := Submodule R R) (comap (F := R →+* S) (algebraMap R S) (conductor R x)) p
q : R
hq : q ∈ I
hpq : p + q = 1
temp :
  HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p : S) z +
      HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) q : S) z =
    z
h :
  Membership.mem (γ := Set S)
    ((⇑(algebraMap (↥R[x]) S) : (a : ↥R[x]) → S) ''
      (↑(Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) : Set ↥R[x]))
    z
x₁ : ↥R[x]
hx₁ : x₁ ∈ (↑(Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) : Set ↥R[x])
hx₂ : (algebraMap (↥R[x]) S : (a : ↥R[x]) → S) x₁ = z
⊢ x₁ = Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) z hz

Tactic:
have : x₁ = ⟨z, hz⟩ := by
      apply h_alg
      simp only [hx₂, algebraMap_eq_smul_one]
      rw [Submonoid.mk_smul, smul_eq_mul, mul_one]
-- Module: Mathlib.RingTheory.Conductor
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
I : Ideal R
hx : comap (F := R →+* S) (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective (α := ↥R[x]) (β := S) (⇑(algebraMap (↥R[x]) S) : (a : ↥R[x]) → S)
z : S
hz : Membership.mem (γ := Subalgebra R S) R[x] z
hy :
  Membership.mem (γ := Submodule ↥R[x] ↥R[x])
    (comap (F := ↥R[x] →+* S) (algebraMap (↥R[x]) S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
    (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) z hz)
p : R
hp : Membership.mem (γ := Submodule R R) (comap (F := R →+* S) (algebraMap R S) (conductor R x)) p
q : R
hq : q ∈ I
hpq : p + q = 1
temp :
  HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p : S) z +
      HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) q : S) z =
    z
h :
  Membership.mem (γ := Set S)
    ((⇑(algebraMap (↥R[x]) S) : (a : ↥R[x]) → S) ''
      (↑(Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) : Set ↥R[x]))
    z
x₁ : ↥R[x]
hx₁ : x₁ ∈ (↑(Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) : Set ↥R[x])
hx₂ : (algebraMap (↥R[x]) S : (a : ↥R[x]) → S) x₁ = z
this : x₁ = Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) z hz
a a₁ a₂ a₃ : Membership.mem (γ := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) x₁
⊢ Membership.mem (γ := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I)
    (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) z hz)

Tactic:
rwa [← this]
-- Module: Mathlib.RingTheory.Conductor
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
I : Ideal R
hx : comap (F := R →+* S) (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective (α := ↥R[x]) (β := S) (⇑(algebraMap (↥R[x]) S) : (a : ↥R[x]) → S)
a :
  LE.le (α := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I)
    (comap (F := ↥R[x] →+* S) (algebraMap (↥R[x]) S)
      (Ideal.map (R := ↥R[x]) (F := ↥R[x] →+* S) (algebraMap (↥R[x]) S)
        (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I)))
⊢ LE.le (α := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I)
    (comap (F := ↥R[x] →+* S) (algebraMap (↥R[x]) S) (Ideal.map (F := R →+* S) (algebraMap R S) I))

Tactic:
rw [IsScalarTower.algebraMap_eq R R<x> S, ← Ideal.map_map]

Premises used: Ideal.map_map
-- Module: Mathlib.RingTheory.Conductor
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
I : Ideal R
hx : comap (F := R →+* S) (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective (α := ↥R[x]) (β := S) (⇑(algebraMap (↥R[x]) S) : (a : ↥R[x]) → S)
⊢ LE.le (α := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I)
    (comap (F := ↥R[x] →+* S) (algebraMap (↥R[x]) S)
      (Ideal.map (R := ↥R[x]) (F := ↥R[x] →+* S) (algebraMap (↥R[x]) S)
        (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I)))

Tactic:
apply Ideal.le_comap_map

Premises used: Ideal.le_comap_map
-- Module: Mathlib.RingTheory.Conductor
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
I : Ideal R
hx : comap (F := R →+* S) (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective (α := ↥R[x]) (β := S) (⇑(algebraMap (↥R[x]) S) : (a : ↥R[x]) → S)
r : ↥R[x]
hr : Membership.mem (γ := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) r
a :
  ∀ (x_1 : R),
    Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x_1 : S)
      ((@RingHom.comp _ ↥R[x] _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥R[x]) S) (algebraMap R ↥R[x]) :
            (a : R) → S)
          x_1 :
        S)
⊢ Eq (α := R →+* S) (algebraMap R S)
    (@RingHom.comp _ ↥R[x] _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥R[x]) S) (algebraMap R ↥R[x]))

Tactic:
ext
-- Module: Mathlib.RingTheory.Conductor
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
I : Ideal R
hx : comap (F := R →+* S) (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective (α := ↥R[x]) (β := S) (⇑(algebraMap (↥R[x]) S) : (a : ↥R[x]) → S)
r : ↥R[x]
hr : Membership.mem (γ := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) r
x_1 : R
⊢ Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) x_1 : S)
    ((@RingHom.comp _ ↥R[x] _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥R[x]) S) (algebraMap R ↥R[x]) : (a : R) → S)
        x_1 :
      S)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Conductor
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
I : Ideal R
hx : comap (F := R →+* S) (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective (α := ↥R[x]) (β := S) (⇑(algebraMap (↥R[x]) S) : (a : ↥R[x]) → S)
r : ↥R[x]
hr : Membership.mem (γ := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) r
⊢ Eq (α := R →+* S) (algebraMap R S)
    (@RingHom.comp _ ↥R[x] _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥R[x]) S) (algebraMap R ↥R[x]))

Tactic:
have : algebraMap R S = (algebraMap R<x> S).comp (algebraMap R R<x>) := by ext; rfl
-- Module: Mathlib.RingTheory.Conductor
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
I : Ideal R
hx : comap (F := R →+* S) (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective (α := ↥R[x]) (β := S) (⇑(algebraMap (↥R[x]) S) : (a : ↥R[x]) → S)
r : ↥R[x]
hr : Membership.mem (γ := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) r
this :
  Eq (α := R →+* S) (algebraMap R S)
    (@RingHom.comp _ ↥R[x] _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥R[x]) S) (algebraMap R ↥R[x]))
rw :
  Membership.mem (α := S) (γ := Ideal S)
    (Ideal.map (R := ↥R[x]) (F := ↥R[x] →+* S) (algebraMap (↥R[x]) S)
      (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I))
    ((algebraMap (↥R[x]) S : (a : ↥R[x]) → S) r : S)
⊢ Eq (α := HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
    ((RingHom.comp (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I)) (algebraMap (↥R[x]) S) :
          (a : ↥R[x]) → S ⧸ Ideal.map (algebraMap R S) I)
        r :
      HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
    (0 : HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))

Tactic:
rw [RingHom.comp_apply, Ideal.Quotient.eq_zero_iff_mem, this, ← Ideal.map_map]

Premises used: Ideal.Quotient.eq_zero_iff_mem, Ideal.map_map, RingHom.comp_apply
-- Module: Mathlib.RingTheory.Conductor
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
I : Ideal R
hx : comap (F := R →+* S) (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective (α := ↥R[x]) (β := S) (⇑(algebraMap (↥R[x]) S) : (a : ↥R[x]) → S)
r : ↥R[x]
hr : Membership.mem (γ := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) r
this :
  Eq (α := R →+* S) (algebraMap R S)
    (@RingHom.comp _ ↥R[x] _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥R[x]) S) (algebraMap R ↥R[x]))
⊢ Membership.mem (α := S) (γ := Ideal S)
    (Ideal.map (R := ↥R[x]) (F := ↥R[x] →+* S) (algebraMap (↥R[x]) S)
      (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I))
    ((algebraMap (↥R[x]) S : (a : ↥R[x]) → S) r : S)

Tactic:
Ideal.mem_map_of_mem _ hr

Premises used: Ideal.mem_map_of_mem, Set.Mem
-- Module: Mathlib.RingTheory.Conductor
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
I : Ideal R
hx : comap (F := R →+* S) (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective (α := ↥R[x]) (β := S) (⇑(algebraMap (↥R[x]) S) : (a : ↥R[x]) → S)
r : ↥R[x]
hr : Membership.mem (γ := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) r
this :
  Eq (α := R →+* S) (algebraMap R S)
    (@RingHom.comp _ ↥R[x] _ _ Semiring.toNonAssocSemiring _ (algebraMap (↥R[x]) S) (algebraMap R ↥R[x]))
⊢ Membership.mem (α := S) (γ := Ideal S)
    (Ideal.map (R := ↥R[x]) (F := ↥R[x] →+* S) (algebraMap (↥R[x]) S)
      (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I))
    ((algebraMap (↥R[x]) S : (a : ↥R[x]) → S) r : S)

Tactic:
exact Ideal.mem_map_of_mem _ hr

Premises used: Ideal.mem_map_of_mem
-- Module: Mathlib.RingTheory.Conductor
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
I : Ideal R
hx : comap (F := R →+* S) (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective (α := ↥R[x]) (β := S) (⇑(algebraMap (↥R[x]) S) : (a : ↥R[x]) → S)
f : HasQuotient.Quotient ↥R[x] (B := Ideal ↥R[x])
    (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) →+*
  HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) :=
  Ideal.Quotient.lift (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I)
    (RingHom.comp (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I)) (algebraMap (↥R[x]) S)) ⋯
refine_1 :
  Function.Injective (α :=
    HasQuotient.Quotient ↥R[x] (B := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I))
    (β := HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
    (⇑f : (a : ↥R[x] ⧸ Ideal.map (algebraMap R ↥R[x]) I) → S ⧸ Ideal.map (algebraMap R S) I)
refine_2 :
  Function.Surjective (α :=
    HasQuotient.Quotient ↥R[x] (B := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I))
    (β := HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
    (⇑f : (a : ↥R[x] ⧸ Ideal.map (algebraMap R ↥R[x]) I) → S ⧸ Ideal.map (algebraMap R S) I)
⊢ HasQuotient.Quotient ↥R[x] (B := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) ≃+*
    HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)

Tactic:
refine RingEquiv.ofBijective f ⟨?_, ?_⟩

Premises used: RingEquiv.ofBijective, And.intro
-- Module: Mathlib.RingTheory.Conductor
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
I : Ideal R
hx : comap (F := R →+* S) (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective (α := ↥R[x]) (β := S) (⇑(algebraMap (↥R[x]) S) : (a : ↥R[x]) → S)
f : HasQuotient.Quotient ↥R[x] (B := Ideal ↥R[x])
    (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) →+*
  HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) :=
  Ideal.Quotient.lift (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I)
    (RingHom.comp (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I)) (algebraMap (↥R[x]) S)) ⋯
⊢ Function.Injective (α :=
    HasQuotient.Quotient ↥R[x] (B := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I))
    (β := HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
    (⇑f : (a : ↥R[x] ⧸ Ideal.map (algebraMap R ↥R[x]) I) → S ⧸ Ideal.map (algebraMap R S) I)

Tactic:
RingHom.lift_injective_of_ker_le_ideal _ _ fun u hu => ?_

Premises used: Subsemiring.mk', Subsemiring.closure, Set.Mem, setOf, RingHom.lift_injective_of_ker_le_ideal
-- Module: Mathlib.RingTheory.Conductor
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
I : Ideal R
hx : comap (F := R →+* S) (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective (α := ↥R[x]) (β := S) (⇑(algebraMap (↥R[x]) S) : (a : ↥R[x]) → S)
f : HasQuotient.Quotient ↥R[x] (B := Ideal ↥R[x])
    (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) →+*
  HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) :=
  Ideal.Quotient.lift (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I)
    (RingHom.comp (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I)) (algebraMap (↥R[x]) S)) ⋯
refine_1 :
  ∀ (u : ↥R[x])
    (hu :
      Membership.mem (γ := Submodule ↥R[x] ↥R[x])
        (ker (F := ↥R[x] →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
          (RingHom.comp (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I)) (algebraMap (↥R[x]) S)))
        u),
    Membership.mem (γ := Submodule ↥R[x] ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) u
⊢ Function.Injective (α :=
    HasQuotient.Quotient ↥R[x] (B := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I))
    (β := HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
    (⇑f : (a : ↥R[x] ⧸ Ideal.map (algebraMap R ↥R[x]) I) → S ⧸ Ideal.map (algebraMap R S) I)

Tactic:
refine RingHom.lift_injective_of_ker_le_ideal _ _ fun u hu => ?_

Premises used: RingHom.lift_injective_of_ker_le_ideal
-- Module: Mathlib.RingTheory.Conductor
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
I : Ideal R
hx : comap (F := R →+* S) (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective (α := ↥R[x]) (β := S) (⇑(algebraMap (↥R[x]) S) : (a : ↥R[x]) → S)
f : HasQuotient.Quotient ↥R[x] (B := Ideal ↥R[x])
    (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) →+*
  HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) :=
  Ideal.Quotient.lift (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I)
    (RingHom.comp (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I)) (algebraMap (↥R[x]) S)) ⋯
⊢ Function.Surjective (α :=
    HasQuotient.Quotient ↥R[x] (B := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I))
    (β := HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
    (⇑f : (a : ↥R[x] ⧸ Ideal.map (algebraMap R ↥R[x]) I) → S ⧸ Ideal.map (algebraMap R S) I)

Tactic:
Ideal.Quotient.lift_surjective_of_surjective _ _ fun y => ?_

Premises used: Subsemiring.mk', Subsemiring.closure, Set.Mem, Ideal.Quotient.lift_surjective_of_surjective, setOf
-- Module: Mathlib.RingTheory.Conductor
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
I : Ideal R
hx : comap (F := R →+* S) (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective (α := ↥R[x]) (β := S) (⇑(algebraMap (↥R[x]) S) : (a : ↥R[x]) → S)
f : HasQuotient.Quotient ↥R[x] (B := Ideal ↥R[x])
    (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) →+*
  HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) :=
  Ideal.Quotient.lift (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I)
    (RingHom.comp (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I)) (algebraMap (↥R[x]) S)) ⋯
refine_2 :
  ∀ (y : HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)),
    ∃ (a : ↥R[x]),
      (RingHom.comp (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I)) (algebraMap (↥R[x]) S) :
            (a : ↥R[x]) → S ⧸ Ideal.map (algebraMap R S) I)
          a =
        y
⊢ Function.Surjective (α :=
    HasQuotient.Quotient ↥R[x] (B := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I))
    (β := HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
    (⇑f : (a : ↥R[x] ⧸ Ideal.map (algebraMap R ↥R[x]) I) → S ⧸ Ideal.map (algebraMap R S) I)

Tactic:
refine Ideal.Quotient.lift_surjective_of_surjective _ _ fun y => ?_

Premises used: Ideal.Quotient.lift_surjective_of_surjective
-- Module: Mathlib.RingTheory.Conductor
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
I : Ideal R
hx : comap (F := R →+* S) (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective (α := ↥R[x]) (β := S) (⇑(algebraMap (↥R[x]) S) : (a : ↥R[x]) → S)
f : HasQuotient.Quotient ↥R[x] (B := Ideal ↥R[x])
    (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) →+*
  HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) :=
  Ideal.Quotient.lift (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I)
    (RingHom.comp (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I)) (algebraMap (↥R[x]) S)) ⋯
y : HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
refine_2 :
  ∀ (z : S)
    (hz :
      (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I) z =
        y),
    ∃ (a : ↥R[x]),
      (RingHom.comp (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I)) (algebraMap (↥R[x]) S) :
            (a : ↥R[x]) → S ⧸ Ideal.map (algebraMap R S) I)
          a =
        y
⊢ ∃ (a : ↥R[x]),
    (RingHom.comp (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I)) (algebraMap (↥R[x]) S) :
          (a : ↥R[x]) → S ⧸ Ideal.map (algebraMap R S) I)
        a =
      y

Tactic:
obtain ⟨z, hz⟩ := Ideal.Quotient.mk_surjective y

Premises used: Ideal.Quotient.mk_surjective
-- Module: Mathlib.RingTheory.Conductor
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
I : Ideal R
hx : comap (F := R →+* S) (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective (α := ↥R[x]) (β := S) (⇑(algebraMap (↥R[x]) S) : (a : ↥R[x]) → S)
f : HasQuotient.Quotient ↥R[x] (B := Ideal ↥R[x])
    (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) →+*
  HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) :=
  Ideal.Quotient.lift (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I)
    (RingHom.comp (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I)) (algebraMap (↥R[x]) S)) ⋯
y : HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
z : S
hz :
  (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I) z = y
this : Eq (α := Ideal S) (conductor R x ⊔ Ideal.map (F := R →+* S) (algebraMap R S) I) ⊤
⊢ Membership.mem (γ := Ideal S) (conductor R x ⊔ Ideal.map (F := R →+* S) (algebraMap R S) I) z

Tactic:
simp only [this, Submodule.mem_top]

Premises used: Submodule.mem_top
-- Module: Mathlib.RingTheory.Conductor
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
I : Ideal R
hx : comap (F := R →+* S) (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective (α := ↥R[x]) (β := S) (⇑(algebraMap (↥R[x]) S) : (a : ↥R[x]) → S)
f : HasQuotient.Quotient ↥R[x] (B := Ideal ↥R[x])
    (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) →+*
  HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) :=
  Ideal.Quotient.lift (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I)
    (RingHom.comp (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I)) (algebraMap (↥R[x]) S)) ⋯
y : HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
z : S
hz :
  (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I) z = y
suffices : Eq (α := Ideal S) (conductor R x ⊔ Ideal.map (F := R →+* S) (algebraMap R S) I) ⊤
⊢ Membership.mem (γ := Ideal S) (conductor R x ⊔ Ideal.map (F := R →+* S) (algebraMap R S) I) z

Tactic:
suffices conductor R x ⊔ I.map (algebraMap R S) = ⊤ by simp only [this, Submodule.mem_top]