-- Mathlib/NumberTheory/KummerDedekind.lean
theorem prod_mem_ideal_map_of_mem_conductor {p : R} {z : S}
    (hp : p ∈ Ideal.comap (algebraMap R S) (conductor R x)) (hz' : z ∈ I.map (algebraMap R S)) :
    algebraMap R S p * z ∈ algebraMap R<x> S '' ↑(I.map (algebraMap R R<x>))

Proof state:
case refine_1
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
p : R
z : S
hp : p ∈ comap (algebraMap R S) (conductor R x)
l : R →₀ S
H : l ∈ Finsupp.supported S S ↑I
H' : (l.sum fun i a => a • (algebraMap R S) i) = z
a : R
ha : a ∈ I
⊢ (algebraMap R ↥(adjoin R {x})) a * ⟨l a * (algebraMap R S) p, ⋯⟩ ∈ ↑(Ideal.map (algebraMap R ↥(adjoin R {x})) I)

Tactic:
rw [mul_comm]

Result:
case refine_1
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
p : R
z : S
hp : p ∈ comap (algebraMap R S) (conductor R x)
l : R →₀ S
H : l ∈ Finsupp.supported S S ↑I
H' : (l.sum fun i a => a • (algebraMap R S) i) = z
a : R
ha : a ∈ I
⊢ ⟨l a * (algebraMap R S) p, ⋯⟩ * (algebraMap R ↥(adjoin R {x})) a ∈ ↑(Ideal.map (algebraMap R ↥(adjoin R {x})) I)

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
p : R
z : S
hp : p ∈ comap (algebraMap R S) (conductor R x)
l : R →₀ S
H : l ∈ Finsupp.supported S S ↑I
H' : (l.sum fun i a => a • (algebraMap R S) i) = z
a : R
ha : a ∈ I
⊢ ∃ x_1 ∈ ↑(Ideal.map (algebraMap R ↥(adjoin R {x})) I),
    (algebraMap (↥(adjoin R {x})) S) x_1 = (algebraMap R S) a * ((algebraMap R S) p * l a)

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⟩) ?_

Result:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
p : R
z : S
hp : p ∈ comap (algebraMap R S) (conductor R x)
l : R →₀ S
H : l ∈ Finsupp.supported S S ↑I
H' : (l.sum fun i a => a • (algebraMap R S) i) = z
a : R
ha : a ∈ I
⊢ (algebraMap R ↥(adjoin R {x})) a * ⟨l a * (algebraMap R S) p, ⋯⟩ ∈ ↑(Ideal.map (algebraMap R ↥(adjoin R {x})) I) ∧
    (algebraMap (↥(adjoin R {x})) S) ((algebraMap R ↥(adjoin R {x})) a * ⟨l a * (algebraMap R S) p, ⋯⟩) =
      (algebraMap R S) a * ((algebraMap R S) p * l a)

case h
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
p : R
z : S
hp : p ∈ comap (algebraMap R S) (conductor R x)
l : R →₀ S
H : l ∈ Finsupp.supported S S ↑I
H' : (l.sum fun i a => a • (algebraMap R S) i) = z
a : R
ha : a ∈ I
⊢ l a * (algebraMap R S) p ∈ adjoin R {x}

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
p : R
z : S
hp : p ∈ comap (algebraMap R S) (conductor R x)
l : R →₀ S
H : l ∈ Finsupp.supported S S ↑I
H' : (l.sum fun i a => a • (algebraMap R S) i) = z
a : R
ha : a ∈ I
⊢ (algebraMap R ↥(adjoin R {x})) a * ⟨l a * (algebraMap R S) p, ⋯⟩ ∈ ↑(Ideal.map (algebraMap R ↥(adjoin R {x})) I) ∧
    (algebraMap (↥(adjoin R {x})) S) ((algebraMap R ↥(adjoin R {x})) a * ⟨l a * (algebraMap R S) p, ⋯⟩) =
      (algebraMap R S) a * ((algebraMap R S) p * l a)

case h
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
p : R
z : S
hp : p ∈ comap (algebraMap R S) (conductor R x)
l : R →₀ S
H : l ∈ Finsupp.supported S S ↑I
H' : (l.sum fun i a => a • (algebraMap R S) i) = z
a : R
ha : a ∈ I
⊢ l a * (algebraMap R S) p ∈ adjoin R {x}

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

