awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.Submodule.Invariant
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : End R M
p q : ↥f.invtSubmodule
obtain :
  ∀ (p : Submodule R M) (hp : p ∈ f.invtSubmodule),
    IsCompl (Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ f.invtSubmodule) p hp) q ↔
      IsCompl (↑(Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ f.invtSubmodule) p hp) : Submodule R M)
        (↑q : Submodule R M)
⊢ IsCompl p q ↔ IsCompl (↑p : Submodule R M) (↑q : Submodule R M)

Tactic:
obtain ⟨p, hp⟩ := p
-- Module: Mathlib.Algebra.Module.Submodule.Invariant
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : End R M
q : ↥f.invtSubmodule
p : Submodule R M
hp : p ∈ f.invtSubmodule
obtain :
  ∀ (q : Submodule R M) (hq : q ∈ f.invtSubmodule),
    IsCompl (Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ f.invtSubmodule) p hp)
        (Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ f.invtSubmodule) q hq) ↔
      IsCompl (↑(Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ f.invtSubmodule) p hp) : Submodule R M)
        (↑(Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ f.invtSubmodule) q hq) : Submodule R M)
⊢ IsCompl (Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ f.invtSubmodule) p hp) q ↔
    IsCompl (↑(Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ f.invtSubmodule) p hp) : Submodule R M)
      (↑q : Submodule R M)

Tactic:
obtain ⟨q, hq⟩ := q
-- Module: Mathlib.Algebra.Module.Submodule.Invariant
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
q : Submodule R M
hq : q ∈ f.invtSubmodule
⊢ IsCompl (Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ f.invtSubmodule) p hp)
      (Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ f.invtSubmodule) q hq) ↔
    IsCompl (↑(Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ f.invtSubmodule) p hp) : Submodule R M)
      (↑(Subtype.mk (p := fun (x : Submodule R M) ↦ x ∈ f.invtSubmodule) q hq) : Submodule R M)

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Submodule.Invariant
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
q : Submodule R ↥p
hq : q ∈ invtSubmodule (LinearMap.restrict f hp)
x : M
hx : x ∈ p
hx' : Subtype.mk (p := fun (x : M) ↦ x ∈ p) x hx ∈ (↑q : Set ↥p)
⊢ Subtype.mk (p := fun (x : M) ↦ x ∈ p) x hx ∈ Submodule.comap (LinearMap.restrict f hp) q

Tactic:
specialize hq hx'
-- Module: Mathlib.Algebra.Module.Submodule.Invariant
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
q : Submodule R ↥p
x : M
hx : x ∈ p
hx' : Subtype.mk (p := fun (x : M) ↦ x ∈ p) x hx ∈ (↑q : Set ↥p)
hq : Subtype.mk (p := fun (x : M) ↦ x ∈ p) x hx ∈ Submodule.comap (LinearMap.restrict f hp) q
⊢ Membership.mem (α := ↥p) q
    (Subtype.mk (p := fun (x : M) ↦ x ∈ p) ((f : (a : M) → M) (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ p) x hx) : M)) ⋯ :
      ↥p)

Tactic:
rw [Submodule.mem_comap, LinearMap.restrict_apply] at hq

Premises used: Submodule.mem_comap, LinearMap.restrict_apply
-- Module: Mathlib.Algebra.Module.Submodule.Invariant
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
q : Submodule R ↥p
x : M
hx : x ∈ p
hx' : Subtype.mk (p := fun (x : M) ↦ x ∈ p) x hx ∈ (↑q : Set ↥p)
hq :
  Membership.mem (α := ↥p) q
    (Subtype.mk (p := fun (x : M) ↦ x ∈ p) ((f : (a : M) → M) (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ p) x hx) : M)) ⋯ :
      ↥p)
⊢ Membership.mem (α := M) (Submodule.comap f (Submodule.map p.subtype q))
    ((p.subtype : (a : ↥p) → M) (Subtype.mk (p := fun (x : M) ↦ x ∈ p) x hx) : M)

