-- Mathlib/RepresentationTheory/Maschke.lean
theorem exists_leftInverse_of_injective
    (f : V →ₗ[MonoidAlgebra k G] W) (hf : LinearMap.ker f = ⊥) :
    ∃ g : W →ₗ[MonoidAlgebra k G] V, g.comp f = LinearMap.id

Proof state:
k : Type u
inst✝⁷ : Field k
G : Type u
inst✝⁶ : Fintype G
inst✝⁵ : NeZero ↑(Fintype.card G)
inst✝⁴ : Group G
V : Type u
inst✝³ : AddCommGroup V
inst✝² : Module (MonoidAlgebra k G) V
W : Type u
inst✝¹ : AddCommGroup W
inst✝ : Module (MonoidAlgebra k G) W
f : V →ₗ[MonoidAlgebra k G] W
hf : LinearMap.ker f = ⊥
A : Type u := MonoidAlgebra k G
this✝ : Module k W := Module.compHom W (algebraMap k A)
this : Module k V := Module.compHom V (algebraMap k A)
⊢ ∃ g, g ∘ₗ f = LinearMap.id

Tactic:
have := IsScalarTower.of_compHom k A W

Result:
k : Type u
inst✝⁷ : Field k
G : Type u
inst✝⁶ : Fintype G
inst✝⁵ : NeZero ↑(Fintype.card G)
inst✝⁴ : Group G
V : Type u
inst✝³ : AddCommGroup V
inst✝² : Module (MonoidAlgebra k G) V
W : Type u
inst✝¹ : AddCommGroup W
inst✝ : Module (MonoidAlgebra k G) W
f : V →ₗ[MonoidAlgebra k G] W
hf : LinearMap.ker f = ⊥
A : Type u := MonoidAlgebra k G
this✝¹ : Module k W := Module.compHom W (algebraMap k A)
this✝ : Module k V := Module.compHom V (algebraMap k A)
this : IsScalarTower k A W
⊢ ∃ g, g ∘ₗ f = LinearMap.id

Proof state:
k : Type u
inst✝⁷ : Field k
G : Type u
inst✝⁶ : Fintype G
inst✝⁵ : NeZero ↑(Fintype.card G)
inst✝⁴ : Group G
V : Type u
inst✝³ : AddCommGroup V
inst✝² : Module (MonoidAlgebra k G) V
W : Type u
inst✝¹ : AddCommGroup W
inst✝ : Module (MonoidAlgebra k G) W
f : V →ₗ[MonoidAlgebra k G] W
hf : LinearMap.ker f = ⊥
⊢ ∃ g, g ∘ₗ f = LinearMap.id

Tactic:
let A := MonoidAlgebra k G

Result:
k : Type u
inst✝⁷ : Field k
G : Type u
inst✝⁶ : Fintype G
inst✝⁵ : NeZero ↑(Fintype.card G)
inst✝⁴ : Group G
V : Type u
inst✝³ : AddCommGroup V
inst✝² : Module (MonoidAlgebra k G) V
W : Type u
inst✝¹ : AddCommGroup W
inst✝ : Module (MonoidAlgebra k G) W
f : V →ₗ[MonoidAlgebra k G] W
hf : LinearMap.ker f = ⊥
A : Type u := MonoidAlgebra k G
⊢ ∃ g, g ∘ₗ f = LinearMap.id

Proof state:
k : Type u
inst✝⁷ : Field k
G : Type u
inst✝⁶ : Fintype G
inst✝⁵ : NeZero ↑(Fintype.card G)
inst✝⁴ : Group G
V : Type u
inst✝³ : AddCommGroup V
inst✝² : Module (MonoidAlgebra k G) V
W : Type u
inst✝¹ : AddCommGroup W
inst✝ : Module (MonoidAlgebra k G) W
f : V →ₗ[MonoidAlgebra k G] W
hf : LinearMap.ker f = ⊥
A : Type u := MonoidAlgebra k G
this✝¹ : Module k W := Module.compHom W (algebraMap k A)
this✝ : Module k V := Module.compHom V (algebraMap k A)
this : IsScalarTower k A W
⊢ ∃ g, g ∘ₗ f = LinearMap.id

