awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs
Goal:
R : Type u_1
S : Type u_2
inst : Mul R
inst_1 : HasDistribNeg R
inst_2 : SetLike S R
inst_3 : MulMemClass S R
s : S
x y : R
hx : x ∈ s
hy : -y ∈ s
⊢ -(x * y) ∈ s

Tactic:
simpa using mul_mem hx hy

Premises used: MulMemClass.mul_mem
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs
Goal:
R : Type u_1
S : Type u_2
inst : Mul R
inst_1 : HasDistribNeg R
inst_2 : SetLike S R
inst_3 : MulMemClass S R
s : S
x y z : R
hx : x ∈ s
hy : -y ∈ s
hz : z ∈ s
⊢ x * -y * z ∈ s

Tactic:
aesop
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs
Goal:
R_1 : Type u
S_1 : Type v
T : Type w
inst : NonUnitalNonAssocSemiring R_1
S : Type u_1
R : Type u
inst_1 : NonUnitalNonAssocSemiring R
inst_2 : SetLike S R
h : NonUnitalSubsemiringClass S R
⊢ MulMemClass S R

Tactic:
{ h with }

Premises used: NonUnitalSubsemiringClass.mul_mem, MulMemClass.mk
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs
Goal:
R : Type u
S : Type v
T : Type w
inst : NonUnitalNonAssocSemiring R
inst_1 : SetLike S R
inst_2 : NonUnitalSubsemiringClass S R
s : S
⊢ ∀ (x y : ↥s), (↑(x + y) : R) = (↑x : R) + (↑y : R)

Tactic:
simp
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs
Goal:
R_1 : Type u
S : Type v
T : Type w
inst : NonUnitalNonAssocSemiring R_1
inst_1 : SetLike S R_1
inst_2 : NonUnitalSubsemiringClass S R_1
s : S
R : Type u_1
inst_3 : NonUnitalNonAssocCommSemiring R
inst_4 : SetLike S R
inst_5 : NonUnitalSubsemiringClass S R
⊢ ∀ (x y : ↥s), (↑(x + y) : R) = (↑x : R) + (↑y : R)

Tactic:
simp
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs
Goal:
R : Type u
S : Type v
T : Type w
inst : NonUnitalNonAssocSemiring R
inst_1 : SetLike S R
inst_2 : NonUnitalSubsemiringClass S R
s : S
inst_3 : NoZeroDivisors R
⊢ NoZeroDivisors.{u} ↥s

Tactic:
Subtype.coe_injective.noZeroDivisors Subtype.val rfl fun _ _ => rfl

