awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
n : ℕ
f : M →ₗ[R] M →ₗ[R] M [⋀^Fin n]→ₗ[R] N
v : Fin (n + 2) → M
⊢ Eq.{u_4 + 1} (α := N)
    (∑ x : Fin (n + 1),
      ∑ x_1 ∈ Finset.Ici x,
        (HPow.hPow (α := ℤ) (-1) (↑x : ℕ) •
            HSMul.hSMul (β := N) (HPow.hPow (α := ℤ) (-1) (↑x_1 : ℕ))
              ((((((f : (a : M) → M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) (v x.castSucc) : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) :
                          (a : M) → M [⋀^Fin n]→ₗ[R] N)
                        (x.castSucc.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v x_1) :
                      M [⋀^Fin n]→ₗ[R] N) :
                    (a : Fin n → M) → N)
                  (x_1.removeNth (α := fun (i : Fin (n + 1)) ↦ M)
                    (x.castSucc.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v)) :
                N) +
          HPow.hPow (α := ℤ) (-1) ((↑x_1 : ℕ) + 1) •
            HSMul.hSMul (β := N) (HPow.hPow (α := ℤ) (-1) (↑x : ℕ))
              ((((((f : (a : M) → M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) (v x_1.succ) : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) :
                          (a : M) → M [⋀^Fin n]→ₗ[R] N)
                        (x_1.succ.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v x) :
                      M [⋀^Fin n]→ₗ[R] N) :
                    (a : Fin n → M) → N)
                  (x.removeNth (α := fun (i : Fin (n + 1)) ↦ M)
                    (x_1.succ.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v)) :
                N)))
    (∑ i : Fin (n + 1),
      ∑ j ∈ Finset.Ici i,
        HPow.hPow (α := ℤ) (-1) ((↑i : ℕ) + (↑j : ℕ)) •
          HSub.hSub (α := N) (β := N)
            ((((((f : (a : M) → M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) (v i.castSucc) : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) :
                        (a : M) → M [⋀^Fin n]→ₗ[R] N)
                      (v j.succ) :
                    M [⋀^Fin n]→ₗ[R] N) :
                  (a : Fin n → M) → N)
                (j.removeNth (α := fun (i : Fin (n + 1)) ↦ M)
                  (i.castSucc.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v)) :
              N)
            ((((((f : (a : M) → M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) (v j.succ) : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) :
                        (a : M) → M [⋀^Fin n]→ₗ[R] N)
                      (v i.castSucc) :
                    M [⋀^Fin n]→ₗ[R] N) :
                  (a : Fin n → M) → N)
                (j.removeNth (α := fun (i : Fin (n + 1)) ↦ M)
                  (i.castSucc.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v)) :
              N))

Tactic:
Fintype.sum_congr _ _ fun i ↦ Finset.sum_congr rfl fun j hj ↦ ?_

Premises used: Fintype.sum_congr, Finset.sum_congr, rfl
-- Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
n : ℕ
f : M →ₗ[R] M →ₗ[R] M [⋀^Fin n]→ₗ[R] N
v : Fin (n + 2) → M
i j : Fin (n + 1)
hj : j ∈ Finset.Ici i
⊢ i ≤ j

Tactic:
rw [Finset.mem_Ici] at hj

Premises used: Finset.mem_Ici
-- Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
n : ℕ
f : M →ₗ[R] M →ₗ[R] M [⋀^Fin n]→ₗ[R] N
v : Fin (n + 2) → M
i j : Fin (n + 1)
hj : i ≤ j
⊢ i.castSucc.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v j = v j.succ

Tactic:
simp [Fin.removeNth_apply, Fin.succAbove_of_le_castSucc, hj]

Premises used: Fin.succAbove_of_le_castSucc, Fin.removeNth_apply
-- Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
n : ℕ
f : M →ₗ[R] M →ₗ[R] M [⋀^Fin n]→ₗ[R] N
v : Fin (n + 2) → M
i j : Fin (n + 1)
hj : i ≤ j
⊢ i.castSucc.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v j = v j.succ

