awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Norm.Transitivity
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Free R S
inst_4 : AddCommGroup A
inst_5 : Module R A
inst_6 : Module S A
inst_7 : IsScalarTower R S A
inst_8 : Module.Free S A
f : A →ₗ[S] A
h : Nontrivial R
h_1 : Nontrivial A
this : Nontrivial S
ιS : Type u_2
bS : Module.Basis ιS R S
let :
  ∀ (ιA : Type u_3) (bA : Module.Basis ιA S A),
    Eq.{u_1 + 1} (α := R)
      ((LinearMap.det : (a : A →ₗ[R] A) → R)
          ((↑R :
              {S : Type u_2} →
                {M M₂ : Type u_3} →
                  [inst : Semiring R] →
                    [inst_9 : Semiring S] →
                      [inst_10 : AddCommMonoid M] →
                        [inst_11 : AddCommMonoid M₂] →
                          [inst_12 : Module R M] →
                            [inst_13 : Module R M₂] →
                              [inst_14 : Module S M] →
                                [inst_15 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            f) :
        R)
      ((Algebra.norm R : (a : S) → R) ((LinearMap.det : (a : A →ₗ[S] A) → S) f : S) : R)
⊢ Eq.{u_1 + 1} (α := R)
    ((LinearMap.det : (a : A →ₗ[R] A) → R)
        ((↑R :
            {S : Type u_2} →
              {M M₂ : Type u_3} →
                [inst : Semiring R] →
                  [inst_9 : Semiring S] →
                    [inst_10 : AddCommMonoid M] →
                      [inst_11 : AddCommMonoid M₂] →
                        [inst_12 : Module R M] →
                          [inst_13 : Module R M₂] →
                            [inst_14 : Module S M] →
                              [inst_15 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          f) :
      R)
    ((Algebra.norm R : (a : S) → R) ((LinearMap.det : (a : A →ₗ[S] A) → S) f : S) : R)

Tactic:
let ⟨ιA, bA⟩ := Module.Free.exists_basis (R := S) (M := A)
-- Module: Mathlib.RingTheory.Norm.Transitivity
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Free R S
inst_4 : AddCommGroup A
inst_5 : Module R A
inst_6 : Module S A
inst_7 : IsScalarTower R S A
inst_8 : Module.Free S A
f : A →ₗ[S] A
h : Nontrivial R
h_1 : Nontrivial A
this : Nontrivial S
ιS : Type u_2
bS : Module.Basis ιS R S
ιA : Type u_3
bA : Module.Basis ιA S A
⊢ Nonempty ιS

Tactic:
have := bS.index_nonempty
-- Module: Mathlib.RingTheory.Norm.Transitivity
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Free R S
inst_4 : AddCommGroup A
inst_5 : Module R A
inst_6 : Module S A
inst_7 : IsScalarTower R S A
inst_8 : Module.Free S A
f : A →ₗ[S] A
h : Nontrivial R
h_1 : Nontrivial A
this_1 : Nontrivial S
ιS : Type u_2
bS : Module.Basis ιS R S
ιA : Type u_3
bA : Module.Basis ιA S A
this : Nonempty ιS
⊢ Nonempty ιA

Tactic:
have := bA.index_nonempty
-- Module: Mathlib.RingTheory.Norm.Transitivity
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Free R S
inst_4 : AddCommGroup A
inst_5 : Module R A
inst_6 : Module S A
inst_7 : IsScalarTower R S A
inst_8 : Module.Free S A
f : A →ₗ[S] A
h : Nontrivial R
h_1 : Nontrivial A
this_1 : Nontrivial S
ιS : Type u_2
bS : Module.Basis ιS R S
ιA : Type u_3
bA : Module.Basis ιA S A
this_2 : Nonempty ιS
this : Nonempty ιA
inl :
  ∀ (val : Fintype ιS),
    Eq.{u_1 + 1} (α := R)
      ((LinearMap.det : (a : A →ₗ[R] A) → R)
          ((↑R :
              {S : Type u_2} →
                {M M₂ : Type u_3} →
                  [inst : Semiring R] →
                    [inst_9 : Semiring S] →
                      [inst_10 : AddCommMonoid M] →
                        [inst_11 : AddCommMonoid M₂] →
                          [inst_12 : Module R M] →
                            [inst_13 : Module R M₂] →
                              [inst_14 : Module S M] →
                                [inst_15 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            f) :
        R)
      ((Algebra.norm R : (a : S) → R) ((LinearMap.det : (a : A →ₗ[S] A) → S) f : S) : R)
inr :
  Infinite ιS →
    Eq.{u_1 + 1} (α := R)
      ((LinearMap.det : (a : A →ₗ[R] A) → R)
          ((↑R :
              {S : Type u_2} →
                {M M₂ : Type u_3} →
                  [inst : Semiring R] →
                    [inst_9 : Semiring S] →
                      [inst_10 : AddCommMonoid M] →
                        [inst_11 : AddCommMonoid M₂] →
                          [inst_12 : Module R M] →
                            [inst_13 : Module R M₂] →
                              [inst_14 : Module S M] →
                                [inst_15 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            f) :
        R)
      ((Algebra.norm R : (a : S) → R) ((LinearMap.det : (a : A →ₗ[S] A) → S) f : S) : R)
⊢ Eq.{u_1 + 1} (α := R)
    ((LinearMap.det : (a : A →ₗ[R] A) → R)
        ((↑R :
            {S : Type u_2} →
              {M M₂ : Type u_3} →
                [inst : Semiring R] →
                  [inst_9 : Semiring S] →
                    [inst_10 : AddCommMonoid M] →
                      [inst_11 : AddCommMonoid M₂] →
                        [inst_12 : Module R M] →
                          [inst_13 : Module R M₂] →
                            [inst_14 : Module S M] →
                              [inst_15 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          f) :
      R)
    ((Algebra.norm R : (a : S) → R) ((LinearMap.det : (a : A →ₗ[S] A) → S) f : S) : R)

Tactic:
cases fintypeOrInfinite ιS

Premises used: fintypeOrInfinite
-- Module: Mathlib.RingTheory.Norm.Transitivity
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Free R S
inst_4 : AddCommGroup A
inst_5 : Module R A
inst_6 : Module S A
inst_7 : IsScalarTower R S A
inst_8 : Module.Free S A
f : A →ₗ[S] A
h : Nontrivial R
h_1 : Nontrivial A
this_1 : Nontrivial S
ιS : Type u_2
bS : Module.Basis ιS R S
ιA : Type u_3
bA : Module.Basis ιA S A
this_2 : Nonempty ιS
this : Nonempty ιA
val : Infinite ιS
inr :
  Eq.{u_1 + 1} (α := R)
    ((LinearMap.det : (a : A →ₗ[R] A) → R)
        ((↑R :
            {S : Type u_2} →
              {M M₂ : Type u_3} →
                [inst : Semiring R] →
                  [inst_9 : Semiring S] →
                    [inst_10 : AddCommMonoid M] →
                      [inst_11 : AddCommMonoid M₂] →
                        [inst_12 : Module R M] →
                          [inst_13 : Module R M₂] →
                            [inst_14 : Module S M] →
                              [inst_15 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          f) :
      R)
    (1 : R)
inr₁ inr₂ : Eq.{u_1 + 1} (α := R) 1 1
⊢ Eq.{u_1 + 1} (α := R)
    ((LinearMap.det : (a : A →ₗ[R] A) → R)
        ((↑R :
            {S : Type u_2} →
              {M M₂ : Type u_3} →
                [inst : Semiring R] →
                  [inst_9 : Semiring S] →
                    [inst_10 : AddCommMonoid M] →
                      [inst_11 : AddCommMonoid M₂] →
                        [inst_12 : Module R M] →
                          [inst_13 : Module R M₂] →
                            [inst_14 : Module S M] →
                              [inst_15 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          f) :
      R)
    ((Algebra.norm R : (a : S) → R) ((LinearMap.det : (a : A →ₗ[S] A) → S) f : S) : R)

Tactic:
rw [Algebra.norm_eq_one_of_not_module_finite (Module.not_finite_of_infinite_basis bS),
      det_eq_one_of_not_module_finite (Module.not_finite_of_infinite_basis (bS.smulTower bA))]

Premises used: LinearMap.det_eq_one_of_not_module_finite, Module.not_finite_of_infinite_basis, Algebra.norm_eq_one_of_not_module_finite, Module.Basis.smulTower
-- Module: Mathlib.RingTheory.Norm.Transitivity
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Free R S
inst_4 : AddCommGroup A
inst_5 : Module R A
inst_6 : Module S A
inst_7 : IsScalarTower R S A
inst_8 : Module.Free S A
f : A →ₗ[S] A
h : Nontrivial R
h_1 : Nontrivial A
this_1 : Nontrivial S
ιS : Type u_2
bS : Module.Basis ιS R S
ιA : Type u_3
bA : Module.Basis ιA S A
this_2 : Nonempty ιS
this : Nonempty ιA
val : Fintype ιS
inl :
  ∀ (val : Fintype ιA),
    Eq.{u_1 + 1} (α := R)
      ((LinearMap.det : (a : A →ₗ[R] A) → R)
          ((↑R :
              {S : Type u_2} →
                {M M₂ : Type u_3} →
                  [inst : Semiring R] →
                    [inst_9 : Semiring S] →
                      [inst_10 : AddCommMonoid M] →
                        [inst_11 : AddCommMonoid M₂] →
                          [inst_12 : Module R M] →
                            [inst_13 : Module R M₂] →
                              [inst_14 : Module S M] →
                                [inst_15 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            f) :
        R)
      ((Algebra.norm R : (a : S) → R) ((LinearMap.det : (a : A →ₗ[S] A) → S) f : S) : R)
inl₁ :
  Infinite ιA →
    Eq.{u_1 + 1} (α := R)
      ((LinearMap.det : (a : A →ₗ[R] A) → R)
          ((↑R :
              {S : Type u_2} →
                {M M₂ : Type u_3} →
                  [inst : Semiring R] →
                    [inst_9 : Semiring S] →
                      [inst_10 : AddCommMonoid M] →
                        [inst_11 : AddCommMonoid M₂] →
                          [inst_12 : Module R M] →
                            [inst_13 : Module R M₂] →
                              [inst_14 : Module S M] →
                                [inst_15 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
            f) :
        R)
      ((Algebra.norm R : (a : S) → R) ((LinearMap.det : (a : A →ₗ[S] A) → S) f : S) : R)
⊢ Eq.{u_1 + 1} (α := R)
    ((LinearMap.det : (a : A →ₗ[R] A) → R)
        ((↑R :
            {S : Type u_2} →
              {M M₂ : Type u_3} →
                [inst : Semiring R] →
                  [inst_9 : Semiring S] →
                    [inst_10 : AddCommMonoid M] →
                      [inst_11 : AddCommMonoid M₂] →
                        [inst_12 : Module R M] →
                          [inst_13 : Module R M₂] →
                            [inst_14 : Module S M] →
                              [inst_15 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          f) :
      R)
    ((Algebra.norm R : (a : S) → R) ((LinearMap.det : (a : A →ₗ[S] A) → S) f : S) : R)

Tactic:
cases fintypeOrInfinite ιA

Premises used: fintypeOrInfinite
-- Module: Mathlib.RingTheory.Norm.Transitivity
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Free R S
inst_4 : AddCommGroup A
inst_5 : Module R A
inst_6 : Module S A
inst_7 : IsScalarTower R S A
inst_8 : Module.Free S A
f : A →ₗ[S] A
h : Nontrivial R
h_1 : Nontrivial A
this_1 : Nontrivial S
ιS : Type u_2
bS : Module.Basis ιS R S
ιA : Type u_3
bA : Module.Basis ιA S A
this_2 : Nonempty ιS
this : Nonempty ιA
val : Fintype ιS
val_1 : Infinite ιA
inl :
  Eq.{u_1 + 1} (α := R)
    ((LinearMap.det : (a : A →ₗ[R] A) → R)
        ((↑R :
            {S : Type u_2} →
              {M M₂ : Type u_3} →
                [inst : Semiring R] →
                  [inst_9 : Semiring S] →
                    [inst_10 : AddCommMonoid M] →
                      [inst_11 : AddCommMonoid M₂] →
                        [inst_12 : Module R M] →
                          [inst_13 : Module R M₂] →
                            [inst_14 : Module S M] →
                              [inst_15 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          f) :
      R)
    ((Algebra.norm R : (a : S) → R) 1 : R)
inl₁ :
  Eq.{u_1 + 1} (α := R)
    ((LinearMap.det : (a : A →ₗ[R] A) → R)
        ((↑R :
            {S : Type u_2} →
              {M M₂ : Type u_3} →
                [inst : Semiring R] →
                  [inst_9 : Semiring S] →
                    [inst_10 : AddCommMonoid M] →
                      [inst_11 : AddCommMonoid M₂] →
                        [inst_12 : Module R M] →
                          [inst_13 : Module R M₂] →
                            [inst_14 : Module S M] →
                              [inst_15 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          f) :
      R)
    (1 : R)
inl₂ inl₃ : Eq.{u_1 + 1} (α := R) 1 1
⊢ Eq.{u_1 + 1} (α := R)
    ((LinearMap.det : (a : A →ₗ[R] A) → R)
        ((↑R :
            {S : Type u_2} →
              {M M₂ : Type u_3} →
                [inst : Semiring R] →
                  [inst_9 : Semiring S] →
                    [inst_10 : AddCommMonoid M] →
                      [inst_11 : AddCommMonoid M₂] →
                        [inst_12 : Module R M] →
                          [inst_13 : Module R M₂] →
                            [inst_14 : Module S M] →
                              [inst_15 : Module S M₂] → [CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          f) :
      R)
    ((Algebra.norm R : (a : S) → R) ((LinearMap.det : (a : A →ₗ[S] A) → S) f : S) : R)

Tactic:
rw [det_eq_one_of_not_module_finite (Module.not_finite_of_infinite_basis bA), map_one,
      det_eq_one_of_not_module_finite (Module.not_finite_of_infinite_basis (bS.smulTower bA))]

Premises used: LinearMap.det_eq_one_of_not_module_finite, Module.not_finite_of_infinite_basis, map_one, Module.Basis.smulTower
-- Module: Mathlib.RingTheory.Norm.Transitivity
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Free R S
A : Type u_6
inst_4 : Ring A
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Module.Free S A
a : A
rw :
  Eq.{u_1 + 1} (α := R)
    (((LinearMap.det.{u_6, u_1} (M := A) (A := R) : MonoidHom.{u_6, u_1} (A →ₗ[R] A) R) : (a : A →ₗ[R] A) → R)
        ((↑R :
            {S : Type u_2} →
              {M M₂ : Type u_6} →
                [inst : Semiring R] →
                  [inst_9 : Semiring S] →
                    [inst_10 : AddCommMonoid M] →
                      [inst_11 : AddCommMonoid M₂] →
                        [inst_12 : Module R M] →
                          [inst_13 : Module R M₂] →
                            [inst_14 : Module S M] →
                              [inst_15 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          (S := S) ((lmul S A : (a : A) → Module.End S A) a)) :
      R)
    (((LinearMap.det.{u_6, u_1} (M := A) (A := R) : MonoidHom.{u_6, u_1} (A →ₗ[R] A) R) : (a : A →ₗ[R] A) → R)
        ((lmul R A : (a : A) → Module.End R A) a : Module.End R A) :
      R)
⊢ Eq.{u_1 + 1} (α := R) ((norm R : (a : S) → R) ((norm S : (a : A) → S) a : S) : R) ((norm R : (a : A) → R) a : R)

Tactic:
rw [norm_apply S, norm_apply R a, ← LinearMap.det_restrictScalars]

Premises used: LinearMap.det_restrictScalars, Algebra.norm_apply
-- Module: Mathlib.RingTheory.Norm.Transitivity
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Free R S
A : Type u_6
inst_4 : Ring A
inst_5 : Algebra R A
inst_6 : Algebra S A
inst_7 : IsScalarTower R S A
inst_8 : Module.Free S A
a : A
⊢ Eq.{u_1 + 1} (α := R)
    (((LinearMap.det.{u_6, u_1} (M := A) (A := R) : MonoidHom.{u_6, u_1} (A →ₗ[R] A) R) : (a : A →ₗ[R] A) → R)
        ((↑R :
            {S : Type u_2} →
              {M M₂ : Type u_6} →
                [inst : Semiring R] →
                  [inst_9 : Semiring S] →
                    [inst_10 : AddCommMonoid M] →
                      [inst_11 : AddCommMonoid M₂] →
                        [inst_12 : Module R M] →
                          [inst_13 : Module R M₂] →
                            [inst_14 : Module S M] →
                              [inst_15 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          (S := S) ((lmul S A : (a : A) → Module.End S A) a)) :
      R)
    (((LinearMap.det.{u_6, u_1} (M := A) (A := R) : MonoidHom.{u_6, u_1} (A →ₗ[R] A) R) : (a : A →ₗ[R] A) → R)
        ((lmul R A : (a : A) → Module.End R A) a : Module.End R A) :
      R)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Norm.Transitivity
Goal:
R : Type u_1
inst : CommRing R
L : Type u_6
K : Type u_7
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra R L
inst_5 : Algebra R K
inst_6 : IsScalarTower R K L
x : L
hx : IsIntegral R x
pos : ∀ (h : FiniteDimensional K L), IsIntegral.{u_1, u_7} R (A := K) ((norm K : (a : L) → K) x : K)
neg : ∀ (h : ¬FiniteDimensional K L), IsIntegral.{u_1, u_7} R (A := K) ((norm K : (a : L) → K) x : K)
⊢ IsIntegral.{u_1, u_7} R (A := K) ((norm K : (a : L) → K) x : K)

Tactic:
by_cases h : FiniteDimensional K L

Premises used: FiniteDimensional
-- Module: Mathlib.RingTheory.Norm.Transitivity
Goal:
R : Type u_1
inst : CommRing R
L : Type u_6
K : Type u_7
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra R L
inst_5 : Algebra R K
inst_6 : IsScalarTower R K L
x : L
hx : IsIntegral R x
h : ¬FiniteDimensional K L
⊢ IsIntegral.{u_1, u_7} R (A := K) ((norm K : (a : L) → K) x : K)

Tactic:
simpa [norm_eq_one_of_not_module_finite h] using isIntegral_one

Premises used: isIntegral_one, Algebra.norm_eq_one_of_not_module_finite
-- Module: Mathlib.RingTheory.Norm.Transitivity
Goal:
R : Type u_1
inst : CommRing R
L : Type u_6
K : Type u_7
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra R L
inst_5 : Algebra R K
inst_6 : IsScalarTower R K L
x : L
hx : IsIntegral R x
h : FiniteDimensional K L
F : IntermediateField K L := K⟮x⟯
pos :
  IsIntegral R
    (HPow.hPow (α := K) ((norm K : (a : ↥F) → K) (gen K x) : K) (Fintype.card.{u_6} (Free.ChooseBasisIndex (↥F) L)))
⊢ IsIntegral.{u_1, u_7} R (A := K) ((norm K : (a : L) → K) x : K)

Tactic:
rw [← norm_norm (S := F), ← coe_gen K x, ← IntermediateField.algebraMap_apply,
    norm_algebraMap_of_basis (Module.Free.chooseBasis F L) (gen K x), map_pow]

Premises used: Algebra.norm_algebraMap_of_basis, IntermediateField.AdjoinSimple.gen, Membership.mem, Subtype, map_pow, IntermediateField.algebraMap_apply, Algebra.norm_norm, IntermediateField.AdjoinSimple.coe_gen, Module.Free.chooseBasis
-- Module: Mathlib.RingTheory.Norm.Transitivity
Goal:
R : Type u_1
inst : CommRing R
L : Type u_6
K : Type u_7
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra R L
inst_5 : Algebra R K
inst_6 : IsScalarTower R K L
x : L
hx : IsIntegral R x
h : FiniteDimensional K L
F : IntermediateField K L := K⟮x⟯
pos : IsIntegral.{u_1, u_7} R (A := K) ((norm K : (a : ↥F) → K) (gen K x) : K)
⊢ IsIntegral R
    (HPow.hPow (α := K) ((norm K : (a : ↥F) → K) (gen K x) : K) (Fintype.card.{u_6} (Free.ChooseBasisIndex (↥F) L)))

Tactic:
apply IsIntegral.pow

Premises used: IsIntegral.pow
-- Module: Mathlib.RingTheory.Norm.Transitivity
Goal:
R : Type u_1
inst : CommRing R
L : Type u_6
K : Type u_7
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra R L
inst_5 : Algebra R K
inst_6 : IsScalarTower R K L
x : L
hx : IsIntegral R x
h : FiniteDimensional K L
F : IntermediateField K L := K⟮x⟯
pos : IsIntegral.{u_1, u_6} R (A := AlgebraicClosure ↥F) (Multiset.prod (aroots (minpoly K x) (AlgebraicClosure ↥F)))
⊢ IsIntegral.{u_1, u_7} R (A := K) ((norm K : (a : ↥F) → K) (gen K x) : K)

Tactic:
rw [← isIntegral_algebraMap_iff (algebraMap K (AlgebraicClosure F)).injective,
    norm_gen_eq_prod_roots _ (IsAlgClosed.splits _)]

Premises used: Algebra.algebraMap, Membership.mem, Subtype, RingHom.injective, isIntegral_algebraMap_iff, IntermediateField.AdjoinSimple.norm_gen_eq_prod_roots, IsAlgClosed.splits, AlgebraicClosure
-- Module: Mathlib.RingTheory.Norm.Transitivity
Goal:
R : Type u_1
inst : CommRing R
L : Type u_6
K : Type u_7
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra R L
inst_5 : Algebra R K
inst_6 : IsScalarTower R K L
x : L
hx : IsIntegral R x
h : FiniteDimensional K L
F : IntermediateField K L := K⟮x⟯
⊢ IsIntegral.{u_1, u_6} R (A := AlgebraicClosure ↥F) (Multiset.prod (aroots (minpoly K x) (AlgebraicClosure ↥F)))

Tactic:
IsIntegral.multiset_prod (fun y hy ↦ ⟨minpoly R x, minpoly.monic hx, ?_⟩)

Premises used: minpoly.monic, IsIntegral.multiset_prod, minpoly, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.Norm.Transitivity
Goal:
R : Type u_1
inst : CommRing R
L : Type u_6
K : Type u_7
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra R L
inst_5 : Algebra R K
inst_6 : IsScalarTower R K L
x : L
hx : IsIntegral R x
h : FiniteDimensional K L
F : IntermediateField K L := K⟮x⟯
pos :
  ∀ (y : AlgebraicClosure ↥F)
    (hy : Membership.mem (γ := Multiset (AlgebraicClosure ↥F)) (aroots (minpoly K x) (AlgebraicClosure ↥F)) y),
    eval₂ (algebraMap R (AlgebraicClosure ↥F)) y (minpoly R x) = 0
⊢ IsIntegral.{u_1, u_6} R (A := AlgebraicClosure ↥F) (Multiset.prod (aroots (minpoly K x) (AlgebraicClosure ↥F)))

Tactic:
refine IsIntegral.multiset_prod (fun y hy ↦ ⟨minpoly R x, minpoly.monic hx, ?_⟩)

Premises used: minpoly.monic, IsIntegral.multiset_prod, minpoly, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.Norm.Transitivity
Goal:
R : Type u_1
inst : CommRing R
L : Type u_6
K : Type u_7
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra R L
inst_5 : Algebra R K
inst_6 : IsScalarTower R K L
x : L
hx : IsIntegral R x
h : FiniteDimensional K L
F : IntermediateField K L := K⟮x⟯
y : AlgebraicClosure ↥F
hy : Membership.mem (γ := Multiset (AlgebraicClosure ↥F)) (aroots (minpoly K x) (AlgebraicClosure ↥F)) y
this :
  Eq.{u_6 + 1} (α := AlgebraicClosure ↥F)
    ((aeval y : (a : K[X]) → AlgebraicClosure ↥F) (Polynomial.map (algebraMap R K) (minpoly R x)) : AlgebraicClosure ↥F)
    (0 : AlgebraicClosure ↥F)
⊢ eval₂ (algebraMap R (AlgebraicClosure ↥F)) y (minpoly R x) = 0

Tactic:
simpa
-- Module: Mathlib.RingTheory.Norm.Transitivity
Goal:
R : Type u_1
inst : CommRing R
L : Type u_6
K : Type u_7
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra R L
inst_5 : Algebra R K
inst_6 : IsScalarTower R K L
x : L
hx : IsIntegral R x
h : FiniteDimensional K L
F : IntermediateField K L := K⟮x⟯
y : AlgebraicClosure ↥F
hy : Membership.mem (γ := Multiset (AlgebraicClosure ↥F)) (aroots (minpoly K x) (AlgebraicClosure ↥F)) y
pos :
  Eq.{u_6 + 1} (α := AlgebraicClosure ↥F)
    ((aeval y : (a : K[X]) → AlgebraicClosure ↥F) (Polynomial.map (algebraMap R K) (minpoly R x)) : AlgebraicClosure ↥F)
    (0 : AlgebraicClosure ↥F)
⊢ eval₂ (algebraMap R (AlgebraicClosure ↥F)) y (minpoly R x) = 0

Tactic:
suffices (aeval y) ((minpoly R x).map (algebraMap R K)) = 0 by simpa
-- Module: Mathlib.RingTheory.Norm.Transitivity
Goal:
R : Type u_1
inst : CommRing R
L : Type u_6
K : Type u_7
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : Algebra R L
inst_5 : Algebra R K
inst_6 : IsScalarTower R K L
x : L
hx : IsIntegral R x
h : FiniteDimensional K L
F : IntermediateField K L := K⟮x⟯
y : AlgebraicClosure ↥F
hy : Membership.mem (γ := Multiset (AlgebraicClosure ↥F)) (aroots (minpoly K x) (AlgebraicClosure ↥F)) y
⊢ Eq.{u_6 + 1} (α := L) ((aeval x : (a : K[X]) → L) (Polynomial.map (algebraMap R K) (minpoly R x)) : L) (0 : L)

Tactic:
simp