awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (goal)
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 := ⋯
⊢ 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))
have 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 sorry) : (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: congr
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (goal)
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 := ⋯
⊢ 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)
have 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 sorry) : (a : C) → Matrix (↥s) (↥s) A) x) i j :
      B)
    ((leftMulMatrix b : (a : C) → Matrix (↥s) (↥s) B) x i j : B)
Tactic: ext i j
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (goal)
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)
⊢ Eq.{u_9 + 1} (α := B) ((e : (a : A) → B) ((norm A : (a : C) → A) x : A) : B) ((norm B : (a : C) → B) x : B)
have neg : ¬∃ (s : Finset C), Nonempty (Basis (↥s) A C)
Tactic: rw [norm_eq_one_of_not_exists_basis _ h, norm_eq_one_of_not_exists_basis, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (goal)
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
⊢ Eq.{u_9 + 1} (α := B) ((e : (a : A) → B) ((norm A : (a : C) → A) x : A) : B) ((norm B : (a : C) → B) x : B)
have 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)
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])⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (goal)
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)
⊢ Eq.{u_9 + 1} (α := B) ((e : (a : A) → B) ((norm A : (a : C) → A) x : A) : B) ((norm B : (a : C) → B) x : B)
have 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)
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])⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (goal)
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)
⊢ Eq.{u_9 + 1} (α := B) ((e : (a : A) → B) ((norm A : (a : C) → A) x : A) : B) ((norm B : (a : C) → B) x : B)
have neg₂ : ∀ (h : ¬∃ (s : Finset C), Nonempty (Basis (↥s) B C)), ¬∃ (s : Finset C), Nonempty (Basis (↥s) A C)
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])⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (goal)
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)
⊢ Eq.{u_9 + 1} (α := B) ((e : (a : A) → B) ((norm A : (a : C) → A) x : A) : B) ((norm B : (a : C) → B) x : B)
have neg₃ : ∀ (h : ¬∃ (s : Finset C), Nonempty (Basis (↥s) B C)) (s : Finset C) (b : Basis (↥s) A C), False
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])⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (goal)
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₁)
⊢ 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₁)
have 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₂)
Tactic: letI := (RingHom.comp (e₂ : B₁ →+* B₂) (algebraMap A₁ B₁)).toAlgebra' ?_
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (goal)
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₁) x : A₁)
    ((e₁.symm : (a : A₂) → A₁) ((norm A₂ : (a : B₂) → A₂) ((e₂ : (a : B₁) → B₂) x : B₂) : A₂) : A₁)
have 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₁)
Tactic: rw [← Algebra.norm_eq_of_ringEquiv e₁ he, ← Algebra.norm_eq_of_algEquiv e']
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (goal)
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₂
⊢ 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₂)
have 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₁)
Tactic: apply e₂.symm.injective
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Defs (goal)
Goal:
R : Type u_1
inst : CommRing R
⊢ Eq (α := R →* R) (norm R) (MonoidHom.id R)
have h : ∀ (x : R), Eq (α := R) ((norm R : (a : R) → R) x : R) ((MonoidHom.id R : (a : R) → R) x : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Defs (goal)
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
⊢ Eq.{u_1 + 1} (α := R) ((norm R : (a : S) → R) x : R) (1 : R)
have 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 sorry))
        else 1 :
        (a : S →ₗ[R] S) → R)
      ((lmul R S : (a : S) → End R S) x : End R S) :
    R)
  (1 : R)
Tactic: rw [norm_apply, LinearMap.det]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Defs (goal)
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
⊢ 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)
have 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 sorry)) :
            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: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Defs (goal)
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)
⊢ 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)
have 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)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Defs (goal)
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)
have refine : (∃ (s : Finset S), Nonempty (Basis (↥s) R S)) → Module.Finite R S
Tactic: refine norm_eq_one_of_not_exists_basis _ (mt ?_ h) _
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Defs (goal)
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) ((norm R : (a : S) → R) s : R)
    (det.{u_1, w} (n := ι) ((leftMulMatrix b : (a : S) → Matrix ι ι R) s) : R)
have 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)))
Tactic: rw [norm_apply, ← LinearMap.det_toMatrix b, ← toMatrix_lmul_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Defs (goal)
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
⊢ (norm R : (a : S) → R) ((algebraMap R S : (a : R) → S) x : S) = x ^ Fintype.card ι
have haveI : ∀ (this : DecidableEq ι), (norm R : (a : S) → R) ((algebraMap R S : (a : R) → S) x : S) = x ^ Fintype.card ι
Tactic: haveI := Classical.decEq ι
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Defs (goal)
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 ι
⊢ (norm R : (a : S) → R) ((algebraMap R S : (a : R) → S) x : S) = x ^ Fintype.card ι
have 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 ι
Tactic: rw [norm_apply, ← det_toMatrix b, lmul_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Defs (goal)
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
⊢ (norm R : (a : S) → R) ((algebraMap R S : (a : R) → S) x : S) = x ^ finrank R S
have 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
Tactic: rw [norm_apply, lmul_algebraMap, det_lsmul]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Defs (goal)
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
⊢ (norm R : (a : S) → R) ((algebraMap R S : (a : R) → S) x : S) = x ^ finrank R S
have 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
Tactic: rw [norm_apply, lmul_algebraMap, det_lsmul]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Defs (goal)
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
⊢ (norm R : (a : S) → R) ((algebraMap R S : (a : R) → S) x : S) = x ^ finrank R S
have rw₂ : x ^ finrank R S = x ^ finrank R S
Tactic: rw [norm_apply, lmul_algebraMap, det_lsmul]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Defs (goal)
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 : ℕ
⊢ (norm R : (a : S) → R) (↑n : S) = HPow.hPow (α := R) (↑n : R) (finrank R S)
have rw : (norm R : (a : S) → R) ((algebraMap R S : (a : R) → S) (↑n : R) : S) = HPow.hPow (α := R) (↑n : R) (finrank R S)
Tactic: rw [← map_natCast (algebraMap R S), Algebra.norm_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Defs (goal)
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)
⊢ (norm R : (a : S) → R) (↑n : S) = HPow.hPow (α := R) (↑n : R) (finrank R S)
have rw₁ : HPow.hPow (α := R) (↑n : R) (finrank R S) = HPow.hPow (α := R) (↑n : R) (finrank R S)
Tactic: rw [← map_natCast (algebraMap R S), Algebra.norm_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.NormTrace (goal)
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
⊢ ∃ (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
have 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
Tactic: haveI : Fintype ι := inferInstance
-- Lean 4 proof step from Mathlib.RingTheory.NormTrace (goal)
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 ι
⊢ ∃ (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
have 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
Tactic: clear_value ι b
Cleared hypotheses: ι, b, this
-- Lean 4 proof step from Mathlib.RingTheory.NormTrace (goal)
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),
    (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
have 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
Tactic: simp_rw [Algebra.norm_eq_matrix_det b, Algebra.trace_eq_matrix_trace b]
-- Lean 4 proof step from Mathlib.RingTheory.NormTrace (goal)
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),
    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
have 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
Tactic: simp only [map_add, map_one, map_smul, Matrix.det_one_add_smul a]