awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Norm.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
F : Type u_6
inst_3 : Field F
inst_4 : Algebra R F
pb : PowerBasis R S
hE : Splits (Polynomial.map (algebraMap R F) (minpoly R pb.gen))
hfx : IsSeparable R pb.gen
this : DecidableEq F := Classical.decEq F
x : { x : F // x ∈ aroots (minpoly R pb.gen) F }
⊢ (↑x : F) = _root_.id (↑x : F)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Norm.Basic
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
F : Type u_6
inst_3 : Field F
inst_4 : Algebra R F
pb : PowerBasis R S
hE : Splits (Polynomial.map (algebraMap R F) (minpoly R pb.gen))
hfx : IsSeparable R pb.gen
this : DecidableEq F := Classical.decEq F
σ : S →ₐ[R] F
⊢ Eq.{u_6 + 1} (α := F) ((fun (σ : S →ₐ[R] F) ↦ ((σ : (a : S) → F) pb.gen : F)) σ)
    ((fun (x : { y : F // y ∈ aroots (minpoly R pb.gen) F }) ↦ (↑x : F))
      ((pb.liftEquiv' : (a : S →ₐ[R] F) → { y : F // y ∈ (minpoly R pb.gen).aroots F }) σ))

Tactic:
simp only [PowerBasis.liftEquiv'_apply_coe]

Premises used: PowerBasis.liftEquiv'_apply_coe
-- Module: Mathlib.RingTheory.Norm.Basic
Goal:
K : Type u_4
L : Type u_5
F : Type u_6
inst : Field K
inst_1 : Field L
inst_2 : Field F
inst_3 : Algebra K L
inst_4 : Algebra K F
E : Type u_7
inst_5 : Field E
inst_6 : Algebra K E
inst_7 : Algebra L F
inst_8 : IsScalarTower K L F
inst_9 : IsAlgClosed E
inst_10 : Algebra.IsSeparable K F
inst_11 : FiniteDimensional K F
pb : PowerBasis K L
⊢ FiniteDimensional L F

Tactic:
haveI : FiniteDimensional L F := FiniteDimensional.right K L F
-- Module: Mathlib.RingTheory.Norm.Basic
Goal:
K : Type u_4
L : Type u_5
F : Type u_6
inst : Field K
inst_1 : Field L
inst_2 : Field F
inst_3 : Algebra K L
inst_4 : Algebra K F
E : Type u_7
inst_5 : Field E
inst_6 : Algebra K E
inst_7 : Algebra L F
inst_8 : IsScalarTower K L F
inst_9 : IsAlgClosed E
inst_10 : Algebra.IsSeparable K F
inst_11 : FiniteDimensional K F
pb : PowerBasis K L
this : FiniteDimensional L F
⊢ Algebra.IsSeparable L F

Tactic:
haveI : Algebra.IsSeparable L F := Algebra.isSeparable_tower_top_of_isSeparable K L F
-- Module: Mathlib.RingTheory.Norm.Basic
Goal:
K : Type u_4
L : Type u_5
F : Type u_6
inst : Field K
inst_1 : Field L
inst_2 : Field F
inst_3 : Algebra K L
inst_4 : Algebra K F
E : Type u_7
inst_5 : Field E
inst_6 : Algebra K E
inst_7 : Algebra L F
inst_8 : IsScalarTower K L F
inst_9 : IsAlgClosed E
inst_10 : Algebra.IsSeparable K F
inst_11 : FiniteDimensional K F
pb : PowerBasis K L
this_1 : FiniteDimensional L F
this_2 : Algebra.IsSeparable L F
this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
rw :
  Eq.{u_7 + 1} (α := E)
    (∏ a : L →ₐ[K] E,
      ∏ s : F →ₐ[L] E,
        (Sigma.fst (β := fun (f : L →ₐ[K] E) ↦ F →ₐ[L] E) (Sigma.mk (β := fun (f : L →ₐ[K] E) ↦ F →ₐ[L] E) a s) :
            (a : L) → E)
          pb.gen)
    (∏ x : L →ₐ[K] E, HPow.hPow (α := E) ((x : (a : L) → E) pb.gen : E) (finrank L F))
rw₁ :
  ∀ (x : F →ₐ[K] E),
    Eq.{u_7 + 1} (α := E) ((x : (a : F) → E) ((algebraMap L F : (a : L) → F) pb.gen : F) : E)
      ((Sigma.fst (β := fun (f : L →ₐ[K] E) ↦ F →ₐ[L] E)
              ((algHomEquivSigma : (a : F →ₐ[K] E) → (f : L →ₐ[K] E) × (F →ₐ[L] E)) x) :
            (a : L) → E)
          pb.gen :
        E)
⊢ ∏ σ : F →ₐ[K] E, (σ : (a : F) → E) ((algebraMap L F : (a : L) → F) pb.gen : F) =
    HPow.hPow (α := E) (∏ σ : L →ₐ[K] E, (σ : (a : L) → E) pb.gen) (finrank L F)

Tactic:
rw [Fintype.prod_equiv algHomEquivSigma (fun σ : F →ₐ[K] E => _) fun σ => σ.1 pb.gen,
    ← Finset.univ_sigma_univ, Finset.prod_sigma, ← Finset.prod_pow]

Premises used: Fintype.prod_equiv, algHomEquivSigma, PowerBasis.gen, Sigma.fst, Finset.prod_sigma, Finset.univ_sigma_univ, Finset.prod_pow, DFunLike.coe
-- Module: Mathlib.RingTheory.Norm.Basic
Goal:
K : Type u_4
L : Type u_5
F : Type u_6
inst : Field K
inst_1 : Field L
inst_2 : Field F
inst_3 : Algebra K L
inst_4 : Algebra K F
E : Type u_7
inst_5 : Field E
inst_6 : Algebra K E
inst_7 : Algebra L F
inst_8 : IsScalarTower K L F
inst_9 : IsAlgClosed E
inst_10 : Algebra.IsSeparable K F
inst_11 : FiniteDimensional K F
pb : PowerBasis K L
this_1 : FiniteDimensional L F
this_2 : Algebra.IsSeparable L F
this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
⊢ Eq.{u_7 + 1} (α := E)
    (∏ a : L →ₐ[K] E,
      ∏ s : F →ₐ[L] E,
        (Sigma.fst (β := fun (f : L →ₐ[K] E) ↦ F →ₐ[L] E) (Sigma.mk (β := fun (f : L →ₐ[K] E) ↦ F →ₐ[L] E) a s) :
            (a : L) → E)
          pb.gen)
    (∏ x : L →ₐ[K] E, HPow.hPow (α := E) ((x : (a : L) → E) pb.gen : E) (finrank L F))

Tactic:
Finset.prod_congr rfl fun σ _ => ?_

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.RingTheory.Norm.Basic
Goal:
K : Type u_4
L : Type u_5
F : Type u_6
inst : Field K
inst_1 : Field L
inst_2 : Field F
inst_3 : Algebra K L
inst_4 : Algebra K F
E : Type u_7
inst_5 : Field E
inst_6 : Algebra K E
inst_7 : Algebra L F
inst_8 : IsScalarTower K L F
inst_9 : IsAlgClosed E
inst_10 : Algebra.IsSeparable K F
inst_11 : FiniteDimensional K F
pb : PowerBasis K L
this_1 : FiniteDimensional L F
this_2 : Algebra.IsSeparable L F
this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
refine :
  ∀ (σ : L →ₐ[K] E),
    Membership.mem (γ := Finset (L →ₐ[K] E)) Finset.univ σ →
      ∏ s : F →ₐ[L] E,
          (Sigma.fst (β := fun (f : L →ₐ[K] E) ↦ F →ₐ[L] E) (Sigma.mk (β := fun (f : L →ₐ[K] E) ↦ F →ₐ[L] E) σ s) :
              (a : L) → E)
            pb.gen =
        HPow.hPow (α := E) ((σ : (a : L) → E) pb.gen : E) (finrank L F)
⊢ Eq.{u_7 + 1} (α := E)
    (∏ a : L →ₐ[K] E,
      ∏ s : F →ₐ[L] E,
        (Sigma.fst (β := fun (f : L →ₐ[K] E) ↦ F →ₐ[L] E) (Sigma.mk (β := fun (f : L →ₐ[K] E) ↦ F →ₐ[L] E) a s) :
            (a : L) → E)
          pb.gen)
    (∏ x : L →ₐ[K] E, HPow.hPow (α := E) ((x : (a : L) → E) pb.gen : E) (finrank L F))

Tactic:
refine Finset.prod_congr rfl fun σ _ => ?_

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.RingTheory.Norm.Basic
Goal:
K : Type u_4
L : Type u_5
F : Type u_6
inst : Field K
inst_1 : Field L
inst_2 : Field F
inst_3 : Algebra K L
inst_4 : Algebra K F
E : Type u_7
inst_5 : Field E
inst_6 : Algebra K E
inst_7 : Algebra L F
inst_8 : IsScalarTower K L F
inst_9 : IsAlgClosed E
inst_10 : Algebra.IsSeparable K F
inst_11 : FiniteDimensional K F
pb : PowerBasis K L
this_1 : FiniteDimensional L F
this_2 : Algebra.IsSeparable L F
this_3 : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
σ : L →ₐ[K] E
h : Membership.mem (γ := Finset (L →ₐ[K] E)) Finset.univ σ
this : Algebra L E := σ.toAlgebra
simp_rw :
  HPow.hPow (α := E) ((σ : (a : L) → E) pb.gen : E) (Finset.card (α := F →ₐ[L] E) Finset.univ) =
    HPow.hPow (α := E) ((σ : (a : L) → E) pb.gen : E) (finrank L F)
⊢ ∏ s : F →ₐ[L] E,
      (Sigma.fst (β := fun (f : L →ₐ[K] E) ↦ F →ₐ[L] E) (Sigma.mk (β := fun (f : L →ₐ[K] E) ↦ F →ₐ[L] E) σ s) :
          (a : L) → E)
        pb.gen =
    HPow.hPow (α := E) ((σ : (a : L) → E) pb.gen : E) (finrank L F)

Tactic:
simp_rw [Finset.prod_const]

Premises used: Finset.prod_const
-- Module: Mathlib.RingTheory.Norm.Basic
Goal:
K : Type u_4
L : Type u_5
F : Type u_6
inst : Field K
inst_1 : Field L
inst_2 : Field F
inst_3 : Algebra K L
inst_4 : Algebra K F
E : Type u_7
inst_5 : Field E
inst_6 : Algebra K E
inst_7 : Algebra L F
inst_8 : IsScalarTower K L F
inst_9 : IsAlgClosed E
inst_10 : Algebra.IsSeparable K F
inst_11 : FiniteDimensional K F
pb : PowerBasis K L
this_1 : FiniteDimensional L F
this_2 : Algebra.IsSeparable L F
this_3 : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
σ : L →ₐ[K] E
h : Membership.mem (γ := Finset (L →ₐ[K] E)) Finset.univ σ
this : Algebra L E := σ.toAlgebra
e_a : Finset.card (α := F →ₐ[L] E) Finset.univ = finrank L F
⊢ HPow.hPow (α := E) ((σ : (a : L) → E) pb.gen : E) (Finset.card (α := F →ₐ[L] E) Finset.univ) =
    HPow.hPow (α := E) ((σ : (a : L) → E) pb.gen : E) (finrank L F)

Tactic:
congr
-- Module: Mathlib.RingTheory.Norm.Basic
Goal:
K : Type u_4
L : Type u_5
F : Type u_6
inst : Field K
inst_1 : Field L
inst_2 : Field F
inst_3 : Algebra K L
inst_4 : Algebra K F
E : Type u_7
inst_5 : Field E
inst_6 : Algebra K E
inst_7 : Algebra L F
inst_8 : IsScalarTower K L F
inst_9 : IsAlgClosed E
inst_10 : Algebra.IsSeparable K F
inst_11 : FiniteDimensional K F
pb : PowerBasis K L
this_1 : FiniteDimensional L F
this_2 : Algebra.IsSeparable L F
this_3 : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
σ : L →ₐ[K] E
h : Membership.mem (γ := Finset (L →ₐ[K] E)) Finset.univ σ
this : Algebra L E := σ.toAlgebra
⊢ Finset.card (α := F →ₐ[L] E) Finset.univ = finrank L F

Tactic:
AlgHom.card L F E

Premises used: Fintype.card, AlgHom.card
-- Module: Mathlib.RingTheory.Norm.Basic
Goal:
K : Type u_4
L : Type u_5
F : Type u_6
inst : Field K
inst_1 : Field L
inst_2 : Field F
inst_3 : Algebra K L
inst_4 : Algebra K F
E : Type u_7
inst_5 : Field E
inst_6 : Algebra K E
inst_7 : Algebra L F
inst_8 : IsScalarTower K L F
inst_9 : IsAlgClosed E
inst_10 : Algebra.IsSeparable K F
inst_11 : FiniteDimensional K F
pb : PowerBasis K L
this_1 : FiniteDimensional L F
this_2 : Algebra.IsSeparable L F
this_3 : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
σ : L →ₐ[K] E
h : Membership.mem (γ := Finset (L →ₐ[K] E)) Finset.univ σ
this : Algebra L E := σ.toAlgebra
⊢ Finset.card (α := F →ₐ[L] E) Finset.univ = finrank L F

Tactic:
exact AlgHom.card L F E

Premises used: AlgHom.card
-- Module: Mathlib.RingTheory.Norm.Basic
Goal:
K : Type u_4
L : Type u_5
F : Type u_6
inst : Field K
inst_1 : Field L
inst_2 : Field F
inst_3 : Algebra K L
inst_4 : Algebra K F
E : Type u_7
inst_5 : Field E
inst_6 : Algebra K E
inst_7 : Algebra L F
inst_8 : IsScalarTower K L F
inst_9 : IsAlgClosed E
inst_10 : Algebra.IsSeparable K F
inst_11 : FiniteDimensional K F
pb : PowerBasis K L
this_1 : FiniteDimensional L F
this_2 : Algebra.IsSeparable L F
this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
σ : F →ₐ[K] E
⊢ Eq.{u_7 + 1} (α := E) ((σ : (a : F) → E) ((algebraMap L F : (a : L) → F) pb.gen : F) : E)
    ((Sigma.fst (β := fun (f : L →ₐ[K] E) ↦ F →ₐ[L] E)
            ((algHomEquivSigma : (a : F →ₐ[K] E) → (f : L →ₐ[K] E) × (F →ₐ[L] E)) σ) :
          (a : L) → E)
        pb.gen :
      E)

Tactic:
simp only [algHomEquivSigma, Equiv.coe_fn_mk, AlgHom.restrictDomain, AlgHom.comp_apply,
      IsScalarTower.coe_toAlgHom']

Premises used: IsScalarTower.coe_toAlgHom', algHomEquivSigma, AlgHom.comp_apply, Equiv.coe_fn_mk, AlgHom.restrictDomain
-- Module: Mathlib.RingTheory.Norm.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : Ring T
inst_4 : Algebra R T
e : S ≃ₐ[R] T
x : S
simp_rw :
  Eq.{u_1 + 1} (α := R)
    (((LinearMap.det.{u_3, u_1} (M := T) (A := R) : MonoidHom.{u_3, u_1} (T →ₗ[R] T) R) : (a : T →ₗ[R] T) → R)
        ((lmul R T : (a : T) → End R T) ((e : (a : S) → T) x : T) : End R T) :
      R)
    (((LinearMap.det.{u_3, u_1} (M := T) (A := R) : MonoidHom.{u_3, u_1} (T →ₗ[R] T) R) : (a : T →ₗ[R] T) → R)
        ((↑(↑e : S ≃ₗ[R] T) : S →ₗ[R] T) ∘ₗ (lmul R S : (a : S) → End R S) x ∘ₗ (↑(↑e : S ≃ₗ[R] T).symm : T →ₗ[R] S)) :
      R)
⊢ Eq.{u_1 + 1} (α := R) ((norm R : (a : T) → R) ((e : (a : S) → T) x : T) : R) ((norm R : (a : S) → R) x : R)

Tactic:
simp_rw [Algebra.norm_apply, ← LinearMap.det_conj _ e.toLinearEquiv]

Premises used: AlgEquiv.toLinearEquiv, Algebra.norm_apply, LinearMap.det_conj
-- Module: Mathlib.RingTheory.Norm.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : Ring T
inst_4 : Algebra R T
e : S ≃ₐ[R] T
x : S
h :
  (lmul R T : (a : T) → End R T) ((e : (a : S) → T) x : T) =
    (↑(↑e : S ≃ₗ[R] T) : S →ₗ[R] T) ∘ₗ (lmul R S : (a : S) → End R S) x ∘ₗ (↑(↑e : S ≃ₗ[R] T).symm : T →ₗ[R] S)
⊢ Eq.{u_1 + 1} (α := R)
    (((LinearMap.det.{u_3, u_1} (M := T) (A := R) : MonoidHom.{u_3, u_1} (T →ₗ[R] T) R) : (a : T →ₗ[R] T) → R)
        ((lmul R T : (a : T) → End R T) ((e : (a : S) → T) x : T) : End R T) :
      R)
    (((LinearMap.det.{u_3, u_1} (M := T) (A := R) : MonoidHom.{u_3, u_1} (T →ₗ[R] T) R) : (a : T →ₗ[R] T) → R)
        ((↑(↑e : S ≃ₗ[R] T) : S →ₗ[R] T) ∘ₗ (lmul R S : (a : S) → End R S) x ∘ₗ (↑(↑e : S ≃ₗ[R] T).symm : T →ₗ[R] S)) :
      R)

Tactic:
congr
-- Module: Mathlib.RingTheory.Norm.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : Ring T
inst_4 : Algebra R T
e : S ≃ₐ[R] T
x : S
h :
  ∀ (x_1 : T),
    Eq (α := T) ((((lmul R T : (a : T) → End R T) ((e : (a : S) → T) x : T) : End R T) : (a : T) → T) x_1 : T)
      (((↑(↑e : S ≃ₗ[R] T) : S →ₗ[R] T) ∘ₗ (lmul R S : (a : S) → End R S) x ∘ₗ (↑(↑e : S ≃ₗ[R] T).symm : T →ₗ[R] S) :
            (a : T) → T)
          x_1 :
        T)
⊢ (lmul R T : (a : T) → End R T) ((e : (a : S) → T) x : T) =
    (↑(↑e : S ≃ₗ[R] T) : S →ₗ[R] T) ∘ₗ (lmul R S : (a : S) → End R S) x ∘ₗ (↑(↑e : S ≃ₗ[R] T).symm : T →ₗ[R] S)

Tactic:
ext
-- Module: Mathlib.RingTheory.Norm.Basic
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : Ring T
inst_4 : Algebra R T
e : S ≃ₐ[R] T
x : S
x_1 : T
⊢ Eq (α := T) ((((lmul R T : (a : T) → End R T) ((e : (a : S) → T) x : T) : End R T) : (a : T) → T) x_1 : T)
    (((↑(↑e : S ≃ₗ[R] T) : S →ₗ[R] T) ∘ₗ (lmul R S : (a : S) → End R S) x ∘ₗ (↑(↑e : S ≃ₗ[R] T).symm : T →ₗ[R] S) :
          (a : T) → T)
        x_1 :
      T)

Tactic:
simp
-- Module: Mathlib.RingTheory.Norm.Basic
Goal:
A : Type u_8
B : Type u_9
C : Type u_10
inst : CommRing A
inst_1 : CommRing B
inst_2 : Ring C
inst_3 : Algebra A C
inst_4 : Algebra B C
e : A ≃+* B
he :
  Eq (α := A →+* C) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B C) (↑e : A →+* B))
    (algebraMap A C)
x : C
pos :
  ∀ (h : ∃ (s : Finset C), Nonempty (Basis (↥s) B C)),
    Eq.{u_9 + 1} (α := B) ((e : (a : A) → B) ((norm A : (a : C) → A) x : A) : B) ((norm B : (a : C) → B) x : B)
neg :
  ∀ (h : ¬∃ (s : Finset C), Nonempty (Basis (↥s) B C)),
    Eq.{u_9 + 1} (α := B) ((e : (a : A) → B) ((norm A : (a : C) → A) x : A) : B) ((norm B : (a : C) → B) x : B)
⊢ Eq.{u_9 + 1} (α := B) ((e : (a : A) → B) ((norm A : (a : C) → A) x : A) : B) ((norm B : (a : C) → B) x : B)

Tactic:
by_cases h : ∃ s : Finset C, Nonempty (Basis s B C)

Premises used: Finset
-- Module: Mathlib.RingTheory.Norm.Basic
Goal:
A : Type u_8
B : Type u_9
C : Type u_10
inst : CommRing A
inst_1 : CommRing B
inst_2 : Ring C
inst_3 : Algebra A C
inst_4 : Algebra B C
e : A ≃+* B
he :
  Eq (α := A →+* C) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B C) (↑e : A →+* B))
    (algebraMap A C)
x : C
h : ∃ (s : Finset C), Nonempty (Basis (↥s) B C)
pos :
  ∀ (s : Finset C) (b : Basis (↥s) B C),
    Eq.{u_9 + 1} (α := B) ((e : (a : A) → B) ((norm A : (a : C) → A) x : A) : B) ((norm B : (a : C) → B) x : B)
⊢ Eq.{u_9 + 1} (α := B) ((e : (a : A) → B) ((norm A : (a : C) → A) x : A) : B) ((norm B : (a : C) → B) x : B)

Tactic:
obtain ⟨s, ⟨b⟩⟩ := h
-- Module: Mathlib.RingTheory.Norm.Basic
Goal:
A : Type u_8
B : Type u_9
C : Type u_10
inst : CommRing A
inst_1 : CommRing B
inst_2 : Ring C
inst_3 : Algebra A C
inst_4 : Algebra B C
e : A ≃+* B
he :
  Eq (α := A →+* C) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B C) (↑e : A →+* B))
    (algebraMap A C)
x : C
s : Finset C
b : Basis (↥s) B C
this_1 : Algebra A B := RingHom.toAlgebra (↑e : A →+* B)
this : IsScalarTower A B C := ⋯
⊢ ∀ (c : B) (x : C), HSMul.hSMul.{u_8, u_10, u_10} (α := A) ((e.symm : (a : B) → A) c : A) x = c • x

Tactic:
simp [Algebra.smul_def, ← he]

Premises used: Algebra.smul_def
-- Module: Mathlib.RingTheory.Norm.Basic
Goal:
A : Type u_8
B : Type u_9
C : Type u_10
inst : CommRing A
inst_1 : CommRing B
inst_2 : Ring C
inst_3 : Algebra A C
inst_4 : Algebra B C
e : A ≃+* B
he :
  Eq (α := A →+* C) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B C) (↑e : A →+* B))
    (algebraMap A C)
x : C
s : Finset C
b : Basis (↥s) B C
this_1 : Algebra A B := RingHom.toAlgebra (↑e : A →+* B)
this : IsScalarTower A B C := ⋯
pos :
  Eq.{u_9 + 1} (α := B)
    (det.{u_9, u_10} (n := ↥s)
      ((e.mapMatrix : (a : Matrix (↥s) (↥s) A) → Matrix (↥s) (↥s) B)
        ((leftMulMatrix (b.mapCoeffs e.symm ⋯) : (a : C) → Matrix (↥s) (↥s) A) x)))
    (det.{u_9, u_10} (n := ↥s) ((leftMulMatrix b : (a : C) → Matrix (↥s) (↥s) B) x))
⊢ Eq.{u_9 + 1} (α := B) ((e : (a : A) → B) ((norm A : (a : C) → A) x : A) : B) ((norm B : (a : C) → B) x : B)

Tactic:
rw [Algebra.norm_eq_matrix_det b,
      Algebra.norm_eq_matrix_det (b.mapCoeffs e.symm (by simp [Algebra.smul_def, ← he])),
      e.map_det]

Premises used: Algebra.norm_eq_matrix_det, Module.Basis.mapCoeffs, RingEquiv.map_det, RingEquiv.symm
-- Module: Mathlib.RingTheory.Norm.Basic
Goal:
A : Type u_8
B : Type u_9
C : Type u_10
inst : CommRing A
inst_1 : CommRing B
inst_2 : Ring C
inst_3 : Algebra A C
inst_4 : Algebra B C
e : A ≃+* B
he :
  Eq (α := A →+* C) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B C) (↑e : A →+* B))
    (algebraMap A C)
