Theorem: Hilbert90_integral
Proof state before:
case intro.intro.intro.intro.intro.refine_2
K : Type u_1
L : Type u_2
inst✝¹⁷ : Field K
inst✝¹⁶ : Field L
inst✝¹⁵ : NumberField K
inst✝¹⁴ : Algebra K L
inst✝¹³ : IsGalois K L
inst✝¹² : FiniteDimensional K L
σ✝ : L ≃ₐ[K] L
hσ✝ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ✝
η✝ : L
hη✝ : (Algebra.norm K) η✝ = 1
A : Type u_4
B : Type u_3
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra A B
inst✝⁸ : Algebra A L
inst✝⁷ : Algebra A K
inst✝⁶ : Algebra B L
inst✝⁵ : IsScalarTower A B L
inst✝⁴ : IsScalarTower A K L
inst✝³ : IsFractionRing A K
inst✝² : IsDomain A
inst✝¹ : IsIntegralClosure B A L
inst✝ : IsDomain B
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
η : B
hη : (Algebra.norm K) ((algebraMap B L) η) = 1
this✝² : NoZeroSMulDivisors A L
this✝¹ : IsFractionRing B L
this✝ : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L
x : B
y : ↥(Algebra.algebraMapSubmonoid B A⁰)
t : A
ht : t ∈ ↑A⁰
ht' : (algebraMap A B) t = ↑y
this : t • IsLocalization.mk' L x y = (algebraMap B L) x
hε : (fun x => t • x) ((algebraMap B L) η * σ (IsLocalization.mk' L x y)) = (fun x => t • x) (IsLocalization.mk' L x y)
⊢ η * ((galRestrict A K L B) σ) x = x

case intro.intro.intro.intro.intro.refine_2
K : Type u_1
L : Type u_2
inst✝¹⁷ : Field K
inst✝¹⁶ : Field L
inst✝¹⁵ : NumberField K
inst✝¹⁴ : Algebra K L
inst✝¹³ : IsGalois K L
inst✝¹² : FiniteDimensional K L
σ✝ : L ≃ₐ[K] L
hσ✝ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ✝
η✝ : L
hη✝ : (Algebra.norm K) η✝ = 1
A : Type u_4
B : Type u_3
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra A B
inst✝⁸ : Algebra A L
inst✝⁷ : Algebra A K
inst✝⁶ : Algebra B L
inst✝⁵ : IsScalarTower A B L
inst✝⁴ : IsScalarTower A K L
inst✝³ : IsFractionRing A K
inst✝² : IsDomain A
inst✝¹ : IsIntegralClosure B A L
inst✝ : IsDomain B
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
η : B
hη : (Algebra.norm K) ((algebraMap B L) η) = 1
this✝² : NoZeroSMulDivisors A L
this✝¹ : IsFractionRing B L
this✝ : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L
x : B
y : ↥(Algebra.algebraMapSubmonoid B A⁰)
hε : (algebraMap B L) η = IsLocalization.mk' L x y / σ (IsLocalization.mk' L x y)
t : A
ht : t ∈ ↑A⁰
ht' : (algebraMap A B) t = ↑y
this : t • IsLocalization.mk' L x y = (algebraMap B L) x
⊢ σ (IsLocalization.mk' L x y) ≠ 0
Tactic:
simp only at hε
Proof state after:
case intro.intro.intro.intro.intro.refine_2
K : Type u_1
L : Type u_2
inst✝¹⁷ : Field K
inst✝¹⁶ : Field L
inst✝¹⁵ : NumberField K
inst✝¹⁴ : Algebra K L
inst✝¹³ : IsGalois K L
inst✝¹² : FiniteDimensional K L
σ✝ : L ≃ₐ[K] L
hσ✝ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ✝
η✝ : L
hη✝ : (Algebra.norm K) η✝ = 1
A : Type u_4
B : Type u_3
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra A B
inst✝⁸ : Algebra A L
inst✝⁷ : Algebra A K
inst✝⁶ : Algebra B L
inst✝⁵ : IsScalarTower A B L
inst✝⁴ : IsScalarTower A K L
inst✝³ : IsFractionRing A K
inst✝² : IsDomain A
inst✝¹ : IsIntegralClosure B A L
inst✝ : IsDomain B
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
η : B
hη : (Algebra.norm K) ((algebraMap B L) η) = 1
this✝² : NoZeroSMulDivisors A L
this✝¹ : IsFractionRing B L
this✝ : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L
x : B
y : ↥(Algebra.algebraMapSubmonoid B A⁰)
t : A
ht : t ∈ ↑A⁰
ht' : (algebraMap A B) t = ↑y
this : t • IsLocalization.mk' L x y = (algebraMap B L) x
hε : t • ((algebraMap B L) η * σ (IsLocalization.mk' L x y)) = t • IsLocalization.mk' L x y
⊢ η * ((galRestrict A K L B) σ) x = x

case intro.intro.intro.intro.intro.refine_2
K : Type u_1
L : Type u_2
inst✝¹⁷ : Field K
inst✝¹⁶ : Field L
inst✝¹⁵ : NumberField K
inst✝¹⁴ : Algebra K L
inst✝¹³ : IsGalois K L
inst✝¹² : FiniteDimensional K L
σ✝ : L ≃ₐ[K] L
hσ✝ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ✝
η✝ : L
hη✝ : (Algebra.norm K) η✝ = 1
A : Type u_4
B : Type u_3
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra A B
inst✝⁸ : Algebra A L
inst✝⁷ : Algebra A K
inst✝⁶ : Algebra B L
inst✝⁵ : IsScalarTower A B L
inst✝⁴ : IsScalarTower A K L
inst✝³ : IsFractionRing A K
inst✝² : IsDomain A
inst✝¹ : IsIntegralClosure B A L
inst✝ : IsDomain B
σ : L ≃ₐ[K] L
hσ : ∀ (x : L ≃ₐ[K] L), x ∈ Subgroup.zpowers σ
η : B
hη : (Algebra.norm K) ((algebraMap B L) η) = 1
this✝² : NoZeroSMulDivisors A L
this✝¹ : IsFractionRing B L
this✝ : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L
x : B
y : ↥(Algebra.algebraMapSubmonoid B A⁰)
hε : (algebraMap B L) η = IsLocalization.mk' L x y / σ (IsLocalization.mk' L x y)
t : A
ht : t ∈ ↑A⁰
ht' : (algebraMap A B) t = ↑y
this : t • IsLocalization.mk' L x y = (algebraMap B L) x
⊢ σ (IsLocalization.mk' L x y) ≠ 0