Theorem: lemma1 (FormalisingMathematics2024/Solutions/Section19algebraicNumberTheory/Sheet2.lean)

State before:
K : Type
inst✝² : CommRing K
R : Type
inst✝¹ : CommRing R
inst✝ : Algebra R K
a : K
⊢ IsIntegral R a ↔ Submodule.FG (Subalgebra.toSubmodule (Algebra.adjoin R {a}))
Tactic:
constructor
State after:
case mp
K : Type
inst✝² : CommRing K
R : Type
inst✝¹ : CommRing R
inst✝ : Algebra R K
a : K
⊢ IsIntegral R a → Submodule.FG (Subalgebra.toSubmodule (Algebra.adjoin R {a}))

case mpr
K : Type
inst✝² : CommRing K
R : Type
inst✝¹ : CommRing R
inst✝ : Algebra R K
a : K
⊢ Submodule.FG (Subalgebra.toSubmodule (Algebra.adjoin R {a})) → IsIntegral R a

State before:
case mp
K : Type
inst✝² : CommRing K
R : Type
inst✝¹ : CommRing R
inst✝ : Algebra R K
a : K
⊢ IsIntegral R a → Submodule.FG (Subalgebra.toSubmodule (Algebra.adjoin R {a}))
Tactic:
exact IsIntegral.fg_adjoin_singleton
State after:
no goals

State before:
case mpr
K : Type
inst✝² : CommRing K
R : Type
inst✝¹ : CommRing R
inst✝ : Algebra R K
a : K
⊢ Submodule.FG (Subalgebra.toSubmodule (Algebra.adjoin R {a})) → IsIntegral R a
Tactic:
intro h
State after:
case mpr
K : Type
inst✝² : CommRing K
R : Type
inst✝¹ : CommRing R
inst✝ : Algebra R K
a : K
h : Submodule.FG (Subalgebra.toSubmodule (Algebra.adjoin R {a}))
⊢ IsIntegral R a

State before:
case mpr
K : Type
inst✝² : CommRing K
R : Type
inst✝¹ : CommRing R
inst✝ : Algebra R K
a : K
h : Submodule.FG (Subalgebra.toSubmodule (Algebra.adjoin R {a}))
⊢ IsIntegral R a
Tactic:
exact IsIntegral.of_mem_of_fg _ h _ (Algebra.self_mem_adjoin_singleton R a)
State after:
no goals