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 : 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
a : R
ha : a ∈ I
rw :
  ∃ x_1 ∈ (↑(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) x_1 =
      HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) a : S)
        (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) p : S) ((l : (a : R) → S) a : 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]))
    (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))

Tactic:
rw [smul_eq_mul, mul_assoc, mul_comm, mul_assoc, Set.mem_image]

Premises used: mul_assoc, Set.mem_image, mul_comm, smul_eq_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
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
a : R
ha : a ∈ I
⊢ ∃ x_1 ∈ (↑(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) x_1 =
      HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) a : S)
        (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) p : S) ((l : (a : R) → S) a : S))

Tactic:
Exists.intro
        (algebraMap R R<x> a * ⟨l a * algebraMap R S p,
          show l a * algebraMap R S p ∈ R<x> from ?h⟩) ?_

Premises used: HMul.hMul, Algebra.algebraMap, Algebra.adjoin, Membership.mem, Subtype, Exists.intro, Singleton.singleton, DFunLike.coe
-- 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
a : R
ha : a ∈ I
refine :
  HMul.hMul (α := ↥R[x]) (β := ↥R[x]) ((algebraMap R ↥R[x] : (a : R) → ↥R[x]) a : ↥R[x])
        (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1)
          (HMul.hMul (α := S) (β := S) ((l : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) p : 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)
        (HMul.hMul (α := ↥R[x]) (β := ↥R[x]) ((algebraMap R ↥R[x] : (a : R) → ↥R[x]) a : ↥R[x])
          (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1)
            (HMul.hMul (α := S) (β := S) ((l : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) p : S)) ⋯)) =
      HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) a : S)
        (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) p : S) ((l : (a : R) → S) a : S))
refine₁ :
  Membership.mem (γ := Subalgebra R S) R[x]
    (HMul.hMul (α := S) (β := S) ((l : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) p : S))
⊢ ∃ x_1 ∈ (↑(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) x_1 =
      HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) a : S)
        (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) p : S) ((l : (a : R) → S) a : S))

Tactic:
refine Exists.intro
        (algebraMap R R<x> a * ⟨l a * algebraMap R S p,
          show l a * algebraMap R S p ∈ R<x> from ?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
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
a : R
ha : a ∈ I
rw :
  Membership.mem (γ := Subalgebra R S) R[x]
    (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) p : S) ((l : (a : R) → S) a : S))
⊢ Membership.mem (γ := Subalgebra R S) R[x]
    (HMul.hMul (α := S) (β := S) ((l : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) p : S))

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
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
a : R
ha : a ∈ I
⊢ Membership.mem (γ := Subalgebra R S) R[x]
    (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) p : S) ((l : (a : R) → S) a : S))

Tactic:
mem_conductor_iff.mp (Ideal.mem_comap.mp hp) _

Premises used: Set.Mem, mem_conductor_iff, Iff.mp, 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
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
a : R
ha : a ∈ I
⊢ Membership.mem (γ := Subalgebra R S) R[x]
    (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) p : S) ((l : (a : R) → S) a : S))

Tactic:
exact mem_conductor_iff.mp (Ideal.mem_comap.mp hp) _

Premises used: mem_conductor_iff, Iff.mp, 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
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
a : R
ha : a ∈ I
⊢ Membership.mem (γ := Subalgebra R S) R[x]
    (HMul.hMul (α := S) (β := S) ((l : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) p : S))

Tactic:
case h =>
      rw [mul_comm]
      exact mem_conductor_iff.mp (Ideal.mem_comap.mp hp) _

Premises used: mem_conductor_iff, Iff.mp, mul_comm, 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
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
a : R
ha : a ∈ I
⊢ HMul.hMul (α := ↥R[x]) (β := ↥R[x]) ((algebraMap R ↥R[x] : (a : R) → ↥R[x]) a : ↥R[x])
        (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1)
          (HMul.hMul (α := S) (β := S) ((l : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) p : 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)
        (HMul.hMul (α := ↥R[x]) (β := ↥R[x]) ((algebraMap R ↥R[x] : (a : R) → ↥R[x]) a : ↥R[x])
          (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1)
            (HMul.hMul (α := S) (β := S) ((l : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) p : S)) ⋯)) =
      HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) a : S)
        (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) p : S) ((l : (a : R) → S) a : S))

Tactic:
⟨?_, ?_⟩

Premises used: And.intro
-- Module: Mathlib.RingTheory.Conductor
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
I : Ideal R
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
a : R
ha : a ∈ I
refine_1 :
  HMul.hMul (α := ↥R[x]) (β := ↥R[x]) ((algebraMap R ↥R[x] : (a : R) → ↥R[x]) a : ↥R[x])
      (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1)
        (HMul.hMul (α := S) (β := S) ((l : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) p : S)) ⋯) ∈
    (↑(Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) : Set ↥R[x])
refine_2 :
  (algebraMap (↥R[x]) S : (a : ↥R[x]) → S)
      (HMul.hMul (α := ↥R[x]) (β := ↥R[x]) ((algebraMap R ↥R[x] : (a : R) → ↥R[x]) a : ↥R[x])
        (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1)
          (HMul.hMul (α := S) (β := S) ((l : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) p : S)) ⋯)) =
    HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) a : S)
      (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) p : S) ((l : (a : R) → S) a : S))