x : C
s : Finset C
b : Basis (↥s) B C
this_1 : Algebra A B := RingHom.toAlgebra (↑e : A →+* B)
this : IsScalarTower A B C := ⋯
pos :
  Eq (α := Matrix.{u_10, u_10, u_9} (↥s) (↥s) B)
    ((e.mapMatrix : (a : Matrix (↥s) (↥s) A) → Matrix (↥s) (↥s) B)
        ((leftMulMatrix (b.mapCoeffs e.symm ⋯) : (a : C) → Matrix (↥s) (↥s) A) x) :
      Matrix.{u_10, u_10, u_9} (↥s) (↥s) B)
    ((leftMulMatrix b : (a : C) → Matrix (↥s) (↥s) B) x : Matrix.{u_10, u_10, u_9} (↥s) (↥s) B)
⊢ Eq.{u_9 + 1} (α := B)
    (det.{u_9, u_10} (n := ↥s)
      ((e.mapMatrix : (a : Matrix (↥s) (↥s) A) → Matrix (↥s) (↥s) B)
        ((leftMulMatrix (b.mapCoeffs e.symm ⋯) : (a : C) → Matrix (↥s) (↥s) A) x)))
    (det.{u_9, u_10} (n := ↥s) ((leftMulMatrix b : (a : C) → Matrix (↥s) (↥s) B) x))

