ι : Type ?u.26829
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : ι → M
N O : Submodule R M
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
y : M
yN : y ∈ N
ϕy_eq : ↑ϕ { val := y, property := (_ : y ∈ O) } = generator (LinearMap.submoduleImage ϕ N)
ψ : { x // x ∈ O } →ₗ[R] R
a : R := generator (LinearMap.submoduleImage ϕ N)
⊢ generator (LinearMap.submoduleImage ϕ N) ∣ ↑ψ { val := y, property := (_ : y ∈ O) }
ι : Type ?u.26829
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : ι → M
N O : Submodule R M
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
y : M
yN : y ∈ N
ϕy_eq : ↑ϕ { val := y, property := (_ : y ∈ O) } = generator (LinearMap.submoduleImage ϕ N)
ψ : { x // x ∈ O } →ₗ[R] R
⊢ generator (LinearMap.submoduleImage ϕ N) ∣ ↑ψ { val := y, property := (_ : y ∈ O) }
let a : R := generator (ϕ.submoduleImage N)
ι : Type ?u.26829
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : ι → M
N O : Submodule R M
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
y : M
yN : y ∈ N
ϕy_eq : ↑ϕ { val := y, property := (_ : y ∈ O) } = generator (LinearMap.submoduleImage ϕ N)
ψ : { x // x ∈ O } →ₗ[R] R
a : R := generator (LinearMap.submoduleImage ϕ N)
d : R := generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }})
⊢ generator (LinearMap.submoduleImage ϕ N) ∣ ↑ψ { val := y, property := (_ : y ∈ O) }
ι : Type ?u.26829
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : ι → M
N O : Submodule R M
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
y : M
yN : y ∈ N
ϕy_eq : ↑ϕ { val := y, property := (_ : y ∈ O) } = generator (LinearMap.submoduleImage ϕ N)
ψ : { x // x ∈ O } →ₗ[R] R
a : R := generator (LinearMap.submoduleImage ϕ N)
⊢ generator (LinearMap.submoduleImage ϕ N) ∣ ↑ψ { val := y, property := (_ : y ∈ O) }
let d : R := IsPrincipal.generator (Submodule.span R {a, ψ ⟨y, hNO yN⟩})
ι : Type ?u.26829
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : ι → M
N O : Submodule R M
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
y : M
yN : y ∈ N
ϕy_eq : ↑ϕ { val := y, property := (_ : y ∈ O) } = generator (LinearMap.submoduleImage ϕ N)
ψ : { x // x ∈ O } →ₗ[R] R
a : R := generator (LinearMap.submoduleImage ϕ N)
d : R := generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }})
d_dvd_left : d ∣ a
⊢ generator (LinearMap.submoduleImage ϕ N) ∣ ↑ψ { val := y, property := (_ : y ∈ O) }
ι : Type ?u.26829
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : ι → M
N O : Submodule R M
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
y : M
yN : y ∈ N
ϕy_eq : ↑ϕ { val := y, property := (_ : y ∈ O) } = generator (LinearMap.submoduleImage ϕ N)
ψ : { x // x ∈ O } →ₗ[R] R
a : R := generator (LinearMap.submoduleImage ϕ N)
d : R := generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }})
⊢ generator (LinearMap.submoduleImage ϕ N) ∣ ↑ψ { val := y, property := (_ : y ∈ O) }
have d_dvd_left : d ∣ a := (mem_iff_generator_dvd _).mp (subset_span (mem_insert _ _))
ι : Type ?u.26829
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : ι → M
N O : Submodule R M
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
y : M
yN : y ∈ N
ϕy_eq : ↑ϕ { val := y, property := (_ : y ∈ O) } = generator (LinearMap.submoduleImage ϕ N)
ψ : { x // x ∈ O } →ₗ[R] R
a : R := generator (LinearMap.submoduleImage ϕ N)
d : R := generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ↑ψ { val := y, property := (_ : y ∈ O) }
⊢ generator (LinearMap.submoduleImage ϕ N) ∣ ↑ψ { val := y, property := (_ : y ∈ O) }
ι : Type ?u.26829
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : ι → M
N O : Submodule R M
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
y : M
yN : y ∈ N
ϕy_eq : ↑ϕ { val := y, property := (_ : y ∈ O) } = generator (LinearMap.submoduleImage ϕ N)
ψ : { x // x ∈ O } →ₗ[R] R
a : R := generator (LinearMap.submoduleImage ϕ N)
d : R := generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }})
d_dvd_left : d ∣ a
⊢ generator (LinearMap.submoduleImage ϕ N) ∣ ↑ψ { val := y, property := (_ : y ∈ O) }
have d_dvd_right : d ∣ ψ ⟨y, hNO yN⟩ :=
  (mem_iff_generator_dvd _).mp (subset_span (mem_insert_of_mem _ (mem_singleton _)))
