awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Norm.Basic
Goal:
A₁ : Type u_8
B₁ : Type u_9
A₂ : Type u_10
B₂ : Type u_11
inst : CommRing A₁
inst_1 : Ring B₁
inst_2 : CommRing A₂
inst_3 : Ring B₂
inst_4 : Algebra A₁ B₁
inst_5 : Algebra A₂ B₂
e₁ : A₁ ≃+* A₂
e₂ : B₁ ≃+* B₂
he :
  Eq (α := A₁ →+* B₂) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A₂ B₂) (↑e₁ : A₁ →+* A₂))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e₂ : B₁ →+* B₂) (algebraMap A₁ B₁))
x : B₁
refine_2 :
  Eq.{u_8 + 1} (α := A₁) ((norm A₁ : (a : B₁) → A₁) x : A₁)
    ((e₁.symm : (a : A₂) → A₁) ((norm A₂ : (a : B₂) → A₂) ((e₂ : (a : B₁) → B₂) x : B₂) : A₂) : A₁)
refine_1 :
  ∀ (c : A₁) (x : B₂),
    HMul.hMul (α := B₂)
        ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e₂ : B₁ →+* B₂) (algebraMap A₁ B₁) : (a : A₁) → B₂) c :
          B₂)
        x =
      HMul.hMul (β := B₂) x
        ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e₂ : B₁ →+* B₂) (algebraMap A₁ B₁) : (a : A₁) → B₂) c :
          B₂)
⊢ Eq.{u_8 + 1} (α := A₁) ((norm A₁ : (a : B₁) → A₁) x : A₁)
    ((e₁.symm : (a : A₂) → A₁) ((norm A₂ : (a : B₂) → A₂) ((e₂ : (a : B₁) → B₂) x : B₂) : A₂) : A₁)

Tactic:
letI := (RingHom.comp (e₂ : B₁ →+* B₂) (algebraMap A₁ B₁)).toAlgebra' ?_
-- Module: Mathlib.RingTheory.Norm.Basic
Goal:
A₁ : Type u_8
B₁ : Type u_9
A₂ : Type u_10
B₂ : Type u_11
inst : CommRing A₁
inst_1 : Ring B₁
inst_2 : CommRing A₂
inst_3 : Ring B₂
inst_4 : Algebra A₁ B₁
inst_5 : Algebra A₂ B₂
e₁ : A₁ ≃+* A₂
e₂ : B₁ ≃+* B₂
he :
  Eq (α := A₁ →+* B₂) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A₂ B₂) (↑e₁ : A₁ →+* A₂))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e₂ : B₁ →+* B₂) (algebraMap A₁ B₁))
x : B₁
this : Algebra A₁ B₂ :=
  RingHom.toAlgebra' (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e₂ : B₁ →+* B₂) (algebraMap A₁ B₁)) ⋯
e' : B₁ ≃ₐ[A₁] B₂ := { toEquiv := e₂.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
refine_2 :
  Eq.{u_8 + 1} (α := A₁) ((norm A₁ : (a : B₂) → A₁) ((e' : (a : B₁) → B₂) x : B₂) : A₁)
    ((e₁.symm : (a : A₂) → A₁)
        ((e₁ : (a : A₁) → A₂) ((norm A₁ : (a : B₂) → A₁) ((e₂ : (a : B₁) → B₂) x : B₂) : A₁) : A₂) :
      A₁)
⊢ Eq.{u_8 + 1} (α := A₁) ((norm A₁ : (a : B₁) → A₁) x : A₁)
    ((e₁.symm : (a : A₂) → A₁) ((norm A₂ : (a : B₂) → A₂) ((e₂ : (a : B₁) → B₂) x : B₂) : A₂) : A₁)

Tactic:
rw [← Algebra.norm_eq_of_ringEquiv e₁ he, ← Algebra.norm_eq_of_algEquiv e']

Premises used: Algebra.norm_eq_of_algEquiv, Algebra.norm_eq_of_ringEquiv
-- Module: Mathlib.RingTheory.Norm.Basic
Goal:
A₁ : Type u_8
B₁ : Type u_9
A₂ : Type u_10
B₂ : Type u_11
inst : CommRing A₁
inst_1 : Ring B₁
inst_2 : CommRing A₂
inst_3 : Ring B₂
inst_4 : Algebra A₁ B₁
inst_5 : Algebra A₂ B₂
e₁ : A₁ ≃+* A₂
e₂ : B₁ ≃+* B₂
he :
  Eq (α := A₁ →+* B₂) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A₂ B₂) (↑e₁ : A₁ →+* A₂))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e₂ : B₁ →+* B₂) (algebraMap A₁ B₁))
