awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.NonUnitalSubsemiring.Defs (goal)
Goal:
R : Type u
S : Type v
T : Type w
inst : NonUnitalNonAssocSemiring R
s : Set R
sg : Subsemigroup R
hg : (↑sg : Set R) = s
sa : AddSubmonoid R
ha : (↑sa : Set R) = s
⊢ ∀ {a b : R}, a ∈ s → b ∈ s → a * b ∈ s
have subst : ∀ (ha : (↑sa : Set R) = (↑sg : Set R)) {a b : R}, a ∈ (↑sg : Set R) → b ∈ (↑sg : Set R) → a * b ∈ (↑sg : Set R)
Tactic: subst hg
Cleared hypotheses: s, hg, ha
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
pb : PowerBasis R S
⊢ (norm R : (a : S) → R) pb.gen = HPow.hPow (α := R) (-1) pb.dim * coeff (minpoly R pb.gen) 0
have rw : det (n := Fin pb.dim)
    (((leftMulMatrix pb.basis : S →ₐ[R] Matrix (Fin pb.dim) (Fin pb.dim) R) :
        (a : S) → Matrix (Fin pb.dim) (Fin pb.dim) R)
      pb.gen) =
  HPow.hPow (α := R) (-1) pb.dim * coeff (minpoly R pb.gen) 0
Tactic: rw [norm_eq_matrix_det pb.basis, det_eq_sign_charpoly_coeff, charpoly_leftMulMatrix,
    Fintype.card_fin]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
pb : PowerBasis R S
rw :
  det (n := Fin pb.dim)
      (((leftMulMatrix pb.basis : S →ₐ[R] Matrix (Fin pb.dim) (Fin pb.dim) R) :
          (a : S) → Matrix (Fin pb.dim) (Fin pb.dim) R)
        pb.gen) =
    HPow.hPow (α := R) (-1) pb.dim * coeff (minpoly R pb.gen) 0
⊢ (norm R : (a : S) → R) pb.gen = HPow.hPow (α := R) (-1) pb.dim * coeff (minpoly R pb.gen) 0
have rw₁ : HPow.hPow (α := R) (-1) (Fintype.card (Fin pb.dim)) *
    coeff
      (charpoly (n := Fin pb.dim)
        (((leftMulMatrix pb.basis : S →ₐ[R] Matrix (Fin pb.dim) (Fin pb.dim) R) :
            (a : S) → Matrix (Fin pb.dim) (Fin pb.dim) R)
          pb.gen))
      0 =
  HPow.hPow (α := R) (-1) pb.dim * coeff (minpoly R pb.gen) 0
Tactic: rw [norm_eq_matrix_det pb.basis, det_eq_sign_charpoly_coeff, charpoly_leftMulMatrix,
    Fintype.card_fin]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
pb : PowerBasis R S
rw :
  det (n := Fin pb.dim)
      (((leftMulMatrix pb.basis : S →ₐ[R] Matrix (Fin pb.dim) (Fin pb.dim) R) :
          (a : S) → Matrix (Fin pb.dim) (Fin pb.dim) R)
        pb.gen) =
    HPow.hPow (α := R) (-1) pb.dim * coeff (minpoly R pb.gen) 0
rw₁ :
  HPow.hPow (α := R) (-1) (Fintype.card (Fin pb.dim)) *
      coeff
        (charpoly (n := Fin pb.dim)
          (((leftMulMatrix pb.basis : S →ₐ[R] Matrix (Fin pb.dim) (Fin pb.dim) R) :
              (a : S) → Matrix (Fin pb.dim) (Fin pb.dim) R)
            pb.gen))
        0 =
    HPow.hPow (α := R) (-1) pb.dim * coeff (minpoly R pb.gen) 0
⊢ (norm R : (a : S) → R) pb.gen = HPow.hPow (α := R) (-1) pb.dim * coeff (minpoly R pb.gen) 0
have rw₂ : HPow.hPow (α := R) (-1) (Fintype.card (Fin pb.dim)) * coeff (minpoly R pb.gen) 0 =
  HPow.hPow (α := R) (-1) pb.dim * coeff (minpoly R pb.gen) 0
