awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
⊢ g ∣ f

Tactic:
have g_dvd_f : g ∣ f := by
      rw [fgh]
      exact dvd_mul_right g h
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
g_dvd_f : g ∣ f
rw : h ∣ g * h
⊢ h ∣ f

Tactic:
rw [fgh]
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
g_dvd_f : g ∣ f
⊢ h ∣ g * h

Tactic:
dvd_mul_left h g

Premises used: dvd_mul_left
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
g_dvd_f : g ∣ f
⊢ h ∣ g * h

Tactic:
exact dvd_mul_left h g

Premises used: dvd_mul_left
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
g_dvd_f : g ∣ f
⊢ h ∣ f

Tactic:
have h_dvd_f : h ∣ f := by
      rw [fgh]
      exact dvd_mul_left h g
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
⊢ g ∣ k

Tactic:
have g_dvd_k : g ∣ k := dvd_mul_right g h.mirror
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
rw : h ∣ g.mirror * h
⊢ h ∣ k.mirror

Tactic:
rw [mirror_mul_of_domain, mirror_mirror]

Premises used: Polynomial.mirror_mul_of_domain, Polynomial.mirror_mirror
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
⊢ h ∣ g.mirror * h

Tactic:
dvd_mul_left h g.mirror

Premises used: Polynomial.mirror, dvd_mul_left
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
⊢ h ∣ g.mirror * h

Tactic:
exact dvd_mul_left h g.mirror

Premises used: Polynomial.mirror, dvd_mul_left
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
⊢ h ∣ k.mirror

Tactic:
have h_dvd_k_rev : h ∣ k.mirror := by
      rw [mirror_mul_of_domain, mirror_mirror]
      exact dvd_mul_left h g.mirror
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ k.mirror
⊢ k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror

Tactic:
have hk := h2 k key
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ k.mirror
hk : k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
isUnit_or_isUnit : ∀ (hk : k = f), IsUnit g ∨ IsUnit h
isUnit_or_isUnit₁ : ∀ (hk : k = -f), IsUnit g ∨ IsUnit h
isUnit_or_isUnit₂ : ∀ (hk : k = f.mirror), IsUnit g ∨ IsUnit h
isUnit_or_isUnit₃ : ∀ (hk : k = -f.mirror), IsUnit g ∨ IsUnit h
⊢ IsUnit g ∨ IsUnit h

Tactic:
rcases hk with (hk | hk | hk | hk)
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ k.mirror
hk : k = f
rwa rwa₁ rwa₂ rwa₃ : h ∣ k.mirror
⊢ h ∣ f.mirror

Tactic:
rwa [← hk]
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ k.mirror
hk : k = f
⊢ IsUnit g ∨ IsUnit h

Tactic:
exact Or.inr (h3 h_dvd_f (by rwa [← hk]))

Premises used: Or.inr
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ k.mirror
hk : k = -f
rwa : h ∣ (-k).mirror
rwa₁ : h ∣ -k.mirror
rwa₂ rwa₃ rwa₄ rwa₅ : h ∣ k.mirror
⊢ h ∣ f.mirror

Tactic:
rwa [← neg_eq_iff_eq_neg.mpr hk, mirror_neg, dvd_neg]

Premises used: Iff.mpr, Polynomial.mirror_neg, neg_eq_iff_eq_neg, dvd_neg
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ k.mirror
hk : k = -f
⊢ IsUnit g ∨ IsUnit h

Tactic:
exact Or.inr (h3 h_dvd_f (by rwa [← neg_eq_iff_eq_neg.mpr hk, mirror_neg, dvd_neg]))

Premises used: Or.inr
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ k.mirror
hk : k = f.mirror
rwa rwa₁ rwa₂ rwa₃ : g ∣ k
⊢ g ∣ f.mirror

Tactic:
rwa [← hk]
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ k.mirror
hk : k = f.mirror
⊢ IsUnit g ∨ IsUnit h

Tactic:
exact Or.inl (h3 g_dvd_f (by rwa [← hk]))

Premises used: Or.inl
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ k.mirror
hk : k = -f.mirror
rwa : g ∣ -k
rwa₁ rwa₂ rwa₃ rwa₄ : g ∣ k
⊢ g ∣ f.mirror