Tactic:
have H₁ : i.castSucc.removeNth v j = v j.succ := by
    simp [Fin.removeNth_apply, Fin.succAbove_of_le_castSucc, hj]
-- Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
n : ℕ
f : M →ₗ[R] M →ₗ[R] M [⋀^Fin n]→ₗ[R] N
v : Fin (n + 2) → M
i j : Fin (n + 1)
hj : i ≤ j
H₁ : i.castSucc.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v j = v j.succ
⊢ j.succ.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v i = v i.castSucc

Tactic:
simp [Fin.removeNth_apply, Fin.succAbove_of_castSucc_lt, hj]

Premises used: Fin.removeNth_apply, Fin.succAbove_of_castSucc_lt
-- Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
n : ℕ
f : M →ₗ[R] M →ₗ[R] M [⋀^Fin n]→ₗ[R] N
v : Fin (n + 2) → M
i j : Fin (n + 1)
hj : i ≤ j
H₁ : i.castSucc.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v j = v j.succ
⊢ j.succ.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v i = v i.castSucc

Tactic:
have H₂ : j.succ.removeNth v i = v i.castSucc := by
    simp [Fin.removeNth_apply, Fin.succAbove_of_castSucc_lt, hj]
-- Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
n : ℕ
f : M →ₗ[R] M →ₗ[R] M [⋀^Fin n]→ₗ[R] N
v : Fin (n + 2) → M
i j : Fin (n + 1)
hj : i ≤ j
H₁ : i.castSucc.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v j = v j.succ
H₂ : j.succ.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v i = v i.castSucc
e_a :
  i.removeNth (α := fun (i : Fin (n + 1)) ↦ M) (j.succ.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v) =
    j.removeNth (α := fun (i : Fin (n + 1)) ↦ M) (i.castSucc.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v)
⊢ HPow.hPow (α := ℤ) (-1) (↑i : ℕ) •
        HSMul.hSMul (β := N) (HPow.hPow (α := ℤ) (-1) (↑j : ℕ))
          ((((((f : (a : M) → M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) (v i.castSucc) : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) :
                      (a : M) → M [⋀^Fin n]→ₗ[R] N)
                    (v j.succ) :
                  M [⋀^Fin n]→ₗ[R] N) :
                (a : Fin n → M) → N)
              (j.removeNth (α := fun (i : Fin (n + 1)) ↦ M)
                (i.castSucc.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v)) :
            N) -
      HPow.hPow (α := ℤ) (-1) (↑i : ℕ) •
        HSMul.hSMul (β := N) (HPow.hPow (α := ℤ) (-1) (↑j : ℕ))
          ((((((f : (a : M) → M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) (v j.succ) : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) :
                      (a : M) → M [⋀^Fin n]→ₗ[R] N)
                    (v i.castSucc) :
                  M [⋀^Fin n]→ₗ[R] N) :
                (a : Fin n → M) → N)
              (i.removeNth (α := fun (i : Fin (n + 1)) ↦ M) (j.succ.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v)) :
            N) =
    HPow.hPow (α := ℤ) (-1) (↑i : ℕ) •
        HSMul.hSMul (β := N) (HPow.hPow (α := ℤ) (-1) (↑j : ℕ))
          ((((((f : (a : M) → M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) (v i.castSucc) : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) :
                      (a : M) → M [⋀^Fin n]→ₗ[R] N)
                    (v j.succ) :
                  M [⋀^Fin n]→ₗ[R] N) :
                (a : Fin n → M) → N)
              (j.removeNth (α := fun (i : Fin (n + 1)) ↦ M)
                (i.castSucc.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v)) :
            N) -
      HPow.hPow (α := ℤ) (-1) (↑i : ℕ) •
        HSMul.hSMul (β := N) (HPow.hPow (α := ℤ) (-1) (↑j : ℕ))
          ((((((f : (a : M) → M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) (v j.succ) : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) :
                      (a : M) → M [⋀^Fin n]→ₗ[R] N)
                    (v i.castSucc) :
                  M [⋀^Fin n]→ₗ[R] N) :
                (a : Fin n → M) → N)
              (j.removeNth (α := fun (i : Fin (n + 1)) ↦ M)
                (i.castSucc.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v)) :
            N)