Result:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
p : R
z : S
hp : p ∈ comap (algebraMap R S) (conductor R x)
l : R →₀ S
H : l ∈ Finsupp.supported S S ↑I
H' : (l.sum fun i a => a • (algebraMap R S) i) = z
a : R
ha : a ∈ I
⊢ (algebraMap R ↥(adjoin R {x})) a * ⟨l a * (algebraMap R S) p, ⋯⟩ ∈ ↑(Ideal.map (algebraMap R ↥(adjoin R {x})) I) ∧
    (algebraMap (↥(adjoin R {x})) S) ((algebraMap R ↥(adjoin R {x})) a * ⟨l a * (algebraMap R S) p, ⋯⟩) =
      (algebraMap R S) a * ((algebraMap R S) p * l a)

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
p : R
z : S
hp : p ∈ comap (algebraMap R S) (conductor R x)
l : R →₀ S
H : l ∈ Finsupp.supported S S ↑I
H' : (l.sum fun i a => a • (algebraMap R S) i) = z
a : R
ha : a ∈ I
⊢ (algebraMap R ↥(adjoin R {x})) a * ⟨l a * (algebraMap R S) p, ⋯⟩ ∈ ↑(Ideal.map (algebraMap R ↥(adjoin R {x})) I) ∧
    (algebraMap (↥(adjoin R {x})) S) ((algebraMap R ↥(adjoin R {x})) a * ⟨l a * (algebraMap R S) p, ⋯⟩) =
      (algebraMap R S) a * ((algebraMap R S) p * l a)

Tactic:
refine ⟨?_, ?_⟩

Result:
case refine_1
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
p : R
z : S
hp : p ∈ comap (algebraMap R S) (conductor R x)
l : R →₀ S
H : l ∈ Finsupp.supported S S ↑I
H' : (l.sum fun i a => a • (algebraMap R S) i) = z
a : R
ha : a ∈ I
⊢ (algebraMap R ↥(adjoin R {x})) a * ⟨l a * (algebraMap R S) p, ⋯⟩ ∈ ↑(Ideal.map (algebraMap R ↥(adjoin R {x})) I)

case refine_2
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
p : R
z : S
hp : p ∈ comap (algebraMap R S) (conductor R x)
l : R →₀ S
H : l ∈ Finsupp.supported S S ↑I
H' : (l.sum fun i a => a • (algebraMap R S) i) = z
a : R
ha : a ∈ I
⊢ (algebraMap (↥(adjoin R {x})) S) ((algebraMap R ↥(adjoin R {x})) a * ⟨l a * (algebraMap R S) p, ⋯⟩) =
    (algebraMap R S) a * ((algebraMap R S) p * l a)

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
p : R
z : S
hp : p ∈ comap (algebraMap R S) (conductor R x)
hz' : z ∈ Ideal.map (algebraMap R S) I
⊢ (algebraMap R S) p * z ∈ ⇑(algebraMap (↥(adjoin R {x})) S) '' ↑(Ideal.map (algebraMap R ↥(adjoin R {x})) I)

Tactic:
rw [Ideal.map, Ideal.span, Finsupp.mem_span_image_iff_linearCombination] at hz'

Result:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
p : R
z : S
hp : p ∈ comap (algebraMap R S) (conductor R x)
hz' : ∃ l ∈ Finsupp.supported S S ↑I, (Finsupp.linearCombination S ⇑(algebraMap R S)) l = z
⊢ (algebraMap R S) p * z ∈ ⇑(algebraMap (↥(adjoin R {x})) S) '' ↑(Ideal.map (algebraMap R ↥(adjoin R {x})) I)

Proof state:
case intro.intro.refine_1.intro.intro.intro.intro
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
p : R
z✝ : S
hp : p ∈ comap (algebraMap R S) (conductor R x)
l : R →₀ S
H : l ∈ Finsupp.supported S S ↑I
H' : (l.sum fun i a => a • (algebraMap R S) i) = z✝
lem :
  ∀ {a : R},
    a ∈ I →
      l a • (algebraMap R S) a * (algebraMap R S) p ∈
        ⇑(algebraMap (↥(adjoin R {x})) S) '' ↑(Ideal.map (algebraMap R ↥(adjoin R {x})) I)
z : ↥(adjoin R {x})
hz : z ∈ ↑(Ideal.map (algebraMap R ↥(adjoin R {x})) I)
y : ↥(adjoin R {x})
hy : y ∈ ↑(Ideal.map (algebraMap R ↥(adjoin R {x})) I)
⊢ (algebraMap (↥(adjoin R {x})) S) (z + y) ∈
    ⇑(algebraMap (↥(adjoin R {x})) S) '' ↑(Ideal.map (algebraMap R ↥(adjoin R {x})) I)

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

Result:
no goals

Proof state:
case refine_2
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
p : R
z : S
hp : p ∈ comap (algebraMap R S) (conductor R x)
l : R →₀ S
H : l ∈ Finsupp.supported S S ↑I
H' : (l.sum fun i a => a • (algebraMap R S) i) = z
a : R
ha : a ∈ I
⊢ (algebraMap (↥(adjoin R {x})) S) ((algebraMap R ↥(adjoin R {x})) a) *
      (algebraMap (↥(adjoin R {x})) S) ⟨l a * (algebraMap R S) p, ⋯⟩ =
    (algebraMap R S) a * (l a * (algebraMap R S) p)

Tactic:
rfl

Result:
no goals