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 : IsDomain A
inst_14 : IsIntegrallyClosed A
inst_15 : IsDomain B
inst_16 : IsIntegrallyClosed B
inst_17 : Module.Finite 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 : Module.Finite Aₘ Bₘ
x : B
hM : M ≤ A⁰
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
this_1 : IsIntegralClosure B A L
this_2 : Algebra.IsAlgebraic.{u_1, u_6} (FractionRing A) (FractionRing B)
this_3 : IsLocalization (algebraMapSubmonoid.{u_1, u_6} (R := A) B A⁰) L
f : Aₘ →+* K := IsLocalization.map (M := M) (T := A⁰) K (RingHom.id A) hM
this_4 : Algebra Aₘ K := f.toAlgebra
this_5 : IsScalarTower A Aₘ K
this_6 : 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_7 : Algebra Bₘ L := g.toAlgebra
this_8 : IsScalarTower B Bₘ L
this_9 : Algebra Aₘ L := RingHom.toAlgebra (RingHom.comp (algebraMap K L) f)
this_10 : IsScalarTower Aₘ K L
this_11 : IsScalarTower Aₘ Bₘ L
this_12 : IsFractionRing Bₘ L := ⋯
this : FiniteDimensional K 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 : IsDomain A
inst_14 : IsIntegrallyClosed A
inst_15 : IsDomain B
inst_16 : IsIntegrallyClosed B
inst_17 : Module.Finite 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 : Module.Finite Aₘ Bₘ
x : B
hM : M ≤ A⁰
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
this_1 : IsIntegralClosure B A L
this_2 : Algebra.IsAlgebraic.{u_1, u_6} (FractionRing A) (FractionRing B)
this_3 : IsLocalization (algebraMapSubmonoid.{u_1, u_6} (R := A) B A⁰) L
f : Aₘ →+* K := IsLocalization.map (M := M) (T := A⁰) K (RingHom.id A) hM
this_4 : Algebra Aₘ K := f.toAlgebra
this_5 : IsScalarTower A Aₘ K
this_6 : 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_7 : Algebra Bₘ L := g.toAlgebra
this_8 : IsScalarTower B Bₘ L
this_9 : Algebra Aₘ L := RingHom.toAlgebra (RingHom.comp (algebraMap K L) f)
this_10 : IsScalarTower Aₘ K L
this_11 : IsScalarTower Aₘ Bₘ L
this_12 : IsFractionRing Bₘ L := ⋯
this_13 : FiniteDimensional K 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ₘ) ((intTrace A B : (a : B) → A) x : A)) :
      K)
    (((algebraMap Aₘ K : Aₘ →+* K) : (a : Aₘ) → K)
        ((intTrace 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ₘ) ((intTrace A B : (a : B) → A) x : A) : Aₘ)
    ((intTrace 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
K : Type u_2
L : Type u_3
L₂ : Type u_4
L₃ : Type u_5
B : Type u_6
B₂ : Type u_7
B₃ : Type u_8
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing B₂
inst_3 : CommRing B₃
inst_4 : Algebra A B
inst_5 : Algebra A B₂
inst_6 : Algebra A B₃
inst_7 : Field K
inst_8 : Field L
inst_9 : Field L₂
inst_10 : Field L₃
inst_11 : Algebra A K
inst_12 : IsFractionRing A K
inst_13 : Algebra K L
inst_14 : Algebra A L
inst_15 : IsScalarTower A K L
inst_16 : Algebra K L₂
inst_17 : Algebra A L₂
inst_18 : IsScalarTower A K L₂
inst_19 : Algebra K L₃
inst_20 : Algebra A L₃
inst_21 : IsScalarTower A K L₃
inst_22 : Algebra B L
inst_23 : IsScalarTower A B L
inst_24 : IsIntegralClosure B A L
inst_25 : Algebra B₂ L₂
inst_26 : IsScalarTower A B₂ L₂
inst_27 : IsIntegralClosure B₂ A L₂
inst_28 : Algebra B₃ L₃
inst_29 : IsScalarTower A B₃ L₃
inst_30 : IsIntegralClosure B₃ A L₃
inst_31 : FiniteDimensional K L
Aₘ : Type ?u.308446
Bₘ : Type ?u.308449
inst_32 : CommRing Aₘ
inst_33 : CommRing Bₘ
inst_34 : Algebra Aₘ Bₘ
inst_35 : Algebra A Aₘ
inst_36 : Algebra B Bₘ
inst_37 : Algebra A Bₘ
inst_38 : IsScalarTower A Aₘ Bₘ
inst_39 : IsScalarTower A B Bₘ
M : Submonoid A
inst_40 : IsLocalization M Aₘ
inst_41 : IsLocalization (algebraMapSubmonoid B M) Bₘ
inst_42 : IsIntegrallyClosed A
⊢ IsIntegralClosure.mk'.{u_1, u_1, u_2} (R := A) A (B := K)
      ((norm K : (a : L) → K) ((algebraMap B L : (a : B) → L) 1 : L) : K) ⋯ =
    1

Tactic:
simp
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
L₂ : Type u_4
L₃ : Type u_5
B : Type u_6
B₂ : Type u_7
B₃ : Type u_8
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing B₂
inst_3 : CommRing B₃
inst_4 : Algebra A B
inst_5 : Algebra A B₂
inst_6 : Algebra A B₃
inst_7 : Field K
inst_8 : Field L
inst_9 : Field L₂
inst_10 : Field L₃
inst_11 : Algebra A K
inst_12 : IsFractionRing A K
inst_13 : Algebra K L
inst_14 : Algebra A L
inst_15 : IsScalarTower A K L
inst_16 : Algebra K L₂
inst_17 : Algebra A L₂
inst_18 : IsScalarTower A K L₂
inst_19 : Algebra K L₃
inst_20 : Algebra A L₃
inst_21 : IsScalarTower A K L₃
inst_22 : Algebra B L
inst_23 : IsScalarTower A B L
inst_24 : IsIntegralClosure B A L
inst_25 : Algebra B₂ L₂
inst_26 : IsScalarTower A B₂ L₂
inst_27 : IsIntegralClosure B₂ A L₂
inst_28 : Algebra B₃ L₃
inst_29 : IsScalarTower A B₃ L₃
inst_30 : IsIntegralClosure B₃ A L₃
inst_31 : FiniteDimensional K L
Aₘ : Type ?u.308446
Bₘ : Type ?u.308449
inst_32 : CommRing Aₘ
inst_33 : CommRing Bₘ
inst_34 : Algebra Aₘ Bₘ
inst_35 : Algebra A Aₘ
inst_36 : Algebra B Bₘ
inst_37 : Algebra A Bₘ
inst_38 : IsScalarTower A Aₘ Bₘ
inst_39 : IsScalarTower A B Bₘ
M : Submonoid A
inst_40 : IsLocalization M Aₘ
inst_41 : IsLocalization (algebraMapSubmonoid B M) Bₘ
inst_42 : IsIntegrallyClosed A
x y : B
⊢ IsIntegralClosure.mk'.{u_1, u_1, u_2} (R := A) A (B := K)
      ((norm K : (a : L) → K) ((algebraMap B L : (a : B) → L) (x * y) : L) : K) ⋯ =
    IsIntegralClosure.mk'.{u_1, u_1, u_2} (R := A) A (B := K)
        ((norm K : (a : L) → K) ((algebraMap B L : (a : B) → L) x : L) : K) ⋯ *
      IsIntegralClosure.mk'.{u_1, u_1, u_2} (R := A) A (B := K)
        ((norm K : (a : L) → K) ((algebraMap B L : (a : B) → L) y : L) : K) ⋯

Tactic:
simpa using IsIntegralClosure.mk'_mul _ _ _ _ _

Premises used: IsIntegralClosure.mk'_mul
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : Algebra B L
inst_11 : IsScalarTower A B L
inst_12 : IsIntegralClosure B A L
inst_13 : IsIntegrallyClosed A
x : B
dsimp :
  Eq.{u_2 + 1} (α := K)
    ((algebraMap A K : (a : A) → K)
        (IsIntegralClosure.mk'.{u_1, u_1, u_2} (R := A) A (B := K)
          ((norm K : (a : L) → K) ((algebraMap B L : (a : B) → L) x : L) : K) ⋯) :
      K)
    ((norm K : (a : L) → K) ((algebraMap B L : (a : B) → L) x : L) : K)
⊢ Eq.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) ((intNormAux A K L B : (a : B) → A) x : A) : K)
    ((norm K : (a : L) → K) ((algebraMap B L : (a : B) → L) x : L) : K)

Tactic:
dsimp [Algebra.intNormAux]

Premises used: Algebra.intNormAux
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : Algebra B L
inst_11 : IsScalarTower A B L
inst_12 : IsIntegralClosure B A L
inst_13 : IsIntegrallyClosed A
x : B
⊢ Eq.{u_2 + 1} (α := K)
    ((algebraMap A K : (a : A) → K)
        (IsIntegralClosure.mk'.{u_1, u_1, u_2} (R := A) A (B := K)
          ((norm K : (a : L) → K) ((algebraMap B L : (a : B) → L) x : L) : K) ⋯) :
      K)
    ((norm K : (a : L) → K) ((algebraMap B L : (a : B) → L) x : L) : K)

Tactic:
IsIntegralClosure.algebraMap_mk' _ _ _

Premises used: IsIntegralClosure.algebraMap_mk'
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : Algebra B L
inst_11 : IsScalarTower A B L
inst_12 : IsIntegralClosure B A L
inst_13 : IsIntegrallyClosed A
x : B
⊢ Eq.{u_2 + 1} (α := K)
    ((algebraMap A K : (a : A) → K)
        (IsIntegralClosure.mk'.{u_1, u_1, u_2} (R := A) A (B := K)
          ((norm K : (a : L) → K) ((algebraMap B L : (a : B) → L) x : L) : K) ⋯) :
      K)
    ((norm K : (a : L) → K) ((algebraMap B L : (a : B) → L) x : L) : K)

Tactic:
exact IsIntegralClosure.algebraMap_mk' _ _ _

Premises used: IsIntegralClosure.algebraMap_mk'
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : Algebra B L
inst_11 : IsScalarTower A B L
inst_12 : IsIntegralClosure B A L
inst_13 : FiniteDimensional K L
inst_14 : IsIntegrallyClosed A
inst_15 : IsDomain A
inst_16 : IsDomain B
inst_17 : IsIntegrallyClosed B
inst_18 : Algebra.IsIntegral A B
inst_19 : IsTorsionFree A B
x : B
⊢ IsFractionRing B L

Tactic:
haveI := IsIntegralClosure.isFractionRing_of_finite_extension A K L B
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : Algebra B L
inst_11 : IsScalarTower A B L
inst_12 : IsIntegralClosure B A L
inst_13 : FiniteDimensional K L
inst_14 : IsIntegrallyClosed A
inst_15 : IsDomain A
inst_16 : IsDomain B
inst_17 : IsIntegrallyClosed B
inst_18 : Algebra.IsIntegral A B
inst_19 : IsTorsionFree A B
x : B
this : IsFractionRing B L
a :
  Eq.{u_1 + 1} (α := FractionRing A)
    (((AlgEquiv.symm (FractionRing.algEquiv A K) : K ≃ₐ[A] FractionRing A) : (a : K) → FractionRing A)
        ((algebraMap A K : (a : A) → K) ((intNorm A B : (a : B) → A) x : A)) :
      FractionRing A)
    (((AlgEquiv.symm (FractionRing.algEquiv A K) : K ≃ₐ[A] FractionRing A) : (a : K) → FractionRing A)
        ((norm K : (a : L) → K) ((algebraMap B L : (a : B) → L) x : L)) :
      FractionRing A)
⊢ Eq.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) ((intNorm A B : (a : B) → A) x : A) : K)
    ((norm K : (a : L) → K) ((algebraMap B L : (a : B) → L) x : L) : K)

