-- Mathlib/NumberTheory/KummerDedekind.lean
theorem comap_map_eq_map_adjoin_of_coprime_conductor
    (hx : (conductor R x).comap (algebraMap R S) ⊔ I = ⊤)
    (h_alg : Function.Injective (algebraMap R<x> S)) :
    (I.map (algebraMap R S)).comap (algebraMap R<x> S) = I.map (algebraMap R R<x>)

Proof state:
case a.mk.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
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective ⇑(algebraMap (↥(adjoin R {x})) S)
z : S
hz : z ∈ adjoin R {x}
hy : ⟨z, hz⟩ ∈ comap (algebraMap (↥(adjoin R {x})) S) (Ideal.map (algebraMap R S) I)
p : R
hp : p ∈ comap (algebraMap R S) (conductor R x)
q : R
hq : q ∈ I
hpq : p + q = 1
temp : (algebraMap R S) p * z + (algebraMap R S) q * z = z
⊢ ⟨z, hz⟩ ∈ Ideal.map (algebraMap R ↥(adjoin R {x})) I

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, _root_.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)

Result:
case a.mk.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
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective ⇑(algebraMap (↥(adjoin R {x})) S)
z : S
hz : z ∈ adjoin R {x}
hy : ⟨z, hz⟩ ∈ comap (algebraMap (↥(adjoin R {x})) S) (Ideal.map (algebraMap R S) I)
p : R
hp : p ∈ comap (algebraMap R S) (conductor R x)
q : R
hq : q ∈ I
hpq : p + q = 1
temp : (algebraMap R S) p * z + (algebraMap R S) q * z = z
⊢ z ∈ ⇑(algebraMap (↥(adjoin R {x})) S) '' ↑(Ideal.map (algebraMap R ↥(adjoin R {x})) I) ↔
    ⟨z, hz⟩ ∈ Ideal.map (algebraMap R ↥(adjoin R {x})) I

Proof state:
case a
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective ⇑(algebraMap (↥(adjoin R {x})) S)
z : S
hz : z ∈ adjoin R {x}
hy : ⟨z, hz⟩ ∈ comap (algebraMap (↥(adjoin R {x})) S) (Ideal.map (algebraMap R S) I)
p : R
hp : p ∈ comap (algebraMap R S) (conductor R x)
q : R
hq : q ∈ I
hpq : p + q = 1
temp : (algebraMap R S) p * z + (algebraMap R S) q * z = z
h : z ∈ ⇑(algebraMap (↥(adjoin R {x})) S) '' ↑(Ideal.map (algebraMap R ↥(adjoin R {x})) I)
x₁ : ↥(adjoin R {x})
hx₁ : x₁ ∈ ↑(Ideal.map (algebraMap R ↥(adjoin R {x})) I)
hx₂ : (algebraMap (↥(adjoin R {x})) S) x₁ = z
⊢ (algebraMap (↥(adjoin R {x})) S) x₁ = (algebraMap (↥(adjoin R {x})) S) ⟨z, hz⟩

Tactic:
simp only [hx₂, algebraMap_eq_smul_one]

Result:
case a
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective ⇑(algebraMap (↥(adjoin R {x})) S)
z : S
hz : z ∈ adjoin R {x}
hy : ⟨z, hz⟩ ∈ comap (algebraMap (↥(adjoin R {x})) S) (Ideal.map (algebraMap R S) I)
p : R
hp : p ∈ comap (algebraMap R S) (conductor R x)
q : R
hq : q ∈ I
hpq : p + q = 1
temp : (algebraMap R S) p * z + (algebraMap R S) q * z = z
h : z ∈ ⇑(algebraMap (↥(adjoin R {x})) S) '' ↑(Ideal.map (algebraMap R ↥(adjoin R {x})) I)
x₁ : ↥(adjoin R {x})
hx₁ : x₁ ∈ ↑(Ideal.map (algebraMap R ↥(adjoin R {x})) I)
hx₂ : (algebraMap (↥(adjoin R {x})) S) x₁ = z
⊢ z = ⟨z, hz⟩ • 1

Proof state:
case a
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective ⇑(algebraMap (↥(adjoin R {x})) S)
this : algebraMap R S = (algebraMap (↥(adjoin R {x})) S).comp (algebraMap R ↥(adjoin R {x}))
⊢ Ideal.map (algebraMap R ↥(adjoin R {x})) I ≤
    comap (algebraMap (↥(adjoin R {x})) S)
      (Ideal.map (algebraMap (↥(adjoin R {x})) S) (Ideal.map (algebraMap R ↥(adjoin R {x})) I))

