awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Module.AEval
Goal:
R : Type u_3
A : Type u_1
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 : FaithfulSMul A M
h :
  ∀ (p : R[X]),
    Membership.mem (γ := Ideal R[X]) (annihilator.{u_3, u_2} R[X] (AEval R M a)) p ↔
      Membership.mem (γ := Ideal R[X]) (RingHom.ker (F := R[X] →ₐ[R] A) (aeval a)) p
⊢ Eq (α := Ideal R[X]) (annihilator.{u_3, u_2} R[X] (AEval R M a)) (RingHom.ker (F := R[X] →ₐ[R] A) (aeval a))

Tactic:
ext p
-- Module: Mathlib.Algebra.Polynomial.Module.AEval
Goal:
R : Type u_3
A : Type u_1
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 : FaithfulSMul A M
p : R[X]
h : (∀ (m : AEval R M a), p • m = 0) ↔ Eq.{u_1 + 1} (α := A) ((aeval a : (a : R[X]) → A) p : A) (0 : A)
⊢ Membership.mem (γ := Ideal R[X]) (annihilator.{u_3, u_2} R[X] (AEval R M a)) p ↔
    Membership.mem (γ := Ideal R[X]) (RingHom.ker (F := R[X] →ₐ[R] A) (aeval a)) p

Tactic:
simp_rw [mem_annihilator, RingHom.mem_ker]

Premises used: Module.mem_annihilator, RingHom.mem_ker
-- Module: Mathlib.Algebra.Polynomial.Module.AEval
Goal:
R : Type u_3
A : Type u_1
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 : FaithfulSMul A M
p : R[X]
h :
  (∀ (m : M), HSMul.hSMul.{u_1, u_2, u_2} (α := A) ((aeval a : (a : R[X]) → A) p : A) m = 0) ↔
    Eq.{u_1 + 1} (α := A) ((aeval a : (a : R[X]) → A) p : A) (0 : A)
⊢ (∀ (m : AEval R M a), p • m = 0) ↔ Eq.{u_1 + 1} (α := A) ((aeval a : (a : R[X]) → A) p : A) (0 : A)

Tactic:
change (∀ m : M, aeval a p • m = 0) ↔ _
-- Module: Mathlib.Algebra.Polynomial.Module.AEval
Goal:
R : Type u_3
A : Type u_1
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 : FaithfulSMul A M
p : R[X]
h : ∀ (m : M), HSMul.hSMul.{u_1, u_2, u_2} (α := A) ((aeval a : (a : R[X]) → A) p : A) m = 0
⊢ ∀ (a_1 : M),
    HSMul.hSMul.{u_1, u_2, u_2} (α := A) ((aeval a : (a : R[X]) → A) p : A) a_1 =
      HSMul.hSMul.{u_1, u_2, u_2} (α := A) 0 a_1

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Polynomial.Module.AEval
Goal:
R : Type u_3
A : Type u_1
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 : FaithfulSMul A M
p : R[X]
h : Eq.{u_1 + 1} (α := A) ((aeval a : (a : R[X]) → A) p : A) (0 : A)
⊢ ∀ (m : M), HSMul.hSMul.{u_1, u_2, u_2} (α := A) ((aeval a : (a : R[X]) → A) p : A) m = 0

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Polynomial.Module.AEval
Goal:
R : Type u_3
A : Type u_1
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 : FaithfulSMul A M
p : R[X]
⊢ (∀ (m : M), HSMul.hSMul.{u_1, u_2, u_2} (α := A) ((aeval a : (a : R[X]) → A) p : A) m = 0) ↔
    Eq.{u_1 + 1} (α := A) ((aeval a : (a : R[X]) → A) p : A) (0 : A)

Tactic:
exact ⟨fun h ↦ eq_of_smul_eq_smul (α := M) <| by simp [h], fun h ↦ by simp [h]⟩
-- Module: Mathlib.Algebra.Polynomial.Module.AEval
Goal:
R : Type u_3
A : Type u_1
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 : FaithfulSMul A M
h :
  ∀ (p : R[X]),
    Membership.mem (γ := Ideal R[X]) (Submodule.annihilator.{u_3, u_2} (M := AEval R M a) ⊤) p ↔
      Membership.mem (γ := Ideal R[X]) (RingHom.ker (F := R[X] →ₐ[R] A) (aeval a)) p