Tactic:
rwa [← neg_eq_iff_eq_neg.mpr hk, dvd_neg]

Premises used: Iff.mpr, neg_eq_iff_eq_neg, dvd_neg
-- Module: Mathlib.Algebra.Polynomial.Mirror
Goal:
R : Type u_1
inst : CommRing R
inst_1 : NoZeroDivisors R
f : R[X]
h1 : ¬IsUnit f
h2 : ∀ (k : R[X]), f * f.mirror = k * k.mirror → k = f ∨ k = -f ∨ k = f.mirror ∨ k = -f.mirror
h3 : IsRelPrime f f.mirror
g h : R[X]
fgh : f = g * h
k : R[X] := g * h.mirror
key : f * f.mirror = k * k.mirror
g_dvd_f : g ∣ f
h_dvd_f : h ∣ f
g_dvd_k : g ∣ k
h_dvd_k_rev : h ∣ k.mirror
hk : k = -f.mirror
⊢ IsUnit g ∨ IsUnit h

Tactic:
exact Or.inl (h3 g_dvd_f (by rwa [← neg_eq_iff_eq_neg.mpr hk, dvd_neg]))

Premises used: Or.inl
-- Module: Mathlib.Algebra.Polynomial.Module.AEval
Goal:
R : Type u_1
A : Type u_3
M : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
a : A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
f : R[X]
m : M
⊢ (of R M a : (a_1 : M) → AEval R M a) (HSMul.hSMul.{u_3, u_2, u_2} (α := A) ((aeval a : (a : R[X]) → A) f : A) m) =
    HSMul.hSMul (β := AEval R M a) f ((of R M a : (a_1 : M) → AEval R M a) m : AEval R M a)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Module.AEval
Goal:
R : Type u_1
A : Type u_3
M : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
a : A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
f : R[X]
m : AEval R M a
⊢ (LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) (f • m) =
    HSMul.hSMul.{u_3, u_2, u_2} (α := A) (β := M) ((aeval a : (a : R[X]) → A) f : A)
      ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) m : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Module.AEval
Goal:
R : Type u_1
A : Type u_3
M : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
a : A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
t : R
m : AEval R M a
⊢ Eq (α := M)
    ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) (HSMul.hSMul (α := R[X]) ((C : (a : R) → R[X]) t : R[X]) m) :
      M)
    ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) (t • m) : M)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Module.AEval
Goal:
R : Type u_2
A : Type u_3
M : Type u_1
inst : CommSemiring R
inst_1 : Semiring A
a : A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
m : M
rw :
  Eq (α := AEval R M a)
    ((of R M a : (a_1 : M) → AEval R M a) (HSMul.hSMul.{u_3, u_1, u_1} (α := A) ((aeval a : (a : R[X]) → A) X : A) m) :
      AEval R M a)
    ((of R M a : (a_1 : M) → AEval R M a) (a • m) : AEval R M a)
rw₁ rw₂ :
  Eq (α := AEval R M a) ((of R M a : (a_1 : M) → AEval R M a) (a • m) : AEval R M a)
    ((of R M a : (a_1 : M) → AEval R M a) (a • m) : AEval R M a)
⊢ HSMul.hSMul.{u_2, u_1, u_1} (α := R[X]) (β := AEval R M a) X ((of R M a : (a_1 : M) → AEval R M a) m : AEval R M a) =
    (of R M a : (a_1 : M) → AEval R M a) (a • m)

Tactic:
rw [← of_aeval_smul, aeval_X]

Premises used: Module.AEval.of_aeval_smul, Polynomial.aeval_X
-- Module: Mathlib.Algebra.Polynomial.Module.AEval
Goal:
R : Type u_2
A : Type u_3
M : Type u_1
inst : CommSemiring R
inst_1 : Semiring A
a : A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
m : M
n : ℕ
rw :
  Eq (α := AEval R M a)
    ((of R M a : (a_1 : M) → AEval R M a)
        (HSMul.hSMul.{u_3, u_1, u_1} (α := A) ((aeval a : (a : R[X]) → A) (HPow.hPow (α := R[X]) X n) : A) m) :
      AEval R M a)
    ((of R M a : (a_1 : M) → AEval R M a) (a ^ n • m) : AEval R M a)