Tactic:
congr
-- Module: Mathlib.RingTheory.Norm.Basic
Goal:
A : Type u_8
B : Type u_9
C : Type u_10
inst : CommRing A
inst_1 : CommRing B
inst_2 : Ring C
inst_3 : Algebra A C
inst_4 : Algebra B C
e : A ≃+* B
he :
  Eq (α := A →+* C) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B C) (↑e : A →+* B))
    (algebraMap A C)
x : C
s : Finset C
b : Basis (↥s) B C
this_1 : Algebra A B := RingHom.toAlgebra (↑e : A →+* B)
this : IsScalarTower A B C := ⋯
pos :
  ∀ (i j : ↥s),
    Eq.{u_9 + 1} (α := B)
      ((e.mapMatrix : (a : Matrix (↥s) (↥s) A) → Matrix (↥s) (↥s) B)
          ((leftMulMatrix (b.mapCoeffs e.symm ⋯) : (a : C) → Matrix (↥s) (↥s) A) x) i j :
        B)
      ((leftMulMatrix b : (a : C) → Matrix (↥s) (↥s) B) x i j : B)
⊢ Eq (α := Matrix.{u_10, u_10, u_9} (↥s) (↥s) B)
    ((e.mapMatrix : (a : Matrix (↥s) (↥s) A) → Matrix (↥s) (↥s) B)
        ((leftMulMatrix (b.mapCoeffs e.symm ⋯) : (a : C) → Matrix (↥s) (↥s) A) x) :
      Matrix.{u_10, u_10, u_9} (↥s) (↥s) B)
    ((leftMulMatrix b : (a : C) → Matrix (↥s) (↥s) B) x : Matrix.{u_10, u_10, u_9} (↥s) (↥s) B)