⊢ Eq (α := Ideal R[X]) (Submodule.annihilator.{u_3, u_2} (M := AEval R M a) ⊤)
    (RingHom.ker (F := R[X] →ₐ[R] A) (aeval a))

Tactic:
ext p
-- Module: Mathlib.Algebra.Polynomial.Module.AEval
Goal:
R : Type u_3
A : Type u_1
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 : FaithfulSMul A M
p : R[X]
h : (∀ (n : AEval R M a), p • n = 0) ↔ Eq.{u_1 + 1} (α := A) ((aeval a : (a : R[X]) → A) p : A) (0 : A)
⊢ Membership.mem (γ := Ideal R[X]) (Submodule.annihilator.{u_3, u_2} (M := AEval R M a) ⊤) p ↔
    Membership.mem (γ := Ideal R[X]) (RingHom.ker (F := R[X] →ₐ[R] A) (aeval a)) p

Tactic:
simp only [Submodule.mem_annihilator, Submodule.mem_top, forall_true_left, RingHom.mem_ker]

Premises used: forall_true_left, RingHom.mem_ker, Submodule.mem_annihilator, Submodule.mem_top
-- Module: Mathlib.Algebra.Polynomial.Module.AEval
Goal:
R : Type u_3
A : Type u_1
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 : FaithfulSMul A M
p : R[X]
h :
  (∀ (m : M), HSMul.hSMul.{u_1, u_2, u_2} (α := A) ((aeval a : (a : R[X]) → A) p : A) m = 0) ↔
    Eq.{u_1 + 1} (α := A) ((aeval a : (a : R[X]) → A) p : A) (0 : A)
⊢ (∀ (n : AEval R M a), p • n = 0) ↔ Eq.{u_1 + 1} (α := A) ((aeval a : (a : R[X]) → A) p : A) (0 : A)

Tactic:
change (∀ m : M, aeval a p • m = 0) ↔ _
-- 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
p : ↥(End.invtSubmodule ((Algebra.lsmul R R M : (a : A) → End R M) a))
f : R[X]
m : M
h : m ∈ (↑p : Submodule R M)
⊢ ∃ x ∈ (↑p : Submodule R M),
    (of R M a : (a_1 : M) → AEval R M a) x =
      HSMul.hSMul (β := AEval R M a) f ((of R M a : (a_1 : M) → AEval R M a) m : AEval R M a)

Tactic:
⟨aeval a f • m, aeval_apply_smul_mem_of_le_comap' h f a p.2, of_aeval_smul a f m⟩

Premises used: Polynomial.aeval_apply_smul_mem_of_le_comap', And.intro, Exists.intro, Module.AEval.of_aeval_smul, HSMul.hSMul, Polynomial.aeval, DFunLike.coe, Subtype.property
-- 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
p : ↥(End.invtSubmodule ((Algebra.lsmul R R M : (a : A) → End R M) a))
f : R[X]
m : M
h : m ∈ (↑p : Submodule R M)
⊢ ∃ x ∈ (↑p : Submodule R M),
    (of R M a : (a_1 : M) → AEval R M a) x =
      HSMul.hSMul (β := AEval R M a) f ((of R M a : (a_1 : M) → AEval R M a) m : AEval R M a)

Tactic:
exact ⟨aeval a f • m, aeval_apply_smul_mem_of_le_comap' h f a p.2, of_aeval_smul a f m⟩
-- 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
q : Submodule.{u_1, u_3} R[X] (AEval R M a)
m : M
hm :
  Membership.mem (γ := Submodule R M)
    ((OrderIso.symm (Submodule.orderIsoMapComap (of R M a)) : (a : Submodule R (AEval R M a)) → Submodule R M)
        (Submodule.restrictScalars R q) :
      Submodule R M)
    m
⊢ Membership.mem (γ := Submodule R M)
    (Submodule.comap (R₂ := R) (M₂ := M) (σ₁₂ := RingHom.id R) ((Algebra.lsmul R R M : (a : A) → End R M) a)
      ((OrderIso.symm (Submodule.orderIsoMapComap (of R M a)) : (a : Submodule R (AEval R M a)) → Submodule R M)
        (Submodule.restrictScalars R q)))
    m