x : B₁
this : Algebra A₁ B₂ :=
  RingHom.toAlgebra' (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e₂ : B₁ →+* B₂) (algebraMap A₁ B₁)) ⋯
e' : B₁ ≃ₐ[A₁] B₂ := { toEquiv := e₂.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
⊢ Eq.{u_8 + 1} (α := A₁) ((norm A₁ : (a : B₂) → A₁) ((e' : (a : B₁) → B₂) x : B₂) : A₁)
    ((e₁.symm : (a : A₂) → A₁)
        ((e₁ : (a : A₁) → A₂) ((norm A₁ : (a : B₂) → A₁) ((e₂ : (a : B₁) → B₂) x : B₂) : A₁) : A₂) :
      A₁)

Tactic:
simp [e']
-- Module: Mathlib.RingTheory.Norm.Basic
Goal:
A₁ : Type u_8
B₁ : Type u_9
A₂ : Type u_10
B₂ : Type u_11
inst : CommRing A₁
inst_1 : Ring B₁
inst_2 : CommRing A₂
inst_3 : Ring B₂
inst_4 : Algebra A₁ B₁
inst_5 : Algebra A₂ B₂
e₁ : A₁ ≃+* A₂
e₂ : B₁ ≃+* B₂
he :
  Eq (α := A₁ →+* B₂) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A₂ B₂) (↑e₁ : A₁ →+* A₂))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e₂ : B₁ →+* B₂) (algebraMap A₁ B₁))
x_1 : B₁
c : A₁
x : B₂
refine_1 :
  Eq.{u_9 + 1} (α := B₁)
    ((e₂.symm : (a : B₂) → B₁)
        (HMul.hMul (α := B₂)
          ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e₂ : B₁ →+* B₂) (algebraMap A₁ B₁) : (a : A₁) → B₂)
              c :
            B₂)
          x) :
      B₁)
    ((e₂.symm : (a : B₂) → B₁)
        (HMul.hMul (β := B₂) x
          ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e₂ : B₁ →+* B₂) (algebraMap A₁ B₁) : (a : A₁) → B₂)
              c :
            B₂)) :
      B₁)
⊢ HMul.hMul (α := B₂)
      ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e₂ : B₁ →+* B₂) (algebraMap A₁ B₁) : (a : A₁) → B₂) c :
        B₂)
      x =
    HMul.hMul (β := B₂) x
      ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e₂ : B₁ →+* B₂) (algebraMap A₁ B₁) : (a : A₁) → B₂) c :
        B₂)

Tactic:
apply e₂.symm.injective

Premises used: RingEquiv.injective, RingEquiv.symm
-- Module: Mathlib.RingTheory.Norm.Basic
Goal:
A₁ : Type u_8
B₁ : Type u_9
A₂ : Type u_10
B₂ : Type u_11
inst : CommRing A₁
inst_1 : Ring B₁
inst_2 : CommRing A₂
inst_3 : Ring B₂
inst_4 : Algebra A₁ B₁
inst_5 : Algebra A₂ B₂
e₁ : A₁ ≃+* A₂
e₂ : B₁ ≃+* B₂
he :
  Eq (α := A₁ →+* B₂) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A₂ B₂) (↑e₁ : A₁ →+* A₂))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e₂ : B₁ →+* B₂) (algebraMap A₁ B₁))