rw₁ rw₂ :
  Eq (α := AEval R M a) ((of R M a : (a_1 : M) → AEval R M a) (a ^ n • m) : AEval R M a)
    ((of R M a : (a_1 : M) → AEval R M a) (a ^ n • m) : AEval R M a)
⊢ HSMul.hSMul (β := AEval R M a) (HPow.hPow (α := R[X]) X n) ((of R M a : (a_1 : M) → AEval R M a) m : AEval R M a) =
    (of R M a : (a_1 : M) → AEval R M a) (a ^ n • m)

Tactic:
rw [← of_aeval_smul, aeval_X_pow]

Premises used: Polynomial.aeval_X_pow, Module.AEval.of_aeval_smul
-- Module: Mathlib.Algebra.Polynomial.Module.AEval
Goal:
R : Type u_1
A : Type u_3
M : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
a : A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
m : AEval R M a
rw :
  HSMul.hSMul.{u_3, u_2, u_2} (α := A) (β := M) ((aeval a : (a : R[X]) → A) X : A)
      ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) m : M) =
    HSMul.hSMul (β := M) a ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) m : M)
rw₁ rw₂ :
  HSMul.hSMul (β := M) a ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) m : M) =
    HSMul.hSMul (β := M) a ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) m : M)
⊢ (LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) (HSMul.hSMul.{u_1, u_2, u_2} (α := R[X]) X m) =
    HSMul.hSMul (β := M) a ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) m : M)

Tactic:
rw [of_symm_smul, aeval_X]

Premises used: Module.AEval.of_symm_smul, Polynomial.aeval_X
-- Module: Mathlib.Algebra.Polynomial.Module.AEval
Goal:
R : Type u_1
A : Type u_3
M : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
a : A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
r : R
f : R[X]
m : AEval R M a
a₁ :
  Eq (α := M) ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) ((r • f) • m) : M)
    ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) (r • f • m) : M)
⊢ (r • f) • m = r • f • m

Tactic:
apply (of R M a).symm.injective

Premises used: LinearEquiv.symm, Module.AEval.of, LinearEquiv.injective
-- Module: Mathlib.Algebra.Polynomial.Module.AEval
Goal:
R : Type u_1
A : Type u_3
M : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
a : A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
r : R
f : R[X]
m : AEval R M a
a₁ :
  HSMul.hSMul.{u_3, u_2, u_2} (α := A) (β := M) ((aeval a : (a : R[X]) → A) (r • f) : A)
      ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) m : M) =
    (LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) (r • f • m)
a₂ :
  HSMul.hSMul (β := M) (HSMul.hSMul (β := A) r ((aeval a : (a : R[X]) → A) f : A))
      ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) m : M) =
    (LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) (r • f • m)
a₃ :
  r •
      HSMul.hSMul.{u_3, u_2, u_2} (α := A) (β := M) ((aeval a : (a : R[X]) → A) f : A)
        ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) m : M) =
    (LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) (r • f • m)
a₄ :
  r •
      HSMul.hSMul.{u_3, u_2, u_2} (α := A) (β := M) ((aeval a : (a : R[X]) → A) f : A)
        ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) m : M) =
    HSMul.hSMul (β := M) r ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) (f • m) : M)
a₅ a₆ :
  r •
      HSMul.hSMul.{u_3, u_2, u_2} (α := A) (β := M) ((aeval a : (a : R[X]) → A) f : A)
        ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) m : M) =
    r •
      HSMul.hSMul.{u_3, u_2, u_2} (α := A) (β := M) ((aeval a : (a : R[X]) → A) f : A)
        ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) m : M)
⊢ Eq (α := M) ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) ((r • f) • m) : M)
    ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) (r • f • m) : M)

Tactic:
rw [of_symm_smul, map_smul, smul_assoc, map_smul, of_symm_smul]

Premises used: Module.AEval.of_symm_smul, smul_assoc, map_smul
-- Module: Mathlib.Algebra.Polynomial.Module.AEval
Goal:
R : Type u_1
A : Type u_3
M : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
a : A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
inst_7 : Module.Finite R M
⊢ Module.Finite.{u_1, u_2} R[X] (AEval R M a)