Tactic:
ext i j
-- Module: Mathlib.RingTheory.Norm.Basic
Goal:
A : Type u_8
B : Type u_9
C : Type u_10
inst : CommRing A
inst_1 : CommRing B
inst_2 : Ring C
inst_3 : Algebra A C
inst_4 : Algebra B C
e : A ≃+* B
he :
  Eq (α := A →+* C) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B C) (↑e : A →+* B))
    (algebraMap A C)
x : C
s : Finset C
b : Basis (↥s) B C
this_1 : Algebra A B := RingHom.toAlgebra (↑e : A →+* B)
this : IsScalarTower A B C := ⋯
i j : ↥s
⊢ Eq.{u_9 + 1} (α := B)
    ((e.mapMatrix : (a : Matrix (↥s) (↥s) A) → Matrix (↥s) (↥s) B)
        ((leftMulMatrix (b.mapCoeffs e.symm ⋯) : (a : C) → Matrix (↥s) (↥s) A) x) i j :
      B)
    ((leftMulMatrix b : (a : C) → Matrix (↥s) (↥s) B) x i j : B)

Tactic:
simp [leftMulMatrix_apply, LinearMap.toMatrix_apply]

Premises used: Algebra.leftMulMatrix_apply, LinearMap.toMatrix_apply
-- Module: Mathlib.RingTheory.Norm.Basic
Goal:
A : Type u_8
B : Type u_9
C : Type u_10
inst : CommRing A
inst_1 : CommRing B
inst_2 : Ring C
inst_3 : Algebra A C
inst_4 : Algebra B C
e : A ≃+* B
he :
  Eq (α := A →+* C) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B C) (↑e : A →+* B))
    (algebraMap A C)
