-- Mathlib/NumberTheory/KummerDedekind.lean
lemma mem_coeSubmodule_conductor {L} [CommRing L] [Algebra S L] [Algebra R L]
    [IsScalarTower R S L] [NoZeroSMulDivisors S L] {x : S} {y : L} :
    y ∈ coeSubmodule L (conductor R x) ↔ ∀ z : S,
      y * (algebraMap S L) z ∈ Algebra.adjoin R {algebraMap S L x}

Proof state:
case mpr.intro.intro
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
L : Type u_3
inst✝⁴ : CommRing L
inst✝³ : Algebra S L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R S L
inst✝ : NoZeroSMulDivisors S L
x : S
y✝ : L
h✝ : Nontrivial L
H : ∀ (z : S), ∃ x_1 ∈ adjoin R {x}, (algebraMap S L) x_1 = y✝ * (algebraMap S L) z
y : S
left✝ : y ∈ adjoin R {x}
e : (algebraMap S L) y = y✝ * (algebraMap S L) 1
⊢ ∃ y ∈ conductor R x, (algebraMap S L) y = y✝

Tactic:
rw [map_one, mul_one] at e

Result:
case mpr.intro.intro
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
L : Type u_3
inst✝⁴ : CommRing L
inst✝³ : Algebra S L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R S L
inst✝ : NoZeroSMulDivisors S L
x : S
y✝ : L
h✝ : Nontrivial L
H : ∀ (z : S), ∃ x_1 ∈ adjoin R {x}, (algebraMap S L) x_1 = y✝ * (algebraMap S L) z
y : S
left✝ : y ∈ adjoin R {x}
e : (algebraMap S L) y = y✝
⊢ ∃ y ∈ conductor R x, (algebraMap S L) y = y✝

Proof state:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
L : Type u_3
inst✝⁴ : CommRing L
inst✝³ : Algebra S L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R S L
inst✝ : NoZeroSMulDivisors S L
x : S
y : L
h✝ : Nontrivial L
⊢ (∀ (z : S), y * (algebraMap S L) z ∈ adjoin R {(IsScalarTower.toAlgHom R S L) x}) ↔
    ∀ (z : S), y * (algebraMap S L) z ∈ adjoin R {(algebraMap S L) x}

Tactic:
rfl

Result:
no goals

Proof state:
case mp
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
L : Type u_3
inst✝⁴ : CommRing L
inst✝³ : Algebra S L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R S L
inst✝ : NoZeroSMulDivisors S L
x : S
y : L
h✝ : Nontrivial L
⊢ (∃ y_1 ∈ conductor R x, (algebraMap S L) y_1 = y) →
    ∀ (z : S), ∃ x_1 ∈ adjoin R {x}, (algebraMap S L) x_1 = y * (algebraMap S L) z

Tactic:
rintro ⟨y, hy, rfl⟩ z

Result:
case mp.intro.intro
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
L : Type u_3
inst✝⁴ : CommRing L
inst✝³ : Algebra S L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R S L
inst✝ : NoZeroSMulDivisors S L
x : S
h✝ : Nontrivial L
y : S
hy : y ∈ conductor R x
z : S
⊢ ∃ x_1 ∈ adjoin R {x}, (algebraMap S L) x_1 = (algebraMap S L) y * (algebraMap S L) z

Proof state:
case mpr.intro.intro
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
L : Type u_3
inst✝⁴ : CommRing L
inst✝³ : Algebra S L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R S L
inst✝ : NoZeroSMulDivisors S L
x : S
h✝ : Nontrivial L
y : S
left✝ : y ∈ adjoin R {x}
H : ∀ (z : S), ∃ x_1 ∈ adjoin R {x}, (algebraMap S L) x_1 = (algebraMap S L) y * (algebraMap S L) z
⊢ ∃ y_1 ∈ conductor R x, (algebraMap S L) y_1 = (algebraMap S L) y

Tactic:
simp only [← _root_.map_mul, (FaithfulSMul.algebraMap_injective S L).eq_iff,
  exists_eq_right] at H