Tactic:
congr 4
-- Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
n : ℕ
f : M →ₗ[R] M →ₗ[R] M [⋀^Fin n]→ₗ[R] N
v : Fin (n + 2) → M
i j : Fin (n + 1)
hj : i ≤ j
H₁ : i.castSucc.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v j = v j.succ
H₂ : j.succ.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v i = v i.castSucc
e_a :
  (i.predAbove j.succ).removeNth (α := fun (i : Fin (n + 1)) ↦ M)
      ((j.succ.succAbove i).removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v) =
    j.removeNth (α := fun (i : Fin (n + 1)) ↦ M) (i.castSucc.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v)
⊢ i.removeNth (α := fun (i : Fin (n + 1)) ↦ M) (j.succ.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v) =
    j.removeNth (α := fun (i : Fin (n + 1)) ↦ M) (i.castSucc.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v)

Tactic:
rw [removeNth_removeNth_eq_swap]

Premises used: Fin.removeNth_removeNth_eq_swap
-- Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
n : ℕ
f : M →ₗ[R] M →ₗ[R] M [⋀^Fin n]→ₗ[R] N
v : Fin (n + 2) → M
i j : Fin (n + 1)
hj : i ≤ j
H₁ : i.castSucc.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v j = v j.succ
H₂ : j.succ.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v i = v i.castSucc
⊢ (i.predAbove j.succ).removeNth (α := fun (i : Fin (n + 1)) ↦ M)
      ((j.succ.succAbove i).removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v) =
    j.removeNth (α := fun (i : Fin (n + 1)) ↦ M) (i.castSucc.removeNth (α := fun (i : Fin (n + 1 + 1)) ↦ M) v)

Tactic:
simp [Fin.predAbove, hj, Fin.succAbove]

Premises used: Fin.succAbove, Fin.predAbove
-- Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
n : ℕ
f : M →ₗ[R] M →ₗ[R] M [⋀^Fin n]→ₗ[R] N
hf :
  ∀ (x y : M),
    Eq (α := M [⋀^Fin n]→ₗ[R] N)
      ((((f : (a : M) → M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) x : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) : (a : M) → M [⋀^Fin n]→ₗ[R] N) y :
        M [⋀^Fin n]→ₗ[R] N)
      ((((f : (a : M) → M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) y : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) : (a : M) → M [⋀^Fin n]→ₗ[R] N) x :
        M [⋀^Fin n]→ₗ[R] N)
H :
  ∀ (v : Fin (n + 1 + 1) → M),
    Eq.{u_4 + 1} (α := N) ((alternatizeUncurryFin (alternatizeUncurryFinLM ∘ₗ f) : (a : Fin (n + 1 + 1) → M) → N) v : N)
      ((0 : (a : Fin (n + 1 + 1) → M) → N) v : N)
⊢ alternatizeUncurryFin (alternatizeUncurryFinLM ∘ₗ f) = 0

Tactic:
ext v
-- Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
n : ℕ
f : M →ₗ[R] M →ₗ[R] M [⋀^Fin n]→ₗ[R] N
hf :
  ∀ (x y : M),
    Eq (α := M [⋀^Fin n]→ₗ[R] N)
      ((((f : (a : M) → M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) x : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) : (a : M) → M [⋀^Fin n]→ₗ[R] N) y :
        M [⋀^Fin n]→ₗ[R] N)
      ((((f : (a : M) → M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) y : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) : (a : M) → M [⋀^Fin n]→ₗ[R] N) x :
        M [⋀^Fin n]→ₗ[R] N)
