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
p : R
z_1 : S
hp : Membership.mem (γ := Ideal R) (comap (F := R →+* S) (algebraMap R S) (conductor R x)) p
l : R →₀ S
H : Membership.mem (γ := Submodule S (R →₀ S)) (Finsupp.supported S S (↑I : Set R)) l
H' : (l.sum fun (i : R) (a : S) ↦ HSMul.hSMul (β := S) a ((algebraMap R S : (a : R) → S) i : S)) = z_1
lem :
  ∀ {a : R},
    a ∈ I →
      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]))
        (HMul.hMul (β := S)
          (HSMul.hSMul (α := S) (β := S) ((l : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) a : S))
          ((algebraMap R S : (a : R) → S) p : S))
z : ↥R[x]
hz : z ∈ (↑(Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) : Set ↥R[x])
y : ↥R[x]
hy : y ∈ (↑(Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) : Set ↥R[x])
⊢ Membership.mem (α := S) (γ := 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]))
    ((algebraMap (↥R[x]) S : (a : ↥R[x]) → S) (z + y) : S)

Tactic:
⟨z + y, Ideal.add_mem _ (SetLike.mem_coe.mp hz) hy, rfl⟩

Premises used: Set.Mem, setOf, Ideal.add_mem, HAdd.hAdd, SetLike.mem_coe, And.intro, Exists.intro, Iff.mp, Set.image, 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
p : R
z_1 : S
hp : Membership.mem (γ := Ideal R) (comap (F := R →+* S) (algebraMap R S) (conductor R x)) p
l : R →₀ S
H : Membership.mem (γ := Submodule S (R →₀ S)) (Finsupp.supported S S (↑I : Set R)) l
H' : (l.sum fun (i : R) (a : S) ↦ HSMul.hSMul (β := S) a ((algebraMap R S : (a : R) → S) i : S)) = z_1
lem :
  ∀ {a : R},
    a ∈ I →
      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]))
        (HMul.hMul (β := S)
          (HSMul.hSMul (α := S) (β := S) ((l : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) a : S))
          ((algebraMap R S : (a : R) → S) p : S))
z : ↥R[x]
hz : z ∈ (↑(Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) : Set ↥R[x])
y : ↥R[x]
hy : y ∈ (↑(Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) : Set ↥R[x])
⊢ Membership.mem (α := S) (γ := 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]))
    ((algebraMap (↥R[x]) S : (a : ↥R[x]) → S) (z + y) : S)

Tactic:
exact ⟨z + y, Ideal.add_mem _ (SetLike.mem_coe.mp hz) hy, 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
p : R
z : S
hp : Membership.mem (γ := Ideal R) (comap (F := R →+* S) (algebraMap R S) (conductor R x)) p
l : R →₀ S
H : Membership.mem (γ := Submodule S (R →₀ S)) (Finsupp.supported S S (↑I : Set R)) l
H' : (l.sum fun (i : R) (a : S) ↦ HSMul.hSMul (β := S) a ((algebraMap R S : (a : R) → S) i : S)) = z
lem :
  ∀ {a : R},
    a ∈ I →
      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]))
        (HMul.hMul (β := S)
          (HSMul.hSMul (α := S) (β := S) ((l : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) a : S))
          ((algebraMap R S : (a : R) → S) p : S))
⊢ (fun (u : S) ↦
      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]))
        u)
    0

Tactic:
⟨0, SetLike.mem_coe.mpr <| Ideal.zero_mem _, map_zero _⟩

Premises used: Iff.mpr, Set.Mem, setOf, map_zero, Ideal.zero_mem, SetLike.mem_coe, And.intro, Exists.intro, Set.image, OfNat.ofNat
-- 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
p : R
z : S
hp : Membership.mem (γ := Ideal R) (comap (F := R →+* S) (algebraMap R S) (conductor R x)) p
l : R →₀ S
H : Membership.mem (γ := Submodule S (R →₀ S)) (Finsupp.supported S S (↑I : Set R)) l
H' : (l.sum fun (i : R) (a : S) ↦ HSMul.hSMul (β := S) a ((algebraMap R S : (a : R) → S) i : S)) = z
lem :
  ∀ {a : R},
    a ∈ I →
      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]))
        (HMul.hMul (β := S)
          (HSMul.hSMul (α := S) (β := S) ((l : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) a : S))
          ((algebraMap R S : (a : R) → S) p : S))
⊢ (fun (u : S) ↦
      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]))
        u)
    0

Tactic:
exact ⟨0, SetLike.mem_coe.mpr <| Ideal.zero_mem _, map_zero _⟩
-- 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
p : R
z : S
hp : Membership.mem (γ := Ideal R) (comap (F := R →+* S) (algebraMap R S) (conductor R x)) p
l : R →₀ S
H : Membership.mem (γ := Submodule S (R →₀ S)) (Finsupp.supported S S (↑I : Set R)) l
H' : (l.sum fun (i : R) (a : S) ↦ HSMul.hSMul (β := S) a ((algebraMap R S : (a : R) → S) i : S)) = z
lem :
  ∀ {a : R},
    a ∈ I →
      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]))
        (HMul.hMul (β := S)
          (HSMul.hSMul (α := S) (β := S) ((l : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) a : S))
          ((algebraMap R S : (a : R) → S) p : S))
y : R
hy : y ∈ l.support
⊢ 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]))
    ((fun (a : R) (c : S) ↦
        HMul.hMul (β := S) (HSMul.hSMul (β := S) c ((algebraMap R S : (a : R) → S) a : S))
          ((algebraMap R S : (a : R) → S) p : S))
      y ((l : (a : R) → S) y))