x : C
h : ¬∃ (s : Finset C), Nonempty (Basis (↥s) B C)
neg : ¬∃ (s : Finset C), Nonempty (Basis (↥s) A C)
⊢ Eq.{u_9 + 1} (α := B) ((e : (a : A) → B) ((norm A : (a : C) → A) x : A) : B) ((norm B : (a : C) → B) x : B)

Tactic:
rw [norm_eq_one_of_not_exists_basis _ h, norm_eq_one_of_not_exists_basis, map_one]

Premises used: map_one, Algebra.norm_eq_one_of_not_exists_basis
-- Module: Mathlib.RingTheory.Norm.Basic
Goal:
A : Type u_8
B : Type u_9
C : Type u_10
inst : CommRing A
inst_1 : CommRing B
inst_2 : Ring C
inst_3 : Algebra A C
inst_4 : Algebra B C
e : A ≃+* B
he :
  Eq (α := A →+* C) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B C) (↑e : A →+* B))
    (algebraMap A C)
x : C
h : ¬∃ (s : Finset C), Nonempty (Basis (↥s) B C)
s : Finset C
b : Basis (↥s) A C
⊢ ∀ (c : A) (x : C), HSMul.hSMul.{u_9, u_10, u_10} (α := B) ((e : (a : A) → B) c : B) x = c • x