x_1 : B₁
c : A₁
x : B₂
⊢ Eq.{u_9 + 1} (α := B₁)
    ((e₂.symm : (a : B₂) → B₁)
        (HMul.hMul (α := B₂)
          ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e₂ : B₁ →+* B₂) (algebraMap A₁ B₁) : (a : A₁) → B₂)
              c :
            B₂)
          x) :
      B₁)
    ((e₂.symm : (a : B₂) → B₁)
        (HMul.hMul (β := B₂) x
          ((@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e₂ : B₁ →+* B₂) (algebraMap A₁ B₁) : (a : A₁) → B₂)
              c :
            B₂)) :
      B₁)

Tactic:
simp only [RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply, map_mul,
    RingEquiv.symm_apply_apply, commutes]

Premises used: RingHom.coe_coe, RingEquiv.symm_apply_apply, map_mul, RingHom.coe_comp, Function.comp_apply, Algebra.commutes
-- Module: Mathlib.RingTheory.Norm.Defs
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
x : S
⊢ Eq.{u_1 + 1} (α := R) ((norm R : (a : S) → R) x : R)
    (((LinearMap.det.{u_2, u_1} (M := S) (A := R) : MonoidHom.{u_2, u_1} (S →ₗ[R] S) R) : (a : S →ₗ[R] S) → R)
        ((lmul R S : (a : S) → End R S) x : End R S) :
      R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Norm.Defs
Goal:
R : Type u_1
inst : CommRing R
h : ∀ (x : R), Eq (α := R) ((norm R : (a : R) → R) x : R) ((MonoidHom.id R : (a : R) → R) x : R)
⊢ Eq (α := R →* R) (norm R) (MonoidHom.id R)

Tactic:
ext
-- Module: Mathlib.RingTheory.Norm.Defs
Goal:
R : Type u_1
inst : CommRing R
x : R
⊢ Eq (α := R) ((norm R : (a : R) → R) x : R) ((MonoidHom.id R : (a : R) → R) x : R)

Tactic:
simp [norm_apply]

Premises used: Algebra.norm_apply
-- Module: Mathlib.RingTheory.Norm.Defs
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
h : ¬∃ (s : Finset S), Nonempty (Basis (↥s) R S)
x : S
rw :
  Eq.{u_1 + 1} (α := R)
    ((if H : ∃ (s : Finset S), Nonempty (Basis (↥s) R S) then
            detAux.{u_2, u_2, u_1} (M := S) (ι := ↥(H.choose (p := fun (s : Finset S) ↦ Nonempty (Basis (↥s) R S))))
              (Trunc.mk (Nonempty.some ⋯))
          else 1 :
          (a : S →ₗ[R] S) → R)
        ((lmul R S : (a : S) → End R S) x : End R S) :
      R)
    (1 : R)
⊢ Eq.{u_1 + 1} (α := R) ((norm R : (a : S) → R) x : R) (1 : R)

Tactic:
rw [norm_apply, LinearMap.det]

Premises used: LinearMap.det, Algebra.norm_apply
-- Module: Mathlib.RingTheory.Norm.Defs
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
h : ¬∃ (s : Finset S), Nonempty (Basis (↥s) R S)
x : S
pos :
  ∀ (h : ∃ (s : Finset S), Nonempty (Basis (↥s) R S)),
    Eq.{u_1 + 1} (α := R)
      (((detAux.{u_2, u_2, u_1} (M := S) (ι := ↥(h.choose (p := fun (s : Finset S) ↦ Nonempty (Basis (↥s) R S))))
                (Trunc.mk (Nonempty.some ⋯)) :
              MonoidHom.{u_2, u_1} (S →ₗ[R] S) R) :
            (a : S →ₗ[R] S) → R)
          ((lmul R S : (a : S) → End R S) x : End R S) :
        R)
      (1 : R)
neg :
  (¬∃ (s : Finset S), Nonempty (Basis (↥s) R S)) →
    Eq.{u_1 + 1} (α := R) ((1 : (a : S →ₗ[R] S) → R) ((lmul R S : (a : S) → End R S) x : End R S) : R) (1 : R)
⊢ Eq.{u_1 + 1} (α := R)
    ((if H : ∃ (s : Finset S), Nonempty (Basis (↥s) R S) then
            detAux.{u_2, u_2, u_1} (M := S) (ι := ↥(H.choose (p := fun (s : Finset S) ↦ Nonempty (Basis (↥s) R S))))
              (Trunc.mk (Nonempty.some ⋯))
          else 1 :
          (a : S →ₗ[R] S) → R)
        ((lmul R S : (a : S) → End R S) x : End R S) :
      R)
    (1 : R)

Tactic:
split_ifs
-- Module: Mathlib.RingTheory.Norm.Defs
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
h : ¬∃ (s : Finset S), Nonempty (Basis (↥s) R S)
x : S
h_1 : ∃ (s : Finset S), Nonempty (Basis (↥s) R S)
⊢ Eq.{u_1 + 1} (α := R)
    (((detAux.{u_2, u_2, u_1} (M := S) (ι := ↥(h_1.choose (p := fun (s : Finset S) ↦ Nonempty (Basis (↥s) R S))))
              (Trunc.mk (Nonempty.some ⋯)) :
            MonoidHom.{u_2, u_1} (S →ₗ[R] S) R) :
          (a : S →ₗ[R] S) → R)
        ((lmul R S : (a : S) → End R S) x : End R S) :
      R)
    (1 : R)

Tactic:
trivial
-- Module: Mathlib.RingTheory.Norm.Defs
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
h : ¬∃ (s : Finset S), Nonempty (Basis (↥s) R S)
x : S
h_1 : ¬∃ (s : Finset S), Nonempty (Basis (↥s) R S)
⊢ Eq.{u_1 + 1} (α := R) ((1 : (a : S →ₗ[R] S) → R) ((lmul R S : (a : S) → End R S) x : End R S) : R) (1 : R)

Tactic:
trivial
-- Module: Mathlib.RingTheory.Norm.Defs
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
h : ¬Module.Finite R S
x : S
⊢ Eq.{u_1 + 1} (α := R) ((norm R : (a : S) → R) x : R) (1 : R)

Tactic:
norm_eq_one_of_not_exists_basis _ (mt ?_ h) _

Premises used: mt, Algebra.norm_eq_one_of_not_exists_basis
-- Module: Mathlib.RingTheory.Norm.Defs
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
h : ¬Module.Finite R S
x : S
refine : (∃ (s : Finset S), Nonempty (Basis (↥s) R S)) → Module.Finite R S
⊢ Eq.{u_1 + 1} (α := R) ((norm R : (a : S) → R) x : R) (1 : R)

Tactic:
refine norm_eq_one_of_not_exists_basis _ (mt ?_ h) _

Premises used: mt, Algebra.norm_eq_one_of_not_exists_basis
-- Module: Mathlib.RingTheory.Norm.Defs
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
h : ¬Module.Finite R S
x : S
s : Finset S
b : Basis (↥s) R S
⊢ Module.Finite R S

Tactic:
Module.Finite.of_basis b

Premises used: Module.Finite.of_basis
-- Module: Mathlib.RingTheory.Norm.Defs
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
h : ¬Module.Finite R S
x : S
s : Finset S
b : Basis (↥s) R S
⊢ Module.Finite R S

Tactic:
exact Module.Finite.of_basis b

Premises used: Module.Finite.of_basis
-- Module: Mathlib.RingTheory.Norm.Defs
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
ι : Type w
inst_3 : Fintype ι
inst_4 : DecidableEq ι
b : Basis ι R S
s : S
rw :
  Eq.{u_1 + 1} (α := R)
    (det.{u_1, w} (n := ι) ((toMatrix b b : (a : S →ₗ[R] S) → Matrix ι ι R) ((lmul R S : (a : S) → End R S) s)))
    (det.{u_1, w} (n := ι) ((toMatrix b b : (a : S →ₗ[R] S) → Matrix ι ι R) (mulLeft R s)))
⊢ Eq.{u_1 + 1} (α := R) ((norm R : (a : S) → R) s : R)
    (det.{u_1, w} (n := ι) ((leftMulMatrix b : (a : S) → Matrix ι ι R) s) : R)

Tactic:
rw [norm_apply, ← LinearMap.det_toMatrix b, ← toMatrix_lmul_eq]

Premises used: Algebra.toMatrix_lmul_eq, Algebra.norm_apply, LinearMap.det_toMatrix
-- Module: Mathlib.RingTheory.Norm.Defs
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
ι : Type w
inst_3 : Fintype ι
inst_4 : DecidableEq ι
b : Basis ι R S
s : S
⊢ Eq.{u_1 + 1} (α := R)
    (det.{u_1, w} (n := ι) ((toMatrix b b : (a : S →ₗ[R] S) → Matrix ι ι R) ((lmul R S : (a : S) → End R S) s)))
    (det.{u_1, w} (n := ι) ((toMatrix b b : (a : S →ₗ[R] S) → Matrix ι ι R) (mulLeft R s)))

Tactic:
rfl
-- Module: Mathlib.RingTheory.Norm.Defs
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
ι : Type w
inst_3 : Fintype ι
b : Basis ι R S
x : R
haveI : ∀ (this : DecidableEq ι), (norm R : (a : S) → R) ((algebraMap R S : (a : R) → S) x : S) = x ^ Fintype.card ι
⊢ (norm R : (a : S) → R) ((algebraMap R S : (a : R) → S) x : S) = x ^ Fintype.card ι

Tactic:
haveI := Classical.decEq ι
-- Module: Mathlib.RingTheory.Norm.Defs
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
ι : Type w
inst_3 : Fintype ι
b : Basis ι R S
x : R
this : DecidableEq ι
rw :
  det.{u_1, w} (n := ι) ((toMatrix b b : (a : S →ₗ[R] S) → Matrix ι ι R) ((lsmul R R S : (a : R) → End R S) x)) =
    x ^ Fintype.card ι
⊢ (norm R : (a : S) → R) ((algebraMap R S : (a : R) → S) x : S) = x ^ Fintype.card ι

Tactic:
rw [norm_apply, ← det_toMatrix b, lmul_algebraMap]

Premises used: Algebra.lmul_algebraMap, Algebra.norm_apply, LinearMap.det_toMatrix
-- Module: Mathlib.RingTheory.Norm.Defs
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
ι : Type w
inst_3 : Fintype ι
b : Basis ι R S
x : R
this : DecidableEq ι
⊢ det.{u_1, w} (n := ι) ((toMatrix b b : (a : S →ₗ[R] S) → Matrix ι ι R) ((lsmul R R S : (a : R) → End R S) x)) =
    x ^ Fintype.card ι

Tactic:
simp
-- Module: Mathlib.RingTheory.Norm.Defs
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : Free R S
x : R
rw :
  ((LinearMap.det.{u_2, u_1} (M := S) (A := R) : MonoidHom.{u_2, u_1} (S →ₗ[R] S) R) : (a : S →ₗ[R] S) → R)
      ((lmul R S : (a : S) → End R S) ((algebraMap R S : (a : R) → S) x : S) : End R S) =
    x ^ finrank R S
rw₁ :
  ((LinearMap.det.{u_2, u_1} (M := S) (A := R) : MonoidHom.{u_2, u_1} (S →ₗ[R] S) R) : (a : S →ₗ[R] S) → R)
      ((lsmul R R S : (a : R) → End R S) x : End R S) =
    x ^ finrank R S
rw₂ rw₃ : x ^ finrank R S = x ^ finrank R S
⊢ (norm R : (a : S) → R) ((algebraMap R S : (a : R) → S) x : S) = x ^ finrank R S

Tactic:
rw [norm_apply, lmul_algebraMap, det_lsmul]

Premises used: Algebra.det_lsmul, Algebra.lmul_algebraMap, Algebra.norm_apply
-- Module: Mathlib.RingTheory.Norm.Defs
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : Free R S
n : ℕ
rw : (norm R : (a : S) → R) ((algebraMap R S : (a : R) → S) (↑n : R) : S) = HPow.hPow (α := R) (↑n : R) (finrank R S)
rw₁ rw₂ : HPow.hPow (α := R) (↑n : R) (finrank R S) = HPow.hPow (α := R) (↑n : R) (finrank R S)
⊢ (norm R : (a : S) → R) (↑n : S) = HPow.hPow (α := R) (↑n : R) (finrank R S)

Tactic:
rw [← map_natCast (algebraMap R S), Algebra.norm_algebraMap]

Premises used: Algebra.algebraMap, map_natCast, Algebra.norm_algebraMap
-- Module: Mathlib.RingTheory.NormTrace
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Free A B
inst_4 : Module.Finite A B
a : A
x : B
ι : Type u_2 := Free.ChooseBasisIndex A B
b : Basis ι A B := Free.chooseBasis A B
haveI :
  ∀ (this : Fintype ι),
    ∃ (r : A),
      (norm A : (a : B) → A) (1 + a • x) =
        1 + HMul.hMul (α := A) ((trace A B : (a : B) → A) x : A) a + r * HPow.hPow (β := ℕ) a 2
⊢ ∃ (r : A),
    (norm A : (a : B) → A) (1 + a • x) =
      1 + HMul.hMul (α := A) ((trace A B : (a : B) → A) x : A) a + r * HPow.hPow (β := ℕ) a 2

Tactic:
haveI : Fintype ι := inferInstance
-- Module: Mathlib.RingTheory.NormTrace
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Free A B
inst_4 : Module.Finite A B
a : A
x : B
ι : Type u_2 := Free.ChooseBasisIndex A B
b : Basis ι A B := Free.chooseBasis A B
this : Fintype ι
clear_value :
  ∀ (ι : Type u_2) (b : Basis ι A B) (this : Fintype ι),
    ∃ (r : A),
      (norm A : (a : B) → A) (1 + a • x) =
        1 + HMul.hMul (α := A) ((trace A B : (a : B) → A) x : A) a + r * HPow.hPow (β := ℕ) a 2
⊢ ∃ (r : A),
    (norm A : (a : B) → A) (1 + a • x) =
      1 + HMul.hMul (α := A) ((trace A B : (a : B) → A) x : A) a + r * HPow.hPow (β := ℕ) a 2

Tactic:
clear_value ι b
-- Module: Mathlib.RingTheory.NormTrace
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Free A B
inst_4 : Module.Finite A B
a : A
x : B
ι : Type u_2
b : Basis ι A B
this : Fintype ι
simp_rw :
  ∃ (r : A),
    Matrix.det.{u_1, u_2} (n := ι) ((leftMulMatrix b : (a : B) → Matrix ι ι A) (1 + a • x)) =
      1 + Matrix.trace.{u_2, u_1} (n := ι) ((leftMulMatrix b : (a : B) → Matrix ι ι A) x) * a +
        r * HPow.hPow (β := ℕ) a 2
⊢ ∃ (r : A),
    (norm A : (a : B) → A) (1 + a • x) =
      1 + HMul.hMul (α := A) ((trace A B : (a : B) → A) x : A) a + r * HPow.hPow (β := ℕ) a 2

Tactic:
simp_rw [Algebra.norm_eq_matrix_det b, Algebra.trace_eq_matrix_trace b]

Premises used: Algebra.norm_eq_matrix_det, Algebra.trace_eq_matrix_trace
-- Module: Mathlib.RingTheory.NormTrace
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Free A B
inst_4 : Module.Finite A B
a : A
x : B
ι : Type u_2
b : Basis ι A B
this : Fintype ι
simp :
  ∃ (r : A),
    1 + Matrix.trace.{u_2, u_1} (n := ι) ((leftMulMatrix b : (a : B) → Matrix ι ι A) x) * a +
        Polynomial.eval a
            (1 +
                    HSMul.hSMul (α := Polynomial A) (β := Matrix.{u_2, u_2, u_1} ι ι (Polynomial A)) Polynomial.X
                      (Matrix.map (α := A) ((leftMulMatrix b : (a : B) → Matrix ι ι A) x)
                        (⇑Polynomial.C : (a : A) → Polynomial A))).det.divX.divX *
          HPow.hPow (β := ℕ) a 2 =
      1 + Matrix.trace.{u_2, u_1} (n := ι) ((leftMulMatrix b : (a : B) → Matrix ι ι A) x) * a +
        r * HPow.hPow (β := ℕ) a 2
⊢ ∃ (r : A),
    Matrix.det.{u_1, u_2} (n := ι) ((leftMulMatrix b : (a : B) → Matrix ι ι A) (1 + a • x)) =
      1 + Matrix.trace.{u_2, u_1} (n := ι) ((leftMulMatrix b : (a : B) → Matrix ι ι A) x) * a +
        r * HPow.hPow (β := ℕ) a 2

Tactic:
simp only [map_add, map_one, map_smul, Matrix.det_one_add_smul a]

Premises used: Matrix.det_one_add_smul, map_add, map_one, map_smul
-- Module: Mathlib.RingTheory.NormTrace
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Free A B
inst_4 : Module.Finite A B
a : A
x : B
ι : Type u_2
b : Basis ι A B
this : Fintype ι
⊢ ∃ (r : A),
    1 + Matrix.trace.{u_2, u_1} (n := ι) ((leftMulMatrix b : (a : B) → Matrix ι ι A) x) * a +
        Polynomial.eval a
            (1 +
                    HSMul.hSMul (α := Polynomial A) (β := Matrix.{u_2, u_2, u_1} ι ι (Polynomial A)) Polynomial.X
                      (Matrix.map (α := A) ((leftMulMatrix b : (a : B) → Matrix ι ι A) x)
                        (⇑Polynomial.C : (a : A) → Polynomial A))).det.divX.divX *
          HPow.hPow (β := ℕ) a 2 =
      1 + Matrix.trace.{u_2, u_1} (n := ι) ((leftMulMatrix b : (a : B) → Matrix ι ι A) x) * a +
        r * HPow.hPow (β := ℕ) a 2

Tactic:
⟨_, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.RingTheory.NormTrace
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Free A B
inst_4 : Module.Finite A B
a : A
x : B
ι : Type u_2
b : Basis ι A B
this : Fintype ι
⊢ ∃ (r : A),
    1 + Matrix.trace.{u_2, u_1} (n := ι) ((leftMulMatrix b : (a : B) → Matrix ι ι A) x) * a +
        Polynomial.eval a
            (1 +
                    HSMul.hSMul (α := Polynomial A) (β := Matrix.{u_2, u_2, u_1} ι ι (Polynomial A)) Polynomial.X
                      (Matrix.map (α := A) ((leftMulMatrix b : (a : B) → Matrix ι ι A) x)
                        (⇑Polynomial.C : (a : A) → Polynomial A))).det.divX.divX *
          HPow.hPow (β := ℕ) a 2 =
      1 + Matrix.trace.{u_2, u_1} (n := ι) ((leftMulMatrix b : (a : B) → Matrix ι ι A) x) * a +
        r * HPow.hPow (β := ℕ) a 2

Tactic:
exact ⟨_, rfl⟩
-- Module: Mathlib.RingTheory.NormTrace
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Free A B
inst_4 : Module.Finite A B
a : A
x : B
let let₁ let₂ let₃ :
  ∃ (r : A),
    (norm A : (a : B) → A) (1 + a • x) =
      1 + HMul.hMul (α := A) ((trace A B : (a : B) → A) x : A) a + r * HPow.hPow (β := ℕ) a 2
let₄ :
  let ι := Free.ChooseBasisIndex A B;
  ∀ (this : Fintype ι),
    ∃ (r : A),
      (norm A : (a : B) → A) (1 + a • x) =
        1 + HMul.hMul (α := A) ((trace A B : (a : B) → A) x : A) a + r * HPow.hPow (β := ℕ) a 2
let₅ :
  ∀ (ι : Type u_2) (b : Basis ι A B) (this : Fintype ι),
    ∃ (r : A),
      (norm A : (a : B) → A) (1 + a • x) =
        1 + HMul.hMul (α := A) ((trace A B : (a : B) → A) x : A) a + r * HPow.hPow (β := ℕ) a 2
let₆ :
  ∀ (ι : Type u_2) (b : Basis ι A B) (this : Fintype ι),
    ∃ (r : A),
      Matrix.det.{u_1, u_2} (n := ι) ((leftMulMatrix b : (a : B) → Matrix ι ι A) (1 + a • x)) =
        1 + Matrix.trace.{u_2, u_1} (n := ι) ((leftMulMatrix b : (a : B) → Matrix ι ι A) x) * a +
          r * HPow.hPow (β := ℕ) a 2
let₇ :
  ∀ (ι : Type u_2) (b : Basis ι A B) (this : Fintype ι),
    ∃ (r : A),
      1 + Matrix.trace.{u_2, u_1} (n := ι) ((leftMulMatrix b : (a : B) → Matrix ι ι A) x) * a +
          Polynomial.eval a
              (1 +
                      HSMul.hSMul (α := Polynomial A) (β := Matrix.{u_2, u_2, u_1} ι ι (Polynomial A)) Polynomial.X
                        (Matrix.map (α := A) ((leftMulMatrix b : (a : B) → Matrix ι ι A) x)
                          (⇑Polynomial.C : (a : A) → Polynomial A))).det.divX.divX *
            HPow.hPow (β := ℕ) a 2 =
        1 + Matrix.trace.{u_2, u_1} (n := ι) ((leftMulMatrix b : (a : B) → Matrix ι ι A) x) * a +
          r * HPow.hPow (β := ℕ) a 2
⊢ ∃ (r : A),
    (norm A : (a : B) → A) (1 + a • x) =
      1 + HMul.hMul (α := A) ((trace A B : (a : B) → A) x : A) a + r * HPow.hPow (β := ℕ) a 2

Tactic:
classical
  let ι := Module.Free.ChooseBasisIndex A B
  let b : Basis ι A B := Module.Free.chooseBasis _ _
  haveI : Fintype ι := inferInstance
  clear_value ι b
  simp_rw [Algebra.norm_eq_matrix_det b, Algebra.trace_eq_matrix_trace b]
  simp only [map_add, map_one, map_smul, Matrix.det_one_add_smul a]
  exact ⟨_, rfl⟩

Premises used: Matrix.det_one_add_smul, map_add, map_one, map_smul
-- Module: Mathlib.RingTheory.NormalClosure
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : IsDomain S
inst_4 : Algebra R S
inst_5 : Module.IsTorsionFree R S
⊢ IsScalarTower S L ↥E

Tactic:
IsScalarTower.of_algebraMap_eq' rfl

Premises used: IsScalarTower.of_algebraMap_eq', rfl
-- Module: Mathlib.RingTheory.NormalClosure
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : IsDomain S
inst_4 : Algebra R S
inst_5 : Module.IsTorsionFree R S
⊢ IsDomain.{u_2} T

Tactic:
inferInstanceAs (IsDomain (integralClosure S E))

Premises used: _private.0.Ring.instIsDomainNormalClosure._proof_1
-- Module: Mathlib.RingTheory.NormalClosure
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : IsDomain S
inst_4 : Algebra R S
inst_5 : Module.IsTorsionFree R S
⊢ Nontrivial.{u_2} T

Tactic:
inferInstanceAs (Nontrivial (integralClosure S E))

Premises used: _private.0.Ring.instNontrivialNormalClosure._proof_1
-- Module: Mathlib.RingTheory.NormalClosure
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : IsDomain S
inst_4 : Algebra R S
inst_5 : Module.IsTorsionFree R S
⊢ IsScalarTower S T ↥E

Tactic:
inferInstanceAs (IsScalarTower S (integralClosure S E) E)

Premises used: _private.0.Ring.instIsScalarTowerNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure._proof_1
-- Module: Mathlib.RingTheory.NormalClosure
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : IsDomain R
inst_3 : IsDomain S
inst_4 : Algebra R S
inst_5 : Module.IsTorsionFree R S
⊢ IsIntegralClosure T S ↥E

Tactic:
integralClosure.isIntegralClosure S E

Premises used: Ring.NormalClosure, Set.Mem, iSup, FractionRing, IntermediateField.normalClosure, Membership.mem, Subtype, IntermediateField.adjoin, integralClosure.isIntegralClosure, AlgebraicClosure