ι : Type ?u.26829
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : ι → M
N O : Submodule R M
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
y : M
yN : y ∈ N
ϕy_eq : ↑ϕ { val := y, property := (_ : y ∈ O) } = generator (LinearMap.submoduleImage ϕ N)
ψ : { x // x ∈ O } →ₗ[R] R
a : R := generator (LinearMap.submoduleImage ϕ N)
d : R := generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ↑ψ { val := y, property := (_ : y ∈ O) }
⊢ generator (LinearMap.submoduleImage ϕ N) ∣ d
ι : Type ?u.26829
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : ι → M
N O : Submodule R M
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
y : M
yN : y ∈ N
ϕy_eq : ↑ϕ { val := y, property := (_ : y ∈ O) } = generator (LinearMap.submoduleImage ϕ N)
ψ : { x // x ∈ O } →ₗ[R] R
a : R := generator (LinearMap.submoduleImage ϕ N)
d : R := generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ↑ψ { val := y, property := (_ : y ∈ O) }
⊢ generator (LinearMap.submoduleImage ϕ N) ∣ ↑ψ { val := y, property := (_ : y ∈ O) }
refine' dvd_trans _ d_dvd_right
ι : Type ?u.26829
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : ι → M
N O : Submodule R M
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
y : M
yN : y ∈ N
ϕy_eq : ↑ϕ { val := y, property := (_ : y ∈ O) } = generator (LinearMap.submoduleImage ϕ N)
ψ : { x // x ∈ O } →ₗ[R] R
a : R := generator (LinearMap.submoduleImage ϕ N)
d : R := generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ↑ψ { val := y, property := (_ : y ∈ O) }
⊢ span R {generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }})} =
    span R {generator (LinearMap.submoduleImage ϕ N)}

ι : Type ?u.26829
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : ι → M
N O : Submodule R M
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
y : M
yN : y ∈ N
ϕy_eq : ↑ϕ { val := y, property := (_ : y ∈ O) } = generator (LinearMap.submoduleImage ϕ N)
ψ : { x // x ∈ O } →ₗ[R] R
a : R := generator (LinearMap.submoduleImage ϕ N)
d : R := generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ↑ψ { val := y, property := (_ : y ∈ O) }
⊢ generator (LinearMap.submoduleImage ϕ N) ∈ span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }}
ι : Type ?u.26829
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : ι → M
N O : Submodule R M
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
y : M
yN : y ∈ N
ϕy_eq : ↑ϕ { val := y, property := (_ : y ∈ O) } = generator (LinearMap.submoduleImage ϕ N)
ψ : { x // x ∈ O } →ₗ[R] R
a : R := generator (LinearMap.submoduleImage ϕ N)
d : R := generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ↑ψ { val := y, property := (_ : y ∈ O) }
⊢ generator (LinearMap.submoduleImage ϕ N) ∣ d
rw [dvd_generator_iff, Ideal.span, ←
  span_singleton_generator (Submodule.span R {a, ψ ⟨y, hNO yN⟩})]
case intro.intro
ι : Type ?u.26829
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : ι → M
N O : Submodule R M
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
y : M
yN : y ∈ N
ϕy_eq : ↑ϕ { val := y, property := (_ : y ∈ O) } = generator (LinearMap.submoduleImage ϕ N)
ψ : { x // x ∈ O } →ₗ[R] R
a : R := generator (LinearMap.submoduleImage ϕ N)
d : R := generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ↑ψ { val := y, property := (_ : y ∈ O) }
r₁ r₂ : R
d_eq : d = r₁ * a + r₂ * ↑ψ { val := y, property := (_ : y ∈ O) }
⊢ span R {generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }})} =
    span R {generator (LinearMap.submoduleImage ϕ N)}

ι : Type ?u.26829
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : ι → M
N O : Submodule R M
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
y : M
yN : y ∈ N
ϕy_eq : ↑ϕ { val := y, property := (_ : y ∈ O) } = generator (LinearMap.submoduleImage ϕ N)
ψ : { x // x ∈ O } →ₗ[R] R
a : R := generator (LinearMap.submoduleImage ϕ N)
d : R := generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ↑ψ { val := y, property := (_ : y ∈ O) }
⊢ generator (LinearMap.submoduleImage ϕ N) ∈ span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }}
ι : Type ?u.26829
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : ι → M
N O : Submodule R M
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
y : M
yN : y ∈ N
ϕy_eq : ↑ϕ { val := y, property := (_ : y ∈ O) } = generator (LinearMap.submoduleImage ϕ N)
ψ : { x // x ∈ O } →ₗ[R] R
a : R := generator (LinearMap.submoduleImage ϕ N)
d : R := generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ↑ψ { val := y, property := (_ : y ∈ O) }
⊢ span R {generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }})} =
    span R {generator (LinearMap.submoduleImage ϕ N)}

ι : Type ?u.26829
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : ι → M
N O : Submodule R M
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
y : M
yN : y ∈ N
ϕy_eq : ↑ϕ { val := y, property := (_ : y ∈ O) } = generator (LinearMap.submoduleImage ϕ N)
ψ : { x // x ∈ O } →ₗ[R] R
a : R := generator (LinearMap.submoduleImage ϕ N)
d : R := generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ↑ψ { val := y, property := (_ : y ∈ O) }
⊢ generator (LinearMap.submoduleImage ϕ N) ∈ span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }}
obtain ⟨r₁, r₂, d_eq⟩ : ∃ r₁ r₂ : R, d = r₁ * a + r₂ * ψ ⟨y, hNO yN⟩ := by
  obtain ⟨r₁, r₂', hr₂', hr₁⟩ :=
    mem_span_insert.mp (IsPrincipal.generator_mem (Submodule.span R {a, ψ ⟨y, hNO yN⟩}))
  obtain ⟨r₂, rfl⟩ := mem_span_singleton.mp hr₂'
  exact ⟨r₁, r₂, hr₁⟩
