awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
Aₘ : Type u_9
Bₘ : Type u_10
inst_3 : CommRing Aₘ
inst_4 : CommRing Bₘ
inst_5 : Algebra Aₘ Bₘ
inst_6 : Algebra A Aₘ
inst_7 : Algebra B Bₘ
inst_8 : Algebra A Bₘ
inst_9 : IsScalarTower A Aₘ Bₘ
inst_10 : IsScalarTower A B Bₘ
M : Submonoid A
inst_11 : IsLocalization M Aₘ
inst_12 : IsLocalization (algebraMapSubmonoid B M) Bₘ
inst_13 : IsIntegrallyClosed A
inst_14 : IsDomain A
inst_15 : IsDomain B
inst_16 : IsIntegrallyClosed B
inst_17 : Algebra.IsIntegral A B
inst_18 : IsTorsionFree A B
inst_19 : IsDomain Aₘ
inst_20 : IsIntegrallyClosed Aₘ
inst_21 : IsDomain Bₘ
inst_22 : IsIntegrallyClosed Bₘ
inst_23 : IsTorsionFree Aₘ Bₘ
inst_24 : Algebra.IsIntegral Aₘ Bₘ
inst_25 : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
x : B
hM : M ≤ A⁰
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
f : Aₘ →+* K := IsLocalization.map (M := M) (T := A⁰) K (RingHom.id A) hM
this_1 : Algebra Aₘ K := f.toAlgebra
this_2 : IsScalarTower A Aₘ K
this_3 : IsFractionRing Aₘ K := ⋯
g : Bₘ →+* L :=
  IsLocalization.map (M := algebraMapSubmonoid B M) (T := algebraMapSubmonoid.{u_1, u_6} (R := A) B A⁰) L (RingHom.id B)
    ⋯
this : Algebra Bₘ L := g.toAlgebra
⊢ IsScalarTower B Bₘ L

Tactic:
have : IsScalarTower B Bₘ L := IsScalarTower.of_algebraMap_eq'
    (by rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, RingHomCompTriple.comp_eq])
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
Aₘ : Type u_9
Bₘ : Type u_10
inst_3 : CommRing Aₘ
inst_4 : CommRing Bₘ
inst_5 : Algebra Aₘ Bₘ
inst_6 : Algebra A Aₘ
inst_7 : Algebra B Bₘ
inst_8 : Algebra A Bₘ
inst_9 : IsScalarTower A Aₘ Bₘ
inst_10 : IsScalarTower A B Bₘ
M : Submonoid A
inst_11 : IsLocalization M Aₘ
inst_12 : IsLocalization (algebraMapSubmonoid B M) Bₘ
inst_13 : IsIntegrallyClosed A
inst_14 : IsDomain A
inst_15 : IsDomain B
inst_16 : IsIntegrallyClosed B
inst_17 : Algebra.IsIntegral A B
inst_18 : IsTorsionFree A B
inst_19 : IsDomain Aₘ
inst_20 : IsIntegrallyClosed Aₘ
inst_21 : IsDomain Bₘ
inst_22 : IsIntegrallyClosed Bₘ
inst_23 : IsTorsionFree Aₘ Bₘ
inst_24 : Algebra.IsIntegral Aₘ Bₘ
inst_25 : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
x : B
hM : M ≤ A⁰
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
f : Aₘ →+* K := IsLocalization.map (M := M) (T := A⁰) K (RingHom.id A) hM
this_1 : Algebra Aₘ K := f.toAlgebra
this_2 : IsScalarTower A Aₘ K
this_3 : IsFractionRing Aₘ K := ⋯
g : Bₘ →+* L :=
  IsLocalization.map (M := algebraMapSubmonoid B M) (T := algebraMapSubmonoid.{u_1, u_6} (R := A) B A⁰) L (RingHom.id B)
    ⋯
this_4 : Algebra Bₘ L := g.toAlgebra
this_5 : IsScalarTower B Bₘ L
this : Algebra Aₘ L := RingHom.toAlgebra (RingHom.comp (algebraMap K L) f)
⊢ IsScalarTower Aₘ K L

