awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : Algebra.IsAlgebraic K L
σ : B →ₐ[A] B₂
this_1 : IsDomain A
this_2 : IsTorsionFree A L₂
this : IsLocalization (Algebra.algebraMapSubmonoid.{u_1, u_6} (R := A) B A⁰) L
H :
  ∀ (y : ↥(Algebra.algebraMapSubmonoid.{u_1, u_6} (R := A) B A⁰)),
    IsUnit.{u_4} (M := L₂)
      ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B₂ L₂) (↑σ : B →+* B₂) : (a : B) → L₂)
          (↑y : B) :
        L₂)
x : A
⊢ Eq.{u_4 + 1} (α := L₂)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (IsLocalization.lift H) (algebraMap K L))
            (algebraMap A K) :
          (a : A) → L₂)
        x :
      L₂)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L₂) (algebraMap A K) : (a : A) → L₂) x : L₂)

Tactic:
simp only [RingHom.coe_comp, Function.comp_apply, ← IsScalarTower.algebraMap_apply A K L,
      ← IsScalarTower.algebraMap_apply A K L₂,
      IsScalarTower.algebraMap_apply A B L, IsScalarTower.algebraMap_apply A B₂ L₂,
      IsLocalization.lift_eq, RingHom.coe_coe, AlgHom.commutes]

Premises used: IsLocalization.lift_eq, RingHom.coe_coe, AlgHom.commutes, RingHom.coe_comp, Function.comp_apply, IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
L₂ : Type u_4
B : Type u_6
B₂ : Type u_7
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing B₂
inst_3 : Algebra A B
inst_4 : Algebra A B₂
inst_5 : Field K
inst_6 : Field L
inst_7 : Field L₂
inst_8 : Algebra A K
inst_9 : IsFractionRing A K
inst_10 : Algebra K L
inst_11 : Algebra A L
inst_12 : IsScalarTower A K L
inst_13 : Algebra K L₂
inst_14 : Algebra A L₂
inst_15 : IsScalarTower A K L₂
inst_16 : Algebra B L
inst_17 : IsScalarTower A B L
inst_18 : IsIntegralClosure B A L
inst_19 : Algebra B₂ L₂
inst_20 : IsScalarTower A B₂ L₂
inst_21 : Algebra.IsAlgebraic K L
σ : B →ₐ[A] B₂
x : B
⊢ Eq.{u_4 + 1} (α := L₂) ((galLift K L L₂ σ : (a : L) → L₂) ((algebraMap B L : (a : B) → L) x : L) : L₂)
    ((algebraMap B₂ L₂ : (a : B₂) → L₂) ((σ : (a : B) → B₂) x : B₂) : L₂)

Tactic:
simp [galLift]

Premises used: galLift
-- 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 : Algebra.IsAlgebraic K L
H : ∀ (x : L), Eq (α := L) ((galLift K L L (AlgHom.id A B) : (a : L) → L) x : L) ((AlgHom.id K L : (a : L) → L) x : L)
⊢ Eq (α := L →ₐ[K] L) (galLift K L L (AlgHom.id A B)) (AlgHom.id K L)

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 : Algebra.IsAlgebraic K L
x : L
⊢ Eq (α := L) ((galLift K L L (AlgHom.id A B) : (a : L) → L) x : L) ((AlgHom.id K L : (a : L) → L) x : L)

Tactic:
simp [galLift]

