-- 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:
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
⊢ (algebraMap R S) p * z + (algebraMap R S) q * z ∈
    ⇑(algebraMap (↥(adjoin R {x})) S) '' ↑(Ideal.map (algebraMap R ↥(adjoin R {x})) I)

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))

Result:
case 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
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 R S) p * z + (algebraMap R S) q * z ∈
    ⇑(algebraMap (↥(adjoin R {x})) S) '' ↑(Ideal.map (algebraMap R ↥(adjoin R {x})) I)

Proof state:
case a.mk.intro.intro.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
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, hz⟩ ∈ Ideal.map (algebraMap R ↥(adjoin R {x})) I

Tactic:
have : x₁ = ⟨z, hz⟩ := by
  apply h_alg
  simp only [hx₂, algebraMap_eq_smul_one]
  rw [Submonoid.mk_smul, smul_eq_mul, mul_one]

Result:
case a.mk.intro.intro.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
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
this : x₁ = ⟨z, hz⟩
⊢ ⟨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)
⊢ comap (algebraMap (↥(adjoin R {x})) S) (Ideal.map (algebraMap R S) I) ≤ Ideal.map (algebraMap R ↥(adjoin R {x})) I

Tactic:
intro y hy

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)
y : ↥(adjoin R {x})
hy : y ∈ comap (algebraMap (↥(adjoin R {x})) S) (Ideal.map (algebraMap R S) I)
⊢ y ∈ 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
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
⊢ ⟨z, hz⟩ ∈ Ideal.map (algebraMap R ↥(adjoin R {x})) I

Tactic:
rw [← this, ← temp]

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
⊢ (algebraMap R S) p * z + (algebraMap R S) q * z ∈
    ⇑(algebraMap (↥(adjoin R {x})) S) '' ↑(Ideal.map (algebraMap R ↥(adjoin R {x})) I)

Proof state:
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
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
⊢ ⟨z, hz⟩ * (algebraMap R ↥(adjoin R {x})) q ∈ Ideal.map (algebraMap R ↥(adjoin R {x})) I

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

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)
⊢ algebraMap R S = (algebraMap (↥(adjoin R {x})) S).comp (algebraMap R ↥(adjoin R {x}))

Tactic:
ext

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)
x✝ : R
⊢ (algebraMap R S) x✝ = ((algebraMap (↥(adjoin R {x})) S).comp (algebraMap R ↥(adjoin R {x}))) x✝