-- Mathlib/RepresentationTheory/Rep.lean
theorem to_Module_monoidAlgebra_map_aux {k G : Type*} [CommRing k] [Monoid G] (V W : Type*)
    [AddCommGroup V] [AddCommGroup W] [Module k V] [Module k W] (ρ : G →* V →ₗ[k] V)
    (σ : G →* W →ₗ[k] W) (f : V →ₗ[k] W) (w : ∀ g : G, f.comp (ρ g) = (σ g).comp f)
    (r : MonoidAlgebra k G) (x : V) :
    f ((((MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ) r) x) =
      (((MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) r) (f x)

Proof state:
case hM
k : Type u_1
G : Type u_2
inst✝⁵ : CommRing k
inst✝⁴ : Monoid G
V : Type u_3
W : Type u_4
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup W
inst✝¹ : Module k V
inst✝ : Module k W
ρ : G →* V →ₗ[k] V
σ : G →* W →ₗ[k] W
f : V →ₗ[k] W
w : ∀ (g : G), f ∘ₗ ρ g = σ g ∘ₗ f
r : MonoidAlgebra k G
x : V
g : G
⊢ f ((((MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ) ((MonoidAlgebra.of k G) g)) x) =
    (((MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) ((MonoidAlgebra.of k G) g)) (f x)

Tactic:
simp only [one_smul, MonoidAlgebra.lift_single, MonoidAlgebra.of_apply]

Result:
case hM
k : Type u_1
G : Type u_2
inst✝⁵ : CommRing k
inst✝⁴ : Monoid G
V : Type u_3
W : Type u_4
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup W
inst✝¹ : Module k V
inst✝ : Module k W
ρ : G →* V →ₗ[k] V
σ : G →* W →ₗ[k] W
f : V →ₗ[k] W
w : ∀ (g : G), f ∘ₗ ρ g = σ g ∘ₗ f
r : MonoidAlgebra k G
x : V
g : G
⊢ f ((ρ g) x) = (σ g) (f x)

Proof state:
case hadd
k : Type u_1
G : Type u_2
inst✝⁵ : CommRing k
inst✝⁴ : Monoid G
V : Type u_3
W : Type u_4
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup W
inst✝¹ : Module k V
inst✝ : Module k W
ρ : G →* V →ₗ[k] V
σ : G →* W →ₗ[k] W
f : V →ₗ[k] W
w : ∀ (g : G), f ∘ₗ ρ g = σ g ∘ₗ f
r : MonoidAlgebra k G
x : V
g h : MonoidAlgebra k G
gw : f ((((MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ) g) x) = (((MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) g) (f x)
hw : f ((((MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ) h) x) = (((MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) h) (f x)
⊢ f ((((MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ) (g + h)) x) = (((MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) (g + h)) (f x)

Tactic:
simp only [map_add, add_left_inj, LinearMap.add_apply, hw, gw]

Result:
no goals

Proof state:
case hM
k : Type u_1
G : Type u_2
inst✝⁵ : CommRing k
inst✝⁴ : Monoid G
V : Type u_3
W : Type u_4
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup W
inst✝¹ : Module k V
inst✝ : Module k W
ρ : G →* V →ₗ[k] V
σ : G →* W →ₗ[k] W
f : V →ₗ[k] W
w : ∀ (g : G), f ∘ₗ ρ g = σ g ∘ₗ f
r : MonoidAlgebra k G
x : V
g : G
⊢ f ((ρ g) x) = (σ g) (f x)

Tactic:
exact LinearMap.congr_fun (w g) x

Result:
no goals

Proof state:
case hsmul
k : Type u_1
G : Type u_2
inst✝⁵ : CommRing k
inst✝⁴ : Monoid G
V : Type u_3
W : Type u_4
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup W
inst✝¹ : Module k V
inst✝ : Module k W
ρ : G →* V →ₗ[k] V
σ : G →* W →ₗ[k] W
f : V →ₗ[k] W
w✝ : ∀ (g : G), f ∘ₗ ρ g = σ g ∘ₗ f
r✝ : MonoidAlgebra k G
x : V
r : k
g : MonoidAlgebra k G
w : f ((((MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ) g) x) = (((MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) g) (f x)
⊢ f ((((MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ) (r • g)) x) = (((MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) (r • g)) (f x)

Tactic:
simp only [map_smul, w, RingHom.id_apply, LinearMap.smul_apply, LinearMap.map_smulₛₗ]

Result:
no goals

Proof state:
k : Type u_1
G : Type u_2
inst✝⁵ : CommRing k
inst✝⁴ : Monoid G
V : Type u_3
W : Type u_4
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup W
inst✝¹ : Module k V
inst✝ : Module k W
ρ : G →* V →ₗ[k] V
σ : G →* W →ₗ[k] W
f : V →ₗ[k] W
w : ∀ (g : G), f ∘ₗ ρ g = σ g ∘ₗ f
r : MonoidAlgebra k G
x : V
⊢ f ((((MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ) r) x) = (((MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) r) (f x)

Tactic:
apply MonoidAlgebra.induction_on r

Result:
case hM
k : Type u_1
G : Type u_2
inst✝⁵ : CommRing k
inst✝⁴ : Monoid G
V : Type u_3
W : Type u_4
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup W
inst✝¹ : Module k V
inst✝ : Module k W
ρ : G →* V →ₗ[k] V
σ : G →* W →ₗ[k] W
f : V →ₗ[k] W
w : ∀ (g : G), f ∘ₗ ρ g = σ g ∘ₗ f
r : MonoidAlgebra k G
x : V
⊢ ∀ (g : G),
    f ((((MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ) ((MonoidAlgebra.of k G) g)) x) =
      (((MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) ((MonoidAlgebra.of k G) g)) (f x)

case hadd
k : Type u_1
G : Type u_2
inst✝⁵ : CommRing k
inst✝⁴ : Monoid G
V : Type u_3
W : Type u_4
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup W
inst✝¹ : Module k V
inst✝ : Module k W
ρ : G →* V →ₗ[k] V
σ : G →* W →ₗ[k] W
f : V →ₗ[k] W
w : ∀ (g : G), f ∘ₗ ρ g = σ g ∘ₗ f
r : MonoidAlgebra k G
x : V
⊢ ∀ (f_1 g : MonoidAlgebra k G),
    f ((((MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ) f_1) x) = (((MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) f_1) (f x) →
      f ((((MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ) g) x) = (((MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) g) (f x) →
        f ((((MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ) (f_1 + g)) x) =
          (((MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) (f_1 + g)) (f x)

case hsmul
k : Type u_1
G : Type u_2
inst✝⁵ : CommRing k
inst✝⁴ : Monoid G
V : Type u_3
W : Type u_4
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup W
inst✝¹ : Module k V
inst✝ : Module k W
ρ : G →* V →ₗ[k] V
σ : G →* W →ₗ[k] W
f : V →ₗ[k] W
w : ∀ (g : G), f ∘ₗ ρ g = σ g ∘ₗ f
r : MonoidAlgebra k G
x : V
⊢ ∀ (r : k) (f_1 : MonoidAlgebra k G),
    f ((((MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ) f_1) x) = (((MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) f_1) (f x) →
      f ((((MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ) (r • f_1)) x) =
        (((MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) (r • f_1)) (f x)

Proof state:
case hadd
k : Type u_1
G : Type u_2
inst✝⁵ : CommRing k
inst✝⁴ : Monoid G
V : Type u_3
W : Type u_4
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup W
inst✝¹ : Module k V
inst✝ : Module k W
ρ : G →* V →ₗ[k] V
σ : G →* W →ₗ[k] W
f : V →ₗ[k] W
w : ∀ (g : G), f ∘ₗ ρ g = σ g ∘ₗ f
r : MonoidAlgebra k G
x : V
⊢ ∀ (f_1 g : MonoidAlgebra k G),
    f ((((MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ) f_1) x) = (((MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) f_1) (f x) →
      f ((((MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ) g) x) = (((MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) g) (f x) →
        f ((((MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ) (f_1 + g)) x) =
          (((MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) (f_1 + g)) (f x)

Tactic:
intro g h gw hw

Result:
case hadd
k : Type u_1
G : Type u_2
inst✝⁵ : CommRing k
inst✝⁴ : Monoid G
V : Type u_3
W : Type u_4
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup W
inst✝¹ : Module k V
inst✝ : Module k W
ρ : G →* V →ₗ[k] V
σ : G →* W →ₗ[k] W
f : V →ₗ[k] W
w : ∀ (g : G), f ∘ₗ ρ g = σ g ∘ₗ f
r : MonoidAlgebra k G
x : V
g h : MonoidAlgebra k G
gw : f ((((MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ) g) x) = (((MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) g) (f x)
hw : f ((((MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ) h) x) = (((MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) h) (f x)
⊢ f ((((MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ) (g + h)) x) = (((MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) (g + h)) (f x)

Proof state:
case hM
k : Type u_1
G : Type u_2
inst✝⁵ : CommRing k
inst✝⁴ : Monoid G
V : Type u_3
W : Type u_4
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup W
inst✝¹ : Module k V
inst✝ : Module k W
ρ : G →* V →ₗ[k] V
σ : G →* W →ₗ[k] W
f : V →ₗ[k] W
w : ∀ (g : G), f ∘ₗ ρ g = σ g ∘ₗ f
r : MonoidAlgebra k G
x : V
⊢ ∀ (g : G),
    f ((((MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ) ((MonoidAlgebra.of k G) g)) x) =
      (((MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) ((MonoidAlgebra.of k G) g)) (f x)

Tactic:
intro g

Result:
case hM
k : Type u_1
G : Type u_2
inst✝⁵ : CommRing k
inst✝⁴ : Monoid G
V : Type u_3
W : Type u_4
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup W
inst✝¹ : Module k V
inst✝ : Module k W
ρ : G →* V →ₗ[k] V
σ : G →* W →ₗ[k] W
f : V →ₗ[k] W
w : ∀ (g : G), f ∘ₗ ρ g = σ g ∘ₗ f
r : MonoidAlgebra k G
x : V
g : G
⊢ f ((((MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ) ((MonoidAlgebra.of k G) g)) x) =
    (((MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) ((MonoidAlgebra.of k G) g)) (f x)