awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
p : R[X]
hroots : p.roots.card = p.natDegree
k : ℕ
h : k ≤ p.natDegree
this : k ≤ p.roots.card
h₁ h₂ : p.natDegree - k = p.natDegree - k
⊢ p.natDegree - k = p.roots.card - k

Tactic:
rw [hroots]
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
F : Type u_2
inst : Field F
p : F[X]
hsplit : p.Splits
k : ℕ
h : k ≤ p.natDegree
⊢ p.coeff k = p.leadingCoeff * HPow.hPow (α := F) (-1) (p.natDegree - k) * p.roots.esymm (p.natDegree - k)

Tactic:
Polynomial.coeff_eq_esymm_roots_of_card (splits_iff_card_roots.1 hsplit) h

Premises used: Polynomial.splits_iff_card_roots, Iff.mp, Polynomial.coeff_eq_esymm_roots_of_card
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : Fintype σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun (i : σ) ↦ X i) (val univ)
rw : Fintype.card σ = Multiset.card.{u_2} (α := σ) (val univ)
rw₁ : Finset.card.{u_2} (α := σ) univ = Multiset.card.{u_2} (α := σ) (val univ)
rw₂ rw₃ : Multiset.card.{u_2} (α := σ) (val univ) = Multiset.card.{u_2} (α := σ) (val univ)
⊢ Fintype.card σ = s.card

Tactic:
rw [Multiset.card_map, ← Finset.card_univ, Finset.card_def]

Premises used: Finset.card_univ, Finset.card_def, Multiset.card_map
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : Fintype σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun (i : σ) ↦ X i) (val univ)
⊢ Fintype.card σ = s.card

Tactic:
have : Fintype.card σ = Multiset.card s := by
    rw [Multiset.card_map, ← Finset.card_univ, Finset.card_def]
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : Fintype σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun (i : σ) ↦ X i) (val univ)
this : Fintype.card σ = s.card
simp_rw :
  Eq (α := (MvPolynomial σ R)[X])
    (Multiset.prod
      (Multiset.map
        (fun (i : σ) ↦
          HAdd.hAdd (α := (MvPolynomial σ R)[X]) (β := (MvPolynomial σ R)[X]) Polynomial.X
            ((Polynomial.C : (a : MvPolynomial σ R) → (MvPolynomial σ R)[X]) (X i) : (MvPolynomial σ R)[X]))
        (val univ)))
    (∑ x ∈ range (s.card + 1),
      HMul.hMul (α := (MvPolynomial σ R)[X])
        ((Polynomial.C : (a : MvPolynomial σ R) → (MvPolynomial σ R)[X])
            (Multiset.esymm (Multiset.map X (val univ)) x) :
          (MvPolynomial σ R)[X])
        (HPow.hPow (α := (MvPolynomial σ R)[X]) Polynomial.X (s.card - x)))
⊢ Eq (α := (MvPolynomial σ R)[X])
    (∏ i : σ,
      HAdd.hAdd (α := (MvPolynomial σ R)[X]) (β := (MvPolynomial σ R)[X]) Polynomial.X
        ((Polynomial.C : (a : MvPolynomial σ R) → (MvPolynomial σ R)[X]) (X i) : (MvPolynomial σ R)[X]))
    (∑ j ∈ range (Fintype.card σ + 1),
      HMul.hMul (α := (MvPolynomial σ R)[X])
        ((Polynomial.C : (a : MvPolynomial σ R) → (MvPolynomial σ R)[X]) (esymm σ R j) : (MvPolynomial σ R)[X])
        (HPow.hPow (α := (MvPolynomial σ R)[X]) Polynomial.X (Fintype.card σ - j)))

Tactic:
simp_rw [this, MvPolynomial.esymm_eq_multiset_esymm σ R, Finset.prod_eq_multiset_prod]