Tactic:
apply Ideal.le_comap_map

Result:
no goals

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
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective ⇑(algebraMap (↥(adjoin R {x})) S)
z : S
hz : z ∈ adjoin R {x}
hy : ⟨z, hz⟩ ∈ comap (algebraMap (↥(adjoin R {x})) S) (Ideal.map (algebraMap R S) I)
p : R
hp : p ∈ comap (algebraMap R S) (conductor R x)
q : R
hq : q ∈ I
hpq : p + q = 1
temp : (algebraMap R S) p * z + (algebraMap R S) q * z = z
this :
  z ∈ ⇑(algebraMap (↥(adjoin R {x})) S) '' ↑(Ideal.map (algebraMap R ↥(adjoin R {x})) I) ↔
    ⟨z, hz⟩ ∈ Ideal.map (algebraMap R ↥(adjoin R {x})) I
a : ↥(adjoin R {x})
ha : a ∈ ↑(Ideal.map (algebraMap R ↥(adjoin R {x})) I) ∧ (algebraMap (↥(adjoin R {x})) S) a = (algebraMap R S) p * z
⊢ (algebraMap (↥(adjoin R {x})) S) (a + (algebraMap R ↥(adjoin R {x})) q * ⟨z, hz⟩) =
    (algebraMap R S) p * z + (algebraMap R S) q * z

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

Result:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective ⇑(algebraMap (↥(adjoin R {x})) S)
z : S
hz : z ∈ adjoin R {x}
hy : ⟨z, hz⟩ ∈ comap (algebraMap (↥(adjoin R {x})) S) (Ideal.map (algebraMap R S) I)
p : R
hp : p ∈ comap (algebraMap R S) (conductor R x)
q : R
hq : q ∈ I
hpq : p + q = 1
temp : (algebraMap R S) p * z + (algebraMap R S) q * z = z
this :
  z ∈ ⇑(algebraMap (↥(adjoin R {x})) S) '' ↑(Ideal.map (algebraMap R ↥(adjoin R {x})) I) ↔
    ⟨z, hz⟩ ∈ Ideal.map (algebraMap R ↥(adjoin R {x})) I
a : ↥(adjoin R {x})
ha : a ∈ ↑(Ideal.map (algebraMap R ↥(adjoin R {x})) I) ∧ (algebraMap (↥(adjoin R {x})) S) a = (algebraMap R S) p * z
⊢ (algebraMap (↥(adjoin R {x})) S) ((algebraMap R ↥(adjoin R {x})) q) * (algebraMap (↥(adjoin R {x})) S) ⟨z, hz⟩ =
    (algebraMap R S) q * z

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
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective ⇑(algebraMap (↥(adjoin R {x})) S)
z : S
hz : z ∈ adjoin R {x}
hy : ⟨z, hz⟩ ∈ comap (algebraMap (↥(adjoin R {x})) S) (Ideal.map (algebraMap R S) I)
p : R
hp : p ∈ comap (algebraMap R S) (conductor R x)
q : R
hq : q ∈ I
hpq : p + q = 1
⊢ (algebraMap R S) p * z + (algebraMap R S) q * z = z

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

Result:
no goals

Proof state:
case a
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective ⇑(algebraMap (↥(adjoin R {x})) S)
this : algebraMap R S = (algebraMap (↥(adjoin R {x})) S).comp (algebraMap R ↥(adjoin R {x}))
⊢ Ideal.map (algebraMap R ↥(adjoin R {x})) I ≤ comap (algebraMap (↥(adjoin R {x})) S) (Ideal.map (algebraMap R S) I)

Tactic:
rw [this, ← Ideal.map_map]

Result:
case a
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
I : Ideal R
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
h_alg : Function.Injective ⇑(algebraMap (↥(adjoin R {x})) S)
this : algebraMap R S = (algebraMap (↥(adjoin R {x})) S).comp (algebraMap R ↥(adjoin R {x}))
⊢ Ideal.map (algebraMap R ↥(adjoin R {x})) I ≤
    comap (algebraMap (↥(adjoin R {x})) S)
      (Ideal.map (algebraMap (↥(adjoin R {x})) S) (Ideal.map (algebraMap R ↥(adjoin R {x})) I))