awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Res (goal)
Goal:
k_1 : Type u
inst : Semiring k_1
G : Type v1
H : Type v2
inst_1 : Monoid G
inst_2 : Monoid H
f : H →* G
M : Rep k_1 G
k : Type u
inst_3 : CommSemiring k
X Y : Rep.{u_1, u, v1} k G
l : X ⟶ Y
r : k
hf :
  Representation.IntertwiningMap.toLinearMap (Hom.hom (CategoryTheory.Functor.map (resFunctor f) (r • l))) =
    (HSMul.hSMul (β := (Functor.obj (resFunctor f) X).ρ.IntertwiningMap (Functor.obj (resFunctor f) Y).ρ) r
        (Hom.hom (CategoryTheory.Functor.map (resFunctor f) l))).toLinearMap
hf₁ :
  Representation.IntertwiningMap.toLinearMap (Hom.hom (CategoryTheory.Functor.map (resFunctor f) (r • l))) =
    HSMul.hSMul (β := (↑(Functor.obj (resFunctor f) X) : Type u_1) →ₗ[k] (↑(Functor.obj (resFunctor f) Y) : Type u_1)) r
      (Representation.IntertwiningMap.toLinearMap (Hom.hom (CategoryTheory.Functor.map (resFunctor f) l)))
hf₂ :
  (Hom.hom (r • l)).toLinearMap =
    HSMul.hSMul (β := (↑(Functor.obj (resFunctor f) X) : Type u_1) →ₗ[k] (↑(Functor.obj (resFunctor f) Y) : Type u_1)) r
      (Representation.IntertwiningMap.toLinearMap (Hom.hom (CategoryTheory.Functor.map (resFunctor f) l)))
hf₃ :
  (r • Hom.hom l).toLinearMap =
    HSMul.hSMul (β := (↑(Functor.obj (resFunctor f) X) : Type u_1) →ₗ[k] (↑(Functor.obj (resFunctor f) Y) : Type u_1)) r
      (Representation.IntertwiningMap.toLinearMap (Hom.hom (CategoryTheory.Functor.map (resFunctor f) l)))
hf₄ :
  r • (Hom.hom l).toLinearMap =
    HSMul.hSMul (β := (↑(Functor.obj (resFunctor f) X) : Type u_1) →ₗ[k] (↑(Functor.obj (resFunctor f) Y) : Type u_1)) r
      (Representation.IntertwiningMap.toLinearMap (Hom.hom (CategoryTheory.Functor.map (resFunctor f) l)))
⊢ Representation.IntertwiningMap.toLinearMap (Hom.hom (CategoryTheory.Functor.map (resFunctor f) (r • l))) =
    (Hom.hom
        (HSMul.hSMul (β := Functor.obj (resFunctor f) X ⟶ Functor.obj (resFunctor f) Y) r
          (CategoryTheory.Functor.map (resFunctor f) l))).toLinearMap
have hf₅ : r • (Hom.hom l).toLinearMap = r • (Hom.hom l).toLinearMap
Tactic: rw [smul_hom, Representation.IntertwiningMap.toLinearMap_smul,
      res_map_hom_toLinearMap, smul_hom, Representation.IntertwiningMap.toLinearMap_smul,
      res_map_hom_toLinearMap]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Semisimple (goal)