Premises used: galLift
-- 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 : Algebra.IsAlgebraic K L
inst_31 : Algebra.IsAlgebraic K L₂
σ : B →ₐ[A] B₂
σ' : B₂ →ₐ[A] B₃
this_1 : IsDomain A
this : IsLocalization (Algebra.algebraMapSubmonoid.{u_1, u_6} (R := A) B A⁰) L
x : B
⊢ Eq.{u_5 + 1} (α := L₃)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(galLift K L L₃ (σ'.comp σ)) : L →+* L₃) (algebraMap B L) :
          (a : B) → L₃)
        x :
      L₃)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _
            (↑(AlgHom.comp (galLift K L₂ L₃ σ') (galLift K L L₂ σ)) : L →+* L₃) (algebraMap B L) :
          (a : B) → L₃)
        x :
      L₃)

Tactic:
simp
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
L₂ : Type u_4
B : Type u_6
B₂ : Type u_7
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing B₂
inst_3 : Algebra A B
inst_4 : Algebra A B₂
inst_5 : Field K
inst_6 : Field L
inst_7 : Field L₂
inst_8 : Algebra A K
inst_9 : IsFractionRing A K
inst_10 : Algebra K L
inst_11 : Algebra A L
inst_12 : IsScalarTower A K L
inst_13 : Algebra K L₂
inst_14 : Algebra A L₂
inst_15 : IsScalarTower A K L₂
inst_16 : Algebra B L
inst_17 : IsScalarTower A B L
inst_18 : IsIntegralClosure B A L
inst_19 : Algebra B₂ L₂
inst_20 : IsScalarTower A B₂ L₂
inst_21 : IsIntegralClosure B₂ A L₂
inst_22 : Algebra.IsAlgebraic K L
σ : L →ₐ[K] L₂
this_1 : IsDomain A
this : IsLocalization (Algebra.algebraMapSubmonoid.{u_1, u_6} (R := A) B A⁰) L
x : B
⊢ Eq.{u_4 + 1} (α := L₂)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑(galLift K L L₂ (galRestrict' A B B₂ σ)) : L →+* L₂)
            (algebraMap B L) :
          (a : B) → L₂)
        x :
      L₂)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑σ : L →+* L₂) (algebraMap B L) : (a : B) → L₂) x : L₂)