Premises used: Finset.prod_eq_multiset_prod, MvPolynomial.esymm_eq_multiset_esymm
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : Fintype σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun (i : σ) ↦ X i) (val univ)
this : Fintype.card σ = s.card
⊢ Eq (α := (MvPolynomial σ R)[X])
    (Multiset.prod
      (Multiset.map
        (fun (r : MvPolynomial σ R) ↦
          HAdd.hAdd (α := (MvPolynomial σ R)[X]) (β := (MvPolynomial σ R)[X]) Polynomial.X
            ((Polynomial.C : (a : MvPolynomial σ R) → (MvPolynomial σ R)[X]) r : (MvPolynomial σ R)[X]))
        s))
    (∑ j ∈ range (s.card + 1),
      HMul.hMul (α := (MvPolynomial σ R)[X])
        ((Polynomial.C : (a : MvPolynomial σ R) → (MvPolynomial σ R)[X]) (s.esymm j) : (MvPolynomial σ R)[X])
        (HPow.hPow (α := (MvPolynomial σ R)[X]) Polynomial.X (s.card - j)))

Tactic:
Multiset.prod_X_add_C_eq_sum_esymm s

Premises used: Multiset.prod_X_add_C_eq_sum_esymm
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : Fintype σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun (i : σ) ↦ X i) (val univ)
this : Fintype.card σ = s.card
h :
  Eq (α := Multiset (MvPolynomial σ R)[X])
    (Multiset.map
      (fun (i : σ) ↦
        HAdd.hAdd (α := (MvPolynomial σ R)[X]) (β := (MvPolynomial σ R)[X]) Polynomial.X
          ((Polynomial.C : (a : MvPolynomial σ R) → (MvPolynomial σ R)[X]) (X i) : (MvPolynomial σ R)[X]))
      (val univ))
    (Multiset.map
      (fun (r : MvPolynomial σ R) ↦
        HAdd.hAdd (α := (MvPolynomial σ R)[X]) (β := (MvPolynomial σ R)[X]) Polynomial.X
          ((Polynomial.C : (a : MvPolynomial σ R) → (MvPolynomial σ R)[X]) r : (MvPolynomial σ R)[X]))
      s)
⊢ Eq (α := (MvPolynomial σ R)[X])
    (Multiset.prod
      (Multiset.map
        (fun (i : σ) ↦
          HAdd.hAdd (α := (MvPolynomial σ R)[X]) (β := (MvPolynomial σ R)[X]) Polynomial.X
            ((Polynomial.C : (a : MvPolynomial σ R) → (MvPolynomial σ R)[X]) (X i) : (MvPolynomial σ R)[X]))
        (val univ)))
    (∑ x ∈ range (s.card + 1),
      HMul.hMul (α := (MvPolynomial σ R)[X])
        ((Polynomial.C : (a : MvPolynomial σ R) → (MvPolynomial σ R)[X])
            (Multiset.esymm (Multiset.map X (val univ)) x) :
          (MvPolynomial σ R)[X])
        (HPow.hPow (α := (MvPolynomial σ R)[X]) Polynomial.X (s.card - x)))

Tactic:
convert! Multiset.prod_X_add_C_eq_sum_esymm s

Premises used: Multiset.prod_X_add_C_eq_sum_esymm
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : Fintype σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun (i : σ) ↦ X i) (val univ)
this : Fintype.card σ = s.card
h :
  Eq (α := Multiset (MvPolynomial σ R)[X])
    (Multiset.map
      (fun (i : σ) ↦
        HAdd.hAdd (α := (MvPolynomial σ R)[X]) (β := (MvPolynomial σ R)[X]) Polynomial.X
          ((Polynomial.C : (a : MvPolynomial σ R) → (MvPolynomial σ R)[X]) (X i) : (MvPolynomial σ R)[X]))
      (val univ))
    (Multiset.map
      (fun (r : MvPolynomial σ R) ↦
        HAdd.hAdd (α := (MvPolynomial σ R)[X]) (β := (MvPolynomial σ R)[X]) Polynomial.X
          ((Polynomial.C : (a : MvPolynomial σ R) → (MvPolynomial σ R)[X]) r : (MvPolynomial σ R)[X]))
      (Multiset.map (fun (i : σ) ↦ X i) (val univ)))
