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
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
simp :
  HMul.hMul (α := S) (β := S)
      ((algebraMap (↥R[x]) S : (a : ↥R[x]) → S) ((algebraMap R ↥R[x] : (a : R) → ↥R[x]) q : ↥R[x]) : S)
      ((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) =
    HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) q : S) z
⊢ (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

Tactic:
simp only [ha.right, map_add, map_mul, add_right_inj]

Premises used: map_add, map_mul, And.right, add_right_inj
-- 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
⊢ HMul.hMul (α := S) (β := S)
      ((algebraMap (↥R[x]) S : (a : ↥R[x]) → S) ((algebraMap R ↥R[x] : (a : R) → ↥R[x]) q : ↥R[x]) : S)
      ((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) =
    HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) q : S) z

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

Tactic:
refine ⟨Ideal.add_mem (I.map (algebraMap R R<x>)) ha.left ?_, by
          simp only [ha.right, map_add, map_mul, add_right_inj]; 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)
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 :
  Membership.mem (γ := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I)
    (HMul.hMul (β := ↥R[x]) (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) z hz)
      ((algebraMap R ↥R[x] : (a : R) → ↥R[x]) q : ↥R[x]))
⊢ Membership.mem (γ := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I)
    (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))

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- 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
⊢ Membership.mem (γ := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I)
    (HMul.hMul (β := ↥R[x]) (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) z hz)
      ((algebraMap R ↥R[x] : (a : R) → ↥R[x]) q : ↥R[x]))

Tactic:
Ideal.mul_mem_left (I.map (algebraMap R R<x>)) _ (Ideal.mem_map_of_mem _ hq)

Premises used: Algebra.algebraMap, Ideal.mem_map_of_mem, Set.Mem, setOf, Algebra.adjoin, Membership.mem, Subtype, Ideal.map, Ideal.mul_mem_left, Singleton.singleton
-- 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
⊢ Membership.mem (γ := Ideal ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I)
    (HMul.hMul (β := ↥R[x]) (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) z hz)
      ((algebraMap R ↥R[x] : (a : R) → ↥R[x]) q : ↥R[x]))

Tactic:
exact Ideal.mul_mem_left (I.map (algebraMap R R<x>)) _ (Ideal.mem_map_of_mem _ hq)
-- 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
a :
  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 (γ := 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:
suffices z ∈ algebraMap R<x> S '' I.map (algebraMap R R<x>) ↔
        (⟨z, hz⟩ : R<x>) ∈ I.map (algebraMap R R<x>) by
      rw [← this, ← temp]
      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))
      use a + algebraMap R R<x> q * ⟨z, hz⟩
      refine ⟨Ideal.add_mem (I.map (algebraMap R R<x>)) ha.left ?_, by
          simp only [ha.right, map_add, map_mul, add_right_inj]; rfl⟩
      rw [mul_comm]
      exact Ideal.mul_mem_left (I.map (algebraMap R R<x>)) _ (Ideal.mem_map_of_mem _ hq)
-- 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 (γ := 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)
⊢ 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])

Tactic:
simp [h]
-- 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
a :
  ∀
    (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),
    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 (γ := 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)

Tactic:
refine ⟨fun h => ?_,
      fun h => (Set.mem_image _ _ _).mpr (Exists.intro ⟨z, hz⟩ ⟨by simp [h], 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)
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
a :
  ∀ (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),
    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 ↥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 ⟨x₁, hx₁, hx₂⟩ := (Set.mem_image _ _ _).mp h

Premises used: 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
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 :
  Eq (α := S) ((algebraMap (↥R[x]) S : (a : ↥R[x]) → S) x₁ : S)
    ((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)
⊢ x₁ = Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) z hz

Tactic:
apply h_alg
-- 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) (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1) z hz) 1
⊢ Eq (α := S) ((algebraMap (↥R[x]) S : (a : ↥R[x]) → S) x₁ : S)
    ((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)

Tactic:
simp only [hx₂, algebraMap_eq_smul_one]

Premises used: Algebra.algebraMap_eq_smul_one