Result:
case mpr.intro.intro
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
L : Type u_3
inst✝⁴ : CommRing L
inst✝³ : Algebra S L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R S L
inst✝ : NoZeroSMulDivisors S L
x : S
h✝ : Nontrivial L
y : S
left✝ : y ∈ adjoin R {x}
H : ∀ (z : S), y * z ∈ adjoin R {x}
⊢ ∃ y_1 ∈ conductor R x, (algebraMap S L) y_1 = (algebraMap S L) y

Proof state:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
L : Type u_3
inst✝⁴ : CommRing L
inst✝³ : Algebra S L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R S L
inst✝ : NoZeroSMulDivisors S L
x : S
y : L
h✝ : Nontrivial L
⊢ (∃ y_1 ∈ conductor R x, (algebraMap S L) y_1 = y) ↔
    ∀ (z : S), ∃ x_1 ∈ adjoin R {x}, (algebraMap S L) x_1 = y * (algebraMap S L) z

Tactic:
constructor

Result:
case mp
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
L : Type u_3
inst✝⁴ : CommRing L
inst✝³ : Algebra S L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R S L
inst✝ : NoZeroSMulDivisors S L
x : S
y : L
h✝ : Nontrivial L
⊢ (∃ y_1 ∈ conductor R x, (algebraMap S L) y_1 = y) →
    ∀ (z : S), ∃ x_1 ∈ adjoin R {x}, (algebraMap S L) x_1 = y * (algebraMap S L) z

case mpr
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
L : Type u_3
inst✝⁴ : CommRing L
inst✝³ : Algebra S L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R S L
inst✝ : NoZeroSMulDivisors S L
x : S
y : L
h✝ : Nontrivial L
⊢ (∀ (z : S), ∃ x_1 ∈ adjoin R {x}, (algebraMap S L) x_1 = y * (algebraMap S L) z) →
    ∃ y_1 ∈ conductor R x, (algebraMap S L) y_1 = y

Proof state:
case mpr
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
L : Type u_3
inst✝⁴ : CommRing L
inst✝³ : Algebra S L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R S L
inst✝ : NoZeroSMulDivisors S L
x : S
y : L
h✝ : Nontrivial L
⊢ (∀ (z : S), ∃ x_1 ∈ adjoin R {x}, (algebraMap S L) x_1 = y * (algebraMap S L) z) →
    ∃ y_1 ∈ conductor R x, (algebraMap S L) y_1 = y

Tactic:
intro H

Result:
case mpr
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
L : Type u_3
inst✝⁴ : CommRing L
inst✝³ : Algebra S L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R S L
inst✝ : NoZeroSMulDivisors S L
x : S
y : L
h✝ : Nontrivial L
H : ∀ (z : S), ∃ x_1 ∈ adjoin R {x}, (algebraMap S L) x_1 = y * (algebraMap S L) z
⊢ ∃ y_1 ∈ conductor R x, (algebraMap S L) y_1 = y

Proof state:
case mpr.intro.intro
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
L : Type u_3
inst✝⁴ : CommRing L
inst✝³ : Algebra S L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R S L
inst✝ : NoZeroSMulDivisors S L
x : S
y✝ : L
h✝ : Nontrivial L
H : ∀ (z : S), ∃ x_1 ∈ adjoin R {x}, (algebraMap S L) x_1 = y✝ * (algebraMap S L) z
y : S
left✝ : y ∈ adjoin R {x}
e : (algebraMap S L) y = y✝
⊢ ∃ y ∈ conductor R x, (algebraMap S L) y = y✝

Tactic:
subst e

Result:
case mpr.intro.intro
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
L : Type u_3
inst✝⁴ : CommRing L
inst✝³ : Algebra S L
inst✝² : Algebra R L
inst✝¹ : IsScalarTower R S L
inst✝ : NoZeroSMulDivisors S L
x : S
h✝ : Nontrivial L
y : S
left✝ : y ∈ adjoin R {x}
H : ∀ (z : S), ∃ x_1 ∈ adjoin R {x}, (algebraMap S L) x_1 = (algebraMap S L) y * (algebraMap S L) z
⊢ ∃ y_1 ∈ conductor R x, (algebraMap S L) y_1 = (algebraMap S L) y