Tactic:
simpa [← X_smul_of] using q.smul_mem (X : R[X]) hm

Premises used: Module.AEval.X_smul_of, Polynomial.X, Submodule.smul_mem
-- 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
p : ↥(End.invtSubmodule ((Algebra.lsmul R R M : (a : A) → End R M) a))
a₁ :
  ∀ (x : M),
    Membership.mem (γ := Submodule R M)
        (↑((fun (q : Submodule.{u_1, u_3} R[X] (AEval R M a)) ↦
                (Subtype.mk (p := fun (x : Submodule R M) ↦
                    Membership.mem (γ := Sublattice (Submodule R M))
                      (End.invtSubmodule ((Algebra.lsmul R R M : (a : A) → End R M) a)) x)
                    ((OrderIso.symm (Submodule.orderIsoMapComap (of R M a)) :
                        (a : Submodule R (AEval R M a)) → Submodule R M)
                      (Submodule.restrictScalars R q))
                    ⋯ :
                  ↥(End.invtSubmodule ((Algebra.lsmul R R M : (a : A) → End R M) a))))
              ((fun (p : ↥(End.invtSubmodule ((Algebra.lsmul R R M : (a : A) → End R M) a))) ↦
                  let __AddSubmonoid : AddSubmonoid (AEval R M a) :=
                    AddSubmonoid.map (F := M ≃ₗ[R] AEval R M a) (of R M a) (↑p : Submodule R M).toAddSubmonoid;
                  { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ : Submodule.{u_1, u_3} R[X] (AEval R M a) })
                p)) :
          Submodule R M)
        x ↔
      x ∈ (↑p : Submodule R M)
⊢ (fun (q : Submodule.{u_1, u_3} R[X] (AEval R M a)) ↦
        (Subtype.mk (p := fun (x : Submodule R M) ↦
            Membership.mem (γ := Sublattice (Submodule R M))
              (End.invtSubmodule ((Algebra.lsmul R R M : (a : A) → End R M) a)) x)
            ((OrderIso.symm (Submodule.orderIsoMapComap (of R M a)) : (a : Submodule R (AEval R M a)) → Submodule R M)
              (Submodule.restrictScalars R q))
            ⋯ :
          ↥(End.invtSubmodule ((Algebra.lsmul R R M : (a : A) → End R M) a))))
      ((fun (p : ↥(End.invtSubmodule ((Algebra.lsmul R R M : (a : A) → End R M) a))) ↦
          let __AddSubmonoid : AddSubmonoid (AEval R M a) :=
            AddSubmonoid.map (F := M ≃ₗ[R] AEval R M a) (of R M a) (↑p : Submodule R M).toAddSubmonoid;
          { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ : Submodule.{u_1, u_3} R[X] (AEval R M a) })
        p) =
    p

Tactic:
ext
-- 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
p : ↥(End.invtSubmodule ((Algebra.lsmul R R M : (a : A) → End R M) a))
x : M
⊢ Membership.mem (γ := Submodule R M)
      (↑((fun (q : Submodule.{u_1, u_3} R[X] (AEval R M a)) ↦
              (Subtype.mk (p := fun (x : Submodule R M) ↦
                  Membership.mem (γ := Sublattice (Submodule R M))
                    (End.invtSubmodule ((Algebra.lsmul R R M : (a : A) → End R M) a)) x)
                  ((OrderIso.symm (Submodule.orderIsoMapComap (of R M a)) :
                      (a : Submodule R (AEval R M a)) → Submodule R M)
                    (Submodule.restrictScalars R q))
                  ⋯ :
                ↥(End.invtSubmodule ((Algebra.lsmul R R M : (a : A) → End R M) a))))
            ((fun (p : ↥(End.invtSubmodule ((Algebra.lsmul R R M : (a : A) → End R M) a))) ↦
                let __AddSubmonoid : AddSubmonoid (AEval R M a) :=
                  AddSubmonoid.map (F := M ≃ₗ[R] AEval R M a) (of R M a) (↑p : Submodule R M).toAddSubmonoid;
                { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ : Submodule.{u_1, u_3} R[X] (AEval R M a) })
              p)) :
        Submodule R M)
      x ↔
    x ∈ (↑p : Submodule R M)