Tactic: rw [norm_eq_matrix_det pb.basis, det_eq_sign_charpoly_coeff, charpoly_leftMulMatrix,
    Fintype.card_fin]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
pb : PowerBasis R S
rw :
  det (n := Fin pb.dim)
      (((leftMulMatrix pb.basis : S →ₐ[R] Matrix (Fin pb.dim) (Fin pb.dim) R) :
          (a : S) → Matrix (Fin pb.dim) (Fin pb.dim) R)
        pb.gen) =
    HPow.hPow (α := R) (-1) pb.dim * coeff (minpoly R pb.gen) 0
rw₁ :
  HPow.hPow (α := R) (-1) (Fintype.card (Fin pb.dim)) *
      coeff
        (charpoly (n := Fin pb.dim)
          (((leftMulMatrix pb.basis : S →ₐ[R] Matrix (Fin pb.dim) (Fin pb.dim) R) :
              (a : S) → Matrix (Fin pb.dim) (Fin pb.dim) R)
            pb.gen))
        0 =
    HPow.hPow (α := R) (-1) pb.dim * coeff (minpoly R pb.gen) 0
rw₂ :
  HPow.hPow (α := R) (-1) (Fintype.card (Fin pb.dim)) * coeff (minpoly R pb.gen) 0 =
    HPow.hPow (α := R) (-1) pb.dim * coeff (minpoly R pb.gen) 0
⊢ (norm R : (a : S) → R) pb.gen = HPow.hPow (α := R) (-1) pb.dim * coeff (minpoly R pb.gen) 0
have rw₃ : HPow.hPow (α := R) (-1) pb.dim * coeff (minpoly R pb.gen) 0 =
  HPow.hPow (α := R) (-1) pb.dim * coeff (minpoly R pb.gen) 0
Tactic: rw [norm_eq_matrix_det pb.basis, det_eq_sign_charpoly_coeff, charpoly_leftMulMatrix,
    Fintype.card_fin]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (hypothesis)
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
hf : Splits (Polynomial.map (algebraMap R F) (minpoly R pb.gen))
⊢ (algebraMap R F : (a : R) → F) ((norm R : (a : S) → R) pb.gen : R) = (aroots (minpoly R pb.gen) F).prod
have this : Nontrivial R
Tactic: haveI := Module.nontrivial R F
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (hypothesis)
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
hf : Splits (Polynomial.map (algebraMap R F) (minpoly R pb.gen))
this : Nontrivial R
⊢ (algebraMap R F : (a : R) → F) ((norm R : (a : S) → R) pb.gen : R) = (aroots (minpoly R pb.gen) F).prod
have this₁ : Monic (minpoly R pb.gen)
Tactic: have := minpoly.monic pb.isIntegral_gen
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (goal)
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
hf : Splits (Polynomial.map (algebraMap R F) (minpoly R pb.gen))
this_1 : Nontrivial R
this : Monic (minpoly R pb.gen)
⊢ (algebraMap R F : (a : R) → F) ((norm R : (a : S) → R) pb.gen : R) = (aroots (minpoly R pb.gen) F).prod
have rw : HMul.hMul (α := F) (β := F) ((algebraMap R F : (a : R) → F) (-1) : F) (-1 : F) ^ natDegree (minpoly R pb.gen) *
    (roots (Polynomial.map (algebraMap R F) (minpoly R pb.gen))).prod =
  (aroots (minpoly R pb.gen) F).prod
Tactic: rw [PowerBasis.norm_gen_eq_coeff_zero_minpoly, ← pb.natDegree_minpoly, map_mul,
    ← coeff_map,
    hf.coeff_zero_eq_prod_roots_of_monic (this.map _),
    this.natDegree_map, map_pow, ← mul_assoc, ← mul_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : Nontrivial S
inst_4 : Free R S
inst_5 : Module.Finite R S
⊢ Eq.{u_1 + 1} (α := R) ((norm R : (a : S) → R) 0 : R) (0 : R)
have a : Nontrivial R
Tactic: nontriviality
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : Nontrivial S
inst_4 : Free R S
inst_5 : Module.Finite R S
h : Nontrivial R
⊢ Eq.{u_1 + 1} (α := R) ((norm R : (a : S) → R) 0 : R) (0 : R)
have rw : Eq.{u_1 + 1} (α := 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) 0 : End R S) :
    R)
  (0 : R)
