awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Invariant (goal)
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
⊢ 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)
have 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)
Tactic: obtain ⟨q, hq⟩ := q
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Invariant (hypothesis)
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)
⊢ 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)
have hq₁ : Subtype.mk (p := fun (x : M) ↦ x ∈ p) x hx ∈ Submodule.comap (LinearMap.restrict f hp) q
Tactic: specialize hq hx'
Cleared hypotheses: hq
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Invariant (hypothesis)
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 (α := 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)
have 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)) sorry : ↥p)
Tactic: rw [Submodule.mem_comap, LinearMap.restrict_apply] at hq
Cleared hypotheses: hq
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Invariant (goal)
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
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Invariant (hypothesis)
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
⊢ 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
have this : (↑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
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Invariant (goal)
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
⊢ 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
have rw : Submodule.map (↑e : M →ₗ[R] N) p ∈ invtSubmodule (((↑e : M →ₗ[R] N) ∘ₗ f) ∘ₗ (↑e.symm : N →ₗ[R] M)) ↔
  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]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Invariant (goal)
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
⊢ 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
have 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
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]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Invariant (goal)
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
⊢ 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
have 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
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]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Invariant (goal)
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
⊢ 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
have 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
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]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Invariant (goal)
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
⊢ 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
have 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
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]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Invariant (goal)
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
⊢ 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
have 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
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]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Invariant (goal)
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
⊢ 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
have 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
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]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Invariant (goal)
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
⊢ 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
have rw₇ : p ≤ Submodule.comap f p ↔ p ≤ Submodule.comap f p
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]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Invariant (goal)
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
⊢ Membership.mem (γ := Sublattice (Submodule R M)) (invtSubmodule (DistribSMul.toLinearMap R M g))
    (span R (MulAction.orbit G x))
have rw : MulAction.orbit G x ⊆ (⇑(DistribSMul.toLinearMap R M g) : (a : M) → M) ⁻¹' (↑(span R (MulAction.orbit G x)) : Set M)
Tactic: rw [mem_invtSubmodule, Submodule.span_le, Submodule.comap_coe]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.Invariant (goal)
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 (γ := Set M)
    ((⇑(DistribSMul.toLinearMap R M g) : (a : M) → M) ⁻¹' (↑(span R (MulAction.orbit G x)) : Set M)) y
have simp : Membership.mem (γ := Submodule R M) (span R (MulAction.orbit G x)) (g • y)
Tactic: simp only [Set.mem_preimage, DistribSMul.toLinearMap_apply, SetLike.mem_coe]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.IterateMapComap (goal)
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 : ℕ
⊢ f.iterateMapComap i n K ≤ f.iterateMapComap i (n + 1) K
have nth_rw : f.iterateMapComap i n K ≤ (fun (K : Submodule R N) ↦ comap f (map i K))^[n + 1] K
Tactic: nth_rw 2 [iterateMapComap]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.IterateMapComap (goal)
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 : ℕ
⊢ f.iterateMapComap i n K ≤ (fun (K : Submodule R N) ↦ comap f (map i K))^[n + 1] K
have rw : map f (f.iterateMapComap i n K) ≤ map i (f.iterateMapComap i n K)
Tactic: rw [iterate_succ', Function.comp_apply, ← iterateMapComap, ← map_le_iff_le_comap]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.IterateMapComap (goal)
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 + 1) K) ≤ map i (f.iterateMapComap i (n + 1) K)
have 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)))
Tactic: simp_rw [iterateMapComap, iterate_succ', Function.comp_apply]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.IterateMapComap (goal)
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 i (f.iterateMapComap i n K) ≤ map i (comap f (map f (f.iterateMapComap i n K)))
have grw : map i (f.iterateMapComap i n K) ≤ map i (f.iterateMapComap i n K)
Tactic: grw [← le_comap_map]
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.IterateMapComap (goal)
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 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)))
have a : map f (f.iterateMapComap i n K) ≤ map i ((fun (K : Submodule R N) ↦ comap f (map i K))^[n] K)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.IterateMapComap (goal)
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 : ℕ
⊢ map f (f.iterateMapComap i n K) ≤ map i (f.iterateMapComap i n K)
have zero : map f (f.iterateMapComap i 0 K) ≤ map i (f.iterateMapComap i 0 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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.IterateMapComap (goal)
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)
⊢ map f (f.iterateMapComap i n K) ≤ map i (f.iterateMapComap i n K)
have 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)
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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.IterateMapComap (goal)
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)
⊢ f.iterateMapComap i 0 K = f.iterateMapComap i (HAdd.hAdd (α := ℕ) 0 1) K
have 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
Tactic: contrapose! heq
Cleared hypotheses: heq
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.IterateMapComap (goal)
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
⊢ f.iterateMapComap i (m + 1) K ≠ f.iterateMapComap i (m + 1 + 1) K
have 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)
Tactic: rw [iterateMapComap, iterateMapComap, iterate_succ', iterate_succ']
-- Lean 4 proof step from Mathlib.Algebra.Module.Submodule.IterateMapComap (goal)
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
⊢ f.iterateMapComap i m K ≠ f.iterateMapComap i (m + 1) K
have 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
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))
Cleared hypotheses: m