Tactic:
simp [galRestrict', Subalgebra.algebraMap_eq, galLift]

Premises used: galRestrict', Subalgebra.algebraMap_eq, galLift
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
L₂ : Type u_4
B : Type u_6
B₂ : Type u_7
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing B₂
inst_3 : Algebra A B
inst_4 : Algebra A B₂
inst_5 : Field K
inst_6 : Field L
inst_7 : Field L₂
inst_8 : Algebra A K
inst_9 : IsFractionRing A K
inst_10 : Algebra K L
inst_11 : Algebra A L
inst_12 : IsScalarTower A K L
inst_13 : Algebra K L₂
inst_14 : Algebra A L₂
inst_15 : IsScalarTower A K L₂
inst_16 : Algebra B L
inst_17 : IsScalarTower A B L
inst_18 : IsIntegralClosure B A L
inst_19 : Algebra B₂ L₂
inst_20 : IsScalarTower A B₂ L₂
inst_21 : IsIntegralClosure B₂ A L₂
inst_22 : Algebra.IsAlgebraic K L
σ : B →ₐ[A] B₂
this_1 : IsDomain A
this : IsLocalization (Algebra.algebraMapSubmonoid.{u_1, u_6} (R := A) B A⁰) L
x : B
⊢ Eq.{u_4 + 1} (α := L₂)
    ((algebraMap B₂ L₂ : (a : B₂) → L₂) ((galRestrict' A B B₂ (galLift K L L₂ σ) : (a : B) → B₂) x : B₂) : L₂)
    ((algebraMap B₂ L₂ : (a : B₂) → L₂) ((σ : (a : B) → B₂) x : B₂) : L₂)

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 : Algebra.IsAlgebraic K L
inst_32 : Algebra.IsAlgebraic K L₂
σ : B ≃ₐ[A] B₂
⊢ Eq (α := L₂ →ₐ[K] L₂) (AlgHom.comp (galLift K L L₂ (↑σ : B →ₐ[A] B₂)) (galLift K L₂ L (↑σ.symm : B₂ →ₐ[A] B)))
    (AlgHom.id K L₂)

Tactic:
simp [← galLift_comp]

Premises used: galLift_comp
-- 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 : Algebra.IsAlgebraic K L
inst_32 : Algebra.IsAlgebraic K L₂
σ : B ≃ₐ[A] B₂
⊢ Eq (α := L →ₐ[K] L) (AlgHom.comp (galLift K L₂ L (↑σ.symm : B₂ →ₐ[A] B)) (galLift K L L₂ (↑σ : B →ₐ[A] B₂)))
    (AlgHom.id K L)

Tactic:
simp [← galLift_comp]

Premises used: galLift_comp
-- Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
L₂ : Type u_4
B : Type u_6
B₂ : Type u_7
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing B₂
inst_3 : Algebra A B
inst_4 : Algebra A B₂
inst_5 : Field K
inst_6 : Field L
inst_7 : Field L₂
inst_8 : Algebra A K
inst_9 : IsFractionRing A K
inst_10 : Algebra K L
inst_11 : Algebra A L
inst_12 : IsScalarTower A K L
inst_13 : Algebra K L₂
inst_14 : Algebra A L₂
inst_15 : IsScalarTower A K L₂
inst_16 : Algebra B L
inst_17 : IsScalarTower A B L
inst_18 : IsIntegralClosure B A L
inst_19 : Algebra B₂ L₂
inst_20 : IsScalarTower A B₂ L₂
inst_21 : IsIntegralClosure B₂ A L₂
inst_22 : Algebra.IsAlgebraic K L
inst_23 : Algebra.IsAlgebraic K L₂
σ : B ≃ₐ[A] B₂
x : B
⊢ Eq.{u_4 + 1} (α := L₂) ((galLiftEquiv K L L₂ σ : (a : L) → L₂) ((algebraMap B L : (a : B) → L) x : L) : L₂)
    ((algebraMap B₂ L₂ : (a : B₂) → L₂) ((σ : (a : B) → B₂) x : B₂) : L₂)

Tactic:
simp [galLiftEquiv]

Premises used: galLiftEquiv
-- 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 : Algebra.IsAlgebraic K L
σ : L →ₐ[K] L
x : B
⊢ Eq.{u_3 + 1} (α := L)
    ((algebraMap B L : (a : B) → L)
        (((((galRestrictHom A K L B : MulEquiv.{u_3, u_6} (L →ₐ[K] L) (B →ₐ[A] B)) : (a : L →ₐ[K] L) → B →ₐ[A] B) σ :
                B →ₐ[A] B) :
              (a : B) → B)
            x :
          B) :
      L)
    ((σ : (a : L) → L) ((algebraMap B L : (a : B) → L) x : L) : L)

Tactic:
algebraMap_galRestrict'_apply _ _ _ _ _

Premises used: algebraMap_galRestrict'_apply
-- 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 : Algebra.IsAlgebraic K L
σ : B →ₐ[A] B
x : B
⊢ Eq (α := L)
    (((((MulEquiv.symm (galRestrictHom A K L B) : MulEquiv.{u_6, u_3} (B →ₐ[A] B) (L →ₐ[K] L)) :
                (a : B →ₐ[A] B) → L →ₐ[K] L)
              σ :
            L →ₐ[K] L) :
          (a : L) → L)
        ((algebraMap B L : (a : B) → L) x : L) :
      L)
    ((algebraMap B L : (a : B) → L) ((σ : (a : B) → B) x : B) : L)

Tactic:
galLift_algebraMap_apply _ _ _ _ _

Premises used: galLift_algebraMap_apply
-- 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 : Algebra.IsAlgebraic K L
σ : Gal(L/K)
⊢ Eq.{u_6 + 1} (α := B →ₐ[A] B)
    (↑(((galRestrict A K L B : MulEquiv.{u_3, u_6} Gal(L/K) (B ≃ₐ[A] B)) : (a : Gal(L/K)) → B ≃ₐ[A] B) σ) : B →ₐ[A] B)
    (((galRestrictHom A K L B : MulEquiv.{u_3, u_6} (L →ₐ[K] L) (B →ₐ[A] B)) : (a : L →ₐ[K] L) → B →ₐ[A] B)
      (↑σ : L →ₐ[K] L))

Tactic:
rfl

Premises used: AlgEquiv.toAlgHom, galRestrict', IsIntegralClosure.mk', Classical.choose, AlgHom.comp, rfl
-- 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 : Algebra.IsAlgebraic K L
σ : Gal(L/K)
x : B
⊢ Eq (α := B)
    (((((galRestrict A K L B : MulEquiv.{u_3, u_6} Gal(L/K) (B ≃ₐ[A] B)) : (a : Gal(L/K)) → B ≃ₐ[A] B) σ : B ≃ₐ[A] B) :
          (a : B) → B)
        x :
      B)
    (((((galRestrictHom A K L B : MulEquiv.{u_3, u_6} (L →ₐ[K] L) (B →ₐ[A] B)) : (a : L →ₐ[K] L) → B →ₐ[A] B)
              (↑σ : L →ₐ[K] L) :
            B →ₐ[A] B) :
          (a : B) → B)
        x :
      B)

Tactic:
rfl

Premises used: IsIntegralClosure.mk', Classical.choose, rfl
-- 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 : Algebra.IsAlgebraic K L
σ : Gal(L/K)
x : B
⊢ Eq.{u_3 + 1} (α := L)
    ((algebraMap B L : (a : B) → L)
        (((((galRestrict A K L B : MulEquiv.{u_3, u_6} Gal(L/K) (B ≃ₐ[A] B)) : (a : Gal(L/K)) → B ≃ₐ[A] B) σ :
                B ≃ₐ[A] B) :
              (a : B) → B)
            x :
          B) :
      L)
    ((σ : (a : L) → L) ((algebraMap B L : (a : B) → L) x : L) : L)

Tactic:
algebraMap_galRestrictHom_apply A K L B σ.toAlgHom x

Premises used: AlgEquiv.toAlgHom, IsIntegralClosure.mk', Classical.choose, algebraMap_galRestrictHom_apply
-- 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 : Algebra.IsAlgebraic K L
σ : B ≃ₐ[A] B
x : B
⊢ Eq (α := L)
    (((((MulEquiv.symm (galRestrict A K L B) : MulEquiv.{u_6, u_3} (B ≃ₐ[A] B) Gal(L/K)) : (a : B ≃ₐ[A] B) → Gal(L/K))
              σ :
            Gal(L/K)) :
          (a : L) → L)
        ((algebraMap B L : (a : B) → L) x : L) :
      L)
    ((algebraMap B L : (a : B) → L) ((σ : (a : B) → B) x : B) : L)

Tactic:
galRestrictHom_symm_algebraMap_apply A K L B σ x

Premises used: AlgEquiv.toAlgHom, galRestrictHom_symm_algebraMap_apply
-- 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 : IsGalois K L
inst_15 : IsIntegrallyClosed A
x : B
a :
  Eq.{u_3 + 1} (α := L)
    ((algebraMap B L : (a : B) → L)
        (∏ σ : Gal(L/K),
          ((((galRestrict A K L B : MulEquiv.{u_3, u_6} Gal(L/K) (B ≃ₐ[A] B)) : (a : Gal(L/K)) → B ≃ₐ[A] B) σ :
                B ≃ₐ[A] B) :
              (a : B) → B)
            x) :
      L)
    ((algebraMap B L : (a : B) → L)
        ((algebraMap A B : (a : A) → B)
            (IsIntegralClosure.mk'.{u_1, u_1, u_2} (R := A) A (B := K)
              ((Algebra.norm K : (a : L) → K) ((algebraMap B L : (a : B) → L) x : L) : K) ⋯) :
          B) :
      L)
⊢ Eq.{u_6 + 1} (α := B)
    (∏ σ : Gal(L/K),
        ((((galRestrict A K L B : MulEquiv.{u_3, u_6} Gal(L/K) (B ≃ₐ[A] B)) : (a : Gal(L/K)) → B ≃ₐ[A] B) σ :
              B ≃ₐ[A] B) :
            (a : B) → B)
          x :
      B)
    ((algebraMap A B : (a : A) → B)
        (IsIntegralClosure.mk'.{u_1, u_1, u_2} (R := A) A (B := K)
          ((Algebra.norm K : (a : L) → K) ((algebraMap B L : (a : B) → L) x : L) : K) ⋯) :
      B)

Tactic:
apply IsIntegralClosure.algebraMap_injective B A L

Premises used: IsIntegralClosure.algebraMap_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 : IsGalois K L
inst_15 : IsIntegrallyClosed A
x : B
a :
  Eq.{u_3 + 1} (α := L)
    ((algebraMap B L : (a : B) → L)
        (∏ σ : Gal(L/K),
          ((((galRestrict A K L B : MulEquiv.{u_3, u_6} Gal(L/K) (B ≃ₐ[A] B)) : (a : Gal(L/K)) → B ≃ₐ[A] B) σ :
                B ≃ₐ[A] B) :
              (a : B) → B)
            x) :
      L)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L) (algebraMap A K) : (a : A) → L)
        (IsIntegralClosure.mk'.{u_1, u_1, u_2} (R := A) A (B := K)
          ((Algebra.norm K : (a : L) → K) ((algebraMap B L : (a : B) → L) x : L) : K) ⋯) :
      L)
⊢ Eq.{u_3 + 1} (α := L)
    ((algebraMap B L : (a : B) → L)
        (∏ σ : Gal(L/K),
          ((((galRestrict A K L B : MulEquiv.{u_3, u_6} Gal(L/K) (B ≃ₐ[A] B)) : (a : Gal(L/K)) → B ≃ₐ[A] B) σ :
                B ≃ₐ[A] B) :
              (a : B) → B)
            x) :
      L)
    ((algebraMap B L : (a : B) → L)
        ((algebraMap A B : (a : A) → B)
            (IsIntegralClosure.mk'.{u_1, u_1, u_2} (R := A) A (B := K)
              ((Algebra.norm K : (a : L) → K) ((algebraMap B L : (a : B) → L) x : L) : K) ⋯) :
          B) :
      L)

Tactic:
rw [← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_eq A K L]

Premises used: IsScalarTower.algebraMap_eq, IsScalarTower.algebraMap_apply
-- 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 : IsGalois K L
inst_15 : IsIntegrallyClosed A
x : B
⊢ Eq.{u_3 + 1} (α := L)
    ((algebraMap B L : (a : B) → L)
        (∏ σ : Gal(L/K),
          ((((galRestrict A K L B : MulEquiv.{u_3, u_6} Gal(L/K) (B ≃ₐ[A] B)) : (a : Gal(L/K)) → B ≃ₐ[A] B) σ :
                B ≃ₐ[A] B) :
              (a : B) → B)
            x) :
      L)
    ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L) (algebraMap A K) : (a : A) → L)
        (IsIntegralClosure.mk'.{u_1, u_1, u_2} (R := A) A (B := K)
          ((Algebra.norm K : (a : L) → K) ((algebraMap B L : (a : B) → L) x : L) : K) ⋯) :
      L)