Tactic:
simp [Algebra.smul_def, ← he]

Premises used: Algebra.smul_def
-- Module: Mathlib.RingTheory.Norm.Basic
Goal:
A : Type u_8
B : Type u_9
C : Type u_10
inst : CommRing A
inst_1 : CommRing B
inst_2 : Ring C
inst_3 : Algebra A C
inst_4 : Algebra B C
e : A ≃+* B
he :
  Eq (α := A →+* C) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B C) (↑e : A →+* B))
    (algebraMap A C)
x : C
h : ¬∃ (s : Finset C), Nonempty (Basis (↥s) B C)
s : Finset C
b : Basis (↥s) A C
⊢ False

Tactic:
exact h ⟨s, ⟨b.mapCoeffs e (by simp [Algebra.smul_def, ← he])⟩⟩

Premises used: Module.Basis.mapCoeffs, Nonempty.intro, Exists.intro
-- Module: Mathlib.RingTheory.Norm.Basic
Goal:
A : Type u_8
B : Type u_9
C : Type u_10
inst : CommRing A
inst_1 : CommRing B
inst_2 : Ring C
inst_3 : Algebra A C
inst_4 : Algebra B C
e : A ≃+* B
he :
  Eq (α := A →+* C) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B C) (↑e : A →+* B))
    (algebraMap A C)