Tactic:
have : IsScalarTower Aₘ K L := IsScalarTower.of_algebraMap_eq' rfl
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
Aₘ : Type u_9
Bₘ : Type u_10
inst_3 : CommRing Aₘ
inst_4 : CommRing Bₘ
inst_5 : Algebra Aₘ Bₘ
inst_6 : Algebra A Aₘ
inst_7 : Algebra B Bₘ
inst_8 : Algebra A Bₘ
inst_9 : IsScalarTower A Aₘ Bₘ
inst_10 : IsScalarTower A B Bₘ
M : Submonoid A
inst_11 : IsLocalization M Aₘ
inst_12 : IsLocalization (algebraMapSubmonoid B M) Bₘ
inst_13 : IsIntegrallyClosed A
inst_14 : IsDomain A
inst_15 : IsDomain B
inst_16 : IsIntegrallyClosed B
inst_17 : Algebra.IsIntegral A B
inst_18 : IsTorsionFree A B
inst_19 : IsDomain Aₘ
inst_20 : IsIntegrallyClosed Aₘ
inst_21 : IsDomain Bₘ
inst_22 : IsIntegrallyClosed Bₘ
inst_23 : IsTorsionFree Aₘ Bₘ
inst_24 : Algebra.IsIntegral Aₘ Bₘ
inst_25 : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
x : B
hM : M ≤ A⁰
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
f : Aₘ →+* K := IsLocalization.map (M := M) (T := A⁰) K (RingHom.id A) hM
this_1 : Algebra Aₘ K := f.toAlgebra
this_2 : IsScalarTower A Aₘ K
this_3 : IsFractionRing Aₘ K := ⋯
g : Bₘ →+* L :=
  IsLocalization.map (M := algebraMapSubmonoid B M) (T := algebraMapSubmonoid.{u_1, u_6} (R := A) B A⁰) L (RingHom.id B)
    ⋯
this_4 : Algebra Bₘ L := g.toAlgebra
this_5 : IsScalarTower B Bₘ L
this_6 : Algebra Aₘ L := RingHom.toAlgebra (RingHom.comp (algebraMap K L) f)
this : IsScalarTower Aₘ K L
h :
  Eq (α := Aₘ →+* L) (algebraMap Aₘ L)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Bₘ L) (algebraMap Aₘ Bₘ))
⊢ IsScalarTower Aₘ Bₘ L

Tactic:
apply IsScalarTower.of_algebraMap_eq'

Premises used: IsScalarTower.of_algebraMap_eq'
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
Aₘ : Type u_9
Bₘ : Type u_10
inst_3 : CommRing Aₘ
inst_4 : CommRing Bₘ
inst_5 : Algebra Aₘ Bₘ
inst_6 : Algebra A Aₘ
inst_7 : Algebra B Bₘ
inst_8 : Algebra A Bₘ
inst_9 : IsScalarTower A Aₘ Bₘ
inst_10 : IsScalarTower A B Bₘ
M : Submonoid A
inst_11 : IsLocalization M Aₘ
inst_12 : IsLocalization (algebraMapSubmonoid B M) Bₘ
inst_13 : IsIntegrallyClosed A
inst_14 : IsDomain A
inst_15 : IsDomain B
inst_16 : IsIntegrallyClosed B
inst_17 : Algebra.IsIntegral A B
inst_18 : IsTorsionFree A B
inst_19 : IsDomain Aₘ
inst_20 : IsIntegrallyClosed Aₘ
inst_21 : IsDomain Bₘ
inst_22 : IsIntegrallyClosed Bₘ
inst_23 : IsTorsionFree Aₘ Bₘ
inst_24 : Algebra.IsIntegral Aₘ Bₘ
inst_25 : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
x : B
hM : M ≤ A⁰
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
f : Aₘ →+* K := IsLocalization.map (M := M) (T := A⁰) K (RingHom.id A) hM
this_1 : Algebra Aₘ K := f.toAlgebra
this_2 : IsScalarTower A Aₘ K
this_3 : IsFractionRing Aₘ K := ⋯
g : Bₘ →+* L :=
  IsLocalization.map (M := algebraMapSubmonoid B M) (T := algebraMapSubmonoid.{u_1, u_6} (R := A) B A⁰) L (RingHom.id B)
    ⋯
