awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Submodule
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
p : ↥ρ.invtSubmodule
x : k[G]
v : V
hv : v ∈ (↑p : Submodule k V)
⊢ Membership.mem (α := V) (↑p : Submodule k V)
    ((ρ.asModuleEquiv : (a : ρ.asModule) → V)
        (HSMul.hSMul (β := ρ.asModule) x ((ρ.asModuleEquiv.symm : (a : V) → ρ.asModule) v : ρ.asModule)) :
      V)

Tactic:
simpa using ρ.asAlgebraHom_mem_of_forall_mem p (ρ.mem_invtSubmodule.mp p.property) v hv x

Premises used: Iff.mp, Subtype.val, Representation.asAlgebraHom_mem_of_forall_mem, Representation.mem_invtSubmodule, Subtype.property
-- Module: Mathlib.RepresentationTheory.Submodule
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
q : Submodule k[G] ρ.asModule
rw :
  ∀ (i : G),
    Membership.mem (α := Submodule k V) (γ := Sublattice (Submodule k V))
      (Module.End.invtSubmodule ((ρ : (a : G) → V →ₗ[k] V) i))
      (((Submodule.orderIsoMapComap ρ.asModuleEquiv.symm).symm : (a : Submodule k ρ.asModule) → Submodule k V)
          (Submodule.restrictScalars k q) :
        Submodule k V)
⊢ Membership.mem (α := Submodule k V) ρ.invtSubmodule
    (((Submodule.orderIsoMapComap ρ.asModuleEquiv.symm).symm : (a : Submodule k ρ.asModule) → Submodule k V)
        (Submodule.restrictScalars k q) :
      Submodule k V)

Tactic:
rw [invtSubmodule, Sublattice.mem_iInf]

Premises used: Representation.invtSubmodule, Sublattice.mem_iInf
-- Module: Mathlib.RepresentationTheory.Submodule
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
q : Submodule k[G] ρ.asModule
g : G
v : V
hv :
  Membership.mem (γ := Submodule k V)
    (((Submodule.orderIsoMapComap ρ.asModuleEquiv.symm).symm : (a : Submodule k ρ.asModule) → Submodule k V)
        (Submodule.restrictScalars k q) :
      Submodule k V)
    v