Premises used: Subtype.coe_injective, Function.Injective.noZeroDivisors, Subtype.val, rfl
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocSemiring R
inst_1 : SetLike S R
inst_2 : NonUnitalSubsemiringClass S R
s : S
x : ↥s
⊢ (subtype s : (a : ↥s) → R) x = (↑x : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocSemiring R
inst_1 : SetLike S R
inst_2 : NonUnitalSubsemiringClass S R
s : S
⊢ Function.Injective (α := ↥s) (β := R) (⇑(subtype s) : (a : ↥s) → R)

Tactic:
Subtype.coe_injective

Premises used: Subtype.coe_injective
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs
Goal:
R : Type u
S : Type v
inst : NonUnitalNonAssocSemiring R
inst_1 : SetLike S R
inst_2 : NonUnitalSubsemiringClass S R
s : S
⊢ Eq (α := (a : ↥s) → R) (⇑(subtype s) : (a : ↥s) → R) (Subtype.val (p := fun (x : R) ↦ x ∈ s))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs
Goal:
R_1 : Type u
S : Type v
T : Type w
inst : NonUnitalNonAssocSemiring R_1
inst_1 : SetLike S R_1
inst_2 : NonUnitalSubsemiringClass S R_1
s : S
R : Type u_1
inst_3 : NonUnitalSemiring R
inst_4 : SetLike S R
inst_5 : NonUnitalSubsemiringClass S R
⊢ ∀ (x y : ↥s), (↑(x + y) : R) = (↑x : R) + (↑y : R)

Tactic:
simp
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs
Goal:
R_1 : Type u
S : Type v
T : Type w
inst : NonUnitalNonAssocSemiring R_1
inst_1 : SetLike S R_1
inst_2 : NonUnitalSubsemiringClass S R_1
s : S
R : Type u_1
inst_3 : NonUnitalCommSemiring R
inst_4 : SetLike S R
inst_5 : NonUnitalSubsemiringClass S R
⊢ ∀ (x y : ↥s), (↑(x + y) : R) = (↑x : R) + (↑y : R)

Tactic:
simp
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
x t : NonUnitalSubsemiring R
s : AddSubmonoid R
hs : ∀ {a b : R}, a ∈ s.carrier → b ∈ s.carrier → a * b ∈ s.carrier
⊢ { toAddSubmonoid := s, mul_mem' := @hs : NonUnitalSubsemiring R }.toAddSubmonoid = t.toAddSubmonoid →
    { toAddSubmonoid := s, mul_mem' := @hs : NonUnitalSubsemiring R } = t

Tactic:
congr!
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
s t : NonUnitalSubsemiring R
⊢ s.toAddSubmonoid = t.toAddSubmonoid ↔ s = t

Tactic:
toAddSubmonoid_injective.eq_iff

Premises used: Function.Injective.eq_iff, NonUnitalSubsemiring.toAddSubmonoid_injective
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
s : NonUnitalSubsemiring R
x : R
⊢ x ∈ s.carrier ↔ x ∈ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
S T : NonUnitalSubsemiring R
h : ∀ (x : R), x ∈ S ↔ x ∈ T
⊢ S = T

Tactic:
SetLike.ext h

Premises used: SetLike.ext
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
S : NonUnitalSubsemiring R
s : Set R
hs : s = (↑S : Set R)
⊢ (↑(S.copy s hs) : Set R) = s

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
S : NonUnitalSubsemiring R
s : Set R
hs : s = (↑S : Set R)
⊢ S.copy s hs = S

Tactic:
SetLike.coe_injective hs

Premises used: SetLike.coe_injective
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs
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
subst : ∀ (hg : (↑sg : Set R) = (↑sa : Set R)) {a b : R}, a ∈ (↑sa : Set R) → b ∈ (↑sa : Set R) → a + b ∈ (↑sa : Set R)
⊢ ∀ {a b : R}, a ∈ s → b ∈ s → a + b ∈ s

Tactic:
subst ha
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs
Goal:
R : Type u
S : Type v
T : Type w
inst : NonUnitalNonAssocSemiring R
sg : Subsemigroup R
sa : AddSubmonoid R
hg : (↑sg : Set R) = (↑sa : Set R)
a b : R
⊢ a ∈ (↑sa : Set R) → b ∈ (↑sa : Set R) → a + b ∈ (↑sa : Set R)

Tactic:
sa.add_mem

Premises used: AddSubmonoid.add_mem
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs
Goal:
R : Type u
S : Type v
T : Type w
inst : NonUnitalNonAssocSemiring R
sg : Subsemigroup R
sa : AddSubmonoid R
hg : (↑sg : Set R) = (↑sa : Set R)
⊢ ∀ {a b : R}, a ∈ (↑sa : Set R) → b ∈ (↑sa : Set R) → a + b ∈ (↑sa : Set R)

Tactic:
exact sa.add_mem

Premises used: AddSubmonoid.add_mem
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs
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
subst : ∀ (hg : (↑sg : Set R) = (↑sa : Set R)), 0 ∈ (↑sa : Set R)
⊢ 0 ∈ s

Tactic:
subst ha
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs
Goal:
R : Type u
S : Type v
T : Type w
inst : NonUnitalNonAssocSemiring R
sg : Subsemigroup R
sa : AddSubmonoid R
hg : (↑sg : Set R) = (↑sa : Set R)
⊢ 0 ∈ (↑sa : Set R)

Tactic:
sa.zero_mem

Premises used: AddSubmonoid.zero_mem
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs
Goal:
R : Type u
S : Type v
T : Type w
inst : NonUnitalNonAssocSemiring R
sg : Subsemigroup R
sa : AddSubmonoid R
hg : (↑sg : Set R) = (↑sa : Set R)
⊢ 0 ∈ (↑sa : Set R)

Tactic:
exact sa.zero_mem

Premises used: AddSubmonoid.zero_mem
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs
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
subst : ∀ (ha : (↑sa : Set R) = (↑sg : Set R)) {a b : R}, a ∈ (↑sg : Set R) → b ∈ (↑sg : Set R) → a * b ∈ (↑sg : Set R)
⊢ ∀ {a b : R}, a ∈ s → b ∈ s → a * b ∈ s

Tactic:
subst hg
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs
Goal:
R : Type u
S : Type v
T : Type w
inst : NonUnitalNonAssocSemiring R
sg : Subsemigroup R
sa : AddSubmonoid R
ha : (↑sa : Set R) = (↑sg : Set R)
a b : R
⊢ a ∈ (↑sg : Set R) → b ∈ (↑sg : Set R) → a * b ∈ (↑sg : Set R)

Tactic:
sg.mul_mem

Premises used: Subsemigroup.mul_mem
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs
Goal:
R : Type u
S : Type v
T : Type w
inst : NonUnitalNonAssocSemiring R
sg : Subsemigroup R
sa : AddSubmonoid R
ha : (↑sa : Set R) = (↑sg : Set R)
⊢ ∀ {a b : R}, a ∈ (↑sg : Set R) → b ∈ (↑sg : Set R) → a * b ∈ (↑sg : Set R)

Tactic:
exact sg.mul_mem

Premises used: Subsemigroup.mul_mem
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
s : Set R
sg : Subsemigroup R
hg : (↑sg : Set R) = s
sa : AddSubmonoid R
ha : (↑sa : Set R) = s
⊢ (↑(NonUnitalSubsemiring.mk' s sg hg sa ha) : Set R) = s

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
s : Set R
sg : Subsemigroup R
hg : (↑sg : Set R) = s
sa : AddSubmonoid R
ha : (↑sa : Set R) = s
x : R
⊢ x ∈ NonUnitalSubsemiring.mk' s sg hg sa ha ↔ x ∈ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
s : Set R
sg : Subsemigroup R
hg : (↑sg : Set R) = s
sa : AddSubmonoid R
ha : (↑sa : Set R) = s
⊢ (NonUnitalSubsemiring.mk' s sg hg sa ha).toSubsemigroup = sg

Tactic:
SetLike.coe_injective hg.symm

Premises used: SetLike.coe_injective, Eq.symm
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
s : Set R
sg : Subsemigroup R
hg : (↑sg : Set R) = s
sa : AddSubmonoid R
ha : (↑sa : Set R) = s
⊢ (NonUnitalSubsemiring.mk' s sg hg sa ha).toAddSubmonoid = sa

Tactic:
SetLike.coe_injective ha.symm

Premises used: SetLike.coe_injective, Eq.symm
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
s : NonUnitalSubsemiring R
⊢ Eq.{u + 1} (α := R) (↑0 : R) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
s : NonUnitalSubsemiring R
x y : ↥s
⊢ (↑(x + y) : R) = (↑x : R) + (↑y : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
s : NonUnitalSubsemiring R
x y : ↥s
⊢ (↑(x * y) : R) = (↑x : R) * (↑y : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
s : NonUnitalSubsemiring R
x : R
⊢ x ∈ s.toSubsemigroup ↔ x ∈ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
s : NonUnitalSubsemiring R
⊢ (↑s.toSubsemigroup : Set R) = (↑s : Set R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
s : NonUnitalSubsemiring R
x : R
⊢ x ∈ s.toAddSubmonoid ↔ x ∈ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
s : NonUnitalSubsemiring R
⊢ (↑s.toAddSubmonoid : Set R) = (↑s : Set R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
x : R
⊢ Membership.mem (γ := NonUnitalSubsemiring R) ⊤ x

Tactic:
Set.mem_univ x

Premises used: Set.Mem, Set.univ, setOf, Set.mem_univ
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
⊢ (↑⊤ : Set R) = Set.univ

Tactic:
rfl

Premises used: Set.univ, setOf, rfl
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
⊢ Eq.{u + 1} (α := AddSubmonoid R) (toAddSubmonoid ⊤) ⊤

Tactic:
rfl

Premises used: Set.univ, setOf, rfl
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
S : NonUnitalSubsemiring R
⊢ S.toAddSubmonoid = ⊤ ↔ S = ⊤

Tactic:
simp [← SetLike.coe_set_eq]

Premises used: SetLike.coe_set_eq
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs
Goal:
R : Type u
S : Type v
T : Type w
inst : NonUnitalNonAssocSemiring R
a b : R
h : Membership.mem (γ := Set R) {0} a
h_1 : Membership.mem (γ := Set R) {0} b
⊢ Membership.mem (γ := Set R) {0} (a + b)

Tactic:
simp_all
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs
Goal:
R : Type u
S : Type v
T : Type w
inst : NonUnitalNonAssocSemiring R
a b : R
h : Membership.mem (γ := Set R) {0} a
h_1 : Membership.mem (γ := Set R) {0} b
⊢ Membership.mem (γ := Set R) {0} (a * b)

Tactic:
simp_all
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
⊢ (↑⊥ : Set R) = {0}

Tactic:
rfl

Premises used: setOf, Set.singleton, rfl
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
x : R
⊢ Membership.mem (γ := NonUnitalSubsemiring R) ⊥ x ↔ x = 0

Tactic:
Set.mem_singleton_iff

Premises used: Set.Mem, setOf, Set.mem_singleton_iff, Set.singleton
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
p p' : NonUnitalSubsemiring R
⊢ (↑(p ⊓ p') : Set R) = (↑p : Set R) ∩ (↑p' : Set R)

Tactic:
rfl

Premises used: setOf, Set.inter, rfl
-- Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs
Goal:
R : Type u
inst : NonUnitalNonAssocSemiring R
p p' : NonUnitalSubsemiring R
x : R
⊢ x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p'

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.inter
-- 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
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
rw₃ 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
⊢ (norm R : (a : S) → 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]

Premises used: Algebra.norm_eq_matrix_det, Fintype.card_fin, charpoly_leftMulMatrix, PowerBasis.basis, Matrix.det_eq_sign_charpoly_coeff
-- 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
hf : Splits (Polynomial.map (algebraMap R F) (minpoly R pb.gen))
⊢ Nontrivial R

Tactic:
haveI := Module.nontrivial R F
-- 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
hf : Splits (Polynomial.map (algebraMap R F) (minpoly R pb.gen))
this : Nontrivial R
⊢ Monic (minpoly R pb.gen)

Tactic:
have := minpoly.monic pb.isIntegral_gen
-- 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
hf : Splits (Polynomial.map (algebraMap R F) (minpoly R pb.gen))
this_1 : Nontrivial R
this : Monic (minpoly R pb.gen)
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
⊢ (algebraMap R F : (a : R) → F) ((norm R : (a : S) → R) pb.gen : R) = (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]

Premises used: Algebra.PowerBasis.norm_gen_eq_coeff_zero_minpoly, Polynomial.coeff_map, mul_assoc, Polynomial.Splits.coeff_zero_eq_prod_roots_of_monic, map_pow, map_mul, Polynomial.Monic.natDegree_map, Polynomial.Monic.map, mul_pow, PowerBasis.natDegree_minpoly
-- 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
hf : Splits (Polynomial.map (algebraMap R F) (minpoly R pb.gen))
this_1 : Nontrivial R
this : Monic (minpoly R pb.gen)
⊢ 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:
simp only [map_neg, map_one, neg_mul, neg_neg, one_pow, one_mul]

Premises used: one_pow, neg_neg, map_neg, map_one, neg_mul, one_mul
-- 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
inst_3 : Nontrivial S
inst_4 : Free R S
inst_5 : Module.Finite R S
⊢ Nontrivial R

Tactic:
nontriviality
-- 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
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)
rw₃ rw₄ : Eq.{u_1 + 1} (α := R) 0 0
⊢ Eq.{u_1 + 1} (α := R) ((norm R : (a : S) → R) 0 : R) (0 : R)

Tactic:
rw [norm_apply, coe_lmul_eq_mul, map_zero, LinearMap.det_zero' (Module.Free.chooseBasis R S)]

Premises used: map_zero, Algebra.norm_apply, LinearMap.det_zero', Algebra.coe_lmul_eq_mul, Module.Free.chooseBasis
-- 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
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
mpr : x = 0 → Eq.{u_1 + 1} (α := R) ((norm R : (a : S) → R) x : R) (0 : R)
⊢ Eq.{u_1 + 1} (α := R) ((norm R : (a : S) → R) x : R) (0 : R) ↔ x = 0

Tactic:
constructor
-- 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
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : Free R S
inst_6 : Module.Finite R S
⊢ Eq.{u_1 + 1} (α := R) ((norm R : (a : S) → R) 0 : R) (0 : R)

Tactic:
norm_zero

Premises used: Algebra.norm_zero
-- 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
inst_3 : IsDomain R
inst_4 : IsDomain S
inst_5 : Free R S
inst_6 : Module.Finite R S
⊢ Eq.{u_1 + 1} (α := R) ((norm R : (a : S) → R) 0 : R) (0 : R)

Tactic:
exact norm_zero

Premises used: Algebra.norm_zero
-- 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
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)
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
⊢ Eq.{u_1 + 1} (α := R) ((norm R : (a : S) → R) x : R) (0 : R) → x = 0

Tactic:
rw [norm_eq_matrix_det b, ← Matrix.exists_mulVec_eq_zero_iff]

Premises used: Algebra.norm_eq_matrix_det, Matrix.exists_mulVec_eq_zero_iff
-- 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
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
⊢ 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

Premises used: Module.Basis.equivFun_symm_apply, Module.Basis.equivFun_apply, LinearEquiv.apply_symm_apply, Algebra.leftMulMatrix_mulVec_repr, Module.Basis.equivFun
-- 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
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

Tactic:
(mul_eq_zero.mp (b.ext_elem fun i => ?_)).resolve_right (show ∑ i, v i • b i ≠ 0 from ?_)

Premises used: Module.Basis.ext_elem, mul_eq_zero, Iff.mp, Or.resolve_right