Tactic:
apply (FractionRing.algEquiv A K).symm.injective

Premises used: AlgEquiv.symm, FractionRing.algEquiv, AlgEquiv.injective
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : Algebra B L
inst_11 : IsScalarTower A B L
inst_12 : IsIntegralClosure B A L
inst_13 : FiniteDimensional K L
inst_14 : IsIntegrallyClosed A
inst_15 : IsDomain A
inst_16 : IsDomain B
inst_17 : IsIntegrallyClosed B
inst_18 : Algebra.IsIntegral A B
inst_19 : IsTorsionFree A B
x : B
this : IsFractionRing B L
a :
  Eq.{u_1 + 1} (α := FractionRing A)
    ((norm (FractionRing A) : (a : FractionRing B) → FractionRing A)
        ((algebraMap B (FractionRing B) : (a : B) → FractionRing B) x) :
      FractionRing A)
    (((AlgEquiv.symm (FractionRing.algEquiv A K) : K ≃ₐ[A] FractionRing A) : (a : K) → FractionRing A)
        ((norm K : (a : L) → K)
          ((FractionRing.algEquiv B L : (a : FractionRing B) → L)
              ((algebraMap B (FractionRing B) : (a : B) → FractionRing B) x : FractionRing B) :
            L)) :
      FractionRing A)