Tactic:
simp
-- 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
q : Submodule.{u_1, u_3} R[X] (AEval R M a)
h :
  ∀ (x : AEval R M a),
    Membership.mem (γ := Submodule.{u_1, u_3} R[X] (AEval R M a))
        ((fun (p : ↥(End.invtSubmodule ((Algebra.lsmul R R M : (a : A) → End R M) a))) ↦
            let __AddSubmonoid : AddSubmonoid (AEval R M a) :=
              AddSubmonoid.map (F := M ≃ₗ[R] AEval R M a) (of R M a) (↑p : Submodule R M).toAddSubmonoid;
            { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ : Submodule.{u_1, u_3} R[X] (AEval R M a) })
          ((fun (q : Submodule.{u_1, u_3} R[X] (AEval R M a)) ↦
              (Subtype.mk (p := fun (x : Submodule R M) ↦
                  Membership.mem (γ := Sublattice (Submodule R M))
                    (End.invtSubmodule ((Algebra.lsmul R R M : (a : A) → End R M) a)) x)
                  ((OrderIso.symm (Submodule.orderIsoMapComap (of R M a)) :
                      (a : Submodule R (AEval R M a)) → Submodule R M)
                    (Submodule.restrictScalars R q))
                  ⋯ :
                ↥(End.invtSubmodule ((Algebra.lsmul R R M : (a : A) → End R M) a))))
            q))
        x ↔
      x ∈ q
⊢ (fun (p : ↥(End.invtSubmodule ((Algebra.lsmul R R M : (a : A) → End R M) a))) ↦
        let __AddSubmonoid : AddSubmonoid (AEval R M a) :=
          AddSubmonoid.map (F := M ≃ₗ[R] AEval R M a) (of R M a) (↑p : Submodule R M).toAddSubmonoid;
        { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ : Submodule.{u_1, u_3} R[X] (AEval R M a) })
      ((fun (q : Submodule.{u_1, u_3} R[X] (AEval R M a)) ↦
          (Subtype.mk (p := fun (x : Submodule R M) ↦
              Membership.mem (γ := Sublattice (Submodule R M))
                (End.invtSubmodule ((Algebra.lsmul R R M : (a : A) → End R M) a)) x)
              ((OrderIso.symm (Submodule.orderIsoMapComap (of R M a)) : (a : Submodule R (AEval R M a)) → Submodule R M)
                (Submodule.restrictScalars R q))
              ⋯ :
            ↥(End.invtSubmodule ((Algebra.lsmul R R M : (a : A) → End R M) a))))
        q) =
    q

Tactic:
ext
-- 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
q : Submodule.{u_1, u_3} R[X] (AEval R M a)
x : AEval R M a
⊢ Membership.mem (γ := Submodule.{u_1, u_3} R[X] (AEval R M a))
      ((fun (p : ↥(End.invtSubmodule ((Algebra.lsmul R R M : (a : A) → End R M) a))) ↦
          let __AddSubmonoid : AddSubmonoid (AEval R M a) :=
            AddSubmonoid.map (F := M ≃ₗ[R] AEval R M a) (of R M a) (↑p : Submodule R M).toAddSubmonoid;
          { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ : Submodule.{u_1, u_3} R[X] (AEval R M a) })
        ((fun (q : Submodule.{u_1, u_3} R[X] (AEval R M a)) ↦
            (Subtype.mk (p := fun (x : Submodule R M) ↦
                Membership.mem (γ := Sublattice (Submodule R M))
                  (End.invtSubmodule ((Algebra.lsmul R R M : (a : A) → End R M) a)) x)
                ((OrderIso.symm (Submodule.orderIsoMapComap (of R M a)) :
                    (a : Submodule R (AEval R M a)) → Submodule R M)
                  (Submodule.restrictScalars R q))
                ⋯ :
              ↥(End.invtSubmodule ((Algebra.lsmul R R M : (a : A) → End R M) a))))
          q))
      x ↔
    x ∈ q