Tactic:
simpa [hq] using hp hx
-- Module: Mathlib.Algebra.Module.Submodule.Invariant
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : End R M
p : Submodule R M
g : End R M
hf : p ∈ f.invtSubmodule
hg : p ∈ g.invtSubmodule
⊢ p ∈ invtSubmodule (f ∘ₗ g)

Tactic:
fun _ hx ↦ hf (hg hx)

Premises used: Set.Mem, setOf, Set.preimage
-- Module: Mathlib.Algebra.Module.Submodule.Invariant
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : End R M
e : M ≃ₗ[R] N
p : Submodule R M
h :
  ∀ (x : M),
    Eq (α := M)
      (((↑e.symm : N →ₗ[R] M) ∘ₗ (((↑e : M →ₗ[R] N) ∘ₗ f) ∘ₗ (↑e.symm : N →ₗ[R] M)) ∘ₗ (↑e : M →ₗ[R] N) : (a : M) → M)
          x :
        M)
      ((f : (a : M) → M) x : M)
⊢ (↑e.symm : N →ₗ[R] M) ∘ₗ (((↑e : M →ₗ[R] N) ∘ₗ f) ∘ₗ (↑e.symm : N →ₗ[R] M)) ∘ₗ (↑e : M →ₗ[R] N) = f

Tactic:
ext
-- Module: Mathlib.Algebra.Module.Submodule.Invariant
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : End R M
e : M ≃ₗ[R] N
p : Submodule R M
x : M
⊢ Eq (α := M)
    (((↑e.symm : N →ₗ[R] M) ∘ₗ (((↑e : M →ₗ[R] N) ∘ₗ f) ∘ₗ (↑e.symm : N →ₗ[R] M)) ∘ₗ (↑e : M →ₗ[R] N) : (a : M) → M) x :
      M)
    ((f : (a : M) → M) x : M)

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Submodule.Invariant
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : End R M
e : M ≃ₗ[R] N
p : Submodule R M
⊢ (↑e.symm : N →ₗ[R] M) ∘ₗ (((↑e : M →ₗ[R] N) ∘ₗ f) ∘ₗ (↑e.symm : N →ₗ[R] M)) ∘ₗ (↑e : M →ₗ[R] N) = f

Tactic:
have : e.symm.toLinearMap ∘ₗ ((e ∘ₗ f) ∘ₗ e.symm.toLinearMap) ∘ₗ e = f := by ext; simp
-- Module: Mathlib.Algebra.Module.Submodule.Invariant
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : End R M
e : M ≃ₗ[R] N
p : Submodule R M
this : (↑e.symm : N →ₗ[R] M) ∘ₗ (((↑e : M →ₗ[R] N) ∘ₗ f) ∘ₗ (↑e.symm : N →ₗ[R] M)) ∘ₗ (↑e : M →ₗ[R] N) = f
rw :
  Submodule.map (↑e : M →ₗ[R] N) p ∈ invtSubmodule (((↑e : M →ₗ[R] N) ∘ₗ f) ∘ₗ (↑e.symm : N →ₗ[R] M)) ↔
    p ∈ f.invtSubmodule
rw₁ :
  Submodule.map (↑e : M →ₗ[R] N) p ≤
      Submodule.comap (((↑e : M →ₗ[R] N) ∘ₗ f) ∘ₗ (↑e.symm : N →ₗ[R] M)) (Submodule.map (↑e : M →ₗ[R] N) p) ↔
    p ∈ f.invtSubmodule
rw₂ :
  Submodule.map (↑e : M →ₗ[R] N) p ≤
      Submodule.comap (((↑e : M →ₗ[R] N) ∘ₗ f) ∘ₗ (↑e.symm : N →ₗ[R] M)) (Submodule.map (↑e : M →ₗ[R] N) p) ↔
    p ≤ Submodule.comap f p
rw₃ :
  p ≤
      Submodule.comap (↑e : M →ₗ[R] N)
        (Submodule.comap (((↑e : M →ₗ[R] N) ∘ₗ f) ∘ₗ (↑e.symm : N →ₗ[R] M)) (Submodule.map (↑e : M →ₗ[R] N) p)) ↔
    p ≤ Submodule.comap f p