v : Fin (n + 1 + 1) → M
⊢ Eq.{u_4 + 1} (α := N) ((alternatizeUncurryFin (alternatizeUncurryFinLM ∘ₗ f) : (a : Fin (n + 1 + 1) → M) → N) v : N)
    ((0 : (a : Fin (n + 1 + 1) → M) → N) v : N)

Tactic:
simp [alternatizeUncurryFin_alternatizeUncurryFinLM_comp_apply, hf (v <| .castSucc _)]

Premises used: AlternatingMap.alternatizeUncurryFin_alternatizeUncurryFinLM_comp_apply, Fin.castSucc
-- Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
a : A
p : R[X]
⊢ Membership.mem (γ := Ideal R[X]) (annIdeal R a) p ↔ Eq.{u_2 + 1} (α := A) ((aeval a : (a : R[X]) → A) p : A) (0 : A)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage, Set.singleton
-- Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
⊢ Eq (α := 𝕜[X]) (annIdealGenerator 𝕜 a) 0 ↔ Eq (α := Ideal 𝕜[X]) (annIdeal 𝕜 a) ⊥

Tactic:
simp only [annIdealGenerator, mul_eq_zero, IsPrincipal.eq_bot_iff_generator_eq_zero,
    Polynomial.C_eq_zero, inv_eq_zero, Polynomial.leadingCoeff_eq_zero, or_self_iff]

Premises used: inv_eq_zero, Polynomial.C_eq_zero, or_self_iff, mul_eq_zero, Polynomial.annIdealGenerator, Submodule.IsPrincipal.eq_bot_iff_generator_eq_zero, Polynomial.leadingCoeff_eq_zero
-- Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
pos :
  ∀ (h : Eq (α := 𝕜[X]) (annIdealGenerator 𝕜 a) 0),
    Eq (α := Ideal 𝕜[X]) (Ideal.span {annIdealGenerator 𝕜 a}) (annIdeal 𝕜 a)
neg :
  ∀ (h : ¬Eq (α := 𝕜[X]) (annIdealGenerator 𝕜 a) 0),
    Eq (α := Ideal 𝕜[X]) (Ideal.span {annIdealGenerator 𝕜 a}) (annIdeal 𝕜 a)
⊢ Eq (α := Ideal 𝕜[X]) (Ideal.span {annIdealGenerator 𝕜 a}) (annIdeal 𝕜 a)

Tactic:
by_cases h : annIdealGenerator 𝕜 a = 0

Premises used: Polynomial.annIdealGenerator
-- Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
h : Eq (α := 𝕜[X]) (annIdealGenerator 𝕜 a) 0
pos : Eq (α := Ideal 𝕜[X]) (Ideal.span {0}) (annIdeal 𝕜 a)
pos₁ : Eq (α := Ideal 𝕜[X]) (Ideal.span {0}) ⊥
pos₂ : Eq.{u_1 + 1} (α := Ideal 𝕜[X]) (Ideal.span 0) ⊥
pos₃ pos₄ : Eq.{u_1 + 1} (α := Ideal 𝕜[X]) ⊥ ⊥
⊢ Eq (α := Ideal 𝕜[X]) (Ideal.span {annIdealGenerator 𝕜 a}) (annIdeal 𝕜 a)

Tactic:
rw [h, annIdealGenerator_eq_zero_iff.mp h, Set.singleton_zero, Ideal.span_zero]

Premises used: Ideal.span_zero, Iff.mp, Polynomial.annIdealGenerator_eq_zero_iff, Set.singleton_zero
-- Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
h : ¬Eq (α := 𝕜[X]) (annIdealGenerator 𝕜 a) 0
neg : IsUnit (M := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) (leadingCoeff (IsPrincipal.generator (annIdeal 𝕜 a)))⁻¹ : 𝕜[X])
⊢ Eq (α := Ideal 𝕜[X]) (Ideal.span {annIdealGenerator 𝕜 a}) (annIdeal 𝕜 a)