h₁ :
  Eq (α := Multiset (MvPolynomial σ R)[X])
    (Multiset.map
      (fun (i : σ) ↦
        HAdd.hAdd (α := (MvPolynomial σ R)[X]) (β := (MvPolynomial σ R)[X]) Polynomial.X
          ((Polynomial.C : (a : MvPolynomial σ R) → (MvPolynomial σ R)[X]) (X i) : (MvPolynomial σ R)[X]))
      (val univ))
    (Multiset.map (α := σ)
      ((fun (r : MvPolynomial σ R) ↦
          HAdd.hAdd (α := (MvPolynomial σ R)[X]) (β := (MvPolynomial σ R)[X]) Polynomial.X
            ((Polynomial.C : (a : MvPolynomial σ R) → (MvPolynomial σ R)[X]) r : (MvPolynomial σ R)[X])) ∘
        fun (i : σ) ↦ X i)
      (val univ))
⊢ Eq (α := Multiset (MvPolynomial σ R)[X])
    (Multiset.map
      (fun (i : σ) ↦
        HAdd.hAdd (α := (MvPolynomial σ R)[X]) (β := (MvPolynomial σ R)[X]) Polynomial.X
          ((Polynomial.C : (a : MvPolynomial σ R) → (MvPolynomial σ R)[X]) (X i) : (MvPolynomial σ R)[X]))
      (val univ))
    (Multiset.map
      (fun (r : MvPolynomial σ R) ↦
        HAdd.hAdd (α := (MvPolynomial σ R)[X]) (β := (MvPolynomial σ R)[X]) Polynomial.X
          ((Polynomial.C : (a : MvPolynomial σ R) → (MvPolynomial σ R)[X]) r : (MvPolynomial σ R)[X]))
      s)

Tactic:
simp_rw [s, Multiset.map_map, Function.comp_apply]

Premises used: Multiset.map_map, Function.comp_apply
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : Fintype σ
k : ℕ
h : k ≤ Fintype.card σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun (i : σ) ↦ X i) (val univ)
rw : Fintype.card σ = Multiset.card.{u_2} (α := σ) (val univ)
rw₁ : Finset.card.{u_2} (α := σ) univ = Multiset.card.{u_2} (α := σ) (val univ)
rw₂ rw₃ : Multiset.card.{u_2} (α := σ) (val univ) = Multiset.card.{u_2} (α := σ) (val univ)
⊢ Fintype.card σ = s.card

Tactic:
rw [Multiset.card_map, ← Finset.card_univ, Finset.card_def]

Premises used: Finset.card_univ, Finset.card_def, Multiset.card_map
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : Fintype σ
k : ℕ
h : k ≤ Fintype.card σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun (i : σ) ↦ X i) (val univ)
⊢ Fintype.card σ = s.card

Tactic:
have : Fintype.card σ = Multiset.card s := by
    rw [Multiset.card_map, ← Finset.card_univ, Finset.card_def]
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : Fintype σ
k : ℕ
h : k ≤ Fintype.card σ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun (i : σ) ↦ X i) (val univ)
this : Fintype.card σ = s.card
rw :
  ∀ (h : k ≤ s.card) (this : Fintype.card σ = s.card),
    Eq (α := MvPolynomial σ R)
      (Polynomial.coeff
        (∏ i : σ,
          HAdd.hAdd (α := (MvPolynomial σ R)[X]) (β := (MvPolynomial σ R)[X]) Polynomial.X
            ((Polynomial.C : (a : MvPolynomial σ R) → (MvPolynomial σ R)[X]) (X i) : (MvPolynomial σ R)[X]))
        k)
      (esymm σ R (s.card - k))
⊢ Eq (α := MvPolynomial σ R)
    (Polynomial.coeff
      (∏ i : σ,
        HAdd.hAdd (α := (MvPolynomial σ R)[X]) (β := (MvPolynomial σ R)[X]) Polynomial.X
          ((Polynomial.C : (a : MvPolynomial σ R) → (MvPolynomial σ R)[X]) (X i) : (MvPolynomial σ R)[X]))
      k)
    (esymm σ R (Fintype.card σ - k))