⊢ HMul.hMul (α := ↥R[x]) (β := ↥R[x]) ((algebraMap R ↥R[x] : (a : R) → ↥R[x]) a : ↥R[x])
        (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1)
          (HMul.hMul (α := S) (β := S) ((l : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) p : 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)
        (HMul.hMul (α := ↥R[x]) (β := ↥R[x]) ((algebraMap R ↥R[x] : (a : R) → ↥R[x]) a : ↥R[x])
          (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1)
            (HMul.hMul (α := S) (β := S) ((l : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) p : S)) ⋯)) =
      HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) a : S)
        (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) p : S) ((l : (a : R) → S) a : S))

Tactic:
refine ⟨?_, ?_⟩
-- 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
a : R
ha : a ∈ I
refine_1 :
  HMul.hMul (α := ↥R[x]) (β := ↥R[x])
      (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1)
        (HMul.hMul (α := S) (β := S) ((l : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) p : S)) ⋯)
      ((algebraMap R ↥R[x] : (a : R) → ↥R[x]) a : ↥R[x]) ∈
    (↑(Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) : Set ↥R[x])
⊢ HMul.hMul (α := ↥R[x]) (β := ↥R[x]) ((algebraMap R ↥R[x] : (a : R) → ↥R[x]) a : ↥R[x])
      (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1)
        (HMul.hMul (α := S) (β := S) ((l : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) p : S)) ⋯) ∈
    (↑(Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) : Set ↥R[x])

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
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
a : R
ha : a ∈ I
⊢ HMul.hMul (α := ↥R[x]) (β := ↥R[x])
      (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1)
        (HMul.hMul (α := S) (β := S) ((l : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) p : S)) ⋯)
      ((algebraMap R ↥R[x] : (a : R) → ↥R[x]) a : ↥R[x]) ∈
    (↑(Ideal.map (F := RingHom.{u_1, u_2} R ↥R[x]) (algebraMap R ↥R[x]) I) : Set ↥R[x])

Tactic:
apply Ideal.mul_mem_left (I.map (algebraMap R R<x>)) _ (Ideal.mem_map_of_mem _ ha)
-- 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
a : R
ha : a ∈ I
refine_2 :
  HMul.hMul (α := S) (β := S)
      ((algebraMap (↥R[x]) S : (a : ↥R[x]) → S) ((algebraMap R ↥R[x] : (a : R) → ↥R[x]) a : ↥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)
            (HMul.hMul (α := S) (β := S) ((l : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) p : S)) ⋯) :
        S) =
    HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) a : S)
      (HMul.hMul (α := S) (β := S) ((l : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) p : S))
⊢ (algebraMap (↥R[x]) S : (a : ↥R[x]) → S)
      (HMul.hMul (α := ↥R[x]) (β := ↥R[x]) ((algebraMap R ↥R[x] : (a : R) → ↥R[x]) a : ↥R[x])
        (Subtype.mk (p := fun (x_1 : S) ↦ Membership.mem (γ := Subalgebra R S) R[x] x_1)
          (HMul.hMul (α := S) (β := S) ((l : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) p : S)) ⋯)) =
    HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) a : S)
      (HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) p : S) ((l : (a : R) → S) a : S))

Tactic:
simp only [map_mul, mul_comm (algebraMap R S p) (l a)]

Premises used: Algebra.algebraMap, map_mul, mul_comm, DFunLike.coe
-- 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
a : R
ha : a ∈ I
⊢ HMul.hMul (α := S) (β := S)
      ((algebraMap (↥R[x]) S : (a : ↥R[x]) → S) ((algebraMap R ↥R[x] : (a : R) → ↥R[x]) a : ↥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)
            (HMul.hMul (α := S) (β := S) ((l : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) p : S)) ⋯) :
        S) =
    HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) a : S)
      (HMul.hMul (α := S) (β := S) ((l : (a : R) → S) a : S) ((algebraMap R S : (a : R) → S) p : S))

Tactic:
rfl
-- Module: Mathlib.RingTheory.Conductor
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
I : Ideal R
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
⊢ ∀ {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))

Tactic:
have lem : ∀ {a : R}, a ∈ I → l a • algebraMap R S a * algebraMap R S p ∈
      algebraMap R<x> S '' I.map (algebraMap R R<x>) := by
    intro a ha
    rw [smul_eq_mul, mul_assoc, mul_comm, mul_assoc, Set.mem_image]
    refine Exists.intro
        (algebraMap R R<x> a * ⟨l a * algebraMap R S p,
          show l a * algebraMap R S p ∈ R<x> from ?h⟩) ?_
    case h =>
      rw [mul_comm]
      exact mem_conductor_iff.mp (Ideal.mem_comap.mp hp) _
    · refine ⟨?_, ?_⟩
      · rw [mul_comm]
        apply Ideal.mul_mem_left (I.map (algebraMap R R<x>)) _ (Ideal.mem_map_of_mem _ ha)
      · simp only [map_mul, mul_comm (algebraMap R S p) (l a)]
        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))
⊢ 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))

Tactic:
Finset.sum_induction _ (fun u => u ∈ algebraMap R<x> S '' I.map (algebraMap R R<x>))
      (fun a b => ?_) ?_ ?_

Premises used: Algebra.algebraMap, Set.Mem, Finsupp.sum, Algebra.adjoin, Membership.mem, Subtype, Ideal.map, SetLike.coe, Finset.sum_induction, Set.image, Singleton.singleton, DFunLike.coe
-- 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))
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
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))
⊢ 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))

Tactic:
refine Finset.sum_induction _ (fun u => u ∈ algebraMap R<x> S '' I.map (algebraMap R R<x>))
      (fun a b => ?_) ?_ ?_
-- 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])
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)
⊢ 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))

Tactic:
rw [← map_add]

Premises used: map_add