rw₄ :
  p ≤
      Submodule.comap (↑e : M →ₗ[R] N)
        (Submodule.comap (((↑e : M →ₗ[R] N) ∘ₗ f) ∘ₗ (↑e.symm : N →ₗ[R] M)) (Submodule.comap (↑e.symm : N →ₗ[R] M) p)) ↔
    p ≤ Submodule.comap f p
rw₅ :
  p ≤
      Submodule.comap ((((↑e : M →ₗ[R] N) ∘ₗ f) ∘ₗ (↑e.symm : N →ₗ[R] M)) ∘ₗ (↑e : M →ₗ[R] N))
        (Submodule.comap (↑e.symm : N →ₗ[R] M) p) ↔
    p ≤ Submodule.comap f p
rw₆ :
  p ≤
      Submodule.comap ((↑e.symm : N →ₗ[R] M) ∘ₗ (((↑e : M →ₗ[R] N) ∘ₗ f) ∘ₗ (↑e.symm : N →ₗ[R] M)) ∘ₗ (↑e : M →ₗ[R] N))
        p ↔
    p ≤ Submodule.comap f p
rw₇ rw₈ : p ≤ Submodule.comap f p ↔ p ≤ Submodule.comap f p
⊢ Membership.mem (γ := Sublattice (Submodule R N)) (invtSubmodule ((e.conj : (a : End R M) → End R N) f))
      (Submodule.map (↑e : M →ₗ[R] N) p) ↔
    p ∈ f.invtSubmodule

Tactic:
rw [LinearEquiv.conj_apply, mem_invtSubmodule, mem_invtSubmodule, Submodule.map_le_iff_le_comap,
    Submodule.map_equiv_eq_comap_symm, ← Submodule.comap_comp, ← Submodule.comap_comp, this]

Premises used: Module.End.mem_invtSubmodule, LinearEquiv.conj_apply, Submodule.map_equiv_eq_comap_symm, Submodule.comap_comp, Submodule.map_le_iff_le_comap
-- Module: Mathlib.Algebra.Module.Submodule.Invariant
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : End R N
e : M ≃ₗ[R] N
p : Submodule R M
⊢ Submodule.map (↑e : M →ₗ[R] N) p ∈ f.invtSubmodule ↔
    Membership.mem (γ := Sublattice (Submodule R M)) (invtSubmodule ((e.symm.conj : (a : End R N) → End R M) f)) p

Tactic:
simp [← e.map_mem_invtSubmodule_conj_iff]

Premises used: LinearEquiv.map_mem_invtSubmodule_conj_iff
-- Module: Mathlib.Algebra.Module.Submodule.Invariant
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
G : Type u_3
inst_3 : Monoid G
inst_4 : DistribMulAction G M
inst_5 : SMulCommClass G R M
x : M
g : G
rw :
  MulAction.orbit G x ⊆ (⇑(DistribSMul.toLinearMap R M g) : (a : M) → M) ⁻¹' (↑(span R (MulAction.orbit G x)) : Set M)
⊢ Membership.mem (γ := Sublattice (Submodule R M)) (invtSubmodule (DistribSMul.toLinearMap R M g))
    (span R (MulAction.orbit G x))

Tactic:
rw [mem_invtSubmodule, Submodule.span_le, Submodule.comap_coe]