case intro.intro
ι : Type ?u.26829
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : ι → M
N O : Submodule R M
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
y : M
yN : y ∈ N
ϕy_eq : ↑ϕ { val := y, property := (_ : y ∈ O) } = generator (LinearMap.submoduleImage ϕ N)
ψ : { x // x ∈ O } →ₗ[R] R
a : R := generator (LinearMap.submoduleImage ϕ N)
d : R := generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ↑ψ { val := y, property := (_ : y ∈ O) }
r₁ r₂ : R
d_eq : d = r₁ * a + r₂ * ↑ψ { val := y, property := (_ : y ∈ O) }
ψ' : { x // x ∈ O } →ₗ[R] R := r₁ • ϕ + r₂ • ψ
⊢ span R {generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }})} =
    span R {generator (LinearMap.submoduleImage ϕ N)}

ι : Type ?u.26829
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : ι → M
N O : Submodule R M
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
y : M
yN : y ∈ N
ϕy_eq : ↑ϕ { val := y, property := (_ : y ∈ O) } = generator (LinearMap.submoduleImage ϕ N)
ψ : { x // x ∈ O } →ₗ[R] R
a : R := generator (LinearMap.submoduleImage ϕ N)
d : R := generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ↑ψ { val := y, property := (_ : y ∈ O) }
⊢ generator (LinearMap.submoduleImage ϕ N) ∈ span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }}
case intro.intro
ι : Type ?u.26829
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : ι → M
N O : Submodule R M
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
y : M
yN : y ∈ N
ϕy_eq : ↑ϕ { val := y, property := (_ : y ∈ O) } = generator (LinearMap.submoduleImage ϕ N)
ψ : { x // x ∈ O } →ₗ[R] R
a : R := generator (LinearMap.submoduleImage ϕ N)
d : R := generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ↑ψ { val := y, property := (_ : y ∈ O) }
r₁ r₂ : R
d_eq : d = r₁ * a + r₂ * ↑ψ { val := y, property := (_ : y ∈ O) }
⊢ span R {generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }})} =
    span R {generator (LinearMap.submoduleImage ϕ N)}

ι : Type ?u.26829
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : ι → M
N O : Submodule R M
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
y : M
yN : y ∈ N
ϕy_eq : ↑ϕ { val := y, property := (_ : y ∈ O) } = generator (LinearMap.submoduleImage ϕ N)
ψ : { x // x ∈ O } →ₗ[R] R
a : R := generator (LinearMap.submoduleImage ϕ N)
d : R := generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ↑ψ { val := y, property := (_ : y ∈ O) }
⊢ generator (LinearMap.submoduleImage ϕ N) ∈ span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }}
let ψ' : O →ₗ[R] R := r₁ • ϕ + r₂ • ψ
case intro.intro
ι : Type ?u.26829
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : ι → M
N O : Submodule R M
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
y : M
yN : y ∈ N
ϕy_eq : ↑ϕ { val := y, property := (_ : y ∈ O) } = generator (LinearMap.submoduleImage ϕ N)
ψ : { x // x ∈ O } →ₗ[R] R
a : R := generator (LinearMap.submoduleImage ϕ N)
d : R := generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ↑ψ { val := y, property := (_ : y ∈ O) }
r₁ r₂ : R
d_eq : d = r₁ * a + r₂ * ↑ψ { val := y, property := (_ : y ∈ O) }
ψ' : { x // x ∈ O } →ₗ[R] R := r₁ • ϕ + r₂ • ψ
this : span R {d} ≤ LinearMap.submoduleImage ψ' N
⊢ span R {generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }})} =
    span R {generator (LinearMap.submoduleImage ϕ N)}

ι : Type ?u.26829
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : ι → M
N O : Submodule R M
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
y : M
yN : y ∈ N
ϕy_eq : ↑ϕ { val := y, property := (_ : y ∈ O) } = generator (LinearMap.submoduleImage ϕ N)
ψ : { x // x ∈ O } →ₗ[R] R
a : R := generator (LinearMap.submoduleImage ϕ N)
d : R := generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ↑ψ { val := y, property := (_ : y ∈ O) }
⊢ generator (LinearMap.submoduleImage ϕ N) ∈ span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }}
case intro.intro
ι : Type ?u.26829
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : ι → M
N O : Submodule R M
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
y : M
yN : y ∈ N
ϕy_eq : ↑ϕ { val := y, property := (_ : y ∈ O) } = generator (LinearMap.submoduleImage ϕ N)
ψ : { x // x ∈ O } →ₗ[R] R
a : R := generator (LinearMap.submoduleImage ϕ N)
d : R := generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ↑ψ { val := y, property := (_ : y ∈ O) }
r₁ r₂ : R
d_eq : d = r₁ * a + r₂ * ↑ψ { val := y, property := (_ : y ∈ O) }
ψ' : { x // x ∈ O } →ₗ[R] R := r₁ • ϕ + r₂ • ψ
⊢ span R {generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }})} =
    span R {generator (LinearMap.submoduleImage ϕ N)}