x : C
pos :
  ∀ (h : ∃ (s : Finset C), Nonempty (Basis (↥s) B C)),
    Eq.{u_9 + 1} (α := B) ((e : (a : A) → B) ((norm A : (a : C) → A) x : A) : B) ((norm B : (a : C) → B) x : B)
neg neg₁ :
  ∀ (h : ¬∃ (s : Finset C), Nonempty (Basis (↥s) B C)),
    Eq.{u_9 + 1} (α := B) ((e : (a : A) → B) ((norm A : (a : C) → A) x : A) : B) ((norm B : (a : C) → B) x : B)
neg₂ : ∀ (h : ¬∃ (s : Finset C), Nonempty (Basis (↥s) B C)), ¬∃ (s : Finset C), Nonempty (Basis (↥s) A C)
neg₃ : ∀ (h : ¬∃ (s : Finset C), Nonempty (Basis (↥s) B C)) (s : Finset C) (b : Basis (↥s) A C), False
⊢ Eq.{u_9 + 1} (α := B) ((e : (a : A) → B) ((norm A : (a : C) → A) x : A) : B) ((norm B : (a : C) → B) x : B)

Tactic:
classical
  by_cases h : ∃ s : Finset C, Nonempty (Basis s B C)
  · obtain ⟨s, ⟨b⟩⟩ := h
    letI : Algebra A B := RingHom.toAlgebra e
    letI : IsScalarTower A B C := IsScalarTower.of_algebraMap_eq' he.symm
    rw [Algebra.norm_eq_matrix_det b,
      Algebra.norm_eq_matrix_det (b.mapCoeffs e.symm (by simp [Algebra.smul_def, ← he])),
      e.map_det]
    congr
    ext i j
    simp [leftMulMatrix_apply, LinearMap.toMatrix_apply]
  rw [norm_eq_one_of_not_exists_basis _ h, norm_eq_one_of_not_exists_basis, map_one]
  intro ⟨s, ⟨b⟩⟩
  exact h ⟨s, ⟨b.mapCoeffs e (by simp [Algebra.smul_def, ← he])⟩⟩

Premises used: Finset, RingEquiv.map_det, map_one, Algebra.norm_eq_one_of_not_exists_basis, Algebra.leftMulMatrix_apply, LinearMap.toMatrix_apply