Tactic:
rw [this] at h ⊢
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : Fintype σ
k : ℕ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun (i : σ) ↦ X i) (val univ)
h : k ≤ s.card
this : Fintype.card σ = s.card
rw :
  Eq (α := MvPolynomial σ R)
    (Polynomial.coeff
      (Multiset.prod
        (Multiset.map
          (fun (i : σ) ↦
            HAdd.hAdd (α := (MvPolynomial σ R)[X]) (β := (MvPolynomial σ R)[X]) Polynomial.X
              ((Polynomial.C : (a : MvPolynomial σ R) → (MvPolynomial σ R)[X]) (X i) : (MvPolynomial σ R)[X]))
          (val univ)))
      k)
    (Multiset.esymm (Multiset.map X (val univ)) (s.card - k))
⊢ Eq (α := MvPolynomial σ R)
    (Polynomial.coeff
      (∏ i : σ,
        HAdd.hAdd (α := (MvPolynomial σ R)[X]) (β := (MvPolynomial σ R)[X]) Polynomial.X
          ((Polynomial.C : (a : MvPolynomial σ R) → (MvPolynomial σ R)[X]) (X i) : (MvPolynomial σ R)[X]))
      k)
    (esymm σ R (s.card - k))

Tactic:
rw [MvPolynomial.esymm_eq_multiset_esymm σ R, Finset.prod_eq_multiset_prod]

Premises used: Finset.prod_eq_multiset_prod, MvPolynomial.esymm_eq_multiset_esymm
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : Fintype σ
k : ℕ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun (i : σ) ↦ X i) (val univ)
h : k ≤ s.card
this : Fintype.card σ = s.card
⊢ Polynomial.coeff
      (Multiset.prod
        (Multiset.map
          (fun (r : MvPolynomial σ R) ↦
            HAdd.hAdd (α := (MvPolynomial σ R)[X]) (β := (MvPolynomial σ R)[X]) Polynomial.X
              ((Polynomial.C : (a : MvPolynomial σ R) → (MvPolynomial σ R)[X]) r : (MvPolynomial σ R)[X]))
          s))
      k =
    s.esymm (s.card - k)

Tactic:
Multiset.prod_X_add_C_coeff s h

Premises used: Multiset.prod_X_add_C_coeff
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : Fintype σ
k : ℕ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun (i : σ) ↦ X i) (val univ)
h : k ≤ s.card
this : Fintype.card σ = s.card
h₁ :
  Eq (α := Semiring (MvPolynomial σ R)) AddMonoidAlgebra.semiring CommSemiring.toSemiring →
    Eq (α := Multiset (MvPolynomial σ R)[X])
      (Multiset.map
        (fun (i : σ) ↦
          HAdd.hAdd (α := (MvPolynomial σ R)[X]) (β := (MvPolynomial σ R)[X]) Polynomial.X
            ((Polynomial.C : (a : MvPolynomial σ R) → (MvPolynomial σ R)[X]) (X i) : (MvPolynomial σ R)[X]))
        (val univ))
      (Multiset.map
        (fun (r : MvPolynomial σ R) ↦
          HAdd.hAdd (α := (MvPolynomial σ R)[X]) (β := (MvPolynomial σ R)[X]) Polynomial.X
            ((Polynomial.C : (a : MvPolynomial σ R) → (MvPolynomial σ R)[X]) r : (MvPolynomial σ R)[X]))
        s)
⊢ Eq (α := MvPolynomial σ R)
    (Polynomial.coeff
      (Multiset.prod
        (Multiset.map
          (fun (i : σ) ↦
            HAdd.hAdd (α := (MvPolynomial σ R)[X]) (β := (MvPolynomial σ R)[X]) Polynomial.X
              ((Polynomial.C : (a : MvPolynomial σ R) → (MvPolynomial σ R)[X]) (X i) : (MvPolynomial σ R)[X]))
          (val univ)))
      k)
    (Multiset.esymm (Multiset.map X (val univ)) (s.card - k))

Tactic:
convert! Multiset.prod_X_add_C_coeff s h