simp :
  ∀
    (hv :
      Membership.mem (α := ρ.asModule) (γ := Submodule k ρ.asModule) (Submodule.restrictScalars k q)
        (((↑ρ.asModuleEquiv.symm : V →ₗ[k] ρ.asModule) : (a : V) → ρ.asModule) v : ρ.asModule)),
    Membership.mem (α := ρ.asModule) (γ := Submodule k ρ.asModule) (Submodule.restrictScalars k q)
      (((↑ρ.asModuleEquiv.symm : V →ₗ[k] ρ.asModule) : (a : V) → ρ.asModule)
          ((((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) v : V) :
        ρ.asModule)
⊢ Membership.mem (γ := Submodule k V)
    (Submodule.comap (R₂ := k) (M₂ := V) (σ₁₂ := RingHom.id k) ((ρ : (a : G) → V →ₗ[k] V) g)
      (((Submodule.orderIsoMapComap ρ.asModuleEquiv.symm).symm : (a : Submodule k ρ.asModule) → Submodule k V)
        (Submodule.restrictScalars k q)))
    v

Tactic:
simp only [Submodule.orderIsoMapComap_symm_apply, Submodule.mem_comap] at hv ⊢

Premises used: Submodule.mem_comap, Submodule.orderIsoMapComap_symm_apply
-- Module: Mathlib.RepresentationTheory.Submodule
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
q : Submodule k[G] ρ.asModule
g : G
v : V
hv :
  Membership.mem (α := ρ.asModule) (γ := Submodule k ρ.asModule) (Submodule.restrictScalars k q)
    (((↑ρ.asModuleEquiv.symm : V →ₗ[k] ρ.asModule) : (a : V) → ρ.asModule) v : ρ.asModule)
⊢ HSMul.hSMul (α := k[G]) (β := ρ.asModule) ((MonoidAlgebra.of k G : (a : G) → k[G]) g : k[G])
      (((↑ρ.asModuleEquiv.symm : V →ₗ[k] ρ.asModule) : (a : V) → ρ.asModule) v : ρ.asModule) ∈
    q

Tactic:
q.smul_mem (MonoidAlgebra.of k G g) hv

Premises used: MonoidAlgebra.of, DFunLike.coe, Submodule.smul_mem
-- Module: Mathlib.RepresentationTheory.Submodule
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
q : Submodule k[G] ρ.asModule
g : G
v : V
hv :
  Membership.mem (α := ρ.asModule) (γ := Submodule k ρ.asModule) (Submodule.restrictScalars k q)
    (((↑ρ.asModuleEquiv.symm : V →ₗ[k] ρ.asModule) : (a : V) → ρ.asModule) v : ρ.asModule)
h :
  ((↑ρ.asModuleEquiv.symm : V →ₗ[k] ρ.asModule) : (a : V) → ρ.asModule)
      ((((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) v : V) =
    HSMul.hSMul (α := k[G]) (β := ρ.asModule) ((MonoidAlgebra.of k G : (a : G) → k[G]) g : k[G])
      (((↑ρ.asModuleEquiv.symm : V →ₗ[k] ρ.asModule) : (a : V) → ρ.asModule) v : ρ.asModule)
⊢ Membership.mem (α := ρ.asModule) (γ := Submodule k ρ.asModule) (Submodule.restrictScalars k q)
    (((↑ρ.asModuleEquiv.symm : V →ₗ[k] ρ.asModule) : (a : V) → ρ.asModule)
        ((((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) v : V) :
      ρ.asModule)

Tactic:
convert! q.smul_mem (MonoidAlgebra.of k G g) hv using 1

Premises used: MonoidAlgebra.of, DFunLike.coe, Submodule.smul_mem
-- Module: Mathlib.RepresentationTheory.Submodule
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
q : Submodule k[G] ρ.asModule
g : G
v : V
hv :
  Membership.mem (α := ρ.asModule) (γ := Submodule k ρ.asModule) (Submodule.restrictScalars k q)
    (((↑ρ.asModuleEquiv.symm : V →ₗ[k] ρ.asModule) : (a : V) → ρ.asModule) v : ρ.asModule)
h :
  (ρ.asModuleEquiv.symm : (a : V) → ρ.asModule) ((((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) v : V) =
    HSMul.hSMul (α := k[G]) (β := ρ.asModule) ((MonoidAlgebra.of k G : (a : G) → k[G]) g : k[G])
      ((ρ.asModuleEquiv.symm : (a : V) → ρ.asModule) v : ρ.asModule)
h₁ h₂ :
  Eq (α := ρ.asModule)
    ((ρ.asModuleEquiv.symm : (a : V) → ρ.asModule) ((((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) v : V) :
      ρ.asModule)
    ((ρ.asModuleEquiv.symm : (a : V) → ρ.asModule) ((((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) v : V) :
      ρ.asModule)
⊢ ((↑ρ.asModuleEquiv.symm : V →ₗ[k] ρ.asModule) : (a : V) → ρ.asModule)
      ((((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) v : V) =
    HSMul.hSMul (α := k[G]) (β := ρ.asModule) ((MonoidAlgebra.of k G : (a : G) → k[G]) g : k[G])
      (((↑ρ.asModuleEquiv.symm : V →ₗ[k] ρ.asModule) : (a : V) → ρ.asModule) v : ρ.asModule)

Tactic:
rw [LinearEquiv.coe_coe, ← asModuleEquiv_symm_map_rho]

Premises used: Representation.asModuleEquiv_symm_map_rho, LinearEquiv.coe_coe
-- Module: Mathlib.RepresentationTheory.Submodule
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
p : ↥ρ.invtSubmodule
a :
  ∀ (x : V),
    Membership.mem (γ := Submodule k V)
        (↑((fun (q : Submodule k[G] ρ.asModule) ↦
                (Subtype.mk (p := fun (x : Submodule k V) ↦ x ∈ ρ.invtSubmodule)
                    (((Submodule.orderIsoMapComap ρ.asModuleEquiv.symm).symm :
                        (a : Submodule k ρ.asModule) → Submodule k V)
                      (Submodule.restrictScalars k q))
                    ⋯ :
                  ↥ρ.invtSubmodule))
              ((fun (p : ↥ρ.invtSubmodule) ↦
                  let __AddSubmonoid : AddSubmonoid ρ.asModule :=
                    AddSubmonoid.map ρ.asModuleEquiv.symm (↑p : Submodule k V).toAddSubmonoid;
                  { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ : Submodule k[G] ρ.asModule })
                p)) :
          Submodule k V)
        x ↔
      x ∈ (↑p : Submodule k V)
⊢ (fun (q : Submodule k[G] ρ.asModule) ↦
        (Subtype.mk (p := fun (x : Submodule k V) ↦ x ∈ ρ.invtSubmodule)
            (((Submodule.orderIsoMapComap ρ.asModuleEquiv.symm).symm : (a : Submodule k ρ.asModule) → Submodule k V)
              (Submodule.restrictScalars k q))
            ⋯ :
          ↥ρ.invtSubmodule))
      ((fun (p : ↥ρ.invtSubmodule) ↦
          let __AddSubmonoid : AddSubmonoid ρ.asModule :=
            AddSubmonoid.map ρ.asModuleEquiv.symm (↑p : Submodule k V).toAddSubmonoid;
          { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ : Submodule k[G] ρ.asModule })
        p) =
    p

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Submodule
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
p : ↥ρ.invtSubmodule
x : V
⊢ Membership.mem (γ := Submodule k V)
      (↑((fun (q : Submodule k[G] ρ.asModule) ↦
              (Subtype.mk (p := fun (x : Submodule k V) ↦ x ∈ ρ.invtSubmodule)
                  (((Submodule.orderIsoMapComap ρ.asModuleEquiv.symm).symm :
                      (a : Submodule k ρ.asModule) → Submodule k V)
                    (Submodule.restrictScalars k q))
                  ⋯ :
                ↥ρ.invtSubmodule))
            ((fun (p : ↥ρ.invtSubmodule) ↦
                let __AddSubmonoid : AddSubmonoid ρ.asModule :=
                  AddSubmonoid.map ρ.asModuleEquiv.symm (↑p : Submodule k V).toAddSubmonoid;
                { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ : Submodule k[G] ρ.asModule })
              p)) :
        Submodule k V)
      x ↔
    x ∈ (↑p : Submodule k V)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Submodule
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
q : Submodule k[G] ρ.asModule
h :
  ∀ (x : ρ.asModule),
    Membership.mem (γ := Submodule k[G] ρ.asModule)
        ((fun (p : ↥ρ.invtSubmodule) ↦
            let __AddSubmonoid : AddSubmonoid ρ.asModule :=
              AddSubmonoid.map ρ.asModuleEquiv.symm (↑p : Submodule k V).toAddSubmonoid;
            { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ : Submodule k[G] ρ.asModule })
          ((fun (q : Submodule k[G] ρ.asModule) ↦
              (Subtype.mk (p := fun (x : Submodule k V) ↦ x ∈ ρ.invtSubmodule)
                  (((Submodule.orderIsoMapComap ρ.asModuleEquiv.symm).symm :
                      (a : Submodule k ρ.asModule) → Submodule k V)
                    (Submodule.restrictScalars k q))
                  ⋯ :
                ↥ρ.invtSubmodule))
            q))
        x ↔
      x ∈ q
⊢ (fun (p : ↥ρ.invtSubmodule) ↦
        let __AddSubmonoid : AddSubmonoid ρ.asModule :=
          AddSubmonoid.map ρ.asModuleEquiv.symm (↑p : Submodule k V).toAddSubmonoid;
        { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ : Submodule k[G] ρ.asModule })
      ((fun (q : Submodule k[G] ρ.asModule) ↦
          (Subtype.mk (p := fun (x : Submodule k V) ↦ x ∈ ρ.invtSubmodule)
              (((Submodule.orderIsoMapComap ρ.asModuleEquiv.symm).symm : (a : Submodule k ρ.asModule) → Submodule k V)
                (Submodule.restrictScalars k q))
              ⋯ :
            ↥ρ.invtSubmodule))
        q) =
    q

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Submodule
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
q : Submodule k[G] ρ.asModule
x : ρ.asModule
⊢ Membership.mem (γ := Submodule k[G] ρ.asModule)
      ((fun (p : ↥ρ.invtSubmodule) ↦
          let __AddSubmonoid : AddSubmonoid ρ.asModule :=
            AddSubmonoid.map ρ.asModuleEquiv.symm (↑p : Submodule k V).toAddSubmonoid;
          { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ : Submodule k[G] ρ.asModule })
        ((fun (q : Submodule k[G] ρ.asModule) ↦
            (Subtype.mk (p := fun (x : Submodule k V) ↦ x ∈ ρ.invtSubmodule)
                (((Submodule.orderIsoMapComap ρ.asModuleEquiv.symm).symm : (a : Submodule k ρ.asModule) → Submodule k V)
                  (Submodule.restrictScalars k q))
                ⋯ :
              ↥ρ.invtSubmodule))
          q))
      x ↔
    x ∈ q

Tactic:
aesop
-- Module: Mathlib.RepresentationTheory.Submodule
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
p q : ↥ρ.invtSubmodule
h :
  LE.le (α := Submodule k[G] ρ.asModule)
    (({
            toFun := fun (p : ↥ρ.invtSubmodule) ↦
              let __AddSubmonoid : AddSubmonoid ρ.asModule :=
                AddSubmonoid.map ρ.asModuleEquiv.symm (↑p : Submodule k V).toAddSubmonoid;
              { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ },
            invFun := fun (q : Submodule k[G] ρ.asModule) ↦
              Subtype.mk (p := fun (x : Submodule k V) ↦ x ∈ ρ.invtSubmodule)
                (((Submodule.orderIsoMapComap ρ.asModuleEquiv.symm).symm : (a : Submodule k ρ.asModule) → Submodule k V)
                  (Submodule.restrictScalars k q))
                ⋯,
            left_inv := ⋯, right_inv := ⋯ } :
          (a : ↥ρ.invtSubmodule) → Submodule k[G] ρ.asModule)
        p :
      Submodule k[G] ρ.asModule)
    (({
            toFun := fun (p : ↥ρ.invtSubmodule) ↦
              let __AddSubmonoid : AddSubmonoid ρ.asModule :=
                AddSubmonoid.map ρ.asModuleEquiv.symm (↑p : Submodule k V).toAddSubmonoid;
              { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ },
            invFun := fun (q : Submodule k[G] ρ.asModule) ↦
              Subtype.mk (p := fun (x : Submodule k V) ↦ x ∈ ρ.invtSubmodule)
                (((Submodule.orderIsoMapComap ρ.asModuleEquiv.symm).symm : (a : Submodule k ρ.asModule) → Submodule k V)
                  (Submodule.restrictScalars k q))
                ⋯,
            left_inv := ⋯, right_inv := ⋯ } :
          (a : ↥ρ.invtSubmodule) → Submodule k[G] ρ.asModule)
        q :
      Submodule k[G] ρ.asModule)
x : V
hx : x ∈ (↑p : Submodule k V)
this :
  Membership.mem (α := ρ.asModule) (γ := AddSubmonoid ρ.asModule)
    (AddSubmonoid.map ρ.asModuleEquiv.symm (↑q : Submodule k V).toAddSubmonoid)
    ((ρ.asModuleEquiv.symm : (a : V) → ρ.asModule) x : ρ.asModule)
⊢ x ∈ (↑q : Submodule k V)

Tactic:
simpa using this
-- Module: Mathlib.RepresentationTheory.Submodule
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
p q : ↥ρ.invtSubmodule
h :
  LE.le (α := Submodule k[G] ρ.asModule)
    (({
            toFun := fun (p : ↥ρ.invtSubmodule) ↦
              let __AddSubmonoid : AddSubmonoid ρ.asModule :=
                AddSubmonoid.map ρ.asModuleEquiv.symm (↑p : Submodule k V).toAddSubmonoid;
              { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ },
            invFun := fun (q : Submodule k[G] ρ.asModule) ↦
              Subtype.mk (p := fun (x : Submodule k V) ↦ x ∈ ρ.invtSubmodule)
                (((Submodule.orderIsoMapComap ρ.asModuleEquiv.symm).symm : (a : Submodule k ρ.asModule) → Submodule k V)
                  (Submodule.restrictScalars k q))
                ⋯,
            left_inv := ⋯, right_inv := ⋯ } :
          (a : ↥ρ.invtSubmodule) → Submodule k[G] ρ.asModule)
        p :
      Submodule k[G] ρ.asModule)
    (({
            toFun := fun (p : ↥ρ.invtSubmodule) ↦
              let __AddSubmonoid : AddSubmonoid ρ.asModule :=
                AddSubmonoid.map ρ.asModuleEquiv.symm (↑p : Submodule k V).toAddSubmonoid;
              { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ },
            invFun := fun (q : Submodule k[G] ρ.asModule) ↦
              Subtype.mk (p := fun (x : Submodule k V) ↦ x ∈ ρ.invtSubmodule)
                (((Submodule.orderIsoMapComap ρ.asModuleEquiv.symm).symm : (a : Submodule k ρ.asModule) → Submodule k V)
                  (Submodule.restrictScalars k q))
                ⋯,
            left_inv := ⋯, right_inv := ⋯ } :
          (a : ↥ρ.invtSubmodule) → Submodule k[G] ρ.asModule)
        q :
      Submodule k[G] ρ.asModule)
x : V
hx : x ∈ (↑p : Submodule k V)
suffices :
  Membership.mem (α := ρ.asModule) (γ := AddSubmonoid ρ.asModule)
    (AddSubmonoid.map ρ.asModuleEquiv.symm (↑q : Submodule k V).toAddSubmonoid)
    ((ρ.asModuleEquiv.symm : (a : V) → ρ.asModule) x : ρ.asModule)
⊢ x ∈ (↑q : Submodule k V)

Tactic:
suffices ρ.asModuleEquiv.symm x ∈
        (q : Submodule k V).toAddSubmonoid.map ρ.asModuleEquiv.symm by simpa using this
-- Module: Mathlib.RepresentationTheory.Submodule
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
p q : ↥ρ.invtSubmodule
h :
  LE.le (α := Submodule k[G] ρ.asModule)
    (({
            toFun := fun (p : ↥ρ.invtSubmodule) ↦
              let __AddSubmonoid : AddSubmonoid ρ.asModule :=
                AddSubmonoid.map ρ.asModuleEquiv.symm (↑p : Submodule k V).toAddSubmonoid;
              { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ },
            invFun := fun (q : Submodule k[G] ρ.asModule) ↦
              Subtype.mk (p := fun (x : Submodule k V) ↦ x ∈ ρ.invtSubmodule)
                (((Submodule.orderIsoMapComap ρ.asModuleEquiv.symm).symm : (a : Submodule k ρ.asModule) → Submodule k V)
                  (Submodule.restrictScalars k q))
                ⋯,
            left_inv := ⋯, right_inv := ⋯ } :
          (a : ↥ρ.invtSubmodule) → Submodule k[G] ρ.asModule)
        p :
      Submodule k[G] ρ.asModule)
    (({
            toFun := fun (p : ↥ρ.invtSubmodule) ↦
              let __AddSubmonoid : AddSubmonoid ρ.asModule :=
                AddSubmonoid.map ρ.asModuleEquiv.symm (↑p : Submodule k V).toAddSubmonoid;
              { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ },
            invFun := fun (q : Submodule k[G] ρ.asModule) ↦
              Subtype.mk (p := fun (x : Submodule k V) ↦ x ∈ ρ.invtSubmodule)
                (((Submodule.orderIsoMapComap ρ.asModuleEquiv.symm).symm : (a : Submodule k ρ.asModule) → Submodule k V)
                  (Submodule.restrictScalars k q))
                ⋯,
            left_inv := ⋯, right_inv := ⋯ } :
          (a : ↥ρ.invtSubmodule) → Submodule k[G] ρ.asModule)
        q :
      Submodule k[G] ρ.asModule)
x : V
hx : x ∈ (↑p : Submodule k V)
⊢ Membership.mem (α := ρ.asModule) (γ := Submodule k[G] ρ.asModule)
    (({
            toFun := fun (p : ↥ρ.invtSubmodule) ↦
              let __AddSubmonoid : AddSubmonoid ρ.asModule :=
                AddSubmonoid.map ρ.asModuleEquiv.symm (↑p : Submodule k V).toAddSubmonoid;
              { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ },
            invFun := fun (q : Submodule k[G] ρ.asModule) ↦
              Subtype.mk (p := fun (x : Submodule k V) ↦ x ∈ ρ.invtSubmodule)
                (((Submodule.orderIsoMapComap ρ.asModuleEquiv.symm).symm : (a : Submodule k ρ.asModule) → Submodule k V)
                  (Submodule.restrictScalars k q))
                ⋯,
            left_inv := ⋯, right_inv := ⋯ } :
          (a : ↥ρ.invtSubmodule) → Submodule k[G] ρ.asModule)
        p :
      Submodule k[G] ρ.asModule)
    ((ρ.asModuleEquiv.symm : (a : V) → ρ.asModule) x : ρ.asModule)

Tactic:
simpa using hx
-- Module: Mathlib.RepresentationTheory.Submodule
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
p q : ↥ρ.invtSubmodule
h :
  LE.le (α := Submodule k[G] ρ.asModule)
    (({
            toFun := fun (p : ↥ρ.invtSubmodule) ↦
              let __AddSubmonoid : AddSubmonoid ρ.asModule :=
                AddSubmonoid.map ρ.asModuleEquiv.symm (↑p : Submodule k V).toAddSubmonoid;
              { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ },
            invFun := fun (q : Submodule k[G] ρ.asModule) ↦
              Subtype.mk (p := fun (x : Submodule k V) ↦ x ∈ ρ.invtSubmodule)
                (((Submodule.orderIsoMapComap ρ.asModuleEquiv.symm).symm : (a : Submodule k ρ.asModule) → Submodule k V)
                  (Submodule.restrictScalars k q))
                ⋯,
            left_inv := ⋯, right_inv := ⋯ } :
          (a : ↥ρ.invtSubmodule) → Submodule k[G] ρ.asModule)
        p :
      Submodule k[G] ρ.asModule)
    (({
            toFun := fun (p : ↥ρ.invtSubmodule) ↦
              let __AddSubmonoid : AddSubmonoid ρ.asModule :=
                AddSubmonoid.map ρ.asModuleEquiv.symm (↑p : Submodule k V).toAddSubmonoid;
              { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ },
            invFun := fun (q : Submodule k[G] ρ.asModule) ↦
              Subtype.mk (p := fun (x : Submodule k V) ↦ x ∈ ρ.invtSubmodule)
                (((Submodule.orderIsoMapComap ρ.asModuleEquiv.symm).symm : (a : Submodule k ρ.asModule) → Submodule k V)
                  (Submodule.restrictScalars k q))
                ⋯,
            left_inv := ⋯, right_inv := ⋯ } :
          (a : ↥ρ.invtSubmodule) → Submodule k[G] ρ.asModule)
        q :
      Submodule k[G] ρ.asModule)
x : V
hx : x ∈ (↑p : Submodule k V)
⊢ Membership.mem (α := ρ.asModule) (γ := AddSubmonoid ρ.asModule)
    (AddSubmonoid.map ρ.asModuleEquiv.symm (↑q : Submodule k V).toAddSubmonoid)
    ((ρ.asModuleEquiv.symm : (a : V) → ρ.asModule) x : ρ.asModule)

Tactic:
exact h <| by simpa using hx
-- Module: Mathlib.RepresentationTheory.Submodule
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : CommSemiring k
inst_1 : Monoid G
inst_2 : AddCommMonoid V
inst_3 : Module k V
ρ : Representation k G V
p q : ↥ρ.invtSubmodule
h : p ≤ q
x : ρ.asModule
hx :
  Membership.mem (γ := Submodule k[G] ρ.asModule)
    (({
            toFun := fun (p : ↥ρ.invtSubmodule) ↦
              let __AddSubmonoid : AddSubmonoid ρ.asModule :=
                AddSubmonoid.map ρ.asModuleEquiv.symm (↑p : Submodule k V).toAddSubmonoid;
              { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ },
            invFun := fun (q : Submodule k[G] ρ.asModule) ↦
              Subtype.mk (p := fun (x : Submodule k V) ↦ x ∈ ρ.invtSubmodule)
                (((Submodule.orderIsoMapComap ρ.asModuleEquiv.symm).symm : (a : Submodule k ρ.asModule) → Submodule k V)
                  (Submodule.restrictScalars k q))
                ⋯,
            left_inv := ⋯, right_inv := ⋯ } :
          (a : ↥ρ.invtSubmodule) → Submodule k[G] ρ.asModule)
        p :
      Submodule k[G] ρ.asModule)
    x
⊢ Membership.mem (γ := Submodule k[G] ρ.asModule)
    (({
            toFun := fun (p : ↥ρ.invtSubmodule) ↦
              let __AddSubmonoid : AddSubmonoid ρ.asModule :=
                AddSubmonoid.map ρ.asModuleEquiv.symm (↑p : Submodule k V).toAddSubmonoid;
              { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ },
            invFun := fun (q : Submodule k[G] ρ.asModule) ↦
              Subtype.mk (p := fun (x : Submodule k V) ↦ x ∈ ρ.invtSubmodule)
                (((Submodule.orderIsoMapComap ρ.asModuleEquiv.symm).symm : (a : Submodule k ρ.asModule) → Submodule k V)
                  (Submodule.restrictScalars k q))
                ⋯,
            left_inv := ⋯, right_inv := ⋯ } :
          (a : ↥ρ.invtSubmodule) → Submodule k[G] ρ.asModule)
        q :
      Submodule k[G] ρ.asModule)
    x

Tactic:
aesop
-- Module: Mathlib.RepresentationTheory.Subrepresentation
Goal:
A : Type u_1
G : Type u_2
W : Type u_3
inst : Semiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid W
inst_3 : Module A W
ρ : Representation A G W
toSubmodule : Submodule A W
apply_mem_toSubmodule :
  ∀ (g : G) ⦃v : W⦄,
    v ∈ toSubmodule →
      Membership.mem (α := W) toSubmodule ((((ρ : (a : G) → W →ₗ[A] W) g : W →ₗ[A] W) : (a : W) → W) v : W)
⊢ ∀ ⦃a₂ : Subrepresentation ρ⦄,
    { toSubmodule := toSubmodule, apply_mem_toSubmodule := apply_mem_toSubmodule : Subrepresentation ρ }.toSubmodule =
        a₂.toSubmodule →
      { toSubmodule := toSubmodule, apply_mem_toSubmodule := apply_mem_toSubmodule : Subrepresentation ρ } = a₂

Tactic:
congr!