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)
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
rw :
  ∀ (hx : 1 ∈ 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))
    (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),
    Membership.mem (γ := Ideal S) (conductor R x ⊔ Ideal.map (F := R →+* S) (algebraMap R S) I) 1
⊢ Eq (α := Ideal S) (conductor R x ⊔ Ideal.map (F := R →+* S) (algebraMap R S) I) ⊤

Tactic:
rw [Ideal.eq_top_iff_one] at hx ⊢

Premises used: Ideal.eq_top_iff_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 : 1 ∈ 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
⊢ Membership.mem.{u_2, u_2} (α := S) (γ := Ideal S)
    (Ideal.map (F := R →+* S) (algebraMap R S) (comap (F := R →+* S) (algebraMap R S) (conductor R x) ⊔ I))
    ((algebraMap R S : (a : R) → S) 1 : S)

Tactic:
replace hx := Ideal.mem_map_of_mem (algebraMap R S) hx
-- 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
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
hx :
  Membership.mem.{u_2, u_2} (α := S) (γ := Ideal S)
    (Ideal.map (F := R →+* S) (algebraMap R S) (comap (F := R →+* S) (algebraMap R S) (conductor R x) ⊔ I))
    ((algebraMap R S : (a : R) → S) 1 : S)
⊢ Membership.mem (γ := Ideal S)
    (Ideal.map (F := R →+* S) (algebraMap R S) (comap (F := R →+* S) (algebraMap R S) (conductor R x)) ⊔
      Ideal.map (F := R →+* S) (algebraMap R S) I)
    1

Tactic:
rw [Ideal.map_sup, map_one] at hx

Premises used: Ideal.map_sup, map_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
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
hx :
  Membership.mem (γ := Ideal S)
    (Ideal.map (F := R →+* S) (algebraMap R S) (comap (F := R →+* S) (algebraMap R S) (conductor R x)) ⊔
      Ideal.map (F := R →+* S) (algebraMap R S) I)
    1
⊢ Membership.mem (γ := Ideal S) (conductor R x ⊔ Ideal.map (F := R →+* S) (algebraMap R S) I) 1

Tactic:
(sup_le_sup
        (show ((conductor R x).comap (algebraMap R S)).map (algebraMap R S) ≤ conductor R x
          from Ideal.map_comap_le)
          (le_refl (I.map (algebraMap R S)))) hx

Premises used: le_refl, sup_le_sup, Algebra.algebraMap, Set.Mem, Ideal.map, Ideal.map_comap_le
-- 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
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
hx :
  Membership.mem (γ := Ideal S)
    (Ideal.map (F := R →+* S) (algebraMap R S) (comap (F := R →+* S) (algebraMap R S) (conductor R x)) ⊔
      Ideal.map (F := R →+* S) (algebraMap R S) I)
    1
⊢ Membership.mem (γ := Ideal S) (conductor R x ⊔ Ideal.map (F := R →+* S) (algebraMap R S) I) 1

Tactic:
exact (sup_le_sup
        (show ((conductor R x).comap (algebraMap R S)).map (algebraMap R S) ≤ conductor R x
          from Ideal.map_comap_le)
          (le_refl (I.map (algebraMap R S)))) hx

Premises used: le_refl, sup_le_sup, Algebra.algebraMap, Ideal.map, Ideal.map_comap_le
-- 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
⊢ Membership.mem (γ := Ideal S) (conductor R x ⊔ Ideal.map (F := R →+* S) (algebraMap R S) I) z

Tactic:
have : z ∈ conductor R x ⊔ I.map (algebraMap R S) := by
      suffices conductor R x ⊔ I.map (algebraMap R S) = ⊤ by simp only [this, Submodule.mem_top]
      rw [Ideal.eq_top_iff_one] at hx ⊢
      replace hx := Ideal.mem_map_of_mem (algebraMap R S) hx
      rw [Ideal.map_sup, map_one] at hx
      exact (sup_le_sup
        (show ((conductor R x).comap (algebraMap R S)).map (algebraMap R S) ≤ conductor R x
          from Ideal.map_comap_le)
          (le_refl (I.map (algebraMap R S)))) hx
