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

Tactic:
obtain ⟨y, _, e⟩ := H 1

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✝ * (algebraMap S L) 1
⊢ ∃ 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
⊢ y ∈ coeSubmodule L (conductor R x) ↔ ∀ (z : S), y * (algebraMap S L) z ∈ adjoin R {(algebraMap S L) x}

Tactic:
cases subsingleton_or_nontrivial L

Result:
case inl
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✝ : Subsingleton L
⊢ y ∈ coeSubmodule L (conductor R x) ↔ ∀ (z : S), y * (algebraMap S L) z ∈ adjoin R {(algebraMap S L) x}

case inr
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 ∈ coeSubmodule L (conductor R x) ↔ ∀ (z : S), y * (algebraMap S L) z ∈ adjoin R {(algebraMap S L) x}

Proof state:
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

Tactic:
exact ⟨_, hy z, map_mul _ _ _⟩

Result:
no goals

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), y * z ∈ adjoin R {x}
⊢ ∃ y_1 ∈ conductor R x, (algebraMap S L) y_1 = (algebraMap S L) y

Tactic:
exact ⟨_, H, rfl⟩

Result:
no goals

Proof state:
case inl
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✝ : Subsingleton L
⊢ y ∈ coeSubmodule L (conductor R x) ↔ ∀ (z : S), y * (algebraMap S L) z ∈ adjoin R {(algebraMap S L) x}

Tactic:
rw [Subsingleton.elim (coeSubmodule L _) ⊤, Subsingleton.elim (Algebra.adjoin R _) ⊤]

Result:
case inl
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✝ : Subsingleton L
⊢ y ∈ ⊤ ↔ ∀ (z : S), y * (algebraMap S L) z ∈ ⊤

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 ∈ coeSubmodule L (conductor R x) ↔
    ∀ (z : S), y * (algebraMap S L) z ∈ Subalgebra.map (IsScalarTower.toAlgHom R S L) (adjoin R {x})

Tactic:
simp only [coeSubmodule, Submodule.mem_map, Algebra.linearMap_apply, Subalgebra.mem_map,
  IsScalarTower.coe_toAlgHom']

Result:
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

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 ∈ Subalgebra.map (IsScalarTower.toAlgHom R S L) (adjoin R {x})) ↔
    ∀ (z : S), y * (algebraMap S L) z ∈ adjoin R {(algebraMap S L) x}

Tactic:
rw [AlgHom.map_adjoin, Set.image_singleton]

Result:
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}

Proof state:
case inr
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 ∈ coeSubmodule L (conductor R x) ↔ ∀ (z : S), y * (algebraMap S L) z ∈ adjoin R {(algebraMap S L) x}

Tactic:
trans ∀ z, y * (algebraMap S L) z ∈ (Algebra.adjoin R {x}).map (IsScalarTower.toAlgHom R S L)

Result:
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 ∈ coeSubmodule L (conductor R x) ↔
    ∀ (z : S), y * (algebraMap S L) z ∈ Subalgebra.map (IsScalarTower.toAlgHom R S L) (adjoin R {x})

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 ∈ Subalgebra.map (IsScalarTower.toAlgHom R S L) (adjoin R {x})) ↔
    ∀ (z : S), y * (algebraMap S L) z ∈ adjoin R {(algebraMap S L) x}

Proof state:
case inl
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✝ : Subsingleton L
⊢ y ∈ ⊤ ↔ ∀ (z : S), y * (algebraMap S L) z ∈ ⊤

Tactic:
simp

Result:
no goals