⊢ Eq.{u_1 + 1} (α := FractionRing A)
    (((AlgEquiv.symm (FractionRing.algEquiv A K) : K ≃ₐ[A] FractionRing A) : (a : K) → FractionRing A)
        ((algebraMap A K : (a : A) → K) ((intNorm A B : (a : B) → A) x : A)) :
      FractionRing A)
    (((AlgEquiv.symm (FractionRing.algEquiv A K) : K ≃ₐ[A] FractionRing A) : (a : K) → FractionRing A)
        ((norm K : (a : L) → K) ((algebraMap B L : (a : B) → L) x : L)) :
      FractionRing A)

Tactic:
rw [AlgEquiv.commutes, Algebra.intNorm, Algebra.map_intNormAux,
    ← AlgEquiv.commutes (FractionRing.algEquiv B L)]

Premises used: Algebra.map_intNormAux, AlgEquiv.commutes, FractionRing.algEquiv, Algebra.intNorm
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : Algebra B L
inst_11 : IsScalarTower A B L
inst_12 : IsIntegralClosure B A L
inst_13 : FiniteDimensional K L
inst_14 : IsIntegrallyClosed A
inst_15 : IsDomain A
inst_16 : IsDomain B
inst_17 : IsIntegrallyClosed B
inst_18 : Algebra.IsIntegral A B
inst_19 : IsTorsionFree A B
x : B
this : IsFractionRing B L
a :
  Eq (α := RingHom.{u_1, u_3} (FractionRing A) L)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L)
      (↑(AlgEquiv.toRingEquiv (FractionRing.algEquiv A K)) : FractionRing A →+* K))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (↑(AlgEquiv.toRingEquiv (FractionRing.algEquiv B L)) : FractionRing B →+* L)
      (algebraMap (FractionRing A) (FractionRing B)))