this_4 : Algebra Bₘ L := g.toAlgebra
this_5 : IsScalarTower B Bₘ L
this_6 : Algebra Aₘ L := RingHom.toAlgebra (RingHom.comp (algebraMap K L) f)
this : IsScalarTower Aₘ K L
h :
  Eq (α := A →+* L) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Aₘ L) (algebraMap A Aₘ))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Bₘ L) (algebraMap Aₘ Bₘ)) (algebraMap A Aₘ))
⊢ Eq (α := Aₘ →+* L) (algebraMap Aₘ L)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap Bₘ L) (algebraMap Aₘ Bₘ))

Tactic:
apply IsLocalization.ringHom_ext M

Premises used: IsLocalization.ringHom_ext
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
Aₘ : Type u_9
Bₘ : Type u_10
inst_3 : CommRing Aₘ
inst_4 : CommRing Bₘ
inst_5 : Algebra Aₘ Bₘ
inst_6 : Algebra A Aₘ
inst_7 : Algebra B Bₘ
inst_8 : Algebra A Bₘ
inst_9 : IsScalarTower A Aₘ Bₘ
inst_10 : IsScalarTower A B Bₘ
M : Submonoid A
inst_11 : IsLocalization M Aₘ
inst_12 : IsLocalization (algebraMapSubmonoid B M) Bₘ
inst_13 : IsIntegrallyClosed A
inst_14 : IsDomain A
inst_15 : IsDomain B
inst_16 : IsIntegrallyClosed B
inst_17 : Algebra.IsIntegral A B
inst_18 : IsTorsionFree A B
inst_19 : IsDomain Aₘ
inst_20 : IsIntegrallyClosed Aₘ
inst_21 : IsDomain Bₘ
inst_22 : IsIntegrallyClosed Bₘ
inst_23 : IsTorsionFree Aₘ Bₘ
inst_24 : Algebra.IsIntegral Aₘ Bₘ
inst_25 : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
x : B
hM : M ≤ A⁰
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
f : Aₘ →+* K := IsLocalization.map (M := M) (T := A⁰) K (RingHom.id A) hM
this_1 : Algebra Aₘ K := f.toAlgebra
this_2 : IsScalarTower A Aₘ K
this_3 : IsFractionRing Aₘ K := ⋯
g : Bₘ →+* L :=
  IsLocalization.map (M := algebraMapSubmonoid B M) (T := algebraMapSubmonoid.{u_1, u_6} (R := A) B A⁰) L (RingHom.id B)
    ⋯
this_4 : Algebra Bₘ L := g.toAlgebra
this_5 : IsScalarTower B Bₘ L
this_6 : Algebra Aₘ L := RingHom.toAlgebra (RingHom.comp (algebraMap K L) f)
this : IsScalarTower Aₘ K L
⊢ IsScalarTower Aₘ Bₘ L

Tactic:
have : IsScalarTower Aₘ Bₘ L := by
    apply IsScalarTower.of_algebraMap_eq'
    apply IsLocalization.ringHom_ext M
    rw [RingHom.algebraMap_toAlgebra, RingHom.algebraMap_toAlgebra (R := Bₘ), RingHom.comp_assoc,
      RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq, IsScalarTower.algebraMap_eq A B Bₘ,
      IsLocalization.map_comp, RingHom.comp_id, ← RingHom.comp_assoc, IsLocalization.map_comp,
      RingHom.comp_id, ← IsScalarTower.algebraMap_eq, ← IsScalarTower.algebraMap_eq]
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
Aₘ : Type u_9
Bₘ : Type u_10
inst_3 : CommRing Aₘ
inst_4 : CommRing Bₘ
inst_5 : Algebra Aₘ Bₘ
inst_6 : Algebra A Aₘ
inst_7 : Algebra B Bₘ
inst_8 : Algebra A Bₘ
inst_9 : IsScalarTower A Aₘ Bₘ
inst_10 : IsScalarTower A B Bₘ
M : Submonoid A
inst_11 : IsLocalization M Aₘ
inst_12 : IsLocalization (algebraMapSubmonoid B M) Bₘ
inst_13 : IsIntegrallyClosed A
inst_14 : IsDomain A
inst_15 : IsDomain B
inst_16 : IsIntegrallyClosed B
inst_17 : Algebra.IsIntegral A B
inst_18 : IsTorsionFree A B
inst_19 : IsDomain Aₘ
inst_20 : IsIntegrallyClosed Aₘ
inst_21 : IsDomain Bₘ
inst_22 : IsIntegrallyClosed Bₘ
inst_23 : IsTorsionFree Aₘ Bₘ
inst_24 : Algebra.IsIntegral Aₘ Bₘ
inst_25 : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
x : B
hM : M ≤ A⁰
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
f : Aₘ →+* K := IsLocalization.map (M := M) (T := A⁰) K (RingHom.id A) hM
this_1 : Algebra Aₘ K := f.toAlgebra
this_2 : IsScalarTower A Aₘ K
this_3 : IsFractionRing Aₘ K := ⋯
g : Bₘ →+* L :=
  IsLocalization.map (M := algebraMapSubmonoid B M) (T := algebraMapSubmonoid.{u_1, u_6} (R := A) B A⁰) L (RingHom.id B)
    ⋯