ι : Type ?u.26829
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : ι → M
N O : Submodule R M
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
y : M
yN : y ∈ N
ϕy_eq : ↑ϕ { val := y, property := (_ : y ∈ O) } = generator (LinearMap.submoduleImage ϕ N)
ψ : { x // x ∈ O } →ₗ[R] R
a : R := generator (LinearMap.submoduleImage ϕ N)
d : R := generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ↑ψ { val := y, property := (_ : y ∈ O) }
⊢ generator (LinearMap.submoduleImage ϕ N) ∈ span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }}
have : span R {d} ≤ ψ'.submoduleImage N := by
  rw [span_le, singleton_subset_iff, SetLike.mem_coe, LinearMap.mem_submoduleImage_of_le hNO]
  refine' ⟨y, yN, _⟩
  change r₁ * ϕ ⟨y, hNO yN⟩ + r₂ * ψ ⟨y, hNO yN⟩ = d
  rw [d_eq, ϕy_eq]
case intro.intro
ι : Type ?u.26829
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : ι → M
N O : Submodule R M
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
y : M
yN : y ∈ N
ϕy_eq : ↑ϕ { val := y, property := (_ : y ∈ O) } = generator (LinearMap.submoduleImage ϕ N)
ψ : { x // x ∈ O } →ₗ[R] R
a : R := generator (LinearMap.submoduleImage ϕ N)
d : R := generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ↑ψ { val := y, property := (_ : y ∈ O) }
r₁ r₂ : R
d_eq : d = r₁ * a + r₂ * ↑ψ { val := y, property := (_ : y ∈ O) }
ψ' : { x // x ∈ O } →ₗ[R] R := r₁ • ϕ + r₂ • ψ
this : span R {d} ≤ LinearMap.submoduleImage ψ' N
⊢ LinearMap.submoduleImage ψ' N = span R {generator (LinearMap.submoduleImage ϕ N)}

ι : Type ?u.26829
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : ι → M
N O : Submodule R M
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
y : M
yN : y ∈ N
ϕy_eq : ↑ϕ { val := y, property := (_ : y ∈ O) } = generator (LinearMap.submoduleImage ϕ N)
ψ : { x // x ∈ O } →ₗ[R] R
a : R := generator (LinearMap.submoduleImage ϕ N)
d : R := generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ↑ψ { val := y, property := (_ : y ∈ O) }
⊢ generator (LinearMap.submoduleImage ϕ N) ∈ span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }}
case intro.intro
ι : Type ?u.26829
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : ι → M
N O : Submodule R M
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
y : M
yN : y ∈ N
ϕy_eq : ↑ϕ { val := y, property := (_ : y ∈ O) } = generator (LinearMap.submoduleImage ϕ N)
ψ : { x // x ∈ O } →ₗ[R] R
a : R := generator (LinearMap.submoduleImage ϕ N)
d : R := generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ↑ψ { val := y, property := (_ : y ∈ O) }
r₁ r₂ : R
d_eq : d = r₁ * a + r₂ * ↑ψ { val := y, property := (_ : y ∈ O) }
ψ' : { x // x ∈ O } →ₗ[R] R := r₁ • ϕ + r₂ • ψ
this : span R {d} ≤ LinearMap.submoduleImage ψ' N
⊢ span R {generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }})} =
    span R {generator (LinearMap.submoduleImage ϕ N)}

ι : Type ?u.26829
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : ι → M
N O : Submodule R M
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
y : M
yN : y ∈ N
ϕy_eq : ↑ϕ { val := y, property := (_ : y ∈ O) } = generator (LinearMap.submoduleImage ϕ N)
ψ : { x // x ∈ O } →ₗ[R] R
a : R := generator (LinearMap.submoduleImage ϕ N)
d : R := generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ↑ψ { val := y, property := (_ : y ∈ O) }
⊢ generator (LinearMap.submoduleImage ϕ N) ∈ span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }}
refine'
  le_antisymm (this.trans (le_of_eq _)) (Ideal.span_singleton_le_span_singleton.mpr d_dvd_left)
