-- 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
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
⊢ x₁ = ⟨z, hz⟩

Tactic:
apply h_alg

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
⊢ (algebraMap (↥(adjoin R {x})) S) x₁ = (algebraMap (↥(adjoin R {x})) S) ⟨z, hz⟩

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

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

Tactic:
simp [h]

Result:
no goals

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

Tactic:
obtain ⟨x₁, hx₁, hx₂⟩ := (Set.mem_image _ _ _).mp h

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
⊢ ⟨z, hz⟩ ∈ 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 ∈ Ideal.map (algebraMap R S) I

Tactic:
rwa [Ideal.mem_comap] at hy

Result:
no goals

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

Tactic:
obtain ⟨p, hp, q, hq, hpq⟩ := Submodule.mem_sup.mp ((Ideal.eq_top_iff_one _).mp hx)

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