this_4 : Algebra Bₘ L := g.toAlgebra
this_5 : IsScalarTower B Bₘ L
this_6 : Algebra Aₘ L := RingHom.toAlgebra (RingHom.comp (algebraMap K L) f)
this_7 : IsScalarTower Aₘ K L
this_8 : IsScalarTower Aₘ Bₘ L
this : IsFractionRing Bₘ L := ⋯
⊢ IsIntegralClosure Bₘ Aₘ L

Tactic:
have : IsIntegralClosure Bₘ Aₘ L :=
    IsIntegralClosure.of_isIntegrallyClosed _ _ _
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
Aₘ : Type u_9
Bₘ : Type u_10
inst_3 : CommRing Aₘ
inst_4 : CommRing Bₘ
inst_5 : Algebra Aₘ Bₘ
inst_6 : Algebra A Aₘ
inst_7 : Algebra B Bₘ
inst_8 : Algebra A Bₘ
inst_9 : IsScalarTower A Aₘ Bₘ
inst_10 : IsScalarTower A B Bₘ
M : Submonoid A
inst_11 : IsLocalization M Aₘ
inst_12 : IsLocalization (algebraMapSubmonoid B M) Bₘ
inst_13 : IsIntegrallyClosed A
inst_14 : IsDomain A
inst_15 : IsDomain B
inst_16 : IsIntegrallyClosed B
inst_17 : Algebra.IsIntegral A B
inst_18 : IsTorsionFree A B
inst_19 : IsDomain Aₘ
inst_20 : IsIntegrallyClosed Aₘ
inst_21 : IsDomain Bₘ
inst_22 : IsIntegrallyClosed Bₘ
inst_23 : IsTorsionFree Aₘ Bₘ
inst_24 : Algebra.IsIntegral Aₘ Bₘ
inst_25 : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
x : B
hM : M ≤ A⁰
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
f : Aₘ →+* K := IsLocalization.map (M := M) (T := A⁰) K (RingHom.id A) hM
this_1 : Algebra Aₘ K := f.toAlgebra
this_2 : IsScalarTower A Aₘ K
this_3 : IsFractionRing Aₘ K := ⋯
g : Bₘ →+* L :=
  IsLocalization.map (M := algebraMapSubmonoid B M) (T := algebraMapSubmonoid.{u_1, u_6} (R := A) B A⁰) L (RingHom.id B)
    ⋯
this_4 : Algebra Bₘ L := g.toAlgebra
this_5 : IsScalarTower B Bₘ L
this_6 : Algebra Aₘ L := RingHom.toAlgebra (RingHom.comp (algebraMap K L) f)
this_7 : IsScalarTower Aₘ K L
this_8 : IsScalarTower Aₘ Bₘ L
this_9 : IsFractionRing Bₘ L := ⋯
this : IsIntegralClosure Bₘ Aₘ L
neg :
  Eq.{u_1 + 1} (α := K)
    (((algebraMap Aₘ K : Aₘ →+* K) : (a : Aₘ) → K)
        ((algebraMap A Aₘ : (a : A) → Aₘ) ((intNorm A B : (a : B) → A) x : A)) :
      K)
    (((algebraMap Aₘ K : Aₘ →+* K) : (a : Aₘ) → K)
        ((intNorm Aₘ Bₘ : (a : Bₘ) → Aₘ) ((algebraMap B Bₘ : (a : B) → Bₘ) x : Bₘ)) :
      K)