⊢ Eq.{u_1 + 1} (α := FractionRing A)
    ((norm (FractionRing A) : (a : FractionRing B) → FractionRing A)
        ((algebraMap B (FractionRing B) : (a : B) → FractionRing B) x) :
      FractionRing A)
    (((AlgEquiv.symm (FractionRing.algEquiv A K) : K ≃ₐ[A] FractionRing A) : (a : K) → FractionRing A)
        ((norm K : (a : L) → K)
          ((FractionRing.algEquiv B L : (a : FractionRing B) → L)
              ((algebraMap B (FractionRing B) : (a : B) → FractionRing B) x : FractionRing B) :
            L)) :
      FractionRing A)

Tactic:
apply Algebra.norm_eq_of_equiv_equiv (FractionRing.algEquiv A K).toRingEquiv
    (FractionRing.algEquiv B L).toRingEquiv

Premises used: Algebra.norm_eq_of_equiv_equiv, FractionRing.algEquiv, AlgEquiv.toRingEquiv
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : Algebra B L
inst_11 : IsScalarTower A B L
inst_12 : IsIntegralClosure B A L
inst_13 : FiniteDimensional K L
inst_14 : IsIntegrallyClosed A
inst_15 : IsDomain A
inst_16 : IsDomain B
inst_17 : IsIntegrallyClosed B
inst_18 : Algebra.IsIntegral A B
inst_19 : IsTorsionFree A B
x : B
this : IsFractionRing B L
a :
  ∀ (x : FractionRing A),
    Eq.{u_3 + 1} (α := L)
      ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L)
              (↑(AlgEquiv.toRingEquiv (FractionRing.algEquiv A K)) : FractionRing A →+* K) :
            (a : FractionRing A) → L)
          x :
        L)
      ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
              (↑(AlgEquiv.toRingEquiv (FractionRing.algEquiv B L)) : FractionRing B →+* L)
              (algebraMap (FractionRing A) (FractionRing B)) :
            (a : FractionRing A) → L)
          x :
        L)
⊢ Eq (α := RingHom.{u_1, u_3} (FractionRing A) L)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L)
      (↑(AlgEquiv.toRingEquiv (FractionRing.algEquiv A K)) : FractionRing A →+* K))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
      (↑(AlgEquiv.toRingEquiv (FractionRing.algEquiv B L)) : FractionRing B →+* L)
      (algebraMap (FractionRing A) (FractionRing B)))