Tactic:
aesop
-- 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
p p' : ↥(End.invtSubmodule ((Algebra.lsmul R R M : (a : A) → End R M) a))
h :
  LE.le (α := Submodule.{u_1, u_3} R[X] (AEval R M a))
    (({
            toFun := fun (p : ↥(End.invtSubmodule ((Algebra.lsmul R R M : (a : A) → End R M) a))) ↦
              let __AddSubmonoid : AddSubmonoid (AEval R M a) :=
                AddSubmonoid.map (F := M ≃ₗ[R] AEval R M a) (of R M a) (↑p : Submodule R M).toAddSubmonoid;
              { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ },
            invFun := fun (q : Submodule.{u_1, u_3} R[X] (AEval R M a)) ↦
              Subtype.mk (p := fun (x : Submodule R M) ↦
                Membership.mem (γ := Sublattice (Submodule R M))
                  (End.invtSubmodule ((Algebra.lsmul R R M : (a : A) → End R M) a)) x)
                ((OrderIso.symm (Submodule.orderIsoMapComap (of R M a)) :
                    (a : Submodule R (AEval R M a)) → Submodule R M)
                  (Submodule.restrictScalars R q))
                ⋯,
            left_inv := ⋯, right_inv := ⋯ } :
          (a_1 : ↥((Algebra.lsmul R R M : (a : A) → End R M) a).invtSubmodule) → Submodule R[X] (AEval R M a))
        p :
      Submodule.{u_1, u_3} R[X] (AEval R M a))
    (({
            toFun := fun (p : ↥(End.invtSubmodule ((Algebra.lsmul R R M : (a : A) → End R M) a))) ↦
              let __AddSubmonoid : AddSubmonoid (AEval R M a) :=
                AddSubmonoid.map (F := M ≃ₗ[R] AEval R M a) (of R M a) (↑p : Submodule R M).toAddSubmonoid;
              { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ },
            invFun := fun (q : Submodule.{u_1, u_3} R[X] (AEval R M a)) ↦
              Subtype.mk (p := fun (x : Submodule R M) ↦
                Membership.mem (γ := Sublattice (Submodule R M))
                  (End.invtSubmodule ((Algebra.lsmul R R M : (a : A) → End R M) a)) x)
                ((OrderIso.symm (Submodule.orderIsoMapComap (of R M a)) :
                    (a : Submodule R (AEval R M a)) → Submodule R M)
                  (Submodule.restrictScalars R q))
                ⋯,
            left_inv := ⋯, right_inv := ⋯ } :
          (a_1 : ↥((Algebra.lsmul R R M : (a : A) → End R M) a).invtSubmodule) → Submodule R[X] (AEval R M a))
        p' :
      Submodule.{u_1, u_3} R[X] (AEval R M a))