Tactic: rw [norm_apply, coe_lmul_eq_mul, map_zero, LinearMap.det_zero' (Module.Free.chooseBasis R S)]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : Nontrivial S
inst_4 : Free R S
inst_5 : Module.Finite R S
h : Nontrivial R
rw :
  Eq.{u_1 + 1} (α := 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) 0 : End R S) :
      R)
    (0 : R)
⊢ Eq.{u_1 + 1} (α := R) ((norm R : (a : S) → R) 0 : R) (0 : R)
have rw₁ : Eq.{u_1 + 1} (α := 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)
      ((mul R S : (a : S) → S →ₗ[R] S) 0 : S →ₗ[R] S) :
    R)
  (0 : R)
Tactic: rw [norm_apply, coe_lmul_eq_mul, map_zero, LinearMap.det_zero' (Module.Free.chooseBasis R S)]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : Nontrivial S
inst_4 : Free R S
inst_5 : Module.Finite R S
h : Nontrivial R
rw :
  Eq.{u_1 + 1} (α := 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) 0 : End R S) :
      R)
    (0 : R)
rw₁ :
  Eq.{u_1 + 1} (α := 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)
        ((mul R S : (a : S) → S →ₗ[R] S) 0 : S →ₗ[R] S) :
      R)
    (0 : R)
⊢ Eq.{u_1 + 1} (α := R) ((norm R : (a : S) → R) 0 : R) (0 : R)
have rw₂ : Eq.{u_1 + 1} (α := 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) 0 : R)
  (0 : R)
Tactic: rw [norm_apply, coe_lmul_eq_mul, map_zero, LinearMap.det_zero' (Module.Free.chooseBasis R S)]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : Nontrivial S
inst_4 : Free R S
inst_5 : Module.Finite R S
h : Nontrivial R
rw :
  Eq.{u_1 + 1} (α := 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) 0 : End R S) :
      R)
    (0 : R)
rw₁ :
  Eq.{u_1 + 1} (α := 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)
        ((mul R S : (a : S) → S →ₗ[R] S) 0 : S →ₗ[R] S) :
      R)
    (0 : R)
rw₂ :
  Eq.{u_1 + 1} (α := 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) 0 : R)
    (0 : R)