⊢ Eq.{u_9 + 1} (α := Aₘ) ((algebraMap A Aₘ : (a : A) → Aₘ) ((intNorm A B : (a : B) → A) x : A) : Aₘ)
    ((intNorm Aₘ Bₘ : (a : Bₘ) → Aₘ) ((algebraMap B Bₘ : (a : B) → Bₘ) x : Bₘ) : Aₘ)

Tactic:
apply IsFractionRing.injective Aₘ K

Premises used: IsFractionRing.injective
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsIntegrallyClosed A
inst_5 : IsDomain B
inst_6 : IsIntegrallyClosed B
inst_7 : Module.Finite A B
inst_8 : IsTorsionFree A B
inst_9 : IsGalois.{u_1, u_6} (FractionRing A) (FractionRing B)
x : B
⊢ FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)

Tactic:
haveI : FiniteDimensional (FractionRing A) (FractionRing B) := .of_isLocalization A B A⁰
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsIntegrallyClosed A
inst_5 : IsDomain B
inst_6 : IsIntegrallyClosed B
inst_7 : Module.Finite A B
inst_8 : IsTorsionFree A B
inst_9 : IsGalois.{u_1, u_6} (FractionRing A) (FractionRing B)
x : B
this : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
rw :
  Eq.{u_6 + 1} (α := B) ((algebraMap A B : (a : A) → B) ((intNorm A B : (a : B) → A) x : A) : B)
    (∏ i : Gal(FractionRing B/FractionRing A),
        ((((MulEquiv.toEquiv (galRestrict A (FractionRing A) (FractionRing B) B) :
                    Gal(FractionRing B/FractionRing A) ≃ B ≃ₐ[A] B) :
                  (a : Gal(FractionRing B/FractionRing A)) → B ≃ₐ[A] B)
                i :
              B ≃ₐ[A] B) :
            (a : B) → B)
          x :
      B)
⊢ Eq.{u_6 + 1} (α := B) ((algebraMap A B : (a : A) → B) ((intNorm A B : (a : B) → A) x : A) : B)
    (∏ σ : B ≃ₐ[A] B, (σ : (a : B) → B) x : B)

Tactic:
rw [← (galRestrict A (FractionRing A) (FractionRing B) B).toEquiv.prod_comp]

Premises used: FractionRing, MulEquiv.toEquiv, Equiv.prod_comp, galRestrict
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsIntegrallyClosed A
inst_5 : IsDomain B
inst_6 : IsIntegrallyClosed B
inst_7 : Module.Finite A B
inst_8 : IsTorsionFree A B
inst_9 : IsGalois.{u_1, u_6} (FractionRing A) (FractionRing B)
x : B
this : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
simp :
  Eq.{u_6 + 1} (α := B) ((algebraMap A B : (a : A) → B) ((intNorm A B : (a : B) → A) x : A) : B)
    (∏ x_1 : Gal(FractionRing B/FractionRing A),
        ((((galRestrict A (FractionRing A) (FractionRing B) B : Gal(FractionRing B/FractionRing A) ≃* B ≃ₐ[A] B) :
                  (a : Gal(FractionRing B/FractionRing A)) → B ≃ₐ[A] B)
                x_1 :
              B ≃ₐ[A] B) :
            (a : B) → B)
          x :
      B)
⊢ Eq.{u_6 + 1} (α := B) ((algebraMap A B : (a : A) → B) ((intNorm A B : (a : B) → A) x : A) : B)
    (∏ i : Gal(FractionRing B/FractionRing A),
        ((((MulEquiv.toEquiv (galRestrict A (FractionRing A) (FractionRing B) B) :
                    Gal(FractionRing B/FractionRing A) ≃ B ≃ₐ[A] B) :
                  (a : Gal(FractionRing B/FractionRing A)) → B ≃ₐ[A] B)
                i :
              B ≃ₐ[A] B) :
            (a : B) → B)
          x :
      B)

