awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Conductor (goal)
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))
⊢ 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]))
    (l.sum 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))
have refine_1 : ∀ (a b : 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)
      a →
    (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)
        b →
      (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)
        (a + b)
Tactic: refine Finset.sum_induction _ (fun u => u ∈ algebraMap R<x> S '' I.map (algebraMap R R<x>))
      (fun a b => ?_) ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Conductor (goal)
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))
refine_1 :
  ∀ (a b : 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)
        a →
      (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)
          b →
        (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)
          (a + b)
⊢ 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]))
    (l.sum 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))
have refine_2 : (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: refine Finset.sum_induction _ (fun u => u ∈ algebraMap R<x> S '' I.map (algebraMap R R<x>))
      (fun a b => ?_) ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Conductor (goal)
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))
refine_1 :
  ∀ (a b : 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)
        a →
      (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)
          b →
        (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)
          (a + b)
refine_2 :
  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]))
    0
⊢ 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]))
    (l.sum 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))
have refine_3 : ∀ x_1 ∈ l.support,
  (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)
    ((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))
      x_1 ((l : (a : R) → S) x_1))
Tactic: refine Finset.sum_induction _ (fun u => u ∈ algebraMap R<x> S '' I.map (algebraMap R R<x>))
      (fun a b => ?_) ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Conductor (goal)
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 (γ := 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]))
    (HAdd.hAdd (α := S) (β := S) ((algebraMap (↥R[x]) S : (a : ↥R[x]) → S) z : S)
      ((algebraMap (↥R[x]) S : (a : ↥R[x]) → S) y : S))
have refine_1 : 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: rw [← map_add]
-- Lean 4 proof step from Mathlib.RingTheory.Conductor (goal)
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)
⊢ 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)
have 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)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.Conductor (goal)
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)
⊢ 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)
have 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))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.Conductor (goal)
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
⊢ Membership.mem (γ := Submodule ↥R[x] ↥R[x]) (Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) y
have 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)
Tactic: obtain ⟨z, hz⟩ := y
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.RingTheory.Conductor (goal)
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)
⊢ 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)
have 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)
Tactic: obtain ⟨p, hp, q, hq, hpq⟩ := Submodule.mem_sup.mp ((Ideal.eq_top_iff_one _).mp hx)
-- Lean 4 proof step from Mathlib.RingTheory.Conductor (hypothesis)
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
⊢ 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)
have 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
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]
-- Lean 4 proof step from Mathlib.RingTheory.Conductor (goal)
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)
⊢ 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)
have 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)
Tactic: rw [← this, ← temp]
-- Lean 4 proof step from Mathlib.RingTheory.Conductor (goal)
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)
⊢ Membership.mem (γ := Ideal S) (Ideal.map (F := R →+* S) (algebraMap R S) I) z
have 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
Tactic: rwa [Ideal.mem_comap] at hy
Cleared hypotheses: hy, p, hp, q, hq, hpq, temp, this
-- Lean 4 proof step from Mathlib.RingTheory.Conductor (goal)
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)
⊢ 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)
have 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)
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))
-- Lean 4 proof step from Mathlib.RingTheory.Conductor (goal)
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 (γ := 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)
have 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
Tactic: use a + algebraMap R R<x> q * ⟨z, hz⟩