-- Mathlib/RingTheory/FiniteLength.lean
theorem LinearEquiv.isFiniteLength (e : M ≃ₗ[R] N)
    (h : IsFiniteLength R M) : IsFiniteLength R N

Proof state:
case of_simple_quotient
R : Type u_1
inst✝⁷ : Ring R
M✝ : Type u_2
inst✝⁶ : AddCommGroup M✝
inst✝⁵ : Module R M✝
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
S : Submodule R M
inst✝² : IsSimpleModule R (M ⧸ S)
a✝ : IsFiniteLength R ↥S
ih : ∀ {N : Type u_3} [inst : AddCommGroup N] [inst_1 : Module R N], (↥S ≃ₗ[R] N) → IsFiniteLength R N
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
e : M ≃ₗ[R] N
⊢ IsFiniteLength R N

Tactic:
have : IsSimpleModule R (N ⧸ Submodule.map (e : M →ₗ[R] N) S) :=
  IsSimpleModule.congr (Submodule.Quotient.equiv S _ e rfl).symm

Result:
case of_simple_quotient
R : Type u_1
inst✝⁷ : Ring R
M✝ : Type u_2
inst✝⁶ : AddCommGroup M✝
inst✝⁵ : Module R M✝
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
S : Submodule R M
inst✝² : IsSimpleModule R (M ⧸ S)
a✝ : IsFiniteLength R ↥S
ih : ∀ {N : Type u_3} [inst : AddCommGroup N] [inst_1 : Module R N], (↥S ≃ₗ[R] N) → IsFiniteLength R N
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
e : M ≃ₗ[R] N
this : IsSimpleModule R (N ⧸ Submodule.map (↑e) S)
⊢ IsFiniteLength R N

Proof state:
case of_subsingleton
R : Type u_1
inst✝⁷ : Ring R
M : Type u_2
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M✝ : Type u_2
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
inst✝² : Subsingleton M✝
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
e : M✝ ≃ₗ[R] N
this : Subsingleton N
⊢ IsFiniteLength R N

Tactic:
exact .of_subsingleton

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : Ring R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
e : M ≃ₗ[R] N
h : IsFiniteLength R M
⊢ IsFiniteLength R N

Tactic:
induction h generalizing N with
| of_subsingleton =>
  have := e.symm.toEquiv.subsingleton; exact .of_subsingleton
| @of_simple_quotient M _ _ S _ _ ih =>
  have : IsSimpleModule R (N ⧸ Submodule.map (e : M →ₗ[R] N) S) :=
    IsSimpleModule.congr (Submodule.Quotient.equiv S _ e rfl).symm
  exact .of_simple_quotient (ih <| e.submoduleMap S)

Result:
no goals

Proof state:
case of_subsingleton
R : Type u_1
inst✝⁷ : Ring R
M : Type u_2
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M✝ : Type u_2
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
inst✝² : Subsingleton M✝
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
e : M✝ ≃ₗ[R] N
⊢ IsFiniteLength R N

Tactic:
have := e.symm.toEquiv.subsingleton

Result:
case of_subsingleton
R : Type u_1
inst✝⁷ : Ring R
M : Type u_2
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
M✝ : Type u_2
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
inst✝² : Subsingleton M✝
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
e : M✝ ≃ₗ[R] N
this : Subsingleton N
⊢ IsFiniteLength R N

Proof state:
case of_simple_quotient
R : Type u_1
inst✝⁷ : Ring R
M✝ : Type u_2
inst✝⁶ : AddCommGroup M✝
inst✝⁵ : Module R M✝
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
S : Submodule R M
inst✝² : IsSimpleModule R (M ⧸ S)
a✝ : IsFiniteLength R ↥S
ih : ∀ {N : Type u_3} [inst : AddCommGroup N] [inst_1 : Module R N], (↥S ≃ₗ[R] N) → IsFiniteLength R N
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
e : M ≃ₗ[R] N
this : IsSimpleModule R (N ⧸ Submodule.map (↑e) S)
⊢ IsFiniteLength R N

Tactic:
exact .of_simple_quotient (ih <| e.submoduleMap S)

Result:
no goals