Tactic:
simp only [MulEquiv.toEquiv_eq_coe, EquivLike.coe_coe]

Premises used: MulEquiv.toEquiv_eq_coe, EquivLike.coe_coe
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsIntegrallyClosed A
inst_5 : IsDomain B
inst_6 : IsIntegrallyClosed B
inst_7 : Module.Finite A B
inst_8 : IsTorsionFree A B
inst_9 : IsGalois.{u_1, u_6} (FractionRing A) (FractionRing B)
x : B
this : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
⊢ Eq.{u_6 + 1} (α := B)
    ((algebraMap A B : (a : A) → B)
        (IsIntegralClosure.mk' A (B := FractionRing A)
          ((norm (FractionRing A) : (a : FractionRing B) → FractionRing A)
              ((algebraMap B (FractionRing B) : (a : B) → FractionRing B) x) :
            FractionRing A)
          ⋯) :
      B)
    (∏ σ : Gal(FractionRing B/FractionRing A),
        ((((galRestrict A (FractionRing A) (FractionRing B) B : Gal(FractionRing B/FractionRing A) ≃* B ≃ₐ[A] B) :
                  (a : Gal(FractionRing B/FractionRing A)) → B ≃ₐ[A] B)
                σ :
              B ≃ₐ[A] B) :
            (a : B) → B)
          x :
      B)

Tactic:
(prod_galRestrict_eq_norm A (FractionRing A) (FractionRing B) B x).symm

Premises used: FractionRing, Eq.symm, prod_galRestrict_eq_norm
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsIntegrallyClosed A
inst_5 : IsDomain B
inst_6 : IsIntegrallyClosed B
inst_7 : Module.Finite A B
inst_8 : IsTorsionFree A B
inst_9 : IsGalois.{u_1, u_6} (FractionRing A) (FractionRing B)
x : B
this : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
⊢ Eq.{u_6 + 1} (α := B) ((algebraMap A B : (a : A) → B) ((intNorm A B : (a : B) → A) x : A) : B)
    (∏ x_1 : Gal(FractionRing B/FractionRing A),
        ((((galRestrict A (FractionRing A) (FractionRing B) B : Gal(FractionRing B/FractionRing A) ≃* B ≃ₐ[A] B) :
                  (a : Gal(FractionRing B/FractionRing A)) → B ≃ₐ[A] B)
                x_1 :
              B ≃ₐ[A] B) :
            (a : B) → B)
          x :
      B)

Tactic:
convert! (prod_galRestrict_eq_norm A (FractionRing A) (FractionRing B) B x).symm

Premises used: FractionRing, Eq.symm, prod_galRestrict_eq_norm
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsIntegrallyClosed A
inst_5 : IsDomain B
inst_6 : IsIntegrallyClosed B
inst_7 : Module.Finite A B
inst_8 : IsTorsionFree A B
x : B
⊢ FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)

Tactic:
haveI : FiniteDimensional (FractionRing A) (FractionRing B) := .of_isLocalization A B A⁰
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsIntegrallyClosed A
inst_5 : IsDomain B
inst_6 : IsIntegrallyClosed B
inst_7 : Module.Finite A B
inst_8 : IsTorsionFree A B
x : B
this : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
pos : ∀ (hx : x = 0), x ∣ (algebraMap A B : (a : A) → B) ((intNorm A B : (a : B) → A) x : A)
neg : ∀ (hx : ¬x = 0), x ∣ (algebraMap A B : (a : A) → B) ((intNorm A B : (a : B) → A) x : A)
⊢ x ∣ (algebraMap A B : (a : A) → B) ((intNorm A B : (a : B) → A) x : A)

Tactic:
by_cases hx : x = 0
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsIntegrallyClosed A
inst_5 : IsDomain B
inst_6 : IsIntegrallyClosed B
inst_7 : Module.Finite A B
inst_8 : IsTorsionFree A B
x : B
this : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
hx : x = 0
⊢ (algebraMap A B : (a : A) → B) ((intNorm A B : (a : B) → A) x : A) = x * 1

