-- Mathlib/Algebra/Module/Submodule/IterateMapComap.lean
theorem iterateMapComap_eq_succ (K : Submodule R N)
    (m : ℕ) (heq : f.iterateMapComap i m K = f.iterateMapComap i (m + 1) K)
    (hf : Surjective f) (hi : Injective i) (n : ℕ) :
    f.iterateMapComap i n K = f.iterateMapComap i (n + 1) K

Proof state:
case zero.succ
R : Type u_1
N : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f i : N →ₗ[R] M
K : Submodule R N
hf : Surjective ⇑f
hi : Injective ⇑i
heq : f.iterateMapComap i 0 K ≠ f.iterateMapComap i (0 + 1) K
m : ℕ
ih : f.iterateMapComap i m K ≠ f.iterateMapComap i (m + 1) K
⊢ ((fun K => comap f (map i K)) ∘ (fun K => comap f (map i K))^[m]) K ≠
    ((fun K => comap f (map i K)) ∘ (fun K => comap f (map i K))^[m + 1]) K

Tactic:
exact fun H ↦ ih (map_injective_of_injective hi (comap_injective_of_surjective hf H))

Result:
no goals

Proof state:
R : Type u_1
N : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f i : N →ₗ[R] M
K : Submodule R N
m : ℕ
heq : f.iterateMapComap i m K = f.iterateMapComap i (m + 1) K
hf : Surjective ⇑f
hi : Injective ⇑i
n : ℕ
⊢ f.iterateMapComap i n K = f.iterateMapComap i (n + 1) K

Tactic:
induction n with
| zero =>
  contrapose! heq
  induction m with
  | zero => exact heq
  | succ m ih =>
    rw [iterateMapComap, iterateMapComap, iterate_succ', iterate_succ']
    exact fun H ↦ ih (map_injective_of_injective hi (comap_injective_of_surjective hf H))
| succ n ih =>
  rw [iterateMapComap, iterateMapComap, iterate_succ', iterate_succ',
    Function.comp_apply, Function.comp_apply, ← iterateMapComap, ← iterateMapComap, ih]

Result:
no goals

Proof state:
case succ
R : Type u_1
N : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f i : N →ₗ[R] M
K : Submodule R N
m : ℕ
heq : f.iterateMapComap i m K = f.iterateMapComap i (m + 1) K
hf : Surjective ⇑f
hi : Injective ⇑i
n : ℕ
ih : f.iterateMapComap i n K = f.iterateMapComap i (n + 1) K
⊢ f.iterateMapComap i (n + 1) K = f.iterateMapComap i (n + 1 + 1) K

Tactic:
rw [iterateMapComap, iterateMapComap, iterate_succ', iterate_succ',
  Function.comp_apply, Function.comp_apply, ← iterateMapComap, ← iterateMapComap, ih]

Result:
no goals

Proof state:
case zero
R : Type u_1
N : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f i : N →ₗ[R] M
K : Submodule R N
m : ℕ
hf : Surjective ⇑f
hi : Injective ⇑i
heq : f.iterateMapComap i 0 K ≠ f.iterateMapComap i (0 + 1) K
⊢ f.iterateMapComap i m K ≠ f.iterateMapComap i (m + 1) K

Tactic:
induction m with
| zero => exact heq
| succ m ih =>
  rw [iterateMapComap, iterateMapComap, iterate_succ', iterate_succ']
  exact fun H ↦ ih (map_injective_of_injective hi (comap_injective_of_surjective hf H))

Result:
no goals

Proof state:
case zero
R : Type u_1
N : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f i : N →ₗ[R] M
K : Submodule R N
m : ℕ
heq : f.iterateMapComap i m K = f.iterateMapComap i (m + 1) K
hf : Surjective ⇑f
hi : Injective ⇑i
⊢ f.iterateMapComap i 0 K = f.iterateMapComap i (0 + 1) K

Tactic:
contrapose! heq

Result:
case zero
R : Type u_1
N : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f i : N →ₗ[R] M
K : Submodule R N
m : ℕ
hf : Surjective ⇑f
hi : Injective ⇑i
heq : f.iterateMapComap i 0 K ≠ f.iterateMapComap i (0 + 1) K
⊢ f.iterateMapComap i m K ≠ f.iterateMapComap i (m + 1) K

Proof state:
case zero.zero
R : Type u_1
N : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f i : N →ₗ[R] M
K : Submodule R N
hf : Surjective ⇑f
hi : Injective ⇑i
heq : f.iterateMapComap i 0 K ≠ f.iterateMapComap i (0 + 1) K
⊢ f.iterateMapComap i 0 K ≠ f.iterateMapComap i (0 + 1) K

Tactic:
exact heq

Result:
no goals

Proof state:
case zero.succ
R : Type u_1
N : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f i : N →ₗ[R] M
K : Submodule R N
hf : Surjective ⇑f
hi : Injective ⇑i
heq : f.iterateMapComap i 0 K ≠ f.iterateMapComap i (0 + 1) K
m : ℕ
ih : f.iterateMapComap i m K ≠ f.iterateMapComap i (m + 1) K
⊢ f.iterateMapComap i (m + 1) K ≠ f.iterateMapComap i (m + 1 + 1) K

Tactic:
rw [iterateMapComap, iterateMapComap, iterate_succ', iterate_succ']

Result:
case zero.succ
R : Type u_1
N : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f i : N →ₗ[R] M
K : Submodule R N
hf : Surjective ⇑f
hi : Injective ⇑i
heq : f.iterateMapComap i 0 K ≠ f.iterateMapComap i (0 + 1) K
m : ℕ
ih : f.iterateMapComap i m K ≠ f.iterateMapComap i (m + 1) K
⊢ ((fun K => comap f (map i K)) ∘ (fun K => comap f (map i K))^[m]) K ≠
    ((fun K => comap f (map i K)) ∘ (fun K => comap f (map i K))^[m + 1]) K