Theorem: Hilbert90_integral (FltRegular/NumberTheory/Hilbert90.lean)

State before:
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
⊢ ∃ ε, ε ≠ 0 ∧ η * ((galRestrict A K L B) σ) ε = ε
Tactic:
haveI : NoZeroSMulDivisors A L := by
  rw [NoZeroSMulDivisors.iff_algebraMap_injective, IsScalarTower.algebraMap_eq A K L]
  exact (algebraMap K L).injective.comp (IsFractionRing.injective A K)
State after:
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
⊢ ∃ ε, ε ≠ 0 ∧ η * ((galRestrict A K L B) σ) ε = ε

State before:
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
⊢ ∃ ε, ε ≠ 0 ∧ η * ((galRestrict A K L B) σ) ε = ε
Tactic:
haveI := IsIntegralClosure.isFractionRing_of_finite_extension A K L B
State after:
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
⊢ ∃ ε, ε ≠ 0 ∧ η * ((galRestrict A K L B) σ) ε = ε

State before:
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
⊢ ∃ ε, ε ≠ 0 ∧ η * ((galRestrict A K L B) σ) ε = ε
Tactic:
have : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L :=
  IsIntegralClosure.isLocalization A K L B
State after:
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
⊢ ∃ ε, ε ≠ 0 ∧ η * ((galRestrict A K L B) σ) ε = ε

State before:
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
⊢ ∃ ε, ε ≠ 0 ∧ η * ((galRestrict A K L B) σ) ε = ε
Tactic:
obtain ⟨ε, hε⟩ := Hilbert90 hσ hη
State after:
case intro
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
ε : L
hε : (algebraMap B L) η = ε / σ ε
⊢ ∃ ε, ε ≠ 0 ∧ η * ((galRestrict A K L B) σ) ε = ε

State before:
case intro
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
ε : L
hε : (algebraMap B L) η = ε / σ ε
⊢ ∃ ε, ε ≠ 0 ∧ η * ((galRestrict A K L B) σ) ε = ε
Tactic:
obtain ⟨x, y, rfl⟩ := IsLocalization.mk'_surjective (Algebra.algebraMapSubmonoid B A⁰) ε
State after:
case intro.intro.intro
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)
⊢ ∃ ε, ε ≠ 0 ∧ η * ((galRestrict A K L B) σ) ε = ε

State before:
case intro.intro.intro
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)
⊢ ∃ ε, ε ≠ 0 ∧ η * ((galRestrict A K L B) σ) ε = ε
Tactic:
obtain ⟨t, ht, ht'⟩ := y.prop
State after:
case intro.intro.intro.intro.intro
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
⊢ ∃ ε, ε ≠ 0 ∧ η * ((galRestrict A K L B) σ) ε = ε