Premises used: Module.End.mem_invtSubmodule, Submodule.comap_coe, Submodule.span_le
-- Module: Mathlib.Algebra.Module.Submodule.Invariant
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
G : Type u_3
inst_3 : Monoid G
inst_4 : DistribMulAction G M
inst_5 : SMulCommClass G R M
x : M
g : G
y : M
hy : y ∈ MulAction.orbit G x
simp : Membership.mem (γ := Submodule R M) (span R (MulAction.orbit G x)) (g • y)
⊢ Membership.mem (γ := Set M)
    ((⇑(DistribSMul.toLinearMap R M g) : (a : M) → M) ⁻¹' (↑(span R (MulAction.orbit G x)) : Set M)) y

Tactic:
simp only [Set.mem_preimage, DistribSMul.toLinearMap_apply, SetLike.mem_coe]

Premises used: SetLike.mem_coe, DistribSMul.toLinearMap_apply, Set.mem_preimage
-- Module: Mathlib.Algebra.Module.Submodule.Invariant
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
G : Type u_3
inst_3 : Monoid G
inst_4 : DistribMulAction G M
inst_5 : SMulCommClass G R M
x : M
g : G
y : M
hy : y ∈ MulAction.orbit G x
⊢ Membership.mem (γ := Submodule R M) (span R (MulAction.orbit G x)) (g • y)

Tactic:
Submodule.subset_span <| MulAction.mem_orbit_of_mem_orbit g hy

Premises used: MulAction.mem_orbit_of_mem_orbit, Submodule.subset_span
-- Module: Mathlib.Algebra.Module.Submodule.Invariant
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
G : Type u_3
inst_3 : Monoid G
inst_4 : DistribMulAction G M
inst_5 : SMulCommClass G R M
x : M
g : G
y : M
hy : y ∈ MulAction.orbit G x
⊢ Membership.mem (γ := Submodule R M) (span R (MulAction.orbit G x)) (g • y)

Tactic:
exact Submodule.subset_span <| MulAction.mem_orbit_of_mem_orbit g hy

Premises used: MulAction.mem_orbit_of_mem_orbit, Submodule.subset_span
-- Module: Mathlib.Algebra.Module.Submodule.IterateMapComap
Goal:
R : Type u_1
N : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
inst_3 : AddCommMonoid M
inst_4 : Module R M
f i : N →ₗ[R] M
K : Submodule R N
h : map f K ≤ map i K
n : ℕ
nth_rw : f.iterateMapComap i n K ≤ (fun (K : Submodule R N) ↦ comap f (map i K))^[n + 1] K
⊢ f.iterateMapComap i n K ≤ f.iterateMapComap i (n + 1) K

Tactic:
nth_rw 2 [iterateMapComap]

Premises used: LinearMap.iterateMapComap
-- Module: Mathlib.Algebra.Module.Submodule.IterateMapComap
Goal:
R : Type u_1
N : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
inst_3 : AddCommMonoid M
inst_4 : Module R M
f i : N →ₗ[R] M
K : Submodule R N
h : map f K ≤ map i K
n : ℕ
rw : map f (f.iterateMapComap i n K) ≤ map i (f.iterateMapComap i n K)
⊢ f.iterateMapComap i n K ≤ (fun (K : Submodule R N) ↦ comap f (map i K))^[n + 1] K

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

Premises used: Function.iterate_succ', LinearMap.iterateMapComap, Function.comp_apply, Submodule.map_le_iff_le_comap
-- Module: Mathlib.Algebra.Module.Submodule.IterateMapComap
Goal:
R : Type u_1
N : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
inst_3 : AddCommMonoid M
inst_4 : Module R M
f i : N →ₗ[R] M
K : Submodule R N
h : map f K ≤ map i K
⊢ map f (f.iterateMapComap i 0 K) ≤ map i (f.iterateMapComap i 0 K)

Tactic:
h

Premises used: Set.Mem
-- Module: Mathlib.Algebra.Module.Submodule.IterateMapComap
Goal:
R : Type u_1
N : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
inst_3 : AddCommMonoid M
inst_4 : Module R M
f i : N →ₗ[R] M
K : Submodule R N
h : map f K ≤ map i K
⊢ map f (f.iterateMapComap i 0 K) ≤ map i (f.iterateMapComap i 0 K)

Tactic:
exact h
-- Module: Mathlib.Algebra.Module.Submodule.IterateMapComap
Goal:
R : Type u_1
N : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
inst_3 : AddCommMonoid M
inst_4 : Module R M
f i : N →ₗ[R] M
K : Submodule R N
h : map f K ≤ map i K
n : ℕ
ih : map f (f.iterateMapComap i n K) ≤ map i (f.iterateMapComap i n K)
succ :
  map f (comap f (map i ((fun (K : Submodule R N) ↦ comap f (map i K))^[n] K))) ≤
    map i (comap f (map i ((fun (K : Submodule R N) ↦ comap f (map i K))^[n] K)))
⊢ map f (f.iterateMapComap i (n + 1) K) ≤ map i (f.iterateMapComap i (n + 1) K)

Tactic:
simp_rw [iterateMapComap, iterate_succ', Function.comp_apply]

Premises used: Function.iterate_succ', LinearMap.iterateMapComap, Function.comp_apply
-- Module: Mathlib.Algebra.Module.Submodule.IterateMapComap
Goal:
R : Type u_1
N : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
inst_3 : AddCommMonoid M
inst_4 : Module R M
f i : N →ₗ[R] M
K : Submodule R N
h : map f K ≤ map i K
n : ℕ
ih : map f (f.iterateMapComap i n K) ≤ map i (f.iterateMapComap i n K)
⊢ map f (comap f (map i (f.iterateMapComap i n K))) ≤ map i (f.iterateMapComap i n K)

Tactic:
map_comap_le _ _

Premises used: Submodule.map_comap_le
-- Module: Mathlib.Algebra.Module.Submodule.IterateMapComap
Goal:
R : Type u_1
N : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
inst_3 : AddCommMonoid M
inst_4 : Module R M
f i : N →ₗ[R] M
K : Submodule R N
h : map f K ≤ map i K
n : ℕ
ih : map f (f.iterateMapComap i n K) ≤ map i (f.iterateMapComap i n K)
grw grw₁ : map i (f.iterateMapComap i n K) ≤ map i (f.iterateMapComap i n K)
⊢ map i (f.iterateMapComap i n K) ≤ map i (comap f (map f (f.iterateMapComap i n K)))

Tactic:
grw [← le_comap_map]

Premises used: Submodule.le_comap_map
-- Module: Mathlib.Algebra.Module.Submodule.IterateMapComap
Goal:
R : Type u_1
N : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
inst_3 : AddCommMonoid M
inst_4 : Module R M
f i : N →ₗ[R] M
K : Submodule R N
h : map f K ≤ map i K
n : ℕ
ih : map f (f.iterateMapComap i n K) ≤ map i (f.iterateMapComap i n K)
a : map f (f.iterateMapComap i n K) ≤ map i ((fun (K : Submodule R N) ↦ comap f (map i K))^[n] K)
⊢ map i (comap f (map f (f.iterateMapComap i n K))) ≤
    map i (comap f (map i ((fun (K : Submodule R N) ↦ comap f (map i K))^[n] K)))

Tactic:
gcongr
-- Module: Mathlib.Algebra.Module.Submodule.IterateMapComap
Goal:
R : Type u_1
N : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
inst_3 : AddCommMonoid M
inst_4 : Module R M
f i : N →ₗ[R] M
K : Submodule R N
h : map f K ≤ map i K
n : ℕ
ih : map f (f.iterateMapComap i n K) ≤ map i (f.iterateMapComap i n K)
⊢ map f (f.iterateMapComap i n K) ≤ map i ((fun (K : Submodule R N) ↦ comap f (map i K))^[n] K)

Tactic:
ih

Premises used: Set.Mem
-- Module: Mathlib.Algebra.Module.Submodule.IterateMapComap
Goal:
R : Type u_1
N : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
inst_3 : AddCommMonoid M
inst_4 : Module R M
f i : N →ₗ[R] M
K : Submodule R N
h : map f K ≤ map i K
n : ℕ
ih : map f (f.iterateMapComap i n K) ≤ map i (f.iterateMapComap i n K)
⊢ map f (f.iterateMapComap i n K) ≤ map i ((fun (K : Submodule R N) ↦ comap f (map i K))^[n] K)

Tactic:
exact ih
-- Module: Mathlib.Algebra.Module.Submodule.IterateMapComap
Goal:
R : Type u_1
N : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
inst_3 : AddCommMonoid M
inst_4 : Module R M
f i : N →ₗ[R] M
K : Submodule R N
h : map f K ≤ map i K
n : ℕ
zero : map f (f.iterateMapComap i 0 K) ≤ map i (f.iterateMapComap i 0 K)
succ :
  ∀ (n : ℕ) (ih : map f (f.iterateMapComap i n K) ≤ map i (f.iterateMapComap i n K)),
    map f (f.iterateMapComap i (n + 1) K) ≤ map i (f.iterateMapComap i (n + 1) K)
⊢ map f (f.iterateMapComap i n K) ≤ map i (f.iterateMapComap i n K)

Tactic:
induction n with
  | zero => exact h
  | succ n ih =>
    simp_rw [iterateMapComap, iterate_succ', Function.comp_apply]
    calc
      _ ≤ (f.iterateMapComap i n K).map i := map_comap_le _ _
      _ ≤ (((f.iterateMapComap i n K).map f).comap f).map i := by grw [← le_comap_map]
      _ ≤ _ := by gcongr; exact ih

Premises used: Function.iterate_succ', LinearMap.iterateMapComap, Submodule.comap, Submodule.zero, Function.comp_apply, Submodule.map_comap_le, Submodule.map
-- Module: Mathlib.Algebra.Module.Submodule.IterateMapComap
Goal:
R : Type u_1
N : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
inst_3 : AddCommMonoid M
inst_4 : 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.{u_2 + 1, u_3 + 1} (α := N) (β := M) (⇑f : (a : N) → M)
hi : Injective.{u_2 + 1, u_3 + 1} (α := N) (β := M) (⇑i : (a : N) → M)
zero :
  ∀ (heq : f.iterateMapComap i 0 K ≠ f.iterateMapComap i (HAdd.hAdd (α := ℕ) 0 1) K),
    f.iterateMapComap i m K ≠ f.iterateMapComap i (m + 1) K
⊢ f.iterateMapComap i 0 K = f.iterateMapComap i (HAdd.hAdd (α := ℕ) 0 1) K

Tactic:
contrapose! heq
-- Module: Mathlib.Algebra.Module.Submodule.IterateMapComap
Goal:
R : Type u_1
N : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
inst_3 : AddCommMonoid M
inst_4 : Module R M
f i : N →ₗ[R] M
K : Submodule R N
hf : Surjective.{u_2 + 1, u_3 + 1} (α := N) (β := M) (⇑f : (a : N) → M)
hi : Injective.{u_2 + 1, u_3 + 1} (α := N) (β := M) (⇑i : (a : N) → M)
heq : f.iterateMapComap i 0 K ≠ f.iterateMapComap i (HAdd.hAdd (α := ℕ) 0 1) K
⊢ f.iterateMapComap i 0 K ≠ f.iterateMapComap i (HAdd.hAdd (α := ℕ) 0 1) K

Tactic:
heq
-- Module: Mathlib.Algebra.Module.Submodule.IterateMapComap
Goal:
R : Type u_1
N : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
inst_3 : AddCommMonoid M
inst_4 : Module R M
f i : N →ₗ[R] M
K : Submodule R N
hf : Surjective.{u_2 + 1, u_3 + 1} (α := N) (β := M) (⇑f : (a : N) → M)
hi : Injective.{u_2 + 1, u_3 + 1} (α := N) (β := M) (⇑i : (a : N) → M)
heq : f.iterateMapComap i 0 K ≠ f.iterateMapComap i (HAdd.hAdd (α := ℕ) 0 1) K
⊢ f.iterateMapComap i 0 K ≠ f.iterateMapComap i (HAdd.hAdd (α := ℕ) 0 1) K

Tactic:
exact heq
-- Module: Mathlib.Algebra.Module.Submodule.IterateMapComap
Goal:
R : Type u_1
N : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
inst_3 : AddCommMonoid M
inst_4 : Module R M
f i : N →ₗ[R] M
K : Submodule R N
hf : Surjective.{u_2 + 1, u_3 + 1} (α := N) (β := M) (⇑f : (a : N) → M)
hi : Injective.{u_2 + 1, u_3 + 1} (α := N) (β := M) (⇑i : (a : N) → M)
heq : f.iterateMapComap i 0 K ≠ f.iterateMapComap i (HAdd.hAdd (α := ℕ) 0 1) K
m : ℕ
ih : f.iterateMapComap i m K ≠ f.iterateMapComap i (m + 1) K
zero :
  Ne (α := Submodule R N)
    (((fun (K : Submodule R N) ↦ comap f (map i K)) ∘ (fun (K : Submodule R N) ↦ comap f (map i K))^[m]) K)
    (((fun (K : Submodule R N) ↦ comap f (map i K)) ∘ (fun (K : Submodule R N) ↦ comap f (map i K))^[m + 1]) K)
⊢ f.iterateMapComap i (m + 1) K ≠ f.iterateMapComap i (m + 1 + 1) K

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

Premises used: Function.iterate_succ', LinearMap.iterateMapComap
-- Module: Mathlib.Algebra.Module.Submodule.IterateMapComap
Goal:
R : Type u_1
N : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
inst_3 : AddCommMonoid M
inst_4 : Module R M
f i : N →ₗ[R] M
K : Submodule R N
hf : Surjective.{u_2 + 1, u_3 + 1} (α := N) (β := M) (⇑f : (a : N) → M)
hi : Injective.{u_2 + 1, u_3 + 1} (α := N) (β := M) (⇑i : (a : N) → M)
heq : f.iterateMapComap i 0 K ≠ f.iterateMapComap i (HAdd.hAdd (α := ℕ) 0 1) K
m : ℕ
ih : f.iterateMapComap i m K ≠ f.iterateMapComap i (m + 1) K
⊢ Ne (α := Submodule R N)
    (((fun (K : Submodule R N) ↦ comap f (map i K)) ∘ (fun (K : Submodule R N) ↦ comap f (map i K))^[m]) K)
    (((fun (K : Submodule R N) ↦ comap f (map i K)) ∘ (fun (K : Submodule R N) ↦ comap f (map i K))^[m + 1]) K)

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

Premises used: Submodule.comap_injective_of_surjective, Not, Submodule.map_injective_of_injective
-- Module: Mathlib.Algebra.Module.Submodule.IterateMapComap
Goal:
R : Type u_1
N : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
inst_3 : AddCommMonoid M
inst_4 : Module R M
f i : N →ₗ[R] M
K : Submodule R N
hf : Surjective.{u_2 + 1, u_3 + 1} (α := N) (β := M) (⇑f : (a : N) → M)
hi : Injective.{u_2 + 1, u_3 + 1} (α := N) (β := M) (⇑i : (a : N) → M)
heq : f.iterateMapComap i 0 K ≠ f.iterateMapComap i (HAdd.hAdd (α := ℕ) 0 1) K
m : ℕ
ih : f.iterateMapComap i m K ≠ f.iterateMapComap i (m + 1) K
⊢ Ne (α := Submodule R N)
    (((fun (K : Submodule R N) ↦ comap f (map i K)) ∘ (fun (K : Submodule R N) ↦ comap f (map i K))^[m]) K)
    (((fun (K : Submodule R N) ↦ comap f (map i K)) ∘ (fun (K : Submodule R N) ↦ comap f (map i K))^[m + 1]) K)

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

Premises used: Submodule.comap_injective_of_surjective, Submodule.map_injective_of_injective
-- Module: Mathlib.Algebra.Module.Submodule.IterateMapComap
Goal:
R : Type u_1
N : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
inst_3 : AddCommMonoid M
inst_4 : Module R M
f i : N →ₗ[R] M
K : Submodule R N
m : ℕ
hf : Surjective.{u_2 + 1, u_3 + 1} (α := N) (β := M) (⇑f : (a : N) → M)
hi : Injective.{u_2 + 1, u_3 + 1} (α := N) (β := M) (⇑i : (a : N) → M)
heq zero : f.iterateMapComap i 0 K ≠ f.iterateMapComap i (HAdd.hAdd (α := ℕ) 0 1) K
zero₁ :
  ∀ (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
⊢ 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))

Premises used: Function.iterate_succ', LinearMap.iterateMapComap, Submodule.zero