Premises used: Multiset.prod_X_add_C_coeff
-- Module: Mathlib.RingTheory.Polynomial.Vieta
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
inst_1 : Fintype σ
k : ℕ
s : Multiset (MvPolynomial σ R) := Multiset.map (fun (i : σ) ↦ X i) (val univ)
h : k ≤ s.card
this : Fintype.card σ = s.card
e_2 : Eq (α := Semiring (MvPolynomial σ R)) AddMonoidAlgebra.semiring CommSemiring.toSemiring
h₁ :
  Eq (α := Multiset (MvPolynomial σ R)[X])
    (Multiset.map
      (fun (i : σ) ↦
        HAdd.hAdd (α := (MvPolynomial σ R)[X]) (β := (MvPolynomial σ R)[X]) Polynomial.X
          ((Polynomial.C : (a : MvPolynomial σ R) → (MvPolynomial σ R)[X]) (X i) : (MvPolynomial σ R)[X]))
      (val univ))
    (Multiset.map
      (fun (r : MvPolynomial σ R) ↦
        HAdd.hAdd (α := (MvPolynomial σ R)[X]) (β := (MvPolynomial σ R)[X]) Polynomial.X
          ((Polynomial.C : (a : MvPolynomial σ R) → (MvPolynomial σ R)[X]) r : (MvPolynomial σ R)[X]))
      (Multiset.map (fun (i : σ) ↦ X i) (val univ)))
h₂ :
  Eq (α := Multiset (MvPolynomial σ R)[X])
    (Multiset.map
      (fun (i : σ) ↦
        HAdd.hAdd (α := (MvPolynomial σ R)[X]) (β := (MvPolynomial σ R)[X]) Polynomial.X
          ((Polynomial.C : (a : MvPolynomial σ R) → (MvPolynomial σ R)[X]) (X i) : (MvPolynomial σ R)[X]))
      (val univ))
    (Multiset.map (α := σ)
      ((fun (r : MvPolynomial σ R) ↦
          HAdd.hAdd (α := (MvPolynomial σ R)[X]) (β := (MvPolynomial σ R)[X]) Polynomial.X
            ((Polynomial.C : (a : MvPolynomial σ R) → (MvPolynomial σ R)[X]) r : (MvPolynomial σ R)[X])) ∘
        fun (i : σ) ↦ X i)
      (val univ))
⊢ Eq (α := Multiset (MvPolynomial σ R)[X])
    (Multiset.map
      (fun (i : σ) ↦
        HAdd.hAdd (α := (MvPolynomial σ R)[X]) (β := (MvPolynomial σ R)[X]) Polynomial.X
          ((Polynomial.C : (a : MvPolynomial σ R) → (MvPolynomial σ R)[X]) (X i) : (MvPolynomial σ R)[X]))
      (val univ))
    (Multiset.map
      (fun (r : MvPolynomial σ R) ↦
        HAdd.hAdd (α := (MvPolynomial σ R)[X]) (β := (MvPolynomial σ R)[X]) Polynomial.X
          ((Polynomial.C : (a : MvPolynomial σ R) → (MvPolynomial σ R)[X]) r : (MvPolynomial σ R)[X]))
      s)

Tactic:
simp_rw [s, Multiset.map_map, Function.comp_apply]

Premises used: Multiset.map_map, Function.comp_apply
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
a b : R[X]
⊢ (((wronskianBilin R : (a : R[X]) → R[X] →ₗ[R] R[X]) a : R[X] →ₗ[R] R[X]) : (a : R[X]) → R[X]) b = a.wronskian b

Tactic:
rfl

Premises used: Polynomial.wronskian, rfl
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
a : R[X]
rw : Eq (α := R[X]) ((0 : (a : R[X]) → R[X]) a : R[X]) (0 : R[X])
⊢ wronskian 0 a = 0

Tactic:
rw [← wronskianBilin_apply 0 a, map_zero]

Premises used: map_zero, Polynomial.wronskianBilin_apply, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
a : R[X]
⊢ Eq (α := R[X]) ((0 : (a : R[X]) → R[X]) a : R[X]) (0 : R[X])

Tactic:
rfl
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
a : R[X]
⊢ a.wronskian 0 = 0

Tactic:
(wronskianBilin R a).map_zero