Tactic:
have := IsScalarTower.of_compHom k A V

Result:
k : Type u
inst✝⁷ : Field k
G : Type u
inst✝⁶ : Fintype G
inst✝⁵ : NeZero ↑(Fintype.card G)
inst✝⁴ : Group G
V : Type u
inst✝³ : AddCommGroup V
inst✝² : Module (MonoidAlgebra k G) V
W : Type u
inst✝¹ : AddCommGroup W
inst✝ : Module (MonoidAlgebra k G) W
f : V →ₗ[MonoidAlgebra k G] W
hf : LinearMap.ker f = ⊥
A : Type u := MonoidAlgebra k G
this✝² : Module k W := Module.compHom W (algebraMap k A)
this✝¹ : Module k V := Module.compHom V (algebraMap k A)
this✝ : IsScalarTower k A W
this : IsScalarTower k A V
⊢ ∃ g, g ∘ₗ f = LinearMap.id

Proof state:
k : Type u
inst✝⁷ : Field k
G : Type u
inst✝⁶ : Fintype G
inst✝⁵ : NeZero ↑(Fintype.card G)
inst✝⁴ : Group G
V : Type u
inst✝³ : AddCommGroup V
inst✝² : Module (MonoidAlgebra k G) V
W : Type u
inst✝¹ : AddCommGroup W
inst✝ : Module (MonoidAlgebra k G) W
f : V →ₗ[MonoidAlgebra k G] W
hf : LinearMap.ker f = ⊥
A : Type u := MonoidAlgebra k G
⊢ ∃ g, g ∘ₗ f = LinearMap.id

Tactic:
letI : Module k W := .compHom W (algebraMap k A)

Result:
k : Type u
inst✝⁷ : Field k
G : Type u
inst✝⁶ : Fintype G
inst✝⁵ : NeZero ↑(Fintype.card G)
inst✝⁴ : Group G
V : Type u
inst✝³ : AddCommGroup V
inst✝² : Module (MonoidAlgebra k G) V
W : Type u
inst✝¹ : AddCommGroup W
inst✝ : Module (MonoidAlgebra k G) W
f : V →ₗ[MonoidAlgebra k G] W
hf : LinearMap.ker f = ⊥
A : Type u := MonoidAlgebra k G
this : Module k W := Module.compHom W (algebraMap k A)
⊢ ∃ g, g ∘ₗ f = LinearMap.id

Proof state:
k : Type u
inst✝⁷ : Field k
G : Type u
inst✝⁶ : Fintype G
inst✝⁵ : NeZero ↑(Fintype.card G)
inst✝⁴ : Group G
V : Type u
inst✝³ : AddCommGroup V
inst✝² : Module (MonoidAlgebra k G) V
W : Type u
inst✝¹ : AddCommGroup W
inst✝ : Module (MonoidAlgebra k G) W
f : V →ₗ[MonoidAlgebra k G] W
hf : LinearMap.ker f = ⊥
A : Type u := MonoidAlgebra k G
this✝² : Module k W := Module.compHom W (algebraMap k A)
this✝¹ : Module k V := Module.compHom V (algebraMap k A)
this✝ : IsScalarTower k A W
this : IsScalarTower k A V
⊢ ∃ g, g ∘ₗ f = LinearMap.id

Tactic:
obtain ⟨φ, hφ⟩ := (f.restrictScalars k).exists_leftInverse_of_injective <| by
  simp only [hf, Submodule.restrictScalars_bot, LinearMap.ker_restrictScalars]

Result:
case intro
k : Type u
inst✝⁷ : Field k
G : Type u
inst✝⁶ : Fintype G
inst✝⁵ : NeZero ↑(Fintype.card G)
inst✝⁴ : Group G
V : Type u
inst✝³ : AddCommGroup V
inst✝² : Module (MonoidAlgebra k G) V
W : Type u
inst✝¹ : AddCommGroup W
inst✝ : Module (MonoidAlgebra k G) W
f : V →ₗ[MonoidAlgebra k G] W
hf : LinearMap.ker f = ⊥
A : Type u := MonoidAlgebra k G
this✝² : Module k W := Module.compHom W (algebraMap k A)
this✝¹ : Module k V := Module.compHom V (algebraMap k A)
this✝ : IsScalarTower k A W
this : IsScalarTower k A V
φ : W →ₗ[k] V
hφ : φ ∘ₗ ↑k f = LinearMap.id
⊢ ∃ g, g ∘ₗ f = LinearMap.id