case intro.intro
ι : Type ?u.26829
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : ι → M
N O : Submodule R M
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
y : M
yN : y ∈ N
ϕy_eq : ↑ϕ { val := y, property := (_ : y ∈ O) } = generator (LinearMap.submoduleImage ϕ N)
ψ : { x // x ∈ O } →ₗ[R] R
a : R := generator (LinearMap.submoduleImage ϕ N)
d : R := generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ↑ψ { val := y, property := (_ : y ∈ O) }
r₁ r₂ : R
d_eq : d = r₁ * a + r₂ * ↑ψ { val := y, property := (_ : y ∈ O) }
ψ' : { x // x ∈ O } →ₗ[R] R := r₁ • ϕ + r₂ • ψ
this : span R {d} ≤ LinearMap.submoduleImage ψ' N
⊢ LinearMap.submoduleImage ψ' N = LinearMap.submoduleImage ϕ N

ι : Type ?u.26829
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : ι → M
N O : Submodule R M
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
y : M
yN : y ∈ N
ϕy_eq : ↑ϕ { val := y, property := (_ : y ∈ O) } = generator (LinearMap.submoduleImage ϕ N)
ψ : { x // x ∈ O } →ₗ[R] R
a : R := generator (LinearMap.submoduleImage ϕ N)
d : R := generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ↑ψ { val := y, property := (_ : y ∈ O) }
⊢ generator (LinearMap.submoduleImage ϕ N) ∈ span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }}
case intro.intro
ι : Type ?u.26829
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : ι → M
N O : Submodule R M
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
y : M
yN : y ∈ N
ϕy_eq : ↑ϕ { val := y, property := (_ : y ∈ O) } = generator (LinearMap.submoduleImage ϕ N)
ψ : { x // x ∈ O } →ₗ[R] R
a : R := generator (LinearMap.submoduleImage ϕ N)
d : R := generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ↑ψ { val := y, property := (_ : y ∈ O) }
r₁ r₂ : R
d_eq : d = r₁ * a + r₂ * ↑ψ { val := y, property := (_ : y ∈ O) }
ψ' : { x // x ∈ O } →ₗ[R] R := r₁ • ϕ + r₂ • ψ
this : span R {d} ≤ LinearMap.submoduleImage ψ' N
⊢ LinearMap.submoduleImage ψ' N = span R {generator (LinearMap.submoduleImage ϕ N)}

ι : Type ?u.26829
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : ι → M
N O : Submodule R M
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
y : M
yN : y ∈ N
ϕy_eq : ↑ϕ { val := y, property := (_ : y ∈ O) } = generator (LinearMap.submoduleImage ϕ N)
ψ : { x // x ∈ O } →ₗ[R] R
a : R := generator (LinearMap.submoduleImage ϕ N)
d : R := generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ↑ψ { val := y, property := (_ : y ∈ O) }
⊢ generator (LinearMap.submoduleImage ϕ N) ∈ span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }}
rw [span_singleton_generator]
ι : Type ?u.26829
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : ι → M
N O : Submodule R M
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
y : M
yN : y ∈ N
ϕy_eq : ↑ϕ { val := y, property := (_ : y ∈ O) } = generator (LinearMap.submoduleImage ϕ N)
ψ : { x // x ∈ O } →ₗ[R] R
a : R := generator (LinearMap.submoduleImage ϕ N)
d : R := generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ↑ψ { val := y, property := (_ : y ∈ O) }
r₁ r₂ : R
d_eq : d = r₁ * a + r₂ * ↑ψ { val := y, property := (_ : y ∈ O) }
ψ' : { x // x ∈ O } →ₗ[R] R := r₁ • ϕ + r₂ • ψ
this : span R {d} ≤ LinearMap.submoduleImage ψ' N
⊢ LinearMap.submoduleImage ϕ N ≤ span R {d}

ι : Type ?u.26829
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : ι → M
N O : Submodule R M
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
y : M
yN : y ∈ N
ϕy_eq : ↑ϕ { val := y, property := (_ : y ∈ O) } = generator (LinearMap.submoduleImage ϕ N)
ψ : { x // x ∈ O } →ₗ[R] R
a : R := generator (LinearMap.submoduleImage ϕ N)
d : R := generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ↑ψ { val := y, property := (_ : y ∈ O) }
⊢ generator (LinearMap.submoduleImage ϕ N) ∈ span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }}
case intro.intro
ι : Type ?u.26829
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : ι → M
N O : Submodule R M
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
y : M
yN : y ∈ N
ϕy_eq : ↑ϕ { val := y, property := (_ : y ∈ O) } = generator (LinearMap.submoduleImage ϕ N)
ψ : { x // x ∈ O } →ₗ[R] R
a : R := generator (LinearMap.submoduleImage ϕ N)
d : R := generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ↑ψ { val := y, property := (_ : y ∈ O) }
r₁ r₂ : R
d_eq : d = r₁ * a + r₂ * ↑ψ { val := y, property := (_ : y ∈ O) }
ψ' : { x // x ∈ O } →ₗ[R] R := r₁ • ϕ + r₂ • ψ
this : span R {d} ≤ LinearMap.submoduleImage ψ' N
⊢ LinearMap.submoduleImage ψ' N = LinearMap.submoduleImage ϕ N

ι : Type ?u.26829
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : ι → M
N O : Submodule R M
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
y : M
yN : y ∈ N
ϕy_eq : ↑ϕ { val := y, property := (_ : y ∈ O) } = generator (LinearMap.submoduleImage ϕ N)
ψ : { x // x ∈ O } →ₗ[R] R
a : R := generator (LinearMap.submoduleImage ϕ N)
d : R := generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ↑ψ { val := y, property := (_ : y ∈ O) }
⊢ generator (LinearMap.submoduleImage ϕ N) ∈ span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }}
apply (le_trans _ this).eq_of_not_gt (hϕ ψ')
ι : Type ?u.26829
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : ι → M
N O : Submodule R M
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
y : M
yN : y ∈ N
ϕy_eq : ↑ϕ { val := y, property := (_ : y ∈ O) } = generator (LinearMap.submoduleImage ϕ N)
ψ : { x // x ∈ O } →ₗ[R] R
a : R := generator (LinearMap.submoduleImage ϕ N)
d : R := generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ↑ψ { val := y, property := (_ : y ∈ O) }
r₁ r₂ : R
d_eq : d = r₁ * a + r₂ * ↑ψ { val := y, property := (_ : y ∈ O) }
ψ' : { x // x ∈ O } →ₗ[R] R := r₁ • ϕ + r₂ • ψ
this : span R {d} ≤ LinearMap.submoduleImage ψ' N
⊢ span R {generator (LinearMap.submoduleImage ϕ N)} ≤ span R {d}

ι : Type ?u.26829
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : ι → M
N O : Submodule R M
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
y : M
yN : y ∈ N
ϕy_eq : ↑ϕ { val := y, property := (_ : y ∈ O) } = generator (LinearMap.submoduleImage ϕ N)
ψ : { x // x ∈ O } →ₗ[R] R
a : R := generator (LinearMap.submoduleImage ϕ N)
d : R := generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ↑ψ { val := y, property := (_ : y ∈ O) }
⊢ generator (LinearMap.submoduleImage ϕ N) ∈ span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }}
ι : Type ?u.26829
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : ι → M
N O : Submodule R M
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
y : M
yN : y ∈ N
ϕy_eq : ↑ϕ { val := y, property := (_ : y ∈ O) } = generator (LinearMap.submoduleImage ϕ N)
ψ : { x // x ∈ O } →ₗ[R] R
a : R := generator (LinearMap.submoduleImage ϕ N)
d : R := generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ↑ψ { val := y, property := (_ : y ∈ O) }
r₁ r₂ : R
d_eq : d = r₁ * a + r₂ * ↑ψ { val := y, property := (_ : y ∈ O) }
ψ' : { x // x ∈ O } →ₗ[R] R := r₁ • ϕ + r₂ • ψ
this : span R {d} ≤ LinearMap.submoduleImage ψ' N
⊢ LinearMap.submoduleImage ϕ N ≤ span R {d}

ι : Type ?u.26829
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : ι → M
N O : Submodule R M
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
y : M
yN : y ∈ N
ϕy_eq : ↑ϕ { val := y, property := (_ : y ∈ O) } = generator (LinearMap.submoduleImage ϕ N)
ψ : { x // x ∈ O } →ₗ[R] R
a : R := generator (LinearMap.submoduleImage ϕ N)
d : R := generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ↑ψ { val := y, property := (_ : y ∈ O) }
⊢ generator (LinearMap.submoduleImage ϕ N) ∈ span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }}
rw [← span_singleton_generator (ϕ.submoduleImage N)]
ι : Type ?u.26829
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : ι → M
N O : Submodule R M
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
y : M
yN : y ∈ N
ϕy_eq : ↑ϕ { val := y, property := (_ : y ∈ O) } = generator (LinearMap.submoduleImage ϕ N)
ψ : { x // x ∈ O } →ₗ[R] R
a : R := generator (LinearMap.submoduleImage ϕ N)
d : R := generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ↑ψ { val := y, property := (_ : y ∈ O) }
⊢ generator (LinearMap.submoduleImage ϕ N) ∈ span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }}
ι : Type ?u.26829
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : ι → M
N O : Submodule R M
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
y : M
yN : y ∈ N
ϕy_eq : ↑ϕ { val := y, property := (_ : y ∈ O) } = generator (LinearMap.submoduleImage ϕ N)
ψ : { x // x ∈ O } →ₗ[R] R
a : R := generator (LinearMap.submoduleImage ϕ N)
d : R := generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ↑ψ { val := y, property := (_ : y ∈ O) }
r₁ r₂ : R
d_eq : d = r₁ * a + r₂ * ↑ψ { val := y, property := (_ : y ∈ O) }
ψ' : { x // x ∈ O } →ₗ[R] R := r₁ • ϕ + r₂ • ψ
this : span R {d} ≤ LinearMap.submoduleImage ψ' N
⊢ span R {generator (LinearMap.submoduleImage ϕ N)} ≤ span R {d}

ι : Type ?u.26829
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : ι → M
N O : Submodule R M
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
y : M
yN : y ∈ N
ϕy_eq : ↑ϕ { val := y, property := (_ : y ∈ O) } = generator (LinearMap.submoduleImage ϕ N)
ψ : { x // x ∈ O } →ₗ[R] R
a : R := generator (LinearMap.submoduleImage ϕ N)
d : R := generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ↑ψ { val := y, property := (_ : y ∈ O) }
⊢ generator (LinearMap.submoduleImage ϕ N) ∈ span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }}
exact Ideal.span_singleton_le_span_singleton.mpr d_dvd_left
case intro.intro.intro
ι : Type ?u.26829
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : ι → M
N O : Submodule R M
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
y : M
yN : y ∈ N
ϕy_eq : ↑ϕ { val := y, property := (_ : y ∈ O) } = generator (LinearMap.submoduleImage ϕ N)
ψ : { x // x ∈ O } →ₗ[R] R
a : R := generator (LinearMap.submoduleImage ϕ N)
d : R := generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ↑ψ { val := y, property := (_ : y ∈ O) }
r₁ r₂' : R
hr₂' : r₂' ∈ span R {↑ψ { val := y, property := (_ : y ∈ O) }}
hr₁ : generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }}) = r₁ • a + r₂'
⊢ ∃ r₁ r₂, d = r₁ * a + r₂ * ↑ψ { val := y, property := (_ : y ∈ O) }
ι : Type ?u.26829
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : ι → M
N O : Submodule R M
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
y : M
yN : y ∈ N
ϕy_eq : ↑ϕ { val := y, property := (_ : y ∈ O) } = generator (LinearMap.submoduleImage ϕ N)
ψ : { x // x ∈ O } →ₗ[R] R
a : R := generator (LinearMap.submoduleImage ϕ N)
d : R := generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ↑ψ { val := y, property := (_ : y ∈ O) }
⊢ ∃ r₁ r₂, d = r₁ * a + r₂ * ↑ψ { val := y, property := (_ : y ∈ O) }
obtain ⟨r₁, r₂', hr₂', hr₁⟩ :=
  mem_span_insert.mp (IsPrincipal.generator_mem (Submodule.span R {a, ψ ⟨y, hNO yN⟩}))
case intro.intro.intro.intro
ι : Type ?u.26829
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : ι → M
N O : Submodule R M
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
y : M
yN : y ∈ N
ϕy_eq : ↑ϕ { val := y, property := (_ : y ∈ O) } = generator (LinearMap.submoduleImage ϕ N)
ψ : { x // x ∈ O } →ₗ[R] R
a : R := generator (LinearMap.submoduleImage ϕ N)
d : R := generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ↑ψ { val := y, property := (_ : y ∈ O) }
r₁ r₂ : R
hr₂' : r₂ • ↑ψ { val := y, property := (_ : y ∈ O) } ∈ span R {↑ψ { val := y, property := (_ : y ∈ O) }}
hr₁ :
  generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }}) =
    r₁ • a + r₂ • ↑ψ { val := y, property := (_ : y ∈ O) }