Tactic:
rw [annIdealGenerator, Ideal.span_singleton_mul_right_unit, Ideal.span_singleton_generator]

Premises used: Ideal.span_singleton_mul_right_unit, Ideal.span_singleton_generator, Polynomial.annIdealGenerator
-- Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
h : ¬Eq (α := 𝕜[X]) (annIdealGenerator 𝕜 a) 0
neg : IsUnit (leadingCoeff (IsPrincipal.generator (annIdeal 𝕜 a)))⁻¹
⊢ IsUnit (M := 𝕜[X]) ((C : (a : 𝕜) → 𝕜[X]) (leadingCoeff (IsPrincipal.generator (annIdeal 𝕜 a)))⁻¹ : 𝕜[X])

Tactic:
apply Polynomial.isUnit_C.mpr

Premises used: Iff.mpr, Polynomial.isUnit_C
-- Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
h : ¬Eq (α := 𝕜[X]) (annIdealGenerator 𝕜 a) 0
neg : (leadingCoeff (IsPrincipal.generator (annIdeal 𝕜 a)))⁻¹ ≠ 0
⊢ IsUnit (leadingCoeff (IsPrincipal.generator (annIdeal 𝕜 a)))⁻¹

Tactic:
apply IsUnit.mk0

Premises used: IsUnit.mk0
-- Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
h : ¬Eq (α := 𝕜[X]) (annIdealGenerator 𝕜 a) 0
neg : ¬leadingCoeff (IsPrincipal.generator (annIdeal 𝕜 a)) = 0
⊢ (leadingCoeff (IsPrincipal.generator (annIdeal 𝕜 a)))⁻¹ ≠ 0

Tactic:
apply inv_eq_zero.not.mpr

Premises used: Iff.mpr, inv_eq_zero, Iff.not
-- Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
h : ¬Eq (α := 𝕜[X]) (annIdealGenerator 𝕜 a) 0
neg : ¬Eq (α := 𝕜[X]) (IsPrincipal.generator (annIdeal 𝕜 a)) 0
⊢ ¬leadingCoeff (IsPrincipal.generator (annIdeal 𝕜 a)) = 0

Tactic:
apply Polynomial.leadingCoeff_eq_zero.not.mpr

Premises used: Iff.mpr, Iff.not, Polynomial.leadingCoeff_eq_zero
-- Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
h : ¬Eq (α := 𝕜[X]) (annIdealGenerator 𝕜 a) 0
⊢ ¬Eq (α := 𝕜[X]) (IsPrincipal.generator (annIdeal 𝕜 a)) 0

Tactic:
apply (mul_ne_zero_iff.mp h).1

Premises used: And.left, Iff.mp, mul_ne_zero_iff
-- Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
⊢ Membership.mem (γ := Ideal 𝕜[X]) (annIdeal 𝕜 a) (annIdealGenerator 𝕜 a)

Tactic:
Ideal.mul_mem_right _ _ (Submodule.IsPrincipal.generator_mem _)

Premises used: Set.Mem, Polynomial.annIdealGenerator, Ideal.mul_mem_right, Submodule.IsPrincipal.generator_mem
-- Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
p : 𝕜[X]
a : A
simp_rw :
  Membership.mem (γ := Ideal 𝕜[X]) (annIdeal 𝕜 a) p ↔
    ∃ (s : 𝕜[X]), HSMul.hSMul (β := 𝕜[X]) s (annIdealGenerator 𝕜 a) = p
simp_rw₁ :
  Membership.mem (γ := Ideal 𝕜[X]) (annIdeal 𝕜 a) p ↔
    Membership.mem (γ := Submodule 𝕜[X] 𝕜[X]) (𝕜[X] ∙ annIdealGenerator 𝕜 a) p
⊢ Membership.mem (γ := Ideal 𝕜[X]) (annIdeal 𝕜 a) p ↔
    ∃ (s : 𝕜[X]), p = HSMul.hSMul (β := 𝕜[X]) s (annIdealGenerator 𝕜 a)