Tactic:
simp only [map_prod, algebraMap_galRestrict_apply, IsIntegralClosure.algebraMap_mk',
    Algebra.norm_eq_prod_automorphisms, RingHom.coe_comp, Function.comp_apply]

Premises used: algebraMap_galRestrict_apply, map_prod, Algebra.norm_eq_prod_automorphisms, IsIntegralClosure.algebraMap_mk', RingHom.coe_comp, Function.comp_apply
-- 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
x : B
⊢ Eq.{u_2 + 1} (α := K) ((algebraMap A K : (a : A) → K) ((intTraceAux A K L B : (a : B) → A) x : A) : K)
    ((trace K L : (a : L) → K) ((algebraMap B L : (a : B) → L) x : L) : K)

Tactic:
IsIntegralClosure.algebraMap_equiv A (integralClosure A K) K A _

Premises used: Membership.mem, Subtype, IsIntegralClosure.algebraMap_equiv, integralClosure
-- 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 : IsDomain A
inst_15 : IsIntegrallyClosed A
inst_16 : IsDomain B
inst_17 : IsIntegrallyClosed B
inst_18 : Module.Finite A B
inst_19 : IsTorsionFree A B
x : B
⊢ IsIntegralClosure B A (FractionRing B)

Tactic:
haveI : IsIntegralClosure B A (FractionRing B) :=
    IsIntegralClosure.of_isIntegrallyClosed _ _ _