R : Type u_2
R₁ : Type ?u.232371
R₂ : Type ?u.232374
R₃ : Type ?u.232377
R₄ : Type ?u.232380
S : Type ?u.232383
K : Type ?u.232386
K₂ : Type ?u.232389
M : Type u_1
M' : Type ?u.232395
M₁ : Type ?u.232398
M₂ : Type ?u.232401
M₃ : Type ?u.232404
M₄ : Type ?u.232407
N : Type ?u.232410
N₂ : Type ?u.232413
ι : Type ?u.232416
V : Type ?u.232419
V₂ : Type ?u.232422
inst✝¹⁷ : Semiring R
inst✝¹⁶ : Semiring R₂
inst✝¹⁵ : Semiring R₃
inst✝¹⁴ : Semiring R₄
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid M₁
inst✝¹¹ : AddCommMonoid M₂
inst✝¹⁰ : AddCommMonoid M₃
inst✝⁹ : AddCommMonoid M₄
inst✝⁸ : Module R M
inst✝⁷ : Module R M₁
inst✝⁶ : Module R₂ M₂
inst✝⁵ : Module R₃ M₃
inst✝⁴ : Module R₄ M₄
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₃₄ : R₃ →+* R₄
σ₁₃ : R →+* R₃
σ₂₄ : R₂ →+* R₄
σ₁₄ : R →+* R₄
inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝² : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝¹ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
f : M →ₛₗ[σ₁₂] M₂
g : M₂ →ₛₗ[σ₂₃] M₃
f' : M →ₗ[R] M
n : ℕ
hn : n ≠ 0
h : Surjective ↑(f' ^ 1 * f' ^ Nat.pred n)
⊢ Surjective ↑f'
R : Type u_2
R₁ : Type ?u.232371
R₂ : Type ?u.232374
R₃ : Type ?u.232377
R₄ : Type ?u.232380
S : Type ?u.232383
K : Type ?u.232386
K₂ : Type ?u.232389
M : Type u_1
M' : Type ?u.232395
M₁ : Type ?u.232398
M₂ : Type ?u.232401
M₃ : Type ?u.232404
M₄ : Type ?u.232407
N : Type ?u.232410
N₂ : Type ?u.232413
ι : Type ?u.232416
V : Type ?u.232419
V₂ : Type ?u.232422
inst✝¹⁷ : Semiring R
inst✝¹⁶ : Semiring R₂
inst✝¹⁵ : Semiring R₃
inst✝¹⁴ : Semiring R₄
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid M₁
inst✝¹¹ : AddCommMonoid M₂
inst✝¹⁰ : AddCommMonoid M₃
inst✝⁹ : AddCommMonoid M₄
inst✝⁸ : Module R M
inst✝⁷ : Module R M₁
inst✝⁶ : Module R₂ M₂
inst✝⁵ : Module R₃ M₃
inst✝⁴ : Module R₄ M₄
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₃₄ : R₃ →+* R₄
σ₁₃ : R →+* R₃
σ₂₄ : R₂ →+* R₄
σ₁₄ : R →+* R₄
inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝² : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝¹ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
f : M →ₛₗ[σ₁₂] M₂
g : M₂ →ₛₗ[σ₂₃] M₃
f' : M →ₗ[R] M
n : ℕ
hn : n ≠ 0
h : Surjective ↑(f' ^ n)
⊢ Surjective ↑f'
rw [← Nat.succ_pred_eq_of_pos (pos_iff_ne_zero.mpr hn),
  Nat.succ_eq_add_one, add_comm, pow_add] at h
no goals
R : Type u_2
R₁ : Type ?u.232371
R₂ : Type ?u.232374
R₃ : Type ?u.232377
R₄ : Type ?u.232380
S : Type ?u.232383
K : Type ?u.232386
K₂ : Type ?u.232389
M : Type u_1
M' : Type ?u.232395
M₁ : Type ?u.232398
M₂ : Type ?u.232401
M₃ : Type ?u.232404
M₄ : Type ?u.232407
N : Type ?u.232410
N₂ : Type ?u.232413
ι : Type ?u.232416
V : Type ?u.232419
V₂ : Type ?u.232422
inst✝¹⁷ : Semiring R
inst✝¹⁶ : Semiring R₂
inst✝¹⁵ : Semiring R₃
inst✝¹⁴ : Semiring R₄
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid M₁
inst✝¹¹ : AddCommMonoid M₂
inst✝¹⁰ : AddCommMonoid M₃
inst✝⁹ : AddCommMonoid M₄
inst✝⁸ : Module R M
inst✝⁷ : Module R M₁
inst✝⁶ : Module R₂ M₂
inst✝⁵ : Module R₃ M₃
inst✝⁴ : Module R₄ M₄
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₃₄ : R₃ →+* R₄
σ₁₃ : R →+* R₃
σ₂₄ : R₂ →+* R₄
σ₁₄ : R →+* R₄
inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝² : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄
inst✝¹ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄
inst✝ : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄
f : M →ₛₗ[σ₁₂] M₂
g : M₂ →ₛₗ[σ₂₃] M₃
f' : M →ₗ[R] M
n : ℕ
hn : n ≠ 0
h : Surjective ↑(f' ^ 1 * f' ^ Nat.pred n)
⊢ Surjective ↑f'
exact Surjective.of_comp h