case zero
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type ?u.292638
M₂ : Type ?u.292641
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₗ[R] M
h : p ≤ comap f p
k : ℕ
h'✝ : optParam (p ≤ comap (f ^ k) p) (_ : p ≤ comap (f ^ k) p)
h' : optParam (p ≤ comap (f ^ Nat.zero) p) (_ : p ≤ comap (f ^ Nat.zero) p)
⊢ mapQ p p (f ^ Nat.zero) h' = mapQ p p f h ^ Nat.zero

case succ
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type ?u.292638
M₂ : Type ?u.292641
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₗ[R] M
h : p ≤ comap f p
k✝ : ℕ
h'✝ : optParam (p ≤ comap (f ^ k✝) p) (_ : p ≤ comap (f ^ k✝) p)
k : ℕ
ih : ∀ (h' : optParam (p ≤ comap (f ^ k) p) (_ : p ≤ comap (f ^ k) p)), mapQ p p (f ^ k) h' = mapQ p p f h ^ k
h' : optParam (p ≤ comap (f ^ Nat.succ k) p) (_ : p ≤ comap (f ^ Nat.succ k) p)
⊢ mapQ p p (f ^ Nat.succ k) h' = mapQ p p f h ^ Nat.succ k
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type ?u.292638
M₂ : Type ?u.292641
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₗ[R] M
h : p ≤ comap f p
k : ℕ
h' : optParam (p ≤ comap (f ^ k) p) (_ : p ≤ comap (f ^ k) p)
⊢ mapQ p p (f ^ k) h' = mapQ p p f h ^ k
induction' k with k ih
no goals
case zero
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type ?u.292638
M₂ : Type ?u.292641
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₗ[R] M
h : p ≤ comap f p
k : ℕ
h'✝ : optParam (p ≤ comap (f ^ k) p) (_ : p ≤ comap (f ^ k) p)
h' : optParam (p ≤ comap (f ^ Nat.zero) p) (_ : p ≤ comap (f ^ Nat.zero) p)
⊢ mapQ p p (f ^ Nat.zero) h' = mapQ p p f h ^ Nat.zero
simp [LinearMap.one_eq_id]
case succ
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type ?u.292638
M₂ : Type ?u.292641
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₗ[R] M
h : p ≤ comap f p
k✝ : ℕ
h'✝ : optParam (p ≤ comap (f ^ k✝) p) (_ : p ≤ comap (f ^ k✝) p)
k : ℕ
ih : ∀ (h' : optParam (p ≤ comap (f ^ k) p) (_ : p ≤ comap (f ^ k) p)), mapQ p p (f ^ k) h' = mapQ p p f h ^ k
h' : optParam (p ≤ comap (f ^ Nat.succ k) p) (_ : p ≤ comap (f ^ Nat.succ k) p)
⊢ mapQ p p (comp (f ^ k) f) (_ : p ≤ comap (comp (f ^ k) f) p) = comp (mapQ p p f h ^ k) (mapQ p p f h)
case succ
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type ?u.292638
M₂ : Type ?u.292641
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₗ[R] M
h : p ≤ comap f p
k✝ : ℕ
h'✝ : optParam (p ≤ comap (f ^ k✝) p) (_ : p ≤ comap (f ^ k✝) p)
k : ℕ
ih : ∀ (h' : optParam (p ≤ comap (f ^ k) p) (_ : p ≤ comap (f ^ k) p)), mapQ p p (f ^ k) h' = mapQ p p f h ^ k
h' : optParam (p ≤ comap (f ^ Nat.succ k) p) (_ : p ≤ comap (f ^ Nat.succ k) p)
⊢ mapQ p p (f ^ Nat.succ k) h' = mapQ p p f h ^ Nat.succ k
simp only [LinearMap.iterate_succ]
case h.e'_3.h.e'_20
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type ?u.292638
M₂ : Type ?u.292641
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₗ[R] M
h : p ≤ comap f p
k✝ : ℕ
h'✝ : optParam (p ≤ comap (f ^ k✝) p) (_ : p ≤ comap (f ^ k✝) p)
k : ℕ
ih : ∀ (h' : optParam (p ≤ comap (f ^ k) p) (_ : p ≤ comap (f ^ k) p)), mapQ p p (f ^ k) h' = mapQ p p f h ^ k
h' : optParam (p ≤ comap (f ^ Nat.succ k) p) (_ : p ≤ comap (f ^ Nat.succ k) p)
⊢ mapQ p p f h ^ k = mapQ p p (f ^ k) (_ : p ≤ comap (f ^ k) p)
case succ
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type ?u.292638
M₂ : Type ?u.292641
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₗ[R] M
h : p ≤ comap f p
k✝ : ℕ
h'✝ : optParam (p ≤ comap (f ^ k✝) p) (_ : p ≤ comap (f ^ k✝) p)
k : ℕ
ih : ∀ (h' : optParam (p ≤ comap (f ^ k) p) (_ : p ≤ comap (f ^ k) p)), mapQ p p (f ^ k) h' = mapQ p p f h ^ k
h' : optParam (p ≤ comap (f ^ Nat.succ k) p) (_ : p ≤ comap (f ^ Nat.succ k) p)
⊢ mapQ p p (comp (f ^ k) f) (_ : p ≤ comap (comp (f ^ k) f) p) = comp (mapQ p p f h ^ k) (mapQ p p f h)
convert mapQ_comp p p p f (f ^ k) h (p.le_comap_pow_of_le_comap h k)
  (h.trans (comap_mono <| p.le_comap_pow_of_le_comap h k))
no goals
case h.e'_3.h.e'_20
R : Type u_1
M : Type u_2
r : R
x y : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
R₂ : Type ?u.292638
M₂ : Type ?u.292641
inst✝² : Ring R₂
inst✝¹ : AddCommGroup M₂
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
q : Submodule R₂ M₂
f : M →ₗ[R] M
h : p ≤ comap f p
k✝ : ℕ
h'✝ : optParam (p ≤ comap (f ^ k✝) p) (_ : p ≤ comap (f ^ k✝) p)
k : ℕ
ih : ∀ (h' : optParam (p ≤ comap (f ^ k) p) (_ : p ≤ comap (f ^ k) p)), mapQ p p (f ^ k) h' = mapQ p p f h ^ k
h' : optParam (p ≤ comap (f ^ Nat.succ k) p) (_ : p ≤ comap (f ^ Nat.succ k) p)
⊢ mapQ p p f h ^ k = mapQ p p (f ^ k) (_ : p ≤ comap (f ^ k) p)
exact (ih _).symm