Goal:
k : Type u_1
G : Type u_2
V : Type u_3
inst : Monoid G
inst_1 : Field k
inst_2 : AddCommGroup V
inst_3 : Module k V
ρ : Representation k G V
⊢ ρ.IsSemisimpleRepresentation ↔ IsSemisimpleModule k[G] ρ.asModule
have rw : ρ.IsSemisimpleRepresentation ↔ ComplementedLattice.{u_3} (Submodule k[G] ρ.asModule)
Tactic: rw [isSemisimpleModule_iff]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Semisimple (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Monoid G
inst_1 : Field k
M : Type u_4
inst_2 : AddCommGroup M
inst_3 : Module k[G] M
⊢ IsSemisimpleModule k[G] M ↔
    IsSemisimpleRepresentation.{u_1, u_2, u_4} (k := k) (G := G) (V := RestrictScalars k k[G] M) (ofModule M)
have rw : ComplementedLattice.{u_4} (Submodule k[G] M) ↔
  IsSemisimpleRepresentation.{u_1, u_2, u_4} (k := k) (G := G) (V := RestrictScalars k k[G] M) (ofModule M)
Tactic: rw [isSemisimpleModule_iff]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Submodule (goal)
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 : Submodule k V
⊢ p ∈ ρ.invtSubmodule ↔
    ∀ (g : G),
      Membership.mem (γ := Sublattice (Submodule k V)) (Module.End.invtSubmodule ((ρ : (a : G) → V →ₗ[k] V) g)) p
have rw : Membership.mem (γ := Sublattice (Submodule k V)) (⨅ (g : G), Module.End.invtSubmodule ((ρ : (a : G) → V →ₗ[k] V) g)) p ↔
  ∀ (g : G), Membership.mem (γ := Sublattice (Submodule k V)) (Module.End.invtSubmodule ((ρ : (a : G) → V →ₗ[k] V) g)) p
Tactic: rw [invtSubmodule, Sublattice.mem_iInf]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Submodule (goal)
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 : Submodule k V
rw :
  Membership.mem (γ := Sublattice (Submodule k V)) (⨅ (g : G), Module.End.invtSubmodule ((ρ : (a : G) → V →ₗ[k] V) g))
      p ↔
    ∀ (g : G),
      Membership.mem (γ := Sublattice (Submodule k V)) (Module.End.invtSubmodule ((ρ : (a : G) → V →ₗ[k] V) g)) p
⊢ p ∈ ρ.invtSubmodule ↔
    ∀ (g : G),
      Membership.mem (γ := Sublattice (Submodule k V)) (Module.End.invtSubmodule ((ρ : (a : G) → V →ₗ[k] V) g)) p
have rw₁ : (∀ (i : G),
    Membership.mem (γ := Sublattice (Submodule k V)) (Module.End.invtSubmodule ((ρ : (a : G) → V →ₗ[k] V) i)) p) ↔
  ∀ (g : G), Membership.mem (γ := Sublattice (Submodule k V)) (Module.End.invtSubmodule ((ρ : (a : G) → V →ₗ[k] V) g)) p
Tactic: rw [invtSubmodule, Sublattice.mem_iInf]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Submodule (goal)
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
⊢ Nontrivial.{u_3} ↥ρ.invtSubmodule ↔ Nontrivial V
have refine_1 : ∀ (h : Nontrivial.{u_3} ↥ρ.invtSubmodule), Nontrivial V
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RepresentationTheory.Submodule (goal)
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
refine_1 : ∀ (h : Nontrivial.{u_3} ↥ρ.invtSubmodule), Nontrivial V
⊢ Nontrivial.{u_3} ↥ρ.invtSubmodule ↔ Nontrivial V
have refine_2 : ∀ (h : Nontrivial V), Nontrivial.{u_3} ↥ρ.invtSubmodule
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RepresentationTheory.Submodule (goal)
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
h : Nontrivial.{u_3} ↥ρ.invtSubmodule
⊢ Nontrivial V
have refine_1 : ∀ (h : Subsingleton V), Subsingleton.{u_3 + 1} ↥ρ.invtSubmodule
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RepresentationTheory.Submodule (goal)
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
h : Nontrivial V
⊢ Nontrivial.{u_3} ↥ρ.invtSubmodule
have refine_2 : Ne.{u_3 + 1} (α := ↥ρ.invtSubmodule) ⊥ ⊤
Tactic: refine ⟨⊥, ⊤, ?_⟩
-- Lean 4 proof step from Mathlib.RepresentationTheory.Submodule (goal)
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
h : Nontrivial V
⊢ Ne.{u_3 + 1} (α := ↥ρ.invtSubmodule) ⊥ ⊤
have refine_2 : Ne.{u_3 + 1} (α := Submodule k V) ⊥ ⊤
Tactic: rw [← Subtype.coe_ne_coe, invtSubmodule.coe_top, invtSubmodule.coe_bot]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Submodule (goal)
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 : Submodule k V
hp : ∀ (g : G), ∀ v ∈ p, Membership.mem (α := V) p ((((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) v : V)
v : V
hv : v ∈ p
x : k[G]
⊢ Membership.mem (α := V) p ((((ρ.asAlgebraHom : (a : k[G]) → Module.End k V) x : Module.End k V) : (a : V) → V) v : V)
have hM : ∀ (m : G),
  Membership.mem (α := V) p
    ((((ρ.asAlgebraHom : (a : k[G]) → Module.End k V) ((MonoidAlgebra.of k G : (a : G) → k[G]) m) : Module.End k V) :
          (a : V) → V)
        v :
      V)
Tactic: apply x.induction_on
-- Lean 4 proof step from Mathlib.RepresentationTheory.Submodule (goal)
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 : Submodule k V
hp : ∀ (g : G), ∀ v ∈ p, Membership.mem (α := V) p ((((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) v : V)
v : V
hv : v ∈ p
x : k[G]
hM :
  ∀ (m : G),
    Membership.mem (α := V) p
      ((((ρ.asAlgebraHom : (a : k[G]) → Module.End k V) ((MonoidAlgebra.of k G : (a : G) → k[G]) m) : Module.End k V) :
            (a : V) → V)
          v :
        V)
⊢ Membership.mem (α := V) p ((((ρ.asAlgebraHom : (a : k[G]) → Module.End k V) x : Module.End k V) : (a : V) → V) v : V)
have hadd : ∀ (x y : k[G]),
  Membership.mem (α := V) p
      ((((ρ.asAlgebraHom : (a : k[G]) → Module.End k V) x : Module.End k V) : (a : V) → V) v : V) →
    Membership.mem (α := V) p
        ((((ρ.asAlgebraHom : (a : k[G]) → Module.End k V) y : Module.End k V) : (a : V) → V) v : V) →
      Membership.mem (α := V) p
        ((((ρ.asAlgebraHom : (a : k[G]) → Module.End k V) (x + y) : Module.End k V) : (a : V) → V) v : V)
Tactic: apply x.induction_on
-- Lean 4 proof step from Mathlib.RepresentationTheory.Submodule (goal)
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 : Submodule k V
hp : ∀ (g : G), ∀ v ∈ p, Membership.mem (α := V) p ((((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) v : V)
v : V
hv : v ∈ p
x : k[G]
hM :
  ∀ (m : G),
    Membership.mem (α := V) p
      ((((ρ.asAlgebraHom : (a : k[G]) → Module.End k V) ((MonoidAlgebra.of k G : (a : G) → k[G]) m) : Module.End k V) :
            (a : V) → V)
          v :
        V)
hadd :
  ∀ (x y : k[G]),
    Membership.mem (α := V) p
        ((((ρ.asAlgebraHom : (a : k[G]) → Module.End k V) x : Module.End k V) : (a : V) → V) v : V) →
      Membership.mem (α := V) p
          ((((ρ.asAlgebraHom : (a : k[G]) → Module.End k V) y : Module.End k V) : (a : V) → V) v : V) →
        Membership.mem (α := V) p
          ((((ρ.asAlgebraHom : (a : k[G]) → Module.End k V) (x + y) : Module.End k V) : (a : V) → V) v : V)
⊢ Membership.mem (α := V) p ((((ρ.asAlgebraHom : (a : k[G]) → Module.End k V) x : Module.End k V) : (a : V) → V) v : V)
have hsmul : ∀ (r : k) (x : k[G]),
  Membership.mem (α := V) p
      ((((ρ.asAlgebraHom : (a : k[G]) → Module.End k V) x : Module.End k V) : (a : V) → V) v : V) →
    Membership.mem (α := V) p
      ((((ρ.asAlgebraHom : (a : k[G]) → Module.End k V) (r • x) : Module.End k V) : (a : V) → V) v : V)
Tactic: apply x.induction_on
-- Lean 4 proof step from Mathlib.RepresentationTheory.Submodule (goal)
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
⊢ ∀ (c : k[G]) {x : ρ.asModule},
    x ∈
        AddSubsemigroup.carrier
          (AddSubmonoid.toAddSubsemigroup (AddSubmonoid.map ρ.asModuleEquiv.symm (↑p : Submodule k V).toAddSubmonoid)) →
      c • x ∈
        AddSubsemigroup.carrier
          (AddSubmonoid.toAddSubsemigroup (AddSubmonoid.map ρ.asModuleEquiv.symm (↑p : Submodule k V).toAddSubmonoid))
have simp : ∀ (c : k[G]),
  ∀ a ∈ (↑p : Submodule k V),
    ∃ x ∈ (↑p : Submodule k V),
      (ρ.asModuleEquiv.symm : (a : V) → ρ.asModule) x =
        HSMul.hSMul (β := ρ.asModule) c ((ρ.asModuleEquiv.symm : (a : V) → ρ.asModule) a : ρ.asModule)
Tactic: simp only [AddSubsemigroup.mem_carrier, AddSubmonoid.mem_toSubsemigroup,
          AddSubmonoid.mem_map, Submodule.mem_toAddSubmonoid, forall_exists_index, and_imp,
          forall_apply_eq_imp_iff₂]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Submodule (goal)
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
⊢ ∀ (c : k[G]),
    ∀ a ∈ (↑p : Submodule k V),
      ∃ x ∈ (↑p : Submodule k V),
        (ρ.asModuleEquiv.symm : (a : V) → ρ.asModule) x =
          HSMul.hSMul (β := ρ.asModule) c ((ρ.asModuleEquiv.symm : (a : V) → ρ.asModule) a : ρ.asModule)
have refine : ∀ (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: refine fun x v hv ↦ ⟨ρ.asModuleEquiv (x • ρ.asModuleEquiv.symm v), ?_, rfl⟩
-- Lean 4 proof step from Mathlib.RepresentationTheory.Submodule (goal)
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
⊢ 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)
have 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)
Tactic: rw [invtSubmodule, Sublattice.mem_iInf]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Submodule (goal)
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
⊢ 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
have 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)
Tactic: simp only [Submodule.orderIsoMapComap_symm_apply, Submodule.mem_comap] at hv ⊢
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.RepresentationTheory.Submodule (goal)
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)
⊢ 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)
have 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)
Tactic: convert! q.smul_mem (MonoidAlgebra.of k G g) hv using 1
-- Lean 4 proof step from Mathlib.RepresentationTheory.Submodule (goal)
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)
⊢ ((↑ρ.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)
have 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)
Tactic: rw [LinearEquiv.coe_coe, ← asModuleEquiv_symm_map_rho]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Submodule (goal)
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)
⊢ ((↑ρ.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)
have 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)
Tactic: rw [LinearEquiv.coe_coe, ← asModuleEquiv_symm_map_rho]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Submodule (goal)
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
⊢ (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
have 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))
                  sorry :
                ↥ρ.invtSubmodule))
            ((fun (p : ↥ρ.invtSubmodule) ↦
                let __AddSubmonoid : AddSubmonoid ρ.asModule :=
                  AddSubmonoid.map ρ.asModuleEquiv.symm (↑p : Submodule k V).toAddSubmonoid;
                { toAddSubmonoid := __AddSubmonoid, smul_mem' := sorry : Submodule k[G] ρ.asModule })
              p)) :
        Submodule k V)
      x ↔
    x ∈ (↑p : Submodule k V)
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Submodule (goal)
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
⊢ (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
have 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' := sorry : 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))
                sorry :
              ↥ρ.invtSubmodule))
          q))
      x ↔
    x ∈ q
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Submodule (goal)
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)
⊢ x ∈ (↑q : Submodule k V)
have suffices : Membership.mem (α := ρ.asModule) (γ := AddSubmonoid ρ.asModule)
  (AddSubmonoid.map ρ.asModuleEquiv.symm (↑q : Submodule k V).toAddSubmonoid)
  ((ρ.asModuleEquiv.symm : (a : V) → ρ.asModule) x : ρ.asModule)
Tactic: suffices ρ.asModuleEquiv.symm x ∈
        (q : Submodule k V).toAddSubmonoid.map ρ.asModuleEquiv.symm by simpa using this