⊢ ∃ r₁ r₂, d = r₁ * a + r₂ * ↑ψ { val := y, property := (_ : y ∈ O) }
case intro.intro.intro
ι : Type ?u.26829
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : ι → M
N O : Submodule R M
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
y : M
yN : y ∈ N
ϕy_eq : ↑ϕ { val := y, property := (_ : y ∈ O) } = generator (LinearMap.submoduleImage ϕ N)
ψ : { x // x ∈ O } →ₗ[R] R
a : R := generator (LinearMap.submoduleImage ϕ N)
d : R := generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ↑ψ { val := y, property := (_ : y ∈ O) }
r₁ r₂' : R
hr₂' : r₂' ∈ span R {↑ψ { val := y, property := (_ : y ∈ O) }}
hr₁ : generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }}) = r₁ • a + r₂'
⊢ ∃ r₁ r₂, d = r₁ * a + r₂ * ↑ψ { val := y, property := (_ : y ∈ O) }
obtain ⟨r₂, rfl⟩ := mem_span_singleton.mp hr₂'
no goals
case intro.intro.intro.intro
ι : Type ?u.26829
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : ι → M
N O : Submodule R M
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
y : M
yN : y ∈ N
ϕy_eq : ↑ϕ { val := y, property := (_ : y ∈ O) } = generator (LinearMap.submoduleImage ϕ N)
ψ : { x // x ∈ O } →ₗ[R] R
a : R := generator (LinearMap.submoduleImage ϕ N)
d : R := generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ↑ψ { val := y, property := (_ : y ∈ O) }
r₁ r₂ : R
hr₂' : r₂ • ↑ψ { val := y, property := (_ : y ∈ O) } ∈ span R {↑ψ { val := y, property := (_ : y ∈ O) }}
hr₁ :
  generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }}) =
    r₁ • a + r₂ • ↑ψ { val := y, property := (_ : y ∈ O) }