Premises used: LinearMap.map_zero, Polynomial.wronskian, DFunLike.coe, Polynomial.wronskianBilin
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
a b : R[X]
⊢ (-a).wronskian b = -a.wronskian b

Tactic:
LinearMap.map_neg₂ (wronskianBilin R) a b

Premises used: Polynomial.wronskian, LinearMap.map_neg₂, Polynomial.wronskianBilin
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
a b : R[X]
⊢ a.wronskian (-b) = -a.wronskian b

Tactic:
(wronskianBilin R a).map_neg b

Premises used: LinearMap.map_neg, Polynomial.wronskian, DFunLike.coe, Polynomial.wronskianBilin
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
a b c : R[X]
⊢ a.wronskian (b + c) = a.wronskian b + a.wronskian c

Tactic:
(wronskianBilin R a).map_add b c

Premises used: LinearMap.map_add, Polynomial.wronskian, DFunLike.coe, Polynomial.wronskianBilin
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
a b c : R[X]
⊢ (a + b).wronskian c = a.wronskian c + b.wronskian c

Tactic:
(wronskianBilin R).map_add₂ a b c

Premises used: Polynomial.wronskian, LinearMap.map_add₂, Polynomial.wronskianBilin
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
a : R[X]
rw :
  HMul.hMul (β := R[X]) a ((derivative : (a : R[X]) → R[X]) a : R[X]) -
      HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) a =
    0
rw₁ :
  HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) a -
      HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) a =
    0
rw₂ rw₃ : Eq.{u_1 + 1} (α := R[X]) 0 0
⊢ a.wronskian a = 0

Tactic:
rw [wronskian, mul_comm, sub_self]

Premises used: sub_self, Polynomial.wronskian, mul_comm
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
⊢ LinearMap.IsAlt (M := R[X]) (wronskianBilin R)

Tactic:
wronskian_self_eq_zero

Premises used: Polynomial.wronskian_self_eq_zero, Polynomial.wronskian, LinearMap.IsAlt
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
a b : R[X]
⊢ -a.wronskian b = b.wronskian a

Tactic:
LinearMap.IsAlt.neg isAlt_wronskianBilin a b

Premises used: Polynomial.isAlt_wronskianBilin, Polynomial.wronskian, LinearMap.IsAlt.neg
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
a b c : R[X]
hAdd : a + b + c = 0
⊢ a.wronskian b = b.wronskian c

Tactic:
isAlt_wronskianBilin.eq_of_add_add_eq_zero hAdd

Premises used: Polynomial.isAlt_wronskianBilin, Polynomial.wronskian, LinearMap.IsAlt.eq_of_add_add_eq_zero
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b ≠ 0
⊢ (a.wronskian b).degree ≤
    max (HMul.hMul (β := R[X]) a ((derivative : (a : R[X]) → R[X]) b : R[X])).degree
      (HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) b).degree

Tactic:
Polynomial.degree_sub_le _ _

Premises used: Polynomial.degree_sub_le, Polynomial.wronskian
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b ≠ 0
rw :
  (HMul.hMul (β := R[X]) a ((derivative : (a : R[X]) → R[X]) b : R[X])).degree < a.degree + b.degree ∧
    (HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) b).degree < a.degree + b.degree
⊢ max (HMul.hMul (β := R[X]) a ((derivative : (a : R[X]) → R[X]) b : R[X])).degree
      (HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) b).degree <
    a.degree + b.degree

Tactic:
rw [max_lt_iff]

Premises used: max_lt_iff
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b ≠ 0
constructor : (HMul.hMul (β := R[X]) a ((derivative : (a : R[X]) → R[X]) b : R[X])).degree < a.degree + b.degree
constructor₁ : (HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) b).degree < a.degree + b.degree
⊢ (HMul.hMul (β := R[X]) a ((derivative : (a : R[X]) → R[X]) b : R[X])).degree < a.degree + b.degree ∧
    (HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) b).degree < a.degree + b.degree

Tactic:
constructor
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b ≠ 0
hab :
  (HMul.hMul (β := R[X]) a ((derivative : (a : R[X]) → R[X]) b : R[X])).degree ≤
    a.degree + degree.{u_1} (R := R) ((derivative : (a : R[X]) → R[X]) b)