Tactic:
ext
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : Algebra B L
inst_11 : IsScalarTower A B L
inst_12 : IsIntegralClosure B A L
inst_13 : FiniteDimensional K L
inst_14 : IsIntegrallyClosed A
inst_15 : IsDomain A
inst_16 : IsDomain B
inst_17 : IsIntegrallyClosed B
inst_18 : Algebra.IsIntegral A B
inst_19 : IsTorsionFree A B
x : B
this : IsFractionRing B L
x_1 : FractionRing A
⊢ Eq.{u_3 + 1} (α := L)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L)
            (↑(AlgEquiv.toRingEquiv (FractionRing.algEquiv A K)) : FractionRing A →+* K) :
          (a : FractionRing A) → L)
        x_1 :
      L)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (↑(AlgEquiv.toRingEquiv (FractionRing.algEquiv B L)) : FractionRing B →+* L)
            (algebraMap (FractionRing A) (FractionRing B)) :
          (a : FractionRing A) → L)
        x_1 :
      L)

Tactic:
IsFractionRing.algEquiv_commutes (FractionRing.algEquiv A K) (FractionRing.algEquiv B L) _

Premises used: FractionRing.algEquiv, IsFractionRing.algEquiv_commutes
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_6
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : Algebra B L
inst_11 : IsScalarTower A B L
inst_12 : IsIntegralClosure B A L
inst_13 : FiniteDimensional K L
inst_14 : IsIntegrallyClosed A
inst_15 : IsDomain A
inst_16 : IsDomain B
inst_17 : IsIntegrallyClosed B
inst_18 : Algebra.IsIntegral A B
inst_19 : IsTorsionFree A B
x : B
this : IsFractionRing B L
x_1 : FractionRing A
⊢ Eq.{u_3 + 1} (α := L)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L)
            (↑(AlgEquiv.toRingEquiv (FractionRing.algEquiv A K)) : FractionRing A →+* K) :
          (a : FractionRing A) → L)
        x_1 :
      L)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (↑(AlgEquiv.toRingEquiv (FractionRing.algEquiv B L)) : FractionRing B →+* L)
            (algebraMap (FractionRing A) (FractionRing B)) :
          (a : FractionRing A) → L)
        x_1 :
      L)

Tactic:
exact IsFractionRing.algEquiv_commutes (FractionRing.algEquiv A K) (FractionRing.algEquiv B L) _

Premises used: FractionRing.algEquiv, IsFractionRing.algEquiv_commutes
-- 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 : IsIntegrallyClosed A
inst_4 : IsDomain A
inst_5 : IsDomain B
inst_6 : IsIntegrallyClosed B
inst_7 : Algebra.IsIntegral A B
inst_8 : IsTorsionFree A B
x : B
⊢ Eq (α := FractionRing A)
    ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) ((intNorm A B : (a : B) → A) x) : FractionRing A)
    ((norm (FractionRing A) : (a : FractionRing B) → FractionRing A)
        ((algebraMap B (FractionRing B) : (a : B) → FractionRing B) x) :
      FractionRing A)

Tactic:
Algebra.map_intNormAux x

Premises used: Set.Mem, setOf, Algebra.map_intNormAux
-- 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 : IsIntegrallyClosed A
inst_4 : IsDomain A
inst_5 : IsDomain B
inst_6 : IsIntegrallyClosed B
inst_7 : Algebra.IsIntegral A B
inst_8 : IsTorsionFree A B
C : Type u_9
inst_9 : CommRing C
inst_10 : IsDomain C
inst_11 : IsIntegrallyClosed C
inst_12 : Algebra A C
inst_13 : Algebra B C
inst_14 : IsScalarTower A B C
inst_15 : Algebra.IsIntegral A C
inst_16 : Algebra.IsIntegral B C
inst_17 : IsTorsionFree A C
inst_18 : IsTorsionFree B C
x : C
a :
  Eq (α := FractionRing A)
    ((algebraMap A (FractionRing A) : (a : A) → FractionRing A)
        ((intNorm A B : (a : B) → A) ((intNorm B C : (a : C) → B) x : B)) :
      FractionRing A)
    ((algebraMap A (FractionRing A) : (a : A) → FractionRing A) ((intNorm A C : (a : C) → A) x) : FractionRing A)
⊢ Eq.{u_1 + 1} (α := A) ((intNorm A B : (a : B) → A) ((intNorm B C : (a : C) → B) x : B) : A)
    ((intNorm A C : (a : C) → A) x : A)

Tactic:
apply FaithfulSMul.algebraMap_injective A (FractionRing A)

Premises used: FractionRing, FaithfulSMul.algebraMap_injective