Tactic:
simp [hx]
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsIntegrallyClosed A
inst_5 : IsDomain B
inst_6 : IsIntegrallyClosed B
inst_7 : Module.Finite A B
inst_8 : IsTorsionFree A B
x : B
this : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
hx : x = 0
⊢ x ∣ (algebraMap A B : (a : A) → B) ((intNorm A B : (a : B) → A) x : A)

Tactic:
exact ⟨1, by simp [hx]⟩
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsIntegrallyClosed A
inst_5 : IsDomain B
inst_6 : IsIntegrallyClosed B
inst_7 : Module.Finite A B
inst_8 : IsTorsionFree A B
x : B
this_1 : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
hx : ¬x = 0
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
E : Type u_6 := AlgebraicClosure L
this :
  IsIntegral A
    (HMul.hMul (α := L) (β := L) (((algebraMap B L : (a : B) → L) x)⁻¹ : L)
      (((algebraMap A L : A →+* L) : (a : A) → L) ((intNorm A B : (a : B) → A) x) : L))
obtain :
  ∀ (y : B)
    (hy :
      (algebraMap B L : (a : B) → L) y =
        HMul.hMul (α := L) (β := L) (((algebraMap B L : (a : B) → L) x)⁻¹ : L)
          (((algebraMap A L : A →+* L) : (a : A) → L) ((intNorm A B : (a : B) → A) x) : L)),
    x ∣ (algebraMap A B : (a : A) → B) ((intNorm A B : (a : B) → A) x : A)
⊢ x ∣ (algebraMap A B : (a : A) → B) ((intNorm A B : (a : B) → A) x : A)

Tactic:
obtain ⟨y, hy⟩ := IsIntegrallyClosed.isIntegral_iff.mp <|
      _root_.IsIntegral.tower_top (A := B) this

Premises used: IsIntegrallyClosed.isIntegral_iff, Iff.mp, IsIntegral.tower_top
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsIntegrallyClosed A
inst_5 : IsDomain B
inst_6 : IsIntegrallyClosed B
inst_7 : Module.Finite A B
inst_8 : IsTorsionFree A B
x : B
this_1 : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
hx : ¬x = 0
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
E : Type u_6 := AlgebraicClosure L
this :
  IsIntegral A
    (HMul.hMul (α := L) (β := L) (((algebraMap B L : (a : B) → L) x)⁻¹ : L)
      (((algebraMap A L : A →+* L) : (a : A) → L) ((intNorm A B : (a : B) → A) x) : L))
y : B
hy :
  (algebraMap B L : (a : B) → L) y =
    HMul.hMul (α := L) (β := L) (((algebraMap B L : (a : B) → L) x)⁻¹ : L)
      (((algebraMap A L : A →+* L) : (a : A) → L) ((intNorm A B : (a : B) → A) x) : L)
⊢ x ∣ (algebraMap A B : (a : A) → B) ((intNorm A B : (a : B) → A) x : A)

Tactic:
⟨y, ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain A
inst_4 : IsIntegrallyClosed A
inst_5 : IsDomain B
inst_6 : IsIntegrallyClosed B
inst_7 : Module.Finite A B
inst_8 : IsTorsionFree A B
x : B
this_1 : FiniteDimensional.{u_1, u_6} (FractionRing A) (FractionRing B)
hx : ¬x = 0
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
E : Type u_6 := AlgebraicClosure L
this :
  IsIntegral A
    (HMul.hMul (α := L) (β := L) (((algebraMap B L : (a : B) → L) x)⁻¹ : L)
      (((algebraMap A L : A →+* L) : (a : A) → L) ((intNorm A B : (a : B) → A) x) : L))
y : B
hy :
  (algebraMap B L : (a : B) → L) y =
    HMul.hMul (α := L) (β := L) (((algebraMap B L : (a : B) → L) x)⁻¹ : L)
      (((algebraMap A L : A →+* L) : (a : A) → L) ((intNorm A B : (a : B) → A) x) : L)
refine : (algebraMap A B : (a : A) → B) ((intNorm A B : (a : B) → A) x : A) = x * y
⊢ x ∣ (algebraMap A B : (a : A) → B) ((intNorm A B : (a : B) → A) x : A)

Tactic:
refine ⟨y, ?_⟩