⊢ ∃ r₁ r₂, d = r₁ * a + r₂ * ↑ψ { val := y, property := (_ : y ∈ O) }
exact ⟨r₁, r₂, hr₁⟩
ι : Type ?u.26829
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : ι → M
N O : Submodule R M
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
y : M
yN : y ∈ N
ϕy_eq : ↑ϕ { val := y, property := (_ : y ∈ O) } = generator (LinearMap.submoduleImage ϕ N)
ψ : { x // x ∈ O } →ₗ[R] R
a : R := generator (LinearMap.submoduleImage ϕ N)
d : R := generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ↑ψ { val := y, property := (_ : y ∈ O) }
r₁ r₂ : R
d_eq : d = r₁ * a + r₂ * ↑ψ { val := y, property := (_ : y ∈ O) }
ψ' : { x // x ∈ O } →ₗ[R] R := r₁ • ϕ + r₂ • ψ
⊢ ∃ y yN, ↑ψ' { val := y, property := (_ : y ∈ O) } = d
ι : Type ?u.26829
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : ι → M
N O : Submodule R M
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
y : M
yN : y ∈ N
ϕy_eq : ↑ϕ { val := y, property := (_ : y ∈ O) } = generator (LinearMap.submoduleImage ϕ N)
ψ : { x // x ∈ O } →ₗ[R] R
a : R := generator (LinearMap.submoduleImage ϕ N)
d : R := generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ↑ψ { val := y, property := (_ : y ∈ O) }
r₁ r₂ : R
d_eq : d = r₁ * a + r₂ * ↑ψ { val := y, property := (_ : y ∈ O) }
ψ' : { x // x ∈ O } →ₗ[R] R := r₁ • ϕ + r₂ • ψ
⊢ span R {d} ≤ LinearMap.submoduleImage ψ' N
rw [span_le, singleton_subset_iff, SetLike.mem_coe, LinearMap.mem_submoduleImage_of_le hNO]
ι : Type ?u.26829
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : ι → M
N O : Submodule R M
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
y : M
yN : y ∈ N
ϕy_eq : ↑ϕ { val := y, property := (_ : y ∈ O) } = generator (LinearMap.submoduleImage ϕ N)
ψ : { x // x ∈ O } →ₗ[R] R
a : R := generator (LinearMap.submoduleImage ϕ N)
d : R := generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ↑ψ { val := y, property := (_ : y ∈ O) }
r₁ r₂ : R
d_eq : d = r₁ * a + r₂ * ↑ψ { val := y, property := (_ : y ∈ O) }
ψ' : { x // x ∈ O } →ₗ[R] R := r₁ • ϕ + r₂ • ψ
⊢ ↑ψ' { val := y, property := (_ : y ∈ O) } = d
ι : Type ?u.26829
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : ι → M
N O : Submodule R M
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
y : M
yN : y ∈ N
ϕy_eq : ↑ϕ { val := y, property := (_ : y ∈ O) } = generator (LinearMap.submoduleImage ϕ N)
ψ : { x // x ∈ O } →ₗ[R] R
a : R := generator (LinearMap.submoduleImage ϕ N)
d : R := generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ↑ψ { val := y, property := (_ : y ∈ O) }
r₁ r₂ : R
d_eq : d = r₁ * a + r₂ * ↑ψ { val := y, property := (_ : y ∈ O) }
ψ' : { x // x ∈ O } →ₗ[R] R := r₁ • ϕ + r₂ • ψ
⊢ ∃ y yN, ↑ψ' { val := y, property := (_ : y ∈ O) } = d
refine' ⟨y, yN, _⟩
ι : Type ?u.26829
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : ι → M
N O : Submodule R M
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
y : M
yN : y ∈ N
ϕy_eq : ↑ϕ { val := y, property := (_ : y ∈ O) } = generator (LinearMap.submoduleImage ϕ N)
ψ : { x // x ∈ O } →ₗ[R] R
a : R := generator (LinearMap.submoduleImage ϕ N)
d : R := generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ↑ψ { val := y, property := (_ : y ∈ O) }
r₁ r₂ : R
d_eq : d = r₁ * a + r₂ * ↑ψ { val := y, property := (_ : y ∈ O) }
ψ' : { x // x ∈ O } →ₗ[R] R := r₁ • ϕ + r₂ • ψ
⊢ r₁ * ↑ϕ { val := y, property := (_ : y ∈ O) } + r₂ * ↑ψ { val := y, property := (_ : y ∈ O) } = d
ι : Type ?u.26829
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : ι → M
N O : Submodule R M
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
y : M
yN : y ∈ N
ϕy_eq : ↑ϕ { val := y, property := (_ : y ∈ O) } = generator (LinearMap.submoduleImage ϕ N)
ψ : { x // x ∈ O } →ₗ[R] R
a : R := generator (LinearMap.submoduleImage ϕ N)
d : R := generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ↑ψ { val := y, property := (_ : y ∈ O) }
r₁ r₂ : R
d_eq : d = r₁ * a + r₂ * ↑ψ { val := y, property := (_ : y ∈ O) }
ψ' : { x // x ∈ O } →ₗ[R] R := r₁ • ϕ + r₂ • ψ
⊢ ↑ψ' { val := y, property := (_ : y ∈ O) } = d
change r₁ * ϕ ⟨y, hNO yN⟩ + r₂ * ψ ⟨y, hNO yN⟩ = d
no goals
ι : Type ?u.26829
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : ι → M
N O : Submodule R M
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
y : M
yN : y ∈ N
ϕy_eq : ↑ϕ { val := y, property := (_ : y ∈ O) } = generator (LinearMap.submoduleImage ϕ N)
ψ : { x // x ∈ O } →ₗ[R] R
a : R := generator (LinearMap.submoduleImage ϕ N)
d : R := generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ↑ψ { val := y, property := (_ : y ∈ O) }
r₁ r₂ : R
d_eq : d = r₁ * a + r₂ * ↑ψ { val := y, property := (_ : y ∈ O) }
ψ' : { x // x ∈ O } →ₗ[R] R := r₁ • ϕ + r₂ • ψ
⊢ r₁ * ↑ϕ { val := y, property := (_ : y ∈ O) } + r₂ * ↑ψ { val := y, property := (_ : y ∈ O) } = d
rw [d_eq, ϕy_eq]
no goals
ι : Type ?u.26829
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : ι → M
N O : Submodule R M
hNO : N ≤ O
ϕ : { x // x ∈ O } →ₗ[R] R
hϕ : ∀ (ψ : { x // x ∈ O } →ₗ[R] R), ¬LinearMap.submoduleImage ϕ N < LinearMap.submoduleImage ψ N
inst✝ : IsPrincipal (LinearMap.submoduleImage ϕ N)
y : M
yN : y ∈ N
ϕy_eq : ↑ϕ { val := y, property := (_ : y ∈ O) } = generator (LinearMap.submoduleImage ϕ N)
ψ : { x // x ∈ O } →ₗ[R] R
a : R := generator (LinearMap.submoduleImage ϕ N)
d : R := generator (span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ↑ψ { val := y, property := (_ : y ∈ O) }
⊢ generator (LinearMap.submoduleImage ϕ N) ∈ span R {a, ↑ψ { val := y, property := (_ : y ∈ O) }}
exact subset_span (mem_insert _ _)