x : M
hx : x ∈ (↑p : Submodule R M)
⊢ x ∈ (↑p' : Submodule R M)

Tactic:
aesop (rule_sets := [SetLike!])
-- 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
p p' : ↥(End.invtSubmodule ((Algebra.lsmul R R M : (a : A) → End R M) a))
h : p ≤ p'
x : AEval R M a
hx :
  Membership.mem (γ := Submodule.{u_1, u_3} R[X] (AEval R M a))
    (({
            toFun := fun (p : ↥(End.invtSubmodule ((Algebra.lsmul R R M : (a : A) → End R M) a))) ↦
              let __AddSubmonoid : AddSubmonoid (AEval R M a) :=
                AddSubmonoid.map (F := M ≃ₗ[R] AEval R M a) (of R M a) (↑p : Submodule R M).toAddSubmonoid;
              { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ },
            invFun := fun (q : Submodule.{u_1, u_3} R[X] (AEval R M a)) ↦
              Subtype.mk (p := fun (x : Submodule R M) ↦
                Membership.mem (γ := Sublattice (Submodule R M))
                  (End.invtSubmodule ((Algebra.lsmul R R M : (a : A) → End R M) a)) x)
                ((OrderIso.symm (Submodule.orderIsoMapComap (of R M a)) :
                    (a : Submodule R (AEval R M a)) → Submodule R M)
                  (Submodule.restrictScalars R q))
                ⋯,
            left_inv := ⋯, right_inv := ⋯ } :
          (a_1 : ↥((Algebra.lsmul R R M : (a : A) → End R M) a).invtSubmodule) → Submodule R[X] (AEval R M a))
        p :
      Submodule.{u_1, u_3} R[X] (AEval R M a))
    x
⊢ Membership.mem (γ := Submodule.{u_1, u_3} R[X] (AEval R M a))
    (({
            toFun := fun (p : ↥(End.invtSubmodule ((Algebra.lsmul R R M : (a : A) → End R M) a))) ↦
              let __AddSubmonoid : AddSubmonoid (AEval R M a) :=
                AddSubmonoid.map (F := M ≃ₗ[R] AEval R M a) (of R M a) (↑p : Submodule R M).toAddSubmonoid;
              { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ },
            invFun := fun (q : Submodule.{u_1, u_3} R[X] (AEval R M a)) ↦
              Subtype.mk (p := fun (x : Submodule R M) ↦
                Membership.mem (γ := Sublattice (Submodule R M))
                  (End.invtSubmodule ((Algebra.lsmul R R M : (a : A) → End R M) a)) x)
                ((OrderIso.symm (Submodule.orderIsoMapComap (of R M a)) :
                    (a : Submodule R (AEval R M a)) → Submodule R M)
                  (Submodule.restrictScalars R q))
                ⋯,
            left_inv := ⋯, right_inv := ⋯ } :
          (a_1 : ↥((Algebra.lsmul R R M : (a : A) → End R M) a).invtSubmodule) → Submodule R[X] (AEval R M a))
        p' :
      Submodule.{u_1, u_3} R[X] (AEval R M a))
    x

Tactic:
aesop
-- 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
p : ↥(End.invtSubmodule ((Algebra.lsmul R R M : (a : A) → End R M) a))
m : AEval R M a
⊢ Membership.mem (γ := Submodule.{u_2, u_1} R[X] (AEval R M a))
      ((mapSubmodule R M a :
            (a_1 : ↥((Algebra.lsmul R R M : (a : A) → End R M) a).invtSubmodule) → Submodule R[X] (AEval R M a))
          p :
        Submodule.{u_2, u_1} R[X] (AEval R M a))
      m ↔
    Membership.mem (α := M) (↑p : Submodule R M) ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) m : M)

Tactic:
⟨fun ⟨_, hm, hm'⟩ ↦ hm'.symm ▸ hm, fun hm ↦ ⟨(of R M a).symm m, hm, rfl⟩⟩

Premises used: LinearEquiv.symm, Module.AEval.of, Membership.mem, Eq.rec, And.intro, Iff.intro, Exists.intro, Eq.symm, Subtype.val, DFunLike.coe, _private.0.Module.AEval.mem_mapSubmodule_apply.match_1, 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
q : Submodule.{u_1, u_2} R[X] (AEval R M a)
m : M
⊢ Membership.mem (γ := Submodule R M)
      (↑((OrderIso.symm (mapSubmodule R M a) :
              (a_1 : Submodule R[X] (AEval R M a)) → ↥((Algebra.lsmul R R M : (a : A) → End R M) a).invtSubmodule)
            q) :
        Submodule R M)
      m ↔
    Membership.mem (α := AEval R M a) q ((of R M a : (a_1 : M) → AEval R M a) m : AEval R M a)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- 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
p : Submodule R M
hp :
  Membership.mem (γ := Sublattice (Submodule R M)) (End.invtSubmodule ((Algebra.lsmul R R M : (a : A) → End R M) a)) p
x : ↥p
⊢ Membership.mem (α := AEval R M a) (γ := Submodule.{u_1, u_3} R[X] (AEval R M a))
    ((mapSubmodule R M a :
          (a_1 : ↥((Algebra.lsmul R R M : (a : A) → End R M) a).invtSubmodule) → Submodule R[X] (AEval R M a))
        (Subtype.mk (p := fun (x : Submodule R M) ↦
          Membership.mem (γ := Sublattice (Submodule R M))
            (End.invtSubmodule ((Algebra.lsmul R R M : (a : A) → End R M) a)) x)
          p hp) :
      Submodule.{u_1, u_3} R[X] (AEval R M a))
    ((of R M a : (a_1 : M) → AEval R M a) (↑x : M) : AEval R M a)

Tactic:
simp