Tactic:
Finite.of_restrictScalars_finite R _ _

Premises used: Module.Finite.of_restrictScalars_finite
-- Module: Mathlib.Algebra.Polynomial.Module.AEval
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
a : A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
N : Type u_4
inst_7 : AddCommMonoid N
inst_8 : Module R N
inst_9 : Module.{u_1, u_4} R[X] N
inst_10 : IsScalarTower R R[X] N
f : M →ₗ[R] N
hf : ∀ (m : M), (f : (a : M) → N) (a • m) = HSMul.hSMul.{u_1, u_4, u_4} (α := R[X]) (β := N) X ((f : (a : M) → N) m : N)
p : R[X]
k : R
m : AEval R M a
⊢ AddHom.toFun (LinearMap.toAddHom (f ∘ₗ (↑(LinearEquiv.symm (of R M a)) : AEval R M a →ₗ[R] M)))
      (HSMul.hSMul (α := R[X]) ((C : (a : R) → R[X]) k : R[X]) m) =
    HSMul.hSMul (α := R[X]) ((RingHom.id R[X] : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) k) : R[X])
      (AddHom.toFun (LinearMap.toAddHom (f ∘ₗ (↑(LinearEquiv.symm (of R M a)) : AEval R M a →ₗ[R] M))) m)

Tactic:
simp [C_eq_algebraMap]

Premises used: Polynomial.C_eq_algebraMap
-- Module: Mathlib.Algebra.Polynomial.Module.AEval
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
a : A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
N : Type u_4
inst_7 : AddCommMonoid N
inst_8 : Module R N
inst_9 : Module.{u_1, u_4} R[X] N
inst_10 : IsScalarTower R R[X] N
f : M →ₗ[R] N
hf : ∀ (m : M), (f : (a : M) → N) (a • m) = HSMul.hSMul.{u_1, u_4, u_4} (α := R[X]) (β := N) X ((f : (a : M) → N) m : N)
p_1 p q : R[X]
hp :
  ∀ (x : AEval R M a),
    AddHom.toFun (LinearMap.toAddHom (f ∘ₗ (↑(LinearEquiv.symm (of R M a)) : AEval R M a →ₗ[R] M))) (p • x) =
      HSMul.hSMul (α := R[X]) ((RingHom.id R[X] : (a : R[X]) → R[X]) p : R[X])
        (AddHom.toFun (LinearMap.toAddHom (f ∘ₗ (↑(LinearEquiv.symm (of R M a)) : AEval R M a →ₗ[R] M))) x)
hq :
  ∀ (x : AEval R M a),
    AddHom.toFun (LinearMap.toAddHom (f ∘ₗ (↑(LinearEquiv.symm (of R M a)) : AEval R M a →ₗ[R] M))) (q • x) =
      HSMul.hSMul (α := R[X]) ((RingHom.id R[X] : (a : R[X]) → R[X]) q : R[X])
        (AddHom.toFun (LinearMap.toAddHom (f ∘ₗ (↑(LinearEquiv.symm (of R M a)) : AEval R M a →ₗ[R] M))) x)
m : AEval R M a
⊢ AddHom.toFun (LinearMap.toAddHom (f ∘ₗ (↑(LinearEquiv.symm (of R M a)) : AEval R M a →ₗ[R] M))) ((p + q) • m) =
    HSMul.hSMul (α := R[X]) ((RingHom.id R[X] : (a : R[X]) → R[X]) (p + q) : R[X])
      (AddHom.toFun (LinearMap.toAddHom (f ∘ₗ (↑(LinearEquiv.symm (of R M a)) : AEval R M a →ₗ[R] M))) m)

Tactic:
simp_all [add_smul]