Tactic:
lem ((Finsupp.mem_supported _ l).mp H hy)

Premises used: Finsupp.mem_supported, Set.Mem, Iff.mp
-- 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
p : R
z : S
hp : Membership.mem (γ := Ideal R) (comap (F := R →+* S) (algebraMap R S) (conductor R x)) p
l : R →₀ S
H : Membership.mem (γ := Submodule S (R →₀ S)) (Finsupp.supported S S (↑I : Set R)) l
H' : (l.sum fun (i : R) (a : S) ↦ HSMul.hSMul (β := S) a ((algebraMap R S : (a : R) → S) i : S)) = z
lem :
  ∀ {a : R},
    a ∈ I →
      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]))
        (HMul.hMul (β := S)
          (HSMul.hSMul (α := S) (β := S) ((l : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) a : S))
          ((algebraMap R S : (a : R) → S) p : S))
y : R
hy : y ∈ l.support
⊢ 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]))
    ((fun (a : R) (c : S) ↦
        HMul.hMul (β := S) (HSMul.hSMul (β := S) c ((algebraMap R S : (a : R) → S) a : S))
          ((algebraMap R S : (a : R) → S) p : S))
      y ((l : (a : R) → S) y))

Tactic:
exact lem ((Finsupp.mem_supported _ l).mp H hy)

Premises used: Finsupp.mem_supported, Iff.mp
-- 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])
    (comap (F := ↥R[x] →+* S) (algebraMap (↥R[x]) S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
    (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I)
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 (F := R →+* S) (algebraMap R S) I))
⊢ Eq (α := Ideal ↥R[x]) (comap (F := ↥R[x] →+* S) (algebraMap (↥R[x]) S) (Ideal.map (F := R →+* S) (algebraMap R S) I))
    (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- 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)
y : ↥R[x]
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)) y
a :
  ∀ (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)),
    Membership.mem (γ := Submodule ↥R[x] ↥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)
⊢ Membership.mem (γ := Submodule ↥R[x] ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) y

Tactic:
obtain ⟨z, hz⟩ := y
-- 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)
a :
  ∀ (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),
    Membership.mem (γ := Submodule ↥R[x] ↥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)
⊢ Membership.mem (γ := Submodule ↥R[x] ↥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:
obtain ⟨p, hp, q, hq, hpq⟩ := Submodule.mem_sup.mp ((Ideal.eq_top_iff_one _).mp hx)

Premises used: Ideal.eq_top_iff_one, Iff.mp, Submodule.mem_sup
-- 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
⊢ 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

Tactic:
simp only [← add_mul, ← map_add (algebraMap R S), hpq, map_one, one_mul]

Premises used: add_mul, Algebra.algebraMap, map_add, map_one, one_mul
-- 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
⊢ 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

Tactic:
have temp : algebraMap R S p * z + algebraMap R S q * z = z := by
      simp only [← add_mul, ← map_add (algebraMap R S), hpq, map_one, one_mul]
-- 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
this :
  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 ↔
    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)
rw :
  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]))
    (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p : S) z +
      HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) q : S) z)
⊢ Membership.mem (γ := Submodule ↥R[x] ↥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:
rw [← this, ← temp]
-- 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
this :
  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 ↔
    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)
rwa rwa₁ rwa₂ rwa₃ :
  ∀
    (hy :
      Membership.mem (α := S) (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I)
        ((algebraMap (↥R[x]) S : (a : ↥R[x]) → S)
            (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) z hz) :
          S))
    (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)
    (this :
      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 ↔
        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)),
    Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) z
⊢ Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) z

Tactic:
rwa [Ideal.mem_comap] at hy

Premises used: Ideal.mem_comap
-- 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
this :
  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 ↔
    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)
obtain :
  ∀ (a : ↥R[x])
    (ha :
      a ∈ (↑(Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) : Set ↥R[x]) ∧
        (algebraMap (↥R[x]) S : (a : ↥R[x]) → S) a = HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p : S) z),
    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]))
      (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p : S) z +
        HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) q : S) z)
⊢ 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]))
    (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p : S) z +
      HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) q : S) z)

Tactic:
obtain ⟨a, ha⟩ := (Set.mem_image _ _ _).mp (prod_mem_ideal_map_of_mem_conductor hp
          (show z ∈ I.map (algebraMap R S) by rwa [Ideal.mem_comap] at hy))

Premises used: prod_mem_ideal_map_of_mem_conductor, Set.mem_image, Iff.mp
-- 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
this :
  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 ↔
    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)
a : ↥R[x]
ha :
  a ∈ (↑(Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) : Set ↥R[x]) ∧
    (algebraMap (↥R[x]) S : (a : ↥R[x]) → S) a = HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p : S) z
h :
  a +
        HMul.hMul (α := ↥R[x]) ((algebraMap R ↥R[x] : (a : R) → ↥R[x]) q : ↥R[x])
          (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) z hz) ∈
      (↑(Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) : Set ↥R[x]) ∧
    (algebraMap (↥R[x]) S : (a : ↥R[x]) → S)
        (a +
          HMul.hMul (α := ↥R[x]) ((algebraMap R ↥R[x] : (a : R) → ↥R[x]) q : ↥R[x])
            (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) z hz)) =
      HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p : S) z +
        HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) q : S) z
⊢ 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]))
    (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) p : S) z +
      HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) q : S) z)

Tactic:
use a + algebraMap R R<x> q * ⟨z, hz⟩