Tactic:
simp_rw [@eq_comm _ p, ← mem_span_singleton, ← span_singleton_annIdealGenerator 𝕜 a]

Premises used: Polynomial.span_singleton_annIdealGenerator, Submodule.mem_span_singleton, eq_comm
-- Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
hg : Ne (α := 𝕜[X]) (annIdealGenerator 𝕜 a) 0
⊢ Monic (annIdealGenerator 𝕜 a)

Tactic:
monic_mul_leadingCoeff_inv (mul_ne_zero_iff.mp hg).1

Premises used: Polynomial.annIdealGenerator, And.left, Polynomial.monic_mul_leadingCoeff_inv, Iff.mp, mul_ne_zero_iff
-- Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
⊢ Eq.{u_2 + 1} (α := A) ((aeval a : (a : 𝕜[X]) → A) (annIdealGenerator 𝕜 a) : A) (0 : A)

Tactic:
mem_annIdeal_iff_aeval_eq_zero.mp (annIdealGenerator_mem 𝕜 a)

Premises used: Polynomial.annIdealGenerator_mem, Polynomial.mem_annIdeal_iff_aeval_eq_zero, Iff.mp
-- Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
p : 𝕜[X]
a : A
rw :
  Membership.mem (γ := Ideal 𝕜[X]) (annIdeal 𝕜 a) p ↔
    Membership.mem (γ := Ideal 𝕜[X]) (Ideal.span {annIdealGenerator 𝕜 a}) p
rw₁ rw₂ : Membership.mem (γ := Ideal 𝕜[X]) (annIdeal 𝕜 a) p ↔ Membership.mem (γ := Ideal 𝕜[X]) (annIdeal 𝕜 a) p
⊢ Membership.mem (γ := Ideal 𝕜[X]) (annIdeal 𝕜 a) p ↔ annIdealGenerator 𝕜 a ∣ p

Tactic:
rw [← Ideal.mem_span_singleton, span_singleton_annIdealGenerator]

Premises used: Polynomial.span_singleton_annIdealGenerator, Ideal.mem_span_singleton
-- Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
p : 𝕜[X]
hp : Membership.mem (γ := Ideal 𝕜[X]) (annIdeal 𝕜 a) p
hpn0 : p ≠ 0
⊢ degree (annIdealGenerator 𝕜 a) ≤ p.degree

Tactic:
degree_le_of_dvd (mem_iff_annIdealGenerator_dvd.1 hp) hpn0

Premises used: Polynomial.degree_le_of_dvd, Polynomial.mem_iff_annIdealGenerator_dvd, Iff.mp
-- Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
pos : ∀ (h : Eq (α := 𝕜[X]) (annIdealGenerator 𝕜 a) 0), Eq (α := 𝕜[X]) (annIdealGenerator 𝕜 a) (minpoly 𝕜 a)
neg : ∀ (h : ¬Eq (α := 𝕜[X]) (annIdealGenerator 𝕜 a) 0), Eq (α := 𝕜[X]) (annIdealGenerator 𝕜 a) (minpoly 𝕜 a)
⊢ Eq (α := 𝕜[X]) (annIdealGenerator 𝕜 a) (minpoly 𝕜 a)

Tactic:
by_cases h : annIdealGenerator 𝕜 a = 0

Premises used: Polynomial.annIdealGenerator
-- Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
h : Eq (α := 𝕜[X]) (annIdealGenerator 𝕜 a) 0
pos : ¬IsIntegral 𝕜 a
⊢ Eq (α := 𝕜[X]) (annIdealGenerator 𝕜 a) (minpoly 𝕜 a)

Tactic:
rw [h, minpoly.eq_zero]

Premises used: minpoly.eq_zero
-- Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
h : Eq (α := 𝕜[X]) (annIdealGenerator 𝕜 a) 0
p : 𝕜[X]
p_monic : p.Monic
hp : Eq.{u_2 + 1} (α := A) ((aeval a : (a : 𝕜[X]) → A) p : A) (0 : A)
⊢ False