Proof state:
k : Type u
inst✝⁷ : Field k
G : Type u
inst✝⁶ : Fintype G
inst✝⁵ : NeZero ↑(Fintype.card G)
inst✝⁴ : Group G
V : Type u
inst✝³ : AddCommGroup V
inst✝² : Module (MonoidAlgebra k G) V
W : Type u
inst✝¹ : AddCommGroup W
inst✝ : Module (MonoidAlgebra k G) W
f : V →ₗ[MonoidAlgebra k G] W
hf : LinearMap.ker f = ⊥
A : Type u := MonoidAlgebra k G
this : Module k W := Module.compHom W (algebraMap k A)
⊢ ∃ g, g ∘ₗ f = LinearMap.id

Tactic:
letI : Module k V := .compHom V (algebraMap k A)

Result:
k : Type u
inst✝⁷ : Field k
G : Type u
inst✝⁶ : Fintype G
inst✝⁵ : NeZero ↑(Fintype.card G)
inst✝⁴ : Group G
V : Type u
inst✝³ : AddCommGroup V
inst✝² : Module (MonoidAlgebra k G) V
W : Type u
inst✝¹ : AddCommGroup W
inst✝ : Module (MonoidAlgebra k G) W
f : V →ₗ[MonoidAlgebra k G] W
hf : LinearMap.ker f = ⊥
A : Type u := MonoidAlgebra k G
this✝ : Module k W := Module.compHom W (algebraMap k A)
this : Module k V := Module.compHom V (algebraMap k A)
⊢ ∃ g, g ∘ₗ f = LinearMap.id

Proof state:
case intro
k : Type u
inst✝⁷ : Field k
G : Type u
inst✝⁶ : Fintype G
inst✝⁵ : NeZero ↑(Fintype.card G)
inst✝⁴ : Group G
V : Type u
inst✝³ : AddCommGroup V
inst✝² : Module (MonoidAlgebra k G) V
W : Type u
inst✝¹ : AddCommGroup W
inst✝ : Module (MonoidAlgebra k G) W
f : V →ₗ[MonoidAlgebra k G] W
hf : LinearMap.ker f = ⊥
A : Type u := MonoidAlgebra k G
this✝² : Module k W := Module.compHom W (algebraMap k A)
this✝¹ : Module k V := Module.compHom V (algebraMap k A)
this✝ : IsScalarTower k A W
this : IsScalarTower k A V
φ : W →ₗ[k] V
hφ : φ ∘ₗ ↑k f = LinearMap.id
⊢ ∀ (x : V), (LinearMap.equivariantProjection G φ ∘ₗ f) x = LinearMap.id x

Tactic:
exact φ.equivariantProjection_condition G _ (.mk0 _ <| NeZero.ne _) <| DFunLike.congr_fun hφ

Result:
no goals

Proof state:
k : Type u
inst✝⁷ : Field k
G : Type u
inst✝⁶ : Fintype G
inst✝⁵ : NeZero ↑(Fintype.card G)
inst✝⁴ : Group G
V : Type u
inst✝³ : AddCommGroup V
inst✝² : Module (MonoidAlgebra k G) V
W : Type u
inst✝¹ : AddCommGroup W
inst✝ : Module (MonoidAlgebra k G) W
f : V →ₗ[MonoidAlgebra k G] W
hf : LinearMap.ker f = ⊥
A : Type u := MonoidAlgebra k G
this✝² : Module k W := Module.compHom W (algebraMap k A)
this✝¹ : Module k V := Module.compHom V (algebraMap k A)
this✝ : IsScalarTower k A W
this : IsScalarTower k A V
⊢ LinearMap.ker (↑k f) = ⊥

Tactic:
simp only [hf, Submodule.restrictScalars_bot, LinearMap.ker_restrictScalars]

Result:
no goals