Theorem: KummersLemma.isIntegralClosure_of_isScalarTower (FltRegular/NumberTheory/KummersLemma/Field.lean)

State before:
K✝ : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝¹⁷ : Field K✝
inst✝¹⁶ : NumberField K✝
inst✝¹⁵ : IsCyclotomicExtension {p} ℚ K✝
hp : p ≠ 2
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K✝)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K✝), v ^ ↑p ≠ (algebraMap (𝓞 K✝) K✝) ↑u
R : Type u_2
A : Type u_3
K : Type u_4
L : Type u_5
B : Type u_6
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing A
inst✝¹² : CommRing K
inst✝¹¹ : CommRing L
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra R K
inst✝⁸ : Algebra A K
inst✝⁷ : Algebra R L
inst✝⁶ : Algebra B L
inst✝⁵ : Algebra A L
inst✝⁴ : Algebra R A
inst✝³ : IsScalarTower R A K
inst✝² : IsScalarTower R A L
inst✝¹ : IsIntegralClosure A R K
inst✝ : IsIntegralClosure B R L
x : L
⊢ IsIntegral A x ↔ ∃ y, (algebraMap B L) y = x
Tactic:
refine Iff.trans ?_ (IsIntegralClosure.isIntegral_iff (R := R) (A := B) (B := L))
State after:
K✝ : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝¹⁷ : Field K✝
inst✝¹⁶ : NumberField K✝
inst✝¹⁵ : IsCyclotomicExtension {p} ℚ K✝
hp : p ≠ 2
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K✝)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K✝), v ^ ↑p ≠ (algebraMap (𝓞 K✝) K✝) ↑u
R : Type u_2
A : Type u_3
K : Type u_4
L : Type u_5
B : Type u_6
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing A
inst✝¹² : CommRing K
inst✝¹¹ : CommRing L
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra R K
inst✝⁸ : Algebra A K
inst✝⁷ : Algebra R L
inst✝⁶ : Algebra B L
inst✝⁵ : Algebra A L
inst✝⁴ : Algebra R A
inst✝³ : IsScalarTower R A K
inst✝² : IsScalarTower R A L
inst✝¹ : IsIntegralClosure A R K
inst✝ : IsIntegralClosure B R L
x : L
⊢ IsIntegral A x ↔ IsIntegral R x

State before:
K✝ : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝¹⁷ : Field K✝
inst✝¹⁶ : NumberField K✝
inst✝¹⁵ : IsCyclotomicExtension {p} ℚ K✝
hp : p ≠ 2
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K✝)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K✝), v ^ ↑p ≠ (algebraMap (𝓞 K✝) K✝) ↑u
R : Type u_2
A : Type u_3
K : Type u_4
L : Type u_5
B : Type u_6
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing A
inst✝¹² : CommRing K
inst✝¹¹ : CommRing L
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra R K
inst✝⁸ : Algebra A K
inst✝⁷ : Algebra R L
inst✝⁶ : Algebra B L
inst✝⁵ : Algebra A L
inst✝⁴ : Algebra R A
inst✝³ : IsScalarTower R A K
inst✝² : IsScalarTower R A L
inst✝¹ : IsIntegralClosure A R K
inst✝ : IsIntegralClosure B R L
x : L
⊢ IsIntegral A x ↔ IsIntegral R x
Tactic:
have := (IsIntegralClosure.isIntegral_algebra R (A := A) K)
State after:
K✝ : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝¹⁷ : Field K✝
inst✝¹⁶ : NumberField K✝
inst✝¹⁵ : IsCyclotomicExtension {p} ℚ K✝
hp : p ≠ 2
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K✝)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K✝), v ^ ↑p ≠ (algebraMap (𝓞 K✝) K✝) ↑u
R : Type u_2
A : Type u_3
K : Type u_4
L : Type u_5
B : Type u_6
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing A
inst✝¹² : CommRing K
inst✝¹¹ : CommRing L
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra R K
inst✝⁸ : Algebra A K
inst✝⁷ : Algebra R L
inst✝⁶ : Algebra B L
inst✝⁵ : Algebra A L
inst✝⁴ : Algebra R A
inst✝³ : IsScalarTower R A K
inst✝² : IsScalarTower R A L
inst✝¹ : IsIntegralClosure A R K
inst✝ : IsIntegralClosure B R L
x : L
this : Algebra.IsIntegral R A
⊢ IsIntegral A x ↔ IsIntegral R x

State before:
K✝ : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝¹⁷ : Field K✝
inst✝¹⁶ : NumberField K✝
inst✝¹⁵ : IsCyclotomicExtension {p} ℚ K✝
hp : p ≠ 2
ζ : K✝
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K✝)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K✝), v ^ ↑p ≠ (algebraMap (𝓞 K✝) K✝) ↑u
R : Type u_2
A : Type u_3
K : Type u_4
L : Type u_5
B : Type u_6
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing A
inst✝¹² : CommRing K
inst✝¹¹ : CommRing L
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra R K
inst✝⁸ : Algebra A K
inst✝⁷ : Algebra R L
inst✝⁶ : Algebra B L
inst✝⁵ : Algebra A L
inst✝⁴ : Algebra R A
inst✝³ : IsScalarTower R A K
inst✝² : IsScalarTower R A L
inst✝¹ : IsIntegralClosure A R K
inst✝ : IsIntegralClosure B R L
x : L
this : Algebra.IsIntegral R A
⊢ IsIntegral A x ↔ IsIntegral R x
Tactic:
exact ⟨isIntegral_trans x, IsIntegral.tower_top⟩
State after:
no goals