Tactic:
p_monic.ne_zero (Ideal.mem_bot.mp ?_)

Premises used: Ideal.mem_bot, Iff.mp, Polynomial.Monic.ne_zero
-- Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
h : Eq (α := 𝕜[X]) (annIdealGenerator 𝕜 a) 0
p : 𝕜[X]
p_monic : p.Monic
hp : Eq.{u_2 + 1} (α := A) ((aeval a : (a : 𝕜[X]) → A) p : A) (0 : A)
pos : Membership.mem (γ := Ideal 𝕜[X]) ⊥ p
⊢ False

Tactic:
refine p_monic.ne_zero (Ideal.mem_bot.mp ?_)

Premises used: Ideal.mem_bot, Iff.mp, Polynomial.Monic.ne_zero
-- Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
h : Eq (α := 𝕜[X]) (annIdealGenerator 𝕜 a) 0
p : 𝕜[X]
p_monic : p.Monic
hp : Eq.{u_2 + 1} (α := A) ((aeval a : (a : 𝕜[X]) → A) p : A) (0 : A)
⊢ Membership.mem (γ := Ideal 𝕜[X]) ⊥ p

Tactic:
simpa only [annIdealGenerator_eq_zero_iff.mp h] using mem_annIdeal_iff_aeval_eq_zero.mpr hp

Premises used: Iff.mpr, Polynomial.mem_annIdeal_iff_aeval_eq_zero, Iff.mp, Polynomial.annIdealGenerator_eq_zero_iff
-- Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
h : ¬Eq (α := 𝕜[X]) (annIdealGenerator 𝕜 a) 0
⊢ Eq (α := 𝕜[X]) (annIdealGenerator 𝕜 a) (minpoly 𝕜 a)

Tactic:
minpoly.unique _ _ (monic_annIdealGenerator _ _ h) (annIdealGenerator_aeval_eq_zero _ _)
      fun q q_monic hq =>
        degree_annIdealGenerator_le_of_mem a q (mem_annIdeal_iff_aeval_eq_zero.mpr hq)
          q_monic.ne_zero

Premises used: Iff.mpr, minpoly.unique, Polynomial.mem_annIdeal_iff_aeval_eq_zero, Polynomial.annIdealGenerator_aeval_eq_zero, Polynomial.degree_annIdealGenerator_le_of_mem, Polynomial.monic_annIdealGenerator, Polynomial.Monic.ne_zero
-- Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
h : ¬Eq (α := 𝕜[X]) (annIdealGenerator 𝕜 a) 0
⊢ Eq (α := 𝕜[X]) (annIdealGenerator 𝕜 a) (minpoly 𝕜 a)

Tactic:
exact minpoly.unique _ _ (monic_annIdealGenerator _ _ h) (annIdealGenerator_aeval_eq_zero _ _)
      fun q q_monic hq =>
        degree_annIdealGenerator_le_of_mem a q (mem_annIdeal_iff_aeval_eq_zero.mpr hq)
          q_monic.ne_zero

Premises used: Iff.mpr, minpoly.unique, Polynomial.mem_annIdeal_iff_aeval_eq_zero, Polynomial.annIdealGenerator_aeval_eq_zero, Polynomial.degree_annIdealGenerator_le_of_mem, Polynomial.monic_annIdealGenerator, Polynomial.Monic.ne_zero
-- Module: Mathlib.LinearAlgebra.AnnihilatingPolynomial
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Field 𝕜
inst_1 : Ring A
inst_2 : Algebra 𝕜 A
a : A
p : 𝕜[X]
p_monic : p.Monic
p_gen : Eq (α := Ideal 𝕜[X]) (Ideal.span {p}) (annIdeal 𝕜 a)
pos : ∀ (h : p = 0), annIdealGenerator 𝕜 a = p
neg : ∀ (h : ¬p = 0), annIdealGenerator 𝕜 a = p
⊢ annIdealGenerator 𝕜 a = p

Tactic:
by_cases h : p = 0