hbc : a.degree + degree.{u_1} (R := R) ((derivative : (a : R[X]) → R[X]) b) < a.degree + b.degree
b₁ : WithBot ℕ
⊢ (HMul.hMul (β := R[X]) a ((derivative : (a : R[X]) → R[X]) b : R[X])).degree < a.degree + b.degree

Tactic:
apply lt_of_le_of_lt

Premises used: lt_of_le_of_lt
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b ≠ 0
⊢ (HMul.hMul (β := R[X]) a ((derivative : (a : R[X]) → R[X]) b : R[X])).degree ≤
    a.degree + degree.{u_1} (R := R) ((derivative : (a : R[X]) → R[X]) b)

Tactic:
degree_mul_le a (derivative b)

Premises used: Polynomial.degree_mul_le, Polynomial.derivative, DFunLike.coe
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b ≠ 0
⊢ (HMul.hMul (β := R[X]) a ((derivative : (a : R[X]) → R[X]) b : R[X])).degree ≤
    a.degree + degree.{u_1} (R := R) ((derivative : (a : R[X]) → R[X]) b)

Tactic:
exact degree_mul_le a (derivative b)

Premises used: Polynomial.degree_mul_le, Polynomial.derivative, DFunLike.coe
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b ≠ 0
⊢ a.degree ≠ ⊥

Tactic:
rw [← Polynomial.degree_ne_bot] at ha

Premises used: Polynomial.degree_ne_bot
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b ≠ 0
ha₁ : a.degree ≠ ⊥
⊢ b ≠ 0

Tactic:
rw [← Polynomial.degree_ne_bot] at ha

Premises used: Polynomial.degree_ne_bot
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
a b : R[X]
ha : a.degree ≠ ⊥
hb : b ≠ 0
hbc : degree.{u_1} (R := R) ((derivative : (a : R[X]) → R[X]) b) < b.degree
⊢ a.degree + degree.{u_1} (R := R) ((derivative : (a : R[X]) → R[X]) b) < a.degree + b.degree

Tactic:
rw [WithBot.add_lt_add_iff_left ha]

Premises used: WithBot.add_lt_add_iff_left
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
a b : R[X]
ha : a.degree ≠ ⊥
hb : b ≠ 0
⊢ degree.{u_1} (R := R) ((derivative : (a : R[X]) → R[X]) b) < b.degree

Tactic:
Polynomial.degree_derivative_lt hb

Premises used: Polynomial.degree_derivative_lt
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
a b : R[X]
ha : a.degree ≠ ⊥
hb : b ≠ 0
⊢ degree.{u_1} (R := R) ((derivative : (a : R[X]) → R[X]) b) < b.degree

Tactic:
exact Polynomial.degree_derivative_lt hb

Premises used: Polynomial.degree_derivative_lt
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b ≠ 0
⊢ (HMul.hMul (β := R[X]) a ((derivative : (a : R[X]) → R[X]) b : R[X])).degree < a.degree + b.degree

Tactic:
case left =>
        apply lt_of_le_of_lt
        · exact degree_mul_le a (derivative b)
        · rw [← Polynomial.degree_ne_bot] at ha
          rw [WithBot.add_lt_add_iff_left ha]
          exact Polynomial.degree_derivative_lt hb

Premises used: Polynomial.degree_mul_le, Polynomial.derivative, lt_of_le_of_lt, Polynomial.degree_derivative_lt, Polynomial.degree_ne_bot, DFunLike.coe, WithBot.add_lt_add_iff_left
-- Module: Mathlib.RingTheory.Polynomial.Wronskian
Goal:
R : Type u_1
inst : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b ≠ 0
hab :
  (HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) b).degree ≤
    degree.{u_1} (R := R) ((derivative : (a : R[X]) → R[X]) a) + b.degree
hbc : degree.{u_1} (R := R) ((derivative : (a : R[X]) → R[X]) a) + b.degree < a.degree + b.degree
b₁ : WithBot ℕ
⊢ (HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) a : R[X]) b).degree < a.degree + b.degree

Tactic:
apply lt_of_le_of_lt

Premises used: lt_of_le_of_lt