State before:
case intro.intro.intro.intro.intro
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
⊢ ∃ ε, ε ≠ 0 ∧ η * ((galRestrict A K L B) σ) ε = ε
Tactic:
have : t • IsLocalization.mk' L x y = algebraMap _ _ x := by
  rw [Algebra.smul_def, IsScalarTower.algebraMap_apply A B L, ht', IsLocalization.mk'_spec']
State after:
case intro.intro.intro.intro.intro
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
⊢ ∃ ε, ε ≠ 0 ∧ η * ((galRestrict A K L B) σ) ε = ε

State before:
case intro.intro.intro.intro.intro
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
⊢ ∃ ε, ε ≠ 0 ∧ η * ((galRestrict A K L B) σ) ε = ε
Tactic:
refine ⟨x, ?_, ?_⟩
State after:
case intro.intro.intro.intro.intro.refine_1
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
⊢ x ≠ 0

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
⊢ η * ((galRestrict A K L B) σ) x = x

State before:
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
⊢ NoZeroSMulDivisors A L
Tactic:
rw [NoZeroSMulDivisors.iff_algebraMap_injective, IsScalarTower.algebraMap_eq A K L]
State after:
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
⊢ Function.Injective ⇑((algebraMap K L).comp (algebraMap A K))

State before:
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
⊢ Function.Injective ⇑((algebraMap K L).comp (algebraMap A K))
Tactic:
exact (algebraMap K L).injective.comp (IsFractionRing.injective A K)
State after:
no goals

State before:
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
⊢ t • IsLocalization.mk' L x y = (algebraMap B L) x
Tactic:
rw [Algebra.smul_def, IsScalarTower.algebraMap_apply A B L, ht', IsLocalization.mk'_spec']
State after:
no goals

State before:
case intro.intro.intro.intro.intro.refine_1
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
⊢ x ≠ 0
Tactic:
rintro rfl
State after:
case intro.intro.intro.intro.intro.refine_1
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
y : ↥(Algebra.algebraMapSubmonoid B A⁰)
t : A
ht : t ∈ ↑A⁰
ht' : (algebraMap A B) t = ↑y
hε : (algebraMap B L) η = IsLocalization.mk' L 0 y / σ (IsLocalization.mk' L 0 y)
this : t • IsLocalization.mk' L 0 y = (algebraMap B L) 0
⊢ False

State before:
case intro.intro.intro.intro.intro.refine_1
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
y : ↥(Algebra.algebraMapSubmonoid B A⁰)
t : A
ht : t ∈ ↑A⁰
ht' : (algebraMap A B) t = ↑y
hε : (algebraMap B L) η = IsLocalization.mk' L 0 y / σ (IsLocalization.mk' L 0 y)
this : t • IsLocalization.mk' L 0 y = (algebraMap B L) 0
⊢ False
Tactic:
simp only [IsLocalization.mk'_zero, _root_.map_zero, ne_eq, not_true, div_zero] at hε
State after:
case intro.intro.intro.intro.intro.refine_1
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
y : ↥(Algebra.algebraMapSubmonoid B A⁰)
t : A
ht : t ∈ ↑A⁰
ht' : (algebraMap A B) t = ↑y
this : t • IsLocalization.mk' L 0 y = (algebraMap B L) 0
hε : (algebraMap B L) η = 0
⊢ False

State before:
case intro.intro.intro.intro.intro.refine_1
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
y : ↥(Algebra.algebraMapSubmonoid B A⁰)
t : A
ht : t ∈ ↑A⁰
ht' : (algebraMap A B) t = ↑y
this : t • IsLocalization.mk' L 0 y = (algebraMap B L) 0
hε : (algebraMap B L) η = 0
⊢ False
Tactic:
rw [hε, Algebra.norm_zero] at hη
State after:
case intro.intro.intro.intro.intro.refine_1
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η : 0 = 1
this✝² : NoZeroSMulDivisors A L
this✝¹ : IsFractionRing B L
this✝ : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L
y : ↥(Algebra.algebraMapSubmonoid B A⁰)
t : A
ht : t ∈ ↑A⁰
ht' : (algebraMap A B) t = ↑y
this : t • IsLocalization.mk' L 0 y = (algebraMap B L) 0
hε : (algebraMap B L) η = 0
⊢ False

State before:
case intro.intro.intro.intro.intro.refine_1
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η : 0 = 1
this✝² : NoZeroSMulDivisors A L
this✝¹ : IsFractionRing B L
this✝ : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L
y : ↥(Algebra.algebraMapSubmonoid B A⁰)
t : A
ht : t ∈ ↑A⁰
ht' : (algebraMap A B) t = ↑y
this : t • IsLocalization.mk' L 0 y = (algebraMap B L) 0
hε : (algebraMap B L) η = 0
⊢ False
Tactic:
exact zero_ne_one hη
State after:
no goals

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⁰)
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
⊢ η * ((galRestrict A K L B) σ) x = x
Tactic:
rw [eq_div_iff_mul_eq] at hε
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⁰)
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
⊢ η * ((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

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

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ε : 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
Tactic:
rw [Algebra.smul_def, mul_left_comm, ← Algebra.smul_def t] at hε
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ε : (algebraMap B L) η * t • σ (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

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ε : (algebraMap B L) η * t • σ (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
Tactic:
change (algebraMap B L) η * t • σ.toAlgHom _ = _ at hε
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ε : (algebraMap B L) η * t • ↑σ (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

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ε : (algebraMap B L) η * t • ↑σ (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
Tactic:
rw [← AlgHom.map_smul_of_tower, this] at hε
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ε : (algebraMap B L) η * ↑σ ((algebraMap B L) x) = (algebraMap B L) x
⊢ η * ((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

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ε : (algebraMap B L) η * ↑σ ((algebraMap B L) x) = (algebraMap B L) x
⊢ η * ((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:
apply IsIntegralClosure.algebraMap_injective B A L
State after:
case intro.intro.intro.intro.intro.refine_2.a
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ε : (algebraMap B L) η * ↑σ ((algebraMap B L) x) = (algebraMap B L) x
⊢ (algebraMap B L) (η * ((galRestrict A K L B) σ) x) = (algebraMap B L) 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

State before:
case intro.intro.intro.intro.intro.refine_2.a
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ε : (algebraMap B L) η * ↑σ ((algebraMap B L) x) = (algebraMap B L) x
⊢ (algebraMap B L) (η * ((galRestrict A K L B) σ) x) = (algebraMap B L) 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:
rw [map_mul, ← hε]
State after:
case intro.intro.intro.intro.intro.refine_2.a
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ε : (algebraMap B L) η * ↑σ ((algebraMap B L) x) = (algebraMap B L) x
⊢ (algebraMap B L) η * (algebraMap B L) (((galRestrict A K L B) σ) x) = (algebraMap B L) η * ↑σ ((algebraMap B L) 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

State before:
case intro.intro.intro.intro.intro.refine_2.a
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ε : (algebraMap B L) η * ↑σ ((algebraMap B L) x) = (algebraMap B L) x
⊢ (algebraMap B L) η * (algebraMap B L) (((galRestrict A K L B) σ) x) = (algebraMap B L) η * ↑σ ((algebraMap B L) 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:
congr 1
State after:
case intro.intro.intro.intro.intro.refine_2.a.e_a
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ε : (algebraMap B L) η * ↑σ ((algebraMap B L) x) = (algebraMap B L) x
⊢ (algebraMap B L) (((galRestrict A K L B) σ) x) = ↑σ ((algebraMap B L) 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

State before:
case intro.intro.intro.intro.intro.refine_2.a.e_a
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ε : (algebraMap B L) η * ↑σ ((algebraMap B L) x) = (algebraMap B L) x
⊢ (algebraMap B L) (((galRestrict A K L B) σ) x) = ↑σ ((algebraMap B L) 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:
exact algebraMap_galRestrictHom_apply A K L B σ x
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⁰)
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

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⁰)
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:
intro e
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⁰)
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
e : σ (IsLocalization.mk' L x y) = 0
⊢ False

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⁰)
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
e : σ (IsLocalization.mk' L x y) = 0
⊢ False
Tactic:
rw [(map_eq_zero _).mp e, zero_div] at hε
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⁰)
hε : (algebraMap B L) η = 0
t : A
ht : t ∈ ↑A⁰
ht' : (algebraMap A B) t = ↑y
this : t • IsLocalization.mk' L x y = (algebraMap B L) x
e : σ (IsLocalization.mk' L x y) = 0
⊢ False

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⁰)
hε : (algebraMap B L) η = 0
t : A
ht : t ∈ ↑A⁰
ht' : (algebraMap A B) t = ↑y
this : t • IsLocalization.mk' L x y = (algebraMap B L) x
e : σ (IsLocalization.mk' L x y) = 0
⊢ False
Tactic:
rw [hε, Algebra.norm_zero] at hη
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η : 0 = 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) η = 0
t : A
ht : t ∈ ↑A⁰
ht' : (algebraMap A B) t = ↑y
this : t • IsLocalization.mk' L x y = (algebraMap B L) x
e : σ (IsLocalization.mk' L x y) = 0
⊢ False

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η : 0 = 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) η = 0
t : A
ht : t ∈ ↑A⁰
ht' : (algebraMap A B) t = ↑y
this : t • IsLocalization.mk' L x y = (algebraMap B L) x
e : σ (IsLocalization.mk' L x y) = 0
⊢ False
Tactic:
exact zero_ne_one hη
State after:
no goals