⊢ Eq.{u_1 + 1} (α := R) ((norm R : (a : S) → R) 0 : R) (0 : R)
have rw₃ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [norm_apply, coe_lmul_eq_mul, map_zero, LinearMap.det_zero' (Module.Free.chooseBasis R S)]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : Free R S
inst_6 : Module.Finite R S
x : S
⊢ Eq.{u_1 + 1} (α := R) ((norm R : (a : S) → R) x : R) (0 : R) ↔ x = 0
have mp : Eq.{u_1 + 1} (α := R) ((norm R : (a : S) → R) x : R) (0 : R) → x = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : Free R S
inst_6 : Module.Finite R S
x : S
mp : Eq.{u_1 + 1} (α := R) ((norm R : (a : S) → R) x : R) (0 : R) → x = 0
⊢ Eq.{u_1 + 1} (α := R) ((norm R : (a : S) → R) x : R) (0 : R) ↔ x = 0
have mpr : x = 0 → Eq.{u_1 + 1} (α := R) ((norm R : (a : S) → R) x : R) (0 : R)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : Free R S
inst_6 : Module.Finite R S
x : S
b : Basis (Free.ChooseBasisIndex R S) R S := Free.chooseBasis R S
decEq : DecidableEq (Free.ChooseBasisIndex R S) := Classical.decEq (Free.ChooseBasisIndex R S)
⊢ Eq.{u_1 + 1} (α := R) ((norm R : (a : S) → R) x : R) (0 : R) → x = 0
have mp : (∃ (v : Free.ChooseBasisIndex R S → R),
    v ≠ 0 ∧
      Eq (α := Free.ChooseBasisIndex R S → R)
        ((leftMulMatrix b : (a : S) → Matrix (Free.ChooseBasisIndex R S) (Free.ChooseBasisIndex R S) R) x *ᵥ v) 0) →
  x = 0
Tactic: rw [norm_eq_matrix_det b, ← Matrix.exists_mulVec_eq_zero_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : Free R S
inst_6 : Module.Finite R S
x : S
b : Basis (Free.ChooseBasisIndex R S) R S := Free.chooseBasis R S
decEq : DecidableEq (Free.ChooseBasisIndex R S) := Classical.decEq (Free.ChooseBasisIndex R S)
v : Free.ChooseBasisIndex R S → R
v_ne : v ≠ 0
hv :
  Eq (α := Free.ChooseBasisIndex R S → R)
    ((leftMulMatrix b : (a : S) → Matrix (Free.ChooseBasisIndex R S) (Free.ChooseBasisIndex R S) R) x *ᵥ v) 0
⊢ x = 0
have hv₁ : Eq (α := Free.ChooseBasisIndex R S → R)
  (⇑((b.repr : (a : S) → Free.ChooseBasisIndex R S →₀ R)
          (x *
            ∑ i : Free.ChooseBasisIndex R S,
              HSMul.hSMul (β := S) (v i) ((b : (a : Free.ChooseBasisIndex R S) → S) i : S)) :
        Finsupp.{u_2, u_1} (Free.ChooseBasisIndex R S) R) :
    (a : Free.ChooseBasisIndex R S) → R)
  0
Tactic: rw [← b.equivFun.apply_symm_apply v, b.equivFun_symm_apply, b.equivFun_apply,
      leftMulMatrix_mulVec_repr] at hv
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : Free R S
inst_6 : Module.Finite R S
x : S
b : Basis (Free.ChooseBasisIndex R S) R S := Free.chooseBasis R S
decEq : DecidableEq (Free.ChooseBasisIndex R S) := Classical.decEq (Free.ChooseBasisIndex R S)
v : Free.ChooseBasisIndex R S → R
v_ne : v ≠ 0
hv :
  Eq (α := Free.ChooseBasisIndex R S → R)
    (⇑((b.repr : (a : S) → Free.ChooseBasisIndex R S →₀ R)
            (x *
              ∑ i : Free.ChooseBasisIndex R S,
                HSMul.hSMul (β := S) (v i) ((b : (a : Free.ChooseBasisIndex R S) → S) i : S)) :
          Finsupp.{u_2, u_1} (Free.ChooseBasisIndex R S) R) :
      (a : Free.ChooseBasisIndex R S) → R)
    0
⊢ x = 0
have mp : ∀ (i : Free.ChooseBasisIndex R S),
  Eq.{u_1 + 1} (α := R)
    ((((b.repr : (a : S) → Free.ChooseBasisIndex R S →₀ R)
              (x *
                ∑ i : Free.ChooseBasisIndex R S,
                  HSMul.hSMul (β := S) (v i) ((b : (a : Free.ChooseBasisIndex R S) → S) i : S)) :
            Finsupp.{u_2, u_1} (Free.ChooseBasisIndex R S) R) :
          (a : Free.ChooseBasisIndex R S) → R)
        i :
      R)
    (((b.repr : (a : S) → Free.ChooseBasisIndex R S →₀ R) 0 : (a : Free.ChooseBasisIndex R S) → R) i : R)
Tactic: refine (mul_eq_zero.mp (b.ext_elem fun i => ?_)).resolve_right (show ∑ i, v i • b i ≠ 0 from ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : Free R S
inst_6 : Module.Finite R S
x : S
b : Basis (Free.ChooseBasisIndex R S) R S := Free.chooseBasis R S
decEq : DecidableEq (Free.ChooseBasisIndex R S) := Classical.decEq (Free.ChooseBasisIndex R S)
v : Free.ChooseBasisIndex R S → R
v_ne : v ≠ 0
hv :
  Eq (α := Free.ChooseBasisIndex R S → R)
    (⇑((b.repr : (a : S) → Free.ChooseBasisIndex R S →₀ R)
            (x *
              ∑ i : Free.ChooseBasisIndex R S,
                HSMul.hSMul (β := S) (v i) ((b : (a : Free.ChooseBasisIndex R S) → S) i : S)) :
          Finsupp.{u_2, u_1} (Free.ChooseBasisIndex R S) R) :
      (a : Free.ChooseBasisIndex R S) → R)
    0
mp :
  ∀ (i : Free.ChooseBasisIndex R S),
    Eq.{u_1 + 1} (α := R)
      ((((b.repr : (a : S) → Free.ChooseBasisIndex R S →₀ R)
                (x *
                  ∑ i : Free.ChooseBasisIndex R S,
                    HSMul.hSMul (β := S) (v i) ((b : (a : Free.ChooseBasisIndex R S) → S) i : S)) :
              Finsupp.{u_2, u_1} (Free.ChooseBasisIndex R S) R) :
            (a : Free.ChooseBasisIndex R S) → R)
          i :
        R)
      (((b.repr : (a : S) → Free.ChooseBasisIndex R S →₀ R) 0 : (a : Free.ChooseBasisIndex R S) → R) i : R)
⊢ x = 0
have mp₁ : Ne.{u_2 + 1} (α := S)
  (∑ i : Free.ChooseBasisIndex R S, HSMul.hSMul (β := S) (v i) ((b : (a : Free.ChooseBasisIndex R S) → S) i : S)) 0
Tactic: refine (mul_eq_zero.mp (b.ext_elem fun i => ?_)).resolve_right (show ∑ i, v i • b i ≠ 0 from ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : Free R S
inst_6 : Module.Finite R S
x : S
b : Basis (Free.ChooseBasisIndex R S) R S := Free.chooseBasis R S
decEq : DecidableEq (Free.ChooseBasisIndex R S) := Classical.decEq (Free.ChooseBasisIndex R S)
v : Free.ChooseBasisIndex R S → R
v_ne : v ≠ 0
hv :
  Eq (α := Free.ChooseBasisIndex R S → R)
    (⇑((b.repr : (a : S) → Free.ChooseBasisIndex R S →₀ R)
            (x *
              ∑ i : Free.ChooseBasisIndex R S,
                HSMul.hSMul (β := S) (v i) ((b : (a : Free.ChooseBasisIndex R S) → S) i : S)) :
          Finsupp.{u_2, u_1} (Free.ChooseBasisIndex R S) R) :
      (a : Free.ChooseBasisIndex R S) → R)
    0
⊢ Ne.{u_2 + 1} (α := S)
    (∑ i : Free.ChooseBasisIndex R S, HSMul.hSMul (β := S) (v i) ((b : (a : Free.ChooseBasisIndex R S) → S) i : S)) 0
have mp : ∀
  (sum_eq :
    Eq.{u_2 + 1} (α := S)
      (∑ i : Free.ChooseBasisIndex R S, HSMul.hSMul (β := S) (v i) ((b : (a : Free.ChooseBasisIndex R S) → S) i : S))
      0),
  v = 0
Tactic: contrapose v_ne with sum_eq
Cleared hypotheses: v_ne
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : Free R S
inst_6 : Module.Finite R S
x : S
b : Basis (Free.ChooseBasisIndex R S) R S := Free.chooseBasis R S
decEq : DecidableEq (Free.ChooseBasisIndex R S) := Classical.decEq (Free.ChooseBasisIndex R S)
v : Free.ChooseBasisIndex R S → R
hv :
  Eq (α := Free.ChooseBasisIndex R S → R)
    (⇑((b.repr : (a : S) → Free.ChooseBasisIndex R S →₀ R)
            (x *
              ∑ i : Free.ChooseBasisIndex R S,
                HSMul.hSMul (β := S) (v i) ((b : (a : Free.ChooseBasisIndex R S) → S) i : S)) :
          Finsupp.{u_2, u_1} (Free.ChooseBasisIndex R S) R) :
      (a : Free.ChooseBasisIndex R S) → R)
    0
sum_eq :
  Eq.{u_2 + 1} (α := S)
    (∑ i : Free.ChooseBasisIndex R S, HSMul.hSMul (β := S) (v i) ((b : (a : Free.ChooseBasisIndex R S) → S) i : S)) 0
⊢ v = 0
have mp : Eq.{u_2 + 1} (α := S) ((b.equivFun.symm : (a : Free.ChooseBasisIndex R S → R) → S) v : S)
  ((b.equivFun.symm : (a : Free.ChooseBasisIndex R S → R) → S) 0 : S)
Tactic: apply b.equivFun.symm.injective
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : Free R S
inst_6 : Module.Finite R S
x : S
b : Basis (Free.ChooseBasisIndex R S) R S := Free.chooseBasis R S
decEq : DecidableEq (Free.ChooseBasisIndex R S) := Classical.decEq (Free.ChooseBasisIndex R S)
v : Free.ChooseBasisIndex R S → R
hv :
  Eq (α := Free.ChooseBasisIndex R S → R)
    (⇑((b.repr : (a : S) → Free.ChooseBasisIndex R S →₀ R)
            (x *
              ∑ i : Free.ChooseBasisIndex R S,
                HSMul.hSMul (β := S) (v i) ((b : (a : Free.ChooseBasisIndex R S) → S) i : S)) :
          Finsupp.{u_2, u_1} (Free.ChooseBasisIndex R S) R) :
      (a : Free.ChooseBasisIndex R S) → R)
    0
sum_eq :
  Eq.{u_2 + 1} (α := S)
    (∑ i : Free.ChooseBasisIndex R S, HSMul.hSMul (β := S) (v i) ((b : (a : Free.ChooseBasisIndex R S) → S) i : S)) 0
⊢ Eq.{u_2 + 1} (α := S) ((b.equivFun.symm : (a : Free.ChooseBasisIndex R S → R) → S) v : S)
    ((b.equivFun.symm : (a : Free.ChooseBasisIndex R S → R) → S) 0 : S)
have mp : Eq.{u_2 + 1} (α := S)
  (∑ i : Free.ChooseBasisIndex R S, HSMul.hSMul (β := S) (v i) ((b : (a : Free.ChooseBasisIndex R S) → S) i : S) : S)
  ((b.equivFun.symm : (a : Free.ChooseBasisIndex R S → R) → S) 0 : S)
Tactic: rw [b.equivFun_symm_apply, sum_eq, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : Free R S
inst_6 : Module.Finite R S
x : S
b : Basis (Free.ChooseBasisIndex R S) R S := Free.chooseBasis R S
decEq : DecidableEq (Free.ChooseBasisIndex R S) := Classical.decEq (Free.ChooseBasisIndex R S)
v : Free.ChooseBasisIndex R S → R
hv :
  Eq (α := Free.ChooseBasisIndex R S → R)
    (⇑((b.repr : (a : S) → Free.ChooseBasisIndex R S →₀ R)
            (x *
              ∑ i : Free.ChooseBasisIndex R S,
                HSMul.hSMul (β := S) (v i) ((b : (a : Free.ChooseBasisIndex R S) → S) i : S)) :
          Finsupp.{u_2, u_1} (Free.ChooseBasisIndex R S) R) :
      (a : Free.ChooseBasisIndex R S) → R)
    0
sum_eq :
  Eq.{u_2 + 1} (α := S)
    (∑ i : Free.ChooseBasisIndex R S, HSMul.hSMul (β := S) (v i) ((b : (a : Free.ChooseBasisIndex R S) → S) i : S)) 0
mp :
  Eq.{u_2 + 1} (α := S)
    (∑ i : Free.ChooseBasisIndex R S, HSMul.hSMul (β := S) (v i) ((b : (a : Free.ChooseBasisIndex R S) → S) i : S) : S)
    ((b.equivFun.symm : (a : Free.ChooseBasisIndex R S → R) → S) 0 : S)
⊢ Eq.{u_2 + 1} (α := S) ((b.equivFun.symm : (a : Free.ChooseBasisIndex R S → R) → S) v : S)
    ((b.equivFun.symm : (a : Free.ChooseBasisIndex R S → R) → S) 0 : S)
have mp₁ : Eq.{u_2 + 1} (α := S) (0 : S) ((b.equivFun.symm : (a : Free.ChooseBasisIndex R S → R) → S) 0 : S)
Tactic: rw [b.equivFun_symm_apply, sum_eq, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : Free R S
inst_6 : Module.Finite R S
x : S
b : Basis (Free.ChooseBasisIndex R S) R S := Free.chooseBasis R S
decEq : DecidableEq (Free.ChooseBasisIndex R S) := Classical.decEq (Free.ChooseBasisIndex R S)
v : Free.ChooseBasisIndex R S → R
hv :
  Eq (α := Free.ChooseBasisIndex R S → R)
    (⇑((b.repr : (a : S) → Free.ChooseBasisIndex R S →₀ R)
            (x *
              ∑ i : Free.ChooseBasisIndex R S,
                HSMul.hSMul (β := S) (v i) ((b : (a : Free.ChooseBasisIndex R S) → S) i : S)) :
          Finsupp.{u_2, u_1} (Free.ChooseBasisIndex R S) R) :
      (a : Free.ChooseBasisIndex R S) → R)
    0
sum_eq :
  Eq.{u_2 + 1} (α := S)
    (∑ i : Free.ChooseBasisIndex R S, HSMul.hSMul (β := S) (v i) ((b : (a : Free.ChooseBasisIndex R S) → S) i : S)) 0
mp :
  Eq.{u_2 + 1} (α := S)
    (∑ i : Free.ChooseBasisIndex R S, HSMul.hSMul (β := S) (v i) ((b : (a : Free.ChooseBasisIndex R S) → S) i : S) : S)
    ((b.equivFun.symm : (a : Free.ChooseBasisIndex R S → R) → S) 0 : S)
mp₁ : Eq.{u_2 + 1} (α := S) (0 : S) ((b.equivFun.symm : (a : Free.ChooseBasisIndex R S → R) → S) 0 : S)
⊢ Eq.{u_2 + 1} (α := S) ((b.equivFun.symm : (a : Free.ChooseBasisIndex R S → R) → S) v : S)
    ((b.equivFun.symm : (a : Free.ChooseBasisIndex R S → R) → S) 0 : S)
have mp₂ : Eq.{u_2 + 1} (α := S) 0 0
Tactic: rw [b.equivFun_symm_apply, sum_eq, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (hypothesis)
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 : Finite ι
inst_4 : IsDomain R
inst_5 : IsDomain S
b : Basis ι R S
x : S
⊢ Eq.{u_1 + 1} (α := R) ((norm R : (a : S) → R) x : R) (0 : R) ↔ x = 0
have this : Free R S
Tactic: haveI : Module.Free R S := Module.Free.of_basis b
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (hypothesis)
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 : Finite ι
inst_4 : IsDomain R
inst_5 : IsDomain S
b : Basis ι R S
x : S
this : Free R S
⊢ Eq.{u_1 + 1} (α := R) ((norm R : (a : S) → R) x : R) (0 : R) ↔ x = 0
have this₁ : Module.Finite R S
Tactic: haveI : Module.Finite R S := Module.Finite.of_basis b
-- Lean 4 proof step from Mathlib.RingTheory.Norm.Basic (goal)
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Module.Finite K L
x : L
⊢ Eq.{u_4 + 1} (α := K) ((norm K : (a : L) → K) x⁻¹ : K) (((norm K : (a : L) → K) x)⁻¹ : K)
have pos : ∀ (hx : x = 0), Eq.{u_4 + 1} (α := K) ((norm K : (a : L) → K) x⁻¹ : K) (((norm K : (a : L) → K) x)⁻¹ : K)
Tactic: by_cases hx : x = 0