R : Type u_1
R₁ : Type ?u.249328
R₂ : Type ?u.249331
R₃ : Type ?u.249334
R₄ : Type ?u.249337
S : Type ?u.249340
K : Type ?u.249343
K₂ : Type ?u.249346
M : Type u_2
M' : Type ?u.249352
M₁ : Type ?u.249355
M₂ : Type ?u.249358
M₃ : Type ?u.249361
M₄ : Type ?u.249364
N : Type ?u.249367
N₂ : Type ?u.249370
ι : Type ?u.249373
V : Type ?u.249376
V₂ : Type ?u.249379
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
p : Submodule R M
n : ℕ
h : ∀ (x : M), x ∈ p → ↑f' x ∈ p
h' : ∀ (x : M), x ∈ p → ↑(f' ^ n) x ∈ p
⊢ restrict f' h ^ n = restrict (f' ^ n) h'
R : Type u_1
R₁ : Type ?u.249328
R₂ : Type ?u.249331
R₃ : Type ?u.249334
R₄ : Type ?u.249337
S : Type ?u.249340
K : Type ?u.249343
K₂ : Type ?u.249346
M : Type u_2
M' : Type ?u.249352
M₁ : Type ?u.249355
M₂ : Type ?u.249358
M₃ : Type ?u.249361
M₄ : Type ?u.249364
N : Type ?u.249367
N₂ : Type ?u.249370
ι : Type ?u.249373
V : Type ?u.249376
V₂ : Type ?u.249379
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
p : Submodule R M
n : ℕ
h : ∀ (x : M), x ∈ p → ↑f' x ∈ p
h' : optParam (∀ (x : M), x ∈ p → ↑(f' ^ n) x ∈ p) (_ : ∀ (x : M), x ∈ p → ↑(f' ^ n) x ∈ p)
⊢ restrict f' h ^ n = restrict (f' ^ n) h'
dsimp [optParam] at h'
case zero.h.a
R : Type u_1
R₁ : Type ?u.249328
R₂ : Type ?u.249331
R₃ : Type ?u.249334
R₄ : Type ?u.249337
S : Type ?u.249340
K : Type ?u.249343
K₂ : Type ?u.249346
M : Type u_2
M' : Type ?u.249352
M₁ : Type ?u.249355
M₂ : Type ?u.249358
M₃ : Type ?u.249361
M₄ : Type ?u.249364
N : Type ?u.249367
N₂ : Type ?u.249370
ι : Type ?u.249373
V : Type ?u.249376
V₂ : Type ?u.249379
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
p : Submodule R M
n : ℕ
h : ∀ (x : M), x ∈ p → ↑f' x ∈ p
h'✝ : ∀ (x : M), x ∈ p → ↑(f' ^ n) x ∈ p
h' : ∀ (x : M), x ∈ p → ↑(f' ^ Nat.zero) x ∈ p
x✝ : { x // x ∈ p }
⊢ ↑(↑(restrict f' h ^ Nat.zero) x✝) = ↑(↑(restrict (f' ^ Nat.zero) h') x✝)

case succ.h.a
R : Type u_1
R₁ : Type ?u.249328
R₂ : Type ?u.249331
R₃ : Type ?u.249334
R₄ : Type ?u.249337
S : Type ?u.249340
K : Type ?u.249343
K₂ : Type ?u.249346
M : Type u_2
M' : Type ?u.249352
M₁ : Type ?u.249355
M₂ : Type ?u.249358
M₃ : Type ?u.249361
M₄ : Type ?u.249364
N : Type ?u.249367
N₂ : Type ?u.249370
ι : Type ?u.249373
V : Type ?u.249376
V₂ : Type ?u.249379
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
p : Submodule R M
n✝ : ℕ
h : ∀ (x : M), x ∈ p → ↑f' x ∈ p
h'✝ : ∀ (x : M), x ∈ p → ↑(f' ^ n✝) x ∈ p
n : ℕ
ih : ∀ (h' : ∀ (x : M), x ∈ p → ↑(f' ^ n) x ∈ p), restrict f' h ^ n = restrict (f' ^ n) h'
h' : ∀ (x : M), x ∈ p → ↑(f' ^ Nat.succ n) x ∈ p
x✝ : { x // x ∈ p }
⊢ ↑(↑(restrict f' h ^ Nat.succ n) x✝) = ↑(↑(restrict (f' ^ Nat.succ n) h') x✝)
R : Type u_1
R₁ : Type ?u.249328
R₂ : Type ?u.249331
R₃ : Type ?u.249334
R₄ : Type ?u.249337
S : Type ?u.249340
K : Type ?u.249343
K₂ : Type ?u.249346
M : Type u_2
M' : Type ?u.249352
M₁ : Type ?u.249355
M₂ : Type ?u.249358
M₃ : Type ?u.249361
M₄ : Type ?u.249364
N : Type ?u.249367
N₂ : Type ?u.249370
ι : Type ?u.249373
V : Type ?u.249376
V₂ : Type ?u.249379
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
p : Submodule R M
n : ℕ
h : ∀ (x : M), x ∈ p → ↑f' x ∈ p
h' : ∀ (x : M), x ∈ p → ↑(f' ^ n) x ∈ p
⊢ restrict f' h ^ n = restrict (f' ^ n) h'
induction' n with n ih <;> ext
no goals
case zero.h.a
R : Type u_1
R₁ : Type ?u.249328
R₂ : Type ?u.249331
R₃ : Type ?u.249334
R₄ : Type ?u.249337
S : Type ?u.249340
K : Type ?u.249343
K₂ : Type ?u.249346
M : Type u_2
M' : Type ?u.249352
M₁ : Type ?u.249355
M₂ : Type ?u.249358
M₃ : Type ?u.249361
M₄ : Type ?u.249364
N : Type ?u.249367
N₂ : Type ?u.249370
ι : Type ?u.249373
V : Type ?u.249376
V₂ : Type ?u.249379
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
p : Submodule R M
n : ℕ
h : ∀ (x : M), x ∈ p → ↑f' x ∈ p
h'✝ : ∀ (x : M), x ∈ p → ↑(f' ^ n) x ∈ p
h' : ∀ (x : M), x ∈ p → ↑(f' ^ Nat.zero) x ∈ p
x✝ : { x // x ∈ p }
⊢ ↑(↑(restrict f' h ^ Nat.zero) x✝) = ↑(↑(restrict (f' ^ Nat.zero) h') x✝)
simp [restrict_apply]
case succ.h.a
R : Type u_1
R₁ : Type ?u.249328
R₂ : Type ?u.249331
R₃ : Type ?u.249334
R₄ : Type ?u.249337
S : Type ?u.249340
K : Type ?u.249343
K₂ : Type ?u.249346
M : Type u_2
M' : Type ?u.249352
M₁ : Type ?u.249355
M₂ : Type ?u.249358
M₃ : Type ?u.249361
M₄ : Type ?u.249364
N : Type ?u.249367
N₂ : Type ?u.249370
ι : Type ?u.249373
V : Type ?u.249376
V₂ : Type ?u.249379
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
p : Submodule R M
n✝ : ℕ
h : ∀ (x : M), x ∈ p → ↑f' x ∈ p
h'✝ : ∀ (x : M), x ∈ p → ↑(f' ^ n✝) x ∈ p
n : ℕ
ih : ∀ (h' : ∀ (x : M), x ∈ p → ↑(f' ^ n) x ∈ p), restrict f' h ^ n = restrict (f' ^ n) h'
h' : ∀ (x : M), x ∈ p → ↑(f' ^ Nat.succ n) x ∈ p
x✝ : { x // x ∈ p }
⊢ ↑(↑(comp (restrict (f' ^ n) (_ : ∀ (x : M), x ∈ p → ↑(f' ^ n) x ∈ p)) (restrict f' h)) x✝) =
    ↑{ val := ↑(f' ^ Nat.succ n) ↑x✝, property := (_ : ↑(f' ^ Nat.succ n) ↑x✝ ∈ p) }
case succ.h.a
R : Type u_1
R₁ : Type ?u.249328
R₂ : Type ?u.249331
R₃ : Type ?u.249334
R₄ : Type ?u.249337
S : Type ?u.249340
K : Type ?u.249343
K₂ : Type ?u.249346
M : Type u_2
M' : Type ?u.249352
M₁ : Type ?u.249355
M₂ : Type ?u.249358
M₃ : Type ?u.249361
M₄ : Type ?u.249364
N : Type ?u.249367
N₂ : Type ?u.249370
ι : Type ?u.249373
V : Type ?u.249376
V₂ : Type ?u.249379
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
p : Submodule R M
n✝ : ℕ
h : ∀ (x : M), x ∈ p → ↑f' x ∈ p
h'✝ : ∀ (x : M), x ∈ p → ↑(f' ^ n✝) x ∈ p
n : ℕ
ih : ∀ (h' : ∀ (x : M), x ∈ p → ↑(f' ^ n) x ∈ p), restrict f' h ^ n = restrict (f' ^ n) h'
h' : ∀ (x : M), x ∈ p → ↑(f' ^ Nat.succ n) x ∈ p
x✝ : { x // x ∈ p }
⊢ ↑(↑(restrict f' h ^ Nat.succ n) x✝) = ↑(↑(restrict (f' ^ Nat.succ n) h') x✝)
rw [restrict_apply, LinearMap.iterate_succ, ih (pow_apply_mem_of_forall_mem n h)]
no goals
case succ.h.a
R : Type u_1
R₁ : Type ?u.249328
R₂ : Type ?u.249331
R₃ : Type ?u.249334
R₄ : Type ?u.249337
S : Type ?u.249340
K : Type ?u.249343
K₂ : Type ?u.249346
M : Type u_2
M' : Type ?u.249352
M₁ : Type ?u.249355
M₂ : Type ?u.249358
M₃ : Type ?u.249361
M₄ : Type ?u.249364
N : Type ?u.249367
N₂ : Type ?u.249370
ι : Type ?u.249373
V : Type ?u.249376
V₂ : Type ?u.249379
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
p : Submodule R M
n✝ : ℕ
h : ∀ (x : M), x ∈ p → ↑f' x ∈ p
h'✝ : ∀ (x : M), x ∈ p → ↑(f' ^ n✝) x ∈ p
n : ℕ
ih : ∀ (h' : ∀ (x : M), x ∈ p → ↑(f' ^ n) x ∈ p), restrict f' h ^ n = restrict (f' ^ n) h'
h' : ∀ (x : M), x ∈ p → ↑(f' ^ Nat.succ n) x ∈ p
x✝ : { x // x ∈ p }
⊢ ↑(↑(comp (restrict (f' ^ n) (_ : ∀ (x : M), x ∈ p → ↑(f' ^ n) x ∈ p)) (restrict f' h)) x✝) =
    ↑{ val := ↑(f' ^ Nat.succ n) ↑x✝, property := (_ : ↑(f' ^ Nat.succ n) ↑x✝ ∈ p) }
simp