Premises used: add_smul
-- Module: Mathlib.Algebra.Polynomial.Module.AEval
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
a : A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
N : Type u_4
inst_7 : AddCommMonoid N
inst_8 : Module R N
inst_9 : Module.{u_1, u_4} R[X] N
inst_10 : IsScalarTower R R[X] N
f : M →ₗ[R] N
hf : ∀ (m : M), (f : (a : M) → N) (a • m) = HSMul.hSMul.{u_1, u_4, u_4} (α := R[X]) (β := N) X ((f : (a : M) → N) m : N)
p : R[X]
n : ℕ
k : R
h :
  ∀ (x : AEval R M a),
    AddHom.toFun (LinearMap.toAddHom (f ∘ₗ (↑(LinearEquiv.symm (of R M a)) : AEval R M a →ₗ[R] M)))
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) k : R[X]) (HPow.hPow (α := R[X]) X n) • x) =
      HSMul.hSMul (α := R[X])
        ((RingHom.id R[X] : (a : R[X]) → R[X])
            (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) k : R[X]) (HPow.hPow (α := R[X]) X n)) :
          R[X])
        (AddHom.toFun (LinearMap.toAddHom (f ∘ₗ (↑(LinearEquiv.symm (of R M a)) : AEval R M a →ₗ[R] M))) x)
m : AEval R M a
simp_rw :
  (f : (a : M) → N)
      ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M)
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) k : R[X]) (HPow.hPow (α := R[X]) X (n + 1)) • m) :
        M) =
    HSMul.hSMul (β := N) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) k : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))
      ((f : (a : M) → N) ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) m : M) : N)
⊢ AddHom.toFun (LinearMap.toAddHom (f ∘ₗ (↑(LinearEquiv.symm (of R M a)) : AEval R M a →ₗ[R] M)))
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) k : R[X]) (HPow.hPow (α := R[X]) X (n + 1)) • m) =
    HSMul.hSMul (α := R[X])
      ((RingHom.id R[X] : (a : R[X]) → R[X])
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) k : R[X]) (HPow.hPow (α := R[X]) X (n + 1))) :
        R[X])
      (AddHom.toFun (LinearMap.toAddHom (f ∘ₗ (↑(LinearEquiv.symm (of R M a)) : AEval R M a →ₗ[R] M))) m)

Tactic:
simp_rw [RingHom.id_apply, AddHom.toFun_eq_coe, LinearMap.coe_toAddHom,
        LinearMap.comp_apply, LinearEquiv.coe_toLinearMap] at h ⊢

Premises used: RingHom.id_apply, LinearMap.comp_apply, AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, LinearEquiv.coe_toLinearMap
-- Module: Mathlib.Algebra.Polynomial.Module.AEval
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
a : A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
N : Type u_4
inst_7 : AddCommMonoid N
inst_8 : Module R N
inst_9 : Module.{u_1, u_4} R[X] N
inst_10 : IsScalarTower R R[X] N
f : M ≃ₗ[R] N
hf : ∀ (m : M), (f : (a : M) → N) (a • m) = HSMul.hSMul.{u_1, u_4, u_4} (α := R[X]) (β := N) X ((f : (a : M) → N) m : N)
x : AEval R M a
⊢ Function.comp (β := M) (⇑(of R M a) : (a_1 : M) → AEval R M a) (⇑f.symm : (a : N) → M)
      (AddHom.toFun (LinearMap.toAddHom (LinearMap.ofAEval a (↑f : M →ₗ[R] N) hf)) x) =
    x

Tactic:
simp [LinearMap.ofAEval]

Premises used: LinearMap.ofAEval
-- Module: Mathlib.Algebra.Polynomial.Module.AEval
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
a : A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
N : Type u_4
inst_7 : AddCommMonoid N
inst_8 : Module R N
inst_9 : Module.{u_1, u_4} R[X] N
inst_10 : IsScalarTower R R[X] N
f : M ≃ₗ[R] N
hf : ∀ (m : M), (f : (a : M) → N) (a • m) = HSMul.hSMul.{u_1, u_4, u_4} (α := R[X]) (β := N) X ((f : (a : M) → N) m : N)
x : N
⊢ AddHom.toFun (M := AEval R M a) (LinearMap.toAddHom (LinearMap.ofAEval a (↑f : M →ₗ[R] N) hf))
      (Function.comp (β := M) (⇑(of R M a) : (a_1 : M) → AEval R M a) (⇑f.symm : (a : N) → M) x) =
    x

Tactic:
simp [LinearMap.ofAEval]

Premises used: LinearMap.ofAEval