-- Mathlib/Algebra/Module/Submodule/Map.lean
theorem _root_.LinearMap.iInf_invariant {σ : R →+* R} [RingHomSurjective σ] {ι : Sort*}
    (f : M →ₛₗ[σ] M) {p : ι → Submodule R M} (hf : ∀ i, ∀ v ∈ p i, f v ∈ p i) :
    ∀ v ∈ iInf p, f v ∈ iInf p

Proof state:
R : Type u_1
M : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
σ : R →+* R
inst✝ : RingHomSurjective σ
ι : Sort u_10
f : M →ₛₗ[σ] M
p : ι → Submodule R M
hf : ∀ (i : ι), ∀ v ∈ p i, f v ∈ p i
⊢ ∀ (i : ι), map f (p i) ≤ p i

Tactic:
rintro i - ⟨v, hv, rfl⟩

Result:
case intro.intro
R : Type u_1
M : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
σ : R →+* R
inst✝ : RingHomSurjective σ
ι : Sort u_10
f : M →ₛₗ[σ] M
p : ι → Submodule R M
hf : ∀ (i : ι), ∀ v ∈ p i, f v ∈ p i
i : ι
v : M
hv : v ∈ ↑(p i)
⊢ f v ∈ p i

Proof state:
R : Type u_1
M : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
σ : R →+* R
inst✝ : RingHomSurjective σ
ι : Sort u_10
f : M →ₛₗ[σ] M
p : ι → Submodule R M
hf : ∀ (i : ι), ∀ v ∈ p i, f v ∈ p i
this✝ : ∀ (i : ι), map f (p i) ≤ p i
this : map f (iInf p) ≤ iInf p
⊢ ∀ v ∈ iInf p, f v ∈ iInf p

Tactic:
exact fun v hv => this ⟨v, hv, rfl⟩

Result:
no goals

Proof state:
case intro.intro
R : Type u_1
M : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
σ : R →+* R
inst✝ : RingHomSurjective σ
ι : Sort u_10
f : M →ₛₗ[σ] M
p : ι → Submodule R M
hf : ∀ (i : ι), ∀ v ∈ p i, f v ∈ p i
i : ι
v : M
hv : v ∈ ↑(p i)
⊢ f v ∈ p i

Tactic:
exact hf i v hv

Result:
no goals

Proof state:
R : Type u_1
M : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
σ : R →+* R
inst✝ : RingHomSurjective σ
ι : Sort u_10
f : M →ₛₗ[σ] M
p : ι → Submodule R M
hf : ∀ (i : ι), ∀ v ∈ p i, f v ∈ p i
this : ∀ (i : ι), map f (p i) ≤ p i
⊢ ∀ v ∈ iInf p, f v ∈ iInf p

Tactic:
suffices (iInf p).map f ≤ iInf p by exact fun v hv => this ⟨v, hv, rfl⟩

Result:
R : Type u_1
M : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
σ : R →+* R
inst✝ : RingHomSurjective σ
ι : Sort u_10
f : M →ₛₗ[σ] M
p : ι → Submodule R M
hf : ∀ (i : ι), ∀ v ∈ p i, f v ∈ p i
this : ∀ (i : ι), map f (p i) ≤ p i
⊢ map f (iInf p) ≤ iInf p

Proof state:
R : Type u_1
M : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
σ : R →+* R
inst✝ : RingHomSurjective σ
ι : Sort u_10
f : M →ₛₗ[σ] M
p : ι → Submodule R M
hf : ∀ (i : ι), ∀ v ∈ p i, f v ∈ p i
this : ∀ (i : ι), map f (p i) ≤ p i
⊢ map f (iInf p) ≤ iInf p

Tactic:
exact le_iInf fun i => (Submodule.map_mono (iInf_le p i)).trans (this i)

Result:
no goals

Proof state:
R : Type u_1
M : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
σ : R →+* R
inst✝ : RingHomSurjective σ
ι : Sort u_10
f : M →ₛₗ[σ] M
p : ι → Submodule R M
hf : ∀ (i : ι), ∀ v ∈ p i, f v ∈ p i
⊢ ∀ v ∈ iInf p, f v ∈ iInf p

Tactic:
have : ∀ i, (p i).map f ≤ p i := by
  rintro i - ⟨v, hv, rfl⟩
  exact hf i v hv

Result:
R : Type u_1
M : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
σ : R →+* R
inst✝ : RingHomSurjective σ
ι : Sort u_10
f : M →ₛₗ[σ] M
p : ι → Submodule R M
hf : ∀ (i : ι), ∀ v ∈ p i, f v ∈ p i
this : ∀ (i : ι), map f (p i) ≤ p i
⊢ ∀ v ∈ iInf p, f v ∈ iInf p