-- 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 : Membership.mem (γ := Ideal S) (conductor R x ⊔ Ideal.map (F := R →+* S) (algebraMap R S) I) z
refine_2 :
  ∀
    (this :
      ∃ (x_1 : S),
        Membership.mem (γ := Ideal S) (conductor R x) x_1 ∧
          (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I)
              x_1 =
            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
refine_2₁ :
  ∀
    (this :
      Membership.mem (γ := Ideal (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)))
        (Ideal.map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
          (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I)) (conductor R x))
        y),
    Function.Surjective.{u_2 + 1, u_2 + 1} (α := S) (β :=
      HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
      (⇑(Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I)) : (a : S) → S ⧸ Ideal.map (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

Tactic:
rw [← Ideal.mem_quotient_iff_mem_sup, hz, Ideal.mem_map_iff_of_surjective] at this

Premises used: Ideal.mem_quotient_iff_mem_sup, Ideal.mem_map_iff_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)
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 :
  ∃ (x_1 : S),
    Membership.mem (γ := Ideal S) (conductor R x) x_1 ∧
      (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I)
          x_1 =
        y
refine_2 :
  ∀ (u : S) (hu : Membership.mem (γ := Ideal S) (conductor R x) u)
    (hu' :
      (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I) u =
        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 ⟨u, hu, hu'⟩ := 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)
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
u : S
hu : Membership.mem (γ := Ideal S) (conductor R x) u
hu' :
  (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I) u = y
h :
  (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)
      (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) u ⋯) =
    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:
use ⟨u, conductor_subset_adjoin hu⟩
-- 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
u : S
hu : Membership.mem (γ := Ideal S) (conductor R x) u
hu' :
  (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I) u = y
h :
  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)
        (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) u ⋯) :
      HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
    ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I) u :
      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)
      (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) u ⋯) =
    y

Tactic:
simp only [← hu']
-- 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
u : S
hu : Membership.mem (γ := Ideal S) (conductor R x) u
hu' :
  (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I) u = y
⊢ 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)
        (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) u ⋯) :
      HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
    ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I) u :
      HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))

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)
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 :
  Membership.mem (γ := Ideal (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)))
    (Ideal.map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I)) (conductor R x))
    y
⊢ Function.Surjective.{u_2 + 1, u_2 + 1} (α := S) (β :=
    HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
    (⇑(Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I)) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I)

Tactic:
Ideal.Quotient.mk_surjective

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 :
  Membership.mem (γ := Ideal (HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)))
    (Ideal.map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
      (Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I)) (conductor R x))
    y
⊢ Function.Surjective.{u_2 + 1, u_2 + 1} (α := S) (β :=
    HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
    (⇑(Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I)) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I)

Tactic:
exact Ideal.Quotient.mk_surjective

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)
a : ↥R[x]
⊢ Eq (α := HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
    ((quotAdjoinEquivQuotMap hx h_alg :
          (a : ↥R[x] ⧸ Ideal.map (algebraMap R ↥R[x]) I) → S ⧸ Ideal.map (algebraMap R S) I)
        ((Ideal.Quotient.mk (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) :
            (a : ↥R[x]) → ↥R[x] ⧸ Ideal.map (algebraMap R ↥R[x]) I)
          a) :
      HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
    ((Ideal.Quotient.mk (Ideal.map (F := R →+* S) (algebraMap R S) I) : (a : S) → S ⧸ Ideal.map (algebraMap R S) I)
        (↑a : S) :
      HasQuotient.Quotient S (B := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, 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
P : Ideal S
inst_3 : P.IsPrime
hx : ¬conductor R x ≤ P
s : Subalgebra R S
hs : s = R[x]
p : Ideal ↥s
inst_4 : p.IsPrime
inst_5 : P.LiesOver p
obtain :
  ∀ (a : S) (ha : Membership.mem (γ := Ideal S) (conductor R x) a) (haP : a ∉ P),
    Function.Bijective (α := Localization.AtPrime p) (β := Localization.AtPrime P)
      (⇑(localRingHom p P (algebraMap (↥s) S) ⋯) : (a : Localization.AtPrime p) → Localization.AtPrime P)
⊢ Function.Bijective (α := Localization.AtPrime p) (β := Localization.AtPrime P)
    (⇑(localRingHom p P (algebraMap (↥s) S) ⋯) : (a : Localization.AtPrime p) → Localization.AtPrime P)

Tactic:
obtain ⟨a, ha, haP⟩ := SetLike.not_le_iff_exists.mp hx

Premises used: Iff.mp, SetLike.not_le_iff_exists
-- 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
P : Ideal S
inst_3 : P.IsPrime
hx : ¬conductor R x ≤ P
s : Subalgebra R S
hs : s = R[x]
p : Ideal ↥s
inst_4 : p.IsPrime
inst_5 : P.LiesOver p
a : S
ha : Membership.mem (γ := Ideal S) (conductor R x) a
haP : a ∉ P
b : S
⊢ a * b ∈ s

Tactic:
simpa [hs] using ha b